--- 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)
--- 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.
--- 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;