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: