# Theory SEQ

Up to index of Isabelle/HOL/HOL-Complex

theory SEQ
imports NatStar
begin

    (*  Title       : SEQ.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 1998  University of Cambridge
        Description : Convergence of sequences and series
        Conversion to Isar and new proofs by Lawrence C Paulson, 2004
        Additional contributions by Jeremy Avigad
    *)

    header {* Sequences and Series *}

    theory SEQ
    imports NatStar
    begin

    constdefs

      LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
        --{*Standard definition of convergence of sequence*}
      "X ----> L == (∀r. 0 < r --> (∃no. ∀n. no ≤ n --> ¦X n + -L¦ < r))"

      NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
        --{*Nonstandard definition of convergence of sequence*}
      "X ----NS> L == (∀N ∈ HNatInfinite. ( *f* X) N ≈ hypreal_of_real L)"

      lim :: "(nat => real) => real"
        --{*Standard definition of limit using choice operator*}
      "lim X == (@L. (X ----> L))"

      nslim :: "(nat => real) => real"
        --{*Nonstandard definition of limit using choice operator*}
      "nslim X == (@L. (X ----NS> L))"

      convergent :: "(nat => real) => bool"
        --{*Standard definition of convergence*}
      "convergent X == (∃L. (X ----> L))"

      NSconvergent :: "(nat => real) => bool"
        --{*Nonstandard definition of convergence*}
      "NSconvergent X == (∃L. (X ----NS> L))"

      Bseq :: "(nat => real) => bool"
        --{*Standard definition for bounded sequence*}
      "Bseq X == ∃K>0.∀n. ¦X n¦ ≤ K"

      NSBseq :: "(nat=>real) => bool"
        --{*Nonstandard definition for bounded sequence*}
      "NSBseq X == (∀N ∈ HNatInfinite. ( *f* X) N : HFinite)"

      monoseq :: "(nat=>real)=>bool"
        --{*Definition for monotonicity*}
      "monoseq X == (∀m. ∀n≥m. X m ≤ X n) | (∀m. ∀n≥m. X n ≤ X m)"

      subseq :: "(nat => nat) => bool"
        --{*Definition of subsequence*}
      "subseq f == ∀m. ∀n>m. (f m) < (f n)"

      Cauchy :: "(nat => real) => bool"
        --{*Standard definition of the Cauchy condition*}
      "Cauchy X == ∀e>0. ∃M. ∀m ≥ M. ∀n ≥ M. abs((X m) + -(X n)) < e"

      NSCauchy :: "(nat => real) => bool"
        --{*Nonstandard definition*}
      "NSCauchy X == (∀M ∈ HNatInfinite. ∀N ∈ HNatInfinite.
                          ( *f* X) M ≈ ( *f* X) N)"

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

    lemma SEQ_Infinitesimal:
          "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
    apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfun)
    apply (simp add: star_n_inverse)
    apply (rule bexI [OF _ Rep_star_star_n])
    apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
    done

    subsection{*LIMSEQ and NSLIMSEQ*}

    lemma LIMSEQ_iff:
          "(X ----> L) = (∀r>0. ∃no. ∀n ≥ no. ¦X n + -L¦ < r)"
    by (simp add: LIMSEQ_def)

    lemma NSLIMSEQ_iff:
        "(X ----NS> L) = (∀N ∈ HNatInfinite. ( *f* X) N ≈ hypreal_of_real L)"
    by (simp add: NSLIMSEQ_def)

    text{*LIMSEQ ==> NSLIMSEQ*}

    lemma LIMSEQ_NSLIMSEQ:
          "X ----> L ==> X ----NS> L"
    apply (simp add: LIMSEQ_def NSLIMSEQ_def)
    apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
    apply (rule_tac x = N in star_cases)
    apply (rule approx_minus_iff [THEN iffD2])
    apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
                  star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n], safe)
    apply (drule_tac x = u in spec, safe)
    apply (drule_tac x = no in spec, fuf)
    apply (blast dest: less_imp_le)
    done

    text{*NSLIMSEQ ==> LIMSEQ*}

    lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). ∀n. n ≤ f n
               ==> {n. f n = 0} = {0} | {n. f n = 0} = {}"
    apply auto
    apply (drule_tac x = xa in spec)
    apply (drule_tac [2] x = x in spec, auto)
    done

    lemma lemma_NSLIMSEQ2: "{n. f n ≤ Suc u} = {n. f n ≤ u} Un {n. f n = Suc u}"
    by (auto simp add: le_Suc_eq)

    lemma lemma_NSLIMSEQ3:
         "!!(f::nat=>nat). ∀n. n ≤ f n ==> {n. f n = Suc u} ≤ {n. n ≤ Suc u}"
    apply auto
    apply (drule_tac x = x in spec, auto)
    done

    text{* the following sequence @{term "f(n)"} defines a hypernatural *}
    lemma NSLIMSEQ_finite_set:
         "!!(f::nat=>nat). ∀n. n ≤ f n ==> finite {n. f n ≤ u}"
    apply (induct u)
    apply (auto simp add: lemma_NSLIMSEQ2)
    apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def])
    apply (drule lemma_NSLIMSEQ1, safe)
    apply (simp_all (no_asm_simp))
    done

    lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n ≤ u}"
    by (auto dest: less_le_trans simp add: le_def)

    text{* the index set is in the free ultrafilter *}
    lemma FreeUltrafilterNat_NSLIMSEQ:
         "!!(f::nat=>nat). ∀n. n ≤ f n ==> {n. u < f n} : FreeUltrafilterNat"
    apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2])
    apply (rule FreeUltrafilterNat_finite)
    apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set)
    done

    text{* thus, the sequence defines an infinite hypernatural! *}
    lemma HNatInfinite_NSLIMSEQ: "∀n. n ≤ f n
              ==> star_n f : HNatInfinite"
    apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n], safe)
    apply (erule FreeUltrafilterNat_NSLIMSEQ)
    done

    lemma lemmaLIM:
         "{n. X (f n) + - L = Y n} Int {n. ¦Y n¦ < r} ≤
          {n. ¦X (f n) + - L¦ < r}"
    by auto

    lemma lemmaLIM2:
      "{n. ¦X (f n) + - L¦ < r} Int {n. r ≤ abs (X (f n) + - (L::real))} = {}"
    by auto

    lemma lemmaLIM3: "[| 0 < r; ∀n. r ≤ ¦X (f n) + - L¦;
               ( *f* X) (star_n f) +
               - hypreal_of_real  L ≈ 0 |] ==> False"
    apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
    apply (rename_tac "Y")
    apply (drule_tac x = r in spec, safe)
    apply (drule FreeUltrafilterNat_Int, assumption)
    apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset])
    apply (drule FreeUltrafilterNat_all)
    apply (erule_tac V = "{n. ¦Y n¦ < r} : FreeUltrafilterNat" in thin_rl)
    apply (drule FreeUltrafilterNat_Int, assumption)
    apply (simp add: lemmaLIM2)
    done

    lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
    apply (simp add: LIMSEQ_def NSLIMSEQ_def)
    apply (rule ccontr, simp, safe)
    txt{* skolemization step *}
    apply (drule choice, safe)
    apply (drule_tac x = "star_n f" in bspec)
    apply (drule_tac [2] approx_minus_iff [THEN iffD1])
    apply (simp_all add: linorder_not_less)
    apply (blast intro: HNatInfinite_NSLIMSEQ)
    apply (blast intro: lemmaLIM3)
    done

    text{* Now, the all-important result is trivially proved! *}
    theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)"
    by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)

    subsection{*Theorems About Sequences*}

    lemma NSLIMSEQ_const: "(%n. k) ----NS> k"
    by (simp add: NSLIMSEQ_def)

    lemma LIMSEQ_const: "(%n. k) ----> k"
    by (simp add: LIMSEQ_def)

    lemma NSLIMSEQ_add:
          "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b"
    by (auto intro: approx_add simp add: NSLIMSEQ_def starfun_add [symmetric])

    lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add)

    lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b"
      apply (subgoal_tac "%n. (f n + b) == %n. (f n + (%n. b) n)")
      apply (subgoal_tac "(%n. b) ----> b")
      apply (auto simp add: LIMSEQ_add LIMSEQ_const)
    done

    lemma NSLIMSEQ_add_const: "f ----NS> a ==> (%n.(f n + b)) ----NS> a + b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_add_const)

    lemma NSLIMSEQ_mult:
          "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
    by (auto intro!: approx_mult_HFinite
            simp add: NSLIMSEQ_def starfun_mult [symmetric])

    lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)

    lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a"
    by (auto simp add: NSLIMSEQ_def starfun_minus [symmetric])

    lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus)

    lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a"
    by (drule LIMSEQ_minus, simp)

    lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a"
    by (drule NSLIMSEQ_minus, simp)

    lemma NSLIMSEQ_add_minus:
         "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b"
    by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y])

    lemma LIMSEQ_add_minus:
         "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus)

    lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b"
    apply (simp add: diff_minus)
    apply (blast intro: LIMSEQ_add_minus)
    done

    lemma NSLIMSEQ_diff:
         "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b"
    apply (simp add: diff_minus)
    apply (blast intro: NSLIMSEQ_add_minus)
    done

    lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n  - b)) ----> a - b"
      apply (subgoal_tac "%n. (f n - b) == %n. (f n - (%n. b) n)")
      apply (subgoal_tac "(%n. b) ----> b")
      apply (auto simp add: LIMSEQ_diff LIMSEQ_const)
    done

    lemma NSLIMSEQ_diff_const: "f ----NS> a ==> (%n.(f n - b)) ----NS> a - b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [THEN sym] LIMSEQ_diff_const)

    text{*Proof is like that of @{text NSLIM_inverse}.*}
    lemma NSLIMSEQ_inverse:
         "[| X ----NS> a;  a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)"
    by (simp add: NSLIMSEQ_def starfun_inverse [symmetric]
                  hypreal_of_real_approx_inverse)

    text{*Standard version of theorem*}
    lemma LIMSEQ_inverse:
         "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)"
    by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff)

    lemma NSLIMSEQ_mult_inverse:
         "[| X ----NS> a;  Y ----NS> b;  b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b"
    by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse)

    lemma LIMSEQ_divide:
         "[| X ----> a;  Y ----> b;  b ~= 0 |] ==> (%n. X n / Y n) ----> a/b"
    by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)

    text{*Uniqueness of limit*}
    lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b"
    apply (simp add: NSLIMSEQ_def)
    apply (drule HNatInfinite_whn [THEN [2] bspec])+
    apply (auto dest: approx_trans3)
    done

    lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique)

    lemma LIMSEQ_setsum:
      assumes n: "!!n. n ∈ S ==> X n ----> L n"
      shows "(λm. ∑n∈S. X n m) ----> (∑n∈S. L n)"
    proof (cases "finite S")
      case True
      thus ?thesis using n
      proof (induct)
        case empty
        show ?case
          by (simp add: LIMSEQ_const)
      next
        case insert
        thus ?case
          by (simp add: LIMSEQ_add)
      qed
    next
      case False
      thus ?thesis
        by (simp add: setsum_def LIMSEQ_const)
    qed

    lemma LIMSEQ_setprod:
      assumes n: "!!n. n ∈ S ==> X n ----> L n"
      shows "(λm. ∏n∈S. X n m) ----> (∏n∈S. L n)"
    proof (cases "finite S")
      case True
      thus ?thesis using n
      proof (induct)
        case empty
        show ?case
          by (simp add: LIMSEQ_const)
      next
        case insert
        thus ?case
          by (simp add: LIMSEQ_mult)
      qed
    next
      case False
      thus ?thesis
        by (simp add: setprod_def LIMSEQ_const)
    qed

    lemma LIMSEQ_ignore_initial_segment: "f ----> a
      ==> (%n. f(n + k)) ----> a"
      apply (unfold LIMSEQ_def)
      apply (clarify)
      apply (drule_tac x = r in spec)
      apply (clarify)
      apply (rule_tac x = "no + k" in exI)
      by auto

    lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
        f ----> a"
      apply (unfold LIMSEQ_def)
      apply clarsimp
      apply (drule_tac x = r in spec)
      apply clarsimp
      apply (rule_tac x = "no + k" in exI)
      apply clarsimp
      apply (drule_tac x = "n - k" in spec)
      apply (frule mp)
      apply arith
      apply simp
    done

    lemma LIMSEQ_diff_approach_zero:
      "g ----> L ==> (%x. f x - g x) ----> 0  ==>
         f ----> L"
      apply (drule LIMSEQ_add)
      apply assumption
      apply simp
    done

    lemma LIMSEQ_diff_approach_zero2:
      "f ----> L ==> (%x. f x - g x) ----> 0  ==>
         g ----> L";
      apply (drule LIMSEQ_diff)
      apply assumption
      apply simp
    done

    subsection{*Nslim and Lim*}

    lemma limI: "X ----> L ==> lim X = L"
    apply (simp add: lim_def)
    apply (blast intro: LIMSEQ_unique)
    done

    lemma nslimI: "X ----NS> L ==> nslim X = L"
    apply (simp add: nslim_def)
    apply (blast intro: NSLIMSEQ_unique)
    done

    lemma lim_nslim_iff: "lim X = nslim X"
    by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)

    subsection{*Convergence*}

    lemma convergentD: "convergent X ==> ∃L. (X ----> L)"
    by (simp add: convergent_def)

    lemma convergentI: "(X ----> L) ==> convergent X"
    by (auto simp add: convergent_def)

    lemma NSconvergentD: "NSconvergent X ==> ∃L. (X ----NS> L)"
    by (simp add: NSconvergent_def)

    lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X"
    by (auto simp add: NSconvergent_def)

    lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X"
    by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff)

    lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)"
    by (auto intro: someI simp add: NSconvergent_def nslim_def)

    lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
    by (auto intro: someI simp add: convergent_def lim_def)

    text{*Subsequence (alternative definition, (e.g. Hoskins)*}

    lemma subseq_Suc_iff: "subseq f = (∀n. (f n) < (f (Suc n)))"
    apply (simp add: subseq_def)
    apply (auto dest!: less_imp_Suc_add)
    apply (induct_tac k)
    apply (auto intro: less_trans)
    done

    subsection{*Monotonicity*}

    lemma monoseq_Suc:
       "monoseq X = ((∀n. X n ≤ X (Suc n))
                     | (∀n. X (Suc n) ≤ X n))"
    apply (simp add: monoseq_def)
    apply (auto dest!: le_imp_less_or_eq)
    apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
    apply (induct_tac "ka")
    apply (auto intro: order_trans)
    apply (erule swap)
    apply (induct_tac "k")
    apply (auto intro: order_trans)
    done

    lemma monoI1: "∀m. ∀ n ≥ m. X m ≤ X n ==> monoseq X"
    by (simp add: monoseq_def)

    lemma monoI2: "∀m. ∀ n ≥ m. X n ≤ X m ==> monoseq X"
    by (simp add: monoseq_def)

    lemma mono_SucI1: "∀n. X n ≤ X (Suc n) ==> monoseq X"
    by (simp add: monoseq_Suc)

    lemma mono_SucI2: "∀n. X (Suc n) ≤ X n ==> monoseq X"
    by (simp add: monoseq_Suc)

    subsection{*Bounded Sequence*}

    lemma BseqD: "Bseq X ==> ∃K. 0 < K & (∀n. ¦X n¦ ≤ K)"
    by (simp add: Bseq_def)

    lemma BseqI: "[| 0 < K; ∀n. ¦X n¦ ≤ K |] ==> Bseq X"
    by (auto simp add: Bseq_def)

    lemma lemma_NBseq_def:
         "(∃K > 0. ∀n. ¦X n¦ ≤ K) =
          (∃N. ∀n. ¦X n¦ ≤ real(Suc N))"
    apply auto
     prefer 2 apply force
    apply (cut_tac x = K in reals_Archimedean2, clarify)
    apply (rule_tac x = n in exI, clarify)
    apply (drule_tac x = na in spec)
    apply (auto simp add: real_of_nat_Suc)
    done

    text{* alternative definition for Bseq *}
    lemma Bseq_iff: "Bseq X = (∃N. ∀n. ¦X n¦ ≤ real(Suc N))"
    apply (simp add: Bseq_def)
    apply (simp (no_asm) add: lemma_NBseq_def)
    done

    lemma lemma_NBseq_def2:
         "(∃K > 0. ∀n. ¦X n¦ ≤ K) = (∃N. ∀n. ¦X n¦ < real(Suc N))"
    apply (subst lemma_NBseq_def, auto)
    apply (rule_tac x = "Suc N" in exI)
    apply (rule_tac [2] x = N in exI)
    apply (auto simp add: real_of_nat_Suc)
     prefer 2 apply (blast intro: order_less_imp_le)
    apply (drule_tac x = n in spec, simp)
    done

    (* yet another definition for Bseq *)
    lemma Bseq_iff1a: "Bseq X = (∃N. ∀n. ¦X n¦ < real(Suc N))"
    by (simp add: Bseq_def lemma_NBseq_def2)

    lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
    by (simp add: NSBseq_def)

    lemma NSBseqI: "∀N ∈ HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
    by (simp add: NSBseq_def)

    text{*The standard definition implies the nonstandard definition*}

    lemma lemma_Bseq: "∀n. ¦X n¦ ≤ K ==> ∀n. abs(X((f::nat=>nat) n)) ≤ K"
    by auto

    lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
    apply (simp add: Bseq_def NSBseq_def, safe)
    apply (rule_tac x = N in star_cases)
    apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff
                          HNatInfinite_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n])
    apply (drule_tac f = Xa in lemma_Bseq)
    apply (rule_tac x = "K+1" in exI)
    apply (drule_tac P="%n. ?f n ≤ K" in FreeUltrafilterNat_all, ultra)
    done

    text{*The nonstandard definition implies the standard definition*}

    (* similar to NSLIM proof in REALTOPOS *)

    text{* We need to get rid of the real variable and do so by proving the
       following, which relies on the Archimedean property of the reals.
       When we skolemize we then get the required function @{term "f::nat=>nat"}.
       Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
       which woulid be useless.*}

    lemma lemmaNSBseq:
         "∀K > 0. ∃n. K < ¦X n¦
          ==> ∀N. ∃n. real(Suc N) < ¦X n¦"
    apply safe
    apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
    done

    lemma lemmaNSBseq2: "∀K > 0. ∃n. K < ¦X n¦
                         ==> ∃f. ∀N. real(Suc N) < ¦X (f N)¦"
    apply (drule lemmaNSBseq)
    apply (drule choice, blast)
    done

    lemma real_seq_to_hypreal_HInfinite:
         "∀N. real(Suc N) < ¦X (f N)¦
          ==>  star_n (X o f) : HInfinite"
    apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
    apply (rule bexI [OF _ Rep_star_star_n], clarify)
    apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
    apply (drule FreeUltrafilterNat_all)
    apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
    apply (auto simp add: real_of_nat_Suc)
    done

    text{* Now prove that we can get out an infinite hypernatural as well
         defined using the skolem function  @{term "f::nat=>nat"} above*}

    lemma lemma_finite_NSBseq:
         "{n. f n ≤ Suc u & real(Suc n) < ¦X (f n)¦} ≤
          {n. f n ≤ u & real(Suc n) < ¦X (f n)¦} Un
          {n. real(Suc n) < ¦X (Suc u)¦}"
    by (auto dest!: le_imp_less_or_eq)

    lemma lemma_finite_NSBseq2:
         "finite {n. f n ≤ (u::nat) &  real(Suc n) < ¦X(f n)¦}"
    apply (induct "u")
    apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
    apply (rule_tac B = "{n. real (Suc n) < ¦X 0¦ }" in finite_subset)
    apply (auto intro: finite_real_of_nat_less_real
                simp add: real_of_nat_Suc less_diff_eq [symmetric])
    done

    lemma HNatInfinite_skolem_f:
         "∀N. real(Suc N) < ¦X (f N)¦
          ==> star_n f : HNatInfinite"
    apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n], safe)
    apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
    apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE])
    apply (subgoal_tac "{n. f n ≤ u & real (Suc n) < ¦X (f n)¦} =
                        {n. f n ≤ u} ∩ {N. real (Suc N) < ¦X (f N)¦}")
    apply (erule ssubst)
     apply (auto simp add: linorder_not_less Compl_def)
    done

    lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
    apply (simp add: Bseq_def NSBseq_def)
    apply (rule ccontr)
    apply (auto simp add: linorder_not_less [symmetric])
    apply (drule lemmaNSBseq2, safe)
    apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
    apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
    apply (auto simp add: starfun o_def HFinite_HInfinite_iff)
    done

    text{* Equivalence of nonstandard and standard definitions
      for a bounded sequence*}
    lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
    by (blast intro!: NSBseq_Bseq Bseq_NSBseq)

    text{*A convergent sequence is bounded:
     Boundedness as a necessary condition for convergence.
     The nonstandard version has no existential, as usual *}

    lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
    apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
    apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite)
    done

    text{*Standard Version: easily now proved using equivalence of NS and
     standard definitions *}
    lemma convergent_Bseq: "convergent X ==> Bseq X"
    by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)

    subsection{*Upper Bounds and Lubs of Bounded Sequences*}

    lemma Bseq_isUb:
      "!!(X::nat=>real). Bseq X ==> ∃U. isUb (UNIV::real set) {x. ∃n. X n = x} U"
    by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff)

    text{* Use completeness of reals (supremum property)
       to show that any bounded sequence has a least upper bound*}

    lemma Bseq_isLub:
      "!!(X::nat=>real). Bseq X ==>
       ∃U. isLub (UNIV::real set) {x. ∃n. X n = x} U"
    by (blast intro: reals_complete Bseq_isUb)

    lemma NSBseq_isUb: "NSBseq X ==> ∃U. isUb UNIV {x. ∃n. X n = x} U"
    by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)

    lemma NSBseq_isLub: "NSBseq X ==> ∃U. isLub UNIV {x. ∃n. X n = x} U"
    by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)

    subsection{*A Bounded and Monotonic Sequence Converges*}

    lemma lemma_converg1:
         "!!(X::nat=>real). [| ∀m. ∀ n ≥ m. X m ≤ X n;
                      isLub (UNIV::real set) {x. ∃n. X n = x} (X ma)
                   |] ==> ∀n ≥ ma. X n = X ma"
    apply safe
    apply (drule_tac y = "X n" in isLubD2)
    apply (blast dest: order_antisym)+
    done

    text{* The best of both worlds: Easier to prove this result as a standard
       theorem and then use equivalence to "transfer" it into the
       equivalent nonstandard form if needed!*}

    lemma Bmonoseq_LIMSEQ: "∀n. m ≤ n --> X n = X m ==> ∃L. (X ----> L)"
    apply (simp add: LIMSEQ_def)
    apply (rule_tac x = "X m" in exI, safe)
    apply (rule_tac x = m in exI, safe)
    apply (drule spec, erule impE, auto)
    done

    text{*Now, the same theorem in terms of NS limit *}
    lemma Bmonoseq_NSLIMSEQ: "∀n ≥ m. X n = X m ==> ∃L. (X ----NS> L)"
    by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)

    lemma lemma_converg2:
       "!!(X::nat=>real).
        [| ∀m. X m ~= U;  isLub UNIV {x. ∃n. X n = x} U |] ==> ∀m. X m < U"
    apply safe
    apply (drule_tac y = "X m" in isLubD2)
    apply (auto dest!: order_le_imp_less_or_eq)
    done

    lemma lemma_converg3: "!!(X ::nat=>real). ∀m. X m ≤ U ==> isUb UNIV {x. ∃n. X n = x} U"
    by (rule setleI [THEN isUbI], auto)

    text{* FIXME: @{term "U - T < U"} is redundant *}
    lemma lemma_converg4: "!!(X::nat=> real).
                   [| ∀m. X m ~= U;
                      isLub UNIV {x. ∃n. X n = x} U;
                      0 < T;
                      U + - T < U
                   |] ==> ∃m. U + -T < X m & X m < U"
    apply (drule lemma_converg2, assumption)
    apply (rule ccontr, simp)
    apply (simp add: linorder_not_less)
    apply (drule lemma_converg3)
    apply (drule isLub_le_isUb, assumption)
    apply (auto dest: order_less_le_trans)
    done

    text{*A standard proof of the theorem for monotone increasing sequence*}

    lemma Bseq_mono_convergent:
         "[| Bseq X; ∀m. ∀n ≥ m. X m ≤ X n |] ==> convergent X"
    apply (simp add: convergent_def)
    apply (frule Bseq_isLub, safe)
    apply (case_tac "∃m. X m = U", auto)
    apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ)
    (* second case *)
    apply (rule_tac x = U in exI)
    apply (subst LIMSEQ_iff, safe)
    apply (frule lemma_converg2, assumption)
    apply (drule lemma_converg4, auto)
    apply (rule_tac x = m in exI, safe)
    apply (subgoal_tac "X m ≤ X n")
     prefer 2 apply blast
    apply (drule_tac x=n and P="%m. X m < U" in spec, arith)
    done

    text{*Nonstandard version of the theorem*}

    lemma NSBseq_mono_NSconvergent:
         "[| NSBseq X; ∀m. ∀n ≥ m. X m ≤ X n |] ==> NSconvergent X"
    by (auto intro: Bseq_mono_convergent
             simp add: convergent_NSconvergent_iff [symmetric]
                       Bseq_NSBseq_iff [symmetric])

    lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))"
    apply (simp add: convergent_def)
    apply (auto dest: LIMSEQ_minus)
    apply (drule LIMSEQ_minus, auto)
    done

    lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X"
    by (simp add: Bseq_def)

    text{*Main monotonicity theorem*}
    lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X"
    apply (simp add: monoseq_def, safe)
    apply (rule_tac [2] convergent_minus_iff [THEN ssubst])
    apply (drule_tac [2] Bseq_minus_iff [THEN ssubst])
    apply (auto intro!: Bseq_mono_convergent)
    done

    subsection{*A Few More Equivalence Theorems for Boundedness*}

    text{*alternative formulation for boundedness*}
    lemma Bseq_iff2: "Bseq X = (∃k > 0. ∃x. ∀n. ¦X(n) + -x¦ ≤ k)"
    apply (unfold Bseq_def, safe)
    apply (rule_tac [2] x = "k + ¦x¦ " in exI)
    apply (rule_tac x = K in exI, simp)
    apply (rule exI [where x = 0], auto)
    apply (drule_tac x=n in spec, arith)+
    done

    text{*alternative formulation for boundedness*}
    lemma Bseq_iff3: "Bseq X = (∃k > 0. ∃N. ∀n. abs(X(n) + -X(N)) ≤ k)"
    apply safe
    apply (simp add: Bseq_def, safe)
    apply (rule_tac x = "K + ¦X N¦ " in exI)
    apply auto
    apply arith
    apply (rule_tac x = N in exI, safe)
    apply (drule_tac x = n in spec, arith)
    apply (auto simp add: Bseq_iff2)
    done

    lemma BseqI2: "(∀n. k ≤ f n & f n ≤ K) ==> Bseq f"
    apply (simp add: Bseq_def)
    apply (rule_tac x = " (¦k¦ + ¦K¦) + 1" in exI, auto)
    apply (drule_tac [2] x = n in spec, arith+)
    done

    subsection{*Equivalence Between NS and Standard Cauchy Sequences*}

    subsubsection{*Standard Implies Nonstandard*}

    lemma lemmaCauchy1:
         "star_n x : HNatInfinite
          ==> {n. M ≤ x n} : FreeUltrafilterNat"
    apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
    apply (drule_tac x = M in spec, ultra)
    done

    lemma lemmaCauchy2:
         "{n. ∀m n. M ≤ m & M ≤ (n::nat) --> ¦X m + - X n¦ < u} Int
          {n. M ≤ xa n} Int {n. M ≤ x n} ≤
          {n. abs (X (xa n) + - X (x n)) < u}"
    by blast

    lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
    apply (simp add: Cauchy_def NSCauchy_def, safe)
    apply (rule_tac x = M in star_cases)
    apply (rule_tac x = N in star_cases)
    apply (rule approx_minus_iff [THEN iffD2])
    apply (rule mem_infmal_iff [THEN iffD1])
    apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
    apply (rule bexI, auto)
    apply (drule spec, auto)
    apply (drule_tac M = M in lemmaCauchy1)
    apply (drule_tac M = M in lemmaCauchy1)
    apply (rule_tac x1 = Xaa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
    apply (rule FreeUltrafilterNat_Int)
    apply (auto intro: FreeUltrafilterNat_Int)
    done

    subsubsection{*Nonstandard Implies Standard*}

    lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X"
    apply (auto simp add: Cauchy_def NSCauchy_def)
    apply (rule ccontr, simp)
    apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)
    apply (drule bspec, assumption)
    apply (drule_tac x = "star_n fa" in bspec);
    apply (auto simp add: starfun)
    apply (drule approx_minus_iff [THEN iffD1])
    apply (drule mem_infmal_iff [THEN iffD2])
    apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
    apply (rename_tac "Y")
    apply (drule_tac x = e in spec, auto)
    apply (drule FreeUltrafilterNat_Int, assumption)
    apply (subgoal_tac "{n. ¦X (f n) + - X (fa n)¦ < e} ∈ \<U>")
     prefer 2 apply (erule FreeUltrafilterNat_subset, force)
    apply (rule FreeUltrafilterNat_empty [THEN notE])
    apply (subgoal_tac
             "{n. abs (X (f n) + - X (fa n)) < e} Int
              {M. ~ abs (X (f M) + - X (fa M)) < e}  =  {}")
    apply auto
    done

    theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
    by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)

    text{*A Cauchy sequence is bounded -- this is the standard
      proof mechanization rather than the nonstandard proof*}

    lemma lemmaCauchy: "∀n ≥ M. ¦X M + - X n¦ < (1::real)
              ==>  ∀n ≥ M. ¦X n¦ < 1 + ¦X M¦"
    apply safe
    apply (drule spec, auto, arith)
    done

    lemma less_Suc_cancel_iff: "(n < Suc M) = (n ≤ M)"
    by auto

    text{* FIXME: Long. Maximal element in subsequence *}
    lemma SUP_rabs_subseq:
         "∃m ≤ M. ∀n ≤ M. ¦(X::nat=> real) n¦ ≤ ¦X m¦"
    apply (induct M)
    apply (rule_tac x = 0 in exI, simp, safe)
    apply (cut_tac x = "¦X (Suc M)¦" and y = "¦X m¦ " in linorder_less_linear)
    apply safe
    apply (rule_tac x = m in exI)
    apply (rule_tac [2] x = m in exI)
    apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
    apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE])
    apply (simp_all add: less_Suc_cancel_iff)
    apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
    done

    lemma lemma_Nat_covered:
         "[| ∀m::nat. m ≤ M --> P M m;
             ∀m ≥ M. P M m |]
          ==> ∀m. P M m"
    by (auto elim: less_asym simp add: le_def)

    lemma lemma_trans1:
         "[| ∀n ≤ M. ¦(X::nat=>real) n¦ ≤ a;  a < b |]
          ==> ∀n ≤ M. ¦X n¦ ≤ b"
    by (blast intro: order_le_less_trans [THEN order_less_imp_le])

    lemma lemma_trans2:
         "[| ∀n ≥ M. ¦(X::nat=>real) n¦ < a; a < b |]
          ==> ∀n ≥ M. ¦X n¦≤ b"
    by (blast intro: order_less_trans [THEN order_less_imp_le])

    lemma lemma_trans3:
         "[| ∀n ≤ M. ¦X n¦ ≤ a; a = b |]
          ==> ∀n ≤ M. ¦X n¦ ≤ b"
    by auto

    lemma lemma_trans4: "∀n ≥ M. ¦(X::nat=>real) n¦ < a
                  ==>  ∀n ≥ M. ¦X n¦ ≤ a"
    by (blast intro: order_less_imp_le)

    text{*Proof is more involved than outlines sketched by various authors
     would suggest*}

    lemma Cauchy_Bseq: "Cauchy X ==> Bseq X"
    apply (simp add: Cauchy_def Bseq_def)
    apply (drule_tac x = 1 in spec)
    apply (erule zero_less_one [THEN [2] impE], safe)
    apply (drule_tac x = M in spec, simp)
    apply (drule lemmaCauchy)
    apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe)
    apply (cut_tac x = "¦X m¦ " and y = "1 + ¦X M¦ " in linorder_less_linear)
    apply safe
    apply (drule lemma_trans1, assumption)
    apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl)
    apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl)
    apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans])
    apply (drule lemma_trans4)
    apply (drule_tac [2] lemma_trans4)
    apply (rule_tac x = "1 + ¦X M¦ " in exI)
    apply (rule_tac [2] x = "1 + ¦X M¦ " in exI)
    apply (rule_tac [3] x = "¦X m¦ " in exI)
    apply (auto elim!: lemma_Nat_covered)
    done

    text{*A Cauchy sequence is bounded -- nonstandard version*}

    lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
    by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)

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

    lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X"
    apply (simp add: NSconvergent_def NSLIMSEQ_def, safe)
    apply (frule NSCauchy_NSBseq)
    apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def)
    apply (drule HNatInfinite_whn [THEN [2] bspec])
    apply (drule HNatInfinite_whn [THEN [2] bspec])
    apply (auto dest!: st_part_Ex simp add: SReal_iff)
    apply (blast intro: approx_trans3)
    done

    text{*Standard proof for free*}
    lemma Cauchy_convergent_iff: "Cauchy X = convergent X"
    by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff)

    text{*We can now try and derive a few properties of sequences,
         starting with the limit comparison property for sequences.*}

    lemma NSLIMSEQ_le:
           "[| f ----NS> l; g ----NS> m;
               ∃N. ∀n ≥ N. f(n) ≤ g(n)
            |] ==> l ≤ m"
    apply (simp add: NSLIMSEQ_def, safe)
    apply (drule starfun_le_mono)
    apply (drule HNatInfinite_whn [THEN [2] bspec])+
    apply (drule_tac x = whn in spec)
    apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
    apply clarify
    apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2)
    done

    (* standard version *)
    lemma LIMSEQ_le:
         "[| f ----> l; g ----> m; ∃N. ∀n ≥ N. f(n) ≤ g(n) |]
          ==> l ≤ m"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)

    lemma LIMSEQ_le_const: "[| X ----> r; ∀n. a ≤ X n |] ==> a ≤ r"
    apply (rule LIMSEQ_le)
    apply (rule LIMSEQ_const, auto)
    done

    lemma NSLIMSEQ_le_const: "[| X ----NS> r; ∀n. a ≤ X n |] ==> a ≤ r"
    by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const)

    lemma LIMSEQ_le_const2: "[| X ----> r; ∀n. X n ≤ a |] ==> r ≤ a"
    apply (rule LIMSEQ_le)
    apply (rule_tac [2] LIMSEQ_const, auto)
    done

    lemma NSLIMSEQ_le_const2: "[| X ----NS> r; ∀n. X n ≤ a |] ==> r ≤ a"
    by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2)

    text{*Shift a convergent series by 1:
      By the equivalence between Cauchiness and convergence and because
      the successor of an infinite hypernatural is also infinite.*}

    lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"
    apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
    apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
    apply (drule bspec, assumption)
    apply (drule bspec, assumption)
    apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add])
    apply (blast intro: approx_trans3)
    done

    text{* standard version *}
    lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)

    lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"
    apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]])
    apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfun_shift_one)
    apply (drule bspec, assumption)
    apply (drule bspec, assumption)
    apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff])
    apply (drule_tac x="N - 1" in bspec)
    apply (auto intro: approx_trans3)
    done

    lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
    apply (simp add: LIMSEQ_NSLIMSEQ_iff)
    apply (erule NSLIMSEQ_imp_Suc)
    done

    lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
    by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)

    lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)"
    by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)

    text{*A sequence tends to zero iff its abs does*}
    lemma LIMSEQ_rabs_zero: "((%n. ¦f n¦) ----> 0) = (f ----> 0)"
    by (simp add: LIMSEQ_def)

    text{*We prove the NS version from the standard one, since the NS proof
       seems more complicated than the standard one above!*}
    lemma NSLIMSEQ_rabs_zero: "((%n. ¦f n¦) ----NS> 0) = (f ----NS> 0)"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero)

    text{*Generalization to other limits*}
    lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. ¦f n¦) ----NS> ¦l¦"
    apply (simp add: NSLIMSEQ_def)
    apply (auto intro: approx_hrabs
                simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
    done

    text{* standard version *}
    lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. ¦f n¦) ----> ¦l¦"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs)

    text{*An unbounded sequence's inverse tends to 0*}

    text{* standard proof seems easier *}
    lemma LIMSEQ_inverse_zero:
          "∀y. ∃N. ∀n ≥ N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
    apply (simp add: LIMSEQ_def, safe)
    apply (drule_tac x = "inverse r" in spec, safe)
    apply (rule_tac x = N in exI, safe)
    apply (drule spec, auto)
    apply (frule positive_imp_inverse_positive)
    apply (frule order_less_trans, assumption)
    apply (frule_tac a = "f n" in positive_imp_inverse_positive)
    apply (simp add: abs_if)
    apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
    apply (auto intro: inverse_less_iff_less [THEN iffD2]
                simp del: inverse_inverse_eq)
    done

    lemma NSLIMSEQ_inverse_zero:
         "∀y. ∃N. ∀n ≥ N. y < f(n)
          ==> (%n. inverse(f n)) ----NS> 0"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)

    text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}

    lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    apply (rule LIMSEQ_inverse_zero, safe)
    apply (cut_tac x = y in reals_Archimedean2)
    apply (safe, rule_tac x = n in exI)
    apply (auto simp add: real_of_nat_Suc)
    done

    lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)

    text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
    infinity is now easily proved*}

    lemma LIMSEQ_inverse_real_of_nat_add:
         "(%n. r + inverse(real(Suc n))) ----> r"
    by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)

    lemma NSLIMSEQ_inverse_real_of_nat_add:
         "(%n. r + inverse(real(Suc n))) ----NS> r"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)

    lemma LIMSEQ_inverse_real_of_nat_add_minus:
         "(%n. r + -inverse(real(Suc n))) ----> r"
    by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto)

    lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
         "(%n. r + -inverse(real(Suc n))) ----NS> r"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus)

    lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
         "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
    by (cut_tac b=1 in
            LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)

    lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:
         "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r"
    by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult)

    text{* Real Powers*}

    lemma NSLIMSEQ_pow [rule_format]:
         "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)"
    apply (induct "m")
    apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const)
    done

    lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m"
    by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow)

    text{*The sequence @{term "x^n"} tends to 0 if @{term "0≤x"} and @{term
    "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
      also fact that bounded and monotonic sequence converges.*}

    lemma Bseq_realpow: "[| 0 ≤ x; x ≤ 1 |] ==> Bseq (%n. x ^ n)"
    apply (simp add: Bseq_def)
    apply (rule_tac x = 1 in exI)
    apply (simp add: power_abs)
    apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
    done

    lemma monoseq_realpow: "[| 0 ≤ x; x ≤ 1 |] ==> monoseq (%n. x ^ n)"
    apply (clarify intro!: mono_SucI2)
    apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
    done

    lemma convergent_realpow: "[| 0 ≤ x; x ≤ 1 |] ==> convergent (%n. x ^ n)"
    by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)

    text{* We now use NS criterion to bring proof of theorem through *}

    lemma NSLIMSEQ_realpow_zero: "[| 0 ≤ x; x < 1 |] ==> (%n. x ^ n) ----NS> 0"
    apply (simp add: NSLIMSEQ_def)
    apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff)
    apply (frule NSconvergentD)
    apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfun_pow)
    apply (frule HNatInfinite_add_one)
    apply (drule bspec, assumption)
    apply (drule bspec, assumption)
    apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
    apply (simp add: hyperpow_add)
    apply (drule approx_mult_subst_SReal, assumption)
    apply (drule approx_trans3, assumption)
    apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
    done

    text{* standard version *}
    lemma LIMSEQ_realpow_zero: "[| 0 ≤ x; x < 1 |] ==> (%n. x ^ n) ----> 0"
    by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)

    lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0"
    apply (cut_tac a = a and x1 = "inverse x" in
            LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero])
    apply (auto simp add: divide_inverse power_inverse)
    apply (simp add: inverse_eq_divide pos_divide_less_eq)
    done

    text{*Limit of @{term "c^n"} for @{term"¦c¦ < 1"}*}

    lemma LIMSEQ_rabs_realpow_zero: "¦c¦ < 1 ==> (%n. ¦c¦ ^ n) ----> 0"
    by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero)

    lemma NSLIMSEQ_rabs_realpow_zero: "¦c¦ < 1 ==> (%n. ¦c¦ ^ n) ----NS> 0"
    by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric])

    lemma LIMSEQ_rabs_realpow_zero2: "¦c¦ < 1 ==> (%n. c ^ n) ----> 0"
    apply (rule LIMSEQ_rabs_zero [THEN iffD1])
    apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
    done

    lemma NSLIMSEQ_rabs_realpow_zero2: "¦c¦ < 1 ==> (%n. c ^ n) ----NS> 0"
    by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])

    subsection{*Hyperreals and Sequences*}

    text{*A bounded sequence is a finite hyperreal*}
    lemma NSBseq_HFinite_hypreal: "NSBseq X ==> star_n X : HFinite"
    by (auto intro!: bexI lemma_starrel_refl
                intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
                simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
                          Bseq_iff1a)

    text{*A sequence converging to zero defines an infinitesimal*}
    lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
          "X ----NS> 0 ==> star_n X : Infinitesimal"
    apply (simp add: NSLIMSEQ_def)
    apply (drule_tac x = whn in bspec)
    apply (simp add: HNatInfinite_whn)
    apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfun)
    done

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

    ML
    {*
    val Cauchy_def = thm"Cauchy_def";
    val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
    val LIMSEQ_iff = thm "LIMSEQ_iff";
    val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
    val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
    val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
    val Compl_less_set = thm "Compl_less_set";
    val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
    val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
    val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
    val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
    val NSLIMSEQ_const = thm "NSLIMSEQ_const";
    val LIMSEQ_const = thm "LIMSEQ_const";
    val NSLIMSEQ_add = thm "NSLIMSEQ_add";
    val LIMSEQ_add = thm "LIMSEQ_add";
    val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
    val LIMSEQ_mult = thm "LIMSEQ_mult";
    val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
    val LIMSEQ_minus = thm "LIMSEQ_minus";
    val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
    val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
    val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
    val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
    val LIMSEQ_diff = thm "LIMSEQ_diff";
    val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
    val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
    val LIMSEQ_inverse = thm "LIMSEQ_inverse";
    val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
    val LIMSEQ_divide = thm "LIMSEQ_divide";
    val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
    val LIMSEQ_unique = thm "LIMSEQ_unique";
    val limI = thm "limI";
    val nslimI = thm "nslimI";
    val lim_nslim_iff = thm "lim_nslim_iff";
    val convergentD = thm "convergentD";
    val convergentI = thm "convergentI";
    val NSconvergentD = thm "NSconvergentD";
    val NSconvergentI = thm "NSconvergentI";
    val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
    val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
    val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
    val subseq_Suc_iff = thm "subseq_Suc_iff";
    val monoseq_Suc = thm "monoseq_Suc";
    val monoI1 = thm "monoI1";
    val monoI2 = thm "monoI2";
    val mono_SucI1 = thm "mono_SucI1";
    val mono_SucI2 = thm "mono_SucI2";
    val BseqD = thm "BseqD";
    val BseqI = thm "BseqI";
    val Bseq_iff = thm "Bseq_iff";
    val Bseq_iff1a = thm "Bseq_iff1a";
    val NSBseqD = thm "NSBseqD";
    val NSBseqI = thm "NSBseqI";
    val Bseq_NSBseq = thm "Bseq_NSBseq";
    val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
    val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
    val NSBseq_Bseq = thm "NSBseq_Bseq";
    val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
    val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
    val convergent_Bseq = thm "convergent_Bseq";
    val Bseq_isUb = thm "Bseq_isUb";
    val Bseq_isLub = thm "Bseq_isLub";
    val NSBseq_isUb = thm "NSBseq_isUb";
    val NSBseq_isLub = thm "NSBseq_isLub";
    val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
    val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
    val Bseq_mono_convergent = thm "Bseq_mono_convergent";
    val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
    val convergent_minus_iff = thm "convergent_minus_iff";
    val Bseq_minus_iff = thm "Bseq_minus_iff";
    val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
    val Bseq_iff2 = thm "Bseq_iff2";
    val Bseq_iff3 = thm "Bseq_iff3";
    val BseqI2 = thm "BseqI2";
    val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
    val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
    val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
    val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
    val SUP_rabs_subseq = thm "SUP_rabs_subseq";
    val Cauchy_Bseq = thm "Cauchy_Bseq";
    val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
    val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
    val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
    val NSLIMSEQ_le = thm "NSLIMSEQ_le";
    val LIMSEQ_le = thm "LIMSEQ_le";
    val LIMSEQ_le_const = thm "LIMSEQ_le_const";
    val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
    val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
    val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
    val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
    val LIMSEQ_Suc = thm "LIMSEQ_Suc";
    val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
    val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
    val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
    val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
    val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
    val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
    val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
    val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
    val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
    val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
    val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
    val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
    val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
    val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
    val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
    val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
    val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
    val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
    val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
    val LIMSEQ_pow = thm "LIMSEQ_pow";
    val Bseq_realpow = thm "Bseq_realpow";
    val monoseq_realpow = thm "monoseq_realpow";
    val convergent_realpow = thm "convergent_realpow";
    val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
    *}

    end

lemma SEQ_Infinitesimal:

      (*f* (%n. inverse (real (Suc n)))) whn ∈ Infinitesimal

### LIMSEQ and NSLIMSEQ

lemma LIMSEQ_iff:

      X ----> L = (∀r>0. ∃no. ∀n. no ≤ n --> ¦X n + - L¦ < r)

lemma NSLIMSEQ_iff:

      X ----NS> L = (∀N∈HNatInfinite. (*f* X) N ≈ star_of L)

lemma LIMSEQ_NSLIMSEQ:

      X ----> L ==> X ----NS> L

lemma lemma_NSLIMSEQ1:

      ∀n. n ≤ f n ==> {n. f n = 0} = {0} ∨ {n. f n = 0} = {}

lemma lemma_NSLIMSEQ2:

      {n. f n ≤ Suc u} = {n. f n ≤ u} ∪ {n. f n = Suc u}

lemma lemma_NSLIMSEQ3:

      ∀n. n ≤ f n ==> {n. f n = Suc u} ⊆ {n. n ≤ Suc u}

lemma NSLIMSEQ_finite_set:

      ∀n. n ≤ f n ==> finite {n. f n ≤ u}

lemma Compl_less_set:

      - {n. u < f n} = {n. f n ≤ u}

lemma FreeUltrafilterNat_NSLIMSEQ:

      ∀n. n ≤ f n ==> {n. u < f n} ∈ \<U>

lemma HNatInfinite_NSLIMSEQ:

      ∀n. n ≤ f n ==> star_n f ∈ HNatInfinite

lemma lemmaLIM:

      {n. X (f n) + - L = Y n} ∩ {n. ¦Y n¦ < r} ⊆ {n. ¦X (f n) + - L¦ < r}

lemma lemmaLIM2:

      {n. ¦X (f n) + - L¦ < r} ∩ {n. r ≤ ¦X (f n) + - L¦} = {}

lemma lemmaLIM3:

      [| 0 < r; ∀n. r ≤ ¦X (f n) + - L¦; (*f* X) (star_n f) + - star_of L ≈ 0 |]
      ==> False

lemma NSLIMSEQ_LIMSEQ:

      X ----NS> L ==> X ----> L

theorem LIMSEQ_NSLIMSEQ_iff:

      f ----> L = f ----NS> L

### Theorems About Sequences

lemma NSLIMSEQ_const:

      (%n. k) ----NS> k

lemma LIMSEQ_const:

      (%n. k) ----> k

lemma NSLIMSEQ_add:

      [| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b

lemma LIMSEQ_add:

      [| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b

lemma LIMSEQ_add_const:

      f ----> a ==> (%n. f n + b) ----> a + b

lemma NSLIMSEQ_add_const:

      f ----NS> a ==> (%n. f n + b) ----NS> a + b

lemma NSLIMSEQ_mult:

      [| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b

lemma LIMSEQ_mult:

      [| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b

lemma NSLIMSEQ_minus:

      X ----NS> a ==> (%n. - X n) ----NS> - a

lemma LIMSEQ_minus:

      X ----> a ==> (%n. - X n) ----> - a

lemma LIMSEQ_minus_cancel:

      (%n. - X n) ----> - a ==> X ----> a

lemma NSLIMSEQ_minus_cancel:

      (%n. - X n) ----NS> - a ==> X ----NS> a

lemma NSLIMSEQ_add_minus:

      [| X ----NS> a; Y ----NS> b |] ==> (%n. X n + - Y n) ----NS> a + - b

lemma LIMSEQ_add_minus:

      [| X ----> a; Y ----> b |] ==> (%n. X n + - Y n) ----> a + - b

lemma LIMSEQ_diff:

      [| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b

lemma NSLIMSEQ_diff:

      [| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b

lemma LIMSEQ_diff_const:

      f ----> a ==> (%n. f n - b) ----> a - b

lemma NSLIMSEQ_diff_const:

      f ----NS> a ==> (%n. f n - b) ----NS> a - b

lemma NSLIMSEQ_inverse:

      [| X ----NS> a; a ≠ 0 |] ==> (%n. inverse (X n)) ----NS> inverse a

lemma LIMSEQ_inverse:

      [| X ----> a; a ≠ 0 |] ==> (%n. inverse (X n)) ----> inverse a

lemma NSLIMSEQ_mult_inverse:

      [| X ----NS> a; Y ----NS> b; b ≠ 0 |] ==> (%n. X n / Y n) ----NS> a / b

lemma LIMSEQ_divide:

      [| X ----> a; Y ----> b; b ≠ 0 |] ==> (%n. X n / Y n) ----> a / b

lemma NSLIMSEQ_unique:

      [| X ----NS> a; X ----NS> b |] ==> a = b

lemma LIMSEQ_unique:

      [| X ----> a; X ----> b |] ==> a = b

lemma LIMSEQ_setsum:

      (!!n. n ∈ S ==> X n ----> L n) ==> (%m. ∑n∈S. X n m) ----> setsum L S

lemma LIMSEQ_setprod:

      (!!n. n ∈ S ==> X n ----> L n) ==> (%m. ∏n∈S. X n m) ----> setprod L S

lemma LIMSEQ_ignore_initial_segment:

      f ----> a ==> (%n. f (n + k)) ----> a

lemma LIMSEQ_offset:

      (%x. f (x + k)) ----> a ==> f ----> a

lemma LIMSEQ_diff_approach_zero:

      [| g ----> L; (%x. f x - g x) ----> 0 |] ==> f ----> L

lemma LIMSEQ_diff_approach_zero2:

      [| f ----> L; (%x. f x - g x) ----> 0 |] ==> g ----> L

### Nslim and Lim

lemma limI:

      X ----> L ==> lim X = L

lemma nslimI:

      X ----NS> L ==> nslim X = L

lemma lim_nslim_iff:

      lim X = nslim X

### Convergence

lemma convergentD:

      convergent X ==> ∃L. X ----> L

lemma convergentI:

      X ----> L ==> convergent X

lemma NSconvergentD:

      NSconvergent X ==> ∃L. X ----NS> L

lemma NSconvergentI:

      X ----NS> L ==> NSconvergent X

lemma convergent_NSconvergent_iff:

      convergent X = NSconvergent X

lemma NSconvergent_NSLIMSEQ_iff:

      NSconvergent X = X ----NS> nslim X

lemma convergent_LIMSEQ_iff:

      convergent X = X ----> lim X

lemma subseq_Suc_iff:

      subseq f = (∀n. f n < f (Suc n))

### Monotonicity

lemma monoseq_Suc:

      monoseq X = ((∀n. X n ≤ X (Suc n)) ∨ (∀n. X (Suc n) ≤ X n))

lemma monoI1:

      ∀m n. m ≤ n --> X m ≤ X n ==> monoseq X

lemma monoI2:

      ∀m n. m ≤ n --> X n ≤ X m ==> monoseq X

lemma mono_SucI1:

      ∀n. X n ≤ X (Suc n) ==> monoseq X

lemma mono_SucI2:

      ∀n. X (Suc n) ≤ X n ==> monoseq X

### Bounded Sequence

lemma BseqD:

      Bseq X ==> ∃K>0. ∀n. ¦X n¦ ≤ K

lemma BseqI:

      [| 0 < K; ∀n. ¦X n¦ ≤ K |] ==> Bseq X

lemma lemma_NBseq_def:

      (∃K>0. ∀n. ¦X n¦ ≤ K) = (∃N. ∀n. ¦X n¦ ≤ real (Suc N))

lemma Bseq_iff:

      Bseq X = (∃N. ∀n. ¦X n¦ ≤ real (Suc N))

lemma lemma_NBseq_def2:

      (∃K>0. ∀n. ¦X n¦ ≤ K) = (∃N. ∀n. ¦X n¦ < real (Suc N))

lemma Bseq_iff1a:

      Bseq X = (∃N. ∀n. ¦X n¦ < real (Suc N))

lemma NSBseqD:

      [| NSBseq X; N ∈ HNatInfinite |] ==> (*f* X) N ∈ HFinite

lemma NSBseqI:

      ∀N∈HNatInfinite. (*f* X) N ∈ HFinite ==> NSBseq X

lemma lemma_Bseq:

      ∀n. ¦X n¦ ≤ K ==> ∀n. ¦X (f n)¦ ≤ K

lemma Bseq_NSBseq:

      Bseq X ==> NSBseq X

lemma lemmaNSBseq:

      ∀K>0. ∃n. K < ¦X n¦ ==> ∀N. ∃n. real (Suc N) < ¦X n¦

lemma lemmaNSBseq2:

      ∀K>0. ∃n. K < ¦X n¦ ==> ∃f. ∀N. real (Suc N) < ¦X (f N)¦

lemma real_seq_to_hypreal_HInfinite:

      ∀N. real (Suc N) < ¦X (f N)¦ ==> star_n (X o f) ∈ HInfinite

lemma lemma_finite_NSBseq:

      {n. f n ≤ Suc u ∧ real (Suc n) < ¦X (f n)¦}
      ⊆ {n. f n ≤ u ∧ real (Suc n) < ¦X (f n)¦} ∪ {n. real (Suc n) < ¦X (Suc u)¦}

lemma lemma_finite_NSBseq2:

      finite {n. f n ≤ u ∧ real (Suc n) < ¦X (f n)¦}

lemma HNatInfinite_skolem_f:

      ∀N. real (Suc N) < ¦X (f N)¦ ==> star_n f ∈ HNatInfinite

lemma NSBseq_Bseq:

      NSBseq X ==> Bseq X

lemma Bseq_NSBseq_iff:

      Bseq X = NSBseq X

lemma NSconvergent_NSBseq:

      NSconvergent X ==> NSBseq X

lemma convergent_Bseq:

      convergent X ==> Bseq X

### Upper Bounds and Lubs of Bounded Sequences

lemma Bseq_isUb:

      Bseq X ==> ∃U. isUb UNIV {x. ∃n. X n = x} U

lemma Bseq_isLub:

      Bseq X ==> ∃U. isLub UNIV {x. ∃n. X n = x} U

lemma NSBseq_isUb:

      NSBseq X ==> ∃U. isUb UNIV {x. ∃n. X n = x} U

lemma NSBseq_isLub:

      NSBseq X ==> ∃U. isLub UNIV {x. ∃n. X n = x} U

### A Bounded and Monotonic Sequence Converges

lemma lemma_converg1:

      [| ∀m n. m ≤ n --> X m ≤ X n; isLub UNIV {x. ∃n. X n = x} (X ma) |]
      ==> ∀n≥ma. X n = X ma

lemma Bmonoseq_LIMSEQ:

      ∀n≥m. X n = X m ==> ∃L. X ----> L

lemma Bmonoseq_NSLIMSEQ:

      ∀n≥m. X n = X m ==> ∃L. X ----NS> L

lemma lemma_converg2:

      [| ∀m. X m ≠ U; isLub UNIV {x. ∃n. X n = x} U |] ==> ∀m. X m < U

lemma lemma_converg3:

      ∀m. X m ≤ U ==> isUb UNIV {x. ∃n. X n = x} U

lemma lemma_converg4:

      [| ∀m. X m ≠ U; isLub UNIV {x. ∃n. X n = x} U; 0 < T; U + - T < U |]
      ==> ∃m. U + - T < X m ∧ X m < U

lemma Bseq_mono_convergent:

      [| Bseq X; ∀m n. m ≤ n --> X m ≤ X n |] ==> convergent X

lemma NSBseq_mono_NSconvergent:

      [| NSBseq X; ∀m n. m ≤ n --> X m ≤ X n |] ==> NSconvergent X

lemma convergent_minus_iff:

      convergent X = convergent (%n. - X n)

lemma Bseq_minus_iff:

      Bseq (%n. - X n) = Bseq X

lemma Bseq_monoseq_convergent:

      [| Bseq X; monoseq X |] ==> convergent X

### A Few More Equivalence Theorems for Boundedness

lemma Bseq_iff2:

      Bseq X = (∃k>0. ∃x. ∀n. ¦X n + - x¦ ≤ k)

lemma Bseq_iff3:

      Bseq X = (∃k>0. ∃N. ∀n. ¦X n + - X N¦ ≤ k)

lemma BseqI2:

      ∀n. k ≤ f n ∧ f n ≤ K ==> Bseq f

### Equivalence Between NS and Standard Cauchy Sequences

#### Standard Implies Nonstandard

lemma lemmaCauchy1:

      star_n x ∈ HNatInfinite ==> {n. M ≤ x n} ∈ \<U>

lemma lemmaCauchy2:

      {n. ∀m n. M ≤ m ∧ M ≤ n --> ¦X m + - X n¦ < u} ∩ {n. M ≤ xa n} ∩ {n. M ≤ x n}
      ⊆ {n. ¦X (xa n) + - X (x n)¦ < u}

lemma Cauchy_NSCauchy:

      Cauchy X ==> NSCauchy X

#### Nonstandard Implies Standard

lemma NSCauchy_Cauchy:

      NSCauchy X ==> Cauchy X

theorem NSCauchy_Cauchy_iff:

      NSCauchy X = Cauchy X

lemma lemmaCauchy:

      ∀n≥M. ¦X M + - X n¦ < 1 ==> ∀n≥M. ¦X n¦ < 1 + ¦X M¦

lemma less_Suc_cancel_iff:

      (n < Suc M) = (n ≤ M)

lemma SUP_rabs_subseq:

      ∃m≤M. ∀n≤M. ¦X n¦ ≤ ¦X m¦

lemma lemma_Nat_covered:

      [| ∀m≤M. P M m; ∀m≥M. P M m |] ==> ∀m. P M m

lemma lemma_trans1:

      [| ∀n≤M. ¦X n¦ ≤ a; a < b |] ==> ∀n≤M. ¦X n¦ ≤ b

lemma lemma_trans2:

      [| ∀n≥M. ¦X n¦ < a; a < b |] ==> ∀n≥M. ¦X n¦ ≤ b

lemma lemma_trans3:

      [| ∀n≤M. ¦X n¦ ≤ a; a = b |] ==> ∀n≤M. ¦X n¦ ≤ b

lemma lemma_trans4:

      ∀n≥M. ¦X n¦ < a ==> ∀n≥M. ¦X n¦ ≤ a

lemma Cauchy_Bseq:

      Cauchy X ==> Bseq X

lemma NSCauchy_NSBseq:

      NSCauchy X ==> NSBseq X

lemma NSCauchy_NSconvergent_iff:

      NSCauchy X = NSconvergent X

lemma Cauchy_convergent_iff:

      Cauchy X = convergent X

lemma NSLIMSEQ_le:

      [| f ----NS> l; g ----NS> m; ∃N. ∀n. N ≤ n --> f n ≤ g n |] ==> l ≤ m

lemma LIMSEQ_le:

      [| f ----> l; g ----> m; ∃N. ∀n. N ≤ n --> f n ≤ g n |] ==> l ≤ m

lemma LIMSEQ_le_const:

      [| X ----> r; ∀n. a ≤ X n |] ==> a ≤ r

lemma NSLIMSEQ_le_const:

      [| X ----NS> r; ∀n. a ≤ X n |] ==> a ≤ r

lemma LIMSEQ_le_const2:

      [| X ----> r; ∀n. X n ≤ a |] ==> r ≤ a

lemma NSLIMSEQ_le_const2:

      [| X ----NS> r; ∀n. X n ≤ a |] ==> r ≤ a

lemma NSLIMSEQ_Suc:

      f ----NS> l ==> (%n. f (Suc n)) ----NS> l

lemma LIMSEQ_Suc:

      f ----> l ==> (%n. f (Suc n)) ----> l

lemma NSLIMSEQ_imp_Suc:

      (%n. f (Suc n)) ----NS> l ==> f ----NS> l

lemma LIMSEQ_imp_Suc:

      (%n. f (Suc n)) ----> l ==> f ----> l

lemma LIMSEQ_Suc_iff:

      (%n. f (Suc n)) ----> l = f ----> l

lemma NSLIMSEQ_Suc_iff:

      (%n. f (Suc n)) ----NS> l = f ----NS> l

lemma LIMSEQ_rabs_zero:

      (%n. ¦f n¦) ----> 0 = f ----> 0

lemma NSLIMSEQ_rabs_zero:

      (%n. ¦f n¦) ----NS> 0 = f ----NS> 0

lemma NSLIMSEQ_imp_rabs:

      f ----NS> l ==> (%n. ¦f n¦) ----NS> ¦l¦

lemma LIMSEQ_imp_rabs:

      f ----> l ==> (%n. ¦f n¦) ----> ¦l¦

lemma LIMSEQ_inverse_zero:

      ∀y. ∃N. ∀n. N ≤ n --> y < f n ==> (%n. inverse (f n)) ----> 0

lemma NSLIMSEQ_inverse_zero:

      ∀y. ∃N. ∀n. N ≤ n --> y < f n ==> (%n. inverse (f n)) ----NS> 0

lemma LIMSEQ_inverse_real_of_nat:

      (%n. inverse (real (Suc n))) ----> 0

lemma NSLIMSEQ_inverse_real_of_nat:

      (%n. inverse (real (Suc n))) ----NS> 0

lemma LIMSEQ_inverse_real_of_nat_add:

      (%n. r + inverse (real (Suc n))) ----> r

lemma NSLIMSEQ_inverse_real_of_nat_add:

      (%n. r + inverse (real (Suc n))) ----NS> r

lemma LIMSEQ_inverse_real_of_nat_add_minus:

      (%n. r + - inverse (real (Suc n))) ----> r

lemma NSLIMSEQ_inverse_real_of_nat_add_minus:

      (%n. r + - inverse (real (Suc n))) ----NS> r

lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:

      (%n. r * (1 + - inverse (real (Suc n)))) ----> r

lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult:

      (%n. r * (1 + - inverse (real (Suc n)))) ----NS> r

lemma NSLIMSEQ_pow:

      X ----NS> a ==> (%n. X n ^ m) ----NS> a ^ m

lemma LIMSEQ_pow:

      X ----> a ==> (%n. X n ^ m) ----> a ^ m

lemma Bseq_realpow:

      [| 0 ≤ x; x ≤ 1 |] ==> Bseq (op ^ x)

lemma monoseq_realpow:

      [| 0 ≤ x; x ≤ 1 |] ==> monoseq (op ^ x)

lemma convergent_realpow:

      [| 0 ≤ x; x ≤ 1 |] ==> convergent (op ^ x)

lemma NSLIMSEQ_realpow_zero:

      [| 0 ≤ x; x < 1 |] ==> op ^ x ----NS> 0

lemma LIMSEQ_realpow_zero:

      [| 0 ≤ x; x < 1 |] ==> op ^ x ----> 0

lemma LIMSEQ_divide_realpow_zero:

      1 < x ==> (%n. a / x ^ n) ----> 0

lemma LIMSEQ_rabs_realpow_zero:

      ¦c¦ < 1 ==> op ^ ¦c¦ ----> 0

lemma NSLIMSEQ_rabs_realpow_zero:

      ¦c¦ < 1 ==> op ^ ¦c¦ ----NS> 0

lemma LIMSEQ_rabs_realpow_zero2:

      ¦c¦ < 1 ==> op ^ c ----> 0

lemma NSLIMSEQ_rabs_realpow_zero2:

      ¦c¦ < 1 ==> op ^ c ----NS> 0

### Hyperreals and Sequences

lemma NSBseq_HFinite_hypreal:

      NSBseq X ==> star_n X ∈ HFinite

lemma NSLIMSEQ_zero_Infinitesimal_hypreal:

      X ----NS> 0 ==> star_n X ∈ Infinitesimal