1.1 --- a/src/HOL/MacLaurin.thy Fri Aug 19 07:45:22 2011 -0700
1.2 +++ b/src/HOL/MacLaurin.thy Fri Aug 19 08:39:43 2011 -0700
1.3 @@ -417,32 +417,32 @@
1.4 cos (x + real (m) * pi / 2)"
1.5 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
1.6
1.7 +lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
1.8 + unfolding sin_coeff_def by simp (* TODO: move *)
1.9 +
1.10 lemma Maclaurin_sin_expansion2:
1.11 "\<exists>t. abs t \<le> abs x &
1.12 sin x =
1.13 - (\<Sum>m=0..<n. (if even m then 0
1.14 - else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
1.15 - x ^ m)
1.16 + (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.17 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.18 apply (cut_tac f = sin and n = n and x = x
1.19 and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.20 apply safe
1.21 apply (simp (no_asm))
1.22 apply (simp (no_asm) add: sin_expansion_lemma)
1.23 -apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
1.24 +apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
1.25 +apply (cases n, simp, simp)
1.26 apply (rule ccontr, simp)
1.27 apply (drule_tac x = x in spec, simp)
1.28 apply (erule ssubst)
1.29 apply (rule_tac x = t in exI, simp)
1.30 apply (rule setsum_cong[OF refl])
1.31 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.32 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
1.33 done
1.34
1.35 lemma Maclaurin_sin_expansion:
1.36 "\<exists>t. sin x =
1.37 - (\<Sum>m=0..<n. (if even m then 0
1.38 - else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
1.39 - x ^ m)
1.40 + (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.41 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.42 apply (insert Maclaurin_sin_expansion2 [of x n])
1.43 apply (blast intro: elim:)
1.44 @@ -452,9 +452,7 @@
1.45 "[| n > 0; 0 < x |] ==>
1.46 \<exists>t. 0 < t & t < x &
1.47 sin x =
1.48 - (\<Sum>m=0..<n. (if even m then 0
1.49 - else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
1.50 - x ^ m)
1.51 + (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.52 + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
1.53 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.54 apply safe
1.55 @@ -463,16 +461,14 @@
1.56 apply (erule ssubst)
1.57 apply (rule_tac x = t in exI, simp)
1.58 apply (rule setsum_cong[OF refl])
1.59 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.60 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
1.61 done
1.62
1.63 lemma Maclaurin_sin_expansion4:
1.64 "0 < x ==>
1.65 \<exists>t. 0 < t & t \<le> x &
1.66 sin x =
1.67 - (\<Sum>m=0..<n. (if even m then 0
1.68 - else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
1.69 - x ^ m)
1.70 + (\<Sum>m=0..<n. sin_coeff m * x ^ m)
1.71 + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.72 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
1.73 apply safe
1.74 @@ -481,15 +477,17 @@
1.75 apply (erule ssubst)
1.76 apply (rule_tac x = t in exI, simp)
1.77 apply (rule setsum_cong[OF refl])
1.78 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
1.79 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
1.80 done
1.81
1.82
1.83 subsection{*Maclaurin Expansion for Cosine Function*}
1.84
1.85 +lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
1.86 + unfolding cos_coeff_def by simp (* TODO: move *)
1.87 +
1.88 lemma sumr_cos_zero_one [simp]:
1.89 - "(\<Sum>m=0..<(Suc n).
1.90 - (if even m then -1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1"
1.91 + "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
1.92 by (induct "n", auto)
1.93
1.94 lemma cos_expansion_lemma:
1.95 @@ -499,10 +497,7 @@
1.96 lemma Maclaurin_cos_expansion:
1.97 "\<exists>t. abs t \<le> abs x &
1.98 cos x =
1.99 - (\<Sum>m=0..<n. (if even m
1.100 - then -1 ^ (m div 2)/(real (fact m))
1.101 - else 0) *
1.102 - x ^ m)
1.103 + (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.104 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.105 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
1.106 apply safe
1.107 @@ -515,17 +510,14 @@
1.108 apply (erule ssubst)
1.109 apply (rule_tac x = t in exI, simp)
1.110 apply (rule setsum_cong[OF refl])
1.111 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.112 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
1.113 done
1.114
1.115 lemma Maclaurin_cos_expansion2:
1.116 "[| 0 < x; n > 0 |] ==>
1.117 \<exists>t. 0 < t & t < x &
1.118 cos x =
1.119 - (\<Sum>m=0..<n. (if even m
1.120 - then -1 ^ (m div 2)/(real (fact m))
1.121 - else 0) *
1.122 - x ^ m)
1.123 + (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.124 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.125 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
1.126 apply safe
1.127 @@ -534,17 +526,14 @@
1.128 apply (erule ssubst)
1.129 apply (rule_tac x = t in exI, simp)
1.130 apply (rule setsum_cong[OF refl])
1.131 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.132 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
1.133 done
1.134
1.135 lemma Maclaurin_minus_cos_expansion:
1.136 "[| x < 0; n > 0 |] ==>
1.137 \<exists>t. x < t & t < 0 &
1.138 cos x =
1.139 - (\<Sum>m=0..<n. (if even m
1.140 - then -1 ^ (m div 2)/(real (fact m))
1.141 - else 0) *
1.142 - x ^ m)
1.143 + (\<Sum>m=0..<n. cos_coeff m * x ^ m)
1.144 + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
1.145 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
1.146 apply safe
1.147 @@ -553,7 +542,7 @@
1.148 apply (erule ssubst)
1.149 apply (rule_tac x = t in exI, simp)
1.150 apply (rule setsum_cong[OF refl])
1.151 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
1.152 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
1.153 done
1.154
1.155 (* ------------------------------------------------------------------------- *)
1.156 @@ -565,8 +554,8 @@
1.157 by auto
1.158
1.159 lemma Maclaurin_sin_bound:
1.160 - "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
1.161 - x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
1.162 + "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
1.163 + \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
1.164 proof -
1.165 have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
1.166 by (rule_tac mult_right_mono,simp_all)
1.167 @@ -592,6 +581,7 @@
1.168 apply (safe dest!: mod_eqD, simp_all)
1.169 done
1.170 show ?thesis
1.171 + unfolding sin_coeff_def
1.172 apply (subst t2)
1.173 apply (rule sin_bound_lemma)
1.174 apply (rule setsum_cong[OF refl])