# HG changeset patch # User hoelzl # Date 1334752161 -7200 # Node ID 400b158f1589886df6d68fd959f362b0c5721d31 # Parent d20bdee675dc201baa43502e30569de124c80a3a replace the float datatype by a type with unique representation diff -r d20bdee675dc -r 400b158f1589 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 18 14:29:20 2012 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 18 14:29:21 2012 +0200 @@ -54,23 +54,9 @@ case 0 thus ?case unfolding lb_0 ub_0 horner.simps by auto next case (Suc n) - have "?lb (Suc n) j' \ ?horner (Suc n) j'" unfolding lb_Suc ub_Suc horner.simps real_of_float_sub diff_minus - proof (rule add_mono) - show "(lapprox_rat prec 1 (f j')) \ 1 / (f j')" using lapprox_rat[of prec 1 "f j'"] by auto - from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct2] `0 \ real x` - show "- real (x * ub n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \ - - (x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)" - unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono) - qed - moreover have "?horner (Suc n) j' \ ?ub (Suc n) j'" unfolding ub_Suc horner.simps real_of_float_sub diff_minus - proof (rule add_mono) - show "1 / (f j') \ (rapprox_rat prec 1 (f j'))" using rapprox_rat[of 1 "f j'" prec] by auto - from Suc[where j'="Suc j'", unfolded funpow.simps comp_def f_Suc, THEN conjunct1] `0 \ real x` - show "- (x * horner F G n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x) \ - - real (x * lb n (F ((F ^^ j') s)) (G ((F ^^ j') s) (f j')) x)" - unfolding real_of_float_mult neg_le_iff_le by (rule mult_left_mono) - qed - ultimately show ?case by blast + thus ?case using lapprox_rat[of prec 1 "f j'"] using rapprox_rat[of 1 "f j'" prec] + Suc[where j'="Suc j'"] `0 \ real x` + by (auto intro!: add_mono mult_left_mono simp add: lb_Suc ub_Suc field_simps f_Suc) qed subsection "Theorems for floating point functions implementing the horner scheme" @@ -106,24 +92,10 @@ shows "(lb n ((F ^^ j') s) (f j') x) \ (\j=0..j=0.. (ub n ((F ^^ j') s) (f j') x)" (is "?ub") proof - - { fix x y z :: float have "x - y * z = x + - y * z" - by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def times_float.simps algebra_simps) - } note diff_mult_minus = this - - { fix x :: float have "- (- x) = x" by (cases x) auto } note minus_minus = this - - have move_minus: "(-x) = -1 * real x" by auto (* coercion "inside" is necessary *) - + { fix x y z :: float have "x - y * z = x + - y * z" by simp } note diff_mult_minus = this have sum_eq: "(\j=0..j = 0.. {0 ..< n}" - show "1 / (f (j' + j)) * real x ^ j = -1 ^ j * (1 / (f (j' + j))) * real (- x) ^ j" - unfolding move_minus power_mult_distrib mult_assoc[symmetric] - unfolding mult_commute unfolding mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric] - by auto - qed - + by (auto simp add: field_simps power_mult_distrib[symmetric]) have "0 \ real (-x)" using assms by auto from horner_bounds[where G=G and F=F and f=f and s=s and prec=prec and lb="\ n i k x. lb n i k (-x)" and ub="\ n i k x. ub n i k (-x)", unfolded lb_Suc ub_Suc diff_mult_minus, @@ -177,9 +149,11 @@ show ?thesis proof (cases "0 < l") case True hence "odd n \ 0 < l" and "0 \ real l" unfolding less_float_def by auto - have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \ 0 < l`] by auto - have "real l ^ n \ x ^ n" and "x ^ n \ real u ^ n " using `0 \ real l` and assms unfolding atLeastAtMost_iff using power_mono[of l x] power_mono[of x u] by auto - thus ?thesis using assms `0 < l` unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto + have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms + unfolding float_power_bnds_def if_P[OF `odd n \ 0 < l`] by auto + have "real l ^ n \ x ^ n" and "x ^ n \ real u ^ n " using `0 \ real l` assms + by (auto simp: power_mono) + thus ?thesis using assms `0 < l` unfolding l1 u1 by auto next case False hence P: "\ (odd n \ 0 < l)" using `even n` by auto show ?thesis @@ -188,25 +162,25 @@ 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 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 + ultimately show ?thesis 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 less_eq_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 less_eq_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 - show ?thesis unfolding atLeastAtMost_iff l1 u1 float_power using zero_le_even_power[OF `even n`] power_mono_even[OF `even n` x_abs] by auto + show ?thesis unfolding atLeastAtMost_iff l1 u1 using zero_le_even_power[OF `even n`] power_mono_even[OF `even n` x_abs] by auto qed qed next case False hence "odd n \ 0 < l" by auto have u1: "u1 = u ^ n" and l1: "l1 = l ^ n" using assms unfolding float_power_bnds_def if_P[OF `odd n \ 0 < l`] by auto have "real l ^ n \ x ^ n" and "x ^ n \ real u ^ n " using assms unfolding atLeastAtMost_iff using power_mono_odd[OF False] by auto - thus ?thesis unfolding atLeastAtMost_iff l1 u1 float_power less_float_def by auto + thus ?thesis unfolding atLeastAtMost_iff l1 u1 less_float_def by auto qed lemma bnds_power: "\ (x::real) l u. (l1, u1) = float_power_bnds n l u \ x \ {l .. u} \ l1 \ x ^ n \ x ^ n \ u1" @@ -222,10 +196,17 @@ *} fun sqrt_iteration :: "nat \ nat \ float \ float" where -"sqrt_iteration prec 0 (Float m e) = Float 1 ((e + bitlen m) div 2 + 1)" | +"sqrt_iteration prec 0 x = Float 1 ((bitlen \mantissa x\ + exponent x) div 2 + 1)" | "sqrt_iteration prec (Suc m) x = (let y = sqrt_iteration prec m x in Float 1 -1 * (y + float_divr prec x y))" +lemma compute_sqrt_iteration_base[code]: + shows "sqrt_iteration prec n (Float m e) = + (if n = 0 then Float 1 ((if m = 0 then 0 else bitlen \m\ + e) div 2 + 1) + else (let y = sqrt_iteration prec (n - 1) (Float m e) in + Float 1 -1 * (y + float_divr prec (Float m e) y)))" + using bitlen_Float by (cases n) simp_all + function ub_sqrt lb_sqrt :: "nat \ float \ float" where "ub_sqrt prec x = (if 0 < x then (sqrt_iteration prec prec x) else if x < 0 then - lb_sqrt prec (- x) @@ -259,23 +240,23 @@ show ?case proof (cases x) case (Float m e) - hence "0 < m" using float_pos_m_pos[unfolded less_float_def] assms by auto + hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps) hence "0 < sqrt m" by auto - have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_ge0 by auto - - have "x = (m / 2^nat (bitlen m)) * pow2 (e + (nat (bitlen m)))" - unfolding pow2_add pow2_int Float real_of_float_simp by auto - also have "\ < 1 * pow2 (e + nat (bitlen m))" + have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_nonneg by auto + + have "x = (m / 2^nat (bitlen m)) * 2 powr (e + (nat (bitlen m)))" + unfolding Float by (auto simp: powr_realpow[symmetric] field_simps powr_add) + also have "\ < 1 * 2 powr (e + 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 qed - finally have "sqrt x < sqrt (pow2 (e + bitlen m))" unfolding int_nat_bl by auto - also have "\ \ pow2 ((e + bitlen m) div 2 + 1)" + finally have "sqrt x < sqrt (2 powr (e + bitlen m))" unfolding int_nat_bl by auto + also have "\ \ 2 powr ((e + bitlen m) div 2 + 1)" proof - let ?E = "e + bitlen m" - have E_mod_pow: "pow2 (?E mod 2) < 4" + have E_mod_pow: "2 powr (?E mod 2) < 4" proof (cases "?E mod 2 = 1") case True thus ?thesis by auto next @@ -287,21 +268,23 @@ 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 .. - 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 - also have "\ < pow2 (?E div 2) * 2" + hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)" by auto + hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" unfolding real_sqrt_abs2 by auto + + have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)" by auto + have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))" + unfolding E_eq unfolding powr_add[symmetric] by (simp add: int_of_reals del: real_of_ints) + also have "\ = 2 powr (?E div 2) * sqrt (2 powr (?E mod 2))" + unfolding real_sqrt_mult[of _ "2 powr (?E mod 2)"] real_sqrt_abs2 by auto + also have "\ < 2 powr (?E div 2) * 2 powr 1" by (rule mult_strict_left_mono, auto intro: E_mod_pow) - also have "\ = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto + also have "\ = 2 powr (?E div 2 + 1)" unfolding add_commute[of _ 1] powr_add[symmetric] + by simp finally show ?thesis by auto qed - finally show ?thesis - unfolding Float sqrt_iteration.simps real_of_float_simp by auto + finally show ?thesis using `0 < m` + unfolding Float + by (subst compute_sqrt_iteration_base) (simp add: ac_simps real_Float del: Float_def) qed next case (Suc n) @@ -310,8 +293,8 @@ also have "\ < real ?b" using Suc . finally have "sqrt x < (?b + x / ?b)/2" using sqrt_ub_pos_pos_1[OF Suc _ `0 < real x`] by auto also have "\ \ (?b + (float_divr prec x ?b))/2" by (rule divide_right_mono, auto simp add: float_divr) - also have "\ = (Float 1 -1) * (?b + (float_divr prec x ?b))" by auto - finally show ?case unfolding sqrt_iteration.simps Let_def real_of_float_mult real_of_float_add right_distrib . + also have "\ = (Float 1 -1) * (?b + (float_divr prec x ?b))" by simp + finally show ?case unfolding sqrt_iteration.simps Let_def right_distrib . qed lemma sqrt_iteration_lower_bound: assumes "0 < real x" @@ -325,9 +308,9 @@ lemma lb_sqrt_lower_bound: assumes "0 \ real x" shows "0 \ real (lb_sqrt prec x)" proof (cases "0 < x") - case True hence "0 < real x" and "0 \ x" using `0 \ real x` unfolding less_float_def le_float_def by auto + case True hence "0 < real x" and "0 \ x" using `0 \ real x` unfolding less_float_def less_eq_float_def by auto hence "0 < sqrt_iteration prec prec x" unfolding less_float_def using sqrt_iteration_lower_bound by auto - hence "0 \ real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \ x`] unfolding le_float_def by auto + hence "0 \ real (float_divl prec x (sqrt_iteration prec prec x))" using float_divl_lower_bound[OF `0 \ x`] unfolding less_eq_float_def by auto thus ?thesis unfolding lb_sqrt.simps using True by auto next case False with `0 \ real x` have "real x = 0" unfolding less_float_def by auto @@ -446,7 +429,7 @@ { have "(x * lb_arctan_horner prec n 1 (x*x)) \ ?S n" using bounds(1) `0 \ real x` - unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric] + unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric] unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"] by (auto intro!: mult_left_mono) also have "\ \ arctan x" using arctan_bounds .. @@ -455,7 +438,7 @@ { have "arctan x \ ?S (Suc n)" using arctan_bounds .. also have "\ \ (x * ub_arctan_horner prec (Suc n) 1 (x*x))" using bounds(2)[of "Suc n"] `0 \ real x` - unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric] + unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric] unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"] by (auto intro!: mult_left_mono) finally have "arctan x \ (x * ub_arctan_horner prec (Suc n) 1 (x*x))" . } @@ -512,8 +495,8 @@ have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto have "0 \ real ?k" by (rule order_trans[OF _ rapprox_rat], auto simp add: `0 \ k`) - have "real ?k \ 1" unfolding rapprox_rat.simps(2)[OF zero_le_one `0 < k`] - by (rule rapprox_posrat_le1, auto simp add: `0 < k` `1 \ k`) + have "real ?k \ 1" + by (rule rapprox_rat_le1, auto simp add: `0 < k` `1 \ k`) have "1 / k \ ?k" using rapprox_rat[where x=1 and y=k] by auto hence "arctan (1 / k) \ arctan ?k" by (rule arctan_monotone') @@ -526,8 +509,7 @@ let ?k = "lapprox_rat prec 1 k" have "1 div k = 0" using div_pos_pos_trivial[OF _ `1 < k`] by auto have "1 / k \ 1" using `1 < k` by auto - - have "\n. 0 \ real ?k" using lapprox_rat_bottom[where x=1 and y=k, OF zero_le_one `0 < k`] by (auto simp add: `1 div k = 0`) + have "\n. 0 \ real ?k" using lapprox_rat_nonneg[where x=1 and y=k, OF zero_le_one `0 < k`] by (auto simp add: `1 div k = 0`) have "\n. real ?k \ 1" using lapprox_rat by (rule order_trans, auto simp add: `1 / k \ 1`) have "?k \ 1 / k" using lapprox_rat[where x=1 and y=k] by auto @@ -539,14 +521,14 @@ } note lb_arctan = this have "pi \ ub_pi n" - unfolding ub_pi_def machin_pi Let_def real_of_float_mult real_of_float_sub unfolding Float_num - using lb_arctan[of 239] ub_arctan[of 5] - by (auto intro!: mult_left_mono add_mono simp add: diff_minus simp del: lapprox_rat.simps rapprox_rat.simps) + unfolding ub_pi_def machin_pi Let_def unfolding Float_num + using lb_arctan[of 239] ub_arctan[of 5] powr_realpow[of 2 2] + by (auto intro!: mult_left_mono add_mono simp add: diff_minus) moreover have "lb_pi n \ pi" - unfolding lb_pi_def machin_pi Let_def real_of_float_mult real_of_float_sub Float_num - using lb_arctan[of 5] ub_arctan[of 239] - by (auto intro!: mult_left_mono add_mono simp add: diff_minus simp del: lapprox_rat.simps rapprox_rat.simps) + unfolding lb_pi_def machin_pi Let_def Float_num + using lb_arctan[of 5] ub_arctan[of 239] powr_realpow[of 2 2] + by (auto intro!: mult_left_mono add_mono simp add: diff_minus) ultimately show ?thesis by auto qed @@ -579,17 +561,17 @@ lemma lb_arctan_bound': assumes "0 \ real x" shows "lb_arctan prec x \ arctan x" proof - - have "\ x < 0" and "0 \ x" unfolding less_float_def le_float_def using `0 \ real x` by auto + have "\ x < 0" and "0 \ x" unfolding less_float_def less_eq_float_def using `0 \ real x` by auto let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)" and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)" show ?thesis proof (cases "x \ Float 1 -1") - case True hence "real x \ 1" unfolding le_float_def Float_num by auto + case True hence "real x \ 1" unfolding less_eq_float_def Float_num by auto show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_P[OF True] using arctan_0_1_bounds[OF `0 \ real x` `real x \ 1`] by auto next - case False hence "0 < real x" unfolding le_float_def Float_num by auto + case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto let ?R = "1 + sqrt (1 + real x * real x)" let ?fR = "1 + ub_sqrt prec (1 + x * x)" let ?DIV = "float_divl prec x ?fR" @@ -621,9 +603,9 @@ moreover have "?DIV \ real x / ?fR" by (rule float_divl) ultimately have "real ?DIV \ 1" unfolding divide_le_eq_1_pos[OF `0 < real ?fR`, symmetric] by auto - have "0 \ real ?DIV" using float_divl_lower_bound[OF `0 \ x` `0 < ?fR`] unfolding le_float_def by auto - - have "(Float 1 1 * ?lb_horner ?DIV) \ 2 * arctan (float_divl prec x ?fR)" unfolding real_of_float_mult[of "Float 1 1"] Float_num + have "0 \ real ?DIV" using float_divl_lower_bound[OF `0 \ x` `0 < ?fR`] unfolding less_eq_float_def by auto + + have "(Float 1 1 * ?lb_horner ?DIV) \ 2 * arctan (float_divl prec x ?fR)" using arctan_0_1_bounds[OF `0 \ real ?DIV` `real ?DIV \ 1`] by auto also have "\ \ 2 * arctan (x / ?R)" using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono) @@ -631,7 +613,7 @@ 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 case False - hence "2 < real x" unfolding le_float_def Float_num by auto + hence "2 < real x" unfolding less_eq_float_def Float_num by auto hence "1 \ real x" by auto let "?invx" = "float_divr prec 1 x" @@ -649,13 +631,14 @@ have "1 / x \ 0" and "0 < 1 / x" using `0 < real x` by auto - have "arctan (1 / x) \ arctan ?invx" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divr) + have "arctan (1 / x) \ arctan ?invx" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divr) also have "\ \ (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \ real ?invx` `real ?invx \ 1`] by auto finally have "pi / 2 - (?ub_horner ?invx) \ arctan x" using `0 \ arctan x` arctan_inverse[OF `1 / x \ 0`] unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto moreover - have "lb_pi prec * Float 1 -1 \ pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto + have "lb_pi prec * Float 1 -1 \ pi / 2" + unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp 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 @@ -667,18 +650,18 @@ lemma ub_arctan_bound': assumes "0 \ real x" shows "arctan x \ ub_arctan prec x" proof - - have "\ x < 0" and "0 \ x" unfolding less_float_def le_float_def using `0 \ real x` by auto + have "\ x < 0" and "0 \ x" unfolding less_float_def less_eq_float_def using `0 \ real x` by auto let "?ub_horner x" = "x * ub_arctan_horner prec (get_odd (prec div 4 + 1)) 1 (x * x)" and "?lb_horner x" = "x * lb_arctan_horner prec (get_even (prec div 4 + 1)) 1 (x * x)" show ?thesis proof (cases "x \ Float 1 -1") - case True hence "real x \ 1" unfolding le_float_def Float_num by auto + case True hence "real x \ 1" unfolding less_eq_float_def Float_num by auto show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\ x < 0`] if_P[OF True] using arctan_0_1_bounds[OF `0 \ real x` `real x \ 1`] by auto next - case False hence "0 < real x" unfolding le_float_def Float_num by auto + case False hence "0 < real x" unfolding less_eq_float_def Float_num by auto let ?R = "1 + sqrt (1 + real x * real x)" let ?fR = "1 + lb_sqrt prec (1 + x * x)" let ?DIV = "float_divr prec x ?fR" @@ -691,7 +674,7 @@ have "lb_sqrt prec (1 + x * x) \ sqrt (1 + x * x)" using bnds_sqrt'[of "1 + x * x"] by auto hence "?fR \ ?R" by auto - have "0 < real ?fR" unfolding real_of_float_add real_of_float_1 by (rule order_less_le_trans[OF zero_less_one], auto simp add: lb_sqrt_lower_bound[OF `0 \ real (1 + x*x)`]) + have "0 < real ?fR" by (rule order_less_le_trans[OF zero_less_one], auto simp add: lb_sqrt_lower_bound[OF `0 \ real (1 + x*x)`]) have monotone: "x / ?R \ (float_divr prec x ?fR)" proof - @@ -707,7 +690,7 @@ show ?thesis proof (cases "?DIV > 1") case True - have "pi / 2 \ ub_pi prec * Float 1 -1" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto + have "pi / 2 \ ub_pi prec * Float 1 -1" unfolding Float_num times_divide_eq_right mult_1_left 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 @@ -720,13 +703,13 @@ have "arctan x = 2 * arctan (x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left . also have "\ \ 2 * arctan (?DIV)" using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono) - also have "\ \ (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num + also have "\ \ (Float 1 1 * ?ub_horner ?DIV)" unfolding 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 - hence "2 < real x" unfolding le_float_def Float_num by auto + hence "2 < real x" unfolding less_eq_float_def Float_num by auto hence "1 \ real x" by auto hence "0 < real x" by auto hence "0 < x" unfolding less_float_def by auto @@ -735,17 +718,17 @@ have "0 \ arctan x" using arctan_monotone'[OF `0 \ real x`] using arctan_tan[of 0, unfolded tan_zero] by auto have "real ?invx \ 1" unfolding less_float_def by (rule order_trans[OF float_divl], auto simp add: `1 \ real x` divide_le_eq_1_pos[OF `0 < real x`]) - have "0 \ real ?invx" unfolding real_of_float_0[symmetric] by (rule float_divl_lower_bound[unfolded le_float_def], auto simp add: `0 < x`) + have "0 \ real ?invx" by (rule float_divl_lower_bound[unfolded less_eq_float_def], auto simp add: `0 < x`) have "1 / x \ 0" and "0 < 1 / x" using `0 < real x` by auto have "(?lb_horner ?invx) \ arctan (?invx)" using arctan_0_1_bounds[OF `0 \ real ?invx` `real ?invx \ 1`] by auto - also have "\ \ arctan (1 / x)" unfolding real_of_float_1[symmetric] by (rule arctan_monotone', rule float_divl) + also have "\ \ arctan (1 / x)" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divl) finally have "arctan x \ pi / 2 - (?lb_horner ?invx)" using `0 \ arctan x` arctan_inverse[OF `1 / x \ 0`] unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto moreover - have "pi / 2 \ 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 + have "pi / 2 \ ub_pi prec * Float 1 -1" unfolding 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 False] by auto @@ -756,15 +739,16 @@ lemma arctan_boundaries: "arctan x \ {(lb_arctan prec x) .. (ub_arctan prec x)}" proof (cases "0 \ x") - case True hence "0 \ real x" unfolding le_float_def by auto + case True hence "0 \ real x" unfolding less_eq_float_def by auto show ?thesis using ub_arctan_bound'[OF `0 \ real x`] lb_arctan_bound'[OF `0 \ real x`] unfolding atLeastAtMost_iff by auto next let ?mx = "-x" - case False hence "x < 0" and "0 \ real ?mx" unfolding le_float_def less_float_def by auto + case False hence "x < 0" and "0 \ real ?mx" unfolding less_eq_float_def less_float_def by auto hence bounds: "lb_arctan prec ?mx \ arctan ?mx \ arctan ?mx \ ub_arctan prec ?mx" using ub_arctan_bound'[OF `0 \ real ?mx`] lb_arctan_bound'[OF `0 \ real ?mx`] by auto show ?thesis unfolding real_of_float_minus arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`] - unfolding atLeastAtMost_iff using bounds[unfolded real_of_float_minus arctan_minus] by auto + unfolding atLeastAtMost_iff using bounds[unfolded real_of_float_minus arctan_minus] + by (simp add: arctan_minus) qed lemma bnds_arctan: "\ (x::real) lx ux. (l, u) = (lb_arctan prec lx, ub_arctan prec ux) \ x \ {lx .. ux} \ l \ arctan x \ arctan x \ u" @@ -800,7 +784,7 @@ shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \ (\ i=0.. i=0.. (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub") proof - - have "0 \ real (x * x)" unfolding real_of_float_mult by auto + have "0 \ real (x * x)" by auto let "?f n" = "fact (2 * n)" { fix n @@ -818,7 +802,7 @@ proof (cases "real x = 0") case False hence "real x \ 0" by auto hence "0 < x" and "0 < real x" using `0 \ real x` unfolding less_float_def by auto - have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_mult real_of_float_0 + have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero using mult_pos_pos[where a="real x" and b="real x"] by auto { fix x n have "(\ i=0.. x" by (rule order_trans[OF _ `0 < real x`[THEN less_imp_le]], auto) with `x \ pi / 2` - show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps real_of_float_minus real_of_float_0 using cos_ge_zero by auto + show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps real_of_float_minus real_of_float_zero using cos_ge_zero by auto qed ultimately show ?thesis by auto next @@ -901,7 +885,9 @@ show ?thesis proof (cases "n = 0") case True - thus ?thesis unfolding `n = 0` get_even_def get_odd_def using `real x = 0` lapprox_rat[where x="-1" and y=1] by auto + thus ?thesis unfolding `n = 0` get_even_def get_odd_def + using `real x = 0` lapprox_rat[where x="-1" and y=1] + by (auto simp: compute_lapprox_rat compute_rapprox_rat) next case False with not0_implies_Suc obtain m where "n = Suc m" by blast thus ?thesis unfolding `n = Suc m` get_even_def get_odd_def using `real x = 0` rapprox_rat[where x=1 and y=1] lapprox_rat[where x=1 and y=1] by (cases "even (Suc m)", auto) @@ -912,7 +898,7 @@ shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \ (\ i=0.. i=0.. (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub") proof - - have "0 \ real (x * x)" unfolding real_of_float_mult by auto + have "0 \ real (x * x)" by auto let "?f n" = "fact (2 * n + 1)" { fix n @@ -922,7 +908,7 @@ from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0, OF `0 \ real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps] - show "?lb" and "?ub" using `0 \ real x` unfolding real_of_float_mult + show "?lb" and "?ub" using `0 \ real x` unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric] unfolding mult_commute[where 'a=real] by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"]) @@ -933,7 +919,7 @@ proof (cases "real x = 0") case False hence "real x \ 0" by auto hence "0 < x" and "0 < real x" using `0 \ real x` unfolding less_float_def by auto - have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_mult real_of_float_0 + have "0 < x * x" using `0 < x` unfolding less_float_def real_of_float_zero using mult_pos_pos[where a="real x" and b="real x"] by auto { fix x n have "(\ j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1)) @@ -1006,7 +992,7 @@ case False hence "get_even n = 0" by auto with `x \ pi / 2` `0 \ real x` - show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps real_of_float_minus real_of_float_0 using sin_ge_zero by auto + show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps real_of_float_minus using sin_ge_zero by auto qed ultimately show ?thesis by auto next @@ -1065,7 +1051,7 @@ case False { fix y x :: float let ?x2 = "(x * Float 1 -1)" assume "y \ cos ?x2" and "-pi \ x" and "x \ pi" - hence "- (pi / 2) \ ?x2" and "?x2 \ pi / 2" using pi_ge_two unfolding real_of_float_mult Float_num by auto + hence "- (pi / 2) \ ?x2" and "?x2 \ pi / 2" using pi_ge_two unfolding Float_num by auto hence "0 \ cos ?x2" by (rule cos_ge_zero) have "(?lb_half y) \ cos x" @@ -1077,14 +1063,14 @@ from mult_mono[OF `y \ cos ?x2` `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 (x / 2) * cos (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 + hence "2 * real y * real y - 1 \ 2 * cos (x / 2) * cos (x / 2) - 1" unfolding Float_num by auto + thus ?thesis unfolding if_not_P[OF False] x_half Float_num by auto qed } note lb_half = this { fix y x :: float let ?x2 = "(x * Float 1 -1)" assume ub: "cos ?x2 \ y" and "- pi \ x" and "x \ pi" - hence "- (pi / 2) \ ?x2" and "?x2 \ pi / 2" using pi_ge_two unfolding real_of_float_mult Float_num by auto + hence "- (pi / 2) \ ?x2" and "?x2 \ pi / 2" using pi_ge_two unfolding Float_num by auto hence "0 \ cos ?x2" by (rule cos_ge_zero) have "cos x \ (?ub_half y)" @@ -1093,8 +1079,8 @@ 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 (x / 2) * cos (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 + hence "2 * cos (x / 2) * cos (x / 2) - 1 \ 2 * real y * real y - 1" unfolding Float_num by auto + thus ?thesis unfolding x_half Float_num by auto qed } note ub_half = this @@ -1106,7 +1092,7 @@ show ?thesis proof (cases "x < 1") case True hence "real x \ 1" unfolding less_float_def by auto - have "0 \ real ?x2" and "?x2 \ pi / 2" using pi_ge_two `0 \ real x` unfolding real_of_float_mult Float_num using assms by auto + have "0 \ real ?x2" and "?x2 \ pi / 2" using pi_ge_two `0 \ real x` using assms by auto from cos_boundaries[OF this] have lb: "(?lb_horner ?x2) \ ?cos ?x2" and ub: "?cos ?x2 \ (?ub_horner ?x2)" by auto @@ -1123,21 +1109,21 @@ ultimately show ?thesis by auto next case False - have "0 \ real ?x4" and "?x4 \ pi / 2" using pi_ge_two `0 \ real x` `x \ pi` unfolding real_of_float_mult Float_num by auto + have "0 \ real ?x4" and "?x4 \ pi / 2" using pi_ge_two `0 \ real x` `x \ pi` unfolding Float_num by auto from cos_boundaries[OF this] have lb: "(?lb_horner ?x4) \ ?cos ?x4" and ub: "?cos ?x4 \ (?ub_horner ?x4)" by auto - have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by (cases x, auto simp add: times_float.simps) + have eq_4: "?x2 * Float 1 -1 = x * Float 1 -2" by simp have "(?lb x) \ ?cos x" proof - - have "-pi \ ?x2" and "?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` `x \ pi` by auto + have "-pi \ ?x2" and "?x2 \ pi" using pi_ge_two `0 \ real x` `x \ pi` by auto from lb_half[OF lb_half[OF lb this] `-pi \ x` `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 \ (?ub x)" proof - - have "-pi \ ?x2" and "?x2 \ pi" unfolding real_of_float_mult Float_num using pi_ge_two `0 \ real x` ` x \ pi` by auto + have "-pi \ ?x2" and "?x2 \ pi" using pi_ge_two `0 \ real x` ` x \ pi` by auto from ub_half[OF ub_half[OF ub this] `-pi \ x` `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 @@ -1155,8 +1141,8 @@ definition bnds_cos :: "nat \ float \ float \ float * float" where "bnds_cos prec lx ux = (let - lpi = round_down prec (lb_pi prec) ; - upi = round_up prec (ub_pi prec) ; + lpi = float_round_down prec (lb_pi prec) ; + upi = float_round_up prec (ub_pi prec) ; k = floor_fl (float_divr prec (lx + lpi) (2 * lpi)) ; lx = lx - k * 2 * (if k < 0 then lpi else upi) ; ux = ux - k * 2 * (if k < 0 then upi else lpi) @@ -1169,14 +1155,7 @@ lemma floor_int: obtains k :: int where "real k = (floor_fl f)" -proof - - assume *: "\ k :: int. real k = (floor_fl f) \ thesis" - obtain m e where fl: "Float m e = floor_fl f" by (cases "floor_fl f", auto) - from floor_pos_exp[OF this] - have "real (m* 2^(nat e)) = (floor_fl f)" - by (auto simp add: fl[symmetric] real_of_float_def pow2_def) - from *[OF this] show thesis by blast -qed + by (simp add: floor_fl_def) lemma cos_periodic_nat[simp]: fixes n :: nat shows "cos (x + n * (2 * pi)) = cos x" proof (induct n arbitrary: x) @@ -1203,8 +1182,8 @@ fix x :: real fix lx ux assume bnds: "(l, u) = bnds_cos prec lx ux" and x: "x \ {lx .. ux}" - let ?lpi = "round_down prec (lb_pi prec)" - let ?upi = "round_up prec (ub_pi prec)" + let ?lpi = "float_round_down prec (lb_pi prec)" + let ?upi = "float_round_up prec (ub_pi prec)" let ?k = "floor_fl (float_divr prec (lx + ?lpi) (2 * ?lpi))" let ?lx = "lx - ?k * 2 * (if ?k < 0 then ?lpi else ?upi)" let ?ux = "ux - ?k * 2 * (if ?k < 0 then ?upi else ?lpi)" @@ -1212,24 +1191,27 @@ obtain k :: int where k: "k = real ?k" using floor_int . have upi: "pi \ ?upi" and lpi: "?lpi \ pi" - using round_up[of "ub_pi prec" prec] pi_boundaries[of prec] - round_down[of prec "lb_pi prec"] by auto + using float_round_up[of "ub_pi prec" prec] pi_boundaries[of prec] + float_round_down[of prec "lb_pi prec"] by auto hence "?lx \ x - k * (2 * pi) \ x - k * (2 * pi) \ ?ux" - using x by (cases "k = 0") (auto intro!: add_mono - simp add: diff_minus k[symmetric] less_float_def) + using x unfolding k[symmetric] + by (cases "k = 0") + (auto intro!: add_mono + simp add: diff_minus k[symmetric] less_float_def + simp del: float_of_numeral) note lx = this[THEN conjunct1] and ux = this[THEN conjunct2] hence lx_less_ux: "?lx \ real ?ux" by (rule order_trans) { assume "- ?lpi \ ?lx" and x_le_0: "x - k * (2 * pi) \ 0" with lpi[THEN le_imp_neg_le] lx have pi_lx: "- pi \ ?lx" and lx_0: "real ?lx \ 0" - by (simp_all add: le_float_def) + by (simp_all add: less_eq_float_def) have "(lb_cos prec (- ?lx)) \ cos (real (- ?lx))" using lb_cos_minus[OF pi_lx lx_0] by simp also have "\ \ cos (x + (-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 + by (simp only: real_of_float_uminus real_of_int_minus cos_minus diff_minus mult_minus_left) finally have "(lb_cos prec (- ?lx)) \ cos x" unfolding cos_periodic_int . } @@ -1238,11 +1220,11 @@ { assume "0 \ ?lx" and pi_x: "x - k * (2 * pi) \ pi" with lx have pi_lx: "?lx \ pi" and lx_0: "0 \ real ?lx" - by (auto simp add: le_float_def) + by (auto simp add: less_eq_float_def) have "cos (x + (-k) * (2 * pi)) \ cos ?lx" using cos_monotone_0_pi'[OF lx_0 lx pi_x] - by (simp only: real_of_float_minus real_of_int_minus + by (simp only: real_of_int_minus cos_minus diff_minus mult_minus_left) also have "\ \ (ub_cos prec ?lx)" using lb_cos[OF lx_0 pi_lx] by simp @@ -1253,11 +1235,11 @@ { assume pi_x: "- pi \ x - k * (2 * pi)" and "?ux \ 0" with ux have pi_ux: "- pi \ ?ux" and ux_0: "real ?ux \ 0" - by (simp_all add: le_float_def) + by (simp_all add: less_eq_float_def) have "cos (x + (-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 + by (simp only: real_of_float_uminus real_of_int_minus cos_minus diff_minus mult_minus_left) also have "\ \ (ub_cos prec (- ?ux))" using lb_cos_minus[OF pi_ux ux_0, of prec] by simp @@ -1268,13 +1250,13 @@ { assume "?ux \ ?lpi" and x_ge_0: "0 \ x - k * (2 * pi)" with lpi ux have pi_ux: "?ux \ pi" and ux_0: "0 \ real ?ux" - by (simp_all add: le_float_def) + by (simp_all add: less_eq_float_def) have "(lb_cos prec ?ux) \ cos ?ux" using lb_cos[OF ux_0 pi_ux] by simp also have "\ \ cos (x + (-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 + by (simp only: real_of_int_minus cos_minus diff_minus mult_minus_left) finally have "(lb_cos prec ?ux) \ cos x" unfolding cos_periodic_int . } @@ -1290,7 +1272,7 @@ from True lpi[THEN le_imp_neg_le] lx ux have "- pi \ x - k * (2 * pi)" and "x - k * (2 * pi) \ 0" - by (auto simp add: le_float_def) + by (auto simp add: less_eq_float_def) with True negative_ux negative_lx show ?thesis unfolding l u by simp next case False note 1 = this show ?thesis @@ -1303,7 +1285,7 @@ from True lpi lx ux have "0 \ x - k * (2 * pi)" and "x - k * (2 * pi) \ pi" - by (auto simp add: le_float_def) + by (auto simp add: less_eq_float_def) with True positive_ux positive_lx show ?thesis unfolding l u by simp next case False note 2 = this show ?thesis @@ -1314,7 +1296,8 @@ by (auto simp add: bnds_cos_def Let_def) show ?thesis unfolding u l using negative_lx positive_ux Cond - by (cases "x - k * (2 * pi) < 0", simp_all add: real_of_float_min) + by (cases "x - k * (2 * pi) < 0") (auto simp add: real_of_float_min) + next case False note 3 = this show ?thesis proof (cases "0 \ ?lx \ ?ux \ 2 * ?lpi") case True note Cond = this with bnds 1 2 3 @@ -1331,28 +1314,27 @@ case False hence "pi \ x - k * (2 * pi)" by simp hence pi_x: "- pi \ x - k * (2 * pi) - 2 * pi" by simp - have "?ux \ 2 * pi" using Cond lpi by (auto simp add: le_float_def) + have "?ux \