more antiquotations;
authorwenzelm
Sat Mar 22 19:33:39 2014 +0100 (2014-03-22)
changeset 56255968667bbb8d2
parent 56254 a2dd9200854d
child 56256 1e01c159e7d9
more antiquotations;
clarified file location;
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Matrix_LP/float_arith.ML
src/HOL/Tools/float_arith.ML
     1.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Mar 22 18:19:57 2014 +0100
     1.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Mar 22 19:33:39 2014 +0100
     1.3 @@ -239,6 +239,6 @@
     1.4  lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
     1.5    nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
     1.6  
     1.7 -ML_file "~~/src/HOL/Tools/float_arith.ML"
     1.8 +ML_file "float_arith.ML"
     1.9  
    1.10  end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Matrix_LP/float_arith.ML	Sat Mar 22 19:33:39 2014 +0100
     2.3 @@ -0,0 +1,221 @@
     2.4 +(*  Title:      HOL/Matrix_LP/float_arith.ML
     2.5 +    Author:     Steven Obua
     2.6 +*)
     2.7 +
     2.8 +signature FLOAT_ARITH =
     2.9 +sig
    2.10 +  exception Destruct_floatstr of string
    2.11 +  val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
    2.12 +
    2.13 +  exception Floating_point of string
    2.14 +  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
    2.15 +  val approx_decstr_by_bin: int -> string -> Float.float * Float.float
    2.16 +
    2.17 +  val mk_float: Float.float -> term
    2.18 +  val dest_float: term -> Float.float
    2.19 +
    2.20 +  val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
    2.21 +    -> string -> term * term
    2.22 +end;
    2.23 +
    2.24 +structure FloatArith : FLOAT_ARITH =
    2.25 +struct
    2.26 +
    2.27 +exception Destruct_floatstr of string;
    2.28 +
    2.29 +fun destruct_floatstr isDigit isExp number =
    2.30 +  let
    2.31 +    val numlist = filter (not o Char.isSpace) (String.explode number)
    2.32 +
    2.33 +    fun countsigns ((#"+")::cs) = countsigns cs
    2.34 +      | countsigns ((#"-")::cs) =
    2.35 +      let
    2.36 +        val (positive, rest) = countsigns cs
    2.37 +      in
    2.38 +        (not positive, rest)
    2.39 +      end
    2.40 +      | countsigns cs = (true, cs)
    2.41 +
    2.42 +    fun readdigits [] = ([], [])
    2.43 +      | readdigits (q as c::cs) =
    2.44 +      if (isDigit c) then
    2.45 +        let
    2.46 +          val (digits, rest) = readdigits cs
    2.47 +        in
    2.48 +          (c::digits, rest)
    2.49 +        end
    2.50 +      else
    2.51 +        ([], q)
    2.52 +
    2.53 +    fun readfromexp_helper cs =
    2.54 +      let
    2.55 +        val (positive, rest) = countsigns cs
    2.56 +        val (digits, rest') = readdigits rest
    2.57 +      in
    2.58 +        case rest' of
    2.59 +          [] => (positive, digits)
    2.60 +          | _ => raise (Destruct_floatstr number)
    2.61 +      end
    2.62 +
    2.63 +    fun readfromexp [] = (true, [])
    2.64 +      | readfromexp (c::cs) =
    2.65 +      if isExp c then
    2.66 +        readfromexp_helper cs
    2.67 +      else
    2.68 +        raise (Destruct_floatstr number)
    2.69 +
    2.70 +    fun readfromdot [] = ([], readfromexp [])
    2.71 +      | readfromdot ((#".")::cs) =
    2.72 +      let
    2.73 +        val (digits, rest) = readdigits cs
    2.74 +        val exp = readfromexp rest
    2.75 +      in
    2.76 +        (digits, exp)
    2.77 +      end
    2.78 +      | readfromdot cs = readfromdot ((#".")::cs)
    2.79 +
    2.80 +    val (positive, numlist) = countsigns numlist
    2.81 +    val (digits1, numlist) = readdigits numlist
    2.82 +     val (digits2, exp) = readfromdot numlist
    2.83 +  in
    2.84 +    (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
    2.85 +  end
    2.86 +
    2.87 +exception Floating_point of string;
    2.88 +
    2.89 +val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
    2.90 +fun exp5 x = Integer.pow x 5;
    2.91 +fun exp10 x = Integer.pow x 10;
    2.92 +fun exp2 x = Integer.pow x 2;
    2.93 +
    2.94 +fun find_most_significant q r =
    2.95 +  let
    2.96 +    fun int2real i =
    2.97 +      case (Real.fromString o string_of_int) i of
    2.98 +        SOME r => r
    2.99 +        | NONE => raise (Floating_point "int2real")
   2.100 +    fun subtract (q, r) (q', r') =
   2.101 +      if r <= r' then
   2.102 +        (q - q' * exp10 (r' - r), r)
   2.103 +      else
   2.104 +        (q * exp10 (r - r') - q', r')
   2.105 +    fun bin2dec d =
   2.106 +      if 0 <= d then
   2.107 +        (exp2 d, 0)
   2.108 +      else
   2.109 +        (exp5 (~ d), d)
   2.110 +
   2.111 +    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
   2.112 +    val L1 = L + 1
   2.113 +
   2.114 +    val (q1, r1) = subtract (q, r) (bin2dec L1) 
   2.115 +  in
   2.116 +    if 0 <= q1 then
   2.117 +      let
   2.118 +        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
   2.119 +      in
   2.120 +        if 0 <= q2 then
   2.121 +          raise (Floating_point "find_most_significant")
   2.122 +        else
   2.123 +          (L1, (q1, r1))
   2.124 +      end
   2.125 +    else
   2.126 +      let
   2.127 +        val (q0, r0) = subtract (q, r) (bin2dec L)
   2.128 +      in
   2.129 +        if 0 <= q0 then
   2.130 +          (L, (q0, r0))
   2.131 +        else
   2.132 +          raise (Floating_point "find_most_significant")
   2.133 +      end
   2.134 +  end
   2.135 +
   2.136 +fun approx_dec_by_bin n (q,r) =
   2.137 +  let
   2.138 +    fun addseq acc d' [] = acc
   2.139 +      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
   2.140 +
   2.141 +    fun seq2bin [] = (0, 0)
   2.142 +      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
   2.143 +
   2.144 +    fun approx d_seq d0 precision (q,r) =
   2.145 +      if q = 0 then
   2.146 +        let val x = seq2bin d_seq in
   2.147 +          (x, x)
   2.148 +        end
   2.149 +      else
   2.150 +        let
   2.151 +          val (d, (q', r')) = find_most_significant q r
   2.152 +        in
   2.153 +          if precision < d0 - d then
   2.154 +            let
   2.155 +              val d' = d0 - precision
   2.156 +              val x1 = seq2bin (d_seq)
   2.157 +              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
   2.158 +            in
   2.159 +              (x1, x2)
   2.160 +            end
   2.161 +          else
   2.162 +            approx (d::d_seq) d0 precision (q', r')
   2.163 +        end
   2.164 +
   2.165 +    fun approx_start precision (q, r) =
   2.166 +      if q = 0 then
   2.167 +        ((0, 0), (0, 0))
   2.168 +      else
   2.169 +        let
   2.170 +          val (d, (q', r')) = find_most_significant q r
   2.171 +        in
   2.172 +          if precision <= 0 then
   2.173 +            let
   2.174 +              val x1 = seq2bin [d]
   2.175 +            in
   2.176 +              if q' = 0 then
   2.177 +                (x1, x1)
   2.178 +              else
   2.179 +                (x1, seq2bin [d + 1])
   2.180 +            end
   2.181 +          else
   2.182 +            approx [d] d precision (q', r')
   2.183 +        end
   2.184 +  in
   2.185 +    if 0 <= q then
   2.186 +      approx_start n (q,r)
   2.187 +    else
   2.188 +      let
   2.189 +        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
   2.190 +      in
   2.191 +        ((~ a2, b2), (~ a1, b1))
   2.192 +      end
   2.193 +  end
   2.194 +
   2.195 +fun approx_decstr_by_bin n decstr =
   2.196 +  let
   2.197 +    fun str2int s = the_default 0 (Int.fromString s)
   2.198 +    fun signint p x = if p then x else ~ x
   2.199 +
   2.200 +    val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
   2.201 +    val s = size d2
   2.202 +
   2.203 +    val q = signint p (str2int d1 * exp10 s + str2int d2)
   2.204 +    val r = signint ep (str2int e) - s
   2.205 +  in
   2.206 +    approx_dec_by_bin n (q,r)
   2.207 +  end
   2.208 +
   2.209 +fun mk_float (a, b) = @{term "float"} $
   2.210 +  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
   2.211 +
   2.212 +fun dest_float (Const (@{const_name float}, _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
   2.213 +      pairself (snd o HOLogic.dest_number) (a, b)
   2.214 +  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
   2.215 +
   2.216 +fun approx_float prec f value =
   2.217 +  let
   2.218 +    val interval = approx_decstr_by_bin prec value
   2.219 +    val (flower, fupper) = f interval
   2.220 +  in
   2.221 +    (mk_float flower, mk_float fupper)
   2.222 +  end;
   2.223 +
   2.224 +end;
     3.1 --- a/src/HOL/Tools/float_arith.ML	Sat Mar 22 18:19:57 2014 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,221 +0,0 @@
     3.4 -(*  Title:  HOL/Tools/float_arith.ML
     3.5 -    Author: Steven Obua
     3.6 -*)
     3.7 -
     3.8 -signature FLOAT_ARITH =
     3.9 -sig
    3.10 -  exception Destruct_floatstr of string
    3.11 -  val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
    3.12 -
    3.13 -  exception Floating_point of string
    3.14 -  val approx_dec_by_bin: int -> Float.float -> Float.float * Float.float
    3.15 -  val approx_decstr_by_bin: int -> string -> Float.float * Float.float
    3.16 -
    3.17 -  val mk_float: Float.float -> term
    3.18 -  val dest_float: term -> Float.float
    3.19 -
    3.20 -  val approx_float: int -> (Float.float * Float.float -> Float.float * Float.float)
    3.21 -    -> string -> term * term
    3.22 -end;
    3.23 -
    3.24 -structure FloatArith : FLOAT_ARITH =
    3.25 -struct
    3.26 -
    3.27 -exception Destruct_floatstr of string;
    3.28 -
    3.29 -fun destruct_floatstr isDigit isExp number =
    3.30 -  let
    3.31 -    val numlist = filter (not o Char.isSpace) (String.explode number)
    3.32 -
    3.33 -    fun countsigns ((#"+")::cs) = countsigns cs
    3.34 -      | countsigns ((#"-")::cs) =
    3.35 -      let
    3.36 -        val (positive, rest) = countsigns cs
    3.37 -      in
    3.38 -        (not positive, rest)
    3.39 -      end
    3.40 -      | countsigns cs = (true, cs)
    3.41 -
    3.42 -    fun readdigits [] = ([], [])
    3.43 -      | readdigits (q as c::cs) =
    3.44 -      if (isDigit c) then
    3.45 -        let
    3.46 -          val (digits, rest) = readdigits cs
    3.47 -        in
    3.48 -          (c::digits, rest)
    3.49 -        end
    3.50 -      else
    3.51 -        ([], q)
    3.52 -
    3.53 -    fun readfromexp_helper cs =
    3.54 -      let
    3.55 -        val (positive, rest) = countsigns cs
    3.56 -        val (digits, rest') = readdigits rest
    3.57 -      in
    3.58 -        case rest' of
    3.59 -          [] => (positive, digits)
    3.60 -          | _ => raise (Destruct_floatstr number)
    3.61 -      end
    3.62 -
    3.63 -    fun readfromexp [] = (true, [])
    3.64 -      | readfromexp (c::cs) =
    3.65 -      if isExp c then
    3.66 -        readfromexp_helper cs
    3.67 -      else
    3.68 -        raise (Destruct_floatstr number)
    3.69 -
    3.70 -    fun readfromdot [] = ([], readfromexp [])
    3.71 -      | readfromdot ((#".")::cs) =
    3.72 -      let
    3.73 -        val (digits, rest) = readdigits cs
    3.74 -        val exp = readfromexp rest
    3.75 -      in
    3.76 -        (digits, exp)
    3.77 -      end
    3.78 -      | readfromdot cs = readfromdot ((#".")::cs)
    3.79 -
    3.80 -    val (positive, numlist) = countsigns numlist
    3.81 -    val (digits1, numlist) = readdigits numlist
    3.82 -     val (digits2, exp) = readfromdot numlist
    3.83 -  in
    3.84 -    (positive, String.implode digits1, String.implode digits2, fst exp, String.implode (snd exp))
    3.85 -  end
    3.86 -
    3.87 -exception Floating_point of string;
    3.88 -
    3.89 -val ln2_10 = Math.ln 10.0 / Math.ln 2.0;
    3.90 -fun exp5 x = Integer.pow x 5;
    3.91 -fun exp10 x = Integer.pow x 10;
    3.92 -fun exp2 x = Integer.pow x 2;
    3.93 -
    3.94 -fun find_most_significant q r =
    3.95 -  let
    3.96 -    fun int2real i =
    3.97 -      case (Real.fromString o string_of_int) i of
    3.98 -        SOME r => r
    3.99 -        | NONE => raise (Floating_point "int2real")
   3.100 -    fun subtract (q, r) (q', r') =
   3.101 -      if r <= r' then
   3.102 -        (q - q' * exp10 (r' - r), r)
   3.103 -      else
   3.104 -        (q * exp10 (r - r') - q', r')
   3.105 -    fun bin2dec d =
   3.106 -      if 0 <= d then
   3.107 -        (exp2 d, 0)
   3.108 -      else
   3.109 -        (exp5 (~ d), d)
   3.110 -
   3.111 -    val L = Real.floor (int2real (IntInf.log2 q) + int2real r * ln2_10)
   3.112 -    val L1 = L + 1
   3.113 -
   3.114 -    val (q1, r1) = subtract (q, r) (bin2dec L1) 
   3.115 -  in
   3.116 -    if 0 <= q1 then
   3.117 -      let
   3.118 -        val (q2, r2) = subtract (q, r) (bin2dec (L1 + 1))
   3.119 -      in
   3.120 -        if 0 <= q2 then
   3.121 -          raise (Floating_point "find_most_significant")
   3.122 -        else
   3.123 -          (L1, (q1, r1))
   3.124 -      end
   3.125 -    else
   3.126 -      let
   3.127 -        val (q0, r0) = subtract (q, r) (bin2dec L)
   3.128 -      in
   3.129 -        if 0 <= q0 then
   3.130 -          (L, (q0, r0))
   3.131 -        else
   3.132 -          raise (Floating_point "find_most_significant")
   3.133 -      end
   3.134 -  end
   3.135 -
   3.136 -fun approx_dec_by_bin n (q,r) =
   3.137 -  let
   3.138 -    fun addseq acc d' [] = acc
   3.139 -      | addseq acc d' (d::ds) = addseq (acc + exp2 (d - d')) d' ds
   3.140 -
   3.141 -    fun seq2bin [] = (0, 0)
   3.142 -      | seq2bin (d::ds) = (addseq 0 d ds + 1, d)
   3.143 -
   3.144 -    fun approx d_seq d0 precision (q,r) =
   3.145 -      if q = 0 then
   3.146 -        let val x = seq2bin d_seq in
   3.147 -          (x, x)
   3.148 -        end
   3.149 -      else
   3.150 -        let
   3.151 -          val (d, (q', r')) = find_most_significant q r
   3.152 -        in
   3.153 -          if precision < d0 - d then
   3.154 -            let
   3.155 -              val d' = d0 - precision
   3.156 -              val x1 = seq2bin (d_seq)
   3.157 -              val x2 = (fst x1 * exp2 (snd x1 - d') + 1,  d') (* = seq2bin (d'::d_seq) *)
   3.158 -            in
   3.159 -              (x1, x2)
   3.160 -            end
   3.161 -          else
   3.162 -            approx (d::d_seq) d0 precision (q', r')
   3.163 -        end
   3.164 -
   3.165 -    fun approx_start precision (q, r) =
   3.166 -      if q = 0 then
   3.167 -        ((0, 0), (0, 0))
   3.168 -      else
   3.169 -        let
   3.170 -          val (d, (q', r')) = find_most_significant q r
   3.171 -        in
   3.172 -          if precision <= 0 then
   3.173 -            let
   3.174 -              val x1 = seq2bin [d]
   3.175 -            in
   3.176 -              if q' = 0 then
   3.177 -                (x1, x1)
   3.178 -              else
   3.179 -                (x1, seq2bin [d + 1])
   3.180 -            end
   3.181 -          else
   3.182 -            approx [d] d precision (q', r')
   3.183 -        end
   3.184 -  in
   3.185 -    if 0 <= q then
   3.186 -      approx_start n (q,r)
   3.187 -    else
   3.188 -      let
   3.189 -        val ((a1,b1), (a2, b2)) = approx_start n (~ q, r)
   3.190 -      in
   3.191 -        ((~ a2, b2), (~ a1, b1))
   3.192 -      end
   3.193 -  end
   3.194 -
   3.195 -fun approx_decstr_by_bin n decstr =
   3.196 -  let
   3.197 -    fun str2int s = the_default 0 (Int.fromString s)
   3.198 -    fun signint p x = if p then x else ~ x
   3.199 -
   3.200 -    val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr
   3.201 -    val s = size d2
   3.202 -
   3.203 -    val q = signint p (str2int d1 * exp10 s + str2int d2)
   3.204 -    val r = signint ep (str2int e) - s
   3.205 -  in
   3.206 -    approx_dec_by_bin n (q,r)
   3.207 -  end
   3.208 -
   3.209 -fun mk_float (a, b) = @{term "float"} $
   3.210 -  HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
   3.211 -
   3.212 -fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
   3.213 -      pairself (snd o HOLogic.dest_number) (a, b)
   3.214 -  | dest_float t = ((snd o HOLogic.dest_number) t, 0);
   3.215 -
   3.216 -fun approx_float prec f value =
   3.217 -  let
   3.218 -    val interval = approx_decstr_by_bin prec value
   3.219 -    val (flower, fupper) = f interval
   3.220 -  in
   3.221 -    (mk_float flower, mk_float fupper)
   3.222 -  end;
   3.223 -
   3.224 -end;