Structure seqTheory

signature seqTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val convergent : thm
    val lim : thm
    val mono : thm
    val mono_decreasing_def : thm
    val mono_increasing_def : thm
    val subseq : thm
    val suminf : thm
    val summable : thm
    val sums : thm
    val tends_num_real : thm
  
  (*  Theorems  *)
    val ABS_NEG_LEMMA : thm
    val BOLZANO_LEMMA : thm
    val BOLZANO_LEMMA_ALT : thm
    val GP : thm
    val GP_FINITE : thm
    val HARMONIC_SERIES_POW_2 : thm
    val INCREASING_SEQ : thm
    val LE_SEQ_IMP_LE_LIM : thm
    val LIM_SEQUENTIALLY_SEQ : thm
    val LIM_SEQUENTIALLY_SEQ' : thm
    val MAX_LEMMA : thm
    val MONO_SUC : thm
    val NEST_LEMMA : thm
    val NEST_LEMMA_UNIQ : thm
    val POS_SUMMABLE : thm
    val POW_HALF_MONO : thm
    val POW_HALF_SER : thm
    val POW_HALF_SMALL : thm
    val SEQ : thm
    val SEQ_ABS : thm
    val SEQ_ABS_IMP : thm
    val SEQ_ADD : thm
    val SEQ_BCONV : thm
    val SEQ_BOUNDED : thm
    val SEQ_BOUNDED_2 : thm
    val SEQ_CAUCHY : thm
    val SEQ_CBOUNDED : thm
    val SEQ_CONST : thm
    val SEQ_DIRECT : thm
    val SEQ_DIV : thm
    val SEQ_ICONV : thm
    val SEQ_INV : thm
    val SEQ_INV0 : thm
    val SEQ_LE : thm
    val SEQ_LE_IMP_LIM_LE : thm
    val SEQ_LE_MONO : thm
    val SEQ_LIM : thm
    val SEQ_MONOSUB : thm
    val SEQ_MONO_LE : thm
    val SEQ_MUL : thm
    val SEQ_NEG : thm
    val SEQ_NEG_BOUNDED : thm
    val SEQ_NEG_CONV : thm
    val SEQ_POWER : thm
    val SEQ_POWER_ABS : thm
    val SEQ_REAL_SUM_IMAGE : thm
    val SEQ_SANDWICH : thm
    val SEQ_SBOUNDED : thm
    val SEQ_SUB : thm
    val SEQ_SUBLE : thm
    val SEQ_SUC : thm
    val SEQ_UNIQ : thm
    val SER_0 : thm
    val SER_ABS : thm
    val SER_ACONV : thm
    val SER_ADD : thm
    val SER_CAUCHY : thm
    val SER_CDIV : thm
    val SER_CMUL : thm
    val SER_COMPAR : thm
    val SER_COMPARA : thm
    val SER_GROUP : thm
    val SER_LE : thm
    val SER_LE2 : thm
    val SER_NEG : thm
    val SER_OFFSET : thm
    val SER_PAIR : thm
    val SER_POS : thm
    val SER_POS_COMPARE : thm
    val SER_POS_LE : thm
    val SER_POS_LT : thm
    val SER_POS_LT_PAIR : thm
    val SER_POS_MONO : thm
    val SER_RATIO : thm
    val SER_SUB : thm
    val SER_ZERO : thm
    val SUBSEQ_SUC : thm
    val SUMINF_2D : thm
    val SUMINF_ADD : thm
    val SUMINF_POS : thm
    val SUMMABLE_LE : thm
    val SUMMABLE_SUM : thm
    val SUMS_EQ : thm
    val SUMS_ZERO : thm
    val SUM_CONST_R : thm
    val SUM_SUMMABLE : thm
    val SUM_UNIQ : thm
    val TRANSFORM_2D_NUM : thm
    val TRIANGLE_2D_NUM : thm
    val cauchy : thm
    val mono_decreasing_suc : thm
    val mono_increasing_converges_to_sup : thm
    val mono_increasing_suc : thm
    val suminf_univ : thm
    val summable_univ : thm
    val sums_univ : thm
  
  val seq_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real_topology] Parent theory of "seq"
   
   [convergent]  Definition
      
      ⊢ ∀f. convergent f ⇔ ∃l. f --> l
   
   [lim]  Definition
      
      ⊢ ∀f. lim f = @l. f --> l
   
   [mono]  Definition
      
      ⊢ ∀f. mono f ⇔ (∀m n. m ≤ n ⇒ f m ≤ f n) ∨ ∀m n. m ≤ n ⇒ f m ≥ f n
   
   [mono_decreasing_def]  Definition
      
      ⊢ ∀f. mono_decreasing f ⇔ ∀m n. m ≤ n ⇒ f n ≤ f m
   
   [mono_increasing_def]  Definition
      
      ⊢ ∀f. mono_increasing f ⇔ ∀m n. m ≤ n ⇒ f m ≤ f n
   
   [subseq]  Definition
      
      ⊢ ∀f. subseq f ⇔ ∀m n. m < n ⇒ f m < f n
   
   [suminf]  Definition
      
      ⊢ ∀f. suminf f = @s. f sums s
   
   [summable]  Definition
      
      ⊢ ∀f. summable f ⇔ ∃s. f sums s
   
   [sums]  Definition
      
      ⊢ ∀f s. f sums s ⇔ (λn. sum (0,n) f) --> s
   
   [tends_num_real]  Definition
      
      ⊢ ∀x x0. x --> x0 ⇔ (x tends x0) (mtop mr1,$>=)
   
   [ABS_NEG_LEMMA]  Theorem
      
      ⊢ ∀c. c ≤ 0 ⇒ ∀x y. abs x ≤ c * abs y ⇒ (x = 0)
   
   [BOLZANO_LEMMA]  Theorem
      
      ⊢ ∀P. (∀a b c. a ≤ b ∧ b ≤ c ∧ P (a,b) ∧ P (b,c) ⇒ P (a,c)) ∧
            (∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b − a < d ⇒ P (a,b)) ⇒
            ∀a b. a ≤ b ⇒ P (a,b)
   
   [BOLZANO_LEMMA_ALT]  Theorem
      
      ⊢ ∀P. (∀a b c. a ≤ b ∧ b ≤ c ∧ P a b ∧ P b c ⇒ P a c) ∧
            (∀x. ∃d. 0 < d ∧ ∀a b. a ≤ x ∧ x ≤ b ∧ b − a < d ⇒ P a b) ⇒
            ∀a b. a ≤ b ⇒ P a b
   
   [GP]  Theorem
      
      ⊢ ∀x. abs x < 1 ⇒ (λn. x pow n) sums (1 − x)⁻¹
   
   [GP_FINITE]  Theorem
      
      ⊢ ∀x. x ≠ 1 ⇒ ∀n. sum (0,n) (λn. x pow n) = (x pow n − 1) / (x − 1)
   
   [HARMONIC_SERIES_POW_2]  Theorem
      
      ⊢ summable (λn. (&SUC n)² ⁻¹)
   
   [INCREASING_SEQ]  Theorem
      
      ⊢ ∀f l.
          (∀n. f n ≤ f (SUC n)) ∧ (∀n. f n ≤ l) ∧
          (∀e. 0 < e ⇒ ∃n. l < f n + e) ⇒
          f --> l
   
   [LE_SEQ_IMP_LE_LIM]  Theorem
      
      ⊢ ∀x y f. (∀n. x ≤ f n) ∧ f --> y ⇒ x ≤ y
   
   [LIM_SEQUENTIALLY_SEQ]  Theorem
      
      ⊢ ∀s l. real_topology$--> s l sequentially ⇔ s --> l
   
   [LIM_SEQUENTIALLY_SEQ']  Theorem
      
      ⊢ ∀f. reallim sequentially f = lim f
   
   [MAX_LEMMA]  Theorem
      
      ⊢ ∀s N. ∃k. ∀n. n < N ⇒ abs (s n) < k
   
   [MONO_SUC]  Theorem
      
      ⊢ ∀f. mono f ⇔ (∀n. f (SUC n) ≥ f n) ∨ ∀n. f (SUC n) ≤ f n
   
   [NEST_LEMMA]  Theorem
      
      ⊢ ∀f g.
          (∀n. f (SUC n) ≥ f n) ∧ (∀n. g (SUC n) ≤ g n) ∧ (∀n. f n ≤ g n) ⇒
          ∃l m. l ≤ m ∧ ((∀n. f n ≤ l) ∧ f --> l) ∧ (∀n. m ≤ g n) ∧ g --> m
   
   [NEST_LEMMA_UNIQ]  Theorem
      
      ⊢ ∀f g.
          (∀n. f (SUC n) ≥ f n) ∧ (∀n. g (SUC n) ≤ g n) ∧ (∀n. f n ≤ g n) ∧
          (λn. f n − g n) --> 0 ⇒
          ∃l. ((∀n. f n ≤ l) ∧ f --> l) ∧ (∀n. l ≤ g n) ∧ g --> l
   
   [POS_SUMMABLE]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∃x. ∀n. sum (0,n) f ≤ x) ⇒ summable f
   
   [POW_HALF_MONO]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m
   
   [POW_HALF_SER]  Theorem
      
      ⊢ (λn. (1 / 2) pow (n + 1)) sums 1
   
   [POW_HALF_SMALL]  Theorem
      
      ⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e
   
   [SEQ]  Theorem
      
      ⊢ ∀x x0. x --> x0 ⇔ ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ abs (x n − x0) < e
   
   [SEQ_ABS]  Theorem
      
      ⊢ ∀f. (λn. abs (f n)) --> 0 ⇔ f --> 0
   
   [SEQ_ABS_IMP]  Theorem
      
      ⊢ ∀f l. f --> l ⇒ (λn. abs (f n)) --> abs l
   
   [SEQ_ADD]  Theorem
      
      ⊢ ∀x x0 y y0. x --> x0 ∧ y --> y0 ⇒ (λn. x n + y n) --> (x0 + y0)
   
   [SEQ_BCONV]  Theorem
      
      ⊢ ∀f. bounded (mr1,$>=) f ∧ mono f ⇒ convergent f
   
   [SEQ_BOUNDED]  Theorem
      
      ⊢ ∀s. bounded (mr1,$>=) s ⇔ ∃k. ∀n. abs (s n) < k
   
   [SEQ_BOUNDED_2]  Theorem
      
      ⊢ ∀f k k'. (∀n. k ≤ f n ∧ f n ≤ k') ⇒ bounded (mr1,$>=) f
   
   [SEQ_CAUCHY]  Theorem
      
      ⊢ ∀f. cauchy f ⇔ convergent f
   
   [SEQ_CBOUNDED]  Theorem
      
      ⊢ ∀f. cauchy f ⇒ bounded (mr1,$>=) f
   
   [SEQ_CONST]  Theorem
      
      ⊢ ∀k. (λx. k) --> k
   
   [SEQ_DIRECT]  Theorem
      
      ⊢ ∀f. subseq f ⇒ ∀N1 N2. ∃n. n ≥ N1 ∧ f n ≥ N2
   
   [SEQ_DIV]  Theorem
      
      ⊢ ∀x x0 y y0.
          x --> x0 ∧ y --> y0 ∧ y0 ≠ 0 ⇒ (λn. x n / y n) --> (x0 / y0)
   
   [SEQ_ICONV]  Theorem
      
      ⊢ ∀f. bounded (mr1,$>=) f ∧ (∀m n. m ≥ n ⇒ f m ≥ f n) ⇒ convergent f
   
   [SEQ_INV]  Theorem
      
      ⊢ ∀x x0. x --> x0 ∧ x0 ≠ 0 ⇒ (λn. (x n)⁻¹) --> x0⁻¹
   
   [SEQ_INV0]  Theorem
      
      ⊢ ∀f. (∀y. ∃N. ∀n. n ≥ N ⇒ f n > y) ⇒ (λn. (f n)⁻¹) --> 0
   
   [SEQ_LE]  Theorem
      
      ⊢ ∀f g l m. f --> l ∧ g --> m ∧ (∃N. ∀n. n ≥ N ⇒ f n ≤ g n) ⇒ l ≤ m
   
   [SEQ_LE_IMP_LIM_LE]  Theorem
      
      ⊢ ∀x y f. (∀n. f n ≤ x) ∧ f --> y ⇒ y ≤ x
   
   [SEQ_LE_MONO]  Theorem
      
      ⊢ ∀f x n. (∀n. f (n + 1) ≤ f n) ∧ f --> x ⇒ x ≤ f n
   
   [SEQ_LIM]  Theorem
      
      ⊢ ∀f. convergent f ⇔ f --> lim f
   
   [SEQ_MONOSUB]  Theorem
      
      ⊢ ∀s. ∃f. subseq f ∧ mono (λn. s (f n))
   
   [SEQ_MONO_LE]  Theorem
      
      ⊢ ∀f x n. (∀n. f n ≤ f (n + 1)) ∧ f --> x ⇒ f n ≤ x
   
   [SEQ_MUL]  Theorem
      
      ⊢ ∀x x0 y y0. x --> x0 ∧ y --> y0 ⇒ (λn. x n * y n) --> (x0 * y0)
   
   [SEQ_NEG]  Theorem
      
      ⊢ ∀x x0. x --> x0 ⇔ (λn. -x n) --> -x0
   
   [SEQ_NEG_BOUNDED]  Theorem
      
      ⊢ ∀f. bounded (mr1,$>=) (λn. -f n) ⇔ bounded (mr1,$>=) f
   
   [SEQ_NEG_CONV]  Theorem
      
      ⊢ ∀f. convergent f ⇔ convergent (λn. -f n)
   
   [SEQ_POWER]  Theorem
      
      ⊢ ∀c. abs c < 1 ⇒ (λn. c pow n) --> 0
   
   [SEQ_POWER_ABS]  Theorem
      
      ⊢ ∀c. abs c < 1 ⇒ (λn. abs c pow n) --> 0
   
   [SEQ_REAL_SUM_IMAGE]  Theorem
      
      ⊢ ∀s. FINITE s ⇒
            ∀f f'.
              (∀x. x ∈ s ⇒ (λn. f n x) --> f' x) ⇒
              (λn. SIGMA (f n) s) --> SIGMA f' s
   
   [SEQ_SANDWICH]  Theorem
      
      ⊢ ∀f g h l. f --> l ∧ h --> l ∧ (∀n. f n ≤ g n ∧ g n ≤ h n) ⇒ g --> l
   
   [SEQ_SBOUNDED]  Theorem
      
      ⊢ ∀s f. bounded (mr1,$>=) s ⇒ bounded (mr1,$>=) (λn. s (f n))
   
   [SEQ_SUB]  Theorem
      
      ⊢ ∀x x0 y y0. x --> x0 ∧ y --> y0 ⇒ (λn. x n − y n) --> (x0 − y0)
   
   [SEQ_SUBLE]  Theorem
      
      ⊢ ∀f. subseq f ⇒ ∀n. n ≤ f n
   
   [SEQ_SUC]  Theorem
      
      ⊢ ∀f l. f --> l ⇔ (λn. f (SUC n)) --> l
   
   [SEQ_UNIQ]  Theorem
      
      ⊢ ∀x x1 x2. x --> x1 ∧ x --> x2 ⇒ (x1 = x2)
   
   [SER_0]  Theorem
      
      ⊢ ∀f n. (∀m. n ≤ m ⇒ (f m = 0)) ⇒ f sums sum (0,n) f
   
   [SER_ABS]  Theorem
      
      ⊢ ∀f. summable (λn. abs (f n)) ⇒
            abs (suminf f) ≤ suminf (λn. abs (f n))
   
   [SER_ACONV]  Theorem
      
      ⊢ ∀f. summable (λn. abs (f n)) ⇒ summable f
   
   [SER_ADD]  Theorem
      
      ⊢ ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n + y n) sums (x0 + y0)
   
   [SER_CAUCHY]  Theorem
      
      ⊢ ∀f. summable f ⇔
            ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ⇒ abs (sum (m,n) f) < e
   
   [SER_CDIV]  Theorem
      
      ⊢ ∀x x0 c. x sums x0 ⇒ (λn. x n / c) sums (x0 / c)
   
   [SER_CMUL]  Theorem
      
      ⊢ ∀x x0 c. x sums x0 ⇒ (λn. c * x n) sums (c * x0)
   
   [SER_COMPAR]  Theorem
      
      ⊢ ∀f g. (∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ summable g ⇒ summable f
   
   [SER_COMPARA]  Theorem
      
      ⊢ ∀f g.
          (∃N. ∀n. n ≥ N ⇒ abs (f n) ≤ g n) ∧ summable g ⇒
          summable (λk. abs (f k))
   
   [SER_GROUP]  Theorem
      
      ⊢ ∀f k. summable f ∧ 0 < k ⇒ (λn. sum (n * k,k) f) sums suminf f
   
   [SER_LE]  Theorem
      
      ⊢ ∀f g.
          (∀n. f n ≤ g n) ∧ summable f ∧ summable g ⇒ suminf f ≤ suminf g
   
   [SER_LE2]  Theorem
      
      ⊢ ∀f g.
          (∀n. abs (f n) ≤ g n) ∧ summable g ⇒
          summable f ∧ suminf f ≤ suminf g
   
   [SER_NEG]  Theorem
      
      ⊢ ∀x x0. x sums x0 ⇒ (λn. -x n) sums -x0
   
   [SER_OFFSET]  Theorem
      
      ⊢ ∀f. summable f ⇒ ∀k. (λn. f (n + k)) sums (suminf f − sum (0,k) f)
   
   [SER_PAIR]  Theorem
      
      ⊢ ∀f. summable f ⇒ (λn. sum (2 * n,2) f) sums suminf f
   
   [SER_POS]  Theorem
      
      ⊢ ∀f. summable f ∧ (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
   
   [SER_POS_COMPARE]  Theorem
      
      ⊢ ∀f g.
          (∀n. 0 ≤ f n) ∧ summable g ∧ (∀n. f n ≤ g n) ⇒
          summable f ∧ suminf f ≤ suminf g
   
   [SER_POS_LE]  Theorem
      
      ⊢ ∀f n. summable f ∧ (∀m. n ≤ m ⇒ 0 ≤ f m) ⇒ sum (0,n) f ≤ suminf f
   
   [SER_POS_LT]  Theorem
      
      ⊢ ∀f n. summable f ∧ (∀m. n ≤ m ⇒ 0 < f m) ⇒ sum (0,n) f < suminf f
   
   [SER_POS_LT_PAIR]  Theorem
      
      ⊢ ∀f n.
          summable f ∧ (∀d. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) ⇒
          sum (0,n) f < suminf f
   
   [SER_POS_MONO]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ mono (λn. sum (0,n) f)
   
   [SER_RATIO]  Theorem
      
      ⊢ ∀f c N.
          c < 1 ∧ (∀n. n ≥ N ⇒ abs (f (SUC n)) ≤ c * abs (f n)) ⇒
          summable f
   
   [SER_SUB]  Theorem
      
      ⊢ ∀x x0 y y0. x sums x0 ∧ y sums y0 ⇒ (λn. x n − y n) sums (x0 − y0)
   
   [SER_ZERO]  Theorem
      
      ⊢ ∀f. summable f ⇒ f --> 0
   
   [SUBSEQ_SUC]  Theorem
      
      ⊢ ∀f. subseq f ⇔ ∀n. f n < f (SUC n)
   
   [SUMINF_2D]  Theorem
      
      ⊢ ∀f g h.
          (∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
          BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
          UNCURRY f ∘ h sums suminf g
   
   [SUMINF_ADD]  Theorem
      
      ⊢ ∀f g.
          summable f ∧ summable g ⇒
          summable (λn. f n + g n) ∧
          (suminf f + suminf g = suminf (λn. f n + g n))
   
   [SUMINF_POS]  Theorem
      
      ⊢ ∀f. (∀n. 0 ≤ f n) ∧ summable f ⇒ 0 ≤ suminf f
   
   [SUMMABLE_LE]  Theorem
      
      ⊢ ∀f x. summable f ∧ (∀n. sum (0,n) f ≤ x) ⇒ suminf f ≤ x
   
   [SUMMABLE_SUM]  Theorem
      
      ⊢ ∀f. summable f ⇒ f sums suminf f
   
   [SUMS_EQ]  Theorem
      
      ⊢ ∀f x. f sums x ⇔ summable f ∧ (suminf f = x)
   
   [SUMS_ZERO]  Theorem
      
      ⊢ K 0 sums 0
   
   [SUM_CONST_R]  Theorem
      
      ⊢ ∀n r. sum (0,n) (K r) = &n * r
   
   [SUM_SUMMABLE]  Theorem
      
      ⊢ ∀f l. f sums l ⇒ summable f
   
   [SUM_UNIQ]  Theorem
      
      ⊢ ∀f x. f sums x ⇒ (x = suminf f)
   
   [TRANSFORM_2D_NUM]  Theorem
      
      ⊢ ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n
   
   [TRIANGLE_2D_NUM]  Theorem
      
      ⊢ ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n
   
   [cauchy]  Theorem
      
      ⊢ ∀f. cauchy f ⇔
            ∀e. 0 < e ⇒ ∃N. ∀m n. m ≥ N ∧ n ≥ N ⇒ abs (f m − f n) < e
   
   [mono_decreasing_suc]  Theorem
      
      ⊢ ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n
   
   [mono_increasing_converges_to_sup]  Theorem
      
      ⊢ ∀f r. mono_increasing f ∧ f --> r ⇒ (r = sup (IMAGE f 𝕌(:num)))
   
   [mono_increasing_suc]  Theorem
      
      ⊢ ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)
   
   [suminf_univ]  Theorem
      
      ⊢ ∀f. infsum 𝕌(:num) f = suminf f
   
   [summable_univ]  Theorem
      
      ⊢ ∀f. real_topology$summable 𝕌(:num) f ⇔ summable f
   
   [sums_univ]  Theorem
      
      ⊢ ∀f l. real_topology$sums f l 𝕌(:num) ⇔ f sums l
   
   
*)
end

HOL 4, Trindemossen-1