src/Provers/clasimp.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69593 3dda49e08b9d
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Provers/clasimp.ML
     2     Author:     David von Oheimb, TU Muenchen
     3 
     4 Combination of classical reasoner and simplifier (depends on
     5 splitter.ML, classical.ML, blast.ML).
     6 *)
     7 
     8 signature CLASIMP_DATA =
     9 sig
    10   structure Splitter: SPLITTER
    11   structure Classical: CLASSICAL
    12   structure Blast: BLAST
    13   val notE: thm
    14   val iffD1: thm
    15   val iffD2: thm
    16 end;
    17 
    18 signature CLASIMP =
    19 sig
    20   val addSss: Proof.context -> Proof.context
    21   val addss: Proof.context -> Proof.context
    22   val clarsimp_tac: Proof.context -> int -> tactic
    23   val mk_auto_tac: Proof.context -> int -> int -> tactic
    24   val auto_tac: Proof.context -> tactic
    25   val force_tac: Proof.context -> int -> tactic
    26   val fast_force_tac: Proof.context -> int -> tactic
    27   val slow_simp_tac: Proof.context -> int -> tactic
    28   val best_simp_tac: Proof.context -> int -> tactic
    29   val iff_add: attribute
    30   val iff_add': attribute
    31   val iff_del: attribute
    32   val iff_modifiers: Method.modifier parser list
    33   val clasimp_modifiers: Method.modifier parser list
    34 end;
    35 
    36 functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
    37 struct
    38 
    39 structure Splitter = Data.Splitter;
    40 structure Classical = Data.Classical;
    41 structure Blast = Data.Blast;
    42 
    43 
    44 (* simp as classical wrapper *)
    45 
    46 (* FIXME !? *)
    47 fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
    48 
    49 (*Add a simpset to the claset!*)
    50 (*Caution: only one simpset added can be added by each of addSss and addss*)
    51 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
    52 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
    53 
    54 
    55 (* iffs: addition of rules to simpsets and clasets simultaneously *)
    56 
    57 local
    58 
    59 (*Takes (possibly conditional) theorems of the form A<->B to
    60         the Safe Intr     rule B==>A and
    61         the Safe Destruct rule A==>B.
    62   Also ~A goes to the Safe Elim rule A ==> ?R
    63   Failing other cases, A is added as a Safe Intr rule*)
    64 
    65 fun add_iff safe unsafe =
    66   Thm.declaration_attribute (fn th => fn context =>
    67     let
    68       val n = Thm.nprems_of th;
    69       val (elim, intro) = if n = 0 then safe else unsafe;
    70       val zero_rotate = zero_var_indexes o rotate_prems n;
    71       val decls =
    72         [(intro, zero_rotate (th RS Data.iffD2)),
    73          (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
    74         handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
    75         handle THM _ => [(intro, th)];
    76     in fold (uncurry Thm.attribute_declaration) decls context end);
    77 
    78 fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
    79   let
    80     val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
    81     val rls =
    82       [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
    83         handle THM _ => [zero_rotate (th RS Data.notE)]
    84         handle THM _ => [th];
    85   in fold (Thm.attribute_declaration del) rls context end);
    86 
    87 in
    88 
    89 val iff_add =
    90   Thm.declaration_attribute (fn th =>
    91     Thm.attribute_declaration (add_iff
    92       (Classical.safe_elim NONE, Classical.safe_intro NONE)
    93       (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
    94     #> Thm.attribute_declaration Simplifier.simp_add th);
    95 
    96 val iff_add' =
    97   add_iff
    98     (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
    99     (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
   100 
   101 val iff_del =
   102   Thm.declaration_attribute (fn th =>
   103     Thm.attribute_declaration (del_iff Classical.rule_del) th #>
   104     Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
   105     Thm.attribute_declaration Simplifier.simp_del th);
   106 
   107 end;
   108 
   109 
   110 (* tactics *)
   111 
   112 fun clarsimp_tac ctxt =
   113   Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
   114   Classical.clarify_tac (addSss ctxt);
   115 
   116 
   117 (* auto_tac *)
   118 
   119 (* a variant of depth_tac that avoids interference of the simplifier
   120    with dup_step_tac when they are combined by auto_tac *)
   121 local
   122 
   123 fun slow_step_tac' ctxt =
   124   Classical.appWrappers ctxt
   125     (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt);
   126 
   127 in
   128 
   129 fun nodup_depth_tac ctxt m i st =
   130   SELECT_GOAL
   131     (Classical.safe_steps_tac ctxt 1 THEN_ELSE
   132       (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
   133         Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
   134           (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
   135 
   136 end;
   137 
   138 (*Designed to be idempotent, except if Blast.depth_tac instantiates variables
   139   in some of the subgoals*)
   140 fun mk_auto_tac ctxt m n =
   141   let
   142     val main_tac =
   143       Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
   144       ORELSE'
   145       (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
   146   in
   147     PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
   148     TRY (Classical.safe_tac ctxt) THEN
   149     REPEAT_DETERM (FIRSTGOAL main_tac) THEN
   150     TRY (Classical.safe_tac (addSss ctxt)) THEN
   151     prune_params_tac ctxt
   152   end;
   153 
   154 fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
   155 
   156 
   157 (* force_tac *)
   158 
   159 (* aimed to solve the given subgoal totally, using whatever tools possible *)
   160 fun force_tac ctxt =
   161   let val ctxt' = addss ctxt in
   162     SELECT_GOAL
   163      (Classical.clarify_tac ctxt' 1 THEN
   164       IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
   165       ALLGOALS (Classical.first_best_tac ctxt'))
   166   end;
   167 
   168 
   169 (* basic combinations *)
   170 
   171 val fast_force_tac = Classical.fast_tac o addss;
   172 val slow_simp_tac = Classical.slow_tac o addss;
   173 val best_simp_tac = Classical.best_tac o addss;
   174 
   175 
   176 
   177 (** concrete syntax **)
   178 
   179 (* attributes *)
   180 
   181 val _ =
   182   Theory.setup
   183     (Attrib.setup @{binding iff}
   184       (Scan.lift
   185         (Args.del >> K iff_del ||
   186           Scan.option Args.add -- Args.query >> K iff_add' ||
   187           Scan.option Args.add >> K iff_add))
   188       "declaration of Simplifier / Classical rules");
   189 
   190 
   191 (* method modifiers *)
   192 
   193 val iffN = "iff";
   194 
   195 val iff_modifiers =
   196  [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
   197   Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
   198   Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
   199 
   200 val clasimp_modifiers =
   201   Simplifier.simp_modifiers @ Splitter.split_modifiers @
   202   Classical.cla_modifiers @ iff_modifiers;
   203 
   204 
   205 (* methods *)
   206 
   207 fun clasimp_method' tac =
   208   Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
   209 
   210 val auto_method =
   211   Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
   212     Method.sections clasimp_modifiers >>
   213   (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
   214     | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
   215 
   216 val _ =
   217   Theory.setup
   218    (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
   219     Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
   220     Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
   221     Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
   222     Method.setup @{binding auto} auto_method "auto" #>
   223     Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
   224       "clarify simplified goal");
   225 
   226 end;