(*

This file is a part of IsarMathLib -

a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 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\_1.thy}*}

theory Group_ZF_1 imports Group_ZF

begin

text{*In this theory we consider right and left translations and odd

functions.*}

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)$.

*}

text{*For an element $a\in G$ the right translation is defined

a function (set of pairs) such that its value (the second element

of a pair) is the value of the group operation on the first element

of the pair and $g$. This looks a bit strange in the raw set notation,

when we write a function explicitely as a set of pairs and value of

the group operation on the pair $\langle a,b \rangle$

as @{text "P`⟨a,b⟩"} instead of the usual infix $a\cdot b$

or $a + b$. *}

definition

"RightTranslation(G,P,g) ≡ {⟨ a,b⟩ ∈ G×G. P`⟨a,g⟩ = b}"

text{*A similar definition of the left translation.*}

definition

"LeftTranslation(G,P,g) ≡ {⟨a,b⟩ ∈ G×G. P`⟨g,a⟩ = b}"

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,P,g) : G->G" and "LeftTranslation(G,P,g) : G->G"

proof -

from A1 have "∀a∈G. a·g ∈ G" and "∀a∈G. g·a ∈ G"

using group_oper_assocA apply_funtype by auto;

then show

"RightTranslation(G,P,g) : G->G"

"LeftTranslation(G,P,g) : G->G"

using RightTranslation_def LeftTranslation_def func1_1_L11A

by auto;

qed;

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

lemma (in group0) group0_5_L2: assumes "g∈G" "a∈G"

shows

"RightTranslation(G,P,g)`(a) = a·g"

"LeftTranslation(G,P,g)`(a) = g·a"

using assms group0_5_L1 RightTranslation_def LeftTranslation_def

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: "T⇩_{g}= LeftTranslation(G,P,g)" "T⇩_{h}= LeftTranslation(G,P,h)"

shows

"T⇩_{g}`(T⇩_{h}`(a)) = g·h·a"

"T⇩_{g}`(T⇩_{h}`(a)) = LeftTranslation(G,P,g·h)`(a)"

proof -;

from A1 have I: "h·a∈G" "g·h∈G"

using group_oper_assocA apply_funtype by auto;

with A1 A2 show "T⇩_{g}`(T⇩_{h}`(a)) = g·h·a"

using group0_5_L2 group_oper_assoc by simp;

with A1 A2 I show

"T⇩_{g}`(T⇩_{h}`(a)) = LeftTranslation(G,P,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: "T⇩_{g}= RightTranslation(G,P,g)" "T⇩_{h}= RightTranslation(G,P,h)"

shows

"T⇩_{g}`(T⇩_{h}`(a)) = a·h·g"

"T⇩_{g}`(T⇩_{h}`(a)) = RightTranslation(G,P,h·g)`(a)"

proof -

from A1 have I: "a·h∈G" "h·g ∈G"

using group_oper_assocA apply_funtype by auto;

with A1 A2 show "T⇩_{g}`(T⇩_{h}`(a)) = a·h·g"

using group0_5_L2 group_oper_assoc by simp;

with A1 A2 I show

"T⇩_{g}`(T⇩_{h}`(a)) = RightTranslation(G,P,h·g)`(a)"

using group0_5_L2 group_oper_assoc by simp;

qed

text{*Point free version of @{text "group0_5_L4"} and @{text "group0_5_L5"}. *}

lemma (in group0) trans_comp: assumes "g∈G" "h∈G" shows

"RightTranslation(G,P,g) O RightTranslation(G,P,h) = RightTranslation(G,P,h·g)"

"LeftTranslation(G,P,g) O LeftTranslation(G,P,h) = LeftTranslation(G,P,g·h)"

proof -

let ?T⇩_{g}= "RightTranslation(G,P,g)"

let ?T⇩_{h}= "RightTranslation(G,P,h)"

from assms have "?T⇩_{g}:G->G" and "?T⇩_{h}:G->G"

using group0_5_L1 by auto

then have "?T⇩_{g}O ?T⇩_{h}:G->G" using comp_fun by simp

moreover from assms have "RightTranslation(G,P,h·g):G->G"

using group_op_closed group0_5_L1 by simp

moreover from assms `?T⇩_{h}:G->G` have

"∀a∈G. (?T⇩_{g}O ?T⇩_{h})`(a) = RightTranslation(G,P,h·g)`(a)"

using comp_fun_apply group0_5_L5 by simp

ultimately show "?T⇩_{g}O ?T⇩_{h}= RightTranslation(G,P,h·g)"

by (rule func_eq)

next

let ?T⇩_{g}= "LeftTranslation(G,P,g)"

let ?T⇩_{h}= "LeftTranslation(G,P,h)"

from assms have "?T⇩_{g}:G->G" and "?T⇩_{h}:G->G"

using group0_5_L1 by auto

then have "?T⇩_{g}O ?T⇩_{h}:G->G" using comp_fun by simp

moreover from assms have "LeftTranslation(G,P,g·h):G->G"

using group_op_closed group0_5_L1 by simp

moreover from assms `?T⇩_{h}:G->G` have

"∀a∈G. (?T⇩_{g}O ?T⇩_{h})`(a) = LeftTranslation(G,P,g·h)`(a)"

using comp_fun_apply group0_5_L4 by simp

ultimately show "?T⇩_{g}O ?T⇩_{h}= LeftTranslation(G,P,g·h)"

by (rule func_eq)

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) trans_comp_image: assumes A1: "g∈G" "h∈G" and

A2: "T⇩_{g}= LeftTranslation(G,P,g)" "T⇩_{h}= LeftTranslation(G,P,h)"

shows "T⇩_{g}``(T⇩_{h}``(A)) = LeftTranslation(G,P,g·h)``(A)"

proof -

from A2 have "T⇩_{g}``(T⇩_{h}``(A)) = (T⇩_{g}O T⇩_{h})``(A)"

using image_comp by simp

with assms show ?thesis using trans_comp by simp

qed

text{*Another form of the image of a set under a composition of translations *}

lemma (in group0) group0_5_L6:

assumes A1: "g∈G" "h∈G" and A2: "A⊆G" and

A3: "T⇩_{g}= RightTranslation(G,P,g)" "T⇩_{h}= RightTranslation(G,P,h)"

shows "T⇩_{g}``(T⇩_{h}``(A)) = {a·h·g. a∈A}"

proof -;

from A2 have "∀a∈A. a∈G" by auto;

from A1 A3 have "T⇩_{g}: G->G" "T⇩_{h}: G->G"

using group0_5_L1 by auto;

with assms `∀a∈A. a∈G` show

"T⇩_{g}``(T⇩_{h}``(A)) = {a·h·g. a∈A}"

using func1_1_L15C group0_5_L5 by auto;

qed

text{*The translation by neutral element is the identity on group.*}

lemma (in group0) trans_neutral: shows

"RightTranslation(G,P,\<one>) = id(G)" and "LeftTranslation(G,P,\<one>) = id(G)"

proof -

have "RightTranslation(G,P,\<one>):G->G" and "∀a∈G. RightTranslation(G,P,\<one>)`(a) = a"

using group0_2_L2 group0_5_L1 group0_5_L2 by auto

then show "RightTranslation(G,P,\<one>) = id(G)" by (rule indentity_fun)

have "LeftTranslation(G,P,\<one>):G->G" and "∀a∈G. LeftTranslation(G,P,\<one>)`(a) = a"

using group0_2_L2 group0_5_L1 group0_5_L2 by auto

then show "LeftTranslation(G,P,\<one>) = id(G)" by (rule indentity_fun)

qed

text{*Composition of translations by an element and its inverse is identity.*}

lemma (in group0) trans_comp_id: assumes "g∈G" shows

"RightTranslation(G,P,g) O RightTranslation(G,P,g¯) = id(G)" and

"RightTranslation(G,P,g¯) O RightTranslation(G,P,g) = id(G)" and

"LeftTranslation(G,P,g) O LeftTranslation(G,P,g¯) = id(G)" and

"LeftTranslation(G,P,g¯) O LeftTranslation(G,P,g) = id(G)"

using assms inverse_in_group trans_comp group0_2_L6 trans_neutral by auto

text{*Translations are bijective.*}

lemma (in group0) trans_bij: assumes "g∈G" shows

"RightTranslation(G,P,g) ∈ bij(G,G)" and "LeftTranslation(G,P,g) ∈ bij(G,G)"

proof-

from assms have

"RightTranslation(G,P,g):G->G" and

"RightTranslation(G,P,g¯):G->G" and

"RightTranslation(G,P,g) O RightTranslation(G,P,g¯) = id(G)"

"RightTranslation(G,P,g¯) O RightTranslation(G,P,g) = id(G)"

using inverse_in_group group0_5_L1 trans_comp_id by auto

then show "RightTranslation(G,P,g) ∈ bij(G,G)" using fg_imp_bijective by simp

from assms have

"LeftTranslation(G,P,g):G->G" and

"LeftTranslation(G,P,g¯):G->G" and

"LeftTranslation(G,P,g) O LeftTranslation(G,P,g¯) = id(G)"

"LeftTranslation(G,P,g¯) O LeftTranslation(G,P,g) = id(G)"

using inverse_in_group group0_5_L1 trans_comp_id by auto

then show "LeftTranslation(G,P,g) ∈ bij(G,G)" using fg_imp_bijective by simp

qed

text{*Converse of a translation is translation by the inverse.*}

lemma (in group0) trans_conv_inv: assumes "g∈G" shows

"converse(RightTranslation(G,P,g)) = RightTranslation(G,P,g¯)" and

"converse(LeftTranslation(G,P,g)) = LeftTranslation(G,P,g¯)" and

"LeftTranslation(G,P,g) = converse(LeftTranslation(G,P,g¯))" and

"RightTranslation(G,P,g) = converse(RightTranslation(G,P,g¯))"

proof -

from assms have

"RightTranslation(G,P,g) ∈ bij(G,G)" "RightTranslation(G,P,g¯) ∈ bij(G,G)" and

"LeftTranslation(G,P,g) ∈ bij(G,G)" "LeftTranslation(G,P,g¯) ∈ bij(G,G)"

using trans_bij inverse_in_group by auto

moreover from assms have

"RightTranslation(G,P,g¯) O RightTranslation(G,P,g) = id(G)" and

"LeftTranslation(G,P,g¯) O LeftTranslation(G,P,g) = id(G)" and

"LeftTranslation(G,P,g) O LeftTranslation(G,P,g¯) = id(G)" and

"LeftTranslation(G,P,g¯) O LeftTranslation(G,P,g) = id(G)"

using trans_comp_id by auto

ultimately show

"converse(RightTranslation(G,P,g)) = RightTranslation(G,P,g¯)" and

"converse(LeftTranslation(G,P,g)) = LeftTranslation(G,P,g¯)" and

"LeftTranslation(G,P,g) = converse(LeftTranslation(G,P,g¯))" and

"RightTranslation(G,P,g) = converse(RightTranslation(G,P,g¯))"

using comp_id_conv by auto

qed

text{*The image of a set by translation is the same as the inverse image by

by the inverse element translation.*}

lemma (in group0) trans_image_vimage: assumes "g∈G" shows

"LeftTranslation(G,P,g)``(A) = LeftTranslation(G,P,g¯)-``(A)" and

"RightTranslation(G,P,g)``(A) = RightTranslation(G,P,g¯)-``(A)"

using assms trans_conv_inv vimage_converse by auto

text{*Another way of looking at translations is that they are sections

of the group operation. *}

lemma (in group0) trans_eq_section: assumes "g∈G" shows

"RightTranslation(G,P,g) = Fix2ndVar(P,g)" and

"LeftTranslation(G,P,g) = Fix1stVar(P,g)"

proof -

let ?T = "RightTranslation(G,P,g)"

let ?F = "Fix2ndVar(P,g)"

from assms have "?T: G->G" and "?F: G->G"

using group0_5_L1 group_oper_assocA fix_2nd_var_fun by auto

moreover from assms have "∀a∈G. ?T`(a) = ?F`(a)"

using group0_5_L2 group_oper_assocA fix_var_val by simp

ultimately show "?T = ?F" by (rule func_eq)

next

let ?T = "LeftTranslation(G,P,g)"

let ?F = "Fix1stVar(P,g)"

from assms have "?T: G->G" and "?F: G->G"

using group0_5_L1 group_oper_assocA fix_1st_var_fun by auto

moreover from assms have "∀a∈G. ?T`(a) = ?F`(a)"

using group0_5_L2 group_oper_assocA fix_var_val by simp

ultimately show "?T = ?F" by (rule func_eq)

qed

text{*A lemma about translating sets.*}

lemma (in group0) ltrans_image: assumes A1: "V⊆G" and A2: "x∈G"

shows "LeftTranslation(G,P,x)``(V) = {x·v. v∈V}"

proof -

from assms have "LeftTranslation(G,P,x)``(V) = {LeftTranslation(G,P,x)`(v). v∈V}"

using group0_5_L1 func_imagedef by blast

moreover from assms have "∀v∈V. LeftTranslation(G,P,x)`(v) = x·v"

using group0_5_L2 by auto

ultimately show ?thesis by auto

qed

text{*A technical lemma about solving equations with translations.*}

lemma (in group0) ltrans_inv_in: assumes A1: "V⊆G" and A2: "y∈G" and

A3: "x ∈ LeftTranslation(G,P,y)``(GroupInv(G,P)``(V))"

shows "y ∈ LeftTranslation(G,P,x)``(V)"

proof -

have "x∈G"

proof -

from A2 have "LeftTranslation(G,P,y):G->G" using group0_5_L1 by simp

then have "LeftTranslation(G,P,y)``(GroupInv(G,P)``(V)) ⊆ G"

using func1_1_L6 by simp

with A3 show "x∈G" by auto

qed

have "∃v∈V. x = y·v¯"

proof -

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

by simp

with assms obtain z where "z ∈ GroupInv(G,P)``(V)" and "x = y·z"

using func1_1_L6 ltrans_image by auto

with A1 `GroupInv(G,P): G->G` show ?thesis using func_imagedef by auto

qed

then obtain v where "v∈V" and "x = y·v¯" by auto

with A1 A2 have "y = x·v" using inv_cancel_two by auto

with assms `x∈G` `v∈V` show ?thesis using ltrans_image by auto

qed

text{*We can look at the result of interval arithmetic operation as union of

translated sets.*}

lemma (in group0) image_ltrans_union: assumes "A⊆G" "B⊆G" shows

"(P {lifted to subsets of} G)`⟨A,B⟩ = (\<Union>a∈A. LeftTranslation(G,P,a)``(B))"

proof

from assms have I: "(P {lifted to subsets of} G)`⟨A,B⟩ = {a·b . ⟨a,b⟩ ∈ A×B}"

using group_oper_assocA lift_subsets_explained by simp

{ fix c assume "c ∈ (P {lifted to subsets of} G)`⟨A,B⟩"

with I obtain a b where "c = a·b" and "a∈A" "b∈B" by auto

hence "c ∈ {a·b. b∈B}" by auto

moreover from assms `a∈A` have

"LeftTranslation(G,P,a)``(B) = {a·b. b∈B}" using ltrans_image by auto

ultimately have "c ∈ LeftTranslation(G,P,a)``(B)" by simp

with `a∈A` have "c ∈ (\<Union>a∈A. LeftTranslation(G,P,a)``(B))" by auto

} thus "(P {lifted to subsets of} G)`⟨A,B⟩ ⊆ (\<Union>a∈A. LeftTranslation(G,P,a)``(B))"

by auto

{ fix c assume "c ∈ (\<Union>a∈A. LeftTranslation(G,P,a)``(B))"

then obtain a where "a∈A" and "c ∈ LeftTranslation(G,P,a)``(B)"

by auto

moreover from assms `a∈A` have "LeftTranslation(G,P,a)``(B) = {a·b. b∈B}"

using ltrans_image by auto

ultimately obtain b where "b∈B" and "c = a·b" by auto

with I `a∈A` have "c ∈ (P {lifted to subsets of} G)`⟨A,B⟩" by auto

} thus "(\<Union>a∈A. LeftTranslation(G,P,a)``(B)) ⊆ (P {lifted to subsets of} G)`⟨A,B⟩"

by auto

qed

text{*If the neutral element belongs to a set, then an element of group belongs

the translation of that set.*}

lemma (in group0) neut_trans_elem:

assumes A1: "A⊆G" "g∈G" and A2: "\<one>∈A"

shows "g ∈ LeftTranslation(G,P,g)``(A)"

proof -

from assms have "g·\<one> ∈ LeftTranslation(G,P,g)``(A)"

using ltrans_image by auto

with A1 show ?thesis using group0_2_L2 by simp

qed

text{*The neutral element belongs to the translation of a set by the inverse

of an element that belongs to it.*}

lemma (in group0) elem_trans_neut: assumes A1: "A⊆G" and A2: "g∈A"

shows "\<one> ∈ LeftTranslation(G,P,g¯)``(A)"

proof -

from assms have "g¯ ∈ G" using inverse_in_group by auto

with assms have "g¯·g ∈ LeftTranslation(G,P,g¯)``(A)"

using ltrans_image by auto

moreover from assms have "g¯·g = \<one>" using group0_2_L6 by auto

ultimately show ?thesis 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}.$*}

definition

"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,P,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" and "((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