--- a/src/HOL/Decision_Procs/Approximation.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Oct 17 14:43:18 2009 +0200
@@ -175,16 +175,16 @@
proof (cases "u < 0")
case True hence "0 \<le> - real u" and "- real u \<le> - x" and "0 \<le> - x" and "-x \<le> - real l" using assms unfolding less_float_def by auto
hence "real u ^ n \<le> x ^ n" and "x ^ n \<le> real l ^ n" using power_mono[of "-x" "-real l" n] power_mono[of "-real u" "-x" n]
- unfolding power_minus_even[OF `even n`] by auto
+ unfolding power_minus_even[OF `even n`] by auto
moreover have u1: "u1 = l ^ n" and l1: "l1 = u ^ n" using assms unfolding float_power_bnds_def if_not_P[OF P] if_P[OF True] by auto
ultimately show ?thesis using float_power by auto
next
case False
have "\<bar>x\<bar> \<le> real (max (-l) u)"
proof (cases "-l \<le> u")
- case True thus ?thesis unfolding max_def if_P[OF True] using assms unfolding le_float_def by auto
+ case True thus ?thesis unfolding max_def if_P[OF True] using assms unfolding le_float_def by auto
next
- case False thus ?thesis unfolding max_def if_not_P[OF False] using assms unfolding le_float_def by auto
+ case False thus ?thesis unfolding max_def if_not_P[OF False] using assms unfolding le_float_def by auto
qed
hence x_abs: "\<bar>x\<bar> \<le> \<bar>real (max (-l) u)\<bar>" by auto
have u1: "u1 = (max (-l) u) ^ n" and l1: "l1 = 0" using assms unfolding float_power_bnds_def if_not_P[OF P] if_not_P[OF False] by auto
@@ -258,7 +258,7 @@
also have "\<dots> < 1 * pow2 (e + int (nat (bitlen m)))"
proof (rule mult_strict_right_mono, auto)
show "real m < 2^nat (bitlen m)" using bitlen_bounds[OF `0 < m`, THEN conjunct2]
- unfolding real_of_int_less_iff[of m, symmetric] by auto
+ unfolding real_of_int_less_iff[of m, symmetric] by auto
qed
finally have "sqrt (real x) < sqrt (pow2 (e + bitlen m))" unfolding int_nat_bl by auto
also have "\<dots> \<le> pow2 ((e + bitlen m) div 2 + 1)"
@@ -266,26 +266,26 @@
let ?E = "e + bitlen m"
have E_mod_pow: "pow2 (?E mod 2) < 4"
proof (cases "?E mod 2 = 1")
- case True thus ?thesis by auto
+ case True thus ?thesis by auto
next
- case False
- have "0 \<le> ?E mod 2" by auto
- have "?E mod 2 < 2" by auto
- from this[THEN zless_imp_add1_zle]
- have "?E mod 2 \<le> 0" using False by auto
- from xt1(5)[OF `0 \<le> ?E mod 2` this]
- show ?thesis by auto
+ case False
+ have "0 \<le> ?E mod 2" by auto
+ have "?E mod 2 < 2" by auto
+ from this[THEN zless_imp_add1_zle]
+ have "?E mod 2 \<le> 0" using False by auto
+ from xt1(5)[OF `0 \<le> ?E mod 2` this]
+ show ?thesis by auto
qed
hence "sqrt (pow2 (?E mod 2)) < sqrt (2 * 2)" by auto
hence E_mod_pow: "sqrt (pow2 (?E mod 2)) < 2" unfolding real_sqrt_abs2 by auto
have E_eq: "pow2 ?E = pow2 (?E div 2 + ?E div 2 + ?E mod 2)" by auto
have "sqrt (pow2 ?E) = sqrt (pow2 (?E div 2) * pow2 (?E div 2) * pow2 (?E mod 2))"
- unfolding E_eq unfolding pow2_add ..
+ unfolding E_eq unfolding pow2_add ..
also have "\<dots> = pow2 (?E div 2) * sqrt (pow2 (?E mod 2))"
- unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
+ unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
also have "\<dots> < pow2 (?E div 2) * 2"
- by (rule mult_strict_left_mono, auto intro: E_mod_pow)
+ by (rule mult_strict_left_mono, auto intro: E_mod_pow)
also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
finally show ?thesis by auto
qed
@@ -338,7 +338,7 @@
mult_pos_pos[OF order_less_trans[OF sqrt_gt0 sqrt_ub] sqrt_gt0]])
also have "\<dots> = sqrt (real x)"
unfolding inverse_eq_iff_eq[of _ "sqrt (real x)", symmetric]
- sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
+ sqrt_divide_self_eq[OF `0 \<le> real x`, symmetric] by auto
finally have "real (lb_sqrt prec x) \<le> sqrt (real x)"
unfolding lb_sqrt.simps if_P[OF `0 < x`] by auto }
note lb = this
@@ -605,7 +605,7 @@
have "real x \<le> sqrt (real (1 + x * x))" using real_sqrt_sum_squares_ge2[where x=1, unfolded numeral_2_eq_2] by auto
also have "\<dots> \<le> real (ub_sqrt prec (1 + x * x))"
- using bnds_sqrt'[of "1 + x * x"] by auto
+ using bnds_sqrt'[of "1 + x * x"] by auto
finally have "real x \<le> real ?fR" by auto
moreover have "real ?DIV \<le> real x / real ?fR" by (rule float_divl)
ultimately have "real ?DIV \<le> 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto
@@ -613,9 +613,9 @@
have "0 \<le> real ?DIV" using float_divl_lower_bound[OF `0 \<le> x` `0 < ?fR`] unfolding le_float_def by auto
have "real (Float 1 1 * ?lb_horner ?DIV) \<le> 2 * arctan (real (float_divl prec x ?fR))" unfolding real_of_float_mult[of "Float 1 1"] Float_num
- using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
+ using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
also have "\<dots> \<le> 2 * arctan (real x / ?R)"
- using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
+ using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
next
@@ -628,26 +628,26 @@
show ?thesis
proof (cases "1 < ?invx")
- case True
- show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
- using `0 \<le> arctan (real x)` by auto
+ case True
+ show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF False] if_P[OF True]
+ using `0 \<le> arctan (real x)` by auto
next
- case False
- hence "real ?invx \<le> 1" unfolding less_float_def by auto
- have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
-
- have "1 / real x \<noteq> 0" and "0 < 1 / real x" using `0 < real x` by auto
-
- have "arctan (1 / real x) \<le> arctan (real ?invx)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr)
- also have "\<dots> \<le> real (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
- finally have "pi / 2 - real (?ub_horner ?invx) \<le> arctan (real x)"
- using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
- unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
- moreover
- have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
- ultimately
- show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
- by auto
+ case False
+ hence "real ?invx \<le> 1" unfolding less_float_def by auto
+ have "0 \<le> real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \<le> real x`)
+
+ have "1 / real x \<noteq> 0" and "0 < 1 / real x" using `0 < real x` by auto
+
+ have "arctan (1 / real x) \<le> arctan (real ?invx)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr)
+ also have "\<dots> \<le> real (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
+ finally have "pi / 2 - real (?ub_horner ?invx) \<le> arctan (real x)"
+ using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
+ unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
+ moreover
+ have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
+ ultimately
+ show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
+ by auto
qed
qed
qed
@@ -695,23 +695,23 @@
case True
show ?thesis
proof (cases "?DIV > 1")
- case True
- have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
- from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
- show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
+ case True
+ have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
+ from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
+ show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
next
- case False
- hence "real ?DIV \<le> 1" unfolding less_float_def by auto
-
- have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
- hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
-
- have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
- also have "\<dots> \<le> 2 * arctan (real ?DIV)"
- using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
- also have "\<dots> \<le> real (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num
- using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
- finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
+ case False
+ hence "real ?DIV \<le> 1" unfolding less_float_def by auto
+
+ have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
+ hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
+
+ have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
+ also have "\<dots> \<le> 2 * arctan (real ?DIV)"
+ using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
+ also have "\<dots> \<le> real (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num
+ using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
+ finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_not_P[OF False] .
qed
next
case False
@@ -731,13 +731,13 @@
have "real (?lb_horner ?invx) \<le> arctan (real ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
also have "\<dots> \<le> arctan (1 / real x)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divl)
finally have "arctan (real x) \<le> pi / 2 - real (?lb_horner ?invx)"
- using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
- unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
+ using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
+ unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
moreover
have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_right using pi_boundaries by auto
ultimately
show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
- by auto
+ by auto
qed
qed
qed
@@ -848,12 +848,12 @@
{
assume "even n"
have "real (lb_sin_cos_aux prec n 1 1 (x * x)) \<le> ?SUM"
- unfolding morph_to_if_power[symmetric] using cos_aux by auto
+ unfolding morph_to_if_power[symmetric] using cos_aux by auto
also have "\<dots> \<le> cos (real x)"
proof -
- from even[OF `even n`] `0 < ?fact` `0 < ?pow`
- have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
- thus ?thesis unfolding cos_eq by auto
+ from even[OF `even n`] `0 < ?fact` `0 < ?pow`
+ have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+ thus ?thesis unfolding cos_eq by auto
qed
finally have "real (lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos (real x)" .
} note lb = this
@@ -862,13 +862,13 @@
assume "odd n"
have "cos (real x) \<le> ?SUM"
proof -
- from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
- have "0 \<le> (- ?rest) / ?fact * ?pow"
- by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
- thus ?thesis unfolding cos_eq by auto
+ from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
+ have "0 \<le> (- ?rest) / ?fact * ?pow"
+ by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+ thus ?thesis unfolding cos_eq by auto
qed
also have "\<dots> \<le> real (ub_sin_cos_aux prec n 1 1 (x * x))"
- unfolding morph_to_if_power[symmetric] using cos_aux by auto
+ unfolding morph_to_if_power[symmetric] using cos_aux by auto
finally have "cos (real x) \<le> real (ub_sin_cos_aux prec n 1 1 (x * x))" .
} note ub = this and lb
} note ub = this(1) and lb = this(2)
@@ -931,9 +931,9 @@
have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
- unfolding sum_split_even_odd ..
+ unfolding sum_split_even_odd ..
also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else -1 ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
- by (rule setsum_cong2) auto
+ by (rule setsum_cong2) auto
finally show ?thesis by assumption
qed } note setsum_morph = this
@@ -958,13 +958,13 @@
assume "even n"
have "real (x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
(\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
- using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
+ using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
also have "\<dots> \<le> ?SUM" by auto
also have "\<dots> \<le> sin (real x)"
proof -
- from even[OF `even n`] `0 < ?fact` `0 < ?pow`
- have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
- thus ?thesis unfolding sin_eq by auto
+ from even[OF `even n`] `0 < ?fact` `0 < ?pow`
+ have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+ thus ?thesis unfolding sin_eq by auto
qed
finally have "real (x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin (real x)" .
} note lb = this
@@ -973,15 +973,15 @@
assume "odd n"
have "sin (real x) \<le> ?SUM"
proof -
- from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
- have "0 \<le> (- ?rest) / ?fact * ?pow"
- by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
- thus ?thesis unfolding sin_eq by auto
+ from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`]
+ have "0 \<le> (- ?rest) / ?fact * ?pow"
+ by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+ thus ?thesis unfolding sin_eq by auto
qed
also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
- by auto
+ by auto
also have "\<dots> \<le> real (x * ub_sin_cos_aux prec n 2 1 (x * x))"
- using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
+ using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
finally have "sin (real x) \<le> real (x * ub_sin_cos_aux prec n 2 1 (x * x))" .
} note ub = this and lb
} note ub = this(1) and lb = this(2)
@@ -1058,15 +1058,15 @@
have "real (?lb_half y) \<le> cos (real x)"
proof (cases "y < 0")
- case True show ?thesis using cos_ge_minus_one unfolding if_P[OF True] by auto
+ case True show ?thesis using cos_ge_minus_one unfolding if_P[OF True] by auto
next
- case False
- hence "0 \<le> real y" unfolding less_float_def by auto
- from mult_mono[OF `real y \<le> cos ?x2` `real y \<le> cos ?x2` `0 \<le> cos ?x2` this]
- have "real y * real y \<le> cos ?x2 * cos ?x2" .
- hence "2 * real y * real y \<le> 2 * cos ?x2 * cos ?x2" by auto
- hence "2 * real y * real y - 1 \<le> 2 * cos (real x / 2) * cos (real x / 2) - 1" unfolding Float_num real_of_float_mult by auto
- thus ?thesis unfolding if_not_P[OF False] x_half Float_num real_of_float_mult real_of_float_sub by auto
+ case False
+ hence "0 \<le> real y" unfolding less_float_def by auto
+ from mult_mono[OF `real y \<le> cos ?x2` `real y \<le> cos ?x2` `0 \<le> cos ?x2` this]
+ have "real y * real y \<le> cos ?x2 * cos ?x2" .
+ hence "2 * real y * real y \<le> 2 * cos ?x2 * cos ?x2" by auto
+ hence "2 * real y * real y - 1 \<le> 2 * cos (real x / 2) * cos (real x / 2) - 1" unfolding Float_num real_of_float_mult by auto
+ thus ?thesis unfolding if_not_P[OF False] x_half Float_num real_of_float_mult real_of_float_sub by auto
qed
} note lb_half = this
@@ -1077,12 +1077,12 @@
have "cos (real x) \<le> real (?ub_half y)"
proof -
- have "0 \<le> real y" using `0 \<le> cos ?x2` ub by (rule order_trans)
- from mult_mono[OF ub ub this `0 \<le> cos ?x2`]
- have "cos ?x2 * cos ?x2 \<le> real y * real y" .
- hence "2 * cos ?x2 * cos ?x2 \<le> 2 * real y * real y" by auto
- hence "2 * cos (real x / 2) * cos (real x / 2) - 1 \<le> 2 * real y * real y - 1" unfolding Float_num real_of_float_mult by auto
- thus ?thesis unfolding x_half real_of_float_mult Float_num real_of_float_sub by auto
+ have "0 \<le> real y" using `0 \<le> cos ?x2` ub by (rule order_trans)
+ from mult_mono[OF ub ub this `0 \<le> cos ?x2`]
+ have "cos ?x2 * cos ?x2 \<le> real y * real y" .
+ hence "2 * cos ?x2 * cos ?x2 \<le> 2 * real y * real y" by auto
+ hence "2 * cos (real x / 2) * cos (real x / 2) - 1 \<le> 2 * real y * real y - 1" unfolding Float_num real_of_float_mult by auto
+ thus ?thesis unfolding x_half real_of_float_mult Float_num real_of_float_sub by auto
qed
} note ub_half = this
@@ -1100,13 +1100,13 @@
have "real (?lb x) \<le> ?cos x"
proof -
- from lb_half[OF lb `-pi \<le> real x` `real x \<le> pi`]
- show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+ from lb_half[OF lb `-pi \<le> real x` `real x \<le> pi`]
+ show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
qed
moreover have "?cos x \<le> real (?ub x)"
proof -
- from ub_half[OF ub `-pi \<le> real x` `real x \<le> pi`]
- show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
+ from ub_half[OF ub `-pi \<le> real x` `real x \<le> pi`]
+ show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\<not> x < 0` `\<not> x < Float 1 -1` `x < 1` by auto
qed
ultimately show ?thesis by auto
next
@@ -1119,15 +1119,15 @@
have "real (?lb x) \<le> ?cos x"
proof -
- have "-pi \<le> real ?x2" and "real ?x2 \<le> pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \<le> real x` `real x \<le> pi` by auto
- from lb_half[OF lb_half[OF lb this] `-pi \<le> real x` `real x \<le> pi`, unfolded eq_4]
- show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+ have "-pi \<le> real ?x2" and "real ?x2 \<le> pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \<le> real x` `real x \<le> pi` by auto
+ from lb_half[OF lb_half[OF lb this] `-pi \<le> real x` `real x \<le> pi`, unfolded eq_4]
+ show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
qed
moreover have "?cos x \<le> real (?ub x)"
proof -
- have "-pi \<le> real ?x2" and "real ?x2 \<le> pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \<le> real x` `real x \<le> pi` by auto
- from ub_half[OF ub_half[OF ub this] `-pi \<le> real x` `real x \<le> pi`, unfolded eq_4]
- show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
+ have "-pi \<le> real ?x2" and "real ?x2 \<le> pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \<le> real x` `real x \<le> pi` by auto
+ from ub_half[OF ub_half[OF ub this] `-pi \<le> real x` `real x \<le> pi`, unfolded eq_4]
+ show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x < Float 1 -1`] if_not_P[OF `\<not> x < 1`] Let_def .
qed
ultimately show ?thesis by auto
qed
@@ -1227,7 +1227,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus real_diff_def mult_minus_left)
finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
unfolding cos_periodic_int . }
note negative_lx = this
@@ -1240,7 +1240,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
using cos_monotone_0_pi'[OF lx_0 lx pi_x]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus real_diff_def mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec ?lx)"
using lb_cos[OF lx_0 pi_lx] by simp
finally have "cos x \<le> real (ub_cos prec ?lx)"
@@ -1255,7 +1255,7 @@
have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus real_diff_def mult_minus_left)
also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
finally have "cos x \<le> real (ub_cos prec (- ?ux))"
@@ -1272,7 +1272,7 @@
also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
by (simp only: real_of_float_minus real_of_int_minus
- cos_minus real_diff_def mult_minus_left)
+ cos_minus real_diff_def mult_minus_left)
finally have "real (lb_cos prec ?ux) \<le> cos x"
unfolding cos_periodic_int . }
note positive_ux = this
@@ -1332,26 +1332,26 @@
hence "x - real k * 2 * pi - 2 * pi \<le> 0" using ux by simp
have ux_0: "real (?ux - 2 * ?lpi) \<le> 0"
- using Cond by (auto simp add: le_float_def)
+ using Cond by (auto simp add: le_float_def)
from 2 and Cond have "\<not> ?ux \<le> ?lpi" by auto
hence "- ?lpi \<le> ?ux - 2 * ?lpi" by (auto simp add: le_float_def)
hence pi_ux: "- pi \<le> real (?ux - 2 * ?lpi)"
- using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
+ using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
have x_le_ux: "x - real k * 2 * pi - 2 * pi \<le> real (?ux - 2 * ?lpi)"
- using ux lpi by auto
+ using ux lpi by auto
have "cos x = cos (x + real (-k) * 2 * pi + real (-1 :: int) * 2 * pi)"
- unfolding cos_periodic_int ..
+ unfolding cos_periodic_int ..
also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
- using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
- by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min real_diff_def mult_minus_left real_mult_1)
+ using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
+ by (simp only: real_of_float_minus real_of_int_minus real_of_one
+ number_of_Min real_diff_def mult_minus_left real_mult_1)
also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
- unfolding real_of_float_minus cos_minus ..
+ unfolding real_of_float_minus cos_minus ..
also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
- using lb_cos_minus[OF pi_ux ux_0] by simp
+ using lb_cos_minus[OF pi_ux ux_0] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
qed
thus ?thesis unfolding l by auto
@@ -1376,24 +1376,24 @@
hence "0 \<le> x - real k * 2 * pi + 2 * pi" using lx by simp
have lx_0: "0 \<le> real (?lx + 2 * ?lpi)"
- using Cond lpi by (auto simp add: le_float_def)
+ using Cond lpi by (auto simp add: le_float_def)
from 1 and Cond have "\<not> -?lpi \<le> ?lx" by auto
hence "?lx + 2 * ?lpi \<le> ?lpi" by (auto simp add: le_float_def)
hence pi_lx: "real (?lx + 2 * ?lpi) \<le> pi"
- using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
+ using lpi[THEN le_imp_neg_le] by (auto simp add: le_float_def)
have lx_le_x: "real (?lx + 2 * ?lpi) \<le> x - real k * 2 * pi + 2 * pi"
- using lx lpi by auto
+ using lx lpi by auto
have "cos x = cos (x + real (-k) * 2 * pi + real (1 :: int) * 2 * pi)"
- unfolding cos_periodic_int ..
+ unfolding cos_periodic_int ..
also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
- using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
- by (simp only: real_of_float_minus real_of_int_minus real_of_one
- number_of_Min real_diff_def mult_minus_left real_mult_1)
+ using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
+ by (simp only: real_of_float_minus real_of_int_minus real_of_one
+ number_of_Min real_diff_def mult_minus_left real_mult_1)
also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
- using lb_cos[OF lx_0 pi_lx] by simp
+ using lb_cos[OF lx_0 pi_lx] by simp
finally show ?thesis unfolding u by (simp add: real_of_float_max)
qed
thus ?thesis unfolding l by auto
@@ -1427,11 +1427,11 @@
also have "\<dots> \<le> exp (real x)"
proof -
obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp (real x) = (\<Sum>m = 0..<get_even n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
- using Maclaurin_exp_le by blast
+ using Maclaurin_exp_le by blast
moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
- by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: get_even zero_le_even_power exp_gt_zero)
+ by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: get_even zero_le_even_power exp_gt_zero)
ultimately show ?thesis
- using get_odd exp_gt_zero by (auto intro!: pordered_cancel_semiring_class.mult_nonneg_nonneg)
+ using get_odd exp_gt_zero by (auto intro!: pordered_cancel_semiring_class.mult_nonneg_nonneg)
qed
finally have "real (lb_exp_horner prec (get_even n) 1 1 x) \<le> exp (real x)" .
} moreover
@@ -1548,14 +1548,14 @@
have "exp (real x) \<le> real (ub_exp prec x)"
proof -
have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
- using float_divr_nonpos_pos_upper_bound[OF `x \<le> 0` `0 < - floor_fl x`] unfolding le_float_def real_of_float_0 .
+ using float_divr_nonpos_pos_upper_bound[OF `x \<le> 0` `0 < - floor_fl x`] unfolding le_float_def real_of_float_0 .
have "exp (real x) = exp (real ?num * (real x / real ?num))" using `real ?num \<noteq> 0` by auto
also have "\<dots> = exp (real x / real ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
also have "\<dots> \<le> exp (real (float_divr prec x (- floor_fl x))) ^ ?num" unfolding num_eq
- by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
+ by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
also have "\<dots> \<le> real ((?ub_exp_horner (float_divr prec x (- floor_fl x))) ^ ?num)" unfolding float_power
- by (rule power_mono, rule bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct2], auto)
+ by (rule power_mono, rule bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct2], auto)
finally show ?thesis unfolding ub_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def .
qed
moreover
@@ -1566,32 +1566,32 @@
show ?thesis
proof (cases "?horner \<le> 0")
- case False hence "0 \<le> real ?horner" unfolding le_float_def by auto
-
- have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
- using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
-
- have "real ((?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num) \<le>
+ case False hence "0 \<le> real ?horner" unfolding le_float_def by auto
+
+ have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
+ using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
+
+ have "real ((?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num) \<le>
exp (real (float_divl prec x (- floor_fl x))) ^ ?num" unfolding float_power
- using `0 \<le> real ?horner`[unfolded Float_floor[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
- also have "\<dots> \<le> exp (real x / real ?num) ^ ?num" unfolding num_eq
- using float_divl by (auto intro!: power_mono simp del: real_of_float_minus)
- also have "\<dots> = exp (real ?num * (real x / real ?num))" unfolding exp_real_of_nat_mult ..
- also have "\<dots> = exp (real x)" using `real ?num \<noteq> 0` by auto
- finally show ?thesis
- unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_not_P[OF False] by auto
+ using `0 \<le> real ?horner`[unfolded Float_floor[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
+ also have "\<dots> \<le> exp (real x / real ?num) ^ ?num" unfolding num_eq
+ using float_divl by (auto intro!: power_mono simp del: real_of_float_minus)
+ also have "\<dots> = exp (real ?num * (real x / real ?num))" unfolding exp_real_of_nat_mult ..
+ also have "\<dots> = exp (real x)" using `real ?num \<noteq> 0` by auto
+ finally show ?thesis
+ unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_not_P[OF False] by auto
next
- case True
- have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
- from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
- have "- 1 \<le> real x / real (- floor_fl x)" unfolding real_of_float_minus by auto
- from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
- have "real (Float 1 -2) \<le> exp (real x / real (- floor_fl x))" unfolding Float_num .
- hence "real (Float 1 -2) ^ ?num \<le> exp (real x / real (- floor_fl x)) ^ ?num"
- by (auto intro!: power_mono simp add: Float_num)
- also have "\<dots> = exp (real x)" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
- finally show ?thesis
- unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_P[OF True] float_power .
+ case True
+ have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
+ from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
+ have "- 1 \<le> real x / real (- floor_fl x)" unfolding real_of_float_minus by auto
+ from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
+ have "real (Float 1 -2) \<le> exp (real x / real (- floor_fl x))" unfolding Float_num .
+ hence "real (Float 1 -2) ^ ?num \<le> exp (real x / real (- floor_fl x)) ^ ?num"
+ by (auto intro!: power_mono simp add: Float_num)
+ also have "\<dots> = exp (real x)" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
+ finally show ?thesis
+ unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_P[OF True] float_power .
qed
qed
ultimately show ?thesis by auto
@@ -1614,8 +1614,8 @@
have "real (float_divl prec 1 (ub_exp prec (-x))) \<le> 1 / real (ub_exp prec (-x))" using float_divl[where x=1] by auto
also have "\<dots> \<le> exp (real x)"
- using ub_exp[unfolded inverse_le_iff_le[OF order_less_le_trans[OF exp_gt_zero ub_exp] exp_gt_zero, symmetric]]
- unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide by auto
+ using ub_exp[unfolded inverse_le_iff_le[OF order_less_le_trans[OF exp_gt_zero ub_exp] exp_gt_zero, symmetric]]
+ unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide by auto
finally show ?thesis unfolding lb_exp.simps if_P[OF True] .
qed
moreover
@@ -1627,9 +1627,9 @@
have lb_exp: "real (lb_exp prec (-x)) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
have "exp (real x) \<le> real (1 :: float) / real (lb_exp prec (-x))"
- using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_0],
- symmetric]]
- unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide real_of_float_1 by auto
+ using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\<not> 0 < -x`, unfolded less_float_def real_of_float_0],
+ symmetric]]
+ unfolding exp_minus nonzero_inverse_inverse_eq[OF exp_not_eq_zero] inverse_eq_divide real_of_float_1 by auto
also have "\<dots> \<le> real (float_divr prec 1 (lb_exp prec (-x)))" using float_divr .
finally show ?thesis unfolding ub_exp.simps if_P[OF True] .
qed
@@ -1683,7 +1683,7 @@
proof (rule mult_mono)
show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
- by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
+ by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
qed auto }
from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq]
@@ -1857,58 +1857,58 @@
let "?lb_horner x" = "x * lb_ln_horner prec (get_even prec) 1 x"
{ have up: "real (rapprox_rat prec 2 3) \<le> 1"
- by (rule rapprox_rat_le1) simp_all
+ by (rule rapprox_rat_le1) simp_all
have low: "2 / 3 \<le> real (rapprox_rat prec 2 3)"
- by (rule order_trans[OF _ rapprox_rat]) simp
+ by (rule order_trans[OF _ rapprox_rat]) simp
from mult_less_le_imp_less[OF * low] *
have pos: "0 < real (x * rapprox_rat prec 2 3 - 1)" by auto
have "ln (real x * 2/3)
- \<le> ln (real (x * rapprox_rat prec 2 3 - 1) + 1)"
+ \<le> ln (real (x * rapprox_rat prec 2 3 - 1) + 1)"
proof (rule ln_le_cancel_iff[symmetric, THEN iffD1])
- show "real x * 2 / 3 \<le> real (x * rapprox_rat prec 2 3 - 1) + 1"
- using * low by auto
- show "0 < real x * 2 / 3" using * by simp
- show "0 < real (x * rapprox_rat prec 2 3 - 1) + 1" using pos by auto
+ show "real x * 2 / 3 \<le> real (x * rapprox_rat prec 2 3 - 1) + 1"
+ using * low by auto
+ show "0 < real x * 2 / 3" using * by simp
+ show "0 < real (x * rapprox_rat prec 2 3 - 1) + 1" using pos by auto
qed
also have "\<dots> \<le> real (?ub_horner (x * rapprox_rat prec 2 3 - 1))"
proof (rule ln_float_bounds(2))
- from mult_less_le_imp_less[OF `real x < 2` up] low *
- show "real (x * rapprox_rat prec 2 3 - 1) < 1" by auto
- show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
+ from mult_less_le_imp_less[OF `real x < 2` up] low *
+ show "real (x * rapprox_rat prec 2 3 - 1) < 1" by auto
+ show "0 \<le> real (x * rapprox_rat prec 2 3 - 1)" using pos by auto
qed
finally have "ln (real x)
- \<le> real (?ub_horner (Float 1 -1))
- + real (?ub_horner (x * rapprox_rat prec 2 3 - 1))"
- using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
+ \<le> real (?ub_horner (Float 1 -1))
+ + real (?ub_horner (x * rapprox_rat prec 2 3 - 1))"
+ using ln_float_bounds(2)[of "Float 1 -1" prec prec] add by auto }
moreover
{ let ?max = "max (x * lapprox_rat prec 2 3 - 1) 0"
have up: "real (lapprox_rat prec 2 3) \<le> 2/3"
- by (rule order_trans[OF lapprox_rat], simp)
+ by (rule order_trans[OF lapprox_rat], simp)
have low: "0 \<le> real (lapprox_rat prec 2 3)"
- using lapprox_rat_bottom[of 2 3 prec] by simp
+ using lapprox_rat_bottom[of 2 3 prec] by simp
have "real (?lb_horner ?max)
- \<le> ln (real ?max + 1)"
+ \<le> ln (real ?max + 1)"
proof (rule ln_float_bounds(1))
- from mult_less_le_imp_less[OF `real x < 2` up] * low
- show "real ?max < 1" by (cases "real (lapprox_rat prec 2 3) = 0",
- auto simp add: real_of_float_max)
- show "0 \<le> real ?max" by (auto simp add: real_of_float_max)
+ from mult_less_le_imp_less[OF `real x < 2` up] * low
+ show "real ?max < 1" by (cases "real (lapprox_rat prec 2 3) = 0",
+ auto simp add: real_of_float_max)
+ show "0 \<le> real ?max" by (auto simp add: real_of_float_max)
qed
also have "\<dots> \<le> ln (real x * 2/3)"
proof (rule ln_le_cancel_iff[symmetric, THEN iffD1])
- show "0 < real ?max + 1" by (auto simp add: real_of_float_max)
- show "0 < real x * 2/3" using * by auto
- show "real ?max + 1 \<le> real x * 2/3" using * up
- by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
- auto simp add: real_of_float_max min_max.sup_absorb1)
+ show "0 < real ?max + 1" by (auto simp add: real_of_float_max)
+ show "0 < real x * 2/3" using * by auto
+ show "real ?max + 1 \<le> real x * 2/3" using * up
+ by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
+ auto simp add: real_of_float_max min_max.sup_absorb1)
qed
finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
- \<le> ln (real x)"
- using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
+ \<le> ln (real x)"
+ using ln_float_bounds(1)[of "Float 1 -1" prec prec] add by auto }
ultimately
show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps Let_def
using `\<not> x \<le> 0` `\<not> x < 1` True False by auto
@@ -1928,12 +1928,12 @@
{
have "real (lb_ln2 prec * ?s) \<le> ln 2 * real (e + (bitlen m - 1))" (is "?lb2 \<le> _")
- unfolding real_of_float_mult real_of_float_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
- using lb_ln2[of prec]
+ unfolding real_of_float_mult real_of_float_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
+ using lb_ln2[of prec]
proof (rule mult_right_mono)
- have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
- from float_gt1_scale[OF this]
- show "0 \<le> real (e + (bitlen m - 1))" by auto
+ have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
+ from float_gt1_scale[OF this]
+ show "0 \<le> real (e + (bitlen m - 1))" by auto
qed
moreover
from bitlen_div[OF `0 < m`, unfolded normalized_float[OF `m \<noteq> 0`, symmetric]]
@@ -1941,7 +1941,7 @@
from ln_float_bounds(1)[OF this]
have "real ((?x - 1) * lb_ln_horner prec (get_even prec) 1 (?x - 1)) \<le> ln (real ?x)" (is "?lb_horner \<le> _") by auto
ultimately have "?lb2 + ?lb_horner \<le> ln (real x)"
- unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
+ unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
}
moreover
{
@@ -1951,15 +1951,15 @@
have "ln (real ?x) \<le> real ((?x - 1) * ub_ln_horner prec (get_odd prec) 1 (?x - 1))" (is "_ \<le> ?ub_horner") by auto
moreover
have "ln 2 * real (e + (bitlen m - 1)) \<le> real (ub_ln2 prec * ?s)" (is "_ \<le> ?ub2")
- unfolding real_of_float_mult real_of_float_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
- using ub_ln2[of prec]
+ unfolding real_of_float_mult real_of_float_ge0_exp[OF order_refl] nat_0 power_0 mult_1_right
+ using ub_ln2[of prec]
proof (rule mult_right_mono)
- have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
- from float_gt1_scale[OF this]
- show "0 \<le> real (e + (bitlen m - 1))" by auto
+ have "1 \<le> Float m e" using `1 \<le> x` Float unfolding le_float_def by auto
+ from float_gt1_scale[OF this]
+ show "0 \<le> real (e + (bitlen m - 1))" by auto
qed
ultimately have "ln (real x) \<le> ?ub2 + ?ub_horner"
- unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
+ unfolding Float ln_shifted_float[OF `0 < m`, of e] by auto
}
ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
@@ -2413,7 +2413,7 @@
unfolding less_float_def using l1_le_u1 l1 by auto
show ?thesis
unfolding inverse_le_iff_le[OF `0 < real u1` `0 < interpret_floatarith a xs`]
- inverse_le_iff_le[OF `0 < interpret_floatarith a xs` `0 < real l1`]
+ inverse_le_iff_le[OF `0 < interpret_floatarith a xs` `0 < real l1`]
using l1 u1 by auto
next
case False hence "u1 < 0" using either by blast
@@ -2421,7 +2421,7 @@
unfolding less_float_def using l1_le_u1 u1 by auto
show ?thesis
unfolding inverse_le_iff_le_neg[OF `real u1 < 0` `interpret_floatarith a xs < 0`]
- inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
+ inverse_le_iff_le_neg[OF `interpret_floatarith a xs < 0` `real l1 < 0`]
using l1 u1 by auto
qed
@@ -2767,11 +2767,11 @@
proof (cases "i = j")
case True
thus ?thesis using `vs ! i = Some (l, u)` Some and bnd `i < length ?xs`
- by auto
+ by auto
next
case False
thus ?thesis using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some
- by auto
+ by auto
qed
qed auto }
thus ?thesis unfolding bounded_by_def by auto
@@ -2878,7 +2878,7 @@
note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
from approx[OF this ap]
have "(interpret_floatarith f (xs[x := t])) \<in> {real l .. real u}"
- by (auto simp add: algebra_simps)
+ by (auto simp add: algebra_simps)
} thus ?thesis by (auto intro!: exI[of _ 0])
next
case True
@@ -2904,7 +2904,7 @@
{ fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
have "(f ^^ Suc n) x = (f ^^ n) (f x)"
- by (induct n, auto) }
+ by (induct n, auto) }
note funpow_Suc = this[symmetric]
from Suc.hyps[OF ate, unfolded this]
obtain n
@@ -2918,14 +2918,14 @@
assume "m < Suc n" and bnd_z: "z \<in> { real lx .. real ux }"
have "DERIV (?f m) z :> ?f (Suc m) z"
proof (cases m)
- case 0
- with DERIV_floatarith[OF `x < length xs` isDERIV_approx'[OF `bounded_by xs vs` bnd_x bnd_z True]]
- show ?thesis by simp
+ case 0
+ with DERIV_floatarith[OF `x < length xs` isDERIV_approx'[OF `bounded_by xs vs` bnd_x bnd_z True]]
+ show ?thesis by simp
next
- case (Suc m')
- hence "m' < n" using `m < Suc n` by auto
- from DERIV_hyp[OF this bnd_z]
- show ?thesis using Suc by simp
+ case (Suc m')
+ hence "m' < n" using `m < Suc n` by auto
+ from DERIV_hyp[OF this bnd_z]
+ show ?thesis using Suc by simp
qed } note DERIV = this
have "\<And> k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
@@ -2937,20 +2937,20 @@
{ fix t assume t: "t \<in> {real lx .. real ux}"
hence "bounded_by [xs!x] [vs!x]"
- using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
- by (cases "vs!x", auto simp add: bounded_by_def)
+ using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
+ by (cases "vs!x", auto simp add: bounded_by_def)
with hyp[THEN bspec, OF t] f_c
have "bounded_by [?f 0 (real c), ?X (Suc k) f n t, xs!x] [Some (l1, u1), Some (l2, u2), vs!x]"
- by (auto intro!: bounded_by_Cons)
+ by (auto intro!: bounded_by_Cons)
from approx[OF this final, unfolded atLeastAtMost_iff[symmetric]]
have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) \<in> {real l .. real u}"
- by (auto simp add: algebra_simps)
+ by (auto simp add: algebra_simps)
also have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) =
(\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
- unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
- by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
+ unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
+ by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
finally have "?T \<in> {real l .. real u}" . }
thus ?thesis using DERIV by blast
qed
@@ -2999,24 +2999,24 @@
proof (cases "xs ! x = real c")
case True
from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis
- unfolding F_def Suc setsum_head_upt_Suc[OF zero_less_Suc] setsum_shift_bounds_Suc_ivl by auto
+ unfolding F_def Suc setsum_head_upt_Suc[OF zero_less_Suc] setsum_shift_bounds_Suc_ivl by auto
next
case False
have "real lx \<le> real c" "real c \<le> real ux" "real lx \<le> xs!x" "xs!x \<le> real ux"
- using Suc bnd_c `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
+ using Suc bnd_c `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
obtain t where t_bnd: "if xs ! x < real c then xs ! x < t \<and> t < real c else real c < t \<and> t < xs ! x"
- and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
- (\<Sum>m = 0..<Suc n'. F m (real c) / real (fact m) * (xs ! x - real c) ^ m) +
+ and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
+ (\<Sum>m = 0..<Suc n'. F m (real c) / real (fact m) * (xs ! x - real c) ^ m) +
F (Suc n') t / real (fact (Suc n')) * (xs ! x - real c) ^ Suc n'"
- by blast
+ by blast
from t_bnd bnd_xs bnd_c have *: "t \<in> {real lx .. real ux}"
- by (cases "xs ! x < real c", auto)
+ by (cases "xs ! x < real c", auto)
have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t"
- unfolding fl_eq Suc by (auto simp add: algebra_simps divide_inverse)
+ unfolding fl_eq Suc by (auto simp add: algebra_simps divide_inverse)
also have "\<dots> \<in> {real l .. real u}" using * by (rule hyp)
finally show ?thesis by simp
qed
@@ -3154,22 +3154,22 @@
case (Less lf rt)
with Bound a b assms
have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 < l)"
- unfolding approx_tse_form_def by auto
+ unfolding approx_tse_form_def by auto
from approx_tse_form'_less[OF this bnd]
show ?thesis using Less by auto
next
case (LessEqual lf rt)
with Bound a b assms
have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
- unfolding approx_tse_form_def by auto
+ unfolding approx_tse_form_def by auto
from approx_tse_form'_le[OF this bnd]
show ?thesis using LessEqual by auto
next
case (AtLeastAtMost x lf rt)
with Bound a b assms
have "approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)"
- and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
- unfolding approx_tse_form_def lazy_conj by auto
+ and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
+ unfolding approx_tse_form_def lazy_conj by auto
from approx_tse_form'_le[OF this(1) bnd] approx_tse_form'_le[OF this(2) bnd]
show ?thesis using AtLeastAtMost by auto
next