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_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