(*

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