src/HOL/Decision_Procs/Approximation_Bounds.thy
changeset 70350 571ae57313a4
parent 70347 e5cd5471c18a
     1.1 --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -2540,16 +2540,16 @@
     1.4      have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e]
     1.5        by (auto simp add: zero_less_mult_iff)
     1.6      define bl where "bl = bitlen m - 1"
     1.7 +    then have bitlen: "bitlen m = bl + 1"
     1.8 +      by simp
     1.9      hence "bl \<ge> 0"
    1.10 -      using \<open>m > 0\<close> by (simp add: bitlen_alt_def)
    1.11 +      using \<open>m > 0\<close> by (auto simp add: bitlen_alt_def)
    1.12      have "1 \<le> Float m e"
    1.13        using \<open>1 \<le> x\<close> Float unfolding less_eq_float_def by auto
    1.14      from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
    1.15      have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
    1.16 -      unfolding bl_def[symmetric]
    1.17 -      by (auto simp: powr_realpow[symmetric] field_simps)
    1.18 -         (auto simp : powr_minus field_simps)
    1.19 -
    1.20 +      using abs_real_le_2_powr_bitlen [of m] \<open>m > 0\<close>
    1.21 +      by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps)
    1.22      {
    1.23        have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
    1.24            (is "real_of_float ?lb2 \<le> _")