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 : meta_rules.ml *)
11 (* DESCRIPTION : Meta rules is a formalisation used to accommodate *)
12 (* Isabelle's inference rules in HOL Light.The technical *)
13 (* details are described in the comments that follow. *)
14 (* Isabelle rule application tactics (rule, erule, etc.) have *)
15 (* been defined to work with meta rules. *)
16 (* We have not been able to accommodate first order rules *)
17 (* allI and exE. We also make use of metavariables which are *)
18 (* restricted by the limitations of term_unify *)
19 (* (ie. no HO unification and no type instantiation). *)
20 (* LAST MODIFIED: October 2012 *)
21 (* ========================================================================= *)
23 (* ------------------------------------------------------------------------- *)
24 (* ----------------------- META-LEVEL IMPLICATION -------------------------- *)
25 (* ------------------------------------------------------------------------- *)
26 (* Emulation of meta-level implication at the object level. *)
27 (* This is purely for syntax and parsing purposes. It solves a number of *)
28 (* problems when parsing theorems as meta-rules (see below). *)
29 (* It is applied at the logic level only for transparency. *)
30 (* ------------------------------------------------------------------------- *)
31 (* Thanks to Phil Scott for the suggestion. *)
32 (* ------------------------------------------------------------------------- *)
35 (* ------------------------------------------------------------------------- *)
36 (* Syntax definition. *)
37 (* ------------------------------------------------------------------------- *)
39 parse_as_infix ("===>",(4,"right"));;
41 let is_mimp = is_binary "===>";;
42 let dest_mimp = dest_binary "===>";;
45 (* ------------------------------------------------------------------------- *)
46 (* Logic definition: Equivalent to object-level implication. *)
47 (* ------------------------------------------------------------------------- *)
49 let MIMP_DEF = new_basic_definition
50 `(===>) = \p q. p ==> q`;;
53 (* ------------------------------------------------------------------------- *)
54 (* CONV, RULE and TACTIC to get rid of meta-level implication in proofs. *)
55 (* ------------------------------------------------------------------------- *)
57 let MIMP_TO_IMP_CONV = BETA_RULE o (PURE_REWRITE_CONV [MIMP_DEF]);;
58 let MIMP_TO_IMP_RULE = BETA_RULE o (PURE_REWRITE_RULE [MIMP_DEF]);;
59 let MIMP_TAC = (PURE_REWRITE_TAC [MIMP_DEF]) THEN BETA_TAC;;
62 (* ------------------------------------------------------------------------- *)
63 (* Equivalent of TAUT after getting rid of meta-level implication. *)
64 (* Helps prove simple propositional meta-rules easily. *)
65 (* ------------------------------------------------------------------------- *)
68 let th = MIMP_TO_IMP_CONV tm in
69 EQ_MP (SYM th) ((TAUT o snd o dest_iff o concl) th);;
72 (* ------------------------------------------------------------------------- *)
73 (* RULE to replace implication by meta-level implication to easily create *)
74 (* meta-theorems from normal theorems. *)
75 (* ------------------------------------------------------------------------- *)
77 let MIMP_THM = MTAUT `(p==>q) <=> (p===>q)`;;
78 let MIMP_RULE = PURE_REWRITE_RULE[MIMP_THM];;
81 (* ------------------------------------------------------------------------- *)
82 (* UNDISCH for meta-level implication. *)
83 (* Also gets rid of meta-level implication in the undischarged term. *)
84 (* ------------------------------------------------------------------------- *)
87 let mth = BETA_RULE (AP_THM (AP_THM MIMP_DEF `p:bool`) `q:bool`) in
88 let th = PURE_ONCE_REWRITE_RULE [mth] th in
89 try let undisch_tm = (rand o rator o concl) th in
90 PROVE_HYP ((UNDISCH o snd o EQ_IMP_RULE o MIMP_TO_IMP_CONV) undisch_tm) (UNDISCH th)
91 with Failure _ -> failwith "MUNDISCH";;
94 (* ------------------------------------------------------------------------- *)
95 (* -------------------------- HELPFUL FUNCTIONS ---------------------------- *)
96 (* ------------------------------------------------------------------------- *)
98 (* ------------------------------------------------------------------------- *)
99 (* REV_PART_MATCH_I: term list -> (term -> term) -> thm -> term *)
100 (* -> instantiation *)
101 (* Does a reverse PART_MATCH and returns the resulting instantiation. *)
102 (* Avoids instantiating any of the given variables/constants. *)
103 (* Does not apply SPEC_ALL like PART_MATCH does. *)
104 (* ------------------------------------------------------------------------- *)
105 (* The original PART_MATCH matches a term to part of a theorem so that we can*)
106 (* instantiate that part with the term. *)
107 (* The reverse used here, matches the part of the theorem with the term so *)
108 (* that the term can be instantiated with the part of the theorem. *)
109 (* We use this in cases such as erule where we want (part of) an assumption *)
110 (* to match a premise of the rule. We need the instantiation of the rule when*)
111 (* matched to the assumption (thm) and not the other way around. *)
112 (* ------------------------------------------------------------------------- *)
114 let REV_PART_MATCH_I =
115 let rec match_bvs t1 t2 acc =
116 try let v1,b1 = dest_abs t1
117 and v2,b2 = dest_abs t2 in
118 let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in
119 let newacc = if n1 = n2 then acc else insert (n1,n2) acc in
120 match_bvs b1 b2 newacc
121 with Failure _ -> try
122 let l1,r1 = dest_comb t1
123 and l2,r2 = dest_comb t2 in
124 match_bvs l1 l2 (match_bvs r1 r2 acc)
125 with Failure _ -> acc in
126 fun avoids partfn th ->
127 let bod = concl th in
128 let pbod = partfn bod in
129 let lconsts = union avoids (intersect (frees (concl th)) (freesl(hyp th))) in
131 let bvms = match_bvs pbod tm [] in
132 let atm = deep_alpha bvms tm in
133 term_match lconsts atm (partfn bod) ;; (* whereas in PART_MATCH we do it the other way around *)
136 (* ------------------------------------------------------------------------- *)
137 (* term_to_asm_match : term list -> term -> (string * thm) list -> *)
138 (* (string * thm) list * (thm * instantiation) *)
139 (* ------------------------------------------------------------------------- *)
140 (* term_to_asm_match tries to match key to one of the assumptions using *)
141 (* REV_PART_MATCH_I. Returns the new assumption list (with the matching *)
142 (* assumption removed), the matching assumption and the resulting *)
143 (* instantiation used. *)
144 (* ------------------------------------------------------------------------- *)
145 (* It is doubtful that this has practical use outside the Xrule_tac's. *)
146 (* It is used in erule, drule and frule to match the major premise to one of *)
147 (* the assumptions. *)
148 (* ------------------------------------------------------------------------- *)
150 let rec (term_to_asm_match: term list -> term -> (string * thm) list -> (string * thm) list * (thm * instantiation)) =
151 fun avoids key asms ->
152 if (asms = []) then failwith ("No assumptions match `" ^ (string_of_term key) ^ "`!")
154 let asm = (snd o hd) asms in
155 let i = REV_PART_MATCH_I avoids I asm key in
157 with Failure _ -> let res,inst = term_to_asm_match avoids key (tl asms) in ((hd asms)::res),inst;;
160 (* ------------------------------------------------------------------------- *)
161 (* term_to_asm_n_match : term list -> term -> (string * thm) list -> int -> *)
162 (* (string * thm) list * (thm * instantiation) *)
163 (* ------------------------------------------------------------------------- *)
164 (* Same as term_to_asm_match but only tries to match nth assumption. *)
165 (* ------------------------------------------------------------------------- *)
166 (* It is doubtful that this has practical use outside the Xrulen_tac's. *)
167 (* It is used in erulen, drulen and frulen to match the major premise to one *)
168 (* of the assumptions. *)
169 (* ------------------------------------------------------------------------- *)
171 let rec (term_to_asm_n_match: term list -> term -> (string * thm) list -> int -> (string * thm) list * (thm * instantiation)) =
172 fun avoids key asms n ->
173 if (asms = []) then failwith "No such assumption found!"
174 else try match n with
176 let asm = (snd o hd) asms in
177 let i = REV_PART_MATCH_I avoids I asm key in
179 | _ -> let re_asms,m = term_to_asm_n_match avoids key (tl asms) (n-1) in
181 with Failure _ -> failwith ("Assumption `" ^ ((string_of_term o concl o snd o hd) asms) ^ "` doesn't match `" ^ (string_of_term key) ^ "`!");;
185 (* gmm is not to be used until qed is updated *)
186 (* We need a MDISCH for that... *)
189 let fvs = sort (<) (map (fst o dest_var) (frees t)) in
191 let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
192 warn true ("Free variables in goal: "^errmsg)
194 let rec split_mimp = fun tm ->
197 let (a,b) = dest_mimp tm in
198 let (asms, concl) = split_mimp b in
201 set_goal (split_mimp t);;
204 (* ------------------------------------------------------------------------- *)
205 (* gm : term -> goalstack *)
206 (* This is used to set a term containing meta-level implication as a goal. *)
207 (* ------------------------------------------------------------------------- *)
208 (* (+) Uses g to set the goal then MIMP_TAC to get rid of meta-implication. *)
209 (* (+) Note that if the goal has normal implication it gets discharged as *)
210 (* well. This will be fixed when gmm is fixed. *)
211 (* ------------------------------------------------------------------------- *)
213 let gm t = g t ; e (MIMP_TAC THEN REPEAT DISCH_TAC);;
216 (* ------------------------------------------------------------------------- *)
217 (* Isabelle's natural deduction rules as thms with meta-level implication. *)
218 (* ------------------------------------------------------------------------- *)
220 let conjI = MTAUT `p===>q===>p/\q`;;
221 let conjunct1 = MTAUT `p/\q===>p`;;
222 let conjunct2 = MTAUT `p/\q===>q`;;
223 let conjE = MTAUT `p/\q===>(p===>q===>r)===>r`;;
224 let disjI1 = MTAUT `p===>p\/q`;;
225 let disjI2 = MTAUT `q===>p\/q`;;
226 let disjE = MTAUT `p\/q===>(p===>r)===>(q===>r)===>r`;;
228 let impI = MTAUT `(p===>q)===>(p==>q)`;;
229 let impE = MTAUT `(p==>q)===>p===>(q===>r)===>r`;;
230 let mp = MTAUT `(p==>q)===>(p===>q)`;;
232 let iffI = MTAUT `(a===>b)===>(b===>a)===>(a<=>b)`;;
233 let iffE = MTAUT `(a<=>b)===>((a==>b) ===> (b==>a) ===> r) ===> r`;;
235 let allE = prove( `(!x:A. P x) ===> (P (a:A) ===> (r:bool)) ===> r` ,
236 MIMP_TAC THEN MESON_TAC[]);;
237 let exI = prove (`P (a:A)===> ?x:A. P x`,
240 (EXISTS_TAC `a:A`) THEN
241 (FIRST_ASSUM ACCEPT_TAC));;
243 let notI = MTAUT `(p===>F)===> ~p`;;
244 let notE = MTAUT `~a ===> a ===> r`;;
247 (* ------------------------------------------------------------------------- *)
248 (* ------------------------------------------------------------------------- *)
249 (* ------------------------ META-RULES START HERE!! ------------------------ *)
250 (* ------------------------------------------------------------------------- *)
251 (* ------------------------------------------------------------------------- *)
253 (* ------------------------------------------------------------------------- *)
254 (* meta_rule (type) *)
255 (* The representation of an Isabelle inference rule in HOL Light. *)
256 (* ------------------------------------------------------------------------- *)
257 (* term = The conclusion of the inference rule. *)
258 (* goal list = The premises represented as "meta-subgoals". *)
259 (* thm = The representation of the rule as a theorem used for justification. *)
261 (* (+) thm must be of the form H1,H2,...,Hn |- G *)
262 (* (+) H1--Hn must be represented as "meta-subgoals" in any order (1) *)
263 (* (+) [|P;Q|] ==> R (in Isabelle notation) is translated as "meta-subgoal" *)
264 (* P,Q ?- R and as P==>Q==>R in the justification theorem. *)
265 (* (+) The form of the premises (assumption order etc) must be kept in the *)
266 (* justification theorem (see example in (2)) *)
267 (* (+) Use "mk_meta_rule" to create proper meta rules from theorems. *)
268 (* ------------------------------------------------------------------------- *)
269 (* (1) Since we use PROVE_HYP instead of MP to justify rule, erule etc, the *)
270 (* order of the subgoals is no longer essential. *)
271 (* (2) Example: conjE *)
272 (* In Isabelle: P/\Q [|P;Q|]==> R *)
273 (* ------------------ *)
276 (* As a meta rule (briefly - see conjEm below for full notation): *)
277 (* `R`, - conclusion *)
278 (* [ - premises list *)
282 (* `P/\Q, P==>Q==>R |- R` - justification theorem *)
284 (* The form of the premises must be preserved in the justification theorem. *)
285 (* ie. using `P/\Q, Q==>P==>R |- R` or `Q/\P, P==>Q==>R |- R` as a *)
286 (* justification theorem would break the justification and result in an *)
287 (* "invalid tactic" exception. *)
288 (* ------------------------------------------------------------------------- *)
290 type meta_rule = term * goal list * thm;;
293 let print_meta_rule: meta_rule->unit =
295 print_term c ; hd (map (print_newline () ; print_goal) glist) ;
296 print_newline () ; print_thm j ; print_newline ();;
299 (* ------------------------------------------------------------------------- *)
300 (* inst_meta_rule: instantiation -> meta_rule -> meta_rule *)
301 (* ------------------------------------------------------------------------- *)
302 (* Instantiates all parts of meta_rules based on an instantiation. *)
303 (* ------------------------------------------------------------------------- *)
305 let inst_meta_rule:instantiation->meta_rule->meta_rule =
306 fun inst (c,glist,j) ->
308 map (inst_goal inst) glist,
309 INSTANTIATE_ALL inst j;;
312 (* ------------------------------------------------------------------------- *)
313 (* meta_rule_frees: meta_rule -> term list *)
314 (* ------------------------------------------------------------------------- *)
315 (* Returns the list of free variables (or Isabelle ?metavariables) in a *)
317 (* ------------------------------------------------------------------------- *)
319 let meta_rule_frees: meta_rule -> term list =
321 itlist (union o gl_frees) glist (union (frees c) (thm_frees l));;
324 (* ------------------------------------------------------------------------- *)
325 (* meta_rule_mk_primed_vars_I: term_list -> meta_rule -> *)
326 (* meta_rule * instantiation *)
327 (* ------------------------------------------------------------------------- *)
328 (* Applies mk_primed_var to all the free variables in a meta_rule. *)
329 (* Returns the new meta_rule and the instantiation for the variable renaming.*)
330 (* ------------------------------------------------------------------------- *)
332 let meta_rule_mk_primed_vars_I: term list -> meta_rule -> meta_rule * instantiation =
334 let fvars = meta_rule_frees r in
335 let rec mk_primed_l = fun avoids vars ->
339 let new_v = mk_primed_var avoids v in
340 compose_insts (term_match [] v new_v) (mk_primed_l (new_v::avoids) rest)
342 let inst = mk_primed_l avoids fvars in
343 (inst_meta_rule inst r),inst;;
346 (* ------------------------------------------------------------------------- *)
347 (* meta_rule_mk_primed_vars: term_list -> meta_rule -> meta_rule *)
348 (* ------------------------------------------------------------------------- *)
349 (* Applies mk_primed_var to all the free variables in a meta_rule. *)
350 (* ------------------------------------------------------------------------- *)
352 let meta_rule_mk_primed_vars: term list -> meta_rule -> meta_rule =
353 fun avoids r -> fst (meta_rule_mk_primed_vars_I avoids r);;
357 (* ------------------------------------------------------------------------- *)
358 (* inst_meta_rule_vars: *)
359 (* (term * term) list -> meta_rule -> term list -> meta_rule *)
360 (* ------------------------------------------------------------------------- *)
361 (* Instantiates the free variables in a meta_rule. Also renames the *)
362 (* uninstantiated variables so as to avoid clashes with free variables and *)
363 (* constants in the given goal. *)
364 (* Essentially it prepares the meta_rule for use with any of xrulem_tac. *)
365 (* ------------------------------------------------------------------------- *)
366 (* (+) By instlist we mean the list of variables and instantiation pairs *)
367 (* given by the user. *)
368 (* (+) First we check the terms given as variables in the instlist. We must *)
369 (* check if they are indeed variables and if they are free variables in the *)
370 (* given meta_rule. *)
371 (* (+) "match_var" is used to compare a variable with a free variable in the *)
372 (* meta_rule. *NOTE* that a variable is accepted as long as it can match a *)
373 (* free variable in the meta_rule allowing only type instantiation. *)
374 (* (+) "mcheck_var" does the is_var check and tries to find a match with the *)
375 (* meta_rule's free vars (rfrees) using match_var. *)
376 (* (+) "mcheck_gvar" tries to match variables on the rhs of each instlist *)
377 (* pair with the free variables in the goal so as to instantiate their types *)
378 (* properly. This is done to free the user from declaring the variable types.*)
379 (* (+) Given variables are replaced with the meta_rule variables (effectively*)
380 (* achieving type instantiation) and later recombined into the instlist. *)
381 (* (+) Secondly, we rename all the variables in the meta_rule using *)
382 (* "meta_rule_mk_primed_vars_I" so that they don't match any of the free *)
383 (* variables in the goal. *)
384 (* (+) We use the same instantiation to rename instlist variables so that *)
385 (* they properly match the new variables of the meta_rule. *)
386 (* (+) "new_instlist" should contain variables that fully match primed *)
387 (* variables in the meta_rule (new_r). *)
388 (* (+) For each instlist pair, we find the instantiation that allows the *)
389 (* variable to be substituted by the given term. *NOTE* that no check is *)
390 (* made on that term. It is the user's responsibility to give a sensible, *)
391 (* matching and correctly typed term. *)
392 (* (+) All the instantiations produced by the instlist are composed into one *)
393 (* which is then applied to new_r to give the result. *)
394 (* ------------------------------------------------------------------------- *)
397 let inst_meta_rule_vars: (term * term) list -> meta_rule -> term list -> meta_rule =
398 fun instlist r gfrees ->
399 let rfrees = meta_rule_frees r in
400 let vars,subs = List.split instlist in
402 let match_var = fun tm1 tm2 ->
403 let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
406 | _ -> failwith "match_var: no match" in
408 let mcheck_var = fun tm ->
409 if (not (is_var tm)) then failwith ("inst_meta_rule_vars: `" ^ string_of_term tm ^ "` is not a variable")
410 else try list_match_first (match_var tm) rfrees
411 with Failure _ -> failwith ("inst_meta_rule_vars: `" ^ string_of_term tm ^ "` could not be found in the meta_rule") in
413 let mcheck_gvar = fun var ->
414 try let mvar = list_match_first (match_var var) gfrees in
415 term_match [] var mvar
417 warn true ("inst_meta_rule_vars: `" ^ string_of_term var ^ "` could not be found in the goal") ;
420 let new_r,prim_inst = meta_rule_mk_primed_vars_I gfrees r in
421 let new_vars = map ((instantiate prim_inst) o mcheck_var) vars in
423 let subs_vars = flat (map frees subs) in
424 let new_subs_inst = itlist compose_insts (map mcheck_gvar subs_vars) null_inst in
425 let new_subs = map (instantiate new_subs_inst) subs in
427 let new_instlist = List.combine new_vars new_subs in
428 let mk_inst = fun t1,t2 -> term_match [] t1 t2 in
429 let inst = itlist compose_insts (map mk_inst new_instlist) null_inst in
430 let result_r = inst_meta_rule inst new_r in
435 (* ------------------------------------------------------------------------- *)
436 (* mk_meta_rule: thm -> meta_rule *)
437 (* Creates a meta_rule out of a theorem. *)
438 (* Theorem must be of the form |- H1 ===> H2 ===> ...===> Hn ===> C *)
439 (* "===>" is the emulation of meta-level implication so this corresponds to *)
440 (* [|H1;H2;...;Hn|] ==> C in Isabelle) *)
441 (* For each Hi that is a meta-level implication, a "meta_subgoal" is created.*)
442 (* ------------------------------------------------------------------------- *)
443 (* (+) undisch_premises uses MUNDISCH to handle meta-level implication. All *)
444 (* the premises are undischarged. It returns the list of premises paired *)
445 (* with the resulting theorem. Note that MUNDISCH also removes meta-level *)
446 (* implication from the undischarged premises. *)
447 (* (+) "mk_meta_subgoal" creates a meta_subgoal from a term. If the term is *)
448 (* an implication, the lhs is added as an assumption/premise of the *)
449 (* meta_subgoal and mk_meta_subgoal is called recursively for the rhs. *)
450 (* (+) The conclusion of the undischarged theorem is the first part of the *)
451 (* produced meta_rule. *)
452 (* (+) mk_meta_subgoal creates the meta_subgoals for all the premises. They *)
453 (* form the second part of the meta_rule. *)
454 (* (+) The theorem itself is used as the justification theorem, after *)
455 (* eliminating any remaining meta-level implication in the conclusion. *)
456 (* In theory, the conclusion should never have any remaining meta-level *)
457 (* implications. We're just making sure because we don't want any meta-level *)
458 (* implications to appear in our new subgoals. *)
459 (* ------------------------------------------------------------------------- *)
461 let (mk_meta_rule: thm -> meta_rule) =
463 let rec undisch_premises th =
464 if is_mimp (concl th)
465 then let rest,res_th = undisch_premises (MUNDISCH th) in
466 (rand(rator(concl th)))::rest,res_th
468 let (prems,thm) = undisch_premises thm in
469 let rec mk_meta_subgoal tm = (
470 if (is_mimp(tm)) then
471 let (a,c) = dest_mimp tm in
472 let (prems,concl) = mk_meta_subgoal c in
473 ("",ASSUME a)::prems,concl
476 concl thm,map mk_meta_subgoal prems,MIMP_TO_IMP_RULE thm;;
479 (* ------------------------------------------------------------------------- *)
480 (* mk_meta_rule_old: thm -> meta_rule *)
481 (* Creates a meta_rule out of a theorem. === DEPRECATED === *)
482 (* Theorem must be of the form H1,H2,...,Hn |- C *)
483 (* If Hi is of the form Hi1==>Hi2==>...==>Hik==>HiC then it is treated as *)
484 (* Hi1,Hi2,...,Hik ?- HiC (or "meta-level" implication *)
485 (* [|Hi1;Hi2;...;Hik|] ==> HiC in Isabelle) and the corresponding *)
486 (* meta_subgoal is created. *)
487 (* ------------------------------------------------------------------------- *)
488 (* --As a result you CANNOT have rules with implication in their premises!-- *)
489 (* (You'll have to use mk_elim_meta_rule or build the meta_rule yourself.) *)
490 (* ------------------------------------------------------------------------- *)
491 (* (+) The theorem is destroyed to its hypothesis list and its conclusion. *)
492 (* The conclusion is the first part of the meta_rule. *)
493 (* (+) "mk_meta_subgoal" creates a meta_subgoal from a term. If the term is *)
494 (* an implication, the lhs is added as an assumption/premise of the *)
495 (* meta_subgoal and mk_meta_subgoal is called recursively for the rhs. *)
496 (* (+) The theorem itself is used as the justification theorem. *)
497 (* ------------------------------------------------------------------------- *)
498 (* Deprecated. New mk_meta_rule uses meta-level implication. *)
499 (* Kept until new mk_meta_rule is tested and stable. *)
500 (* ------------------------------------------------------------------------- *)
502 let (mk_meta_rule_old: thm -> meta_rule) =
504 let (hyps,concl) = dest_thm thm in
505 let rec mk_meta_subgoal tm = (
507 let (a,c) = dest_imp tm in
508 let (prems,concl) = mk_meta_subgoal c in
509 ("",ASSUME a)::prems,concl
512 concl,map mk_meta_subgoal hyps,thm;;
516 (* ------------------------------------------------------------------------- *)
517 (* mk_elim_meta_rule_old: thm -> meta_rule *)
518 (* Creates a meta_rule out of a theorem. === DEPRECATED === *)
519 (* Works like mk_meta_rule but acommodates elimination/destruction rules *)
520 (* a little bit better by not breaking the major premise. This effectively *)
521 (* allows the major premise to be an implication. *)
522 (* ------------------------------------------------------------------------- *)
523 (* In an elimination or destruction rule, the first or major premise is *)
524 (* matched against one of the assumptions. Therefore, you cannot have a *)
525 (* meta_subgoal for a major premise. If there is an implication there we *)
526 (* shall leave it intact and not treat it as "meta-level" implication. *)
527 (* This still disallows the use of implication in the rest of the premises *)
528 (* (by treating it as "meta-level" implication). *)
529 (* ------------------------------------------------------------------------- *)
530 (* Deprecated. New mk_meta_rule uses meta-level implication. *)
531 (* Kept until new mk_meta_rule is tested and stable. *)
532 (* ------------------------------------------------------------------------- *)
534 let (mk_elim_meta_rule_old: thm -> meta_rule) =
536 let (hyps,concl) = dest_thm thm in
537 if (hyps = []) then failwith "mk_elim_meta_rule: Invalid rule - no premises!"
538 else let major_prem,hyps = ([],hd hyps),tl hyps in
539 let rec mk_meta_subgoal tm = (
541 let (a,c) = dest_imp tm in
542 let (prems,concl) = mk_meta_subgoal c in
543 ("",ASSUME a)::prems,concl
546 concl,major_prem :: (map mk_meta_subgoal hyps),thm;;
550 (* ------------------------------------------------------------------------- *)
551 (* Isabelle's natural deduction inference rules as meta_rules. *)
552 (* ------------------------------------------------------------------------- *)
553 (* The trailing 'm' indicates they are represented as meta_rules as opposed *)
555 (* Use "mk_meta_rule" to create meta_rules from theorems. *)
556 (* Most of the following can be created using mk_meta_rule but are left here *)
558 (* ------------------------------------------------------------------------- *)
559 (* Deprecated. New mk_meta_rule uses meta-level implication so now ALL of *)
560 (* these can be represented at the object-level and turned into meta_rules *)
561 (* using mk_meta_rule. *)
562 (* ------------------------------------------------------------------------- *)
564 let conjIm:meta_rule =
572 let conjEm:meta_rule =
576 [("",ASSUME `p:bool`);("",ASSUME `q:bool`)],`r:bool`
578 (UNDISCH o UNDISCH o TAUT) `p/\q==>(p==>q==>r)==>r`
581 let notEm:meta_rule =
587 (UNDISCH o UNDISCH o TAUT) `~a==>a==>r`
590 let disjI1m:meta_rule =
595 UNDISCH ( TAUT `p==>p\/q` ));;
597 let disjI2m:meta_rule =
602 UNDISCH ( TAUT `q==>p\/q` ));;
604 let disjEm:meta_rule =
608 [("",ASSUME `p:bool`)],`r:bool`;
609 [("",ASSUME `q:bool`)],`r:bool`
611 (UNDISCH o UNDISCH o UNDISCH) ( TAUT `p\/q==>(p==>r)==>(q==>r)==>r`)
615 let impIm:meta_rule =
618 [("",ASSUME `p:bool`)],`q:bool`
620 UNDISCH (TAUT `(p==>q)==>(p==>q)`)
624 let impEm:meta_rule =
629 [("",ASSUME `q:bool`)],`r:bool`
631 (UNDISCH o UNDISCH o UNDISCH o TAUT) `(p==>q)==>p==>(q==>r)==>r`
641 (UNDISCH o UNDISCH o TAUT) `(p==>q)==>(p==>q)`
644 (* Note from old mk_meta_rule: *)
645 (* This one cannot be expressed as a theorem because HOL Light insists on *)
646 (* ordering the assumptions of the theorem so the major premise is `p` *)
647 (* instead of `~p`. *)
649 let notEm:meta_rule =
655 (UNDISCH o UNDISCH o TAUT) `~a==>a==>r`
659 (* ------------------------------------------------------------------------- *)
660 (* rulem_tac: ((term * term) list -> meta_rule -> tactic): *)
661 (* Isabelle's rule as a HOL Light meta_rule tactic. *)
662 (* Uses a rule of the form H1,H2,...,Hn |- C represented as a meta_rule *)
663 (* to solve A1,A2,...,Am ?- G *)
664 (* Matches C to the goal G, then splits the goal to *)
665 (* A1,A2,...,Am ?- H1 *)
666 (* A1,A2,...,Am ?- H2 *)
668 (* A1,A2,...,Am ?- Hn *)
669 (* Hi can be of the form Hi1,Hi2,...,Hik ?- HiC then the goal produced is *)
670 (* A1,A2,...,Am,Hi1,Hi2,...,Hik ?- HiC *)
671 (* ------------------------------------------------------------------------- *)
672 (* (+) "avoids" lists all the free variables in the assumptions and goal so *)
673 (* as to avoid instantiating those (as in variable conflicts with the rule *)
674 (* or partly instantiated rule in the case of erule) *)
675 (* (+) First we check if C matches G. If it does we keep the resulting *)
676 (* instantiation (ins). *)
677 (* (+) We instantiate the "meta-subgoals" of the meta_rule using ins. *)
678 (* In essence we're instantiating the premises of the rule. (new_hyps) *)
679 (* (+) The "create_goal" function creates the new goals by adding the *)
680 (* assumption list A1--Am to the instantiated "meta-subgoal". *)
681 (* (+) create_goal is mapped on new_hyps to create the new subgoal list. *)
682 (* (+) The "create_dischl" function creates the list of the terms involved *)
683 (* in the premises of each instantiated meta-subgoal. In order to create the *)
684 (* justification of the tactic, we need to convert Hi1,Hi2,...,Hik |- HiC *)
685 (* into |- Hi1==>Hi2==>...==>Hik==>HiC. That is the only way we can capture *)
686 (* the notion of a "subgoal" within a HOL Light object-level theorem. *)
687 (* We will then use PROVE_HYP to eliminate each of the proven subgoals from *)
688 (* the rule's justification theorem. In order to achieve this conversion we *)
689 (* need to keep a list of the instantiated premises of the rule (dischls) *)
690 (* for each meta_subgoal so as to avoid discharging the original goal's *)
691 (* assumptions or _FALSITY_. *)
692 (* (+) "disch_pair" is used for convenience. dishls is combined with the *)
693 (* list of proven subgoals so that each subgoal is attached to its *)
694 (* corresponding premises list (dischl). disch_pair then does the discharges.*)
695 (* It also takes care of instantiating the meta-variables in those premises *)
696 (* for proper justification. *)
697 (* (+) normalfrees is used to calculate the list of metavariables that will *)
698 (* end up in the new subgoals. It contains all the free variables in the *)
699 (* goal and instlist. *)
700 (* (+) The newly introduced metavariables are found by subtracting *)
701 (* normalfrees from the set of all free variables in all new goals. *)
702 (* ------------------------------------------------------------------------- *)
704 let (rulem_tac: (term*term) list->meta_rule->tactic) =
705 fun instlist r ((asl,w) as g) ->
706 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
708 let ins = try ( term_match [] c w ) with Failure _ -> failwith "Rule doesn't match!" in
710 let new_hyps = map (inst_goal ins) hyps in
711 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
712 let new_goals = map (create_goal asl) new_hyps in
713 let rec create_dischl = fun (asms,g) -> if (asms = []) then [] else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
714 let dischls = map create_dischl new_hyps in
715 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
716 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
717 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
718 (mvs,null_inst),new_goals,fun i l ->
719 List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm) (map (disch_pair i) (List.combine dischls l));;
722 (* ------------------------------------------------------------------------- *)
723 (* erulem_tac: ((term * term) list -> meta_rule -> tactic): *)
724 (* Isabelle's erule as a HOL Light meta_rule tactic. *)
725 (* Works like rulem but also matches the first hypothesis H1 with one of the *)
726 (* assumptions A1--Am and instantiates accordingly. *)
727 (* A "proper" elimination rule H1 is of the form ?- H1 (ie. has no premises) *)
728 (* ------------------------------------------------------------------------- *)
729 (* Same as rulem with some added stuff. *)
730 (* (+) If there are no "meta_subgoals" (no new subgoals to create) we fail. *)
731 (* (+) Otherwise we use the first "meta_subgoal" as our primary hypothesis *)
732 (* (the one that will be eliminated - prim_hyp). *)
733 (* (+) If prim_hyp has premises then this is not a "proper" elimination rule.*)
734 (* (+) Otherwise try to match any of the assumptions with prim_hyp. The *)
735 (* resulting instantiation is elim_inst. *)
736 (* (+) Instantiate all generated meta_subgoals with elim_inst. Retrieve the *)
737 (* (now instantiated) prim_hyp and remove it from the new subgoals (it is *)
738 (* trivially proven). We get a "pattern-matching is not exhaustive" warning *)
739 (* here, but we have already checked that new_hyps is non-empty. *)
740 (* (+) prim_thm is a trivial theorem that proves the subgoal corresponding *)
742 (* (+) Instantiate the justification theorem with elim_thm. *)
743 (* (+) Add prim_hyp to the justification (pretending its a proven subgoal). *)
744 (* (+) Use a hack to add the eliminated assumption to the proven subgoals so *)
745 (* that we pass the validity check properly. *)
746 (* ------------------------------------------------------------------------- *)
748 let (erulem_tac: (term * term) list -> meta_rule->tactic) =
749 fun instlist r ((asl,w) as g) ->
750 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
752 let ins = try ( term_match [] c w )
753 with Failure _ -> failwith "Rule doesn't match!" in
754 let new_hyps = map (inst_goal ins) hyps in
756 let (prems,prim_hyp) =
757 if (new_hyps = []) then failwith "erule: Not a proper elimination rule: no premises!"
759 let avoids = gl_frees g in
761 let asl,(prim_thm,elim_inst) =
763 then try term_to_asm_match avoids prim_hyp asl with Failure s -> failwith ("erule: " ^ s)
764 else failwith "erule: Not a proper elimination rule: major premise has assumptions!" in
765 let (_,prim_hyp)::new_hyps = map (inst_goal elim_inst) new_hyps in
766 let thm = INSTANTIATE_ALL elim_inst thm in
768 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
769 let new_goals = map (create_goal asl) new_hyps in
770 let rec create_dischl =
772 if (asms = []) then []
773 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
774 let dischls = map create_dischl new_hyps in
775 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
777 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
778 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
779 (mvs,null_inst),new_goals,fun i l ->
780 let major_thmi = INSTANTIATE_ALL i prim_thm in
781 List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm)
782 (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l)));;
785 (* ------------------------------------------------------------------------- *)
786 (* drulem_tac: ((term * term) list -> meta_rule -> tactic): *)
787 (* Isabelle's drule as a HOL Light meta_rule tactic. *)
788 (* Uses rules as shown in "rule". *)
789 (* Matches the first hypothesis H1 with one of the *)
790 (* assumptions A1--Am and instantiates accordingly. *)
791 (* The assumption is removed from the list and the trivial goal is proven *)
793 (* A "proper" destructio rule H1 is of the form ?- H1 (ie. has no premises) *)
794 (* The goal A1,A2,...,Am,G ?- C is also added. *)
795 (* ------------------------------------------------------------------------- *)
796 (* Same as erulem with a few differences. *)
797 (* [+] Does not try to match the goal c. *)
798 (* [+] Adds an extra goal c ?- w after instantiating c. *)
799 (* [+] The new goal is treated slightly different in the justification. *)
800 (* It is the one whose premises must be proven so as to get to the final *)
801 (* goal. So it gets proven using PROVE_HYP by the result of the *)
802 (* justification on the original rule. *)
803 (* ------------------------------------------------------------------------- *)
805 let (drulem_tac: (term * term) list -> meta_rule->tactic) =
806 fun instlist r ((asl,w) as g) ->
807 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
809 let (prems,major_prem) =
810 if (hyps = []) then failwith "drule: Not a proper destruction rule: no premises!"
812 let avoids = gl_frees g in
814 let asl,(major_thm,elim_inst) =
816 then try term_to_asm_match avoids major_prem asl with Failure s -> failwith ("drule: " ^ s)
817 else failwith "drule: not a proper destruction rule: major premise has assumptions!" in
818 let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
819 let thm = INSTANTIATE_ALL elim_inst thm in
820 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
821 let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in
823 let rec create_dischl =
825 if (asms = []) then []
826 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
827 (* We add an empty discharge list at the end for the extra goal. *)
828 let dischls = map create_dischl new_hyps @ [[]] in
829 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
831 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
832 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
833 (mvs,null_inst),new_goals,fun i l ->
834 let major_thmi = INSTANTIATE_ALL i major_thm in
835 let l = (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l))) in
836 PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;
839 (* ------------------------------------------------------------------------- *)
840 (* frulem_tac: ((term * term) list -> meta_rule -> tactic): *)
841 (* Isabelle's frule as a HOL Light meta_rule tactic. *)
842 (* Same as drule, but does not remove the matching assumption from the list. *)
843 (* ------------------------------------------------------------------------- *)
844 (* Same as drulem only skipping the parts that eat up the assumption and *)
845 (* re-add it to the proven subgoals. *)
846 (* ------------------------------------------------------------------------- *)
848 let (frulem_tac: (term * term) list -> meta_rule->tactic) =
849 fun instlist r ((asl,w) as g) ->
850 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
852 let (prems,major_prem) =
853 if (hyps = []) then failwith "frule: Not a proper destruction rule: no premises!"
855 let avoids = gl_frees g in
857 let _,(major_thm,elim_inst) =
859 then try term_to_asm_match avoids major_prem asl with Failure s -> failwith ("frule: " ^ s)
860 else failwith "frule: Not a proper destruction rule: major premise has assumptions!" in
861 let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
862 let thm = INSTANTIATE_ALL elim_inst thm in
863 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
864 let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in
866 let rec create_dischl =
868 if (asms = []) then []
869 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
870 let dischls = map create_dischl new_hyps @ [[]] in
871 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
873 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
874 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
875 (mvs,null_inst),new_goals,fun i l ->
876 let major_thmi = INSTANTIATE_ALL i major_thm in
877 let l = (major_thmi :: ((map (disch_pair i)) o (List.combine dischls)) l) in
878 PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;
881 (* ------------------------------------------------------------------------- *)
882 (* cutm_tac: ((term * term) list -> meta_rule -> tactic): *)
883 (* Isabelle's cut_tac as a HOL Light meta_rule tactic. *)
884 (* Inserts a theorem in the assumptions. *)
885 (* ------------------------------------------------------------------------- *)
886 (* (+) WARNING: It does not introduce metavariables like the other tactics *)
887 (* do! In the TODO list... *)
888 (* ------------------------------------------------------------------------- *)
890 let (cutm_tac: (term * term) list -> meta_rule->tactic) =
892 let (_,_,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
896 (* ------------------------------------------------------------------------- *)
897 (* erulenm_tac : (term * term) list -> int -> meta_rule->tactic) *)
898 (* drulenm_tac : (term * term) list -> int -> meta_rule->tactic) *)
899 (* frulenm_tac : (term * term) list -> int -> meta_rule->tactic) *)
900 (* Identical to their counterparts, the only difference being that they try *)
901 (* to match a particular assumption given by number. *)
902 (* ------------------------------------------------------------------------- *)
904 let (erulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
905 fun instlist n r ((asl,w) as g) ->
906 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
908 let ins = try ( term_match [] c w )
909 with Failure _ -> failwith "Rule doesn't match!" in
910 let new_hyps = map (inst_goal ins) hyps in
912 let (prems,prim_hyp) =
913 if (new_hyps = []) then failwith "erule: Not a proper elimination rule: no premises!"
915 let avoids = gl_frees g in
917 let asl,(prim_thm,elim_inst) =
919 then try term_to_asm_n_match avoids prim_hyp (rev asl) n with Failure s -> failwith ("erule: " ^ s)
920 else failwith "erule: Not a proper elimination rule: major premise has assumptions!" in
921 let (_,prim_hyp)::new_hyps = map (inst_goal elim_inst) new_hyps in
922 let thm = INSTANTIATE_ALL elim_inst thm in
924 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
925 let new_goals = map (create_goal asl) new_hyps in
926 let rec create_dischl =
928 if (asms = []) then []
929 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
930 let dischls = map create_dischl new_hyps in
931 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
933 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
934 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
935 (mvs,null_inst),new_goals,fun i l ->
936 let major_thmi = INSTANTIATE_ALL i prim_thm in
937 List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL (compose_insts ins i) thm)
938 (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l)));;
941 let (drulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
942 fun instlist n r ((asl,w) as g) ->
943 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
945 let (prems,major_prem) =
946 if (hyps = []) then failwith "drule: Not a proper destruction rule: no premises!"
948 let avoids = gl_frees g in
950 let asl,(major_thm,elim_inst) =
952 then try term_to_asm_n_match avoids major_prem (rev asl) n with Failure s -> failwith ("drule: " ^ s)
953 else failwith "drule: not a proper destruction rule: major premise has assumptions!" in
954 let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
955 let thm = INSTANTIATE_ALL elim_inst thm in
956 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
957 let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in
959 let rec create_dischl =
961 if (asms = []) then []
962 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
963 (* We add an empty discharge list at the end for the extra goal. *)
964 let dischls = map create_dischl new_hyps @ [[]] in
965 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
967 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
968 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
969 (mvs,null_inst),new_goals,fun i l ->
970 let major_thmi = INSTANTIATE_ALL i major_thm in
971 let l = (major_thmi :: map (ADD_HYP major_thmi) (map (disch_pair i) (List.combine dischls l))) in
972 PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;
975 let (frulenm_tac: (term * term) list -> int -> meta_rule->tactic) =
976 fun instlist n r ((asl,w) as g) ->
977 let (c,hyps,thm) = inst_meta_rule_vars instlist r (gl_frees g) in
979 let (prems,major_prem) =
980 if (hyps = []) then failwith "frule: Not a proper destruction rule: no premises!"
982 let avoids = gl_frees g in
984 let _,(major_thm,elim_inst) =
986 then try term_to_asm_n_match avoids major_prem (rev asl) n with Failure s -> failwith ("frule: " ^ s)
987 else failwith "frule: Not a proper destruction rule: major premise has assumptions!" in
988 let (_,major_asm)::new_hyps = map (inst_goal elim_inst) hyps in
989 let thm = INSTANTIATE_ALL elim_inst thm in
990 let create_goal = fun asms (hs,gl) -> (hs@asms,gl) in
991 let new_goals = (map (create_goal asl) new_hyps) @ [create_goal asl (["",ASSUME (instantiate elim_inst c)],w)] in
993 let rec create_dischl =
995 if (asms = []) then []
996 else ((concl o snd o hd) asms)::(create_dischl ((tl asms),g)) in
997 let dischls = map create_dischl new_hyps @ [[]] in
998 let disch_pair = fun i (dischl,thm) -> DISCHL (map (instantiate i) dischl) thm in
1000 let normalfrees = itlist union (map ( fun (_,y) -> frees y ) instlist ) (gl_frees g) in
1001 let mvs = subtract (itlist union (map gl_frees new_goals) []) normalfrees in
1002 (mvs,null_inst),new_goals,fun i l ->
1003 let major_thmi = INSTANTIATE_ALL i major_thm in
1004 let l = (major_thmi :: ((map (disch_pair i)) o (List.combine dischls)) l) in
1005 PROVE_HYP (List.fold_left (fun t1 t2 -> PROVE_HYP (INSTANTIATE_ALL i t2) t1) (INSTANTIATE_ALL i thm) ((butlast) l)) (last l);;
1008 (* ------------------------------------------------------------------------- *)
1009 (* Xrulem versions for empty instlist. *)
1010 (* ------------------------------------------------------------------------- *)
1012 let rulem: meta_rule -> tactic = rulem_tac [];;
1013 let erulem: meta_rule -> tactic = erulem_tac [];;
1014 let drulem: meta_rule -> tactic = drulem_tac [];;
1015 let frulem: meta_rule -> tactic = frulem_tac [];;
1017 let erulenm: int -> meta_rule -> tactic = erulenm_tac [];;
1018 let drulenm: int -> meta_rule -> tactic = drulenm_tac [];;
1019 let frulenm: int -> meta_rule -> tactic = frulenm_tac [];;
1021 (* For consistency with HOL Light capitalized tactics: *)
1022 let RULEM,ERULEM,DRULEM,FRULEM = rulem,erulem,drulem,frulem;;
1023 let ERULENM,DRULENM,FRULENM = erulenm,drulenm,frulenm;;
1026 (* ------------------------------------------------------------------------- *)
1027 (* Xrule and Xrule_tac using arbitrary inference rules in the form of thms. *)
1028 (* (see mk_meta_rule and meta_rule type) *)
1029 (* ------------------------------------------------------------------------- *)
1031 let rule_tac: (term * term) list -> thm -> tactic =
1033 rulem_tac instlist (mk_meta_rule thm);;
1035 let erule_tac: (term * term) list -> thm -> tactic =
1037 erulem_tac instlist (mk_meta_rule thm);;
1039 let drule_tac: (term * term) list -> thm -> tactic =
1041 drulem_tac instlist (mk_meta_rule thm);;
1043 let frule_tac: (term * term) list -> thm -> tactic =
1045 frulem_tac instlist (mk_meta_rule thm);;
1047 let cut_tac: (term * term) list -> thm -> tactic =
1049 cutm_tac instlist (mk_meta_rule thm);;
1051 let RULE_TAC,ERULE_TAC,DRULE_TAC,FRULE_TAC,CUT_TAC = rule_tac,erule_tac,drule_tac,frule_tac,cut_tac;;
1054 let erulen_tac: (term * term) list -> int -> thm -> tactic =
1055 fun instlist n thm ->
1056 erulenm_tac instlist n (mk_meta_rule thm);;
1058 let drulen_tac: (term * term) list -> int -> thm -> tactic =
1059 fun instlist n thm ->
1060 drulenm_tac instlist n (mk_meta_rule thm);;
1062 let frulen_tac: (term * term) list -> int -> thm -> tactic =
1063 fun instlist n thm ->
1064 frulenm_tac instlist n (mk_meta_rule thm);;
1066 let ERULEN_TAC,DRULEN_TAC,FRULEN_TAC = erulen_tac,drulen_tac,frulen_tac;;
1069 let rule: (thm -> tactic) = rule_tac [];;
1070 let erule: (thm -> tactic) = erule_tac [];;
1071 let drule: (thm -> tactic) = drule_tac [];;
1072 let frule: (thm -> tactic) = frule_tac [];;
1074 let RULE,ERULE,DRULE,FRULE = rule,erule,drule,frule;;
1077 let erulen: (int -> thm -> tactic) = erulen_tac [];;
1078 let drulen: (int -> thm -> tactic) = drulen_tac [];;
1079 let frulen: (int -> thm -> tactic) = frulen_tac [];;
1081 let ERULEN,DRULEN,FRULEN = erulen,drulen,frulen;;