IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Monoid_ZF_1 imports Monoid_ZF
begin

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}\)).

Notation and basic properties of sums of lists of monoid elements

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.

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 +

defines \( 0 \equiv \text{ TheNeutralElement}(G,f) \)

defines \( \sum s \equiv \text{Fold}(f, 0 ,s) \)

defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)

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 \( 0 \in G \) and \( f:G\times G \rightarrow G \) using monoidAssum, unit_is_neutral unfolding IsAmonoid_def, IsAssociative_def

The sum of a list of monoid elements is a monoid element.

lemma (in monoid1) sum_in_mono:

assumes \( n\in nat \), \( \forall k\in n.\ q(k)\in G \)

shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \in G \)proof
let \( a = \{\langle k,q(k)\rangle .\ k\in n\} \)
from assms have \( n \in nat \), \( f:G\times G \rightarrow G \), \( a:n \rightarrow G \), \( 0 \in G \), \( G\neq 0 \) using zero_monoid_oper, ZF_fun_from_total
then show \( thesis \) using fold_props
qed

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\rightarrow G \)

shows \( (\sum s) = 0 \) using assms, zero_monoid_oper, fold_empty, group0_1_L3A

For nonempty lists our \(\Sigma\) is the same as Fold1.

lemma (in monoid1) sum_nonempty:

assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \)proof
from assms have \( s(0) \in G \) using empty_in_every_succ, apply_funtype
with assms have \( (\sum s) = \text{Fold}(f, 0 \oplus s(0), \text{Tail}(s)) \) using zero_monoid_oper, fold_detach_first
with \( s(0) \in G \) show \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \) using unit_is_neutral
then show \( (\sum s) = \text{Fold1}(f,s) \) unfolding Fold1_def
qed

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 \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \)proof
from assms have \( s(0) \in G \) using empty_in_every_succ, apply_funtype
{
assume \( n=0 \)
with assms have \( \text{Tail}(s):0\rightarrow G \) using tail_props(1)
with assms, \( s(0) \in G \) have \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \) using sum_nonempty(1), sum_empty, zero_monoid_oper(2), group0_1_L3A, fold_empty, unit_is_neutral
}
moreover {
assume \( n\neq 0 \)
with assms(1) obtain \( m \) where \( m\in nat \) and \( n = succ(m) \) using Nat_ZF_1_L3
with assms have \( \text{Tail}(s):succ(m)\rightarrow G \) using tail_props(1)
let \( a = \{\langle 0,s(0)\rangle \} \)
from \( s(0) \in G \) have \( 0\in nat \), \( a:succ(0)\rightarrow G \) using pair_func_singleton, succ_explained
with \( m\in nat \), \( \text{Tail}(s):succ(m)\rightarrow G \) have \( f\langle \text{Fold1}(f,a), \text{Fold1}(f, \text{Tail}(s))\rangle = \text{Fold1}(f, \text{Concat}(a, \text{Tail}(s))) \) using semigr0_valid_in_monoid0, prod_conc_distr
with assms, \( a:succ(0)\rightarrow G \), \( m\in nat \), \( \text{Tail}(s):succ(m)\rightarrow G \) have \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \) using semigr0_valid_in_monoid0, prod_of_1elem, pair_val, sum_nonempty(2), first_concat_tail
} ultimately show \( thesis \)
qed

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 \in nat \), \( \forall k\in n + 1.\ q(k) \in G \)

shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \), \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \)proof
let \( s = \{\langle k,q(k)\rangle .\ k\in n + 1\} \)
from assms(1) have \( 0 \in n + 1 \) using empty_in_every_succ, succ_add_one(1)
then have \( s(0) = q(0) \) by (rule ZF_fun_from_tot_val1 )
from assms(2) have \( s: n + 1 \rightarrow G \) by (rule ZF_fun_from_total )
with assms(1), \( s(0) = q(0) \) have \( (\sum s) = q(0) \oplus (\sum \text{Tail}(s)) \) using seq_sum_pull_first0
moreover
from assms have \( \text{Tail}(s) = \{\langle k,q(k + 1)\rangle .\ k \in n\} \) using tail_formula
ultimately show \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \)
from assms show \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \) using zero_monoid_oper, fold_detach_last
qed

The sum of a singleton list is its only element,

lemma (in monoid1) seq_sum_singleton:

assumes \( q(0) \in G \)

shows \( (\sum \{\langle k,q(k)\rangle .\ k\in 1\}) = q(0) \)proof
from assms have \( 0\in nat \) and \( \forall k\in 0 + 1.\ q(k) \in G \)
then have \( (\sum \{\langle k,q(k)\rangle .\ k\in 0 + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in 0\}) \) by (rule seq_sum_pull_one_elem )
with assms show \( thesis \) using sum_empty, unit_is_neutral
qed

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 \text{ is commutative on } G \), \( n\in nat \) and \( a : n + 1 \rightarrow G \), \( b : n + 1 \rightarrow G \), \( c : n + 1 \rightarrow G \) and \( \forall j\in n + 1.\ c(j) = a(j) \oplus b(j) \)

shows \( (\sum c) = (\sum a) \oplus (\sum b) \) using assms, succ_add_one(1), sum_nonempty, semigr0_valid_in_monoid0, prod_comm_distrib

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 \text{ is commutative on } G \), \( n\in nat \) and \( \forall k\in n.\ p(k) \in G \), \( \forall k\in n.\ q(k) \in G \)

shows \( (\sum \{\langle k,p(k)\oplus q(k)\rangle .\ k\in n\}) = (\sum \{\langle k,p(k)\rangle .\ k\in n\}) \oplus (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \)proof
let \( a = \{\langle k,p(k)\rangle .\ k\in n\} \)
let \( b = \{\langle k,q(k)\rangle .\ k\in n\} \)
let \( c = \{\langle k,p(k)\oplus q(k)\rangle .\ k\in n\} \)
{
assume \( n=0 \)
then have \( (\sum c) = (\sum a) \oplus (\sum b) \) using sum_empty, unit_is_neutral
}
moreover {
assume \( n\neq 0 \)
with assms(2) obtain \( m \) where \( m\in nat \) and \( n = m + 1 \) using nat_not0_succ
from assms(3,4) have \( a:n\rightarrow G \), \( b:n\rightarrow G \), \( c:n\rightarrow G \) using group0_1_L1, ZF_fun_from_total
with assms(1), \( m\in nat \), \( n = m + 1 \) have \( f \text{ is commutative on } G \), \( m\in nat \) and \( a:m + 1\rightarrow G \), \( b:m + 1\rightarrow G \), \( c:m + 1\rightarrow G \)
moreover
have \( \forall k\in m + 1.\ c(k) = a(k) \oplus b(k) \)proof
{
fix \( k \)
assume \( k \in m + 1 \)
with \( n = m + 1 \) have \( k\in n \)
then have \( c(k) = a(k) \oplus b(k) \) using ZF_fun_from_tot_val1
}
thus \( thesis \)
qed
ultimately have \( (\sum c) = (\sum a) \oplus (\sum b) \) using sum_comm_distrib0
} ultimately show \( thesis \)
qed

Multiplying monoid elements by natural numbers

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.

The zero's multiple of a monoid element is its neutral element.

lemma (in monoid1) nat_mult_zero:

shows \( 0\cdot x = 0 \) using sum_empty

Any multiple of a monoid element is a monoid element.

lemma (in monoid1) nat_mult_type:

assumes \( n\in nat \), \( x\in G \)

shows \( n\cdot x \in G \) using assms, sum_in_mono

Taking one more multiple of \(x\) adds \(x\).

lemma (in monoid1) nat_mult_add_one:

assumes \( n\in nat \), \( x\in G \)

shows \( (n + 1)\cdot x = n\cdot x \oplus x \) and \( (n + 1)\cdot x = x \oplus n\cdot x \)proof
from assms(2) have I: \( \forall k\in n + 1.\ x \in G \)
with assms(1) have \( (\sum \{\langle k,x\rangle .\ k \in n + 1\}) = x \oplus (\sum \{\langle k,x\rangle .\ k\in n\}) \) by (rule seq_sum_pull_one_elem )
thus \( (n + 1)\cdot x = x \oplus n\cdot x \)
from assms(1), I have \( (\sum \{\langle k,x\rangle .\ k\in n + 1\}) = (\sum \{\langle k,x\rangle .\ k\in n\}) \oplus x \) by (rule seq_sum_pull_one_elem )
thus \( (n + 1)\cdot x = n\cdot x \oplus x \)
qed

One element of a monoid is that element.

lemma (in monoid1) nat_mult_one:

assumes \( x\in G \)

shows \( 1\cdot x = x \)proof
from assms have \( (0 + 1)\cdot x = 0\cdot x \oplus x \) using nat_mult_add_one(1)
with assms show \( thesis \) using nat_mult_zero, unit_is_neutral
qed

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\in nat \), \( m\in nat \), \( x\in G \)

shows \( (n + m)\cdot x = n\cdot x \oplus m\cdot x \)proof
from assms have \( m\in nat \) and \( (n + 0)\cdot x = n\cdot x \oplus 0\cdot x \) using nat_mult_type, unit_is_neutral, nat_mult_zero
moreover
from assms(1,3) have \( \forall k\in nat.\ (n + k)\cdot x = n\cdot x \oplus k\cdot x \longrightarrow (n + (k + 1))\cdot x = n\cdot x \oplus (k + 1)\cdot x \) using nat_mult_type, nat_mult_add_one(1), sum_associative
ultimately show \( thesis \) by (rule ind_on_nat1 )
qed
end
lemma (in monoid0) unit_is_neutral:

assumes \( e = \text{ TheNeutralElement}(G,f) \)

shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)
Definition of IsAmonoid: \( \text{IsAmonoid}(G,f) \equiv \) \( f \text{ is associative on } G \wedge \) \( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative: \( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \) \( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \) \( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in monoid1) zero_monoid_oper: shows \( 0 \in G \) and \( f:G\times G \rightarrow G \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
theorem fold_props:

assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \), \( x\in X \), \( Y\neq 0 \)

shows \( \text{Fold}(f,x,a) = \text{FoldSeq}(f,x,a)(n) \) and \( \text{Fold}(f,x,a) \in X \)
theorem fold_empty:

assumes \( f : X\times Y \rightarrow X \) and \( a:0\rightarrow Y \), \( x\in X \), \( Y\neq 0 \)

shows \( \text{Fold}(f,x,a) = x \)
lemma (in monoid0) group0_1_L3A: shows \( G\neq 0 \)
lemma empty_in_every_succ:

assumes \( n \in nat \)

shows \( 0 \in succ(n) \)
lemma fold_detach_first:

assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( y:succ(n)\rightarrow Y \), \( x\in X \)

shows \( \text{Fold}(f,x,y) = \text{Fold}(f,f\langle x,y(0)\rangle , \text{Tail}(y)) \)
Definition of Fold1: \( \text{Fold1}(f,a) \equiv \text{Fold}(f,a(0), \text{Tail}(a)) \)
theorem tail_props:

assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)

shows \( \text{Tail}(a) : n \rightarrow X \), \( \forall k \in n.\ \text{Tail}(a)(k) = a(succ(k)) \)
lemma (in monoid1) sum_nonempty:

assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \)
lemma (in monoid1) sum_empty:

assumes \( s:0\rightarrow G \)

shows \( (\sum s) = 0 \)
lemma (in monoid1) zero_monoid_oper: shows \( 0 \in G \) and \( f:G\times G \rightarrow G \)
lemma Nat_ZF_1_L3:

assumes \( n \in nat \) and \( n\neq 0 \)

shows \( \exists k\in nat.\ n = succ(k) \)
lemma pair_func_singleton:

assumes \( y \in Y \)

shows \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \)
lemma succ_explained: shows \( succ(n) = n \cup \{n\} \)
lemma (in monoid0) semigr0_valid_in_monoid0: shows \( semigr0(G,f) \)
theorem (in semigr0) prod_conc_distr:

assumes \( n \in nat \), \( k \in nat \) and \( a : succ(n) \rightarrow G \), \( b: succ(k) \rightarrow G \)

shows \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \)
lemma (in semigr0) prod_of_1elem:

assumes \( a: 1 \rightarrow G \)

shows \( (\prod a) = a(0) \)
lemma pair_val: shows \( \{\langle x,y\rangle \}(x) = y \)
lemma (in monoid1) sum_nonempty:

assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \)
lemma first_concat_tail:

assumes \( n\in nat \), \( a:succ(n)\rightarrow X \)

shows \( a = \text{Concat}(\{\langle 0,a(0)\rangle \}, \text{Tail}(a)) \)
lemma succ_add_one:

assumes \( n\in nat \)

shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \)
lemma ZF_fun_from_tot_val1:

assumes \( x\in X \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \)
lemma (in monoid1) seq_sum_pull_first0:

assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \)
lemma tail_formula:

assumes \( n \in nat \) and \( \forall k \in n + 1.\ q(k) \in X \)

shows \( \text{Tail}(\{\langle k,q(k)\rangle .\ k \in n + 1\}) = \{\langle k,q(k + 1)\rangle .\ k \in n\} \)
lemma fold_detach_last:

assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( x\in X \), \( \forall k\in n + 1.\ q(k) \in Y \)

shows \( \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n + 1\}) = f\langle \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n\}), q(n)\rangle \)
theorem (in monoid1) seq_sum_pull_one_elem:

assumes \( n \in nat \), \( \forall k\in n + 1.\ q(k) \in G \)

shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \), \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \)
lemma (in monoid1) sum_nonempty:

assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)

shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \)
theorem (in semigr0) prod_comm_distrib:

assumes \( f \text{ is commutative on } G \) and \( n\in nat \) and \( a : succ(n)\rightarrow G \), \( b : succ(n)\rightarrow G \), \( c : succ(n)\rightarrow G \) and \( \forall j\in succ(n).\ c(j) = a(j) \cdot b(j) \)

shows \( (\prod c) = (\prod a) \cdot (\prod b) \)
lemma nat_not0_succ:

assumes \( n\in nat \), \( n\neq 0 \)

shows \( \exists m\in nat.\ n = m #+1 \)
lemma (in monoid0) group0_1_L1:

assumes \( a\in G \), \( b\in G \)

shows \( a\oplus b \in G \)
lemma (in monoid1) sum_comm_distrib0:

assumes \( f \text{ is commutative on } G \), \( n\in nat \) and \( a : n + 1 \rightarrow G \), \( b : n + 1 \rightarrow G \), \( c : n + 1 \rightarrow G \) and \( \forall j\in n + 1.\ c(j) = a(j) \oplus b(j) \)

shows \( (\sum c) = (\sum a) \oplus (\sum b) \)
lemma (in monoid1) sum_in_mono:

assumes \( n\in nat \), \( \forall k\in n.\ q(k)\in G \)

shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \in G \)
lemma (in monoid1) nat_mult_add_one:

assumes \( n\in nat \), \( x\in G \)

shows \( (n + 1)\cdot x = n\cdot x \oplus x \) and \( (n + 1)\cdot x = x \oplus n\cdot x \)
lemma (in monoid1) nat_mult_zero: shows \( 0\cdot x = 0 \)
lemma (in monoid1) nat_mult_type:

assumes \( n\in nat \), \( x\in G \)

shows \( n\cdot x \in G \)
lemma (in monoid0) sum_associative:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( (a\oplus b)\oplus c = a\oplus (b\oplus c) \)
lemma ind_on_nat1:

assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)

shows \( P(n) \)