move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
1.1 --- a/src/HOL/Complex.thy Fri Aug 19 18:08:05 2011 -0700
1.2 +++ b/src/HOL/Complex.thy Fri Aug 19 18:42:41 2011 -0700
1.3 @@ -606,14 +606,6 @@
1.4 abbreviation expi :: "complex \<Rightarrow> complex"
1.5 where "expi \<equiv> exp"
1.6
1.7 -lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
1.8 - unfolding cos_coeff_def sin_coeff_def
1.9 - by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
1.10 -
1.11 -lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
1.12 - unfolding cos_coeff_def sin_coeff_def
1.13 - by (simp del: mult_Suc)
1.14 -
1.15 lemma expi_imaginary: "expi (Complex 0 b) = cis b"
1.16 proof (rule complex_eqI)
1.17 { fix n have "Complex 0 b ^ n =
2.1 --- a/src/HOL/MacLaurin.thy Fri Aug 19 18:08:05 2011 -0700
2.2 +++ b/src/HOL/MacLaurin.thy Fri Aug 19 18:42:41 2011 -0700
2.3 @@ -417,9 +417,6 @@
2.4 cos (x + real (m) * pi / 2)"
2.5 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
2.6
2.7 -lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
2.8 - unfolding sin_coeff_def by simp (* TODO: move *)
2.9 -
2.10 lemma Maclaurin_sin_expansion2:
2.11 "\<exists>t. abs t \<le> abs x &
2.12 sin x =
2.13 @@ -486,9 +483,6 @@
2.14
2.15 subsection{*Maclaurin Expansion for Cosine Function*}
2.16
2.17 -lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
2.18 - unfolding cos_coeff_def by simp (* TODO: move *)
2.19 -
2.20 lemma sumr_cos_zero_one [simp]:
2.21 "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
2.22 by (induct "n", auto)
3.1 --- a/src/HOL/Transcendental.thy Fri Aug 19 18:08:05 2011 -0700
3.2 +++ b/src/HOL/Transcendental.thy Fri Aug 19 18:42:41 2011 -0700
3.3 @@ -1220,6 +1220,20 @@
3.4 definition cos :: "real \<Rightarrow> real" where
3.5 "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
3.6
3.7 +lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
3.8 + unfolding sin_coeff_def by simp
3.9 +
3.10 +lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
3.11 + unfolding cos_coeff_def by simp
3.12 +
3.13 +lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
3.14 + unfolding cos_coeff_def sin_coeff_def
3.15 + by (simp del: mult_Suc)
3.16 +
3.17 +lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
3.18 + unfolding cos_coeff_def sin_coeff_def
3.19 + by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
3.20 +
3.21 lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
3.22 unfolding sin_coeff_def
3.23 apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
3.24 @@ -1238,42 +1252,27 @@
3.25 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
3.26 unfolding cos_def by (rule summable_cos [THEN summable_sums])
3.27
3.28 -lemma sin_fdiffs: "diffs sin_coeff = cos_coeff"
3.29 -unfolding sin_coeff_def cos_coeff_def
3.30 -by (auto intro!: ext
3.31 - simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
3.32 - simp del: mult_Suc of_nat_Suc)
3.33 -
3.34 -lemma sin_fdiffs2: "diffs sin_coeff n = cos_coeff n"
3.35 -by (simp only: sin_fdiffs)
3.36 -
3.37 -lemma cos_fdiffs: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
3.38 -unfolding sin_coeff_def cos_coeff_def
3.39 -by (auto intro!: ext
3.40 - simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
3.41 - simp del: mult_Suc of_nat_Suc)
3.42 -
3.43 -lemma cos_fdiffs2: "diffs cos_coeff n = - sin_coeff n"
3.44 -by (simp only: cos_fdiffs)
3.45 +lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
3.46 + by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
3.47 +
3.48 +lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
3.49 + by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
3.50
3.51 text{*Now at last we can get the derivatives of exp, sin and cos*}
3.52
3.53 -lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
3.54 -by (auto intro!: sums_unique sums_minus sin_converges)
3.55 -
3.56 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
3.57 -unfolding sin_def cos_def
3.58 -apply (auto simp add: sin_fdiffs2 [symmetric])
3.59 -apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
3.60 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
3.61 -done
3.62 + unfolding sin_def cos_def
3.63 + apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
3.64 + apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
3.65 + summable_minus summable_sin summable_cos)
3.66 + done
3.67
3.68 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
3.69 -unfolding cos_def
3.70 -apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
3.71 -apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
3.72 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
3.73 -done
3.74 + unfolding cos_def sin_def
3.75 + apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
3.76 + apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
3.77 + summable_minus summable_sin summable_cos suminf_minus)
3.78 + done
3.79
3.80 lemma isCont_sin: "isCont sin x"
3.81 by (rule DERIV_sin [THEN DERIV_isCont])