Theory lemma_2_2_11

(*  Title:      bpl/lemma_2_2_11.thy
    ID:         $Id: lemma_2_2_11.thy $
    Author:     Jesus Aransay
    Comments:   The set of lemmas proving the equational part of the BPL
*)

header{*Previous definitions and Propositions 2.2.9, 2.2.10 and Lemma 2.2.11 in Aransay's memoir*}

theory lemma_2_2_11 
  imports 
  "~~/src/HOL/Algebra/Coset" 
  HomGroupsCompletion
  begin

text{*Definitions and results leading to prove that the @{text ker} and @{text image} sets of a given homomorphism are subgroups
  and give place to suitable algebraic structures*}

locale comm_group_hom = group_hom +
  assumes comm_group_G: "comm_group G"
  and comm_group_H: "comm_group H"
  and hom_completion_h: "h ∈ completion_fun2 G H"

lemma comm_group_hom [intro]: assumes G: "comm_group G" and H: "comm_group H" and h: "h ∈ hom_completion G H" 
  shows "comm_group_hom G H h"
  using G H h 
  by (unfold comm_group_hom_def comm_group_hom_axioms_def group_hom_def group_hom_axioms_def hom_completion_def comm_group_def, simp)

lemma (in comm_group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
  by (rule subgroup.intro) (auto simp add: kernel_def)

lemma (in comm_group_hom) kernel_comm_group: "comm_group (| carrier = (kernel G H h), mult = mult G, one = one G|)),"
  using prems
  apply (intro comm_groupI)
  apply (unfold comm_group_hom_def comm_group_hom_axioms_def comm_group_def comm_monoid_axioms_def kernel_def, auto simp add: G.m_assoc)
  apply (unfold comm_monoid_def comm_monoid_axioms_def, simp)
  done

locale diff_group_hom_diff = comm_group_hom D C h +
  assumes diff_group_axioms_D: "diff_group_axioms D"
  and diff_group_axioms_C: "diff_group_axioms C"
  and diff_hom_h: "h o differD = differC o h"

lemma diff_group_hom_diffI: assumes d_g_D: "diff_group D" and d_g_C: "diff_group C" and h_hom: "h ∈ hom_diff D C" 
  shows "diff_group_hom_diff D C h"
  using d_g_D and d_g_C and h_hom
  by (unfold diff_group_hom_diff_def diff_group_hom_diff_axioms_def comm_group_hom_def comm_group_hom_axioms_def diff_group_def
    hom_diff_def hom_completion_def group_hom_def group_hom_axioms_def comm_group_def, simp)

lemma (in diff_group_hom_diff) diff_group_D: shows "diff_group D"
  using prems by (unfold diff_group_def diff_group_hom_diff_def diff_group_hom_diff_axioms_def 
    comm_group_hom_def comm_group_hom_axioms_def group_hom_def group_hom_axioms_def comm_group_def) (simp)

lemma (in diff_group_hom_diff) diff_group_C: shows "diff_group C"
  using prems by (unfold diff_group_def diff_group_hom_diff_def diff_group_hom_diff_axioms_def 
    comm_group_hom_def comm_group_hom_axioms_def group_hom_def group_hom_axioms_def comm_group_def) (simp)

lemma (in diff_group_hom_diff) hom_diff_h: shows "h ∈ hom_diff D C"
  using prems by (unfold diff_group_def diff_group_hom_diff_def diff_group_hom_diff_axioms_def
    comm_group_hom_def comm_group_hom_axioms_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def) simp

lemma (in diff_group_hom_diff) group_hom_D_D_differ: shows "group_hom D D (differD)"
  using prems by (unfold group_hom_def group_hom_axioms_def diff_group_hom_diff_def
    diff_group_hom_diff_axioms_def comm_group_hom_def diff_group_axioms_def [of D] hom_completion_def) simp

lemma (in diff_group_hom_diff) group_hom_C_C_differ: shows "group_hom C C (differC)"
  using prems by (unfold group_hom_def group_hom_axioms_def diff_group_hom_diff_def
    diff_group_hom_diff_axioms_def comm_group_hom_def diff_group_axioms_def [of C] hom_completion_def) simp

(*lemma diff_group_hom_diff [intro]: assumes "diff_group D" and "diff_group C" and "h ∈ hom_diff D C"
  shows "diff_group_hom_diff D C h"
  using prems by (unfold diff_group_hom_diff_def diff_group_hom_diff_axioms_def 
    comm_group_hom_def comm_group_hom_axioms_def group_hom_def group_hom_axioms_def diff_group_def hom_diff_def hom_completion_def 
    comm_group_def, simp)
*)

lemma (in diff_group_hom_diff) subgroup_kernel: "subgroup (kernel D C h) D"
  by (rule subgroup.intro) (auto simp add: kernel_def)

text{*The following lemma corresponds to Proposition 2.2.9 in Aransay's thesis*}

text{*Due to the use of completion functions for the differential, we need to define the @{term diff} function, which originally
  was a completion from @{term D} into @{term D}, as a completion from the kernel into the original differential group @{term D}*}

lemma (in diff_group_hom_diff) kernel_diff_group:
  "diff_group (| carrier = (kernel D C h), mult = mult D, one = one D, 
  diff = completion (|carrier = (kernel D C h), mult = mult D, one = one D, diff = diff D |)), D (diff D)|)),"
  (is "diff_group ?KER")
proof (intro diff_groupI, simp_all)
  fix x y
  assume x_in_ker: "x ∈ kernel D C h" and y_in_ker: "y ∈ kernel D C h"
  from group_hom.subgroup_kernel [of D C h] and subgroup_def [of "kernel D C h" D] and prems show "x ⊗ y ∈ kernel D C h"
    by (unfold diff_group_hom_diff_def comm_group_hom_def, simp)
next
  from group_hom.subgroup_kernel [of D C h] and subgroup_def [of "kernel D C h" D] and prems
  show "\<one> ∈ kernel D C h" by (unfold diff_group_hom_diff_def comm_group_hom_def, simp)
next
  fix x y z
  assume x_in_ker: "x ∈ kernel D C h" and y_in_ker: "y ∈ kernel D C h" and z_in_ker: "z ∈ kernel D C h"
  from group_hom.subgroup_kernel [of D C h] and subgroup_def [of "kernel D C h" D] and prems and D.m_assoc [of x y z]
  show "x ⊗ y ⊗ z = x ⊗ (y ⊗ z)"  by (unfold diff_group_hom_diff_def comm_group_hom_def, auto)
next
  fix x y assume x_in_ker: "x ∈ kernel D C h" and y_in_ker: "y ∈ kernel D C h"
  from group_hom.subgroup_kernel [of D C h] and prems 
    and psubsetD [of "kernel D C h" "carrier D" x]
    and psubsetD [of "kernel D C h" "carrier D" y]
    and comm_monoid.m_ac (2) [of D x y]
  show "x ⊗ y = y ⊗ x" unfolding diff_group_hom_diff_def unfolding comm_group_hom_def 
    unfolding subgroup_def
    unfolding comm_group_hom_axioms_def unfolding comm_group_def [of D] by auto
next
  fix x assume x_in_ker: "x ∈ kernel D C h"
  from group_hom.subgroup_kernel [of D C h] and subgroup_def [of "kernel D C h" D] and prems show "\<one> ⊗ x = x"
    unfolding diff_group_hom_diff_def comm_group_hom_def by auto
next
  fix x assume x_in_ker: "x ∈ kernel D C h"
  from bexI [of "(λy. y ⊗ x = \<one>)" "inv x" "kernel D C h"] show "∃y∈kernel D C h. y ⊗ x = \<one>"
    using m_inv_def [of _ x]
    using prems (1) using group_hom.subgroup_kernel [of D C h] using x_in_ker
    unfolding diff_group_hom_diff_def unfolding comm_group_hom_def unfolding subgroup_def by auto
next
  from prems and diff_group_hom_diff.group_hom_C_C_differ [of D C h] diff_group_hom_diff.group_hom_D_D_differ [of D C h]
    and group_hom.hom_one [of C C "differC"]
  show "completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>, diff = differ|)), D (differ)
    ∈ hom_completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>,
    diff = completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>, diff = differ|)), D (differ)|)),
    (|carrier = kernel D C h, mult = op ⊗, one = \<one>, 
    diff = completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>, diff = differ|)), D (differ)|)),"
    (*The following proof step should be reduced somehow*)
    unfolding diff_group_hom_diff_def diff_group_hom_diff_axioms_def comm_group_hom_def comm_group_hom_axioms_def
      group_hom_def group_hom_axioms_def diff_group_axioms_def hom_completion_def hom_def completion_def completion_fun2_def 
      Pi_def kernel_def by (auto simp add: expand_fun_eq)
next
  fix x
  from prems and diff_group.diff_nilpot [OF diff_group_hom_diff.diff_group_D [of D C h]] and group_hom.hom_one [of D D "differD"]
    and diff_group_hom_diff.group_hom_D_D_differ [of D C h]
  show "completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>, diff = differ|)), D (differ)
    (completion (|carrier = kernel D C h, mult = op ⊗, one = \<one>, diff = differ|)), D (differ) x) = \<one>"
    unfolding completion_def diff_group_hom_diff_def comm_group_hom_def by (auto simp add: expand_fun_eq)
qed

text{*The following lemma corresponds to Proposition 2.2.10 in Aransay's thesis; here it is proved for a generic homomorphism @{term h}*}

lemma (in diff_group_hom_diff) image_diff_group:
  "diff_group (| carrier = image h (carrier D), mult = mult C, one = one C,
  diff = completion (| carrier = image h (carrier D), mult = mult C, one = one C, diff = diff C|)), C (diff C)|)),"
  (is "diff_group (| carrier = ?img_set, mult = mult C, one = one C, diff = ?compl |))," is "diff_group ?IMG")
proof (intro diff_groupI, auto)
  fix x y
  assume x: "x ∈ carrier D" and y: "y ∈ carrier D"
  from hom_mult [OF x y] and D.m_closed [OF x y] show "h x ⊗C h y ∈ ?img_set" unfolding image_def by force
next
  from D.one_closed and group_hom.hom_one [of D C h] show "\<one>C ∈ ?img_set" unfolding image_def by force
next
  fix x y z
  assume x: "x ∈ carrier D" and y: "y ∈ carrier D" and z: "z ∈ carrier D"
  from m_assoc and hom_closed and x y z show "h x ⊗C h y ⊗C h z = h x ⊗C (h y ⊗C h z)" by simp
next
  fix x y
  assume x: "x ∈ carrier D" and y: "y ∈ carrier D"
  from prems and hom_closed [OF x] and hom_closed [OF y] and x y and comm_monoid.m_comm [of C "h x" "h y"] 
    and diff_group_hom_diff.diff_group_C [of D C h]
  show "h x ⊗C h y = h y ⊗C h x" unfolding diff_group_def comm_group_def [of C] by auto
next
  fix x
  assume x: "x ∈ carrier D"
    (*There should be a lemma in Group.thy stating that "group D; x ∈ carrier D" => ∃y ∈ carrier D. y ⊗ x = \<one>*)
  from Units_def [of D] and D.Units_eq and x obtain y where y: "y ∈ carrier D" and y_x: "y ⊗D x = \<one>D" by fast
  from group_hom.hom_one [of D C h] and hom_mult [OF y x] and y_x and y show "∃y∈carrier D. h y ⊗C h x = \<one>C" by auto
next
  show "?compl∈ hom_completion ?IMG ?IMG"
  proof (intro hom_completionI homI, auto)
    show "?compl ∈ completion_fun2 ?IMG ?IMG" unfolding completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
  next
    fix x
    assume x: "x ∈ carrier D"
    from prems and diff_group_hom_diff.diff_group_D [of D C h]
      and hom_completion_closed [OF diff_group.diff_hom [of D]  x] 
      and imageI [of "(differD) x" "carrier D" h] and diff_group_hom_diff.diff_hom_h [of D C h]
    show "(differC) (h x) ∈ ?img_set" unfolding image_def by (simp add: expand_fun_eq)
  next
    fix x y
    assume x: "x ∈ carrier D" and y: "y ∈ carrier D"
    from hom_mult [OF x y] and D.m_closed [OF x y]
    have "?compl (h x ⊗C h y) = (differC) (h (x ⊗ y))" by (unfold completion_def image_def, auto)
    also from diff_group_hom_diff.diff_group_C [of D C h] and hom_mult [OF x y] 
      and hom_completion_mult [OF diff_group.diff_hom [of C] hom_closed [OF x] hom_closed [OF y]] and prems
    have "… = (differC) (h x) ⊗C (differC) (h y)" by simp
    finally show "?compl (h x ⊗C h y) = (differC) (h x) ⊗C (differC) (h y)" by simp
  qed
next
  from diff_group_hom_diff.diff_group_C [of D C h] and diff_group.diff_nilpot [of C] 
    and diff_group.diff_hom [of C] and image_def and diff_group_hom_diff.group_hom_C_C_differ [of D C h]
    and group_hom.hom_one [of C C "differC"] and prems show "!!x. ?compl (?compl x) = \<one>C"
    unfolding hom_completion_def completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
qed

text{*Before proving Lemma 2.2.11, we first must introduce the definition of @{term reduction}*}

locale reduction = diff_group D + diff_group C + var f + var g + var h +
  assumes f_hom_diff: "f ∈ hom_diff D C"
  and g_hom_diff: "g ∈ hom_diff C D"
  and h_hom_compl: "h ∈ hom_completion D D"
  and fg: "f o g = (λx. if x ∈ carrier C then id x else \<one>C)"
  and gf_dh_hd: "(λx. if x ∈ carrier D then (g o f) x ⊗ (if x ∈ carrier D then ((differ) o h) x ⊗ (h o (differ)) x else \<one>D) else \<one>D) = 
  (λx. if x ∈ carrier D then id x else \<one>D)"
  and fh: "f o h = (λx. if x ∈ carrier D then \<one>C else \<one>C)"
  and hg: "h o g = (λx. if x ∈ carrier C then \<one>D else \<one>D)"
  and hh: "h o h = (λx. if x ∈ carrier D then \<one>D else \<one>D)"

text{*Due to the nature of the formula @{thm [locale=reduction] gf_dh_hd}, we associate first the addition 
  of @{term "d o h"} and @{term "h o d"}, and then @{term "g o f"}*}

lemma reductionI:
  includes struct D + struct C 
  assumes src_diff_group: "diff_group D"
  and trg_diff_group: "diff_group C"
  assumes "f ∈ hom_diff D C"
  and "g ∈ hom_diff C D"
  and "h ∈ hom_completion D D"
  and "f o g = (λx. if x ∈ carrier C then id x else \<one>C)"
  and "(λx. if x ∈ carrier D then (g o f) x ⊗ (if x ∈ carrier D then ((differ) o h) x ⊗ (h o (differ)) x else \<one>D) else \<one>D) = 
  (λx. if x ∈ carrier D then id x else \<one>D)"
  and "f o h = (λx. if x ∈ carrier D then \<one>C else \<one>C)"
  and "h o g = (λx. if x ∈ carrier C then \<one>D else \<one>D)"
  and "h o h = (λx. if x ∈ carrier D then \<one>D else \<one>D)"
  shows "reduction D C f g h"
  using prems unfolding reduction_def reduction_axioms_def diff_group_def by simp

lemma (in reduction) C_diff_group: shows "diff_group C" using prems unfolding reduction_def by simp

lemma (in reduction) D_diff_group: shows "diff_group D" using prems unfolding reduction_def by simp

lemma (in reduction) D_C_f_diff_group_hom_diff: shows "diff_group_hom_diff D C f" using prems and diff_group_hom_diffI [of D C f]
  unfolding reduction_def reduction_axioms_def by auto

lemma (in reduction) D_C_f_group_hom: shows "group_hom D C f" using D_C_f_diff_group_hom_diff 
  unfolding diff_group_hom_diff_def comm_group_hom_def by simp

lemma (in reduction) C_D_g_diff_group_hom_diff: shows "diff_group_hom_diff C D g" using prems and diff_group_hom_diffI [of C D g]
  unfolding reduction_def reduction_axioms_def by auto

lemma (in reduction) C_D_g_group_hom: shows "group_hom C D g" using C_D_g_diff_group_hom_diff 
  unfolding diff_group_hom_diff_def comm_group_hom_def by simp

subsection{*Definition of isomorphic differential groups*}

text{* Lemma 2.2.11, which corresponds to the first lemma in the BPL proof, has been already proved in our first approach.*}
text{* It requires introducing first the notion of isomorphic differential groups; the definition is based on
  the one of isomorphic monoids presented in Group.thy for homomorphisms, by extending it to be coherent with the differentials.*}

constdefs
  iso_diff :: "('a, 'c) diff_group_scheme => ('b, 'd) diff_group_scheme => ('a => 'b) set"  (infixr "≅diff" 60)
  "D ≅diff C == {h. h ∈ hom_diff D C & bij_betw h (carrier D) (carrier C)}"

lemma iso_diffI: assumes closed: "!!x. x ∈ carrier D ==> h x ∈ carrier C"
  and mult: "!!x y. [|x ∈ carrier D; y ∈ carrier D|] ==> h (x ⊗D y) = h x ⊗C h y"
  and complect: "∃g. h = (λx. if x ∈ carrier D then g x else \<one>C)"
  and coherent: "!!x. h ((differD) x) = (differC) (h x)"
  and inj_on: "!!x y. [| x ∈ carrier D;  y ∈ carrier D;  h (x) = h (y) |] ==> x=y"
  and image: "!!y. y∈carrier C ==> ∃x ∈ carrier D. y = h (x)"
  shows "h ∈ D ≅diff C"
  using prems
  unfolding iso_diff_def unfolding hom_diff_def apply (simp add: expand_fun_eq)
  unfolding hom_completion_def apply simp
  unfolding completion_fun2_def completion_def apply (simp add: expand_fun_eq)
  unfolding hom_def unfolding Pi_def apply simp
  unfolding bij_betw_def inj_on_def apply simp
  unfolding image_def by auto

    (*The following notion corresponds to the one of "inverse isomorphisms"; whenever we have two isomorphisms, 
    such that their compositions in both senses are equal to the corresponding identities, we define them to be "inverse isomorphisms"*)
    (*Subindexes are not allowed inside of the infix name "≅invdiff"*)

definition
  iso_inv_diff :: "('a, 'c) diff_group_scheme => ('b, 'd) diff_group_scheme => (('a => 'b) × ('b => 'a)) set"  (infixr "≅invdiff" 60)
  where "D ≅invdiff C == {(f, g). f ∈ (D ≅diff C) & g ∈ (C ≅diff D) & (f o g = completion C C id) & (g o f = completion D D id)}"

lemma iso_inv_diffI: assumes f: "f ∈ (D ≅diff C)" and g: "g ∈ (C ≅diff D)" and fg_id: "(f o g = completion C C id)" 
  and gf_id: "(g o f = completion D D id)" shows "(f, g) ∈ (D ≅invdiff C)"
  using f g fg_id gf_id unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_iso_diff: assumes f_f': "(f, f') ∈ (D ≅invdiff C)" shows "f ∈ (D ≅diff C)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_iso_diff2: assumes f_f': "(f, f') ∈ (D ≅invdiff C)" shows "f' ∈ (C ≅diff D)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_id: assumes f_f': "(f, f') ∈ (D ≅invdiff C)" shows "f' o f = completion D D id"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_id2: assumes f_f': "(f, f') ∈ (D ≅invdiff C)" shows "f o f' = completion C C id"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_rev: assumes f_f': "(f, f') ∈ (D ≅invdiff C)" shows "(f', f) ∈ (C ≅invdiff D)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_diff_hom_diff: assumes h: "h ∈ D ≅diff C" shows "h ∈ hom_diff D C"
  using h unfolding iso_diff_def by simp

subsection{*Previous facts for Lemma 2.2.11*}

lemma (in reduction) g_f_hom_diff: shows "g o f ∈ hom_diff D D"
proof (unfold hom_diff_def hom_completion_def, auto)
  from f_hom_diff and g_hom_diff have f: "f ∈ completion_fun2 D C" and g: "g ∈ completion_fun2 C D"
    by (unfold hom_diff_def hom_completion_def, simp_all)
  show "g o f ∈ completion_fun2 D D"
  proof (unfold completion_fun2_def, simp, intro exI [of _ "g o f"], unfold completion_def, auto simp add: expand_fun_eq)
    fix x assume x: "x ∉ carrier D"
    from C_diff_group D_diff_group g_hom_diff and completion_closed2 [OF f x] and group_hom.hom_one [of C D g] 
    show "g (f x) = \<one>" unfolding diff_group_def comm_group_def group_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def 
      by simp
  qed
next
  show "g o f ∈ hom D D"
  proof (intro homI)
    fix x
    assume x: "x ∈ carrier D"
    from hom_diff_closed [OF f_hom_diff x] and hom_diff_closed [OF g_hom_diff, of "f x"] show "(g o f) x ∈ carrier D" by simp
  next
    fix x y
    assume x: "x ∈ carrier D" and y: "y ∈ carrier D"
    from f_hom_diff g_hom_diff and x y and hom_completion_mult [of f D C x y] hom_completion_mult [of g C D "f x" "f y"] 
      and hom_diff_closed [of f D C x] hom_diff_closed [of f D C y] 
    show "(g o f) (x ⊗ y) = (g o f) x ⊗ (g o f) y" unfolding hom_diff_def by simp
  qed
next
  from hom_diff_coherent [OF f_hom_diff] and hom_diff_coherent [OF g_hom_diff] and o_assoc [of g f differ] 
    and o_assoc [of g "differC" f] and o_assoc [of differ g f] show "g o f o differ = differ o (g o f)" by simp
qed

lemma (in reduction) D_D_g_f_diff_group_hom_diff: shows "diff_group_hom_diff D D (g o f)" using g_f_hom_diff and D_diff_group
  and diff_group_hom_diffI [of D D "(g o f)"] by simp_all

lemma (in reduction) D_D_g_f_group_hom: shows "group_hom D D (g o f)" using D_D_g_f_diff_group_hom_diff
  unfolding diff_group_hom_diff_def comm_group_hom_def by simp

text{*The following lemma proves that, in a general reduction, @{term f}, @{term g}, @{term h}, the set image of @{term "g o f"} 
  with the operations inherited from @{term D} is a differential group.*}

lemma (in reduction) image_g_f_diff_group: shows "diff_group (|carrier = image (g o f) (carrier D), mult = mult D, one = one D, 
  diff = completion (|carrier = image (g o f) (carrier D), mult = mult D, one = one D, diff = diff D |)), D (diff D) |)),"
  using diff_group_hom_diff.image_diff_group [of D D "g o f"] and diff_group_hom_diffI [OF D_diff_group D_diff_group g_f_hom_diff] by simp

subsection{*Lemma 2.2.11*}

text{*The following lemmas correpond to Lemma 2.2.11 in Aransay's thesis*}
text{*In the version in the thesis, two differential groups are defined to be isomorphic whenever there exists 
  two homomorphisms @{term f} and @{term g} such that their composition is the identity in both directions*}
text{*The Isabelle definition is slightly different, and it requires proving that there exists \emph{one homomorphism}, 
  which is, additionally, injective and surjective*}
text{*This is the reason why the lemma is proved in Isabelle in four different lemmas; the first two, prove that the isomorphism
  exists, and then we prove that they are mutually inverse*}

text{*We first introduce a locale which only contains some abbreviations, the main reason is to shorten proofs and statements*}
text{*We will avoid the use of record update operations*}

locale lemma_2_2_11 = reduction D C f g h

text{*FIXME:Probably the following @{term definitions} would be more suitably stored as @{term abbreviations} or @{term notations}*}

context lemma_2_2_11
begin

definition im_gf where "im_gf == image (g o f) (carrier D)"

definition diff_group_im_gf where "diff_group_im_gf == (|carrier = image (g o f) (carrier D), mult = mult D, one = one D, 
  diff =completion (|carrier = image (g o f) (carrier D), mult = mult D, one = one D, diff = diff D|)), D (diff D)|)),"

definition diff_im_gf where "diff_im_gf == completion diff_group_im_gf D (diff D)"

end

lemma (in lemma_2_2_11) lemma_2_2_11_first_part: shows "g ∈ (C ≅diff diff_group_im_gf)"
proof (intro iso_diffI)
  fix x
  assume x: "x ∈ carrier C"
  show "g x ∈ carrier diff_group_im_gf"
  proof (unfold diff_group_im_gf_def image_def, simp, intro bexI [of _ "g x"])
    from fg and x show "g x = g (f (g x))" by (auto simp add: expand_fun_eq)
  next
    from hom_diff_closed [OF g_hom_diff x]show "g x ∈ carrier D" by simp
  qed
next
  fix x y
  assume x: "x ∈ carrier C" and y: "y ∈ carrier C"
  from hom_diff_mult [OF g_hom_diff x y] and diff_group_im_gf_def show "g (x ⊗C y) = g x ⊗diff_group_im_gf g y" by simp
next
  from g_hom_diff and f_in_completion_fun2_f_completion [of g C D] and completion_def [of C D g] and diff_group_im_gf_def
  show " ∃ga. g = (λx. if x ∈ carrier C then ga x else \<one>diff_group_im_gf)"
    unfolding hom_diff_def hom_completion_def completion_fun2_def expand_fun_eq by (intro exI [of _ g]) auto
next
  fix x
  show "g ((differC) x) = (differdiff_group_im_gf) (g x)"
  proof (cases "x ∈ carrier C")
    case True then have "g x ∈ (g o f) ` carrier D"
    proof (unfold image_def, simp, intro bexI [of _ "g x"])
      from fg and True show "g x = g (f (g x))" by (simp add: expand_fun_eq)
    next
      from hom_diff_closed [OF g_hom_diff True] show "g x ∈ carrier D" by simp
    qed
    then have "(differdiff_group_im_gf) (g x) = (differ) (g x)" unfolding completion_def diff_group_im_gf_def im_gf_def by auto
    with g_hom_diff and hom_diff_coherent [of g C D] show "g ((differC) x) =(differdiff_group_im_gf) (g x)"
      unfolding diff_group_im_gf_def im_gf_def by (simp add: expand_fun_eq)
  next
    case False
    from C.diff_hom and hom_completion_def [of C C] and completion_closed2 [OF _ False, of "differC" C] have "(differC) x = \<one>C" by simp
    with group_hom.hom_one [of C D g] and C_D_g_group_hom
    have "g ((differC) x) = \<one>D" by simp
    moreover
    from D_C_f_group_hom C_D_g_group_hom D.diff_hom and group_hom.hom_one [of D C f] group_hom.hom_one [of C D g] 
      group_hom.hom_one [of D D differ] and D.one_closed and False and diff_group_im_gf_def and C_diff_group D_diff_group g_hom_diff f_hom_diff
    have comp_one: "(differdiff_group_im_gf) (g x) = \<one>D"
     unfolding group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def 
       diff_group_def comm_group_def by auto
    ultimately show "g ((differC) x) = (differdiff_group_im_gf) (g x)" by simp
  qed
next
  fix x y
  assume x: "x ∈ carrier C" and y: "y ∈ carrier C" and g_eq: "g x = g y"
  from g_eq have fg_eq: "f (g x) = f (g y)" by simp
  with fg and x and y show "x = y" by (simp add: expand_fun_eq)
next
  fix y
  assume y: "y ∈ carrier diff_group_im_gf" then have "y ∈ (g o f)` (carrier D)" by (unfold diff_group_im_gf_def, simp)
  then obtain x where "g (f x) = y" and x: "x ∈ carrier D" by auto
  with bexI [of "λx. (y = g x)" "f x" "carrier C"] and hom_diff_closed [OF f_hom_diff x] show "∃x∈carrier C. y = g x" by simp
qed

text{*The inverse of @{term g} is the restriction of @{term f} to the image set of @{term "g o f"}*}

lemma (in lemma_2_2_11) lemma_2_2_11_second_part: shows "completion diff_group_im_gf C f ∈ (diff_group_im_gf ≅diff C)"
(is "?compl_f ∈ (?IM ≅diff C)")
proof (intro iso_diffI)
  fix x
  assume x: "x ∈ carrier ?IM" then have x_im: "x ∈ (g o f)` (carrier D)" by (unfold diff_group_im_gf_def, simp)
  then obtain y where gf_y: "g (f y) = x" and y: "y ∈ carrier D" by auto
  from x_im have "?compl_f x = f x" by (unfold completion_def diff_group_im_gf_def, simp)
  with gf_y and hom_diff_closed [OF f_hom_diff y] hom_diff_closed [OF g_hom_diff, of "f y"] hom_diff_closed [OF f_hom_diff, of "g (f y)"]
  show "?compl_f x ∈ carrier C" by simp
next
  fix x y
  assume x: "x ∈ carrier ?IM" and y: "y ∈ carrier ?IM" then obtain x' y' where gf_x': "g (f x') = x" and gf_y': "g (f y') = y" 
    and x': "x' ∈ carrier D" and y': "y' ∈ carrier D" unfolding diff_group_im_gf_def by auto
  with sym [OF hom_diff_mult [OF g_hom_diff, of "f x'" "f y'"]] and hom_diff_closed [OF f_hom_diff x'] hom_diff_closed [OF f_hom_diff y']
  and x y and sym [OF hom_diff_mult [OF f_hom_diff x' y']]
  have "?compl_f (x ⊗?IM y) = f (x ⊗D y)" unfolding diff_group_im_gf_def completion_def by auto
  also from gf_x' gf_y' have "… = f (g (f x') ⊗D g (f y'))" by simp
  also from hom_diff_closed [OF f_hom_diff x'] hom_diff_closed [OF f_hom_diff y'] hom_diff_closed [OF g_hom_diff, of "f x'"]
    hom_diff_closed [OF g_hom_diff, of "f y'"] and hom_diff_mult [OF f_hom_diff] have "… = f (g (f x')) ⊗C f (g (f y'))" by simp
  also from gf_x' gf_y' and x' y' have "… = ?compl_f x ⊗C ?compl_f y" unfolding completion_def diff_group_im_gf_def by auto
  finally show "?compl_f (x ⊗?IM y) = ?compl_f x ⊗C ?compl_f y" by simp
next
  show "∃g. ?compl_f = (λx. if x ∈ carrier ?IM then g x else \<one>C)" unfolding completion_def by (rule exI [of _ f]) simp
next
  fix x
  show "?compl_f ((differ?IM) x) = (differC) (?compl_f x)"
  proof (cases "x ∈ carrier ?IM")
    case True then obtain y where y: "y ∈ carrier D" and gf_y: "x = g (f y)" unfolding diff_group_im_gf_def by auto
    then have "?compl_f ((differ?IM) x) = ?compl_f ((differ) (g (f y)))" unfolding completion_def diff_group_im_gf_def by auto
    also have "… = f ((differ) (g (f y)))"
    proof -
      from hom_diff_coherent [OF g_hom_diff] and hom_diff_coherent [OF f_hom_diff] have "((differ) (g (f y))) = (g (f ((differ) y)))"
        by (simp add: expand_fun_eq)
      with hom_completion_closed [OF D.diff_hom y] show ?thesis unfolding image_def diff_group_im_gf_def completion_def by auto
    qed
    also from hom_diff_coherent [OF f_hom_diff] have "… = (differC) (f (g (f y)))" by (simp add: expand_fun_eq)
    also from y and gf_y have "… = (differC) (?compl_f x)" unfolding completion_def image_def diff_group_im_gf_def by auto
    finally show ?thesis by simp
  next
    case False then have diff_one: "((differ?IM) x) = \<one>" unfolding diff_group_im_gf_def completion_def by auto
    from D_C_f_group_hom and C_D_g_group_hom and group_hom.hom_one [of D C f] and group_hom.hom_one [of C D g] and bexI [of _ "\<one>"]
    and diff_group_im_gf_def and im_gf_def have one_image: "\<one> ∈ (g o f)` carrier D" unfolding image_def by simp
    with diff_one have "?compl_f ((differ?IM) x) = f \<one>" unfolding completion_def diff_group_im_gf_def by simp
    also from D_C_f_group_hom and group_hom.hom_one [of D C f] have "… = \<one>C" by simp
    finally have l_h_s: "?compl_f ((differ?IM) x) = \<one>C" by simp
    from False have diff_one: "(differC) (?compl_f x) = (differC) \<one>C" unfolding completion_def by simp
    also from C.diff_hom and group_hom.hom_one [of C C "(differC)"] and C_diff_group have "… = \<one>C"
      unfolding group_hom_def group_hom_axioms_def diff_group_def comm_group_def hom_completion_def by simp
    with diff_one have r_h_s: "(differC) (?compl_f x) = \<one>C" by simp
    from l_h_s and r_h_s show ?thesis by simp
  qed
next
  fix x y
  assume x: "x ∈ carrier ?IM" and y: "y ∈ carrier ?IM" then obtain x' y' where gf_x': "g (f x') = x" and gf_y': "g (f y') = y" 
    and x': "x' ∈ carrier D" and y': "y' ∈ carrier D" unfolding diff_group_im_gf_def by auto  
  assume eq: "?compl_f x = ?compl_f y" with x y have "f x = f y" unfolding completion_def by simp
  with gf_x' gf_y' have "f (g (f x')) = f (g (f y'))" by simp
  then have "g (f (g (f x'))) = g (f (g (f y')))" by simp
  with fg and hom_diff_closed [OF f_hom_diff x'] hom_diff_closed [OF f_hom_diff y'] and gf_x' gf_y' show "x = y"  
    by (auto simp add: expand_fun_eq)
next
  fix y
  assume y: "y ∈ carrier C"
  from fg have fg_idemp: "(f o g) o (f o g) = (f o g)" by (simp add: expand_fun_eq)
  with bexI [of "λx. (y = f (g (f x)))" "g y" "carrier D"] and hom_diff_closed [OF g_hom_diff y] and fg and y
  show "∃x∈carrier ?IM. y = ?compl_f x" unfolding completion_def diff_group_im_gf_def image_def by (auto simp add: expand_fun_eq)
qed

text{*We now prove that @{term g} and the restriction of @{term f} are inverse of each other.*}

lemma (in lemma_2_2_11) lemma_2_2_11_third_part: shows "completion diff_group_im_gf C f o g = (λx. if x ∈ carrier C then id x else \<one>C)"
(is "?compl_f o g = ?id_C")
proof (unfold expand_fun_eq, auto)
  fix x
  assume x: "x ∈ carrier C" with diff_group_im_gf_def and image_def [of "(g o f)" "carrier D"] 
    and bexI [of  "λy. (g x = (g o f) y)" "g x" "carrier D"] and fg and hom_diff_closed [OF g_hom_diff x] 
  show "?compl_f (g x) = x" unfolding completion_def by (simp add: expand_fun_eq)
next
  fix x
  assume x: "x ∉ carrier C"
  from diff_group_im_gf_def and g_hom_diff and completion_closed2 [OF _ x, of g D] and D_C_f_group_hom and group_hom.hom_one [of D C f] 
  show "?compl_f (g x) = \<one>C" unfolding hom_diff_def hom_completion_def completion_def by simp
qed

lemma (in lemma_2_2_11) lemma_2_2_11_fourth_part:
  shows "g o completion diff_group_im_gf C f = (λx. if x ∈ carrier diff_group_im_gf then id x else \<one>diff_group_im_gf)"
(is "g o ?compl_f = ?id_IM")
proof (unfold diff_group_im_gf_def completion_def expand_fun_eq, auto)
  fix x
  assume x: "x ∈ carrier D"
  from fg and hom_diff_closed [OF f_hom_diff x] show "g (f (g (f x))) = g (f x)" by (simp add: expand_fun_eq)
next
  from C_D_g_group_hom and group_hom.hom_one [of C D g] show "g \<one>C = \<one>D" by simp
qed

text{*The following is just the recollection of the four parts in which we have divided the proof of Lemma 2.2.11*}

text{*The following statement should be compared to Lemma 2.2.11 in Aransay memoir*}

lemma (in lemma_2_2_11) lemma_2_2_11: shows "(g, completion diff_group_im_gf C f) ∈ (C ≅invdiff diff_group_im_gf)"
  using lemma_2_2_11_first_part and lemma_2_2_11_second_part and lemma_2_2_11_third_part and lemma_2_2_11_fourth_part
    unfolding iso_inv_diff_def completion_def by simp

end