1(* Title: Provers/clasimp.ML 2 Author: David von Oheimb, TU Muenchen 3 4Combination of classical reasoner and simplifier (depends on 5splitter.ML, classical.ML, blast.ML). 6*) 7 8signature CLASIMP_DATA = 9sig 10 structure Splitter: SPLITTER 11 structure Classical: CLASSICAL 12 structure Blast: BLAST 13 val notE: thm 14 val iffD1: thm 15 val iffD2: thm 16end; 17 18signature CLASIMP = 19sig 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 34end; 35 36functor Clasimp(Data: CLASIMP_DATA): CLASIMP = 37struct 38 39structure Splitter = Data.Splitter; 40structure Classical = Data.Classical; 41structure Blast = Data.Blast; 42 43 44(* simp as classical wrapper *) 45 46(* FIXME !? *) 47fun 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*) 51val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac; 52val 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 57local 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 65fun 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 78fun 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 87in 88 89val 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 96val 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 101val 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 107end; 108 109 110(* tactics *) 111 112fun 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 *) 121local 122 123fun slow_step_tac' ctxt = 124 Classical.appWrappers ctxt 125 (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt); 126 127in 128 129fun 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 136end; 137 138(*Designed to be idempotent, except if Blast.depth_tac instantiates variables 139 in some of the subgoals*) 140fun 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 154fun 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 *) 160fun 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 171val fast_force_tac = Classical.fast_tac o addss; 172val slow_simp_tac = Classical.slow_tac o addss; 173val best_simp_tac = Classical.best_tac o addss; 174 175 176 177(** concrete syntax **) 178 179(* attributes *) 180 181val _ = 182 Theory.setup 183 (Attrib.setup \<^binding>\<open>iff\<close> 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 193val iffN = "iff"; 194 195val 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 200val clasimp_modifiers = 201 Simplifier.simp_modifiers @ Splitter.split_modifiers @ 202 Classical.cla_modifiers @ iff_modifiers; 203 204 205(* methods *) 206 207fun clasimp_method' tac = 208 Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac); 209 210val 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 216val _ = 217 Theory.setup 218 (Method.setup \<^binding>\<open>fastforce\<close> (clasimp_method' fast_force_tac) "combined fast and simp" #> 219 Method.setup \<^binding>\<open>slowsimp\<close> (clasimp_method' slow_simp_tac) "combined slow and simp" #> 220 Method.setup \<^binding>\<open>bestsimp\<close> (clasimp_method' best_simp_tac) "combined best and simp" #> 221 Method.setup \<^binding>\<open>force\<close> (clasimp_method' force_tac) "force" #> 222 Method.setup \<^binding>\<open>auto\<close> auto_method "auto" #> 223 Method.setup \<^binding>\<open>clarsimp\<close> (clasimp_method' (CHANGED_PROP oo clarsimp_tac)) 224 "clarify simplified goal"); 225 226end; 227