added more rat functions
authornipkow
Sun Aug 07 12:28:10 2005 +0200 (2005-08-07)
changeset 17028a497f621bfd4
parent 17027 8bbe57116d13
child 17029 7839e85fc246
added more rat functions
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Aug 06 18:06:56 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Aug 07 12:28:10 2005 +0200
     1.3 @@ -144,6 +144,10 @@
     1.4    type rat
     1.5    exception RAT of string
     1.6    val rep_rat: rat -> IntInf.int * IntInf.int
     1.7 +  val ratge0: rat -> bool
     1.8 +  val ratgt0: rat -> bool
     1.9 +  val ratle: rat * rat -> bool
    1.10 +  val ratlt: rat * rat -> bool
    1.11    val ratadd: rat * rat -> rat
    1.12    val ratmul: rat * rat -> rat
    1.13    val ratinv: rat -> rat
    1.14 @@ -151,6 +155,7 @@
    1.15    val ratneg: rat -> rat
    1.16    val rat_of_int: int -> rat
    1.17    val rat_of_intinf: IntInf.int -> rat
    1.18 +  val rat0: rat
    1.19  
    1.20    (*strings*)
    1.21    val nth_elem_string: int * string -> string
    1.22 @@ -1224,6 +1229,7 @@
    1.23  
    1.24  
    1.25  (** rational numbers **)
    1.26 +(* Keep them normalized! *)
    1.27  
    1.28  datatype rat = Rat of bool * IntInf.int * IntInf.int
    1.29  
    1.30 @@ -1236,9 +1242,27 @@
    1.31        val m = gcd(absp,q)
    1.32    in Rat(a = (0 <= p), absp div m, q div m) end;
    1.33  
    1.34 -fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
    1.35 +fun ratcommon(p,q,r,s) =
    1.36    let val den = lcm(q,s)
    1.37 -      val p = p*(den div q) and r = r*(den div s)
    1.38 +  in (p*(den div q), r*(den div s), den) end
    1.39 +
    1.40 +fun ratge0(Rat(a,p,q)) = a;
    1.41 +fun ratgt0(Rat(a,p,q)) = a andalso p > 0;
    1.42 +
    1.43 +fun ratle(Rat(a,p,q),Rat(b,r,s)) =
    1.44 +  not a andalso b orelse
    1.45 +  a = b andalso
    1.46 +    let val (p,r,_) = ratcommon(p,q,r,s)
    1.47 +    in if a then p <= r else r <= p end
    1.48 +
    1.49 +fun ratlt(Rat(a,p,q),Rat(b,r,s)) =
    1.50 +  not a andalso b orelse
    1.51 +  a = b andalso
    1.52 +    let val (p,r,_) = ratcommon(p,q,r,s)
    1.53 +    in if a then p < r else r < p end
    1.54 +
    1.55 +fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
    1.56 +  let val (p,q,den) = ratcommon(p,q,r,s)
    1.57        val num = (if a then p else ~p) + (if b then r else ~r)
    1.58    in ratnorm(true,num,den) end;
    1.59  
    1.60 @@ -1255,6 +1279,7 @@
    1.61  
    1.62  fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
    1.63  
    1.64 +val rat0 = rat_of_int 0; 
    1.65  
    1.66  (** misc **)
    1.67