(*  Title       : SEQ.ML
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Standard and NS treatment of sequences
*) 

fun CLAIM_SIMP str thms =
               prove_goal thy str
               (fn prems => [cut_facts_tac prems 1,
                   auto_tac (claset(),simpset() addsimps thms)]);
fun CLAIM str = CLAIM_SIMP str [];

(*------------------------------------------------------*)
(* Example of an hypersequence (i.e. an extended        *)
(* standard sequence) whose term with an hypernatural   *)
(* suffix is an infinitesimal i.e. the whn'nth term of  *)
(* the hypersequence is a member of Infinitesimal       *)
(*------------------------------------------------------*)

Goalw [hypnat_omega_def] 
      "(*fNat* (%n::nat. rinv(real_of_posnat n))) whn : Infinitesimal";
by (auto_tac (claset(),simpset() addsimps 
    [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by (asm_full_simp_tac (simpset() addsimps [real_of_posnat_less_zero,
    real_rinv_gt_zero,rabs_eqI2,FreeUltrafilterNat_rinv_real_of_posnat]) 1);
qed "SEQ_Infinitesimal";

(*------------------------------------------------------*)
(*      Rules for LIMSEQ and NSLIMSEQ etc.              *)
(*------------------------------------------------------*)



(*** LIMSEQ ***)
Goalw [LIMSEQ_def] 
      "!!X. X ----> L ==> \
\      ALL r. 0r < r --> (EX no. ALL n. no <= n --> rabs(X n + -L) < r)";
by (Asm_simp_tac 1);
qed "LIMSEQD1";

Goalw [LIMSEQ_def] 
      "!!X. [| X ----> L; 0r < r|] ==> \
\      EX no. ALL n. no <= n --> rabs(X n + -L) < r";
by (Asm_simp_tac 1);
qed "LIMSEQD2";

Goalw [LIMSEQ_def] 
      "!!X. ALL r. 0r < r --> (EX no. ALL n. \
\      no <= n --> rabs(X n + -L) < r) ==> X ----> L";
by (Asm_simp_tac 1);
qed "LIMSEQI";

Goalw [LIMSEQ_def] 
      "!!X. (X ----> L) = \
\      (ALL r. 0r <r --> (EX no. ALL n. no <= n --> rabs(X n + -L) < r))";
by (Simp_tac 1);
qed "LIMSEQ_iff";

(*** NSLIMSEQ ***)
Goalw [NSLIMSEQ_def] 
      "!!X. X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
by (Asm_simp_tac 1);
qed "NSLIMSEQD1";

Goalw [NSLIMSEQ_def] 
      "!!X. [| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
by (Asm_simp_tac 1);
qed "NSLIMSEQD2";

Goalw [NSLIMSEQ_def] 
      "!!X. ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
by (Asm_simp_tac 1);
qed "NSLIMSEQI";

Goalw [NSLIMSEQ_def] 
      "!!X. (X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
by (Simp_tac 1);
qed "NSLIMSEQ_iff";

(*------------------------------------------------------*)
(*                 LIMSEQ ==> NSLIMSEQ                  *)
(*------------------------------------------------------*)

Goalw [LIMSEQ_def,NSLIMSEQ_def] 
      "!!X. X ----> L ==> X ----NS> L";
by (auto_tac (claset(),simpset() addsimps 
    [HNatInfinite_FreeUltrafilterNat_iff]));
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (rtac (inf_close_minus_iff RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
    mem_infmal_iff RS sym,hypreal_of_real_def,
    hypreal_minus,hypreal_add,
    Infinitesimal_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1);
by (dres_inst_tac [("x","no")] spec 1);
by (Fuf_tac 1);
by (blast_tac (claset() addDs [less_imp_le]) 1);
qed "LIMSEQ_NSLIMSEQ";

(*------------------------------------------------------*)
(*         NSLIMSEQ ==> LIMSEQ                          *)
(* proving NS def ==> Standard def is trickier as usual *)
(*------------------------------------------------------*)

(* the following sequence f(n) defines a hypernatural *)
(* lemmas etc. first *)
Goal "!!(f::nat=>nat). ALL n. n <= f n \
\          ==> {n. f n = 0} = {0} | {n. f n = 0} = {}";
by (Auto_tac);
by (dres_inst_tac [("x","xa")] spec 1);
by (dres_inst_tac [("x","x")] spec 2);
by (Auto_tac);
val lemma_NSLIMSEQ1 = result();

Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
val lemma_NSLIMSEQ2 = result();

Goal "!!(f::nat=>nat). ALL n. n <= f n \
\          ==> {n. f n = Suc u} <= {n. n <= Suc u}";
by (Auto_tac);
by (dres_inst_tac [("x","x")] spec 1);
by (Auto_tac);
val lemma_NSLIMSEQ3 = result();

Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
\         ==> finite {n. f n <= u}";
by (induct_tac "u" 1);
by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
    finite_nat_le_segment],simpset()));
by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
by (ALLGOALS(Asm_simp_tac));
qed "NSLIMSEQ_finite_set";

Goal "- {n. u < (f::nat=>nat) n} = {n. f n <= u}";
by (auto_tac (claset() addDs [less_le_trans],
    simpset() addsimps [le_def]));
qed "Compl_less_set";

(* the index set is in the free ultrafilter *)
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
\         ==> {n. u < f n} : FreeUltrafilterNat";
by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1);
by (rtac FreeUltrafilterNat_finite 1);
by (auto_tac (claset() addDs [NSLIMSEQ_finite_set],
    simpset() addsimps [Compl_less_set]));
qed "FreeUltrafilterNat_NSLIMSEQ";

(* thus, the sequence defines an infinite hypernatural! *)
Goal "!!f. ALL n. n <= f n \
\         ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite";
by (auto_tac (claset(),simpset() addsimps 
    [HNatInfinite_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, 
    Step_tac 1]);
by (etac FreeUltrafilterNat_NSLIMSEQ 1);
qed "HNatInfinite_NSLIMSEQ";

val lemmaLIM = CLAIM  "{n. X (f n) + - L = Y n} \
\              Int {n. rabs (Y n) < r} <= \
\              {n. rabs (X (f n) + - L) < r}";

Goal "{n. rabs (X (f n) + - L) < r} Int \
\         {n. r <= rabs (X (f n) + - L)} = {}";
by (auto_tac (claset() addDs [real_less_le_trans] 
    addIs [real_less_irrefl],simpset()));
val lemmaLIM2 = result();

Goal "!!f. [| 0r < r; ALL n. r <= rabs (X (f n) + - L); \
\          (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \
\          - hypreal_of_real  L @= 0hr |] ==> False";
by (auto_tac (claset(),simpset() addsimps [starfunNat,
    mem_infmal_iff RS sym,hypreal_of_real_def,
    hypreal_minus,hypreal_add,
    Infinitesimal_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
by (dtac FreeUltrafilterNat_all 1);
by (thin_tac "{n. rabs (Y n) < r} : FreeUltrafilterNat" 1);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
    FreeUltrafilterNat_empty]) 1);
val lemmaLIM3 = result();

(* finally we reach our goal*)
Goalw [LIMSEQ_def,NSLIMSEQ_def] 
      "!!X. X ----NS> L ==> X ----> L";
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
by (Step_tac 1);
(* skolemization step *)
by (dtac choice 1 THEN Step_tac 1);
by (dres_inst_tac [("x","Abs_hypnat(hypnatrel^^{f})")] bspec 1);
by (dtac (inf_close_minus_iff RS iffD1) 2);
by (fold_tac [real_le_def]);
by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
by (blast_tac (claset() addIs [lemmaLIM3]) 1);
qed "NSLIMSEQ_LIMSEQ";

(* Now the all important result is trivially proved! *)
Goal "(f ----> L) = (f ----NS> L)";
by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1);
qed "LIMSEQ_NSLIMSEQ_iff";

(*------------------------------------------------------*)
(*              Theorems about sequences                *)
(*------------------------------------------------------*)

Goalw [NSLIMSEQ_def] "(%n. k) ----NS> k";
by (Auto_tac);
qed "NSLIMSEQ_const";

Goalw [LIMSEQ_def] "(%n. k) ----> k";
by (Auto_tac);
qed "LIMSEQ_const";

Goalw [NSLIMSEQ_def]
      "!!X. [| X ----NS> a; Y ----NS> b |] \
\           ==> (%n. X n + Y n) ----NS> a + b";
by (auto_tac (claset() addIs [inf_close_add],
    simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
qed "NSLIMSEQ_add";

Goal "!!X. [| X ----> a; Y ----> b |] \
\           ==> (%n. X n + Y n) ----> a + b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_add]) 1);
qed "LIMSEQ_add";

Goalw [NSLIMSEQ_def]
      "!!X. [| X ----NS> a; Y ----NS> b |] \
\           ==> (%n. X n * Y n) ----NS> a * b";
by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close],
    simpset() addsimps [hypreal_of_real_mult]));
qed "NSLIMSEQ_mult";

Goal "!!X. [| X ----> a; Y ----> b |] \
\           ==> (%n. X n * Y n) ----> a * b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_mult]) 1);
qed "LIMSEQ_mult";

Goalw [NSLIMSEQ_def] 
      "!!X. X ----NS> a ==> (%n. -(X n)) ----NS> -a";
by (auto_tac (claset() addIs [inf_close_minus],
    simpset() addsimps [starfunNat_minus RS sym,
    hypreal_of_real_minus]));
qed "NSLIMSEQ_minus";

Goal "!!X. X ----> a ==> (%n. -(X n)) ----> -a";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_minus]) 1);
qed "LIMSEQ_minus";

Goal "(%n. -(X n)) ----> -a ==> X ----> a";
by (dtac LIMSEQ_minus 1);
by (Asm_full_simp_tac 1);
qed "LIMSEQ_minus_cancel";

Goal "(%n. -(X n)) ----NS> -a ==> X ----NS> a";
by (dtac NSLIMSEQ_minus 1);
by (Asm_full_simp_tac 1);
qed "NSLIMSEQ_minus_cancel";

Goal "!!X. [| X ----NS> a; Y ----NS> b |] \
\               ==> (%n. X n + -Y n) ----NS> a + -b";
by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
qed "NSLIMSEQ_add_minus";

Goal "!!X. [| X ----> a; Y ----> b |] \
\               ==> (%n. X n + -Y n) ----> a + -b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_add_minus]) 1);
qed "LIMSEQ_add_minus";

goalw SEQ.thy [real_diff_def] 
      "!!X. [| X ----> a; Y ----> b |] \
\               ==> (%n. X n - Y n) ----> a - b";
by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
qed "LIMSEQ_diff";

goalw SEQ.thy [real_diff_def] 
      "!!X. [| X ----NS> a; Y ----NS> b |] \
\               ==> (%n. X n - Y n) ----NS> a - b";
by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
qed "NSLIMSEQ_diff";

(*------------------------------------------------------*)
(* Proof is exactly same as that of NSLIM_rinv except   *)
(* for starfunNat_hrinv2 --- would not be the case if   *)
(* we had generalised net theorems for example. Not our *)
(* real concern though.                                 *)
(*------------------------------------------------------*)

Goalw [NSLIMSEQ_def] 
       "!!X. [| X ----NS> a; a ~= 0r |] \
\            ==> (%n. rinv(X n)) ----NS> rinv(a)";
by (Step_tac 1);
by (dtac bspec 1 THEN auto_tac (claset(),simpset() 
    addsimps [hypreal_of_real_not_zero_iff RS sym,
    hypreal_of_real_hrinv RS sym]));
by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 
    THEN assume_tac 1);
by (auto_tac (claset() addSEs [(starfunNat_hrinv2 RS subst),
    inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal],
    simpset()));
qed "NSLIMSEQ_rinv";

(*------ Standard version of theorem -------*)
Goal
       "!!X. [| X ----> a; a ~= 0r |] \
\            ==> (%n. rinv(X n)) ----> rinv(a)";
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_rinv,
    LIMSEQ_NSLIMSEQ_iff]) 1);
qed "LIMSEQ_rinv";

(* trivially proved *)
Goal
     "!!X. [| X ----NS> a; Y ----NS> b; b ~= 0r |] \
\          ==> (%n. (X n) * rinv(Y n)) ----NS> a*rinv(b)";
by (blast_tac (claset() addDs [NSLIMSEQ_rinv,NSLIMSEQ_mult]) 1);
qed "NSLIMSEQ_mult_rinv";

(* let's give a standard proof of theorem *)
Goal 
     "!!X. [| X ----> a; Y ----> b; b ~= 0r |] \
\          ==> (%n. (X n) * rinv(Y n)) ----> a*rinv(b)";
by (blast_tac (claset() addDs [LIMSEQ_rinv,LIMSEQ_mult]) 1);
qed "LIMSEQ_mult_rinv";

(*------------------------------------------------------*)
(*               Uniqueness of limit                    *)
(*------------------------------------------------------*)

Goalw [NSLIMSEQ_def] 
      "!!X. [| X ----NS> a; X ----NS> b |] \
\           ==> a = b";
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
by (auto_tac (claset() addDs [inf_close_trans3],simpset()));
qed "NSLIMSEQ_unique";

Goal "!!X. [| X ----> a; X ----> b |] \
\              ==> a = b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_unique]) 1);
qed "LIMSEQ_unique";

(*------------------------------------------------------*)
(*        theorems about nslim and lim                  *)
(*------------------------------------------------------*)

Goalw [lim_def] "!!X. X ----> L ==> lim X = L";
by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
qed "limI";

Goalw [nslim_def] "!!X. X ----NS> L ==> nslim X = L";
by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
qed "nslimI";

Goalw [lim_def,nslim_def] "lim X = nslim X";
by (asm_full_simp_tac (simpset() addsimps 
    [LIMSEQ_NSLIMSEQ_iff]) 1);
qed "lim_nslim_iff";

(*------------------------------------------------------*)
(*                   Convergence                        *)
(*------------------------------------------------------*)

Goalw [convergent_def]
      "!!f. convergent X ==> EX L. (X ----> L)";
by (assume_tac 1);
qed "convergentD";

Goalw [convergent_def]
      "!!f. (X ----> L) ==> convergent X";
by (Blast_tac 1);
qed "convergentI";

Goalw [NSconvergent_def]
      "!!f. NSconvergent X ==> EX L. (X ----NS> L)";
by (assume_tac 1);
qed "NSconvergentD";

Goalw [NSconvergent_def]
      "!!f. (X ----NS> L) ==> NSconvergent X";
by (Blast_tac 1);
qed "NSconvergentI";

Goalw [convergent_def,NSconvergent_def] 
      "convergent X = NSconvergent X";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
qed "convergent_NSconvergent_iff";

Goalw [NSconvergent_def,nslim_def] 
      "NSconvergent X = (X ----NS> nslim X)";
by (auto_tac (claset() addIs [selectI],simpset()));
qed "NSconvergent_NSLIMSEQ_iff";

Goalw [convergent_def,lim_def] 
      "convergent X = (X ----> lim X)";
by (auto_tac (claset() addIs [selectI],simpset()));
qed "convergent_LIMSEQ_iff";

(*------------------------------------------------------*)
(*  Subsequence (alternative definition) (e.g. Hoskins) *)
(*------------------------------------------------------*)

Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
by (auto_tac (claset() addSDs [less_eq_Suc_add],simpset()));
by (nat_ind_tac "k" 1);
by (auto_tac (claset() addIs [less_trans],simpset()));
qed "subseq_Suc_iff";

(*------------------------------------------------------*)
(*                   Monotonicity                       *)
(*------------------------------------------------------*)

Goalw [monoseq_def]
   "monoseq X = ((ALL n. X n <= X (Suc n)) \
\                | (ALL n. X (Suc n) <= X n))";
by (auto_tac (claset () addSDs [le_imp_less_or_eq],
    simpset() addsimps [real_le_refl]));
by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
    addSDs [less_eq_Suc_add],simpset()));
by (induct_tac "ka" 1);
by (auto_tac (claset() addIs [real_le_trans],simpset()));
by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
by (induct_tac "k" 1);
by (auto_tac (claset() addIs [real_le_trans],simpset()));
qed "monoseq_Suc";

Goalw [monoseq_def] 
       "!!X. ALL m n. m <= n --> X m <= X n ==> monoseq X";
by (Blast_tac 1);
qed "monoI1";

Goalw [monoseq_def] 
       "!!X. ALL m n. m <= n --> X n <= X m ==> monoseq X";
by (Blast_tac 1);
qed "monoI2";

Goal "!!X. ALL n. X n <= X (Suc n) ==> monoseq X";
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
qed "mono_SucI1";

Goal "!!X. ALL n. X (Suc n) <= X n ==> monoseq X";
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
qed "mono_SucI2";

(*------------------------------------------------------*)
(*                  Bounded Sequence                    *)
(*------------------------------------------------------*)

Goalw [Bseq_def] 
      "!!X. Bseq X ==> EX K. 0r < K & (ALL n. rabs(X n) <= K)";
by (assume_tac 1);
qed "BseqD";

Goalw [Bseq_def]
      "!!X. [| 0r < K; ALL n. rabs(X n) <= K |] \
\           ==> Bseq X";
by (Blast_tac 1);
qed "BseqI";

Goal "(EX K. 0r < K & (ALL n. rabs(X n) <= K)) = \
\         (EX N. ALL n. rabs(X n) <= real_of_posnat N)";
by (auto_tac (claset(),simpset() addsimps 
    [real_gt_zero_preal_Ex,real_of_posnat_less_zero]));
by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
by (blast_tac (claset() addIs [real_le_less_trans,
    real_less_imp_le]) 1);
by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def]));
qed "lemma_NBseq_def";

(* alternative definition for Bseq *)
Goalw [Bseq_def] 
      "Bseq X = (EX N. ALL n. rabs(X n) <= real_of_posnat N)";
by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
qed "Bseq_iff";

Goal "(EX K. 0r < K & (ALL n. rabs(X n) <= K)) = \
\         (EX N. ALL n. rabs(X n) < real_of_posnat N)";
by (auto_tac (claset(),simpset() addsimps 
    [real_gt_zero_preal_Ex,real_of_posnat_less_zero]));
by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1);
by (blast_tac (claset() addIs [real_less_trans,
    real_le_less_trans]) 1);
by (auto_tac (claset() addIs [real_less_imp_le],
    simpset() addsimps [real_of_posnat_def]));
qed "lemma_NBseq_def2";

(* yet another definition for Bseq *)
Goalw [Bseq_def] 
      "Bseq X = (EX N. ALL n. rabs(X n) < real_of_posnat N)";
by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
qed "Bseq_iff1a";

Goalw [NSBseq_def]
      "!!X. [| NSBseq X; N: HNatInfinite |] \
\           ==> (*fNat* X) N : HFinite";
by (Blast_tac 1);
qed "NSBseqD";

Goalw [NSBseq_def]
      "!!X. ALL N: HNatInfinite. (*fNat* X) N : HFinite \
\           ==> NSBseq X";
by (assume_tac 1);
qed "NSBseqI";

(*------------------------------------------------------*)
(*       Standard definition ==> NS definition          *)
(*------------------------------------------------------*)

(* a few lemmas *)
Goal "!!K. ALL n. rabs(X n) <= K ==> \
\              ALL n. rabs(X((f::nat=>nat) n)) <= K";
by (Auto_tac);
val lemma_Bseq = result();

Goal "{n. rabs (X (Xb n)) <= K} <= \
\         {n. rabs (X (Xb n)) < K + 1r}";
by (Step_tac 1);
by (rtac real_le_less_trans 1);
by (rtac real_self_less_add_one 2 THEN assume_tac 1);
val lemma_Bseq2 = result();

Goalw [Bseq_def,NSBseq_def] "!!X. Bseq X ==> NSBseq X";
by (Step_tac 1);
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,    
    HFinite_FreeUltrafilterNat_iff,
    HNatInfinite_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
by (dres_inst_tac [("f","Xb")] lemma_Bseq 1); 
by (res_inst_tac [("x","K+1r")] exI 1);
by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1);
by (blast_tac (claset() addIs [lemma_Bseq2 RSN 
    (2,FreeUltrafilterNat_subset)]) 1);
qed "Bseq_NSBseq";

(*------------------------------------------------------*)
(*       NS  definition ==> Standard definition         *)
(*------------------------------------------------------*)

(* similar to NSLIM proof in RealTopos *)

(*------------------------------------------------------*)
(* We need to get rid of the real variable and do so by *)
(* proving the following which relies on the Archimedean*) 
(* property of the reals. When we skolemize we then get *)
(* the required function f::nat=>nat  o/w we would be   *)
(* stuck with a skolem function f :: real=>nat which is *)
(* not what we want (read useless!)                     *)
(*------------------------------------------------------*)
 
Goal "!!X. ALL K. 0r < K --> (EX n. K < rabs (X n)) \
\          ==> ALL N. EX n. real_of_posnat  N < rabs (X n)";
by (Step_tac 1);
by (cut_inst_tac [("n","N")] real_of_posnat_less_zero 1);
by (Blast_tac 1);
val lemmaNSBseq = result();

Goal "!!X. ALL K. 0r < K --> (EX n. K < rabs (X n)) \
\         ==> EX f. ALL N. real_of_posnat  N < rabs (X (f N))";
by (dtac lemmaNSBseq 1);
by (dtac choice 1);
by (Blast_tac 1);
val lemmaNSBseq2 = result();

Goal "!!X. ALL N. real_of_posnat  N < rabs (X (f N)) \
\         ==>  Abs_hypreal(hyprel^^{X o f}) : HInfinite";
by (auto_tac (claset(),simpset() addsimps 
    [HInfinite_FreeUltrafilterNat_iff,o_def]));
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, 
    Step_tac 1]);
by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
by (blast_tac (claset() addDs [FreeUltrafilterNat_all,
    FreeUltrafilterNat_Int] addIs [real_less_trans,
    FreeUltrafilterNat_subset]) 1);
qed "real_seq_to_hypreal_HInfinite";

(*------------------------------------------------------*)
(* Now prove that we can get out an infinite            *)
(* hypernatural as well defined using the skolem        *)
(* function f::nat=>nat above                           *)
(*------------------------------------------------------*)

Goal "{n. f n <= Suc u & real_of_posnat  n < rabs (X (f n))} <= \
\         {n. f n <= u & real_of_posnat  n < rabs (X (f n))} \
\         Un {n. real_of_posnat n < rabs (X (Suc u))}";
by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le],
    simpset() addsimps [less_Suc_eq]));
val lemma_finite_NSBseq = result();

Goal "finite {n. f n <= (u::nat) &  real_of_posnat n < rabs(X(f n))}";
by (nat_ind_tac "u" 1);
by (rtac (CLAIM "{n. f n <= 0 & real_of_posnat n < rabs (X (f n))} <= \
\         {n. real_of_posnat n < rabs (X 0)}" 
          RS finite_subset) 1);
by (rtac finite_real_of_posnat_less_real 1);
by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
by (auto_tac (claset() addIs [finite_real_of_posnat_less_real],simpset()));
val lemma_finite_NSBseq2 = result();

Goal "!!X. ALL N. real_of_posnat  N < rabs (X (f N)) \
\              ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite";
by (auto_tac (claset(),simpset() addsimps 
    [HNatInfinite_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, 
    Step_tac 1]);
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
by (asm_full_simp_tac (simpset() addsimps 
   [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
\   = {n. f n <= u}" [le_def]]) 1);
by (dtac FreeUltrafilterNat_all 1);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (auto_tac (claset(),simpset() addsimps 
    [CLAIM "({n. f n <= u} Int {n. real_of_posnat n < rabs(X(f n))}) = \
\          {n. f n <= (u::nat) &  real_of_posnat n < rabs(X(f n))}",
     lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
qed "HNatInfinite_skolem_f";

Goalw [Bseq_def,NSBseq_def] 
      "!!X. NSBseq X ==> Bseq X";
by (rtac ccontr 1);
by (auto_tac (claset(),simpset() addsimps [real_le_def]));
by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
    o_def,HFinite_HInfinite_iff]));
qed "NSBseq_Bseq";

(*------------------------------------------------------*)
(* Equivalence of nonstandard and standard definitions  *)
(* for a bounded sequence                               *)
(*------------------------------------------------------*)

Goal "(Bseq X) = (NSBseq X)";
by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1);
qed "Bseq_NSBseq_iff";

(*------------------------------------------------------*)
(*      A convergent sequence is bounded                *)
(* Boundedness as a necessary condition for convergence *)
(*------------------------------------------------------*)

(* easier --- nonstandard version - no existential as usual *)
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
          "!!X. NSconvergent X ==> NSBseq X";
by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
               (inf_close_sym RSN (2,inf_close_HFinite))]) 1);
qed "NSconvergent_NSBseq";

(* standard version - easily now proved using *)
(* equivalence of NS and standard definitions *)
Goal "!!X. convergent X ==> Bseq X";
by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
    convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
qed "convergent_Bseq";

(*------------------------------------------------------*)
(*   Results about Ubs and Lubs of bounded sequences    *)
(*------------------------------------------------------*)
Goalw [Bseq_def]
  "!!(X::nat=>real). Bseq X ==> \
\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
by (auto_tac (claset() addIs [isUbI,setleI],
    simpset() addsimps [rabs_le_interval_iff]));
qed "Bseq_isUb";

(*------------------------------------------------------*)
(*   Use completeness of reals (supremum property)      *)
(*   to show that any bounded sequence has a lub        *)
(*------------------------------------------------------*)

Goal "!!(X::nat=>real). Bseq X ==> \
\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
by (blast_tac (claset() addIs [reals_complete,
    Bseq_isUb]) 1);
qed "Bseq_isLub";

(* nonstandard version of premise will be *)
(* handy when we work in NS universe      *)
Goal   "!!X. NSBseq X ==> \
\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
by (asm_full_simp_tac (simpset() addsimps 
    [Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
qed "NSBseq_isUb";

Goal
  "!!X. NSBseq X ==> \
\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
by (asm_full_simp_tac (simpset() addsimps 
    [Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
qed "NSBseq_isLub";

(*------------------------------------------------------*)
(*      Bounded and monotonic sequence converges        *)      
(*------------------------------------------------------*)

(* lemmas *)
Goal 
     "!!(X::nat=>real). [| ALL m n. m <= n -->  X m <= X n; \
\                 isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \
\              |] ==> ALL n. ma <= n --> X n = X ma";
by (Step_tac 1);
by (dres_inst_tac [("y","X n")] isLubD2 1);
by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym])));
val lemma_converg1 = result();


(*------------------------------------------------------*)
(* The best of both world: Easier to prove this result  *)
(* as a standard theorem and then use equivalence to    *)
(* "transfer" it into the equivalent nonstandard form   *)
(* if needed!                                           *)
(*------------------------------------------------------*)

Goalw [LIMSEQ_def] 
         "!!X. ALL n. m <= n --> X n = X m \
\         ==> EX L. (X ----> L)";  
by (res_inst_tac [("x","X m")] exI 1);
by (Step_tac 1);
by (res_inst_tac [("x","m")] exI 1);
by (Step_tac 1);
by (dtac spec 1 THEN etac impE 1);
by (Auto_tac);
qed "Bmonoseq_LIMSEQ";

(* Now same theorem in terms of NS limit *)
Goal "!!X. ALL n. m <= n --> X n = X m \
\         ==> EX L. (X ----NS> L)";  
by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
    simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
qed "Bmonoseq_NSLIMSEQ";

(* a few more lemmas *)
Goal "!!(X::nat=>real). \
\              [| ALL m. X m ~= U; \
\                 isLub UNIV {x. EX n. X n = x} U \
\              |] ==> ALL m. X m < U";
by (Step_tac 1);
by (dres_inst_tac [("y","X m")] isLubD2 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
              simpset()));
val lemma_converg2 = result();

Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
\         isUb UNIV {x. EX n. X n = x} U";
by (rtac (setleI RS isUbI) 1);
by (Auto_tac);
val lemma_converg3 = result();

Goal "!!(X::nat=> real). \
\              [| ALL m. X m ~= U; \
\                 isLub UNIV {x. EX n. X n = x} U; \
\                 0r < T; \
\                 U + - T < U \
\              |] ==> EX m. U + -T < X m & X m < U";
by (dtac lemma_converg2 1 THEN assume_tac 1);
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
by (fold_tac [real_le_def]);
by (dtac lemma_converg3 1);
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [real_less_le_trans],
    simpset() addsimps [real_minus_zero_le_iff]));
val lemma_converg4 = result();

(* yet another (boring) lemma *)
Goal "!!X. [| U + -R < U; X < (U::real) |] \
\              ==> X + -U < R";
by (Simp_tac 1);
val blemma = result();

Goal "!!(U::real). U + -R < X ==> -R < X + -U";
by (Simp_tac 1);
val blemma2 = result();

(*------------------------------------------------------*)
(* A standard proof of the theorem for monotone         *) 
(* increasing sequence                                  *)
(*------------------------------------------------------*)

Goalw [convergent_def] 
     "!!X. [| Bseq X; ALL m n. m <= n --> X m <= X n |] \
\                ==> convergent X";
by (forward_tac [Bseq_isLub] 1);
by (Step_tac 1);
by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
by (blast_tac (claset() addDs [lemma_converg1,
    Bmonoseq_LIMSEQ]) 1);
(* second case *)
by (res_inst_tac [("x","U")] exI 1);
by (rtac LIMSEQI 1 THEN Step_tac 1);
by (forw_inst_tac [("u","U")] real_add_minus_positive_less_self 1);
by (forward_tac [lemma_converg2] 1 THEN assume_tac 1);
by (dtac lemma_converg4 1 THEN Auto_tac);
by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
by (rotate_tac 5 1 THEN dres_inst_tac [("x","n")] spec 1);
by (dtac real_less_le_trans 1 THEN assume_tac 1);
by (auto_tac (claset() addIs [blemma,blemma2],
    simpset() addsimps [rabs_interval_iff]));
qed "Bseq_mono_convergent";

(* NS version of theorem *)
Goalw [convergent_def] 
     "!!X. [| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
\                ==> NSconvergent X";
by (auto_tac (claset() addIs [Bseq_mono_convergent], 
    simpset() addsimps [convergent_NSconvergent_iff RS sym,
    Bseq_NSBseq_iff RS sym]));
qed "NSBseq_mono_NSconvergent";

Goalw [convergent_def] 
      "!!X. (convergent X) = (convergent (%n. -(X n)))";
by (auto_tac (claset() addDs [LIMSEQ_minus],simpset()));
by (dtac LIMSEQ_minus 1 THEN Auto_tac);
qed "convergent_minus_iff";

Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
by (asm_full_simp_tac (simpset() addsimps [rabs_minus_cancel]) 1);
qed "Bseq_minus_iff";

(*-------------------------*)
(* main mono theorem       *)
(*-------------------------*)
Goalw [monoseq_def] 
      "!!X. [| Bseq X; monoseq X |] ==> convergent X";
by (Step_tac 1);
by (rtac (convergent_minus_iff RS ssubst) 2);
by (dtac (Bseq_minus_iff RS ssubst) 2);
by (auto_tac (claset() addSIs [Bseq_mono_convergent],simpset()));
qed "Bseq_monoseq_convergent";

(*------------------------------------------------------*)
(*   A few more equivalence theorems for boundedness    *)
(*------------------------------------------------------*)

context RealAbs.thy;

Goal "rabs(x) <= rabs(x + -y) + rabs(y)";
by (res_inst_tac [("j","rabs(x + -y + y)")] real_le_trans 1);
by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
              rabs_triangle_ineq]) 1);
qed "rabs_triangle_ineq_minus_cancel";

context thy;

(***--- alternative formulation for boundedness---***)
Goalw [Bseq_def] 
   "Bseq X = (EX k x. 0r < k & (ALL n. rabs(X(n) + -x) <= k))";
by (Step_tac 1);
by (res_inst_tac [("x","K")] exI 1);
by (res_inst_tac [("x","0r")] exI 1);
by (Auto_tac);
by (res_inst_tac [("x","k + rabs(x)")] exI 1);
by (Step_tac 1);
by (res_inst_tac [("j","rabs(X n + -x) + rabs x")] 
    real_le_trans 2);
by (rtac rabs_triangle_ineq_minus_cancel 2);
by (rtac real_add_le_mono1 2);
by (etac rabs_add_pos_gt_zero 1);
by (Blast_tac 1);
qed "Bseq_iff2";

(***--- alternative formulation for boundedness ---***)
Goal 
      "Bseq X = (EX k N. 0r < k & (ALL n. \
\                        rabs(X(n) + -X(N)) <= k))";
by (Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","K + rabs(X N)")] exI 1);
by (Auto_tac);
by (etac rabs_add_pos_gt_zero 1);
by (res_inst_tac [("x","N")] exI 1);
by (Step_tac 1);
by (res_inst_tac [("j","rabs(X n) + rabs (X N)")] 
    real_le_trans 1);
by (auto_tac (claset() addIs [rabs_triangle_minus_ineq,
    real_add_le_mono1],simpset() addsimps [Bseq_iff2]));
qed "Bseq_iff3";

Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
by (res_inst_tac [("x","(rabs(k) + rabs(K)) + 1r")] exI 1);
by (Auto_tac);
by (res_inst_tac [("j","rabs k + rabs K")] real_le_less_trans 1);
by (auto_tac (claset() addSIs [real_le_add_order],simpset() 
    addsimps [rabs_ge_zero,real_zero_less_one]));
by (case_tac "0r <= f n" 1);
by (auto_tac (claset(),simpset() addsimps [rabs_eqI1,
     rabs_minus_eqI2]));
by (res_inst_tac [("j","rabs K")] real_le_trans 1);
by (res_inst_tac [("j","rabs k")] real_le_trans 3);
by (auto_tac (claset() addSIs [real_le_add_order] addDs 
    [real_le_trans],simpset() 
    addsimps [rabs_ge_zero,real_zero_less_one,rabs_eqI1]));
by (subgoal_tac "k < 0r" 1);
by (rtac (CLAIM "~ x <= y ==> y < (x::real)" 
    RSN (2,real_le_less_trans)) 2);
by (auto_tac (claset(),simpset() addsimps [rabs_minus_eqI2]));
qed "BseqI2";


(*-------------------------------------------------------------*)
(*   Equivalence between NS and standard definitions           *)
(*   of Cauchy seqs  1.  Standard def => NS def                *)
(*-------------------------------------------------------------*)

Goal "!!x. Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \
\         ==> {n. M <= x n} : FreeUltrafilterNat";
by (auto_tac (claset(),simpset() addsimps 
     [HNatInfinite_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","M")] spec 1);
by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1);
val lemmaCauchy1 = result();

Goal "{n. ALL m n. M <= m & M <= n --> rabs (X m + - X n) < u} Int \
\     {n. M <= xa n} Int {n. M <= x n} <= \
\     {n. rabs (X (xa n) + - X (x n)) < u}";
by (Blast_tac 1);
val lemmaCauchy2 = result();

Goalw [Cauchy_def,NSCauchy_def] 
      "!!X. Cauchy X ==> NSCauchy X";
by (Step_tac 1);
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (rtac (inf_close_minus_iff RS iffD2) 1);
by (rtac (mem_infmal_iff RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [starfunNat,
    hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, Auto_tac]);
by (dtac spec 1 THEN Auto_tac);
by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
by (res_inst_tac [("x1","xa")] 
    (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
        FreeUltrafilterNat_Nat_set],simpset()));
qed "Cauchy_NSCauchy";

(*-----------------------------------------------*)
(*     NS def => Standard def -- rather long but *) 
(*     straightforward proof in this case        *)
(*-----------------------------------------------*)

Goalw [Cauchy_def,NSCauchy_def] 
      "!!X. NSCauchy X ==> Cauchy X";
by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
by (dtac choice 1 THEN auto_tac (claset(),simpset() 
         addsimps [all_conj_distrib]));
by (dtac choice 1 THEN step_tac (claset() addSDs 
         [all_conj_distrib RS iffD1]) 1);
by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
by (dtac bspec 1 THEN assume_tac 1);
by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 
    THEN auto_tac (claset(),simpset() addsimps [starfunNat]));
by (dtac (inf_close_minus_iff RS iffD1) 1);
by (dtac (mem_infmal_iff RS iffD2) 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
    hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
\         {n. rabs (Y n) < e} <= \
\         {n. rabs (X (f n) + - X (fa n)) < e}" RSN 
          (2,FreeUltrafilterNat_subset)) 1);
by (thin_tac "{n. rabs (Y n) < e} : FreeUltrafilterNat" 1);
by (dtac FreeUltrafilterNat_all 1);
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps 
    [CLAIM "{n. rabs (X (f n) + - X (fa n)) < e} Int \
\         {M. ~ rabs (X (f M) + - X (fa M)) < e} = {}",
     FreeUltrafilterNat_empty]) 1);
qed "NSCauchy_Cauchy";

(*----- Equivalence -----*)
Goal "NSCauchy X = Cauchy X";
by (blast_tac (claset() addSIs[NSCauchy_Cauchy,
    Cauchy_NSCauchy]) 1);
qed "NSCauchy_Cauchy_iff";

(*------------------------------------------------------*)
(*  Cauchy sequence is bounded -- Standard formulation  *)
(*------------------------------------------------------*)

(***----------------  VARIOUS LEMMAS -----------------***)
Goal "!!X. ALL n. M <= n --> rabs (X M + - X n) < 1r \
\         ==>  ALL n. M <= n --> rabs(X n) < 1r + rabs(X M)";
by (Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
by (res_inst_tac [("j","rabs(X n + -X M) + rabs (X M)")] 
    real_le_less_trans 1);
by (rtac rabs_triangle_ineq_minus_cancel 1);
by (rtac real_add_less_mono1 1);
by (asm_full_simp_tac (simpset() addsimps 
    [rabs_minus_add_cancel]) 1);
val lemmaCauchy = result();

Goal "(n < Suc M) = (n <= M)";
by (auto_tac (claset() addIs [less_imp_le]
    addDs [le_imp_less_or_eq],
    simpset() addsimps [less_Suc_eq]));
qed "less_Suc_cancel_iff";

(* Maximal element in subsequence *)
Goal "EX m. m <= M & (ALL n. n <= M --> \
\         rabs ((X::nat=> real) n) <= rabs (X m))";
by (nat_ind_tac "M" 1);
by (res_inst_tac [("x","0")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [real_le_refl]) 1);
by (Step_tac 1);
by (cut_inst_tac [("R1.0","rabs (X (Suc M))"),("R2.0","rabs(X m)")]
        real_linear 1);
by (Step_tac 1);
by (res_inst_tac [("x","m")] exI 1);
by (res_inst_tac [("x","m")] exI 2);
by (res_inst_tac [("x","Suc M")] exI 3);
by (ALLGOALS(Asm_full_simp_tac));
by (Step_tac 1);
by (ALLGOALS(eres_inst_tac [("m1","n")] 
    (le_imp_less_or_eq RS disjE)));
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
    [real_le_refl,less_Suc_cancel_iff,
     real_less_imp_le])));
by (blast_tac (claset() addIs [real_le_less_trans RS
    real_less_imp_le]) 1);
qed "SUP_rabs_subseq";

(* lemmas to help proof - mostly trivial *)
Goal "!!M. [| ALL m::nat. m <= M --> P M m; \
\                 ALL m. M <= m --> P M m\
\              |] ==> ALL m. P M m";
by (Step_tac 1);
by (REPEAT(dres_inst_tac [("x","m")] spec 1));
by (auto_tac (claset() addEs [less_asym],
    simpset() addsimps [le_def]));
val lemma_Nat_covered = result();

Goal "!!M X::nat=>real. \
\              [| ALL n. n <= M --> rabs (X n) <= a; \
\                    a < b \
\              |] ==> ALL n. n <= M --> rabs(X n) <= b";
by (blast_tac (claset() addIs [real_le_less_trans RS 
               real_less_imp_le]) 1);
val lemma_trans1 = result();

Goal "!!M X::nat=>real. \
\              [| ALL n. M <= n --> rabs (X n) < a; \
\                 a < b \
\              |] ==> ALL n. M <= n --> rabs(X n)<= b";
by (blast_tac (claset() addIs [real_less_trans RS 
               real_less_imp_le]) 1);
val lemma_trans2 = result();

Goal "!!M X::nat=>real. [| ALL n. n <= M --> rabs (X n) <= a; \
\                 a = b \
\              |] ==> ALL n. n <= M --> rabs(X n) <= b";
by (Auto_tac);
val lemma_trans3 = result();

Goal "!!M X::nat=>real. \
\             ALL n. M <= n --> rabs (X n) < a \
\             ==>  ALL n. M <= n --> rabs (X n) <= a";
by (blast_tac (claset() addIs [real_less_imp_le]) 1);
val lemma_trans4 = result();

(*----------------------------------------------------------*)
(*   Standard Proof:                                        *)
(*   Trickier than expected --- proof is more involved than *)
(*   outlines sketched by various authors would suggest     *)
(* ---------------------------------------------------------*)

Goalw [Cauchy_def,Bseq_def] "!!X. Cauchy X ==> Bseq X";
by (dres_inst_tac [("x","1r")] spec 1);
by (etac (real_zero_less_one RSN (2,impE)) 1);
by (Step_tac 1);
by (dres_inst_tac [("x","M")] spec 1);
by (Asm_full_simp_tac 1);
by (dtac lemmaCauchy 1);
by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
by (Step_tac 1);
by (cut_inst_tac [("R1.0","rabs(X m)"),
     ("R2.0","1r + rabs(X M)")] real_linear 1);
by (Step_tac 1);
by (dtac lemma_trans1 1 THEN assume_tac 1);
by (dtac lemma_trans2 3 THEN assume_tac 3);
by (dtac lemma_trans3 2 THEN assume_tac 2);
by (dtac (rabs_add_one_gt_zero RS real_less_trans) 3);
by (dtac lemma_trans4 1);
by (dtac lemma_trans4 2);
by (res_inst_tac [("x","1r + rabs(X M)")] exI 1);
by (res_inst_tac [("x","1r + rabs(X M)")] exI 2);
by (res_inst_tac [("x","rabs(X m)")] exI 3);
by (auto_tac (claset() addSEs [lemma_Nat_covered],
              simpset()));
qed "Cauchy_Bseq";

(*-------------------------------------------------*)
(*  Cauchy sequence is bounded -- NSformulation    *)
(* ------------------------------------------------*)
Goal "!!X. NSCauchy X ==> NSBseq X";
by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq,
    Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1);
qed "NSCauchy_NSBseq";


(*-----------------------------------------------------------------
          Equivalence of Cauchy criterion and convergence
  
  We will prove this using our NS formulation which provides a
  much easier proof than using the standard definition. We do not 
  need to use properties of subsequences such as boundedness, 
  monotonicity etc... Compare with Harrison's corresponding proof
  in HOL which is much longer and more complicated. Of course, we do
  not have problems which he encountered with guessing the right 
  instantiations for his 'espsilon-delta' proof(s) in this case
  since the NS formulations do not involve existentials.
 -----------------------------------------------------------------*)

Goalw [NSconvergent_def,NSLIMSEQ_def]
      "NSCauchy X = NSconvergent X";
by (Step_tac 1);
by (forward_tac [NSCauchy_NSBseq] 1);
by (auto_tac (claset() addIs [inf_close_trans2], 
    simpset() addsimps 
    [NSBseq_def,NSCauchy_def]));
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
by (auto_tac (claset() addSDs [st_part_Ex],simpset() 
              addsimps [SReal_iff]));
by (blast_tac (claset() addIs [inf_close_trans3]) 1);
qed "NSCauchy_NSconvergent_iff";

(* Standard proof for free *)
Goal "Cauchy X = convergent X";
by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym,
    convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1);
qed "Cauchy_convergent_iff";

(*------------------------------------------------------------*)
(* We can now try and derive a few properties of sequences    *)
(* starting with the limit comparison property for sequences  *)
(* -----------------------------------------------------------*)

Goalw [NSLIMSEQ_def]
       "!!f. [| f ----NS> l; g ----NS> m; \
\                  EX N. ALL n. N <= n --> f(n) <= g(n) \
\               |] ==> l <= m";
by (Step_tac 1);
by (dtac starfun_le_mono 1);
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
by (dres_inst_tac [("x","whn")] spec 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
by (auto_tac (claset() addIs 
    [hypreal_of_real_le_add_Infininitesimal_cancel2],simpset()));
qed "NSLIMSEQ_le";

(* standard version *)
Goal "!!f. [| f ----> l; g ----> m; \
\                 EX N. ALL n. N <= n --> f(n) <= g(n) \
\              |] ==> l <= m";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_le]) 1);
qed "LIMSEQ_le";

(*---------------*)
(*    Also...    *)
(* --------------*)

Goal "!!X. [| X ----> r; ALL n. a <= X n |] ==> a <= r";
by (rtac LIMSEQ_le 1);
by (rtac LIMSEQ_const 1);
by (Auto_tac);
qed "LIMSEQ_le_const";

Goal "!!X. [| X ----NS> r; ALL n. a <= X n |] ==> a <= r";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    LIMSEQ_le_const]) 1);
qed "NSLIMSEQ_le_const";

Goal "!!X. [| X ----> r; ALL n. X n <= a |] ==> r <= a";
by (rtac LIMSEQ_le 1);
by (rtac LIMSEQ_const 2);
by (Auto_tac);
qed "LIMSEQ_le_const2";

Goal "!!X. [| X ----NS> r; ALL n. X n <= a |] ==> r <= a";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    LIMSEQ_le_const2]) 1);
qed "NSLIMSEQ_le_const2";

(*-----------------------------------------------------*)
(*  Shift a convergent series by 1:                    *)
(*  We use the fact that Cauchyness and convergence    *)
(*  are equivalent and also that the successor of an   *)
(*  infinite hypernatural is also infinite.            *)
(* ----------------------------------------------------*)

Goal "!!f. f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
by (forward_tac [NSconvergentI RS 
    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
    NSLIMSEQ_def,starfunNat_shift_one]));
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
by (blast_tac (claset() addIs [inf_close_trans3]) 1);
qed "NSLIMSEQ_Suc";

(* standard version *)
Goal "!!f. f ----> l ==> (%n. f(Suc n)) ----> l";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_Suc]) 1);
qed "LIMSEQ_Suc";

goal SEQ.thy "!!f. (%n. f(Suc n)) ----NS> l ==> f ----NS> l";
by (forward_tac [NSconvergentI RS 
    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
by (auto_tac (claset(),simpset() addsimps [NSCauchy_def,
    NSLIMSEQ_def,starfunNat_shift_one]));
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
by (rotate_tac 2 1);
by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3],
    simpset()));
qed "NSLIMSEQ_imp_Suc";

goal SEQ.thy "!!f. (%n. f(Suc n)) ----> l ==> f ----> l";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
by (etac NSLIMSEQ_imp_Suc 1);
qed "LIMSEQ_imp_Suc";

goal SEQ.thy "(%n. f(Suc n) ----> l) = (f ----> l)";
by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1);
qed "LIMSEQ_Suc_iff";

goal SEQ.thy "(%n. f(Suc n) ----NS> l) = (f ----NS> l)";
by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1);
qed "NSLIMSEQ_Suc_iff";

(*------------------------------------------------------*)
(*       A sequence tends to zero iff its abs does      *)
(*  we can prove this directly since proof is trivial   *)
(*------------------------------------------------------*)

Goalw [LIMSEQ_def] 
      "!!f. ((%n. rabs(f n)) ----> 0r) = (f ----> 0r)";
by (simp_tac (simpset() addsimps [rabs_idempotent]) 1);
qed "LIMSEQ_rabs_zero";

(*------------------------------------------------------*)
(* We prove the NS version from the standard one        *)
(* Actually pure NS proof seems more complicated        *)
(* than the direct standard one above!                  *)
(*------------------------------------------------------*)

Goal "!!f. ((%n. rabs(f n)) ----NS> 0r) = (f ----NS> 0r)";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
             LIMSEQ_rabs_zero]) 1);
qed "NSLIMSEQ_rabs_zero";

(*------------------------------------------------------*)
(*    Also we have for a general limit                  *)
(*        (NS proof much easier)                        *)
(*------------------------------------------------------*)

Goalw [NSLIMSEQ_def] 
       "!!f. f ----NS> l ==> (%n. rabs(f n)) ----NS> rabs(l)";
by (auto_tac (claset() addIs [inf_close_hrabs],simpset() 
    addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
qed "NSLIMSEQ_imp_rabs";

(* standard version *)
Goal "!!f. f ----> l ==> (%n. rabs(f n)) ----> rabs(l)";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_imp_rabs]) 1);
qed "LIMSEQ_imp_rabs";

(*------------------------------------------------------*)
(*    An unbounded sequence's inverse tends to 0r       *)
(*------------------------------------------------------*)

Goalw [LIMSEQ_def] 
          "!!f. ALL y. EX N. ALL n. N <= n --> y < f(n) \
\          ==> (%n. rinv(f n)) ----> 0r";
by (Step_tac 1 THEN Asm_full_simp_tac 1);
by (dres_inst_tac [("x","rinv r")] spec 1 THEN Step_tac 1);
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
by (forward_tac [real_rinv_gt_zero] 1);
by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
by (forw_inst_tac [("x","f n")] real_rinv_gt_zero 1);
by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1);
by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
by (etac (real_not_refl2 RS not_sym) 1);
by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1],simpset()));
qed "LIMSEQ_rinv_zero";

Goal "!!f. ALL y. EX N. ALL n. N <= n --> y < f(n) \
\              ==> (%n. rinv(f n)) ----NS> 0r";
by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
                  LIMSEQ_rinv_zero]) 1);
qed "NSLIMSEQ_rinv_zero";

(*------------------------------------------------------*)
(*        Sequence  1/n --> 0 as n --> infinity         *)
(*------------------------------------------------------*)

Goal "(%n. rinv(real_of_posnat n)) ----> 0r";
by (rtac LIMSEQ_rinv_zero 1 THEN Step_tac 1);
by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
by (dtac (real_of_posnat_less_iff RS iffD2) 1);
by (auto_tac (claset() addEs [real_less_trans],simpset()));
qed "LIMSEQ_rinv_real_of_posnat";

Goal "(%n. rinv(real_of_posnat n)) ----NS> 0r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
    LIMSEQ_rinv_real_of_posnat]) 1);
qed "NSLIMSEQ_rinv_real_of_posnat";

(*------------------------------------------------------*)
(*    Sequence  r + 1/n --> r as n --> infinity         *)
(*    now easily proved                                 *)
(*------------------------------------------------------*)

Goal "(%n. r + rinv(real_of_posnat n)) ----> r";
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
    MRS LIMSEQ_add] 1);
by (Auto_tac);
qed "LIMSEQ_rinv_real_of_posnat_add";

Goal "(%n. r + rinv(real_of_posnat n)) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
    LIMSEQ_rinv_real_of_posnat_add]) 1);
qed "NSLIMSEQ_rinv_real_of_posnat_add";

(*---------------*)
(*    Also...    *)
(* --------------*)

Goal "(%n. r + -rinv(real_of_posnat n)) ----> r";
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat]
    MRS LIMSEQ_add_minus] 1);
by (Auto_tac);
qed "LIMSEQ_rinv_real_of_posnat_add_minus";

Goal "(%n. r + -rinv(real_of_posnat n)) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
    LIMSEQ_rinv_real_of_posnat_add_minus]) 1);
qed "NSLIMSEQ_rinv_real_of_posnat_add_minus";

Goal "(%n. r*( 1r + -rinv(real_of_posnat n))) ----> r";
by (cut_inst_tac [("b","1r")] ([LIMSEQ_const,
    LIMSEQ_rinv_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
by (Auto_tac);
qed "LIMSEQ_rinv_real_of_posnat_add_minus_mult";

Goal "(%n. r*( 1r + -rinv(real_of_posnat n))) ----NS> r";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
    LIMSEQ_rinv_real_of_posnat_add_minus_mult]) 1);
qed "NSLIMSEQ_rinv_real_of_posnat_add_minus_mult";


(*------------------------------------------------------*)
(*                   Real Powers                        *)
(*------------------------------------------------------*)

Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)";
by (induct_tac "m" 1);
by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const],
    simpset()));
qed_spec_mp "NSLIMSEQ_pow";

Goal "!!X. X ----> a ==> (%n. (X n) ^ m) ----> a ^ m";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
    NSLIMSEQ_pow]) 1);
qed "LIMSEQ_pow";

(*------------------------------------------------------*)
(*            0 <= x < 1r ==> (x ^ n ----> 0r)          *)
(* Proof will use (NS) Cauchy equivalence for           *) 
(* convergence and also fact that bounded and monotonic *)
(* sequence converges.                                  *)
(*------------------------------------------------------*)

Goalw [Bseq_def] 
      "!!x. [| 0r <= x; x < 1r |] ==> Bseq (%n. x ^ n)";
by (res_inst_tac [("x","1r")] exI 1);
by (auto_tac (claset() addDs [conjI RS realpow_le2] 
    addIs [real_less_imp_le],simpset() addsimps 
    [real_zero_less_one,rabs_eqI1,realpow_rabs RS sym] ));
qed "Bseq_realpow";

Goal
     "!!x. [| 0r <= x; x < 1r |] ==> monoseq (%n. x ^ n)";
by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1);
qed "monoseq_realpow";

Goal "!!x. [| 0r <= x; x < 1r |] ==> convergent (%n. x ^ n)";
by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
    Bseq_realpow,monoseq_realpow]) 1);
qed "convergent_realpow";

(* We now use NS criterion to bring proof of theorem through *)

Goalw [NSLIMSEQ_def]
     "[| 0r <= x; x < 1r |] ==> (%n. x ^ n) ----NS> 0r";
by (auto_tac (claset() addSDs [convergent_realpow],
    simpset() addsimps [convergent_NSconvergent_iff]));
by (forward_tac [NSconvergentD] 1);
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_def,
    NSCauchy_NSconvergent_iff RS sym,NSCauchy_def,
    starfunNat_pow]));
by (forward_tac [HNatInfinite_add_one] 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dtac bspec 1 THEN assume_tac 1);
by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
by (dtac inf_close_trans3 1 THEN assume_tac 1);
by (auto_tac (claset() addSDs [real_not_refl2 RS 
    real_mult_eq_self_zero2],simpset() addsimps 
    [hypreal_of_real_mult RS sym]));
qed "NSLIMSEQ_realpow_zero";

(*--------------------  standard version ------------------------*)
Goal 
     "!!x. [| 0r <= x; x < 1r |] ==> (%n. x ^ n) ----> 0r";
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
    LIMSEQ_NSLIMSEQ_iff]) 1);
qed "LIMSEQ_realpow_zero";

(*------------------------------------------------------*)
(*              Limit of c^n for |c| < 1                *)
(*------------------------------------------------------*)

Goal "rabs(c) < 1r ==> (%n. rabs(c) ^ n) ----> 0r";
by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,rabs_ge_zero]) 1);
qed "LIMSEQ_rabs_realpow_zero";

Goal "rabs(c) < 1r ==> (%n. rabs(c) ^ n) ----NS> 0r";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero,
    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
qed "NSLIMSEQ_rabs_realpow_zero";

Goal "rabs(c) < 1r ==> (%n. c ^ n) ----> 0r";
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
         simpset() addsimps [realpow_rabs RS sym]));
qed "LIMSEQ_rabs_realpow_zero2";

Goal "!!c. rabs(c) < 1r ==> (%n. c ^ n) ----NS> 0r";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2,
    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
qed "NSLIMSEQ_rabs_realpow_zero2";

(*------------------------------------------------------*)
(*  Someof the theorems about Hyperreals and Sequences  *)
(*------------------------------------------------------*)

(*** A bounded sequence is a finite hyperreal ***)
Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite";
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
       [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
       simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
        Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
qed "NSBseq_HFinite_hypreal";

(*** A sequence converging to zero defines an infinitesimal ***)
Goalw [NSLIMSEQ_def] 
      "X ----NS> 0r ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal";
by (dres_inst_tac [("x","whn")] bspec 1);
by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def,
    mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero]));
qed "NSLIMSEQ_zero_Infinitesimal_hypreal";

(***---------------------------------------------------------------
    Theorems proved by Harrison in HOL that we do not need 
    in order to prove equivalence between Cauchy criterion 
    and convergence:
 -- Show that every sequence contains a monotonic subsequence   
Goal "EX f. subseq f & monoseq (%n. s (f n))";
 -- Show that a subsequence of a bounded sequence is bounded
Goal "!!X. Bseq X ==> Bseq (%n. X (f n))";
 -- Show we can take subsequential terms arbitrarily far 
    up a sequence       
Goal "!!f. subseq f ==> n <= f(n)";
Goal "!!f. subseq f ==> EX n. N1 <= n & N2 <= f(n)";
 ---------------------------------------------------------------***)