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.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.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.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.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"
```