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

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:

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