(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005 - 2008 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 Monoid_ZF

begin;

text{*This theory file covers basics of group theory.*}

section{*Definition and basic properties of groups*}

text{*In this section we define the notion of a group and set up the

notation for discussing groups. We prove some basic theorems about

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. *}

definition

"IsAgroup(G,f) ≡

(IsAmonoid(G,f) ∧ (∀g∈G. ∃b∈G. f`⟨g,b⟩ = TheNeutralElement(G,f)))"

text{*We define the group inverse as the set

$\{\langle x,y \rangle \in G\times G: x\cdot y = e \}$, where $e$ is the

neutral element of the group. This set (which can be written as

$(\cdot)^{-1}\{ e\}$) is a certain relation on the group (carrier).

Since, as we show later, for every $x\in G$ there is exactly one $y\in G$

such that $x \cdot y = e$ this relation is in fact a function from $G$ to $G$.*}

definition

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

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

element is denoted $1$.*}

locale group0 =

fixes G

fixes P

assumes groupAssum: "IsAgroup(G,P)"

fixes neut ("\<one>")

defines neut_def[simp]: "\<one> ≡ TheNeutralElement(G,P)"

fixes groper (infixl "·" 70)

defines groper_def[simp]: "a · b ≡ P`⟨a,b⟩"

fixes inv ("_¯ " [90] 91)

defines inv_def[simp]: "x¯ ≡ GroupInv(G,P)`(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: shows "monoid0(G,P)"

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 assms IsAgroup_def by simp;

text{*A 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.unit_is_neutral 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 assms 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 assms 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 @{text "group0"} context.*}

lemma (in group0) group_oper_assocA: shows "P : G×G->G"

using groupAssum IsAgroup_def IsAmonoid_def IsAssociative_def

by simp;

text{*The definition of a 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 "c∈G" by simp;

have "\<one>∈G" using group0_2_L2 by simp;

with A1 A2 I have "b·g = b·(g·(b·c))"

using group_op_closed group0_2_L2 group_oper_assoc

by simp;

also from A1 A2 `c∈G` 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. Recall that

in Isabelle @{text "f-``(A)"} denotes the inverse image of

the set $A$. *}

theorem (in group0) group0_2_T3: shows "P-``{\<one>} = GroupInv(G,P)"

proof -;

from groupAssum have "P : G×G -> G"

using IsAgroup_def IsAmonoid_def IsAssociative_def

by simp;

then show "P-``{\<one>} = GroupInv(G,P)"

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,P) : 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,P) : G->G"

using group0_2_T2 by simp;

with A1 have "⟨x,x¯⟩ ∈ GroupInv(G,P)"

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;

text{*See the comment to @{text "group0_2_L7"}.*}

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 a unit either.*}

lemma (in group0) group0_2_L8B:

assumes "a∈G" and "a ≠ \<one>"

shows "a¯ ≠ \<one>" using assms group0_2_L8A by auto;

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

lemma (in group0) group0_2_L8C:

assumes "a∈G" and "a¯ ≠ \<one>"

shows "a≠\<one>"

using assms 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¯" and "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 "g∈G"

moreover from A1 `g∈G` have "b(g) ∈ G" by simp;

moreover from A1 `g∈G` 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

"b¯∈G" "a¯∈G" "a·b∈G" "b¯·a¯ ∈ G"

using inverse_in_group group_op_closed

by auto;

from A1 A2 `b¯·a¯ ∈ G` have "a·b·(b¯·a¯) = a·(b·(b¯·a¯))"

using group_oper_assoc by simp;

moreover from A2 `b¯∈G` `a¯∈G` have "b·(b¯·a¯) = b·b¯·a¯"

using group_oper_assoc by simp;

moreover from A2 `a¯∈G` 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 `a·b ∈ G` `b¯·a¯ ∈ G` 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 assms inverse_in_group group0_2_L6 group0_2_L9

by simp;

text{*Group inverse is nilpotent, therefore a bijection and involution.*}

lemma (in group0) group_inv_bij:

shows "GroupInv(G,P) O GroupInv(G,P) = id(G)" and "GroupInv(G,P) ∈ bij(G,G)" and

"GroupInv(G,P) = converse(GroupInv(G,P))"

proof -

have I: "GroupInv(G,P): G->G" using groupAssum group0_2_T2 by simp

then have "GroupInv(G,P) O GroupInv(G,P): G->G" and "id(G):G->G"

using comp_fun id_type by auto

moreover

{ fix g assume "g∈G"

with I have "(GroupInv(G,P) O GroupInv(G,P))`(g) = id(G)`(g)"

using comp_fun_apply group_inv_of_inv id_conv by simp

} hence "∀g∈G. (GroupInv(G,P) O GroupInv(G,P))`(g) = id(G)`(g)" by simp

ultimately show "GroupInv(G,P) O GroupInv(G,P) = id(G)"

by (rule func_eq)

with I show "GroupInv(G,P) ∈ bij(G,G)" using nilpotent_imp_bijective

by simp

with `GroupInv(G,P) O GroupInv(G,P) = id(G)` show

"GroupInv(G,P) = converse(GroupInv(G,P))" using comp_id_conv by simp

qed

text{*For the group inverse the image is the same as inverse image.*}

lemma (in group0) inv_image_vimage: shows "GroupInv(G,P)``(V) = GroupInv(G,P)-``(V)"

using group_inv_bij vimage_converse by simp

text{*If the unit is in a set then it is in the inverse of that set.*}

lemma (in group0) neut_inv_neut: assumes "A⊆G" and "\<one>∈A"

shows "\<one> ∈ GroupInv(G,P)``(A)"

proof -

have "GroupInv(G,P):G->G" using groupAssum group0_2_T2 by simp

with assms have "\<one>¯ ∈ GroupInv(G,P)``(A)" using func_imagedef by auto

then show ?thesis using group_inv_of_one by simp

qed

text{*The group inverse is onto.*}

lemma (in group0) group_inv_surj: shows "GroupInv(G,P)``(G) = G"

using group_inv_bij bij_def surj_range_image_domain by auto

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¯" and "(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{*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 of four group

elements.*}

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) inv_cancel_two:

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 inv_cancel_two

by simp;

qed;

text{*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 "H⊆G"

and "H {is closed under} P"

shows "(H ∪ {\<one>}) {is closed under} P"

using assms IsOpClosed_def group0_2_L2 by auto;

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" and "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 inv_cancel_two 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 operation is 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.

The rest of this section is devoted to proving the equivalence of these two

definitions of the notion of a subgroup.

*}

text{*A pair $(H,P)$ is a subgroup if $H$ forms a group with the

operation $P$ restricted to $H\times H$. It may be surprising that

we don't require $H$ to be a subset of $G$. This however can be inferred

from the definition if the pair $(G,P)$ is a group,

see lemma @{text "group0_3_L2"}.*}

definition

"IsAsubgroup(H,P) ≡ IsAgroup(H, restrict(P,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.

The next lemma states that the neutral element of

a 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 I:

"?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 A2 I show "∀h∈H. ?b`⟨n,h⟩ = h" and "∀h∈H. ?b`⟨h,n⟩ = h"

by auto;

qed;

text{*A subgroup is contained in the group.*}

lemma (in group0) group0_3_L2:

assumes A1: "IsAsubgroup(H,P)"

shows "H ⊆ G"

proof;

fix h assume "h∈H";

let ?b = "restrict(P,H×H)"

let ?n = "TheNeutralElement(H,restrict(P,H×H))"

from A1 have "?b ∈ H×H->H"

using IsAsubgroup_def IsAgroup_def

IsAmonoid_def IsAssociative_def by simp;

moreover from A1 `h∈H` have "⟨ ?n,h⟩ ∈ H×H"

using group0_3_L1 by simp;

moreover from A1 `h∈H` 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⟩ ∈ P" using restrict_subset by auto

moreover from groupAssum have "P: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's neutral element (denoted $1$ in the group0 context)

is a neutral element for the subgroup with respect to the group action.*}

lemma (in group0) group0_3_L3:

assumes "IsAsubgroup(H,P)"

shows "∀h∈H. \<one>·h = h ∧ h·\<one> = h"

using assms groupAssum group0_3_L2 group0_2_L2

by auto;

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,P)"

shows "TheNeutralElement(H,restrict(P,H×H)) = \<one>"

proof -;

let ?n = "TheNeutralElement(H,restrict(P,H×H))"

from A1 have "?n ∈ H" using group0_3_L1 by simp;

with groupAssum A1 have "?n∈G" using group0_3_L2 by auto;

with A1 `?n ∈ H` 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,P)"

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,P)"

and A2: "a∈H" "b∈H"

shows "a·b ∈ H"

proof -;

let ?f = "restrict(P,H×H)"

from A1 have "monoid0(H,?f)" using

IsAsubgroup_def IsAgroup_def monoid0_def by simp;

with A2 have "?f` (⟨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 -

let ?e = "TheNeutralElement(G,f)"

let ?e⇩_{1}= "TheNeutralElement(H,g)"

from A1 have "group0(G,f)" using group0_def by simp;

from A2 A3 have "group0(H,g)"

using IsAsubgroup_def group0_def by simp;

from `group0(G,f)` A2 A3 have "GroupInv(G,f) = f-``{?e⇩_{1}}"

using group0.group0_3_L4 group0.group0_2_T3

by simp;

moreover have "g-``{?e⇩_{1}} = f-``{?e⇩_{1}} ∩ H×H"

proof -

from A1 have "f ∈ G×G->G"

using IsAgroup_def IsAmonoid_def IsAssociative_def

by simp;

moreover from A2 `group0(G,f)` have "H×H ⊆ G×G"

using group0.group0_3_L2 by auto;

ultimately show "g-``{?e⇩_{1}} = f-``{?e⇩_{1}} ∩ H×H"

using A3 func1_2_L1 by simp;

qed;

moreover from A3 `group0(H,g)` have "GroupInv(H,g) = g-``{?e⇩_{1}}"

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,P)"

and A2: "g = restrict(P,H×H)"

shows "GroupInv(H,g) = restrict(GroupInv(G,P),H)"

proof -;

from groupAssum have "GroupInv(G,P) : 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,P) ∩ 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,P)"

and "g = restrict(P,H×H)"

shows "∀h∈H. GroupInv(H,g)`(h) = h¯"

using assms group0_3_T1 restrict_if by simp;

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

theorem (in group0) group0_3_T3A:

assumes A1: "IsAsubgroup(H,P)" and A2: "h∈H"

shows "h¯∈ H"

proof -

let ?g = "restrict(P,H×H)";

from 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 A2 show "h¯∈ H" using group0_3_T2 by simp;

qed;

text{*The next theorem states that a nonempty subset 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} P"

and A4: "∀x∈H. x¯ ∈ H"

shows "IsAsubgroup(H,P)"

proof -;

let ?g = "restrict(P,H×H)"

let ?n = "TheNeutralElement(H,?g)"

from A3 have I: "∀x∈H.∀y∈H. x·y ∈ H"

using IsOpClosed_def by simp;

from A1 obtain x where "x∈H" by auto;

with A4 I A2 have "\<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 "h∈H"

with A4 A2 have "h·h¯ = \<one>"

using group0_2_L6 by auto;

moreover from groupAssum A2 A3 `\<one>∈H` have "\<one> = ?n"

using IsAgroup_def group0_1_L6 by auto;

moreover from A4 `h∈H` have "?g`⟨h,h¯⟩ = h·h¯"

using restrict_if by simp;

ultimately have "?g`⟨h,h¯⟩ = ?n" by simp;

with A4 `h∈H` show "∃b∈H. ?g`⟨h,b⟩ = ?n" by auto;

qed;

ultimately show "IsAsubgroup(H,P)" using

IsAsubgroup_def IsAgroup_def by simp;

qed;

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

lemma group0_3_L7:

assumes A1: "IsAgroup(G,f)"

and A2: "IsAsubgroup(H⇩_{1},f)"

and A3: "IsAsubgroup(H⇩_{2},f)"

shows "IsAsubgroup(H⇩_{1}∩H⇩_{2},restrict(f,H⇩_{1}×H⇩_{1}))"

proof -;

let ?e = "TheNeutralElement(G,f)"

let ?g = "restrict(f,H⇩_{1}×H⇩_{1})"

from A1 have I: "group0(G,f)"

using group0_def by simp;

from A2 have "group0(H⇩_{1},?g)"

using IsAsubgroup_def group0_def by simp;

moreover have "H⇩_{1}∩H⇩_{2}≠ 0"

proof -

from A1 A2 A3 have "?e ∈ H⇩_{1}∩H⇩_{2}"

using group0_def group0.group0_3_L5 by simp;

thus ?thesis by auto;

qed;

moreover have "H⇩_{1}∩H⇩_{2}⊆ H⇩_{1}" by auto;

moreover from A2 A3 I `H⇩_{1}∩H⇩_{2}⊆ H⇩_{1}` have

"H⇩_{1}∩H⇩_{2}{is closed under} ?g"

using group0.group0_3_L6 IsOpClosed_def

func_ZF_4_L7 func_ZF_4_L5 by simp;

moreover from A2 A3 I have

"∀x ∈ H⇩_{1}∩H⇩_{2}. GroupInv(H⇩_{1},?g)`(x) ∈ H⇩_{1}∩H⇩_{2}"

using group0.group0_3_T2 group0.group0_3_T3A

by simp;

ultimately show ?thesis

using group0.group0_3_T3 by simp;

qed;

text{*The range of the subgroup operation is the whole subgroup.*}

lemma image_subgr_op: assumes A1: "IsAsubgroup(H,P)"

shows "restrict(P,H×H)``(H×H) = H"

proof -

from A1 have "monoid0(H,restrict(P,H×H))"

using IsAsubgroup_def IsAgroup_def monoid0_def

by simp

then show ?thesis by (rule monoid0.range_carr);

qed

text{*If we restrict the inverse to a subgroup, then the restricted

inverse is onto the subgroup.*}

lemma (in group0) restr_inv_onto: assumes A1: "IsAsubgroup(H,P)"

shows "restrict(GroupInv(G,P),H)``(H) = H"

proof -

from A1 have "GroupInv(H,restrict(P,H×H))``(H) = H"

using IsAsubgroup_def group0_def group0.group_inv_surj

by simp;

with A1 show ?thesis using group0_3_T1 by simp;

qed;

end