(* ========================================================================= *) (* Implicational conversions, implicational rewriting and target rewriting. *) (* *) (* (c) Copyright, Vincent Aravantinos, 2012-2013 *) (* Analysis and Design of Dependable Systems *) (* fortiss GmbH, Munich, Germany *) (* *) (* Formerly: Hardware Verification Group, *) (* Concordia University *) (* *) (* Contact: <vincent.aravantinos@fortiss.org> *) (* ========================================================================= *) let IMP_REWRITE_TAC,TARGET_REWRITE_TAC,HINT_EXISTS_TAC, SEQ_IMP_REWRITE_TAC,CASE_REWRITE_TAC = let I = fun x -> x in (* Same as [UNDISCH] but also returns the undischarged term *) let UNDISCH_TERM th = let p = (fst o dest_imp o concl) th in p,UNDISCH th in (* Same as [UNDISCH_ALL] but also returns the undischarged terms *) let rec UNDISCH_TERMS th = try let t,th' = UNDISCH_TERM th in let ts,th'' = UNDISCH_TERMS th' in t::ts,th'' with Failure _ -> [],th in (* Comblies the function [f] to the conclusion of an implicational theorem. *) let MAP_CONCLUSION f th = let p,th = UNDISCH_TERM th in DISCH p (f th) in let strip_conj = binops `(/\)` in (* For a list [f1;...;fk], returns the first [fi x] that succeeds. *) let rec tryfind_fun fs x = match fs with |[] -> failwith "tryfind_fun" |f::fs' -> try f x with Failure _ -> tryfind_fun fs' x in (* Same as [mapfilter] but also provides the rank of the iteration as an * argument to [f]. *) let mapfilteri f = let rec self i = function |[] -> [] |h::t -> let rest = self (i+1) t in try f i h :: rest with Failure _ -> rest in self 0 in let list_of_option = function None -> [] | Some x -> [x] in let try_list f x = try f x with Failure _ -> [] in (* A few constants. *) let A_ = `A:bool` and B_ = `B:bool` and C_ = `C:bool` and D_ = `D:bool` in let T_ = `T:bool` in (* For a term t, builds `t ==> t` *) let IMP_REFL = let lem = TAUT `A ==> A` in fun t -> INST [t,A_] lem in (* Conversion version of [variant]: * Given variables [v1;...;vk] to avoid and a term [t], * returns [|- t = t'] where [t'] is the same as [t] without any use of the * variables [v1;...;vk]. *) let VARIANT_CONV av t = let vs = variables t in let mapping = filter (fun (x,y) -> x <> y) (zip vs (variants av vs)) in DEPTH_CONV (fun u -> ALPHA_CONV (assoc (bndvar u) mapping) u) t in (* Rule version of [VARIANT_CONV] *) let VARIANT_RULE = CONV_RULE o VARIANT_CONV in (* Discharges the first hypothesis of a theorem. *) let DISCH_HD th = DISCH (hd (hyp th)) th in (* Rule version of [REWR_CONV] *) let REWR_RULE = CONV_RULE o REWR_CONV in (* Given a list [A1;...;Ak] and a theorem [th], * returns [|- A1 /\ ... /\ Ak ==> th]. *) let DISCH_IMP_IMP = let f = function |[] -> I |t::ts -> rev_itlist (fun t -> REWR_RULE IMP_IMP o DISCH t) ts o DISCH t in f o rev in (* Given a term [A /\ B] and a theorem [th], returns [|- A ==> B ==> th]. *) let rec DISCH_CONJ t th = try let t1,t2 = dest_conj t in REWR_RULE IMP_IMP (DISCH_CONJ t1 (DISCH_CONJ t2 th)) with Failure _ -> DISCH t th in (* Specializes all the universally quantified variables of a theorem, * and returns both the theorem and the list of variables. *) let rec SPEC_VARS th = try let v,th' = SPEC_VAR th in let vs,th'' = SPEC_VARS th' in v::vs,th'' with Failure _ -> [],th in (* Comblies the function [f] to the body of a universally quantified theorem. *) let MAP_FORALL_BODY f th = let vs,th = SPEC_VARS th in GENL vs (f th) in (* Given a theorem of the form [!xyz. P ==> !uvw. C] and a function [f], * return [!xyz. P ==> !uvw. f C]. *) let GEN_MAP_CONCLUSION = MAP_FORALL_BODY o MAP_CONCLUSION o MAP_FORALL_BODY in (* Turn a theorem of the form [x ==> y /\ z] into [(x==>y) /\ (x==>z)]. * Also deals with universal quantifications if necessary * (e.g., [x ==> !v. y /\ z] will be turned into * [(x ==> !v. y) /\ (x ==> !v. z)]) * * possible improvement: apply the rewrite more locally *) let IMPLY_AND = let IMPLY_AND_RDISTRIB = TAUT `(x ==> y /\ z) <=> (x==>y) /\(x==>z)` in PURE_REWRITE_RULE [GSYM AND_FORALL_THM;IMP_IMP; RIGHT_IMP_FORALL_THM;IMPLY_AND_RDISTRIB;GSYM CONJ_ASSOC] in (* Returns the two operands of a binary combination. * Contrary to [dest_binary], does not check what is the operator. *) let dest_binary_blind = function |Comb(Comb(_,l),r) -> l,r |_ -> failwith "dest_binary_blind" in let spec_all = repeat (snd o dest_forall) in let thm_lt (th1:thm) th2 = th1 < th2 in (* GMATCH_MP (U1 |- !x1...xn. H1 /\ ... /\ Hk ==> C) (U2 |- P) * = (U1 u U2 |- !y1...ym. G1' /\ ... /\ Gl' ==> C') * where: * - P matches some Hi * - C' is the result of applying the matching substitution to C * - Gj' is the result of applying the matching substitution to Hj * - G1',...,Gl' is the list corresponding to H1,...,Hk but without Hi * - y1...ym are the variables among x1,...,xn that are not instantiated * * possible improvement: make a specific conversion, * define a MATCH_MP that also returns the instantiated variables *) let GMATCH_MP = let swap = CONV_RULE (REWR_CONV (TAUT `(p==>q==>r) <=> (q==>p==>r)`)) in fun th1 -> let vs,th1' = SPEC_VARS th1 in let hs,th1'' = UNDISCH_TERMS (PURE_REWRITE_RULE [IMP_CONJ] th1') in fun th2 -> let f h hs = let th1''' = DISCH h th1'' in let th1'''' = try swap (DISCH_IMP_IMP hs th1''') with Failure _ -> th1''' in MATCH_MP (GENL vs th1'''') th2 in let rec loop acc = function |[] -> [] |h::hs -> (try [f h (acc @ hs)] with Failure _ -> []) @ loop (h::acc) hs in loop [] hs in let GMATCH_MPS ths1 ths2 = let insert (y:thm) = function |[] -> [y] |x::_ as xs when equals_thm x y -> xs |x::xs when thm_lt x y -> x :: insert y xs |_::_ as xs -> y::xs in let inserts ys = itlist insert ys in match ths1 with |[] -> [] |th1::ths1' -> let rec self acc th1 ths1 = function |[] -> (match ths1 with [] -> acc | th::ths1' -> self acc th ths1' ths2) |th2::ths2' -> self (inserts (GMATCH_MP th1 th2) acc) th1 ths1 ths2' in self [] th1 ths1' ths2 in let MP_CLOSURE ths1 ths2 = let ths1 = filter (is_imp o spec_all o concl) ths1 in let rec self ths2 = function |[] -> [] |_::_ as ths1 -> let ths1'' = GMATCH_MPS ths1 ths2 in self ths2 ths1'' @ ths1'' in self ths2 ths1 in (* Set of terms. Implemented as ordered lists. *) let module Tset = struct type t = term list let cmp (x:term) y = Pervasives.compare x y let lt (x:term) y = Pervasives.compare x y < 0 let lift f = List.sort cmp o f let of_list = lift I let insert ts t = let rec self = function |[] -> [t] |x::xs when lt x t -> x::self xs |x::_ as xs when x = t -> xs |xs -> t::xs in if t = T_ then ts else self ts let remove ts t = let rec self = function |[] -> [] |x::xs when lt x t -> x::self xs |x::xs when x = t -> xs |_::_ as xs -> xs in self ts let strip_conj = let rec self acc t = try let t1,t2 = dest_conj t in self (self acc t1) t2 with Failure _ -> insert acc t in self [] let rec union l1 l2 = match l1 with |[] -> l2 |h1::t1 -> match l2 with |[] -> l1 |h2::t2 when lt h1 h2 -> h1::union t1 l2 |h2::t2 when h1 = h2 -> h1::union t1 t2 |h2::t2 -> h2::union l1 t2 let rec mem x = function |x'::xs when x' = x -> true |x'::xs when lt x' x -> mem x xs |_ -> false let subtract l1 l2 = filter (fun x -> not (mem x l2)) l1 let empty = [] let flat_revmap f = let rec self acc = function |[] -> acc |x::xs -> self (union (f x) acc) xs in self [] let flat_map f = flat_revmap f o rev let rec frees acc = function |Var _ as t -> insert acc t |Const _ -> acc |Abs(v,b) -> remove (frees acc b) v |Comb(u,v) -> frees (frees acc u) v let freesl ts = itlist (C frees) ts empty let frees = frees empty end in let module Type_annoted_term = struct type t = |Var_ of string * hol_type |Const_ of string * hol_type * term |Comb_ of t * t * hol_type |Abs_ of t * t * hol_type let type_of = function |Var_(_,ty) -> ty |Const_(_,ty,_) -> ty |Comb_(_,_,ty) -> ty |Abs_(_,_,ty) -> ty let rec of_term = function |Var(s,ty) -> Var_(s,ty) |Const(s,ty) as t -> Const_(s,ty,t) |Comb(u,v) -> let u' = of_term u and v' = of_term v in Comb_(u',v',snd (dest_fun_ty (type_of u'))) |Abs(x,b) -> let x' = of_term x and b' = of_term b in Abs_(x',b',mk_fun_ty (type_of x') (type_of b')) let rec equal t1 t2 = match t1,t2 with |Var_(s1,ty1),Var_(s2,ty2) |Const_(s1,ty1,_),Const_(s2,ty2,_) -> s1 = s2 & ty1 = ty2 |Comb_(u1,v1,_),Comb_(u2,v2,_) -> equal u1 u2 & equal v1 v2 |Abs_(v1,b1,_),Abs_(v2,b2,_) -> equal v1 v2 & equal b1 b2 |_ -> false let rec to_term = function |Var_(s,ty) -> mk_var(s,ty) |Const_(_,_,t) -> t |Comb_(u,v,_) -> mk_comb(to_term u,to_term v) |Abs_(v,b,_) -> mk_abs(to_term v,to_term b) let dummy = Var_("",aty) let rec find_term p t = if p t then t else match t with |Abs_(_,b,_) -> find_term p b |Comb_(u,v,_) -> try find_term p u with Failure _ -> find_term p v |_ -> failwith "Annot.find_term" end in let module Annot = Type_annoted_term in (* ------------------------------------------------------------------------- *) (* First-order matching of terms. *) (* *) (* Same note as in [drule.ml]: *) (* in the event of spillover patterns, this may return false results; *) (* but there's usually an implicit check outside that the match worked *) (* anyway. A test could be put in (see if any "env" variables are left in *) (* the term after abstracting out the pattern instances) but it'd be slower. *) (* ------------------------------------------------------------------------- *) let fo_term_match lcs p t = let fail () = failwith "fo_term_match" in let rec self bnds (tenv,tyenv as env) p t = match p,t with |Comb(p1,p2),Annot.Comb_(t1,t2,_) -> self bnds (self bnds env p1 t1) p2 t2 |Abs(v,p),Annot.Abs_(v',t,_) -> let tyenv' = type_match (type_of v) (Annot.type_of v') tyenv in self ((v',v)::bnds) (tenv,tyenv') p t |Const(n,ty),Annot.Const_(n',ty',_) -> if n <> n' then fail () else let tyenv' = type_match ty ty' tyenv in tenv,tyenv' |Var(n,ty) as v,t -> (* Is [v] bound? *) (try if Annot.equal t (rev_assoc v bnds) then env else fail () (* No *) with Failure _ -> if mem v lcs then match t with |Annot.Var_(n',ty') when n' = n & ty' = ty -> env |_ -> fail () else let tyenv' = type_match ty (Annot.type_of t) tyenv in let t' = try Some (rev_assoc v tenv) with Failure _ -> None in match t' with |Some t' -> if t = t' then tenv,tyenv' else fail () |None -> (t,v)::tenv,tyenv') |_ -> fail () in let tenv,tyenv = self [] ([],[]) p (Annot.of_term t) in let inst = inst tyenv in List.rev_map (fun t,v -> Annot.to_term t,inst v) tenv,tyenv in let GEN_PART_MATCH_ALL = let rec match_bvs t1 t2 acc = try let v1,b1 = dest_abs t1 and v2,b2 = dest_abs t2 in let n1 = fst(dest_var v1) and n2 = fst(dest_var v2) in let newacc = if n1 = n2 then acc else insert (n1,n2) acc in match_bvs b1 b2 newacc with Failure _ -> try let l1,r1 = dest_comb t1 and l2,r2 = dest_comb t2 in match_bvs l1 l2 (match_bvs r1 r2 acc) with Failure _ -> acc in fun partfn th -> let sth = SPEC_ALL th in let bod = concl sth in let pbod = partfn bod in let lcs = intersect (frees (concl th)) (freesl(hyp th)) in let fvs = subtract (subtract (frees bod) (frees pbod)) lcs in fun tm -> let bvms = match_bvs tm pbod [] in let abod = deep_alpha bvms bod in let ath = EQ_MP (ALPHA bod abod) sth in let insts,tyinsts = fo_term_match lcs (partfn abod) tm in let eth = INSTANTIATE_ALL ([],insts,tyinsts) (GENL fvs ath) in let fth = itlist (fun v th -> snd(SPEC_VAR th)) fvs eth in let tm' = partfn (concl fth) in if Pervasives.compare tm' tm = 0 then fth else try SUBS[ALPHA tm' tm] fth with Failure _ -> failwith "PART_MATCH: Sanity check failure" in let exists_subterm p t = try ignore (find_term p t);true with Failure _ -> false in let module Fo_nets = struct type term_label = |Vnet of int |Lcnet of string * int |Cnet of string * int |Lnet of int type 'a t = Netnode of (term_label * 'a t) list * 'a list let empty_net = Netnode([],[]) let enter = let label_to_store lcs t = let op,args = strip_comb t in let nargs = length args in match op with |Const(n,_) -> Cnet(n,nargs),args |Abs(v,b) -> let b' = if mem v lcs then vsubst [genvar(type_of v),v] b else b in Lnet nargs,b'::args |Var(n,_) when mem op lcs -> Lcnet(n,nargs),args |Var(_,_) -> Vnet nargs,args |_ -> assert false in let rec net_update lcs elem (Netnode(edges,tips)) = function |[] -> Netnode(edges,elem::tips) |t::rts -> let label,nts = label_to_store lcs t in let child,others = try (snd F_F I) (remove (fun (x,y) -> x = label) edges) with Failure _ -> empty_net,edges in let new_child = net_update lcs elem child (nts@rts) in Netnode ((label,new_child)::others,tips) in fun lcs (t,elem) net -> net_update lcs elem net [t] let lookup = let label_for_lookup t = let op,args = strip_comb t in let nargs = length args in match op with |Const(n,_) -> Cnet(n,nargs),args |Abs(_,b) -> Lnet nargs,b::args |Var(n,_) -> Lcnet(n,nargs),args |Comb _ -> assert false in let rec follow (Netnode(edges,tips)) = function |[] -> tips |t::rts -> let label,nts = label_for_lookup t in let collection = try follow (assoc label edges) (nts@rts) with Failure _ -> [] in let rec support = function |[] -> [0,rts] |t::ts -> let ((k,nts')::res') as res = support ts in (k+1,(t::nts'))::res in let follows = let f (k,nts) = try follow (assoc (Vnet k) edges) nts with Failure _ -> [] in map f (support nts) in collection @ flat follows in fun t net -> follow net [t] let rec filter p (Netnode(edges,tips)) = Netnode( List.map (fun l,n -> l,filter p n) edges, List.filter p tips) end in let module Variance = struct type t = Co | Contra let neg = function Co -> Contra | Contra -> Co end in (*****************************************************************************) (* IMPLICATIONAL RULES *) (* i.e., rules to build propositions based on implications rather than *) (* equivalence. *) (*****************************************************************************) let module Impconv = struct let MKIMP_common lem th1 th2 = let a,b = dest_imp (concl th1) and c,d = dest_imp (concl th2) in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) (* Similar to [MK_CONJ] but theorems should be implicational instead of * equational, i.e., conjoin both sides of two implicational theorems. * * More precisely: given two theorems [A ==> B] and [C ==> D], * returns [A /\ C ==> B /\ D]. *) let MKIMP_CONJ = MKIMP_common MONO_AND (* Similar to [MK_DISJ] but theorems should be implicational instead of * equational, i.e., disjoin both sides of two implicational theorems. * * More precisely: given two theorems [A ==> B] and [C ==> D], * returns [A \/ C ==> B \/ D]. *) let MKIMP_DISJ = MKIMP_common MONO_OR let MKIMP_IFF = let lem = TAUT `((A ==> B) ==> (C ==> D)) /\ ((B ==> A) ==> (D ==> C)) ==> (A <=> B) ==> (C <=> D)` in fun th1 th2 -> let ab,cd = dest_imp (concl th1) in let a,b = dest_imp ab and c,d = dest_imp cd in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) (* th1 = (A ==> B) ==> C1 * th2 = (B ==> A) ==> C2 * output = (A <=> B) ==> (C1 /\ C2) *) let MKIMP_CONTRA_IFF = let lem = TAUT `((A ==> B) ==> C) /\ ((B ==> A) ==> D) ==> (A <=> B) ==> C /\ D` in fun th1 th2 -> let ab,c = dest_imp (concl th1) and _,d = dest_imp (concl th2) in let a,b = dest_imp ab in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) let MKIMPL_CONTRA_IFF = let lem = TAUT `((A ==> B) ==> C) ==> (A <=> B) ==> C /\ (B ==> A)` in fun th -> let ab,c = dest_imp (concl th) in let a,b = dest_imp ab in MP (INST [a,A_;b,B_;c,C_] lem) th let MKIMPR_CONTRA_IFF = let lem = TAUT `((B ==> A) ==> D) ==> (A <=> B) ==> (A ==> B) /\ D` in fun th -> let ba,d = dest_imp (concl th) in let b,a = dest_imp ba in MP (INST [a,A_;b,B_;d,D_] lem) th let MKIMP_CO_IFF = let lem = TAUT `(C ==> A ==> B) /\ (D ==> B ==> A) ==> C /\ D ==> (A <=> B)` in fun th1 th2 -> let c,ab = dest_imp (concl th1) and d,_ = dest_imp (concl th2) in let a,b = dest_imp ab in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) let MKIMPL_CO_IFF = let lem = TAUT `(C ==> A ==> B) ==> C /\ (B ==> A) ==> (A <=> B)` in fun th -> let c,ab = dest_imp (concl th) in let a,b = dest_imp ab in MP (INST [a,A_;b,B_;c,C_] lem) th let MKIMPR_CO_IFF = let lem = TAUT `(D ==> B ==> A) ==> (A ==> B) /\ D ==> (A <=> B)` in fun th -> let d,ba = dest_imp (concl th) in let b,a = dest_imp ba in MP (INST [a,A_;b,B_;d,D_] lem) th (* Given two theorems [A ==> B] and [C ==> D], * returns [(B ==> C) ==> (A ==> D)]. *) let MKIMP_IMP th1 th2 = let b,a = dest_imp (concl th1) and c,d = dest_imp (concl th2) in MP (INST [a,A_;b,B_;c,C_;d,D_] MONO_IMP) (CONJ th1 th2) let MKIMPL_common lem = let lem' = REWRITE_RULE[] (INST [C_,D_] lem) in fun th t -> let a,b = dest_imp (concl th) in MP (INST [a,A_;b,B_;t,C_] lem') th (* Given a theorem [A ==> B] and a term [C], * returns [A /\ C ==> B /\ C]. *) let MKIMPL_CONJ = MKIMPL_common MONO_AND (* Given a theorem [A ==> B] and a term [C], * returns [A \/ C ==> B \/ C]. *) let MKIMPL_DISJ = MKIMPL_common MONO_OR (* Given a theorem [A ==> B] and a term [C], * returns [(B ==> C) ==> (A ==> C)]. *) let MKIMPL_IMP = let MONO_IMP' = REWRITE_RULE[] (INST [C_,D_] MONO_IMP) in fun th t -> let b,a = dest_imp (concl th) in MP (INST [a,A_;b,B_;t,C_] MONO_IMP') th let MKIMPR_common lem = let lem' = REWRITE_RULE[] (INST [A_,B_] lem) in fun t th -> let c,d = dest_imp (concl th) in MP (INST [c,C_;d,D_;t,A_] lem') th (* Given a term [A] and a theorem [B ==> C], * returns [A /\ B ==> A /\ C]. *) let MKIMPR_CONJ = MKIMPR_common MONO_AND (* Given a term [A] and a theorem [B ==> C], * returns [A \/ B ==> A \/ C]. *) let MKIMPR_DISJ = MKIMPR_common MONO_OR (* Given a term [A] and a theorem [B ==> C], * returns [(A ==> B) ==> (A ==> C)]. *) let MKIMPR_IMP = MKIMPR_common MONO_IMP (* Given a theorem [A ==> B], returns [~B ==> ~A]. *) let MKIMP_NOT th = let b,a = dest_imp (concl th) in MP (INST [a,A_;b,B_] MONO_NOT) th let MKIMP_QUANT lem x th = let x_ty = type_of x and p,q = dest_imp (concl th) in let p' = mk_abs(x,p) and q' = mk_abs(x,q) in let P = mk_var("P",mk_fun_ty x_ty bool_ty) in let Q = mk_var("Q",mk_fun_ty x_ty bool_ty) in let lem = INST [p',P;q',Q] (INST_TYPE [x_ty,aty] lem) in let c = ONCE_DEPTH_CONV (ALPHA_CONV x) THENC ONCE_DEPTH_CONV BETA_CONV in MP (CONV_RULE c lem) (GEN x th) (* Given a variable [x] and a theorem [A ==> B], * returns [(!x. A) ==> (!x. B)]. *) let MKIMP_FORALL = MKIMP_QUANT MONO_FORALL (* Given a variable [x] and a theorem [A ==> B], * returns [(?x. A) ==> (?x. B)]. *) let MKIMP_EXISTS = MKIMP_QUANT MONO_EXISTS (* Given two theorems [A ==> B] and [B ==> C ==> D], * returns [(B ==> C) ==> (A ==> D)], * i.e., similar to [MKIMP_IMP] but allows to remove the context [B] * since it is a consequence of [A]. *) let MKIMP_IMP_CONTRA_CTXT = let lem = TAUT `(B==>A) /\ (A==>B==>C==>D) ==> (A==>C) ==> (B==>D)` in fun th1 th2 -> let a,bcd = dest_imp (concl th2) in let b,cd = dest_imp bcd in let c,d = dest_imp cd in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) let MKIMP_IMP_CO_CTXT = let lem = TAUT `(A==>B) /\ (A==>B==>D==>C) ==> (B==>D) ==> (A==>C)` in fun th1 th2 -> let a,bdc = dest_imp (concl th2) in let b,dc = dest_imp bdc in let d,c = dest_imp dc in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) (* Given a theorem [B ==> C ==> D], returns [(B ==> C) ==> (B ==> D)], * i.e., similar to [MKIMP_IMP] but allows to remove the context [B] * since it is a consequence of [A]. *) let MKIMPR_IMP_CTXT = let lem = TAUT `(A==>C==>D) ==> (A==>C) ==> (A==>D)` in fun th -> let a,cd = dest_imp (concl th) in let c,d = dest_imp cd in MP (INST [c,C_;d,D_;a,A_] lem) th (* Given two theorems [A ==> B] and [A ==> B ==> C ==> D], * returns [(A /\ C) ==> (B /\ D)], * i.e., similar to [MKIMP_CONJ] but allows to remove the contexts [A] and [B]. *) let MKIMP_CONJ_CONTRA_CTXT = let lem = TAUT `(C==>A==>B) /\ (A==>B==>C==>D) ==> (A/\C==>B/\D)` in fun th1 th2 -> let a,bcd = dest_imp (concl th2) in let b,cd = dest_imp bcd in let c,d = dest_imp cd in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) let MKIMPL_CONJ_CONTRA_CTXT = let lem = TAUT `(C==>A==>B) ==> (A/\C==>B/\C)` in fun th -> let c,ab = dest_imp (concl th) in let a,b = dest_imp ab in MP (INST [a,A_;b,B_;c,C_] lem) th let MKIMPR_CONJ_CONTRA_CTXT = let lem = TAUT `(A==>C==>D) ==> (A/\C==>A/\D)` in fun th -> let a,cd = dest_imp (concl th) in let c,d = dest_imp cd in MP (INST [a,A_;c,C_;d,D_] lem) th let MKIMP_CONJ_CO_CTXT = let lem = TAUT `(B==>A) /\ (B==>D==>C) ==> (B/\D==>A/\C)` in fun th1 th2 -> let b,a = dest_imp (concl th1) in let d,c = dest_imp (snd (dest_imp (concl th2))) in MP (INST [a,A_;b,B_;c,C_;d,D_] lem) (CONJ th1 th2) let MKIMPL_CONJ_CO_CTXT = let lem = TAUT `(B==>A) ==> (B/\C==>A/\C)` in fun th -> let b,a = dest_imp (concl th) in fun c -> MP (INST [a,A_;b,B_;c,C_] lem) th let MKIMPL_CONJ_CO2_CTXT = let lem = TAUT `(C==>B==>A) ==> (B/\C==>A/\C)` in fun th -> let c,ba = dest_imp (concl th) in let b,a = dest_imp ba in MP (INST [a,A_;b,B_;c,C_] lem) th let MKIMPR_CONJ_CO_CTXT = MKIMPR_CONJ_CONTRA_CTXT (*****************************************************************************) (* IMPLICATIONAL CONVERSIONS *) (*****************************************************************************) open Variance (* An implicational conversion maps a term t to a theorem of the form: * t' ==> t if covariant * t ==> t' if contravariant *) type imp_conv = Variance.t -> term -> thm (* Trivial embedding of conversions into implicational conversions. *) let imp_conv_of_conv:conv->imp_conv = fun c v t -> let th1,th2 = EQ_IMP_RULE (c t) in match v with Co -> th2 | Contra -> th1 (* Retrieves the outcome of an implicational conversion, i.e., t'. *) let imp_conv_outcome th v = let t1,t2 = dest_binary_blind (concl th) in match v with Co -> t1 | Contra -> t2 (* [ALL_IMPCONV _ t] returns `t==>t` *) let ALL_IMPCONV:imp_conv = fun _ -> IMP_REFL (* The implicational conversion which always fails. *) let NO_IMPCONV:imp_conv = fun _ _ -> failwith "NO_IMPCONV" let bind_impconv (c:imp_conv) v th = let t1,t2 = dest_imp (concl th) in match v with |Co -> IMP_TRANS (c v t1) th |Contra -> IMP_TRANS th (c v t2) let THEN_IMPCONV (c1:imp_conv) c2 v t = bind_impconv c2 v (c1 v t) (*****************************************************************************) (* SOME USEFUL IMPLICATIONAL CONVERSIONS *) (*****************************************************************************) (* Given a theorem [p ==> c], returns the implicational conversion which: * - in the covariant case, matches the input term [t] against [c] and returns * [s(p) ==> t], where [s] is the matching substitution * - in the contravariant case, matches the input term [t] against [p] and returns * [t ==> s(c)], where [s] is the matching substitution *) let MATCH_MP_IMPCONV:thm->imp_conv = fun th -> function |Co -> GEN_PART_MATCH rand th |Contra -> GEN_PART_MATCH lhand th (*****************************************************************************) (* INTERFACE *) (*****************************************************************************) (* From an implicational conversion builds a rule, i.e., a function which * takes a theorem and returns a new theorem. *) let IMPCONV_RULE:imp_conv->thm->thm = fun c th -> let t = concl th in MATCH_MP (c Contra t) th (* From an implicational conversion builds a tactic. *) let IMPCONV_TAC:imp_conv->tactic = fun cnv (_,c as g) -> (MATCH_MP_TAC (cnv Co c) THEN TRY (ACCEPT_TAC TRUTH)) g (*****************************************************************************) (* CONTEXT HANDLING *) (*****************************************************************************) (* [term list] = terms to add to the context *) type 'a with_context = With_context of 'a * (Tset.t -> 'a with_context) * (term -> 'a with_context) let apply (With_context(c,_,_)) = c (* Maybe avoid the augment if the input list is empty? *) let augment (With_context(_,a,_)) = a let diminish (With_context(_,_,d)) = d let apply_with_context c ctx v t = DISCH_CONJ ctx (apply (augment c (Tset.strip_conj ctx)) v t) let imp_conv_of_ctx_imp_conv = (apply:imp_conv with_context -> imp_conv) (* Consider two implicational conversions ic1, ic2. * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C], * then [CONJ_IMPCONV ic1 ic2 Co (A /\ C)] returns [B /\ D ==> A /\ C]. * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns * [C ==> D], then [CONJ_IMPCONV ic1 ic2 Contra (A /\ B)] * returns [A /\ B ==> C /\ D]. * * Additionally takes the context into account, i.e., if [ic2 Co C] returns * [A |- D ==> C], * then [CONJ_IMPCONV ic1 ic2 Co (A /\ B)] returns [|- C /\ D ==> A /\ B] * (i.e., [A] does not appear in the hypotheses). *) let rec CONJ_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> let t1,t2 = dest_conj t in match v with |Co -> (try let th1 = apply c Co t1 in try let t1' = imp_conv_outcome th1 Co in MKIMP_CONJ_CO_CTXT th1 (apply_with_context c t1' Co t2) with Failure _ -> MKIMPL_CONJ_CO_CTXT th1 t2 with Failure _ -> MKIMPR_CONJ_CO_CTXT (apply_with_context c t1 Co t2)) |Contra -> try (* note: we remove t1 in case it appears in t2, since otherwise, * t1 removes t2 and t2 removes t1 *) let t2s = Tset.remove (Tset.strip_conj t2) t1 in let th1 = apply (augment c t2s) Contra t1 in try let t1' = imp_conv_outcome th1 Contra in let t1s = Tset.strip_conj t1 and t1s' = Tset.strip_conj t1' in let t1s'' = Tset.union t1s t1s' in let th2 = apply (augment c t1s'') Contra t2 in let th2' = DISCH_CONJ t1 (DISCH_CONJ t1' th2) in MKIMP_CONJ_CONTRA_CTXT (DISCH_CONJ t2 th1) th2' with Failure _ -> MKIMPL_CONJ_CONTRA_CTXT (DISCH_CONJ t2 th1) with Failure _ -> MKIMPR_CONJ_CONTRA_CTXT (apply_with_context c t1 Contra t2)) :imp_conv), CONJ_CTXIMPCONV o augment c, CONJ_CTXIMPCONV o diminish c) (* Consider two implicational conversions ic1, ic2. * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Co C] returns [D ==> C], * then [DISJ_IMPCONV ic1 ic2 Co (A \/ C)] returns [B \/ D ==> A \/ C]. * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Contra C] returns * [C ==> D], then [DISJ_IMPCONV ic1 ic2 Contra (A \/ B)] * returns [A \/ B ==> C \/ D]. *) let rec DISJ_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> let t1,t2 = dest_disj t in try let th1 = apply c v t1 in try MKIMP_DISJ th1 (apply c v t2) with Failure _ -> MKIMPL_DISJ th1 t2 with Failure _ -> MKIMPR_DISJ t1 (apply c v t2)):imp_conv), DISJ_CTXIMPCONV o augment c, DISJ_CTXIMPCONV o diminish c) (* Consider two implicational conversions ic1, ic2. * Suppose [ic1 Contra A] returns [A ==> B], and [ic2 Co C] returns [D ==> C], * then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns [(B ==> D) ==> (A ==> C)]. * Suppose [ic1 Co A] returns [B ==> A], and [ic2 Contra C] returns * [C ==> D], then [IMP_IMPCONV ic1 ic2 Contra (A ==> C)] * returns [(A ==> C) ==> (B ==> D)]. * * Additionally takes the context into account, i.e., if [ic2 Co C] returns * [B |- D ==> C], then [IMP_IMPCONV ic1 ic2 Co (A ==> C)] returns * [|- (B ==> D) ==> (A ==> C)] (i.e., [B] does not appear in the hypotheses). *) let rec IMP_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> let t1,t2 = dest_imp t in try let v' = Variance.neg v in let th1 = apply c v' t1 in let t1' = imp_conv_outcome th1 v' in let t1s = Tset.union (Tset.strip_conj t1) (Tset.strip_conj t1') in let c' = augment c t1s in let mk = match v with Co -> MKIMP_IMP_CO_CTXT | Contra -> MKIMP_IMP_CONTRA_CTXT in try mk th1 (DISCH_CONJ t1 (DISCH_CONJ t1' (apply c' v t2))) with Failure _ -> MKIMPL_IMP th1 t2 with Failure _ -> MKIMPR_IMP_CTXT (apply_with_context c t1 v t2) ):imp_conv), IMP_CTXIMPCONV o augment c, IMP_CTXIMPCONV o diminish c) let rec IFF_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> let t1,t2 = dest_iff t in let lr,l,r = match v with |Co -> MKIMP_CO_IFF,MKIMPL_CO_IFF,MKIMPR_CO_IFF |Contra -> MKIMP_CONTRA_IFF,MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF in (try let th1 = apply c v (mk_imp (t1,t2)) in try let th2 = apply c v (mk_imp (t2,t1)) in (try MKIMP_IFF th1 th2 with Failure _ -> lr th1 th2) with Failure _ -> l th1 with Failure _ -> r (apply c v (mk_imp (t2,t1))))):imp_conv), IFF_CTXIMPCONV o augment c, IFF_CTXIMPCONV o diminish c) (* Consider an implicational conversion ic. * Suppose [ic Contra A] returns [A ==> B] * then [NOT_IMPCONV ic Co ~A] returns [~B ==> ~A]. * Suppose [ic Co A] returns [B ==> A] * then [NOT_IMPCONV ic Contra ~A] returns [~A ==> ~B]. *) let rec NOT_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> MKIMP_NOT (apply c (Variance.neg v) (dest_neg t))):imp_conv), NOT_CTXIMPCONV o augment c, NOT_CTXIMPCONV o diminish c) let rec QUANT_CTXIMPCONV mkimp sel (c:imp_conv with_context) = With_context( ((fun v t -> let x,b = sel t in let c' = diminish c x in mkimp x (apply c' v b)):imp_conv), QUANT_CTXIMPCONV mkimp sel o augment c, QUANT_CTXIMPCONV mkimp sel o diminish c) (* Consider an implicational conversion ic. * Suppose [ic Co A] returns [B ==> A] * then [FORALL_IMPCONV ic Co (!x.A)] returns [(!x.B) ==> (!x.A)]. * Suppose [ic Contra A] returns [A ==> B] * then [FORALL_IMPCONV ic Contra (!x.A)] returns [(!x.A) ==> (!x.B)]. *) let FORALL_CTXIMPCONV = QUANT_CTXIMPCONV MKIMP_FORALL dest_forall (* Consider an implicational conversion ic. * Suppose [ic Co A] returns [B ==> A] * then [EXISTS_IMPCONV ic Co (?x.A)] returns [(?x.B) ==> (?x.A)]. * Suppose [ic Contra A] returns [A ==> B] * then [EXISTS_IMPCONV ic Contra (?x.A)] returns [(?x.A) ==> (?x.B)]. *) let EXISTS_CTXIMPCONV = QUANT_CTXIMPCONV MKIMP_EXISTS dest_exists (* Applies an implicational conversion on the subformula(s) of the input term*) let rec SUB_CTXIMPCONV = let iff_ty = `:bool->bool->bool` in fun c -> With_context( ((fun v t -> let n,ty = dest_const (fst (strip_comb t)) in apply ((match n with |"==>" -> IMP_CTXIMPCONV |"/\\" -> CONJ_CTXIMPCONV |"\\/" -> DISJ_CTXIMPCONV |"=" when ty = iff_ty -> IFF_CTXIMPCONV |"!" -> FORALL_CTXIMPCONV |"?" -> EXISTS_CTXIMPCONV |"~" -> NOT_CTXIMPCONV |_ -> failwith "SUB_CTXIMPCONV") c) v t):imp_conv), SUB_CTXIMPCONV o augment c, SUB_CTXIMPCONV o diminish c) (* Takes a theorem which results of an implicational conversion and applies * another implicational conversion on the outcome. *) let bind_ctximpconv (c:imp_conv with_context) v th = let t1,t2 = dest_imp (concl th) in match v with |Co -> IMP_TRANS (apply c v t1) th |Contra -> IMP_TRANS th (apply c v t2) let rec BIND_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v th -> bind_ctximpconv c v th), BIND_CTXIMPCONV o augment c, BIND_CTXIMPCONV o diminish c)) (* Sequential combinator. *) let rec THEN_CTXIMPCONV (c1:imp_conv with_context) (c2:imp_conv with_context) = With_context( ((fun v t -> bind_ctximpconv c2 v (apply c1 v t)):imp_conv), (fun x -> THEN_CTXIMPCONV (augment c1 x) (augment c2 x)), (fun x -> THEN_CTXIMPCONV (diminish c1 x) (diminish c2 x))) (* Try combinator *) let rec TRY_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> try apply c v t with Failure _ | Unchanged -> ALL_IMPCONV v t):imp_conv), TRY_CTXIMPCONV o augment c, TRY_CTXIMPCONV o diminish c) (* Applies the first of two implicational conversions that succeeds. *) let rec ORELSE_CTXIMPCONV (c1:imp_conv with_context) (c2:imp_conv with_context) = With_context( ((fun v t -> try apply c1 v t with Failure _ -> apply c2 v t):imp_conv), (fun x -> ORELSE_CTXIMPCONV (augment c1 x) (augment c2 x)), (fun x -> ORELSE_CTXIMPCONV (diminish c1 x) (diminish c2 x))) (* Makes an implicational conversion fail if applying it leaves a term * unchanged. *) let rec CHANGED_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> let th = apply c v t in let l,r = dest_imp (concl th) in if aconv l r then failwith "CHANGED_CTXIMPCONV" else th):imp_conv), CHANGED_CTXIMPCONV o augment c, CHANGED_CTXIMPCONV o diminish c) let rec UNCHANGED_OF_FAIL_CTXIMPCONV (c:imp_conv with_context) = With_context( ((fun v t -> try apply c v t with Failure _ -> raise Unchanged ):imp_conv), UNCHANGED_OF_FAIL_CTXIMPCONV o augment c, UNCHANGED_OF_FAIL_CTXIMPCONV o diminish c) let rec REPEAT_UNCHANGED_CTXIMPCONV = let rec map_all f xs x = match xs with |[] -> [] |y::ys -> f y x :: map_all f ys x in fun (cs:imp_conv with_context list) -> With_context( ((fun v t -> let rec loop changed acc = function |[] when changed -> loop false acc cs |[] -> acc |c::cs' -> try let acc' = bind_ctximpconv c v acc in loop true acc' cs' with Unchanged -> loop changed acc cs' in loop false (IMP_REFL t) cs):imp_conv), REPEAT_UNCHANGED_CTXIMPCONV o map_all augment cs, REPEAT_UNCHANGED_CTXIMPCONV o map_all diminish cs) type atomic = Atomic | Non_atomic let DEPTH_CTXIMPCONV = let bind c na v th = let t1,t2 = dest_imp (concl th) in match v with |Co -> IMP_TRANS (apply c na v t1) th |Contra -> IMP_TRANS th (apply c na v t2) in let rec self (c:(atomic->imp_conv) with_context) = With_context( (fun v t -> try let th1 = apply (SUB_CTXIMPCONV (self c)) v t in (try bind c Non_atomic v th1 with Failure _ -> th1) with | Failure "SUB_CTXIMPCONV" -> let th1 = apply c Atomic v t in (try bind_ctximpconv (self c) v th1 with Failure _ -> th1) | Failure _ -> apply c Non_atomic v t), self o augment c, self o diminish c) in UNCHANGED_OF_FAIL_CTXIMPCONV o self let TOP_DEPTH_CTXIMPCONV = let rec self (c:imp_conv with_context) = With_context( (fun v t -> try let th = apply c v t in try bind_ctximpconv (self c) v th with Failure _ -> th with Failure _ -> apply (SUB_CTXIMPCONV (self c)) v t), self o augment c, self o diminish c) in UNCHANGED_OF_FAIL_CTXIMPCONV o self let ONCE_DEPTH_CTXIMPCONV = let rec self (c:(atomic->imp_conv) with_context) = With_context( (fun v t -> try apply (SUB_CTXIMPCONV (self c)) v t with | Failure "SUB_CTXIMPCONV" -> apply c Atomic v t | Failure _ -> apply c Non_atomic v t), self o augment c, self o diminish c) in UNCHANGED_OF_FAIL_CTXIMPCONV o self let CTXIMPCONV_RULE (c:imp_conv with_context) th = MATCH_MP (apply c Contra (concl th)) th let CTXIMPCONV_TAC (cnv:imp_conv with_context) : tactic = fun (asms,c as g) -> let cnv' = augment cnv (map (concl o snd) asms) in (MATCH_MP_TAC (apply cnv' Co c) THEN TRY (ACCEPT_TAC TRUTH)) g (*****************************************************************************) (* REWRITE IMPLICATIONAL CONVERSION *) (*****************************************************************************) (* Given a theorem [H1,...,Hn |- P ==> l = r], * returns the variables that occur in [P] and [r] but not in the rest. * Basically represents the variables that are introduced by the implicational * rewrite (similar status as variables occurring in the r.h.s. of a rewrite * but not in the l.h.s.). *) let indep_vars th = let hs,c = dest_thm (SPEC_ALL th) in let p,c = dest_imp c in let all_vars = union (frees p) (frees (rhs c)) in let dep_vars = union (frees (lhs c)) (freesl hs) in subtract all_vars dep_vars (* Given a list of variables to avoid [v1,...,vk], a theorem of the form * [hs |- !x1...xn. p ==> !y1...ym. l = r], and a term [t], matches [t] with * [l], yielding the substitution [s], and returns the theorem * [s(hs) |- !z1...zp. s(p) ==> s(l) = s(r)] where [z1], ..., [zp] are the * variables among [x1], ..., [xn], [y1], ..., [ym] that are not instantiated * by [s], and renamed so as to avoid [v1], ..., [vk]. *) let GEN_IMPREWR_CONV avs = let sel = lhs o snd o strip_forall o snd o dest_imp in let pmatch = GEN_PART_MATCH_ALL sel in fun th -> let pmatch' = pmatch th in fun t -> let th' = pmatch' t in VARIANT_RULE avs (GENL (indep_vars th') th') (* A conversion which returns not only a theorem but also a list of terms * which is a sublist of the theorem hypotheses, and a list of terms which * are the variables newly introduced by the conversion. * * See [IMPREWR_CONV] for an example. *) type annot_conv = term -> thm * term option * term list (* Takes a list of variables to avoid [av], a theorem [th] of the form * [h1,..,hk |- !x1...xn. p ==> !y1...ym. l = r], and a term [t] * and returns a conversion with hypotheses defined as follows: * for a term [t], if [t] matches [l] with substitution [s], then return * the theorem [h1,...,hk,s(p) |- t = s(r)] and the the list containing only * [s(p)]. * * The purpose of the conversion with hypothesis is to be able to distinguish * which hypothesis comes from the input theorem and which is added by the * conversion itself. *) let IMPREWR_CONV:Tset.t->thm->annot_conv = fun avs th -> let f t = SPEC_VARS (GEN_IMPREWR_CONV avs th t) in fun t -> let vs,uh = f t in let u = fst (dest_imp (concl uh)) in UNDISCH uh,Some u,Tset.of_list vs let REWR_ANNOTCONV avs th t = let th' = PART_MATCH lhs th t in let _,t' = dest_binary_blind (concl th') in let new_vars = Tset.frees t' in let old_vars = Tset.union (Tset.frees t) (Tset.freesl (hyp th')) in th',None,Tset.subtract new_vars old_vars let ORDER_ANNOTCONV cnv t = let th,_,_ as res = cnv t in let l,r = dest_binary_blind (concl th) in if term_order l r then res else failwith "ORDER_ANNOTCONV" (* Takes a theorem, a net of conversions with hypotheses (which also take * variables to avoid), and adds to the net the conversion corresponding to * the theorem. * * Special cases: * - usual term rewriting is handled with [REWR_CONV] instead of introducing * a fake premise. Might be useful though to introduce a fake premise since * the conversion would benefit from a better handling of variables occurring * in the r.h.s. but not in the l.h.s. * - a theorem of the form [p ==> c] where [c] is not equational is turned into * [p ==> c = T] * - a theorem of the form [p ==> ~c] is turned into [p ==> c = F] *) let pat_cnv_of_thm th : (term * (term list->annot_conv)) = let th = SPEC_ALL th in let lconsts = freesl (hyp th) and c = concl th in match c with |Comb(Comb(Const("=",_),l),r) as t -> let matches = C (can o term_match lconsts) in if free_in l r or (matches l r & matches r l) then t,C REWR_ANNOTCONV (MAP_FORALL_BODY EQT_INTRO th) else l,C REWR_ANNOTCONV th |Comb(Comb(Const("==>",_),p),c) as t -> let matches = C (can o fo_term_match lconsts) in let imprewr_concl f = C IMPREWR_CONV (GEN_MAP_CONCLUSION f th) in (match c with |Comb(Comb(Const("=",_),l),r) -> if free_in l r or (matches l r & matches r l) or is_var l then if matches p c then t, C REWR_ANNOTCONV (EQT_INTRO th) else c, imprewr_concl EQT_INTRO else l, C IMPREWR_CONV th |Comb(Const("~",_),l) -> l, imprewr_concl EQF_INTRO |l -> l, imprewr_concl EQT_INTRO) |Comb(Const("~",_),l) -> l, C REWR_ANNOTCONV (EQF_INTRO th) |Const("T",bool_ty) -> failwith "pat_cnv_of_thm" |l -> l, C REWR_ANNOTCONV (EQT_INTRO th) let impconv_net_of_thm th = try let p,c = pat_cnv_of_thm th in let vs = Tset.freesl (hyp th) in Fo_nets.enter vs (p,(c,vs,th)) with Failure _ -> I let patterns_of_thm = fst o pat_cnv_of_thm (* Apply a conversion net to the term at the top level, taking * avoided variables as parameter too. *) let REWRITES_IMPCONV (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t = tryfind (fun c,_,_ -> c avs t) (Fo_nets.lookup t net) let extra_basic_rewrites = itlist (mk_rewrites false) [NOT_FORALL_THM;NOT_IMP] [] let IMPREWR_CTXCONV :thm list -> (atomic->annot_conv) with_context = let rec top_depth c avs t = let rec (++) c1 c2 avs t = match c1 avs t with |_,Some _,_ as c1t -> c1t |th1,None,vs1 as c1t -> (try let th2,ho2,vs2 = c2 (Tset.union vs1 avs) (rand (concl th1)) in TRANS th1 th2, ho2, Tset.union vs1 vs2 with Failure _ -> c1t) and (+) c1 c2 avs t = try (c1 ++ c2) avs t with Failure _ -> c2 avs t and COMB_QCONV c avs l r = try match c avs l with |th,(Some _ as ho),vs -> AP_THM th r,ho,vs |th1,None,vs1 -> (try let th2,ho2,vs2 = c (Tset.union vs1 avs) r in MK_COMB (th1,th2), ho2, Tset.union vs1 vs2 with Failure _ -> AP_THM th1 r,None,vs1) with Failure _ -> let th2,ho2,vs2 = c avs r in AP_TERM l th2,ho2,vs2 in let SUB_QCONV c avs t = match t with |Comb(l,r) -> COMB_QCONV c avs l r |Abs(v,_) -> let ho = ref None and vs = ref [] in let c' t = let th,ho',vs' = c (Tset.insert avs v) t in ho := ho'; vs := vs'; th in let res = ABS_CONV c' t in res,!ho,!vs |_ -> failwith "SUB_QCONV" in let rec (!) c avs t = (c ++ !c) avs t in (!c + (SUB_QCONV (top_depth c) ++ top_depth c)) avs t in let bigger_net() = itlist (net_of_thm false) extra_basic_rewrites (basic_net()) in let basic_cnv t = REWRITES_CONV (bigger_net ()) t,None,[] in let rec self net ths = let avs = Tset.flat_revmap (Tset.freesl o hyp) ths in let cnv avs t = try REWRITES_IMPCONV net avs t with Failure _ -> basic_cnv t in With_context( (fun a t -> let f = match a with Atomic -> top_depth | Non_atomic -> I in f cnv (Tset.union (Tset.frees t) avs) t), (fun ts -> let ths' = map ASSUME ts in (*let ths'' = ths' @ GMATCH_MPS ths ths' in*) let ths'' = MP_CLOSURE ths' ths' @ ths' @ MP_CLOSURE ths ths' in self (itlist impconv_net_of_thm ths'' net) (ths'' @ ths)), (fun v -> let ths = ref [] in let f (_,vs,th) = if not (Tset.mem v vs) then (ths := th :: !ths; true) else false in let net' = Fo_nets.filter f net in self net' !ths)) in fun ths -> self (itlist impconv_net_of_thm ths Fo_nets.empty_net) ths (*****************************************************************************) (* SOME USEFUL IMPLICATIONAL CONVERSIONS *) (*****************************************************************************) (* Takes a conversion with hypotheses (with context) and makes an * implicational conversion out of it. * Basically turns a rewrite with hypotheses into an implicational rewrite * withouth hypotheses. * Adds existential quantifications for variables introduced by the rewrite. *) let rec REWR_IMPCONV_OF_CONV = let IMP_SYM = REWR_RULE (TAUT `A==>B==>C <=> B==>A==>C`) in let IMP_EXIST = GSYM LEFT_IMP_EXISTS_THM in let TRY_GEN v th = try GEN v th with Failure _ -> th in fun (c:(atomic -> annot_conv) with_context) -> With_context( ((fun a v t -> let th,ho,new_vars = apply c a t in let th1,th2 = EQ_IMP_RULE th in let res = match v with |Co -> let p,th2' = UNDISCH_TERM th2 in let rec exists_intro = function |[] -> DISCH_IMP_IMP (p::list_of_option ho) th2' |v::vs -> let th = exists_intro vs in try REWR_RULE IMP_EXIST (GEN v th) with Failure _ -> th in exists_intro new_vars |Contra -> let th1' = match ho with None -> th1 | Some h -> IMP_SYM (DISCH h th1) in match new_vars with |[] -> th1' |_::_ -> MAP_CONCLUSION (itlist TRY_GEN new_vars) th1' in let t1,t2 = dest_imp (concl res) in if t1 = t2 then raise Unchanged else res):atomic->imp_conv), REWR_IMPCONV_OF_CONV o augment c, REWR_IMPCONV_OF_CONV o diminish c) (* Applies the implicational rewrite, with context simplifications. *) let REWRITE_CTXIMPCONV = DEPTH_CTXIMPCONV o REWR_IMPCONV_OF_CONV o IMPREWR_CTXCONV (*****************************************************************************) (* INTERFACE *) (*****************************************************************************) (* Preprocessor. For now takes a theorem of the form [p ==> c1 /\ ... /\ ck] * and returns the list of theorems [p ==> c1], ..., [p ==> ck]. *) let preprocess = CONJUNCTS o IMPLY_AND (* Tactic for implicational rewrite. *) let IMP_REWRITE_TAC ths = CTXIMPCONV_TAC (REWRITE_CTXIMPCONV (flat (map preprocess ths))) let SEQ_IMP_REWRITE_TAC ths = let cnv = match ths with |[] -> REWRITE_CTXIMPCONV [TRUTH] |[th] -> REWRITE_CTXIMPCONV (preprocess th) |_::_ -> let fcnv = REWRITE_CTXIMPCONV o preprocess in REPEAT_UNCHANGED_CTXIMPCONV (map fcnv ths) in CTXIMPCONV_TAC cnv (* Tactic for implicational rewrite with assumptions. *) let ASM_IMP_REWRITE_TAC = ASM IMP_REWRITE_TAC (* Cases-like conversion for implicational theorems, i.e., for a theorem of * the form: * [h1,..,hk |- !x1...xn. p ==> !y1...ym. l = r], and a term [t], * return [(p ==> t') /\ (~p ==> t)], where [t'] is the result of rewriting * [t] by [l=r]. *) let rec CASE_REWR_IMPCONV_OF_CONV = let MP_TAUT th = MATCH_MP (TAUT th) in let MP_LEM1 = MP_TAUT `(~P ==> Q = R) ==> (Q <=> (~P ==> R) /\ (P ==> Q))` in let MP_LEM2 = MP_TAUT `(P ==> Q = R) ==> (Q <=> (P ==> R) /\ (~P ==> Q))` in fun (c:(atomic -> annot_conv) with_context) -> With_context( (fun a v t -> match apply c a t with |_,None,_ -> failwith "CASE_REWR_IMPCONV_OF_CONV" |th,Some h,_ -> let th' = DISCH h th in let th'' = try MP_LEM1 th' with Failure _ -> MP_LEM2 th' in imp_conv_of_conv (REWR_CONV th'') v t), CASE_REWR_IMPCONV_OF_CONV o augment c, CASE_REWR_IMPCONV_OF_CONV o diminish c) let CASE_REWRITE_CTXIMPCONV = ONCE_DEPTH_CTXIMPCONV o CASE_REWR_IMPCONV_OF_CONV o IMPREWR_CTXCONV (* Tactic version of it. *) let CASE_REWRITE_TAC = CTXIMPCONV_TAC o CASE_REWRITE_CTXIMPCONV o preprocess (*****************************************************************************) (* IMPLICATIONAL CONVERSIONS WITH MULTIPLE RESULTS *) (*****************************************************************************) (* Multiple implicational conversion. *) type imp_mconv = Variance.t -> term -> thm list let mapply_with_context c ctx v t = map (DISCH_CONJ ctx) (apply (augment c (Tset.strip_conj ctx)) v t) (* Consider two multiple implicational conversions ic1, ic2. * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A], * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C], * then [CONJ_IMPMCONV ic1 ic2 Co (A /\ C)] returns * [B1 /\ C ==> A /\ C; ...; Bk /\ C ==> A /\ C; A /\ D1 ==> A /\ C; ...; Dn * ==> A /\ C]. * * And similarly for the contravariant case. *) let rec CONJ_CTXIMPMCONV (c:imp_mconv with_context) : imp_mconv with_context = With_context( (fun v t -> let t1,t2 = dest_conj t in let left,right = match v with |Co -> MKIMPL_CONJ_CO2_CTXT,MKIMPR_CONJ_CO_CTXT |Contra -> MKIMPL_CONJ_CONTRA_CTXT,MKIMPR_CONJ_CONTRA_CTXT in let th1s = map left (mapply_with_context c t2 v t1) in let th2s = map right (mapply_with_context c t1 v t2) in th1s @ th2s), CONJ_CTXIMPMCONV o augment c, CONJ_CTXIMPMCONV o diminish c) (* Consider two multiple implicational conversions ic1, ic2. * Suppose [ic1 Co A] returns a list [B1 ==> A; ...; Bk ==> A], * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C], * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns * [B1 \/ C ==> A \/ C; ...; Bk \/ C ==> A \/ C; A \/ D1 ==> A \/ C; ...; Dn * ==> A \/ C]. * * And similarly for the contravariant case. *) let rec DISJ_CTXIMPMCONV (c:imp_mconv with_context) : imp_mconv with_context = With_context( (fun v t -> let t1,t2 = dest_disj t in let th1s = map (C MKIMPL_DISJ t2) (apply c v t1) in let th2s = map (MKIMPR_DISJ t1) (apply c v t2) in th1s @ th2s), DISJ_CTXIMPMCONV o augment c, DISJ_CTXIMPMCONV o diminish c) (* Consider two multiple implicational conversions ic1, ic2. * Suppose [ic1 Contra A] returns a list [A ==> B1; ...; A ==> Bk], * and [ic2 Co C] returns [D1 ==> C; ...; Dn ==> C], * then [DISJ_IMPMCONV ic1 ic2 Co (A \/ C)] returns * [(B1 ==> C) ==> (A ==> C); ...; (Bk ==> C) ==> (A ==> C); (A ==> D1) ==> (A * ==> C); ...; (A ==> Dn) ==> (A ==> C)]. * * And similarly for the contravariant case. *) let rec IMP_CTXIMPMCONV (c:imp_mconv with_context) : imp_mconv with_context = With_context( (fun v t -> let t1,t2 = dest_imp t in let th1s = map (C MKIMPL_IMP t2) (apply c (Variance.neg v) t1) in let th2s = map MKIMPR_IMP_CTXT (mapply_with_context c t1 v t2) in th1s @ th2s), CONJ_CTXIMPMCONV o augment c, CONJ_CTXIMPMCONV o diminish c) let rec IFF_CTXIMPCONV (c:imp_mconv with_context) = With_context( ((fun v t -> let t1,t2 = dest_iff t in let left,right = match v with |Co -> MKIMPL_CO_IFF,MKIMPR_CO_IFF |Contra -> MKIMPL_CONTRA_IFF,MKIMPR_CONTRA_IFF in let th1s = map left (apply c v (mk_imp(t1,t2))) in let th2s = map right (apply c v (mk_imp(t2,t1))) in th1s @ th2s):imp_mconv), IFF_CTXIMPCONV o augment c, IFF_CTXIMPCONV o diminish c) (* Consider one multiple implicational conversion ic. * Suppose [ic Contra A] returns a list [A ==> B1; ...; A ==> Bk], * then [NOT_IMPMCONV ic Co ~A] returns [~B1 ==> ~A; ...; ~Bk ==> ~A]. * * And similarly for the contravariant case. *) let rec NOT_CTXIMPMCONV (c:imp_mconv with_context) : imp_mconv with_context = With_context( (fun v t -> map MKIMP_NOT (try_list (apply c (Variance.neg v)) (dest_neg t))), NOT_CTXIMPMCONV o augment c, NOT_CTXIMPMCONV o diminish c) let rec QUANT_CTXIMPMCONV mkimp sel (c:imp_mconv with_context) : imp_mconv with_context = With_context( (fun v t -> let x,b = sel t in let c' = diminish c x in map (mkimp x) (try_list (apply c' v) b)), QUANT_CTXIMPMCONV mkimp sel o augment c, QUANT_CTXIMPMCONV mkimp sel o diminish c) (* Consider one multiple implicational conversion ic. * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A], * then [FORALL_IMPMCONV ic Co (!x.A)] returns [(!x.B1) ==> (!x.A); ...; * (!x.Bk) ==> (!x.A)]. * * And similarly for the contravariant case. *) let FORALL_CTXIMPMCONV = QUANT_CTXIMPMCONV MKIMP_FORALL dest_forall (* Consider one multiple implicational conversion ic. * Suppose [ic Co A] returns a list [B1 ==> A; ...; Bk ==> A], * then [EXISTS_IMPMCONV ic Co (?x.A)] returns [(?x.B1) ==> (?x.A); ...; * (?x.Bk) ==> (?x.A)]. * * And similarly for the contravariant case. *) let EXISTS_CTXIMPMCONV = QUANT_CTXIMPMCONV MKIMP_EXISTS dest_exists (* Applies a multiple implicational conversion on the subformula(s) of the * input term *) let rec SUB_CTXIMPMCONV = let iff_ty = `:bool->bool->bool` in fun c -> With_context( ((fun v t -> let n,ty = dest_const (fst (strip_comb t)) in apply ((match n with |"==>" -> IMP_CTXIMPMCONV |"/\\" -> CONJ_CTXIMPMCONV |"\\/" -> DISJ_CTXIMPMCONV |"!" -> FORALL_CTXIMPMCONV |"?" -> EXISTS_CTXIMPMCONV |"~" -> NOT_CTXIMPMCONV |"=" when ty = iff_ty -> IFF_CTXIMPCONV |_ -> failwith "SUB_CTXIMPMCONV") c) v t):imp_mconv), SUB_CTXIMPMCONV o augment c, SUB_CTXIMPMCONV o diminish c) (* Applies a multiple implicational conversion once to the first suitable sub-term(s) * encountered in bottom-up order. *) let rec DEPTH_CTXIMPMCONV (c : (atomic->imp_mconv) with_context) = With_context( (fun v t -> try let ths = apply (SUB_CTXIMPMCONV (DEPTH_CTXIMPMCONV c)) v t in apply c Non_atomic v t @ ths with Failure "SUB_CTXIMPMCONV" -> (apply c Atomic v t)), DEPTH_CTXIMPMCONV o augment c, DEPTH_CTXIMPMCONV o diminish c) (*****************************************************************************) (* REWRITE IMPLICATIONAL CONVERSIONS *) (*****************************************************************************) (* Multiple implicational conversion with hypotheses. *) type annot_mconv = term -> (thm * term option * term list) list (* Takes a theorem, a net of conversions with hypotheses (which also take * variables to avoid), and adds to the net the conversion corresponding to * the theorem. * * Special cases: * - usual term rewriting is handled with [REWR_CONV] instead of introducing * a fake premise. Might be useful though to introduce a fake premise since * the conversion would benefit from a better handling of variables occurring * in the r.h.s. but not in the l.h.s. * - a theorem of the form [p ==> c] where [c] is not equational is turned into * [p ==> c = T] * - a theorem of the form [p ==> ~c] is turned into [p ==> c = F] *) let target_pat_cnv_of_thm th : (term * (term list->annot_conv)) = let th = SPEC_ALL th in match concl th with |Comb(Comb(Const("=",_),l),_) -> l,C REWR_ANNOTCONV th |Comb(Comb(Const("==>",_),_),c) -> let pat,th' = match c with |Comb(Comb(Const("=",_),l),_) -> l, th |Comb(Const("~",_),l) -> l, GEN_MAP_CONCLUSION EQF_INTRO th |l -> c, GEN_MAP_CONCLUSION EQT_INTRO th in pat, C IMPREWR_CONV th' |Comb(Const("~",_),l) -> l, C REWR_ANNOTCONV (EQF_INTRO th) |Const("T",bool_ty) -> failwith "target_pat_cnv_of_thm" |l -> l, C REWR_ANNOTCONV (EQT_INTRO th) let target_impconv_net_of_thm th = try let p,c = target_pat_cnv_of_thm th in let vs = Tset.freesl (hyp th) in Fo_nets.enter vs (p,(c,vs,th)) with Failure _ -> I let target_patterns_of_thm = fst o target_pat_cnv_of_thm (* Multiple conversion which returns all the possible rewrites (on one subterm * only) by one theorem. *) let DEEP_IMP_REWR_MCONV:thm list->(atomic->annot_mconv) with_context = let map_fst f (x,y,z) = f x,y,z in let COMB_MCONV c l r = map (map_fst (C AP_THM r)) (c l) @ map (map_fst (AP_TERM l)) (c r) and ABS_MCONV c v b = let ths = c b in try map (map_fst (ABS v)) ths with Failure _ -> let gv = genvar(type_of v) in let f (gth,ho,vs) = let gtm = concl gth in let l,r = dest_eq gtm in let v' = variant (frees gtm) v in let l' = alpha v' l and r' = alpha v' r in EQ_MP (ALPHA gtm (mk_eq(l',r'))) gth,ho,vs in let b' = vsubst[gv,v] b in map f (map (map_fst (ABS gv)) (c b')) in let SUB_MCONV c = function |Comb(l,r) -> COMB_MCONV c l r |Abs(v,b) -> ABS_MCONV c v b |Const _ | Var _ -> [] in let rec top_depth c t = SUB_MCONV (top_depth c) t @ c t in let REWRITES_IMPCONV (net:((term list -> annot_conv) * Tset.t * thm) Fo_nets.t) avs t = mapfilter (fun c,_,_ -> c avs t) (Fo_nets.lookup t net) in let rec self net ths = let avs = Tset.flat_revmap (Tset.freesl o hyp) ths in With_context( (fun a t -> let avs' = Tset.union (Tset.frees t) avs in let cnv t = REWRITES_IMPCONV net avs' t in let f = match a with |Atomic -> top_depth |Non_atomic -> (fun cnv avs -> cnv avs) in f cnv t), (fun _ -> self net ths), (fun v -> let ths = ref [] in let f (_,vs,th) = if not (Tset.mem v vs) then (ths := th :: !ths; true) else false in let net' = Fo_nets.filter f net in self net' !ths)) in fun ths -> self (itlist target_impconv_net_of_thm ths Fo_nets.empty_net) ths (* Takes a multiple conversion with hypotheses (which also takes a context as * parameter) and makes a multiple implicational conversion out of it. * * Basically extends [GENERAL_REWRITE_IMPCONV] to the multiple conversion * case. *) let rec REWR_IMPMCONV_OF_MCONV = let IMP_SYM = REWR_RULE (TAUT `A==>B==>C <=> B==>A==>C`) in let IMP_EXIST = GSYM LEFT_IMP_EXISTS_THM in let TRY_GEN v th = try GEN v th with Failure _ -> th in fun (c:(atomic -> annot_mconv) with_context) -> With_context( ((fun a v t -> let f (th,ho,new_vars) = let th1,th2 = EQ_IMP_RULE th in match v with |Co -> let p,th2' = UNDISCH_TERM th2 in let rec exists_intro = function |[] -> DISCH_IMP_IMP (p::list_of_option ho) th2' |v::vs -> let th = exists_intro vs in try REWR_RULE IMP_EXIST (GEN v th) with Failure _ -> th in exists_intro new_vars |Contra -> let th1' = match ho with None -> th1 | Some h -> IMP_SYM (DISCH h th1) in match new_vars with |[] -> th1' |_::_ -> MAP_CONCLUSION (itlist TRY_GEN new_vars) th1' in map f (apply c a t)):atomic->imp_mconv), REWR_IMPMCONV_OF_MCONV o augment c, REWR_IMPMCONV_OF_MCONV o diminish c) (*****************************************************************************) (* TARGET REWRITING *) (*****************************************************************************) let EXISTS_CTXIMPCONV:imp_conv with_context = let EXISTSs i p = let codom,dom = unzip i in let f i ps = vsubst [i] (snd (dest_exists (hd ps))) :: ps in let h::ps = rev_itlist f i [list_mk_exists(dom,p)] in rev_itlist EXISTS (zip ps (rev codom)) (ASSUME h) in let LEFT_FORALL_IMP = REWR_RULE LEFT_FORALL_IMP_THM in let rec self ts = With_context ((fun v t -> match v,t with |Co,Comb(Const("?",_),_) -> let vs,b = strip_exists t in let bs = strip_conj b in let hmatch (n,b) = match partition (C mem vs) (variables b) with |[],_ -> failwith "EXISTS_CTXIMPCONV" |_::_ as lvs,lcs -> fun h -> match term_match lcs b h with |_,i,j when filter (uncurry (<>)) j = [] -> (if i = [] then zip lvs lvs else i),n |_ -> failwith "EXISTS_CTXIMPCONV" in let s,n = tryfind_fun (mapfilteri (curry (tryfind o hmatch)) bs) ts in let th = EXISTSs (map (fun v -> rev_assocd v s v,v) vs) b in let th' = DISCH_HD th in let h = fst (dest_imp (concl th')) in (match strip_conj h with |[] -> assert false |[h] -> DISCH T_ th |_::_ as hs -> let hs1,h'::hs2 = chop_list n hs in let hs_th = CONJ_ACI_RULE (mk_eq(h,list_mk_conj (h'::(hs1@hs2)))) in let th1 = CONV_RULE (LAND_CONV (REWR_CONV hs_th)) th' in let th2 = UNDISCH (CONV_RULE (REWR_CONV IMP_CONJ) th1) in let vs' = subtract vs (map snd s) in let f v th = try LEFT_FORALL_IMP (GEN v th) with Failure _ -> th in itlist f vs' th2) |_ -> failwith "EXISTS_CTXIMPCONV"), (fun ts' -> self (Tset.union ts' ts)), (fun _ -> self ts)) in self [] (* Takes a theorem which results of an implicational conversion and applies a * multiple implicational conversion on the outcome. *) let bind_impmconv (c:imp_mconv) v th = let t1,t2 = dest_imp (concl th) in match v with |Co -> map (C IMP_TRANS th) (c v t1) |Contra -> map (IMP_TRANS th) (c v t2) (* Target rewrite implicational conversion: * [TARGET_REWRITE_IMPCONV sths ts] is an implicational conversion which * applies all the possible implicational rewrites on the input term until * one of the resulting terms matches one of the terms in [ts]. * * Note that we allow several target terms and not just one. See * TARGET_REWRITE_TAC for a justification. *) let TARGET_REWRITE_IMPCONV : thm list -> term list -> imp_conv = let PRE = apply (TRY_CTXIMPCONV (REWRITE_CTXIMPCONV [])) in let POST = TRY_CTXIMPCONV (TOP_DEPTH_CTXIMPCONV EXISTS_CTXIMPCONV) in fun sths -> let one_step_sths v uh = let pre v th = try bind_impconv PRE v th with Unchanged -> th in let post v = bind_ctximpconv POST v in let f = DEPTH_CTXIMPMCONV o REWR_IMPMCONV_OF_MCONV o DEEP_IMP_REWR_MCONV in map (post v) (bind_impmconv (apply (f sths)) v (pre v uh)) in let flat l = uniq (itlist (merge thm_lt) l []) in fun ts v t -> let rec self ths = let pool = flat (map (mergesort thm_lt o one_step_sths v) ths) in let sel th = imp_conv_outcome th v in let is_one_sol g = (can o find_term o can o fo_term_match []) g o sel in let is_sol th = tryfind is_one_sol ts th in try bind_ctximpconv POST v (find is_sol pool) with _ -> match pool with |[] -> failwith "TARGET_REWRITE_IMPCONV: no path found" |_::_ -> self (map (bind_ctximpconv POST v) pool) in self [IMP_REFL t] (* Tactic version of it. * * Since the target theorem is preprocessed, it can yield several theorems. * Therefore, there is not just one possible target pattern but several. *) let TARGET_REWRITE_TAC sths th = let sths' = flat (map preprocess sths) in let ths = preprocess th and (+) = THEN_IMPCONV in IMPCONV_TAC (TARGET_REWRITE_IMPCONV sths' (map patterns_of_thm ths) + imp_conv_of_ctx_imp_conv (REWRITE_CTXIMPCONV ths)) let HINT_EXISTS_TAC = CTXIMPCONV_TAC (TOP_DEPTH_CTXIMPCONV EXISTS_CTXIMPCONV) end in Impconv.IMP_REWRITE_TAC, Impconv.TARGET_REWRITE_TAC, Impconv.HINT_EXISTS_TAC, Impconv.SEQ_IMP_REWRITE_TAC, Impconv.CASE_REWRITE_TAC;;