# Structure sum_numTheory

Source File Identifier index Theory binding index

```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_def : thm
val GSUM_def_compute : 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_def_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

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

```

Source File Identifier index Theory binding index