1 (* ========================================================================= *)
3 (* Isabelle/Procedural style additions and other user-friendly shortcuts. *)
5 (* Petros Papapanagiotou, Jacques Fleuriot *)
6 (* Center of Intelligent Systems and their Applications *)
7 (* University of Edinburgh *)
9 (* ========================================================================= *)
10 (* FILE : new_tactics.ml *)
11 (* DESCRIPTION : Various tactics to facilitate procedural-style users. *)
12 (* Mostly inspired by Isabelle's similar tactics. *)
13 (* LAST MODIFIED: October 2012 *)
14 (* ========================================================================= *)
16 (* ------------------------------------------------------------------------- *)
17 (* e_all : tactic -> goalstack *)
18 (* Same as "e" but applies tactic to ALL subgoals. *)
19 (* ------------------------------------------------------------------------- *)
22 let c = (count_goals()) in
25 then (!current_goalstack)
26 else let _ = e tac in let _ = r 1 in f (i-1)
30 (* ------------------------------------------------------------------------- *)
32 (* Rotates assumptions N times. *)
33 (* ------------------------------------------------------------------------- *)
34 (* Pops the entire assumption list doing nothing (K ALL_TAC) then maps *)
35 (* LABEL_TAC to the rotated list of assumptions. The list is reversed so as *)
36 (* to match the external order. The result is applied to (asl,w) so as to *)
37 (* obtain the resulting goalstate as required by the tactic type. *)
38 (* ------------------------------------------------------------------------- *)
40 let (ROTATE_N_TAC :int->tactic) =
42 let rotateasm = fun (asl) -> (tl asl)@[hd asl] in
43 (POP_ASSUM_LIST(K ALL_TAC) THEN
44 MAP_EVERY (fun (s,th) -> LABEL_TAC s th) (funpow n rotateasm (rev asl)))
48 (* ------------------------------------------------------------------------- *)
50 (* Rotates assumptions once. *)
51 (* ------------------------------------------------------------------------- *)
53 let (ROTATE_TAC :tactic) = (ROTATE_N_TAC 1);;
57 (* ------------------------------------------------------------------------- *)
59 (* Applies an inference rule to Nth assumption only. *)
60 (* Like drule for HOL Light's inference rules without matching. *)
61 (* ------------------------------------------------------------------------- *)
62 (* Works like RULE_ASSUM_TAC except it numbers the assumption list with *)
63 (* num_list and only applies the rule to the Nth assumption. *)
64 (* ------------------------------------------------------------------------- *)
66 let (DRULE_N_TAC :int->(thm->thm)->tactic) =
67 fun n rule (asl,w) -> (POP_ASSUM_LIST(K ALL_TAC) THEN
68 MAP_EVERY (fun (i,(s,th)) -> LABEL_TAC s (if (i=n) then (rule th) else th))
69 (num_list(rev asl))) (asl,w);;
73 (* ------------------------------------------------------------------------- *)
75 (* Applies an inference rule to Nth assumption only then adds the result as *)
76 (* a new assumption. *)
77 (* Like frule for HOL Light's inference rules without matching. *)
78 (* ------------------------------------------------------------------------- *)
79 (* Works like DRULE_N_TAC except it leaves the assumption intact and *)
80 (* adds the result as a new assumption. *)
81 (* ------------------------------------------------------------------------- *)
83 let (FRULE_N_TAC :int->(thm->thm)->tactic) =
84 fun n rule (asl,w) -> (
85 let asmlist = num_list(rev asl) in
86 let (_,asm_n) = try assoc n asmlist with Failure _ ->
87 failwith("FRULE_N_TAC: didn't find assumption "^string_of_int(n)) in
88 ASSUME_TAC (rule asm_n)) (asl,w);;
92 (* ------------------------------------------------------------------------- *)
94 (* Applies an inference rule (such as MP) to the Mth and Nth assumptions and *)
95 (* adds the result as a new assumption. *)
96 (* ------------------------------------------------------------------------- *)
97 (* Numbers the assumption list, finds the Mth and Nth assumptions, applies *)
98 (* the rule to them and adds the result as a new assumption. *)
99 (* ------------------------------------------------------------------------- *)
101 let (FRULE_MN_TAC :int->int->(thm->thm->thm)->tactic) =
102 fun m n rule (asl,w) -> (
103 let asmlist = num_list(rev asl) in
104 let (_,asm_m) = try assoc m asmlist with Failure _ ->
105 failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(m)) in
106 let (_,asm_n) = try assoc n asmlist with Failure _ ->
107 failwith("FRULE_MN_TAC: didn't find assumption "^string_of_int(n)) in
108 ASSUME_TAC (rule asm_m asm_n)) (asl,w);;
113 (* ------------------------------------------------------------------------- *)
114 (* ----------------------- SIMP TACTICS START HERE!! ----------------------- *)
115 (* ------------------------------------------------------------------------- *)
117 (* ------------------------------------------------------------------------- *)
118 (* GENERAL_ASM_TAC: (thm list -> thm -> thm) -> thm list -> tactic *)
119 (* General function that uses a rewrite rule to rewrite the assumptions. *)
120 (* Each assumption is rewritten using the rest of the assumptions and the *)
121 (* given list of theorems. *)
122 (* ------------------------------------------------------------------------- *)
123 (* A filter is applied to ensure that the assumption is not used to rewrite *)
125 (* ------------------------------------------------------------------------- *)
127 let GENERAL_ASM_TAC = fun rule thl (asl,w) ->
128 let asm = map snd asl in
129 (POP_ASSUM_LIST(K ALL_TAC) THEN
130 MAP_EVERY (fun (s,th) -> LABEL_TAC s
131 (rule ((filter (fun x -> not (th = x)) asm) @ thl) th)
132 ) (rev asl)) (asl,w);;
134 (* ------------------------------------------------------------------------- *)
135 (* Using the above GENERAL_ASSUM_TAC, we define 4 tactics to rewrite *)
136 (* assumptions based on the 4 rewrite rules available in HOL Light. *)
137 (* ------------------------------------------------------------------------- *)
139 let REWRITE_ASM_TAC,ONCE_REWRITE_ASM_TAC,PURE_REWRITE_ASM_TAC,
140 PURE_ONCE_REWRITE_ASM_TAC =
141 GENERAL_ASM_TAC REWRITE_RULE,
142 GENERAL_ASM_TAC ONCE_REWRITE_RULE,
143 GENERAL_ASM_TAC PURE_REWRITE_RULE,
144 GENERAL_ASM_TAC PURE_ONCE_REWRITE_RULE;;
146 (* ------------------------------------------------------------------------- *)
147 (* And for simplification. *)
148 (* ------------------------------------------------------------------------- *)
150 let SIMP_ASM_TAC,ONCE_SIMP_ASM_TAC,PURE_SIMP_ASM_TAC =
151 GENERAL_ASM_TAC SIMP_RULE,
152 GENERAL_ASM_TAC ONCE_SIMP_RULE,
153 GENERAL_ASM_TAC PURE_SIMP_RULE;;
155 (* ------------------------------------------------------------------------- *)
156 (* FULL_REWRITE_TAC : thm list -> tactic *)
157 (* simp : thm list -> tactic *)
158 (* Similar to Isabelle's simp. Rewrites assumptions then rewrites goal *)
159 (* using the assumptions. *)
160 (* ------------------------------------------------------------------------- *)
162 let FULL_REWRITE_TAC thl =
163 REWRITE_ASM_TAC thl THEN ASM_SIMP_TAC thl;;
165 let simp = FULL_REWRITE_TAC;;
167 (* ------------------------------------------------------------------------- *)
168 (* FULL_SIMP_TAC : thm list -> tactic *)
169 (* Hybrid simplifier. Uses HOL Light's SIMP_TAC then FULL_REWRITE_TAC. *)
170 (* ------------------------------------------------------------------------- *)
172 let FULL_SIMP_TAC thl =
173 SIMP_TAC thl THEN REWRITE_ASM_TAC thl THEN ASM_REWRITE_TAC thl;;
177 (* ------------------------------------------------------------------------- *)
178 (* assumption (tactic): *)
179 (* Shortcut to match an assumption to the goal as Isabelle's "assumption". *)
180 (* ------------------------------------------------------------------------- *)
182 let assumption = FIRST_ASSUM MATCH_ACCEPT_TAC;;
185 (* ------------------------------------------------------------------------- *)
186 (* ALL_UNIFY_ACCEPT_TAC (term list -> thm -> tactic): *)
187 (* Altered UNIFY_ACCEPT_TAC. Uses INSTANTIATE_ALL instead of INSTANTIATE. *)
188 (* ------------------------------------------------------------------------- *)
189 (* This allows for some valid instantiations that weren't otherwise allowed. *)
190 (* eg After using allE, the `a` metavariable can't be instantiated otherwise.*)
191 (* ------------------------------------------------------------------------- *)
193 let ALL_UNIFY_ACCEPT_TAC mvs th (asl,w) =
194 let insts = term_unify mvs (concl th) w in
196 let th' = INSTANTIATE_ALL insts th in
197 fun i [] -> INSTANTIATE_ALL i th';;
201 (* ------------------------------------------------------------------------- *)
202 (* meta_assumption (term list -> tactic): *)
203 (* Shortcut to match an assumption to the goal as Isabelle's "assumption". *)
204 (* This version also tries unification by instantiation of meta-variables *)
205 (* which, unfortunately, need to be given manually in a list. *)
206 (* ------------------------------------------------------------------------- *)
207 (* Invalid instantiations may be produced. *)
208 (* eg g `!x:num. (?a:num. R a x) ==> (?y. R y x)`;; *)
210 (* e (rule impI);; *)
212 (* e (FIRST_X_ASSUM (X_CHOOSE_TAC `b:num`));; *)
213 (* e (meta_assumption [`a:num`]);; *)
214 (* This succeeds but top_thm() is unable to reconstruct the theorem. *)
215 (* ------------------------------------------------------------------------- *)
217 let meta_assumption mvs = (FIRST_ASSUM MATCH_ACCEPT_TAC) ORELSE
218 (FIRST_ASSUM (ALL_UNIFY_ACCEPT_TAC mvs));;
221 (* ------------------------------------------------------------------------- *)
222 (* Shortcut for interactive proofs so that you don't have to enumerate *)
224 (* ------------------------------------------------------------------------- *)
226 let ema () = (e o meta_assumption o top_metas o p) () ;;
229 (* ------------------------------------------------------------------------- *)
230 (* X_MATCH_CHOOSE_TAC : (term -> tactic) *)
231 (* Version of X_CHOOSE_TAC with type matching. *)
232 (* ------------------------------------------------------------------------- *)
233 (* If the variable given as an argument has a vartype then its type is *)
234 (* instantiated to the type of the existentially quantified variable. *)
235 (* Usefull so that the user need not specify the type for his variable. *)
236 (* It is still acceptable if the user does specify it. *)
237 (* ------------------------------------------------------------------------- *)
239 let (X_MATCH_CHOOSE_TAC: term -> thm_tactic) =
241 try let xtm = concl xth in
242 let x,bod = dest_exists xtm in
243 let x'type = type_of x' in
244 let x'' = if (is_vartype x'type) then
245 inst (type_match x'type (type_of x) []) x'
247 let pat = vsubst[x'',x] bod in
248 let xth' = ASSUME pat in
250 let avoids = itlist (union o frees o concl o snd) asl
251 (union (frees w) (thm_frees xth)) in
252 if mem x' avoids then failwith "X_CHOOSE_TAC" else
253 null_meta,[("",xth')::asl,w],
254 fun i [th] -> CHOOSE(x'',INSTANTIATE_ALL i xth) th
255 with Failure _ -> failwith "X_CHOOSE_TAC";;
260 (* ------------------------------------------------------------------------- *)
261 (* exE : (term -> tactic) *)
262 (* Existential elimination tactic (since we are unable to accommodate *)
263 (* erule exE with the current meta_rule system because of lack of meta-level *)
264 (* quantification). *)
265 (* ------------------------------------------------------------------------- *)
267 let exE = FIRST_X_ASSUM o X_MATCH_CHOOSE_TAC;;
270 (* ------------------------------------------------------------------------- *)
271 (* allI : (term -> tactic) *)
272 (* Universal introduction tactic (since we are unable to accommodate *)
273 (* rule allI with the current meta_rule system because of lack of meta-level *)
274 (* quantification). *)
275 (* ------------------------------------------------------------------------- *)
276 (* (+) We can use X_GEN_TAC to allow the user to give his own term, but *)
277 (* this is rarely useful in procedural style proofs. *)
278 (* ------------------------------------------------------------------------- *)
283 (* ------------------------------------------------------------------------- *)
284 (* qed : (unit -> thm) *)
285 (* Reconstructs the theorem at the end of an interactive proof. *)
286 (* May fail if an incorrect metavariable instantiation has occured during the*)
288 (* ------------------------------------------------------------------------- *)
289 (* (+) There are plans to upgrade this for better accommodation of proofs *)
290 (* containing meta-level implication (see meta_rules.ml and gmm). *)
291 (* ------------------------------------------------------------------------- *)
296 (* ------------------------------------------------------------------------- *)
297 (* ASM_STRUCT_CASES_TAC : (thm_tactic) *)
298 (* Replacement/fix of STRUCT_CASES_TAC where each case is added as an *)
299 (* assumption like ASM_CASES_TAC does for booleans. *)
300 (* ------------------------------------------------------------------------- *)
302 let ASM_STRUCT_CASES_TAC =
303 REPEAT_TCL STRIP_THM_THEN ASSUME_TAC;;
305 (* ------------------------------------------------------------------------- *)
306 (* case_tac : (term -> tactic) *)
307 (* Isabelle's case_tac for splitting cases. *)
308 (* ------------------------------------------------------------------------- *)
310 let (case_tac:term->tactic) =
311 fun tm ((_,w) as g) ->
312 let trymatch = fun tm1 tm2 ->
313 try ( let inst = term_match (gl_frees g) tm1 tm2 in
319 with Failure _ -> false in
320 let tm' = try (find_term (trymatch tm) w)
321 with Failure _ -> tm in
322 let ty = (fst o dest_type o type_of) tm' in
323 let thm = try (cases ty)
324 with Failure _ -> failwith ("case_tac: Failed to find cases theorem for type \"" ^ ty ^ "\".") in
325 ASM_STRUCT_CASES_TAC (ISPEC tm' thm) g;;
328 (* ------------------------------------------------------------------------- *)
329 (* gen_case_tac : tactic *)
330 (* Case split on the leading universal quantifier of the goal. *)
331 (* ------------------------------------------------------------------------- *)
333 let (gen_case_tac:tactic) =
335 case_tac ((fst o dest_forall) w) g;;
338 (* ------------------------------------------------------------------------- *)
339 (* subgoal_tac : (term -> tactic) *)
340 (* Introduces a new subgoal which gets added as an assumption. *)
341 (* Isabelle's subgoal_tac. *)
342 (* ------------------------------------------------------------------------- *)
344 let subgoal_tac = fun tm -> SUBGOAL_THEN tm ASSUME_TAC;;
347 (* ------------------------------------------------------------------------- *)
348 (* meson : (thm list -> tactic) *)
349 (* Lower-case shortcut for ASM_MESON_TAC *)
350 (* ------------------------------------------------------------------------- *)
352 let meson = ASM_MESON_TAC;;