Theory HomGroupCompletion

(*  Title:      inst_locales/HomGroupCompletion.thy
    ID:         $Id: HomGroupCompletion.thy $
    Author:     Jesus Aransay
    Comments:   Completion homomorphisms form a ring 
*)


header{*Definition of a ring of completion homomorphisms*}

theory HomGroupCompletion 
  imports
  "~~/src/HOL/Algebra/Ring"
begin

section{*Definition of completion functions and some related lemmas*}

  (*Maybe some of the following definitions could be used, if we try to use function types?:

  The following definition is given for the product, that's why we restrict ourselves to 'a, 'a, 'a

  constdefs
  option_binary_map :: "('a => 'a => 'a) => ('a option => 'a option => 'a option)"
  "option_binary_map == %f x y. case x of None => None 
                                                   | Some x' => (case y of None => None 
                                                             | Some y' => Some (f x' y'))"
  
  definition
  "Hom G H == {f. dom f = carrier G & (∀x∈ dom f. ∀y∈dom f. f (the(option_binary_map (mult G) (Some x) (Some y))) =
  option_binary_map (mult H) (f x) (f y) )}"
  
  lemma assumes f: "g ∈ Hom G H" and g: "f ∈ Hom H I" shows "f om g ∈ Hom G I"
  using prems
  apply (unfold Hom_def Hom_def [of G H] Hom_def [of H G] option_binary_map_def map_comp_def, cases)
  apply auto
  
  definition
  "Hom G H == {f. dom f = carrier G & (∀x∈dom f. ∀y∈dom f.
  (the (f((mult G) x y))) =
  (mult H) (the (f x)) (the (f y)))}"
  
  *)

constdefs
  completion :: "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme, ('a => 'b)] => ('a => 'b)"
  "completion G G' f == (%x. if x ∈ carrier G then f x else one G')"

lemma completion_in_funcset: "(!!x. x ∈ carrier G ==> f x ∈ carrier G') ==> (completion G G' f) ∈ carrier G -> carrier G'"
  by (simp add: Pi_def completion_def)

lemma completion_in_hom: includes group_hom G G' h shows "completion G G' h ∈ hom G G'"
  by (unfold completion_def hom_def Pi_def, auto)

lemma completion_apply_carrier [simp]: "x ∈ carrier G ==> completion G G' h x = h x"
  by (simp add: completion_def)

lemma completion_apply_not_carrier [simp]: "x ∉ carrier G ==> completion G G' h x = one G'"
  by (simp add: completion_def)

lemma completion_ext: "(!!x. x ∈ carrier G ==> h x = g x) ==> (completion G G' h) = (completion G G' g)"
  by (simp add: expand_fun_eq Pi_def completion_def)

lemma inj_on_completion_eq: "inj_on (completion G G' h) (carrier G) = inj_on h (carrier G)"
  by (unfold inj_on_def, simp)

constdefs
  completion_fun :: "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a => 'b) set"
  "completion_fun G G' == {f. f = (%x. if x ∈ carrier G then f x else one G')}"

constdefs
  completion_fun2 :: "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a => 'b) set"
  "completion_fun2 G G' == {f. ∃ g. f = completion G G' g}"

lemma f_in_completion_fun2_f_completion: "f ∈ completion_fun2 G G' ==> f = completion G G' f"
  by (unfold completion_fun2_def, unfold completion_def, auto simp add: if_def)

lemma completion_in_completion_fun: "completion G G' h ∈ completion_fun G G'"
  by (unfold completion_fun_def completion_def) (simp add: if_def)

lemma completion_in_completion_fun2: shows "completion G G' h ∈ completion_fun2 G G'"
  by (unfold completion_fun2_def) auto

lemma completion_fun_completion_fun2: "completion_fun G G' = completion_fun2 G G'"
  by (unfold completion_fun_def completion_fun2_def completion_def) (auto simp add: if_def)

lemma completion_id_in_completion_fun: shows "completion G G' id ∈ completion_fun G G'"
  by (unfold completion_fun_def completion_def, auto simp add: expand_fun_eq)

lemma completion_closed2: assumes h: "h ∈ completion_fun2 G G'" and x: "x ∉ carrier G" shows "h x = one G'"
  using prems 
  by (unfold completion_fun2_def completion_def, auto)

subsection {*Homomorphisms defined as completions*}

constdefs
  hom_completion :: "[('a, 'c) monoid_scheme, ('b, 'd) monoid_scheme] => ('a => 'b)set"
  "hom_completion G G' ==  {h. h ∈ completion_fun2 G G' & h ∈ hom G G'}"

lemma hom_completionI: assumes "h ∈ completion_fun2 G G'" and "h ∈ hom G G'" shows "h ∈ hom_completion G G'"
  by (unfold hom_completion_def, simp add: prems)

lemma hom_completion_is_hom: assumes f: "f ∈ hom_completion G G'" shows "f ∈ hom G G'"
  using f by (unfold hom_completion_def, simp)

lemma hom_completion_mult: assumes "h ∈ hom_completion G G'" and "x ∈ carrier G" and "y ∈ carrier G" 
  shows "h (mult G x y) = mult G' (h x) (h y)"
  using prems by (simp add: hom_completion_is_hom hom_mult)

lemma hom_completion_closed: assumes h: "h ∈ hom_completion G G'" and x: "x ∈ carrier G" shows "h x ∈ carrier G'"
  using h and x by (unfold hom_completion_def hom_def Pi_def, simp)

lemma hom_completion_one[simp]: includes group G + group G'
  assumes h: "h ∈ hom_completion G G'" shows "h (one G) = one G'"
  using h and group_hom.hom_one [of G G' h] and prems
  by (unfold hom_completion_def group_hom_def group_hom_axioms_def, simp)

lemma comp_sum: includes group G
  assumes h: "h ∈ hom G G" and h': "h' ∈ hom G G" and x: "x ∈ carrier G" and y: "y ∈ carrier G"
  shows "h' (h (mult G x y)) = mult G (h' (h x))  (h' (h y))"
proof -
  have "h (mult G x y) = mult G (h x) (h y)"
    by (rule hom_mult [of "h" "G" "G" "x" "y"], simp_all add: h x y)
  then have "h' (h (mult G x y)) =  h' (mult G (h x) (h y))" by simp
  also from h h' x y have "… = mult G (h' (h x))  (h' (h y))"
    by (intro hom_mult, unfold hom_def Pi_def, simp_all)
  finally show ?thesis by simp
qed

lemma comp_is_hom: includes group G
  assumes h: "h ∈ hom G G" and h': "h' ∈ hom G G"
  shows "h' o h ∈ hom G G"
  using h h' by (unfold hom_def Pi_def, simp)

text{*Usual composition @{term "op o"} of completion homomorphisms is closed*}

lemma hom_completion_comp: includes group G 
  assumes "f ∈ hom_completion G G" and "g ∈ hom_completion G G" 
  shows "f o g ∈ hom_completion G G"
proof -
  from prems show ?thesis
    apply (unfold hom_completion_def hom_def Pi_def, auto)
    apply (unfold completion_fun2_def completion_def, simp)
    apply (intro exI [of _ "f o g"])
    apply (auto simp add: expand_fun_eq)
    done
qed

subsection{*Completion homomorphisms with usual composition form a monoid*}

text{*The underlying algebraic structures in our development, except otherwise stated, will be commutative groups or differential groups*}

lemma (in comm_group) hom_completion_monoid:
  shows "monoid (| carrier = hom_completion G G, mult = op o, one = (λx. if x ∈ carrier G then id x else \<one>) |)"  
  (is "monoid ?H_CO")
proof (intro monoidI)
  fix x y
  assume x: "x ∈ carrier ?H_CO" and y: "y ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y ∈ carrier ?H_CO"
    by (simp, intro hom_completion_comp)(simp_all add: comm_group_def)
next
  show "\<one>?H_CO ∈ carrier ?H_CO"
    by (unfold hom_completion_def hom_def completion_fun2_def completion_def)(auto simp add: Pi_def)
next
  fix x y z
    (*assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO" and "z ∈ carrier ?H_CO"*)
  show "x ⊗?H_CO y ⊗?H_CO z = x ⊗?H_CO (y ⊗?H_CO z)"
    by (simp) (rule sym, rule o_assoc)
next
  fix x
  assume x: "x ∈ carrier ?H_CO"
  from prems show "\<one>?H_CO ⊗?H_CO x = x"
    by (unfold hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto simp add: expand_fun_eq)
next
  fix x
  assume x: "x ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO \<one>?H_CO = x"
    by (unfold hom_completion_def completion_fun2_def, auto simp add: expand_fun_eq)
  (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def hom_def Pi_def comm_group_def, simp)
qed

text{*Homomorphisms, without the completion condition, are also a monoid with usual composition and the identity*}

lemma (in group) hom_group_monoid:
  shows "monoid (| carrier = hom G G, mult = op o, one = id |)"
  (is "monoid ?HOM")
proof (intro monoidI)
  fix x y
  assume "x ∈ carrier ?HOM" and "y ∈ carrier ?HOM"
  from prems show "x ⊗?HOM y ∈ carrier ?HOM" by (simp add: Pi_def hom_def)
next
  show "\<one>?HOM ∈ carrier ?HOM" by (simp add: hom_def Pi_def)
next
  fix x y z
  assume "x ∈ carrier ?HOM" and "y ∈ carrier ?HOM" and "z ∈ carrier ?HOM"  
  show "x ⊗?HOM y ⊗?HOM z = x ⊗?HOM (y ⊗?HOM z)" using o_assoc [of x y z] by simp
next
  fix x
  assume "x ∈ carrier ?HOM"
  show "\<one>?HOM ⊗?HOM x = x" by simp
next
  fix x
  assume "x ∈ carrier ?HOM"
  show "x ⊗?HOM \<one>?HOM = x" by simp
qed

subsection{*Preliminary facts about addition of homomorphisms*}

lemma homI:
  assumes closed: "!!x. x ∈ carrier G ==> f x ∈ carrier H"
  and mult: "!!x y. [|x ∈ carrier G; y ∈ carrier G|] ==> f (x ⊗G y) = f x ⊗H f y"
  shows "f ∈ hom G H" by (unfold hom_def) (simp add: Pi_def closed mult)

text{*The operation we are going to use as addition for homomorphisms is 
  based on the multiplicative operation of the underlying algebraic structures*}

text{*The three following lemmas show how we can define the addition of homomorphisms in different ways with satisfactory result*}

lemma (in comm_group) hom_mult_is_hom: assumes F: "f ∈ hom G G" and G: "g ∈ hom G G" shows "(λx. f x ⊗ g x) ∈ hom G G"
proof (rule homI)
  fix x
  assume X: "x ∈ carrier G"
  from prems show "f x ⊗ g x ∈ carrier G" by (intro m_closed, simp_all only: hom_closed)
next
  fix x y
  assume X: "x ∈ carrier G" and Y: "y ∈ carrier G"
  from prems have "f (x ⊗ y) ⊗ g (x ⊗ y) = f x ⊗ f y ⊗ (g x ⊗ g y)" by (unfold hom_def, simp add: m_ac)
  with prems show "f (x ⊗ y) ⊗ g (x ⊗ y) = f x ⊗ g x ⊗ (f y ⊗ g y)" by (simp add: m_ac hom_closed)
qed

lemma (in comm_group) hom_mult_is_hom_rest:
  assumes f: "f ∈ hom G G" and g: "g ∈ hom G G"
  shows "(λx∈carrier G. f x ⊗ g x) ∈ hom G G" (is "?fg ∈ _")
proof (rule homI)
  fix x assume "x ∈ carrier G"
  with f g show "?fg x ∈ carrier G" by (simp add: hom_closed)
next
  fix x y assume "x ∈ carrier G" "y ∈ carrier G"
  with f g show "?fg (x ⊗ y) = ?fg x ⊗ ?fg y" by (simp add: hom_closed hom_mult m_ac)
qed

lemma (in comm_group) hom_mult_is_hom_completion:
  assumes f: "f ∈ hom G G" and g: "g ∈ hom G G" 
  shows "(λx. if x ∈ carrier G then f x ⊗ g x else \<one>) ∈ hom G G"
  (is "?fg ∈ _")
  apply (rule homI)
  using f g apply (simp add: hom_closed)
  using f g apply (simp add: hom_mult m_ac hom_closed)
  done

text{*The inverse for the addition of homomorphisms will be given by the @{term [locale=comm_group] "(λx. inv f x)"} operation*}

lemma (in comm_group) hom_inv_is_hom: assumes f: "f ∈ hom G G" shows "(λx. inv f x) ∈ hom G G"
proof (unfold hom_def, simp, intro conjI)
  from f show "(λx. inv f x) ∈ carrier G -> carrier G" by (unfold Pi_def hom_def, auto)
next
  show "∀x∈carrier G. ∀y∈carrier G. inv f (x ⊗ y) = inv f x ⊗ inv f y"
  proof (intro ballI)
    fix x y assume x: "x ∈ carrier G" and y: "y ∈ carrier G"
    from prems show "inv f (x ⊗ y) = inv f x ⊗ inv f y"
    proof -
      from prems have "f (x ⊗ y) = f x ⊗ f y" by (intro hom_mult, simp_all)
      then have "inv f (x ⊗ y) = inv (f x ⊗ f y)" by simp
      also from prems have "… = inv (f y) ⊗ inv (f x)"
        by (intro inv_mult_group) (simp_all add: hom_closed)
      also from prems have "… = inv (f x) ⊗ inv (f y)"
        by (intro m_comm) (simp_all add: inv_closed hom_closed)
      finally show ?thesis by simp
    qed
  qed
qed

text{*Lemma @{thm [locale=comm_group] hom_inv_is_hom} proves that the multiplicative inverse of the underlying structure 
  preserves the homomorphism definition*}

locale group_end = group_hom G G h

text{*Due to the partial definitions of domains, it would not be possible to prove that 
  @{term [locale=group_end] "h o (λx. inv h x) = (λx. \<one>)"}; 
  the closer fact that can be proven is @{term [locale=group_end] "h o (λx. inv h x) = (λx∈carrier G. \<one>)"}; *}

lemma (in comm_group) hom_completion_inv_is_hom_completion:
  assumes "f ∈ hom_completion G G"
  shows "(λx. if x ∈ carrier G then inv f x else \<one>) ∈ hom_completion G G"
proof (unfold hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show "∃g. (λg. if g ∈ carrier G then inv f g else \<one>) = (λx. if x ∈ carrier G then g x else \<one>)"
    by (rule exI [of _ "λx. inv (f x)"], simp)
next
  show "(λx. if x ∈ carrier G then inv f x else \<one>) ∈ hom G G"
  proof (unfold hom_def, simp, intro conjI)
    from prems show "(λx. if x ∈ carrier G then inv f x else \<one>) ∈ carrier G -> carrier G"
      by (unfold Pi_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
  next
    show "∀x∈carrier G. ∀y∈carrier G. inv f (x ⊗ y) = inv f x ⊗ inv f y"
    proof (intro ballI)
      fix x y
      assume "x ∈ carrier G" and "y ∈ carrier G"
      show "inv f (x ⊗ y) = inv f x ⊗ inv f y"
      proof -
        from prems have "f (x ⊗ y) = f x ⊗ f y" by (intro hom_mult, unfold hom_completion_def, simp_all)
        then have "inv f (x ⊗ y) = inv (f x ⊗ f y)" by simp
        also from prems have "… = inv (f y) ⊗ inv (f x)"
          by (intro inv_mult_group) (unfold hom_completion_def hom_def Pi_def, simp_all)
        also from prems have "… = inv (f x) ⊗ inv (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

lemma (in comm_group) hom_completion_mult_inv_is_hom_completion:
  assumes "f ∈ hom_completion G G"
  shows "∃g∈hom_completion G G. (λx. if x ∈ carrier G then g x ⊗ f x else \<one>) = (λx. \<one>)"
proof (intro bexI [of _ "(λx. if x ∈ carrier G then inv (f x) else \<one>)"])
  from prems show "(λg. if g ∈ carrier G then inv f g else \<one>) ∈ hom_completion G G"
    by (intro hom_completion_inv_is_hom_completion)
next
  from prems show "(λx. if x ∈ carrier G then (if x ∈ carrier G then inv f x else \<one>) ⊗ f x else \<one>) = (λx. \<one>)"
    by (unfold hom_completion_def hom_def Pi_def, auto simp add: expand_fun_eq)
qed

subsection{*Completion homomorphisms are a commutative group with the underlying operation*}

lemma (in comm_group) hom_completion_mult_comm_group:
  shows "comm_group (|carrier = hom_completion G G, mult = λf. λg. (λx. if x ∈ carrier G then f x ⊗ g x else \<one>),
  one = (λx. if x ∈ carrier G then \<one> else \<one>)|)"
  (is "comm_group ?H_CO")
proof (intro comm_groupI)
  fix x y 
  assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y ∈ carrier ?H_CO"
    by (unfold hom_completion_def completion_fun2_def completion_def, auto simp add: hom_mult_is_hom_completion)
next
  show "\<one>?H_CO ∈ carrier ?H_CO"
    by (unfold hom_completion_def completion_fun2_def completion_def hom_def Pi_def expand_fun_eq, auto)
next
  fix x y z
  assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO" and "z ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y ⊗?H_CO z = x ⊗?H_CO (y ⊗?H_CO z)"
    by (unfold hom_completion_def completion_fun2_def completion_def expand_fun_eq, auto simp add: hom_def Pi_def m_assoc)
next
  fix x y
  assume "x ∈ carrier ?H_CO" and "y ∈ carrier ?H_CO"
  from prems show "x ⊗?H_CO y = y ⊗?H_CO x"
    by (unfold comm_monoid_axioms_def expand_fun_eq hom_completion_def hom_def Pi_def, simp add: m_comm)
next
  fix x
  assume "x ∈ carrier ?H_CO"
  from prems show "\<one>?H_CO ⊗?H_CO x = x"
    by (unfold hom_completion_def completion_fun2_def completion_def expand_fun_eq group_axioms_def hom_def Pi_def, auto)
next
  fix x
  assume "x ∈ carrier ?H_CO"
    (*When we omit the G G' in the instantiation, the premises monoid G monoid G' are lost. Why?*)
  from prems and hom_completion_mult_inv_is_hom_completion [of x] show "∃y∈carrier ?H_CO. y ⊗?H_CO x = \<one> ?H_CO "
    by simp
qed

(*The only difference of the following lemma with the previous one is that here (λx. if x ∈ carrier G then \<one> else \<one>) 
    appears like (λx. \<one>); we will need this statement later*)

lemma (in comm_group) hom_completion_mult_comm_group2:
  shows "comm_group (| carrier = hom_completion G G, mult = λf. λg. (λx. if x ∈ carrier G then f x ⊗ g x else \<one>), one = (λx. \<one>)|)"
proof -
  from prems have "comm_group (|carrier = hom_completion G G, mult = λf g x. if x ∈ carrier G then f x ⊗ g x else \<one>, 
    one = λx. if x ∈ carrier G then \<one> else \<one>|))," by (intro hom_completion_mult_comm_group)
  then show ?thesis by simp
qed

lemma (in comm_group) hom_completion_mult_comm_monoid:
  includes comm_group G
  shows "comm_monoid (| carrier = hom_completion G G, mult = λf. λg. (λx. if x ∈ carrier G then f x ⊗ g x else \<one>), one = (λx. \<one>)|)"
proof -
  from prems have "comm_group (|carrier = hom_completion G G, mult = λf g x. if x ∈ carrier G then f x ⊗ g x else \<one>, 
    one = λx. if x ∈ carrier G then \<one> else \<one>|))," by (intro hom_completion_mult_comm_group)
  then have "comm_group (|carrier = hom_completion G G, mult = λf g x. if x ∈ carrier G then f x ⊗ g x else \<one>, 
    one = λx. \<one>|))," by simp
  then show ?thesis by (unfold comm_group_def comm_monoid_def, simp)
qed

subsection{*Endomorphisms with suitable operations form a ring*}

text{*The distributive law is proved first*}

lemma (in comm_group) r_mult_dist_add: assumes"f ∈ hom_completion G G" and "g ∈ hom_completion G G" and "h ∈ hom_completion G G" 
  shows "(λx. if x ∈ carrier G then f x ⊗ g x else \<one>) o h = (λx. if x ∈ carrier G then (f o h) x ⊗ (g o h) x else \<one>)"
proof (simp add: expand_fun_eq, intro allI impI conjI)
  fix x
  assume "x ∈ carrier G" and "h x ∉ carrier G"
  from prems show "\<one> = f (h x) ⊗ g (h x)"
    by (unfold hom_completion_def completion_fun2_def completion_def, auto)
next
  fix x
  assume "x ∉ carrier G" and "h x ∈ carrier G"
  show "f (h x) ⊗ g (h x) = \<one>"
  proof -
    from prems have "f (h x) = \<one>" and "g (h x) = \<one>"
      apply (unfold hom_completion_def completion_fun2_def completion_def, auto)
      apply (intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def comm_group_def hom_completion_def hom_def Pi_def, auto)+
      done
    then show ?thesis by simp
  qed
qed

lemma (in comm_group) l_mult_dist_add: assumes"f ∈ hom_completion G G" and "g ∈ hom_completion G G" and "h ∈ hom_completion G G" 
  shows "h o (λx. if x ∈ carrier G then f x ⊗ g x else \<one>) = (λx. if x ∈ carrier G then (h o f) x ⊗ (h o g) x else \<one>)"
proof -
  from prems show ?thesis
    apply (simp add: expand_fun_eq, intro allI impI conjI)
    apply (intro hom_mult, unfold hom_completion_def hom_def Pi_def, auto)
    apply (intro group_hom.hom_one)
    apply (unfold comm_group_def group_hom_def group_hom_axioms_def hom_def Pi_def, simp)
    done
qed

text{*Endomorphisms with the previous operations form a ring*}

lemma (in comm_group) hom_completion_ring: 
  shows "ring (| carrier = hom_completion G G, mult = op o, one = (λx. if x ∈ carrier G then id x else \<one>),
  zero = (λx. if x ∈ carrier G then \<one> else \<one>), add = λf. λg. (λx. if x ∈ carrier G then f x ⊗ g x else \<one>)|)"
proof (rule ringI, unfold abelian_group_def abelian_monoid_def abelian_group_axioms_def, 
    simp_all add: hom_completion_mult_comm_monoid hom_completion_mult_comm_group)
  show "monoid (| carrier = hom_completion G G, mult = op o, one = λx. if x ∈ carrier G then id x else \<one>, zero = λx. \<one>,
    add = λf g x. if x ∈ carrier G then f x ⊗ g x else \<one> |)"
  proof -
    from comm_group.hom_completion_monoid and prems 
    have "monoid (|carrier = hom_completion G G, mult = op o, one = λx. if x ∈ carrier G then id x else \<one>|)),"
      by (unfold comm_group_def, auto)
    then show ?thesis by (unfold monoid_def, simp)
  qed
next
  show "comm_group (|carrier = hom_completion G G, mult = λf g x. if x ∈ carrier G then f x ⊗ g x else \<one>, one = λx. \<one>|)),"
    by (intro hom_completion_mult_comm_group2)
next
  show "!!x y z. [|x ∈ hom_completion G G; y ∈ hom_completion G G; z ∈ hom_completion G G|]
    ==> (λxa. if xa ∈ carrier G then x xa ⊗ y xa else \<one>) o z = (λxa. if xa ∈ carrier G then (x o z) xa ⊗ (y o z) xa else \<one>)"
    by (erule r_mult_dist_add) (assumption+)
next
  show "!!x y z. [| x ∈ hom_completion G G; y ∈ hom_completion G G; z ∈ hom_completion G G |]
    ==> z o (λxa. if xa ∈ carrier G then x xa ⊗ y xa else \<one>) = (λxa. if xa ∈ carrier G then (z o x) xa ⊗ (z o y) xa else \<one>)"
    by (erule l_mult_dist_add)(assumption+)
qed

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

text{*Some examples where it is shown the usefulness of the previous proofs*}

lemma (in hom_completion_ring) r_dist_minus:
  "[|f ∈ carrier R; g ∈ carrier R; h ∈ carrier R|] 
  ==> (f \<ominus>2 g) ⊗2 h  = (f ⊗2 h) \<ominus>2 (g ⊗2 h)" by algebra

lemma (in hom_completion_ring) sublemma:
  "[| f ∈ carrier R; h ∈ carrier R; f ⊗2 h = h |] ==> (\<one>2 \<ominus>2 f) ⊗2 h = \<zero>2" by algebra

subsection{*Definition of differential group*}
text{*According to Section 2.3 in Aransay's memoir, in the following we will be dealing with ungraded algebraic structures.*}
text{*The Basic Perturbation Lemma is usually stated in terms of differential structures; 
  these include diferential groups as well as chain complexes.*}
text{*Moreover, chain complexes can be defined in terms of differential groups (more concretely, 
  as indexed collections of differential groups).*}
text{*The proof of the Basic Perturbation Lemma does not include any reference to graded structures or proof obligations
  derived from the degree information.*}
text{*Thus, we preferred to state and prove the Basic Perturbation Lemma in terms of ungrades structures (differential and abelian groups),
  for the sake of simplicity, and avoid implementing and dealing with graded structures (chain complexes and graded groups).*}

record 'a diff_group = "'a monoid" +
  diff :: "'a => 'a" ("differ\<index>" 81)

locale diff_group = comm_group D +
  assumes diff_hom : "differ ∈ hom_completion D D"
  and  diff_nilpot : "differ o differ = (λx. \<one>)"

lemma diff_groupI:
  includes struct D
  assumes m_closed:
  "!!x y. [| x ∈ carrier D; y ∈ carrier D |] ==> x ⊗ y ∈ carrier D"
  and one_closed: "\<one> ∈ carrier D"
  and m_assoc:
  "!!x y z. [| x ∈ carrier D; y ∈ carrier D; z ∈ carrier D |] ==> (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
  and m_comm:
  "!!x y. [| x ∈ carrier D; y ∈ carrier D |] ==> x ⊗ y = y ⊗ x"
  and l_one: "!!x. x ∈ carrier D ==> \<one> ⊗ x = x"
  and l_inv_ex: "!!x. x ∈ carrier D ==> ∃y ∈ carrier D. y ⊗ x = \<one>"
  and diff_hom: "differ ∈ hom_completion D D"
  and diff_nilpot: "!!x. (differ) ((differ) x) = \<one>"
  shows "diff_group D"
  using prems by (unfold diff_group_def diff_group_axioms_def comm_group_def group_def group_axioms_def comm_monoid_def 
    comm_monoid_axioms_def Units_def monoid_def, auto simp add: expand_fun_eq)


subsection{*Definition of homomorphisms between differential groups*}

locale hom_completion_diff = diff_group C + diff_group D + var f +
  assumes f_hom_completion: "f ∈ hom_completion C D"
  and f_coherent: "f o differ1 = differ2 o f"

constdefs (structure C and D)
  hom_diff :: "_ => _  => ('a => 'b) set"
  "hom_diff C D == {f. f ∈ hom_completion C D & (f o (differC) = (differD) o f)}"

lemma hom_diff_is_hom_completion: assumes h: "h ∈ hom_diff C D"
  shows "h ∈ hom_completion C D"
  using h by (unfold hom_diff_def, simp)

lemma hom_diff_closed: assumes h: "h ∈ hom_diff C D" and x: "x ∈ carrier C" shows "h x ∈ carrier D"
  using h and x by (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)

lemma hom_diff_mult: assumes h: "h ∈ hom_diff C D" and x: "x ∈ carrier C" and y: "y ∈ carrier C" shows "h (x ⊗C y) = h (x) ⊗D h (y)"
  using hom_completion_mult [of h C D x y] and h and x and y by (unfold hom_diff_def, simp)

lemma hom_diff_coherent: assumes h: "h ∈ hom_diff C D" shows "h o differC = differD o h"
  using h by (unfold hom_diff_def, simp)

lemma (in diff_group) hom_diff_comp_closed: assumes "f ∈ hom_diff D D" and "g ∈ hom_diff D D" shows "g o f ∈ hom_diff D D"
proof -
  from prems show "g o f ∈ hom_diff D D"
  proof (unfold hom_diff_def, auto)
    from prems show "g o f ∈ hom_completion D D" 
      by (intro hom_completion_comp, unfold comm_group_def group_def group_axioms_def hom_diff_def, simp_all)
    from prems show " g o f o differ = differ o (g o f)"
    proof -
      have "g o f o differ = g o (f o differ)" 
        by (rule sym, rule o_assoc)
      also from prems have "… = g o (differ o f)"
        by (unfold hom_diff_def, auto)
      also have "… = (g o differ) o f"
        by (rule o_assoc)
      also from prems have "… = (differ o g) o f"
        by (unfold hom_diff_def, auto)
      also have "… = differ o (g o f)"
        by (rule sym, rule o_assoc)
      finally show ?thesis by simp
    qed
  qed
qed

lemma (in diff_group) hom_diff_monoid:
  shows "monoid (|carrier = hom_diff D D, mult = op o, one = (λx. if x ∈ carrier D then id x else \<one>)|)"
  (is "monoid ?DIFF")
proof (intro monoidI)
  fix x y
  assume "x ∈ carrier ?DIFF" "y ∈ carrier ?DIFF"
  then show "x ⊗?DIFF y ∈ carrier ?DIFF" by simp (rule hom_diff_comp_closed)
next
  show "\<one>?DIFF ∈ carrier ?DIFF"
  proof (simp, unfold hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def diff_group_def, auto)
    from prems show "(λx. if x ∈ carrier D then id x else \<one>) o differ = differ o (λx. if x ∈ carrier D then id x else \<one>)"
      apply (unfold diff_group_def diff_group_axioms_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def)
      apply (auto simp add: expand_fun_eq)
      apply (rule sym, intro group_hom.hom_one, unfold group_hom_def group_hom_axioms_def comm_group_def hom_def Pi_def, simp)
      done
  qed
next
  fix x y z
  assume "x ∈ carrier ?DIFF" and "y ∈ carrier ?DIFF" and "z ∈ carrier ?DIFF"
  show "x ⊗?DIFF y ⊗?DIFF z = x ⊗?DIFF (y ⊗?DIFF z)" by (simp add: o_assoc)
next
  fix x
  assume "x ∈ carrier ?DIFF" from prems show "\<one>?DIFF ⊗?DIFF x = x"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def completion_fun2_def completion_def, auto simp add: expand_fun_eq)
next
  fix x
  assume "x ∈ carrier ?DIFF"
  from prems show "x ⊗?DIFF \<one>?DIFF = x"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def completion_fun2_def completion_def,auto simp add: expand_fun_eq)
  (rule group_hom.hom_one, unfold group_hom_def group_hom_axioms_def diff_group_def comm_group_def hom_def Pi_def, simp)
qed

subsection{*Completion homomorphisms between differential structures form a commutative group with the underlying operation*}

lemma (in diff_group) hom_diff_mult_closed: assumes "f ∈ hom_diff D D" and "g ∈ hom_diff D D" 
  shows "(λx. if x ∈ carrier D then f x ⊗ g x else \<one>) ∈ hom_diff D D"
proof (unfold hom_diff_def hom_completion_def completion_fun2_def completion_def, simp, intro conjI)
  show "∃ga. (λx. if x ∈ carrier D then f x ⊗ g x else \<one>) = (λx. if x ∈ carrier D then ga x else \<one>)"
    by (rule exI [of _ "λx. f x ⊗ g x"], simp)
next
  from prems show "(λx. if x ∈ carrier D then f x ⊗ g x else \<one>) ∈ hom D D"
    by (unfold hom_diff_def hom_completion_def hom_def Pi_def, auto simp add: m_ac) 
next
  show "(λx. if x ∈ carrier D then f x ⊗ g x else \<one>) o differ = differ o (λx. if x ∈ carrier D then f x ⊗ g x else \<one>)"
  proof (rule ext)
    fix x
    show "((λx. if x ∈ carrier D then f x ⊗ g x else \<one>) o differ) x = (differ o (λx. if x ∈ carrier D then f x ⊗ g x else \<one>)) x"
    proof (cases "x ∈ carrier D")
      case True
      from prems show ?thesis
        by (unfold diff_group_axioms_def hom_diff_def hom_completion_def completion_fun2_def diff_group_def completion_def hom_def Pi_def)
      (auto simp add: expand_fun_eq)
    next
      case False
      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)
    qed
  qed
qed

lemma (in diff_group) hom_diff_inv_def: assumes "f ∈ hom_diff D D" 
  shows "(λx. if x ∈ carrier D then inv f x else \<one>) ∈ hom_diff D D"
proof (unfold hom_diff_def, auto)
  from prems show "(λx. if x ∈ carrier D then inv f x else \<one>) ∈ hom_completion D D"
    by (intro hom_completion_inv_is_hom_completion, unfold hom_diff_def, simp)
next
  from prems show "(λx. if x ∈ carrier D then inv f x else \<one>) o differ = differ o (λx. if x ∈ carrier D then inv f x else \<one>)"
  proof (simp add: expand_fun_eq, intro allI impI conjI)
    fix x
    assume "x ∈ carrier D"
    show "inv f ((differ) x) = (differ) (inv 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 f ((differ) x) = (differ) (inv f x)) = (inv f ((differ) x) ⊗ f ((differ) x) = (differ) (inv f x) ⊗ f ((differ) x))"
      proof (rule sym, rule r_cancel)
        from prems show "f ((differ) x) ∈ 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 f ((differ) x) ∈ 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) (inv f x) ∈ 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 f ((differ) x) ⊗ f ((differ) x) = (differ) (inv f x) ⊗ f ((differ) x)"
      proof -
        have l_h: "inv f ((differ) x) ⊗ f ((differ) x) = \<one>"
        proof (rule l_inv)
          from prems show "f ((differ) x) ∈ carrier D"
            by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def hom_def Pi_def, simp)
        qed
        have r_h: "(differ) (inv f x) ⊗ f ((differ) x) = \<one>"
        proof -
          have "(differ) (inv f x) ⊗ f ((differ) x) = (differ) (inv f x) ⊗ (differ) (f x)"
          proof -
            from prems have "f ((differ) x) = (differ) (f x)"
              by (unfold diff_group_def 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 "… = (differ) (inv f x ⊗ f x)"
          proof (rule sym, rule hom_mult)
            from prems show "differ ∈ hom D D"
              by (unfold diff_group_def diff_group_axioms_def hom_diff_def hom_completion_def, simp)
          next
            from prems show "inv f x ∈ carrier D"
              by (intro inv_closed, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
          next
            from prems show "f x ∈ carrier D"
              by (unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
          qed
          also have "… = (differ) (\<one>)"
          proof -
            from prems have "inv f x ⊗ f x = \<one>"
              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 "… =  \<one>"
          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 ∈ 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
        from l_h and r_h show ?thesis by simp
      qed
      finally show ?thesis by simp
    qed
  next
      (*The following cases are the non meaningful ones; for instance, when x ∉ carrier D*)
    fix x
    assume "x ∈ carrier D" and "(differ) x ∉ carrier D"
      (*From these premises a contradiction follows*)
    from prems show "\<one> = (differ) (inv 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 ∉ carrier D"
    from prems show "inv f ((differ) x) = (differ) \<one>"
    proof - 
      have l_h: "inv f ((differ) x) = \<one>" thm inv_one
      proof -
        from prems have "inv f ((differ) x) = inv 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 "… = inv \<one>"
        proof -
          from prems have "f \<one> = \<one>"
            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 "… = \<one>"
          by (rule inv_one)
        finally show ?thesis by simp
      qed
      from prems have r_h: "(differ) \<one> = \<one>"
        by (intro group_hom.hom_one)
      (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)
      from r_h and l_h show ?thesis by simp
    qed
  next
    show "\<one> = (differ) \<one>"
    proof (rule sym, intro group_hom.hom_one)
      from prems show "group_hom D D (differ)"
        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

lemma (in diff_group) hom_diff_inv: assumes "f ∈ hom_diff D D" 
  shows "∃g∈hom_diff D D. (λx. if x ∈ carrier D then g x ⊗ f x else \<one>) = (λx. \<one>)"
proof (rule bexI [of _ "(λx. if x ∈ carrier D then inv f x else \<one>)"])
  from prems  show "(λx. if x ∈ carrier D then (if x ∈ carrier D then inv f x else \<one>) ⊗ f x else \<one>) = (λx. \<one>)"
    by (auto simp add: expand_fun_eq) (rule l_inv, unfold hom_diff_def hom_completion_def hom_def Pi_def, simp)
next
  show "(λx. if x ∈ carrier D then inv f x else \<one>) ∈ hom_diff D D" by (rule hom_diff_inv_def, simp add: prems)
qed

subsection{*Differential homomorphisms form a commutative group with the underlying operation*}

lemma (in diff_group) hom_diff_mult_comm_group:
  shows "comm_group (|carrier = hom_diff D D, mult = λf. λg. (λx. if x ∈ carrier D then f x ⊗ g x else \<one>),
  one = (λx. if x ∈ carrier D then \<one> else \<one>)|)"
  (is "comm_group ?DIFF")
proof (intro comm_groupI)
  fix x y
  assume "x ∈ carrier ?DIFF" and "y ∈ carrier ?DIFF"
  then show "x ⊗?DIFF y ∈ carrier ?DIFF" by simp (erule hom_diff_mult_closed, assumption)
next
  from prems show "\<one>?DIFF ∈ carrier ?DIFF"
  proof (simp, unfold hom_diff_def hom_completion_def hom_def Pi_def completion_fun2_def, auto)
    show "∃g. (λx. \<one>) = completion D D g" by (rule exI [of _ "λx. \<one>"], unfold completion_def, simp)
  next
    from prems show "(λx. \<one>) o differ = differ o (λx. \<one>)"
    proof (auto simp add: expand_fun_eq)
      show "\<one> = (differ) \<one>"
      proof (rule sym, intro group_hom.hom_one)
        from prems show "group_hom D D (differ)" 
          by (unfold group_hom_def group_hom_axioms_def diff_group_def comm_group_def diff_group_axioms_def hom_diff_def 
            hom_completion_def, simp)
      qed
    qed
  qed
next
  fix x y z
  assume "x ∈ carrier ?DIFF" and "y ∈ carrier ?DIFF" and "z ∈ carrier ?DIFF"
  from prems show "x ⊗?DIFF y ⊗?DIFF z = x ⊗?DIFF (y ⊗?DIFF z)"
    by (auto simp add: expand_fun_eq) (intro m_assoc, unfold hom_diff_def hom_completion_def, auto simp add: hom_closed)
next
  fix x y
  assume "x ∈ carrier ?DIFF" and "y ∈ carrier ?DIFF"
  from prems show "x ⊗?DIFF y = y ⊗?DIFF x"
    by (auto simp add: expand_fun_eq) (intro m_comm, unfold hom_diff_def hom_completion_def hom_def Pi_def, auto)
next
  fix x
  assume "x ∈ carrier ?DIFF"
  from prems show "\<one>?DIFF ⊗?DIFF x = x "
    by (auto simp add: expand_fun_eq)
  (intro l_one, unfold hom_diff_def hom_completion_def completion_fun2_def completion_def hom_def Pi_def, auto)
next
  fix x
  assume "x ∈ carrier ?DIFF"
    (*When we omit the G G' in the instantiation, the premises monoid G monoid G' are lost. Why?*)
  from prems and hom_diff_inv [of x] show "∃y∈carrier ?DIFF. y ⊗?DIFF x = \<one> ?DIFF " by simp
qed

text{*The completion homomorphisms between differential groups are a ring with suitable operations*}

lemma (in diff_group) hom_diff_ring: 
  shows "ring (| carrier = hom_diff 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>)|)"
  (is "ring ?DIFF")
proof (rule ringI, unfold abelian_group_def abelian_group_axioms_def abelian_monoid_def, auto)
  show "monoid (| carrier = hom_diff D D, mult = op o, one = λx. if x ∈ carrier D then id x else \<one>, zero = λx. \<one>,
    add = λf g x. if x ∈ carrier D then f x ⊗ g x else \<one> |)"
  proof -
    from diff_group.hom_diff_monoid and prems have "monoid (|carrier = hom_diff D D, mult = op o, 
      one = λx. if x ∈ carrier D then id x else \<one>|)),"
      by (unfold diff_group_def, auto)
    then show ?thesis by (unfold monoid_def, simp)
  qed
next
  show "comm_monoid (|carrier = hom_diff D D, mult = λf g x. if x ∈ carrier D then f x ⊗ g x else \<one>, one = λx. \<one>|)),"
  proof -
    from diff_group.hom_diff_mult_comm_group and prems
    have "comm_group (|carrier = hom_diff D D, mult = λf g x. if x ∈ carrier D then f x ⊗ g x else \<one>, 
      one = λx. if x ∈ carrier D then \<one> else \<one>|)),"
      by (unfold diff_group_def, auto)
    then show ?thesis by (unfold comm_group_def comm_monoid_def, simp)
  qed
next
  show "comm_group (|carrier = hom_diff D D, mult = λf g x. if x ∈ carrier D then f x ⊗ g x else \<one>, one = λx. \<one>|)),"
  proof -
    from diff_group.hom_diff_mult_comm_group and prems
    have "comm_group (|carrier = hom_diff D D, mult = λf g x. if x ∈ carrier D then f x ⊗ g x else \<one>, 
      one = λx. if x ∈ carrier D then \<one> else \<one>|)),"
      by (unfold diff_group_def, auto)
    then show ?thesis by simp
  qed
next
  show "!!x y z. [|x ∈ hom_diff D D; y ∈ hom_diff D D; z ∈ hom_diff D D|]
    ==> (λxa. if xa ∈ carrier D then x xa ⊗ y xa else \<one>) o z = (λxa. if xa ∈ carrier D then (x o z) xa ⊗ (y o z) xa else \<one>)"
  proof -
    fix x y z
    assume "x ∈ hom_diff D D" and "y ∈ hom_diff D D" and "z ∈ hom_diff D D"
    from prems
    show "(λxa. if xa ∈ carrier D then x xa ⊗ y xa else \<one>) o z = (λxa. if xa ∈ carrier D then (x o z) xa ⊗ (y o z) xa else \<one>)"
      by (intro r_mult_dist_add) (unfold hom_diff_def, simp_all)
  qed
next
  show "!!x y z. [| x ∈ hom_diff D D; y ∈ hom_diff D D; z ∈ hom_diff D D|]
    ==> z o (λxa. if xa ∈ carrier D then x xa ⊗ y xa else \<one>) = (λxa. if xa ∈ carrier D then (z o x) xa ⊗ (z o y) xa else \<one>)"
    by (intro l_mult_dist_add) (unfold hom_diff_def, simp_all)
qed (simp_all add: hom_diff_def)

end