src/HOL/Library/Float.thy
changeset 44766 d4d33a4d7548
parent 42676 8724f20bf69c
child 45495 c55a07526dbe
     1.1 --- a/src/HOL/Library/Float.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -719,11 +719,11 @@
     1.4    shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
     1.5  proof -
     1.6    have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
     1.7 -    by (rule zadd_left_mono, 
     1.8 +    by (rule add_left_mono, 
     1.9          auto intro!: mult_nonneg_nonneg 
    1.10               simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
    1.11    hence "real (x div y) * real c \<le> real (x * c div y)" 
    1.12 -    unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
    1.13 +    unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto
    1.14    hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
    1.15      using `0 < c` by auto
    1.16    thus ?thesis unfolding mult_assoc using `0 < c` by auto
    1.17 @@ -777,7 +777,7 @@
    1.18  
    1.19      have "?X = y * (?X div y) + ?X mod y" by auto
    1.20      also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le])
    1.21 -    also have "\<dots> = y * (?X div y + 1)" unfolding zadd_zmult_distrib2 by auto
    1.22 +    also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto
    1.23      finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
    1.24      hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)" 
    1.25        by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
    1.26 @@ -1144,7 +1144,7 @@
    1.27      have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
    1.28        using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
    1.29      also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
    1.30 -      unfolding pow_split zpower_zadd_distrib by auto
    1.31 +      unfolding pow_split power_add by auto
    1.32      finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
    1.33        using `0 < m` by (rule zdiv_mono1)
    1.34      hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
    1.35 @@ -1273,7 +1273,7 @@
    1.36      next
    1.37        case False
    1.38        have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    1.39 -      also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    1.40 +      also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    1.41        finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
    1.42          unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    1.43          by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
    1.44 @@ -1361,7 +1361,7 @@
    1.45      have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l"
    1.46      proof -
    1.47        have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto
    1.48 -      hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding zmult_1 real_of_int_less_iff[symmetric] by auto
    1.49 +      hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding mult_1 real_of_int_less_iff[symmetric] by auto
    1.50        
    1.51        have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
    1.52        also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto