src/HOL/Library/Float.thy
changeset 47165 9344891b504b
parent 47108 2a1953f0d20d
child 47230 6584098d5378
     1.1 --- a/src/HOL/Library/Float.thy	Tue Mar 27 16:04:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Mar 27 19:21:05 2012 +0200
     1.3 @@ -488,7 +488,7 @@
     1.4          hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
     1.5          thus ?thesis by auto
     1.6        qed
     1.7 -      also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto
     1.8 +      also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` div_mod_equality[of x 2 0] by auto
     1.9        also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
    1.10        also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
    1.11        finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
    1.12 @@ -1122,7 +1122,7 @@
    1.13      show ?thesis
    1.14      proof (cases "m mod ?p = 0")
    1.15        case True
    1.16 -      have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
    1.17 +      have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using mod_div_equality [symmetric] .
    1.18        have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
    1.19          by (auto simp add: pow2_add `0 < ?d` pow_d)
    1.20        thus ?thesis
    1.21 @@ -1130,7 +1130,7 @@
    1.22          by auto
    1.23      next
    1.24        case False
    1.25 -      have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    1.26 +      have "m = m div ?p * ?p + m mod ?p" unfolding mod_div_equality ..
    1.27        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.28        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.29          unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
    1.30 @@ -1156,7 +1156,7 @@
    1.31      case True
    1.32      hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    1.33      have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
    1.34 -    also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    1.35 +    also have "\<dots> \<le> m" unfolding mod_div_equality ..
    1.36      finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
    1.37        unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
    1.38        by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)