src/HOL/Library/Float.thy
changeset 56536 aefb4a8da31f
parent 56479 91958d4b30f7
child 56544 b60d5d119489
     1.1 --- a/src/HOL/Library/Float.thy	Fri Apr 11 12:43:22 2014 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Fri Apr 11 13:36:57 2014 +0200
     1.3 @@ -618,7 +618,7 @@
     1.4    using round_up_correct[of e f] by simp
     1.5  
     1.6  lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
     1.7 -  by (auto simp: round_down_def intro!: mult_nonneg_nonneg)
     1.8 +  by (auto simp: round_down_def)
     1.9  
    1.10  lemma ceil_divide_floor_conv:
    1.11  assumes "b \<noteq> 0"
    1.12 @@ -1418,20 +1418,20 @@
    1.13      by simp
    1.14    moreover
    1.15    have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
    1.16 -    using `x > 0` by (auto intro: mult_nonneg_nonneg)
    1.17 +    using `x > 0` by auto
    1.18    ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
    1.19      by simp
    1.20    also have "\<dots> \<subseteq> {0}" by auto
    1.21    finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
    1.22    with assms show ?thesis
    1.23 -    by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    1.24 +    by (auto simp: truncate_down_def round_down_def)
    1.25  qed
    1.26  
    1.27  lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
    1.28 -  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    1.29 +  by (auto simp: truncate_down_def round_down_def)
    1.30  
    1.31  lemma truncate_down_zero: "truncate_down prec 0 = 0"
    1.32 -  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    1.33 +  by (auto simp: truncate_down_def round_down_def)
    1.34  
    1.35  lemma truncate_down_switch_sign_mono:
    1.36    assumes "x \<le> 0" "0 \<le> y"
    1.37 @@ -1485,7 +1485,7 @@
    1.38        by simp
    1.39      also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
    1.40        using `0 \<le> y` `0 \<le> x` assms(2)
    1.41 -      by (auto intro!: powr_mono mult_nonneg_nonneg mult_pos_pos divide_left_mono
    1.42 +      by (auto intro!: powr_mono mult_pos_pos divide_left_mono
    1.43          simp: real_of_nat_diff powr_add
    1.44          powr_divide2[symmetric])
    1.45      also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"