1.1 --- a/src/HOL/Complex/ex/linreif.ML Tue Sep 18 11:06:22 2007 +0200
1.2 +++ b/src/HOL/Complex/ex/linreif.ML Tue Sep 18 16:08:00 2007 +0200
1.3 @@ -10,8 +10,6 @@
1.4
1.5 open Ferrack;
1.6
1.7 -val nat = Ferrack.nat o Integer.int;
1.8 -
1.9 exception LINR;
1.10
1.11 (* pseudo reification : term -> intterm *)
2.1 --- a/src/HOL/Import/proof_kernel.ML Tue Sep 18 11:06:22 2007 +0200
2.2 +++ b/src/HOL/Import/proof_kernel.ML Tue Sep 18 16:08:00 2007 +0200
2.3 @@ -466,7 +466,7 @@
2.4 end
2.5
2.6 val protected_varnames = ref (Symtab.empty:string Symtab.table)
2.7 -val invented_isavar = ref (IntInf.fromInt 0)
2.8 +val invented_isavar = ref 0
2.9
2.10 fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
2.11
2.12 @@ -484,8 +484,8 @@
2.13 SOME t => t
2.14 | NONE =>
2.15 let
2.16 - val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
2.17 - val t = "u_"^(IntInf.toString (!invented_isavar))
2.18 + val _ = inc invented_isavar
2.19 + val t = "u_" ^ string_of_int (!invented_isavar)
2.20 val _ = ImportRecorder.protect_varname s t
2.21 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
2.22 in
2.23 @@ -499,8 +499,8 @@
2.24 SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
2.25 | NONE =>
2.26 let
2.27 - val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1)
2.28 - val t = "u_"^(IntInf.toString (!invented_isavar))
2.29 + val _ = inc invented_isavar
2.30 + val t = "u_" ^ string_of_int (!invented_isavar)
2.31 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
2.32 in
2.33 ()
3.1 --- a/src/HOL/IntDiv.thy Tue Sep 18 11:06:22 2007 +0200
3.2 +++ b/src/HOL/IntDiv.thy Tue Sep 18 16:08:00 2007 +0200
3.3 @@ -530,7 +530,7 @@
3.4 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
3.5 if n = 0 then NONE
3.6 else
3.7 - let val (k, l) = IntInf.divMod (m, n);
3.8 + let val (k, l) = Integer.div_mod m n;
3.9 fun mk_num x = HOLogic.mk_number HOLogic.intT x;
3.10 in SOME (rule OF [prove ctxt (t == plus (mult u (mk_num k)) (mk_num l))])
3.11 end);
4.1 --- a/src/HOL/Lambda/WeakNorm.thy Tue Sep 18 11:06:22 2007 +0200
4.2 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Sep 18 16:08:00 2007 +0200
4.3 @@ -425,8 +425,8 @@
4.4 export_code type_NF nat int in SML module_name Norm
4.5
4.6 ML {*
4.7 -val nat_of_int = Norm.nat o IntInf.fromInt;
4.8 -val int_of_nat = IntInf.toInt o Norm.int;
4.9 +val nat_of_int = Norm.nat;
4.10 +val int_of_nat = Norm.int;
4.11
4.12 fun dBtype_of_typ (Type ("fun", [T, U])) =
4.13 Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
5.1 --- a/src/HOL/Library/Efficient_Nat.thy Tue Sep 18 11:06:22 2007 +0200
5.2 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 18 16:08:00 2007 +0200
5.3 @@ -164,14 +164,14 @@
5.4 *}
5.5
5.6 code_type nat
5.7 - (SML "IntInf.int")
5.8 + (SML "int")
5.9 (OCaml "Big'_int.big'_int")
5.10 (Haskell "Integer")
5.11
5.12 types_code
5.13 nat ("int")
5.14 attach (term_of) {*
5.15 -val term_of_nat = HOLogic.mk_number HOLogic.natT o IntInf.fromInt;
5.16 +val term_of_nat = HOLogic.mk_number HOLogic.natT;
5.17 *}
5.18 attach (test) {*
5.19 fun gen_nat i = random_range 0 i;
5.20 @@ -224,7 +224,7 @@
5.21 val simplify_less = Simplifier.rewrite
5.22 (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
5.23 fun mk_rew (t, ty) =
5.24 - if ty = HOLogic.natT andalso IntInf.<= (0, HOLogic.dest_numeral t) then
5.25 + if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then
5.26 Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
5.27 |> simplify_less
5.28 |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
6.1 --- a/src/HOL/Library/Numeral_Type.thy Tue Sep 18 11:06:22 2007 +0200
6.2 +++ b/src/HOL/Library/Numeral_Type.thy Tue Sep 18 16:08:00 2007 +0200
6.3 @@ -168,12 +168,12 @@
6.4 else if n = 0 then num0_const
6.5 else if n = ~1 then raise TERM ("negative type numeral", [])
6.6 else
6.7 - let val (q, r) = IntInf.divMod (n, 2);
6.8 + let val (q, r) = Integer.div_mod n 2;
6.9 in mk_bit r $ bin_of q end;
6.10 in bin_of n end;
6.11
6.12 fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
6.13 - mk_bintype (valOf (IntInf.fromString str))
6.14 + mk_bintype (valOf (Int.fromString str))
6.15 | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
6.16
6.17 in [("_NumeralType", numeral_tr)] end;
6.18 @@ -182,7 +182,7 @@
6.19 print_translation {*
6.20 let
6.21 fun int_of [] = 0
6.22 - | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
6.23 + | int_of (b :: bs) = b + 2 * int_of bs;
6.24
6.25 fun bin_of (Const ("num0", _)) = []
6.26 | bin_of (Const ("num1", _)) = [1]
6.27 @@ -194,7 +194,7 @@
6.28 let
6.29 val rev_digs = b :: bin_of t handle TERM _ => raise Match
6.30 val i = int_of rev_digs;
6.31 - val num = IntInf.toString (IntInf.abs i);
6.32 + val num = string_of_int (abs i);
6.33 in
6.34 Syntax.const "_NumeralType" $ Syntax.free num
6.35 end
7.1 --- a/src/HOL/Library/Pretty_Char_chr.thy Tue Sep 18 11:06:22 2007 +0200
7.2 +++ b/src/HOL/Library/Pretty_Char_chr.thy Tue Sep 18 16:08:00 2007 +0200
7.3 @@ -38,7 +38,7 @@
7.4 by (cases c) auto
7.5
7.6 code_const int_of_char and char_of_int
7.7 - (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
7.8 + (SML "!Char.ord" and "!Char.chr")
7.9 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
7.10 (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
7.11
8.1 --- a/src/HOL/Library/Pretty_Int.thy Tue Sep 18 11:06:22 2007 +0200
8.2 +++ b/src/HOL/Library/Pretty_Int.thy Tue Sep 18 16:08:00 2007 +0200
8.3 @@ -16,7 +16,7 @@
8.4 *}
8.5
8.6 code_type int
8.7 - (SML "IntInf.int")
8.8 + (SML "int")
8.9 (OCaml "Big'_int.big'_int")
8.10 (Haskell "Integer")
8.11
8.12 @@ -44,51 +44,51 @@
8.13 and "error/ \"Bit\"")
8.14
8.15 code_const Numeral.pred
8.16 - (SML "IntInf.- ((_), 1)")
8.17 + (SML "Int.- ((_), 1)")
8.18 (OCaml "Big'_int.pred'_big'_int")
8.19 (Haskell "!(_/ -/ 1)")
8.20
8.21 code_const Numeral.succ
8.22 - (SML "IntInf.+ ((_), 1)")
8.23 + (SML "Int.+ ((_), 1)")
8.24 (OCaml "Big'_int.succ'_big'_int")
8.25 (Haskell "!(_/ +/ 1)")
8.26
8.27 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
8.28 - (SML "IntInf.+ ((_), (_))")
8.29 + (SML "Int.+ ((_), (_))")
8.30 (OCaml "Big'_int.add'_big'_int")
8.31 (Haskell infixl 6 "+")
8.32
8.33 code_const "uminus \<Colon> int \<Rightarrow> int"
8.34 - (SML "IntInf.~")
8.35 + (SML "Int.~")
8.36 (OCaml "Big'_int.minus'_big'_int")
8.37 (Haskell "negate")
8.38
8.39 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
8.40 - (SML "IntInf.- ((_), (_))")
8.41 + (SML "Int.- ((_), (_))")
8.42 (OCaml "Big'_int.sub'_big'_int")
8.43 (Haskell infixl 6 "-")
8.44
8.45 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
8.46 - (SML "IntInf.* ((_), (_))")
8.47 + (SML "Int.* ((_), (_))")
8.48 (OCaml "Big'_int.mult'_big'_int")
8.49 (Haskell infixl 7 "*")
8.50
8.51 code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
8.52 - (SML "!((_ : IntInf.int) = _)")
8.53 + (SML "!((_ : Int.int) = _)")
8.54 (OCaml "Big'_int.eq'_big'_int")
8.55 (Haskell infixl 4 "==")
8.56
8.57 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
8.58 - (SML "IntInf.<= ((_), (_))")
8.59 + (SML "Int.<= ((_), (_))")
8.60 (OCaml "Big'_int.le'_big'_int")
8.61 (Haskell infix 4 "<=")
8.62
8.63 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
8.64 - (SML "IntInf.< ((_), (_))")
8.65 + (SML "Int.< ((_), (_))")
8.66 (OCaml "Big'_int.lt'_big'_int")
8.67 (Haskell infix 4 "<")
8.68
8.69 -code_reserved SML IntInf
8.70 +code_reserved SML Int
8.71 code_reserved OCaml Big_int
8.72
8.73 end
8.74 \ No newline at end of file
9.1 --- a/src/HOL/Library/comm_ring.ML Tue Sep 18 11:06:22 2007 +0200
9.2 +++ b/src/HOL/Library/comm_ring.ML Tue Sep 18 16:08:00 2007 +0200
9.3 @@ -46,7 +46,7 @@
9.4 in if i = 0
9.5 then pol_PX T $ (pol_Pc T $ cring_one T)
9.6 $ one $ (pol_Pc T $ cring_zero T)
9.7 - else pol_Pinj T $ HOLogic.mk_nat (Integer.int i)
9.8 + else pol_Pinj T $ HOLogic.mk_nat i
9.9 $ (pol_PX T $ (pol_Pc T $ cring_one T)
9.10 $ one $ (pol_Pc T $ cring_zero T))
9.11 end
10.1 --- a/src/HOL/Library/sct.ML Tue Sep 18 11:06:22 2007 +0200
10.2 +++ b/src/HOL/Library/sct.ML Tue Sep 18 16:08:00 2007 +0200
10.3 @@ -157,8 +157,8 @@
10.4 measures
10.5 end
10.6
10.7 -val mk_number = HOLogic.mk_nat o IntInf.fromInt
10.8 -val dest_number = IntInf.toInt o HOLogic.dest_nat
10.9 +val mk_number = HOLogic.mk_nat
10.10 +val dest_number = HOLogic.dest_nat
10.11
10.12 fun nums_to i = map mk_number (0 upto (i - 1))
10.13
11.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 18 11:06:22 2007 +0200
11.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Sep 18 16:08:00 2007 +0200
11.3 @@ -14,9 +14,9 @@
11.4 val approx_vector : int -> (float -> float) -> vector -> term * term
11.5 val approx_matrix : int -> (float -> float) -> matrix -> term * term
11.6
11.7 - val mk_spvec_entry : integer -> float -> term
11.8 - val mk_spvec_entry' : integer -> term -> term
11.9 - val mk_spmat_entry : integer -> term -> term
11.10 + val mk_spvec_entry : int -> float -> term
11.11 + val mk_spvec_entry' : int -> term -> term
11.12 + val mk_spmat_entry : int -> term -> term
11.13 val spvecT: typ
11.14 val spmatT: typ
11.15
11.16 @@ -76,7 +76,7 @@
11.17 fun app (index, s) (lower, upper) =
11.18 let
11.19 val (flower, fupper) = approx_value prec pprt s
11.20 - val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
11.21 + val index = HOLogic.mk_number HOLogic.natT index
11.22 val elower = HOLogic.mk_prod (index, flower)
11.23 val eupper = HOLogic.mk_prod (index, fupper)
11.24 in (elower :: lower, eupper :: upper) end;
11.25 @@ -89,7 +89,7 @@
11.26 fun app (index, v) (lower, upper) =
11.27 let
11.28 val (flower, fupper) = approx_vector prec pprt v
11.29 - val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
11.30 + val index = HOLogic.mk_number HOLogic.natT index
11.31 val elower = HOLogic.mk_prod (index, flower)
11.32 val eupper = HOLogic.mk_prod (index, fupper)
11.33 in (elower :: lower, eupper :: upper) end;
12.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML Tue Sep 18 11:06:22 2007 +0200
12.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Tue Sep 18 16:08:00 2007 +0200
12.3 @@ -284,11 +284,10 @@
12.4 val index = xlen-i
12.5 val (r12_1, r12_2) = abs_estimate (i-1) r1 r2
12.6 val b1 = Inttab.lookup r1 index
12.7 - val b2 = Inttab.lookup r2 index
12.8 - val i' = Integer.int index
12.9 + val b2 = Inttab.lookup r2 index
12.10 in
12.11 - (add_row_entry r12_1 i' @{term "lbound :: real => real"} ((names index)^"l") b1,
12.12 - add_row_entry r12_2 i' @{term "ubound :: real => real"} ((names index)^"u") b2)
12.13 + (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1,
12.14 + add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2)
12.15 end
12.16
12.17 val (r1, r2) = abs_estimate xlen r1 r2
13.1 --- a/src/HOL/Numeral.thy Tue Sep 18 11:06:22 2007 +0200
13.2 +++ b/src/HOL/Numeral.thy Tue Sep 18 16:08:00 2007 +0200
13.3 @@ -635,12 +635,10 @@
13.4 code_modulename Haskell
13.5 Numeral Integer
13.6
13.7 -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
13.8 -
13.9 types_code
13.10 "int" ("int")
13.11 attach (term_of) {*
13.12 -val term_of_int = HOLogic.mk_number HOLogic.intT o IntInf.fromInt;
13.13 +val term_of_int = HOLogic.mk_number HOLogic.intT;
13.14 *}
13.15 attach (test) {*
13.16 fun gen_int i = one_of [~1, 1] * random_range 0 i;
13.17 @@ -656,7 +654,7 @@
13.18 let val i = HOLogic.dest_numeral (strip_number_of t)
13.19 in
13.20 SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
13.21 - Pretty.str (IntInf.toString i))
13.22 + Pretty.str (string_of_int i))
13.23 end handle TERM _ => NONE;
13.24
13.25 in
14.1 --- a/src/HOL/Real/Rational.thy Tue Sep 18 11:06:22 2007 +0200
14.2 +++ b/src/HOL/Real/Rational.thy Tue Sep 18 16:08:00 2007 +0200
14.3 @@ -697,8 +697,8 @@
14.4 val p = random_range 0 i;
14.5 val q = random_range 1 (i + 1);
14.6 val g = Integer.gcd p q;
14.7 - val p' = Integer.div p g;
14.8 - val q' = Integer.div q g;
14.9 + val p' = p div g;
14.10 + val q' = q div g;
14.11 in
14.12 (if one_of [true, false] then p' else ~ p',
14.13 if p' = 0 then 0 else q')
15.1 --- a/src/HOL/Real/RealDef.thy Tue Sep 18 11:06:22 2007 +0200
15.2 +++ b/src/HOL/Real/RealDef.thy Tue Sep 18 16:08:00 2007 +0200
15.3 @@ -1011,8 +1011,8 @@
15.4 val p = random_range 0 i;
15.5 val q = random_range 1 (i + 1);
15.6 val g = Integer.gcd p q;
15.7 - val p' = Integer.div p g;
15.8 - val q' = Integer.div q g;
15.9 + val p' = p div g;
15.10 + val q' = q div g;
15.11 in
15.12 (if one_of [true, false] then p' else ~ p',
15.13 if p' = 0 then 0 else q')
16.1 --- a/src/HOL/Real/float_arith.ML Tue Sep 18 11:06:22 2007 +0200
16.2 +++ b/src/HOL/Real/float_arith.ML Tue Sep 18 16:08:00 2007 +0200
16.3 @@ -9,7 +9,7 @@
16.4 val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
16.5
16.6 exception Floating_point of string
16.7 - val approx_dec_by_bin: integer -> Float.float -> Float.float * Float.float
16.8 + val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
16.9 val approx_decstr_by_bin: int -> string -> Float.float * Float.float
16.10
16.11 val mk_float: Float.float -> term
16.12 @@ -91,30 +91,30 @@
16.13 fun find_most_significant q r =
16.14 let
16.15 fun int2real i =
16.16 - case (Real.fromString o Integer.string_of_int) i of
16.17 + case (Real.fromString o string_of_int) i of
16.18 SOME r => r
16.19 | NONE => raise (Floating_point "int2real")
16.20 fun subtract (q, r) (q', r') =
16.21 - if r <=% r' then
16.22 + if r <= r' then
16.23 (q - q' * exp10 (r' - r), r)
16.24 else
16.25 (q * exp10 (r - r') - q', r')
16.26 fun bin2dec d =
16.27 - if 0 <=% d then
16.28 - (Integer.exp d, 0)
16.29 + if 0 <= d then
16.30 + (Integer.square d, 0)
16.31 else
16.32 (exp5 (~ d), d)
16.33
16.34 - val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10))
16.35 + val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
16.36 val L1 = L + 1
16.37
16.38 val (q1, r1) = subtract (q, r) (bin2dec L1)
16.39 in
16.40 - if 0 <=% q1 then
16.41 + if 0 <= q1 then
16.42 let
16.43 val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
16.44 in
16.45 - if 0 <=% q2 then
16.46 + if 0 <= q2 then
16.47 raise (Floating_point "find_most_significant")
16.48 else
16.49 (L1, (q1, r1))
16.50 @@ -123,7 +123,7 @@
16.51 let
16.52 val (q0, r0) = subtract (q, r) (bin2dec L)
16.53 in
16.54 - if 0 <=% q0 then
16.55 + if 0 <= q0 then
16.56 (L, (q0, r0))
16.57 else
16.58 raise (Floating_point "find_most_significant")
16.59 @@ -133,10 +133,10 @@
16.60 fun approx_dec_by_bin n (q,r) =
16.61 let
16.62 fun addseq acc d' [] = acc
16.63 - | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds
16.64 + | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds
16.65
16.66 fun seq2bin [] = (0, 0)
16.67 - | seq2bin (d::ds) = (addseq 0 d ds +% 1, d)
16.68 + | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
16.69
16.70 fun approx d_seq d0 precision (q,r) =
16.71 if q = 0 then
16.72 @@ -147,11 +147,11 @@
16.73 let
16.74 val (d, (q', r')) = find_most_significant q r
16.75 in
16.76 - if precision <% d0 - d then
16.77 + if precision < d0 - d then
16.78 let
16.79 val d' = d0 - precision
16.80 val x1 = seq2bin (d_seq)
16.81 - val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *)
16.82 + val x2 = (fst x1 * Integer.square (snd x1 - d') + 1, d') (* = seq2bin (d'::d_seq) *)
16.83 in
16.84 (x1, x2)
16.85 end
16.86 @@ -160,26 +160,26 @@
16.87 end
16.88
16.89 fun approx_start precision (q, r) =
16.90 - if q =% 0 then
16.91 + if q = 0 then
16.92 ((0, 0), (0, 0))
16.93 else
16.94 let
16.95 val (d, (q', r')) = find_most_significant q r
16.96 in
16.97 - if precision <=% 0 then
16.98 + if precision <= 0 then
16.99 let
16.100 val x1 = seq2bin [d]
16.101 in
16.102 if q' = 0 then
16.103 (x1, x1)
16.104 else
16.105 - (x1, seq2bin [d +% 1])
16.106 + (x1, seq2bin [d + 1])
16.107 end
16.108 else
16.109 approx [d] d precision (q', r')
16.110 end
16.111 in
16.112 - if 0 <=% q then
16.113 + if 0 <= q then
16.114 approx_start n (q,r)
16.115 else
16.116 let
16.117 @@ -191,16 +191,16 @@
16.118
16.119 fun approx_decstr_by_bin n decstr =
16.120 let
16.121 - fun str2int s = the_default 0 (Integer.int_of_string s);
16.122 - fun signint p x = if p then x else Integer.neg x
16.123 + fun str2int s = the_default 0 (Int.fromString s)
16.124 + fun signint p x = if p then x else ~ x
16.125
16.126 val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
16.127 - val s = Integer.int (size d2)
16.128 + val s = size d2
16.129
16.130 val q = signint p (str2int d1 * exp10 s + str2int d2)
16.131 val r = signint ep (str2int e) - s
16.132 in
16.133 - approx_dec_by_bin (Integer.int n) (q,r)
16.134 + approx_dec_by_bin n (q,r)
16.135 end
16.136
16.137 fun mk_float (a, b) = @{term "float"} $
17.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Sep 18 11:06:22 2007 +0200
17.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Sep 18 16:08:00 2007 +0200
17.3 @@ -41,8 +41,8 @@
17.4 (* ------------------------------------------------------------------------- *)
17.5
17.6 datatype history =
17.7 - Start of integer
17.8 - | Mmul of (Rat.rat * (integer list)) * history
17.9 + Start of int
17.10 + | Mmul of (Rat.rat * int list) * history
17.11 | Add of history * history;
17.12
17.13
17.14 @@ -54,8 +54,8 @@
17.15 ([],[]) => false
17.16 | (x1::o1,x2::o2) => x1 > x2 orelse x1 = x2 andalso lexorder o1 o2
17.17 | _ => error "morder: inconsistent monomial lengths"
17.18 - val n1 = fold Integer.add m1 0
17.19 - val n2 = fold Integer.add m2 0 in
17.20 + val n1 = Integer.sum m1
17.21 + val n2 = Integer.sum m2 in
17.22 n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
17.23 end;
17.24
17.25 @@ -80,7 +80,7 @@
17.26
17.27 fun grob_sub l1 l2 = grob_add l1 (grob_neg l2);
17.28
17.29 -fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2,map2 Integer.add m1 m2);
17.30 +fun grob_mmul (c1,m1) (c2,m2) = (c1*/c2, ListPair.map (op +) (m1, m2));
17.31
17.32 fun grob_cmul cm pol = map (grob_mmul cm) pol;
17.33
17.34 @@ -108,29 +108,27 @@
17.35 fun grob_pow vars l n =
17.36 if n < 0 then error "grob_pow: negative power"
17.37 else if n = 0 then [(rat_1,map (fn v => 0) vars)]
17.38 - else grob_mul l (grob_pow vars l (n -% 1));
17.39 -
17.40 -val max = fn (x: integer) => fn y => if x < y then y else x;
17.41 + else grob_mul l (grob_pow vars l (n - 1));
17.42
17.43 fun degree vn p =
17.44 case p of
17.45 [] => error "Zero polynomial"
17.46 | [(c,ns)] => nth ns vn
17.47 -| (c,ns)::p' => max (nth ns vn) (degree vn p');
17.48 +| (c,ns)::p' => Int.max (nth ns vn, degree vn p');
17.49
17.50 fun head_deg vn p = let val d = degree vn p in
17.51 (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;
17.52
17.53 -val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) (0: integer)) ns);
17.54 +val is_zerop = forall (fn (c,ns) => c =/ rat_0 andalso forall (curry (op =) 0) ns);
17.55 val grob_pdiv =
17.56 let fun pdiv_aux vn (n,a) p k s =
17.57 if is_zerop s then (k,s) else
17.58 let val (m,b) = head_deg vn s
17.59 in if m < n then (k,s) else
17.60 - let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m -% n else 0)
17.61 + let val p' = grob_mul p [(rat_1, map_index (fn (i,v) => if i = vn then m - n else 0)
17.62 (snd (hd s)))]
17.63 in if a = b then pdiv_aux vn (n,a) p k (grob_sub s p')
17.64 - else pdiv_aux vn (n,a) p (k +% 1) (grob_sub (grob_mul a s) (grob_mul b p'))
17.65 + else pdiv_aux vn (n,a) p (k + 1) (grob_sub (grob_mul a s) (grob_mul b p'))
17.66 end
17.67 end
17.68 in fn vn => fn s => fn p => pdiv_aux vn (head_deg vn p) p 0 s
17.69 @@ -140,11 +138,11 @@
17.70
17.71 fun mdiv (c1,m1) (c2,m2) =
17.72 (c1//c2,
17.73 - map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 -% n2) m1 m2);
17.74 + map2 (fn n1 => fn n2 => if n1 < n2 then error "mdiv" else n1 - n2) m1 m2);
17.75
17.76 (* Lowest common multiple of two monomials. *)
17.77
17.78 -fun mlcm (c1,m1) (c2,m2) = (rat_1,map2 max m1 m2);
17.79 +fun mlcm (c1,m1) (c2,m2) = (rat_1, ListPair.map Int.max (m1, m2));
17.80
17.81 (* Reduce monomial cm by polynomial pol, returning replacement for cm. *)
17.82
17.83 @@ -221,7 +219,7 @@
17.84 | _ => false;
17.85
17.86 fun poly_eq p1 p2 =
17.87 - forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: integer list) = m2) p1 p2;
17.88 + forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
17.89
17.90 fun memx ((p1,h1),(p2,h2)) ppairs =
17.91 not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);
17.92 @@ -237,7 +235,7 @@
17.93 (* Test for hitting constant polynomial. *)
17.94
17.95 fun constant_poly p =
17.96 - length p = 1 andalso forall (fn x => x = (0: integer)) (snd(hd p));
17.97 + length p = 1 andalso forall (fn x => x = 0) (snd(hd p));
17.98
17.99 (* ------------------------------------------------------------------------- *)
17.100 (* Grobner basis algorithm. *)
17.101 @@ -299,8 +297,7 @@
17.102 (* ------------------------------------------------------------------------- *)
17.103
17.104 fun grobner pols =
17.105 - let val npols = map2 (fn p => fn n => (p,Start n)) pols
17.106 - (map Integer.int (0 upto (length pols - 1)))
17.107 + let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
17.108 val phists = filter (fn (p,_) => not (null p)) npols
17.109 val bas = grobner_interreduce [] (map monic phists)
17.110 val prs0 = product bas bas
17.111 @@ -376,7 +373,7 @@
17.112 val pol' = augment pol
17.113 val allpols = (grob_sub (grob_mul grob_z pol') grob_1)::pols'
17.114 val (l,cert) = grobner_weak vars' allpols
17.115 - val d = fold_rev (fold_rev (max o hd o snd) o snd) cert 0
17.116 + val d = fold_rev (fold_rev (curry Int.max o hd o snd) o snd) cert 0
17.117 fun transform_monomial (c,m) =
17.118 grob_cmul (c,tl m) (grob_pow vars pol (d - hd m))
17.119 fun transform_polynomial q = fold_rev (grob_add o transform_monomial) q []
17.120 @@ -575,7 +572,7 @@
17.121 let fun holify_varpow (v,n) =
17.122 if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n) (* FIXME *)
17.123 fun holify_monomial vars (c,m) =
17.124 - let val xps = map holify_varpow (filter (fn (_,n) => n <> (0: integer)) (vars ~~ m))
17.125 + let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
17.126 in end_itlist ring_mk_mul (mk_const c :: xps)
17.127 end
17.128 fun holify_polynomial vars p =
17.129 @@ -624,7 +621,7 @@
17.130 grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
17.131 val (deg,l,cert) = grobner_strong vars pols pol
17.132 val th1 = Conv.fconv_rule((arg_conv o arg_conv)(binop_conv ring_normalize_conv)) nth
17.133 - val th2 = funpow (Integer.machine_int deg) (idom_rule o HOLogic.conj_intr th1) neq_01
17.134 + val th2 = funpow deg (idom_rule o HOLogic.conj_intr th1) neq_01
17.135 in (vars,l,cert,th2)
17.136 end)
17.137 (* val _ = writeln ("Translating certificate to HOL inferences") *)
17.138 @@ -637,7 +634,7 @@
17.139 if null pols then reflexive(mk_const rat_0) else
17.140 end_itlist mk_add
17.141 (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p)
17.142 - (nth eths (Integer.machine_int i) |> mk_meta_eq)) pols)
17.143 + (nth eths i |> mk_meta_eq)) pols)
17.144 val th1 = thm_fn herts_pos
17.145 val th2 = thm_fn herts_neg
17.146 val th3 = HOLogic.conj_intr(mk_add (symmetric th1) th2 |> mk_object_eq) noteqth
17.147 @@ -681,7 +678,7 @@
17.148 val pol = grobify_term vars tm
17.149 val cert = grobner_ideal vars pols pol
17.150 in map (fn n => these (AList.lookup (op =) cert n) |> holify_polynomial vars)
17.151 - (map Integer.int (0 upto (length pols - 1)))
17.152 + (0 upto (length pols - 1))
17.153 end
17.154 in (ring,ideal)
17.155 end;
18.1 --- a/src/HOL/Tools/Qelim/cooper.ML Tue Sep 18 11:06:22 2007 +0200
18.2 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Sep 18 16:08:00 2007 +0200
18.3 @@ -14,7 +14,6 @@
18.4
18.5 open Conv;
18.6 open Normalizer;
18.7 -structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
18.8
18.9 exception COOPER of string * exn;
18.10 val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
18.11 @@ -178,10 +177,10 @@
18.12 | linear_cmul n tm =
18.13 case tm of
18.14 Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)
18.15 - | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x
18.16 + | Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (fn m => n * m) c)$x
18.17 | Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)
18.18 | (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)
18.19 - | _ => numeral1 (Integer.mult n) tm;
18.20 + | _ => numeral1 (fn m => n * m) tm;
18.21 fun earlier [] x y = false
18.22 | earlier (h::t) x y =
18.23 if h aconv y then false else if h aconv x then true else earlier t x y;
18.24 @@ -191,7 +190,7 @@
18.25 (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,
18.26 Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>
18.27 if x1 = x2 then
18.28 - let val c = numeral2 Integer.add c1 c2
18.29 + let val c = numeral2 (curry op +) c1 c2
18.30 in if c = zero then linear_add vars r1 r2
18.31 else addC$(mulC$c$x1)$(linear_add vars r1 r2)
18.32 end
18.33 @@ -201,7 +200,7 @@
18.34 addC$(mulC$c1$x1)$(linear_add vars r1 tm2)
18.35 | (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>
18.36 addC$(mulC$c2$x2)$(linear_add vars tm1 r2)
18.37 - | (_,_) => numeral2 Integer.add tm1 tm2;
18.38 + | (_,_) => numeral2 (curry op +) tm1 tm2;
18.39
18.40 fun linear_neg tm = linear_cmul ~1 tm;
18.41 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
18.42 @@ -294,7 +293,7 @@
18.43 let
18.44 val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
18.45 val x = term_of cx
18.46 - val ins = insert (op = : integer*integer -> bool)
18.47 + val ins = insert (op = : int * int -> bool)
18.48 fun h (acc,dacc) t =
18.49 case (term_of t) of
18.50 Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
18.51 @@ -312,7 +311,7 @@
18.52 | Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
18.53 | _ => (acc, dacc)
18.54 val (cs,ds) = h ([],[]) p
18.55 - val l = fold Integer.lcm (cs union ds) 1
18.56 + val l = Integer.lcms (cs union ds)
18.57 fun cv k ct =
18.58 let val (tm as b$s$t) = term_of ct
18.59 in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
18.60 @@ -325,10 +324,10 @@
18.61 (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
18.62 @{cterm "0::int"})))
18.63 in equal_elim (Thm.symmetric th) TrueI end;
18.64 - val notz = let val tab = fold Integertab.update
18.65 - (ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty
18.66 + val notz = let val tab = fold Inttab.update
18.67 + (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
18.68 in
18.69 - (fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral))
18.70 + (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
18.71 handle Option => (writeln "noz: Theorems-Table contains no entry for";
18.72 print_cterm ct ; raise Option)))
18.73 end
18.74 @@ -340,15 +339,15 @@
18.75 | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
18.76 if x=y andalso member (op =)
18.77 ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
18.78 - then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
18.79 + then cv (l div dest_numeral c) t else Thm.reflexive t
18.80 | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>
18.81 if x=y andalso member (op =)
18.82 [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
18.83 - then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
18.84 + then cv (l div dest_numeral c) t else Thm.reflexive t
18.85 | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) =>
18.86 if x=y then
18.87 let
18.88 - val k = Integer.div l (dest_numeral c)
18.89 + val k = l div dest_numeral c
18.90 val kt = HOLogic.mk_number iT k
18.91 val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
18.92 ((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
18.93 @@ -384,7 +383,6 @@
18.94
18.95 val D_tm = @{cpat "?D::int"};
18.96
18.97 -val int_eq = (op =):integer*integer -> bool;
18.98 fun cooperex_conv ctxt vs q =
18.99 let
18.100
18.101 @@ -403,11 +401,11 @@
18.102 | Le t => (bacc, ins (plus1 t) aacc,dacc)
18.103 | Gt t => (ins t bacc, aacc,dacc)
18.104 | Ge t => (ins (minus1 t) bacc, aacc,dacc)
18.105 - | Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc)
18.106 - | NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)
18.107 + | Dvd (d,s) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
18.108 + | NDvd (d,s) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
18.109 | _ => (bacc, aacc, dacc)
18.110 val (b0,a0,ds) = h p ([],[],[])
18.111 - val d = fold Integer.lcm ds 1
18.112 + val d = Integer.lcms ds
18.113 val cd = Numeral.mk_cnumber @{ctyp "int"} d
18.114 val dt = term_of cd
18.115 fun divprop x =
18.116 @@ -417,9 +415,9 @@
18.117 (Thm.capply @{cterm Trueprop}
18.118 (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
18.119 in equal_elim (Thm.symmetric th) TrueI end;
18.120 - val dvd = let val tab = fold Integertab.update
18.121 - (ds ~~ (map divprop ds)) Integertab.empty in
18.122 - (fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral))
18.123 + val dvd = let val tab = fold Inttab.update
18.124 + (ds ~~ (map divprop ds)) Inttab.empty in
18.125 + (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
18.126 handle Option => (writeln "dvd: Theorems-Table contains no entry for";
18.127 print_cterm ct ; raise Option)))
18.128 end
18.129 @@ -545,7 +543,7 @@
18.130 | SOME n => Bound n)
18.131 | @{term "0::int"} => C 0
18.132 | @{term "1::int"} => C 1
18.133 - | Term.Bound i => Bound (Integer.int i)
18.134 + | Term.Bound i => Bound i
18.135 | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
18.136 | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
18.137 | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
18.138 @@ -641,8 +639,7 @@
18.139
18.140 fun cooper_oracle thy t =
18.141 let
18.142 - val (vs, ps) = pairself (map_index (swap o apfst Integer.int))
18.143 - (term_frees t, term_bools [] t);
18.144 + val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
18.145 in
18.146 equals propT $ HOLogic.mk_Trueprop t $
18.147 HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
19.1 --- a/src/HOL/Tools/numeral.ML Tue Sep 18 11:06:22 2007 +0200
19.2 +++ b/src/HOL/Tools/numeral.ML Tue Sep 18 16:08:00 2007 +0200
19.3 @@ -7,8 +7,8 @@
19.4
19.5 signature NUMERAL =
19.6 sig
19.7 - val mk_cnumeral: integer -> cterm
19.8 - val mk_cnumber: ctyp -> integer -> cterm
19.9 + val mk_cnumeral: int -> cterm
19.10 + val mk_cnumber: ctyp -> int -> cterm
19.11 end;
19.12
19.13 structure Numeral: NUMERAL =
19.14 @@ -23,9 +23,8 @@
19.15 fun mk_cnumeral 0 = @{cterm "Numeral.Pls"}
19.16 | mk_cnumeral ~1 = @{cterm "Numeral.Min"}
19.17 | mk_cnumeral i =
19.18 - let val (q, r) = Integer.divmod i 2 in
19.19 - Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q))
19.20 - (mk_cbit (Integer.machine_int r))
19.21 + let val (q, r) = Integer.div_mod i 2 in
19.22 + Thm.capply (Thm.capply @{cterm "Numeral.Bit"} (mk_cnumeral q)) (mk_cbit r)
19.23 end;
19.24
19.25
20.1 --- a/src/HOL/Tools/numeral_syntax.ML Tue Sep 18 11:06:22 2007 +0200
20.2 +++ b/src/HOL/Tools/numeral_syntax.ML Tue Sep 18 16:08:00 2007 +0200
20.3 @@ -23,7 +23,7 @@
20.4 fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b;
20.5 fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
20.6 | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min})
20.7 - | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
20.8 + | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
20.9 in mk value end;
20.10
20.11 in
20.12 @@ -54,7 +54,7 @@
20.13 | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
20.14
20.15 fun int_of [] = 0
20.16 - | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
20.17 + | int_of (b :: bs) = b + 2 * int_of bs;
20.18
20.19 fun dest_bin_str tm =
20.20 let
20.21 @@ -64,7 +64,7 @@
20.22 ~1 :: bs => ("-", leading 1 bs)
20.23 | bs => ("", leading 0 bs));
20.24 val i = int_of rev_digs;
20.25 - val num = IntInf.toString (IntInf.abs i);
20.26 + val num = string_of_int (abs i);
20.27 in
20.28 if (i = 0 orelse i = 1) andalso z = 0 then raise Match
20.29 else sign ^ implode (replicate z "0") ^ num
21.1 --- a/src/HOL/ex/Binary.thy Tue Sep 18 11:06:22 2007 +0200
21.2 +++ b/src/HOL/ex/Binary.thy Tue Sep 18 16:08:00 2007 +0200
21.3 @@ -29,8 +29,7 @@
21.4
21.5 fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
21.6 | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
21.7 - | dest_binary (Const ("Binary.bit", _) $ bs $ b) =
21.8 - 2 * dest_binary bs + IntInf.fromInt (dest_bit b)
21.9 + | dest_binary (Const ("Binary.bit", _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
21.10 | dest_binary t = raise TERM ("dest_binary", [t]);
21.11
21.12 fun mk_bit 0 = @{term False}
21.13 @@ -42,8 +41,8 @@
21.14 | mk_binary n =
21.15 if n < 0 then raise TERM ("mk_binary", [])
21.16 else
21.17 - let val (q, r) = IntInf.divMod (n, 2)
21.18 - in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
21.19 + let val (q, r) = Integer.div_mod n 2
21.20 + in @{term bit} $ mk_binary q $ mk_bit r end;
21.21 end
21.22 *}
21.23
21.24 @@ -162,7 +161,7 @@
21.25 fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
21.26 if n = 0 then NONE
21.27 else
21.28 - let val (k, l) = IntInf.divMod (m, n)
21.29 + let val (k, l) = Integer.div_mod m n
21.30 in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
21.31
21.32 end;
22.1 --- a/src/HOL/ex/Random.thy Tue Sep 18 11:06:22 2007 +0200
22.2 +++ b/src/HOL/ex/Random.thy Tue Sep 18 16:08:00 2007 +0200
22.3 @@ -131,30 +131,27 @@
22.4 ML {*
22.5 signature RANDOM =
22.6 sig
22.7 - type seed = IntInf.int;
22.8 + type seed = int;
22.9 val seed: unit -> seed;
22.10 - val value: IntInf.int -> seed -> IntInf.int * seed;
22.11 + val value: int -> seed -> int * seed;
22.12 end;
22.13
22.14 structure Random : RANDOM =
22.15 struct
22.16
22.17 -open IntInf;
22.18 -
22.19 exception RANDOM;
22.20
22.21 type seed = int;
22.22
22.23 local
22.24 - val a = fromInt 16807;
22.25 - (*greetings to SML/NJ*)
22.26 - val m = (the o fromString) "2147483647";
22.27 + val a = 16807;
22.28 + val m = 2147483647;
22.29 in
22.30 fun next s = (a * s) mod m;
22.31 end;
22.32
22.33 local
22.34 - val seed_ref = ref (fromInt 1);
22.35 + val seed_ref = ref 1;
22.36 in
22.37 fun seed () = CRITICAL (fn () =>
22.38 let
23.1 --- a/src/HOL/ex/coopereif.ML Tue Sep 18 11:06:22 2007 +0200
23.2 +++ b/src/HOL/ex/coopereif.ML Tue Sep 18 16:08:00 2007 +0200
23.3 @@ -10,8 +10,6 @@
23.4
23.5 open GeneratedCooper;
23.6
23.7 -val nat = GeneratedCooper.nat o Integer.int;
23.8 -
23.9 fun i_of_term vs t = case t
23.10 of Free(xn,xT) => (case AList.lookup (op aconv) vs t
23.11 of NONE => error "Variable not found in the list!"
24.1 --- a/src/HOL/ex/reflection.ML Tue Sep 18 11:06:22 2007 +0200
24.2 +++ b/src/HOL/ex/reflection.ML Tue Sep 18 16:08:00 2007 +0200
24.3 @@ -200,7 +200,7 @@
24.4 val t's = map (fn xn => snd (valOf (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*)
24.5 val subst_ns = map (fn (Const _ $ vs $ n, Var (xn0,T)) =>
24.6 (cert n, snd (valOf (AList.lookup (op =) tml xn0))
24.7 - |> (index_of #> IntInf.fromInt #> HOLogic.mk_nat #> cert)))
24.8 + |> (index_of #> HOLogic.mk_nat #> cert)))
24.9 subst
24.10 val subst_vs =
24.11 let
25.1 --- a/src/HOL/ex/svc_funcs.ML Tue Sep 18 11:06:22 2007 +0200
25.2 +++ b/src/HOL/ex/svc_funcs.ML Tue Sep 18 16:08:00 2007 +0200
25.3 @@ -27,12 +27,8 @@
25.4 | UnInterp of string * expr list
25.5 | FalseExpr
25.6 | TrueExpr
25.7 - | Int of IntInf.int
25.8 - | Rat of IntInf.int * IntInf.int;
25.9 -
25.10 - fun signedInt i =
25.11 - if i < 0 then "-" ^ IntInf.toString (~i)
25.12 - else IntInf.toString i;
25.13 + | Int of int
25.14 + | Rat of int * int;
25.15
25.16 fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
25.17
25.18 @@ -49,8 +45,8 @@
25.19 "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
25.20 | ue (FalseExpr) = "FALSE "
25.21 | ue (TrueExpr) = "TRUE "
25.22 - | ue (Int i) = (signedInt i) ^ " "
25.23 - | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
25.24 + | ue (Int i) = signed_string_of_int i ^ " "
25.25 + | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " "
25.26 in
25.27 ue t
25.28 end;
26.1 --- a/src/HOL/hologic.ML Tue Sep 18 11:06:22 2007 +0200
26.2 +++ b/src/HOL/hologic.ML Tue Sep 18 16:08:00 2007 +0200
26.3 @@ -82,8 +82,8 @@
26.4 val mk_Suc: term -> term
26.5 val dest_Suc: term -> term
26.6 val Suc_zero: term
26.7 - val mk_nat: integer -> term
26.8 - val dest_nat: term -> integer
26.9 + val mk_nat: int -> term
26.10 + val dest_nat: term -> int
26.11 val class_size: string
26.12 val size_const: typ -> term
26.13 val bitT: typ
26.14 @@ -95,12 +95,12 @@
26.15 val pls_const: term
26.16 val min_const: term
26.17 val bit_const: term
26.18 - val mk_numeral: integer -> term
26.19 - val dest_numeral: term -> integer
26.20 + val mk_numeral: int -> term
26.21 + val dest_numeral: term -> int
26.22 val number_of_const: typ -> term
26.23 val add_numerals: term -> (term * typ) list -> (term * typ) list
26.24 - val mk_number: typ -> integer -> term
26.25 - val dest_number: term -> typ * integer
26.26 + val mk_number: typ -> int -> term
26.27 + val dest_number: term -> typ * int
26.28 val realT: typ
26.29 val nibbleT: typ
26.30 val mk_nibble: int -> term
26.31 @@ -423,13 +423,13 @@
26.32
26.33 val Suc_zero = mk_Suc zero;
26.34
26.35 -fun mk_nat (n: integer) =
26.36 +fun mk_nat n =
26.37 let
26.38 fun mk 0 = zero
26.39 | mk n = mk_Suc (mk (n - 1));
26.40 in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
26.41
26.42 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer)
26.43 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
26.44 | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
26.45 | dest_nat t = raise TERM ("dest_nat", [t]);
26.46
26.47 @@ -465,13 +465,12 @@
26.48 fun mk_numeral 0 = pls_const
26.49 | mk_numeral ~1 = min_const
26.50 | mk_numeral i =
26.51 - let val (q, r) = Integer.divmod i 2
26.52 - in bit_const $ mk_numeral q $ mk_bit (Integer.machine_int r) end;
26.53 + let val (q, r) = Integer.div_mod i 2;
26.54 + in bit_const $ mk_numeral q $ mk_bit r end;
26.55
26.56 fun dest_numeral (Const ("Numeral.Pls", _)) = 0
26.57 | dest_numeral (Const ("Numeral.Min", _)) = ~1
26.58 - | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
26.59 - 2 * dest_numeral bs + Integer.int (dest_bit b)
26.60 + | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
26.61 | dest_numeral t = raise TERM ("dest_numeral", [t]);
26.62
26.63 fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
27.1 --- a/src/HOL/int_arith1.ML Tue Sep 18 11:06:22 2007 +0200
27.2 +++ b/src/HOL/int_arith1.ML Tue Sep 18 16:08:00 2007 +0200
27.3 @@ -147,9 +147,9 @@
27.4 (*Order integers by absolute value and then by sign. The standard integer
27.5 ordering is not well-founded.*)
27.6 fun num_ord (i,j) =
27.7 - (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
27.8 - EQUAL => int_ord (IntInf.sign i, IntInf.sign j)
27.9 - | ord => ord);
27.10 + (case int_ord (abs i, abs j) of
27.11 + EQUAL => int_ord (Int.sign i, Int.sign j)
27.12 + | ord => ord);
27.13
27.14 (*This resembles Term.term_ord, but it puts binary numerals before other
27.15 non-atomic terms.*)
27.16 @@ -265,11 +265,11 @@
27.17
27.18 (*Fractions as pairs of ints. Can't use Rat.rat because the representation
27.19 needs to preserve negative values in the denominator.*)
27.20 -fun mk_frac (p, q : IntInf.int) = if q = 0 then raise Div else (p, q);
27.21 +fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
27.22
27.23 (*Don't reduce fractions; sums must be proved by rule add_frac_eq.
27.24 Fractions are reduced later by the cancel_numeral_factor simproc.*)
27.25 -fun add_frac ((p1 : IntInf.int, q1 : IntInf.int), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
27.26 +fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
27.27
27.28 val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
27.29
27.30 @@ -421,9 +421,9 @@
27.31
27.32 structure CombineNumeralsData =
27.33 struct
27.34 - type coeff = IntInf.int
27.35 - val iszero = (fn x : IntInf.int => x = 0)
27.36 - val add = IntInf.+
27.37 + type coeff = int
27.38 + val iszero = (fn x => x = 0)
27.39 + val add = op +
27.40 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
27.41 val dest_sum = dest_sum
27.42 val mk_coeff = mk_coeff
27.43 @@ -451,8 +451,8 @@
27.44 (*Version for fields, where coefficients can be fractions*)
27.45 structure FieldCombineNumeralsData =
27.46 struct
27.47 - type coeff = IntInf.int * IntInf.int
27.48 - val iszero = (fn (p : IntInf.int, q) => p = 0)
27.49 + type coeff = int * int
27.50 + val iszero = (fn (p, q) => p = 0)
27.51 val add = add_frac
27.52 val mk_sum = long_mk_sum
27.53 val dest_sum = dest_sum
28.1 --- a/src/HOL/nat_simprocs.ML Tue Sep 18 11:06:22 2007 +0200
28.2 +++ b/src/HOL/nat_simprocs.ML Tue Sep 18 16:08:00 2007 +0200
28.3 @@ -20,7 +20,7 @@
28.4 (*Utilities*)
28.5
28.6 fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
28.7 -fun dest_number t = IntInf.max (0, snd (HOLogic.dest_number t));
28.8 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
28.9
28.10 fun find_first_numeral past (t::terms) =
28.11 ((dest_number t, t, rev past @ terms)
28.12 @@ -119,7 +119,7 @@
28.13 in
28.14 if relaxed orelse exists prod_has_numeral ts then
28.15 if k=0 then ts
28.16 - else mk_number (IntInf.fromInt k) :: ts
28.17 + else mk_number k :: ts
28.18 else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
28.19 end;
28.20
28.21 @@ -234,9 +234,9 @@
28.22
28.23 structure CombineNumeralsData =
28.24 struct
28.25 - type coeff = IntInf.int
28.26 - val iszero = (fn x : IntInf.int => x = 0)
28.27 - val add = IntInf.+
28.28 + type coeff = int
28.29 + val iszero = (fn x => x = 0)
28.30 + val add = op +
28.31 val mk_sum = (fn T:typ => long_mk_sum) (*to work for 2*x + 3*x *)
28.32 val dest_sum = dest_Sucs_sum false
28.33 val mk_coeff = mk_coeff
29.1 --- a/src/Provers/Arith/cancel_factor.ML Tue Sep 18 11:06:22 2007 +0200
29.2 +++ b/src/Provers/Arith/cancel_factor.ML Tue Sep 18 16:08:00 2007 +0200
29.3 @@ -60,12 +60,11 @@
29.4 val d = 0
29.5 |> fold (Integer.gcd o snd) tks
29.6 |> fold (Integer.gcd o snd) uks;
29.7 - val d' = Integer.machine_int d;
29.8 in
29.9 if d = 0 orelse d = 1 then NONE
29.10 else SOME
29.11 (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
29.12 - (t, Data.mk_bal (div_sum d' tks, div_sum d' uks)))
29.13 + (t, Data.mk_bal (div_sum d tks, div_sum d uks)))
29.14 end));
29.15
29.16
30.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML Tue Sep 18 11:06:22 2007 +0200
30.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Tue Sep 18 16:08:00 2007 +0200
30.3 @@ -22,8 +22,8 @@
30.4 (*abstract syntax*)
30.5 val mk_bal: term * term -> term
30.6 val dest_bal: term -> term * term
30.7 - val mk_coeff: IntInf.int * term -> term
30.8 - val dest_coeff: term -> IntInf.int * term
30.9 + val mk_coeff: int * term -> term
30.10 + val dest_coeff: term -> int * term
30.11 (*rules*)
30.12 val cancel: thm
30.13 val neg_exchanges: bool (*true if a negative coeff swaps the two operands,
31.1 --- a/src/Provers/Arith/cancel_numerals.ML Tue Sep 18 11:06:22 2007 +0200
31.2 +++ b/src/Provers/Arith/cancel_numerals.ML Tue Sep 18 16:08:00 2007 +0200
31.3 @@ -29,9 +29,9 @@
31.4 val dest_sum: term -> term list
31.5 val mk_bal: term * term -> term
31.6 val dest_bal: term -> term * term
31.7 - val mk_coeff: IntInf.int * term -> term
31.8 - val dest_coeff: term -> IntInf.int * term
31.9 - val find_first_coeff: term -> term list -> IntInf.int * term list
31.10 + val mk_coeff: int * term -> term
31.11 + val dest_coeff: term -> int * term
31.12 + val find_first_coeff: term -> term list -> int * term list
31.13 (*rules*)
31.14 val bal_add1: thm
31.15 val bal_add2: thm
32.1 --- a/src/Provers/Arith/fast_lin_arith.ML Tue Sep 18 11:06:22 2007 +0200
32.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Sep 18 16:08:00 2007 +0200
32.3 @@ -58,7 +58,7 @@
32.4
32.5 (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
32.6 val pre_tac: Proof.context -> int -> tactic
32.7 - val number_of: IntInf.int * typ -> term
32.8 + val number_of: int * typ -> term
32.9
32.10 (*the limit on the number of ~= allowed; because each ~= is split
32.11 into two cases, this can lead to an explosion*)
32.12 @@ -154,11 +154,11 @@
32.13 | NotLessD of injust
32.14 | NotLeD of injust
32.15 | NotLeDD of injust
32.16 - | Multiplied of IntInf.int * injust
32.17 - | Multiplied2 of IntInf.int * injust
32.18 + | Multiplied of int * injust
32.19 + | Multiplied2 of int * injust
32.20 | Added of injust * injust;
32.21
32.22 -datatype lineq = Lineq of IntInf.int * lineq_type * IntInf.int list * injust;
32.23 +datatype lineq = Lineq of int * lineq_type * int list * injust;
32.24
32.25 (* ------------------------------------------------------------------------- *)
32.26 (* Finding a (counter) example from the trace of a failed elimination *)
32.27 @@ -178,7 +178,7 @@
32.28 | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
32.29
32.30 (* PRE: ex[v] must be 0! *)
32.31 -fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) =
32.32 +fun eval ex v (a, le, cs) =
32.33 let
32.34 val rs = map Rat.rat_of_int cs;
32.35 val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
32.36 @@ -332,9 +332,9 @@
32.37 fun is_answer (ans as Lineq(k,ty,l,_)) =
32.38 case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
32.39
32.40 -fun calc_blowup (l:IntInf.int list) =
32.41 +fun calc_blowup l =
32.42 let val (p,n) = List.partition (curry (op <) 0) (List.filter (curry (op <>) 0) l)
32.43 - in (length p) * (length n) end;
32.44 + in length p * length n end;
32.45
32.46 (* ------------------------------------------------------------------------- *)
32.47 (* Main elimination code: *)
32.48 @@ -360,9 +360,9 @@
32.49 fun print_ineqs ineqs =
32.50 if !trace then
32.51 tracing(cat_lines(""::map (fn Lineq(c,t,l,_) =>
32.52 - IntInf.toString c ^
32.53 + string_of_int c ^
32.54 (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^
32.55 - commas(map IntInf.toString l)) ineqs))
32.56 + commas(map string_of_int l)) ineqs))
32.57 else ();
32.58
32.59 type history = (int * lineq list) list;
32.60 @@ -381,7 +381,7 @@
32.61 let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
32.62 if not (null eqs) then
32.63 let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
32.64 - val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
32.65 + val sclist = sort (fn (x,y) => int_ord (abs x, abs y))
32.66 (List.filter (fn i => i<>0) clist)
32.67 val c = hd sclist
32.68 val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
32.69 @@ -487,8 +487,8 @@
32.70 | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
32.71 | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
32.72 | mk (Added (j1, j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
32.73 - | mk (Multiplied (n, j)) = (trace_msg ("*" ^ IntInf.toString n); trace_thm "*" (multn (n, mk j)))
32.74 - | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ IntInf.toString n); trace_thm "**" (multn2 (n, mk j)))
32.75 + | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
32.76 + | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
32.77
32.78 in trace_msg "mkthm";
32.79 let val thm = trace_thm "Final thm:" (mk just)
32.80 @@ -507,13 +507,11 @@
32.81 end;
32.82
32.83 fun coeff poly atom =
32.84 - AList.lookup (op aconv) poly atom |> the_default (0: integer);
32.85 -
32.86 -fun lcms ks = fold Integer.lcm ks 1;
32.87 + AList.lookup (op aconv) poly atom |> the_default 0;
32.88
32.89 fun integ(rlhs,r,rel,rrhs,s,d) =
32.90 let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
32.91 - val m = lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
32.92 + val m = Integer.lcms(map (abs o snd o Rat.quotient_of_rat) (r :: s :: map snd rlhs @ map snd rrhs))
32.93 fun mult(t,r) =
32.94 let val (i,j) = Rat.quotient_of_rat r
32.95 in (t,i * (m div j)) end
32.96 @@ -547,9 +545,9 @@
32.97
32.98 fun print_atom((a,d),r) =
32.99 let val (p,q) = Rat.quotient_of_rat r
32.100 - val s = if d then IntInf.toString p else
32.101 + val s = if d then string_of_int p else
32.102 if p = 0 then "0"
32.103 - else IntInf.toString p ^ "/" ^ IntInf.toString q
32.104 + else string_of_int p ^ "/" ^ string_of_int q
32.105 in a ^ " = " ^ s end;
32.106
32.107 fun produce_ex sds =
33.1 --- a/src/Pure/Syntax/lexicon.ML Tue Sep 18 11:06:22 2007 +0200
33.2 +++ b/src/Pure/Syntax/lexicon.ML Tue Sep 18 16:08:00 2007 +0200
33.3 @@ -29,7 +29,7 @@
33.4 val var: indexname -> term
33.5 val read_nat: string -> int option
33.6 val read_int: string -> int option
33.7 - val read_xnum: string -> {radix: int, leading_zeros: int, value: IntInf.int}
33.8 + val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
33.9 val read_idents: string -> string list
33.10 val fixedN: string
33.11 val constN: string
33.12 @@ -402,7 +402,7 @@
33.13 | "0" :: "b" :: cs => (1, 2, cs)
33.14 | "-" :: cs => (~1, 10, cs)
33.15 | cs => (1, 10, cs));
33.16 - val value = IntInf.fromInt sign * #1 (Library.read_intinf radix digs);
33.17 + val value = sign * #1 (Library.read_radix_int radix digs);
33.18 in {radix = radix, leading_zeros = leading_zeros digs, value = value} end;
33.19
33.20 end;
34.1 --- a/src/Pure/library.ML Tue Sep 18 11:06:22 2007 +0200
34.2 +++ b/src/Pure/library.ML Tue Sep 18 16:08:00 2007 +0200
34.3 @@ -125,7 +125,7 @@
34.4 val string_of_int: int -> string
34.5 val signed_string_of_int: int -> string
34.6 val string_of_indexname: string * int -> string
34.7 - val read_intinf: int -> string list -> IntInf.int * string list
34.8 + val read_radix_int: int -> string list -> int * string list
34.9 val read_int: string list -> int * string list
34.10 val oct_char: string -> string
34.11
34.12 @@ -640,20 +640,20 @@
34.13
34.14 (* read integers *)
34.15
34.16 -fun read_intinf radix cs =
34.17 +fun read_radix_int radix cs =
34.18 let
34.19 val zero = ord "0";
34.20 val limit = zero + radix;
34.21 fun scan (num, []) = (num, [])
34.22 | scan (num, c :: cs) =
34.23 if zero <= ord c andalso ord c < limit then
34.24 - scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs)
34.25 + scan (radix * num + (ord c - zero), cs)
34.26 else (num, c :: cs);
34.27 - in scan (IntInf.fromInt 0, cs) end;
34.28 + in scan (0, cs) end;
34.29
34.30 -fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);
34.31 +val read_int = read_radix_int 10;
34.32
34.33 -fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));
34.34 +fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
34.35
34.36
34.37
35.1 --- a/src/Tools/code/code_target.ML Tue Sep 18 11:06:22 2007 +0200
35.2 +++ b/src/Tools/code/code_target.ML Tue Sep 18 16:08:00 2007 +0200
35.3 @@ -236,12 +236,12 @@
35.4 else if c = c_bit1 then SOME 1
35.5 else NONE
35.6 | dest_bit _ = NONE;
35.7 - fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME (IntInf.fromInt 0)
35.8 - else if c = c_min then SOME (IntInf.fromInt ~1)
35.9 + fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
35.10 + else if c = c_min then SOME ~1
35.11 else NONE
35.12 | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
35.13 if c = c_bit then case (dest_numeral t1, dest_bit t2)
35.14 - of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)
35.15 + of (SOME n, SOME b) => SOME (2 * n + b)
35.16 | _ => NONE
35.17 else NONE
35.18 | dest_numeral _ = NONE;
35.19 @@ -1631,15 +1631,15 @@
35.20 val pretty : (string * {
35.21 pretty_char: string -> string,
35.22 pretty_string: string -> string,
35.23 - pretty_numeral: bool -> IntInf.int -> string,
35.24 + pretty_numeral: bool -> int -> string,
35.25 pretty_list: Pretty.T list -> Pretty.T,
35.26 infix_cons: int * string
35.27 }) list = [
35.28 ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
35.29 pretty_string = ML_Syntax.print_string,
35.30 pretty_numeral = fn unbounded => fn k =>
35.31 - if unbounded then "(" ^ IntInf.toString k ^ " : IntInf.int)"
35.32 - else IntInf.toString k,
35.33 + if unbounded then "(" ^ string_of_int k ^ " : int)"
35.34 + else string_of_int k,
35.35 pretty_list = Pretty.enum "," "[" "]",
35.36 infix_cons = (7, "::")}),
35.37 ("OCaml", { pretty_char = fn c => enclose "'" "'"
35.38 @@ -1649,15 +1649,15 @@
35.39 else c
35.40 end),
35.41 pretty_string = (fn _ => error "OCaml: no pretty strings"),
35.42 - pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
35.43 + pretty_numeral = fn unbounded => fn k => if k >= 0 then
35.44 if unbounded then
35.45 - "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
35.46 - else IntInf.toString k
35.47 + "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
35.48 + else string_of_int k
35.49 else
35.50 if unbounded then
35.51 "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
35.52 - o IntInf.toString o op ~) k ^ ")"
35.53 - else (enclose "(" ")" o prefix "-" o IntInf.toString o op ~) k,
35.54 + o string_of_int o op ~) k ^ ")"
35.55 + else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
35.56 pretty_list = Pretty.enum ";" "[" "]",
35.57 infix_cons = (6, "::")}),
35.58 ("Haskell", { pretty_char = fn c => enclose "'" "'"
35.59 @@ -1667,10 +1667,8 @@
35.60 else c
35.61 end),
35.62 pretty_string = ML_Syntax.print_string,
35.63 - pretty_numeral = fn unbounded => fn k => if k >= IntInf.fromInt 0 then
35.64 - IntInf.toString k
35.65 - else
35.66 - (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
35.67 + pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
35.68 + else enclose "(" ")" (signed_string_of_int k),
35.69 pretty_list = Pretty.enum "," "[" "]",
35.70 infix_cons = (5, ":")})
35.71 ];
36.1 --- a/src/Tools/float.ML Tue Sep 18 11:06:22 2007 +0200
36.2 +++ b/src/Tools/float.ML Tue Sep 18 16:08:00 2007 +0200
36.3 @@ -7,7 +7,7 @@
36.4
36.5 signature FLOAT =
36.6 sig
36.7 - type float = integer * integer
36.8 + type float = int * int
36.9 val zero: float
36.10 val eq: float * float -> bool
36.11 val ord: float * float -> order
36.12 @@ -25,25 +25,25 @@
36.13 structure Float : FLOAT =
36.14 struct
36.15
36.16 -type float = integer * integer;
36.17 +type float = int * int;
36.18
36.19 val zero: float = (0, 0);
36.20
36.21 fun add (a1, b1) (a2, b2) =
36.22 - if Integer.ord (b1, b2) = LESS then
36.23 - (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
36.24 + if b1 < b2 then
36.25 + (a1 + a2 * Integer.square (b2 - b1), b1)
36.26 else
36.27 - (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
36.28 + (a1 * Integer.square (b1 - b2) + a2, b2);
36.29
36.30 fun sub (a1, b1) (a2, b2) =
36.31 - if Integer.ord (b1, b2) = LESS then
36.32 - (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
36.33 + if b1 < b2 then
36.34 + (a1 - a2 * Integer.square (b2 - b1), b1)
36.35 else
36.36 - (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
36.37 + (a1 * Integer.square (b1 - b2) - a2, b2);
36.38
36.39 -fun neg (a, b) = (Integer.neg a, b);
36.40 +fun neg (a, b) = (~ a, b);
36.41
36.42 -fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
36.43 +fun mult (a1, b1) (a2, b2) = (a1 * a2, b1 + b2);
36.44
36.45 fun sign (a, b) = Integer.sign a;
36.46
36.47 @@ -54,7 +54,7 @@
36.48 fun min r s = case ord (r, s) of LESS => r | _ => s;
36.49 fun max r s = case ord (r, s) of LESS => s | _ => r;
36.50
36.51 -fun positive_part (a, b) = (Integer.max 0 a, b);
36.52 -fun negative_part (a, b) = (Integer.min 0 a, b);
36.53 +fun positive_part (a, b) = (Int.max (0, a), b);
36.54 +fun negative_part (a, b) = (Int.min (0, a), b);
36.55
36.56 end;
37.1 --- a/src/Tools/integer.ML Tue Sep 18 11:06:22 2007 +0200
37.2 +++ b/src/Tools/integer.ML Tue Sep 18 16:08:00 2007 +0200
37.3 @@ -7,73 +7,27 @@
37.4
37.5 signature INTEGER =
37.6 sig
37.7 - eqtype int
37.8 - val zero: int
37.9 - val one: int
37.10 - val two: int
37.11 - val int: Int.int -> int
37.12 - val machine_int: int -> Int.int
37.13 - val string_of_int: int -> string
37.14 - val int_of_string: string -> int option
37.15 - val eq: int * int -> bool
37.16 - val ord: int * int -> order
37.17 - val le: int -> int -> bool
37.18 - val lt: int -> int -> bool
37.19 - val signabs: int -> order * int
37.20 val sign: int -> order
37.21 - val abs: int -> int
37.22 - val min: int -> int -> int
37.23 - val max: int -> int -> int
37.24 - val inc: int -> int
37.25 - val add: int -> int -> int
37.26 - val sub: int -> int -> int
37.27 - val mult: int -> int -> int
37.28 - val divmod: int -> int -> int * int
37.29 - val div: int -> int -> int
37.30 - val mod: int -> int -> int
37.31 - val neg: int -> int
37.32 - val exp: int -> int
37.33 - val log: int -> int
37.34 + val sum: int list -> int
37.35 + val div_mod: int -> int -> int * int
37.36 + val square: int -> int
37.37 val pow: int -> int -> int (* exponent -> base -> result *)
37.38 val gcd: int -> int -> int
37.39 + val gcds: int list -> int
37.40 val lcm: int -> int -> int
37.41 + val lcms: int list -> int
37.42 end;
37.43
37.44 structure Integer : INTEGER =
37.45 struct
37.46
37.47 -open IntInf;
37.48 +fun sign x = int_ord (x, 0);
37.49
37.50 -val int = fromInt;
37.51 +fun sum xs = fold (curry op +) xs 0;
37.52
37.53 -val zero = int 0;
37.54 -val one = int 1;
37.55 -val two = int 2;
37.56 +fun div_mod x y = IntInf.divMod (x, y);
37.57
37.58 -val machine_int = toInt;
37.59 -val string_of_int = toString;
37.60 -val int_of_string = fromString;
37.61 -
37.62 -val eq = op = : int * int -> bool;
37.63 -val ord = compare;
37.64 -val le = curry (op <=);
37.65 -val lt = curry (op <);
37.66 -
37.67 -fun sign k = ord (k, zero);
37.68 -fun signabs k = (ord (k, zero), abs k);
37.69 -
37.70 -val min = curry min;
37.71 -val max = curry max;
37.72 -
37.73 -val inc = curry (op +) one;
37.74 -
37.75 -val add = curry (op +);
37.76 -val sub = curry (op -);
37.77 -val mult = curry ( op * );
37.78 -val divmod = curry divMod;
37.79 -nonfix div val div = curry div;
37.80 -nonfix mod val mod = curry mod;
37.81 -val neg = ~;
37.82 +fun square x = x * x;
37.83
37.84 fun pow k l =
37.85 let
37.86 @@ -81,38 +35,24 @@
37.87 | pw 1 l = l
37.88 | pw k l =
37.89 let
37.90 - val (k', r) = divmod k 2;
37.91 - val l' = pw k' (mult l l);
37.92 - in if r = 0 then l' else mult l' l end;
37.93 - in if k < zero
37.94 + val (k', r) = div_mod k 2;
37.95 + val l' = pw k' (l * l);
37.96 + in if r = 0 then l' else l' * l end;
37.97 + in
37.98 + if k < 0
37.99 then error "pow: negative exponent"
37.100 else pw k l
37.101 end;
37.102
37.103 -fun exp k = pow k two;
37.104 -val log = int o log2;
37.105 -
37.106 fun gcd x y =
37.107 let
37.108 - fun gxd x y = if y = zero then x else gxd y (mod x y)
37.109 - in if lt x y then gxd y x else gxd x y end;
37.110 + fun gxd x y = if y = 0 then x else gxd y (x mod y)
37.111 + in if x < y then gxd y x else gxd x y end;
37.112
37.113 -fun lcm x y = div (mult x y) (gcd x y);
37.114 +fun gcds xs = fold gcd xs 0;
37.115 +
37.116 +fun lcm x y = (x * y) div (gcd x y);
37.117 +fun lcms xs = fold lcm xs 1;
37.118
37.119 end;
37.120
37.121 -type integer = Integer.int;
37.122 -
37.123 -infix 7 *%;
37.124 -infix 6 +% -%;
37.125 -infix 4 =% <% <=% >% >=% <>%;
37.126 -
37.127 -fun a +% b = Integer.add a b;
37.128 -fun a -% b = Integer.sub a b;
37.129 -fun a *% b = Integer.mult a b;
37.130 -fun a =% b = Integer.eq (a, b);
37.131 -fun a <% b = Integer.lt a b;
37.132 -fun a <=% b = Integer.le a b;
37.133 -fun a >% b = b <% a;
37.134 -fun a >=% b = b <=% a;
37.135 -fun a <>% b = not (a =% b);
38.1 --- a/src/Tools/rat.ML Tue Sep 18 11:06:22 2007 +0200
38.2 +++ b/src/Tools/rat.ML Tue Sep 18 16:08:00 2007 +0200
38.3 @@ -12,15 +12,14 @@
38.4 val zero: rat
38.5 val one: rat
38.6 val two: rat
38.7 - val rat_of_int: integer -> rat
38.8 - val rat_of_quotient: integer * integer -> rat
38.9 - val quotient_of_rat: rat -> integer * integer
38.10 + val rat_of_int: int -> rat
38.11 + val rat_of_quotient: int * int -> rat
38.12 + val quotient_of_rat: rat -> int * int
38.13 val string_of_rat: rat -> string
38.14 val eq: rat * rat -> bool
38.15 val ord: rat * rat -> order
38.16 val le: rat -> rat -> bool
38.17 val lt: rat -> rat -> bool
38.18 - val signabs: rat -> order * rat
38.19 val sign: rat -> order
38.20 val abs: rat -> rat
38.21 val add: rat -> rat -> rat
38.22 @@ -37,16 +36,16 @@
38.23 fun common (p1, q1) (p2, q2) =
38.24 let
38.25 val m = Integer.lcm q1 q2;
38.26 - in ((Integer.mult p1 (Integer.div m q1), Integer.mult p2 (Integer.div m q2)), m) end;
38.27 + in ((p1 * (m div q1), p2 * (m div q2)), m) end;
38.28
38.29 -datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)
38.30 +datatype rat = Rat of int * int; (*nominator, denominator (positive!)*)
38.31
38.32 exception DIVZERO;
38.33
38.34 fun rat_of_quotient (p, q) =
38.35 let
38.36 - val m = Integer.gcd (Integer.abs p) q
38.37 - in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO;
38.38 + val m = Integer.gcd (Int.abs p) q
38.39 + in Rat (p div m, q div m) end handle Div => raise DIVZERO;
38.40
38.41 fun quotient_of_rat (Rat r) = r;
38.42
38.43 @@ -57,11 +56,12 @@
38.44 val two = rat_of_int 2;
38.45
38.46 fun string_of_rat (Rat (p, q)) =
38.47 - Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;
38.48 + string_of_int p ^ "/" ^ string_of_int q;
38.49
38.50 fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
38.51
38.52 -fun ord (Rat (p1, q1), Rat (p2, q2)) = case (Integer.sign p1, Integer.sign p2)
38.53 +fun ord (Rat (p1, q1), Rat (p2, q2)) =
38.54 + case (Integer.sign p1, Integer.sign p2)
38.55 of (LESS, EQUAL) => LESS
38.56 | (LESS, GREATER) => LESS
38.57 | (EQUAL, LESS) => GREATER
38.58 @@ -69,38 +69,35 @@
38.59 | (EQUAL, GREATER) => LESS
38.60 | (GREATER, LESS) => GREATER
38.61 | (GREATER, EQUAL) => GREATER
38.62 - | _ => Integer.ord (fst (common (p1, q1) (p2, q2)));
38.63 + | _ => int_ord (fst (common (p1, q1) (p2, q2)));
38.64
38.65 fun le a b = not (ord (a, b) = GREATER);
38.66 fun lt a b = (ord (a, b) = LESS);
38.67
38.68 fun sign (Rat (p, _)) = Integer.sign p;
38.69
38.70 -fun abs (Rat (p, q)) = Rat (Integer.abs p, q);
38.71 -
38.72 -fun signabs (Rat (p, q)) =
38.73 - let
38.74 - val (s, p') = Integer.signabs p;
38.75 - in (s, Rat (p', q)) end;
38.76 +fun abs (Rat (p, q)) = Rat (Int.abs p, q);
38.77
38.78 fun add (Rat (p1, q1)) (Rat (p2, q2)) =
38.79 let
38.80 val ((m1, m2), n) = common (p1, q1) (p2, q2);
38.81 - in rat_of_quotient (Integer.add m1 m2, n) end;
38.82 + in rat_of_quotient (m1 + m2, n) end;
38.83
38.84 fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
38.85 - rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
38.86 + rat_of_quotient (p1 * p2, q1 * q2);
38.87
38.88 -fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
38.89 +fun neg (Rat (p, q)) = Rat (~ p, q);
38.90
38.91 -fun inv (Rat (p, q)) = case Integer.sign p
38.92 - of LESS => Rat (Integer.neg q, Integer.neg p)
38.93 +fun inv (Rat (p, q)) =
38.94 + case Integer.sign p
38.95 + of LESS => Rat (~ q, ~ p)
38.96 | EQUAL => raise DIVZERO
38.97 | GREATER => Rat (q, p);
38.98
38.99 -fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
38.100 +fun rounddown (Rat (p, q)) = Rat (p div q, 1);
38.101
38.102 -fun roundup (Rat (p, q)) = case Integer.divmod p q
38.103 +fun roundup (Rat (p, q)) =
38.104 + case Integer.div_mod p q
38.105 of (m, 0) => Rat (m, 1)
38.106 | (m, _) => Rat (m + 1, 1);
38.107
39.1 --- a/src/ZF/Tools/numeral_syntax.ML Tue Sep 18 11:06:22 2007 +0200
39.2 +++ b/src/ZF/Tools/numeral_syntax.ML Tue Sep 18 16:08:00 2007 +0200
39.3 @@ -8,8 +8,8 @@
39.4
39.5 signature NUMERAL_SYNTAX =
39.6 sig
39.7 - val dest_bin : term -> IntInf.int
39.8 - val mk_bin : IntInf.int -> term
39.9 + val dest_bin : term -> int
39.10 + val mk_bin : int -> term
39.11 val int_tr : term list -> term
39.12 val int_tr' : bool -> typ -> term list -> term
39.13 val setup : theory -> theory
39.14 @@ -23,7 +23,7 @@
39.15 val zero = Const("0", iT);
39.16 val succ = Const("succ", iT --> iT);
39.17
39.18 -fun mk_bit (0: IntInf.int) = zero
39.19 +fun mk_bit 0 = zero
39.20 | mk_bit 1 = succ$zero
39.21 | mk_bit _ = sys_error "mk_bit";
39.22
39.23 @@ -42,7 +42,7 @@
39.24 and min_const = Const ("Bin.bin.Min", iT)
39.25 and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
39.26
39.27 -fun mk_bin (i: IntInf.int) =
39.28 +fun mk_bin i =
39.29 let fun bin_of_int 0 = []
39.30 | bin_of_int ~1 = [~1]
39.31 | bin_of_int n = (n mod 2) :: bin_of_int (n div 2);
39.32 @@ -67,8 +67,8 @@
39.33 | bin_of _ = raise Match;
39.34
39.35 (*Convert a list of bits to an integer*)
39.36 -fun integ_of [] = 0 : IntInf.int
39.37 - | integ_of (b :: bs) = (IntInf.fromInt b) + 2 * integ_of bs;
39.38 +fun integ_of [] = 0
39.39 + | integ_of (b :: bs) = b + 2 * integ_of bs;
39.40
39.41 val dest_bin = integ_of o bin_of;
39.42
39.43 @@ -82,7 +82,7 @@
39.44 (case rev rev_digs of
39.45 ~1 :: bs => ("-", prefix_len (equal 1) bs)
39.46 | bs => ("", prefix_len (equal 0) bs));
39.47 - val num = IntInf.toString (abs (integ_of rev_digs));
39.48 + val num = string_of_int (abs (integ_of rev_digs));
39.49 in
39.50 "#" ^ sign ^ implode (replicate zs "0") ^ num
39.51 end;
40.1 --- a/src/ZF/arith_data.ML Tue Sep 18 11:06:22 2007 +0200
40.2 +++ b/src/ZF/arith_data.ML Tue Sep 18 16:08:00 2007 +0200
40.3 @@ -100,13 +100,13 @@
40.4 handle TERM _ => [t];
40.5
40.6 (*Dummy version: the only arguments are 0 and 1*)
40.7 -fun mk_coeff (0: IntInf.int, t) = zero
40.8 +fun mk_coeff (0, t) = zero
40.9 | mk_coeff (1, t) = t
40.10 | mk_coeff _ = raise TERM("mk_coeff", []);
40.11
40.12 (*Dummy version: the "coefficient" is always 1.
40.13 In the result, the factors are sorted terms*)
40.14 -fun dest_coeff t = (1 : IntInf.int, mk_prod (sort Term.term_ord (dest_prod t)));
40.15 +fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
40.16
40.17 (*Find first coefficient-term THAT MATCHES u*)
40.18 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
41.1 --- a/src/ZF/int_arith.ML Tue Sep 18 11:06:22 2007 +0200
41.2 +++ b/src/ZF/int_arith.ML Tue Sep 18 16:08:00 2007 +0200
41.3 @@ -293,9 +293,9 @@
41.4
41.5 structure CombineNumeralsData =
41.6 struct
41.7 - type coeff = IntInf.int
41.8 - val iszero = (fn x : IntInf.int => x = 0)
41.9 - val add = IntInf.+
41.10 + type coeff = int
41.11 + val iszero = (fn x => x = 0)
41.12 + val add = op +
41.13 val mk_sum = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
41.14 val dest_sum = dest_sum
41.15 val mk_coeff = mk_coeff
41.16 @@ -333,9 +333,9 @@
41.17
41.18 structure CombineNumeralsProdData =
41.19 struct
41.20 - type coeff = IntInf.int
41.21 - val iszero = (fn x : IntInf.int => x = 0)
41.22 - val add = IntInf.*
41.23 + type coeff = int
41.24 + val iszero = (fn x => x = 0)
41.25 + val add = op *
41.26 val mk_sum = (fn T:typ => mk_prod)
41.27 val dest_sum = dest_prod
41.28 fun mk_coeff(k,t) = if t=one then mk_numeral k