# HG changeset patch
# User paulson
# Date 1116232155 -7200
# Node ID f422f82834914a7208c0cb2f11662c1252e95fe9
# Parent  f2074e12d1d4d9908e03d07efa14923874e44ba7
Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ

diff -r f2074e12d1d4 -r f422f8283491 TODO
--- a/TODO	Mon May 16 09:35:05 2005 +0200
+++ b/TODO	Mon May 16 10:29:15 2005 +0200
@@ -13,6 +13,8 @@
 - a global "disprove" menu item both as an action and (if it can be done)
   as a setting (Stefan & Tjark)
 
+- convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias)
+
 - update or remove ex/MT (Larry)  
 
 - Include IsaPlanner? (Larry to co-ordinate)
@@ -23,8 +25,6 @@
 
 - ball, bex and setsum congruence rules (Tobias & Stefan)
 
-- use IntInf.int (Steven)
-
 - html generation: somtimes lemma names and whole lemmas are missing.
   See http://afp.sourceforge.net/browser_info/current/HOL/HOL-Complex/Integration/SetsumThms.html
   (Markus?)
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Mon May 16 10:29:15 2005 +0200
@@ -860,7 +860,7 @@
 ML {*
 fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
       Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
-        (SOME (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin)))
+        (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
         handle TERM _ => NONE)
   | number_of_codegen thy gr s b (Const ("Numeral.number_of",
       Type ("fun", [_, Type ("nat", [])])) $ bin) =
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Mon May 16 10:29:15 2005 +0200
@@ -85,13 +85,14 @@
  
 fun mk_numeral 0 = Const("0",HOLogic.intT)
    |mk_numeral 1 = Const("1",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
+   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
  
 (*Transform an Term to an natural number*)	  
 	  
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
-   |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
+   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
+       IntInf.toInt (HOLogic.dest_binum n);
 (*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
@@ -245,12 +246,13 @@
 (* ------------------------------------------------------------------------- *) 
 (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
  
+(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
 fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
     (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
-    (is_arith_rel fm) andalso (x = y) then abs(dest_numeral c) else 1 
+    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
@@ -281,7 +283,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun unitycoeff x fm = 
-  let val l = formlcm x fm 
+  let val l = formlcm x fm
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
@@ -453,7 +455,8 @@
 
 
 val operations = 
-  [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
+  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
+   ("op >=",Int.>=), 
    ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
  
 fun applyoperation (SOME f) (a,b) = f (a, b) 
@@ -486,13 +489,14 @@
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
    ( case assoc (operations,p) of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
+                else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case assoc (operations,p) of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
-    HOLogic.false_const else HOLogic.true_const)  
+    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
+               then HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
       | _ =>  at; 
@@ -678,7 +682,8 @@
 (* Minusinfinity Version*) 
 fun coopermi vars1 fm = 
   case fm of 
-   Const ("Ex",_) $ Abs(x0,T,p0) => let 
+   Const ("Ex",_) $ Abs(x0,T,p0) => 
+   let 
     val (xn,p1) = variant_abs (x0,T,p0) 
     val x = Free (xn,T)  
     val vars = (xn::vars1) 
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon May 16 10:29:15 2005 +0200
@@ -149,8 +149,8 @@
 (*Order integers by absolute value and then by sign. The standard integer
   ordering is not well-founded.*)
 fun num_ord (i,j) =
-      (case Int.compare (abs i, abs j) of
-            EQUAL => Int.compare (Int.sign i, Int.sign j) 
+      (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
+            EQUAL => Int.compare (IntInf.sign i, IntInf.sign j) 
           | ord => ord);
 
 (*This resembles Term.term_ord, but it puts binary numerals before other
@@ -388,7 +388,7 @@
 
 structure CombineNumeralsData =
   struct
-  val add               = op + : int*int -> int
+  val add               = IntInf.+ 
   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
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Mon May 16 10:29:15 2005 +0200
@@ -29,7 +29,7 @@
 fun dest_numeral (Const ("0", _)) = 0
   | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
   | dest_numeral (Const("Numeral.number_of", _) $ w) =
-      (BasisLibrary.Int.max (0, HOLogic.dest_binum w)
+      (IntInf.max (0, HOLogic.dest_binum w)
        handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
 
@@ -245,7 +245,7 @@
 
 structure CombineNumeralsData =
   struct
-  val add               = op + : int*int -> int
+  val add               = IntInf.+
   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   val dest_sum          = restricted_dest_Sucs_sum
   val mk_coeff          = mk_coeff
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Main.thy	Mon May 16 10:29:15 2005 +0200
@@ -32,11 +32,12 @@
 
 quickcheck_params [default_type = int]
 
+(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
 ML {*
 fun wf_rec f x = f (wf_rec f) x;
 
 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-val term_of_int = HOLogic.mk_int;
+val term_of_int = HOLogic.mk_int o IntInf.fromInt;
 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
 
 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 10:29:15 2005 +0200
@@ -85,13 +85,14 @@
  
 fun mk_numeral 0 = Const("0",HOLogic.intT)
    |mk_numeral 1 = Const("1",HOLogic.intT)
-   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
+   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
  
 (*Transform an Term to an natural number*)	  
 	  
 fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
-   |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
+   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
+       IntInf.toInt (HOLogic.dest_binum n);
 (*Some terms often used for pattern matching*) 
  
 val zero = mk_numeral 0; 
@@ -245,12 +246,13 @@
 (* ------------------------------------------------------------------------- *) 
 (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
  
+(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
 fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
 fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
  
 fun formlcm x fm = case fm of 
     (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
-    (is_arith_rel fm) andalso (x = y) then abs(dest_numeral c) else 1 
+    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
   | ( Const ("Not", _) $p) => formlcm x p 
   | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
   | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
@@ -281,7 +283,7 @@
 (* ------------------------------------------------------------------------- *) 
  
 fun unitycoeff x fm = 
-  let val l = formlcm x fm 
+  let val l = formlcm x fm
       val fm' = adjustcoeff x l fm in
       if l = 1 then fm' 
 	 else 
@@ -453,7 +455,8 @@
 
 
 val operations = 
-  [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
+  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
+   ("op >=",Int.>=), 
    ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
  
 fun applyoperation (SOME f) (a,b) = f (a, b) 
@@ -486,13 +489,14 @@
 fun evalc_atom at = case at of  
   (Const (p,_) $ s $ t) =>
    ( case assoc (operations,p) of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
+                else HOLogic.false_const)  
     handle _ => at) 
       | _ =>  at) 
       |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
   case assoc (operations,p) of 
-    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
-    HOLogic.false_const else HOLogic.true_const)  
+    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
+               then HOLogic.false_const else HOLogic.true_const)  
     handle _ => at) 
       | _ =>  at) 
       | _ =>  at; 
@@ -678,7 +682,8 @@
 (* Minusinfinity Version*) 
 fun coopermi vars1 fm = 
   case fm of 
-   Const ("Ex",_) $ Abs(x0,T,p0) => let 
+   Const ("Ex",_) $ Abs(x0,T,p0) => 
+   let 
     val (xn,p1) = variant_abs (x0,T,p0) 
     val x = Free (xn,T)  
     val vars = (xn::vars1) 
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Mon May 16 10:29:15 2005 +0200
@@ -317,7 +317,8 @@
 fun make_nnf th = th |> simplify nnf_ss
                      |> check_no_bool |> make_nnf1
 
-(*Pull existential quantifiers (Skolemization)*)
+(*Pull existential quantifiers to front. This accomplishes Skolemization for
+  clauses that arise from a subgoal.*)
 fun skolemize th =
   if not (has_consts ["Ex"] (prop_of th)) then th
   else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
@@ -331,7 +332,7 @@
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
 fun make_clauses ths =
-   (  sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
+    (sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
 
 
 (*Convert a list of clauses to (contrapositive) Horn clauses*)
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Mon May 16 10:29:15 2005 +0200
@@ -28,7 +28,7 @@
       (case rev rev_digs of
         ~1 :: bs => ("-", prefix_len (equal 1) bs)
       | bs => ("", prefix_len (equal 0) bs));
-    val i = HOLogic.intinf_of rev_digs;
+    val i = HOLogic.int_of rev_digs;
     val num = IntInf.toString (IntInf.abs i);
   in
     if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
@@ -38,7 +38,7 @@
 (* translation of integer numeral tokens to and from bitstrings *)
 
 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
-      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin_from_intinf (valOf (IntInf.fromString str))))
+      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/arith_data.ML	Mon May 16 10:29:15 2005 +0200
@@ -265,27 +265,27 @@
 let
 fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
         Const("Numeral.number_of",_)$n
-        => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
+        => demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
       | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
-        => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
+        => demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n))))
       | Const("Suc",_) $ _
         => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
       | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
       | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
           let val den = HOLogic.dest_binum dent
           in if den = 0 then raise Zero
-             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_int den)))
+             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den)))
           end
       | _ => atomult(mC,s,t,m)
       ) handle TERM _ => atomult(mC,s,t,m))
   | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) =
       (let val den = HOLogic.dest_binum dent
-       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
+       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end
        handle TERM _ => (SOME atom,m))
   | demult(Const("0",_),m) = (NONE, rat_of_int 0)
   | demult(Const("1",_),m) = (NONE, m)
   | demult(t as Const("Numeral.number_of",_)$n,m) =
-      ((NONE,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
+      ((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
        handle TERM _ => (SOME t,m))
   | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
   | demult(t as Const f $ x, m) =
@@ -316,7 +316,7 @@
          (NONE,m') => (p,ratadd(i,m'))
        | (SOME u,m') => add_atom(u,m',pi))
   | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
-      ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
+      ((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t))))
        handle TERM _ => add_atom all)
   | poly(all as Const f $ x, m, pi) =
       if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
@@ -363,7 +363,8 @@
   let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
   in decomp2 (sg,discrete,inj_consts) end
 
-fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
+(*FIXME: remove the IntInf.fromInt when linear arithmetic is converted to IntInfs*)
+fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin (IntInf.fromInt n))
 
 end;
 
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/ex/BinEx.thy	Mon May 16 10:29:15 2005 +0200
@@ -186,6 +186,10 @@
 lemma "(1234567::int) \<le> 1234567"
   by simp
 
+text{*No integer overflow!*}
+lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
+  by simp
+
 
 text {* \medskip Quotient and Remainder *}
 
@@ -205,7 +209,7 @@
 
 text {*
   A negative dividend\footnote{The definition agrees with mathematical
-  convention but not with the hardware of most computers}
+  convention and with ML, but not with the hardware of most computers}
 *}
 
 lemma "(-10::int) div 3 = -4"
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Mon May 16 10:29:15 2005 +0200
@@ -27,14 +27,14 @@
    | UnInterp of string * expr list
    | FalseExpr 
    | TrueExpr
-   | Int of int
-   | Rat of int * int;
+   | Int of IntInf.int
+   | Rat of IntInf.int * IntInf.int;
 
  open BasisLibrary
 
  fun signedInt i = 
-     if i < 0 then "-" ^ Int.toString (~i)
-     else Int.toString i;
+     if i < 0 then "-" ^ IntInf.toString (~i)
+     else IntInf.toString i;
 	 
  fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
  
diff -r f2074e12d1d4 -r f422f8283491 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/HOL/hologic.ML	Mon May 16 10:29:15 2005 +0200
@@ -17,6 +17,7 @@
   val not_const: term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
+  val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
   val conj: term
@@ -70,7 +71,7 @@
   val mk_nat: int -> term
   val dest_nat: term -> int
   val intT: typ
-  val mk_int: int -> term
+  val mk_int: IntInf.int -> term
   val realT: typ
   val bitT: typ
   val B0_const: term
@@ -80,11 +81,9 @@
   val min_const: term
   val bit_const: term
   val number_of_const: typ -> term
-  val int_of: int list -> int
-  val intinf_of: int list -> IntInf.int
-  val dest_binum: term -> int
-  val mk_bin: int -> term
-  val mk_bin_from_intinf: IntInf.int -> term
+  val int_of: int list -> IntInf.int 
+  val dest_binum: term -> IntInf.int
+  val mk_bin: IntInf.int -> term
   val bin_of : term -> int list
   val mk_list: ('a -> term) -> typ -> 'a list -> term
   val dest_list: term -> term list
@@ -311,12 +310,8 @@
 
 fun number_of_const T = Const ("Numeral.number_of", binT --> T);
 
-
-fun int_of [] = 0
-  | int_of (b :: bs) = b + 2 * int_of bs;
-
-fun intinf_of [] = IntInf.fromInt 0
-  | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
+fun int_of [] = 0 
+  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
 
 (*When called from a print translation, the Numeral qualifier will probably have
   been removed from Bit, bin.B0, etc.*)
@@ -338,22 +333,18 @@
   | mk_bit 1 = B1_const
   | mk_bit _ = sys_error "mk_bit";
 
-fun mk_bin_from_intinf  n =
+fun mk_bin  n =
     let
-	val zero = IntInf.fromInt 0
-	val minus_one = IntInf.fromInt ~1
-	val two = IntInf.fromInt 2
-
-	fun mk_bit n = if n = zero then B0_const else B1_const
+	fun mk_bit n = if n = 0 then B0_const else B1_const
 								 
 	fun bin_of n = 
-	    if n = zero then pls_const
-	    else if n = minus_one then min_const
+	    if n = 0 then pls_const
+	    else if n = ~1 then min_const
 	    else 
 		let 
-		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!*)
-	            val q = IntInf.div (n, two)
-		    val r = IntInf.mod (n, two)
+		    (*val (q,r) = IntInf.divMod (n, 2): doesn't work in SML 10.0.7, but in newer versions!  FIXME: put this back after new SML released!*)
+	            val q = IntInf.div (n, 2)
+		    val r = IntInf.mod (n, 2)
 		in
 		    bit_const $ bin_of q $ mk_bit r
 		end
@@ -361,8 +352,6 @@
 	bin_of n
     end
 
-val mk_bin = mk_bin_from_intinf o IntInf.fromInt;
-
 
 (* int *)
 
diff -r f2074e12d1d4 -r f422f8283491 src/Provers/Arith/cancel_factor.ML
--- a/src/Provers/Arith/cancel_factor.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/cancel_factor.ML	Mon May 16 10:29:15 2005 +0200
@@ -15,7 +15,7 @@
   (*rules*)
   val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
   val norm_tac: tactic			(*AC0 etc.*)
-  val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
+  val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
 end;
 
 signature CANCEL_FACTOR =
diff -r f2074e12d1d4 -r f422f8283491 src/Provers/Arith/cancel_numeral_factor.ML
--- a/src/Provers/Arith/cancel_numeral_factor.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML	Mon May 16 10:29:15 2005 +0200
@@ -22,8 +22,8 @@
   (*abstract syntax*)
   val mk_bal: term * term -> term
   val dest_bal: term -> term * term
-  val mk_coeff: int * term -> term
-  val dest_coeff: term -> int * term
+  val mk_coeff: IntInf.int * term -> term
+  val dest_coeff: term -> IntInf.int * term
   (*rules*)
   val cancel: thm
   val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
@@ -45,11 +45,6 @@
 =
 struct
 
-
-(* greatest common divisor *)
-fun gcd (0, n) = abs n
-  | gcd (m, n) = gcd (n mod m, m);
-
 (*the simplification procedure*)
 fun proc sg ss t =
   let
@@ -61,7 +56,7 @@
       and (m2, t2') = Data.dest_coeff t2
       val d = (*if both are negative, also divide through by ~1*)
           if (m1<0 andalso m2<=0) orelse
-             (m1<=0 andalso m2<0) then ~ (gcd(m1,m2)) else gcd(m1,m2)
+             (m1<=0 andalso m2<0) then ~ (abs(gcd(m1,m2))) else abs (gcd(m1,m2))
       val _ = if d=1 then   (*trivial, so do nothing*)
 		      raise TERM("cancel_numeral_factor", []) 
               else ()
diff -r f2074e12d1d4 -r f422f8283491 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Mon May 16 10:29:15 2005 +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: int * term -> term
-  val dest_coeff: term -> int * term
-  val find_first_coeff: term -> term list -> int * term list
+  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
   (*rules*)
   val bal_add1: thm
   val bal_add2: thm
diff -r f2074e12d1d4 -r f422f8283491 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Mon May 16 10:29:15 2005 +0200
@@ -19,11 +19,11 @@
 signature COMBINE_NUMERALS_DATA =
 sig
   (*abstract syntax*)
-  val add: int * int -> int          (*addition (or multiplication) *)
+  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
   val mk_sum: typ -> term list -> term
   val dest_sum: term -> term list
-  val mk_coeff: int * term -> term
-  val dest_coeff: term -> int * term
+  val mk_coeff: IntInf.int * term -> term
+  val dest_coeff: term -> IntInf.int * term
   (*rules*)
   val left_distrib: thm
   (*proof tools*)
diff -r f2074e12d1d4 -r f422f8283491 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 10:29:15 2005 +0200
@@ -15,6 +15,8 @@
 
 Only take premises and conclusions into account that are already (negated)
 (in)equations. lin_arith_prover tries to prove or disprove the term.
+
+FIXME: convert to IntInf.int throughout. 
 *)
 
 (* Debugging: set Fast_Arith.trace *)
@@ -189,15 +191,15 @@
 val ratrelmax = foldr1 ratrelmax2;
 
 fun ratroundup r = let val (p,q) = rep_rat r
-                   in if q=1 then r else rat_of_int((p div q) + 1) end
+                   in if q=1 then r else rat_of_intinf((p div q) + 1) end
 
 fun ratrounddown r = let val (p,q) = rep_rat r
-                     in if q=1 then r else rat_of_int((p div q) - 1) end
+                     in if q=1 then r else rat_of_intinf((p div q) - 1) end
 
 fun ratexact up (r,exact) =
   if exact then r else
   let val (p,q) = rep_rat r
-      val nth = ratinv(rat_of_int q)
+      val nth = ratinv(rat_of_intinf q)
   in ratadd(r,if up then nth else ratneg nth) end;
 
 fun ratmiddle(r,s) = ratmul(ratadd(r,s),ratinv(rat_of_int 2));
@@ -299,7 +301,7 @@
 
 fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
   let val c1 = el v l1 and c2 = el v l2
-      val m = lcm(abs c1,abs c2)
+      val m = IntInf.toInt (lcm(IntInf.fromInt (abs c1), IntInf.fromInt(abs c2)))
       val m1 = m div (abs c1) and m2 = m div (abs c2)
       val (n1,n2) =
         if (c1 >= 0) = (c2 >= 0)
@@ -497,12 +499,15 @@
 
 fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i;
 
-fun lcms is = Library.foldl lcm (1,is);
+fun lcms_intinf is = Library.foldl lcm (1, is);
+fun lcms is = IntInf.toInt (lcms_intinf (map IntInf.fromInt is));
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
-let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s
-    val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs))
-    fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end
+let val (rn,rd) = pairself IntInf.toInt (rep_rat r) and (sn,sd) = pairself IntInf.toInt (rep_rat s)
+    val m = IntInf.toInt (lcms_intinf(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)))
+    fun mult(t,r) = 
+        let val (i,j) =  pairself IntInf.toInt (rep_rat r) 
+        in (t,i * (m div j)) end
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
 
 fun mklineq n atoms =
@@ -533,9 +538,9 @@
 
 fun print_atom((a,d),r) =
   let val (p,q) = rep_rat r
-      val s = if d then string_of_int p else
+      val s = if d then IntInf.toString p else
               if p = 0 then "0"
-              else string_of_int p ^ "/" ^ string_of_int q
+              else IntInf.toString p ^ "/" ^ IntInf.toString q
   in a ^ " = " ^ s end;
 
 fun print_ex sds =
diff -r f2074e12d1d4 -r f422f8283491 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon May 16 10:29:15 2005 +0200
@@ -30,7 +30,7 @@
   val skolem: string -> string
   val dest_skolem: string -> string
   val read_nat: string -> int option
-  val read_xnum: string -> int
+  val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
 end;
 
@@ -365,6 +365,16 @@
 
 (* read_xnum *)
 
+fun read_intinf cs : IntInf.int * string list =
+  let val zero = ord"0"
+      val limit = zero+10
+      fun scan (num,[]) = (num,[])
+        | scan (num, c::cs) =
+              if  zero <= ord c  andalso  ord c < limit
+              then scan(10*num + IntInf.fromInt (ord c - zero), cs)
+              else (num, c::cs)
+  in  scan(0,cs)  end;
+
 fun read_xnum str =
   let
     val (sign, digs) =
@@ -373,7 +383,7 @@
       | "#" :: cs => (1, cs)
       | "-" :: cs => (~1, cs)
       | cs => (1, cs));
-  in sign * #1 (Library.read_int digs) end;
+  in sign * #1 (read_intinf digs) end;
 
 
 (* read_ident(s) *)
diff -r f2074e12d1d4 -r f422f8283491 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/Pure/library.ML	Mon May 16 10:29:15 2005 +0200
@@ -117,8 +117,8 @@
   val suffixes1: 'a list -> 'a list list
 
   (*integers*)
-  val gcd: int * int -> int
-  val lcm: int * int -> int
+  val gcd: IntInf.int * IntInf.int -> IntInf.int
+  val lcm: IntInf.int * IntInf.int -> IntInf.int
   val inc: int ref -> int
   val dec: int ref -> int
   val upto: int * int -> int list
@@ -136,13 +136,14 @@
   (*rational numbers*)
   type rat
   exception RAT of string
-  val rep_rat: rat -> int * int
+  val rep_rat: rat -> IntInf.int * IntInf.int
   val ratadd: rat * rat -> rat
   val ratmul: rat * rat -> rat
   val ratinv: rat -> rat
-  val int_ratdiv: int * int -> rat
+  val int_ratdiv: IntInf.int * IntInf.int -> rat
   val ratneg: rat -> rat
   val rat_of_int: int -> rat
+  val rat_of_intinf: IntInf.int -> rat
 
   (*strings*)
   val nth_elem_string: int * string -> string
@@ -665,7 +666,7 @@
 (** integers **)
 
 fun gcd(x,y) =
-  let fun gxd x y =
+  let fun gxd x y : IntInf.int =
     if y = 0 then x else gxd y (x mod y)
   in if x < y then gxd y x else gxd x y end;
 
@@ -1186,7 +1187,7 @@
 
 (** rational numbers **)
 
-datatype rat = Rat of bool * int * int
+datatype rat = Rat of bool * IntInf.int * IntInf.int
 
 exception RAT of string;
 
@@ -1212,7 +1213,9 @@
 
 fun ratneg(Rat(b,p,q)) = Rat(not b,p,q);
 
-fun rat_of_int i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
+fun rat_of_intinf i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
+
+fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
 
 
 (** misc **)
diff -r f2074e12d1d4 -r f422f8283491 src/ZF/Integ/int_arith.ML
--- a/src/ZF/Integ/int_arith.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/ZF/Integ/int_arith.ML	Mon May 16 10:29:15 2005 +0200
@@ -291,7 +291,7 @@
 
 structure CombineNumeralsData =
   struct
-  val add               = op + : int*int -> int
+  val add               = IntInf.+ 
   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
@@ -327,7 +327,7 @@
 
 structure CombineNumeralsProdData =
   struct
-  val add               = op * : int*int -> int
+  val add               = IntInf.*
   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
diff -r f2074e12d1d4 -r f422f8283491 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML	Mon May 16 10:29:15 2005 +0200
@@ -8,8 +8,8 @@
 
 signature NUMERAL_SYNTAX =
 sig
-  val dest_bin : term -> int
-  val mk_bin   : int -> term
+  val dest_bin : term -> IntInf.int
+  val mk_bin   : IntInf.int -> term
   val int_tr   : term list -> term
   val int_tr'  : bool -> typ -> term list -> term
   val setup    : (theory -> theory) list
@@ -23,7 +23,7 @@
 val zero = Const("0", iT);
 val succ = Const("succ", iT --> iT);
 
-fun mk_bit 0 = zero
+fun mk_bit (0: IntInf.int) = zero
   | mk_bit 1 = succ$zero
   | mk_bit _ = sys_error "mk_bit";
 
@@ -42,16 +42,16 @@
 and min_const = Const ("Bin.bin.Min", iT)
 and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
 
-fun mk_bin i =
-  let fun bin_of 0  = []
-	| bin_of ~1 = [~1]
-	| bin_of n  = (n mod 2) :: bin_of (n div 2);
+fun mk_bin (i: IntInf.int) =
+  let fun bin_of_int 0  = []
+  	    | bin_of_int ~1 = [~1]
+    	| bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
 
       fun term_of []   = pls_const
-	| term_of [~1] = min_const
-	| term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
+	    | term_of [~1] = min_const
+	    | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
   in
-    term_of (bin_of i)
+    term_of (bin_of_int i)
   end;
 
 (*we consider all "spellings", since they could vary depending on the caller*)
@@ -66,13 +66,15 @@
   | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
-fun integ_of [] = 0
-  | integ_of (b :: bs) = b + 2 * integ_of bs;
+(*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;
 
 val dest_bin = integ_of o bin_of;
 
-(*leading 0s and (for negative numbers) -1s cause complications,
-  though they should never arise in normal use.*)
+(*leading 0s and (for negative numbers) -1s cause complications, though they 
+  should never arise in normal use. The formalization used in HOL prevents 
+  them altogether.*)
 fun show_int t =
   let
     val rev_digs = bin_of t;
@@ -80,7 +82,7 @@
 	(case rev rev_digs of
 	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
 	   | bs =>       ("",  prefix_len (equal 0) bs));
-    val num = string_of_int (abs (integ_of rev_digs));
+    val num = IntInf.toString (abs (integ_of rev_digs));
   in
     "#" ^ sign ^ implode (replicate zs "0") ^ num
   end;
diff -r f2074e12d1d4 -r f422f8283491 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Mon May 16 09:35:05 2005 +0200
+++ b/src/ZF/arith_data.ML	Mon May 16 10:29:15 2005 +0200
@@ -101,13 +101,13 @@
       handle TERM _ => [t];
 
 (*Dummy version: the only arguments are 0 and 1*)
-fun mk_coeff (0, t) = zero
+fun mk_coeff (0: IntInf.int, 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, mk_prod (sort Term.term_ord (dest_prod t)));
+fun dest_coeff t = (1 : IntInf.int, 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", [])