src/HOL/MacLaurin.thy
changeset 44306 33572a766836
parent 41166 4b2a457b17e8
child 44308 d2a6f9af02f4
     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])