# HG changeset patch
# User huffman
# Date 1179631665 -7200
# Node ID 5dbfd67516a4cad8e00b8283601b1de57711c43e
# Parent  492514b39956e34fa260173f757cdb634ecf3bea
rearranged sections

diff -r 492514b39956 -r 5dbfd67516a4 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 03:19:42 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 05:27:45 2007 +0200
@@ -11,133 +11,7 @@
 imports NthRoot Fact Series EvenOdd Deriv
 begin
 
-definition
-  exp :: "real => real" where
-  "exp x = (\<Sum>n. inverse(real (fact n)) * (x ^ n))"
-
-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)"
- 
-definition
-  diffs :: "(nat => real) => nat => real" where
-  "diffs c = (%n. real (Suc n) * c(Suc 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)"
-  
-definition
-  ln :: "real => real" where
-  "ln x = (THE u. exp u = x)"
-
-definition
-  pi :: "real" where
-  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
-
-definition
-  tan :: "real => real" where
-  "tan x = (sin x)/(cos x)"
-
-definition
-  arcsin :: "real => real" where
-  "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
-
-definition
-  arccos :: "real => real" where
-  "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
-
-definition     
-  arctan :: "real => real" where
-  "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
-
-
-subsection{*Exponential Function*}
-
-lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
-apply (cut_tac 'a = real in zero_less_one [THEN dense], safe)
-apply (cut_tac x = r in reals_Archimedean3, auto)
-apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
-apply (rule_tac N = n and c = r in ratio_test)
-apply (safe, simp add: abs_mult mult_assoc [symmetric] del: fact_Suc)
-apply (rule mult_right_mono)
-apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
-apply (subst fact_Suc)
-apply (subst real_of_nat_mult)
-apply (auto)
-apply (simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
-apply (rule order_less_imp_le)
-apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: mult_assoc)
-apply (erule order_less_trans)
-apply (auto simp add: mult_less_cancel_left mult_ac)
-done
-
-lemma summable_sin: 
-     "summable (%n.  
-           (if even n then 0  
-           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
-                x ^ n)"
-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)"
-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 lemma_STAR_sin [simp]:
-     "(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]:
-     "0 < n -->  
-      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos1 [simp]:
-     "0 < n -->  
-      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos2 [simp]:
-  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
-                         else 0) = 0"
-apply (induct "n")
-apply (case_tac [2] "n", auto)
-done
-
-lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
-apply (simp add: exp_def)
-apply (rule summable_exp [THEN summable_sums])
-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)"
-apply (simp add: sin_def)
-apply (rule summable_sin [THEN summable_sums])
-done
-
-lemma cos_converges: 
-      "(%n. (if even n then  
-           (- 1) ^ (n div 2)/(real (fact n))  
-           else 0) * x ^ n) sums cos(x)"
-apply (simp add: cos_def)
-apply (rule summable_cos [THEN summable_sums])
-done
+subsection{*Properties of Power Series*}
 
 lemma lemma_realpow_diff [rule_format (no_asm)]:
      "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
@@ -149,9 +23,6 @@
        del: realpow_Suc)
 done
 
-
-subsection{*Properties of Power Series*}
-
 lemma lemma_realpow_diff_sumr:
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
@@ -239,7 +110,11 @@
 done
 
 
-subsection{*Differentiation of Power Series*}
+subsection{*Term-by-Term Differentiability of Power Series*}
+
+definition
+  diffs :: "(nat => real) => nat => real" where
+  "diffs c = (%n. real (Suc n) * c(Suc n))"
 
 text{*Lemma about distributing negation over it*}
 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
@@ -274,9 +149,6 @@
 apply (simp add: diffs_def summable_LIMSEQ_zero)
 done
 
-
-subsection{*Term-by-Term Differentiability of Power Series*}
-
 lemma lemma_termdiff1:
   "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
    (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
@@ -539,6 +411,116 @@
 qed
 
 
+subsection{*Exponential Function*}
+
+definition
+  exp :: "real => real" where
+  "exp x = (\<Sum>n. inverse(real (fact n)) * (x ^ n))"
+
+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)"
+ 
+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_exp: "summable (%n. inverse (real (fact n)) * x ^ n)"
+apply (cut_tac 'a = real in zero_less_one [THEN dense], safe)
+apply (cut_tac x = r in reals_Archimedean3, auto)
+apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
+apply (rule_tac N = n and c = r in ratio_test)
+apply (safe, simp add: abs_mult mult_assoc [symmetric] del: fact_Suc)
+apply (rule mult_right_mono)
+apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
+apply (subst fact_Suc)
+apply (subst real_of_nat_mult)
+apply (auto)
+apply (simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
+apply (rule order_less_imp_le)
+apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
+apply (auto simp add: mult_assoc)
+apply (erule order_less_trans)
+apply (auto simp add: mult_less_cancel_left mult_ac)
+done
+
+lemma summable_sin: 
+     "summable (%n.  
+           (if even n then 0  
+           else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) *  
+                x ^ n)"
+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)"
+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 lemma_STAR_sin [simp]:
+     "(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]:
+     "0 < n -->  
+      (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
+by (induct "n", auto)
+
+lemma lemma_STAR_cos1 [simp]:
+     "0 < n -->  
+      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
+by (induct "n", auto)
+
+lemma lemma_STAR_cos2 [simp]:
+  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
+                         else 0) = 0"
+apply (induct "n")
+apply (case_tac [2] "n", auto)
+done
+
+lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)"
+apply (simp add: exp_def)
+apply (rule summable_exp [THEN summable_sums])
+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)"
+apply (simp add: sin_def)
+apply (rule summable_sin [THEN summable_sums])
+done
+
+lemma cos_converges: 
+      "(%n. (if even n then  
+           (- 1) ^ (n div 2)/(real (fact n))  
+           else 0) * x ^ n) sums cos(x)"
+apply (simp add: cos_def)
+apply (rule summable_cos [THEN summable_sums])
+done
+
+lemma lemma_realpow_diff [rule_format (no_asm)]:
+     "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
+apply (induct "n", auto)
+apply (subgoal_tac "p = Suc n")
+apply (simp (no_asm_simp), auto)
+apply (drule sym)
+apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] 
+       del: realpow_Suc)
+done
+
+
 subsection{*Formal Derivatives of Exp, Sin, and Cos Series*} 
 
 lemma exp_fdiffs: 
@@ -780,13 +762,17 @@
 
 subsection{*Properties of the Logarithmic Function*}
 
-lemma ln_exp[simp]: "ln(exp x) = x"
+definition
+  ln :: "real => real" where
+  "ln x = (THE u. exp u = x)"
+
+lemma ln_exp [simp]: "ln (exp x) = x"
 by (simp add: ln_def)
 
 lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
 by (auto dest: exp_total)
 
-lemma exp_ln_iff[simp]: "(exp(ln x) = x) = (0 < x)"
+lemma exp_ln_iff [simp]: "(exp (ln x) = x) = (0 < x)"
 apply (auto dest: exp_total)
 apply (erule subst, simp) 
 done
@@ -1149,6 +1135,10 @@
 
 subsection{*The Constant Pi*}
 
+definition
+  pi :: "real" where
+  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
+
 text{*Show that there's a least positive @{term x} with @{term "cos(x) = 0"}; 
    hence define pi.*}
 
@@ -1548,6 +1538,10 @@
 
 subsection{*Tangent*}
 
+definition
+  tan :: "real => real" where
+  "tan x = (sin x)/(cos x)"
+
 lemma tan_zero [simp]: "tan 0 = 0"
 by (simp add: tan_def)
 
@@ -1678,6 +1672,21 @@
 	    simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym]) 
 done
 
+
+subsection {* Inverse Trigonometric Functions *}
+
+definition
+  arcsin :: "real => real" where
+  "arcsin y = (THE x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
+
+definition
+  arccos :: "real => real" where
+  "arccos y = (THE x. 0 \<le> x & x \<le> pi & cos x = y)"
+
+definition     
+  arctan :: "real => real" where
+  "arctan y = (THE x. -(pi/2) < x & x < pi/2 & tan x = y)"
+
 lemma arcsin:
      "[| -1 \<le> y; y \<le> 1 |]  
       ==> -(pi/2) \<le> arcsin y &  
@@ -1803,6 +1812,8 @@
         simp del: realpow_Suc)
 done
 
+subsection {* More Theorems about Sin and Cos *}
+
 text{*NEEDED??*}
 lemma [simp]:
      "sin (x + 1 / 2 * real (Suc m) * pi) =  
@@ -2056,6 +2067,8 @@
 apply (auto intro: lemma_DERIV_ln3 simp del: exp_ln)
 done
 
+subsection {* Theorems about Limits *}
+
 (* need to rename second isCont_inverse *)
 
 lemma isCont_inv_fun: