(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2021 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 ‹ Loops › theory Loop_ZF imports Quasigroup_ZF begin text‹This theory specifies the definition and proves basic properites of loops. Loops are very similar to groups, the only property that is missing is associativity of the operation.› subsection‹ Definitions and notation › text‹ In this section we define the notions of identity element and left and right inverse. › text‹ A loop is a quasigroup with an identity elemen. › definition "IsAloop(G,A) ≡ IsAquasigroup(G,A) ∧ (∃e∈G. ∀x∈G. A`⟨e,x⟩ = x ∧ A`⟨x,e⟩ = x)" text‹ The neutral element for a binary operation $A:G\times G \rightarrow G $ is defined as the only element $e$ of $G$ such that $A\langle x,e\rangle = x$ and $A\langle e,x\rangle = x$ for all $x\in G$. Note that although the loop definition guarantees the existence of (some) such element(s) at this point we do not know if this element is unique. We can define this notion h ere but it will become usable only after we prove uniqueness. › definition "TheNeutralElement(G,f) ≡ ( THE e. e∈G ∧ (∀ g∈G. f`⟨e,g⟩ = g ∧ f`⟨g,e⟩ = g))" text‹We will reuse the notation defined in the ‹quasigroup0› locale, just adding the assumption about the existence of a neutral element and notation for it.› locale loop0 = quasigroup0 + assumes ex_ident: "∃e∈G. ∀x∈G. e⋅x = x ∧ x⋅e = x" fixes neut ("𝟭") defines neut_def[simp]: "𝟭 ≡ TheNeutralElement(G,A)" text‹ In the loop context the pair ‹(G,A)› forms a loop. › lemma (in loop0) is_loop: shows "IsAloop(G,A)" unfolding IsAloop_def using ex_ident qgroupassum by simp text‹If we know that a pair ‹(G,A)› forms a loop then the assumptions of the ‹loop0› locale hold. › lemma loop_loop0_valid: assumes "IsAloop(G,A)" shows "loop0(G,A)" using assms unfolding IsAloop_def loop0_axioms_def quasigroup0_def loop0_def by auto text‹The neutral element is unique in the loop. › lemma (in loop0) neut_uniq_loop: shows "∃!e. e∈G ∧ (∀x∈G. e⋅x = x ∧ x⋅e = x)" proof from ex_ident show "∃e. e ∈ G ∧ (∀x∈G. e ⋅ x = x ∧ x ⋅ e = x)" by auto next fix e y assume "e ∈ G ∧ (∀x∈G. e ⋅ x = x ∧ x ⋅ e = x)" "y ∈ G ∧ (∀x∈G. y ⋅ x = x ∧ x ⋅ y = x)" then have "e⋅y =y" and "e⋅y = e" by auto thus "e=y" by simp qed text‹ The neutral element as defined in the ‹loop0› locale is indeed neutral. › lemma (in loop0) neut_props_loop: shows "𝟭∈G" and "∀x∈G. 𝟭⋅x =x ∧ x⋅𝟭 = x" proof - let ?n = "THE e. e∈G ∧ (∀x∈G. e⋅x = x ∧ x⋅e = x)" have "𝟭 = TheNeutralElement(G,A)" by simp then have "𝟭 = ?n" unfolding TheNeutralElement_def by simp moreover have "?n∈G ∧ (∀x∈G. ?n⋅x = x ∧ x⋅?n = x)" using neut_uniq_loop theI by simp ultimately show "𝟭∈G" and "∀x∈G. 𝟭⋅x = x ∧ x⋅𝟭 = x" by auto qed text‹Every element of a loop has unique left and right inverse (which need not be the same). Here we define the left inverse as a function on $G$. › definition "LeftInv(G,A) ≡ {⟨x,⋃{y∈G. A`⟨y,x⟩ = TheNeutralElement(G,A)}⟩. x∈G}" text‹Definition of the right inverse as a function on $G$: › definition "RightInv(G,A) ≡ {⟨x,⋃{y∈G. A`⟨x,y⟩ = TheNeutralElement(G,A)}⟩. x∈G}" text‹In a loop $G$ right and left inverses are functions on $G$. › lemma (in loop0) lr_inv_fun: shows "LeftInv(G,A):G→G" "RightInv(G,A):G→G" unfolding LeftInv_def RightInv_def using neut_props_loop lrdiv_props(1,4) ZF1_1_L9 ZF_fun_from_total by auto text‹Right and left inverses have desired properties.› lemma (in loop0) lr_inv_props: assumes "x∈G" shows "LeftInv(G,A)`(x) ∈ G" "(LeftInv(G,A)`(x))⋅x = 𝟭" "RightInv(G,A)`(x) ∈ G" "x⋅(RightInv(G,A)`(x)) = 𝟭" proof - from assms show "LeftInv(G,A)`(x) ∈ G" and "RightInv(G,A)`(x) ∈ G" using lr_inv_fun apply_funtype by auto from assms have "∃!y. y∈G ∧ y⋅x = 𝟭" using neut_props_loop(1) lrdiv_props(1) by simp then have "(⋃{y∈G. y⋅x = 𝟭})⋅x = 𝟭" by (rule ZF1_1_L9) with assms show "(LeftInv(G,A)`(x))⋅x = 𝟭" using lr_inv_fun(1) ZF_fun_from_tot_val unfolding LeftInv_def by simp from assms have "∃!y. y∈G ∧ x⋅y = 𝟭" using neut_props_loop(1) lrdiv_props(4) by simp then have "x⋅(⋃{y∈G. x⋅y = 𝟭}) = 𝟭" by (rule ZF1_1_L9) with assms show "x⋅(RightInv(G,A)`(x)) = 𝟭" using lr_inv_fun(2) ZF_fun_from_tot_val unfolding RightInv_def by simp qed end