src/HOL/Library/Float.thy
changeset 70347 e5cd5471c18a
parent 69593 3dda49e08b9d
child 70355 a80ad0ac0837
     1.1 --- a/src/HOL/Library/Float.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Float.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -495,10 +495,10 @@
     1.4    by (auto simp: mantissa_exponent sign_simps)
     1.5  
     1.6  lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
     1.7 -  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
     1.8 +  by (auto simp: mantissa_exponent sign_simps)
     1.9  
    1.10  lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
    1.11 -  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
    1.12 +  by (auto simp: mantissa_exponent sign_simps)
    1.13  
    1.14  lemma
    1.15    fixes m e :: int
    1.16 @@ -1788,8 +1788,8 @@
    1.17    using truncate_down_uminus_eq[of p "x + y"]
    1.18    by transfer (simp add: plus_down_def plus_up_def ac_simps)
    1.19  
    1.20 -lemma mantissa_zero[simp]: "mantissa 0 = 0"
    1.21 -  by (metis mantissa_0 zero_float.abs_eq)
    1.22 +lemma mantissa_zero: "mantissa 0 = 0"
    1.23 +  by (fact mantissa_0)
    1.24  
    1.25  qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (float_plus_down 0 b (- a))"
    1.26    using truncate_down[of 0 "b - a"] truncate_down_pos[of "b - a" 0]
    1.27 @@ -1972,8 +1972,10 @@
    1.28      from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
    1.29        by auto
    1.30      with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
    1.31 -    have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
    1.32 -      by (metis floor_less_cancel linorder_cases not_le)+
    1.33 +    have logless: "log 2 x < log 2 y"
    1.34 +      by linarith
    1.35 +    have flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
    1.36 +      using \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> \<open>log 2 x \<le> log 2 y\<close> by linarith
    1.37      have "truncate_up prec x =
    1.38        real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> )\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)"
    1.39        using assms by (simp add: truncate_up_def round_up_def)