Theory Semigroup_ZF

theory Semigroup_ZF
imports Partitions_ZF Fold_ZF Enumeration_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{Semigroup\_ZF.thy}*}

theory Semigroup_ZF imports Partitions_ZF Fold_ZF Enumeration_ZF

begin

text{*It seems that the minimal setup needed to talk about a product of a 
  sequence is a set with a binary operation. 
  Such object is called "magma". However, interesting properties
  show up when the binary operation is associative and such alebraic structure
  is called a semigroup. 
  In this theory file we define and study sequences of partial 
  products of sequences of magma and semigroup elements.*}

section{*Products of sequences of semigroup elements*}

text{*Semigroup is a a magma in which the binary operation is associative.
  In this section we mostly study the products of sequences of elements 
  of semigroup. The goal is to establish the fact that taking the product of 
  a sequence is distributive with respect to concatenation of sequences, 
  i.e for two sequences $a,b$ of the semigroup elements we have 
  $\prod (a\sqcup b) = (\prod a)\cdot (\prod b)$, where "$a \sqcup b$" 
  is concatenation of $a$ and $b$ ($a$@{text "++"}$b$ in Haskell notation).
  Less formally, we want to show that we can discard parantheses in 
  expressions of the form 
  $(a_0\cdot a_1\cdot .. \cdot a_n)\cdot (b_0\cdot .. \cdot b_k)$.
  *}

text{*First we define a notion similar to @{text "Fold"}, except that
  that the initial element of the fold is given by the first element
  of sequence. By analogy with Haskell fold we call that @{text "Fold1"}
  *}

definition
  "Fold1(f,a) ≡ Fold(f,a`(0),Tail(a))"

text{*The definition of the @{text "semigr0"} context below introduces notation
  for writing about finite sequences and semigroup products. 
  In the context we fix the carrier and
  denote it $G$. The binary operation on $G$ is called $f$. 
  All theorems proven in the context @{text "semigr0"} 
  will implicitly assume that $f$ is an associative operation on $G$.
  We will use multiplicative notation for the semigroup operation.
  The product of a sequence $a$ is denoted $\prod a$.
  We will write
  $a\hookleftarrow x$ for the result of appending an element $x$ to
  the finite sequence (list) $a$. This is a bit nonstandard, 
  but I don't have a better idea for the "append" notation. Finally,
  $a\sqcup b$ will denote the concatenation of the lists $a$ and $b$.*}

locale semigr0 =
  
  fixes G f

  assumes assoc_assum: "f {is associative on} G"

  fixes prod (infixl "·" 72)
  defines prod_def [simp]: "x · y ≡ f`⟨x,y⟩"

  fixes seqprod ("∏ _" 71)
  defines seqprod_def [simp]: "∏ a ≡ Fold1(f,a)"

  fixes append (infix "\<hookleftarrow>" 72)
  defines append_def [simp]: "a \<hookleftarrow> x ≡ Append(a,x)"

  fixes concat (infixl "\<squnion>" 69)
  defines concat_def [simp]: "a \<squnion> b ≡ Concat(a,b)";

text{*The next lemma shows our assumption on the associativity
  of the semigroup operation in the notation defined in in the 
  @{text "semigr0"} context.*}

lemma (in semigr0) semigr_assoc: assumes "x ∈ G"  "y ∈ G"  "z ∈ G"
  shows "x·y·z = x·(y·z)"
  using assms assoc_assum IsAssociative_def by simp;

text{*In the way we define associativity the assumption that
  $f$ is associative on $G$ also implies that it is a binary
  operation on $X$. *}

lemma (in semigr0) semigr_binop: shows "f : G×G -> G"
  using assoc_assum IsAssociative_def by simp;

text{*Semigroup operation is closed.*}

lemma (in semigr0) semigr_closed: 
  assumes "a∈G"  "b∈G" shows "a·b ∈ G"
  using assms semigr_binop apply_funtype by simp;

text{*Lemma @{text "append_1elem"} written in the notation used in 
  the @{text "semigr0"} context.*}

lemma (in semigr0) append_1elem_nice: 
  assumes "n ∈ nat" and "a: n -> X" and "b : 1 -> X"
  shows "a \<squnion> b = a \<hookleftarrow> b`(0)"
  using assms append_1elem by simp;

text{*Lemma @{text "concat_init_last_elem"} rewritten
  in the notation used in the @{text "semigr0"} context.*}

lemma (in semigr0) concat_init_last: 
  assumes "n ∈ nat"  "k ∈ nat" and 
  "a: n -> X"  and "b : succ(k) -> X"
  shows "(a \<squnion> Init(b)) \<hookleftarrow> b`(k) = a \<squnion> b"
  using assms concat_init_last_elem by simp;

text{*The product of semigroup (actually, magma -- we don't
   need associativity for this) elements is in the semigroup.*}

lemma (in semigr0) prod_type: 
  assumes "n ∈ nat" and "a : succ(n) -> G"
  shows "(∏ a) ∈ G"
proof -
  from assms have 
    "succ(n) ∈ nat"  "f : G×G -> G"  "Tail(a) : n -> G"
    using semigr_binop tail_props by auto;
  moreover from assms have "a`(0) ∈ G" and "G ≠ 0"
    using empty_in_every_succ apply_funtype
    by auto;
  ultimately show "(∏ a) ∈ G" using Fold1_def fold_props
    by simp;
qed;

text{*What is the product of one element list?*}

lemma (in semigr0) prod_of_1elem: assumes A1: "a: 1 -> G"
  shows "(∏ a) = a`(0)"
proof -
  have "f : G×G -> G" using semigr_binop by simp;
  moreover from A1 have "Tail(a) : 0 -> G" using tail_props
    by blast;
  moreover from A1 have "a`(0) ∈ G" and "G ≠ 0" 
    using apply_funtype by auto;
  ultimately show "(∏ a) =  a`(0)" using fold_empty Fold1_def 
    by simp;
qed;

text{*What happens to the product of a list when we append an element 
  to the list?*}

lemma (in semigr0) prod_append: assumes A1: "n ∈ nat" and
  A2: "a : succ(n) -> G" and A3: "x∈G"
  shows "(∏ a\<hookleftarrow>x) = (∏ a) · x"
proof -
  from A1 A2 have I: "Tail(a) : n -> G"  "a`(0) ∈ G"
    using tail_props empty_in_every_succ apply_funtype
    by auto;
  from assms have "(∏ a\<hookleftarrow>x) = Fold(f,a`(0),Tail(a)\<hookleftarrow>x)"
    using head_of_append tail_append_commute Fold1_def
    by simp;
  also from A1 A3 I have "… = (∏ a) · x"
    using semigr_binop fold_append Fold1_def 
    by simp;
  finally show ?thesis by simp;
qed;

text{*The main theorem of the section: taking the product of 
  a sequence is distributive with respect to concatenation of sequences.
  The proof is by induction on the length of the second list.*}

theorem (in semigr0) prod_conc_distr: 
  assumes A1: "n ∈ nat"  "k ∈ nat" and
  A2: "a : succ(n) -> G"   "b: succ(k) -> G"
  shows "(∏ a) · (∏ b) = ∏ (a \<squnion> b)"
proof -
  from A1 have "k ∈ nat" by simp;
  moreover have "∀b ∈ succ(0) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b)"
  proof -
    { fix b assume A3: "b : succ(0) -> G"
      with A1 A2 have
	"succ(n) ∈ nat"  "a : succ(n) -> G"  "b : 1 -> G" 
	by auto;
      then have "a \<squnion> b = a \<hookleftarrow> b`(0)" by (rule append_1elem_nice);
      with A1 A2 A3 have "(∏ a) · (∏ b) = ∏ (a \<squnion> b)"
	using apply_funtype prod_append semigr_binop prod_of_1elem
	by simp;
    } thus ?thesis by simp;
  qed;
  moreover have "∀j ∈ nat. 
    (∀b ∈ succ(j) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b)) -->
    (∀b ∈ succ(succ(j)) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b))"
  proof -
    { fix j assume A4: "j ∈ nat" and 
      A5: "(∀b ∈ succ(j) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b))"
      { fix b assume A6: "b : succ(succ(j)) -> G"
	let ?c = "Init(b)"
	from A4 A6 have  T: "b`(succ(j)) ∈ G" and
	  I: "?c : succ(j) -> G" and II: "b = ?c\<hookleftarrow>b`(succ(j))"
	  using apply_funtype init_props by auto;
	from A1 A2 A4 A6 have
	  "succ(n) ∈ nat"  "succ(j) ∈ nat"
	  "a : succ(n) -> G"  "b : succ(succ(j)) -> G"
	  by auto;
	then have III: "(a \<squnion> ?c) \<hookleftarrow> b`(succ(j)) = a \<squnion> b"
	  by (rule concat_init_last);
	from A4 I T have "(∏ ?c\<hookleftarrow>b`(succ(j))) = (∏ ?c) · b`(succ(j))"
	  by (rule prod_append);
	with II have 
	  "(∏ a) · (∏ b) = (∏ a) · ((∏ ?c) · b`(succ(j)))"
	  by simp;
	moreover from A1 A2 A4 T I have
	  "(∏ a) ∈ G"  "(∏ ?c) ∈ G"  "b`(succ(j)) ∈ G"
	  using prod_type by auto;
	ultimately have 
	  "(∏ a) · (∏ b) =  ((∏ a) · (∏ ?c)) · b`(succ(j))"
	  using semigr_assoc by auto;
	with A5 I have "(∏ a) · (∏ b) = (∏ (a \<squnion> ?c))·b`(succ(j))"
	  by simp;
	moreover
	from A1 A2 A4 I have
	  T1: "succ(n) ∈ nat"  "succ(j) ∈ nat" and
	  "a : succ(n) -> G"   "?c : succ(j) -> G"
	  by auto;
	then have "Concat(a,?c): succ(n) #+ succ(j) -> G"
	  by (rule concat_props);
	with A1 A4 T have
	  "succ(n #+ j) ∈ nat"   
	  "a \<squnion> ?c : succ(succ(n #+j)) -> G"
	  "b`(succ(j)) ∈ G"
	  using succ_plus by auto;
	then have 
	  "(∏ (a \<squnion> ?c)\<hookleftarrow>b`(succ(j))) = (∏ (a \<squnion> ?c))·b`(succ(j))"
	  by (rule prod_append);
	with III have "(∏ (a \<squnion> ?c))·b`(succ(j)) =  ∏ (a \<squnion> b)"
	  by simp;
	ultimately have "(∏ a) · (∏ b) = ∏ (a \<squnion> b)"
	  by simp;
      } hence "(∀b ∈ succ(succ(j)) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b))"
	by simp;
    } thus ?thesis by blast;
  qed;
  ultimately have "∀b ∈ succ(k) -> G. (∏ a) · (∏ b) = ∏ (a \<squnion> b)"
    by (rule ind_on_nat);
  with A2 show "(∏ a) · (∏ b) = ∏ (a \<squnion> b)" by simp;
qed;

section{*Products over sets of indices*}

text{*In this section we study the properties of 
  expressions of the form
  $\prod_{i\in \Lambda} a_i = a_{i_0}\cdot a_{i_1} \cdot .. \cdot a_{i-1}$,
  i.e. what we denote as @{text "\<pr>(Λ,a)"}. $\Lambda$ here is
  a finite subset of some set $X$ and $a$ is a function defined
  on $X$ with values in the semigroup $G$.*}


text{* Suppose $a: X \rightarrow G$ is an indexed family of elements
  of a semigroup $G$ and 
  $\Lambda = \{i_0, i_1, .. , i_{n-1}\} \subseteq \mathbb{N}$ is a finite 
  set of indices. We want to define 
  $\prod_{i\in \Lambda} a_i = a_{i_0}\cdot a_{i_1} \cdot .. \cdot a_{i-1}$.
  To do that we use the notion of @{text "Enumeration"} defined in the
  @{text "Enumeration_ZF"} theory file that takes a set of indices and 
  lists them in increasing order, thus converting it to list. Then we use 
  the @{text "Fold1"} to multiply the resulting list. Recall that in 
  Isabelle/ZF the capital letter ''O'' denotes the composition of two 
  functions (or relations).
  *}

definition
  "SetFold(f,a,Λ,r) = Fold1(f,a O Enumeration(Λ,r))"

text{*  For 
  a finite subset $\Lambda$ of a linearly ordered set $X$
  we will write $\sigma (\Lambda )$ 
  to denote the enumeration of the elements of $\Lambda$, i.e. the only 
  order isomorphism $|\Lambda | \rightarrow \Lambda$, where 
  $|\Lambda | \in \mathbb{N}$ is the number of elements of $\Lambda $.
  We also define
  notation for taking a product over a set of indices of some sequence
  of semigroup elements. The product of semigroup
  elements over some set $\Lambda \subseteq X$ of indices
  of a sequence $a: X \rightarrow G$ (i.e. $\prod_{i\in \Lambda} a_i$) 
  is denoted @{text "\<pr>(Λ,a)"}.
  In the @{text "semigr1"} context we assume that $a$ is a 
  function defined on some
  linearly ordered set $X$ with values in the semigroup $G$.
  *}

locale semigr1 = semigr0 +
  
  fixes X r
  assumes linord: "IsLinOrder(X,r)"

  fixes a
  assumes a_is_fun: "a : X -> G"

  fixes σ
  defines σ_def [simp]: "σ(A) ≡ Enumeration(A,r)"

  fixes setpr ("\<pr>")
  defines setpr_def [simp]: "\<pr>(Λ,b) ≡ SetFold(f,b,Λ,r)";

text{*We can use the @{text "enums"} locale in the @{text "semigr0"} 
  context.*}

lemma (in semigr1) enums_valid_in_semigr1: shows "enums(X,r)"
  using linord enums_def by simp;

text{*Definition of product over a set expressed
  in notation of the @{text "semigr0"} locale.*}

lemma (in semigr1) setproddef: 
  shows "\<pr>(Λ,a) = ∏ (a O σ(Λ))"
  using SetFold_def by simp;

text{*A composition of enumeration of a nonempty 
  finite subset of $\mathbb{N}$
  with a sequence of elements of $G$ is a nonempty list of elements of $G$.
  This implies that a product over set of a finite set of indices belongs
  to the (carrier of) semigroup.
  *}

lemma (in semigr1) setprod_type: assumes 
  A1: "Λ ∈ FinPow(X)" and A2: "Λ≠0"
  shows 
  "∃n ∈ nat . |Λ| = succ(n) ∧ a O σ(Λ) : succ(n) -> G"
  and "\<pr>(Λ,a) ∈ G"
proof -
  from assms obtain n where "n ∈ nat" and "|Λ| = succ(n)"
    using card_non_empty_succ by auto
  from A1 have "σ(Λ) : |Λ| -> Λ"
    using enums_valid_in_semigr1 enums.enum_props 
    by simp;
  with A1 have "a O σ(Λ): |Λ| -> G"
    using a_is_fun FinPow_def comp_fun_subset 
    by simp;
  with `n ∈ nat` and `|Λ| = succ(n)` show 
    "∃n ∈ nat . |Λ| = succ(n) ∧ a O σ(Λ) : succ(n) -> G"
    by auto;
  from  `n ∈ nat` `|Λ| = succ(n)` `a O σ(Λ): |Λ| -> G`
  show "\<pr>(Λ,a) ∈ G" using prod_type setproddef 
    by auto;
qed;

text{*The @{text "enum_append"} lemma from the 
  @{text "Enemeration"} theory specialized for natural
  numbers.*} 

lemma (in semigr1) semigr1_enum_append: 
  assumes "Λ ∈ FinPow(X)" and
  "n ∈ X - Λ" and "∀k∈Λ. ⟨k,n⟩ ∈ r"
  shows "σ(Λ ∪ {n}) = σ(Λ)\<hookleftarrow> n"
  using assms  FinPow_def enums_valid_in_semigr1 
    enums.enum_append by simp;

text{*What is product over a singleton?*}

lemma (in semigr1) gen_prod_singleton: 
  assumes A1: "x ∈ X"
  shows  "\<pr>({x},a) = a`(x)"
proof -
  from A1 have "σ({x}): 1 -> X" and  "σ({x})`(0) = x"
    using enums_valid_in_semigr1 enums.enum_singleton
    by auto;
  then show "\<pr>({x},a) = a`(x)"
    using a_is_fun comp_fun setproddef prod_of_1elem 
      comp_fun_apply by simp;
qed;

text{*A generalization of @{text "prod_append"} to the products
  over sets of indices.*}

lemma (in semigr1) gen_prod_append: 
  assumes
  A1: "Λ ∈ FinPow(X)" and A2: "Λ ≠ 0" and
  A3: "n ∈ X -  Λ" and
  A4: "∀k∈Λ. ⟨k,n⟩ ∈ r"
  shows "\<pr>(Λ ∪ {n}, a) = (\<pr>(Λ,a)) · a`(n)"
proof -
  have "\<pr>(Λ ∪ {n}, a) =  ∏ (a O σ(Λ ∪ {n}))"
    using setproddef by simp;
  also from A1 A3 A4 have "… = ∏ (a O (σ(Λ)\<hookleftarrow> n))"
    using semigr1_enum_append by simp;
  also have "… = ∏ ((a O σ(Λ))\<hookleftarrow> a`(n))"
  proof -
    from A1 A3 have 
      "|Λ| ∈ nat" and "σ(Λ) : |Λ| -> X" and "n ∈ X" 
      using card_fin_is_nat enums_valid_in_semigr1 enums.enum_fun
      by auto;
    then show ?thesis using a_is_fun list_compose_append
      by simp;
  qed;
  also from assms have "… = (∏ (a O σ(Λ)))·a`(n)"
    using a_is_fun setprod_type apply_funtype prod_append
    by blast;
  also have "… = (\<pr>(Λ,a)) · a`(n)" 
    using SetFold_def by simp;
  finally show "\<pr>(Λ ∪ {n}, a) = (\<pr>(Λ,a)) · a`(n)"
    by simp;
qed;

text{*Very similar to @{text "gen_prod_append"}: a relation
  between a product over a set of indices and the product
  over the set with the maximum removed. *}

lemma (in semigr1) gen_product_rem_point:
  assumes A1: "A ∈ FinPow(X)" and
  A2: "n ∈ A" and  A4: "A - {n} ≠ 0" and
  A3: "∀k∈A. ⟨k, n⟩ ∈ r"
  shows
  "(\<pr>(A - {n},a)) · a`(n) = \<pr>(A, a)"
proof -
  let  = "A - {n}"
  from A1 A2 have "?Λ ∈ FinPow(X)" and "n ∈ X -  ?Λ"
    using fin_rem_point_fin FinPow_def by auto;
  with A3 A4 have "\<pr>(?Λ ∪ {n}, a) = (\<pr>(?Λ,a)) · a`(n)"
    using a_is_fun gen_prod_append by blast;
  with A2 show ?thesis using rem_add_eq by simp;
qed;

section{*Commutative semigroups*}

text{*Commutative semigroups are those whose operation is 
  commutative, i.e. $a\cdot b = b\cdot a$. This implies that
  for any permutation $s : n \rightarrow n$ we have
  $\prod_{j=0}^n a_j = \prod_{j=0}^n a_{s (j)}$,
  or, closer to the notation we are using in the @{text "semigr0"}
  context, $\prod a = \prod (a \circ s )$. Maybe one day we 
  will be able to prove this, but for now the goal is to prove 
  something simpler: that if the semigroup operation is commutative
  taking the product of a sequence is distributive with respect
  to the operation: 
  $\prod_{j=0}^n (a_j\cdot b_j) = \left(\prod_{j=0}^n a_j)\right) \left(\prod_{j=0}^n b_j)\right)$.
  Many of the rearrangements (namely those that don't use the inverse)
  proven in the @{text "AbelianGroup_ZF"} theory hold in fact in semigroups.
  Some of them will be reproven in this section.*}

text{*A rearrangement with 3 elements.*}

lemma (in semigr0) rearr3elems:
  assumes "f {is commutative on} G" and "a∈G"  "b∈G"  "c∈G"
  shows "a·b·c = a·c·b"
  using assms semigr_assoc IsCommutative_def by simp;

text{*A rearrangement of four elements.*}

lemma (in semigr0) rearr4elems: 
  assumes A1: "f {is commutative on} G" and 
  A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows "a·b·(c·d) = a·c·(b·d)"
proof -
  from A2 have "a·b·(c·d) = a·b·c·d"
    using semigr_closed semigr_assoc by simp;
  also have "a·b·c·d =  a·c·(b·d)"
  proof -
    from A1 A2 have "a·b·c·d = c·(a·b)·d"
      using IsCommutative_def semigr_closed 
      by simp;
    also from A2 have "… =  c·a·b·d"
      using semigr_closed semigr_assoc 
      by simp;
    also from A1 A2 have "… = a·c·b·d"
      using IsCommutative_def semigr_closed 
      by simp;
    also from A2 have "… = a·c·(b·d)" 
      using semigr_closed semigr_assoc
      by simp;
    finally show  "a·b·c·d =  a·c·(b·d)" by simp;
  qed;
  finally show  "a·b·(c·d) = a·c·(b·d)"
    by simp;
qed;
  
text{*We start with a version of @{text "prod_append"} that will shorten a bit
  the proof of the main theorem.*}

lemma (in semigr0) shorter_seq: assumes A1: "k ∈ nat" and
  A2: "a ∈ succ(succ(k)) -> G" 
  shows "(∏ a) = (∏ Init(a)) · a`(succ(k))"
proof -
  let ?x = "Init(a)"
  from assms have
    "a`(succ(k)) ∈ G" and "?x : succ(k) -> G"
    using apply_funtype init_props by auto;
  with A1 have "(∏ ?x\<hookleftarrow>a`(succ(k))) = (∏ ?x) · a`(succ(k))"
    using prod_append by simp;
  with assms show ?thesis using init_props
    by simp;
qed;

text{*A lemma useful in the induction step of the main theorem.*}

lemma (in semigr0) prod_distr_ind_step:
  assumes A1: "k ∈ nat" and
  A2: "a : succ(succ(k)) -> G" and
  A3: "b : succ(succ(k)) -> G" and
  A4: "c : succ(succ(k)) -> G" and
  A5: "∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j)"
  shows
  "Init(a) : succ(k) -> G"
  "Init(b) : succ(k) -> G"
  "Init(c) : succ(k) -> G"
  "∀j∈succ(k). Init(c)`(j) = Init(a)`(j) · Init(b)`(j)"
proof -
  from A1 A2 A3 A4 show 
    "Init(a) : succ(k) -> G"
    "Init(b) : succ(k) -> G"
    "Init(c) : succ(k) -> G"
    using init_props by auto;
  from A1 have T: "succ(k) ∈ nat" by simp;
  from T A2 have "∀j∈succ(k). Init(a)`(j) = a`(j)"
    by (rule init_props);
  moreover from T A3 have "∀j∈succ(k). Init(b)`(j) = b`(j)"
     by (rule init_props);
   moreover from T A4 have "∀j∈succ(k). Init(c)`(j) = c`(j)"
     by (rule init_props);
   moreover from A5 have "∀j∈succ(k). c`(j) = a`(j) · b`(j)"
     by simp;
   ultimately show "∀j∈succ(k). Init(c)`(j) = Init(a)`(j) · Init(b)`(j)"
     by simp;
qed;

text{*For commutative operations taking the product of a sequence 
  is distributive with respect to the operation.
  This version will probably not be used in applications,
  it is formulated in a way that is easier to prove by induction.
  For a more convenient formulation see @{text "prod_comm_distrib"}.
  The proof by induction on the length of the sequence.*}

theorem (in semigr0) prod_comm_distr: 
  assumes A1: "f {is commutative on} G" and A2: "n∈nat" 
  shows "∀ a b c. 
  (a : succ(n)->G ∧ b : succ(n)->G ∧ c : succ(n)->G ∧ 
  (∀j∈succ(n). c`(j) = a`(j) · b`(j))) -->
  (∏ c) = (∏ a) · (∏ b)"
proof -;
  note A2
  moreover have "∀ a b c. 
    (a : succ(0)->G ∧ b : succ(0)->G ∧ c : succ(0)->G ∧ 
    (∀j∈succ(0). c`(j) = a`(j) · b`(j))) -->
    (∏ c) = (∏ a) · (∏ b)"
  proof -
    { fix a b c 
      assume "a : succ(0)->G ∧ b : succ(0)->G ∧ c : succ(0)->G ∧ 
	(∀j∈succ(0). c`(j) = a`(j) · b`(j))"
      then have
	I: "a : 1->G"  "b : 1->G"  "c : 1->G" and
	II: "c`(0) = a`(0) · b`(0)" by auto;
      from I have
	"(∏ a) = a`(0)" and "(∏ b) = b`(0)" and "(∏ c) = c`(0)"
	using prod_of_1elem by auto;
      with II have "(∏ c) = (∏ a) · (∏ b)" by simp;
    } then show ?thesis using Fold1_def by simp;
  qed;
  moreover have "∀k ∈ nat. 
    (∀ a b c. 
    (a : succ(k)->G ∧ b : succ(k)->G ∧ c : succ(k)->G ∧ 
    (∀j∈succ(k). c`(j) = a`(j) · b`(j))) -->
    (∏ c) = (∏ a) · (∏ b)) -->
    (∀ a b c. 
    (a : succ(succ(k))->G ∧ b : succ(succ(k))->G ∧ c : succ(succ(k))->G ∧ 
    (∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j))) -->
    (∏ c) = (∏ a) · (∏ b))"
  proof;
    fix k assume "k ∈ nat"
    show "(∀a b c.
      a ∈ succ(k) -> G ∧
      b ∈ succ(k) -> G ∧ c ∈ succ(k) -> G ∧ 
      (∀j∈succ(k). c`(j) = a`(j) · b`(j)) -->
      (∏ c) = (∏ a) · (∏ b)) -->
      (∀a b c.
      a ∈ succ(succ(k)) -> G ∧
      b ∈ succ(succ(k)) -> G ∧
      c ∈ succ(succ(k)) -> G ∧ 
      (∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j)) -->
      (∏ c) = (∏ a) · (∏ b))"
    proof;
      assume A3: "∀a b c.
	a ∈ succ(k) -> G ∧
	b ∈ succ(k) -> G ∧ c ∈ succ(k) -> G ∧ 
	(∀j∈succ(k). c`(j) = a`(j) · b`(j)) -->
	(∏ c) = (∏ a) · (∏ b)"
      show "∀a b c.
	a ∈ succ(succ(k)) -> G ∧
	b ∈ succ(succ(k)) -> G ∧
	c ∈ succ(succ(k)) -> G ∧ 
	(∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j)) -->
	(∏ c) = (∏ a) · (∏ b)"
      proof -
	{ fix a b c 
	  assume 
	    "a ∈ succ(succ(k)) -> G ∧
	    b ∈ succ(succ(k)) -> G ∧
	    c ∈ succ(succ(k)) -> G ∧ 
	    (∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j))"
	  with `k ∈ nat` have I:
	    "a : succ(succ(k)) -> G"
	    "b : succ(succ(k)) -> G"
	    "c : succ(succ(k)) -> G"
	    and II: "∀j∈succ(succ(k)). c`(j) = a`(j) · b`(j)"
	    by auto;   
	  let ?x = "Init(a)"
          let ?y = "Init(b)"
          let ?z = "Init(c)"
	  from `k ∈ nat` I have III:
	    "(∏ a) = (∏ ?x) · a`(succ(k))"
	    "(∏ b) = (∏ ?y) · b`(succ(k))" and
	    IV: "(∏ c) = (∏ ?z) · c`(succ(k))"
	    using  shorter_seq by auto;
	  moreover
	  from  `k ∈ nat` I II have
	    "?x : succ(k) -> G"
	    "?y : succ(k) -> G"
	    "?z : succ(k) -> G" and
	    "∀j∈succ(k). ?z`(j) = ?x`(j) · ?y`(j)"
	    using prod_distr_ind_step by auto;
	  with A3 II IV have
	    "(∏ c) = (∏ ?x)·(∏ ?y)·(a`(succ(k)) · b`(succ(k)))"
	    by simp;
	  moreover from A1 `k ∈ nat` I III have
	    "(∏ ?x)·(∏ ?y)·(a`(succ(k)) · b`(succ(k)))=
	    (∏ a) · (∏ b)" 
	    using init_props prod_type apply_funtype 
	      rearr4elems by simp;
	  ultimately have "(∏ c) = (∏ a) · (∏ b)"
	    by simp;
	} thus ?thesis by auto;
      qed
    qed
  qed
  ultimately show ?thesis by (rule ind_on_nat);
qed;

text{*A reformulation of @{text "prod_comm_distr"} that is more
  convenient in applications.*}

theorem (in semigr0) prod_comm_distrib:
  assumes  "f {is commutative on} G" and "n∈nat" and
  "a : succ(n)->G"  "b : succ(n)->G"  "c : succ(n)->G" and
  "∀j∈succ(n). c`(j) = a`(j) · b`(j)"
  shows "(∏ c) = (∏ a) · (∏ b)"
  using assms prod_comm_distr by simp;

text{*A product of two products over disjoint sets of indices is the 
  product over the union.*}

lemma (in semigr1) prod_bisect:
  assumes  A1: "f {is commutative on} G"  and A2: "Λ ∈ FinPow(X)"
  shows 
  "∀P ∈  Bisections(Λ). \<pr>(Λ,a) = (\<pr>(fst(P),a))·(\<pr>(snd(P),a))"
proof -
  have "IsLinOrder(X,r)" using linord by simp;
  moreover have 
    "∀P ∈  Bisections(0). \<pr>(0,a) = (\<pr>(fst(P),a))·(\<pr>(snd(P),a))"
    using bisec_empty by simp;
  moreover have "∀ A ∈ FinPow(X). 
    ( ∀ n ∈ X - A. 
    (∀P ∈  Bisections(A). \<pr>(A,a) = (\<pr>(fst(P),a))·(\<pr>(snd(P),a))) 
    ∧ (∀k∈A. ⟨k,n⟩ ∈ r ) --> 
    (∀Q ∈  Bisections(A ∪ {n}). 
    \<pr>(A ∪ {n},a) = (\<pr>(fst(Q),a))·(\<pr>(snd(Q),a))))"
  proof -
    { fix A assume "A ∈ FinPow(X)"
      fix n assume "n ∈ X - A"
      have "( ∀P ∈ Bisections(A). 
	\<pr>(A,a) = (\<pr>(fst(P),a))·(\<pr>(snd(P),a))) 
	∧ (∀k∈A. ⟨k,n⟩ ∈ r )  --> 
	(∀Q ∈  Bisections(A ∪ {n}). 
	\<pr>(A ∪ {n},a) = (\<pr>(fst(Q),a))·(\<pr>(snd(Q),a)))"
      proof -
	{ assume I:
	  "∀P ∈ Bisections(A). \<pr>(A,a) = (\<pr>(fst(P),a))·(\<pr>(snd(P),a))"
	  and II: "∀k∈A. ⟨k,n⟩ ∈ r"
	  have "∀Q ∈  Bisections(A ∪ {n}). 
	    \<pr>(A ∪ {n},a) = (\<pr>(fst(Q),a))·(\<pr>(snd(Q),a))"
	  proof -
	    { fix Q assume "Q ∈  Bisections(A ∪ {n})"
	      let ?Q0 = "fst(Q)"
	      let ?Q1 = "snd(Q)"	      
	      from `A ∈ FinPow(X)` `n ∈ X - A` have "A ∪ {n} ∈ FinPow(X)"
		using singleton_in_finpow union_finpow by auto;
	      with `Q ∈  Bisections(A ∪ {n})` have
		"?Q0 ∈ FinPow(X)" "?Q0 ≠ 0" and "?Q1 ∈ FinPow(X)" "?Q1 ≠ 0"
		using bisect_fin bisec_is_pair Bisections_def by auto;
	      then have "\<pr>(?Q0,a) ∈ G" and "\<pr>(?Q1,a) ∈ G"
		using a_is_fun setprod_type by auto;
	      from `Q ∈ Bisections(A ∪ {n})` `A ∈ FinPow(X)` `n ∈ X-A`
	      have "refl(X,r)"  "?Q0 ⊆ A ∪ {n}"  "?Q1 ⊆ A ∪ {n}" 
		"A ⊆ X" and "n ∈ X"
		using linord IsLinOrder_def total_is_refl Bisections_def
		FinPow_def by auto;
	      from `refl(X,r)`  `?Q0 ⊆ A ∪ {n}`  `A ⊆ X` `n ∈ X` II 
	      have III: "∀k ∈ ?Q0. ⟨k, n⟩ ∈ r" by (rule refl_add_point);
	      from `refl(X,r)`  `?Q1 ⊆ A ∪ {n}`  `A ⊆ X` `n ∈ X` II 
	      have  IV: "∀k ∈ ?Q1. ⟨k, n⟩ ∈ r" by (rule refl_add_point);
	      from `n ∈ X - A` `Q ∈  Bisections(A ∪ {n})` have
		"?Q0 = {n} ∨ ?Q1 = {n} ∨ ⟨?Q0 - {n},?Q1-{n}⟩ ∈  Bisections(A)"
		using bisec_is_pair bisec_add_point by simp;
	      moreover
	      { assume "?Q1 = {n}"
		from `n ∈ X - A` have "n ∉ A" by auto;
		moreover 
		from  `Q ∈  Bisections(A ∪ {n})` 
		have "⟨?Q0,?Q1 ⟩ ∈  Bisections(A ∪ {n})"
		  using bisec_is_pair by simp;
		with `?Q1 = {n}` have "⟨?Q0, {n}⟩ ∈  Bisections(A ∪ {n})"
		  by simp;
		ultimately have "?Q0 = A" and "A ≠ 0" 
		  using set_point_bisec by auto;
		with `A ∈ FinPow(X)` `n ∈ X - A` II `?Q1 = {n}` 
		have "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·\<pr>(?Q1,a)"
		  using a_is_fun gen_prod_append gen_prod_singleton 
		  by simp }
	      moreover
	      { assume "?Q0 = {n}"
		from `n ∈ X - A` have "n ∈ X" by auto;
		then have "{n} ∈ FinPow(X)" and "{n} ≠ 0"
		  using singleton_in_finpow by auto;
		from `n ∈ X - A` have "n ∉ A" by auto;
		moreover 
		from  `Q ∈ Bisections(A ∪ {n})`
		have "⟨?Q0, ?Q1⟩ ∈  Bisections(A ∪ {n})"
		  using bisec_is_pair by simp;
		with `?Q0 = {n}` have "⟨{n}, ?Q1⟩ ∈  Bisections(A ∪ {n})"
		  by simp;
		ultimately have "?Q1 = A" and "A ≠ 0" using point_set_bisec
		  by auto;
		with A1 `A ∈ FinPow(X)` `n ∈ X - A` II
		  `{n} ∈ FinPow(X)`  `{n} ≠ 0` `?Q0 = {n}`
		have "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·(\<pr>(?Q1,a))"
		  using a_is_fun gen_prod_append gen_prod_singleton 
		    setprod_type IsCommutative_def by auto }
	      moreover
	      { assume A4: "⟨?Q0 - {n},?Q1 - {n}⟩ ∈  Bisections(A)"
		with `A ∈ FinPow(X)` have 
		  "?Q0 - {n} ∈ FinPow(X)" "?Q0 - {n} ≠ 0" and 
		  "?Q1 - {n} ∈ FinPow(X)" "?Q1 - {n} ≠ 0"
		  using FinPow_def Bisections_def by auto;
		with `n ∈ X - A` have 
		  "\<pr>(?Q0 - {n},a) ∈ G"  "\<pr>(?Q1 - {n},a) ∈ G"  and
		  T: "a`(n) ∈ G"
		  using a_is_fun setprod_type apply_funtype by auto;
		from `Q ∈ Bisections(A ∪ {n})` A4 have
		  "(⟨?Q0, ?Q1 - {n}⟩ ∈ Bisections(A) ∧ n ∈ ?Q1) ∨ 
		  (⟨?Q0 - {n}, ?Q1⟩ ∈ Bisections(A) ∧ n ∈ ?Q0) "
		  using bisec_is_pair bisec_add_point_case3 by auto;
		moreover
		{ assume "⟨?Q0, ?Q1 - {n}⟩ ∈ Bisections(A)" and "n ∈ ?Q1"
		  then have "A ≠ 0" using bisec_props by simp;
		  with A2 `A ∈ FinPow(X)` `n ∈ X - A` I II T IV
		    `⟨?Q0, ?Q1 - {n}⟩ ∈ Bisections(A)` `\<pr>(?Q0,a) ∈ G` 
		    `\<pr>(?Q1 - {n},a) ∈ G` `?Q1 ∈ FinPow(X)` 
		    `n ∈ ?Q1` `?Q1 - {n} ≠ 0`
		  have "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·(\<pr>(?Q1,a))"
		    using gen_prod_append semigr_assoc gen_product_rem_point 
		    by simp }
		moreover
		{ assume "⟨?Q0 - {n}, ?Q1⟩ ∈ Bisections(A)" and "n ∈ ?Q0"
		  then have "A ≠ 0" using bisec_props by simp;
		  with A1 A2 `A ∈ FinPow(X)` `n ∈ X - A` I II III T 
		    `⟨?Q0 - {n}, ?Q1⟩∈Bisections(A)` `\<pr>(?Q0 - {n},a)∈G` 
		    `\<pr>(?Q1,a) ∈ G` `?Q0 ∈ FinPow(X)` `n ∈ ?Q0` `?Q0-{n}≠0`
		  have "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·(\<pr>(?Q1,a))"
		    using gen_prod_append rearr3elems gen_product_rem_point 
		      by simp }
		ultimately have
		  "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·(\<pr>(?Q1,a))"
		  by auto }
	      ultimately have "\<pr>(A ∪ {n},a) = (\<pr>(?Q0,a))·(\<pr>(?Q1,a))"
		by auto;	
	    } thus ?thesis by simp
	  qed
	} thus ?thesis by simp;
      qed;
    } thus ?thesis by simp;
  qed  
  moreover note A2
  ultimately show ?thesis by (rule fin_ind_add_max);
qed;

text{*A better looking reformulation of @{text "prod_bisect"}.
  *}

theorem (in semigr1) prod_disjoint: assumes
  A1: "f {is commutative on} G"  and 
  A2: "A ∈ FinPow(X)" "A ≠ 0" and
  A3: "B ∈ FinPow(X)" "B ≠ 0" and
  A4: "A ∩ B = 0"
  shows "\<pr>(A∪B,a) = (\<pr>(A,a))·(\<pr>(B,a))"
proof -
  from A2 A3 A4 have "⟨A,B⟩ ∈ Bisections(A∪B)"
    using is_bisec by simp;
  with A1 A2 A3 show ?thesis
    using a_is_fun union_finpow prod_bisect by simp;
qed;

text{*A generalization of @{text "prod_disjoint"}.*}

lemma (in semigr1) prod_list_of_lists: assumes
  A1: "f {is commutative on} G"  and A2: "n ∈ nat"
  shows "∀M ∈ succ(n) -> FinPow(X). 
  M {is partition} --> 
  (∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ succ(n)}) = 
  (\<pr>(\<Union>i ∈ succ(n). M`(i),a))"
proof -
  note A2
  moreover have "∀M ∈ succ(0) -> FinPow(X). 
    M {is partition} --> 
    (∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ succ(0)}) = (\<pr>(\<Union>i ∈ succ(0). M`(i),a))"
    using a_is_fun func1_1_L1 Partition_def apply_funtype setprod_type
      list_len1_singleton prod_of_1elem 
    by simp;
  moreover have "∀k ∈ nat. 
    (∀M ∈ succ(k) -> FinPow(X). 
    M {is partition} --> 
    (∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ succ(k)}) = 
    (\<pr>(\<Union>i ∈ succ(k). M`(i),a))) -->
    (∀M ∈ succ(succ(k)) -> FinPow(X). 
    M {is partition} --> 
    (∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ succ(succ(k))}) = 
    (\<pr>(\<Union>i ∈ succ(succ(k)). M`(i),a)))";
  proof -
    { fix k assume "k ∈ nat"
      assume A3: "∀M ∈ succ(k) -> FinPow(X). 
	M {is partition} --> 
	(∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ succ(k)}) = 
	(\<pr>(\<Union>i ∈ succ(k). M`(i),a))";
      have "(∀N ∈ succ(succ(k)) -> FinPow(X). 
	N {is partition} --> 
	(∏ {⟨i,\<pr>(N`(i),a)⟩. i ∈ succ(succ(k))}) = 
	(\<pr>(\<Union>i ∈ succ(succ(k)). N`(i),a)))"
      proof -
	{ fix N assume A4: "N : succ(succ(k)) -> FinPow(X)"
	  assume A5: "N {is partition}"
	  with A4 have I: "∀i ∈ succ(succ(k)). N`(i) ≠ 0"
	    using func1_1_L1 Partition_def by simp;
	  let ?b = "{⟨i,\<pr>(N`(i),a)⟩. i ∈ succ(succ(k))}"
	  let ?c = "{⟨i,\<pr>(N`(i),a)⟩. i ∈ succ(k)}"
	  have II: "∀i ∈ succ(succ(k)). \<pr>(N`(i),a) ∈ G"
	  proof 
	    fix i assume "i ∈ succ(succ(k))"
	    with A4 I have "N`(i) ∈ FinPow(X)" and "N`(i) ≠ 0"
	      using apply_funtype by auto;
	    then show "\<pr>(N`(i),a) ∈ G" using setprod_type
	      by simp;
	  qed;
	  hence "∀i ∈ succ(k).  \<pr>(N`(i),a) ∈ G" by auto;
	  then have "?c : succ(k) -> G" by (rule ZF_fun_from_total);
	  have "?b = {⟨i,\<pr>(N`(i),a)⟩. i ∈ succ(succ(k))}"
	    by simp;
	  with II have "?b = Append(?c,\<pr>(N`(succ(k)),a))"
	    by (rule set_list_append);
	  with  II  `k ∈ nat` `?c : succ(k) -> G` 
	  have "(∏ ?b) = (∏ ?c)·(\<pr>(N`(succ(k)),a))"
	    using prod_append by simp;
	  also have 
	    "… =  (\<pr>(\<Union>i ∈ succ(k). N`(i),a))·(\<pr>(N`(succ(k)),a))"
	  proof -
	    let ?M = "restrict(N,succ(k))"
	    have "succ(k) ⊆ succ(succ(k))" by auto;
	    with `N : succ(succ(k)) -> FinPow(X)`
	    have "?M : succ(k) -> FinPow(X)" and
	      III: "∀i ∈ succ(k). ?M`(i) = N`(i)"
	      using restrict_type2 restrict apply_funtype 
	      by auto;
	    with A5 `?M : succ(k) -> FinPow(X)`have "?M {is partition}"
	      using func1_1_L1 Partition_def by simp;
	    with A3 `?M : succ(k) -> FinPow(X)` have
	      "(∏ {⟨i,\<pr>(?M`(i),a)⟩. i ∈ succ(k)}) = 
	      (\<pr>(\<Union>i ∈ succ(k). ?M`(i),a))"
	      by blast;
	    with III show ?thesis by simp;
	  qed;
	  also have "… = (\<pr>(\<Union>i ∈ succ(succ(k)). N`(i),a))"
	  proof -
	    let ?A = "\<Union>i ∈ succ(k). N`(i)"
	    let ?B = "N`(succ(k))"
	    from A4 `k ∈ nat` have "succ(k) ∈ nat" and
	      "∀i ∈ succ(k). N`(i) ∈ FinPow(X)"
	      using apply_funtype by auto;
	    then have "?A ∈ FinPow(X)" by (rule union_fin_list_fin);
	    moreover from I have "?A ≠ 0" by auto;
	    moreover from A4 I have 
	      "N`(succ(k)) ∈ FinPow(X)" and "N`(succ(k)) ≠ 0"
	      using apply_funtype by auto;
	    moreover from `succ(k) ∈ nat` A4 A5 have "?A ∩ ?B = 0"
	      by (rule list_partition);
	    moreover note A1
	    ultimately have "\<pr>(?A∪?B,a) = (\<pr>(?A,a))·(\<pr>(?B,a))"
	      using prod_disjoint by simp;
	    moreover have "?A ∪ ?B = (\<Union>i ∈ succ(succ(k)). N`(i))"
	      by auto;
	    ultimately show ?thesis by simp;
	  qed;
	  finally have "(∏ {⟨i,\<pr>(N`(i),a)⟩. i ∈ succ(succ(k))}) = 
	    (\<pr>(\<Union>i ∈ succ(succ(k)). N`(i),a))"
	    by simp;
	  } thus ?thesis by auto;
	qed
	} thus ?thesis by simp;
  qed
  ultimately show ?thesis by (rule ind_on_nat);
qed;

text{*A more convenient reformulation of @{text "prod_list_of_lists"}.
  *}

theorem (in semigr1) prod_list_of_sets: 
  assumes A1: "f {is commutative on} G"  and 
  A2: "n ∈ nat"  "n ≠ 0" and
  A3: "M : n -> FinPow(X)"   "M {is partition}"
  shows
  "(∏ {⟨i,\<pr>(M`(i),a)⟩. i ∈ n}) = (\<pr>(\<Union>i ∈ n. M`(i),a))"
proof -
  from A2 obtain k where "k ∈ nat" and "n = succ(k)"
    using Nat_ZF_1_L3 by auto;
  with A1 A3 show ?thesis using prod_list_of_lists
    by simp;
qed

text{*The definition of the product 
  @{text "\<pr>(A,a) ≡ SetFold(f,a,A,r)"} of a some (finite) set of 
  semigroup elements requires that $r$ is a linear order on the set 
  of indices $A$. This is necessary so that we know in which order
  we are multiplying the elements. The product over $A$ is defined 
  so that we have $\prod_A a = \prod a \circ \sigma(A)$ where
  $\sigma : |A| \rightarrow A$ is the enumeration of $A$ (the only
  order isomorphism between the number of elements in $A$ and $A$), see
  lemma @{text "setproddef"}.
  However, if the operation is commutative, the order is irrelevant. 
  The next theorem formalizes that fact stating that we can replace
  the enumeration $\sigma (A)$ by any bijection between $|A|$ and $A$.
  In a way this is a generalization of @{text "setproddef"}. 
  The proof is based on application of @{text "prod_list_of_sets"}
  to the finite collection of singletons that comprise $A$.*}

theorem (in semigr1) prod_order_irr: 
  assumes A1: "f {is commutative on} G" and
  A2: "A ∈ FinPow(X)" "A ≠ 0" and
  A3: "b ∈ bij(|A|,A)"
  shows "(∏ (a O b)) = \<pr>(A,a)"
proof -
  let ?n = "|A|"
  let ?M = "{⟨k, {b`(k)}⟩. k ∈ ?n}"
  have "(∏ (a O b)) = (∏ {⟨i,\<pr>(?M`(i),a)⟩. i ∈ ?n})"
  proof -
    have "∀i ∈ ?n. \<pr>(?M`(i),a) = (a O b)`(i)"
    proof;
      fix i assume "i ∈ ?n"
      with A2 A3 `i ∈ ?n` have "b`(i) ∈ X" 
	using bij_def inj_def apply_funtype FinPow_def
	by auto;
      then have "\<pr>({b`(i)},a) = a`(b`(i))" 
	using gen_prod_singleton by simp;
      with A3 `i ∈ ?n` have "\<pr>({b`(i)},a) = (a O b)`(i)"
	using bij_def inj_def comp_fun_apply by auto;
      with `i ∈ ?n` A3 show "\<pr>(?M`(i),a) = (a O b)`(i)"
	using bij_def inj_partition by auto;
    qed;
    hence "{⟨i,\<pr>(?M`(i),a)⟩. i ∈ ?n} = {⟨i,(a O b)`(i)⟩. i ∈ ?n}"
      by simp;
    moreover have "{⟨i,(a O b)`(i)⟩. i ∈ ?n} = a O b"
    proof -
      from A3 have "b : ?n -> A" using bij_def inj_def by simp;
      moreover from A2 have "A ⊆ X" using FinPow_def by simp;
      ultimately have "b : ?n -> X" by (rule func1_1_L1B);
      then have "a O b: ?n -> G" using a_is_fun comp_fun
	by simp;
      then show "{⟨i,(a O b)`(i)⟩. i ∈ ?n} = a O b"
	using fun_is_set_of_pairs by simp;
    qed;
    ultimately show ?thesis by simp;
  qed;
  also have "… = (\<pr>(\<Union>i ∈ ?n. ?M`(i),a))"
  proof -
    note A1
    moreover from A2 have "?n ∈ nat" and "?n ≠ 0"
      using card_fin_is_nat card_non_empty_non_zero by auto;
    moreover have "?M : ?n -> FinPow(X)" and "?M {is partition}"
    proof -
      from A2 A3 have "∀k ∈ ?n. {b`(k)} ∈  FinPow(X)"
	using bij_def inj_def apply_funtype FinPow_def
	  singleton_in_finpow by auto;
      then show "?M : ?n -> FinPow(X)" using ZF_fun_from_total
	by simp;
      from A3 show "?M {is partition}" using bij_def inj_partition
	by auto;
    qed;
    ultimately show
      "(∏ {⟨i,\<pr>(?M`(i),a)⟩. i ∈ ?n}) = (\<pr>(\<Union>i ∈ ?n. ?M`(i),a))"
      by (rule prod_list_of_sets);
  qed;
  also from A3 have "(\<pr>(\<Union>i ∈ ?n. ?M`(i),a)) = \<pr>(A,a)"
    using bij_def inj_partition surj_singleton_image
    by auto;
  finally show ?thesis by simp;
qed;

text{*Another way of expressing the fact that the product dos not depend
  on the order. *}

corollary (in semigr1) prod_bij_same: 
  assumes "f {is commutative on} G" and
  "A ∈ FinPow(X)" "A ≠ 0" and
  "b ∈ bij(|A|,A)" "c ∈ bij(|A|,A)"
  shows "(∏ (a O b)) = (∏ (a O c))"
  using assms prod_order_irr by simp;
    
end