src/HOL/Library/Float.thy
changeset 53381 355a4cac5440
parent 53215 5e47c31c6f7c
child 54230 b1d955791529
     1.1 --- a/src/HOL/Library/Float.thy	Tue Sep 03 19:58:00 2013 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Sep 03 22:04:23 2013 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
     1.6  lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
     1.7 -lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp  
     1.8 +lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
     1.9  lemma neg_numeral_float[simp]: "neg_numeral i \<in> float" by (intro floatI[of "neg_numeral i" 0]) simp
    1.10  lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
    1.11  lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
    1.12 @@ -175,7 +175,7 @@
    1.13  lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
    1.14    by (induct n) simp_all
    1.15  
    1.16 -lemma fixes x y::float 
    1.17 +lemma fixes x y::float
    1.18    shows real_of_float_min: "real (min x y) = min (real x) (real y)"
    1.19      and real_of_float_max: "real (max x y) = max (real x) (real y)"
    1.20    by (simp_all add: min_def max_def)
    1.21 @@ -197,7 +197,7 @@
    1.22    then show "\<exists>c. a < c \<and> c < b"
    1.23      apply (intro exI[of _ "(a + b) * Float 1 -1"])
    1.24      apply transfer
    1.25 -    apply (simp add: powr_neg_numeral) 
    1.26 +    apply (simp add: powr_neg_numeral)
    1.27      done
    1.28  qed
    1.29  
    1.30 @@ -222,14 +222,14 @@
    1.31                    plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
    1.32    done
    1.33  
    1.34 -lemma transfer_numeral [transfer_rule]: 
    1.35 +lemma transfer_numeral [transfer_rule]:
    1.36    "fun_rel (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
    1.37    unfolding fun_rel_def float.pcr_cr_eq  cr_float_def by simp
    1.38  
    1.39  lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
    1.40    by (simp add: minus_numeral[symmetric] del: minus_numeral)
    1.41  
    1.42 -lemma transfer_neg_numeral [transfer_rule]: 
    1.43 +lemma transfer_neg_numeral [transfer_rule]:
    1.44    "fun_rel (op =) pcr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    1.45    unfolding fun_rel_def float.pcr_cr_eq cr_float_def by simp
    1.46  
    1.47 @@ -321,7 +321,7 @@
    1.48    "exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
    1.49     \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
    1.50  
    1.51 -lemma 
    1.52 +lemma
    1.53    shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
    1.54      and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
    1.55  proof -
    1.56 @@ -351,7 +351,7 @@
    1.57  lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
    1.58    using mantissa_not_dvd[of f] by auto
    1.59  
    1.60 -lemma 
    1.61 +lemma
    1.62    fixes m e :: int
    1.63    defines "f \<equiv> float_of (m * 2 powr e)"
    1.64    assumes dvd: "\<not> 2 dvd m"
    1.65 @@ -740,19 +740,23 @@
    1.66  qed
    1.67  
    1.68  lemma bitlen_Float:
    1.69 -fixes m e
    1.70 -defines "f \<equiv> Float m e"
    1.71 -shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
    1.72 -proof cases
    1.73 -  assume "m \<noteq> 0"
    1.74 +  fixes m e
    1.75 +  defines "f \<equiv> Float m e"
    1.76 +  shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
    1.77 +proof (cases "m = 0")
    1.78 +  case True
    1.79 +  then show ?thesis by (simp add: f_def bitlen_def Float_def)
    1.80 +next
    1.81 +  case False
    1.82    hence "f \<noteq> float_of 0"
    1.83      unfolding real_of_float_eq by (simp add: f_def)
    1.84    hence "mantissa f \<noteq> 0"
    1.85      by (simp add: mantissa_noteq_0)
    1.86    moreover
    1.87 -  from f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`] guess i .
    1.88 +  obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
    1.89 +    by (rule f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`])
    1.90    ultimately show ?thesis by (simp add: abs_mult)
    1.91 -qed (simp add: f_def bitlen_def Float_def)
    1.92 +qed
    1.93  
    1.94  lemma compute_bitlen[code]:
    1.95    shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
    1.96 @@ -865,9 +869,9 @@
    1.97    is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
    1.98  
    1.99  lemma compute_lapprox_posrat[code]:
   1.100 -  fixes prec x y 
   1.101 -  shows "lapprox_posrat prec x y = 
   1.102 -   (let 
   1.103 +  fixes prec x y
   1.104 +  shows "lapprox_posrat prec x y =
   1.105 +   (let
   1.106         l = rat_precision prec x y;
   1.107         d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
   1.108      in normfloat (Float d (- l)))"
   1.109 @@ -948,7 +952,7 @@
   1.110    assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   1.111    shows "real (rapprox_posrat n x y) < 1"
   1.112  proof -
   1.113 -  have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
   1.114 +  have powr1: "2 powr real (rat_precision n (int x) (int y)) =
   1.115      2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms
   1.116      by (simp add: powr_realpow[symmetric])
   1.117    have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) *
   1.118 @@ -978,7 +982,7 @@
   1.119      (if y = 0 then 0
   1.120      else if 0 \<le> x then
   1.121        (if 0 < y then lapprox_posrat prec (nat x) (nat y)
   1.122 -      else - (rapprox_posrat prec (nat x) (nat (-y)))) 
   1.123 +      else - (rapprox_posrat prec (nat x) (nat (-y))))
   1.124        else (if 0 < y
   1.125          then - (rapprox_posrat prec (nat (-x)) (nat y))
   1.126          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   1.127 @@ -993,7 +997,7 @@
   1.128      (if y = 0 then 0
   1.129      else if 0 \<le> x then
   1.130        (if 0 < y then rapprox_posrat prec (nat x) (nat y)
   1.131 -      else - (lapprox_posrat prec (nat x) (nat (-y)))) 
   1.132 +      else - (lapprox_posrat prec (nat x) (nat (-y))))
   1.133        else (if 0 < y
   1.134          then - (lapprox_posrat prec (nat (-x)) (nat y))
   1.135          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   1.136 @@ -1017,7 +1021,7 @@
   1.137      by (simp add: field_simps powr_divide2[symmetric])
   1.138  
   1.139    show ?thesis
   1.140 -    using not_0 
   1.141 +    using not_0
   1.142      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
   1.143  qed (transfer, auto)
   1.144  hide_fact (open) compute_float_divl
   1.145 @@ -1037,7 +1041,7 @@
   1.146      by (simp add: field_simps powr_divide2[symmetric])
   1.147  
   1.148    show ?thesis
   1.149 -    using not_0 
   1.150 +    using not_0
   1.151      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   1.152  qed (transfer, auto)
   1.153  hide_fact (open) compute_float_divr
   1.154 @@ -1104,7 +1108,7 @@
   1.155         (simp add: powr_minus inverse_eq_divide)
   1.156  qed
   1.157  
   1.158 -lemma rapprox_rat_nonneg_neg: 
   1.159 +lemma rapprox_rat_nonneg_neg:
   1.160    "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
   1.161    unfolding rapprox_rat_def round_up_def
   1.162    by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
   1.163 @@ -1157,7 +1161,7 @@
   1.164    "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
   1.165  proof transfer
   1.166    fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
   1.167 -  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>" 
   1.168 +  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
   1.169    show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
   1.170    proof cases
   1.171      assume nonneg: "0 \<le> p"
   1.172 @@ -1279,12 +1283,16 @@
   1.173  lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
   1.174  
   1.175  lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
   1.176 -proof cases
   1.177 -  assume nzero: "floor_fl x \<noteq> float_of 0"
   1.178 -  have "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
   1.179 -  from denormalize_shift[OF this[THEN eq_reflection] nzero] guess i . note i = this
   1.180 -  thus ?thesis by simp
   1.181 -qed (simp add: floor_fl_def)
   1.182 +proof (cases "floor_fl x = float_of 0")
   1.183 +  case True
   1.184 +  then show ?thesis by (simp add: floor_fl_def)
   1.185 +next
   1.186 +  case False
   1.187 +  have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
   1.188 +  obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
   1.189 +    by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
   1.190 +  then show ?thesis by simp
   1.191 +qed
   1.192  
   1.193  end
   1.194