tuned
authorhaftmann
Sun May 13 18:15:25 2007 +0200 (2007-05-13)
changeset 229508b6d28fc6532
parent 22949 997cef733bdd
child 22951 dfafcd6223ad
tuned
src/HOL/Library/comm_ring.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/General/rat.ML
     1.1 --- a/src/HOL/Library/comm_ring.ML	Sun May 13 18:15:24 2007 +0200
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Sun May 13 18:15:25 2007 +0200
     1.3 @@ -17,109 +17,84 @@
     1.4  exception CRing of string;
     1.5  
     1.6  (* Zero and One of the commutative ring *)
     1.7 -fun cring_zero T = Const("HOL.zero",T);
     1.8 -fun cring_one T = Const("HOL.one",T);
     1.9 +fun cring_zero T = Const (@{const_name "HOL.zero"}, T);
    1.10 +fun cring_one T = Const (@{const_name "HOL.one"}, T);
    1.11  
    1.12  (* reification functions *)
    1.13  (* add two polynom expressions *)
    1.14 -fun polT t = Type ("Commutative_Ring.pol",[t]);
    1.15 -fun polexT t = Type("Commutative_Ring.polex",[t]);
    1.16 -val nT = HOLogic.natT;
    1.17 -fun listT T = Type ("List.list",[T]);
    1.18 -
    1.19 -(* Reification of the constructors *)
    1.20 -(* Nat*)
    1.21 -val succ = Const("Suc",nT --> nT);
    1.22 -val zero = Const("HOL.zero",nT);
    1.23 -val one = Const("HOL.one",nT);
    1.24 -
    1.25 -(* Lists *)
    1.26 -fun reif_list T [] = Const("List.list.Nil",listT T)
    1.27 -  | reif_list T (x::xs) = Const("List.list.Cons",[T,listT T] ---> listT T)
    1.28 -                             $x$(reif_list T xs);
    1.29 +fun polT t = Type ("Commutative_Ring.pol", [t]);
    1.30 +fun polexT t = Type ("Commutative_Ring.polex", [t]);
    1.31  
    1.32  (* pol *)
    1.33 -fun pol_Pc t = Const("Commutative_Ring.pol.Pc",t --> polT t);
    1.34 -fun pol_Pinj t = Const("Commutative_Ring.pol.Pinj",[nT,polT t] ---> polT t);
    1.35 -fun pol_PX t = Const("Commutative_Ring.pol.PX",[polT t, nT, polT t] ---> polT t);
    1.36 +fun pol_Pc t = Const ("Commutative_Ring.pol.Pc", t --> polT t);
    1.37 +fun pol_Pinj t = Const ("Commutative_Ring.pol.Pinj", HOLogic.natT --> polT t --> polT t);
    1.38 +fun pol_PX t = Const ("Commutative_Ring.pol.PX", polT t --> HOLogic.natT --> polT t --> polT t);
    1.39  
    1.40  (* polex *)
    1.41 -fun polex_add t = Const("Commutative_Ring.polex.Add",[polexT t,polexT t] ---> polexT t);
    1.42 -fun polex_sub t = Const("Commutative_Ring.polex.Sub",[polexT t,polexT t] ---> polexT t);
    1.43 -fun polex_mul t = Const("Commutative_Ring.polex.Mul",[polexT t,polexT t] ---> polexT t);
    1.44 -fun polex_neg t = Const("Commutative_Ring.polex.Neg",polexT t --> polexT t);
    1.45 -fun polex_pol t = Const("Commutative_Ring.polex.Pol",polT t --> polexT t);
    1.46 -fun polex_pow t = Const("Commutative_Ring.polex.Pow",[polexT t, nT] ---> polexT t);
    1.47 -
    1.48 -(* reification of natural numbers *)
    1.49 -fun reif_nat n =
    1.50 -    if n>0 then succ$(reif_nat (n-1))
    1.51 -    else if n=0 then zero
    1.52 -    else raise CRing "ring_tac: reif_nat negative n";
    1.53 +fun polex_add t = Const ("Commutative_Ring.polex.Add", polexT t --> polexT t --> polexT t);
    1.54 +fun polex_sub t = Const ("Commutative_Ring.polex.Sub", polexT t --> polexT t --> polexT t);
    1.55 +fun polex_mul t = Const ("Commutative_Ring.polex.Mul", polexT t --> polexT t --> polexT t);
    1.56 +fun polex_neg t = Const ("Commutative_Ring.polex.Neg", polexT t --> polexT t);
    1.57 +fun polex_pol t = Const ("Commutative_Ring.polex.Pol", polT t --> polexT t);
    1.58 +fun polex_pow t = Const ("Commutative_Ring.polex.Pow", polexT t --> HOLogic.natT --> polexT t);
    1.59  
    1.60  (* reification of polynoms : primitive cring expressions *)
    1.61 -fun reif_pol T vs t =
    1.62 -    case t of
    1.63 -       Free(_,_) =>
    1.64 -        let val i = find_index_eq t vs
    1.65 -        in if i = 0
    1.66 -           then (pol_PX T)$((pol_Pc T)$ (cring_one T))
    1.67 -                          $one$((pol_Pc T)$(cring_zero T))
    1.68 -           else (pol_Pinj T)$(reif_nat i)$
    1.69 -                            ((pol_PX T)$((pol_Pc T)$ (cring_one T))
    1.70 -                                       $one$
    1.71 -                                       ((pol_Pc T)$(cring_zero T)))
    1.72 +fun reif_pol T vs (t as Free _) =
    1.73 +      let
    1.74 +        val one = @{term "1::nat"};
    1.75 +        val i = find_index_eq t vs
    1.76 +      in if i = 0
    1.77 +        then pol_PX T $ (pol_Pc T $ cring_one T)
    1.78 +          $ one $ (pol_Pc T $ cring_zero T)
    1.79 +        else pol_Pinj T $ HOLogic.mk_nat i
    1.80 +          $ (pol_PX T $ (pol_Pc T $ cring_one T)
    1.81 +            $ one $ (pol_Pc T $ cring_zero T))
    1.82          end
    1.83 -      | _ => (pol_Pc T)$ t;
    1.84 -
    1.85 +  | reif_pol T vs t = pol_Pc T $ t;
    1.86  
    1.87  (* reification of polynom expressions *)
    1.88 -fun reif_polex T vs t =
    1.89 -    case t of
    1.90 -        Const("HOL.plus",_)$a$b => (polex_add T)
    1.91 -                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    1.92 -      | Const("HOL.minus",_)$a$b => (polex_sub T)
    1.93 -                                   $ (reif_polex T vs a)$(reif_polex T vs b)
    1.94 -      | Const("HOL.times",_)$a$b =>  (polex_mul T)
    1.95 -                                    $ (reif_polex T vs a)$ (reif_polex T vs b)
    1.96 -      | Const("HOL.uminus",_)$a => (polex_neg T)
    1.97 -                                   $ (reif_polex T vs a)
    1.98 -      | (Const("Nat.power",_)$a$n) => (polex_pow T) $ (reif_polex T vs a) $ n
    1.99 -
   1.100 -      | _ => (polex_pol T) $ (reif_pol T vs t);
   1.101 +fun reif_polex T vs (Const (@{const_name "HOL.plus"}, _) $ a $ b) =
   1.102 +      polex_add T $ reif_polex T vs a $ reif_polex T vs b
   1.103 +  | reif_polex T vs (Const (@{const_name "HOL.minus"}, _) $ a $ b) =
   1.104 +      polex_sub T $ reif_polex T vs a $ reif_polex T vs b
   1.105 +  | reif_polex T vs (Const (@{const_name "HOL.times"}, _) $ a $ b) =
   1.106 +      polex_mul T $ reif_polex T vs a $ reif_polex T vs b
   1.107 +  | reif_polex T vs (Const (@{const_name "HOL.uminus"}, _) $ a) =
   1.108 +      polex_neg T $ reif_polex T vs a
   1.109 +  | reif_polex T vs (Const (@{const_name "Nat.power"}, _) $ a $ n) =
   1.110 +      polex_pow T $ reif_polex T vs a $ n
   1.111 +  | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
   1.112  
   1.113  (* reification of the equation *)
   1.114 -val cr_sort = Sign.read_sort (the_context ()) "{comm_ring,recpower}";
   1.115 -fun reif_eq thy (eq as Const("op =",Type("fun",a::_))$lhs$rhs) =
   1.116 -    if Sign.of_sort thy (a,cr_sort)
   1.117 -    then
   1.118 -        let val fs = term_frees eq
   1.119 -            val cvs = cterm_of thy (reif_list a fs)
   1.120 -            val clhs = cterm_of thy (reif_polex a fs lhs)
   1.121 -            val crhs = cterm_of thy (reif_polex a fs rhs)
   1.122 -            val ca = ctyp_of thy a
   1.123 -        in (ca,cvs,clhs, crhs)
   1.124 -        end
   1.125 -    else raise CRing "reif_eq: not an equation over comm_ring + recpower"
   1.126 +val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"};
   1.127 +
   1.128 +fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) =
   1.129 +      if Sign.of_sort thy (T, cr_sort) then
   1.130 +        let
   1.131 +          val fs = term_frees eq;
   1.132 +          val cvs = cterm_of thy (HOLogic.mk_list T fs);
   1.133 +          val clhs = cterm_of thy (reif_polex T fs lhs);
   1.134 +          val crhs = cterm_of thy (reif_polex T fs rhs);
   1.135 +          val ca = ctyp_of thy T;
   1.136 +        in (ca, cvs, clhs, crhs) end
   1.137 +      else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
   1.138    | reif_eq _ _ = raise CRing "reif_eq: not an equation";
   1.139  
   1.140 -(*The cring tactic  *)
   1.141 +(* The cring tactic *)
   1.142  (* Attention: You have to make sure that no t^0 is in the goal!! *)
   1.143  (* Use simply rewriting t^0 = 1 *)
   1.144  val cring_simps =
   1.145 -  map thm ["mkPX_def", "mkPinj_def","sub_def", "power_add","even_def","pow_if"] @
   1.146 -  [sym OF [thm "power_add"]];
   1.147 -
   1.148 -val norm_eq = thm "norm_eq"
   1.149 +  [@{thm mkPX_def}, @{thm mkPinj_def}, @{thm sub_def}, @{thm power_add},
   1.150 +    @{thm even_def}, @{thm pow_if}, sym OF [@{thm power_add}]];
   1.151  
   1.152  fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
   1.153    let
   1.154 -    val thy = ProofContext.theory_of ctxt
   1.155 -    val cring_ss = Simplifier.local_simpset_of ctxt  (* FIXME really the full simpset!? *)
   1.156 -      addsimps cring_simps
   1.157 +    val thy = ProofContext.theory_of ctxt;
   1.158 +    val cring_ss = Simplifier.local_simpset_of ctxt  (*FIXME really the full simpset!?*)
   1.159 +      addsimps cring_simps;
   1.160      val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
   1.161      val norm_eq_th =
   1.162 -      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] norm_eq)
   1.163 +      simplify cring_ss (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs] @{thm norm_eq})
   1.164    in
   1.165      cut_rules_tac [norm_eq_th] i
   1.166      THEN (simp_tac cring_ss i)
     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sun May 13 18:15:24 2007 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun May 13 18:15:25 2007 +0200
     2.3 @@ -172,81 +172,91 @@
     2.4     Need to know if it is a lower or upper bound for unambiguous interpretation!
     2.5  *)
     2.6  
     2.7 -fun elim_eqns(ineqs,Lineq(i,Le,cs,_)) = (i,true,cs)::ineqs
     2.8 -  | elim_eqns(ineqs,Lineq(i,Eq,cs,_)) = (i,true,cs)::(~i,true,map ~ cs)::ineqs
     2.9 -  | elim_eqns(ineqs,Lineq(i,Lt,cs,_)) = (i,false,cs)::ineqs;
    2.10 +fun elim_eqns (Lineq (i, Le, cs, _)) = [(i, true, cs)]
    2.11 +  | elim_eqns (Lineq (i, Eq, cs, _)) = [(i, true, cs),(~i, true, map ~ cs)]
    2.12 +  | elim_eqns (Lineq (i, Lt, cs, _)) = [(i, false, cs)];
    2.13  
    2.14  (* PRE: ex[v] must be 0! *)
    2.15 -fun eval (ex:Rat.rat list) v (a:IntInf.int,le,cs:IntInf.int list) =
    2.16 -  let val rs = map Rat.rat_of_intinf cs
    2.17 -      val rsum = Library.foldl Rat.add (Rat.zero, map Rat.mult (rs ~~ ex))
    2.18 -  in (Rat.mult (Rat.add(Rat.rat_of_intinf a,Rat.neg rsum), Rat.inv(el v rs)), le) end;
    2.19 +fun eval ex v (a:IntInf.int,le,cs:IntInf.int list) =
    2.20 +  let
    2.21 +    val rs = map Rat.rat_of_int cs;
    2.22 +    val rsum = fold2 (Rat.add oo Rat.mult) rs ex Rat.zero;
    2.23 +  in (Rat.mult (Rat.add (Rat.rat_of_int a) (Rat.neg rsum)) (Rat.inv (el v rs)), le) end;
    2.24  (* If el v rs < 0, le should be negated.
    2.25     Instead this swap is taken into account in ratrelmin2.
    2.26  *)
    2.27  
    2.28 -fun ratrelmin2(x as (r,ler),y as (s,les)) =
    2.29 -  if r=s then (r, (not ler) andalso (not les)) else if Rat.le(r,s) then x else y;
    2.30 -fun ratrelmax2(x as (r,ler),y as (s,les)) =
    2.31 -  if r=s then (r,ler andalso les) else if Rat.le(r,s) then y else x;
    2.32 +fun ratrelmin2 (x as (r, ler), y as (s, les)) =
    2.33 +  case Rat.cmp (r, s)
    2.34 +   of EQUAL => (r, (not ler) andalso (not les))
    2.35 +    | LESS => x
    2.36 +    | GREATER => y;
    2.37 +
    2.38 +fun ratrelmax2 (x as (r, ler), y as (s, les)) =
    2.39 +  case Rat.cmp (r, s)
    2.40 +   of EQUAL => (r, ler andalso les)
    2.41 +    | LESS => y
    2.42 +    | GREATER => x;
    2.43  
    2.44  val ratrelmin = foldr1 ratrelmin2;
    2.45  val ratrelmax = foldr1 ratrelmax2;
    2.46  
    2.47 -fun ratexact up (r,exact) =
    2.48 +fun ratexact up (r, exact) =
    2.49    if exact then r else
    2.50 -  let val (p,q) = Rat.quotient_of_rat r
    2.51 -      val nth = Rat.inv(Rat.rat_of_intinf q)
    2.52 -  in Rat.add(r,if up then nth else Rat.neg nth) end;
    2.53 +  let
    2.54 +    val (p, q) = Rat.quotient_of_rat r;
    2.55 +    val nth = Rat.inv (Rat.rat_of_int q);
    2.56 +  in Rat.add r (if up then nth else Rat.neg nth) end;
    2.57  
    2.58 -fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
    2.59 +fun ratmiddle (r, s) = Rat.mult (Rat.add r s) (Rat.inv Rat.two);
    2.60  
    2.61  fun choose2 d ((lb, exactl), (ub, exactu)) =
    2.62 -  if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
    2.63 -     Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
    2.64 -  then Rat.zero else
    2.65 -  if not d
    2.66 -  then (if Rat.ge0 lb
    2.67 +  let val ord = Rat.cmp_zero lb in
    2.68 +  if (ord = LESS orelse exactl) andalso (ord = GREATER orelse exactu)
    2.69 +    then Rat.zero
    2.70 +    else if not d then
    2.71 +      if ord = GREATER
    2.72          then if exactl then lb else ratmiddle (lb, ub)
    2.73 -        else if exactu then ub else ratmiddle (lb, ub))
    2.74 -  else (* discrete domain, both bounds must be exact *)
    2.75 -  if Rat.ge0 lb then let val lb' = Rat.roundup lb
    2.76 -                    in if Rat.le (lb', ub) then lb' else raise NoEx end
    2.77 -               else let val ub' = Rat.rounddown ub
    2.78 -                    in if Rat.le (lb, ub') then ub' else raise NoEx end;
    2.79 +        else if exactu then ub else ratmiddle (lb, ub)
    2.80 +      else (*discrete domain, both bounds must be exact*)
    2.81 +      if ord = GREATER (*FIXME this is apparently nonsense*)
    2.82 +        then let val lb' = Rat.roundup lb in
    2.83 +          if Rat.le lb' ub then lb' else raise NoEx end
    2.84 +        else let val ub' = Rat.rounddown ub in
    2.85 +          if Rat.le lb ub' then ub' else raise NoEx end
    2.86 +  end;
    2.87  
    2.88 -fun findex1 discr (ex, (v, lineqs)) =
    2.89 -  let val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
    2.90 -      val ineqs = Library.foldl elim_eqns ([],nz)
    2.91 -      val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
    2.92 -      val lb = ratrelmax (map (eval ex v) ge)
    2.93 -      val ub = ratrelmin (map (eval ex v) le)
    2.94 +fun findex1 discr (v, lineqs) ex =
    2.95 +  let
    2.96 +    val nz = filter (fn (Lineq (_, _, cs, _)) => el v cs <> 0) lineqs;
    2.97 +    val ineqs = maps elim_eqns nz;
    2.98 +    val (ge, le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
    2.99 +    val lb = ratrelmax (map (eval ex v) ge)
   2.100 +    val ub = ratrelmin (map (eval ex v) le)
   2.101    in nth_map v (K (choose2 (nth discr v) (lb, ub))) ex end;
   2.102  
   2.103 -fun findex discr = Library.foldl (findex1 discr);
   2.104 -
   2.105  fun elim1 v x =
   2.106 -  map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
   2.107 +  map (fn (a,le,bs) => (Rat.add a (Rat.neg (Rat.mult (el v bs) x)), le,
   2.108                          nth_map v (K Rat.zero) bs));
   2.109  
   2.110 -fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
   2.111 +fun single_var v (_,_,cs) = (filter_out (curry (op =) EQUAL o Rat.cmp_zero) cs = [el v cs]);
   2.112  
   2.113  (* The base case:
   2.114     all variables occur only with positive or only with negative coefficients *)
   2.115  fun pick_vars discr (ineqs,ex) =
   2.116 -  let val nz = filter_out (fn (_,_,cs) => forall (equal Rat.zero) cs) ineqs
   2.117 +  let val nz = filter_out (fn (_,_,cs) => forall (curry (op =) EQUAL o Rat.cmp_zero) cs) ineqs
   2.118    in case nz of [] => ex
   2.119       | (_,_,cs) :: _ =>
   2.120 -       let val v = find_index (not o equal Rat.zero) cs
   2.121 -           val d = nth discr v
   2.122 -           val pos = Rat.ge0(el v cs)
   2.123 -           val sv = List.filter (single_var v) nz
   2.124 +       let val v = find_index (not o curry (op =) EQUAL o Rat.cmp_zero) cs
   2.125 +           val d = nth discr v;
   2.126 +           val pos = not (Rat.cmp_zero (el v cs) = LESS);
   2.127 +           val sv = filter (single_var v) nz;
   2.128             val minmax =
   2.129               if pos then if d then Rat.roundup o fst o ratrelmax
   2.130                           else ratexact true o ratrelmax
   2.131                      else if d then Rat.rounddown o fst o ratrelmin
   2.132                           else ratexact false o ratrelmin
   2.133 -           val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv
   2.134 +           val bnds = map (fn (a,le,bs) => (Rat.mult a (Rat.inv (el v bs)), le)) sv
   2.135             val x = minmax((Rat.zero,if pos then true else false)::bnds)
   2.136             val ineqs' = elim1 v x nz
   2.137             val ex' = nth_map v (K x) ex
   2.138 @@ -254,8 +264,8 @@
   2.139    end;
   2.140  
   2.141  fun findex0 discr n lineqs =
   2.142 -  let val ineqs = Library.foldl elim_eqns ([],lineqs)
   2.143 -      val rineqs = map (fn (a,le,cs) => (Rat.rat_of_intinf a, le, map Rat.rat_of_intinf cs))
   2.144 +  let val ineqs = maps elim_eqns lineqs
   2.145 +      val rineqs = map (fn (a,le,cs) => (Rat.rat_of_int a, le, map Rat.rat_of_int cs))
   2.146                         ineqs
   2.147    in pick_vars discr (rineqs,replicate n Rat.zero) end;
   2.148  
   2.149 @@ -546,9 +556,10 @@
   2.150    | (v, lineqs) :: hist' =>
   2.151      let val frees = map Free params
   2.152          fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
   2.153 -        val start = if v = ~1 then (findex0 discr n lineqs, hist')
   2.154 -                    else (replicate n Rat.zero, hist)
   2.155 -        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
   2.156 +        val start = if v = ~1 then (hist', findex0 discr n lineqs)
   2.157 +          else (hist, replicate n Rat.zero)
   2.158 +        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr)
   2.159 +          (uncurry (fold (findex1 discr)) start))
   2.160            handle NoEx => NONE
   2.161      in
   2.162        case ex of
   2.163 @@ -678,7 +689,7 @@
   2.164             (do_pre : bool) (terms : term list) : injust list option =
   2.165    refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
   2.166  
   2.167 -fun count P xs = length (List.filter P xs);
   2.168 +fun count P xs = length (filter P xs);
   2.169  
   2.170  (* The limit on the number of ~= allowed.
   2.171     Because each ~= is split into two cases, this can lead to an explosion.
     3.1 --- a/src/Pure/General/rat.ML	Sun May 13 18:15:24 2007 +0200
     3.2 +++ b/src/Pure/General/rat.ML	Sun May 13 18:15:25 2007 +0200
     3.3 @@ -11,21 +11,19 @@
     3.4    exception DIVZERO
     3.5    val zero: rat
     3.6    val one: rat
     3.7 -  val rat_of_int: int -> rat
     3.8 -  val rat_of_intinf: IntInf.int -> rat
     3.9 -  val rat_of_quotient: IntInf.int * IntInf.int -> rat
    3.10 -  val quotient_of_rat: rat -> IntInf.int * IntInf.int
    3.11 +  val two: rat
    3.12 +  val rat_of_int: Intt.int -> rat
    3.13 +  val rat_of_quotient: Intt.int * Intt.int -> rat
    3.14 +  val quotient_of_rat: rat -> Intt.int * Intt.int
    3.15    val string_of_rat: rat -> string
    3.16    val eq: rat * rat -> bool
    3.17 -  val le: rat * rat -> bool
    3.18 -  val lt: rat * rat -> bool
    3.19 -  val ord: rat * rat -> order
    3.20 -  val add: rat * rat -> rat
    3.21 -  val mult: rat * rat -> rat
    3.22 +  val cmp: rat * rat -> order
    3.23 +  val le: rat -> rat -> bool
    3.24 +  val cmp_zero: rat -> order
    3.25 +  val add: rat -> rat -> rat
    3.26 +  val mult: rat -> rat -> rat
    3.27    val neg: rat -> rat
    3.28    val inv: rat -> rat
    3.29 -  val ge0: rat -> bool
    3.30 -  val gt0: rat -> bool
    3.31    val roundup: rat -> rat
    3.32    val rounddown: rat -> rat
    3.33  end;
    3.34 @@ -33,104 +31,95 @@
    3.35  structure Rat: RAT =
    3.36  struct
    3.37  
    3.38 -(*keep them normalized!*)
    3.39 -
    3.40 -datatype rat = Rat of bool * IntInf.int * IntInf.int;
    3.41 +datatype rat = Rat of bool * Intt.int * Intt.int;
    3.42  
    3.43  exception DIVZERO;
    3.44  
    3.45 -val zero = Rat (true, IntInf.fromInt 0, IntInf.fromInt 1);
    3.46 -
    3.47 -val one = Rat (true, IntInf.fromInt 1, IntInf.fromInt 1);
    3.48 +val zero = Rat (true, Intt.int 0, Intt.int 1);
    3.49 +val one = Rat (true, Intt.int 1, Intt.int 1);
    3.50 +val two = Rat (true, Intt.int 2, Intt.int 1);
    3.51  
    3.52 -fun rat_of_intinf i =
    3.53 -  if i < IntInf.fromInt 0
    3.54 -  then Rat (false, ~i, IntInf.fromInt 1)
    3.55 -  else Rat (true, i, IntInf.fromInt 1);
    3.56 -
    3.57 -fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
    3.58 +fun rat_of_int i =
    3.59 +  if i < Intt.int 0
    3.60 +  then Rat (false, ~i, Intt.int 1)
    3.61 +  else Rat (true, i, Intt.int 1);
    3.62  
    3.63  fun norm (a, p, q) =
    3.64 -  if p = IntInf.fromInt 0 then Rat (true, IntInf.fromInt 0, IntInf.fromInt 1)
    3.65 +  if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1)
    3.66    else
    3.67      let
    3.68        val absp = abs p
    3.69        val m = gcd (absp, q)
    3.70 -    in Rat(a = (IntInf.fromInt 0 <= p), absp div m, q div m) end;
    3.71 +    in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end;
    3.72  
    3.73  fun common (p1, q1, p2, q2) =
    3.74    let val q' = lcm (q1, q2)
    3.75    in (p1 * (q' div q1), p2 * (q' div q2), q') end
    3.76  
    3.77  fun rat_of_quotient (p, q) =
    3.78 -  if q = IntInf.fromInt 0 then raise DIVZERO
    3.79 -  else norm (IntInf.fromInt 0 <= q, p, abs q);
    3.80 +  if q = Intt.int 0 then raise DIVZERO
    3.81 +  else norm (Intt.int 0 <= q, p, abs q);
    3.82  
    3.83  fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q);
    3.84  
    3.85  fun string_of_rat r =
    3.86    let val (p, q) = quotient_of_rat r
    3.87 -  in IntInf.toString p ^ "/" ^ IntInf.toString q end;
    3.88 +  in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end;
    3.89  
    3.90  fun eq (Rat (false, _, _), Rat (true, _, _)) = false
    3.91    | eq (Rat (true, _, _), Rat (false, _, _)) = false
    3.92    | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2
    3.93  
    3.94 -fun le (Rat (false, _, _), Rat (true, _, _)) = true
    3.95 -  | le (Rat (true, _, _), Rat (false, _, _)) = false
    3.96 -  | le (Rat (a, p1, q1), Rat (_, p2, q2)) =
    3.97 +fun le (Rat (false, _, _)) (Rat (true, _, _)) = true
    3.98 +  | le (Rat (true, _, _)) (Rat (false, _, _)) = false
    3.99 +  | le (Rat (a, p1, q1)) (Rat (_, p2, q2)) =
   3.100        let val (r1, r2, _) = common (p1, q1, p2, q2)
   3.101        in if a then r1 <= r2 else r2 <= r1 end;
   3.102  
   3.103 -fun lt (Rat (false, _, _), Rat (true, _, _)) = true
   3.104 -  | lt (Rat (true, _, _), Rat (false, _, _)) = false
   3.105 -  | lt (Rat (a, p1, q1), Rat (_, p2, q2)) =
   3.106 +fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
   3.107 +  | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
   3.108 +  | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) =
   3.109        let val (r1, r2, _) = common (p1, q1, p2, q2)
   3.110 -      in if a then r1 < r2 else r2 < r1 end;
   3.111 +      in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end;
   3.112  
   3.113 -fun ord (Rat (false, _, _), Rat (true, _, _)) = LESS
   3.114 -  | ord (Rat (true, _, _), Rat (false, _, _)) = GREATER
   3.115 -  | ord (Rat (a, p1, q1), Rat (_, p2, q2)) =
   3.116 -      let val (r1, r2, _) = common (p1, q1, p2, q2)
   3.117 -      in if a then IntInf.compare (r1, r2) else IntInf.compare (r2, r1) end;
   3.118 +fun cmp_zero (Rat (false, _, _)) = LESS
   3.119 +  | cmp_zero (Rat (_, 0, _)) = EQUAL
   3.120 +  | cmp_zero (Rat (_, _, _)) = GREATER;
   3.121  
   3.122 -fun add (Rat (a1, p1, q1), Rat(a2, p2, q2)) =
   3.123 +fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
   3.124    let
   3.125      val (r1, r2, den) = common (p1, q1, p2, q2)
   3.126      val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2)
   3.127    in norm (true, num, den) end;
   3.128  
   3.129 -fun mult (Rat (a1, p1, q1), Rat (a2, p2, q2)) =
   3.130 +fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
   3.131    norm (a1=a2, p1*p2, q1*q2);
   3.132  
   3.133  fun neg (r as Rat (b, p, q)) =
   3.134 -  if p = IntInf.fromInt 0 then r
   3.135 +  if p = Intt.int 0 then r
   3.136    else Rat (not b, p, q);
   3.137  
   3.138  fun inv (Rat (a, p, q)) =
   3.139 -  if p = IntInf.fromInt 0 then raise DIVZERO
   3.140 +  if p = Intt.int 0 then raise DIVZERO
   3.141    else Rat (a, q, p);
   3.142  
   3.143 -fun ge0 (Rat (a, _, _)) = a;
   3.144 -fun gt0 (Rat (a, p, _)) = a andalso p > IntInf.fromInt 0;
   3.145 -
   3.146  fun roundup (r as Rat (a, p, q)) =
   3.147 -  if q = IntInf.fromInt 1 then r
   3.148 +  if q = Intt.int 1 then r
   3.149    else
   3.150      let
   3.151 -      fun round true q = Rat (true, q + IntInf.fromInt 1, IntInf.fromInt 1)
   3.152 +      fun round true q = Rat (true, q + Intt.int 1, Intt.int 1)
   3.153          | round false q =
   3.154 -            if q = IntInf.fromInt 0
   3.155 -            then Rat (true, IntInf.fromInt 0, IntInf.fromInt 1)
   3.156 -            else Rat (false, q, IntInf.fromInt 1);
   3.157 +            if q = Intt.int 0
   3.158 +            then Rat (true, Intt.int 0, Intt.int 1)
   3.159 +            else Rat (false, q, Intt.int 1);
   3.160      in round a (p div q) end;
   3.161  
   3.162  fun rounddown (r as Rat (a, p, q)) =
   3.163 -  if q = IntInf.fromInt 1 then r
   3.164 +  if q = Intt.int 1 then r
   3.165    else
   3.166      let
   3.167 -      fun round true q = Rat (true, q, IntInf.fromInt 1)
   3.168 -        | round false q = Rat (false, q + IntInf.fromInt 1, IntInf.fromInt 1)
   3.169 +      fun round true q = Rat (true, q, Intt.int 1)
   3.170 +        | round false q = Rat (false, q + Intt.int 1, Intt.int 1)
   3.171      in round a (p div q) end;
   3.172  
   3.173  end;