section ‹Commutative Semigroups›
theory CommutativeSemigroup_ZF imports Semigroup_ZF
begin
text‹In the ‹Semigroup› theory we introduced a notion
of ‹SetFold(f,a,Λ,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.
›
subsection‹Sum of a function over a set›
text‹The $r$ parameter in the definition of ‹SetFold(f,a,Λ,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$.›
text‹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 ‹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
‹{Fold1(f,a O b). b ∈ bij( |Λ|, Λ)}› is a singleton
and we can extract its only value by taking its union.›
definition
"CommSetFold(f,a,Λ) = ⋃{Fold1(f,a O b). b ∈ bij(|Λ|, Λ)}"
text‹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 =
fixes G f
assumes csgassoc: "f {is associative on} G"
assumes csgcomm: "f {is commutative on} G"
fixes csgsum (infixl "\<ra>" 69)
defines csgsum_def[simp]: "x \<ra> y ≡ f`⟨x,y⟩"
fixes X a
assumes csgaisfun: "a : X → G"
fixes csglistsum ("∑ _" 70)
defines csglistsum_def[simp]: "∑k ≡ Fold1(f,k)"
fixes csgsetsum ("\<ssum>")
defines csgsetsum_def[simp]: "\<ssum>(A,h) ≡ CommSetFold(f,h,A)"
text‹Definition of a sum of function over a set in
notation defined in the ‹commsemigr› locale.›
lemma (in commsemigr) CommSetFolddef:
shows "(\<ssum>(A,a)) = (⋃{∑(a O b). b ∈ bij(|A|, A)})"
using CommSetFold_def by simp
text‹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 ∈ FinPow(X)" "A ≠ 0" and A2: "b ∈ bij(|A|,A)"
shows "(\<ssum>(A,a)) = (∑ (a O b))"
proof -
have
"∀c ∈ bij(|A|,A). ∀ d ∈ bij(|A|,A). (∑(a O c)) = (∑(a O d))"
proof -
{ fix c assume "c ∈ bij(|A|,A)"
fix d assume "d ∈ bij(|A|,A)"
let ?r = "InducedRelation(converse(c), Le)"
have "semigr1(G,f,A,?r,restrict(a, A))"
proof -
have "semigr0(G,f)" using csgassoc semigr0_def by simp
moreover from A1 ‹c ∈ bij(|A|,A)› have "IsLinOrder(A,?r)"
using bij_converse_bij card_fin_is_nat
natord_lin_on_each_nat ind_rel_pres_lin by simp
moreover from A1 have "restrict(a, A) : A → G"
using FinPow_def csgaisfun restrict_fun by simp
ultimately show ?thesis using semigr1_axioms.intro semigr1_def
by simp
qed
moreover have "f {is commutative on} G" using csgcomm
by simp
moreover from A1 have "A ∈ FinPow(A)" "A ≠ 0"
using FinPow_def by auto
moreover note ‹c ∈ bij(|A|,A)› ‹d ∈ bij(|A|,A)›
ultimately have
"Fold1(f,restrict(a,A) O c) = Fold1(f,restrict(a,A) O d)"
by (rule semigr1.prod_bij_same)
hence "(∑ (restrict(a,A) O c)) = (∑ (restrict(a,A) O d))"
by simp
moreover from A1 ‹c ∈ bij(|A|,A)› ‹d ∈ bij(|A|,A)›
have
"restrict(a,A) O c = a O c" and "restrict(a,A) O d = a O d"
using bij_def surj_def csgaisfun FinPow_def comp_restrict
by auto
ultimately have "(∑(a O c)) = (∑(a O d))" by simp
} thus ?thesis by blast
qed
with A2 have "(⋃{∑(a O b). b ∈ bij(|A|, A)}) = (∑ (a O b))"
by (rule singleton_comprehension)
then show ?thesis using CommSetFolddef by simp
qed
text‹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 ∈ FinPow(X)" "A ≠ 0"
shows "\<ssum>(A,a) ∈ G" and
"∀x ∈ X-A. \<ssum>(A ∪ {x},a) = (\<ssum>(A,a)) \<ra> a`(x)"
proof -
from A1 obtain b where "b ∈ bij(|A|,A)"
using fin_bij_card by auto
with A1 have "\<ssum>(A,a) = (∑ (a O b))"
using sum_over_set_bij by simp
from A1 have "|A| ∈ nat" using card_fin_is_nat by simp
have "semigr0(G,f)" using csgassoc semigr0_def by simp
moreover
from A1 obtain n where "n ∈ nat" and "|A| = succ(n)"
using card_non_empty_succ by auto
with A1 ‹b ∈ bij(|A|,A)› have
"n ∈ nat" and "a O b : succ(n) → G"
using bij_def inj_def FinPow_def comp_fun_subset csgaisfun
by auto
ultimately have "Fold1(f,a O b) ∈ G" by (rule semigr0.prod_type)
with ‹\<ssum>(A,a) = (∑ (a O b))› show "\<ssum>(A,a) ∈ G"
by simp
{ fix x assume "x ∈ X-A"
with A1 have "(A ∪ {x}) ∈ FinPow(X)" and "A ∪ {x} ≠ 0"
using singleton_in_finpow union_finpow by auto
moreover have "Append(b,x) ∈ bij(|A ∪ {x}|, A ∪ {x})"
proof -
note ‹|A| ∈ nat› ‹b ∈ bij(|A|,A)›
moreover from ‹x ∈ X-A› have "x ∉ A" by simp
ultimately have "Append(b,x) ∈ bij(succ(|A|), A ∪ {x})"
by (rule bij_append_point)
with A1 ‹x ∈ X-A› show ?thesis
using card_fin_add_one by auto
qed
ultimately have "(\<ssum>(A ∪ {x},a)) = (∑ (a O Append(b,x)))"
using sum_over_set_bij by simp
also have "… = (∑ Append(a O b, a`(x)))"
proof -
note ‹|A| ∈ nat›
moreover
from A1 ‹b ∈ bij(|A|, A)› have
"b : |A| → A" and "A ⊆ X"
using bij_def inj_def using FinPow_def by auto
then have "b : |A| → X" by (rule func1_1_L1B)
moreover from ‹x ∈ X-A› have "x ∈ X" and "a : X → G"
using csgaisfun by auto
ultimately show ?thesis using list_compose_append
by simp
qed
also have "… = (\<ssum>(A,a)) \<ra> a`(x)"
proof -
note ‹semigr0(G,f)› ‹n ∈ nat› ‹a O b : succ(n) → G›
moreover from ‹x ∈ X-A› have "a`(x) ∈ G"
using csgaisfun apply_funtype by simp
ultimately have
"Fold1(f,Append(a O b, a`(x))) = f`⟨Fold1(f,a O b),a`(x)⟩"
by (rule semigr0.prod_append)
with A1 ‹b ∈ bij(|A|,A)› show ?thesis
using sum_over_set_bij by simp
qed
finally have "(\<ssum>(A ∪ {x},a)) = (\<ssum>(A,a)) \<ra> a`(x)"
by simp
} thus "∀x ∈ X-A. \<ssum>(A ∪ {x},a) = (\<ssum>(A,a)) \<ra> a`(x)"
by simp
qed
end