Use of IntInf.int instead of int in most numeric simprocs; avoids
authorpaulson
Mon May 16 10:29:15 2005 +0200 (2005-05-16)
changeset 15965f422f8283491
parent 15964 f2074e12d1d4
child 15966 73cf5ef8ed20
Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ
TODO
src/HOL/Integ/NatBin.thy
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Main.thy
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/arith_data.ML
src/HOL/ex/BinEx.thy
src/HOL/ex/svc_funcs.ML
src/HOL/hologic.ML
src/Provers/Arith/cancel_factor.ML
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Syntax/lexicon.ML
src/Pure/library.ML
src/ZF/Integ/int_arith.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/arith_data.ML
     1.1 --- a/TODO	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/TODO	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4  - a global "disprove" menu item both as an action and (if it can be done)
     1.5    as a setting (Stefan & Tjark)
     1.6  
     1.7 +- convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias)
     1.8 +
     1.9  - update or remove ex/MT (Larry)  
    1.10  
    1.11  - Include IsaPlanner? (Larry to co-ordinate)
    1.12 @@ -23,8 +25,6 @@
    1.13  
    1.14  - ball, bex and setsum congruence rules (Tobias & Stefan)
    1.15  
    1.16 -- use IntInf.int (Steven)
    1.17 -
    1.18  - html generation: somtimes lemma names and whole lemmas are missing.
    1.19    See http://afp.sourceforge.net/browser_info/current/HOL/HOL-Complex/Integration/SetsumThms.html
    1.20    (Markus?)
     2.1 --- a/src/HOL/Integ/NatBin.thy	Mon May 16 09:35:05 2005 +0200
     2.2 +++ b/src/HOL/Integ/NatBin.thy	Mon May 16 10:29:15 2005 +0200
     2.3 @@ -860,7 +860,7 @@
     2.4  ML {*
     2.5  fun number_of_codegen thy gr s b (Const ("Numeral.number_of",
     2.6        Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) =
     2.7 -        (SOME (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin)))
     2.8 +        (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin)))
     2.9          handle TERM _ => NONE)
    2.10    | number_of_codegen thy gr s b (Const ("Numeral.number_of",
    2.11        Type ("fun", [_, Type ("nat", [])])) $ bin) =
     3.1 --- a/src/HOL/Integ/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
     3.2 +++ b/src/HOL/Integ/cooper_dec.ML	Mon May 16 10:29:15 2005 +0200
     3.3 @@ -85,13 +85,14 @@
     3.4   
     3.5  fun mk_numeral 0 = Const("0",HOLogic.intT)
     3.6     |mk_numeral 1 = Const("1",HOLogic.intT)
     3.7 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
     3.8 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
     3.9   
    3.10  (*Transform an Term to an natural number*)	  
    3.11  	  
    3.12  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    3.13     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    3.14 -   |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
    3.15 +   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    3.16 +       IntInf.toInt (HOLogic.dest_binum n);
    3.17  (*Some terms often used for pattern matching*) 
    3.18   
    3.19  val zero = mk_numeral 0; 
    3.20 @@ -245,12 +246,13 @@
    3.21  (* ------------------------------------------------------------------------- *) 
    3.22  (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
    3.23   
    3.24 +(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
    3.25  fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
    3.26  fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
    3.27   
    3.28  fun formlcm x fm = case fm of 
    3.29      (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
    3.30 -    (is_arith_rel fm) andalso (x = y) then abs(dest_numeral c) else 1 
    3.31 +    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
    3.32    | ( Const ("Not", _) $p) => formlcm x p 
    3.33    | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
    3.34    | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
    3.35 @@ -281,7 +283,7 @@
    3.36  (* ------------------------------------------------------------------------- *) 
    3.37   
    3.38  fun unitycoeff x fm = 
    3.39 -  let val l = formlcm x fm 
    3.40 +  let val l = formlcm x fm
    3.41        val fm' = adjustcoeff x l fm in
    3.42        if l = 1 then fm' 
    3.43  	 else 
    3.44 @@ -453,7 +455,8 @@
    3.45  
    3.46  
    3.47  val operations = 
    3.48 -  [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    3.49 +  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
    3.50 +   ("op >=",Int.>=), 
    3.51     ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
    3.52   
    3.53  fun applyoperation (SOME f) (a,b) = f (a, b) 
    3.54 @@ -486,13 +489,14 @@
    3.55  fun evalc_atom at = case at of  
    3.56    (Const (p,_) $ s $ t) =>
    3.57     ( case assoc (operations,p) of 
    3.58 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    3.59 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
    3.60 +                else HOLogic.false_const)  
    3.61      handle _ => at) 
    3.62        | _ =>  at) 
    3.63        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    3.64    case assoc (operations,p) of 
    3.65 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    3.66 -    HOLogic.false_const else HOLogic.true_const)  
    3.67 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
    3.68 +               then HOLogic.false_const else HOLogic.true_const)  
    3.69      handle _ => at) 
    3.70        | _ =>  at) 
    3.71        | _ =>  at; 
    3.72 @@ -678,7 +682,8 @@
    3.73  (* Minusinfinity Version*) 
    3.74  fun coopermi vars1 fm = 
    3.75    case fm of 
    3.76 -   Const ("Ex",_) $ Abs(x0,T,p0) => let 
    3.77 +   Const ("Ex",_) $ Abs(x0,T,p0) => 
    3.78 +   let 
    3.79      val (xn,p1) = variant_abs (x0,T,p0) 
    3.80      val x = Free (xn,T)  
    3.81      val vars = (xn::vars1) 
     4.1 --- a/src/HOL/Integ/int_arith1.ML	Mon May 16 09:35:05 2005 +0200
     4.2 +++ b/src/HOL/Integ/int_arith1.ML	Mon May 16 10:29:15 2005 +0200
     4.3 @@ -149,8 +149,8 @@
     4.4  (*Order integers by absolute value and then by sign. The standard integer
     4.5    ordering is not well-founded.*)
     4.6  fun num_ord (i,j) =
     4.7 -      (case Int.compare (abs i, abs j) of
     4.8 -            EQUAL => Int.compare (Int.sign i, Int.sign j) 
     4.9 +      (case IntInf.compare (IntInf.abs i, IntInf.abs j) of
    4.10 +            EQUAL => Int.compare (IntInf.sign i, IntInf.sign j) 
    4.11            | ord => ord);
    4.12  
    4.13  (*This resembles Term.term_ord, but it puts binary numerals before other
    4.14 @@ -388,7 +388,7 @@
    4.15  
    4.16  structure CombineNumeralsData =
    4.17    struct
    4.18 -  val add               = op + : int*int -> int
    4.19 +  val add               = IntInf.+ 
    4.20    val mk_sum            = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
    4.21    val dest_sum          = dest_sum
    4.22    val mk_coeff          = mk_coeff
     5.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon May 16 09:35:05 2005 +0200
     5.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon May 16 10:29:15 2005 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4  fun dest_numeral (Const ("0", _)) = 0
     5.5    | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
     5.6    | dest_numeral (Const("Numeral.number_of", _) $ w) =
     5.7 -      (BasisLibrary.Int.max (0, HOLogic.dest_binum w)
     5.8 +      (IntInf.max (0, HOLogic.dest_binum w)
     5.9         handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
    5.10    | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
    5.11  
    5.12 @@ -245,7 +245,7 @@
    5.13  
    5.14  structure CombineNumeralsData =
    5.15    struct
    5.16 -  val add               = op + : int*int -> int
    5.17 +  val add               = IntInf.+
    5.18    val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
    5.19    val dest_sum          = restricted_dest_Sucs_sum
    5.20    val mk_coeff          = mk_coeff
     6.1 --- a/src/HOL/Main.thy	Mon May 16 09:35:05 2005 +0200
     6.2 +++ b/src/HOL/Main.thy	Mon May 16 10:29:15 2005 +0200
     6.3 @@ -32,11 +32,12 @@
     6.4  
     6.5  quickcheck_params [default_type = int]
     6.6  
     6.7 +(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
     6.8  ML {*
     6.9  fun wf_rec f x = f (wf_rec f) x;
    6.10  
    6.11  fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    6.12 -val term_of_int = HOLogic.mk_int;
    6.13 +val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    6.14  fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    6.15  
    6.16  val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
     7.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 09:35:05 2005 +0200
     7.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon May 16 10:29:15 2005 +0200
     7.3 @@ -85,13 +85,14 @@
     7.4   
     7.5  fun mk_numeral 0 = Const("0",HOLogic.intT)
     7.6     |mk_numeral 1 = Const("1",HOLogic.intT)
     7.7 -   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin n); 
     7.8 +   |mk_numeral n = (HOLogic.number_of_const HOLogic.intT) $ (HOLogic.mk_bin (IntInf.fromInt n)); 
     7.9   
    7.10  (*Transform an Term to an natural number*)	  
    7.11  	  
    7.12  fun dest_numeral (Const("0",Type ("IntDef.int", []))) = 0
    7.13     |dest_numeral (Const("1",Type ("IntDef.int", []))) = 1
    7.14 -   |dest_numeral (Const ("Numeral.number_of",_) $ n)= HOLogic.dest_binum n; 
    7.15 +   |dest_numeral (Const ("Numeral.number_of",_) $ n) = 
    7.16 +       IntInf.toInt (HOLogic.dest_binum n);
    7.17  (*Some terms often used for pattern matching*) 
    7.18   
    7.19  val zero = mk_numeral 0; 
    7.20 @@ -245,12 +246,13 @@
    7.21  (* ------------------------------------------------------------------------- *) 
    7.22  (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) 
    7.23   
    7.24 +(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*)
    7.25  fun gcd a b = if a=0 then b else gcd (b mod a) a ; 
    7.26  fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); 
    7.27   
    7.28  fun formlcm x fm = case fm of 
    7.29      (Const (p,_)$ _ $(Const ("op +", _)$(Const ("op *",_)$ c $ y ) $z ) ) =>  if 
    7.30 -    (is_arith_rel fm) andalso (x = y) then abs(dest_numeral c) else 1 
    7.31 +    (is_arith_rel fm) andalso (x = y) then  (abs(dest_numeral c)) else 1 
    7.32    | ( Const ("Not", _) $p) => formlcm x p 
    7.33    | ( Const ("op &",_) $ p $ q) => lcm_num (formlcm x p) (formlcm x q) 
    7.34    | ( Const ("op |",_) $ p $ q )=> lcm_num (formlcm x p) (formlcm x q) 
    7.35 @@ -281,7 +283,7 @@
    7.36  (* ------------------------------------------------------------------------- *) 
    7.37   
    7.38  fun unitycoeff x fm = 
    7.39 -  let val l = formlcm x fm 
    7.40 +  let val l = formlcm x fm
    7.41        val fm' = adjustcoeff x l fm in
    7.42        if l = 1 then fm' 
    7.43  	 else 
    7.44 @@ -453,7 +455,8 @@
    7.45  
    7.46  
    7.47  val operations = 
    7.48 -  [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    7.49 +  [("op =",op=), ("op <",Int.<), ("op >",Int.>), ("op <=",Int.<=) , 
    7.50 +   ("op >=",Int.>=), 
    7.51     ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
    7.52   
    7.53  fun applyoperation (SOME f) (a,b) = f (a, b) 
    7.54 @@ -486,13 +489,14 @@
    7.55  fun evalc_atom at = case at of  
    7.56    (Const (p,_) $ s $ t) =>
    7.57     ( case assoc (operations,p) of 
    7.58 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
    7.59 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const 
    7.60 +                else HOLogic.false_const)  
    7.61      handle _ => at) 
    7.62        | _ =>  at) 
    7.63        |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
    7.64    case assoc (operations,p) of 
    7.65 -    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
    7.66 -    HOLogic.false_const else HOLogic.true_const)  
    7.67 +    SOME f => ((if (f ((dest_numeral s),(dest_numeral t))) 
    7.68 +               then HOLogic.false_const else HOLogic.true_const)  
    7.69      handle _ => at) 
    7.70        | _ =>  at) 
    7.71        | _ =>  at; 
    7.72 @@ -678,7 +682,8 @@
    7.73  (* Minusinfinity Version*) 
    7.74  fun coopermi vars1 fm = 
    7.75    case fm of 
    7.76 -   Const ("Ex",_) $ Abs(x0,T,p0) => let 
    7.77 +   Const ("Ex",_) $ Abs(x0,T,p0) => 
    7.78 +   let 
    7.79      val (xn,p1) = variant_abs (x0,T,p0) 
    7.80      val x = Free (xn,T)  
    7.81      val vars = (xn::vars1) 
     8.1 --- a/src/HOL/Tools/meson.ML	Mon May 16 09:35:05 2005 +0200
     8.2 +++ b/src/HOL/Tools/meson.ML	Mon May 16 10:29:15 2005 +0200
     8.3 @@ -317,7 +317,8 @@
     8.4  fun make_nnf th = th |> simplify nnf_ss
     8.5                       |> check_no_bool |> make_nnf1
     8.6  
     8.7 -(*Pull existential quantifiers (Skolemization)*)
     8.8 +(*Pull existential quantifiers to front. This accomplishes Skolemization for
     8.9 +  clauses that arise from a subgoal.*)
    8.10  fun skolemize th =
    8.11    if not (has_consts ["Ex"] (prop_of th)) then th
    8.12    else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
    8.13 @@ -331,7 +332,7 @@
    8.14  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    8.15    The resulting clauses are HOL disjunctions.*)
    8.16  fun make_clauses ths =
    8.17 -   (  sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    8.18 +    (sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    8.19  
    8.20  
    8.21  (*Convert a list of clauses to (contrapositive) Horn clauses*)
     9.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon May 16 09:35:05 2005 +0200
     9.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon May 16 10:29:15 2005 +0200
     9.3 @@ -28,7 +28,7 @@
     9.4        (case rev rev_digs of
     9.5          ~1 :: bs => ("-", prefix_len (equal 1) bs)
     9.6        | bs => ("", prefix_len (equal 0) bs));
     9.7 -    val i = HOLogic.intinf_of rev_digs;
     9.8 +    val i = HOLogic.int_of rev_digs;
     9.9      val num = IntInf.toString (IntInf.abs i);
    9.10    in
    9.11      if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
    9.12 @@ -38,7 +38,7 @@
    9.13  (* translation of integer numeral tokens to and from bitstrings *)
    9.14  
    9.15  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    9.16 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin_from_intinf (valOf (IntInf.fromString str))))
    9.17 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin (valOf (IntInf.fromString str))))
    9.18    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    9.19  
    9.20  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    10.1 --- a/src/HOL/arith_data.ML	Mon May 16 09:35:05 2005 +0200
    10.2 +++ b/src/HOL/arith_data.ML	Mon May 16 10:29:15 2005 +0200
    10.3 @@ -265,27 +265,27 @@
    10.4  let
    10.5  fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
    10.6          Const("Numeral.number_of",_)$n
    10.7 -        => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
    10.8 +        => demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
    10.9        | Const("uminus",_)$(Const("Numeral.number_of",_)$n)
   10.10 -        => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
   10.11 +        => demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n))))
   10.12        | Const("Suc",_) $ _
   10.13          => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
   10.14        | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
   10.15        | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
   10.16            let val den = HOLogic.dest_binum dent
   10.17            in if den = 0 then raise Zero
   10.18 -             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_int den)))
   10.19 +             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den)))
   10.20            end
   10.21        | _ => atomult(mC,s,t,m)
   10.22        ) handle TERM _ => atomult(mC,s,t,m))
   10.23    | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) =
   10.24        (let val den = HOLogic.dest_binum dent
   10.25 -       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
   10.26 +       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end
   10.27         handle TERM _ => (SOME atom,m))
   10.28    | demult(Const("0",_),m) = (NONE, rat_of_int 0)
   10.29    | demult(Const("1",_),m) = (NONE, m)
   10.30    | demult(t as Const("Numeral.number_of",_)$n,m) =
   10.31 -      ((NONE,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
   10.32 +      ((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n)))
   10.33         handle TERM _ => (SOME t,m))
   10.34    | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
   10.35    | demult(t as Const f $ x, m) =
   10.36 @@ -316,7 +316,7 @@
   10.37           (NONE,m') => (p,ratadd(i,m'))
   10.38         | (SOME u,m') => add_atom(u,m',pi))
   10.39    | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
   10.40 -      ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
   10.41 +      ((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t))))
   10.42         handle TERM _ => add_atom all)
   10.43    | poly(all as Const f $ x, m, pi) =
   10.44        if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
   10.45 @@ -363,7 +363,8 @@
   10.46    let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
   10.47    in decomp2 (sg,discrete,inj_consts) end
   10.48  
   10.49 -fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n)
   10.50 +(*FIXME: remove the IntInf.fromInt when linear arithmetic is converted to IntInfs*)
   10.51 +fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin (IntInf.fromInt n))
   10.52  
   10.53  end;
   10.54  
    11.1 --- a/src/HOL/ex/BinEx.thy	Mon May 16 09:35:05 2005 +0200
    11.2 +++ b/src/HOL/ex/BinEx.thy	Mon May 16 10:29:15 2005 +0200
    11.3 @@ -186,6 +186,10 @@
    11.4  lemma "(1234567::int) \<le> 1234567"
    11.5    by simp
    11.6  
    11.7 +text{*No integer overflow!*}
    11.8 +lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
    11.9 +  by simp
   11.10 +
   11.11  
   11.12  text {* \medskip Quotient and Remainder *}
   11.13  
   11.14 @@ -205,7 +209,7 @@
   11.15  
   11.16  text {*
   11.17    A negative dividend\footnote{The definition agrees with mathematical
   11.18 -  convention but not with the hardware of most computers}
   11.19 +  convention and with ML, but not with the hardware of most computers}
   11.20  *}
   11.21  
   11.22  lemma "(-10::int) div 3 = -4"
    12.1 --- a/src/HOL/ex/svc_funcs.ML	Mon May 16 09:35:05 2005 +0200
    12.2 +++ b/src/HOL/ex/svc_funcs.ML	Mon May 16 10:29:15 2005 +0200
    12.3 @@ -27,14 +27,14 @@
    12.4     | UnInterp of string * expr list
    12.5     | FalseExpr 
    12.6     | TrueExpr
    12.7 -   | Int of int
    12.8 -   | Rat of int * int;
    12.9 +   | Int of IntInf.int
   12.10 +   | Rat of IntInf.int * IntInf.int;
   12.11  
   12.12   open BasisLibrary
   12.13  
   12.14   fun signedInt i = 
   12.15 -     if i < 0 then "-" ^ Int.toString (~i)
   12.16 -     else Int.toString i;
   12.17 +     if i < 0 then "-" ^ IntInf.toString (~i)
   12.18 +     else IntInf.toString i;
   12.19  	 
   12.20   fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
   12.21   
    13.1 --- a/src/HOL/hologic.ML	Mon May 16 09:35:05 2005 +0200
    13.2 +++ b/src/HOL/hologic.ML	Mon May 16 10:29:15 2005 +0200
    13.3 @@ -17,6 +17,7 @@
    13.4    val not_const: term
    13.5    val mk_setT: typ -> typ
    13.6    val dest_setT: typ -> typ
    13.7 +  val Trueprop: term
    13.8    val mk_Trueprop: term -> term
    13.9    val dest_Trueprop: term -> term
   13.10    val conj: term
   13.11 @@ -70,7 +71,7 @@
   13.12    val mk_nat: int -> term
   13.13    val dest_nat: term -> int
   13.14    val intT: typ
   13.15 -  val mk_int: int -> term
   13.16 +  val mk_int: IntInf.int -> term
   13.17    val realT: typ
   13.18    val bitT: typ
   13.19    val B0_const: term
   13.20 @@ -80,11 +81,9 @@
   13.21    val min_const: term
   13.22    val bit_const: term
   13.23    val number_of_const: typ -> term
   13.24 -  val int_of: int list -> int
   13.25 -  val intinf_of: int list -> IntInf.int
   13.26 -  val dest_binum: term -> int
   13.27 -  val mk_bin: int -> term
   13.28 -  val mk_bin_from_intinf: IntInf.int -> term
   13.29 +  val int_of: int list -> IntInf.int 
   13.30 +  val dest_binum: term -> IntInf.int
   13.31 +  val mk_bin: IntInf.int -> term
   13.32    val bin_of : term -> int list
   13.33    val mk_list: ('a -> term) -> typ -> 'a list -> term
   13.34    val dest_list: term -> term list
   13.35 @@ -311,12 +310,8 @@
   13.36  
   13.37  fun number_of_const T = Const ("Numeral.number_of", binT --> T);
   13.38  
   13.39 -
   13.40 -fun int_of [] = 0
   13.41 -  | int_of (b :: bs) = b + 2 * int_of bs;
   13.42 -
   13.43 -fun intinf_of [] = IntInf.fromInt 0
   13.44 -  | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
   13.45 +fun int_of [] = 0 
   13.46 +  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
   13.47  
   13.48  (*When called from a print translation, the Numeral qualifier will probably have
   13.49    been removed from Bit, bin.B0, etc.*)
   13.50 @@ -338,22 +333,18 @@
   13.51    | mk_bit 1 = B1_const
   13.52    | mk_bit _ = sys_error "mk_bit";
   13.53  
   13.54 -fun mk_bin_from_intinf  n =
   13.55 +fun mk_bin  n =
   13.56      let
   13.57 -	val zero = IntInf.fromInt 0
   13.58 -	val minus_one = IntInf.fromInt ~1
   13.59 -	val two = IntInf.fromInt 2
   13.60 -
   13.61 -	fun mk_bit n = if n = zero then B0_const else B1_const
   13.62 +	fun mk_bit n = if n = 0 then B0_const else B1_const
   13.63  								 
   13.64  	fun bin_of n = 
   13.65 -	    if n = zero then pls_const
   13.66 -	    else if n = minus_one then min_const
   13.67 +	    if n = 0 then pls_const
   13.68 +	    else if n = ~1 then min_const
   13.69  	    else 
   13.70  		let 
   13.71 -		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!*)
   13.72 -	            val q = IntInf.div (n, two)
   13.73 -		    val r = IntInf.mod (n, two)
   13.74 +		    (*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!*)
   13.75 +	            val q = IntInf.div (n, 2)
   13.76 +		    val r = IntInf.mod (n, 2)
   13.77  		in
   13.78  		    bit_const $ bin_of q $ mk_bit r
   13.79  		end
   13.80 @@ -361,8 +352,6 @@
   13.81  	bin_of n
   13.82      end
   13.83  
   13.84 -val mk_bin = mk_bin_from_intinf o IntInf.fromInt;
   13.85 -
   13.86  
   13.87  (* int *)
   13.88  
    14.1 --- a/src/Provers/Arith/cancel_factor.ML	Mon May 16 09:35:05 2005 +0200
    14.2 +++ b/src/Provers/Arith/cancel_factor.ML	Mon May 16 10:29:15 2005 +0200
    14.3 @@ -15,7 +15,7 @@
    14.4    (*rules*)
    14.5    val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
    14.6    val norm_tac: tactic			(*AC0 etc.*)
    14.7 -  val multiply_tac: int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
    14.8 +  val multiply_tac: IntInf.int -> tactic	(*apply a ~~ b  ==  k * a ~~ k * b  (for k > 0)*)
    14.9  end;
   14.10  
   14.11  signature CANCEL_FACTOR =
    15.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Mon May 16 09:35:05 2005 +0200
    15.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Mon May 16 10:29:15 2005 +0200
    15.3 @@ -22,8 +22,8 @@
    15.4    (*abstract syntax*)
    15.5    val mk_bal: term * term -> term
    15.6    val dest_bal: term -> term * term
    15.7 -  val mk_coeff: int * term -> term
    15.8 -  val dest_coeff: term -> int * term
    15.9 +  val mk_coeff: IntInf.int * term -> term
   15.10 +  val dest_coeff: term -> IntInf.int * term
   15.11    (*rules*)
   15.12    val cancel: thm
   15.13    val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
   15.14 @@ -45,11 +45,6 @@
   15.15  =
   15.16  struct
   15.17  
   15.18 -
   15.19 -(* greatest common divisor *)
   15.20 -fun gcd (0, n) = abs n
   15.21 -  | gcd (m, n) = gcd (n mod m, m);
   15.22 -
   15.23  (*the simplification procedure*)
   15.24  fun proc sg ss t =
   15.25    let
   15.26 @@ -61,7 +56,7 @@
   15.27        and (m2, t2') = Data.dest_coeff t2
   15.28        val d = (*if both are negative, also divide through by ~1*)
   15.29            if (m1<0 andalso m2<=0) orelse
   15.30 -             (m1<=0 andalso m2<0) then ~ (gcd(m1,m2)) else gcd(m1,m2)
   15.31 +             (m1<=0 andalso m2<0) then ~ (abs(gcd(m1,m2))) else abs (gcd(m1,m2))
   15.32        val _ = if d=1 then   (*trivial, so do nothing*)
   15.33  		      raise TERM("cancel_numeral_factor", []) 
   15.34                else ()
    16.1 --- a/src/Provers/Arith/cancel_numerals.ML	Mon May 16 09:35:05 2005 +0200
    16.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Mon May 16 10:29:15 2005 +0200
    16.3 @@ -29,9 +29,9 @@
    16.4    val dest_sum: term -> term list
    16.5    val mk_bal: term * term -> term
    16.6    val dest_bal: term -> term * term
    16.7 -  val mk_coeff: int * term -> term
    16.8 -  val dest_coeff: term -> int * term
    16.9 -  val find_first_coeff: term -> term list -> int * term list
   16.10 +  val mk_coeff: IntInf.int * term -> term
   16.11 +  val dest_coeff: term -> IntInf.int * term
   16.12 +  val find_first_coeff: term -> term list -> IntInf.int * term list
   16.13    (*rules*)
   16.14    val bal_add1: thm
   16.15    val bal_add2: thm
    17.1 --- a/src/Provers/Arith/combine_numerals.ML	Mon May 16 09:35:05 2005 +0200
    17.2 +++ b/src/Provers/Arith/combine_numerals.ML	Mon May 16 10:29:15 2005 +0200
    17.3 @@ -19,11 +19,11 @@
    17.4  signature COMBINE_NUMERALS_DATA =
    17.5  sig
    17.6    (*abstract syntax*)
    17.7 -  val add: int * int -> int          (*addition (or multiplication) *)
    17.8 +  val add: IntInf.int * IntInf.int -> IntInf.int     (*addition (or multiplication) *)
    17.9    val mk_sum: typ -> term list -> term
   17.10    val dest_sum: term -> term list
   17.11 -  val mk_coeff: int * term -> term
   17.12 -  val dest_coeff: term -> int * term
   17.13 +  val mk_coeff: IntInf.int * term -> term
   17.14 +  val dest_coeff: term -> IntInf.int * term
   17.15    (*rules*)
   17.16    val left_distrib: thm
   17.17    (*proof tools*)
    18.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 09:35:05 2005 +0200
    18.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 16 10:29:15 2005 +0200
    18.3 @@ -15,6 +15,8 @@
    18.4  
    18.5  Only take premises and conclusions into account that are already (negated)
    18.6  (in)equations. lin_arith_prover tries to prove or disprove the term.
    18.7 +
    18.8 +FIXME: convert to IntInf.int throughout. 
    18.9  *)
   18.10  
   18.11  (* Debugging: set Fast_Arith.trace *)
   18.12 @@ -189,15 +191,15 @@
   18.13  val ratrelmax = foldr1 ratrelmax2;
   18.14  
   18.15  fun ratroundup r = let val (p,q) = rep_rat r
   18.16 -                   in if q=1 then r else rat_of_int((p div q) + 1) end
   18.17 +                   in if q=1 then r else rat_of_intinf((p div q) + 1) end
   18.18  
   18.19  fun ratrounddown r = let val (p,q) = rep_rat r
   18.20 -                     in if q=1 then r else rat_of_int((p div q) - 1) end
   18.21 +                     in if q=1 then r else rat_of_intinf((p div q) - 1) end
   18.22  
   18.23  fun ratexact up (r,exact) =
   18.24    if exact then r else
   18.25    let val (p,q) = rep_rat r
   18.26 -      val nth = ratinv(rat_of_int q)
   18.27 +      val nth = ratinv(rat_of_intinf q)
   18.28    in ratadd(r,if up then nth else ratneg nth) end;
   18.29  
   18.30  fun ratmiddle(r,s) = ratmul(ratadd(r,s),ratinv(rat_of_int 2));
   18.31 @@ -299,7 +301,7 @@
   18.32  
   18.33  fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
   18.34    let val c1 = el v l1 and c2 = el v l2
   18.35 -      val m = lcm(abs c1,abs c2)
   18.36 +      val m = IntInf.toInt (lcm(IntInf.fromInt (abs c1), IntInf.fromInt(abs c2)))
   18.37        val m1 = m div (abs c1) and m2 = m div (abs c2)
   18.38        val (n1,n2) =
   18.39          if (c1 >= 0) = (c2 >= 0)
   18.40 @@ -497,12 +499,15 @@
   18.41  
   18.42  fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i;
   18.43  
   18.44 -fun lcms is = Library.foldl lcm (1,is);
   18.45 +fun lcms_intinf is = Library.foldl lcm (1, is);
   18.46 +fun lcms is = IntInf.toInt (lcms_intinf (map IntInf.fromInt is));
   18.47  
   18.48  fun integ(rlhs,r,rel,rrhs,s,d) =
   18.49 -let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s
   18.50 -    val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs))
   18.51 -    fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end
   18.52 +let val (rn,rd) = pairself IntInf.toInt (rep_rat r) and (sn,sd) = pairself IntInf.toInt (rep_rat s)
   18.53 +    val m = IntInf.toInt (lcms_intinf(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)))
   18.54 +    fun mult(t,r) = 
   18.55 +        let val (i,j) =  pairself IntInf.toInt (rep_rat r) 
   18.56 +        in (t,i * (m div j)) end
   18.57  in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
   18.58  
   18.59  fun mklineq n atoms =
   18.60 @@ -533,9 +538,9 @@
   18.61  
   18.62  fun print_atom((a,d),r) =
   18.63    let val (p,q) = rep_rat r
   18.64 -      val s = if d then string_of_int p else
   18.65 +      val s = if d then IntInf.toString p else
   18.66                if p = 0 then "0"
   18.67 -              else string_of_int p ^ "/" ^ string_of_int q
   18.68 +              else IntInf.toString p ^ "/" ^ IntInf.toString q
   18.69    in a ^ " = " ^ s end;
   18.70  
   18.71  fun print_ex sds =
    19.1 --- a/src/Pure/Syntax/lexicon.ML	Mon May 16 09:35:05 2005 +0200
    19.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon May 16 10:29:15 2005 +0200
    19.3 @@ -30,7 +30,7 @@
    19.4    val skolem: string -> string
    19.5    val dest_skolem: string -> string
    19.6    val read_nat: string -> int option
    19.7 -  val read_xnum: string -> int
    19.8 +  val read_xnum: string -> IntInf.int
    19.9    val read_idents: string -> string list
   19.10  end;
   19.11  
   19.12 @@ -365,6 +365,16 @@
   19.13  
   19.14  (* read_xnum *)
   19.15  
   19.16 +fun read_intinf cs : IntInf.int * string list =
   19.17 +  let val zero = ord"0"
   19.18 +      val limit = zero+10
   19.19 +      fun scan (num,[]) = (num,[])
   19.20 +        | scan (num, c::cs) =
   19.21 +              if  zero <= ord c  andalso  ord c < limit
   19.22 +              then scan(10*num + IntInf.fromInt (ord c - zero), cs)
   19.23 +              else (num, c::cs)
   19.24 +  in  scan(0,cs)  end;
   19.25 +
   19.26  fun read_xnum str =
   19.27    let
   19.28      val (sign, digs) =
   19.29 @@ -373,7 +383,7 @@
   19.30        | "#" :: cs => (1, cs)
   19.31        | "-" :: cs => (~1, cs)
   19.32        | cs => (1, cs));
   19.33 -  in sign * #1 (Library.read_int digs) end;
   19.34 +  in sign * #1 (read_intinf digs) end;
   19.35  
   19.36  
   19.37  (* read_ident(s) *)
    20.1 --- a/src/Pure/library.ML	Mon May 16 09:35:05 2005 +0200
    20.2 +++ b/src/Pure/library.ML	Mon May 16 10:29:15 2005 +0200
    20.3 @@ -117,8 +117,8 @@
    20.4    val suffixes1: 'a list -> 'a list list
    20.5  
    20.6    (*integers*)
    20.7 -  val gcd: int * int -> int
    20.8 -  val lcm: int * int -> int
    20.9 +  val gcd: IntInf.int * IntInf.int -> IntInf.int
   20.10 +  val lcm: IntInf.int * IntInf.int -> IntInf.int
   20.11    val inc: int ref -> int
   20.12    val dec: int ref -> int
   20.13    val upto: int * int -> int list
   20.14 @@ -136,13 +136,14 @@
   20.15    (*rational numbers*)
   20.16    type rat
   20.17    exception RAT of string
   20.18 -  val rep_rat: rat -> int * int
   20.19 +  val rep_rat: rat -> IntInf.int * IntInf.int
   20.20    val ratadd: rat * rat -> rat
   20.21    val ratmul: rat * rat -> rat
   20.22    val ratinv: rat -> rat
   20.23 -  val int_ratdiv: int * int -> rat
   20.24 +  val int_ratdiv: IntInf.int * IntInf.int -> rat
   20.25    val ratneg: rat -> rat
   20.26    val rat_of_int: int -> rat
   20.27 +  val rat_of_intinf: IntInf.int -> rat
   20.28  
   20.29    (*strings*)
   20.30    val nth_elem_string: int * string -> string
   20.31 @@ -665,7 +666,7 @@
   20.32  (** integers **)
   20.33  
   20.34  fun gcd(x,y) =
   20.35 -  let fun gxd x y =
   20.36 +  let fun gxd x y : IntInf.int =
   20.37      if y = 0 then x else gxd y (x mod y)
   20.38    in if x < y then gxd y x else gxd x y end;
   20.39  
   20.40 @@ -1186,7 +1187,7 @@
   20.41  
   20.42  (** rational numbers **)
   20.43  
   20.44 -datatype rat = Rat of bool * int * int
   20.45 +datatype rat = Rat of bool * IntInf.int * IntInf.int
   20.46  
   20.47  exception RAT of string;
   20.48  
   20.49 @@ -1212,7 +1213,9 @@
   20.50  
   20.51  fun ratneg(Rat(b,p,q)) = Rat(not b,p,q);
   20.52  
   20.53 -fun rat_of_int i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
   20.54 +fun rat_of_intinf i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
   20.55 +
   20.56 +fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
   20.57  
   20.58  
   20.59  (** misc **)
    21.1 --- a/src/ZF/Integ/int_arith.ML	Mon May 16 09:35:05 2005 +0200
    21.2 +++ b/src/ZF/Integ/int_arith.ML	Mon May 16 10:29:15 2005 +0200
    21.3 @@ -291,7 +291,7 @@
    21.4  
    21.5  structure CombineNumeralsData =
    21.6    struct
    21.7 -  val add               = op + : int*int -> int
    21.8 +  val add               = IntInf.+ 
    21.9    val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   21.10    val dest_sum          = dest_sum
   21.11    val mk_coeff          = mk_coeff
   21.12 @@ -327,7 +327,7 @@
   21.13  
   21.14  structure CombineNumeralsProdData =
   21.15    struct
   21.16 -  val add               = op * : int*int -> int
   21.17 +  val add               = IntInf.*
   21.18    val mk_sum            = (fn T:typ => mk_prod)
   21.19    val dest_sum          = dest_prod
   21.20    fun mk_coeff(k,t) = if t=one then mk_numeral k
    22.1 --- a/src/ZF/Tools/numeral_syntax.ML	Mon May 16 09:35:05 2005 +0200
    22.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Mon May 16 10:29:15 2005 +0200
    22.3 @@ -8,8 +8,8 @@
    22.4  
    22.5  signature NUMERAL_SYNTAX =
    22.6  sig
    22.7 -  val dest_bin : term -> int
    22.8 -  val mk_bin   : int -> term
    22.9 +  val dest_bin : term -> IntInf.int
   22.10 +  val mk_bin   : IntInf.int -> term
   22.11    val int_tr   : term list -> term
   22.12    val int_tr'  : bool -> typ -> term list -> term
   22.13    val setup    : (theory -> theory) list
   22.14 @@ -23,7 +23,7 @@
   22.15  val zero = Const("0", iT);
   22.16  val succ = Const("succ", iT --> iT);
   22.17  
   22.18 -fun mk_bit 0 = zero
   22.19 +fun mk_bit (0: IntInf.int) = zero
   22.20    | mk_bit 1 = succ$zero
   22.21    | mk_bit _ = sys_error "mk_bit";
   22.22  
   22.23 @@ -42,16 +42,16 @@
   22.24  and min_const = Const ("Bin.bin.Min", iT)
   22.25  and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
   22.26  
   22.27 -fun mk_bin i =
   22.28 -  let fun bin_of 0  = []
   22.29 -	| bin_of ~1 = [~1]
   22.30 -	| bin_of n  = (n mod 2) :: bin_of (n div 2);
   22.31 +fun mk_bin (i: IntInf.int) =
   22.32 +  let fun bin_of_int 0  = []
   22.33 +  	    | bin_of_int ~1 = [~1]
   22.34 +    	| bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
   22.35  
   22.36        fun term_of []   = pls_const
   22.37 -	| term_of [~1] = min_const
   22.38 -	| term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
   22.39 +	    | term_of [~1] = min_const
   22.40 +	    | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
   22.41    in
   22.42 -    term_of (bin_of i)
   22.43 +    term_of (bin_of_int i)
   22.44    end;
   22.45  
   22.46  (*we consider all "spellings", since they could vary depending on the caller*)
   22.47 @@ -66,13 +66,15 @@
   22.48    | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   22.49    | bin_of _ = raise Match;
   22.50  
   22.51 -fun integ_of [] = 0
   22.52 -  | integ_of (b :: bs) = b + 2 * integ_of bs;
   22.53 +(*Convert a list of bits to an integer*)
   22.54 +fun integ_of [] = 0 : IntInf.int
   22.55 +  | integ_of (b :: bs) = (IntInf.fromInt b) + 2 * integ_of bs;
   22.56  
   22.57  val dest_bin = integ_of o bin_of;
   22.58  
   22.59 -(*leading 0s and (for negative numbers) -1s cause complications,
   22.60 -  though they should never arise in normal use.*)
   22.61 +(*leading 0s and (for negative numbers) -1s cause complications, though they 
   22.62 +  should never arise in normal use. The formalization used in HOL prevents 
   22.63 +  them altogether.*)
   22.64  fun show_int t =
   22.65    let
   22.66      val rev_digs = bin_of t;
   22.67 @@ -80,7 +82,7 @@
   22.68  	(case rev rev_digs of
   22.69  	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
   22.70  	   | bs =>       ("",  prefix_len (equal 0) bs));
   22.71 -    val num = string_of_int (abs (integ_of rev_digs));
   22.72 +    val num = IntInf.toString (abs (integ_of rev_digs));
   22.73    in
   22.74      "#" ^ sign ^ implode (replicate zs "0") ^ num
   22.75    end;
    23.1 --- a/src/ZF/arith_data.ML	Mon May 16 09:35:05 2005 +0200
    23.2 +++ b/src/ZF/arith_data.ML	Mon May 16 10:29:15 2005 +0200
    23.3 @@ -101,13 +101,13 @@
    23.4        handle TERM _ => [t];
    23.5  
    23.6  (*Dummy version: the only arguments are 0 and 1*)
    23.7 -fun mk_coeff (0, t) = zero
    23.8 +fun mk_coeff (0: IntInf.int, t) = zero
    23.9    | mk_coeff (1, t) = t
   23.10    | mk_coeff _       = raise TERM("mk_coeff", []);
   23.11  
   23.12  (*Dummy version: the "coefficient" is always 1.
   23.13    In the result, the factors are sorted terms*)
   23.14 -fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
   23.15 +fun dest_coeff t = (1 : IntInf.int, mk_prod (sort Term.term_ord (dest_prod t)));
   23.16  
   23.17  (*Find first coefficient-term THAT MATCHES u*)
   23.18  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])