241 from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp |
241 from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp |
242 { |
242 { |
243 fix x y z :: real |
243 fix x y z :: real |
244 assume "y \<noteq> 0" |
244 assume "y \<noteq> 0" |
245 then have "(x * inverse y = z) = (x = z * y)" |
245 then have "(x * inverse y = z) = (x = z * y)" |
246 by auto |
246 by auto |
247 } |
247 } |
248 note inverse = this |
248 note inverse = this |
249 have eq': "real a * (pow2 (b - b')) = real a'" |
249 have eq': "real a * (pow2 (b - b')) = real a'" |
250 apply (subst diff_int_def) |
250 apply (subst diff_int_def) |
251 apply (subst pow2_add) |
251 apply (subst pow2_add) |
549 also have "\<dots> \<le> x" using `0 < x` by auto |
549 also have "\<dots> \<le> x" using `0 < x` by auto |
550 finally have "2^nat (1 + bitlen (x div 2) - 1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto |
550 finally have "2^nat (1 + bitlen (x div 2) - 1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto |
551 } moreover |
551 } moreover |
552 { have "x + 1 \<le> x - x mod 2 + 2" |
552 { have "x + 1 \<le> x - x mod 2 + 2" |
553 proof - |
553 proof - |
554 have "x mod 2 < 2" using `0 < x` by auto |
554 have "x mod 2 < 2" using `0 < x` by auto |
555 hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto |
555 hence "x < x - x mod 2 + 2" unfolding algebra_simps by auto |
556 thus ?thesis by auto |
556 thus ?thesis by auto |
557 qed |
557 qed |
558 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 |
558 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 |
559 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) |
559 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) |
560 also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto |
560 also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto |
561 finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" . |
561 finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" . |
837 hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto |
837 hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto |
838 |
838 |
839 have "0 < ?X div y" |
839 have "0 < ?X div y" |
840 proof - |
840 proof - |
841 have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)" |
841 have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)" |
842 using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto |
842 using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto |
843 hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans) |
843 hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans) |
844 hence "bitlen x \<le> bitlen y" by auto |
844 hence "bitlen x \<le> bitlen y" by auto |
845 hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto |
845 hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto |
846 |
846 |
847 have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto |
847 have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto |
848 |
848 |
849 have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l" |
849 have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l" |
850 using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto |
850 using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto |
851 |
851 |
852 have "y * 2^nat (bitlen x - 1) \<le> y * x" |
852 have "y * 2^nat (bitlen x - 1) \<le> y * x" |
853 using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono) |
853 using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono) |
854 also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono) |
854 also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono) |
855 also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`) |
855 also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`) |
856 finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))" |
856 finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))" |
857 unfolding real_of_int_le_iff[symmetric] by auto |
857 unfolding real_of_int_le_iff[symmetric] by auto |
858 hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" |
858 hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" |
859 unfolding real_mult_assoc real_divide_def by auto |
859 unfolding real_mult_assoc real_divide_def by auto |
860 also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto |
860 also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto |
861 finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto |
861 finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto |
862 thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto |
862 thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto |
863 qed |
863 qed |
864 |
864 |
1192 show ?thesis |
1192 show ?thesis |
1193 proof (cases "m mod ?p = 0") |
1193 proof (cases "m mod ?p = 0") |
1194 case True |
1194 case True |
1195 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] . |
1195 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] . |
1196 have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real] |
1196 have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real] |
1197 by (auto simp add: pow2_add `0 < ?d` pow_d) |
1197 by (auto simp add: pow2_add `0 < ?d` pow_d) |
1198 thus ?thesis |
1198 thus ?thesis |
1199 unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`] |
1199 unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`] |
1200 by auto |
1200 by auto |
1201 next |
1201 next |
1202 case False |
1202 case False |
1203 have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. |
1203 have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] .. |
1204 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]) |
1204 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]) |
1205 finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e] |
1205 finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e] |
1206 unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] |
1206 unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric] |
1207 by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
1207 by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d) |
1208 thus ?thesis |
1208 thus ?thesis |
1209 unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] . |
1209 unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] . |
1210 qed |
1210 qed |
1211 next |
1211 next |
1212 case False |
1212 case False |
1213 show ?thesis |
1213 show ?thesis |
1214 unfolding Float round_up.simps Let_def if_not_P[OF False] .. |
1214 unfolding Float round_up.simps Let_def if_not_P[OF False] .. |
1262 next |
1262 next |
1263 case True |
1263 case True |
1264 have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m" |
1264 have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m" |
1265 proof - |
1265 proof - |
1266 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] |
1266 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] |
1267 using `?l > 0` by auto |
1267 using `?l > 0` by auto |
1268 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 |
1268 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 |
1269 also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] .. |
1269 also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] .. |
1270 finally show ?thesis by auto |
1270 finally show ?thesis by auto |
1271 qed |
1271 qed |
1272 thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto |
1272 thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto |