# HG changeset patch # User paulson # Date 864121797 -7200 # Node ID 241838c01cafa0c01f5bc86a953ffa8f79765c64 # Parent 71b760618f30daba567fa96bf634cab83add3420 Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable diff -r 71b760618f30 -r 241838c01caf TFL/dcterm.sml --- a/TFL/dcterm.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/dcterm.sml Tue May 20 11:49:57 1997 +0200 @@ -4,9 +4,6 @@ structure Dcterm : sig - val caconv : cterm -> cterm -> bool - val mk_eq : cterm * cterm -> cterm - val mk_imp : cterm * cterm -> cterm val mk_conj : cterm * cterm -> cterm val mk_disj : cterm * cterm -> cterm val mk_select : cterm * cterm -> cterm @@ -40,12 +37,9 @@ val is_pair : cterm -> bool val is_select : cterm -> bool val is_var : cterm -> bool - val list_mk_comb : cterm * cterm list -> cterm val list_mk_abs : cterm list -> cterm -> cterm - val list_mk_imp : cterm list * cterm -> cterm val list_mk_exists : cterm list * cterm -> cterm val list_mk_forall : cterm list * cterm -> cterm - val list_mk_conj : cterm list -> cterm val list_mk_disj : cterm list -> cterm val strip_abs : cterm -> cterm list * cterm val strip_comb : cterm -> cterm * cterm list @@ -68,7 +62,6 @@ val can = Utils.can; val quote = Utils.quote; fun swap (x,y) = (y,x); -val bool = Type("bool",[]); fun itlist f L base_value = let fun it [] = base_value @@ -76,24 +69,7 @@ in it L end; -fun end_itlist f = -let fun endit [] = raise ERR"end_itlist" "list too short" - | endit alist = - let val (base::ralist) = rev alist - in itlist f (rev ralist) base end -in endit -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; - -(*--------------------------------------------------------------------------- - * Alpha conversion. - *---------------------------------------------------------------------------*) -fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2)); +val end_itlist = Utils.end_itlist; (*--------------------------------------------------------------------------- @@ -103,44 +79,30 @@ fun mk_const sign pr = cterm_of sign (Const pr); val mk_hol_const = mk_const (sign_of HOL.thy); -fun list_mk_comb (h,[]) = h - | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h; - - -fun mk_eq(lhs,rhs) = - let val ty = #T(rep_cterm lhs) - val c = mk_hol_const("op =", ty --> ty --> bool) - in list_mk_comb(c,[lhs,rhs]) - end; - -local val c = mk_hol_const("op -->", bool --> bool --> bool) -in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq]) -end; - fun mk_select (r as (Bvar,Body)) = let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("Eps", (ty --> bool) --> ty) + val c = mk_hol_const("Eps", (ty --> HOLogic.boolT) --> ty) in capply c (uncurry cabs r) end; fun mk_forall (r as (Bvar,Body)) = let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("All", (ty --> bool) --> bool) + val c = mk_hol_const("All", (ty --> HOLogic.boolT) --> HOLogic.boolT) in capply c (uncurry cabs r) end; fun mk_exists (r as (Bvar,Body)) = let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("Ex", (ty --> bool) --> bool) + 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 &", bool --> bool --> bool) +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 |", bool --> bool --> bool) +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; @@ -226,10 +188,8 @@ *---------------------------------------------------------------------------*) val list_mk_abs = itlist cabs; -fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c; fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t; fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t; -val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm)) val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm)) (*--------------------------------------------------------------------------- diff -r 71b760618f30 -r 241838c01caf TFL/post.sml --- a/TFL/post.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/post.sml Tue May 20 11:49:57 1997 +0200 @@ -1,3 +1,11 @@ +(*------------------------------------------------------------------------- +there are 3 postprocessors that get applied to the definition: + + - a wellfoundedness prover (WF_TAC) + - a simplifier (tries to eliminate the language of termination expressions) + - a termination prover +*-------------------------------------------------------------------------*) + signature TFL = sig structure Prim : TFL_sig @@ -38,7 +46,7 @@ * have a tactic directly applied to them. *--------------------------------------------------------------------------*) fun termination_goals rules = - map (Logic.freeze_vars o S.drop_Trueprop) + map (Logic.freeze_vars o HOLogic.dest_Trueprop) (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); (*--------------------------------------------------------------------------- @@ -48,26 +56,23 @@ fun tgoalw thy defs rules = let val L = termination_goals rules open USyntax - val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L)) + val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L)) in goalw_cterm defs g end; - val tgoal = Utils.C tgoalw []; + fun tgoal thy = tgoalw thy []; (*--------------------------------------------------------------------------- * Simple wellfoundedness prover. *--------------------------------------------------------------------------*) fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) - val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, - wf_pred_nat, wf_pred_list, wf_trancl]; + val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, + wf_pred_list, wf_trancl]; - val terminator = simp_tac(!simpset addsimps [less_than_def, pred_nat_def, - pred_list_def]) 1 + val terminator = simp_tac(!simpset addsimps [less_Suc_eq, pred_list_def]) 1 THEN TRY(best_tac - (!claset addSDs [not0_implies_Suc] - addIs [r_into_trancl, - trans_trancl RS transD] - addss (!simpset)) 1); + (!claset addSDs [not0_implies_Suc] + addss (!simpset)) 1); val simpls = [less_eq RS eq_reflection, lex_prod_def, rprod_def, measure_def, inv_image_def]; @@ -83,7 +88,7 @@ simplifier = Prim.Rules.simpl_conv simpls}; val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ - [less_than_def, pred_nat_def, pred_list_def]); + [pred_list_def]); fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); @@ -102,12 +107,12 @@ end; (*lcp's version: takes strings; doesn't return "thm" - (whose signature is a draft and therefore useless) *) + (whose signature is a draft and therefore useless) *) fun define thy R eqs = let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) val (thy',(_,pats)) = - define_i thy (read thy R) - (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) + define_i thy (read thy R) + (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) in (thy',pats) end handle Utils.ERR {mesg,...} => error mesg; @@ -134,7 +139,7 @@ Const("==",_)$_$_ => r | _$(Const("op =",_)$_$_) => r RS eq_reflection | _ => r RS P_imp_P_eq_True -fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L)) +fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss)) fun join_assums th = @@ -143,7 +148,7 @@ 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 = U.union S.aconv cntxtl cntxtr + val cntxt = gen_union (op aconv) (cntxtl, cntxtr) in R.GEN_ALL (R.DISCH_ALL @@ -198,22 +203,22 @@ fun simplify_defn (thy,(id,pats)) = let val dummy = deny (id mem map ! (stamps_of_thy thy)) ("Recursive definition " ^ id ^ - " would clash with the theory of the same name!") + " would clash with the theory of the same name!") val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) val {theory,rules,TCs,full_pats_TCs,patterns} = - Prim.post_definition (thy,(def,pats)) + Prim.post_definition (thy,(def,pats)) val {lhs=f,rhs} = S.dest_eq(concl def) val (_,[R,_]) = S.strip_comb rhs val {induction, rules, tcs} = proof_stage theory reducer - {f = f, R = R, rules = rules, - full_pats_TCs = full_pats_TCs, - TCs = TCs} + {f = f, R = R, rules = rules, + full_pats_TCs = full_pats_TCs, + TCs = TCs} val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules) in {induct = meta_outer - (normalize_thm [RSspec,RSmp] (induction RS spec')), - rules = rules', - tcs = (termination_goals rules') @ tcs} + (normalize_thm [RSspec,RSmp] (induction RS spec')), + rules = rules', + tcs = (termination_goals rules') @ tcs} end handle Utils.ERR {mesg,...} => error mesg end; diff -r 71b760618f30 -r 241838c01caf TFL/rules.new.sml --- a/TFL/rules.new.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/rules.new.sml Tue May 20 11:49:57 1997 +0200 @@ -10,23 +10,16 @@ structure U = Utils; structure D = Dcterm; -type Type = USyntax.Type -type Preterm = USyntax.Preterm -type Term = USyntax.Term -type Thm = Thm.thm -type Tactic = tactic; fun RULES_ERR{func,mesg} = Utils.ERR{module = "FastRules",func=func,mesg=mesg}; -nonfix ##; val ## = Utils.##; infix 4 ##; 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 drop = S.drop_Trueprop - val {prop,hyps,...} = rep_thm thm - in (map drop hyps, drop prop) + let val {prop,hyps,...} = rep_thm thm + in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end; @@ -46,11 +39,9 @@ in equal_elim (transitive ctm2_eq ctm1_eq) thm end; -val BETA_RULE = Utils.I; - (*---------------------------------------------------------------------------- - * Type instantiation + * typ instantiation *---------------------------------------------------------------------------*) fun INST_TYPE blist thm = let val {sign,...} = rep_thm thm @@ -82,9 +73,9 @@ fun FILTER_DISCH_ALL P thm = - let fun check tm = U.holds P (S.drop_Trueprop (#t(rep_cterm tm))) - in U.itlist (fn tm => fn th => if (check tm) then DISCH tm th else th) - (chyps thm) 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! *) @@ -97,10 +88,10 @@ 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 _ = by (rtac impI 1) - val _ = by (rtac (p2 RS mp) 1) - val _ = by (rtac (p1 RS mp) 1) - val _ = by (assume_tac 1) + 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) @@ -167,11 +158,11 @@ * *---------------------------------------------------------------------------*) local val [p1,p2,p3] = goal HOL.thy "(P | Q) ==> (P --> R) ==> (Q --> R) ==> R" - val _ = by (rtac (p1 RS disjE) 1) - val _ = by (rtac (p2 RS mp) 1) - val _ = by (assume_tac 1) - val _ = by (rtac (p3 RS mp) 1) - val _ = by (assume_tac 1) + 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 = @@ -215,7 +206,9 @@ (* freezeT expensive! *) fun DISJ_CASESL disjth thl = let val c = cconcl disjth - fun eq th atm = exists (D.caconv atm) (chyps th) + 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 @@ -262,7 +255,7 @@ 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, S.drop_Trueprop rst) (* get rid of trueprop *) + 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 @@ -289,8 +282,8 @@ let val fth = freezeT th val {prop,sign,...} = rep_thm fth fun mk_inst (Var(v,T)) = - (cterm_of sign (Var(v,T)), - cterm_of sign (Free(string_of v, T))) + (cterm_of sign (Var(v,T)), + cterm_of sign (Free(string_of v, T))) val insts = map mk_inst (term_vars prop) in instantiate ([],insts) fth end @@ -318,10 +311,10 @@ *---------------------------------------------------------------------------*) local val [p1,p2] = goal HOL.thy "(? x. P x) ==> (!x. P x --> Q) ==> Q" - val _ = by (rtac (p1 RS exE) 1) - val _ = by (rtac ((p2 RS allE) RS mp) 1) - val _ = by (assume_tac 2) - val _ = by (assume_tac 1) + 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 = @@ -378,7 +371,7 @@ in U.itlist (fn (b as (r1 |-> r2)) => fn thm => - EXISTS(?r2(S.subst[b] (S.drop_Trueprop(#prop(rep_thm thm)))), tych r1) + EXISTS(?r2(S.subst[b] (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) thm) blist' th end; @@ -426,10 +419,6 @@ *---------------------------------------------------------------------------*) - -val bool = S.bool -val prop = Type("prop",[]); - (* Object language quantifier, i.e., "!" *) fun Forall v M = S.mk_forall{Bvar=v, Body=M}; @@ -452,8 +441,8 @@ | dest_equal tm = S.dest_eq tm; -fun get_rhs tm = #rhs(dest_equal (S.drop_Trueprop tm)); -fun get_lhs tm = #lhs(dest_equal (S.drop_Trueprop tm)); +fun get_rhs tm = #rhs(dest_equal (HOLogic.dest_Trueprop tm)); +fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); fun variants FV vlist = rev(#1(U.rev_itlist (fn v => fn (V,W) => @@ -589,17 +578,11 @@ local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end fun mk_fst tm = - let val ty = S.type_of tm - val {Tyop="*",Args=[fty,sty]} = S.dest_type ty - val fst = S.mk_const{Name="fst",Ty = ty --> fty} - in S.mk_comb{Rator=fst, Rand=tm} - end + let val ty as Type("*", [fty,sty]) = type_of tm + in Const ("fst", ty --> fty) $ tm end fun mk_snd tm = - let val ty = S.type_of tm - val {Tyop="*",Args=[fty,sty]} = S.dest_type ty - val snd = S.mk_const{Name="snd",Ty = ty --> sty} - in S.mk_comb{Rator=snd, Rand=tm} - end + 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 = @@ -622,7 +605,7 @@ fun VSTRUCT_ELIM tych a vstr th = let val L = S.free_vars_lr vstr - val bind1 = tych (S.mk_prop (S.mk_eq{lhs=a, rhs=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 @@ -648,7 +631,7 @@ *---------------------------------------------------------------------------*) fun dest_pbeta_redex M n = let val (f,args) = dest_combn M n - val _ = dest_aabs f + val dummy = dest_aabs f in (strip_aabs f,args) end; @@ -666,30 +649,30 @@ fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} = let val tc_list = ref[]: term list ref - val _ = term_ref := [] - val _ = thm_ref := [] - val _ = mss_ref := [] + val dummy = term_ref := [] + val dummy = thm_ref := [] + val dummy = mss_ref := [] val cut_lemma' = (cut_lemma RS mp) RS eq_reflection fun prover mss thm = let fun cong_prover mss thm = - let val _ = say "cong_prover:\n" + let val dummy = say "cong_prover:\n" val cntxt = prems_of_mss mss - val _ = print_thms "cntxt:\n" cntxt - val _ = say "cong rule:\n" - val _ = say (string_of_thm thm^"\n") - val _ = thm_ref := (thm :: !thm_ref) - val _ = mss_ref := (mss :: !mss_ref) + val dummy = print_thms "cntxt:\n" cntxt + val dummy = say "cong rule:\n" + val dummy = say (string_of_thm thm^"\n") + 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 _ = print_cterms "To eliminate:\n" [tych imp] + val dummy = print_cterms "To eliminate:\n" [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 = rewrite_cterm(false,true)mss' prover lhs handle _ => reflexive lhs - val _ = print_thms "proven:\n" [lhs_eq_lhs1] + val dummy = print_thms "proven:\n" [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 @@ -697,10 +680,12 @@ end fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) = let val ((vstrl,_),args) = dest_pbeta_redex lhs_eq(length vlist) - val true = forall (fn (tm1,tm2) => S.aconv tm1 tm2) - (Utils.zip vlist args) + val dummy = assert (forall (op aconv) + (ListPair.zip (vlist, args))) + "assertion failed in CONTEXT_REWRITE_RULE" (* val fbvs1 = variants (S.free_vars imp) fbvs *) - val imp_body1 = S.subst (map (op|->) (U.zip args vstrl)) + val imp_body1 = S.subst (map (op|->) + (ListPair.zip (args, vstrl))) imp_body val tych = cterm_of sign val ants1 = map tych (Logic.strip_imp_prems imp_body1) @@ -711,8 +696,8 @@ val mss' = add_prems(mss, map ASSUME ants1) val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1 handle _ => reflexive Q1 - val Q2 = get_rhs(S.drop_Trueprop(#prop(rep_thm Q1eeqQ2))) - val Q3 = tych(S.list_mk_comb(list_mk_aabs(vstrl,Q2),vstrl)) + val Q2 = get_rhs(HOLogic.dest_Trueprop(#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 _ => @@ -757,12 +742,12 @@ end handle _ => None fun restrict_prover mss thm = - let val _ = say "restrict_prover:\n" + let val dummy = say "restrict_prover:\n" val cntxt = rev(prems_of_mss mss) - val _ = print_thms "cntxt:\n" cntxt + val dummy = print_thms "cntxt:\n" cntxt val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, sign,...} = rep_thm thm - fun genl tm = let val vlist = U.set_diff (U.curry(op aconv)) + fun genl tm = let val vlist = U.set_diff (curry(op aconv)) (add_term_frees(tm,[])) [func,R] in U.itlist Forall vlist tm end @@ -780,19 +765,19 @@ handle _ => false val nested = U.can(S.find_term is_func) val rcontext = rev cntxt - val cncl = S.drop_Trueprop o #prop o rep_thm + 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 _ = print_cterms "func:\n" [cterm_of sign func] - val _ = print_cterms "TC:\n" [cterm_of sign (S.mk_prop TC)] - val _ = tc_list := (TC :: !tc_list) + val dummy = print_cterms "func:\n" [cterm_of sign func] + val dummy = print_cterms "TC:\n" [cterm_of sign (HOLogic.mk_Trueprop TC)] + val dummy = tc_list := (TC :: !tc_list) val nestedp = nested TC - val _ = if nestedp then say "nested\n" else say "not_nested\n" - val _ = term_ref := ([func,TC]@(!term_ref)) + val dummy = if nestedp then say "nested\n" else say "not_nested\n" + 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 (S.mk_prop TC) + else let val cTC = cterm_of sign (HOLogic.mk_Trueprop TC) in case rcontext of [] => SPEC_ALL(ASSUME cTC) | _ => MP (SPEC_ALL (ASSUME cTC)) @@ -809,14 +794,14 @@ prover ctm val th2 = equal_elim th1 th in - (th2, U.filter (not o restricted) (!tc_list)) + (th2, filter (not o restricted) (!tc_list)) end; fun prove (tm,tac) = let val {t,sign,...} = rep_cterm tm - val ptm = cterm_of sign(S.mk_prop t) + val ptm = cterm_of sign(HOLogic.mk_Trueprop t) in freeze(prove_goalw_cterm [] ptm (fn _ => [tac])) end; diff -r 71b760618f30 -r 241838c01caf TFL/rules.sig --- a/TFL/rules.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/rules.sig Tue May 20 11:49:57 1997 +0200 @@ -1,65 +1,59 @@ signature Rules_sig = sig (* structure USyntax : USyntax_sig *) - type Type - type Preterm - type Term - type Thm - type Tactic type 'a binding - val dest_thm : Thm -> Preterm list * Preterm + val dest_thm : thm -> term list * term (* Inference rules *) - val REFL :Term -> Thm - val ASSUME :Term -> 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 :Term -> Thm -> Thm - val UNDISCH :Thm -> Thm - val INST_TYPE :Type binding list -> Thm -> Thm - val SPEC :Term -> Thm -> Thm - val ISPEC :Term -> Thm -> Thm - val ISPECL :Term list -> Thm -> Thm - val GEN :Term -> Thm -> Thm - val GENL :Term list -> Thm -> Thm - val BETA_RULE :Thm -> Thm - val LIST_CONJ :Thm list -> Thm + 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 binding 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 : (Preterm -> 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 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 : Term * Thm -> Thm -> Thm - val EXISTS : Term * Term -> Thm -> Thm - val EXISTL : Term list -> Thm -> Thm - val IT_EXISTS : Term binding list -> Thm -> Thm + val CHOOSE : cterm * thm -> thm -> thm + val EXISTS : cterm * cterm -> thm -> thm + val EXISTL : cterm list -> thm -> thm + val IT_EXISTS : cterm binding list -> thm -> thm - val EVEN_ORS : Thm list -> Thm list - val DISJ_CASESL : Thm -> Thm list -> Thm + val EVEN_ORS : thm list -> thm list + val DISJ_CASESL : thm -> thm list -> thm - val SUBS : Thm list -> Thm -> Thm - val simplify : Thm list -> Thm -> Thm - val simpl_conv : Thm list -> Term -> Thm + val SUBS : thm list -> thm -> thm + val simplify : thm list -> thm -> thm + val simpl_conv : thm list -> cterm -> thm (* For debugging my isabelle solver in the conditional rewriter *) (* - val term_ref : Preterm list ref - val thm_ref : Thm list ref + 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 : Preterm * Preterm - -> {thms:Thm list,congs: Thm list, th:Thm} - -> Thm * Preterm list - val RIGHT_ASSOC : Thm -> Thm + val CONTEXT_REWRITE_RULE : term * term + -> {thms:thm list,congs: thm list, th:thm} + -> thm * term list + val RIGHT_ASSOC : thm -> thm - val prove : Term * Tactic -> Thm + val prove : cterm * tactic -> thm end; diff -r 71b760618f30 -r 241838c01caf TFL/sys.sml --- a/TFL/sys.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/sys.sml Tue May 20 11:49:57 1997 +0200 @@ -7,7 +7,6 @@ (* Establish a base of common and/or helpful functions. *) use "utils.sig"; -use "utils.sml"; (* Get the specifications - these are independent of any system *) use "usyntax.sig"; @@ -23,16 +22,16 @@ use "tfl.sml"; -structure Utils = UTILS(val int_to_string = string_of_int); +use "utils.sml"; (*---------------------------------------------------------------------------- * Supply implementations *---------------------------------------------------------------------------*) -(* Ignore "Time" exception raised at end of building theory. *) use "usyntax.sml"; use "thms.sml"; -use"dcterm.sml"; use"rules.new.sml"; +use"dcterm.sml"; +use"rules.new.sml"; use "thry.sml"; diff -r 71b760618f30 -r 241838c01caf TFL/tfl.sig --- a/TFL/tfl.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/tfl.sig Tue May 20 11:49:57 1997 +0200 @@ -5,57 +5,51 @@ structure Thry : Thry_sig structure USyntax : USyntax_sig - type Preterm - type Term - type Thm - type Thry - type Tactic - - datatype pattern = GIVEN of Preterm * int - | OMITTED of Preterm * int + datatype pattern = GIVEN of term * int + | OMITTED of term * int - val mk_functional : Thry -> Preterm - -> {functional:Preterm, + val mk_functional : theory -> term + -> {functional:term, pats: pattern list} - val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry + val wfrec_definition0 : theory -> term -> term -> thm * theory - val post_definition : Thry * (Thm * pattern list) - -> {theory : Thry, - rules : Thm, - TCs : Preterm list list, - full_pats_TCs : (Preterm * Preterm list) list, + val post_definition : theory * (thm * pattern list) + -> {theory : theory, + rules : thm, + TCs : term list list, + full_pats_TCs : (term * term list) list, patterns : pattern list} - val wfrec_eqns : Thry -> Preterm - -> {WFR : Preterm, - proto_def : Preterm, - extracta :(Thm * Preterm list) list, + val wfrec_eqns : theory -> term + -> {WFR : term, + proto_def : term, + extracta :(thm * term list) list, pats : pattern list} - val lazyR_def : Thry - -> Preterm - -> {theory:Thry, - rules :Thm, - R :Preterm, - full_pats_TCs :(Preterm * Preterm list) list, + val lazyR_def : theory + -> term + -> {theory:theory, + rules :thm, + R :term, + full_pats_TCs :(term * term list) list, patterns: pattern list} - val mk_induction : Thry - -> Preterm -> Preterm - -> (Preterm * Preterm list) list - -> Thm + val mk_induction : theory + -> term -> term + -> (term * term list) list + -> thm - val postprocess: {WFtac:Tactic, terminator:Tactic, simplifier:Term -> Thm} - -> Thry - -> {rules:Thm, induction:Thm, TCs:Preterm list list} - -> {rules:Thm, induction:Thm, nested_tcs:Thm list} + val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm} + -> theory + -> {rules:thm, induction:thm, TCs:term list list} + -> {rules:thm, induction:thm, nested_tcs:thm list} structure Context : sig - val read : unit -> Thm list - val write : Thm list -> unit + val read : unit -> thm list + val write : thm list -> unit end end; diff -r 71b760618f30 -r 241838c01caf TFL/tfl.sml --- a/TFL/tfl.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/tfl.sml Tue May 20 11:49:57 1997 +0200 @@ -2,11 +2,7 @@ structure Thry : Thry_sig structure Thms : Thms_sig sharing type Rules.binding = Thry.binding = - Thry.USyntax.binding = Mask.binding - sharing type Rules.Type = Thry.Type = Thry.USyntax.Type - sharing type Rules.Preterm = Thry.Preterm = Thry.USyntax.Preterm - sharing type Rules.Term = Thry.Term = Thry.USyntax.Term - sharing type Thms.Thm = Rules.Thm = Thry.Thm) : TFL_sig = + Thry.USyntax.binding = Mask.binding) : TFL_sig = struct (* Declarations *) @@ -15,12 +11,6 @@ structure Thry = Thry; structure USyntax = Thry.USyntax; -type Preterm = Thry.USyntax.Preterm; -type Term = Thry.USyntax.Term; -type Thm = Thms.Thm; -type Thry = Thry.Thry; -type Tactic = Rules.Tactic; - (* Abbreviations *) structure R = Rules; @@ -30,22 +20,16 @@ (* Declares 'a binding datatype *) open Mask; -nonfix mem --> |-> ##; +nonfix mem --> |->; val --> = S.-->; -val ## = U.##; infixr 3 -->; infixr 7 |->; -infix 4 ##; val concl = #2 o R.dest_thm; val hyp = #1 o R.dest_thm; -val list_mk_type = U.end_itlist (U.curry(op -->)); - -fun flatten [] = [] - | flatten (h::t) = h@flatten t; - +val list_mk_type = U.end_itlist (curry(op -->)); fun gtake f = let fun grab(0,rst) = ([],rst) @@ -59,8 +43,8 @@ rev(#1(U.rev_itlist (fn x => fn (alist,i) => ((x,i)::alist, i+1)) L ([],0))); fun stringize [] = "" - | stringize [i] = U.int_to_string i - | stringize (h::t) = (U.int_to_string h^", "^stringize t); + | stringize [i] = Int.toString i + | stringize (h::t) = (Int.toString h^", "^stringize t); fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg}; @@ -78,12 +62,12 @@ in fun gvvariant vlist = let val slist = ref (map (#Name o S.dest_var) vlist) - val mem = U.mem (U.curry (op=)) - val _ = counter := 0 + val mem = U.mem (curry (op=)) + val dummy = counter := 0 fun pass str = if (mem str (!slist)) then ( counter := !counter + 1; - pass (U.concat"v" (U.int_to_string(!counter)))) + pass (U.concat"v" (Int.toString(!counter)))) else (slist := str :: !slist; str) in fn ty => S.mk_var{Name=pass "v", Ty=ty} @@ -111,7 +95,7 @@ then ((args@rst, rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]) - val col_types = U.take S.type_of (length L, #1(hd in_group)) + val col_types = U.take type_of (length L, #1(hd in_group)) in part{constrs = crst, rows = not_in_group, A = {constructor = c, @@ -127,8 +111,8 @@ * This datatype carries some information about the origin of a * clause in a function definition. *---------------------------------------------------------------------------*) -datatype pattern = GIVEN of S.Preterm * int - | OMITTED of S.Preterm * int +datatype pattern = GIVEN of term * int + | OMITTED of term * int fun psubst theta (GIVEN (tm,i)) = GIVEN(S.subst theta tm, i) | psubst theta (OMITTED (tm,i)) = OMITTED(S.subst theta tm, i); @@ -195,13 +179,13 @@ * Misc. routines used in mk_case *---------------------------------------------------------------------------*) -fun mk_pat c = - let val L = length(#1(S.strip_type(S.type_of c))) +fun mk_pat (c,l) = + let val L = length(#1(S.strip_type(type_of c))) fun build (prefix,tag,plist) = - let val (args,plist') = gtake U.I (L, plist) - in (prefix,tag,S.list_mk_comb(c,args)::plist') end - in map build - end; + let val args = take (L,plist) + and plist' = drop(L,plist) + in (prefix,tag,list_comb(c,args)::plist') end + in map build l end; fun v_to_prefix (prefix, v::pats) = (v::prefix,pats) | v_to_prefix _ = raise TFL_ERR{func="mk_case", mesg="v_to_prefix"}; @@ -228,7 +212,7 @@ if (S.is_var p) then let val fresh = fresh_constr ty_match ty fresh_var fun expnd (c,gvs) = - let val capp = S.list_mk_comb(c,gvs) + let val capp = list_comb(c,gvs) in ((prefix, capp::rst), psubst[p |-> capp] rhs) end in map expnd (map fresh constructors) end @@ -241,41 +225,44 @@ | mk{path=[], rows = _::_} = mk_case_fail"blunder" | mk{path as u::rstp, rows as ((prefix, []), rhs)::rst} = mk{path = path, - rows = ((prefix, [fresh_var(S.type_of u)]), rhs)::rst} + rows = ((prefix, [fresh_var(type_of u)]), rhs)::rst} | mk{path = u::rstp, rows as ((_, p::_), _)::_} = - let val (pat_rectangle,rights) = U.unzip rows + let val (pat_rectangle,rights) = ListPair.unzip rows val col0 = map(hd o #2) pat_rectangle in - if (U.all S.is_var col0) - then let val rights' = map(fn(v,e) => psubst[v|->u] e) (U.zip col0 rights) + if (forall S.is_var col0) + then let val rights' = map (fn(v,e) => psubst[v|->u] e) + (ListPair.zip (col0, rights)) val pat_rectangle' = map v_to_prefix pat_rectangle val (pref_patl,tm) = mk{path = rstp, - rows = U.zip pat_rectangle' rights'} + rows = ListPair.zip (pat_rectangle', + rights')} in (map v_to_pats pref_patl, tm) end else - let val pty = S.type_of p - val ty_name = (#Tyop o S.dest_type) pty + let val pty as Type (ty_name,_) = type_of p in case (ty_info ty_name) - of U.NONE => mk_case_fail("Not a known datatype: "^ty_name) - | U.SOME{case_const,constructors} => + of None => mk_case_fail("Not a known datatype: "^ty_name) + | Some{case_const,constructors} => let val case_const_name = #Name(S.dest_const case_const) - val nrows = flatten (map (expand constructors pty) rows) + 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}) - (U.zip new_formals groups) + (ListPair.zip (new_formals, groups)) val rec_calls = map mk news - val (pat_rect,dtrees) = U.unzip rec_calls - val case_functions = map S.list_mk_abs(U.zip new_formals dtrees) - val types = map S.type_of (case_functions@[u]) @ [range_ty] + 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' = S.mk_const{Name = case_const_name, Ty = list_mk_type types} - val tree = S.list_mk_comb(case_const', case_functions@[u]) - val pat_rect1 = flatten(U.map2 mk_pat constructors' pat_rect) + 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 @@ -307,24 +294,26 @@ and paired2{Rator,Rand} = (Rator,Rand) fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s} fun single [f] = f - | single fs = mk_functional_err (Int.toString (length fs) ^ - " distinct function names!") + | single fs = mk_functional_err (Int.toString (length fs) ^ + " distinct function names!") in fun mk_functional thy eqs = let val clauses = S.strip_conj eqs - val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall) - clauses) - val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L) + val (L,R) = ListPair.unzip + (map (paired1 o S.dest_eq o #2 o S.strip_forall) + clauses) + val (funcs,pats) = ListPair.unzip(map (paired2 o S.dest_comb) L) val f = single (U.mk_set (S.aconv) funcs) val fvar = if (S.is_var f) then f else S.mk_var(S.dest_const f) - val _ = map (no_repeat_vars thy) pats - val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R)) + val dummy = map (no_repeat_vars thy) pats + val rows = ListPair.zip (map (fn x => ([],[x])) pats, + map GIVEN (enumerate R)) val fvs = S.free_varsl R - val a = S.variant fvs (S.mk_var{Name="a", Ty = S.type_of(hd pats)}) + val a = S.variant fvs (S.mk_var{Name="a", Ty = type_of(hd pats)}) val FV = a::fvs val ty_info = Thry.match_info thy val ty_match = Thry.match_type thy - val range_ty = S.type_of (hd R) + val range_ty = type_of (hd R) val (patts, case_tm) = mk_case ty_info ty_match FV range_ty {path=[a], rows=rows} val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts handle _ @@ -333,7 +322,7 @@ val finals = map row_of_pat patts2 val originals = map (row_of_pat o #2) rows fun int_eq i1 (i2:int) = (i1=i2) - val _ = case (U.set_diff int_eq originals finals) + val dummy = case (U.set_diff int_eq originals finals) of [] => () | L => mk_functional_err("The following rows (counting from zero)\ \ are inaccessible: "^stringize L) @@ -365,8 +354,8 @@ val def_name = U.concat Name "_def" val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty}) val wfrec' = S.inst ty_theta wfrec - val wfrec_R_M' = S.list_mk_comb(wfrec',[R,functional]) - val def_term = S.mk_eq{lhs=Bvar, rhs=wfrec_R_M'} + val wfrec_R_M' = list_comb(wfrec',[R,functional]) + val def_term = HOLogic.mk_eq(Bvar, wfrec_R_M') in Thry.make_definition thy def_name def_term end @@ -380,7 +369,7 @@ *---------------------------------------------------------------------------*) structure Context = struct - val non_datatype_context = ref []:Rules.Thm list ref + val non_datatype_context = ref []: thm list ref fun read() = !non_datatype_context fun write L = (non_datatype_context := L) end; @@ -430,14 +419,14 @@ {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA], congs = context_congs, th = th} - val (rules, TCs) = U.unzip (map xtract corollaries') + val (rules, TCs) = ListPair.unzip (map xtract corollaries') val rules0 = map (R.simplify [Thms.CUT_DEF]) rules val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR) val rules1 = R.LIST_CONJ(map mk_cond_rule rules0) in {theory = theory, (* holds def, if it's needed *) rules = rules1, - full_pats_TCs = merge (map pat_of pats) (U.zip given_pats TCs), + full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), TCs = TCs, patterns = pats} end; @@ -452,8 +441,7 @@ val given_pats = givens pats val {Bvar = f, Body} = S.dest_abs functional val {Bvar = x, ...} = S.dest_abs Body - val {Name,Ty = fty} = S.dest_var f - val {Tyop="fun", Args = [f_dty, f_rty]} = S.dest_type fty + val {Name, Ty = Type("fun", [f_dty, f_rty])} = S.dest_var f val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY @@ -487,8 +475,8 @@ val R1 = S.rand WFR val f = S.lhs proto_def val {Name,...} = S.dest_var f - val (extractants,TCl) = U.unzip extracta - val TCs = U.Union S.aconv TCl + val (extractants,TCl) = ListPair.unzip extracta + 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' @@ -502,11 +490,11 @@ (R.SPEC (tych R') (R.GENL[tych R1, tych f] baz))) def val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt) - val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)) + val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX) body_th in {theory = theory, R=R1, rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def', - full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl), + full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), patterns = pats} end; @@ -538,22 +526,21 @@ * pairing the incoming new variable with the term it gets beta-reduced into. *---------------------------------------------------------------------------*) -fun alpha_ex_unroll xlist tm = +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 = U.zip vlist xlist - val args = map (U.C (U.assoc1 (U.uncurry S.aconv)) plist) qvars - val args' = map (fn U.SOME(_,v) => v - | U.NONE => raise TFL_ERR{func = "alpha_ex_unroll", - mesg = "no correspondence"}) args + 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 ex (v::rst) = let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v}) in ex1::build ex1 rst end - val (nex::exl) = rev (tm::build tm args') + val (nex::exl) = rev (tm::build tm args) in - (nex, U.zip args' (rev exl)) + (nex, ListPair.zip (args, rev exl)) end; @@ -574,27 +561,28 @@ | 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) = U.unzip rows + let val (pat_rectangle,rights) = ListPair.unzip rows val col0 = map hd pat_rectangle val pat_rectangle' = map tl pat_rectangle in - if (U.all S.is_var col0) (* column 0 is all variables *) + if (forall S.is_var col0) (* column 0 is all variables *) then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[u|->v])) - (U.zip rights col0) - in mk{path = rstp, rows = U.zip pat_rectangle' rights'} + (ListPair.zip (rights, col0)) + in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')} end else (* column 0 is all constructors *) - let val ty_name = (#Tyop o S.dest_type o S.type_of) p + let val Type (ty_name,_) = type_of p in case (ty_info ty_name) - of U.NONE => fail("Not a known datatype: "^ty_name) - | U.SOME{constructors,nchotomy} => + 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 = U.map2 alpha_ex_unroll new_formals disjuncts + 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)) @@ -602,8 +590,10 @@ rows = map (expnd c) rows}) (U.zip3 new_formals groups constraints) val recursive_thms = map mk news - val build_exists = U.itlist(R.CHOOSE o (tych##(R.ASSUME o tych))) - val thms' = U.map2 build_exists vexl recursive_thms + 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 @@ -618,11 +608,11 @@ val ty_info = Thry.induct_info thy in fn pats => let val FV0 = S.free_varsl pats - val a = S.variant FV0 (pmk_var "a" (S.type_of(hd pats))) - val v = S.variant (a::FV0) (pmk_var "v" (S.type_of a)) + val a = S.variant FV0 (pmk_var "a" (type_of(hd pats))) + val v = S.variant (a::FV0) (pmk_var "v" (type_of a)) val FV = a::v::FV0 - val a_eq_v = S.mk_eq{lhs = a, rhs = v} - val ex_th0 = R.EXISTS ((tych##tych) (S.mk_exists{Bvar=v,Body=a_eq_v},a)) + 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 @@ -665,7 +655,7 @@ end in case TCs of [] => (S.list_mk_forall(globals, P^pat), []) - | _ => let val (ihs, TCs_locals) = U.unzip(map dest_TC TCs) + | _ => 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 @@ -725,15 +715,13 @@ 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] = U.filter (U.can S.dest_eq) (#1 (R.dest_thm thm)) + 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 U.snd(U.itlist CHOOSER L (veq,thm)) - end; + in #2 (U.itlist CHOOSER L (veq,thm)) end; fun combize M N = S.mk_comb{Rator=M,Rand=N}; -fun eq v tm = S.mk_eq{lhs=v,rhs=tm}; (*---------------------------------------------------------------------------- @@ -746,15 +734,15 @@ fun mk_induction thy f R pat_TCs_list = let val tych = Thry.typecheck thy val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM) - val (pats,TCsl) = U.unzip pat_TCs_list + val (pats,TCsl) = ListPair.unzip pat_TCs_list val case_thm = complete_cases thy pats - val domain = (S.type_of o hd) pats - val P = S.variant (S.all_varsl (pats@flatten TCsl)) - (S.mk_var{Name="P", Ty=domain --> S.bool}) + val domain = (type_of o hd) pats + val P = S.variant (S.all_varsl (pats @ List_.concat TCsl)) + (S.mk_var{Name="P", Ty=domain --> HOLogic.boolT}) val Sinduct = R.SPEC (tych P) Sinduction val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) val Rassums_TCl' = map (build_ih f P) pat_TCs_list - val (Rassums,TCl') = U.unzip Rassums_TCl' + val (Rassums,TCl') = ListPair.unzip Rassums_TCl' val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums)) val cases = map (S.beta_conv o combize Sinduct_assumf) pats val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) @@ -762,12 +750,13 @@ val v = S.variant (S.free_varsl (map concl proved_cases)) (S.mk_var{Name="v", Ty=domain}) val vtyped = tych v - val substs = map (R.SYM o R.ASSUME o tych o eq v) pats - val proved_cases1 = U.map2 (fn th => R.SUBS[th]) substs proved_cases + 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 = S.type_of(#Bvar(S.dest_forall(concl dc))) + val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc))) val vars = map (gvvariant[P]) (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) @@ -880,11 +869,10 @@ 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 = U.zip (R.CONJUNCTS rules1) TCs + 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; (* TFL *) diff -r 71b760618f30 -r 241838c01caf TFL/thms.sig --- a/TFL/thms.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/thms.sig Tue May 20 11:49:57 1997 +0200 @@ -1,16 +1,15 @@ signature Thms_sig = sig - type Thm - val WF_INDUCTION_THM:Thm - val WFREC_COROLLARY :Thm - val CUT_DEF :Thm - val CUT_LEMMA :Thm - val SELECT_AX :Thm + val WF_INDUCTION_THM:thm + val WFREC_COROLLARY :thm + val CUT_DEF :thm + val CUT_LEMMA :thm + val SELECT_AX :thm - val COND_CONG :Thm - val LET_CONG :Thm + val COND_CONG :thm + val LET_CONG :thm - val eqT :Thm - val rev_eq_mp :Thm - val simp_thm :Thm + val eqT :thm + val rev_eq_mp :thm + val simp_thm :thm end; diff -r 71b760618f30 -r 241838c01caf TFL/thms.sml --- a/TFL/thms.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/thms.sml Tue May 20 11:49:57 1997 +0200 @@ -1,7 +1,5 @@ structure Thms : Thms_sig = struct - type Thm = Thm.thm - val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec" val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct" val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply" diff -r 71b760618f30 -r 241838c01caf TFL/thry.sig --- a/TFL/thry.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/thry.sig Tue May 20 11:49:57 1997 +0200 @@ -1,30 +1,25 @@ signature Thry_sig = sig - type Type - type Preterm - type Term - type Thm - type Thry type 'a binding structure USyntax : USyntax_sig - val match_term : Thry -> Preterm -> Preterm - -> Preterm binding list * Type binding list + val match_term : theory -> term -> term + -> term binding list * typ binding list - val match_type : Thry -> Type -> Type -> Type binding list + val match_type : theory -> typ -> typ -> typ binding list - val typecheck : Thry -> Preterm -> Term + val typecheck : theory -> term -> cterm - val make_definition: Thry -> string -> Preterm -> Thm * Thry + val make_definition: theory -> string -> term -> thm * theory (* Datatype facts of various flavours *) - val match_info: Thry -> string -> {constructors:Preterm list, - case_const:Preterm} USyntax.Utils.option + val match_info: theory -> string -> {constructors:term list, + case_const:term} option - val induct_info: Thry -> string -> {constructors:Preterm list, - nchotomy:Thm} USyntax.Utils.option + val induct_info: theory -> string -> {constructors:term list, + nchotomy:thm} option - val extract_info: Thry -> {case_congs:Thm list, case_rewrites:Thm list} + val extract_info: theory -> {case_congs:thm list, case_rewrites:thm list} end; diff -r 71b760618f30 -r 241838c01caf TFL/thry.sml --- a/TFL/thry.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/thry.sml Tue May 20 11:49:57 1997 +0200 @@ -2,11 +2,6 @@ struct structure USyntax = USyntax; -type Type = USyntax.Type -type Preterm = USyntax.Preterm -type Term = USyntax.Term -type Thm = Thm.thm -type Thry = theory; open Mask; structure S = USyntax; @@ -66,9 +61,9 @@ val {Name,Ty} = S.dest_var lhs val lhs1 = S.mk_const{Name = Name, Ty = Ty} val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} - val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) + val dtm = list_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) val (_, tm', _) = Sign.infer_types (sign_of parent) - (K None) (K None) [] true ([dtm],propT) + (K None) (K None) [] true ([dtm],propT) val new_thy = add_defs_i [(s,tm')] parent in (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) @@ -112,24 +107,24 @@ * is temporary, I hope! *---------------------------------------------------------------------------*) val match_info = fn thy => - fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record), + fn "*" => Some({case_const = #case_const (#2 prod_record), constructors = #constructors (#2 prod_record)}) - | "nat" => Utils.SOME({case_const = #case_const (#2 nat_record), + | "nat" => Some({case_const = #case_const (#2 nat_record), constructors = #constructors (#2 nat_record)}) | ty => case assoc(!datatypes,ty) - of None => Utils.NONE + of None => None | Some{case_const,constructors, ...} => - Utils.SOME{case_const=case_const, constructors=constructors} + Some{case_const=case_const, constructors=constructors} val induct_info = fn thy => - fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record), + fn "*" => Some({nchotomy = #nchotomy (#2 prod_record), constructors = #constructors (#2 prod_record)}) - | "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record), + | "nat" => Some({nchotomy = #nchotomy (#2 nat_record), constructors = #constructors (#2 nat_record)}) | ty => case assoc(!datatypes,ty) - of None => Utils.NONE + of None => None | Some{nchotomy,constructors, ...} => - Utils.SOME{nchotomy=nchotomy, constructors=constructors} + Some{nchotomy=nchotomy, constructors=constructors} val extract_info = fn thy => let val case_congs = map (#case_cong o #2) (!datatypes) @@ -140,5 +135,4 @@ #case_rewrites(#2 nat_record)@case_rewrites} end; - end; (* Thry *) diff -r 71b760618f30 -r 241838c01caf TFL/usyntax.sig --- a/TFL/usyntax.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/usyntax.sig Tue May 20 11:49:57 1997 +0200 @@ -2,133 +2,122 @@ sig structure Utils : Utils_sig - type Type - type Term - type Preterm type 'a binding - datatype lambda = VAR of {Name : string, Ty : Type} - | CONST of {Name : string, Ty : Type} - | COMB of {Rator: Preterm, Rand : Preterm} - | LAMB of {Bvar : Preterm, Body : Preterm} + 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 : Type - val bool : Type - val mk_preterm : Term -> Preterm - val drop_Trueprop : Preterm -> Preterm + val alpha : typ + val mk_preterm : cterm -> term (* Types *) - val type_vars : Type -> Type list - val type_varsl : Type list -> Type list - val mk_type : {Tyop: string, Args:Type list} -> Type - val dest_type : Type -> {Tyop : string, Args : Type list} - val mk_vartype : string -> Type - val is_vartype : Type -> bool - val --> : Type * Type -> Type - val strip_type : Type -> Type list * Type - val strip_prod_type : Type -> Type list - val match_type: Type -> Type -> Type binding list + val type_vars : typ -> typ list + val type_varsl : typ list -> typ list + val mk_vartype : string -> typ + val is_vartype : typ -> bool + val --> : typ * typ -> typ + val strip_type : typ -> typ list * typ + val strip_prod_type : typ -> typ list + val match_type: typ -> typ -> typ binding list (* Terms *) - val free_vars : Preterm -> Preterm list - val free_varsl : Preterm list -> Preterm list - val free_vars_lr : Preterm -> Preterm list - val all_vars : Preterm -> Preterm list - val all_varsl : Preterm list -> Preterm list - val variant : Preterm list -> Preterm -> Preterm - val type_of : Preterm -> Type - val type_vars_in_term : Preterm -> Type list - val dest_term : Preterm -> lambda + val free_vars : term -> term list + val free_varsl : term list -> term list + val free_vars_lr : term -> term list + val all_vars : term -> term list + val all_varsl : term list -> term list + val variant : term list -> term -> term + val type_vars_in_term : term -> typ list + val dest_term : term -> lambda (* Prelogic *) - val aconv : Preterm -> Preterm -> bool - val subst : Preterm binding list -> Preterm -> Preterm - val inst : Type binding list -> Preterm -> Preterm - val beta_conv : Preterm -> Preterm + val aconv : term -> term -> bool + val subst : term binding list -> term -> term + val inst : typ binding list -> term -> term + val beta_conv : term -> term (* Construction routines *) - val mk_prop :Preterm -> Preterm - val mk_var :{Name : string, Ty : Type} -> Preterm - val mk_const :{Name : string, Ty : Type} -> Preterm - val mk_comb :{Rator : Preterm, Rand : Preterm} -> Preterm - val mk_abs :{Bvar : Preterm, Body : Preterm} -> Preterm + val mk_var :{Name : string, Ty : typ} -> term + val mk_const :{Name : string, Ty : typ} -> term + val mk_comb :{Rator : term, Rand : term} -> term + val mk_abs :{Bvar : term, Body : term} -> term - val mk_eq :{lhs : Preterm, rhs : Preterm} -> Preterm - val mk_imp :{ant : Preterm, conseq : Preterm} -> Preterm - val mk_select :{Bvar : Preterm, Body : Preterm} -> Preterm - val mk_forall :{Bvar : Preterm, Body : Preterm} -> Preterm - val mk_exists :{Bvar : Preterm, Body : Preterm} -> Preterm - val mk_conj :{conj1 : Preterm, conj2 : Preterm} -> Preterm - val mk_disj :{disj1 : Preterm, disj2 : Preterm} -> Preterm - val mk_pabs :{varstruct : Preterm, body : Preterm} -> Preterm + 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_var : Preterm -> {Name : string, Ty : Type} - val dest_const: Preterm -> {Name : string, Ty : Type} - val dest_comb : Preterm -> {Rator : Preterm, Rand : Preterm} - val dest_abs : Preterm -> {Bvar : Preterm, Body : Preterm} - val dest_eq : Preterm -> {lhs : Preterm, rhs : Preterm} - val dest_imp : Preterm -> {ant : Preterm, conseq : Preterm} - val dest_select : Preterm -> {Bvar : Preterm, Body : Preterm} - val dest_forall : Preterm -> {Bvar : Preterm, Body : Preterm} - val dest_exists : Preterm -> {Bvar : Preterm, Body : Preterm} - val dest_neg : Preterm -> Preterm - val dest_conj : Preterm -> {conj1 : Preterm, conj2 : Preterm} - val dest_disj : Preterm -> {disj1 : Preterm, disj2 : Preterm} - val dest_pair : Preterm -> {fst : Preterm, snd : Preterm} - val dest_pabs : Preterm -> {varstruct : Preterm, body : Preterm} + val dest_var : term -> {Name : string, Ty : typ} + val dest_const: term -> {Name : string, Ty : typ} + val dest_comb : term -> {Rator : term, Rand : term} + val dest_abs : term -> {Bvar : term, Body : term} + val dest_eq : term -> {lhs : term, rhs : term} + val dest_imp : term -> {ant : term, conseq : term} + val dest_select : term -> {Bvar : term, Body : 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 : term -> {varstruct : term, body : term} - val lhs : Preterm -> Preterm - val rhs : Preterm -> Preterm - val rator : Preterm -> Preterm - val rand : Preterm -> Preterm - val bvar : Preterm -> Preterm - val body : Preterm -> Preterm + val lhs : term -> term + val rhs : term -> term + val rator : term -> term + val rand : term -> term + val bvar : term -> term + val body : term -> term (* Query routines *) - val is_var : Preterm -> bool - val is_const: Preterm -> bool - val is_comb : Preterm -> bool - val is_abs : Preterm -> bool - val is_eq : Preterm -> bool - val is_imp : Preterm -> bool - val is_forall : Preterm -> bool - val is_exists : Preterm -> bool - val is_neg : Preterm -> bool - val is_conj : Preterm -> bool - val is_disj : Preterm -> bool - val is_pair : Preterm -> bool - val is_pabs : Preterm -> bool + val is_var : term -> bool + val is_const: term -> bool + val is_comb : term -> bool + val is_abs : term -> bool + val is_eq : term -> bool + 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 Preterm from a list of Preterms *) - val list_mk_comb : (Preterm * Preterm list) -> Preterm - val list_mk_abs : (Preterm list * Preterm) -> Preterm - val list_mk_imp : (Preterm list * Preterm) -> Preterm - val list_mk_forall : (Preterm list * Preterm) -> Preterm - val list_mk_exists : (Preterm list * Preterm) -> Preterm - val list_mk_conj : Preterm list -> Preterm - val list_mk_disj : Preterm list -> Preterm + (* 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_exists : (term list * term) -> term + val list_mk_conj : term list -> term + val list_mk_disj : term list -> term - (* Destructing a Preterm to a list of Preterms *) - val strip_comb : Preterm -> (Preterm * Preterm list) - val strip_abs : Preterm -> (Preterm list * Preterm) - val strip_imp : Preterm -> (Preterm list * Preterm) - val strip_forall : Preterm -> (Preterm list * Preterm) - val strip_exists : Preterm -> (Preterm list * Preterm) - val strip_conj : Preterm -> Preterm list - val strip_disj : Preterm -> Preterm list - val strip_pair : Preterm -> Preterm list + (* 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_conj : term -> term list + val strip_disj : term -> term list + val strip_pair : term -> term list (* Miscellaneous *) - val mk_vstruct : Type -> Preterm list -> Preterm - val gen_all : Preterm -> Preterm - val find_term : (Preterm -> bool) -> Preterm -> Preterm - val find_terms : (Preterm -> bool) -> Preterm -> Preterm list - val dest_relation : Preterm -> Preterm * Preterm * Preterm - val is_WFR : Preterm -> bool - val ARB : Type -> Preterm + val mk_vstruct : typ -> term list -> term + val gen_all : term -> term + val find_term : (term -> bool) -> term -> term + val find_terms : (term -> bool) -> term -> term list + val dest_relation : term -> term * term * term + val is_WFR : term -> bool + val ARB : typ -> term (* Prettyprinting *) - val Term_to_string : Term -> string + val Term_to_string : cterm -> string end; diff -r 71b760618f30 -r 241838c01caf TFL/usyntax.sml --- a/TFL/usyntax.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/usyntax.sml Tue May 20 11:49:57 1997 +0200 @@ -10,24 +10,15 @@ fun ERR{func,mesg} = Utils.ERR{module = "USyntax", func = func, mesg = mesg}; -type Type = typ -type Term = cterm -type Preterm = term - (*--------------------------------------------------------------------------- * * Types * *---------------------------------------------------------------------------*) -fun mk_type{Tyop, Args} = Type(Tyop,Args); val mk_prim_vartype = TVar; fun mk_vartype s = mk_prim_vartype((s,0),["term"]); -fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args} - | dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"}; - - (* But internally, it's useful *) fun dest_vtype (TVar x) = x | dest_vtype _ = raise ERR{func = "dest_vtype", @@ -36,14 +27,12 @@ val is_vartype = Utils.can dest_vtype; val type_vars = map mk_prim_vartype o typ_tvars -fun type_varsl L = Utils.mk_set (Utils.curry op=) - (Utils.rev_itlist (Utils.curry op @ o type_vars) L []); +fun type_varsl L = Utils.mk_set (curry op=) + (Utils.rev_itlist (curry op @ o type_vars) L []); val alpha = mk_vartype "'a" val beta = mk_vartype "'b" -val bool = Type("bool",[]); - fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"}; @@ -52,19 +41,11 @@ val --> = -->; infixr 3 -->; -(* hol_type -> hol_type list * hol_type *) -fun strip_type ty = - let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty - val (D,r) = strip_type ty2 - in (ty1::D, r) - end - handle _ => ([],ty); +fun strip_type ty = (binder_types ty, body_type ty); -(* hol_type -> hol_type list *) -fun strip_prod_type ty = - let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty - in strip_prod_type ty1 @ strip_prod_type ty2 - end handle _ => [ty]; +fun strip_prod_type (Type("*", [ty1,ty2])) = + strip_prod_type ty1 @ strip_prod_type ty2 + | strip_prod_type ty = [ty]; @@ -74,7 +55,7 @@ * *---------------------------------------------------------------------------*) nonfix aconv; -val aconv = Utils.curry (op aconv); +val aconv = curry (op aconv); fun free_vars tm = add_term_frees(tm,[]); @@ -94,9 +75,8 @@ fun free_varsl L = Utils.mk_set aconv - (Utils.rev_itlist (Utils.curry op @ o free_vars) L []); + (Utils.rev_itlist (curry op @ o free_vars) L []); -val type_of = type_of; val type_vars_in_term = map mk_prim_vartype o term_tvars; (* Can't really be very exact in Isabelle *) @@ -110,7 +90,7 @@ in rev(add(tm,[])) end; fun all_varsl L = Utils.mk_set aconv - (Utils.rev_itlist (Utils.curry op @ o all_vars) L []); + (Utils.rev_itlist (curry op @ o all_vars) L []); (* Prelogic *) @@ -151,52 +131,42 @@ | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) | mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"}; -fun list_mk_comb (h,[]) = h - | list_mk_comb (h,L) = - rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h; - - -fun mk_eq{lhs,rhs} = - let val ty = type_of lhs - val c = mk_const{Name = "op =", Ty = ty --> ty --> bool} - in list_mk_comb(c,[lhs,rhs]) - end fun mk_imp{ant,conseq} = - let val c = mk_const{Name = "op -->", Ty = bool --> bool --> bool} - in list_mk_comb(c,[ant,conseq]) + let val c = mk_const{Name = "op -->", Ty = 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 = mk_const{Name = "Eps", Ty = (ty --> bool) --> ty} - in list_mk_comb(c,[mk_abs r]) + val c = mk_const{Name = "Eps", Ty = (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 = mk_const{Name = "All", Ty = (ty --> bool) --> bool} - in list_mk_comb(c,[mk_abs r]) + val c = mk_const{Name = "All", Ty = (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 = mk_const{Name = "Ex", Ty = (ty --> bool) --> bool} - in list_mk_comb(c,[mk_abs r]) + val c = mk_const{Name = "Ex", Ty = (ty --> HOLogic.boolT) --> HOLogic.boolT} + in list_comb(c,[mk_abs r]) end; fun mk_conj{conj1,conj2} = - let val c = mk_const{Name = "op &", Ty = bool --> bool --> bool} - in list_mk_comb(c,[conj1,conj2]) + let val c = mk_const{Name = "op &", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} + in list_comb(c,[conj1,conj2]) end; fun mk_disj{disj1,disj2} = - let val c = mk_const{Name = "op |", Ty = bool --> bool --> bool} - in list_mk_comb(c,[disj1,disj2]) + let val c = mk_const{Name = "op |", Ty = HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT} + in list_comb(c,[disj1,disj2]) end; -fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]}; +fun prod_ty ty1 ty2 = Type("*", [ty1,ty2]); local fun mk_uncurry(xt,yt,zt) = @@ -220,10 +190,10 @@ (* Destruction routines *) -datatype lambda = VAR of {Name : string, Ty : Type} - | CONST of {Name : string, Ty : Type} - | COMB of {Rator: Preterm, Rand : Preterm} - | LAMB of {Bvar : Preterm, Body : Preterm}; +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} @@ -279,25 +249,27 @@ let val ty1 = type_of fst val ty2 = type_of snd val c = mk_const{Name = "Pair", Ty = ty1 --> ty2 --> prod_ty ty1 ty2} - in list_mk_comb(c,[fst,snd]) + in list_comb(c,[fst,snd]) end; fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} | dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}; -local val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const) +local fun ucheck t = (if #Name(dest_const t) = "split" then t + else raise Match) in fun dest_pabs tm = let val {Bvar,Body} = dest_abs tm in {varstruct = Bvar, body = Body} - end handle _ - => let val {Rator,Rand} = dest_comb tm - val _ = ucheck Rator - val {varstruct = lv,body} = dest_pabs Rand - val {varstruct = rv,body} = dest_pabs body - in {varstruct = mk_pair{fst = lv, snd = rv}, body = body} - end + end + handle + _ => let val {Rator,Rand} = dest_comb tm + val _ = ucheck Rator + val {varstruct = lv,body} = dest_pabs Rand + val {varstruct = rv,body} = dest_pabs body + in {varstruct = mk_pair{fst = lv, snd = rv}, body = body} + end end; @@ -326,7 +298,7 @@ val is_pabs = can dest_pabs -(* Construction of a Term from a list of Terms *) +(* 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; @@ -341,7 +313,7 @@ (* Need to reverse? *) fun gen_all tm = list_mk_forall(free_vars tm, tm); -(* Destructing a Term to a list of Terms *) +(* 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 @@ -359,7 +331,7 @@ fun strip_imp fm = if (is_imp fm) then let val {ant,conseq} = dest_imp fm - val (was,wb) = strip_imp conseq + val (was,wb) = strip_imp conseq in ((ant::was), wb) end else ([],fm); @@ -411,25 +383,15 @@ fun mk_preterm tm = #t(rep_cterm tm); -fun mk_prop (tm as Const("Trueprop",_) $ _) = tm - | mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop", - Ty = bool --> mk_type{Tyop = "prop",Args=[]}}, - Rand = tm}; - -fun drop_Trueprop (Const("Trueprop",_) $ X) = X - | drop_Trueprop X = X; - (* Miscellaneous *) fun mk_vstruct ty V = - let fun follow_prod_type ty vs = - let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty - 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 handle _ => (hd vs, tl vs) - in fst(follow_prod_type ty V) - end; + 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. *) @@ -446,7 +408,7 @@ end; (******************************************************************* - * find_terms: (term -> bool) -> term -> term list + * find_terms: (term -> HOLogic.boolT) -> term -> term list * * Find all subterms in a term that satisfy a given predicate p. * @@ -467,7 +429,7 @@ val Term_to_string = string_of_cterm; fun dest_relation tm = - if (type_of tm = bool) + if (type_of tm = HOLogic.boolT) then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm in (R,y,x) end handle _ => raise ERR{func="dest_relation", @@ -477,6 +439,6 @@ fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false; fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty}, - Body=mk_const{Name="True",Ty=bool}}; + Body=mk_const{Name="True",Ty=HOLogic.boolT}}; end; (* Syntax *) diff -r 71b760618f30 -r 241838c01caf TFL/utils.sig --- a/TFL/utils.sig Tue May 20 11:47:33 1997 +0200 +++ b/TFL/utils.sig Tue May 20 11:49:57 1997 +0200 @@ -4,50 +4,25 @@ exception ERR of {module:string,func:string, mesg:string} val Raise : exn -> 'a - (* infix 3 ## *) - val ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd val can : ('a -> 'b) -> 'a -> bool val holds : ('a -> bool) -> 'a -> bool - val assert: ('a -> bool) -> 'a -> 'a - val W : ('a -> 'a -> 'b) -> 'a -> 'b val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c - val I : 'a -> 'a - val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c - val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c - val fst : 'a * 'b -> 'a - val snd : 'a * 'b -> 'b - - (* option type *) - datatype 'a option = SOME of 'a | NONE (* Set operations *) val mem : ('a -> 'a -> bool) -> 'a -> 'a list -> bool - val union : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list - val Union : ('a -> 'a -> bool) -> 'a list list -> 'a list - val intersect : ('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list val set_diff : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list val mk_set : ('a -> 'a -> bool) -> 'a list -> 'a list - val set_eq : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool - val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list 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 filter : ('a -> bool) -> 'a list -> 'a list val mapfilter : ('a -> 'b) -> 'a list -> 'b list val pluck : ('a -> bool) -> 'a list -> 'a * 'a list - val assoc1 : ('a*'a->bool) -> 'a -> ('a * 'b) list -> ('a * 'b) option val front_back : 'a list -> 'a list * 'a - val all : ('a -> bool) -> 'a list -> bool - val exists : ('a -> bool) -> 'a list -> bool - val zip : 'a list -> 'b list -> ('a*'b) list val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list - val unzip : ('a*'b) list -> ('a list * 'b list) val take : ('a -> 'b) -> int * 'a list -> 'b list val sort : ('a -> 'a -> bool) -> 'a list -> 'a list - - val int_to_string : int -> string val concat : string -> string -> string val quote : string -> string diff -r 71b760618f30 -r 241838c01caf TFL/utils.sml --- a/TFL/utils.sml Tue May 20 11:47:33 1997 +0200 +++ b/TFL/utils.sml Tue May 20 11:49:57 1997 +0200 @@ -1,10 +1,9 @@ (*--------------------------------------------------------------------------- - * Some common utilities. This strucuture is parameterized over - * "int_to_string" because there is a difference between the string - * operations of SML/NJ versions 93 and 109. + * Some common utilities. *---------------------------------------------------------------------------*) -functor UTILS (val int_to_string : int -> string) :Utils_sig = + +structure Utils = struct (* Standard exception for TFL. *) @@ -19,40 +18,18 @@ val MESG_string = info_string "Message" end; -fun Raise (e as ERR sss) = (output(std_out, ERR_string sss); raise e) +fun Raise (e as ERR sss) = (TextIO.output(TextIO.stdOut, ERR_string sss); + raise e) | Raise e = raise e; -(* option type *) -datatype 'a option = SOME of 'a | NONE - - (* Simple combinators *) -infix 3 ## -fun f ## g = (fn (x,y) => (f x, g y)) - -fun W f x = f x x fun C f x y = f y x -fun I x = x - -fun curry f x y = f(x,y) -fun uncurry f (x,y) = f x y - -fun fst(x,y) = x -fun snd(x,y) = y; val concat = curry (op ^) fun quote s = "\""^s^"\""; -fun map2 f L1 L2 = - let fun mp2 [] [] L = rev L - | mp2 (a1::rst1) (a2::rst2) L = mp2 rst1 rst2 (f a1 a2::L) - | mp2 _ _ _ = raise UTILS_ERR{func="map2",mesg="different length lists"} - in mp2 L1 L2 [] - end; - - fun itlist f L base_value = let fun it [] = base_value | it (a::rst) = f a (it rst) @@ -81,8 +58,6 @@ in it (L1,L2) end; -fun filter p L = itlist (fn x => fn y => if (p x) then x::y else y) L [] - fun mapfilter f alist = itlist (fn i=>fn L=> (f i::L) handle _ => L) alist []; fun pluck p = @@ -104,24 +79,6 @@ in grab end; -fun all p = - let fun every [] = true - | every (a::rst) = (p a) andalso every rst - in every - end; - -fun exists p = - let fun ex [] = false - | ex (a::rst) = (p a) orelse ex rst - in ex - end; - -fun zip [] [] = [] - | zip (a::b) (c::d) = (a,c)::(zip b d) - | zip _ _ = raise UTILS_ERR{func = "zip",mesg = "different length lists"}; - -fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]); - 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"}; @@ -131,18 +88,8 @@ fun holds P x = P x handle _ => false; -fun assert p x = - if (p x) then x else raise UTILS_ERR{func="assert", mesg="predicate not true"} - -fun assoc1 eq item = - let fun assc ((entry as (key,_))::rst) = - if eq(item,key) then SOME entry else assc rst - | assc [] = NONE - in assc - end; - (* Set ops *) -nonfix mem union; (* Gag Barf Choke *) +nonfix mem; (* Gag Barf Choke *) fun mem eq_func i = let val eqi = eq_func i fun mm [] = false @@ -150,14 +97,6 @@ in mm end; -fun union eq_func = - let val mem = mem eq_func - fun un S1 [] = S1 - | un [] S1 = S1 - | un (a::rst) S2 = if (mem a S2) then (un rst S2) else (a::un rst S2) - in un - end; - fun mk_set eq_func = let val mem = mem eq_func fun mk [] = [] @@ -165,17 +104,9 @@ in mk end; -(* Union of a family of sets *) -fun Union eq_func set_o_sets = itlist (union eq_func) set_o_sets []; - -fun intersect eq_func S1 S2 = mk_set eq_func (filter (C (mem eq_func) S2) S1); - (* All the elements in the first set that are not also in the second set. *) fun set_diff eq_func S1 S2 = filter (fn x => not (mem eq_func x S2)) S1 -fun set_eq eq_func S1 S2 = - null(set_diff eq_func S1 S2) andalso null(set_diff eq_func S2 S1); - fun sort R = let fun part (m, []) = ([],[]) @@ -192,6 +123,5 @@ end; -val int_to_string = int_to_string; end; (* Utils *)