# HG changeset patch
# User huffman
# Date 1181147525 -7200
# Node ID 375335bf619f8d90bbacd1b6f799e4caf17ee701
# Parent  aa158e145ea395c836fdcc38d2041c88671e552a
clean up proofs of exp_zero, sin_zero, cos_zero

diff -r aa158e145ea3 -r 375335bf619f src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 06 17:01:33 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 06 18:32:05 2007 +0200
@@ -659,14 +659,18 @@
 
 subsection{*Properties of the Exponential Function*}
 
-lemma exp_zero [simp]: "exp 0 = 1"
+lemma powser_zero:
+  fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra_1,recpower}"
+  shows "(\<Sum>n. f n * 0 ^ n) = f 0"
 proof -
-  have "(\<Sum>n = 0..<1. (0::'a) ^ n /# real (fact n)) =
-        (\<Sum>n. 0 ^ n /# real (fact n))"
+  have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
     by (rule sums_unique [OF series_zero], simp add: power_0_left)
-  thus ?thesis by (simp add: exp_def)
+  thus ?thesis by simp
 qed
 
+lemma exp_zero [simp]: "exp 0 = 1"
+unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
+
 lemma setsum_head2:
   "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}"
 by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost)
@@ -997,19 +1001,10 @@
 subsection{*Basic Properties of the Trigonometric Functions*}
 
 lemma sin_zero [simp]: "sin 0 = 0"
-by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
-         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}"
-by (auto intro: series_zero)
+unfolding sin_def by (simp add: powser_zero)
 
 lemma cos_zero [simp]: "cos 0 = 1"
-apply (simp add: cos_def)
-apply (rule sums_unique [symmetric])
-apply (cut_tac n = 1 and f = "(%n. (if even n then -1 ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2)
-apply auto
-done
+unfolding cos_def by (simp add: powser_zero)
 
 lemma DERIV_sin_sin_mult [simp]:
      "DERIV (%x. sin(x)*sin(x)) x :> cos(x) * sin(x) + cos(x) * sin(x)"