https://github.com/JacquesCarette/hol-light
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
impconv.ml
(* ========================================================================= *)
(* 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> *)
(* *)
(* Distributed under the same license as HOL Light. *)
(* ========================================================================= *)
needs "quot.ml";;
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
|Quote (_) -> acc
|Abs(v,b) -> remove (frees acc b) v
|Comb(u,v) -> frees (frees acc u) v
|Eval(e,ty) -> acc
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
|Quote_ of t
|Hole_ of t * hol_type
|Eval_ of t * hol_type
let type_of = function
|Var_(_,ty) -> ty
|Const_(_,ty,_) -> ty
|Comb_(_,_,ty) -> ty
|Abs_(_,_,ty) -> ty
|Quote_(_) -> mk_type("epsilon",[])
|Hole_(_,ty) -> ty
|Eval_(_,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'))
|Quote(e) -> Quote_(of_term e)
|Hole(e,ty) -> Hole_(of_term e,ty)
|Eval(e,ty) -> Eval_(of_term e,ty)
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
|Quote_(e1),Quote_(e2) -> equal e1 e2
|Hole_(e1,ty1),Hole_(e2,ty2) -> equal e1 e2
|Eval_(e1,ty1_),Eval_(e2,ty2) -> equal e1 e2
|_ -> 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)
|Quote_(e) -> mk_quote(to_term e)
|Hole_(e,ty) -> mk_hole(to_term e,ty)
|Eval_(e,ty) -> mk_eval(to_term e,ty)
let dummy = Var_("",aty)
let rec find_term p t =
if p t then t else
match t with
|Eval_ _ -> failwith "Annot.find_term"
|Quote_ _ -> failwith "Annot.find_term"
|Hole_ _ -> failwith "Annot.find_term"
|Var_ _ -> failwith "Annot.find_term"
|Const_ _ -> failwith "Annot.find_term"
|Abs_(_,b,_) -> find_term p b
|Comb_(u,v,_) -> try find_term p u with Failure _ -> find_term p v
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 module Fo_nets =
struct
type term_label =
|Vnet of int
|Lcnet of string * int
|Cnet of string * int
|Lnet of int
|Qnet of hol_type
|Enet of hol_type
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
|Eval(e,ty) -> Enet(ty),args
|Quote(e) -> Qnet(ep_ty),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
|Quote (e) -> Qnet(ep_ty),args
|Eval (e,ty) -> Enet(ty),args
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 || (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 || (matches l r && matches r l) || 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 _ | Quote _ -> []
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;;