conversion of SEQ.ML to Isar script
authorpaulson
Wed Jul 28 16:26:27 2004 +0200 (2004-07-28)
changeset 150826c3276a2735b
parent 15081 32402f5624d1
child 15083 a471fd1d9961
conversion of SEQ.ML to Isar script
src/HOL/Hyperreal/Integration.ML
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/SEQ.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:25:40 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.ML	Wed Jul 28 16:26:27 2004 +0200
     1.3 @@ -10,6 +10,13 @@
     1.4  fun ARITH_PROVE str = prove_goal thy str
     1.5                        (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
     1.6  
     1.7 +fun CLAIM_SIMP str thms =
     1.8 +               prove_goal (the_context()) str
     1.9 +               (fn prems => [cut_facts_tac prems 1,
    1.10 +                   auto_tac (claset(),simpset() addsimps thms)]);
    1.11 +
    1.12 +fun CLAIM str = CLAIM_SIMP str [];
    1.13 +
    1.14  Goalw [psize_def] "a = b ==> psize (%n. if n = 0 then a else b) = 0";
    1.15  by Auto_tac;
    1.16  qed "partition_zero";
     2.1 --- a/src/HOL/Hyperreal/SEQ.ML	Wed Jul 28 16:25:40 2004 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1345 +0,0 @@
     2.4 -(*  Title       : SEQ.ML
     2.5 -    Author      : Jacques D. Fleuriot
     2.6 -    Copyright   : 1998  University of Cambridge
     2.7 -    Description : Theory of sequence and series of real numbers
     2.8 -*) 
     2.9 -
    2.10 -val Nats_1 = thm"Nats_1";
    2.11 -
    2.12 -fun CLAIM_SIMP str thms =
    2.13 -               prove_goal (the_context()) str
    2.14 -               (fn prems => [cut_facts_tac prems 1,
    2.15 -                   auto_tac (claset(),simpset() addsimps thms)]);
    2.16 -
    2.17 -fun CLAIM str = CLAIM_SIMP str [];
    2.18 -
    2.19 -(*---------------------------------------------------------------------------
    2.20 -   Example of an hypersequence (i.e. an extended standard sequence) 
    2.21 -   whose term with an hypernatural suffix is an infinitesimal i.e. 
    2.22 -   the whn'nth term of the hypersequence is a member of Infinitesimal 
    2.23 - -------------------------------------------------------------------------- *)
    2.24 -
    2.25 -Goalw [hypnat_omega_def] 
    2.26 -      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
    2.27 -by (auto_tac (claset(),
    2.28 -      simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
    2.29 -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    2.30 -by (auto_tac (claset(),
    2.31 -              simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2,
    2.32 -                            FreeUltrafilterNat_inverse_real_of_posnat]));
    2.33 -qed "SEQ_Infinitesimal";
    2.34 -
    2.35 -(*--------------------------------------------------------------------------
    2.36 -                  Rules for LIMSEQ and NSLIMSEQ etc.
    2.37 - --------------------------------------------------------------------------*)
    2.38 -
    2.39 -Goalw [LIMSEQ_def] 
    2.40 -      "(X ----> L) = \
    2.41 -\      (ALL r. 0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
    2.42 -by (Simp_tac 1);
    2.43 -qed "LIMSEQ_iff";
    2.44 -
    2.45 -Goalw [NSLIMSEQ_def] 
    2.46 -    "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)";
    2.47 -by (Simp_tac 1);
    2.48 -qed "NSLIMSEQ_iff";
    2.49 -
    2.50 -(*----------------------------------------
    2.51 -          LIMSEQ ==> NSLIMSEQ
    2.52 - ---------------------------------------*)
    2.53 -Goalw [LIMSEQ_def,NSLIMSEQ_def] 
    2.54 -      "X ----> L ==> X ----NS> L";
    2.55 -by (auto_tac (claset(),simpset() addsimps 
    2.56 -    [HNatInfinite_FreeUltrafilterNat_iff]));
    2.57 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
    2.58 -by (rtac (approx_minus_iff RS iffD2) 1);
    2.59 -by (auto_tac (claset(),simpset() addsimps [starfunNat,
    2.60 -    mem_infmal_iff RS sym,hypreal_of_real_def,
    2.61 -    hypreal_minus,hypreal_add,
    2.62 -    Infinitesimal_FreeUltrafilterNat_iff]));
    2.63 -by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
    2.64 -by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1);
    2.65 -by (dres_inst_tac [("x","no")] spec 1);
    2.66 -by (Fuf_tac 1);
    2.67 -by (blast_tac (claset() addDs [less_imp_le]) 1);
    2.68 -qed "LIMSEQ_NSLIMSEQ";
    2.69 -
    2.70 -(*-------------------------------------------------------------
    2.71 -          NSLIMSEQ ==> LIMSEQ
    2.72 -    proving NS def ==> Standard def is trickier as usual 
    2.73 - -------------------------------------------------------------*)
    2.74 -(* the following sequence f(n) defines a hypernatural *)
    2.75 -(* lemmas etc. first *)
    2.76 -Goal "!!(f::nat=>nat). ALL n. n <= f n \
    2.77 -\          ==> {n. f n = 0} = {0} | {n. f n = 0} = {}";
    2.78 -by (Auto_tac);
    2.79 -by (dres_inst_tac [("x","xa")] spec 1);
    2.80 -by (dres_inst_tac [("x","x")] spec 2);
    2.81 -by (Auto_tac);
    2.82 -qed "lemma_NSLIMSEQ1";
    2.83 -
    2.84 -Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
    2.85 -by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
    2.86 -qed "lemma_NSLIMSEQ2";
    2.87 -
    2.88 -Goal "!!(f::nat=>nat). ALL n. n <= f n \
    2.89 -\          ==> {n. f n = Suc u} <= {n. n <= Suc u}";
    2.90 -by (Auto_tac);
    2.91 -by (dres_inst_tac [("x","x")] spec 1);
    2.92 -by (Auto_tac);
    2.93 -qed "lemma_NSLIMSEQ3";
    2.94 -
    2.95 -Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
    2.96 -\         ==> finite {n. f n <= u}";
    2.97 -by (induct_tac "u" 1);
    2.98 -by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
    2.99 -by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
   2.100 -    rewrite_rule [atMost_def] finite_atMost], simpset()));
   2.101 -by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
   2.102 -by (ALLGOALS(Asm_simp_tac));
   2.103 -qed "NSLIMSEQ_finite_set";
   2.104 -
   2.105 -Goal "- {n. u < (f::nat=>nat) n} = {n. f n <= u}";
   2.106 -by (auto_tac (claset() addDs [less_le_trans],
   2.107 -    simpset() addsimps [le_def]));
   2.108 -qed "Compl_less_set";
   2.109 -
   2.110 -(* the index set is in the free ultrafilter *)
   2.111 -Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
   2.112 -\         ==> {n. u < f n} : FreeUltrafilterNat";
   2.113 -by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1);
   2.114 -by (rtac FreeUltrafilterNat_finite 1);
   2.115 -by (auto_tac (claset() addDs [NSLIMSEQ_finite_set],
   2.116 -    simpset() addsimps [Compl_less_set]));
   2.117 -qed "FreeUltrafilterNat_NSLIMSEQ";
   2.118 -
   2.119 -(* thus, the sequence defines an infinite hypernatural! *)
   2.120 -Goal "ALL n. n <= f n \
   2.121 -\         ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite";
   2.122 -by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   2.123 -by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
   2.124 -by (etac FreeUltrafilterNat_NSLIMSEQ 1);
   2.125 -qed "HNatInfinite_NSLIMSEQ";
   2.126 -
   2.127 -val lemmaLIM = CLAIM  "{n. X (f n) + - L = Y n} Int {n. abs (Y n) < r} <= \
   2.128 -\         {n. abs (X (f n) + - L) < r}";
   2.129 -
   2.130 -Goal "{n. abs (X (f n) + - L) < r} Int {n. r <= abs (X (f n) + - (L::real))} \
   2.131 -\     = {}";
   2.132 -by Auto_tac;  
   2.133 -qed "lemmaLIM2";
   2.134 -
   2.135 -Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
   2.136 -\          ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
   2.137 -\          - hypreal_of_real  L @= 0 |] ==> False";
   2.138 -by (auto_tac (claset(),simpset() addsimps [starfunNat,
   2.139 -    mem_infmal_iff RS sym,hypreal_of_real_def,
   2.140 -    hypreal_minus,hypreal_add,
   2.141 -    Infinitesimal_FreeUltrafilterNat_iff]));
   2.142 -by (rename_tac "Y" 1);
   2.143 -by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
   2.144 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   2.145 -by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
   2.146 -by (dtac FreeUltrafilterNat_all 1);
   2.147 -by (thin_tac "{n. abs (Y n) < r} : FreeUltrafilterNat" 1);
   2.148 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   2.149 -by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
   2.150 -                                  FreeUltrafilterNat_empty]) 1);
   2.151 -qed "lemmaLIM3";
   2.152 -
   2.153 -Goalw [LIMSEQ_def,NSLIMSEQ_def] 
   2.154 -      "X ----NS> L ==> X ----> L";
   2.155 -by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
   2.156 -by (Step_tac 1);
   2.157 -(* skolemization step *)
   2.158 -by (dtac choice 1 THEN Step_tac 1);
   2.159 -by (dres_inst_tac [("x","Abs_hypnat(hypnatrel``{f})")] bspec 1);
   2.160 -by (dtac (approx_minus_iff RS iffD1) 2);
   2.161 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [linorder_not_less])));
   2.162 -by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
   2.163 -by (blast_tac (claset() addIs [lemmaLIM3]) 1);
   2.164 -qed "NSLIMSEQ_LIMSEQ";
   2.165 -
   2.166 -(* Now the all important result is trivially proved! *)
   2.167 -Goal "(f ----> L) = (f ----NS> L)";
   2.168 -by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1);
   2.169 -qed "LIMSEQ_NSLIMSEQ_iff";
   2.170 -
   2.171 -(*-------------------------------------------------------------------
   2.172 -                   Theorems about sequences
   2.173 - ------------------------------------------------------------------*)
   2.174 -Goalw [NSLIMSEQ_def] "(%n. k) ----NS> k";
   2.175 -by (Auto_tac);
   2.176 -qed "NSLIMSEQ_const";
   2.177 -
   2.178 -Goalw [LIMSEQ_def] "(%n. k) ----> k";
   2.179 -by (Auto_tac);
   2.180 -qed "LIMSEQ_const";
   2.181 -
   2.182 -Goalw [NSLIMSEQ_def]
   2.183 -      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
   2.184 -by (auto_tac (claset() addIs [approx_add],
   2.185 -    simpset() addsimps [starfunNat_add RS sym]));
   2.186 -qed "NSLIMSEQ_add";
   2.187 -
   2.188 -Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
   2.189 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   2.190 -                                           NSLIMSEQ_add]) 1);
   2.191 -qed "LIMSEQ_add";
   2.192 -
   2.193 -Goalw [NSLIMSEQ_def]
   2.194 -      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
   2.195 -by (auto_tac (claset() addSIs [approx_mult_HFinite],
   2.196 -    simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
   2.197 -qed "NSLIMSEQ_mult";
   2.198 -
   2.199 -Goal "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b";
   2.200 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   2.201 -                                           NSLIMSEQ_mult]) 1);
   2.202 -qed "LIMSEQ_mult";
   2.203 -
   2.204 -Goalw [NSLIMSEQ_def] 
   2.205 -     "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
   2.206 -by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym]));
   2.207 -qed "NSLIMSEQ_minus";
   2.208 -
   2.209 -Goal "X ----> a ==> (%n. -(X n)) ----> -a";
   2.210 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   2.211 -                                           NSLIMSEQ_minus]) 1);
   2.212 -qed "LIMSEQ_minus";
   2.213 -
   2.214 -Goal "(%n. -(X n)) ----> -a ==> X ----> a";
   2.215 -by (dtac LIMSEQ_minus 1);
   2.216 -by (Asm_full_simp_tac 1);
   2.217 -qed "LIMSEQ_minus_cancel";
   2.218 -
   2.219 -Goal "(%n. -(X n)) ----NS> -a ==> X ----NS> a";
   2.220 -by (dtac NSLIMSEQ_minus 1);
   2.221 -by (Asm_full_simp_tac 1);
   2.222 -qed "NSLIMSEQ_minus_cancel";
   2.223 -
   2.224 -Goal "[| X ----NS> a; Y ----NS> b |] \
   2.225 -\               ==> (%n. X n + -Y n) ----NS> a + -b";
   2.226 -by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
   2.227 -by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
   2.228 -qed "NSLIMSEQ_add_minus";
   2.229 -
   2.230 -Goal "[| X ----> a; Y ----> b |] \
   2.231 -\               ==> (%n. X n + -Y n) ----> a + -b";
   2.232 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   2.233 -    NSLIMSEQ_add_minus]) 1);
   2.234 -qed "LIMSEQ_add_minus";
   2.235 -
   2.236 -Goalw [real_diff_def] 
   2.237 -     "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b";
   2.238 -by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
   2.239 -qed "LIMSEQ_diff";
   2.240 -
   2.241 -Goalw [real_diff_def] 
   2.242 -     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b";
   2.243 -by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
   2.244 -qed "NSLIMSEQ_diff";
   2.245 -
   2.246 -(*---------------------------------------------------------------
   2.247 -    Proof is like that of NSLIM_inverse.
   2.248 - --------------------------------------------------------------*)
   2.249 -Goalw [NSLIMSEQ_def] 
   2.250 -     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
   2.251 -by (Clarify_tac 1);
   2.252 -by (dtac bspec 1);
   2.253 -by (auto_tac (claset(), 
   2.254 -              simpset() addsimps [starfunNat_inverse RS sym, 
   2.255 -                                  hypreal_of_real_approx_inverse]));  
   2.256 -qed "NSLIMSEQ_inverse";
   2.257 -
   2.258 -
   2.259 -(*------ Standard version of theorem -------*)
   2.260 -Goal "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)";
   2.261 -by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse,
   2.262 -    LIMSEQ_NSLIMSEQ_iff]) 1);
   2.263 -qed "LIMSEQ_inverse";
   2.264 -
   2.265 -Goal "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] \
   2.266 -\     ==> (%n. X n / Y n) ----NS> a/b";
   2.267 -by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse, 
   2.268 -                                           real_divide_def]) 1);
   2.269 -qed "NSLIMSEQ_mult_inverse";
   2.270 -
   2.271 -Goal "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b";
   2.272 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse, 
   2.273 -                                           real_divide_def]) 1);
   2.274 -qed "LIMSEQ_divide";
   2.275 -
   2.276 -(*-----------------------------------------------
   2.277 -            Uniqueness of limit
   2.278 - ----------------------------------------------*)
   2.279 -Goalw [NSLIMSEQ_def] 
   2.280 -     "[| X ----NS> a; X ----NS> b |] ==> a = b";
   2.281 -by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
   2.282 -by (auto_tac (claset() addDs [approx_trans3], simpset()));
   2.283 -qed "NSLIMSEQ_unique";
   2.284 -
   2.285 -Goal "[| X ----> a; X ----> b |] ==> a = b";
   2.286 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   2.287 -    NSLIMSEQ_unique]) 1);
   2.288 -qed "LIMSEQ_unique";
   2.289 -
   2.290 -(*-----------------------------------------------------------------
   2.291 -    theorems about nslim and lim
   2.292 - ----------------------------------------------------------------*)
   2.293 -Goalw [lim_def] "X ----> L ==> lim X = L";
   2.294 -by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
   2.295 -qed "limI";
   2.296 -
   2.297 -Goalw [nslim_def] "X ----NS> L ==> nslim X = L";
   2.298 -by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
   2.299 -qed "nslimI";
   2.300 -
   2.301 -Goalw [lim_def,nslim_def] "lim X = nslim X";
   2.302 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
   2.303 -qed "lim_nslim_iff";
   2.304 -
   2.305 -(*------------------------------------------------------------------
   2.306 -                      Convergence
   2.307 - -----------------------------------------------------------------*)
   2.308 -Goalw [convergent_def]
   2.309 -     "convergent X ==> EX L. (X ----> L)";
   2.310 -by (assume_tac 1);
   2.311 -qed "convergentD";
   2.312 -
   2.313 -Goalw [convergent_def]
   2.314 -     "(X ----> L) ==> convergent X";
   2.315 -by (Blast_tac 1);
   2.316 -qed "convergentI";
   2.317 -
   2.318 -Goalw [NSconvergent_def]
   2.319 -     "NSconvergent X ==> EX L. (X ----NS> L)";
   2.320 -by (assume_tac 1);
   2.321 -qed "NSconvergentD";
   2.322 -
   2.323 -Goalw [NSconvergent_def]
   2.324 -     "(X ----NS> L) ==> NSconvergent X";
   2.325 -by (Blast_tac 1);
   2.326 -qed "NSconvergentI";
   2.327 -
   2.328 -Goalw [convergent_def,NSconvergent_def] 
   2.329 -     "convergent X = NSconvergent X";
   2.330 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
   2.331 -qed "convergent_NSconvergent_iff";
   2.332 -
   2.333 -Goalw [NSconvergent_def,nslim_def] 
   2.334 -     "NSconvergent X = (X ----NS> nslim X)";
   2.335 -by (auto_tac (claset() addIs [someI], simpset()));
   2.336 -qed "NSconvergent_NSLIMSEQ_iff";
   2.337 -
   2.338 -Goalw [convergent_def,lim_def] 
   2.339 -     "convergent X = (X ----> lim X)";
   2.340 -by (auto_tac (claset() addIs [someI], simpset()));
   2.341 -qed "convergent_LIMSEQ_iff";
   2.342 -
   2.343 -(*-------------------------------------------------------------------
   2.344 -         Subsequence (alternative definition) (e.g. Hoskins)
   2.345 - ------------------------------------------------------------------*)
   2.346 -Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
   2.347 -by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
   2.348 -by (induct_tac "k" 1);
   2.349 -by (auto_tac (claset() addIs [less_trans], simpset()));
   2.350 -qed "subseq_Suc_iff";
   2.351 -
   2.352 -(*-------------------------------------------------------------------
   2.353 -                   Monotonicity
   2.354 - ------------------------------------------------------------------*)
   2.355 -
   2.356 -Goalw [monoseq_def]
   2.357 -   "monoseq X = ((ALL n. X n <= X (Suc n)) \
   2.358 -\                | (ALL n. X (Suc n) <= X n))";
   2.359 -by (auto_tac (claset () addSDs [le_imp_less_or_eq], simpset()));
   2.360 -by (auto_tac (claset() addSIs [lessI RS less_imp_le]
   2.361 -                       addSDs [less_imp_Suc_add], 
   2.362 -    simpset()));
   2.363 -by (induct_tac "ka" 1);
   2.364 -by (auto_tac (claset() addIs [order_trans], simpset()));
   2.365 -by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
   2.366 -by (induct_tac "k" 1);
   2.367 -by (auto_tac (claset() addIs [order_trans], simpset()));
   2.368 -qed "monoseq_Suc";
   2.369 -
   2.370 -Goalw [monoseq_def] 
   2.371 -       "ALL m n. m <= n --> X m <= X n ==> monoseq X";
   2.372 -by (Blast_tac 1);
   2.373 -qed "monoI1";
   2.374 -
   2.375 -Goalw [monoseq_def] 
   2.376 -       "ALL m n. m <= n --> X n <= X m ==> monoseq X";
   2.377 -by (Blast_tac 1);
   2.378 -qed "monoI2";
   2.379 -
   2.380 -Goal "ALL n. X n <= X (Suc n) ==> monoseq X";
   2.381 -by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
   2.382 -qed "mono_SucI1";
   2.383 -
   2.384 -Goal "ALL n. X (Suc n) <= X n ==> monoseq X";
   2.385 -by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
   2.386 -qed "mono_SucI2";
   2.387 -
   2.388 -(*-------------------------------------------------------------------
   2.389 -                  Bounded Sequence
   2.390 - ------------------------------------------------------------------*)
   2.391 -Goalw [Bseq_def] 
   2.392 -      "Bseq X ==> EX K. 0 < K & (ALL n. abs(X n) <= K)";
   2.393 -by (assume_tac 1);
   2.394 -qed "BseqD";
   2.395 -
   2.396 -Goalw [Bseq_def]
   2.397 -      "[| 0 < K; ALL n. abs(X n) <= K |] ==> Bseq X";
   2.398 -by (Blast_tac 1);
   2.399 -qed "BseqI";
   2.400 -
   2.401 -Goal "(EX K. 0 < K & (ALL n. abs(X n) <= K)) = \
   2.402 -\     (EX N. ALL n. abs(X n) <= real(Suc N))";
   2.403 -by Auto_tac;
   2.404 -by (Force_tac 2);
   2.405 -by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
   2.406 -by (Clarify_tac 1); 
   2.407 -by (res_inst_tac [("x","n")] exI 1); 
   2.408 -by (Clarify_tac 1); 
   2.409 -by (dres_inst_tac [("x","na")] spec 1); 
   2.410 -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
   2.411 -qed "lemma_NBseq_def";
   2.412 -
   2.413 -(* alternative definition for Bseq *)
   2.414 -Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real(Suc N))";
   2.415 -by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
   2.416 -qed "Bseq_iff";
   2.417 -
   2.418 -Goal "(EX K. 0 < K & (ALL n. abs(X n) <= K)) = \
   2.419 -\     (EX N. ALL n. abs(X n) < real(Suc N))";
   2.420 -by (stac lemma_NBseq_def 1); 
   2.421 -by Auto_tac;
   2.422 -by (res_inst_tac [("x","Suc N")] exI 1); 
   2.423 -by (res_inst_tac [("x","N")] exI 2); 
   2.424 -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
   2.425 -by (blast_tac (claset() addIs [order_less_imp_le]) 2);
   2.426 -by (dres_inst_tac [("x","n")] spec 1); 
   2.427 -by (Asm_simp_tac 1); 
   2.428 -qed "lemma_NBseq_def2";
   2.429 -
   2.430 -(* yet another definition for Bseq *)
   2.431 -Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real(Suc N))";
   2.432 -by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
   2.433 -qed "Bseq_iff1a";
   2.434 -
   2.435 -Goalw [NSBseq_def]
   2.436 -     "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite";
   2.437 -by (Blast_tac 1);
   2.438 -qed "NSBseqD";
   2.439 -
   2.440 -Goalw [NSBseq_def]
   2.441 -     "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X";
   2.442 -by (assume_tac 1);
   2.443 -qed "NSBseqI";
   2.444 -
   2.445 -(*-----------------------------------------------------------
   2.446 -       Standard definition ==> NS definition
   2.447 - ----------------------------------------------------------*)
   2.448 -(* a few lemmas *)
   2.449 -Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
   2.450 -by (Auto_tac);
   2.451 -qed "lemma_Bseq";
   2.452 -
   2.453 -Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
   2.454 -by (Step_tac 1);
   2.455 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   2.456 -by (auto_tac (claset(),
   2.457 -              simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff,
   2.458 -                                  HNatInfinite_FreeUltrafilterNat_iff]));
   2.459 -by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
   2.460 -by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
   2.461 -by (res_inst_tac [("x","K+1")] exI 1);
   2.462 -by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1);
   2.463 -by (Ultra_tac 1);
   2.464 -qed "Bseq_NSBseq";
   2.465 -
   2.466 -(*---------------------------------------------------------------
   2.467 -       NS  definition ==> Standard definition
   2.468 - ---------------------------------------------------------------*)
   2.469 -(* similar to NSLIM proof in REALTOPOS *)
   2.470 -(*------------------------------------------------------------------- 
   2.471 -   We need to get rid of the real variable and do so by proving the
   2.472 -   following which relies on the Archimedean property of the reals
   2.473 -   When we skolemize we then get the required function f::nat=>nat 
   2.474 -   o/w we would be stuck with a skolem function f :: real=>nat which
   2.475 -   is not what we want (read useless!)
   2.476 - -------------------------------------------------------------------*)
   2.477 - 
   2.478 -Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
   2.479 -\          ==> ALL N. EX n. real(Suc N) < abs (X n)";
   2.480 -by (Step_tac 1);
   2.481 -by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
   2.482 -by (Blast_tac 1);
   2.483 -qed "lemmaNSBseq";
   2.484 -
   2.485 -Goal "ALL K. 0 < K --> (EX n. K < abs (X n)) \
   2.486 -\         ==> EX f. ALL N. real(Suc N) < abs (X (f N))";
   2.487 -by (dtac lemmaNSBseq 1);
   2.488 -by (dtac choice 1);
   2.489 -by (Blast_tac 1);
   2.490 -qed "lemmaNSBseq2";
   2.491 -
   2.492 -Goal "ALL N. real(Suc N) < abs (X (f N)) \
   2.493 -\         ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite";
   2.494 -by (auto_tac (claset(),
   2.495 -              simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
   2.496 -by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
   2.497 -by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
   2.498 -by (dtac FreeUltrafilterNat_all 1);
   2.499 -by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); 
   2.500 -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
   2.501 -qed "real_seq_to_hypreal_HInfinite";
   2.502 -
   2.503 -(*-----------------------------------------------------------------------------
   2.504 -     Now prove that we can get out an infinite hypernatural as well 
   2.505 -     defined using the skolem function f::nat=>nat above
   2.506 - ----------------------------------------------------------------------------*)
   2.507 -
   2.508 -Goal "{n. f n <= Suc u & real(Suc n) < abs (X (f n))} <= \
   2.509 -\         {n. f n <= u & real(Suc n) < abs (X (f n))} \
   2.510 -\         Un {n. real(Suc n) < abs (X (Suc u))}";
   2.511 -by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
   2.512 -qed "lemma_finite_NSBseq";
   2.513 -
   2.514 -Goal "finite {n. f n <= (u::nat) &  real(Suc n) < abs(X(f n))}";
   2.515 -by (induct_tac "u" 1);
   2.516 -by (res_inst_tac [("B","{n. real(Suc n) < abs(X 0)}")] finite_subset 1);
   2.517 -by (Force_tac 1); 
   2.518 -by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
   2.519 -by (auto_tac (claset() addIs [finite_real_of_nat_less_real], 
   2.520 -              simpset() addsimps [real_of_nat_Suc, less_diff_eq RS sym]));
   2.521 -qed "lemma_finite_NSBseq2";
   2.522 -
   2.523 -Goal "ALL N. real(Suc N) < abs (X (f N)) \
   2.524 -\     ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
   2.525 -by (auto_tac (claset(),
   2.526 -              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   2.527 -by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
   2.528 -by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
   2.529 -by (asm_full_simp_tac (simpset() addsimps 
   2.530 -   [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
   2.531 -\   = {n. f n <= u}" [le_def]]) 1);
   2.532 -by (dtac FreeUltrafilterNat_all 1);
   2.533 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   2.534 -by (auto_tac (claset(), 
   2.535 -     simpset() addsimps 
   2.536 -    [CLAIM "({n. f n <= u} Int {n. real(Suc n) < abs(X(f n))}) = \
   2.537 -\          {n. f n <= (u::nat) &  real(Suc n) < abs(X(f n))}",
   2.538 -     lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
   2.539 -qed "HNatInfinite_skolem_f";
   2.540 -
   2.541 -Goalw [Bseq_def,NSBseq_def] 
   2.542 -      "NSBseq X ==> Bseq X";
   2.543 -by (rtac ccontr 1);
   2.544 -by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));
   2.545 -by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
   2.546 -by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
   2.547 -by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
   2.548 -by (auto_tac (claset(), 
   2.549 -              simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff]));
   2.550 -qed "NSBseq_Bseq";
   2.551 -
   2.552 -(*----------------------------------------------------------------------
   2.553 -  Equivalence of nonstandard and standard definitions 
   2.554 -  for a bounded sequence
   2.555 - -----------------------------------------------------------------------*)
   2.556 -Goal "(Bseq X) = (NSBseq X)";
   2.557 -by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1);
   2.558 -qed "Bseq_NSBseq_iff";
   2.559 -
   2.560 -(*----------------------------------------------------------------------
   2.561 -   A convergent sequence is bounded
   2.562 -   (Boundedness as a necessary condition for convergence)
   2.563 - -----------------------------------------------------------------------*)
   2.564 -(* easier --- nonstandard version - no existential as usual *)
   2.565 -Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
   2.566 -          "NSconvergent X ==> NSBseq X";
   2.567 -by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
   2.568 -               (approx_sym RSN (2,approx_HFinite))]) 1);
   2.569 -qed "NSconvergent_NSBseq";
   2.570 -
   2.571 -(* standard version - easily now proved using *)
   2.572 -(* equivalence of NS and standard definitions *)
   2.573 -Goal "convergent X ==> Bseq X";
   2.574 -by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
   2.575 -    convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
   2.576 -qed "convergent_Bseq";
   2.577 -
   2.578 -(*----------------------------------------------------------------------
   2.579 -             Results about Ubs and Lubs of bounded sequences
   2.580 - -----------------------------------------------------------------------*)
   2.581 -Goalw [Bseq_def]
   2.582 -  "!!(X::nat=>real). Bseq X ==> \
   2.583 -\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
   2.584 -by (auto_tac (claset() addIs [isUbI,setleI],
   2.585 -    simpset() addsimps [abs_le_interval_iff]));
   2.586 -qed "Bseq_isUb";
   2.587 -
   2.588 -(*----------------------------------------------------------------------
   2.589 -   Use completeness of reals (supremum property) 
   2.590 -   to show that any bounded sequence has a lub 
   2.591 ------------------------------------------------------------------------*)
   2.592 -Goal
   2.593 -  "!!(X::nat=>real). Bseq X ==> \
   2.594 -\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
   2.595 -by (blast_tac (claset() addIs [reals_complete,
   2.596 -    Bseq_isUb]) 1);
   2.597 -qed "Bseq_isLub";
   2.598 -
   2.599 -(* nonstandard version of premise will be *)
   2.600 -(* handy when we work in NS universe      *)
   2.601 -Goal   "NSBseq X ==> \
   2.602 -\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
   2.603 -by (asm_full_simp_tac (simpset() addsimps 
   2.604 -    [Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
   2.605 -qed "NSBseq_isUb";
   2.606 -
   2.607 -Goal
   2.608 -  "NSBseq X ==> \
   2.609 -\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
   2.610 -by (asm_full_simp_tac (simpset() addsimps 
   2.611 -    [Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
   2.612 -qed "NSBseq_isLub";
   2.613 -
   2.614 -(*--------------------------------------------------------------------
   2.615 -             Bounded and monotonic sequence converges              
   2.616 - --------------------------------------------------------------------*)
   2.617 -(* lemmas *)
   2.618 -Goal 
   2.619 -     "!!(X::nat=>real). [| ALL m n. m <= n -->  X m <= X n; \
   2.620 -\                 isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \
   2.621 -\              |] ==> ALL n. ma <= n --> X n = X ma";
   2.622 -by (Step_tac 1);
   2.623 -by (dres_inst_tac [("y","X n")] isLubD2 1);
   2.624 -by (ALLGOALS(blast_tac (claset() addDs [order_antisym])));
   2.625 -qed "lemma_converg1";
   2.626 -
   2.627 -(*------------------------------------------------------------------- 
   2.628 -   The best of both world: Easier to prove this result as a standard
   2.629 -   theorem and then use equivalence to "transfer" it into the
   2.630 -   equivalent nonstandard form if needed!
   2.631 - -------------------------------------------------------------------*)
   2.632 -Goalw [LIMSEQ_def] 
   2.633 -         "ALL n. m <= n --> X n = X m \
   2.634 -\         ==> EX L. (X ----> L)";  
   2.635 -by (res_inst_tac [("x","X m")] exI 1);
   2.636 -by (Step_tac 1);
   2.637 -by (res_inst_tac [("x","m")] exI 1);
   2.638 -by (Step_tac 1);
   2.639 -by (dtac spec 1 THEN etac impE 1);
   2.640 -by (Auto_tac);
   2.641 -qed "Bmonoseq_LIMSEQ";
   2.642 -
   2.643 -(* Now same theorem in terms of NS limit *)
   2.644 -Goal "ALL n. m <= n --> X n = X m \
   2.645 -\         ==> EX L. (X ----NS> L)";  
   2.646 -by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
   2.647 -    simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
   2.648 -qed "Bmonoseq_NSLIMSEQ";
   2.649 -
   2.650 -(* a few more lemmas *)
   2.651 -Goal "!!(X::nat=>real). \
   2.652 -\ [| ALL m. X m ~= U;  isLub UNIV {x. EX n. X n = x} U |] ==> ALL m. X m < U";
   2.653 -by (Step_tac 1);
   2.654 -by (dres_inst_tac [("y","X m")] isLubD2 1);
   2.655 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq],
   2.656 -              simpset()));
   2.657 -qed "lemma_converg2";
   2.658 -
   2.659 -Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
   2.660 -\         isUb UNIV {x. EX n. X n = x} U";
   2.661 -by (rtac (setleI RS isUbI) 1);
   2.662 -by (Auto_tac);
   2.663 -qed "lemma_converg3";
   2.664 -
   2.665 -(* FIXME: U - T < U redundant *)
   2.666 -Goal "!!(X::nat=> real). \
   2.667 -\              [| ALL m. X m ~= U; \
   2.668 -\                 isLub UNIV {x. EX n. X n = x} U; \
   2.669 -\                 0 < T; \
   2.670 -\                 U + - T < U \
   2.671 -\              |] ==> EX m. U + -T < X m & X m < U";
   2.672 -by (dtac lemma_converg2 1 THEN assume_tac 1);
   2.673 -by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
   2.674 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
   2.675 -by (dtac lemma_converg3 1);
   2.676 -by (dtac isLub_le_isUb 1 THEN assume_tac 1);
   2.677 -by (auto_tac (claset() addDs [order_less_le_trans],
   2.678 -              simpset()));
   2.679 -qed "lemma_converg4";
   2.680 -
   2.681 -(*-------------------------------------------------------------------
   2.682 -  A standard proof of the theorem for monotone increasing sequence
   2.683 - ------------------------------------------------------------------*)
   2.684 -
   2.685 -Goalw [convergent_def] 
   2.686 -     "[| Bseq X; ALL m n. m <= n --> X m <= X n |] \
   2.687 -\                ==> convergent X";
   2.688 -by (ftac Bseq_isLub 1);
   2.689 -by (Step_tac 1);
   2.690 -by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
   2.691 -by (blast_tac (claset() addDs [lemma_converg1,
   2.692 -    Bmonoseq_LIMSEQ]) 1);
   2.693 -(* second case *)
   2.694 -by (res_inst_tac [("x","U")] exI 1);
   2.695 -by (stac LIMSEQ_iff 1 THEN Step_tac 1);
   2.696 -by (ftac lemma_converg2 1 THEN assume_tac 1);
   2.697 -by (dtac lemma_converg4 1 THEN Auto_tac);
   2.698 -by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
   2.699 -by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
   2.700 -by (rotate_tac 3 1 THEN dres_inst_tac [("x","n")] spec 1);
   2.701 -by (arith_tac 1);
   2.702 -qed "Bseq_mono_convergent";
   2.703 -
   2.704 -(* NS version of theorem *)
   2.705 -Goalw [convergent_def] 
   2.706 -     "[| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
   2.707 -\                ==> NSconvergent X";
   2.708 -by (auto_tac (claset() addIs [Bseq_mono_convergent], 
   2.709 -    simpset() addsimps [convergent_NSconvergent_iff RS sym,
   2.710 -    Bseq_NSBseq_iff RS sym]));
   2.711 -qed "NSBseq_mono_NSconvergent";
   2.712 -
   2.713 -Goalw [convergent_def] 
   2.714 -      "(convergent X) = (convergent (%n. -(X n)))";
   2.715 -by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
   2.716 -by (dtac LIMSEQ_minus 1 THEN Auto_tac);
   2.717 -qed "convergent_minus_iff";
   2.718 -
   2.719 -Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
   2.720 -by (Asm_full_simp_tac 1);
   2.721 -qed "Bseq_minus_iff";
   2.722 -
   2.723 -(*--------------------------------
   2.724 -   **** main mono theorem ****
   2.725 - -------------------------------*)
   2.726 -Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
   2.727 -by (Step_tac 1);
   2.728 -by (stac convergent_minus_iff 2);
   2.729 -by (dtac (Bseq_minus_iff RS ssubst) 2);
   2.730 -by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
   2.731 -qed "Bseq_monoseq_convergent";
   2.732 -
   2.733 -(*----------------------------------------------------------------
   2.734 -          A few more equivalence theorems for boundedness 
   2.735 - ---------------------------------------------------------------*)
   2.736 - 
   2.737 -(***--- alternative formulation for boundedness---***)
   2.738 -Goalw [Bseq_def] 
   2.739 -   "Bseq X = (EX k x. 0 < k & (ALL n. abs(X(n) + -x) <= k))";
   2.740 -by (Step_tac 1);
   2.741 -by (res_inst_tac [("x","k + abs(x)")] exI 2);
   2.742 -by (res_inst_tac [("x","K")] exI 1);
   2.743 -by (res_inst_tac [("x","0")] exI 1);
   2.744 -by (Auto_tac);
   2.745 -by (ALLGOALS (dres_inst_tac [("x","n")] spec));
   2.746 -by (ALLGOALS arith_tac);
   2.747 -qed "Bseq_iff2";
   2.748 -
   2.749 -(***--- alternative formulation for boundedness ---***)
   2.750 -Goal "Bseq X = (EX k N. 0 < k & (ALL n. abs(X(n) + -X(N)) <= k))";
   2.751 -by (Step_tac 1);
   2.752 -by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
   2.753 -by (Step_tac 1);
   2.754 -by (res_inst_tac [("x","K + abs(X N)")] exI 1);
   2.755 -by (Auto_tac);
   2.756 -by (arith_tac 1);
   2.757 -by (res_inst_tac [("x","N")] exI 1);
   2.758 -by (Step_tac 1);
   2.759 -by (dres_inst_tac [("x","n")] spec 1);
   2.760 -by (arith_tac 1);
   2.761 -by (auto_tac (claset(), simpset() addsimps [Bseq_iff2]));
   2.762 -qed "Bseq_iff3";
   2.763 -
   2.764 -Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
   2.765 -by (res_inst_tac [("x","(abs(k) + abs(K)) + 1")] exI 1);
   2.766 -by (Auto_tac);
   2.767 -by (dres_inst_tac [("x","n")] spec 2);
   2.768 -by (ALLGOALS arith_tac);
   2.769 -qed "BseqI2";
   2.770 -
   2.771 -(*-------------------------------------------------------------------
   2.772 -   Equivalence between NS and standard definitions of Cauchy seqs
   2.773 - ------------------------------------------------------------------*)
   2.774 -(*-------------------------------
   2.775 -      Standard def => NS def
   2.776 - -------------------------------*)
   2.777 -Goal "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite \
   2.778 -\         ==> {n. M <= x n} : FreeUltrafilterNat";
   2.779 -by (auto_tac (claset(),
   2.780 -              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   2.781 -by (dres_inst_tac [("x","M")] spec 1);
   2.782 -by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
   2.783 -qed "lemmaCauchy1";
   2.784 -
   2.785 -Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
   2.786 -\     {n. M <= xa n} Int {n. M <= x n} <= \
   2.787 -\     {n. abs (X (xa n) + - X (x n)) < u}";
   2.788 -by (Blast_tac 1);
   2.789 -qed "lemmaCauchy2";
   2.790 -
   2.791 -Goalw [Cauchy_def,NSCauchy_def] 
   2.792 -      "Cauchy X ==> NSCauchy X";
   2.793 -by (Step_tac 1);
   2.794 -by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
   2.795 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   2.796 -by (rtac (approx_minus_iff RS iffD2) 1);
   2.797 -by (rtac (mem_infmal_iff RS iffD1) 1);
   2.798 -by (auto_tac (claset(),
   2.799 -              simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
   2.800 -                                  Infinitesimal_FreeUltrafilterNat_iff]));
   2.801 -by (EVERY[rtac bexI 1, Auto_tac]);
   2.802 -by (dtac spec 1 THEN Auto_tac);
   2.803 -by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
   2.804 -by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
   2.805 -by (res_inst_tac [("x1","xa")] 
   2.806 -    (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
   2.807 -by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
   2.808 -by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
   2.809 -        FreeUltrafilterNat_Nat_set], simpset()));
   2.810 -qed "Cauchy_NSCauchy";
   2.811 -
   2.812 -(*-----------------------------------------------
   2.813 -     NS def => Standard def -- rather long but 
   2.814 -     straightforward proof in this case
   2.815 - ---------------------------------------------*)
   2.816 -Goalw [Cauchy_def,NSCauchy_def] 
   2.817 -      "NSCauchy X ==> Cauchy X";
   2.818 -by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
   2.819 -by (dtac choice 1 THEN 
   2.820 -    auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
   2.821 -by (dtac choice 1 THEN 
   2.822 -    step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
   2.823 -by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
   2.824 -by (dtac bspec 1 THEN assume_tac 1);
   2.825 -by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {fa})")] bspec 1 
   2.826 -    THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
   2.827 -by (dtac (approx_minus_iff RS iffD1) 1);
   2.828 -by (dtac (mem_infmal_iff RS iffD2) 1);
   2.829 -by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
   2.830 -    hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
   2.831 -by (rename_tac "Y" 1);
   2.832 -by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
   2.833 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   2.834 -by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
   2.835 -\         {n. abs (Y n) < e} <= \
   2.836 -\         {n. abs (X (f n) + - X (fa n)) < e}" RSN 
   2.837 -          (2,FreeUltrafilterNat_subset)) 1);
   2.838 -by (thin_tac "{n. abs (Y n) < e} : FreeUltrafilterNat" 1);
   2.839 -by (dtac FreeUltrafilterNat_all 1);
   2.840 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   2.841 -by (asm_full_simp_tac (simpset() addsimps 
   2.842 -    [CLAIM "{n. abs (X (f n) + - X (fa n)) < e} Int \
   2.843 -\         {M. ~ abs (X (f M) + - X (fa M)) < e} = {}",
   2.844 -     FreeUltrafilterNat_empty]) 1);
   2.845 -qed "NSCauchy_Cauchy";
   2.846 -
   2.847 -(*----- Equivalence -----*)
   2.848 -Goal "NSCauchy X = Cauchy X";
   2.849 -by (blast_tac (claset() addSIs[NSCauchy_Cauchy,
   2.850 -    Cauchy_NSCauchy]) 1);
   2.851 -qed "NSCauchy_Cauchy_iff";
   2.852 -
   2.853 -(*-------------------------------------------------------
   2.854 -  Cauchy sequence is bounded -- this is the standard 
   2.855 -  proof mechanization rather than the nonstandard proof 
   2.856 - -------------------------------------------------------*)
   2.857 -
   2.858 -(***-------------  VARIOUS LEMMAS --------------***)
   2.859 -Goal "ALL n. M <= n --> abs (X M + - X n) < (1::real) \
   2.860 -\         ==>  ALL n. M <= n --> abs(X n) < 1 + abs(X M)";
   2.861 -by (Step_tac 1);
   2.862 -by (dtac spec 1 THEN Auto_tac);
   2.863 -by (arith_tac 1);
   2.864 -qed "lemmaCauchy";
   2.865 -
   2.866 -Goal "(n < Suc M) = (n <= M)";
   2.867 -by Auto_tac;
   2.868 -qed "less_Suc_cancel_iff";
   2.869 -
   2.870 -(* FIXME: Long. Maximal element in subsequence *)
   2.871 -Goal "EX m. m <= M & (ALL n. n <= M --> \
   2.872 -\         abs ((X::nat=> real) n) <= abs (X m))";
   2.873 -by (induct_tac "M" 1);
   2.874 -by (res_inst_tac [("x","0")] exI 1);
   2.875 -by (Asm_full_simp_tac 1);
   2.876 -by (Step_tac 1);
   2.877 -by (cut_inst_tac [("x","abs (X (Suc n))"),("y","abs(X m)")]
   2.878 -        linorder_less_linear 1);
   2.879 -by (Step_tac 1);
   2.880 -by (res_inst_tac [("x","m")] exI 1);
   2.881 -by (res_inst_tac [("x","m")] exI 2);
   2.882 -by (res_inst_tac [("x","Suc n")] exI 3);
   2.883 -by (ALLGOALS(Asm_full_simp_tac));
   2.884 -by (Step_tac 1);
   2.885 -by (ALLGOALS(eres_inst_tac [("m1","na")] 
   2.886 -    (le_imp_less_or_eq RS disjE)));
   2.887 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
   2.888 -    [less_Suc_cancel_iff, order_less_imp_le])));
   2.889 -by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
   2.890 -qed "SUP_rabs_subseq";
   2.891 -
   2.892 -(* lemmas to help proof - mostly trivial *)
   2.893 -Goal "[| ALL m::nat. m <= M --> P M m; \
   2.894 -\        ALL m. M <= m --> P M m |] \
   2.895 -\     ==> ALL m. P M m";
   2.896 -by (Step_tac 1);
   2.897 -by (REPEAT(dres_inst_tac [("x","m")] spec 1));
   2.898 -by (auto_tac (claset() addEs [less_asym],
   2.899 -    simpset() addsimps [le_def]));
   2.900 -qed "lemma_Nat_covered";
   2.901 -
   2.902 -Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a;  a < b |] \
   2.903 -\     ==> ALL n. n <= M --> abs(X n) <= b";
   2.904 -by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
   2.905 -qed "lemma_trans1";
   2.906 -
   2.907 -Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
   2.908 -\        a < b |] \
   2.909 -\     ==> ALL n. M <= n --> abs(X n)<= b";
   2.910 -by (blast_tac (claset() addIs [order_less_trans RS order_less_imp_le]) 1);
   2.911 -qed "lemma_trans2";
   2.912 -
   2.913 -Goal "[| ALL n. n <= M --> abs (X n) <= a; \
   2.914 -\        a = b |] \
   2.915 -\     ==> ALL n. n <= M --> abs(X n) <= b";
   2.916 -by (Auto_tac);
   2.917 -qed "lemma_trans3";
   2.918 -
   2.919 -Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
   2.920 -\             ==>  ALL n. M <= n --> abs (X n) <= a";
   2.921 -by (blast_tac (claset() addIs [order_less_imp_le]) 1);
   2.922 -qed "lemma_trans4";
   2.923 -
   2.924 -(*---------------------------------------------------------- 
   2.925 -   Trickier than expected --- proof is more involved than
   2.926 -   outlines sketched by various authors would suggest
   2.927 - ---------------------------------------------------------*)
   2.928 -Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X";
   2.929 -by (dres_inst_tac [("x","1")] spec 1);
   2.930 -by (etac (zero_less_one RSN (2,impE)) 1);
   2.931 -by (Step_tac 1);
   2.932 -by (dres_inst_tac [("x","M")] spec 1);
   2.933 -by (Asm_full_simp_tac 1);
   2.934 -by (dtac lemmaCauchy 1);
   2.935 -by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
   2.936 -by (Step_tac 1);
   2.937 -by (cut_inst_tac [("x","abs(X m)"),
   2.938 -     ("y","1 + abs(X M)")] linorder_less_linear 1);
   2.939 -by (Step_tac 1);
   2.940 -by (dtac lemma_trans1 1 THEN assume_tac 1);
   2.941 -by (dtac lemma_trans2 3 THEN assume_tac 3);
   2.942 -by (dtac lemma_trans3 2 THEN assume_tac 2);
   2.943 -by (dtac (abs_add_one_gt_zero RS order_less_trans) 3);
   2.944 -by (dtac lemma_trans4 1);
   2.945 -by (dtac lemma_trans4 2);
   2.946 -by (res_inst_tac [("x","1 + abs(X M)")] exI 1);
   2.947 -by (res_inst_tac [("x","1 + abs(X M)")] exI 2);
   2.948 -by (res_inst_tac [("x","abs(X m)")] exI 3);
   2.949 -by (auto_tac (claset() addSEs [lemma_Nat_covered],
   2.950 -              simpset()));
   2.951 -by (ALLGOALS arith_tac);
   2.952 -qed "Cauchy_Bseq";
   2.953 -
   2.954 -(*------------------------------------------------
   2.955 -  Cauchy sequence is bounded -- NSformulation
   2.956 - ------------------------------------------------*)
   2.957 -Goal "NSCauchy X ==> NSBseq X";
   2.958 -by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq,
   2.959 -    Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1);
   2.960 -qed "NSCauchy_NSBseq";
   2.961 -
   2.962 -
   2.963 -(*-----------------------------------------------------------------
   2.964 -          Equivalence of Cauchy criterion and convergence
   2.965 -  
   2.966 -  We will prove this using our NS formulation which provides a
   2.967 -  much easier proof than using the standard definition. We do not 
   2.968 -  need to use properties of subsequences such as boundedness, 
   2.969 -  monotonicity etc... Compare with Harrison's corresponding proof
   2.970 -  in HOL which is much longer and more complicated. Of course, we do
   2.971 -  not have problems which he encountered with guessing the right 
   2.972 -  instantiations for his 'espsilon-delta' proof(s) in this case
   2.973 -  since the NS formulations do not involve existential quantifiers.
   2.974 - -----------------------------------------------------------------*)
   2.975 -Goalw [NSconvergent_def,NSLIMSEQ_def]
   2.976 -      "NSCauchy X = NSconvergent X";
   2.977 -by (Step_tac 1);
   2.978 -by (ftac NSCauchy_NSBseq 1);
   2.979 -by (auto_tac (claset() addIs [approx_trans2], 
   2.980 -    simpset() addsimps 
   2.981 -    [NSBseq_def,NSCauchy_def]));
   2.982 -by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
   2.983 -by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
   2.984 -by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
   2.985 -              addsimps [SReal_iff]));
   2.986 -by (blast_tac (claset() addIs [approx_trans3]) 1);
   2.987 -qed "NSCauchy_NSconvergent_iff";
   2.988 -
   2.989 -(* Standard proof for free *)
   2.990 -Goal "Cauchy X = convergent X";
   2.991 -by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym,
   2.992 -    convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1);
   2.993 -qed "Cauchy_convergent_iff";
   2.994 -
   2.995 -(*-----------------------------------------------------------------
   2.996 -     We can now try and derive a few properties of sequences
   2.997 -     starting with the limit comparison property for sequences
   2.998 - -----------------------------------------------------------------*)
   2.999 -Goalw [NSLIMSEQ_def]
  2.1000 -       "[| f ----NS> l; g ----NS> m; \
  2.1001 -\                  EX N. ALL n. N <= n --> f(n) <= g(n) \
  2.1002 -\               |] ==> l <= m";
  2.1003 -by (Step_tac 1);
  2.1004 -by (dtac starfun_le_mono 1);
  2.1005 -by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
  2.1006 -by (dres_inst_tac [("x","whn")] spec 1);
  2.1007 -by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
  2.1008 -by Auto_tac;
  2.1009 -by (auto_tac (claset() addIs 
  2.1010 -    [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
  2.1011 -qed "NSLIMSEQ_le";
  2.1012 -
  2.1013 -(* standard version *)
  2.1014 -Goal "[| f ----> l; g ----> m; \
  2.1015 -\        EX N. ALL n. N <= n --> f(n) <= g(n) |] \
  2.1016 -\     ==> l <= m";
  2.1017 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1018 -    NSLIMSEQ_le]) 1);
  2.1019 -qed "LIMSEQ_le";
  2.1020 -
  2.1021 -(*---------------
  2.1022 -    Also...
  2.1023 - --------------*)
  2.1024 -Goal "[| X ----> r; ALL n. a <= X n |] ==> a <= r";
  2.1025 -by (rtac LIMSEQ_le 1);
  2.1026 -by (rtac LIMSEQ_const 1);
  2.1027 -by (Auto_tac);
  2.1028 -qed "LIMSEQ_le_const";
  2.1029 -
  2.1030 -Goal "[| X ----NS> r; ALL n. a <= X n |] ==> a <= r";
  2.1031 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1032 -    LIMSEQ_le_const]) 1);
  2.1033 -qed "NSLIMSEQ_le_const";
  2.1034 -
  2.1035 -Goal "[| X ----> r; ALL n. X n <= a |] ==> r <= a";
  2.1036 -by (rtac LIMSEQ_le 1);
  2.1037 -by (rtac LIMSEQ_const 2);
  2.1038 -by (Auto_tac);
  2.1039 -qed "LIMSEQ_le_const2";
  2.1040 -
  2.1041 -Goal "[| X ----NS> r; ALL n. X n <= a |] ==> r <= a";
  2.1042 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1043 -    LIMSEQ_le_const2]) 1);
  2.1044 -qed "NSLIMSEQ_le_const2";
  2.1045 -
  2.1046 -(*-----------------------------------------------------
  2.1047 -            Shift a convergent series by 1
  2.1048 -  We use the fact that Cauchyness and convergence
  2.1049 -  are equivalent and also that the successor of an
  2.1050 -  infinite hypernatural is also infinite.
  2.1051 - -----------------------------------------------------*)
  2.1052 -Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
  2.1053 -by (forward_tac [NSconvergentI RS 
  2.1054 -    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  2.1055 -by (auto_tac (claset(), 
  2.1056 -     simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
  2.1057 -by (dtac bspec 1 THEN assume_tac 1);
  2.1058 -by (dtac bspec 1 THEN assume_tac 1);
  2.1059 -by (dtac (Nats_1 RSN (2,HNatInfinite_SHNat_add)) 1);
  2.1060 -by (blast_tac (claset() addIs [approx_trans3]) 1);
  2.1061 -qed "NSLIMSEQ_Suc";
  2.1062 -
  2.1063 -(* standard version *)
  2.1064 -Goal "f ----> l ==> (%n. f(Suc n)) ----> l";
  2.1065 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1066 -    NSLIMSEQ_Suc]) 1);
  2.1067 -qed "LIMSEQ_Suc";
  2.1068 -
  2.1069 -Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
  2.1070 -by (forward_tac [NSconvergentI RS 
  2.1071 -    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  2.1072 -by (auto_tac (claset(),
  2.1073 -      simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
  2.1074 -by (dtac bspec 1 THEN assume_tac 1);
  2.1075 -by (dtac bspec 1 THEN assume_tac 1);
  2.1076 -by (ftac (Nats_1 RSN (2,HNatInfinite_SHNat_diff)) 1);
  2.1077 -by (rotate_tac 2 1);
  2.1078 -by (auto_tac (claset() addSDs [bspec] addIs [approx_trans3],
  2.1079 -    simpset()));
  2.1080 -qed "NSLIMSEQ_imp_Suc";
  2.1081 -
  2.1082 -Goal "(%n. f(Suc n)) ----> l ==> f ----> l";
  2.1083 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
  2.1084 -by (etac NSLIMSEQ_imp_Suc 1);
  2.1085 -qed "LIMSEQ_imp_Suc";
  2.1086 -
  2.1087 -Goal "((%n. f(Suc n)) ----> l) = (f ----> l)";
  2.1088 -by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1);
  2.1089 -qed "LIMSEQ_Suc_iff";
  2.1090 -
  2.1091 -Goal "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)";
  2.1092 -by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1);
  2.1093 -qed "NSLIMSEQ_Suc_iff";
  2.1094 -
  2.1095 -(*-----------------------------------------------------
  2.1096 -       A sequence tends to zero iff its abs does
  2.1097 - ----------------------------------------------------*)
  2.1098 -(* we can prove this directly since proof is trivial *)
  2.1099 -Goalw [LIMSEQ_def] 
  2.1100 -      "((%n. abs(f n)) ----> 0) = (f ----> 0)";
  2.1101 -by (simp_tac (simpset() addsimps [abs_idempotent]) 1);
  2.1102 -qed "LIMSEQ_rabs_zero";
  2.1103 -
  2.1104 -(*-----------------------------------------------------*)
  2.1105 -(* We prove the NS version from the standard one       *)
  2.1106 -(* Actually pure NS proof seems more complicated       *)
  2.1107 -(* than the direct standard one above!                 *)
  2.1108 -(*-----------------------------------------------------*)
  2.1109 -
  2.1110 -Goal "((%n. abs(f n)) ----NS> 0) = (f ----NS> 0)";
  2.1111 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1112 -             LIMSEQ_rabs_zero]) 1);
  2.1113 -qed "NSLIMSEQ_rabs_zero";
  2.1114 -
  2.1115 -(*----------------------------------------
  2.1116 -    Also we have for a general limit 
  2.1117 -        (NS proof much easier)
  2.1118 - ---------------------------------------*)
  2.1119 -Goalw [NSLIMSEQ_def] 
  2.1120 -       "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
  2.1121 -by (auto_tac (claset() addIs [approx_hrabs], simpset() 
  2.1122 -    addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
  2.1123 -qed "NSLIMSEQ_imp_rabs";
  2.1124 -
  2.1125 -(* standard version *)
  2.1126 -Goal "f ----> l ==> (%n. abs(f n)) ----> abs(l)";
  2.1127 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1128 -    NSLIMSEQ_imp_rabs]) 1);
  2.1129 -qed "LIMSEQ_imp_rabs";
  2.1130 -
  2.1131 -(*-----------------------------------------------------
  2.1132 -       An unbounded sequence's inverse tends to 0
  2.1133 -  ----------------------------------------------------*)
  2.1134 -(* standard proof seems easier *)
  2.1135 -Goalw [LIMSEQ_def] 
  2.1136 -      "ALL y. EX N. ALL n. N <= n --> y < f(n) \
  2.1137 -\      ==> (%n. inverse(f n)) ----> 0";
  2.1138 -by (Step_tac 1 THEN Asm_full_simp_tac 1);
  2.1139 -by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1);
  2.1140 -by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
  2.1141 -by (dtac spec 1 THEN Auto_tac);
  2.1142 -by (ftac positive_imp_inverse_positive 1);
  2.1143 -by (ftac order_less_trans 1 THEN assume_tac 1);
  2.1144 -by (forw_inst_tac [("a","f n")] positive_imp_inverse_positive 1);
  2.1145 -by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
  2.1146 -by (res_inst_tac [("t","r")] (inverse_inverse_eq RS subst) 1);
  2.1147 -by (auto_tac (claset() addIs [inverse_less_iff_less RS iffD2], 
  2.1148 -            simpset() delsimps [inverse_inverse_eq]));
  2.1149 -qed "LIMSEQ_inverse_zero";
  2.1150 -
  2.1151 -Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
  2.1152 -\     ==> (%n. inverse(f n)) ----NS> 0";
  2.1153 -by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1154 -                  LIMSEQ_inverse_zero]) 1);
  2.1155 -qed "NSLIMSEQ_inverse_zero";
  2.1156 -
  2.1157 -(*--------------------------------------------------------------
  2.1158 -             Sequence  1/n --> 0 as n --> infinity 
  2.1159 - -------------------------------------------------------------*)
  2.1160 -
  2.1161 -Goal "(%n. inverse(real(Suc n))) ----> 0";
  2.1162 -by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1);
  2.1163 -by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
  2.1164 -by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
  2.1165 -by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
  2.1166 -qed "LIMSEQ_inverse_real_of_nat";
  2.1167 -
  2.1168 -Goal "(%n. inverse(real(Suc n))) ----NS> 0";
  2.1169 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1170 -    LIMSEQ_inverse_real_of_nat]) 1);
  2.1171 -qed "NSLIMSEQ_inverse_real_of_nat";
  2.1172 -
  2.1173 -(*--------------------------------------------
  2.1174 -    Sequence  r + 1/n --> r as n --> infinity 
  2.1175 -    now easily proved
  2.1176 - --------------------------------------------*)
  2.1177 -Goal "(%n. r + inverse(real(Suc n))) ----> r";
  2.1178 -by (cut_facts_tac
  2.1179 -    [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
  2.1180 -by Auto_tac;
  2.1181 -qed "LIMSEQ_inverse_real_of_nat_add";
  2.1182 -
  2.1183 -Goal "(%n. r + inverse(real(Suc n))) ----NS> r";
  2.1184 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1185 -    LIMSEQ_inverse_real_of_nat_add]) 1);
  2.1186 -qed "NSLIMSEQ_inverse_real_of_nat_add";
  2.1187 -
  2.1188 -(*--------------
  2.1189 -    Also...
  2.1190 - --------------*)
  2.1191 -
  2.1192 -Goal "(%n. r + -inverse(real(Suc n))) ----> r";
  2.1193 -by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
  2.1194 -                   MRS LIMSEQ_add_minus] 1);
  2.1195 -by (Auto_tac);
  2.1196 -qed "LIMSEQ_inverse_real_of_nat_add_minus";
  2.1197 -
  2.1198 -Goal "(%n. r + -inverse(real(Suc n))) ----NS> r";
  2.1199 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1200 -    LIMSEQ_inverse_real_of_nat_add_minus]) 1);
  2.1201 -qed "NSLIMSEQ_inverse_real_of_nat_add_minus";
  2.1202 -
  2.1203 -Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r";
  2.1204 -by (cut_inst_tac [("b","1")] ([LIMSEQ_const,
  2.1205 -    LIMSEQ_inverse_real_of_nat_add_minus] MRS LIMSEQ_mult) 1);
  2.1206 -by (Auto_tac);
  2.1207 -qed "LIMSEQ_inverse_real_of_nat_add_minus_mult";
  2.1208 -
  2.1209 -Goal "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r";
  2.1210 -by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  2.1211 -    LIMSEQ_inverse_real_of_nat_add_minus_mult]) 1);
  2.1212 -qed "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
  2.1213 -
  2.1214 -(*---------------------------------------------------------------
  2.1215 -                          Real Powers
  2.1216 - --------------------------------------------------------------*)
  2.1217 -Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)";
  2.1218 -by (induct_tac "m" 1);
  2.1219 -by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const],
  2.1220 -    simpset()));
  2.1221 -qed_spec_mp "NSLIMSEQ_pow";
  2.1222 -
  2.1223 -Goal "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m";
  2.1224 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  2.1225 -    NSLIMSEQ_pow]) 1);
  2.1226 -qed "LIMSEQ_pow";
  2.1227 -
  2.1228 -(*----------------------------------------------------------------
  2.1229 -               0 <= x <= 1 ==> (x ^ n ----> 0)
  2.1230 -  Proof will use (NS) Cauchy equivalence for convergence and
  2.1231 -  also fact that bounded and monotonic sequence converges.  
  2.1232 - ---------------------------------------------------------------*)
  2.1233 -Goalw [Bseq_def] "[| 0 <= x; x <= 1 |] ==> Bseq (%n. x ^ n)";
  2.1234 -by (res_inst_tac [("x","1")] exI 1);
  2.1235 -by (asm_full_simp_tac (simpset() addsimps [power_abs]) 1);
  2.1236 -by (auto_tac (claset() addDs [power_mono] 
  2.1237 -                       addIs [order_less_imp_le], 
  2.1238 -              simpset() addsimps [abs_if] ));
  2.1239 -qed "Bseq_realpow";
  2.1240 -
  2.1241 -Goal "[| 0 <= x; x <= 1 |] ==> monoseq (%n. x ^ n)";
  2.1242 -by (clarify_tac (claset() addSIs [mono_SucI2]) 1);
  2.1243 -by (cut_inst_tac [("n","n"),("N","Suc n"),("a","x")] power_decreasing 1);
  2.1244 -by Auto_tac;
  2.1245 -qed "monoseq_realpow";
  2.1246 -
  2.1247 -Goal "[| 0 <= x; x <= 1 |] ==> convergent (%n. x ^ n)";
  2.1248 -by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
  2.1249 -                                Bseq_realpow,monoseq_realpow]) 1);
  2.1250 -qed "convergent_realpow";
  2.1251 -
  2.1252 -(* We now use NS criterion to bring proof of theorem through *)
  2.1253 -
  2.1254 -
  2.1255 -Goalw [NSLIMSEQ_def]
  2.1256 -     "[| 0 <= x; x < 1 |] ==> (%n. x ^ n) ----NS> 0";
  2.1257 -by (auto_tac (claset() addSDs [convergent_realpow],
  2.1258 -              simpset() addsimps [convergent_NSconvergent_iff]));
  2.1259 -by (ftac NSconvergentD 1);
  2.1260 -by (auto_tac (claset(),
  2.1261 -        simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
  2.1262 -                            NSCauchy_def, starfunNat_pow]));
  2.1263 -by (ftac HNatInfinite_add_one 1);
  2.1264 -by (dtac bspec 1 THEN assume_tac 1);
  2.1265 -by (dtac bspec 1 THEN assume_tac 1);
  2.1266 -by (dres_inst_tac [("x","N + (1::hypnat)")] bspec 1 THEN assume_tac 1);
  2.1267 -by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
  2.1268 -by (dtac approx_mult_subst_SReal 1 THEN assume_tac 1);
  2.1269 -by (dtac approx_trans3 1 THEN assume_tac 1);
  2.1270 -by (auto_tac (claset(),
  2.1271 -              simpset() delsimps [hypreal_of_real_mult]
  2.1272 -			addsimps [hypreal_of_real_mult RS sym]));
  2.1273 -qed "NSLIMSEQ_realpow_zero";
  2.1274 -
  2.1275 -(*---------------  standard version ---------------*)
  2.1276 -Goal "[| 0 <= x; x < 1 |] ==> (%n. x ^ n) ----> 0";
  2.1277 -by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
  2.1278 -                                      LIMSEQ_NSLIMSEQ_iff]) 1);
  2.1279 -qed "LIMSEQ_realpow_zero";
  2.1280 -
  2.1281 -Goal "1 < x ==> (%n. a / (x ^ n)) ----> 0";
  2.1282 -by (cut_inst_tac [("a","a"),("x1","inverse x")] 
  2.1283 -    ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
  2.1284 -by (auto_tac (claset(), 
  2.1285 -              simpset() addsimps [real_divide_def, power_inverse])); 
  2.1286 -by (asm_simp_tac (simpset() addsimps [inverse_eq_divide,
  2.1287 -                                      pos_divide_less_eq]) 1); 
  2.1288 -qed "LIMSEQ_divide_realpow_zero";
  2.1289 -
  2.1290 -(*----------------------------------------------------------------
  2.1291 -               Limit of c^n for |c| < 1  
  2.1292 - ---------------------------------------------------------------*)
  2.1293 -Goal "abs(c) < 1 ==> (%n. abs(c) ^ n) ----> 0";
  2.1294 -by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1);
  2.1295 -qed "LIMSEQ_rabs_realpow_zero";
  2.1296 -
  2.1297 -Goal "abs(c) < 1 ==> (%n. abs(c) ^ n) ----NS> 0";
  2.1298 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero,
  2.1299 -    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
  2.1300 -qed "NSLIMSEQ_rabs_realpow_zero";
  2.1301 -
  2.1302 -Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0";
  2.1303 -by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
  2.1304 -by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
  2.1305 -              simpset() addsimps [power_abs]));
  2.1306 -qed "LIMSEQ_rabs_realpow_zero2";
  2.1307 -
  2.1308 -Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0";
  2.1309 -by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2,
  2.1310 -    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
  2.1311 -qed "NSLIMSEQ_rabs_realpow_zero2";
  2.1312 -
  2.1313 -(***---------------------------------------------------------------
  2.1314 -                 Hyperreals and Sequences
  2.1315 - ---------------------------------------------------------------***)
  2.1316 -(*** A bounded sequence is a finite hyperreal ***)
  2.1317 -Goal "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite";
  2.1318 -by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
  2.1319 -       [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
  2.1320 -       simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
  2.1321 -        Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
  2.1322 -qed "NSBseq_HFinite_hypreal";
  2.1323 -
  2.1324 -(*** A sequence converging to zero defines an infinitesimal ***)
  2.1325 -Goalw [NSLIMSEQ_def] 
  2.1326 -      "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal";
  2.1327 -by (dres_inst_tac [("x","whn")] bspec 1);
  2.1328 -by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
  2.1329 -by (auto_tac (claset(),
  2.1330 -              simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
  2.1331 -                                  starfunNat]));
  2.1332 -qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
  2.1333 -
  2.1334 -(***---------------------------------------------------------------
  2.1335 -    Theorems proved by Harrison in HOL that we do not need 
  2.1336 -    in order to prove equivalence between Cauchy criterion 
  2.1337 -    and convergence:
  2.1338 - -- Show that every sequence contains a monotonic subsequence   
  2.1339 -Goal "EX f. subseq f & monoseq (%n. s (f n))";
  2.1340 - -- Show that a subsequence of a bounded sequence is bounded
  2.1341 -Goal "Bseq X ==> Bseq (%n. X (f n))";
  2.1342 - -- Show we can take subsequential terms arbitrarily far 
  2.1343 -    up a sequence       
  2.1344 -Goal "subseq f ==> n <= f(n)";
  2.1345 -Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
  2.1346 - ---------------------------------------------------------------***)
  2.1347 -
  2.1348 -
     3.1 --- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 28 16:25:40 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 28 16:26:27 2004 +0200
     3.3 @@ -2,62 +2,1226 @@
     3.4      Author      : Jacques D. Fleuriot
     3.5      Copyright   : 1998  University of Cambridge
     3.6      Description : Convergence of sequences and series
     3.7 -*) 
     3.8 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     3.9 +*)
    3.10  
    3.11 -SEQ = NatStar + HyperPow + 
    3.12 +theory SEQ = NatStar + HyperPow:
    3.13  
    3.14  constdefs
    3.15  
    3.16 -  (* Standard definition of convergence of sequence *)           
    3.17 -  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" [60, 60] 60)
    3.18 -  "X ----> L == (ALL r. 0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
    3.19 -  
    3.20 -  (* Nonstandard definition of convergence of sequence *)
    3.21 -  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
    3.22 -  "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"
    3.23 +  LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
    3.24 +    --{*Standard definition of convergence of sequence*}
    3.25 +  "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
    3.26  
    3.27 -  (* define value of limit using choice operator*)
    3.28 -  lim :: (nat => real) => real
    3.29 +  NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
    3.30 +    --{*Nonstandard definition of convergence of sequence*}
    3.31 +  "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
    3.32 +
    3.33 +  lim :: "(nat => real) => real"
    3.34 +    --{*Standard definition of limit using choice operator*}
    3.35    "lim X == (@L. (X ----> L))"
    3.36  
    3.37 -  nslim :: (nat => real) => real
    3.38 +  nslim :: "(nat => real) => real"
    3.39 +    --{*Nonstandard definition of limit using choice operator*}
    3.40    "nslim X == (@L. (X ----NS> L))"
    3.41  
    3.42 -  (* Standard definition of convergence *)
    3.43 -  convergent :: (nat => real) => bool
    3.44 -  "convergent X == (EX L. (X ----> L))"
    3.45 -
    3.46 -  (* Nonstandard definition of convergence *)
    3.47 -  NSconvergent :: (nat => real) => bool
    3.48 -  "NSconvergent X == (EX L. (X ----NS> L))"
    3.49 +  convergent :: "(nat => real) => bool"
    3.50 +    --{*Standard definition of convergence*}
    3.51 +  "convergent X == (\<exists>L. (X ----> L))"
    3.52  
    3.53 -  (* Standard definition for bounded sequence *)
    3.54 -  Bseq :: (nat => real) => bool
    3.55 -  "Bseq X == (EX K. (0 < K & (ALL n. abs(X n) <= K)))"
    3.56 - 
    3.57 -  (* Nonstandard definition for bounded sequence *)
    3.58 -  NSBseq :: (nat=>real) => bool
    3.59 -  "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" 
    3.60 +  NSconvergent :: "(nat => real) => bool"
    3.61 +    --{*Nonstandard definition of convergence*}
    3.62 +  "NSconvergent X == (\<exists>L. (X ----NS> L))"
    3.63 +
    3.64 +  Bseq :: "(nat => real) => bool"
    3.65 +    --{*Standard definition for bounded sequence*}
    3.66 +  "Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))"
    3.67  
    3.68 -  (* Definition for monotonicity *)
    3.69 -  monoseq :: (nat=>real)=>bool
    3.70 -  "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) |
    3.71 -                 (ALL m n. m <= n --> X n <= X m))"   
    3.72 +  NSBseq :: "(nat=>real) => bool"
    3.73 +    --{*Nonstandard definition for bounded sequence*}
    3.74 +  "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite)"
    3.75 +
    3.76 +  monoseq :: "(nat=>real)=>bool"
    3.77 +    --{*Definition for monotonicity*}
    3.78 +  "monoseq X == ((\<forall>(m::nat) n. m \<le> n --> X m \<le> X n) |
    3.79 +                 (\<forall>m n. m \<le> n --> X n \<le> X m))"
    3.80  
    3.81 -  (* Definition of subsequence *)
    3.82 -  subseq :: (nat => nat) => bool
    3.83 -  "subseq f == (ALL m n. m < n --> (f m) < (f n))"
    3.84 +  subseq :: "(nat => nat) => bool"
    3.85 +    --{*Definition of subsequence*}
    3.86 +  "subseq f == (\<forall>m n. m < n --> (f m) < (f n))"
    3.87  
    3.88 -  (** Cauchy condition **)
    3.89 -
    3.90 -  (* Standard definition *)
    3.91 -  Cauchy :: (nat => real) => bool
    3.92 -  "Cauchy X == (ALL e. (0 < e -->
    3.93 -                       (EX M. (ALL m n. M <= m & M <= n 
    3.94 +  Cauchy :: "(nat => real) => bool"
    3.95 +    --{*Standard definition of the Cauchy condition*}
    3.96 +  "Cauchy X == (\<forall>e. (0 < e -->
    3.97 +                       (\<exists>M. (\<forall>m n. M \<le> m & M \<le> n
    3.98                               --> abs((X m) + -(X n)) < e))))"
    3.99  
   3.100 -  NSCauchy :: (nat => real) => bool
   3.101 -  "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
   3.102 -                      ( *fNat* X) M @= ( *fNat* X) N)"
   3.103 +  NSCauchy :: "(nat => real) => bool"
   3.104 +    --{*Nonstandard definition*}
   3.105 +  "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
   3.106 +                      ( *fNat* X) M \<approx> ( *fNat* X) N)"
   3.107 +
   3.108 +
   3.109 +
   3.110 +text{* Example of an hypersequence (i.e. an extended standard sequence)
   3.111 +   whose term with an hypernatural suffix is an infinitesimal i.e.
   3.112 +   the whn'nth term of the hypersequence is a member of Infinitesimal*}
   3.113 +
   3.114 +lemma SEQ_Infinitesimal:
   3.115 +      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
   3.116 +apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
   3.117 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
   3.118 +apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat)
   3.119 +done
   3.120 +
   3.121 +
   3.122 +subsection{*LIMSEQ and NSLIMSEQ*}
   3.123 +
   3.124 +lemma LIMSEQ_iff:
   3.125 +      "(X ----> L) =
   3.126 +       (\<forall>r. 0 <r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
   3.127 +by (simp add: LIMSEQ_def)
   3.128 +
   3.129 +lemma NSLIMSEQ_iff:
   3.130 +    "(X ----NS> L) = (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)"
   3.131 +by (simp add: NSLIMSEQ_def)
   3.132 +
   3.133 +
   3.134 +text{*LIMSEQ ==> NSLIMSEQ*}
   3.135 +
   3.136 +lemma LIMSEQ_NSLIMSEQ:
   3.137 +      "X ----> L ==> X ----NS> L"
   3.138 +apply (simp add: LIMSEQ_def NSLIMSEQ_def)
   3.139 +apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   3.140 +apply (rule_tac z = N in eq_Abs_hypnat)
   3.141 +apply (rule approx_minus_iff [THEN iffD2])
   3.142 +apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
   3.143 +              hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   3.144 +apply (rule bexI [OF _ lemma_hyprel_refl], safe)
   3.145 +apply (drule_tac x = u in spec, safe)
   3.146 +apply (drule_tac x = no in spec, fuf)
   3.147 +apply (blast dest: less_imp_le)
   3.148 +done
   3.149 +
   3.150 +
   3.151 +text{*NSLIMSEQ ==> LIMSEQ*}
   3.152 +
   3.153 +lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n
   3.154 +           ==> {n. f n = 0} = {0} | {n. f n = 0} = {}"
   3.155 +apply auto
   3.156 +apply (drule_tac x = xa in spec)
   3.157 +apply (drule_tac [2] x = x in spec, auto)
   3.158 +done
   3.159 +
   3.160 +lemma lemma_NSLIMSEQ2: "{n. f n \<le> Suc u} = {n. f n \<le> u} Un {n. f n = Suc u}"
   3.161 +by (auto simp add: le_Suc_eq)
   3.162 +
   3.163 +lemma lemma_NSLIMSEQ3:
   3.164 +     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. f n = Suc u} \<le> {n. n \<le> Suc u}"
   3.165 +apply auto
   3.166 +apply (drule_tac x = x in spec, auto)
   3.167 +done
   3.168 +
   3.169 +text{* the following sequence @{term "f(n)"} defines a hypernatural *}
   3.170 +lemma NSLIMSEQ_finite_set:
   3.171 +     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
   3.172 +apply (induct u)
   3.173 +apply (auto simp add: lemma_NSLIMSEQ2)
   3.174 +apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def])
   3.175 +apply (drule lemma_NSLIMSEQ1, safe)
   3.176 +apply (simp_all (no_asm_simp)) 
   3.177 +done
   3.178 +
   3.179 +lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n \<le> u}"
   3.180 +by (auto dest: less_le_trans simp add: le_def)
   3.181 +
   3.182 +text{* the index set is in the free ultrafilter *}
   3.183 +lemma FreeUltrafilterNat_NSLIMSEQ:
   3.184 +     "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. u < f n} : FreeUltrafilterNat"
   3.185 +apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2])
   3.186 +apply (rule FreeUltrafilterNat_finite)
   3.187 +apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set)
   3.188 +done
   3.189 +
   3.190 +text{* thus, the sequence defines an infinite hypernatural! *}
   3.191 +lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
   3.192 +          ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite"
   3.193 +apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   3.194 +apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
   3.195 +apply (erule FreeUltrafilterNat_NSLIMSEQ)
   3.196 +done
   3.197 +
   3.198 +lemma lemmaLIM:
   3.199 +     "{n. X (f n) + - L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le>
   3.200 +      {n. \<bar>X (f n) + - L\<bar> < r}"
   3.201 +by auto
   3.202 +
   3.203 +lemma lemmaLIM2:
   3.204 +  "{n. \<bar>X (f n) + - L\<bar> < r} Int {n. r \<le> abs (X (f n) + - (L::real))} = {}"
   3.205 +by auto
   3.206 +
   3.207 +lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
   3.208 +           ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
   3.209 +           - hypreal_of_real  L \<approx> 0 |] ==> False"
   3.210 +apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   3.211 +apply (rename_tac "Y")
   3.212 +apply (drule_tac x = r in spec, safe)
   3.213 +apply (drule FreeUltrafilterNat_Int, assumption)
   3.214 +apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
   3.215 +apply (drule FreeUltrafilterNat_all)
   3.216 +apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
   3.217 +apply (drule FreeUltrafilterNat_Int, assumption)
   3.218 +apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty)
   3.219 +done
   3.220 +
   3.221 +lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
   3.222 +apply (simp add: LIMSEQ_def NSLIMSEQ_def)
   3.223 +apply (rule ccontr, simp, safe)
   3.224 +txt{* skolemization step *}
   3.225 +apply (drule choice, safe)
   3.226 +apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec)
   3.227 +apply (drule_tac [2] approx_minus_iff [THEN iffD1])
   3.228 +apply (simp_all add: linorder_not_less)
   3.229 +apply (blast intro: HNatInfinite_NSLIMSEQ)
   3.230 +apply (blast intro: lemmaLIM3)
   3.231 +done
   3.232 +
   3.233 +text{* Now, the all-important result is trivially proved! *}
   3.234 +theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
   3.235 +by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   3.236 +
   3.237 +
   3.238 +subsection{*Theorems About Sequences*}
   3.239 +
   3.240 +lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
   3.241 +by (simp add: NSLIMSEQ_def)
   3.242 +
   3.243 +lemma LIMSEQ_const: "(%n. k) ----> k"
   3.244 +by (simp add: LIMSEQ_def)
   3.245 +
   3.246 +lemma NSLIMSEQ_add:
   3.247 +      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
   3.248 +by (auto intro: approx_add simp add: NSLIMSEQ_def starfunNat_add [symmetric])
   3.249 +
   3.250 +lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
   3.251 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)
   3.252 +
   3.253 +lemma NSLIMSEQ_mult:
   3.254 +      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
   3.255 +by (auto intro!: approx_mult_HFinite 
   3.256 +        simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric])
   3.257 +
   3.258 +lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
   3.259 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
   3.260 +
   3.261 +lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
   3.262 +by (auto simp add: NSLIMSEQ_def starfunNat_minus [symmetric])
   3.263 +
   3.264 +lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
   3.265 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)
   3.266 +
   3.267 +lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
   3.268 +by (drule LIMSEQ_minus, simp)
   3.269 +
   3.270 +lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
   3.271 +by (drule NSLIMSEQ_minus, simp)
   3.272 +
   3.273 +lemma NSLIMSEQ_add_minus:
   3.274 +     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
   3.275 +by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y])
   3.276 +
   3.277 +lemma LIMSEQ_add_minus:
   3.278 +     "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
   3.279 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)
   3.280 +
   3.281 +lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
   3.282 +apply (simp add: diff_minus)
   3.283 +apply (blast intro: LIMSEQ_add_minus)
   3.284 +done
   3.285 +
   3.286 +lemma NSLIMSEQ_diff:
   3.287 +     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
   3.288 +apply (simp add: diff_minus)
   3.289 +apply (blast intro: NSLIMSEQ_add_minus)
   3.290 +done
   3.291 +
   3.292 +text{*Proof is like that of @{text NSLIM_inverse}.*}
   3.293 +lemma NSLIMSEQ_inverse:
   3.294 +     "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
   3.295 +by (simp add: NSLIMSEQ_def starfunNat_inverse [symmetric] 
   3.296 +              hypreal_of_real_approx_inverse)
   3.297 +
   3.298 +
   3.299 +text{*Standard version of theorem*}
   3.300 +lemma LIMSEQ_inverse:
   3.301 +     "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
   3.302 +by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)
   3.303 +
   3.304 +lemma NSLIMSEQ_mult_inverse:
   3.305 +     "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
   3.306 +by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)
   3.307 +
   3.308 +lemma LIMSEQ_divide:
   3.309 +     "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
   3.310 +by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
   3.311 +
   3.312 +text{*Uniqueness of limit*}
   3.313 +lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
   3.314 +apply (simp add: NSLIMSEQ_def)
   3.315 +apply (drule HNatInfinite_whn [THEN [2] bspec])+
   3.316 +apply (auto dest: approx_trans3)
   3.317 +done
   3.318 +
   3.319 +lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
   3.320 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)
   3.321 +
   3.322 +
   3.323 +subsection{*Nslim and Lim*}
   3.324 +
   3.325 +lemma limI: "X ----> L ==> lim X = L"
   3.326 +apply (simp add: lim_def)
   3.327 +apply (blast intro: LIMSEQ_unique)
   3.328 +done
   3.329 +
   3.330 +lemma nslimI: "X ----NS> L ==> nslim X = L"
   3.331 +apply (simp add: nslim_def)
   3.332 +apply (blast intro: NSLIMSEQ_unique)
   3.333 +done
   3.334 +
   3.335 +lemma lim_nslim_iff: "lim X = nslim X"
   3.336 +by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)
   3.337 +
   3.338 +
   3.339 +subsection{*Convergence*}
   3.340 +
   3.341 +lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
   3.342 +by (simp add: convergent_def)
   3.343 +
   3.344 +lemma convergentI: "(X ----> L) ==> convergent X"
   3.345 +by (auto simp add: convergent_def)
   3.346 +
   3.347 +lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X ----NS> L)"
   3.348 +by (simp add: NSconvergent_def)
   3.349 +
   3.350 +lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
   3.351 +by (auto simp add: NSconvergent_def)
   3.352 +
   3.353 +lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
   3.354 +by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)
   3.355 +
   3.356 +lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
   3.357 +by (auto intro: someI simp add: NSconvergent_def nslim_def)
   3.358 +
   3.359 +lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
   3.360 +by (auto intro: someI simp add: convergent_def lim_def)
   3.361 +
   3.362 +text{*Subsequence (alternative definition, (e.g. Hoskins)*}
   3.363 +
   3.364 +lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
   3.365 +apply (simp add: subseq_def)
   3.366 +apply (auto dest!: less_imp_Suc_add)
   3.367 +apply (induct_tac k)
   3.368 +apply (auto intro: less_trans)
   3.369 +done
   3.370 +
   3.371 +
   3.372 +subsection{*Monotonicity*}
   3.373 +
   3.374 +lemma monoseq_Suc:
   3.375 +   "monoseq X = ((\<forall>n. X n \<le> X (Suc n))
   3.376 +                 | (\<forall>n. X (Suc n) \<le> X n))"
   3.377 +apply (simp add: monoseq_def)
   3.378 +apply (auto dest!: le_imp_less_or_eq)
   3.379 +apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
   3.380 +apply (induct_tac "ka")
   3.381 +apply (auto intro: order_trans)
   3.382 +apply (erule swap) 
   3.383 +apply (induct_tac "k")
   3.384 +apply (auto intro: order_trans)
   3.385 +done
   3.386 +
   3.387 +lemma monoI1: "\<forall>m n. m \<le> n --> X m \<le> X n ==> monoseq X"
   3.388 +by (simp add: monoseq_def)
   3.389 +
   3.390 +lemma monoI2: "\<forall>m n. m \<le> n --> X n \<le> X m ==> monoseq X"
   3.391 +by (simp add: monoseq_def)
   3.392 +
   3.393 +lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
   3.394 +by (simp add: monoseq_Suc)
   3.395 +
   3.396 +lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
   3.397 +by (simp add: monoseq_Suc)
   3.398 +
   3.399 +
   3.400 +subsection{*Bounded Sequence*}
   3.401 +
   3.402 +lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)"
   3.403 +by (simp add: Bseq_def)
   3.404 +
   3.405 +lemma BseqI: "[| 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K |] ==> Bseq X"
   3.406 +by (auto simp add: Bseq_def)
   3.407 +
   3.408 +lemma lemma_NBseq_def:
   3.409 +     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
   3.410 +      (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
   3.411 +apply auto
   3.412 + prefer 2 apply force
   3.413 +apply (cut_tac x = K in reals_Archimedean2, clarify)
   3.414 +apply (rule_tac x = n in exI, clarify)
   3.415 +apply (drule_tac x = na in spec)
   3.416 +apply (auto simp add: real_of_nat_Suc)
   3.417 +done
   3.418 +
   3.419 +text{* alternative definition for Bseq *}
   3.420 +lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))"
   3.421 +apply (simp add: Bseq_def)
   3.422 +apply (simp (no_asm) add: lemma_NBseq_def)
   3.423 +done
   3.424 +
   3.425 +lemma lemma_NBseq_def2:
   3.426 +     "(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) =
   3.427 +      (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
   3.428 +apply (subst lemma_NBseq_def, auto)
   3.429 +apply (rule_tac x = "Suc N" in exI)
   3.430 +apply (rule_tac [2] x = N in exI)
   3.431 +apply (auto simp add: real_of_nat_Suc)
   3.432 + prefer 2 apply (blast intro: order_less_imp_le)
   3.433 +apply (drule_tac x = n in spec, simp)
   3.434 +done
   3.435 +
   3.436 +(* yet another definition for Bseq *)
   3.437 +lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))"
   3.438 +by (simp add: Bseq_def lemma_NBseq_def2)
   3.439 +
   3.440 +lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite"
   3.441 +by (simp add: NSBseq_def)
   3.442 +
   3.443 +lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X"
   3.444 +by (simp add: NSBseq_def)
   3.445 +
   3.446 +text{*The standard definition implies the nonstandard definition*}
   3.447 +
   3.448 +lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K"
   3.449 +by auto
   3.450 +
   3.451 +lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
   3.452 +apply (simp add: Bseq_def NSBseq_def, safe)
   3.453 +apply (rule_tac z = N in eq_Abs_hypnat)
   3.454 +apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff 
   3.455 +                      HNatInfinite_FreeUltrafilterNat_iff)
   3.456 +apply (rule bexI [OF _ lemma_hyprel_refl]) 
   3.457 +apply (drule_tac f = Xa in lemma_Bseq)
   3.458 +apply (rule_tac x = "K+1" in exI)
   3.459 +apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
   3.460 +done
   3.461 +
   3.462 +text{*The nonstandard definition implies the standard definition*}
   3.463 +
   3.464 +(* similar to NSLIM proof in REALTOPOS *)
   3.465 +
   3.466 +text{* We need to get rid of the real variable and do so by proving the
   3.467 +   following, which relies on the Archimedean property of the reals.
   3.468 +   When we skolemize we then get the required function @{term "f::nat=>nat"}.
   3.469 +   Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
   3.470 +   which woulid be useless.*}
   3.471 +
   3.472 +lemma lemmaNSBseq:
   3.473 +     "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
   3.474 +      ==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>"
   3.475 +apply safe
   3.476 +apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
   3.477 +done
   3.478 +
   3.479 +lemma lemmaNSBseq2: "\<forall>K. 0 < K --> (\<exists>n. K < \<bar>X n\<bar>)
   3.480 +                     ==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>"
   3.481 +apply (drule lemmaNSBseq)
   3.482 +apply (drule choice, blast)
   3.483 +done
   3.484 +
   3.485 +lemma real_seq_to_hypreal_HInfinite:
   3.486 +     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
   3.487 +      ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite"
   3.488 +apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
   3.489 +apply (rule bexI [OF _ lemma_hyprel_refl], clarify)  
   3.490 +apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
   3.491 +apply (drule FreeUltrafilterNat_all)
   3.492 +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
   3.493 +apply (auto simp add: real_of_nat_Suc)
   3.494 +done
   3.495 +
   3.496 +text{* Now prove that we can get out an infinite hypernatural as well
   3.497 +     defined using the skolem function  @{term "f::nat=>nat"} above*}
   3.498 +
   3.499 +lemma lemma_finite_NSBseq:
   3.500 +     "{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le>
   3.501 +      {n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un
   3.502 +      {n. real(Suc n) < \<bar>X (Suc u)\<bar>}"
   3.503 +by (auto dest!: le_imp_less_or_eq)
   3.504 +
   3.505 +lemma lemma_finite_NSBseq2:
   3.506 +     "finite {n. f n \<le> (u::nat) &  real(Suc n) < \<bar>X(f n)\<bar>}"
   3.507 +apply (induct_tac "u")
   3.508 +apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
   3.509 +apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset)
   3.510 +apply (auto intro: finite_real_of_nat_less_real 
   3.511 +            simp add: real_of_nat_Suc less_diff_eq [symmetric])
   3.512 +done
   3.513 +
   3.514 +lemma HNatInfinite_skolem_f:
   3.515 +     "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
   3.516 +      ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite"
   3.517 +apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   3.518 +apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
   3.519 +apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
   3.520 +apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
   3.521 +apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
   3.522 +                    {n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}")
   3.523 +apply (erule ssubst) 
   3.524 + apply (auto simp add: linorder_not_less Compl_def)
   3.525 +done
   3.526 +
   3.527 +lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
   3.528 +apply (simp add: Bseq_def NSBseq_def)
   3.529 +apply (rule ccontr)
   3.530 +apply (auto simp add: linorder_not_less [symmetric])
   3.531 +apply (drule lemmaNSBseq2, safe)
   3.532 +apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
   3.533 +apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
   3.534 +apply (auto simp add: starfunNat o_def HFinite_HInfinite_iff)
   3.535 +done
   3.536 +
   3.537 +text{* Equivalence of nonstandard and standard definitions
   3.538 +  for a bounded sequence*}
   3.539 +lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
   3.540 +by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
   3.541 +
   3.542 +text{*A convergent sequence is bounded: 
   3.543 + Boundedness as a necessary condition for convergence. 
   3.544 + The nonstandard version has no existential, as usual *}
   3.545 +
   3.546 +lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
   3.547 +apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
   3.548 +apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
   3.549 +done
   3.550 +
   3.551 +text{*Standard Version: easily now proved using equivalence of NS and
   3.552 + standard definitions *}
   3.553 +lemma convergent_Bseq: "convergent X ==> Bseq X"
   3.554 +by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
   3.555 +
   3.556 +
   3.557 +subsection{*Upper Bounds and Lubs of Bounded Sequences*}
   3.558 +
   3.559 +lemma Bseq_isUb:
   3.560 +  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   3.561 +by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)
   3.562 +
   3.563 +
   3.564 +text{* Use completeness of reals (supremum property)
   3.565 +   to show that any bounded sequence has a least upper bound*}
   3.566 +
   3.567 +lemma Bseq_isLub:
   3.568 +  "!!(X::nat=>real). Bseq X ==>
   3.569 +   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   3.570 +by (blast intro: reals_complete Bseq_isUb)
   3.571 +
   3.572 +lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U"
   3.573 +by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
   3.574 +
   3.575 +lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U"
   3.576 +by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
   3.577 +
   3.578 +
   3.579 +subsection{*A Bounded and Monotonic Sequence Converges*}
   3.580 +
   3.581 +lemma lemma_converg1:
   3.582 +     "!!(X::nat=>real). [| \<forall>m n. m \<le> n -->  X m \<le> X n;
   3.583 +                  isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma)
   3.584 +               |] ==> \<forall>n. ma \<le> n --> X n = X ma"
   3.585 +apply safe
   3.586 +apply (drule_tac y = "X n" in isLubD2)
   3.587 +apply (blast dest: order_antisym)+
   3.588 +done
   3.589 +
   3.590 +text{* The best of both worlds: Easier to prove this result as a standard
   3.591 +   theorem and then use equivalence to "transfer" it into the
   3.592 +   equivalent nonstandard form if needed!*}
   3.593 +
   3.594 +lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
   3.595 +apply (simp add: LIMSEQ_def)
   3.596 +apply (rule_tac x = "X m" in exI, safe)
   3.597 +apply (rule_tac x = m in exI, safe)
   3.598 +apply (drule spec, erule impE, auto)
   3.599 +done
   3.600 +
   3.601 +text{*Now, the same theorem in terms of NS limit *}
   3.602 +lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----NS> L)"
   3.603 +by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
   3.604 +
   3.605 +lemma lemma_converg2:
   3.606 +   "!!(X::nat=>real).
   3.607 +    [| \<forall>m. X m ~= U;  isLub UNIV {x. \<exists>n. X n = x} U |] ==> \<forall>m. X m < U"
   3.608 +apply safe
   3.609 +apply (drule_tac y = "X m" in isLubD2)
   3.610 +apply (auto dest!: order_le_imp_less_or_eq)
   3.611 +done
   3.612 +
   3.613 +lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U"
   3.614 +by (rule setleI [THEN isUbI], auto)
   3.615 +
   3.616 +text{* FIXME: @{term "U - T < U"} is redundant *}
   3.617 +lemma lemma_converg4: "!!(X::nat=> real).
   3.618 +               [| \<forall>m. X m ~= U;
   3.619 +                  isLub UNIV {x. \<exists>n. X n = x} U;
   3.620 +                  0 < T;
   3.621 +                  U + - T < U
   3.622 +               |] ==> \<exists>m. U + -T < X m & X m < U"
   3.623 +apply (drule lemma_converg2, assumption)
   3.624 +apply (rule ccontr, simp)
   3.625 +apply (simp add: linorder_not_less)
   3.626 +apply (drule lemma_converg3)
   3.627 +apply (drule isLub_le_isUb, assumption)
   3.628 +apply (auto dest: order_less_le_trans)
   3.629 +done
   3.630 +
   3.631 +text{*A standard proof of the theorem for monotone increasing sequence*}
   3.632 +
   3.633 +lemma Bseq_mono_convergent:
   3.634 +     "[| Bseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> convergent X"
   3.635 +apply (simp add: convergent_def)
   3.636 +apply (frule Bseq_isLub, safe)
   3.637 +apply (case_tac "\<exists>m. X m = U", auto)
   3.638 +apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
   3.639 +(* second case *)
   3.640 +apply (rule_tac x = U in exI)
   3.641 +apply (subst LIMSEQ_iff, safe)
   3.642 +apply (frule lemma_converg2, assumption)
   3.643 +apply (drule lemma_converg4, auto)
   3.644 +apply (rule_tac x = m in exI, safe)
   3.645 +apply (subgoal_tac "X m \<le> X n")
   3.646 + prefer 2 apply blast
   3.647 +apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
   3.648 +done
   3.649 +
   3.650 +text{*Nonstandard version of the theorem*}
   3.651 +
   3.652 +lemma NSBseq_mono_NSconvergent:
   3.653 +     "[| NSBseq X; \<forall>m n. m \<le> n --> X m \<le> X n |] ==> NSconvergent X"
   3.654 +by (auto intro: Bseq_mono_convergent 
   3.655 +         simp add: convergent_NSconvergent_iff [symmetric] 
   3.656 +                   Bseq_NSBseq_iff [symmetric])
   3.657 +
   3.658 +lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
   3.659 +apply (simp add: convergent_def)
   3.660 +apply (auto dest: LIMSEQ_minus)
   3.661 +apply (drule LIMSEQ_minus, auto)
   3.662 +done
   3.663 +
   3.664 +lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
   3.665 +by (simp add: Bseq_def)
   3.666 +
   3.667 +text{*Main monotonicity theorem*}
   3.668 +lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
   3.669 +apply (simp add: monoseq_def, safe)
   3.670 +apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
   3.671 +apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
   3.672 +apply (auto intro!: Bseq_mono_convergent)
   3.673 +done
   3.674 +
   3.675 +
   3.676 +subsection{*A Few More Equivalence Theorems for Boundedness*}
   3.677 +
   3.678 +text{*alternative formulation for boundedness*}
   3.679 +lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + -x\<bar> \<le> k))"
   3.680 +apply (unfold Bseq_def, safe)
   3.681 +apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI)
   3.682 +apply (rule_tac x = K in exI)
   3.683 +apply (rule_tac x = 0 in exI, auto)
   3.684 +apply (drule_tac [!] x=n in spec, arith+)
   3.685 +done
   3.686 +
   3.687 +text{*alternative formulation for boundedness*}
   3.688 +lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + -X(N)) \<le> k))"
   3.689 +apply safe
   3.690 +apply (simp add: Bseq_def, safe)
   3.691 +apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
   3.692 +apply auto
   3.693 +apply arith
   3.694 +apply (rule_tac x = N in exI, safe)
   3.695 +apply (drule_tac x = n in spec, arith)
   3.696 +apply (auto simp add: Bseq_iff2)
   3.697 +done
   3.698 +
   3.699 +lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
   3.700 +apply (simp add: Bseq_def)
   3.701 +apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI)
   3.702 +apply auto
   3.703 +apply (drule_tac [2] x = n in spec, arith+)
   3.704 +done
   3.705 +
   3.706 +
   3.707 +subsection{*Equivalence Between NS and Standard Cauchy Sequences*}
   3.708 +
   3.709 +subsubsection{*Standard Implies Nonstandard*}
   3.710 +
   3.711 +lemma lemmaCauchy1:
   3.712 +     "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
   3.713 +      ==> {n. M \<le> x n} : FreeUltrafilterNat"
   3.714 +apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
   3.715 +apply (drule_tac x = M in spec, ultra)
   3.716 +done
   3.717 +
   3.718 +lemma lemmaCauchy2:
   3.719 +     "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> \<bar>X m + - X n\<bar> < u} Int
   3.720 +      {n. M \<le> xa n} Int {n. M \<le> x n} \<le>
   3.721 +      {n. abs (X (xa n) + - X (x n)) < u}"
   3.722 +by blast
   3.723 +
   3.724 +lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
   3.725 +apply (simp add: Cauchy_def NSCauchy_def, safe)
   3.726 +apply (rule_tac z = M in eq_Abs_hypnat)
   3.727 +apply (rule_tac z = N in eq_Abs_hypnat)
   3.728 +apply (rule approx_minus_iff [THEN iffD2])
   3.729 +apply (rule mem_infmal_iff [THEN iffD1])
   3.730 +apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   3.731 +apply (rule bexI, auto)
   3.732 +apply (drule spec, auto)
   3.733 +apply (drule_tac M = M in lemmaCauchy1)
   3.734 +apply (drule_tac M = M in lemmaCauchy1)
   3.735 +apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
   3.736 +apply (rule FreeUltrafilterNat_Int)
   3.737 +apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
   3.738 +done
   3.739 +
   3.740 +subsubsection{*Nonstandard Implies Standard*}
   3.741 +
   3.742 +lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
   3.743 +apply (auto simp add: Cauchy_def NSCauchy_def)
   3.744 +apply (rule ccontr, simp)
   3.745 +apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
   3.746 +apply (drule bspec, assumption)
   3.747 +apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); 
   3.748 +apply (auto simp add: starfunNat)
   3.749 +apply (drule approx_minus_iff [THEN iffD1])
   3.750 +apply (drule mem_infmal_iff [THEN iffD2])
   3.751 +apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
   3.752 +apply (rename_tac "Y")
   3.753 +apply (drule_tac x = e in spec, auto)
   3.754 +apply (drule FreeUltrafilterNat_Int, assumption)
   3.755 +apply (subgoal_tac "{n. \<bar>X (f n) + - X (fa n)\<bar> < e} \<in> \<U>") 
   3.756 + prefer 2 apply (erule FreeUltrafilterNat_subset, force) 
   3.757 +apply (rule FreeUltrafilterNat_empty [THEN notE]) 
   3.758 +apply (subgoal_tac
   3.759 +         "{n. abs (X (f n) + - X (fa n)) < e} Int 
   3.760 +          {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
   3.761 +apply auto  
   3.762 +done
   3.763 +
   3.764 +
   3.765 +theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
   3.766 +by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
   3.767 +
   3.768 +text{*A Cauchy sequence is bounded -- this is the standard
   3.769 +  proof mechanization rather than the nonstandard proof*}
   3.770 +
   3.771 +lemma lemmaCauchy: "\<forall>n. M \<le> n --> \<bar>X M + - X n\<bar> < (1::real)
   3.772 +          ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
   3.773 +apply safe
   3.774 +apply (drule spec, auto, arith)
   3.775 +done
   3.776 +
   3.777 +lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
   3.778 +by auto
   3.779 +
   3.780 +text{* FIXME: Long. Maximal element in subsequence *}
   3.781 +lemma SUP_rabs_subseq:
   3.782 +     "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
   3.783 +apply (induct M)
   3.784 +apply (rule_tac x = 0 in exI, simp, safe)
   3.785 +apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
   3.786 +apply safe
   3.787 +apply (rule_tac x = m in exI)
   3.788 +apply (rule_tac [2] x = m in exI)
   3.789 +apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
   3.790 +apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) 
   3.791 +apply (simp_all add: less_Suc_cancel_iff)
   3.792 +apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
   3.793 +done
   3.794 +
   3.795 +lemma lemma_Nat_covered:
   3.796 +     "[| \<forall>m::nat. m \<le> M --> P M m;
   3.797 +         \<forall>m. M \<le> m --> P M m |]
   3.798 +      ==> \<forall>m. P M m"
   3.799 +by (auto elim: less_asym simp add: le_def)
   3.800 +
   3.801 +
   3.802 +lemma lemma_trans1:
   3.803 +     "[| \<forall>n. n \<le> M --> \<bar>(X::nat=>real) n\<bar> \<le> a;  a < b |]
   3.804 +      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
   3.805 +by (blast intro: order_le_less_trans [THEN order_less_imp_le])
   3.806 +
   3.807 +lemma lemma_trans2:
   3.808 +     "[| \<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a; a < b |]
   3.809 +      ==> \<forall>n. M \<le> n --> \<bar>X n\<bar>\<le> b"
   3.810 +by (blast intro: order_less_trans [THEN order_less_imp_le])
   3.811 +
   3.812 +lemma lemma_trans3:
   3.813 +     "[| \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> a; a = b |]
   3.814 +      ==> \<forall>n. n \<le> M --> \<bar>X n\<bar> \<le> b"
   3.815 +by auto
   3.816 +
   3.817 +lemma lemma_trans4: "\<forall>n. M \<le> n --> \<bar>(X::nat=>real) n\<bar> < a
   3.818 +              ==>  \<forall>n. M \<le> n --> \<bar>X n\<bar> \<le> a"
   3.819 +by (blast intro: order_less_imp_le)
   3.820 +
   3.821 +
   3.822 +text{*Proof is more involved than outlines sketched by various authors
   3.823 + would suggest*}
   3.824 +
   3.825 +lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
   3.826 +apply (simp add: Cauchy_def Bseq_def)
   3.827 +apply (drule_tac x = 1 in spec)
   3.828 +apply (erule zero_less_one [THEN [2] impE], safe)
   3.829 +apply (drule_tac x = M in spec, simp)
   3.830 +apply (drule lemmaCauchy)
   3.831 +apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
   3.832 +apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear)
   3.833 +apply safe
   3.834 +apply (drule lemma_trans1, assumption)
   3.835 +apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
   3.836 +apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
   3.837 +apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
   3.838 +apply (drule lemma_trans4)
   3.839 +apply (drule_tac [2] lemma_trans4)
   3.840 +apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI)
   3.841 +apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI)
   3.842 +apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI)
   3.843 +apply (auto elim!: lemma_Nat_covered, arith+)
   3.844 +done
   3.845 +
   3.846 +text{*A Cauchy sequence is bounded -- nonstandard version*}
   3.847 +
   3.848 +lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
   3.849 +by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
   3.850 +
   3.851 +
   3.852 +text{*Equivalence of Cauchy criterion and convergence:
   3.853 +  We will prove this using our NS formulation which provides a
   3.854 +  much easier proof than using the standard definition. We do not
   3.855 +  need to use properties of subsequences such as boundedness,
   3.856 +  monotonicity etc... Compare with Harrison's corresponding proof
   3.857 +  in HOL which is much longer and more complicated. Of course, we do
   3.858 +  not have problems which he encountered with guessing the right
   3.859 +  instantiations for his 'espsilon-delta' proof(s) in this case
   3.860 +  since the NS formulations do not involve existential quantifiers.*}
   3.861 +
   3.862 +lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
   3.863 +apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
   3.864 +apply (frule NSCauchy_NSBseq)
   3.865 +apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
   3.866 +apply (drule HNatInfinite_whn [THEN [2] bspec])
   3.867 +apply (drule HNatInfinite_whn [THEN [2] bspec])
   3.868 +apply (auto dest!: st_part_Ex simp add: SReal_iff)
   3.869 +apply (blast intro: approx_trans3)
   3.870 +done
   3.871 +
   3.872 +text{*Standard proof for free*}
   3.873 +lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
   3.874 +by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)
   3.875 +
   3.876 +
   3.877 +text{*We can now try and derive a few properties of sequences,
   3.878 +     starting with the limit comparison property for sequences.*}
   3.879 +
   3.880 +lemma NSLIMSEQ_le:
   3.881 +       "[| f ----NS> l; g ----NS> m;
   3.882 +           \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n)
   3.883 +                |] ==> l \<le> m"
   3.884 +apply (simp add: NSLIMSEQ_def, safe)
   3.885 +apply (drule starfun_le_mono)
   3.886 +apply (drule HNatInfinite_whn [THEN [2] bspec])+
   3.887 +apply (drule_tac x = whn in spec)
   3.888 +apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
   3.889 +apply clarify
   3.890 +apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
   3.891 +done
   3.892 +
   3.893 +(* standard version *)
   3.894 +lemma LIMSEQ_le:
   3.895 +     "[| f ----> l; g ----> m; \<exists>N. \<forall>n. N \<le> n --> f(n) \<le> g(n) |]
   3.896 +      ==> l \<le> m"
   3.897 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
   3.898 +
   3.899 +lemma LIMSEQ_le_const: "[| X ----> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   3.900 +apply (rule LIMSEQ_le)
   3.901 +apply (rule LIMSEQ_const, auto)
   3.902 +done
   3.903 +
   3.904 +lemma NSLIMSEQ_le_const: "[| X ----NS> r; \<forall>n. a \<le> X n |] ==> a \<le> r"
   3.905 +by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)
   3.906 +
   3.907 +lemma LIMSEQ_le_const2: "[| X ----> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   3.908 +apply (rule LIMSEQ_le)
   3.909 +apply (rule_tac [2] LIMSEQ_const, auto)
   3.910 +done
   3.911 +
   3.912 +lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \<forall>n. X n \<le> a |] ==> r \<le> a"
   3.913 +by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)
   3.914 +
   3.915 +text{*Shift a convergent series by 1:
   3.916 +  By the equivalence between Cauchiness and convergence and because
   3.917 +  the successor of an infinite hypernatural is also infinite.*}
   3.918 +
   3.919 +lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
   3.920 +apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   3.921 +apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
   3.922 +apply (drule bspec, assumption)
   3.923 +apply (drule bspec, assumption)
   3.924 +apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
   3.925 +apply (blast intro: approx_trans3)
   3.926 +done
   3.927 +
   3.928 +text{* standard version *}
   3.929 +lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
   3.930 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
   3.931 +
   3.932 +lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
   3.933 +apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
   3.934 +apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one)
   3.935 +apply (drule bspec, assumption)
   3.936 +apply (drule bspec, assumption)
   3.937 +apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
   3.938 +apply (drule_tac x="N - 1" in bspec) 
   3.939 +apply (auto intro: approx_trans3)
   3.940 +done
   3.941 +
   3.942 +lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
   3.943 +apply (simp add: LIMSEQ_NSLIMSEQ_iff)
   3.944 +apply (erule NSLIMSEQ_imp_Suc)
   3.945 +done
   3.946 +
   3.947 +lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
   3.948 +by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
   3.949 +
   3.950 +lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
   3.951 +by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   3.952 +
   3.953 +text{*A sequence tends to zero iff its abs does*}
   3.954 +lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----> 0) = (f ----> 0)"
   3.955 +by (simp add: LIMSEQ_def)
   3.956 +
   3.957 +text{*We prove the NS version from the standard one, since the NS proof
   3.958 +   seems more complicated than the standard one above!*}
   3.959 +lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) ----NS> 0) = (f ----NS> 0)"
   3.960 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)
   3.961 +
   3.962 +text{*Generalization to other limits*}
   3.963 +lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
   3.964 +apply (simp add: NSLIMSEQ_def)
   3.965 +apply (auto intro: approx_hrabs 
   3.966 +            simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric])
   3.967 +done
   3.968 +
   3.969 +text{* standard version *}
   3.970 +lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \<bar>f n\<bar>) ----> \<bar>l\<bar>"
   3.971 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)
   3.972 +
   3.973 +text{*An unbounded sequence's inverse tends to 0*}
   3.974 +
   3.975 +text{* standard proof seems easier *}
   3.976 +lemma LIMSEQ_inverse_zero:
   3.977 +      "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n) ==> (%n. inverse(f n)) ----> 0"
   3.978 +apply (simp add: LIMSEQ_def, safe)
   3.979 +apply (drule_tac x = "inverse r" in spec, safe)
   3.980 +apply (rule_tac x = N in exI, safe)
   3.981 +apply (drule spec, auto)
   3.982 +apply (frule positive_imp_inverse_positive)
   3.983 +apply (frule order_less_trans, assumption)
   3.984 +apply (frule_tac a = "f n" in positive_imp_inverse_positive)
   3.985 +apply (simp add: abs_if) 
   3.986 +apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
   3.987 +apply (auto intro: inverse_less_iff_less [THEN iffD2]
   3.988 +            simp del: inverse_inverse_eq)
   3.989 +done
   3.990 +
   3.991 +lemma NSLIMSEQ_inverse_zero:
   3.992 +     "\<forall>y. \<exists>N. \<forall>n. N \<le> n --> y < f(n)
   3.993 +      ==> (%n. inverse(f n)) ----NS> 0"
   3.994 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
   3.995 +
   3.996 +text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
   3.997 +
   3.998 +lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
   3.999 +apply (rule LIMSEQ_inverse_zero, safe)
  3.1000 +apply (cut_tac x = y in reals_Archimedean2)
  3.1001 +apply (safe, rule_tac x = n in exI)
  3.1002 +apply (auto simp add: real_of_nat_Suc)
  3.1003 +done
  3.1004 +
  3.1005 +lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
  3.1006 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
  3.1007 +
  3.1008 +text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
  3.1009 +infinity is now easily proved*}
  3.1010 +
  3.1011 +lemma LIMSEQ_inverse_real_of_nat_add:
  3.1012 +     "(%n. r + inverse(real(Suc n))) ----> r"
  3.1013 +by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
  3.1014 +
  3.1015 +lemma NSLIMSEQ_inverse_real_of_nat_add:
  3.1016 +     "(%n. r + inverse(real(Suc n))) ----NS> r"
  3.1017 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
  3.1018 +
  3.1019 +lemma LIMSEQ_inverse_real_of_nat_add_minus:
  3.1020 +     "(%n. r + -inverse(real(Suc n))) ----> r"
  3.1021 +by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)
  3.1022 +
  3.1023 +lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
  3.1024 +     "(%n. r + -inverse(real(Suc n))) ----NS> r"
  3.1025 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)
  3.1026 +
  3.1027 +lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
  3.1028 +     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
  3.1029 +by (cut_tac b=1 in
  3.1030 +        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
  3.1031 +
  3.1032 +lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
  3.1033 +     "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
  3.1034 +by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)
  3.1035 +
  3.1036 +
  3.1037 +text{* Real Powers*}
  3.1038 +
  3.1039 +lemma NSLIMSEQ_pow [rule_format]:
  3.1040 +     "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
  3.1041 +apply (induct_tac "m")
  3.1042 +apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
  3.1043 +done
  3.1044 +
  3.1045 +lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
  3.1046 +by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)
  3.1047 +
  3.1048 +text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
  3.1049 +"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
  3.1050 +  also fact that bounded and monotonic sequence converges.*}
  3.1051 +
  3.1052 +lemma Bseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> Bseq (%n. x ^ n)"
  3.1053 +apply (simp add: Bseq_def)
  3.1054 +apply (rule_tac x = 1 in exI)
  3.1055 +apply (simp add: power_abs)
  3.1056 +apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
  3.1057 +done
  3.1058 +
  3.1059 +lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
  3.1060 +apply (clarify intro!: mono_SucI2)
  3.1061 +apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
  3.1062 +done
  3.1063 +
  3.1064 +lemma convergent_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> convergent (%n. x ^ n)"
  3.1065 +by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
  3.1066 +
  3.1067 +text{* We now use NS criterion to bring proof of theorem through *}
  3.1068 +
  3.1069 +lemma NSLIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
  3.1070 +apply (simp add: NSLIMSEQ_def)
  3.1071 +apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
  3.1072 +apply (frule NSconvergentD)
  3.1073 +apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow)
  3.1074 +apply (frule HNatInfinite_add_one)
  3.1075 +apply (drule bspec, assumption)
  3.1076 +apply (drule bspec, assumption)
  3.1077 +apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
  3.1078 +apply (simp add: hyperpow_add)
  3.1079 +apply (drule approx_mult_subst_SReal, assumption)
  3.1080 +apply (drule approx_trans3, assumption)
  3.1081 +apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric])
  3.1082 +done
  3.1083 +
  3.1084 +text{* standard version *}
  3.1085 +lemma LIMSEQ_realpow_zero: "[| 0 \<le> x; x < 1 |] ==> (%n. x ^ n) ----> 0"
  3.1086 +by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
  3.1087 +
  3.1088 +lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
  3.1089 +apply (cut_tac a = a and x1 = "inverse x" in
  3.1090 +        LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
  3.1091 +apply (auto simp add: divide_inverse power_inverse)
  3.1092 +apply (simp add: inverse_eq_divide pos_divide_less_eq)
  3.1093 +done
  3.1094 +
  3.1095 +subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
  3.1096 +
  3.1097 +lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----> 0"
  3.1098 +by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)
  3.1099 +
  3.1100 +lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) ----NS> 0"
  3.1101 +by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])
  3.1102 +
  3.1103 +lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----> 0"
  3.1104 +apply (rule LIMSEQ_rabs_zero [THEN iffD1])
  3.1105 +apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
  3.1106 +done
  3.1107 +
  3.1108 +lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) ----NS> 0"
  3.1109 +by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
  3.1110 +
  3.1111 +subsection{*Hyperreals and Sequences*}
  3.1112 +
  3.1113 +text{*A bounded sequence is a finite hyperreal*}
  3.1114 +lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
  3.1115 +by (auto intro!: bexI lemma_hyprel_refl 
  3.1116 +            intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
  3.1117 +            simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
  3.1118 +                      Bseq_iff1a)
  3.1119 +
  3.1120 +text{*A sequence converging to zero defines an infinitesimal*}
  3.1121 +lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
  3.1122 +      "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
  3.1123 +apply (simp add: NSLIMSEQ_def)
  3.1124 +apply (drule_tac x = whn in bspec)
  3.1125 +apply (simp add: HNatInfinite_whn)
  3.1126 +apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat)
  3.1127 +done
  3.1128 +
  3.1129 +(***---------------------------------------------------------------
  3.1130 +    Theorems proved by Harrison in HOL that we do not need
  3.1131 +    in order to prove equivalence between Cauchy criterion
  3.1132 +    and convergence:
  3.1133 + -- Show that every sequence contains a monotonic subsequence
  3.1134 +Goal "\<exists>f. subseq f & monoseq (%n. s (f n))"
  3.1135 + -- Show that a subsequence of a bounded sequence is bounded
  3.1136 +Goal "Bseq X ==> Bseq (%n. X (f n))";
  3.1137 + -- Show we can take subsequential terms arbitrarily far
  3.1138 +    up a sequence
  3.1139 +Goal "subseq f ==> n \<le> f(n)";
  3.1140 +Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
  3.1141 + ---------------------------------------------------------------***)
  3.1142 +
  3.1143 +ML
  3.1144 +{*
  3.1145 +val Cauchy_def = thm"Cauchy_def";
  3.1146 +val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
  3.1147 +val LIMSEQ_iff = thm "LIMSEQ_iff";
  3.1148 +val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
  3.1149 +val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
  3.1150 +val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
  3.1151 +val Compl_less_set = thm "Compl_less_set";
  3.1152 +val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
  3.1153 +val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
  3.1154 +val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
  3.1155 +val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
  3.1156 +val NSLIMSEQ_const = thm "NSLIMSEQ_const";
  3.1157 +val LIMSEQ_const = thm "LIMSEQ_const";
  3.1158 +val NSLIMSEQ_add = thm "NSLIMSEQ_add";
  3.1159 +val LIMSEQ_add = thm "LIMSEQ_add";
  3.1160 +val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
  3.1161 +val LIMSEQ_mult = thm "LIMSEQ_mult";
  3.1162 +val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
  3.1163 +val LIMSEQ_minus = thm "LIMSEQ_minus";
  3.1164 +val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
  3.1165 +val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
  3.1166 +val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
  3.1167 +val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
  3.1168 +val LIMSEQ_diff = thm "LIMSEQ_diff";
  3.1169 +val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
  3.1170 +val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
  3.1171 +val LIMSEQ_inverse = thm "LIMSEQ_inverse";
  3.1172 +val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
  3.1173 +val LIMSEQ_divide = thm "LIMSEQ_divide";
  3.1174 +val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
  3.1175 +val LIMSEQ_unique = thm "LIMSEQ_unique";
  3.1176 +val limI = thm "limI";
  3.1177 +val nslimI = thm "nslimI";
  3.1178 +val lim_nslim_iff = thm "lim_nslim_iff";
  3.1179 +val convergentD = thm "convergentD";
  3.1180 +val convergentI = thm "convergentI";
  3.1181 +val NSconvergentD = thm "NSconvergentD";
  3.1182 +val NSconvergentI = thm "NSconvergentI";
  3.1183 +val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
  3.1184 +val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
  3.1185 +val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
  3.1186 +val subseq_Suc_iff = thm "subseq_Suc_iff";
  3.1187 +val monoseq_Suc = thm "monoseq_Suc";
  3.1188 +val monoI1 = thm "monoI1";
  3.1189 +val monoI2 = thm "monoI2";
  3.1190 +val mono_SucI1 = thm "mono_SucI1";
  3.1191 +val mono_SucI2 = thm "mono_SucI2";
  3.1192 +val BseqD = thm "BseqD";
  3.1193 +val BseqI = thm "BseqI";
  3.1194 +val Bseq_iff = thm "Bseq_iff";
  3.1195 +val Bseq_iff1a = thm "Bseq_iff1a";
  3.1196 +val NSBseqD = thm "NSBseqD";
  3.1197 +val NSBseqI = thm "NSBseqI";
  3.1198 +val Bseq_NSBseq = thm "Bseq_NSBseq";
  3.1199 +val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
  3.1200 +val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
  3.1201 +val NSBseq_Bseq = thm "NSBseq_Bseq";
  3.1202 +val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
  3.1203 +val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
  3.1204 +val convergent_Bseq = thm "convergent_Bseq";
  3.1205 +val Bseq_isUb = thm "Bseq_isUb";
  3.1206 +val Bseq_isLub = thm "Bseq_isLub";
  3.1207 +val NSBseq_isUb = thm "NSBseq_isUb";
  3.1208 +val NSBseq_isLub = thm "NSBseq_isLub";
  3.1209 +val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
  3.1210 +val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
  3.1211 +val Bseq_mono_convergent = thm "Bseq_mono_convergent";
  3.1212 +val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
  3.1213 +val convergent_minus_iff = thm "convergent_minus_iff";
  3.1214 +val Bseq_minus_iff = thm "Bseq_minus_iff";
  3.1215 +val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
  3.1216 +val Bseq_iff2 = thm "Bseq_iff2";
  3.1217 +val Bseq_iff3 = thm "Bseq_iff3";
  3.1218 +val BseqI2 = thm "BseqI2";
  3.1219 +val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
  3.1220 +val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
  3.1221 +val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
  3.1222 +val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
  3.1223 +val SUP_rabs_subseq = thm "SUP_rabs_subseq";
  3.1224 +val Cauchy_Bseq = thm "Cauchy_Bseq";
  3.1225 +val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
  3.1226 +val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
  3.1227 +val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
  3.1228 +val NSLIMSEQ_le = thm "NSLIMSEQ_le";
  3.1229 +val LIMSEQ_le = thm "LIMSEQ_le";
  3.1230 +val LIMSEQ_le_const = thm "LIMSEQ_le_const";
  3.1231 +val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
  3.1232 +val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
  3.1233 +val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
  3.1234 +val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
  3.1235 +val LIMSEQ_Suc = thm "LIMSEQ_Suc";
  3.1236 +val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
  3.1237 +val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
  3.1238 +val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
  3.1239 +val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
  3.1240 +val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
  3.1241 +val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
  3.1242 +val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
  3.1243 +val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
  3.1244 +val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
  3.1245 +val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
  3.1246 +val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
  3.1247 +val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
  3.1248 +val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
  3.1249 +val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
  3.1250 +val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
  3.1251 +val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
  3.1252 +val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
  3.1253 +val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
  3.1254 +val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
  3.1255 +val LIMSEQ_pow = thm "LIMSEQ_pow";
  3.1256 +val Bseq_realpow = thm "Bseq_realpow";
  3.1257 +val monoseq_realpow = thm "monoseq_realpow";
  3.1258 +val convergent_realpow = thm "convergent_realpow";
  3.1259 +val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
  3.1260 +val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
  3.1261 +val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
  3.1262 +val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
  3.1263 +val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
  3.1264 +val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
  3.1265 +val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
  3.1266 +val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
  3.1267 +val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
  3.1268 +*}
  3.1269 +
  3.1270  end
  3.1271  
     4.1 --- a/src/HOL/IsaMakefile	Wed Jul 28 16:25:40 2004 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Wed Jul 28 16:26:27 2004 +0200
     4.3 @@ -154,7 +154,7 @@
     4.4    Hyperreal/Lim.thy Hyperreal/Log.thy\
     4.5    Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy\
     4.6    Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy\
     4.7 -  Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
     4.8 +  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
     4.9    Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
    4.10    Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
    4.11    Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\