src/HOL/MacLaurin.thy
 changeset 36974 b877866b5b00 parent 32047 c141f139ce26 child 41120 74e41b2d48ea
```     1.1 --- a/src/HOL/MacLaurin.thy	Mon May 17 12:00:10 2010 -0700
1.2 +++ b/src/HOL/MacLaurin.thy	Mon May 17 15:58:32 2010 -0700
1.3 @@ -383,6 +383,11 @@
1.4
1.5  text{*It is unclear why so many variant results are needed.*}
1.6
1.7 +lemma sin_expansion_lemma:
1.8 +     "sin (x + real (Suc m) * pi / 2) =
1.9 +      cos (x + real (m) * pi / 2)"
1.11 +
1.12  lemma Maclaurin_sin_expansion2:
1.13       "\<exists>t. abs t \<le> abs x &
1.14         sin x =
1.15 @@ -394,7 +399,7 @@
1.16          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
1.17  apply safe
1.18  apply (simp (no_asm))
1.19 -apply (simp (no_asm))
1.20 +apply (simp (no_asm) add: sin_expansion_lemma)
1.21  apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
1.22  apply (rule ccontr, simp)
1.23  apply (drule_tac x = x in spec, simp)
1.24 @@ -414,7 +419,6 @@
1.25  apply (blast intro: elim:);
1.26  done
1.27
1.28 -
1.29  lemma Maclaurin_sin_expansion3:
1.30       "[| n > 0; 0 < x |] ==>
1.31         \<exists>t. 0 < t & t < x &
1.32 @@ -426,7 +430,7 @@
1.33  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.34  apply safe
1.35  apply simp
1.36 -apply (simp (no_asm))
1.37 +apply (simp (no_asm) add: sin_expansion_lemma)
1.38  apply (erule ssubst)
1.39  apply (rule_tac x = t in exI, simp)
1.40  apply (rule setsum_cong[OF refl])
1.41 @@ -444,7 +448,7 @@
1.42  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.43  apply safe
1.44  apply simp
1.45 -apply (simp (no_asm))
1.46 +apply (simp (no_asm) add: sin_expansion_lemma)
1.47  apply (erule ssubst)
1.48  apply (rule_tac x = t in exI, simp)
1.49  apply (rule setsum_cong[OF refl])
1.50 @@ -459,6 +463,10 @@
1.51       (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
1.52  by (induct "n", auto)
1.53
1.54 +lemma cos_expansion_lemma:
1.55 +  "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
1.57 +
1.58  lemma Maclaurin_cos_expansion:
1.59       "\<exists>t. abs t \<le> abs x &
1.60         cos x =
1.61 @@ -470,7 +478,7 @@
1.62  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.63  apply safe
1.64  apply (simp (no_asm))
1.65 -apply (simp (no_asm))
1.66 +apply (simp (no_asm) add: cos_expansion_lemma)
1.67  apply (case_tac "n", simp)
1.68  apply (simp del: setsum_op_ivl_Suc)
1.69  apply (rule ccontr, simp)
1.70 @@ -493,7 +501,7 @@
1.71  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.72  apply safe
1.73  apply simp
1.74 -apply (simp (no_asm))
1.75 +apply (simp (no_asm) add: cos_expansion_lemma)
1.76  apply (erule ssubst)
1.77  apply (rule_tac x = t in exI, simp)
1.78  apply (rule setsum_cong[OF refl])
1.79 @@ -512,7 +520,7 @@
1.80  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.81  apply safe
1.82  apply simp
1.83 -apply (simp (no_asm))
1.84 +apply (simp (no_asm) add: cos_expansion_lemma)
1.85  apply (erule ssubst)
1.86  apply (rule_tac x = t in exI, simp)
1.87  apply (rule setsum_cong[OF refl])
```