(*  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 \<in> completion_fun2 G H"

lemma comm_group_hom [intro]: assumes G: "comm_group G" and H: "comm_group H" and h: "h \<in> 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 \<lparr> carrier = (kernel G H h), mult = mult G, one = one G\<rparr>"
  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 \<circ> differ\<^bsub>D\<^esub> = differ\<^bsub>C\<^esub> \<circ> h"

lemma diff_group_hom_diffI: assumes d_g_D: "diff_group D" and d_g_C: "diff_group C" and h_hom: "h \<in> 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 \<in> 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 (differ\<^bsub>D\<^esub>)"
  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 (differ\<^bsub>C\<^esub>)"
  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 \<in> 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 \<lparr> carrier = (kernel D C h), mult = mult D, one = one D, 
  diff = completion \<lparr>carrier = (kernel D C h), mult = mult D, one = one D, diff = diff D \<rparr> D (diff D)\<rparr>"
  (is "diff_group ?KER")
proof (intro diff_groupI, simp_all)
  fix x y
  assume x_in_ker: "x \<in> kernel D C h" and y_in_ker: "y \<in> 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 \<otimes> y \<in> 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> \<in> 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 \<in> kernel D C h" and y_in_ker: "y \<in> kernel D C h" and z_in_ker: "z \<in> 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 \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)"  by (unfold diff_group_hom_diff_def comm_group_hom_def, auto)
next
  fix x y assume x_in_ker: "x \<in> kernel D C h" and y_in_ker: "y \<in> 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 \<otimes> y = y \<otimes> 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 \<in> 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> \<otimes> x = x"
    unfolding diff_group_hom_diff_def comm_group_hom_def by auto
next
  fix x assume x_in_ker: "x \<in> kernel D C h"
  from bexI [of "(\<lambda>y. y \<otimes> x = \<one>)" "inv x" "kernel D C h"] show "\<exists>y\<in>kernel D C h. y \<otimes> 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 "differ\<^bsub>C\<^esub>"]
  show "completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> D (differ)
    \<in> hom_completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>,
    diff = completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> D (differ)\<rparr>
    \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, 
    diff = completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> D (differ)\<rparr>"
    (*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 "differ\<^bsub>D\<^esub>"]
    and diff_group_hom_diff.group_hom_D_D_differ [of D C h]
  show "completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> D (differ)
    (completion \<lparr>carrier = kernel D C h, mult = op \<otimes>, one = \<one>, diff = differ\<rparr> 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 \<lparr> carrier = image h (carrier D), mult = mult C, one = one C,
  diff = completion \<lparr> carrier = image h (carrier D), mult = mult C, one = one C, diff = diff C\<rparr> C (diff C)\<rparr>"
  (is "diff_group \<lparr> carrier = ?img_set, mult = mult C, one = one C, diff = ?compl \<rparr>" is "diff_group ?IMG")
proof (intro diff_groupI, auto)
  fix x y
  assume x: "x \<in> carrier D" and y: "y \<in> carrier D"
  from hom_mult [OF x y] and D.m_closed [OF x y] show "h x \<otimes>\<^bsub>C\<^esub> h y \<in> ?img_set" unfolding image_def by force
next
  from D.one_closed and group_hom.hom_one [of D C h] show "\<one>\<^bsub>C\<^esub> \<in> ?img_set" unfolding image_def by force
next
  fix x y z
  assume x: "x \<in> carrier D" and y: "y \<in> carrier D" and z: "z \<in> carrier D"
  from m_assoc and hom_closed and x y z show "h x \<otimes>\<^bsub>C\<^esub> h y \<otimes>\<^bsub>C\<^esub> h z = h x \<otimes>\<^bsub>C\<^esub> (h y \<otimes>\<^bsub>C\<^esub> h z)" by simp
next
  fix x y
  assume x: "x \<in> carrier D" and y: "y \<in> 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 \<otimes>\<^bsub>C\<^esub> h y = h y \<otimes>\<^bsub>C\<^esub> h x" unfolding diff_group_def comm_group_def [of C] by auto
next
  fix x
  assume x: "x \<in> carrier D"
    (*There should be a lemma in Group.thy stating that "group D; x \<in> carrier D" => \<exists>y \<in> carrier D. y \<otimes> x = \<one>*)
  from Units_def [of D] and D.Units_eq and x obtain y where y: "y \<in> carrier D" and y_x: "y \<otimes>\<^bsub>D\<^esub> x = \<one>\<^bsub>D\<^esub>" by fast
  from group_hom.hom_one [of D C h] and hom_mult [OF y x] and y_x and y show "\<exists>y\<in>carrier D. h y \<otimes>\<^bsub>C\<^esub> h x = \<one>\<^bsub>C\<^esub>" by auto
next
  show "?compl\<in> hom_completion ?IMG ?IMG"
  proof (intro hom_completionI homI, auto)
    show "?compl \<in> completion_fun2 ?IMG ?IMG" unfolding completion_fun2_def completion_def by (auto simp add: expand_fun_eq)
  next
    fix x
    assume x: "x \<in> 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 "(differ\<^bsub>D\<^esub>) x" "carrier D" h] and diff_group_hom_diff.diff_hom_h [of D C h]
    show "(differ\<^bsub>C\<^esub>) (h x) \<in> ?img_set" unfolding image_def by (simp add: expand_fun_eq)
  next
    fix x y
    assume x: "x \<in> carrier D" and y: "y \<in> carrier D"
    from hom_mult [OF x y] and D.m_closed [OF x y]
    have "?compl (h x \<otimes>\<^bsub>C\<^esub> h y) = (differ\<^bsub>C\<^esub>) (h (x \<otimes> 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 "\<dots> = (differ\<^bsub>C\<^esub>) (h x) \<otimes>\<^bsub>C\<^esub> (differ\<^bsub>C\<^esub>) (h y)" by simp
    finally show "?compl (h x \<otimes>\<^bsub>C\<^esub> h y) = (differ\<^bsub>C\<^esub>) (h x) \<otimes>\<^bsub>C\<^esub> (differ\<^bsub>C\<^esub>) (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 "differ\<^bsub>C\<^esub>"] and prems show "\<And>x. ?compl (?compl x) = \<one>\<^bsub>C\<^esub>"
    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 \<in> hom_diff D C"
  and g_hom_diff: "g \<in> hom_diff C D"
  and h_hom_compl: "h \<in> hom_completion D D"
  and fg: "f \<circ> g = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)"
  and gf_dh_hd: "(\<lambda>x. if x \<in> carrier D then (g \<circ> f) x \<otimes> (if x \<in> carrier D then ((differ) \<circ> h) x \<otimes> (h \<circ> (differ)) x else \<one>\<^bsub>D\<^esub>) else \<one>\<^bsub>D\<^esub>) = 
  (\<lambda>x. if x \<in> carrier D then id x else \<one>\<^bsub>D\<^esub>)"
  and fh: "f \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)"
  and hg: "h \<circ> g = (\<lambda>x. if x \<in> carrier C then \<one>\<^bsub>D\<^esub> else \<one>\<^bsub>D\<^esub>)"
  and hh: "h \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>D\<^esub> else \<one>\<^bsub>D\<^esub>)"

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

lemma reductionI:
  includes struct D + struct C 
  assumes src_diff_group: "diff_group D"
  and trg_diff_group: "diff_group C"
  assumes "f \<in> hom_diff D C"
  and "g \<in> hom_diff C D"
  and "h \<in> hom_completion D D"
  and "f \<circ> g = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)"
  and "(\<lambda>x. if x \<in> carrier D then (g \<circ> f) x \<otimes> (if x \<in> carrier D then ((differ) \<circ> h) x \<otimes> (h \<circ> (differ)) x else \<one>\<^bsub>D\<^esub>) else \<one>\<^bsub>D\<^esub>) = 
  (\<lambda>x. if x \<in> carrier D then id x else \<one>\<^bsub>D\<^esub>)"
  and "f \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>C\<^esub> else \<one>\<^bsub>C\<^esub>)"
  and "h \<circ> g = (\<lambda>x. if x \<in> carrier C then \<one>\<^bsub>D\<^esub> else \<one>\<^bsub>D\<^esub>)"
  and "h \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>D\<^esub> else \<one>\<^bsub>D\<^esub>)"
  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 "\<cong>\<^bsub>diff\<^esub>" 60)
  "D \<cong>\<^bsub>diff\<^esub> C == {h. h \<in> hom_diff D C & bij_betw h (carrier D) (carrier C)}"

lemma iso_diffI: assumes closed: "\<And>x. x \<in> carrier D \<Longrightarrow> h x \<in> carrier C"
  and mult: "\<And>x y. \<lbrakk>x \<in> carrier D; y \<in> carrier D\<rbrakk> \<Longrightarrow> h (x \<otimes>\<^bsub>D\<^esub> y) = h x \<otimes>\<^bsub>C\<^esub> h y"
  and complect: "\<exists>g. h = (\<lambda>x. if x \<in> carrier D then g x else \<one>\<^bsub>C\<^esub>)"
  and coherent: "\<And>x. h ((differ\<^bsub>D\<^esub>) x) = (differ\<^bsub>C\<^esub>) (h x)"
  and inj_on: "\<And>x y. \<lbrakk> x \<in> carrier D;  y \<in> carrier D;  h (x) = h (y) \<rbrakk> \<Longrightarrow> x=y"
  and image: "\<And>y. y\<in>carrier C \<Longrightarrow> \<exists>x \<in> carrier D. y = h (x)"
  shows "h \<in> D \<cong>\<^bsub>diff\<^esub> 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 "\<cong>\<^bsub>invdiff\<^esub>"*)

definition
  iso_inv_diff :: "('a, 'c) diff_group_scheme => ('b, 'd) diff_group_scheme => (('a => 'b) \<times> ('b => 'a)) set"  (infixr "\<cong>\<^bsub>invdiff\<^esub>" 60)
  where "D \<cong>\<^bsub>invdiff\<^esub> C == {(f, g). f \<in> (D \<cong>\<^bsub>diff\<^esub> C) & g \<in> (C \<cong>\<^bsub>diff\<^esub> D) & (f \<circ> g = completion C C id) & (g \<circ> f = completion D D id)}"

lemma iso_inv_diffI: assumes f: "f \<in> (D \<cong>\<^bsub>diff\<^esub> C)" and g: "g \<in> (C \<cong>\<^bsub>diff\<^esub> D)" and fg_id: "(f \<circ> g = completion C C id)" 
  and gf_id: "(g \<circ> f = completion D D id)" shows "(f, g) \<in> (D \<cong>\<^bsub>invdiff\<^esub> 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') \<in> (D \<cong>\<^bsub>invdiff\<^esub> C)" shows "f \<in> (D \<cong>\<^bsub>diff\<^esub> C)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_iso_diff2: assumes f_f': "(f, f') \<in> (D \<cong>\<^bsub>invdiff\<^esub> C)" shows "f' \<in> (C \<cong>\<^bsub>diff\<^esub> D)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_inv_diff_id: assumes f_f': "(f, f') \<in> (D \<cong>\<^bsub>invdiff\<^esub> C)" shows "f' \<circ> 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') \<in> (D \<cong>\<^bsub>invdiff\<^esub> C)" shows "f \<circ> 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') \<in> (D \<cong>\<^bsub>invdiff\<^esub> C)" shows "(f', f) \<in> (C \<cong>\<^bsub>invdiff\<^esub> D)"
  using f_f' unfolding iso_inv_diff_def by simp

lemma iso_diff_hom_diff: assumes h: "h \<in> D \<cong>\<^bsub>diff\<^esub> C" shows "h \<in> 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 \<circ> f \<in> hom_diff D D"
proof (unfold hom_diff_def hom_completion_def, auto)
  from f_hom_diff and g_hom_diff have f: "f \<in> completion_fun2 D C" and g: "g \<in> completion_fun2 C D"
    by (unfold hom_diff_def hom_completion_def, simp_all)
  show "g \<circ> f \<in> completion_fun2 D D"
  proof (unfold completion_fun2_def, simp, intro exI [of _ "g \<circ> f"], unfold completion_def, auto simp add: expand_fun_eq)
    fix x assume x: "x \<notin> 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 \<circ> f \<in> hom D D"
  proof (intro homI)
    fix x
    assume x: "x \<in> carrier D"
    from hom_diff_closed [OF f_hom_diff x] and hom_diff_closed [OF g_hom_diff, of "f x"] show "(g \<circ> f) x \<in> carrier D" by simp
  next
    fix x y
    assume x: "x \<in> carrier D" and y: "y \<in> 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 \<circ> f) (x \<otimes> y) = (g \<circ> f) x \<otimes> (g \<circ> 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 "differ\<^bsub>C\<^esub>" f] and o_assoc [of differ g f] show "g \<circ> f \<circ> differ = differ \<circ> (g \<circ> f)" by simp
qed

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

lemma (in reduction) D_D_g_f_group_hom: shows "group_hom D D (g \<circ> 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 \<circ> f"} 
  with the operations inherited from @{term D} is a differential group.*}

lemma (in reduction) image_g_f_diff_group: shows "diff_group \<lparr>carrier = image (g \<circ> f) (carrier D), mult = mult D, one = one D, 
  diff = completion \<lparr>carrier = image (g \<circ> f) (carrier D), mult = mult D, one = one D, diff = diff D \<rparr> D (diff D) \<rparr>"
  using diff_group_hom_diff.image_diff_group [of D D "g \<circ> 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 \<circ> f) (carrier D)"

definition diff_group_im_gf where "diff_group_im_gf == \<lparr>carrier = image (g \<circ> f) (carrier D), mult = mult D, one = one D, 
  diff =completion \<lparr>carrier = image (g \<circ> f) (carrier D), mult = mult D, one = one D, diff = diff D\<rparr> D (diff D)\<rparr>"

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 \<in> (C \<cong>\<^bsub>diff\<^esub> diff_group_im_gf)"
proof (intro iso_diffI)
  fix x
  assume x: "x \<in> carrier C"
  show "g x \<in> 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 \<in> carrier D" by simp
  qed
next
  fix x y
  assume x: "x \<in> carrier C" and y: "y \<in> carrier C"
  from hom_diff_mult [OF g_hom_diff x y] and diff_group_im_gf_def show "g (x \<otimes>\<^bsub>C\<^esub> y) = g x \<otimes>\<^bsub>diff_group_im_gf\<^esub> 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 " \<exists>ga. g = (\<lambda>x. if x \<in> carrier C then ga x else \<one>\<^bsub>diff_group_im_gf\<^esub>)"
    unfolding hom_diff_def hom_completion_def completion_fun2_def expand_fun_eq by (intro exI [of _ g]) auto
next
  fix x
  show "g ((differ\<^bsub>C\<^esub>) x) = (differ\<^bsub>diff_group_im_gf\<^esub>) (g x)"
  proof (cases "x \<in> carrier C")
    case True then have "g x \<in> (g \<circ> 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 \<in> carrier D" by simp
    qed
    then have "(differ\<^bsub>diff_group_im_gf\<^esub>) (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 ((differ\<^bsub>C\<^esub>) x) =(differ\<^bsub>diff_group_im_gf\<^esub>) (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 "differ\<^bsub>C\<^esub>" C] have "(differ\<^bsub>C\<^esub>) x = \<one>\<^bsub>C\<^esub>" by simp
    with group_hom.hom_one [of C D g] and C_D_g_group_hom
    have "g ((differ\<^bsub>C\<^esub>) x) = \<one>\<^bsub>D\<^esub>" 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: "(differ\<^bsub>diff_group_im_gf\<^esub>) (g x) = \<one>\<^bsub>D\<^esub>"
     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 ((differ\<^bsub>C\<^esub>) x) = (differ\<^bsub>diff_group_im_gf\<^esub>) (g x)" by simp
  qed
next
  fix x y
  assume x: "x \<in> carrier C" and y: "y \<in> 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 \<in> carrier diff_group_im_gf" then have "y \<in> (g \<circ> f)` (carrier D)" by (unfold diff_group_im_gf_def, simp)
  then obtain x where "g (f x) = y" and x: "x \<in> carrier D" by auto
  with bexI [of "\<lambda>x. (y = g x)" "f x" "carrier C"] and hom_diff_closed [OF f_hom_diff x] show "\<exists>x\<in>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 \<circ> f"}*}

lemma (in lemma_2_2_11) lemma_2_2_11_second_part: shows "completion diff_group_im_gf C f \<in> (diff_group_im_gf \<cong>\<^bsub>diff\<^esub> C)"
(is "?compl_f \<in> (?IM \<cong>\<^bsub>diff\<^esub> C)")
proof (intro iso_diffI)
  fix x
  assume x: "x \<in> carrier ?IM" then have x_im: "x \<in> (g \<circ> f)` (carrier D)" by (unfold diff_group_im_gf_def, simp)
  then obtain y where gf_y: "g (f y) = x" and y: "y \<in> 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 \<in> carrier C" by simp
next
  fix x y
  assume x: "x \<in> carrier ?IM" and y: "y \<in> carrier ?IM" then obtain x' y' where gf_x': "g (f x') = x" and gf_y': "g (f y') = y" 
    and x': "x' \<in> carrier D" and y': "y' \<in> 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 \<otimes>\<^bsub>?IM\<^esub> y) = f (x \<otimes>\<^bsub>D\<^esub> y)" unfolding diff_group_im_gf_def completion_def by auto
  also from gf_x' gf_y' have "\<dots> = f (g (f x') \<otimes>\<^bsub>D\<^esub> 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 "\<dots> = f (g (f x')) \<otimes>\<^bsub>C\<^esub> f (g (f y'))" by simp
  also from gf_x' gf_y' and x' y' have "\<dots> = ?compl_f x \<otimes>\<^bsub>C\<^esub> ?compl_f y" unfolding completion_def diff_group_im_gf_def by auto
  finally show "?compl_f (x \<otimes>\<^bsub>?IM\<^esub> y) = ?compl_f x \<otimes>\<^bsub>C\<^esub> ?compl_f y" by simp
next
  show "\<exists>g. ?compl_f = (\<lambda>x. if x \<in> carrier ?IM then g x else \<one>\<^bsub>C\<^esub>)" unfolding completion_def by (rule exI [of _ f]) simp
next
  fix x
  show "?compl_f ((differ\<^bsub>?IM\<^esub>) x) = (differ\<^bsub>C\<^esub>) (?compl_f x)"
  proof (cases "x \<in> carrier ?IM")
    case True then obtain y where y: "y \<in> carrier D" and gf_y: "x = g (f y)" unfolding diff_group_im_gf_def by auto
    then have "?compl_f ((differ\<^bsub>?IM\<^esub>) x) = ?compl_f ((differ) (g (f y)))" unfolding completion_def diff_group_im_gf_def by auto
    also have "\<dots> = 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 "\<dots> = (differ\<^bsub>C\<^esub>) (f (g (f y)))" by (simp add: expand_fun_eq)
    also from y and gf_y have "\<dots> = (differ\<^bsub>C\<^esub>) (?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\<^bsub>?IM\<^esub>) 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> \<in> (g \<circ> f)` carrier D" unfolding image_def by simp
    with diff_one have "?compl_f ((differ\<^bsub>?IM\<^esub>) 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 "\<dots> = \<one>\<^bsub>C\<^esub>" by simp
    finally have l_h_s: "?compl_f ((differ\<^bsub>?IM\<^esub>) x) = \<one>\<^bsub>C\<^esub>" by simp
    from False have diff_one: "(differ\<^bsub>C\<^esub>) (?compl_f x) = (differ\<^bsub>C\<^esub>) \<one>\<^bsub>C\<^esub>" unfolding completion_def by simp
    also from C.diff_hom and group_hom.hom_one [of C C "(differ\<^bsub>C\<^esub>)"] and C_diff_group have "\<dots> = \<one>\<^bsub>C\<^esub>"
      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: "(differ\<^bsub>C\<^esub>) (?compl_f x) = \<one>\<^bsub>C\<^esub>" by simp
    from l_h_s and r_h_s show ?thesis by simp
  qed
next
  fix x y
  assume x: "x \<in> carrier ?IM" and y: "y \<in> carrier ?IM" then obtain x' y' where gf_x': "g (f x') = x" and gf_y': "g (f y') = y" 
    and x': "x' \<in> carrier D" and y': "y' \<in> 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 \<in> carrier C"
  from fg have fg_idemp: "(f \<circ> g) \<circ> (f \<circ> g) = (f \<circ> g)" by (simp add: expand_fun_eq)
  with bexI [of "\<lambda>x. (y = f (g (f x)))" "g y" "carrier D"] and hom_diff_closed [OF g_hom_diff y] and fg and y
  show "\<exists>x\<in>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 \<circ> g = (\<lambda>x. if x \<in> carrier C then id x else \<one>\<^bsub>C\<^esub>)"
(is "?compl_f \<circ> g = ?id_C")
proof (unfold expand_fun_eq, auto)
  fix x
  assume x: "x \<in> carrier C" with diff_group_im_gf_def and image_def [of "(g \<circ> f)" "carrier D"] 
    and bexI [of  "\<lambda>y. (g x = (g \<circ> 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 \<notin> 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>\<^bsub>C\<^esub>" 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 \<circ> completion diff_group_im_gf C f = (\<lambda>x. if x \<in> carrier diff_group_im_gf then id x else \<one>\<^bsub>diff_group_im_gf\<^esub>)"
(is "g \<circ> ?compl_f = ?id_IM")
proof (unfold diff_group_im_gf_def completion_def expand_fun_eq, auto)
  fix x
  assume x: "x \<in> 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>\<^bsub>C\<^esub> = \<one>\<^bsub>D\<^esub>" 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) \<in> (C \<cong>\<^bsub>invdiff\<^esub> 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