--- a/TFL/tfl.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/TFL/tfl.ML Thu Mar 03 12:43:01 2005 +0100
@@ -201,8 +201,8 @@
fun mk_pat (c,l) =
let val L = length (binder_types (type_of c))
fun build (prfx,tag,plist) =
- let val args = take (L,plist)
- and plist' = drop(L,plist)
+ let val args = Library.take (L,plist)
+ and plist' = Library.drop(L,plist)
in (prfx,tag,list_comb(c,args)::plist') end
in map build l end;
@@ -336,7 +336,7 @@
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map (fn (t,i) => (t,(i,true))) (enumerate R))
- val names = foldr add_term_names (R,[])
+ val names = Library.foldr add_term_names (R,[])
val atype = type_of(hd pats)
and aname = variant names "a"
val a = Free(aname,atype)
@@ -433,13 +433,13 @@
end;
-fun givens pats = map pat_of (filter given pats);
+fun givens pats = map pat_of (List.filter given pats);
fun post_definition meta_tflCongs (theory, (def, pats)) =
let val tych = Thry.typecheck theory
val f = #lhs(S.dest_eq(concl def))
val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
- val pats' = filter given pats
+ val pats' = List.filter given pats
val given_pats = map pat_of pats'
val rows = map row_of_pat pats'
val WFR = #ant(S.dest_imp(concl corollary))
@@ -499,7 +499,7 @@
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
- val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
+ val R = Free (variant (Library.foldr add_term_names (eqns,[])) Rname,
Rtype)
val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
@@ -540,7 +540,7 @@
prths extractants;
())
else ()
- val TCs = foldr (gen_union (op aconv)) (TCl, [])
+ val TCs = Library.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'
@@ -622,7 +622,7 @@
let val (qvars,body) = S.strip_exists tm
val vlist = #2(S.strip_comb (S.rhs body))
val plist = ListPair.zip (vlist, xlist)
- val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
+ val args = map (fn qv => valOf (gen_assoc (op aconv) (plist, qv))) qvars
handle Option => sys_error
"TFL fault [alpha_ex_unroll]: no correspondence"
fun build ex [] = []
@@ -682,7 +682,7 @@
rows = map (expnd c) rows})
(U.zip3 new_formals groups constraints)
val recursive_thms = map mk news
- val build_exists = foldr
+ val build_exists = Library.foldr
(fn((x,t), th) =>
R.CHOOSE (tych x, R.ASSUME (tych t)) th)
val thms' = ListPair.map build_exists (vexl, recursive_thms)
@@ -698,7 +698,7 @@
let val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
- let val names = foldr add_term_names (pats,[])
+ let val names = Library.foldr add_term_names (pats,[])
val T = type_of (hd pats)
val aname = Term.variant names "a"
val vname = Term.variant (aname::names) "v"
@@ -733,7 +733,7 @@
in
fun build_ih f P (pat,TCs) =
let val globals = S.free_vars_lr pat
- fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
val (R,y,_) = S.dest_relation R_y_pat
@@ -762,7 +762,7 @@
fun build_ih f (P,SV) (pat,TCs) =
let val pat_vars = S.free_vars_lr pat
val globals = pat_vars@SV
- fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
val (R,y,_) = S.dest_relation R_y_pat
@@ -795,7 +795,7 @@
let val tych = Thry.typecheck thy
val antc = tych(#ant(S.dest_imp tm))
val thm' = R.SPEC_ALL thm
- fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
R.GENL (map tych locals)
@@ -832,7 +832,7 @@
let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
end
- val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
+ val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm))
val {lhs,rhs} = S.dest_eq veq
val L = S.free_vars_lr rhs
in #2 (U.itlist CHOOSER L (veq,thm)) end;
@@ -851,7 +851,7 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val Pname = Term.variant (foldr (foldr add_term_names)
+ val Pname = Term.variant (Library.foldr (Library.foldr add_term_names)
(pats::TCsl, [])) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = R.SPEC (tych P) Sinduction
@@ -862,7 +862,7 @@
val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case fconst thy) tasks
- val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
+ val v = Free (variant (Library.foldr add_term_names (map concl proved_cases, []))
"v",
domain)
val vtyped = tych v