# Theory CommutativeSemigroup_ZF

theory CommutativeSemigroup_ZF
imports Semigroup_ZF
(*     This file is a part of IsarMathLib -     a library of formalized mathematics for Isabelle/Isar.    Copyright (C) 2007-2009  Slawomir Kolodynski    This progr\rightarowam is free software; Redistribution and use in source and binary forms,     with or without modification, are permitted provided that the following conditions are met:   1. Redistributions of source code must retain the above copyright notice,    this list of conditions and the following disclaimer.   2. Redistributions in binary form must reproduce the above copyright notice,    this list of conditions and the following disclaimer in the documentation and/or    other materials provided with the distribution.   3. The name of the author may not be used to endorse or promote products    derived from this software without specific prior written permission.THIS SOFTWARE IS PROVIDED BY THE AUTHOR AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.*)header{*\isaheader{CommutativeSemigroup\_ZF.thy}*}theory CommutativeSemigroup_ZF imports Semigroup_ZFbegintext{*In the @{text "Semigroup"} theory we introduced a notion   of @{text "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.   *}section{*Sum of a function over a set*}text{* The $r$ parameter in the definition of @{text "SetFold(f,a,Λ,r)"}  (from @{text "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 @{text "Fold1(f,c)"}   is defined in @{text "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 O b). b ∈ bij( |Λ|, Λ)}"} is a singleton  and we can extract its only value by taking its union.*}definition  "CommSetFold(f,a,Λ) = \<Union>{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 @{text "commsemigr"} locale.*}lemma (in commsemigr) CommSetFolddef:   shows "(\<ssum>(A,a)) = (\<Union>{∑(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   @{text "prod_order_irr"} in the @{text "Semigroup"} theory,  except that the @{text "semigr1"} locale assumes  that the domain of the function we sum up is linearly  ordered, while in @{text "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 "(\<Union>{∑(a O b). b ∈ bij(|A|, A)}) = (∑ (a O b))"    by (rule singleton_comprehension);  then show ?thesis using CommSetFolddef by simp;qedtext{*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