# HG changeset patch # User haftmann # Date 1181049422 -7200 # Node ID 471b576aad25ae019e296a8baee482f741f7205e # Parent 9886802cbbd67dd0d8eb2c89d0929b63d72e1c82 moved generic algebra modules diff -r 9886802cbbd6 -r 471b576aad25 NEWS --- a/NEWS Tue Jun 05 15:16:11 2007 +0200 +++ b/NEWS Tue Jun 05 15:17:02 2007 +0200 @@ -738,8 +738,7 @@ * Renamed constants "0" to "HOL.zero_class.zero" and "1" to "HOL.one_class.one". INCOMPATIBILITY. -* Added theory Code_Generator providing class 'eq', allowing for code -generation with polymorphic equality. +* Added class "HOL.eq", allowing for code generation with polymorphic equality. * Numeral syntax: type 'bin' which was a mere type copy of 'int' has been abandoned in favour of plain 'int'. INCOMPATIBILITY -- @@ -952,6 +951,8 @@ *** ML *** +* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML + * Context data interfaces (Theory/Proof/GenericDataFun): removed name/print, uninitialized data defaults to ad-hoc copy of empty value, init only required for impure data. INCOMPATIBILITY: empty really diff -r 9886802cbbd6 -r 471b576aad25 src/HOL/Real/Float.thy --- a/src/HOL/Real/Float.thy Tue Jun 05 15:16:11 2007 +0200 +++ b/src/HOL/Real/Float.thy Tue Jun 05 15:17:02 2007 +0200 @@ -7,7 +7,7 @@ theory Float imports Real Parity -uses "~~/src/Pure/General/float.ML" ("float_arith.ML") +uses "~~/src/Tools/float.ML" ("float_arith.ML") begin definition diff -r 9886802cbbd6 -r 471b576aad25 src/Pure/General/float.ML --- a/src/Pure/General/float.ML Tue Jun 05 15:16:11 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -(* Title: Pure/General/float.ML - ID: $Id$ - Author: Steven Obua, Florian Haftmann, TU Muenchen - -Implementation of real numbers as mantisse-exponent pairs. -*) - -signature FLOAT = -sig - type float = Intt.int * Intt.int - val zero: float - val eq: float * float -> bool - val cmp: float * float -> order - val cmp_zero: float -> order - val min: float -> float -> float - val max: float -> float -> float - val add: float -> float -> float - val sub: float -> float -> float - val neg: float -> float - val mult: float -> float -> float - val positive_part: float -> float - val negative_part: float -> float -end; - -structure Float : FLOAT = -struct - -type float = Intt.int * Intt.int; - -val zero = (Intt.zero, Intt.zero); - -fun add (a1, b1) (a2, b2) = - if Intt.cmp (b1, b2) = LESS then - (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) - else - (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); - -fun sub (a1, b1) (a2, b2) = - if Intt.cmp (b1, b2) = LESS then - (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) - else - (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); - -fun neg (a, b) = (Intt.neg a, b); - -fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2); - -fun cmp_zero (a, b) = Intt.cmp_zero a; - -fun cmp (r, s) = cmp_zero (sub r s); - -fun eq (r, s) = cmp (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 positive_part (a, b) = (Intt.max Intt.zero a, b); -fun negative_part (a, b) = (Intt.min Intt.zero a, b); - -end; diff -r 9886802cbbd6 -r 471b576aad25 src/Pure/General/int.ML --- a/src/Pure/General/int.ML Tue Jun 05 15:16:11 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -(* Title: Pure/General/int.ML - ID: $Id$ - Author: Florian Haftmann, TU Muenchen - -Unbounded integers. -*) - -signature INTT = -sig - type int - val zero: int - val one: int - val two: int - val int: Int.int -> int - val machine_int: int -> Int.int - val string_of_int: int -> string - val int_of_string: string -> int option - val eq: int * int -> bool - val cmp: int * int -> order - val le: int -> int -> bool - val cmp_zero: int -> order - val min: int -> int -> int - val max: int -> int -> int - val inc: int -> int - val add: int -> int -> int - val sub: int -> int -> int - val mult: int -> int -> int - val divmod: int -> int -> int * int - val div: int -> int -> int - val mod: int -> int -> int - val neg: int -> int - val exp: int -> int - val log: int -> int - val pow: int -> int -> int (* exponent -> base -> result *) -end; - -structure Intt: INTT = -struct - -open IntInf; - -val int = fromInt; - -val zero = int 0; -val one = int 1; -val two = int 2; - -val machine_int = toInt; -val string_of_int = toString; -val int_of_string = fromString; - -val eq = op = : int * int -> bool; -val cmp = compare; -val le = curry (op <=); -val cmp_zero = curry cmp zero; - -val min = curry min; -val max = curry max; - -val inc = curry (op +) one; - -val add = curry (op +); -val sub = curry (op -); -val mult = curry ( op * ); -val divmod = curry divMod; -nonfix div val div = curry div; -nonfix mod val mod = curry mod; -val neg = ~; - -fun pow k l = - let - fun pw 0 = 1 - | pw k = mult l (pw (sub k 1)); - in if k < zero - then error "pow: negative exponent" - else pw k - end; - -fun exp k = pow k two; -val log = int o log2; - -end; diff -r 9886802cbbd6 -r 471b576aad25 src/Pure/General/rat.ML --- a/src/Pure/General/rat.ML Tue Jun 05 15:16:11 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,140 +0,0 @@ -(* Title: Pure/General/rat.ML - ID: $Id$ - Author: Tobias Nipkow, TU Muenchen - -Canonical implementation of exact rational numbers. -*) - -signature RAT = -sig - type rat - exception DIVZERO - val zero: rat - val one: rat - 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 cmp: rat * rat -> order - val le: rat -> rat -> bool - val lt: 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 roundup: rat -> rat - val rounddown: rat -> rat -end; - -structure Rat : RAT = -struct - -datatype rat = Rat of bool * Intt.int * Intt.int; - -exception DIVZERO; - -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_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 = 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 = (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 = 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 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 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 Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end; - -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 cmp_zero (Rat (false, _, _)) = LESS - | cmp_zero (Rat (_, 0, _)) = EQUAL - | cmp_zero (Rat (_, _, _)) = GREATER; - -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)) = - norm (a1=a2, p1*p2, q1*q2); - -fun neg (r as Rat (b, p, q)) = - if p = Intt.int 0 then r - else Rat (not b, p, q); - -fun inv (Rat (a, p, q)) = - if p = Intt.int 0 then raise DIVZERO - else Rat (a, q, p); - -fun roundup (r as Rat (a, p, q)) = - if q = Intt.int 1 then r - else - let - fun round true q = Rat (true, q + Intt.int 1, Intt.int 1) - | round false q = - 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 = Intt.int 1 then r - else - let - 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; - -infix 5 +/; -infix 5 -/; -infix 7 */; -infix 7 //; -infix 4 =/ / >=/ <>/; - -fun a +/ b = Rat.add a b; -fun a -/ b = a +/ Rat.neg b; -fun a */ b = Rat.mult a b; -fun a // b = a */ Rat.inv b; -fun a =/ b = Rat.eq (a,b); -fun a / b = b =/ b = b <=/ a; -fun a <>/ b = not (a =/ b); diff -r 9886802cbbd6 -r 471b576aad25 src/Pure/library.ML --- a/src/Pure/library.ML Tue Jun 05 15:16:11 2007 +0200 +++ b/src/Pure/library.ML Tue Jun 05 15:17:02 2007 +0200 @@ -124,8 +124,6 @@ val suffixes: 'a list -> 'a list list (*integers*) - val gcd: IntInf.int * IntInf.int -> IntInf.int - val lcm: IntInf.int * IntInf.int -> IntInf.int val inc: int ref -> int val dec: int ref -> int val upto: int * int -> int list @@ -639,13 +637,6 @@ (** integers **) -fun gcd (x, y) = - let fun gxd x y : IntInf.int = - if y = IntInf.fromInt 0 then x else gxd y (x mod y) - in if x < y then gxd y x else gxd x y end; - -fun lcm (x, y) = (x * y) div gcd (x, y); - fun inc i = (i := ! i + 1; ! i); fun dec i = (i := ! i - 1; ! i); diff -r 9886802cbbd6 -r 471b576aad25 src/Tools/float.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/float.ML Tue Jun 05 15:17:02 2007 +0200 @@ -0,0 +1,60 @@ +(* Title: Pure/General/float.ML + ID: $Id$ + Author: Steven Obua, Florian Haftmann, TU Muenchen + +Implementation of real numbers as mantisse-exponent pairs. +*) + +signature FLOAT = +sig + type float = Intt.int * Intt.int + val zero: float + val eq: float * float -> bool + val cmp: float * float -> order + val cmp_zero: float -> order + val min: float -> float -> float + val max: float -> float -> float + val add: float -> float -> float + val sub: float -> float -> float + val neg: float -> float + val mult: float -> float -> float + val positive_part: float -> float + val negative_part: float -> float +end; + +structure Float : FLOAT = +struct + +type float = Intt.int * Intt.int; + +val zero = (Intt.zero, Intt.zero); + +fun add (a1, b1) (a2, b2) = + if Intt.cmp (b1, b2) = LESS then + (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) + else + (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); + +fun sub (a1, b1) (a2, b2) = + if Intt.cmp (b1, b2) = LESS then + (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) + else + (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); + +fun neg (a, b) = (Intt.neg a, b); + +fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2); + +fun cmp_zero (a, b) = Intt.cmp_zero a; + +fun cmp (r, s) = cmp_zero (sub r s); + +fun eq (r, s) = cmp (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 positive_part (a, b) = (Intt.max Intt.zero a, b); +fun negative_part (a, b) = (Intt.min Intt.zero a, b); + +end; diff -r 9886802cbbd6 -r 471b576aad25 src/Tools/integer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/integer.ML Tue Jun 05 15:17:02 2007 +0200 @@ -0,0 +1,116 @@ +(* Title: Pure/General/int.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Unbounded integers. +*) + +signature INTEGER = +sig + type int + val zero: int + val one: int + val two: int + val int: Int.int -> int + val machine_int: int -> Int.int + val string_of_int: int -> string + val int_of_string: string -> int option + val eq: int * int -> bool + val cmp: int * int -> order + val le: int -> int -> bool + val lt: int -> int -> bool + val cmp_zero: int -> order + val min: int -> int -> int + val max: int -> int -> int + val inc: int -> int + val add: int -> int -> int + val sub: int -> int -> int + val mult: int -> int -> int + val divmod: int -> int -> int * int + 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 *) + val gcd: int -> int -> int + val lcm: int -> int -> int +end; + +structure Integer : INTEGER = +struct + +open IntInf; + +val int = fromInt; + +val zero = int 0; +val one = int 1; +val two = int 2; + +val machine_int = toInt; +val string_of_int = toString; +val int_of_string = fromString; + +val eq = op = : int * int -> bool; +val cmp = compare; +val le = curry (op <=); +val lt = curry (op <); +fun cmp_zero k = cmp (k, zero); + +val min = curry min; +val max = curry max; + +val inc = curry (op +) one; + +val add = curry (op +); +val sub = curry (op -); +val mult = curry ( op * ); +val divmod = curry divMod; +nonfix div val div = curry div; +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)); + in if k < zero + then error "pow: negative exponent" + else pw k + end; + +fun exp k = pow k two; +val log = int o log2; + +fun gcd x y = + let + fun gxd x y = if y = zero then x else gxd y (mod x y) + in if lt x y then gxd y x else gxd x y end; + +fun lcm x y = div (mult x y) (gcd x y); + +end; + +type integer = Integer.int; + +infix 7 *%; +infix 6 +% -%; +infix 4 =% <% <=% >% >=% <>%; + +fun a +% b = Integer.add a b; +fun a -% b = a +% Integer.neg b; +fun a *% b = Integer.mult a b; +fun a =% b = Integer.eq (a, b); +fun a <% b = Integer.lt a b; +fun a <=% b = Integer.le a b; +fun a >% b = b <% a; +fun a >=% b = b <=% a; +fun a <>% b = not (a =% b); + +structure Intt = Integer; (*FIXME*) +val gcd = uncurry Integer.gcd; (*FIXME*) +val lcm = uncurry Integer.lcm; (*FIXME*) diff -r 9886802cbbd6 -r 471b576aad25 src/Tools/rat.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/rat.ML Tue Jun 05 15:17:02 2007 +0200 @@ -0,0 +1,140 @@ +(* Title: Pure/General/rat.ML + ID: $Id$ + Author: Tobias Nipkow, TU Muenchen + +Canonical implementation of exact rational numbers. +*) + +signature RAT = +sig + type rat + exception DIVZERO + val zero: rat + val one: rat + 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 cmp: rat * rat -> order + val le: rat -> rat -> bool + val lt: 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 roundup: rat -> rat + val rounddown: rat -> rat +end; + +structure Rat : RAT = +struct + +datatype rat = Rat of bool * Intt.int * Intt.int; + +exception DIVZERO; + +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_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 = 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 = (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 = 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 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 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 Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end; + +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 cmp_zero (Rat (false, _, _)) = LESS + | cmp_zero (Rat (_, 0, _)) = EQUAL + | cmp_zero (Rat (_, _, _)) = GREATER; + +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)) = + norm (a1=a2, p1*p2, q1*q2); + +fun neg (r as Rat (b, p, q)) = + if p = Intt.int 0 then r + else Rat (not b, p, q); + +fun inv (Rat (a, p, q)) = + if p = Intt.int 0 then raise DIVZERO + else Rat (a, q, p); + +fun roundup (r as Rat (a, p, q)) = + if q = Intt.int 1 then r + else + let + fun round true q = Rat (true, q + Intt.int 1, Intt.int 1) + | round false q = + 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 = Intt.int 1 then r + else + let + 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; + +infix 5 +/; +infix 5 -/; +infix 7 */; +infix 7 //; +infix 4 =/ / >=/ <>/; + +fun a +/ b = Rat.add a b; +fun a -/ b = a +/ Rat.neg b; +fun a */ b = Rat.mult a b; +fun a // b = a */ Rat.inv b; +fun a =/ b = Rat.eq (a,b); +fun a / b = b =/ b = b <=/ a; +fun a <>/ b = not (a =/ b);