lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
(* Title: TFL/rules.ML
ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
Emulation of HOL inference rules for TFL
*)
signature RULES =
sig
val dest_thm : thm -> term list * term
(* Inference rules *)
val REFL :cterm -> thm
val ASSUME :cterm -> thm
val MP :thm -> thm -> thm
val MATCH_MP :thm -> thm -> thm
val CONJUNCT1 :thm -> thm
val CONJUNCT2 :thm -> thm
val CONJUNCTS :thm -> thm list
val DISCH :cterm -> thm -> thm
val UNDISCH :thm -> thm
val SPEC :cterm -> thm -> thm
val ISPEC :cterm -> thm -> thm
val ISPECL :cterm list -> thm -> thm
val GEN :cterm -> thm -> thm
val GENL :cterm list -> thm -> thm
val LIST_CONJ :thm list -> thm
val SYM : thm -> thm
val DISCH_ALL : thm -> thm
val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
val SPEC_ALL : thm -> thm
val GEN_ALL : thm -> thm
val IMP_TRANS : thm -> thm -> thm
val PROVE_HYP : thm -> thm -> thm
val CHOOSE : cterm * thm -> thm -> thm
val EXISTS : cterm * cterm -> thm -> thm
val EXISTL : cterm list -> thm -> thm
val IT_EXISTS : (cterm*cterm) list -> thm -> thm
val EVEN_ORS : thm list -> thm list
val DISJ_CASESL : thm -> thm list -> thm
val list_beta_conv : cterm -> cterm list -> thm
val SUBS : thm list -> thm -> thm
val simpl_conv : simpset -> thm list -> cterm -> thm
val rbeta : thm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
val term_ref : term list ref
val thm_ref : thm list ref
val ss_ref : simpset list ref
val tracing : bool ref
val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
-> thm -> thm * term list
val RIGHT_ASSOC : thm -> thm
val prove : bool -> cterm * tactic -> thm
end;
structure Rules: RULES =
struct
structure S = USyntax;
structure U = Utils;
structure D = Dcterm;
fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
fun dest_thm thm =
let val {prop,hyps,...} = Thm.rep_thm thm
in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end
handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
(* Inference rules *)
(*---------------------------------------------------------------------------
* Equality (one step)
*---------------------------------------------------------------------------*)
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
fun SYM thm = thm RS sym
handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
fun ALPHA thm ctm1 =
let
val ctm2 = Thm.cprop_of thm;
val ctm2_eq = Thm.reflexive ctm2;
val ctm1_eq = Thm.reflexive ctm1;
in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
fun rbeta th =
(case D.strip_comb (cconcl th) of
(_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
| _ => raise RULES_ERR "rbeta" "");
(*----------------------------------------------------------------------------
* Implication and the assumption list
*
* Assumptions get stuck on the meta-language assumption list. Implications
* are in the object language, so discharging an assumption "A" from theorem
* "B" results in something that looks like "A --> B".
*---------------------------------------------------------------------------*)
fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
(*---------------------------------------------------------------------------
* Implication in TFL is -->. Meta-language implication (==>) is only used
* in the implementation of some of the inference rules below.
*---------------------------------------------------------------------------*)
fun MP th1 th2 = th2 RS (th1 RS mp)
handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
(*forces the first argument to be a proposition if necessary*)
fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
fun DISCH_ALL thm = U.itlist DISCH (#hyps (Thm.crep_thm thm)) thm;
fun FILTER_DISCH_ALL P thm =
let fun check tm = P (#t (Thm.rep_cterm tm))
in foldr (fn (tm,th) => if check tm then DISCH tm th else th)
(chyps thm, thm)
end;
(* freezeT expensive! *)
fun UNDISCH thm =
let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
(*----------------------------------------------------------------------------
* Conjunction
*---------------------------------------------------------------------------*)
fun CONJUNCT1 thm = thm RS conjunct1
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
fun CONJUNCT2 thm = thm RS conjunct2
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
| LIST_CONJ [th] = th
| LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
(*----------------------------------------------------------------------------
* Disjunction
*---------------------------------------------------------------------------*)
local val {prop,sign,...} = rep_thm disjI1
val [P,Q] = term_vars prop
val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1
in
fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
local val {prop,sign,...} = rep_thm disjI2
val [P,Q] = term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2
in
fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
end;
(*----------------------------------------------------------------------------
*
* A1 |- M1, ..., An |- Mn
* ---------------------------------------------------
* [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
*
*---------------------------------------------------------------------------*)
fun EVEN_ORS thms =
let fun blue ldisjs [] _ = []
| blue ldisjs (th::rst) rdisjs =
let val tail = tl rdisjs
val rdisj_tl = D.list_mk_disj tail
in U.itlist DISJ2 ldisjs (DISJ1 th rdisj_tl)
:: blue (ldisjs @ [cconcl th]) rst tail
end handle U.ERR _ => [U.itlist DISJ2 ldisjs th]
in blue [] thms (map cconcl thms) end;
(*----------------------------------------------------------------------------
*
* A |- P \/ Q B,P |- R C,Q |- R
* ---------------------------------------------------
* A U B U C |- R
*
*---------------------------------------------------------------------------*)
fun DISJ_CASES th1 th2 th3 =
let
val c = D.drop_prop (cconcl th1);
val (disj1, disj2) = D.dest_disj c;
val th2' = DISCH disj1 th2;
val th3' = DISCH disj2 th3;
in
th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
end;
(*-----------------------------------------------------------------------------
*
* |- A1 \/ ... \/ An [A1 |- M, ..., An |- M]
* ---------------------------------------------------
* |- M
*
* Note. The list of theorems may be all jumbled up, so we have to
* first organize it to align with the first argument (the disjunctive
* theorem).
*---------------------------------------------------------------------------*)
fun organize eq = (* a bit slow - analogous to insertion sort *)
let fun extract a alist =
let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
| ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
in ex ([],alist)
end
fun place [] [] = []
| place (a::rst) alist =
let val (item,next) = extract a alist
in item::place rst next
end
| place _ _ = raise RULES_ERR "organize" "not a permutation.2"
in place
end;
(* freezeT expensive! *)
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
aconv term_of atm)
(#hyps(rep_thm th))
val tml = D.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
| DL th [th1,th2] = DISJ_CASES th th1 th2
| DL th (th1::rst) =
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
in DL (freezeT disjth) (organize eq tml thl)
end;
(*----------------------------------------------------------------------------
* Universals
*---------------------------------------------------------------------------*)
local (* this is fragile *)
val {prop,sign,...} = rep_thm spec
val x = hd (tl (term_vars prop))
val (TVar (indx,_)) = type_of x
val gspec = forall_intr (cterm_of sign x) spec
in
fun SPEC tm thm =
let val {sign,T,...} = rep_cterm tm
val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec
in
thm RS (forall_elim tm gspec')
end
end;
fun SPEC_ALL thm = U.rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm;
val ISPEC = SPEC
val ISPECL = U.rev_itlist ISPEC;
(* Not optimized! Too complicated. *)
local val {prop,sign,...} = rep_thm allI
val [P] = add_term_vars (prop, [])
fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty))
fun ctm_theta s = map (fn (i,tm2) =>
let val ctm2 = cterm_of s tm2
in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2)
end)
fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta,
ctm_theta s tm_theta)
in
fun GEN v th =
let val gth = forall_intr v th
val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
val tsig = Sign.tsig_of sign
val theta = Pattern.match tsig (P,P')
val allI2 = instantiate (certify sign theta) allI
val thm = Thm.implies_elim allI2 gth
val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
val prop' = tp $ (A $ Abs(x,ty,M))
in ALPHA thm (cterm_of sign prop')
end
end;
val GENL = U.itlist GEN;
fun GEN_ALL thm =
let val {prop,sign,...} = rep_thm thm
val tycheck = cterm_of sign
val vlist = map tycheck (add_term_vars (prop, []))
in GENL vlist thm
end;
fun MATCH_MP th1 th2 =
if (D.is_forall (D.drop_prop(cconcl th1)))
then MATCH_MP (th1 RS spec) th2
else MP th1 th2;
(*----------------------------------------------------------------------------
* Existentials
*---------------------------------------------------------------------------*)
(*---------------------------------------------------------------------------
* Existential elimination
*
* A1 |- ?x.t[x] , A2, "t[v]" |- t'
* ------------------------------------ (variable v occurs nowhere)
* A1 u A2 |- t'
*
*---------------------------------------------------------------------------*)
fun CHOOSE (fvar, exth) fact =
let
val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
val redex = D.capply lam fvar
val {sign, t = t$u,...} = Thm.rep_cterm redex
val residue = Thm.cterm_of sign (betapply (t, u))
in
GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
local val {prop,sign,...} = rep_thm exI
val [P,x] = term_vars prop
in
fun EXISTS (template,witness) thm =
let val {prop,sign,...} = rep_thm thm
val P' = cterm_of sign P
val x' = cterm_of sign x
val abstr = #2 (D.dest_comb template)
in
thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
end
end;
(*----------------------------------------------------------------------------
*
* A |- M
* ------------------- [v_1,...,v_n]
* A |- ?v1...v_n. M
*
*---------------------------------------------------------------------------*)
fun EXISTL vlist th =
U.itlist (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
vlist th;
(*----------------------------------------------------------------------------
*
* A |- M[x_1,...,x_n]
* ---------------------------- [(x |-> y)_1,...,(x |-> y)_n]
* A |- ?y_1...y_n. M
*
*---------------------------------------------------------------------------*)
(* Could be improved, but needs "subst_free" for certified terms *)
fun IT_EXISTS blist th =
let val {sign,...} = rep_thm th
val tych = cterm_of sign
val detype = #t o rep_cterm
val blist' = map (fn (x,y) => (detype x, detype y)) blist
fun ?v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
in
U.itlist (fn (b as (r1,r2)) => fn thm =>
EXISTS(?r2(subst_free[b]
(HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
thm)
blist' th
end;
(*---------------------------------------------------------------------------
* Faster version, that fails for some as yet unknown reason
* fun IT_EXISTS blist th =
* let val {sign,...} = rep_thm th
* val tych = cterm_of sign
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
* in
* fold (fn (b as (r1,r2), thm) =>
* EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))),
* r1) thm) blist th
* end;
*---------------------------------------------------------------------------*)
(*----------------------------------------------------------------------------
* Rewriting
*---------------------------------------------------------------------------*)
fun SUBS thl =
rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl);
val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE));
fun simpl_conv ss thl ctm =
rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq;
val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc];
(*---------------------------------------------------------------------------
* TERMINATION CONDITION EXTRACTION
*---------------------------------------------------------------------------*)
(* Object language quantifier, i.e., "!" *)
fun Forall v M = S.mk_forall{Bvar=v, Body=M};
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
fun is_cong thm =
let val {prop, ...} = rep_thm thm
in case prop
of (Const("==>",_)$(Const("Trueprop",_)$ _) $
(Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
| _ => true
end;
fun dest_equal(Const ("==",_) $
(Const ("Trueprop",_) $ lhs)
$ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = S.dest_eq tm;
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
| dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
val is_all = can (dest_all []);
fun strip_all used fm =
if (is_all fm)
then let val ({Bvar, Body}, used') = dest_all used fm
val (bvs, core, used'') = strip_all used' Body
in ((Bvar::bvs), core, used'')
end
else ([], fm, used);
fun break_all(Const("all",_) $ Abs (_,_,body)) = body
| break_all _ = raise RULES_ERR "break_all" "not a !!";
fun list_break_all(Const("all",_) $ Abs (s,ty,body)) =
let val (L,core) = list_break_all body
in ((s,ty)::L, core)
end
| list_break_all tm = ([],tm);
(*---------------------------------------------------------------------------
* Rename a term of the form
*
* !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
* ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
* to one of
*
* !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
* ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
*
* This prevents name problems in extraction, and helps the result to read
* better. There is a problem with varstructs, since they can introduce more
* than n variables, and some extra reasoning needs to be done.
*---------------------------------------------------------------------------*)
fun get ([],_,L) = rev L
| get (ant::rst,n,L) =
case (list_break_all ant)
of ([],_) => get (rst, n+1,L)
| (vlist,body) =>
let val eq = Logic.strip_imp_concl body
val (f,args) = S.strip_comb (get_lhs eq)
val (vstrl,_) = S.strip_abs f
val names = variantlist (map (#1 o dest_Free) vstrl,
add_term_names(body, []))
in get (rst, n+1, (names,n)::L) end
handle TERM _ => get (rst, n+1, L)
| U.ERR _ => get (rst, n+1, L);
(* Note: rename_params_rule counts from 1, not 0 *)
fun rename thm =
let val {prop,sign,...} = rep_thm thm
val tych = cterm_of sign
val ants = Logic.strip_imp_prems prop
val news = get (ants,1,[])
in
U.rev_itlist rename_params_rule news thm
end;
(*---------------------------------------------------------------------------
* Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
*---------------------------------------------------------------------------*)
fun list_beta_conv tm =
let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th))))
fun iter [] = Thm.reflexive tm
| iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v))
in iter end;
(*---------------------------------------------------------------------------
* Trace information for the rewriter
*---------------------------------------------------------------------------*)
val term_ref = ref[] : term list ref
val ss_ref = ref [] : simpset list ref;
val thm_ref = ref [] : thm list ref;
val tracing = ref false;
fun say s = if !tracing then writeln s else ();
fun print_thms s L =
say (cat_lines (s :: map string_of_thm L));
fun print_cterms s L =
say (cat_lines (s :: map string_of_cterm L));
(*---------------------------------------------------------------------------
* General abstraction handlers, should probably go in USyntax.
*---------------------------------------------------------------------------*)
fun mk_aabs (vstr, body) =
S.mk_abs {Bvar = vstr, Body = body}
handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
fun list_mk_aabs (vstrl,tm) =
U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
fun dest_aabs used tm =
let val ({Bvar,Body}, used') = S.dest_abs used tm
in (Bvar, Body, used') end
handle U.ERR _ =>
let val {varstruct, body, used} = S.dest_pabs used tm
in (varstruct, body, used) end;
fun strip_aabs used tm =
let val (vstr, body, used') = dest_aabs used tm
val (bvs, core, used'') = strip_aabs used' body
in (vstr::bvs, core, used'') end
handle U.ERR _ => ([], tm, used);
fun dest_combn tm 0 = (tm,[])
| dest_combn tm n =
let val {Rator,Rand} = S.dest_comb tm
val (f,rands) = dest_combn Rator (n-1)
in (f,Rand::rands)
end;
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
fun mk_fst tm =
let val ty as Type("*", [fty,sty]) = type_of tm
in Const ("fst", ty --> fty) $ tm end
fun mk_snd tm =
let val ty as Type("*", [fty,sty]) = type_of tm
in Const ("snd", ty --> sty) $ tm end
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =
if (is_Free p)
then tych xocc::L
else let val (p1,p2) = dest_pair p
in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L)
end
in
traverse vstruct x []
end end;
(*---------------------------------------------------------------------------
* Replace a free tuple (vstr) by a universally quantified variable (a).
* Note that the notion of "freeness" for a tuple is different than for a
* variable: if variables in the tuple also occur in any other place than
* an occurrences of the tuple, they aren't "free" (which is thus probably
* the wrong word to use).
*---------------------------------------------------------------------------*)
fun VSTRUCT_ELIM tych a vstr th =
let val L = S.free_vars_lr vstr
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th)
val thm2 = forall_intr_list (map tych L) thm1
val thm3 = forall_elim_list (XFILL tych a vstr) thm2
in refl RS
rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3
end;
fun PGEN tych a vstr th =
let val a1 = tych a
val vstr1 = tych vstr
in
forall_intr a1
(if (is_Free vstr)
then cterm_instantiate [(vstr1,a1)] th
else VSTRUCT_ELIM tych a vstr th)
end;
(*---------------------------------------------------------------------------
* Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
*
* (([x,y],N),vstr)
*---------------------------------------------------------------------------*)
fun dest_pbeta_redex used M n =
let val (f,args) = dest_combn M n
val dummy = dest_aabs used f
in (strip_aabs used f,args)
end;
fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
fun dest_impl tm =
let val ants = Logic.strip_imp_prems tm
val eq = Logic.strip_imp_concl tm
in (ants,get_lhs eq)
end;
fun restricted t = is_some (S.find_term
(fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false)
t)
fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
let val globals = func::G
val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
val tc_list = ref[]: term list ref
val dummy = term_ref := []
val dummy = thm_ref := []
val dummy = ss_ref := []
val cut_lemma' = cut_lemma RS eq_reflection
fun prover used ss thm =
let fun cong_prover ss thm =
let val dummy = say "cong_prover:"
val cntxt = MetaSimplifier.prems_of_ss ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
val dummy = say (string_of_thm thm)
val dummy = thm_ref := (thm :: !thm_ref)
val dummy = ss_ref := (ss :: !ss_ref)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp,sign) =
let val tych = cterm_of sign
val dummy = print_cterms "To eliminate:" [tych imp]
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
val lhs = tych(get_lhs eq)
val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss
val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
handle U.ERR _ => Thm.reflexive lhs
val dummy = print_thms "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
in
lhs_eeq_lhs2 COMP thm
end
fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val dummy = assert (forall (op aconv)
(ListPair.zip (vlist, args)))
"assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
val tych = cterm_of sign
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
val QeqQ1 = pbeta_reduce (tych Q)
val Q1 = #2(D.dest_eq(cconcl QeqQ1))
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
handle U.ERR _ => Thm.reflexive Q1
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
((Q2eeqQ3 RS meta_eq_to_obj_eq)
RS ((thA RS meta_eq_to_obj_eq) RS trans))
RS eq_reflection
val impth = implies_intr_list ants1 QeeqQ3
val impth1 = impth RS meta_eq_to_obj_eq
(* Need to abstract *)
val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
in ant_th COMP thm
end
fun q_eliminate (thm,imp,sign) =
let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
then pq_eliminate (thm,sign,vlist,imp_body,Q)
else
let val tych = cterm_of sign
val ants1 = map tych ants
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
(false,true,false) (prover used') ss' (tych Q)
handle U.ERR _ => Thm.reflexive (tych Q)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
in
ant_th COMP thm
end end
fun eliminate thm =
case (rep_thm thm)
of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
eliminate
(if not(is_all imp)
then uq_eliminate (thm,imp,sign)
else q_eliminate (thm,imp,sign))
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
fun restrict_prover ss thm =
let val dummy = say "restrict_prover:"
val cntxt = rev(MetaSimplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
sign,...} = rep_thm thm
fun genl tm = let val vlist = gen_rems (op aconv)
(add_term_frees(tm,[]), globals)
in U.itlist Forall vlist tm
end
(*--------------------------------------------------------------
* This actually isn't quite right, since it will think that
* not-fully applied occs. of "f" in the context mean that the
* current call is nested. The real solution is to pass in a
* term "f v1..vn" which is a pattern that any full application
* of "f" will match.
*-------------------------------------------------------------*)
val func_name = #1(dest_Const func)
fun is_func (Const (name,_)) = (name = func_name)
| is_func _ = false
val rcontext = rev cntxt
val cncl = HOLogic.dest_Trueprop o Thm.prop_of
val antl = case rcontext of [] => []
| _ => [S.list_mk_conj(map cncl rcontext)]
val TC = genl(S.list_mk_imp(antl, A))
val dummy = print_cterms "func:" [cterm_of sign func]
val dummy = print_cterms "TC:"
[cterm_of sign (HOLogic.mk_Trueprop TC)]
val dummy = tc_list := (TC :: !tc_list)
val nestedp = is_some (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
else let val cTC = cterm_of sign
(HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
| _ => MP (SPEC_ALL (ASSUME cTC))
(LIST_CONJ rcontext)
end
val th'' = th' RS thm
in SOME (th'')
end handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
in
(if (is_cong thm) then cong_prover else restrict_prover) ss thm
end
val ctm = cprop_of th
val names = add_term_names (term_of ctm, [])
val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
(prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
val th2 = equal_elim th1 th
in
(th2, filter (not o restricted) (!tc_list))
end;
fun prove strict (ptm, tac) =
let val result =
if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
else
transform_error (fn () =>
Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
in #1 (freeze_thaw result) end;
end;