Theory Group_ZF_3

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES 
OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

header {*\isaheader{Group\_ZF\_3.thy}*}

theory Group_ZF_3 imports Group_ZF_2 Finite1 

begin

text{*In this theory we consider notions in group theory that are useful 
  for the construction of real numbers in the @{text "Real_ZF_x"} series of 
  theories.*}

section{*Group valued finite range functions*}

text{*In this section show that the group valued functions 
  $f : X\rightarrow G$, with the property that $f(X)$ is 
  a finite subset of $G$, is a group. Such functions play an important
  role in the construction of real numbers in the Real\_ZF\_x.thy series. *}

text{*The following proves the essential condition to show that the set of 
  finite range functions is
  closed with respect to the lifted group operation.*}

lemma (in group0) Group_ZF_3_1_L1: 
  assumes A1: "F = f {lifted to function space over} X"
  and 
  A2:"s ∈ FinRangeFunctions(X,G)" "r ∈  FinRangeFunctions(X,G)" 
  shows "F`<s,r> ∈ FinRangeFunctions(X,G)"
proof -;
  let ?q = "F`<s,r>"
  from A2 have T1:"s:X->G" "r:X->G"
    using FinRangeFunctions_def by auto;
  with A1 have T2:"?q : X->G"
    using group0_2_L1 monoid0.Group_ZF_2_1_L0
    by simp;
  moreover have "?q``(X) ∈ Fin(G)"
  proof -;
    from A2 have
      "{s`(x). x∈X} ∈ Fin(G)"
      "{r`(x). x∈X} ∈ Fin(G)"
      using Finite1_L18 by auto;
    with A1 T1 T2 show ?thesis using 
      group_oper_assocA Finite1_L15 Group_ZF_2_1_L3 func_imagedef
      by simp;
  qed;
  ultimately show ?thesis using FinRangeFunctions_def
    by simp;
qed;

text{*The set of group valued finite range functions is closed with respect 
  to the lifted group operation. *}

lemma (in group0) Group_ZF_3_1_L2:
  assumes A1: "F = f {lifted to function space over} X"
  shows "FinRangeFunctions(X,G) {is closed under} F"
proof -;
  let ?A = "FinRangeFunctions(X,G)"
  from A1 have "∀x∈?A. ∀y∈?A. F`<x,y> ∈ ?A"
    using Group_ZF_3_1_L1 by simp;
  then show ?thesis using IsOpClosed_def by simp;
qed;

text{*A composition of a finite range function with the group inverse is
  a finite range function.*}

lemma (in group0) Group_ZF_3_1_L3: 
  assumes A1: "s ∈ FinRangeFunctions(X,G)"
  shows "GroupInv(G,f) O s ∈ FinRangeFunctions(X,G)"
  using groupAssum prems group0_2_T2 Finite1_L20 by simp;

text{*The set of finite range functions is s subgroup of the lifted group.*}

theorem Group_ZF_3_1_T1: 
  assumes A1:"IsAgroup(G,f)" 
  and A2:"F = f {lifted to function space over} X"
  and A3:"X≠0"
  shows "IsAsubgroup(FinRangeFunctions(X,G),F)"
proof -;
  let ?e = "TheNeutralElement(G,f)"
  let ?S = "FinRangeFunctions(X,G)"
  from A1 have T1:"group0(G,f)" using group0_def 
    by simp;
  with A1 A2 have T2:"group0(X->G,F)"
    using group0.Group_ZF_2_1_T2 group0_def
    by simp;
  moreover have "?S ≠ 0"
  proof -;   
    from T1 A3 have 
      "ConstantFunction(X,?e) ∈ ?S"
      using group0.group0_2_L1 monoid0.group0_1_L3
        Finite1_L17 by simp;
    thus ?thesis by auto;
  qed;
  moreover have "?S ⊆ X->G"
    using FinRangeFunctions_def by auto;
  moreover from A2 T1 have
    "?S {is closed under} F"
    using group0.Group_ZF_3_1_L2
    by simp;
  moreover from A1 A2 T1 have
    "∀s ∈ ?S. GroupInv(X->G,F)`(s) ∈ ?S"
    using FinRangeFunctions_def group0.Group_ZF_2_1_L6
      group0.Group_ZF_3_1_L3 by simp;
  ultimately show ?thesis
    using group0.group0_3_T3 by simp;
qed;

section{*Almost homomorphisms*}

text{*An almost homomorphism is a group valued function 
  defined on a monoid $M$ 
  with the property that the set $\{ f(m+n)-f(m)-f(n)\}_{m,n \in M}$ is finite.
  This term is used by R. D. Arthan in "The Eudoxus Real Numbers". We use this
  term in the general group context and use the A`Campo's term "slopes" 
  (see his "A natural construction for the real numbers") to mean
  an almost homomorphism mapping interegers into themselves. 
  We consider almost homomorphisms because we use slopes to 
  define real numbers in the @{text "Real_ZF_x"} series. *}

text{*HomDiff is an acronym for "homomorphism difference". 
  This is the expression
  $s(mn)(s(m)s(n))^{-1}$, or $s(m+n)-s(m)-s(n)$ in the additive notation.
  It is equal to the neutral element of the group if $s$ is a homomorphism.
  Almost homomorphisms are defined as those maps 
  $s:G\rightarrow G$ such that the 
  homomorphism difference takes only finite number of values on $G\times G$.
  Although almost homomorphisms can be in principle defined on a monoid with 
  values in a group, we limit ourselves to the situation where the monoid and
  the group are the same. 
  The set of slopes related to a specific group is called 
  AlmostHoms$(G,f)$. AlHomOp1$(G,f)$ is the group operation on almost 
  homomorphisms defined in a natural way 
  by $(s\cdot r)(n) = s(n)\cdot r(n)$. In the terminology defined in 
  func1.thy this is the group operation $f$ (on $G$) 
  lifted to the function space $G\rightarrow G$ and restricted to the set 
  AlmostHoms$(G,f)$.
  We also define a composition (binary) operator on almost homomorphisms in 
  a natural way. We call that operator AlHomOp2 - the second operation 
  on almost homomorphisms. 
  Composition of almost homomorphisms is used to define 
  multiplication of real numbers in Real\_ZF\_x.thy series.*}

constdefs
  "HomDiff(G,f,s,x) ≡ 
  f`⟨s`(f`<fst(x),snd(x)>) , 
  (GroupInv(G,f)`(f`<s`(fst(x)),s`(snd(x))>))⟩"

  "AlmostHoms(G,f) ≡ 
  {s ∈ G->G.{HomDiff(G,f,s,x). x ∈ G×G } ∈ Fin(G)}"

  "AlHomOp1(G,f) ≡ 
  restrict(f {lifted to function space over} G,
  AlmostHoms(G,f)×AlmostHoms(G,f))"
 
  "AlHomOp2(G,f) ≡ 
  restrict(Composition(G),AlmostHoms(G,f)×AlmostHoms(G,f))"
  
text{*This lemma provides more readable notation for the HomDiff
  definition. Not really intended to be used in proofs, but just to see the
  definition in the notation defined in the group0 locale.*}

lemma (in group0) Group_ZF_3_2_L1:
  shows "HomDiff(G,f,s,<m,n>) = s`(m·n)·(s`(m)·s`(n))¯"
  using HomDiff_def by simp;

text{*The next lemma shows the set from the definition of almost 
  homomorphism in a different form.*}

lemma (in group0) Group_ZF_3_2_L1A:
  "{HomDiff(G,f,s,x). x ∈ G×G } = {s`(m·n)·(s`(m)·s`(n))¯. <m,n> ∈ G×G}"
proof -
  have "∀m∈G.∀n∈G. HomDiff(G,f,s,<m,n>) = s`(m·n)·(s`(m)·s`(n))¯"
    using Group_ZF_3_2_L1 by simp;
  then show ?thesis by (rule ZF1_1_L4A);
qed;

text{*Let's define some notation. We inherit the notation and assumptions 
  from the group0 context (locale) 
  and add some. We will use AH to denote the set of almost homomorphisms.
  $\sim$ is the inverse (negative if the group is the group of integers) of 
  almost homomorphisms, $(\sim p)(n)= p(n)^{-1}$.  
  $\delta $ will denote the homomorphism difference specific
  for the group (HomDiff$(G,f)$). The notation $s \approx r$ will mean that
  $s,r$ are almost equal, that is they are in the equivalence relation 
  defined by the group of finite range
  functions (that is a normal subgroup of almost homomorphisms, 
  if the group is abelian). We show that 
  this is equivalent to the set $\{ s(n)\cdot r(n)^{-1}: n\in G\}$ being
  finite.
  We also add an assumption that the
  $G$ is abelian as many needed properties do not hold without that. *}

locale group1 = group0 +
  assumes isAbelian: "f {is commutative on} G"

  fixes AH 
  defines AH_def [simp]: "AH ≡ AlmostHoms(G,f)"

  fixes Op1 
  defines Op1_def [simp]: "Op1 ≡ AlHomOp1(G,f)"
 
  fixes Op2
  defines Op2_def [simp]: "Op2 ≡ AlHomOp2(G,f)"
  
  fixes FR 
  defines FR_def [simp]: "FR ≡ FinRangeFunctions(G,G)"

  fixes neg :: "i=>i" ("∼_" [90] 91)
  defines neg_def [simp]: "∼s ≡ GroupInv(G,f) O s"

  fixes δ
  defines δ_def [simp]: "δ(s,x) ≡ HomDiff(G,f,s,x)"

  fixes AHprod (infix "•" 69)
  defines AHprod_def [simp]: "s • r ≡  AlHomOp1(G,f)`<s,r>"

  fixes AHcomp (infix "o" 70)
  defines AHcomp_def [simp]: "s o r ≡  AlHomOp2(G,f)`<s,r>"

  fixes AlEq (infix "≈" 68)
  defines AlEq_def [simp]: 
  "s ≈ r ≡ <s,r> ∈ QuotientGroupRel(AH,Op1,FR)"


text{*HomDiff is a homomorphism on the lifted group structure.*}

lemma (in group1) Group_ZF_3_2_L1: 
  assumes A1: "s:G->G"  "r:G->G"
  and A2: "x ∈ G×G"
  and A3: "F = f {lifted to function space over} G"
  shows "δ(F`<s,r>,x) = δ(s,x)·δ(r,x)"
proof -;
  let ?p = "F`<s,r>"
  from A2 obtain m n where
    D1: "x = <m,n>" "m∈G" "n∈G" 
    by auto;
  then have T1:"m·n ∈ G"
    using group0_2_L1 monoid0.group0_1_L1 by simp;
  with A1 D1 have T2:
    "s`(m)∈G" "s`(n)∈G" "r`(m)∈G" 
    "r`(n)∈G" "s`(m·n)∈G" "r`(m·n)∈G"
    using apply_funtype by auto;
  from A3 A1 have T3:"?p : G->G"
    using group0_2_L1 monoid0.Group_ZF_2_1_L0
    by simp;
  from D1 T3 have
    "δ(?p,x) = ?p`(m·n)·((?p`(n))¯·(?p`(m))¯)"
    using Group_ZF_3_2_L1 apply_funtype group_inv_of_two 
    by simp;
  also from A3 A1 D1 T1 isAbelian T2 have
    "… = δ(s,x)· δ(r,x)"
    using Group_ZF_2_1_L3 group0_4_L3  Group_ZF_3_2_L1
    by simp;
  finally show ?thesis by simp;
qed;

text{*The group operation lifted to the function space over $G$ preserves
  almost homomorphisms.*}

lemma (in group1) Group_ZF_3_2_L2: assumes A1: "s ∈ AH" "r ∈ AH"
  and A2: "F = f {lifted to function space over} G"
  shows "F`<s,r> ∈ AH"
proof -
  let ?p = "F`<s,r>"
  from A1 A2 have "?p : G->G"
    using AlmostHoms_def group0_2_L1 monoid0.Group_ZF_2_1_L0
    by simp;
  moreover have
    "{δ(?p,x). x ∈ G×G} ∈ Fin(G)"
  proof -;
    from A1 have
      "{δ(s,x). x ∈ G×G } ∈ Fin(G)" 
      "{δ(r,x). x ∈ G×G } ∈ Fin(G)"
      using AlmostHoms_def by auto;
    with groupAssum A1 A2 show ?thesis
      using IsAgroup_def IsAmonoid_def IsAssociative_def
      Finite1_L15 AlmostHoms_def Group_ZF_3_2_L1
      by auto;
  qed;
  ultimately show ?thesis using AlmostHoms_def
    by simp;
qed;

text{*The set of almost homomorphisms is closed under the 
  lifted group operation.*}

lemma (in group1) Group_ZF_3_2_L3:
  assumes "F = f {lifted to function space over} G"
  shows "AH {is closed under} F"
  using prems IsOpClosed_def Group_ZF_3_2_L2 by simp;

text{*The terms in the homomorphism difference for a function
  are in the group.*}

lemma (in group1) Group_ZF_3_2_L4:
  assumes "s:G->G" and "m∈G"  "n∈G"
  shows 
  "m·n ∈ G" 
  "s`(m·n) ∈ G"
  "s`(m) ∈ G" "s`(n) ∈ G"
  "δ(s,<m,n>) ∈ G"
  "s`(m)·s`(n) ∈ G"
  using prems group_op_closed inverse_in_group  
    apply_funtype HomDiff_def by auto;

text{*It is handy to have a version of @{text " Group_ZF_3_2_L4"}
  specifically for almost homomorphisms.*}
  
corollary (in group1) Group_ZF_3_2_L4A:  
  assumes "s ∈ AH" and "m∈G"  "n∈G"
  shows "m·n ∈ G" 
  "s`(m·n) ∈ G"
  "s`(m) ∈ G" "s`(n) ∈ G"
  "δ(s,<m,n>) ∈ G"
  "s`(m)·s`(n) ∈ G"
  using prems AlmostHoms_def Group_ZF_3_2_L4
  by auto;

text{*The terms in the homomorphism difference are in the group, 
  a different form.*}

lemma (in group1) Group_ZF_3_2_L4B:  
  assumes A1:"s ∈ AH" and A2:"x∈G×G"
  shows "fst(x)·snd(x) ∈ G" 
  "s`(fst(x)·snd(x)) ∈ G"
  "s`(fst(x)) ∈ G" "s`(snd(x)) ∈ G"
  "δ(s,x) ∈ G"
  "s`(fst(x))·s`(snd(x)) ∈ G"
proof -;
  let ?m = "fst(x)" 
  let ?n = "snd(x)";
  from A1 A2 show 
    "?m·?n ∈ G"  "s`(?m·?n) ∈ G" 
    "s`(?m) ∈ G" "s`(?n) ∈ G"
    "s`(?m)·s`(?n) ∈ G"
    using Group_ZF_3_2_L4A
    by auto;
  from A1 A2 have "δ(s,<?m,?n>) ∈ G" using Group_ZF_3_2_L4A
    by simp;
  moreover from A2 have "<?m,?n> = x" by auto;
  ultimately show "δ(s,x) ∈ G" by simp;
qed;

text{*What are the values of the inverse of an almost homomorphism?*}

lemma (in group1) Group_ZF_3_2_L5:
  assumes "s ∈ AH" and "n∈G"
  shows "(∼s)`(n) = (s`(n))¯"
  using prems AlmostHoms_def comp_fun_apply by auto;

text{*Homomorphism difference commutes with the inverse for almost
  homomorphisms.*}
  
lemma (in group1) Group_ZF_3_2_L6:  
  assumes A1:"s ∈ AH" and A2:"x∈G×G"
  shows "δ(∼s,x) = (δ(s,x))¯"
proof -;
  let ?m = "fst(x)"
  let ?n = "snd(x)"
  have "δ(∼s,x) = (∼s)`(?m·?n)·((∼s)`(?m)·(∼s)`(?n))¯"
    using HomDiff_def by simp;
  from A1 A2 isAbelian show ?thesis
    using Group_ZF_3_2_L4B HomDiff_def 
      Group_ZF_3_2_L5 group0_4_L4A
    by simp;
qed;

text{*The inverse of an almost homomorphism  maps the group into itself.*}

lemma (in group1) Group_ZF_3_2_L7: 
  assumes "s ∈ AH"
  shows "∼s : G->G"
  using groupAssum prems AlmostHoms_def group0_2_T2 comp_fun by auto;

text{*The inverse of an almost homomorphism is an almost homomorphism.*}

lemma (in group1) Group_ZF_3_2_L8:
  assumes A1: "F = f {lifted to function space over} G"
  and A2: "s ∈ AH"
  shows "GroupInv(G->G,F)`(s) ∈ AH"
proof -;
  from A2 have "{δ(s,x). x ∈ G×G} ∈ Fin(G)"
    using AlmostHoms_def by simp;
  with groupAssum  have
    "GroupInv(G,f)``{δ(s,x). x ∈ G×G} ∈ Fin(G)"
    using group0_2_T2 Finite1_L6A by blast;
  moreover have 
     "GroupInv(G,f)``{δ(s,x). x ∈ G×G} =
    {(δ(s,x))¯. x ∈ G×G}"
  proof -;
    from groupAssum have 
      "GroupInv(G,f) : G->G"
      using group0_2_T2 by simp;
    moreover from A2 have 
      "∀x∈G×G. δ(s,x)∈G"
      using Group_ZF_3_2_L4B by simp;
    ultimately show ?thesis 
      using func1_1_L17 by simp;
  qed
  ultimately have "{(δ(s,x))¯. x ∈ G×G} ∈ Fin(G)"
    by simp;
  moreover from A2 have
    "{(δ(s,x))¯. x ∈ G×G} = {δ(∼s,x). x ∈ G×G}"
    using Group_ZF_3_2_L6 by simp;
  ultimately have "{δ(∼s,x). x ∈ G×G} ∈ Fin(G)"
    by simp;
  with A2 groupAssum A1 show ?thesis
    using Group_ZF_3_2_L7 AlmostHoms_def Group_ZF_2_1_L6
    by simp;
qed;

text{*The function that assigns the neutral element everywhere 
  is an almost homomorphism. *}

lemma (in group1) Group_ZF_3_2_L9:
  "ConstantFunction(G,\<one>) ∈ AH"
  "AH≠0"
proof -;
  let ?z = "ConstantFunction(G,\<one>)"
  have "G×G≠0" using group0_2_L1 monoid0.group0_1_L3A
    by blast;
  moreover have "∀x∈G×G. δ(?z,x) = \<one>"
  proof;
    fix x assume A1:"x ∈ G × G"
    then obtain m n where "x = <m,n>" "m∈G" "n∈G"
      by auto;
    then show "δ(?z,x) = \<one>"
      using group0_2_L1 monoid0.group0_1_L1
        func1_3_L2 HomDiff_def group0_2_L2 
        group_inv_of_one by simp;
  qed;
  ultimately have "{δ(?z,x). x∈G×G} = {\<one>}" by (rule ZF1_1_L5);
  then show "?z ∈ AH" using group0_2_L2 Finite1_L16
    func1_3_L1 group0_2_L2 AlmostHoms_def by simp;
  then show "AH≠0" by auto;
qed;

text{*If the group is abelian, then almost homomorphisms form a 
  subgroup of the lifted group.*}

lemma Group_ZF_3_2_L10:
  assumes A1: "IsAgroup(G,f)"
  and A2: "f {is commutative on} G"
  and A3: "F = f {lifted to function space over} G"
  shows "IsAsubgroup(AlmostHoms(G,f),F)"
proof -;
  let ?AH = "AlmostHoms(G,f)"
  from A2 A1 have T1:"group1(G,f)"
    using group1_axioms.intro group0_def group1_def
    by simp;
  from A1 A3 have "group0(G->G,F)"
    using group0_def group0.Group_ZF_2_1_T2 by simp;
  moreover from T1 have "?AH≠0"
    using group1.Group_ZF_3_2_L9 by simp;
  moreover have T2:"?AH ⊆ G->G"
    using AlmostHoms_def by auto;
  moreover from T1 A3 have 
    "?AH {is closed under} F"
    using group1.Group_ZF_3_2_L3 by simp;
  moreover from T1 A3 have
    "∀s∈?AH. GroupInv(G->G,F)`(s) ∈ ?AH"
    using group1.Group_ZF_3_2_L8 by simp;
  ultimately show "IsAsubgroup(AlmostHoms(G,f),F)"
    using group0.group0_3_T3 by simp
qed;

text{*If the group is abelian, then almost homomorphisms form a group
  with the first operation, hence we can use theorems proven in group0
  context aplied to this group.*}

lemma (in group1) Group_ZF_3_2_L10A: 
  shows "IsAgroup(AH,Op1)" "group0(AH,Op1)"
    using groupAssum isAbelian Group_ZF_3_2_L10 IsAsubgroup_def 
      AlHomOp1_def group0_def by auto;

text{*The group of almost homomorphisms is abelian*}

lemma Group_ZF_3_2_L11: assumes A1: "IsAgroup(G,f)"
  and A2: "f {is commutative on} G"
  shows 
  "IsAgroup(AlmostHoms(G,f),AlHomOp1(G,f))"
  "AlHomOp1(G,f) {is commutative on} AlmostHoms(G,f)"
proof-
  let ?AH = "AlmostHoms(G,f)"
  let ?F = "f {lifted to function space over} G"
  from A1 A2 have "IsAsubgroup(?AH,?F)"
    using Group_ZF_3_2_L10 by simp;
  then show "IsAgroup(?AH,AlHomOp1(G,f))"
    using IsAsubgroup_def AlHomOp1_def by simp;
  from A1 have "?F : (G->G)×(G->G)->(G->G)"
    using IsAgroup_def monoid0_def monoid0.Group_ZF_2_1_L0A
    by simp;
  moreover have "?AH ⊆ G->G"
    using AlmostHoms_def by auto
  moreover from A1 A2 have
    "?F {is commutative on} (G->G)"
    using group0_def group0.Group_ZF_2_1_L7
    by simp;
  ultimately show 
    "AlHomOp1(G,f){is commutative on} ?AH"
    using func_ZF_4_L1 AlHomOp1_def by simp;
qed;

text{*The first operation on homomorphisms acts in a natural way on its 
  operands.*}

lemma (in group1) Group_ZF_3_2_L12: 
  assumes "s∈AH"  "r∈AH" and "n∈G"
  shows "(s•r)`(n) = s`(n)·r`(n)"
  using prems AlHomOp1_def restrict AlmostHoms_def Group_ZF_2_1_L3
  by simp;

text{* What is the group inverse in the group of almost homomorphisms? *}

lemma (in group1) Group_ZF_3_2_L13: 
  assumes A1: "s∈AH"
  shows 
  "GroupInv(AH,Op1)`(s) = GroupInv(G,f) O s"
  "GroupInv(AH,Op1)`(s) ∈ AH"
  "GroupInv(G,f) O s ∈ AH"
proof -;
  let ?F = "f {lifted to function space over} G"
  from groupAssum isAbelian have "IsAsubgroup(AH,?F)" 
    using Group_ZF_3_2_L10 by simp;
  with A1 show I: "GroupInv(AH,Op1)`(s) = GroupInv(G,f) O s"
    using AlHomOp1_def Group_ZF_2_1_L6A by simp;
  from A1 show "GroupInv(AH,Op1)`(s) ∈ AH"
    using Group_ZF_3_2_L10A group0.inverse_in_group by simp;
  with I show "GroupInv(G,f) O s ∈ AH" by simp
qed;

text{*The group inverse in the group of almost homomorphisms acts in a 
  natural way on its operand.*}

lemma (in group1) Group_ZF_3_2_L14:
  assumes "s∈AH" and "n∈G"
  shows "(GroupInv(AH,Op1)`(s))`(n) = (s`(n))¯"
  using isAbelian prems Group_ZF_3_2_L13 AlmostHoms_def comp_fun_apply
  by auto;

text{*The next lemma states that if $s,r$ are almost homomorphisms, then
  $s\cdot r^{-1}$ is also an almost homomorphism.*}

lemma Group_ZF_3_2_L15: assumes "IsAgroup(G,f)"
  and "f {is commutative on} G"
  and "AH = AlmostHoms(G,f)" "Op1 = AlHomOp1(G,f)"
  and "s ∈ AH"  "r ∈ AH"
  shows 
  "Op1`<s,r> ∈ AH"
  "GroupInv(AH,Op1)`(r) ∈ AH"
  "Op1`<s,GroupInv(AH,Op1)`(r)> ∈ AH"
  using prems group0_def group1_axioms.intro group1_def
      group1.Group_ZF_3_2_L10A group0.group0_2_L1 
      monoid0.group0_1_L1 group0.inverse_in_group by auto

text{*A version of @{text "Group_ZF_3_2_L15"} formulated in notation
  used in @{text "group1"} context. States that the product of almost
  homomorphisms is an almost homomorphism and the the product
  of an almost homomorphism with a (pointwise) inverse of an almost 
  homomorphism is an almost homomorphism.*}

corollary (in group1) Group_ZF_3_2_L16: assumes "s ∈ AH"  "r ∈ AH"
  shows "s•r ∈ AH"   "s•(∼r) ∈ AH"
  using prems isAbelian group0_def group1_axioms.intro group1_def
  Group_ZF_3_2_L15  Group_ZF_3_2_L13 by auto;

section{*The classes of almost homomorphisms*}

text{*In the Real\_ZF\_x series we define real numbers as a quotient
  of the group of integer almost homomorphisms by the integer finite range
  functions. In this section we setup the background for that in the general
  group context.*}

text{*Finite range functions are almost homomorphisms.*}

lemma (in group1) Group_ZF_3_3_L1: "FR ⊆ AH"
proof;
  fix s assume A1:"s ∈ FR"
  then have T1:"{s`(n). n ∈ G} ∈ Fin(G)"
    "{s`(fst(x)). x∈G×G} ∈ Fin(G)"
    "{s`(snd(x)). x∈G×G} ∈ Fin(G)"
    using Finite1_L18 Finite1_L6B by auto;
  have "{s`(fst(x)·snd(x)). x ∈ G×G} ∈ Fin(G)"
  proof -;
    have "∀x∈G×G. fst(x)·snd(x) ∈ G"
      using group0_2_L1 monoid0.group0_1_L1 by simp;
    moreover from T1 have "{s`(n). n ∈ G} ∈ Fin(G)" by simp;
    ultimately show ?thesis by (rule Finite1_L6B);
  qed
  moreover have 
    "{(s`(fst(x))·s`(snd(x)))¯. x∈G×G} ∈ Fin(G)"
  proof -;
    have "∀g∈G. g¯ ∈ G" using inverse_in_group 
      by simp
    moreover from T1 have 
      "{s`(fst(x))·s`(snd(x)). x∈G×G} ∈ Fin(G)"
      using group_oper_assocA  Finite1_L15 by simp;
    ultimately show ?thesis 
      by (rule Finite1_L6C);
  qed;
  ultimately have "{δ(s,x). x∈G×G} ∈ Fin(G)"
    using HomDiff_def Finite1_L15  group_oper_assocA 
    by simp;
  with A1 show "s ∈ AH" 
    using FinRangeFunctions_def AlmostHoms_def 
    by simp;
qed;

text{*Finite range functions valued in an abelian group form a normal 
  subgroup of almost homomorphisms.*}

lemma Group_ZF_3_3_L2: assumes A1:"IsAgroup(G,f)"
  and A2:"f {is commutative on} G"
  shows
  "IsAsubgroup(FinRangeFunctions(G,G),AlHomOp1(G,f))"
  "IsAnormalSubgroup(AlmostHoms(G,f),AlHomOp1(G,f),
  FinRangeFunctions(G,G))"
proof -;
  let ?H1 = "AlmostHoms(G,f)"
  let ?H2 = "FinRangeFunctions(G,G)"
  let ?F = "f {lifted to function space over} G"
  from A1 A2 have T1:"group0(G,f)"
    "monoid0(G,f)" "group1(G,f)"
    using group0_def group0.group0_2_L1  
      group1_axioms.intro group1_def
    by auto;
  with A1 A2 have "IsAgroup(G->G,?F)"
    "IsAsubgroup(?H1,?F)" "IsAsubgroup(?H2,?F)"
    using group0.Group_ZF_2_1_T2 Group_ZF_3_2_L10
      monoid0.group0_1_L3A Group_ZF_3_1_T1
    by auto;
  then have 
    "IsAsubgroup(?H1∩?H2,restrict(?F,?H1×?H1))"
    using group0_3_L7 by simp;
  moreover from T1 have "?H1∩?H2 = ?H2"
    using group1.Group_ZF_3_3_L1 by auto;
  ultimately show "IsAsubgroup(?H2,AlHomOp1(G,f))"
    using AlHomOp1_def by simp;
  with A1 A2 show "IsAnormalSubgroup(AlmostHoms(G,f),AlHomOp1(G,f),
    FinRangeFunctions(G,G))"
    using Group_ZF_3_2_L11 Group_ZF_2_4_L6
    by simp;
qed;

text{*The group of almost homomorphisms divided by the subgroup of finite
  range functions is an abelian group.*}

theorem (in group1) Group_ZF_3_3_T1:
  shows 
  "IsAgroup(AH//QuotientGroupRel(AH,Op1,FR),QuotientGroupOp(AH,Op1,FR))"
  and
  "QuotientGroupOp(AH,Op1,FR) {is commutative on}
  (AH//QuotientGroupRel(AH,Op1,FR))"
  using groupAssum isAbelian Group_ZF_3_3_L2 Group_ZF_3_2_L10A 
    Group_ZF_2_4_T1 Group_ZF_3_2_L10A Group_ZF_3_2_L11  
    Group_ZF_3_3_L2 IsAnormalSubgroup_def Group_ZF_2_4_L6 by auto;

text{*It is useful to have a direct statement that the 
  quotient group relation is an equivalence relation for the group of AH and
  subgroup FR.*}

lemma (in group1) Group_ZF_3_3_L3:
  "QuotientGroupRel(AH,Op1,FR) ⊆ AH × AH"
  "equiv(AH,QuotientGroupRel(AH,Op1,FR))"
  using groupAssum isAbelian QuotientGroupRel_def 
    Group_ZF_3_3_L2 Group_ZF_3_2_L10A group0.Group_ZF_2_4_L3 
  by auto;

text{*The "almost equal" relation is symmetric.*}
(* simp works but 100 search depth *)
lemma (in group1) Group_ZF_3_3_L3A: assumes A1: "s≈r"
  shows "r≈s"
proof -
  let ?R = "QuotientGroupRel(AH,Op1,FR)"
  from A1 have "equiv(AH,?R)" and "⟨s,r⟩ ∈ ?R"
    using Group_ZF_3_3_L3 by auto;
  then have "⟨r,s⟩ ∈ ?R" by (rule equiv_is_sym);
  then show "r≈s" by simp;
qed;

text{*Although we have bypassed this fact when proving that 
  group of almost homomorphisms divided by the subgroup of finite
  range functions is a group, it is still useful to know directly 
  that the first group operation on AH is congruent with respect to the
  quotient group relation.*}

lemma (in group1) Group_ZF_3_3_L4: 
  shows "Congruent2(QuotientGroupRel(AH,Op1,FR),Op1)"
  using groupAssum isAbelian Group_ZF_3_2_L10A Group_ZF_3_3_L2 
    Group_ZF_2_4_L5A by simp;

text{*The class of an almost homomorphism $s$ is the neutral element
  of the quotient group of almost homomorphisms iff $s$ is a finite range
  function.*}

lemma (in group1) Group_ZF_3_3_L5: assumes "s ∈ AH" and
  "r = QuotientGroupRel(AH,Op1,FR)" and
  "TheNeutralElement(AH//r,QuotientGroupOp(AH,Op1,FR)) = e"
  shows "r``{s} = e <-> s ∈ FR"
  using groupAssum isAbelian prems Group_ZF_3_2_L11 
    group0_def Group_ZF_3_3_L2 group0.Group_ZF_2_4_L5E
  by simp;

text{*The group inverse of a class of an almost homomorphism $f$
  is the class of the inverse of $f$.*}

lemma (in group1) Group_ZF_3_3_L6: 
  assumes A1: "s ∈ AH"  and 
  "r = QuotientGroupRel(AH,Op1,FR)" and 
  "F = ProjFun2(AH,r,Op1)"
  shows "r``{∼s} = GroupInv(AH//r,F)`(r``{s})"
proof -
  from groupAssum isAbelian prems have
    "r``{GroupInv(AH, Op1)`(s)} = GroupInv(AH//r,F)`(r `` {s})"
    using Group_ZF_3_2_L10A Group_ZF_3_3_L2 QuotientGroupOp_def
      group0.Group_ZF_2_4_L7 by simp;
  with A1 show ?thesis using Group_ZF_3_2_L13
    by simp;
qed;

section{*Compositions of almost homomorphisms*}

text{*The goal of this section is to establish some facts about composition
  of almost homomorphisms. needed for the real numbers construction in 
  Real\_ZF\_x.thy serias. In particular we show that the set of almost 
  homomorphisms is closed under composition and that composition
  is congruent with respect to the equivalence relation defined by the group
  of finite range functions (a normal subgroup of almost homomorphisms). *}

text{*The next formula restates the definition of the homomorphism 
  difference to express the value an almost homomorphism on a product.*}

lemma (in group1) Group_ZF_3_4_L1: 
  assumes "s∈AH" and  "m∈G"  "n∈G" 
  shows "s`(m·n) = s`(m)·s`(n)·δ(s,<m,n>)"
  using isAbelian prems Group_ZF_3_2_L4A HomDiff_def group0_4_L5
  by simp;

text{*What is the value of a composition of almost homomorhisms?*}

lemma (in group1) Group_ZF_3_4_L2:
  assumes "s∈AH"  "r∈AH" and "m∈G"
  shows "(sor)`(m) = s`(r`(m))"  "s`(r`(m)) ∈ G"
  using prems AlmostHoms_def func_ZF_5_L3 restrict AlHomOp2_def
    apply_funtype by auto;

text{*What is the homomorphism difference of a composition?*}

lemma (in group1) Group_ZF_3_4_L3:
  assumes A1: "s∈AH"  "r∈AH" and A2: "m∈G"  "n∈G"
  shows "δ(sor,<m,n>) = 
  δ(s,<r`(m),r`(n)>)·s`(δ(r,<m,n>))·δ(s,<r`(m)·r`(n),δ(r,<m,n>)>)"
proof -
  from A1 A2 have T1:
    "s`(r`(m))· s`(r`(n)) ∈ G"
    "δ(s,<r`(m),r`(n)>)∈ G" "s`(δ(r,<m,n>)) ∈G" 
    "δ(s,<(r`(m)·r`(n)),δ(r,<m,n>)>) ∈ G"
    using Group_ZF_3_4_L2 AlmostHoms_def apply_funtype 
      Group_ZF_3_2_L4A group0_2_L1 monoid0.group0_1_L1
    by auto;
  from A1 A2 have "δ(sor,<m,n>) =
    s`(r`(m)·r`(n)·δ(r,<m,n>))·(s`((r`(m)))·s`(r`(n)))¯"
    using HomDiff_def group0_2_L1 monoid0.group0_1_L1 Group_ZF_3_4_L2
      Group_ZF_3_4_L1 by simp;
  moreover from A1 A2 have
    "s`(r`(m)·r`(n)·δ(r,<m,n>)) =
    s`(r`(m)·r`(n))·s`(δ(r,<m,n>))·δ(s,<(r`(m)·r`(n)),δ(r,<m,n>)>)"
    "s`(r`(m)·r`(n)) = s`(r`(m))·s`(r`(n))·δ(s,<r`(m),r`(n)>)"
    using Group_ZF_3_2_L4A Group_ZF_3_4_L1 by auto;
  moreover from T1 isAbelian have
    "s`(r`(m))·s`(r`(n))·δ(s,<r`(m),r`(n)>)·
    s`(δ(r,<m,n>))·δ(s,<(r`(m)·r`(n)),δ(r,<m,n>)>)·
    (s`((r`(m)))·s`(r`(n)))¯ = 
    δ(s,<r`(m),r`(n)>)·s`(δ(r,<m,n>))·δ(s,<(r`(m)·r`(n)),δ(r,<m,n>)>)" 
    using group0_4_L6C by simp;
  ultimately show ?thesis by simp;
qed;
  
text{*What is the homomorphism difference of a composition (another form)?
  Here we split the homomorphism difference of a composition 
  into a product of three factors.
  This will help us in proving that the range of homomorphism difference
  for the composition is finite, as each factor has finite range.*}

lemma (in group1) Group_ZF_3_4_L4:
  assumes A1: "s∈AH"  "r∈AH" and A2: "x ∈ G×G"
  and A3:
  "A = δ(s,<r`(fst(x)),r`(snd(x))>)"
  "B = s`(δ(r,x))"
  "C = δ(s,<(r`(fst(x))·r`(snd(x))),δ(r,x)>)"
  shows "δ(sor,x) = A·B·C"
proof -;
  let ?m = "fst(x)"
  let ?n = "snd(x)"
  from A1 have "s∈AH" "r∈AH" .
  moreover from A2 have "?m∈G" "?n∈G"
    by auto
  ultimately have
    "δ(sor,<?m,?n>) = 
    δ(s,<r`(?m),r`(?n)>)·s`(δ(r,<?m,?n>))·
    δ(s,<(r`(?m)·r`(?n)),δ(r,<?m,?n>)>)"
    by (rule Group_ZF_3_4_L3);
  with A1 A2 A3 show ?thesis
    by auto;
qed;

text{*The range of the homomorphism difference of a composition
  of two almost homomorphisms is finite. This is the essential condition
  to show that a composition of almost homomorphisms is an almost 
  homomorphism.*}

lemma (in group1) Group_ZF_3_4_L5:
  assumes A1: "s∈AH"  "r∈AH"
  shows "{δ(Composition(G)`<s,r>,x). x ∈ G×G} ∈ Fin(G)"
proof -;
  from A1 have 
    "∀x∈G×G. <r`(fst(x)),r`(snd(x))> ∈ G×G"
    using Group_ZF_3_2_L4B by simp;
  moreover from A1 have 
    "{δ(s,x). x∈G×G} ∈ Fin(G)"
    using AlmostHoms_def by simp;
  ultimately have 
    "{δ(s,<r`(fst(x)),r`(snd(x))>). x∈G×G} ∈ Fin(G)"
    by (rule Finite1_L6B);
  moreover have "{s`(δ(r,x)). x∈G×G} ∈ Fin(G)"
  proof -;
    from A1 have "∀m∈G. s`(m) ∈ G" 
      using AlmostHoms_def apply_funtype by auto;
    moreover from A1 have "{δ(r,x). x∈G×G} ∈ Fin(G)"
      using AlmostHoms_def by simp;
    ultimately show ?thesis
      by (rule Finite1_L6C);
  qed;
  ultimately have
    "{δ(s,<r`(fst(x)),r`(snd(x))>)·s`(δ(r,x)). x∈G×G} ∈ Fin(G)"
    using group_oper_assocA Finite1_L15 by simp;
  moreover have 
    "{δ(s,<(r`(fst(x))·r`(snd(x))),δ(r,x)>).  x∈G×G} ∈ Fin(G)"
  proof -;
    from A1 have 
    "∀x∈G×G. <(r`(fst(x))·r`(snd(x))),δ(r,x)> ∈ G×G"
      using Group_ZF_3_2_L4B by simp;
    moreover from A1 have 
      "{δ(s,x). x∈G×G} ∈ Fin(G)"
      using AlmostHoms_def by simp;
    ultimately show ?thesis by (rule Finite1_L6B);
  qed;
  ultimately have
    "{δ(s,<r`(fst(x)),r`(snd(x))>)·s`(δ(r,x))·
    δ(s,<(r`(fst(x))·r`(snd(x))),δ(r,x)>). x∈G×G} ∈ Fin(G)"
    using group_oper_assocA Finite1_L15 by simp;
  moreover from A1 have "{δ(sor,x). x∈G×G} = 
    {δ(s,<r`(fst(x)),r`(snd(x))>)·s`(δ(r,x))·
    δ(s,<(r`(fst(x))·r`(snd(x))),δ(r,x)>). x∈G×G}"
    using Group_ZF_3_4_L4 by simp;
  ultimately have "{δ(sor,x). x∈G×G} ∈ Fin(G)" by simp;
  with A1 show ?thesis using restrict AlHomOp2_def
    by simp;
qed;

text{*Composition of almost homomorphisms is an almost homomorphism.*}

theorem (in group1) Group_ZF_3_4_T1:
  assumes A1: "s∈AH"  "r∈AH"
  shows "Composition(G)`<s,r> ∈ AH" "sor ∈ AH"
proof -
  from A1 have "<s,r> ∈ (G->G)×(G->G)"
    using AlmostHoms_def by simp;
  then have "Composition(G)`<s,r> : G->G"
    using func_ZF_5_L1 apply_funtype by blast;
  with A1 show "Composition(G)`<s,r> ∈ AH" 
    using Group_ZF_3_4_L5 AlmostHoms_def
    by simp;
  with A1 show  "sor ∈ AH" using AlHomOp2_def restrict 
    by simp;
qed;

text{*The set of almost homomorphisms is closed under composition.
  The second operation on almost homomorphisms is associative.*}

lemma (in group1) Group_ZF_3_4_L6: shows 
  "AH {is closed under} Composition(G)"
  "AlHomOp2(G,f) {is associative on} AH"
proof -;
  show "AH {is closed under} Composition(G)"
    using Group_ZF_3_4_T1 IsOpClosed_def by simp;
  moreover have "AH ⊆ G->G" using AlmostHoms_def
    by auto;
  moreover have 
    "Composition(G) {is associative on} (G->G)"
    using func_ZF_5_L5 by simp;
  ultimately show "AlHomOp2(G,f) {is associative on} AH"
    using func_ZF_4_L3 AlHomOp2_def by simp;
qed;

text{*Type information related to the situation of two almost
  homomorphisms.*}

lemma (in group1) Group_ZF_3_4_L7: 
  assumes A1: "s∈AH"  "r∈AH" and A2: "n∈G"
  shows 
  "s`(n) ∈ G" "(r`(n))¯ ∈ G" 
  "s`(n)·(r`(n))¯ ∈ G"   "s`(r`(n)) ∈ G"
proof -;
  from A1 A2 show 
    "s`(n) ∈ G"
    "(r`(n))¯ ∈ G"
    "s`(r`(n)) ∈ G"
    "s`(n)·(r`(n))¯ ∈ G"
    using AlmostHoms_def apply_type  
      group0_2_L1 monoid0.group0_1_L1 inverse_in_group
    by auto;
qed;

text{*Type information related to the situation of three almost
  homomorphisms.*}

lemma (in group1) Group_ZF_3_4_L8: 
  assumes A1: "s∈AH"  "r∈AH"  "q∈AH" and A2: "n∈G"
  shows 
  "q`(n)∈G"
  "s`(r`(n)) ∈ G"
  "r`(n)·(q`(n))¯ ∈ G"
  "s`(r`(n)·(q`(n))¯) ∈ G"
  "δ(s,<q`(n),r`(n)·(q`(n))¯>) ∈ G"
proof -;
  from A1 A2 show 
    "q`(n)∈ G"  "s`(r`(n)) ∈ G" "r`(n)·(q`(n))¯ ∈ G"
    using AlmostHoms_def apply_type  
      group0_2_L1 monoid0.group0_1_L1 inverse_in_group
    by auto;
  with A1 A2 show "s`(r`(n)·(q`(n))¯) ∈ G"
    "δ(s,<q`(n),r`(n)·(q`(n))¯>) ∈ G"
    using AlmostHoms_def apply_type Group_ZF_3_2_L4A
    by auto
qed;

text{*A formula useful in showing that the composition of almost
  homomorphisms is congruent with respect 
  to the quotient group relation.*}

lemma (in group1) Group_ZF_3_4_L9:
  assumes A1: "s1 ∈ AH"  "r1 ∈ AH"  "s2 ∈ AH"  "r2 ∈ AH"
  and A2: "n∈G"
  shows "(s1or1)`(n)·((s2or2)`(n))¯ =
  s1`(r2`(n))· (s2`(r2`(n)))¯·s1`(r1`(n)·(r2`(n))¯)·
  δ(s1,<r2`(n),r1`(n)·(r2`(n))¯>)"
proof -
  from A1 A2 isAbelian have
    "(s1or1)`(n)·((s2or2)`(n))¯ =
    s1`(r2`(n)·(r1`(n)·(r2`(n))¯))·(s2`(r2`(n)))¯"
    using Group_ZF_3_4_L2 Group_ZF_3_4_L7 group0_4_L6A
      group_oper_assoc by simp;
  with A1 A2 have "(s1or1)`(n)·((s2or2)`(n))¯ = s1`(r2`(n))·
    s1`(r1`(n)·(r2`(n))¯)·δ(s1,<r2`(n),r1`(n)·(r2`(n))¯>)·
    (s2`(r2`(n)))¯"
    using Group_ZF_3_4_L8 Group_ZF_3_4_L1 by simp;
  with A1 A2 isAbelian show ?thesis using
    Group_ZF_3_4_L8 group0_4_L7 by simp;
qed;

text{*The next lemma shows a formula that translates an expression
  in terms of the first group operation on almost homomorphisms and the
  group inverse in the group of almost homomorphisms to an expression using
  only the underlying group operations.*}

lemma (in group1) Group_ZF_3_4_L10: assumes A1: "s ∈ AH"  "r ∈ AH"
  and A2: "n ∈ G"
  shows "(s•(GroupInv(AH,Op1)`(r)))`(n) = s`(n)·(r`(n))¯"
proof -;
  from isAbelian A1 A2 show ?thesis
    using Group_ZF_3_2_L13 Group_ZF_3_2_L12 Group_ZF_3_2_L14
    by simp;
qed;

text{*A neccessary condition for two a. h. to be almost equal.*}

lemma (in group1) Group_ZF_3_4_L11:
  assumes A1: "s≈r"
  shows "{s`(n)·(r`(n))¯. n∈G} ∈ Fin(G)"
proof -
  from A1 have "s∈AH" "r∈AH"
    using QuotientGroupRel_def by auto;
  moreover from A1 have 
    "{(s•(GroupInv(AH,Op1)`(r)))`(n). n∈G} ∈ Fin(G)"
    using QuotientGroupRel_def Finite1_L18 by simp;
  ultimately show ?thesis
    using Group_ZF_3_4_L10 by simp
qed;

text{*A sufficient condition for two a. h. to be almost equal.*}

lemma (in group1) Group_ZF_3_4_L12: assumes A1: "s∈AH"  "r∈AH"
  and A2: "{s`(n)·(r`(n))¯. n∈G} ∈ Fin(G)"
  shows "s≈r"
proof -;
  from groupAssum isAbelian A1 A2 show ?thesis
    using Group_ZF_3_2_L15 AlmostHoms_def 
    Group_ZF_3_4_L10 Finite1_L19 QuotientGroupRel_def
    by simp;
qed;

text{*Another sufficient consdition for two a.h. to be almost
  equal. It is actually just an expansion of the definition
  of the quotient group relation.*}

lemma (in group1) Group_ZF_3_4_L12A: assumes "s∈AH"  "r∈AH"
  and "s•(GroupInv(AH,Op1)`(r)) ∈ FR"
  shows "s≈r"  "r≈s"
proof  -
  from prems show "s≈r" using prems QuotientGroupRel_def 
    by simp;
  then show "r≈s" by (rule Group_ZF_3_3_L3A)
qed;

text{*Another necessary condition for two a.h. to be almost
  equal. It is actually just an expansion of the definition
  of the quotient group relation.*}

lemma (in group1) Group_ZF_3_4_L12B: assumes "s≈r"
  shows "s•(GroupInv(AH,Op1)`(r)) ∈ FR"
  using prems QuotientGroupRel_def by simp;

text{*The next lemma states the essential condition for 
  the composition of a. h. to be congruent
  with respect to the quotient group relation for the subgroup of finite 
  range functions.*} 

lemma (in group1) Group_ZF_3_4_L13: 
  assumes A1: "s1≈s2"  "r1≈r2"
  shows "(s1or1) ≈ (s2or2)"
proof -
  have "{s1`(r2`(n))· (s2`(r2`(n)))¯. n∈G} ∈ Fin(G)"
  proof -
    from A1 have "∀n∈G. r2`(n) ∈ G"
      using QuotientGroupRel_def AlmostHoms_def apply_funtype
      by auto;
    moreover from A1 have "{s1`(n)·(s2`(n))¯. n∈G} ∈ Fin(G)"
      using Group_ZF_3_4_L11 by simp;
    ultimately show ?thesis by (rule Finite1_L6B)
  qed;
  moreover have "{s1`(r1`(n)·(r2`(n))¯). n ∈ G} ∈ Fin(G)"
  proof -
    from A1 have "∀n∈G. s1`(n)∈G"
      using QuotientGroupRel_def AlmostHoms_def apply_funtype
      by auto;
    moreover from A1 have "{r1`(n)·(r2`(n))¯. n∈G} ∈ Fin(G)"
      using Group_ZF_3_4_L11 by simp;
    ultimately show ?thesis by (rule Finite1_L6C);
  qed;
  ultimately have
    "{s1`(r2`(n))· (s2`(r2`(n)))¯·s1`(r1`(n)·(r2`(n))¯). 
    n∈G} ∈ Fin(G)"
    using group_oper_assocA Finite1_L15 by simp;
  moreover have 
    "{δ(s1,<r2`(n),r1`(n)·(r2`(n))¯>). n∈G} ∈ Fin(G)"
  proof -;
    from A1 have "∀n∈G. <r2`(n),r1`(n)·(r2`(n))¯> ∈ G×G" 
      using QuotientGroupRel_def Group_ZF_3_4_L7 by auto;
    moreover from A1 have "{δ(s1,x). x ∈ G×G} ∈ Fin(G)"
      using QuotientGroupRel_def AlmostHoms_def by simp;
    ultimately show ?thesis by (rule Finite1_L6B);
  qed
  ultimately have
    "{s1`(r2`(n))· (s2`(r2`(n)))¯·s1`(r1`(n)·(r2`(n))¯)·
    δ(s1,<r2`(n),r1`(n)·(r2`(n))¯>). n∈G} ∈ Fin(G)"
    using group_oper_assocA Finite1_L15 by simp;
  with A1 show ?thesis using
    QuotientGroupRel_def Group_ZF_3_4_L9 
    Group_ZF_3_4_T1 Group_ZF_3_4_L12 by simp;
qed;

text{*Composition of a. h. to is congruent
  with respect to the quotient group relation for the subgroup of finite 
  range functions. Recall that if an operation say "$\circ $" on $X$ is 
  congruent with respect to an equivalence relation $R$ then we can 
  define the operation 
  on the quotient space $X/R$ by $[s]_R\circ [r]_R := [s\circ r]_R$ and this
  definition will be correct i.e. it will not depend on the choice of 
  representants for the classes $[x]$ and $[y]$. This is why we want it here.*}

lemma (in group1) Group_ZF_3_4_L13A: 
  "Congruent2(QuotientGroupRel(AH,Op1,FR),Op2)"
proof -;
  show ?thesis using Group_ZF_3_4_L13 Congruent2_def
    by simp;
qed;
  
text{*The homomorphism difference for the identity function is equal to
  the neutral element of the group (denoted $e$ in the group1 context).*}

lemma (in group1) Group_ZF_3_4_L14: assumes A1: "x ∈ G×G"
  shows "δ(id(G),x) = \<one>"
proof -;
  from A1 show ?thesis using
    group0_2_L1 monoid0.group0_1_L1 HomDiff_def id_conv group0_2_L6
    by simp;
qed;
 
text{*The identity function ($I(x) = x$) on $G$ is an almost homomorphism.*}

lemma (in group1) Group_ZF_3_4_L15: "id(G) ∈ AH"
proof -;
  have "G×G ≠ 0" using group0_2_L1 monoid0.group0_1_L3A 
    by blast;
  then show ?thesis using Group_ZF_3_4_L14 group0_2_L2
    id_type AlmostHoms_def by simp;
qed;
  
text{*Almost homomorphisms form a monoid with composition.
  The identity function on the group is the neutral element there.*}

lemma (in group1) Group_ZF_3_4_L16: 
  shows
  "IsAmonoid(AH,Op2)"
  "monoid0(AH,Op2)"
  "id(G) = TheNeutralElement(AH,Op2)"
proof-
  let ?i = "TheNeutralElement(G->G,Composition(G))"
  have
    "IsAmonoid(G->G,Composition(G))"
    "monoid0(G->G,Composition(G))"
    using monoid0_def Group_ZF_2_5_L2 by auto;
  moreover have "AH {is closed under} Composition(G)" 
    using Group_ZF_3_4_L6 by simp;
  moreover have "AH ⊆ G->G"
    using AlmostHoms_def by auto;
  moreover have "?i ∈ AH"
    using Group_ZF_2_5_L2 Group_ZF_3_4_L15 by simp;
  moreover have "id(G) =  ?i"
    using Group_ZF_2_5_L2 by simp;
  ultimately show 
    "IsAmonoid(AH,Op2)"
    "monoid0(AH,Op2)"
    "id(G) = TheNeutralElement(AH,Op2)"
    using monoid0.group0_1_T1 group0_1_L6 AlHomOp2_def monoid0_def
    by auto;
qed;

text{*We can project the monoid of almost homomorphisms with composition
  to the group of almost homomorphisms divided by the subgroup of finite
  range functions. The class of the identity function is the neutral element
  of the quotient (monoid).*}

theorem (in group1) Group_ZF_3_4_T2:
  assumes A1: "R = QuotientGroupRel(AH,Op1,FR)"
  shows 
  "IsAmonoid(AH//R,ProjFun2(AH,R,Op2))"
  "R``{id(G)} = TheNeutralElement(AH//R,ProjFun2(AH,R,Op2))"
proof - 
  have "group0(AH,Op1)" using Group_ZF_3_2_L10A group0_def
    by simp;
  with A1 groupAssum isAbelian show 
    "IsAmonoid(AH//R,ProjFun2(AH,R,Op2))"
    "R``{id(G)} = TheNeutralElement(AH//R,ProjFun2(AH,R,Op2))"
    using Group_ZF_3_3_L2 group0.Group_ZF_2_4_L3 Group_ZF_3_4_L13A 
      Group_ZF_3_4_L16 monoid0.Group_ZF_2_2_T1 Group_ZF_2_2_L1
    by auto;
qed;

section{*Shifting almost homomorphisms*}

text{*In this this section we consider what happens if we multiply
  an almost homomorphism by a group element. We show that the
  resulting function is also an a. h., and almost equal to the original
  one. This is used only for slopes (integer a.h.) in @{text "Int_ZF_2"}
  where we need to correct a positive slopes by adding a constant, so that
  it is at least $2$ on positive integers.*}

text{*If $s$ is an almost homomorphism and $c$ is some constant from the group, 
  then $s\cdot c$ is an almost homomorphism. *}

lemma (in group1) Group_ZF_3_5_L1: 
  assumes A1: "s ∈ AH" and A2: "c∈G" and
  A3: "r = {⟨x,s`(x)·c⟩. x∈G}"
  shows
  "∀x∈G. r`(x) = s`(x)·c"
  "r ∈ AH"
  "s ≈ r"
proof -
  from A1 A2 A3 have I: "r:G->G"
    using AlmostHoms_def apply_funtype group_op_closed 
    ZF_fun_from_total by auto;
  with A3 show II: "∀x∈G. r`(x) = s`(x)·c"
    using ZF_fun_from_tot_val by simp;
  with isAbelian A1 A2 have III:
    "∀p ∈ G×G. δ(r,p) = δ(s,p)·c¯"
    using group_op_closed AlmostHoms_def apply_funtype
    HomDiff_def group0_4_L7 by auto;
  have "{δ(r,p). p ∈ G×G} ∈ Fin(G)"
  proof -
    from A1 A2 have
      "{δ(s,p). p ∈ G×G} ∈ Fin(G)"   "c¯∈G"
      using AlmostHoms_def inverse_in_group by auto;
    then have "{δ(s,p)·c¯. p ∈ G×G} ∈ Fin(G)"
      using group_oper_assocA Finite1_L16AA
      by simp;
    moreover from III have
      "{δ(r,p). p ∈ G×G} = {δ(s,p)·c¯. p ∈ G×G}"
      by (rule ZF1_1_L4B);
    ultimately show ?thesis by simp
  qed
  with I show IV: "r ∈ AH" using AlmostHoms_def
    by simp;
  from isAbelian A1 A2 I II have 
    "∀n ∈ G. s`(n)·(r`(n))¯ = c¯"
    using AlmostHoms_def apply_funtype group0_4_L6AB
    by auto;
  then have "{s`(n)·(r`(n))¯. n∈G} = {c¯. n∈G}"
    by (rule ZF1_1_L4B);
  with A1 A2 IV show "s ≈ r"
    using group0_2_L1 monoid0.group0_1_L3A 
      inverse_in_group Group_ZF_3_4_L12 by simp;
qed;
  
end