(* ------------------------------------------------------------------ *)
(* MORE RECENT ADDITIONS *)
(* ------------------------------------------------------------------ *)



(* abbrev_type copied from definitions_group.ml *)

let pthm = 
prove_by_refinement( `(\ (x:A) .T) (@(x:A). T)`,
[BETA_TAC]);;
let abbrev_type ty s = let (a,b) = new_basic_type_definition s ("mk_"^s,"dest_"^s) (INST_TYPE [ty,`:A`] pthm) in let abst t = list_mk_forall ((frees t), t) in let a' = abst (concl a) in let b' = abst (rhs (concl b)) in ( prove_by_refinement(a',[REWRITE_TAC[a]]), prove_by_refinement(b',[REWRITE_TAC[GSYM b]]));; (* ------------------------------------------------------------------ *) (* KILL IN *) (* ------------------------------------------------------------------ *) let un = REWRITE_RULE[IN];; (* ------------------------------------------------------------------ *) let SUBCONJ_TAC = MATCH_MP_TAC (TAUT `A /\ (A ==>B) ==> (A /\ B)`) THEN CONJ_TAC;; let PROOF_BY_CONTR_TAC = MATCH_MP_TAC (TAUT `(~A ==> F) ==> A`) THEN DISCH_TAC;; (* ------------------------------------------------------------------ *) (* some general tactics *) (* ------------------------------------------------------------------ *) (* before adding assumption to hypothesis list, cleanse it of unnecessary conditions *) let CLEAN_ASSUME_TAC th = MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_TAC;; let CLEAN_THEN th ttac = MP_TAC th THEN ASM_REWRITE_TAC[] THEN DISCH_THEN ttac;; (* looks for a hypothesis by matching a subterm *) let (UNDISCH_FIND_TAC: term -> tactic) = fun tm (asl,w) -> let p = can (term_match[] tm) in try let sthm,_ = remove (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in UNDISCH_TAC (concl (snd sthm)) (asl,w) with Failure _ -> failwith "UNDISCH_FIND_TAC";; let (UNDISCH_FIND_THEN: term -> thm_tactic -> tactic) = fun tm ttac (asl,w) -> let p = can (term_match[] tm) in try let sthm,_ = remove (fun (_,asm) -> can (find_term p) (concl ( asm))) asl in UNDISCH_THEN (concl (snd sthm)) ttac (asl,w) with Failure _ -> failwith "UNDISCH_FIND_TAC";; (* ------------------------------------------------------------------ *) (* NAME_CONFLICT_TAC : eliminate name conflicts in a term *) (* ------------------------------------------------------------------ *) let relabel_bound_conv tm = let rec vars_and_constants tm acc = match tm with | Var _ -> tm::acc | Const _ -> tm::acc | Comb(a,b) -> vars_and_constants b (vars_and_constants a acc) | Abs(a,b) -> a::(vars_and_constants b acc) in let relabel_bound tm = match tm with | Abs(x,t) -> let avoids = filter ((!=) x) (vars_and_constants tm []) in let x' = mk_primed_var avoids x in if (x=x') then failwith "relabel_bound" else (alpha x' tm) | _ -> failwith "relabel_bound" in DEPTH_CONV (fun t -> ALPHA t (relabel_bound t)) tm;; (* example *) let _ = let bad_term = mk_abs (`x:bool`,`(x:num)+1=2`) in relabel_bound_conv bad_term;; let NAME_CONFLICT_CONV = relabel_bound_conv;; let NAME_CONFLICT_TAC = CONV_TAC (relabel_bound_conv);; (* renames given bound variables *) let alpha_conv env tm = ALPHA tm (deep_alpha env tm);; (* replaces given alpha-equivalent terms with- the term itself *) let unify_alpha_tac = SUBST_ALL_TAC o REFL;; let rec get_abs tm acc = match tm with Abs(u,v) -> get_abs v (tm::acc) |Comb(u,v) -> get_abs u (get_abs v acc) |_ -> acc;; (* for purposes such as sorting, it helps if ALL ALPHA-equiv abstractions are replaced by equal abstractions *) let (alpha_tac:tactic) = fun (asl,w' ) -> EVERY (map unify_alpha_tac (get_abs w' [])) (asl,w');; (* ------------------------------------------------------------------ *) (* SELECT ELIMINATION. SELECT_TAC should work whenever there is a single predicate selected. Something more sophisticated might be needed when there is (@)A and (@)B in the same formula. Useful for proving statements such as `1 + (@x. (x=3)) = 4` *) (* ------------------------------------------------------------------ *) (* spec form of SELECT_AX *) let select_thm select_fn select_exist = BETA_RULE (ISPECL [select_fn;select_exist] SELECT_AX);; (* example *) select_thm `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`;;
let SELECT_EXIST = 
prove_by_refinement( `!(P:A->bool) Q. (?y. P y) /\ (!t. (P t ==> Q t)) ==> Q ((@) P)`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; UNDISCH_FIND_TAC `(?)`; DISCH_THEN CHOOSE_TAC; ASSUME_TAC (ISPECL[`P:(A->bool)`;`y:A`] SELECT_AX); ASM_MESON_TAC[]; ]);;
(* }}} *)
let SELECT_THM = 
prove_by_refinement( `!(P:A->bool) Q. (((?y. P y) ==> (!t. (P t ==> Q t))) /\ ((~(?y. P y)) ==> (!t. Q t))) ==> Q ((@) P)`,
(* {{{ proof *) [ MESON_TAC[SELECT_EXIST]; ]);;
(* }}} *) let SELECT_TAC = (* explicitly pull apart the clause Q((@) P), because MATCH_MP_TAC isn't powerful enough to do this by itself. *)
let unbeta = 
prove( `!(P:A->bool) (Q:A->bool). (Q ((@) P)) <=> (\t. Q t) ((@) P)`,
MESON_TAC[]) in let unbeta_tac = CONV_TAC (HIGHER_REWRITE_CONV[unbeta] true) in unbeta_tac THEN (MATCH_MP_TAC SELECT_THM) THEN BETA_TAC THEN CONJ_TAC THENL[ (DISCH_THEN (fun t-> ALL_TAC)) THEN GEN_TAC; DISCH_TAC THEN GEN_TAC];;
(* EXAMPLE: # g `(R:A->bool) ((@) S)`;; val it : Core.goalstack = 1 subgoal (1 total) `R ((@) S)` # e SELECT_TAC ;; val it : Core.goalstack = 2 subgoals (2 total) 0 [`~(?y. S y)`] `R t` `S t ==> R t` *) (* ------------------------------------------------------------------ *) (* TYPE_THEN and TYPEL_THEN calculate the types of the terms supplied in a proof, avoiding the hassle of working them out by hand. It locates the terms among the free variables in the goal. Ambiguious if a free variables have name conflicts. Now TYPE_THEN handles general terms. *) (* ------------------------------------------------------------------ *) let rec type_set: (string*term) list -> (term list*term) -> (term list*term)= fun typinfo (acclist,utm) -> match acclist with | [] -> (acclist,utm) | (Var(s,_) as a)::rest -> let a' = (assocd s typinfo a) in if (a = a') then type_set typinfo (rest,utm) else let inst = instantiate (term_match [] a a') in type_set typinfo ((map inst rest),inst utm) | _ -> failwith "type_set: variable expected" ;; let has_stv t = let typ = (type_vars_in_term t) in can (find (fun ty -> (is_vartype ty) && ((dest_vartype ty).[0] = '?'))) typ;; let TYPE_THEN: term -> (term -> tactic) -> tactic = fun t (tac:term->tactic) (asl,w) -> let avoids = itlist (union o frees o concl o snd) asl (frees w) in let strip = fun t-> (match t with |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in let typinfo = map strip avoids in let t' = (snd (type_set typinfo ((frees t),t))) in (warn ((has_stv t')) "TYPE_THEN: unresolved type variables"); tac t' (asl,w);; (* this version must take variables *) let TYPEL_THEN: term list -> (term list -> tactic) -> tactic = fun t (tac:term list->tactic) (asl,w) -> let avoids = itlist (union o frees o concl o snd) asl (frees w) in let strip = fun t-> (match t with |Var(s,_) -> (s,t) | _ -> failwith "TYPE_THEN" ) in let typinfo = map strip avoids in let t' = map (fun u -> snd (type_set typinfo ((frees u),u))) t in (warn ((can (find has_stv) t')) "TYPEL_THEN: unresolved type vars"); tac t' (asl,w);; (* trivial example *)
let _ = 
prove_by_refinement(`!y. y:num = y`,
[ GEN_TAC; TYPE_THEN `y:A` (fun t -> ASSUME_TAC(ISPEC t (TAUT `!x:B. x=x`))); UNDISCH_TAC `y:num = y`; (* evidence that `y:A` was retyped as `y:num` *) MESON_TAC[]; ]);;
(* ------------------------------------------------------------------ *) (* SAVE the goalstate, and retrieve later *) (* ------------------------------------------------------------------ *) let (save_goal,get_goal) = let goal_buffer = ref [] in let save_goal s = goal_buffer := (s,!current_goalstack )::!goal_buffer in let get_goal (s:string) = (current_goalstack:= assoc s !goal_buffer) in (save_goal,get_goal);; (* ------------------------------------------------------------------ *) (* ordered rewrites with general ord function . This allows rewrites with an arbitrary condition -- adapted from simp.ml *) (* ------------------------------------------------------------------ *) let net_of_thm_ord ord rep force th = let t = concl th in let lconsts = freesl (hyp th) in let matchable = can o term_match lconsts in try let l,r = dest_eq t in if rep & free_in l r then let th' = EQT_INTRO th in enter lconsts (l,(1,REWR_CONV th')) else if rep & matchable l r & matchable r l then enter lconsts (l,(1,ORDERED_REWR_CONV ord th)) else if force then enter lconsts (l,(1,ORDERED_REWR_CONV ord th)) else enter lconsts (l,(1,REWR_CONV th)) with Failure _ -> let l,r = dest_eq(rand t) in if rep & free_in l r then let tm = lhand t in let th' = DISCH tm (EQT_INTRO(UNDISCH th)) in enter lconsts (l,(3,IMP_REWR_CONV th')) else if rep & matchable l r & matchable r l then enter lconsts (l,(3,ORDERED_IMP_REWR_CONV ord th)) else enter lconsts(l,(3,IMP_REWR_CONV th));; let GENERAL_REWRITE_ORD_CONV ord rep force (cnvl:conv->conv) (builtin_net:gconv net) thl = let thl_canon = itlist (mk_rewrites false) thl [] in let final_net = itlist (net_of_thm_ord ord rep force ) thl_canon builtin_net in cnvl (REWRITES_CONV final_net);; let GEN_REWRITE_ORD_CONV ord force (cnvl:conv->conv) thl = GENERAL_REWRITE_ORD_CONV ord false force cnvl empty_net thl;; let PURE_REWRITE_ORD_CONV ord force thl = GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV empty_net thl;; let REWRITE_ORD_CONV ord force thl = GENERAL_REWRITE_ORD_CONV ord true force TOP_DEPTH_CONV (basic_net()) thl;; let PURE_ONCE_REWRITE_ORD_CONV ord force thl = GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV empty_net thl;; let ONCE_REWRITE_ORD_CONV ord force thl = GENERAL_REWRITE_ORD_CONV ord false force ONCE_DEPTH_CONV (basic_net()) thl;; let REWRITE_ORD_TAC ord force thl = CONV_TAC(REWRITE_ORD_CONV ord force thl);; (* ------------------------------------------------------------------ *) (* poly reduction *) (* ------------------------------------------------------------------ *) (* move vars leftward *) (* if ord old_lhs new_rhs THEN swap *) let new_factor_order t1 t2 = try let t1v = fst(dest_binop `( *. )` t1) in let t2v = fst(dest_binop `( *. )` t2) in if (is_var t1v) & (is_var t2v) then term_order t1v t2v else if (is_var t2v) then true else false with Failure _ -> false ;; (* false if it contains a variable or abstraction. *) let rec is_arith_const tm = if is_var tm then false else if is_abs tm then false else if is_comb tm then let (a,b) = (dest_comb tm) in is_arith_const (a) & is_arith_const (b) else true;; (* const leftward *) let new_factor_order2 t1 t2 = try let t1v = fst(dest_binop `( *. )` t1) in let t2v = fst(dest_binop `( *. )` t2) in if (is_var t1v) & (is_var t2v) then term_order t1v t2v else if (is_arith_const t2v) then true else false with Failure _ -> false ;; let rec mon_sz tm = if is_var tm then Int (Hashtbl.hash tm) else try let (a,b) = dest_binop `( *. )` tm in (mon_sz a) */ (mon_sz b) with Failure _ -> Int 1;; let rec new_summand_order t1 t2 = try let t1v = fst(dest_binop `( +. )` t1) in let t2v = fst(dest_binop `( +. )` t2) in (mon_sz t2v >/ mon_sz t1v) with Failure _ -> false ;; let rec new_distrib_order t1 t2 = try let t2v = fst(dest_binop `( *. )` t2) in if (is_arith_const t2v) then true else false with Failure _ -> try let t2' = fst(dest_binop `( +. )` t2) in new_distrib_order t1 t2' with Failure _ -> false ;; let real_poly_conv = (* same side *) ONCE_REWRITE_CONV [GSYM REAL_SUB_0] THENC (* expand ALL *) REWRITE_CONV[real_div;REAL_RDISTRIB;REAL_SUB_RDISTRIB; pow; GSYM REAL_MUL_ASSOC;GSYM REAL_ADD_ASSOC; REAL_ARITH `(x -. (--y) = x + y) /\ (x - y = x + (-- y)) /\ (--(x + y) = --x + (--y)) /\ (--(x - y) = --x + y)`; REAL_ARITH `(x*.(-- y) = -- (x*. y)) /\ (--. (--. x) = x) /\ ((--. x)*.y = --.(x*.y))`; REAL_SUB_LDISTRIB;REAL_LDISTRIB] THENC (* move constants rightward on monomials *) REWRITE_ORD_CONV new_factor_order false [REAL_MUL_AC;] THENC GEN_REWRITE_CONV ONCE_DEPTH_CONV [REAL_ARITH `-- x = (x*(-- &.1))`] THENC REWRITE_CONV[GSYM REAL_MUL_ASSOC] THENC REAL_RAT_REDUCE_CONV THENC (* collect like monomials *) REWRITE_ORD_CONV new_summand_order false [REAL_ADD_AC;] THENC (* move constants leftward AND collect them together *) REWRITE_ORD_CONV new_factor_order2 false [REAL_MUL_AC;] THENC REWRITE_ORD_CONV new_distrib_order true [ REAL_ARITH `(a*b +. d*b = (a+d)*b) /\ (a*b + b = (a+ &.1)*b ) /\ ( b + a*b = (a+ &.1)*b) /\ (a*b +. d*b +e = (a+d)*b + e) /\ (a*b + b + e= (a+. &.1)* b +e ) /\ ( b + a*b + e = (a + &.1)*b +e) `;] THENC REAL_RAT_REDUCE_CONV THENC REWRITE_CONV[REAL_ARITH `(&.0 * x = &.0) /\ (x + &.0 = x) /\ (&.0 + x = x)`];; let real_poly_tac = CONV_TAC real_poly_conv;;
let test_real_poly_tac = 
prove_by_refinement( `!x y . (x + (&.2)*y)*(x- (&.2)*y) = (x*x -. (&.4)*y*y)`,
(* {{{ proof *) [ DISCH_ALL_TAC; real_poly_tac; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* REAL INEQUALITIES *) (* Take inequality certificate A + B1 + B2 +.... + P = C as a term. Prove it as an inequality. Reduce to an ineq (A < C) WITH side conditions 0 <= Bi, 0 < P. If (not strict), write as an ineq (A <= C) WITH side conditions 0 <= Bi. Expand each Bi (or P) that is a product U*V as 0 <= U /\ 0 <= V. To prevent expansion of Bi write (U*V) as (&0 + (U*V)). CALL as ineq_le_tac `A + B1 + B2 = C`; *) (* ------------------------------------------------------------------ *)
let strict_lemma = 
prove_by_refinement( `!A B C. (A+B = C) ==> ((&.0 <. B) ==> (A <. C) )`,
(* {{{ proof *) [ REAL_ARITH_TAC; ]);;
(* }}} *)
let weak_lemma = 
prove_by_refinement( `!A B C. (A+B = C) ==> ((&.0 <=. B) ==> (A <=. C))`,
(* {{{ proof *) [ REAL_ARITH_TAC; ]);;
(* }}} *)
let strip_lt_lemma = 
prove_by_refinement( `!B1 B2 C. ((&.0 <. (B1+B2)) ==> C) ==> ((&.0 <. B2) ==> ((&.0 <=. B1) ==> C))`,
(* {{{ proof *) [ ASM_MESON_TAC[REAL_LET_ADD]; ]);;
(* }}} *)
let strip_le_lemma = 
prove_by_refinement( `!B1 B2 C. ((&.0 <=. (B1+B2)) ==> C) ==> ((&.0 <=. B2) ==> ((&.0 <=. B1) ==> C))`,
(* {{{ proof *) [ ASM_MESON_TAC[REAL_LE_ADD]; ]);;
(* }}} *) let is_x_prod_le tm = try let hyp = fst(dest_binop `( ==> )` tm) in let arg = snd(dest_binop `( <=. ) ` hyp) in let fac = dest_binop `( *. )` arg in true with Failure _ -> false;; let switch_lemma_le_order t1 t2 = if (is_x_prod_le t1) & (is_x_prod_le t2) then term_order t1 t2 else if (is_x_prod_le t2) then true else false;; let is_x_prod_lt tm = try let hyp = fst(dest_binop `( ==> )` tm) in let arg = snd(dest_binop `( <. ) ` hyp) in let fac = dest_binop `( *. )` arg in true with Failure _ -> false;; let switch_lemma_lt_order t1 t2 = if (is_x_prod_lt t1) & (is_x_prod_lt t2) then term_order t1 t2 else if (is_x_prod_lt t2) then true else false;;
let switch_lemma_le = 
prove_by_refinement( `!A B C. ((&.0 <= A) ==> (&.0 <= B) ==> C) = ((&.0 <=. B) ==> (&.0 <= A) ==> C)`,
(* {{{ proof *) [ ASM_MESON_TAC[]; ]);;
(* }}} *)
let switch_lemma_let = 
prove_by_refinement( `!A B C. ((&.0 < A) ==> (&.0 <= B) ==> C) = ((&.0 <=. B) ==> (&.0 < A) ==> C)`,
(* {{{ proof *) [ ASM_MESON_TAC[]; ]);;
(* }}} *)
let switch_lemma_lt = 
prove_by_refinement( `!A B C. ((&.0 < A) ==> (&.0 < B) ==> C) = ((&.0 <. B) ==> (&.0 < A) ==> C)`,
(* {{{ proof *) [ ASM_MESON_TAC[]; ]);;
(* }}} *)
let expand_prod_lt = 
prove_by_refinement( `!B1 B2 C. (&.0 < B1*B2 ==> C) ==> ((&.0 <. B1) ==> (&.0 <. B2) ==> C)`,
(* {{{ proof *) [ ASM_MESON_TAC[REAL_LT_MUL ]; ]);;
(* }}} *)
let expand_prod_le = 
prove_by_refinement( `!B1 B2 C. (&.0 <= B1*B2 ==> C) ==> ((&.0 <=. B1) ==> (&.0 <=. B2) ==> C)`,
(* {{{ proof *) [ ASM_MESON_TAC[REAL_LE_MUL ]; ]);;
(* }}} *) let ineq_cert_gen_tac v cert = let DISCH_RULE f = DISCH_THEN (fun t-> MP_TAC (f t)) in TYPE_THEN cert (MP_TAC o (REWRITE_CONV[REAL_POW_2] THENC real_poly_conv)) THEN REWRITE_TAC[] THEN DISCH_RULE (MATCH_MP v) THEN DISCH_RULE (repeat (MATCH_MP strip_lt_lemma)) THEN DISCH_RULE (repeat (MATCH_MP strip_le_lemma)) THEN DISCH_RULE (repeat (MATCH_MP expand_prod_lt o (CONV_RULE (REWRITE_ORD_CONV switch_lemma_lt_order true[switch_lemma_lt])))) THEN DISCH_RULE (repeat (MATCH_MP expand_prod_le o (CONV_RULE (REWRITE_ORD_CONV switch_lemma_le_order true [switch_lemma_le])) o (REWRITE_RULE[switch_lemma_let]))) THEN DISCH_RULE (repeat (MATCH_MP (TAUT `(A ==> B==>C) ==> (A /\ B ==> C)`))) THEN REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_SIMP_TAC[REAL_LE_POW_2; REAL_ARITH `(&.0 < x ==> &.0 <= x) /\ (&.0 + x = x) /\ (a <= b ==> &.0 <= b - a) /\ (a < b ==> &.0 <= b - a) /\ (~(b < a) ==> &.0 <= b - a) /\ (~(b <= a) ==> &.0 <= b - a) /\ (a < b ==> &.0 < b - a) /\ (~(b <= a) ==> &.0 < b - a)`];; let ineq_lt_tac = ineq_cert_gen_tac strict_lemma;; let ineq_le_tac = ineq_cert_gen_tac weak_lemma;; (* test *)
let test_ineq_tac  = 
prove_by_refinement( `!x y z. (&.0 <= x*y) /\ (&.0 <. z) ==> (x*y) <. x*x + (&.3)*x*y + &.4 `,
(* {{{ proof *) [ DISCH_ALL_TAC; ineq_lt_tac `x * y + x pow 2 + &2 * (&.0 + x * y) + &2 * &2 = x * x + &3 * x * y + &4`; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* Move quantifier left. Use class.ml and theorems.ml to bubble quantifiers towards the head of an expression. It should move quantifiers past other quantifiers, past conjunctions, disjunctions, implications, etc. val quant_left_CONV : string -> term -> thm = <fun> Arguments: var_name:string -- The name of the variable that is to be shifted. It tends to return `T` when the conversion fails. Example: quant_left_CONV "a" `!b. ?a. a = b*4`;; val it : thm = |- (!b. ?a. a = b *| 4) <=> (?a. !b. a b = b *| 4) *) (* ------------------------------------------------------------------ *)
let tagb = new_definition `TAGB (x:bool) = x`;;
let is_quant tm = (is_forall tm) or (is_exists tm);; (*** JRH replaced Comb and Abs with abstract type constructors ***) let rec tag_quant var_name tm = if (is_forall tm && (fst (dest_var (fst (dest_forall tm))) = var_name)) then mk_comb (`TAGB`,tm) else if (is_exists tm && (fst (dest_var (fst (dest_exists tm))) = var_name)) then mk_comb (`TAGB`,tm) else match tm with | Comb (x,y) -> mk_comb(tag_quant var_name x,tag_quant var_name y) | Abs (x,y) -> mk_abs(x,tag_quant var_name y) | _ -> tm;; let quant_left_CONV = (* ~! -> ?~ *) let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
let NOT_FORALL_TAG = 
prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
REWRITE_TAC[tagb;NOT_FORALL_THM]) in
let SKOLEM_TAG =
  prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
     ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
 let SKOLEM_TAG2 =
   prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
         REWRITE_TAC[tagb;SKOLEM_THM]) in
 (* !1 !2 -> !2 !1 *)
 let SWAP_FORALL_TAG =
  prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
    REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
 let SWAP_EXISTS_THM = iprove
  `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
 (* ! /\ ! -> ! /\ *)
 let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
   (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\  Q) <=>
   (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
   (!x. P  /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let TRIV_OR_FORALL_TAG = prove
 (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_IMP_FORALL_TAG = prove
 (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let OR_EXISTS_THM = iprove
  `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
 let LEFT_OR_EXISTS_THM = iprove
 `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
 let RIGHT_OR_EXISTS_THM = iprove
 `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
 let LEFT_AND_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
 let RIGHT_AND_EXISTS_THM = iprove
 `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
 let TRIV_AND_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
 let LEFT_IMP_EXISTS_THM = iprove
 `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
 let TRIV_FORALL_IMP_THM = iprove
 `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
 let TRIV_EXISTS_IMP_THM = iprove
 `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
 let NOT_EXISTS_TAG = prove(
 `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 let LEFT_OR_FORALL_TAG = prove
 (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 let RIGHT_OR_FORALL_TAG = prove
 (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
  REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 let LEFT_IMP_FORALL_TAG = prove
 (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 let RIGHT_IMP_EXISTS_TAG = prove
 (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
  fun var_name tm ->
     REWRITE_RULE [tagb]
       (TOP_SWEEP_CONV
       (GEN_REWRITE_CONV I
         [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
          SWAP_FORALL_TAG;SWAP_EXISTS_THM;
          SWAP_EXISTS_THM;
          AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
          TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
          OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
          LEFT_AND_EXISTS_THM;
          RIGHT_AND_EXISTS_THM;
          TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
          TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
          LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
          RIGHT_IMP_EXISTS_TAG;
         ])
       (tag_quant var_name tm));;
(* same, but never pass a quantifier past another. No Skolem, etc. *) let quant_left_noswap_CONV = (* ~! -> ?~ *) let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
let NOT_FORALL_TAG = 
prove(`!P. ~(TAGB(!x. P x)) <=> (?x:A. ~(P x))`,
REWRITE_TAC[tagb;NOT_FORALL_THM]) in
let SKOLEM_TAG =
  prove(`!P. (?y. TAGB (!(x:A). P x ((y:A->B) x))) <=>
     ( (!(x:A). ?y. P x ((y:B))))`,REWRITE_TAC[tagb;SKOLEM_THM]) in
 let SKOLEM_TAG2 =
   prove(`!P. (!x:A. TAGB(?y:B. P x y)) <=> (?y. !x. P x (y x))`,
         REWRITE_TAC[tagb;SKOLEM_THM]) in
 (* !1 !2 -> !2 !1 *)
 let SWAP_FORALL_TAG =
  prove(`!P:A->B->bool. (!x. TAGB(! y. P x y)) <=> (!y x. P x y)`,
    REWRITE_TAC[SWAP_FORALL_THM;tagb]) in
 let SWAP_EXISTS_THM = iprove
  `!P:A->B->bool. (?x. TAGB (?y. P x y)) <=> (?y x. P x y)` in
 (* ! /\ ! -> ! /\ *)
 let AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\ TAGB (!x. Q x) <=>
   (!x. P x /\ Q x))`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let LEFT_AND_FORALL_TAG = prove(`!P Q. (TAGB (!x. P x) /\  Q) <=>
   (!x. P x /\ Q )`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_AND_FORALL_TAG = prove(`!P Q. P /\ TAGB (!x. Q x) <=>
   (!x. P  /\ Q x)`,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let TRIV_OR_FORALL_TAG = prove
 (`!P Q. TAGB (!x:A. P) \/ TAGB (!x:A. Q) <=> (!x:A. P \/ Q)`,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_IMP_FORALL_TAG = prove
 (`!P Q. (P ==> TAGB (!x:A. Q x)) <=> (!x. P ==> Q x)`,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let OR_EXISTS_THM = iprove
  `!P Q. TAGB (?x. P x) \/ TAGB (?x. Q x) <=> (?x:A. P x \/ Q x)` in
 let LEFT_OR_EXISTS_THM = iprove
 `!P Q. TAGB (?x. P x) \/ Q <=> (?x:A. P x \/ Q)` in
 let RIGHT_OR_EXISTS_THM = iprove
 `!P Q. P \/ TAGB (?x. Q x) <=> (?x:A. P \/ Q x)` in
 let LEFT_AND_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P x) /\ Q <=> (?x:A. P x /\ Q)` in
 let RIGHT_AND_EXISTS_THM = iprove
 `!P Q. P /\ TAGB (?x:A. Q x) <=> (?x:A. P /\ Q x)` in
 let TRIV_AND_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P) /\ TAGB (?x:A. Q) <=> (?x:A. P /\ Q)` in
 let LEFT_IMP_EXISTS_THM = iprove
 `!P Q. (TAGB (?x:A. P x) ==> Q) <=> (!x. P x ==> Q)` in
 let TRIV_FORALL_IMP_THM = iprove
 `!P Q. (TAGB (?x:A. P) ==> TAGB (!x:A. Q)) <=> (!x:A. P ==> Q) ` in
 let TRIV_EXISTS_IMP_THM = iprove
 `!P Q. (TAGB(!x:A. P) ==> TAGB (?x:A. Q)) <=> (?x:A. P ==> Q) ` in
 let NOT_EXISTS_TAG = prove(
 `!P. ~(TAGB(?x:A. P x)) <=> (!x. ~(P x))`,
 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 let LEFT_OR_FORALL_TAG = prove
 (`!P Q. TAGB(!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 let RIGHT_OR_FORALL_TAG = prove
 (`!P Q. P \/ TAGB(!x:A. Q x) <=> (!x. P \/ Q x)`,
  REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 let LEFT_IMP_FORALL_TAG = prove
 (`!P Q. (TAGB(!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 let RIGHT_IMP_EXISTS_TAG = prove
 (`!P Q. (P ==> TAGB(?x:A. Q x)) <=> (?x:A. P ==> Q x)`,
 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
  fun var_name tm ->
     REWRITE_RULE [tagb]
       (TOP_SWEEP_CONV
       (GEN_REWRITE_CONV I
         [NOT_FORALL_TAG; (* SKOLEM_TAG;SKOLEM_TAG2; *)
          (* SWAP_FORALL_TAG;SWAP_EXISTS_THM;
          SWAP_EXISTS_THM; *)
          AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
          TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
          OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
          LEFT_AND_EXISTS_THM;
          RIGHT_AND_EXISTS_THM;
          TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
          TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
          LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
          RIGHT_IMP_EXISTS_TAG;
         ])
       (tag_quant var_name tm));;
let quant_right_CONV = (* ~! -> ?~ *) let iprove f = prove(f,REWRITE_TAC[tagb] THEN ITAUT_TAC) in
let NOT_FORALL_TAG = 
prove(`!P. TAGB(?x:A. ~(P x)) <=> ~((!x. P x))`,
REWRITE_TAC[tagb;GSYM NOT_FORALL_THM]) in
let SKOLEM_TAG =
  prove(`!P. ( TAGB(!(x:A). ?y. P x ((y:B)))) <=>
   (?y.  (!(x:A). P x ((y:A->B) x)))`,
   REWRITE_TAC[tagb;GSYM SKOLEM_THM])
   in
 let SKOLEM_TAG2 =
   prove(`!P. TAGB(?y. !x. P x (y x)) <=> (!x:A. (?y:B. P x y))`,
         REWRITE_TAC[tagb;GSYM SKOLEM_THM]) in
 (* !1 !2 -> !2 !1.. *)
 let SWAP_FORALL_TAG =
  prove(`!P:A->B->bool.  TAGB(!y x. P x y) <=> (!x. (! y. P x y))`,
    REWRITE_TAC[GSYM SWAP_FORALL_THM;tagb]) in
 let SWAP_EXISTS_THM = iprove
  `!P:A->B->bool.  TAGB (?y x. P x y) <=> (?x. (?y. P x y))` in
 (* ! /\ ! -> ! /\ *)
 let AND_FORALL_TAG = iprove`!P Q. TAGB(!x. P x /\ Q x) <=>
   ((!x. P x) /\ (!x. Q x))` in
 let LEFT_AND_FORALL_TAG = prove(`!P Q.
   TAGB(!x. P x /\ Q ) <=> ((!x. P x) /\  Q)`,
   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_AND_FORALL_TAG = prove(`!P Q.
   TAGB(!x. P  /\ Q x) <=> P /\  (!x. Q x)`,
   REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let TRIV_OR_FORALL_TAG = prove
 (`!P Q.   TAGB(!x:A. P \/ Q) <=>(!x:A. P) \/  (!x:A. Q)`,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let RIGHT_IMP_FORALL_TAG = prove
 (`!P Q. TAGB (!x. P ==> Q x) <=> (P ==>  (!x:A. Q x)) `,
  REWRITE_TAC[tagb] THEN ITAUT_TAC) in
 let OR_EXISTS_THM = iprove
  `!P Q.  TAGB(?x:A. P x \/ Q x) <=> (?x. P x) \/ (?x. Q x) ` in
 let LEFT_OR_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P x \/ Q) <=>  (?x. P x) \/ Q ` in
 let RIGHT_OR_EXISTS_THM = iprove
 `!P Q.TAGB (?x:A. P \/ Q x) <=>  P \/ (?x. Q x)` in
 let LEFT_AND_EXISTS_THM = iprove
 `!P Q.TAGB (?x:A. P x /\ Q) <=>  (?x:A. P x) /\ Q` in
 let RIGHT_AND_EXISTS_THM = iprove
 `!P Q. TAGB (?x:A. P /\ Q x) <=>  P /\ (?x:A. Q x) ` in
 let TRIV_AND_EXISTS_THM = iprove
 `!P Q. TAGB(?x:A. P /\ Q) <=>  (?x:A. P) /\  (?x:A. Q) ` in (* *)
 let LEFT_IMP_EXISTS_THM = iprove
 `!P Q. TAGB(!x. P x ==> Q) <=> ( (?x:A. P x) ==> Q) ` in (* *)
 let TRIV_FORALL_IMP_THM = iprove
 `!P Q. TAGB(!x:A. P ==> Q)  <=> ( (?x:A. P) ==>  (!x:A. Q)) ` in
 let TRIV_EXISTS_IMP_THM = iprove
 `!P Q. TAGB(?x:A. P ==> Q)  <=> ((!x:A. P) ==>  (?x:A. Q)) ` in
 let NOT_EXISTS_TAG = prove(
 `!P. TAGB(!x. ~(P x)) <=> ~((?x:A. P x)) `,
 REWRITE_TAC[tagb;NOT_EXISTS_THM]) in
 let LEFT_OR_FORALL_TAG = prove
 (`!P Q. TAGB(!x. P x \/ Q) <=> (!x:A. P x) \/ Q `,
 REWRITE_TAC[tagb;LEFT_OR_FORALL_THM]) in
 let RIGHT_OR_FORALL_TAG = prove
 (`!P Q. TAGB(!x. P \/ Q x) <=> P \/ (!x:A. Q x) `,
  REWRITE_TAC[tagb;RIGHT_OR_FORALL_THM]) in
 let LEFT_IMP_FORALL_TAG = prove
 (`!P Q. TAGB(?x. P x ==> Q) <=> ((!x:A. P x) ==> Q) `,
 REWRITE_TAC[tagb;LEFT_IMP_FORALL_THM]) in
 let RIGHT_IMP_EXISTS_TAG = prove
 (`!P Q. TAGB(?x:A. P ==> Q x) <=> (P ==> (?x:A. Q x)) `,
 REWRITE_TAC[tagb;RIGHT_IMP_EXISTS_THM]) in
  fun var_name tm ->
     REWRITE_RULE [tagb]
       (TOP_SWEEP_CONV
       (GEN_REWRITE_CONV I
         [NOT_FORALL_TAG;SKOLEM_TAG;SKOLEM_TAG2;
          SWAP_FORALL_TAG;SWAP_EXISTS_THM;
          SWAP_EXISTS_THM;
          AND_FORALL_TAG;LEFT_AND_FORALL_TAG;RIGHT_AND_FORALL_TAG;
          TRIV_OR_FORALL_TAG;RIGHT_IMP_FORALL_TAG;
          OR_EXISTS_THM;LEFT_OR_EXISTS_THM;RIGHT_OR_EXISTS_THM;
          LEFT_AND_EXISTS_THM;
          RIGHT_AND_EXISTS_THM;
          TRIV_AND_EXISTS_THM;LEFT_IMP_EXISTS_THM;TRIV_FORALL_IMP_THM;
          TRIV_EXISTS_IMP_THM;NOT_EXISTS_TAG;
          LEFT_OR_FORALL_TAG;RIGHT_OR_FORALL_TAG;LEFT_IMP_FORALL_TAG;
          RIGHT_IMP_EXISTS_TAG;
         ])
       (tag_quant var_name tm));;
(* ------------------------------------------------------------------ *) (* Dropping Superfluous Quantifiers . Example: ?u. (u = t) /\ ... We can eliminate the u. *) (* ------------------------------------------------------------------ *)
let mark_term = new_definition `mark_term (u:A) = u`;;
(*** JRH replaced Comb and Abs with explicit constructors ***) let rec markq qname tm = match tm with Var (a,b) -> if (a=qname) then mk_icomb (`mark_term:A->A`,tm) else tm |Const(_,_) -> tm |Comb(s,b) -> mk_comb(markq qname s,markq qname b) |Abs (x,t) -> mk_abs(x,markq qname t);; let rec getquants tm = if (is_forall tm) then (fst (dest_var (fst (dest_forall tm)))):: (getquants (snd (dest_forall tm))) else if (is_exists tm) then (fst (dest_var (fst (dest_exists tm)))):: (getquants (snd (dest_exists tm))) else match tm with Comb(s,b) -> (getquants s) @ (getquants b) | Abs (x,t) -> (getquants t) | _ -> [];; (* can loop if there are TWO *) let rewrite_conjs = [ prove_by_refinement (`!A B C. (A /\ B) /\ C <=> A /\ B /\ C`,[REWRITE_TAC[CONJ_ACI]]); prove_by_refinement (`!u. (mark_term (u:A) = mark_term u) <=> T`,[MESON_TAC[]]); prove_by_refinement (`!u t. (t = mark_term (u:A)) <=> (mark_term u = t)`,[MESON_TAC[]]); prove_by_refinement (`!u a b. (mark_term (u:A) = a) /\ (mark_term u = b) <=> (mark_term u = a) /\ (a = b)`,[MESON_TAC[]]); 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[]]); prove_by_refinement (`!u t A C. A /\ (mark_term (u:A) = t) /\ C <=> (mark_term u = t) /\ A /\ C`,[MESON_TAC[]]); prove_by_refinement (`!A u t. A /\ (mark_term (u:A) = t) <=> (mark_term u = t) /\ A `,[MESON_TAC[]]); prove_by_refinement (`!u t C D. (((mark_term (u:A) = t) /\ C) ==> D) <=> ((mark_term (u:A) = t) ==> C ==> D)`,[MESON_TAC[]]); prove_by_refinement (`!A u t B. (A ==> (mark_term (u:A) = t) ==> B) <=> ((mark_term (u:A) = t) ==> A ==> B)`,[MESON_TAC[]]); ];; let higher_conjs = [ prove_by_refinement (`!C u t. ((mark_term u = t) ==> C (mark_term u)) <=> ((mark_term u = t) ==> C (t:A))`,[MESON_TAC[mark_term]]); prove_by_refinement (`!C u t. ((mark_term u = t) /\ C (mark_term u)) <=> ((mark_term u = t) /\ C (t:A))`,[MESON_TAC[mark_term]]); ];; let dropq_conv = let drop_exist = REWRITE_CONV [prove_by_refinement (`!t. ?(u:A). (u = t)`,[MESON_TAC[]])] in fun qname tm -> let quanlist = getquants tm in let quantleft_CONV = EVERY_CONV (map (REPEATC o quant_left_noswap_CONV) quanlist) in let qname_conv tm = prove(mk_eq(tm,markq qname tm), REWRITE_TAC[mark_term]) in let conj_conv = REWRITE_CONV rewrite_conjs in let quantright_CONV = (REPEATC (quant_right_CONV qname)) in let drop_mark_CONV = REWRITE_CONV [mark_term] in (quantleft_CONV THENC qname_conv THENC conj_conv THENC (ONCE_REWRITE_CONV higher_conjs) THENC drop_mark_CONV THENC quantright_CONV THENC drop_exist ) tm ;; (* Examples : *) dropq_conv "u" `!P Q R . (?(u:B). (?(x:A). (u = P x) /\ (Q x)) /\ (R u))`;; dropq_conv "t" `!P Q R. (!(t:B). (?(x:A). P x /\ (t = Q x)) ==> R t)`;; dropq_conv "u" `?u v. ((t * (a + &1) + (&1 - t) *a = u) /\ (t * (b + &0) + (&1 - t) * b = v)) /\ a < u /\ u < r /\ (v = b)`;; (* ------------------------------------------------------------------ *) (* SOME GENERAL TACTICS FOR THE ASSUMPTION LIST *) (* ------------------------------------------------------------------ *) let (%) i = HYP (string_of_int i);; let WITH i rule = (H_VAL (rule) (HYP (string_of_int i))) ;; let (UND:int -> tactic) = fun i (asl,w) -> let name = "Z-"^(string_of_int i) in try let thm= assoc name asl in let tm = concl (thm) in let (_,asl') = partition (fun t-> ((=) name (fst t))) asl in null_meta,[asl',mk_imp(tm,w)], fun i [th] -> MP th (INSTANTIATE_ALL i thm) with Failure _ -> failwith "UND";; let KILL i = (UND i) THEN (DISCH_THEN (fun t -> ALL_TAC));; let USE i rule = (WITH i rule) THEN (KILL i);; let CHO i = (UND i) THEN (DISCH_THEN CHOOSE_TAC);; let X_CHO i t = (UND i) THEN (DISCH_THEN (X_CHOOSE_TAC t));; let AND i = (UND i) THEN (DISCH_THEN (fun t-> (ASSUME_TAC (CONJUNCT1 t) THEN (ASSUME_TAC (CONJUNCT2 t)))));; let JOIN i j = (H_VAL2 CONJ ((%)i) ((%)j)) THEN (KILL i) THEN (KILL j);; let COPY i = WITH i I;; let REP n tac = EVERY (replicate tac n);; let REWR i = (UND i) THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC;; let LEFT i t = (USE i (CONV_RULE (quant_left_CONV t)));; let RIGHT i t = (USE i (CONV_RULE (quant_right_CONV t)));; let LEFT_TAC t = ((CONV_TAC (quant_left_CONV t)));; let RIGHT_TAC t = ( (CONV_TAC (quant_right_CONV t)));; let INR = REWRITE_RULE[IN];; (* let rec REP n tac = if (n<=0) then ALL_TAC else (tac THEN (REP (n-1) tac));; (* doesn't seem to work? *) let COPY i = (UNDISCH_WITH i) THEN (DISCH_THEN (fun t->ALL_TAC));; MANIPULATING ASSUMPTIONS. (MAKE 0= GOAL) COPY: int -> tactic Make a copy in adjacent slot. EXPAND: int -> tactic. conjunction -> two separate. exists/goal-forall -> choose. goal-if-then -> discharge EXPAND_TERM: int -> term -> tactic. constant -> expand definition or other rewrites associated. ADD: term -> tactic. SIMPLIFY: int -> tactic. Apply simplification rules. *) let CONTRAPOSITIVE_TAC = MATCH_MP_TAC (TAUT `(~q ==> ~p) ==> (p ==> q)`) THEN REWRITE_TAC[];; let REWRT_TAC = (fun t-> REWRITE_TAC[t]);; let (REDUCE_CONV,REDUCE_TAC) = let list = [ (* reals *) REAL_NEG_GE0; REAL_HALF_DOUBLE; REAL_SUB_REFL ; REAL_NEG_NEG; REAL_LE; LE_0; REAL_ADD_LINV;REAL_ADD_RINV; REAL_NEG_0; REAL_NEG_LE0; REAL_NEG_GE0; REAL_LE_NEGL; REAL_LE_NEGR; REAL_LE_NEG; REAL_NEG_EQ_0; REAL_SUB_RNEG; REAL_ARITH `!(x:real). (--x = x) <=> (x = &.0)`; REAL_ARITH `!(a:real) b. (a - b + b) = a`; REAL_ADD_LID; REAL_ADD_RID ; REAL_INV_0; REAL_OF_NUM_EQ; REAL_OF_NUM_LE; REAL_OF_NUM_LT; REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_POS; REAL_MUL_RZERO; REAL_MUL_LZERO; REAL_LE_01; REAL_SUB_RZERO; REAL_LE_SQUARE; REAL_MUL_RID; REAL_MUL_LID; REAL_ABS_ZERO; REAL_ABS_NUM; REAL_ABS_1; REAL_ABS_NEG; REAL_ABS_POS; ABS_ZERO; ABS_ABS; REAL_NEG_LT0; REAL_NEG_GT0; REAL_LT_NEG; REAL_NEG_MUL2; REAL_OF_NUM_POW; REAL_LT_INV_EQ; REAL_POW_1; REAL_INV2; prove (`(--. (&.n) < (&.m)) <=> (&.0 < (&.n) + (&.m))`,REAL_ARITH_TAC); prove (`(--. (&.n) <= (&.m)) <=> (&.0 <= (&.n) + (&.m))`,REAL_ARITH_TAC); prove (`(--. (&.n) = (&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC); prove (`((&.n) < --.(&.m)) <=> ((&.n) + (&.m) <. (&.0))`,REAL_ARITH_TAC); prove (`((&.n) <= --.(&.m)) <=> ((&.n) + (&.m) <=. (&.0))`,REAL_ARITH_TAC); prove (`((&.n) = --.(&.m)) <=> ((&.n) + (&.m) = (&.0))`,REAL_ARITH_TAC); prove (`((&.n) < --.(&.m) + &.r) <=> ((&.n) + (&.m) < (&.r))`,REAL_ARITH_TAC); prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC); prove (`(--(&.n) < --.(&.m) + &.r) <=> ( (&.m) < &.n + (&.r))`,REAL_ARITH_TAC); prove (`(--. x = --. y) <=> (x = y)`,REAL_ARITH_TAC); prove (`((--. (&.1))* x < --. y <=> y < x)`,REAL_ARITH_TAC ); prove (`((--. (&.1))* x <= --. y <=> y <= x)`,REAL_ARITH_TAC ); (* num *) EXP_1; EXP_LT_0; ADD_0; ARITH_RULE `0+| m = m`; ADD_EQ_0; prove (`(0 = m +|n) <=> (m = 0)/\ (n=0)`,MESON_TAC[ADD_EQ_0]); EQ_ADD_LCANCEL_0; EQ_ADD_RCANCEL_0; LT_ADD; LT_ADDR; ARITH_RULE `(0 = j -| i) <=> (j <=| i)`; ARITH_RULE `(j -| i = 0) <=> (j <=| i)`; ARITH_RULE `0 -| i = 0`; ARITH_RULE `(i<=| j) /\ (j <=| i) <=> (i = j)`; ARITH_RULE `0 <| 1`; (* SUC *) NOT_SUC; SUC_INJ; PRE; ADD_CLAUSES; MULT; MULT_CLAUSES; LE; LT; ARITH_RULE `SUC b -| 1 = b`; ARITH_RULE `SUC b -| b = 1`; prove(`&.(SUC x) - &.x = &.1`, REWRITE_TAC [REAL_ARITH `(a -. b=c) <=> (a = b+.c)`; REAL_OF_NUM_ADD;REAL_OF_NUM_EQ] THEN ARITH_TAC); (* (o) *) o_DEF; (* I *) I_THM; I_O_ID; (* pow *) REAL_POW_1; REAL_POW_ONE; (* INT *) INT_ADD_LINV; INT_ADD_RINV; INT_ADD_SUB2; INT_EQ_NEG2; INT_LE_NEG; INT_LE_NEGL; INT_LE_NEGR; INT_LT_NEG; INT_LT_NEG2; INT_NEGNEG; INT_NEG_0; INT_NEG_EQ_0; INT_NEG_GE0; INT_NEG_GT0; INT_NEG_LE0; INT_NEG_LT0; GSYM INT_NEG_MINUS1; INT_NEG_MUL2; INT_NEG_NEG; (* sets *) ] in (REWRITE_CONV list,REWRITE_TAC list);; (* prove by squaring *)
let REAL_POW_2_LE = 
prove_by_refinement( `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <=. y pow 2) ==> (x <=. y)`,
(* {{{ proof *) [ DISCH_ALL_TAC; MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LE); ASM_REWRITE_TAC[]; ASM_SIMP_TAC[REAL_POW_LE]; ASM_SIMP_TAC[POW_2_SQRT]; ]);;
(* }}} *) (* prove by squaring *)
let REAL_POW_2_LT = 
prove_by_refinement( `!x y. (&.0 <= x) /\ (&.0 <= y) /\ (x pow 2 <. y pow 2) ==> (x <. y)`,
(* {{{ proof *) [ DISCH_ALL_TAC; MP_TAC (SPECL[` (x:real) pow 2`;`(y:real)pow 2`] SQRT_MONO_LT); ASM_REWRITE_TAC[]; ASM_SIMP_TAC[REAL_POW_LE]; ASM_SIMP_TAC[POW_2_SQRT]; ]);;
(* }}} *) let SQUARE_TAC = FIRST[ MATCH_MP_TAC REAL_LE_LSQRT; MATCH_MP_TAC REAL_POW_2_LT; MATCH_MP_TAC REAL_POW_2_LE ] THEN REWRITE_TAC[];; (****) let SPEC2_TAC t = SPEC_TAC (t,t);; let IN_ELIM i = (USE i (REWRITE_RULE[IN]));; let rec range i n = if (n>0) then (i::(range (i+1) (n-1))) else [];; (* in elimination *) let (IN_OUT_TAC: tactic) = fun (asl,g) -> (REWRITE_TAC [IN] THEN (EVERY (map (IN_ELIM) (range 0 (length asl))))) (asl,g);; let (IWRITE_TAC : thm list -> tactic) = fun thlist -> REWRITE_TAC (map INR thlist);; let (IWRITE_RULE : thm list -> thm -> thm) = fun thlist -> REWRITE_RULE (map INR thlist);; let IMATCH_MP imp ant = MATCH_MP (INR imp) (INR ant);; let IMATCH_MP_TAC imp = MATCH_MP_TAC (INR imp);; let GBETA_TAC = (CONV_TAC (TOP_DEPTH_CONV GEN_BETA_CONV));; let GBETA_RULE = (CONV_RULE (TOP_DEPTH_CONV GEN_BETA_CONV));; (* breaks antecedent into multiple cases *) let REP_CASES_TAC = REPEAT (DISCH_THEN (REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC));; let TSPEC t i = TYPE_THEN t (USE i o SPEC);; let IMP_REAL t i = (USE i (MATCH_MP (REAL_ARITH t)));; (* goes from f = g to fz = gz *) let TAPP z i = TYPE_THEN z (fun u -> (USE i(fun t -> AP_THM t u)));; (* ONE NEW TACTIC -- DOESN'T WORK!! DON'T USE.... let CONCL_TAC t = let co = snd (dest_imp (concl t)) in SUBGOAL_TAC co THEN (TRY (IMATCH_MP_TAC t));; *) (* subgoal the antecedent of a THM, in order to USE the conclusion *) let ANT_TAC t = let (ant,co) = (dest_imp (concl t)) in SUBGOAL_TAC ant THENL [ALL_TAC;DISCH_THEN (fun u-> MP_TAC (MATCH_MP t u))];; let TH_INTRO_TAC tl th = TYPEL_THEN tl (fun t-> ANT_TAC (ISPECL t th));; let THM_INTRO_TAC tl th = TYPEL_THEN tl (fun t-> let s = ISPECL t th in if is_imp (concl s) then ANT_TAC s else ASSUME_TAC s);; let (DISCH_THEN_FULL_REWRITE:tactic) = DISCH_THEN (fun t-> REWRITE_TAC[t] THEN (RULE_ASSUM_TAC (REWRITE_RULE[t])));; let FULL_REWRITE_TAC t = (REWRITE_TAC t THEN (RULE_ASSUM_TAC (REWRITE_RULE t)));; (* ------------------------------------------------------------------ *) let BASIC_TAC = [ GEN_TAC; IMATCH_MP_TAC (TAUT ` (a ==> b ==> C) ==> ( a /\ b ==> C)`); DISCH_THEN (CHOOSE_THEN MP_TAC); FIRST_ASSUM (fun t-> UNDISCH_TAC (concl t) THEN (DISCH_THEN CHOOSE_TAC)); FIRST_ASSUM (fun t -> (if (length (CONJUNCTS t) < 2) then failwith "BASIC_TAC" else UNDISCH_TAC (concl t))); DISCH_TAC; ];; let REP_BASIC_TAC = REPEAT (CHANGED_TAC (FIRST BASIC_TAC));; (* ------------------------------------------------------------------ *) let USE_FIRST rule = FIRST_ASSUM (fun t -> (UNDISCH_TAC (concl t) THEN (DISCH_THEN (ASSUME_TAC o rule))));; let WITH_FIRST rule = FIRST_ASSUM (fun t -> ASSUME_TAC (rule t));; let UNDF t = (TYPE_THEN t UNDISCH_FIND_TAC );; let GRABF t ttac = (UNDF t THEN (DISCH_THEN ttac));; let USEF t rule = (TYPE_THEN t (fun t' -> UNDISCH_FIND_THEN t' (fun u -> ASSUME_TAC (rule u))));; (* ------------------------------------------------------------------ *) (* UNIFY_EXISTS_TAC *) (* ------------------------------------------------------------------ *) let rec EXISTSL_TAC tml = match tml with a::tml' -> EXISTS_TAC a THEN EXISTSL_TAC tml' | [] -> ALL_TAC;; (* Goal: ?x1....xn. P1 /\ ... /\ Pm Try to pick ALL of x1...xn to unify ONE or more Pi with terms appearing in the assumption list, trying term_unify on each Pi with each assumption. *) let (UNIFY_EXISTS_TAC:tactic) = let run_one wc assum (varl,sofar) = if varl = [] then (varl,sofar) else try ( let wc' = instantiate ([],sofar,[]) wc in let (_,ins,_) = term_unify varl wc' assum in let insv = map snd ins in ( subtract varl insv , union sofar ins ) ) with failure -> (varl,sofar) in let run_onel asl wc (varl,sofar) = itlist (run_one wc) asl (varl,sofar) in let run_all varl sofar wcl asl = itlist (run_onel asl) wcl (varl,sofar) in let full_unify (asl,w) = let (varl,ws) = strip_exists w in let vargl = map genvar (map type_of varl) in let wg = instantiate ([],zip vargl varl,[]) ws in let wcg = conjuncts wg in let (vargl',sofar) = run_all vargl [] wcg ( asl) in if (vargl' = []) then map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl) else failwith "full_unify: unification not found " in fun (asl,w) -> try( let asl' = map (concl o snd) asl in let asl'' = flat (map (conjuncts ) asl') in let varsub = full_unify (asl'',w) in EXISTSL_TAC varsub (asl,w) ) with failure -> failwith "UNIFY_EXIST_TAC: unification not found.";; (* partial example *) let unify_exists_tac_example = try(prove_by_refinement( `!C a b v A R TX U SS. (A v /\ (a = v) /\ (C:num->num->bool) a b /\ R a ==> ?v v'. TX v' /\ U v v' /\ C v' v /\ SS v)`, (* {{{ proof *) [ REP_BASIC_TAC; UNIFY_EXISTS_TAC; (* v' -> a and v -> b *) (* not finished. Here is a variant approach. *) REP_GEN_TAC; DISCH_TAC; UNIFY_EXISTS_TAC; ])) with failure -> (REFL `T`);; (* }}} *) (* ------------------------------------------------------------------ *) (* UNIFY_EXISTS conversion *) (* ------------------------------------------------------------------ *) (* FIRST argument is the "certificate" second arg is the goal. Example: UNIFY_EXISTS `(f:num->bool) x` `?t. (f:num->bool) t` *) let (UNIFY_EXISTS:thm -> term -> thm) = let run_one wc assum (varl,sofar) = if varl = [] then (varl,sofar) else try ( let wc' = instantiate ([],sofar,[]) wc in let (_,ins,_) = term_unify varl wc' assum in let insv = map snd ins in ( subtract varl insv , union sofar ins ) ) with failure -> (varl,sofar) in let run_onel asl wc (varl,sofar) = itlist (run_one wc) asl (varl,sofar) in let run_all varl sofar wcl asl = itlist (run_onel asl) wcl (varl,sofar) in let full_unify (t,w) = let (varl,ws) = strip_exists w in let vargl = map genvar (map type_of varl) in let wg = instantiate ([],zip vargl varl,[]) ws in let wcg = conjuncts wg in let (vargl',sofar) = run_all vargl [] wcg ( [concl t]) in if (vargl' = []) then map (C rev_assoc sofar) (map (C rev_assoc (zip vargl varl)) varl) else failwith "full_unify: unification not found " in fun t w -> try( if not(is_exists w) then failwith "UNIFY_EXISTS: not EXISTS" else let varl' = (full_unify (t,w)) in let (varl,ws) = strip_exists w in let varsub = zip varl' varl in let varlb = map (fun s-> chop_list s (rev varl)) (range 1 (length varl)) in let targets = map (fun s-> (instantiate ([],varsub,[]) (list_mk_exists( rev (fst s), ws)) )) varlb in let target_zip = zip (rev targets) varl' in itlist (fun s th -> EXISTS s th) target_zip t ) with failure -> failwith "UNIFY_EXISTS: unification not found.";; let unify_exists_example= UNIFY_EXISTS (ARITH_RULE `2 = 0+2`) `(?x y. ((x:num) = y))`;; (* now make a prover for it *) (* ------------------------------------------------------------------ *) (* drop_ant_tac replaces 0 A ==>B 1 A with 0 B 1 A in hypothesis list *) let DROP_ANT_TAC pq = UNDISCH_TAC pq THEN (UNDISCH_TAC (fst (dest_imp pq))) THEN DISCH_THEN (fun pthm -> ASSUME_TAC pthm THEN DISCH_THEN (fun pqthm -> ASSUME_TAC (MATCH_MP pqthm pthm )));; let (DROP_ALL_ANT_TAC:tactic) = fun (asl,w) -> let imps = filter (is_imp) (map (concl o snd) asl) in MAP_EVERY (TRY o DROP_ANT_TAC) imps (asl,w);;
let drop_ant_tac_example = 
prove_by_refinement( `!A B C D E. (A /\ (A ==> B) /\ (C ==>D) /\ C) ==> (E \/ C \/ B)`,
(* {{{ proof *) [ REP_BASIC_TAC; DROP_ALL_ANT_TAC; ASM_REWRITE_TAC[]; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* ASSUME tm, then prove it later. almost the same as asm-cases-tac *) let (BACK_TAC : term -> tactic) = fun tm (asl,w) -> let ng = mk_imp (tm,w) in (SUBGOAL_TAC ng THENL [ALL_TAC;DISCH_THEN IMATCH_MP_TAC ]) (asl,w);; (* --- *) (* Using hash numbers for tactics *) (* --- *) let label_of_hash ((asl,g):goal) (h:int) = let one_label h (s,tm) = if (h = hash_of_term (concl tm)) then let s1 = String.sub s 2 (String.length s - 2) in int_of_string s1 else failwith "label_of_hash" in tryfind (one_label h) asl;; let HASHIFY m h w = m (label_of_hash w h) w;; let UNDH = HASHIFY UND;; let REWRH = HASHIFY REWR;; let KILLH = HASHIFY KILL;; let COPYH = HASHIFY COPY;; let HASHIFY1 m h tm w = m (label_of_hash w h) tm w;; let USEH = HASHIFY1 USE;; let LEFTH = HASHIFY1 LEFT;; let RIGHTH = HASHIFY1 RIGHT;; let TSPECH tm h w = TSPEC tm (label_of_hash w h) w ;;