Theory Monoid_ZF_1
section ‹Summing lists in a monoid›
theory Monoid_ZF_1 imports Monoid_ZF
begin
text‹This theory consider properties of sums of monoid elements, similar
to the ones formalized in the ‹Semigroup_ZF› theory for sums of semigroup elements. The main
difference is that since each monoid has a neutral element it makes sense to define a sum
of an empty list of monoid elements. In multiplicative notation the properties considered here
can be applied to natural powers of elements ($x^n, n\in \mathbb{N}$) in group or ring theory or,
when written additively, to natural multiplicities $n\cdot x, n\in \mathbb{N}$). ›
subsection‹Notation and basic properties of sums of lists of monoid elements›
text‹In this section we setup a contex (locale) with notation for sums of lists of
monoid elements and prove basic properties of those sums in terms of that notation. ›
text‹The locale (context) ‹monoid1› extends the locale ‹monoid1›, adding the notation for the
neutral element as $0$ and the sum of a list of monoid elements.
It also defines a notation for natural multiple of an element of a monoid,
i.e. $n\cdot x = x\oplus x\oplus ... \oplus x$ (n times). ›
locale monoid1 = monoid0 +
fixes mzero ("𝟬")
defines mzero_def [simp]: "𝟬 ≡ TheNeutralElement(G,f)"
fixes listsum ("∑ _" 70)
defines listsum_def [simp]: "∑s ≡ Fold(f,𝟬,s)"
fixes nat_mult (infix "⋅" 72)
defines nat_mult_def [simp]: "n⋅x ≡ ∑{⟨k,x⟩. k∈n}"
text‹Let's recall that the neutral element of the monoid is an element of the monoid (carrier) $G$
and the monoid operation ($f$ in our notation) is a function that maps $G\times G$
to $G$.›
lemma (in monoid1) zero_monoid_oper: shows "𝟬∈G" and "f:G×G → G"
using monoidAssum unit_is_neutral unfolding IsAmonoid_def IsAssociative_def
by simp_all
text‹The sum of a list of monoid elements is a monoid element.›
lemma (in monoid1) sum_in_mono: assumes "n∈nat" "∀k∈n. q(k)∈G"
shows "(∑{⟨k,q(k)⟩. k∈n}) ∈ G"
proof -
let ?a = "{⟨k,q(k)⟩. k∈n}"
from assms have "n ∈ nat" "f:G×G → G" "?a:n → G" "𝟬∈G" "G≠0"
using zero_monoid_oper ZF_fun_from_total by auto
then show ?thesis using fold_props by simp
qed
text‹The reason we start from $0$ in the definition of the summation sign in the ‹monoid1› locale
is that we want to be able to sum the empty list. Such sum of the empty list is $0$. ›
lemma (in monoid1) sum_empty: assumes "s:0→G" shows "(∑s) = 𝟬"
using assms zero_monoid_oper fold_empty group0_1_L3A by simp
text‹For nonempty lists our $\Sigma$ is the same as ‹Fold1›. ›
lemma (in monoid1) sum_nonempty: assumes "n ∈ nat" "s:succ(n)→G"
shows
"(∑s) = Fold(f,s`(0),Tail(s))"
"(∑s) = Fold1(f,s)"
proof -
from assms have "s`(0) ∈ G" using empty_in_every_succ apply_funtype
by simp
with assms have "(∑s) = Fold(f,𝟬⊕s`(0),Tail(s))"
using zero_monoid_oper fold_detach_first by simp
with ‹s`(0) ∈ G› show "(∑s) = Fold(f,s`(0),Tail(s))"
using unit_is_neutral by simp
then show "(∑s) = Fold1(f,s)" unfolding Fold1_def by simp
qed
text‹We can pull the first component of a sum of a nonempty list of monoid elements
before the summation sign. ›
lemma (in monoid1) seq_sum_pull_first0: assumes "n ∈ nat" "s:succ(n)→G"
shows "(∑s) = s`(0) ⊕ (∑Tail(s))"
proof -
from assms have "s`(0) ∈ G" using empty_in_every_succ apply_funtype
by simp
{ assume "n=0"
with assms have "Tail(s):0→G" using tail_props(1) by blast
with assms ‹s`(0) ∈ G› have "(∑s) = s`(0) ⊕ (∑Tail(s))"
using sum_nonempty(1) sum_empty zero_monoid_oper(2) group0_1_L3A
fold_empty unit_is_neutral by simp
}
moreover
{ assume "n≠0"
with assms(1) obtain m where "m∈nat" and "n = succ(m)"
using Nat_ZF_1_L3 by blast
with assms have "Tail(s):succ(m)→G" using tail_props(1)
by simp
let ?a = "{⟨0,s`(0)⟩}"
from ‹s`(0) ∈ G› have "0∈nat" "?a:succ(0)→G"
using pair_func_singleton succ_explained by simp_all
with ‹m∈nat› ‹Tail(s):succ(m)→G›
have "f`⟨Fold1(f,?a),Fold1(f,Tail(s))⟩ = Fold1(f,Concat(?a,Tail(s)))"
using semigr0_valid_in_monoid0 semigr0.prod_conc_distr
by blast
with assms ‹?a:succ(0)→G› ‹m∈nat› ‹Tail(s):succ(m)→G›
have "(∑s) = s`(0) ⊕ (∑Tail(s))"
using semigr0_valid_in_monoid0 semigr0.prod_of_1elem pair_val
sum_nonempty(2) first_concat_tail by simp
}
ultimately show ?thesis by auto
qed
text‹The first assertion of the next theorem is similar in content to ‹seq_sum_pull_first0›
formulated in terms of the expression defining the list of monoid elements. The second
one shows the dual statement: the last element of a sequence can be pulled out of the
sequence and put after the summation sign. So, we are showing here that
$\sum_{k=0}^{n} q_k = q_0 \oplus \sum_{k=0}^{n-1} q_{k+1} = (\sum_{k=0}^{n-1} q_k) \oplus q_n. $ ›
theorem (in monoid1) seq_sum_pull_one_elem:
assumes "n ∈ nat" "∀k∈n #+ 1. q(k) ∈ G"
shows
"(∑{⟨k,q(k)⟩. k∈n #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈n})"
"(∑{⟨k,q(k)⟩. k∈n #+ 1}) = (∑{⟨k,q(k)⟩. k∈n}) ⊕ q(n)"
proof -
let ?s = "{⟨k,q(k)⟩. k∈n #+ 1}"
from assms(1) have "0 ∈ n #+ 1" using empty_in_every_succ succ_add_one(1)
by simp
then have "?s`(0) = q(0)" by (rule ZF_fun_from_tot_val1)
from assms(2) have "?s: n #+ 1 → G" by (rule ZF_fun_from_total)
with assms(1) ‹?s`(0) = q(0)› have "(∑?s) = q(0) ⊕ (∑Tail(?s))"
using seq_sum_pull_first0 by simp
moreover from assms have "Tail(?s) = {⟨k,q(k #+ 1)⟩. k ∈ n}"
using tail_formula by simp
ultimately show "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈n})"
by simp
from assms show "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = (∑{⟨k,q(k)⟩. k∈n}) ⊕ q(n)"
using zero_monoid_oper fold_detach_last by simp
qed
text‹The sum of a singleton list is its only element,›
lemma (in monoid1) seq_sum_singleton: assumes "q(0) ∈ G"
shows "(∑{⟨k,q(k)⟩. k∈1}) = q(0)"
proof -
from assms have "0∈nat" and "∀k∈0 #+ 1. q(k) ∈ G" by simp_all
then have
"(∑{⟨k,q(k)⟩. k∈0 #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈0})"
by (rule seq_sum_pull_one_elem)
with assms show ?thesis using sum_empty unit_is_neutral by simp
qed
text‹If the monoid operation is commutative, then the sum of a nonempty sequence
added to another sum of a nonempty sequence of the same length is equal
to the sum of pointwise sums of the sequence elements.
This is the same as the theorem ‹prod_comm_distrib› from the
‹Semigroup_ZF› theory, just written in the notation used in the ‹monoid1› locale.›
lemma (in monoid1) sum_comm_distrib0:
assumes "f {is commutative on} G" "n∈nat" and
"a : n #+ 1 → G" "b : n #+ 1 → G" "c : n #+ 1 → G" and
"∀j∈n #+ 1. c`(j) = a`(j) ⊕ b`(j)"
shows "(∑ c) = (∑ a) ⊕ (∑ b)"
using assms succ_add_one(1) sum_nonempty
semigr0_valid_in_monoid0 semigr0.prod_comm_distrib by simp
text‹Another version of ‹sum_comm_distrib0› written in terms of the expressions
defining the sequences, shows that for commutative monoids we have
$\sum_{k=0}^{n-1}q(k) \oplus p(k) = (\sum_{k=0}^{n-1} p(k))\oplus (\sum_{k=0}^{n-1} q(k))$. ›
theorem (in monoid1) sum_comm_distrib:
assumes "f {is commutative on} G" "n∈nat" and
"∀k∈n. p(k) ∈ G" "∀k∈n. q(k) ∈ G"
shows
"(∑{⟨k,p(k)⊕q(k)⟩. k∈n}) = (∑{⟨k,p(k)⟩. k∈n}) ⊕ (∑{⟨k,q(k)⟩. k∈n})"
proof -
let ?a = "{⟨k,p(k)⟩. k∈n}"
let ?b = "{⟨k,q(k)⟩. k∈n}"
let ?c = "{⟨k,p(k)⊕q(k)⟩. k∈n}"
{ assume "n=0"
then have "(∑?c) = (∑?a) ⊕ (∑?b)"
using sum_empty unit_is_neutral by simp
}
moreover
{ assume "n≠0"
with assms(2) obtain m where "m∈nat" and "n = m #+ 1"
using nat_not0_succ by blast
from assms(3,4) have "?a:n→G" "?b:n→G" "?c:n→G"
using group0_1_L1 ZF_fun_from_total by simp_all
with assms(1) ‹m∈nat› ‹n = m #+ 1› have
"f {is commutative on} G" "m∈nat" and
"?a:m #+ 1→G" "?b:m #+ 1→G" "?c:m #+ 1→G"
by simp_all
moreover have "∀k∈m #+ 1. ?c`(k) = ?a`(k) ⊕ ?b`(k)"
proof -
{ fix k assume "k ∈ m #+ 1"
with ‹n = m #+ 1› have "k∈n" by simp
then have "?c`(k) = ?a`(k) ⊕ ?b`(k)"
using ZF_fun_from_tot_val1 by simp_all
} thus ?thesis by simp
qed
ultimately have "(∑?c) = (∑?a) ⊕ (∑?b)"
using sum_comm_distrib0 by simp
}
ultimately show ?thesis by blast
qed
subsection‹Multiplying monoid elements by natural numbers›
text‹A special case of summing (or, using more notation-neutral term ‹folding›)
a list of monoid elements is taking a natural multiple of a single element.
This can be applied to various monoids embedded in other algebraic structures.
For example a ring is a monoid with addition as the operation, so the notion of
natural multiple directly transfers there. Another monoid in a ring is formed by its
multiplication operation. In that case the natural multiple maps into natural powers of a ring
element. ›
text‹The zero's multiple of a monoid element is its neutral element.›
lemma (in monoid1) nat_mult_zero: shows "0⋅x = 𝟬" using sum_empty by simp
text‹Any multiple of a monoid element is a monoid element.›
lemma (in monoid1) nat_mult_type: assumes "n∈nat" "x∈G"
shows "n⋅x ∈ G" using assms sum_in_mono by simp
text‹Taking one more multiple of $x$ adds $x$. ›
lemma (in monoid1) nat_mult_add_one: assumes "n∈nat" "x∈G"
shows "(n #+ 1)⋅x = n⋅x ⊕ x" and "(n #+ 1)⋅x = x ⊕ n⋅x"
proof -
from assms(2) have I: "∀k∈n #+ 1. x ∈ G" by simp
with assms(1) have "(∑{⟨k,x⟩. k ∈ n #+ 1}) = x ⊕ (∑{⟨k,x⟩. k∈n})"
by (rule seq_sum_pull_one_elem)
thus "(n #+ 1)⋅x = x ⊕ n⋅x" by simp
from assms(1) I have "(∑{⟨k,x⟩. k∈n #+ 1}) = (∑{⟨k,x⟩. k∈n}) ⊕ x"
by (rule seq_sum_pull_one_elem)
thus "(n #+ 1)⋅x = n⋅x ⊕ x" by simp
qed
text‹One element of a monoid is that element.›
lemma (in monoid1) nat_mult_one: assumes "x∈G" shows "1⋅x = x"
proof -
from assms have "(0 #+ 1)⋅x = 0⋅x ⊕ x" using nat_mult_add_one(1) by blast
with assms show ?thesis using nat_mult_zero unit_is_neutral by simp
qed
text‹Multiplication of $x$ by a natural number induces a homomorphism between natural numbers
with addition and and the natural multiples of $x$. ›
lemma (in monoid1) nat_mult_add: assumes "n∈nat" "m∈nat" "x∈G"
shows "(n #+ m)⋅x = n⋅x ⊕ m⋅x"
proof -
from assms have "m∈nat" and "(n #+ 0)⋅x = n⋅x ⊕ 0⋅x"
using nat_mult_type unit_is_neutral nat_mult_zero by simp_all
moreover from assms(1,3) have
"∀k∈nat. (n #+ k)⋅x = n⋅x ⊕ k⋅x ⟶ (n #+ (k #+ 1))⋅x = n⋅x ⊕ (k #+ 1)⋅x"
using nat_mult_type nat_mult_add_one(1) sum_associative by simp
ultimately show ?thesis by (rule ind_on_nat1)
qed
end