Structure sum_numTheory

signature sum_numTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val SUM_def : thm
  
  (*  Theorems  *)
    val GSUM_1 : thm
    val GSUM_ADD : thm
    val GSUM_EQUAL : thm
    val GSUM_FUN_EQUAL : thm
    val GSUM_LESS : thm
    val GSUM_MONO : thm
    val GSUM_ZERO : thm
    val GSUM_compute : thm
    val GSUM_def : thm
    val GSUM_ind : thm
    val SUM : thm
    val SUM_1 : thm
    val SUM_EQUAL : thm
    val SUM_FOLDL : thm
    val SUM_FUN_EQUAL : thm
    val SUM_LESS : thm
    val SUM_MONO : thm
    val SUM_ZERO : thm
    val SUM_compute : thm
  
  val sum_num_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "sum_num"
   
   [patternMatches] Parent theory of "sum_num"
   
   [SUM_def]  Definition
      
      ⊢ (∀f. SUM 0 f = 0) ∧ ∀m f. SUM (SUC m) f = SUM m f + f m
   
   [GSUM_1]  Theorem
      
      ⊢ ∀m f. GSUM (m,1) f = f m
   
   [GSUM_ADD]  Theorem
      
      ⊢ ∀p m n f. GSUM (p,m + n) f = GSUM (p,m) f + GSUM (p + m,n) f
   
   [GSUM_EQUAL]  Theorem
      
      ⊢ ∀p m n f.
            GSUM (p,m) f = GSUM (p,n) f ⇔
            m ≤ n ∧ (∀q. p + m ≤ q ∧ q < p + n ⇒ f q = 0) ∨
            n < m ∧ ∀q. p + n ≤ q ∧ q < p + m ⇒ f q = 0
   
   [GSUM_FUN_EQUAL]  Theorem
      
      ⊢ ∀p n f g.
            (∀x. p ≤ x ∧ x < p + n ⇒ f x = g x) ⇒
            GSUM (p,n) f = GSUM (p,n) g
   
   [GSUM_LESS]  Theorem
      
      ⊢ ∀p m n f.
            (∃q. m + p ≤ q ∧ q < n + p ∧ f q ≠ 0) ⇔
            GSUM (p,m) f < GSUM (p,n) f
   
   [GSUM_MONO]  Theorem
      
      ⊢ ∀p m n f. m ≤ n ∧ f (p + n) ≠ 0 ⇒ GSUM (p,m) f < GSUM (p,SUC n) f
   
   [GSUM_ZERO]  Theorem
      
      ⊢ ∀p n f. (∀m. p ≤ m ∧ m < p + n ⇒ f m = 0) ⇔ GSUM (p,n) f = 0
   
   [GSUM_compute]  Theorem
      
      ⊢ (∀n f. GSUM (n,0) f = 0) ∧
        (∀n m f.
             GSUM (n,NUMERAL (BIT1 m)) f =
             GSUM (n,NUMERAL (BIT1 m) − 1) f +
             f (n + (NUMERAL (BIT1 m) − 1))) ∧
        ∀n m f.
            GSUM (n,NUMERAL (BIT2 m)) f =
            GSUM (n,NUMERAL (BIT1 m)) f + f (n + NUMERAL (BIT1 m))
   
   [GSUM_def]  Theorem
      
      ⊢ (∀n f. GSUM (n,0) f = 0) ∧
        ∀n m f. GSUM (n,SUC m) f = GSUM (n,m) f + f (n + m)
   
   [GSUM_ind]  Theorem
      
      ⊢ ∀P.
            (∀n f. P (n,0) f) ∧ (∀n m f. P (n,m) f ⇒ P (n,SUC m) f) ⇒
            ∀v v1 v2. P (v,v1) v2
   
   [SUM]  Theorem
      
      ⊢ ∀m f. SUM m f = GSUM (0,m) f
   
   [SUM_1]  Theorem
      
      ⊢ ∀f. SUM 1 f = f 0
   
   [SUM_EQUAL]  Theorem
      
      ⊢ ∀m n f.
            SUM m f = SUM n f ⇔
            m ≤ n ∧ (∀q. m ≤ q ∧ q < n ⇒ f q = 0) ∨
            n < m ∧ ∀q. n ≤ q ∧ q < m ⇒ f q = 0
   
   [SUM_FOLDL]  Theorem
      
      ⊢ ∀n f. SUM n f = FOLDL (λx n. f n + x) 0 (COUNT_LIST n)
   
   [SUM_FUN_EQUAL]  Theorem
      
      ⊢ ∀f g. (∀x. x < n ⇒ f x = g x) ⇒ SUM n f = SUM n g
   
   [SUM_LESS]  Theorem
      
      ⊢ ∀m n f. (∃q. m ≤ q ∧ q < n ∧ f q ≠ 0) ⇔ SUM m f < SUM n f
   
   [SUM_MONO]  Theorem
      
      ⊢ ∀m n f. m ≤ n ∧ f n ≠ 0 ⇒ SUM m f < SUM (SUC n) f
   
   [SUM_ZERO]  Theorem
      
      ⊢ ∀n f. (∀m. m < n ⇒ f m = 0) ⇔ SUM n f = 0
   
   [SUM_compute]  Theorem
      
      ⊢ (∀f. SUM 0 f = 0) ∧
        (∀m f.
             SUM (NUMERAL (BIT1 m)) f =
             SUM (NUMERAL (BIT1 m) − 1) f + f (NUMERAL (BIT1 m) − 1)) ∧
        ∀m f.
            SUM (NUMERAL (BIT2 m)) f =
            SUM (NUMERAL (BIT1 m)) f + f (NUMERAL (BIT1 m))
   
   
*)
end

HOL 4, Kananaskis-13