remove simp attribute from lemma_STAR theorems
authorhuffman
Tue Jun 05 07:58:50 2007 +0200 (2007-06-05)
changeset 23242e1526d5fa80d
parent 23241 5f12b40a95bf
child 23243 a37d3e6e8323
remove simp attribute from lemma_STAR theorems
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 00:54:03 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 07:58:50 2007 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4  apply safe
     1.5  apply (simp (no_asm))
     1.6  apply (simp (no_asm))
     1.7 -apply (case_tac "n", clarify, simp, simp)
     1.8 +apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
     1.9  apply (rule ccontr, simp)
    1.10  apply (drule_tac x = x in spec, simp)
    1.11  apply (erule ssubst)
     2.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 00:54:03 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 07:58:50 2007 +0200
     2.3 @@ -516,22 +516,22 @@
     2.4  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
     2.5  done
     2.6  
     2.7 -lemma lemma_STAR_sin [simp]:
     2.8 +lemma lemma_STAR_sin:
     2.9       "(if even n then 0  
    2.10         else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
    2.11  by (induct "n", auto)
    2.12  
    2.13 -lemma lemma_STAR_cos [simp]:
    2.14 +lemma lemma_STAR_cos:
    2.15       "0 < n -->  
    2.16        -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    2.17  by (induct "n", auto)
    2.18  
    2.19 -lemma lemma_STAR_cos1 [simp]:
    2.20 +lemma lemma_STAR_cos1:
    2.21       "0 < n -->  
    2.22        (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    2.23  by (induct "n", auto)
    2.24  
    2.25 -lemma lemma_STAR_cos2 [simp]:
    2.26 +lemma lemma_STAR_cos2:
    2.27    "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n 
    2.28                           else 0) = 0"
    2.29  apply (induct "n")
    2.30 @@ -1001,7 +1001,7 @@
    2.31  
    2.32  lemma sin_zero [simp]: "sin 0 = 0"
    2.33  by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
    2.34 -         simp add: sin_def sums_def simp del: power_0_left)
    2.35 +         simp add: sin_def sums_def lemma_STAR_sin)
    2.36  
    2.37  lemma lemma_series_zero2:
    2.38   "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"