# HG changeset patch # User paulson # Date 924863001 -7200 # Node ID 1ebbe18fe236ea4e21041ede6f126be48eb76023 # Parent 120ca2bb27e1021ce7961af307b33491b3ad9851 Now for recdefs that omit the WF relation; removed the separation between draft and theory modes diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/post.sml --- a/TFL/post.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/post.sml Fri Apr 23 12:23:21 1999 +0200 @@ -23,15 +23,18 @@ val define : theory -> xstring -> string -> string list -> theory * Prim.pattern list + val function_i : theory -> xstring + -> thm list (* congruence rules *) + -> term list -> theory * thm + + val function : theory -> xstring + -> thm list + -> string list -> theory * thm + val simplify_defn : simpset * thm list -> theory * (string * Prim.pattern list) -> {rules:thm list, induct:thm, tcs:term list} - (*------------------------------------------------------------------------- - val function : theory -> term -> {theory:theory, eq_ind : thm} - val lazyR_def: theory -> term -> {theory:theory, eqns : thm} - *-------------------------------------------------------------------------*) - end; @@ -40,216 +43,217 @@ structure Prim = Prim structure S = USyntax -(*--------------------------------------------------------------------------- - * Extract termination goals so that they can be put it into a goalstack, or - * have a tactic directly applied to them. - *--------------------------------------------------------------------------*) -fun termination_goals rules = - map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) - (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); + val trace = Prim.trace + + (*--------------------------------------------------------------------------- + * Extract termination goals so that they can be put it into a goalstack, or + * have a tactic directly applied to them. + *--------------------------------------------------------------------------*) + fun termination_goals rules = + map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) + (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); -(*--------------------------------------------------------------------------- - * Finds the termination conditions in (highly massaged) definition and - * puts them into a goalstack. + (*--------------------------------------------------------------------------- + * Finds the termination conditions in (highly massaged) definition and + * puts them into a goalstack. + *--------------------------------------------------------------------------*) + fun tgoalw thy defs rules = + case termination_goals rules of + [] => error "tgoalw: no termination conditions to prove" + | L => goalw_cterm defs + (Thm.cterm_of (Theory.sign_of thy) + (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); + + fun tgoal thy = tgoalw thy []; + + (*--------------------------------------------------------------------------- + * Three postprocessors are applied to the definition. It + * attempts to prove wellfoundedness of the given relation, simplifies the + * non-proved termination conditions, and finally attempts to prove the + * simplified termination conditions. *--------------------------------------------------------------------------*) -fun tgoalw thy defs rules = - case termination_goals rules of - [] => error "tgoalw: no termination conditions to prove" - | L => goalw_cterm defs - (Thm.cterm_of (Theory.sign_of thy) - (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); - -fun tgoal thy = tgoalw thy []; - -(*--------------------------------------------------------------------------- -* Three postprocessors are applied to the definition. It -* attempts to prove wellfoundedness of the given relation, simplifies the -* non-proved termination conditions, and finally attempts to prove the -* simplified termination conditions. -*--------------------------------------------------------------------------*) -fun std_postprocessor ss = - Prim.postprocess - {WFtac = REPEAT (ares_tac [wf_empty, wf_measure, wf_inv_image, - wf_lex_prod, wf_less_than, wf_trancl] 1), - terminator = asm_simp_tac ss 1 - THEN TRY(CLASET' (fn cs => best_tac - (cs addSDs [not0_implies_Suc] addss ss)) 1), - simplifier = Rules.simpl_conv ss []}; + fun std_postprocessor ss = + Prim.postprocess + {WFtac = REPEAT (ares_tac [wf_empty, wf_pred_nat, + wf_measure, wf_inv_image, + wf_lex_prod, wf_less_than, wf_trancl] 1), + terminator = asm_simp_tac ss 1 + THEN TRY(CLASET' (fn cs => best_tac + (cs addSDs [not0_implies_Suc] addss ss)) 1), + simplifier = Rules.simpl_conv ss []}; -val concl = #2 o Rules.dest_thm; + val concl = #2 o Rules.dest_thm; -(*--------------------------------------------------------------------------- - * Defining a function with an associated termination relation. - *---------------------------------------------------------------------------*) -fun define_i thy fid R eqs = - let val {functional,pats} = Prim.mk_functional thy eqs - in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats) - end; + (*--------------------------------------------------------------------------- + * Defining a function with an associated termination relation. + *---------------------------------------------------------------------------*) + fun define_i thy fid R eqs = + let val {functional,pats} = Prim.mk_functional thy eqs + in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats) + end; -(*lcp's version: takes strings; doesn't return "thm" - (whose signature is a draft and therefore useless) *) -fun define thy fid R eqs = - let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) - in define_i thy fid (read thy R) (map (read thy) eqs) end - handle Utils.ERR {mesg,...} => error mesg; + fun define thy fid R eqs = + let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) + in define_i thy fid (read thy R) (map (read thy) eqs) end + handle Utils.ERR {mesg,...} => error mesg; (*--------------------------------------------------------------------------- * Postprocess a definition made by "define". This is a separate stage of * processing from the definition stage. *---------------------------------------------------------------------------*) -local -structure R = Rules -structure U = Utils + local + structure R = Rules + structure U = Utils -(* The rest of these local definitions are for the tricky nested case *) -val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl + (* The rest of these local definitions are for the tricky nested case *) + val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl -fun id_thm th = - let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) - in lhs aconv rhs - end handle _ => false + fun id_thm th = + let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) + in lhs aconv rhs + end handle _ => false -fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); -val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; -val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; -fun mk_meta_eq r = case concl_of r of - Const("==",_)$_$_ => r - | _$(Const("op =",_)$_$_) => r RS eq_reflection - | _ => r RS P_imp_P_eq_True + fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); + val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; + val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; + fun mk_meta_eq r = case concl_of r of + Const("==",_)$_$_ => r + | _ $(Const("op =",_)$_$_) => r RS eq_reflection + | _ => r RS P_imp_P_eq_True -(*Is this the best way to invoke the simplifier??*) -fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) + (*Is this the best way to invoke the simplifier??*) + fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) -fun join_assums th = - let val {sign,...} = rep_thm th - val tych = cterm_of sign - val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) - val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) - val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) - val cntxt = gen_union (op aconv) (cntxtl, cntxtr) - in - R.GEN_ALL - (R.DISCH_ALL - (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) - end - val gen_all = S.gen_all -in -fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = - let val dummy = writeln "Proving induction theorem.. " - val ind = Prim.mk_induction theory f R full_pats_TCs - val dummy = writeln "Proved induction theorem.\nPostprocessing.. " - val {rules, induction, nested_tcs} = - std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} - in - case nested_tcs - of [] => (writeln "Postprocessing done."; - {induction=induction, rules=rules,tcs=[]}) - | L => let val dummy = writeln "Simplifying nested TCs.. " - val (solved,simplified,stubborn) = - U.itlist (fn th => fn (So,Si,St) => - if (id_thm th) then (So, Si, th::St) else - if (solved th) then (th::So, Si, St) - else (So, th::Si, St)) nested_tcs ([],[],[]) - val simplified' = map join_assums simplified - val rewr = full_simplify (ss addsimps (solved @ simplified')); - val induction' = rewr induction - and rules' = rewr rules - val dummy = writeln "Postprocessing done." - in - {induction = induction', - rules = rules', - tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) - (simplified@stubborn)} - end - end; + fun join_assums th = + let val {sign,...} = rep_thm th + val tych = cterm_of sign + val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) + val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) + val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) + val cntxt = gen_union (op aconv) (cntxtl, cntxtr) + in + R.GEN_ALL + (R.DISCH_ALL + (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) + end + val gen_all = S.gen_all + in + fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = + let val dummy = writeln "Proving induction theorem.. " + val ind = Prim.mk_induction theory + {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} + val dummy = writeln "Proved induction theorem.\nPostprocessing.. " + val {rules, induction, nested_tcs} = + std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} + in + case nested_tcs + of [] => (writeln "Postprocessing done."; + {induction=induction, rules=rules,tcs=[]}) + | L => let val dummy = writeln "Simplifying nested TCs.. " + val (solved,simplified,stubborn) = + U.itlist (fn th => fn (So,Si,St) => + if (id_thm th) then (So, Si, th::St) else + if (solved th) then (th::So, Si, St) + else (So, th::Si, St)) nested_tcs ([],[],[]) + val simplified' = map join_assums simplified + val rewr = full_simplify (ss addsimps (solved @ simplified')); + val induction' = rewr induction + and rules' = rewr rules + val dummy = writeln "Postprocessing done." + in + {induction = induction', + rules = rules', + tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) + (simplified@stubborn)} + end + end; -(*lcp: curry the predicate of the induction rule*) -fun curry_rule rl = split_rule_var - (head_of (HOLogic.dest_Trueprop (concl_of rl)), - rl); - -(*lcp: put a theorem into Isabelle form, using meta-level connectives*) -val meta_outer = - curry_rule o standard o - rule_by_tactic (REPEAT - (FIRSTGOAL (resolve_tac [allI, impI, conjI] - ORELSE' etac conjE))); + (*lcp: curry the predicate of the induction rule*) + fun curry_rule rl = split_rule_var + (head_of (HOLogic.dest_Trueprop (concl_of rl)), + rl); -(*Strip off the outer !P*) -val spec'= read_instantiate [("x","P::?'b=>bool")] spec; - -val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; + (*lcp: put a theorem into Isabelle form, using meta-level connectives*) + val meta_outer = + curry_rule o standard o + rule_by_tactic (REPEAT + (FIRSTGOAL (resolve_tac [allI, impI, conjI] + ORELSE' etac conjE))); -(*Convert conclusion from = to ==*) -val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); + (*Strip off the outer !P*) + val spec'= read_instantiate [("x","P::?'b=>bool")] spec; -(*--------------------------------------------------------------------------- - * Install the basic context notions. Others (for nat and list and prod) - * have already been added in thry.sml - *---------------------------------------------------------------------------*) -val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong]; + val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; + + (*Convert conclusion from = to ==*) + val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); -fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = - let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy))) - ("Recursive definition " ^ id ^ - " would clash with the theory of the same name!") - val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq - val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs) - val {theory,rules,TCs,full_pats_TCs,patterns} = - Prim.post_definition - (ss', defaultTflCongs @ eq_reflect_list tflCongs) - (thy, (def,pats)) - val {lhs=f,rhs} = S.dest_eq(concl def) - val (_,[R,_]) = S.strip_comb rhs - val {induction, rules, tcs} = - proof_stage ss' theory - {f = f, R = R, rules = rules, - full_pats_TCs = full_pats_TCs, - TCs = TCs} - val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) - in {induct = meta_outer - (normalize_thm [RSspec,RSmp] (induction RS spec')), - rules = rules', - tcs = (termination_goals rules') @ tcs} - end - handle Utils.ERR {mesg,func,module} => - error (mesg ^ - "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); -end; + (*--------------------------------------------------------------------------- + * Install the basic context notions. Others (for nat and list and prod) + * have already been added in thry.sml + *---------------------------------------------------------------------------*) + fun simplify_defn (ss, tflCongs) (thy,(id,pats)) = + let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy))) + ("Recursive definition " ^ id ^ + " would clash with the theory of the same name!") + val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq + val {theory,rules,TCs,full_pats_TCs,patterns} = + Prim.post_definition (Prim.congs tflCongs) + (thy, (def,pats)) + val {lhs=f,rhs} = S.dest_eq(concl def) + val (_,[R,_]) = S.strip_comb rhs + val ss' = ss addsimps Prim.default_simps + val {induction, rules, tcs} = + proof_stage ss' theory + {f = f, R = R, rules = rules, + full_pats_TCs = full_pats_TCs, + TCs = TCs} + val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) + in {induct = meta_outer + (normalize_thm [RSspec,RSmp] (induction RS spec')), + rules = rules', + tcs = (termination_goals rules') @ tcs} + end + handle Utils.ERR {mesg,func,module} => + error (mesg ^ + "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); (*--------------------------------------------------------------------------- * - * Definitions with synthesized termination relation temporarily - * deleted -- it's not clear how to integrate this facility with - * the Isabelle theory file scheme, which restricts - * inference at theory-construction time. - * - -local structure R = Rules -in -fun function theory eqs = - let val dummy = writeln "Making definition.. " - val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs - val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) - val dummy = writeln "Definition made." - val dummy = writeln "Proving induction theorem.. " - val induction = Prim.mk_induction theory f R full_pats_TCs - val dummy = writeln "Induction theorem proved." - in {theory = theory, - eq_ind = standard (induction RS (rules RS conjI))} - end -end; - - -fun lazyR_def theory eqs = - let val {rules,theory, ...} = Prim.lazyR_def theory eqs - in {eqns=rules, theory=theory} - end - handle e => print_exn e; - * + * Definitions with synthesized termination relation * *---------------------------------------------------------------------------*) + + local open USyntax + in + fun func_of_cond_eqn tm = + #1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm))))))) + end; + + fun function_i thy fid congs eqs = + let val dum = Theory.requires thy "WF_Rel" "recursive function definitions" + val {rules,R,theory,full_pats_TCs,SV,...} = + Prim.lazyR_def thy fid congs eqs + val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) + val dummy = writeln "Definition made.\nProving induction theorem.. " + val induction = Prim.mk_induction theory + {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} + val dummy = writeln "Induction theorem proved." + in (theory, + (*return the conjoined induction rule and recursion equations, + with assumptions remaining to discharge*) + standard (induction RS (rules RS conjI))) + end + + fun function thy fid congs seqs = + let val _ = writeln ("Deferred recursive function " ^ fid) + fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) + in function_i thy fid congs (map (read thy) seqs) end + handle Utils.ERR {mesg,...} => error mesg; + + end; + end; diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/rules.new.sml --- a/TFL/rules.new.sml Fri Apr 23 12:22:30 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,784 +0,0 @@ -(* Title: TFL/rules - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Emulation of HOL inference rules for TFL -*) - -structure Rules : Rules_sig = -struct - -open Utils; - -structure USyntax = USyntax; -structure S = USyntax; -structure U = Utils; -structure D = Dcterm; - - -fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg}; - - -fun cconcl thm = D.drop_prop(#prop(crep_thm thm)); -fun chyps thm = map D.drop_prop(#hyps(crep_thm thm)); - -fun dest_thm thm = - let val {prop,hyps,...} = rep_thm thm - in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) - end; - - - -(* Inference rules *) - -(*--------------------------------------------------------------------------- - * Equality (one step) - *---------------------------------------------------------------------------*) -fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq; -fun SYM thm = thm RS sym; - -fun ALPHA thm ctm1 = - let val ctm2 = cprop_of thm - val ctm2_eq = reflexive ctm2 - val ctm1_eq = reflexive ctm1 - in equal_elim (transitive ctm2_eq ctm1_eq) thm - end; - - -(*---------------------------------------------------------------------------- - * typ instantiation - *---------------------------------------------------------------------------*) -fun INST_TYPE blist thm = - let val {sign,...} = rep_thm thm - val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist - in Thm.instantiate (blist',[]) thm - end - handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; - - -(*---------------------------------------------------------------------------- - * 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); - -fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI; - -fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm; - - -fun FILTER_DISCH_ALL P thm = - let fun check tm = U.holds P (#t(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 (freezeT thm)))) - in implies_elim (thm RS mp) (ASSUME tm) - end - handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; - -fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; - -local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)" - val dummy = by (rtac impI 1) - val dummy = by (rtac (p2 RS mp) 1) - val dummy = by (rtac (p1 RS mp) 1) - val dummy = by (assume_tac 1) - val imp_trans = result() -in -fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans) -end; - -(*---------------------------------------------------------------------------- - * Conjunction - *---------------------------------------------------------------------------*) -fun CONJUNCT1 thm = (thm RS conjunct1) -fun CONJUNCT2 thm = (thm RS conjunct2); -fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) - handle _ => [th]; - -fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"} - | LIST_CONJ [th] = th - | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst); - - -(*---------------------------------------------------------------------------- - * Disjunction - *---------------------------------------------------------------------------*) -local val {prop,sign,...} = rep_thm disjI1 - val [P,Q] = term_vars prop - val disj1 = forall_intr (cterm_of sign Q) disjI1 -in -fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1) -end; - -local val {prop,sign,...} = rep_thm disjI2 - val [P,Q] = term_vars prop - val disj2 = forall_intr (cterm_of sign P) disjI2 -in -fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2) -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 itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) - :: blue (ldisjs@[cconcl th]) rst tail - end handle _ => [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 - * - *---------------------------------------------------------------------------*) -local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R" - val dummy = by (rtac (p1 RS disjE) 1) - val dummy = by (rtac (p2 RS mp) 1) - val dummy = by (assume_tac 1) - val dummy = by (rtac (p3 RS mp) 1) - val dummy = by (assume_tac 1) - val tfl_exE = result() -in -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 tfl_exE)) - end -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{func = "organize", - mesg = "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{func = "organize", - mesg = "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{func="DISJ_CASESL",mesg="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 = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm; - -val ISPEC = SPEC -val ISPECL = 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 = 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 = 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' - * - *---------------------------------------------------------------------------*) - -local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q" - val dummy = by (rtac (p1 RS exE) 1) - val dummy = by (rtac ((p2 RS allE) RS mp) 1) - val dummy = by (assume_tac 2) - val dummy = by (assume_tac 1) - val choose_thm = result() -in -fun CHOOSE(fvar,exth) fact = - let val lam = #2(dest_comb(D.drop_prop(cconcl exth))) - val redex = capply lam fvar - val {sign, t = t$u,...} = rep_cterm redex - val residue = cterm_of sign (betapply(t,u)) - in GEN fvar (DISCH residue fact) RS (exth RS choose_thm) - end -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(dest_comb template) - in - thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) - 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 _ => th) thl); - -local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None)) -in -fun simpl_conv ss thl ctm = - rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm - RS meta_eq_to_obj_eq -end; - -local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]) -in -val RIGHT_ASSOC = rewrite_rule [prover"((a|b)|c) = (a|(b|c))" RS eq_reflection] -val ASM = refl RS iffD1 -end; - - - - -(*--------------------------------------------------------------------------- - * 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 ("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(Const("all",_) $ (a as Abs _)) = S.dest_abs a - | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"}; - -val is_all = Utils.can dest_all; - -fun strip_all fm = - if (is_all fm) - then let val {Bvar,Body} = dest_all fm - val (bvs,core) = strip_all Body - in ((Bvar::bvs), core) - end - else ([],fm); - -fun break_all(Const("all",_) $ Abs (_,_,body)) = body - | break_all _ = raise RULES_ERR{func = "break_all", mesg = "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 _ => 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 = transitive th (beta_conversion(#2(D.dest_eq(cconcl th)))) - fun iter [] = reflexive tm - | iter (v::rst) = rbeta (combination(iter rst) (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 _ => 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 tm = - let val {Bvar,Body} = S.dest_abs tm - in (Bvar,Body) - end handle _ => let val {varstruct,body} = S.dest_pabs tm - in (varstruct,body) - end; - -fun strip_aabs tm = - let val (vstr,body) = dest_aabs tm - val (bvs, core) = strip_aabs body - in (vstr::bvs, core) - end - handle _ => ([],tm); - -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[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 M n = - let val (f,args) = dest_combn M n - val dummy = dest_aabs f - in (strip_aabs f,args) - end; - -fun pbeta_redex M n = U.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("cut",_)) =>true | _ => false) - t) - -fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th = - let val pbeta_reduce = simpl_conv 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 mp) RS eq_reflection - fun prover 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 = Thm.rewrite_cterm(false,true,false)mss' prover lhs - handle _ => 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,_),args) = dest_pbeta_redex 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 = Thm.rewrite_cterm (false,true,false) mss' prover Q1 - handle _ => 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 = symmetric(pbeta_reduce Q3 RS eq_reflection) - val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 - val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => - ((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) = strip_all 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 = Thm.rewrite_cterm(false,true,false) mss' - prover (tych Q) - handle _ => 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 _ => None - - 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,[]), [func,R]) - 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{func = "solver", - mesg = "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 _ => None - in - (if (is_cong thm) then cong_prover else restrict_prover) mss thm - end - val ctm = cprop_of th - val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs)) - prover ctm - val th2 = equal_elim th1 th - in - (th2, filter (not o restricted) (!tc_list)) - end; - - - -fun prove (ptm,tac) = - #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac]))); - - -end; (* Rules *) diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/rules.sig --- a/TFL/rules.sig Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/rules.sig Fri Apr 23 12:23:21 1999 +0200 @@ -52,8 +52,8 @@ 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 : simpset * term * term * thm * thm list + val tracing : bool ref + val CONTEXT_REWRITE_RULE : term * term list * thm * thm list -> thm -> thm * term list val RIGHT_ASSOC : thm -> thm diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/rules.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/TFL/rules.sml Fri Apr 23 12:23:21 1999 +0200 @@ -0,0 +1,788 @@ +(* Title: TFL/rules + ID: $Id$ + Author: Konrad Slind, Cambridge University Computer Laboratory + Copyright 1997 University of Cambridge + +Emulation of HOL inference rules for TFL +*) + + +structure Rules : Rules_sig = +struct + +open Utils; + +structure USyntax = USyntax; +structure S = USyntax; +structure U = Utils; +structure D = Dcterm; + + +fun RULES_ERR{func,mesg} = Utils.ERR{module = "Rules",func=func,mesg=mesg}; + + +fun cconcl thm = D.drop_prop(#prop(crep_thm thm)); +fun chyps thm = map D.drop_prop(#hyps(crep_thm thm)); + +fun dest_thm thm = + let val {prop,hyps,...} = rep_thm thm + in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) + end; + + + +(* Inference rules *) + +(*--------------------------------------------------------------------------- + * Equality (one step) + *---------------------------------------------------------------------------*) +fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq; +fun SYM thm = thm RS sym; + +fun ALPHA thm ctm1 = + let val ctm2 = cprop_of thm + val ctm2_eq = reflexive ctm2 + val ctm1_eq = reflexive ctm1 + in equal_elim (transitive ctm2_eq ctm1_eq) thm + end; + + +(*---------------------------------------------------------------------------- + * typ instantiation + *---------------------------------------------------------------------------*) +fun INST_TYPE blist thm = + let val {sign,...} = rep_thm thm + val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist + in Thm.instantiate (blist',[]) thm + end + handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; + + +(*---------------------------------------------------------------------------- + * 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); + +(*forces the first argument to be a proposition if necessary*) +fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI; + +fun DISCH_ALL thm = Utils.itlist DISCH (#hyps (crep_thm thm)) thm; + + +fun FILTER_DISCH_ALL P thm = + let fun check tm = U.holds P (#t(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 (freezeT thm)))) + in implies_elim (thm RS mp) (ASSUME tm) + end + handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; + +fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; + +local val [p1,p2] = goal HOL.thy "(A-->B) ==> (B --> C) ==> (A-->C)" + val dummy = by (rtac impI 1) + val dummy = by (rtac (p2 RS mp) 1) + val dummy = by (rtac (p1 RS mp) 1) + val dummy = by (assume_tac 1) + val imp_trans = result() +in +fun IMP_TRANS th1 th2 = th2 RS (th1 RS imp_trans) +end; + +(*---------------------------------------------------------------------------- + * Conjunction + *---------------------------------------------------------------------------*) +fun CONJUNCT1 thm = (thm RS conjunct1) +fun CONJUNCT2 thm = (thm RS conjunct2); +fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) + handle _ => [th]; + +fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"} + | LIST_CONJ [th] = th + | LIST_CONJ (th::rst) = MP(MP(conjI COMP (impI RS impI)) th) (LIST_CONJ rst); + + +(*---------------------------------------------------------------------------- + * Disjunction + *---------------------------------------------------------------------------*) +local val {prop,sign,...} = rep_thm disjI1 + val [P,Q] = term_vars prop + val disj1 = forall_intr (cterm_of sign Q) disjI1 +in +fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1) +end; + +local val {prop,sign,...} = rep_thm disjI2 + val [P,Q] = term_vars prop + val disj2 = forall_intr (cterm_of sign P) disjI2 +in +fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2) +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 itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) + :: blue (ldisjs@[cconcl th]) rst tail + end handle _ => [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 + * + *---------------------------------------------------------------------------*) +local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R" + val dummy = by (rtac (p1 RS disjE) 1) + val dummy = by (rtac (p2 RS mp) 1) + val dummy = by (assume_tac 1) + val dummy = by (rtac (p3 RS mp) 1) + val dummy = by (assume_tac 1) + val tfl_exE = result() +in +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 tfl_exE)) + end +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{func = "organize", + mesg = "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{func = "organize", + mesg = "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{func="DISJ_CASESL",mesg="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 = rev_itlist SPEC (#1(D.strip_forall(cconcl thm))) thm; + +val ISPEC = SPEC +val ISPECL = 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 = 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 = 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' + * + *---------------------------------------------------------------------------*) + +local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q" + val dummy = by (rtac (p1 RS exE) 1) + val dummy = by (rtac ((p2 RS allE) RS mp) 1) + val dummy = by (assume_tac 2) + val dummy = by (assume_tac 1) + val choose_thm = result() +in +fun CHOOSE(fvar,exth) fact = + let val lam = #2(dest_comb(D.drop_prop(cconcl exth))) + val redex = capply lam fvar + val {sign, t = t$u,...} = rep_cterm redex + val residue = cterm_of sign (betapply(t,u)) + in GEN fvar (DISCH residue fact) RS (exth RS choose_thm) + end +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(dest_comb template) + in + thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) + 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 _ => th) thl); + +local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None)) +in +fun simpl_conv ss thl ctm = + rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm + RS meta_eq_to_obj_eq +end; + +local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]) +in +val RIGHT_ASSOC = rewrite_rule [prover"((a|b)|c) = (a|(b|c))" RS eq_reflection] +val ASM = refl RS iffD1 +end; + + + + +(*--------------------------------------------------------------------------- + * 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 ("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(Const("all",_) $ (a as Abs _)) = S.dest_abs a + | dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"}; + +val is_all = Utils.can dest_all; + +fun strip_all fm = + if (is_all fm) + then let val {Bvar,Body} = dest_all fm + val (bvs,core) = strip_all Body + in ((Bvar::bvs), core) + end + else ([],fm); + +fun break_all(Const("all",_) $ Abs (_,_,body)) = body + | break_all _ = raise RULES_ERR{func = "break_all", mesg = "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 _ => 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 = transitive th (beta_conversion(#2(D.dest_eq(cconcl th)))) + fun iter [] = reflexive tm + | iter (v::rst) = rbeta (combination(iter rst) (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 _ => 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 tm = + let val {Bvar,Body} = S.dest_abs tm + in (Bvar,Body) + end handle _ => let val {varstruct,body} = S.dest_pabs tm + in (varstruct,body) + end; + +fun strip_aabs tm = + let val (vstr,body) = dest_aabs tm + val (bvs, core) = strip_aabs body + in (vstr::bvs, core) + end + handle _ => ([],tm); + +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[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 M n = + let val (f,args) = dest_combn M n + val dummy = dest_aabs f + in (strip_aabs f,args) + end; + +fun pbeta_redex M n = U.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("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 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 = Thm.rewrite_cterm(false,true,false)mss' prover lhs + handle _ => 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,_),args) = dest_pbeta_redex 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 = Thm.rewrite_cterm (false,true,false) mss' prover Q1 + handle _ => 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 = symmetric(pbeta_reduce Q3 RS eq_reflection) + val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 + val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => + ((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) = strip_all 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 = Thm.rewrite_cterm(false,true,false) mss' + prover (tych Q) + handle _ => 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 _ => None + + 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{func = "solver", + mesg = "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 _ => None + in + (if (is_cong thm) then cong_prover else restrict_prover) mss thm + end + val ctm = cprop_of th + val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs)) + prover ctm + val th2 = equal_elim th1 th + in + (th2, filter (not o restricted) (!tc_list)) + end; + + + +fun prove (ptm,tac) = + #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac]))); + + +end; (* Rules *) diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/sys.sml --- a/TFL/sys.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/sys.sml Fri Apr 23 12:23:21 1999 +0200 @@ -26,7 +26,7 @@ use "usyntax.sml"; use "thms.sml"; use "dcterm.sml"; -use "rules.new.sml"; +use "rules.sml"; use "thry.sml"; diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/tfl.sig --- a/TFL/tfl.sig Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/tfl.sig Fri Apr 23 12:23:21 1999 +0200 @@ -8,6 +8,13 @@ signature TFL_sig = sig + + val trace : bool ref + + val default_simps : thm list (*simprules used for deriving rules...*) + + val congs : thm list -> thm list (*fn to make congruent rules*) + datatype pattern = GIVEN of term * int | OMITTED of term * int @@ -17,30 +24,37 @@ val wfrec_definition0 : theory -> string -> term -> term -> theory - val post_definition : simpset * thm list -> theory * (thm * pattern list) - -> {theory : theory, + val post_definition : thm list -> theory * (thm * pattern list) + -> {theory : theory, rules : thm, TCs : term list list, full_pats_TCs : (term * term list) list, patterns : pattern list} -(*CURRENTLY UNUSED - val wfrec_eqns : simpset * thm list -> theory -> term list - -> {WFR : term, + val wfrec_eqns : theory -> xstring + -> thm list (* congruence rules *) + -> term list + -> {WFR : term, SV : term list, proto_def : term, extracta :(thm * term list) list, pats : pattern list} - val lazyR_def : theory + val lazyR_def : theory -> xstring + -> thm list (* congruence rules *) -> term list - -> {theory:theory, - rules :thm, - R :term, - full_pats_TCs :(term * term list) list, - patterns: pattern list} ----------------------*) + -> {theory : theory, + rules : thm, + R : term, + SV : term list, + full_pats_TCs : (term * term list) list, + patterns : pattern list} - val mk_induction : theory -> term -> term -> (term * term list) list -> thm + val mk_induction : theory + -> {fconst:term, + R : term, + SV : term list, + pat_TCs_list : (term * term list) list} + -> thm val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm} -> theory diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/tfl.sml --- a/TFL/tfl.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/tfl.sml Fri Apr 23 12:23:21 1999 +0200 @@ -9,6 +9,8 @@ structure Prim : TFL_sig = struct +val trace = ref false; + (* Abbreviations *) structure R = Rules; structure S = USyntax; @@ -31,6 +33,23 @@ (*--------------------------------------------------------------------------- + handling of user-supplied congruence rules: lcp*) + +(*Convert conclusion from = to ==*) +val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th); + +(*default congruence rules include those for LET and IF*) +val default_congs = eq_reflect_list [Thms.LET_CONG, if_cong]; + +fun congs ths = default_congs @ eq_reflect_list ths; + +val default_simps = + [less_Suc_eq RS iffD2, lex_prod_def, measure_def, inv_image_def]; + + + + +(*--------------------------------------------------------------------------- * The next function is common to pattern-match translation and * proof of completeness of cases for the induction theorem. * @@ -314,6 +333,12 @@ *---------------------------------------------------------------------------*) +(*For Isabelle, the lhs of a definition must be a constant.*) +fun mk_const_def sign (Name, Ty, rhs) = + Sign.infer_types sign (K None) (K None) [] false + ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT) + |> #1; + (*Make all TVars available for instantiation by adding a ? to the front*) fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts) | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort) @@ -335,10 +360,7 @@ val wfrec_R_M = map_term_types poly_tvars (wfrec $ map_term_types poly_tvars R) $ functional - val (def_term, _) = - Sign.infer_types (Theory.sign_of thy) (K None) (K None) [] false - ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], - propT) + val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M) in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end end; @@ -379,7 +401,8 @@ | givens (GIVEN(tm,_)::pats) = tm :: givens pats | givens (OMITTED _::pats) = givens pats; -fun post_definition (ss, tflCongs) (theory, (def, pats)) = +(*called only by Tfl.simplify_defn*) +fun post_definition meta_tflCongs (theory, (def, pats)) = let val tych = Thry.typecheck theory val f = #lhs(S.dest_eq(concl def)) val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def @@ -392,9 +415,7 @@ val (case_rewrites,context_congs) = extraction_thms theory val corollaries' = map(rewrite_rule case_rewrites) corollaries val extract = R.CONTEXT_REWRITE_RULE - (ss, f, R, - R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA, - tflCongs@context_congs) + (f, [R], cut_apply, meta_tflCongs@context_congs) val (rules, TCs) = ListPair.unzip (map extract corollaries') val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) @@ -402,23 +423,29 @@ in {theory = theory, (* holds def, if it's needed *) rules = rules1, - full_pats_TCs = merge (map pat_of pats) - (ListPair.zip (given_pats, TCs)), + full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), TCs = TCs, patterns = pats} end; + (*--------------------------------------------------------------------------- * Perform the extraction without making the definition. Definition and - * extraction commute for the non-nested case. For hol90 users, this - * function can be invoked without being in draft mode. - * CURRENTLY UNUSED -fun wfrec_eqns (ss, tflCongs) thy eqns = - let val {functional,pats} = mk_functional thy eqns + * extraction commute for the non-nested case. (Deferred recdefs) + *---------------------------------------------------------------------------*) +fun wfrec_eqns thy fid tflCongs eqns = + let val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns val given_pats = givens pats - val {Bvar = f, Body} = S.dest_abs functional - val {Bvar = x, ...} = S.dest_abs Body - val (Name, Type("fun", [f_dty, f_rty])) = dest_Free f + val f = #1 (S.strip_comb(#lhs(S.dest_eq (hd eqns)))) + (* val f = Free(Name,Ty) *) + val Type("fun", [f_dty, f_rty]) = Ty + val dummy = if Name<>fid then + raise TFL_ERR{func = "lazyR_def", + mesg = "Expected a definition of " ^ + quote fid ^ " but found one of " ^ + quote Name} + else () + val SV = S.free_vars_lr functional (* schema variables *) val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY @@ -427,20 +454,25 @@ Rtype) val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0 val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) + val dummy = + if !trace then + writeln ("ORIGINAL PROTO_DEF: " ^ + Sign.string_of_term (Theory.sign_of thy) proto_def) + else () val R1 = S.rand WFR val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM) val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats val corollaries' = map (rewrite_rule case_rewrites) corollaries - val extract = R.CONTEXT_REWRITE_RULE - (ss, f, R1, - R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA, - tflCongs@context_congs) - in {proto_def=proto_def, + fun extract X = R.CONTEXT_REWRITE_RULE + (f, R1::SV, cut_apply, tflCongs@context_congs) X + in {proto_def = (*Use == rather than = for definitions*) + mk_const_def (Theory.sign_of thy) + (Name, Ty, S.rhs proto_def), + SV=SV, WFR=WFR, pats=pats, extracta = map extract corollaries'} end; - *---------------------------------------------------------------------------*) (*--------------------------------------------------------------------------- @@ -448,37 +480,56 @@ * wellfounded relation used in the definition is computed by using the * choice operator on the extracted conditions (plus the condition that * such a relation must be wellfounded). - * CURRENTLY UNUSED -fun lazyR_def ss thy eqns = - let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns + *---------------------------------------------------------------------------*) +fun lazyR_def thy fid tflCongs eqns = + let val {proto_def,WFR,pats,extracta,SV} = + wfrec_eqns thy fid (congs tflCongs) eqns val R1 = S.rand WFR - val f = S.lhs proto_def - val (Name,_) = dest_Free f + val f = #1 (Logic.dest_equals proto_def) val (extractants,TCl) = ListPair.unzip extracta + val dummy = if !trace + then (writeln "Extractants = "; + prths extractants; + ()) + else () val TCs = foldr (gen_union (op aconv)) (TCl, []) val full_rqt = WFR::TCs val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} val R'abs = S.rand R' + val proto_def' = subst_free[(R1,R')] proto_def + val dummy = if !trace then writeln ("proto_def' = " ^ + Sign.string_of_term + (Theory.sign_of thy) proto_def') + else () val theory = thy - |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)]; - val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq) + |> PureThy.add_defs_i + [Thm.no_attributes (fid ^ "_def", proto_def')]; + val def = get_axiom theory (fid ^ "_def") RS meta_eq_to_obj_eq + val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def) + else () val fconst = #lhs(S.dest_eq(concl def)) val tych = Thry.typecheck theory - val baz = R.DISCH (tych proto_def) - (U.itlist (R.DISCH o tych) full_rqt (R.LIST_CONJ extractants)) + val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt + (*lcp: a lot of object-logic inference to remove*) + val baz = R.DISCH_ALL + (U.itlist R.DISCH full_rqt_prop + (R.LIST_CONJ extractants)) + val dum = if !trace then writeln ("baz = " ^ string_of_thm baz) + else () + val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) val def' = R.MP (R.SPEC (tych fconst) - (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz))) + (R.SPEC (tych R') + (R.GENL[tych R1, tych f_free] baz))) def - val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt) + val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX) body_th - in {theory = theory, R=R1, + in {theory = theory, R=R1, SV=SV, rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), patterns = pats} end; - *---------------------------------------------------------------------------*) @@ -617,7 +668,7 @@ * * Note. When the context is empty, there can be no local variables. *---------------------------------------------------------------------------*) - +(* local infix 5 ==> fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} in @@ -644,12 +695,38 @@ end end end; +*) - +local infix 5 ==> + fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} +in +fun build_ih f (P,SV) (pat,TCs) = + let val pat_vars = S.free_vars_lr pat + val globals = pat_vars@SV + fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) + fun dest_TC tm = + let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) + val (R,y,_) = S.dest_relation R_y_pat + val P_y = if (nested tm) then R_y_pat ==> P$y else P$y + in case cntxt + of [] => (P_y, (tm,[])) + | _ => let + val imp = S.list_mk_conj cntxt ==> P_y + val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) + val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs + in (S.list_mk_forall(locals,imp), (tm,locals)) end + end + in case TCs + of [] => (S.list_mk_forall(pat_vars, P$pat), []) + | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) + val ind_clause = S.list_mk_conj ihs ==> P$pat + in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals) + end + end +end; (*--------------------------------------------------------------------------- - * This function makes good on the promise made in "build_ih: we prove - * . + * This function makes good on the promise made in "build_ih". * * Input is tm = "(!y. R y pat ==> P y) ==> P pat", * TCs = TC_1[pat] ... TC_n[pat] @@ -711,7 +788,7 @@ * recursion induction (Rinduct) by proving the antecedent of Sinduct from * the antecedent of Rinduct. *---------------------------------------------------------------------------*) -fun mk_induction thy f R pat_TCs_list = +fun mk_induction thy {fconst, R, SV, pat_TCs_list} = let val tych = Thry.typecheck thy val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM) val (pats,TCsl) = ListPair.unzip pat_TCs_list @@ -722,12 +799,12 @@ val P = Free(Pname, domain --> HOLogic.boolT) val Sinduct = R.SPEC (tych P) Sinduction val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) - val Rassums_TCl' = map (build_ih f P) pat_TCs_list + val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list val (Rassums,TCl') = ListPair.unzip Rassums_TCl' val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums)) val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) - val proved_cases = map (prove_case f thy) tasks + val proved_cases = map (prove_case fconst thy) tasks val v = Free (variant (foldr add_term_names (map concl proved_cases, [])) "v", domain) @@ -803,8 +880,20 @@ * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else * 3. replace tc by tc' in both the rules and the induction theorem. *---------------------------------------------------------------------*) + +fun print_thms s L = + if !trace then writeln (cat_lines (s :: map string_of_thm L)) + else (); + +fun print_cterms s L = + if !trace then writeln (cat_lines (s :: map string_of_cterm L)) + else ();; + fun simplify_tc tc (r,ind) = - let val tc_eq = simplifier (tych tc) + let val tc1 = tych tc + val _ = print_cterms "TC before simplification: " [tc1] + val tc_eq = simplifier tc1 + val _ = print_thms "result: " [tc_eq] in elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind) handle _ => diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/thms.sig --- a/TFL/thms.sig Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/thms.sig Fri Apr 23 12:23:21 1999 +0200 @@ -9,7 +9,6 @@ val WF_INDUCTION_THM:thm val WFREC_COROLLARY :thm val CUT_DEF :thm - val CUT_LEMMA :thm val SELECT_AX :thm val LET_CONG :thm diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/thms.sml --- a/TFL/thms.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/thms.sml Fri Apr 23 12:23:21 1999 +0200 @@ -6,9 +6,8 @@ structure Thms : Thms_sig = struct - val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec" - val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct" - val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply" + val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec" + val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct" val CUT_DEF = cut_def local val _ = goal HOL.thy "!P x. P x --> P (Eps P)" diff -r 120ca2bb27e1 -r 1ebbe18fe236 TFL/usyntax.sml --- a/TFL/usyntax.sml Fri Apr 23 12:22:30 1999 +0200 +++ b/TFL/usyntax.sml Fri Apr 23 12:23:21 1999 +0200 @@ -214,7 +214,6 @@ end; -(* Garbage - ought to be dropped *) val lhs = #lhs o dest_eq val rhs = #rhs o dest_eq val rand = #Rand o dest_comb