1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
5 (* Copied from HOL Light jordan directory *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
10 module Tactics_jordan = struct
17 (* ------------------------------------------------------------------ *)
18 (* MORE RECENT ADDITIONS *)
19 (* ------------------------------------------------------------------ *)
21 Parse_ext_override_interface.unambiguous_interface();;
27 (* ------------------------------------------------------------------ *)
28 (* SOME EASY TACTICS *)
29 (* ------------------------------------------------------------------ *)
31 let TAUT_TAC t = (MATCH_MP_TAC (TAUT t));;
33 let REP_GEN_TAC = REPEAT GEN_TAC;;
35 let SUBGOAL_MP_TAC t = SUBGOAL_THEN t MP_TAC;;
37 let DISCH_ALL_TAC = REP_GEN_TAC THEN
38 let tac = TAUT_TAC `(b ==> a==> c) ==> (a /\ b ==> c)` in
39 (REPEAT ((REPEAT tac) THEN DISCH_TAC)) THEN LABEL_ALL_TAC;;
41 (* ------------------------------------------------------------------ *)
42 (* TACTICS BY NUMBER. These are probably best avoided.
44 The numbering is that in the asm list -- not the printed numbers! *)
45 (* ------------------------------------------------------------------ *)
47 let (UNDISCH_EL_TAC:int -> tactic) =
49 let (asl,w) = dest_goal gl in
50 try let sthm,asl' = (el i asl),(drop i asl) in
51 let tm = concl (snd (el i asl)) in
53 null_meta,[asl',mk_imp(tm,w)],
54 fun i [th] -> MP th (INSTANTIATE_ALL i thm)
55 with Failure _ -> failwith "UNDISCH_EL_TAC";;
57 (* remove hypotheses by number *)
58 let rec (POPL_TAC:int list ->tactic) =
59 let (POP_TAC:int->tactic) =
60 fun i -> (UNDISCH_EL_TAC i) THEN (TAUT_TAC `B ==> (A==>B)`) in
62 map(fun j -> if j<=i then j else (j-1)) in
63 function [] -> ALL_TAC |
64 (i::b) -> (POP_TAC i) THEN (POPL_TAC (renumber i b));;
66 let rec (UNDISCH_LIST:int list -> tactic) =
68 map(fun j -> if j<=i then j else (j-1)) in
69 function [] -> ALL_TAC |
70 (i::b) -> (UNDISCH_EL_TAC i) THEN (UNDISCH_LIST (renumber i b));;
72 (* ------------------------------------------------------------------ *)
73 (* Transformations of Hypothesis List by LABELS *)
74 (* ------------------------------------------------------------------ *)
76 type goalthm = goal -> thm;;
78 let (HYP_INT:int->goalthm) =
81 snd (el i (goal_asms gl));;
83 let (HYP:string->goalthm) =
85 let asl = goal_asms gl in
87 with Failure _ -> try assoc ("Z-"^s) asl
88 with Failure _ -> failwith ("HYP not found: "^ s);;
90 let (THM:thm->goalthm) =
94 (* We are constructing functors, so to speak *)
96 let (H_RULER: (thm list->thm->thm)->(goalthm list)-> goalthm -> tactic) =
99 let (asl,w) = dest_goal gl in
100 let thl = map (fun x-> (x gl)) gthl in
101 let th = rule thl (gthm gl) in
104 (* The next few term rules into goal_rules *)
105 (* H_type (x:type) should return an object
106 similar to x but with thms made into goalthms *)
108 let (H_RULE_LIST: (thm list->thm->thm)->(goalthm list)-> goalthm -> goalthm) =
109 fun rule gthl gthm g ->
110 let thl = map (fun x-> (x g)) gthl in
113 let H_RULE2 (rule:thm->thm->thm) =
114 fun gthm1 gthm2 -> H_RULE_LIST (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
116 let H_RULE (rule:thm->thm) = fun gthm -> H_RULE_LIST (fun _ th -> rule th) [] gthm;;
118 let (H_TTAC : thm_tactic -> goalthm -> tactic ) =
119 fun ttac gthm g -> (ttac (gthm g) g);;
121 let H_ASSUME_TAC = H_TTAC ASSUME_TAC;;
122 let INPUT = fun gth -> (H_ASSUME_TAC gth) THEN LABEL_ALL_TAC;;
124 let H_VAL2 (rule:thm->thm->thm) =
125 fun gthm1 gthm2 -> H_RULER (fun thl th -> rule (hd thl) th) [gthm1] gthm2;;
127 let H_CONJ = H_VAL2(CONJ);;
128 let H_MATCH_MP = H_VAL2(MATCH_MP);;
130 let H_REWRITE_RULE gthml gth = H_RULER REWRITE_RULE gthml gth;;
131 let H_ONCE_REWRITE_RULE gthml gth = H_RULER ONCE_REWRITE_RULE gthml gth;;
132 let H_SIMP_RULE = H_RULER SIMP_RULE;;
134 let H_VAL (rule:thm->thm) = fun gthm -> H_RULER (fun _ th -> rule th) [] gthm;;
137 let H_CONJUNCT1 = H_VAL CONJUNCT1;;
138 let H_CONJUNCT2 = H_VAL CONJUNCT2;;
139 let H_EQT_INTRO = H_VAL EQT_INTRO;;
140 let H_EQT_ELIM = H_VAL EQT_ELIM;;
141 let H_SPEC = fun t -> H_VAL(SPEC t);;
142 let H_GEN = fun t -> H_VAL(GEN t);;
143 let H_DISJ1 = C (fun t -> H_VAL ((C DISJ1) t));;
144 let H_DISJ2 = (fun t -> H_VAL (( DISJ2) t));;
145 (* beware! One is inverted here. *)
146 let H_NOT_ELIM = H_VAL (NOT_ELIM);;
147 let H_NOT_INTRO = H_VAL (NOT_INTRO);;
148 let H_EQF_ELIM = H_VAL (EQF_ELIM);;
149 let H_EQF_INTRO = H_VAL (EQF_INTRO);;
150 let (&&&) = H_RULE2 CONJ;;
152 let (H_UNDISCH_TAC:goalthm -> tactic) =
154 let tm = concl(gthm g) in
159 (* let upgs tac gs = by tac gs;; *)
161 let (thm_op:goalthm->goalthm->goalthm) =
163 if (is_eq (snd (strip_forall (concl (gt1 g)))))
164 then REWRITE_RULE[gt1 g] (gt2 g) else
165 MATCH_MP (gt1 g) (gt2 g);;
167 let (COMBO:goalthm list-> goalthm) =
168 fun gthl -> end_itlist thm_op gthl;;
170 let INPUT_COMBO = INPUT o COMBO;;
175 (* abbrev_type copied from definitions_group.ml *)
178 let pthm = prove_by_refinement(
179 `(\ (x:A) .T) (@(x:A). T)`,
182 let abbrev_type ty s = let (a,b) = new_basic_type_definition s
184 (INST_TYPE [ty,`:A`] pthm) in
185 let abst t = list_mk_forall ((frees t), t) in
186 let a' = abst (concl a) in
187 let b' = abst (rhs (concl b)) in
189 prove_by_refinement(a',[REWRITE_TAC[a]]),
190 prove_by_refinement(b',[REWRITE_TAC[GSYM b]]));;
193 (* ------------------------------------------------------------------ *)
195 (* ------------------------------------------------------------------ *)
197 let un = REWRITE_RULE[IN];;
199 (* ------------------------------------------------------------------ *)
202 MATCH_MP_TAC (TAUT `A /\ (A ==>B) ==> (A /\ B)`) THEN CONJ_TAC;;
204 let PROOF_BY_CONTR_TAC =
205 MATCH_MP_TAC (TAUT `(~A ==> F) ==> A`) THEN DISCH_TAC;;
209 (* ------------------------------------------------------------------ *)
210 (* some general tactics *)
211 (* ------------------------------------------------------------------ *)
213 (* before adding assumption to hypothesis list, cleanse it
214 of unnecessary conditions *)
217 let CLEAN_ASSUME_TAC th =
218 MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_TAC;;
220 let CLEAN_THEN th ttac =
221 MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_THEN ttac;;
223 (* looks for a hypothesis by matching a subterm *)
224 let (UNDISCH_FIND_TAC: term -> tactic) =
226 let (asl,w) = dest_goal gl in
227 let p = can (term_match[] tm) in
228 try let sthm,_ = remove
229 (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in
230 UNDISCH_TAC (concl (snd sthm)) gl
231 with Failure _ -> failwith "UNDISCH_FIND_TAC";;
233 let (UNDISCH_FIND_THEN: term -> thm_tactic -> tactic) =
235 let (asl,w) = dest_goal gl in
236 let p = can (term_match[] tm) in
237 try let sthm,_ = remove
238 (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in
239 UNDISCH_THEN (concl (snd sthm)) ttac gl
240 with Failure _ -> failwith "UNDISCH_FIND_TAC";;
242 (* ------------------------------------------------------------------ *)
243 (* NAME_CONFLICT_TAC : eliminate name conflicts in a term *)
244 (* ------------------------------------------------------------------ *)
246 let relabel_bound_conv tm =
247 let rec vars_and_constants tm acc =
251 | Comb(a,b) -> vars_and_constants b (vars_and_constants a acc)
252 | Abs(a,b) -> a::(vars_and_constants b acc) in
253 let relabel_bound tm =
256 let avoids = filter ((!=) x) (vars_and_constants tm []) in
257 let x' = mk_primed_var avoids x in
258 if (x=x') then failwith "relabel_bound" else (alpha x' tm)
259 | _ -> failwith "relabel_bound" in
260 DEPTH_CONV (fun t -> ALPHA t (relabel_bound t)) tm;;
264 let bad_term = mk_abs (`x:bool`,`(x:num)+1=2`) in
265 relabel_bound_conv bad_term;;
267 let NAME_CONFLICT_CONV = relabel_bound_conv;;
269 let NAME_CONFLICT_TAC = CONV_TAC (relabel_bound_conv);;
271 (* renames given bound variables *)
272 let alpha_conv env tm = ALPHA tm (deep_alpha env tm);;
274 (* replaces given alpha-equivalent terms with- the term itself *)
275 let unify_alpha_tac = SUBST_ALL_TAC o REFL;;
277 let rec get_abs tm acc = match tm with
278 Abs(u,v) -> get_abs v (tm::acc)
279 |Comb(u,v) -> get_abs u (get_abs v acc)
282 (* for purposes such as sorting, it helps if ALL ALPHA-equiv
283 abstractions are replaced by equal abstractions *)
284 let (alpha_tac:tactic) =
286 EVERY (map unify_alpha_tac (get_abs (goal_concl gl) [])) gl;;
288 (* ------------------------------------------------------------------ *)
289 (* SELECT ELIMINATION.
290 SELECT_TAC should work whenever there is a single predicate selected.
291 Something more sophisticated might be needed when there
294 Useful for proving statements such as `1 + (@x. (x=3)) = 4` *)
295 (* ------------------------------------------------------------------ *)
297 (* spec form of SELECT_AX *)
298 let select_thm select_fn select_exist =
299 BETA_RULE (ISPECL [select_fn;select_exist]
304 `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`;;
306 let SELECT_EXIST = prove_by_refinement(
307 `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
313 UNDISCH_FIND_TAC `(?)`;
314 DISCH_THEN CHOOSE_TAC;
315 ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX);
321 let SELECT_THM = prove_by_refinement(
322 `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==>
323 (!t. Q t))) ==> Q ((@) P)`,
326 MESON_TAC[SELECT_EXIST];
331 (* explicitly pull apart the clause Q((@) P),
332 because MATCH_MP_TAC isn't powerful
333 enough to do this by itself. *)
335 `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,MESON_TAC[]) in
336 let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in
337 unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN CONJ_TAC
339 (DISCH_THEN (fun t-> ALL_TAC)) THEN GEN_TAC;
340 DISCH_TAC THEN GEN_TAC];;
344 # g `(R:A->bool) ((@) S)`;;
345 val it : Core.goalstack = 1 subgoal (1 total)
350 val it : Core.goalstack = 2 subgoals (2 total)
361 (* ------------------------------------------------------------------ *)
362 (* TYPE_THEN and TYPEL_THEN calculate the types of the terms supplied
363 in a proof, avoiding the hassle of working them out by hand.
364 It locates the terms among the free variables in the goal.
365 Ambiguious if a free variables have name conflicts.
367 Now TYPE_THEN handles general terms.
369 (* ------------------------------------------------------------------ *)
372 let rec type_set: (string*term) list -> (term list*term) -> (term list*term)=
373 fun typinfo (acclist,utm) -> match acclist with
374 | [] -> (acclist,utm)
375 | (Var(s,_) as a)::rest ->
376 let a' = (assocd s typinfo a) in
377 if (a = a') then type_set typinfo (rest,utm)
378 else let inst = instantiate (term_match [] a a') in
379 type_set typinfo ((map inst rest),inst utm)
380 | _ -> failwith "type_set: variable expected"
384 let typ = (type_vars_in_term t) in
385 can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;;
388 let TYPE_THEN: term -> (term -> tactic) -> tactic =
389 fun t (tac:term->tactic) gl ->
390 let (asl,w) = dest_goal gl in
391 let avoids = itlist (union o frees o concl o snd) asl
393 let strip = fun t-> (match t with
394 |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
395 let typinfo = map strip avoids in
396 let t' = (snd (type_set typinfo ((frees t),t))) in
397 (warn ((has_stv t')) "TYPE_THEN: unresolved type variables");
400 (* this version must take variables *)
401 let TYPEL_THEN: term list -> (term list -> tactic) -> tactic =
402 fun t (tac:term list->tactic) gl ->
403 let (asl,w) = dest_goal gl in
404 let avoids = itlist (union o frees o concl o snd) asl
406 let strip = fun t-> (match t with
407 |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in
408 let typinfo = map strip avoids in
409 let t' = map (fun u -> snd (type_set typinfo ((frees u),u))) t in
410 (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars");
413 (* trivial example *)
415 let _ = prove_by_refinement(`!y. y:num = y`,
418 TYPE_THEN `y:A` (fun t -> ASSUME_TAC(ISPEC t (TAUT `!x:B. x=x`)));
419 UNDISCH_TAC `y:num = y`; (* evidence that `y:A` was retyped as `y:num` *)
426 (* ------------------------------------------------------------------ *)
427 (* SAVE the goalstate, and retrieve later *)
428 (* ------------------------------------------------------------------ *)
430 let (save_goal,get_goal) =
431 let goal_buffer = ref [] in
433 goal_buffer := (s,!current_goalstack )::!goal_buffer in
434 let get_goal (s:string) = (current_goalstack:= assoc s !goal_buffer) in
435 (save_goal,get_goal);;
438 (* ------------------------------------------------------------------ *)
439 (* ordered rewrites with general ord function .
440 This allows rewrites with an arbitrary condition
441 -- adapted from simp.ml *)
442 (* ------------------------------------------------------------------ *)
446 let net_of_thm_ord ord rep force th =
448 let lconsts = freesl (hyp th) in
449 let matchable = can o term_match lconsts in
450 try let l,r = dest_eq t in
451 if rep & free_in l r then
452 let th' = EQT_INTRO th in
453 enter lconsts (l,(1,REWR_CONV th'))
454 else if rep & matchable l r & matchable r l then
455 enter lconsts (l,(1,ORDERED_REWR_CONV ord th))
457 enter lconsts (l,(1,ORDERED_REWR_CONV ord th))
458 else enter lconsts (l,(1,REWR_CONV th))
460 let l,r = dest_eq(rand t) in
461 if rep & free_in l r then
463 let th' = DISCH tm (EQT_INTRO(UNDISCH th)) in
464 enter lconsts (l,(3,IMP_REWR_CONV th'))
465 else if rep & matchable l r & matchable r l then
466 enter lconsts (l,(3,ORDERED_IMP_REWR_CONV ord th))
467 else enter lconsts(l,(3,IMP_REWR_CONV th));;
469 let GENERAL_REWRITE_ORD_CONV ord rep force (cnvl:conv->conv) (builtin_net:gconv net) thl =
470 let thl_canon = itlist (mk_rewrites false) thl [] in
471 let final_net = itlist (net_of_thm_ord ord rep force ) thl_canon builtin_net in
472 cnvl (REWRITES_CONV final_net);;
474 let GEN_REWRITE_ORD_CONV ord force (cnvl:conv->conv) thl =
475 GENERAL_REWRITE_ORD_CONV ord false force cnvl empty_net thl;;
477 let PURE_REWRITE_ORD_CONV ord force thl =
478 GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV empty_net thl;;
480 let REWRITE_ORD_CONV ord force thl =
481 GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV (basic_net()) thl;;
483 let PURE_ONCE_REWRITE_ORD_CONV ord force thl =
484 GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV empty_net thl;;
486 let ONCE_REWRITE_ORD_CONV ord force thl =
487 GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV (basic_net()) thl;;
489 let REWRITE_ORD_TAC ord force thl = CONV_TAC(REWRITE_ORD_CONV ord force thl);;
494 (* ------------------------------------------------------------------ *)
496 (* ------------------------------------------------------------------ *)
499 (* move vars leftward *)
500 (* if ord old_lhs new_rhs THEN swap *)
503 let new_factor_order t1 t2 =
504 try let t1v = fst(dest_binop `( *. )` t1) in
505 let t2v = fst(dest_binop `( *. )` t2) in
506 if (is_var t1v) & (is_var t2v) then term_order t1v t2v
507 else if (is_var t2v) then true else false
508 with Failure _ -> false ;;
510 (* false if it contains a variable or abstraction. *)
511 let rec is_arith_const tm =
512 if is_var tm then false else
513 if is_abs tm then false else
515 let (a,b) = (dest_comb tm) in
516 is_arith_const (a) & is_arith_const (b)
520 let new_factor_order2 t1 t2 =
521 try let t1v = fst(dest_binop `( *. )` t1) in
522 let t2v = fst(dest_binop `( *. )` t2) in
523 if (is_var t1v) & (is_var t2v) then term_order t1v t2v
524 else if (is_arith_const t2v) then true else false
525 with Failure _ -> false ;;
529 Int (Hashtbl.hash tm)
531 try let (a,b) = dest_binop `( *. )` tm in
532 (mon_sz a) */ (mon_sz b)
533 with Failure _ -> Int 1;;
535 let rec new_summand_order t1 t2 =
536 try let t1v = fst(dest_binop `( +. )` t1) in
537 let t2v = fst(dest_binop `( +. )` t2) in
538 (mon_sz t2v >/ mon_sz t1v)
539 with Failure _ -> false ;;
541 let rec new_distrib_order t1 t2 =
542 try let t2v = fst(dest_binop `( *. )` t2) in
543 if (is_arith_const t2v) then true else false
546 let t2' = fst(dest_binop `( +. )` t2) in
547 new_distrib_order t1 t2'
548 with Failure _ -> false ;;
550 let REAL_RDISTRIB = REAL_ARITH
551 `!x y z. (x + y) * z = (x * z) + (y * z)`;; (* new *)
553 let REAL_LDISTRIB = REAL_ADD_LDISTRIB;;
557 ONCE_REWRITE_CONV [GSYM REAL_SUB_0] THENC
559 REWRITE_CONV[real_div;REAL_RDISTRIB;REAL_SUB_RDISTRIB;
561 GSYM REAL_MUL_ASSOC;GSYM REAL_ADD_ASSOC;
562 REAL_ARITH `(x -. (--y) = x + y) /\ (x - y = x + (-- y)) /\
563 (--(x + y) = --x + (--y)) /\ (--(x - y) = --x + y)`;
565 `(x*.(-- y) = -- (x*. y)) /\ (--. (--. x) = x) /\
566 ((--. x)*.y = --.(x*.y))`;
567 REAL_SUB_LDISTRIB;REAL_LDISTRIB] THENC
568 (* move constants rightward on monomials *)
569 REWRITE_ORD_CONV new_factor_order false [REAL_MUL_AC;] THENC
570 GEN_REWRITE_CONV ONCE_DEPTH_CONV
571 [REAL_ARITH `-- x = (x*(-- &.1))`] THENC
572 REWRITE_CONV[GSYM REAL_MUL_ASSOC] THENC
573 REAL_RAT_REDUCE_CONV THENC
574 (* collect like monomials *)
575 REWRITE_ORD_CONV new_summand_order false [REAL_ADD_AC;] THENC
576 (* move constants leftward AND collect them together *)
577 REWRITE_ORD_CONV new_factor_order2 false [REAL_MUL_AC;] THENC
578 REWRITE_ORD_CONV new_distrib_order true [
579 REAL_ARITH `(a*b +. d*b = (a+d)*b) /\
580 (a*b + b = (a+ &.1)*b ) /\ ( b + a*b = (a+ &.1)*b) /\
581 (a*b +. d*b +e = (a+d)*b + e) /\
582 (a*b + b + e= (a+. &.1)* b +e ) /\
583 ( b + a*b + e = (a + &.1)*b +e) `;] THENC
584 REAL_RAT_REDUCE_CONV THENC
585 REWRITE_CONV[REAL_ARITH `(&.0 * x = &.0) /\ (x + &.0 = x) /\
588 let real_poly_tac = CONV_TAC real_poly_conv;;
590 let test_real_poly_tac = prove_by_refinement(
591 `!x y . (x + (&.2)*y)*(x- (&.2)*y) = (x*x -. (&.4)*y*y)`,
602 (* ------------------------------------------------------------------ *)
603 (* REAL INEQUALITIES *)
606 (* Take inequality certificate A + B1 + B2 +.... + P = C as a term.
607 Prove it as an inequality.
608 Reduce to an ineq (A < C) WITH side conditions
611 If (not strict), write as an ineq (A <= C) WITH side conditions
614 Expand each Bi (or P) that is a product U*V as 0 <= U /\ 0 <= V.
615 To prevent expansion of Bi write (U*V) as (&0 + (U*V)).
618 ineq_le_tac `A + B1 + B2 = C`;
621 (* ------------------------------------------------------------------ *)
624 let strict_lemma = prove_by_refinement(
625 `!A B C. (A+B = C) ==> ((&.0 <. B) ==> (A <. C) )`,
632 let weak_lemma = prove_by_refinement(
633 `!A B C. (A+B = C) ==> ((&.0 <=. B) ==> (A <=. C))`,
640 let strip_lt_lemma = prove_by_refinement(
641 `!B1 B2 C. ((&.0 <. (B1+B2)) ==> C) ==>
642 ((&.0 <. B2) ==> ((&.0 <=. B1) ==> C))`,
646 ASM_MESON_TAC[REAL_LET_ADD];
651 let strip_le_lemma = prove_by_refinement(
652 `!B1 B2 C. ((&.0 <=. (B1+B2)) ==> C) ==>
653 ((&.0 <=. B2) ==> ((&.0 <=. B1) ==> C))`,
657 ASM_MESON_TAC[REAL_LE_ADD];
662 let is_x_prod_le tm =
663 try let hyp = fst(dest_binop `( ==> )` tm) in
664 let arg = snd(dest_binop `( <=. ) ` hyp) in
665 let fac = dest_binop `( *. )` arg in
667 with Failure _ -> false;;
669 let switch_lemma_le_order t1 t2 =
670 if (is_x_prod_le t1) & (is_x_prod_le t2) then
671 term_order t1 t2 else
672 if (is_x_prod_le t2) then true else false;;
674 let is_x_prod_lt tm =
675 try let hyp = fst(dest_binop `( ==> )` tm) in
676 let arg = snd(dest_binop `( <. ) ` hyp) in
677 let fac = dest_binop `( *. )` arg in
679 with Failure _ -> false;;
681 let switch_lemma_lt_order t1 t2 =
682 if (is_x_prod_lt t1) & (is_x_prod_lt t2) then
683 term_order t1 t2 else
684 if (is_x_prod_lt t2) then true else false;;
686 let switch_lemma_le = prove_by_refinement(
687 `!A B C. ((&.0 <= A) ==> (&.0 <= B) ==> C) =
688 ((&.0 <=. B) ==> (&.0 <= A) ==> C)`,
695 let switch_lemma_let = prove_by_refinement(
696 `!A B C. ((&.0 < A) ==> (&.0 <= B) ==> C) =
697 ((&.0 <=. B) ==> (&.0 < A) ==> C)`,
704 let switch_lemma_lt = prove_by_refinement(
705 `!A B C. ((&.0 < A) ==> (&.0 < B) ==> C) =
706 ((&.0 <. B) ==> (&.0 < A) ==> C)`,
713 let expand_prod_lt = prove_by_refinement(
714 `!B1 B2 C. (&.0 < B1*B2 ==> C) ==>
715 ((&.0 <. B1) ==> (&.0 <. B2) ==> C)`,
718 ASM_MESON_TAC[REAL_LT_MUL ];
722 let expand_prod_le = prove_by_refinement(
723 `!B1 B2 C. (&.0 <= B1*B2 ==> C) ==>
724 ((&.0 <=. B1) ==> (&.0 <=. B2) ==> C)`,
728 ASM_MESON_TAC[REAL_LE_MUL ];
734 let ineq_cert_gen_tac v cert =
735 let DISCH_RULE f = DISCH_THEN (fun t-> MP_TAC (f t)) in
737 (MP_TAC o (REWRITE_CONV[REAL_POW_2] THENC real_poly_conv)) THEN
739 DISCH_RULE (MATCH_MP v) THEN
740 DISCH_RULE (repeat (MATCH_MP strip_lt_lemma)) THEN
741 DISCH_RULE (repeat (MATCH_MP strip_le_lemma)) THEN
742 DISCH_RULE (repeat (MATCH_MP expand_prod_lt o
744 (REWRITE_ORD_CONV switch_lemma_lt_order true[switch_lemma_lt])))) THEN
745 DISCH_RULE (repeat (MATCH_MP expand_prod_le o
746 (CONV_RULE (REWRITE_ORD_CONV switch_lemma_le_order true
747 [switch_lemma_le])) o
748 (REWRITE_RULE[switch_lemma_let]))) THEN
749 DISCH_RULE (repeat (MATCH_MP
750 (TAUT `(A ==> B==>C) ==> (A /\ B ==> C)`))) THEN
751 REWRITE_TAC[REAL_MUL_LID] THEN
752 DISCH_THEN MATCH_MP_TAC THEN
753 CONV_TAC REAL_RAT_REDUCE_CONV THEN
754 ASM_SIMP_TAC[REAL_LE_POW_2;
755 REAL_ARITH `(&.0 < x ==> &.0 <= x) /\ (&.0 + x = x) /\
756 (a <= b ==> &.0 <= b - a) /\
757 (a < b ==> &.0 <= b - a) /\
758 (~(b < a) ==> &.0 <= b - a) /\
759 (~(b <= a) ==> &.0 <= b - a) /\
760 (a < b ==> &.0 < b - a) /\
761 (~(b <= a) ==> &.0 < b - a)`];;
763 let ineq_lt_tac = ineq_cert_gen_tac strict_lemma;;
764 let ineq_le_tac = ineq_cert_gen_tac weak_lemma;;
769 let test_ineq_tac = prove_by_refinement(
770 `!x y z. (&.0 <= x*y) /\ (&.0 <. z) ==>
771 (x*y) <. x*x + (&.3)*x*y + &.4 `,
775 ineq_lt_tac `x * y + x pow 2 + &2 * (&.0 + x * y) + &2 * &2 = x * x + &3 * x * y + &4`;
781 (* ------------------------------------------------------------------ *)
782 (* Move quantifier left. Use class.ml and theorems.ml to bubble
783 quantifiers towards the head of an expression. It should move
784 quantifiers past other quantifiers, past conjunctions, disjunctions,
787 val quant_left_CONV : string -> term -> thm = <fun>
789 var_name:string -- The name of the variable that is to be shifted.
791 It tends to return `T` when the conversion fails.
794 quant_left_CONV "a" `!b. ?a. a = b*4`;;
795 val it : thm = |- (!b. ?a. a = b *| 4) <=> (?a. !b. a b = b *| 4)
797 (* ------------------------------------------------------------------ *)
799 let tagb = new_definition `TAGB (x:bool) = x`;;
801 let is_quant tm = (is_forall tm) or (is_exists tm);;
803 (*** JRH replaced Comb and Abs with abstract type constructors ***)
805 let rec tag_quant var_name tm =
806 if (is_forall tm && (fst (dest_var (fst (dest_forall tm))) = var_name))
807 then mk_comb (`TAGB`,tm)
808 else if (is_exists tm && (fst (dest_var (fst (dest_exists tm))) = var_name)) then mk_comb (`TAGB`,tm)
810 | Comb (x,y) -> mk_comb(tag_quant var_name x,tag_quant var_name y)
811 | Abs (x,y) -> mk_abs(x,tag_quant var_name y)
814 let quant_left_CONV =
816 let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
817 let NOT_FORALL_TAG = prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
818 REWRITE_TAC[tagb;NOT_FORALL_THM]) in
820 prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
821 ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
823 prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
824 REWRITE_TAC[tagb;SKOLEM_THM]) in
826 let SWAP_FORALL_TAG =
827 prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
828 REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
829 let SWAP_EXISTS_THM = iprove
830 `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
832 let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
833 (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
834 let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ Q) <=>
835 (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
836 let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
837 (!x. P /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
838 let TRIV_OR_FORALL_TAG = prove
839 (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
840 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
841 let RIGHT_IMP_FORALL_TAG = prove
842 (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
843 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
844 let OR_EXISTS_THM = iprove
845 `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
846 let LEFT_OR_EXISTS_THM = iprove
847 `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
848 let RIGHT_OR_EXISTS_THM = iprove
849 `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
850 let LEFT_AND_EXISTS_THM = iprove
851 `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
852 let RIGHT_AND_EXISTS_THM = iprove
853 `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
854 let TRIV_AND_EXISTS_THM = iprove
855 `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
856 let LEFT_IMP_EXISTS_THM = iprove
857 `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
858 let TRIV_FORALL_IMP_THM = iprove
859 `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
860 let TRIV_EXISTS_IMP_THM = iprove
861 `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
862 let NOT_EXISTS_TAG = prove(
863 `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
864 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
865 let LEFT_OR_FORALL_TAG = prove
866 (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
867 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
868 let RIGHT_OR_FORALL_TAG = prove
869 (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
870 REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
871 let LEFT_IMP_FORALL_TAG = prove
872 (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
873 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
874 let RIGHT_IMP_EXISTS_TAG = prove
875 (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
876 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
881 [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
882 SWAP_FORALL_TAG;SWAP_EXISTS_THM;
884 AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
885 TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
886 OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
888 RIGHT_AND_EXISTS_THM;
889 TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
890 TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
891 LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
892 RIGHT_IMP_EXISTS_TAG;
894 (tag_quant var_name tm));;
896 (* same, but never pass a quantifier past another. No Skolem, etc. *)
897 let quant_left_noswap_CONV =
899 let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
900 let NOT_FORALL_TAG = prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
901 REWRITE_TAC[tagb;NOT_FORALL_THM]) in
903 prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
904 ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
906 prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
907 REWRITE_TAC[tagb;SKOLEM_THM]) in
909 let SWAP_FORALL_TAG =
910 prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
911 REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
912 let SWAP_EXISTS_THM = iprove
913 `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
915 let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
916 (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
917 let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ Q) <=>
918 (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
919 let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
920 (!x. P /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
921 let TRIV_OR_FORALL_TAG = prove
922 (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
923 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
924 let RIGHT_IMP_FORALL_TAG = prove
925 (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
926 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
927 let OR_EXISTS_THM = iprove
928 `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
929 let LEFT_OR_EXISTS_THM = iprove
930 `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
931 let RIGHT_OR_EXISTS_THM = iprove
932 `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
933 let LEFT_AND_EXISTS_THM = iprove
934 `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
935 let RIGHT_AND_EXISTS_THM = iprove
936 `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
937 let TRIV_AND_EXISTS_THM = iprove
938 `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
939 let LEFT_IMP_EXISTS_THM = iprove
940 `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
941 let TRIV_FORALL_IMP_THM = iprove
942 `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
943 let TRIV_EXISTS_IMP_THM = iprove
944 `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
945 let NOT_EXISTS_TAG = prove(
946 `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
947 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
948 let LEFT_OR_FORALL_TAG = prove
949 (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
950 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
951 let RIGHT_OR_FORALL_TAG = prove
952 (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
953 REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
954 let LEFT_IMP_FORALL_TAG = prove
955 (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
956 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
957 let RIGHT_IMP_EXISTS_TAG = prove
958 (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
959 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
964 [NOT_FORALL_TAG; (* SKOLEM_TAG;SKOLEM_TAG2; *)
965 (* SWAP_FORALL_TAG;SWAP_EXISTS_THM;
967 AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
968 TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
969 OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
971 RIGHT_AND_EXISTS_THM;
972 TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
973 TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
974 LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
975 RIGHT_IMP_EXISTS_TAG;
977 (tag_quant var_name tm));;
979 let quant_right_CONV =
981 let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
982 let NOT_FORALL_TAG = prove(`!P. TAGB(?x:A. ~(P x)) <=> ~((!x. P x))`,
983 REWRITE_TAC[tagb;GSYM NOT_FORALL_THM]) in
985 prove(`!P. ( TAGB(!(x:A). ?y. P x ((y:B)))) <=>
986 (?y. (!(x:A). P x ((y:A->B) x)))`,
987 REWRITE_TAC[tagb;GSYM SKOLEM_THM])
990 prove(`!P. TAGB(?y. !x. P x (y x)) <=> (!x:A. (?y:B. P x y))`,
991 REWRITE_TAC[tagb;GSYM SKOLEM_THM]) in
992 (* !1 !2 -> !2 !1.. *)
993 let SWAP_FORALL_TAG =
994 prove(`!P:A->B->bool. TAGB(!y x. P x y) <=> (!x. (! y. P x y))`,
995 REWRITE_TAC[GSYM SWAP_FORALL_THM;tagb]) in
996 let SWAP_EXISTS_THM = iprove
997 `!P:A->B->bool. TAGB (?y x. P x y) <=> (?x. (?y. P x y))` in
999 let AND_FORALL_TAG = iprove`!P Q. TAGB(!x. P x /\ Q x) <=>
1000 ((!x. P x) /\ (!x. Q x))` in
1001 let LEFT_AND_FORALL_TAG = prove(`!P Q.
1002 TAGB(!x. P x /\ Q ) <=> ((!x. P x) /\ Q)`,
1003 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
1004 let RIGHT_AND_FORALL_TAG = prove(`!P Q.
1005 TAGB(!x. P /\ Q x) <=> P /\ (!x. Q x)`,
1006 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
1007 let TRIV_OR_FORALL_TAG = prove
1008 (`!P Q. TAGB(!x:A. P \/ Q) <=>(!x:A. P) \/ (!x:A. Q)`,
1009 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
1010 let RIGHT_IMP_FORALL_TAG = prove
1011 (`!P Q. TAGB (!x. P ==> Q x) <=> (P ==> (!x:A. Q x)) `,
1012 REWRITE_TAC[tagb] THEN ITAUT_TAC) in
1013 let OR_EXISTS_THM = iprove
1014 `!P Q. TAGB(?x:A. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x) ` in
1015 let LEFT_OR_EXISTS_THM = iprove
1016 `!P Q. TAGB (?x:A. P x \/ Q) <=> (?x. P x) \/ Q ` in
1017 let RIGHT_OR_EXISTS_THM = iprove
1018 `!P Q.TAGB (?x:A. P \/ Q x) <=> P \/ (?x. Q x)` in
1019 let LEFT_AND_EXISTS_THM = iprove
1020 `!P Q.TAGB (?x:A. P x /\ Q) <=> (?x:A. P x) /\ Q` in
1021 let RIGHT_AND_EXISTS_THM = iprove
1022 `!P Q. TAGB (?x:A. P /\ Q x) <=> P /\ (?x:A. Q x) ` in
1023 let TRIV_AND_EXISTS_THM = iprove
1024 `!P Q. TAGB(?x:A. P /\ Q) <=> (?x:A. P) /\ (?x:A. Q) ` in (* *)
1025 let LEFT_IMP_EXISTS_THM = iprove
1026 `!P Q. TAGB(!x. P x ==> Q) <=> ( (?x:A. P x) ==> Q) ` in (* *)
1027 let TRIV_FORALL_IMP_THM = iprove
1028 `!P Q. TAGB(!x:A. P ==> Q) <=> ( (?x:A. P) ==> (!x:A. Q)) ` in
1029 let TRIV_EXISTS_IMP_THM = iprove
1030 `!P Q. TAGB(?x:A. P ==> Q) <=> ((!x:A. P) ==> (?x:A. Q)) ` in
1031 let NOT_EXISTS_TAG = prove(
1032 `!P. TAGB(!x. ~(P x)) <=> ~((?x:A. P x)) `,
1033 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
1034 let LEFT_OR_FORALL_TAG = prove
1035 (`!P Q. TAGB(!x. P x \/ Q) <=> (!x:A. P x) \/ Q `,
1036 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
1037 let RIGHT_OR_FORALL_TAG = prove
1038 (`!P Q. TAGB(!x. P \/ Q x) <=> P \/ (!x:A. Q x) `,
1039 REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
1040 let LEFT_IMP_FORALL_TAG = prove
1041 (`!P Q. TAGB(?x. P x ==> Q) <=> ((!x:A. P x) ==> Q) `,
1042 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
1043 let RIGHT_IMP_EXISTS_TAG = prove
1044 (`!P Q. TAGB(?x:A. P ==> Q x) <=> (P ==> (?x:A. Q x)) `,
1045 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
1050 [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
1051 SWAP_FORALL_TAG;SWAP_EXISTS_THM;
1053 AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
1054 TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
1055 OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
1056 LEFT_AND_EXISTS_THM;
1057 RIGHT_AND_EXISTS_THM;
1058 TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
1059 TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
1060 LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
1061 RIGHT_IMP_EXISTS_TAG;
1063 (tag_quant var_name tm));;
1066 (* ------------------------------------------------------------------ *)
1067 (* Dropping Superfluous Quantifiers .
1068 Example: ?u. (u = t) /\ ...
1069 We can eliminate the u.
1071 (* ------------------------------------------------------------------ *)
1073 let mark_term = new_definition `mark_term (u:A) = u`;;
1075 (*** JRH replaced Comb and Abs with explicit constructors ***)
1077 let rec markq qname tm =
1079 Var (a,b) -> if (a=qname) then mk_icomb (`mark_term:A->A`,tm) else tm
1081 |Comb(s,b) -> mk_comb(markq qname s,markq qname b)
1082 |Abs (x,t) -> mk_abs(x,markq qname t);;
1084 let rec getquants tm =
1085 if (is_forall tm) then
1086 (fst (dest_var (fst (dest_forall tm))))::
1087 (getquants (snd (dest_forall tm)))
1088 else if (is_exists tm) then
1089 (fst (dest_var (fst (dest_exists tm))))::
1090 (getquants (snd (dest_exists tm)))
1092 Comb(s,b) -> (getquants s) @ (getquants b)
1093 | Abs (x,t) -> (getquants t)
1096 (* can loop if there are TWO *)
1097 let rewrite_conjs = [
1098 prove_by_refinement (`!A B C. (A /\ B) /\ C <=> A /\ B /\ C`,[REWRITE_TAC[CONJ_ACI]]);
1099 prove_by_refinement (`!u. (mark_term (u:A) = mark_term u) <=> T`,[MESON_TAC[]]);
1100 prove_by_refinement (`!u t. (t = mark_term (u:A)) <=> (mark_term u = t)`,[MESON_TAC[]]);
1101 prove_by_refinement (`!u a b. (mark_term (u:A) = a) /\ (mark_term u = b) <=> (mark_term u = a) /\ (a = b)`,[MESON_TAC[]]);
1102 prove_by_refinement (`!u a b B. (mark_term (u:A) = a) /\ (mark_term u = b) /\ B <=> (mark_term u = a) /\ (a = b) /\ B`,[MESON_TAC[]]);
1103 prove_by_refinement (`!u t A C. A /\ (mark_term (u:A) = t) /\ C <=>
1104 (mark_term u = t) /\ A /\ C`,[MESON_TAC[]]);
1105 prove_by_refinement (`!A u t. A /\ (mark_term (u:A) = t) <=>
1106 (mark_term u = t) /\ A `,[MESON_TAC[]]);
1107 prove_by_refinement (`!u t C D. (((mark_term (u:A) = t) /\ C) ==> D) <=>
1108 ((mark_term (u:A) = t) ==> C ==> D)`,[MESON_TAC[]]);
1109 prove_by_refinement (`!A u t B. (A ==> (mark_term (u:A) = t) ==> B) <=>
1110 ((mark_term (u:A) = t) ==> A ==> B)`,[MESON_TAC[]]);
1113 let higher_conjs = [
1114 prove_by_refinement (`!C u t. ((mark_term u = t) ==> C (mark_term u)) <=>
1115 ((mark_term u = t) ==> C (t:A))`,[MESON_TAC[mark_term]]);
1116 prove_by_refinement (`!C u t. ((mark_term u = t) /\ C (mark_term u)) <=>
1117 ((mark_term u = t) /\ C (t:A))`,[MESON_TAC[mark_term]]);
1123 REWRITE_CONV [prove_by_refinement (`!t. ?(u:A). (u = t)`,[MESON_TAC[]])] in
1125 let quanlist = getquants tm in
1126 let quantleft_CONV = EVERY_CONV
1127 (map (REPEATC o quant_left_noswap_CONV) quanlist) in
1128 let qname_conv tm = prove(mk_eq(tm,markq qname tm),
1129 REWRITE_TAC[mark_term]) in
1130 let conj_conv = REWRITE_CONV rewrite_conjs in
1131 let quantright_CONV = (REPEATC (quant_right_CONV qname)) in
1132 let drop_mark_CONV = REWRITE_CONV [mark_term] in
1133 (quantleft_CONV THENC qname_conv THENC conj_conv THENC
1134 (ONCE_REWRITE_CONV higher_conjs)
1135 THENC drop_mark_CONV THENC quantright_CONV THENC
1140 dropq_conv "u" `!P Q R . (?(u:B). (?(x:A). (u = P x) /\ (Q x)) /\ (R u))`;;
1141 dropq_conv "t" `!P Q R. (!(t:B). (?(x:A). P x /\ (t = Q x)) ==> R t)`;;
1143 dropq_conv "u" `?u v.
1144 ((t * (a + &1) + (&1 - t) *a = u) /\
1145 (t * (b + &0) + (&1 - t) * b = v)) /\
1152 (* ------------------------------------------------------------------ *)
1153 (* SOME GENERAL TACTICS FOR THE ASSUMPTION LIST *)
1154 (* ------------------------------------------------------------------ *)
1156 let (%) i = HYP (string_of_int i);;
1158 let WITH i rule = (H_VAL (rule) (HYP (string_of_int i))) ;;
1160 let (UND:int -> tactic) =
1162 let (asl,w) = dest_goal gl in
1163 let name = "Z-"^(string_of_int i) in
1164 try let thm= assoc name asl in
1165 let tm = concl (thm) in
1166 let (_,asl') = partition (fun t-> ((=) name (fst t))) asl in
1167 null_meta,[asl',mk_imp(tm,w)],
1168 fun i [th] -> MP th (INSTANTIATE_ALL i thm)
1169 with Failure _ -> failwith "UND";;
1172 (UND i) THEN (DISCH_THEN (fun t -> ALL_TAC));;
1174 let USE i rule = (WITH i rule) THEN (KILL i);;
1176 let CHO i = (UND i) THEN (DISCH_THEN CHOOSE_TAC);;
1178 let X_CHO i t = (UND i) THEN (DISCH_THEN (X_CHOOSE_TAC t));;
1180 let AND i = (UND i) THEN
1181 (DISCH_THEN (fun t-> (ASSUME_TAC (CONJUNCT1 t)
1182 THEN (ASSUME_TAC (CONJUNCT2 t)))));;
1185 (H_VAL2 CONJ ((%)i) ((%)j)) THEN (KILL i) THEN (KILL j);;
1187 let COPY i = WITH i I;;
1189 let REP n tac = EVERY (replicate tac n);;
1191 let REWR i = (UND i) THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;;
1193 let LEFT i t = (USE i (CONV_RULE (quant_left_CONV t)));;
1195 let RIGHT i t = (USE i (CONV_RULE (quant_right_CONV t)));;
1197 let LEFT_TAC t = ((CONV_TAC (quant_left_CONV t)));;
1199 let RIGHT_TAC t = ( (CONV_TAC (quant_right_CONV t)));;
1201 let INR = REWRITE_RULE[IN];;
1207 let rec REP n tac = if (n<=0) then ALL_TAC
1208 else (tac THEN (REP (n-1) tac));; (* doesn't seem to work? *)
1211 let COPY i = (UNDISCH_WITH i) THEN (DISCH_THEN (fun t->ALL_TAC));;
1214 MANIPULATING ASSUMPTIONS. (MAKE 0= GOAL)
1216 COPY: int -> tactic Make a copy in adjacent slot.
1219 EXPAND: int -> tactic.
1220 conjunction -> two separate.
1221 exists/goal-forall -> choose.
1222 goal-if-then -> discharge
1223 EXPAND_TERM: int -> term -> tactic.
1224 constant -> expand definition or other rewrites associated.
1225 ADD: term -> tactic.
1227 SIMPLIFY: int -> tactic. Apply simplification rules.
1232 let CONTRAPOSITIVE_TAC = MATCH_MP_TAC (TAUT `(~q ==> ~p) ==> (p ==> q)`)
1233 THEN REWRITE_TAC[];;
1235 let REWRT_TAC = (fun t-> REWRITE_TAC[t]);;
1237 let REAL_HALF_DOUBLE = REAL_ARITH `!x. (x / &2) + (x / &2) = x`;;
1238 let REAL_DOUBLE = REAL_ARITH `!x. x + x = &2 * x`;;
1239 let ABS_ZERO = REAL_ABS_ZERO;; (* new *)
1240 let ABS_ABS = REAL_ABS_ABS;;
1242 let (REDUCE_CONV,REDUCE_TAC) =
1244 (* reals *) REAL_NEG_GE0;
1249 REAL_ADD_LINV;REAL_ADD_RINV;
1258 REAL_ARITH `!(x:real). (--x = x) <=> (x = &.0)`;
1259 REAL_ARITH `!(a:real) b. (a - b + b) = a`;
1291 prove (`(--. (&.n) < (&.m)) <=> (&.0 < (&.n) + (&.m))`,REAL_ARITH_TAC);
1292 prove (`(--. (&.n) <= (&.m)) <=> (&.0 <= (&.n) + (&.m))`,REAL_ARITH_TAC);
1293 prove (`(--. (&.n) = (&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC);
1294 prove (`((&.n) < --.(&.m)) <=> ((&.n) + (&.m) <. (&.0))`,REAL_ARITH_TAC);
1295 prove (`((&.n) <= --.(&.m)) <=> ((&.n) + (&.m) <=. (&.0))`,REAL_ARITH_TAC);
1296 prove (`((&.n) = --.(&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC);
1297 prove (`((&.n) < --.(&.m) + &.r) <=> ((&.n) + (&.m) < (&.r))`,REAL_ARITH_TAC);
1298 prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC);
1299 prove (`(--(&.n) < --.(&.m) + &.r) <=> ( (&.m) < &.n + (&.r))`,REAL_ARITH_TAC);
1300 prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC);
1301 prove (`((--. (&.1))* x < --. y <=> y < x)`,REAL_ARITH_TAC );
1302 prove (`((--. (&.1))* x <= --. y <=> y <= x)`,REAL_ARITH_TAC );
1307 ARITH_RULE `0+| m = m`;
1309 prove (`(0 = m +|n) <=> (m = 0)/\ (n=0)`,MESON_TAC[ADD_EQ_0]);
1314 ARITH_RULE `(0 = j -| i) <=> (j <=| i)`;
1315 ARITH_RULE `(j -| i = 0) <=> (j <=| i)`;
1316 ARITH_RULE `0 -| i = 0`;
1317 ARITH_RULE `(i<=| j) /\ (j <=| i) <=> (i = j)`;
1318 ARITH_RULE `0 <| 1`;
1327 ARITH_RULE `SUC b -| 1 = b`;
1328 ARITH_RULE `SUC b -| b = 1`;
1329 prove(`&.(SUC x) - &.x = &.1`,
1330 REWRITE_TAC [REAL_ARITH `(a -. b=c) <=> (a = b+.c)`;
1331 REAL_OF_NUM_ADD;REAL_OF_NUM_EQ] THEN ARITH_TAC);
1357 GSYM INT_NEG_MINUS1;
1362 (REWRITE_CONV list,REWRITE_TAC list);;
1368 (* prove by squaring *)
1369 let REAL_POW_2_LE = prove_by_refinement(
1370 `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <=. y pow 2) ==> (x <=. y)`,
1374 MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LE);
1376 ASM_SIMP_TAC[REAL_POW_LE];
1377 ASM_SIMP_TAC[POW_2_SQRT];
1381 (* prove by squaring *)
1382 let REAL_POW_2_LT = prove_by_refinement(
1383 `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <. y pow 2) ==> (x <. y)`,
1388 MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LT);
1390 ASM_SIMP_TAC[REAL_POW_LE];
1391 ASM_SIMP_TAC[POW_2_SQRT];
1398 MATCH_MP_TAC REAL_LE_LSQRT;
1399 MATCH_MP_TAC REAL_POW_2_LT;
1400 MATCH_MP_TAC REAL_POW_2_LE
1402 THEN REWRITE_TAC[];;
1406 let SPEC2_TAC t = SPEC_TAC (t,t);;
1408 let IN_ELIM i = (USE i (REWRITE_RULE[IN]));;
1411 if (n>0) then (i::(range (i+1) (n-1))) else [];;
1414 (* in elimination *)
1416 let (IN_OUT_TAC: tactic) =
1417 fun gl -> (REWRITE_TAC [IN] THEN
1418 (EVERY (map (IN_ELIM) (range 0 (length (goal_asms gl)))))) gl;;
1420 let (IWRITE_TAC : thm list -> tactic) =
1421 fun thlist -> REWRITE_TAC (map INR thlist);;
1423 let (IWRITE_RULE : thm list -> thm -> thm) =
1424 fun thlist -> REWRITE_RULE (map INR thlist);;
1426 let IMATCH_MP imp ant = MATCH_MP (INR imp) (INR ant);;
1428 let IMATCH_MP_TAC imp = MATCH_MP_TAC (INR imp);;
1431 let GBETA_TAC = (CONV_TAC (TOP_DEPTH_CONV GEN_BETA_CONV));;
1432 let GBETA_RULE = (CONV_RULE (TOP_DEPTH_CONV GEN_BETA_CONV));;
1434 (* breaks antecedent into multiple cases *)
1436 REPEAT (DISCH_THEN (REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC));;
1438 let TSPEC t i = TYPE_THEN t (USE i o SPEC);;
1440 let IMP_REAL t i = (USE i (MATCH_MP (REAL_ARITH t)));;
1442 (* goes from f = g to fz = gz *)
1443 let TAPP z i = TYPE_THEN z (fun u -> (USE i(fun t -> AP_THM t u)));;
1445 (* ONE NEW TACTIC -- DOESN'T WORK!! DON'T USE....
1446 let CONCL_TAC t = let co = snd (dest_imp (concl t)) in
1447 SUBGOAL_MP_TAC co THEN (TRY (IMATCH_MP_TAC t));;
1450 (* subgoal the antecedent of a THM, in order to USE the conclusion *)
1451 let ANT_TAC t = let (ant,co) = (dest_imp (concl t)) in
1453 THENL [ALL_TAC;DISCH_THEN (fun u-> MP_TAC (MATCH_MP t u))];;
1456 let TH_INTRO_TAC tl th = TYPEL_THEN tl (fun t-> ANT_TAC (ISPECL t th));;
1458 let THM_INTRO_TAC tl th = TYPEL_THEN tl
1460 let s = ISPECL t th in
1461 if is_imp (concl s) then ANT_TAC s else ASSUME_TAC s);;
1463 let (DISCH_THEN_FULL_REWRITE:tactic) =
1464 DISCH_THEN (fun t-> REWRITE_TAC[t] THEN
1465 (RULE_ASSUM_TAC (REWRITE_RULE[t])));;
1467 let FULL_REWRITE_TAC t = (REWRITE_TAC t THEN (RULE_ASSUM_TAC (REWRITE_RULE t)));;
1469 (* ------------------------------------------------------------------ *)
1473 IMATCH_MP_TAC (TAUT ` (a ==> b ==> C) ==> ( a /\ b ==> C)`);
1474 DISCH_THEN (CHOOSE_THEN MP_TAC);
1475 FIRST_ASSUM (fun t-> UNDISCH_TAC (concl t) THEN
1476 (DISCH_THEN CHOOSE_TAC));
1477 FIRST_ASSUM (fun t ->
1478 (if (length (CONJUNCTS t) < 2) then failwith "BASIC_TAC"
1479 else UNDISCH_TAC (concl t)));
1483 let REP_BASIC_TAC = REPEAT (CHANGED_TAC (FIRST BASIC_TAC));;
1485 (* ------------------------------------------------------------------ *)
1487 let USE_FIRST rule =
1488 FIRST_ASSUM (fun t -> (UNDISCH_TAC (concl t) THEN
1489 (DISCH_THEN (ASSUME_TAC o rule))));;
1491 let WITH_FIRST rule =
1492 FIRST_ASSUM (fun t -> ASSUME_TAC (rule t));;
1494 let UNDF t = (TYPE_THEN t UNDISCH_FIND_TAC );;
1496 let GRABF t ttac = (UNDF t THEN (DISCH_THEN ttac));;
1499 (TYPE_THEN t (fun t' -> UNDISCH_FIND_THEN t'
1500 (fun u -> ASSUME_TAC (rule u))));;
1503 (* ------------------------------------------------------------------ *)
1504 (* UNIFY_EXISTS_TAC *)
1505 (* ------------------------------------------------------------------ *)
1507 let rec EXISTSL_TAC tml = match tml with
1508 a::tml' -> EXISTS_TAC a THEN EXISTSL_TAC tml' |
1512 Goal: ?x1....xn. P1 /\ ... /\ Pm
1513 Try to pick ALL of x1...xn to unify ONE or more Pi with terms
1514 appearing in the assumption list, trying term_unify on
1515 each Pi with each assumption.
1517 let (UNIFY_EXISTS_TAC:tactic) =
1518 let run_one wc assum (varl,sofar) =
1519 if varl = [] then (varl,sofar) else
1521 let wc' = instantiate ([],sofar,[]) wc in
1522 let (_,ins,_) = term_unify varl wc' assum in
1523 let insv = map snd ins in
1524 ( subtract varl insv , union sofar ins )
1525 ) with failure -> (varl,sofar) in
1526 let run_onel asl wc (varl,sofar) =
1527 itlist (run_one wc) asl (varl,sofar) in
1528 let run_all varl sofar wcl asl =
1529 itlist (run_onel asl) wcl (varl,sofar) in
1530 let full_unify asl w =
1531 let (varl,ws) = strip_exists w in
1532 let vargl = map genvar (map type_of varl) in
1533 let wg = instantiate ([],zip vargl varl,[]) ws in
1534 let wcg = conjuncts wg in
1535 let (vargl',sofar) = run_all vargl [] wcg ( asl) in
1536 if (vargl' = []) then
1537 map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl)
1538 else failwith "full_unify: unification not found " in
1540 let (asl,w) = dest_goal gl in
1542 let asl' = map (concl o snd) asl in
1543 let asl'' = flat (map (conjuncts ) asl') in
1544 let varsub = full_unify asl'' w in
1545 EXISTSL_TAC varsub gl
1546 ) with failure -> failwith "UNIFY_EXIST_TAC: unification not found.";;
1548 (* partial example *)
1549 let unify_exists_tac_example = try(prove_by_refinement(
1550 `!C a b v A R TX U SS. (A v /\ (a = v) /\ (C:num->num->bool) a b /\ R a ==>
1551 ?v v'. TX v' /\ U v v' /\ C v' v /\ SS v)`,
1556 UNIFY_EXISTS_TAC; (* v' -> a and v -> b *)
1557 (* not finished. Here is a variant approach. *)
1561 ])) with failure -> (REFL `T`);;
1565 (* ------------------------------------------------------------------ *)
1566 (* UNIFY_EXISTS conversion *)
1567 (* ------------------------------------------------------------------ *)
1570 FIRST argument is the "certificate"
1571 second arg is the goal.
1573 UNIFY_EXISTS `(f:num->bool) x` `?t. (f:num->bool) t`
1576 let (UNIFY_EXISTS:thm -> term -> thm) =
1577 let run_one wc assum (varl,sofar) =
1578 if varl = [] then (varl,sofar) else
1580 let wc' = instantiate ([],sofar,[]) wc in
1581 let (_,ins,_) = term_unify varl wc' assum in
1582 let insv = map snd ins in
1583 ( subtract varl insv , union sofar ins )
1584 ) with failure -> (varl,sofar) in
1585 let run_onel asl wc (varl,sofar) =
1586 itlist (run_one wc) asl (varl,sofar) in
1587 let run_all varl sofar wcl asl =
1588 itlist (run_onel asl) wcl (varl,sofar) in
1589 let full_unify (t,w) =
1590 let (varl,ws) = strip_exists w in
1591 let vargl = map genvar (map type_of varl) in
1592 let wg = instantiate ([],zip vargl varl,[]) ws in
1593 let wcg = conjuncts wg in
1594 let (vargl',sofar) = run_all vargl [] wcg ( [concl t]) in
1595 if (vargl' = []) then
1596 map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl)
1597 else failwith "full_unify: unification not found " in
1600 if not(is_exists w) then failwith "UNIFY_EXISTS: not EXISTS" else
1601 let varl' = (full_unify (t,w)) in
1602 let (varl,ws) = strip_exists w in
1603 let varsub = zip varl' varl in
1604 let varlb = map (fun s-> chop_list s (rev varl))
1605 (range 1 (length varl)) in
1606 let targets = map (fun s-> (instantiate ([],varsub,[])
1607 (list_mk_exists( rev (fst s), ws)) )) varlb in
1608 let target_zip = zip (rev targets) varl' in
1609 itlist (fun s th -> EXISTS s th) target_zip t
1610 ) with failure -> failwith "UNIFY_EXISTS: unification not found.";;
1612 let unify_exists_example=
1613 UNIFY_EXISTS (ARITH_RULE `2 = 0+2`) `(?x y. ((x:num) = y))`;;
1615 (* now make a prover for it *)
1618 (* ------------------------------------------------------------------ *)
1621 drop_ant_tac replaces
1629 let DROP_ANT_TAC pq =
1630 UNDISCH_TAC pq THEN (UNDISCH_TAC (fst (dest_imp pq))) THEN
1631 DISCH_THEN (fun pthm -> ASSUME_TAC pthm THEN
1632 DISCH_THEN (fun pqthm -> ASSUME_TAC (MATCH_MP pqthm pthm )));;
1634 let (DROP_ALL_ANT_TAC:tactic) =
1636 let imps = filter (is_imp) (map (concl o snd) (goal_asms gl)) in
1637 MAP_EVERY (TRY o DROP_ANT_TAC) imps gl;;
1639 let drop_ant_tac_example = prove_by_refinement(
1640 `!A B C D E. (A /\ (A ==> B) /\ (C ==>D) /\ C) ==> (E \/ C \/ B)`,
1649 (* ------------------------------------------------------------------ *)
1651 (* ASSUME tm, then prove it later. almost the same as asm-cases-tac *)
1652 let (BACK_TAC : term -> tactic) =
1654 let ng = mk_imp (tm,goal_concl gl) in
1655 (SUBGOAL_MP_TAC ng THENL [ALL_TAC;DISCH_THEN IMATCH_MP_TAC ]) gl;;
1657 (* working with hashed assumptions *)
1659 let hash_of_term = Hash_term.hash_of_term;;
1661 let HASH_UNDISCH_TAC h =
1662 FIRST_X_ASSUM (fun t->
1663 let _ = (hash_of_term (concl t) = h) or failwith "bad hash" in
1666 let HASH_COPY_TAC h = HASH_UNDISCH_TAC h THEN (DISCH_THEN (fun t -> ASSUME_TAC t THEN ASSUME_TAC t));;
1668 let HASH_RULE_TAC h r = HASH_UNDISCH_TAC h THEN DISCH_THEN (fun t -> MP_TAC (r t));;
1670 let HASH_KILL_TAC h = HASH_UNDISCH_TAC h THEN (DISCH_THEN (fun t -> ALL_TAC));;
1672 let HASH_CHOOSE_TAC h = HASH_UNDISCH_TAC h THEN (DISCH_THEN CHOOSE_TAC);;
1674 let HASH_X_CHOOSE_TAC h t = HASH_UNDISCH_TAC h THEN (DISCH_THEN (X_CHOOSE_TAC t));;
1676 let HASH_ASM_REWRITE_TAC h gl =
1677 let (asl2) = filter (fun t -> not(hash_of_term (concl (snd t)) = h)) (goal_asms gl) in
1678 (HASH_UNDISCH_TAC h THEN
1679 DISCH_THEN (fun t-> ASSUME_TAC(REWRITE_RULE (map snd asl2) t))) gl;;
1681 (* working with numbered assumptions,
1682 Follow HOL Light's reverse numbering convention on assumptions. *)
1685 hash_of_term (el i (map (concl o snd) (List.rev (goal_asms gl))));;
1687 let use_el i ttac gl =
1688 let h = el_hash i gl in
1689 (HASH_UNDISCH_TAC h THEN (DISCH_THEN ttac)) gl;;
1693 (* Using hash numbers for tactics *)
1696 let label_of_hash gl (h:int) =
1697 let one_label h (s,tm) =
1698 if (h = hash_of_term (concl tm)) then
1699 let s1 = String.sub s 2 (String.length s - 2) in
1701 else failwith "label_of_hash" in
1702 tryfind (one_label h) (goal_asms gl);;
1704 let HASHIFY m h w = m (label_of_hash w h) w;;
1705 let UNDH = HASHIFY UND;;
1706 let REWRH = HASHIFY REWR;;
1707 let KILLH = HASHIFY KILL;;
1708 let COPYH = HASHIFY COPY;;
1709 let HASHIFY1 m h tm w = m (label_of_hash w h) tm w;;
1710 let USEH = HASHIFY1 USE;;
1711 let LEFTH = HASHIFY1 LEFT;;
1712 let RIGHTH = HASHIFY1 RIGHT;;
1713 let TSPECH tm h w = TSPEC tm (label_of_hash w h) w ;;