author huffman Sun, 20 May 2007 05:27:45 +0200 changeset 23043 5dbfd67516a4 parent 23042 492514b39956 child 23044 2ad82c359175
rearranged sections
```--- 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 (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 (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 (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 (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 @@
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 (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 (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 (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 (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"

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"

@@ -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:```