# HG changeset patch
# User huffman
# Date 1274137112 25200
# Node ID b877866b5b001fe13997827471d6df3533e3cd79
# Parent  522ed38eb70aad4a26c8a1367ad486df5b64e716
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used

diff -r 522ed38eb70a -r b877866b5b00 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Mon May 17 12:00:10 2010 -0700
+++ b/src/HOL/MacLaurin.thy	Mon May 17 15:58:32 2010 -0700
@@ -383,6 +383,11 @@
 
 text{*It is unclear why so many variant results are needed.*}
 
+lemma sin_expansion_lemma:
+     "sin (x + real (Suc m) * pi / 2) =  
+      cos (x + real (m) * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
        sin x =
@@ -394,7 +399,7 @@
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
@@ -414,7 +419,6 @@
 apply (blast intro: elim:); 
 done
 
-
 lemma Maclaurin_sin_expansion3:
      "[| n > 0; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
@@ -426,7 +430,7 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -444,7 +448,7 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -459,6 +463,10 @@
      (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
 by (induct "n", auto)
 
+lemma cos_expansion_lemma:
+  "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
        cos x =
@@ -470,7 +478,7 @@
 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)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (case_tac "n", simp)
 apply (simp del: setsum_op_ivl_Suc)
 apply (rule ccontr, simp)
@@ -493,7 +501,7 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -512,7 +520,7 @@
 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)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
diff -r 522ed38eb70a -r b877866b5b00 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon May 17 12:00:10 2010 -0700
+++ b/src/HOL/Transcendental.thy	Mon May 17 15:58:32 2010 -0700
@@ -2580,18 +2580,6 @@
 lemma tan_60: "tan (pi / 3) = sqrt 3"
 unfolding tan_def by (simp add: sin_60 cos_60)
 
-text{*NEEDED??*}
-lemma [simp]:
-     "sin (x + 1 / 2 * real (Suc m) * pi) =  
-      cos (x + 1 / 2 * real  (m) * pi)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
-
-text{*NEEDED??*}
-lemma [simp]:
-     "sin (x + real (Suc m) * pi / 2) =  
-      cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
-
 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
   by (auto intro!: DERIV_intros)
 
@@ -2620,16 +2608,6 @@
 apply (subst sin_add, simp)
 done
 
-(*NEEDED??*)
-lemma [simp]:
-     "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
-apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
-done
-
-(*NEEDED??*)
-lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
-
 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)