Structure powserTheory

signature powserTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val diffs : thm

  (*  Theorems  *)
    val DIFFS_EQUIV : thm
    val DIFFS_LEMMA : thm
    val DIFFS_LEMMA2 : thm
    val DIFFS_NEG : thm
    val POWDIFF : thm
    val POWDIFF_LEMMA : thm
    val POWREV : thm
    val POWSER_INSIDE : thm
    val POWSER_INSIDEA : thm
    val TERMDIFF : thm
    val TERMDIFF_LEMMA1 : thm
    val TERMDIFF_LEMMA2 : thm
    val TERMDIFF_LEMMA3 : thm
    val TERMDIFF_LEMMA4 : thm
    val TERMDIFF_LEMMA5 : thm

  val powser_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [lim] Parent theory of "powser"

   [diffs]  Definition

      |- ∀c. diffs c = (λn. &SUC n * c (SUC n))

   [DIFFS_EQUIV]  Theorem

      |- ∀c x.
           summable (λn. diffs c n * x pow n) ⇒
           (λn. &n * (c n * x pow (n − 1))) sums
           suminf (λn. diffs c n * x pow n)

   [DIFFS_LEMMA]  Theorem

      |- ∀n c x.
           sum (0,n) (λn. diffs c n * x pow n) =
           sum (0,n) (λn. &n * (c n * x pow (n − 1))) +
           &n * (c n * x pow (n − 1))

   [DIFFS_LEMMA2]  Theorem

      |- ∀n c x.
           sum (0,n) (λn. &n * (c n * x pow (n − 1))) =
           sum (0,n) (λn. diffs c n * x pow n) − &n * (c n * x pow (n − 1))

   [DIFFS_NEG]  Theorem

      |- ∀c. diffs (λn. -c n) = (λn. -diffs c n)

   [POWDIFF]  Theorem

      |- ∀n x y.
           x pow SUC n − y pow SUC n =
           (x − y) * sum (0,SUC n) (λp. x pow p * y pow (n − p))

   [POWDIFF_LEMMA]  Theorem

      |- ∀n x y.
           sum (0,SUC n) (λp. x pow p * y pow (SUC n − p)) =
           y * sum (0,SUC n) (λp. x pow p * y pow (n − p))

   [POWREV]  Theorem

      |- ∀n x y.
           sum (0,SUC n) (λp. x pow p * y pow (n − p)) =
           sum (0,SUC n) (λp. x pow (n − p) * y pow p)

   [POWSER_INSIDE]  Theorem

      |- ∀f x z.
           summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
           summable (λn. f n * z pow n)

   [POWSER_INSIDEA]  Theorem

      |- ∀f x z.
           summable (λn. f n * x pow n) ∧ abs z < abs x ⇒
           summable (λn. abs (f n) * z pow n)

   [TERMDIFF]  Theorem

      |- ∀c k' x.
           summable (λn. c n * k' pow n) ∧
           summable (λn. diffs c n * k' pow n) ∧
           summable (λn. diffs (diffs c) n * k' pow n) ∧ abs x < abs k' ⇒
           ((λx. suminf (λn. c n * x pow n)) diffl
            suminf (λn. diffs c n * x pow n)) x

   [TERMDIFF_LEMMA1]  Theorem

      |- ∀m z h.
           sum (0,m) (λp. (z + h) pow (m − p) * z pow p − z pow m) =
           sum (0,m) (λp. z pow p * ((z + h) pow (m − p) − z pow (m − p)))

   [TERMDIFF_LEMMA2]  Theorem

      |- ∀z h n.
           h ≠ 0 ⇒
           (((z + h) pow n − z pow n) / h − &n * z pow (n − 1) =
            h *
            sum (0,n − 1)
              (λp.
                 z pow p *
                 sum (0,n − 1 − p)
                   (λq. (z + h) pow q * z pow (n − 2 − p − q))))

   [TERMDIFF_LEMMA3]  Theorem

      |- ∀z h n k'.
           h ≠ 0 ∧ abs z ≤ k' ∧ abs (z + h) ≤ k' ⇒
           abs (((z + h) pow n − z pow n) / h − &n * z pow (n − 1)) ≤
           &n * (&(n − 1) * (k' pow (n − 2) * abs h))

   [TERMDIFF_LEMMA4]  Theorem

      |- ∀f k' k.
           0 < k ∧ (∀h. 0 < abs h ∧ abs h < k ⇒ abs (f h) ≤ k' * abs h) ⇒
           (f -> 0) 0

   [TERMDIFF_LEMMA5]  Theorem

      |- ∀f g k.
           0 < k ∧ summable f ∧
           (∀h. 0 < abs h ∧ abs h < k ⇒ ∀n. abs (g h n) ≤ f n * abs h) ⇒
           ((λh. suminf (g h)) -> 0) 0


*)
end

HOL 4, Kananaskis-10