simplified computations based on round_up by reducing to round_down;
authorimmler
Wed Nov 12 17:36:29 2014 +0100 (2014-11-12)
changeset 5898227e7e3f9e665
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
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Float.thy
     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.16    by transfer (auto simp add: powr_add zmod_eq_0_iff)
    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.29 +  real_of_int_add
    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.39 +  real_of_nat_add
    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.54    by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
    2.55      (simp add: powr_add[symmetric])
    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.72 +    by (simp add: round_up_def) (simp add: powr_minus inverse_eq_divide)
    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.152 -  unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
   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.179 -    by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow
   2.180 -      intro: exI[where x="m*2^nat (e+p)"])
   2.181 -  then show ?thesis using `\<not> p + e < 0`
   2.182 -    by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus)
   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.191 -  real_of_int_add
   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.201 -  real_of_nat_add
   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.263      using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
   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.288 -    using powr_add [of 2 _ "- 1", simplified add_uminus_conv_diff] by (simp add: powr_minus)
   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.332    by (simp add: real_divr_def)
   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.351 -      simp add: field_simps)
   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.523    by (simp add: truncate_up_def)
   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.530    by (simp add: truncate_up_def)
   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)