Theory Group_ZF_1b

theory Group_ZF_1b
imports Group_ZF
(* 
    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\_1b.thy}*}

theory Group_ZF_1b 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:

  A: there is an element $e\in G$ such that for all 
  $g\in G$ we have $e\cdot g = g$ and $g\cdot e =g$. We call this element a 
  "unit" or a "neutral element" of the group.
  
  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.

  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 units
  $e$ is not empty. Of course it does work in the end as we can prove that
  the set of such neutral elements has exactly one element, but still the definition
  by itself is not valid. You just can't reference a variable bound by a quantifier
  outside of the scope of that quantifier.
  
  One way around this is to first use condition A to define
  the notion of a monoid, then prove the uniqueness of $e$ and then use the 
  condition B to define groups. 

  Another way is to write conditions A and B together as follows:
  
  $\exists_{e \in G} \ (\forall_{g \in G} \ e\cdot g = g \wedge g\cdot e = g) 
  \wedge (\forall_{a\in G}\exists_{b\in G}\  a\cdot b = e).$

  This is rather ugly.

  What I want to talk about 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 associative operation "$\cdot $" 
  such that 
  
  C: for every $a,b\in G$ the equations $a\cdot x = b$ and 
  $y\cdot a = b$ can be solved in $G$.
  
  This theory file aims at proving the equivalence of this 
  alternative definition with the usual definition of the group, as 
  formulated in @{text "Group_ZF.thy"}. The informal proofs come from an Aug. 14, 2005
  post by buli on the matematyka.org forum. *}

section{*An alternative definition of group*}

text{*First we will define notation for writing about groups.*}

text{*We will use the multiplicative notation for the group operation. To do this, we
  define a context (locale) 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{*The next theorem states that a set $G$ with an associative operation 
  that satisfies condition C is a group, as defined in IsarMathLib
  @{text "Group_ZF"} theory.*}

theorem (in group2) altgroup_is_group: 
  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 "a∈G" by auto;
  with A3 obtain x where "x∈G" and "a·x = a" 
    by auto;
  from A4 `a∈G` obtain y where "y∈G" and "y·a = a"
    by auto;
  have I: "∀b∈G. b = b·x ∧ b = y·b"
  proof;
    fix b assume "b∈G"
     with A4 `a∈G` obtain yb where "yb∈G"  
      and "yb·a = b" by auto;
    from A3 `a∈G` `b∈G` obtain xb where "xb∈G"  
      and "a·xb = b" by auto;
    from `a·x = a` `y·a = a` `yb·a = b` `a·xb = b` 
    have "b = yb·(a·x)" and "b = (y·a)·xb" 
      by auto;
    moreover from A2 `a∈G` `x∈G` `y∈G` `xb∈G` `yb∈G` have 
      "(y·a)·xb = y·(a·xb)"  "yb·(a·x) = (yb·a)·x"
      using IsAssociative_def by auto;
    moreover from `yb·a = b` `a·xb = b` 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 `x∈G` I have "x = y·x" by simp;  
    also from `y∈G` I have "y·x = y" by simp;
    finally show "x = y" by simp;
  qed;
  ultimately have "∀b∈G. b·x = b ∧ x·b = b" by simp;
  with A2 `x∈G` have "IsAmonoid(G,P)" using IsAmonoid_def by auto;
  with A3 show "IsAgroup(G,P)"
    using monoid0_def monoid0.unit_is_neutral IsAgroup_def
    by simp;
qed;

text{* The converse of @{text "altgroup_is_group"}: 
  in every (classically defined) group condition C holds.  
  In informal mathematics we can say "Obviously
  condition C holds in any group." In formalized mathematics the word "obviously" 
  is not in the language. The next theorem is proven in the context called
  @{text "group0"} defined in the theory @{text "Group_ZF.thy"}. Similarly to the
  @{text "group2"} that context defines $a\cdot b$ as $P\langle a,b\rangle$ 
  It also defines notation related to the group inverse and 
  adds an assumption that the pair $(G,P)$ is a group 
  to all its theorems. This is why in the next theorem we don't 
  explicitely assume that $(G,P)$ is a group - this assumption 
  is implicit in the context.*}

theorem (in group0) group_is_altgroup: shows 
  "∀a∈G.∀b∈G. ∃x∈G. a·x = b" and "∀a∈G.∀b∈G. ∃y∈G. y·a = b"
proof -
  { fix a b assume "a∈G"  "b∈G"
    let ?x = "a¯· b"
    let ?y = "b·a¯"
    from `a∈G`  `b∈G`  have 
      "?x ∈ G"  "?y ∈ G"  and  "a·?x = b"  "?y·a = b"
      using inverse_in_group group_op_closed inv_cancel_two
      by auto;
    hence "∃x∈G. a·x = b" and "∃y∈G. y·a = b" by auto;
  } thus 
      "∀a∈G.∀b∈G. ∃x∈G. a·x = b" and
      "∀a∈G.∀b∈G. ∃y∈G. y·a = b"
    by auto;
qed;
    
end