Theory lemma_2_2_15_local_nilpot

(*  Title:      bpl/lemma_2_2_15_local_nilpot.thy
    ID:         $Id: lemma_2_2_15_local_nilpot.thy $
    Author:     Jesus Aransay
    Comments:   The set of lemmas proving the equational part of the BPL
*)

header{*Lemma 2.2.15 in Aransay's memoir*}

theory lemma_2_2_15_local_nilpot imports analytic_part_local
  begin

text{*We define a locale setting merging the specifications introduced for @{text "lemma 2.2.14"} and also the one created for the
  @{text "local nilpotent term alpha"}*}
text{*A few definitions are also provided in this locale setting*}

locale lemma_2_2_15 = lemma_2_2_14 D R h + local_nilpotent_alpha D R C f g h δ α bound_phi

definition (in lemma_2_2_15)
  h' where "h' == h ⊗R Φ"
definition (in lemma_2_2_15)
  p' where "p' == ((differD) ⊕R δ) ⊗R h' ⊕R h' ⊗R ((differD) ⊕R δ)"
definition (in lemma_2_2_15)
  diff' where "diff' == differ ⊕R δ"
definition (in lemma_2_2_15)
  D' where "D' == (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),"
definition (in lemma_2_2_15)
  ker_p' where "ker_p' == kernel (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), p'"
definition (in lemma_2_2_15)
  diff_group_ker_p' where "diff_group_ker_p' == (|carrier = kernel (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), p', mult = mult D,
  one = one D, diff = completion ((|carrier = kernel (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), p', mult = mult D, one = one D, diff = differ ⊕R δ|)),)
  (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), (differ ⊕R δ) |)),"
definition (in lemma_2_2_15)
  inc_ker_p' where "inc_ker_p' == (λx. if x ∈ kernel (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (| carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),  p' then x else \<one>D')"

lemma (in lemma_2_2_15) h'_in_R [simp]: shows "h' ∈ carrier R"
  using h'_def by simp

lemma (in lemma_2_2_15) pert_in_R [simp]: shows "δ ∈ carrier R"
  using delta_pert and pert_def [of D] by simp

lemma (in lemma_2_2_15) p'_in_R [simp]: shows "p' ∈ carrier R"
  using p'_def and diff_pert_in_R [OF delta_pert] and h'_in_R by simp

lemma (in lemma_2_2_15) diff'_in_R [simp]: shows "diff' ∈ carrier R"
  using diff'_def diff_in_R pert_in_R by simp

text{*The endomorphisms (not the differential endomorphisms) over a differential group happen to be the same ones as
  the homomorphisms over a perturbed version of this differential group*}
text{*In other words, the definition of homomorphism over a differential group is independient of the differential*}
text{*In the case of differential homomorphisms, this is not always true*}

lemma (in ring_endomorphisms) hom_completion_eq: assumes "δ ∈ pert D"
  shows "hom_completion (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),
  (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), = hom_completion D D"
  using ring_R by (unfold hom_completion_def completion_fun2_def completion_def hom_def expand_fun_eq) (auto)

lemma (in ring_endomorphisms) ring_endomorphisms_pert: assumes delta: "δ ∈ pert D"
  shows "ring_endomorphisms (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)), R"
  (is "ring_endomorphisms ?D' R")
proof -
  from diff_group_pert_is_diff_group [OF delta] have diff_group_pert: "diff_group ?D'" by simp
  moreover from ring_endomorphisms_def [of D R] and prems have R_ring: "ring R" by (unfold ring_def, simp)
  moreover from ring_R have "R = (|carrier = hom_completion ?D' ?D', mult = op o,
    one = λx. if x ∈ carrier ?D' then id x else \<one>?D',
    zero = λx. if x ∈ carrier ?D' then \<one>?D' else \<one>?D',
    add = λf g x. if x ∈ carrier ?D' then f x ⊗?D'  g x else \<one>?D'|)),"
    proof -
    from ring_R and hom_completion_eq [OF delta] have "carrier R = hom_completion ?D' ?D'" by simp
    moreover from ring_R have "mult R = op o" by simp
    moreover from ring_R have "one R = (λx. if x ∈ carrier ?D' then id x else \<one>?D')" by (simp add: expand_fun_eq)
    moreover from ring_R have "zero R = (λx. if x ∈ carrier ?D' then \<one>?D' else \<one>?D')" by simp
    moreover from ring_R have "add R = (λf g x. if x ∈ carrier ?D' then f x ⊗?D' g x else \<one>?D')" by (simp add: expand_fun_eq)
    ultimately show ?thesis by auto
      (* Another possible proof, a bit more obscure
      apply (unfold ring_endomorphisms_def expand_fun_eq)
      apply (auto simp add: prems)
      apply (unfold hom_completion_def completion_fun2_def completion_def hom_def expand_fun_eq)
      apply (auto simp add: prems)
      *)
  qed
  ultimately show ?thesis by (unfold ring_endomorphisms_def ring_endomorphisms_axioms_def ring_def diff_group_def, simp)
qed

text{*The two following lemmas prove that @{term [locale=lemma_2_2_15] "h' ⊗R h' = \<zero>R"}
  and @{term [locale=lemma_2_2_15] "h' ⊗R diff' ⊗R h' = h'"};
  these are the properties that will allow us to introduce @{thm [locale=lemma_2_2_14] lemma_2_2_14}
  in order to define the reduction needed for @{text "Lemma 2.2.15"}*}

lemma (in lemma_2_2_15) h'_nil: shows "h' ⊗R h' = \<zero>R"
proof -
  from h'_def have "h' ⊗R h' = (h ⊗R Φ) ⊗R (h ⊗R Φ)" by simp
  also from psi_h_h_phi and h_in_R phi_in_R psi_in_R and R.m_assoc [of Ψ h "(h ⊗R Φ)"]
    and R.m_assoc [of h h Φ]
  have "… = Ψ ⊗R (h ⊗R h ⊗R Φ)" by simp
  also from h_nil have "… = \<zero>R" by simp
  finally show ?thesis by simp
qed

lemma (in lemma_2_2_15) h'd'h'_h': shows "h' ⊗R diff' ⊗R h' = h'"
    (*Maybe this simplification process could be tried in another theorem prover, just in order to see if it succeeds faster*)
    (*The equations in the premises are a bit tricky, since they can produce very easily infinite loops*)
proof -
  from h'_def have "h' ⊗R diff' ⊗R h' = (h ⊗R Φ) ⊗R diff' ⊗R (h ⊗R Φ)" by simp
  also from psi_h_h_phi have "… = (Ψ ⊗R h) ⊗R diff' ⊗R (h ⊗R Φ)" by simp
  also from h_in_R phi_in_R psi_in_R diff'_def diff_in_R pert_in_R
  have "… = (Ψ ⊗R (h ⊗R (differD) ⊗R h ⊗R Φ)) ⊕R (Ψ ⊗R h) ⊗R ((δ ⊗R h) ⊗R Φ)" by algebra
  also have "… = (Ψ ⊗R (h ⊗R Φ)) ⊕R (Ψ ⊗R h) ⊗R (\<one>R \<ominus>R Φ)"
  proof -
    from phi_prop have "Φ = \<one>R \<ominus>R δ ⊗R h ⊗R Φ" by simp
    with h_in_R phi_in_R pert_in_R have "\<one>R \<ominus>R Φ = \<one>R \<ominus>R  (\<one>R \<ominus>R δ ⊗R h ⊗R Φ)" by algebra
    with h_in_R phi_in_R pert_in_R have r_h_p: "\<one>R \<ominus>R Φ = δ ⊗R h ⊗R Φ" by algebra
    from hdh_h have l_h_p: "h ⊗R (differD) ⊗R h = h" by simp
    from r_h_p and l_h_p show ?thesis by simp
  qed
  also from h_in_R phi_in_R psi_in_R diff_in_R pert_in_R have "… = Ψ ⊗R h ⊗R Φ ⊕R Ψ ⊗R h \<ominus>R Ψ ⊗R h ⊗R Φ" by algebra (simp)
    (*Here I would expect "by algebra" to finish the work*)
  also from h_in_R phi_in_R psi_in_R diff_in_R pert_in_R have "… = Ψ ⊗R h" by algebra
  also from psi_h_h_phi have "… = h ⊗R Φ" by simp
  also from h'_def have "… = h'" by simp
  finally show ?thesis by simp
qed

text{*The following lemma is an instantiation of @{term [locale=lemma_2_2_14] "lemma_2_2_14"}, where
  @{term [locale=lemma_2_2_15] "D' = (|carrier = carrier D, mult = mult D, one = one D, diff = differ ⊕R δ|)),"}
  @{term [locale=lemma_2_2_15] "R = R"}, and finally @{term [locale=lemma_2_2_15] "h = h ⊗R Φ"}. *}
text{*Therefore, the premises of locale @{text "lemma_2_2_14"} have to be verified *}
text{*It is not neccesary to explicitly prove that @{term [locale=lemma_2_2_15] "diff_group_ker_p'"} is a differential group,
  since it is one of the premises in the definition of reduction*}

lemma (in lemma_2_2_15) lemma_2_2_15: shows "reduction D' diff_group_ker_p' (\<one>R \<ominus>R p') inc_ker_p' h'"
proof -
    (*Point 1) in the proof in the memoir*)
  from diff_group_pert_is_diff_group and delta_pert and D'_def have diff_group_D': "diff_group D'" by simp
  moreover (*This point was omitted in the memoir; actually, it can be considered trivial*)
  from h'_in_R and ring_R and hom_completion_eq [OF delta_pert] and D'_def have "h' ∈ hom_completion D' D'" by simp
  moreover (*Point 2) in the proof in the memoir*)
  from h'_nil have h'_nilpot: "h' ⊗R h' = \<zero>R" by simp
  moreover (*Point 3) in the memoir proof*)
  from h'd'h'_h' have "h' ⊗R diff' ⊗R h' = h'" by simp
  moreover (*This point was omitted in the memoir; it can be seen as trivial in an informal proof*)
  from ring_endomorphisms_pert [OF delta_pert] and D'_def have ring_D': "ring_endomorphisms D' R" by (unfold ring_endomorphisms_def, simp)
      (*With the previous facts, lemma_2_2_14 can be directly applied*)
  ultimately have lemma_2_2_14: "lemma_2_2_14 D' R h'"
    by (unfold lemma_2_2_14_def lemma_2_2_14_axioms_def diff_group_def ring_endomorphisms_def diff'_def D'_def, simp)
  from lemma_2_2_14.p_def [OF lemma_2_2_14] lemma_2_2_14.inc_ker_p_def [OF lemma_2_2_14] lemma_2_2_14.diff_group_ker_p_def [OF lemma_2_2_14]
    lemma_2_2_14.lemma_2_2_14 [OF lemma_2_2_14] show ?thesis
    by (simp add: diff_group_ker_p'_def inc_ker_p'_def inc_ker_p_def p'_def D'_def)
qed

end