# HG changeset patch # User boehmes # Date 1256041374 -7200 # Node ID 49abb2ae137993d7b5c569e95ec188609d0217e5 # Parent 4fb8a33f74d69d9fbd5394d2fec11e55d9e62269# Parent 575bd6548df9d86244c1d9a2252ef22b8c31cb93 merged diff -r 4fb8a33f74d6 -r 49abb2ae1379 doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Tue Oct 20 14:22:02 2009 +0200 +++ b/doc-src/TutorialI/Rules/rules.tex Tue Oct 20 14:22:54 2009 +0200 @@ -1357,7 +1357,7 @@ some $x$ such that $P(x)$ is true, provided one exists. Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$. -Here is the definition of~\cdx{inv}, which expresses inverses of +Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_onto}, which we ignore here.} which expresses inverses of functions: \begin{isabelle} inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y% diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Oct 20 14:22:54 2009 +0200 @@ -52,11 +52,11 @@ fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t; val rhs = hs val np = length ps - val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) - (foldr HOLogic.mk_imp c rhs, np) ps + val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) + (List.foldr HOLogic.mk_imp c rhs, np) ps val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT) (OldTerm.term_frees fm' @ OldTerm.term_vars fm'); - val fm2 = foldr mk_all2 fm' vs + val fm2 = List.foldr mk_all2 fm' vs in (fm2, np + length vs, length rhs) end; (*Object quantifier to meta --*) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Tue Oct 20 14:22:54 2009 +0200 @@ -58,11 +58,11 @@ val rhs = hs (* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *) val np = length ps - val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) - (foldr HOLogic.mk_imp c rhs, np) ps + val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) + (List.foldr HOLogic.mk_imp c rhs, np) ps val (vs, _) = List.partition (fn t => q orelse (type_of t) = HOLogic.natT) (OldTerm.term_frees fm' @ OldTerm.term_vars fm'); - val fm2 = foldr mk_all2 fm' vs + val fm2 = List.foldr mk_all2 fm' vs in (fm2, np + length vs, length rhs) end; (*Object quantifier to meta --*) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Oct 20 14:22:54 2009 +0200 @@ -73,11 +73,11 @@ val rhs = hs (* val (rhs,irhs) = List.partition (relevant (rev ps)) hs *) val np = length ps - val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) - (foldr HOLogic.mk_imp c rhs, np) ps + val (fm',np) = List.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n))) + (List.foldr HOLogic.mk_imp c rhs, np) ps val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT) (OldTerm.term_frees fm' @ OldTerm.term_vars fm'); - val fm2 = foldr mk_all2 fm' vs + val fm2 = List.foldr mk_all2 fm' vs in (fm2, np + length vs, length rhs) end; (*Object quantifier to meta --*) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Hilbert_Choice.thy Tue Oct 20 14:22:54 2009 +0200 @@ -91,6 +91,9 @@ subsection {*Function Inverse*} +lemma inv_def: "inv f = (%y. SOME x. f x = y)" +by(simp add: inv_onto_def) + lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A" apply (simp add: inv_onto_def) apply (fast intro: someI2) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Tue Oct 20 14:22:54 2009 +0200 @@ -9,7 +9,6 @@ val pss_tree_to_cert : RealArith.pss_tree -> string val cert_to_pss_tree : Proof.context -> string -> RealArith.pss_tree - end @@ -101,7 +100,7 @@ (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >> - foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty + List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty fun parse_cmonomial ctxt = rat_int --| str "*" -- (parse_monomial ctxt) >> swap || @@ -109,7 +108,7 @@ rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r)) fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >> - foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty + List.foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty (* positivstellensatz parser *) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 14:22:54 2009 +0200 @@ -223,7 +223,7 @@ fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1); val monomial_mul = - FuncUtil.Ctermfunc.combine (curry op +) (K false); + FuncUtil.Ctermfunc.combine Integer.add (K false); fun monomial_pow m k = if k = 0 then monomial_1 @@ -233,7 +233,7 @@ FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;; fun monomial_div m1 m2 = - let val m = FuncUtil.Ctermfunc.combine (curry op +) + let val m = FuncUtil.Ctermfunc.combine Integer.add (fn x => x = 0) m1 (FuncUtil.Ctermfunc.map (fn x => ~ x) m2) in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m else error "monomial_div: non-divisible" diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Oct 20 14:22:54 2009 +0200 @@ -83,8 +83,8 @@ else let val mon1 = dest_monomial m1 val mon2 = dest_monomial m2 - val deg1 = fold (curry op + o snd) mon1 0 - val deg2 = fold (curry op + o snd) mon2 0 + val deg1 = fold (Integer.add o snd) mon1 0 + val deg2 = fold (Integer.add o snd) mon2 0 in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2) end; diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Oct 20 14:22:54 2009 +0200 @@ -252,7 +252,7 @@ fun newName (Var(ix,_), (pairs,used)) = let val v = Name.variant used (string_of_indexname ix) in ((ix,v)::pairs, v::used) end; - val (alist, _) = foldr newName ([], used) vars; + val (alist, _) = List.foldr newName ([], used) vars; fun mk_inst (Var(v,T)) = (Var(v,T), Free ((the o AList.lookup (op =) alist) v, T)); val insts = map mk_inst vars; diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/SMT/etc/settings --- a/src/HOL/SMT/etc/settings Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/SMT/etc/settings Tue Oct 20 14:22:54 2009 +0200 @@ -1,10 +1,10 @@ ISABELLE_SMT="$COMPONENT" -REMOTE_SMT_SOLVER="$COMPONENT/lib/scripts/remote_smt.pl" +REMOTE_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/remote_smt.pl" REMOTE_SMT_URL="http://www4.in.tum.de/smt/smt" -CERT_SMT_SOLVER="$COMPONENT/lib/scripts/cert_smt.pl" +CERT_SMT_SOLVER="$ISABELLE_SMT/lib/scripts/cert_smt.pl" # # Paths to local SMT solvers: diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Statespace/state_fun.ML Tue Oct 20 14:22:54 2009 +0200 @@ -157,8 +157,6 @@ | _ => NONE )); -fun foldl1 f (x::xs) = foldl f x xs; - local val meta_ext = @{thm StateFun.meta_ext}; val ss' = (HOL_ss addsimps @@ -182,7 +180,7 @@ in (Const ("Fun.comp",gT --> fT --> T)$g$f,T) end fun mk_comps fs = - foldl1 (fn ((f,fT),(g,gT)) => mk_comp f fT g gT) fs; + foldl1 (fn ((f,fT),(g,gT)) => mk_comp g gT f fT) fs; fun append n c cT f fT d dT comps = (case AList.lookup (op aconv) comps n of diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Oct 20 14:22:54 2009 +0200 @@ -20,7 +20,7 @@ val (_, _, constrs) = the (AList.lookup (op =) descr i); fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i then NONE - else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i) + else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i) | arg_nonempty _ = SOME 0; fun max xs = Library.foldl (fn (NONE, _) => NONE diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Tue Oct 20 14:22:54 2009 +0200 @@ -54,7 +54,7 @@ val _ = map check_constr_pattern args (* just count occurrences to check linearity *) - val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs + val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs then err "Nonlinear patterns" else () in () diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Function/scnp_solve.ML --- a/src/HOL/Tools/Function/scnp_solve.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Oct 20 14:22:54 2009 +0200 @@ -46,7 +46,7 @@ fun num_prog_pts (GP (arities, _)) = length arities ; fun num_graphs (GP (_, gs)) = length gs ; fun arity (GP (arities, gl)) i = nth arities i ; -fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1 +fun ndigits (GP (arities, _)) = IntInf.log2 (Integer.sum arities) + 1 (** Propositional formulas **) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Tue Oct 20 14:22:54 2009 +0200 @@ -391,8 +391,8 @@ in fn tm1 => fn tm2 => let val vdegs1 = map dest_varpow (powervars tm1) val vdegs2 = map dest_varpow (powervars tm2) - val deg1 = fold_rev ((curry (op +)) o snd) vdegs1 num_0 - val deg2 = fold_rev ((curry (op +)) o snd) vdegs2 num_0 + val deg1 = fold (Integer.add o snd) vdegs1 num_0 + val deg2 = fold (Integer.add o snd) vdegs2 num_0 in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 else lexorder vdegs1 vdegs2 end diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 20 14:22:54 2009 +0200 @@ -897,7 +897,7 @@ fun cprod ([], ys) = [] | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); -fun cprods xss = foldr (map op :: o cprod) [[]] xss; +fun cprods xss = List.foldr (map op :: o cprod) [[]] xss; fun cprods_subset [] = [[]] | cprods_subset (xs :: xss) = diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 14:22:54 2009 +0200 @@ -188,7 +188,7 @@ (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => if x1 = x2 then - let val c = numeral2 (curry op +) c1 c2 + let val c = numeral2 Integer.add c1 c2 in if c = zero then linear_add vars r1 r2 else addC$(mulC$c$x1)$(linear_add vars r1 r2) end @@ -198,7 +198,7 @@ addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) => addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 - | (_, _) => numeral2 (curry op +) tm1 tm2; + | (_, _) => numeral2 Integer.add tm1 tm2; fun linear_neg tm = linear_cmul ~1 tm; fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/Tools/refute.ML Tue Oct 20 14:22:54 2009 +0200 @@ -1616,30 +1616,14 @@ end; (* ------------------------------------------------------------------------- *) -(* sum: returns the sum of a list 'xs' of integers *) -(* ------------------------------------------------------------------------- *) - - (* int list -> int *) - - fun sum xs = List.foldl op+ 0 xs; - -(* ------------------------------------------------------------------------- *) -(* product: returns the product of a list 'xs' of integers *) -(* ------------------------------------------------------------------------- *) - - (* int list -> int *) - - fun product xs = List.foldl op* 1 xs; - -(* ------------------------------------------------------------------------- *) (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) (* is the sum (over its constructors) of the product (over *) (* their arguments) of the size of the argument types *) (* ------------------------------------------------------------------------- *) fun size_of_dtyp thy typ_sizes descr typ_assoc constructors = - sum (map (fn (_, dtyps) => - product (map (size_of_type thy (typ_sizes, []) o + Integer.sum (map (fn (_, dtyps) => + Integer.prod (map (size_of_type thy (typ_sizes, []) o (typ_of_dtyp descr typ_assoc)) dtyps)) constructors); @@ -2326,8 +2310,8 @@ let (* number of all constructors, including those of different *) (* (mutually recursive) datatypes within the same descriptor *) - val mconstrs_count = sum (map (fn (_, (_, _, cs)) => length cs) - (#descr info)) + val mconstrs_count = + Integer.sum (map (fn (_, (_, _, cs)) => length cs) (#descr info)) in if mconstrs_count < length params then (* too many actual parameters; for now we'll use the *) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Tue Oct 20 14:22:54 2009 +0200 @@ -825,7 +825,7 @@ fun cprod ([], ys) = [] | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); -fun cprods xss = foldr (map op :: o cprod) [[]] xss; +fun cprods xss = List.foldr (map op :: o cprod) [[]] xss; diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Oct 20 14:22:54 2009 +0200 @@ -71,7 +71,7 @@ to generate parse rules for non-alphanumeric names*) fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in if tvar mem typevars then freetvar ("t"^s) n else tvar end; - fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; + fun mk_matT (a,bs,c) = a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; fun mat (con,args,mx) = (mat_name_ con, mk_matT(dtype, map third args, freetvar "t" 1), Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/HOLCF/Tools/fixrec.ML Tue Oct 20 14:22:54 2009 +0200 @@ -36,7 +36,7 @@ infixr 6 ->>; val (op ->>) = cfunT; -fun cfunsT (Ts, U) = foldr cfunT U Ts; +fun cfunsT (Ts, U) = List.foldr cfunT U Ts; fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 20 14:22:54 2009 +0200 @@ -301,14 +301,14 @@ if n = 1 then i else if n = 0 andalso ty = Lt then sys_error "multiply_ineq" else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" - else Lineq (n * k, ty, map (curry op* n) l, Multiplied (n, just)); + else Lineq (n * k, ty, map (Integer.mult n) l, Multiplied (n, just)); (* ------------------------------------------------------------------------- *) (* Add together (in)equations. *) (* ------------------------------------------------------------------------- *) fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = - let val l = map2 (curry (op +)) l1 l2 + let val l = map2 Integer.add l1 l2 in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end; (* ------------------------------------------------------------------------- *) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Pure/General/integer.ML --- a/src/Pure/General/integer.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Pure/General/integer.ML Tue Oct 20 14:22:54 2009 +0200 @@ -1,13 +1,16 @@ (* Title: Pure/General/integer.ML Author: Florian Haftmann, TU Muenchen -Unbounded integers. +Auxiliary operations on (unbounded) integers. *) signature INTEGER = sig + val add: int -> int -> int + val mult: int -> int -> int + val sum: int list -> int + val prod: int list -> int val sign: int -> order - val sum: int list -> int val div_mod: int -> int -> int * int val square: int -> int val pow: int -> int -> int (* exponent -> base -> result *) @@ -20,9 +23,13 @@ structure Integer : INTEGER = struct -fun sign x = int_ord (x, 0); +fun add x y = x + y; +fun mult x y = x * y; -fun sum xs = fold (curry op +) xs 0; +fun sum xs = fold add xs 0; +fun prod xs = fold mult xs 1; + +fun sign x = int_ord (x, 0); fun div_mod x y = IntInf.divMod (x, y); diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Pure/ML-Systems/polyml_common.ML --- a/src/Pure/ML-Systems/polyml_common.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Pure/ML-Systems/polyml_common.ML Tue Oct 20 14:22:54 2009 +0200 @@ -18,6 +18,8 @@ val forget_structure = PolyML.Compiler.forgetStructure; +val _ = PolyML.Compiler.forgetValue "foldl"; +val _ = PolyML.Compiler.forgetValue "foldr"; val _ = PolyML.Compiler.forgetValue "print"; val _ = PolyML.Compiler.forgetValue "ref"; val _ = PolyML.Compiler.forgetType "ref"; diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Tools/Metis/metis.ML --- a/src/Tools/Metis/metis.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Tools/Metis/metis.ML Tue Oct 20 14:22:54 2009 +0200 @@ -64,6 +64,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* Isabelle ML SPECIFIC FUNCTIONS *) (* ========================================================================= *) @@ -348,6 +351,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* PP -- pretty-printing -- from the SML/NJ library *) (* *) @@ -1272,6 +1278,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* ML UTILITY FUNCTIONS *) (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *) @@ -1974,6 +1983,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* SUPPORT FOR LAZY EVALUATION *) (* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *) @@ -2053,6 +2065,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* ORDERED TYPES *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -2189,6 +2204,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -2806,6 +2824,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FINITE SETS *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -3170,6 +3191,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -3803,6 +3827,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FINITE MAPS *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -4083,6 +4110,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* PRESERVING SHARING OF ML VALUES *) (* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *) @@ -4271,6 +4301,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -4521,6 +4554,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* A HEAP DATATYPE FOR ML *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -4755,6 +4791,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* PARSER COMBINATORS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -5258,6 +5297,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* PROCESSING COMMAND LINE OPTIONS *) (* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *) @@ -5527,6 +5569,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* NAMES *) (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *) @@ -5802,6 +5847,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FIRST ORDER LOGIC TERMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -6578,6 +6626,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FIRST ORDER LOGIC SUBSTITUTIONS *) (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) @@ -6936,6 +6987,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FIRST ORDER LOGIC ATOMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -7373,6 +7427,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FIRST ORDER LOGIC FORMULAS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -8064,6 +8121,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* FIRST ORDER LOGIC LITERALS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -8498,6 +8558,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES *) (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *) @@ -8787,6 +8850,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* PROOFS IN FIRST ORDER LOGIC *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -9459,6 +9525,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -10256,6 +10325,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* NORMALIZING FORMULAS *) (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *) @@ -11425,6 +11497,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* RANDOM FINITE MODELS *) (* Copyright (c) 2003-2007 Joe Hurd, distributed under the BSD License *) @@ -12086,6 +12161,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -12334,6 +12412,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -12813,6 +12894,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -12935,6 +13019,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -13073,6 +13160,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) @@ -13442,6 +13532,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *) (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) @@ -13793,6 +13886,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* ORDERED REWRITING FOR FIRST ORDER TERMS *) (* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *) @@ -14507,6 +14603,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* A STORE FOR UNIT THEOREMS *) (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) @@ -14731,6 +14830,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* CLAUSE = ID + THEOREM *) (* Copyright (c) 2002-2004 Joe Hurd, distributed under the BSD License *) @@ -15145,6 +15247,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* THE ACTIVE SET OF CLAUSES *) (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) @@ -16009,6 +16114,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* THE WAITING SET OF CLAUSES *) (* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *) @@ -16258,6 +16366,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* THE RESOLUTION PROOF PROCEDURE *) (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *) @@ -16456,6 +16567,9 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + (* ========================================================================= *) (* THE TPTP PROBLEM FILE FORMAT (TPTP v2) *) (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Tools/Metis/metis_env.ML --- a/src/Tools/Metis/metis_env.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Tools/Metis/metis_env.ML Tue Oct 20 14:22:54 2009 +0200 @@ -3,3 +3,6 @@ val explode = String.explode; val implode = String.implode; val print = TextIO.print; +val foldl = List.foldl; +val foldr = List.foldr; + diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Tools/atomize_elim.ML --- a/src/Tools/atomize_elim.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Tools/atomize_elim.ML Tue Oct 20 14:22:54 2009 +0200 @@ -42,7 +42,7 @@ (* rearrange_prems as a conversion *) fun rearrange_prems_conv pi ct = let - val pi' = 0 :: map (curry op + 1) pi + val pi' = 0 :: map (Integer.add 1) pi val fwd = Thm.trivial ct |> Drule.rearrange_prems pi' val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd))) diff -r 4fb8a33f74d6 -r 49abb2ae1379 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Oct 20 14:22:02 2009 +0200 +++ b/src/Tools/nbe.ML Tue Oct 20 14:22:54 2009 +0200 @@ -303,7 +303,7 @@ fun subst_nonlin_vars args = let val vs = (fold o Code_Thingol.fold_varnames) - (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args []; + (fn v => AList.map_default (op =) (v, 0) (Integer.add 1)) args []; val names = Name.make_context (map fst vs); fun declare v k ctxt = let val vs = Name.invents ctxt v k in (vs, fold Name.declare vs ctxt) end;