author huffman Tue, 05 Jun 2007 07:58:50 +0200 changeset 23242 e1526d5fa80d parent 23241 5f12b40a95bf child 23243 a37d3e6e8323
remove simp attribute from lemma_STAR theorems
```--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Jun 05 07:58:50 2007 +0200
@@ -420,7 +420,7 @@
apply safe
apply (simp (no_asm))
apply (simp (no_asm))
-apply (case_tac "n", clarify, simp, simp)
+apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)```
```--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Jun 05 07:58:50 2007 +0200
@@ -516,22 +516,22 @@
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done

-lemma lemma_STAR_sin [simp]:
+lemma lemma_STAR_sin:
"(if even n then 0
else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
by (induct "n", auto)

-lemma lemma_STAR_cos [simp]:
+lemma lemma_STAR_cos:
"0 < n -->
-1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
by (induct "n", auto)

-lemma lemma_STAR_cos1 [simp]:
+lemma lemma_STAR_cos1:
"0 < n -->
(-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
by (induct "n", auto)

-lemma lemma_STAR_cos2 [simp]:
+lemma lemma_STAR_cos2:
"(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
else 0) = 0"
apply (induct "n")
@@ -1001,7 +1001,7 @@

lemma sin_zero [simp]: "sin 0 = 0"
by (auto intro!: sums_unique [symmetric] LIMSEQ_const
-         simp add: sin_def sums_def simp del: power_0_left)
+         simp add: sin_def sums_def lemma_STAR_sin)

lemma lemma_series_zero2:
"(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"```