author immler Wed Nov 12 17:36:29 2014 +0100 (2014-11-12) changeset 58982 27e7e3f9e665 parent 58981 11b6c099f5f3 child 58983 9c390032e4eb
simplified computations based on round_up by reducing to round_down;
more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 12 17:36:25 2014 +0100
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Nov 12 17:36:29 2014 +0100
1.3 @@ -450,7 +450,8 @@
1.4      let ?k = "lapprox_rat prec 1 k"
1.5      have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto
1.6      have "1 / k \<le> 1" using `1 < k` by auto
1.7 -    have "\<And>n. 0 \<le> real ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one `0 < k`] by (auto simp add: `1 div k = 0`)
1.8 +    have "\<And>n. 0 \<le> real ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one `0 \<le> k`]
1.9 +      by (auto simp add: `1 div k = 0`)
1.10      have "\<And>n. real ?k \<le> 1" using lapprox_rat by (rule order_trans, auto simp add: `1 / k \<le> 1`)
1.11
1.12      have "?k \<le> 1 / k" using lapprox_rat[where x=1 and y=k] by auto
1.13 @@ -1398,7 +1399,7 @@
1.14    have "1 / 4 = (Float 1 (- 2))" unfolding Float_num by auto
1.15    also have "\<dots> \<le> lb_exp_horner 1 (get_even 4) 1 1 (- 1)"
1.16      unfolding get_even_def eq4
1.17 -    by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat
1.18 +    by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat divmod_int_mod_div
1.19                    Float.compute_lapprox_posrat Float.compute_rapprox_posrat rat_precision_def Float.compute_bitlen)
1.20    also have "\<dots> \<le> exp (- 1 :: float)" using bnds_exp_horner[where x="- 1"] by auto
1.21    finally show ?thesis by simp
1.22 @@ -1458,14 +1459,14 @@
1.23      hence "real (int_floor_fl x) < 0" unfolding less_float_def by auto
1.24      have fl_eq: "real (- int_floor_fl x) = real (- floor_fl x)"
1.25        by (simp add: floor_fl_def int_floor_fl_def)
1.26 -    from `0 < - int_floor_fl x` have "0 < real (- floor_fl x)"
1.27 +    from `0 < - int_floor_fl x` have "0 \<le> real (- floor_fl x)"
1.28        by (simp add: floor_fl_def int_floor_fl_def)
1.29      from `real (int_floor_fl x) < 0` have "real (floor_fl x) < 0"
1.30        by (simp add: floor_fl_def int_floor_fl_def)
1.31      have "exp x \<le> ub_exp prec x"
1.32      proof -
1.33        have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
1.34 -        using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
1.35 +        using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 \<le> real (- floor_fl x)`]
1.36          unfolding less_eq_float_def zero_float.rep_eq .
1.37
1.38        have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
1.39 @@ -1669,7 +1670,8 @@
1.40    have lb2: "0 \<le> real (Float 1 (- 1))" and ub2: "real (Float 1 (- 1)) < 1" unfolding Float_num by auto
1.41
1.42    have "0 \<le> (1::int)" and "0 < (3::int)" by auto
1.43 -  have ub3_ub: "real ?uthird < 1" by (simp add: Float.compute_rapprox_rat rapprox_posrat_less1)
1.44 +  have ub3_ub: "real ?uthird < 1"
1.45 +    by (simp add: Float.compute_rapprox_rat Float.compute_lapprox_rat rapprox_posrat_less1)
1.46
1.47    have third_gt0: "(0 :: real) < 1 / 3 + 1" by auto
1.48    have uthird_gt0: "0 < real ?uthird + 1" using ub3_lb by auto
1.49 @@ -1714,7 +1716,7 @@
1.50  termination proof (relation "measure (\<lambda> v. let (prec, x) = case_sum id id v in (if x < 1 then 1 else 0))", auto)
1.51    fix prec and x :: float assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divl (max prec (Suc 0)) 1 x) < 1"
1.52    hence "0 < real x" "1 \<le> max prec (Suc 0)" "real x < 1" by auto
1.53 -  from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1` `1 \<le> max prec (Suc 0)`]
1.54 +  from float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`[THEN less_imp_le] `1 \<le> max prec (Suc 0)`]
1.55    show False using `real (float_divl (max prec (Suc 0)) 1 x) < 1` by auto
1.56  next
1.57    fix prec x assume "\<not> real x \<le> 0" and "real x < 1" and "real (float_divr prec 1 x) < 1"
1.58 @@ -1963,13 +1965,13 @@
1.59    show ?thesis using ub_ln_lb_ln_bounds'[OF `1 \<le> x`] .
1.60  next
1.61    case True have "\<not> x \<le> 0" using `0 < x` by auto
1.62 -  from True have "real x < 1" by simp
1.63 +  from True have "real x \<le> 1" "x \<le> 1" by simp_all
1.64    have "0 < real x" and "real x \<noteq> 0" using `0 < x` by auto
1.65    hence A: "0 < 1 / real x" by auto
1.66
1.67    {
1.68      let ?divl = "float_divl (max prec 1) 1 x"
1.69 -    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x < 1`] by auto
1.70 +    have A': "1 \<le> ?divl" using float_divl_pos_less1_bound[OF `0 < real x` `real x \<le> 1`] by auto
1.71      hence B: "0 < real ?divl" by auto
1.72
1.73      have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
1.74 @@ -1979,7 +1981,7 @@
1.75    } moreover
1.76    {
1.77      let ?divr = "float_divr prec 1 x"
1.78 -    have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x < 1`] unfolding less_eq_float_def less_float_def by auto
1.79 +    have A': "1 \<le> ?divr" using float_divr_pos_less1_lower_bound[OF `0 < x` `x \<le> 1`] unfolding less_eq_float_def less_float_def by auto
1.80      hence B: "0 < real ?divr" by auto
1.81
1.82      have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
```
```     2.1 --- a/src/HOL/Library/Float.thy	Wed Nov 12 17:36:25 2014 +0100
2.2 +++ b/src/HOL/Library/Float.thy	Wed Nov 12 17:36:29 2014 +0100
2.3 @@ -435,13 +435,12 @@
2.4    by transfer simp
2.5  hide_fact (open) compute_float_one
2.6
2.7 -definition normfloat :: "float \<Rightarrow> float" where
2.8 -  [simp]: "normfloat x = x"
2.9 +lift_definition normfloat :: "float \<Rightarrow> float" is "\<lambda>x. x" .
2.10 +lemma normloat_id[simp]: "normfloat x = x" by transfer rule
2.11
2.12  lemma compute_normfloat[code]: "normfloat (Float m e) =
2.13    (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
2.14                             else if m = 0 then 0 else Float m e)"
2.15 -  unfolding normfloat_def
2.17  hide_fact (open) compute_normfloat
2.18
2.19 @@ -510,6 +509,33 @@
2.20    by transfer simp
2.21  hide_fact (open) compute_float_eq
2.22
2.23 +
2.24 +subsection {* Lemmas for types @{typ real}, @{typ nat}, @{typ int}*}
2.25 +
2.26 +lemmas real_of_ints =
2.27 +  real_of_int_zero
2.28 +  real_of_one
2.30 +  real_of_int_minus
2.31 +  real_of_int_diff
2.32 +  real_of_int_mult
2.33 +  real_of_int_power
2.34 +  real_numeral
2.35 +lemmas real_of_nats =
2.36 +  real_of_nat_zero
2.37 +  real_of_nat_one
2.38 +  real_of_nat_1
2.40 +  real_of_nat_mult
2.41 +  real_of_nat_power
2.42 +
2.43 +lemmas int_of_reals = real_of_ints[symmetric]
2.44 +lemmas nat_of_reals = real_of_nats[symmetric]
2.45 +
2.46 +lemma two_real_int: "(2::real) = real (2::int)" by simp
2.47 +lemma two_real_nat: "(2::real) = real (2::nat)" by simp
2.48 +
2.49 +
2.50  subsection {* Rounding Real numbers *}
2.51
2.52  definition round_down :: "int \<Rightarrow> real \<Rightarrow> real" where
2.53 @@ -561,6 +587,86 @@
2.56
2.57 +lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
2.58 +  and round_down_uminus_eq: "round_down p (-x) = - round_up p x"
2.59 +  by (auto simp: round_up_def round_down_def ceiling_def)
2.60 +
2.61 +lemma round_up_mono: "x \<le> y \<Longrightarrow> round_up p x \<le> round_up p y"
2.62 +  by (auto intro!: ceiling_mono simp: round_up_def)
2.63 +
2.64 +lemma round_up_le1:
2.65 +  assumes "x \<le> 1" "prec \<ge> 0"
2.66 +  shows "round_up prec x \<le> 1"
2.67 +proof -
2.68 +  have "real \<lceil>x * 2 powr prec\<rceil> \<le> real \<lceil>2 powr real prec\<rceil>"
2.69 +    using assms by (auto intro!: ceiling_mono)
2.70 +  also have "\<dots> = 2 powr prec" using assms by (auto simp: powr_int intro!: exI[where x="2^nat prec"])
2.71 +  finally show ?thesis
2.73 +qed
2.74 +
2.75 +lemma round_up_less1:
2.76 +  assumes "x < 1 / 2" "p > 0"
2.77 +  shows "round_up p x < 1"
2.78 +proof -
2.79 +  have powr1: "2 powr p = 2 ^ nat p"
2.80 +    using `p > 0` by (simp add: powr_realpow[symmetric])
2.81 +  have "x * 2 powr p < 1 / 2 * 2 powr p"
2.82 +    using assms by simp
2.83 +  also have "\<dots> = 2 powr (p - 1)"
2.84 +    by (simp add: algebra_simps powr_mult_base)
2.85 +  also have "\<dots> = 2 ^ nat (p - 1)"
2.86 +    using `p > 0` by (simp add: powr_realpow[symmetric])
2.87 +  also have "\<dots> \<le> 2 ^ nat p - 1"
2.88 +    using `p > 0`
2.89 +    unfolding int_of_reals real_of_int_le_iff
2.90 +    by simp
2.91 +  finally show ?thesis
2.92 +    apply (simp add: round_up_def field_simps powr_minus powr1)
2.93 +    unfolding int_of_reals real_of_int_less_iff
2.94 +    apply (simp add: ceiling_less_eq)
2.95 +    done
2.96 +qed
2.97 +
2.98 +lemma round_down_ge1:
2.99 +  assumes x: "x \<ge> 1"
2.100 +  assumes prec: "p \<ge> - log 2 x"
2.101 +  shows "1 \<le> round_down p x"
2.102 +proof cases
2.103 +  assume nonneg: "0 \<le> p"
2.104 +  hence "2 powr real (p) = floor (real ((2::int) ^ nat p)) * floor (1::real)"
2.105 +    by (simp add: powr_int del: real_of_int_power) simp
2.106 +  also have "floor (1::real) \<le> floor x" using x by simp
2.107 +  also have "floor (real ((2::int) ^ nat p)) * floor x \<le>
2.108 +    floor (real ((2::int) ^ nat p) * x)"
2.109 +    using x
2.110 +    by (intro le_mult_floor) (auto simp: less_imp_le)
2.111 +  finally have "2 powr real p \<le> floor (2 powr nat p * x)" by (simp add: powr_realpow)
2.112 +  thus ?thesis
2.113 +    using x nonneg by (simp add: powr_minus inverse_eq_divide round_down_def mult.commute)
2.114 +next
2.115 +  assume neg: "\<not> 0 \<le> p"
2.116 +  have "x = 2 powr (log 2 x)"
2.117 +    using x by simp
2.118 +  also have "2 powr (log 2 x) \<ge> 2 powr - p"
2.119 +    using prec by auto
2.120 +  finally have x_le: "x \<ge> 2 powr -p" .
2.121 +
2.122 +  from neg have "2 powr real p \<le> 2 powr 0"
2.123 +    by (intro powr_mono) auto
2.124 +  also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
2.125 +  also have "\<dots> \<le> \<lfloor>x * 2 powr real p\<rfloor>" unfolding real_of_int_le_iff
2.126 +    using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
2.127 +  finally show ?thesis
2.128 +    using prec x
2.129 +    by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
2.130 +qed
2.131 +
2.132 +lemma round_up_le0: "x \<le> 0 \<Longrightarrow> round_up p x \<le> 0"
2.133 +  unfolding round_up_def
2.134 +  by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
2.135 +
2.136 +
2.137  subsection {* Rounding Floats *}
2.138
2.139  lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
2.140 @@ -649,72 +755,10 @@
2.141    floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
2.142
2.143  lemma compute_float_up[code]:
2.144 -  "float_up p (Float m e) =
2.145 -    (let P = 2^nat (-(p + e)); r = m mod P in
2.146 -      if p + e < 0 then Float (m div P + (if r = 0 then 0 else 1)) (-p) else Float m e)"
2.147 -proof cases
2.148 -  assume "p + e < 0"
2.149 -  hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
2.150 -    using powr_realpow[of 2 "nat (-(p + e))"] by simp
2.151 -  also have "... = 1 / 2 powr p / 2 powr e"
2.153 -  finally have twopow_rewrite:
2.154 -    "real ((2::int) ^ nat (- (p + e))) = 1 / 2 powr real p / 2 powr real e" .
2.155 -  with `p + e < 0` have powr_rewrite:
2.156 -    "2 powr real e * 2 powr real p = 1 / real ((2::int) ^ nat (- (p + e)))"
2.157 -    unfolding powr_divide2 by simp
2.158 -  show ?thesis
2.159 -  proof cases
2.160 -    assume "2^nat (-(p + e)) dvd m"
2.161 -    with `p + e < 0` twopow_rewrite show ?thesis
2.162 -      by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div dvd_eq_mod_eq_0)
2.163 -  next
2.164 -    assume ndvd: "\<not> 2 ^ nat (- (p + e)) dvd m"
2.165 -    have one_div: "real m * (1 / real ((2::int) ^ nat (- (p + e)))) =
2.166 -      real m / real ((2::int) ^ nat (- (p + e)))"
2.167 -      by (simp add: field_simps)
2.168 -    have "real \<lceil>real m * (2 powr real e * 2 powr real p)\<rceil> =
2.169 -      real \<lfloor>real m * (2 powr real e * 2 powr real p)\<rfloor> + 1"
2.170 -      using ndvd unfolding powr_rewrite one_div
2.171 -      by (subst ceil_divide_floor_conv) (auto simp: field_simps)
2.172 -    thus ?thesis using `p + e < 0` twopow_rewrite
2.173 -      by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div[symmetric])
2.174 -  qed
2.175 -next
2.176 -  assume "\<not> p + e < 0"
2.177 -  then have r1: "real e + real p = real (nat (e + p))" by simp
2.178 -  have r: "\<lceil>(m * 2 powr e) * 2 powr real p\<rceil> = (m * 2 powr e) * 2 powr real p"
2.180 -      intro: exI[where x="m*2^nat (e+p)"])
2.181 -  then show ?thesis using `\<not> p + e < 0`
2.183 -qed
2.184 +  "float_up p x = - float_down p (-x)"
2.185 +  by transfer (simp add: round_down_uminus_eq)
2.186  hide_fact (open) compute_float_up
2.187
2.188 -lemmas real_of_ints =
2.189 -  real_of_int_zero
2.190 -  real_of_one
2.192 -  real_of_int_minus
2.193 -  real_of_int_diff
2.194 -  real_of_int_mult
2.195 -  real_of_int_power
2.196 -  real_numeral
2.197 -lemmas real_of_nats =
2.198 -  real_of_nat_zero
2.199 -  real_of_nat_one
2.200 -  real_of_nat_1
2.202 -  real_of_nat_mult
2.203 -  real_of_nat_power
2.204 -
2.205 -lemmas int_of_reals = real_of_ints[symmetric]
2.206 -lemmas nat_of_reals = real_of_nats[symmetric]
2.207 -
2.208 -lemma two_real_int: "(2::real) = real (2::int)" by simp
2.209 -lemma two_real_nat: "(2::real) = real (2::nat)" by simp
2.210 -
2.211 -lemma mult_cong: "a = c ==> b = d ==> a*b = c*d" by simp
2.212
2.213  subsection {* Compute bitlen of integers *}
2.214
2.215 @@ -901,7 +945,7 @@
2.216         l = rat_precision prec x y;
2.217         d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
2.218      in normfloat (Float d (- l)))"
2.219 -    unfolding div_mult_twopow_eq normfloat_def
2.220 +    unfolding div_mult_twopow_eq
2.221      by transfer
2.222         (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
2.223               del: two_powr_minus_int_float)
2.224 @@ -910,18 +954,17 @@
2.225  lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
2.226    is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
2.227
2.228 -(* TODO: optimize using zmod_zmult2_eq, pdivmod ? *)
2.229  lemma compute_rapprox_posrat[code]:
2.230    fixes prec x y
2.231 +  notes divmod_int_mod_div[simp]
2.232    defines "l \<equiv> rat_precision prec x y"
2.233    shows "rapprox_posrat prec x y = (let
2.234       l = l ;
2.235       X = if 0 \<le> l then (x * 2^nat l, y) else (x, y * 2^nat(-l)) ;
2.236 -     d = fst X div snd X ;
2.237 -     m = fst X mod snd X
2.238 +     (d, m) = divmod_int (fst X) (snd X)
2.239     in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
2.240  proof (cases "y = 0")
2.241 -  assume "y = 0" thus ?thesis unfolding normfloat_def by transfer simp
2.242 +  assume "y = 0" thus ?thesis by transfer simp
2.243  next
2.244    assume "y \<noteq> 0"
2.245    show ?thesis
2.246 @@ -932,7 +975,6 @@
2.247      moreover have "real x * 2 powr real l = real x'"
2.248        by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
2.249      ultimately show ?thesis
2.250 -      unfolding normfloat_def
2.251        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
2.252          l_def[symmetric, THEN meta_eq_to_obj_eq]
2.253        by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
2.254 @@ -945,7 +987,6 @@
2.255        using `\<not> 0 \<le> l`
2.256        by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
2.257      ultimately show ?thesis
2.258 -      unfolding normfloat_def
2.259        using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
2.260          l_def[symmetric, THEN meta_eq_to_obj_eq]
2.261        by transfer
2.262 @@ -966,41 +1007,9 @@
2.264  qed
2.265
2.266 -lemma power_aux:
2.267 -  assumes "x > 0"
2.268 -  shows "(2::int) ^ nat (x - 1) \<le> 2 ^ nat x - 1"
2.269 -proof -
2.270 -  def y \<equiv> "nat (x - 1)"
2.271 -  moreover
2.272 -  have "(2::int) ^ y \<le> (2 ^ (y + 1)) - 1" by simp
2.273 -  ultimately show ?thesis using assms by simp
2.274 -qed
2.275 -
2.276  lemma rapprox_posrat_less1:
2.277 -  assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
2.278 -  shows "real (rapprox_posrat n x y) < 1"
2.279 -proof -
2.280 -  have powr1: "2 powr real (rat_precision n (int x) (int y)) =
2.281 -    2 ^ nat (rat_precision n (int x) (int y))" using rat_precision_pos[of x y n] assms
2.282 -    by (simp add: powr_realpow[symmetric])
2.283 -  have "x * 2 powr real (rat_precision n (int x) (int y)) / y = (x / y) *
2.284 -     2 powr real (rat_precision n (int x) (int y))" by simp
2.285 -  also have "... < (1 / 2) * 2 powr real (rat_precision n (int x) (int y))"
2.286 -    apply (rule mult_strict_right_mono) by (insert assms) auto
2.287 -  also have "\<dots> = 2 powr real (rat_precision n (int x) (int y) - 1)"
2.289 -  also have "\<dots> = 2 ^ nat (rat_precision n (int x) (int y) - 1)"
2.290 -    using rat_precision_pos[of x y n] assms by (simp add: powr_realpow[symmetric])
2.291 -  also have "\<dots> \<le> 2 ^ nat (rat_precision n (int x) (int y)) - 1"
2.292 -    unfolding int_of_reals real_of_int_le_iff
2.293 -    using rat_precision_pos[OF assms] by (rule power_aux)
2.294 -  finally show ?thesis
2.295 -    apply (transfer fixing: n x y)
2.296 -    apply (simp add: round_up_def field_simps powr_minus powr1)
2.297 -    unfolding int_of_reals real_of_int_less_iff
2.298 -    apply (simp add: ceiling_less_eq)
2.299 -    done
2.300 -qed
2.301 +  shows "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 2 * x < y \<Longrightarrow> 0 < n \<Longrightarrow> real (rapprox_posrat n x y) < 1"
2.302 +  by transfer (simp add: rat_precision_pos round_up_less1)
2.303
2.304  lift_definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
2.305    "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
2.306 @@ -1020,16 +1029,15 @@
2.307  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
2.308    "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
2.309
2.310 +lemma "rapprox_rat = rapprox_posrat"
2.311 +  by transfer auto
2.312 +
2.313 +lemma "lapprox_rat = lapprox_posrat"
2.314 +  by transfer auto
2.315 +
2.316  lemma compute_rapprox_rat[code]:
2.317 -  "rapprox_rat prec x y =
2.318 -    (if y = 0 then 0
2.319 -    else if 0 \<le> x then
2.320 -      (if 0 < y then rapprox_posrat prec (nat x) (nat y)
2.321 -      else - (lapprox_posrat prec (nat x) (nat (-y))))
2.322 -      else (if 0 < y
2.323 -        then - (lapprox_posrat prec (nat (-x)) (nat y))
2.324 -        else rapprox_posrat prec (nat (-x)) (nat (-y))))"
2.325 -  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
2.326 +  "rapprox_rat prec x y = - lapprox_rat prec (-x) y"
2.327 +  by transfer (simp add: round_down_uminus_eq)
2.328  hide_fact (open) compute_rapprox_rat
2.329
2.330  subsection {* Division *}
2.331 @@ -1063,22 +1071,10 @@
2.333
2.334  lemma compute_float_divr[code]:
2.335 -  "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
2.336 -proof cases
2.337 -  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
2.338 -  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
2.339 -  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
2.340 -  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)"
2.341 -    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
2.342 -  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
2.343 -    by (simp add: field_simps powr_divide2[symmetric])
2.344 +  "float_divr prec x y = - float_divl prec (-x) y"
2.345 +  by transfer (simp add: real_divr_def real_divl_def round_down_uminus_eq)
2.346 +hide_fact (open) compute_float_divr
2.347
2.348 -  show ?thesis
2.349 -    using not_0
2.350 -    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift real_divr_def,
2.352 -qed (transfer, auto simp: real_divr_def)
2.353 -hide_fact (open) compute_float_divr
2.354
2.355  subsection {* Lemmas needed by Approximate *}
2.356
2.357 @@ -1113,12 +1109,9 @@
2.358
2.359  lemma lapprox_rat_nonneg:
2.360    fixes n x y
2.361 -  defines "p \<equiv> int n - ((bitlen \<bar>x\<bar>) - (bitlen \<bar>y\<bar>))"
2.362 -  assumes "0 \<le> x" and "0 < y"
2.363 +  assumes "0 \<le> x" and "0 \<le> y"
2.364    shows "0 \<le> real (lapprox_rat n x y)"
2.365 -using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
2.366 -   powr_int[of 2, simplified]
2.367 -  by auto
2.368 +  using assms by (auto simp: lapprox_rat_def simp: round_down_nonneg)
2.369
2.370  lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
2.371    using round_up by (simp add: rapprox_rat_def)
2.372 @@ -1130,32 +1123,17 @@
2.373  proof -
2.374    have "bitlen \<bar>x\<bar> \<le> bitlen \<bar>y\<bar>"
2.375      using xy unfolding bitlen_def by (auto intro!: floor_mono)
2.376 -  then have "0 \<le> rat_precision n \<bar>x\<bar> \<bar>y\<bar>" by (simp add: rat_precision_def)
2.377 -  have "real \<lceil>real x / real y * 2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)\<rceil>
2.378 -      \<le> real \<lceil>2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)\<rceil>"
2.379 -    using xy by (auto intro!: ceiling_mono simp: field_simps)
2.380 -  also have "\<dots> = 2 powr real (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)"
2.381 -    using `0 \<le> rat_precision n \<bar>x\<bar> \<bar>y\<bar>`
2.382 -    by (auto intro!: exI[of _ "2^nat (rat_precision n \<bar>x\<bar> \<bar>y\<bar>)"] simp: powr_int)
2.383 -  finally show ?thesis
2.384 -    by (simp add: rapprox_rat_def round_up_def)
2.385 -       (simp add: powr_minus inverse_eq_divide)
2.386 +  from this assms show ?thesis
2.387 +    by transfer (auto intro!: round_up_le1 simp: rat_precision_def)
2.388  qed
2.389
2.390 -lemma rapprox_rat_nonneg_neg:
2.391 -  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
2.392 -  unfolding rapprox_rat_def round_up_def
2.393 -  by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
2.394 +lemma rapprox_rat_nonneg_nonpos:
2.395 +  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
2.396 +  by transfer (simp add: round_up_le0 divide_nonneg_nonpos)
2.397
2.398 -lemma rapprox_rat_neg:
2.399 -  "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
2.400 -  unfolding rapprox_rat_def round_up_def
2.401 -  by (auto simp: field_simps mult_le_0_iff)
2.402 -
2.403 -lemma rapprox_rat_nonpos_pos:
2.404 -  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
2.405 -  unfolding rapprox_rat_def round_up_def
2.406 -  by (auto simp: field_simps mult_le_0_iff)
2.407 +lemma rapprox_rat_nonpos_nonneg:
2.408 +  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
2.409 +  by transfer (simp add: round_up_le0 divide_nonpos_nonneg)
2.410
2.411  lemma real_divl: "real_divl prec x y \<le> x / y"
2.412    by (simp add: real_divl_def round_down)
2.413 @@ -1168,7 +1146,7 @@
2.414
2.415  lemma real_divl_lower_bound:
2.416    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y"
2.417 -  by (simp add: real_divl_def round_down_def zero_le_mult_iff zero_le_divide_iff)
2.418 +  by (simp add: real_divl_def round_down_nonneg)
2.419
2.420  lemma float_divl_lower_bound:
2.421    "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
2.422 @@ -1202,82 +1180,45 @@
2.423  qed
2.424
2.425  lemma real_divl_pos_less1_bound:
2.426 -  "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real_divl prec 1 x"
2.427 -proof (unfold real_divl_def)
2.428 -  fix prec :: nat and x :: real assume x: "0 < x" "x < 1" and prec: "1 \<le> prec"
2.429 -  def p \<equiv> "int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor>"
2.430 -  show "1 \<le> round_down (int prec + \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - \<lfloor>log 2 \<bar>1\<bar>\<rfloor>) (1 / x) "
2.431 -  proof cases
2.432 -    assume nonneg: "0 \<le> p"
2.433 -    hence "2 powr real (p) = floor (real ((2::int) ^ nat p)) * floor (1::real)"
2.434 -      by (simp add: powr_int del: real_of_int_power) simp
2.435 -    also have "floor (1::real) \<le> floor (1 / x)" using x prec by simp
2.436 -    also have "floor (real ((2::int) ^ nat p)) * floor (1 / x) \<le>
2.437 -      floor (real ((2::int) ^ nat p) * (1 / x))"
2.438 -      by (rule le_mult_floor) (auto simp: x prec less_imp_le)
2.439 -    finally have "2 powr real p \<le> floor (2 powr nat p / x)" by (simp add: powr_realpow)
2.440 -    thus ?thesis unfolding p_def[symmetric]
2.441 -      using x prec nonneg by (simp add: powr_minus inverse_eq_divide round_down_def)
2.442 -  next
2.443 -    assume neg: "\<not> 0 \<le> p"
2.444 -
2.445 -    have "x = 2 powr (log 2 x)"
2.446 -      using x by simp
2.447 -    also have "2 powr (log 2 x) \<le> 2 powr p"
2.448 -    proof (rule powr_mono)
2.449 -      have "log 2 x \<le> \<lceil>log 2 x\<rceil>"
2.450 -        by simp
2.451 -      also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + 1"
2.452 -        using ceiling_diff_floor_le_1[of "log 2 x"] by simp
2.453 -      also have "\<dots> \<le> \<lfloor>log 2 x\<rfloor> + prec"
2.454 -        using prec by simp
2.455 -      finally show "log 2 x \<le> real p"
2.456 -        using x by (simp add: p_def)
2.457 -    qed simp
2.458 -    finally have x_le: "x \<le> 2 powr p" .
2.459 -
2.460 -    from neg have "2 powr real p \<le> 2 powr 0"
2.461 -      by (intro powr_mono) auto
2.462 -    also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
2.463 -    also have "\<dots> \<le> \<lfloor>2 powr real p / x\<rfloor>" unfolding real_of_int_le_iff
2.464 -      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq)
2.465 -    finally show ?thesis
2.466 -      using prec x unfolding p_def[symmetric]
2.467 -      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
2.468 -  qed
2.469 +  assumes "0 < x" "x \<le> 1" "prec \<ge> 1"
2.470 +  shows "1 \<le> real_divl prec 1 x"
2.471 +proof -
2.472 +  have "log 2 x \<le> real prec + real \<lfloor>log 2 x\<rfloor>" using `prec \<ge> 1` by arith
2.473 +  from this assms show ?thesis
2.474 +    by (simp add: real_divl_def log_divide round_down_ge1)
2.475  qed
2.476
2.477  lemma float_divl_pos_less1_bound:
2.478 -  "0 < real x \<Longrightarrow> real x < 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
2.479 +  "0 < real x \<Longrightarrow> real x \<le> 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
2.480    by (transfer, rule real_divl_pos_less1_bound)
2.481
2.482  lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
2.483    by transfer (rule real_divr)
2.484
2.485 -lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> real_divr prec 1 x"
2.486 +lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x \<le> 1" shows "1 \<le> real_divr prec 1 x"
2.487  proof -
2.488 -  have "1 \<le> 1 / x" using `0 < x` and `x < 1` by auto
2.489 +  have "1 \<le> 1 / x" using `0 < x` and `x <= 1` by auto
2.490    also have "\<dots> \<le> real_divr prec 1 x" using real_divr[where x=1 and y=x] by auto
2.491    finally show ?thesis by auto
2.492  qed
2.493
2.494 -lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x"
2.495 +lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x"
2.496    by transfer (rule real_divr_pos_less1_lower_bound)
2.497
2.498  lemma real_divr_nonpos_pos_upper_bound:
2.499 -  "x \<le> 0 \<Longrightarrow> 0 < y \<Longrightarrow> real_divr prec x y \<le> 0"
2.500 -  by (auto simp: field_simps mult_le_0_iff divide_le_0_iff round_up_def real_divr_def)
2.501 +  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_divr prec x y \<le> 0"
2.502 +  by (simp add: real_divr_def round_up_le0 divide_le_0_iff)
2.503
2.504  lemma float_divr_nonpos_pos_upper_bound:
2.505 -  "real x \<le> 0 \<Longrightarrow> 0 < real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
2.506 +  "real x \<le> 0 \<Longrightarrow> 0 \<le> real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
2.507    by transfer (rule real_divr_nonpos_pos_upper_bound)
2.508
2.509  lemma real_divr_nonneg_neg_upper_bound:
2.510 -  "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> real_divr prec x y \<le> 0"
2.511 -  by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff divide_le_0_iff round_up_def real_divr_def)
2.512 +  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_divr prec x y \<le> 0"
2.513 +  by (simp add: real_divr_def round_up_le0 divide_le_0_iff)
2.514
2.515  lemma float_divr_nonneg_neg_upper_bound:
2.516 -  "0 \<le> real x \<Longrightarrow> real y < 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
2.517 +  "0 \<le> real x \<Longrightarrow> real y \<le> 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
2.518    by transfer (rule real_divr_nonneg_neg_upper_bound)
2.519
2.520  definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real" where
2.521 @@ -1301,6 +1242,10 @@
2.522  lemma truncate_up_zero[simp]: "truncate_up prec 0 = 0"
2.524
2.525 +lemma truncate_up_uminus_eq: "truncate_up prec (-x) = - truncate_down prec x"
2.526 +  and truncate_down_uminus_eq: "truncate_down prec (-x) = - truncate_up prec x"
2.527 +  by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
2.528 +
2.529  lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up
2.531
2.532 @@ -1326,19 +1271,10 @@
2.533  hide_fact (open) compute_float_round_down
2.534
2.535  lemma compute_float_round_up[code]:
2.536 -  "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
2.537 -     if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P
2.538 -                   in Float (n + (if r = 0 then 0 else 1)) (e + d)
2.539 -              else Float m e)"
2.540 -  using Float.compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
2.541 -  unfolding Let_def
2.542 -  by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_up_def
2.543 -    cong del: if_weak_cong)
2.544 +  "float_round_up prec x = - float_round_down prec (-x)"
2.545 +  by transfer (simp add: truncate_down_uminus_eq)
2.546  hide_fact (open) compute_float_round_up
2.547
2.548 -lemma round_up_mono: "x \<le> y \<Longrightarrow> round_up p x \<le> round_up p y"
2.549 -  by (auto intro!: ceiling_mono simp: round_up_def)
2.550 -
2.551  lemma truncate_up_nonneg_mono:
2.552    assumes "0 \<le> x" "x \<le> y"
2.553    shows "truncate_up prec x \<le> truncate_up prec y"
2.554 @@ -1453,16 +1389,6 @@
2.555    finally show ?thesis .
2.556  qed
2.557
2.558 -lemma truncate_up_uminus_truncate_down:
2.559 -  "truncate_up prec x = - truncate_down prec (- x)"
2.560 -  "truncate_up prec (-x) = - truncate_down prec x"
2.561 -  by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
2.562 -
2.563 -lemma truncate_down_uminus_truncate_up:
2.564 -  "truncate_down prec x = - truncate_up prec (- x)"
2.565 -  "truncate_down prec (-x) = - truncate_up prec x"
2.566 -  by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
2.567 -
2.568  lemma truncate_down_nonneg_mono:
2.569    assumes "0 \<le> x" "x \<le> y"
2.570    shows "truncate_down prec x \<le> truncate_down prec y"
2.571 @@ -1522,16 +1448,20 @@
2.572    } ultimately show ?thesis by blast
2.573  qed
2.574
2.575 +lemma truncate_down_eq_truncate_up: "truncate_down p x = - truncate_up p (-x)"
2.576 +  and truncate_up_eq_truncate_down: "truncate_up p x = - truncate_down p (-x)"
2.577 +  by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)
2.578 +
2.579  lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
2.580    apply (cases "0 \<le> x")
2.581    apply (rule truncate_down_nonneg_mono, assumption+)
2.582 -  apply (simp add: truncate_down_uminus_truncate_up)
2.583 +  apply (simp add: truncate_down_eq_truncate_up)
2.584    apply (cases "0 \<le> y")
2.585    apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
2.586    done
2.587
2.588  lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
2.589 -  by (simp add: truncate_up_uminus_truncate_down truncate_down_mono)
2.590 +  by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
2.591
2.592  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
2.593   apply (auto simp: zero_float_def mult_le_0_iff)
```