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