IsarMathLib

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

theory Semigroup_ZF imports Partitions_ZF Fold_ZF Enumeration_ZF
begin

It seems that the minimal setup needed to talk about a product of a sequence is a set with a binary operation. Such object is called "magma". However, interesting properties show up when the binary operation is associative and such alebraic structure is called a semigroup. In this theory file we define and study sequences of partial products of sequences of magma and semigroup elements.

Products of sequences of semigroup elements

Semigroup is a a magma in which the binary operation is associative. In this section we mostly study the products of sequences of elements of semigroup. The goal is to establish the fact that taking the product of a sequence is distributive with respect to concatenation of sequences, i.e for two sequences \(a,b\) of the semigroup elements we have \(\prod (a\sqcup b) = (\prod a)\cdot (\prod b)\), where "\(a \sqcup b\)" is concatenation of \(a\) and \(b\) (\(a\)\( ++ \)\(b\) in Haskell notation). Less formally, we want to show that we can discard parantheses in expressions of the form \((a_0\cdot a_1\cdot .. \cdot a_n)\cdot (b_0\cdot .. \cdot b_k)\).

First we define a notion similar to Fold, except that that the initial element of the fold is given by the first element of sequence. By analogy with Haskell fold we call that Fold1

definition

\( \text{Fold1}(f,a) \equiv \text{Fold}(f,a(0), \text{Tail}(a)) \)

The definition of the semigr0 context below introduces notation for writing about finite sequences and semigroup products. In the context we fix the carrier and denote it \(G\). The binary operation on \(G\) is called \(f\). All theorems proven in the context semigr0 will implicitly assume that \(f\) is an associative operation on \(G\). We will use multiplicative notation for the semigroup operation. The product of a sequence \(a\) is denoted \(\prod a\). We will write \(a\hookleftarrow x\) for the result of appending an element \(x\) to the finite sequence (list) \(a\). This is a bit nonstandard, but I don't have a better idea for the "append" notation. Finally, \(a\sqcup b\) will denote the concatenation of the lists \(a\) and \(b\).

locale semigr0

assumes assoc_assum: \( f \text{ is associative on } G \)

defines \( x \cdot y \equiv f\langle x,y\rangle \)

defines \( \prod a \equiv \text{Fold1}(f,a) \)

defines \( a \hookleftarrow x \equiv \text{Append}(a,x) \)

defines \( a \sqcup b \equiv \text{Concat}(a,b) \)

The next lemma shows our assumption on the associativity of the semigroup operation in the notation defined in in the semigr0 context.

lemma (in semigr0) semigr_assoc:

assumes \( x \in G \), \( y \in G \), \( z \in G \)

shows \( x\cdot y\cdot z = x\cdot (y\cdot z) \) using assms, assoc_assum, IsAssociative_def

In the way we define associativity the assumption that \(f\) is associative on \(G\) also implies that it is a binary operation on \(X\).

lemma (in semigr0) semigr_binop:

shows \( f : G\times G \rightarrow G \) using assoc_assum, IsAssociative_def

Semigroup operation is closed.

lemma (in semigr0) semigr_closed:

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

shows \( a\cdot b \in G \) using assms, semigr_binop, apply_funtype

Lemma append_1elem written in the notation used in the semigr0 context.

lemma (in semigr0) append_1elem_nice:

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

shows \( a \sqcup b = a \hookleftarrow b(0) \) using assms, append_1elem

Lemma concat_init_last_elem rewritten in the notation used in the semigr0 context.

lemma (in semigr0) concat_init_last:

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

shows \( (a \sqcup \text{Init}(b)) \hookleftarrow b(k) = a \sqcup b \) using assms, concat_init_last_elem

The product of semigroup (actually, magma -- we don't need associativity for this) elements is in the semigroup.

lemma (in semigr0) prod_type:

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

shows \( (\prod a) \in G \)proof
from assms have \( succ(n) \in nat \), \( f : G\times G \rightarrow G \), \( \text{Tail}(a) : n \rightarrow G \) using semigr_binop, tail_props
moreover
from assms have \( a(0) \in G \) and \( G \neq 0 \) using empty_in_every_succ, apply_funtype
ultimately show \( (\prod a) \in G \) using Fold1_def, fold_props
qed

What is the product of one element list?

lemma (in semigr0) prod_of_1elem:

assumes A1: \( a: 1 \rightarrow G \)

shows \( (\prod a) = a(0) \)proof
have \( f : G\times G \rightarrow G \) using semigr_binop
moreover
from A1 have \( \text{Tail}(a) : 0 \rightarrow G \) using tail_props
moreover
from A1 have \( a(0) \in G \) and \( G \neq 0 \) using apply_funtype
ultimately show \( (\prod a) = a(0) \) using fold_empty, Fold1_def
qed

What happens to the product of a list when we append an element to the list?

lemma (in semigr0) prod_append:

assumes A1: \( n \in nat \) and A2: \( a : succ(n) \rightarrow G \) and A3: \( x\in G \)

shows \( (\prod a\hookleftarrow x) = (\prod a) \cdot x \)proof
from A1, A2 have I: \( \text{Tail}(a) : n \rightarrow G \), \( a(0) \in G \) using tail_props, empty_in_every_succ, apply_funtype
from assms have \( (\prod a\hookleftarrow x) = \text{Fold}(f,a(0), \text{Tail}(a)\hookleftarrow x) \) using head_of_append, tail_append_commute, Fold1_def
also
from A1, A3, I have \( \ldots = (\prod a) \cdot x \) using semigr_binop, fold_append, Fold1_def
finally show \( thesis \)
qed

The main theorem of the section: taking the product of a sequence is distributive with respect to concatenation of sequences. The proof is by induction on the length of the second list.

theorem (in semigr0) prod_conc_distr:

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

shows \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \)proof
from A1 have \( k \in nat \)
moreover
have \( \forall b \in succ(0) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \)proof
{
fix \( b \)
assume A3: \( b : succ(0) \rightarrow G \)
with A1, A2 have \( succ(n) \in nat \), \( a : succ(n) \rightarrow G \), \( b : 1 \rightarrow G \)
then have \( a \sqcup b = a \hookleftarrow b(0) \) by (rule append_1elem_nice )
with A1, A2, A3 have \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \) using apply_funtype, prod_append, semigr_binop, prod_of_1elem
}
thus \( thesis \)
qed
moreover
have \( \forall j \in nat.\ \) \( (\forall b \in succ(j) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b)) \longrightarrow \) \( (\forall b \in succ(succ(j)) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b)) \)proof
{
fix \( j \)
assume A4: \( j \in nat \) and A5: \( (\forall b \in succ(j) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b)) \)
{
fix \( b \)
assume A6: \( b : succ(succ(j)) \rightarrow G \)
let \( c = \text{Init}(b) \)
from A4, A6 have T: \( b(succ(j)) \in G \) and I: \( c : succ(j) \rightarrow G \) and II: \( b = c\hookleftarrow b(succ(j)) \) using apply_funtype, init_props
from A1, A2, A4, A6 have \( succ(n) \in nat \), \( succ(j) \in nat \), \( a : succ(n) \rightarrow G \), \( b : succ(succ(j)) \rightarrow G \)
then have III: \( (a \sqcup c) \hookleftarrow b(succ(j)) = a \sqcup b \) by (rule concat_init_last )
from A4, I, T have \( (\prod c\hookleftarrow b(succ(j))) = (\prod c) \cdot b(succ(j)) \) by (rule prod_append )
with II have \( (\prod a) \cdot (\prod b) = (\prod a) \cdot ((\prod c) \cdot b(succ(j))) \)
moreover
from A1, A2, A4, T, I have \( (\prod a) \in G \), \( (\prod c) \in G \), \( b(succ(j)) \in G \) using prod_type
ultimately have \( (\prod a) \cdot (\prod b) = ((\prod a) \cdot (\prod c)) \cdot b(succ(j)) \) using semigr_assoc
with A5, I have \( (\prod a) \cdot (\prod b) = (\prod (a \sqcup c))\cdot b(succ(j)) \)
moreover
from A1, A2, A4, I have T1: \( succ(n) \in nat \), \( succ(j) \in nat \) and \( a : succ(n) \rightarrow G \), \( c : succ(j) \rightarrow G \)
then have \( \text{Concat}(a,c): succ(n) + succ(j) \rightarrow G \) by (rule concat_props )
with A1, A4, T have \( succ(n + j) \in nat \), \( a \sqcup c : succ(succ(n #+j)) \rightarrow G \), \( b(succ(j)) \in G \) using succ_plus
then have \( (\prod (a \sqcup c)\hookleftarrow b(succ(j))) = (\prod (a \sqcup c))\cdot b(succ(j)) \) by (rule prod_append )
with III have \( (\prod (a \sqcup c))\cdot b(succ(j)) = \prod (a \sqcup b) \)
ultimately have \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \)
}
hence \( (\forall b \in succ(succ(j)) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b)) \)
}
thus \( thesis \)
qed
ultimately have \( \forall b \in succ(k) \rightarrow G.\ (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \) by (rule ind_on_nat )
with A2 show \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \)
qed

\(a\cdot b \cdot (c\cdot d) = a\cdot (b \cdot c) \cdot d\) for semigrouop elements \(a,b,c,d \in G\). The Commutative semigroups section below contains a couple of rearrangements that need commutativity of the semigroup operation, but this one uses only associativity, so it's here.

lemma (in semigr0) rearr4elem_assoc:

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

shows \( a\cdot b\cdot (c\cdot d) = a\cdot (b\cdot c)\cdot d \)proof
from assms have \( a\cdot b\cdot (c\cdot d) = a\cdot b\cdot c\cdot d \) using semigr_closed, semigr_assoc
with assms(1,2,3) show \( thesis \) using semigr_assoc
qed

Products over sets of indices

In this section we study the properties of expressions of the form \(\prod_{i\in \Lambda} a_i = a_{i_0}\cdot a_{i_1} \cdot .. \cdot a_{i-1}\), i.e. what we denote as \( \prod (\Lambda ,a) \). \(\Lambda\) here is a finite subset of some set \(X\) and \(a\) is a function defined on \(X\) with values in the semigroup \(G\).

Suppose \(a: X \rightarrow G\) is an indexed family of elements of a semigroup \(G\) and \(\Lambda = \{i_0, i_1, .. , i_{n-1}\} \subseteq \mathbb{N}\) is a finite set of indices. We want to define \(\prod_{i\in \Lambda} a_i = a_{i_0}\cdot a_{i_1} \cdot .. \cdot a_{i-1}\). To do that we use the notion of Enumeration defined in the Enumeration_ZF theory file that takes a set of indices and lists them in increasing order, thus converting it to list. Then we use the Fold1 to multiply the resulting list. Recall that in Isabelle/ZF the capital letter ''O'' denotes the composition of two functions (or relations).

definition

\( \text{SetFold}(f,a,\Lambda ,r) = \text{Fold1}(f,a\circ \text{Enumeration}(\Lambda ,r)) \)

For a finite subset \(\Lambda\) of a linearly ordered set \(X\) we will write \(\sigma (\Lambda )\) to denote the enumeration of the elements of \(\Lambda\), i.e. the only order isomorphism \(|\Lambda | \rightarrow \Lambda\), where \(|\Lambda | \in \mathbb{N}\) is the number of elements of \(\Lambda \). We also define notation for taking a product over a set of indices of some sequence of semigroup elements. The product of semigroup elements over some set \(\Lambda \subseteq X\) of indices of a sequence \(a: X \rightarrow G\) (i.e. \(\prod_{i\in \Lambda} a_i\)) is denoted \( \prod (\Lambda ,a) \). In the semigr1 context we assume that \(a\) is a function defined on some linearly ordered set \(X\) with values in the semigroup \(G\).

locale semigr1 = semigr0 +

assumes linord: \( \text{IsLinOrder}(X,r) \)

assumes a_is_fun: \( a : X \rightarrow G \)

defines \( \sigma (A) \equiv \text{Enumeration}(A,r) \)

defines \( \prod (\Lambda ,b) \equiv \text{SetFold}(f,b,\Lambda ,r) \)

We can use the enums locale in the semigr0 context.

lemma (in semigr1) enums_valid_in_semigr1:

shows \( enums(X,r) \) using linord, enums_def

Definition of product over a set expressed in notation of the semigr0 locale.

lemma (in semigr1) setproddef:

shows \( \prod (\Lambda ,a) = \prod (a\circ \sigma (\Lambda )) \) using SetFold_def

A composition of enumeration of a nonempty finite subset of \(\mathbb{N}\) with a sequence of elements of \(G\) is a nonempty list of elements of \(G\). This implies that a product over set of a finite set of indices belongs to the (carrier of) semigroup.

lemma (in semigr1) setprod_type:

assumes A1: \( \Lambda \in \text{FinPow}(X) \) and A2: \( \Lambda \neq 0 \)

shows \( \exists n \in nat .\ |\Lambda | = succ(n) \wedge a\circ \sigma (\Lambda ) : succ(n) \rightarrow G \) and \( \prod (\Lambda ,a) \in G \)proof
from assms obtain \( n \) where \( n \in nat \) and \( |\Lambda | = succ(n) \) using card_non_empty_succ
from A1 have \( \sigma (\Lambda ) : |\Lambda | \rightarrow \Lambda \) using enums_valid_in_semigr1, enum_props
with A1 have \( a\circ \sigma (\Lambda ): |\Lambda | \rightarrow G \) using a_is_fun, FinPow_def, comp_fun_subset
with \( n \in nat \), and, \( |\Lambda | = succ(n) \) show \( \exists n \in nat .\ |\Lambda | = succ(n) \wedge a\circ \sigma (\Lambda ) : succ(n) \rightarrow G \)
from \( n \in nat \), \( |\Lambda | = succ(n) \), \( a\circ \sigma (\Lambda ): |\Lambda | \rightarrow G \) show \( \prod (\Lambda ,a) \in G \) using prod_type, setproddef
qed

The enum_append lemma from the Enemeration theory specialized for natural numbers.

lemma (in semigr1) semigr1_enum_append:

assumes \( \Lambda \in \text{FinPow}(X) \) and \( n \in X - \Lambda \) and \( \forall k\in \Lambda .\ \langle k,n\rangle \in r \)

shows \( \sigma (\Lambda \cup \{n\}) = \sigma (\Lambda )\hookleftarrow n \) using assms, FinPow_def, enums_valid_in_semigr1, enum_append

What is product over a singleton?

lemma (in semigr1) gen_prod_singleton:

assumes A1: \( x \in X \)

shows \( \prod (\{x\},a) = a(x) \)proof
from A1 have \( \sigma (\{x\}): 1 \rightarrow X \) and \( \sigma (\{x\})(0) = x \) using enums_valid_in_semigr1, enum_singleton
then show \( \prod (\{x\},a) = a(x) \) using a_is_fun, comp_fun, setproddef, prod_of_1elem, comp_fun_apply
qed

A generalization of prod_append to the products over sets of indices.

lemma (in semigr1) gen_prod_append:

assumes A1: \( \Lambda \in \text{FinPow}(X) \) and A2: \( \Lambda \neq 0 \) and A3: \( n \in X - \Lambda \) and A4: \( \forall k\in \Lambda .\ \langle k,n\rangle \in r \)

shows \( \prod (\Lambda \cup \{n\}, a) = (\prod (\Lambda ,a)) \cdot a(n) \)proof
have \( \prod (\Lambda \cup \{n\}, a) = \prod (a\circ \sigma (\Lambda \cup \{n\})) \) using setproddef
also
from A1, A3, A4 have \( \ldots = \prod (a\circ (\sigma (\Lambda )\hookleftarrow n)) \) using semigr1_enum_append
also
have \( \ldots = \prod ((a\circ \sigma (\Lambda ))\hookleftarrow a(n)) \)proof
from A1, A3 have \( |\Lambda | \in nat \) and \( \sigma (\Lambda ) : |\Lambda | \rightarrow X \) and \( n \in X \) using card_fin_is_nat, enums_valid_in_semigr1, enum_fun
then show \( thesis \) using a_is_fun, list_compose_append
qed
also
from assms have \( \ldots = (\prod (a\circ \sigma (\Lambda )))\cdot a(n) \) using a_is_fun, setprod_type, apply_funtype, prod_append
also
have \( \ldots = (\prod (\Lambda ,a)) \cdot a(n) \) using SetFold_def
finally show \( \prod (\Lambda \cup \{n\}, a) = (\prod (\Lambda ,a)) \cdot a(n) \)
qed

Very similar to gen_prod_append: a relation between a product over a set of indices and the product over the set with the maximum removed.

lemma (in semigr1) gen_product_rem_point:

assumes A1: \( A \in \text{FinPow}(X) \) and A2: \( n \in A \) and A4: \( A - \{n\} \neq 0 \) and A3: \( \forall k\in A.\ \langle k, n\rangle \in r \)

shows \( (\prod (A - \{n\},a)) \cdot a(n) = \prod (A, a) \)proof
let \( \Lambda = A - \{n\} \)
from A1, A2 have \( \Lambda \in \text{FinPow}(X) \) and \( n \in X - \Lambda \) using fin_rem_point_fin, FinPow_def
with A3, A4 have \( \prod (\Lambda \cup \{n\}, a) = (\prod (\Lambda ,a)) \cdot a(n) \) using a_is_fun, gen_prod_append
with A2 show \( thesis \) using rem_add_eq
qed

Commutative semigroups

Commutative semigroups are those whose operation is commutative, i.e. \(a\cdot b = b\cdot a\). This implies that for any permutation \(s : n \rightarrow n\) we have \(\prod_{j=0}^n a_j = \prod_{j=0}^n a_{s (j)}\), or, closer to the notation we are using in the semigr0 context, \(\prod a = \prod (a \circ s )\). Maybe one day we will be able to prove this, but for now the goal is to prove something simpler: that if the semigroup operation is commutative taking the product of a sequence is distributive with respect to the operation: \(\prod_{j=0}^n (a_j\cdot b_j) = \left(\prod_{j=0}^n a_j)\right) \left(\prod_{j=0}^n b_j)\right)\). Many of the rearrangements (namely those that don't use the inverse) proven in the AbelianGroup_ZF theory hold in fact in semigroups. Some of them will be reproven in this section.

A rearrangement with 3 elements.

lemma (in semigr0) rearr3elems:

assumes \( f \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = a\cdot c\cdot b \) using assms, semigr_assoc, IsCommutative_def

A rearrangement of four elements.

lemma (in semigr0) rearr4elems:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \)proof
from A2 have \( a\cdot b\cdot (c\cdot d) = a\cdot b\cdot c\cdot d \) using semigr_closed, semigr_assoc
also
have \( a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d) \)proof
from A1, A2 have \( a\cdot b\cdot c\cdot d = c\cdot (a\cdot b)\cdot d \) using IsCommutative_def, semigr_closed
also
from A2 have \( \ldots = c\cdot a\cdot b\cdot d \) using semigr_closed, semigr_assoc
also
from A1, A2 have \( \ldots = a\cdot c\cdot b\cdot d \) using IsCommutative_def, semigr_closed
also
from A2 have \( \ldots = a\cdot c\cdot (b\cdot d) \) using semigr_closed, semigr_assoc
finally show \( a\cdot b\cdot c\cdot d = a\cdot c\cdot (b\cdot d) \)
qed
finally show \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \)
qed

We start with a version of prod_append that will shorten a bit the proof of the main theorem.

lemma (in semigr0) shorter_seq:

assumes A1: \( k \in nat \) and A2: \( a \in succ(succ(k)) \rightarrow G \)

shows \( (\prod a) = (\prod \text{Init}(a)) \cdot a(succ(k)) \)proof
let \( x = \text{Init}(a) \)
from assms have \( a(succ(k)) \in G \) and \( x : succ(k) \rightarrow G \) using apply_funtype, init_props
with A1 have \( (\prod x\hookleftarrow a(succ(k))) = (\prod x) \cdot a(succ(k)) \) using prod_append
with assms show \( thesis \) using init_props
qed

A lemma useful in the induction step of the main theorem.

lemma (in semigr0) prod_distr_ind_step:

assumes A1: \( k \in nat \) and A2: \( a : succ(succ(k)) \rightarrow G \) and A3: \( b : succ(succ(k)) \rightarrow G \) and A4: \( c : succ(succ(k)) \rightarrow G \) and A5: \( \forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j) \)

shows \( \text{Init}(a) : succ(k) \rightarrow G \), \( \text{Init}(b) : succ(k) \rightarrow G \), \( \text{Init}(c) : succ(k) \rightarrow G \), \( \forall j\in succ(k).\ \text{Init}(c)(j) = \text{Init}(a)(j) \cdot \text{Init}(b)(j) \)proof
from A1, A2, A3, A4 show \( \text{Init}(a) : succ(k) \rightarrow G \), \( \text{Init}(b) : succ(k) \rightarrow G \), \( \text{Init}(c) : succ(k) \rightarrow G \) using init_props
from A1 have T: \( succ(k) \in nat \)
from T, A2 have \( \forall j\in succ(k).\ \text{Init}(a)(j) = a(j) \) by (rule init_props )
moreover
from T, A3 have \( \forall j\in succ(k).\ \text{Init}(b)(j) = b(j) \) by (rule init_props )
moreover
from T, A4 have \( \forall j\in succ(k).\ \text{Init}(c)(j) = c(j) \) by (rule init_props )
moreover
from A5 have \( \forall j\in succ(k).\ c(j) = a(j) \cdot b(j) \)
ultimately show \( \forall j\in succ(k).\ \text{Init}(c)(j) = \text{Init}(a)(j) \cdot \text{Init}(b)(j) \)
qed

For commutative operations taking the product of a sequence is distributive with respect to the operation. This version will probably not be used in applications, it is formulated in a way that is easier to prove by induction. For a more convenient formulation see prod_comm_distrib. The proof by induction on the length of the sequence.

theorem (in semigr0) prod_comm_distr:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( n\in nat \)

shows \( \forall a b c.\ \) \( (a : succ(n)\rightarrow G \wedge b : succ(n)\rightarrow G \wedge c : succ(n)\rightarrow G \wedge \) \( (\forall j\in succ(n).\ c(j) = a(j) \cdot b(j))) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b) \)proof
note A2
moreover
have \( \forall a b c.\ \) \( (a : succ(0)\rightarrow G \wedge b : succ(0)\rightarrow G \wedge c : succ(0)\rightarrow G \wedge \) \( (\forall j\in succ(0).\ c(j) = a(j) \cdot b(j))) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b) \)proof
{
fix \( a \) \( b \) \( c \)
assume \( a : succ(0)\rightarrow G \wedge b : succ(0)\rightarrow G \wedge c : succ(0)\rightarrow G \wedge \) \( (\forall j\in succ(0).\ c(j) = a(j) \cdot b(j)) \)
then have I: \( a : 1\rightarrow G \), \( b : 1\rightarrow G \), \( c : 1\rightarrow G \) and II: \( c(0) = a(0) \cdot b(0) \)
from I have \( (\prod a) = a(0) \) and \( (\prod b) = b(0) \) and \( (\prod c) = c(0) \) using prod_of_1elem
with II have \( (\prod c) = (\prod a) \cdot (\prod b) \)
}
then show \( thesis \) using Fold1_def
qed
moreover
have \( \forall k \in nat.\ \) \( (\forall a b c.\ \) \( (a : succ(k)\rightarrow G \wedge b : succ(k)\rightarrow G \wedge c : succ(k)\rightarrow G \wedge \) \( (\forall j\in succ(k).\ c(j) = a(j) \cdot b(j))) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b)) \longrightarrow \) \( (\forall a b c.\ \) \( (a : succ(succ(k))\rightarrow G \wedge b : succ(succ(k))\rightarrow G \wedge c : succ(succ(k))\rightarrow G \wedge \) \( (\forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j))) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b)) \)proof
fix \( k \)
assume \( k \in nat \)
show \( (\forall a b c.\ \) \( a \in succ(k) \rightarrow G \wedge \) \( b \in succ(k) \rightarrow G \wedge c \in succ(k) \rightarrow G \wedge \) \( (\forall j\in succ(k).\ c(j) = a(j) \cdot b(j)) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b)) \longrightarrow \) \( (\forall a b c.\ \) \( a \in succ(succ(k)) \rightarrow G \wedge \) \( b \in succ(succ(k)) \rightarrow G \wedge \) \( c \in succ(succ(k)) \rightarrow G \wedge \) \( (\forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j)) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b)) \)proof
assume A3: \( \forall a b c.\ \) \( a \in succ(k) \rightarrow G \wedge \) \( b \in succ(k) \rightarrow G \wedge c \in succ(k) \rightarrow G \wedge \) \( (\forall j\in succ(k).\ c(j) = a(j) \cdot b(j)) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b) \)
show \( \forall a b c.\ \) \( a \in succ(succ(k)) \rightarrow G \wedge \) \( b \in succ(succ(k)) \rightarrow G \wedge \) \( c \in succ(succ(k)) \rightarrow G \wedge \) \( (\forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j)) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b) \)proof
{
fix \( a \) \( b \) \( c \)
assume \( a \in succ(succ(k)) \rightarrow G \wedge \) \( b \in succ(succ(k)) \rightarrow G \wedge \) \( c \in succ(succ(k)) \rightarrow G \wedge \) \( (\forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j)) \)
with \( k \in nat \) have I: \( a : succ(succ(k)) \rightarrow G \), \( b : succ(succ(k)) \rightarrow G \), \( c : succ(succ(k)) \rightarrow G \) and II: \( \forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j) \)
let \( x = \text{Init}(a) \)
let \( y = \text{Init}(b) \)
let \( z = \text{Init}(c) \)
from \( k \in nat \), I have III: \( (\prod a) = (\prod x) \cdot a(succ(k)) \), \( (\prod b) = (\prod y) \cdot b(succ(k)) \) and IV: \( (\prod c) = (\prod z) \cdot c(succ(k)) \) using shorter_seq
moreover
from \( k \in nat \), I, II have \( x : succ(k) \rightarrow G \), \( y : succ(k) \rightarrow G \), \( z : succ(k) \rightarrow G \) and \( \forall j\in succ(k).\ z(j) = x(j) \cdot y(j) \) using prod_distr_ind_step
with A3, II, IV have \( (\prod c) = (\prod x)\cdot (\prod y)\cdot (a(succ(k)) \cdot b(succ(k))) \)
moreover
from A1, \( k \in nat \), I, III have \( (\prod x)\cdot (\prod y)\cdot (a(succ(k)) \cdot b(succ(k)))=\) \( (\prod a) \cdot (\prod b) \) using init_props, prod_type, apply_funtype, rearr4elems
ultimately have \( (\prod c) = (\prod a) \cdot (\prod b) \)
}
thus \( thesis \)
qed
qed
qed
ultimately show \( thesis \) by (rule ind_on_nat )
qed

A reformulation of prod_comm_distr that is more convenient in applications.

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) \) using assms, prod_comm_distr

A product of two products over disjoint sets of indices is the product over the union.

lemma (in semigr1) prod_bisect:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( \Lambda \in \text{FinPow}(X) \)

shows \( \forall P \in \text{Bisections}(\Lambda ).\ \prod (\Lambda ,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a)) \)proof
have \( \text{IsLinOrder}(X,r) \) using linord
moreover
have \( \forall P \in \text{Bisections}(0).\ \prod (0,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a)) \) using bisec_empty
moreover
have \( \forall A \in \text{FinPow}(X).\ \) \( ( \forall n \in X - A.\ \) \( (\forall P \in \text{Bisections}(A).\ \prod (A,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a))) \) \( \wedge (\forall k\in A.\ \langle k,n\rangle \in r ) \longrightarrow \) \( (\forall Q \in \text{Bisections}(A \cup \{n\}).\ \) \( \prod (A \cup \{n\},a) = (\prod (\text{fst}(Q),a))\cdot (\prod (\text{snd}(Q),a)))) \)proof
{
fix \( A \)
assume \( A \in \text{FinPow}(X) \)
fix \( n \)
assume \( n \in X - A \)
have \( ( \forall P \in \text{Bisections}(A).\ \) \( \prod (A,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a))) \) \( \wedge (\forall k\in A.\ \langle k,n\rangle \in r ) \longrightarrow \) \( (\forall Q \in \text{Bisections}(A \cup \{n\}).\ \) \( \prod (A \cup \{n\},a) = (\prod (\text{fst}(Q),a))\cdot (\prod (\text{snd}(Q),a))) \)proof
{
assume I: \( \forall P \in \text{Bisections}(A).\ \prod (A,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a)) \) and II: \( \forall k\in A.\ \langle k,n\rangle \in r \)
have \( \forall Q \in \text{Bisections}(A \cup \{n\}).\ \) \( \prod (A \cup \{n\},a) = (\prod (\text{fst}(Q),a))\cdot (\prod (\text{snd}(Q),a)) \)proof
{
fix \( Q \)
assume \( Q \in \text{Bisections}(A \cup \{n\}) \)
let \( Q_0 = \text{fst}(Q) \)
let \( Q_1 = \text{snd}(Q) \)
from \( A \in \text{FinPow}(X) \), \( n \in X - A \) have \( A \cup \{n\} \in \text{FinPow}(X) \) using singleton_in_finpow, union_finpow
with \( Q \in \text{Bisections}(A \cup \{n\}) \) have \( Q_0 \in \text{FinPow}(X) \), \( Q_0 \neq 0 \) and \( Q_1 \in \text{FinPow}(X) \), \( Q_1 \neq 0 \) using bisect_fin, bisec_is_pair, Bisections_def
then have \( \prod (Q_0,a) \in G \) and \( \prod (Q_1,a) \in G \) using a_is_fun, setprod_type
from \( Q \in \text{Bisections}(A \cup \{n\}) \), \( A \in \text{FinPow}(X) \), \( n \in X-A \) have \( \text{refl}(X,r) \), \( Q_0 \subseteq A \cup \{n\} \), \( Q_1 \subseteq A \cup \{n\} \), \( A \subseteq X \) and \( n \in X \) using linord, IsLinOrder_def, total_is_refl, Bisections_def, FinPow_def
from \( \text{refl}(X,r) \), \( Q_0 \subseteq A \cup \{n\} \), \( A \subseteq X \), \( n \in X \), II have III: \( \forall k \in Q_0.\ \langle k, n\rangle \in r \) by (rule refl_add_point )
from \( \text{refl}(X,r) \), \( Q_1 \subseteq A \cup \{n\} \), \( A \subseteq X \), \( n \in X \), II have IV: \( \forall k \in Q_1.\ \langle k, n\rangle \in r \) by (rule refl_add_point )
from \( n \in X - A \), \( Q \in \text{Bisections}(A \cup \{n\}) \) have \( Q_0 = \{n\} \vee Q_1 = \{n\} \vee \langle Q_0 - \{n\},Q_1-\{n\}\rangle \in \text{Bisections}(A) \) using bisec_is_pair, bisec_add_point
moreover {
assume \( Q_1 = \{n\} \)
from \( n \in X - A \) have \( n \notin A \)
moreover
from \( Q \in \text{Bisections}(A \cup \{n\}) \) have \( \langle Q_0,Q_1 \rangle \in \text{Bisections}(A \cup \{n\}) \) using bisec_is_pair
with \( Q_1 = \{n\} \) have \( \langle Q_0, \{n\}\rangle \in \text{Bisections}(A \cup \{n\}) \)
ultimately have \( Q_0 = A \) and \( A \neq 0 \) using set_point_bisec
with \( A \in \text{FinPow}(X) \), \( n \in X - A \), II, \( Q_1 = \{n\} \) have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot \prod (Q_1,a) \) using a_is_fun, gen_prod_append, gen_prod_singleton
} moreover {
assume \( Q_0 = \{n\} \)
from \( n \in X - A \) have \( n \in X \)
then have \( \{n\} \in \text{FinPow}(X) \) and \( \{n\} \neq 0 \) using singleton_in_finpow
from \( n \in X - A \) have \( n \notin A \)
moreover
from \( Q \in \text{Bisections}(A \cup \{n\}) \) have \( \langle Q_0, Q_1\rangle \in \text{Bisections}(A \cup \{n\}) \) using bisec_is_pair
with \( Q_0 = \{n\} \) have \( \langle \{n\}, Q_1\rangle \in \text{Bisections}(A \cup \{n\}) \)
ultimately have \( Q_1 = A \) and \( A \neq 0 \) using point_set_bisec
with A1, \( A \in \text{FinPow}(X) \), \( n \in X - A \), II, \( \{n\} \in \text{FinPow}(X) \), \( \{n\} \neq 0 \), \( Q_0 = \{n\} \) have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot (\prod (Q_1,a)) \) using a_is_fun, gen_prod_append, gen_prod_singleton, setprod_type, IsCommutative_def
} moreover {
assume A4: \( \langle Q_0 - \{n\},Q_1 - \{n\}\rangle \in \text{Bisections}(A) \)
with \( A \in \text{FinPow}(X) \) have \( Q_0 - \{n\} \in \text{FinPow}(X) \), \( Q_0 - \{n\} \neq 0 \) and \( Q_1 - \{n\} \in \text{FinPow}(X) \), \( Q_1 - \{n\} \neq 0 \) using FinPow_def, Bisections_def
with \( n \in X - A \) have \( \prod (Q_0 - \{n\},a) \in G \), \( \prod (Q_1 - \{n\},a) \in G \) and T: \( a(n) \in G \) using a_is_fun, setprod_type, apply_funtype
from \( Q \in \text{Bisections}(A \cup \{n\}) \), A4 have \( (\langle Q_0, Q_1 - \{n\}\rangle \in \text{Bisections}(A) \wedge n \in Q_1) \vee \) \( (\langle Q_0 - \{n\}, Q_1\rangle \in \text{Bisections}(A) \wedge n \in Q_0) \) using bisec_is_pair, bisec_add_point_case3
moreover {
assume \( \langle Q_0, Q_1 - \{n\}\rangle \in \text{Bisections}(A) \) and \( n \in Q_1 \)
then have \( A \neq 0 \) using bisec_props
with A2, \( A \in \text{FinPow}(X) \), \( n \in X - A \), I, II, T, IV, \( \langle Q_0, Q_1 - \{n\}\rangle \in \text{Bisections}(A) \), \( \prod (Q_0,a) \in G \), \( \prod (Q_1 - \{n\},a) \in G \), \( Q_1 \in \text{FinPow}(X) \), \( n \in Q_1 \), \( Q_1 - \{n\} \neq 0 \) have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot (\prod (Q_1,a)) \) using gen_prod_append, semigr_assoc, gen_product_rem_point
} moreover {
assume \( \langle Q_0 - \{n\}, Q_1\rangle \in \text{Bisections}(A) \) and \( n \in Q_0 \)
then have \( A \neq 0 \) using bisec_props
with A1, A2, \( A \in \text{FinPow}(X) \), \( n \in X - A \), I, II, III, T, \( \langle Q_0 - \{n\}, Q_1\rangle \in \text{Bisections}(A) \), \( \prod (Q_0 - \{n\},a)\in G \), \( \prod (Q_1,a) \in G \), \( Q_0 \in \text{FinPow}(X) \), \( n \in Q_0 \), \( Q_0-\{n\}\neq 0 \) have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot (\prod (Q_1,a)) \) using gen_prod_append, rearr3elems, gen_product_rem_point
} ultimately have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot (\prod (Q_1,a)) \)
} ultimately have \( \prod (A \cup \{n\},a) = (\prod (Q_0,a))\cdot (\prod (Q_1,a)) \)
}
thus \( thesis \)
qed
}
thus \( thesis \)
qed
}
thus \( thesis \)
qed
moreover
note A2
ultimately show \( thesis \) by (rule fin_ind_add_max )
qed

A better looking reformulation of prod_bisect.

theorem (in semigr1) prod_disjoint:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and A3: \( B \in \text{FinPow}(X) \), \( B \neq 0 \) and A4: \( A \cap B = 0 \)

shows \( \prod (A\cup B,a) = (\prod (A,a))\cdot (\prod (B,a)) \)proof
from A2, A3, A4 have \( \langle A,B\rangle \in \text{Bisections}(A\cup B) \) using is_bisec
with A1, A2, A3 show \( thesis \) using a_is_fun, union_finpow, prod_bisect
qed

A generalization of prod_disjoint.

lemma (in semigr1) prod_list_of_lists:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( n \in nat \)

shows \( \forall M \in succ(n) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(n)\}) = \) \( (\prod (\bigcup i \in succ(n).\ M(i),a)) \)proof
note A2
moreover
have \( \forall M \in succ(0) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(0)\}) = (\prod (\bigcup i \in succ(0).\ M(i),a)) \) using a_is_fun, func1_1_L1, Partition_def, apply_funtype, setprod_type, list_len1_singleton, prod_of_1elem
moreover
have \( \forall k \in nat.\ \) \( (\forall M \in succ(k) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(k)\}) = \) \( (\prod (\bigcup i \in succ(k).\ M(i),a))) \longrightarrow \) \( (\forall M \in succ(succ(k)) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(succ(k))\}) = \) \( (\prod (\bigcup i \in succ(succ(k)).\ M(i),a))) \)proof
{
fix \( k \)
assume \( k \in nat \)
assume A3: \( \forall M \in succ(k) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(k)\}) = \) \( (\prod (\bigcup i \in succ(k).\ M(i),a)) \)
have \( (\forall N \in succ(succ(k)) \rightarrow \text{FinPow}(X).\ \) \( N \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (N(i),a)\rangle .\ i \in succ(succ(k))\}) = \) \( (\prod (\bigcup i \in succ(succ(k)).\ N(i),a))) \)proof
{
fix \( N \)
assume A4: \( N : succ(succ(k)) \rightarrow \text{FinPow}(X) \)
assume A5: \( N \text{ is partition } \)
with A4 have I: \( \forall i \in succ(succ(k)).\ N(i) \neq 0 \) using func1_1_L1, Partition_def
let \( b = \{\langle i,\prod (N(i),a)\rangle .\ i \in succ(succ(k))\} \)
let \( c = \{\langle i,\prod (N(i),a)\rangle .\ i \in succ(k)\} \)
have II: \( \forall i \in succ(succ(k)).\ \prod (N(i),a) \in G \)proof
fix \( i \)
assume \( i \in succ(succ(k)) \)
with A4, I have \( N(i) \in \text{FinPow}(X) \) and \( N(i) \neq 0 \) using apply_funtype
then show \( \prod (N(i),a) \in G \) using setprod_type
qed
hence \( \forall i \in succ(k).\ \prod (N(i),a) \in G \)
then have \( c : succ(k) \rightarrow G \) by (rule ZF_fun_from_total )
have \( b = \{\langle i,\prod (N(i),a)\rangle .\ i \in succ(succ(k))\} \)
with II have \( b = \text{Append}(c,\prod (N(succ(k)),a)) \) by (rule set_list_append )
with II, \( k \in nat \), \( c : succ(k) \rightarrow G \) have \( (\prod b) = (\prod c)\cdot (\prod (N(succ(k)),a)) \) using prod_append
also
have \( \ldots = (\prod (\bigcup i \in succ(k).\ N(i),a))\cdot (\prod (N(succ(k)),a)) \)proof
let \( M = \text{restrict}(N,succ(k)) \)
have \( succ(k) \subseteq succ(succ(k)) \)
with \( N : succ(succ(k)) \rightarrow \text{FinPow}(X) \) have \( M : succ(k) \rightarrow \text{FinPow}(X) \) and III: \( \forall i \in succ(k).\ M(i) = N(i) \) using restrict_type2, restrict, apply_funtype
with A5, \( M : succ(k) \rightarrow \text{FinPow}(X) \) have \( M \text{ is partition } \) using func1_1_L1, Partition_def
with A3, \( M : succ(k) \rightarrow \text{FinPow}(X) \) have \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(k)\}) = \) \( (\prod (\bigcup i \in succ(k).\ M(i),a)) \)
with III show \( thesis \)
qed
also
have \( \ldots = (\prod (\bigcup i \in succ(succ(k)).\ N(i),a)) \)proof
let \( A = \bigcup i \in succ(k).\ N(i) \)
let \( B = N(succ(k)) \)
from A4, \( k \in nat \) have \( succ(k) \in nat \) and \( \forall i \in succ(k).\ N(i) \in \text{FinPow}(X) \) using apply_funtype
then have \( A \in \text{FinPow}(X) \) by (rule union_fin_list_fin )
moreover
from I have \( A \neq 0 \)
moreover
from A4, I have \( N(succ(k)) \in \text{FinPow}(X) \) and \( N(succ(k)) \neq 0 \) using apply_funtype
moreover
from \( succ(k) \in nat \), A4, A5 have \( A \cap B = 0 \) by (rule list_partition )
moreover
note A1
ultimately have \( \prod (A\cup B,a) = (\prod (A,a))\cdot (\prod (B,a)) \) using prod_disjoint
moreover
have \( A \cup B = (\bigcup i \in succ(succ(k)).\ N(i)) \)
ultimately show \( thesis \)
qed
finally have \( (\prod \{\langle i,\prod (N(i),a)\rangle .\ i \in succ(succ(k))\}) = \) \( (\prod (\bigcup i \in succ(succ(k)).\ N(i),a)) \)
}
thus \( thesis \)
qed
}
thus \( thesis \)
qed
ultimately show \( thesis \) by (rule ind_on_nat )
qed

A more convenient reformulation of prod_list_of_lists.

theorem (in semigr1) prod_list_of_sets:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( n \in nat \), \( n \neq 0 \) and A3: \( M : n \rightarrow \text{FinPow}(X) \), \( M \text{ is partition } \)

shows \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in n\}) = (\prod (\bigcup i \in n.\ M(i),a)) \)proof
from A2 obtain \( k \) where \( k \in nat \) and \( n = succ(k) \) using Nat_ZF_1_L3
with A1, A3 show \( thesis \) using prod_list_of_lists
qed

The definition of the product \( \prod (A,a) \equiv \text{SetFold}(f,a,A,r) \) of a some (finite) set of semigroup elements requires that \(r\) is a linear order on the set of indices \(A\). This is necessary so that we know in which order we are multiplying the elements. The product over \(A\) is defined so that we have \(\prod_A a = \prod a \circ \sigma(A)\) where \(\sigma : |A| \rightarrow A\) is the enumeration of \(A\) (the only order isomorphism between the number of elements in \(A\) and \(A\)), see lemma setproddef. However, if the operation is commutative, the order is irrelevant. The next theorem formalizes that fact stating that we can replace the enumeration \(\sigma (A)\) by any bijection between \(|A|\) and \(A\). In a way this is a generalization of setproddef. The proof is based on application of prod_list_of_sets to the finite collection of singletons that comprise \(A\).

theorem (in semigr1) prod_order_irr:

assumes A1: \( f \text{ is commutative on } G \) and A2: \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and A3: \( b \in \text{bij}(|A|,A) \)

shows \( (\prod (a\circ b)) = \prod (A,a) \)proof
let \( n = |A| \)
let \( M = \{\langle k, \{b(k)\}\rangle .\ k \in n\} \)
have \( (\prod (a\circ b)) = (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in n\}) \)proof
have \( \forall i \in n.\ \prod (M(i),a) = (a\circ b)(i) \)proof
fix \( i \)
assume \( i \in n \)
with A2, A3, \( i \in n \) have \( b(i) \in X \) using bij_def, inj_def, apply_funtype, FinPow_def
then have \( \prod (\{b(i)\},a) = a(b(i)) \) using gen_prod_singleton
with A3, \( i \in n \) have \( \prod (\{b(i)\},a) = (a\circ b)(i) \) using bij_def, inj_def, comp_fun_apply
with \( i \in n \), A3 show \( \prod (M(i),a) = (a\circ b)(i) \) using bij_def, inj_partition
qed
hence \( \{\langle i,\prod (M(i),a)\rangle .\ i \in n\} = \{\langle i,(a\circ b)(i)\rangle .\ i \in n\} \)
moreover
have \( \{\langle i,(a\circ b)(i)\rangle .\ i \in n\} = a\circ b \)proof
from A3 have \( b : n \rightarrow A \) using bij_def, inj_def
moreover
from A2 have \( A \subseteq X \) using FinPow_def
ultimately have \( b : n \rightarrow X \) by (rule func1_1_L1B )
then have \( a\circ b: n \rightarrow G \) using a_is_fun, comp_fun
then show \( \{\langle i,(a\circ b)(i)\rangle .\ i \in n\} = a\circ b \) using fun_is_set_of_pairs
qed
ultimately show \( thesis \)
qed
also
have \( \ldots = (\prod (\bigcup i \in n.\ M(i),a)) \)proof
note A1
moreover
from A2 have \( n \in nat \) and \( n \neq 0 \) using card_fin_is_nat, card_non_empty_non_zero
moreover
have \( M : n \rightarrow \text{FinPow}(X) \) and \( M \text{ is partition } \)proof
from A2, A3 have \( \forall k \in n.\ \{b(k)\} \in \text{FinPow}(X) \) using bij_def, inj_def, apply_funtype, FinPow_def, singleton_in_finpow
then show \( M : n \rightarrow \text{FinPow}(X) \) using ZF_fun_from_total
from A3 show \( M \text{ is partition } \) using bij_def, inj_partition
qed
ultimately show \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in n\}) = (\prod (\bigcup i \in n.\ M(i),a)) \) by (rule prod_list_of_sets )
qed
also
from A3 have \( (\prod (\bigcup i \in n.\ M(i),a)) = \prod (A,a) \) using bij_def, inj_partition, surj_singleton_image
finally show \( thesis \)
qed

Another way of expressing the fact that the product dos not depend on the order.

corollary (in semigr1) prod_bij_same:

assumes \( f \text{ is commutative on } G \) and \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and \( b \in \text{bij}(|A|,A) \), \( c \in \text{bij}(|A|,A) \)

shows \( (\prod (a\circ b)) = (\prod (a\circ c)) \) using assms, prod_order_irr
end
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 semigr0) semigr_binop: shows \( f : G\times G \rightarrow G \)
lemma append_1elem:

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

shows \( \text{Concat}(a,b) = \text{Append}(a,b(0)) \)
lemma concat_init_last_elem:

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

shows \( \text{Append}( \text{Concat}(a, \text{Init}(b)),b(k)) = \text{Concat}(a,b) \)
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 empty_in_every_succ:

assumes \( n \in nat \)

shows \( 0 \in succ(n) \)
Definition of Fold1: \( \text{Fold1}(f,a) \equiv \text{Fold}(f,a(0), \text{Tail}(a)) \)
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 \)
corollary head_of_append:

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

shows \( \text{Append}(a,x)(0) = a(0) \)
theorem tail_append_commute:

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

shows \( \text{Append}( \text{Tail}(a),x) = \text{Tail}( \text{Append}(a,x)) \)
theorem fold_append:

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

shows \( \text{FoldSeq}(f,x, \text{Append}(a,y))(n) = \text{Fold}(f,x,a) \) and \( \text{Fold}(f,x, \text{Append}(a,y)) = f\langle \text{Fold}(f,x,a), y\rangle \)
lemma (in semigr0) append_1elem_nice:

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

shows \( a \sqcup b = a \hookleftarrow b(0) \)
lemma (in semigr0) prod_append:

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

shows \( (\prod a\hookleftarrow x) = (\prod a) \cdot x \)
lemma (in semigr0) prod_of_1elem:

assumes \( a: 1 \rightarrow G \)

shows \( (\prod a) = a(0) \)
theorem init_props:

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

shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \)
lemma (in semigr0) concat_init_last:

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

shows \( (a \sqcup \text{Init}(b)) \hookleftarrow b(k) = a \sqcup b \)
lemma (in semigr0) prod_type:

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

shows \( (\prod a) \in G \)
lemma (in semigr0) semigr_assoc:

assumes \( x \in G \), \( y \in G \), \( z \in G \)

shows \( x\cdot y\cdot z = x\cdot (y\cdot z) \)
theorem concat_props:

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

shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in Nat \text{Interval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \)
lemma succ_plus:

assumes \( n \in nat \), \( k \in nat \)

shows \( succ(n + j) \in nat \), \( succ(n) + succ(j) = succ(succ(n + j)) \)
theorem ind_on_nat:

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

shows \( P(n) \)
lemma (in semigr0) semigr_closed:

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

shows \( a\cdot b \in G \)
Definition of SetFold: \( \text{SetFold}(f,a,\Lambda ,r) = \text{Fold1}(f,a\circ \text{Enumeration}(\Lambda ,r)) \)
lemma card_non_empty_succ:

assumes \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)

shows \( \exists n \in nat.\ |A| = succ(n) \)
lemma (in semigr1) enums_valid_in_semigr1: shows \( enums(X,r) \)
lemma (in enums) enum_props:

assumes \( A \in \text{FinPow}(X) \)

shows \( \sigma (A) \in ord\_iso(|A|,Le, A,r) \), \( \sigma (A) \in \text{bij}(|A|,A) \), \( \sigma (A) : |A| \rightarrow A \)
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
lemma comp_fun_subset:

assumes \( g:A\rightarrow B \) and \( f:C\rightarrow D \) and \( B \subseteq C \)

shows \( f\circ g : A \rightarrow D \)
lemma (in semigr1) setproddef: shows \( \prod (\Lambda ,a) = \prod (a\circ \sigma (\Lambda )) \)
lemma (in enums) enum_append:

assumes \( A \in \text{FinPow}(X) \) and \( b \in X-A \) and \( \forall a\in A.\ a\leq b \)

shows \( \sigma (A \cup \{b\}) = \sigma (A)\hookleftarrow b \)
lemma (in enums) enum_singleton:

assumes \( x\in X \)

shows \( \sigma (\{x\}): 1 \rightarrow X \) and \( \sigma (\{x\})(0) = x \)
lemma (in semigr1) semigr1_enum_append:

assumes \( \Lambda \in \text{FinPow}(X) \) and \( n \in X - \Lambda \) and \( \forall k\in \Lambda .\ \langle k,n\rangle \in r \)

shows \( \sigma (\Lambda \cup \{n\}) = \sigma (\Lambda )\hookleftarrow n \)
lemma card_fin_is_nat:

assumes \( A \in \text{FinPow}(X) \)

shows \( |A| \in nat \) and \( A \approx |A| \)
lemma (in enums) enum_fun:

assumes \( A \in \text{FinPow}(X) \)

shows \( \sigma (A) : |A| \rightarrow X \)
lemma list_compose_append:

assumes \( n \in nat \) and \( a : n \rightarrow X \) and \( x \in X \) and \( c : X \rightarrow Y \)

shows \( c\circ \text{Append}(a,x) : succ(n) \rightarrow Y \), \( c\circ \text{Append}(a,x) = \text{Append}(c\circ a, c(x)) \)
lemma (in semigr1) setprod_type:

assumes \( \Lambda \in \text{FinPow}(X) \) and \( \Lambda \neq 0 \)

shows \( \exists n \in nat .\ |\Lambda | = succ(n) \wedge a\circ \sigma (\Lambda ) : succ(n) \rightarrow G \) and \( \prod (\Lambda ,a) \in G \)
corollary fin_rem_point_fin:

assumes \( A \in \text{FinPow}(X) \)

shows \( A - \{a\} \in \text{FinPow}(X) \)
lemma (in semigr1) gen_prod_append:

assumes \( \Lambda \in \text{FinPow}(X) \) and \( \Lambda \neq 0 \) and \( n \in X - \Lambda \) and \( \forall k\in \Lambda .\ \langle k,n\rangle \in r \)

shows \( \prod (\Lambda \cup \{n\}, a) = (\prod (\Lambda ,a)) \cdot a(n) \)
lemma rem_add_eq:

assumes \( a\in A \)

shows \( (A-\{a\}) \cup \{a\} = A \)
Definition of IsCommutative: \( f \text{ is commutative on } G \equiv \forall x\in G.\ \forall y\in G.\ f\langle x,y\rangle = f\langle y,x\rangle \)
lemma (in semigr0) shorter_seq:

assumes \( k \in nat \) and \( a \in succ(succ(k)) \rightarrow G \)

shows \( (\prod a) = (\prod \text{Init}(a)) \cdot a(succ(k)) \)
lemma (in semigr0) prod_distr_ind_step:

assumes \( k \in nat \) and \( a : succ(succ(k)) \rightarrow G \) and \( b : succ(succ(k)) \rightarrow G \) and \( c : succ(succ(k)) \rightarrow G \) and \( \forall j\in succ(succ(k)).\ c(j) = a(j) \cdot b(j) \)

shows \( \text{Init}(a) : succ(k) \rightarrow G \), \( \text{Init}(b) : succ(k) \rightarrow G \), \( \text{Init}(c) : succ(k) \rightarrow G \), \( \forall j\in succ(k).\ \text{Init}(c)(j) = \text{Init}(a)(j) \cdot \text{Init}(b)(j) \)
lemma (in semigr0) rearr4elems:

assumes \( f \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\cdot b\cdot (c\cdot d) = a\cdot c\cdot (b\cdot d) \)
theorem (in semigr0) prod_comm_distr:

assumes \( f \text{ is commutative on } G \) and \( n\in nat \)

shows \( \forall a b c.\ \) \( (a : succ(n)\rightarrow G \wedge b : succ(n)\rightarrow G \wedge c : succ(n)\rightarrow G \wedge \) \( (\forall j\in succ(n).\ c(j) = a(j) \cdot b(j))) \longrightarrow \) \( (\prod c) = (\prod a) \cdot (\prod b) \)
lemma bisec_empty: shows \( \text{Bisections}(0) = 0 \)
lemma singleton_in_finpow:

assumes \( x \in X \)

shows \( \{x\} \in \text{FinPow}(X) \)
lemma union_finpow:

assumes \( A \in \text{FinPow}(X) \) and \( B \in \text{FinPow}(X) \)

shows \( A \cup B \in \text{FinPow}(X) \)
lemma bisect_fin:

assumes \( A \in \text{FinPow}(X) \) and \( Q \in \text{Bisections}(A) \)

shows \( \text{fst}(Q) \in \text{FinPow}(X) \) and \( \text{snd}(Q) \in \text{FinPow}(X) \)
lemma bisec_is_pair:

assumes \( Q \in \text{Bisections}(X) \)

shows \( Q = \langle \text{fst}(Q), \text{snd}(Q)\rangle \)
Definition of Bisections: \( \text{Bisections}(X) = \{p \in Pow(X)\times Pow(X).\ \) \( \text{fst}(p)\neq 0 \wedge \text{snd}(p)\neq 0 \wedge \text{fst}(p)\cap \text{snd}(p) = 0 \wedge \text{fst}(p)\cup \text{snd}(p) = X\} \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma total_is_refl:

assumes \( r \text{ is total on } X \)

shows \( \text{refl}(X,r) \)
lemma refl_add_point:

assumes \( \text{refl}(X,r) \) and \( A \subseteq B \cup \{x\} \) and \( B \subseteq X \) and \( x \in X \) and \( \forall y\in B.\ \langle y,x\rangle \in r \)

shows \( \forall a\in A.\ \langle a,x\rangle \in r \)
lemma bisec_add_point:

assumes \( x \notin X \) and \( \langle A,B\rangle \in \text{Bisections}(X \cup \{x\}) \)

shows \( (A = \{x\} \vee B = \{x\}) \vee (\langle A - \{x\}, B - \{x\}\rangle \in \text{Bisections}(X)) \)
lemma set_point_bisec:

assumes \( x \notin X \) and \( \langle A, \{x\}\rangle \in \text{Bisections}(X \cup \{x\}) \)

shows \( A = X \) and \( X \neq 0 \)
lemma (in semigr1) gen_prod_singleton:

assumes \( x \in X \)

shows \( \prod (\{x\},a) = a(x) \)
lemma point_set_bisec:

assumes \( x \notin X \) and \( \langle \{x\}, A\rangle \in \text{Bisections}(X \cup \{x\}) \)

shows \( A = X \) and \( X \neq 0 \)
lemma bisec_add_point_case3:

assumes \( \langle A,B\rangle \in \text{Bisections}(X \cup \{x\}) \) and \( \langle A - \{x\}, B - \{x\}\rangle \in \text{Bisections}(X) \)

shows \( (\langle A, B - \{x\}\rangle \in \text{Bisections}(X) \wedge x \in B) \vee \) \( (\langle A - \{x\}, B\rangle \in \text{Bisections}(X) \wedge x \in A) \)
lemma bisec_props:

assumes \( \langle A,B\rangle \in \text{Bisections}(X) \)

shows \( A\neq 0 \), \( B\neq 0 \), \( A \subseteq X \), \( B \subseteq X \), \( A \cap B = 0 \), \( A \cup B = X \), \( X \neq 0 \)
lemma (in semigr1) gen_product_rem_point:

assumes \( A \in \text{FinPow}(X) \) and \( n \in A \) and \( A - \{n\} \neq 0 \) and \( \forall k\in A.\ \langle k, n\rangle \in r \)

shows \( (\prod (A - \{n\},a)) \cdot a(n) = \prod (A, a) \)
lemma (in semigr0) rearr3elems:

assumes \( f \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot b\cdot c = a\cdot c\cdot b \)
lemma fin_ind_add_max:

assumes \( \text{IsLinOrder}(X,r) \) and \( P(0) \) and \( \forall A \in \text{FinPow}(X).\ \) \( ( \forall x \in X-A.\ P(A) \wedge (\forall a\in A.\ \langle a,x\rangle \in r ) \longrightarrow P(A \cup \{x\})) \) and \( B \in \text{FinPow}(X) \)

shows \( P(B) \)
lemma is_bisec:

assumes \( A\neq 0 \), \( B\neq 0 \), \( A \cap B = 0 \)

shows \( \langle A,B\rangle \in \text{Bisections}(A\cup B) \)
lemma (in semigr1) prod_bisect:

assumes \( f \text{ is commutative on } G \) and \( \Lambda \in \text{FinPow}(X) \)

shows \( \forall P \in \text{Bisections}(\Lambda ).\ \prod (\Lambda ,a) = (\prod (\text{fst}(P),a))\cdot (\prod (\text{snd}(P),a)) \)
lemma func1_1_L1:

assumes \( f:A\rightarrow C \)

shows \( domain(f) = A \)
Definition of Partition: \( P \text{ is partition } \equiv \forall x \in domain(P).\ \) \( P(x) \neq 0 \wedge (\forall y \in domain(P).\ x\neq y \longrightarrow P(x) \cap P(y) = 0) \)
lemma list_len1_singleton:

assumes \( x\in X \)

shows \( \{\langle 0,x\rangle \} : 1 \rightarrow X \) and \( \{\langle 0,x\rangle \} \in \text{NELists}(X) \)
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 \)
lemma set_list_append:

assumes \( \forall i \in succ(k).\ b(i) \in X \) and \( a = \{\langle i,b(i)\rangle .\ i \in succ(k)\} \)

shows \( a: succ(k) \rightarrow X \), \( \{\langle i,b(i)\rangle .\ i \in k\}: k \rightarrow X \), \( a = \text{Append}(\{\langle i,b(i)\rangle .\ i \in k\},b(k)) \)
lemma union_fin_list_fin:

assumes \( n \in nat \) and \( \forall k \in n.\ N(k) \in \text{FinPow}(X) \)

shows \( \{N(k).\ k \in n\} \in \text{FinPow}( \text{FinPow}(X)) \) and \( (\bigcup k \in n.\ N(k)) \in \text{FinPow}(X) \)
lemma list_partition:

assumes \( n \in nat \) and \( a : succ(n) \rightarrow X \), \( a \text{ is partition } \)

shows \( (\bigcup i\in n.\ a(i)) \cap a(n) = 0 \)
theorem (in semigr1) prod_disjoint:

assumes \( f \text{ is commutative on } G \) and \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and \( B \in \text{FinPow}(X) \), \( B \neq 0 \) and \( A \cap B = 0 \)

shows \( \prod (A\cup B,a) = (\prod (A,a))\cdot (\prod (B,a)) \)
lemma Nat_ZF_1_L3:

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

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

assumes \( f \text{ is commutative on } G \) and \( n \in nat \)

shows \( \forall M \in succ(n) \rightarrow \text{FinPow}(X).\ \) \( M \text{ is partition } \longrightarrow \) \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in succ(n)\}) = \) \( (\prod (\bigcup i \in succ(n).\ M(i),a)) \)
lemma inj_partition:

assumes \( b \in \text{inj}(X,Y) \)

shows \( \forall x \in X.\ \{\langle x, \{b(x)\}\rangle .\ x \in X\}(x) = \{b(x)\} \) and \( \{\langle x, \{b(x)\}\rangle .\ x \in X\} \text{ is partition } \)
lemma func1_1_L1B:

assumes \( f:X\rightarrow Y \) and \( Y\subseteq Z \)

shows \( f:X\rightarrow Z \)
theorem fun_is_set_of_pairs:

assumes \( f:X\rightarrow Y \)

shows \( f = \{\langle x, f(x)\rangle .\ x \in X\} \)
lemma card_non_empty_non_zero:

assumes \( A \in \text{FinPow}(X) \) and \( A \neq 0 \)

shows \( |A| \neq 0 \)
theorem (in semigr1) prod_list_of_sets:

assumes \( f \text{ is commutative on } G \) and \( n \in nat \), \( n \neq 0 \) and \( M : n \rightarrow \text{FinPow}(X) \), \( M \text{ is partition } \)

shows \( (\prod \{\langle i,\prod (M(i),a)\rangle .\ i \in n\}) = (\prod (\bigcup i \in n.\ M(i),a)) \)
lemma surj_singleton_image:

assumes \( f \in \text{surj}(X,Y) \)

shows \( (\bigcup x\in X.\ \{f(x)\}) = Y \)
theorem (in semigr1) prod_order_irr:

assumes \( f \text{ is commutative on } G \) and \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and \( b \in \text{bij}(|A|,A) \)

shows \( (\prod (a\circ b)) = \prod (A,a) \)