diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Decision_Procs/Approximation.thy --- 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 \ - real u" and "- real u \ - x" and "0 \ - x" and "-x \ - real l" using assms unfolding less_float_def by auto hence "real u ^ n \ x ^ n" and "x ^ n \ 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 "\x\ \ real (max (-l) u)" proof (cases "-l \ 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: "\x\ \ \real (max (-l) u)\" 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 "\ < 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 "\ \ 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 \ ?E mod 2" by auto - have "?E mod 2 < 2" by auto - from this[THEN zless_imp_add1_zle] - have "?E mod 2 \ 0" using False by auto - from xt1(5)[OF `0 \ ?E mod 2` this] - show ?thesis by auto + case False + have "0 \ ?E mod 2" by auto + have "?E mod 2 < 2" by auto + from this[THEN zless_imp_add1_zle] + have "?E mod 2 \ 0" using False by auto + from xt1(5)[OF `0 \ ?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 "\ = 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 "\ < 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 "\ = 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 "\ = sqrt (real x)" unfolding inverse_eq_iff_eq[of _ "sqrt (real x)", symmetric] - sqrt_divide_self_eq[OF `0 \ real x`, symmetric] by auto + sqrt_divide_self_eq[OF `0 \ real x`, symmetric] by auto finally have "real (lb_sqrt prec x) \ sqrt (real x)" unfolding lb_sqrt.simps if_P[OF `0 < x`] by auto } note lb = this @@ -605,7 +605,7 @@ have "real x \ sqrt (real (1 + x * x))" using real_sqrt_sum_squares_ge2[where x=1, unfolded numeral_2_eq_2] by auto also have "\ \ 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 \ real ?fR" by auto moreover have "real ?DIV \ real x / real ?fR" by (rule float_divl) ultimately have "real ?DIV \ 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto @@ -613,9 +613,9 @@ have "0 \ real ?DIV" using float_divl_lower_bound[OF `0 \ x` `0 < ?fR`] unfolding le_float_def by auto have "real (Float 1 1 * ?lb_horner ?DIV) \ 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 \ real ?DIV` `real ?DIV \ 1`] by auto + using arctan_0_1_bounds[OF `0 \ real ?DIV` `real ?DIV \ 1`] by auto also have "\ \ 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 `\ x < 0`] if_not_P[OF `\ x \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF False] if_P[OF True] - using `0 \ arctan (real x)` by auto + case True + show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF False] if_P[OF True] + using `0 \ arctan (real x)` by auto next - case False - hence "real ?invx \ 1" unfolding less_float_def by auto - have "0 \ real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \ real x`) - - have "1 / real x \ 0" and "0 < 1 / real x" using `0 < real x` by auto - - have "arctan (1 / real x) \ arctan (real ?invx)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr) - also have "\ \ real (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \ real ?invx` `real ?invx \ 1`] by auto - finally have "pi / 2 - real (?ub_horner ?invx) \ arctan (real x)" - using `0 \ arctan (real x)` arctan_inverse[OF `1 / real x \ 0`] - unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto - moreover - have "real (lb_pi prec * Float 1 -1) \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF `\ x \ Float 1 1`] if_not_P[OF False] - by auto + case False + hence "real ?invx \ 1" unfolding less_float_def by auto + have "0 \ real ?invx" by (rule order_trans[OF _ float_divr], auto simp add: `0 \ real x`) + + have "1 / real x \ 0" and "0 < 1 / real x" using `0 < real x` by auto + + have "arctan (1 / real x) \ arctan (real ?invx)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr) + also have "\ \ real (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \ real ?invx` `real ?invx \ 1`] by auto + finally have "pi / 2 - real (?ub_horner ?invx) \ arctan (real x)" + using `0 \ arctan (real x)` arctan_inverse[OF `1 / real x \ 0`] + unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto + moreover + have "real (lb_pi prec * Float 1 -1) \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF `\ x \ 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 \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_P[OF `x \ Float 1 1`] if_P[OF True] . + case True + have "pi / 2 \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_P[OF `x \ Float 1 1`] if_P[OF True] . next - case False - hence "real ?DIV \ 1" unfolding less_float_def by auto - - have "0 \ real x / ?R" using `0 \ real x` `0 < ?R` unfolding real_0_le_divide_iff by auto - hence "0 \ 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 "\ \ 2 * arctan (real ?DIV)" - using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono) - also have "\ \ 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 \ real ?DIV` `real ?DIV \ 1`] by auto - finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_P[OF `x \ Float 1 1`] if_not_P[OF False] . + case False + hence "real ?DIV \ 1" unfolding less_float_def by auto + + have "0 \ real x / ?R" using `0 \ real x` `0 < ?R` unfolding real_0_le_divide_iff by auto + hence "0 \ 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 "\ \ 2 * arctan (real ?DIV)" + using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono) + also have "\ \ 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 \ real ?DIV` `real ?DIV \ 1`] by auto + finally show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_P[OF `x \ Float 1 1`] if_not_P[OF False] . qed next case False @@ -731,13 +731,13 @@ have "real (?lb_horner ?invx) \ arctan (real ?invx)" using arctan_0_1_bounds[OF `0 \ real ?invx` `real ?invx \ 1`] by auto also have "\ \ arctan (1 / real x)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divl) finally have "arctan (real x) \ pi / 2 - real (?lb_horner ?invx)" - using `0 \ arctan (real x)` arctan_inverse[OF `1 / real x \ 0`] - unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto + using `0 \ arctan (real x)` arctan_inverse[OF `1 / real x \ 0`] + unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto moreover have "pi / 2 \ 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 `\ x < 0`] if_not_P[OF `\ x \ Float 1 -1`] if_not_P[OF `\ x \ 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)) \ ?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 "\ \ cos (real x)" proof - - from even[OF `even n`] `0 < ?fact` `0 < ?pow` - have "0 \ (?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 \ (?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)) \ cos (real x)" . } note lb = this @@ -862,13 +862,13 @@ assume "odd n" have "cos (real x) \ ?SUM" proof - - from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`] - have "0 \ (- ?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 \ (- ?rest) / ?fact * ?pow" + by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le) + thus ?thesis unfolding cos_eq by auto qed also have "\ \ 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) \ 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 = (\ j = 0 ..< n. 0) + ?SUM" by auto also have "\ = (\ 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 "\ = (\ 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)) \ (\ 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 \ real x`] unfolding setsum_morph[symmetric] by auto + using sin_aux[OF `0 \ real x`] unfolding setsum_morph[symmetric] by auto also have "\ \ ?SUM" by auto also have "\ \ sin (real x)" proof - - from even[OF `even n`] `0 < ?fact` `0 < ?pow` - have "0 \ (?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 \ (?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)) \ sin (real x)" . } note lb = this @@ -973,15 +973,15 @@ assume "odd n" have "sin (real x) \ ?SUM" proof - - from `0 < ?fact` and `0 < ?pow` and odd[OF `odd n`] - have "0 \ (- ?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 \ (- ?rest) / ?fact * ?pow" + by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le) + thus ?thesis unfolding sin_eq by auto qed also have "\ \ (\ 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 "\ \ real (x * ub_sin_cos_aux prec n 2 1 (x * x))" - using sin_aux[OF `0 \ real x`] unfolding setsum_morph[symmetric] by auto + using sin_aux[OF `0 \ real x`] unfolding setsum_morph[symmetric] by auto finally have "sin (real x) \ 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) \ 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 \ real y" unfolding less_float_def by auto - from mult_mono[OF `real y \ cos ?x2` `real y \ cos ?x2` `0 \ cos ?x2` this] - have "real y * real y \ cos ?x2 * cos ?x2" . - hence "2 * real y * real y \ 2 * cos ?x2 * cos ?x2" by auto - hence "2 * real y * real y - 1 \ 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 \ real y" unfolding less_float_def by auto + from mult_mono[OF `real y \ cos ?x2` `real y \ cos ?x2` `0 \ cos ?x2` this] + have "real y * real y \ cos ?x2 * cos ?x2" . + hence "2 * real y * real y \ 2 * cos ?x2 * cos ?x2" by auto + hence "2 * real y * real y - 1 \ 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) \ real (?ub_half y)" proof - - have "0 \ real y" using `0 \ cos ?x2` ub by (rule order_trans) - from mult_mono[OF ub ub this `0 \ cos ?x2`] - have "cos ?x2 * cos ?x2 \ real y * real y" . - hence "2 * cos ?x2 * cos ?x2 \ 2 * real y * real y" by auto - hence "2 * cos (real x / 2) * cos (real x / 2) - 1 \ 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 \ real y" using `0 \ cos ?x2` ub by (rule order_trans) + from mult_mono[OF ub ub this `0 \ cos ?x2`] + have "cos ?x2 * cos ?x2 \ real y * real y" . + hence "2 * cos ?x2 * cos ?x2 \ 2 * real y * real y" by auto + hence "2 * cos (real x / 2) * cos (real x / 2) - 1 \ 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) \ ?cos x" proof - - from lb_half[OF lb `-pi \ real x` `real x \ pi`] - show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\ x < 0` `\ x < Float 1 -1` `x < 1` by auto + from lb_half[OF lb `-pi \ real x` `real x \ pi`] + show ?thesis unfolding lb_cos_def[where x=x] Let_def using `\ x < 0` `\ x < Float 1 -1` `x < 1` by auto qed moreover have "?cos x \ real (?ub x)" proof - - from ub_half[OF ub `-pi \ real x` `real x \ pi`] - show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\ x < 0` `\ x < Float 1 -1` `x < 1` by auto + from ub_half[OF ub `-pi \ real x` `real x \ pi`] + show ?thesis unfolding ub_cos_def[where x=x] Let_def using `\ x < 0` `\ x < Float 1 -1` `x < 1` by auto qed ultimately show ?thesis by auto next @@ -1119,15 +1119,15 @@ have "real (?lb x) \ ?cos x" proof - - have "-pi \ real ?x2" and "real ?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` `real x \ pi` by auto - from lb_half[OF lb_half[OF lb this] `-pi \ real x` `real x \ pi`, unfolded eq_4] - show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\ x < 0`] if_not_P[OF `\ x < Float 1 -1`] if_not_P[OF `\ x < 1`] Let_def . + have "-pi \ real ?x2" and "real ?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` `real x \ pi` by auto + from lb_half[OF lb_half[OF lb this] `-pi \ real x` `real x \ pi`, unfolded eq_4] + show ?thesis unfolding lb_cos_def[where x=x] if_not_P[OF `\ x < 0`] if_not_P[OF `\ x < Float 1 -1`] if_not_P[OF `\ x < 1`] Let_def . qed moreover have "?cos x \ real (?ub x)" proof - - have "-pi \ real ?x2" and "real ?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` `real x \ pi` by auto - from ub_half[OF ub_half[OF ub this] `-pi \ real x` `real x \ pi`, unfolded eq_4] - show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\ x < 0`] if_not_P[OF `\ x < Float 1 -1`] if_not_P[OF `\ x < 1`] Let_def . + have "-pi \ real ?x2" and "real ?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` `real x \ pi` by auto + from ub_half[OF ub_half[OF ub this] `-pi \ real x` `real x \ pi`, unfolded eq_4] + show ?thesis unfolding ub_cos_def[where x=x] if_not_P[OF `\ x < 0`] if_not_P[OF `\ x < Float 1 -1`] if_not_P[OF `\ x < 1`] Let_def . qed ultimately show ?thesis by auto qed @@ -1227,7 +1227,7 @@ also have "\ \ 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)) \ cos x" unfolding cos_periodic_int . } note negative_lx = this @@ -1240,7 +1240,7 @@ have "cos (x + real (-k) * 2 * pi) \ 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 "\ \ real (ub_cos prec ?lx)" using lb_cos[OF lx_0 pi_lx] by simp finally have "cos x \ real (ub_cos prec ?lx)" @@ -1255,7 +1255,7 @@ have "cos (x + real (-k) * 2 * pi) \ 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 "\ \ real (ub_cos prec (- ?ux))" using lb_cos_minus[OF pi_ux ux_0, of prec] by simp finally have "cos x \ real (ub_cos prec (- ?ux))" @@ -1272,7 +1272,7 @@ also have "\ \ 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) \ cos x" unfolding cos_periodic_int . } note positive_ux = this @@ -1332,26 +1332,26 @@ hence "x - real k * 2 * pi - 2 * pi \ 0" using ux by simp have ux_0: "real (?ux - 2 * ?lpi) \ 0" - using Cond by (auto simp add: le_float_def) + using Cond by (auto simp add: le_float_def) from 2 and Cond have "\ ?ux \ ?lpi" by auto hence "- ?lpi \ ?ux - 2 * ?lpi" by (auto simp add: le_float_def) hence pi_ux: "- pi \ 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 \ 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 "\ \ 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 "\ = cos (real (- (?ux - 2 * ?lpi)))" - unfolding real_of_float_minus cos_minus .. + unfolding real_of_float_minus cos_minus .. also have "\ \ 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 \ x - real k * 2 * pi + 2 * pi" using lx by simp have lx_0: "0 \ 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 "\ -?lpi \ ?lx" by auto hence "?lx + 2 * ?lpi \ ?lpi" by (auto simp add: le_float_def) hence pi_lx: "real (?lx + 2 * ?lpi) \ 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) \ 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 "\ \ 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 "\ \ 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 "\ \ exp (real x)" proof - obtain t where "\t\ \ \real x\" and "exp (real x) = (\m = 0.. 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) \ exp (real x)" . } moreover @@ -1548,14 +1548,14 @@ have "exp (real x) \ real (ub_exp prec x)" proof - have div_less_zero: "real (float_divr prec x (- floor_fl x)) \ 0" - using float_divr_nonpos_pos_upper_bound[OF `x \ 0` `0 < - floor_fl x`] unfolding le_float_def real_of_float_0 . + using float_divr_nonpos_pos_upper_bound[OF `x \ 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 \ 0` by auto also have "\ = exp (real x / real ?num) ^ ?num" unfolding exp_real_of_nat_mult .. also have "\ \ 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 "\ \ 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 `\ 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def . qed moreover @@ -1566,32 +1566,32 @@ show ?thesis proof (cases "?horner \ 0") - case False hence "0 \ real ?horner" unfolding le_float_def by auto - - have div_less_zero: "real (float_divl prec x (- floor_fl x)) \ 0" - using `real (floor_fl x) < 0` `real x \ 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) \ + case False hence "0 \ real ?horner" unfolding le_float_def by auto + + have div_less_zero: "real (float_divl prec x (- floor_fl x)) \ 0" + using `real (floor_fl x) < 0` `real x \ 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) \ exp (real (float_divl prec x (- floor_fl x))) ^ ?num" unfolding float_power - using `0 \ 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 "\ \ 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 "\ = exp (real ?num * (real x / real ?num))" unfolding exp_real_of_nat_mult .. - also have "\ = exp (real x)" using `real ?num \ 0` by auto - finally show ?thesis - unfolding lb_exp.simps if_not_P[OF `\ 0 < x`] if_P[OF `x < - 1`] float.cases Float_floor Let_def if_not_P[OF False] by auto + using `0 \ 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 "\ \ 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 "\ = exp (real ?num * (real x / real ?num))" unfolding exp_real_of_nat_mult .. + also have "\ = exp (real x)" using `real ?num \ 0` by auto + finally show ?thesis + unfolding lb_exp.simps if_not_P[OF `\ 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) \ 0" and "real (floor_fl x) \ 0" using `real (floor_fl x) < 0` by auto - from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \ 0`, unfolded divide_self[OF `real (floor_fl x) \ 0`]] - have "- 1 \ 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) \ exp (real x / real (- floor_fl x))" unfolding Float_num . - hence "real (Float 1 -2) ^ ?num \ exp (real x / real (- floor_fl x)) ^ ?num" - by (auto intro!: power_mono simp add: Float_num) - also have "\ = exp (real x)" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \ 0` by auto - finally show ?thesis - unfolding lb_exp.simps if_not_P[OF `\ 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) \ 0" and "real (floor_fl x) \ 0" using `real (floor_fl x) < 0` by auto + from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \ 0`, unfolded divide_self[OF `real (floor_fl x) \ 0`]] + have "- 1 \ 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) \ exp (real x / real (- floor_fl x))" unfolding Float_num . + hence "real (Float 1 -2) ^ ?num \ exp (real x / real (- floor_fl x)) ^ ?num" + by (auto intro!: power_mono simp add: Float_num) + also have "\ = exp (real x)" unfolding num_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \ 0` by auto + finally show ?thesis + unfolding lb_exp.simps if_not_P[OF `\ 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))) \ 1 / real (ub_exp prec (-x))" using float_divl[where x=1] by auto also have "\ \ 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)) \ exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto have "exp (real x) \ real (1 :: float) / real (lb_exp prec (-x))" - using lb_exp[unfolded inverse_le_iff_le[OF exp_gt_zero lb_exp_pos[OF `\ 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 `\ 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 "\ \ 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 \ x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \ x`) have "x ^ Suc (Suc n) \ 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 \ x`) + by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \ x`) thus "x ^ Suc (Suc n) \ x ^ Suc n" by auto qed auto } from summable_Leibniz'(2,4)[OF `?a ----> 0` `\n. 0 \ ?a n`, OF `\n. ?a (Suc n) \ ?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) \ 1" - by (rule rapprox_rat_le1) simp_all + by (rule rapprox_rat_le1) simp_all have low: "2 / 3 \ 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) - \ ln (real (x * rapprox_rat prec 2 3 - 1) + 1)" + \ ln (real (x * rapprox_rat prec 2 3 - 1) + 1)" proof (rule ln_le_cancel_iff[symmetric, THEN iffD1]) - show "real x * 2 / 3 \ 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 \ 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 "\ \ 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 \ 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 \ real (x * rapprox_rat prec 2 3 - 1)" using pos by auto qed finally have "ln (real x) - \