(* 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_ZF begin text{*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 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