Removal of redundant code (unused or already present in Isabelle.
This eliminates HOL compatibility but makes the code smaller and more
readable
--- 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))
(*---------------------------------------------------------------------------
--- 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;
--- 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;
--- 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;
--- 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";
--- 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;
--- 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 *)
--- 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;
--- 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"
--- 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;
--- 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 *)
--- 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;
--- 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 *)
--- 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
--- 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 *)