Theory "sum_num"

Signature

Definitions

SUM_def

⊢ (∀f. SUM 0 f = 0) ∧ ∀m f. SUM (SUC m) f = SUM m f + f m

Theorems

GSUM_ind

⊢ ∀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

GSUM_def

⊢ (∀n f. GSUM (n,0) f = 0) ∧
  ∀n m f. GSUM (n,SUC m) f = GSUM (n,m) f + f (n + m)

GSUM_def_compute

⊢ (∀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_1

⊢ ∀m f. GSUM (m,1) f = f m

GSUM_ADD

⊢ ∀p m n f. GSUM (p,m + n) f = GSUM (p,m) f + GSUM (p + m,n) f

GSUM_ZERO

⊢ ∀p n f. (∀m. p ≤ m ∧ m < p + n ⇒ f m = 0) ⇔ GSUM (p,n) f = 0

GSUM_MONO

⊢ ∀p m n f. m ≤ n ∧ f (p + n) ≠ 0 ⇒ GSUM (p,m) f < GSUM (p,SUC n) f

GSUM_LESS

⊢ ∀p m n f.
      (∃q. m + p ≤ q ∧ q < n + p ∧ f q ≠ 0) ⇔ GSUM (p,m) f < GSUM (p,n) f

GSUM_EQUAL

⊢ ∀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

⊢ ∀p n f g. (∀x. p ≤ x ∧ x < p + n ⇒ f x = g x) ⇒ GSUM (p,n) f = GSUM (p,n) g

SUM_def_compute

⊢ (∀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))

SUM

⊢ ∀m f. SUM m f = GSUM (0,m) f

SUM_1

⊢ ∀f. SUM 1 f = f 0

SUM_MONO

⊢ ∀m n f. m ≤ n ∧ f n ≠ 0 ⇒ SUM m f < SUM (SUC n) f

SUM_LESS

⊢ ∀m n f. (∃q. m ≤ q ∧ q < n ∧ f q ≠ 0) ⇔ SUM m f < SUM n f

SUM_EQUAL

⊢ ∀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_FUN_EQUAL

⊢ ∀f g. (∀x. x < n ⇒ f x = g x) ⇒ SUM n f = SUM n g

SUM_ZERO

⊢ ∀n f. (∀m. m < n ⇒ f m = 0) ⇔ SUM n f = 0

SUM_FOLDL

⊢ ∀n f. SUM n f = FOLDL (λx n. f n + x) 0 (COUNT_LIST n)