Update from HH
[hl193./.git] / IsabelleLight / new_tactics.ml
1 (* ========================================================================= *)
2 (*                              Isabelle Light                               *)
3 (*   Isabelle/Procedural style additions and other user-friendly shortcuts.  *)
4 (*                                                                           *)
5 (*                   Petros Papapanagiotou, Jacques Fleuriot                 *)
6 (*              Center of Intelligent Systems and their Applications         *)
7 (*                          University of Edinburgh                          *)
8 (*                                 2009-2010                                 *)
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 (* ========================================================================= *)
15
16 (* ------------------------------------------------------------------------- *)
17 (* e_all : tactic -> goalstack                                               *) 
18 (* Same as "e" but applies tactic to ALL subgoals.                           *)
19 (* ------------------------------------------------------------------------- *)
20
21 let e_all tac =
22   let c = (count_goals()) in
23   let rec f i = ( 
24     if (i = 0) 
25     then (!current_goalstack) 
26     else let _ = e tac in let _ = r 1 in f (i-1) 
27    ) in f c;;
28
29
30 (* ------------------------------------------------------------------------- *)
31 (* ROTATE_N_TAC:                                                             *)
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 (* ------------------------------------------------------------------------- *)
39
40 let (ROTATE_N_TAC :int->tactic) = 
41   fun n (asl,w) ->
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))) 
45       (asl,w);;
46
47
48 (* ------------------------------------------------------------------------- *)
49 (* ROTATE_TAC:                                                               *)
50 (* Rotates assumptions once.                                                 *)
51 (* ------------------------------------------------------------------------- *)
52
53 let (ROTATE_TAC :tactic) = (ROTATE_N_TAC 1);;
54
55
56
57 (* ------------------------------------------------------------------------- *)
58 (* DRULE_N_TAC:                                                              *)
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 (* ------------------------------------------------------------------------- *)
65
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);;
70
71
72
73 (* ------------------------------------------------------------------------- *)
74 (* FRULE_N_TAC:                                                              *)
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 (* ------------------------------------------------------------------------- *)
82
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);;
89
90
91
92 (* ------------------------------------------------------------------------- *)
93 (* FRULE_MN_TAC:                                                       *)
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 (* ------------------------------------------------------------------------- *)
100
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);;
109
110
111
112
113 (* ------------------------------------------------------------------------- *)
114 (* ----------------------- SIMP TACTICS START HERE!! ----------------------- *)
115 (* ------------------------------------------------------------------------- *)
116
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  *)
124 (* itself.                                                                   *)
125 (* ------------------------------------------------------------------------- *)
126
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);;
133
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 (* ------------------------------------------------------------------------- *)
138
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;;
145
146 (* ------------------------------------------------------------------------- *)
147 (* And for simplification.                                                   *)
148 (* ------------------------------------------------------------------------- *)
149
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;;
154
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 (* ------------------------------------------------------------------------- *)
161
162 let FULL_REWRITE_TAC thl = 
163   REWRITE_ASM_TAC thl THEN ASM_SIMP_TAC thl;;
164
165 let simp = FULL_REWRITE_TAC;;
166
167 (* ------------------------------------------------------------------------- *)
168 (* FULL_SIMP_TAC : thm list -> tactic                                        *)
169 (* Hybrid simplifier. Uses HOL Light's SIMP_TAC then FULL_REWRITE_TAC.       *)
170 (* ------------------------------------------------------------------------- *)
171
172 let FULL_SIMP_TAC thl = 
173   SIMP_TAC thl THEN REWRITE_ASM_TAC thl THEN ASM_REWRITE_TAC thl;;
174
175
176
177 (* ------------------------------------------------------------------------- *)
178 (* assumption (tactic):                                                      *)
179 (* Shortcut to match an assumption to the goal as Isabelle's "assumption".   *)
180 (* ------------------------------------------------------------------------- *)
181
182 let assumption = FIRST_ASSUM MATCH_ACCEPT_TAC;;
183
184
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 (* ------------------------------------------------------------------------- *)
192
193 let ALL_UNIFY_ACCEPT_TAC mvs th (asl,w) =
194   let insts = term_unify mvs (concl th) w in
195   ([],insts),[],
196   let th' = INSTANTIATE_ALL insts th in
197   fun i [] -> INSTANTIATE_ALL i th';;
198
199
200
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)`;;                          *)
209 (*    e GEN_TAC;;                                                            *)
210 (*    e (rule impI);;                                                        *)
211 (*    e (rule exI);;                                                         *)
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 (* ------------------------------------------------------------------------- *)
216
217 let meta_assumption mvs = (FIRST_ASSUM MATCH_ACCEPT_TAC) ORELSE 
218                       (FIRST_ASSUM (ALL_UNIFY_ACCEPT_TAC mvs));;
219
220
221 (* ------------------------------------------------------------------------- *)
222 (* Shortcut for interactive proofs so that you don't have to enumerate       *)
223 (* metavariables.                                                            *)
224 (* ------------------------------------------------------------------------- *)
225
226 let ema () = (e o meta_assumption o top_metas o p) ()  ;;
227
228
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 (* ------------------------------------------------------------------------- *)
238
239 let (X_MATCH_CHOOSE_TAC: term -> thm_tactic) =
240   fun x' xth ->
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'
246         else x' in
247         let pat = vsubst[x'',x] bod in
248         let xth' = ASSUME pat in
249         fun (asl,w) ->
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";;
256
257
258
259
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 (* ------------------------------------------------------------------------- *)
266
267 let exE = FIRST_X_ASSUM o X_MATCH_CHOOSE_TAC;;
268
269
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 (* ------------------------------------------------------------------------- *)
279
280 let allI = GEN_TAC;;
281
282
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*)
287 (* proof.                                                                    *)
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 (* ------------------------------------------------------------------------- *)
292
293 let qed = top_thm;;
294
295
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 (* ------------------------------------------------------------------------- *)
301
302 let ASM_STRUCT_CASES_TAC =
303     REPEAT_TCL STRIP_THM_THEN ASSUME_TAC;;
304
305 (* ------------------------------------------------------------------------- *)
306 (* case_tac : (term -> tactic)                                               *)
307 (* Isabelle's case_tac for splitting cases.                                  *)
308 (* ------------------------------------------------------------------------- *)
309
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
314             if (is_var tm1) 
315             then match inst with
316                 [],[],_ -> true
317               | _  -> false
318             else true )
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;;
326
327
328 (* ------------------------------------------------------------------------- *)
329 (* gen_case_tac : tactic                                                     *)
330 (* Case split on the leading universal quantifier of the goal.               *)
331 (* ------------------------------------------------------------------------- *)
332
333 let (gen_case_tac:tactic) =
334   fun ((_,w) as g) ->
335     case_tac ((fst o dest_forall) w) g;;
336
337
338 (* ------------------------------------------------------------------------- *)
339 (* subgoal_tac : (term -> tactic)                                            *)
340 (* Introduces a new subgoal which gets added as an assumption.               *)
341 (* Isabelle's subgoal_tac.                                                   *)
342 (* ------------------------------------------------------------------------- *)
343
344 let subgoal_tac = fun tm -> SUBGOAL_THEN tm ASSUME_TAC;;
345
346
347 (* ------------------------------------------------------------------------- *)
348 (* meson : (thm list -> tactic)                                              *)
349 (* Lower-case shortcut for ASM_MESON_TAC                                     *)
350 (* ------------------------------------------------------------------------- *)
351
352 let meson = ASM_MESON_TAC;;
353