# HG changeset patch
# User huffman
# Date 1180643030 -7200
# Node ID 40a760921d94a7f81412383725d1c422892af0f3
# Parent  267ba70e7a9dcab574c7b9dd861a75a3f5f19898
simplify some proofs

diff -r 267ba70e7a9d -r 40a760921d94 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 21:09:14 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu May 31 22:23:50 2007 +0200
@@ -580,9 +580,7 @@
        = (if even n then  
                  (- 1) ^ (n div 2)/(real (fact n))  
               else 0)"
-by (auto intro!: ext 
-         simp add: diffs_def divide_inverse real_of_nat_def
-         simp del: mult_Suc of_nat_Suc)
+by (simp only: sin_fdiffs)
 
 lemma cos_fdiffs: 
       "diffs(%n. if even n then  
@@ -599,9 +597,7 @@
                  (- 1) ^ (n div 2)/(real (fact n)) else 0) n 
        = - (if even n then 0  
            else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))"
-by (auto intro!: ext 
-         simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def
-         simp del: mult_Suc of_nat_Suc)
+by (simp only: cos_fdiffs)
 
 text{*Now at last we can get the derivatives of exp, sin and cos*}
 
@@ -1254,12 +1250,10 @@
             (if even k then 0
              else (- 1) ^ ((k - Suc 0) div 2) / real (fact k)) *
             x ^ k) 
-	sums
-	(\<Sum>n. (if even n then 0
-		     else (- 1) ^ ((n - Suc 0) div 2) / real (fact n)) *
-	            x ^ n)" 
+	sums sin x"
+    unfolding sin_def
     by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
-  thus ?thesis by (simp add: mult_ac sin_def)
+  thus ?thesis by (simp add: mult_ac)
 qed
 
 lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
@@ -1323,11 +1317,10 @@
   have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
             (if even k then (- 1) ^ (k div 2) / real (fact k) else 0) *
             x ^ k) 
-        sums
-	(\<Sum>n. (if even n then (- 1) ^ (n div 2) / real (fact n) else 0) *
-	      x ^ n)" 
+        sums cos x"
+    unfolding cos_def
     by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) 
-  thus ?thesis by (simp add: mult_ac cos_def)
+  thus ?thesis by (simp add: mult_ac)
 qed
 
 declare zero_less_power [simp]