Theory Loop_ZF

(* 
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

textThis 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)  (eG. xG. 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. eG  ( gG. f`e,g = g  f`g,e = g))"

textWe 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: "eG. xG. ex = x  xe = 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

textIf 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

textThe neutral element is unique in the loop. 

lemma (in loop0) neut_uniq_loop: shows 
  "∃!e. eG  (xG. ex = x  xe = x)"
proof
  from ex_ident show "e. e  G  (xG. e  x = x  x  e = x)" by auto
next
  fix e y 
  assume "e  G  (xG. e  x = x  x  e = x)"  "y  G  (xG. y  x = x  x  y = x)"
  then have "ey =y" and "ey = 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 "xG. 𝟭x =x  x𝟭 = x"
proof -  
  let ?n = "THE e. eG  (xG. ex = x  xe = x)"
  have "𝟭 = TheNeutralElement(G,A)" by simp
  then have "𝟭 = ?n" unfolding TheNeutralElement_def by simp
  moreover have "?nG  (xG. ?nx = x  x?n = x)" using neut_uniq_loop theI
    by simp
  ultimately show "𝟭G" and "xG. 𝟭x = x  x𝟭 = x"
    by auto
qed

textEvery 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,{yG. A`y,x = TheNeutralElement(G,A)}. xG}"

textDefinition of the right inverse as a function on $G$: 

definition
  "RightInv(G,A)  {x,{yG. A`x,y = TheNeutralElement(G,A)}. xG}"

textIn a loop $G$ right and left inverses are functions on $G$. 

lemma (in loop0) lr_inv_fun: shows "LeftInv(G,A):GG" "RightInv(G,A):GG"
  unfolding LeftInv_def RightInv_def
  using neut_props_loop lrdiv_props(1,4) ZF1_1_L9 ZF_fun_from_total
  by auto

textRight and left inverses have desired properties.

lemma (in loop0) lr_inv_props: assumes "xG"
  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. yG  yx = 𝟭"
    using neut_props_loop(1) lrdiv_props(1) by simp
  then have "({yG.  yx = 𝟭})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. yG  xy = 𝟭"
    using neut_props_loop(1) lrdiv_props(4) by simp
  then have "x({yG.  xy = 𝟭}) = 𝟭"
    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