Theory Group_ZF_1

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

*)

section ‹Groups 1›

theory Group_ZF_1 imports Group_ZF

begin

text‹In this theory we consider right and left translations and odd 
  functions.›

subsection‹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 ‹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_fun 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_fun 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_fun 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 ‹group0_5_L4› and ‹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,𝟭) = id(G)" and "LeftTranslation(G,P,𝟭) = id(G)"
proof -
  have "RightTranslation(G,P,𝟭):G→G" and "∀a∈G. RightTranslation(G,P,𝟭)`(a) = a"
    using group0_2_L2 group0_5_L1 group0_5_L2  by auto
  then show "RightTranslation(G,P,𝟭) = id(G)" by (rule indentity_fun)
  have "LeftTranslation(G,P,𝟭):G→G" and "∀a∈G. LeftTranslation(G,P,𝟭)`(a) = a"
    using group0_2_L2 group0_5_L1 group0_5_L2  by auto
  then show "LeftTranslation(G,P,𝟭) = id(G)" by (rule indentity_fun)
qed

text‹Translation by neutral element does not move sets. ›

lemma (in group0) trans_neutral_image: assumes "V⊆G"
  shows "RightTranslation(G,P,𝟭)``(V) = V" and "LeftTranslation(G,P,𝟭)``(V) = V"
  using assms trans_neutral image_id_same by auto

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_fun fix_2nd_var_fun by auto
  moreover from assms have "∀a∈G. ?T`(a) = ?F`(a)"
    using group0_5_L2 group_oper_fun 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_fun fix_1st_var_fun by auto
  moreover from assms have "∀a∈G. ?T`(a) = ?F`(a)"
    using group0_5_L2 group_oper_fun fix_var_val by simp
  ultimately show "?T = ?F" by (rule func_eq)
qed

text‹A lemma demonstrating what is the left translation of a set›

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 lemma demonstrating what is the right translation of a set›

lemma (in group0) rtrans_image: assumes A1: "V⊆G" and A2: "x∈G"
  shows "RightTranslation(G,P,x)``(V) = {v⋅x. v∈V}"
proof -
  from assms have "RightTranslation(G,P,x)``(V) = {RightTranslation(G,P,x)`(v). v∈V}"
    using group0_5_L1 func_imagedef by blast
  moreover from assms have "∀v∈V. RightTranslation(G,P,x)`(v) = v⋅x"
    using group0_5_L2 by auto
  ultimately show ?thesis by auto
qed

text‹Right and left translations of a set are subsets of the group. 
  Interestingly, we do not have to assume the set is a subset of the group. ›

lemma (in group0) lrtrans_in_group: assumes "x∈G"
  shows "LeftTranslation(G,P,x)``(V) ⊆ G" and "RightTranslation(G,P,x)``(V) ⊆ G" 
proof -
  from assms have "LeftTranslation(G,P,x):G→G" and "RightTranslation(G,P,x):G→G"
    using group0_5_L1 by auto
  then show "LeftTranslation(G,P,x)``(V) ⊆ G" and "RightTranslation(G,P,x)``(V) ⊆ G"
    using func1_1_L6(2) 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
  left translated sets.›

lemma (in group0) image_ltrans_union: assumes "A⊆G" "B⊆G" shows
  "(P {lifted to subsets of} G)`⟨A,B⟩ = (⋃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_fun 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 ∈ (⋃a∈A.  LeftTranslation(G,P,a)``(B))" by auto
  } thus "(P {lifted to subsets of} G)`⟨A,B⟩ ⊆ (⋃a∈A.  LeftTranslation(G,P,a)``(B))"
    by auto
  { fix c assume "c ∈ (⋃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 "(⋃a∈A. LeftTranslation(G,P,a)``(B)) ⊆ (P {lifted to subsets of} G)`⟨A,B⟩"
    by auto
qed

text‹ The right translation version of ‹image_ltrans_union› The proof follows the same schema.›

lemma (in group0) image_rtrans_union: assumes "A⊆G" "B⊆G" shows
  "(P {lifted to subsets of} G)`⟨A,B⟩ = (⋃b∈B.  RightTranslation(G,P,b)``(A))"
proof
  from assms have I: "(P {lifted to subsets of} G)`⟨A,B⟩ = {a⋅b . ⟨a,b⟩ ∈ A×B}"
    using group_oper_fun 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. a∈A}" by auto
    moreover from assms ‹b∈B› have 
      "RightTranslation(G,P,b)``(A) = {a⋅b. a∈A}" using rtrans_image by auto
    ultimately have "c ∈ RightTranslation(G,P,b)``(A)" by simp
    with ‹b∈B› have "c ∈ (⋃b∈B.  RightTranslation(G,P,b)``(A))" by auto
  } thus "(P {lifted to subsets of} G)`⟨A,B⟩ ⊆ (⋃b∈B.  RightTranslation(G,P,b)``(A))"
    by auto
  { fix c assume "c ∈ (⋃b∈B.  RightTranslation(G,P,b)``(A))"
    then obtain b where "b∈B" and "c ∈ RightTranslation(G,P,b)``(A)"
      by auto
    moreover from assms ‹b∈B› have "RightTranslation(G,P,b)``(A) = {a⋅b. a∈A}"
      using rtrans_image by auto
    ultimately obtain a where "a∈A" and "c = a⋅b" by auto
    with I ‹b∈B› have "c ∈ (P {lifted to subsets of} G)`⟨A,B⟩" by auto
  } thus "(⋃b∈B. RightTranslation(G,P,b)``(A)) ⊆ (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: "𝟭∈A" 
  shows "g ∈ LeftTranslation(G,P,g)``(A)" "g ∈ RightTranslation(G,P,g)``(A)"
proof -
  from assms have "g⋅𝟭 ∈ LeftTranslation(G,P,g)``(A)"
    using ltrans_image by auto
  with A1 show "g ∈ LeftTranslation(G,P,g)``(A)" using group0_2_L2 by simp
  from assms have "𝟭⋅g ∈ RightTranslation(G,P,g)``(A)"
    using rtrans_image by auto
  with A1 show "g ∈ RightTranslation(G,P,g)``(A)" 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 "𝟭 ∈ LeftTranslation(G,P,g¯)``(A)" "𝟭 ∈ RightTranslation(G,P,g¯)``(A)"
proof -
  from assms have ginv:"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 = 𝟭" using group0_2_L6 by auto
  ultimately show "𝟭 ∈ LeftTranslation(G,P,g¯)``(A)" by simp
  from ginv assms have "g⋅g¯ ∈ RightTranslation(G,P,g¯)``(A)"
    using rtrans_image by auto
  moreover from assms have "g⋅g¯ = 𝟭" using group0_2_L6 by auto
  ultimately show "𝟭 ∈ RightTranslation(G,P,g¯)``(A)" by simp
qed

subsection‹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

subsection‹Subgroups and interval arithmetic›

text‹ The section ‹Binary operations› in the ‹func_ZF› theory defines the notion of 
  "lifting operation to subsets". In short, every binary operation 
  $f:X\times X \longrightarrow X $ on a set $X$ defines an operation
  on the subsets of $X$ defined by $F(A,B) = \{ f\langle x,y \rangle | x\in A, y\in B\}$.
  In the group context using multiplicative notation we can write this as 
  $H\cdot K = \{ x\cdot y | x\in A, y\in B\}$. Similarly we can define $H^{-1}=\{ x^{-1} | x\in H\}$.
  In this section we study properties of these derived operations and how they relate to the concept
  of subgroups.›

text‹The next locale extends the ‹groups0› locale with notation related to interval arithmetics.›

locale group4 = group0 +
  fixes sdot (infixl "\<sdot>" 70)
  defines sdot_def [simp]: "A\<sdot>B  ≡ (P {lifted to subsets of} G)`⟨A,B⟩"

  fixes sinv ("_\<sinv> " [90] 91)
  defines sinv_def[simp]: "A\<sinv> ≡ GroupInv(G,P)``(A)"

text‹The next lemma shows a somewhat more explicit way of defining the product 
  of two subsets of a group.›

lemma (in group4) interval_prod: assumes "A⊆G" "B⊆G" 
  shows "A\<sdot>B =  {x⋅y. ⟨x,y⟩ ∈ A×B}"
  using assms group_oper_fun lift_subsets_explained by auto

text‹Product of elements of subsets of the group is in the set product of those subsets›

lemma (in group4) interval_prod_el: assumes "A⊆G" "B⊆G" "x∈A" "y∈B"
  shows "x⋅y ∈ A\<sdot>B"
  using assms interval_prod by auto

text‹An alternative definition of a group inverse of a set.›

lemma (in group4) interval_inv: assumes "A⊆G"
  shows "A\<sinv> = {x¯.x∈A}"
proof -
  from groupAssum have "GroupInv(G,P):G→G" using group0_2_T2 by simp
  with assms show "A\<sinv> = {x¯.x∈A}" using func_imagedef by simp
qed

text‹Group inverse of a set is a subset of the group. 
  Interestingly we don't need to assume the set is a subset of the group.›

lemma (in group4) interval_inv_cl: shows "A\<sinv> ⊆ G"
proof -
  from groupAssum have "GroupInv(G,P):G→G" using group0_2_T2 by simp
  then show "A\<sinv> ⊆ G" using func1_1_L6(2) by simp
qed

text‹The product of two subsets of a group is a subset of the group.›

lemma (in group4) interval_prod_closed: assumes "A⊆G" "B⊆G"
  shows "A\<sdot>B ⊆ G"
proof
  fix z assume "z ∈ A\<sdot>B"
  with assms obtain x y where "x∈A" "y∈B" "z=x⋅y" using interval_prod by auto
  with assms show "z∈G" using group_op_closed by auto
qed

text‹ The product of sets operation is associative.›

lemma (in group4) interval_prod_assoc: assumes "A⊆G" "B⊆G" "C⊆G"
  shows "A\<sdot>B\<sdot>C = A\<sdot>(B\<sdot>C)"
proof -
  from groupAssum have "(P {lifted to subsets of} G) {is associative on} Pow(G)" 
    unfolding IsAgroup_def IsAmonoid_def using lift_subset_assoc by simp
  with assms show ?thesis unfolding IsAssociative_def by auto
qed

text‹ A simple rearrangement following from associativity of the product of sets operation.›

lemma (in group4) interval_prod_rearr1: assumes "A⊆G" "B⊆G" "C⊆G" "D⊆G"
  shows "A\<sdot>B\<sdot>(C\<sdot>D) = A\<sdot>(B\<sdot>C)\<sdot>D"
proof -
  from assms(1,2) have "A\<sdot>B ⊆ G" using interval_prod_closed by simp
  with assms(3,4) have "A\<sdot>B\<sdot>(C\<sdot>D) = A\<sdot>B\<sdot>C\<sdot>D"
    using interval_prod_assoc by simp
  also from assms(1,2,3) have "A\<sdot>B\<sdot>C\<sdot>D = A\<sdot>(B\<sdot>C)\<sdot>D"
    using interval_prod_assoc by simp
  finally show ?thesis by simp
qed

text‹A subset $A$ of the group is closed with respect to the group operation 
  iff $A\cdot A \subseteq A$. ›

lemma (in group4) subset_gr_op_cl: assumes "A⊆G" 
  shows "(A {is closed under} P) ⟷ A\<sdot>A ⊆ A"
proof
  assume "A {is closed under} P"
  { fix z assume "z ∈ A\<sdot>A"
    with assms obtain x y where "x∈A" "y∈A" and "z=x⋅y" using interval_prod by auto
    with ‹A {is closed under} P› have "z∈A" unfolding IsOpClosed_def by simp
  } thus "A\<sdot>A ⊆ A" by auto
next
  assume "A\<sdot>A ⊆ A"
  { fix x y assume "x∈A" "y∈A"
    with assms have "x⋅y ∈ A\<sdot>A" using interval_prod by auto
    with ‹A\<sdot>A ⊆ A› have "x⋅y ∈ A" by auto
  } then show "A {is closed under} P" unfolding IsOpClosed_def by simp
qed

text‹Inverse and square of a subgroup is this subgroup.›

lemma (in group4) subgroup_inv_sq: assumes "IsAsubgroup(H,P)" 
   shows "H\<sinv> = H" and "H\<sdot>H = H"
proof
  from assms have "H⊆G" using group0_3_L2 by simp
  with assms show "H\<sinv> ⊆ H" using interval_inv group0_3_T3A by auto
  { fix x assume "x∈H"
    with assms have "(x¯)¯ ∈ {y¯.y∈H}" using group0_3_T3A by auto
    moreover from ‹x∈H› ‹H⊆G› have "(x¯)¯ = x" using group_inv_of_inv by auto
    ultimately have "x ∈ {y¯.y∈H}" by auto
    with ‹H⊆G› have "x ∈ H\<sinv>" using interval_inv by simp
  } thus "H ⊆ H\<sinv>" by auto
  from assms have "H {is closed under} P" using group0_3_L6 unfolding IsOpClosed_def by simp
  with assms have "H\<sdot>H ⊆ H" using subset_gr_op_cl group0_3_L2 by simp
  moreover
  { fix x assume "x∈H"
    with assms have "x∈G" using group0_3_L2 by auto
    from assms ‹H⊆G› ‹x∈H› have "x⋅𝟭 ∈ H\<sdot>H" using group0_3_L5 interval_prod by auto
    with ‹x∈G› have "x ∈ H\<sdot>H" using group0_2_L2 by simp
  } hence "H ⊆ H\<sdot>H" by auto
  ultimately show "H\<sdot>H = H" by auto
qed

text‹Inverse of a product two sets is a product of inverses with the reversed order.›

lemma (in group4) interval_prod_inv: assumes "A⊆G" "B⊆G"
  shows 
    "(A\<sdot>B)\<sinv> = {(x⋅y)¯.⟨x,y⟩ ∈ A×B}"
    "(A\<sdot>B)\<sinv> = {y¯⋅x¯.⟨x,y⟩ ∈ A×B}"
    "(A\<sdot>B)\<sinv> = (B\<sinv>)\<sdot>(A\<sinv>)"
proof -
  from assms have "(A\<sdot>B) ⊆ G" using interval_prod_closed by simp
  then have I: "(A\<sdot>B)\<sinv> = {z¯.z∈A\<sdot>B}" using interval_inv by simp
  show II: "(A\<sdot>B)\<sinv> = {(x⋅y)¯.⟨x,y⟩ ∈ A×B}"
  proof
    { fix p assume "p ∈ (A\<sdot>B)\<sinv>"
      with I obtain z where "p=z¯" and "z∈A\<sdot>B" by auto
      with assms obtain x y where "⟨x,y⟩ ∈ A×B" and "z=x⋅y" using interval_prod by auto
      with ‹p=z¯› have "p∈{(x⋅y)¯.⟨x,y⟩ ∈ A×B}" by auto
    } thus "(A\<sdot>B)\<sinv> ⊆ {(x⋅y)¯.⟨x,y⟩ ∈ A×B}" by blast
    { fix p assume "p∈{(x⋅y)¯.⟨x,y⟩ ∈ A×B}"
      then obtain x y where "x∈A" "y∈B" and "p=(x⋅y)¯" by auto
      with assms ‹(A\<sdot>B) ⊆ G› have "p∈(A\<sdot>B)\<sinv>" using interval_prod interval_inv
        by auto
    } thus "{(x⋅y)¯.⟨x,y⟩ ∈ A×B} ⊆ (A\<sdot>B)\<sinv>" by blast
  qed
  have "{(x⋅y)¯.⟨x,y⟩ ∈ A×B} = {y¯⋅x¯.⟨x,y⟩ ∈ A×B}"
  proof 
    { fix p assume "p ∈ {(x⋅y)¯.⟨x,y⟩ ∈ A×B}"
      then obtain x y where "x∈A" "y∈B" and "p=(x⋅y)¯" by auto
      with assms have "y¯⋅x¯ = (x⋅y)¯" using group_inv_of_two by auto
      with ‹p=(x⋅y)¯› have "p = y¯⋅x¯" by simp
      with ‹x∈A› ‹y∈B› have "p∈{y¯⋅x¯.⟨x,y⟩ ∈ A×B}" by auto
    } thus "{(x⋅y)¯.⟨x,y⟩ ∈ A×B} ⊆ {y¯⋅x¯.⟨x,y⟩ ∈ A×B}" by blast
    { fix p assume "p∈{y¯⋅x¯.⟨x,y⟩ ∈ A×B}"
      then obtain x y where "x∈A" "y∈B" and "p=y¯⋅x¯" by auto
      with assms have "p = (x⋅y)¯" using group_inv_of_two by auto
      with ‹x∈A› ‹y∈B› have "p ∈ {(x⋅y)¯.⟨x,y⟩ ∈ A×B}" by auto
    } thus "{y¯⋅x¯.⟨x,y⟩ ∈ A×B} ⊆ {(x⋅y)¯.⟨x,y⟩ ∈ A×B}" by blast
  qed
  with II show III: "(A\<sdot>B)\<sinv> = {y¯⋅x¯.⟨x,y⟩ ∈ A×B}" by simp
  have "{y¯⋅x¯.⟨x,y⟩ ∈ A×B} = (B\<sinv>)\<sdot>(A\<sinv>)"
  proof    
    { fix p assume "p∈{y¯⋅x¯.⟨x,y⟩ ∈ A×B}"
      then obtain x y where "x∈A" "y∈B" and "p=y¯⋅x¯" by auto
      with assms have "y¯ ∈ (B\<sinv>)" and "x¯ ∈ (A\<sinv>)"
        using interval_inv by auto
      with ‹p=y¯⋅x¯› have "p ∈ (B\<sinv>)\<sdot>(A\<sinv>)" using interval_inv_cl interval_prod
        by auto
    } thus "{y¯⋅x¯.⟨x,y⟩ ∈ A×B} ⊆ (B\<sinv>)\<sdot>(A\<sinv>)" by blast
    { fix p assume "p ∈ (B\<sinv>)\<sdot>(A\<sinv>)"
      then obtain y x where "y∈B\<sinv>" "x∈A\<sinv>" and "p=y⋅x"
        using interval_inv_cl interval_prod by auto
      with assms obtain x⇩₁ y⇩₁ where "x⇩₁ ∈ A" "y⇩₁ ∈ B" and "x=x⇩₁¯" "y=y⇩₁¯" using interval_inv
        by auto
      with ‹p=y⋅x› have "p ∈ {y¯⋅x¯.⟨x,y⟩ ∈ A×B}" by auto 
    } thus "(B\<sinv>)\<sdot>(A\<sinv>) ⊆ {y¯⋅x¯.⟨x,y⟩ ∈ A×B}" by blast
  qed
  with III show "(A\<sdot>B)\<sinv> = (B\<sinv>)\<sdot>(A\<sinv>)" by simp
qed

text‹ If $H,K$ are subgroups then $H\cdot K$ is a subgroup iff $H\cdot K = K\cdot H$. ›

theorem (in group4) prod_subgr_subgr: 
  assumes "IsAsubgroup(H,P)" and "IsAsubgroup(K,P)"
  shows "IsAsubgroup(H\<sdot>K,P) ⟷  H\<sdot>K = K\<sdot>H"
proof
  assume "IsAsubgroup(H\<sdot>K,P)"
  then have "(H\<sdot>K)\<sinv> = H\<sdot>K" using subgroup_inv_sq(1) by simp
  with assms show "H\<sdot>K = K\<sdot>H" using group0_3_L2 interval_prod_inv subgroup_inv_sq(1)
    by auto
next
  from assms have "H⊆G" and "K⊆G" using group0_3_L2 by auto
  have I: "H\<sdot>K ≠ 0"
  proof -
    let ?x = "𝟭" let ?y = "𝟭"
    from assms have "?x⋅?y ∈ (H\<sdot>K)" using group0_3_L5 group0_3_L2 interval_prod 
      by auto
    thus ?thesis by auto
  qed
  from ‹H⊆G› ‹K⊆G› have II: "H\<sdot>K ⊆ G" using interval_prod_closed by simp 
  assume "H\<sdot>K = K\<sdot>H"
  have III: "(H\<sdot>K){is closed under} P"
  proof -
    have "(H\<sdot>K)\<sdot>(H\<sdot>K) = H\<sdot>K"
    proof -
      from ‹H⊆G› ‹K⊆G› have "(H\<sdot>K)\<sdot>(H\<sdot>K) = H\<sdot>(K\<sdot>H)\<sdot>K"
        using interval_prod_rearr1 by simp
      also from ‹H\<sdot>K = K\<sdot>H› have "... = H\<sdot>(H\<sdot>K)\<sdot>K" by simp
      also from ‹H⊆G› ‹K⊆G› have "... = (H\<sdot>H)\<sdot>(K\<sdot>K)"
        using interval_prod_rearr1 by simp
      also from assms have "... = H\<sdot>K" using subgroup_inv_sq(2) by simp
      finally show ?thesis by simp
    qed
    with ‹H\<sdot>K ⊆ G› show ?thesis using subset_gr_op_cl by simp
  qed
  have IV: "∀x ∈ H\<sdot>K. x¯ ∈ H\<sdot>K"
  proof -
    { fix x assume "x ∈ H\<sdot>K" 
      with ‹H\<sdot>K ⊆ G› have "x¯ ∈ (H\<sdot>K)\<sinv>" using interval_inv by auto
      with assms ‹H⊆G› ‹K⊆G› ‹H\<sdot>K = K\<sdot>H› have "x¯ ∈ H\<sdot>K"
        using interval_prod_inv subgroup_inv_sq(1) by simp
    } thus ?thesis by auto
  qed
  from I II III IV show "IsAsubgroup(H\<sdot>K,P)" using group0_3_T3 by simp
qed

end