# HG changeset patch
# User paulson
# Date 1091024787 -7200
# Node ID 6c3276a2735b2aa2be759e1ae738bf60d156a293
# Parent  32402f5624d132973221aa14c40ee6eb1cb12ae3
conversion of SEQ.ML to Isar script

diff -r 32402f5624d1 -r 6c3276a2735b src/HOL/Hyperreal/Integration.ML
--- a/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:25:40 2004 +0200
+++ b/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:26:27 2004 +0200
@@ -10,6 +10,13 @@
 fun ARITH_PROVE str = prove_goal thy str
                       (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
 
+fun CLAIM_SIMP str thms =
+               prove_goal (the_context()) str
+               (fn prems => [cut_facts_tac prems 1,
+                   auto_tac (claset(),simpset() addsimps thms)]);
+
+fun CLAIM str = CLAIM_SIMP str [];
+
 Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
 by Auto_tac;
 qed "partition_zero";
diff -r 32402f5624d1 -r 6c3276a2735b src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Wed Jul 28 16:25:40 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1345 +0,0 @@
-(*  Title       : SEQ.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Description : Theory of sequence and series of real numbers
-*) 
-
-val Nats_1 = thm"Nats_1";
-
-fun CLAIM_SIMP str thms =
-               prove_goal (the_context()) str
-               (fn prems => [cut_facts_tac prems 1,
-                   auto_tac (claset(),simpset() addsimps thms)]);
-
-fun CLAIM str = CLAIM_SIMP str [];
-
-(*---------------------------------------------------------------------------
-   Example of an hypersequence (i.e. an extended standard sequence) 
-   whose term with an hypernatural suffix is an infinitesimal i.e. 
-   the whn'nth term of the hypersequence is a member of Infinitesimal 
- -------------------------------------------------------------------------- *)
-
-Goalw [hypnat_omega_def] 
-      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
-by (auto_tac (claset(),
-      simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by (auto_tac (claset(),
-              simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2,
-                            FreeUltrafilterNat_inverse_real_of_posnat]));
-qed "SEQ_Infinitesimal";
-
-(*--------------------------------------------------------------------------
-                  Rules for LIMSEQ and NSLIMSEQ etc.
- --------------------------------------------------------------------------*)
-
-Goalw [LIMSEQ_def] 
-      "(X ----> L) = \
-\      (ALL r. 0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
-by (Simp_tac 1);
-qed "LIMSEQ_iff";
-
-Goalw [NSLIMSEQ_def] 
-    "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)";
-by (Simp_tac 1);
-qed "NSLIMSEQ_iff";
-
-(*----------------------------------------
-          LIMSEQ ==> NSLIMSEQ
- ---------------------------------------*)
-Goalw [LIMSEQ_def,NSLIMSEQ_def] 
-      "X ----> L ==> X ----NS> L";
-by (auto_tac (claset(),simpset() addsimps 
-    [HNatInfinite_FreeUltrafilterNat_iff]));
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (rtac (approx_minus_iff RS iffD2) 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    mem_infmal_iff RS sym,hypreal_of_real_def,
-    hypreal_minus,hypreal_add,
-    Infinitesimal_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
-by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1);
-by (dres_inst_tac [("x","no")] spec 1);
-by (Fuf_tac 1);
-by (blast_tac (claset() addDs [less_imp_le]) 1);
-qed "LIMSEQ_NSLIMSEQ";
-
-(*-------------------------------------------------------------
-          NSLIMSEQ ==> LIMSEQ
-    proving NS def ==> Standard def is trickier as usual 
- -------------------------------------------------------------*)
-(* the following sequence f(n) defines a hypernatural *)
-(* lemmas etc. first *)
-Goal "!!(f::nat=>nat). ALL n. n <= f n \
-\          ==> {n. f n = 0} = {0} | {n. f n = 0} = {}";
-by (Auto_tac);
-by (dres_inst_tac [("x","xa")] spec 1);
-by (dres_inst_tac [("x","x")] spec 2);
-by (Auto_tac);
-qed "lemma_NSLIMSEQ1";
-
-Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
-by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
-qed "lemma_NSLIMSEQ2";
-
-Goal "!!(f::nat=>nat). ALL n. n <= f n \
-\          ==> {n. f n = Suc u} <= {n. n <= Suc u}";
-by (Auto_tac);
-by (dres_inst_tac [("x","x")] spec 1);
-by (Auto_tac);
-qed "lemma_NSLIMSEQ3";
-
-Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
-\         ==> finite {n. f n <= u}";
-by (induct_tac "u" 1);
-by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
-by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
-    rewrite_rule [atMost_def] finite_atMost], simpset()));
-by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
-by (ALLGOALS(Asm_simp_tac));
-qed "NSLIMSEQ_finite_set";
-
-Goal "- {n. u < (f::nat=>nat) n} = {n. f n <= u}";
-by (auto_tac (claset() addDs [less_le_trans],
-    simpset() addsimps [le_def]));
-qed "Compl_less_set";
-
-(* the index set is in the free ultrafilter *)
-Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
-\         ==> {n. u < f n} : FreeUltrafilterNat";
-by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1);
-by (rtac FreeUltrafilterNat_finite 1);
-by (auto_tac (claset() addDs [NSLIMSEQ_finite_set],
-    simpset() addsimps [Compl_less_set]));
-qed "FreeUltrafilterNat_NSLIMSEQ";
-
-(* thus, the sequence defines an infinite hypernatural! *)
-Goal "ALL n. n <= f n \
-\         ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite";
-by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
-by (etac FreeUltrafilterNat_NSLIMSEQ 1);
-qed "HNatInfinite_NSLIMSEQ";
-
-val lemmaLIM = CLAIM  "{n. X (f n) + - L = Y n} Int {n. abs (Y n) < r} <= \
-\         {n. abs (X (f n) + - L) < r}";
-
-Goal "{n. abs (X (f n) + - L) < r} Int {n. r <= abs (X (f n) + - (L::real))} \
-\     = {}";
-by Auto_tac;  
-qed "lemmaLIM2";
-
-Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
-\          ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
-\          - hypreal_of_real  L @= 0 |] ==> False";
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
-    mem_infmal_iff RS sym,hypreal_of_real_def,
-    hypreal_minus,hypreal_add,
-    Infinitesimal_FreeUltrafilterNat_iff]));
-by (rename_tac "Y" 1);
-by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
-by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
-by (dtac FreeUltrafilterNat_all 1);
-by (thin_tac "{n. abs (Y n) < r} : FreeUltrafilterNat" 1);
-by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
-                                  FreeUltrafilterNat_empty]) 1);
-qed "lemmaLIM3";
-
-Goalw [LIMSEQ_def,NSLIMSEQ_def] 
-      "X ----NS> L ==> X ----> L";
-by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
-by (Step_tac 1);
-(* skolemization step *)
-by (dtac choice 1 THEN Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat(hypnatrel``{f})")] bspec 1);
-by (dtac (approx_minus_iff RS iffD1) 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [linorder_not_less])));
-by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
-by (blast_tac (claset() addIs [lemmaLIM3]) 1);
-qed "NSLIMSEQ_LIMSEQ";
-
-(* Now the all important result is trivially proved! *)
-Goal "(f ----> L) = (f ----NS> L)";
-by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1);
-qed "LIMSEQ_NSLIMSEQ_iff";
-
-(*-------------------------------------------------------------------
-                   Theorems about sequences
- ------------------------------------------------------------------*)
-Goalw [NSLIMSEQ_def] "(%n. k) ----NS> k";
-by (Auto_tac);
-qed "NSLIMSEQ_const";
-
-Goalw [LIMSEQ_def] "(%n. k) ----> k";
-by (Auto_tac);
-qed "LIMSEQ_const";
-
-Goalw [NSLIMSEQ_def]
-      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
-by (auto_tac (claset() addIs [approx_add],
-    simpset() addsimps [starfunNat_add RS sym]));
-qed "NSLIMSEQ_add";
-
-Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-                                           NSLIMSEQ_add]) 1);
-qed "LIMSEQ_add";
-
-Goalw [NSLIMSEQ_def]
-      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
-by (auto_tac (claset() addSIs [approx_mult_HFinite],
-    simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
-qed "NSLIMSEQ_mult";
-
-Goal "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-                                           NSLIMSEQ_mult]) 1);
-qed "LIMSEQ_mult";
-
-Goalw [NSLIMSEQ_def] 
-     "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
-by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym]));
-qed "NSLIMSEQ_minus";
-
-Goal "X ----> a ==> (%n. -(X n)) ----> -a";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-                                           NSLIMSEQ_minus]) 1);
-qed "LIMSEQ_minus";
-
-Goal "(%n. -(X n)) ----> -a ==> X ----> a";
-by (dtac LIMSEQ_minus 1);
-by (Asm_full_simp_tac 1);
-qed "LIMSEQ_minus_cancel";
-
-Goal "(%n. -(X n)) ----NS> -a ==> X ----NS> a";
-by (dtac NSLIMSEQ_minus 1);
-by (Asm_full_simp_tac 1);
-qed "NSLIMSEQ_minus_cancel";
-
-Goal "[| X ----NS> a; Y ----NS> b |] \
-\               ==> (%n. X n + -Y n) ----NS> a + -b";
-by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
-by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
-qed "NSLIMSEQ_add_minus";
-
-Goal "[| X ----> a; Y ----> b |] \
-\               ==> (%n. X n + -Y n) ----> a + -b";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_add_minus]) 1);
-qed "LIMSEQ_add_minus";
-
-Goalw [real_diff_def] 
-     "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b";
-by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
-qed "LIMSEQ_diff";
-
-Goalw [real_diff_def] 
-     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b";
-by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
-qed "NSLIMSEQ_diff";
-
-(*---------------------------------------------------------------
-    Proof is like that of NSLIM_inverse.
- --------------------------------------------------------------*)
-Goalw [NSLIMSEQ_def] 
-     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
-by (Clarify_tac 1);
-by (dtac bspec 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [starfunNat_inverse RS sym, 
-                                  hypreal_of_real_approx_inverse]));  
-qed "NSLIMSEQ_inverse";
-
-
-(*------ Standard version of theorem -------*)
-Goal "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)";
-by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse,
-    LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "LIMSEQ_inverse";
-
-Goal "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] \
-\     ==> (%n. X n / Y n) ----NS> a/b";
-by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse, 
-                                           real_divide_def]) 1);
-qed "NSLIMSEQ_mult_inverse";
-
-Goal "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse, 
-                                           real_divide_def]) 1);
-qed "LIMSEQ_divide";
-
-(*-----------------------------------------------
-            Uniqueness of limit
- ----------------------------------------------*)
-Goalw [NSLIMSEQ_def] 
-     "[| X ----NS> a; X ----NS> b |] ==> a = b";
-by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
-by (auto_tac (claset() addDs [approx_trans3], simpset()));
-qed "NSLIMSEQ_unique";
-
-Goal "[| X ----> a; X ----> b |] ==> a = b";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_unique]) 1);
-qed "LIMSEQ_unique";
-
-(*-----------------------------------------------------------------
-    theorems about nslim and lim
- ----------------------------------------------------------------*)
-Goalw [lim_def] "X ----> L ==> lim X = L";
-by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
-qed "limI";
-
-Goalw [nslim_def] "X ----NS> L ==> nslim X = L";
-by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
-qed "nslimI";
-
-Goalw [lim_def,nslim_def] "lim X = nslim X";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "lim_nslim_iff";
-
-(*------------------------------------------------------------------
-                      Convergence
- -----------------------------------------------------------------*)
-Goalw [convergent_def]
-     "convergent X ==> EX L. (X ----> L)";
-by (assume_tac 1);
-qed "convergentD";
-
-Goalw [convergent_def]
-     "(X ----> L) ==> convergent X";
-by (Blast_tac 1);
-qed "convergentI";
-
-Goalw [NSconvergent_def]
-     "NSconvergent X ==> EX L. (X ----NS> L)";
-by (assume_tac 1);
-qed "NSconvergentD";
-
-Goalw [NSconvergent_def]
-     "(X ----NS> L) ==> NSconvergent X";
-by (Blast_tac 1);
-qed "NSconvergentI";
-
-Goalw [convergent_def,NSconvergent_def] 
-     "convergent X = NSconvergent X";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "convergent_NSconvergent_iff";
-
-Goalw [NSconvergent_def,nslim_def] 
-     "NSconvergent X = (X ----NS> nslim X)";
-by (auto_tac (claset() addIs [someI], simpset()));
-qed "NSconvergent_NSLIMSEQ_iff";
-
-Goalw [convergent_def,lim_def] 
-     "convergent X = (X ----> lim X)";
-by (auto_tac (claset() addIs [someI], simpset()));
-qed "convergent_LIMSEQ_iff";
-
-(*-------------------------------------------------------------------
-         Subsequence (alternative definition) (e.g. Hoskins)
- ------------------------------------------------------------------*)
-Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
-by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
-by (induct_tac "k" 1);
-by (auto_tac (claset() addIs [less_trans], simpset()));
-qed "subseq_Suc_iff";
-
-(*-------------------------------------------------------------------
-                   Monotonicity
- ------------------------------------------------------------------*)
-
-Goalw [monoseq_def]
-   "monoseq X = ((ALL n. X n <= X (Suc n)) \
-\                | (ALL n. X (Suc n) <= X n))";
-by (auto_tac (claset () addSDs [le_imp_less_or_eq], simpset()));
-by (auto_tac (claset() addSIs [lessI RS less_imp_le]
-                       addSDs [less_imp_Suc_add], 
-    simpset()));
-by (induct_tac "ka" 1);
-by (auto_tac (claset() addIs [order_trans], simpset()));
-by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
-by (induct_tac "k" 1);
-by (auto_tac (claset() addIs [order_trans], simpset()));
-qed "monoseq_Suc";
-
-Goalw [monoseq_def] 
-       "ALL m n. m <= n --> X m <= X n ==> monoseq X";
-by (Blast_tac 1);
-qed "monoI1";
-
-Goalw [monoseq_def] 
-       "ALL m n. m <= n --> X n <= X m ==> monoseq X";
-by (Blast_tac 1);
-qed "monoI2";
-
-Goal "ALL n. X n <= X (Suc n) ==> monoseq X";
-by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
-qed "mono_SucI1";
-
-Goal "ALL n. X (Suc n) <= X n ==> monoseq X";
-by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
-qed "mono_SucI2";
-
-(*-------------------------------------------------------------------
-                  Bounded Sequence
- ------------------------------------------------------------------*)
-Goalw [Bseq_def] 
-      "Bseq X ==> EX K. 0 < K & (ALL n. abs(X n) <= K)";
-by (assume_tac 1);
-qed "BseqD";
-
-Goalw [Bseq_def]
-      "[| 0 < K; ALL n. abs(X n) <= K |] ==> Bseq X";
-by (Blast_tac 1);
-qed "BseqI";
-
-Goal "(EX K. 0 < K & (ALL n. abs(X n) <= K)) = \
-\     (EX N. ALL n. abs(X n) <= real(Suc N))";
-by Auto_tac;
-by (Force_tac 2);
-by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
-by (Clarify_tac 1); 
-by (res_inst_tac [("x","n")] exI 1); 
-by (Clarify_tac 1); 
-by (dres_inst_tac [("x","na")] spec 1); 
-by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
-qed "lemma_NBseq_def";
-
-(* alternative definition for Bseq *)
-Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real(Suc N))";
-by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
-qed "Bseq_iff";
-
-Goal "(EX K. 0 < K & (ALL n. abs(X n) <= K)) = \
-\     (EX N. ALL n. abs(X n) < real(Suc N))";
-by (stac lemma_NBseq_def 1); 
-by Auto_tac;
-by (res_inst_tac [("x","Suc N")] exI 1); 
-by (res_inst_tac [("x","N")] exI 2); 
-by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
-by (blast_tac (claset() addIs [order_less_imp_le]) 2);
-by (dres_inst_tac [("x","n")] spec 1); 
-by (Asm_simp_tac 1); 
-qed "lemma_NBseq_def2";
-
-(* yet another definition for Bseq *)
-Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real(Suc N))";
-by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
-qed "Bseq_iff1a";
-
-Goalw [NSBseq_def]
-     "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite";
-by (Blast_tac 1);
-qed "NSBseqD";
-
-Goalw [NSBseq_def]
-     "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X";
-by (assume_tac 1);
-qed "NSBseqI";
-
-(*-----------------------------------------------------------
-       Standard definition ==> NS definition
- ----------------------------------------------------------*)
-(* a few lemmas *)
-Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
-by (Auto_tac);
-qed "lemma_Bseq";
-
-Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
-by (Step_tac 1);
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
-              simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff,
-                                  HNatInfinite_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
-by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
-by (res_inst_tac [("x","K+1")] exI 1);
-by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1);
-by (Ultra_tac 1);
-qed "Bseq_NSBseq";
-
-(*---------------------------------------------------------------
-       NS  definition ==> Standard definition
- ---------------------------------------------------------------*)
-(* similar to NSLIM proof in REALTOPOS *)
-(*------------------------------------------------------------------- 
-   We need to get rid of the real variable and do so by proving the
-   following which relies on the Archimedean property of the reals
-   When we skolemize we then get the required function f::nat=>nat 
-   o/w we would be stuck with a skolem function f :: real=>nat which
-   is not what we want (read useless!)
- -------------------------------------------------------------------*)
- 
-Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
-\          ==> ALL N. EX n. real(Suc N) < abs (X n)";
-by (Step_tac 1);
-by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
-by (Blast_tac 1);
-qed "lemmaNSBseq";
-
-Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
-\         ==> EX f. ALL N. real(Suc N) < abs (X (f N))";
-by (dtac lemmaNSBseq 1);
-by (dtac choice 1);
-by (Blast_tac 1);
-qed "lemmaNSBseq2";
-
-Goal "ALL N. real(Suc N) < abs (X (f N)) \
-\         ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite";
-by (auto_tac (claset(),
-              simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
-by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
-by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
-by (dtac FreeUltrafilterNat_all 1);
-by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); 
-by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
-qed "real_seq_to_hypreal_HInfinite";
-
-(*-----------------------------------------------------------------------------
-     Now prove that we can get out an infinite hypernatural as well 
-     defined using the skolem function f::nat=>nat above
- ----------------------------------------------------------------------------*)
-
-Goal "{n. f n <= Suc u & real(Suc n) < abs (X (f n))} <= \
-\         {n. f n <= u & real(Suc n) < abs (X (f n))} \
-\         Un {n. real(Suc n) < abs (X (Suc u))}";
-by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
-qed "lemma_finite_NSBseq";
-
-Goal "finite {n. f n <= (u::nat) &  real(Suc n) < abs(X(f n))}";
-by (induct_tac "u" 1);
-by (res_inst_tac [("B","{n. real(Suc n) < abs(X 0)}")] finite_subset 1);
-by (Force_tac 1); 
-by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
-by (auto_tac (claset() addIs [finite_real_of_nat_less_real], 
-              simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym]));
-qed "lemma_finite_NSBseq2";
-
-Goal "ALL N. real(Suc N) < abs (X (f N)) \
-\     ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
-by (auto_tac (claset(),
-              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
-by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
-by (asm_full_simp_tac (simpset() addsimps 
-   [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
-\   = {n. f n <= u}" [le_def]]) 1);
-by (dtac FreeUltrafilterNat_all 1);
-by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (auto_tac (claset(), 
-     simpset() addsimps 
-    [CLAIM "({n. f n <= u} Int {n. real(Suc n) < abs(X(f n))}) = \
-\          {n. f n <= (u::nat) &  real(Suc n) < abs(X(f n))}",
-     lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
-qed "HNatInfinite_skolem_f";
-
-Goalw [Bseq_def,NSBseq_def] 
-      "NSBseq X ==> Bseq X";
-by (rtac ccontr 1);
-by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
-by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
-by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
-by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff]));
-qed "NSBseq_Bseq";
-
-(*----------------------------------------------------------------------
-  Equivalence of nonstandard and standard definitions 
-  for a bounded sequence
- -----------------------------------------------------------------------*)
-Goal "(Bseq X) = (NSBseq X)";
-by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1);
-qed "Bseq_NSBseq_iff";
-
-(*----------------------------------------------------------------------
-   A convergent sequence is bounded
-   (Boundedness as a necessary condition for convergence)
- -----------------------------------------------------------------------*)
-(* easier --- nonstandard version - no existential as usual *)
-Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
-          "NSconvergent X ==> NSBseq X";
-by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
-               (approx_sym RSN (2,approx_HFinite))]) 1);
-qed "NSconvergent_NSBseq";
-
-(* standard version - easily now proved using *)
-(* equivalence of NS and standard definitions *)
-Goal "convergent X ==> Bseq X";
-by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
-    convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
-qed "convergent_Bseq";
-
-(*----------------------------------------------------------------------
-             Results about Ubs and Lubs of bounded sequences
- -----------------------------------------------------------------------*)
-Goalw [Bseq_def]
-  "!!(X::nat=>real). Bseq X ==> \
-\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
-by (auto_tac (claset() addIs [isUbI,setleI],
-    simpset() addsimps [abs_le_interval_iff]));
-qed "Bseq_isUb";
-
-(*----------------------------------------------------------------------
-   Use completeness of reals (supremum property) 
-   to show that any bounded sequence has a lub 
------------------------------------------------------------------------*)
-Goal
-  "!!(X::nat=>real). Bseq X ==> \
-\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
-by (blast_tac (claset() addIs [reals_complete,
-    Bseq_isUb]) 1);
-qed "Bseq_isLub";
-
-(* nonstandard version of premise will be *)
-(* handy when we work in NS universe      *)
-Goal   "NSBseq X ==> \
-\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
-by (asm_full_simp_tac (simpset() addsimps 
-    [Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
-qed "NSBseq_isUb";
-
-Goal
-  "NSBseq X ==> \
-\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
-by (asm_full_simp_tac (simpset() addsimps 
-    [Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
-qed "NSBseq_isLub";
-
-(*--------------------------------------------------------------------
-             Bounded and monotonic sequence converges              
- --------------------------------------------------------------------*)
-(* lemmas *)
-Goal 
-     "!!(X::nat=>real). [| ALL m n. m <= n -->  X m <= X n; \
-\                 isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \
-\              |] ==> ALL n. ma <= n --> X n = X ma";
-by (Step_tac 1);
-by (dres_inst_tac [("y","X n")] isLubD2 1);
-by (ALLGOALS(blast_tac (claset() addDs [order_antisym])));
-qed "lemma_converg1";
-
-(*------------------------------------------------------------------- 
-   The best of both world: Easier to prove this result as a standard
-   theorem and then use equivalence to "transfer" it into the
-   equivalent nonstandard form if needed!
- -------------------------------------------------------------------*)
-Goalw [LIMSEQ_def] 
-         "ALL n. m <= n --> X n = X m \
-\         ==> EX L. (X ----> L)";  
-by (res_inst_tac [("x","X m")] exI 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","m")] exI 1);
-by (Step_tac 1);
-by (dtac spec 1 THEN etac impE 1);
-by (Auto_tac);
-qed "Bmonoseq_LIMSEQ";
-
-(* Now same theorem in terms of NS limit *)
-Goal "ALL n. m <= n --> X n = X m \
-\         ==> EX L. (X ----NS> L)";  
-by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
-    simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
-qed "Bmonoseq_NSLIMSEQ";
-
-(* a few more lemmas *)
-Goal "!!(X::nat=>real). \
-\ [| ALL m. X m ~= U;  isLub UNIV {x. EX n. X n = x} U |] ==> ALL m. X m < U";
-by (Step_tac 1);
-by (dres_inst_tac [("y","X m")] isLubD2 1);
-by (auto_tac (claset() addSDs [order_le_imp_less_or_eq],
-              simpset()));
-qed "lemma_converg2";
-
-Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
-\         isUb UNIV {x. EX n. X n = x} U";
-by (rtac (setleI RS isUbI) 1);
-by (Auto_tac);
-qed "lemma_converg3";
-
-(* FIXME: U - T < U redundant *)
-Goal "!!(X::nat=> real). \
-\              [| ALL m. X m ~= U; \
-\                 isLub UNIV {x. EX n. X n = x} U; \
-\                 0 < T; \
-\                 U + - T < U \
-\              |] ==> EX m. U + -T < X m & X m < U";
-by (dtac lemma_converg2 1 THEN assume_tac 1);
-by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
-by (dtac lemma_converg3 1);
-by (dtac isLub_le_isUb 1 THEN assume_tac 1);
-by (auto_tac (claset() addDs [order_less_le_trans],
-              simpset()));
-qed "lemma_converg4";
-
-(*-------------------------------------------------------------------
-  A standard proof of the theorem for monotone increasing sequence
- ------------------------------------------------------------------*)
-
-Goalw [convergent_def] 
-     "[| Bseq X; ALL m n. m <= n --> X m <= X n |] \
-\                ==> convergent X";
-by (ftac Bseq_isLub 1);
-by (Step_tac 1);
-by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
-by (blast_tac (claset() addDs [lemma_converg1,
-    Bmonoseq_LIMSEQ]) 1);
-(* second case *)
-by (res_inst_tac [("x","U")] exI 1);
-by (stac LIMSEQ_iff 1 THEN Step_tac 1);
-by (ftac lemma_converg2 1 THEN assume_tac 1);
-by (dtac lemma_converg4 1 THEN Auto_tac);
-by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
-by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
-by (rotate_tac 3 1 THEN dres_inst_tac [("x","n")] spec 1);
-by (arith_tac 1);
-qed "Bseq_mono_convergent";
-
-(* NS version of theorem *)
-Goalw [convergent_def] 
-     "[| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
-\                ==> NSconvergent X";
-by (auto_tac (claset() addIs [Bseq_mono_convergent], 
-    simpset() addsimps [convergent_NSconvergent_iff RS sym,
-    Bseq_NSBseq_iff RS sym]));
-qed "NSBseq_mono_NSconvergent";
-
-Goalw [convergent_def] 
-      "(convergent X) = (convergent (%n. -(X n)))";
-by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
-by (dtac LIMSEQ_minus 1 THEN Auto_tac);
-qed "convergent_minus_iff";
-
-Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
-by (Asm_full_simp_tac 1);
-qed "Bseq_minus_iff";
-
-(*--------------------------------
-   **** main mono theorem ****
- -------------------------------*)
-Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
-by (Step_tac 1);
-by (stac convergent_minus_iff 2);
-by (dtac (Bseq_minus_iff RS ssubst) 2);
-by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
-qed "Bseq_monoseq_convergent";
-
-(*----------------------------------------------------------------
-          A few more equivalence theorems for boundedness 
- ---------------------------------------------------------------*)
- 
-(***--- alternative formulation for boundedness---***)
-Goalw [Bseq_def] 
-   "Bseq X = (EX k x. 0 < k & (ALL n. abs(X(n) + -x) <= k))";
-by (Step_tac 1);
-by (res_inst_tac [("x","k + abs(x)")] exI 2);
-by (res_inst_tac [("x","K")] exI 1);
-by (res_inst_tac [("x","0")] exI 1);
-by (Auto_tac);
-by (ALLGOALS (dres_inst_tac [("x","n")] spec));
-by (ALLGOALS arith_tac);
-qed "Bseq_iff2";
-
-(***--- alternative formulation for boundedness ---***)
-Goal "Bseq X = (EX k N. 0 < k & (ALL n. abs(X(n) + -X(N)) <= k))";
-by (Step_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","K + abs(X N)")] exI 1);
-by (Auto_tac);
-by (arith_tac 1);
-by (res_inst_tac [("x","N")] exI 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n")] spec 1);
-by (arith_tac 1);
-by (auto_tac (claset(), simpset() addsimps [Bseq_iff2]));
-qed "Bseq_iff3";
-
-Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
-by (res_inst_tac [("x","(abs(k) + abs(K)) + 1")] exI 1);
-by (Auto_tac);
-by (dres_inst_tac [("x","n")] spec 2);
-by (ALLGOALS arith_tac);
-qed "BseqI2";
-
-(*-------------------------------------------------------------------
-   Equivalence between NS and standard definitions of Cauchy seqs
- ------------------------------------------------------------------*)
-(*-------------------------------
-      Standard def => NS def
- -------------------------------*)
-Goal "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite \
-\         ==> {n. M <= x n} : FreeUltrafilterNat";
-by (auto_tac (claset(),
-              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
-by (dres_inst_tac [("x","M")] spec 1);
-by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
-qed "lemmaCauchy1";
-
-Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
-\     {n. M <= xa n} Int {n. M <= x n} <= \
-\     {n. abs (X (xa n) + - X (x n)) < u}";
-by (Blast_tac 1);
-qed "lemmaCauchy2";
-
-Goalw [Cauchy_def,NSCauchy_def] 
-      "Cauchy X ==> NSCauchy X";
-by (Step_tac 1);
-by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (rtac (approx_minus_iff RS iffD2) 1);
-by (rtac (mem_infmal_iff RS iffD1) 1);
-by (auto_tac (claset(),
-              simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
-                                  Infinitesimal_FreeUltrafilterNat_iff]));
-by (EVERY[rtac bexI 1, Auto_tac]);
-by (dtac spec 1 THEN Auto_tac);
-by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
-by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
-by (res_inst_tac [("x1","xa")] 
-    (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
-by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
-by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
-        FreeUltrafilterNat_Nat_set], simpset()));
-qed "Cauchy_NSCauchy";
-
-(*-----------------------------------------------
-     NS def => Standard def -- rather long but 
-     straightforward proof in this case
- ---------------------------------------------*)
-Goalw [Cauchy_def,NSCauchy_def] 
-      "NSCauchy X ==> Cauchy X";
-by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
-by (dtac choice 1 THEN 
-    auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
-by (dtac choice 1 THEN 
-    step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
-by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
-by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {fa})")] bspec 1 
-    THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
-by (dtac (approx_minus_iff RS iffD1) 1);
-by (dtac (mem_infmal_iff RS iffD2) 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
-    hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
-by (rename_tac "Y" 1);
-by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
-by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
-\         {n. abs (Y n) < e} <= \
-\         {n. abs (X (f n) + - X (fa n)) < e}" RSN 
-          (2,FreeUltrafilterNat_subset)) 1);
-by (thin_tac "{n. abs (Y n) < e} : FreeUltrafilterNat" 1);
-by (dtac FreeUltrafilterNat_all 1);
-by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps 
-    [CLAIM "{n. abs (X (f n) + - X (fa n)) < e} Int \
-\         {M. ~ abs (X (f M) + - X (fa M)) < e} = {}",
-     FreeUltrafilterNat_empty]) 1);
-qed "NSCauchy_Cauchy";
-
-(*----- Equivalence -----*)
-Goal "NSCauchy X = Cauchy X";
-by (blast_tac (claset() addSIs[NSCauchy_Cauchy,
-    Cauchy_NSCauchy]) 1);
-qed "NSCauchy_Cauchy_iff";
-
-(*-------------------------------------------------------
-  Cauchy sequence is bounded -- this is the standard 
-  proof mechanization rather than the nonstandard proof 
- -------------------------------------------------------*)
-
-(***-------------  VARIOUS LEMMAS --------------***)
-Goal "ALL n. M <= n --> abs (X M + - X n) < (1::real) \
-\         ==>  ALL n. M <= n --> abs(X n) < 1 + abs(X M)";
-by (Step_tac 1);
-by (dtac spec 1 THEN Auto_tac);
-by (arith_tac 1);
-qed "lemmaCauchy";
-
-Goal "(n < Suc M) = (n <= M)";
-by Auto_tac;
-qed "less_Suc_cancel_iff";
-
-(* FIXME: Long. Maximal element in subsequence *)
-Goal "EX m. m <= M & (ALL n. n <= M --> \
-\         abs ((X::nat=> real) n) <= abs (X m))";
-by (induct_tac "M" 1);
-by (res_inst_tac [("x","0")] exI 1);
-by (Asm_full_simp_tac 1);
-by (Step_tac 1);
-by (cut_inst_tac [("x","abs (X (Suc n))"),("y","abs(X m)")]
-        linorder_less_linear 1);
-by (Step_tac 1);
-by (res_inst_tac [("x","m")] exI 1);
-by (res_inst_tac [("x","m")] exI 2);
-by (res_inst_tac [("x","Suc n")] exI 3);
-by (ALLGOALS(Asm_full_simp_tac));
-by (Step_tac 1);
-by (ALLGOALS(eres_inst_tac [("m1","na")] 
-    (le_imp_less_or_eq RS disjE)));
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
-    [less_Suc_cancel_iff, order_less_imp_le])));
-by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
-qed "SUP_rabs_subseq";
-
-(* lemmas to help proof - mostly trivial *)
-Goal "[| ALL m::nat. m <= M --> P M m; \
-\        ALL m. M <= m --> P M m |] \
-\     ==> ALL m. P M m";
-by (Step_tac 1);
-by (REPEAT(dres_inst_tac [("x","m")] spec 1));
-by (auto_tac (claset() addEs [less_asym],
-    simpset() addsimps [le_def]));
-qed "lemma_Nat_covered";
-
-Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a;  a < b |] \
-\     ==> ALL n. n <= M --> abs(X n) <= b";
-by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
-qed "lemma_trans1";
-
-Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
-\        a < b |] \
-\     ==> ALL n. M <= n --> abs(X n)<= b";
-by (blast_tac (claset() addIs [order_less_trans RS order_less_imp_le]) 1);
-qed "lemma_trans2";
-
-Goal "[| ALL n. n <= M --> abs (X n) <= a; \
-\        a = b |] \
-\     ==> ALL n. n <= M --> abs(X n) <= b";
-by (Auto_tac);
-qed "lemma_trans3";
-
-Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
-\             ==>  ALL n. M <= n --> abs (X n) <= a";
-by (blast_tac (claset() addIs [order_less_imp_le]) 1);
-qed "lemma_trans4";
-
-(*---------------------------------------------------------- 
-   Trickier than expected --- proof is more involved than
-   outlines sketched by various authors would suggest
- ---------------------------------------------------------*)
-Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X";
-by (dres_inst_tac [("x","1")] spec 1);
-by (etac (zero_less_one RSN (2,impE)) 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","M")] spec 1);
-by (Asm_full_simp_tac 1);
-by (dtac lemmaCauchy 1);
-by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
-by (Step_tac 1);
-by (cut_inst_tac [("x","abs(X m)"),
-     ("y","1 + abs(X M)")] linorder_less_linear 1);
-by (Step_tac 1);
-by (dtac lemma_trans1 1 THEN assume_tac 1);
-by (dtac lemma_trans2 3 THEN assume_tac 3);
-by (dtac lemma_trans3 2 THEN assume_tac 2);
-by (dtac (abs_add_one_gt_zero RS order_less_trans) 3);
-by (dtac lemma_trans4 1);
-by (dtac lemma_trans4 2);
-by (res_inst_tac [("x","1 + abs(X M)")] exI 1);
-by (res_inst_tac [("x","1 + abs(X M)")] exI 2);
-by (res_inst_tac [("x","abs(X m)")] exI 3);
-by (auto_tac (claset() addSEs [lemma_Nat_covered],
-              simpset()));
-by (ALLGOALS arith_tac);
-qed "Cauchy_Bseq";
-
-(*------------------------------------------------
-  Cauchy sequence is bounded -- NSformulation
- ------------------------------------------------*)
-Goal "NSCauchy X ==> NSBseq X";
-by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq,
-    Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1);
-qed "NSCauchy_NSBseq";
-
-
-(*-----------------------------------------------------------------
-          Equivalence of Cauchy criterion and convergence
-  
-  We will prove this using our NS formulation which provides a
-  much easier proof than using the standard definition. We do not 
-  need to use properties of subsequences such as boundedness, 
-  monotonicity etc... Compare with Harrison's corresponding proof
-  in HOL which is much longer and more complicated. Of course, we do
-  not have problems which he encountered with guessing the right 
-  instantiations for his 'espsilon-delta' proof(s) in this case
-  since the NS formulations do not involve existential quantifiers.
- -----------------------------------------------------------------*)
-Goalw [NSconvergent_def,NSLIMSEQ_def]
-      "NSCauchy X = NSconvergent X";
-by (Step_tac 1);
-by (ftac NSCauchy_NSBseq 1);
-by (auto_tac (claset() addIs [approx_trans2], 
-    simpset() addsimps 
-    [NSBseq_def,NSCauchy_def]));
-by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
-by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
-by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
-              addsimps [SReal_iff]));
-by (blast_tac (claset() addIs [approx_trans3]) 1);
-qed "NSCauchy_NSconvergent_iff";
-
-(* Standard proof for free *)
-Goal "Cauchy X = convergent X";
-by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym,
-    convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1);
-qed "Cauchy_convergent_iff";
-
-(*-----------------------------------------------------------------
-     We can now try and derive a few properties of sequences
-     starting with the limit comparison property for sequences
- -----------------------------------------------------------------*)
-Goalw [NSLIMSEQ_def]
-       "[| f ----NS> l; g ----NS> m; \
-\                  EX N. ALL n. N <= n --> f(n) <= g(n) \
-\               |] ==> l <= m";
-by (Step_tac 1);
-by (dtac starfun_le_mono 1);
-by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
-by (dres_inst_tac [("x","whn")] spec 1);
-by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
-by Auto_tac;
-by (auto_tac (claset() addIs 
-    [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
-qed "NSLIMSEQ_le";
-
-(* standard version *)
-Goal "[| f ----> l; g ----> m; \
-\        EX N. ALL n. N <= n --> f(n) <= g(n) |] \
-\     ==> l <= m";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_le]) 1);
-qed "LIMSEQ_le";
-
-(*---------------
-    Also...
- --------------*)
-Goal "[| X ----> r; ALL n. a <= X n |] ==> a <= r";
-by (rtac LIMSEQ_le 1);
-by (rtac LIMSEQ_const 1);
-by (Auto_tac);
-qed "LIMSEQ_le_const";
-
-Goal "[| X ----NS> r; ALL n. a <= X n |] ==> a <= r";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    LIMSEQ_le_const]) 1);
-qed "NSLIMSEQ_le_const";
-
-Goal "[| X ----> r; ALL n. X n <= a |] ==> r <= a";
-by (rtac LIMSEQ_le 1);
-by (rtac LIMSEQ_const 2);
-by (Auto_tac);
-qed "LIMSEQ_le_const2";
-
-Goal "[| X ----NS> r; ALL n. X n <= a |] ==> r <= a";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    LIMSEQ_le_const2]) 1);
-qed "NSLIMSEQ_le_const2";
-
-(*-----------------------------------------------------
-            Shift a convergent series by 1
-  We use the fact that Cauchyness and convergence
-  are equivalent and also that the successor of an
-  infinite hypernatural is also infinite.
- -----------------------------------------------------*)
-Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
-by (forward_tac [NSconvergentI RS 
-    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
-by (auto_tac (claset(), 
-     simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
-by (dtac bspec 1 THEN assume_tac 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (dtac (Nats_1 RSN (2,HNatInfinite_SHNat_add)) 1);
-by (blast_tac (claset() addIs [approx_trans3]) 1);
-qed "NSLIMSEQ_Suc";
-
-(* standard version *)
-Goal "f ----> l ==> (%n. f(Suc n)) ----> l";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_Suc]) 1);
-qed "LIMSEQ_Suc";
-
-Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
-by (forward_tac [NSconvergentI RS 
-    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
-by (auto_tac (claset(),
-      simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
-by (dtac bspec 1 THEN assume_tac 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (ftac (Nats_1 RSN (2,HNatInfinite_SHNat_diff)) 1);
-by (rotate_tac 2 1);
-by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
-    simpset()));
-qed "NSLIMSEQ_imp_Suc";
-
-Goal "(%n. f(Suc n)) ----> l ==> f ----> l";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
-by (etac NSLIMSEQ_imp_Suc 1);
-qed "LIMSEQ_imp_Suc";
-
-Goal "((%n. f(Suc n)) ----> l) = (f ----> l)";
-by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1);
-qed "LIMSEQ_Suc_iff";
-
-Goal "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)";
-by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1);
-qed "NSLIMSEQ_Suc_iff";
-
-(*-----------------------------------------------------
-       A sequence tends to zero iff its abs does
- ----------------------------------------------------*)
-(* we can prove this directly since proof is trivial *)
-Goalw [LIMSEQ_def] 
-      "((%n. abs(f n)) ----> 0) = (f ----> 0)";
-by (simp_tac (simpset() addsimps [abs_idempotent]) 1);
-qed "LIMSEQ_rabs_zero";
-
-(*-----------------------------------------------------*)
-(* We prove the NS version from the standard one       *)
-(* Actually pure NS proof seems more complicated       *)
-(* than the direct standard one above!                 *)
-(*-----------------------------------------------------*)
-
-Goal "((%n. abs(f n)) ----NS> 0) = (f ----NS> 0)";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-             LIMSEQ_rabs_zero]) 1);
-qed "NSLIMSEQ_rabs_zero";
-
-(*----------------------------------------
-    Also we have for a general limit 
-        (NS proof much easier)
- ---------------------------------------*)
-Goalw [NSLIMSEQ_def] 
-       "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
-by (auto_tac (claset() addIs [approx_hrabs], simpset() 
-    addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
-qed "NSLIMSEQ_imp_rabs";
-
-(* standard version *)
-Goal "f ----> l ==> (%n. abs(f n)) ----> abs(l)";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_imp_rabs]) 1);
-qed "LIMSEQ_imp_rabs";
-
-(*-----------------------------------------------------
-       An unbounded sequence's inverse tends to 0
-  ----------------------------------------------------*)
-(* standard proof seems easier *)
-Goalw [LIMSEQ_def] 
-      "ALL y. EX N. ALL n. N <= n --> y < f(n) \
-\      ==> (%n. inverse(f n)) ----> 0";
-by (Step_tac 1 THEN Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1);
-by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
-by (dtac spec 1 THEN Auto_tac);
-by (ftac positive_imp_inverse_positive 1);
-by (ftac order_less_trans 1 THEN assume_tac 1);
-by (forw_inst_tac [("a","f n")] positive_imp_inverse_positive 1);
-by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
-by (res_inst_tac [("t","r")] (inverse_inverse_eq RS subst) 1);
-by (auto_tac (claset() addIs [inverse_less_iff_less RS iffD2], 
-            simpset() delsimps [inverse_inverse_eq]));
-qed "LIMSEQ_inverse_zero";
-
-Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
-\     ==> (%n. inverse(f n)) ----NS> 0";
-by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-                  LIMSEQ_inverse_zero]) 1);
-qed "NSLIMSEQ_inverse_zero";
-
-(*--------------------------------------------------------------
-             Sequence  1/n --> 0 as n --> infinity 
- -------------------------------------------------------------*)
-
-Goal "(%n. inverse(real(Suc n))) ----> 0";
-by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1);
-by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
-by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
-qed "LIMSEQ_inverse_real_of_nat";
-
-Goal "(%n. inverse(real(Suc n))) ----NS> 0";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_nat]) 1);
-qed "NSLIMSEQ_inverse_real_of_nat";
-
-(*--------------------------------------------
-    Sequence  r + 1/n --> r as n --> infinity 
-    now easily proved
- --------------------------------------------*)
-Goal "(%n. r + inverse(real(Suc n))) ----> r";
-by (cut_facts_tac
-    [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
-by Auto_tac;
-qed "LIMSEQ_inverse_real_of_nat_add";
-
-Goal "(%n. r + inverse(real(Suc n))) ----NS> r";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_nat_add]) 1);
-qed "NSLIMSEQ_inverse_real_of_nat_add";
-
-(*--------------
-    Also...
- --------------*)
-
-Goal "(%n. r + -inverse(real(Suc n))) ----> r";
-by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
-                   MRS LIMSEQ_add_minus] 1);
-by (Auto_tac);
-qed "LIMSEQ_inverse_real_of_nat_add_minus";
-
-Goal "(%n. r + -inverse(real(Suc n))) ----NS> r";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_nat_add_minus]) 1);
-qed "NSLIMSEQ_inverse_real_of_nat_add_minus";
-
-Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r";
-by (cut_inst_tac [("b","1")] ([LIMSEQ_const,
-    LIMSEQ_inverse_real_of_nat_add_minus] MRS LIMSEQ_mult) 1);
-by (Auto_tac);
-qed "LIMSEQ_inverse_real_of_nat_add_minus_mult";
-
-Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r";
-by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
-    LIMSEQ_inverse_real_of_nat_add_minus_mult]) 1);
-qed "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
-
-(*---------------------------------------------------------------
-                          Real Powers
- --------------------------------------------------------------*)
-Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)";
-by (induct_tac "m" 1);
-by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const],
-    simpset()));
-qed_spec_mp "NSLIMSEQ_pow";
-
-Goal "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
-    NSLIMSEQ_pow]) 1);
-qed "LIMSEQ_pow";
-
-(*----------------------------------------------------------------
-               0 <= x <= 1 ==> (x ^ n ----> 0)
-  Proof will use (NS) Cauchy equivalence for convergence and
-  also fact that bounded and monotonic sequence converges.  
- ---------------------------------------------------------------*)
-Goalw [Bseq_def] "[| 0 <= x; x <= 1 |] ==> Bseq (%n. x ^ n)";
-by (res_inst_tac [("x","1")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [power_abs]) 1);
-by (auto_tac (claset() addDs [power_mono] 
-                       addIs [order_less_imp_le], 
-              simpset() addsimps [abs_if] ));
-qed "Bseq_realpow";
-
-Goal "[| 0 <= x; x <= 1 |] ==> monoseq (%n. x ^ n)";
-by (clarify_tac (claset() addSIs [mono_SucI2]) 1);
-by (cut_inst_tac [("n","n"),("N","Suc n"),("a","x")] power_decreasing 1);
-by Auto_tac;
-qed "monoseq_realpow";
-
-Goal "[| 0 <= x; x <= 1 |] ==> convergent (%n. x ^ n)";
-by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
-                                Bseq_realpow,monoseq_realpow]) 1);
-qed "convergent_realpow";
-
-(* We now use NS criterion to bring proof of theorem through *)
-
-
-Goalw [NSLIMSEQ_def]
-     "[| 0 <= x; x < 1 |] ==> (%n. x ^ n) ----NS> 0";
-by (auto_tac (claset() addSDs [convergent_realpow],
-              simpset() addsimps [convergent_NSconvergent_iff]));
-by (ftac NSconvergentD 1);
-by (auto_tac (claset(),
-        simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
-                            NSCauchy_def, starfunNat_pow]));
-by (ftac HNatInfinite_add_one 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (dtac bspec 1 THEN assume_tac 1);
-by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
-by (dtac approx_mult_subst_SReal 1 THEN assume_tac 1);
-by (dtac approx_trans3 1 THEN assume_tac 1);
-by (auto_tac (claset(),
-              simpset() delsimps [hypreal_of_real_mult]
-			addsimps [hypreal_of_real_mult RS sym]));
-qed "NSLIMSEQ_realpow_zero";
-
-(*---------------  standard version ---------------*)
-Goal "[| 0 <= x; x < 1 |] ==> (%n. x ^ n) ----> 0";
-by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
-                                      LIMSEQ_NSLIMSEQ_iff]) 1);
-qed "LIMSEQ_realpow_zero";
-
-Goal "1 < x ==> (%n. a / (x ^ n)) ----> 0";
-by (cut_inst_tac [("a","a"),("x1","inverse x")] 
-    ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [real_divide_def, power_inverse])); 
-by (asm_simp_tac (simpset() addsimps [inverse_eq_divide,
-                                      pos_divide_less_eq]) 1); 
-qed "LIMSEQ_divide_realpow_zero";
-
-(*----------------------------------------------------------------
-               Limit of c^n for |c| < 1  
- ---------------------------------------------------------------*)
-Goal "abs(c) < 1 ==> (%n. abs(c) ^ n) ----> 0";
-by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1);
-qed "LIMSEQ_rabs_realpow_zero";
-
-Goal "abs(c) < 1 ==> (%n. abs(c) ^ n) ----NS> 0";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero,
-    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
-qed "NSLIMSEQ_rabs_realpow_zero";
-
-Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0";
-by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
-by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
-              simpset() addsimps [power_abs]));
-qed "LIMSEQ_rabs_realpow_zero2";
-
-Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0";
-by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2,
-    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
-qed "NSLIMSEQ_rabs_realpow_zero2";
-
-(***---------------------------------------------------------------
-                 Hyperreals and Sequences
- ---------------------------------------------------------------***)
-(*** A bounded sequence is a finite hyperreal ***)
-Goal "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite";
-by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
-       [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
-       simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
-        Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
-qed "NSBseq_HFinite_hypreal";
-
-(*** A sequence converging to zero defines an infinitesimal ***)
-Goalw [NSLIMSEQ_def] 
-      "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal";
-by (dres_inst_tac [("x","whn")] bspec 1);
-by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
-by (auto_tac (claset(),
-              simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
-                                  starfunNat]));
-qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
-
-(***---------------------------------------------------------------
-    Theorems proved by Harrison in HOL that we do not need 
-    in order to prove equivalence between Cauchy criterion 
-    and convergence:
- -- Show that every sequence contains a monotonic subsequence   
-Goal "EX f. subseq f & monoseq (%n. s (f n))";
- -- Show that a subsequence of a bounded sequence is bounded
-Goal "Bseq X ==> Bseq (%n. X (f n))";
- -- Show we can take subsequential terms arbitrarily far 
-    up a sequence       
-Goal "subseq f ==> n <= f(n)";
-Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
- ---------------------------------------------------------------***)
-
-
diff -r 32402f5624d1 -r 6c3276a2735b src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 28 16:25:40 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 28 16:26:27 2004 +0200
@@ -2,62 +2,1226 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Convergence of sequences and series
-*) 
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+*)
 
-SEQ = NatStar + HyperPow + 
+theory SEQ = NatStar + HyperPow:
 
 constdefs
 
-  (* Standard definition of convergence of sequence *)           
-  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" [60, 60] 60)
-  "X ----> L == (ALL r. 0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
-  
-  (* Nonstandard definition of convergence of sequence *)
-  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
-  "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"
+  LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
+    --{*Standard definition of convergence of sequence*}
+  "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
 
-  (* define value of limit using choice operator*)
-  lim :: (nat => real) => real
+  NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
+    --{*Nonstandard definition of convergence of sequence*}
+  "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
+
+  lim :: "(nat => real) => real"
+    --{*Standard definition of limit using choice operator*}
   "lim X == (@L. (X ----> L))"
 
-  nslim :: (nat => real) => real
+  nslim :: "(nat => real) => real"
+    --{*Nonstandard definition of limit using choice operator*}
   "nslim X == (@L. (X ----NS> L))"
 
-  (* Standard definition of convergence *)
-  convergent :: (nat => real) => bool
-  "convergent X == (EX L. (X ----> L))"
-
-  (* Nonstandard definition of convergence *)
-  NSconvergent :: (nat => real) => bool
-  "NSconvergent X == (EX L. (X ----NS> L))"
+  convergent :: "(nat => real) => bool"
+    --{*Standard definition of convergence*}
+  "convergent X == (\<exists>L. (X ----> L))"
 
-  (* Standard definition for bounded sequence *)
-  Bseq :: (nat => real) => bool
-  "Bseq X == (EX K. (0 < K & (ALL n. abs(X n) <= K)))"
- 
-  (* Nonstandard definition for bounded sequence *)
-  NSBseq :: (nat=>real) => bool
-  "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" 
+  NSconvergent :: "(nat => real) => bool"
+    --{*Nonstandard definition of convergence*}
+  "NSconvergent X == (\<exists>L. (X ----NS> L))"
+
+  Bseq :: "(nat => real) => bool"
+    --{*Standard definition for bounded sequence*}
+  "Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))"
 
-  (* Definition for monotonicity *)
-  monoseq :: (nat=>real)=>bool
-  "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) |
-                 (ALL m n. m <= n --> X n <= X m))"   
+  NSBseq :: "(nat=>real) => bool"
+    --{*Nonstandard definition for bounded sequence*}
+  "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite)"
+
+  monoseq :: "(nat=>real)=>bool"
+    --{*Definition for monotonicity*}
+  "monoseq X == ((\<forall>(m::nat) n. m \<le> n --> X m \<le> X n) |
+                 (\<forall>m n. m \<le> n --> X n \<le> X m))"
 
-  (* Definition of subsequence *)
-  subseq :: (nat => nat) => bool
-  "subseq f == (ALL m n. m < n --> (f m) < (f n))"
+  subseq :: "(nat => nat) => bool"
+    --{*Definition of subsequence*}
+  "subseq f == (\<forall>m n. m < n --> (f m) < (f n))"
 
-  (** Cauchy condition **)
-
-  (* Standard definition *)
-  Cauchy :: (nat => real) => bool
-  "Cauchy X == (ALL e. (0 < e -->
-                       (EX M. (ALL m n. M <= m & M <= n 
+  Cauchy :: "(nat => real) => bool"
+    --{*Standard definition of the Cauchy condition*}
+  "Cauchy X == (\<forall>e. (0 < e -->
+                       (\<exists>M. (\<forall>m n. M \<le> m & M \<le> n
                              --> abs((X m) + -(X n)) < e))))"
 
-  NSCauchy :: (nat => real) => bool
-  "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
-                      ( *fNat* X) M @= ( *fNat* X) N)"
+  NSCauchy :: "(nat => real) => bool"
+    --{*Nonstandard definition*}
+  "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
+                      ( *fNat* X) M \<approx> ( *fNat* X) N)"
+
+
+
+text{* Example of an hypersequence (i.e. an extended standard sequence)
+   whose term with an hypernatural suffix is an infinitesimal i.e.
+   the whn'nth term of the hypersequence is a member of Infinitesimal*}
+
+lemma SEQ_Infinitesimal:
+      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
+apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
+done
+
+
+subsection{*LIMSEQ and NSLIMSEQ*}
+
+lemma LIMSEQ_iff:
+      "(X ----> L) =
+       (\<forall>r. 0 <r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+by (simp add: LIMSEQ_def)
+
+lemma NSLIMSEQ_iff:
+    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
+by (simp add: NSLIMSEQ_def)
+
+
+text{*LIMSEQ ==> NSLIMSEQ*}
+
+lemma LIMSEQ_NSLIMSEQ:
+      "X ----> L ==> X ----NS> L"
+apply (simp add: LIMSEQ_def NSLIMSEQ_def)
+apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule approx_minus_iff [THEN iffD2])
+apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
+              hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (drule_tac x = u in spec, safe)
+apply (drule_tac x = no in spec, fuf)
+apply (blast dest: less_imp_le)
+done
+
+
+text{*NSLIMSEQ ==> LIMSEQ*}
+
+lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n
+           ==> {n. f n = 0} = {0} | {n. f n = 0} = {}"
+apply auto
+apply (drule_tac x = xa in spec)
+apply (drule_tac [2] x = x in spec, auto)
+done
+
+lemma lemma_NSLIMSEQ2: "{n. f n \<le> Suc u} = {n. f n \<le> u} Un {n. f n = Suc u}"
+by (auto simp add: le_Suc_eq)
+
+lemma lemma_NSLIMSEQ3:
+     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. f n = Suc u} \<le> {n. n \<le> Suc u}"
+apply auto
+apply (drule_tac x = x in spec, auto)
+done
+
+text{* the following sequence @{term "f(n)"} defines a hypernatural *}
+lemma NSLIMSEQ_finite_set:
+     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
+apply (induct u)
+apply (auto simp add: lemma_NSLIMSEQ2)
+apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def])
+apply (drule lemma_NSLIMSEQ1, safe)
+apply (simp_all (no_asm_simp)) 
+done
+
+lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n \<le> u}"
+by (auto dest: less_le_trans simp add: le_def)
+
+text{* the index set is in the free ultrafilter *}
+lemma FreeUltrafilterNat_NSLIMSEQ:
+     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. u < f n} : FreeUltrafilterNat"
+apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2])
+apply (rule FreeUltrafilterNat_finite)
+apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set)
+done
+
+text{* thus, the sequence defines an infinite hypernatural! *}
+lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
+          ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite"
+apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (erule FreeUltrafilterNat_NSLIMSEQ)
+done
+
+lemma lemmaLIM:
+     "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
+      {n. \<bar>X (f n) + - L\<bar> < r}"
+by auto
+
+lemma lemmaLIM2:
+  "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
+by auto
+
+lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
+           ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
+           - hypreal_of_real  L \<approx> 0 |] ==> False"
+apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (rename_tac "Y")
+apply (drule_tac x = r in spec, safe)
+apply (drule FreeUltrafilterNat_Int, assumption)
+apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
+apply (drule FreeUltrafilterNat_all)
+apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
+apply (drule FreeUltrafilterNat_Int, assumption)
+apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty)
+done
+
+lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
+apply (simp add: LIMSEQ_def NSLIMSEQ_def)
+apply (rule ccontr, simp, safe)
+txt{* skolemization step *}
+apply (drule choice, safe)
+apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec)
+apply (drule_tac [2] approx_minus_iff [THEN iffD1])
+apply (simp_all add: linorder_not_less)
+apply (blast intro: HNatInfinite_NSLIMSEQ)
+apply (blast intro: lemmaLIM3)
+done
+
+text{* Now, the all-important result is trivially proved! *}
+theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
+by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
+
+
+subsection{*Theorems About Sequences*}
+
+lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
+by (simp add: NSLIMSEQ_def)
+
+lemma LIMSEQ_const: "(%n. k) ----> k"
+by (simp add: LIMSEQ_def)
+
+lemma NSLIMSEQ_add:
+      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
+by (auto intro: approx_add simp add: NSLIMSEQ_def starfunNat_add [symmetric])
+
+lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
+
+lemma NSLIMSEQ_mult:
+      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
+by (auto intro!: approx_mult_HFinite 
+        simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric])
+
+lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
+
+lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
+by (auto simp add: NSLIMSEQ_def starfunNat_minus [symmetric])
+
+lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
+
+lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
+by (drule LIMSEQ_minus, simp)
+
+lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
+by (drule NSLIMSEQ_minus, simp)
+
+lemma NSLIMSEQ_add_minus:
+     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
+by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y])
+
+lemma LIMSEQ_add_minus:
+     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)
+
+lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
+apply (simp add: diff_minus)
+apply (blast intro: LIMSEQ_add_minus)
+done
+
+lemma NSLIMSEQ_diff:
+     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
+apply (simp add: diff_minus)
+apply (blast intro: NSLIMSEQ_add_minus)
+done
+
+text{*Proof is like that of @{text NSLIM_inverse}.*}
+lemma NSLIMSEQ_inverse:
+     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
+by (simp add: NSLIMSEQ_def starfunNat_inverse [symmetric] 
+              hypreal_of_real_approx_inverse)
+
+
+text{*Standard version of theorem*}
+lemma LIMSEQ_inverse:
+     "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
+by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
+
+lemma NSLIMSEQ_mult_inverse:
+     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
+by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
+
+lemma LIMSEQ_divide:
+     "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
+by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
+
+text{*Uniqueness of limit*}
+lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
+apply (simp add: NSLIMSEQ_def)
+apply (drule HNatInfinite_whn [THEN [2] bspec])+
+apply (auto dest: approx_trans3)
+done
+
+lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
+
+
+subsection{*Nslim and Lim*}
+
+lemma limI: "X ----> L ==> lim X = L"
+apply (simp add: lim_def)
+apply (blast intro: LIMSEQ_unique)
+done
+
+lemma nslimI: "X ----NS> L ==> nslim X = L"
+apply (simp add: nslim_def)
+apply (blast intro: NSLIMSEQ_unique)
+done
+
+lemma lim_nslim_iff: "lim X = nslim X"
+by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
+
+
+subsection{*Convergence*}
+
+lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
+by (simp add: convergent_def)
+
+lemma convergentI: "(X ----> L) ==> convergent X"
+by (auto simp add: convergent_def)
+
+lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
+by (simp add: NSconvergent_def)
+
+lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
+by (auto simp add: NSconvergent_def)
+
+lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
+by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
+
+lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
+by (auto intro: someI simp add: NSconvergent_def nslim_def)
+
+lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
+by (auto intro: someI simp add: convergent_def lim_def)
+
+text{*Subsequence (alternative definition, (e.g. Hoskins)*}
+
+lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
+apply (simp add: subseq_def)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k)
+apply (auto intro: less_trans)
+done
+
+
+subsection{*Monotonicity*}
+
+lemma monoseq_Suc:
+   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
+                 | (\<forall>n. X (Suc n) \<le> X n))"
+apply (simp add: monoseq_def)
+apply (auto dest!: le_imp_less_or_eq)
+apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
+apply (induct_tac "ka")
+apply (auto intro: order_trans)
+apply (erule swap) 
+apply (induct_tac "k")
+apply (auto intro: order_trans)
+done
+
+lemma monoI1: "\<forall>m n. m \<le> n --> X m \<le> X n ==> monoseq X"
+by (simp add: monoseq_def)
+
+lemma monoI2: "\<forall>m n. m \<le> n --> X n \<le> X m ==> monoseq X"
+by (simp add: monoseq_def)
+
+lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
+by (simp add: monoseq_Suc)
+
+lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
+by (simp add: monoseq_Suc)
+
+
+subsection{*Bounded Sequence*}
+
+lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
+by (simp add: Bseq_def)
+
+lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
+by (auto simp add: Bseq_def)
+
+lemma lemma_NBseq_def:
+     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
+      (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+apply auto
+ prefer 2 apply force
+apply (cut_tac x = K in reals_Archimedean2, clarify)
+apply (rule_tac x = n in exI, clarify)
+apply (drule_tac x = na in spec)
+apply (auto simp add: real_of_nat_Suc)
+done
+
+text{* alternative definition for Bseq *}
+lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
+apply (simp add: Bseq_def)
+apply (simp (no_asm) add: lemma_NBseq_def)
+done
+
+lemma lemma_NBseq_def2:
+     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
+      (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+apply (subst lemma_NBseq_def, auto)
+apply (rule_tac x = "Suc N" in exI)
+apply (rule_tac [2] x = N in exI)
+apply (auto simp add: real_of_nat_Suc)
+ prefer 2 apply (blast intro: order_less_imp_le)
+apply (drule_tac x = n in spec, simp)
+done
+
+(* yet another definition for Bseq *)
+lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
+by (simp add: Bseq_def lemma_NBseq_def2)
+
+lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite"
+by (simp add: NSBseq_def)
+
+lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X"
+by (simp add: NSBseq_def)
+
+text{*The standard definition implies the nonstandard definition*}
+
+lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
+by auto
+
+lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
+apply (simp add: Bseq_def NSBseq_def, safe)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff 
+                      HNatInfinite_FreeUltrafilterNat_iff)
+apply (rule bexI [OF _ lemma_hyprel_refl]) 
+apply (drule_tac f = Xa in lemma_Bseq)
+apply (rule_tac x = "K+1" in exI)
+apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
+done
+
+text{*The nonstandard definition implies the standard definition*}
+
+(* similar to NSLIM proof in REALTOPOS *)
+
+text{* We need to get rid of the real variable and do so by proving the
+   following, which relies on the Archimedean property of the reals.
+   When we skolemize we then get the required function @{term "f::nat=>nat"}.
+   Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
+   which woulid be useless.*}
+
+lemma lemmaNSBseq:
+     "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+      ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
+apply safe
+apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
+done
+
+lemma lemmaNSBseq2: "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
+                     ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
+apply (drule lemmaNSBseq)
+apply (drule choice, blast)
+done
+
+lemma real_seq_to_hypreal_HInfinite:
+     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+      ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite"
+apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
+apply (rule bexI [OF _ lemma_hyprel_refl], clarify)  
+apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
+apply (drule FreeUltrafilterNat_all)
+apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
+apply (auto simp add: real_of_nat_Suc)
+done
+
+text{* Now prove that we can get out an infinite hypernatural as well
+     defined using the skolem function  @{term "f::nat=>nat"} above*}
+
+lemma lemma_finite_NSBseq:
+     "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
+      {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
+      {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
+by (auto dest!: le_imp_less_or_eq)
+
+lemma lemma_finite_NSBseq2:
+     "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
+apply (induct_tac "u")
+apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
+apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
+apply (auto intro: finite_real_of_nat_less_real 
+            simp add: real_of_nat_Suc less_diff_eq [symmetric])
+done
+
+lemma HNatInfinite_skolem_f:
+     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
+      ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite"
+apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
+apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
+apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
+                    {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
+apply (erule ssubst) 
+ apply (auto simp add: linorder_not_less Compl_def)
+done
+
+lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
+apply (simp add: Bseq_def NSBseq_def)
+apply (rule ccontr)
+apply (auto simp add: linorder_not_less [symmetric])
+apply (drule lemmaNSBseq2, safe)
+apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
+apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
+apply (auto simp add: starfunNat o_def HFinite_HInfinite_iff)
+done
+
+text{* Equivalence of nonstandard and standard definitions
+  for a bounded sequence*}
+lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
+by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
+
+text{*A convergent sequence is bounded: 
+ Boundedness as a necessary condition for convergence. 
+ The nonstandard version has no existential, as usual *}
+
+lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
+apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
+apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
+done
+
+text{*Standard Version: easily now proved using equivalence of NS and
+ standard definitions *}
+lemma convergent_Bseq: "convergent X ==> Bseq X"
+by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
+
+
+subsection{*Upper Bounds and Lubs of Bounded Sequences*}
+
+lemma Bseq_isUb:
+  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
+
+
+text{* Use completeness of reals (supremum property)
+   to show that any bounded sequence has a least upper bound*}
+
+lemma Bseq_isLub:
+  "!!(X::nat=>real). Bseq X ==>
+   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (blast intro: reals_complete Bseq_isUb)
+
+lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
+by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
+
+lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
+by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
+
+
+subsection{*A Bounded and Monotonic Sequence Converges*}
+
+lemma lemma_converg1:
+     "!!(X::nat=>real). [| \<forall>m n. m \<le> n -->  X m \<le> X n;
+                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
+               |] ==> \<forall>n. ma \<le> n --> X n = X ma"
+apply safe
+apply (drule_tac y = "X n" in isLubD2)
+apply (blast dest: order_antisym)+
+done
+
+text{* The best of both worlds: Easier to prove this result as a standard
+   theorem and then use equivalence to "transfer" it into the
+   equivalent nonstandard form if needed!*}
+
+lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
+apply (simp add: LIMSEQ_def)
+apply (rule_tac x = "X m" in exI, safe)
+apply (rule_tac x = m in exI, safe)
+apply (drule spec, erule impE, auto)
+done
+
+text{*Now, the same theorem in terms of NS limit *}
+lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----NS> L)"
+by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
+
+lemma lemma_converg2:
+   "!!(X::nat=>real).
+    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
+apply safe
+apply (drule_tac y = "X m" in isLubD2)
+apply (auto dest!: order_le_imp_less_or_eq)
+done
+
+lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
+by (rule setleI [THEN isUbI], auto)
+
+text{* FIXME: @{term "U - T < U"} is redundant *}
+lemma lemma_converg4: "!!(X::nat=> real).
+               [| \<forall>m. X m ~= U;
+                  isLub UNIV {x. \<exists>n. X n = x} U;
+                  0 < T;
+                  U + - T < U
+               |] ==> \<exists>m. U + -T < X m & X m < U"
+apply (drule lemma_converg2, assumption)
+apply (rule ccontr, simp)
+apply (simp add: linorder_not_less)
+apply (drule lemma_converg3)
+apply (drule isLub_le_isUb, assumption)
+apply (auto dest: order_less_le_trans)
+done
+
+text{*A standard proof of the theorem for monotone increasing sequence*}
+
+lemma Bseq_mono_convergent:
+     "[| Bseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> convergent X"
+apply (simp add: convergent_def)
+apply (frule Bseq_isLub, safe)
+apply (case_tac "\<exists>m. X m = U", auto)
+apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
+(* second case *)
+apply (rule_tac x = U in exI)
+apply (subst LIMSEQ_iff, safe)
+apply (frule lemma_converg2, assumption)
+apply (drule lemma_converg4, auto)
+apply (rule_tac x = m in exI, safe)
+apply (subgoal_tac "X m \<le> X n")
+ prefer 2 apply blast
+apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
+done
+
+text{*Nonstandard version of the theorem*}
+
+lemma NSBseq_mono_NSconvergent:
+     "[| NSBseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> NSconvergent X"
+by (auto intro: Bseq_mono_convergent 
+         simp add: convergent_NSconvergent_iff [symmetric] 
+                   Bseq_NSBseq_iff [symmetric])
+
+lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
+apply (simp add: convergent_def)
+apply (auto dest: LIMSEQ_minus)
+apply (drule LIMSEQ_minus, auto)
+done
+
+lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
+by (simp add: Bseq_def)
+
+text{*Main monotonicity theorem*}
+lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
+apply (simp add: monoseq_def, safe)
+apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
+apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
+apply (auto intro!: Bseq_mono_convergent)
+done
+
+
+subsection{*A Few More Equivalence Theorems for Boundedness*}
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + -x\<bar> \<le> k))"
+apply (unfold Bseq_def, safe)
+apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
+apply (rule_tac x = K in exI)
+apply (rule_tac x = 0 in exI, auto)
+apply (drule_tac [!] x=n in spec, arith+)
+done
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + -X(N)) \<le> k))"
+apply safe
+apply (simp add: Bseq_def, safe)
+apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
+apply auto
+apply arith
+apply (rule_tac x = N in exI, safe)
+apply (drule_tac x = n in spec, arith)
+apply (auto simp add: Bseq_iff2)
+done
+
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
+apply (simp add: Bseq_def)
+apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI)
+apply auto
+apply (drule_tac [2] x = n in spec, arith+)
+done
+
+
+subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
+
+subsubsection{*Standard Implies Nonstandard*}
+
+lemma lemmaCauchy1:
+     "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
+      ==> {n. M \<le> x n} : FreeUltrafilterNat"
+apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
+apply (drule_tac x = M in spec, ultra)
+done
+
+lemma lemmaCauchy2:
+     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
+      {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
+      {n. abs (X (xa n) + - X (x n)) < u}"
+by blast
+
+lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
+apply (simp add: Cauchy_def NSCauchy_def, safe)
+apply (rule_tac z = M in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule approx_minus_iff [THEN iffD2])
+apply (rule mem_infmal_iff [THEN iffD1])
+apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (rule bexI, auto)
+apply (drule spec, auto)
+apply (drule_tac M = M in lemmaCauchy1)
+apply (drule_tac M = M in lemmaCauchy1)
+apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
+apply (rule FreeUltrafilterNat_Int)
+apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
+done
+
+subsubsection{*Nonstandard Implies Standard*}
+
+lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
+apply (auto simp add: Cauchy_def NSCauchy_def)
+apply (rule ccontr, simp)
+apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
+apply (drule bspec, assumption)
+apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); 
+apply (auto simp add: starfunNat)
+apply (drule approx_minus_iff [THEN iffD1])
+apply (drule mem_infmal_iff [THEN iffD2])
+apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (rename_tac "Y")
+apply (drule_tac x = e in spec, auto)
+apply (drule FreeUltrafilterNat_Int, assumption)
+apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>") 
+ prefer 2 apply (erule FreeUltrafilterNat_subset, force) 
+apply (rule FreeUltrafilterNat_empty [THEN notE]) 
+apply (subgoal_tac
+         "{n. abs (X (f n) + - X (fa n)) < e} Int 
+          {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
+apply auto  
+done
+
+
+theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
+by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
+
+text{*A Cauchy sequence is bounded -- this is the standard
+  proof mechanization rather than the nonstandard proof*}
+
+lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
+          ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
+apply safe
+apply (drule spec, auto, arith)
+done
+
+lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
+by auto
+
+text{* FIXME: Long. Maximal element in subsequence *}
+lemma SUP_rabs_subseq:
+     "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
+apply (induct M)
+apply (rule_tac x = 0 in exI, simp, safe)
+apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
+apply safe
+apply (rule_tac x = m in exI)
+apply (rule_tac [2] x = m in exI)
+apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
+apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) 
+apply (simp_all add: less_Suc_cancel_iff)
+apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
+done
+
+lemma lemma_Nat_covered:
+     "[| \<forall>m::nat. m \<le> M --> P M m;
+         \<forall>m. M \<le> m --> P M m |]
+      ==> \<forall>m. P M m"
+by (auto elim: less_asym simp add: le_def)
+
+
+lemma lemma_trans1:
+     "[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
+      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+by (blast intro: order_le_less_trans [THEN order_less_imp_le])
+
+lemma lemma_trans2:
+     "[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
+      ==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
+by (blast intro: order_less_trans [THEN order_less_imp_le])
+
+lemma lemma_trans3:
+     "[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
+      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
+by auto
+
+lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
+              ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
+by (blast intro: order_less_imp_le)
+
+
+text{*Proof is more involved than outlines sketched by various authors
+ would suggest*}
+
+lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
+apply (simp add: Cauchy_def Bseq_def)
+apply (drule_tac x = 1 in spec)
+apply (erule zero_less_one [THEN [2] impE], safe)
+apply (drule_tac x = M in spec, simp)
+apply (drule lemmaCauchy)
+apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
+apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
+apply safe
+apply (drule lemma_trans1, assumption)
+apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
+apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
+apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
+apply (drule lemma_trans4)
+apply (drule_tac [2] lemma_trans4)
+apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
+apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
+apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
+apply (auto elim!: lemma_Nat_covered, arith+)
+done
+
+text{*A Cauchy sequence is bounded -- nonstandard version*}
+
+lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
+by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
+
+
+text{*Equivalence of Cauchy criterion and convergence:
+  We will prove this using our NS formulation which provides a
+  much easier proof than using the standard definition. We do not
+  need to use properties of subsequences such as boundedness,
+  monotonicity etc... Compare with Harrison's corresponding proof
+  in HOL which is much longer and more complicated. Of course, we do
+  not have problems which he encountered with guessing the right
+  instantiations for his 'espsilon-delta' proof(s) in this case
+  since the NS formulations do not involve existential quantifiers.*}
+
+lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
+apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
+apply (frule NSCauchy_NSBseq)
+apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
+apply (drule HNatInfinite_whn [THEN [2] bspec])
+apply (drule HNatInfinite_whn [THEN [2] bspec])
+apply (auto dest!: st_part_Ex simp add: SReal_iff)
+apply (blast intro: approx_trans3)
+done
+
+text{*Standard proof for free*}
+lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
+by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
+
+
+text{*We can now try and derive a few properties of sequences,
+     starting with the limit comparison property for sequences.*}
+
+lemma NSLIMSEQ_le:
+       "[| f ----NS> l; g ----NS> m;
+           \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
+                |] ==> l \<le> m"
+apply (simp add: NSLIMSEQ_def, safe)
+apply (drule starfun_le_mono)
+apply (drule HNatInfinite_whn [THEN [2] bspec])+
+apply (drule_tac x = whn in spec)
+apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
+apply clarify
+apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
+done
+
+(* standard version *)
+lemma LIMSEQ_le:
+     "[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
+      ==> l \<le> m"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
+
+lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+apply (rule LIMSEQ_le)
+apply (rule LIMSEQ_const, auto)
+done
+
+lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
+by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
+
+lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+apply (rule LIMSEQ_le)
+apply (rule_tac [2] LIMSEQ_const, auto)
+done
+
+lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
+by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
+
+text{*Shift a convergent series by 1:
+  By the equivalence between Cauchiness and convergence and because
+  the successor of an infinite hypernatural is also infinite.*}
+
+lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
+apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
+apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
+apply (drule bspec, assumption)
+apply (drule bspec, assumption)
+apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
+apply (blast intro: approx_trans3)
+done
+
+text{* standard version *}
+lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
+
+lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
+apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
+apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
+apply (drule bspec, assumption)
+apply (drule bspec, assumption)
+apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
+apply (drule_tac x="N - 1" in bspec) 
+apply (auto intro: approx_trans3)
+done
+
+lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
+apply (simp add: LIMSEQ_NSLIMSEQ_iff)
+apply (erule NSLIMSEQ_imp_Suc)
+done
+
+lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
+by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+
+lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
+by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
+
+text{*A sequence tends to zero iff its abs does*}
+lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
+by (simp add: LIMSEQ_def)
+
+text{*We prove the NS version from the standard one, since the NS proof
+   seems more complicated than the standard one above!*}
+lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
+
+text{*Generalization to other limits*}
+lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
+apply (simp add: NSLIMSEQ_def)
+apply (auto intro: approx_hrabs 
+            simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric])
+done
+
+text{* standard version *}
+lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
+
+text{*An unbounded sequence's inverse tends to 0*}
+
+text{* standard proof seems easier *}
+lemma LIMSEQ_inverse_zero:
+      "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
+apply (simp add: LIMSEQ_def, safe)
+apply (drule_tac x = "inverse r" in spec, safe)
+apply (rule_tac x = N in exI, safe)
+apply (drule spec, auto)
+apply (frule positive_imp_inverse_positive)
+apply (frule order_less_trans, assumption)
+apply (frule_tac a = "f n" in positive_imp_inverse_positive)
+apply (simp add: abs_if) 
+apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
+apply (auto intro: inverse_less_iff_less [THEN iffD2]
+            simp del: inverse_inverse_eq)
+done
+
+lemma NSLIMSEQ_inverse_zero:
+     "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
+      ==> (%n. inverse(f n)) ----NS> 0"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
+
+text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
+
+lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
+apply (rule LIMSEQ_inverse_zero, safe)
+apply (cut_tac x = y in reals_Archimedean2)
+apply (safe, rule_tac x = n in exI)
+apply (auto simp add: real_of_nat_Suc)
+done
+
+lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
+
+text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
+infinity is now easily proved*}
+
+lemma LIMSEQ_inverse_real_of_nat_add:
+     "(%n. r + inverse(real(Suc n))) ----> r"
+by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
+
+lemma NSLIMSEQ_inverse_real_of_nat_add:
+     "(%n. r + inverse(real(Suc n))) ----NS> r"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus:
+     "(%n. r + -inverse(real(Suc n))) ----> r"
+by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
+
+lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
+     "(%n. r + -inverse(real(Suc n))) ----NS> r"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
+     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
+by (cut_tac b=1 in
+        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
+
+lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
+     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
+
+
+text{* Real Powers*}
+
+lemma NSLIMSEQ_pow [rule_format]:
+     "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
+apply (induct_tac "m")
+apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
+done
+
+lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
+by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
+
+text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
+"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
+  also fact that bounded and monotonic sequence converges.*}
+
+lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
+apply (simp add: Bseq_def)
+apply (rule_tac x = 1 in exI)
+apply (simp add: power_abs)
+apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
+done
+
+lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
+apply (clarify intro!: mono_SucI2)
+apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
+done
+
+lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
+by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
+
+text{* We now use NS criterion to bring proof of theorem through *}
+
+lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
+apply (simp add: NSLIMSEQ_def)
+apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
+apply (frule NSconvergentD)
+apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow)
+apply (frule HNatInfinite_add_one)
+apply (drule bspec, assumption)
+apply (drule bspec, assumption)
+apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
+apply (simp add: hyperpow_add)
+apply (drule approx_mult_subst_SReal, assumption)
+apply (drule approx_trans3, assumption)
+apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric])
+done
+
+text{* standard version *}
+lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
+by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
+
+lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
+apply (cut_tac a = a and x1 = "inverse x" in
+        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
+apply (auto simp add: divide_inverse power_inverse)
+apply (simp add: inverse_eq_divide pos_divide_less_eq)
+done
+
+subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
+
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
+by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
+
+lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
+by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
+
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
+apply (rule LIMSEQ_rabs_zero [THEN iffD1])
+apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
+done
+
+lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
+by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
+
+subsection{*Hyperreals and Sequences*}
+
+text{*A bounded sequence is a finite hyperreal*}
+lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
+by (auto intro!: bexI lemma_hyprel_refl 
+            intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
+            simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
+                      Bseq_iff1a)
+
+text{*A sequence converging to zero defines an infinitesimal*}
+lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
+      "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
+apply (simp add: NSLIMSEQ_def)
+apply (drule_tac x = whn in bspec)
+apply (simp add: HNatInfinite_whn)
+apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat)
+done
+
+(***---------------------------------------------------------------
+    Theorems proved by Harrison in HOL that we do not need
+    in order to prove equivalence between Cauchy criterion
+    and convergence:
+ -- Show that every sequence contains a monotonic subsequence
+Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
+ -- Show that a subsequence of a bounded sequence is bounded
+Goal "Bseq X ==> Bseq (%n. X (f n))";
+ -- Show we can take subsequential terms arbitrarily far
+    up a sequence
+Goal "subseq f ==> n \<le> f(n)";
+Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
+ ---------------------------------------------------------------***)
+
+ML
+{*
+val Cauchy_def = thm"Cauchy_def";
+val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
+val LIMSEQ_iff = thm "LIMSEQ_iff";
+val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
+val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
+val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
+val Compl_less_set = thm "Compl_less_set";
+val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
+val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
+val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
+val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
+val NSLIMSEQ_const = thm "NSLIMSEQ_const";
+val LIMSEQ_const = thm "LIMSEQ_const";
+val NSLIMSEQ_add = thm "NSLIMSEQ_add";
+val LIMSEQ_add = thm "LIMSEQ_add";
+val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
+val LIMSEQ_mult = thm "LIMSEQ_mult";
+val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
+val LIMSEQ_minus = thm "LIMSEQ_minus";
+val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
+val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
+val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
+val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
+val LIMSEQ_diff = thm "LIMSEQ_diff";
+val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
+val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
+val LIMSEQ_inverse = thm "LIMSEQ_inverse";
+val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
+val LIMSEQ_divide = thm "LIMSEQ_divide";
+val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
+val LIMSEQ_unique = thm "LIMSEQ_unique";
+val limI = thm "limI";
+val nslimI = thm "nslimI";
+val lim_nslim_iff = thm "lim_nslim_iff";
+val convergentD = thm "convergentD";
+val convergentI = thm "convergentI";
+val NSconvergentD = thm "NSconvergentD";
+val NSconvergentI = thm "NSconvergentI";
+val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
+val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
+val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
+val subseq_Suc_iff = thm "subseq_Suc_iff";
+val monoseq_Suc = thm "monoseq_Suc";
+val monoI1 = thm "monoI1";
+val monoI2 = thm "monoI2";
+val mono_SucI1 = thm "mono_SucI1";
+val mono_SucI2 = thm "mono_SucI2";
+val BseqD = thm "BseqD";
+val BseqI = thm "BseqI";
+val Bseq_iff = thm "Bseq_iff";
+val Bseq_iff1a = thm "Bseq_iff1a";
+val NSBseqD = thm "NSBseqD";
+val NSBseqI = thm "NSBseqI";
+val Bseq_NSBseq = thm "Bseq_NSBseq";
+val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
+val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
+val NSBseq_Bseq = thm "NSBseq_Bseq";
+val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
+val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
+val convergent_Bseq = thm "convergent_Bseq";
+val Bseq_isUb = thm "Bseq_isUb";
+val Bseq_isLub = thm "Bseq_isLub";
+val NSBseq_isUb = thm "NSBseq_isUb";
+val NSBseq_isLub = thm "NSBseq_isLub";
+val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
+val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
+val Bseq_mono_convergent = thm "Bseq_mono_convergent";
+val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
+val convergent_minus_iff = thm "convergent_minus_iff";
+val Bseq_minus_iff = thm "Bseq_minus_iff";
+val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
+val Bseq_iff2 = thm "Bseq_iff2";
+val Bseq_iff3 = thm "Bseq_iff3";
+val BseqI2 = thm "BseqI2";
+val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
+val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
+val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
+val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
+val SUP_rabs_subseq = thm "SUP_rabs_subseq";
+val Cauchy_Bseq = thm "Cauchy_Bseq";
+val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
+val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
+val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
+val NSLIMSEQ_le = thm "NSLIMSEQ_le";
+val LIMSEQ_le = thm "LIMSEQ_le";
+val LIMSEQ_le_const = thm "LIMSEQ_le_const";
+val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
+val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
+val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
+val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
+val LIMSEQ_Suc = thm "LIMSEQ_Suc";
+val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
+val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
+val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
+val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
+val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
+val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
+val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
+val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
+val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
+val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
+val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
+val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
+val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
+val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
+val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
+val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
+val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
+val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
+val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
+val LIMSEQ_pow = thm "LIMSEQ_pow";
+val Bseq_realpow = thm "Bseq_realpow";
+val monoseq_realpow = thm "monoseq_realpow";
+val convergent_realpow = thm "convergent_realpow";
+val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
+val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
+val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
+val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
+val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
+val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
+val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
+val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
+val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
+*}
+
 end
 
diff -r 32402f5624d1 -r 6c3276a2735b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 28 16:25:40 2004 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 28 16:26:27 2004 +0200
@@ -154,7 +154,7 @@
   Hyperreal/Lim.thy Hyperreal/Log.thy\
   Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
-  Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
+  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
   Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
   Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\