(*  Title:      inst_locales/HomGroupsCompletion.thy
    ID:         $Id: HomGroupsCompletion.thy $
    Author:     Jesus Aransay
    Comments:   We prove that completion homomorphisms between two commutative groups form a commutative group
                with the given product
*)

theory HomGroupsCompletion 
  imports 
  HomGroupCompletion
  begin

subsection{*Homomorphisms seen as algebraic structures*}

text{*Homomorphisms with the underlying operation are closed*}

lemma hom_mult_completion_is_hom:
  includes comm_group G + comm_group G'
  shows "[|f : hom G G'; g : hom G G' |] ==> (%x. if x \<in>  carrier G then f x \<otimes>\<^sub>2 g x else \<one>\<^sub>2) : hom G G'"
  apply (unfold hom_def, simp add: prems, auto simp add: Pi_def m_closed)
  apply (simp add: m_ac hom_completion_closed)
  done

lemma hom_completion_mult_is_hom_completion:
  includes comm_group G + comm_group G'
  assumes "f \<in> hom_completion G G'" and "g \<in> hom_completion G G'"
  shows "(\<lambda>x. if x \<in> carrier G then f x \<otimes>\<^bsub>G'\<^esub>  g x else \<one>\<^bsub>G'\<^esub>) \<in> hom_completion G G'"
proof (unfold hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show " \<exists>ga. (\<lambda>x. if x \<in> carrier G then f x \<otimes>\<^bsub>G'\<^esub> g x else \<one>\<^bsub>G'\<^esub>) = (\<lambda>x. if x \<in> carrier G then ga x else \<one>\<^bsub>G'\<^esub>)"
    by (rule exI [of _ "(\<lambda>x. f x \<otimes>\<^bsub>G'\<^esub> g x)"])(simp)
next
  from prems show "(\<lambda>x. if x \<in> carrier G then f x \<otimes>\<^bsub>G'\<^esub> g x else \<one>\<^bsub>G'\<^esub>) \<in> hom G G'"
    by (intro hom_mult_completion_is_hom, unfold comm_group_def hom_completion_def)(simp_all)
qed

text{*Proof of the existence of an inverse homomorphism*}

lemma hom_completions_mult_inv_is_hom_completion:
  includes comm_group G + comm_group G'
  assumes "f \<in> hom_completion G G'"
  shows "\<exists>g\<in>hom_completion G G'. (\<lambda>x. if x \<in> carrier G then g x \<otimes>\<^bsub>G'\<^esub> f x else \<one>\<^bsub>G'\<^esub>) = (\<lambda>x. \<one>\<^bsub>G'\<^esub>)"
proof (intro bexI [of _ "(\<lambda>x. if x \<in> carrier G then inv\<^bsub>G'\<^esub> (f x) else \<one>\<^bsub>G'\<^esub>)"])
  show "(\<lambda>g. if g \<in> carrier G then inv\<^bsub>G'\<^esub> f g else \<one>\<^bsub>G'\<^esub>) \<in> hom_completion G G'"
  proof (unfold hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
    show "\<exists>g. (\<lambda>g. if g \<in> carrier G then inv\<^bsub>G'\<^esub> f g else \<one>\<^bsub>G'\<^esub>) = (\<lambda>x. if x \<in> carrier G then g x else \<one>\<^bsub>G'\<^esub>)"
      by (rule exI [of _ "\<lambda>x. inv\<^bsub>G'\<^esub> (f x)"], simp)
  next
    show "(\<lambda>x. if x \<in> carrier G then inv\<^bsub>G'\<^esub> f x else \<one>\<^bsub>G'\<^esub>) \<in> hom G G'"
    proof (unfold hom_def, simp, intro conjI)
      from prems show "(\<lambda>x. if x \<in> carrier G then inv\<^bsub>G'\<^esub> f x else \<one>\<^bsub>G'\<^esub>) \<in> carrier G \<rightarrow> carrier G'"
	by (unfold Pi_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
    next
      show "\<forall>x\<in>carrier G. \<forall>y\<in>carrier G. inv\<^bsub>G'\<^esub> f (x \<otimes> y) = inv\<^bsub>G'\<^esub> f x \<otimes>\<^bsub>G'\<^esub> inv\<^bsub>G'\<^esub> f y"
      proof (intro ballI)
	fix x y
	assume "x \<in> carrier G" and "y \<in> carrier G"
	show "inv\<^bsub>G'\<^esub> f (x \<otimes> y) = inv\<^bsub>G'\<^esub> f x \<otimes>\<^bsub>G'\<^esub> inv\<^bsub>G'\<^esub> f y"
	proof -
	  from prems have "f (x \<otimes> y) = f x \<otimes>\<^bsub>G'\<^esub> f y" by (intro hom_mult, unfold hom_completion_def, simp_all)
	  then have "inv\<^bsub>G'\<^esub> f (x \<otimes> y) = inv\<^bsub>G'\<^esub> (f x \<otimes>\<^bsub>G'\<^esub> f y)" by simp
	  also from prems have "\<dots> = inv\<^bsub>G'\<^esub> (f y) \<otimes>\<^bsub>G'\<^esub> inv\<^bsub>G'\<^esub> (f x)"
	    by (intro inv_mult_group) (unfold hom_completion_def hom_def Pi_def, simp_all)
	  also from prems have "\<dots> = inv\<^bsub>G'\<^esub> (f x) \<otimes>\<^bsub>G'\<^esub> inv\<^bsub>G'\<^esub> (f y)"
	    by (intro m_comm)(unfold hom_completion_def hom_def Pi_def, simp_all)
	  finally show ?thesis by simp
	qed
      qed
    qed
  qed
next
  from prems
  show "(\<lambda>x. if x \<in> carrier G then (if x \<in> carrier G then inv\<^bsub>G'\<^esub> f x else \<one>\<^bsub>G'\<^esub>) \<otimes>\<^bsub>G'\<^esub> f x else \<one>\<^bsub>G'\<^esub>) = (\<lambda>x. \<one>\<^bsub>G'\<^esub>)"
    by (unfold hom_completion_def hom_def Pi_def, auto simp add: expand_fun_eq) 
qed
    
subsection{*Completion homomorphisms between two algebraic structures form a commutative group*}

lemma hom_completion_groups_mult_comm_group:
  includes comm_group G + comm_group G'                                        
  shows "comm_group (| carrier = hom_completion G G', mult = \<lambda>f. \<lambda>g. (\<lambda>x. if x \<in> carrier G then f x \<otimes>\<^sub>2 g x else \<one>\<^sub>2),
  one = (\<lambda>x. if x \<in> carrier G then \<one>\<^sub>2 else \<one>\<^sub>2)|)"
  (is "comm_group ?H_CO")
proof (intro comm_groupI)
  fix f g
  assume "f \<in> carrier ?H_CO" and "g \<in> carrier ?H_CO"
  from prems show "f \<otimes>\<^bsub>?H_CO\<^esub> g \<in> carrier ?H_CO"
    by simp (intro hom_completion_mult_is_hom_completion, unfold comm_group_def, simp_all)
next
  show "\<one>\<^bsub>?H_CO\<^esub> \<in> carrier ?H_CO"
  proof (unfold hom_completion_def completion_fun2_def completion_def, auto)
    show "\<exists>g. (\<lambda>x. \<one>\<^bsub>G'\<^esub>) = (\<lambda>x. if x \<in> carrier G then g x else \<one>\<^bsub>G'\<^esub>)" by (intro exI [of _ "\<lambda>x. \<one>\<^bsub>G'\<^esub>"], simp)
  next
    show "(\<lambda>x. \<one>\<^bsub>G'\<^esub>) \<in> hom G G'" by (unfold hom_def Pi_def, simp)
  qed
next
  fix x y z
  assume "x \<in> carrier ?H_CO" and "y \<in> carrier ?H_CO" and "z \<in> carrier ?H_CO"
  from prems show "x \<otimes>\<^bsub>?H_CO\<^esub> y \<otimes>\<^bsub>?H_CO\<^esub> z = x \<otimes>\<^bsub>?H_CO\<^esub> (y \<otimes>\<^bsub>?H_CO\<^esub> z)"
    by (auto simp add: expand_fun_eq hom_completion_def hom_def Pi_def) (rule m_assoc, simp_all)
next
  fix x y
  assume "x \<in> carrier ?H_CO" and "y \<in> carrier ?H_CO"
  from prems show "x \<otimes>\<^bsub>?H_CO\<^esub> y = y \<otimes>\<^bsub>?H_CO\<^esub> x"
    by (auto simp add: expand_fun_eq hom_completion_def hom_def Pi_def) (rule m_comm, simp_all)
next
  fix x
  assume "x \<in> carrier ?H_CO"
  from prems show "\<one>\<^bsub>?H_CO\<^esub>\<otimes>\<^bsub>?H_CO\<^esub> x = x"
    by (auto simp add: expand_fun_eq hom_completion_def completion_fun2_def completion_def hom_def Pi_def)
next
  fix x
  assume "x \<in> carrier ?H_CO"
  from prems and hom_completions_mult_inv_is_hom_completion [of G G' x] show "\<exists>y\<in>carrier ?H_CO. y \<otimes>\<^bsub>?H_CO\<^esub> x = \<one>\<^bsub>?H_CO\<^esub>"
    by (unfold comm_group_def, simp)
qed

subsection{*Previous facts about homomorphisms of differential structures*}

lemma hom_diff_mult_is_hom_diff:
  includes diff_group D + diff_group D'
  assumes "f \<in> hom_diff D D'" and "g \<in> hom_diff D D'"
  shows "(\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub>  g x else \<one>\<^bsub>D'\<^esub>) \<in> hom_diff D D'"
proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show " \<exists>ga. (\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>) = (\<lambda>x. if x \<in> carrier D then ga x else \<one>\<^bsub>D'\<^esub>)"
    by (rule exI [of _ "(\<lambda>x. f x \<otimes>\<^bsub>D'\<^esub> g x)"])(simp)
next
  from prems show "(\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>) \<in> hom D D'"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def, auto simp add: m_ac)
next
  show "(\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>) \<circ> differ = differ\<^bsub>D'\<^esub> \<circ> (\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>)"
  proof (rule ext)
    fix x
    show "((\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>) \<circ> differ) x = (differ\<^bsub>D'\<^esub> \<circ> (\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^bsub>D'\<^esub> g x else \<one>\<^bsub>D'\<^esub>)) x"
    proof (cases "x \<in> carrier D")
      case True
      from prems show ?thesis
	by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def 
	  completion_fun2_def completion_def hom_def Pi_def) (auto simp add: expand_fun_eq)
    next
      case False
      then show ?thesis
      proof (auto simp add: expand_fun_eq)
	show "f ((differ) x) \<otimes>\<^bsub>D'\<^esub> g ((differ) x) = (differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub>"
	proof -
	  from prems have l_h_s_1: "f ((differ) x) = \<one>\<^bsub>D'\<^esub>"
	    by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def, 
	      auto) (intro group_hom.hom_one, unfold comm_group_def group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
	  moreover from prems have l_h_s_2: "g ((differ) x) = \<one>\<^bsub>D'\<^esub>" 
	    by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def, 
	      auto) (intro group_hom.hom_one, unfold comm_group_def group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
	  moreover from prems have r_h_s: "(differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub> =  \<one>\<^bsub>D'\<^esub>"
	    by (intro group_hom.hom_one)(unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def 
	    hom_diff_def hom_completion_def, simp)
	  ultimately show ?thesis by simp
	qed
      next
	show "\<one>\<^bsub>D'\<^esub> = (differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub>"
	proof (rule sym, intro group_hom.hom_one)
	  from prems show "group_hom D' D' (differ\<^bsub>D'\<^esub>)"
	    by (unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def hom_diff_def 
	      hom_completion_def, simp)
	qed
      qed
    qed
  qed
qed

lemma hom_diff_mult_inv_is_hom_diff:
  includes diff_group D + diff_group D'
  assumes "f \<in> hom_diff D D'"
  shows "\<exists>g\<in>hom_diff D D'. (\<lambda>x. if x \<in> carrier D then g x \<otimes>\<^bsub>D'\<^esub> f x else \<one>\<^bsub>D'\<^esub>) = (\<lambda>x. \<one>\<^bsub>D'\<^esub>)"
proof (intro bexI [of _ "(\<lambda>x. if x \<in> carrier D then inv\<^bsub>D'\<^esub> (f x) else \<one>\<^bsub>D'\<^esub>)"])
  show "(\<lambda>g. if g \<in> carrier D then inv\<^bsub>D'\<^esub> f g else \<one>\<^bsub>D'\<^esub>) \<in> hom_diff D D'"
  proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
    show "\<exists>g. (\<lambda>g. if g \<in> carrier D then inv\<^bsub>D'\<^esub> f g else \<one>\<^bsub>D'\<^esub>) = (\<lambda>x. if x \<in> carrier D then g x else \<one>\<^bsub>D'\<^esub>)"
      by (rule exI [of _ "\<lambda>x. inv\<^bsub>D'\<^esub> (f x)"], simp)
  next
    show "(\<lambda>x. if x \<in> carrier D then inv\<^bsub>D'\<^esub> f x else \<one>\<^bsub>D'\<^esub>) \<in> hom D D'"
    proof (unfold hom_def, simp, intro conjI)
      from prems show "(\<lambda>x. if x \<in> carrier D then inv\<^bsub>D'\<^esub> f x else \<one>\<^bsub>D'\<^esub>) \<in> carrier D \<rightarrow> carrier D'"
	by (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
    next
      show "\<forall>x\<in>carrier D. \<forall>y\<in>carrier D. inv\<^bsub>D'\<^esub> f (x \<otimes> y) = inv\<^bsub>D'\<^esub> f x \<otimes>\<^bsub>D'\<^esub> inv\<^bsub>D'\<^esub> f y"
      proof (intro ballI)
	fix x y
	assume "x \<in> carrier D" and "y \<in> carrier D"
	show "inv\<^bsub>D'\<^esub> f (x \<otimes> y) = inv\<^bsub>D'\<^esub> f x \<otimes>\<^bsub>D'\<^esub> inv\<^bsub>D'\<^esub> f y"
	proof -
	  from prems have "f (x \<otimes> y) = f x \<otimes>\<^bsub>D'\<^esub> f y" by (intro hom_mult, unfold hom_diff_def hom_completion_def, simp_all)
	  then have "inv\<^bsub>D'\<^esub> f (x \<otimes> y) = inv\<^bsub>D'\<^esub> (f x \<otimes>\<^bsub>D'\<^esub> f y)" by simp
	  also from prems have "\<dots> = inv\<^bsub>D'\<^esub> (f y) \<otimes>\<^bsub>D'\<^esub> inv\<^bsub>D'\<^esub> (f x)"
	    by (intro inv_mult_group) (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp_all)
	  also from prems have "\<dots> = inv\<^bsub>D'\<^esub> (f x) \<otimes>\<^bsub>D'\<^esub> inv\<^bsub>D'\<^esub> (f y)"
	    by (intro m_comm)(unfold hom_diff_def hom_completion_def hom_def Pi_def, simp_all)
	  finally show ?thesis by simp
	qed
      qed
    qed
  next
    show "(\<lambda>g. if g \<in> carrier D then inv\<^bsub>D'\<^esub> f g else \<one>\<^bsub>D'\<^esub>) \<circ> differ = differ\<^bsub>D'\<^esub> \<circ> (\<lambda>g. if g \<in> carrier D then inv\<^bsub>D'\<^esub> f g else \<one>\<^bsub>D'\<^esub>)"
    proof (simp add: expand_fun_eq, intro allI impI conjI)
      fix x
      assume "x \<in> carrier D"
      show "inv\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x)"
      proof -
	  (*We prove that f ((differ) x) is the opposite of both inv f ((differ) x) and (differ) (inv f x)*)
	have "(inv\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x)) = (inv\<^bsub>D'\<^esub> f ((differ) x) \<otimes>\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) 
	  \<otimes>\<^bsub>D'\<^esub> f ((differ) x))"
	proof (rule sym, rule r_cancel)
	  from prems show "f ((differ) x) \<in> carrier D'"
	    by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
	next
	  from prems show "inv\<^bsub>D'\<^esub> f ((differ) x) \<in> carrier D'"
	    by (intro inv_closed)(unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
	next
	  from prems show "(differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) \<in> carrier D'"
	    by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
	qed
	also have "(inv\<^bsub>D'\<^esub> f ((differ) x) \<otimes>\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) \<otimes>\<^bsub>D'\<^esub> f ((differ) x))"
	proof -
	  have l_h: "inv\<^bsub>D'\<^esub> f ((differ) x) \<otimes>\<^bsub>D'\<^esub>  f ((differ) x) = \<one>\<^bsub>D'\<^esub>"
	  proof (rule l_inv)
	    from prems show "f ((differ) x) \<in> carrier D'"
	      by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
	  qed
	  moreover have r_h: "(differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) \<otimes>\<^bsub>D'\<^esub> f ((differ) x) = \<one>\<^bsub>D'\<^esub>"
	  proof -
	    have "(differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) \<otimes>\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x) \<otimes>\<^bsub>D'\<^esub> (differ\<^bsub>D'\<^esub>) (f x)"
	    proof -
	      from prems have "f ((differ) x) = (differ\<^bsub>D'\<^esub>) (f x)"
		by (unfold diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp add: expand_fun_eq)
	      then show ?thesis by simp
	    qed
	    also have "\<dots> = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x \<otimes>\<^bsub>D'\<^esub> f x)"
	    proof (rule sym, rule hom_mult)
	      from prems show "differ\<^bsub>D'\<^esub> \<in> hom D' D'"
		by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
	    next
	      from prems show "inv\<^bsub>D'\<^esub> f x \<in> carrier D'"
		by (intro inv_closed, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
	    next
	      from prems show "f x \<in> carrier D'"
		by (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
	    qed
	    also have "\<dots> = (differ\<^bsub>D'\<^esub>) (\<one>\<^bsub>D'\<^esub>)"
	    proof -
	      from prems have "inv\<^bsub>D'\<^esub> f x \<otimes>\<^bsub>D'\<^esub> f x = \<one>\<^bsub>D'\<^esub>"
		by (intro l_inv, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
	      then show ?thesis by simp
	    qed
	    also from prems have "\<dots> = \<one>\<^bsub>D'\<^esub>"
	    proof (intro group_hom.hom_one, unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def, intro conjI, simp_all)
	      from prems show "differ\<^bsub>D'\<^esub> \<in> hom D' D'"
		by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
	    qed
	    finally show ?thesis by simp
	  qed
	  ultimately show ?thesis by simp
	qed
	finally show ?thesis by simp
      qed
    next
	(*The following cases are the non meaningful ones, for instance, when x \<notin> carrier D and so*)
      fix x
      assume "x \<in> carrier D" and "(differ) x \<notin> carrier D"
	(*From these premises a contradiction follows*)
      from prems show "\<one>\<^bsub>D'\<^esub> = (differ\<^bsub>D'\<^esub>) (inv\<^bsub>D'\<^esub> f x)"
	by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
    next
      fix x
      assume "x \<notin> carrier D"
      from prems show "inv\<^bsub>D'\<^esub> f ((differ) x) = (differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub>"
      proof - 
	have l_h: "inv\<^bsub>D'\<^esub> f ((differ) x) = \<one>\<^bsub>D'\<^esub>"
	proof -
	  from prems have "inv\<^bsub>D'\<^esub> f ((differ) x) = inv\<^bsub>D'\<^esub> f (\<one>)"
	    by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def completion_def Pi_def, auto)
	  also have "\<dots> = inv\<^bsub>D'\<^esub> \<one>\<^bsub>D'\<^esub>"
	  proof -
	    from prems have "f \<one> = \<one>\<^bsub>D'\<^esub>"
	      by (intro group_hom.hom_one) (unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
	    then show ?thesis by simp
	  qed
	  also have "\<dots> = \<one>\<^bsub>D'\<^esub>"
	    by (rule inv_one)
	  finally show ?thesis by simp
	qed
	moreover from prems have r_h: "(differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub> = \<one>\<^bsub>D'\<^esub>"
	  by (intro group_hom.hom_one)
	(unfold diff_group_def diff_group_axioms_def comm_group_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
	ultimately show ?thesis by simp
      qed
    next
      show "\<one>\<^bsub>D'\<^esub> = (differ\<^bsub>D'\<^esub>) \<one>\<^bsub>D'\<^esub>"
      proof (rule sym, intro group_hom.hom_one)
	from prems show "group_hom D' D' (differ\<^bsub>D'\<^esub>)"
	  by (unfold diff_group_def comm_group_def diff_group_axioms_def group_hom_def group_hom_axioms_def hom_diff_def hom_completion_def, auto)
      qed
    qed
  qed
next
  from prems show "(\<lambda>x. if x \<in> carrier D then (if x \<in> carrier D then inv\<^bsub>D'\<^esub> f x else \<one>\<^bsub>D'\<^esub>) \<otimes>\<^bsub>D'\<^esub> f x else \<one>\<^bsub>D'\<^esub>) = (\<lambda>x. \<one>\<^bsub>D'\<^esub>)"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def, auto simp add: expand_fun_eq) 
qed

text{*The set of completion differential homomorphisms between two differential groups are a commutative group*}

lemma hom_diff_groups_mult_comm_group:
  includes diff_group D + diff_group D'                                        
  shows "comm_group (| carrier = hom_diff D D', mult = \<lambda>f. \<lambda>g. (\<lambda>x. if x \<in> carrier D then f x \<otimes>\<^sub>2 g x else \<one>\<^sub>2),
  one = (\<lambda>x. if x \<in> carrier D then \<one>\<^sub>2 else \<one>\<^sub>2)|)"
  (is "comm_group ?H_DI")
proof (intro comm_groupI)
  fix f g
  assume "f \<in> carrier ?H_DI" and "g \<in> carrier ?H_DI"
  from prems and hom_diff_mult_is_hom_diff [of D D' f g] show "f \<otimes>\<^bsub>?H_DI\<^esub> g \<in> carrier ?H_DI"
    by (unfold diff_group_def, simp)
next
  show "\<one>\<^bsub>?H_DI\<^esub> \<in> carrier ?H_DI"
  proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, auto)
    show "\<exists>g. (\<lambda>x. \<one>\<^bsub>D'\<^esub>) = (\<lambda>x. if x \<in> carrier D then g x else \<one>\<^bsub>D'\<^esub>)"
      by (intro exI [of _ "\<lambda>x. \<one>\<^bsub>D'\<^esub>"], simp)
  next
    show "(\<lambda>x. \<one>\<^bsub>D'\<^esub>) \<in> hom D D'"
      by (unfold hom_def Pi_def, simp)
  next
    from prems show "(\<lambda>x. \<one>\<^bsub>D'\<^esub>) \<circ> differ = differ\<^bsub>D'\<^esub> \<circ> (\<lambda>x. \<one>\<^bsub>D'\<^esub>)"
      by (auto simp add: expand_fun_eq) (rule sym, intro group_hom.hom_one,
	unfold diff_group_def comm_group_def group_hom_def group_hom_axioms_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
  qed
next
  fix x y z
  assume "x \<in> carrier ?H_DI" and "y \<in> carrier ?H_DI" and "z \<in> carrier ?H_DI"
  from prems show "x \<otimes>\<^bsub>?H_DI\<^esub> y \<otimes>\<^bsub>?H_DI\<^esub> z = x \<otimes>\<^bsub>?H_DI\<^esub> (y \<otimes>\<^bsub>?H_DI\<^esub> z)"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def hom_def Pi_def) (rule m_assoc, simp_all)
next
  fix x y
  assume "x \<in> carrier ?H_DI" and "y \<in> carrier ?H_DI"
  from prems show "x \<otimes>\<^bsub>?H_DI\<^esub> y = y \<otimes>\<^bsub>?H_DI\<^esub> x"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def hom_def Pi_def) (rule m_comm, simp_all)
next
  fix x
  assume "x \<in> carrier ?H_DI"
  from prems show "\<one>\<^bsub> ?H_DI \<^esub>\<otimes>\<^bsub>?H_DI\<^esub> x = x"
    by (auto simp add: expand_fun_eq hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def)
next
  fix x
  assume "x \<in> carrier ?H_DI"
    (*When we omit the G G' in the instantiation, the premises monoid G monoid G' are lost. Why?*)
  from prems and hom_diff_mult_inv_is_hom_diff [of D D' x] show "\<exists>y\<in>carrier ?H_DI. y \<otimes>\<^bsub>?H_DI\<^esub> x = \<one>\<^bsub> ?H_DI \<^esub>"
    by (unfold diff_group_def, simp)
qed

text{*The following result has been already proved in @{thm [locale=diff_group] hom_diff_mult_comm_group};
    now that we have provided a proof of a similar result but for two different differential groups, @{term D} and @{term D'}, 
    it can be trivially proved for the case @{term "D = D'"}*}

lemma (in diff_group) hom_diff_group_mult_comm_group_inst:
  shows "comm_group (| carrier = hom_diff D D, mult = \<lambda>f. \<lambda>g. (\<lambda>x. if x \<in> carrier D then f x \<otimes> g x else \<one>),
  one = (\<lambda>x. if x \<in> carrier D then \<one> else \<one>)|)"
  using prems hom_diff_groups_mult_comm_group [of D D] by simp

end