src/HOL/Hyperreal/SEQ.thy
author paulson
Tue Oct 12 11:48:21 2004 +0200 (2004-10-12)
changeset 15241 a3949068537e
parent 15236 f289e8ba2bb3
child 15251 bb6f072c8d10
permissions -rw-r--r--
tweaks concerned with poly bug-fixing
     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
    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 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 exI [where x = 0], 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, auto)
   660 apply (drule_tac [2] x = n in spec, arith+)
   661 done
   662 
   663 
   664 subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
   665 
   666 subsubsection{*Standard Implies Nonstandard*}
   667 
   668 lemma lemmaCauchy1:
   669      "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
   670       ==> {n. M \<le> x n} : FreeUltrafilterNat"
   671 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   672 apply (drule_tac x = M in spec, ultra)
   673 done
   674 
   675 lemma lemmaCauchy2:
   676      "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
   677       {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
   678       {n. abs (X (xa n) + - X (x n)) < u}"
   679 by blast
   680 
   681 lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
   682 apply (simp add: Cauchy_def NSCauchy_def, safe)
   683 apply (rule_tac z = M in eq_Abs_hypnat)
   684 apply (rule_tac z = N in eq_Abs_hypnat)
   685 apply (rule approx_minus_iff [THEN iffD2])
   686 apply (rule mem_infmal_iff [THEN iffD1])
   687 apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   688 apply (rule bexI, auto)
   689 apply (drule spec, auto)
   690 apply (drule_tac M = M in lemmaCauchy1)
   691 apply (drule_tac M = M in lemmaCauchy1)
   692 apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
   693 apply (rule FreeUltrafilterNat_Int)
   694 apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
   695 done
   696 
   697 subsubsection{*Nonstandard Implies Standard*}
   698 
   699 lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
   700 apply (auto simp add: Cauchy_def NSCauchy_def)
   701 apply (rule ccontr, simp)
   702 apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
   703 apply (drule bspec, assumption)
   704 apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); 
   705 apply (auto simp add: starfunNat)
   706 apply (drule approx_minus_iff [THEN iffD1])
   707 apply (drule mem_infmal_iff [THEN iffD2])
   708 apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   709 apply (rename_tac "Y")
   710 apply (drule_tac x = e in spec, auto)
   711 apply (drule FreeUltrafilterNat_Int, assumption)
   712 apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>") 
   713  prefer 2 apply (erule FreeUltrafilterNat_subset, force) 
   714 apply (rule FreeUltrafilterNat_empty [THEN notE]) 
   715 apply (subgoal_tac
   716          "{n. abs (X (f n) + - X (fa n)) < e} Int 
   717           {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
   718 apply auto  
   719 done
   720 
   721 
   722 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
   723 by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
   724 
   725 text{*A Cauchy sequence is bounded -- this is the standard
   726   proof mechanization rather than the nonstandard proof*}
   727 
   728 lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
   729           ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
   730 apply safe
   731 apply (drule spec, auto, arith)
   732 done
   733 
   734 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
   735 by auto
   736 
   737 text{* FIXME: Long. Maximal element in subsequence *}
   738 lemma SUP_rabs_subseq:
   739      "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
   740 apply (induct M)
   741 apply (rule_tac x = 0 in exI, simp, safe)
   742 apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
   743 apply safe
   744 apply (rule_tac x = m in exI)
   745 apply (rule_tac [2] x = m in exI)
   746 apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
   747 apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE]) 
   748 apply (simp_all add: less_Suc_cancel_iff)
   749 apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
   750 done
   751 
   752 lemma lemma_Nat_covered:
   753      "[| \<forall>m::nat. m \<le> M --> P M m;
   754          \<forall>m. M \<le> m --> P M m |]
   755       ==> \<forall>m. P M m"
   756 by (auto elim: less_asym simp add: le_def)
   757 
   758 
   759 lemma lemma_trans1:
   760      "[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
   761       ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
   762 by (blast intro: order_le_less_trans [THEN order_less_imp_le])
   763 
   764 lemma lemma_trans2:
   765      "[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
   766       ==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
   767 by (blast intro: order_less_trans [THEN order_less_imp_le])
   768 
   769 lemma lemma_trans3:
   770      "[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
   771       ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
   772 by auto
   773 
   774 lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
   775               ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
   776 by (blast intro: order_less_imp_le)
   777 
   778 
   779 text{*Proof is more involved than outlines sketched by various authors
   780  would suggest*}
   781 
   782 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
   783 apply (simp add: Cauchy_def Bseq_def)
   784 apply (drule_tac x = 1 in spec)
   785 apply (erule zero_less_one [THEN [2] impE], safe)
   786 apply (drule_tac x = M in spec, simp)
   787 apply (drule lemmaCauchy)
   788 apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
   789 apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
   790 apply safe
   791 apply (drule lemma_trans1, assumption)
   792 apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
   793 apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
   794 apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
   795 apply (drule lemma_trans4)
   796 apply (drule_tac [2] lemma_trans4)
   797 apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
   798 apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
   799 apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
   800 apply (auto elim!: lemma_Nat_covered)
   801 done
   802 
   803 text{*A Cauchy sequence is bounded -- nonstandard version*}
   804 
   805 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
   806 by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
   807 
   808 
   809 text{*Equivalence of Cauchy criterion and convergence:
   810   We will prove this using our NS formulation which provides a
   811   much easier proof than using the standard definition. We do not
   812   need to use properties of subsequences such as boundedness,
   813   monotonicity etc... Compare with Harrison's corresponding proof
   814   in HOL which is much longer and more complicated. Of course, we do
   815   not have problems which he encountered with guessing the right
   816   instantiations for his 'espsilon-delta' proof(s) in this case
   817   since the NS formulations do not involve existential quantifiers.*}
   818 
   819 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
   820 apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
   821 apply (frule NSCauchy_NSBseq)
   822 apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
   823 apply (drule HNatInfinite_whn [THEN [2] bspec])
   824 apply (drule HNatInfinite_whn [THEN [2] bspec])
   825 apply (auto dest!: st_part_Ex simp add: SReal_iff)
   826 apply (blast intro: approx_trans3)
   827 done
   828 
   829 text{*Standard proof for free*}
   830 lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
   831 by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
   832 
   833 
   834 text{*We can now try and derive a few properties of sequences,
   835      starting with the limit comparison property for sequences.*}
   836 
   837 lemma NSLIMSEQ_le:
   838        "[| f ----NS> l; g ----NS> m;
   839            \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
   840                 |] ==> l \<le> m"
   841 apply (simp add: NSLIMSEQ_def, safe)
   842 apply (drule starfun_le_mono)
   843 apply (drule HNatInfinite_whn [THEN [2] bspec])+
   844 apply (drule_tac x = whn in spec)
   845 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   846 apply clarify
   847 apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   848 done
   849 
   850 (* standard version *)
   851 lemma LIMSEQ_le:
   852      "[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
   853       ==> l \<le> m"
   854 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
   855 
   856 lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   857 apply (rule LIMSEQ_le)
   858 apply (rule LIMSEQ_const, auto)
   859 done
   860 
   861 lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   862 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
   863 
   864 lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   865 apply (rule LIMSEQ_le)
   866 apply (rule_tac [2] LIMSEQ_const, auto)
   867 done
   868 
   869 lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   870 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
   871 
   872 text{*Shift a convergent series by 1:
   873   By the equivalence between Cauchiness and convergence and because
   874   the successor of an infinite hypernatural is also infinite.*}
   875 
   876 lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
   877 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   878 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
   879 apply (drule bspec, assumption)
   880 apply (drule bspec, assumption)
   881 apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
   882 apply (blast intro: approx_trans3)
   883 done
   884 
   885 text{* standard version *}
   886 lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
   887 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
   888 
   889 lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
   890 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   891 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
   892 apply (drule bspec, assumption)
   893 apply (drule bspec, assumption)
   894 apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
   895 apply (drule_tac x="N - 1" in bspec) 
   896 apply (auto intro: approx_trans3)
   897 done
   898 
   899 lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
   900 apply (simp add: LIMSEQ_NSLIMSEQ_iff)
   901 apply (erule NSLIMSEQ_imp_Suc)
   902 done
   903 
   904 lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
   905 by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
   906 
   907 lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
   908 by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   909 
   910 text{*A sequence tends to zero iff its abs does*}
   911 lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
   912 by (simp add: LIMSEQ_def)
   913 
   914 text{*We prove the NS version from the standard one, since the NS proof
   915    seems more complicated than the standard one above!*}
   916 lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
   917 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
   918 
   919 text{*Generalization to other limits*}
   920 lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
   921 apply (simp add: NSLIMSEQ_def)
   922 apply (auto intro: approx_hrabs 
   923             simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric])
   924 done
   925 
   926 text{* standard version *}
   927 lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
   928 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
   929 
   930 text{*An unbounded sequence's inverse tends to 0*}
   931 
   932 text{* standard proof seems easier *}
   933 lemma LIMSEQ_inverse_zero:
   934       "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
   935 apply (simp add: LIMSEQ_def, safe)
   936 apply (drule_tac x = "inverse r" in spec, safe)
   937 apply (rule_tac x = N in exI, safe)
   938 apply (drule spec, auto)
   939 apply (frule positive_imp_inverse_positive)
   940 apply (frule order_less_trans, assumption)
   941 apply (frule_tac a = "f n" in positive_imp_inverse_positive)
   942 apply (simp add: abs_if) 
   943 apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
   944 apply (auto intro: inverse_less_iff_less [THEN iffD2]
   945             simp del: inverse_inverse_eq)
   946 done
   947 
   948 lemma NSLIMSEQ_inverse_zero:
   949      "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
   950       ==> (%n. inverse(f n)) ----NS> 0"
   951 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   952 
   953 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
   954 
   955 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
   956 apply (rule LIMSEQ_inverse_zero, safe)
   957 apply (cut_tac x = y in reals_Archimedean2)
   958 apply (safe, rule_tac x = n in exI)
   959 apply (auto simp add: real_of_nat_Suc)
   960 done
   961 
   962 lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
   963 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
   964 
   965 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
   966 infinity is now easily proved*}
   967 
   968 lemma LIMSEQ_inverse_real_of_nat_add:
   969      "(%n. r + inverse(real(Suc n))) ----> r"
   970 by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
   971 
   972 lemma NSLIMSEQ_inverse_real_of_nat_add:
   973      "(%n. r + inverse(real(Suc n))) ----NS> r"
   974 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
   975 
   976 lemma LIMSEQ_inverse_real_of_nat_add_minus:
   977      "(%n. r + -inverse(real(Suc n))) ----> r"
   978 by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
   979 
   980 lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
   981      "(%n. r + -inverse(real(Suc n))) ----NS> r"
   982 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
   983 
   984 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
   985      "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
   986 by (cut_tac b=1 in
   987         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
   988 
   989 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
   990      "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
   991 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
   992 
   993 
   994 text{* Real Powers*}
   995 
   996 lemma NSLIMSEQ_pow [rule_format]:
   997      "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
   998 apply (induct_tac "m")
   999 apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
  1000 done
  1001 
  1002 lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
  1003 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
  1004 
  1005 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
  1006 "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
  1007   also fact that bounded and monotonic sequence converges.*}
  1008 
  1009 lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
  1010 apply (simp add: Bseq_def)
  1011 apply (rule_tac x = 1 in exI)
  1012 apply (simp add: power_abs)
  1013 apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
  1014 done
  1015 
  1016 lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
  1017 apply (clarify intro!: mono_SucI2)
  1018 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
  1019 done
  1020 
  1021 lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
  1022 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
  1023 
  1024 text{* We now use NS criterion to bring proof of theorem through *}
  1025 
  1026 lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
  1027 apply (simp add: NSLIMSEQ_def)
  1028 apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
  1029 apply (frule NSconvergentD)
  1030 apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow)
  1031 apply (frule HNatInfinite_add_one)
  1032 apply (drule bspec, assumption)
  1033 apply (drule bspec, assumption)
  1034 apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
  1035 apply (simp add: hyperpow_add)
  1036 apply (drule approx_mult_subst_SReal, assumption)
  1037 apply (drule approx_trans3, assumption)
  1038 apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric])
  1039 done
  1040 
  1041 text{* standard version *}
  1042 lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
  1043 by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
  1044 
  1045 lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
  1046 apply (cut_tac a = a and x1 = "inverse x" in
  1047         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
  1048 apply (auto simp add: divide_inverse power_inverse)
  1049 apply (simp add: inverse_eq_divide pos_divide_less_eq)
  1050 done
  1051 
  1052 text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
  1053 
  1054 lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
  1055 by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
  1056 
  1057 lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
  1058 by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
  1059 
  1060 lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
  1061 apply (rule LIMSEQ_rabs_zero [THEN iffD1])
  1062 apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
  1063 done
  1064 
  1065 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
  1066 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
  1067 
  1068 subsection{*Hyperreals and Sequences*}
  1069 
  1070 text{*A bounded sequence is a finite hyperreal*}
  1071 lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
  1072 by (auto intro!: bexI lemma_hyprel_refl 
  1073             intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
  1074             simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
  1075                       Bseq_iff1a)
  1076 
  1077 text{*A sequence converging to zero defines an infinitesimal*}
  1078 lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
  1079       "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
  1080 apply (simp add: NSLIMSEQ_def)
  1081 apply (drule_tac x = whn in bspec)
  1082 apply (simp add: HNatInfinite_whn)
  1083 apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat)
  1084 done
  1085 
  1086 (***---------------------------------------------------------------
  1087     Theorems proved by Harrison in HOL that we do not need
  1088     in order to prove equivalence between Cauchy criterion
  1089     and convergence:
  1090  -- Show that every sequence contains a monotonic subsequence
  1091 Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
  1092  -- Show that a subsequence of a bounded sequence is bounded
  1093 Goal "Bseq X ==> Bseq (%n. X (f n))";
  1094  -- Show we can take subsequential terms arbitrarily far
  1095     up a sequence
  1096 Goal "subseq f ==> n \<le> f(n)";
  1097 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
  1098  ---------------------------------------------------------------***)
  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 *}
  1219 
  1220 
  1221 end
  1222