src/HOL/Library/Float.thy
changeset 35344 e0b46cd72414
parent 35032 7efe662e41b4
child 36778 739a9379e29b
     1.1 --- a/src/HOL/Library/Float.thy	Tue Feb 23 07:45:54 2010 -0800
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Feb 23 10:37:25 2010 -0800
     1.3 @@ -789,12 +789,12 @@
     1.4      hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
     1.5  
     1.6      from real_of_int_div4[of "?X" y]
     1.7 -    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of .
     1.8 +    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
     1.9      also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
    1.10      finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
    1.11      hence "?X div y + 1 \<le> 2^?l" by auto
    1.12      hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
    1.13 -      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
    1.14 +      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
    1.15        by (rule mult_right_mono, auto)
    1.16      hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
    1.17      thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
    1.18 @@ -863,12 +863,12 @@
    1.19      qed
    1.20  
    1.21      from real_of_int_div4[of "?X" y]
    1.22 -    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power[symmetric] real_number_of .
    1.23 +    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
    1.24      also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
    1.25      finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
    1.26      hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
    1.27      hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
    1.28 -      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
    1.29 +      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
    1.30        by (rule mult_strict_right_mono, auto)
    1.31      hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
    1.32      thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
    1.33 @@ -1188,7 +1188,7 @@
    1.34    show "?thesis"
    1.35    proof (cases "0 < ?d")
    1.36      case True
    1.37 -    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
    1.38 +    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    1.39      show ?thesis
    1.40      proof (cases "m mod ?p = 0")
    1.41        case True
    1.42 @@ -1224,7 +1224,7 @@
    1.43    show "?thesis"
    1.44    proof (cases "0 < ?d")
    1.45      case True
    1.46 -    hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
    1.47 +    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
    1.48      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.49      also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
    1.50      finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
    1.51 @@ -1263,7 +1263,7 @@
    1.52      case True
    1.53      have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
    1.54      proof -
    1.55 -      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power[symmetric] real_number_of unfolding pow2_int[symmetric] 
    1.56 +      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] 
    1.57          using `?l > 0` by auto
    1.58        also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
    1.59        also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
    1.60 @@ -1329,7 +1329,7 @@
    1.61      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
    1.62      have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
    1.63      also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
    1.64 -    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
    1.65 +    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
    1.66      also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
    1.67      finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
    1.68    next
    1.69 @@ -1357,7 +1357,7 @@
    1.70      case False
    1.71      hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
    1.72      have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
    1.73 -    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
    1.74 +    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
    1.75      also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
    1.76      also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
    1.77      finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .