(*  Title:      bpl/analytic_part_local.thy
    ID:         $Id: analytic_part_local.thy $
    Author:     Jesus Aransay
    Comments:
*)

header{*Definition of local nilpotency and Lemmas 2.2.1 to 2.2.6 in Aransay's memoir*}

theory analytic_part_local 
  imports 
  lemma_2_2_14 
  "~~/src/HOL/Library/Infinite_Set"
  begin

subsection{*Definition of local nilpotent element and the bound function*}

locale local_nilpotent_term = ring_endomorphisms D R + var a + var bound_funct + 
  constrains bound_funct :: "'a => nat"
  assumes a_in_R: "a \<in> carrier R"
  and a_local_nilpot: "\<forall>x\<in>carrier D. (a (^)\<^bsub>R\<^esub> (bound_funct x)) x = \<one>\<^bsub>D\<^esub>"
  and bound_is_least: "bound_funct x =(LEAST n. (a (^)\<^bsub>R\<^esub> (n::nat)) x = \<one>\<^bsub>D\<^esub>)"

text{*The following lemma maybe could be included in the @{text Group.thy} file; there is already a lemma called 
  @{thm [locale=group] nat_pow_one}, about @{term [locale=group] "\<one>\<^bsub>G\<^esub>"}, but nothing about @{term [locale=group] "(x::'a)(^)1"}*}

lemma (in monoid) nat_pow_1: assumes x: "x \<in> carrier G" shows "x (^)\<^bsub>G\<^esub> (1::nat) = x"
  using nat_pow_Suc [of x 0] and nat_pow_0 [of x] and l_one [OF x] by simp

text{*If the element @{term a} is nilpotent, with @{term [locale=local_nilpotent_term] "(a(^)\<^bsub>R\<^esub>(bound x)) x = \<one>\<^bsub>D\<^esub>"}, 
  and @{term [locale=local_nilpotent_term] "bound_funct x \<le> m"}, then @{term [locale=local_nilpotent_term] "(a(^)\<^bsub>R\<^esub>(m::nat)) x = \<one>\<^bsub>D\<^esub>"}*}

lemma (in local_nilpotent_term) a_n_zero_a_m_zero: assumes bound_le_m: "bound_funct x \<le> m" 
  shows "(a(^)\<^bsub>R\<^esub>(m)) x = \<one>\<^bsub>D\<^esub>"
proof (cases "x \<in> carrier D")
  case True 
  then have x_in_D: "x \<in> carrier D" by simp
  show "(a (^)\<^bsub>R\<^esub> m) x = \<one>"
    using a_local_nilpot and bound_le_m proof (induct m)
    case 0 assume bound_le_zero: "bound_funct x \<le> 0" and alpha_n: "\<forall>x\<in>carrier D. (a (^)\<^bsub>R\<^esub> bound_funct x) x = \<one>" with x_in_D
    show "(a (^)\<^bsub>R\<^esub> (0::nat)) x = \<one>\<^bsub>D\<^esub>" by auto
  next
    case (Suc m)
    assume hypo: "\<lbrakk>\<forall>x\<in>carrier D. (a (^)\<^bsub>R\<^esub> bound_funct x) x = \<one>; bound_funct x \<le> m\<rbrakk> \<Longrightarrow> (a (^)\<^bsub>R\<^esub> m) x = \<one>" 
      and a_bound_funct: "\<forall>x\<in>carrier D. (a (^)\<^bsub>R\<^esub> bound_funct x) x = \<one>" and bound_funct_le_Suc_m: "bound_funct x \<le> Suc m" 
    then show "(a (^)\<^bsub>R\<^esub> Suc m) x = \<one>"
    proof (cases "bound_funct x = Suc m")
      case True with a_bound_funct and x_in_D show ?thesis by auto
    next
      case False with bound_funct_le_Suc_m have "bound_funct x \<le> m " by arith
      with hypo and a_bound_funct have a_m: "(a (^)\<^bsub>R\<^esub> m) x = \<one>" by simp
      have "(a (^)\<^bsub>R\<^esub> Suc m) x  = (a \<otimes>\<^bsub>R\<^esub> (a (^)\<^bsub>R\<^esub> m)) x"
      proof -
	have "Suc m = (1::nat) + m" by arith
	with sym [OF nat_pow_mult [OF a_in_R, of "1" "m"]] and nat_pow_1 [OF a_in_R] show ?thesis by (simp only: expand_fun_eq)
      qed
      also from ring_R and x_in_D and a_m have "\<dots> = a \<one>" by simp
      also from ring_R and hom_completion_one [of D D a] and D_diff_group and a_in_R have "\<dots> = \<one>"
	unfolding diff_group_def comm_group_def group_def by simp
      finally show "(a (^)\<^bsub>R\<^esub> Suc m) x = \<one>" by simp
    qed
  qed
next
  case False
  with nat_pow_closed [OF a_in_R, of m] and ring_R and completion_closed2 [of " a (^)\<^bsub>R\<^esub> m " D D x] 
  show " (a (^)\<^bsub>R\<^esub> m) x = \<one>" unfolding hom_completion_def completion_fun2_def by simp
qed

text{*The following definition is the power series of the local nilpotent endomorphism @{term a} in an element of its domain @{term x}; 
  the power series is defined as the finite product in the differential group @{term D} of the powers 
  @{term [locale=local_nilpotent_term] "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x)"}, up to @{term "bound_funct x"}*}
text{*A different solution would be to consider the finite sum in the ring of endomorphisms @{term R}
  of terms @{term [locale=local_nilpotent_term] "\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i)"} and then apply it to each element of the domain @{term x}*}
text{*The first solution seems to me more coherent with the notion of "local nilpotency" we are dealing with, but both are identical*}

subsection{*Definition of power series and some lemmas*}

context local_nilpotent_term
begin
definition "power_series x == finprod D (\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i) x) {..bound_funct x}"
end

text{*Some results about the power series*}

lemma (in local_nilpotent_term) power_pi: "(op (^)\<^bsub>R\<^esub> a) \<in> {..(k::nat)} \<rightarrow> carrier R"
  using nat_pow_closed [OF a_in_R] and Pi_def [of "{..k}" "(\<lambda>i::nat. carrier R)"] by simp

lemma (in local_nilpotent_term) power_pi_D: "(\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i) x) \<in> {..(k::nat)} \<rightarrow> carrier D"
proof (unfold Pi_def, auto, cases "x \<in> carrier D")
  fix i
  assume "i \<le> k"
  from nat_pow_closed [OF a_in_R, of i] have a_i_in_R: "(a (^)\<^bsub>R\<^esub> i) \<in> carrier R" by simp
  case True with a_i_in_R and ring_R and hom_completion_closed [of "(a(^)\<^bsub>R\<^esub> i)" D D x] show "(a (^)\<^bsub>R\<^esub> i) x \<in> carrier D" by simp
next
  fix i
  assume "i \<le> k"
  from nat_pow_closed [OF a_in_R, of i] have a_i_in_R: "(a (^)\<^bsub>R\<^esub> i) \<in> carrier R" by simp
  case False with a_i_in_R completion_closed2 [of "(a (^)\<^bsub>R\<^esub> i)" D D x] and ring_R show "(a (^)\<^bsub>R\<^esub> i) x \<in> carrier D"
    unfolding hom_completion_def completion_fun2_def by simp
qed

text{*As we already stated, 
  @{term [locale=local_nilpotent_term] "\<lambda>x. finprod D (\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i) x) {..j}"} is equal to 
  @{term [locale=local_nilpotent_term] "\<lambda>x. (finsum R (\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i)) {..j}) x"}*}

lemma (in local_nilpotent_term) finprod_eq_finsum_bound_funct:
  shows "finprod D (\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i) x) {..bound_funct x} = ((finsum R (\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i)) {..bound_funct x}) x)"
proof (induct "bound_funct x")
  case 0
  from nat_pow_0 [of a] and finsum_0 [of "op (^)\<^bsub>R\<^esub> a"] and power_pi [of "0::nat"] and finprod_0 [of "(\<lambda>i::nat. (a(^)\<^bsub>R\<^esub> i) x)"]
    and power_pi_D [of x "0::nat"]
  show "(\<Otimes>i\<Colon>nat\<in>{..0\<Colon>nat}. (a (^)\<^bsub>R\<^esub> i) x) = finsum R (op (^)\<^bsub>R\<^esub> a) {..0\<Colon>nat} x" by simp
next
  case (Suc n)
  assume hypo: "(\<Otimes>i\<in>{..n}. (a (^)\<^bsub>R\<^esub> i) x) = finsum R (op (^)\<^bsub>R\<^esub> a) {..n} x"
  show "(\<Otimes>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x) = finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n} x"
  proof (cases "x \<in> carrier D")
    case True
    from finsum_Suc [OF power_pi, of n] have "finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n} = a (^)\<^bsub>R\<^esub> Suc n \<oplus>\<^bsub>R\<^esub> finsum R (op (^)\<^bsub>R\<^esub> a) {..n}" by simp
    with ring_R and True have "finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n} x = (a (^)\<^bsub>R\<^esub> Suc n) x \<otimes>\<^bsub>D\<^esub> (finsum R (op (^)\<^bsub>R\<^esub> a) {..n}) x" by simp
    moreover
    from True and finprod_Suc [OF power_pi_D, of x n] have "(\<Otimes>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> Suc n) x \<otimes> (\<Otimes>i\<in>{..n}. (a (^)\<^bsub>R\<^esub> i) x)"
      by simp
    with hypo have "(\<Otimes>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> Suc n) x \<otimes> (finsum R (op (^)\<^bsub>R\<^esub> a) {..n}) x" by simp
    ultimately show ?thesis by simp
  next
    case False
    from finsum_closed [OF _ power_pi] and finite_nat_iff_bounded [of "{..Suc n}"] have "finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n} \<in> carrier R" by simp
    with ring_R and completion_closed2 [of "finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n}" D D] and False 
    have finsum_one: "finsum R (op (^)\<^bsub>R\<^esub> a) {..Suc n} x = \<one>" unfolding hom_completion_def completion_fun2_def by simp
    moreover
    have "\<forall>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x = \<one>"
    proof
      fix i assume i_in_nat: "i \<in> {..Suc n}"
      from nat_pow_closed [OF a_in_R, of i] and ring_R and completion_closed2 [of _ D D] and False show "(a (^)\<^bsub>R\<^esub> i) x = \<one>" 
	unfolding hom_completion_def completion_fun2_def by simp
    qed
    with finprod_cong [of "{..Suc n}" "{..Suc n}" "(\<lambda>i. (a (^)\<^bsub>R\<^esub> i) x)" "\<lambda>x. \<one>"] and power_pi_D [of x "Suc n"]
    have "(\<Otimes>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x) = (\<Otimes>i\<in>{..Suc n}. \<one>)" by simp 
    with finprod_one [of "{..Suc n}"] and finite_nat_iff_bounded [of "{..Suc n}"] have finprod_one: "(\<Otimes>i\<in>{..Suc n}. (a (^)\<^bsub>R\<^esub> i) x) = \<one>"
      by simp
    ultimately show ?thesis by simp
  qed
qed

lemma (in local_nilpotent_term) power_series_closed: shows "(\<Otimes>i\<in>{..m::nat}. (a (^)\<^bsub>R\<^esub> i) x) \<in> carrier D"
proof (rule finprod_closed)
  from finite_nat_iff_bounded show "finite {..m}" by auto
  from power_pi_D [of x m] show "(\<lambda>i\<Colon>nat. (a (^)\<^bsub>R\<^esub> i) x) \<in> {..m} \<rightarrow> carrier D" by simp
qed

text{*The following result is equal to the previous one but for the case of definition of the power series*}

lemma (in local_nilpotent_term) power_series_closed2: "(\<Otimes>i\<in>{..bound_funct x}. (a (^)\<^bsub>R\<^esub> i) x) \<in> carrier D"
proof (rule finprod_closed)
  from finite_nat_iff_bounded show "finite {..bound_funct x}" by auto
  from power_pi_D [of x "bound_funct x"] and Pi_def [of "{..bound_funct x}" "(\<lambda>i::nat. carrier R)"]
  show "(\<lambda>i\<Colon>nat. (a (^)\<^bsub>R\<^esub> i) x) \<in> {..bound_funct x} \<rightarrow> carrier D" by simp
qed

lemma (in local_nilpotent_term) power_series_extended: assumes bf_le_m: "bound_funct x \<le> m" 
  shows "power_series x = finprod D (\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x) {..m}"
  using bf_le_m proof (induct m)
  case 0
  from this and power_series_def [of x] show "power_series x = (\<Otimes>i\<in>{..(0::nat)}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
next
  case (Suc m)
  assume hypo: "bound_funct x \<le> m \<Longrightarrow> power_series x = (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)" and bf_le_Suc_m: "bound_funct x \<le> Suc m"
  show "power_series x = (\<Otimes>i\<in>{..Suc m}. (a (^)\<^bsub>R\<^esub> i) x)"
  proof (cases "bound_funct x = Suc m")
    case True thus ?thesis unfolding power_series_def by simp
  next
    case False with bf_le_Suc_m and hypo have hypo_m: "power_series x = (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)" by arith
    from a_n_zero_a_m_zero [OF bf_le_Suc_m] have a_Suc_m_one: "(a (^)\<^bsub>R\<^esub> Suc m) x = \<one>".
    from power_pi_D [of x "Suc m"] and finprod_Suc [of "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x)" "m"]
    have "(\<Otimes>i\<in>{..Suc m}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> Suc m) x \<otimes> (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
    also from a_Suc_m_one have "\<dots> = \<one> \<otimes> (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
    also from hypo_m and D.l_one [OF power_series_closed [of x m]] have "\<dots> = power_series x" by simp
    finally show ?thesis by simp
  qed
qed

text{*The power series is itself an endomorphism of the differential group*}

lemma (in local_nilpotent_term) power_series_in_R: shows "power_series \<in> carrier R"
proof -
  have "power_series \<in> hom_completion D D"
  proof (unfold hom_completion_def hom_def Pi_def, auto)
    fix x
    assume x_in_D: "x \<in> carrier D"
    from power_series_closed [of x "bound_funct x"] and power_series_def [of x] show "power_series x \<in> carrier D" by simp
  next
    fix x y
    assume x_in_D: "x \<in> carrier D" and y_in_D: "y \<in> carrier D"
    show "power_series (x \<otimes> y) = power_series x \<otimes> power_series y"
    proof -
      let ?max = "max (bound_funct (x \<otimes> y)) (max (bound_funct x) (bound_funct y))"
      from power_series_extended [of "x \<otimes> y" ?max] have p_s_ex_xy: "power_series (x \<otimes> y) = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) (x \<otimes> y))" by arith
      from power_series_extended [of x ?max] have p_s_ex_x: "power_series x = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) x)" by arith
      from power_series_extended [of y ?max] have p_s_ex_y: "power_series y = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) y)" by arith
      from p_s_ex_x and p_s_ex_y
      have "power_series x \<otimes> power_series y = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) x) \<otimes> (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) y)" by simp
      also from sym [OF finprod_mult [of "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x)" ?max "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) y)"]] 
	and power_pi_D [of x ?max] power_pi_D [of y ?max] and finite_nat_iff_bounded [of "{..?max}"]
      have "\<dots> = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) x \<otimes> (a (^)\<^bsub>R\<^esub> i) y)" by simp
      also from nat_pow_closed [OF a_in_R] and hom_completion_mult [OF _ x_in_D y_in_D, of _ D] and ring_R
      have "\<dots> = (\<Otimes>i\<in>{..?max}. (a (^)\<^bsub>R\<^esub> i) (x \<otimes> y))" by simp
      also from sym [OF p_s_ex_xy] have "\<dots> = power_series (x \<otimes> y)" by simp
      finally show ?thesis by simp
    qed
  next
    show "power_series \<in> completion_fun2 D D"
    proof (unfold completion_fun2_def completion_def expand_fun_eq, simp, intro exI [of _ "power_series"], auto)
      fix x
      assume "x \<notin> carrier D" 
      with nat_pow_closed [OF a_in_R] and completion_closed2 [of _ D D x] and ring_R have "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x) = (\<lambda>i::nat. \<one>)"
	by (unfold hom_completion_def expand_fun_eq, auto)
      with finprod_one [of "{..bound_funct x}"] and power_series_def [of x]
      show "power_series x = \<one>" by auto
    qed
  qed
  with ring_R show "power_series \<in> carrier R" by simp
qed

subsection{*Some basic operations over finite series*}

text{*Right distributivity of the product*}

lemma (in ring) finsum_dist_r: assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R" 
  shows "b \<otimes> finsum R (op (^) a) {..(m::nat)} = (\<Oplus>i\<in>{..(m::nat)}. b \<otimes> a (^) i)"
proof (induct m)
  case 0
  from finsum_0 [of "\<lambda>i::nat. a(^)i"] and finsum_0 [of "\<lambda>i::nat. b \<otimes> a(^)i"] and b_in_R
  show " b \<otimes> finsum R (op (^) a) {..(0::nat)} = (\<Oplus>i\<in>{..(0::nat)}. b \<otimes> a (^) i)" by simp
next
  case (Suc m)
  assume hypo: "b \<otimes> finsum R (op (^) a) {..m} = (\<Oplus>i\<in>{..m}. b \<otimes> a (^) i)"
  show "b \<otimes> finsum R (op (^) a) {..Suc m} = (\<Oplus>i\<in>{..Suc m}. b \<otimes> a (^) i)"
  proof -
    from finsum_Suc [of "(op (^) a)" "m"] and Pi_def [of "{..Suc m}" "\<lambda>i::nat. carrier R"] nat_pow_closed [OF a_in_R]
    have "b \<otimes> (\<Oplus>i\<in>{..Suc m}. a (^) i) = b \<otimes> (a(^)(Suc m) \<oplus> (\<Oplus>i\<in>{..m}. a (^) i))" by simp
    also from r_distr [OF nat_pow_closed [OF a_in_R, of "Suc m"] _ b_in_R, of "finsum R (op (^) a) {..m}"] 
      b_in_R nat_pow_closed [OF a_in_R, of "Suc m"] finsum_closed [of "{..m}" "op (^) a"] 
      and Pi_def [of "{..m}" "\<lambda>i::nat. carrier R"] nat_pow_closed [OF a_in_R] and finite_nat_iff_bounded [of "{..m}"]
    have "\<dots> = b \<otimes> a(^)(Suc m) \<oplus> b \<otimes> (\<Oplus>i\<in>{..m}. a (^) i)" by simp
    also from hypo have "\<dots> = b \<otimes> a(^)(Suc m) \<oplus> (\<Oplus>i\<in>{..m}. b \<otimes> a (^) i)" by simp
    also from finsum_Suc [of "(\<lambda>i::nat. b \<otimes> a (^) i)", of m] and Pi_def [of "{..Suc m}" "\<lambda>i::nat. carrier R"] 
      nat_pow_closed [OF a_in_R] and b_in_R
    have "\<dots> = (\<Oplus>i\<in>{..Suc m}. b \<otimes> a (^) i)" by simp
    finally show ?thesis by simp
  qed
qed

lemma (in local_nilpotent_term) b_power_pi_D: assumes b_in_R: "b \<in> carrier R" shows "(\<lambda>i. b ((a (^)\<^bsub>R\<^esub> i) x)) \<in> {..(k::nat)} \<rightarrow> carrier D"
  using power_pi_D [of x k] and ring_R and b_in_R unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def by auto

lemma (in local_nilpotent_term) nat_pow_closed_D: shows "(a (^)\<^bsub>R\<^esub> (m::nat)) x \<in> carrier D"
  using ring_R and nat_pow_closed [OF a_in_R, of m] unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def by auto

text{*Left distributivity of the product of a finite sum*}

lemma (in local_nilpotent_term) power_series_dist_l: assumes b_in_R: "b \<in> carrier R"
  shows "b (\<Otimes>i\<in>{..(m::nat)}. (a (^)\<^bsub>R\<^esub> i) x) = (\<Otimes>i\<in>{..(m::nat)}. (b ((a (^)\<^bsub>R\<^esub> i) x)))"
proof (induct m)
  case 0
  from finprod_0 [of "(\<lambda>i. (a (^)\<^bsub>R\<^esub> i) x)"] and power_pi_D [of x "0::nat"] and finprod_0 [of "(\<lambda>i. b ((a (^)\<^bsub>R\<^esub> i) x))"] 
    and b_power_pi_D [OF b_in_R, of x "0::nat"] show "b (\<Otimes>i\<in>{..0::nat}. (a (^)\<^bsub>R\<^esub> i) x) = (\<Otimes>i\<in>{..0::nat}. b ((a (^)\<^bsub>R\<^esub> i) x))" by simp
next
  case (Suc m)
  assume hypo: "b (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x) = (\<Otimes>i\<in>{..m}. b ((a (^)\<^bsub>R\<^esub> i) x))"
  show "b (\<Otimes>i\<in>{..Suc m}. (a (^)\<^bsub>R\<^esub> i) x) = (\<Otimes>i\<in>{..Suc m}. b ((a (^)\<^bsub>R\<^esub> i) x))"
  proof -
    from finprod_Suc [OF power_pi_D [of x], of m] have "b (\<Otimes>i\<in>{..Suc m}. (a (^)\<^bsub>R\<^esub> i) x) = b ((a (^)\<^bsub>R\<^esub> Suc m) x \<otimes> (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x))"
      by simp
    also from b_in_R and ring_R and hom_completion_mult [of b D D "(a (^)\<^bsub>R\<^esub> Suc m) x" " (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)"] 
      and finprod_closed [of "{..m}" "(\<lambda>i. (a (^)\<^bsub>R\<^esub> i) x)"] power_pi_D [of x m] nat_pow_closed_D [of "Suc m" x]
    have "\<dots> =  b ((a (^)\<^bsub>R\<^esub> Suc m) x) \<otimes> b ((\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x))" by simp
    also from hypo have "\<dots> = b ((a (^)\<^bsub>R\<^esub> Suc m) x) \<otimes> (\<Otimes>i\<in>{..m}. b ((a (^)\<^bsub>R\<^esub> i) x))" by simp
    also from sym [OF finprod_Suc [OF b_power_pi_D [OF b_in_R, of x], of m]] have "\<dots> = (\<Otimes>i\<in>{..Suc m}. b ((a (^)\<^bsub>R\<^esub> i) x))" by simp
    finally show ?thesis by simp
  qed
qed

lemma (in local_nilpotent_term) power_pi_b_D: assumes b_in_R: "b \<in> carrier R" shows "(\<lambda>i. (a (^)\<^bsub>R\<^esub> i) (b x)) \<in> {..(k::nat)} \<rightarrow> carrier D"
  using power_pi_D [of "b x" k] and ring_R and b_in_R by simp

lemma (in local_nilpotent_term) power_series_dist_r: assumes b_in_R: "b \<in> carrier R"
  shows "(\<lambda>x. (\<Otimes>i\<in>{..m}. (a (^)\<^bsub>R\<^esub> i) x)) (b x) = (\<Otimes>i\<in>{..(m::nat)}. ((a (^)\<^bsub>R\<^esub> i) (b x)))" by simp

text{*The following lemma showed to be useful in some situations*}

lemma (in comm_monoid) finprod_singleton [simp]:
  "f \<in> {i::nat} -> carrier G ==> finprod G f {i} = f i" by (simp add: Pi_def)

text{*Finite series can be decomposed in the product of its first element and the remaining part*}

lemma (in local_nilpotent_term) power_series_first_element: 
  shows "finprod D (\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x) {..(i::nat)} = (a(^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> finprod D (\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x) {1..(i::nat)}"
proof (induct i)
  case 0 
  from ring_R have one_x: "\<one>\<^bsub>R\<^esub> x \<in> carrier D" unfolding hom_completion_def completion_fun2_def completion_def by auto
  from finprod_0 [of "(\<lambda>i. (a (^)\<^bsub>R\<^esub> i) x)"] and power_pi_D [of x 0] and  D.r_one [OF one_x]
  show "(\<Otimes>i\<in>{..(0::nat)}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{(1::nat)..0}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
next
  case (Suc i)
  assume hypo: "(\<Otimes>i\<in>{..i}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)"
  show "(\<Otimes>i\<in>{..Suc i}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{1..Suc i}. (a (^)\<^bsub>R\<^esub> i) x)"
  proof -
    from finprod_Suc [of "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x)" i] and power_pi_D [of x "Suc i"]
    have "(\<Otimes>i\<in>{..Suc i}. (a (^)\<^bsub>R\<^esub> i) x) = (a (^)\<^bsub>R\<^esub> Suc i) x \<otimes> (\<Otimes>i\<in>{..i}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
    also from hypo have "\<dots> = (a (^)\<^bsub>R\<^esub> Suc i) x \<otimes> ((a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x))" by simp
    also have "\<dots> =  ((a (^)\<^bsub>R\<^esub> Suc i) x \<otimes> (a (^)\<^bsub>R\<^esub> (0::nat)) x) \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)"
    proof (rule sym [OF D.m_assoc [of "(a (^)\<^bsub>R\<^esub> Suc i) x" "(a (^)\<^bsub>R\<^esub> (0::nat)) x" "(\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)"]])
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)\<^bsub>R\<^esub> Suc i) x \<in> carrier D" by simp
      from  nat_pow_closed_D [of "0::nat" x] show "(a (^)\<^bsub>R\<^esub> (0::nat)) x \<in> carrier D" by simp
      from finprod_closed [of "{1..i}" "(\<lambda>i::nat. (a(^)\<^bsub>R\<^esub>i) x)"] and finite_nat_iff_bounded [of "{1..i}"] 
	and nat_pow_closed_D [of _ x] and Pi_def [of "{1..i}" "\<lambda>i::nat. carrier D"] 
      show "(\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x) \<in> carrier D" by simp
    qed
    also from m_comm [OF nat_pow_closed_D [of "Suc i" x] nat_pow_closed_D [of "0::nat" x]]
    have "\<dots> = ((a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (a (^)\<^bsub>R\<^esub> Suc i) x) \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
    also have "\<dots> = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> ((a (^)\<^bsub>R\<^esub> Suc i) x \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x))"
    proof (rule D.m_assoc [of "(a (^)\<^bsub>R\<^esub> (0::nat)) x" "(a (^)\<^bsub>R\<^esub> (Suc i)) x" "(\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)"])
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)\<^bsub>R\<^esub> Suc i) x \<in> carrier D" by simp
      from  nat_pow_closed_D [of "0::nat" x] show "(a (^)\<^bsub>R\<^esub> (0::nat)) x \<in> carrier D" by simp
      from finprod_closed [of "{1..i}" "(\<lambda>i::nat. (a(^)\<^bsub>R\<^esub>i) x)"] and finite_nat_iff_bounded [of "{1..i}"] 
	and nat_pow_closed_D [of _ x] and Pi_def [of "{1..i}" "\<lambda>i::nat. carrier D"] 
      show "(\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x) \<in> carrier D" by simp
    qed
    also from nat_pow_closed_D [of "Suc i" x] 
    have "\<dots> = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> ((\<Otimes>i\<in>{Suc i}. (a (^)\<^bsub>R\<^esub> i) x) \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x))" by simp
    also from sym [OF finprod_Un_disjoint [of "{Suc i}" "{1..i}" "(\<lambda>i::nat. (a (^)\<^bsub>R\<^esub> i) x)"]]
      and finite_nat_iff_bounded [of "{1..i}"] finite_nat_iff_bounded [of "{Suc i}"] and Pi_def [of "{(1::nat)..i}" "(\<lambda>i::nat. carrier D)"]
      Pi_def [of "{Suc i}" "(\<lambda>i::nat. carrier D)"] and nat_pow_closed_D [of "Suc i" x] nat_pow_closed_D [of _ x]
    have "(a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> ((\<Otimes>i\<in>{Suc i}. (a (^)\<^bsub>R\<^esub> i) x) \<otimes> (\<Otimes>i\<in>{1..i}. (a (^)\<^bsub>R\<^esub> i) x)) 
      = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{1..i} \<union> {Suc i}. (a (^)\<^bsub>R\<^esub> i) x)" by simp
    also have "\<dots> = (a (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>i\<in>{1..Suc i}. (a (^)\<^bsub>R\<^esub> i) x)"
    proof -
      have "{1..i} \<union> {Suc i} = {1..Suc i}" by auto
      then show ?thesis by simp
    qed
    finally show ?thesis by simp
  qed
qed

text{*Finite series which start in index one can be seen as the product of the generic term and the finite series in index zero*}

lemma (in local_nilpotent_term) power_series_factor: shows "(\<Otimes>j\<in>{(1::nat)..Suc i}. (a (^)\<^bsub>R\<^esub> j) x) = a (\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x)"
proof (induct i)
  case 0
  have "a x = a (\<one>\<^bsub>R\<^esub> x)"
  proof (cases "x \<in> carrier D")
    case True with ring_R show "a x = a (\<one>\<^bsub>R\<^esub> x)" by simp
  next
    case False with completion_closed2 [of a D D x] hom_completion_one [of D D a] and D_diff_group and a_in_R and ring_R 
    show "a x = a (\<one>\<^bsub>R\<^esub> x)" unfolding diff_group_def comm_group_def group_def hom_completion_def completion_fun2_def by simp
  qed
  with finprod_0 [of "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)"] finprod_insert [of "{}" "Suc 0" "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)"] 
    and nat_pow_closed_D [of "Suc 0" x] and  nat_pow_closed_D [of 0 x] a_in_R finprod_singleton [of "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)" "Suc 0"]
  show "(\<Otimes>j\<in>{1..Suc 0}. (a (^)\<^bsub>R\<^esub> j) x) = a (\<Otimes>j\<in>{..0::nat}. (a (^)\<^bsub>R\<^esub> j) x)" by simp
next
  case (Suc i)
  assume hypo: "(\<Otimes>j\<in>{1..Suc i}. (a (^)\<^bsub>R\<^esub> j) x) = a (\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x)"
  show "(\<Otimes>j\<in>{1..Suc (Suc i)}. (a (^)\<^bsub>R\<^esub> j) x) = a (\<Otimes>j\<in>{..Suc i}. (a (^)\<^bsub>R\<^esub> j) x)"
  proof -
    have "(\<Otimes>j\<in>{1..Suc (Suc i)}. (a (^)\<^bsub>R\<^esub> j) x) = (\<Otimes>j\<in>{1..Suc i} \<union> {Suc (Suc i)}. (a (^)\<^bsub>R\<^esub> j) x)"
    proof -
      have "{1..Suc i} \<union> {Suc (Suc i)} = {1..Suc (Suc i)}" by auto
      thus ?thesis by simp
    qed
    also from finprod_Un_disjoint [of "{1..Suc i}" "{Suc (Suc i)}" "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)"]
      and finite_nat_iff_bounded [of "{1..Suc i}"] finite_nat_iff_bounded [of "{Suc (Suc i)}"] and 
      Pi_def [of "{(1::nat)..Suc i}" "(\<lambda>j::nat. carrier D)"]
      Pi_def [of "{Suc (Suc i)}" "(\<lambda>j::nat. carrier D)"] and nat_pow_closed_D [of "Suc (Suc i)" x] nat_pow_closed_D [of _ x]
    have "\<dots> = (\<Otimes>j\<in>{1..Suc i}. (a (^)\<^bsub>R\<^esub> j) x) \<otimes> (\<Otimes>j\<in>{Suc (Suc i)}. (a (^)\<^bsub>R\<^esub> j) x)" by simp
    also from hypo and finprod_singleton [of "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)" "Suc (Suc i)"] and nat_pow_closed_D [of "Suc (Suc i)" x]
    have "\<dots> = a (\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x) \<otimes> ((a (^)\<^bsub>R\<^esub> Suc (Suc i)) x)" by simp
    also from ring_R have "\<dots> = a (\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x) \<otimes> a ((a (^)\<^bsub>R\<^esub> Suc i) x)"
    proof -
      have "1 + Suc i = Suc (Suc i)" by arith
      with sym [OF nat_pow_mult [OF a_in_R, of "1" "Suc i"]] and nat_pow_1 [OF a_in_R]
      have "a (^)\<^bsub>R\<^esub> Suc (Suc i) = a \<otimes>\<^bsub>R\<^esub> (a (^)\<^bsub>R\<^esub> Suc i)" by simp
      with ring_R have "((a (^)\<^bsub>R\<^esub> Suc (Suc i)) x) = a ((a (^)\<^bsub>R\<^esub> Suc i) x)" by simp
      then show ?thesis by simp
    qed
    also have "\<dots> = a ((\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x) \<otimes> (a (^)\<^bsub>R\<^esub> Suc i) x)"
    proof (intro sym [OF hom_completion_mult [of a D D "\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x" "(a (^)\<^bsub>R\<^esub> Suc i) x"]])
      from ring_R and a_in_R show "a \<in> hom_completion D D" by simp
      from finprod_closed [of "{..i}" "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)"] and power_pi_D [of x i]
      show "(\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x) \<in> carrier D" by simp
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)\<^bsub>R\<^esub> Suc i) x \<in> carrier D" by simp
    qed
    also from nat_pow_closed_D [of "Suc i" x] have "\<dots> = a ((\<Otimes>j\<in>{..i}. (a (^)\<^bsub>R\<^esub> j) x) \<otimes> (\<Otimes>j\<in>{Suc i}.(a (^)\<^bsub>R\<^esub> Suc i) x))"
      by simp
    also from sym [OF finprod_Un_disjoint [of "{..i}" "{Suc i}" "(\<lambda>j::nat. (a (^)\<^bsub>R\<^esub> j) x)"]]
      and finite_nat_iff_bounded [of "{..i}"] finite_nat_iff_bounded [of "{Suc i}"] and Pi_def [of "{..i}" "(\<lambda>j::nat. carrier D)"]
      Pi_def [of "{Suc i}" "(\<lambda>j::nat. carrier D)"] and nat_pow_closed_D [of "Suc i" x] nat_pow_closed_D [of _ x]
    have "\<dots> = a (\<Otimes>j\<in>{..i} \<union> {Suc i}. (a (^)\<^bsub>R\<^esub> j) x)" by simp
    also have "\<dots> = a (\<Otimes>j\<in>{..Suc i}. (a (^)\<^bsub>R\<^esub> j) x)"
    proof -
      have "{..i} \<union> {Suc i} = {..Suc i}" by auto
      thus ?thesis by simp
    qed
    finally show ?thesis by simp
  qed
qed

text{*If we were able to interpret locales, now the idea would be to interpret the @{text "locale nilpotent_term"} with 
  local nilpotent term @{term "\<alpha>"}, as later defined in locale @{text alpha_beta}*}

subsection{*Definition and some lemmas of perturbations*}

text{*Perturbations are a homomorphism of @{term [locale=ring_endomorphisms] "D"} (not a differential homomorphism!) 
  such that its addition with the differential is again a differential*}

constdefs (structure D)
  pert :: "_ => ('a => 'a) set"
  "pert D == {\<delta>. \<delta> \<in> hom_completion D D & 
  diff_group \<lparr> carrier = carrier D, mult = mult D, one = one D, diff = (\<lambda>x. if x \<in> carrier D then ((differ) x) \<otimes> (\<delta> x) else \<one>)\<rparr> }"

locale diff_group_pert = diff_group D + var \<delta> +
  assumes delta_pert: "\<delta> \<in> pert D"

lemma (in diff_group_pert) diff_group_pert_is_diff_group: 
  shows "diff_group \<lparr>carrier = carrier D, mult = mult D, one = one D, diff = (\<lambda>x. if x \<in> carrier D then ((differ\<^bsub>D\<^esub>) x) \<otimes>\<^bsub>D\<^esub> (\<delta> x) else \<one>\<^bsub>D\<^esub>)\<rparr>"
  using diff_group_pert.delta_pert [of D \<delta>] and prems unfolding diff_group_pert_def pert_def by simp

lemma (in diff_group_pert) pert_is_hom: shows "\<delta> \<in> hom_completion D D"
  using diff_group_pert.delta_pert [of D \<delta>] and prems unfolding diff_group_pert_def pert_def by simp

lemma (in ring_endomorphisms) diff_group_pert_is_diff_group: assumes delta: "\<delta> \<in> pert D"
  shows "diff_group \<lparr> carrier = carrier D, mult = mult D, one = one D, diff = (differ\<^bsub>D\<^esub>) \<oplus>\<^bsub>R\<^esub> \<delta> \<rparr>"
  using diff_group_pert.diff_group_pert_is_diff_group [of D \<delta>] and ring_R and prems
  unfolding diff_group_pert_def diff_group_pert_axioms_def ring_endomorphisms_def by simp

lemma (in ring_endomorphisms) pert_in_R [simp]: assumes delta: "\<delta> \<in> pert D" shows "\<delta> \<in> carrier R"
  using ring_R and diff_group_pert.pert_is_hom [of D \<delta>] and prems
  unfolding diff_group_pert_def diff_group_pert_axioms_def ring_endomorphisms_def by simp

lemma (in ring_endomorphisms) diff_pert_in_R [simp]: assumes delta: "\<delta> \<in> pert D" shows "(differ\<^bsub>D\<^esub>) \<oplus>\<^bsub>R\<^esub> \<delta> \<in> carrier R" 
  using delta by simp

text{*The reason to introduce @{term \<alpha>} by means of a @{text "defines"} command is to get the expected behavior when merging this locale 
  with locale @{text "local_nilpotent_term D R \<alpha> bound_phi"} in the definition of locale @{text "local_nilpotent_alpha"}*}

locale alpha_beta = ring_endomorphisms + reduction + var \<delta> + var \<alpha> +
  assumes delta_pert: "\<delta> \<in> pert D"
  defines alpha_def: "\<alpha> == \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h)"

  (*definition (in alpha_beta)
  alpha_def: "\<alpha> = \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h)"
  *)

context alpha_beta
begin

definition beta_def: "\<beta> = \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>)"

end

locale local_nilpotent_alpha = alpha_beta + local_nilpotent_term D R \<alpha> bound_phi

text{*The definition of @{term \<Phi>} corresponds with the one given in the Basic Perturbation Lemma, Lemma 2.3.1 in Aransay's memoir*}

context local_nilpotent_alpha
begin

definition phi_def: "\<Phi> == local_nilpotent_term.power_series D R \<alpha> bound_phi"

end

lemma (in alpha_beta) pert_in_R [simp]: shows "\<delta> \<in> carrier R"
  using delta_pert and ring_R by (unfold pert_def, simp)

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

lemma (in alpha_beta) alpha_in_R: shows "\<alpha> \<in> carrier R"
  using alpha_def and pert_in_R and h_in_R by simp

lemma (in alpha_beta) beta_in_R: shows "\<beta> \<in> carrier R"
  using beta_def and pert_in_R and h_in_R by simp

lemma (in alpha_beta) alpha_i_in_R: shows "\<alpha>(^)\<^bsub>R\<^esub> (i::nat) \<in> carrier R"
  using alpha_in_R and R.nat_pow_closed by simp

lemma (in alpha_beta) beta_i_in_R: shows "\<beta>(^)\<^bsub>R\<^esub> (i::nat) \<in> carrier R"
  using beta_in_R and nat_pow_closed by simp

lemma (in ring) power_minus_a_b: 
  assumes a: "a \<in> carrier R" and b: "b \<in> carrier R" shows "(\<ominus> (a \<otimes> b)) (^) Suc n = \<ominus> a \<otimes> ((\<ominus> (b \<otimes> a)) (^) n) \<otimes> b"
proof (induct n)
  case 0
  from a and b and nat_pow_0 [of "a \<otimes> b"] show "\<ominus> (a \<otimes> b) (^) Suc 0 = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) (0::nat) \<otimes> b" by simp algebra
next
  case (Suc n)
  assume hypo: "(\<ominus> (a \<otimes> b)) (^) Suc n = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) n \<otimes> b"
  have "(\<ominus> (a \<otimes> b)) (^) Suc (Suc n) = \<ominus> (a \<otimes> b) (^) (Suc n) \<otimes> \<ominus> (a \<otimes> b)" by simp
  also from hypo have "\<dots> = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) n \<otimes> b \<otimes> \<ominus> (a \<otimes> b)" by simp
  also from sym [OF l_minus [OF a b]] have "\<dots> = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) n \<otimes> b \<otimes> (\<ominus> a \<otimes> b)" by simp 
  also from sym [OF m_assoc [OF b _ b, of "\<ominus> a"]] and a_inv_closed [OF a] and nat_pow_closed [of "\<ominus> (b \<otimes> a)" n] 
    and a_inv_closed [of "b \<otimes> a"] and a b r_minus [OF b a]
  have "\<dots> = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) n \<otimes> (\<ominus> (b \<otimes> a) \<otimes> b)" by algebra
  also from nat_pow_closed [of "\<ominus> (b \<otimes> a)" n] and a_inv_closed [of "b \<otimes> a"] and a b 
    and sym [OF m_assoc[of "(\<ominus> (b \<otimes> a)) (^) n" "(\<ominus> (b \<otimes> a))" b]]
  have "\<dots> = \<ominus> a \<otimes> (\<ominus> (b \<otimes> a) (^) n \<otimes> (\<ominus> (b \<otimes> a))) \<otimes> b" by algebra
  also from sym [OF nat_pow_Suc [of "\<ominus> (b \<otimes> a)" n]]
  have "\<dots> = \<ominus> a \<otimes> (\<ominus> (b \<otimes> a)) (^) (Suc n) \<otimes> b" by simp 
  finally show "\<ominus> (a \<otimes> b) (^) Suc (Suc n) = \<ominus> a \<otimes> \<ominus> (b \<otimes> a) (^) Suc n \<otimes> b" by simp
qed

text{*The following comment is already obsolete in the @{text "Isabelle_11-Feb-2007"} repository version*}
text{*Comment: At the moment, the "definition" command is not inherited by locales defined from old ones; in the following lemma, 
  there would be two ways of recovering the definition of @{term [locale=alpha_beta] \<beta>}. The first one would be to 
  give its long name @{text "local_nilpotent_alpha.\<beta> \<delta>"}, and the other way is to use abbreviations.*}
text{*Due to aesthetic reasons, we choose the second solution, while waiting to the "definition" command to be properly inherited*}

text{*@{text "abbreviation (in local_nilpotent_alpha) \<beta> == alpha_beta.\<beta> R h \<delta>"}*}

text{*The following lemma proves that whenever @{term [locale=local_nilpotent_alpha] "\<alpha>"} is a local nilpotent term,
  so will be @{term [locale=local_nilpotent_alpha] "\<beta>"}*}

lemma (in local_nilpotent_alpha) nilp_alpha_nilp_beta: shows "local_nilpotent_term D R \<beta> (\<lambda>x. (LEAST n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>\<^bsub>D\<^esub>))"
proof (unfold local_nilpotent_alpha_def local_nilpotent_term_def local_nilpotent_term_axioms_def, simp, intro conjI)
  from prems show "ring_endomorphisms D R" by intro_locales
  from beta_in_R show "\<beta> \<in> carrier R" by simp
  show "\<forall>x\<in>carrier D. (\<beta> (^)\<^bsub>R\<^esub> (LEAST n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>)) x = \<one>"
  proof (intro ballI)
    fix x assume x_in_D: "x \<in> carrier D"
    show "(\<beta> (^)\<^bsub>R\<^esub> (LEAST n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>)) x = \<one>"
    proof (rule LeastI_ex [of "\<lambda>n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>"])
      from a_local_nilpot and pert_in_R and ring_R and hom_completion_closed [OF _ x_in_D, of \<delta> D]
      have alpha_nilpot: "(\<alpha> (^)\<^bsub>R\<^esub> bound_phi (\<delta> x)) (\<delta> x) = \<one>" by simp
      from beta_def have "(\<beta> (^)\<^bsub>R\<^esub> (Suc (bound_phi (\<delta> x)))) x = ((\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>)) (^)\<^bsub>R\<^esub> (Suc (bound_phi (\<delta> x)))) x" by simp
      also from h_in_R and pert_in_R and power_minus_a_b [OF h_in_R pert_in_R, of "bound_phi (\<delta> x)"]
      have "\<dots> = (\<ominus>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) (^)\<^bsub>R\<^esub> (bound_phi (\<delta> x))) \<otimes>\<^bsub>R\<^esub> \<delta>) x" by simp
      also from alpha_nilpot and alpha_def and ring_R have "\<dots> = (\<ominus>\<^bsub>R\<^esub> h) \<one>" by simp
      also from a_inv_closed [OF h_in_R] and ring_R and hom_completion_one [of D D "\<ominus>\<^bsub>R\<^esub> h"] and D_diff_group
      have "\<dots> = \<one>" by (unfold diff_group_def comm_group_def group_def, simp)
      finally have beta_nil: "(\<beta> (^)\<^bsub>R\<^esub> (Suc (bound_phi (\<delta> x)))) x = \<one>" by simp
      from exI [of "\<lambda>n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>" "(Suc (bound_phi (\<delta> x)))"] and beta_nil
      show "\<exists>n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>" by simp 
    qed
  qed
qed

lemma (in local_nilpotent_alpha) bound_psi_exists: shows "\<exists>bound_psi. local_nilpotent_term D R \<beta> bound_psi"
  using nilp_alpha_nilp_beta by iprover

context local_nilpotent_alpha
begin

definition "bound_psi \<equiv> (\<lambda>x. (LEAST n::nat. (\<beta> (^)\<^bsub>R\<^esub> n) x = \<one>\<^bsub>D\<^esub>))"

text{*The definition of @{term \<Psi>} below is equivalent to the one given in the statement of Lemma 2.3.1 in Aransay's memoir*}

definition psi_def: "\<Psi> \<equiv> local_nilpotent_term.power_series D R \<beta> bound_psi"

end

subsection{*Some properties of the endomorphisms @{term "\<Phi>"}, @{term "\<Psi>"}, @{term "\<alpha>"} and @{term "\<beta>"}*}

lemma (in local_nilpotent_alpha) local_nilpotent_term_alpha: shows "local_nilpotent_term D R \<alpha> bound_phi"
  using prems by (unfold local_nilpotent_alpha_def local_nilpotent_term_def, simp)

lemma (in local_nilpotent_alpha) local_nilpotent_term_beta: shows "local_nilpotent_term D R \<beta> bound_psi"
  using prems and nilp_alpha_nilp_beta and bound_psi_def by (unfold local_nilpotent_term_def, simp)

lemma (in local_nilpotent_alpha) phi_x_in_D [simp]: shows "\<Phi> x \<in> carrier D"
  using phi_def local_nilpotent_term.power_series_def [OF local_nilpotent_term_alpha, of x]
    D.finprod_closed [of "{..bound_phi x}" "(\<lambda>i::nat. (\<alpha>(^)\<^bsub>R\<^esub>i) x)"] and finite_nat_iff_bounded [of "{..bound_phi x}"] 
    and local_nilpotent_term.power_pi_D [OF local_nilpotent_term_alpha, of x "bound_phi x"] by simp

lemma (in local_nilpotent_alpha) phi_in_R [simp]: shows "\<Phi> \<in> carrier R"
  using phi_def local_nilpotent_term.power_series_in_R [OF local_nilpotent_term_alpha] by simp
 
lemma (in local_nilpotent_alpha) phi_in_hom: shows "\<Phi> \<in> hom_completion D D"
  using phi_in_R and ring_R by simp
  
lemma (in local_nilpotent_alpha) psi_in_R [simp]: shows "\<Psi> \<in> carrier R"
  using psi_def local_nilpotent_term.power_series_in_R [OF local_nilpotent_term_beta] by simp
  
lemma (in local_nilpotent_alpha) psi_in_hom: shows "\<Psi> \<in> hom_completion D D"
  using psi_in_R and ring_R by simp

lemma (in local_nilpotent_alpha) psi_x_in_D [simp]: shows "\<Psi> x \<in> carrier D"
  using psi_def local_nilpotent_term.power_series_def [OF local_nilpotent_term_beta, of x]
    D.finprod_closed [of "{..bound_psi x}" "(\<lambda>i::nat. (\<alpha>(^)\<^bsub>R\<^esub>i) x)"] and finite_nat_iff_bounded [of "{..bound_psi x}"] 
    and local_nilpotent_term.power_pi_D [OF local_nilpotent_term_beta, of x "bound_psi x"] by simp

lemma (in local_nilpotent_alpha) h_alpha_eq_beta_h: "h \<otimes>\<^bsub>R\<^esub> \<alpha>(^)\<^bsub>R\<^esub>(i::nat) = \<beta> (^)\<^bsub>R\<^esub> i \<otimes>\<^bsub>R\<^esub> h"
proof (induct i)
  case 0
  from h_in_R and R.nat_pow_0 show "h \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> (0::nat) = \<beta> (^)\<^bsub>R\<^esub> (0::nat) \<otimes>\<^bsub>R\<^esub> h" by simp
next
  case (Suc i)
  assume hypo: "h \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> i = \<beta> (^)\<^bsub>R\<^esub> i \<otimes>\<^bsub>R\<^esub> h"
  from R.nat_pow_mult [OF beta_in_R, of "(1::nat)" i] and R.nat_pow_1 [OF beta_in_R]
  have "\<beta> (^)\<^bsub>R\<^esub> (Suc i) \<otimes>\<^bsub>R\<^esub> h = \<beta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i \<otimes>\<^bsub>R\<^esub> h" by simp
  also from hypo and R.m_assoc [OF beta_in_R beta_i_in_R [of i] h_in_R] have "\<dots> = \<beta> \<otimes>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> i)" by simp
  also from sym [OF R.m_assoc [OF beta_in_R h_in_R alpha_i_in_R [of i]]] and beta_def and h_in_R pert_in_R alpha_i_in_R [of i]
  have "\<dots> = h \<otimes>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> i" by algebra
  also from R.m_assoc [OF h_in_R _ alpha_i_in_R [of i], of "\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h)"] pert_in_R h_in_R
  have "\<dots> = h \<otimes>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> i)" by simp
  also from alpha_def and sym [OF R.nat_pow_1 [OF alpha_in_R]] and R.nat_pow_mult [OF alpha_in_R, of "(1::nat)" i]
  have "\<dots> = h \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> (Suc i)" by simp
  finally show "h \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> Suc i = \<beta> (^)\<^bsub>R\<^esub> Suc i \<otimes>\<^bsub>R\<^esub> h" by simp
qed

subsection{*Lemmas 2.2.1 to 2.2.6*}

text{*Lemma 2.2.1*}

lemma (in local_nilpotent_alpha) lemma_2_2_1: shows "bound_psi (h x) \<le> bound_phi x"
proof -
  from h_alpha_eq_beta_h and ring_R have "(\<beta> (^)\<^bsub>R\<^esub> bound_phi x) (h x) = (h ((\<alpha> (^)\<^bsub>R\<^esub> bound_phi x) x))" by (auto simp add: expand_fun_eq)
  also have "\<dots> = h (\<one>)"
  proof (cases "x \<in> carrier D")
    case True with local_nilpotent_term.a_local_nilpot [OF local_nilpotent_term_alpha] show ?thesis by simp
  next
    case False from alpha_i_in_R [of "bound_phi x"] and ring_R and completion_closed2 [OF _ False, of "\<alpha> (^)\<^bsub>R\<^esub> bound_phi x"  D]
    show ?thesis unfolding hom_completion_def by simp
  qed
  also from hom_completion_one [of D D h] h_in_R ring_R and D_diff_group have "\<dots> = \<one>" unfolding diff_group_def comm_group_def group_def by simp
  finally have beta_x_h_x_eq_one: "(\<beta> (^)\<^bsub>R\<^esub> bound_phi x) (h x) = \<one>" by simp
  have beta_h_x_h_x_eq_one: "(\<beta> (^)\<^bsub>R\<^esub> bound_psi (h x)) (h x) = \<one>"
  proof (cases "h x \<in> carrier D")
    case True with local_nilpotent_term.a_local_nilpot [OF local_nilpotent_term_beta] show ?thesis by simp
  next
    case False with ring_R and h_in_R 
    show ?thesis unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def by auto
  qed
  from beta_x_h_x_eq_one and beta_h_x_h_x_eq_one 
    and local_nilpotent_term.bound_is_least [OF local_nilpotent_term_beta, of "h x"] 
    and Least_le [of "\<lambda>i::nat. (\<beta> (^)\<^bsub>R\<^esub> i) (h x) = \<one>" "bound_phi x"] show ?thesis by simp
qed

text{*Lemma 2.2.3 with endomorphisms applied to elements*}

lemma (in local_nilpotent_alpha) lemma_2_2_3_elements: shows "(h \<circ> \<Phi>) x = (\<Psi> \<circ> h) x"
proof -
  let ?max = "max (bound_phi x) (bound_psi x)"
  from ring_R have "(h \<circ> \<Phi>) x = h (\<Phi> x)" by simp
  also from phi_def have "\<dots> = h (local_nilpotent_term.power_series D R \<alpha> bound_phi x)" by simp
  also from local_nilpotent_term.power_series_extended [OF local_nilpotent_term_alpha, of x ?max]
    and le_maxI1 [of "bound_phi x" "bound_psi x"]
  have "\<dots> = h (\<Otimes>i\<in>{..?max}. (\<alpha> (^)\<^bsub>R\<^esub> i) x)" by simp
  also from local_nilpotent_term.power_series_dist_l [OF local_nilpotent_term_alpha h_in_R, of x ?max] and h_in_R
  have "\<dots> = (\<Otimes>i\<in>{..?max}. h ((\<alpha> (^)\<^bsub>R\<^esub> i) x))" by simp
  also from h_alpha_eq_beta_h and ring_R have "\<dots> = (\<Otimes>i\<in>{..?max}. ((\<beta> (^)\<^bsub>R\<^esub> i) (h x)))" by (auto simp add: expand_fun_eq)
  also from sym [OF local_nilpotent_term.power_series_extended [OF local_nilpotent_term_beta, of "h x" ?max]] 
    and lemma_2_2_1 [of x]
  have "\<dots> = local_nilpotent_term.power_series D R \<beta> bound_psi (h x)" by arith
  also from psi_def have "\<dots> = \<Psi> (h x)" by simp
  also have "\<dots> = (\<Psi> \<circ> h) x" by simp
  finally show ?thesis by simp
qed

text{*Lemma 2.2.3 with endomorphisms*}

corollary (in local_nilpotent_alpha) lemma_2_2_3: shows "(h \<circ> \<Phi>) = (\<Psi> \<circ> h)" using lemma_2_2_3_elements by (simp add: expand_fun_eq)

text{*The following lemma is simple a renaming of the previous one; the idea is to give to the previous result 
  the name it had before as a premise, to keep the files correspoding to the equational part of the proof working*}

lemma (in local_nilpotent_alpha) psi_h_h_phi: shows "\<Psi> \<otimes>\<^bsub>R\<^esub> h = h \<otimes>\<^bsub>R\<^esub> \<Phi>" using lemma_2_2_3 and ring_R by simp

lemma (in local_nilpotent_alpha) alpha_delta_eq_delta_beta: shows "\<alpha>(^)\<^bsub>R\<^esub>(i::nat) \<otimes>\<^bsub>R\<^esub> \<delta> = \<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i"
proof (induct i)
  case 0
  from pert_in_R and R.nat_pow_0 show "\<alpha> (^)\<^bsub>R\<^esub> (0::nat) \<otimes>\<^bsub>R\<^esub> \<delta> = \<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> (0::nat)" by simp
next
  case (Suc i)
  assume hypo: "\<alpha> (^)\<^bsub>R\<^esub> i \<otimes>\<^bsub>R\<^esub> \<delta> = \<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i"
  from R.nat_pow_mult [OF alpha_in_R, of "(1::nat)" i] and R.nat_pow_1 [OF alpha_in_R]
  have "\<alpha> (^)\<^bsub>R\<^esub> (Suc i) \<otimes>\<^bsub>R\<^esub> \<delta> = \<alpha> \<otimes>\<^bsub>R\<^esub> \<alpha> (^)\<^bsub>R\<^esub> i \<otimes>\<^bsub>R\<^esub> \<delta>" by simp
  also from hypo and R.m_assoc [OF alpha_in_R alpha_i_in_R [of i] pert_in_R] have "\<dots> = \<alpha> \<otimes>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i)" by simp
  also from sym [OF R.m_assoc [OF alpha_in_R pert_in_R beta_i_in_R [of i]]] and alpha_def and h_in_R pert_in_R beta_i_in_R [of i]
  have "\<dots> = \<delta> \<otimes>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i" by algebra
  also from R.m_assoc [OF pert_in_R _ beta_i_in_R [of i], of "\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>)"] pert_in_R h_in_R
  have "\<dots> = \<delta> \<otimes>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> i)" by simp
  also from beta_def and sym [OF R.nat_pow_1 [OF beta_in_R]] and R.nat_pow_mult [OF beta_in_R, of "(1::nat)" i]
  have "\<dots> = \<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> (Suc i)" by simp
  finally show "\<alpha> (^)\<^bsub>R\<^esub> Suc i \<otimes>\<^bsub>R\<^esub> \<delta> = \<delta> \<otimes>\<^bsub>R\<^esub> \<beta> (^)\<^bsub>R\<^esub> Suc i" by simp
qed

text{*Lemma 2.2.2 in Aransay's memoir*}

lemma (in local_nilpotent_alpha) lemma_2_2_2: shows "bound_phi (\<delta> x) \<le> bound_psi x"
proof -
  from alpha_delta_eq_delta_beta and ring_R have "(\<alpha> (^)\<^bsub>R\<^esub> bound_psi x) (\<delta> x) = (\<delta> ((\<beta> (^)\<^bsub>R\<^esub> bound_psi x) x))" by (auto simp add: expand_fun_eq)
  also have "\<dots> = \<delta> (\<one>)"
  proof (cases "x \<in> carrier D")
    case True with local_nilpotent_term.a_local_nilpot [OF local_nilpotent_term_beta] show ?thesis by simp
  next
    case False from beta_i_in_R [of "bound_psi x"] and ring_R and completion_closed2 [OF _ False, of "\<beta> (^)\<^bsub>R\<^esub> bound_psi x"  D]
    show ?thesis unfolding hom_completion_def by simp
  qed
  also from hom_completion_one [of D D \<delta>] pert_in_R ring_R and D_diff_group have "\<dots> = \<one>" 
    unfolding diff_group_def comm_group_def group_def by simp
  finally have alpha_x_pert_x_eq_one: "(\<alpha> (^)\<^bsub>R\<^esub> bound_psi x) (\<delta> x) = \<one>" by simp
  have alpha_pert_x_pert_x_eq_one: "(\<alpha> (^)\<^bsub>R\<^esub> bound_phi (\<delta> x)) (\<delta> x) = \<one>"
  proof (cases "\<delta> x \<in> carrier D")
    case True with local_nilpotent_term.a_local_nilpot [OF local_nilpotent_term_alpha] show ?thesis by simp
  next
    case False with ring_R and pert_in_R 
    show ?thesis unfolding hom_completion_def completion_fun2_def completion_def hom_def Pi_def by auto
  qed
  from alpha_x_pert_x_eq_one and alpha_pert_x_pert_x_eq_one 
    and local_nilpotent_term.bound_is_least [OF local_nilpotent_term_alpha, of "\<delta> x"] 
    and Least_le [of "\<lambda>i::nat. (\<alpha> (^)\<^bsub>R\<^esub> i) (\<delta> x) = \<one>" "bound_psi x"] show ?thesis by simp
qed

text{*Lemma 2.2.4 over endomorphisms applied to generic elements*}

lemma (in local_nilpotent_alpha) lemma_2_2_4_elements: shows "(\<delta> \<circ> \<Psi>) x = (\<Phi> \<circ> \<delta>) x"
proof -
  let ?max = "max (bound_psi x) (bound_phi x)"
  from ring_R have "(\<delta> \<circ> \<Psi>) x = \<delta> (\<Psi> x)" by simp
  also from psi_def have "\<dots> = \<delta> (local_nilpotent_term.power_series D R \<beta> bound_psi x)" by simp
  also from local_nilpotent_term.power_series_extended [OF local_nilpotent_term_beta, of x ?max]
    and le_maxI1 [of "bound_psi x" "bound_phi x"]
  have "\<dots> = \<delta> (\<Otimes>i\<in>{..?max}. (\<beta> (^)\<^bsub>R\<^esub> i) x)" by simp
  also from local_nilpotent_term.power_series_dist_l [OF local_nilpotent_term_beta pert_in_R, of x ?max] and pert_in_R
  have "\<dots> = (\<Otimes>i\<in>{..?max}. \<delta> ((\<beta> (^)\<^bsub>R\<^esub> i) x))" by simp
  also from alpha_delta_eq_delta_beta and ring_R have "\<dots> = (\<Otimes>i\<in>{..?max}. ((\<alpha> (^)\<^bsub>R\<^esub> i) (\<delta> x)))" by (auto simp add: expand_fun_eq)
  also from sym [OF local_nilpotent_term.power_series_extended [OF local_nilpotent_term_alpha, of "\<delta> x" ?max]] 
    and lemma_2_2_2 [of x] have "\<dots> = local_nilpotent_term.power_series D R \<alpha> bound_phi (\<delta> x)" by arith
  also from phi_def have "\<dots> = (\<Phi> \<circ> \<delta>) x" by simp
  finally show ?thesis by simp
qed

text{*Lemma 2.2.4 over endomorphisms*}

corollary (in local_nilpotent_alpha) lemma_2_2_4: shows "(\<delta> \<circ> \<Psi>) = (\<Phi> \<circ> \<delta>)" using lemma_2_2_4_elements by (simp add: expand_fun_eq)

text{*The following lemma is simple a renaming of the previous one; the idea is to give to the previous result 
  the name it had before as a premise, to keep the files correspoding to the equational part of the proof working*}

lemma (in local_nilpotent_alpha) delta_psi_phi_delta: shows "\<delta> \<otimes>\<^bsub>R\<^esub> \<Psi> = \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta>" using lemma_2_2_4 and ring_R by simp

text{*Lemma 2.2.5 over a generic element of the domain*}

lemma (in local_nilpotent_alpha) lemma_2_2_5_elements: shows "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<Psi>)) x" and "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta>)) x" 
  and "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)) x"
proof -
  from psi_def have "\<Psi> x = local_nilpotent_term.power_series D R \<beta> bound_psi x" by simp
  also from local_nilpotent_term.power_series_extended [OF local_nilpotent_term_beta, of x "Suc (bound_psi x)"]
  have "\<dots> = (\<Otimes>j\<in>{..Suc (bound_psi x)}. (\<beta> (^)\<^bsub>R\<^esub> j) x)" by simp
  also from local_nilpotent_term.power_series_first_element [OF local_nilpotent_term_beta, of x "Suc (bound_psi x)"]
  have "\<dots> = (\<beta> (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>j\<in>{1..Suc (bound_psi x)}. (\<beta> (^)\<^bsub>R\<^esub> j) x)" by simp
  also from  local_nilpotent_term.power_series_factor [OF local_nilpotent_term_beta, of x "bound_psi x"]
  have "\<dots> =  (\<beta> (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<beta> (\<Otimes>j\<in>{..bound_psi x}. (\<beta> (^)\<^bsub>R\<^esub> j) x))" by simp
  also from R.nat_pow_0 [of \<beta>] and beta_def and psi_def 
    and local_nilpotent_term.power_series_def [OF local_nilpotent_term_beta, of x] ring_R
  have "\<dots> = \<one>\<^bsub>R\<^esub> x \<otimes> (\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>) x" by simp
  also have "\<dots> = (\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>)) x"
  proof (cases "x \<in> carrier D") 
    case True with ring_R show ?thesis by simp 
  next
    case False 
    with ring_R have one_x: "\<one>\<^bsub>R\<^esub> x = \<one>" by simp
    moreover
    from h_in_R pert_in_R and psi_in_R have "(\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>) \<in> carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>)" D D x] have h_pert_psi: "(\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>) x = \<one>"
      by (unfold hom_completion_def, simp)
    moreover
    from h_in_R pert_in_R and psi_in_R have "\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>) \<in> carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>)" D D x]
    have one_h_pert_psi: "(\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta>) \<otimes>\<^bsub>R\<^esub> \<Psi>) x = \<one>" by simp
    ultimately show ?thesis by simp
  qed
  also from R.one_closed and pert_in_R and h_in_R and psi_in_R have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<Psi>)) x" by algebra
  finally show psi_eq: "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<Psi>)) x" by simp
  from lemma_2_2_4 and R.m_assoc [OF h_in_R pert_in_R psi_in_R] and sym [OF R.m_assoc [OF h_in_R phi_in_R pert_in_R]] and ring_R and psi_eq
  show psi_eq2: "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta>)) x" by simp
  with lemma_2_2_3 and ring_R show "\<Psi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)) x" by simp
qed

text{*Lemma 2.2.5 in generic terms*}

lemma (in local_nilpotent_alpha) lemma_2_2_5: shows "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<Psi>)" and "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta>)" 
  and "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)" using lemma_2_2_5_elements by (simp_all add: expand_fun_eq)

text{*The following lemma is simple a renaming of the previous one; the idea is to give to the previous result 
  the name it had before as a premise, to keep the proofs correspoding to the equational part of the proof working*}

lemma (in local_nilpotent_alpha) psi_prop: shows "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> \<Psi>)" and "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (h \<otimes>\<^bsub>R\<^esub> \<Phi> \<otimes>\<^bsub>R\<^esub> \<delta>)" 
  and "\<Psi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Psi> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<delta>)" using lemma_2_2_5 .

text{*Lemma 2.2.6 over a generic element of the domain*}

lemma (in local_nilpotent_alpha) lemma_2_2_6_elements: shows "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) x" and "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> \<Psi> \<otimes>\<^bsub>R\<^esub> h)) x" 
  and "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h)) x"
proof -
  from phi_def have "\<Phi> x = local_nilpotent_term.power_series D R \<alpha> bound_phi x" by simp
  also from local_nilpotent_term.power_series_extended [OF local_nilpotent_term_alpha, of x "Suc (bound_phi x)"]
  have "\<dots> = (\<Otimes>j\<in>{..Suc (bound_phi x)}. (\<alpha> (^)\<^bsub>R\<^esub> j) x)" by simp
  also from local_nilpotent_term.power_series_first_element [OF local_nilpotent_term_alpha, of x "Suc (bound_phi x)"]
  have "\<dots> = (\<alpha> (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<Otimes>j\<in>{1..Suc (bound_phi x)}. (\<alpha> (^)\<^bsub>R\<^esub> j) x)" by simp
  also from local_nilpotent_term.power_series_factor [OF local_nilpotent_term_alpha, of x "bound_phi x"]
  have "\<dots> =  (\<alpha> (^)\<^bsub>R\<^esub> (0::nat)) x \<otimes> (\<alpha> (\<Otimes>j\<in>{..bound_phi x}. (\<alpha>  (^)\<^bsub>R\<^esub> j) x))" by simp
  also from R.nat_pow_0 [of \<alpha>] and alpha_def and phi_def and local_nilpotent_term.power_series_def [OF local_nilpotent_term_alpha, of x] 
    ring_R
  have "\<dots> = \<one>\<^bsub>R\<^esub> x \<otimes> (\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>) x" by simp
  also have "\<dots> = (\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>)) x"
  proof (cases "x \<in> carrier D")
    case True with ring_R show ?thesis by simp 
  next
    case False
    with ring_R have one_x: "\<one>\<^bsub>R\<^esub> x = \<one>" by simp
    moreover
    from h_in_R pert_in_R and phi_in_R have "(\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>) \<in> carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>)" D D x] have h_pert_psi: "(\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>) x = \<one>"
      unfolding hom_completion_def by simp
    moreover
    from h_in_R pert_in_R and phi_in_R have "\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>) \<in> carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>)" D D x]
    have one_h_pert_psi: "(\<one>\<^bsub>R\<^esub> \<oplus>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h) \<otimes>\<^bsub>R\<^esub> \<Phi>) x = \<one>" by simp
    ultimately show ?thesis by simp
  qed
  also from R.one_closed and pert_in_R and h_in_R and phi_in_R have "\<dots> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) x" by algebra
  finally show phi_eq: "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)) x" by simp
  from lemma_2_2_3 and R.m_assoc [OF pert_in_R h_in_R phi_in_R] and sym [OF R.m_assoc [OF pert_in_R psi_in_R h_in_R]] and ring_R and phi_eq
  show phi_eq2: "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> \<Psi> \<otimes>\<^bsub>R\<^esub> h)) x" by simp
  with lemma_2_2_4 and ring_R show "\<Phi> x = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h)) x" by simp
qed

text{*Lemma 2.2.6*}

lemma (in local_nilpotent_alpha) lemma_2_2_6: shows "\<Phi> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>))" and "\<Phi> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> \<Psi> \<otimes>\<^bsub>R\<^esub> h))" 
  and "\<Phi> = (\<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h))" using lemma_2_2_6_elements by (simp_all add: expand_fun_eq)

text{*The following lemma is simple a renaming of the previous one; the idea is to give to the previous result 
  the name it had before as a premise, to keep the proofs correspoding to the equational part of the proof working*}

lemma (in local_nilpotent_alpha) phi_prop: shows "\<Phi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> h \<otimes>\<^bsub>R\<^esub> \<Phi>)" and "\<Phi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<delta> \<otimes>\<^bsub>R\<^esub> \<Psi> \<otimes>\<^bsub>R\<^esub> h)" 
  and "\<Phi> = \<one>\<^bsub>R\<^esub> \<ominus>\<^bsub>R\<^esub> (\<Phi> \<otimes>\<^bsub>R\<^esub> \<delta> \<otimes>\<^bsub>R\<^esub> h)" using lemma_2_2_6 .

end