tuned arithmetic modules

--- a/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -125,13 +125,13 @@
         fun calc_sure_bound_from_sources g (key as (_, btype)) =
             let
                 fun mult_upper x (lower, upper) =
-                    if Float.cmp_zero x = LESS then
+                    if Float.sign x = LESS then
                         Float.mult x lower
                     else
                         Float.mult x upper
 
                 fun mult_lower x (lower, upper) =
-                    if Float.cmp_zero x = LESS then
+                    if Float.sign x = LESS then
                         Float.mult x upper
                     else
                         Float.mult x lower
@@ -240,7 +240,7 @@
                                                             UPPER => (Float.neg src_upper, Float.neg src_lower)
                                                           | LOWER => src_value
                                         in
-                                            if Float.cmp_zero src_lower = LESS then
+                                            if Float.sign src_lower = LESS then
                                                 add_edge g (src_index, UPPER) dest_key row_index coeff
                                             else
                                                 add_edge g (src_index, LOWER) dest_key row_index coeff

--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -13,7 +13,7 @@
 struct
 open Conv;
 open Normalizer;
-structure Integertab = TableFun(type key = integer val ord = Integer.cmp);
+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);
 

--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -185,13 +185,13 @@
 *)
 
 fun ratrelmin2 (x as (r, ler), y as (s, les)) =
-  case Rat.cmp (r, s)
+  case Rat.ord (r, s)
    of EQUAL => (r, (not ler) andalso (not les))
     | LESS => x
     | GREATER => y;
 
 fun ratrelmax2 (x as (r, ler), y as (s, les)) =
-  case Rat.cmp (r, s)
+  case Rat.ord (r, s)
    of EQUAL => (r, ler andalso les)
     | LESS => y
     | GREATER => x;
@@ -209,7 +209,7 @@
 fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
 
 fun choose2 d ((lb, exactl), (ub, exactu)) =
-  let val ord = Rat.cmp_zero lb in
+  let val ord = Rat.sign lb in
   if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
     then Rat.zero
     else if not d then
@@ -237,19 +237,19 @@
   map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (nth bs v) x)), le,
                         nth_map v (K Rat.zero) bs));
 
-fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs
+fun single_var v (_, _, cs) = case filter_out (curry (op =) EQUAL o Rat.sign) cs
  of [x] => x =/ nth cs v
   | _ => false;
 
 (* The base case:
    all variables occur only with positive or only with negative coefficients *)
 fun pick_vars discr (ineqs,ex) =
-  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs
+  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.sign) cs) ineqs
   in case nz of [] => ex
      | (_,_,cs) :: _ =>
-       let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
+       let val v = find_index (not o curry (op =) EQUAL o Rat.sign) cs
            val d = nth discr v;
-           val pos = not (Rat.cmp_zero (nth cs v) = LESS);
+           val pos = not (Rat.sign (nth cs v) = LESS);
            val sv = filter (single_var v) nz;
            val minmax =
              if pos then if d then Rat.roundup o fst o ratrelmax

--- a/src/Tools/float.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/float.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -10,8 +10,8 @@
   type float = integer * integer
   val zero: float
   val eq: float * float -> bool
-  val cmp: float * float -> order
-  val cmp_zero: float -> order
+  val ord: float * float -> order
+  val sign: float -> order
   val min: float -> float -> float
   val max: float -> float -> float
   val add: float -> float -> float
@@ -30,13 +30,13 @@
 val zero: float = (0, 0);
 
 fun add (a1, b1) (a2, b2) =
-  if Integer.cmp (b1, b2) = LESS then
+  if Integer.ord (b1, b2) = LESS then
     (a1 +% a2 *% Integer.exp (b2 -% b1), b1)
   else
     (a1 *% Integer.exp (b1 -% b2) +% a2, b2);
 
 fun sub (a1, b1) (a2, b2) =
-  if Integer.cmp (b1, b2) = LESS then
+  if Integer.ord (b1, b2) = LESS then
     (a1 -% a2 *% Integer.exp (b2 -% b1), b1)
   else
     (a1 *% Integer.exp (b1 -% b2) -% a2, b2);
@@ -45,14 +45,14 @@
 
 fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2);
 
-fun cmp_zero (a, b) = Integer.cmp_zero a;
+fun sign (a, b) = Integer.sign a;
 
-fun cmp (r, s) = cmp_zero (sub r s);
+fun ord (r, s) = sign (sub r s);
 
-fun eq (r, s) = cmp (r, s) = EQUAL;
+fun eq (r, s) = ord (r, s) = EQUAL;
 
-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 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);

--- a/src/Tools/integer.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/integer.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -16,10 +16,12 @@
   val string_of_int: int -> string
   val int_of_string: string -> int option
   val eq: int * int -> bool
-  val cmp: int * int -> order
+  val ord: int * int -> order
   val le: int -> int -> bool
   val lt: int -> int -> bool
-  val cmp_zero: int -> order
+  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
@@ -30,7 +32,6 @@
   val div: int -> int -> int
   val mod: int -> int -> int
   val neg: int -> int
-  val signabs: int -> bool * int
   val exp: int -> int
   val log: int -> int
   val pow: int -> int -> int (* exponent -> base -> result *)
@@ -43,8 +44,6 @@
 
 open IntInf;
 
-type integer = int;
-
 val int = fromInt;
 
 val zero = int 0;
@@ -56,10 +55,12 @@
 val int_of_string = fromString;
 
 val eq = op = : int * int -> bool;
-val cmp = compare;
+val ord = compare;
 val le = curry (op <=);
 val lt = curry (op <);
-fun cmp_zero k = cmp (k, zero);
+
+fun sign k = ord (k, zero);
+fun signabs k = (ord (k, zero), abs k);
 
 val min = curry min;
 val max = curry max;
@@ -74,15 +75,18 @@
 nonfix mod val mod = curry mod;
 val neg = ~;
 
-fun signabs k = if cmp_zero k = LESS then (false, neg k) else (true, k);
-
 fun pow k l =
   let
-    fun pw 0 = 1
-      | pw k = mult l (pw (sub k 1));
+    fun pw 0 _ = 1
+      | 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
     then error "pow: negative exponent"
-    else pw k
+    else pw k l
   end;
 
 fun exp k = pow k two;

--- a/src/Tools/rat.ML	Fri Jun 29 18:21:25 2007 +0200
+++ b/src/Tools/rat.ML	Fri Jun 29 21:23:05 2007 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/General/rat.ML
     ID:         $Id$
-    Author:     Tobias Nipkow, TU Muenchen
+    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 
 Canonical implementation of exact rational numbers.
 *)
@@ -17,113 +17,90 @@
   val quotient_of_rat: rat -> integer * integer
   val string_of_rat: rat -> string
   val eq: rat * rat -> bool
-  val cmp: rat * rat -> order
+  val ord: rat * rat -> order
   val le: rat -> rat -> bool
   val lt: rat -> rat -> bool
-  val cmp_zero: rat -> order
+  val signabs: rat -> order * rat
+  val sign: rat -> order
+  val abs: rat -> rat
   val add: rat -> rat -> rat
   val mult: rat -> rat -> rat
   val neg: rat -> rat
   val inv: rat -> rat
+  val rounddown: rat -> rat
   val roundup: rat -> rat
-  val rounddown: rat -> rat
 end;
 
 structure Rat : RAT =
 struct
 
-datatype rat = Rat of bool * integer * integer;
+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;
+
+datatype rat = Rat of integer * integer; (* nominator, denominator (positive!) *)
 
 exception DIVZERO;
 
-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, 1) end;
-
-fun norm (a, p, q) =
-  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, absp div m, q div m) end;
-
-fun common (p1, q1, p2, q2) =
-  let
-    val q' = Integer.lcm q1 q2;
-  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 absq = 0 then raise DIVZERO
-    else norm (a, p, absq)
-  end;
+    val m = Integer.gcd (Integer.abs p) q
+  in Rat (Integer.div p m, Integer.div q m) end handle Div => raise DIVZERO;
+
+fun quotient_of_rat (Rat r) = r;
+
+fun rat_of_int i = Rat (i, 1);
 
-fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~ p, q);
+val zero = rat_of_int 0;
+val one = rat_of_int 1;
+val two = rat_of_int 2;
 
-fun string_of_rat r =
-  let
-    val (p, q) = quotient_of_rat r;
-  in Integer.string_of_int p ^ "/" ^ Integer.string_of_int q end;
+fun string_of_rat (Rat (p, q)) =
+  Integer.string_of_int p ^ "/" ^ Integer.string_of_int q;
+
+fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
 
-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;
+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
+  | (EQUAL, EQUAL) => EQUAL
+  | (EQUAL, GREATER) => LESS
+  | (GREATER, LESS) => GREATER
+  | (GREATER, EQUAL) => GREATER
+  | _ => Integer.ord (fst (common (p1, q1) (p2, q2)));
 
-fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
-  | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
-  | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
-      let val (r1, r2, _) = common (p1, q1, p2, q2)
-      in if a then Integer.cmp (r1, r2) else Integer.cmp (r2, r1) end;
+fun le a b = not (ord (a, b) = GREATER);
+fun lt a b = (ord (a, b) = LESS);
 
-fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end;
-fun lt a b = (cmp (a, b) = LESS);
+fun sign (Rat (p, _)) = Integer.sign p;
 
-fun cmp_zero (Rat (false, _, _)) = LESS
-  | cmp_zero (Rat (_, 0, _)) = EQUAL
-  | cmp_zero (Rat (_, _, _)) = GREATER;
+fun abs (Rat (p, q)) = Rat (Integer.abs p, q);
 
-fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
+fun signabs (Rat (p, q)) =
   let
-    val (r1, r2, den) = common (p1, q1, p2, q2);
-    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);
+    val (s, p') = Integer.signabs p;
+  in (s, Rat (p', q)) end;
 
-fun neg (r as Rat (b, p, q)) =
-  if p = 0 then r
-  else Rat (not b, 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;
 
-fun inv (Rat (a, p, q)) =
-  if q = 0 then raise DIVZERO
-  else Rat (a, q, p);
+fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
+  rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
 
-fun roundup (r as Rat (a, p, q)) =
-  if q = 1 then r
-  else
-    let
-      fun round true q = Rat (true, q + 1, 1)
-        | round false q =
-            Rat (q = 0, 0, 1);
-    in round a (p div q) end;
+fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
+
+fun inv (Rat (p, 0)) = raise DIVZERO
+  | inv (Rat (p, q)) = Rat (q, p);
 
-fun rounddown (r as Rat (a, p, q)) =
-  if q = 1 then r
-  else
-    let
-      fun round true q = Rat (true, q, 1)
-        | round false q = Rat (false, q + 1, 1)
-    in round a (p div q) end;
+fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
+
+fun roundup (Rat (p, q)) = case Integer.divmod p q
+ of (m, 0) => Rat (m, 1)
+  | (m, _) => Rat (m + 1, 1);
 
 end;