# HG changeset patch
# User huffman
# Date 1243486010 25200
# Node ID 703183ff0926525e3ea9d58356a01820c303028c
# Parent  0237e5e40b71791a512eb9c0913afd5812feaead# Parent  40c00d6848002d3bd122232cb51a79ed894a9f7d
merged

diff -r 40c00d684800 -r 703183ff0926 src/HOL/NSA/HTranscendental.thy
--- a/src/HOL/NSA/HTranscendental.thy	Wed May 27 22:20:29 2009 +0200
+++ b/src/HOL/NSA/HTranscendental.thy	Wed May 27 21:46:50 2009 -0700
@@ -18,13 +18,11 @@
 
 definition
   sinhr :: "real => hypreal" where
-  "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else
-             ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
+  "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))"
   
 definition
   coshr :: "real => hypreal" where
-  "coshr x = st(sumhr (0, whn, %n. (if even(n) then
-            ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
+  "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
 
 
 subsection{*Nonstandard Extension of Square Root Function*}
@@ -242,7 +240,7 @@
 apply (rule subst [where P="\<lambda>x. 1 \<approx> x", OF _ approx_refl])
 apply (rule rev_mp [OF hypnat_one_less_hypnat_omega])
 apply (rule_tac x="whn" in spec)
-apply (unfold sumhr_app, transfer, simp)
+apply (unfold sumhr_app, transfer, simp add: cos_coeff_def)
 done
 
 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
@@ -406,17 +404,14 @@
 Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
 *)
 
-lemma HFinite_sin [simp]:
-     "sumhr (0, whn, %n. (if even(n) then 0 else  
-              (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
-              \<in> HFinite"
+lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of)
 apply (rule NSBseqD2)
 apply (rule NSconvergent_NSBseq)
 apply (rule convergent_NSconvergent_iff [THEN iffD1])
 apply (rule summable_convergent_sumr_iff [THEN iffD1])
-apply (simp only: One_nat_def summable_sin)
+apply (rule summable_sin)
 done
 
 lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
@@ -432,10 +427,7 @@
            simp add: mult_assoc)
 done
 
-lemma HFinite_cos [simp]:
-     "sumhr (0, whn, %n. (if even(n) then  
-            (-1 ^ (n div 2))/(real (fact n)) else  
-            0) * x ^ n) \<in> HFinite"
+lemma HFinite_cos [simp]: "sumhr (0, whn, %n. cos_coeff n * x ^ n) \<in> HFinite"
 unfolding sumhr_app
 apply (simp only: star_zero_def starfun2_star_of)
 apply (rule NSBseqD2)
diff -r 40c00d684800 -r 703183ff0926 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed May 27 22:20:29 2009 +0200
+++ b/src/HOL/Transcendental.thy	Wed May 27 21:46:50 2009 -0700
@@ -1252,30 +1252,31 @@
 subsection {* Sine and Cosine *}
 
 definition
+  sin_coeff :: "nat \<Rightarrow> real" where
+  "sin_coeff = (\<lambda>n. if even n then 0 else -1 ^ ((n - Suc 0) div 2) / real (fact n))"
+
+definition
+  cos_coeff :: "nat \<Rightarrow> real" where
+  "cos_coeff = (\<lambda>n. if even n then (-1 ^ (n div 2)) / real (fact n) else 0)"
+
+definition
   sin :: "real => real" where
-  "sin x = (\<Sum>n. (if even(n) then 0 else
-             (-1 ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
- 
+  "sin x = (\<Sum>n. sin_coeff n * x ^ n)"
+
 definition
   cos :: "real => real" where
-  "cos x = (\<Sum>n. (if even(n) then (-1 ^ (n div 2))/(real (fact n)) 
-                            else 0) * x ^ n)"
-
-lemma summable_sin: 
-     "summable (%n.  
-           (if even n then 0  
-           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
-                x ^ n)"
+  "cos x = (\<Sum>n. cos_coeff n * x ^ n)"
+
+lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
+unfolding sin_coeff_def
 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
 apply (rule_tac [2] summable_exp)
 apply (rule_tac x = 0 in exI)
 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
 done
 
-lemma summable_cos: 
-      "summable (%n.  
-           (if even n then  
-           -1 ^ (n div 2)/(real (fact n)) else 0) * x ^ n)"
+lemma summable_cos: "summable (\<lambda>n. cos_coeff n * x ^ n)"
+unfolding cos_coeff_def
 apply (rule_tac g = "(%n. inverse (real (fact n)) * \<bar>x\<bar> ^ n)" in summable_comparison_test)
 apply (rule_tac [2] summable_exp)
 apply (rule_tac x = 0 in exI)
@@ -1304,71 +1305,39 @@
 apply (case_tac [2] "n", auto)
 done
 
-lemma sin_converges: 
-      "(%n. (if even n then 0  
-            else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
-                 x ^ n) sums sin(x)"
+lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
 unfolding sin_def by (rule summable_sin [THEN summable_sums])
 
-lemma cos_converges: 
-      "(%n. (if even n then  
-           -1 ^ (n div 2)/(real (fact n))  
-           else 0) * x ^ n) sums cos(x)"
+lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)"
 unfolding cos_def by (rule summable_cos [THEN summable_sums])
 
-lemma sin_fdiffs: 
-      "diffs(%n. if even n then 0  
-           else -1 ^ ((n - Suc 0) div 2)/(real (fact n)))  
-       = (%n. if even n then  
-                 -1 ^ (n div 2)/(real (fact n))  
-              else 0)"
+lemma sin_fdiffs: "diffs sin_coeff = cos_coeff"
+unfolding sin_coeff_def cos_coeff_def
 by (auto intro!: ext 
          simp add: diffs_def divide_inverse real_of_nat_def of_nat_mult
          simp del: mult_Suc of_nat_Suc)
 
-lemma sin_fdiffs2: 
-       "diffs(%n. if even n then 0  
-           else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) n  
-       = (if even n then  
-                 -1 ^ (n div 2)/(real (fact n))  
-              else 0)"
+lemma sin_fdiffs2: "diffs sin_coeff n = cos_coeff n"
 by (simp only: sin_fdiffs)
 
-lemma cos_fdiffs: 
-      "diffs(%n. if even n then  
-                 -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))))"
+lemma cos_fdiffs: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
+unfolding sin_coeff_def cos_coeff_def
 by (auto intro!: ext 
          simp add: diffs_def divide_inverse odd_Suc_mult_two_ex real_of_nat_def of_nat_mult
          simp del: mult_Suc of_nat_Suc)
 
-
-lemma cos_fdiffs2: 
-      "diffs(%n. if even n then  
-                 -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)))"
+lemma cos_fdiffs2: "diffs cos_coeff n = - sin_coeff n"
 by (simp only: cos_fdiffs)
 
 text{*Now at last we can get the derivatives of exp, sin and cos*}
 
-lemma lemma_sin_minus:
-     "- sin x = (\<Sum>n. - ((if even n then 0 
-                  else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n))"
+lemma lemma_sin_minus: "- sin x = (\<Sum>n. - (sin_coeff n * x ^ n))"
 by (auto intro!: sums_unique sums_minus sin_converges)
 
-lemma lemma_sin_ext:
-     "sin = (%x. \<Sum>n. 
-                   (if even n then 0  
-                       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) *  
-                   x ^ n)"
+lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
 by (auto intro!: ext simp add: sin_def)
 
-lemma lemma_cos_ext:
-     "cos = (%x. \<Sum>n. 
-                   (if even n then -1 ^ (n div 2)/(real (fact n)) else 0) *
-                   x ^ n)"
+lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
 by (auto intro!: ext simp add: cos_def)
 
 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
@@ -1396,10 +1365,10 @@
 subsection {* Properties of Sine and Cosine *}
 
 lemma sin_zero [simp]: "sin 0 = 0"
-unfolding sin_def by (simp add: powser_zero)
+unfolding sin_def sin_coeff_def by (simp add: powser_zero)
 
 lemma cos_zero [simp]: "cos 0 = 1"
-unfolding cos_def by (simp add: powser_zero)
+unfolding cos_def cos_coeff_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)"
@@ -1632,14 +1601,10 @@
      "(%n. -1 ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) 
       sums  sin x"
 proof -
-  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2.
-            (if even k then 0
-             else -1 ^ ((k - Suc 0) div 2) / real (fact k)) *
-            x ^ k) 
-	sums sin x"
+  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
     unfolding sin_def
     by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
-  thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
+  thus ?thesis unfolding One_nat_def sin_coeff_def by (simp add: mult_ac)
 qed
 
 text {* FIXME: This is a long, ugly proof! *}
@@ -1702,13 +1667,10 @@
 lemma cos_paired:
      "(%n. -1 ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
 proof -
-  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 cos x"
+  have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
     unfolding cos_def
     by (rule cos_converges [THEN sums_summable, THEN sums_group], simp) 
-  thus ?thesis by (simp add: mult_ac)
+  thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
 qed
 
 lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"