IsarMathLib

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

theory CommutativeSemigroup_ZF imports Semigroup_ZF
begin

In the Semigroup theory we introduced a notion of \( \text{SetFold}(f,a,\Lambda ,r) \) that represents the sum of values of some function \(a\) valued in a semigroup where the arguments of that function vary over some set \(\Lambda\). Using the additive notation something like this would be expressed as \(\sum_{x\in \Lambda} f(x)\) in informal mathematics. This theory considers an alternative to that notion that is more specific to commutative semigroups.

Sum of a function over a set

The \(r\) parameter in the definition of \( \text{SetFold}(f,a,\Lambda ,r) \) (from Semigroup_ZF) represents a linear order relation on \(\Lambda\) that is needed to indicate in what order we are summing the values \(f(x)\). If the semigroup operation is commutative the order does not matter and the relation \(r\) is not needed. In this section we define a notion of summing up values of some function \(a : X \rightarrow G\) over a finite set of indices \(\Gamma \subseteq X\), without using any order relation on \(X\).

We define the sum of values of a function \(a: X\rightarrow G\) over a set \(\Lambda\) as the only element of the set of sums of lists that are bijections between the number of values in \(\Lambda\) (which is a natural number \(n = \{0,1, .. , n-1\}\) if \(\Lambda\) is finite) and \(\Lambda\). The notion of \( \text{Fold1}(f,c) \) is defined in Semigroup_ZF as the fold (sum) of the list \(c\) starting from the first element of that list. The intention is to use the fact that since the result of summing up a list does not depend on the order, the set \( \{ \text{Fold1}(f,a\circ b).\ b \in \text{bij}( |\Lambda |, \Lambda )\} \) is a singleton and we can extract its only value by taking its union.

definition

\( \text{CommSetFold}(f,a,\Lambda ) = \bigcup \{ \text{Fold1}(f,a\circ b).\ b \in \text{bij}(|\Lambda |, \Lambda )\} \)

the next locale sets up notation for writing about summation in commutative semigroups. We define two kinds of sums. One is the sum of elements of a list (which are just functions defined on a natural number) and the second one represents a more general notion the sum of values of a semigroup valued function over some set of arguments. Since those two types of sums are different notions they are represented by different symbols. However in the presentations they are both intended to be printed as \(\sum \).

locale commsemigr

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

assumes csgcomm: \( f \text{ is commutative on } G \)

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

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

defines \( \sum k \equiv \text{Fold1}(f,k) \)

defines \( \sum (A,h) \equiv \text{CommSetFold}(f,h,A) \)

Definition of a sum of function over a set in notation defined in the commsemigr locale.

lemma (in commsemigr) CommSetFolddef:

shows \( (\sum (A,a)) = (\bigcup \{\sum (a\circ b).\ b \in \text{bij}(|A|, A)\}) \) using CommSetFold_def

The next lemma states that the result of a sum does not depend on the order we calculate it. This is similar to lemma prod_order_irr in the Semigroup theory, except that the semigr1 locale assumes that the domain of the function we sum up is linearly ordered, while in commsemigr we don't have this assumption.

lemma (in commsemigr) sum_over_set_bij:

assumes A1: \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and A2: \( b \in \text{bij}(|A|,A) \)

shows \( (\sum (A,a)) = (\sum (a\circ b)) \)proof
have \( \forall c \in \text{bij}(|A|,A).\ \forall d \in \text{bij}(|A|,A).\ (\sum (a\circ c)) = (\sum (a\circ d)) \)proof
{
fix \( c \)
assume \( c \in \text{bij}(|A|,A) \)
fix \( d \)
assume \( d \in \text{bij}(|A|,A) \)
let \( r = \text{InducedRelation}(converse(c), Le) \)
have \( semigr1(G,f,A,r,\text{restrict}(a, A)) \)proof
have \( semigr0(G,f) \) using csgassoc, semigr0_def
moreover
from A1, \( c \in \text{bij}(|A|,A) \) have \( \text{IsLinOrder}(A,r) \) using bij_converse_bij, card_fin_is_nat, natord_lin_on_each_nat, ind_rel_pres_lin
moreover
from A1 have \( \text{restrict}(a, A) : A \rightarrow G \) using FinPow_def, csgaisfun, restrict_fun
ultimately show \( thesis \) using semigr1_axioms.intro, semigr1_def
qed
moreover
have \( f \text{ is commutative on } G \) using csgcomm
moreover
from A1 have \( A \in \text{FinPow}(A) \), \( A \neq 0 \) using FinPow_def
moreover
note \( c \in \text{bij}(|A|,A) \), \( d \in \text{bij}(|A|,A) \)
ultimately have \( \text{Fold1}(f,\text{restrict}(a,A)\circ c) = \text{Fold1}(f,\text{restrict}(a,A)\circ d) \) by (rule prod_bij_same )
hence \( (\sum (\text{restrict}(a,A)\circ c)) = (\sum (\text{restrict}(a,A)\circ d)) \)
moreover
from A1, \( c \in \text{bij}(|A|,A) \), \( d \in \text{bij}(|A|,A) \) have \( \text{restrict}(a,A)\circ c = a\circ c \) and \( \text{restrict}(a,A)\circ d = a\circ d \) using bij_def, surj_def, csgaisfun, FinPow_def, comp_restrict
ultimately have \( (\sum (a\circ c)) = (\sum (a\circ d)) \)
}
thus \( thesis \)
qed
with A2 have \( (\bigcup \{\sum (a\circ b).\ b \in \text{bij}(|A|, A)\}) = (\sum (a\circ b)) \) by (rule singleton_comprehension )
then show \( thesis \) using CommSetFolddef
qed

The result of a sum is in the semigroup. Also, as the second assertion we show that every semigroup valued function generates a homomorphism between the finite subsets of a semigroup and the semigroup. Adding an element to a set coresponds to adding a value.

lemma (in commsemigr) sum_over_set_add_point:

assumes A1: \( A \in \text{FinPow}(X) \), \( A \neq 0 \)

shows \( \sum (A,a) \in G \) and \( \forall x \in X-A.\ \sum (A \cup \{x\},a) = (\sum (A,a)) + a(x) \)proof
from A1 obtain \( b \) where \( b \in \text{bij}(|A|,A) \) using fin_bij_card
with A1 have \( \sum (A,a) = (\sum (a\circ b)) \) using sum_over_set_bij
from A1 have \( |A| \in nat \) using card_fin_is_nat
have \( semigr0(G,f) \) using csgassoc, semigr0_def
moreover
from A1 obtain \( n \) where \( n \in nat \) and \( |A| = succ(n) \) using card_non_empty_succ
with A1, \( b \in \text{bij}(|A|,A) \) have \( n \in nat \) and \( a\circ b : succ(n) \rightarrow G \) using bij_def, inj_def, FinPow_def, comp_fun_subset, csgaisfun
ultimately have \( \text{Fold1}(f,a\circ b) \in G \) by (rule prod_type )
with \( \sum (A,a) = (\sum (a\circ b)) \) show \( \sum (A,a) \in G \)
{
fix \( x \)
assume \( x \in X-A \)
with A1 have \( (A \cup \{x\}) \in \text{FinPow}(X) \) and \( A \cup \{x\} \neq 0 \) using singleton_in_finpow, union_finpow
moreover
have \( \text{Append}(b,x) \in \text{bij}(|A \cup \{x\}|, A \cup \{x\}) \)proof
note \( |A| \in nat \), \( b \in \text{bij}(|A|,A) \)
moreover
from \( x \in X-A \) have \( x \notin A \)
ultimately have \( \text{Append}(b,x) \in \text{bij}(succ(|A|), A \cup \{x\}) \) by (rule bij_append_point )
with A1, \( x \in X-A \) show \( thesis \) using card_fin_add_one
qed
ultimately have \( (\sum (A \cup \{x\},a)) = (\sum (a\circ \text{Append}(b,x))) \) using sum_over_set_bij
also
have \( \ldots = (\sum \text{Append}(a\circ b, a(x))) \)proof
note \( |A| \in nat \)
moreover
from A1, \( b \in \text{bij}(|A|, A) \) have \( b : |A| \rightarrow A \) and \( A \subseteq X \) using bij_def, inj_def using FinPow_def
then have \( b : |A| \rightarrow X \) by (rule func1_1_L1B )
moreover
from \( x \in X-A \) have \( x \in X \) and \( a : X \rightarrow G \) using csgaisfun
ultimately show \( thesis \) using list_compose_append
qed
also
have \( \ldots = (\sum (A,a)) + a(x) \)proof
note \( semigr0(G,f) \), \( n \in nat \), \( a\circ b : succ(n) \rightarrow G \)
moreover
from \( x \in X-A \) have \( a(x) \in G \) using csgaisfun, apply_funtype
ultimately have \( \text{Fold1}(f, \text{Append}(a\circ b, a(x))) = f\langle \text{Fold1}(f,a\circ b),a(x)\rangle \) by (rule prod_append )
with A1, \( b \in \text{bij}(|A|,A) \) show \( thesis \) using sum_over_set_bij
qed
finally have \( (\sum (A \cup \{x\},a)) = (\sum (A,a)) + a(x) \)
}
thus \( \forall x \in X-A.\ \sum (A \cup \{x\},a) = (\sum (A,a)) + a(x) \)
qed
end
Definition of CommSetFold: \( \text{CommSetFold}(f,a,\Lambda ) = \bigcup \{ \text{Fold1}(f,a\circ b).\ b \in \text{bij}(|\Lambda |, \Lambda )\} \)
lemma card_fin_is_nat:

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

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

assumes \( n \in nat \)

shows \( \text{IsLinOrder}(n,Le) \)
lemma ind_rel_pres_lin:

assumes \( f \in \text{bij}(A,B) \) and \( \text{IsLinOrder}(B,R) \)

shows \( \text{IsLinOrder}(A, \text{InducedRelation}(f,R)) \)
Definition of FinPow: \( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
corollary restrict_fun:

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

shows \( \text{restrict}(f,A) : A \rightarrow Y \)
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)) \)
lemma comp_restrict:

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

shows \( g\circ f = \text{restrict}(g,B)\circ f \)
lemma singleton_comprehension:

assumes \( y\in X \) and \( \forall x\in X.\ \forall y\in X.\ P(x) = P(y) \)

shows \( (\bigcup \{P(x).\ x\in X\}) = P(y) \)
lemma (in commsemigr) CommSetFolddef: shows \( (\sum (A,a)) = (\bigcup \{\sum (a\circ b).\ b \in \text{bij}(|A|, A)\}) \)
lemma fin_bij_card:

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

shows \( \exists b.\ b \in \text{bij}(|A|, A) \)
lemma (in commsemigr) sum_over_set_bij:

assumes \( A \in \text{FinPow}(X) \), \( A \neq 0 \) and \( b \in \text{bij}(|A|,A) \)

shows \( (\sum (A,a)) = (\sum (a\circ b)) \)
lemma card_non_empty_succ:

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

shows \( \exists n \in nat.\ |A| = succ(n) \)
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 semigr0) prod_type:

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

shows \( (\prod a) \in G \)
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 bij_append_point:

assumes \( n \in nat \) and \( b \in \text{bij}(n,X) \) and \( x \notin X \)

shows \( \text{Append}(b,x) \in \text{bij}(succ(n), X \cup \{x\}) \)
lemma card_fin_add_one:

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

shows \( |A \cup \{a\}| = succ( |A| ) \), \( |A \cup \{a\}| = |A| \cup \{|A|\} \)
lemma func1_1_L1B:

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

shows \( f:X\rightarrow Z \)
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 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 \)