src/HOL/Transcendental.thy
changeset 44319 806e0390de53
parent 44318 425c1f8f9487
child 44568 e6f291cb5810
     1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 18:08:05 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 18:42:41 2011 -0700
     1.3 @@ -1220,6 +1220,20 @@
     1.4  definition cos :: "real \<Rightarrow> real" where
     1.5    "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
     1.6  
     1.7 +lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
     1.8 +  unfolding sin_coeff_def by simp
     1.9 +
    1.10 +lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
    1.11 +  unfolding cos_coeff_def by simp
    1.12 +
    1.13 +lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
    1.14 +  unfolding cos_coeff_def sin_coeff_def
    1.15 +  by (simp del: mult_Suc)
    1.16 +
    1.17 +lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
    1.18 +  unfolding cos_coeff_def sin_coeff_def
    1.19 +  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
    1.20 +
    1.21  lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
    1.22  unfolding sin_coeff_def
    1.23  apply (rule summable_comparison_test [OF _ summable_exp [where x="\<bar>x\<bar>"]])
    1.24 @@ -1238,42 +1252,27 @@
    1.25  lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
    1.26  unfolding cos_def by (rule summable_cos [THEN summable_sums])
    1.27  
    1.28 -lemma sin_fdiffs: "diffs sin_coeff = cos_coeff"
    1.29 -unfolding sin_coeff_def cos_coeff_def
    1.30 -by (auto intro!: ext
    1.31 -         simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
    1.32 -         simp del: mult_Suc of_nat_Suc)
    1.33 -
    1.34 -lemma sin_fdiffs2: "diffs sin_coeff n = cos_coeff n"
    1.35 -by (simp only: sin_fdiffs)
    1.36 -
    1.37 -lemma cos_fdiffs: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
    1.38 -unfolding sin_coeff_def cos_coeff_def
    1.39 -by (auto intro!: ext
    1.40 -         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
    1.41 -         simp del: mult_Suc of_nat_Suc)
    1.42 -
    1.43 -lemma cos_fdiffs2: "diffs cos_coeff n = - sin_coeff n"
    1.44 -by (simp only: cos_fdiffs)
    1.45 +lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
    1.46 +  by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
    1.47 +
    1.48 +lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
    1.49 +  by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
    1.50  
    1.51  text{*Now at last we can get the derivatives of exp, sin and cos*}
    1.52  
    1.53 -lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
    1.54 -by (auto intro!: sums_unique sums_minus sin_converges)
    1.55 -
    1.56  lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
    1.57 -unfolding sin_def cos_def
    1.58 -apply (auto simp add: sin_fdiffs2 [symmetric])
    1.59 -apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
    1.60 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
    1.61 -done
    1.62 +  unfolding sin_def cos_def
    1.63 +  apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
    1.64 +  apply (simp_all add: diffs_sin_coeff diffs_cos_coeff
    1.65 +    summable_minus summable_sin summable_cos)
    1.66 +  done
    1.67  
    1.68  lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
    1.69 -unfolding cos_def
    1.70 -apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
    1.71 -apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
    1.72 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
    1.73 -done
    1.74 +  unfolding cos_def sin_def
    1.75 +  apply (rule DERIV_cong, rule termdiffs [where K="1 + \<bar>x\<bar>"])
    1.76 +  apply (simp_all add: diffs_sin_coeff diffs_cos_coeff diffs_minus
    1.77 +    summable_minus summable_sin summable_cos suminf_minus)
    1.78 +  done
    1.79  
    1.80  lemma isCont_sin: "isCont sin x"
    1.81    by (rule DERIV_sin [THEN DERIV_isCont])