# HG changeset patch # User wenzelm # Date 978633593 -3600 # Node ID 856773b19058c99769e526bafbcc9989baacd4ea # Parent b0d961105f469a967f8a3962caa64bb4b2f502ff renamed .sml files to .ML; diff -r b0d961105f46 -r 856773b19058 TFL/dcterm.sml --- a/TFL/dcterm.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,193 +0,0 @@ -(* Title: TFL/dcterm.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -(*--------------------------------------------------------------------------- - * Derived efficient cterm destructors. - *---------------------------------------------------------------------------*) - -structure Dcterm : -sig - val mk_conj : cterm * cterm -> cterm - val mk_disj : cterm * cterm -> cterm - val mk_exists : cterm * cterm -> cterm - - val dest_conj : cterm -> cterm * cterm - val dest_const : cterm -> {Name:string, Ty:typ} - val dest_disj : cterm -> cterm * cterm - val dest_eq : cterm -> cterm * cterm - val dest_exists : cterm -> cterm * cterm - val dest_forall : cterm -> cterm * cterm - val dest_imp : cterm -> cterm * cterm - val dest_let : cterm -> cterm * cterm - val dest_neg : cterm -> cterm - val dest_pair : cterm -> cterm * cterm - val dest_var : cterm -> {Name:string, Ty:typ} - val is_conj : cterm -> bool - val is_cons : cterm -> bool - val is_disj : cterm -> bool - val is_eq : cterm -> bool - val is_exists : cterm -> bool - val is_forall : cterm -> bool - val is_imp : cterm -> bool - val is_let : cterm -> bool - val is_neg : cterm -> bool - val is_pair : cterm -> bool - val list_mk_disj : cterm list -> cterm - val strip_abs : cterm -> cterm list * cterm - val strip_comb : cterm -> cterm * cterm list - val strip_disj : cterm -> cterm list - val strip_exists : cterm -> cterm list * cterm - val strip_forall : cterm -> cterm list * cterm - val strip_imp : cterm -> cterm list * cterm - val drop_prop : cterm -> cterm - val mk_prop : cterm -> cterm - end = -struct - -fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg}; - -(*--------------------------------------------------------------------------- - * General support routines - *---------------------------------------------------------------------------*) -val can = Utils.can; -fun swap (x,y) = (y,x); - - -(*--------------------------------------------------------------------------- - * Some simple constructor functions. - *---------------------------------------------------------------------------*) - -fun mk_const sign pr = cterm_of sign (Const pr); -val mk_hol_const = mk_const (Theory.sign_of HOL.thy); - -fun mk_exists (r as (Bvar,Body)) = - let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT) - in capply c (uncurry cabs r) - end; - - -local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) -in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 -end; - -local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) -in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 -end; - - -(*--------------------------------------------------------------------------- - * The primitives. - *---------------------------------------------------------------------------*) -fun dest_const ctm = - (case #t(rep_cterm ctm) - of Const(s,ty) => {Name = s, Ty = ty} - | _ => raise ERR "dest_const" "not a constant"); - -fun dest_var ctm = - (case #t(rep_cterm ctm) - of Var((s,i),ty) => {Name=s, Ty=ty} - | Free(s,ty) => {Name=s, Ty=ty} - | _ => raise ERR "dest_var" "not a variable"); - - -(*--------------------------------------------------------------------------- - * Derived destructor operations. - *---------------------------------------------------------------------------*) - -fun dest_monop expected tm = - let exception Fail - val (c,N) = dest_comb tm - in if (#Name(dest_const c) = expected) then N else raise Fail - end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected); - -fun dest_binop expected tm = - let val (M,N) = dest_comb tm - in (dest_monop expected M, N) - end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected); - -(* For "if-then-else" -fun dest_triop expected tm = - let val (MN,P) = dest_comb tm - val (M,N) = dest_binop expected MN - in (M,N,P) - end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected); -*) - -fun dest_binder expected tm = - dest_abs None (dest_monop expected tm) - handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected); - - -val dest_neg = dest_monop "not" -val dest_pair = dest_binop "Pair"; -val dest_eq = dest_binop "op =" -val dest_imp = dest_binop "op -->" -val dest_conj = dest_binop "op &" -val dest_disj = dest_binop "op |" -val dest_cons = dest_binop "Cons" -val dest_let = swap o dest_binop "Let"; -(* val dest_cond = dest_triop "if" *) -val dest_select = dest_binder "Eps" -val dest_exists = dest_binder "Ex" -val dest_forall = dest_binder "All" - -(* Query routines *) - -val is_eq = can dest_eq -val is_imp = can dest_imp -val is_select = can dest_select -val is_forall = can dest_forall -val is_exists = can dest_exists -val is_neg = can dest_neg -val is_conj = can dest_conj -val is_disj = can dest_disj -(* val is_cond = can dest_cond *) -val is_pair = can dest_pair -val is_let = can dest_let -val is_cons = can dest_cons - - -(*--------------------------------------------------------------------------- - * Iterated creation. - *---------------------------------------------------------------------------*) -val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm)) - -(*--------------------------------------------------------------------------- - * Iterated destruction. (To the "right" in a term.) - *---------------------------------------------------------------------------*) -fun strip break tm = - let fun dest (p as (ctm,accum)) = - let val (M,N) = break ctm - in dest (N, M::accum) - end handle _ => p (* FIXME do not handle _ !!! *) - in dest (tm,[]) - end; - -fun rev2swap (x,l) = (rev l, x); - -val strip_comb = strip (swap o dest_comb) (* Goes to the "left" *) -val strip_imp = rev2swap o strip dest_imp -val strip_abs = rev2swap o strip (dest_abs None) -val strip_forall = rev2swap o strip dest_forall -val strip_exists = rev2swap o strip dest_exists - -val strip_disj = rev o (op::) o strip dest_disj - - -(*--------------------------------------------------------------------------- - * Going into and out of prop - *---------------------------------------------------------------------------*) -local val prop = cterm_of (Theory.sign_of HOL.thy) (read"Trueprop") -in fun mk_prop ctm = - case (#t(rep_cterm ctm)) - of (Const("Trueprop",_)$_) => ctm - | _ => capply prop ctm -end; - -fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm; (* FIXME do not handle _ !!! *) - -end; diff -r b0d961105f46 -r 856773b19058 TFL/post.sml --- a/TFL/post.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,231 +0,0 @@ -(* Title: TFL/post.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Second part of main module (postprocessing of TFL definitions). -*) - -signature TFL = -sig - val trace: bool ref - val quiet_mode: bool ref - val message: string -> unit - val tgoalw: theory -> thm list -> thm list -> thm list - val tgoal: theory -> thm list -> thm list - val std_postprocessor: claset -> simpset -> thm list -> theory -> - {induction: thm, rules: thm, TCs: term list list} -> - {induction: thm, rules: thm, nested_tcs: thm list} - val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring -> - term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} - val define: theory -> claset -> simpset -> thm list -> thm list -> xstring -> - string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} - val defer_i: theory -> thm list -> xstring -> term list -> theory * thm - val defer: theory -> thm list -> xstring -> string list -> theory * thm -end; - -structure Tfl: TFL = -struct - -structure S = USyntax - - -(* messages *) - -val trace = Prim.trace - -val quiet_mode = ref false; -fun message s = if ! quiet_mode then () else writeln s; - - -(* misc *) - -fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT; - - -(*--------------------------------------------------------------------------- - * 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. - *--------------------------------------------------------------------------*) -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 cs ss wfs = - Prim.postprocess - {wf_tac = REPEAT (ares_tac wfs 1), - terminator = asm_simp_tac ss 1 - THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), - simplifier = Rules.simpl_conv ss []}; - - - -val concl = #2 o Rules.dest_thm; - -(*--------------------------------------------------------------------------- - * Postprocess a definition made by "define". This is a separate stage of - * processing from the definition stage. - *---------------------------------------------------------------------------*) -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 - -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 (* FIXME do not handle _ !!! *) - -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)) - -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 cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = - let - val _ = message "Proving induction theorem ..." - val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} - val _ = message "Postprocessing ..."; - val {rules, induction, nested_tcs} = - std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} - in - case nested_tcs - of [] => {induction=induction, rules=rules,tcs=[]} - | L => let val dummy = message "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 - 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))); - -(*Strip off the outer !P*) -val spec'= read_instantiate [("x","P::?'b=>bool")] spec; - -fun simplify_defn thy cs ss congs wfs id pats def0 = - let val def = freezeT def0 RS meta_eq_to_obj_eq - val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) - val {lhs=f,rhs} = S.dest_eq (concl def) - val (_,[R,_]) = S.strip_comb rhs - val {induction, rules, tcs} = - proof_stage cs ss wfs theory - {f = f, R = R, rules = rules, - full_pats_TCs = full_pats_TCs, - TCs = TCs} - val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules) - in {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')), - rules = ListPair.zip(rules', rows), - tcs = (termination_goals rules') @ tcs} - end - handle Utils.ERR {mesg,func,module} => - error (mesg ^ - "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); - -(*--------------------------------------------------------------------------- - * Defining a function with an associated termination relation. - *---------------------------------------------------------------------------*) -fun define_i thy cs ss congs wfs fid R eqs = - let val {functional,pats} = Prim.mk_functional thy eqs - val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional - in (thy, simplify_defn thy cs ss congs wfs fid pats def) end; - -fun define thy cs ss congs wfs fid R seqs = - define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) - handle Utils.ERR {mesg,...} => error mesg; - - -(*--------------------------------------------------------------------------- - * - * 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 defer_i thy congs fid eqs = - let val {rules,R,theory,full_pats_TCs,SV,...} = - Prim.lazyR_def thy (Sign.base_name fid) congs eqs - val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) (* FIXME do not handle _ !!! *) - val dummy = message "Proving induction theorem ..."; - val induction = Prim.mk_induction theory - {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} - in (theory, - (*return the conjoined induction rule and recursion equations, - with assumptions remaining to discharge*) - standard (induction RS (rules RS conjI))) - end - -fun defer thy congs fid seqs = - defer_i thy congs fid (map (read_term thy) seqs) - handle Utils.ERR {mesg,...} => error mesg; -end; - -end; diff -r b0d961105f46 -r 856773b19058 TFL/rules.sml --- a/TFL/rules.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,847 +0,0 @@ -(* 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 = -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 INST_TYPE :(typ*typ)list -> 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_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; - -fun rbeta th = - case Dcterm.strip_comb (cconcl th) - of (eeq,[l,r]) => transitive th (beta_conversion false r) - | _ => raise RULES_ERR{func="rbeta", mesg =""}; - -(*---------------------------------------------------------------------------- - * 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 = ""}; (* FIXME do not handle _ !!! *) - - -(*---------------------------------------------------------------------------- - * 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 = ""}; (* FIXME do not handle _ !!! *) - -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]; (* FIXME do not handle _ !!! *) - -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] (* FIXME do not handle _ !!! *) - 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); (* FIXME do not handle _ !!! *) - -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; - -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 ("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{func = "dest_all", mesg = "not a !!"}; - -val is_all = Utils.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{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); (* FIXME do not handle _ !!! *) - -(* 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 false (#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}; (* FIXME do not handle _ !!! *) - -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 _ => (* FIXME do not handle _ !!! *) - 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 _ => ([], tm, used); (* FIXME do not handle _ !!! *) - -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 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 = 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("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 _ => reflexive lhs (* FIXME do not handle _ !!! *) - 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 _ => reflexive Q1 (* FIXME do not handle _ !!! *) - 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 _ => (* FIXME do not 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, 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 _ => reflexive (tych Q) (* FIXME do not handle _ !!! *) - 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 (* FIXME do not handle _ !!! *) - - 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 (* FIXME do not handle _ !!! *) - 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) = - #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac]))); - - -end; (* Rules *) diff -r b0d961105f46 -r 856773b19058 TFL/tfl.sml --- a/TFL/tfl.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1006 +0,0 @@ -(* Title: TFL/tfl.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -First part of main module. -*) - -signature TFL_sig = -sig - val trace: bool ref - type pattern - val mk_functional: theory -> term list -> {functional: term, pats: pattern list} - val wfrec_definition0: theory -> string -> term -> term -> theory * thm - val post_definition: thm list -> theory * (thm * pattern list) -> - {theory: theory, - rules: thm, - rows: int list, - TCs: term list list, - full_pats_TCs: (term * term list) list} - val wfrec_eqns: theory -> xstring -> thm list -> term list -> - {WFR: term, - SV: term list, - proto_def: term, - extracta: (thm * term list) list, - pats: pattern list} - val lazyR_def: theory -> xstring -> thm list -> term list -> - {theory: theory, - rules: thm, - R: term, - SV: term list, - full_pats_TCs: (term * term list) list, - patterns : pattern list} - val mk_induction: theory -> - {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm - val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory -> - {rules: thm, induction: thm, TCs: term list list} -> - {rules: thm, induction: thm, nested_tcs: thm list} -end; - - -structure Prim: TFL_sig = -struct - -val trace = ref false; - -open BasisLibrary; - -structure R = Rules; -structure S = USyntax; -structure U = Utils; - - -fun TFL_ERR {func, mesg} = U.ERR {module = "Tfl", func = func, mesg = mesg}; - -val concl = #2 o R.dest_thm; -val hyp = #1 o R.dest_thm; - -val list_mk_type = U.end_itlist (curry (op -->)); - -fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1)); - -fun front_last [] = raise TFL_ERR {func="front_last", mesg="empty list"} - | front_last [x] = ([],x) - | front_last (h::t) = - let val (pref,x) = front_last t - in - (h::pref,x) - end; - - -(*--------------------------------------------------------------------------- - * The next function is common to pattern-match translation and - * proof of completeness of cases for the induction theorem. - * - * The curried function "gvvariant" returns a function to generate distinct - * variables that are guaranteed not to be in names. The names of - * the variables go u, v, ..., z, aa, ..., az, ... The returned - * function contains embedded refs! - *---------------------------------------------------------------------------*) -fun gvvariant names = - let val slist = ref names - val vname = ref "u" - fun new() = - if !vname mem_string (!slist) - then (vname := bump_string (!vname); new()) - else (slist := !vname :: !slist; !vname) - in - fn ty => Free(new(), ty) - end; - - -(*--------------------------------------------------------------------------- - * Used in induction theorem production. This is the simple case of - * partitioning up pattern rows by the leading constructor. - *---------------------------------------------------------------------------*) -fun ipartition gv (constructors,rows) = - let fun pfail s = raise TFL_ERR{func = "partition.part", mesg = s} - fun part {constrs = [], rows = [], A} = rev A - | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" - | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" - | part {constrs = c::crst, rows, A} = - let val (Name,Ty) = dest_Const c - val L = binder_types Ty - val (in_group, not_in_group) = - U.itlist (fn (row as (p::rst, rhs)) => - fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p - in if (#1(dest_Const pc) = Name) - then ((args@rst, rhs)::in_group, not_in_group) - else (in_group, row::not_in_group) - end) rows ([],[]) - val col_types = U.take type_of (length L, #1(hd in_group)) - in - part{constrs = crst, rows = not_in_group, - A = {constructor = c, - new_formals = map gv col_types, - group = in_group}::A} - end - in part{constrs = constructors, rows = rows, A = []} - end; - - - -(*--------------------------------------------------------------------------- - * Each pattern carries with it a tag (i,b) where - * i is the clause it came from and - * b=true indicates that clause was given by the user - * (or is an instantiation of a user supplied pattern) - * b=false --> i = ~1 - *---------------------------------------------------------------------------*) - -type pattern = term * (int * bool) - -fun pattern_map f (tm,x) = (f tm, x); - -fun pattern_subst theta = pattern_map (subst_free theta); - -val pat_of = fst; -fun row_of_pat x = fst (snd x); -fun given x = snd (snd x); - -(*--------------------------------------------------------------------------- - * Produce an instance of a constructor, plus genvars for its arguments. - *---------------------------------------------------------------------------*) -fun fresh_constr ty_match colty gv c = - let val (_,Ty) = dest_Const c - val L = binder_types Ty - and ty = body_type Ty - val ty_theta = ty_match ty colty - val c' = S.inst ty_theta c - val gvars = map (S.inst ty_theta o gv) L - in (c', gvars) - end; - - -(*--------------------------------------------------------------------------- - * Goes through a list of rows and picks out the ones beginning with a - * pattern with constructor = Name. - *---------------------------------------------------------------------------*) -fun mk_group Name rows = - U.itlist (fn (row as ((prfx, p::rst), rhs)) => - fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p - in if ((#1(dest_Const pc) = Name) handle _ => false) (* FIXME do not handle _ !!! *) - then (((prfx,args@rst), rhs)::in_group, not_in_group) - else (in_group, row::not_in_group) end) - rows ([],[]); - -(*--------------------------------------------------------------------------- - * Partition the rows. Not efficient: we should use hashing. - *---------------------------------------------------------------------------*) -fun partition _ _ (_,_,_,[]) = raise TFL_ERR{func="partition", mesg="no rows"} - | partition gv ty_match - (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) = -let val fresh = fresh_constr ty_match colty gv - fun part {constrs = [], rows, A} = rev A - | part {constrs = c::crst, rows, A} = - let val (c',gvars) = fresh c - val (Name,Ty) = dest_Const c' - val (in_group, not_in_group) = mk_group Name rows - val in_group' = - if (null in_group) (* Constructor not given *) - then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))] - else in_group - in - part{constrs = crst, - rows = not_in_group, - A = {constructor = c', - new_formals = gvars, - group = in_group'}::A} - end -in part{constrs=constructors, rows=rows, A=[]} -end; - -(*--------------------------------------------------------------------------- - * Misc. routines used in mk_case - *---------------------------------------------------------------------------*) - -fun mk_pat (c,l) = - let val L = length (binder_types (type_of c)) - fun build (prfx,tag,plist) = - let val args = take (L,plist) - and plist' = drop(L,plist) - in (prfx,tag,list_comb(c,args)::plist') end - in map build l end; - -fun v_to_prfx (prfx, v::pats) = (v::prfx,pats) - | v_to_prfx _ = raise TFL_ERR{func="mk_case", mesg="v_to_prfx"}; - -fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats) - | v_to_pats _ = raise TFL_ERR{func="mk_case", mesg="v_to_pats"}; - - -(*---------------------------------------------------------------------------- - * Translation of pattern terms into nested case expressions. - * - * This performs the translation and also builds the full set of patterns. - * Thus it supports the construction of induction theorems even when an - * incomplete set of patterns is given. - *---------------------------------------------------------------------------*) - -fun mk_case ty_info ty_match usednames range_ty = - let - fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s} - val fresh_var = gvvariant usednames - val divide = partition fresh_var ty_match - fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row" - | expand constructors ty (row as ((prfx, p::rst), rhs)) = - if (is_Free p) - then let val fresh = fresh_constr ty_match ty fresh_var - fun expnd (c,gvs) = - let val capp = list_comb(c,gvs) - in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs) - end - in map expnd (map fresh constructors) end - else [row] - fun mk{rows=[],...} = mk_case_fail"no rows" - | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *) - ([(prfx,tag,[])], tm) - | mk{path=[], rows = _::_} = mk_case_fail"blunder" - | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} = - mk{path = path, - rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst} - | mk{path = u::rstp, rows as ((_, p::_), _)::_} = - let val (pat_rectangle,rights) = ListPair.unzip rows - val col0 = map(hd o #2) pat_rectangle - in - if (forall is_Free col0) - then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e) - (ListPair.zip (col0, rights)) - val pat_rectangle' = map v_to_prfx pat_rectangle - val (pref_patl,tm) = mk{path = rstp, - rows = ListPair.zip (pat_rectangle', - rights')} - in (map v_to_pats pref_patl, tm) - end - else - let val pty as Type (ty_name,_) = type_of p - in - case (ty_info ty_name) - of None => mk_case_fail("Not a known datatype: "^ty_name) - | Some{case_const,constructors} => - let - val case_const_name = #1(dest_Const case_const) - val nrows = List.concat (map (expand constructors pty) rows) - val subproblems = divide(constructors, pty, range_ty, nrows) - val groups = map #group subproblems - and new_formals = map #new_formals subproblems - and constructors' = map #constructor subproblems - val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows}) - (ListPair.zip (new_formals, groups)) - val rec_calls = map mk news - val (pat_rect,dtrees) = ListPair.unzip rec_calls - val case_functions = map S.list_mk_abs - (ListPair.zip (new_formals, dtrees)) - val types = map type_of (case_functions@[u]) @ [range_ty] - val case_const' = Const(case_const_name, list_mk_type types) - val tree = list_comb(case_const', case_functions@[u]) - val pat_rect1 = List.concat - (ListPair.map mk_pat (constructors', pat_rect)) - in (pat_rect1,tree) - end - end end - in mk - end; - - -(* Repeated variable occurrences in a pattern are not allowed. *) -fun FV_multiset tm = - case (S.dest_term tm) - of S.VAR{Name,Ty} => [Free(Name,Ty)] - | S.CONST _ => [] - | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand - | S.LAMB _ => raise TFL_ERR{func = "FV_multiset", mesg = "lambda"}; - -fun no_repeat_vars thy pat = - let fun check [] = true - | check (v::rst) = - if mem_term (v,rst) then - raise TFL_ERR{func = "no_repeat_vars", - mesg = quote(#1(dest_Free v)) ^ - " occurs repeatedly in the pattern " ^ - quote (string_of_cterm (Thry.typecheck thy pat))} - else check rst - in check (FV_multiset pat) - end; - -fun dest_atom (Free p) = p - | dest_atom (Const p) = p - | dest_atom _ = raise TFL_ERR {func="dest_atom", - mesg="function name not an identifier"}; - -fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q); - -local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s} - fun single [_$_] = - mk_functional_err "recdef does not allow currying" - | single [f] = f - | single fs = - (*multiple function names?*) - if length (gen_distinct same_name fs) < length fs - then mk_functional_err - "The function being declared appears with multiple types" - else mk_functional_err - (Int.toString (length fs) ^ - " distinct function names being declared") -in -fun mk_functional thy clauses = - let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses) - handle _ => raise TFL_ERR (* FIXME do not handle _ !!! *) - {func = "mk_functional", - mesg = "recursion equations must use the = relation"} - val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) - val atom = single (gen_distinct (op aconv) funcs) - val (fname,ftype) = dest_atom atom - val dummy = map (no_repeat_vars thy) pats - val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, - map (fn (t,i) => (t,(i,true))) (enumerate R)) - val names = foldr add_term_names (R,[]) - val atype = type_of(hd pats) - and aname = variant names "a" - val a = Free(aname,atype) - val ty_info = Thry.match_info thy - val ty_match = Thry.match_type thy - val range_ty = type_of (hd R) - val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty - {path=[a], rows=rows} - val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts - handle _ => mk_functional_err "error in pattern-match translation" (* FIXME do not handle _ !!! *) - val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1 - val finals = map row_of_pat patts2 - val originals = map (row_of_pat o #2) rows - val dummy = case (originals\\finals) - of [] => () - | L => mk_functional_err - ("The following clauses are redundant (covered by preceding clauses): " ^ - commas (map (fn i => Int.toString (i + 1)) L)) - in {functional = Abs(Sign.base_name fname, ftype, - abstract_over (atom, - absfree(aname,atype, case_tm))), - pats = patts2} -end end; - - -(*---------------------------------------------------------------------------- - * - * PRINCIPLES OF DEFINITION - * - *---------------------------------------------------------------------------*) - - -(*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) - | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort); - -local val f_eq_wfrec_R_M = - #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY)))) - val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M - val (fname,_) = dest_Free f - val (wfrec,_) = S.strip_comb rhs -in -fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) = - let val def_name = if Name<>fid then - raise TFL_ERR{func = "wfrec_definition0", - mesg = "Expected a definition of " ^ - quote fid ^ " but found one of " ^ - quote Name} - else Name ^ "_def" - val wfrec_R_M = map_term_types poly_tvars - (wfrec $ map_term_types poly_tvars R) - $ functional - val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M) - val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy - in (thy', def) end; -end; - - - -(*--------------------------------------------------------------------------- - * This structure keeps track of congruence rules that aren't derived - * from a datatype definition. - *---------------------------------------------------------------------------*) -fun extraction_thms thy = - let val {case_rewrites,case_congs} = Thry.extract_info thy - in (case_rewrites, case_congs) - end; - - -(*--------------------------------------------------------------------------- - * Pair patterns with termination conditions. The full list of patterns for - * a definition is merged with the TCs arising from the user-given clauses. - * There can be fewer clauses than the full list, if the user omitted some - * cases. This routine is used to prepare input for mk_induction. - *---------------------------------------------------------------------------*) -fun merge full_pats TCs = -let fun insert (p,TCs) = - let fun insrt ((x as (h,[]))::rst) = - if (p aconv h) then (p,TCs)::rst else x::insrt rst - | insrt (x::rst) = x::insrt rst - | insrt[] = raise TFL_ERR{func="merge.insert", - mesg="pattern not found"} - in insrt end - fun pass ([],ptcl_final) = ptcl_final - | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl) -in - pass (TCs, map (fn p => (p,[])) full_pats) -end; - - -fun givens pats = map pat_of (filter given pats); - -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 - val pats' = filter given pats - val given_pats = map pat_of pats' - val rows = map row_of_pat pats' - val WFR = #ant(S.dest_imp(concl corollary)) - val R = #Rand(S.dest_comb WFR) - val corollary' = R.UNDISCH corollary (* put WF R on assums *) - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') - given_pats - val (case_rewrites,context_congs) = extraction_thms theory - val corollaries' = map(rewrite_rule case_rewrites) corollaries - val extract = R.CONTEXT_REWRITE_RULE - (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) - val rules1 = R.LIST_CONJ(map mk_cond_rule rules0) - in - {theory = theory, (* holds def, if it's needed *) - rules = rules1, - rows = rows, - full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), - TCs = TCs} - end; - - -(*--------------------------------------------------------------------------- - * Perform the extraction without making the definition. Definition and - * extraction commute for the non-nested case. (Deferred recdefs) - * - * The purpose of wfrec_eqns is merely to instantiate the recursion theorem - * and extract termination conditions: no definition is made. - *---------------------------------------------------------------------------*) - -fun wfrec_eqns thy fid tflCongs eqns = - let val {lhs,rhs} = S.dest_eq (hd eqns) - val (f,args) = S.strip_comb lhs - val (fname,fty) = dest_atom f - val (SV,a) = front_last args (* SV = schematic variables *) - val g = list_comb(f,SV) - val h = Free(fname,type_of g) - val eqns1 = map (subst_free[(g,h)]) eqns - val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns1 - val given_pats = givens pats - (* val f = Free(Name,Ty) *) - val Type("fun", [f_dty, f_rty]) = Ty - val dummy = if Name<>fid then - raise TFL_ERR{func = "wfrec_eqns", - mesg = "Expected a definition of " ^ - quote fid ^ " but found one of " ^ - quote Name} - else () - val (case_rewrites,context_congs) = extraction_thms thy - val tych = Thry.typecheck thy - val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY - val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 - val R = Free (variant (foldr add_term_names (eqns,[])) Rname, - Rtype) - val WFREC_THM = R.ISPECL [tych R, tych g] 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 - fun extract X = R.CONTEXT_REWRITE_RULE - (f, R1::SV, cut_apply, tflCongs@context_congs) X - in {proto_def = proto_def, - SV=SV, - WFR=WFR, - pats=pats, - extracta = map extract corollaries'} - end; - - -(*--------------------------------------------------------------------------- - * Define the constant after extracting the termination conditions. The - * 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). - *---------------------------------------------------------------------------*) - -fun lazyR_def thy fid tflCongs eqns = - let val {proto_def,WFR,pats,extracta,SV} = - wfrec_eqns thy fid tflCongs eqns - val R1 = S.rand WFR - val f = #lhs(S.dest_eq 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 {lhs,rhs} = S.dest_eq proto_def' - val (c,args) = S.strip_comb lhs - val (Name,Ty) = dest_atom c - val defn = mk_const_def (Theory.sign_of thy) - (Name, Ty, S.list_mk_abs (args,rhs)) - val (theory, [def0]) = - thy - |> PureThy.add_defs_i false - [Thm.no_attributes (fid ^ "_def", defn)] - val def = freezeT def0; - 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 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 SV' = map tych SV; - val SVrefls = map reflexive SV' - val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x)) - SVrefls def) - RS meta_eq_to_obj_eq - val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 - 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, 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; - - - -(*---------------------------------------------------------------------------- - * - * INDUCTION THEOREM - * - *---------------------------------------------------------------------------*) - - -(*------------------------ Miscellaneous function -------------------------- - * - * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n] - * ----------------------------------------------------------- - * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]), - * ... - * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] ) - * - * This function is totally ad hoc. Used in the production of the induction - * theorem. The nchotomy theorem can have clauses that look like - * - * ?v1..vn. z = C vn..v1 - * - * in which the order of quantification is not the order of occurrence of the - * quantified variables as arguments to C. Since we have no control over this - * aspect of the nchotomy theorem, we make the correspondence explicit by - * pairing the incoming new variable with the term it gets beta-reduced into. - *---------------------------------------------------------------------------*) - -fun alpha_ex_unroll (xlist, tm) = - let val (qvars,body) = S.strip_exists tm - val vlist = #2(S.strip_comb (S.rhs body)) - val plist = ListPair.zip (vlist, xlist) - val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars - handle OPTION => error - "TFL fault [alpha_ex_unroll]: no correspondence" - fun build ex [] = [] - | build (_$rex) (v::rst) = - let val ex1 = betapply(rex, v) - in ex1 :: build ex1 rst - end - val (nex::exl) = rev (tm::build tm args) - in - (nex, ListPair.zip (args, rev exl)) - end; - - - -(*---------------------------------------------------------------------------- - * - * PROVING COMPLETENESS OF PATTERNS - * - *---------------------------------------------------------------------------*) - -fun mk_case ty_info usednames thy = - let - val divide = ipartition (gvvariant usednames) - val tych = Thry.typecheck thy - fun tych_binding(x,y) = (tych x, tych y) - fun fail s = raise TFL_ERR{func = "mk_case", mesg = s} - fun mk{rows=[],...} = fail"no rows" - | mk{path=[], rows = [([], (thm, bindings))]} = - R.IT_EXISTS (map tych_binding bindings) thm - | mk{path = u::rstp, rows as (p::_, _)::_} = - let val (pat_rectangle,rights) = ListPair.unzip rows - val col0 = map hd pat_rectangle - val pat_rectangle' = map tl pat_rectangle - in - if (forall is_Free col0) (* column 0 is all variables *) - then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)])) - (ListPair.zip (rights, col0)) - in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')} - end - else (* column 0 is all constructors *) - let val Type (ty_name,_) = type_of p - in - case (ty_info ty_name) - of None => fail("Not a known datatype: "^ty_name) - | Some{constructors,nchotomy} => - let val thm' = R.ISPEC (tych u) nchotomy - val disjuncts = S.strip_disj (concl thm') - val subproblems = divide(constructors, rows) - val groups = map #group subproblems - and new_formals = map #new_formals subproblems - val existentials = ListPair.map alpha_ex_unroll - (new_formals, disjuncts) - val constraints = map #1 existentials - val vexl = map #2 existentials - fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b)) - val news = map (fn (nf,rows,c) => {path = nf@rstp, - rows = map (expnd c) rows}) - (U.zip3 new_formals groups constraints) - val recursive_thms = map mk news - val build_exists = foldr - (fn((x,t), th) => - R.CHOOSE (tych x, R.ASSUME (tych t)) th) - val thms' = ListPair.map build_exists (vexl, recursive_thms) - val same_concls = R.EVEN_ORS thms' - in R.DISJ_CASESL thm' same_concls - end - end end - in mk - end; - - -fun complete_cases thy = - let val tych = Thry.typecheck thy - val ty_info = Thry.induct_info thy - in fn pats => - let val names = foldr add_term_names (pats,[]) - val T = type_of (hd pats) - val aname = Term.variant names "a" - val vname = Term.variant (aname::names) "v" - val a = Free (aname, T) - val v = Free (vname, T) - val a_eq_v = HOLogic.mk_eq(a,v) - val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a) - (R.REFL (tych a)) - val th0 = R.ASSUME (tych a_eq_v) - val rows = map (fn x => ([x], (th0,[]))) pats - in - R.GEN (tych a) - (R.RIGHT_ASSOC - (R.CHOOSE(tych v, ex_th0) - (mk_case ty_info (vname::aname::names) - thy {path=[v], rows=rows}))) - end end; - - -(*--------------------------------------------------------------------------- - * Constructing induction hypotheses: one for each recursive call. - * - * Note. R will never occur as a variable in the ind_clause, because - * to do so, it would have to be from a nested definition, and we don't - * allow nested defns to have R variable. - * - * 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 -fun build_ih f P (pat,TCs) = - let val globals = S.free_vars_lr pat - 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 (* FIXME do not handle _ !!! *) - in (S.list_mk_forall(locals,imp), (tm,locals)) end - end - in case TCs - of [] => (S.list_mk_forall(globals, 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(globals,ind_clause), TCs_locals) - 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 (* FIXME do not handle _ !!! *) - 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". - * - * Input is tm = "(!y. R y pat ==> P y) ==> P pat", - * TCs = TC_1[pat] ... TC_n[pat] - * thm = ih1 /\ ... /\ ih_n |- ih[pat] - *---------------------------------------------------------------------------*) -fun prove_case f thy (tm,TCs_locals,thm) = - let val tych = Thry.typecheck thy - val antc = tych(#ant(S.dest_imp tm)) - val thm' = R.SPEC_ALL thm - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm) - fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) - fun mk_ih ((TC,locals),th2,nested) = - R.GENL (map tych locals) - (if nested - then R.DISCH (get_cntxt TC) th2 handle _ => th2 (* FIXME do not handle _ !!! *) - else if S.is_imp(concl TC) - then R.IMP_TRANS TC th2 - else R.MP th2 TC) - in - R.DISCH antc - (if S.is_imp(concl thm') (* recursive calls in this clause *) - then let val th1 = R.ASSUME antc - val TCs = map #1 TCs_locals - val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o - #2 o S.strip_forall) TCs - val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs)) - TCs_locals - val th2list = map (U.C R.SPEC th1 o tych) ylist - val nlist = map nested TCs - val triples = U.zip3 TClist th2list nlist - val Pylist = map mk_ih triples - in R.MP thm' (R.LIST_CONJ Pylist) end - else thm') - end; - - -(*--------------------------------------------------------------------------- - * - * x = (v1,...,vn) |- M[x] - * --------------------------------------------- - * ?v1 ... vn. x = (v1,...,vn) |- M[x] - * - *---------------------------------------------------------------------------*) -fun LEFT_ABS_VSTRUCT tych thm = - let fun CHOOSER v (tm,thm) = - let val ex_tm = S.mk_exists{Bvar=v,Body=tm} - in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm) - end - val [veq] = filter (U.can S.dest_eq) (#1 (R.dest_thm thm)) - val {lhs,rhs} = S.dest_eq veq - val L = S.free_vars_lr rhs - in #2 (U.itlist CHOOSER L (veq,thm)) end; - - -(*---------------------------------------------------------------------------- - * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)] - * - * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove - * recursion induction (Rinduct) by proving the antecedent of Sinduct from - * the antecedent of Rinduct. - *---------------------------------------------------------------------------*) -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 - val case_thm = complete_cases thy pats - val domain = (type_of o hd) pats - val Pname = Term.variant (foldr (foldr add_term_names) - (pats::TCsl, [])) "P" - 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 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 fconst thy) tasks - val v = Free (variant (foldr add_term_names (map concl proved_cases, [])) - "v", - domain) - val vtyped = tych v - val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats - val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') - (substs, proved_cases) - val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1 - val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases) - val dc = R.MP Sinduct dant - val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc))) - val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty) - val dc' = U.itlist (R.GEN o tych) vars - (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc) -in - R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') -end -handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"}; (* FIXME do not handle _ !!! *) - - - - -(*--------------------------------------------------------------------------- - * - * POST PROCESSING - * - *---------------------------------------------------------------------------*) - - -fun simplify_induction thy hth ind = - let val tych = Thry.typecheck thy - val (asl,_) = R.dest_thm ind - val (_,tc_eq_tc') = R.dest_thm hth - val tc = S.lhs tc_eq_tc' - fun loop [] = ind - | loop (asm::rst) = - if (U.can (Thry.match_term thy asm) tc) - then R.UNDISCH - (R.MATCH_MP - (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind)) - hth) - else loop rst - in loop asl -end; - - -(*--------------------------------------------------------------------------- - * The termination condition is an antecedent to the rule, and an - * assumption to the theorem. - *---------------------------------------------------------------------------*) -fun elim_tc tcthm (rule,induction) = - (R.MP rule tcthm, R.PROVE_HYP tcthm induction) - - -fun postprocess{wf_tac, terminator, simplifier} theory {rules,induction,TCs} = -let val tych = Thry.typecheck theory - - (*--------------------------------------------------------------------- - * Attempt to eliminate WF condition. It's the only assumption of rules - *---------------------------------------------------------------------*) - val (rules1,induction1) = - let val thm = R.prove(tych(HOLogic.mk_Trueprop - (hd(#1(R.dest_thm rules)))), - wf_tac) - in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction) - end handle _ => (rules,induction) (* FIXME do not handle _ !!! *) - - (*---------------------------------------------------------------------- - * The termination condition (tc) is simplified to |- tc = tc' (there - * might not be a change!) and then 3 attempts are made: - * - * 1. if |- tc = T, then eliminate it with eqT; otherwise, - * 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 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 _ => (* FIXME do not handle _ !!! *) - (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), - terminator))) - (r,ind) - handle _ => (* FIXME do not handle _ !!! *) - (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), - simplify_induction theory tc_eq ind)) - end - - (*---------------------------------------------------------------------- - * Nested termination conditions are harder to get at, since they are - * left embedded in the body of the function (and in induction - * theorem hypotheses). Our "solution" is to simplify them, and try to - * prove termination, but leave the application of the resulting theorem - * to a higher level. So things go much as in "simplify_tc": the - * termination condition (tc) is simplified to |- tc = tc' (there might - * not be a change) and then 2 attempts are made: - * - * 1. if |- tc = T, then return |- tc; otherwise, - * 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else - * 3. return |- tc = tc' - *---------------------------------------------------------------------*) - fun simplify_nested_tc tc = - let val tc_eq = simplifier (tych (#2 (S.strip_forall tc))) - in - R.GEN_ALL - (R.MATCH_MP Thms.eqT tc_eq - handle _ (* FIXME do not handle _ !!! *) - => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))), - terminator)) - handle _ => tc_eq)) (* FIXME do not handle _ !!! *) - end - - (*------------------------------------------------------------------- - * Attempt to simplify the termination conditions in each rule and - * in the induction theorem. - *-------------------------------------------------------------------*) - fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm - fun loop ([],extras,R,ind) = (rev R, ind, extras) - | loop ((r,ftcs)::rst, nthms, R, ind) = - let val tcs = #1(strip_imp (concl r)) - val extra_tcs = gen_rems (op aconv) (ftcs, tcs) - val extra_tc_thms = map simplify_nested_tc extra_tcs - val (r1,ind1) = U.rev_itlist simplify_tc tcs (r,ind) - val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1 - in loop(rst, nthms@extra_tc_thms, r2::R, ind1) - end - val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs) - val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1) -in - {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras} -end; - -end; diff -r b0d961105f46 -r 856773b19058 TFL/thms.sml --- a/TFL/thms.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* Title: TFL/thms.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -signature Thms_sig = -sig - val WF_INDUCTION_THM: thm - val WFREC_COROLLARY: thm - val CUT_DEF: thm - val SELECT_AX: thm - val eqT: thm - val rev_eq_mp: thm - val simp_thm: thm -end; - -structure Thms: Thms_sig = -struct - val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec"; - val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct"; - val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def"; - - val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)" - (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]); - - fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); - - val eqT = prove"(x = True) --> x"; - val rev_eq_mp = prove"(x = y) --> y --> x"; - val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)"; -end; diff -r b0d961105f46 -r 856773b19058 TFL/thry.sml --- a/TFL/thry.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -(* Title: TFL/thry.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -signature Thry_sig = -sig - val match_term : theory -> term -> term - -> (term*term)list * (typ*typ)list - - val match_type : theory -> typ -> typ -> (typ*typ)list - - val typecheck : theory -> term -> cterm - - (* Datatype facts of various flavours *) - val match_info: theory -> string -> {constructors:term list, - case_const:term} option - - val induct_info: theory -> string -> {constructors:term list, - nchotomy:thm} option - - val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list} - -end; - - -structure Thry : Thry_sig (* LThry_sig *) = -struct - -structure S = USyntax; - -fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg}; - -(*--------------------------------------------------------------------------- - * Matching - *---------------------------------------------------------------------------*) - -local fun tybind (x,y) = (TVar (x,["term"]) , y) - fun tmbind (x,y) = (Var (x,type_of y), y) -in - fun match_term thry pat ob = - let val tsig = #tsig(Sign.rep_sg(Theory.sign_of thry)) - val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) - in (map tmbind tm_theta, map tybind ty_theta) - end - - fun match_type thry pat ob = map tybind (Vartab.dest - (Type.typ_match (#tsig(Sign.rep_sg(Theory.sign_of thry))) (Vartab.empty, (pat,ob)))) -end; - - -(*--------------------------------------------------------------------------- - * Typing - *---------------------------------------------------------------------------*) - -fun typecheck thry = Thm.cterm_of (Theory.sign_of thry); - - -(*--------------------------------------------------------------------------- - * Get information about datatypes - *---------------------------------------------------------------------------*) - -fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty); - -fun match_info thy tname = - case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of - (Some case_const, Some constructors) => - Some {case_const = case_const, constructors = constructors} - | _ => None; - -fun induct_info thy tname = case get_info thy tname of - None => None - | Some {nchotomy, ...} => - Some {nchotomy = nchotomy, - constructors = the (DatatypePackage.constrs_of thy tname)}; - -fun extract_info thy = - let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy)) - in {case_congs = map (mk_meta_eq o #case_cong) infos, - case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)} - end; - -end; (* Thry *) diff -r b0d961105f46 -r 856773b19058 TFL/usyntax.sml --- a/TFL/usyntax.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,416 +0,0 @@ -(* Title: TFL/usyntax.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Emulation of HOL's abstract syntax functions. -*) - -signature USyntax_sig = -sig - datatype lambda = VAR of {Name : string, Ty : typ} - | CONST of {Name : string, Ty : typ} - | COMB of {Rator: term, Rand : term} - | LAMB of {Bvar : term, Body : term} - - val alpha : typ - - (* Types *) - val type_vars : typ -> typ list - val type_varsl : typ list -> typ list - val mk_vartype : string -> typ - val is_vartype : typ -> bool - val strip_prod_type : typ -> typ list - - (* Terms *) - val free_vars_lr : term -> term list - val type_vars_in_term : term -> typ list - val dest_term : term -> lambda - - (* Prelogic *) - val inst : (typ*typ) list -> term -> term - - (* Construction routines *) - val mk_abs :{Bvar : term, Body : term} -> term - - val mk_imp :{ant : term, conseq : term} -> term - val mk_select :{Bvar : term, Body : term} -> term - val mk_forall :{Bvar : term, Body : term} -> term - val mk_exists :{Bvar : term, Body : term} -> term - val mk_conj :{conj1 : term, conj2 : term} -> term - val mk_disj :{disj1 : term, disj2 : term} -> term - val mk_pabs :{varstruct : term, body : term} -> term - - (* Destruction routines *) - val dest_const: term -> {Name : string, Ty : typ} - val dest_comb : term -> {Rator : term, Rand : term} - val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list - val dest_eq : term -> {lhs : term, rhs : term} - val dest_imp : term -> {ant : term, conseq : term} - val dest_forall : term -> {Bvar : term, Body : term} - val dest_exists : term -> {Bvar : term, Body : term} - val dest_neg : term -> term - val dest_conj : term -> {conj1 : term, conj2 : term} - val dest_disj : term -> {disj1 : term, disj2 : term} - val dest_pair : term -> {fst : term, snd : term} - val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list} - - val lhs : term -> term - val rhs : term -> term - val rand : term -> term - - (* Query routines *) - val is_imp : term -> bool - val is_forall : term -> bool - val is_exists : term -> bool - val is_neg : term -> bool - val is_conj : term -> bool - val is_disj : term -> bool - val is_pair : term -> bool - val is_pabs : term -> bool - - (* Construction of a term from a list of Preterms *) - val list_mk_abs : (term list * term) -> term - val list_mk_imp : (term list * term) -> term - val list_mk_forall : (term list * term) -> term - val list_mk_conj : term list -> term - - (* Destructing a term to a list of Preterms *) - val strip_comb : term -> (term * term list) - val strip_abs : term -> (term list * term) - val strip_imp : term -> (term list * term) - val strip_forall : term -> (term list * term) - val strip_exists : term -> (term list * term) - val strip_disj : term -> term list - - (* Miscellaneous *) - val mk_vstruct : typ -> term list -> term - val gen_all : term -> term - val find_term : (term -> bool) -> term -> term option - val dest_relation : term -> term * term * term - val is_WFR : term -> bool - val ARB : typ -> term -end; - - -structure USyntax : USyntax_sig = -struct - -open Utils; - -infix 4 ##; - -fun USYN_ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg}; - - -(*--------------------------------------------------------------------------- - * - * Types - * - *---------------------------------------------------------------------------*) -val mk_prim_vartype = TVar; -fun mk_vartype s = mk_prim_vartype((s,0),["term"]); - -(* But internally, it's useful *) -fun dest_vtype (TVar x) = x - | dest_vtype _ = raise USYN_ERR{func = "dest_vtype", - mesg = "not a flexible type variable"}; - -val is_vartype = Utils.can dest_vtype; - -val type_vars = map mk_prim_vartype o typ_tvars -fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []); - -val alpha = mk_vartype "'a" -val beta = mk_vartype "'b" - -val strip_prod_type = HOLogic.prodT_factors; - - - -(*--------------------------------------------------------------------------- - * - * Terms - * - *---------------------------------------------------------------------------*) - -(* Free variables, in order of occurrence, from left to right in the - * syntax tree. *) -fun free_vars_lr tm = - let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end - fun add (t, frees) = case t of - Free _ => if (memb t frees) then frees else t::frees - | Abs (_,_,body) => add(body,frees) - | f$t => add(t, add(f, frees)) - | _ => frees - in rev(add(tm,[])) - end; - - - -val type_vars_in_term = map mk_prim_vartype o term_tvars; - - - -(* Prelogic *) -fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) -fun inst theta = subst_vars (map dest_tybinding theta,[]) - - -(* Construction routines *) - -fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) - | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) - | mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; - - -fun mk_imp{ant,conseq} = - let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[ant,conseq]) - end; - -fun mk_select (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("Eps",(ty --> HOLogic.boolT) --> ty) - in list_comb(c,[mk_abs r]) - end; - -fun mk_forall (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) - in list_comb(c,[mk_abs r]) - end; - -fun mk_exists (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) - in list_comb(c,[mk_abs r]) - end; - - -fun mk_conj{conj1,conj2} = - let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[conj1,conj2]) - end; - -fun mk_disj{disj1,disj2} = - let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[disj1,disj2]) - end; - -fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); - -local -fun mk_uncurry(xt,yt,zt) = - Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} - | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"} -fun is_var(Var(_)) = true | is_var (Free _) = true | is_var _ = false -in -fun mk_pabs{varstruct,body} = - let fun mpa(varstruct,body) = - if (is_var varstruct) - then mk_abs{Bvar = varstruct, Body = body} - else let val {fst,snd} = dest_pair varstruct - in mk_uncurry(type_of fst,type_of snd,type_of body) $ - mpa(fst,mpa(snd,body)) - end - in mpa(varstruct,body) - end - handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""}; (* FIXME do not handle _ !!! *) -end; - -(* Destruction routines *) - -datatype lambda = VAR of {Name : string, Ty : typ} - | CONST of {Name : string, Ty : typ} - | COMB of {Rator: term, Rand : term} - | LAMB of {Bvar : term, Body : term}; - - -fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} - | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} - | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} - | dest_term(M$N) = COMB{Rator=M,Rand=N} - | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) - in LAMB{Bvar = v, Body = betapply (M,v)} - end - | dest_term(Bound _) = raise USYN_ERR{func = "dest_term",mesg = "Bound"}; - -fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} - | dest_const _ = raise USYN_ERR{func = "dest_const", mesg = "not a constant"}; - -fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} - | dest_comb _ = raise USYN_ERR{func = "dest_comb", mesg = "not a comb"}; - -fun dest_abs used (a as Abs(s, ty, M)) = - let - val s' = variant used s; - val v = Free(s', ty); - in ({Bvar = v, Body = betapply (a,v)}, s'::used) - end - | dest_abs _ _ = raise USYN_ERR{func = "dest_abs", mesg = "not an abstraction"}; - -fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} - | dest_eq _ = raise USYN_ERR{func = "dest_eq", mesg = "not an equality"}; - -fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} - | dest_imp _ = raise USYN_ERR{func = "dest_imp", mesg = "not an implication"}; - -fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a) - | dest_forall _ = raise USYN_ERR{func = "dest_forall", mesg = "not a forall"}; - -fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a) - | dest_exists _ = raise USYN_ERR{func = "dest_exists", mesg="not an existential"}; - -fun dest_neg(Const("not",_) $ M) = M - | dest_neg _ = raise USYN_ERR{func = "dest_neg", mesg = "not a negation"}; - -fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} - | dest_conj _ = raise USYN_ERR{func = "dest_conj", mesg = "not a conjunction"}; - -fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} - | dest_disj _ = raise USYN_ERR{func = "dest_disj", mesg = "not a disjunction"}; - -fun mk_pair{fst,snd} = - let val ty1 = type_of fst - val ty2 = type_of snd - val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) - in list_comb(c,[fst,snd]) - end; - -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} - | dest_pair _ = raise USYN_ERR{func = "dest_pair", mesg = "not a pair"}; - - -local fun ucheck t = (if #Name(dest_const t) = "split" then t - else raise Match) -in -fun dest_pabs used tm = - let val ({Bvar,Body}, used') = dest_abs used tm - in {varstruct = Bvar, body = Body, used = used'} - end - handle (* FIXME do not handle _ !!! *) - _ => let val {Rator,Rand} = dest_comb tm - val _ = ucheck Rator - val {varstruct = lv, body, used = used'} = dest_pabs used Rand - val {varstruct = rv, body, used = used''} = dest_pabs used' body - in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} - end -end; - - -val lhs = #lhs o dest_eq -val rhs = #rhs o dest_eq -val rand = #Rand o dest_comb - - -(* Query routines *) -val is_imp = can dest_imp -val is_forall = can dest_forall -val is_exists = can dest_exists -val is_neg = can dest_neg -val is_conj = can dest_conj -val is_disj = can dest_disj -val is_pair = can dest_pair -val is_pabs = can (dest_pabs []) - - -(* Construction of a cterm from a list of Terms *) - -fun list_mk_abs(L,tm) = itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; - -(* These others are almost never used *) -fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; -fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t; -val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) - - -(* Need to reverse? *) -fun gen_all tm = list_mk_forall(term_frees tm, tm); - -(* Destructing a cterm to a list of Terms *) -fun strip_comb tm = - let fun dest(M$N, A) = dest(M, N::A) - | dest x = x - in dest(tm,[]) - end; - -fun strip_abs(tm as Abs _) = - let val ({Bvar,Body}, _) = dest_abs [] tm - val (bvs, core) = strip_abs Body - in (Bvar::bvs, core) - end - | strip_abs M = ([],M); - - -fun strip_imp fm = - if (is_imp fm) - then let val {ant,conseq} = dest_imp fm - val (was,wb) = strip_imp conseq - in ((ant::was), wb) - end - else ([],fm); - -fun strip_forall fm = - if (is_forall fm) - then let val {Bvar,Body} = dest_forall fm - val (bvs,core) = strip_forall Body - in ((Bvar::bvs), core) - end - else ([],fm); - - -fun strip_exists fm = - if (is_exists fm) - then let val {Bvar, Body} = dest_exists fm - val (bvs,core) = strip_exists Body - in (Bvar::bvs, core) - end - else ([],fm); - -fun strip_disj w = - if (is_disj w) - then let val {disj1,disj2} = dest_disj w - in (strip_disj disj1@strip_disj disj2) - end - else [w]; - - -(* Miscellaneous *) - -fun mk_vstruct ty V = - let fun follow_prod_type (Type("*",[ty1,ty2])) vs = - let val (ltm,vs1) = follow_prod_type ty1 vs - val (rtm,vs2) = follow_prod_type ty2 vs1 - in (mk_pair{fst=ltm, snd=rtm}, vs2) end - | follow_prod_type _ (v::vs) = (v,vs) - in #1 (follow_prod_type ty V) end; - - -(* Search a term for a sub-term satisfying the predicate p. *) -fun find_term p = - let fun find tm = - if (p tm) then Some tm - else case tm of - Abs(_,_,body) => find body - | (t$u) => (Some (the (find t)) handle _ => find u) (* FIXME do not handle _ !!! *) - | _ => None - in find - end; - -fun dest_relation tm = - if (type_of tm = HOLogic.boolT) - then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm - in (R,y,x) - end handle _ => raise USYN_ERR{func="dest_relation", - mesg="unexpected term structure"} (* FIXME do not handle _ !!! *) - else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"}; - -fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true - | is_WFR _ = false; - -fun ARB ty = mk_select{Bvar=Free("v",ty), - Body=Const("True",HOLogic.boolT)}; - -end; (* Syntax *) diff -r b0d961105f46 -r 856773b19058 TFL/utils.sml --- a/TFL/utils.sml Thu Jan 04 18:13:27 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -(* Title: TFL/utils.sml - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Basic utilities. -*) - -signature Utils_sig = -sig - exception ERR of {module:string,func:string, mesg:string} - - val can : ('a -> 'b) -> 'a -> bool - val holds : ('a -> bool) -> 'a -> bool - val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c - - val itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b - val rev_itlist : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b - val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a - val itlist2 :('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val pluck : ('a -> bool) -> 'a list -> 'a * 'a list - val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list - val take : ('a -> 'b) -> int * 'a list -> 'b list - val sort : ('a -> 'a -> bool) -> 'a list -> 'a list - -end; - - -structure Utils = -struct - -(* Standard exception for TFL. *) -exception ERR of {module:string,func:string, mesg:string}; -fun UTILS_ERR{func,mesg} = ERR{module = "Utils",func=func,mesg=mesg}; - - -(* Simple combinators *) - -fun C f x y = f y x - -fun itlist f L base_value = - let fun it [] = base_value - | it (a::rst) = f a (it rst) - in it L - end; - -fun rev_itlist f = - let fun rev_it [] base = base - | rev_it (a::rst) base = rev_it rst (f a base) - in rev_it - end; - -fun end_itlist f = - let fun endit [] = raise UTILS_ERR{func="end_itlist", mesg="list too short"} - | endit alist = - let val (base::ralist) = rev alist - in itlist f (rev ralist) base - end - in endit - end; - -fun itlist2 f L1 L2 base_value = - let fun it ([],[]) = base_value - | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) - | it _ = raise UTILS_ERR{func="itlist2",mesg="different length lists"} - in it (L1,L2) - end; - -fun pluck p = - let fun remv ([],_) = raise UTILS_ERR{func="pluck",mesg = "item not found"} - | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) - in fn L => remv(L,[]) - end; - -fun take f = - let fun grab(0,L) = [] - | grab(n, x::rst) = f x::grab(n-1,rst) - in grab - end; - -fun zip3 [][][] = [] - | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 - | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"}; - - -fun can f x = (f x ; true) handle _ => false; (* FIXME do not handle _ !!! *) -fun holds P x = P x handle _ => false; (* FIXME do not handle _ !!! *) - - -fun sort R = -let fun part (m, []) = ([],[]) - | part (m, h::rst) = - let val (l1,l2) = part (m,rst) - in if (R h m) then (h::l1, l2) - else (l1, h::l2) end - fun qsort [] = [] - | qsort (h::rst) = - let val (l1,l2) = part(h,rst) - in qsort l1@ [h] @qsort l2 - end -in qsort -end; - - -end;