(*    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 = (\<lambda>x. if x \<in> carrier D then id x else \<one>), 
  zero = (\<lambda>x. if x \<in> carrier D then \<one> else \<one>),
  add = \<lambda>f. \<lambda>g. (\<lambda>x. if x \<in> carrier D then f x \<otimes> g x else \<one>)|)"

locale lemma_2_2_14 = ring_endomorphisms D R + var h +
  assumes h_hom: "h \<in> hom_completion D D"
  and h_nil: "h \<otimes>\<^bsub>R\<^esub> h = \<zero>\<^bsub>R\<^esub>"
  and hdh_h: "h \<otimes>\<^bsub>R\<^esub> differ \<otimes>\<^bsub>R\<^esub> h = h"

context lemma_2_2_14
begin

definition p where "p == (differ) \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> (differ)"

definition ker_p where "ker_p == kernel D D p"

definition diff_group_ker_p where "diff_group_ker_p == \<lparr> carrier = kernel D D p, mult = mult D, one = one D, 
  diff = completion \<lparr>carrier = kernel D D p, mult = mult D, one = one D, diff = diff D\<rparr> D (diff D)\<rparr>"
definition inc_ker_p where "inc_ker_p == (\<lambda>x. if x \<in> (kernel D D p) then x else \<one>\<^bsub>D\<^esub>)"

end

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

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

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

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

lemma (in ring_endomorphisms) diff_nilpot[simp]: shows "differ \<otimes>\<^bsub>R\<^esub> differ = \<zero>\<^bsub>R\<^esub>" 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 \<in> hom_diff D D"
proof (unfold hom_diff_def, simp, intro conjI)
  from ring_R and p_in_R show "p \<in> hom_completion D D" by simp
next
  show "p \<circ> differ = differ \<circ> 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 \<circ> differ = p \<otimes>\<^bsub>R\<^esub> differ" by simp
    also from p_def have "\<dots> = ((differ) \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> (differ)) \<otimes>\<^bsub>R\<^esub> differ" by simp
    also from h_in_R and diff_in_R have "\<dots> = ((differ) \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> (differ) \<oplus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<otimes>\<^bsub>R\<^esub> differ" by algebra
    also from h_in_R and diff_in_R have "\<dots> = (differ) \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<oplus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<otimes>\<^bsub>R\<^esub> differ" by algebra
    also from h_in_R and diff_in_R have "\<dots> = (differ) \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> differ)" by algebra
    also from h_in_R and diff_in_R and diff_nilpot have "\<dots> = (differ) \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<oplus>\<^bsub>R\<^esub> \<zero>\<^bsub>R\<^esub>" by algebra
    also have "\<dots> = (differ) \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> differ \<otimes>\<^bsub>R\<^esub> h)" by simp
    also from h_in_R and diff_in_R have "\<dots> = (differ) \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> (differ)) \<oplus>\<^bsub>R\<^esub> differ \<otimes>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h)" by algebra
    also from h_in_R and diff_in_R have "\<dots> = differ \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> differ \<oplus>\<^bsub>R\<^esub> differ \<otimes>\<^bsub>R\<^esub> h)" by algebra
    also from h_in_R and diff_in_R have "\<dots> = differ \<otimes>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)" by algebra
    also from p_def and ring_R have "\<dots> = differ \<circ> 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"
  using diff_group_hom_diffI [OF D_diff_group D_diff_group p_in_hom_diff] and diff_group_ker_p_def
  using diff_group_hom_diff.kernel_diff_group by simp

    (*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 \<in> hom G G'" and "g \<in> hom G G'" and "h \<in> hom G G'"
    and "f x = \<one>\<^bsub>G'\<^esub>" and "g y = \<one>\<^bsub>G'\<^esub>" and "h z = \<one>\<^bsub>G'\<^esub>" shows "f x \<otimes>\<^bsub>G'\<^esub> 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 \<in> hom_completion D D" and "h \<circ> differ \<circ> h = h" and "h \<circ> h = (\<lambda>x. \<one>)"
    shows "(\<lambda>x. if x \<in> carrier D then (differ \<circ> h) (x) \<otimes> (h \<circ> differ) (x) else \<one>) \<in> hom_diff D D"
    proof (unfold hom_diff_def, auto)
    from prems show "(\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) \<in> 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 "(\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) \<circ> differ =
    differ \<circ> (\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>)"
    proof (rule ext)
    fix x
    show " ((\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) \<circ> differ) x =
    (differ \<circ> (\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>)) x"
    proof (cases "x \<in> carrier D")
    case True
    from prems show "((\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) \<circ> differ) x =
    (differ \<circ> (\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>)) x"
    proof  (auto simp add: expand_fun_eq)
    show "(differ) (h ((differ) x)) \<otimes> h ((differ) ((differ) x)) = (differ) ((differ) (h x) \<otimes> h ((differ) x))"
    proof -
    have l_h_s: "(differ) (h ((differ) x)) \<otimes> h ((differ) ((differ) x)) = (differ) (h ((differ) x))"
    proof -
    have "(differ) (h ((differ) x)) \<otimes> h ((differ) ((differ) x)) = (differ) (h ((differ) x)) \<otimes> \<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 "\<dots> = \<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 "\<dots> = (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) \<otimes> h ((differ) x)) = (differ) (h ((differ) x))"
    proof -
    from prems have "(differ) ((differ) (h x) \<otimes> h ((differ) x)) = (differ) ((differ) (h x)) \<otimes>  (differ) (h ((differ) x))"
    by (intro hom_mult) (unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    also have "\<dots> = \<one> \<otimes> (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 "\<dots> = (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 \<notin> carrier D"
    from prems show "\<one> = (differ) ((differ) (h x) \<otimes> h ((differ) x))"
    by (unfold diff_group_axioms_def hom_completion_def hom_def Pi_def, auto)
    qed
    next
    case False
    from prems show "((\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) \<circ> differ) x =
    (differ \<circ> (\<lambda>x. if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> 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 "\<forall>x. x \<in> carrier D \<longrightarrow> g x \<in> carrier D" and "\<forall>x. x \<in> carrier D \<longrightarrow> ga x \<in> carrier D"
    and "\<forall>x\<in>carrier D. \<forall>y\<in>carrier D. ga (x \<otimes> y) = ga x \<otimes> ga y" and "\<forall>x\<in>carrier D. \<forall>y\<in>carrier D. g (x \<otimes> y) = g x \<otimes> g y"
    from prems show "g (ga \<one>) \<otimes> 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 \<in> carrier R" and p_idemp: "p \<otimes>\<^bsub>R\<^esub> p = p"
  shows "image (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) (carrier D) \<subseteq> kernel D D p"
proof (unfold image_def kernel_def, auto)
  fix x
  assume x_in_D: "x \<in> carrier D"
  from minus_closed [OF one_closed p_in_R] and ring_R have one_minus_p: "(\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<in> hom_completion D D" by simp
  from hom_completion_closed [OF one_minus_p x_in_D] show "(\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x \<in> carrier D" by simp
next
  fix x
  assume "x \<in> carrier D"
  show "p ((\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> 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 \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) = p \<otimes>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R \<^esub> p \<otimes>\<^bsub>R\<^esub> p" by algebra
    also from p_in_R and p_idemp have "\<dots> = p \<ominus>\<^bsub>R \<^esub> p" by simp (*Here "by algebra" did not work*)
    also from p_in_R have "\<dots> = \<zero>\<^bsub>R\<^esub>" by algebra
    finally have "p \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) = \<zero>\<^bsub>R\<^esub>" by simp
    then have "(p \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p))(x) = \<zero>\<^bsub>R\<^esub> (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 \<in> kernel G H h" and y_in_ker: "y \<in> kernel G H h"
  shows "x \<otimes> y \<in> kernel G H h"
  using x_in_ker and y_in_ker unfolding kernel_def by auto

subsection{*Lemma 2.2.14*}

text{*The following lemma, proved in a generic ring, will help us to prove that @{term "p = d \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> d"} is a projector*}

lemma (in ring) idemp_prod: assumes a: "a \<in> carrier R" and b: "b \<in> carrier R" and a_idemp: "a \<otimes> a = a" and b_idemp: "b \<otimes> b = b" 
  and a_b: "a \<otimes> b = \<zero>" and b_a: "b \<otimes> a = \<zero>" shows "(a \<oplus> b) \<otimes> (a \<oplus> b) = (a \<oplus> 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 \<otimes>\<^bsub>R\<^esub> p = p"
proof -
  from p_def have "p \<otimes>\<^bsub>R\<^esub> p = (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ) \<otimes>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)"
    (is "p \<otimes>\<^bsub>R\<^esub> p = (?d_h \<oplus>\<^bsub>R\<^esub> ?h_d) \<otimes>\<^bsub>R\<^esub> (?d_h \<oplus>\<^bsub>R\<^esub> ?h_d)") by simp
  also have "\<dots> = (?d_h \<oplus>\<^bsub>R\<^esub> ?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 \<in> carrier R" by simp
    show "?h_d \<in> carrier R" by simp
    from R.m_assoc [of differ h "differ \<otimes>\<^bsub>R\<^esub> h"] and R.m_assoc [of h differ h] and diff_in_R h_in_R hdh_h 
    show "?d_h \<otimes>\<^bsub>R\<^esub> ?d_h = ?d_h" by simp
    from R.m_assoc [of "h \<otimes>\<^bsub>R\<^esub> differ" h differ] and diff_in_R and h_in_R and hdh_h show "?h_d \<otimes>\<^bsub>R\<^esub> ?h_d = ?h_d" by simp
    from h_nil and R.m_assoc [of differ  h "h \<otimes>\<^bsub>R\<^esub> differ"] and sym [OF R.m_assoc [of h h differ]] show "?d_h \<otimes>\<^bsub>R\<^esub> ?h_d = \<zero>\<^bsub>R\<^esub>" by simp
    from h_nil and R.m_assoc [of h differ "differ \<otimes>\<^bsub>R\<^esub> h"] and sym [OF R.m_assoc [of differ differ h]] show "?h_d \<otimes>\<^bsub>R\<^esub> ?d_h = \<zero>\<^bsub>R\<^esub>" by simp
  qed
  also from p_def have "\<dots> = 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 \<in> carrier G; y \<in> carrier G; y \<oplus> x = \<zero> |] ==> \<ominus> x = y"
  using group.inv_equality [OF a_group, of y x] unfolding a_inv_def by simp

lemma (in abelian_monoid) minus_unique:
  "[| x \<in> carrier G; y \<in> carrier G; y' \<in> carrier G; y \<oplus> x = \<zero>; x \<oplus> y' = \<zero> |] ==> y = y'"
  using monoid.inv_unique [OF a_monoid, of y x] 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 \<in> carrier R" 
  shows "(\<ominus>\<^bsub>R\<^esub> a) = (\<lambda>x. if x \<in> carrier D then inv\<^bsub>D\<^esub> (a x) else \<one>\<^bsub>D\<^esub>)"
proof (rule abelian_group.minus_equality)
  from prems show "abelian_group R" by intro_locales
next
  show "a \<in> 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: "(\<lambda>x. if x \<in> carrier D then inv a x else \<one>) \<in> carrier R" unfolding diff_group_def comm_group_def by simp
next
  from ring_R and a and hom_completion_closed [of a D D] show "(\<lambda>x. if x \<in> carrier D then inv a x else \<one>) \<oplus>\<^bsub>R\<^esub> a = \<zero>\<^bsub>R\<^esub>"
    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, \<dots>)"}*}

lemma (in lemma_2_2_14) one_minus_p_hom_diff: shows "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<in> 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<in> hom_completion D D" by simp
next
  show "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> differ = differ \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p"
  proof -
    from ring_R have "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> differ = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<otimes>\<^bsub>R\<^esub> differ" by simp
    also from diff_in_R and p_in_R have "\<dots> = (differ) \<ominus>\<^bsub>R\<^esub> (p \<otimes>\<^bsub>R\<^esub> differ)" by algebra
    also from ring_R and hom_diff_coherent [OF p_in_hom_diff] have "\<dots> = differ \<ominus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> p)" by simp
    also from sym [OF R.r_one [of differ]] have "\<dots> = (differ \<otimes>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>) \<ominus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> p)" by simp
    also from diff_in_R and p_in_R have "\<dots> = differ \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p)" by algebra
    also from ring_R have "\<dots> = differ \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> 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) \<subseteq> C'" 
  shows "h \<in> hom_diff D \<lparr> carrier = C', mult = mult C, one = one C, 
  diff = completion \<lparr>carrier = C', mult = mult C, one = one C, diff = diff C\<rparr> C (diff C)\<rparr>"
proof -
  from diff_group_hom_diff.hom_diff_h [of D C h] and prems have h_hom_diff: "h \<in> hom_diff D C" by simp
  with image_subset and group_hom.hom_one [of C C "differ\<^bsub>C\<^esub>"] and diff_group_hom_diff.group_hom_C_C_differ [of D C h] and prems
  show ?thesis unfolding hom_diff_def hom_completion_def hom_def completion_fun2_def completion_def image_def Pi_def
    unfolding expand_fun_eq by 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 \<in> hom_diff D D"
  shows "(\<lambda>x. if x \<in> kernel D D h then x else \<one>\<^bsub>D\<^esub>) \<in> 
  hom_diff \<lparr>carrier = kernel D D h, mult = mult D, one = one D, 
  diff = completion \<lparr>carrier = kernel D D h, mult = mult D, one = one D, diff = diff D\<rparr> D (diff D)\<rparr> D"
  (is "?inc_KER \<in> hom_diff ?KER _")
proof (unfold hom_diff_def hom_completion_def, auto)
  show "?inc_KER \<in> completion_fun2 ?KER D" unfolding completion_fun2_def by (auto simp add: expand_fun_eq)
next
  show "?inc_KER \<in> hom ?KER D"
  proof (rule homI, auto)
    fix x
    assume "x \<in> kernel D D h" then show "x \<in> carrier D" unfolding kernel_def by simp
  next
    fix x y
    assume x_ker: "x \<in> kernel D D h" and y_ker: "y \<in> kernel D D h" and x_times_y: "x \<otimes> y \<notin> kernel D D h"
    from group_hom.ker_m_closed [of D D h x y] and prems show "\<one> = x \<otimes> y"
      unfolding group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def diff_group_def comm_group_def by simp
  qed
next
  show "?inc_KER \<circ> completion \<lparr>carrier = kernel D D h, mult = mult D, one = one D, diff = diff D\<rparr> D (differ) = differ \<circ> ?inc_KER"
    (is "?inc_KER \<circ> ?compl_diff = differ \<circ> ?inc_KER")
  proof (rule ext)
    fix x
    show "(?inc_KER \<circ> ?compl_diff) x = (differ \<circ> ?inc_KER) x"
    proof (cases "x \<in> 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 \<circ> differ" "differ \<circ> h"] and group_hom.hom_one [of D D differ]
	and prems
      show "(?inc_KER \<circ> ?compl_diff) x = (differ \<circ> ?inc_KER) x"
	unfolding diff_group_def comm_group_def group_hom_def 
	  group_hom_axioms_def kernel_def subset_eq hom_diff_def hom_completion_def by 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 \<circ> ?compl_diff) x = (differ \<circ> ?inc_KER) x"
	unfolding diff_group_def comm_group_def group_hom_def group_hom_axioms_def hom_completion_def by 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) inc_ker_p h"
  (is "reduction D ?KER (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<in> 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 \<in> hom_diff ?KER D" by simp
next
  from h_hom show "h \<in> hom_completion D D" by simp
next
    (*Property a) in the thesis*)
  show "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> ?inc_KER = (\<lambda>x. if x \<in> carrier ?KER then id x else \<one>\<^bsub>?KER\<^esub>)"
    (is "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> ?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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) = (\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> p))" by algebra
    also from ring_R and minus_interpret [OF p_in_R]
    have "\<dots> = (\<lambda>x. if x \<in> carrier D then (\<lambda>x. if x \<in> carrier D then id x else \<one>\<^bsub>D\<^esub>) x 
      \<otimes> (\<lambda>x. if x \<in> carrier D then inv p x else \<one>\<^bsub>D\<^esub>) x else \<one>\<^bsub>D\<^esub>)" by simp
    finally have one_minus_p: "(\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) = (\<lambda>x. if x \<in> carrier D then (\<lambda>x. if x \<in> carrier D then id x else \<one>\<^bsub>D\<^esub>) x 
      \<otimes> (\<lambda>x. if x \<in> carrier D then inv p x else \<one>\<^bsub>D\<^esub>) x else \<one>\<^bsub>D\<^esub>)" by simp
    then show "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> ?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>"
	unfolding group_hom_def group_hom_axioms_def hom_diff_def diff_group_def comm_group_def hom_completion_def by 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 "(\<lambda>x. if x \<in> carrier D then
    (?inc_KER \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x \<otimes> (if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) else \<one>) =
    (\<lambda>x. if x \<in> carrier D then id x else \<one>)"
    (*The expression corresponds to (is "(?inc_KER \<circ> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<otimes> (differ \<circ> h \<otimes> h \<circ> differ))") but i did not find a suitable way to 
    make it shorter*)
  proof -
    from ring_R
    have "(\<lambda>x. if x \<in> carrier D then (?inc_KER \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x \<otimes> (if x \<in> carrier D then (differ \<circ> h) x \<otimes> (h \<circ> differ) x else \<one>) else \<one>) 
      = (?inc_KER \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ))" by (simp add: expand_fun_eq)
    also have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)"
    proof -
      from ring_R have "?inc_KER \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) = ?inc_KER \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p" by simp
      also have "?inc_KER \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p"
      proof (rule ext)
	fix x
	show "(?inc_KER \<circ> \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x"
	proof (cases "x \<in> carrier D") 
	  case True with image_subset [OF p_in_R p_projector] have "(\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) x \<in> 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p)" D] show ?thesis unfolding hom_completion_def by simp
	qed
      qed
      finally have "?inc_KER \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) =  \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p" by simp
      then show "(?inc_KER \<otimes>\<^bsub>R\<^esub> (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)) = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<oplus>\<^bsub>R\<^esub> (differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ)" by simp
    qed
    also from p_def have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<oplus>\<^bsub>R\<^esub> p" by simp
    also from p_in_R have "\<dots> = \<one>\<^bsub>R\<^esub>" by algebra
    also from ring_R have "\<dots> = (\<lambda>x. if x \<in> 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>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one>\<^bsub>?KER\<^esub> else \<one>\<^bsub>?KER\<^esub>)"
    (is "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> h = ?zero_R")
  proof -
      (*Another nice example of application of calculational reasoning with endomorphisms*)
    from ring_R have "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> h = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p) \<otimes>\<^bsub>R\<^esub> h" by simp
    also from h_in_R and p_in_R have "\<dots> = h \<ominus>\<^bsub>R\<^esub> (p \<otimes>\<^bsub>R\<^esub> h)" by algebra
    also from p_def have "\<dots> = h \<ominus>\<^bsub>R\<^esub> ((differ \<otimes>\<^bsub>R\<^esub> h \<oplus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> differ) \<otimes>\<^bsub>R\<^esub> h)" by simp
    also  from diff_in_R and h_in_R and hdh_h and h_nil have "\<dots> = h \<ominus>\<^bsub>R\<^esub> h" by algebra
    also from h_in_R have "\<dots> = \<zero>\<^bsub>R\<^esub>" by algebra
    also from ring_R and diff_group_ker_p_def have "\<dots> = ?zero_R" by simp
    finally show "\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> p \<circ> h = ?zero_R" by simp
  qed
next
  show "h \<circ> ?inc_KER = (\<lambda>x. if x \<in> carrier diff_group_ker_p then \<one> else \<one>)"
    (is "h \<circ> ?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 \<in> 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 \<in> kernel D D p"
    show "h x = \<one>"
    proof -
      from hdh_h and ring_R and expand_fun_eq [of "h \<circ> differ \<circ> 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 "\<dots> = h ((differ) (h x)) \<otimes>\<^bsub>D\<^esub> \<one>" by (unfold kernel_def, simp)
      also from h_nil and ring_R have "\<dots> = h ((differ) (h x)) \<otimes>\<^bsub>D\<^esub> 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 "\<dots> = h ((differ) (h x) \<otimes>\<^bsub>D\<^esub> h ((differ) x))" unfolding kernel_def by simp
      also from p_def and ring_R and x_in_ker have "\<dots> = h (p (x))" unfolding expand_fun_eq kernel_def by simp
      also from x_in_ker have "\<dots> = h \<one>\<^bsub>D\<^esub>" unfolding kernel_def by simp
      also from hom_completion_one [OF _ _ h_hom] and D_diff_group have "\<dots> = \<one>\<^bsub>D\<^esub>" unfolding diff_group_def comm_group_def group_def by simp
      finally show "h x = \<one>" by simp
    qed
  next
      (*This is the meaningless case*)
    fix x assume "x \<notin> kernel D D p"
    from hom_completion_one [OF _ _ h_hom] and D_diff_group show "h \<one>\<^bsub>D\<^esub> = \<one>\<^bsub>D\<^esub>" unfolding diff_group_def comm_group_def group_def by simp
  qed
next
    (*Property e) in the thesis*)
  from h_nil and ring_R show "h \<circ> h = (\<lambda>x. if x \<in> carrier D then \<one> else \<one>)" by simp
qed

end