src/HOL/Real/Hyperreal/SEQ.ML
changeset 10045 c76b73e16711
child 10558 09a91221ced1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/SEQ.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,1403 @@
     1.4 +(*  Title       : SEQ.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Theory of sequence and series of real numbers
     1.8 +*) 
     1.9 +
    1.10 +(*---------------------------------------------------------------------------
    1.11 +   Example of an hypersequence (i.e. an extended standard sequence) 
    1.12 +   whose term with an hypernatural suffix is an infinitesimal i.e. 
    1.13 +   the whn'nth term of the hypersequence is a member of Infinitesimal 
    1.14 + -------------------------------------------------------------------------- *)
    1.15 +
    1.16 +Goalw [hypnat_omega_def] 
    1.17 +      "(*fNat* (%n::nat. rinv(real_of_posnat n))) whn : Infinitesimal";
    1.18 +by (auto_tac (claset(),simpset() addsimps 
    1.19 +    [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
    1.20 +by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.21 +by (auto_tac (claset(),simpset() addsimps (map rename_numerals) 
    1.22 +    [real_of_posnat_gt_zero,real_rinv_gt_zero,abs_eqI2,
    1.23 +     FreeUltrafilterNat_rinv_real_of_posnat]));
    1.24 +qed "SEQ_Infinitesimal";
    1.25 +
    1.26 +(*--------------------------------------------------------------------------
    1.27 +                  Rules for LIMSEQ and NSLIMSEQ etc.
    1.28 + --------------------------------------------------------------------------*)
    1.29 +
    1.30 +(*** LIMSEQ ***)
    1.31 +Goalw [LIMSEQ_def] 
    1.32 +      "!!X. X ----> L ==> \
    1.33 +\      ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r)";
    1.34 +by (Asm_simp_tac 1);
    1.35 +qed "LIMSEQD1";
    1.36 +
    1.37 +Goalw [LIMSEQ_def] 
    1.38 +      "!!X. [| X ----> L; #0 < r|] ==> \
    1.39 +\      EX no. ALL n. no <= n --> abs(X n + -L) < r";
    1.40 +by (Asm_simp_tac 1);
    1.41 +qed "LIMSEQD2";
    1.42 +
    1.43 +Goalw [LIMSEQ_def] 
    1.44 +      "!!X. ALL r. #0 < r --> (EX no. ALL n. \
    1.45 +\      no <= n --> abs(X n + -L) < r) ==> X ----> L";
    1.46 +by (Asm_simp_tac 1);
    1.47 +qed "LIMSEQI";
    1.48 +
    1.49 +Goalw [LIMSEQ_def] 
    1.50 +      "!!X. (X ----> L) = \
    1.51 +\      (ALL r. #0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
    1.52 +by (Simp_tac 1);
    1.53 +qed "LIMSEQ_iff";
    1.54 +
    1.55 +(*** NSLIMSEQ ***)
    1.56 +Goalw [NSLIMSEQ_def] 
    1.57 +      "!!X. X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
    1.58 +by (Asm_simp_tac 1);
    1.59 +qed "NSLIMSEQD1";
    1.60 +
    1.61 +Goalw [NSLIMSEQ_def] 
    1.62 +      "!!X. [| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
    1.63 +by (Asm_simp_tac 1);
    1.64 +qed "NSLIMSEQD2";
    1.65 +
    1.66 +Goalw [NSLIMSEQ_def] 
    1.67 +      "!!X. ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
    1.68 +by (Asm_simp_tac 1);
    1.69 +qed "NSLIMSEQI";
    1.70 +
    1.71 +Goalw [NSLIMSEQ_def] 
    1.72 +      "!!X. (X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
    1.73 +by (Simp_tac 1);
    1.74 +qed "NSLIMSEQ_iff";
    1.75 +
    1.76 +(*----------------------------------------
    1.77 +          LIMSEQ ==> NSLIMSEQ
    1.78 + ---------------------------------------*)
    1.79 +Goalw [LIMSEQ_def,NSLIMSEQ_def] 
    1.80 +      "!!X. X ----> L ==> X ----NS> L";
    1.81 +by (auto_tac (claset(),simpset() addsimps 
    1.82 +    [HNatInfinite_FreeUltrafilterNat_iff]));
    1.83 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
    1.84 +by (rtac (inf_close_minus_iff RS iffD2) 1);
    1.85 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
    1.86 +    mem_infmal_iff RS sym,hypreal_of_real_def,
    1.87 +    hypreal_minus,hypreal_add,
    1.88 +    Infinitesimal_FreeUltrafilterNat_iff]));
    1.89 +by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
    1.90 +by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1);
    1.91 +by (dres_inst_tac [("x","no")] spec 1);
    1.92 +by (Fuf_tac 1);
    1.93 +by (blast_tac (claset() addDs [less_imp_le]) 1);
    1.94 +qed "LIMSEQ_NSLIMSEQ";
    1.95 +
    1.96 +(*-------------------------------------------------------------
    1.97 +          NSLIMSEQ ==> LIMSEQ
    1.98 +    proving NS def ==> Standard def is trickier as usual 
    1.99 + -------------------------------------------------------------*)
   1.100 +(* the following sequence f(n) defines a hypernatural *)
   1.101 +(* lemmas etc. first *)
   1.102 +Goal "!!(f::nat=>nat). ALL n. n <= f n \
   1.103 +\          ==> {n. f n = 0} = {0} | {n. f n = 0} = {}";
   1.104 +by (Auto_tac);
   1.105 +by (dres_inst_tac [("x","xa")] spec 1);
   1.106 +by (dres_inst_tac [("x","x")] spec 2);
   1.107 +by (Auto_tac);
   1.108 +val lemma_NSLIMSEQ1 = result();
   1.109 +
   1.110 +Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
   1.111 +by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
   1.112 +val lemma_NSLIMSEQ2 = result();
   1.113 +
   1.114 +Goal "!!(f::nat=>nat). ALL n. n <= f n \
   1.115 +\          ==> {n. f n = Suc u} <= {n. n <= Suc u}";
   1.116 +by (Auto_tac);
   1.117 +by (dres_inst_tac [("x","x")] spec 1);
   1.118 +by (Auto_tac);
   1.119 +val lemma_NSLIMSEQ3 = result();
   1.120 +
   1.121 +Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
   1.122 +\         ==> finite {n. f n <= u}";
   1.123 +by (induct_tac "u" 1);
   1.124 +by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
   1.125 +by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
   1.126 +    finite_nat_le_segment],simpset()));
   1.127 +by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
   1.128 +by (ALLGOALS(Asm_simp_tac));
   1.129 +qed "NSLIMSEQ_finite_set";
   1.130 +
   1.131 +Goal "- {n. u < (f::nat=>nat) n} = {n. f n <= u}";
   1.132 +by (auto_tac (claset() addDs [less_le_trans],
   1.133 +    simpset() addsimps [le_def]));
   1.134 +qed "Compl_less_set";
   1.135 +
   1.136 +(* the index set is in the free ultrafilter *)
   1.137 +Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
   1.138 +\         ==> {n. u < f n} : FreeUltrafilterNat";
   1.139 +by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1);
   1.140 +by (rtac FreeUltrafilterNat_finite 1);
   1.141 +by (auto_tac (claset() addDs [NSLIMSEQ_finite_set],
   1.142 +    simpset() addsimps [Compl_less_set]));
   1.143 +qed "FreeUltrafilterNat_NSLIMSEQ";
   1.144 +
   1.145 +(* thus, the sequence defines an infinite hypernatural! *)
   1.146 +Goal "!!f. ALL n. n <= f n \
   1.147 +\         ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite";
   1.148 +by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
   1.149 +by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
   1.150 +by (etac FreeUltrafilterNat_NSLIMSEQ 1);
   1.151 +qed "HNatInfinite_NSLIMSEQ";
   1.152 +
   1.153 +val lemmaLIM = CLAIM  "{n. X (f n) + - L = Y n} Int {n. abs (Y n) < r} <= \
   1.154 +\         {n. abs (X (f n) + - L) < r}";
   1.155 +
   1.156 +Goal "{n. abs (X (f n) + - L) < r} Int \
   1.157 +\         {n. r <= abs (X (f n) + - (L::real))} = {}";
   1.158 +by (auto_tac (claset() addDs [real_less_le_trans] 
   1.159 +    addIs [real_less_irrefl],simpset()));
   1.160 +val lemmaLIM2 = result();
   1.161 +
   1.162 +Goal "!!f. [| #0 < r; ALL n. r <= abs (X (f n) + - L); \
   1.163 +\          (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \
   1.164 +\          - hypreal_of_real  L @= 0 |] ==> False";
   1.165 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.166 +    mem_infmal_iff RS sym,hypreal_of_real_def,
   1.167 +    hypreal_minus,hypreal_add,
   1.168 +    Infinitesimal_FreeUltrafilterNat_iff]));
   1.169 +by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
   1.170 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   1.171 +by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
   1.172 +by (dtac FreeUltrafilterNat_all 1);
   1.173 +by (thin_tac "{n. abs (Y n) < r} : FreeUltrafilterNat" 1);
   1.174 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   1.175 +by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
   1.176 +    FreeUltrafilterNat_empty]) 1);
   1.177 +val lemmaLIM3 = result();
   1.178 +
   1.179 +Goalw [LIMSEQ_def,NSLIMSEQ_def] 
   1.180 +      "!!X. X ----NS> L ==> X ----> L";
   1.181 +by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
   1.182 +by (Step_tac 1);
   1.183 +(* skolemization step *)
   1.184 +by (dtac choice 1 THEN Step_tac 1);
   1.185 +by (dres_inst_tac [("x","Abs_hypnat(hypnatrel^^{f})")] bspec 1);
   1.186 +by (dtac (inf_close_minus_iff RS iffD1) 2);
   1.187 +by (fold_tac [real_le_def]);
   1.188 +by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
   1.189 +by (blast_tac (claset() addIs [rename_numerals lemmaLIM3]) 1);
   1.190 +qed "NSLIMSEQ_LIMSEQ";
   1.191 +
   1.192 +(* Now the all important result is trivially proved! *)
   1.193 +Goal "(f ----> L) = (f ----NS> L)";
   1.194 +by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1);
   1.195 +qed "LIMSEQ_NSLIMSEQ_iff";
   1.196 +
   1.197 +(*-------------------------------------------------------------------
   1.198 +                   Theorems about sequences
   1.199 + ------------------------------------------------------------------*)
   1.200 +Goalw [NSLIMSEQ_def] "(%n. k) ----NS> k";
   1.201 +by (Auto_tac);
   1.202 +qed "NSLIMSEQ_const";
   1.203 +
   1.204 +Goalw [LIMSEQ_def] "(%n. k) ----> k";
   1.205 +by (Auto_tac);
   1.206 +qed "LIMSEQ_const";
   1.207 +
   1.208 +Goalw [NSLIMSEQ_def]
   1.209 +      "!!X. [| X ----NS> a; Y ----NS> b |] \
   1.210 +\           ==> (%n. X n + Y n) ----NS> a + b";
   1.211 +by (auto_tac (claset() addIs [inf_close_add],
   1.212 +    simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
   1.213 +qed "NSLIMSEQ_add";
   1.214 +
   1.215 +Goal "!!X. [| X ----> a; Y ----> b |] \
   1.216 +\           ==> (%n. X n + Y n) ----> a + b";
   1.217 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   1.218 +    NSLIMSEQ_add]) 1);
   1.219 +qed "LIMSEQ_add";
   1.220 +
   1.221 +Goalw [NSLIMSEQ_def]
   1.222 +      "!!X. [| X ----NS> a; Y ----NS> b |] \
   1.223 +\           ==> (%n. X n * Y n) ----NS> a * b";
   1.224 +by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close],
   1.225 +    simpset() addsimps [hypreal_of_real_mult]));
   1.226 +qed "NSLIMSEQ_mult";
   1.227 +
   1.228 +Goal "!!X. [| X ----> a; Y ----> b |] \
   1.229 +\           ==> (%n. X n * Y n) ----> a * b";
   1.230 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   1.231 +    NSLIMSEQ_mult]) 1);
   1.232 +qed "LIMSEQ_mult";
   1.233 +
   1.234 +Goalw [NSLIMSEQ_def] 
   1.235 +      "!!X. X ----NS> a ==> (%n. -(X n)) ----NS> -a";
   1.236 +by (auto_tac (claset() addIs [inf_close_minus],
   1.237 +    simpset() addsimps [starfunNat_minus RS sym,
   1.238 +    hypreal_of_real_minus]));
   1.239 +qed "NSLIMSEQ_minus";
   1.240 +
   1.241 +Goal "!!X. X ----> a ==> (%n. -(X n)) ----> -a";
   1.242 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   1.243 +    NSLIMSEQ_minus]) 1);
   1.244 +qed "LIMSEQ_minus";
   1.245 +
   1.246 +Goal "(%n. -(X n)) ----> -a ==> X ----> a";
   1.247 +by (dtac LIMSEQ_minus 1);
   1.248 +by (Asm_full_simp_tac 1);
   1.249 +qed "LIMSEQ_minus_cancel";
   1.250 +
   1.251 +Goal "(%n. -(X n)) ----NS> -a ==> X ----NS> a";
   1.252 +by (dtac NSLIMSEQ_minus 1);
   1.253 +by (Asm_full_simp_tac 1);
   1.254 +qed "NSLIMSEQ_minus_cancel";
   1.255 +
   1.256 +Goal "!!X. [| X ----NS> a; Y ----NS> b |] \
   1.257 +\               ==> (%n. X n + -Y n) ----NS> a + -b";
   1.258 +by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
   1.259 +by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
   1.260 +qed "NSLIMSEQ_add_minus";
   1.261 +
   1.262 +Goal "!!X. [| X ----> a; Y ----> b |] \
   1.263 +\               ==> (%n. X n + -Y n) ----> a + -b";
   1.264 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   1.265 +    NSLIMSEQ_add_minus]) 1);
   1.266 +qed "LIMSEQ_add_minus";
   1.267 +
   1.268 +goalw SEQ.thy [real_diff_def] 
   1.269 +      "!!X. [| X ----> a; Y ----> b |] \
   1.270 +\               ==> (%n. X n - Y n) ----> a - b";
   1.271 +by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
   1.272 +qed "LIMSEQ_diff";
   1.273 +
   1.274 +goalw SEQ.thy [real_diff_def] 
   1.275 +      "!!X. [| X ----NS> a; Y ----NS> b |] \
   1.276 +\               ==> (%n. X n - Y n) ----NS> a - b";
   1.277 +by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
   1.278 +qed "NSLIMSEQ_diff";
   1.279 +
   1.280 +(*---------------------------------------------------------------
   1.281 +    Proof is exactly same as that of NSLIM_rinv except 
   1.282 +    for starfunNat_hrinv2 --- would not be the case if we
   1.283 +    had generalised net theorems for example. Not our
   1.284 +    real concern though.
   1.285 + --------------------------------------------------------------*)
   1.286 +Goalw [NSLIMSEQ_def] 
   1.287 +       "!!X. [| X ----NS> a; a ~= #0 |] \
   1.288 +\            ==> (%n. rinv(X n)) ----NS> rinv(a)";
   1.289 +by (Step_tac 1);
   1.290 +by (dtac bspec 1 THEN auto_tac (claset(),simpset() 
   1.291 +    addsimps [hypreal_of_real_not_zero_iff RS sym,
   1.292 +    hypreal_of_real_hrinv RS sym]));
   1.293 +by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 
   1.294 +    THEN assume_tac 1);
   1.295 +by (auto_tac (claset() addSEs [(starfunNat_hrinv2 RS subst),
   1.296 +    inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal],
   1.297 +    simpset()));
   1.298 +qed "NSLIMSEQ_rinv";
   1.299 +
   1.300 +(*------ Standard version of theorem -------*)
   1.301 +Goal
   1.302 +       "!!X. [| X ----> a; a ~= #0 |] \
   1.303 +\            ==> (%n. rinv(X n)) ----> rinv(a)";
   1.304 +by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_rinv,
   1.305 +    LIMSEQ_NSLIMSEQ_iff]) 1);
   1.306 +qed "LIMSEQ_rinv";
   1.307 +
   1.308 +(* trivially proved *)
   1.309 +Goal
   1.310 +     "!!X. [| X ----NS> a; Y ----NS> b; b ~= #0 |] \
   1.311 +\          ==> (%n. (X n) * rinv(Y n)) ----NS> a*rinv(b)";
   1.312 +by (blast_tac (claset() addDs [NSLIMSEQ_rinv,NSLIMSEQ_mult]) 1);
   1.313 +qed "NSLIMSEQ_mult_rinv";
   1.314 +
   1.315 +(* let's give a standard proof of theorem *)
   1.316 +Goal 
   1.317 +     "!!X. [| X ----> a; Y ----> b; b ~= #0 |] \
   1.318 +\          ==> (%n. (X n) * rinv(Y n)) ----> a*rinv(b)";
   1.319 +by (blast_tac (claset() addDs [LIMSEQ_rinv,LIMSEQ_mult]) 1);
   1.320 +qed "LIMSEQ_mult_rinv";
   1.321 +
   1.322 +(*-----------------------------------------------
   1.323 +            Uniqueness of limit
   1.324 + ----------------------------------------------*)
   1.325 +Goalw [NSLIMSEQ_def] 
   1.326 +      "!!X. [| X ----NS> a; X ----NS> b |] \
   1.327 +\           ==> a = b";
   1.328 +by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
   1.329 +by (auto_tac (claset() addDs [inf_close_trans3],simpset()));
   1.330 +qed "NSLIMSEQ_unique";
   1.331 +
   1.332 +Goal "!!X. [| X ----> a; X ----> b |] \
   1.333 +\              ==> a = b";
   1.334 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
   1.335 +    NSLIMSEQ_unique]) 1);
   1.336 +qed "LIMSEQ_unique";
   1.337 +
   1.338 +(*-----------------------------------------------------------------
   1.339 +    theorems about nslim and lim
   1.340 + ----------------------------------------------------------------*)
   1.341 +Goalw [lim_def] "!!X. X ----> L ==> lim X = L";
   1.342 +by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
   1.343 +qed "limI";
   1.344 +
   1.345 +Goalw [nslim_def] "!!X. X ----NS> L ==> nslim X = L";
   1.346 +by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
   1.347 +qed "nslimI";
   1.348 +
   1.349 +Goalw [lim_def,nslim_def] "lim X = nslim X";
   1.350 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
   1.351 +qed "lim_nslim_iff";
   1.352 +
   1.353 +(*------------------------------------------------------------------
   1.354 +                      Convergence
   1.355 + -----------------------------------------------------------------*)
   1.356 +Goalw [convergent_def]
   1.357 +      "!!f. convergent X ==> EX L. (X ----> L)";
   1.358 +by (assume_tac 1);
   1.359 +qed "convergentD";
   1.360 +
   1.361 +Goalw [convergent_def]
   1.362 +      "!!f. (X ----> L) ==> convergent X";
   1.363 +by (Blast_tac 1);
   1.364 +qed "convergentI";
   1.365 +
   1.366 +Goalw [NSconvergent_def]
   1.367 +      "!!f. NSconvergent X ==> EX L. (X ----NS> L)";
   1.368 +by (assume_tac 1);
   1.369 +qed "NSconvergentD";
   1.370 +
   1.371 +Goalw [NSconvergent_def]
   1.372 +      "!!f. (X ----NS> L) ==> NSconvergent X";
   1.373 +by (Blast_tac 1);
   1.374 +qed "NSconvergentI";
   1.375 +
   1.376 +Goalw [convergent_def,NSconvergent_def] 
   1.377 +      "convergent X = NSconvergent X";
   1.378 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
   1.379 +qed "convergent_NSconvergent_iff";
   1.380 +
   1.381 +Goalw [NSconvergent_def,nslim_def] 
   1.382 +      "NSconvergent X = (X ----NS> nslim X)";
   1.383 +by (auto_tac (claset() addIs [someI],simpset()));
   1.384 +qed "NSconvergent_NSLIMSEQ_iff";
   1.385 +
   1.386 +Goalw [convergent_def,lim_def] 
   1.387 +      "convergent X = (X ----> lim X)";
   1.388 +by (auto_tac (claset() addIs [someI],simpset()));
   1.389 +qed "convergent_LIMSEQ_iff";
   1.390 +
   1.391 +(*-------------------------------------------------------------------
   1.392 +         Subsequence (alternative definition) (e.g. Hoskins)
   1.393 + ------------------------------------------------------------------*)
   1.394 +Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
   1.395 +by (auto_tac (claset() addSDs [less_eq_Suc_add],simpset()));
   1.396 +by (nat_ind_tac "k" 1);
   1.397 +by (auto_tac (claset() addIs [less_trans],simpset()));
   1.398 +qed "subseq_Suc_iff";
   1.399 +
   1.400 +(*-------------------------------------------------------------------
   1.401 +                   Monotonicity
   1.402 + ------------------------------------------------------------------*)
   1.403 +
   1.404 +Goalw [monoseq_def]
   1.405 +   "monoseq X = ((ALL n. X n <= X (Suc n)) \
   1.406 +\                | (ALL n. X (Suc n) <= X n))";
   1.407 +by (auto_tac (claset () addSDs [le_imp_less_or_eq],
   1.408 +    simpset() addsimps [real_le_refl]));
   1.409 +by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
   1.410 +    addSDs [less_eq_Suc_add],simpset()));
   1.411 +by (induct_tac "ka" 1);
   1.412 +by (auto_tac (claset() addIs [real_le_trans],simpset()));
   1.413 +by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
   1.414 +by (induct_tac "k" 1);
   1.415 +by (auto_tac (claset() addIs [real_le_trans],simpset()));
   1.416 +qed "monoseq_Suc";
   1.417 +
   1.418 +Goalw [monoseq_def] 
   1.419 +       "!!X. ALL m n. m <= n --> X m <= X n ==> monoseq X";
   1.420 +by (Blast_tac 1);
   1.421 +qed "monoI1";
   1.422 +
   1.423 +Goalw [monoseq_def] 
   1.424 +       "!!X. ALL m n. m <= n --> X n <= X m ==> monoseq X";
   1.425 +by (Blast_tac 1);
   1.426 +qed "monoI2";
   1.427 +
   1.428 +Goal "!!X. ALL n. X n <= X (Suc n) ==> monoseq X";
   1.429 +by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
   1.430 +qed "mono_SucI1";
   1.431 +
   1.432 +Goal "!!X. ALL n. X (Suc n) <= X n ==> monoseq X";
   1.433 +by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
   1.434 +qed "mono_SucI2";
   1.435 +
   1.436 +(*-------------------------------------------------------------------
   1.437 +                  Bounded Sequence
   1.438 + ------------------------------------------------------------------*)
   1.439 +Goalw [Bseq_def] 
   1.440 +      "!!X. Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)";
   1.441 +by (assume_tac 1);
   1.442 +qed "BseqD";
   1.443 +
   1.444 +Goalw [Bseq_def]
   1.445 +      "!!X. [| #0 < K; ALL n. abs(X n) <= K |] \
   1.446 +\           ==> Bseq X";
   1.447 +by (Blast_tac 1);
   1.448 +qed "BseqI";
   1.449 +
   1.450 +Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
   1.451 +\         (EX N. ALL n. abs(X n) <= real_of_posnat N)";
   1.452 +by (auto_tac (claset(),simpset() addsimps 
   1.453 +    (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
   1.454 +by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
   1.455 +by (blast_tac (claset() addIs [real_le_less_trans,
   1.456 +    real_less_imp_le]) 1);
   1.457 +by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def]));
   1.458 +qed "lemma_NBseq_def";
   1.459 +
   1.460 +(* alternative definition for Bseq *)
   1.461 +Goalw [Bseq_def] 
   1.462 +      "Bseq X = (EX N. ALL n. abs(X n) <= real_of_posnat N)";
   1.463 +by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
   1.464 +qed "Bseq_iff";
   1.465 +
   1.466 +Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
   1.467 +\         (EX N. ALL n. abs(X n) < real_of_posnat N)";
   1.468 +by (auto_tac (claset(),simpset() addsimps 
   1.469 +    (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero]));
   1.470 +by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
   1.471 +by (blast_tac (claset() addIs [real_less_trans,
   1.472 +    real_le_less_trans]) 1);
   1.473 +by (auto_tac (claset() addIs [real_less_imp_le],
   1.474 +    simpset() addsimps [real_of_posnat_def]));
   1.475 +qed "lemma_NBseq_def2";
   1.476 +
   1.477 +(* yet another definition for Bseq *)
   1.478 +Goalw [Bseq_def] 
   1.479 +      "Bseq X = (EX N. ALL n. abs(X n) < real_of_posnat N)";
   1.480 +by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
   1.481 +qed "Bseq_iff1a";
   1.482 +
   1.483 +Goalw [NSBseq_def]
   1.484 +      "!!X. [| NSBseq X; N: HNatInfinite |] \
   1.485 +\           ==> (*fNat* X) N : HFinite";
   1.486 +by (Blast_tac 1);
   1.487 +qed "NSBseqD";
   1.488 +
   1.489 +Goalw [NSBseq_def]
   1.490 +      "!!X. ALL N: HNatInfinite. (*fNat* X) N : HFinite \
   1.491 +\           ==> NSBseq X";
   1.492 +by (assume_tac 1);
   1.493 +qed "NSBseqI";
   1.494 +
   1.495 +(*-----------------------------------------------------------
   1.496 +       Standard definition ==> NS definition
   1.497 + ----------------------------------------------------------*)
   1.498 +(* a few lemmas *)
   1.499 +Goal "ALL n. abs(X n) <= K ==> \
   1.500 +\     ALL n. abs(X((f::nat=>nat) n)) <= K";
   1.501 +by (Auto_tac);
   1.502 +val lemma_Bseq = result();
   1.503 +
   1.504 +Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
   1.505 +by (Step_tac 1);
   1.506 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.507 +by (auto_tac (claset(),simpset() addsimps [starfunNat,    
   1.508 +    HFinite_FreeUltrafilterNat_iff,
   1.509 +    HNatInfinite_FreeUltrafilterNat_iff]));
   1.510 +by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
   1.511 +by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
   1.512 +by (res_inst_tac [("x","K+#1")] exI 1);
   1.513 +by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1);
   1.514 +by (Ultra_tac 1);
   1.515 +qed "Bseq_NSBseq";
   1.516 +
   1.517 +(*---------------------------------------------------------------
   1.518 +       NS  definition ==> Standard definition
   1.519 + ---------------------------------------------------------------*)
   1.520 +(* similar to NSLIM proof in REALTOPOS *)
   1.521 +(*------------------------------------------------------------------- 
   1.522 +   We need to get rid of the real variable and do so by proving the
   1.523 +   following which relies on the Archimedean property of the reals
   1.524 +   When we skolemize we then get the required function f::nat=>nat 
   1.525 +   o/w we would be stuck with a skolem function f :: real=>nat which
   1.526 +   is not what we want (read useless!)
   1.527 + -------------------------------------------------------------------*)
   1.528 + 
   1.529 +Goal "!!X. ALL K. #0 < K --> (EX n. K < abs (X n)) \
   1.530 +\          ==> ALL N. EX n. real_of_posnat  N < abs (X n)";
   1.531 +by (Step_tac 1);
   1.532 +by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 1);
   1.533 +by (Blast_tac 1);
   1.534 +val lemmaNSBseq = result();
   1.535 +
   1.536 +Goal "!!X. ALL K. #0 < K --> (EX n. K < abs (X n)) \
   1.537 +\         ==> EX f. ALL N. real_of_posnat  N < abs (X (f N))";
   1.538 +by (dtac lemmaNSBseq 1);
   1.539 +by (dtac choice 1);
   1.540 +by (Blast_tac 1);
   1.541 +val lemmaNSBseq2 = result();
   1.542 +
   1.543 +Goal "!!X. ALL N. real_of_posnat  N < abs (X (f N)) \
   1.544 +\         ==>  Abs_hypreal(hyprel^^{X o f}) : HInfinite";
   1.545 +by (auto_tac (claset(),simpset() addsimps 
   1.546 +    [HInfinite_FreeUltrafilterNat_iff,o_def]));
   1.547 +by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, 
   1.548 +    Step_tac 1]);
   1.549 +by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
   1.550 +by (blast_tac (claset() addDs [FreeUltrafilterNat_all,
   1.551 +    FreeUltrafilterNat_Int] addIs [real_less_trans,
   1.552 +    FreeUltrafilterNat_subset]) 1);
   1.553 +qed "real_seq_to_hypreal_HInfinite";
   1.554 +
   1.555 +(*--------------------------------------------------------------------------------
   1.556 +     Now prove that we can get out an infinite hypernatural as well 
   1.557 +     defined using the skolem function f::nat=>nat above
   1.558 + --------------------------------------------------------------------------------*)
   1.559 +
   1.560 +Goal "{n. f n <= Suc u & real_of_posnat  n < abs (X (f n))} <= \
   1.561 +\         {n. f n <= u & real_of_posnat  n < abs (X (f n))} \
   1.562 +\         Un {n. real_of_posnat n < abs (X (Suc u))}";
   1.563 +by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le],
   1.564 +    simpset() addsimps [less_Suc_eq]));
   1.565 +val lemma_finite_NSBseq = result();
   1.566 +
   1.567 +Goal "finite {n. f n <= (u::nat) &  real_of_posnat n < abs(X(f n))}";
   1.568 +by (induct_tac "u" 1);
   1.569 +by (rtac (CLAIM "{n. f n <= (0::nat) & real_of_posnat n < abs (X (f n))} <= \
   1.570 +\         {n. real_of_posnat n < abs (X 0)}"
   1.571 +          RS finite_subset) 1);
   1.572 +by (rtac finite_real_of_posnat_less_real 1);
   1.573 +by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
   1.574 +by (auto_tac (claset() addIs [finite_real_of_posnat_less_real],simpset()));
   1.575 +val lemma_finite_NSBseq2 = result();
   1.576 +
   1.577 +Goal "ALL N. real_of_posnat  N < abs (X (f N)) \
   1.578 +\     ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite";
   1.579 +by (auto_tac (claset(),simpset() addsimps 
   1.580 +    [HNatInfinite_FreeUltrafilterNat_iff]));
   1.581 +by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, 
   1.582 +    Step_tac 1]);
   1.583 +by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
   1.584 +by (asm_full_simp_tac (simpset() addsimps 
   1.585 +   [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
   1.586 +\   = {n. f n <= u}" [le_def]]) 1);
   1.587 +by (dtac FreeUltrafilterNat_all 1);
   1.588 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   1.589 +by (auto_tac (claset(),simpset() addsimps 
   1.590 +    [CLAIM "({n. f n <= u} Int {n. real_of_posnat n < abs(X(f n))}) = \
   1.591 +\          {n. f n <= (u::nat) &  real_of_posnat n < abs(X(f n))}",
   1.592 +     lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
   1.593 +qed "HNatInfinite_skolem_f";
   1.594 +
   1.595 +Goalw [Bseq_def,NSBseq_def] 
   1.596 +      "NSBseq X ==> Bseq X";
   1.597 +by (rtac ccontr 1);
   1.598 +by (auto_tac (claset(),simpset() addsimps [real_le_def]));
   1.599 +by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
   1.600 +by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
   1.601 +by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
   1.602 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.603 +    o_def,HFinite_HInfinite_iff]));
   1.604 +qed "NSBseq_Bseq";
   1.605 +
   1.606 +(*----------------------------------------------------------------------
   1.607 +  Equivalence of nonstandard and standard definitions 
   1.608 +  for a bounded sequence
   1.609 + -----------------------------------------------------------------------*)
   1.610 +Goal "(Bseq X) = (NSBseq X)";
   1.611 +by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1);
   1.612 +qed "Bseq_NSBseq_iff";
   1.613 +
   1.614 +(*----------------------------------------------------------------------
   1.615 +   A convergent sequence is bounded
   1.616 +   (Boundedness as a necessary condition for convergence)
   1.617 + -----------------------------------------------------------------------*)
   1.618 +(* easier --- nonstandard version - no existential as usual *)
   1.619 +Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
   1.620 +          "!!X. NSconvergent X ==> NSBseq X";
   1.621 +by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
   1.622 +               (inf_close_sym RSN (2,inf_close_HFinite))]) 1);
   1.623 +qed "NSconvergent_NSBseq";
   1.624 +
   1.625 +(* standard version - easily now proved using *)
   1.626 +(* equivalence of NS and standard definitions *)
   1.627 +Goal "!!X. convergent X ==> Bseq X";
   1.628 +by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
   1.629 +    convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
   1.630 +qed "convergent_Bseq";
   1.631 +
   1.632 +(*----------------------------------------------------------------------
   1.633 +             Results about Ubs and Lubs of bounded sequences
   1.634 + -----------------------------------------------------------------------*)
   1.635 +Goalw [Bseq_def]
   1.636 +  "!!(X::nat=>real). Bseq X ==> \
   1.637 +\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
   1.638 +by (auto_tac (claset() addIs [isUbI,setleI],
   1.639 +    simpset() addsimps [abs_le_interval_iff]));
   1.640 +qed "Bseq_isUb";
   1.641 +
   1.642 +(*----------------------------------------------------------------------
   1.643 +   Use completeness of reals (supremum property) 
   1.644 +   to show that any bounded sequence has a lub 
   1.645 +-----------------------------------------------------------------------*)
   1.646 +Goal
   1.647 +  "!!(X::nat=>real). Bseq X ==> \
   1.648 +\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
   1.649 +by (blast_tac (claset() addIs [reals_complete,
   1.650 +    Bseq_isUb]) 1);
   1.651 +qed "Bseq_isLub";
   1.652 +
   1.653 +(* nonstandard version of premise will be *)
   1.654 +(* handy when we work in NS universe      *)
   1.655 +Goal   "!!X. NSBseq X ==> \
   1.656 +\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
   1.657 +by (asm_full_simp_tac (simpset() addsimps 
   1.658 +    [Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
   1.659 +qed "NSBseq_isUb";
   1.660 +
   1.661 +Goal
   1.662 +  "!!X. NSBseq X ==> \
   1.663 +\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
   1.664 +by (asm_full_simp_tac (simpset() addsimps 
   1.665 +    [Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
   1.666 +qed "NSBseq_isLub";
   1.667 +
   1.668 +(*--------------------------------------------------------------------
   1.669 +             Bounded and monotonic sequence converges              
   1.670 + --------------------------------------------------------------------*)
   1.671 +(* lemmas *)
   1.672 +Goal 
   1.673 +     "!!(X::nat=>real). [| ALL m n. m <= n -->  X m <= X n; \
   1.674 +\                 isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \
   1.675 +\              |] ==> ALL n. ma <= n --> X n = X ma";
   1.676 +by (Step_tac 1);
   1.677 +by (dres_inst_tac [("y","X n")] isLubD2 1);
   1.678 +by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym])));
   1.679 +val lemma_converg1 = result();
   1.680 +
   1.681 +(*------------------------------------------------------------------- 
   1.682 +   The best of both world: Easier to prove this result as a standard
   1.683 +   theorem and then use equivalence to "transfer" it into the
   1.684 +   equivalent nonstandard form if needed!
   1.685 + -------------------------------------------------------------------*)
   1.686 +Goalw [LIMSEQ_def] 
   1.687 +         "!!X. ALL n. m <= n --> X n = X m \
   1.688 +\         ==> EX L. (X ----> L)";  
   1.689 +by (res_inst_tac [("x","X m")] exI 1);
   1.690 +by (Step_tac 1);
   1.691 +by (res_inst_tac [("x","m")] exI 1);
   1.692 +by (Step_tac 1);
   1.693 +by (dtac spec 1 THEN etac impE 1);
   1.694 +by (Auto_tac);
   1.695 +qed "Bmonoseq_LIMSEQ";
   1.696 +
   1.697 +(* Now same theorem in terms of NS limit *)
   1.698 +Goal "!!X. ALL n. m <= n --> X n = X m \
   1.699 +\         ==> EX L. (X ----NS> L)";  
   1.700 +by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
   1.701 +    simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
   1.702 +qed "Bmonoseq_NSLIMSEQ";
   1.703 +
   1.704 +(* a few more lemmas *)
   1.705 +Goal "!!(X::nat=>real). \
   1.706 +\              [| ALL m. X m ~= U; \
   1.707 +\                 isLub UNIV {x. EX n. X n = x} U \
   1.708 +\              |] ==> ALL m. X m < U";
   1.709 +by (Step_tac 1);
   1.710 +by (dres_inst_tac [("y","X m")] isLubD2 1);
   1.711 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
   1.712 +              simpset()));
   1.713 +val lemma_converg2 = result();
   1.714 +
   1.715 +Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
   1.716 +\         isUb UNIV {x. EX n. X n = x} U";
   1.717 +by (rtac (setleI RS isUbI) 1);
   1.718 +by (Auto_tac);
   1.719 +val lemma_converg3 = result();
   1.720 +
   1.721 +(* FIXME: U - T < U redundant *)
   1.722 +Goal "!!(X::nat=> real). \
   1.723 +\              [| ALL m. X m ~= U; \
   1.724 +\                 isLub UNIV {x. EX n. X n = x} U; \
   1.725 +\                 #0 < T; \
   1.726 +\                 U + - T < U \
   1.727 +\              |] ==> EX m. U + -T < X m & X m < U";
   1.728 +by (dtac lemma_converg2 1 THEN assume_tac 1);
   1.729 +by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
   1.730 +by (fold_tac [real_le_def]);
   1.731 +by (dtac lemma_converg3 1);
   1.732 +by (dtac isLub_le_isUb 1 THEN assume_tac 1);
   1.733 +by (auto_tac (claset() addDs [real_less_le_trans],
   1.734 +    simpset() addsimps [real_minus_zero_le_iff]));
   1.735 +val lemma_converg4 = result();
   1.736 +
   1.737 +(*-------------------------------------------------------------------
   1.738 +  A standard proof of the theorem for monotone increasing sequence
   1.739 + ------------------------------------------------------------------*)
   1.740 +
   1.741 +Goalw [convergent_def] 
   1.742 +     "!!X. [| Bseq X; ALL m n. m <= n --> X m <= X n |] \
   1.743 +\                ==> convergent X";
   1.744 +by (forward_tac [Bseq_isLub] 1);
   1.745 +by (Step_tac 1);
   1.746 +by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
   1.747 +by (blast_tac (claset() addDs [lemma_converg1,
   1.748 +    Bmonoseq_LIMSEQ]) 1);
   1.749 +(* second case *)
   1.750 +by (res_inst_tac [("x","U")] exI 1);
   1.751 +by (rtac LIMSEQI 1 THEN Step_tac 1);
   1.752 +by (forward_tac [lemma_converg2] 1 THEN assume_tac 1);
   1.753 +by (dtac lemma_converg4 1 THEN Auto_tac);
   1.754 +by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
   1.755 +by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
   1.756 +by (rotate_tac 3 1 THEN dres_inst_tac [("x","n")] spec 1);
   1.757 +by (arith_tac 1);
   1.758 +qed "Bseq_mono_convergent";
   1.759 +
   1.760 +(* NS version of theorem *)
   1.761 +Goalw [convergent_def] 
   1.762 +     "!!X. [| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
   1.763 +\                ==> NSconvergent X";
   1.764 +by (auto_tac (claset() addIs [Bseq_mono_convergent], 
   1.765 +    simpset() addsimps [convergent_NSconvergent_iff RS sym,
   1.766 +    Bseq_NSBseq_iff RS sym]));
   1.767 +qed "NSBseq_mono_NSconvergent";
   1.768 +
   1.769 +Goalw [convergent_def] 
   1.770 +      "!!X. (convergent X) = (convergent (%n. -(X n)))";
   1.771 +by (auto_tac (claset() addDs [LIMSEQ_minus],simpset()));
   1.772 +by (dtac LIMSEQ_minus 1 THEN Auto_tac);
   1.773 +qed "convergent_minus_iff";
   1.774 +
   1.775 +Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
   1.776 +by (asm_full_simp_tac (simpset() addsimps [abs_minus_cancel]) 1);
   1.777 +qed "Bseq_minus_iff";
   1.778 +
   1.779 +(*--------------------------------
   1.780 +   **** main mono theorem ****
   1.781 + -------------------------------*)
   1.782 +Goalw [monoseq_def] 
   1.783 +      "!!X. [| Bseq X; monoseq X |] ==> convergent X";
   1.784 +by (Step_tac 1);
   1.785 +by (rtac (convergent_minus_iff RS ssubst) 2);
   1.786 +by (dtac (Bseq_minus_iff RS ssubst) 2);
   1.787 +by (auto_tac (claset() addSIs [Bseq_mono_convergent],simpset()));
   1.788 +qed "Bseq_monoseq_convergent";
   1.789 +
   1.790 +(*----------------------------------------------------------------
   1.791 +          A few more equivalence theorems for boundedness 
   1.792 + ---------------------------------------------------------------*)
   1.793 + 
   1.794 +(***--- alternative formulation for boundedness---***)
   1.795 +Goalw [Bseq_def] 
   1.796 +   "Bseq X = (EX k x. #0 < k & (ALL n. abs(X(n) + -x) <= k))";
   1.797 +by (Step_tac 1);
   1.798 +by (res_inst_tac [("x","K")] exI 1);
   1.799 +by (res_inst_tac [("x","0")] exI 1);
   1.800 +by (Auto_tac);
   1.801 +by (res_inst_tac [("x","k + abs(x)")] exI 1);
   1.802 +by (Step_tac 1);
   1.803 +by (dres_inst_tac [("x","n")] spec 2);
   1.804 +by (ALLGOALS(arith_tac));
   1.805 +qed "Bseq_iff2";
   1.806 +
   1.807 +(***--- alternative formulation for boundedness ---***)
   1.808 +Goal "Bseq X = (EX k N. #0 < k & (ALL n. \
   1.809 +\                        abs(X(n) + -X(N)) <= k))";
   1.810 +by (Step_tac 1);
   1.811 +by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
   1.812 +by (Step_tac 1);
   1.813 +by (res_inst_tac [("x","K + abs(X N)")] exI 1);
   1.814 +by (Auto_tac);
   1.815 +by (etac abs_add_pos_gt_zero 1);
   1.816 +by (res_inst_tac [("x","N")] exI 1);
   1.817 +by (Step_tac 1);
   1.818 +by (res_inst_tac [("j","abs(X n) + abs (X N)")] 
   1.819 +    real_le_trans 1);
   1.820 +by (auto_tac (claset() addIs [abs_triangle_minus_ineq,
   1.821 +    real_add_le_mono1],simpset() addsimps [Bseq_iff2]));
   1.822 +qed "Bseq_iff3";
   1.823 +
   1.824 +val real_not_leE = CLAIM "~ m <= n ==> n < (m::real)";
   1.825 +
   1.826 +Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
   1.827 +by (res_inst_tac [("x","(abs(k) + abs(K)) + #1")] exI 1);
   1.828 +by (Auto_tac);
   1.829 +by (arith_tac 1);
   1.830 +by (case_tac "#0 <= f n" 1);
   1.831 +by (auto_tac (claset(),simpset() addsimps [abs_eqI1,
   1.832 +    real_not_leE RS abs_minus_eqI2]));
   1.833 +by (res_inst_tac [("j","abs K")] real_le_trans 1);
   1.834 +by (res_inst_tac [("j","abs k")] real_le_trans 3);
   1.835 +by (auto_tac (claset() addSIs [rename_numerals real_le_add_order] addDs 
   1.836 +    [real_le_trans],simpset() 
   1.837 +    addsimps [abs_ge_zero,rename_numerals real_zero_less_one,abs_eqI1]));
   1.838 +by (subgoal_tac "k < 0" 1);
   1.839 +by (rtac (real_not_leE RSN (2,real_le_less_trans)) 2);
   1.840 +by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2]));
   1.841 +qed "BseqI2";
   1.842 +
   1.843 +(*-------------------------------------------------------------------
   1.844 +   Equivalence between NS and standard definitions of Cauchy seqs
   1.845 + ------------------------------------------------------------------*)
   1.846 +(*-------------------------------
   1.847 +      Standard def => NS def
   1.848 + -------------------------------*)
   1.849 +Goal "!!x. Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \
   1.850 +\         ==> {n. M <= x n} : FreeUltrafilterNat";
   1.851 +by (auto_tac (claset(),simpset() addsimps 
   1.852 +     [HNatInfinite_FreeUltrafilterNat_iff]));
   1.853 +by (dres_inst_tac [("x","M")] spec 1);
   1.854 +by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1);
   1.855 +val lemmaCauchy1 = result();
   1.856 +
   1.857 +Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
   1.858 +\     {n. M <= xa n} Int {n. M <= x n} <= \
   1.859 +\     {n. abs (X (xa n) + - X (x n)) < u}";
   1.860 +by (Blast_tac 1);
   1.861 +val lemmaCauchy2 = result();
   1.862 +
   1.863 +Goalw [Cauchy_def,NSCauchy_def] 
   1.864 +      "Cauchy X ==> NSCauchy X";
   1.865 +by (Step_tac 1);
   1.866 +by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
   1.867 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   1.868 +by (rtac (inf_close_minus_iff RS iffD2) 1);
   1.869 +by (rtac (mem_infmal_iff RS iffD1) 1);
   1.870 +by (auto_tac (claset(),simpset() addsimps [starfunNat,
   1.871 +    hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
   1.872 +by (EVERY[rtac bexI 1, Auto_tac]);
   1.873 +by (dtac spec 1 THEN Auto_tac);
   1.874 +by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
   1.875 +by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
   1.876 +by (res_inst_tac [("x1","xa")] 
   1.877 +    (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
   1.878 +by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
   1.879 +by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
   1.880 +        FreeUltrafilterNat_Nat_set],simpset()));
   1.881 +qed "Cauchy_NSCauchy";
   1.882 +
   1.883 +(*-----------------------------------------------
   1.884 +     NS def => Standard def -- rather long but 
   1.885 +     straightforward proof in this case
   1.886 + ---------------------------------------------*)
   1.887 +Goalw [Cauchy_def,NSCauchy_def] 
   1.888 +      "NSCauchy X ==> Cauchy X";
   1.889 +by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
   1.890 +by (dtac choice 1 THEN auto_tac (claset(),simpset() 
   1.891 +         addsimps [all_conj_distrib]));
   1.892 +by (dtac choice 1 THEN step_tac (claset() addSDs 
   1.893 +         [all_conj_distrib RS iffD1]) 1);
   1.894 +by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
   1.895 +by (dtac bspec 1 THEN assume_tac 1);
   1.896 +by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 
   1.897 +    THEN auto_tac (claset(),simpset() addsimps [starfunNat]));
   1.898 +by (dtac (inf_close_minus_iff RS iffD1) 1);
   1.899 +by (dtac (mem_infmal_iff RS iffD2) 1);
   1.900 +by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
   1.901 +    hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
   1.902 +by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
   1.903 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   1.904 +by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
   1.905 +\         {n. abs (Y n) < e} <= \
   1.906 +\         {n. abs (X (f n) + - X (fa n)) < e}" RSN 
   1.907 +          (2,FreeUltrafilterNat_subset)) 1);
   1.908 +by (thin_tac "{n. abs (Y n) < e} : FreeUltrafilterNat" 1);
   1.909 +by (dtac FreeUltrafilterNat_all 1);
   1.910 +by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   1.911 +by (asm_full_simp_tac (simpset() addsimps 
   1.912 +    [CLAIM "{n. abs (X (f n) + - X (fa n)) < e} Int \
   1.913 +\         {M. ~ abs (X (f M) + - X (fa M)) < e} = {}",
   1.914 +     FreeUltrafilterNat_empty]) 1);
   1.915 +qed "NSCauchy_Cauchy";
   1.916 +
   1.917 +(*----- Equivalence -----*)
   1.918 +Goal "NSCauchy X = Cauchy X";
   1.919 +by (blast_tac (claset() addSIs[NSCauchy_Cauchy,
   1.920 +    Cauchy_NSCauchy]) 1);
   1.921 +qed "NSCauchy_Cauchy_iff";
   1.922 +
   1.923 +(*-------------------------------------------------------
   1.924 +  Cauchy sequence is bounded -- this is the standard 
   1.925 +  proof mechanization rather than the nonstandard proof 
   1.926 + -------------------------------------------------------*)
   1.927 +
   1.928 +(***-------------  VARIOUS LEMMAS --------------***)
   1.929 +Goal "!!X. ALL n. M <= n --> abs (X M + - X n) < (#1::real) \
   1.930 +\         ==>  ALL n. M <= n --> abs(X n) < #1 + abs(X M)";
   1.931 +by (Step_tac 1);
   1.932 +by (dtac spec 1 THEN Auto_tac);
   1.933 +by (arith_tac 1);
   1.934 +val lemmaCauchy = result();
   1.935 +
   1.936 +Goal "(n < Suc M) = (n <= M)";
   1.937 +by Auto_tac;
   1.938 +qed "less_Suc_cancel_iff";
   1.939 +
   1.940 +(* FIXME: Long. Maximal element in subsequence *)
   1.941 +Goal "EX m. m <= M & (ALL n. n <= M --> \
   1.942 +\         abs ((X::nat=> real) n) <= abs (X m))";
   1.943 +by (induct_tac "M" 1);
   1.944 +by (res_inst_tac [("x","0")] exI 1);
   1.945 +by (Asm_full_simp_tac 1);
   1.946 +by (Step_tac 1);
   1.947 +by (cut_inst_tac [("R1.0","abs (X (Suc n))"),("R2.0","abs(X m)")]
   1.948 +        real_linear 1);
   1.949 +by (Step_tac 1);
   1.950 +by (res_inst_tac [("x","m")] exI 1);
   1.951 +by (res_inst_tac [("x","m")] exI 2);
   1.952 +by (res_inst_tac [("x","Suc n")] exI 3);
   1.953 +by (ALLGOALS(Asm_full_simp_tac));
   1.954 +by (Step_tac 1);
   1.955 +by (ALLGOALS(eres_inst_tac [("m1","na")] 
   1.956 +    (le_imp_less_or_eq RS disjE)));
   1.957 +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
   1.958 +    [real_le_refl,less_Suc_cancel_iff,
   1.959 +     real_less_imp_le])));
   1.960 +by (blast_tac (claset() addIs [real_le_less_trans RS
   1.961 +    real_less_imp_le]) 1);
   1.962 +qed "SUP_rabs_subseq";
   1.963 +
   1.964 +(* lemmas to help proof - mostly trivial *)
   1.965 +Goal "[| ALL m::nat. m <= M --> P M m; \
   1.966 +\        ALL m. M <= m --> P M m |] \
   1.967 +\     ==> ALL m. P M m";
   1.968 +by (Step_tac 1);
   1.969 +by (REPEAT(dres_inst_tac [("x","m")] spec 1));
   1.970 +by (auto_tac (claset() addEs [less_asym],
   1.971 +    simpset() addsimps [le_def]));
   1.972 +val lemma_Nat_covered = result();
   1.973 +
   1.974 +Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a; \
   1.975 +\        a < b |] \
   1.976 +\     ==> ALL n. n <= M --> abs(X n) <= b";
   1.977 +by (blast_tac (claset() addIs [real_le_less_trans RS 
   1.978 +               real_less_imp_le]) 1);
   1.979 +val lemma_trans1 = result();
   1.980 +
   1.981 +Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
   1.982 +\        a < b |] \
   1.983 +\     ==> ALL n. M <= n --> abs(X n)<= b";
   1.984 +by (blast_tac (claset() addIs [real_less_trans RS 
   1.985 +               real_less_imp_le]) 1);
   1.986 +val lemma_trans2 = result();
   1.987 +
   1.988 +Goal "[| ALL n. n <= M --> abs (X n) <= a; \
   1.989 +\        a = b |] \
   1.990 +\     ==> ALL n. n <= M --> abs(X n) <= b";
   1.991 +by (Auto_tac);
   1.992 +val lemma_trans3 = result();
   1.993 +
   1.994 +Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
   1.995 +\             ==>  ALL n. M <= n --> abs (X n) <= a";
   1.996 +by (blast_tac (claset() addIs [real_less_imp_le]) 1);
   1.997 +val lemma_trans4 = result();
   1.998 +
   1.999 +(*---------------------------------------------------------- 
  1.1000 +   Trickier than expected --- proof is more involved than
  1.1001 +   outlines sketched by various authors would suggest
  1.1002 + ---------------------------------------------------------*)
  1.1003 +Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X";
  1.1004 +by (dres_inst_tac [("x","#1")] spec 1);
  1.1005 +by (etac (rename_numerals real_zero_less_one RSN (2,impE)) 1);
  1.1006 +by (Step_tac 1);
  1.1007 +by (dres_inst_tac [("x","M")] spec 1);
  1.1008 +by (Asm_full_simp_tac 1);
  1.1009 +by (dtac lemmaCauchy 1);
  1.1010 +by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
  1.1011 +by (Step_tac 1);
  1.1012 +by (cut_inst_tac [("R1.0","abs(X m)"),
  1.1013 +     ("R2.0","#1 + abs(X M)")] real_linear 1);
  1.1014 +by (Step_tac 1);
  1.1015 +by (dtac lemma_trans1 1 THEN assume_tac 1);
  1.1016 +by (dtac lemma_trans2 3 THEN assume_tac 3);
  1.1017 +by (dtac lemma_trans3 2 THEN assume_tac 2);
  1.1018 +by (dtac (abs_add_one_gt_zero RS real_less_trans) 3);
  1.1019 +by (dtac lemma_trans4 1);
  1.1020 +by (dtac lemma_trans4 2);
  1.1021 +by (res_inst_tac [("x","#1 + abs(X M)")] exI 1);
  1.1022 +by (res_inst_tac [("x","#1 + abs(X M)")] exI 2);
  1.1023 +by (res_inst_tac [("x","abs(X m)")] exI 3);
  1.1024 +by (auto_tac (claset() addSEs [lemma_Nat_covered],
  1.1025 +              simpset()));
  1.1026 +qed "Cauchy_Bseq";
  1.1027 +
  1.1028 +(*------------------------------------------------
  1.1029 +  Cauchy sequence is bounded -- NSformulation
  1.1030 + ------------------------------------------------*)
  1.1031 +Goal "NSCauchy X ==> NSBseq X";
  1.1032 +by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq,
  1.1033 +    Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1);
  1.1034 +qed "NSCauchy_NSBseq";
  1.1035 +
  1.1036 +
  1.1037 +(*-----------------------------------------------------------------
  1.1038 +          Equivalence of Cauchy criterion and convergence
  1.1039 +  
  1.1040 +  We will prove this using our NS formulation which provides a
  1.1041 +  much easier proof than using the standard definition. We do not 
  1.1042 +  need to use properties of subsequences such as boundedness, 
  1.1043 +  monotonicity etc... Compare with Harrison's corresponding proof
  1.1044 +  in HOL which is much longer and more complicated. Of course, we do
  1.1045 +  not have problems which he encountered with guessing the right 
  1.1046 +  instantiations for his 'espsilon-delta' proof(s) in this case
  1.1047 +  since the NS formulations do not involve existential quantifiers.
  1.1048 + -----------------------------------------------------------------*)
  1.1049 +Goalw [NSconvergent_def,NSLIMSEQ_def]
  1.1050 +      "NSCauchy X = NSconvergent X";
  1.1051 +by (Step_tac 1);
  1.1052 +by (forward_tac [NSCauchy_NSBseq] 1);
  1.1053 +by (auto_tac (claset() addIs [inf_close_trans2], 
  1.1054 +    simpset() addsimps 
  1.1055 +    [NSBseq_def,NSCauchy_def]));
  1.1056 +by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
  1.1057 +by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
  1.1058 +by (auto_tac (claset() addSDs [st_part_Ex],simpset() 
  1.1059 +              addsimps [SReal_iff]));
  1.1060 +by (blast_tac (claset() addIs [inf_close_trans3]) 1);
  1.1061 +qed "NSCauchy_NSconvergent_iff";
  1.1062 +
  1.1063 +(* Standard proof for free *)
  1.1064 +Goal "Cauchy X = convergent X";
  1.1065 +by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym,
  1.1066 +    convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1);
  1.1067 +qed "Cauchy_convergent_iff";
  1.1068 +
  1.1069 +(*-----------------------------------------------------------------
  1.1070 +     We can now try and derive a few properties of sequences
  1.1071 +     starting with the limit comparison property for sequences
  1.1072 + -----------------------------------------------------------------*)
  1.1073 +Goalw [NSLIMSEQ_def]
  1.1074 +       "!!f. [| f ----NS> l; g ----NS> m; \
  1.1075 +\                  EX N. ALL n. N <= n --> f(n) <= g(n) \
  1.1076 +\               |] ==> l <= m";
  1.1077 +by (Step_tac 1);
  1.1078 +by (dtac starfun_le_mono 1);
  1.1079 +by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
  1.1080 +by (dres_inst_tac [("x","whn")] spec 1);
  1.1081 +by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
  1.1082 +by (auto_tac (claset() addIs 
  1.1083 +    [hypreal_of_real_le_add_Infininitesimal_cancel2],simpset()));
  1.1084 +qed "NSLIMSEQ_le";
  1.1085 +
  1.1086 +(* standard version *)
  1.1087 +Goal "[| f ----> l; g ----> m; \
  1.1088 +\        EX N. ALL n. N <= n --> f(n) <= g(n) |] \
  1.1089 +\     ==> l <= m";
  1.1090 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1091 +    NSLIMSEQ_le]) 1);
  1.1092 +qed "LIMSEQ_le";
  1.1093 +
  1.1094 +(*---------------
  1.1095 +    Also...
  1.1096 + --------------*)
  1.1097 +Goal "[| X ----> r; ALL n. a <= X n |] ==> a <= r";
  1.1098 +by (rtac LIMSEQ_le 1);
  1.1099 +by (rtac LIMSEQ_const 1);
  1.1100 +by (Auto_tac);
  1.1101 +qed "LIMSEQ_le_const";
  1.1102 +
  1.1103 +Goal "[| X ----NS> r; ALL n. a <= X n |] ==> a <= r";
  1.1104 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1105 +    LIMSEQ_le_const]) 1);
  1.1106 +qed "NSLIMSEQ_le_const";
  1.1107 +
  1.1108 +Goal "[| X ----> r; ALL n. X n <= a |] ==> r <= a";
  1.1109 +by (rtac LIMSEQ_le 1);
  1.1110 +by (rtac LIMSEQ_const 2);
  1.1111 +by (Auto_tac);
  1.1112 +qed "LIMSEQ_le_const2";
  1.1113 +
  1.1114 +Goal "[| X ----NS> r; ALL n. X n <= a |] ==> r <= a";
  1.1115 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1116 +    LIMSEQ_le_const2]) 1);
  1.1117 +qed "NSLIMSEQ_le_const2";
  1.1118 +
  1.1119 +(*-----------------------------------------------------
  1.1120 +            Shift a convergent series by 1
  1.1121 +  We use the fact that Cauchyness and convergence
  1.1122 +  are equivalent and also that the successor of an
  1.1123 +  infinite hypernatural is also infinite.
  1.1124 + -----------------------------------------------------*)
  1.1125 +Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
  1.1126 +by (forward_tac [NSconvergentI RS 
  1.1127 +    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  1.1128 +by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
  1.1129 +    NSLIMSEQ_def,starfunNat_shift_one]));
  1.1130 +by (dtac bspec 1 THEN assume_tac 1);
  1.1131 +by (dtac bspec 1 THEN assume_tac 1);
  1.1132 +by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
  1.1133 +by (blast_tac (claset() addIs [inf_close_trans3]) 1);
  1.1134 +qed "NSLIMSEQ_Suc";
  1.1135 +
  1.1136 +(* standard version *)
  1.1137 +Goal "f ----> l ==> (%n. f(Suc n)) ----> l";
  1.1138 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1139 +    NSLIMSEQ_Suc]) 1);
  1.1140 +qed "LIMSEQ_Suc";
  1.1141 +
  1.1142 +Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
  1.1143 +by (forward_tac [NSconvergentI RS 
  1.1144 +    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
  1.1145 +by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
  1.1146 +    NSLIMSEQ_def,starfunNat_shift_one]));
  1.1147 +by (dtac bspec 1 THEN assume_tac 1);
  1.1148 +by (dtac bspec 1 THEN assume_tac 1);
  1.1149 +by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
  1.1150 +by (rotate_tac 2 1);
  1.1151 +by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3],
  1.1152 +    simpset()));
  1.1153 +qed "NSLIMSEQ_imp_Suc";
  1.1154 +
  1.1155 +Goal "(%n. f(Suc n)) ----> l ==> f ----> l";
  1.1156 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
  1.1157 +by (etac NSLIMSEQ_imp_Suc 1);
  1.1158 +qed "LIMSEQ_imp_Suc";
  1.1159 +
  1.1160 +Goal "(%n. f(Suc n) ----> l) = (f ----> l)";
  1.1161 +by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1);
  1.1162 +qed "LIMSEQ_Suc_iff";
  1.1163 +
  1.1164 +Goal "(%n. f(Suc n) ----NS> l) = (f ----NS> l)";
  1.1165 +by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1);
  1.1166 +qed "NSLIMSEQ_Suc_iff";
  1.1167 +
  1.1168 +(*-----------------------------------------------------
  1.1169 +       A sequence tends to zero iff its abs does
  1.1170 + ----------------------------------------------------*)
  1.1171 +(* we can prove this directly since proof is trivial *)
  1.1172 +Goalw [LIMSEQ_def] 
  1.1173 +      "((%n. abs(f n)) ----> #0) = (f ----> #0)";
  1.1174 +by (simp_tac (simpset() addsimps [abs_idempotent]) 1);
  1.1175 +qed "LIMSEQ_rabs_zero";
  1.1176 +
  1.1177 +(*-----------------------------------------------------*)
  1.1178 +(* We prove the NS version from the standard one       *)
  1.1179 +(* Actually pure NS proof seems more complicated       *)
  1.1180 +(* than the direct standard one above!                 *)
  1.1181 +(*-----------------------------------------------------*)
  1.1182 +
  1.1183 +Goal "((%n. abs(f n)) ----NS> #0) = (f ----NS> #0)";
  1.1184 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1185 +             LIMSEQ_rabs_zero]) 1);
  1.1186 +qed "NSLIMSEQ_rabs_zero";
  1.1187 +
  1.1188 +(*----------------------------------------
  1.1189 +    Also we have for a general limit 
  1.1190 +        (NS proof much easier)
  1.1191 + ---------------------------------------*)
  1.1192 +Goalw [NSLIMSEQ_def] 
  1.1193 +       "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
  1.1194 +by (auto_tac (claset() addIs [inf_close_hrabs],simpset() 
  1.1195 +    addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
  1.1196 +qed "NSLIMSEQ_imp_rabs";
  1.1197 +
  1.1198 +(* standard version *)
  1.1199 +Goal "f ----> l ==> (%n. abs(f n)) ----> abs(l)";
  1.1200 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1201 +    NSLIMSEQ_imp_rabs]) 1);
  1.1202 +qed "LIMSEQ_imp_rabs";
  1.1203 +
  1.1204 +(*-----------------------------------------------------
  1.1205 +       An unbounded sequence's inverse tends to 0
  1.1206 +  ----------------------------------------------------*)
  1.1207 +(* standard proof seems easier *)
  1.1208 +Goalw [LIMSEQ_def] 
  1.1209 +      "ALL y. EX N. ALL n. N <= n --> y < f(n) \
  1.1210 +\      ==> (%n. rinv(f n)) ----> #0";
  1.1211 +by (Step_tac 1 THEN Asm_full_simp_tac 1);
  1.1212 +by (dres_inst_tac [("x","rinv r")] spec 1 THEN Step_tac 1);
  1.1213 +by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
  1.1214 +by (dtac spec 1 THEN Auto_tac);
  1.1215 +by (forward_tac [rename_numerals real_rinv_gt_zero] 1);
  1.1216 +by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
  1.1217 +by (forw_inst_tac [("x","f n")] (rename_numerals real_rinv_gt_zero) 1);
  1.1218 +by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
  1.1219 +by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
  1.1220 +by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1],simpset()));
  1.1221 +qed "LIMSEQ_rinv_zero";
  1.1222 +
  1.1223 +Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
  1.1224 +\     ==> (%n. rinv(f n)) ----NS> #0";
  1.1225 +by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1226 +                  LIMSEQ_rinv_zero]) 1);
  1.1227 +qed "NSLIMSEQ_rinv_zero";
  1.1228 +
  1.1229 +(*--------------------------------------------------------------
  1.1230 +             Sequence  1/n --> 0 as n --> infinity 
  1.1231 + -------------------------------------------------------------*)
  1.1232 +Goal "(%n. rinv(real_of_posnat n)) ----> #0";
  1.1233 +by (rtac LIMSEQ_rinv_zero 1 THEN Step_tac 1);
  1.1234 +by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
  1.1235 +by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
  1.1236 +by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
  1.1237 +by (dtac (real_of_posnat_less_iff RS iffD2) 1);
  1.1238 +by (auto_tac (claset() addEs [real_less_trans],simpset()));
  1.1239 +qed "LIMSEQ_rinv_real_of_posnat";
  1.1240 +
  1.1241 +Goal "(%n. rinv(real_of_posnat n)) ----NS> #0";
  1.1242 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1243 +    LIMSEQ_rinv_real_of_posnat]) 1);
  1.1244 +qed "NSLIMSEQ_rinv_real_of_posnat";
  1.1245 +
  1.1246 +(*--------------------------------------------
  1.1247 +    Sequence  r + 1/n --> r as n --> infinity 
  1.1248 +    now easily proved
  1.1249 + --------------------------------------------*)
  1.1250 +Goal "(%n. r + rinv(real_of_posnat n)) ----> r";
  1.1251 +by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
  1.1252 +    MRS LIMSEQ_add] 1);
  1.1253 +by (Auto_tac);
  1.1254 +qed "LIMSEQ_rinv_real_of_posnat_add";
  1.1255 +
  1.1256 +Goal "(%n. r + rinv(real_of_posnat n)) ----NS> r";
  1.1257 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1258 +    LIMSEQ_rinv_real_of_posnat_add]) 1);
  1.1259 +qed "NSLIMSEQ_rinv_real_of_posnat_add";
  1.1260 +
  1.1261 +(*--------------
  1.1262 +    Also...
  1.1263 + --------------*)
  1.1264 +
  1.1265 +Goal "(%n. r + -rinv(real_of_posnat n)) ----> r";
  1.1266 +by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
  1.1267 +    MRS LIMSEQ_add_minus] 1);
  1.1268 +by (Auto_tac);
  1.1269 +qed "LIMSEQ_rinv_real_of_posnat_add_minus";
  1.1270 +
  1.1271 +Goal "(%n. r + -rinv(real_of_posnat n)) ----NS> r";
  1.1272 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1273 +    LIMSEQ_rinv_real_of_posnat_add_minus]) 1);
  1.1274 +qed "NSLIMSEQ_rinv_real_of_posnat_add_minus";
  1.1275 +
  1.1276 +Goal "(%n. r*( #1 + -rinv(real_of_posnat n))) ----> r";
  1.1277 +by (cut_inst_tac [("b","#1")] ([LIMSEQ_const,
  1.1278 +    LIMSEQ_rinv_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
  1.1279 +by (Auto_tac);
  1.1280 +qed "LIMSEQ_rinv_real_of_posnat_add_minus_mult";
  1.1281 +
  1.1282 +Goal "(%n. r*( #1 + -rinv(real_of_posnat n))) ----NS> r";
  1.1283 +by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
  1.1284 +    LIMSEQ_rinv_real_of_posnat_add_minus_mult]) 1);
  1.1285 +qed "NSLIMSEQ_rinv_real_of_posnat_add_minus_mult";
  1.1286 +
  1.1287 +(*---------------------------------------------------------------
  1.1288 +                          Real Powers
  1.1289 + --------------------------------------------------------------*)
  1.1290 +Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)";
  1.1291 +by (induct_tac "m" 1);
  1.1292 +by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const],
  1.1293 +    simpset()));
  1.1294 +qed_spec_mp "NSLIMSEQ_pow";
  1.1295 +
  1.1296 +Goal "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m";
  1.1297 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
  1.1298 +    NSLIMSEQ_pow]) 1);
  1.1299 +qed "LIMSEQ_pow";
  1.1300 +
  1.1301 +(*----------------------------------------------------------------
  1.1302 +               0 <= x < #1 ==> (x ^ n ----> 0)
  1.1303 +  Proof will use (NS) Cauchy equivalence for convergence and
  1.1304 +  also fact that bounded and monotonic sequence converges.  
  1.1305 + ---------------------------------------------------------------*)
  1.1306 +Goalw [Bseq_def] 
  1.1307 +      "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
  1.1308 +by (res_inst_tac [("x","#1")] exI 1);
  1.1309 +by (auto_tac (claset() addDs [conjI RS realpow_le2] 
  1.1310 +    addIs [real_less_imp_le],simpset() addsimps 
  1.1311 +    [real_zero_less_one,abs_eqI1,realpow_abs RS sym] ));
  1.1312 +qed "Bseq_realpow";
  1.1313 +
  1.1314 +Goal "[| #0 <= x; x < #1 |] ==> monoseq (%n. x ^ n)";
  1.1315 +by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1);
  1.1316 +qed "monoseq_realpow";
  1.1317 +
  1.1318 +Goal "[| #0 <= x; x < #1 |] ==> convergent (%n. x ^ n)";
  1.1319 +by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
  1.1320 +    Bseq_realpow,monoseq_realpow]) 1);
  1.1321 +qed "convergent_realpow";
  1.1322 +
  1.1323 +(* We now use NS criterion to bring proof of theorem through *)
  1.1324 +
  1.1325 +Goalw [NSLIMSEQ_def]
  1.1326 +     "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
  1.1327 +by (auto_tac (claset() addSDs [convergent_realpow],
  1.1328 +    simpset() addsimps [convergent_NSconvergent_iff]));
  1.1329 +by (forward_tac [NSconvergentD] 1);
  1.1330 +by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_def,
  1.1331 +    NSCauchy_NSconvergent_iff RS sym,NSCauchy_def,
  1.1332 +    starfunNat_pow]));
  1.1333 +by (forward_tac [HNatInfinite_add_one] 1);
  1.1334 +by (dtac bspec 1 THEN assume_tac 1);
  1.1335 +by (dtac bspec 1 THEN assume_tac 1);
  1.1336 +by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1);
  1.1337 +by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
  1.1338 +by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
  1.1339 +by (dtac inf_close_trans3 1 THEN assume_tac 1);
  1.1340 +by (auto_tac (claset() addSDs [rename_numerals (real_not_refl2 RS 
  1.1341 +    real_mult_eq_self_zero2)],simpset() addsimps 
  1.1342 +    [hypreal_of_real_mult RS sym]));
  1.1343 +qed "NSLIMSEQ_realpow_zero";
  1.1344 +
  1.1345 +(*---------------  standard version ---------------*)
  1.1346 +Goal "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----> #0";
  1.1347 +by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
  1.1348 +    LIMSEQ_NSLIMSEQ_iff]) 1);
  1.1349 +qed "LIMSEQ_realpow_zero";
  1.1350 +
  1.1351 +(*----------------------------------------------------------------
  1.1352 +               Limit of c^n for |c| < 1  
  1.1353 + ---------------------------------------------------------------*)
  1.1354 +Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) ----> #0";
  1.1355 +by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1);
  1.1356 +qed "LIMSEQ_rabs_realpow_zero";
  1.1357 +
  1.1358 +Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) ----NS> #0";
  1.1359 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero,
  1.1360 +    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
  1.1361 +qed "NSLIMSEQ_rabs_realpow_zero";
  1.1362 +
  1.1363 +Goal "abs(c) < #1 ==> (%n. c ^ n) ----> #0";
  1.1364 +by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
  1.1365 +by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
  1.1366 +         simpset() addsimps [realpow_abs RS sym]));
  1.1367 +qed "LIMSEQ_rabs_realpow_zero2";
  1.1368 +
  1.1369 +Goal "abs(c) < #1 ==> (%n. c ^ n) ----NS> #0";
  1.1370 +by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2,
  1.1371 +    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
  1.1372 +qed "NSLIMSEQ_rabs_realpow_zero2";
  1.1373 +
  1.1374 +(***---------------------------------------------------------------
  1.1375 +                 Hyperreals and Sequences
  1.1376 + ---------------------------------------------------------------***)
  1.1377 +(*** A bounded sequence is a finite hyperreal ***)
  1.1378 +Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite";
  1.1379 +by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
  1.1380 +       [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
  1.1381 +       simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
  1.1382 +        Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
  1.1383 +qed "NSBseq_HFinite_hypreal";
  1.1384 +
  1.1385 +(*** A sequence converging to zero defines an infinitesimal ***)
  1.1386 +Goalw [NSLIMSEQ_def] 
  1.1387 +      "X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal";
  1.1388 +by (dres_inst_tac [("x","whn")] bspec 1);
  1.1389 +by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
  1.1390 +by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def,
  1.1391 +    mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero]));
  1.1392 +qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
  1.1393 +
  1.1394 +(***---------------------------------------------------------------
  1.1395 +    Theorems proved by Harrison in HOL that we do not need 
  1.1396 +    in order to prove equivalence between Cauchy criterion 
  1.1397 +    and convergence:
  1.1398 + -- Show that every sequence contains a monotonic subsequence   
  1.1399 +Goal "EX f. subseq f & monoseq (%n. s (f n))";
  1.1400 + -- Show that a subsequence of a bounded sequence is bounded
  1.1401 +Goal "!!X. Bseq X ==> Bseq (%n. X (f n))";
  1.1402 + -- Show we can take subsequential terms arbitrarily far 
  1.1403 +    up a sequence       
  1.1404 +Goal "!!f. subseq f ==> n <= f(n)";
  1.1405 +Goal "!!f. subseq f ==> EX n. N1 <= n & N2 <= f(n)";
  1.1406 + ---------------------------------------------------------------***)