# HG changeset patch
# User huffman
# Date 1159078941 -7200
# Node ID 3b887ad7d1969b91dc33940b5250ac657e6e1c52
# Parent  1cc6fefbff1a8c28cd22c7ef7a49b23bf96bf215
reorganized subsection headings

diff -r 1cc6fefbff1a -r 3b887ad7d196 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 07:18:16 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 08:22:21 2006 +0200
@@ -65,18 +65,125 @@
   "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
 
 
-subsection{*LIMSEQ and NSLIMSEQ*}
+subsection {* Limits of Sequences *}
+
+subsubsection {* Purely standard proofs *}
 
 lemma LIMSEQ_iff:
       "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
 by (simp add: LIMSEQ_def)
 
+lemma LIMSEQ_const: "(%n. k) ----> k"
+by (simp add: LIMSEQ_def)
+
+lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
+apply (simp add: LIMSEQ_def, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="no" in exI, safe)
+apply (drule_tac x="n" in spec, safe)
+apply (erule order_le_less_trans [OF norm_triangle_ineq3])
+done
+
+lemma LIMSEQ_ignore_initial_segment: "f ----> a 
+  ==> (%n. f(n + k)) ----> a"
+  apply (unfold LIMSEQ_def) 
+  apply (clarify)
+  apply (drule_tac x = r in spec)
+  apply (clarify)
+  apply (rule_tac x = "no + k" in exI)
+  by auto
+
+lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
+    f ----> a"
+  apply (unfold LIMSEQ_def)
+  apply clarsimp
+  apply (drule_tac x = r in spec)
+  apply clarsimp
+  apply (rule_tac x = "no + k" in exI)
+  apply clarsimp
+  apply (drule_tac x = "n - k" in spec)
+  apply (frule mp)
+  apply arith
+  apply simp
+done
+
+subsubsection {* Purely nonstandard proofs *}
+
 lemma NSLIMSEQ_iff:
     "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 by (simp add: NSLIMSEQ_def)
 
+lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
+by (simp add: NSLIMSEQ_def)
+
+lemma NSLIMSEQ_add:
+      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
+by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
+
+lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
+by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
+
+lemma NSLIMSEQ_mult:
+  fixes a b :: "'a::real_normed_algebra"
+  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
+by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
+
+lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
+by (auto simp add: NSLIMSEQ_def)
+
+lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
+by (drule NSLIMSEQ_minus, simp)
+
+(* FIXME: delete *)
+lemma NSLIMSEQ_add_minus:
+     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
+by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
+
+lemma NSLIMSEQ_diff:
+     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
+by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
+
+lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
+by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
+
+lemma NSLIMSEQ_inverse:
+  fixes a :: "'a::real_normed_div_algebra"
+  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
+by (simp add: NSLIMSEQ_def star_of_approx_inverse)
+
+lemma NSLIMSEQ_mult_inverse:
+  fixes a b :: "'a::real_normed_field"
+  shows
+     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
+by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
+
+lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
+by transfer simp
+
+lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
+by transfer simp
+
+lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
+by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
+
+text{*Uniqueness of limit*}
+lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
+apply (simp add: NSLIMSEQ_def)
+apply (drule HNatInfinite_whn [THEN [2] bspec])+
+apply (auto dest: approx_trans3)
+done
+
+lemma NSLIMSEQ_pow [rule_format]:
+  fixes a :: "'a::{real_normed_algebra,recpower}"
+  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
+apply (induct "m")
+apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
+done
+
+subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
 
 text{*LIMSEQ ==> NSLIMSEQ*}
+
 lemma LIMSEQ_NSLIMSEQ:
       "X ----> L ==> X ----NS> L"
 apply (simp add: LIMSEQ_def NSLIMSEQ_def, safe)
@@ -90,7 +197,6 @@
 apply (erule ultra, simp add: less_imp_le)
 done
 
-
 text{*NSLIMSEQ ==> LIMSEQ*}
 
 lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n
@@ -172,18 +278,7 @@
 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
 
-
-subsection{*Theorems About Sequences*}
-
-lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
-by (simp add: NSLIMSEQ_def)
-
-lemma LIMSEQ_const: "(%n. k) ----> k"
-by (simp add: LIMSEQ_def)
-
-lemma NSLIMSEQ_add:
-      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
-by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
+subsubsection {* Derived theorems about @{term LIMSEQ} *}
 
 lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
@@ -191,37 +286,17 @@
 lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
 by (simp add: LIMSEQ_add LIMSEQ_const)
 
-lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
-
-lemma NSLIMSEQ_mult:
-  fixes a b :: "'a::real_normed_algebra"
-  shows "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
-by (auto intro!: approx_mult_HFinite 
-        simp add: NSLIMSEQ_def starfun_mult [symmetric])
-
 lemma LIMSEQ_mult:
   fixes a b :: "'a::real_normed_algebra"
   shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
 
-lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
-by (auto simp add: NSLIMSEQ_def starfun_minus [symmetric])
-
 lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
 
 lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
 by (drule LIMSEQ_minus, simp)
 
-lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
-by (drule NSLIMSEQ_minus, simp)
-
-(* FIXME: delete *)
-lemma NSLIMSEQ_add_minus:
-     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
-by (simp add: NSLIMSEQ_add NSLIMSEQ_minus)
-
 (* FIXME: delete *)
 lemma LIMSEQ_add_minus:
      "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
@@ -230,67 +305,27 @@
 lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
 by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus)
 
-lemma NSLIMSEQ_diff:
-     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
-by (simp add: diff_minus NSLIMSEQ_add NSLIMSEQ_minus)
-
 lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
 by (simp add: LIMSEQ_diff LIMSEQ_const)
 
-lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
-by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
-
-text{*Proof is like that of @{text NSLIM_inverse}.*}
-lemma NSLIMSEQ_inverse:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
-by (simp add: NSLIMSEQ_def star_of_approx_inverse)
-
-
-text{*Standard version of theorem*}
 lemma LIMSEQ_inverse:
   fixes a :: "'a::real_normed_div_algebra"
   shows "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
 
-lemma NSLIMSEQ_mult_inverse:
-  fixes a b :: "'a::{real_normed_div_algebra,field}"
-  shows
-     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
-by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
-
 lemma LIMSEQ_divide:
-  fixes a b :: "'a::{real_normed_div_algebra,field}"
+  fixes a b :: "'a::real_normed_field"
   shows "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
 
-lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
-by transfer simp
-
-lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
-by transfer simp
-
-lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
-by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
-
-lemma LIMSEQ_norm: "X ----> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----> norm a"
-apply (simp add: LIMSEQ_def, safe)
-apply (drule_tac x="r" in spec, safe)
-apply (rule_tac x="no" in exI, safe)
-apply (drule_tac x="n" in spec, safe)
-apply (erule order_le_less_trans [OF norm_triangle_ineq3])
-done
-
-text{*Uniqueness of limit*}
-lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
-apply (simp add: NSLIMSEQ_def)
-apply (drule HNatInfinite_whn [THEN [2] bspec])+
-apply (auto dest: approx_trans3)
-done
-
 lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
 
+lemma LIMSEQ_pow:
+  fixes a :: "'a::{real_normed_algebra,recpower}"
+  shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
+
 lemma LIMSEQ_setsum:
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
   shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
@@ -334,29 +369,6 @@
     by (simp add: setprod_def LIMSEQ_const)
 qed
 
-lemma LIMSEQ_ignore_initial_segment: "f ----> a 
-  ==> (%n. f(n + k)) ----> a"
-  apply (unfold LIMSEQ_def) 
-  apply (clarify)
-  apply (drule_tac x = r in spec)
-  apply (clarify)
-  apply (rule_tac x = "no + k" in exI)
-  by auto
-
-lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
-    f ----> a"
-  apply (unfold LIMSEQ_def)
-  apply clarsimp
-  apply (drule_tac x = r in spec)
-  apply clarsimp
-  apply (rule_tac x = "no + k" in exI)
-  apply clarsimp
-  apply (drule_tac x = "n - k" in spec)
-  apply (frule mp)
-  apply arith
-  apply simp
-done
-
 lemma LIMSEQ_diff_approach_zero: 
   "g ----> L ==> (%x. f x - g x) ----> 0  ==>
      f ----> L"
@@ -374,7 +386,7 @@
 done
 
 
-subsection{*Nslim and Lim*}
+subsection {* Convergence *}
 
 lemma limI: "X ----> L ==> lim X = L"
 apply (simp add: lim_def)
@@ -389,9 +401,6 @@
 lemma lim_nslim_iff: "lim X = nslim X"
 by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
 
-
-subsection{*Convergence*}
-
 lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
 by (simp add: convergent_def)
 
@@ -413,6 +422,15 @@
 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
 by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
 
+lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
+apply (simp add: convergent_def)
+apply (auto dest: LIMSEQ_minus)
+apply (drule LIMSEQ_minus, auto)
+done
+
+
+subsection {* Bounded Monotonic Sequences *}
+
 text{*Subsequence (alternative definition, (e.g. Hoskins)*}
 
 lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
@@ -422,9 +440,6 @@
 apply (auto intro: less_trans)
 done
 
-
-subsection{*Monotonicity*}
-
 lemma monoseq_Suc:
    "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
                  | (\<forall>n. X (Suc n) \<le> X n))"
@@ -450,8 +465,7 @@
 lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
 by (simp add: monoseq_Suc)
 
-
-subsection{*Bounded Sequence*}
+text{*Bounded Sequence*}
 
 lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
 by (simp add: Bseq_def)
@@ -603,8 +617,7 @@
 lemma convergent_Bseq: "convergent X ==> Bseq X"
 by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
 
-
-subsection{*Upper Bounds and Lubs of Bounded Sequences*}
+subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
 
 lemma Bseq_isUb:
   "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
@@ -626,7 +639,7 @@
 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
 
 
-subsection{*A Bounded and Monotonic Sequence Converges*}
+subsubsection{*A Bounded and Monotonic Sequence Converges*}
 
 lemma lemma_converg1:
      "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
@@ -705,12 +718,6 @@
          simp add: convergent_NSconvergent_iff [symmetric] 
                    Bseq_NSBseq_iff [symmetric])
 
-lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
-apply (simp add: convergent_def)
-apply (auto dest: LIMSEQ_minus)
-apply (drule LIMSEQ_minus, auto)
-done
-
 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
 by (simp add: Bseq_def)
 
@@ -722,8 +729,7 @@
 apply (auto intro!: Bseq_mono_convergent)
 done
 
-
-subsection{*A Few More Equivalence Theorems for Boundedness*}
+subsubsection{*A Few More Equivalence Theorems for Boundedness*}
 
 text{*alternative formulation for boundedness*}
 lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
@@ -757,9 +763,11 @@
 done
 
 
-subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
+subsection {* Cauchy Sequences *}
 
-subsubsection{*Standard Implies Nonstandard*}
+subsubsection{*Equivalence Between NS and Standard*}
+
+text{*Standard Implies Nonstandard*}
 
 lemma lemmaCauchy1:
      "star_n x : HNatInfinite
@@ -789,7 +797,7 @@
 apply (auto intro: FreeUltrafilterNat_Int)
 done
 
-subsubsection{*Nonstandard Implies Standard*}
+text{*Nonstandard Implies Standard*}
 
 lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
 apply (auto simp add: Cauchy_def NSCauchy_def)
@@ -808,6 +816,8 @@
 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
 by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
 
+subsubsection {* Cauchy Sequences are Bounded *}
+
 text{*A Cauchy sequence is bounded -- this is the standard
   proof mechanization rather than the nonstandard proof*}
 
@@ -900,6 +910,7 @@
 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
 by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
 
+subsubsection {* Cauchy Sequences are Convergent *}
 
 text{*Equivalence of Cauchy criterion and convergence:
   We will prove this using our NS formulation which provides a
@@ -936,6 +947,8 @@
 by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
 
 
+subsection {* More Properties of Sequences *}
+
 text{*We can now try and derive a few properties of sequences,
      starting with the limit comparison property for sequences.*}
 
@@ -1097,19 +1110,7 @@
 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
 
 
-text{* Real Powers*}
-
-lemma NSLIMSEQ_pow [rule_format]:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
-  shows "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
-apply (induct "m")
-apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
-done
-
-lemma LIMSEQ_pow:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
-  shows "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
-by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
+subsection {* Power Sequences *}
 
 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
 "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and