Theory analytic_part_local

(*  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 ∈ carrier R"
  and a_local_nilpot: "∀x∈carrier D. (a (^)R (bound_funct x)) x = \<one>D"
  and bound_is_least: "bound_funct x =(LEAST n. (a (^)R (n::nat)) x = \<one>D)"

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>G"}, but nothing about @{term [locale=group] "(x::'a)(^)1"}*}

lemma (in monoid) nat_pow_1: assumes x: "x ∈ carrier G" shows "x (^)G (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(^)R(bound x)) x = \<one>D"}, 
  and @{term [locale=local_nilpotent_term] "bound_funct x ≤ m"}, then @{term [locale=local_nilpotent_term] "(a(^)R(m::nat)) x = \<one>D"}*}

lemma (in local_nilpotent_term) a_n_zero_a_m_zero: assumes bound_le_m: "bound_funct x ≤ m" 
  shows "(a(^)R(m)) x = \<one>D"
proof (cases "x ∈ carrier D")
  case True 
  then have x_in_D: "x ∈ carrier D" by simp
  show "(a (^)R m) x = \<one>"
    using a_local_nilpot and bound_le_m proof (induct m)
    case 0 assume bound_le_zero: "bound_funct x ≤ 0" and alpha_n: "∀x∈carrier D. (a (^)R bound_funct x) x = \<one>" with x_in_D
    show "(a (^)R (0::nat)) x = \<one>D" by auto
  next
    case (Suc m)
    assume hypo: "[|∀x∈carrier D. (a (^)R bound_funct x) x = \<one>; bound_funct x ≤ m|] ==> (a (^)R m) x = \<one>" 
      and a_bound_funct: "∀x∈carrier D. (a (^)R bound_funct x) x = \<one>" and bound_funct_le_Suc_m: "bound_funct x ≤ Suc m" 
    then show "(a (^)R 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 ≤ m " by arith
      with hypo and a_bound_funct have a_m: "(a (^)R m) x = \<one>" by simp
      have "(a (^)R Suc m) x  = (a ⊗R (a (^)R 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 "… = 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 "… = \<one>"
        unfolding diff_group_def comm_group_def group_def by simp
      finally show "(a (^)R 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 (^)R m " D D x] 
  show " (a (^)R 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] "(λi::nat. (a (^)R 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] "λi::nat. (a (^)R 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 (λi::nat. (a(^)R i) x) {..bound_funct x}"
end

text{*Some results about the power series*}

lemma (in local_nilpotent_term) power_pi: "(op (^)R a) ∈ {..(k::nat)} -> carrier R"
  using nat_pow_closed [OF a_in_R] and Pi_def [of "{..k}" "(λi::nat. carrier R)"] by simp

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

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

lemma (in local_nilpotent_term) finprod_eq_finsum_bound_funct:
  shows "finprod D (λi::nat. (a(^)R i) x) {..bound_funct x} = ((finsum R (λi::nat. (a(^)R i)) {..bound_funct x}) x)"
proof (induct "bound_funct x")
  case 0
  from nat_pow_0 [of a] and finsum_0 [of "op (^)R a"] and power_pi [of "0::nat"] and finprod_0 [of "(λi::nat. (a(^)R i) x)"]
    and power_pi_D [of x "0::nat"]
  show "(\<Otimes>i::nat∈{..0::nat}. (a (^)R i) x) = finsum R (op (^)R a) {..0::nat} x" by simp
next
  case (Suc n)
  assume hypo: "(\<Otimes>i∈{..n}. (a (^)R i) x) = finsum R (op (^)R a) {..n} x"
  show "(\<Otimes>i∈{..Suc n}. (a (^)R i) x) = finsum R (op (^)R a) {..Suc n} x"
  proof (cases "x ∈ carrier D")
    case True
    from finsum_Suc [OF power_pi, of n] have "finsum R (op (^)R a) {..Suc n} = a (^)R Suc n ⊕R finsum R (op (^)R a) {..n}" by simp
    with ring_R and True have "finsum R (op (^)R a) {..Suc n} x = (a (^)R Suc n) x ⊗D (finsum R (op (^)R a) {..n}) x" by simp
    moreover
    from True and finprod_Suc [OF power_pi_D, of x n] have "(\<Otimes>i∈{..Suc n}. (a (^)R i) x) = (a (^)R Suc n) x ⊗ (\<Otimes>i∈{..n}. (a (^)R i) x)"
      by simp
    with hypo have "(\<Otimes>i∈{..Suc n}. (a (^)R i) x) = (a (^)R Suc n) x ⊗ (finsum R (op (^)R 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 (^)R a) {..Suc n} ∈ carrier R" by simp
    with ring_R and completion_closed2 [of "finsum R (op (^)R a) {..Suc n}" D D] and False 
    have finsum_one: "finsum R (op (^)R a) {..Suc n} x = \<one>" unfolding hom_completion_def completion_fun2_def by simp
    moreover
    have "∀i∈{..Suc n}. (a (^)R i) x = \<one>"
    proof
      fix i assume i_in_nat: "i ∈ {..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 (^)R i) x = \<one>" 
        unfolding hom_completion_def completion_fun2_def by simp
    qed
    with finprod_cong [of "{..Suc n}" "{..Suc n}" "(λi. (a (^)R i) x)" "λx. \<one>"] and power_pi_D [of x "Suc n"]
    have "(\<Otimes>i∈{..Suc n}. (a (^)R i) x) = (\<Otimes>i∈{..Suc n}. \<one>)" by simp 
    with finprod_one [of "{..Suc n}"] and finite_nat_iff_bounded [of "{..Suc n}"] have finprod_one: "(\<Otimes>i∈{..Suc n}. (a (^)R i) x) = \<one>"
      by simp
    ultimately show ?thesis by simp
  qed
qed

lemma (in local_nilpotent_term) power_series_closed: shows "(\<Otimes>i∈{..m::nat}. (a (^)R i) x) ∈ carrier D"
proof (rule finprod_closed)
  from finite_nat_iff_bounded show "finite {..m}" by auto
  from power_pi_D [of x m] show "(λi::nat. (a (^)R i) x) ∈ {..m} -> 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∈{..bound_funct x}. (a (^)R i) x) ∈ 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}" "(λi::nat. carrier R)"]
  show "(λi::nat. (a (^)R i) x) ∈ {..bound_funct x} -> carrier D" by simp
qed

lemma (in local_nilpotent_term) power_series_extended: assumes bf_le_m: "bound_funct x ≤ m" 
  shows "power_series x = finprod D (λi::nat. (a (^)R 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∈{..(0::nat)}. (a (^)R i) x)" by simp
next
  case (Suc m)
  assume hypo: "bound_funct x ≤ m ==> power_series x = (\<Otimes>i∈{..m}. (a (^)R i) x)" and bf_le_Suc_m: "bound_funct x ≤ Suc m"
  show "power_series x = (\<Otimes>i∈{..Suc m}. (a (^)R 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∈{..m}. (a (^)R i) x)" by arith
    from a_n_zero_a_m_zero [OF bf_le_Suc_m] have a_Suc_m_one: "(a (^)R Suc m) x = \<one>".
    from power_pi_D [of x "Suc m"] and finprod_Suc [of "(λi::nat. (a (^)R i) x)" "m"]
    have "(\<Otimes>i∈{..Suc m}. (a (^)R i) x) = (a (^)R Suc m) x ⊗ (\<Otimes>i∈{..m}. (a (^)R i) x)" by simp
    also from a_Suc_m_one have "… = \<one> ⊗ (\<Otimes>i∈{..m}. (a (^)R i) x)" by simp
    also from hypo_m and D.l_one [OF power_series_closed [of x m]] have "… = 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 ∈ carrier R"
proof -
  have "power_series ∈ hom_completion D D"
  proof (unfold hom_completion_def hom_def Pi_def, auto)
    fix x
    assume x_in_D: "x ∈ carrier D"
    from power_series_closed [of x "bound_funct x"] and power_series_def [of x] show "power_series x ∈ carrier D" by simp
  next
    fix x y
    assume x_in_D: "x ∈ carrier D" and y_in_D: "y ∈ carrier D"
    show "power_series (x ⊗ y) = power_series x ⊗ power_series y"
    proof -
      let ?max = "max (bound_funct (x ⊗ y)) (max (bound_funct x) (bound_funct y))"
      from power_series_extended [of "x ⊗ y" ?max] have p_s_ex_xy: "power_series (x ⊗ y) = (\<Otimes>i∈{..?max}. (a (^)R i) (x ⊗ y))" by arith
      from power_series_extended [of x ?max] have p_s_ex_x: "power_series x = (\<Otimes>i∈{..?max}. (a (^)R i) x)" by arith
      from power_series_extended [of y ?max] have p_s_ex_y: "power_series y = (\<Otimes>i∈{..?max}. (a (^)R i) y)" by arith
      from p_s_ex_x and p_s_ex_y
      have "power_series x ⊗ power_series y = (\<Otimes>i∈{..?max}. (a (^)R i) x) ⊗ (\<Otimes>i∈{..?max}. (a (^)R i) y)" by simp
      also from sym [OF finprod_mult [of "(λi::nat. (a (^)R i) x)" ?max "(λi::nat. (a (^)R i) y)"]] 
        and power_pi_D [of x ?max] power_pi_D [of y ?max] and finite_nat_iff_bounded [of "{..?max}"]
      have "… = (\<Otimes>i∈{..?max}. (a (^)R i) x ⊗ (a (^)R 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 "… = (\<Otimes>i∈{..?max}. (a (^)R i) (x ⊗ y))" by simp
      also from sym [OF p_s_ex_xy] have "… = power_series (x ⊗ y)" by simp
      finally show ?thesis by simp
    qed
  next
    show "power_series ∈ 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 ∉ carrier D" 
      with nat_pow_closed [OF a_in_R] and completion_closed2 [of _ D D x] and ring_R have "(λi::nat. (a (^)R i) x) = (λ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 ∈ 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 ∈ carrier R" and b_in_R: "b ∈ carrier R" 
  shows "b ⊗ finsum R (op (^) a) {..(m::nat)} = (\<Oplus>i∈{..(m::nat)}. b ⊗ a (^) i)"
proof (induct m)
  case 0
  from finsum_0 [of "λi::nat. a(^)i"] and finsum_0 [of "λi::nat. b ⊗ a(^)i"] and b_in_R
  show " b ⊗ finsum R (op (^) a) {..(0::nat)} = (\<Oplus>i∈{..(0::nat)}. b ⊗ a (^) i)" by simp
next
  case (Suc m)
  assume hypo: "b ⊗ finsum R (op (^) a) {..m} = (\<Oplus>i∈{..m}. b ⊗ a (^) i)"
  show "b ⊗ finsum R (op (^) a) {..Suc m} = (\<Oplus>i∈{..Suc m}. b ⊗ a (^) i)"
  proof -
    from finsum_Suc [of "(op (^) a)" "m"] and Pi_def [of "{..Suc m}" "λi::nat. carrier R"] nat_pow_closed [OF a_in_R]
    have "b ⊗ (\<Oplus>i∈{..Suc m}. a (^) i) = b ⊗ (a(^)(Suc m) ⊕ (\<Oplus>i∈{..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}" "λi::nat. carrier R"] nat_pow_closed [OF a_in_R] and finite_nat_iff_bounded [of "{..m}"]
    have "… = b ⊗ a(^)(Suc m) ⊕ b ⊗ (\<Oplus>i∈{..m}. a (^) i)" by simp
    also from hypo have "… = b ⊗ a(^)(Suc m) ⊕ (\<Oplus>i∈{..m}. b ⊗ a (^) i)" by simp
    also from finsum_Suc [of "(λi::nat. b ⊗ a (^) i)", of m] and Pi_def [of "{..Suc m}" "λi::nat. carrier R"] 
      nat_pow_closed [OF a_in_R] and b_in_R
    have "… = (\<Oplus>i∈{..Suc m}. b ⊗ 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 ∈ carrier R" shows "(λi. b ((a (^)R i) x)) ∈ {..(k::nat)} -> 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 (^)R (m::nat)) x ∈ 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 ∈ carrier R"
  shows "b (\<Otimes>i∈{..(m::nat)}. (a (^)R i) x) = (\<Otimes>i∈{..(m::nat)}. (b ((a (^)R i) x)))"
proof (induct m)
  case 0
  from finprod_0 [of "(λi. (a (^)R i) x)"] and power_pi_D [of x "0::nat"] and finprod_0 [of "(λi. b ((a (^)R i) x))"] 
    and b_power_pi_D [OF b_in_R, of x "0::nat"] show "b (\<Otimes>i∈{..0::nat}. (a (^)R i) x) = (\<Otimes>i∈{..0::nat}. b ((a (^)R i) x))" by simp
next
  case (Suc m)
  assume hypo: "b (\<Otimes>i∈{..m}. (a (^)R i) x) = (\<Otimes>i∈{..m}. b ((a (^)R i) x))"
  show "b (\<Otimes>i∈{..Suc m}. (a (^)R i) x) = (\<Otimes>i∈{..Suc m}. b ((a (^)R i) x))"
  proof -
    from finprod_Suc [OF power_pi_D [of x], of m] have "b (\<Otimes>i∈{..Suc m}. (a (^)R i) x) = b ((a (^)R Suc m) x ⊗ (\<Otimes>i∈{..m}. (a (^)R i) x))"
      by simp
    also from b_in_R and ring_R and hom_completion_mult [of b D D "(a (^)R Suc m) x" " (\<Otimes>i∈{..m}. (a (^)R i) x)"] 
      and finprod_closed [of "{..m}" "(λi. (a (^)R i) x)"] power_pi_D [of x m] nat_pow_closed_D [of "Suc m" x]
    have "… =  b ((a (^)R Suc m) x) ⊗ b ((\<Otimes>i∈{..m}. (a (^)R i) x))" by simp
    also from hypo have "… = b ((a (^)R Suc m) x) ⊗ (\<Otimes>i∈{..m}. b ((a (^)R i) x))" by simp
    also from sym [OF finprod_Suc [OF b_power_pi_D [OF b_in_R, of x], of m]] have "… = (\<Otimes>i∈{..Suc m}. b ((a (^)R 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 ∈ carrier R" shows "(λi. (a (^)R i) (b x)) ∈ {..(k::nat)} -> 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 ∈ carrier R"
  shows "(λx. (\<Otimes>i∈{..m}. (a (^)R i) x)) (b x) = (\<Otimes>i∈{..(m::nat)}. ((a (^)R i) (b x)))" by simp

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

lemma (in comm_monoid) finprod_singleton [simp]:
  "f ∈ {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 (λi::nat. (a (^)R i) x) {..(i::nat)} = (a(^)R (0::nat)) x ⊗ finprod D (λi::nat. (a (^)R i) x) {1..(i::nat)}"
proof (induct i)
  case 0 
  from ring_R have one_x: "\<one>R x ∈ carrier D" unfolding hom_completion_def completion_fun2_def completion_def by auto
  from finprod_0 [of "(λi. (a (^)R i) x)"] and power_pi_D [of x 0] and  D.r_one [OF one_x]
  show "(\<Otimes>i∈{..(0::nat)}. (a (^)R i) x) = (a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{(1::nat)..0}. (a (^)R i) x)" by simp
next
  case (Suc i)
  assume hypo: "(\<Otimes>i∈{..i}. (a (^)R i) x) = (a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x)"
  show "(\<Otimes>i∈{..Suc i}. (a (^)R i) x) = (a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{1..Suc i}. (a (^)R i) x)"
  proof -
    from finprod_Suc [of "(λi::nat. (a (^)R i) x)" i] and power_pi_D [of x "Suc i"]
    have "(\<Otimes>i∈{..Suc i}. (a (^)R i) x) = (a (^)R Suc i) x ⊗ (\<Otimes>i∈{..i}. (a (^)R i) x)" by simp
    also from hypo have "… = (a (^)R Suc i) x ⊗ ((a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x))" by simp
    also have "… =  ((a (^)R Suc i) x ⊗ (a (^)R (0::nat)) x) ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x)"
    proof (rule sym [OF D.m_assoc [of "(a (^)R Suc i) x" "(a (^)R (0::nat)) x" "(\<Otimes>i∈{1..i}. (a (^)R i) x)"]])
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)R Suc i) x ∈ carrier D" by simp
      from  nat_pow_closed_D [of "0::nat" x] show "(a (^)R (0::nat)) x ∈ carrier D" by simp
      from finprod_closed [of "{1..i}" "(λi::nat. (a(^)Ri) x)"] and finite_nat_iff_bounded [of "{1..i}"] 
        and nat_pow_closed_D [of _ x] and Pi_def [of "{1..i}" "λi::nat. carrier D"] 
      show "(\<Otimes>i∈{1..i}. (a (^)R i) x) ∈ 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 "… = ((a (^)R (0::nat)) x ⊗ (a (^)R Suc i) x) ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x)" by simp
    also have "… = (a (^)R (0::nat)) x ⊗ ((a (^)R Suc i) x ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x))"
    proof (rule D.m_assoc [of "(a (^)R (0::nat)) x" "(a (^)R (Suc i)) x" "(\<Otimes>i∈{1..i}. (a (^)R i) x)"])
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)R Suc i) x ∈ carrier D" by simp
      from  nat_pow_closed_D [of "0::nat" x] show "(a (^)R (0::nat)) x ∈ carrier D" by simp
      from finprod_closed [of "{1..i}" "(λi::nat. (a(^)Ri) x)"] and finite_nat_iff_bounded [of "{1..i}"] 
        and nat_pow_closed_D [of _ x] and Pi_def [of "{1..i}" "λi::nat. carrier D"] 
      show "(\<Otimes>i∈{1..i}. (a (^)R i) x) ∈ carrier D" by simp
    qed
    also from nat_pow_closed_D [of "Suc i" x] 
    have "… = (a (^)R (0::nat)) x ⊗ ((\<Otimes>i∈{Suc i}. (a (^)R i) x) ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x))" by simp
    also from sym [OF finprod_Un_disjoint [of "{Suc i}" "{1..i}" "(λi::nat. (a (^)R i) x)"]]
      and finite_nat_iff_bounded [of "{1..i}"] finite_nat_iff_bounded [of "{Suc i}"] and Pi_def [of "{(1::nat)..i}" "(λi::nat. carrier D)"]
      Pi_def [of "{Suc i}" "(λi::nat. carrier D)"] and nat_pow_closed_D [of "Suc i" x] nat_pow_closed_D [of _ x]
    have "(a (^)R (0::nat)) x ⊗ ((\<Otimes>i∈{Suc i}. (a (^)R i) x) ⊗ (\<Otimes>i∈{1..i}. (a (^)R i) x)) 
      = (a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{1..i} ∪ {Suc i}. (a (^)R i) x)" by simp
    also have "… = (a (^)R (0::nat)) x ⊗ (\<Otimes>i∈{1..Suc i}. (a (^)R i) x)"
    proof -
      have "{1..i} ∪ {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∈{(1::nat)..Suc i}. (a (^)R j) x) = a (\<Otimes>j∈{..i}. (a (^)R j) x)"
proof (induct i)
  case 0
  have "a x = a (\<one>R x)"
  proof (cases "x ∈ carrier D")
    case True with ring_R show "a x = a (\<one>R 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>R x)" unfolding diff_group_def comm_group_def group_def hom_completion_def completion_fun2_def by simp
  qed
  with finprod_0 [of "(λj::nat. (a (^)R j) x)"] finprod_insert [of "{}" "Suc 0" "(λj::nat. (a (^)R 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 "(λj::nat. (a (^)R j) x)" "Suc 0"]
  show "(\<Otimes>j∈{1..Suc 0}. (a (^)R j) x) = a (\<Otimes>j∈{..0::nat}. (a (^)R j) x)" by simp
next
  case (Suc i)
  assume hypo: "(\<Otimes>j∈{1..Suc i}. (a (^)R j) x) = a (\<Otimes>j∈{..i}. (a (^)R j) x)"
  show "(\<Otimes>j∈{1..Suc (Suc i)}. (a (^)R j) x) = a (\<Otimes>j∈{..Suc i}. (a (^)R j) x)"
  proof -
    have "(\<Otimes>j∈{1..Suc (Suc i)}. (a (^)R j) x) = (\<Otimes>j∈{1..Suc i} ∪ {Suc (Suc i)}. (a (^)R j) x)"
    proof -
      have "{1..Suc i} ∪ {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)}" "(λj::nat. (a (^)R 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}" "(λj::nat. carrier D)"]
      Pi_def [of "{Suc (Suc i)}" "(λj::nat. carrier D)"] and nat_pow_closed_D [of "Suc (Suc i)" x] nat_pow_closed_D [of _ x]
    have "… = (\<Otimes>j∈{1..Suc i}. (a (^)R j) x) ⊗ (\<Otimes>j∈{Suc (Suc i)}. (a (^)R j) x)" by simp
    also from hypo and finprod_singleton [of "(λj::nat. (a (^)R j) x)" "Suc (Suc i)"] and nat_pow_closed_D [of "Suc (Suc i)" x]
    have "… = a (\<Otimes>j∈{..i}. (a (^)R j) x) ⊗ ((a (^)R Suc (Suc i)) x)" by simp
    also from ring_R have "… = a (\<Otimes>j∈{..i}. (a (^)R j) x) ⊗ a ((a (^)R 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 (^)R Suc (Suc i) = a ⊗R (a (^)R Suc i)" by simp
      with ring_R have "((a (^)R Suc (Suc i)) x) = a ((a (^)R Suc i) x)" by simp
      then show ?thesis by simp
    qed
    also have "… = a ((\<Otimes>j∈{..i}. (a (^)R j) x) ⊗ (a (^)R Suc i) x)"
    proof (intro sym [OF hom_completion_mult [of a D D "\<Otimes>j∈{..i}. (a (^)R j) x" "(a (^)R Suc i) x"]])
      from ring_R and a_in_R show "a ∈ hom_completion D D" by simp
      from finprod_closed [of "{..i}" "(λj::nat. (a (^)R j) x)"] and power_pi_D [of x i]
      show "(\<Otimes>j∈{..i}. (a (^)R j) x) ∈ carrier D" by simp
      from nat_pow_closed_D [of "Suc i" x] show "(a (^)R Suc i) x ∈ carrier D" by simp
    qed
    also from nat_pow_closed_D [of "Suc i" x] have "… = a ((\<Otimes>j∈{..i}. (a (^)R j) x) ⊗ (\<Otimes>j∈{Suc i}.(a (^)R Suc i) x))"
      by simp
    also from sym [OF finprod_Un_disjoint [of "{..i}" "{Suc i}" "(λj::nat. (a (^)R j) x)"]]
      and finite_nat_iff_bounded [of "{..i}"] finite_nat_iff_bounded [of "{Suc i}"] and Pi_def [of "{..i}" "(λj::nat. carrier D)"]
      Pi_def [of "{Suc i}" "(λj::nat. carrier D)"] and nat_pow_closed_D [of "Suc i" x] nat_pow_closed_D [of _ x]
    have "… = a (\<Otimes>j∈{..i} ∪ {Suc i}. (a (^)R j) x)" by simp
    also have "… = a (\<Otimes>j∈{..Suc i}. (a (^)R j) x)"
    proof -
      have "{..i} ∪ {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 "α"}, 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 == {δ. δ ∈ hom_completion D D & 
  diff_group (| carrier = carrier D, mult = mult D, one = one D, diff = (λx. if x ∈ carrier D then ((differ) x) ⊗ (δ x) else \<one>)|)), }"

locale diff_group_pert = diff_group D + var δ +
  assumes delta_pert: "δ ∈ pert D"

lemma (in diff_group_pert) diff_group_pert_is_diff_group: 
  shows "diff_group (|carrier = carrier D, mult = mult D, one = one D, diff = (λx. if x ∈ carrier D then ((differD) x) ⊗D (δ x) else \<one>D)|)),"
  using diff_group_pert.delta_pert [of D δ] and prems unfolding diff_group_pert_def pert_def by simp

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

lemma (in ring_endomorphisms) diff_group_pert_is_diff_group: assumes delta: "δ ∈ pert D"
  shows "diff_group (| carrier = carrier D, mult = mult D, one = one D, diff = (differD) ⊕R δ |)),"
  using diff_group_pert.diff_group_pert_is_diff_group [of D δ] 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: "δ ∈ pert D" shows "δ ∈ carrier R"
  using ring_R and diff_group_pert.pert_is_hom [of D δ] 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: "δ ∈ pert D" shows "(differD) ⊕R δ ∈ carrier R" 
  using delta by simp

text{*The reason to introduce @{term α} 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 α bound_phi"} in the definition of locale @{text "local_nilpotent_alpha"}*}

locale alpha_beta = ring_endomorphisms + reduction + var δ + var α +
  assumes delta_pert: "δ ∈ pert D"
  defines alpha_def: "α == \<ominus>R (δ ⊗R h)"

  (*definition (in alpha_beta)
  alpha_def: "α = \<ominus>R (δ ⊗R h)"
  *)

context alpha_beta
begin

definition beta_def: "β = \<ominus>R (h ⊗R δ)"

end

locale local_nilpotent_alpha = alpha_beta + local_nilpotent_term D R α bound_phi

text{*The definition of @{term Φ} 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: "Φ == local_nilpotent_term.power_series D R α bound_phi"

end

lemma (in alpha_beta) pert_in_R [simp]: shows "δ ∈ carrier R"
  using delta_pert and ring_R by (unfold pert_def, simp)

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

lemma (in alpha_beta) alpha_in_R: shows "α ∈ carrier R"
  using alpha_def and pert_in_R and h_in_R by simp

lemma (in alpha_beta) beta_in_R: shows "β ∈ carrier R"
  using beta_def and pert_in_R and h_in_R by simp

lemma (in alpha_beta) alpha_i_in_R: shows "α(^)R (i::nat) ∈ carrier R"
  using alpha_in_R and R.nat_pow_closed by simp

lemma (in alpha_beta) beta_i_in_R: shows "β(^)R (i::nat) ∈ carrier R"
  using beta_in_R and nat_pow_closed by simp

lemma (in ring) power_minus_a_b: 
  assumes a: "a ∈ carrier R" and b: "b ∈ carrier R" shows "(\<ominus> (a ⊗ b)) (^) Suc n = \<ominus> a ⊗ ((\<ominus> (b ⊗ a)) (^) n) ⊗ b"
proof (induct n)
  case 0
  from a and b and nat_pow_0 [of "a ⊗ b"] show "\<ominus> (a ⊗ b) (^) Suc 0 = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) (0::nat) ⊗ b" by simp algebra
next
  case (Suc n)
  assume hypo: "(\<ominus> (a ⊗ b)) (^) Suc n = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) n ⊗ b"
  have "(\<ominus> (a ⊗ b)) (^) Suc (Suc n) = \<ominus> (a ⊗ b) (^) (Suc n) ⊗ \<ominus> (a ⊗ b)" by simp
  also from hypo have "… = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) n ⊗ b ⊗ \<ominus> (a ⊗ b)" by simp
  also from sym [OF l_minus [OF a b]] have "… = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) n ⊗ b ⊗ (\<ominus> a ⊗ 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 ⊗ a)" n] 
    and a_inv_closed [of "b ⊗ a"] and a b r_minus [OF b a]
  have "… = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) n ⊗ (\<ominus> (b ⊗ a) ⊗ b)" by algebra
  also from nat_pow_closed [of "\<ominus> (b ⊗ a)" n] and a_inv_closed [of "b ⊗ a"] and a b 
    and sym [OF m_assoc[of "(\<ominus> (b ⊗ a)) (^) n" "(\<ominus> (b ⊗ a))" b]]
  have "… = \<ominus> a ⊗ (\<ominus> (b ⊗ a) (^) n ⊗ (\<ominus> (b ⊗ a))) ⊗ b" by algebra
  also from sym [OF nat_pow_Suc [of "\<ominus> (b ⊗ a)" n]]
  have "… = \<ominus> a ⊗ (\<ominus> (b ⊗ a)) (^) (Suc n) ⊗ b" by simp 
  finally show "\<ominus> (a ⊗ b) (^) Suc (Suc n) = \<ominus> a ⊗ \<ominus> (b ⊗ a) (^) Suc n ⊗ 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] β}. The first one would be to 
  give its long name @{text "local_nilpotent_alpha.β δ"}, 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) β == alpha_beta.β R h δ"}*}

text{*The following lemma proves that whenever @{term [locale=local_nilpotent_alpha] "α"} is a local nilpotent term,
  so will be @{term [locale=local_nilpotent_alpha] "β"}*}

lemma (in local_nilpotent_alpha) nilp_alpha_nilp_beta: shows "local_nilpotent_term D R β (λx. (LEAST n::nat. (β (^)R n) x = \<one>D))"
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 "β ∈ carrier R" by simp
  show "∀x∈carrier D. (β (^)R (LEAST n::nat. (β (^)R n) x = \<one>)) x = \<one>"
  proof (intro ballI)
    fix x assume x_in_D: "x ∈ carrier D"
    show "(β (^)R (LEAST n::nat. (β (^)R n) x = \<one>)) x = \<one>"
    proof (rule LeastI_ex [of "λn::nat. (β (^)R n) x = \<one>"])
      from a_local_nilpot and pert_in_R and ring_R and hom_completion_closed [OF _ x_in_D, of δ D]
      have alpha_nilpot: "(α (^)R bound_phi (δ x)) (δ x) = \<one>" by simp
      from beta_def have "(β (^)R (Suc (bound_phi (δ x)))) x = ((\<ominus>R (h ⊗R δ)) (^)R (Suc (bound_phi (δ 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 (δ x)"]
      have "… = (\<ominus>R h ⊗R (\<ominus>R (δ ⊗R h) (^)R (bound_phi (δ x))) ⊗R δ) x" by simp
      also from alpha_nilpot and alpha_def and ring_R have "… = (\<ominus>R h) \<one>" by simp
      also from a_inv_closed [OF h_in_R] and ring_R and hom_completion_one [of D D "\<ominus>R h"] and D_diff_group
      have "… = \<one>" by (unfold diff_group_def comm_group_def group_def, simp)
      finally have beta_nil: "(β (^)R (Suc (bound_phi (δ x)))) x = \<one>" by simp
      from exI [of "λn::nat. (β (^)R n) x = \<one>" "(Suc (bound_phi (δ x)))"] and beta_nil
      show "∃n::nat. (β (^)R n) x = \<one>" by simp 
    qed
  qed
qed

lemma (in local_nilpotent_alpha) bound_psi_exists: shows "∃bound_psi. local_nilpotent_term D R β bound_psi"
  using nilp_alpha_nilp_beta by iprover

context local_nilpotent_alpha
begin

definition "bound_psi ≡ (λx. (LEAST n::nat. (β (^)R n) x = \<one>D))"

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

definition psi_def: "Ψ ≡ local_nilpotent_term.power_series D R β bound_psi"

end

subsection{*Some properties of the endomorphisms @{term "Φ"}, @{term "Ψ"}, @{term "α"} and @{term "β"}*}

lemma (in local_nilpotent_alpha) local_nilpotent_term_alpha: shows "local_nilpotent_term D R α 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 β 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 "Φ x ∈ 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}" "(λi::nat. (α(^)Ri) 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 "Φ ∈ 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 "Φ ∈ hom_completion D D"
  using phi_in_R and ring_R by simp
  
lemma (in local_nilpotent_alpha) psi_in_R [simp]: shows "Ψ ∈ 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 "Ψ ∈ hom_completion D D"
  using psi_in_R and ring_R by simp

lemma (in local_nilpotent_alpha) psi_x_in_D [simp]: shows "Ψ x ∈ 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}" "(λi::nat. (α(^)Ri) 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 ⊗R α(^)R(i::nat) = β (^)R i ⊗R h"
proof (induct i)
  case 0
  from h_in_R and R.nat_pow_0 show "h ⊗R α (^)R (0::nat) = β (^)R (0::nat) ⊗R h" by simp
next
  case (Suc i)
  assume hypo: "h ⊗R α (^)R i = β (^)R i ⊗R h"
  from R.nat_pow_mult [OF beta_in_R, of "(1::nat)" i] and R.nat_pow_1 [OF beta_in_R]
  have "β (^)R (Suc i) ⊗R h = β ⊗R β (^)R i ⊗R h" by simp
  also from hypo and R.m_assoc [OF beta_in_R beta_i_in_R [of i] h_in_R] have "… = β ⊗R (h ⊗R α (^)R 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 "… = h ⊗R \<ominus>R (δ ⊗R h) ⊗R α (^)R i" by algebra
  also from R.m_assoc [OF h_in_R _ alpha_i_in_R [of i], of "\<ominus>R (δ ⊗R h)"] pert_in_R h_in_R
  have "… = h ⊗R (\<ominus>R (δ ⊗R h) ⊗R α (^)R 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 "… = h ⊗R α (^)R (Suc i)" by simp
  finally show "h ⊗R α (^)R Suc i = β (^)R Suc i ⊗R 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) ≤ bound_phi x"
proof -
  from h_alpha_eq_beta_h and ring_R have "(β (^)R bound_phi x) (h x) = (h ((α (^)R bound_phi x) x))" by (auto simp add: expand_fun_eq)
  also have "… = h (\<one>)"
  proof (cases "x ∈ 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 "α (^)R 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 "… = \<one>" unfolding diff_group_def comm_group_def group_def by simp
  finally have beta_x_h_x_eq_one: "(β (^)R bound_phi x) (h x) = \<one>" by simp
  have beta_h_x_h_x_eq_one: "(β (^)R bound_psi (h x)) (h x) = \<one>"
  proof (cases "h x ∈ 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 "λi::nat. (β (^)R 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 o Φ) x = (Ψ o h) x"
proof -
  let ?max = "max (bound_phi x) (bound_psi x)"
  from ring_R have "(h o Φ) x = h (Φ x)" by simp
  also from phi_def have "… = h (local_nilpotent_term.power_series D R α 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 "… = h (\<Otimes>i∈{..?max}. (α (^)R 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 "… = (\<Otimes>i∈{..?max}. h ((α (^)R i) x))" by simp
  also from h_alpha_eq_beta_h and ring_R have "… = (\<Otimes>i∈{..?max}. ((β (^)R 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 "… = local_nilpotent_term.power_series D R β bound_psi (h x)" by arith
  also from psi_def have "… = Ψ (h x)" by simp
  also have "… = (Ψ o 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 o Φ) = (Ψ o 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 "Ψ ⊗R h = h ⊗R Φ" using lemma_2_2_3 and ring_R by simp

lemma (in local_nilpotent_alpha) alpha_delta_eq_delta_beta: shows "α(^)R(i::nat) ⊗R δ = δ ⊗R β (^)R i"
proof (induct i)
  case 0
  from pert_in_R and R.nat_pow_0 show "α (^)R (0::nat) ⊗R δ = δ ⊗R β (^)R (0::nat)" by simp
next
  case (Suc i)
  assume hypo: "α (^)R i ⊗R δ = δ ⊗R β (^)R i"
  from R.nat_pow_mult [OF alpha_in_R, of "(1::nat)" i] and R.nat_pow_1 [OF alpha_in_R]
  have "α (^)R (Suc i) ⊗R δ = α ⊗R α (^)R i ⊗R δ" by simp
  also from hypo and R.m_assoc [OF alpha_in_R alpha_i_in_R [of i] pert_in_R] have "… = α ⊗R (δ ⊗R β (^)R 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 "… = δ ⊗R \<ominus>R (h ⊗R δ) ⊗R β (^)R i" by algebra
  also from R.m_assoc [OF pert_in_R _ beta_i_in_R [of i], of "\<ominus>R (h ⊗R δ)"] pert_in_R h_in_R
  have "… = δ ⊗R (\<ominus>R (h ⊗R δ) ⊗R β (^)R 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 "… = δ ⊗R β (^)R (Suc i)" by simp
  finally show "α (^)R Suc i ⊗R δ = δ ⊗R β (^)R 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 (δ x) ≤ bound_psi x"
proof -
  from alpha_delta_eq_delta_beta and ring_R have "(α (^)R bound_psi x) (δ x) = (δ ((β (^)R bound_psi x) x))" by (auto simp add: expand_fun_eq)
  also have "… = δ (\<one>)"
  proof (cases "x ∈ 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 "β (^)R bound_psi x"  D]
    show ?thesis unfolding hom_completion_def by simp
  qed
  also from hom_completion_one [of D D δ] pert_in_R ring_R and D_diff_group have "… = \<one>" 
    unfolding diff_group_def comm_group_def group_def by simp
  finally have alpha_x_pert_x_eq_one: "(α (^)R bound_psi x) (δ x) = \<one>" by simp
  have alpha_pert_x_pert_x_eq_one: "(α (^)R bound_phi (δ x)) (δ x) = \<one>"
  proof (cases "δ x ∈ 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 "δ x"] 
    and Least_le [of "λi::nat. (α (^)R i) (δ 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 "(δ o Ψ) x = (Φ o δ) x"
proof -
  let ?max = "max (bound_psi x) (bound_phi x)"
  from ring_R have "(δ o Ψ) x = δ (Ψ x)" by simp
  also from psi_def have "… = δ (local_nilpotent_term.power_series D R β 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 "… = δ (\<Otimes>i∈{..?max}. (β (^)R 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 "… = (\<Otimes>i∈{..?max}. δ ((β (^)R i) x))" by simp
  also from alpha_delta_eq_delta_beta and ring_R have "… = (\<Otimes>i∈{..?max}. ((α (^)R i) (δ x)))" by (auto simp add: expand_fun_eq)
  also from sym [OF local_nilpotent_term.power_series_extended [OF local_nilpotent_term_alpha, of "δ x" ?max]] 
    and lemma_2_2_2 [of x] have "… = local_nilpotent_term.power_series D R α bound_phi (δ x)" by arith
  also from phi_def have "… = (Φ o δ) 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 "(δ o Ψ) = (Φ o δ)" 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 "δ ⊗R Ψ = Φ ⊗R δ" 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 "Ψ x = (\<one>R \<ominus>R (h ⊗R δ ⊗R Ψ)) x" and "Ψ x = (\<one>R \<ominus>R (h ⊗R Φ ⊗R δ)) x" 
  and "Ψ x = (\<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)) x"
proof -
  from psi_def have "Ψ x = local_nilpotent_term.power_series D R β 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 "… = (\<Otimes>j∈{..Suc (bound_psi x)}. (β (^)R 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 "… = (β (^)R (0::nat)) x ⊗ (\<Otimes>j∈{1..Suc (bound_psi x)}. (β (^)R j) x)" by simp
  also from  local_nilpotent_term.power_series_factor [OF local_nilpotent_term_beta, of x "bound_psi x"]
  have "… =  (β (^)R (0::nat)) x ⊗ (β (\<Otimes>j∈{..bound_psi x}. (β (^)R j) x))" by simp
  also from R.nat_pow_0 [of β] and beta_def and psi_def 
    and local_nilpotent_term.power_series_def [OF local_nilpotent_term_beta, of x] ring_R
  have "… = \<one>R x ⊗ (\<ominus>R (h ⊗R δ) ⊗R Ψ) x" by simp
  also have "… = (\<one>R ⊕R (\<ominus>R (h ⊗R δ) ⊗R Ψ)) x"
  proof (cases "x ∈ carrier D") 
    case True with ring_R show ?thesis by simp 
  next
    case False 
    with ring_R have one_x: "\<one>R x = \<one>" by simp
    moreover
    from h_in_R pert_in_R and psi_in_R have "(\<ominus>R (h ⊗R δ) ⊗R Ψ) ∈ carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>R (h ⊗R δ) ⊗R Ψ)" D D x] have h_pert_psi: "(\<ominus>R (h ⊗R δ) ⊗R Ψ) x = \<one>"
      by (unfold hom_completion_def, simp)
    moreover
    from h_in_R pert_in_R and psi_in_R have "\<one>R ⊕R (\<ominus>R (h ⊗R δ) ⊗R Ψ) ∈ carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>R (h ⊗R δ) ⊗R Ψ)" D D x]
    have one_h_pert_psi: "(\<one>R ⊕R \<ominus>R (h ⊗R δ) ⊗R Ψ) 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 "… = (\<one>R \<ominus>R (h ⊗R δ ⊗R Ψ)) x" by algebra
  finally show psi_eq: "Ψ x = (\<one>R \<ominus>R (h ⊗R δ ⊗R Ψ)) 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: "Ψ x = (\<one>R \<ominus>R (h ⊗R Φ ⊗R δ)) x" by simp
  with lemma_2_2_3 and ring_R show "Ψ x = (\<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)) x" by simp
qed

text{*Lemma 2.2.5 in generic terms*}

lemma (in local_nilpotent_alpha) lemma_2_2_5: shows "Ψ = \<one>R \<ominus>R (h ⊗R δ ⊗R Ψ)" and "Ψ = \<one>R \<ominus>R (h ⊗R Φ ⊗R δ)" 
  and "Ψ = \<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)" 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 "Ψ = \<one>R \<ominus>R (h ⊗R δ ⊗R Ψ)" and "Ψ = \<one>R \<ominus>R (h ⊗R Φ ⊗R δ)" 
  and "Ψ = \<one>R \<ominus>R (Ψ ⊗R h ⊗R δ)" 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 "Φ x = (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ)) x" and "Φ x = (\<one>R \<ominus>R (δ ⊗R Ψ ⊗R h)) x" 
  and "Φ x = (\<one>R \<ominus>R (Φ ⊗R δ ⊗R h)) x"
proof -
  from phi_def have "Φ x = local_nilpotent_term.power_series D R α 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 "… = (\<Otimes>j∈{..Suc (bound_phi x)}. (α (^)R 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 "… = (α (^)R (0::nat)) x ⊗ (\<Otimes>j∈{1..Suc (bound_phi x)}. (α (^)R j) x)" by simp
  also from local_nilpotent_term.power_series_factor [OF local_nilpotent_term_alpha, of x "bound_phi x"]
  have "… =  (α (^)R (0::nat)) x ⊗ (α (\<Otimes>j∈{..bound_phi x}. (α  (^)R j) x))" by simp
  also from R.nat_pow_0 [of α] and alpha_def and phi_def and local_nilpotent_term.power_series_def [OF local_nilpotent_term_alpha, of x] 
    ring_R
  have "… = \<one>R x ⊗ (\<ominus>R (δ ⊗R h) ⊗R Φ) x" by simp
  also have "… = (\<one>R ⊕R (\<ominus>R (δ ⊗R h) ⊗R Φ)) x"
  proof (cases "x ∈ carrier D")
    case True with ring_R show ?thesis by simp 
  next
    case False
    with ring_R have one_x: "\<one>R x = \<one>" by simp
    moreover
    from h_in_R pert_in_R and phi_in_R have "(\<ominus>R (δ ⊗R h) ⊗R Φ) ∈ carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>R (δ ⊗R h) ⊗R Φ)" D D x] have h_pert_psi: "(\<ominus>R (δ ⊗R h) ⊗R Φ) x = \<one>"
      unfolding hom_completion_def by simp
    moreover
    from h_in_R pert_in_R and phi_in_R have "\<one>R ⊕R (\<ominus>R (δ ⊗R h) ⊗R Φ) ∈ carrier R" by simp
    with False and ring_R and completion_closed2 [of "(\<ominus>R (δ ⊗R h) ⊗R Φ)" D D x]
    have one_h_pert_psi: "(\<one>R ⊕R \<ominus>R (δ ⊗R h) ⊗R Φ) 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 "… = (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ)) x" by algebra
  finally show phi_eq: "Φ x = (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ)) 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: "Φ x = (\<one>R \<ominus>R (δ ⊗R Ψ ⊗R h)) x" by simp
  with lemma_2_2_4 and ring_R show "Φ x = (\<one>R \<ominus>R (Φ ⊗R δ ⊗R h)) x" by simp
qed

text{*Lemma 2.2.6*}

lemma (in local_nilpotent_alpha) lemma_2_2_6: shows "Φ = (\<one>R \<ominus>R (δ ⊗R h ⊗R Φ))" and "Φ = (\<one>R \<ominus>R (δ ⊗R Ψ ⊗R h))" 
  and "Φ = (\<one>R \<ominus>R (Φ ⊗R δ ⊗R 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 "Φ = \<one>R \<ominus>R (δ ⊗R h ⊗R Φ)" and "Φ = \<one>R \<ominus>R (δ ⊗R Ψ ⊗R h)" 
  and "Φ = \<one>R \<ominus>R (Φ ⊗R δ ⊗R h)" using lemma_2_2_6 .

end