: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))" + using \even p\ by (auto simp add: dvd_def power_eq_if) from \n \ p\ np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \ p" by arith+ have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0" by simp - with \n \ p\ np * show ?thesis - apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add) - apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus - mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc) - done + with \n \ p\ np \

* show ?thesis + by (simp add: flip: div_add power_add) qed then show ?thesis using \n\p\ by (auto simp: algebra_simps sin_coeff_def binomial_fact) @@ -3884,22 +3869,31 @@ lemma sin_two_pi [simp]: "sin (2 * pi) = 0" by (simp add: sin_double) +context + fixes w :: "'a::{real_normed_field,banach}" + +begin + lemma sin_times_sin: "sin w * sin z = (cos (w - z) - cos (w + z)) / 2" - for w :: "'a::{real_normed_field,banach}" by (simp add: cos_diff cos_add) lemma sin_times_cos: "sin w * cos z = (sin (w + z) + sin (w - z)) / 2" - for w :: "'a::{real_normed_field,banach}" by (simp add: sin_diff sin_add) lemma cos_times_sin: "cos w * sin z = (sin (w + z) - sin (w - z)) / 2" - for w :: "'a::{real_normed_field,banach}" by (simp add: sin_diff sin_add) lemma cos_times_cos: "cos w * cos z = (cos (w - z) + cos (w + z)) / 2" - for w :: "'a::{real_normed_field,banach}" by (simp add: cos_diff cos_add) +lemma cos_double_cos: "cos (2 * w) = 2 * cos w ^ 2 - 1" + by (simp add: cos_double sin_squared_eq) + +lemma cos_double_sin: "cos (2 * w) = 1 - 2 * sin w ^ 2" + by (simp add: cos_double sin_squared_eq) + +end + lemma sin_plus_sin: "sin w + sin z = 2 * sin ((w + z) / 2) * cos ((w - z) / 2)" for w :: "'a::{real_normed_field,banach}" apply (simp add: mult.assoc sin_times_cos) @@ -3924,14 +3918,6 @@ apply (simp add: field_simps) done -lemma cos_double_cos: "cos (2 * z) = 2 * cos z ^ 2 - 1" - for z :: "'a::{real_normed_field,banach}" - by (simp add: cos_double sin_squared_eq) - -lemma cos_double_sin: "cos (2 * z) = 1 - 2 * sin z ^ 2" - for z :: "'a::{real_normed_field,banach}" - by (simp add: cos_double sin_squared_eq) - lemma sin_pi_minus [simp]: "sin (pi - x) = sin x" by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff) @@ -4074,7 +4060,7 @@ lemma cos_zero_lemma: assumes "0 \ x" "cos x = 0" - shows "\n. odd n \ x = of_nat n * (pi/2) \ n > 0" + shows "\n. odd n \ x = of_nat n * (pi/2)" proof - have xle: "x < (1 + real_of_int \x/pi\) * pi" using floor_correct [of "x/pi"] @@ -4101,12 +4087,17 @@ by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps) qed -lemma sin_zero_lemma: "0 \ x \ sin x = 0 \ \n::nat. even n \ x = real n * (pi/2)" - using cos_zero_lemma [of "x + pi/2"] - apply (clarsimp simp add: cos_add) - apply (rule_tac x = "n - 1" in exI) - apply (simp add: algebra_simps of_nat_diff) - done +lemma sin_zero_lemma: + assumes "0 \ x" "sin x = 0" + shows "\n::nat. even n \ x = real n * (pi/2)" +proof - + obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0" + using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add) + then have "x = real (n - 1) * (pi / 2)" + by (simp add: algebra_simps of_nat_diff) + then show ?thesis + by (simp add: \odd n\) +qed lemma cos_zero_iff: "cos x = 0 \ ((\n. odd n \ x = real n * (pi/2)) \ (\n. odd n \ x = - (real n * (pi/2))))" @@ -4146,7 +4137,7 @@ using that assms by (auto simp: sin_zero_iff) qed auto -lemma cos_zero_iff_int: "cos x = 0 \ (\n. odd n \ x = of_int n * (pi/2))" +lemma cos_zero_iff_int: "cos x = 0 \ (\i. odd i \ x = of_int i * (pi/2))" proof - have 1: "\n. odd n \ \i. odd i \ real n = real_of_int i" by (metis even_of_nat of_int_of_nat_eq) @@ -4159,15 +4150,21 @@ by (force simp: cos_zero_iff intro!: 1 2 3) qed -lemma sin_zero_iff_int: "sin x = 0 \ (\n. even n \ x = of_int n * (pi/2))" +lemma sin_zero_iff_int: "sin x = 0 \ (\i. even i \ x = of_int i * (pi/2))" (is "?lhs = ?rhs") proof safe - assume "sin x = 0" + assume ?lhs + then consider (plus) n where "even n" "x = real n * (pi/2)" | (minus) n where "even n" "x = - (real n * (pi/2))" + using sin_zero_iff by auto then show "\n. even n \ x = of_int n * (pi/2)" - apply (simp add: sin_zero_iff, safe) - apply (metis even_of_nat of_int_of_nat_eq) - apply (rule_tac x="- (int n)" in exI) - apply simp - done + proof cases + case plus + then show ?rhs + by (metis even_of_nat of_int_of_nat_eq) + next + case minus + then show ?thesis + by (rule_tac x="- (int n)" in exI) simp + qed next fix i :: int assume "even i" @@ -4175,12 +4172,16 @@ by (cases i rule: int_cases2, simp_all add: sin_zero_iff) qed -lemma sin_zero_iff_int2: "sin x = 0 \ (\n::int. x = of_int n * pi)" - apply (simp only: sin_zero_iff_int) - apply (safe elim!: evenE) - apply (simp_all add: field_simps) - using dvd_triv_left apply fastforce - done +lemma sin_zero_iff_int2: "sin x = 0 \ (\i::int. x = of_int i * pi)" +proof - + have "sin x = 0 \ (\i. even i \ x = real_of_int i * (pi / 2))" + by (auto simp: sin_zero_iff_int) + also have "... = (\j. x = real_of_int (2*j) * (pi / 2))" + using dvd_triv_left by blast + also have "... = (\i::int. x = of_int i * pi)" + by auto + finally show ?thesis . +qed lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0" by (simp add: sin_zero_iff_int2) @@ -4252,15 +4253,14 @@ lemma sin_x_le_x: fixes x :: real - assumes x: "x \ 0" + assumes "x \ 0" shows "sin x \ x" proof - let ?f = "\x. x - sin x" - from x have "?f x \ ?f 0" - apply (rule DERIV_nonneg_imp_nondecreasing) - apply (intro allI impI exI[of _ "1 - cos x" for x]) - apply (auto intro!: derivative_eq_intros simp: field_simps) - done + have "\u. \0 \ u; u \ x\ \ \y. (?f has_real_derivative 1 - cos u) (at u)" + by (auto intro!: derivative_eq_intros simp: field_simps) + then have "?f x \ ?f 0" + by (metis cos_le_one diff_ge_0_iff_ge DERIV_nonneg_imp_nondecreasing [OF assms]) then show "sin x \ x" by simp qed @@ -4270,11 +4270,10 @@ shows "sin x \ - x" proof - let ?f = "\x. x + sin x" - from x have "?f x \ ?f 0" - apply (rule DERIV_nonneg_imp_nondecreasing) - apply (intro allI impI exI[of _ "1 + cos x" for x]) - apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff) - done + have \

: "\u. \0 \ u; u \ x\ \ \y. (?f has_real_derivative 1 + cos u) (at u)" + by (auto intro!: derivative_eq_intros simp: field_simps) + have "?f x \ ?f 0" + by (rule DERIV_nonneg_imp_nondecreasing [OF assms]) (use \

real_0_le_add_iff in force) then show "sin x \ -x" by simp qed @@ -4409,9 +4408,8 @@ have "cos(3 * x) = cos(2*x + x)" by simp also have "\ = 4 * cos x ^ 3 - 3 * cos x" - apply (simp only: cos_add cos_double sin_double) - apply (simp add: * field_simps power2_eq_square power3_eq_cube) - done + unfolding cos_add cos_double sin_double + by (simp add: * field_simps power2_eq_square power3_eq_cube) finally show ?thesis . qed @@ -4482,12 +4480,18 @@ by (metis Ints_of_int sin_integer_2pi) lemma sincos_principal_value: "\y. (- pi < y \ y \ pi) \ (sin y = sin x \ cos y = cos x)" - apply (rule exI [where x="pi - (2 * pi) * frac ((pi - x) / (2 * pi))"]) - apply (auto simp: field_simps frac_lt_1) - apply (simp_all add: frac_def field_simps) - apply (simp_all add: add_divide_distrib diff_divide_distrib) - apply (simp_all add: sin_add cos_add mult.assoc [symmetric]) - done +proof - + define y where "y \ pi - (2 * pi) * frac ((pi - x) / (2 * pi))" + have "-pi < y"" y \ pi" + by (auto simp: field_simps frac_lt_1 y_def) + moreover + have "sin y = sin x" "cos y = cos x" + unfolding y_def + apply (simp_all add: frac_def divide_simps sin_add cos_add) + by (metis sin_int_2pin cos_int_2pin diff_zero add.right_neutral mult.commute mult.left_neutral mult_zero_left)+ + ultimately + show ?thesis by metis +qed subsection \Tangent\ @@ -5238,10 +5242,11 @@ qed (use assms isCont_arccos in auto) lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)" -proof (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"]) - show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))" - apply (rule derivative_eq_intros | simp)+ +proof (rule DERIV_inverse_function) + have "inverse ((cos (arctan x))\<^sup>2) = 1 + x\<^sup>2" by (metis arctan cos_arctan_not_zero power_inverse tan_sec) + then show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))" + by (auto intro!: derivative_eq_intros) show "\y. \x - 1 < y; y < x + 1\ \ tan (arctan y) = y" using tan_arctan by blast show "1 + x\<^sup>2 \ 0" @@ -5999,19 +6004,15 @@ assumes "x \ 0" shows "arctan (1 / x) = sgn x * pi/2 - arctan x" proof (rule arctan_unique) + have \

: "x > 0 \ arctan x < pi" + using arctan_bounded [of x] by linarith show "- (pi/2) < sgn x * pi/2 - arctan x" - using arctan_bounded [of x] assms - unfolding sgn_real_def - apply (auto simp: arctan algebra_simps) - apply (drule zero_less_arctan_iff [THEN iffD2], arith) - done + using assms by (auto simp: sgn_real_def arctan algebra_simps \

) show "sgn x * pi/2 - arctan x < pi/2" using arctan_bounded [of "- x"] assms - unfolding sgn_real_def arctan_minus - by (auto simp: algebra_simps) + by (auto simp: algebra_simps sgn_real_def arctan_minus) show "tan (sgn x * pi/2 - arctan x) = 1 / x" - unfolding tan_inverse [of "arctan x", unfolded tan_arctan] - unfolding sgn_real_def + unfolding tan_inverse [of "arctan x", unfolded tan_arctan] sgn_real_def by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff) qed @@ -6032,18 +6033,18 @@ by (rule power2_le_imp_le [OF _ zero_le_one]) (simp add: power_divide divide_le_eq not_sum_power2_lt_zero) -lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one] - -lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one] - lemma polar_Ex: "\r::real. \a. x = r * cos a \ y = r * sin a" proof - - have polar_ex1: "0 < y \ \r a. x = r * cos a \ y = r * sin a" for y - apply (rule exI [where x = "sqrt (x\<^sup>2 + y\<^sup>2)"]) - apply (rule exI [where x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))"]) - apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide - real_sqrt_mult [symmetric] right_diff_distrib) - done + have polar_ex1: "\r a. x = r * cos a \ y = r * sin a" if "0 < y" for y + proof - + have "x = sqrt (x\<^sup>2 + y\<^sup>2) * cos (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))" + by (simp add: cos_arccos_abs [OF cos_x_y_le_one]) + moreover have "y = sqrt (x\<^sup>2 + y\<^sup>2) * sin (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))" + using that + by (simp add: sin_arccos_abs [OF cos_x_y_le_one] power_divide right_diff_distrib flip: real_sqrt_mult) + ultimately show ?thesis + by blast + qed show ?thesis proof (cases "0::real" y rule: linorder_cases) case less @@ -6083,24 +6084,24 @@ assumes m: "\i. i > m \ a i = 0" and n: "\j. j > n \ b j = 0" shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = - (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" -proof - + (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" +proof - + have "\i j. \m + n - i < j; a i \ 0\ \ b j = 0" + by (meson le_add_diff leI le_less_trans m n) + then have \

: "(\(i,j)\(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0" + by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral) have "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = (\i\m. \j\n. (a i * x ^ i) * (b j * x ^ j))" by (rule sum_product) also have "\ = (\i\m + n. \j\n + m. a i * x ^ i * (b j * x ^ j))" using assms by (auto simp: sum_up_index_split) also have "\ = (\r\m + n. \j\m + n - r. a r * x ^ r * (b j * x ^ j))" - apply (simp add: add_ac sum.Sigma product_atMost_eq_Un) - apply (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral) - apply (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE) - done + by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \

) also have "\ = (\(i,j)\{(i,j). i+j \ m+n}. (a i * x ^ i) * (b j * x ^ j))" by (auto simp: pairs_le_eq_Sigma sum.Sigma) + also have "... = (\k\m + n. \i\k. a i * x ^ i * (b (k - i) * x ^ (k - i)))" + by (rule sum.triangle_reindex_eq) also have "\ = (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" - apply (subst sum.triangle_reindex_eq) - apply (auto simp: algebra_simps sum_distrib_left intro!: sum.cong) - apply (metis le_add_diff_inverse power_add) - done + by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong) finally show ?thesis . qed @@ -6109,7 +6110,7 @@ assumes m: "\i. i > m \ a i = 0" and n: "\j. j > n \ b j = 0" shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = - (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" + (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" using polynomial_product [of m a n b x] assms by (simp only: of_nat_mult [symmetric] of_nat_power [symmetric] of_nat_eq_iff Int.int_sum [symmetric]) @@ -6148,10 +6149,10 @@ have "(\i=Suc j..n. a i * y^(i - j - 1)) = (\ki. i - (j + 1)) {Suc j..n} (lessThan (n-j))" - apply (auto simp: bij_betw_def inj_on_def) - apply (rule_tac x="x + Suc j" in image_eqI, auto) - done + have "\k. k < n - j \ k \ (\i. i - Suc j) ` {Suc j..n}" + by (rule_tac x="k + Suc j" in image_eqI, auto) + then have h: "bij_betw (\i. i - (j + 1)) {Suc j..n} (lessThan (n-j))" + by (auto simp: bij_betw_def inj_on_def) then show ?thesis by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp) qed