src/HOL/Nonstandard_Analysis/HSEQ.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (19 months ago)
changeset 67006 b1278ed3cd46
parent 66453 cc19f7ca2ed6
child 67443 3abf6a722518
permissions -rw-r--r--
prefer main entry points of HOL;
     1 (*  Title:      HOL/Nonstandard_Analysis/HSEQ.thy
     2     Author:     Jacques D. Fleuriot
     3     Copyright:  1998  University of Cambridge
     4 
     5 Convergence of sequences and series.
     6 
     7 Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     8 Additional contributions by Jeremy Avigad and Brian Huffman.
     9 *)
    10 
    11 section \<open>Sequences and Convergence (Nonstandard)\<close>
    12 
    13 theory HSEQ
    14   imports Complex_Main NatStar
    15   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
    16 begin
    17 
    18 definition NSLIMSEQ :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
    19     ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
    20     \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
    21   "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    22 
    23 definition nslim :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
    24   where "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    25   \<comment> \<open>Nonstandard definition of limit using choice operator\<close>
    26 
    27 
    28 definition NSconvergent :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    29   where "NSconvergent X \<longleftrightarrow> (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
    30   \<comment> \<open>Nonstandard definition of convergence\<close>
    31 
    32 definition NSBseq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    33   where "NSBseq X \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite)"
    34   \<comment> \<open>Nonstandard definition for bounded sequence\<close>
    35 
    36 
    37 definition NSCauchy :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
    38   where "NSCauchy X \<longleftrightarrow> (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
    39   \<comment> \<open>Nonstandard definition\<close>
    40 
    41 
    42 subsection \<open>Limits of Sequences\<close>
    43 
    44 lemma NSLIMSEQ_iff: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) \<longleftrightarrow> (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
    45   by (simp add: NSLIMSEQ_def)
    46 
    47 lemma NSLIMSEQ_I: "(\<And>N. N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L) \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
    48   by (simp add: NSLIMSEQ_def)
    49 
    50 lemma NSLIMSEQ_D: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X N \<approx> star_of L"
    51   by (simp add: NSLIMSEQ_def)
    52 
    53 lemma NSLIMSEQ_const: "(\<lambda>n. k) \<longlonglongrightarrow>\<^sub>N\<^sub>S k"
    54   by (simp add: NSLIMSEQ_def)
    55 
    56 lemma NSLIMSEQ_add: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    57   by (auto intro: approx_add simp add: NSLIMSEQ_def)
    58 
    59 lemma NSLIMSEQ_add_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n + b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + b"
    60   by (simp only: NSLIMSEQ_add NSLIMSEQ_const)
    61 
    62 lemma NSLIMSEQ_mult: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n * Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a * b"
    63   for a b :: "'a::real_normed_algebra"
    64   by (auto intro!: approx_mult_HFinite simp add: NSLIMSEQ_def)
    65 
    66 lemma NSLIMSEQ_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S - a"
    67   by (auto simp add: NSLIMSEQ_def)
    68 
    69 lemma NSLIMSEQ_minus_cancel: "(\<lambda>n. - X n) \<longlonglongrightarrow>\<^sub>N\<^sub>S -a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S a"
    70   by (drule NSLIMSEQ_minus) simp
    71 
    72 lemma NSLIMSEQ_diff: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
    73   using NSLIMSEQ_add [of X a "- Y" "- b"] by (simp add: NSLIMSEQ_minus fun_Compl_def)
    74 
    75 (* FIXME: delete *)
    76 lemma NSLIMSEQ_add_minus: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> (\<lambda>n. X n + - Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a + - b"
    77   by (simp add: NSLIMSEQ_diff)
    78 
    79 lemma NSLIMSEQ_diff_const: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. f n - b) \<longlonglongrightarrow>\<^sub>N\<^sub>S a - b"
    80   by (simp add: NSLIMSEQ_diff NSLIMSEQ_const)
    81 
    82 lemma NSLIMSEQ_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S inverse a"
    83   for a :: "'a::real_normed_div_algebra"
    84   by (simp add: NSLIMSEQ_def star_of_approx_inverse)
    85 
    86 lemma NSLIMSEQ_mult_inverse: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> Y \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> (\<lambda>n. X n / Y n) \<longlonglongrightarrow>\<^sub>N\<^sub>S a / b"
    87   for a b :: "'a::real_normed_field"
    88   by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
    89 
    90 lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
    91   by transfer simp
    92 
    93 lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
    94   by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
    95 
    96 text \<open>Uniqueness of limit.\<close>
    97 lemma NSLIMSEQ_unique: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S b \<Longrightarrow> a = b"
    98   apply (simp add: NSLIMSEQ_def)
    99   apply (drule HNatInfinite_whn [THEN [2] bspec])+
   100   apply (auto dest: approx_trans3)
   101   done
   102 
   103 lemma NSLIMSEQ_pow [rule_format]: "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S a) \<longrightarrow> ((\<lambda>n. (X n) ^ m) \<longlonglongrightarrow>\<^sub>N\<^sub>S a ^ m)"
   104   for a :: "'a::{real_normed_algebra,power}"
   105   by (induct m) (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
   106 
   107 text \<open>We can now try and derive a few properties of sequences,
   108   starting with the limit comparison property for sequences.\<close>
   109 
   110 lemma NSLIMSEQ_le: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> g \<longlonglongrightarrow>\<^sub>N\<^sub>S m \<Longrightarrow> \<exists>N. \<forall>n \<ge> N. f n \<le> g n \<Longrightarrow> l \<le> m"
   111   for l m :: real
   112   apply (simp add: NSLIMSEQ_def, safe)
   113   apply (drule starfun_le_mono)
   114   apply (drule HNatInfinite_whn [THEN [2] bspec])+
   115   apply (drule_tac x = whn in spec)
   116   apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   117   apply clarify
   118   apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   119   done
   120 
   121 lemma NSLIMSEQ_le_const: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. a \<le> X n \<Longrightarrow> a \<le> r"
   122   for a r :: real
   123   by (erule NSLIMSEQ_le [OF NSLIMSEQ_const]) auto
   124 
   125 lemma NSLIMSEQ_le_const2: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S r \<Longrightarrow> \<forall>n. X n \<le> a \<Longrightarrow> r \<le> a"
   126   for a r :: real
   127   by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const]) auto
   128 
   129 text \<open>Shift a convergent series by 1:
   130   By the equivalence between Cauchiness and convergence and because
   131   the successor of an infinite hypernatural is also infinite.\<close>
   132 
   133 lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   134   apply (unfold NSLIMSEQ_def)
   135   apply safe
   136   apply (drule_tac x="N + 1" in bspec)
   137    apply (erule HNatInfinite_add)
   138   apply (simp add: starfun_shift_one)
   139   done
   140 
   141 lemma NSLIMSEQ_imp_Suc: "(\<lambda>n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   142   apply (unfold NSLIMSEQ_def)
   143   apply safe
   144   apply (drule_tac x="N - 1" in bspec)
   145    apply (erule Nats_1 [THEN [2] HNatInfinite_diff])
   146   apply (simp add: starfun_shift_one one_le_HNatInfinite)
   147   done
   148 
   149 lemma NSLIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   150   by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   151 
   152 
   153 subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
   154 
   155 lemma LIMSEQ_NSLIMSEQ:
   156   assumes X: "X \<longlonglongrightarrow> L"
   157   shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   158 proof (rule NSLIMSEQ_I)
   159   fix N
   160   assume N: "N \<in> HNatInfinite"
   161   have "starfun X N - star_of L \<in> Infinitesimal"
   162   proof (rule InfinitesimalI2)
   163     fix r :: real
   164     assume r: "0 < r"
   165     from LIMSEQ_D [OF X r] obtain no where "\<forall>n\<ge>no. norm (X n - L) < r" ..
   166     then have "\<forall>n\<ge>star_of no. hnorm (starfun X n - star_of L) < star_of r"
   167       by transfer
   168     then show "hnorm (starfun X N - star_of L) < star_of r"
   169       using N by (simp add: star_of_le_HNatInfinite)
   170   qed
   171   then show "starfun X N \<approx> star_of L"
   172     by (simp only: approx_def)
   173 qed
   174 
   175 lemma NSLIMSEQ_LIMSEQ:
   176   assumes X: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   177   shows "X \<longlonglongrightarrow> L"
   178 proof (rule LIMSEQ_I)
   179   fix r :: real
   180   assume r: "0 < r"
   181   have "\<exists>no. \<forall>n\<ge>no. hnorm (starfun X n - star_of L) < star_of r"
   182   proof (intro exI allI impI)
   183     fix n
   184     assume "whn \<le> n"
   185     with HNatInfinite_whn have "n \<in> HNatInfinite"
   186       by (rule HNatInfinite_upward_closed)
   187     with X have "starfun X n \<approx> star_of L"
   188       by (rule NSLIMSEQ_D)
   189     then have "starfun X n - star_of L \<in> Infinitesimal"
   190       by (simp only: approx_def)
   191     then show "hnorm (starfun X n - star_of L) < star_of r"
   192       using r by (rule InfinitesimalD2)
   193   qed
   194   then show "\<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
   195     by transfer
   196 qed
   197 
   198 theorem LIMSEQ_NSLIMSEQ_iff: "f \<longlonglongrightarrow> L \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   199   by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   200 
   201 
   202 subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
   203 
   204 text \<open>We prove the NS version from the standard one, since the NS proof
   205   seems more complicated than the standard one above!\<close>
   206 lemma NSLIMSEQ_norm_zero: "(\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   207   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
   208 
   209 lemma NSLIMSEQ_rabs_zero: "(\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0 \<longleftrightarrow> f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real)"
   210   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
   211 
   212 text \<open>Generalization to other limits.\<close>
   213 lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l \<Longrightarrow> (\<lambda>n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
   214   for l :: real
   215   by (simp add: NSLIMSEQ_def) (auto intro: approx_hrabs simp add: starfun_abs)
   216 
   217 lemma NSLIMSEQ_inverse_zero: "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f n \<Longrightarrow> (\<lambda>n. inverse (f n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   218   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   219 
   220 lemma NSLIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   221   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: of_nat_Suc)
   222 
   223 lemma NSLIMSEQ_inverse_real_of_nat_add: "(\<lambda>n. r + inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   224   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: of_nat_Suc)
   225 
   226 lemma NSLIMSEQ_inverse_real_of_nat_add_minus: "(\<lambda>n. r + - inverse (real (Suc n))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   227   using LIMSEQ_inverse_real_of_nat_add_minus by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   228 
   229 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
   230   "(\<lambda>n. r * (1 + - inverse (real (Suc n)))) \<longlonglongrightarrow>\<^sub>N\<^sub>S r"
   231   using LIMSEQ_inverse_real_of_nat_add_minus_mult
   232   by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
   233 
   234 
   235 subsection \<open>Convergence\<close>
   236 
   237 lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> nslim X = L"
   238   by (simp add: nslim_def) (blast intro: NSLIMSEQ_unique)
   239 
   240 lemma lim_nslim_iff: "lim X = nslim X"
   241   by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
   242 
   243 lemma NSconvergentD: "NSconvergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   244   by (simp add: NSconvergent_def)
   245 
   246 lemma NSconvergentI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> NSconvergent X"
   247   by (auto simp add: NSconvergent_def)
   248 
   249 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
   250   by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
   251 
   252 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X \<longleftrightarrow> X \<longlonglongrightarrow>\<^sub>N\<^sub>S nslim X"
   253   by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
   254 
   255 
   256 subsection \<open>Bounded Monotonic Sequences\<close>
   257 
   258 lemma NSBseqD: "NSBseq X \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> ( *f* X) N \<in> HFinite"
   259   by (simp add: NSBseq_def)
   260 
   261 lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
   262   by (auto simp: Standard_def)
   263 
   264 lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
   265   apply (cases "N \<in> HNatInfinite")
   266    apply (erule (1) NSBseqD)
   267   apply (rule subsetD [OF Standard_subset_HFinite])
   268   apply (simp add: HNatInfinite_def Nats_eq_Standard)
   269   done
   270 
   271 lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N \<in> HFinite \<Longrightarrow> NSBseq X"
   272   by (simp add: NSBseq_def)
   273 
   274 text \<open>The standard definition implies the nonstandard definition.\<close>
   275 lemma Bseq_NSBseq: "Bseq X \<Longrightarrow> NSBseq X"
   276   unfolding NSBseq_def
   277 proof safe
   278   assume X: "Bseq X"
   279   fix N
   280   assume N: "N \<in> HNatInfinite"
   281   from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K"
   282     by fast
   283   then have "\<forall>N. hnorm (starfun X N) \<le> star_of K"
   284     by transfer
   285   then have "hnorm (starfun X N) \<le> star_of K"
   286     by simp
   287   also have "star_of K < star_of (K + 1)"
   288     by simp
   289   finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x"
   290     by (rule bexI) simp
   291   then show "starfun X N \<in> HFinite"
   292     by (simp add: HFinite_def)
   293 qed
   294 
   295 text \<open>The nonstandard definition implies the standard definition.\<close>
   296 lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
   297   using HInfinite_omega
   298   by (simp add: HInfinite_def) (simp add: order_less_imp_le)
   299 
   300 lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
   301 proof (rule ccontr)
   302   let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
   303   assume "NSBseq X"
   304   then have finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
   305     by (rule NSBseqD2)
   306   assume "\<not> Bseq X"
   307   then have "\<forall>K>0. \<exists>n. K < norm (X n)"
   308     by (simp add: Bseq_def linorder_not_le)
   309   then have "\<forall>K>0. K < norm (X (?n K))"
   310     by (auto intro: LeastI_ex)
   311   then have "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
   312     by transfer
   313   then have "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   314     by simp
   315   then have "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
   316     by (simp add: order_less_trans [OF SReal_less_omega])
   317   then have "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
   318     by (simp add: HInfinite_def)
   319   with finite show "False"
   320     by (simp add: HFinite_HInfinite_iff)
   321 qed
   322 
   323 text \<open>Equivalence of nonstandard and standard definitions for a bounded sequence.\<close>
   324 lemma Bseq_NSBseq_iff: "Bseq X = NSBseq X"
   325   by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
   326 
   327 text \<open>A convergent sequence is bounded:
   328   Boundedness as a necessary condition for convergence.
   329   The nonstandard version has no existential, as usual.\<close>
   330 lemma NSconvergent_NSBseq: "NSconvergent X \<Longrightarrow> NSBseq X"
   331   by (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
   332     (blast intro: HFinite_star_of approx_sym approx_HFinite)
   333 
   334 text \<open>Standard Version: easily now proved using equivalence of NS and
   335  standard definitions.\<close>
   336 
   337 lemma convergent_Bseq: "convergent X \<Longrightarrow> Bseq X"
   338   for X :: "nat \<Rightarrow> 'b::real_normed_vector"
   339   by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
   340 
   341 
   342 subsubsection \<open>Upper Bounds and Lubs of Bounded Sequences\<close>
   343 
   344 lemma NSBseq_isUb: "NSBseq X \<Longrightarrow> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
   345   by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
   346 
   347 lemma NSBseq_isLub: "NSBseq X \<Longrightarrow> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
   348   by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
   349 
   350 
   351 subsubsection \<open>A Bounded and Monotonic Sequence Converges\<close>
   352 
   353 text \<open>The best of both worlds: Easier to prove this result as a standard
   354    theorem and then use equivalence to "transfer" it into the
   355    equivalent nonstandard form if needed!\<close>
   356 
   357 lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   358   by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
   359 
   360 lemma NSBseq_mono_NSconvergent: "NSBseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> NSconvergent X"
   361   for X :: "nat \<Rightarrow> real"
   362   by (auto intro: Bseq_mono_convergent
   363       simp: convergent_NSconvergent_iff [symmetric] Bseq_NSBseq_iff [symmetric])
   364 
   365 
   366 subsection \<open>Cauchy Sequences\<close>
   367 
   368 lemma NSCauchyI:
   369   "(\<And>M N. M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N) \<Longrightarrow> NSCauchy X"
   370   by (simp add: NSCauchy_def)
   371 
   372 lemma NSCauchyD:
   373   "NSCauchy X \<Longrightarrow> M \<in> HNatInfinite \<Longrightarrow> N \<in> HNatInfinite \<Longrightarrow> starfun X M \<approx> starfun X N"
   374   by (simp add: NSCauchy_def)
   375 
   376 
   377 subsubsection \<open>Equivalence Between NS and Standard\<close>
   378 
   379 lemma Cauchy_NSCauchy:
   380   assumes X: "Cauchy X"
   381   shows "NSCauchy X"
   382 proof (rule NSCauchyI)
   383   fix M
   384   assume M: "M \<in> HNatInfinite"
   385   fix N
   386   assume N: "N \<in> HNatInfinite"
   387   have "starfun X M - starfun X N \<in> Infinitesimal"
   388   proof (rule InfinitesimalI2)
   389     fix r :: real
   390     assume r: "0 < r"
   391     from CauchyD [OF X r] obtain k where "\<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r" ..
   392     then have "\<forall>m\<ge>star_of k. \<forall>n\<ge>star_of k. hnorm (starfun X m - starfun X n) < star_of r"
   393       by transfer
   394     then show "hnorm (starfun X M - starfun X N) < star_of r"
   395       using M N by (simp add: star_of_le_HNatInfinite)
   396   qed
   397   then show "starfun X M \<approx> starfun X N"
   398     by (simp only: approx_def)
   399 qed
   400 
   401 lemma NSCauchy_Cauchy:
   402   assumes X: "NSCauchy X"
   403   shows "Cauchy X"
   404 proof (rule CauchyI)
   405   fix r :: real
   406   assume r: "0 < r"
   407   have "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. hnorm (starfun X m - starfun X n) < star_of r"
   408   proof (intro exI allI impI)
   409     fix M
   410     assume "whn \<le> M"
   411     with HNatInfinite_whn have M: "M \<in> HNatInfinite"
   412       by (rule HNatInfinite_upward_closed)
   413     fix N
   414     assume "whn \<le> N"
   415     with HNatInfinite_whn have N: "N \<in> HNatInfinite"
   416       by (rule HNatInfinite_upward_closed)
   417     from X M N have "starfun X M \<approx> starfun X N"
   418       by (rule NSCauchyD)
   419     then have "starfun X M - starfun X N \<in> Infinitesimal"
   420       by (simp only: approx_def)
   421     then show "hnorm (starfun X M - starfun X N) < star_of r"
   422       using r by (rule InfinitesimalD2)
   423   qed
   424   then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. norm (X m - X n) < r"
   425     by transfer
   426 qed
   427 
   428 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
   429   by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
   430 
   431 
   432 subsubsection \<open>Cauchy Sequences are Bounded\<close>
   433 
   434 text \<open>A Cauchy sequence is bounded -- nonstandard version.\<close>
   435 
   436 lemma NSCauchy_NSBseq: "NSCauchy X \<Longrightarrow> NSBseq X"
   437   by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
   438 
   439 
   440 subsubsection \<open>Cauchy Sequences are Convergent\<close>
   441 
   442 text \<open>Equivalence of Cauchy criterion and convergence:
   443   We will prove this using our NS formulation which provides a
   444   much easier proof than using the standard definition. We do not
   445   need to use properties of subsequences such as boundedness,
   446   monotonicity etc... Compare with Harrison's corresponding proof
   447   in HOL which is much longer and more complicated. Of course, we do
   448   not have problems which he encountered with guessing the right
   449   instantiations for his 'espsilon-delta' proof(s) in this case
   450   since the NS formulations do not involve existential quantifiers.\<close>
   451 
   452 lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
   453   by (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def) (auto intro: approx_trans2)
   454 
   455 lemma real_NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
   456   for X :: "nat \<Rightarrow> real"
   457   apply (simp add: NSconvergent_def NSLIMSEQ_def)
   458   apply (frule NSCauchy_NSBseq)
   459   apply (simp add: NSBseq_def NSCauchy_def)
   460   apply (drule HNatInfinite_whn [THEN [2] bspec])
   461   apply (drule HNatInfinite_whn [THEN [2] bspec])
   462   apply (auto dest!: st_part_Ex simp add: SReal_iff)
   463   apply (blast intro: approx_trans3)
   464   done
   465 
   466 lemma NSCauchy_NSconvergent: "NSCauchy X \<Longrightarrow> NSconvergent X"
   467   for X :: "nat \<Rightarrow> 'a::banach"
   468   apply (drule NSCauchy_Cauchy [THEN Cauchy_convergent])
   469   apply (erule convergent_NSconvergent_iff [THEN iffD1])
   470   done
   471 
   472 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
   473   for X :: "nat \<Rightarrow> 'a::banach"
   474   by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
   475 
   476 
   477 subsection \<open>Power Sequences\<close>
   478 
   479 text \<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
   480   "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
   481   also fact that bounded and monotonic sequence converges.\<close>
   482 
   483 text \<open>We now use NS criterion to bring proof of theorem through.\<close>
   484 lemma NSLIMSEQ_realpow_zero: "0 \<le> x \<Longrightarrow> x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   485   for x :: real
   486   apply (simp add: NSLIMSEQ_def)
   487   apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
   488   apply (frule NSconvergentD)
   489   apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
   490   apply (frule HNatInfinite_add_one)
   491   apply (drule bspec, assumption)
   492   apply (drule bspec, assumption)
   493   apply (drule_tac x = "N + 1" in bspec, assumption)
   494   apply (simp add: hyperpow_add)
   495   apply (drule approx_mult_subst_star_of, assumption)
   496   apply (drule approx_trans3, assumption)
   497   apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
   498   done
   499 
   500 lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   501   for c :: real
   502   by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
   503 
   504 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   505   for c :: real
   506   by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
   507 
   508 (***---------------------------------------------------------------
   509     Theorems proved by Harrison in HOL that we do not need
   510     in order to prove equivalence between Cauchy criterion
   511     and convergence:
   512  -- Show that every sequence contains a monotonic subsequence
   513 Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
   514  -- Show that a subsequence of a bounded sequence is bounded
   515 Goal "Bseq X ==> Bseq (%n. X (f n))";
   516  -- Show we can take subsequential terms arbitrarily far
   517     up a sequence
   518 Goal "subseq f ==> n \<le> f(n)";
   519 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
   520  ---------------------------------------------------------------***)
   521 
   522 end