author huffman Fri Aug 19 08:39:43 2011 -0700 (2011-08-19) changeset 44306 33572a766836 parent 44305 3bdc02eb1637 child 44307 6a383003d0a9
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
 src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | revisions src/HOL/MacLaurin.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 07:45:22 2011 -0700
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 19 08:39:43 2011 -0700
1.3 @@ -839,7 +839,8 @@
1.4        cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
1.5        + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
1.6        (is "_ = ?SUM + ?rest / ?fact * ?pow")
1.7 -      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`] by auto
1.8 +      using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
1.9 +      unfolding cos_coeff_def by auto
1.10
1.11      have "cos t * -1^n = cos t * cos (n * pi) + sin t * sin (n * pi)" by auto
1.12      also have "\<dots> = cos (t + n * pi)"  using cos_add by auto
1.13 @@ -951,7 +952,8 @@
1.14        sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
1.15        + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
1.16        (is "_ = ?SUM + ?rest / ?fact * ?pow")
1.17 -      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`] by auto
1.18 +      using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
1.19 +      unfolding sin_coeff_def by auto
1.20
1.21      have "?rest = cos t * -1^n" unfolding sin_add cos_add real_of_nat_add left_distrib right_distrib by auto
1.22      moreover
```
```     2.1 --- a/src/HOL/MacLaurin.thy	Fri Aug 19 07:45:22 2011 -0700
2.2 +++ b/src/HOL/MacLaurin.thy	Fri Aug 19 08:39:43 2011 -0700
2.3 @@ -417,32 +417,32 @@
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 -       (\<Sum>m=0..<n. (if even m then 0
2.14 -                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
2.15 -                       x ^ m)
2.16 +       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
2.17        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.18  apply (cut_tac f = sin and n = n and x = x
2.19          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
2.20  apply safe
2.21  apply (simp (no_asm))
2.22  apply (simp (no_asm) add: sin_expansion_lemma)
2.23 -apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
2.24 +apply (subst (asm) setsum_0', clarify, case_tac "a", simp, simp)
2.25 +apply (cases n, simp, simp)
2.26  apply (rule ccontr, simp)
2.27  apply (drule_tac x = x in spec, simp)
2.28  apply (erule ssubst)
2.29  apply (rule_tac x = t in exI, simp)
2.30  apply (rule setsum_cong[OF refl])
2.31 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
2.32 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
2.33  done
2.34
2.35  lemma Maclaurin_sin_expansion:
2.36       "\<exists>t. sin x =
2.37 -       (\<Sum>m=0..<n. (if even m then 0
2.38 -                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
2.39 -                       x ^ m)
2.40 +       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
2.41        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.42  apply (insert Maclaurin_sin_expansion2 [of x n])
2.43  apply (blast intro: elim:)
2.44 @@ -452,9 +452,7 @@
2.45       "[| n > 0; 0 < x |] ==>
2.46         \<exists>t. 0 < t & t < x &
2.47         sin x =
2.48 -       (\<Sum>m=0..<n. (if even m then 0
2.49 -                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
2.50 -                       x ^ m)
2.51 +       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
2.52        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
2.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)
2.54  apply safe
2.55 @@ -463,16 +461,14 @@
2.56  apply (erule ssubst)
2.57  apply (rule_tac x = t in exI, simp)
2.58  apply (rule setsum_cong[OF refl])
2.59 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
2.60 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
2.61  done
2.62
2.63  lemma Maclaurin_sin_expansion4:
2.64       "0 < x ==>
2.65         \<exists>t. 0 < t & t \<le> x &
2.66         sin x =
2.67 -       (\<Sum>m=0..<n. (if even m then 0
2.68 -                       else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
2.69 -                       x ^ m)
2.70 +       (\<Sum>m=0..<n. sin_coeff m * x ^ m)
2.71        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.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)
2.73  apply safe
2.74 @@ -481,15 +477,17 @@
2.75  apply (erule ssubst)
2.76  apply (rule_tac x = t in exI, simp)
2.77  apply (rule setsum_cong[OF refl])
2.78 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
2.79 +apply (auto simp add: sin_coeff_def sin_zero_iff odd_Suc_mult_two_ex)
2.80  done
2.81
2.82
2.83  subsection{*Maclaurin Expansion for Cosine Function*}
2.84
2.85 +lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
2.86 +  unfolding cos_coeff_def by simp (* TODO: move *)
2.87 +
2.88  lemma sumr_cos_zero_one [simp]:
2.89 - "(\<Sum>m=0..<(Suc n).
2.90 -     (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
2.91 +  "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
2.92  by (induct "n", auto)
2.93
2.94  lemma cos_expansion_lemma:
2.95 @@ -499,10 +497,7 @@
2.96  lemma Maclaurin_cos_expansion:
2.97       "\<exists>t. abs t \<le> abs x &
2.98         cos x =
2.99 -       (\<Sum>m=0..<n. (if even m
2.100 -                       then -1 ^ (m div 2)/(real (fact m))
2.101 -                       else 0) *
2.102 -                       x ^ m)
2.103 +       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
2.104        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.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)
2.106  apply safe
2.107 @@ -515,17 +510,14 @@
2.108  apply (erule ssubst)
2.109  apply (rule_tac x = t in exI, simp)
2.110  apply (rule setsum_cong[OF refl])
2.111 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
2.112 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
2.113  done
2.114
2.115  lemma Maclaurin_cos_expansion2:
2.116       "[| 0 < x; n > 0 |] ==>
2.117         \<exists>t. 0 < t & t < x &
2.118         cos x =
2.119 -       (\<Sum>m=0..<n. (if even m
2.120 -                       then -1 ^ (m div 2)/(real (fact m))
2.121 -                       else 0) *
2.122 -                       x ^ m)
2.123 +       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
2.124        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.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)
2.126  apply safe
2.127 @@ -534,17 +526,14 @@
2.128  apply (erule ssubst)
2.129  apply (rule_tac x = t in exI, simp)
2.130  apply (rule setsum_cong[OF refl])
2.131 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
2.132 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
2.133  done
2.134
2.135  lemma Maclaurin_minus_cos_expansion:
2.136       "[| x < 0; n > 0 |] ==>
2.137         \<exists>t. x < t & t < 0 &
2.138         cos x =
2.139 -       (\<Sum>m=0..<n. (if even m
2.140 -                       then -1 ^ (m div 2)/(real (fact m))
2.141 -                       else 0) *
2.142 -                       x ^ m)
2.143 +       (\<Sum>m=0..<n. cos_coeff m * x ^ m)
2.144        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
2.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)
2.146  apply safe
2.147 @@ -553,7 +542,7 @@
2.148  apply (erule ssubst)
2.149  apply (rule_tac x = t in exI, simp)
2.150  apply (rule setsum_cong[OF refl])
2.151 -apply (auto simp add: cos_zero_iff even_mult_two_ex)
2.152 +apply (auto simp add: cos_coeff_def cos_zero_iff even_mult_two_ex)
2.153  done
2.154
2.155  (* ------------------------------------------------------------------------- *)
2.156 @@ -565,8 +554,8 @@
2.157  by auto
2.158
2.159  lemma Maclaurin_sin_bound:
2.160 -  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
2.161 -  x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
2.162 +  "abs(sin x - (\<Sum>m=0..<n. sin_coeff m * x ^ m))
2.163 +  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
2.164  proof -
2.165    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
2.166      by (rule_tac mult_right_mono,simp_all)
2.167 @@ -592,6 +581,7 @@
2.168      apply (safe dest!: mod_eqD, simp_all)
2.169      done
2.170    show ?thesis
2.171 +    unfolding sin_coeff_def
2.172      apply (subst t2)
2.173      apply (rule sin_bound_lemma)
2.174      apply (rule setsum_cong[OF refl])
```