# HG changeset patch
# User wenzelm
# Date 1181341726 -7200
# Node ID 06f108974fa180b3da14fbcbd67f8c8a5e6ba009
# Parent  25f28f9c28a390e672a135696589f452ebd66f00
simplified type integer;

diff -r 25f28f9c28a3 -r 06f108974fa1 src/HOL/Matrix/cplex/fspmlp.ML
--- a/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -207,8 +207,8 @@
 
         fun test_1 (lower, upper) =
             if lower = upper then
-                (if Float.eq (lower, (Integer.int ~1, Integer.zero)) then ~1
-                 else if Float.eq (lower, (Integer.int 1, Integer.zero)) then 1
+                (if Float.eq (lower, (~1, 0)) then ~1
+                 else if Float.eq (lower, (1, 0)) then 1
                  else 0)
             else 0
 
diff -r 25f28f9c28a3 -r 06f108974fa1 src/HOL/Real/float_arith.ML
--- a/src/HOL/Real/float_arith.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/HOL/Real/float_arith.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -85,11 +85,8 @@
 exception Floating_point of string;
 
 val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
-val exp5 = Integer.pow (Integer.int 5);
-val exp10 = Integer.pow (Integer.int 10);
-
-fun intle a b = not (Integer.cmp (a, b) = GREATER);
-fun intless a b = Integer.cmp (a, b) = LESS;
+val exp5 = Integer.pow 5;
+val exp10 = Integer.pow 10;
 
 fun find_most_significant q r =
   let
@@ -98,26 +95,26 @@
         SOME r => r
         | NONE => raise (Floating_point "int2real")
     fun subtract (q, r) (q', r') =
-      if intle r r' then
-        (Integer.sub q (Integer.mult q' (exp10 (Integer.sub r' r))), r)
+      if r <=% r' then
+        (q - q' * exp10 (r' - r), r)
       else
-        (Integer.sub (Integer.mult q (exp10 (Integer.sub r r'))) q', r')
+        (q * exp10 (r - r') - q', r')
     fun bin2dec d =
-      if intle Integer.zero d then
-        (Integer.exp d, Integer.zero)
+      if 0 <=% d then
+        (Integer.exp d, 0)
       else
-        (exp5 (Integer.neg d), d)
+        (exp5 (~ d), d)
 
     val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10))
-    val L1 = Integer.inc L
+    val L1 = L + 1
 
     val (q1, r1) = subtract (q, r) (bin2dec L1) 
   in
-    if intle Integer.zero q1 then
+    if 0 <=% q1 then
       let
-        val (q2, r2) = subtract (q, r) (bin2dec (Integer.inc L1))
+        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
       in
-        if intle Integer.zero q2 then
+        if 0 <=% q2 then
           raise (Floating_point "find_most_significant")
         else
           (L1, (q1, r1))
@@ -126,7 +123,7 @@
       let
         val (q0, r0) = subtract (q, r) (bin2dec L)
       in
-        if intle Integer.zero q0 then
+        if 0 <=% q0 then
           (L, (q0, r0))
         else
           raise (Floating_point "find_most_significant")
@@ -136,13 +133,13 @@
 fun approx_dec_by_bin n (q,r) =
   let
     fun addseq acc d' [] = acc
-      | addseq acc d' (d::ds) = addseq (Integer.add acc (Integer.exp (Integer.sub d d'))) d' ds
+      | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds
 
-    fun seq2bin [] = (Integer.zero, Integer.zero)
-      | seq2bin (d::ds) = (Integer.inc (addseq Integer.zero d ds), d)
+    fun seq2bin [] = (0, 0)
+      | seq2bin (d::ds) = (addseq 0 d ds +% 1, d)
 
     fun approx d_seq d0 precision (q,r) =
-      if q = Integer.zero then
+      if q = 0 then
         let val x = seq2bin d_seq in
           (x, x)
         end
@@ -150,13 +147,11 @@
         let
           val (d, (q', r')) = find_most_significant q r
         in
-          if intless precision (Integer.sub d0 d) then
+          if precision <% d0 - d then
             let
-              val d' = Integer.sub d0 precision
+              val d' = d0 - precision
               val x1 = seq2bin (d_seq)
-              val x2 = (Integer.inc
-                (Integer.mult (fst x1)
-                (Integer.exp (Integer.sub (snd x1) d'))),  d') (* = seq2bin (d'::d_seq) *)
+              val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
             in
               (x1, x2)
             end
@@ -165,45 +160,45 @@
         end
 
     fun approx_start precision (q, r) =
-      if q = Integer.zero then
-        ((Integer.zero, Integer.zero), (Integer.zero, Integer.zero))
+      if q =% 0 then
+        ((0, 0), (0, 0))
       else
         let
           val (d, (q', r')) = find_most_significant q r
         in
-          if intle precision Integer.zero then
+          if precision <=% 0 then
             let
               val x1 = seq2bin [d]
             in
-              if q' = Integer.zero then
+              if q' = 0 then
                 (x1, x1)
               else
-                (x1, seq2bin [Integer.inc d])
+                (x1, seq2bin [d +% 1])
             end
           else
             approx [d] d precision (q', r')
         end
   in
-    if intle Integer.zero q then
+    if 0 <=% q then
       approx_start n (q,r)
     else
       let
-        val ((a1,b1), (a2, b2)) = approx_start n (Integer.neg q, r)
+        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
       in
-        ((Integer.neg a2, b2), (Integer.neg a1, b1))
+        ((~ a2, b2), (~ a1, b1))
       end
   end
 
 fun approx_decstr_by_bin n decstr =
   let
-    fun str2int s = the_default Integer.zero (Integer.int_of_string s);
+    fun str2int s = the_default 0 (Integer.int_of_string s);
     fun signint p x = if p then x else Integer.neg 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 q = signint p (Integer.add (Integer.mult (str2int d1) (exp10 s)) (str2int d2))
-    val r = Integer.sub (signint ep (str2int e)) s
+    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)
   end
@@ -213,7 +208,7 @@
 
 fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
       pairself (snd o HOLogic.dest_number) (a, b)
-  | dest_float t = ((snd o HOLogic.dest_number) t, Integer.zero);
+  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
 
 fun approx_float prec f value =
   let
diff -r 25f28f9c28a3 -r 06f108974fa1 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/HOL/hologic.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -295,17 +295,14 @@
 
 val Suc_zero = mk_Suc zero;
 
-fun mk_nat n =
+fun mk_nat (n: integer) =
   let
     fun mk 0 = zero
-      | mk n = mk_Suc (mk (n -% 1));
-  in if n < 0
-    then error "mk_nat: negative numeral"
-    else mk n
-  end;
+      | mk n = mk_Suc (mk (n - 1));
+  in if n < 0 then raise TERM ("mk_nat: negative numeral", []) else mk n end;
 
-fun dest_nat (Const ("HOL.zero_class.zero", _)) = Integer.zero
-  | dest_nat (Const ("Suc", _) $ t) = Integer.inc (dest_nat t)
+fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer)
+  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   | dest_nat t = raise TERM ("dest_nat", [t]);
 
 val class_size = "Nat.size";
@@ -346,7 +343,7 @@
 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)
+      2 * dest_numeral bs + Integer.int (dest_bit b)
   | dest_numeral t = raise TERM ("dest_numeral", [t]);
 
 fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
diff -r 25f28f9c28a3 -r 06f108974fa1 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -499,9 +499,9 @@
 end;
 
 fun coeff poly atom =
-  AList.lookup (op =) poly atom |> the_default Integer.zero;
+  AList.lookup (op =) poly atom |> the_default (0: integer);
 
-fun lcms ks = fold Integer.lcm ks Integer.one;
+fun lcms ks = fold Integer.lcm ks 1;
 
 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
diff -r 25f28f9c28a3 -r 06f108974fa1 src/Tools/float.ML
--- a/src/Tools/float.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/Tools/float.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -27,7 +27,7 @@
 
 type float = integer * integer;
 
-val zero = (Integer.zero, Integer.zero);
+val zero: float = (0, 0);
 
 fun add (a1, b1) (a2, b2) =
   if Integer.cmp (b1, b2) = LESS then
@@ -54,7 +54,7 @@
 fun min r s = case cmp (r, s) of LESS => r | _ => s;
 fun max r s = case cmp (r, s) of LESS => s | _ => r;
 
-fun positive_part (a, b) = (Integer.max Integer.zero a, b);
-fun negative_part (a, b) = (Integer.min Integer.zero a, b);
+fun positive_part (a, b) = (Integer.max 0 a, b);
+fun negative_part (a, b) = (Integer.min 0 a, b);
 
 end;
diff -r 25f28f9c28a3 -r 06f108974fa1 src/Tools/rat.ML
--- a/src/Tools/rat.ML	Fri Jun 08 18:13:58 2007 +0200
+++ b/src/Tools/rat.ML	Sat Jun 09 00:28:46 2007 +0200
@@ -7,7 +7,7 @@
 
 signature RAT =
 sig
-  type rat
+  eqtype rat
   exception DIVZERO
   val zero: rat
   val one: rat
@@ -36,37 +36,37 @@
 
 exception DIVZERO;
 
-val zero = Rat (true, Integer.zero, Integer.one);
-val one = Rat (true, Integer.one, Integer.one);
-val two = Rat (true, Integer.two, Integer.one);
+val zero = Rat (true, 0, 1);
+val one = Rat (true, 1, 1);
+val two = Rat (true, 2, 1);
 
 fun rat_of_int i =
   let
     val (a, p) = Integer.signabs i
-  in Rat (a, p, Integer.one) end;
+  in Rat (a, p, 1) end;
 
 fun norm (a, p, q) =
-  if Integer.cmp_zero p = EQUAL then Rat (true, Integer.zero, Integer.one)
+  if p = 0 then Rat (true, 0, 1)
   else
     let
       val (b, absp) = Integer.signabs p;
       val m = Integer.gcd absp q;
-    in Rat (a = b, Integer.div absp m, Integer.div q m) end;
+    in Rat (a = b, absp div m, q div m) end;
 
 fun common (p1, q1, p2, q2) =
   let
     val q' = Integer.lcm q1 q2;
-  in (p1 *% (Integer.div q' q1), p2 *% (Integer.div q' q2), q') end
+  in (p1 * (q' div q1), p2 * (q' div q2), q') end
 
 fun rat_of_quotient (p, q) =
   let
     val (a, absq) = Integer.signabs q;
   in
-    if Integer.cmp_zero absq = EQUAL then raise DIVZERO
+    if absq = 0 then raise DIVZERO
     else norm (a, p, absq)
   end;
 
-fun quotient_of_rat (Rat (a, p, q)) = (if a then p else Integer.neg p, q);
+fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~ p, q);
 
 fun string_of_rat r =
   let
@@ -75,7 +75,7 @@
 
 fun eq (Rat (false, _, _), Rat (true, _, _)) = false
   | eq (Rat (true, _, _), Rat (false, _, _)) = false
-  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 =% p2 andalso q1 =% q2;
+  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2;
 
 fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
   | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
@@ -93,48 +93,48 @@
 fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
   let
     val (r1, r2, den) = common (p1, q1, p2, q2);
-    val num = (if a1 then r1 else Integer.neg r1)
-      +% (if a2 then r2 else Integer.neg r2);
+    val num = (if a1 then r1 else ~ r1)
+      + (if a2 then r2 else ~ r2);
   in norm (true, num, den) end;
 
 fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
-  norm (a1 = a2, p1 *% p2, q1 *% q2);
+  norm (a1 = a2, p1 * p2, q1 * q2);
 
 fun neg (r as Rat (b, p, q)) =
-  if Integer.cmp_zero p = EQUAL then r
+  if p = 0 then r
   else Rat (not b, p, q);
 
 fun inv (Rat (a, p, q)) =
-  if Integer.cmp_zero q = EQUAL then raise DIVZERO
+  if q = 0 then raise DIVZERO
   else Rat (a, q, p);
 
 fun roundup (r as Rat (a, p, q)) =
-  if q = Integer.one then r
+  if q = 1 then r
   else
     let
-      fun round true q = Rat (true, Integer.inc q, Integer.one)
+      fun round true q = Rat (true, q + 1, 1)
         | round false q =
-            Rat (Integer.cmp_zero q = EQUAL, Integer.int 0, Integer.int 1);
-    in round a (Integer.div p q) end;
+            Rat (q = 0, 0, 1);
+    in round a (p div q) end;
 
 fun rounddown (r as Rat (a, p, q)) =
-  if q = Integer.one then r
+  if q = 1 then r
   else
     let
-      fun round true q = Rat (true, q, Integer.one)
-        | round false q = Rat (false, Integer.inc q, Integer.one)
-    in round a (Integer.div p q) end;
+      fun round true q = Rat (true, q, 1)
+        | round false q = Rat (false, q + 1, 1)
+    in round a (p div q) end;
 
 end;
 
 infix 7 */ //;
-infix 6 +/ -/; 
+infix 6 +/ -/;
 infix 4 =/ </ <=/ >/ >=/ <>/;
 
 fun a +/ b = Rat.add a b;
 fun a -/ b = a +/ Rat.neg b;
 fun a */ b = Rat.mult a b;
-fun a // b = a */ Rat.inv b; 
+fun a // b = a */ Rat.inv b;
 fun a =/ b = Rat.eq (a, b);
 fun a </ b = Rat.lt a b;
 fun a <=/ b = Rat.le a b;