Theory lemma_2_2_14

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


header{*Propositions 2.2.12, 2.2.13 and Lemma 2.2.14 in Aransay's memoir*}

theory lemma_2_2_14 imports lemma_2_2_11
  begin

subsection{*Previous definitions for Lemma 2.2.14*}

text{*In the following we introduce some locale specifications and definitions that will ease our proofs*}
text{*For instance, we introduce the locale @{text ring_endomorphisms} which will allow us to apply
  equational reasoning with endomorphisms*}
text{*In the @{text ring_endomorphisms} specification we introduce as an assumption the fact @{text ring_R},
  stating that completion endomorphisms are a ring;
  we have proved this fact in the library @{text "HomGroupCompletion.thy"} and here it should be introduced by means of
  an \emph{interpretation}, but some technical limitations in the interpretation mechanism led us to introduce this fact as an assumption*}

locale ring_endomorphisms = diff_group D + ring R +
  assumes ring_R: "R = (| carrier = hom_completion D D, mult = op o,
  one = (λx. if x ∈ carrier D then id x else \<one>),
  zero = (λx. if x ∈ carrier D then \<one> else \<one>),
  add = λf. λg. (λx. if x ∈ carrier D then f x ⊗ g x else \<one>)|)"

locale lemma_2_2_14 = ring_endomorphisms D R + var h +
  assumes h_hom: "h ∈ hom_completion D D"
  and h_nil: "h ⊗R h = \<zero>R"
  and hdh_h: "h ⊗R differ ⊗R h = h"

definition (in lemma_2_2_14)
  p where "p == (differ) ⊗R h ⊕R h ⊗R (differ)"
definition (in lemma_2_2_14)
  ker_p where "ker_p == kernel D D p"
definition (in lemma_2_2_14)
  diff_group_ker_p where "diff_group_ker_p == (| carrier = kernel D D p, mult = mult D, one = one D,
  diff = completion (|carrier = kernel D D p, mult = mult D, one = one D, diff = diff D|)), D (diff D)|)),"
definition (in lemma_2_2_14)
  inc_ker_p where "inc_ker_p == (λx. if x ∈ (kernel D D p) then x else \<one>D)"

lemma (in ring_endomorphisms) D_diff_group: shows "diff_group D" using prems by (unfold ring_endomorphisms_def, simp)

lemma (in ring_endomorphisms) diff_in_R [simp]: shows "differ ∈ carrier R" using D.diff_hom and ring_R by simp

lemma (in lemma_2_2_14) h_in_R [simp]: shows "h ∈ carrier R" using h_hom and ring_R by simp

lemma (in lemma_2_2_14) p_in_R [simp]: shows "p ∈ carrier R" using p_def by simp

lemma (in ring_endomorphisms) diff_nilpot[simp]: shows "differ ⊗R differ = \<zero>R" using ring_R and D.diff_nilpot by simp

subsection{*Proposition 2.2.12*}

text{*The following two lemmas correspond to Proposition 2.2.12 in Aransay's memoir*}

lemma (in lemma_2_2_14) p_in_hom_diff: shows "p ∈ hom_diff D D"
proof (unfold hom_diff_def, simp, intro conjI)
  from ring_R and p_in_R show "p ∈ hom_completion D D" by simp
next
  show "p o differ = differ o p"
  proof -
      (*Probably some of the steps in the calcultation could be even avoided; the reason to keep them is to follow the proof in the memoir*)
    from ring_R have "p o differ = p ⊗R differ" by simp
    also from p_def have "… = ((differ) ⊗R h ⊕R h ⊗R (differ)) ⊗R differ" by simp
    also from h_in_R and diff_in_R have "… = ((differ) ⊗R h) ⊗R (differ) ⊕R (h ⊗R (differ)) ⊗R differ" by algebra
    also from h_in_R and diff_in_R have "… = (differ) ⊗R (h ⊗R (differ)) ⊕R (h ⊗R (differ)) ⊗R differ" by algebra
    also from h_in_R and diff_in_R have "… = (differ) ⊗R (h ⊗R (differ)) ⊕R h ⊗R (differ ⊗R differ)" by algebra
    also from h_in_R and diff_in_R and diff_nilpot have "… = (differ) ⊗R (h ⊗R (differ)) ⊕R \<zero>R" by algebra
    also have "… = (differ) ⊗R (h ⊗R (differ)) ⊕R (differ ⊗R differ ⊗R h)" by simp
    also from h_in_R and diff_in_R have "… = (differ) ⊗R (h ⊗R (differ)) ⊕R differ ⊗R (differ ⊗R h)" by algebra
    also from h_in_R and diff_in_R have "… = differ ⊗R (h ⊗R differ ⊕R differ ⊗R h)" by algebra
    also from h_in_R and diff_in_R have "… = differ ⊗R (differ ⊗R h ⊕R h ⊗R differ)" by algebra
    also from p_def and ring_R have "… = differ o p" by simp
    finally show ?thesis by simp
  qed
qed

lemma (in lemma_2_2_14) ker_p_diff_group: "diff_group diff_group_ker_p"
proof -
  from D_diff_group have D: "diff_group D" by simp
  from diff_group_hom_diffI [OF D D p_in_hom_diff] and diff_group_ker_p_def show ?thesis
    by (simp only: diff_group_hom_diff.kernel_diff_group)
qed

    (*I leave the two following lemmas commented because they prove the same that the previous lemma_2_2_14.p_in_hom_diff,
    but without making use of the advantages of the ring of endomorphisms. At some point, they could be used as an example of how
    the situation has improved.*)

    (*lemma mult_ones [simp]: includes group G + group G'
    assumes "f ∈ hom G G'" and "g ∈ hom G G'" and "h ∈ hom G G'"
    and "f x = \<one>G'" and "g y = \<one>G'" and "h z = \<one>G'" shows "f x ⊗G' g y = h z"
    proof -
    from prems show ?thesis by simp
    qed
    *)

    (*
    lemma d_h_h_d_is_hom_diff: includes diff_group D
    assumes  "h ∈ hom_completion D D" and "h o differ o h = h" and "h o h = (λx. \<one>)"
    shows "(λx. if x ∈ carrier D then (differ o h) (x) ⊗ (h o differ) (x) else \<one>) ∈ hom_diff D D"
    proof (unfold hom_diff_def, auto)
    from prems show "(λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) ∈ hom_completion D D"
    by (unfold hom_diff_def diff_group_def diff_group_axioms_def hom_completion_def
    completion_fun2_def completion_def hom_def Pi_def, auto simp add: m_ac)
    next
    show "(λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) o differ =
    differ o (λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>)"
    proof (rule ext)
    fix x
    show " ((λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) o differ) x =
    (differ o (λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>)) x"
    proof (cases "x ∈ carrier D")
    case True
    from prems show "((λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) o differ) x =
    (differ o (λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>)) x"
    proof  (auto simp add: expand_fun_eq)
    show "(differ) (h ((differ) x)) ⊗ h ((differ) ((differ) x)) = (differ) ((differ) (h x) ⊗ h ((differ) x))"
    proof -
    have l_h_s: "(differ) (h ((differ) x)) ⊗ h ((differ) ((differ) x)) = (differ) (h ((differ) x))"
    proof -
    have "(differ) (h ((differ) x)) ⊗ h ((differ) ((differ) x)) = (differ) (h ((differ) x)) ⊗ \<one>"
    proof -
    have "h ((differ) ((differ) x)) = \<one>"
    proof -
    have "h ((differ) ((differ) x)) = h (\<one>)"
    proof -
    from prems have "(differ) ((differ) x) = \<one>"
    by (unfold diff_group_axioms_def expand_fun_eq, simp)
    then show ?thesis by simp
    qed
    also from prems have "… = \<one>"
    by (intro group_hom.hom_one [of D D h], unfold group_hom_def group_hom_axioms_def hom_completion_def, clarify)
    finally show ?thesis by simp
    qed
    then show ?thesis by simp
    qed
    also from prems have "… = (differ) (h ((differ) x))"
    by (intro r_one, unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    finally show ?thesis by simp
    qed
    moreover
    have r_h_s: "(differ) ((differ) (h x) ⊗ h ((differ) x)) = (differ) (h ((differ) x))"
    proof -
    from prems have "(differ) ((differ) (h x) ⊗ h ((differ) x)) = (differ) ((differ) (h x)) ⊗  (differ) (h ((differ) x))"
    by (intro hom_mult) (unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    also have "… = \<one> ⊗ (differ) (h ((differ) x))"
    proof -
    from prems have "(differ) ((differ) (h x)) = \<one>"
    by (unfold diff_group_axioms_def, auto simp add: expand_fun_eq)
    then show ?thesis by simp
    qed
    also from prems have "… = (differ) (h ((differ) x))"
    by (intro l_one, unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    finally show ?thesis by simp
    qed
    ultimately show ?thesis by simp
    qed
    next
    assume "(differ) x ∉ carrier D"
    from prems show "\<one> = (differ) ((differ) (h x) ⊗ h ((differ) x))"
    by (unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    qed
    next
    case False
    from prems show "((λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) o differ) x =
    (differ o (λx. if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>)) x"
    proof (unfold diff_group_axioms_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def,
    auto simp add: expand_fun_eq)
    fix g ga
    assume "∀x. x ∈ carrier D --> g x ∈ carrier D" and "∀x. x ∈ carrier D --> ga x ∈ carrier D"
    and "∀x∈carrier D. ∀y∈carrier D. ga (x ⊗ y) = ga x ⊗ ga y" and "∀x∈carrier D. ∀y∈carrier D. g (x ⊗ y) = g x ⊗ g y"
    from prems show "g (ga \<one>) ⊗ ga \<one> = g \<one>"
    proof (intro mult_ones [of D D g ga g _ _ _], auto simp add: hom_completion_def hom_def Pi_def group_def)
    show "g (ga \<one>) = \<one>"
    proof -
    from prems have "ga \<one> = \<one>" by (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
    with prems show ?thesis by (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
    qed
    next
    from prems show "ga \<one> = \<one>" by (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
    next
    from prems show "g \<one> = \<one>" by (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
    qed
    qed
    qed
    qed
    qed
    *)

subsection{*Proposition 2.2.13*}

text{*The following lemma corresponds to Proposition 2.2.13 in Aransay's Ph.D.*}

lemma (in ring_endomorphisms) image_subset: assumes p_in_R: "p ∈ carrier R" and p_idemp: "p ⊗R p = p"
  shows "image (\<one>R \<ominus>R p) (carrier D) ⊆ kernel D D p"
proof (unfold image_def kernel_def, auto)
  fix x
  assume x_in_D: "x ∈ carrier D"
  from minus_closed [OF one_closed p_in_R] and ring_R have one_minus_p: "(\<one>R \<ominus>R p) ∈ hom_completion D D" by simp
  from hom_completion_closed [OF one_minus_p x_in_D] show "(\<one>R \<ominus>R p) x ∈ carrier D" by simp
next
  fix x
  assume "x ∈ carrier D"
  show "p ((\<one>R \<ominus>R p) x) = \<one>"
  proof -
      (*This proof could be compared with the mathematical proof in the Ph.D., both are almost identical*)
    from p_in_R have "p ⊗R (\<one>R \<ominus>R p) = p ⊗R \<one>R \<ominus>R  p ⊗R p" by algebra
    also from p_in_R and p_idemp have "… = p \<ominus>R  p" by simp (*Here "by algebra" did not work*)
    also from p_in_R have "… = \<zero>R" by algebra
    finally have "p ⊗R (\<one>R \<ominus>R p) = \<zero>R" by simp
    then have "(p ⊗R (\<one>R \<ominus>R p))(x) = \<zero>R (x)" by (simp only: expand_fun_eq)
    with ring_R show ?thesis by simp
  qed
qed

lemma (in group_hom) ker_m_closed: assumes x_in_ker: "x ∈ kernel G H h" and y_in_ker: "y ∈ kernel G H h"
  shows "x ⊗ y ∈ kernel G H h"
  using x_in_ker and y_in_ker by (unfold kernel_def, auto)

subsection{*Lemma 2.2.14*}

text{*The following lemma, proved in a generic ring, will help us to prove that @{term "p = d ⊗R h ⊕R h ⊗R d"} is a projector*}

lemma (in ring) idemp_prod: assumes a: "a ∈ carrier R" and b: "b ∈ carrier R" and a_idemp: "a ⊗ a = a" and b_idemp: "b ⊗ b = b"
  and a_b: "a ⊗ b = \<zero>" and b_a: "b ⊗ a = \<zero>" shows "(a ⊕ b) ⊗ (a ⊕ b) = (a ⊕ b)"
  using a b a_idemp b_idemp a_b b_a by algebra

text{*The following lemma corresponds to the first part of Lemma 2.2.14 as stated in Aransay's memoir*}

lemma (in lemma_2_2_14) p_projector: shows "p ⊗R p = p"
proof -
  from p_def have "p ⊗R p = (differ ⊗R h ⊕R h ⊗R differ) ⊗R (differ ⊗R h ⊕R h ⊗R differ)"
    (is "p ⊗R p = (?d_h ⊕R ?h_d) ⊗R (?d_h ⊕R ?h_d)") by simp
  also have "… = (?d_h ⊕R ?h_d)"
  proof (intro ring.idemp_prod)
    from ring_endomorphisms_def [of D R] and prems show "ring R" by (unfold lemma_2_2_14_def, simp)
    show"?d_h ∈ carrier R" by simp
    show "?h_d ∈ carrier R" by simp
    from R.m_assoc [of differ h "differ ⊗R h"] and R.m_assoc [of h differ h] and diff_in_R h_in_R hdh_h
    show "?d_h ⊗R ?d_h = ?d_h" by simp
    from R.m_assoc [of "h ⊗R differ" h differ] and diff_in_R and h_in_R and hdh_h show "?h_d ⊗R ?h_d = ?h_d" by simp
    from h_nil and R.m_assoc [of differ  h "h ⊗R differ"] and sym [OF R.m_assoc [of h h differ]] show "?d_h ⊗R ?h_d = \<zero>R" by simp
    from h_nil and R.m_assoc [of h differ "differ ⊗R h"] and sym [OF R.m_assoc [of differ differ h]] show "?h_d ⊗R ?d_h = \<zero>R" by simp
  qed
  also from p_def have "… = p" by simp
  finally show ?thesis by simp
qed

(*The two following lemmas about the minus operation are to be added to the theory Ring; meanwhile I introduce them here*)

lemma (in abelian_group) minus_equality:
  "[| x ∈ carrier G; y ∈ carrier G; y ⊕ x = \<zero> |] ==> \<ominus> x = y"
  using group.inv_equality [OF a_group] by (auto simp add: a_inv_def)

lemma (in abelian_monoid) minus_unique:
  "[| x ∈ carrier G; y ∈ carrier G; y' ∈ carrier G; y ⊕ x = \<zero>; x ⊕ y' = \<zero> |] ==> y = y'"
  using monoid.inv_unique [OF a_monoid] inv_equality unfolding a_inv_def inv_equality by simp

text{*When proving that @{term R} is a ring, you have to give an element such that it satisfies the condition of the additive inverse;
  nevertheless, when you really want to know the explicit expression of this inverse, there is no direct way to recover it.
  This makes a difference with the rest of constants and operations in a ring, such as the addition, the product, or the units.*}

text{*This is the reason why we had to introduce the following lemma, giving us the expression of the additive inverse of any
  element @{term a} in @{term R}*}

lemma (in ring_endomorphisms) minus_interpret: assumes a: "a ∈ carrier R"
  shows "(\<ominus>R a) = (λx. if x ∈ carrier D then invD (a x) else \<one>D)"
proof (rule abelian_group.minus_equality)
  from prems show "abelian_group R" by intro_locales
next
  show "a ∈ carrier R" by assumption
next
  from ring_R and a and comm_group.hom_completion_inv_is_hom_completion [of D a] and D_diff_group
  show inv_in_R: "(λx. if x ∈ carrier D then inv a x else \<one>) ∈ carrier R" by (unfold diff_group_def comm_group_def, simp)
next
  from ring_R and a and hom_completion_closed [of a D D] show "(λx. if x ∈ carrier D then inv a x else \<one>) ⊕R a = \<zero>R"
    by (auto simp add: expand_fun_eq)
qed

text{*The following proof is a nice example of how we can take advantage of reasoning with endomorphisms as elements of a ring,
  making use of the automatic tactics for this structure @{text "(by algebra, …)"}*}

lemma (in lemma_2_2_14) one_minus_p_hom_diff: shows "\<one>R \<ominus>R p ∈ hom_diff D D"
proof (unfold hom_diff_def, simp, intro conjI)
  from R.minus_closed [OF R.one_closed p_in_R] and ring_R show "\<one>R \<ominus>R p ∈ hom_completion D D" by simp
next
  show "\<one>R \<ominus>R p o differ = differ o \<one>R \<ominus>R p"
  proof -
    from ring_R have "\<one>R \<ominus>R p o differ = (\<one>R \<ominus>R p) ⊗R differ" by simp
    also from diff_in_R and p_in_R have "… = (differ) \<ominus>R (p ⊗R differ)" by algebra
    also from ring_R and hom_diff_coherent [OF p_in_hom_diff] have "… = differ \<ominus>R (differ ⊗R p)" by simp
    also from sym [OF R.r_one [of differ]] have "… = (differ ⊗R \<one>R) \<ominus>R (differ ⊗R p)" by simp
    also from diff_in_R and p_in_R have "… = differ ⊗R (\<one>R \<ominus>R p)" by algebra
    also from ring_R have "… = differ o (\<one>R \<ominus>R p)" by simp
    finally  show ?thesis by simp
  qed
qed

text{*The following lemma allows us to change the codomain of a homomorphism, whenever its image set is a subset of the new codomain*}

lemma (in diff_group_hom_diff) h_image_hom_diff: assumes image_subset: "image h (carrier D) ⊆ C'"
  shows "h ∈ hom_diff D (| carrier = C', mult = mult C, one = one C,
  diff = completion (|carrier = C', mult = mult C, one = one C, diff = diff C|)), C (diff C)|)),"
proof -
  from diff_group_hom_diff.hom_diff_h [of D C h] and prems have h_hom_diff: "h ∈ hom_diff D C" by simp
  with image_subset and group_hom.hom_one [of C C "differC"] and diff_group_hom_diff.group_hom_C_C_differ [of D C h] and prems
  show ?thesis by (unfold hom_diff_def hom_completion_def hom_def completion_fun2_def completion_def image_def Pi_def subset_def,
      auto simp add: expand_fun_eq) auto
qed

text{*We denote as inclusion, @{term inc}, a homomorphism from a subgroup into a group such that it maps every element to the
  same element*}

lemma inc_ker_hom_diff: includes diff_group D
  assumes h_hom_diff: "h ∈ hom_diff D D"
  shows "(λx. if x ∈ kernel D D h then x else \<one>D) ∈
  hom_diff (|carrier = kernel D D h, mult = mult D, one = one D,
  diff = completion (|carrier = kernel D D h, mult = mult D, one = one D, diff = diff D|)), D (diff D)|)), D"
  (is "?inc_KER ∈ hom_diff ?KER _")
proof (unfold hom_diff_def hom_completion_def, auto)
  show "?inc_KER ∈ completion_fun2 ?KER D" by (unfold completion_fun2_def, auto simp add: expand_fun_eq)
next
  show "?inc_KER ∈ hom ?KER D"
  proof (rule homI, auto)
    fix x
    assume "x ∈ kernel D D h" then show "x ∈ carrier D" by (unfold kernel_def, simp)
  next
    fix x y
    assume x_ker: "x ∈ kernel D D h" and y_ker: "y ∈ kernel D D h" and x_times_y: "x ⊗ y ∉ kernel D D h"
    from group_hom.ker_m_closed [of D D h x y] and prems show "\<one> = x ⊗ y"
      by (unfold group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def diff_group_def comm_group_def, simp)
  qed
next
  show "?inc_KER o completion (|carrier = kernel D D h, mult = mult D, one = one D, diff = diff D|)), D (differ) = differ o ?inc_KER"
    (is "?inc_KER o ?compl_diff = differ o ?inc_KER")
  proof (rule ext)
    fix x
    show "(?inc_KER o ?compl_diff) x = (differ o ?inc_KER) x"
    proof (cases "x ∈ kernel D D h")
      case True
      from True and diff_group.diff_hom [of D] and hom_completion_closed [of "differ" D D x] and
        hom_diff_def [of D D] and h_hom_diff and expand_fun_eq [of "h o differ" "differ o h"] and group_hom.hom_one [of D D differ]
        and prems
      show "(?inc_KER o ?compl_diff) x = (differ o ?inc_KER) x"
        by (unfold diff_group_def comm_group_def group_hom_def
          group_hom_axioms_def kernel_def subset_def hom_diff_def hom_completion_def, simp)
    next
      case False
      from False and diff_group.diff_hom [of D] and group_hom.hom_one [of D D differ] and prems
      show "(?inc_KER o ?compl_diff) x = (differ o ?inc_KER) x"
        by (unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def hom_completion_def, auto)
    qed
  qed
qed

text{*The following lemma corresponds to the second part of Lemma 2.2.14 in Aransay's memoir; we prove that a given triple
  of homomorphisms is a reduction*}

lemma (in lemma_2_2_14) lemma_2_2_14: shows "reduction D diff_group_ker_p (\<one>R \<ominus>R p) inc_ker_p h"
  (is "reduction D ?KER (\<one>R \<ominus>R p) ?inc_KER h")
proof (intro reductionI)
  from D_diff_group show "diff_group D" by simp
next
  from D_diff_group diff_group_hom_diff.kernel_diff_group [of D D p] and diff_group_ker_p_def and diff_group_hom_diffI [OF _ _ p_in_hom_diff]
  show "diff_group ?KER" by simp
next
  from  diff_group_hom_diff.h_image_hom_diff [of D D "\<one>R \<ominus>R p" "kernel D D p"] and diff_group_hom_diffI [OF _ _ one_minus_p_hom_diff]
    and image_subset [OF p_in_R p_projector] and D_diff_group and diff_group_ker_p_def show "\<one>R \<ominus>R p ∈ hom_diff D ?KER" by simp
next
  from D_diff_group and inc_ker_hom_diff [OF _ p_in_hom_diff] and diff_group_ker_p_def and inc_ker_p_def
  show "?inc_KER ∈ hom_diff ?KER D" by simp
next
  from h_hom show "h ∈ hom_completion D D" by simp
next
    (*Property a) in the thesis*)
  show "\<one>R \<ominus>R p o ?inc_KER = (λx. if x ∈ carrier ?KER then id x else \<one>?KER)"
    (is "\<one>R \<ominus>R p o ?inc_KER = ?id_KER")
  proof -
      (*First we unfold the function (id - p) o ?inc_KER and then apply expand_fun_eq*)
      (*There could be a way to prove the same without unfolding the homomorphisms?*)
    from p_in_R have "(\<one>R \<ominus>R p) = (\<one>R ⊕R (\<ominus>R p))" by algebra
    also from ring_R and minus_interpret [OF p_in_R]
    have "… = (λx. if x ∈ carrier D then (λx. if x ∈ carrier D then id x else \<one>D) x
      ⊗ (λx. if x ∈ carrier D then inv p x else \<one>D) x else \<one>D)" by simp
    finally have one_minus_p: "(\<one>R \<ominus>R p) = (λx. if x ∈ carrier D then (λx. if x ∈ carrier D then id x else \<one>D) x
      ⊗ (λx. if x ∈ carrier D then inv p x else \<one>D) x else \<one>D)" by simp
    then show "\<one>R \<ominus>R p o ?inc_KER = ?id_KER"
    proof -
      from group_hom.hom_one [of D D p] and p_in_hom_diff and D_diff_group have "p \<one> = \<one>"
        by (unfold group_hom_def group_hom_axioms_def hom_diff_def diff_group_def comm_group_def hom_completion_def, simp)
      then have inv_p_one: "inv p \<one> = \<one>" by simp
      with one_minus_p and diff_group_ker_p_def and inc_ker_p_def show ?thesis by (auto simp add: kernel_def expand_fun_eq)
    qed
  qed
next
    (*Property b) in the memoir text*)
  show "(λx. if x ∈ carrier D then
    (?inc_KER o \<one>R \<ominus>R p) x ⊗ (if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) else \<one>) =
    (λx. if x ∈ carrier D then id x else \<one>)"
    (*The expression corresponds to (is "(?inc_KER o (\<one>R \<ominus>R p) ⊗ (differ o h ⊗ h o differ))") but i did not find a suitable way to
    make it shorter*)
  proof -
    from ring_R
    have "(λx. if x ∈ carrier D then (?inc_KER o \<one>R \<ominus>R p) x ⊗ (if x ∈ carrier D then (differ o h) x ⊗ (h o differ) x else \<one>) else \<one>)
      = (?inc_KER ⊗R (\<one>R \<ominus>R p) ⊕R (differ ⊗R h ⊕R h ⊗R differ))" by (simp add: expand_fun_eq)
    also have "… = (\<one>R \<ominus>R p) ⊕R (differ ⊗R h ⊕R h ⊗R differ)"
    proof -
      from ring_R have "?inc_KER ⊗R (\<one>R \<ominus>R p) = ?inc_KER o \<one>R \<ominus>R p" by simp
      also have "?inc_KER o \<one>R \<ominus>R p = \<one>R \<ominus>R p"
      proof (rule ext)
        fix x
        show "(?inc_KER o \<one>R \<ominus>R p) x = (\<one>R \<ominus>R p) x"
        proof (cases "x ∈ carrier D")
          case True with image_subset [OF p_in_R p_projector] have "(\<one>R \<ominus>R p) x ∈ kernel D D p" by (auto simp add: imageI)
          with inc_ker_p_def show ?thesis by simp
        next
          case False from inc_ker_p_def and minus_closed [OF one_closed p_in_R] and ring_R
            and completion_closed2 [OF _ False, of "(\<one>R \<ominus>R p)" D] show ?thesis by (unfold hom_completion_def, simp)
        qed
      qed
      finally have "?inc_KER ⊗R (\<one>R \<ominus>R p) =  \<one>R \<ominus>R p" by simp
      then show "(?inc_KER ⊗R (\<one>R \<ominus>R p) ⊕R (differ ⊗R h ⊕R h ⊗R differ)) = (\<one>R \<ominus>R p) ⊕R (differ ⊗R h ⊕R h ⊗R differ)" by simp
    qed
    also from p_def have "… = (\<one>R \<ominus>R p) ⊕R p" by simp
    also from p_in_R have "… = \<one>R" by algebra
    also from ring_R have "… = (λx. if x ∈ carrier D then id x else \<one>)" by simp
    finally show ?thesis by simp
  qed
next
    (*Property c) in the thesis*)
  from prems show "\<one>R \<ominus>R p o h = (λx. if x ∈ carrier D then \<one>?KER else \<one>?KER)"
    (is "\<one>R \<ominus>R p o h = ?zero_R")
  proof -
      (*Another nice example of application of calculational reasoning with endomorphisms*)
    from ring_R have "\<one>R \<ominus>R p o h = (\<one>R \<ominus>R p) ⊗R h" by simp
    also from h_in_R and p_in_R have "… = h \<ominus>R (p ⊗R h)" by algebra
    also from p_def have "… = h \<ominus>R ((differ ⊗R h ⊕R h ⊗R differ) ⊗R h)" by simp
    also  from diff_in_R and h_in_R and hdh_h and h_nil have "… = h \<ominus>R h" by algebra
    also from h_in_R have "… = \<zero>R" by algebra
    also from ring_R and diff_group_ker_p_def have "… = ?zero_R" by simp
    finally show "\<one>R \<ominus>R p o h = ?zero_R" by simp
  qed
next
  show "h o ?inc_KER = (λx. if x ∈ carrier diff_group_ker_p then \<one> else \<one>)"
    (is "h o ?inc_KER = ?zero_KER")
      (*Property d) in the thesis*)
  proof (unfold inc_ker_p_def diff_group_ker_p_def, auto simp add: expand_fun_eq)
      (*The case where x ∈ kernel D D p is the one in the thesis; it could be seen as an example of proof that cannot be proved
      at the level of endomorphisms as elements of a ring, using only "equational reasoning"*)
    fix x
    assume x_in_ker: "x ∈ kernel D D p"
    show "h x = \<one>"
    proof -
      from hdh_h and ring_R and expand_fun_eq [of "h o differ o h" h] have "h x = h ((differ) (h x))" by auto
      also from sym [OF D.r_one [of "h ((differ) (h x))"]] and hom_completion_closed [OF h_hom, of x]
        and x_in_ker and hom_completion_closed [of differ D D "h x"] and D.diff_hom
        and hom_completion_closed [OF h_hom, of "(differ) (h x)"] have "… = h ((differ) (h x)) ⊗D \<one>" by (unfold kernel_def, simp)
      also from h_nil and ring_R have "… = h ((differ) (h x)) ⊗D h (h ((differ) x))" by (simp add: expand_fun_eq)
      also from sym [OF hom_completion_mult [OF h_hom, of "(differ) (h x)" "h ((differ) x)"]] and D.diff_hom
        and hom_completion_closed [OF h_hom, of "(differ) x"] hom_completion_closed [OF D.diff_hom, of x]
        and hom_completion_closed [OF D.diff_hom, of "h x"] hom_completion_closed [OF h_hom, of x] and x_in_ker
      have "… = h ((differ) (h x) ⊗D h ((differ) x))" by (unfold kernel_def, simp)
      also from p_def and ring_R and x_in_ker have "… = h (p (x))" by (unfold expand_fun_eq kernel_def, simp)
      also from x_in_ker have "… = h \<one>D" by (unfold kernel_def, simp)
      also from hom_completion_one [OF _ _ h_hom] and D_diff_group have "… = \<one>D"
        by (unfold diff_group_def comm_group_def group_def, simp)
      finally show "h x = \<one>" by simp
    qed
  next
      (*This is the meaningless case*)
    fix x assume "x ∉ kernel D D p"
    from hom_completion_one [OF _ _ h_hom] and D_diff_group show "h \<one>D = \<one>D" by (unfold diff_group_def comm_group_def group_def, simp)
  qed
next
    (*Property e) in the thesis*)
  from h_nil and ring_R show "h o h = (λx. if x ∈ carrier D then \<one> else \<one>)" by simp
qed

end