Theory Group_ZF

(* 
This file is a part of IsarMathLib - 
a library of formalized mathematics 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.thy}*}

theory Group_ZF imports func_ZF 

begin;

text{*This theory file will cover basics of group theory.*}

section{*Monoids.*}

text{*Monoid is a set with an associative operation and a neutral element.
  The operation is of course a function on $G\times G$ with values in $G$, 
  and therefore it is a subset of $(G\times G)\times G$. 
  Those who don't like that can go to HOL. 
  Monoid is like a group except that we don't require existence of 
  the inverse.*}

constdefs
  "IsAmonoid(G,f) ≡
  f {is associative on} G ∧ 
  (∃e∈G. (∀ g∈G. ( (f`(<e,g>) = g) ∧ (f`(<g,e>) = g))))";

text{*We use locales to define notation. This allows to separate notation 
  and notion definitions. We would like to use additive notation for 
  monoid, but unfortunately + is already taken.*}

locale monoid0 =
  fixes G and f
  assumes monoidAsssum:"IsAmonoid(G,f)"
  
  fixes monoper (infixl "⊕" 70)
  defines monoper_def [simp]: "a ⊕ b ≡ f`<a,b>";

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 prems monoidAsssum IsAmonoid_def IsAssociative_def apply_funtype
  by auto;

text{*There is only one neutral element in monoid.*}

lemma (in monoid0) group0_1_L2: 
  "∃!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 monoidAsssum show 
    "∃e. e∈ G ∧ (∀ g∈G. e⊕g = g ∧ g⊕e = g)"
    using IsAmonoid_def by auto;
qed;

text{*We could put the definition of neutral element anywhere, 
  but it is only usable in conjuction 
  with the above lemma.*}

constdefs 
 "TheNeutralElement(G,f) ≡ 
  ( THE e. e∈G ∧ (∀ g∈G. f`<e,g> = g ∧ f`<g,e> = g))";

text{*The neutral element is neutral.*}

lemma (in monoid0) group0_1_L3:
  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;
  hence "?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: "G≠0"
proof -;
  have "TheNeutralElement(G,f) ∈ G" using group0_1_L3
    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: "range(f) = G"
proof;
  from monoidAsssum have T1:"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 group0_1_L3 by auto;
    with T1 show "g ∈ range(f)"
      using func1_1_L5A by blast;
  qed;
qed;
      
text{*In a monoid a 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 from A1 have 
    "e ∈ G ∧ (∀g∈G. e ⊕ g = g ∧ g ⊕ e = g)" .;
  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. This is proven separately because it is
  used more than once.
*}

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  group0_1_L3 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 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 monoidAsssum 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 monoidAsssum 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 @{text " 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 -
  def D1: e ≡ "TheNeutralElement(G,f)"
  def D2: g ≡ "restrict(f,H×H)"
  with A1 A2 A3 A4 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 -;
    from A1 A2 have "monoid0(G,f)" "∀x∈H.∀y∈H. f`<x,y> ∈ H"
      using monoid0_def IsOpClosed_def by auto;
    with A3 D1 D2 A4 show ?thesis
      using monoid0.group0_1_L5 by blast;
  qed;
  ultimately have "e =  TheNeutralElement(H,g)"
    using monoid0.group0_1_L4 by auto;
  with D1 D2 show ?thesis by simp;
qed;
 
section{*Basic definitions and results for groups*}

text{*To define a group we take a monoid and add a requirement 
  that the right inverse needs to exist for every element of the group.
  We also define the group inverse as a relation on the group carrier.
  Later we will show that this relation is a function. 
  The @{text "GroupInv"} below is really the right inverse, understood as a function, 
  that is a subset of $G\times G$.*}

constdefs
  "IsAgroup(G,f) ≡ 
  (IsAmonoid(G,f) ∧ (∀g∈G. ∃b∈G. f`<g,b> = TheNeutralElement(G,f)))"

  "GroupInv(G,f) ≡ {<x,y> ∈ G×G. f`<x,y> = TheNeutralElement(G,f)}"

text{*We will use the miltiplicative notation for groups.*}

locale group0 =
  fixes G and f
  assumes groupAssum: "IsAgroup(G,f)"

  fixes neut ("\<one>")
  defines neut_def[simp]: "\<one> ≡ TheNeutralElement(G,f)"
  
  fixes groper (infixl "·" 70)
  defines groper_def [simp]: "a · b ≡ f`<a,b>"
  
  fixes inv ("_¯ " [90] 91)
  defines inv_def[simp]: "x¯ ≡ GroupInv(G,f)`(x)"

text{*First we show a lemma that says that we can use theorems proven in
  the @{text "monoid0"} context (locale).*}

lemma (in group0) group0_2_L1: "monoid0(G,f)"
  using groupAssum IsAgroup_def monoid0_def by simp;

text{*In some strange cases Isabelle has difficulties with applying
  the definition of a group. The next lemma defines a rule to be applied
  in such cases.*}

lemma definition_of_group: assumes "IsAmonoid(G,f)" 
  and "∀g∈G. ∃b∈G. f`⟨g,b⟩ = TheNeutralElement(G,f)"
  shows "IsAgroup(G,f)" 
  using prems IsAgroup_def by simp;

text{*Technical lemma that allows to use $1$ as the neutral element of 
the group without referencing a list of lemmas and definitions.*}

lemma (in group0) group0_2_L2: 
  shows "\<one>∈G ∧ (∀g∈G.(\<one>·g = g ∧ g·\<one> = g))"
  using group0_2_L1 monoid0.group0_1_L3 by simp;

text{*The group is closed under the group operation. Used all the time,
  useful to have handy.*}

lemma (in group0) group_op_closed: assumes "a∈G"  "b∈G"
  shows "a·b ∈ G" using prems group0_2_L1 monoid0.group0_1_L1 
  by simp;

text{*The group operation is associative. This is another technical lemma 
  that allows to shorten the list of referenced lemmas in some proofs.*}

lemma (in group0) group_oper_assoc: 
  assumes "a∈G"  "b∈G"  "c∈G" shows "a·(b·c) = a·b·c"
  using groupAssum prems IsAgroup_def IsAmonoid_def 
    IsAssociative_def group_op_closed by simp;

text{*The group operation maps $G\times G$ into $G$. It is conveniet to have
  this fact easily accessible in the group0 context.*}

lemma (in group0) group_oper_assocA: shows "f : G×G->G"
  using groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def
  by simp;
  
text{*The definition of group requires the existence of the right inverse.
  We show that this is also the left inverse.*}

theorem (in group0) group0_2_T1: 
  assumes A1: "g∈G" and A2: "b∈G" and A3: "g·b = \<one>"
  shows "b·g = \<one>";
proof -
  from A2 groupAssum obtain c where I: "c ∈ G ∧ b·c = \<one>" 
    using IsAgroup_def by auto;
  then have T1: "c∈G" by simp;
  have T2: "\<one>∈G" using group0_2_L2 by simp;
  from A1 A2 T2 I have "b·g =  b·(g·(b·c))"
    using group_op_closed group0_2_L2 group_oper_assoc 
    by simp;
  also from  A1 A2 T1 have "b·(g·(b·c)) = b·(g·b·c)"
    using group_oper_assoc by simp;
  also from A3 A2 I have "b·(g·b·c)= \<one>" using group0_2_L2 by simp;
  finally show "b·g = \<one>" by simp;
qed;

text{*For every element of a group there is only one inverse.*}

lemma (in group0) group0_2_L4: 
  assumes A1:"x∈G" shows "∃!y. y∈G ∧ x·y = \<one>"
proof;
  from A1 groupAssum show "∃y. y∈G ∧  x·y = \<one>" 
    using IsAgroup_def by auto;
  fix y n
  assume A2:"y∈G ∧  x·y = \<one>" and A3:"n∈G ∧ x·n = \<one>" show "y=n"
  proof -
    from A1 A2 have T1:"y·x = \<one>"
      using group0_2_T1 by simp;
    from A2 A3 have "y = y·(x·n)" 
      using group0_2_L2 by simp;
    also from A1 A2 A3 have "… = (y·x)·n" 
      using group_oper_assoc by blast;
    also from T1 A3 have "… = n" 
      using group0_2_L2 by simp;
    finally show "y=n" by simp;
  qed;
qed;

text{*The group inverse is a function that maps G into G.*}

theorem group0_2_T2: 
  assumes A1: "IsAgroup(G,f)" shows "GroupInv(G,f) : G->G"
proof -;
  have "GroupInv(G,f) ⊆ G×G" using GroupInv_def by auto;
  moreover from A1 have
    "∀x∈G. ∃!y. y∈ G ∧ <x,y> ∈ GroupInv(G,f)"
    using group0_def group0.group0_2_L4 GroupInv_def by simp;
  ultimately show ?thesis using func1_1_L11 by simp;
qed;

text{*We can think about the group inverse (the function) 
  as the inverse image of the neutral element.*}

theorem (in group0) group0_2_T3: shows "f-``{\<one>} = GroupInv(G,f)"
proof -;
  from groupAssum have "f : G×G -> G" 
    using IsAgroup_def IsAmonoid_def IsAssociative_def 
    by simp;
  then show "f-``{\<one>} = GroupInv(G,f)"
    using func1_1_L14 GroupInv_def by auto;
qed;

text{*The inverse is in the group.*}

lemma (in group0) inverse_in_group: assumes A1: "x∈G" shows "x¯∈G"
proof -
  from groupAssum have "GroupInv(G,f) : G->G" using group0_2_T2 by simp;
  with A1 show ?thesis using apply_type by simp;
qed;

text{*The notation for the inverse means what it is supposed to mean.*}

lemma (in group0) group0_2_L6: 
  assumes A1: "x∈G" shows "x·x¯ = \<one> ∧ x¯·x = \<one>"
proof;
  from groupAssum have "GroupInv(G,f) : G->G" 
    using group0_2_T2 by simp; 
  with A1 have "<x,x¯> ∈  GroupInv(G,f)" 
    using apply_Pair by simp;
  then show "x·x¯ = \<one>" using GroupInv_def by simp;
  with A1 show "x¯·x = \<one>" using inverse_in_group group0_2_T1 by blast; 
qed;

text{*The next two lemmas state that unless we multiply by 
  the neutral element, the result is always 
  different than any of the operands.*}

lemma (in group0) group0_2_L7: 
  assumes A1: "a∈G" and A2: "b∈G" and A3: "a·b = a"
  shows "b=\<one>"
proof -;
  from A3 have "a¯ · (a·b) = a¯·a" by simp;
  with A1 A2 show ?thesis using
    inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
    by simp;
qed;

lemma (in group0) group0_2_L8: 
  assumes A1: "a∈G" and A2: "b∈G" and A3:"a·b = b"
  shows "a=\<one>"
proof -;
  from A3 have "(a·b)·b¯  = b·b¯" by simp;
  with A1 A2 have "a·(b·b¯)  = b·b¯" using
    inverse_in_group group_oper_assoc by simp;
  with A1 A2 show ?thesis 
    using group0_2_L6 group0_2_L2 by simp;
qed;

text{*The inverse of the neutral element is the neutral element.*}

lemma (in group0) group_inv_of_one: shows "\<one>¯=\<one>"
  using group0_2_L2 inverse_in_group group0_2_L6 group0_2_L7 by blast;

text{*if $a^{-1} = 1$, then $a=1$. *}

lemma (in group0) group0_2_L8A:  
  assumes A1: "a∈G" and A2: "a¯ = \<one>"
  shows "a = \<one>"
proof -
  from A1 have "a·a¯ = \<one>" using group0_2_L6 by simp
  with A1 A2 show "a = \<one>" using group0_2_L2 by simp
qed;

text{*If $a$ is not a unit, then its inverse is not either.*}

lemma (in group0) group0_2_L8B:
  assumes "a∈G" and "a ≠ \<one>"
  shows "a¯ ≠ \<one>" using prems group0_2_L8A by auto;

text{*If $a^{-1}$ is not a unit, then a is not either.*}

lemma (in group0) group0_2_L8C:
  assumes "a∈G" and "a¯ ≠ \<one>"
  shows "a≠\<one>"
  using prems group0_2_L8A group_inv_of_one by auto;

text{*If a product of two elements of a group is equal to the neutral
element then they are inverses of each other. *}

lemma (in group0) group0_2_L9: 
  assumes A1: "a∈G" and A2: "b∈G" and A3: "a·b = \<one>" 
  shows "a = b¯"  "b = a¯"
proof -;
  from A3 have "a·b·b¯ = \<one>·b¯" by simp; 
  with A1 A2 have "a·(b·b¯) = \<one>·b¯" using
    inverse_in_group group_oper_assoc by simp;
  with A1 A2 show "a = b¯" using
    group0_2_L6 inverse_in_group group0_2_L2 by simp;
  from A3 have "a¯·(a·b) = a¯·\<one>" by simp;
  with A1 A2 show "b = a¯" using 
    inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
    by simp;
qed;

text{*It happens quite often that we know what is (have a meta-function for) 
  the right inverse in a group. The next lemma shows that the value 
  of the group inverse (function) is equal to the right inverse 
  (meta-function).*}

lemma (in group0) group0_2_L9A: 
  assumes A1: "∀g∈G. b(g) ∈ G ∧ g·b(g) = \<one>"
  shows "∀g∈G. b(g) = g¯"
proof;
  fix g assume A2: "g∈G"
  moreover from A2 A1 have "b(g) ∈ G" by simp;
  moreover from A1 A2 have "g·b(g) = \<one>" by simp;
  ultimately show "b(g) = g¯" by (rule group0_2_L9);
qed;
 
text{*What is the inverse of a product?*}

lemma (in group0) group_inv_of_two:
  assumes A1: "a∈G" and A2: "b∈G" 
  shows " b¯·a¯ = (a·b)¯"
proof -;
  from A1 A2 have 
    T1: "b¯∈G" and T2: "a¯∈G" and T3: "a·b∈G" and T4: "b¯·a¯ ∈ G"
    using inverse_in_group group_op_closed 
    by auto;
  from A1 A2 T4 have "a·b·(b¯·a¯) = a·(b·(b¯·a¯))"
    using group_oper_assoc by simp;
  moreover from A2 T1 T2 have "b·(b¯·a¯) = b·b¯·a¯"
    using group_oper_assoc by simp;
  moreover from A2 T2 have "b·b¯·a¯ = a¯"
     using group0_2_L6 group0_2_L2 by simp;
  ultimately have "a·b·(b¯·a¯) = a·a¯"
    by simp;
  with A1 have "a·b·(b¯·a¯) = \<one>"
    using group0_2_L6 by simp;
  with T3 T4 show "b¯·a¯ = (a·b)¯"
    using group0_2_L9 by simp;
qed;

text{*What is the inverse of a product of three elements?*}

lemma (in group0) group_inv_of_three:
  assumes A1: "a∈G"  "b∈G"  "c∈G"
  shows
  "(a·b·c)¯ = c¯·(a·b)¯"
  "(a·b·c)¯ = c¯·(b¯·a¯)"
  "(a·b·c)¯ = c¯·b¯·a¯"
proof -
  from A1 have T: 
    "a·b ∈ G" "a¯ ∈ G"  "b¯ ∈ G"   "c¯ ∈ G"  
    using group_op_closed inverse_in_group by auto;
  with A1 show 
    "(a·b·c)¯ = c¯·(a·b)¯" and "(a·b·c)¯ = c¯·(b¯·a¯)"
     using group_inv_of_two by auto;
   with T show "(a·b·c)¯ = c¯·b¯·a¯" using group_oper_assoc
     by simp;
qed;

text{*The inverse of the inverse is the element.*}

lemma (in group0) group_inv_of_inv:
  assumes "a∈G" shows "a = (a¯)¯"
  using prems inverse_in_group group0_2_L6 group0_2_L9 
  by simp;

text{*If $a^{-1}\cdot b=1$, then $a=b$.*}

lemma (in group0) group0_2_L11:
  assumes A1: "a∈G"  "b∈G" and A2: "a¯·b = \<one>"
  shows "a=b"
proof -
  from A1 A2 have "a¯ ∈ G"  "b∈G"  "a¯·b = \<one>" 
    using inverse_in_group by auto;
  then have "b = (a¯)¯" by (rule group0_2_L9);
  with A1 show "a=b" using group_inv_of_inv by simp;
qed;

text{*If $a\cdot b^{-1}=1$, then $a=b$.*}

lemma (in group0) group0_2_L11A: 
  assumes A1: "a∈G"  "b∈G" and A2: "a·b¯ = \<one>"
  shows "a=b"
proof -
  from A1 A2 have "a ∈ G"  "b¯∈G"  "a·b¯ = \<one>"
    using inverse_in_group by auto
  then have "a = (b¯)¯" by (rule group0_2_L9)
  with A1 show "a=b" using group_inv_of_inv by simp
qed;

text{*If if the inverse of $b$ is different than $a$, then the
  inverse of $a$ is different than $b$.*}

lemma (in group0) group0_2_L11B:
  assumes A1: "a∈G" and A2: "b¯ ≠ a"
  shows "a¯ ≠ b"
proof -
  { assume "a¯ = b"
    then have "(a¯)¯ = b¯" by simp
    with A1 A2 have False using group_inv_of_inv
      by simp;
  } then show "a¯ ≠ b" by auto;
qed;

text{*What is the inverse of $ab^{-1}$ ?*}

lemma (in group0) group0_2_L12:
  assumes A1: "a∈G"  "b∈G" 
  shows 
  "(a·b¯)¯ = b·a¯"
  "(a¯·b)¯ = b¯·a"
proof -
  from A1 have 
    "(a·b¯)¯ = (b¯)¯· a¯"  "(a¯·b)¯ = b¯·(a¯)¯"
    using inverse_in_group group_inv_of_two by auto;
  with A1 show  "(a·b¯)¯ = b·a¯"  "(a¯·b)¯ = b¯·a"
    using group_inv_of_inv by auto
qed;

(*text{*What is the inverse of a product of three elements?*}

lemma (in group0) group_inv_of_three: 
  assumes A1: "a∈G"  "b∈G"  "c∈G"
  shows "(a·b·c)¯ = c¯·b¯·a¯"
proof -
  from A1 have T: "a·b ∈ G"  "a¯ ∈ G"  "b¯ ∈ G"  "c¯ ∈ G"
    using group_op_closed inverse_in_group by auto;
  with A1 have 
    "(a·b·c)¯ =  c¯·(b¯·a¯)"
    using group_inv_of_two by auto;
  also from T have "… = c¯·b¯·a¯"
    using group_oper_assoc by simp
  finally show "(a·b·c)¯ = c¯·b¯·a¯" by simp;
qed;*)

text{*A couple useful rearrangements with three elements: 
  we can insert a $b\cdot b^{-1}$ 
  between two group elements (another version) and one about a product of 
  an element and inverse of a product, and two others.*}

lemma (in group0) group0_2_L14A:
  assumes A1: "a∈G"  "b∈G"  "c∈G"
  shows 
  "a·c¯= (a·b¯)·(b·c¯)"
  "a¯·c = (a¯·b)·(b¯·c)"
  "a·(b·c)¯ = a·c¯·b¯"
  "a·(b·c¯) = a·b·c¯"
  "(a·b¯·c¯)¯ = c·b·a¯"
  "a·b·c¯·(c·b¯) = a"
  "a·(b·c)·c¯ = a·b"
proof -
  from A1 have T: 
    "a¯ ∈ G"  "b¯∈G"  "c¯∈G"  
    "a¯·b ∈ G"  "a·b¯ ∈ G"  "a·b ∈ G"  
    "c·b¯ ∈ G"  "b·c ∈ G"
    using inverse_in_group group_op_closed
    by auto;
   from A1 T have 
     "a·c¯ =  a·(b¯·b)·c¯"
     "a¯·c =  a¯·(b·b¯)·c"
    using group0_2_L2 group0_2_L6 by auto;
   with A1 T show 
     "a·c¯= (a·b¯)·(b·c¯)"
     "a¯·c = (a¯·b)·(b¯·c)"
     using group_oper_assoc by auto;
  from A1 have "a·(b·c)¯ = a·(c¯·b¯)"
    using group_inv_of_two by simp;
  with A1 T show "a·(b·c)¯ =a·c¯·b¯" 
    using group_oper_assoc by simp;
  from A1 T show "a·(b·c¯) = a·b·c¯"
    using group_oper_assoc by simp
  from A1 T show  "(a·b¯·c¯)¯ = c·b·a¯"
    using group_inv_of_three  group_inv_of_inv
    by simp;
  from T have "a·b·c¯·(c·b¯) = a·b·(c¯·(c·b¯))"
    using group_oper_assoc by simp;
  also from A1 T have "… =  a·b·b¯"
    using group_oper_assoc group0_2_L6 group0_2_L2
    by simp;
  also from A1 T have "… = a·(b·b¯)"
    using group_oper_assoc by simp;
  also from A1 have "… = a"
    using group0_2_L6 group0_2_L2 by simp;
  finally show "a·b·c¯·(c·b¯) = a" by simp;
  from A1 T have "a·(b·c)·c¯ =  a·(b·(c·c¯))"
    using group_oper_assoc by simp;
  also from A1 T have "… = a·b"
    using  group0_2_L6 group0_2_L2 by simp;
  finally show "a·(b·c)·c¯ = a·b"
    by simp;
qed;
  
text{*Another lemma about rearranging a product.*}

lemma (in group0) group0_2_L15:
  assumes A1: "a∈G" "b∈G" "c∈G" "d∈G"
  shows "(a·b)·(c·d)¯ = a·(b·d¯)·a¯·(a·c¯)"
proof -
  from A1 have T1:
    "d¯∈G"  "c¯∈G" "a·b∈G" "a·(b·d¯)∈G"
    using inverse_in_group group_op_closed
    by auto;
  with A1 have "(a·b)·(c·d)¯ = (a·b)·(d¯·c¯)"
    using group_inv_of_two by simp;
  also from A1 T1 have "… = a·(b·d¯)·c¯"
    using group_oper_assoc by simp;
  also from A1 T1 have "… = a·(b·d¯)·a¯·(a·c¯)"
    using group0_2_L14A by blast;
  finally show ?thesis by simp;
qed;

text{*We can cancel an element with its inverse that is written next to it.*}

lemma (in group0) group0_2_L16:
  assumes A1: "a∈G"  "b∈G"
  shows 
  "a·b¯·b = a"  
  "a·b·b¯ = a"
  "a¯·(a·b) = b"
  "a·(a¯·b) = b"
proof -
  from A1 have 
    "a·b¯·b = a·(b¯·b)"   "a·b·b¯ = a·(b·b¯)"
    "a¯·(a·b) = a¯·a·b"   "a·(a¯·b) = a·a¯·b"
    using inverse_in_group group_oper_assoc by auto;
  with A1 show
    "a·b¯·b = a"
    "a·b·b¯ = a"
    "a¯·(a·b) = b"
    "a·(a¯·b) = b"
    using group0_2_L6 group0_2_L2 by auto;
qed;

text{*Another lemma about cancelling with two group elements.*}

lemma (in group0) group0_2_L16A:
  assumes A1: "a∈G"  "b∈G"
  shows "a·(b·a)¯ = b¯"
proof -
  from A1 have "(b·a)¯ = a¯·b¯"  "b¯ ∈ G"
    using group_inv_of_two inverse_in_group by auto;
  with A1 show "a·(b·a)¯ = b¯" using group0_2_L16
    by simp;
qed;

text{*A hard to clasify fact: adding a neutral element to a set that is 
  closed under the group operation results in a set that is closed under the 
  group operation.*}

lemma (in group0) group0_2_L17: 
  assumes A1: "H⊆G"
  and A2: "H {is closed under} f"
  shows "(H ∪ {\<one>}) {is closed under} f"
proof -;
  { fix a b assume A3: "a ∈ H ∪ {\<one>}"  "b ∈ H ∪ {\<one>}"
    have "a·b ∈ H ∪ {\<one>}"
    proof (cases "a∈H")
      assume A4: "a∈H" show "a·b ∈ H ∪ {\<one>}"
      proof (cases "b∈H")
        assume "b∈H"
        with A2 A4 show "a·b ∈ H ∪ {\<one>}" using IsOpClosed_def
          by simp;
      next assume "b∉H" 
        with A1 A3 A4 show "a·b ∈ H ∪ {\<one>}"
          using group0_2_L2 by auto;
      qed;
    next assume "a∉H"
      with A1 A3 show "a·b ∈ H ∪ {\<one>}"
        using group0_2_L2 by auto;
    qed
  } then show "(H ∪ {\<one>}) {is closed under} f"
    using IsOpClosed_def by auto;
qed;

text{*We can put an element on the other side of an equation.*}

lemma (in group0) group0_2_L18:
  assumes A1: "a∈G"  "b∈G"  "c∈G"
  and A2: "c = a·b"
  shows "c·b¯ = a"  "a¯·c = b" 
proof-;
  from A2 A1 have "c·b¯ =  a·(b·b¯)"  "a¯·c = (a¯·a)·b"
    using inverse_in_group group_oper_assoc by auto;
  moreover from A1 have "a·(b·b¯) = a"  "(a¯·a)·b = b"
    using group0_2_L6 group0_2_L2 by auto;
  ultimately show "c·b¯ = a"  "a¯·c = b" 
    by auto;
qed;

text{*Multiplying different group elements by the same factor results
  in different group elements.*}

lemma (in group0) group0_2_L19: 
  assumes A1: "a∈G"  "b∈G"  "c∈G" and A2: "a≠b"
  shows 
  "a·c ≠ b·c"
  "c·a ≠ c·b"
proof -
  { assume "a·c = b·c ∨ c·a =c·b"
    then have "a·c·c¯ = b·c·c¯ ∨ c¯·(c·a) = c¯·(c·b)"
      by auto;
    with A1 A2 have False using group0_2_L16 by simp;
  } then show "a·c ≠ b·c" and "c·a ≠ c·b" by auto;
qed;

section{*Subgroups*}

text{*There are two common ways to define subgroups. One requires that the
  group operations are closed in the subgroup. The second one defines subgroup 
  as a subset of a group which is itself a group under the group operations.
  We use the second approach because it results in shorter definition. 
  We do not 
  require $H$ to be a subset of $G$ as this can be inferred from our 
  definition.
  The rest of this section is devoted to proving the equivalence of these two
  definitions of the notion of a subgroup. 
  *}

constdefs 
  "IsAsubgroup(H,f) ≡ IsAgroup(H, restrict(f,H×H))"

text{*Formally the group operation in a subgroup is different than in the
  group as they have different domains. Of course we want to use the original 
  operation with the associated notation in the subgroup. The next couple of 
  lemmas will allow for that.*}

text{*The neutral element of the subgroup is in the subgroup and it is 
both right and left neutral there. The notation is very ugly because
we don't want to introduce a separate notation for the subgroup operation.
*}

lemma group0_3_L1: 
  assumes A1:"IsAsubgroup(H,f)"
  and A2: "n = TheNeutralElement(H,restrict(f,H×H))"
  shows "n ∈ H"
  "∀h∈H. restrict(f,H×H)`<n,h > = h"
  "∀h∈H. restrict(f,H×H)`<h,n > = h"
proof -;
  let ?b = "restrict(f,H×H)"
  let ?e = "TheNeutralElement(H,restrict(f,H×H))"
  from A1 have "group0(H,?b)"
    using IsAsubgroup_def group0_def by simp;
  then have T1:
    "?e ∈ H ∧ (∀h∈H. (?b`<?e,h > = h ∧ ?b`<h,?e > = h))"
    by (rule group0.group0_2_L2);
  with A2 show "n ∈ H" by simp;
  from T1 A2 show "∀h∈H. ?b`<n,h > = h" "∀h∈H. ?b`<h,n> = h"
    by auto;
qed;

text{*Subgroup is contained in the group.*}

lemma (in group0) group0_3_L2: 
  assumes A1:"IsAsubgroup(H,f)"
  shows "H⊆G"
proof;
  fix h assume A2:"h∈H";
  let ?b = "restrict(f,H×H)"
  let ?n = "TheNeutralElement(H,restrict(f,H×H))"
   from A1 have "?b ∈ H×H->H" 
    using IsAsubgroup_def IsAgroup_def 
      IsAmonoid_def IsAssociative_def by simp;
  moreover from A2 A1 have "<?n,h> ∈ H×H" 
    using group0_3_L1 by simp;
  moreover from A1 A2 have "h = ?b`<?n,h >" 
    using group0_3_L1 by simp;
  ultimately have "⟨<?n,h>,h⟩ ∈ ?b" 
    using func1_1_L5A by blast;
  then have "⟨<?n,h>,h⟩ ∈ f" using restrict_subset by auto
  moreover from groupAssum have "f:G×G->G"
    using IsAgroup_def IsAmonoid_def IsAssociative_def 
    by simp;
  ultimately show "h∈G" using func1_1_L5 
    by blast;
qed;

text{*The group neutral element (denoted $1$ in the group0 context)
is a neutral element for the subgroup with respect to the froup action.*}

lemma (in group0) group0_3_L3:
  assumes A1:"IsAsubgroup(H,f)"
  shows "∀h∈H. \<one>·h = h ∧ h·\<one> = h"
proof;
  fix h assume "h∈H" 
  with groupAssum A1 show "\<one>·h = h ∧ h·\<one> = h"
    using group0_3_L2 group0_2_L2 by auto;
qed;

text{*The neutral element of a subgroup is the same as that of the group.*}

lemma (in group0) group0_3_L4: assumes A1:"IsAsubgroup(H,f)"
  shows "TheNeutralElement(H,restrict(f,H×H)) = \<one>"
proof -;
  let ?n =  "TheNeutralElement(H,restrict(f,H×H))"
  from A1 have T1:"?n ∈ H" using group0_3_L1 by simp;
  with groupAssum A1 have "?n∈G" using  group0_3_L2 by auto;
  with A1 T1 show ?thesis using 
     group0_3_L1 restrict_if group0_2_L7 by simp;
qed;

text{*The neutral element of the group (denoted $1$ in the group0 context)
belongs to every subgroup.*}

lemma (in group0) group0_3_L5: assumes A1: "IsAsubgroup(H,f)"
  shows "\<one>∈H"
proof -;
  from A1 show "\<one>∈H" using group0_3_L1 group0_3_L4 
    by fast;
qed;

text{*Subgroups are closed with respect to the group operation.*}

lemma (in group0) group0_3_L6: assumes A1:"IsAsubgroup(H,f)"
  and A2:"a∈H" "b∈H"
  shows "a·b ∈ H"
proof -; 
  let ?b = "restrict(f,H×H)"
  from A1 have "monoid0(H,?b)" using
    IsAsubgroup_def IsAgroup_def monoid0_def by simp;
  with A2 have "?b` (<a,b>) ∈ H" using monoid0.group0_1_L1
    by blast;
 with A2 show "a·b ∈ H" using restrict_if by simp;
qed;

text{*A preliminary lemma that we need to  show that taking the inverse 
  in the subgroup is the same as taking the inverse
  in the group.*}

lemma group0_3_L7A: 
  assumes A1:"IsAgroup(G,f)" 
  and A2:"IsAsubgroup(H,f)" and A3:"g=restrict(f,H×H)"
  shows "GroupInv(G,f) ∩ H×H = GroupInv(H,g)"
proof -
  def D1: e ≡ "TheNeutralElement(G,f)"
  def D2: e1 ≡ "TheNeutralElement(H,g)"
  from A1 have T1:"group0(G,f)" using group0_def by simp;
  from A2 A3 have T2:"group0(H,g)" 
    using IsAsubgroup_def group0_def by simp 
  from T1 A2 A3 D1 D2 have "e1 = e" 
    using group0.group0_3_L4 by simp;
  with T1 D1 have "GroupInv(G,f) = f-``{e1}" 
    using group0.group0_2_T3 by simp;
  moreover have "g-``{e1} = f-``{e1} ∩ H×H"
  proof -;
    from A1 have "f ∈ G×G->G" 
      using IsAgroup_def IsAmonoid_def IsAssociative_def 
      by simp;
    moreover from T1 A2 have "H×H ⊆ G×G" 
      using group0.group0_3_L2 by auto;
    ultimately show "g-``{e1} = f-``{e1} ∩ H×H" 
      using A3 func1_2_L1 by simp;
  qed;
  moreover from T2 A3 D2 have "GroupInv(H,g) = g-``{e1}" 
    using group0.group0_2_T3 by simp;
  ultimately show ?thesis by simp;
qed;

text{*Using the lemma above we can show the actual statement: 
  taking the inverse in the subgroup is the same as taking the inverse
  in the group.*}

theorem (in group0) group0_3_T1:
  assumes A1: "IsAsubgroup(H,f)" 
  and A2:"g=restrict(f,H×H)"
  shows "GroupInv(H,g) = restrict(GroupInv(G,f),H)"
proof -;
  from groupAssum have "GroupInv(G,f) : G->G" 
    using group0_2_T2 by simp;
  moreover from A1 A2 have "GroupInv(H,g) : H->H"
    using IsAsubgroup_def group0_2_T2 by simp;
  moreover from A1 have "H⊆G" 
    using group0_3_L2 by simp;
  moreover from groupAssum A1 A2 have 
    "GroupInv(G,f) ∩ H×H = GroupInv(H,g)"
    using group0_3_L7A by simp;
  ultimately show ?thesis
    using func1_2_L3 by simp;
qed;

text{*A sligtly weaker, but more convenient in applications,
  reformulation of the above theorem.*}

theorem (in group0) group0_3_T2: 
  assumes "IsAsubgroup(H,f)" 
  and "g=restrict(f,H×H)"
  shows "∀h∈H. GroupInv(H,g)`(h) = h¯"
  using prems group0_3_T1 restrict_if by simp;

text{*Subgroups are closed with respect to taking the group inverse.
  Again, I was unable to apply @{text "inverse_in_group"} directly to the group 
  $H$. This problem is worked around by repeating the (short) proof of 
  @{text "inverse_in_group"} in the proof below.*}

theorem (in group0) group0_3_T3A: 
  assumes A1:"IsAsubgroup(H,f)" and A2:"h∈H"
  shows "h¯∈ H"
proof -
  def D1: g ≡ "restrict(f,H×H)";
  with A1 have  "GroupInv(H,g) ∈ H->H"
    using IsAsubgroup_def group0_2_T2 by simp;
  with A2 have "GroupInv(H,g)`(h) ∈ H"
    using apply_type by simp;
  with A1 D1 A2 show "h¯∈ H" using group0_3_T2 by simp;
qed;

text{*The next theorem states that a nonempty subset of 
of a group $G$ that is closed under the group operation and 
taking the inverse is a subgroup of the group.*}

theorem (in group0) group0_3_T3:
  assumes A1: "H≠0"
  and A2: "H⊆G"
  and A3: "H {is closed under} f"
  and A4: "∀x∈H. x¯ ∈ H"
  shows "IsAsubgroup(H,f)"
proof -;
  let ?g = "restrict(f,H×H)"
  let ?n = "TheNeutralElement(H,?g)"
  from A3 have T0:"∀x∈H.∀y∈H. x·y ∈ H"
    using IsOpClosed_def by simp;
  from A1 obtain x where "x∈H" by auto;
  with A4 T0 A2 have T1:"\<one>∈H"
    using group0_2_L6 by blast;
  with A3 A2 have T2:"IsAmonoid(H,?g)"
    using group0_2_L1 monoid0.group0_1_T1
    by simp;
  moreover have "∀h∈H.∃b∈H. ?g`<h,b> = ?n"
  proof;
    fix h assume A5:"h∈H"
    with A4 A2 have "h·h¯ = \<one>"
      using group0_2_L6 by auto;
    moreover from groupAssum A3 A2 T1 have "\<one> = ?n"
      using IsAgroup_def group0_1_L6 by auto;
    moreover from A5 A4 have "?g`<h,h¯> = h·h¯"
      using restrict_if by simp;
    ultimately have "?g`<h,h¯> = ?n" by simp;
    with A5 A4 show "∃b∈H. ?g`<h,b> = ?n" by auto;
  qed;
  ultimately show "IsAsubgroup(H,f)" using 
    IsAsubgroup_def IsAgroup_def by simp;
qed;

text{*Intersection of subgroups is a subgroup of each factor.*}

lemma group0_3_L7:
  assumes A1:"IsAgroup(G,f)"
  and A2:"IsAsubgroup(H1,f)"
  and A3:"IsAsubgroup(H2,f)"
  shows "IsAsubgroup(H1∩H2,restrict(f,H1×H1))"
proof -;
  let ?e = "TheNeutralElement(G,f)"
  let ?g = "restrict(f,H1×H1)"
  from A1 have T1: "group0(G,f)"
    using group0_def by simp;
  from A2 have "group0(H1,?g)"
    using IsAsubgroup_def group0_def by simp;
  moreover have "H1∩H2 ≠ 0"
  proof -
    from A1 A2 A3 have "?e ∈ H1∩H2"
      using group0_def group0.group0_3_L5 by simp;
    thus ?thesis by auto;
  qed;
  moreover have T2:"H1∩H2 ⊆ H1" by auto;
  moreover from T1 T2 A2 A3 have 
    "H1∩H2 {is closed under} ?g"
    using group0.group0_3_L6 IsOpClosed_def 
      func_ZF_4_L7 func_ZF_4_L5 by simp;
  moreover from T1 A2 A3 have 
    "∀x ∈ H1∩H2. GroupInv(H1,?g)`(x) ∈ H1∩H2"
    using group0.group0_3_T2 group0.group0_3_T3A
    by simp;
  ultimately show ?thesis
    using group0.group0_3_T3 by simp;
qed;

section{*Abelian groups*}

text{*Here we will prove some facts specific to abelian groups. *}

text{*Proving the facts about associative and commutative operations is 
  quite tedious in formalized mathematics. To a human the thing is simple:
  we can arrange the elements in any order and put parantheses wherever we 
  want, it is all the same. However, formalizing this statement would be 
  rather difficult (I think). The next lemma attempts a quasi-algorithmic
  approach to this type of problem. To prove that two expressions are equal, 
  we first strip one from parantheses, then rearrange the elements in proper 
  order, then put the parantheses where we want them to be. The algorithm for 
  rearrangement is easy to describe: we keep putting the first element 
  (from the right) that is in the wrong place at the left-most position
  until we get the proper arrangement. For the parantheses simp does it 
  very well.*}

lemma (in group0) group0_4_L2:
  assumes A1:"f {is commutative on} G"
  and A2:"a∈G" "b∈G" "c∈G" "d∈G" "E∈G" "F∈G"
  shows "(a·b)·(c·d)·(E·F) = (a·(d·F))·(b·(c·E))"
proof -;
  from A2 have "(a·b)·(c·d)·(E·F) = a·b·c·d·E·F"
    using group_op_closed group_oper_assoc
    by simp;
  also have  "a·b·c·d·E·F = a·d·F·b·c·E"
  proof -
    from A1 A2 have "a·b·c·d·E·F = F·(a·b·c·d·E)"
      using IsCommutative_def group_op_closed 
      by simp;
    also from A2 have "F·(a·b·c·d·E) = F·a·b·c·d·E"
      using group_op_closed group_oper_assoc
      by simp;
    also from A1 A2 have "F·a·b·c·d·E = d·(F·a·b·c)·E"
      using IsCommutative_def group_op_closed
      by simp;
    also from A2 have "d·(F·a·b·c)·E = d·F·a·b·c·E"
      using group_op_closed group_oper_assoc
      by simp;
    also from A1 A2 have " d·F·a·b·c·E = a·(d·F)·b·c·E"
      using IsCommutative_def group_op_closed
      by simp;
    also from A2 have "a·(d·F)·b·c·E = a·d·F·b·c·E" 
      using group_op_closed group_oper_assoc
      by simp;
    finally show ?thesis by simp;
  qed;
  also from A2 have "a·d·F·b·c·E = (a·(d·F))·(b·(c·E))"
    using group_op_closed group_oper_assoc
    by simp;
  finally show ?thesis by simp;
qed;
  
text{*Another useful rearrangement.*}

lemma (in group0) group0_4_L3:
  assumes A1:"f {is commutative on} G" 
  and A2: "a∈G"  "b∈G" and A3: "c∈G"  "d∈G"  "E∈G"  "F∈G"
  shows "a·b·((c·d)¯·(E·F)¯) = (a·(E·c)¯)·(b·(F·d)¯)"
proof -;
  from A3 have T1:
    "c¯∈G" "d¯∈G" "E¯∈G" "F¯∈G" "(c·d)¯∈G" "(E·F)¯∈G"
    using inverse_in_group group_op_closed 
    by auto;
  from A2 T1 have 
    "a·b·((c·d)¯·(E·F)¯) = a·b·(c·d)¯·(E·F)¯"
    using group_op_closed group_oper_assoc
    by simp;
  also from A2 A3 have 
    "a·b·(c·d)¯·(E·F)¯ = (a·b)·(d¯·c¯)·(F¯·E¯)"
    using group_inv_of_two by simp;
   also from A1 A2 T1 have 
    "(a·b)·(d¯·c¯)·(F¯·E¯) = (a·(c¯·E¯))·(b·(d¯·F¯))"
    using group0_4_L2 by simp;
  also from A2 A3 have 
    "(a·(c¯·E¯))·(b·(d¯·F¯)) = (a·(E·c)¯)·(b·(F·d)¯)"
    using group_inv_of_two by simp;
  finally show ?thesis by simp;
qed;

text{*Some useful rearrangements for two elements of a group.*}

lemma (in group0) group0_4_L4:
  assumes A1:"f {is commutative on} G"
  and A2: "a∈G" "b∈G"
  shows 
  "b¯·a¯ = a¯·b¯" 
  "(a·b)¯ = a¯·b¯" 
  "(a·b¯)¯ = a¯·b"
proof -;
  from A2 have T1: "b¯∈G" "a¯∈G" using inverse_in_group by auto;
  with A1 show "b¯·a¯ = a¯·b¯" using IsCommutative_def by simp;
  with A2 show "(a·b)¯ = a¯·b¯" using group_inv_of_two by simp;
  from A2 T1 have "(a·b¯)¯ = (b¯)¯·a¯" using group_inv_of_two by simp;
  with A1 A2 T1 show "(a·b¯)¯ = a¯·b" 
    using group_inv_of_inv IsCommutative_def by simp;
qed;
 
text{*Another bunch of useful rearrangements with three elements.*}

lemma (in group0) group0_4_L4A: 
  assumes A1:"f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"
  shows 
  "a·b·c = c·a·b" 
  "a¯·(b¯·c¯)¯ = (a·(b·c)¯)¯" 
  "a·(b·c)¯ = a·b¯·c¯" 
  "a·(b·c¯)¯ = a·b¯·c" 
  "a·b¯·c¯ = a·c¯·b¯"
proof -
  from A1 A2 have "a·b·c = c·(a·b)"
    using IsCommutative_def group_op_closed
    by simp;
  with A2 show "a·b·c = c·a·b" using
     group_op_closed group_oper_assoc
    by simp
  from A2 have T: 
    "b¯∈G"  "c¯∈G"  "b¯·c¯ ∈ G"  "a·b ∈ G"
    using inverse_in_group group_op_closed
    by auto;
  with A1 A2 show "a¯·(b¯·c¯)¯ = (a·(b·c)¯)¯"
    using group_inv_of_two IsCommutative_def 
    by simp;
  from A1 A2 T have "a·(b·c)¯ = a·(b¯·c¯)"
    using group_inv_of_two IsCommutative_def by simp;
  with A2 T show "a·(b·c)¯ = a·b¯·c¯"
    using group_oper_assoc by simp;
  from A1 A2 T have "a·(b·c¯)¯ = a·(b¯·(c¯)¯)"
    using group_inv_of_two IsCommutative_def by simp;
  with A2 T show "a·(b·c¯)¯ = a·b¯·c"
    using group_oper_assoc group_inv_of_inv by simp;
  from A1 A2 T have "a·b¯·c¯ = a·(c¯·b¯)"
    using group_oper_assoc IsCommutative_def by simp;
  with A2 T show "a·b¯·c¯ = a·c¯·b¯"
    using group_oper_assoc by simp
qed;

text{*Another useful rearrangement.*}

lemma (in group0) group0_4_L4B: 
  assumes "f {is commutative on} G"
  and "a∈G"  "b∈G"  "c∈G"
  shows "a·b¯·(b·c¯) = a·c¯"  
  using prems inverse_in_group group_op_closed 
    group0_4_L4 group_oper_assoc group0_2_L16 by simp;

text{*A couple of permutations of order for three alements.*}

lemma (in group0) group0_4_L4C: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G" "b∈G" "c∈G"
  shows
  "a·b·c = c·a·b"
  "a·b·c = a·(c·b)"
  "a·b·c = c·(a·b)"
  "a·b·c = c·b·a"
proof -
  from A1 A2 show I: "a·b·c = c·a·b"
    using group0_4_L4A by simp
  also from A1 A2 have "c·a·b = a·c·b"
    using IsCommutative_def by simp;
  also from A2 have "a·c·b = a·(c·b)"
    using group_oper_assoc by simp;
  finally show "a·b·c = a·(c·b)" by simp;
  from A2 I show "a·b·c = c·(a·b)"
    using group_oper_assoc by simp;
  also from A1 A2 have "c·(a·b) = c·(b·a)"
    using IsCommutative_def by simp;
  also from A2 have "c·(b·a) = c·b·a"
    using group_oper_assoc by simp;
  finally show "a·b·c = c·b·a" by simp;
qed;

text{*Some rearangement with three elements and inverse.*}

lemma (in group0) group0_4_L4D:
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"
  shows 
  "a¯·b¯·c = c·a¯·b¯"
  "b¯·a¯·c = c·a¯·b¯"
  "(a¯·b·c)¯ = a·b¯·c¯"
proof -
  from A2 have T: 
    "a¯ ∈ G"  "b¯ ∈ G"  "c¯∈G"
    using inverse_in_group by auto;
  with A1 A2 show 
    "a¯·b¯·c = c·a¯·b¯"
    "b¯·a¯·c = c·a¯·b¯"
    using  group0_4_L4A by auto
  from A1 A2 T show "(a¯·b·c)¯ = a·b¯·c¯"
    using group_inv_of_three group_inv_of_inv group0_4_L4C
    by simp;
qed;

text{*Another rearrangement lemma with three elements and equation.*}

lemma (in group0) group0_4_L5: assumes A1:"f {is commutative on} G" 
  and A2: "a∈G"  "b∈G"  "c∈G"
  and A3: "c = a·b¯"
  shows "a = b·c"
proof -; 
  from A2 A3 have "c·(b¯)¯ = a"
    using inverse_in_group group0_2_L18
    by simp;
  with A1 A2 show ?thesis using 
     group_inv_of_inv IsCommutative_def by simp;
qed;

text{*In abelian groups we can cancel an element with its inverse
  even if separated by another element.*}

lemma (in group0) group0_4_L6A: assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"
  shows 
  "a·b·a¯ = b"
  "a¯·b·a = b"
  "a¯·(b·a) = b"
  "a·(b·a¯) = b"
proof -;
  from A1 A2 have 
    "a·b·a¯ = a¯·a·b"
    using inverse_in_group group0_4_L4A by blast
  also from A2 have "… = b"
    using group0_2_L6 group0_2_L2 by simp;
  finally show "a·b·a¯ = b" by simp;
  from A1 A2 have 
    "a¯·b·a = a·a¯·b"
    using inverse_in_group group0_4_L4A by blast;
  also from A2 have "… = b"
    using group0_2_L6 group0_2_L2 by simp;
  finally show "a¯·b·a = b" by simp
  moreover from A2 have "a¯·b·a = a¯·(b·a)"
    using inverse_in_group group_oper_assoc by simp;
  ultimately show "a¯·(b·a) = b" by simp;
  from A1 A2 show "a·(b·a¯) = b"
     using inverse_in_group IsCommutative_def group0_2_L16
     by simp;
qed;

text{*Another lemma about cancelling with two elements.*}

lemma (in group0) group0_4_L6AA: 
  assumes A1: "f {is commutative on} G" and A2: "a∈G"  "b∈G"
  shows 
  "a·b¯·a¯ = b¯"
  using prems inverse_in_group group0_4_L6A
  by auto;

text{*Another lemma about cancelling with two elements.*}

lemma (in group0) group0_4_L6AB: 
  assumes A1: "f {is commutative on} G" and A2: "a∈G"  "b∈G"
  shows 
  "a·(a·b)¯ = b¯"
  "a·(b·a¯) = b"
proof -
    from A2 have "a·(a·b)¯ = a·(b¯·a¯)"
      using group_inv_of_two by simp
    also from A2 have "… = a·b¯·a¯"
      using inverse_in_group group_oper_assoc by simp;
    also from A1 A2 have "… =  b¯"
      using group0_4_L6AA by simp;
    finally show "a·(a·b)¯ = b¯" by simp;
    from A1 A2 have "a·(b·a¯) = a·(a¯·b)"
      using inverse_in_group IsCommutative_def by simp;
    also from A2 have "… = b"
      using inverse_in_group group_oper_assoc group0_2_L6 group0_2_L2
      by simp;
    finally show "a·(b·a¯) = b" by simp;
qed;

text{*Another lemma about cancelling with two elements.*}

lemma (in group0) group0_4_L6AC: 
  assumes "f {is commutative on} G" and "a∈G"  "b∈G"
  shows "a·(a·b¯)¯ = b"
  using prems inverse_in_group group0_4_L6AB group_inv_of_inv
  by simp;


text{*In abelian groups we can cancel an element with its inverse
  even if separated by two other elements.*}

lemma (in group0) group0_4_L6B: assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G" 
  shows 
  "a·b·c·a¯ = b·c"
  "a¯·b·c·a = b·c"
proof -
   from A2 have 
     "a·b·c·a¯ = a·(b·c)·a¯"
     "a¯·b·c·a = a¯·(b·c)·a"
    using group_op_closed group_oper_assoc inverse_in_group
    by auto;
  with A1 A2 show
    "a·b·c·a¯ = b·c"
    "a¯·b·c·a = b·c"
    using group_op_closed group0_4_L6A
    by auto;
qed;

text{*In abelian groups we can cancel an element with its inverse
  even if separated by three other elements.*}

lemma (in group0) group0_4_L6C: assumes A1: "f {is commutative on} G"
  and A2: "a∈G" "b∈G" "c∈G" "d∈G"
  shows "a·b·c·d·a¯ = b·c·d" 
proof -
  from A2 have "a·b·c·d·a¯ = a·(b·c·d)·a¯"
    using group_op_closed group_oper_assoc
    by simp;
  with A1 A2 show ?thesis 
    using group_op_closed group0_4_L6A 
    by simp;
qed;

text{*Another couple of useful rearrangements of three elements
  and cancelling.*}

lemma (in group0) group0_4_L6D: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"
  shows 
  "a·b¯·(a·c¯)¯ = c·b¯"
  "(a·c)¯·(b·c) = a¯·b"
  "a·(b·(c·a¯·b¯)) = c"
  "a·b·c¯·(c·a¯) = b"
proof -
  from A2 have T: 
    "a¯ ∈ G"  "b¯ ∈ G"  "c¯ ∈ G" 
    "a·b ∈ G"  "a·b¯ ∈ G"  "c¯·a¯ ∈ G"  "c·a¯ ∈ G"
    using inverse_in_group group_op_closed by auto;
  with A1 A2 show "a·b¯·(a·c¯)¯ = c·b¯"
    using group0_2_L12 group_oper_assoc group0_4_L6B
    IsCommutative_def by simp;
  from A2 T have "(a·c)¯·(b·c) = c¯·a¯·b·c"
    using group_inv_of_two group_oper_assoc by simp;
  also from A1 A2 T have "… = a¯·b"
    using group0_4_L6B by simp;
  finally show "(a·c)¯·(b·c) = a¯·b"
    by simp;
  from A1 A2 T show "a·(b·(c·a¯·b¯)) = c"
    using group_oper_assoc group0_4_L6B group0_4_L6A
    by simp;
  from T have "a·b·c¯·(c·a¯) = a·b·(c¯·(c·a¯))"
    using group_oper_assoc by simp;
  also from A1 A2 T have "… = b"
    using group_oper_assoc group0_2_L6 group0_2_L2 group0_4_L6A
    by simp;
  finally show "a·b·c¯·(c·a¯) = b" by simp;
qed;

text{*Another useful rearrangement of three elements
  and cancelling.*}

lemma (in group0) group0_4_L6E: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"
  shows 
  "a·b·(a·c)¯ = b·c¯"
proof -
  from A2 have T: "b¯ ∈ G"  "c¯ ∈ G"
    using inverse_in_group by auto;
  with A1 A2 have
    "a·(b¯)¯·(a·(c¯)¯)¯ = c¯·(b¯)¯"
    using group0_4_L6D by simp;
  with A1 A2 T show "a·b·(a·c)¯ = b·c¯"
    using group_inv_of_inv IsCommutative_def
    by simp;
qed;

text{*A rearrangement with two elements and canceelling,
  special case of @{text "group0_4_L6D"} when $c=b^{-1}$.*}

lemma (in group0) group0_4_L6F: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"
  shows "a·b¯·(a·b)¯ = b¯·b¯"
proof -
  from A2 have "b¯ ∈ G" 
    using inverse_in_group by simp
  with A1 A2 have "a·b¯·(a·(b¯)¯)¯ = b¯·b¯"
    using group0_4_L6D by simp;
  with A2 show "a·b¯·(a·b)¯ = b¯·b¯"
    using group_inv_of_inv by simp;
qed;

text{*Some other rearrangements with four elements.
  The algorithm for proof as in @{text "group0_4_L2"}
  works very well here.*}

lemma (in group0) rearr_ab_gr_4_elemA:
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows 
  "a·b·c·d = a·d·b·c"
  "a·b·c·d = a·c·(b·d)"
proof -
  from A1 A2 have "a·b·c·d = d·(a·b·c)"
    using  IsCommutative_def group_op_closed
    by simp;
  also from A2 have "… = d·a·b·c"
    using group_op_closed group_oper_assoc
    by simp;
  also from A1 A2 have "… = a·d·b·c"
    using IsCommutative_def group_op_closed
    by simp;
  finally show "a·b·c·d = a·d·b·c"
    by simp;
  from A1 A2 have "a·b·c·d = c·(a·b)·d"
    using IsCommutative_def group_op_closed
    by simp
  also from A2 have "… = c·a·b·d"
    using group_op_closed group_oper_assoc
    by simp
  also from A1 A2 have "… = a·c·b·d"
    using IsCommutative_def group_op_closed
    by simp
  also from A2 have "… = a·c·(b·d)"
    using group_op_closed group_oper_assoc
    by simp
  finally show "a·b·c·d = a·c·(b·d)"
    by simp
qed;

text{*Some rearrangements with four elements and inverse
  that are applications of @{text "rearr_ab_gr_4_elem"} 
  *}

lemma (in group0) rearr_ab_gr_4_elemB:
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows 
  "a·b¯·c¯·d¯ = a·d¯·b¯·c¯"
  "a·b·c·d¯ = a·d¯·b·c"
  "a·b·c¯·d¯ =  a·c¯·(b·d¯)"
proof -
  from A2 have T: "b¯ ∈ G"  "c¯ ∈ G"  "d¯ ∈ G"
    using inverse_in_group by auto;
  with A1 A2 show 
    "a·b¯·c¯·d¯ = a·d¯·b¯·c¯"
    "a·b·c·d¯ = a·d¯·b·c"
    "a·b·c¯·d¯ =  a·c¯·(b·d¯)"
    using rearr_ab_gr_4_elemA by auto;
qed;
  
text{*Some rearrangement lemmas with four elements.*}
 
lemma (in group0) group0_4_L7: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows 
  "a·b·c·d¯ = a·d¯· b·c" 
  "a·d·(b·d·(c·d))¯ = a·(b·c)¯·d¯"
  "a·(b·c)·d = a·b·d·c"
proof -
  from A2 have T:
    "b·c ∈ G" "d¯ ∈ G" "b¯∈G" "c¯∈G" 
    "d¯·b ∈ G" "c¯·d ∈ G" "(b·c)¯ ∈ G"
    "b·d ∈ G"  "b·d·c ∈ G"  "(b·d·c)¯ ∈ G"
    "a·d ∈ G"  "b·c ∈ G"
    using group_op_closed inverse_in_group 
    by auto;
  with A1 A2 have "a·b·c·d¯ = a·(d¯·b·c)"
    using group_oper_assoc group0_4_L4A by simp;
  also from A2 T have "a·(d¯·b·c) = a·d¯·b·c"
    using group_oper_assoc by simp; 
  finally show "a·b·c·d¯ = a·d¯· b·c" by simp;
  from A2 T have "a·d·(b·d·(c·d))¯ = a·d·(d¯·(b·d·c)¯)"
    using group_oper_assoc group_inv_of_two by simp;
  also from A2 T have "… = a·(b·d·c)¯"
    using group_oper_assoc group0_2_L16 by simp;
  also from A1 A2 have "… =  a·(d·(b·c))¯"
    using IsCommutative_def group_oper_assoc by simp;
  also from A2 T have "… = a·((b·c)¯·d¯)"
    using group_inv_of_two by simp;
  also from A2 T have "… =  a·(b·c)¯·d¯"
    using group_oper_assoc by simp;
  finally show "a·d·(b·d·(c·d))¯ = a·(b·c)¯·d¯"
    by simp;
  from A2 have "a·(b·c)·d = a·(b·(c·d))"
    using group_op_closed group_oper_assoc by simp;
  also from A1 A2 have "… =  a·(b·(d·c))"
    using IsCommutative_def group_op_closed by simp;
  also from A2 have "… =  a·b·d·c"
    using group_op_closed group_oper_assoc by simp;
  finally show "a·(b·c)·d = a·b·d·c" by simp;
qed;

text{*Some other rearrangements with four elements.*}

lemma (in group0) group0_4_L8: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows 
  "a·(b·c)¯ = (a·d¯·c¯)·(d·b¯)"
  "a·b·(c·d) = c·a·(b·d)"
  "a·b·(c·d) = a·c·(b·d)"
  "a·(b·c¯)·d = a·b·d·c¯"
  "(a·b)·(c·d)¯·(b·d¯)¯ = a·c¯"
proof -
  from A2 have T:
    "b·c ∈ G" "a·b ∈ G" "d¯ ∈ G" "b¯∈G" "c¯∈G" 
    "d¯·b ∈ G" "c¯·d ∈ G" "(b·c)¯ ∈ G"
    "a·b ∈ G"  "(c·d)¯ ∈ G"  "(b·d¯)¯ ∈ G"  "d·b¯ ∈ G"
    using group_op_closed inverse_in_group 
    by auto;
  from A2 have "a·(b·c)¯ = a·c¯·b¯" using group0_2_L14A by blast;
  moreover from A2 have "a·c¯ = (a·d¯)·(d·c¯)" using group0_2_L14A
    by blast;
  ultimately have "a·(b·c)¯ = (a·d¯)·(d·c¯)·b¯" by simp;
  with A1 A2 T have "a·(b·c)¯= a·d¯·(c¯·d)·b¯"
    using IsCommutative_def by simp;
  with A2 T show "a·(b·c)¯ = (a·d¯·c¯)·(d·b¯)"
    using group_op_closed group_oper_assoc by simp;
  from A2 T have "a·b·(c·d) = a·b·c·d"
    using group_oper_assoc by simp;
  also have "a·b·c·d = c·a·b·d"
  proof -;
    from A1 A2 have "a·b·c·d = c·(a·b)·d"
      using IsCommutative_def group_op_closed
      by simp;
    also from A2 have "… = c·a·b·d"
      using group_op_closed group_oper_assoc
      by simp;
    finally show ?thesis by simp;
  qed;
  also from A2 have "c·a·b·d =  c·a·(b·d)"
    using group_op_closed group_oper_assoc
    by simp;
  finally show "a·b·(c·d) = c·a·(b·d)" by simp;
  with A1 A2 show "a·b·(c·d) = a·c·(b·d)"
    using IsCommutative_def by simp
  from A1 A2 T show "a·(b·c¯)·d = a·b·d·c¯"
    using group0_4_L7 by simp;
  from T have "(a·b)·(c·d)¯·(b·d¯)¯ = (a·b)·((c·d)¯·(b·d¯)¯)"
    using group_oper_assoc by simp;
  also from A1 A2 T have "… = (a·b)·(c¯·d¯·(d·b¯))"
    using group_inv_of_two group0_2_L12 IsCommutative_def
    by simp;
  also from T have "… = (a·b)·(c¯·(d¯·(d·b¯)))"
    using group_oper_assoc by simp;
  also from A1 A2 T have "… = a·c¯"
    using group_oper_assoc group0_2_L6 group0_2_L2 IsCommutative_def
    group0_2_L16 by simp;
  finally show "(a·b)·(c·d)¯·(b·d¯)¯ = a·c¯"
    by simp;
qed;


text{*Some other rearrangements with four elements.*}

lemma (in group0) group0_4_L8A: 
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  shows 
  "a·b¯·(c·d¯) = a·c·(b¯·d¯)"
  "a·b¯·(c·d¯) = a·c·b¯·d¯"
proof -
  from A2 have 
    T: "a∈G"  "b¯ ∈ G"  "c∈G"  "d¯ ∈ G"
    using inverse_in_group by auto
  with A1 show "a·b¯·(c·d¯) = a·c·(b¯·d¯)"
    by (rule group0_4_L8);
  with A2 T show  "a·b¯·(c·d¯) = a·c·b¯·d¯"
    using group_op_closed group_oper_assoc
    by simp;
qed;


text{*Another rearrangement about equation.*}

lemma (in group0) group0_4_L9:
  assumes A1: "f {is commutative on} G"
  and A2: "a∈G"  "b∈G"  "c∈G"  "d∈G"
  and A3: "a = b·c¯·d¯"
  shows 
  "d = b·a¯·c¯"
  "d = a¯·b·c¯"
  "b = a·d·c"
proof -
  from A2 have T: 
    "a¯ ∈ G"  "c¯ ∈ G"  "d¯ ∈ G"  "b·c¯ ∈ G"
    using group_op_closed inverse_in_group 
    by auto
  with A2 A3 have "a·(d¯)¯ =  b·c¯"
    using group0_2_L18 by simp;
  with A2 have "b·c¯ = a·d"
    using group_inv_of_inv by simp;
  with A2 T have I: "a¯·(b·c¯) = d"
    using group0_2_L18 by simp;
  with A1 A2 T show 
    "d = b·a¯·c¯"
    "d = a¯·b·c¯"
    using group_oper_assoc IsCommutative_def by auto;
  from A3 have "a·d·c = (b·c¯·d¯)·d·c" by simp;
  also from A2 T have "… = b·c¯·(d¯·d)·c"
    using group_oper_assoc by simp;
  also from A2 T have "… =  b·c¯·c"
    using group0_2_L6 group0_2_L2 by simp;
  also from A2 T have "… =  b·(c¯·c)"
    using group_oper_assoc by simp;
  also from A2 have "… = b"
    using group0_2_L6 group0_2_L2 by simp
  finally have "a·d·c = b" by simp;
  thus "b = a·d·c" by simp;
qed;

section{*Translations*}

text{*In this section we consider translations. Translations are maps 
  $T: G\rightarrow G$ of the form $T_g (a) = g\cdot a$ or 
  $T_g (a) = a\cdot g$. We also consider two-dimensional translations
  $T_g : G\times G \rightarrow G\times G$, where 
  $T_g(a,b) = (a\cdot g, b\cdot g)$ or$T_g(a,b) = (g\cdot a, g\cdot b)$. 
  *}

constdefs
  "RightTranslation(G,P,g) ≡ {<a,b> ∈ G×G. P`<a,g> = b}"

  "LeftTranslation(G,P,g) ≡ {<a,b> ∈ G×G. P`<g,a> = b}"
 
  "RightTranslation2(G,P,g) ≡ 
  {<x,y> ∈ (G×G)×(G×G). ⟨P`<fst(x),g>, P`<snd(x),g>⟩ = y}"

  "LeftTranslation2(G,P,g) ≡ 
  {<x,y> ∈ (G×G)×(G×G). ⟨P`<g,fst(x)>, P`<g,snd(x)>⟩ = y}"

text{*Translations map $G$ into $G$. Two dimensional translations map
  $G\times G$ into itself.*}

lemma (in group0) group0_5_L1: assumes A1: "g∈G"
  shows "RightTranslation(G,f,g) : G->G"
  "LeftTranslation(G,f,g) : G->G"
  "RightTranslation2(G,f,g) : (G×G)->(G×G)"
  "LeftTranslation2(G,f,g) : (G×G)->(G×G)"
proof -
  from A1 have "∀a∈G. a·g ∈ G" "∀a∈G. g·a ∈ G"
    "∀x ∈ G×G.  <fst(x)·g, snd(x)·g> ∈ G×G"
    "∀x ∈ G×G.  <g·fst(x),g·snd(x)> ∈ G×G"
    using group_oper_assocA apply_funtype by auto;
  then show "RightTranslation(G,f,g) : G->G" 
    "LeftTranslation(G,f,g) : G->G"
    "RightTranslation2(G,f,g) : (G×G)->(G×G)"
    "LeftTranslation2(G,f,g) : (G×G)->(G×G)"
    using RightTranslation_def LeftTranslation_def
      RightTranslation2_def LeftTranslation2_def func1_1_L11A
    by auto;
qed;

text{*The values of the translations are what we expect.*}

lemma (in group0) group0_5_L2: assumes A1: "g∈G" "a∈G"
  shows 
  "RightTranslation(G,f,g)`(a) = a·g"
  "LeftTranslation(G,f,g)`(a) = g·a"
  using prems group0_5_L1 RightTranslation_def LeftTranslation_def
    func1_1_L11B by auto;

text{*The values of the two-dimensional translations are what we expect.*}

lemma (in group0) group0_5_L3: assumes A1: "g∈G" "a∈G" "b∈G"
  shows "RightTranslation2(G,f,g)`<a,b> = <a·g,b·g>"
  "LeftTranslation2(G,f,g)`<a,b> = <g·a,g·b>"
  using prems RightTranslation2_def LeftTranslation2_def
    group0_5_L1 func1_1_L11B by auto;


text{*Composition of left translations is a left translation by the product.*}

lemma (in group0) group0_5_L4: assumes A1:"g∈G" "h∈G" "a∈G"
  and A2: "Tg = LeftTranslation(G,f,g)" "Th = LeftTranslation(G,f,h)"
  shows "Tg`(Th`(a)) = g·h·a"
  "Tg`(Th`(a)) = LeftTranslation(G,f,g·h)`(a)"
proof -;
  from A1 have T1:"h·a∈G" "g·h∈G"
    using group_oper_assocA apply_funtype by auto;
  with A1 A2 show "Tg`(Th`(a)) = g·h·a"
    using group0_5_L2 group_oper_assoc by simp;
  with A1 A2 T1 show 
    "Tg`(Th`(a)) = LeftTranslation(G,f,g·h)`(a)"
    using group0_5_L2 group_oper_assoc by simp;
qed;

text{*Composition of right translations is a right translation by 
  the product.*}

lemma (in group0) group0_5_L5: assumes A1:"g∈G" "h∈G" "a∈G"
  and A2: "Tg = RightTranslation(G,f,g)" "Th = RightTranslation(G,f,h)"
  shows "Tg`(Th`(a)) = a·h·g"
  "Tg`(Th`(a)) = RightTranslation(G,f,h·g)`(a)"
proof -
  from A1 have T1: "a·h∈G" "h·g ∈G"
    using group_oper_assocA apply_funtype by auto;
  with A1 A2 show "Tg`(Th`(a)) = a·h·g" 
    using group0_5_L2 group_oper_assoc by simp;
  with A1 A2 T1 show 
    "Tg`(Th`(a)) = RightTranslation(G,f,h·g)`(a)"
    using group0_5_L2 group_oper_assoc by simp;
qed;

text{*The image of a set under a composition of translations is the same as
  the image under translation by a product.*}

lemma (in group0) group0_5_L6: assumes A1: "g∈G" "h∈G" and A2: "A⊆G"
  and A3: "Tg = RightTranslation(G,f,g)" "Th = RightTranslation(G,f,h)"
  shows "Tg``(Th``(A)) = {a·h·g. a∈A}"
proof -;
  from A2 have T1:"∀a∈A. a∈G" by auto;
  from A1 A3 have "Tg : G->G" "Th : G->G"
    using group0_5_L1 by auto;
  with A1 A2 T1 A3 show "Tg``(Th``(A)) = {a·h·g. a∈A}"
    using func1_1_L15C group0_5_L5 by simp;
qed;

section{*Odd functions*}

text{*This section is about odd functions.*}

text{*Odd functions are those that commute with the group inverse:
  $f(a^{-1}) = (f(a))^{-1}.$*}

constdefs

  "IsOdd(G,P,f) ≡ (∀a∈G. f`(GroupInv(G,P)`(a)) = GroupInv(G,P)`(f`(a)) )"

text{*Let's see the definition of an odd function in a more readable 
  notation.*}

lemma (in group0) group0_6_L1: 
  shows "IsOdd(G,f,p) <-> (∀a∈G. p`(a¯) = (p`(a))¯)"
  using IsOdd_def by simp;

text{*We can express the definition of an odd function in two ways.*}

lemma (in group0) group0_6_L2:
  assumes A1: "p : G->G" shows 
  "(∀a∈G. p`(a¯) = (p`(a))¯) <-> (∀a∈G. (p`(a¯))¯ = p`(a))"
proof
  assume "∀a∈G. p`(a¯) = (p`(a))¯"
  with A1 show "∀a∈G. (p`(a¯))¯ = p`(a)"
    using apply_funtype group_inv_of_inv by simp;
next assume A2: "∀a∈G. (p`(a¯))¯ = p`(a)"
  { fix a assume "a∈G"
    with A1 A2 have "p`(a¯) ∈ G"   "((p`(a¯))¯)¯ =  (p`(a))¯"
      using apply_funtype inverse_in_group by auto;
    then have "p`(a¯) = (p`(a))¯"
      using group_inv_of_inv by simp;
  } then show "∀a∈G. p`(a¯) = (p`(a))¯" by simp;
qed;

end