Structure iterateTheory
signature iterateTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FINREC_def : thm
val from_def : thm
val iterate : thm
val monoidal : thm
val neutral : thm
val nproduct : thm
val nsum : thm
val numseg : thm
val support : thm
(* Theorems *)
val ADD_SUB2 : thm
val ADD_SUBR : thm
val ADD_SUBR2 : thm
val BIGINTER_BIGUNION : thm
val BIGUNION_BIGINTER : thm
val BOUNDS_LINEAR : thm
val BOUNDS_LINEAR_0 : thm
val CARD_BIGUNION : thm
val CARD_EQ_NSUM : thm
val CARD_NUMSEG : thm
val CARD_NUMSEG_1 : thm
val CARD_NUMSEG_LEMMA : thm
val CARD_UNION_EQ : thm
val CHOOSE_SUBSET : thm
val CHOOSE_SUBSET_STRONG : thm
val COUNTABLE_FROM : thm
val COUNT_NUMSEG : thm
val DIFF_BIGINTER2 : thm
val DISJOINT_COUNT_FROM : thm
val DISJOINT_FROM_COUNT : thm
val DISJOINT_NUMSEG : thm
val EMPTY_BIGUNION : thm
val EXISTS_FINITE_SUBSET_IMAGE : thm
val FINITE_INDEX_NUMBERS : thm
val FINITE_INDEX_NUMSEG : thm
val FINITE_NUMSEG : thm
val FINITE_NUMSEG_LE : thm
val FINITE_NUMSEG_LT : thm
val FINITE_POWERSET : thm
val FINITE_RECURSION : thm
val FINITE_RESTRICT : thm
val FINITE_SUBSET_IMAGE : thm
val FINITE_SUPPORT : thm
val FINITE_SUPPORT_DELTA : thm
val FINREC_1_LEMMA : thm
val FINREC_EXISTS_LEMMA : thm
val FINREC_FUN : thm
val FINREC_FUN_LEMMA : thm
val FINREC_SUC_LEMMA : thm
val FINREC_UNIQUE_LEMMA : thm
val FINREC_compute : thm
val FORALL_FINITE_SUBSET_IMAGE : thm
val FROM_0 : thm
val FROM_INTER_NUMSEG : thm
val FROM_INTER_NUMSEG_GEN : thm
val FROM_INTER_NUMSEG_MAX : thm
val FROM_NOT_EMPTY : thm
val FUN_IN_IMAGE : thm
val HAS_SIZE_NUMSEG : thm
val HAS_SIZE_NUMSEG_1 : thm
val HAS_SIZE_NUMSEG_LE : thm
val HAS_SIZE_NUMSEG_LT : thm
val INFINITE_FROM : thm
val IN_FROM : thm
val IN_NUMSEG : thm
val IN_NUMSEG_0 : thm
val IN_SUPPORT : thm
val ITERATE_AND : thm
val ITERATE_BIJECTION : thm
val ITERATE_CASES : thm
val ITERATE_CLAUSES : thm
val ITERATE_CLAUSES_GEN : thm
val ITERATE_CLAUSES_NUMSEG : thm
val ITERATE_CLOSED : thm
val ITERATE_DELETE : thm
val ITERATE_DELTA : thm
val ITERATE_DIFF : thm
val ITERATE_DIFF_GEN : thm
val ITERATE_EQ : thm
val ITERATE_EQ_GENERAL : thm
val ITERATE_EQ_GENERAL_INVERSES : thm
val ITERATE_EQ_NEUTRAL : thm
val ITERATE_EXPAND_CASES : thm
val ITERATE_IMAGE : thm
val ITERATE_IMAGE_NONZERO : thm
val ITERATE_INCL_EXCL : thm
val ITERATE_INJECTION : thm
val ITERATE_ITERATE_PRODUCT : thm
val ITERATE_OP : thm
val ITERATE_OP_GEN : thm
val ITERATE_PAIR : thm
val ITERATE_PERMUTE : thm
val ITERATE_PERMUTES : thm
val ITERATE_RELATED : thm
val ITERATE_SING : thm
val ITERATE_SOME : thm
val ITERATE_SUPERSET : thm
val ITERATE_SUPPORT : thm
val ITERATE_UNION : thm
val ITERATE_UNION_GEN : thm
val ITERATE_UNION_NONZERO : thm
val ITSET_alt : thm
val LAMBDA_PAIR : thm
val LE_ADD : thm
val LE_ADDR : thm
val MOD_NSUM_MOD : thm
val MOD_NSUM_MOD_NUMSEG : thm
val MONOIDAL_AC : thm
val MONOIDAL_ADD : thm
val MONOIDAL_AND : thm
val MONOIDAL_LIFTED : thm
val MONOIDAL_MUL : thm
val NEUTRAL_ADD : thm
val NEUTRAL_AND : thm
val NEUTRAL_LIFTED : thm
val NEUTRAL_MUL : thm
val NOT_EQ : thm
val NPRODUCT_ADD_SPLIT : thm
val NPRODUCT_CLAUSES : thm
val NPRODUCT_CLAUSES_LEFT : thm
val NPRODUCT_CLAUSES_NUMSEG : thm
val NPRODUCT_CLAUSES_RIGHT : thm
val NPRODUCT_CLOSED : thm
val NPRODUCT_CONG : thm
val NPRODUCT_CONST : thm
val NPRODUCT_CONST_NUMSEG : thm
val NPRODUCT_CONST_NUMSEG_1 : thm
val NPRODUCT_DELETE : thm
val NPRODUCT_DELTA : thm
val NPRODUCT_EQ : thm
val NPRODUCT_EQ_0 : thm
val NPRODUCT_EQ_0_NUMSEG : thm
val NPRODUCT_EQ_1 : thm
val NPRODUCT_EQ_1_NUMSEG : thm
val NPRODUCT_EQ_NUMSEG : thm
val NPRODUCT_FACT : thm
val NPRODUCT_IMAGE : thm
val NPRODUCT_LE : thm
val NPRODUCT_LE_NUMSEG : thm
val NPRODUCT_MUL : thm
val NPRODUCT_MUL_GEN : thm
val NPRODUCT_MUL_NUMSEG : thm
val NPRODUCT_OFFSET : thm
val NPRODUCT_ONE : thm
val NPRODUCT_PAIR : thm
val NPRODUCT_POS_LT : thm
val NPRODUCT_POS_LT_NUMSEG : thm
val NPRODUCT_SING : thm
val NPRODUCT_SING_NUMSEG : thm
val NPRODUCT_SUPERSET : thm
val NPRODUCT_SUPPORT : thm
val NPRODUCT_UNION : thm
val NSUM_0 : thm
val NSUM_ADD : thm
val NSUM_ADD_GEN : thm
val NSUM_ADD_NUMSEG : thm
val NSUM_ADD_SPLIT : thm
val NSUM_BIGUNION_NONZERO : thm
val NSUM_BIJECTION : thm
val NSUM_BOUND : thm
val NSUM_BOUND_GEN : thm
val NSUM_BOUND_LT : thm
val NSUM_BOUND_LT_ALL : thm
val NSUM_BOUND_LT_GEN : thm
val NSUM_CASES : thm
val NSUM_CLAUSES : thm
val NSUM_CLAUSES_LEFT : thm
val NSUM_CLAUSES_NUMSEG : thm
val NSUM_CLAUSES_RIGHT : thm
val NSUM_CLOSED : thm
val NSUM_CONG : thm
val NSUM_CONST : thm
val NSUM_CONST_NUMSEG : thm
val NSUM_DEGENERATE : thm
val NSUM_DELETE : thm
val NSUM_DELTA : thm
val NSUM_DIFF : thm
val NSUM_EQ : thm
val NSUM_EQ_0 : thm
val NSUM_EQ_0_IFF : thm
val NSUM_EQ_0_IFF_NUMSEG : thm
val NSUM_EQ_0_NUMSEG : thm
val NSUM_EQ_GENERAL : thm
val NSUM_EQ_GENERAL_INVERSES : thm
val NSUM_EQ_NUMSEG : thm
val NSUM_EQ_SUPERSET : thm
val NSUM_GROUP : thm
val NSUM_IMAGE : thm
val NSUM_IMAGE_GEN : thm
val NSUM_IMAGE_NONZERO : thm
val NSUM_INCL_EXCL : thm
val NSUM_INJECTION : thm
val NSUM_LE : thm
val NSUM_LE_GEN : thm
val NSUM_LE_NUMSEG : thm
val NSUM_LMUL : thm
val NSUM_LT : thm
val NSUM_LT_ALL : thm
val NSUM_MULTICOUNT : thm
val NSUM_MULTICOUNT_GEN : thm
val NSUM_NSUM_PRODUCT : thm
val NSUM_NSUM_RESTRICT : thm
val NSUM_OFFSET : thm
val NSUM_OFFSET_0 : thm
val NSUM_PAIR : thm
val NSUM_PERMUTE : thm
val NSUM_PERMUTE_COUNT : thm
val NSUM_PERMUTE_NUMSEG : thm
val NSUM_POS_BOUND : thm
val NSUM_POS_LT : thm
val NSUM_POS_LT_ALL : thm
val NSUM_RESTRICT : thm
val NSUM_RESTRICT_SET : thm
val NSUM_RMUL : thm
val NSUM_SING : thm
val NSUM_SING_NUMSEG : thm
val NSUM_SUBSET : thm
val NSUM_SUBSET_SIMPLE : thm
val NSUM_SUPERSET : thm
val NSUM_SUPPORT : thm
val NSUM_SWAP : thm
val NSUM_SWAP_NUMSEG : thm
val NSUM_TRIV_NUMSEG : thm
val NSUM_UNION : thm
val NSUM_UNION_EQ : thm
val NSUM_UNION_LZERO : thm
val NSUM_UNION_NONZERO : thm
val NSUM_UNION_RZERO : thm
val NUMSEG_ADD_SPLIT : thm
val NUMSEG_CLAUSES : thm
val NUMSEG_COMBINE_L : thm
val NUMSEG_COMBINE_R : thm
val NUMSEG_EMPTY : thm
val NUMSEG_LE : thm
val NUMSEG_LREC : thm
val NUMSEG_LT : thm
val NUMSEG_OFFSET_IMAGE : thm
val NUMSEG_REC : thm
val NUMSEG_RREC : thm
val NUMSEG_SING : thm
val POWERSET_CLAUSES : thm
val SET_PROVE_CASES : thm
val SET_RECURSION_LEMMA : thm
val SIMPLE_IMAGE_GEN : thm
val SUBSET_NUMSEG : thm
val SUBSET_RESTRICT : thm
val SUPPORT_CLAUSES : thm
val SUPPORT_DELTA : thm
val SUPPORT_EMPTY : thm
val SUPPORT_SUBSET : thm
val SUPPORT_SUPPORT : thm
val TOPOLOGICAL_SORT : thm
val TOPOLOGICAL_SORT' : thm
val TRANSFORM_2D_NUM : thm
val TRANSITIVE_STEPWISE_LE : thm
val TRANSITIVE_STEPWISE_LE_EQ : thm
val TRIANGLE_2D_NUM : thm
val UNION_COUNT_FROM : thm
val UNION_FROM_COUNT : thm
val UPPER_BOUND_FINITE_SET : thm
val lifted : thm
val lifted_ind : thm
(*
[permutes] Parent theory of "iterate"
[FINREC_def] Definition
⊢ (∀f b s a. FINREC f b s a 0 ⇔ s = ∅ ∧ a = b) ∧
∀f b s a n.
FINREC f b s a (SUC n) ⇔
∃x c. x ∈ s ∧ FINREC f b (s DELETE x) c n ∧ a = f x c
[from_def] Definition
⊢ ∀n. from n = {m | n ≤ m}
[iterate] Definition
⊢ ∀op s f.
iterate op s f =
if FINITE (support op f s) then
ITSET (λx a. op (f x) a) (support op f s) (neutral op)
else neutral op
[monoidal] Definition
⊢ ∀op.
monoidal op ⇔
(∀x y. op x y = op y x) ∧
(∀x y z. op x (op y z) = op (op x y) z) ∧
∀x. op (neutral op) x = x
[neutral] Definition
⊢ ∀op. neutral op = @x. ∀y. op x y = y ∧ op y x = y
[nproduct] Definition
⊢ nproduct = iterate $*
[nsum] Definition
⊢ nsum = iterate $+
[numseg] Definition
⊢ ∀m n. {m .. n} = {x | m ≤ x ∧ x ≤ n}
[support] Definition
⊢ ∀op f s. support op f s = {x | x ∈ s ∧ f x ≠ neutral op}
[ADD_SUB2] Theorem
⊢ ∀m n. m + n − m = n
[ADD_SUBR] Theorem
⊢ ∀m n. n − (m + n) = 0
[ADD_SUBR2] Theorem
⊢ ∀m n. m − (m + n) = 0
[BIGINTER_BIGUNION] Theorem
⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}
[BIGUNION_BIGINTER] Theorem
⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}
[BOUNDS_LINEAR] Theorem
⊢ ∀A B C. (∀n. A * n ≤ B * n + C) ⇔ A ≤ B
[BOUNDS_LINEAR_0] Theorem
⊢ ∀A B. (∀n. A * n ≤ B) ⇔ A = 0
[CARD_BIGUNION] Theorem
⊢ ∀s. FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t u. t ∈ s ∧ u ∈ s ∧ t ≠ u ⇒ t ∩ u = ∅) ⇒
CARD (BIGUNION s) = nsum s CARD
[CARD_EQ_NSUM] Theorem
⊢ ∀s. FINITE s ⇒ CARD s = nsum s (λx. 1)
[CARD_NUMSEG] Theorem
⊢ ∀m n. CARD {m .. n} = n + 1 − m
[CARD_NUMSEG_1] Theorem
⊢ ∀n. CARD {1 .. n} = n
[CARD_NUMSEG_LEMMA] Theorem
⊢ ∀m d. CARD {m .. m + d} = d + 1
[CARD_UNION_EQ] Theorem
⊢ ∀s t u. FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ CARD s + CARD t = CARD u
[CHOOSE_SUBSET] Theorem
⊢ ∀s. FINITE s ⇒ ∀n. n ≤ CARD s ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[CHOOSE_SUBSET_STRONG] Theorem
⊢ ∀n s. (FINITE s ⇒ n ≤ CARD s) ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[COUNTABLE_FROM] Theorem
⊢ ∀n. countable (from n)
[COUNT_NUMSEG] Theorem
⊢ ∀n. 0 < n ⇒ count n = {0 .. n − 1}
[DIFF_BIGINTER2] Theorem
⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}
[DISJOINT_COUNT_FROM] Theorem
⊢ ∀n. DISJOINT (count n) (from n)
[DISJOINT_FROM_COUNT] Theorem
⊢ ∀n. DISJOINT (from n) (count n)
[DISJOINT_NUMSEG] Theorem
⊢ ∀m n p q.
DISJOINT {m .. n} {p .. q} ⇔ n < p ∨ q < m ∨ n < m ∨ q < p
[EMPTY_BIGUNION] Theorem
⊢ ∀s. BIGUNION s = ∅ ⇔ ∀t. t ∈ s ⇒ t = ∅
[EXISTS_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
∃t. FINITE t ∧ t ⊆ s ∧ P (IMAGE f t)
[FINITE_INDEX_NUMBERS] Theorem
⊢ ∀s. FINITE s ⇔
∃k f.
(∀i j. i ∈ k ∧ j ∈ k ∧ f i = f j ⇒ i = j) ∧ FINITE k ∧
s = IMAGE f k
[FINITE_INDEX_NUMSEG] Theorem
⊢ ∀s. FINITE s ⇔
∃f. (∀i j.
i ∈ {1 .. CARD s} ∧ j ∈ {1 .. CARD s} ∧ f i = f j ⇒
i = j) ∧ s = IMAGE f {1 .. CARD s}
[FINITE_NUMSEG] Theorem
⊢ ∀m n. FINITE {m .. n}
[FINITE_NUMSEG_LE] Theorem
⊢ ∀n. FINITE {m | m ≤ n}
[FINITE_NUMSEG_LT] Theorem
⊢ ∀n. FINITE {m | m < n}
[FINITE_POWERSET] Theorem
⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}
[FINITE_RECURSION] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
ITSET f ∅ b = b ∧
∀x s.
FINITE s ⇒
ITSET f (x INSERT s) b =
if x ∈ s then ITSET f s b else f x (ITSET f s b)
[FINITE_RESTRICT] Theorem
⊢ ∀s P. FINITE s ⇒ FINITE {x | x ∈ s ∧ P x}
[FINITE_SUBSET_IMAGE] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ IMAGE f s ⇔
∃s'. FINITE s' ∧ s' ⊆ s ∧ t = IMAGE f s'
[FINITE_SUPPORT] Theorem
⊢ ∀op f s. FINITE s ⇒ FINITE (support op f s)
[FINITE_SUPPORT_DELTA] Theorem
⊢ ∀op f a.
FINITE (support op (λx. if x = a then f x else neutral op) s)
[FINREC_1_LEMMA] Theorem
⊢ ∀f b s a. FINREC f b s a (SUC 0) ⇔ ∃x. s = {x} ∧ a = f x b
[FINREC_EXISTS_LEMMA] Theorem
⊢ ∀f b s. FINITE s ⇒ ∃a n. FINREC f b s a n
[FINREC_FUN] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∃g. g ∅ = b ∧ ∀s x. FINITE s ∧ x ∈ s ⇒ g s = f x (g (s DELETE x))
[FINREC_FUN_LEMMA] Theorem
⊢ ∀P R.
(∀s. P s ⇒ ∃a n. R s a n) ∧
(∀n1 n2 s a1 a2. R s a1 n1 ∧ R s a2 n2 ⇒ a1 = a2 ∧ n1 = n2) ⇒
∃f. ∀s a. P s ⇒ ((∃n. R s a n) ⇔ f s = a)
[FINREC_SUC_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∀n s z.
FINREC f b s z (SUC n) ⇒
∀x. x ∈ s ⇒ ∃w. FINREC f b (s DELETE x) w n ∧ z = f x w
[FINREC_UNIQUE_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∀n1 n2 s a1 a2.
FINREC f b s a1 n1 ∧ FINREC f b s a2 n2 ⇒ a1 = a2 ∧ n1 = n2
[FINREC_compute] Theorem
⊢ (∀f b s a. FINREC f b s a 0 ⇔ s = ∅ ∧ a = b) ∧
(∀f b s a n.
FINREC f b s a <..num comp'n..> ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c (<..num comp'n..> − 1) ∧
a = f x c) ∧
∀f b s a n.
FINREC f b s a <..num comp'n..> ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c <..num comp'n..> ∧ a = f x c
[FORALL_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
∀t. FINITE t ∧ t ⊆ s ⇒ P (IMAGE f t)
[FROM_0] Theorem
⊢ from 0 = 𝕌(:num)
[FROM_INTER_NUMSEG] Theorem
⊢ ∀k n. from k ∩ {0 .. n} = {k .. n}
[FROM_INTER_NUMSEG_GEN] Theorem
⊢ ∀k m n. from k ∩ {m .. n} = if m < k then {k .. n} else {m .. n}
[FROM_INTER_NUMSEG_MAX] Theorem
⊢ ∀m n p. from p ∩ {m .. n} = {MAX p m .. n}
[FROM_NOT_EMPTY] Theorem
⊢ ∀n. from n ≠ ∅
[FUN_IN_IMAGE] Theorem
⊢ ∀f s x. x ∈ s ⇒ f x ∈ IMAGE f s
[HAS_SIZE_NUMSEG] Theorem
⊢ ∀m n. {m .. n} HAS_SIZE n + 1 − m
[HAS_SIZE_NUMSEG_1] Theorem
⊢ ∀n. {1 .. n} HAS_SIZE n
[HAS_SIZE_NUMSEG_LE] Theorem
⊢ ∀n. {m | m ≤ n} HAS_SIZE n + 1
[HAS_SIZE_NUMSEG_LT] Theorem
⊢ ∀n. {m | m < n} HAS_SIZE n
[INFINITE_FROM] Theorem
⊢ ∀n. INFINITE (from n)
[IN_FROM] Theorem
⊢ ∀m n. m ∈ from n ⇔ n ≤ m
[IN_NUMSEG] Theorem
⊢ x ∈ {m .. n} ⇔ m ≤ x ∧ x ≤ n
[IN_NUMSEG_0] Theorem
⊢ ∀m n. m ∈ {0 .. n} ⇔ m ≤ n
[IN_SUPPORT] Theorem
⊢ ∀op f x s. x ∈ support op f s ⇔ x ∈ s ∧ f x ≠ neutral op
[ITERATE_AND] Theorem
⊢ ∀p s. FINITE s ⇒ (iterate $/\ s p ⇔ ∀x. x ∈ s ⇒ p x)
[ITERATE_BIJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
iterate op s f = iterate op s (f ∘ p)
[ITERATE_CASES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s P f g.
FINITE s ⇒
iterate op s (λx. if P x then f x else g x) =
op (iterate op {x | x ∈ s ∧ P x} f)
(iterate op {x | x ∈ s ∧ ¬P x} g)
[ITERATE_CLAUSES] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
FINITE s ⇒
iterate op (x INSERT s) f =
if x ∈ s then iterate op s f else op (f x) (iterate op s f)
[ITERATE_CLAUSES_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
monoidal op ∧ FINITE (support op f s) ⇒
iterate op (x INSERT s) f =
if x ∈ s then iterate op s f else op (f x) (iterate op s f)
[ITERATE_CLAUSES_NUMSEG] Theorem
⊢ ∀op.
monoidal op ⇒
(∀m. iterate op {m .. 0} f = if m = 0 then f 0 else neutral op) ∧
∀m n.
iterate op {m .. SUC n} f =
if m ≤ SUC n then op (iterate op {m .. n} f) (f (SUC n))
else iterate op {m .. n} f
[ITERATE_CLOSED] Theorem
⊢ ∀op.
monoidal op ⇒
∀P. P (neutral op) ∧ (∀x y. P x ∧ P y ⇒ P (op x y)) ⇒
∀f s.
(∀x. x ∈ s ∧ f x ≠ neutral op ⇒ P (f x)) ⇒
P (iterate op s f)
[ITERATE_DELETE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s a.
FINITE s ∧ a ∈ s ⇒
op (f a) (iterate op (s DELETE a) f) = iterate op s f
[ITERATE_DELTA] Theorem
⊢ ∀op.
monoidal op ⇒
∀f a s.
iterate op s (λx. if x = a then f x else neutral op) =
if a ∈ s then f a else neutral op
[ITERATE_DIFF] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ t ⊆ s ⇒
op (iterate op (s DIFF t) f) (iterate op t f) = iterate op s f
[ITERATE_DIFF_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ support op f t ⊆ support op f s ⇒
op (iterate op (s DIFF t) f) (iterate op t f) = iterate op s f
[ITERATE_EQ] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ iterate op s f = iterate op s g
[ITERATE_EQ_GENERAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
iterate op s f = iterate op t g
[ITERATE_EQ_GENERAL_INVERSES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
iterate op s f = iterate op t g
[ITERATE_EQ_NEUTRAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s.
(∀x. x ∈ s ⇒ f x = neutral op) ⇒ iterate op s f = neutral op
[ITERATE_EXPAND_CASES] Theorem
⊢ ∀op f s.
iterate op s f =
if FINITE (support op f s) then iterate op (support op f s) f
else neutral op
[ITERATE_IMAGE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
iterate op (IMAGE f s) g = iterate op s (g ∘ f)
[ITERATE_IMAGE_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀g f s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ f x = f y ⇒ g (f x) = neutral op) ⇒
iterate op (IMAGE f s) g = iterate op s (g ∘ f)
[ITERATE_INCL_EXCL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f.
FINITE s ∧ FINITE t ⇒
op (iterate op s f) (iterate op t f) =
op (iterate op (s ∪ t) f) (iterate op (s ∩ t) f)
[ITERATE_INJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
iterate op s (f ∘ p) = iterate op s f
[ITERATE_ITERATE_PRODUCT] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
iterate op s (λi. iterate op (t i) (x i)) =
iterate op {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[ITERATE_OP] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE s ⇒
iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g)
[ITERATE_OP_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE (support op f s) ∧ FINITE (support op g s) ⇒
iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g)
[ITERATE_PAIR] Theorem
⊢ ∀op.
monoidal op ⇒
∀f m n.
iterate op {2 * m .. 2 * n + 1} f =
iterate op {m .. n} (λi. op (f (2 * i)) (f (2 * i + 1)))
[ITERATE_PERMUTE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s. p permutes s ⇒ iterate op s f = iterate op s (f ∘ p)
[ITERATE_PERMUTES] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s. p PERMUTES s ⇒ iterate op s f = iterate op s (f ∘ p)
[ITERATE_RELATED] Theorem
⊢ ∀op.
monoidal op ⇒
∀R. R (neutral op) (neutral op) ∧
(∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 ⇒ R (op x1 y1) (op x2 y2)) ⇒
∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ R (f x) (g x)) ⇒
R (iterate op s f) (iterate op s g)
[ITERATE_SING] Theorem
⊢ ∀op. monoidal op ⇒ ∀f x. iterate op {x} f = f x
[ITERATE_SOME] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s.
FINITE s ⇒
iterate (lifted op) s (λx. SOME (f x)) = SOME (iterate op s f)
[ITERATE_SUPERSET] Theorem
⊢ ∀op.
monoidal op ⇒
∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = neutral op) ⇒
iterate op v f = iterate op u f
[ITERATE_SUPPORT] Theorem
⊢ ∀op f s. iterate op (support op f s) f = iterate op s f
[ITERATE_UNION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITERATE_UNION_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ FINITE (support op f t) ∧
DISJOINT (support op f s) (support op f t) ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITERATE_UNION_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = neutral op) ⇒
iterate op (s ∪ t) f = op (iterate op s f) (iterate op t f)
[ITSET_alt] Theorem
⊢ ∀f s b.
(∀x y z. f x (f y z) = f y (f x z)) ∧ FINITE s ⇒
ITSET f s b =
(@g. g ∅ = b ∧
∀x s.
FINITE s ⇒
g (x INSERT s) = if x ∈ s then g s else f x (g s)) s
[LAMBDA_PAIR] Theorem
⊢ (λ(x,y). P x y) = (λp. P (FST p) (SND p))
[LE_ADD] Theorem
⊢ ∀m n. m ≤ m + n
[LE_ADDR] Theorem
⊢ ∀m n. n ≤ m + n
[MOD_NSUM_MOD] Theorem
⊢ ∀f n s.
FINITE s ∧ n ≠ 0 ⇒ nsum s f MOD n = nsum s (λi. f i MOD n) MOD n
[MOD_NSUM_MOD_NUMSEG] Theorem
⊢ ∀f a b n.
n ≠ 0 ⇒
nsum {a .. b} f MOD n = nsum {a .. b} (λi. f i MOD n) MOD n
[MONOIDAL_AC] Theorem
⊢ ∀op.
monoidal op ⇒
(∀a. op (neutral op) a = a) ∧ (∀a. op a (neutral op) = a) ∧
(∀a b. op a b = op b a) ∧
(∀a b c. op (op a b) c = op a (op b c)) ∧
∀a b c. op a (op b c) = op b (op a c)
[MONOIDAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_AND] Theorem
⊢ monoidal $/\
[MONOIDAL_LIFTED] Theorem
⊢ ∀op. monoidal op ⇒ monoidal (lifted op)
[MONOIDAL_MUL] Theorem
⊢ monoidal $*
[NEUTRAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_AND] Theorem
⊢ neutral $/\ ⇔ T
[NEUTRAL_LIFTED] Theorem
⊢ ∀op. monoidal op ⇒ neutral (lifted op) = SOME (neutral op)
[NEUTRAL_MUL] Theorem
⊢ neutral $* = 1
[NOT_EQ] Theorem
⊢ ∀a b. a ≠ b ⇔ a ≠ b
[NPRODUCT_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
nproduct {m .. n + p} f =
nproduct {m .. n} f * nproduct {n + 1 .. n + p} f
[NPRODUCT_CLAUSES] Theorem
⊢ (∀f. nproduct ∅ f = 1) ∧
∀x f s.
FINITE s ⇒
nproduct (x INSERT s) f =
if x ∈ s then nproduct s f else f x * nproduct s f
[NPRODUCT_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ nproduct {m .. n} f = f m * nproduct {m + 1 .. n} f
[NPRODUCT_CLAUSES_NUMSEG] Theorem
⊢ (∀m. nproduct {m .. 0} f = if m = 0 then f 0 else 1) ∧
∀m n.
nproduct {m .. SUC n} f =
if m ≤ SUC n then nproduct {m .. n} f * f (SUC n)
else nproduct {m .. n} f
[NPRODUCT_CLAUSES_RIGHT] Theorem
⊢ ∀f m n.
0 < n ∧ m ≤ n ⇒
nproduct {m .. n} f = nproduct {m .. n − 1} f * f n
[NPRODUCT_CLOSED] Theorem
⊢ ∀P f s.
P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (nproduct s f)
[NPRODUCT_CONG] Theorem
⊢ (∀f g s.
(∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s (λi. f i) = nproduct s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
nproduct {a .. b} (λi. f i) = nproduct {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
nproduct {y | p y} (λi. f i) = nproduct {y | p y} g
[NPRODUCT_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ nproduct s (λx. c) = c ** CARD s
[NPRODUCT_CONST_NUMSEG] Theorem
⊢ ∀c m n. nproduct {m .. n} (λx. c) = c ** (n + 1 − m)
[NPRODUCT_CONST_NUMSEG_1] Theorem
⊢ ∀c n. nproduct {1 .. n} (λx. c) = c ** n
[NPRODUCT_DELETE] Theorem
⊢ ∀f s a.
FINITE s ∧ a ∈ s ⇒ f a * nproduct (s DELETE a) f = nproduct s f
[NPRODUCT_DELTA] Theorem
⊢ ∀s a.
nproduct s (λx. if x = a then b else 1) = if a ∈ s then b else 1
[NPRODUCT_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s f = nproduct s g
[NPRODUCT_EQ_0] Theorem
⊢ ∀f s. FINITE s ⇒ (nproduct s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
[NPRODUCT_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. nproduct {m .. n} f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
[NPRODUCT_EQ_1] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ nproduct s f = 1
[NPRODUCT_EQ_1_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ nproduct {m .. n} f = 1
[NPRODUCT_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
nproduct {m .. n} f = nproduct {m .. n} g
[NPRODUCT_FACT] Theorem
⊢ ∀n. nproduct {1 .. n} (λm. m) = FACT n
[NPRODUCT_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
nproduct (IMAGE f s) g = nproduct s (g ∘ f)
[NPRODUCT_LE] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
nproduct s f ≤ nproduct s g
[NPRODUCT_LE_NUMSEG] Theorem
⊢ ∀f m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
nproduct {m .. n} f ≤ nproduct {m .. n} g
[NPRODUCT_MUL] Theorem
⊢ ∀f g s.
FINITE s ⇒
nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
[NPRODUCT_MUL_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
[NPRODUCT_MUL_NUMSEG] Theorem
⊢ ∀f g m n.
nproduct {m .. n} (λx. f x * g x) =
nproduct {m .. n} f * nproduct {m .. n} g
[NPRODUCT_OFFSET] Theorem
⊢ ∀f m p.
nproduct {m + p .. n + p} f = nproduct {m .. n} (λi. f (i + p))
[NPRODUCT_ONE] Theorem
⊢ ∀s. nproduct s (λn. 1) = 1
[NPRODUCT_PAIR] Theorem
⊢ ∀f m n.
nproduct {2 * m .. 2 * n + 1} f =
nproduct {m .. n} (λi. f (2 * i) * f (2 * i + 1))
[NPRODUCT_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < nproduct s f
[NPRODUCT_POS_LT_NUMSEG] Theorem
⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < nproduct {m .. n} f
[NPRODUCT_SING] Theorem
⊢ ∀f x. nproduct {x} f = f x
[NPRODUCT_SING_NUMSEG] Theorem
⊢ ∀f n. nproduct {n .. n} f = f n
[NPRODUCT_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒
nproduct v f = nproduct u f
[NPRODUCT_SUPPORT] Theorem
⊢ ∀f s. nproduct (support $* f s) f = nproduct s f
[NPRODUCT_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
nproduct (s ∪ t) f = nproduct s f * nproduct t f
[NSUM_0] Theorem
⊢ ∀s. nsum s (λn. 0) = 0
[NSUM_ADD] Theorem
⊢ ∀f g s. FINITE s ⇒ nsum s (λx. f x + g x) = nsum s f + nsum s g
[NSUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
nsum s (λx. f x + g x) = nsum s f + nsum s g
[NSUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
nsum {m .. n} (λi. f i + g i) = nsum {m .. n} f + nsum {m .. n} g
[NSUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
nsum {m .. n + p} f = nsum {m .. n} f + nsum {n + 1 .. n + p} f
[NSUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x. t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ f x = 0) ⇒
nsum (BIGUNION s) f = nsum s (λt. nsum t f)
[NSUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ p x = y) ⇒
nsum s f = nsum s (f ∘ p)
[NSUM_BOUND] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ nsum s f ≤ CARD s * b
[NSUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b DIV CARD s) ⇒
nsum s f ≤ b
[NSUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
nsum s f < CARD s * b
[NSUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒ nsum s f < CARD s * b
[NSUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b DIV CARD s) ⇒
nsum s f < b
[NSUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
nsum s (λx. if P x then f x else g x) =
nsum {x | x ∈ s ∧ P x} f + nsum {x | x ∈ s ∧ ¬P x} g
[NSUM_CLAUSES] Theorem
⊢ (∀f. nsum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
nsum (x INSERT s) f = if x ∈ s then nsum s f else f x + nsum s f
[NSUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ nsum {m .. n} f = f m + nsum {m + 1 .. n} f
[NSUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. nsum {m .. 0} f = if m = 0 then f 0 else 0) ∧
∀m n.
nsum {m .. SUC n} f =
if m ≤ SUC n then nsum {m .. n} f + f (SUC n)
else nsum {m .. n} f
[NSUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ nsum {m .. n} f = nsum {m .. n − 1} f + f n
[NSUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (nsum s f)
[NSUM_CONG] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nsum s (λi. f i) = nsum s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
nsum {a .. b} (λi. f i) = nsum {a .. b} g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
nsum {y | p y} (λi. f i) = nsum {y | p y} g
[NSUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ nsum s (λn. c) = CARD s * c
[NSUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. nsum {m .. n} (λn. c) = (n + 1 − m) * c
[NSUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ nsum s f = 0
[NSUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ f a + nsum (s DELETE a) f = nsum s f
[NSUM_DELTA] Theorem
⊢ ∀s a. nsum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[NSUM_DIFF] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ nsum (s DIFF t) f = nsum s f − nsum t f
[NSUM_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nsum s f = nsum s g
[NSUM_EQ_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 0) ⇒ nsum s f = 0
[NSUM_EQ_0_IFF] Theorem
⊢ ∀s. FINITE s ⇒ (nsum s f = 0 ⇔ ∀x. x ∈ s ⇒ f x = 0)
[NSUM_EQ_0_IFF_NUMSEG] Theorem
⊢ ∀f m n. nsum {m .. n} f = 0 ⇔ ∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0
[NSUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 0) ⇒ nsum {m .. n} f = 0
[NSUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ h x = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ g (h x) = f x) ⇒
nsum s f = nsum t g
[NSUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ h (k y) = y) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ k (h x) = x ∧ g (h x) = f x) ⇒
nsum s f = nsum t g
[NSUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
nsum {m .. n} f = nsum {m .. n} g
[NSUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ f x = g x) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ f x = 0) ⇒
nsum s f = nsum t g
[NSUM_GROUP] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
nsum t (λy. nsum {x | x ∈ s ∧ f x = y} g) = nsum s g
[NSUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
nsum (IMAGE f s) g = nsum s (g ∘ f)
[NSUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
nsum s g = nsum (IMAGE f s) (λy. nsum {x | x ∈ s ∧ f x = y} g)
[NSUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ i x = i y ⇒ d (i x) = 0) ⇒
nsum (IMAGE i s) d = nsum s (d ∘ i)
[NSUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
nsum s f + nsum t f = nsum (s ∪ t) f + nsum (s ∩ t) f
[NSUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y) ⇒
nsum s (f ∘ p) = nsum s f
[NSUM_LE] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ nsum s f ≤ nsum s g
[NSUM_LE_GEN] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x ≤ g x) ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
nsum s f ≤ nsum s g
[NSUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒
nsum {m .. n} f ≤ nsum {m .. n} g
[NSUM_LMUL] Theorem
⊢ ∀f c s. nsum s (λx. c * f x) = c * nsum s f
[NSUM_LT] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
nsum s f < nsum s g
[NSUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ nsum s f < nsum s g
[NSUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧ (∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k) ⇒
nsum s (λi. CARD (equiv_class R t i)) = k * CARD t
[NSUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ CARD {i | i ∈ s ∧ R i j} = k j) ⇒
nsum s (λi. CARD (equiv_class R t i)) = nsum t (λi. k i)
[NSUM_NSUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
nsum s (λi. nsum (t i) (x i)) =
nsum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j)
[NSUM_NSUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
nsum s (λx. nsum (equiv_class R t x) (λy. f x y)) =
nsum t (λy. nsum {x | x ∈ s ∧ R x y} (λx. f x y))
[NSUM_OFFSET] Theorem
⊢ ∀p f m n. nsum {m + p .. n + p} f = nsum {m .. n} (λi. f (i + p))
[NSUM_OFFSET_0] Theorem
⊢ ∀f m n. m ≤ n ⇒ nsum {m .. n} f = nsum {0 .. n − m} (λi. f (i + m))
[NSUM_PAIR] Theorem
⊢ ∀f m n.
nsum {2 * m .. 2 * n + 1} f =
nsum {m .. n} (λi. f (2 * i) + f (2 * i + 1))
[NSUM_PERMUTE] Theorem
⊢ ∀f p s. p permutes s ⇒ nsum s f = nsum s (f ∘ p)
[NSUM_PERMUTE_COUNT] Theorem
⊢ ∀f p n.
p permutes count n ⇒ nsum (count n) f = nsum (count n) (f ∘ p)
[NSUM_PERMUTE_NUMSEG] Theorem
⊢ ∀f p m n.
p permutes count n DIFF count m ⇒
nsum (count n DIFF count m) f =
nsum (count n DIFF count m) (f ∘ p)
[NSUM_POS_BOUND] Theorem
⊢ ∀f b s. FINITE s ∧ nsum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b
[NSUM_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < nsum s f
[NSUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < nsum s f
[NSUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ nsum s (λx. if x ∈ s then f x else 0) = nsum s f
[NSUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
nsum {x | x ∈ s ∧ P x} f = nsum s (λx. if P x then f x else 0)
[NSUM_RMUL] Theorem
⊢ ∀f c s. nsum s (λx. f x * c) = nsum s f * c
[NSUM_SING] Theorem
⊢ ∀f x. nsum {x} f = f x
[NSUM_SING_NUMSEG] Theorem
⊢ ∀f n. nsum {n .. n} f = f n
[NSUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x = 0) ⇒
nsum u f ≤ nsum v f
[NSUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f. FINITE v ∧ u ⊆ v ⇒ nsum u f ≤ nsum v f
[NSUM_SUPERSET] Theorem
⊢ ∀f u v. u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒ nsum v f = nsum u f
[NSUM_SUPPORT] Theorem
⊢ ∀f s. nsum (support $+ f s) f = nsum s f
[NSUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
nsum s (λi. nsum t (f i)) = nsum t (λj. nsum s (λi. f i j))
[NSUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
nsum {a .. b} (λi. nsum {c .. d} (f i)) =
nsum {c .. d} (λj. nsum {a .. b} (λi. f i j))
[NSUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ nsum {m .. n} f = 0
[NSUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
nsum (s ∪ t) f = nsum s f + nsum t f
[NSUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ s ∩ t = ∅ ∧ s ∪ t = u ⇒ nsum s f + nsum t f = nsum u f
[NSUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ f x = 0) ⇒
nsum (u ∪ v) f = nsum v f
[NSUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ f x = 0) ⇒
nsum (s ∪ t) f = nsum s f + nsum t f
[NSUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 0) ⇒
nsum (u ∪ v) f = nsum u f
[NUMSEG_ADD_SPLIT] Theorem
⊢ ∀m n p. m ≤ n + 1 ⇒ {m .. n + p} = {m .. n} ∪ {n + 1 .. n + p}
[NUMSEG_CLAUSES] Theorem
⊢ (∀m. {m .. 0} = if m = 0 then {0} else ∅) ∧
∀m n.
{m .. SUC n} =
if m ≤ SUC n then SUC n INSERT {m .. n} else {m .. n}
[NUMSEG_COMBINE_L] Theorem
⊢ ∀m p n. m ≤ p ∧ p ≤ n + 1 ⇒ {m .. p − 1} ∪ {p .. n} = {m .. n}
[NUMSEG_COMBINE_R] Theorem
⊢ ∀m p n. m ≤ p + 1 ∧ p ≤ n ⇒ {m .. p} ∪ {p + 1 .. n} = {m .. n}
[NUMSEG_EMPTY] Theorem
⊢ ∀m n. {m .. n} = ∅ ⇔ n < m
[NUMSEG_LE] Theorem
⊢ ∀n. {x | x ≤ n} = {0 .. n}
[NUMSEG_LREC] Theorem
⊢ ∀m n. m ≤ n ⇒ m INSERT {m + 1 .. n} = {m .. n}
[NUMSEG_LT] Theorem
⊢ ∀n. {x | x < n} = if n = 0 then ∅ else {0 .. n − 1}
[NUMSEG_OFFSET_IMAGE] Theorem
⊢ ∀m n p. {m + p .. n + p} = IMAGE (λi. i + p) {m .. n}
[NUMSEG_REC] Theorem
⊢ ∀m n. m ≤ SUC n ⇒ {m .. SUC n} = SUC n INSERT {m .. n}
[NUMSEG_RREC] Theorem
⊢ ∀m n. m ≤ n ⇒ n INSERT {m .. n − 1} = {m .. n}
[NUMSEG_SING] Theorem
⊢ ∀n. {n .. n} = {n}
[POWERSET_CLAUSES] Theorem
⊢ {s | s ⊆ ∅} = {∅} ∧
∀a t.
{s | s ⊆ a INSERT t} =
{s | s ⊆ t} ∪ IMAGE (λs. a INSERT s) {s | s ⊆ t}
[SET_PROVE_CASES] Theorem
⊢ ∀P. P ∅ ∧ (∀a s. a ∉ s ⇒ P (a INSERT s)) ⇒ ∀s. P s
[SET_RECURSION_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ f x (f y s) = f y (f x s)) ⇒
∃g. g ∅ = b ∧
∀x s.
FINITE s ⇒
g (x INSERT s) = if x ∈ s then g s else f x (g s)
[SIMPLE_IMAGE_GEN] Theorem
⊢ ∀f P. {f x | P x} = IMAGE f {x | P x}
[SUBSET_NUMSEG] Theorem
⊢ ∀m n p q. {m .. n} ⊆ {p .. q} ⇔ n < m ∨ p ≤ m ∧ n ≤ q
[SUBSET_RESTRICT] Theorem
⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s
[SUPPORT_CLAUSES] Theorem
⊢ (∀f. support op f ∅ = ∅) ∧
(∀f x s.
support op f (x INSERT s) =
if f x = neutral op then support op f s
else x INSERT support op f s) ∧
(∀f x s. support op f (s DELETE x) = support op f s DELETE x) ∧
(∀f s t. support op f (s ∪ t) = support op f s ∪ support op f t) ∧
(∀f s t. support op f (s ∩ t) = support op f s ∩ support op f t) ∧
(∀f s t.
support op f (s DIFF t) = support op f s DIFF support op f t) ∧
∀f g s. support op g (IMAGE f s) = IMAGE f (support op (g ∘ f) s)
[SUPPORT_DELTA] Theorem
⊢ ∀op s f a.
support op (λx. if x = a then f x else neutral op) s =
if a ∈ s then support op f {a} else ∅
[SUPPORT_EMPTY] Theorem
⊢ ∀op f s. (∀x. x ∈ s ⇒ f x = neutral op) ⇔ support op f s = ∅
[SUPPORT_SUBSET] Theorem
⊢ ∀op f s. support op f s ⊆ s
[SUPPORT_SUPPORT] Theorem
⊢ ∀op f s. support op f (support op f s) = support op f s
[TOPOLOGICAL_SORT] Theorem
⊢ ∀ $<<.
(∀x y. x << y ∧ y << x ⇒ x = y) ∧
(∀x y z. x << y ∧ y << z ⇒ x << z) ⇒
∀n s.
s HAS_SIZE n ⇒
∃f. s = IMAGE f {1 .. n} ∧
∀j k. j ∈ {1 .. n} ∧ k ∈ {1 .. n} ∧ j < k ⇒ ¬(f k << f j)
[TOPOLOGICAL_SORT'] Theorem
⊢ ∀R s n.
transitive R ∧ antisymmetric R ∧ s HAS_SIZE n ⇒
∃f. s = IMAGE f (count n) ∧
∀j k. j < n ∧ k < n ∧ j < k ⇒ ¬R (f k) (f j)
[TRANSFORM_2D_NUM] Theorem
⊢ ∀P. (∀m n. P m n ⇒ P n m) ∧ (∀m n. P m (m + n)) ⇒ ∀m n. P m n
[TRANSITIVE_STEPWISE_LE] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
(∀n. R n (SUC n)) ⇒
∀m n. m ≤ n ⇒ R m n
[TRANSITIVE_STEPWISE_LE_EQ] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
((∀m n. m ≤ n ⇒ R m n) ⇔ ∀n. R n (SUC n))
[TRIANGLE_2D_NUM] Theorem
⊢ ∀P. (∀d n. P n (d + n)) ⇒ ∀m n. m ≤ n ⇒ P m n
[UNION_COUNT_FROM] Theorem
⊢ ∀n. count n ∪ from n = 𝕌(:num)
[UNION_FROM_COUNT] Theorem
⊢ ∀n. from n ∪ count n = 𝕌(:num)
[UPPER_BOUND_FINITE_SET] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[lifted] Theorem
⊢ lifted op NONE v0 = NONE ∧ lifted op (SOME v5) NONE = NONE ∧
lifted op (SOME x) (SOME y) = SOME (op x y)
[lifted_ind] Theorem
⊢ ∀P. (∀op v0. P op NONE v0) ∧ (∀op v5. P op (SOME v5) NONE) ∧
(∀op x y. P op (SOME x) (SOME y)) ⇒
∀v v1 v2. P v v1 v2
*)
end
HOL 4, Trindemossen-2