diff -r a7282df327c6 -r 70b9b0cfe05f TFL/rules.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/TFL/rules.ML Wed Jan 03 21:20:40 2001 +0100 @@ -0,0 +1,824 @@ +(* Title: TFL/rules.sml + 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 mss_ref : meta_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 : 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 = #tsig(Sign.rep_sg 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); + +local fun rew_conv mss = MetaSimplifier.rewrite_cterm (true,false,false) (K(K None)) mss +in +fun simpl_conv ss thl ctm = + rew_conv (MetaSimplifier.mss_of (#simps (MetaSimplifier.dest_mss (#mss (rep_ss ss))) @ thl)) ctm + RS meta_eq_to_obj_eq +end; + +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 mss_ref = ref [] : meta_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 RS eq_reflection]; + val tc_list = ref[]: term list ref + val dummy = term_ref := [] + val dummy = thm_ref := [] + val dummy = mss_ref := [] + val cut_lemma' = cut_lemma RS eq_reflection + fun prover used mss thm = + let fun cong_prover mss thm = + let val dummy = say "cong_prover:" + val cntxt = prems_of_mss mss + 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 = mss_ref := (mss :: !mss_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 mss' = add_prems(mss, map ASSUME ants) + val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' 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 mss' = add_prems(mss, map ASSUME ants1) + val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1 + handle U.ERR _ => Thm.reflexive Q1 + val Q2 = #2 (Logic.dest_equals (#prop(rep_thm 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 mss' = add_prems(mss, map ASSUME ants1) + val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm + (false,true,false) (prover used') mss' (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 mss thm = + let val dummy = say "restrict_prover:" + val cntxt = rev(prems_of_mss mss) + 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 #prop o rep_thm + 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) mss 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) (add_congs(mss_of [cut_lemma'], congs)) ctm + val th2 = equal_elim th1 th + in + (th2, filter (not o restricted) (!tc_list)) + end; + + +fun prove (ptm, tac) = + let val result = + Library.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;