Up to index of Isabelle/HOL/HOL-Algebra/example_Bicomplex
theory BPL_classes_2008(* Title: code_generation/BPL_classes_2008.thy
ID: $Id: BPL_classes_Isabelle2008.thy $
Author: Jesus Aransay
*)
theory BPL_classes_2008
imports
Basic_Perturbation_Lemma_local_nilpot
While
begin
section{*Additional type classes*}
text{*In this section we introduce some additional type classes
to those provided by the Isabelle standard distribution*}
text{*For instance, we need a class @{term diff_group_add} that
can be defined from the @{term ab_group_add} type
class from the Isabelle library:*}
class diff_group_add = ab_group_add +
fixes diff :: "'a => 'a" ("d _" [81] 80)
assumes diff_hom: "d (x + y) = (d x) + (d y)"
and diff_nilpot: "diff o diff = (λx. 0)"
lemma (in diff_group_add) [simp]: "d (d x) = 0"
using diff_nilpot
unfolding expand_fun_eq by simp
text{*According to the previous syntax definitions,
@{term [locale=diff_group_add] "(λx. d x)"} is to be used
with the parameter over which it is applied,
and @{term [locale=diff_group_add] diff} remains to be used as a function*}
text{*We can indeed prove instances of the specified type classes.
An instance of a type class makes the type class sound.*}
instantiation int :: diff_group_add
begin
definition diff_int_def: "diff ≡ (λx. 0::int)"
instance
proof
show "diff o diff = (λx::int. 0)"
unfolding diff_int_def
unfolding expand_fun_eq by simp
fix x y ::int
show "d (x + y) = (d x) + (d y)"
unfolding diff_int_def by arith
qed
end
text{*A limitation of type classes can be observed in the following definition;
using the @{term "op +"} symbol for @{term "fun"} is not possible.
In a type class definition, symbols only refer to the type class being defined.*}
text{*The following type class definition is not valid;
the + operation can only be used for the type class being defined*}
(*class diff_group_add_pert = diff_group_add +
fixes pert :: "'a => 'a" ("δ _" [81] 80)
assumes pert_hom_ab: "δ (a + b) = δ a + δ b"
and pert_preserv_diff_group_add:
"diff_group_add (op -) (λx. - x) 0 (op +) (diff + pert)"*)
text{*The following type class represents a
differential group and a perturbation over it.*}
class diff_group_add_pert = diff_group_add +
fixes pert :: "'a => 'a" ("δ _" [81] 80)
assumes pert_hom_ab: "δ (a + b) = δ a + δ b"
and pert_preserv_diff_group_add:
"diff_group_add (op -) (λx. - x) 0 (op +) (λx. d x + δ x)"
instantiation int :: diff_group_add_pert
begin
definition pert_int_def: "pert ≡ (λx. 0::int)"
instance proof
fix a b :: int
show "δ (a + b) = δ a + δ b"
unfolding pert_int_def by simp
next
show "diff_group_add op - uminus (0::int) op + (λx. d x + δ x)"
unfolding diff_group_add_def
unfolding diff_group_add_axioms_def
proof (intro conjI)
show " ab_group_add op - uminus (0::int) op +"
by intro_locales
next
show "∀x (y::int). d (x + y) + δ (x + y) = d x + δ x + (d y + δ y)"
proof (rule allI)+
fix a b :: int
show "d (a + b) + δ (a + b) = d a + δ a + (d b + δ b)"
unfolding diff_int_def
unfolding pert_int_def by arith
qed
next
show "(λx::int. d x + δ x) o (λx. d x + δ x) = (λx. 0)"
unfolding diff_int_def
unfolding pert_int_def by (simp add: expand_fun_eq)
qed
qed
end
text{*We now prove some facts about generic functions.
With appropriate restrictions over the type classes over which they are defined,
functions can be proved to be also instances of some type classes.*}
instantiation "fun" :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
begin
definition plus_fun_def: "f + g == (%x. f x + g x)"
instance proof
fix x y z :: "'a => 'b"
show "x + y + z = x + (y + z)"
unfolding plus_fun_def by (auto simp add: add_assoc)
next
fix x y :: "'a => 'b"
show "x + y = y + x"
unfolding plus_fun_def by (auto simp add: add_commute)
qed
end
instantiation "fun" :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
begin
definition zero_fun_def: "0 == (λx. 0)"
instance proof
fix a :: "'a => 'b"
show "0 + a = a"
unfolding zero_fun_def plus_fun_def by simp
qed
end
text{*The Isabelle release 2008 already contains the definition
of the difference of functions and also the unary minus*}
instantiation "fun" :: (ab_group_add, ab_group_add) ab_group_add
begin
instance proof
fix a :: "'a => 'b"
show "- a + a = 0"
unfolding fun_Compl_def
unfolding zero_fun_def
unfolding plus_fun_def by simp
next
fix a b :: "'a => 'b"
show "a - b = a + - b"
unfolding plus_fun_def
unfolding fun_diff_def
unfolding fun_Compl_def by (simp add: expand_fun_eq)
qed
end
text{*The following type class specifies a differential group
with a perturbation and also a homotopy operator.*}
text{*The previous fact about the @{text "fun"} datatype contructor
allows us now to use @{term "op -"}
to define @{text α} in a more readable way*}
class diff_group_add_pert_hom = diff_group_add_pert +
fixes hom_oper:: "'a => 'a" ("h _" [81] 80)
assumes h_hom_ab: "h (a + b) = h a + h b"
and h_nilpot: "(λx. h x) o (λx. h x) = (λx. 0)"
begin
definition α :: "'a => 'a"
where "α = (λx. - (pert (hom_oper x)))"
end
instantiation int :: diff_group_add_pert_hom
begin
definition hom_oper_int_def: "hom_oper ≡ (λx. 0::int)"
instance proof
fix a b :: int
show "h (a + b) = h a + h b"
unfolding hom_oper_int_def by arith
next
show "(λx. h x) o (λx. h x) = (λx::int. 0)"
unfolding hom_oper_int_def
unfolding expand_fun_eq by auto
qed
end
lemma [code]: shows "α = (- ((λ x. δ x) o (λx. h x)))"
unfolding α_def
unfolding fun_Compl_def by simp
section{*Local nilpotency*}
text{*We add now the notion of @{text "local_bounded_func"}in a purely
\emph{existential} way; from the existential definition we will later
define the function providing this local bound for every x.*}
text{*The reason to introduce now this notion is that @{term α}
is the function verifying the local nilpotency condition*}
context ab_group_add
begin
definition local_bounded_func :: "('a => 'a) => bool"
where "local_bounded_func f = (∀ x. ∃ n. (f^n) x = 0)"
text{*Here is a relevant difference with the previous proof of the BPL;
there, the local bound was defined as the Least natural
number @{term "n::nat"} satisfying the property
@{term [locale=diff_group_add_pert_hom] "(α^n) (x::'a) = 0"}.
Now, in our attempt to make this definition computable, or executable,
we define it as an iterating structure (a \emph{For} loop),
where the boolean condition in the loop is expressed as
@{term [locale=ab_group_add] "(λ y. y ≠ 0)"}*}
text{*Later we will try to apply the code generator over these definitions*}
definition local_bound_gen :: "('a => 'a) => 'a => nat => nat"
where "local_bound_gen f x n == For (λ y. y ≠ 0) f (λ y n. n + (1::nat)) x n"
definition local_bound:: "('a => 'a) => 'a => nat"
where "local_bound f x = local_bound_gen f x 0"
end
text{* We now define the simplification rule for @{term "local_bound_gen"}: *}
lemmas local_bound_gen_simp =
For_simp[of "(λ y. y ≠ (0::'a::ab_group_add))" _ "λ y n. n+(1::nat)",
simplified local_bound_gen_def[symmetric]]
text{*Two simple "calculations" with @{term "local_bound"}: *}
lemma "local_bound f 0 = 0"
unfolding local_bound_def
unfolding local_bound_gen_simp [of f 0 0] by simp
lemma "x ≠ 0 ==> local_bound (λ x. 0) x = 1"
unfolding local_bound_def
using local_bound_gen_simp by simp
text{*Now, we connect the neccesary termination of For with our termination condition,
@{term local_bounded_func}. *}
text{*Then, under the @{term local_bounded_func} premise the loop will be terminating.*}
lemma local_bounded_func_impl_terminates_loop:
"local_bounded_func f = (∀ x. terminates (λ y. y ≠ 0, f, x))"
unfolding local_bounded_func_def
unfolding terminates_simp
unfolding Orbit_def by simp
lemma LEAST_local_bound_0:
"(LEAST n::nat. (f ^ n) (0::'a::ab_group_add) = (0::'a)) = 0"
using Least_le [of "λn. (f ^n) 0 = 0" 0] by simp
lemma local_bound_gen_correct:
"terminates (λ y. y ≠ (0::'a::ab_group_add), f, x)
==> local_bound_gen f x m = m + (LEAST n::nat. (f^n) x = 0)"
apply (rule For_pinduct[where i=x and s=m and Ac="λ y n. n+1"])
apply simp
apply (subst local_bound_gen_simp)
apply (case_tac "i = 0")
apply (simp add: LEAST_local_bound_0)
apply simp
apply (frule_tac x=i in terminates_implies)
apply (frule_tac i=i in terminates_imp)
apply simp
apply (frule_tac x="f i" in terminates_implies)
apply auto
apply (rule Least_Suc2[symmetric])
apply (auto simp add: funpow_zip)
done
text{*The following lemma exactly represents the difference between our
old definitions, with which we proved the BPL, and the new ones,
from which we are trying to generate code;
under the termination premise, both
@{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"},
the old definition of local nilpotency,
and @{term [locale=ab_group_add] "local_bound f x"},
the loop computing the lower bound, are equivalent*}
text{*Whereas @{term "(LEAST n::nat. (f^n) (x::'a::ab_group_add) = 0)"}
does not have a computable interpretation,
@{term [locale=ab_group_add] "local_bound f x"} does have it,
and code can be generated from it.*}
lemma local_bound_correct:
"terminates (λ y. y ≠ (0::'a::ab_group_add), f, x)
==> local_bound f x = (LEAST n::nat. (f^n) x = 0)"
unfolding local_bound_def
unfolding local_bound_gen_correct [of f x 0] by arith
lemma local_bounded_func_impl_local_bound_is_Least:
assumes lbf_f:"local_bounded_func f"
shows "local_bound f x = (LEAST n::nat. (f^n) x = 0)"
using lbf_f
unfolding local_bounded_func_impl_terminates_loop [OF ]
using local_bound_correct [of f x] ..
text{* Both @{term "local_bound"} and @{term "terminates"} are executable.*}
text{*This is another possible definition of our iterative process as a
tail recursion, instead of using @{term While},
suggested by Alexander Krauss;
code generation is also possible from this definition.*}
text{*A good motivation to use the @{term While} operator instead of this one,
is that some additional induction principles
have been provided for the @{term For} and @{term While} operators.*}
function (tailrec) local_bound' :: "('a::zero => 'a) => 'a => nat => nat"
where
"local_bound' f x n
= (if (f^n) x = 0 then n else local_bound' f x (Suc n))"
by pat_completeness auto
lemma [code func]:
"local_bound' f (x::'a::zero) n
= (if (f^n) x = 0 then n else local_bound' f x (Suc n))"
by simp
export_code local_bound'
in SML file "local_bound.ML"
lemma [code func]:
"While continue f s
= (if continue s then While continue f (f s) else s)"
unfolding While_simp [of continue f s] ..
export_code While
in SML file "Loop.ML"
export_code local_bound
in SML file "local_bound2.ML"
section{*Finite sums*}
text{*The following definition of @{term fin_sum} will replace
the definitions for sums of series used in the formal proof of the BPL.*}
text{*That definitions were based on the fold operator over sets,
from which direct code generation cannot be obtained.*}
text{*The finite sum of a series is defined as a primitive recursive
function over the natural numbers.*}
text{*This definition will have to be proved later equivalent,
in our setting, to the sums appearing in the BPL proof.*}
primrec fin_sum :: "(('a::ab_group_add) => 'a) => nat => ('a => 'a)"
where
"fin_sum f 0 =id"
| "fin_sum f (Suc n) = f^(Suc n) + (fin_sum f n)"
text{*The following definition of @{term diff_group_add_pert_hom_bound_exist}
contains the local nilpotency condition.
It is based on an existential statement.*}
text{*For all @{term "x"} belonging to our differential group,
we state the existence of a natural number @{term "n::nat"} which is a bound
for @{term [locale=diff_group_add_pert_hom] "α"}*}
text{*We then prove that it is equivalent to the previously given
definition of @{term locale_bounded_func}.*}
text{*Finally, we link this fact to the previous results about
computation of the bounds as a \emph{For} operator.*}
class diff_group_add_pert_hom_bound_exist =
diff_group_add_pert_hom +
assumes local_nilp_cond: "∀x.∃n::nat. (α^n) x = 0"
(*The following definition cannot be inserted in the @{text "class"} context
begin
definition Φ :: "'a => 'a"
where "Φ == (λx. (fin_sum α) (local_bound α x) x)"
end*)
lemma diff_group_add_pert_hom_bound_exist_impl_local_bounded_func_alpha:
assumes diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist
op - (λx. - x) 0 op + (λx. d x) (λx. δ x) (λx. h x)"
shows "local_bounded_func (α::'a::diff_group_add_pert_hom_bound_exist => 'a)"
unfolding local_bounded_func_def
using local_nilp_cond .
lemma diff_group_add_pert_hom_bound_exist_impl_local_bound_is_Least:
assumes diff:
"diff_group_add_pert_hom_bound_exist
op - (λx. - x) 0 op + (λx. d x) (λx. δ x) (λx. h x)"
shows "local_bound α (x::'a::diff_group_add_pert_hom_bound_exist)
= (LEAST n::nat. (α^n) x = 0)"
unfolding local_bounded_func_impl_local_bound_is_Least
[OF diff_group_add_pert_hom_bound_exist_impl_local_bounded_func_alpha
[OF diff]] ..
(*text The definition command does not allow the following:
definition (in diff_group_add_pert_hom_bound_exist)
Φ :: "'a => 'a"
where "Φ == (λx. fin_sum (α) (local_bound α x) x)"*)
text{*Apparently, @{typ "'a"} does not belong to the appropriate type class.*}
text{*It does not seem either a good option to use
long qualifiers with the locale name*}
text{*Instead, we have to use the following
explicit restriction of the type parameter*}
text{*The following definitions will have to be later compared with the ones
@{term [locale=BPL] "Φ"}, \dots*}
text{*Additionally, code generation from them must be possible.*}
(*definition Φ :: "('a::diff_group_add_pert_hom_bound_exist => 'a)"
where "Φ == (λx. fin_sum α (local_bound (diff_group_add_pert_hom.α uminus pert hom_oper) x) x)"*)
definition Φ ::
"('a::diff_group_add_pert_hom_bound_exist => 'a)"
where "Φ = (λx. fin_sum α (local_bound α x) x)"
definition β :: "('a::diff_group_add_pert_hom_bound_exist => 'a)"
where "β = (- ((λx. h x) o (λ x. δ x)))"
definition Ψ :: "('a::diff_group_add_pert_hom_bound_exist => 'a)"
where "Ψ = (λx. fin_sum β (local_bound β x) x)"
text{*The following definitions are also to be compared with the ones
appearing in the output of the @{thm BPL.BPL}*}
definition dC' :: "('a::diff_group_add_pert_hom_bound_exist => 'b::diff_group_add)
=> ('b => 'a) => ('b => 'b)"
where "dC' f g = diff + (f o (λx. δ x) o Ψ o g)"
definition f' :: "('a::diff_group_add_pert_hom_bound_exist => 'b::diff_group_add)
=> ('a => 'b)"
where "f' f = f o Φ"
definition g' :: "('b::diff_group_add => 'a::diff_group_add_pert_hom_bound_exist)
=> ('b => 'a)"
where g'_def: "g' g == Ψ o g"
definition h' :: "('a::diff_group_add_pert_hom_bound_exist => 'a)"
where "h' == (λx. h x) o Φ"
export_code Φ Ψ f' g' h' dC' in SML file "output_reduction.ML"
text{*Some facts about the product of types:*}
instantiation * :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
begin
definition mult_plus_def:
"x + y ≡ (let (x1, x2) = x; (y1, y2) = y in (x1 + y1, x2 + y2))"
instance proof
fix a::"'a::ab_semigroup_add × 'b::ab_semigroup_add"
obtain i j where a_split: "a = (i, j)" by force
fix b::"'a × 'b"
obtain k l where b_split: "b = (k, l)" by force
fix c::"'a × 'b"
obtain m n where c_split: "c = (m, n)" by force
show "a + b + c = a + (b + c)"
unfolding a_split b_split c_split
unfolding mult_plus_def
by (auto simp add: add_assoc)
show "a + b = b + a"
unfolding a_split b_split
unfolding mult_plus_def
by (auto simp add: add_commute)
qed
end
definition x5:: "(int × int)"
where "x5 = ((3::int), (5::int)) + (5, 7)"
definition x6 :: "(int × int) × (int × int)"
where "x6 = (((3::int), (5::int)), ((3::int), (5::int))) + ((5, 7), (5, 7))"
export_code x5 x6
in SML file "x6.ML"
instantiation * :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
begin
definition mult_zero_def: "0 ≡ (0, 0)"
instance by default (simp add: split_paired_all mult_plus_def mult_zero_def)
end
section{*Equivalence of both approaches*}
subsection{*Algebraic structures*}
text{*In the following section we prove that the results already
proved using the definitions provided by the Algebra Isabelle
Library (leading to the @{thm [locale=BPL] BPL}) also hold for the
new definitions, where algebraic structures are
implemented by means of type classes.*}
text{*This does not mean that the proof of the BPL can be
developed only by using type classes; the degree of expressivity needed in
its proofs should be quite hard to achieve using type classes;
specially, the parts where restrictions of domains of functions
have to be used.*}
text{*We only pretend to prove that the new definitions,
to some extent simplified (see for instance the new proposed series in relation
to the previous implementation of series), are equivalent to the old ones,
and thus, also satisfy the BPL.*}
text{*Functions (or functors) translating type classes into algebraic
structures implemented as recods are used; these translations are
the natural ones*}
definition monoid_functor :: "('a => 'a => 'a) => ('a) => 'a monoid"
where "monoid_functor A B == (| carrier = UNIV, mult = A, one = B|)),"
lemma monoid_add_impl_monoid:
assumes mon_add: "monoid_add zero' plus'"
shows "monoid (| carrier = UNIV, mult = plus', one = zero'|)),"
using mon_add
unfolding monoid_def
unfolding monoid_add_def monoid_add_axioms_def
unfolding ab_semigroup_add_def
unfolding ab_semigroup_add_axioms_def
unfolding semigroup_add_def by simp
lemma monoid_functor_preserv:
assumes monoid_add:"monoid_add zero' plus'"
shows "monoid (monoid_functor plus' zero')"
using monoid_add_impl_monoid [OF monoid_add]
unfolding monoid_functor_def [of plus' zero'] .
lemma comm_monoid_add_impl_monoid_add:
assumes comm_monoid_add: "comm_monoid_add zero' plus'"
shows "monoid_add zero' plus'"
using comm_monoid_add
unfolding comm_monoid_add_def
unfolding monoid_add_def
unfolding ab_semigroup_add_def
unfolding comm_monoid_add_axioms_def
unfolding monoid_add_axioms_def
unfolding ab_semigroup_add_axioms_def by auto
lemma comm_monoid_add_impl_monoid:
assumes c_m: "comm_monoid_add zero' plus'"
shows "monoid (| carrier = UNIV, mult = plus', one = zero'|)),"
using monoid_add_impl_monoid [OF comm_monoid_add_impl_monoid_add
[OF c_m]] .
lemma ab_group_add_impl_comm_monoid_add:
assumes ab_gr_add: "ab_group_add uminus' minus' zero' plus'"
shows "comm_monoid_add zero' plus'"
using ab_gr_add
unfolding ab_group_add_def ..
lemma ab_group_class_impl_group:
assumes ab_gr_class: "ab_group_add uminus' minus' zero' plus'"
shows "group (| carrier = UNIV, mult = plus', one = zero'|)),"
proof (intro_locales)
show "monoid (|carrier = UNIV, mult = plus', one = zero'|)),"
using monoid_add_impl_monoid
[OF comm_monoid_add_impl_monoid_add
[OF ab_group_add_impl_comm_monoid_add
[OF ab_gr_class]]] .
show "group_axioms (|carrier = UNIV, mult = plus', one = zero'|)),"
using ab_gr_class
unfolding group_axioms_def
unfolding Units_def
unfolding ab_group_add_def
unfolding comm_monoid_add_def
unfolding ab_group_add_axioms_def
unfolding ab_semigroup_add_def
ab_semigroup_add_axioms_def by auto+
qed
lemma monoid_functor_preserv_group:
assumes ab_gr: "ab_group_add uminus' minus' zero' plus'"
shows "group (monoid_functor plus' zero')"
using ab_group_class_impl_group [OF ab_gr]
unfolding monoid_functor_def [of plus' zero'] .
lemma ab_group_add_impl_comm_group:
assumes ab_gr_add: "ab_group_add uminus' minus' zero' plus'"
shows "comm_group (| carrier = UNIV, mult = plus', one = zero'|)),"
proof (intro_locales)
show "monoid (|carrier = UNIV, mult = plus', one = zero'|)),"
using comm_monoid_add_impl_monoid
[OF ab_group_add_impl_comm_monoid_add
[OF ab_gr_add]] .
show "comm_monoid_axioms (|carrier = UNIV, mult = plus', one = zero'|)),"
using ab_gr_add
unfolding comm_monoid_axioms_def
unfolding ab_group_add_def
unfolding comm_monoid_add_def
unfolding ab_group_add_axioms_def
unfolding ab_semigroup_add_def
unfolding ab_semigroup_add_axioms_def by auto
show "group_axioms (|carrier = UNIV, mult = plus', one = zero'|)),"
using ab_gr_add
unfolding group_axioms_def
unfolding Units_def
unfolding ab_group_add_def
unfolding comm_monoid_add_def
unfolding ab_group_add_axioms_def
unfolding ab_semigroup_add_def
unfolding ab_semigroup_add_axioms_def by auto+
qed
lemma monoid_functor_preserv_ab_group:
assumes ab_gr_add: "ab_group_add uminus' minus' zero' plus'"
shows "comm_group (monoid_functor plus' zero')"
using ab_group_add_impl_comm_group [OF ab_gr_add]
unfolding monoid_functor_def [of plus' zero'] .
lemma diff_group_add_impl_comm_group:
assumes diff_gr_add: "diff_group_add uminus' minus' zero' plus' diff'"
shows "comm_group (|carrier = UNIV, mult = plus', one = zero'|)),"
proof (rule ab_group_add_impl_comm_group)
show "ab_group_add uminus' minus' zero' plus'"
using diff_gr_add
unfolding diff_group_add_def by simp
qed
lemma diff_group_add_impl_diff_group:
assumes diff_gr_add: "diff_group_add uminus' minus' zero' prod' diff'"
shows "diff_group (|carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff' |)),"
proof (intro_locales)
from diff_group_add_impl_comm_group [OF diff_gr_add]
have comm_gr: "comm_group (|carrier = UNIV, mult = prod', one = zero'|)),"
by simp
show "monoid (|carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff'|)),"
using comm_gr
unfolding comm_group_def
unfolding comm_monoid_def
unfolding monoid_def by simp
show "comm_monoid_axioms (|carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff'|)),"
using comm_gr
unfolding comm_group_def
unfolding comm_monoid_def
unfolding comm_monoid_axioms_def by simp
show "group_axioms (|carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff'|)),"
using comm_gr
unfolding comm_group_def
unfolding group_def
unfolding group_axioms_def
unfolding Units_def by simp
show "diff_group_axioms (|carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff'|)),"
using diff_gr_add
unfolding diff_group_add_def
unfolding diff_group_add_axioms_def
unfolding diff_group_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding completion_fun2_def
unfolding completion_def by auto
qed
definition diff_group_functor ::
"('a => 'a) => ('a => 'a => 'a) => ('a)
=> ('a => 'a => 'a) => ('a => 'a) => 'a diff_group"
where "diff_group_functor uminus' minus' zero' prod' diff' =
(| carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff'|)),"
lemma diff_group_functor_preserves:
assumes diff_gr_add: "diff_group_add minus' uminus' zero' prod' diff'"
shows "diff_group (diff_group_functor uminus' minus' zero' prod' diff')"
using diff_group_add_impl_diff_group [OF diff_gr_add]
unfolding diff_group_functor_def [of uminus' minus' zero' prod' diff'] .
text{*After the previous equivalences between algebraic structures,
now we prove the equivalence between the old definitions about
homomorphisms and the new ones:*}
subsection{*Homomorphisms and endomorphisms.*}
(*definition homo :: "('a::monoid_add => 'b::monoid_add) => bool"
where "homo f <-> (ALL a b. f (a + b) = f a + f b)"*)
definition homo_ab :: "('a::comm_monoid_add => 'b::comm_monoid_add) => bool"
where "homo_ab f = (ALL a b. f (a + b) = f a + f b)"
lemma homo_ab_apply:
assumes h_f: "homo_ab f"
shows "f (a + b) = f a + f b"
using homo_ab_def [of f] h_f by simp
lemma homo_ab_preserves_hom_completion:
assumes homo_ab_f: "homo_ab f"
shows "f ∈ hom_completion (monoid_functor (op +) 0) (monoid_functor (op +) 0)"
using homo_ab_f
unfolding hom_completion_def
unfolding homo_ab_def
unfolding monoid_functor_def
unfolding completion_fun2_def
unfolding completion_def
unfolding hom_def by auto
lemma plus_fun_apply:
"(f + g) (x::'a::ab_semigroup_add) = f x + g x"
using plus_fun_def [of f g] by simp
lemma homo_ab_plus_closed:
assumes comm_monoid_add_A: "comm_monoid_add (0::'a::comm_monoid_add) op +"
and comm_monoid_add_B: "comm_monoid_add (0::'b::comm_monoid_add) op +"
and x: "homo_ab (x::'a::comm_monoid_add => 'b::comm_monoid_add)"
and y: "homo_ab y"
shows "homo_ab (x + y)"
proof (unfold homo_ab_def, rule allI, rule allI)
have ab_semigroup_add_plus: "ab_semigroup_add (op +::'b => 'b => 'b)"
using comm_monoid_add_B
unfolding comm_monoid_add_def ..
fix a b :: 'a
show "(x + y) (a + b) = (x + y) a + (x + y) b"
proof -
have "(x + y) (a + b) = x (a + b) + y (a + b)"
using plus_fun_apply [of x y "a + b"] .
also have "… = x a + x b + (y a + y b)"
unfolding homo_ab_apply [OF x]
unfolding homo_ab_apply [OF y] ..
also have "… = x a + (x b + y a + y b)"
by (auto simp add: add_assoc)
also have "… = x a + (y a + x b + y b)"
by (auto simp add: add_commute add_assoc)
also have "… = x a + y a + (x b + y b)"
by (auto simp add: add_assoc)
also have "… = (x + y) a + (x + y) b"
unfolding sym [OF plus_fun_apply [of x y a]]
unfolding sym [OF plus_fun_apply [of x y b]] ..
finally show ?thesis .
qed
qed
lemma end_comm_monoid_add_closed:
assumes comm_monoid_add: "comm_monoid_add (0::'a::comm_monoid_add) op +"
and x: "homo_ab (x::'a::comm_monoid_add => 'a)"
and y: "homo_ab y"
shows "homo_ab (x + y)"
using homo_ab_plus_closed [OF comm_monoid_add comm_monoid_add x y] .
lemma comm_monoid_add_impl_homo_abelian_monoid:
assumes comm_monoid_add: "comm_monoid_add (0::'a::comm_monoid_add) op +"
shows "abelian_monoid (|carrier = {f::'a::comm_monoid_add => 'a. homo_ab f},
mult = op o,
one = id,
zero = 0,
add = op +|)),"
proof (intro abelian_monoidI, auto)
fix x y :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y"
show "homo_ab (x + y)"
using end_comm_monoid_add_closed [OF comm_monoid_add x y] .
next
show "homo_ab (0::'a => 'a)"
unfolding zero_fun_def homo_ab_def by simp
next
fix x y z :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y" and z: "homo_ab z"
show "x + y + z = x + (y + z)"
unfolding plus_fun_def by (simp only: add_assoc)
next
fix x y :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y"
show "x + y = y + x" unfolding plus_fun_def expand_fun_eq by (simp add: add_ac)
qed
lemma ab_group_add_impl_uminus_fun_closed:
assumes ab_group_add: "ab_group_add op - (λx. - x) (0::'a::ab_group_add) op +"
and f: "homo_ab (f::'a::ab_group_add => 'a)"
shows "homo_ab (- f)"
proof (unfold fun_Compl_def homo_ab_def, rule allI, rule allI)
fix a b :: 'a
show "- f (a + b) = - f a + - f b"
proof -
have l_h_s: "f (a + b) + - f (a + b) = 0"
using sym [OF add_commute [of "- f (a + b)" "f (a + b)"]]
unfolding ab_left_minus [of "f (a + b)"] .
have "f (a + b) + (- f a + - f b) = - f a + - f b + f (a + b)"
using sym [OF add_commute [of "- f a + - f b" "f (a + b)"]] .
also have "- f a + - f b + f (a + b) = - f a + - f b + (f a + f b)"
unfolding homo_ab_apply [OF f] ..
also have "… = ((- f a + - f b) + f a) + f b"
unfolding sym [OF add_assoc [of "- f a + - f b" "f a" "f b"]] ..
also have "… = (- f a + (- f b + f a)) + f b"
unfolding add_assoc [of "- f a" "- f b" "f a"] ..
also have "… = (- f a + (f a + - f b)) + f b"
unfolding add_commute [of "- f b" "f a"] ..
also have "… = ((- f a + f a) + - f b) + f b"
unfolding sym [OF add_assoc [of "- f a" "f a" "- f b"]] ..
also have "… = 0 + - f b + f b"
unfolding ab_left_minus [of "f a"] ..
also have "… = 0 + (- f b + f b)"
unfolding add_assoc [of 0 "- f b" "f b"] ..
also have "… = 0 + 0" unfolding ab_left_minus [of "f b"] ..
also have "… = 0" by simp
finally have r_h_s: "f (a + b) + (- f a + - f b) = 0" .
with l_h_s have "f (a + b) + - f (a + b) = f (a + b) + (- f a + - f b)" by simp
then have "- (f::'a => 'a) ((a::'a) + (b::'a)) + (f (a + b) + - f (a + b))
= - f (a + b) + (f (a + b) + (- f a + - f b))" by simp
with sym [OF add_assoc [of "- f (a + b)" "f (a + b)" "- f (a + b)"]]
sym [OF add_assoc [of "- f (a + b)" "f (a + b)" "- f a + - f b"]]
have "(- (f::'a => 'a) ((a::'a) + (b::'a)) + f (a + b)) + - f (a + b)
= (- f (a + b) + f (a + b)) + (- f a + - f b)" by simp
with ab_left_minus [of "f (a + b)"]
have "0 + - f (a + b) = 0 + (- f a + - f b)" by simp
with left_minus [of "- f (a + b)"] left_minus [of "(- f a + - f b)"]
show ?thesis by simp
qed
qed
lemma ab_group_add_impl_homo_abelian_group_axioms:
assumes ab_group_add: "ab_group_add op - (λx. - x) (0::'a::ab_group_add) op +"
shows "abelian_group_axioms (|carrier = {f::'a::ab_group_add => 'a. homo_ab f},
mult = op o,
one = id,
zero = 0,
add = op +|)),"
proof (unfold abelian_group_axioms_def, simp)
show "comm_group (|carrier = Collect homo_ab, mult = op +, one = (0::'a => 'a)|)),"
proof (intro_locales)
show "monoid (|carrier = Collect homo_ab, mult = op +, one = (0::'a => 'a)|)),"
proof (intro monoidI, simp_all)
fix x y :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y"
show "homo_ab (x + y)"
using ab_group_add end_comm_monoid_add_closed [OF _ x y]
unfolding ab_group_add_def by simp
next
show "homo_ab (0::'a => 'a)"
unfolding zero_fun_def homo_ab_def by simp
qed
next
show "comm_monoid_axioms (|carrier = Collect homo_ab,
monoid.mult = op +,
one = (0::'a => 'a)|)),"
unfolding comm_monoid_axioms_def by auto
next
show "group_axioms (|carrier = Collect homo_ab,
monoid.mult = op +,
one = (0::'a => 'a)|)),"
proof (unfold group_axioms_def Units_def, auto)
fix x :: "'a => 'a"
assume x: "homo_ab x"
show "∃y::'a => 'a. homo_ab y ∧ y + x = 0 ∧ x + y = 0"
proof (rule exI [of _ "- x"], intro conjI)
show "homo_ab (- x)"
using ab_group_add_impl_uminus_fun_closed [OF ab_group_add x] .
show "(- x) + x = 0" by simp
show "x + (- x) = 0" by simp
qed
qed
qed
qed
text{*The previous lemma, @{thm ab_group_add_impl_homo_abelian_group_axioms},
proves the elements of @{term homo_ab} to be an abelian monoid
under suitable operations.*}
text{*In order to show that composition gives place to a monoid,
the underlying structure needs not to be even a monoid*}
lemma homo_monoid:
shows "monoid (|carrier = {f. homo_ab f},
monoid.mult = op o,
one = id,
zero = 0,
add = op +|)),"
(is "monoid ?HOMO_AB")
proof (intro monoidI, auto)
fix x y :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y"
then show "homo_ab (x o y)" unfolding homo_ab_def by simp
next
show "homo_ab id" unfolding homo_ab_def by simp
next
fix x y z :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y" and z: "homo_ab z"
show "x o y o z = x o (y o z)" by (simp add: expand_fun_eq)
qed
text{*A couple of lemmas completing the proof of the set @{term homo_ab}
being a ring, with suitable operations*}
lemma ab_group_add_impl_homo_ring_axioms:
assumes ab_group_add: "ab_group_add op - (λx. - x) (0::'a::ab_group_add) op +"
shows "ring_axioms (|carrier = {f. homo_ab f},
mult = op o,
one = id,
zero = (0::'a::ab_group_add => 'a),
add = op +|)),"
proof (intro ring_axioms.intro, auto)
fix x y z :: "'a => 'a"
assume x: "homo_ab x" and y: "homo_ab y" and z: "homo_ab z"
show "(x::'a => 'a) + y o z = (x o z) + (y o z)"
unfolding plus_fun_def
unfolding expand_fun_eq by auto
show "(z::'a => 'a) o x + y = (z o x) + (z o y)"
using z
unfolding expand_fun_eq plus_fun_def homo_ab_def by auto
qed
lemma ab_group_add_impl_homo_ring:
assumes ab_group_add: "ab_group_add op - (λx. - x) (0::'a::ab_group_add) op +"
shows "ring (|carrier = {f::'a::ab_group_add => 'a. homo_ab f},
mult = op o,
one = id,
zero = (0::'a => 'a),
add = op +|)),"
using ab_group_add
using comm_monoid_add_impl_homo_abelian_monoid
using ab_group_add_impl_homo_abelian_group_axioms
using homo_monoid
using ab_group_add_impl_homo_ring_axioms by (unfold ab_group_add_def, intro_locales, auto)
text{*The following definition includes the notion of differential homomorphism,
a homomorphism that additionally
commutes with the corresponding differentials.*}
definition homo_diff :: "('a::diff_group_add => 'b::diff_group_add) => bool"
where "homo_diff f = ((ALL a b. f (a + b) = f a + f b) ∧ f o diff = diff o f)"
lemma homo_diff_preserves_hom_diff:
assumes homo_diff_f: "homo_diff f"
shows "f ∈ hom_diff (diff_group_functor (λx. - x) op - 0 (op +) diff)
(diff_group_functor (λx. - x) op - 0 (op +) diff)"
using homo_diff_f
unfolding hom_diff_def
unfolding hom_completion_def
unfolding homo_diff_def
unfolding diff_group_functor_def
unfolding completion_fun2_def
unfolding completion_def
unfolding hom_def
by auto
subsection{*Definition of constants.*}
text{*The following definition of reduction is to be understand as follows:
a pair of homomorphisms @{text "(f, g)"} will be a reduction
iff: the underlying algebraic structures (given as classes) are,
respectively, a differential group class with a perturbation and a
homology operator (i.e, class @{term diff_group_add_pert_hom_bound_exists})
satisfying the local nilpotency condition,
and a differential group class (@{term diff_group_add}),
and the homomorphisms @{text f}, @{text g} and @{text h}
satisfy the properties required by the usual reduction definition.*}
text{*In the definition it can be noted the convenience of using overloading
symbols provided by the class mechanism.*}
definition
reduction_class_ext ::
"('a::diff_group_add_pert_hom_bound_exist => 'b::diff_group_add)
=> ('b => 'a) => bool"
where "reduction_class_ext f g =
((diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 (op +) diff pert hom_oper)
∧ (diff_group_add op - (λx::'b. - x) 0 (op +) diff)
∧ (homo_diff f) ∧ (homo_diff g)
∧ (f o g = id)
∧ ((g o f) + (diff o hom_oper) + (hom_oper o diff) = id)
∧ (f o hom_oper = (0::'a => 'b))
∧ (hom_oper o g = (0::'b => 'a)))"
text{*The previous definition contains all the ingredients
required to apply the old proof of the BPL.*}
lemma reduction_class_ext_impl_diff_group_add_pert_hom_bound_exist:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "(diff_group_add_pert_hom_bound_exist op -
(λx::'a::diff_group_add_pert_hom_bound_exist. - x) 0 (op +) diff pert hom_oper)"
using r_c_e unfolding reduction_class_ext_def ..
lemma reduction_class_ext_impl_diff_group_add:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "(diff_group_add op - (λx::'b::diff_group_add. - x) 0 (op +) diff)"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_homo_diff_f:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "homo_diff f"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_homo_diff_g:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "homo_diff g"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_fg_id:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "f o g = id"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_gf_dh_hd_id:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "(g o f) + (diff o hom_oper) + (hom_oper o diff) = id"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_fh_0:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "f o hom_oper = 0"
using r_c_e unfolding reduction_class_ext_def by fast
lemma reduction_class_ext_impl_hg_0:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "hom_oper o g = 0"
using r_c_e unfolding reduction_class_ext_def by fast
text{*The following lemma will be useful later, when we verify the premises of the BPL*}
lemma hdh_eq_h:
assumes r_c_e: "reduction_class_ext f (g::'b::diff_group_add
=> 'a::diff_group_add_pert_hom_bound_exist)"
shows "(hom_oper::'a::diff_group_add_pert_hom_bound_exist => 'a)
o diff o hom_oper = hom_oper"
proof -
have "hom_oper = hom_oper o id" by simp
also have "… = hom_oper o ((g o f) + (diff o hom_oper) + (hom_oper o diff))"
using r_c_e
unfolding reduction_class_ext_def by simp
also have "… = hom_oper o (diff o hom_oper)"
using reduction_class_ext_impl_diff_group_add_pert_hom_bound_exist
[OF r_c_e]
using reduction_class_ext_impl_hg_0 [OF r_c_e]
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding expand_fun_eq plus_fun_def zero_fun_def by auto
finally show ?thesis by (simp add: o_assoc)
qed
lemma diff_group_add_pert_hom_bound_exist_impl_diff_group_add:
assumes d_g: "(diff_group_add_pert_hom_bound_exist op -
(λx::'a::diff_group_add_pert_hom_bound_exist. - x) 0 (op +) diff pert hom_oper)"
shows "diff_group_add op -
(λx::'a::diff_group_add_pert_hom_bound_exist. - x) 0 (op +) diff"
using d_g
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_def by fast
text{*The new definition of @{term reduction_class_ext} preserves
the previous definition of reduction in the old approach, @{term reduction}*}
lemma reduction_class_ext_preserves_reduction:
assumes r_c_e: "reduction_class_ext f g"
shows "reduction (diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
(op -) 0 (op +) diff)
(diff_group_functor (λx::'b::diff_group_add. - x) (op -) 0 (op +) diff)
f g hom_oper"
(is "reduction ?D ?C f g hom_oper")
proof (unfold reduction_def reduction_axioms_def, auto)
have dga: "diff_group_add_pert_hom_bound_exist op - uminus (0::'a) op + diff pert hom_oper"
using reduction_class_ext_impl_diff_group_add_pert_hom_bound_exist [OF r_c_e] .
show "diff_group ?D"
using diff_group_functor_preserves [of "op -" uminus "(0::'a)" "op +" diff]
diff_group_add_pert_hom_bound_exist_impl_diff_group_add [OF dga] by simp
next
show "diff_group ?C"
using r_c_e diff_group_functor_preserves [of "op -" uminus "(0::'b)" "op +" diff]
unfolding reduction_class_ext_def [of f g] by simp
next
show "f ∈ hom_diff ?D ?C"
using r_c_e homo_diff_preserves_hom_diff [of f]
unfolding reduction_class_ext_def [of f g] by simp
next
show "g ∈ hom_diff ?C ?D"
using r_c_e homo_diff_preserves_hom_diff [of g]
unfolding reduction_class_ext_def [of f g] by simp
next
show "hom_oper ∈ hom_completion ?D ?D"
using diff_group_add_pert_hom.h_hom_ab
[of "op -" uminus "(0::'a)" "op +" diff pert hom_oper]
using homo_ab_preserves_hom_completion [of "(λx::'a. h x)"]
using r_c_e
unfolding hom_completion_def
unfolding hom_def
unfolding completion_fun2_def
unfolding completion_def
unfolding reduction_class_ext_def
unfolding diff_group_functor_def
unfolding diff_group_add_pert_hom_bound_exist_def by auto
next
show "(λx. h x) o (λx. h x) = (λx::'a. monoid.one ?D)"
using diff_group_add_pert_hom.h_nilpot
[of "op -" uminus "(0::'a)" "op +" diff pert hom_oper]
using r_c_e
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding zero_fun_def
unfolding reduction_class_ext_def
unfolding diff_group_functor_def by simp
next
show "f o g = (λx::'b. if x ∈ carrier ?C then id x else monoid.one ?C)"
using r_c_e
unfolding reduction_class_ext_def
unfolding diff_group_functor_def expand_fun_eq by simp
next
show "f o (λx. h x) = (λx::'a. monoid.one ?C)"
using r_c_e
unfolding reduction_class_ext_def diff_group_functor_def zero_fun_def
by simp
next
show "(λx. h x) o g = (λx::'b. monoid.one ?D)"
using r_c_e
unfolding reduction_class_ext_def diff_group_functor_def zero_fun_def
by simp
next
show "(λx::'a. if x ∈ carrier ?D then monoid.mult ?D ((g o f) x)
(if x ∈ carrier ?D then monoid.mult ?D ((diff_group.diff ?D o hom_oper) x)
((hom_oper o diff_group.diff ?D) x) else monoid.one ?D)
else monoid.one ?D) =
(λx::'a. if x ∈ carrier ?D then id x else monoid.one ?D)"
using r_c_e
unfolding reduction_class_ext_def
unfolding diff_group_functor_def
unfolding plus_fun_def
by (auto simp add: expand_fun_eq add_assoc)
qed
text{*The new definition of perturbation, included in the definition
of @{term diff_group_add_pert}, also preserves the old definition
of perturbation, @{term "analytic_part_local.pert"}*}
lemma diff_group_add_pert_hom_bound_exist_preserves_pert:
assumes diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist (op -)
(λx::'a::diff_group_add_pert_hom_bound_exist. - x) 0 (op +) diff pert hom_oper"
shows "pert ∈ analytic_part_local.pert
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) (op -) 0 (op +) diff)"
(is "pert ∈ analytic_part_local.pert ?D")
proof (unfold pert_def, auto)
show "pert ∈ hom_completion ?D ?D"
using diff_group_add_pert_hom_bound_exist
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding diff_group_functor_def
unfolding monoid_functor_def
unfolding hom_completion_def
unfolding completion_fun2_def completion_def hom_def by simp
next
have diff_group_add: "diff_group_add (op -) uminus (0::'a) op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
show "diff_group (|carrier = carrier ?D, mult = mult ?D, one = one ?D,
diff_group.diff = λx::'a. if x ∈ carrier ?D
then mult ?D (diff_group.diff ?D x) (δ x) else one ?D|)),"
using diff_group_add_pert_hom_bound_exist
using diff_group_functor_preserves [of "op -" uminus "(0::'a)" "op +" "diff + pert"]
unfolding plus_fun_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def diff_group_functor_def by auto
qed
text{*From the premises stated in @{term diff_group_add_pert_hom_bound_exist},
@{term [locale=diff_group_add_pert_hom_bound_exist] α}
is nilpotent*}
lemma α_locally_nilpotent:
assumes diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist (op -)
(λx::'a::diff_group_add_pert_hom_bound_exist. - x) 0 (op +) diff pert hom_oper"
shows "(α^(local_bound α x)) (x::'a::diff_group_add_pert_hom_bound_exist) = 0"
unfolding diff_group_add_pert_hom_bound_exist_impl_local_bound_is_Least
[OF diff_group_add_pert_hom_bound_exist, of x]
proof (rule LeastI_ex)
show "∃k. (α ^ k) x = (0::'a)"
proof -
obtain n where n_bound: "(α^ n) (x::'a::diff_group_add_pert_hom_bound_exist) = 0"
using diff_group_add_pert_hom_bound_exist_impl_local_bounded_func_alpha
[OF diff_group_add_pert_hom_bound_exist]
unfolding local_bounded_func_def by auto
then show ?thesis using exI by auto
qed
qed
text{*The algebraic structure given by the endomorphisms of a
@{text "diff_group_add"} with suitable operations is a ring*}
lemma (in group_add) shows "op - = (λx y. x + (- y))"
unfolding expand_fun_eq unfolding diff_minus by simp
lemma (in diff_group_add) hom_completion_ring:
shows "ring (|carrier = hom_completion
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff),
mult = op o,
one = λx::'a. if x ∈ carrier (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff) then id x
else one (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff),
zero = λx::'a. if x ∈ carrier (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)
then one (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)
else one (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff),
add = λ(f::'a => 'a) (g::'a => 'a) x::'a.
if x ∈ carrier (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff) then
mult (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff) (f x) (g x)
else one (diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)|)),"
using diff_group_functor_preserves [OF prems]
using comm_group.hom_completion_ring
[of "(diff_group_functor (λx::'a. - x) op - 0 (op +) diff)"]
using diff_minus
unfolding diff_group_def by simp
lemma homo_ab_is_hom_completion:
assumes homo_ab_f: "homo_ab f"
and diff_group_add: "diff_group_add (op -)
(λx::'a::diff_group_add. - x) 0 (op +) diff"
shows "f ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)"
using homo_ab_f
using diff_group_add
unfolding hom_completion_def
unfolding homo_ab_def
unfolding diff_group_functor_def
unfolding hom_def
unfolding completion_fun2_def
unfolding completion_def by auto
lemma hom_completion_is_homo_ab:
assumes f_hom_compl: "f ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)"
and diff_group_add: "diff_group_add (op -) (λx::'a::diff_group_add. - x) 0 (op +) diff"
shows "homo_ab f"
using f_hom_compl
using diff_group_add
unfolding hom_completion_def
unfolding homo_ab_def
unfolding diff_group_functor_def
unfolding hom_def
unfolding completion_fun2_def
unfolding completion_def by auto
lemma hom_completion_equiv_homo_ab:
assumes diff_group_add: "diff_group_add (op -) (λx::'a::diff_group_add. - x) 0 (op +) diff"
shows "homo_ab f <-> f ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)"
using homo_ab_is_hom_completion [of f]
using hom_completion_is_homo_ab [of f]
using diff_group_add by auto
text{*Equivalence between the definition of power in the Isabelle Algebra Library,
@{term nat_pow_def}, over the ring of endomorphisms,
and the definition of power for functions, definition @{term fun_pow}*}
definition ring_hom_compl :: "('a diff_group) => ('a => 'a) ring"
where "ring_hom_compl D == (|carrier = hom_completion D D,
mult = op o,
one = λx::'a. if x ∈ carrier D then id x else one D,
zero = λx::'a. if x ∈ carrier D then one D else one D,
add = λ(f::'a => 'a) (g::'a => 'a) x::'a. if x ∈ carrier D then mult D (f x) (g x) else one D|)),"
(*abbreviation "ring_hom D D == (|carrier = hom_completion D D, mult = op o,
one = λx::'a. if x ∈ carrier D then id x else one D,
zero = λx::'a. if x ∈ carrier D then one D else one D,
add = λ(f::'a => 'a) (g::'a => 'a) x::'a. if x ∈ carrier D then mult D (f x) (g x) else one D|)),"*)
lemma ring_nat_pow_equiv_funpow:
assumes diff_group_add: "diff_group_add (op -) (λx::'a::diff_group_add. - x) 0 (op +) diff"
and f_hom_completion: "f ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)"
shows "f (^)ring_hom_compl (diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff) (n::nat) = f^n"
(is "f (^)?R n = f^n")
proof (induct n)
case 0
show "f(^)?R (0::nat) = f^0"
unfolding ring_hom_compl_def
unfolding nat_pow_def
unfolding diff_group_functor_def expand_fun_eq by auto
next
case Suc
fix n :: nat
assume hypo: "f (^)?R n = f^n"
show "f (^)?R (Suc n) = f^(Suc n)"
proof -
have " f^(Suc n) = f o (f^n)" by simp
also have "… = mult ?R (f (^)?R (1::nat)) (f (^)?R n)"
using hypo analytic_part_local.monoid.nat_pow_1 [of ?R f]
using f_hom_completion
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def ring_hom_compl_def by simp
also have "… = f (^)?R (1 + n)"
using monoid.nat_pow_mult [of ?R f 1 n]
using f_hom_completion diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def ring_hom_compl_def by simp
also have "… = f (^)?R (Suc n)" by simp
finally show ?thesis by simp
qed
qed
text{*Equivalence between the @{text "uminus"} definition in the ring of endomorphisms,
and the @{thm fun_Compl_def}*}
lemma minus_ring_homo_equal_uminus_fun:
assumes diff_group_add: "diff_group_add (op -) (λx::'a::diff_group_add. - x) 0 (op +) diff"
and homo_ab_f: "homo_ab f"
shows "\<ominus>ring_hom_compl (diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff) (f::'a::diff_group_add => 'a) = - f"
(is "\<ominus>?R f = - f")
using diff_group_add.hom_completion_ring [OF diff_group_add]
using abelian_group.minus_equality [of ?R f "- f"]
using homo_ab_is_hom_completion [OF homo_ab_f diff_group_add]
using homo_ab_is_hom_completion
[OF ab_group_add_impl_uminus_fun_closed
[OF _ homo_ab_f]]
using diff_group_add
unfolding ring_hom_compl_def
[of "diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff"]
unfolding Ring.ring_def
unfolding abelian_group_def
unfolding diff_group_add_def
unfolding ab_group_add_def
unfolding ab_group_add_axioms_def
unfolding fun_Compl_def
unfolding plus_fun_def zero_fun_def
unfolding diff_group_functor_def expand_fun_eq by auto
lemma minus_ring_hom_completion_equal_uminus_fun:
assumes diff_group_add: "diff_group_add (op -) (λx::'a::diff_group_add. - x) 0 (op +) diff"
and f_hom_completion: "f ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff)
(diff_group_functor (λx::'a. - x) (op -) 0 (op +) diff)"
shows "\<ominus>ring_hom_compl (diff_group_functor (λx::'a::diff_group_add. - x) (op -) 0 (op +) diff) f = - f"
(is "\<ominus>?R f = - f")
using minus_ring_homo_equal_uminus_fun
using hom_completion_equiv_homo_ab
using diff_group_add
using f_hom_completion by auto
lemma α_in_hom_completion:
assumes diff_group_add_pert_hom:
"diff_group_add_pert_hom (op -) (λx::'a::diff_group_add_pert_hom. - x)
0 op + diff pert hom_oper"
shows "α ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add_pert_hom. - x) op - 0 op + diff)
(diff_group_functor (λx::'a. - x) op - 0 op + diff)"
(is "α ∈ hom_completion ?D ?D")
proof -
let ?R = "ring_hom_compl ?D"
have diff_group_add: "diff_group_add op - uminus (0::'a) op + diff"
using diff_group_add_pert_hom by (intro_locales)
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using diff_group_add_pert_hom
unfolding ring_hom_compl_def
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def completion_def
unfolding diff_group_functor_def by auto
have deltah_in_R: "pert o hom_oper ∈ carrier ?R"
using delta_in_R
using h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of "?R" "pert" "hom_oper"]
unfolding Ring.ring_def ring_hom_compl_def by simp
show ?thesis
using deltah_in_R
using abelian_group.a_inv_closed [OF _ deltah_in_R]
using diff_group_add.hom_completion_ring [OF diff_group_add]
using minus_ring_hom_completion_equal_uminus_fun
[of "pert o hom_oper", OF diff_group_add]
unfolding ring_hom_compl_def α_def Ring.ring_def fun_Compl_def by simp
qed
lemma β_in_hom_completion:
assumes diff_group_add_pert_hom:
"diff_group_add_pert_hom op - (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
0 op + diff pert hom_oper"
shows "β ∈ hom_completion
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(diff_group_functor (λx::'a. - x) op - 0 op + diff)"
(is "β ∈ hom_completion ?D ?D")
proof -
let ?R = "ring_hom_compl ?D"
have diff_group_add: "diff_group_add op - uminus (0::'a) op + diff"
using diff_group_add_pert_hom by (intro_locales)
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using diff_group_add_pert_hom
unfolding ring_hom_compl_def
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def completion_def
unfolding diff_group_functor_def by auto
have hdelta_in_R: "hom_oper o pert ∈ carrier ?R"
using delta_in_R
using h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of "?R" "hom_oper" "pert"]
unfolding Ring.ring_def ring_hom_compl_def by simp
show ?thesis
using hdelta_in_R
using abelian_group.a_inv_closed [OF _ hdelta_in_R]
using diff_group_add.hom_completion_ring [OF diff_group_add]
using minus_ring_hom_completion_equal_uminus_fun
[of "hom_oper o pert", OF diff_group_add]
unfolding ring_hom_compl_def β_def Ring.ring_def fun_Compl_def by simp
qed
text{*Our previous deinition of @{term "reduction_class_ext"}
satisfies the definition of the locale @{term "local_nilpotent_term"}*}
lemma reduction_class_ext_preserves_local_nilpotent_term:
assumes reduction_class_ext_f_g:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist => 'b::diff_group_add) g"
shows "local_nilpotent_term
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
α (local_bound α)"
(is "local_nilpotent_term ?D ?R α (local_bound α)")
proof (intro_locales)
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 op + diff pert hom_oper"
using reduction_class_ext_f_g
unfolding reduction_class_ext_def [of f g] by simp
then have diff_group_add_pert_hom:
"diff_group_add_pert_hom op - (λx::'a. - x) 0 op + diff pert hom_oper"
unfolding diff_group_add_pert_hom_bound_exist_def by simp
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist]
by simp
show "monoid ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def comm_monoid_def by fast
show "comm_monoid_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def comm_monoid_def by fast
show "group_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def group_def by simp
show "diff_group_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def by simp
show "abelian_monoid ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def Ring.ring_def abelian_group_def by simp
show "abelian_group_axioms ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def Ring.ring_def abelian_group_def by simp
show "ring_axioms ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def ring_hom_compl_def by simp
show "monoid ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def abelian_group_def ring_hom_compl_def by simp
show "ring_endomorphisms_axioms ?D ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def ring_endomorphisms_axioms_def by simp
show "local_nilpotent_term_axioms ?D ?R α (local_bound α)"
proof (unfold local_nilpotent_term_axioms_def, intro conjI)
show alpha_in_R: "α ∈ carrier ?R"
using α_in_hom_completion [OF diff_group_add_pert_hom]
unfolding α_def Ring.ring_def ring_hom_compl_def by simp
show "∀x ∈ carrier ?D. (α (^)?R (local_bound α x)) x = one ?D"
proof (rule ballI)
fix x
assume x_in_D: "x ∈ carrier ?D"
show "(α (^)?R (local_bound α x)) x = monoid.one ?D"
proof -
have "(α (^)?R (local_bound α x)) x = (α^(local_bound α x)) x"
using ring_nat_pow_equiv_funpow [OF diff_group_add, of α] alpha_in_R
unfolding ring_hom_compl_def by simp
also have "(α ^ local_bound α (x::'a::diff_group_add_pert_hom_bound_exist)) x = 0"
using α_locally_nilpotent [OF diff_group_add_pert_hom_bound_exist, of "x::'a"]
by simp
also have "… = one ?D" unfolding diff_group_functor_def by simp
finally show ?thesis by simp
qed
qed
show "∀x::'a. (local_bound α x) = (LEAST n::nat. (α (^)?R n) x = one ?D)"
using diff_group_add_pert_hom_bound_exist_impl_local_bounded_func_alpha
[OF diff_group_add_pert_hom_bound_exist]
using local_bounded_func_impl_terminates_loop [of "α::'a => 'a"]
using local_bound_correct [of "α::'a => 'a"]
using ring_nat_pow_equiv_funpow [OF diff_group_add, of "α:: 'a => 'a"]
using alpha_in_R
unfolding ring_hom_compl_def diff_group_functor_def by auto
qed
qed
text{*The following lemma states that the @{term reduction_class_ext} definition together
with @{term local_bound_exists} satisifies the premises of the @{thm BPL.BPL}.*}
text{*In addition to this result, we also have to prove later that the definitions
given in this file for @{term f'}, @{term g'}, @{term Φ},
are equivalent to the ones given inside of the local BPL*}
lemma reduction_class_ext_preserves_BPL:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist => 'b::diff_group_add) g"
shows "BPL
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper
(diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
f g pert
(local_bound α)"
(is "BPL ?D ?R hom_oper ?C f g pert (local_bound α)")
proof (intro_locales)
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] ..
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
show "monoid ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def
unfolding comm_monoid_def by fast
show "comm_monoid_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def
unfolding comm_monoid_def by fast
show "group_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def comm_group_def group_def by fast
show "diff_group_axioms ?D"
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def ..
have diff_group_add_C: "diff_group_add op - (λx::'b. - x) 0 op + diff"
using r_c_e
unfolding reduction_class_ext_def by simp
show "monoid ?C"
using diff_group_functor_preserves [OF diff_group_add_C]
unfolding diff_group_def
unfolding comm_group_def
unfolding comm_monoid_def by fast
show "comm_monoid_axioms ?C"
using diff_group_functor_preserves [OF diff_group_add_C]
unfolding diff_group_def
unfolding comm_group_def
unfolding comm_monoid_def by fast
show "group_axioms ?C"
using diff_group_functor_preserves [OF diff_group_add_C]
unfolding diff_group_def
unfolding comm_group_def
unfolding group_def by fast
show "diff_group_axioms ?C"
using diff_group_functor_preserves [OF diff_group_add_C]
unfolding diff_group_def by fast
show "abelian_monoid ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def
unfolding Ring.ring_def
unfolding abelian_group_def by fast
show "abelian_group_axioms ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def
unfolding abelian_group_def
unfolding ring_hom_compl_def by fast
show "ring_axioms ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def
unfolding Ring.ring_def by fast
show "monoid ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding Ring.ring_def
unfolding abelian_group_def
unfolding ring_hom_compl_def by fast
show "ring_endomorphisms_axioms ?D ?R"
using diff_group_add.hom_completion_ring [OF diff_group_add]
unfolding ring_hom_compl_def
unfolding ring_endomorphisms_axioms_def by fast
show "lemma_2_2_14_axioms ?D ?R (λx. h x)"
proof (unfold lemma_2_2_14_axioms_def ring_hom_compl_def, simp, intro conjI)
show "hom_oper ∈ hom_completion ?D ?D"
using r_c_e
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by simp
show "(λx. h x) o (λx. h x) = (λx::'a. one ?D)"
using r_c_e
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding zero_fun_def
unfolding diff_group_functor_def by simp
show "(λx. h x) o diff_group.diff ?D o (λx. h x) = (λx. h x)"
unfolding diff_group_functor_def
apply simp
using hdh_eq_h [OF r_c_e] .
qed
show "reduction_axioms ?D ?C f g (λx. h x)"
using reduction_class_ext_preserves_reduction [OF r_c_e]
unfolding reduction_def by fast
show "alpha_beta_axioms ?D (λx. δ x)"
using diff_group_add_pert_hom_bound_exist_preserves_pert
[OF diff_group_add_pert_hom_bound_exist]
unfolding alpha_beta_axioms_def .
show "local_nilpotent_term_axioms
?D ?R (\<ominus>?R mult ?R (λx. δ x) (λx. h x)) (local_bound α)"
proof -
have delta_in_R: "(λx. δ x) ∈ carrier ?R"
and h_in_R: "(λx. h x) ∈ carrier ?R"
using r_c_e
unfolding ring_hom_compl_def
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by simp_all
have deltah_in_R: "(λx. δ x) o (λx. h x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "λx. δ x" "λx. h x"]
unfolding ring_hom_compl_def
unfolding Ring.ring_def by simp
have minus_eq: "(\<ominus>?R mult ?R (λx. δ x) (λx. h x))
= - ((λx. δ x) o (λx. h x))"
using deltah_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using abelian_group.a_inv_closed [OF _ deltah_in_R]
using minus_ring_hom_completion_equal_uminus_fun
[OF diff_group_add, of "(λx. δ x) o (λx. h x)"]
unfolding ring_hom_compl_def by simp
show ?thesis
using reduction_class_ext_preserves_local_nilpotent_term
[OF r_c_e]
unfolding minus_eq
unfolding local_nilpotent_term_def
unfolding α_def
unfolding fun_Compl_def unfolding o_apply ..
qed
qed
text{*The definition of @{term reduction_class_ext} satisfies
the definition of the locale @{term "lemma_2_2_15"}.*}
lemma reduction_class_ext_preserves_lemma_2_2_15:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "lemma_2_2_15
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper (diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
f g pert
(local_bound α)"
using reduction_class_ext_preserves_BPL [OF r_c_e]
unfolding BPL_def
unfolding lemma_2_2_17_def
unfolding proposition_2_2_16_def ..
text{*The definition of @{term reduction_class_ext} satisfies
the definiton of the locale @{term local_nilpotent_alpha}*}
lemma reduction_class_ext_preserves_local_nilpotent_alpha:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_alpha
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
(diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
f g hom_oper pert
(local_bound α)"
using reduction_class_ext_preserves_BPL [OF r_c_e]
unfolding BPL_def
unfolding lemma_2_2_17_def
unfolding proposition_2_2_16_def
unfolding lemma_2_2_15_def by fast
text{*The definition @{term "(λx::'a::diff_group_add_pert_hom_bound_exist.
fin_sum α (local_bound α x) x)"}
in @{term reduction_class_ext} is equivalent to the previous definition of
@{term [locale=local_nilpotent_term] power_series}
in locale @{term local_nilpotent_term}.*}
lemma reduction_class_ext_preserves_power_series:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_term.power_series
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
α
(local_bound α) = (λx::'a. fin_sum α (local_bound α x) x)"
(is "local_nilpotent_term.power_series ?D ?R α (local_bound α)
= (λx. fin_sum α (local_bound α x) x)")
proof (unfold expand_fun_eq, rule allI)
fix x :: 'a
show "local_nilpotent_term.power_series ?D ?R α (local_bound α) x
= fin_sum α (local_bound α x) x"
proof -
have local_nilpotent_term: "local_nilpotent_term ?D ?R α (local_bound α)"
using reduction_class_ext_preserves_local_nilpotent_term [OF r_c_e] .
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] ..
have diff_group_add_pert_hom:
"diff_group_add_pert_hom op - (λx::'a. - x) 0 op + diff pert hom_oper"
using diff_group_add_pert_hom_bound_exist
by (intro_locales)
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have "local_nilpotent_term.power_series ?D ?R α (local_bound α) x
= (\<Otimes>?Di::nat∈{..local_bound α x}. (α (^)?R i) x)"
using local_nilpotent_term.power_series_def [OF local_nilpotent_term]
by simp
also have "(\<Otimes>?Di::nat∈{..local_bound α x}. (α (^)?R i) x)
= (\<Otimes>?Di::nat∈{..local_bound α x}. (α^i) x)"
unfolding ring_nat_pow_equiv_funpow [OF diff_group_add
α_in_hom_completion [OF diff_group_add_pert_hom]] ..
also have "… = fin_sum α (local_bound α x) x"
proof (induct "local_bound α x")
case 0
{
have "(\<Otimes>?Di::nat∈{..0::nat}. (α^i) x) = (α^(0::nat)) x"
using comm_monoid.finprod_0 [of ?D]
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def
unfolding comm_group_def
unfolding diff_group_functor_def by simp
also have "… = fin_sum α (0::nat) x" by simp
finally show "(\<Otimes>?Di::nat∈{..0::nat}. (α^i) x) = fin_sum α (0::nat) x" .
}
next
case Suc
{
fix n :: nat
assume hypo: "(\<Otimes>?Di::nat∈{..n}. (α^i) x) = fin_sum α n x"
have "(\<Otimes>?Di::nat∈{..Suc n}. (α^i) x)
= monoid.mult ?D ((α^(Suc n)) x) (\<Otimes>?Di::nat∈{..n}. (α^i) x)"
using comm_monoid.finprod_Suc [of ?D]
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def
unfolding comm_group_def
unfolding diff_group_functor_def by simp
also have "… = monoid.mult ?D ((α^(Suc n)) x) (fin_sum α n x)"
unfolding hypo ..
also have "… = ((α^(Suc n)) x) + (fin_sum α n x)"
unfolding diff_group_functor_def
unfolding monoid.select_convs (1) ..
also have "… = ((α^(Suc n)) + (fin_sum α (n))) x"
unfolding plus_fun_def [of "((α::'a => 'a)^(Suc n))" "(fin_sum α (n))"] ..
also have "… = (fin_sum α (Suc n) x)"
unfolding fin_sum.simps (2) ..
finally
show "(\<Otimes>?Di::nat∈{..Suc (n::nat)}. (α^i) (x::'a)) = fin_sum α (Suc n) x" .
}
qed
finally show ?thesis .
qed
qed
text{*The definition of @{thm Φ_def} is equivalent to the previous definition
of @{term [locale=local_nilpotent_alpha] Φ}
in @{term "locale_nilpotent_alpha"}*}
lemma reduction_class_ext_preserves_Φ:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_alpha.Φ
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper
pert
(local_bound α) = Φ"
(is "local_nilpotent_alpha.Φ ?D ?R hom_oper pert (local_bound α) = Φ")
unfolding local_nilpotent_alpha.phi_def
[OF reduction_class_ext_preserves_local_nilpotent_alpha
[OF r_c_e]]
unfolding local_nilpotent_term.power_series_def [OF _, of x]
proof -
show "local_nilpotent_term.power_series ?D ?R
(\<ominus>?R monoid.mult ?R pert hom_oper) (local_bound α) = Φ"
proof -
have "local_nilpotent_term.power_series ?D ?R
(\<ominus>?R monoid.mult ?R (λx. δ x) (λx. h x)) (local_bound α) =
local_nilpotent_term.power_series ?D ?R α (local_bound α)"
proof -
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0
op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] by fast
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "(λx. h x) ∈ carrier ?R"
using r_c_e
unfolding ring_hom_compl_def
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by auto
have deltah_in_R: "(λx. δ x) o (λx. h x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "(λx. δ x)" "(λx. h x)"]
unfolding Ring.ring_def ring_hom_compl_def by simp
have minus_equiv: "\<ominus>?R mult ?R (λx. δ x) (λx. h x) = α"
using abelian_group.a_inv_closed [OF _ deltah_in_R]
using diff_group_add.hom_completion_ring [OF diff_group_add]
using minus_ring_hom_completion_equal_uminus_fun
[of "(λx. δ x) o (λx. h x)", OF diff_group_add]
using deltah_in_R
unfolding α_def
unfolding ring_hom_compl_def
unfolding fun_Compl_def by simp
show ?thesis unfolding minus_equiv ..
qed
also have "… = (λx::'a. (fin_sum α (local_bound α x)) x)"
unfolding reduction_class_ext_preserves_power_series
[OF r_c_e] ..
also have "… = Φ" unfolding Φ_def α_def ..
finally show ?thesis .
qed
qed
text{*Now, as a corollary, we prove that the previous definition
of the output @{term [locale=BPL] "f'"} of the @{text "BPL"}, is equivalent
to the definition @{term "f o Φ"}.*}
corollary reduction_class_ext_preserves_output_f:
assumes r_c_e: "reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "f o
local_nilpotent_alpha.Φ
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper
pert
(local_bound α)
= f o Φ"
unfolding reduction_class_ext_preserves_Φ [OF r_c_e] ..
text{*Now, as a corollary, we prove that the previous definition
of the output @{term "h'"} of the @{text "BPL"}, is equivalent
to the definition @{thm "h'_def"}.*}
corollary reduction_class_ext_preserves_output_h:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "lemma_2_2_15.h'
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper
pert
(local_bound α)
= h'"
unfolding lemma_2_2_15.h'_def
[OF reduction_class_ext_preserves_lemma_2_2_15
[OF r_c_e]]
unfolding reduction_class_ext_preserves_Φ [OF r_c_e]
unfolding h'_def
unfolding ring_hom_compl_def
unfolding monoid.select_convs (1) ..
text{*The definition of @{term "reduction_class_ext"} satisfies the
definition of the locale @{text "alpha_beta"}*}
lemma reduction_class_ext_preserves_alpha_beta:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "alpha_beta (diff_group_functor (λx::'a. - x) op - 0 op + diff)
(ring_hom_compl
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff))
(diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
f
g (λx. h x) (λx. δ x)"
using reduction_class_ext_preserves_BPL [OF r_c_e]
unfolding BPL_def
unfolding lemma_2_2_17_def
unfolding proposition_2_2_16_def
unfolding lemma_2_2_15_def
unfolding lemma_2_2_14_def
unfolding local_nilpotent_alpha_def by fast
text{*The new definition of the power series over @{thm "β_def"}
is equivalent to the definition of the power series over @{term "β"}
in the previous version.*}
lemma reduction_class_ext_preserves_beta_bound:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_bounded_func (β::'a::diff_group_add_pert_hom_bound_exist => 'a)"
proof -
let ?D = "(diff_group_functor (λx::'a. - x) op - 0 op + diff)"
let ?R = "ring_hom_compl ?D"
obtain "bound_psi"
where local_nilp_term:
"local_nilpotent_term ?D ?R (alpha_beta.β ?R hom_oper pert) bound_psi"
using local_nilpotent_alpha.bound_psi_exists
[OF reduction_class_ext_preserves_local_nilpotent_alpha
[OF r_c_e]] by auto
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] by fast
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using r_c_e
unfolding ring_hom_compl_def
unfolding reduction_class_ext_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by auto
have hdelta_in_R: "(λx. h x) o (λx. δ x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "(λx. h x)" "(λx. δ x)"]
unfolding Ring.ring_def ring_hom_compl_def by simp
have β_equiv: "alpha_beta.β ?R (λx. h x) (λx. δ x) = β"
proof -
have "alpha_beta.β ?R (λx. h x) (λx. δ x)
= \<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)"
unfolding alpha_beta.beta_def
[OF reduction_class_ext_preserves_alpha_beta
[OF r_c_e]] ..
also have "\<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)
= - ((λx. h x) o (λx. δ x))"
using hdelta_in_R
using minus_ring_hom_completion_equal_uminus_fun
[OF diff_group_add]
unfolding ring_hom_compl_def by simp
finally show ?thesis unfolding β_def .
qed
have lnt: "local_nilpotent_term ?D ?R β bound_psi"
unfolding sym [OF β_equiv]
using local_nilp_term .
have bound_ex:"∀x::'a. ∃n::nat. (β (^)?R n) x = 0"
using lnt
unfolding local_nilpotent_term_def
unfolding local_nilpotent_term_axioms_def
unfolding diff_group_functor_def by auto
have "∀x::'a. ∃n::nat. (β ^ n) x = 0"
using ring_nat_pow_equiv_funpow
[OF diff_group_add β_in_hom_completion]
using diff_group_add_pert_hom_bound_exist
using bound_ex
unfolding diff_group_add_pert_hom_bound_exist_def by simp
then show ?thesis
unfolding local_bounded_func_def .
qed
lemma reduction_class_ext_preserves_power_series_β:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_term.power_series
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
β (local_bound β)
= (λx::'a. fin_sum β (local_bound β x) x)"
(is "local_nilpotent_term.power_series ?D ?R β (local_bound β)
= (λx::'a. fin_sum β (local_bound β x) x)")
proof (unfold expand_fun_eq, rule allI)
fix x :: 'a
show "local_nilpotent_term.power_series ?D ?R β (local_bound β) x
= fin_sum β (local_bound β x) x"
proof -
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist op - (λx::'a. - x) 0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] by fast
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using r_c_e
unfolding reduction_class_ext_def
unfolding ring_hom_compl_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by auto
have hdelta_in_R: "(λx. h x) o (λx. δ x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "(λx. h x)" "(λx. δ x)"]
unfolding ring_hom_compl_def
unfolding Ring.ring_def by simp
have β_equiv: "alpha_beta.β ?R (λx. h x) (λx. δ x) = β"
proof -
have "alpha_beta.β ?R (λx. h x) (λx. δ x)
= \<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)"
unfolding alpha_beta.beta_def
[OF reduction_class_ext_preserves_alpha_beta
[OF r_c_e]] ..
also have "\<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)
= - ((λx. h x) o (λx. δ x))"
using hdelta_in_R
using minus_ring_hom_completion_equal_uminus_fun
[of "(λx. h x) o (λx. δ x)", OF diff_group_add]
unfolding ring_hom_compl_def by simp
finally show ?thesis unfolding β_def .
qed
have bound_equiv: "(λx. LEAST n. (β (^)?R n) x = one ?D) = (local_bound β)"
using local_bounded_func_impl_local_bound_is_Least
[OF reduction_class_ext_preserves_beta_bound
[OF r_c_e]]
using ring_nat_pow_equiv_funpow [OF diff_group_add β_in_hom_completion]
using diff_group_add_pert_hom_bound_exist
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_functor_def by (simp add: expand_fun_eq)
have local_nilpotent_term: "local_nilpotent_term ?D ?R β (local_bound β)"
using local_nilpotent_alpha.nilp_alpha_nilp_beta
[OF reduction_class_ext_preserves_local_nilpotent_alpha
[OF r_c_e]]
using local_nilpotent_alpha.nilp_alpha_nilp_beta
using β_equiv
using bound_equiv by simp
have "local_nilpotent_term.power_series ?D ?R β (local_bound β) x
= (\<Otimes>?Di::nat∈{..local_bound β x}. (β (^)?R i) x)"
unfolding local_nilpotent_term.power_series_def [OF local_nilpotent_term] ..
also have "(\<Otimes>?Di::nat∈{..local_bound β x}. (β (^)?R i) x)
= (\<Otimes>?Di::nat∈{..local_bound β x}. (β^i) x)"
using ring_nat_pow_equiv_funpow [OF diff_group_add β_in_hom_completion]
using diff_group_add_pert_hom_bound_exist
unfolding diff_group_add_pert_hom_bound_exist_def by simp
also have "… = fin_sum β (local_bound β x) x"
proof (induct "local_bound β x")
case 0
{
have "(\<Otimes>?Di::nat∈{..0::nat}. (β^i) x) = (β^(0::nat)) x"
using comm_monoid.finprod_0 [of ?D]
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def
unfolding comm_group_def
unfolding diff_group_functor_def by simp
also have "… = fin_sum β (0::nat) x" by simp
finally show "(\<Otimes>?Di::nat∈{..0::nat}. (β^i) x) = fin_sum β (0::nat) x" by simp
}
next
case Suc
{
fix n :: nat
assume hypo: "(\<Otimes>?Di::nat∈{..n}. (β^i) x) = fin_sum β n x"
have "(\<Otimes>?Di::nat∈{..Suc n}. (β^i) x)
= mult ?D ((β^(Suc n)) x) (\<Otimes>?Di::nat∈{..n}. (β^i) x)"
using comm_monoid.finprod_Suc [of ?D]
using diff_group_functor_preserves [OF diff_group_add]
unfolding diff_group_def
unfolding comm_group_def
unfolding diff_group_functor_def by simp
also have "… = monoid.mult ?D ((β^(Suc n)) x) (fin_sum β n x)"
unfolding hypo ..
also have "… = ((β^(Suc n)) x) + (fin_sum β n x)"
unfolding diff_group_functor_def
unfolding monoid.select_convs (1) ..
also have "… = ((β^(Suc n)) + (fin_sum β (n))) x"
unfolding plus_fun_def [of "((β::'a => 'a)^(Suc n))" "(fin_sum β (n))"] ..
also have "… = (fin_sum β (Suc n) x)" by simp
finally show "(\<Otimes>?Di::nat∈{..Suc (n::nat)}. (β^i) (x::'a))
= fin_sum β (Suc n) x" .
}
qed
finally show ?thesis by simp
qed
qed
text{*As well as the equivalence between both definitions of the power series,
also the definitions of the bounds are equivalent.*}
lemma reduction_class_ext_preserves_bound_psi:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_alpha.bound_psi
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper pert
= (local_bound β)"
(is "local_nilpotent_alpha.bound_psi ?D ?R (λx. h x) (λx. δ x) = (local_bound β)")
proof -
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist
op - (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] by fast
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using r_c_e
unfolding reduction_class_ext_def
unfolding ring_hom_compl_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by auto
have hdelta_in_R: "(λx. h x) o (λx. δ x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "(λx. h x)" "(λx. δ x)"]
unfolding Ring.ring_def ring_hom_compl_def by simp
have "local_nilpotent_alpha.bound_psi ?D ?R (λx. h x) (λx. δ x)
= (λx::'a. LEAST n::nat. (alpha_beta.β ?R (λx. h x) (λx. δ x) (^)?R n) x = one ?D)"
using local_nilpotent_alpha.bound_psi_def
[OF reduction_class_ext_preserves_local_nilpotent_alpha
[OF r_c_e]] by simp
also have "… = (λx::'a. LEAST n::nat. (β (^)?R n) x = one ?D)"
proof -
have β_equiv: "alpha_beta.β ?R (λx. h x) (λx. δ x) = β"
proof -
have "alpha_beta.β ?R (λx. h x) (λx. δ x)
= \<ominus>?R mult ?R (λx. h x) (λx. δ x)"
unfolding alpha_beta.beta_def
[OF reduction_class_ext_preserves_alpha_beta
[OF r_c_e]] ..
also have "\<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)
= - ((λx. h x) o (λx. δ x))"
using hdelta_in_R
using minus_ring_hom_completion_equal_uminus_fun
[of "(λx. h x) o (λx. δ x)", OF diff_group_add]
unfolding ring_hom_compl_def by simp
finally show ?thesis unfolding β_def .
qed
then show ?thesis by simp
qed
also have "… = (λx::'a. LEAST n::nat. (β (^)?R n) x = (0::'a))"
unfolding diff_group_functor_def
unfolding monoid.select_convs ..
also have "… = (λx::'a. LEAST n::nat. (β^n) x = (0::'a))"
using ring_nat_pow_equiv_funpow
[OF diff_group_add β_in_hom_completion]
using diff_group_add_pert_hom_bound_exist
unfolding diff_group_add_pert_hom_bound_exist_def by simp
also have bound_equiv: "… = (local_bound β)"
unfolding expand_fun_eq
unfolding local_bounded_func_impl_local_bound_is_Least
[OF reduction_class_ext_preserves_beta_bound
[OF r_c_e]] by fast
finally show ?thesis .
qed
text{*From the equivalence betwen the power series and the equality of the bounds,
it follows the equivalence between the old and the new definition of
@{term [locale=BPL] "Ψ"}*}
lemma reduction_class_ext_preserves_Ψ:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_alpha.Ψ
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper pert
= Ψ"
(is "local_nilpotent_alpha.Ψ ?D ?R (λx. h x) (λx. δ x) = Ψ")
proof -
have diff_group_add_pert_hom_bound_exist:
"diff_group_add_pert_hom_bound_exist
op - (λx::'a::diff_group_add_pert_hom_bound_exist. - x)
0 op + diff pert hom_oper"
using r_c_e
unfolding reduction_class_ext_def [of f g] by fast
have diff_group_add: "diff_group_add op - (λx::'a. - x) 0 op + diff"
using diff_group_add_pert_hom_bound_exist_impl_diff_group_add
[OF diff_group_add_pert_hom_bound_exist] .
have delta_in_R: "pert ∈ carrier ?R" and h_in_R: "hom_oper ∈ carrier ?R"
using r_c_e
unfolding reduction_class_ext_def
unfolding ring_hom_compl_def
unfolding diff_group_add_pert_hom_bound_exist_def
unfolding diff_group_add_pert_hom_def
unfolding diff_group_add_pert_hom_axioms_def
unfolding diff_group_add_pert_def
unfolding diff_group_add_pert_axioms_def
unfolding hom_completion_def
unfolding hom_def
unfolding Pi_def
unfolding completion_fun2_def
unfolding completion_def
unfolding diff_group_functor_def by auto
have hdelta_in_R: "(λx. h x) o (λx. δ x) ∈ carrier ?R"
using delta_in_R h_in_R
using diff_group_add.hom_completion_ring [OF diff_group_add]
using monoid.m_closed [of ?R "(λx. h x)" "(λx. δ x)"]
unfolding ring_hom_compl_def Ring.ring_def by simp
have "local_nilpotent_alpha.Ψ ?D ?R (λx. h x) (λx. δ x)
= local_nilpotent_term.power_series ?D ?R (alpha_beta.β ?R (λx. h x) (λx. δ x))
(local_nilpotent_alpha.bound_psi ?D ?R (λx. h x) (λx. δ x))"
unfolding local_nilpotent_alpha.psi_def
[OF reduction_class_ext_preserves_local_nilpotent_alpha
[OF r_c_e]] ..
also have "…
= local_nilpotent_term.power_series ?D ?R (alpha_beta.β ?R
(λx. h x) (λx. δ x)) (local_bound β)"
using reduction_class_ext_preserves_bound_psi [OF r_c_e] by simp
also have "… = local_nilpotent_term.power_series ?D ?R β (local_bound β)"
proof -
have β_equiv: "alpha_beta.β ?R (λx. h x) (λx. δ x) = β"
proof -
have "alpha_beta.β ?R (λx. h x) (λx. δ x)
= \<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x)"
using alpha_beta.beta_def
[OF reduction_class_ext_preserves_alpha_beta
[OF r_c_e]] .
also have "\<ominus>?R monoid.mult ?R (λx. h x) (λx. δ x) = β"
using hdelta_in_R
using minus_ring_hom_completion_equal_uminus_fun
[of "(λx. h x) o (λx. δ x)", OF diff_group_add]
unfolding ring_hom_compl_def by (fold β_def, simp)
finally show ?thesis .
qed
then show ?thesis by simp
qed
also have "… = (λx. fin_sum β (local_bound β x) x)"
using reduction_class_ext_preserves_power_series_β [OF r_c_e] .
also have "… = Ψ" unfolding Ψ_def β_def ..
finally show ?thesis .
qed
text{*Now, as a corollary, we prove the equivalence between the previous
definition of the output @{term g} of the BPL,
and the one in this new approach*}
corollary reduction_class_ext_preserves_output_g:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "local_nilpotent_alpha.Ψ
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper pert o g
= Ψ o g"
unfolding reduction_class_ext_preserves_Ψ [OF r_c_e] ..
text{*It also follows the equality of the previous definition
of @{term [locale=BPL] "differC'"} and the new definition, @{thm "dC'_def"}*}
corollary reduction_class_ext_preserves_output_dC:
assumes r_c_e:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "(λx::'b.
if x ∈ carrier (diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
then mult (diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff)
(diff_group.diff (diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff) x)
((f o pert o
(local_nilpotent_alpha.Ψ
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl (diff_group_functor (λx::'a. - x) op - 0 op + diff))
hom_oper pert) o g) x) else one (diff_group_functor (λx::'b. - x) op - 0 op + diff))
= dC' f g"
unfolding reduction_class_ext_preserves_Ψ
[OF r_c_e]
unfolding dC'_def [of f g]
unfolding diff_group_functor_def
unfolding plus_fun_def by simp
text{*Now, from he previous equivalences, we are ready to give the proof of the
@{thm [locale=BPL] "BPL"}
with the new introduced definitions in terms of classes:*}
lemma assumes reduction_class_ext_f_g:
"reduction_class_ext (f::'a::diff_group_add_pert_hom_bound_exist
=> 'b::diff_group_add) g"
shows "reduction
(lemma_2_2_15.D'
(diff_group_functor (λx::'a::diff_group_add_pert_hom_bound_exist. - x) op - 0 op + diff)
(ring_hom_compl
(diff_group_functor (λx::'a. - x) op - 0 op + diff)) pert)
(|carrier = carrier (diff_group_functor (λx::'b::diff_group_add. - x) op - 0 op + diff),
mult = mult (diff_group_functor (λx::'b. - x) op - 0 op + diff),
one = one (diff_group_functor (λx::'b. - x) op - 0 op + diff),
diff_group.diff = dC' f g|)),
(f' f)
(g' g)
(h')"
using BPL.BPL
[OF reduction_class_ext_preserves_BPL
[OF reduction_class_ext_f_g]]
unfolding reduction_class_ext_preserves_output_f [OF reduction_class_ext_f_g]
unfolding reduction_class_ext_preserves_output_g [OF reduction_class_ext_f_g]
unfolding reduction_class_ext_preserves_output_h [OF reduction_class_ext_f_g]
unfolding reduction_class_ext_preserves_output_dC [OF reduction_class_ext_f_g]
unfolding f'_def [of f]
unfolding g'_def [of g]
unfolding h'_def
unfolding dC'_def [of f g] .
end
lemma
d (d x) = (0::'a)
lemma
α = - (diff_group_add_pert_class.pert o hom_oper)
lemma local_bound_gen_simp:
local_bound_gen f x ac =
(if x ≠ (0::'a) then local_bound_gen f (f x) (ac + 1) else ac)
lemma
local_bound f (0::'a) = 0
lemma
x ≠ (0::'a) ==> local_bound (λx. 0::'a) x = 1
lemma local_bounded_func_impl_terminates_loop:
local_bounded_func f = (∀x. terminates (λy. y ≠ (0::'a), f, x))
lemma LEAST_local_bound_0:
(LEAST n. (f ^ n) (0::'a) = (0::'a)) = 0
lemma local_bound_gen_correct:
terminates (λy. y ≠ (0::'a), f, x)
==> local_bound_gen f x m = m + (LEAST n. (f ^ n) x = (0::'a))
lemma local_bound_correct:
terminates (λy. y ≠ (0::'a), f, x)
==> local_bound f x = (LEAST n. (f ^ n) x = (0::'a))
lemma local_bounded_func_impl_local_bound_is_Least:
local_bounded_func f ==> local_bound f x = (LEAST n. (f ^ n) x = (0::'a))
lemma
local_bound' f x n =
(if (f ^ n) x = (0::'a) then n else local_bound' f x (Suc n))
lemma
While continue f s = (if continue s then While continue f (f s) else s)
lemma diff_group_add_pert_hom_bound_exist_impl_local_bounded_func_alpha:
diff_group_add_pert_hom_bound_exist op - uminus (0::'b) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
==> local_bounded_func α
lemma diff_group_add_pert_hom_bound_exist_impl_local_bound_is_Least:
diff_group_add_pert_hom_bound_exist op - uminus (0::'b) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
==> local_bound α x = (LEAST n. (α ^ n) x = (0::'a))
lemma monoid_add_impl_monoid:
monoid_add zero' plus'
==> monoid (| carrier = UNIV, mult = plus', one = zero' |)
lemma monoid_functor_preserv:
monoid_add zero' plus' ==> monoid (monoid_functor plus' zero')
lemma comm_monoid_add_impl_monoid_add:
comm_monoid_add zero' plus' ==> monoid_add zero' plus'
lemma comm_monoid_add_impl_monoid:
comm_monoid_add zero' plus'
==> monoid (| carrier = UNIV, mult = plus', one = zero' |)
lemma ab_group_add_impl_comm_monoid_add:
ab_group_add uminus' minus' zero' plus' ==> comm_monoid_add zero' plus'
lemma ab_group_class_impl_group:
ab_group_add uminus' minus' zero' plus'
==> group (| carrier = UNIV, mult = plus', one = zero' |)
lemma monoid_functor_preserv_group:
ab_group_add uminus' minus' zero' plus' ==> group (monoid_functor plus' zero')
lemma ab_group_add_impl_comm_group:
ab_group_add uminus' minus' zero' plus'
==> comm_group (| carrier = UNIV, mult = plus', one = zero' |)
lemma monoid_functor_preserv_ab_group:
ab_group_add uminus' minus' zero' plus'
==> comm_group (monoid_functor plus' zero')
lemma diff_group_add_impl_comm_group:
diff_group_add uminus' minus' zero' plus' diff'
==> comm_group (| carrier = UNIV, mult = plus', one = zero' |)
lemma diff_group_add_impl_diff_group:
diff_group_add uminus' minus' zero' prod' diff'
==> diff_group
(| carrier = UNIV, mult = prod', one = zero', diff_group.diff = diff' |)
lemma diff_group_functor_preserves:
diff_group_add minus' uminus' zero' prod' diff'
==> diff_group (diff_group_functor uminus' minus' zero' prod' diff')
lemma homo_ab_apply:
homo_ab f ==> f (a + b) = f a + f b
lemma homo_ab_preserves_hom_completion:
homo_ab f
==> f ∈ hom_completion (monoid_functor op + (0::'a))
(monoid_functor op + (0::'b))
lemma plus_fun_apply:
(f + g) x = f x + g x
lemma homo_ab_plus_closed:
[| comm_monoid_add (0::'a) op +; comm_monoid_add (0::'b) op +; homo_ab x;
homo_ab y |]
==> homo_ab (x + y)
lemma end_comm_monoid_add_closed:
[| comm_monoid_add (0::'a) op +; homo_ab x; homo_ab y |] ==> homo_ab (x + y)
lemma comm_monoid_add_impl_homo_abelian_monoid:
comm_monoid_add (0::'a) op +
==> abelian_monoid
(| carrier = {f. homo_ab f}, mult = op o, one = id, zero = 0, add = op + |)
lemma ab_group_add_impl_uminus_fun_closed:
[| ab_group_add op - uminus (0::'a) op +; homo_ab f |] ==> homo_ab (- f)
lemma ab_group_add_impl_homo_abelian_group_axioms:
ab_group_add op - uminus (0::'a) op +
==> abelian_group_axioms
(| carrier = {f. homo_ab f}, mult = op o, one = id, zero = 0, add = op + |)
lemma homo_monoid:
monoid
(| carrier = {f. homo_ab f}, mult = op o, one = id, zero = 0::'b, add = op + |)
lemma ab_group_add_impl_homo_ring_axioms:
ab_group_add op - uminus (0::'a) op +
==> ring_axioms
(| carrier = {f. homo_ab f}, mult = op o, one = id, zero = 0, add = op + |)
lemma ab_group_add_impl_homo_ring:
ab_group_add op - uminus (0::'a) op +
==> Ring.ring
(| carrier = {f. homo_ab f}, mult = op o, one = id, zero = 0, add = op + |)
lemma homo_diff_preserves_hom_diff:
homo_diff f
==> f ∈ hom_diff
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff)
lemma reduction_class_ext_impl_diff_group_add_pert_hom_bound_exist:
reduction_class_ext f g
==> diff_group_add_pert_hom_bound_exist op - uminus (0::'a) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
lemma reduction_class_ext_impl_diff_group_add:
reduction_class_ext f g
==> diff_group_add op - uminus (0::'b) op + diff_group_add_class.diff
lemma reduction_class_ext_impl_homo_diff_f:
reduction_class_ext f g ==> homo_diff f
lemma reduction_class_ext_impl_homo_diff_g:
reduction_class_ext f g ==> homo_diff g
lemma reduction_class_ext_impl_fg_id:
reduction_class_ext f g ==> f o g = id
lemma reduction_class_ext_impl_gf_dh_hd_id:
reduction_class_ext f g
==> (g o f) + (diff_group_add_class.diff o hom_oper) +
(hom_oper o diff_group_add_class.diff) =
id
lemma reduction_class_ext_impl_fh_0:
reduction_class_ext f g ==> f o hom_oper = 0
lemma reduction_class_ext_impl_hg_0:
reduction_class_ext f g ==> hom_oper o g = 0
lemma hdh_eq_h:
reduction_class_ext f g
==> hom_oper o diff_group_add_class.diff o hom_oper = hom_oper
lemma diff_group_add_pert_hom_bound_exist_impl_diff_group_add:
diff_group_add_pert_hom_bound_exist op - uminus (0::'a) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
==> diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff
lemma reduction_class_ext_preserves_reduction:
reduction_class_ext f g
==> reduction
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) f g
hom_oper
lemma diff_group_add_pert_hom_bound_exist_preserves_pert:
diff_group_add_pert_hom_bound_exist op - uminus (0::'a) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
==> diff_group_add_pert_class.pert
∈ analytic_part_local.pert
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
lemma α_locally_nilpotent:
diff_group_add_pert_hom_bound_exist op - uminus (0::'a) op +
diff_group_add_class.diff diff_group_add_pert_class.pert hom_oper
==> (α ^ local_bound α x) x = (0::'a)
lemma
op - = (λx y. x + - y)
lemma hom_completion_ring:
Ring.ring
(| carrier =
hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff),
mult = op o,
one = λx. if x ∈ carrier
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff)
then id x
else \<one>diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff,
zero =
λx. if x ∈ carrier
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff)
then \<one>diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff
else \<one>diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff,
add = λf g x.
if x ∈ carrier
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff)
then f x ⊗diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff
g x
else \<one>diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff |)
lemma homo_ab_is_hom_completion:
[| homo_ab f;
diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff |]
==> f ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
lemma hom_completion_is_homo_ab:
[| f ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff);
diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff |]
==> homo_ab f
lemma hom_completion_equiv_homo_ab:
diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff
==> homo_ab f =
(f ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff))
lemma ring_nat_pow_equiv_funpow:
[| diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff;
f ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff) |]
==> f (^)ring_hom_compl (diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
n =
f ^ n
lemma minus_ring_homo_equal_uminus_fun:
[| diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff;
homo_ab f |]
==> \<ominus>ring_hom_compl (diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff) f =
- f
lemma minus_ring_hom_completion_equal_uminus_fun:
[| diff_group_add op - uminus (0::'a) op + diff_group_add_class.diff;
f ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff) |]
==> \<ominus>ring_hom_compl (diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff) f =
- f
lemma α_in_hom_completion:
diff_group_add_pert_hom op - uminus (0::'a) op + diff_group_add_class.diff
diff_group_add_pert_class.pert hom_oper
==> α ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
lemma β_in_hom_completion:
diff_group_add_pert_hom op - uminus (0::'a) op + diff_group_add_class.diff
diff_group_add_pert_class.pert hom_oper
==> β ∈ hom_completion
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
lemma reduction_class_ext_preserves_local_nilpotent_term:
reduction_class_ext f g
==> local_nilpotent_term
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
α (local_bound α)
lemma reduction_class_ext_preserves_BPL:
reduction_class_ext f g
==> BPL (diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) f g
diff_group_add_pert_class.pert (local_bound α)
lemma reduction_class_ext_preserves_lemma_2_2_15:
reduction_class_ext f g
==> lemma_2_2_15
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) f g
diff_group_add_pert_class.pert (local_bound α)
lemma reduction_class_ext_preserves_local_nilpotent_alpha:
reduction_class_ext f g
==> local_nilpotent_alpha
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) f g
hom_oper diff_group_add_pert_class.pert (local_bound α)
lemma reduction_class_ext_preserves_power_series:
reduction_class_ext f g
==> local_nilpotent_term.power_series
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
α (local_bound α) =
(λx. fin_sum α (local_bound α x) x)
lemma reduction_class_ext_preserves_Φ:
reduction_class_ext f g
==> local_nilpotent_alpha.Φ
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert (local_bound α) =
Φ
corollary reduction_class_ext_preserves_output_f:
reduction_class_ext f g
==> f o local_nilpotent_alpha.Φ
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert (local_bound α) =
f o Φ
corollary reduction_class_ext_preserves_output_h:
reduction_class_ext f g
==> lemma_2_2_15.h'
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert (local_bound α) =
h'
lemma reduction_class_ext_preserves_alpha_beta:
reduction_class_ext f g
==> alpha_beta
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
(diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) f g
hom_oper diff_group_add_pert_class.pert
lemma reduction_class_ext_preserves_beta_bound:
reduction_class_ext f g ==> local_bounded_func β
lemma reduction_class_ext_preserves_power_series_β:
reduction_class_ext f g
==> local_nilpotent_term.power_series
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
β (local_bound β) =
(λx. fin_sum β (local_bound β x) x)
lemma reduction_class_ext_preserves_bound_psi:
reduction_class_ext f g
==> local_nilpotent_alpha.bound_psi
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert =
local_bound β
lemma reduction_class_ext_preserves_Ψ:
reduction_class_ext f g
==> local_nilpotent_alpha.Ψ
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert =
Ψ
corollary reduction_class_ext_preserves_output_g:
reduction_class_ext f g
==> local_nilpotent_alpha.Ψ
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert o
g =
Ψ o g
corollary reduction_class_ext_preserves_output_dC:
reduction_class_ext f g
==> (λx. if x ∈ carrier
(diff_group_functor uminus op - (0::'b) op +
diff_group_add_class.diff)
then diff_group.diff
(diff_group_functor uminus op - (0::'b) op +
diff_group_add_class.diff)
x ⊗diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff
(f o diff_group_add_pert_class.pert o
local_nilpotent_alpha.Ψ
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff))
hom_oper diff_group_add_pert_class.pert o
g)
x
else \<one>diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff) =
dC' f g
lemma
reduction_class_ext f g
==> reduction
(lemma_2_2_15.D'
(diff_group_functor uminus op - (0::'a) op + diff_group_add_class.diff)
(ring_hom_compl
(diff_group_functor uminus op - (0::'a) op +
diff_group_add_class.diff))
diff_group_add_pert_class.pert)
(| carrier =
carrier
(diff_group_functor uminus op - (0::'b) op +
diff_group_add_class.diff),
mult =
op ⊗diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff,
one = \<one>diff_group_functor uminus op - (0::'b) op + diff_group_add_class.diff,
diff_group.diff = dC' f g |)
(f' f) (g' g) h'