src/HOL/Hyperreal/SEQ.thy
 author huffman Thu Sep 15 23:46:22 2005 +0200 (2005-09-15) changeset 17429 e8d6ed3aacfe parent 17318 bc1c75855f3d child 17439 a358da1a0218 permissions -rw-r--r--
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
```     1 (*  Title       : SEQ.thy
```
```     2     Author      : Jacques D. Fleuriot
```
```     3     Copyright   : 1998  University of Cambridge
```
```     4     Description : Convergence of sequences and series
```
```     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
```
```     6     Additional contributions by Jeremy Avigad
```
```     7 *)
```
```     8
```
```     9 theory SEQ
```
```    10 imports NatStar
```
```    11 begin
```
```    12
```
```    13 constdefs
```
```    14
```
```    15   LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
```
```    16     --{*Standard definition of convergence of sequence*}
```
```    17   "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
```
```    18
```
```    19   NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
```
```    20     --{*Nonstandard definition of convergence of sequence*}
```
```    21   "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
```
```    22
```
```    23   lim :: "(nat => real) => real"
```
```    24     --{*Standard definition of limit using choice operator*}
```
```    25   "lim X == (@L. (X ----> L))"
```
```    26
```
```    27   nslim :: "(nat => real) => real"
```
```    28     --{*Nonstandard definition of limit using choice operator*}
```
```    29   "nslim X == (@L. (X ----NS> L))"
```
```    30
```
```    31   convergent :: "(nat => real) => bool"
```
```    32     --{*Standard definition of convergence*}
```
```    33   "convergent X == (\<exists>L. (X ----> L))"
```
```    34
```
```    35   NSconvergent :: "(nat => real) => bool"
```
```    36     --{*Nonstandard definition of convergence*}
```
```    37   "NSconvergent X == (\<exists>L. (X ----NS> L))"
```
```    38
```
```    39   Bseq :: "(nat => real) => bool"
```
```    40     --{*Standard definition for bounded sequence*}
```
```    41   "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K"
```
```    42
```
```    43   NSBseq :: "(nat=>real) => bool"
```
```    44     --{*Nonstandard definition for bounded sequence*}
```
```    45   "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
```
```    46
```
```    47   monoseq :: "(nat=>real)=>bool"
```
```    48     --{*Definition for monotonicity*}
```
```    49   "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
```
```    50
```
```    51   subseq :: "(nat => nat) => bool"
```
```    52     --{*Definition of subsequence*}
```
```    53   "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)"
```
```    54
```
```    55   Cauchy :: "(nat => real) => bool"
```
```    56     --{*Standard definition of the Cauchy condition*}
```
```    57   "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e"
```
```    58
```
```    59   NSCauchy :: "(nat => real) => bool"
```
```    60     --{*Nonstandard definition*}
```
```    61   "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
```
```    62                       ( *f* X) M \<approx> ( *f* X) N)"
```
```    63
```
```    64
```
```    65
```
```    66 text{* Example of an hypersequence (i.e. an extended standard sequence)
```
```    67    whose term with an hypernatural suffix is an infinitesimal i.e.
```
```    68    the whn'nth term of the hypersequence is a member of Infinitesimal*}
```
```    69
```
```    70 lemma SEQ_Infinitesimal:
```
```    71       "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
```
```    72 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
```
```    73 apply (simp add: star_n_inverse)
```
```    74 apply (rule bexI [OF _ Rep_star_star_n])
```
```    75 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
```
```    76 done
```
```    77
```
```    78
```
```    79 subsection{*LIMSEQ and NSLIMSEQ*}
```
```    80
```
```    81 lemma LIMSEQ_iff:
```
```    82       "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. \<bar>X n + -L\<bar> < r)"
```
```    83 by (simp add: LIMSEQ_def)
```
```    84
```
```    85 lemma NSLIMSEQ_iff:
```
```    86     "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
```
```    87 by (simp add: NSLIMSEQ_def)
```
```    88
```
```    89
```
```    90 text{*LIMSEQ ==> NSLIMSEQ*}
```
```    91
```
```    92 lemma LIMSEQ_NSLIMSEQ:
```
```    93       "X ----> L ==> X ----NS> L"
```
```    94 apply (simp add: LIMSEQ_def NSLIMSEQ_def)
```
```    95 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
```
```    96 apply (rule_tac x = N in star_cases)
```
```    97 apply (rule approx_minus_iff [THEN iffD2])
```
```    98 apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
```
```    99               star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
```
```   100 apply (rule bexI [OF _ Rep_star_star_n], safe)
```
```   101 apply (drule_tac x = u in spec, safe)
```
```   102 apply (drule_tac x = no in spec, fuf)
```
```   103 apply (blast dest: less_imp_le)
```
```   104 done
```
```   105
```
```   106
```
```   107 text{*NSLIMSEQ ==> LIMSEQ*}
```
```   108
```
```   109 lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n
```
```   110            ==> {n. f n = 0} = {0} | {n. f n = 0} = {}"
```
```   111 apply auto
```
```   112 apply (drule_tac x = xa in spec)
```
```   113 apply (drule_tac [2] x = x in spec, auto)
```
```   114 done
```
```   115
```
```   116 lemma lemma_NSLIMSEQ2: "{n. f n \<le> Suc u} = {n. f n \<le> u} Un {n. f n = Suc u}"
```
```   117 by (auto simp add: le_Suc_eq)
```
```   118
```
```   119 lemma lemma_NSLIMSEQ3:
```
```   120      "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. f n = Suc u} \<le> {n. n \<le> Suc u}"
```
```   121 apply auto
```
```   122 apply (drule_tac x = x in spec, auto)
```
```   123 done
```
```   124
```
```   125 text{* the following sequence @{term "f(n)"} defines a hypernatural *}
```
```   126 lemma NSLIMSEQ_finite_set:
```
```   127      "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
```
```   128 apply (induct u)
```
```   129 apply (auto simp add: lemma_NSLIMSEQ2)
```
```   130 apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def])
```
```   131 apply (drule lemma_NSLIMSEQ1, safe)
```
```   132 apply (simp_all (no_asm_simp))
```
```   133 done
```
```   134
```
```   135 lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n \<le> u}"
```
```   136 by (auto dest: less_le_trans simp add: le_def)
```
```   137
```
```   138 text{* the index set is in the free ultrafilter *}
```
```   139 lemma FreeUltrafilterNat_NSLIMSEQ:
```
```   140      "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. u < f n} : FreeUltrafilterNat"
```
```   141 apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2])
```
```   142 apply (rule FreeUltrafilterNat_finite)
```
```   143 apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set)
```
```   144 done
```
```   145
```
```   146 text{* thus, the sequence defines an infinite hypernatural! *}
```
```   147 lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
```
```   148           ==> star_n f : HNatInfinite"
```
```   149 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
```
```   150 apply (rule bexI [OF _ Rep_star_star_n], safe)
```
```   151 apply (erule FreeUltrafilterNat_NSLIMSEQ)
```
```   152 done
```
```   153
```
```   154 lemma lemmaLIM:
```
```   155      "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
```
```   156       {n. \<bar>X (f n) + - L\<bar> < r}"
```
```   157 by auto
```
```   158
```
```   159 lemma lemmaLIM2:
```
```   160   "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
```
```   161 by auto
```
```   162
```
```   163 lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
```
```   164            ( *f* X) (star_n f) +
```
```   165            - hypreal_of_real  L \<approx> 0 |] ==> False"
```
```   166 apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
```
```   167 apply (rename_tac "Y")
```
```   168 apply (drule_tac x = r in spec, safe)
```
```   169 apply (drule FreeUltrafilterNat_Int, assumption)
```
```   170 apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
```
```   171 apply (drule FreeUltrafilterNat_all)
```
```   172 apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
```
```   173 apply (drule FreeUltrafilterNat_Int, assumption)
```
```   174 apply (simp add: lemmaLIM2)
```
```   175 done
```
```   176
```
```   177 lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
```
```   178 apply (simp add: LIMSEQ_def NSLIMSEQ_def)
```
```   179 apply (rule ccontr, simp, safe)
```
```   180 txt{* skolemization step *}
```
```   181 apply (drule choice, safe)
```
```   182 apply (drule_tac x = "star_n f" in bspec)
```
```   183 apply (drule_tac [2] approx_minus_iff [THEN iffD1])
```
```   184 apply (simp_all add: linorder_not_less)
```
```   185 apply (blast intro: HNatInfinite_NSLIMSEQ)
```
```   186 apply (blast intro: lemmaLIM3)
```
```   187 done
```
```   188
```
```   189 text{* Now, the all-important result is trivially proved! *}
```
```   190 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
```
```   191 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
```
```   192
```
```   193
```
```   194 subsection{*Theorems About Sequences*}
```
```   195
```
```   196 lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
```
```   197 by (simp add: NSLIMSEQ_def)
```
```   198
```
```   199 lemma LIMSEQ_const: "(%n. k) ----> k"
```
```   200 by (simp add: LIMSEQ_def)
```
```   201
```
```   202 lemma NSLIMSEQ_add:
```
```   203       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
```
```   204 by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])
```
```   205
```
```   206 lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
```
```   207 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
```
```   208
```
```   209 lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
```
```   210   apply (subgoal_tac "%n. (f n + b) == %n. (f n + (%n. b) n)")
```
```   211   apply (subgoal_tac "(%n. b) ----> b")
```
```   212   apply (auto simp add: LIMSEQ_add LIMSEQ_const)
```
```   213 done
```
```   214
```
```   215 lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
```
```   216 by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)
```
```   217
```
```   218 lemma NSLIMSEQ_mult:
```
```   219       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
```
```   220 by (auto intro!: approx_mult_HFinite
```
```   221         simp add: NSLIMSEQ_def starfun_mult [symmetric])
```
```   222
```
```   223 lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
```
```   224 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
```
```   225
```
```   226 lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
```
```   227 by (auto simp add: NSLIMSEQ_def starfun_minus [symmetric])
```
```   228
```
```   229 lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
```
```   230 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
```
```   231
```
```   232 lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
```
```   233 by (drule LIMSEQ_minus, simp)
```
```   234
```
```   235 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
```
```   236 by (drule NSLIMSEQ_minus, simp)
```
```   237
```
```   238 lemma NSLIMSEQ_add_minus:
```
```   239      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
```
```   240 by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y])
```
```   241
```
```   242 lemma LIMSEQ_add_minus:
```
```   243      "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
```
```   244 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)
```
```   245
```
```   246 lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
```
```   247 apply (simp add: diff_minus)
```
```   248 apply (blast intro: LIMSEQ_add_minus)
```
```   249 done
```
```   250
```
```   251 lemma NSLIMSEQ_diff:
```
```   252      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
```
```   253 apply (simp add: diff_minus)
```
```   254 apply (blast intro: NSLIMSEQ_add_minus)
```
```   255 done
```
```   256
```
```   257 lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
```
```   258   apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
```
```   259   apply (subgoal_tac "(%n. b) ----> b")
```
```   260   apply (auto simp add: LIMSEQ_diff LIMSEQ_const)
```
```   261 done
```
```   262
```
```   263 lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
```
```   264 by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_diff_const)
```
```   265
```
```   266 text{*Proof is like that of @{text NSLIM_inverse}.*}
```
```   267 lemma NSLIMSEQ_inverse:
```
```   268      "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
```
```   269 by (simp add: NSLIMSEQ_def starfun_inverse [symmetric]
```
```   270               hypreal_of_real_approx_inverse)
```
```   271
```
```   272
```
```   273 text{*Standard version of theorem*}
```
```   274 lemma LIMSEQ_inverse:
```
```   275      "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
```
```   276 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
```
```   277
```
```   278 lemma NSLIMSEQ_mult_inverse:
```
```   279      "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
```
```   280 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
```
```   281
```
```   282 lemma LIMSEQ_divide:
```
```   283      "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
```
```   284 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
```
```   285
```
```   286 text{*Uniqueness of limit*}
```
```   287 lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
```
```   288 apply (simp add: NSLIMSEQ_def)
```
```   289 apply (drule HNatInfinite_whn [THEN [2] bspec])+
```
```   290 apply (auto dest: approx_trans3)
```
```   291 done
```
```   292
```
```   293 lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
```
```   294 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
```
```   295
```
```   296 lemma LIMSEQ_setsum:
```
```   297   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
```
```   298   shows "(\<lambda>m. \<Sum>n\<in>S. X n m) ----> (\<Sum>n\<in>S. L n)"
```
```   299 proof (cases "finite S")
```
```   300   case True
```
```   301   thus ?thesis using n
```
```   302   proof (induct)
```
```   303     case empty
```
```   304     show ?case
```
```   305       by (simp add: LIMSEQ_const)
```
```   306   next
```
```   307     case insert
```
```   308     thus ?case
```
```   309       by (simp add: LIMSEQ_add)
```
```   310   qed
```
```   311 next
```
```   312   case False
```
```   313   thus ?thesis
```
```   314     by (simp add: setsum_def LIMSEQ_const)
```
```   315 qed
```
```   316
```
```   317 lemma LIMSEQ_setprod:
```
```   318   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"
```
```   319   shows "(\<lambda>m. \<Prod>n\<in>S. X n m) ----> (\<Prod>n\<in>S. L n)"
```
```   320 proof (cases "finite S")
```
```   321   case True
```
```   322   thus ?thesis using n
```
```   323   proof (induct)
```
```   324     case empty
```
```   325     show ?case
```
```   326       by (simp add: LIMSEQ_const)
```
```   327   next
```
```   328     case insert
```
```   329     thus ?case
```
```   330       by (simp add: LIMSEQ_mult)
```
```   331   qed
```
```   332 next
```
```   333   case False
```
```   334   thus ?thesis
```
```   335     by (simp add: setprod_def LIMSEQ_const)
```
```   336 qed
```
```   337
```
```   338 lemma LIMSEQ_ignore_initial_segment: "f ----> a
```
```   339   ==> (%n. f(n + k)) ----> a"
```
```   340   apply (unfold LIMSEQ_def)
```
```   341   apply (clarify)
```
```   342   apply (drule_tac x = r in spec)
```
```   343   apply (clarify)
```
```   344   apply (rule_tac x = "no + k" in exI)
```
```   345   by auto
```
```   346
```
```   347 lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
```
```   348     f ----> a"
```
```   349   apply (unfold LIMSEQ_def)
```
```   350   apply clarsimp
```
```   351   apply (drule_tac x = r in spec)
```
```   352   apply clarsimp
```
```   353   apply (rule_tac x = "no + k" in exI)
```
```   354   apply clarsimp
```
```   355   apply (drule_tac x = "n - k" in spec)
```
```   356   apply (frule mp)
```
```   357   apply arith
```
```   358   apply simp
```
```   359 done
```
```   360
```
```   361 lemma LIMSEQ_diff_approach_zero:
```
```   362   "g ----> L ==> (%x. f x - g x) ----> 0  ==>
```
```   363      f ----> L"
```
```   364   apply (drule LIMSEQ_add)
```
```   365   apply assumption
```
```   366   apply simp
```
```   367 done
```
```   368
```
```   369 lemma LIMSEQ_diff_approach_zero2:
```
```   370   "f ----> L ==> (%x. f x - g x) ----> 0  ==>
```
```   371      g ----> L";
```
```   372   apply (drule LIMSEQ_diff)
```
```   373   apply assumption
```
```   374   apply simp
```
```   375 done
```
```   376
```
```   377
```
```   378 subsection{*Nslim and Lim*}
```
```   379
```
```   380 lemma limI: "X ----> L ==> lim X = L"
```
```   381 apply (simp add: lim_def)
```
```   382 apply (blast intro: LIMSEQ_unique)
```
```   383 done
```
```   384
```
```   385 lemma nslimI: "X ----NS> L ==> nslim X = L"
```
```   386 apply (simp add: nslim_def)
```
```   387 apply (blast intro: NSLIMSEQ_unique)
```
```   388 done
```
```   389
```
```   390 lemma lim_nslim_iff: "lim X = nslim X"
```
```   391 by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
```
```   392
```
```   393
```
```   394 subsection{*Convergence*}
```
```   395
```
```   396 lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
```
```   397 by (simp add: convergent_def)
```
```   398
```
```   399 lemma convergentI: "(X ----> L) ==> convergent X"
```
```   400 by (auto simp add: convergent_def)
```
```   401
```
```   402 lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
```
```   403 by (simp add: NSconvergent_def)
```
```   404
```
```   405 lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
```
```   406 by (auto simp add: NSconvergent_def)
```
```   407
```
```   408 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
```
```   409 by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
```
```   410
```
```   411 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
```
```   412 by (auto intro: someI simp add: NSconvergent_def nslim_def)
```
```   413
```
```   414 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
```
```   415 by (auto intro: someI simp add: convergent_def lim_def)
```
```   416
```
```   417 text{*Subsequence (alternative definition, (e.g. Hoskins)*}
```
```   418
```
```   419 lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
```
```   420 apply (simp add: subseq_def)
```
```   421 apply (auto dest!: less_imp_Suc_add)
```
```   422 apply (induct_tac k)
```
```   423 apply (auto intro: less_trans)
```
```   424 done
```
```   425
```
```   426
```
```   427 subsection{*Monotonicity*}
```
```   428
```
```   429 lemma monoseq_Suc:
```
```   430    "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
```
```   431                  | (\<forall>n. X (Suc n) \<le> X n))"
```
```   432 apply (simp add: monoseq_def)
```
```   433 apply (auto dest!: le_imp_less_or_eq)
```
```   434 apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
```
```   435 apply (induct_tac "ka")
```
```   436 apply (auto intro: order_trans)
```
```   437 apply (erule swap)
```
```   438 apply (induct_tac "k")
```
```   439 apply (auto intro: order_trans)
```
```   440 done
```
```   441
```
```   442 lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
```
```   443 by (simp add: monoseq_def)
```
```   444
```
```   445 lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
```
```   446 by (simp add: monoseq_def)
```
```   447
```
```   448 lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
```
```   449 by (simp add: monoseq_Suc)
```
```   450
```
```   451 lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
```
```   452 by (simp add: monoseq_Suc)
```
```   453
```
```   454
```
```   455 subsection{*Bounded Sequence*}
```
```   456
```
```   457 lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
```
```   458 by (simp add: Bseq_def)
```
```   459
```
```   460 lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
```
```   461 by (auto simp add: Bseq_def)
```
```   462
```
```   463 lemma lemma_NBseq_def:
```
```   464      "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) =
```
```   465       (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
```
```   466 apply auto
```
```   467  prefer 2 apply force
```
```   468 apply (cut_tac x = K in reals_Archimedean2, clarify)
```
```   469 apply (rule_tac x = n in exI, clarify)
```
```   470 apply (drule_tac x = na in spec)
```
```   471 apply (auto simp add: real_of_nat_Suc)
```
```   472 done
```
```   473
```
```   474 text{* alternative definition for Bseq *}
```
```   475 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
```
```   476 apply (simp add: Bseq_def)
```
```   477 apply (simp (no_asm) add: lemma_NBseq_def)
```
```   478 done
```
```   479
```
```   480 lemma lemma_NBseq_def2:
```
```   481      "(\<exists>K > 0. \<forall>n. \<bar>X n\<bar> \<le> K) = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
```
```   482 apply (subst lemma_NBseq_def, auto)
```
```   483 apply (rule_tac x = "Suc N" in exI)
```
```   484 apply (rule_tac [2] x = N in exI)
```
```   485 apply (auto simp add: real_of_nat_Suc)
```
```   486  prefer 2 apply (blast intro: order_less_imp_le)
```
```   487 apply (drule_tac x = n in spec, simp)
```
```   488 done
```
```   489
```
```   490 (* yet another definition for Bseq *)
```
```   491 lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
```
```   492 by (simp add: Bseq_def lemma_NBseq_def2)
```
```   493
```
```   494 lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
```
```   495 by (simp add: NSBseq_def)
```
```   496
```
```   497 lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
```
```   498 by (simp add: NSBseq_def)
```
```   499
```
```   500 text{*The standard definition implies the nonstandard definition*}
```
```   501
```
```   502 lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
```
```   503 by auto
```
```   504
```
```   505 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
```
```   506 apply (simp add: Bseq_def NSBseq_def, safe)
```
```   507 apply (rule_tac x = N in star_cases)
```
```   508 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff
```
```   509                       HNatInfinite_FreeUltrafilterNat_iff)
```
```   510 apply (rule bexI [OF _ Rep_star_star_n])
```
```   511 apply (drule_tac f = Xa in lemma_Bseq)
```
```   512 apply (rule_tac x = "K+1" in exI)
```
```   513 apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
```
```   514 done
```
```   515
```
```   516 text{*The nonstandard definition implies the standard definition*}
```
```   517
```
```   518 (* similar to NSLIM proof in REALTOPOS *)
```
```   519
```
```   520 text{* We need to get rid of the real variable and do so by proving the
```
```   521    following, which relies on the Archimedean property of the reals.
```
```   522    When we skolemize we then get the required function @{term "f::nat=>nat"}.
```
```   523    Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
```
```   524    which woulid be useless.*}
```
```   525
```
```   526 lemma lemmaNSBseq:
```
```   527      "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
```
```   528       ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
```
```   529 apply safe
```
```   530 apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
```
```   531 done
```
```   532
```
```   533 lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n. K < \<bar>X n\<bar>
```
```   534                      ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
```
```   535 apply (drule lemmaNSBseq)
```
```   536 apply (drule choice, blast)
```
```   537 done
```
```   538
```
```   539 lemma real_seq_to_hypreal_HInfinite:
```
```   540      "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
```
```   541       ==>  star_n (X o f) : HInfinite"
```
```   542 apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
```
```   543 apply (rule bexI [OF _ Rep_star_star_n], clarify)
```
```   544 apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
```
```   545 apply (drule FreeUltrafilterNat_all)
```
```   546 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
```
```   547 apply (auto simp add: real_of_nat_Suc)
```
```   548 done
```
```   549
```
```   550 text{* Now prove that we can get out an infinite hypernatural as well
```
```   551      defined using the skolem function  @{term "f::nat=>nat"} above*}
```
```   552
```
```   553 lemma lemma_finite_NSBseq:
```
```   554      "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
```
```   555       {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
```
```   556       {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
```
```   557 by (auto dest!: le_imp_less_or_eq)
```
```   558
```
```   559 lemma lemma_finite_NSBseq2:
```
```   560      "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
```
```   561 apply (induct "u")
```
```   562 apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
```
```   563 apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
```
```   564 apply (auto intro: finite_real_of_nat_less_real
```
```   565             simp add: real_of_nat_Suc less_diff_eq [symmetric])
```
```   566 done
```
```   567
```
```   568 lemma HNatInfinite_skolem_f:
```
```   569      "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
```
```   570       ==> star_n f : HNatInfinite"
```
```   571 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
```
```   572 apply (rule bexI [OF _ Rep_star_star_n], safe)
```
```   573 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
```
```   574 apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE])
```
```   575 apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
```
```   576                     {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
```
```   577 apply (erule ssubst)
```
```   578  apply (auto simp add: linorder_not_less Compl_def)
```
```   579 done
```
```   580
```
```   581 lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
```
```   582 apply (simp add: Bseq_def NSBseq_def)
```
```   583 apply (rule ccontr)
```
```   584 apply (auto simp add: linorder_not_less [symmetric])
```
```   585 apply (drule lemmaNSBseq2, safe)
```
```   586 apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
```
```   587 apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
```
```   588 apply (auto simp add: starfun o_def HFinite_HInfinite_iff)
```
```   589 done
```
```   590
```
```   591 text{* Equivalence of nonstandard and standard definitions
```
```   592   for a bounded sequence*}
```
```   593 lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
```
```   594 by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
```
```   595
```
```   596 text{*A convergent sequence is bounded:
```
```   597  Boundedness as a necessary condition for convergence.
```
```   598  The nonstandard version has no existential, as usual *}
```
```   599
```
```   600 lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
```
```   601 apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
```
```   602 apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
```
```   603 done
```
```   604
```
```   605 text{*Standard Version: easily now proved using equivalence of NS and
```
```   606  standard definitions *}
```
```   607 lemma convergent_Bseq: "convergent X ==> Bseq X"
```
```   608 by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
```
```   609
```
```   610
```
```   611 subsection{*Upper Bounds and Lubs of Bounded Sequences*}
```
```   612
```
```   613 lemma Bseq_isUb:
```
```   614   "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
```
```   615 by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
```
```   616
```
```   617
```
```   618 text{* Use completeness of reals (supremum property)
```
```   619    to show that any bounded sequence has a least upper bound*}
```
```   620
```
```   621 lemma Bseq_isLub:
```
```   622   "!!(X::nat=>real). Bseq X ==>
```
```   623    \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
```
```   624 by (blast intro: reals_complete Bseq_isUb)
```
```   625
```
```   626 lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
```
```   627 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
```
```   628
```
```   629 lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
```
```   630 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
```
```   631
```
```   632
```
```   633 subsection{*A Bounded and Monotonic Sequence Converges*}
```
```   634
```
```   635 lemma lemma_converg1:
```
```   636      "!!(X::nat=>real). [| \<forall>m. \<forall> n \<ge> m. X m \<le> X n;
```
```   637                   isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
```
```   638                |] ==> \<forall>n \<ge> ma. X n = X ma"
```
```   639 apply safe
```
```   640 apply (drule_tac y = "X n" in isLubD2)
```
```   641 apply (blast dest: order_antisym)+
```
```   642 done
```
```   643
```
```   644 text{* The best of both worlds: Easier to prove this result as a standard
```
```   645    theorem and then use equivalence to "transfer" it into the
```
```   646    equivalent nonstandard form if needed!*}
```
```   647
```
```   648 lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
```
```   649 apply (simp add: LIMSEQ_def)
```
```   650 apply (rule_tac x = "X m" in exI, safe)
```
```   651 apply (rule_tac x = m in exI, safe)
```
```   652 apply (drule spec, erule impE, auto)
```
```   653 done
```
```   654
```
```   655 text{*Now, the same theorem in terms of NS limit *}
```
```   656 lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X ----NS> L)"
```
```   657 by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
```
```   658
```
```   659 lemma lemma_converg2:
```
```   660    "!!(X::nat=>real).
```
```   661     [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
```
```   662 apply safe
```
```   663 apply (drule_tac y = "X m" in isLubD2)
```
```   664 apply (auto dest!: order_le_imp_less_or_eq)
```
```   665 done
```
```   666
```
```   667 lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
```
```   668 by (rule setleI [THEN isUbI], auto)
```
```   669
```
```   670 text{* FIXME: @{term "U - T < U"} is redundant *}
```
```   671 lemma lemma_converg4: "!!(X::nat=> real).
```
```   672                [| \<forall>m. X m ~= U;
```
```   673                   isLub UNIV {x. \<exists>n. X n = x} U;
```
```   674                   0 < T;
```
```   675                   U + - T < U
```
```   676                |] ==> \<exists>m. U + -T < X m & X m < U"
```
```   677 apply (drule lemma_converg2, assumption)
```
```   678 apply (rule ccontr, simp)
```
```   679 apply (simp add: linorder_not_less)
```
```   680 apply (drule lemma_converg3)
```
```   681 apply (drule isLub_le_isUb, assumption)
```
```   682 apply (auto dest: order_less_le_trans)
```
```   683 done
```
```   684
```
```   685 text{*A standard proof of the theorem for monotone increasing sequence*}
```
```   686
```
```   687 lemma Bseq_mono_convergent:
```
```   688      "[| Bseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> convergent X"
```
```   689 apply (simp add: convergent_def)
```
```   690 apply (frule Bseq_isLub, safe)
```
```   691 apply (case_tac "\<exists>m. X m = U", auto)
```
```   692 apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
```
```   693 (* second case *)
```
```   694 apply (rule_tac x = U in exI)
```
```   695 apply (subst LIMSEQ_iff, safe)
```
```   696 apply (frule lemma_converg2, assumption)
```
```   697 apply (drule lemma_converg4, auto)
```
```   698 apply (rule_tac x = m in exI, safe)
```
```   699 apply (subgoal_tac "X m \<le> X n")
```
```   700  prefer 2 apply blast
```
```   701 apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
```
```   702 done
```
```   703
```
```   704 text{*Nonstandard version of the theorem*}
```
```   705
```
```   706 lemma NSBseq_mono_NSconvergent:
```
```   707      "[| NSBseq X; \<forall>m. \<forall>n \<ge> m. X m \<le> X n |] ==> NSconvergent X"
```
```   708 by (auto intro: Bseq_mono_convergent
```
```   709          simp add: convergent_NSconvergent_iff [symmetric]
```
```   710                    Bseq_NSBseq_iff [symmetric])
```
```   711
```
```   712 lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
```
```   713 apply (simp add: convergent_def)
```
```   714 apply (auto dest: LIMSEQ_minus)
```
```   715 apply (drule LIMSEQ_minus, auto)
```
```   716 done
```
```   717
```
```   718 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
```
```   719 by (simp add: Bseq_def)
```
```   720
```
```   721 text{*Main monotonicity theorem*}
```
```   722 lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
```
```   723 apply (simp add: monoseq_def, safe)
```
```   724 apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
```
```   725 apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
```
```   726 apply (auto intro!: Bseq_mono_convergent)
```
```   727 done
```
```   728
```
```   729
```
```   730 subsection{*A Few More Equivalence Theorems for Boundedness*}
```
```   731
```
```   732 text{*alternative formulation for boundedness*}
```
```   733 lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. \<bar>X(n) + -x\<bar> \<le> k)"
```
```   734 apply (unfold Bseq_def, safe)
```
```   735 apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
```
```   736 apply (rule_tac x = K in exI, simp)
```
```   737 apply (rule exI [where x = 0], auto)
```
```   738 apply (drule_tac x=n in spec, arith)+
```
```   739 done
```
```   740
```
```   741 text{*alternative formulation for boundedness*}
```
```   742 lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. abs(X(n) + -X(N)) \<le> k)"
```
```   743 apply safe
```
```   744 apply (simp add: Bseq_def, safe)
```
```   745 apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
```
```   746 apply auto
```
```   747 apply arith
```
```   748 apply (rule_tac x = N in exI, safe)
```
```   749 apply (drule_tac x = n in spec, arith)
```
```   750 apply (auto simp add: Bseq_iff2)
```
```   751 done
```
```   752
```
```   753 lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
```
```   754 apply (simp add: Bseq_def)
```
```   755 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
```
```   756 apply (drule_tac [2] x = n in spec, arith+)
```
```   757 done
```
```   758
```
```   759
```
```   760 subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
```
```   761
```
```   762 subsubsection{*Standard Implies Nonstandard*}
```
```   763
```
```   764 lemma lemmaCauchy1:
```
```   765      "star_n x : HNatInfinite
```
```   766       ==> {n. M \<le> x n} : FreeUltrafilterNat"
```
```   767 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
```
```   768 apply (drule_tac x = M in spec, ultra)
```
```   769 done
```
```   770
```
```   771 lemma lemmaCauchy2:
```
```   772      "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
```
```   773       {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
```
```   774       {n. abs (X (xa n) + - X (x n)) < u}"
```
```   775 by blast
```
```   776
```
```   777 lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
```
```   778 apply (simp add: Cauchy_def NSCauchy_def, safe)
```
```   779 apply (rule_tac x = M in star_cases)
```
```   780 apply (rule_tac x = N in star_cases)
```
```   781 apply (rule approx_minus_iff [THEN iffD2])
```
```   782 apply (rule mem_infmal_iff [THEN iffD1])
```
```   783 apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
```
```   784 apply (rule bexI, auto)
```
```   785 apply (drule spec, auto)
```
```   786 apply (drule_tac M = M in lemmaCauchy1)
```
```   787 apply (drule_tac M = M in lemmaCauchy1)
```
```   788 apply (rule_tac x1 = Xaa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
```
```   789 apply (rule FreeUltrafilterNat_Int)
```
```   790 apply (auto intro: FreeUltrafilterNat_Int)
```
```   791 done
```
```   792
```
```   793 subsubsection{*Nonstandard Implies Standard*}
```
```   794
```
```   795 lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
```
```   796 apply (auto simp add: Cauchy_def NSCauchy_def)
```
```   797 apply (rule ccontr, simp)
```
```   798 apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)
```
```   799 apply (drule bspec, assumption)
```
```   800 apply (drule_tac x = "star_n fa" in bspec);
```
```   801 apply (auto simp add: starfun)
```
```   802 apply (drule approx_minus_iff [THEN iffD1])
```
```   803 apply (drule mem_infmal_iff [THEN iffD2])
```
```   804 apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
```
```   805 apply (rename_tac "Y")
```
```   806 apply (drule_tac x = e in spec, auto)
```
```   807 apply (drule FreeUltrafilterNat_Int, assumption)
```
```   808 apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>")
```
```   809  prefer 2 apply (erule FreeUltrafilterNat_subset, force)
```
```   810 apply (rule FreeUltrafilterNat_empty [THEN notE])
```
```   811 apply (subgoal_tac
```
```   812          "{n. abs (X (f n) + - X (fa n)) < e} Int
```
```   813           {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
```
```   814 apply auto
```
```   815 done
```
```   816
```
```   817
```
```   818 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
```
```   819 by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
```
```   820
```
```   821 text{*A Cauchy sequence is bounded -- this is the standard
```
```   822   proof mechanization rather than the nonstandard proof*}
```
```   823
```
```   824 lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
```
```   825           ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
```
```   826 apply safe
```
```   827 apply (drule spec, auto, arith)
```
```   828 done
```
```   829
```
```   830 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
```
```   831 by auto
```
```   832
```
```   833 text{* FIXME: Long. Maximal element in subsequence *}
```
```   834 lemma SUP_rabs_subseq:
```
```   835      "\<exists>m \<le> M. \<forall>n \<le> M. \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>"
```
```   836 apply (induct M)
```
```   837 apply (rule_tac x = 0 in exI, simp, safe)
```
```   838 apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
```
```   839 apply safe
```
```   840 apply (rule_tac x = m in exI)
```
```   841 apply (rule_tac [2] x = m in exI)
```
```   842 apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
```
```   843 apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE])
```
```   844 apply (simp_all add: less_Suc_cancel_iff)
```
```   845 apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
```
```   846 done
```
```   847
```
```   848 lemma lemma_Nat_covered:
```
```   849      "[| \<forall>m::nat. m \<le> M --> P M m;
```
```   850          \<forall>m \<ge> M. P M m |]
```
```   851       ==> \<forall>m. P M m"
```
```   852 by (auto elim: less_asym simp add: le_def)
```
```   853
```
```   854
```
```   855 lemma lemma_trans1:
```
```   856      "[| \<forall>n \<le> M. \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
```
```   857       ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
```
```   858 by (blast intro: order_le_less_trans [THEN order_less_imp_le])
```
```   859
```
```   860 lemma lemma_trans2:
```
```   861      "[| \<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a; a < b |]
```
```   862       ==> \<forall>n \<ge> M. \<bar>X n\<bar>\<le> b"
```
```   863 by (blast intro: order_less_trans [THEN order_less_imp_le])
```
```   864
```
```   865 lemma lemma_trans3:
```
```   866      "[| \<forall>n \<le> M. \<bar>X n\<bar> \<le> a; a = b |]
```
```   867       ==> \<forall>n \<le> M. \<bar>X n\<bar> \<le> b"
```
```   868 by auto
```
```   869
```
```   870 lemma lemma_trans4: "\<forall>n \<ge> M. \<bar>(X::nat=>real) n\<bar> < a
```
```   871               ==>  \<forall>n \<ge> M. \<bar>X n\<bar> \<le> a"
```
```   872 by (blast intro: order_less_imp_le)
```
```   873
```
```   874
```
```   875 text{*Proof is more involved than outlines sketched by various authors
```
```   876  would suggest*}
```
```   877
```
```   878 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
```
```   879 apply (simp add: Cauchy_def Bseq_def)
```
```   880 apply (drule_tac x = 1 in spec)
```
```   881 apply (erule zero_less_one [THEN [2] impE], safe)
```
```   882 apply (drule_tac x = M in spec, simp)
```
```   883 apply (drule lemmaCauchy)
```
```   884 apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
```
```   885 apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
```
```   886 apply safe
```
```   887 apply (drule lemma_trans1, assumption)
```
```   888 apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
```
```   889 apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
```
```   890 apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
```
```   891 apply (drule lemma_trans4)
```
```   892 apply (drule_tac [2] lemma_trans4)
```
```   893 apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
```
```   894 apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
```
```   895 apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
```
```   896 apply (auto elim!: lemma_Nat_covered)
```
```   897 done
```
```   898
```
```   899 text{*A Cauchy sequence is bounded -- nonstandard version*}
```
```   900
```
```   901 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
```
```   902 by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
```
```   903
```
```   904
```
```   905 text{*Equivalence of Cauchy criterion and convergence:
```
```   906   We will prove this using our NS formulation which provides a
```
```   907   much easier proof than using the standard definition. We do not
```
```   908   need to use properties of subsequences such as boundedness,
```
```   909   monotonicity etc... Compare with Harrison's corresponding proof
```
```   910   in HOL which is much longer and more complicated. Of course, we do
```
```   911   not have problems which he encountered with guessing the right
```
```   912   instantiations for his 'espsilon-delta' proof(s) in this case
```
```   913   since the NS formulations do not involve existential quantifiers.*}
```
```   914
```
```   915 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
```
```   916 apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
```
```   917 apply (frule NSCauchy_NSBseq)
```
```   918 apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
```
```   919 apply (drule HNatInfinite_whn [THEN [2] bspec])
```
```   920 apply (drule HNatInfinite_whn [THEN [2] bspec])
```
```   921 apply (auto dest!: st_part_Ex simp add: SReal_iff)
```
```   922 apply (blast intro: approx_trans3)
```
```   923 done
```
```   924
```
```   925 text{*Standard proof for free*}
```
```   926 lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
```
```   927 by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
```
```   928
```
```   929
```
```   930 text{*We can now try and derive a few properties of sequences,
```
```   931      starting with the limit comparison property for sequences.*}
```
```   932
```
```   933 lemma NSLIMSEQ_le:
```
```   934        "[| f ----NS> l; g ----NS> m;
```
```   935            \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n)
```
```   936         |] ==> l \<le> m"
```
```   937 apply (simp add: NSLIMSEQ_def, safe)
```
```   938 apply (drule starfun_le_mono)
```
```   939 apply (drule HNatInfinite_whn [THEN [2] bspec])+
```
```   940 apply (drule_tac x = whn in spec)
```
```   941 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
```
```   942 apply clarify
```
```   943 apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
```
```   944 done
```
```   945
```
```   946 (* standard version *)
```
```   947 lemma LIMSEQ_le:
```
```   948      "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
```
```   949       ==> l \<le> m"
```
```   950 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
```
```   951
```
```   952 lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
```
```   953 apply (rule LIMSEQ_le)
```
```   954 apply (rule LIMSEQ_const, auto)
```
```   955 done
```
```   956
```
```   957 lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
```
```   958 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
```
```   959
```
```   960 lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
```
```   961 apply (rule LIMSEQ_le)
```
```   962 apply (rule_tac [2] LIMSEQ_const, auto)
```
```   963 done
```
```   964
```
```   965 lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
```
```   966 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
```
```   967
```
```   968 text{*Shift a convergent series by 1:
```
```   969   By the equivalence between Cauchiness and convergence and because
```
```   970   the successor of an infinite hypernatural is also infinite.*}
```
```   971
```
```   972 lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
```
```   973 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
```
```   974 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
```
```   975 apply (drule bspec, assumption)
```
```   976 apply (drule bspec, assumption)
```
```   977 apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
```
```   978 apply (blast intro: approx_trans3)
```
```   979 done
```
```   980
```
```   981 text{* standard version *}
```
```   982 lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
```
```   983 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
```
```   984
```
```   985 lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
```
```   986 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
```
```   987 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
```
```   988 apply (drule bspec, assumption)
```
```   989 apply (drule bspec, assumption)
```
```   990 apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
```
```   991 apply (drule_tac x="N - 1" in bspec)
```
```   992 apply (auto intro: approx_trans3)
```
```   993 done
```
```   994
```
```   995 lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
```
```   996 apply (simp add: LIMSEQ_NSLIMSEQ_iff)
```
```   997 apply (erule NSLIMSEQ_imp_Suc)
```
```   998 done
```
```   999
```
```  1000 lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
```
```  1001 by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
```
```  1002
```
```  1003 lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
```
```  1004 by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
```
```  1005
```
```  1006 text{*A sequence tends to zero iff its abs does*}
```
```  1007 lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
```
```  1008 by (simp add: LIMSEQ_def)
```
```  1009
```
```  1010 text{*We prove the NS version from the standard one, since the NS proof
```
```  1011    seems more complicated than the standard one above!*}
```
```  1012 lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
```
```  1013 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
```
```  1014
```
```  1015 text{*Generalization to other limits*}
```
```  1016 lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
```
```  1017 apply (simp add: NSLIMSEQ_def)
```
```  1018 apply (auto intro: approx_hrabs
```
```  1019             simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
```
```  1020 done
```
```  1021
```
```  1022 text{* standard version *}
```
```  1023 lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
```
```  1024 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
```
```  1025
```
```  1026 text{*An unbounded sequence's inverse tends to 0*}
```
```  1027
```
```  1028 text{* standard proof seems easier *}
```
```  1029 lemma LIMSEQ_inverse_zero:
```
```  1030       "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
```
```  1031 apply (simp add: LIMSEQ_def, safe)
```
```  1032 apply (drule_tac x = "inverse r" in spec, safe)
```
```  1033 apply (rule_tac x = N in exI, safe)
```
```  1034 apply (drule spec, auto)
```
```  1035 apply (frule positive_imp_inverse_positive)
```
```  1036 apply (frule order_less_trans, assumption)
```
```  1037 apply (frule_tac a = "f n" in positive_imp_inverse_positive)
```
```  1038 apply (simp add: abs_if)
```
```  1039 apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
```
```  1040 apply (auto intro: inverse_less_iff_less [THEN iffD2]
```
```  1041             simp del: inverse_inverse_eq)
```
```  1042 done
```
```  1043
```
```  1044 lemma NSLIMSEQ_inverse_zero:
```
```  1045      "\<forall>y. \<exists>N. \<forall>n \<ge> N. y < f(n)
```
```  1046       ==> (%n. inverse(f n)) ----NS> 0"
```
```  1047 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
```
```  1048
```
```  1049 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
```
```  1050
```
```  1051 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
```
```  1052 apply (rule LIMSEQ_inverse_zero, safe)
```
```  1053 apply (cut_tac x = y in reals_Archimedean2)
```
```  1054 apply (safe, rule_tac x = n in exI)
```
```  1055 apply (auto simp add: real_of_nat_Suc)
```
```  1056 done
```
```  1057
```
```  1058 lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
```
```  1059 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
```
```  1060
```
```  1061 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
```
```  1062 infinity is now easily proved*}
```
```  1063
```
```  1064 lemma LIMSEQ_inverse_real_of_nat_add:
```
```  1065      "(%n. r + inverse(real(Suc n))) ----> r"
```
```  1066 by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
```
```  1067
```
```  1068 lemma NSLIMSEQ_inverse_real_of_nat_add:
```
```  1069      "(%n. r + inverse(real(Suc n))) ----NS> r"
```
```  1070 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
```
```  1071
```
```  1072 lemma LIMSEQ_inverse_real_of_nat_add_minus:
```
```  1073      "(%n. r + -inverse(real(Suc n))) ----> r"
```
```  1074 by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
```
```  1075
```
```  1076 lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
```
```  1077      "(%n. r + -inverse(real(Suc n))) ----NS> r"
```
```  1078 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
```
```  1079
```
```  1080 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
```
```  1081      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
```
```  1082 by (cut_tac b=1 in
```
```  1083         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
```
```  1084
```
```  1085 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
```
```  1086      "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
```
```  1087 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
```
```  1088
```
```  1089
```
```  1090 text{* Real Powers*}
```
```  1091
```
```  1092 lemma NSLIMSEQ_pow [rule_format]:
```
```  1093      "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
```
```  1094 apply (induct "m")
```
```  1095 apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
```
```  1096 done
```
```  1097
```
```  1098 lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
```
```  1099 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
```
```  1100
```
```  1101 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
```
```  1102 "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
```
```  1103   also fact that bounded and monotonic sequence converges.*}
```
```  1104
```
```  1105 lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
```
```  1106 apply (simp add: Bseq_def)
```
```  1107 apply (rule_tac x = 1 in exI)
```
```  1108 apply (simp add: power_abs)
```
```  1109 apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
```
```  1110 done
```
```  1111
```
```  1112 lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
```
```  1113 apply (clarify intro!: mono_SucI2)
```
```  1114 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
```
```  1115 done
```
```  1116
```
```  1117 lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
```
```  1118 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
```
```  1119
```
```  1120 text{* We now use NS criterion to bring proof of theorem through *}
```
```  1121
```
```  1122 lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
```
```  1123 apply (simp add: NSLIMSEQ_def)
```
```  1124 apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
```
```  1125 apply (frule NSconvergentD)
```
```  1126 apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
```
```  1127 apply (frule HNatInfinite_add_one)
```
```  1128 apply (drule bspec, assumption)
```
```  1129 apply (drule bspec, assumption)
```
```  1130 apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
```
```  1131 apply (simp add: hyperpow_add)
```
```  1132 apply (drule approx_mult_subst_SReal, assumption)
```
```  1133 apply (drule approx_trans3, assumption)
```
```  1134 apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
```
```  1135 done
```
```  1136
```
```  1137 text{* standard version *}
```
```  1138 lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
```
```  1139 by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
```
```  1140
```
```  1141 lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
```
```  1142 apply (cut_tac a = a and x1 = "inverse x" in
```
```  1143         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
```
```  1144 apply (auto simp add: divide_inverse power_inverse)
```
```  1145 apply (simp add: inverse_eq_divide pos_divide_less_eq)
```
```  1146 done
```
```  1147
```
```  1148 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
```
```  1149
```
```  1150 lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
```
```  1151 by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
```
```  1152
```
```  1153 lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
```
```  1154 by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```  1155
```
```  1156 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
```
```  1157 apply (rule LIMSEQ_rabs_zero [THEN iffD1])
```
```  1158 apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
```
```  1159 done
```
```  1160
```
```  1161 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
```
```  1162 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
```
```  1163
```
```  1164 subsection{*Hyperreals and Sequences*}
```
```  1165
```
```  1166 text{*A bounded sequence is a finite hyperreal*}
```
```  1167 lemma NSBseq_HFinite_hypreal: "NSBseq X ==> star_n X : HFinite"
```
```  1168 by (auto intro!: bexI lemma_starrel_refl
```
```  1169             intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
```
```  1170             simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
```
```  1171                       Bseq_iff1a)
```
```  1172
```
```  1173 text{*A sequence converging to zero defines an infinitesimal*}
```
```  1174 lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
```
```  1175       "X ----NS> 0 ==> star_n X : Infinitesimal"
```
```  1176 apply (simp add: NSLIMSEQ_def)
```
```  1177 apply (drule_tac x = whn in bspec)
```
```  1178 apply (simp add: HNatInfinite_whn)
```
```  1179 apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfun)
```
```  1180 done
```
```  1181
```
```  1182 (***---------------------------------------------------------------
```
```  1183     Theorems proved by Harrison in HOL that we do not need
```
```  1184     in order to prove equivalence between Cauchy criterion
```
```  1185     and convergence:
```
```  1186  -- Show that every sequence contains a monotonic subsequence
```
```  1187 Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
```
```  1188  -- Show that a subsequence of a bounded sequence is bounded
```
```  1189 Goal "Bseq X ==> Bseq (%n. X (f n))";
```
```  1190  -- Show we can take subsequential terms arbitrarily far
```
```  1191     up a sequence
```
```  1192 Goal "subseq f ==> n \<le> f(n)";
```
```  1193 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
```
```  1194  ---------------------------------------------------------------***)
```
```  1195
```
```  1196
```
```  1197 ML
```
```  1198 {*
```
```  1199 val Cauchy_def = thm"Cauchy_def";
```
```  1200 val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
```
```  1201 val LIMSEQ_iff = thm "LIMSEQ_iff";
```
```  1202 val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
```
```  1203 val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
```
```  1204 val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
```
```  1205 val Compl_less_set = thm "Compl_less_set";
```
```  1206 val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
```
```  1207 val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
```
```  1208 val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
```
```  1209 val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
```
```  1210 val NSLIMSEQ_const = thm "NSLIMSEQ_const";
```
```  1211 val LIMSEQ_const = thm "LIMSEQ_const";
```
```  1212 val NSLIMSEQ_add = thm "NSLIMSEQ_add";
```
```  1213 val LIMSEQ_add = thm "LIMSEQ_add";
```
```  1214 val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
```
```  1215 val LIMSEQ_mult = thm "LIMSEQ_mult";
```
```  1216 val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
```
```  1217 val LIMSEQ_minus = thm "LIMSEQ_minus";
```
```  1218 val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
```
```  1219 val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
```
```  1220 val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
```
```  1221 val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
```
```  1222 val LIMSEQ_diff = thm "LIMSEQ_diff";
```
```  1223 val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
```
```  1224 val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
```
```  1225 val LIMSEQ_inverse = thm "LIMSEQ_inverse";
```
```  1226 val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
```
```  1227 val LIMSEQ_divide = thm "LIMSEQ_divide";
```
```  1228 val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
```
```  1229 val LIMSEQ_unique = thm "LIMSEQ_unique";
```
```  1230 val limI = thm "limI";
```
```  1231 val nslimI = thm "nslimI";
```
```  1232 val lim_nslim_iff = thm "lim_nslim_iff";
```
```  1233 val convergentD = thm "convergentD";
```
```  1234 val convergentI = thm "convergentI";
```
```  1235 val NSconvergentD = thm "NSconvergentD";
```
```  1236 val NSconvergentI = thm "NSconvergentI";
```
```  1237 val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
```
```  1238 val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
```
```  1239 val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
```
```  1240 val subseq_Suc_iff = thm "subseq_Suc_iff";
```
```  1241 val monoseq_Suc = thm "monoseq_Suc";
```
```  1242 val monoI1 = thm "monoI1";
```
```  1243 val monoI2 = thm "monoI2";
```
```  1244 val mono_SucI1 = thm "mono_SucI1";
```
```  1245 val mono_SucI2 = thm "mono_SucI2";
```
```  1246 val BseqD = thm "BseqD";
```
```  1247 val BseqI = thm "BseqI";
```
```  1248 val Bseq_iff = thm "Bseq_iff";
```
```  1249 val Bseq_iff1a = thm "Bseq_iff1a";
```
```  1250 val NSBseqD = thm "NSBseqD";
```
```  1251 val NSBseqI = thm "NSBseqI";
```
```  1252 val Bseq_NSBseq = thm "Bseq_NSBseq";
```
```  1253 val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
```
```  1254 val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
```
```  1255 val NSBseq_Bseq = thm "NSBseq_Bseq";
```
```  1256 val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
```
```  1257 val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
```
```  1258 val convergent_Bseq = thm "convergent_Bseq";
```
```  1259 val Bseq_isUb = thm "Bseq_isUb";
```
```  1260 val Bseq_isLub = thm "Bseq_isLub";
```
```  1261 val NSBseq_isUb = thm "NSBseq_isUb";
```
```  1262 val NSBseq_isLub = thm "NSBseq_isLub";
```
```  1263 val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
```
```  1264 val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
```
```  1265 val Bseq_mono_convergent = thm "Bseq_mono_convergent";
```
```  1266 val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
```
```  1267 val convergent_minus_iff = thm "convergent_minus_iff";
```
```  1268 val Bseq_minus_iff = thm "Bseq_minus_iff";
```
```  1269 val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
```
```  1270 val Bseq_iff2 = thm "Bseq_iff2";
```
```  1271 val Bseq_iff3 = thm "Bseq_iff3";
```
```  1272 val BseqI2 = thm "BseqI2";
```
```  1273 val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
```
```  1274 val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
```
```  1275 val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
```
```  1276 val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
```
```  1277 val SUP_rabs_subseq = thm "SUP_rabs_subseq";
```
```  1278 val Cauchy_Bseq = thm "Cauchy_Bseq";
```
```  1279 val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
```
```  1280 val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
```
```  1281 val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
```
```  1282 val NSLIMSEQ_le = thm "NSLIMSEQ_le";
```
```  1283 val LIMSEQ_le = thm "LIMSEQ_le";
```
```  1284 val LIMSEQ_le_const = thm "LIMSEQ_le_const";
```
```  1285 val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
```
```  1286 val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
```
```  1287 val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
```
```  1288 val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
```
```  1289 val LIMSEQ_Suc = thm "LIMSEQ_Suc";
```
```  1290 val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
```
```  1291 val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
```
```  1292 val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
```
```  1293 val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
```
```  1294 val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
```
```  1295 val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
```
```  1296 val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
```
```  1297 val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
```
```  1298 val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
```
```  1299 val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
```
```  1300 val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
```
```  1301 val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
```
```  1302 val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
```
```  1303 val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
```
```  1304 val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
```
```  1305 val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
```
```  1306 val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
```
```  1307 val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
```
```  1308 val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
```
```  1309 val LIMSEQ_pow = thm "LIMSEQ_pow";
```
```  1310 val Bseq_realpow = thm "Bseq_realpow";
```
```  1311 val monoseq_realpow = thm "monoseq_realpow";
```
```  1312 val convergent_realpow = thm "convergent_realpow";
```
```  1313 val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
```
```  1314 *}
```
```  1315
```
```  1316
```
```  1317 end
```