Theory Group_ZF_1

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2005, 2006  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{Group\_ZF\_1.thy}*}

theory Group_ZF_1 imports Group_ZF 

begin

text{* In a typical textbook a group is defined as a set $G$ with an 
  associative operation such that two conditions hold: *}
text{* A: there is an element $e\in G$ such that for all 
  $g\in G$ we have $e\cdot a = a$ and $a\cdot e =a$. We call this element a 
  "unit" or a "neutral element" of the group.*}
text{* B: for every $a\in G$ there exists a $b\in G$ such that $a\cdot b = e$, 
  where $e$ is the element of $G$ whose existence is guaranteed by A. *}
text{*The validity of this definition is rather dubious to me, as condition 
  A does not define any specific element $e$ that can be referred to in 
  condition B - it merely states that a set of such neutral elements 
  $e$ is not empty.
  One way around this is to first use condition A to define
  the notion of monoid, then prove the uniqueness of $e$ and then use the 
  condition B to define groups. 
  However, there is an amusing way to define groups directly 
  without any reference to the neutral elements. Namely, we can define 
  a group as a non-empty set $G$ with an assocative operation "$\cdot $" 
  such that*} 
text{*C: for every $a,b\in G$ the equations $a\cdot x = b$ and 
  $y\cdot a = b$ can be solved in $G$.*}
text{*This theory file aims at proving the equivalence of this 
  alternative definition with the usual definition of the group, as 
  formulated in Group\_ZF.thy. The romantic proofs come from an Aug. 14, 2005, 2006
  post by buli on the matematyka.org forum.*}

section{*An alternative definition of group*}

text{*We will use the multiplicative notation for the group. To do this, we
  define a context (locale) similar to group0, that tells Isabelle
  to interpret $a\cdot b$ as the value of function $P$ on the pair 
  $\langle a,b \rangle$.*}

locale group2 =
  fixes P 
  fixes dot (infixl "·" 70)
  defines dot_def [simp]: "a · b ≡ P`<a,b>";

text{*A set $G$ with an associative operation that satisfies condition C is 
  a group, as defined in @{text "Group_ZF"} theory file.*}

theorem (in group2) Group_ZF_1_T1: 
  assumes A1: "G≠0" and A2: "P {is associative on} G"
  and A3: "∀a∈G.∀b∈G. ∃x∈G. a·x = b"
  and A4: "∀a∈G.∀b∈G. ∃y∈G. y·a = b"
  shows "IsAgroup(G,P)"
proof -;
  from A1 obtain a where D1: "a∈G" by auto;
  with A3 obtain x where D2: "x∈G" and D3: "a·x = a" 
    by auto;
  from D1 A4 obtain y where D4: "y∈G" and D5: "y·a = a"
    by auto;
  have T1: "∀b∈G. b = b·x ∧ b = y·b"
  proof;
    fix b assume A5: "b∈G"
     with D1 A4 obtain yb where D6: "yb∈G"  
      and D7: "yb·a = b" by auto;
    from A5 D1 A3 obtain xb where D8: "xb∈G"  
      and D9: "a·xb = b" by auto;
    from D7 D3 D9 D5 have 
      "b = yb·(a·x)"  "b = (y·a)·xb" by auto;
    moreover from D1 D2 D4 D8 D6 A2 have 
      "(y·a)·xb = y·(a·xb)"  "yb·(a·x) = (yb·a)·x"
      using IsAssociative_def by auto;
    moreover from D7 D9 have 
      "(yb·a)·x = b·x"  "y·(a·xb) = y·b"
      by auto;
    ultimately show "b = b·x ∧ b = y·b" by simp;
  qed;
  moreover have "x = y"
  proof -;
    from D2 T1 have "x = y·x" by simp;  
    also from D4 T1 have "y·x = y" by simp;
    finally show ?thesis by simp;
  qed;
  ultimately have "∀b∈G. b·x = b ∧ x·b = b" by simp;
  with D2 A2 have "IsAmonoid(G,P)" using IsAmonoid_def by auto;
  with A3 show "IsAgroup(G,P)"
    using monoid0_def monoid0.group0_1_L3 IsAgroup_def
    by simp;
qed;
    
end