--- 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 *)
--- 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
()
--- 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);
--- 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)
--- 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 \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
|> simplify_less
|> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
--- 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
--- 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)")
--- 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 + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.+ ((_), (_))")
+ (SML "Int.+ ((_), (_))")
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
code_const "uminus \<Colon> int \<Rightarrow> int"
- (SML "IntInf.~")
+ (SML "Int.~")
(OCaml "Big'_int.minus'_big'_int")
(Haskell "negate")
code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.- ((_), (_))")
+ (SML "Int.- ((_), (_))")
(OCaml "Big'_int.sub'_big'_int")
(Haskell infixl 6 "-")
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.* ((_), (_))")
+ (SML "Int.* ((_), (_))")
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "!((_ : IntInf.int) = _)")
+ (SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "IntInf.<= ((_), (_))")
+ (SML "Int.<= ((_), (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> 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
--- 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
--- 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))
--- 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;
--- 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
--- 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
--- 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')
--- 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')
--- 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"} $
--- 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;
--- 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)))
--- 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;
--- 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
--- 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;
--- 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
--- 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!"
--- 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
--- 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;
--- 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);
--- 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
--- 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
--- 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));
--- 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,
--- 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
--- 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 =
--- 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;
--- 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)));
--- 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, ":")})
];
--- 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;
--- 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);
--- 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);
--- 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;
--- 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", [])
--- 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