Theory AbelianGroup_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{AbelianGroup\_ZF.thy}*}

theory AbelianGroup_ZF imports Group_ZF

begin

text{*A group is called ``abelian`` if its operation is commutative, i.e.
  $P\langle a,b \rangle  = P\langle a,b \rangle$ for all group 
  elements $a,b$, where $P$ is the group operation. It is customary
  to use the additive notation for abelian groups, so this condition
  is typically written as $a+b = b+a$. We will be using multiplicative 
  notation though (in which the commutativity condition 
  of the operation is written as $a\cdot b = b\cdot a$), just to avoid
  the hassle of changing the notation we used for general groups. 
  *}

section{*Rearrangement formulae*}

text{*This section is not interesting and should not be read.
  Here we will prove formulas is which right hand side uses the same
  factors as the left hand side, just in different order. These facts
  are obvious in informal math sense, but Isabelle prover is not able
  to derive them automatically, so we have to prove them by hand. 
  *}

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. 
  As far removing parantheses is concerned Isabelle does its job 
  automatically.*}

lemma (in group0) group0_4_L2:
  assumes A1:"P {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:"P {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:"P {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: "P {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 "P {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 inv_cancel_two by simp;

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

lemma (in group0) group0_4_L4C: 
  assumes A1: "P {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: "P {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:"P {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: "P {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 inv_cancel_two
     by simp;
qed;

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

lemma (in group0) group0_4_L6AA: 
  assumes A1: "P {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: "P {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 "P {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: "P {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: "P {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: "P {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: "P {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: "P {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: "P {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: "P {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: "P {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 inv_cancel_two 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: "P {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
    inv_cancel_two 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: "P {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{*Some rearrangements with an equation.*}

lemma (in group0) group0_4_L9:
  assumes A1: "P {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;

end