simplified type integer;
authorwenzelm
Sat Jun 09 00:28:46 2007 +0200 (2007-06-09)
changeset 2329706f108974fa1
parent 23296 25f28f9c28a3
child 23298 404988d8b1e0
simplified type integer;
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/Real/float_arith.ML
src/HOL/hologic.ML
src/Provers/Arith/fast_lin_arith.ML
src/Tools/float.ML
src/Tools/rat.ML
     1.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Fri Jun 08 18:13:58 2007 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Sat Jun 09 00:28:46 2007 +0200
     1.3 @@ -207,8 +207,8 @@
     1.4  
     1.5          fun test_1 (lower, upper) =
     1.6              if lower = upper then
     1.7 -                (if Float.eq (lower, (Integer.int ~1, Integer.zero)) then ~1
     1.8 -                 else if Float.eq (lower, (Integer.int 1, Integer.zero)) then 1
     1.9 +                (if Float.eq (lower, (~1, 0)) then ~1
    1.10 +                 else if Float.eq (lower, (1, 0)) then 1
    1.11                   else 0)
    1.12              else 0
    1.13  
     2.1 --- a/src/HOL/Real/float_arith.ML	Fri Jun 08 18:13:58 2007 +0200
     2.2 +++ b/src/HOL/Real/float_arith.ML	Sat Jun 09 00:28:46 2007 +0200
     2.3 @@ -85,11 +85,8 @@
     2.4  exception Floating_point of string;
     2.5  
     2.6  val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
     2.7 -val exp5 = Integer.pow (Integer.int 5);
     2.8 -val exp10 = Integer.pow (Integer.int 10);
     2.9 -
    2.10 -fun intle a b = not (Integer.cmp (a, b) = GREATER);
    2.11 -fun intless a b = Integer.cmp (a, b) = LESS;
    2.12 +val exp5 = Integer.pow 5;
    2.13 +val exp10 = Integer.pow 10;
    2.14  
    2.15  fun find_most_significant q r =
    2.16    let
    2.17 @@ -98,26 +95,26 @@
    2.18          SOME r => r
    2.19          | NONE => raise (Floating_point "int2real")
    2.20      fun subtract (q, r) (q', r') =
    2.21 -      if intle r r' then
    2.22 -        (Integer.sub q (Integer.mult q' (exp10 (Integer.sub r' r))), r)
    2.23 +      if r <=% r' then
    2.24 +        (q - q' * exp10 (r' - r), r)
    2.25        else
    2.26 -        (Integer.sub (Integer.mult q (exp10 (Integer.sub r r'))) q', r')
    2.27 +        (q * exp10 (r - r') - q', r')
    2.28      fun bin2dec d =
    2.29 -      if intle Integer.zero d then
    2.30 -        (Integer.exp d, Integer.zero)
    2.31 +      if 0 <=% d then
    2.32 +        (Integer.exp d, 0)
    2.33        else
    2.34 -        (exp5 (Integer.neg d), d)
    2.35 +        (exp5 (~ d), d)
    2.36  
    2.37      val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10))
    2.38 -    val L1 = Integer.inc L
    2.39 +    val L1 = L + 1
    2.40  
    2.41      val (q1, r1) = subtract (q, r) (bin2dec L1) 
    2.42    in
    2.43 -    if intle Integer.zero q1 then
    2.44 +    if 0 <=% q1 then
    2.45        let
    2.46 -        val (q2, r2) = subtract (q, r) (bin2dec (Integer.inc L1))
    2.47 +        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
    2.48        in
    2.49 -        if intle Integer.zero q2 then
    2.50 +        if 0 <=% q2 then
    2.51            raise (Floating_point "find_most_significant")
    2.52          else
    2.53            (L1, (q1, r1))
    2.54 @@ -126,7 +123,7 @@
    2.55        let
    2.56          val (q0, r0) = subtract (q, r) (bin2dec L)
    2.57        in
    2.58 -        if intle Integer.zero q0 then
    2.59 +        if 0 <=% q0 then
    2.60            (L, (q0, r0))
    2.61          else
    2.62            raise (Floating_point "find_most_significant")
    2.63 @@ -136,13 +133,13 @@
    2.64  fun approx_dec_by_bin n (q,r) =
    2.65    let
    2.66      fun addseq acc d' [] = acc
    2.67 -      | addseq acc d' (d::ds) = addseq (Integer.add acc (Integer.exp (Integer.sub d d'))) d' ds
    2.68 +      | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds
    2.69  
    2.70 -    fun seq2bin [] = (Integer.zero, Integer.zero)
    2.71 -      | seq2bin (d::ds) = (Integer.inc (addseq Integer.zero d ds), d)
    2.72 +    fun seq2bin [] = (0, 0)
    2.73 +      | seq2bin (d::ds) = (addseq 0 d ds +% 1, d)
    2.74  
    2.75      fun approx d_seq d0 precision (q,r) =
    2.76 -      if q = Integer.zero then
    2.77 +      if q = 0 then
    2.78          let val x = seq2bin d_seq in
    2.79            (x, x)
    2.80          end
    2.81 @@ -150,13 +147,11 @@
    2.82          let
    2.83            val (d, (q', r')) = find_most_significant q r
    2.84          in
    2.85 -          if intless precision (Integer.sub d0 d) then
    2.86 +          if precision <% d0 - d then
    2.87              let
    2.88 -              val d' = Integer.sub d0 precision
    2.89 +              val d' = d0 - precision
    2.90                val x1 = seq2bin (d_seq)
    2.91 -              val x2 = (Integer.inc
    2.92 -                (Integer.mult (fst x1)
    2.93 -                (Integer.exp (Integer.sub (snd x1) d'))),  d') (* = seq2bin (d'::d_seq) *)
    2.94 +              val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
    2.95              in
    2.96                (x1, x2)
    2.97              end
    2.98 @@ -165,45 +160,45 @@
    2.99          end
   2.100  
   2.101      fun approx_start precision (q, r) =
   2.102 -      if q = Integer.zero then
   2.103 -        ((Integer.zero, Integer.zero), (Integer.zero, Integer.zero))
   2.104 +      if q =% 0 then
   2.105 +        ((0, 0), (0, 0))
   2.106        else
   2.107          let
   2.108            val (d, (q', r')) = find_most_significant q r
   2.109          in
   2.110 -          if intle precision Integer.zero then
   2.111 +          if precision <=% 0 then
   2.112              let
   2.113                val x1 = seq2bin [d]
   2.114              in
   2.115 -              if q' = Integer.zero then
   2.116 +              if q' = 0 then
   2.117                  (x1, x1)
   2.118                else
   2.119 -                (x1, seq2bin [Integer.inc d])
   2.120 +                (x1, seq2bin [d +% 1])
   2.121              end
   2.122            else
   2.123              approx [d] d precision (q', r')
   2.124          end
   2.125    in
   2.126 -    if intle Integer.zero q then
   2.127 +    if 0 <=% q then
   2.128        approx_start n (q,r)
   2.129      else
   2.130        let
   2.131 -        val ((a1,b1), (a2, b2)) = approx_start n (Integer.neg q, r)
   2.132 +        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
   2.133        in
   2.134 -        ((Integer.neg a2, b2), (Integer.neg a1, b1))
   2.135 +        ((~ a2, b2), (~ a1, b1))
   2.136        end
   2.137    end
   2.138  
   2.139  fun approx_decstr_by_bin n decstr =
   2.140    let
   2.141 -    fun str2int s = the_default Integer.zero (Integer.int_of_string s);
   2.142 +    fun str2int s = the_default 0 (Integer.int_of_string s);
   2.143      fun signint p x = if p then x else Integer.neg x
   2.144  
   2.145      val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
   2.146      val s = Integer.int (size d2)
   2.147  
   2.148 -    val q = signint p (Integer.add (Integer.mult (str2int d1) (exp10 s)) (str2int d2))
   2.149 -    val r = Integer.sub (signint ep (str2int e)) s
   2.150 +    val q = signint p (str2int d1 * exp10 s + str2int d2)
   2.151 +    val r = signint ep (str2int e) - s
   2.152    in
   2.153      approx_dec_by_bin (Integer.int n) (q,r)
   2.154    end
   2.155 @@ -213,7 +208,7 @@
   2.156  
   2.157  fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
   2.158        pairself (snd o HOLogic.dest_number) (a, b)
   2.159 -  | dest_float t = ((snd o HOLogic.dest_number) t, Integer.zero);
   2.160 +  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
   2.161  
   2.162  fun approx_float prec f value =
   2.163    let
     3.1 --- a/src/HOL/hologic.ML	Fri Jun 08 18:13:58 2007 +0200
     3.2 +++ b/src/HOL/hologic.ML	Sat Jun 09 00:28:46 2007 +0200
     3.3 @@ -295,17 +295,14 @@
     3.4  
     3.5  val Suc_zero = mk_Suc zero;
     3.6  
     3.7 -fun mk_nat n =
     3.8 +fun mk_nat (n: integer) =
     3.9    let
    3.10      fun mk 0 = zero
    3.11 -      | mk n = mk_Suc (mk (n -% 1));
    3.12 -  in if n < 0
    3.13 -    then error "mk_nat: negative numeral"
    3.14 -    else mk n
    3.15 -  end;
    3.16 +      | mk n = mk_Suc (mk (n - 1));
    3.17 +  in if n < 0 then raise TERM ("mk_nat: negative numeral", []) else mk n end;
    3.18  
    3.19 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = Integer.zero
    3.20 -  | dest_nat (Const ("Suc", _) $ t) = Integer.inc (dest_nat t)
    3.21 +fun dest_nat (Const ("HOL.zero_class.zero", _)) = (0: integer)
    3.22 +  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
    3.23    | dest_nat t = raise TERM ("dest_nat", [t]);
    3.24  
    3.25  val class_size = "Nat.size";
    3.26 @@ -346,7 +343,7 @@
    3.27  fun dest_numeral (Const ("Numeral.Pls", _)) = 0
    3.28    | dest_numeral (Const ("Numeral.Min", _)) = ~1
    3.29    | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) =
    3.30 -      2 *% dest_numeral bs +% Integer.int (dest_bit b)
    3.31 +      2 * dest_numeral bs + Integer.int (dest_bit b)
    3.32    | dest_numeral t = raise TERM ("dest_numeral", [t]);
    3.33  
    3.34  fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
     4.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 08 18:13:58 2007 +0200
     4.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Jun 09 00:28:46 2007 +0200
     4.3 @@ -499,9 +499,9 @@
     4.4  end;
     4.5  
     4.6  fun coeff poly atom =
     4.7 -  AList.lookup (op =) poly atom |> the_default Integer.zero;
     4.8 +  AList.lookup (op =) poly atom |> the_default (0: integer);
     4.9  
    4.10 -fun lcms ks = fold Integer.lcm ks Integer.one;
    4.11 +fun lcms ks = fold Integer.lcm ks 1;
    4.12  
    4.13  fun integ(rlhs,r,rel,rrhs,s,d) =
    4.14  let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
     5.1 --- a/src/Tools/float.ML	Fri Jun 08 18:13:58 2007 +0200
     5.2 +++ b/src/Tools/float.ML	Sat Jun 09 00:28:46 2007 +0200
     5.3 @@ -27,7 +27,7 @@
     5.4  
     5.5  type float = integer * integer;
     5.6  
     5.7 -val zero = (Integer.zero, Integer.zero);
     5.8 +val zero: float = (0, 0);
     5.9  
    5.10  fun add (a1, b1) (a2, b2) =
    5.11    if Integer.cmp (b1, b2) = LESS then
    5.12 @@ -54,7 +54,7 @@
    5.13  fun min r s = case cmp (r, s) of LESS => r | _ => s;
    5.14  fun max r s = case cmp (r, s) of LESS => s | _ => r;
    5.15  
    5.16 -fun positive_part (a, b) = (Integer.max Integer.zero a, b);
    5.17 -fun negative_part (a, b) = (Integer.min Integer.zero a, b);
    5.18 +fun positive_part (a, b) = (Integer.max 0 a, b);
    5.19 +fun negative_part (a, b) = (Integer.min 0 a, b);
    5.20  
    5.21  end;
     6.1 --- a/src/Tools/rat.ML	Fri Jun 08 18:13:58 2007 +0200
     6.2 +++ b/src/Tools/rat.ML	Sat Jun 09 00:28:46 2007 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  
     6.5  signature RAT =
     6.6  sig
     6.7 -  type rat
     6.8 +  eqtype rat
     6.9    exception DIVZERO
    6.10    val zero: rat
    6.11    val one: rat
    6.12 @@ -36,37 +36,37 @@
    6.13  
    6.14  exception DIVZERO;
    6.15  
    6.16 -val zero = Rat (true, Integer.zero, Integer.one);
    6.17 -val one = Rat (true, Integer.one, Integer.one);
    6.18 -val two = Rat (true, Integer.two, Integer.one);
    6.19 +val zero = Rat (true, 0, 1);
    6.20 +val one = Rat (true, 1, 1);
    6.21 +val two = Rat (true, 2, 1);
    6.22  
    6.23  fun rat_of_int i =
    6.24    let
    6.25      val (a, p) = Integer.signabs i
    6.26 -  in Rat (a, p, Integer.one) end;
    6.27 +  in Rat (a, p, 1) end;
    6.28  
    6.29  fun norm (a, p, q) =
    6.30 -  if Integer.cmp_zero p = EQUAL then Rat (true, Integer.zero, Integer.one)
    6.31 +  if p = 0 then Rat (true, 0, 1)
    6.32    else
    6.33      let
    6.34        val (b, absp) = Integer.signabs p;
    6.35        val m = Integer.gcd absp q;
    6.36 -    in Rat (a = b, Integer.div absp m, Integer.div q m) end;
    6.37 +    in Rat (a = b, absp div m, q div m) end;
    6.38  
    6.39  fun common (p1, q1, p2, q2) =
    6.40    let
    6.41      val q' = Integer.lcm q1 q2;
    6.42 -  in (p1 *% (Integer.div q' q1), p2 *% (Integer.div q' q2), q') end
    6.43 +  in (p1 * (q' div q1), p2 * (q' div q2), q') end
    6.44  
    6.45  fun rat_of_quotient (p, q) =
    6.46    let
    6.47      val (a, absq) = Integer.signabs q;
    6.48    in
    6.49 -    if Integer.cmp_zero absq = EQUAL then raise DIVZERO
    6.50 +    if absq = 0 then raise DIVZERO
    6.51      else norm (a, p, absq)
    6.52    end;
    6.53  
    6.54 -fun quotient_of_rat (Rat (a, p, q)) = (if a then p else Integer.neg p, q);
    6.55 +fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~ p, q);
    6.56  
    6.57  fun string_of_rat r =
    6.58    let
    6.59 @@ -75,7 +75,7 @@
    6.60  
    6.61  fun eq (Rat (false, _, _), Rat (true, _, _)) = false
    6.62    | eq (Rat (true, _, _), Rat (false, _, _)) = false
    6.63 -  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 =% p2 andalso q1 =% q2;
    6.64 +  | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2;
    6.65  
    6.66  fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS
    6.67    | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER
    6.68 @@ -93,48 +93,48 @@
    6.69  fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) =
    6.70    let
    6.71      val (r1, r2, den) = common (p1, q1, p2, q2);
    6.72 -    val num = (if a1 then r1 else Integer.neg r1)
    6.73 -      +% (if a2 then r2 else Integer.neg r2);
    6.74 +    val num = (if a1 then r1 else ~ r1)
    6.75 +      + (if a2 then r2 else ~ r2);
    6.76    in norm (true, num, den) end;
    6.77  
    6.78  fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) =
    6.79 -  norm (a1 = a2, p1 *% p2, q1 *% q2);
    6.80 +  norm (a1 = a2, p1 * p2, q1 * q2);
    6.81  
    6.82  fun neg (r as Rat (b, p, q)) =
    6.83 -  if Integer.cmp_zero p = EQUAL then r
    6.84 +  if p = 0 then r
    6.85    else Rat (not b, p, q);
    6.86  
    6.87  fun inv (Rat (a, p, q)) =
    6.88 -  if Integer.cmp_zero q = EQUAL then raise DIVZERO
    6.89 +  if q = 0 then raise DIVZERO
    6.90    else Rat (a, q, p);
    6.91  
    6.92  fun roundup (r as Rat (a, p, q)) =
    6.93 -  if q = Integer.one then r
    6.94 +  if q = 1 then r
    6.95    else
    6.96      let
    6.97 -      fun round true q = Rat (true, Integer.inc q, Integer.one)
    6.98 +      fun round true q = Rat (true, q + 1, 1)
    6.99          | round false q =
   6.100 -            Rat (Integer.cmp_zero q = EQUAL, Integer.int 0, Integer.int 1);
   6.101 -    in round a (Integer.div p q) end;
   6.102 +            Rat (q = 0, 0, 1);
   6.103 +    in round a (p div q) end;
   6.104  
   6.105  fun rounddown (r as Rat (a, p, q)) =
   6.106 -  if q = Integer.one then r
   6.107 +  if q = 1 then r
   6.108    else
   6.109      let
   6.110 -      fun round true q = Rat (true, q, Integer.one)
   6.111 -        | round false q = Rat (false, Integer.inc q, Integer.one)
   6.112 -    in round a (Integer.div p q) end;
   6.113 +      fun round true q = Rat (true, q, 1)
   6.114 +        | round false q = Rat (false, q + 1, 1)
   6.115 +    in round a (p div q) end;
   6.116  
   6.117  end;
   6.118  
   6.119  infix 7 */ //;
   6.120 -infix 6 +/ -/; 
   6.121 +infix 6 +/ -/;
   6.122  infix 4 =/ </ <=/ >/ >=/ <>/;
   6.123  
   6.124  fun a +/ b = Rat.add a b;
   6.125  fun a -/ b = a +/ Rat.neg b;
   6.126  fun a */ b = Rat.mult a b;
   6.127 -fun a // b = a */ Rat.inv b; 
   6.128 +fun a // b = a */ Rat.inv b;
   6.129  fun a =/ b = Rat.eq (a, b);
   6.130  fun a </ b = Rat.lt a b;
   6.131  fun a <=/ b = Rat.le a b;