Theory Monoid_ZF

theory Monoid_ZF
imports func_ZF
(* 
This file is a part of IsarMathLib - 
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005 - 2008  Slawomir Kolodynski

This program 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{Monoid\_ZF.thy}*}

theory Monoid_ZF imports func_ZF

begin

text{*This theory provides basic facts about monoids.*}

section{*Definition and basic properties*}

text{*In this section we talk about monoids. 
  The notion of a monoid is similar to the notion of a semigroup 
  except that we require the existence of a neutral element.
  It is also similar to the notion of group except that
  we don't require existence of the inverse.*}

text{*Monoid is a set $G$ with an associative operation and a neutral element.
  The operation is a function on $G\times G$ with values in $G$. 
  In the context of ZF set theory this means that it is a set of pairs
  $\langle x,y \rangle$, where $x\in G\times G$ and $y\in G$. In other words 
  the operation is a certain subset of $(G\times G)\times G$. We express
  all this by defing a predicate @{text "IsAmonoid(G,f)"}. Here $G$ is the 
 ''carrier'' of the group and $f$ is the binary operation on it.
  *}

definition
  "IsAmonoid(G,f) ≡
  f {is associative on} G ∧ 
  (∃e∈G. (∀ g∈G. ( (f`(⟨e,g⟩) = g) ∧ (f`(⟨g,e⟩) = g))))"

text{* The next locale called ''monoid0'' defines a context for theorems
  that concern monoids. In this contex we assume that the pair $(G,f)$
  is a monoid.  We will use
  the @{text "⊕"} symbol to denote the monoid operation (for 
  no particular reason).*}

locale monoid0 =
  fixes G 
  fixes f
  assumes monoidAsssum: "IsAmonoid(G,f)"
  
  fixes monoper (infixl "⊕" 70)
  defines monoper_def [simp]: "a ⊕ b ≡ f`⟨a,b⟩";

text{*The result of the monoid operation is in the monoid (carrier).*}

lemma (in monoid0) group0_1_L1: 
  assumes "a∈G"  "b∈G" shows "a⊕b ∈ G"; 
  using assms monoidAsssum IsAmonoid_def IsAssociative_def apply_funtype
  by auto;

text{*There is only one neutral element in a monoid.*}

lemma (in monoid0) group0_1_L2: shows
  "∃!e. e∈G ∧ (∀ g∈G. ( (e⊕g = g) ∧ g⊕e = g))"
proof
  fix e y
  assume "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
    and "y ∈ G ∧ (∀g∈G. y ⊕ g = g ∧ g ⊕ y = g)"
  then have "y⊕e = y" "y⊕e = e" by auto;
  thus "e = y" by simp;
next from monoidAsssum show 
    "∃e. e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)"
    using IsAmonoid_def by auto;
qed;

text{*We could put the definition of neutral element anywhere, 
  but it is only usable in conjuction  with the above lemma.*}

definition 
 "TheNeutralElement(G,f) ≡ 
  ( THE e. e∈G ∧ (∀ g∈G. f`⟨e,g⟩ = g ∧ f`⟨g,e⟩ = g))";

text{*The neutral element is neutral.*}

lemma (in monoid0) unit_is_neutral:
  assumes A1: "e = TheNeutralElement(G,f)"
  shows "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
proof -;
  let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)";
  have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
    using group0_1_L2 by simp;
  then have "?n∈ G ∧ (∀ g∈G. ?n⊕g = g ∧ g⊕?n = g)"
    by (rule theI);
  with A1 show ?thesis 
    using TheNeutralElement_def by simp;
qed;

text{*The monoid carrier is not empty.*}

lemma (in monoid0) group0_1_L3A: shows "G≠0"
proof -;
  have "TheNeutralElement(G,f) ∈ G" using unit_is_neutral
    by simp;
  thus ?thesis by auto;
qed;

text{* The range of the monoid operation is the whole monoid carrier.*}

lemma (in monoid0) group0_1_L3B: shows "range(f) = G"
proof;
  from monoidAsssum have "f : G×G->G"
     using IsAmonoid_def IsAssociative_def by simp;
  then show "range(f) ⊆ G" 
    using func1_1_L5B by simp;
  show "G ⊆ range(f)"
  proof;
    fix g assume A1: "g∈G"
    let ?e = "TheNeutralElement(G,f)"
    from A1 have "⟨?e,g⟩ ∈ G×G" "g = f`⟨?e,g⟩"
      using unit_is_neutral by auto;
    with `f : G×G->G` show "g ∈ range(f)"
      using func1_1_L5A by blast;
  qed;
qed

text{*Another way to state that the range of the monoid operation
  is the whole monoid carrier.*}

lemma (in monoid0) range_carr: shows "f``(G×G) = G"
  using monoidAsssum IsAmonoid_def IsAssociative_def
    group0_1_L3B range_image_domain by auto;
      
text{*In a monoid any neutral element is the neutral element.*}

lemma (in monoid0) group0_1_L4: 
  assumes A1: "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)"
  shows "e = TheNeutralElement(G,f)"
proof -
  let ?n = "THE b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)";
  have "∃!b. b∈ G ∧ (∀ g∈G. b⊕g = g ∧ g⊕b = g)"
    using group0_1_L2 by simp;
  moreover note A1
  ultimately have "?n = e" by (rule the_equality2);
  then show ?thesis using TheNeutralElement_def by simp;
qed;

text{*The next lemma shows that if the if we restrict the monoid operation to
  a subset of $G$ that contains the neutral element, then the 
  neutral element of the monoid operation is also neutral with the 
  restricted operation.
*}

lemma (in monoid0) group0_1_L5:
  assumes A1: "∀x∈H.∀y∈H. x⊕y ∈ H"
  and A2: "H⊆G"
  and A3: "e = TheNeutralElement(G,f)"
  and A4: "g = restrict(f,H×H)"
  and A5: "e∈H"
  and A6: "h∈H"
  shows "g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h";
proof -;
  from A4 A6 A5 have 
    "g`⟨e,h⟩ = e⊕h ∧ g`⟨h,e⟩ = h⊕e"
    using restrict_if by simp;
  with A3 A4 A6 A2 show 
    "g`⟨e,h⟩ = h ∧ g`⟨h,e⟩ = h"
    using  unit_is_neutral by auto;
qed

text{*The next theorem shows that if the monoid operation is closed
  on a subset of $G$ then this set is a (sub)monoid (although 
  we do not define this notion). This fact will be 
  useful when we study subgroups. *}

theorem (in monoid0) group0_1_T1: 
  assumes A1: "H {is closed under} f"
  and A2: "H⊆G"
  and A3: "TheNeutralElement(G,f) ∈ H"
  shows  "IsAmonoid(H,restrict(f,H×H))"
proof -;
  let ?g = "restrict(f,H×H)"
  let ?e = "TheNeutralElement(G,f)"
  from monoidAsssum have "f ∈ G×G->G" 
    using IsAmonoid_def IsAssociative_def by simp;
  moreover from A2 have "H×H ⊆ G×G" by auto;
  moreover from A1 have "∀p ∈ H×H. f`(p) ∈ H"
    using IsOpClosed_def by auto;
  ultimately have "?g ∈ H×H->H";
    using func1_2_L4 by simp;
  moreover have "∀x∈H.∀y∈H.∀z∈H. 
    ?g`⟨?g`⟨x,y⟩ ,z⟩ = ?g`⟨x,?g`⟨y,z⟩⟩"
  proof -
    from A1 have "∀x∈H.∀y∈H.∀z∈H.
      ?g`⟨?g`⟨x,y⟩,z⟩ = x⊕y⊕z"
      using IsOpClosed_def restrict_if by simp;
    moreover have "∀x∈H.∀y∈H.∀z∈H. x⊕y⊕z = x⊕(y⊕z)"
    proof -;
      from monoidAsssum have 
	"∀x∈G.∀y∈G.∀z∈G. x⊕y⊕z = x⊕(y⊕z)"
	using IsAmonoid_def IsAssociative_def 
	by simp;
      with A2 show ?thesis by auto;
    qed;
    moreover from A1 have 
      "∀x∈H.∀y∈H.∀z∈H. x⊕(y⊕z) = ?g`⟨ x,?g`⟨y,z⟩ ⟩"
      using IsOpClosed_def restrict_if by simp;
    ultimately show ?thesis by simp; 
  qed;
  moreover have 
    "∃n∈H. (∀h∈H. ?g`⟨n,h⟩ = h ∧ ?g`⟨h,n⟩ = h)"
  proof -;
    from A1 have "∀x∈H.∀y∈H. x⊕y ∈ H"
      using IsOpClosed_def by simp;
    with A2 A3 have 
      "∀ h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h"
      using group0_1_L5 by blast;
    with A3 show ?thesis by auto;
  qed;
  ultimately show ?thesis using IsAmonoid_def IsAssociative_def 
    by simp;
qed;
    
text{*Under the assumptions of @{text " group0_1_T1"}
  the neutral element of a 
  submonoid is the same as that of the monoid.*}

lemma group0_1_L6: 
  assumes A1: "IsAmonoid(G,f)"
  and A2: "H {is closed under} f"
  and A3: "H⊆G"
  and A4: "TheNeutralElement(G,f) ∈ H"
  shows "TheNeutralElement(H,restrict(f,H×H)) = TheNeutralElement(G,f)"
proof -
  let ?e = "TheNeutralElement(G,f)"
  let ?g = "restrict(f,H×H)"
  from assms have "monoid0(H,?g)";
    using monoid0_def monoid0.group0_1_T1 
    by simp;
  moreover have 
    "?e ∈ H ∧ (∀h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h)"
  proof -;
    { fix h assume "h ∈ H"
      with assms have
	"monoid0(G,f)"  "∀x∈H.∀y∈H. f`⟨x,y⟩ ∈ H" 
	"H⊆G"  "?e = TheNeutralElement(G,f)"  "?g = restrict(f,H×H)"
	"?e ∈ H"  "h ∈ H" 
	using monoid0_def IsOpClosed_def by auto;
      then have "?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h"
	by (rule monoid0.group0_1_L5);
    } hence "∀h∈H. ?g`⟨?e,h⟩ = h ∧ ?g`⟨h,?e⟩ = h" by simp;
    with A4 show ?thesis by simp;
  qed;
  ultimately have "?e =  TheNeutralElement(H,?g)"
    by (rule monoid0.group0_1_L4);
  thus ?thesis by simp;
qed;

text{*If a sum of two elements is not zero, 
  then at least one has to be nonzero.*}

lemma (in monoid0) sum_nonzero_elmnt_nonzero: 
  assumes "a ⊕ b ≠ TheNeutralElement(G,f)"
  shows "a ≠ TheNeutralElement(G,f) ∨ b ≠ TheNeutralElement(G,f)";
  using assms unit_is_neutral by auto;

end