src/HOL/Library/Float.thy
changeset 54782 cd8f55c358c5
parent 54489 03ff4d1e6784
child 54783 25860d89a044
     1.1 --- a/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -555,29 +555,37 @@
     1.4  lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
     1.5  declare float_up.rep_eq[simp]
     1.6  
     1.7 -lemma float_up_correct:
     1.8 -  shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
     1.9 +lemma round_up_correct:
    1.10 +  shows "round_up e f - f \<in> {0..2 powr -e}"
    1.11  unfolding atLeastAtMost_iff
    1.12  proof
    1.13    have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
    1.14    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    1.15 -  finally show "real (float_up e f) - real f \<le> 2 powr real (- e)"
    1.16 +  finally show "round_up e f - f \<le> 2 powr real (- e)"
    1.17      by simp
    1.18  qed (simp add: algebra_simps round_up)
    1.19  
    1.20 +lemma float_up_correct:
    1.21 +  shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
    1.22 +  by transfer (rule round_up_correct)
    1.23 +
    1.24  lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
    1.25  declare float_down.rep_eq[simp]
    1.26  
    1.27 -lemma float_down_correct:
    1.28 -  shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
    1.29 +lemma round_down_correct:
    1.30 +  shows "f - (round_down e f) \<in> {0..2 powr -e}"
    1.31  unfolding atLeastAtMost_iff
    1.32  proof
    1.33    have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
    1.34    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    1.35 -  finally show "real f - real (float_down e f) \<le> 2 powr real (- e)"
    1.36 +  finally show "f - round_down e f \<le> 2 powr real (- e)"
    1.37      by simp
    1.38  qed (simp add: algebra_simps round_down)
    1.39  
    1.40 +lemma float_down_correct:
    1.41 +  shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
    1.42 +  by transfer (rule round_down_correct)
    1.43 +
    1.44  lemma compute_float_down[code]:
    1.45    "float_down p (Float m e) =
    1.46      (if p + e < 0 then Float (m div 2^nat (-(p + e))) (-p) else Float m e)"
    1.47 @@ -602,6 +610,15 @@
    1.48  qed
    1.49  hide_fact (open) compute_float_down
    1.50  
    1.51 +lemma abs_round_down_le: "\<bar>f - (round_down e f)\<bar> \<le> 2 powr -e"
    1.52 +  using round_down_correct[of f e] by simp
    1.53 +
    1.54 +lemma abs_round_up_le: "\<bar>f - (round_up e f)\<bar> \<le> 2 powr -e"
    1.55 +  using round_up_correct[of e f] by simp
    1.56 +
    1.57 +lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
    1.58 +  by (auto simp: round_down_def intro!: mult_nonneg_nonneg)
    1.59 +
    1.60  lemma ceil_divide_floor_conv:
    1.61  assumes "b \<noteq> 0"
    1.62  shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)"
    1.63 @@ -1006,8 +1023,12 @@
    1.64  
    1.65  subsection {* Division *}
    1.66  
    1.67 -lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
    1.68 -  "\<lambda>(prec::nat) a b. round_down (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
    1.69 +definition "real_divl prec a b = round_down (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
    1.70 +
    1.71 +definition "real_divr prec a b = round_up (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
    1.72 +
    1.73 +lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl
    1.74 +  by (simp add: real_divl_def)
    1.75  
    1.76  lemma compute_float_divl[code]:
    1.77    "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
    1.78 @@ -1022,12 +1043,13 @@
    1.79  
    1.80    show ?thesis
    1.81      using not_0
    1.82 -    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
    1.83 -qed (transfer, auto)
    1.84 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift real_divl_def,
    1.85 +      simp add: field_simps)
    1.86 +qed (transfer, auto simp: real_divl_def)
    1.87  hide_fact (open) compute_float_divl
    1.88  
    1.89 -lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
    1.90 -  "\<lambda>(prec::nat) a b. round_up (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
    1.91 +lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
    1.92 +  by (simp add: real_divr_def)
    1.93  
    1.94  lemma compute_float_divr[code]:
    1.95    "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
    1.96 @@ -1042,8 +1064,9 @@
    1.97  
    1.98    show ?thesis
    1.99      using not_0
   1.100 -    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   1.101 -qed (transfer, auto)
   1.102 +    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift real_divr_def,
   1.103 +      simp add: field_simps)
   1.104 +qed (transfer, auto simp: real_divr_def)
   1.105  hide_fact (open) compute_float_divr
   1.106  
   1.107  subsection {* Lemmas needed by Approximate *}
   1.108 @@ -1123,12 +1146,22 @@
   1.109    unfolding rapprox_rat_def round_up_def
   1.110    by (auto simp: field_simps mult_le_0_iff)
   1.111  
   1.112 +lemma real_divl: "real_divl prec x y \<le> x / y"
   1.113 +  by (simp add: real_divl_def round_down)
   1.114 +
   1.115 +lemma real_divr: "x / y \<le> real_divr prec x y"
   1.116 +  using round_up by (simp add: real_divr_def)
   1.117 +
   1.118  lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
   1.119 -  by transfer (simp add: round_down)
   1.120 +  by transfer (rule real_divl)
   1.121 +
   1.122 +lemma real_divl_lower_bound:
   1.123 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y"
   1.124 +  by (simp add: real_divl_def round_down_def zero_le_mult_iff zero_le_divide_iff)
   1.125  
   1.126  lemma float_divl_lower_bound:
   1.127 -  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
   1.128 -  by transfer (simp add: round_down_def zero_le_mult_iff zero_le_divide_iff)
   1.129 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
   1.130 +  by transfer (rule real_divl_lower_bound)
   1.131  
   1.132  lemma exponent_1: "exponent 1 = 0"
   1.133    using exponent_float[of 1 0] by (simp add: one_float_def)
   1.134 @@ -1157,10 +1190,10 @@
   1.135    finally show ?thesis by (simp add: powr_add)
   1.136  qed
   1.137  
   1.138 -lemma float_divl_pos_less1_bound:
   1.139 -  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
   1.140 -proof transfer
   1.141 -  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" "x \<in> float" and prec: "1 \<le> prec"
   1.142 +lemma real_divl_pos_less1_bound:
   1.143 +  "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real_divl prec 1 x"
   1.144 +proof (unfold real_divl_def)
   1.145 +  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" and prec: "1 \<le> prec"
   1.146    def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
   1.147    show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
   1.148    proof cases
   1.149 @@ -1203,35 +1236,71 @@
   1.150    qed
   1.151  qed
   1.152  
   1.153 -lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
   1.154 -  using round_up by transfer simp
   1.155 +lemma float_divl_pos_less1_bound:
   1.156 +  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
   1.157 +  by (transfer, rule real_divl_pos_less1_bound)
   1.158  
   1.159 -lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
   1.160 +lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
   1.161 +  by transfer (rule real_divr)
   1.162 +
   1.163 +lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> real_divr prec 1 x"
   1.164  proof -
   1.165 -  have "1 \<le> 1 / real x" using `0 < x` and `x < 1` by auto
   1.166 -  also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
   1.167 +  have "1 \<le> 1 / x" using `0 < x` and `x < 1` by auto
   1.168 +  also have "\<dots> \<le> real_divr prec 1 x" using real_divr[where x=1 and y=x] by auto
   1.169    finally show ?thesis by auto
   1.170  qed
   1.171  
   1.172 +lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x"
   1.173 +  by transfer (rule real_divr_pos_less1_lower_bound)
   1.174 +
   1.175 +lemma real_divr_nonpos_pos_upper_bound:
   1.176 +  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> real_divr prec x y \<le> 0"
   1.177 +  by (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def real_divr_def)
   1.178 +
   1.179  lemma float_divr_nonpos_pos_upper_bound:
   1.180    "real x \<le> 0 \<Longrightarrow> 0 < real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
   1.181 -  by transfer (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def)
   1.182 +  by transfer (rule real_divr_nonpos_pos_upper_bound)
   1.183 +
   1.184 +lemma real_divr_nonneg_neg_upper_bound:
   1.185 +  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real_divr prec x y \<le> 0"
   1.186 +  by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def real_divr_def)
   1.187  
   1.188  lemma float_divr_nonneg_neg_upper_bound:
   1.189    "0 \<le> real x \<Longrightarrow> real y < 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
   1.190 -  by transfer (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def)
   1.191 +  by transfer (rule real_divr_nonneg_neg_upper_bound)
   1.192 +
   1.193 +definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real" where
   1.194 +  "truncate_down prec x = round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   1.195 +
   1.196 +lemma truncate_down: "truncate_down prec x \<le> x"
   1.197 +  using round_down by (simp add: truncate_down_def)
   1.198 +
   1.199 +lemma truncate_down_le: "x \<le> y \<Longrightarrow> truncate_down prec x \<le> y"
   1.200 +  by (rule order_trans[OF truncate_down])
   1.201  
   1.202 -lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is
   1.203 -  "\<lambda>(prec::nat) x. round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
   1.204 +definition truncate_up::"nat \<Rightarrow> real \<Rightarrow> real" where
   1.205 +  "truncate_up prec x = round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   1.206 +
   1.207 +lemma truncate_up: "x \<le> truncate_up prec x"
   1.208 +  using round_up by (simp add: truncate_up_def)
   1.209 +
   1.210 +lemma truncate_up_le: "x \<le> y \<Longrightarrow> x \<le> truncate_up prec y"
   1.211 +  by (rule order_trans[OF _ truncate_up])
   1.212 +
   1.213 +lemma truncate_up_zero[simp]: "truncate_up prec 0 = 0"
   1.214 +  by (simp add: truncate_up_def)
   1.215 +
   1.216 +lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up
   1.217 +  by (simp add: truncate_up_def)
   1.218  
   1.219  lemma float_round_up: "real x \<le> real (float_round_up prec x)"
   1.220 -  using round_up by transfer simp
   1.221 +  using truncate_up by transfer simp
   1.222  
   1.223 -lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is
   1.224 -  "\<lambda>(prec::nat) x. round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x" by simp
   1.225 +lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_down
   1.226 +  by (simp add: truncate_down_def)
   1.227  
   1.228  lemma float_round_down: "real (float_round_down prec x) \<le> real x"
   1.229 -  using round_down by transfer simp
   1.230 +  using truncate_down by transfer simp
   1.231  
   1.232  lemma floor_add2[simp]: "\<lfloor> real i + x \<rfloor> = i + \<lfloor> x \<rfloor>"
   1.233    using floor_add[of x i] by (simp del: floor_add add: ac_simps)
   1.234 @@ -1241,7 +1310,8 @@
   1.235      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
   1.236               else Float m e)"
   1.237    using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   1.238 -  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   1.239 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def
   1.240 +    cong del: if_weak_cong)
   1.241  hide_fact (open) compute_float_round_down
   1.242  
   1.243  lemma compute_float_round_up[code]:
   1.244 @@ -1251,7 +1321,8 @@
   1.245                else Float m e)"
   1.246    using Float.compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   1.247    unfolding Let_def
   1.248 -  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   1.249 +  by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_up_def
   1.250 +    cong del: if_weak_cong)
   1.251  hide_fact (open) compute_float_round_up
   1.252  
   1.253  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"