(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2005 - 2023 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. *) section ‹Monoids› theory Monoid_ZF imports func_ZF Loop_ZF Semigroup_ZF begin text‹This theory provides basic facts about monoids.› subsection‹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 ‹IsAmonoid(G,f)›. Here $G$ is the ''carrier'' of the monoid 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 ‹⊕› symbol to denote the monoid operation (for no particular reason).› locale monoid0 = fixes G f assumes monoidAssum: "IsAmonoid(G,f)" fixes monoper (infixl "⊕" 70) defines monoper_def [simp]: "a ⊕ b ≡ f`⟨a,b⟩" text‹Propositions proven in the ‹semigr0› locale are valid in the ‹monoid0› locale.› lemma (in monoid0) semigr0_valid_in_monoid0: shows "semigr0(G,f)" using monoidAssum IsAmonoid_def semigr0_def by simp 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 monoidAssum 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 monoidAssum show "∃e. e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)" using IsAmonoid_def by auto qed 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 monoidAssum 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 monoidAssum 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 monoidAssum 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 monoidAssum 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 ‹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 text‹The monoid operation is associative.› lemma (in monoid0) sum_associative: assumes "a∈G" "b∈G" "c∈G" shows "(a⊕b)⊕c = a⊕(b⊕c)" using assms monoidAssum unfolding IsAmonoid_def IsAssociative_def by auto text‹A simple rearrangement of four monoid elements transferred from the ‹semigr0› locale: › lemma (in monoid0) rearr4elem_monoid: assumes "a∈G" "b∈G" "c∈G" "d∈G" shows "a⊕b⊕(c⊕d) = a⊕(b⊕c)⊕d" using assms semigr0_valid_in_monoid0 semigr0.rearr4elem_assoc by simp end