# HG changeset patch # User wenzelm # Date 1190124480 -7200 # Node ID 351a308ab58df6d13f96ba68e28a564b3d9d5de0 # Parent 65947eb930faf14c944a7cf82430481e746411d4 simplified type int (eliminated IntInf.int, integer); diff -r 65947eb930fa -r 351a308ab58d src/HOL/Complex/ex/linreif.ML --- a/src/HOL/Complex/ex/linreif.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Complex/ex/linreif.ML Tue Sep 18 16:08:00 2007 +0200 @@ -10,8 +10,6 @@ open Ferrack; -val nat = Ferrack.nat o Integer.int; - exception LINR; (* pseudo reification : term -> intterm *) diff -r 65947eb930fa -r 351a308ab58d src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Sep 18 16:08:00 2007 +0200 @@ -466,7 +466,7 @@ end val protected_varnames = ref (Symtab.empty:string Symtab.table) -val invented_isavar = ref (IntInf.fromInt 0) +val invented_isavar = ref 0 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s) @@ -484,8 +484,8 @@ SOME t => t | NONE => let - val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) - val t = "u_"^(IntInf.toString (!invented_isavar)) + val _ = inc invented_isavar + val t = "u_" ^ string_of_int (!invented_isavar) val _ = ImportRecorder.protect_varname s t val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) in @@ -499,8 +499,8 @@ SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') | NONE => let - val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) - val t = "u_"^(IntInf.toString (!invented_isavar)) + val _ = inc invented_isavar + val t = "u_" ^ string_of_int (!invented_isavar) val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) in () diff -r 65947eb930fa -r 351a308ab58d src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/IntDiv.thy Tue Sep 18 16:08:00 2007 +0200 @@ -530,7 +530,7 @@ fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => if n = 0 then NONE else - let val (k, l) = IntInf.divMod (m, n); + let val (k, l) = Integer.div_mod m n; fun mk_num x = HOLogic.mk_number HOLogic.intT x; in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))]) end); diff -r 65947eb930fa -r 351a308ab58d src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Sep 18 16:08:00 2007 +0200 @@ -425,8 +425,8 @@ export_code type_NF nat int in SML module_name Norm ML {* -val nat_of_int = Norm.nat o IntInf.fromInt; -val int_of_nat = IntInf.toInt o Norm.int; +val nat_of_int = Norm.nat; +val int_of_nat = Norm.int; fun dBtype_of_typ (Type ("fun", [T, U])) = Norm.Fun (dBtype_of_typ T, dBtype_of_typ U) diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 18 16:08:00 2007 +0200 @@ -164,14 +164,14 @@ *} code_type nat - (SML "IntInf.int") + (SML "int") (OCaml "Big'_int.big'_int") (Haskell "Integer") types_code nat ("int") attach (term_of) {* -val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt; +val term_of_nat = HOLogic.mk_number HOLogic.natT; *} attach (test) {* fun gen_nat i = random_range 0 i; @@ -224,7 +224,7 @@ val simplify_less = Simplifier.rewrite (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code})); fun mk_rew (t, ty) = - if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then + if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then Thm.capply @{cterm "(op \) Numeral.Pls"} (Thm.cterm_of thy t) |> simplify_less |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm]) diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Tue Sep 18 16:08:00 2007 +0200 @@ -168,12 +168,12 @@ else if n = 0 then num0_const else if n = ~1 then raise TERM ("negative type numeral", []) else - let val (q, r) = IntInf.divMod (n, 2); + let val (q, r) = Integer.div_mod n 2; in mk_bit r $ bin_of q end; in bin_of n end; fun numeral_tr (*"_NumeralType"*) [Const (str, _)] = - mk_bintype (valOf (IntInf.fromString str)) + mk_bintype (valOf (Int.fromString str)) | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts); in [("_NumeralType", numeral_tr)] end; @@ -182,7 +182,7 @@ print_translation {* let fun int_of [] = 0 - | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs); + | int_of (b :: bs) = b + 2 * int_of bs; fun bin_of (Const ("num0", _)) = [] | bin_of (Const ("num1", _)) = [1] @@ -194,7 +194,7 @@ let val rev_digs = b :: bin_of t handle TERM _ => raise Match val i = int_of rev_digs; - val num = IntInf.toString (IntInf.abs i); + val num = string_of_int (abs i); in Syntax.const "_NumeralType" $ Syntax.free num end diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/Pretty_Char_chr.thy --- a/src/HOL/Library/Pretty_Char_chr.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/Pretty_Char_chr.thy Tue Sep 18 16:08:00 2007 +0200 @@ -38,7 +38,7 @@ by (cases c) auto code_const int_of_char and char_of_int - (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") + (SML "!Char.ord" and "!Char.chr") (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)") diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/Pretty_Int.thy --- a/src/HOL/Library/Pretty_Int.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/Pretty_Int.thy Tue Sep 18 16:08:00 2007 +0200 @@ -16,7 +16,7 @@ *} code_type int - (SML "IntInf.int") + (SML "int") (OCaml "Big'_int.big'_int") (Haskell "Integer") @@ -44,51 +44,51 @@ and "error/ \"Bit\"") code_const Numeral.pred - (SML "IntInf.- ((_), 1)") + (SML "Int.- ((_), 1)") (OCaml "Big'_int.pred'_big'_int") (Haskell "!(_/ -/ 1)") code_const Numeral.succ - (SML "IntInf.+ ((_), 1)") + (SML "Int.+ ((_), 1)") (OCaml "Big'_int.succ'_big'_int") (Haskell "!(_/ +/ 1)") code_const "op + \ int \ int \ int" - (SML "IntInf.+ ((_), (_))") + (SML "Int.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") code_const "uminus \ int \ int" - (SML "IntInf.~") + (SML "Int.~") (OCaml "Big'_int.minus'_big'_int") (Haskell "negate") code_const "op - \ int \ int \ int" - (SML "IntInf.- ((_), (_))") + (SML "Int.- ((_), (_))") (OCaml "Big'_int.sub'_big'_int") (Haskell infixl 6 "-") code_const "op * \ int \ int \ int" - (SML "IntInf.* ((_), (_))") + (SML "Int.* ((_), (_))") (OCaml "Big'_int.mult'_big'_int") (Haskell infixl 7 "*") code_const "op = \ int \ int \ bool" - (SML "!((_ : IntInf.int) = _)") + (SML "!((_ : Int.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") code_const "op \ \ int \ int \ bool" - (SML "IntInf.<= ((_), (_))") + (SML "Int.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") code_const "op < \ int \ int \ bool" - (SML "IntInf.< ((_), (_))") + (SML "Int.< ((_), (_))") (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") -code_reserved SML IntInf +code_reserved SML Int code_reserved OCaml Big_int end \ No newline at end of file diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/comm_ring.ML --- a/src/HOL/Library/comm_ring.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/comm_ring.ML Tue Sep 18 16:08:00 2007 +0200 @@ -46,7 +46,7 @@ in if i = 0 then pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T) - else pol_Pinj T $ HOLogic.mk_nat (Integer.int i) + else pol_Pinj T $ HOLogic.mk_nat i $ (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)) end diff -r 65947eb930fa -r 351a308ab58d src/HOL/Library/sct.ML --- a/src/HOL/Library/sct.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/sct.ML Tue Sep 18 16:08:00 2007 +0200 @@ -157,8 +157,8 @@ measures end -val mk_number = HOLogic.mk_nat o IntInf.fromInt -val dest_number = IntInf.toInt o HOLogic.dest_nat +val mk_number = HOLogic.mk_nat +val dest_number = HOLogic.dest_nat fun nums_to i = map mk_number (0 upto (i - 1)) diff -r 65947eb930fa -r 351a308ab58d src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 18 16:08:00 2007 +0200 @@ -14,9 +14,9 @@ val approx_vector : int -> (float -> float) -> vector -> term * term val approx_matrix : int -> (float -> float) -> matrix -> term * term - val mk_spvec_entry : integer -> float -> term - val mk_spvec_entry' : integer -> term -> term - val mk_spmat_entry : integer -> term -> term + val mk_spvec_entry : int -> float -> term + val mk_spvec_entry' : int -> term -> term + val mk_spmat_entry : int -> term -> term val spvecT: typ val spmatT: typ @@ -76,7 +76,7 @@ fun app (index, s) (lower, upper) = let val (flower, fupper) = approx_value prec pprt s - val index = HOLogic.mk_number HOLogic.natT (Integer.int index) + val index = HOLogic.mk_number HOLogic.natT index val elower = HOLogic.mk_prod (index, flower) val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; @@ -89,7 +89,7 @@ fun app (index, v) (lower, upper) = let val (flower, fupper) = approx_vector prec pprt v - val index = HOLogic.mk_number HOLogic.natT (Integer.int index) + val index = HOLogic.mk_number HOLogic.natT index val elower = HOLogic.mk_prod (index, flower) val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; diff -r 65947eb930fa -r 351a308ab58d src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Tue Sep 18 16:08:00 2007 +0200 @@ -284,11 +284,10 @@ val index = xlen-i val (r12_1, r12_2) = abs_estimate (i-1) r1 r2 val b1 = Inttab.lookup r1 index - val b2 = Inttab.lookup r2 index - val i' = Integer.int index + val b2 = Inttab.lookup r2 index in - (add_row_entry r12_1 i' @{term "lbound :: real => real"} ((names index)^"l") b1, - add_row_entry r12_2 i' @{term "ubound :: real => real"} ((names index)^"u") b2) + (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1, + add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2) end val (r1, r2) = abs_estimate xlen r1 r2 diff -r 65947eb930fa -r 351a308ab58d src/HOL/Numeral.thy --- a/src/HOL/Numeral.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Numeral.thy Tue Sep 18 16:08:00 2007 +0200 @@ -635,12 +635,10 @@ code_modulename Haskell Numeral Integer -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*) - types_code "int" ("int") attach (term_of) {* -val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt; +val term_of_int = HOLogic.mk_number HOLogic.intT; *} attach (test) {* fun gen_int i = one_of [~1, 1] * random_range 0 i; @@ -656,7 +654,7 @@ let val i = HOLogic.dest_numeral (strip_number_of t) in SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)), - Pretty.str (IntInf.toString i)) + Pretty.str (string_of_int i)) end handle TERM _ => NONE; in diff -r 65947eb930fa -r 351a308ab58d src/HOL/Real/Rational.thy --- a/src/HOL/Real/Rational.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Real/Rational.thy Tue Sep 18 16:08:00 2007 +0200 @@ -697,8 +697,8 @@ val p = random_range 0 i; val q = random_range 1 (i + 1); val g = Integer.gcd p q; - val p' = Integer.div p g; - val q' = Integer.div q g; + val p' = p div g; + val q' = q div g; in (if one_of [true, false] then p' else ~ p', if p' = 0 then 0 else q') diff -r 65947eb930fa -r 351a308ab58d src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Real/RealDef.thy Tue Sep 18 16:08:00 2007 +0200 @@ -1011,8 +1011,8 @@ val p = random_range 0 i; val q = random_range 1 (i + 1); val g = Integer.gcd p q; - val p' = Integer.div p g; - val q' = Integer.div q g; + val p' = p div g; + val q' = q div g; in (if one_of [true, false] then p' else ~ p', if p' = 0 then 0 else q') diff -r 65947eb930fa -r 351a308ab58d src/HOL/Real/float_arith.ML --- a/src/HOL/Real/float_arith.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Real/float_arith.ML Tue Sep 18 16:08:00 2007 +0200 @@ -9,7 +9,7 @@ val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string exception Floating_point of string - val approx_dec_by_bin: integer -> Float.float -> Float.float * Float.float + val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float val approx_decstr_by_bin: int -> string -> Float.float * Float.float val mk_float: Float.float -> term @@ -91,30 +91,30 @@ fun find_most_significant q r = let fun int2real i = - case (Real.fromString o Integer.string_of_int) i of + case (Real.fromString o string_of_int) i of SOME r => r | NONE => raise (Floating_point "int2real") fun subtract (q, r) (q', r') = - if r <=% r' then + if r <= r' then (q - q' * exp10 (r' - r), r) else (q * exp10 (r - r') - q', r') fun bin2dec d = - if 0 <=% d then - (Integer.exp d, 0) + if 0 <= d then + (Integer.square d, 0) else (exp5 (~ d), d) - val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10)) + val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10) val L1 = L + 1 val (q1, r1) = subtract (q, r) (bin2dec L1) in - if 0 <=% q1 then + if 0 <= q1 then let val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1)) in - if 0 <=% q2 then + if 0 <= q2 then raise (Floating_point "find_most_significant") else (L1, (q1, r1)) @@ -123,7 +123,7 @@ let val (q0, r0) = subtract (q, r) (bin2dec L) in - if 0 <=% q0 then + if 0 <= q0 then (L, (q0, r0)) else raise (Floating_point "find_most_significant") @@ -133,10 +133,10 @@ fun approx_dec_by_bin n (q,r) = let fun addseq acc d' [] = acc - | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds + | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds fun seq2bin [] = (0, 0) - | seq2bin (d::ds) = (addseq 0 d ds +% 1, d) + | seq2bin (d::ds) = (addseq 0 d ds + 1, d) fun approx d_seq d0 precision (q,r) = if q = 0 then @@ -147,11 +147,11 @@ let val (d, (q', r')) = find_most_significant q r in - if precision <% d0 - d then + if precision < d0 - d then let val d' = d0 - precision val x1 = seq2bin (d_seq) - val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *) + val x2 = (fst x1 * Integer.square (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *) in (x1, x2) end @@ -160,26 +160,26 @@ end fun approx_start precision (q, r) = - if q =% 0 then + if q = 0 then ((0, 0), (0, 0)) else let val (d, (q', r')) = find_most_significant q r in - if precision <=% 0 then + if precision <= 0 then let val x1 = seq2bin [d] in if q' = 0 then (x1, x1) else - (x1, seq2bin [d +% 1]) + (x1, seq2bin [d + 1]) end else approx [d] d precision (q', r') end in - if 0 <=% q then + if 0 <= q then approx_start n (q,r) else let @@ -191,16 +191,16 @@ fun approx_decstr_by_bin n decstr = let - fun str2int s = the_default 0 (Integer.int_of_string s); - fun signint p x = if p then x else Integer.neg x + fun str2int s = the_default 0 (Int.fromString s) + fun signint p x = if p then x else ~ x val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr - val s = Integer.int (size d2) + val s = size d2 val q = signint p (str2int d1 * exp10 s + str2int d2) val r = signint ep (str2int e) - s in - approx_dec_by_bin (Integer.int n) (q,r) + approx_dec_by_bin n (q,r) end fun mk_float (a, b) = @{term "float"} $ diff -r 65947eb930fa -r 351a308ab58d src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Sep 18 16:08:00 2007 +0200 @@ -41,8 +41,8 @@ (* ------------------------------------------------------------------------- *) datatype history = - Start of integer - | Mmul of (Rat.rat * (integer list)) * history + Start of int + | Mmul of (Rat.rat * int list) * history | Add of history * history; @@ -54,8 +54,8 @@ ([],[]) => false | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2 | _ => error "morder: inconsistent monomial lengths" - val n1 = fold Integer.add m1 0 - val n2 = fold Integer.add m2 0 in + val n1 = Integer.sum m1 + val n2 = Integer.sum m2 in n1 < n2 orelse n1 = n2 andalso lexorder m1 m2 end; @@ -80,7 +80,7 @@ fun grob_sub l1 l2 = grob_add l1 (grob_neg l2); -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 Integer.add m1 m2); +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2)); fun grob_cmul cm pol = map (grob_mmul cm) pol; @@ -108,29 +108,27 @@ fun grob_pow vars l n = if n < 0 then error "grob_pow: negative power" else if n = 0 then [(rat_1,map (fn v => 0) vars)] - else grob_mul l (grob_pow vars l (n -% 1)); - -val max = fn (x: integer) => fn y => if x < y then y else x; + else grob_mul l (grob_pow vars l (n - 1)); fun degree vn p = case p of [] => error "Zero polynomial" | [(c,ns)] => nth ns vn -| (c,ns)::p' => max (nth ns vn) (degree vn p'); +| (c,ns)::p' => Int.max (nth ns vn, degree vn p'); fun head_deg vn p = let val d = degree vn p in (d,fold (fn (c,r) => fn q => grob_add q [(c, map_index (fn (i,n) => if i = vn then 0 else n) r)]) (filter (fn (c,ns) => c <>/ rat_0 andalso nth ns vn = d) p) []) end; -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) (0: integer)) ns); +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns); val grob_pdiv = let fun pdiv_aux vn (n,a) p k s = if is_zerop s then (k,s) else let val (m,b) = head_deg vn s in if m < n then (k,s) else - let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m -% n else 0) + let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0) (snd (hd s)))] in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p') - else pdiv_aux vn (n,a) p (k +% 1) (grob_sub (grob_mul a s) (grob_mul b p')) + else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p')) end end in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s @@ -140,11 +138,11 @@ fun mdiv (c1,m1) (c2,m2) = (c1//c2, - map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 -% n2) m1 m2); + map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2); (* Lowest common multiple of two monomials. *) -fun mlcm (c1,m1) (c2,m2) = (rat_1,map2 max m1 m2); +fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2)); (* Reduce monomial cm by polynomial pol, returning replacement for cm. *) @@ -221,7 +219,7 @@ | _ => false; fun poly_eq p1 p2 = - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: integer list) = m2) p1 p2; + forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2; fun memx ((p1,h1),(p2,h2)) ppairs = not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs); @@ -237,7 +235,7 @@ (* Test for hitting constant polynomial. *) fun constant_poly p = - length p = 1 andalso forall (fn x => x = (0: integer)) (snd(hd p)); + length p = 1 andalso forall (fn x => x = 0) (snd(hd p)); (* ------------------------------------------------------------------------- *) (* Grobner basis algorithm. *) @@ -299,8 +297,7 @@ (* ------------------------------------------------------------------------- *) fun grobner pols = - let val npols = map2 (fn p => fn n => (p,Start n)) pols - (map Integer.int (0 upto (length pols - 1))) + let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1)) val phists = filter (fn (p,_) => not (null p)) npols val bas = grobner_interreduce [] (map monic phists) val prs0 = product bas bas @@ -376,7 +373,7 @@ val pol' = augment pol val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols' val (l,cert) = grobner_weak vars' allpols - val d = fold_rev (fold_rev (max o hd o snd) o snd) cert 0 + val d = fold_rev (fold_rev (curry Int.max o hd o snd) o snd) cert 0 fun transform_monomial (c,m) = grob_cmul (c,tl m) (grob_pow vars pol (d - hd m)) fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q [] @@ -575,7 +572,7 @@ let fun holify_varpow (v,n) = if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *) fun holify_monomial vars (c,m) = - let val xps = map holify_varpow (filter (fn (_,n) => n <> (0: integer)) (vars ~~ m)) + let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m)) in end_itlist ring_mk_mul (mk_const c :: xps) end fun holify_polynomial vars p = @@ -624,7 +621,7 @@ grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths)) val (deg,l,cert) = grobner_strong vars pols pol val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth - val th2 = funpow (Integer.machine_int deg) (idom_rule o HOLogic.conj_intr th1) neq_01 + val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01 in (vars,l,cert,th2) end) (* val _ = writeln ("Translating certificate to HOL inferences") *) @@ -637,7 +634,7 @@ if null pols then reflexive(mk_const rat_0) else end_itlist mk_add (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p) - (nth eths (Integer.machine_int i) |> mk_meta_eq)) pols) + (nth eths i |> mk_meta_eq)) pols) val th1 = thm_fn herts_pos val th2 = thm_fn herts_neg val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth @@ -681,7 +678,7 @@ val pol = grobify_term vars tm val cert = grobner_ideal vars pols pol in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars) - (map Integer.int (0 upto (length pols - 1))) + (0 upto (length pols - 1)) end in (ring,ideal) end; diff -r 65947eb930fa -r 351a308ab58d src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Sep 18 16:08:00 2007 +0200 @@ -14,7 +14,6 @@ open Conv; open Normalizer; -structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord); exception COOPER of string * exn; val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms); @@ -178,10 +177,10 @@ | linear_cmul n tm = case tm of Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b) - | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x + | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (fn m => n * m) c)$x | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b) | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a) - | _ => numeral1 (Integer.mult n) tm; + | _ => numeral1 (fn m => n * m) tm; fun earlier [] x y = false | earlier (h::t) x y = if h aconv y then false else if h aconv x then true else earlier t x y; @@ -191,7 +190,7 @@ (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => if x1 = x2 then - let val c = numeral2 Integer.add c1 c2 + let val c = numeral2 (curry op +) c1 c2 in if c = zero then linear_add vars r1 r2 else addC$(mulC$c$x1)$(linear_add vars r1 r2) end @@ -201,7 +200,7 @@ addC$(mulC$c1$x1)$(linear_add vars r1 tm2) | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) => addC$(mulC$c2$x2)$(linear_add vars tm1 r2) - | (_,_) => numeral2 Integer.add tm1 tm2; + | (_,_) => numeral2 (curry op +) tm1 tm2; fun linear_neg tm = linear_cmul ~1 tm; fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); @@ -294,7 +293,7 @@ let val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE val x = term_of cx - val ins = insert (op = : integer*integer -> bool) + val ins = insert (op = : int * int -> bool) fun h (acc,dacc) t = case (term_of t) of Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => @@ -312,7 +311,7 @@ | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t) | _ => (acc, dacc) val (cs,ds) = h ([],[]) p - val l = fold Integer.lcm (cs union ds) 1 + val l = Integer.lcms (cs union ds) fun cv k ct = let val (tm as b$s$t) = term_of ct in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) @@ -325,10 +324,10 @@ (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) @{cterm "0::int"}))) in equal_elim (Thm.symmetric th) TrueI end; - val notz = let val tab = fold Integertab.update - (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty + val notz = let val tab = fold Inttab.update + (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty in - (fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral)) + (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) handle Option => (writeln "noz: Theorems-Table contains no entry for"; print_cterm ct ; raise Option))) end @@ -340,15 +339,15 @@ | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => if x=y andalso member (op =) ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s - then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t + then cv (l div dest_numeral c) t else Thm.reflexive t | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => if x=y andalso member (op =) [@{const_name HOL.less}, @{const_name HOL.less_eq}] s - then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t + then cv (l div dest_numeral c) t else Thm.reflexive t | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => if x=y then let - val k = Integer.div l (dest_numeral c) + val k = l div dest_numeral c val kt = HOLogic.mk_number iT k val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono) @@ -384,7 +383,6 @@ val D_tm = @{cpat "?D::int"}; -val int_eq = (op =):integer*integer -> bool; fun cooperex_conv ctxt vs q = let @@ -403,11 +401,11 @@ | Le t => (bacc, ins (plus1 t) aacc,dacc) | Gt t => (ins t bacc, aacc,dacc) | Ge t => (ins (minus1 t) bacc, aacc,dacc) - | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc) - | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc) + | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc) + | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc) | _ => (bacc, aacc, dacc) val (b0,a0,ds) = h p ([],[],[]) - val d = fold Integer.lcm ds 1 + val d = Integer.lcms ds val cd = Numeral.mk_cnumber @{ctyp "int"} d val dt = term_of cd fun divprop x = @@ -417,9 +415,9 @@ (Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd)) in equal_elim (Thm.symmetric th) TrueI end; - val dvd = let val tab = fold Integertab.update - (ds ~~ (map divprop ds)) Integertab.empty in - (fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral)) + val dvd = let val tab = fold Inttab.update + (ds ~~ (map divprop ds)) Inttab.empty in + (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) handle Option => (writeln "dvd: Theorems-Table contains no entry for"; print_cterm ct ; raise Option))) end @@ -545,7 +543,7 @@ | SOME n => Bound n) | @{term "0::int"} => C 0 | @{term "1::int"} => C 1 - | Term.Bound i => Bound (Integer.int i) + | Term.Bound i => Bound i | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t') | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2) | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2) @@ -641,8 +639,7 @@ fun cooper_oracle thy t = let - val (vs, ps) = pairself (map_index (swap o apfst Integer.int)) - (term_frees t, term_bools [] t); + val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t); in equals propT $ HOLogic.mk_Trueprop t $ HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))) diff -r 65947eb930fa -r 351a308ab58d src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Tools/numeral.ML Tue Sep 18 16:08:00 2007 +0200 @@ -7,8 +7,8 @@ signature NUMERAL = sig - val mk_cnumeral: integer -> cterm - val mk_cnumber: ctyp -> integer -> cterm + val mk_cnumeral: int -> cterm + val mk_cnumber: ctyp -> int -> cterm end; structure Numeral: NUMERAL = @@ -23,9 +23,8 @@ fun mk_cnumeral 0 = @{cterm "Numeral.Pls"} | mk_cnumeral ~1 = @{cterm "Numeral.Min"} | mk_cnumeral i = - let val (q, r) = Integer.divmod i 2 in - Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) - (mk_cbit (Integer.machine_int r)) + let val (q, r) = Integer.div_mod i 2 in + Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r) end; diff -r 65947eb930fa -r 351a308ab58d src/HOL/Tools/numeral_syntax.ML --- a/src/HOL/Tools/numeral_syntax.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Tools/numeral_syntax.ML Tue Sep 18 16:08:00 2007 +0200 @@ -23,7 +23,7 @@ fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b; fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls}) | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min}) - | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end; + | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; in mk value end; in @@ -54,7 +54,7 @@ | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; fun int_of [] = 0 - | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs; + | int_of (b :: bs) = b + 2 * int_of bs; fun dest_bin_str tm = let @@ -64,7 +64,7 @@ ~1 :: bs => ("-", leading 1 bs) | bs => ("", leading 0 bs)); val i = int_of rev_digs; - val num = IntInf.toString (IntInf.abs i); + val num = string_of_int (abs i); in if (i = 0 orelse i = 1) andalso z = 0 then raise Match else sign ^ implode (replicate z "0") ^ num diff -r 65947eb930fa -r 351a308ab58d src/HOL/ex/Binary.thy --- a/src/HOL/ex/Binary.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/ex/Binary.thy Tue Sep 18 16:08:00 2007 +0200 @@ -29,8 +29,7 @@ fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0 | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1 - | dest_binary (Const ("Binary.bit", _) $ bs $ b) = - 2 * dest_binary bs + IntInf.fromInt (dest_bit b) + | dest_binary (Const ("Binary.bit", _) $ bs $ b) = 2 * dest_binary bs + dest_bit b | dest_binary t = raise TERM ("dest_binary", [t]); fun mk_bit 0 = @{term False} @@ -42,8 +41,8 @@ | mk_binary n = if n < 0 then raise TERM ("mk_binary", []) else - let val (q, r) = IntInf.divMod (n, 2) - in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end; + let val (q, r) = Integer.div_mod n 2 + in @{term bit} $ mk_binary q $ mk_bit r end; end *} @@ -162,7 +161,7 @@ fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) => if n = 0 then NONE else - let val (k, l) = IntInf.divMod (m, n) + let val (k, l) = Integer.div_mod m n in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end); end; diff -r 65947eb930fa -r 351a308ab58d src/HOL/ex/Random.thy --- a/src/HOL/ex/Random.thy Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/ex/Random.thy Tue Sep 18 16:08:00 2007 +0200 @@ -131,30 +131,27 @@ ML {* signature RANDOM = sig - type seed = IntInf.int; + type seed = int; val seed: unit -> seed; - val value: IntInf.int -> seed -> IntInf.int * seed; + val value: int -> seed -> int * seed; end; structure Random : RANDOM = struct -open IntInf; - exception RANDOM; type seed = int; local - val a = fromInt 16807; - (*greetings to SML/NJ*) - val m = (the o fromString) "2147483647"; + val a = 16807; + val m = 2147483647; in fun next s = (a * s) mod m; end; local - val seed_ref = ref (fromInt 1); + val seed_ref = ref 1; in fun seed () = CRITICAL (fn () => let diff -r 65947eb930fa -r 351a308ab58d src/HOL/ex/coopereif.ML --- a/src/HOL/ex/coopereif.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/ex/coopereif.ML Tue Sep 18 16:08:00 2007 +0200 @@ -10,8 +10,6 @@ open GeneratedCooper; -val nat = GeneratedCooper.nat o Integer.int; - fun i_of_term vs t = case t of Free(xn,xT) => (case AList.lookup (op aconv) vs t of NONE => error "Variable not found in the list!" diff -r 65947eb930fa -r 351a308ab58d src/HOL/ex/reflection.ML --- a/src/HOL/ex/reflection.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/ex/reflection.ML Tue Sep 18 16:08:00 2007 +0200 @@ -200,7 +200,7 @@ val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) => (cert n, snd (valOf (AList.lookup (op =) tml xn0)) - |> (index_of #> IntInf.fromInt #> HOLogic.mk_nat #> cert))) + |> (index_of #> HOLogic.mk_nat #> cert))) subst val subst_vs = let diff -r 65947eb930fa -r 351a308ab58d src/HOL/ex/svc_funcs.ML --- a/src/HOL/ex/svc_funcs.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/ex/svc_funcs.ML Tue Sep 18 16:08:00 2007 +0200 @@ -27,12 +27,8 @@ | UnInterp of string * expr list | FalseExpr | TrueExpr - | Int of IntInf.int - | Rat of IntInf.int * IntInf.int; - - fun signedInt i = - if i < 0 then "-" ^ IntInf.toString (~i) - else IntInf.toString i; + | Int of int + | Rat of int * int; fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT; @@ -49,8 +45,8 @@ "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " | ue (FalseExpr) = "FALSE " | ue (TrueExpr) = "TRUE " - | ue (Int i) = (signedInt i) ^ " " - | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " " + | ue (Int i) = signed_string_of_int i ^ " " + | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " " in ue t end; diff -r 65947eb930fa -r 351a308ab58d src/HOL/hologic.ML --- a/src/HOL/hologic.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/hologic.ML Tue Sep 18 16:08:00 2007 +0200 @@ -82,8 +82,8 @@ val mk_Suc: term -> term val dest_Suc: term -> term val Suc_zero: term - val mk_nat: integer -> term - val dest_nat: term -> integer + val mk_nat: int -> term + val dest_nat: term -> int val class_size: string val size_const: typ -> term val bitT: typ @@ -95,12 +95,12 @@ val pls_const: term val min_const: term val bit_const: term - val mk_numeral: integer -> term - val dest_numeral: term -> integer + val mk_numeral: int -> term + val dest_numeral: term -> int val number_of_const: typ -> term val add_numerals: term -> (term * typ) list -> (term * typ) list - val mk_number: typ -> integer -> term - val dest_number: term -> typ * integer + val mk_number: typ -> int -> term + val dest_number: term -> typ * int val realT: typ val nibbleT: typ val mk_nibble: int -> term @@ -423,13 +423,13 @@ val Suc_zero = mk_Suc zero; -fun mk_nat (n: integer) = +fun mk_nat n = let fun mk 0 = zero | mk n = mk_Suc (mk (n - 1)); in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end; -fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer) +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0 | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1 | dest_nat t = raise TERM ("dest_nat", [t]); @@ -465,13 +465,12 @@ fun mk_numeral 0 = pls_const | mk_numeral ~1 = min_const | mk_numeral i = - let val (q, r) = Integer.divmod i 2 - in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end; + let val (q, r) = Integer.div_mod i 2; + in bit_const $ mk_numeral q $ mk_bit r end; fun dest_numeral (Const ("Numeral.Pls", _)) = 0 | dest_numeral (Const ("Numeral.Min", _)) = ~1 - | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = - 2 * dest_numeral bs + Integer.int (dest_bit b) + | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b | dest_numeral t = raise TERM ("dest_numeral", [t]); fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T); diff -r 65947eb930fa -r 351a308ab58d src/HOL/int_arith1.ML --- a/src/HOL/int_arith1.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/int_arith1.ML Tue Sep 18 16:08:00 2007 +0200 @@ -147,9 +147,9 @@ (*Order integers by absolute value and then by sign. The standard integer ordering is not well-founded.*) fun num_ord (i,j) = - (case IntInf.compare (IntInf.abs i, IntInf.abs j) of - EQUAL => int_ord (IntInf.sign i, IntInf.sign j) - | ord => ord); + (case int_ord (abs i, abs j) of + EQUAL => int_ord (Int.sign i, Int.sign j) + | ord => ord); (*This resembles Term.term_ord, but it puts binary numerals before other non-atomic terms.*) @@ -265,11 +265,11 @@ (*Fractions as pairs of ints. Can't use Rat.rat because the representation needs to preserve negative values in the denominator.*) -fun mk_frac (p, q : IntInf.int) = if q = 0 then raise Div else (p, q); +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); (*Don't reduce fractions; sums must be proved by rule add_frac_eq. Fractions are reduced later by the cancel_numeral_factor simproc.*) -fun add_frac ((p1 : IntInf.int, q1 : IntInf.int), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; @@ -421,9 +421,9 @@ structure CombineNumeralsData = struct - type coeff = IntInf.int - val iszero = (fn x : IntInf.int => x = 0) - val add = IntInf.+ + type coeff = int + val iszero = (fn x => x = 0) + val add = op + val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) val dest_sum = dest_sum val mk_coeff = mk_coeff @@ -451,8 +451,8 @@ (*Version for fields, where coefficients can be fractions*) structure FieldCombineNumeralsData = struct - type coeff = IntInf.int * IntInf.int - val iszero = (fn (p : IntInf.int, q) => p = 0) + type coeff = int * int + val iszero = (fn (p, q) => p = 0) val add = add_frac val mk_sum = long_mk_sum val dest_sum = dest_sum diff -r 65947eb930fa -r 351a308ab58d src/HOL/nat_simprocs.ML --- a/src/HOL/nat_simprocs.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/nat_simprocs.ML Tue Sep 18 16:08:00 2007 +0200 @@ -20,7 +20,7 @@ (*Utilities*) fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n; -fun dest_number t = IntInf.max (0, snd (HOLogic.dest_number t)); +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t)); fun find_first_numeral past (t::terms) = ((dest_number t, t, rev past @ terms) @@ -119,7 +119,7 @@ in if relaxed orelse exists prod_has_numeral ts then if k=0 then ts - else mk_number (IntInf.fromInt k) :: ts + else mk_number k :: ts else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t]) end; @@ -234,9 +234,9 @@ structure CombineNumeralsData = struct - type coeff = IntInf.int - val iszero = (fn x : IntInf.int => x = 0) - val add = IntInf.+ + type coeff = int + val iszero = (fn x => x = 0) + val add = op + val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *) val dest_sum = dest_Sucs_sum false val mk_coeff = mk_coeff diff -r 65947eb930fa -r 351a308ab58d src/Provers/Arith/cancel_factor.ML --- a/src/Provers/Arith/cancel_factor.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Provers/Arith/cancel_factor.ML Tue Sep 18 16:08:00 2007 +0200 @@ -60,12 +60,11 @@ val d = 0 |> fold (Integer.gcd o snd) tks |> fold (Integer.gcd o snd) uks; - val d' = Integer.machine_int d; in if d = 0 orelse d = 1 then NONE else SOME (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss) - (t, Data.mk_bal (div_sum d' tks, div_sum d' uks))) + (t, Data.mk_bal (div_sum d tks, div_sum d uks))) end)); diff -r 65947eb930fa -r 351a308ab58d src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Tue Sep 18 16:08:00 2007 +0200 @@ -22,8 +22,8 @@ (*abstract syntax*) val mk_bal: term * term -> term val dest_bal: term -> term * term - val mk_coeff: IntInf.int * term -> term - val dest_coeff: term -> IntInf.int * term + val mk_coeff: int * term -> term + val dest_coeff: term -> int * term (*rules*) val cancel: thm val neg_exchanges: bool (*true if a negative coeff swaps the two operands, diff -r 65947eb930fa -r 351a308ab58d src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Tue Sep 18 16:08:00 2007 +0200 @@ -29,9 +29,9 @@ val dest_sum: term -> term list val mk_bal: term * term -> term val dest_bal: term -> term * term - val mk_coeff: IntInf.int * term -> term - val dest_coeff: term -> IntInf.int * term - val find_first_coeff: term -> term list -> IntInf.int * term list + val mk_coeff: int * term -> term + val dest_coeff: term -> int * term + val find_first_coeff: term -> term list -> int * term list (*rules*) val bal_add1: thm val bal_add2: thm diff -r 65947eb930fa -r 351a308ab58d src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 18 16:08:00 2007 +0200 @@ -58,7 +58,7 @@ (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*) val pre_tac: Proof.context -> int -> tactic - val number_of: IntInf.int * typ -> term + val number_of: int * typ -> term (*the limit on the number of ~= allowed; because each ~= is split into two cases, this can lead to an explosion*) @@ -154,11 +154,11 @@ | NotLessD of injust | NotLeD of injust | NotLeDD of injust - | Multiplied of IntInf.int * injust - | Multiplied2 of IntInf.int * injust + | Multiplied of int * injust + | Multiplied2 of int * injust | Added of injust * injust; -datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust; +datatype lineq = Lineq of int * lineq_type * int list * injust; (* ------------------------------------------------------------------------- *) (* Finding a (counter) example from the trace of a failed elimination *) @@ -178,7 +178,7 @@ | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)]; (* PRE: ex[v] must be 0! *) -fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) = +fun eval ex v (a, le, cs) = let val rs = map Rat.rat_of_int cs; val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero; @@ -332,9 +332,9 @@ fun is_answer (ans as Lineq(k,ty,l,_)) = case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; -fun calc_blowup (l:IntInf.int list) = +fun calc_blowup l = let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l) - in (length p) * (length n) end; + in length p * length n end; (* ------------------------------------------------------------------------- *) (* Main elimination code: *) @@ -360,9 +360,9 @@ fun print_ineqs ineqs = if !trace then tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => - IntInf.toString c ^ + string_of_int c ^ (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ - commas(map IntInf.toString l)) ineqs)) + commas(map string_of_int l)) ineqs)) else (); type history = (int * lineq list) list; @@ -381,7 +381,7 @@ let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in if not (null eqs) then let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) - val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y))) + val sclist = sort (fn (x,y) => int_ord (abs x, abs y)) (List.filter (fn i => i<>0) clist) val c = hd sclist val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = @@ -487,8 +487,8 @@ | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) | mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) - | mk (Multiplied (n, j)) = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j))) - | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j))) + | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j))) + | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j))) in trace_msg "mkthm"; let val thm = trace_thm "Final thm:" (mk just) @@ -507,13 +507,11 @@ end; fun coeff poly atom = - AList.lookup (op aconv) poly atom |> the_default (0: integer); - -fun lcms ks = fold Integer.lcm ks 1; + AList.lookup (op aconv) poly atom |> the_default 0; fun integ(rlhs,r,rel,rrhs,s,d) = let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s - val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) + val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs)) fun mult(t,r) = let val (i,j) = Rat.quotient_of_rat r in (t,i * (m div j)) end @@ -547,9 +545,9 @@ fun print_atom((a,d),r) = let val (p,q) = Rat.quotient_of_rat r - val s = if d then IntInf.toString p else + val s = if d then string_of_int p else if p = 0 then "0" - else IntInf.toString p ^ "/" ^ IntInf.toString q + else string_of_int p ^ "/" ^ string_of_int q in a ^ " = " ^ s end; fun produce_ex sds = diff -r 65947eb930fa -r 351a308ab58d src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Pure/Syntax/lexicon.ML Tue Sep 18 16:08:00 2007 +0200 @@ -29,7 +29,7 @@ val var: indexname -> term val read_nat: string -> int option val read_int: string -> int option - val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int} + val read_xnum: string -> {radix: int, leading_zeros: int, value: int} val read_idents: string -> string list val fixedN: string val constN: string @@ -402,7 +402,7 @@ | "0" :: "b" :: cs => (1, 2, cs) | "-" :: cs => (~1, 10, cs) | cs => (1, 10, cs)); - val value = IntInf.fromInt sign * #1 (Library.read_intinf radix digs); + val value = sign * #1 (Library.read_radix_int radix digs); in {radix = radix, leading_zeros = leading_zeros digs, value = value} end; end; diff -r 65947eb930fa -r 351a308ab58d src/Pure/library.ML --- a/src/Pure/library.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Pure/library.ML Tue Sep 18 16:08:00 2007 +0200 @@ -125,7 +125,7 @@ val string_of_int: int -> string val signed_string_of_int: int -> string val string_of_indexname: string * int -> string - val read_intinf: int -> string list -> IntInf.int * string list + val read_radix_int: int -> string list -> int * string list val read_int: string list -> int * string list val oct_char: string -> string @@ -640,20 +640,20 @@ (* read integers *) -fun read_intinf radix cs = +fun read_radix_int radix cs = let val zero = ord "0"; val limit = zero + radix; fun scan (num, []) = (num, []) | scan (num, c :: cs) = if zero <= ord c andalso ord c < limit then - scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs) + scan (radix * num + (ord c - zero), cs) else (num, c :: cs); - in scan (IntInf.fromInt 0, cs) end; + in scan (0, cs) end; -fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs); +val read_int = read_radix_int 10; -fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s)))); +fun oct_char s = chr (#1 (read_radix_int 8 (explode s))); diff -r 65947eb930fa -r 351a308ab58d src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Tools/code/code_target.ML Tue Sep 18 16:08:00 2007 +0200 @@ -236,12 +236,12 @@ else if c = c_bit1 then SOME 1 else NONE | dest_bit _ = NONE; - fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0) - else if c = c_min then SOME (IntInf.fromInt ~1) + fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0 + else if c = c_min then SOME ~1 else NONE | dest_numeral (IConst (c, _) `$ t1 `$ t2) = if c = c_bit then case (dest_numeral t1, dest_bit t2) - of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b) + of (SOME n, SOME b) => SOME (2 * n + b) | _ => NONE else NONE | dest_numeral _ = NONE; @@ -1631,15 +1631,15 @@ val pretty : (string * { pretty_char: string -> string, pretty_string: string -> string, - pretty_numeral: bool -> IntInf.int -> string, + pretty_numeral: bool -> int -> string, pretty_list: Pretty.T list -> Pretty.T, infix_cons: int * string }) list = [ ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char, pretty_string = ML_Syntax.print_string, pretty_numeral = fn unbounded => fn k => - if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)" - else IntInf.toString k, + if unbounded then "(" ^ string_of_int k ^ " : int)" + else string_of_int k, pretty_list = Pretty.enum "," "[" "]", infix_cons = (7, "::")}), ("OCaml", { pretty_char = fn c => enclose "'" "'" @@ -1649,15 +1649,15 @@ else c end), pretty_string = (fn _ => error "OCaml: no pretty strings"), - pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then + pretty_numeral = fn unbounded => fn k => if k >= 0 then if unbounded then - "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")" - else IntInf.toString k + "(Big_int.big_int_of_int " ^ string_of_int k ^ ")" + else string_of_int k else if unbounded then "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-" - o IntInf.toString o op ~) k ^ ")" - else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k, + o string_of_int o op ~) k ^ ")" + else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k, pretty_list = Pretty.enum ";" "[" "]", infix_cons = (6, "::")}), ("Haskell", { pretty_char = fn c => enclose "'" "'" @@ -1667,10 +1667,8 @@ else c end), pretty_string = ML_Syntax.print_string, - pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then - IntInf.toString k - else - (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k, + pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k + else enclose "(" ")" (signed_string_of_int k), pretty_list = Pretty.enum "," "[" "]", infix_cons = (5, ":")}) ]; diff -r 65947eb930fa -r 351a308ab58d src/Tools/float.ML --- a/src/Tools/float.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Tools/float.ML Tue Sep 18 16:08:00 2007 +0200 @@ -7,7 +7,7 @@ signature FLOAT = sig - type float = integer * integer + type float = int * int val zero: float val eq: float * float -> bool val ord: float * float -> order @@ -25,25 +25,25 @@ structure Float : FLOAT = struct -type float = integer * integer; +type float = int * int; val zero: float = (0, 0); fun add (a1, b1) (a2, b2) = - if Integer.ord (b1, b2) = LESS then - (a1 +% a2 *% Integer.exp (b2 -% b1), b1) + if b1 < b2 then + (a1 + a2 * Integer.square (b2 - b1), b1) else - (a1 *% Integer.exp (b1 -% b2) +% a2, b2); + (a1 * Integer.square (b1 - b2) + a2, b2); fun sub (a1, b1) (a2, b2) = - if Integer.ord (b1, b2) = LESS then - (a1 -% a2 *% Integer.exp (b2 -% b1), b1) + if b1 < b2 then + (a1 - a2 * Integer.square (b2 - b1), b1) else - (a1 *% Integer.exp (b1 -% b2) -% a2, b2); + (a1 * Integer.square (b1 - b2) - a2, b2); -fun neg (a, b) = (Integer.neg a, b); +fun neg (a, b) = (~ a, b); -fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2); +fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2); fun sign (a, b) = Integer.sign a; @@ -54,7 +54,7 @@ fun min r s = case ord (r, s) of LESS => r | _ => s; fun max r s = case ord (r, s) of LESS => s | _ => r; -fun positive_part (a, b) = (Integer.max 0 a, b); -fun negative_part (a, b) = (Integer.min 0 a, b); +fun positive_part (a, b) = (Int.max (0, a), b); +fun negative_part (a, b) = (Int.min (0, a), b); end; diff -r 65947eb930fa -r 351a308ab58d src/Tools/integer.ML --- a/src/Tools/integer.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Tools/integer.ML Tue Sep 18 16:08:00 2007 +0200 @@ -7,73 +7,27 @@ signature INTEGER = sig - eqtype int - val zero: int - val one: int - val two: int - val int: Int.int -> int - val machine_int: int -> Int.int - val string_of_int: int -> string - val int_of_string: string -> int option - val eq: int * int -> bool - val ord: int * int -> order - val le: int -> int -> bool - val lt: int -> int -> bool - val signabs: int -> order * int val sign: int -> order - val abs: int -> int - val min: int -> int -> int - val max: int -> int -> int - val inc: int -> int - val add: int -> int -> int - val sub: int -> int -> int - val mult: int -> int -> int - val divmod: int -> int -> int * int - val div: int -> int -> int - val mod: int -> int -> int - val neg: int -> int - val exp: int -> int - val log: int -> int + val sum: int list -> int + val div_mod: int -> int -> int * int + val square: int -> int val pow: int -> int -> int (* exponent -> base -> result *) val gcd: int -> int -> int + val gcds: int list -> int val lcm: int -> int -> int + val lcms: int list -> int end; structure Integer : INTEGER = struct -open IntInf; - -val int = fromInt; +fun sign x = int_ord (x, 0); -val zero = int 0; -val one = int 1; -val two = int 2; - -val machine_int = toInt; -val string_of_int = toString; -val int_of_string = fromString; +fun sum xs = fold (curry op +) xs 0; -val eq = op = : int * int -> bool; -val ord = compare; -val le = curry (op <=); -val lt = curry (op <); - -fun sign k = ord (k, zero); -fun signabs k = (ord (k, zero), abs k); +fun div_mod x y = IntInf.divMod (x, y); -val min = curry min; -val max = curry max; - -val inc = curry (op +) one; - -val add = curry (op +); -val sub = curry (op -); -val mult = curry ( op * ); -val divmod = curry divMod; -nonfix div val div = curry div; -nonfix mod val mod = curry mod; -val neg = ~; +fun square x = x * x; fun pow k l = let @@ -81,38 +35,24 @@ | pw 1 l = l | pw k l = let - val (k', r) = divmod k 2; - val l' = pw k' (mult l l); - in if r = 0 then l' else mult l' l end; - in if k < zero + val (k', r) = div_mod k 2; + val l' = pw k' (l * l); + in if r = 0 then l' else l' * l end; + in + if k < 0 then error "pow: negative exponent" else pw k l end; -fun exp k = pow k two; -val log = int o log2; - fun gcd x y = let - fun gxd x y = if y = zero then x else gxd y (mod x y) - in if lt x y then gxd y x else gxd x y end; + fun gxd x y = if y = 0 then x else gxd y (x mod y) + in if x < y then gxd y x else gxd x y end; -fun lcm x y = div (mult x y) (gcd x y); +fun gcds xs = fold gcd xs 0; + +fun lcm x y = (x * y) div (gcd x y); +fun lcms xs = fold lcm xs 1; end; -type integer = Integer.int; - -infix 7 *%; -infix 6 +% -%; -infix 4 =% <% <=% >% >=% <>%; - -fun a +% b = Integer.add a b; -fun a -% b = Integer.sub a b; -fun a *% b = Integer.mult a b; -fun a =% b = Integer.eq (a, b); -fun a <% b = Integer.lt a b; -fun a <=% b = Integer.le a b; -fun a >% b = b <% a; -fun a >=% b = b <=% a; -fun a <>% b = not (a =% b); diff -r 65947eb930fa -r 351a308ab58d src/Tools/rat.ML --- a/src/Tools/rat.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/Tools/rat.ML Tue Sep 18 16:08:00 2007 +0200 @@ -12,15 +12,14 @@ val zero: rat val one: rat val two: rat - val rat_of_int: integer -> rat - val rat_of_quotient: integer * integer -> rat - val quotient_of_rat: rat -> integer * integer + val rat_of_int: int -> rat + val rat_of_quotient: int * int -> rat + val quotient_of_rat: rat -> int * int val string_of_rat: rat -> string val eq: rat * rat -> bool val ord: rat * rat -> order val le: rat -> rat -> bool val lt: rat -> rat -> bool - val signabs: rat -> order * rat val sign: rat -> order val abs: rat -> rat val add: rat -> rat -> rat @@ -37,16 +36,16 @@ fun common (p1, q1) (p2, q2) = let val m = Integer.lcm q1 q2; - in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end; + in ((p1 * (m div q1), p2 * (m div q2)), m) end; -datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *) +datatype rat = Rat of int * int; (*nominator, denominator (positive!)*) exception DIVZERO; fun rat_of_quotient (p, q) = let - val m = Integer.gcd (Integer.abs p) q - in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO; + val m = Integer.gcd (Int.abs p) q + in Rat (p div m, q div m) end handle Div => raise DIVZERO; fun quotient_of_rat (Rat r) = r; @@ -57,11 +56,12 @@ val two = rat_of_int 2; fun string_of_rat (Rat (p, q)) = - Integer.string_of_int p ^ "/" ^ Integer.string_of_int q; + string_of_int p ^ "/" ^ string_of_int q; fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2); -fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2) +fun ord (Rat (p1, q1), Rat (p2, q2)) = + case (Integer.sign p1, Integer.sign p2) of (LESS, EQUAL) => LESS | (LESS, GREATER) => LESS | (EQUAL, LESS) => GREATER @@ -69,38 +69,35 @@ | (EQUAL, GREATER) => LESS | (GREATER, LESS) => GREATER | (GREATER, EQUAL) => GREATER - | _ => Integer.ord (fst (common (p1, q1) (p2, q2))); + | _ => int_ord (fst (common (p1, q1) (p2, q2))); fun le a b = not (ord (a, b) = GREATER); fun lt a b = (ord (a, b) = LESS); fun sign (Rat (p, _)) = Integer.sign p; -fun abs (Rat (p, q)) = Rat (Integer.abs p, q); - -fun signabs (Rat (p, q)) = - let - val (s, p') = Integer.signabs p; - in (s, Rat (p', q)) end; +fun abs (Rat (p, q)) = Rat (Int.abs p, q); fun add (Rat (p1, q1)) (Rat (p2, q2)) = let val ((m1, m2), n) = common (p1, q1) (p2, q2); - in rat_of_quotient (Integer.add m1 m2, n) end; + in rat_of_quotient (m1 + m2, n) end; fun mult (Rat (p1, q1)) (Rat (p2, q2)) = - rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2); + rat_of_quotient (p1 * p2, q1 * q2); + +fun neg (Rat (p, q)) = Rat (~ p, q); -fun neg (Rat (p, q)) = Rat (Integer.neg p, q); - -fun inv (Rat (p, q)) = case Integer.sign p - of LESS => Rat (Integer.neg q, Integer.neg p) +fun inv (Rat (p, q)) = + case Integer.sign p + of LESS => Rat (~ q, ~ p) | EQUAL => raise DIVZERO | GREATER => Rat (q, p); -fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1); +fun rounddown (Rat (p, q)) = Rat (p div q, 1); -fun roundup (Rat (p, q)) = case Integer.divmod p q +fun roundup (Rat (p, q)) = + case Integer.div_mod p q of (m, 0) => Rat (m, 1) | (m, _) => Rat (m + 1, 1); diff -r 65947eb930fa -r 351a308ab58d src/ZF/Tools/numeral_syntax.ML --- a/src/ZF/Tools/numeral_syntax.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Tue Sep 18 16:08:00 2007 +0200 @@ -8,8 +8,8 @@ signature NUMERAL_SYNTAX = sig - val dest_bin : term -> IntInf.int - val mk_bin : IntInf.int -> term + val dest_bin : term -> int + val mk_bin : int -> term val int_tr : term list -> term val int_tr' : bool -> typ -> term list -> term val setup : theory -> theory @@ -23,7 +23,7 @@ val zero = Const("0", iT); val succ = Const("succ", iT --> iT); -fun mk_bit (0: IntInf.int) = zero +fun mk_bit 0 = zero | mk_bit 1 = succ$zero | mk_bit _ = sys_error "mk_bit"; @@ -42,7 +42,7 @@ and min_const = Const ("Bin.bin.Min", iT) and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT); -fun mk_bin (i: IntInf.int) = +fun mk_bin i = let fun bin_of_int 0 = [] | bin_of_int ~1 = [~1] | bin_of_int n = (n mod 2) :: bin_of_int (n div 2); @@ -67,8 +67,8 @@ | bin_of _ = raise Match; (*Convert a list of bits to an integer*) -fun integ_of [] = 0 : IntInf.int - | integ_of (b :: bs) = (IntInf.fromInt b) + 2 * integ_of bs; +fun integ_of [] = 0 + | integ_of (b :: bs) = b + 2 * integ_of bs; val dest_bin = integ_of o bin_of; @@ -82,7 +82,7 @@ (case rev rev_digs of ~1 :: bs => ("-", prefix_len (equal 1) bs) | bs => ("", prefix_len (equal 0) bs)); - val num = IntInf.toString (abs (integ_of rev_digs)); + val num = string_of_int (abs (integ_of rev_digs)); in "#" ^ sign ^ implode (replicate zs "0") ^ num end; diff -r 65947eb930fa -r 351a308ab58d src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/ZF/arith_data.ML Tue Sep 18 16:08:00 2007 +0200 @@ -100,13 +100,13 @@ handle TERM _ => [t]; (*Dummy version: the only arguments are 0 and 1*) -fun mk_coeff (0: IntInf.int, t) = zero +fun mk_coeff (0, t) = zero | mk_coeff (1, t) = t | mk_coeff _ = raise TERM("mk_coeff", []); (*Dummy version: the "coefficient" is always 1. In the result, the factors are sorted terms*) -fun dest_coeff t = (1 : IntInf.int, mk_prod (sort Term.term_ord (dest_prod t))); +fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t))); (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) diff -r 65947eb930fa -r 351a308ab58d src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/ZF/int_arith.ML Tue Sep 18 16:08:00 2007 +0200 @@ -293,9 +293,9 @@ structure CombineNumeralsData = struct - type coeff = IntInf.int - val iszero = (fn x : IntInf.int => x = 0) - val add = IntInf.+ + type coeff = int + val iszero = (fn x => x = 0) + val add = op + val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *) val dest_sum = dest_sum val mk_coeff = mk_coeff @@ -333,9 +333,9 @@ structure CombineNumeralsProdData = struct - type coeff = IntInf.int - val iszero = (fn x : IntInf.int => x = 0) - val add = IntInf.* + type coeff = int + val iszero = (fn x => x = 0) + val add = op * val mk_sum = (fn T:typ => mk_prod) val dest_sum = dest_prod fun mk_coeff(k,t) = if t=one then mk_numeral k