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