remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
authorhuffman
Mon May 17 15:58:32 2010 -0700 (2010-05-17)
changeset 36974b877866b5b00
parent 36971 522ed38eb70a
child 36975 fa6244be5215
remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
src/HOL/MacLaurin.thy
src/HOL/Transcendental.thy
     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.10 +by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
    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.56 +by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
    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])
     2.1 --- a/src/HOL/Transcendental.thy	Mon May 17 12:00:10 2010 -0700
     2.2 +++ b/src/HOL/Transcendental.thy	Mon May 17 15:58:32 2010 -0700
     2.3 @@ -2580,18 +2580,6 @@
     2.4  lemma tan_60: "tan (pi / 3) = sqrt 3"
     2.5  unfolding tan_def by (simp add: sin_60 cos_60)
     2.6  
     2.7 -text{*NEEDED??*}
     2.8 -lemma [simp]:
     2.9 -     "sin (x + 1 / 2 * real (Suc m) * pi) =  
    2.10 -      cos (x + 1 / 2 * real  (m) * pi)"
    2.11 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
    2.12 -
    2.13 -text{*NEEDED??*}
    2.14 -lemma [simp]:
    2.15 -     "sin (x + real (Suc m) * pi / 2) =  
    2.16 -      cos (x + real (m) * pi / 2)"
    2.17 -by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
    2.18 -
    2.19  lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
    2.20    by (auto intro!: DERIV_intros)
    2.21  
    2.22 @@ -2620,16 +2608,6 @@
    2.23  apply (subst sin_add, simp)
    2.24  done
    2.25  
    2.26 -(*NEEDED??*)
    2.27 -lemma [simp]:
    2.28 -     "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
    2.29 -apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
    2.30 -done
    2.31 -
    2.32 -(*NEEDED??*)
    2.33 -lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
    2.34 -by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
    2.35 -
    2.36  lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
    2.37  by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
    2.38