src/HOL/Library/Float.thy
changeset 47601 050718fe6eee
parent 47600 e12289b5796b
child 47608 572d7e51de4d
     1.1 --- a/src/HOL/Library/Float.thy	Wed Apr 18 14:29:22 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Apr 19 11:55:30 2012 +0200
     1.3 @@ -8,13 +8,16 @@
     1.4    morphisms real_of_float float_of
     1.5    by auto
     1.6  
     1.7 -setup_lifting type_definition_float
     1.8 +defs (overloaded)
     1.9 +  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
    1.10 +
    1.11 +lemma type_definition_float': "type_definition real float_of float"
    1.12 +  using type_definition_float unfolding real_of_float_def .
    1.13 +
    1.14 +setup_lifting (no_code) type_definition_float'
    1.15  
    1.16  lemmas float_of_inject[simp]
    1.17  
    1.18 -defs (overloaded)
    1.19 -  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
    1.20 -
    1.21  declare [[coercion "real :: float \<Rightarrow> real"]]
    1.22  
    1.23  lemma real_of_float_eq:
    1.24 @@ -27,10 +30,6 @@
    1.25  lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
    1.26    unfolding real_of_float_def by (rule float_of_inverse)
    1.27  
    1.28 -lemma transfer_real_of_float [transfer_rule]:
    1.29 -  "(fun_rel cr_float op =) (\<lambda>x. x) real"
    1.30 -  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def)
    1.31 -
    1.32  subsection {* Real operations preserving the representation as floating point number *}
    1.33  
    1.34  lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
    1.35 @@ -124,6 +123,9 @@
    1.36  qed
    1.37  
    1.38  lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
    1.39 +declare Float.rep_eq[simp]
    1.40 +
    1.41 +code_datatype Float
    1.42  
    1.43  subsection {* Arithmetic operations on floating point numbers *}
    1.44  
    1.45 @@ -131,41 +133,34 @@
    1.46  begin
    1.47  
    1.48  lift_definition zero_float :: float is 0 by simp
    1.49 +declare zero_float.rep_eq[simp]
    1.50  lift_definition one_float :: float is 1 by simp
    1.51 +declare one_float.rep_eq[simp]
    1.52  lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
    1.53 +declare plus_float.rep_eq[simp]
    1.54  lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
    1.55 +declare times_float.rep_eq[simp]
    1.56  lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
    1.57 +declare minus_float.rep_eq[simp]
    1.58  lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
    1.59 +declare uminus_float.rep_eq[simp]
    1.60  
    1.61  lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
    1.62 +declare abs_float.rep_eq[simp]
    1.63  lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
    1.64 +declare sgn_float.rep_eq[simp]
    1.65  
    1.66  lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
    1.67  
    1.68  lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
    1.69 +declare less_eq_float.rep_eq[simp]
    1.70  lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
    1.71 +declare less_float.rep_eq[simp]
    1.72  
    1.73  instance
    1.74    proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
    1.75  end
    1.76  
    1.77 -lemma
    1.78 -  fixes x y :: float
    1.79 -  shows real_of_float_uminus[simp]: "real (- x) = - real x"
    1.80 -    and real_of_float_plus[simp]: "real (y + x) = real y + real x"
    1.81 -    and real_of_float_minus[simp]: "real (y - x) = real y - real x"
    1.82 -    and real_of_float_times[simp]: "real (y * x) = real y * real x"
    1.83 -    and real_of_float_zero[simp]: "real (0::float) = 0"
    1.84 -    and real_of_float_one[simp]: "real (1::float) = 1"
    1.85 -    and real_of_float_le[simp]: "x \<le> y \<longleftrightarrow> real x \<le> real y"
    1.86 -    and real_of_float_less[simp]: "x < y \<longleftrightarrow> real x < real y"
    1.87 -    and real_of_float_abs[simp]: "real (abs x) = abs (real x)"
    1.88 -    and real_of_float_sgn[simp]: "real (sgn x) = sgn (real x)"
    1.89 -  using uminus_float.rep_eq plus_float.rep_eq minus_float.rep_eq times_float.rep_eq
    1.90 -    zero_float.rep_eq one_float.rep_eq less_eq_float.rep_eq less_float.rep_eq
    1.91 -    abs_float.rep_eq sgn_float.rep_eq
    1.92 -  by (simp_all add: real_of_float_def)
    1.93 -
    1.94  lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
    1.95    by (induct n) simp_all
    1.96  
    1.97 @@ -213,7 +208,7 @@
    1.98    apply (induct x)
    1.99    apply simp
   1.100    apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
   1.101 -                  real_of_float_plus real_of_float_one plus_float numeral_float one_float)
   1.102 +                  plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
   1.103    done
   1.104  
   1.105  lemma transfer_numeral [transfer_rule]: 
   1.106 @@ -366,12 +361,9 @@
   1.107  
   1.108  subsection {* Compute arithmetic operations *}
   1.109  
   1.110 -lemma real_Float[simp]: "real (Float m e) = m * 2 powr e"
   1.111 -  using Float.rep_eq by (simp add: real_of_float_def)
   1.112 -
   1.113  lemma real_of_float_Float[code]: "real_of_float (Float m e) =
   1.114    (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
   1.115 -by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric] Float_def)
   1.116 +by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
   1.117  
   1.118  lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   1.119    unfolding real_of_float_eq mantissa_exponent[of f] by simp
   1.120 @@ -537,9 +529,7 @@
   1.121  subsection {* Rounding Floats *}
   1.122  
   1.123  lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
   1.124 -
   1.125 -lemma real_of_float_float_up[simp]: "real (float_up e f) = round_up e (real f)"
   1.126 -  using float_up.rep_eq by (simp add: real_of_float_def)
   1.127 +declare float_up.rep_eq[simp]
   1.128  
   1.129  lemma float_up_correct:
   1.130    shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
   1.131 @@ -552,9 +542,7 @@
   1.132  qed (simp add: algebra_simps round_up)
   1.133  
   1.134  lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
   1.135 -
   1.136 -lemma real_of_float_float_down[simp]: "real (float_down e f) = round_down e (real f)"
   1.137 -  using float_down.rep_eq by (simp add: real_of_float_def)
   1.138 +declare float_down.rep_eq[simp]
   1.139  
   1.140  lemma float_down_correct:
   1.141    shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
   1.142 @@ -929,7 +917,8 @@
   1.143    ultimately show ?thesis using assms by simp
   1.144  qed
   1.145  
   1.146 -lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   1.147 +lemma rapprox_posrat_less1:
   1.148 +  assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   1.149    shows "real (rapprox_posrat n x y) < 1"
   1.150  proof -
   1.151    have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
   1.152 @@ -947,14 +936,10 @@
   1.153      unfolding int_of_reals real_of_int_le_iff
   1.154      using rat_precision_pos[OF assms] by (rule power_aux)
   1.155    finally show ?thesis
   1.156 -    unfolding rapprox_posrat_def
   1.157 -    apply (simp add: round_up_def)
   1.158 -    apply (simp add: field_simps powr_minus inverse_eq_divide)
   1.159 -    unfolding powr1
   1.160 +    apply (transfer fixing: n x y)
   1.161 +    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
   1.162      unfolding int_of_reals real_of_int_less_iff
   1.163 -    unfolding ceiling_less_eq
   1.164 -    using rat_precision_pos[of x y n] assms
   1.165 -    apply simp
   1.166 +    apply (simp add: ceiling_less_eq)
   1.167      done
   1.168  qed
   1.169  
   1.170 @@ -970,12 +955,7 @@
   1.171        else (if 0 < y
   1.172          then - (rapprox_posrat prec (nat (-x)) (nat y))
   1.173          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   1.174 -  apply transfer
   1.175 -  apply (cases "y = 0")
   1.176 -  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   1.177 -                    int_of_reals simp del: real_of_ints)
   1.178 -  apply (auto simp: ac_simps)
   1.179 -  done
   1.180 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   1.181  
   1.182  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   1.183    "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
   1.184 @@ -989,12 +969,7 @@
   1.185        else (if 0 < y
   1.186          then - (lapprox_posrat prec (nat (-x)) (nat y))
   1.187          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   1.188 -  apply transfer
   1.189 -  apply (cases "y = 0")
   1.190 -  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
   1.191 -                    int_of_reals simp del: real_of_ints)
   1.192 -  apply (auto simp: ac_simps)
   1.193 -  done
   1.194 +  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   1.195  
   1.196  subsection {* Division *}
   1.197  
   1.198 @@ -1004,23 +979,17 @@
   1.199  lemma compute_float_divl[code]:
   1.200    "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   1.201  proof cases
   1.202 -  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.203 -  then show ?thesis
   1.204 -  proof transfer
   1.205 -    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.206 -    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   1.207 -    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   1.208 +  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   1.209 +  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   1.210 +  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.211 +  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   1.212 +    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   1.213 +  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   1.214 +    by (simp add: field_simps powr_divide2[symmetric])
   1.215  
   1.216 -    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   1.217 -      by (simp add: field_simps powr_divide2[symmetric])
   1.218 -    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   1.219 -        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   1.220 -      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   1.221 -    
   1.222 -    show "round_down (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   1.223 -      round_down (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   1.224 -      using not_0 unfolding eq1 eq2 round_down_shift by (simp add: field_simps)
   1.225 -  qed
   1.226 +  show ?thesis
   1.227 +    using not_0 
   1.228 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
   1.229  qed (transfer, auto)
   1.230  
   1.231  lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
   1.232 @@ -1029,23 +998,17 @@
   1.233  lemma compute_float_divr[code]:
   1.234    "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   1.235  proof cases
   1.236 -  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.237 -  then show ?thesis
   1.238 -  proof transfer
   1.239 -    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.240 -    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   1.241 -    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   1.242 +  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
   1.243 +  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
   1.244 +  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
   1.245 +  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   1.246 +    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   1.247 +  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   1.248 +    by (simp add: field_simps powr_divide2[symmetric])
   1.249  
   1.250 -    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
   1.251 -      by (simp add: field_simps powr_divide2[symmetric])
   1.252 -    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
   1.253 -        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
   1.254 -      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
   1.255 -    
   1.256 -    show "round_up (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
   1.257 -      round_up (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
   1.258 -      using not_0 unfolding eq1 eq2 round_up_shift by (simp add: field_simps)
   1.259 -  qed
   1.260 +  show ?thesis
   1.261 +    using not_0 
   1.262 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   1.263  qed (transfer, auto)
   1.264  
   1.265  subsection {* Lemmas needed by Approximate *}
   1.266 @@ -1242,12 +1205,9 @@
   1.267    "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
   1.268      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
   1.269               else Float m e)"
   1.270 +  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   1.271    unfolding Let_def
   1.272 -  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   1.273 -  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
   1.274 -  apply (cases "m = 0")
   1.275 -  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
   1.276 -  done
   1.277 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   1.278  
   1.279  lemma compute_float_round_up[code]:
   1.280    "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
   1.281 @@ -1256,10 +1216,7 @@
   1.282                else Float m e)"
   1.283    using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   1.284    unfolding Let_def
   1.285 -  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
   1.286 -  apply (cases "m = 0")
   1.287 -  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
   1.288 -  done
   1.289 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   1.290  
   1.291  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   1.292   apply (auto simp: zero_float_def mult_le_0_iff)
   1.293 @@ -1282,15 +1239,13 @@
   1.294  lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
   1.295  
   1.296  lemma compute_int_floor_fl[code]:
   1.297 -  shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e
   1.298 -                                  else m div (2 ^ (nat (-e))))"
   1.299 +  "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   1.300    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   1.301  
   1.302  lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
   1.303  
   1.304  lemma compute_floor_fl[code]:
   1.305 -  shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e
   1.306 -                                  else Float (m div (2 ^ (nat (-e)))) 0)"
   1.307 +  "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   1.308    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   1.309  
   1.310  lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
   1.311 @@ -1305,7 +1260,5 @@
   1.312    thus ?thesis by simp
   1.313  qed (simp add: floor_fl_def)
   1.314  
   1.315 -code_datatype Float
   1.316 -
   1.317  end
   1.318