src/HOL/Real/float_arith.ML
changeset 24630 351a308ab58d
parent 24584 01e83ffa6c54
child 25300 bc3a1c964704
     1.1 --- a/src/HOL/Real/float_arith.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/HOL/Real/float_arith.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
     1.5  
     1.6    exception Floating_point of string
     1.7 -  val approx_dec_by_bin: integer -> Float.float -> Float.float * Float.float
     1.8 +  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
     1.9    val approx_decstr_by_bin: int -> string -> Float.float * Float.float
    1.10  
    1.11    val mk_float: Float.float -> term
    1.12 @@ -91,30 +91,30 @@
    1.13  fun find_most_significant q r =
    1.14    let
    1.15      fun int2real i =
    1.16 -      case (Real.fromString o Integer.string_of_int) i of
    1.17 +      case (Real.fromString o string_of_int) i of
    1.18          SOME r => r
    1.19          | NONE => raise (Floating_point "int2real")
    1.20      fun subtract (q, r) (q', r') =
    1.21 -      if r <=% r' then
    1.22 +      if r <= r' then
    1.23          (q - q' * exp10 (r' - r), r)
    1.24        else
    1.25          (q * exp10 (r - r') - q', r')
    1.26      fun bin2dec d =
    1.27 -      if 0 <=% d then
    1.28 -        (Integer.exp d, 0)
    1.29 +      if 0 <= d then
    1.30 +        (Integer.square d, 0)
    1.31        else
    1.32          (exp5 (~ d), d)
    1.33  
    1.34 -    val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10))
    1.35 +    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
    1.36      val L1 = L + 1
    1.37  
    1.38      val (q1, r1) = subtract (q, r) (bin2dec L1) 
    1.39    in
    1.40 -    if 0 <=% q1 then
    1.41 +    if 0 <= q1 then
    1.42        let
    1.43          val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
    1.44        in
    1.45 -        if 0 <=% q2 then
    1.46 +        if 0 <= q2 then
    1.47            raise (Floating_point "find_most_significant")
    1.48          else
    1.49            (L1, (q1, r1))
    1.50 @@ -123,7 +123,7 @@
    1.51        let
    1.52          val (q0, r0) = subtract (q, r) (bin2dec L)
    1.53        in
    1.54 -        if 0 <=% q0 then
    1.55 +        if 0 <= q0 then
    1.56            (L, (q0, r0))
    1.57          else
    1.58            raise (Floating_point "find_most_significant")
    1.59 @@ -133,10 +133,10 @@
    1.60  fun approx_dec_by_bin n (q,r) =
    1.61    let
    1.62      fun addseq acc d' [] = acc
    1.63 -      | addseq acc d' (d::ds) = addseq (acc +% Integer.exp (d - d')) d' ds
    1.64 +      | addseq acc d' (d::ds) = addseq (acc + Integer.square (d - d')) d' ds
    1.65  
    1.66      fun seq2bin [] = (0, 0)
    1.67 -      | seq2bin (d::ds) = (addseq 0 d ds +% 1, d)
    1.68 +      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
    1.69  
    1.70      fun approx d_seq d0 precision (q,r) =
    1.71        if q = 0 then
    1.72 @@ -147,11 +147,11 @@
    1.73          let
    1.74            val (d, (q', r')) = find_most_significant q r
    1.75          in
    1.76 -          if precision <% d0 - d then
    1.77 +          if precision < d0 - d then
    1.78              let
    1.79                val d' = d0 - precision
    1.80                val x1 = seq2bin (d_seq)
    1.81 -              val x2 = (fst x1 * Integer.exp (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
    1.82 +              val x2 = (fst x1 * Integer.square (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
    1.83              in
    1.84                (x1, x2)
    1.85              end
    1.86 @@ -160,26 +160,26 @@
    1.87          end
    1.88  
    1.89      fun approx_start precision (q, r) =
    1.90 -      if q =% 0 then
    1.91 +      if q = 0 then
    1.92          ((0, 0), (0, 0))
    1.93        else
    1.94          let
    1.95            val (d, (q', r')) = find_most_significant q r
    1.96          in
    1.97 -          if precision <=% 0 then
    1.98 +          if precision <= 0 then
    1.99              let
   1.100                val x1 = seq2bin [d]
   1.101              in
   1.102                if q' = 0 then
   1.103                  (x1, x1)
   1.104                else
   1.105 -                (x1, seq2bin [d +% 1])
   1.106 +                (x1, seq2bin [d + 1])
   1.107              end
   1.108            else
   1.109              approx [d] d precision (q', r')
   1.110          end
   1.111    in
   1.112 -    if 0 <=% q then
   1.113 +    if 0 <= q then
   1.114        approx_start n (q,r)
   1.115      else
   1.116        let
   1.117 @@ -191,16 +191,16 @@
   1.118  
   1.119  fun approx_decstr_by_bin n decstr =
   1.120    let
   1.121 -    fun str2int s = the_default 0 (Integer.int_of_string s);
   1.122 -    fun signint p x = if p then x else Integer.neg x
   1.123 +    fun str2int s = the_default 0 (Int.fromString s)
   1.124 +    fun signint p x = if p then x else ~ x
   1.125  
   1.126      val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
   1.127 -    val s = Integer.int (size d2)
   1.128 +    val s = size d2
   1.129  
   1.130      val q = signint p (str2int d1 * exp10 s + str2int d2)
   1.131      val r = signint ep (str2int e) - s
   1.132    in
   1.133 -    approx_dec_by_bin (Integer.int n) (q,r)
   1.134 +    approx_dec_by_bin n (q,r)
   1.135    end
   1.136  
   1.137  fun mk_float (a, b) = @{term "float"} $