# HG changeset patch
# User haftmann
# Date 1179072925 -7200
# Node ID 8b6d28fc653250989712895a117cca7b783fe6cc
# Parent  997cef733bddfaab3485f0842b31155492af8e80
tuned

diff -r 997cef733bdd -r 8b6d28fc6532 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Sun May 13 18:15:24 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML	Sun May 13 18:15:25 2007 +0200
@@ -17,109 +17,84 @@
 exception CRing of string;
 
 (* Zero and One of the commutative ring *)
-fun cring_zero T = Const("HOL.zero",T);
-fun cring_one T = Const("HOL.one",T);
+fun cring_zero T = Const (@{const_name "HOL.zero"}, T);
+fun cring_one T = Const (@{const_name "HOL.one"}, T);
 
 (* reification functions *)
 (* add two polynom expressions *)
-fun polT t = Type ("Commutative_Ring.pol",[t]);
-fun polexT t = Type("Commutative_Ring.polex",[t]);
-val nT = HOLogic.natT;
-fun listT T = Type ("List.list",[T]);
-
-(* Reification of the constructors *)
-(* Nat*)
-val succ = Const("Suc",nT --> nT);
-val zero = Const("HOL.zero",nT);
-val one = Const("HOL.one",nT);
-
-(* Lists *)
-fun reif_list T [] = Const("List.list.Nil",listT T)
-  | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
-                             $x$(reif_list T xs);
+fun polT t = Type ("Commutative_Ring.pol", [t]);
+fun polexT t = Type ("Commutative_Ring.polex", [t]);
 
 (* pol *)
-fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
-fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
-fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
+fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
+fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
+fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
 
 (* polex *)
-fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
-fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
-fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
-fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
-fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
-fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
-
-(* reification of natural numbers *)
-fun reif_nat n =
-    if n>0 then succ$(reif_nat (n-1))
-    else if n=0 then zero
-    else raise CRing "ring_tac: reif_nat negative n";
+fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
+fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
+fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
+fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
+fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
+fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
 
 (* reification of polynoms : primitive cring expressions *)
-fun reif_pol T vs t =
-    case t of
-       Free(_,_) =>
-        let val i = find_index_eq t vs
-        in if i = 0
-           then (pol_PX T)$((pol_Pc T)$ (cring_one T))
-                          $one$((pol_Pc T)$(cring_zero T))
-           else (pol_Pinj T)$(reif_nat i)$
-                            ((pol_PX T)$((pol_Pc T)$ (cring_one T))
-                                       $one$
-                                       ((pol_Pc T)$(cring_zero T)))
+fun reif_pol T vs (t as Free _) =
+      let
+        val one = @{term "1::nat"};
+        val i = find_index_eq t vs
+      in if i = 0
+        then pol_PX T $ (pol_Pc T $ cring_one T)
+          $ one $ (pol_Pc T $ cring_zero T)
+        else pol_Pinj T $ HOLogic.mk_nat i
+          $ (pol_PX T $ (pol_Pc T $ cring_one T)
+            $ one $ (pol_Pc T $ cring_zero T))
         end
-      | _ => (pol_Pc T)$ t;
-
+  | reif_pol T vs t = pol_Pc T $ t;
 
 (* reification of polynom expressions *)
-fun reif_polex T vs t =
-    case t of
-        Const("HOL.plus",_)$a$b => (polex_add T)
-                                   $ (reif_polex T vs a)$(reif_polex T vs b)
-      | Const("HOL.minus",_)$a$b => (polex_sub T)
-                                   $ (reif_polex T vs a)$(reif_polex T vs b)
-      | Const("HOL.times",_)$a$b =>  (polex_mul T)
-                                    $ (reif_polex T vs a)$ (reif_polex T vs b)
-      | Const("HOL.uminus",_)$a => (polex_neg T)
-                                   $ (reif_polex T vs a)
-      | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
-
-      | _ => (polex_pol T) $ (reif_pol T vs t);
+fun reif_polex T vs (Const (@{const_name "HOL.plus"}, _) $ a $ b) =
+      polex_add T $ reif_polex T vs a $ reif_polex T vs b
+  | reif_polex T vs (Const (@{const_name "HOL.minus"}, _) $ a $ b) =
+      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
+  | reif_polex T vs (Const (@{const_name "HOL.times"}, _) $ a $ b) =
+      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
+  | reif_polex T vs (Const (@{const_name "HOL.uminus"}, _) $ a) =
+      polex_neg T $ reif_polex T vs a
+  | reif_polex T vs (Const (@{const_name "Nat.power"}, _) $ a $ n) =
+      polex_pow T $ reif_polex T vs a $ n
+  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
 (* reification of the equation *)
-val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
-fun reif_eq thy (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
-    if Sign.of_sort thy (a,cr_sort)
-    then
-        let val fs = term_frees eq
-            val cvs = cterm_of thy (reif_list a fs)
-            val clhs = cterm_of thy (reif_polex a fs lhs)
-            val crhs = cterm_of thy (reif_polex a fs rhs)
-            val ca = ctyp_of thy a
-        in (ca,cvs,clhs, crhs)
-        end
-    else raise CRing "reif_eq: not an equation over comm_ring + recpower"
+val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
+
+fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
+      if Sign.of_sort thy (T, cr_sort) then
+        let
+          val fs = term_frees eq;
+          val cvs = cterm_of thy (HOLogic.mk_list T fs);
+          val clhs = cterm_of thy (reif_polex T fs lhs);
+          val crhs = cterm_of thy (reif_polex T fs rhs);
+          val ca = ctyp_of thy T;
+        in (ca, cvs, clhs, crhs) end
+      else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
   | reif_eq _ _ = raise CRing "reif_eq: not an equation";
 
-(*The cring tactic  *)
+(* The cring tactic *)
 (* Attention: You have to make sure that no t^0 is in the goal!! *)
 (* Use simply rewriting t^0 = 1 *)
 val cring_simps =
-  map thm ["mkPX_def", "mkPinj_def","sub_def", "power_add","even_def","pow_if"] @
-  [sym OF [thm "power_add"]];
-
-val norm_eq = thm "norm_eq"
+  [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
+    @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
 
 fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
   let
-    val thy = ProofContext.theory_of ctxt
-    val cring_ss = Simplifier.local_simpset_of ctxt  (* FIXME really the full simpset!? *)
-      addsimps cring_simps
+    val thy = ProofContext.theory_of ctxt;
+    val cring_ss = Simplifier.local_simpset_of ctxt  (*FIXME really the full simpset!?*)
+      addsimps cring_simps;
     val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
     val norm_eq_th =
-      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] norm_eq)
+      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
   in
     cut_rules_tac [norm_eq_th] i
     THEN (simp_tac cring_ss i)
diff -r 997cef733bdd -r 8b6d28fc6532 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sun May 13 18:15:24 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun May 13 18:15:25 2007 +0200
@@ -172,81 +172,91 @@
    Need to know if it is a lower or upper bound for unambiguous interpretation!
 *)
 
-fun elim_eqns(ineqs,Lineq(i,Le,cs,_)) = (i,true,cs)::ineqs
-  | elim_eqns(ineqs,Lineq(i,Eq,cs,_)) = (i,true,cs)::(~i,true,map ~ cs)::ineqs
-  | elim_eqns(ineqs,Lineq(i,Lt,cs,_)) = (i,false,cs)::ineqs;
+fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)]
+  | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)]
+  | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
 
 (* PRE: ex[v] must be 0! *)
-fun eval (ex:Rat.rat list) v (a:IntInf.int,le,cs:IntInf.int list) =
-  let val rs = map Rat.rat_of_intinf cs
-      val rsum = Library.foldl Rat.add (Rat.zero, map Rat.mult (rs ~~ ex))
-  in (Rat.mult (Rat.add(Rat.rat_of_intinf a,Rat.neg rsum), Rat.inv(el v rs)), le) end;
+fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) =
+  let
+    val rs = map Rat.rat_of_int cs;
+    val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
+  in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (el v rs)), le) end;
 (* If el v rs < 0, le should be negated.
    Instead this swap is taken into account in ratrelmin2.
 *)
 
-fun ratrelmin2(x as (r,ler),y as (s,les)) =
-  if r=s then (r, (not ler) andalso (not les)) else if Rat.le(r,s) then x else y;
-fun ratrelmax2(x as (r,ler),y as (s,les)) =
-  if r=s then (r,ler andalso les) else if Rat.le(r,s) then y else x;
+fun ratrelmin2 (x as (r, ler), y as (s, les)) =
+  case Rat.cmp (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)
+   of EQUAL => (r, ler andalso les)
+    | LESS => y
+    | GREATER => x;
 
 val ratrelmin = foldr1 ratrelmin2;
 val ratrelmax = foldr1 ratrelmax2;
 
-fun ratexact up (r,exact) =
+fun ratexact up (r, exact) =
   if exact then r else
-  let val (p,q) = Rat.quotient_of_rat r
-      val nth = Rat.inv(Rat.rat_of_intinf q)
-  in Rat.add(r,if up then nth else Rat.neg nth) end;
+  let
+    val (p, q) = Rat.quotient_of_rat r;
+    val nth = Rat.inv (Rat.rat_of_int q);
+  in Rat.add r (if up then nth else Rat.neg nth) end;
 
-fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
+fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
 
 fun choose2 d ((lb, exactl), (ub, exactu)) =
-  if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
-     Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
-  then Rat.zero else
-  if not d
-  then (if Rat.ge0 lb
+  let val ord = Rat.cmp_zero lb in
+  if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
+    then Rat.zero
+    else if not d then
+      if ord = GREATER
         then if exactl then lb else ratmiddle (lb, ub)
-        else if exactu then ub else ratmiddle (lb, ub))
-  else (* discrete domain, both bounds must be exact *)
-  if Rat.ge0 lb then let val lb' = Rat.roundup lb
-                    in if Rat.le (lb', ub) then lb' else raise NoEx end
-               else let val ub' = Rat.rounddown ub
-                    in if Rat.le (lb, ub') then ub' else raise NoEx end;
+        else if exactu then ub else ratmiddle (lb, ub)
+      else (*discrete domain, both bounds must be exact*)
+      if ord = GREATER (*FIXME this is apparently nonsense*)
+        then let val lb' = Rat.roundup lb in
+          if Rat.le lb' ub then lb' else raise NoEx end
+        else let val ub' = Rat.rounddown ub in
+          if Rat.le lb ub' then ub' else raise NoEx end
+  end;
 
-fun findex1 discr (ex, (v, lineqs)) =
-  let val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
-      val ineqs = Library.foldl elim_eqns ([],nz)
-      val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
-      val lb = ratrelmax (map (eval ex v) ge)
-      val ub = ratrelmin (map (eval ex v) le)
+fun findex1 discr (v, lineqs) ex =
+  let
+    val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
+    val ineqs = maps elim_eqns nz;
+    val (ge, le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
+    val lb = ratrelmax (map (eval ex v) ge)
+    val ub = ratrelmin (map (eval ex v) le)
   in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
 
-fun findex discr = Library.foldl (findex1 discr);
-
 fun elim1 v x =
-  map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
+  map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (el v bs) x)), le,
                         nth_map v (K Rat.zero) bs));
 
-fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
+fun single_var v (_,_,cs) = (filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs = [el v cs]);
 
 (* 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 (equal Rat.zero) cs) ineqs
+  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs
   in case nz of [] => ex
      | (_,_,cs) :: _ =>
-       let val v = find_index (not o equal Rat.zero) cs
-           val d = nth discr v
-           val pos = Rat.ge0(el v cs)
-           val sv = List.filter (single_var v) nz
+       let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
+           val d = nth discr v;
+           val pos = not (Rat.cmp_zero (el v cs) = LESS);
+           val sv = filter (single_var v) nz;
            val minmax =
              if pos then if d then Rat.roundup o fst o ratrelmax
                          else ratexact true o ratrelmax
                     else if d then Rat.rounddown o fst o ratrelmin
                          else ratexact false o ratrelmin
-           val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv
+           val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (el v bs)), le)) sv
            val x = minmax((Rat.zero,if pos then true else false)::bnds)
            val ineqs' = elim1 v x nz
            val ex' = nth_map v (K x) ex
@@ -254,8 +264,8 @@
   end;
 
 fun findex0 discr n lineqs =
-  let val ineqs = Library.foldl elim_eqns ([],lineqs)
-      val rineqs = map (fn (a,le,cs) => (Rat.rat_of_intinf a, le, map Rat.rat_of_intinf cs))
+  let val ineqs = maps elim_eqns lineqs
+      val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs))
                        ineqs
   in pick_vars discr (rineqs,replicate n Rat.zero) end;
 
@@ -546,9 +556,10 @@
   | (v, lineqs) :: hist' =>
     let val frees = map Free params
         fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
-        val start = if v = ~1 then (findex0 discr n lineqs, hist')
-                    else (replicate n Rat.zero, hist)
-        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
+        val start = if v = ~1 then (hist', findex0 discr n lineqs)
+          else (hist, replicate n Rat.zero)
+        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr)
+          (uncurry (fold (findex1 discr)) start))
           handle NoEx => NONE
     in
       case ex of
@@ -678,7 +689,7 @@
            (do_pre : bool) (terms : term list) : injust list option =
   refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
 
-fun count P xs = length (List.filter P xs);
+fun count P xs = length (filter P xs);
 
 (* The limit on the number of ~= allowed.
    Because each ~= is split into two cases, this can lead to an explosion.
diff -r 997cef733bdd -r 8b6d28fc6532 src/Pure/General/rat.ML
--- a/src/Pure/General/rat.ML	Sun May 13 18:15:24 2007 +0200
+++ b/src/Pure/General/rat.ML	Sun May 13 18:15:25 2007 +0200
@@ -11,21 +11,19 @@
   exception DIVZERO
   val zero: rat
   val one: rat
-  val rat_of_int: int -> rat
-  val rat_of_intinf: IntInf.int -> rat
-  val rat_of_quotient: IntInf.int * IntInf.int -> rat
-  val quotient_of_rat: rat -> IntInf.int * IntInf.int
+  val two: rat
+  val rat_of_int: Intt.int -> rat
+  val rat_of_quotient: Intt.int * Intt.int -> rat
+  val quotient_of_rat: rat -> Intt.int * Intt.int
   val string_of_rat: rat -> string
   val eq: rat * rat -> bool
-  val le: rat * rat -> bool
-  val lt: rat * rat -> bool
-  val ord: rat * rat -> order
-  val add: rat * rat -> rat
-  val mult: rat * rat -> rat
+  val cmp: rat * rat -> order
+  val le: rat -> rat -> bool
+  val cmp_zero: rat -> order
+  val add: rat -> rat -> rat
+  val mult: rat -> rat -> rat
   val neg: rat -> rat
   val inv: rat -> rat
-  val ge0: rat -> bool
-  val gt0: rat -> bool
   val roundup: rat -> rat
   val rounddown: rat -> rat
 end;
@@ -33,104 +31,95 @@
 structure Rat: RAT =
 struct
 
-(*keep them normalized!*)
-
-datatype rat = Rat of bool * IntInf.int * IntInf.int;
+datatype rat = Rat of bool * Intt.int * Intt.int;
 
 exception DIVZERO;
 
-val zero = Rat (true, IntInf.fromInt 0, IntInf.fromInt 1);
-
-val one = Rat (true, IntInf.fromInt 1, IntInf.fromInt 1);
+val zero = Rat (true, Intt.int 0, Intt.int 1);
+val one = Rat (true, Intt.int 1, Intt.int 1);
+val two = Rat (true, Intt.int 2, Intt.int 1);
 
-fun rat_of_intinf i =
-  if i < IntInf.fromInt 0
-  then Rat (false, ~i, IntInf.fromInt 1)
-  else Rat (true, i, IntInf.fromInt 1);
-
-fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
+fun rat_of_int i =
+  if i < Intt.int 0
+  then Rat (false, ~i, Intt.int 1)
+  else Rat (true, i, Intt.int 1);
 
 fun norm (a, p, q) =
-  if p = IntInf.fromInt 0 then Rat (true, IntInf.fromInt 0, IntInf.fromInt 1)
+  if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1)
   else
     let
       val absp = abs p
       val m = gcd (absp, q)
-    in Rat(a = (IntInf.fromInt 0 <= p), absp div m, q div m) end;
+    in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end;
 
 fun common (p1, q1, p2, q2) =
   let val q' = lcm (q1, q2)
   in (p1 * (q' div q1), p2 * (q' div q2), q') end
 
 fun rat_of_quotient (p, q) =
-  if q = IntInf.fromInt 0 then raise DIVZERO
-  else norm (IntInf.fromInt 0 <= q, p, abs q);
+  if q = Intt.int 0 then raise DIVZERO
+  else norm (Intt.int 0 <= q, p, abs q);
 
 fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q);
 
 fun string_of_rat r =
   let val (p, q) = quotient_of_rat r
-  in IntInf.toString p ^ "/" ^ IntInf.toString q end;
+  in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end;
 
 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 le (Rat (false, _, _), Rat (true, _, _)) = true
-  | le (Rat (true, _, _), Rat (false, _, _)) = false
-  | le (Rat (a, p1, q1), Rat (_, p2, q2)) =
+fun le (Rat (false, _, _)) (Rat (true, _, _)) = true
+  | le (Rat (true, _, _)) (Rat (false, _, _)) = false
+  | le (Rat (a, p1, q1)) (Rat (_, p2, q2)) =
       let val (r1, r2, _) = common (p1, q1, p2, q2)
       in if a then r1 <= r2 else r2 <= r1 end;
 
-fun lt (Rat (false, _, _), Rat (true, _, _)) = true
-  | lt (Rat (true, _, _), Rat (false, _, _)) = false
-  | lt (Rat (a, p1, q1), Rat (_, 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 r1 < r2 else r2 < r1 end;
+      in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
 
-fun ord (Rat (false, _, _), Rat (true, _, _)) = LESS
-  | ord (Rat (true, _, _), Rat (false, _, _)) = GREATER
-  | ord (Rat (a, p1, q1), Rat (_, p2, q2)) =
-      let val (r1, r2, _) = common (p1, q1, p2, q2)
-      in if a then IntInf.compare (r1, r2) else IntInf.compare (r2, r1) end;
+fun cmp_zero (Rat (false, _, _)) = LESS
+  | cmp_zero (Rat (_, 0, _)) = EQUAL
+  | cmp_zero (Rat (_, _, _)) = GREATER;
 
-fun add (Rat (a1, p1, q1), Rat(a2, p2, q2)) =
+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 ~r1) + (if a2 then r2 else ~r2)
   in norm (true, num, den) end;
 
-fun mult (Rat (a1, p1, q1), Rat (a2, p2, q2)) =
+fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
   norm (a1=a2, p1*p2, q1*q2);
 
 fun neg (r as Rat (b, p, q)) =
-  if p = IntInf.fromInt 0 then r
+  if p = Intt.int 0 then r
   else Rat (not b, p, q);
 
 fun inv (Rat (a, p, q)) =
-  if p = IntInf.fromInt 0 then raise DIVZERO
+  if p = Intt.int 0 then raise DIVZERO
   else Rat (a, q, p);
 
-fun ge0 (Rat (a, _, _)) = a;
-fun gt0 (Rat (a, p, _)) = a andalso p > IntInf.fromInt 0;
-
 fun roundup (r as Rat (a, p, q)) =
-  if q = IntInf.fromInt 1 then r
+  if q = Intt.int 1 then r
   else
     let
-      fun round true q = Rat (true, q + IntInf.fromInt 1, IntInf.fromInt 1)
+      fun round true q = Rat (true, q + Intt.int 1, Intt.int 1)
         | round false q =
-            if q = IntInf.fromInt 0
-            then Rat (true, IntInf.fromInt 0, IntInf.fromInt 1)
-            else Rat (false, q, IntInf.fromInt 1);
+            if q = Intt.int 0
+            then Rat (true, Intt.int 0, Intt.int 1)
+            else Rat (false, q, Intt.int 1);
     in round a (p div q) end;
 
 fun rounddown (r as Rat (a, p, q)) =
-  if q = IntInf.fromInt 1 then r
+  if q = Intt.int 1 then r
   else
     let
-      fun round true q = Rat (true, q, IntInf.fromInt 1)
-        | round false q = Rat (false, q + IntInf.fromInt 1, IntInf.fromInt 1)
+      fun round true q = Rat (true, q, Intt.int 1)
+        | round false q = Rat (false, q + Intt.int 1, Intt.int 1)
     in round a (p div q) end;
 
 end;