Theory Formal_Power_Series_Ring
section ‹The Hilbert Basis theorem for Formal Power Series›
theory Formal_Power_Series_Ring
imports
"HOL-Library.Extended_Nat"
"HOL-Computational_Algebra.Formal_Power_Series"
"HOL-Algebra.Module"
"HOL-Algebra.Ring_Divisibility"
begin
text ‹We define the ring of formal power series over a domain (idom) as a record to match
HOL-Algebra definitions. We then show that it is a domain for addition and multiplication.
This is immediate with the existing theory from HOL-Analysis.
We then proceed to show the theorem similar to Hilbert's basis theorem but for the
ring of Formal power series.›
subsection ‹Preliminaries definition and lemmas›
context
fixes R::‹'a::{idom} ring› (structure)
defines R:‹R ≡ ⦇carrier = UNIV, monoid.mult = (*), one = 1, zero = 0, add = (+)⦈›
begin
lemma ring_R:‹ring R›
apply(unfold_locales)
using add.right_inverse
by (auto simp add: R mult.assoc ab_semigroup_add_class.add_ac(1)
add.left_commute Units_def add.commute ring_class.ring_distribs(2)
ring_class.ring_distribs(1) exI[of _ "- x" for x])
lemma domain_R:‹domain R›
apply(rule domainI)
apply(rule cringI)
apply (simp add: ring.is_abelian_group ring_R)
apply (metis Groups.mult_ac(2) R monoid.monoid_comm_monoidI
monoid.simps(1) ring.is_monoid ring_R)
apply (simp add: ring.ring_simprules(13) ring_R)
apply (simp add: R)
by (simp add: R)
definition
FPS_ring :: "'a::{idom} fps ring"
where "FPS_ring = ⦇carrier = UNIV, monoid.mult = (*), one = 1, zero = 0, add = (+)⦈"
lemma ring_FPS:‹ring FPS_ring›
apply(rule ringI)
apply(rule abelian_groupI)
apply (simp_all add: FPS_ring_def ab_semigroup_add_class.add_ac(1)
add.left_commute add.commute)
apply (metis ab_group_add_class.ab_left_minus add.commute)
apply(rule monoidI)
by(simp_all add: FPS_ring_def mult.assoc ab_semigroup_add_class.add_ac(1)
add.left_commute add.commute ring_class.ring_distribs(2) ring_class.ring_distribs(1))
lemma cring_FPS:‹cring FPS_ring›
apply(rule cringI)
apply (simp add: ring.is_abelian_group ring_FPS)
apply(rule comm_monoidI)
apply (simp add: ring.ring_simprules(5) ring_FPS)
apply (simp add: ring.ring_simprules(6) ring_FPS)
apply (simp add: ring.ring_simprules(11) ring_FPS)
apply (simp add: ring.ring_simprules(12) ring_FPS)
apply (simp add: FPS_ring_def)
by (simp add: ring.ring_simprules(13) ring_FPS)
lemma domain_FPS:‹domain FPS_ring›
apply(rule domainI)
apply (simp add: cring_FPS)
apply (simp add: FPS_ring_def)
by (simp add: FPS_ring_def)
text ‹valuation over $FPS_ring$›
definition v_subdegree :: "('a::{idom}) fps ⇒ enat" where
"v_subdegree f = (if f = 0 then ∞ else subdegree f)"
definition valuation::‹'a::{idom} fps ⇒ enat› ("ν")where
‹ν x ≡ Sup {enat k |k. x∈ cgenideal FPS_ring (fps_X^k)}›
lemma fps_X_pow_k_ideal_iff:‹cgenideal FPS_ring (fps_X^k) = {x. v_subdegree x ≥ k}›
proof(induct k)
case 0
then show ?case unfolding cgenideal_def
using enat_def zero_enat_def
by (simp add: FPS_ring_def)
next
case (Suc k)
have ‹x∈carrier FPS_ring ⟹ v_subdegree (x*fps_X^r) ≥ r› for r x
apply(cases ‹x=0›)
unfolding v_subdegree_def by(auto)
then show ?case unfolding cgenideal_def v_subdegree_def FPS_ring_def
apply(safe)
apply(auto simp:FPS_ring_def) [1]
by (metis (mono_tags, opaque_lifting) UNIV_I enat_ord_simps(1) fps_shift_times_fps_X_power
monoid.select_convs(1) mult_zero_left partial_object.select_convs(1))
qed
lemma valuation_miscs_1:assumes h1:‹f ∈carrier FPS_ring›
shows ‹(valuation f) = (∞::enat) ⟷ f = 0›
apply(safe)
unfolding valuation_def apply(subst (asm) fps_X_pow_k_ideal_iff)
apply (smt (verit, best) Sup_least infinity_ileE mem_Collect_eq v_subdegree_def)
apply(subst fps_X_pow_k_ideal_iff)
unfolding v_subdegree_def
unfolding enat_def apply(clarsimp)
by (smt (verit, ccfv_threshold) Suc_ile_eq Sup_le_iff enat.exhaust enat_def enat_ord_simps(2)
mem_Collect_eq nat_less_le order.refl)
lemma valuation_miscs_0:
shows ‹valuation f = Inf {enat n |n. fps_nth f n ≠ 0}›
proof(cases ‹f=0›)
case 1:True
have f1:‹valuation f = ∞›
using 1 valuation_miscs_1
by (simp add: FPS_ring_def)
have f0:‹{enat n |n. fps_nth f n ≠ 0} = {}›
by (simp add: "1")
show ?thesis
apply(subst f0)
unfolding Inf_enat_def using f1 by(auto)
next
case 2:False
have f0:‹fps_nth f n ≠ 0 ⟹ f ∉ cgenideal FPS_ring (fps_X^(Suc n))› for n
apply(subst fps_X_pow_k_ideal_iff)
unfolding v_subdegree_def
using not_less_eq_eq subdegree_leI by auto
then have ‹f ∉ cgenideal FPS_ring (fps_X^(n)) ⟹ ∀i≥n. f ∉ cgenideal FPS_ring (fps_X^(i))›
for n
by (simp add: 2 fps_X_pow_k_ideal_iff v_subdegree_def)
with f0 have f2:‹fps_nth f n ≠ 0 ⟹ valuation f ≤ n› for n
unfolding valuation_def
by (smt (verit, del_insts) Sup_le_iff enat_ord_simps(1) mem_Collect_eq not_less_eq_eq)
then have ‹valuation f = v_subdegree f›
by (smt (verit, best) "2" Orderings.order_eq_iff Sup_le_iff fps_X_pow_k_ideal_iff
mem_Collect_eq v_subdegree_def valuation_def)
then show ?thesis unfolding v_subdegree_def subdegree_def
using 2 enat_def
by (smt (z3) "2" LeastI_ex cInf_eq_minimum enat_def f2 fps_nonzero_nth mem_Collect_eq)
qed
lemma valuation_miscs_3:‹valuation f = v_subdegree f›
proof(cases ‹f=0›)
case 1:True
have f1:‹valuation f = ∞›
using 1 valuation_miscs_1
by (simp add: FPS_ring_def)
show ?thesis
by (metis "1" Formal_Power_Series_Ring.v_subdegree_def f1)
next
case 2:False
have f0:‹fps_nth f n ≠ 0 ⟹ f ∉ cgenideal FPS_ring (fps_X^(Suc n))› for n
apply(subst fps_X_pow_k_ideal_iff)
unfolding v_subdegree_def
using not_less_eq_eq subdegree_leI by auto
then have ‹f ∉ cgenideal FPS_ring (fps_X^(n)) ⟹ ∀i≥n. f ∉ cgenideal FPS_ring (fps_X^(i))›
for n
by (simp add: 2 fps_X_pow_k_ideal_iff v_subdegree_def)
with f0 have f2:‹fps_nth f n ≠ 0 ⟹ valuation f ≤ n› for n
unfolding valuation_def
by (smt (verit, del_insts) Sup_le_iff enat_ord_simps(1) mem_Collect_eq not_less_eq_eq)
then show ‹valuation f = v_subdegree f›
by (smt (verit, best) "2" Orderings.order_eq_iff Sup_le_iff fps_X_pow_k_ideal_iff
mem_Collect_eq v_subdegree_def valuation_def)
qed
lemma triangular_ineq_v:‹valuation (f + g) ≥ min (valuation f) (valuation g)›
apply(subst (1 2 3) valuation_miscs_3)
unfolding v_subdegree_def
by (simp add: subdegree_add_ge')
lemma triang_eq_v:assumes h1:‹valuation f≠ valuation g›
shows ‹valuation (f+g) = min (valuation f) (valuation g)›
proof -
have f0:‹valuation (f+g) ≥ min (valuation f) (valuation g)›
by (simp add:triangular_ineq_v FPS_ring_def)
have ‹valuation (f+g) ≤ min (valuation f) (valuation g)›
apply(subst (1 2 3) valuation_miscs_3) unfolding min_def v_subdegree_def
by (smt (verit, ccfv_threshold) Suc_le_eq add_cancel_right_left add_diff_cancel_right'
add_eq_0_iff2 diff_zero enat_ord_simps(2) enat_ord_simps(3) h1 not_less_eq_eq order_le_less
subdegree_add_eq1 subdegree_add_eq2 subdegree_uminus v_subdegree_def valuation_miscs_3)
then show ?thesis using f0
by order
qed
lemma prod_triang_v:‹valuation (f*g) = valuation f + valuation g›
apply(subst (1 2 3) valuation_miscs_3)
unfolding v_subdegree_def by(auto)
subsection ‹Premisses for noetherian ring proof›
definition subdeg_poly_set:‹subdeg_poly_set S k = {a. a∈S ∧ subdegree a = k}∪{0}›
definition sublead_coeff_set::‹'b::{zero} fps set⇒ nat ⇒ 'b set›
where ‹sublead_coeff_set S k ≡ { fps_nth a (subdegree a) | a. a∈ subdeg_poly_set S k}›
lemma ideal_nonempty:‹ideal I FPS_ring ⟹ I ≠ {}›
by (metis FPS_ring_def UNIV_I empty_iff ideal.axioms(2)
partial_object.select_convs(1) ring.quotient_eq_iff_same_a_r_cos)
lemma mult_X_in_ideal:‹ideal I FPS_ring ⟹ ∀x∈I. fps_X * x ∈ I›
unfolding ideal_def ideal_axioms_def
by (simp add: FPS_ring_def)
lemma non_empty_sublead:‹ideal I FPS_ring ⟹ sublead_coeff_set I k ≠ {}›
unfolding sublead_coeff_set_def subdeg_poly_set by(auto)
lemma inv_unique:‹∀x∈carrier FPS_ring. ∃!y. x + y = 0›
by (metis add.right_inverse add_diff_cancel_left')
lemma inv_same_degree:assumes h:‹x∈carrier FPS_ring›
shows‹subdegree (inv⇘add_monoid FPS_ring⇙ x) = subdegree x›
by (metis FPS_ring_def ring_FPS abelian_group.a_group add_eq_0_iff2 group.l_inv h
monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) ring_def
ring_record_simps(11) ring_record_simps(12) subdegree_uminus)
lemma inv_subdegree_is_inv: assumes h:"x∈carrier FPS_ring"
shows ‹fps_nth (inv⇘add_monoid FPS_ring⇙ x) (subdegree x) =
(inv⇘add_monoid R⇙ (fps_nth x (subdegree x)))›
unfolding a_inv_def
by (metis FPS_ring_def ring_FPS R UNIV_I a_inv_def
fps_add_nth partial_object.select_convs(1)
ring.ring_simprules(17) ring.ring_simprules(9) ring_R
ring_record_simps(12))
lemma subdeg_inv_in_sublead:
assumes h1:‹ideal I FPS_ring› and h2:‹a ∈ sublead_coeff_set I k›
shows ‹inv⇘add_monoid R⇙ a ∈ sublead_coeff_set I k›
proof -
have f0:‹x∈I ⟹ inv⇘add_monoid FPS_ring⇙ x ∈ I› for x
by (meson additive_subgroup_def h1 ideal.axioms(1) subgroup.m_inv_closed)
then have f1:‹x∈I ⟹ inv⇘add_monoid FPS_ring⇙ x ∈ subdeg_poly_set I (subdegree x)› for x
unfolding subdeg_poly_set using UnCI h1 ideal.Icarr[of I FPS_ring x] inv_same_degree[of x]
mem_Collect_eq by(auto)
have f2:‹x∈I ⟹ (inv⇘add_monoid R⇙ (fps_nth x (subdegree x)))
∈ sublead_coeff_set I (subdegree x)›
for x
unfolding sublead_coeff_set_def
using f1[of x] h1 ideal.Icarr[of I FPS_ring x] inv_same_degree[of x]
inv_subdegree_is_inv[of x] mem_Collect_eq
by force
have ‹0∈I›
by (metis FPS_ring_def additive_subgroup.zero_closed h1 ideal.axioms(1) ring.simps(1))
then have f3:‹a≠0 ⟹ ∃x∈I. a = fps_nth x (subdegree x) ∧ subdegree x = k›
using h2 unfolding sublead_coeff_set_def subdeg_poly_set
by(auto)
then obtain x where ‹a ≠0 ⟹ x∈I ∧ a = fps_nth x (subdegree x)∧ subdegree x = k› by blast
then have f5:‹a≠0 ⟹ inv⇘add_monoid R⇙ a = fps_nth (inv⇘add_monoid FPS_ring⇙ x) (subdegree x)›
by (metis FPS_ring_def UNIV_I inv_subdegree_is_inv partial_object.select_convs(1))
then have f6:‹a≠0 ⟹ fps_nth (inv⇘add_monoid FPS_ring⇙ x) (subdegree x) ∈ sublead_coeff_set I k›
using ‹a ≠ 0 ⟹ x ∈ I ∧ a = fps_nth x (subdegree x) ∧ subdegree x = k› f2 by force
then show ?thesis
apply(cases ‹a=0›)
apply (metis R a_inv_def h2 ring.minus_zero ring_R ring_record_simps(11))
using f5 by presburger
qed
lemma mult_stable_sublead:
assumes h1:‹ideal I FPS_ring›
and h2:‹a ∈ sublead_coeff_set I k›
and h3:‹b ∈ sublead_coeff_set I k›
shows ‹a ⊗⇘R⇙ b ∈ sublead_coeff_set I k›
proof -
have ‹0∈I›
by (metis FPS_ring_def additive_subgroup.zero_closed h1 ideal.axioms(1) ring.simps(1))
{assume h4:‹a≠0› and h5:‹b≠0›
then have f3:‹∃x∈I. a = fps_nth x (subdegree x) ∧ subdegree x = k›
using h2 unfolding sublead_coeff_set_def subdeg_poly_set
by(auto)
then obtain x where f0:‹ x∈I ∧ a = fps_nth x (subdegree x)∧ subdegree x = k› by blast
then have ‹fps_const b ∈carrier FPS_ring›
by (simp add: FPS_ring_def)
then have ‹fps_const b*x ∈ I›
by (metis FPS_ring_def f0 h1 ideal_axioms_def ideal_def monoid.simps(1))
then have ‹fps_nth (fps_const b * x) k = a*b›
by (simp add: f0)
then have ‹subdegree (fps_const b * x) = k›
using f0 h4 h5 by force
then have ‹a ⊗⇘R⇙ b ∈ sublead_coeff_set I k›
unfolding sublead_coeff_set_def subdeg_poly_set FPS_ring_def
using R ‹fps_const b * x ∈ I› ‹fps_nth (fps_const b * x) k = a * b› by force
}note proof_2=this
then show ?thesis
apply(cases ‹a=0 ∨ b=0›)
using R h2 h3 by auto
qed
lemma add_stable_sublead:
assumes h1:‹ideal I FPS_ring›
and h2:‹a ∈ sublead_coeff_set I k›
and h3:‹b ∈ sublead_coeff_set I k›
shows ‹a ⊗⇘add_monoid R⇙ b ∈ sublead_coeff_set I k›
proof -
have f0:‹0∈I›
by (metis FPS_ring_def additive_subgroup.zero_closed h1 ideal.axioms(1) ring.simps(1))
have p2:‹a=-b ⟹ a + b ∈ sublead_coeff_set I k›
unfolding sublead_coeff_set_def subdeg_poly_set by(auto)
{assume h4:‹a≠0› and h5:‹b≠0› and h6:‹a≠- b›
then have f3:‹∃x∈I. a = fps_nth x (subdegree x) ∧ subdegree x = k›
using h2 unfolding sublead_coeff_set_def subdeg_poly_set
by(auto)
then obtain x where f2:‹ x∈I ∧ a = fps_nth x (subdegree x)∧ subdegree x = k› by blast
have f4:‹∃x∈I. b = fps_nth x (subdegree x) ∧ subdegree x = k›
using f0 h3 h4 h5 unfolding sublead_coeff_set_def subdeg_poly_set
by(auto)
then obtain y where f1:‹y∈I ∧ b = fps_nth y (subdegree y)∧ subdegree y = k› by blast
then have ‹x + y ∈ I› using h1 unfolding ideal_def
using f2 additive_subgroup.a_closed[of I FPS_ring x y]
by (simp add: FPS_ring_def)
have f4:‹fps_nth (x+y) k = a + b›
by (simp add: f1 f2)
have ‹∀i<k. fps_nth (x+y) i = 0›
by (simp add: f1 f2 nth_less_subdegree_zero)
then have f5:‹subdegree (x + y) = k›
by (metis ‹fps_nth (x + y) k = a + b› eq_neg_iff_add_eq_0 h6 subdegreeI)
then have ‹a+b ∈ sublead_coeff_set I k›
using f4 f5 unfolding sublead_coeff_set_def subdeg_poly_set
using ‹x + y ∈ I› by force
}note proof_1=this
then show ?thesis
apply(cases ‹a=0 ∨ b = 0 ∨ a = -b›)
using R h2 h3 p2 proof_1 by auto
qed
lemma outer_stable_sublead:
assumes h1:‹ideal I FPS_ring›and h2:‹a ∈ sublead_coeff_set I k› and h3:‹b ∈ carrier R›
shows ‹b ⊗ a ∈ sublead_coeff_set I k›
proof -
have ‹0∈I›
by (metis FPS_ring_def additive_subgroup.zero_closed h1 ideal.axioms(1) ring.simps(1))
then have p2:‹0∈sublead_coeff_set I k› unfolding sublead_coeff_set_def subdeg_poly_set by(auto)
{assume h4:‹a≠0› and h5:‹b≠0›
then have f3:‹∃x∈I. a = fps_nth x (subdegree x) ∧ subdegree x = k›
using h2 unfolding sublead_coeff_set_def subdeg_poly_set
by(auto)
then obtain x where f0:‹ x∈I ∧ a = fps_nth x (subdegree x)∧ subdegree x = k› by blast
then have ‹fps_const b ∈carrier FPS_ring›
by (simp add: FPS_ring_def)
then have ‹fps_const b*x ∈ I›
by (metis FPS_ring_def f0 h1 ideal_axioms_def ideal_def monoid.simps(1))
then have ‹fps_nth (fps_const b * x) k = a*b›
by (simp add: f0)
then have ‹subdegree (fps_const b * x) = k›
using f0 h4 h5 by force
then have ‹b ⊗⇘R⇙ a ∈ sublead_coeff_set I k›
unfolding sublead_coeff_set_def subdeg_poly_set FPS_ring_def
using R ‹fps_const b * x ∈ I› ‹fps_nth (fps_const b * x) k = a * b› by force
}note proof_2=this
then show ?thesis
apply(cases ‹a=0 ∨ b=0›)
using R h2 h3 proof_2 p2 by auto
qed
lemma sublead_ideal:‹ideal I FPS_ring ⟹ ideal (sublead_coeff_set I k) R›
apply(rule idealI)
apply(simp add:ring_R)
apply(rule group.subgroupI)
using abelian_group.a_group ring.is_abelian_group ring_R apply fastforce
apply (simp add: R)
apply(simp add:non_empty_sublead)
using subdeg_inv_in_sublead apply blast
using add_stable_sublead apply force
apply (simp add: outer_stable_sublead mult.commute)
by (metis Groups.mult_ac(2) R monoid.simps(1) outer_stable_sublead)
lemma order_sublead:
assumes h1:‹J1 ⊆ J2› and h2:‹ideal J1 FPS_ring› and h3:‹ideal J2 FPS_ring›
shows ‹sublead_coeff_set J1 k ⊆ sublead_coeff_set J2 k›
unfolding sublead_coeff_set_def subdeg_poly_set
using h1 by blast
lemma sup_sublead_stable_add:‹ideal I FPS_ring ⟹
a ∈ ⋃ (range (sublead_coeff_set I)) ⟹
b ∈ ⋃ (range (sublead_coeff_set I))
⟹ a ⊗⇘add_monoid R⇙ b ∈ ⋃ (range (sublead_coeff_set I))›
proof -
have f2:‹x≠0 ∧ x∈subdeg_poly_set I k ⟹ subdegree x = k› for x k
unfolding subdeg_poly_set by auto
then have f1:‹x≠0 ∧ x∈subdeg_poly_set I k ⟹ fps_nth x k ∈ sublead_coeff_set I k› for x k
unfolding sublead_coeff_set_def by blast
assume h1:‹ideal I FPS_ring› ‹a ∈ ⋃ (range (sublead_coeff_set I))›
‹b ∈ ⋃ (range (sublead_coeff_set I))›
then obtain x x' k k'
where f0:‹a = fps_nth x k ∧ x∈subdeg_poly_set I k ∧ b = fps_nth x' k' ∧ x'∈subdeg_poly_set I k'›
unfolding sublead_coeff_set_def apply(safe)
by (metis (mono_tags, lifting) Un_def mem_Collect_eq subdeg_poly_set)
have p1:‹k=k'⟹a≠0 ⟹b≠0 ⟹ a∈sublead_coeff_set I k ∧ b ∈ sublead_coeff_set I k›
using h1 f0 f1 fps_nonzero_nth by blast
have f3:‹k<k' ⟹ a≠0 ⟹ b≠0 ⟹ fps_X^(k'-k)*x ∈ I›
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def UNIV_I Un_iff
additive_subgroup.zero_closed f0 h1(1) ideal_axioms_def ideal_def mem_Collect_eq monoid.simps(1)
partial_object.select_convs(1) ring.simps(1) singletonD subdeg_poly_set)
then have f4:‹k<k' ⟹ a≠0 ⟹ b≠0 ⟹ subdegree (fps_X^(k'-k)*x) = k'›
by (metis f2 add_diff_inverse_nat f0 fps_nonzero_nth fps_subdegree_mult_fps_X_power(1)
less_numeral_extra(3) nat_diff_split_asm zero_less_diff)
then have f5:‹k<k'⟹ a≠0 ⟹ b≠ 0 ⟹ (fps_X^(k'-k)*x) ∈ subdeg_poly_set I k'›
unfolding subdeg_poly_set using f3 by auto
then have f6:‹k<k' ⟹ a≠0 ⟹ b≠0
⟹ fps_nth ((fps_X^(k'-k)*x) + x') k' ∈ ⋃ (range (sublead_coeff_set I))›
by (metis R UNIV_I UN_iff add_stable_sublead f0 f1 fps_add_nth fps_mult_fps_X_power_nonzero(1)
fps_zero_nth h1(1) monoid.simps(1) ring_record_simps(12))
have f7:‹b ≠ 0 ⟹ k < k'⟹ a = - b ⟹ ∃r. 0 ∈ sublead_coeff_set I r ›
by (metis R additive_subgroup.zero_closed h1(1) ideal_def ring.simps(1) sublead_ideal)
have f8:‹a ≠ 0 ⟹ b ≠ 0 ⟹ k < k' ⟹ a ≠ - b ⟹ ∃r. a + b ∈ sublead_coeff_set I r›
by (metis UN_E add_diff_cancel_left' add_less_same_cancel2 diff_add_inverse2 f0 f6
fps_X_power_mult_nth fps_add_nth less_imp_add_positive not_less_zero)
then have p2:‹a ≠ 0 ⟹ b ≠ 0 ⟹ k < k' ⟹ ∃r. a ⊕ b ∈ sublead_coeff_set I r›
apply(cases ‹a=-b›)
by(auto simp:R FPS_ring_def f7)
have f3':‹k'<k ⟹ a≠0 ⟹ b≠0 ⟹ fps_X^(k-k')*x' ∈ I›
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def UNIV_I Un_iff
additive_subgroup.zero_closed f0 h1(1) ideal_axioms_def ideal_def mem_Collect_eq monoid.simps(1)
partial_object.select_convs(1) ring.simps(1) singletonD subdeg_poly_set)
then have f4':‹k'<k ⟹ a≠0 ⟹ b≠0 ⟹ subdegree (fps_X^(k-k')*x') = k›
by (metis f2 add_diff_inverse_nat f0 fps_nonzero_nth fps_subdegree_mult_fps_X_power(1)
less_numeral_extra(3) nat_diff_split_asm zero_less_diff)
then have f5':‹k'<k⟹ a≠0 ⟹ b≠ 0 ⟹ (fps_X^(k-k')*x') ∈ subdeg_poly_set I k›
unfolding subdeg_poly_set using f3' by auto
then have f6':‹k'<k ⟹ a≠0 ⟹ b≠0
⟹ fps_nth ((fps_X^(k-k')*x') + x) k ∈ ⋃ (range (sublead_coeff_set I))›
by (metis R UNIV_I UN_iff add_stable_sublead f0 f1 fps_add_nth fps_mult_fps_X_power_nonzero(1)
fps_zero_nth h1(1) monoid.simps(1) ring_record_simps(12))
have f7':‹b ≠ 0 ⟹ k' < k ⟹ a = - b ⟹ ∃r. 0 ∈ sublead_coeff_set I r ›
by (metis R additive_subgroup.zero_closed h1(1) ideal_def ring.simps(1) sublead_ideal)
have f8':‹a ≠ 0 ⟹ b ≠ 0 ⟹ k' < k ⟹ a ≠ - b ⟹ ∃r. a + b ∈ sublead_coeff_set I r›
by (metis (no_types, lifting) UN_iff f8 add.commute add_diff_cancel_right' add_diff_inverse_nat
f0 f4' f6' fps_X_power_mult_nth fps_add_nth not_less_zero nth_subdegree_zero_iff subdegree_0)
then have p3:‹a ≠ 0 ⟹ b ≠ 0 ⟹ k' < k ⟹ ∃r. a ⊕ b ∈ sublead_coeff_set I r›
apply(cases ‹a=-b›)
by(auto simp:R FPS_ring_def f7')
have cases:‹k=k' ∨ k<k' ∨ k'<k›
by auto
then show ?thesis
apply(cases ‹a=0 ∨ b= 0›)
using R h1(2) h1(3) apply force
using Formal_Power_Series_Ring.add_stable_sublead R h1(1) p1 p2 p3 by(force)
qed
lemma sup_sublead_ideal:‹ideal I FPS_ring ⟹ ideal (⋃ k. sublead_coeff_set I k) R›
apply(rule idealI)
apply (simp add: ring_R)
apply(rule group.subgroupI)
using abelian_group.a_group ring.is_abelian_group ring_R apply blast
apply (simp add: R)
using non_empty_sublead apply force
using subdeg_inv_in_sublead apply force
using sup_sublead_stable_add apply force
apply (metis UN_iff outer_stable_sublead)
by (metis UN_iff ideal.I_r_closed sublead_ideal)
lemma Sub_subdeg_eq_ideal:‹ideal J FPS_ring ⟹ (⋃k. subdeg_poly_set J k) = J›
unfolding subdeg_poly_set apply(safe)
apply (metis Formal_Power_Series_Ring.FPS_ring_def
additive_subgroup.zero_closed ideal.axioms(1) ring.simps(1))
by auto
lemma eq_subdeg:
assumes h1:‹J1 ⊆ J2›
and h3:‹ ideal J1 FPS_ring› and h4:‹ideal J2 FPS_ring›
shows ‹J1 = J2 ⟷ (∀k. subdeg_poly_set J1 k = subdeg_poly_set J2 k)›
proof -
have ‹∀k. subdeg_poly_set J1 k = subdeg_poly_set J2 k
⟹ (⋃k. subdeg_poly_set J1 k) = (⋃k. subdeg_poly_set J2 k)›
by auto
then have f0:‹∀k. subdeg_poly_set J1 k = subdeg_poly_set J2 k ⟹ J1 = J2›
by (metis Sub_subdeg_eq_ideal h3 h4)
have f1:‹J1 = J2 ⟹ ∀k. subdeg_poly_set J1 k = subdeg_poly_set J2 k›
unfolding subdeg_poly_set by auto
then show ?thesis using f0 f1 by auto
qed
lemma inculded_sublead:‹ideal I FPS_ring ⟹ sublead_coeff_set I k ⊆ sublead_coeff_set I (k+1)›
unfolding sublead_coeff_set_def subdeg_poly_set
proof(safe)
fix x a
assume ‹ideal I local.FPS_ring›
‹a ∈ I›
‹k = subdegree a ›
show ‹∃aa. fps_nth a (subdegree a) = fps_nth aa (subdegree aa)
∧ aa ∈ {aa ∈ I. subdegree aa = subdegree a + 1} ∪ {0}›
apply(rule exI[where x=‹fps_X * a›])
by (simp add:subdegree_eq_0_iff ‹a ∈ I› ‹ideal I local.FPS_ring› mult_X_in_ideal)+
next
show ‹∃a. fps_nth 0 (subdegree 0) = fps_nth a (subdegree a)
∧ a ∈ {a ∈ I. subdegree a = k + 1} ∪ {0}›
by auto
qed
lemma included_sublead_gen:assumes ‹ideal I FPS_ring› ‹k≤k'›
shows ‹sublead_coeff_set I k ⊆ sublead_coeff_set I (k')›
using assms
apply(induct ‹k'-k›)
apply simp
by (metis Suc_eq_plus1 inculded_sublead lift_Suc_mono_le)
lemma sup_sublead:
assumes h1:‹ideal I FPS_ring›
and h2: ‹noetherian_ring R›
shows ‹(⋃{sublead_coeff_set I k|k. k∈UNIV}) ∈ {sublead_coeff_set I k|k. k∈UNIV}›
apply(rule noetherian_ring.ideal_chain_is_trivial[OF h2, of ‹{sublead_coeff_set I k|k. k∈UNIV}›])
apply blast
unfolding subset_chain_def using included_sublead_gen
by(auto simp add: h1 sublead_ideal)(meson h1 in_mono linorder_linear)
lemma subdeg_inf_imp_s_tendsto_zero:
fixes s::‹nat ⇒ 'a::{idom} fps›
assumes g2:‹strict_mono (λn. subdegree (s n))›
shows ‹s ⇢ 0›
proof -
have g1:‹(λx. 1/x) ⇢ 0›
using lim_1_over_n by force
have ‹∀n. ∃k. n < subdegree (s k)›
by (metis dual_order.strict_trans g2 gt_ex linorder_not_le
nat_neq_iff strict_mono_imp_increasing)
have r1:‹r>0 ⟹ (n::nat) > log 2 (1/r) ⟹ (1/2^n < r) ⟷ 2^n > 1/r› for n r
by(auto simp:field_simps)
have r2:‹r>0 ⟹ (n::nat) > log 2 (1/r) ⟹ 2^n > 2 powr (log 2 (1/r))› for n r
by (simp add: log_less_iff powr_realpow)
then have r3:‹r>0 ⟹ (n::nat) > log 2 (1/r) ⟹ 2 powr (log 2 (1/r)) = 1/r› for r n
by auto
then have r4:‹r>0 ⟹ (n::nat) > log 2 (1/r) ⟹ 2^n > 1/r› for r n
using ‹⋀r n. ⟦0 < r; log 2 (1 / r) < real n⟧ ⟹ 2 powr log 2 (1 / r) < 2 ^ n› by force
then have r5:‹r>0 ⟹ (n::nat) > log 2 (1/r) ⟹ 1/2^n < r› for r n
using ‹⋀r n. ⟦0 < r; log 2 (1 / r) < real n⟧ ⟹ (1 / 2 ^ n < r) = (1 / r < 2 ^ n)› by blast
have ‹ceiling (r::real) ≥ r› for r
by simp
then have r6:‹r>0 ⟹ (ceiling (log 2 (1/r))) ≥ log 2 (1/r)› for r
by auto
then have r7:‹r>0 ⟹ (n::nat) > (ceiling (log 2 (1/r))) ⟹ 1/2^n < r› for r n
by (metis ‹⋀r n. ⟦0 < r; log 2 (1 / r) < real n⟧ ⟹ 1 / 2 ^ n < r›
ceiling_less_cancel ceiling_of_nat)
have r8:‹r>0 ⟹ ∃n::nat. n> (log 2 (1/r))› for r
by (simp add: reals_Archimedean2)
have r9:‹∀(r::real)>0. ∃n0. ∀n≥n0. 1/2^n < r›
proof(safe)
fix r::real
assume ‹r>0›
then obtain n::nat where ‹n> (log 2 (1/r))› using r8 by blast
show ‹∃n0. ∀n≥n0. 1 / 2 ^ n < r›
apply(rule exI[where x=n])
using ‹0 < r› ‹log 2 (1 / r) < real n› r5 by auto
qed
show t2:‹s ⇢ 0›
proof(rule metric_LIMSEQ_I)
fix r::real
assume ‹0<r›
then obtain n where ‹n>0 ∧ 1/2^n < r› using r9
by (metis gr0I less_or_eq_imp_le zero_less_numeral)
then have ‹∀k≥n. inverse (2^k) < r›
by (smt (verit, ccfv_threshold) inverse_eq_divide
inverse_less_iff_less power_increasing_iff zero_less_power)
then obtain n1 where ‹1/2^(subdegree (s n1)) < r ∧ n1>0›
by (metis ‹∀n. ∃k. n < subdegree (s k)› bot_nat_0.not_eq_extremum divide_inverse
mult_1 nle_le not_less_iff_gr_or_eq order_less_le_trans)
then have ‹dist (s n1) 0 < r›
by (simp add: ‹0 < r› dist_fps_def inverse_eq_divide)
then show ‹∃no. ∀n≥no. dist (s n) 0 < r›
apply(intro exI[where x=n1])
apply(safe) using g2
unfolding dist_fps_def strict_mono_def
using power_strict_increasing_iff[of 2 ‹subdegree (s n1)›] inverse_eq_divide inverse_le_iff_le
by (smt (verit) ‹0 < r› ‹1 / 2 ^ subdegree (s n1) < r ∧ 0 < n1›
diff_zero le_eq_less_or_eq power_less1_D)
qed
qed
lemma idl_sum:‹finite A ⟹ ideal {x. ∃s. x=(∑i∈{0..<card A}. s i * from_nat_into A i)} R› for A
proof(rule idealI)
assume ‹finite A›
show ‹ring R›
using ring_R by(simp)
show ‹subgroup {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)} (add_monoid R)›
proof(rule group.subgroupI)
show ‹Group.group (add_monoid R)›
using abelian_group.a_group ring.is_abelian_group ring_R by blast
show ‹{x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)} ⊆ carrier (add_monoid R)›
by (simp add: R)
show ‹{x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)} ≠ {}›
by blast
next
fix a assume ‹a ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
then show ‹inv⇘add_monoid R⇙ a ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
proof(safe)
fix s
have p6:‹(THE y. (∑i = 0..<card A. s i * from_nat_into A i) + y = 0 ∧ y +
(∑i = 0..<card A. s i * from_nat_into A i) = 0)
= (∑i = 0..<card A. - (s i * from_nat_into A i))› for A::‹'a set› and s
using theI'[of ‹λy. (∑i = 0..<card A. s i * from_nat_into A i) + y = 0 ∧ y +
(∑i = 0..<card A. s i * from_nat_into A i) = 0›]
by (smt (verit, best) add.commute add.right_inverse add_left_imp_eq sum.cong sum_negf)
assume ‹a = (∑i = 0..<card A. s i * from_nat_into A i)›
then show ‹ ∃sa. inv⇘add_monoid R⇙ (∑i = 0..<card A. s i *
from_nat_into A i) = (∑i = 0..<card A. sa i * from_nat_into A i)›
apply(intro exI[where x=‹-s›])
by(auto simp add:m_inv_def p6 R)
qed
next
fix a b
assume ‹a ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
‹b ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
then show ‹a ⊗⇘add_monoid R⇙ b ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
proof(safe)
fix s sa
assume ‹a = (∑i = 0..<card A. s i * from_nat_into A i)›
‹b = (∑i = 0..<card A. sa i * from_nat_into A i)›
then show ‹ ∃sb. (∑i = 0..<card A. s i * from_nat_into A i) ⊗⇘add_monoid R⇙
(∑i = 0..<card A. sa i * from_nat_into A i) = (∑i = 0..<card A. sb i * from_nat_into A i)›
apply(intro exI[where x=‹λi. s i + sa i›])
by(simp add:R comm_semiring_class.distrib sum.distrib)
qed
qed
next
fix a x
assume ‹finite A› ‹a ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}› ‹x ∈ carrier R›
then show ‹x ⊗ a ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
‹a ⊗ x ∈ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
proof(safe)
fix s
assume ‹a = (∑i = 0..<card A. s i * from_nat_into A i)›
then show
‹∃sa. x ⊗ (∑i = 0..<card A. s i * from_nat_into A i) = (∑i = 0..<card A. sa i * from_nat_into A i)›
apply(intro exI[where x=‹(λi. x * s i)›])
by (simp add:R comm_semiring_class.distrib sum.distrib mult.assoc sum_distrib_left)
show
‹∃sa. (∑i = 0..<card A. s i * from_nat_into A i) ⊗ x = (∑i = 0..<card A. sa i * from_nat_into A i)›
apply(intro exI[where x=‹(λi. x * s i)›])
by (simp add:R comm_semiring_class.distrib sum.distrib mult.assoc
sum_distrib_left mult.left_commute mult.commute)
qed
qed
lemma genideal_sum_rep:
‹finite A ⟹ genideal R A = {x. ∃s. x=(∑i∈{0..<card A}. s i * from_nat_into A i)}› for A
proof(subst set_eq_subset, rule conjI)
assume hr:‹finite A›
then have unq:‹x∈A ⟹ ∃!i. i<card A ∧ from_nat_into A i = x› for x
using bij_betw_from_nat_into_finite[of A, OF ‹finite A›]
unfolding bij_betw_def inj_on_def
by (smt (verit, ccfv_threshold) ‹bij_betw (from_nat_into A) {..<card A} A›
bij_betw_iff_bijections lessThan_iff)
have ‹A≠{}⟹ (card ({0..<card A} ∩ {i. from_nat_into A i = x})) = 1› if hh:‹x∈A› for x
proof(rule ccontr)
assume hhh:‹card ({0..<card A} ∩ {i. from_nat_into A i = x}) ≠ 1› ‹A≠{}›
then have jm:
‹card ({0..<card A} ∩ {i. from_nat_into A i = x}) > 1 ⟹ ∃i1 i2. i1≠i2 ∧ i1 <card A
∧ i2<card A∧ from_nat_into A i1 = from_nat_into A i2 ∧ from_nat_into A i1 = x›
by (smt (verit, ccfv_SIG) Int_Collect One_nat_def atLeastLessThan_iff card_le_Suc0_iff_eq
finite_Int finite_atLeastLessThan linorder_not_less n_not_Suc_n)
then have ‹card ({0..<card A} ∩ {i. from_nat_into A i = x}) > 1› using hhh hr
by (metis (mono_tags, lifting) Int_def atLeastLessThan_iff card_eq_0_iff emptyE finite_Int
finite_atLeastLessThan le0 less_one linorder_neqE_nat mem_Collect_eq that unq)
then show False using jm unq[OF hh] by(auto)
qed
then have ‹A⊆{x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
proof(safe)
fix x
assume hhhh:‹(⋀x. x ∈ A ⟹ A ≠ {} ⟹ card ({0..<card A} ∩ {i. from_nat_into A i = x}) = 1)›
‹x∈A›
then have ‹of_nat (card ({0..<card A} ∩ {xa. from_nat_into A xa = x})) = 1›
by (metis One_nat_def card.empty less_nat_zero_code of_nat_1 unq)
with hhhh show ‹∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)›
apply(cases ‹x=0›)
apply(rule exI[where x=‹λi. 0›])
apply(simp)
apply(rule exI[where x=‹λi. if from_nat_into A i = x then 1 else 0›])
apply(subst if_distrib[where f=‹λx. x*a› for a])
apply(subst sum.If_cases)
by(simp)+
qed
then show ‹Idl A ⊆ {x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)}›
unfolding genideal_def using idl_sum[OF hr] by(auto)
show ‹{x. ∃s. x = (∑i = 0..<card A. s i * from_nat_into A i)} ⊆ Idl A ›
proof(safe)
fix x and s::‹nat⇒'a›
have a:‹∀i<card A. from_nat_into A i ∈ A›
by (metis card.empty from_nat_into less_nat_zero_code)
then have b:‹∀i. s i ∈ carrier R›
using R by auto
then have ‹∀i<card A. s i * from_nat_into A i ∈ genideal R A›
using ring.genideal_ideal[OF ring_R, of A] ideal.I_l_closed[of _ R ]
by (metis R a ideal_def monoid.simps(1) partial_object.select_convs(1)
ring.genideal_self subsetD subset_UNIV)
have ff:‹A⊆ carrier R› by (simp add:R)
then have ‹∀i<n. g i ∈ genideal R A ⟹ (∑i∈{0..<n}. g i) ∈ genideal R A›
for g::‹nat ⇒ 'a› and n
apply(induct n)
apply (metis R additive_subgroup.zero_closed atLeastLessThan_iff
ideal_def not_less_zero ring.genideal_ideal ring.simps(1) ring_R sum.neutral)
using ring.genideal_ideal[OF ring_R, of A, OF ‹A⊆ carrier R›]
additive_subgroup.a_closed[of ‹genideal R A› R _ _] unfolding ideal_def by(auto simp:R)
then show ‹(∑i = 0..<card A. s i * from_nat_into A i) ∈ Idl A›
using ‹∀i<card A. s i * from_nat_into A i ∈ Idl A› by presburger
qed
qed
lemma fps_sum_rep_nth':
"fps_nth (sum (λi. fps_const(a i)*fps_X^i) {0..m}) n = (if n ≤ m then a n else 0)"
by (simp add: fps_sum_nth if_distrib cong del: if_weak_cong)
lemma abs_tndsto: shows ‹(λn. (∑i≤n. fps_const (s i) * fps_X^i)::'a fps) ⇢ Abs_fps s›
(is ‹?s ⇢ ?a›)
proof -
have "∃n0. ∀n ≥ n0. dist (?s n) ?a < r" if "r > 0" for r
proof -
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
using reals_power_lt_ex[OF ‹r > 0›, of 2] by auto
show ?thesis
proof -
have "dist (?s n) ?a < r" if nn0: "n ≥ n0" for n
proof -
from that have thnn0: "(1/2)^n ≤ (1/2 :: real)^n0"
by (simp add: field_split_simps)
show ?thesis
proof (cases "?s n = ?a")
case True
then show ?thesis
unfolding metric_space.dist_eq_0_iff
using ‹r > 0› by (simp del: dist_eq_0_iff)
next
case False
from False have dth: "dist (?s n) ?a = (1/2)^subdegree (?s n - ?a)"
by (simp add: dist_fps_def field_simps)
from False have kn: "subdegree (?s n - ?a) > n"
apply (intro subdegree_greaterI) apply(simp_all add: fps_sum_rep_nth')
by (metis (full_types) atLeast0AtMost fps_sum_rep_nth')
then have "dist (?s n) ?a < (1/2)^n"
by (simp add: field_simps dist_fps_def)
also have "… ≤ (1/2)^n0"
using nn0 by (simp add: field_split_simps)
also have "… < r"
using n0 by simp
finally show ?thesis .
qed
qed
then show ?thesis by blast
qed
qed
then show ?thesis
unfolding lim_sequentially by blast
qed
lemma add_stable_FPS_ring:‹ideal I FPS_ring ⟹ a∈I ⟹ b∈I ⟹ a+b ∈ I›
unfolding FPS_ring_def
by (metis additive_subgroup.a_closed ideal.axioms(1) ring_record_simps(12))
lemma abs_tndsto_le: shows ‹(λn. (∑i<n. fps_const (s i) * fps_X^i)::'a fps) ⇢ Abs_fps s›
using LIMSEQ_lessThan_iff_atMost abs_tndsto by blast
lemma bij_betw_strict_mono:
assumes ‹strict_mono (f::nat⇒nat)›
shows ‹bij_betw f UNIV (f`UNIV)›
by (simp add: assms bij_betw_imageI strict_mono_on_imp_inj_on)
lemma no_i_inf_0:‹strict_mono (f::nat⇒nat) ⟹ i<f 0 ⟹ ¬(∃j. f j = i)›
by (auto simp add: strict_mono_less)
lemma inter_mt:‹strict_mono (f::nat⇒nat) ⟹ {..<f 0} ∩ range f = {}›
by (metis Int_emptyI lessThan_iff no_i_inf_0 rangeE)
lemma range_inter_f:‹strict_mono (f::nat⇒nat) ⟹ {..<f n} ∩ range f = f`{0..<n}›
apply(induct n)
apply (simp add: inter_mt)
by (auto simp:strict_mono_less strict_monoD)
lemma simp_rule_sum:‹strict_mono (f::nat⇒nat) ⟹ (∑i∈{..<f (Suc n)}. (if i ∈ range f
then (s ((inv_into UNIV f) i)) *fps_X^i else 0)) = (∑i∈{..<f n}. (if i ∈ range f then
(s ((inv_into UNIV f) i)) *fps_X^i else 0)) + (s ((inv_into UNIV f) (f n))) *fps_X^(f n)›
proof -
assume h1:‹strict_mono f›
have f0:‹∀i∈{f n<..<f (Suc n)}. (if i ∈ range f then (s ((inv_into UNIV f) i)) *fps_X^i else 0) = 0›
by (metis greaterThanLessThan_iff h1 not_less_eq rangeE strict_mono_less)
then have s:‹{..<f (Suc n)} = {..f n} ∪ {f n<..<f (Suc n)}›
by (metis h1 ivl_disj_un_one(1) strict_mono_Suc_iff)
show ?thesis
apply(subst s)
apply(subst sum.union_disjoint)
apply(auto)[3]
using f0 apply(simp)
by (smt (verit, ccfv_SIG) lessThan_Suc_atMost rangeI sum.lessThan_Suc)
qed
lemma rewriting_sum: assumes ‹strict_mono (f::nat⇒nat)›
shows ‹(∑i<n. fps_const (s i) * fps_X^(f i))
= (∑i∈{..<f n}. (if i ∈ range f then fps_const (s (inv_into UNIV f i)) *fps_X^i else 0))›
proof(induct n)
case 0
then show ?case
by (simp add: assms inter_mt sum.If_cases )
next
case (Suc n)
then show ?case
apply(subst simp_rule_sum)
by(auto simp:assms strict_mono_on_imp_inj_on)
qed
lemma exists_seq:‹strict_mono (f::nat⇒nat) ⟹
∃s. (∑i∈{..<f n}. (if i ∈ range f then fps_const (s' (inv_into UNIV f i)) *fps_X^i else 0))
= (∑i∈{..<f n}. fps_const (s i) *fps_X^i)›
apply(rule exI[where x=‹λi. (if i ∈ range f then (s' ((inv_into UNIV f) i)) else 0) ›])
using rewriting_sum
by (smt (verit, best) fps_const_0_eq_0 lambda_zero sum.cong)
lemma exists_seq':‹strict_mono (f::nat⇒nat) ⟹
∃s. (∑i<n. fps_const (s' i) * (fps_X::'a fps)^(f i)) =
(∑i∈{..<f n}. fps_const (s i) *fps_X^i)›
apply(subst rewriting_sum[])
using exists_seq[of f ‹λi. (s' i)›]
by(auto)
lemma exists_seq_all:‹strict_mono (f::nat⇒nat) ⟹
∃s. ∀n. (∑i∈{..<f n}. (if i ∈ range f then fps_const (s' (inv_into UNIV f i)) *fps_X^i else 0))
= (∑i∈{..<f n}. fps_const (s i) *fps_X^i)›
apply(rule exI[where x=‹λi. (if i ∈ range f then (s' ((inv_into UNIV f) i)) else 0) ›])
using rewriting_sum
by (smt (verit, best) fps_const_0_eq_0 lambda_zero sum.cong)
lemma exists_seq_all':‹strict_mono (f::nat⇒nat) ⟹
∃s. ∀n. (∑i<n. fps_const (s' i) * fps_X^(f i)) =
(∑i∈{..<f n}. fps_const (s i) *fps_X^i)›
apply(subst rewriting_sum)
using exists_seq_all[of f ‹λi. (s' i)›]
by(auto)
lemma tendsto_f_seq:assumes ‹strict_mono (f::nat⇒nat)›
shows ‹(λn. (∑i∈{..<f n}. fps_const (s i) *fps_X^i)::'a fps) ⇢ Abs_fps (λi. s i)›
using fps_notation LIMSEQ_subseq_LIMSEQ[OF abs_tndsto_le[of s], of f] assms
by(auto simp:o_def)
lemma LIMSEQ_add_fps:
fixes x y :: "'a::idom fps"
assumes f:"f ⇢ x" and g:"(g ⇢ y)"
shows "((λx. f x + g x) ⇢ x + y)"
proof -
from f have ‹∀e>0. ∃n. ∀j≥n. dist (f j) x < e/2›
using lim_sequentially
using half_gt_zero by blast
from g have f0:‹∀e>0. ∃n. ∀j≥n. dist (g j) y < e/2›
using lim_sequentially half_gt_zero by blast
have f4:‹dist (f j - x) 0 = dist (f j) x› for j
unfolding dist_fps_def by(auto)
have f5:‹dist (g j - y) 0 = dist (g j) y› for j
by (metis diff_0_right dist_fps_def eq_iff_diff_eq_0)
then have f0':‹dist (f j + g j) (x + y) = dist (f j - x + g j - y) 0› for j
unfolding dist_fps_def
by (auto simp add: add.commute add_diff_eq diff_diff_eq2)
have f1:‹dist (f j - x + g j - y) 0 ≤ max (dist (f j - x) 0) (dist (g j - y) 0)› for j
unfolding dist_fps_def apply(auto simp:le_max_iff_disj field_simps)[1]
by (metis (no_types, lifting) add_diff_add eq_iff_diff_eq_0 min_le_iff_disj subdegree_add_ge')
then have f2:‹dist (f j - x + g j - y) 0 ≤ dist (f j - x) 0 + dist (g j - y) 0 › for j
by (smt (verit) zero_le_dist)
from f0 have f3:‹∀e>0. ∃n. ∀j≥n. dist (f j) x + dist (g j) y < e/2 + e/2›
by (metis ‹∀e>0. ∃n. ∀j≥n. dist (f j) x < e / 2› add_strict_mono le_trans linorder_le_cases)
then show ?thesis
unfolding LIMSEQ_def
by (metis f0' f2 f4 f5 field_sum_of_halves order_le_less_trans)
qed
lemma LIMSEQ_cmult_fps:
fixes x y :: "'a::idom fps"
assumes f:"f ⇢ x"
shows "((λx. c * f x) ⇢ c*x)"
proof -
from f have ‹∀e>0. ∃n. ∀j≥n. dist (f j) x < e›
using lim_sequentially
using half_gt_zero by blast
have ‹dist (c*f j - c*x) 0 = dist (c*(f j)) (c*x) › for j
unfolding dist_fps_def by auto
have ‹∀i≤n . fps_nth (f j) i = fps_nth x i ⟹
(∑i = 0..n. fps_nth c i * fps_nth (f j) (n - i)) = (∑i = 0..n. fps_nth c i * fps_nth x (n - i))›
for j n
using diff_le_self by presburger
have ‹c≠0 ⟹ dist (f j) x ≥ dist (c*f j) (c*x)› for j
proof(cases ‹x = f j›)
case True
then show ?thesis
unfolding dist_fps_def subdegree_def
by(auto)
next
case False
then have rule_su:‹(LEAST n. fps_nth (f j) n ≠ fps_nth x n) ≤
(LEAST n. fps_nth (c * f j) n ≠ fps_nth (c * x) n)
⟹ c≠0 ⟹ dist (c * f j) (c * x) ≤ dist (f j) x›
unfolding dist_fps_def subdegree_def by(auto)
have f0:‹n < (LEAST n. fps_nth (f j) n ≠ fps_nth x n) ⟹
(∑i = 0..n. fps_nth c i * fps_nth (f j) (n - i)) = (∑i = 0..n. fps_nth c i * fps_nth x (n - i))›
for n
by (metis (mono_tags, lifting) less_imp_diff_less not_less_Least)
have f1:‹∀n. (∑i = 0..n. fps_nth c i * fps_nth (f j) (n - i))
= (∑i = 0..n. fps_nth c i * fps_nth x (n - i)) ⟹
x ≠ f j ⟹ c ≠ 0 ⟹ (LEAST n. fps_nth (f j) n ≠ fps_nth x n) ≤ (LEAST n. False)›
(is ‹?P ⟹ ?R1 ⟹ ?R2 ⟹ ?R3›)
proof -
assume a1: "c ≠ 0"
assume a2: "x ≠ f j"
assume "∀n. (∑i = 0..n. fps_nth c i * fps_nth (f j) (n - i)) =
(∑i = 0..n. fps_nth c i * fps_nth x (n - i))" (is ?P)
then show "(LEAST n. fps_nth (f j) n ≠ fps_nth x n) ≤ (LEAST n. False)"
using a2 a1 by (metis (no_types) fps_ext fps_mult_nth mult_cancel_left)
qed
have f2:‹x ≠ f j ⟹ c ≠ 0 ⟹ (LEAST n. fps_nth (f j) n ≠ fps_nth x n)
≤ (LEAST n. (∑i = 0..n. fps_nth c i * fps_nth (f j) (n - i)) ≠
(∑i = 0..n. fps_nth c i * fps_nth x (n - i)))› (is ‹?R1⟹?R2⟹?P1›)
proof (cases ‹?P›)
case True
assume ‹x≠f j› ‹c≠0›
then show ?thesis using True f1 by(auto)
next
case False
assume a1: "c ≠ 0"
assume a2: "x ≠ f j"
show ?thesis
proof(insert False a1 a2, rule ccontr)
fix n
assume **:‹¬ ?P›
assume *:‹¬ ?P1›
(is ‹¬ ?a ≤ ?b›)
then have ‹fps_nth (f j) ?b = fps_nth (f j) ?b›
by blast
also have ‹(∑i = 0..?b. fps_nth c i * fps_nth (f j) (?b - i))
≠ (∑i = 0..?b. fps_nth c i * fps_nth x (?b - i))›
using *
by (smt (verit, best) "**" LeastI sum.cong)
thus False
using "*" f0 linorder_not_le by blast
qed
qed
from False show ?thesis
unfolding dist_fps_def subdegree_def
by (simp add: f2 fps_mult_nth)
qed
then show ?thesis
unfolding LIMSEQ_def
by (metis ‹∀e>0. ∃n. ∀j≥n. dist (f j) x < e› dist_self lambda_zero order_le_less_trans)
qed
subsection ‹The Hilbert Basis theorem›
theorem Hilbert_basis_FPS:
assumes h2:‹noetherian_ring R›
shows ‹noetherian_ring FPS_ring›
proof(rule ring.noetherian_ringI)
show fst:‹ring FPS_ring›
by (simp add: ring_FPS)
fix I
assume h1:‹ideal I FPS_ring›
show ‹∃A⊆carrier FPS_ring. finite A ∧ I = Idl⇘FPS_ring⇙ A›
proof(cases ‹I={0} ∨ I = carrier FPS_ring›)
case True
then show ?thesis apply(safe)
apply(rule exI[where x=‹{0}›])
apply(simp add:genideal_def)
using h1 ideal.Icarr apply fastforce
apply(rule exI[where x=‹{1}›])
using ideal.I_l_closed by(fastforce simp:FPS_ring_def genideal_def)
next
case False
have f0:‹subset.chain {I. ideal I R} {(sublead_coeff_set I k)|k. k∈UNIV} ›
unfolding subset_chain_def using included_sublead_gen[OF h1] sublead_ideal[OF h1]
by (smt (verit, ccfv_threshold) mem_Collect_eq nle_le subsetI)
have f2:‹{(sublead_coeff_set I k)|k. k∈UNIV} ≠ {}›
using h1 by(auto)
have ‹genideal R S = genideal R (S∪{0})› for S
unfolding genideal_def
by (metis R Un_insert_right additive_subgroup.zero_closed
ideal.axioms(1) insert_subset ring.simps(1) sup_bot_right)
have ‹ (⋃k. sublead_coeff_set I k) ∈ { sublead_coeff_set I m|m. m∈UNIV}›
by (smt (verit, best) Collect_cong full_SetCompr_eq h1 h2 image_iff mem_Collect_eq sup_sublead)
then have ‹∃m. (⋃k. sublead_coeff_set I k) = sublead_coeff_set I m› by auto
then obtain m where f60:‹ (⋃k. sublead_coeff_set I k) = sublead_coeff_set I m ∧ m>0›
by (metis Formal_Power_Series_Ring.included_sublead_gen UNIV_I UN_upper
bot_nat_0.extremum dual_order.eq_iff h1 less_Suc0 neq0_conv)
have ‹∀k≥m. sublead_coeff_set I m = sublead_coeff_set I k›
using Formal_Power_Series_Ring.included_sublead_gen f60 h1 by auto
from f2 have ‹∃S. ∀k. finite (S k) ∧ (sublead_coeff_set I k) = genideal R (S k)›
using h2 h1 sublead_ideal[OF h1] unfolding noetherian_ring_def noetherian_ring_axioms_def
by meson
then obtain S where f4:‹∀k. finite (S k) ∧ (sublead_coeff_set I k) = genideal R (S k)› by blast
then have
‹∃S. ∀k. finite (S k)∧ 0∉S k ∧ (sublead_coeff_set I k) = genideal R (S k) ∧ (∀k≥m. S k = S m)›
apply(intro exI[where x= ‹(λk. if k≤m then S k - {0} else S m - {0})›])
by (smt (verit, ccfv_threshold) Diff_iff Un_Diff_cancel Un_commute ‹⋀S. Idl S = Idl (S ∪ {0})›
‹∀k≥m. sublead_coeff_set I m = sublead_coeff_set I k› finite_Diff nle_le singletonI)
then obtain S' where f5:
‹∀k. finite (S' k)∧ 0 ∉ S' k ∧ (sublead_coeff_set I k) = genideal R (S' k) ∧ (∀k≥m. S' k = S' m)›
by blast
have *:‹∀x∈(S' j). ∃y∈I. subdegree y = j ∧ fps_nth y j = x› for j
proof (safe)
fix x
assume h3:‹x∈S' j›
then have ‹x∈sublead_coeff_set I j›
using f5 unfolding genideal_def by(auto)
then show ‹∃y∈I. subdegree y = j ∧ fps_nth y j = x›
unfolding sublead_coeff_set_def subdeg_poly_set using f5
using h3 by auto
qed
define f where ‹f = (λj x. (SOME y. y∈I ∧ subdegree y = j ∧ fps_nth y j = x))›
define B where ‹B = (λj. {f j x|x. x∈S' j})›
have ‹bij_betw (f k) (S' k) (B k)› for k
apply(rule bij_betwI[where g=‹λx. fps_nth x k›])
using B_def apply blast
using f5 B_def image_def f_def Pi_def apply(safe)
apply (smt (verit, del_insts) "*" someI_ex)
apply (smt (verit, del_insts) "*" f_def someI_ex)
unfolding f_def B_def image_def
apply(safe)
by (smt (verit, ccfv_threshold) "*" Eps_cong someI_ex)
then have f6:‹card (B j) = card (S' j)› for j
by (metis bij_betw_same_card)
have f7:‹bij_betw (from_nat_into (B k)) ({0..<card (B k)}) (B k)› for k
by (simp add: B_def atLeast0LessThan bij_betw_from_nat_into_finite f5)
have f8:‹bij_betw (from_nat_into (S' k)) ({0..<card (S' k)}) (S' k)› for k
by (simp add: B_def atLeast0LessThan bij_betw_from_nat_into_finite f5)
have ‹∀x∈ S' k. ∃y∈B k. x = fps_nth y k› for k
using f5 unfolding B_def f_def sublead_coeff_set_def subdeg_poly_set
apply(safe)
by (smt (verit, ccfv_threshold) "*" mem_Collect_eq someI_ex)
have f30:‹∀x∈ B k. ∃y∈S' k. y = fps_nth x k› for k
using f5 unfolding B_def f_def sublead_coeff_set_def subdeg_poly_set
apply(safe)
by (smt (verit, ccfv_threshold) "*" mem_Collect_eq someI_ex)
have ‹∀i<card (B k). ∃!n. n<card (B k) ∧ fps_nth (from_nat_into (B k) n) k = from_nat_into (S' k) i›
for k
proof(safe)
fix i
assume ‹i<card (B k)›
then have ‹from_nat_into (S' k) i ∈ S' k›
by (metis card.empty f6 from_nat_into less_nat_zero_code)
then show ‹∃n<card (B k). fps_nth (from_nat_into (B k) n) k = from_nat_into (S' k) i›
by (smt (verit, ccfv_threshold) ‹⋀k. ∀x∈S' k. ∃y∈B k. x = fps_nth y k›
atLeastLessThan_iff bij_betw_iff_bijections f7)
next
have f9:‹h∈B k ∧ g∈ B k ⟹ h ≠ g ⟷ fps_nth h k ≠ fps_nth g k› for k h g
using f5 unfolding B_def f_def sublead_coeff_set_def subdeg_poly_set apply(safe)
by (smt (verit) "*" someI_ex)+
fix i n y
assume ‹i < card (B k)› ‹n < card (B k)›
‹fps_nth (from_nat_into (B k) n) k = from_nat_into (S' k) i› ‹y < card (B k)›
‹fps_nth (from_nat_into (B k) y) k = from_nat_into (S' k) i›
then have ‹(from_nat_into (B k) n) = (from_nat_into (B k) y)›
using f9
by (metis card.empty from_nat_into less_nat_zero_code)
then show ‹n = y› using f7 unfolding bij_betw_def inj_on_def
by (metis (no_types, opaque_lifting) ‹n < card (B k)› ‹y < card (B k)›
atLeastLessThan_iff bij_betw_iff_bijections f7 zero_le)
qed
then have ‹∃p. (∀i<card (S' k). fps_nth (from_nat_into (B k) (p i)) k = from_nat_into (S' k) i)›
for k
apply(intro exI[where x=‹λi. THE n. n<card (B k)
∧ fps_nth (from_nat_into (B k) (n)) k = from_nat_into (S' k) i›])
apply(safe)
by (smt (z3) f6 theI')
then obtain p
where f11:‹(∀i<card (S' k). fps_nth (from_nat_into (B k) (p k i)) k = from_nat_into (S' k) i)›
for k
by metis
have ‹x≠y ⟹ x∈S' j ∧ y∈S' j⟹ (SOME y. y∈I ∧ subdegree y = j ∧ fps_nth y j = x)
≠ (SOME y'. y'∈I ∧ subdegree y' = j ∧ fps_nth y' j = y)› for x y j
using *
apply(safe)
by (smt (verit, best) someI_ex)
then have ‹∀x y. x∈S' j ∧ y∈S' j ∧ x≠y ⟶ f j x ≠ f j y› for j
unfolding f_def by(auto)
have f10:‹finite (B j)› for j
using f6 f5 B_def
using ‹⋀k. bij_betw (f k) (S' k) (B k)› bij_betw_finite by blast
from idl_sum
have ‹∀x∈sublead_coeff_set I m. (∃s. x = (∑i∈{0..<card (S m)}. s i * from_nat_into (S m) i))›
using f4 genideal_sum_rep by blast
have ‹genideal R {} = {0}›
unfolding genideal_def
proof(safe)
fix x
assume 1:‹ x ∈ ⋂ {I. ideal I R ∧ {} ⊆ I} › ‹x ∉ {}›
have ‹ideal ({0}) R›
using R ring.zeroideal ring_R by fastforce
then have ‹x∈{0}› using 1 by auto
then show ‹x=0› by auto
next
fix X
assume 2:‹ideal X R› ‹{}⊆X›
then show ‹0∈X›
using R additive_subgroup.zero_closed ideal.axioms(1) by fastforce
qed
have ‹sublead_coeff_set I m ≠ {0} ⟹ S m ≠ {}›
using ‹Idl {} = {0}› f4 by force
define I' where ‹I' ≡ genideal FPS_ring (⋃k≤m. B k)›
have f62:‹(⋃k≤m. B k) ⊆ I ∧ finite (⋃k≤m. B k)›
apply(rule conjI)
using B_def f_def f10 apply(auto simp:image_def * some_eq_ex)[1]
apply (smt (verit, del_insts) "*" some_eq_ex)
using f10 apply(induct m) by(auto)
then have ‹I' ⊆ I›
unfolding I'_def
by (meson Formal_Power_Series_Ring.ring_FPS h1 ring.genideal_minimal)
have ‹∀k≥m. S' m = S' k›
using f5 by blast
have eq_fps_S':‹{fps_nth f k|f. f∈B k} = S' k› for k
unfolding B_def f_def apply(safe)
using B_def f30 f_def apply blast
using B_def ‹⋀k. ∀x∈S' k. ∃y∈B k. x = fps_nth y k› f_def by blast
{
fix f m'
assume h9:‹f ≠ 0› ‹f∈I› ‹subdegree f ≤ m› ‹f∉I'› ‹subdegree f = m'›
with h9 have ‹fps_nth f m' ∈ sublead_coeff_set I m'›
unfolding sublead_coeff_set_def subdeg_poly_set
by blast
then have ‹∃s. fps_nth f m' = (∑k=0..<card (S' m'). (s k)*from_nat_into (S' m') k)›
using f5
using genideal_sum_rep by blast
then obtain s where f12:‹fps_nth f m' = (∑k=0..<card (S' m'). (s k)*from_nat_into (S' m') k)›
by blast
then have f21:‹(∑k=0..<card (S' m'). (s k)*from_nat_into (S' m') k)
= fps_nth (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k)) m'›
using f11
apply(subst fps_sum_nth)
apply(subst fps_mult_left_const_nth)
using f6 by fastforce
then have f14:
‹fps_nth f m' = fps_nth (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k)) m'›
using f11 f12 by auto
then have
‹fps_nth ((f - (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k)))) m' = 0›
by auto
have f22:‹(from_nat_into (B m') (p m' ka)) ∈ B m'› for ka
by (metis atLeastLessThan0 card.empty f12 f6 from_nat_into h9(1)
h9(5) nth_subdegree_zero_iff sum.empty)
then have f13:‹∀k<m'. fps_nth (from_nat_into (B m') (p m' ka)) k = 0› for ka
unfolding B_def f_def using f5 unfolding sublead_coeff_set_def subdeg_poly_set
by (smt (verit, best) "*" h9 mem_Collect_eq nth_less_subdegree_zero someI_ex)
then have
‹∀ka<m'. fps_nth (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k)) ka = 0›
apply(subst fps_sum_nth)
apply(subst fps_mult_left_const_nth) apply(safe)
apply(subst f13) by(auto)
then have f18:‹ka≤m' ⟹ (fps_nth (f-(∑k=0..<card (B m').
(fps_const (s k))*from_nat_into (B m') (p m' k))) ka = 0)› for ka
apply(cases ‹ka=m'›)
using f14 apply fastforce
using nth_less_subdegree_zero
using h9(5) by force
have ‹from_nat_into (B m') (p m' k) ∈ I'› for k
using f22 unfolding I'_def genideal_def
using h9(3) h9(5) by blast
then have f23:‹(fps_const (s k))*from_nat_into (B m') (p m' k) ∈ I'› for k
by (metis FPS_ring_def I'_def UNIV_I ideal.I_l_closed monoid.select_convs(1)
partial_object.select_convs(1) ring.genideal_ideal ring_FPS subset_UNIV)
have f24:‹(∑k=0..<r. (fps_const (s k))*from_nat_into (B m') (p m' k)) ∈ I'› for r using f22
apply(induct r)
apply (metis (full_types) Formal_Power_Series_Ring.FPS_ring_def I'_def
additive_subgroup.zero_closed atLeastLessThan0 ideal_def partial_object.select_convs(1)
ring.genideal_ideal ring.simps(1) ring_FPS sum.empty top_greatest)
apply(subst sum.atLeast0_lessThan_Suc)
unfolding I'_def
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def I'_def
additive_subgroup.a_closed f23 ideal.axioms(1) partial_object.select_convs(1)
ring.genideal_ideal ring_FPS ring_record_simps(12) subset_UNIV)
then have f26:
‹(f - (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k))) = 0 ⟹ False›
using h9 by auto
have ‹subdegree (f - (∑k=0..<card (B m'). (fps_const (s k))*from_nat_into (B m') (p m' k))) > m'›
using f26
by (smt (verit, ccfv_SIG)f18 enat_ord_code(4) enat_ord_simps(1)
linorder_not_less nth_subdegree_zero_iff)
then have ‹∃g∈I'. subdegree (f + g) > m'∧ (f + g) ≠ 0›
using f26
apply(intro bexI[where x=‹- (∑k=0..<card (B m'). (fps_const (s k))*
from_nat_into (B m') (p m' k))›])
using f26 f24 apply(safe)
apply(auto)[2]
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def
Formal_Power_Series_Ring.ring_FPS I'_def UNIV_I ideal.I_l_closed monoid.select_convs(1)
mult_1s(3) partial_object.select_convs(1) ring.genideal_ideal subset_UNIV)
} note first = this
{
fix f
assume h10:‹f≠0› ‹f∈I› ‹f∉I'› ‹subdegree f < m›
have ‹∃g∈I'. subdegree (f + g) > subdegree f ∧ f+g ≠0 ›
using first[OF h10(1) h10(2) _ h10(3)]
using h10(4) nat_less_le
by blast
have ‹∃g∈I'. subdegree (f + g) ≥ m' ∧ f+g ≠0› if hh:‹m'≤m› for m'
using hh h10 proof(induct m' arbitrary:f)
case 0
then show ?case
using first less_or_eq_imp_le by blast
next
case (Suc m')
then obtain g where g1:‹g∈I' ∧ subdegree (f + g) ≥ m' ∧ f+g ≠0›
using first order_less_imp_le
by (metis less_Suc_eq_le nle_le)
{assume hh1:"subdegree (f+g) < Suc m'"
with g1 have g2:‹subdegree (f+g) = m'›
by auto
have g3:‹f+g ∈ I›
by (metis Formal_Power_Series_Ring.FPS_ring_def Suc.prems(3)
‹I' ⊆ I› additive_subgroup.a_closed g1 h1 ideal.axioms(1)
in_mono ring_record_simps(12))
have g4:‹f+g ∉ I'›
proof(rule ccontr)
assume ‹¬f+g ∉ I'›
have ‹-g ∈ I'›
using g1 unfolding I'_def
by (metis (no_types, lifting) FPS_ring_def Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum UNIV_I f62 ideal.I_l_closed monoid.select_convs(1)
mult_1s(3) partial_object.select_convs(1))
then have ‹f+g-g ∈ I'›
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def
Formal_Power_Series_Ring.genideal_sum_rep Formal_Power_Series_Ring.idl_sum I'_def
Suc.prems(4) f62 ‹¬f+g ∉ I'› add.commute additive_subgroup.a_closed ideal.axioms(1)
minus_add_cancel ring_record_simps(12))
then have ‹f∈I'› by auto
then show False
using Suc.prems(4) by auto
qed
have g5: ‹subdegree (f+g)≤m›
by (simp add: Suc.prems(1) Suc_leD g2)
then obtain g' where ‹g'∈I' ∧ subdegree (f + g +g') > subdegree (f+g) ∧ f+g+g' ≠0›
using first[OF _ g3 g5 g4, of m']
using g1 g2 by blast
then have ‹subdegree (f+g+g') ≥ Suc m'›
using Suc_le_eq g2 by blast
then have ‹∃g'∈I'. subdegree (f + g +g') ≥ Suc m' ∧ f+g+g' ≠0›
using ‹g' ∈ I' ∧ subdegree (f + g) < subdegree (f + g + g') ∧ f + g + g' ≠ 0› by blast
}note proof1=this
then obtain g' where ttt:‹subdegree (f+g) <Suc m' ⟹ g' ∈ I' ∧
subdegree (f + g) < subdegree (f + g + g') ∧ f + g + g' ≠ 0›
using order_less_le_trans by blast
show ?case apply(cases ‹subdegree (f+g) ≥Suc m'›)
using g1 apply blast
using proof1
apply(intro bexI[where x=‹g +g'›])
apply (metis Suc_leI ab_semigroup_add_class.add_ac(1)
g1 le_less_Suc_eq linorder_not_less ttt)
unfolding I'_def
by (metis (no_types, lifting) FPS_ring_def Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum I'_def ‹⋃ (B ` {..m}) ⊆ I ∧ finite (⋃ (B ` {..m}))›
additive_subgroup.a_closed g1 ideal.axioms(1) linorder_not_less ring_record_simps(12) ttt)
qed
} note snd=this
{
fix f m'
assume h9:‹f ≠ 0› ‹f∈I› ‹subdegree f ≥ m› ‹subdegree f = m'› ‹f∉I'›
then have ‹fps_nth f m' ∈ sublead_coeff_set I m'›
unfolding sublead_coeff_set_def subdeg_poly_set by auto
then have f28:‹fps_nth f m' ∈ sublead_coeff_set I m›
‹sublead_coeff_set I m' = genideal R (S' m)›
using ‹∀k≥m. sublead_coeff_set I m = sublead_coeff_set I k›
h9 less_or_eq_imp_le apply blast
using f5 by (metis h9(3-4))
then have ‹∃s. fps_nth f m' = (∑k=0..<card (S' m). (s k)*from_nat_into (S' m) k)›
using genideal_sum_rep f5 by blast
then obtain s where f12:‹fps_nth f m' = (∑k=0..<card (S' m). (s k)*from_nat_into (S' m) k)›
by blast
then have f21:‹(∑k=0..<card (S' m). (s k)*from_nat_into (S' m) k)
=fps_nth (∑k=0..<card (B m). (fps_const (s k))*from_nat_into (B m) (p m k)) m›
using f11
apply(subst fps_sum_nth)
apply(subst fps_mult_left_const_nth)
using f6 by fastforce
then have f14:
‹fps_nth f m' = fps_nth (∑k=0..<card (B m). (fps_const (s k))*from_nat_into (B m) (p m k)) m›
using f11 f12 by auto
have f22:‹(from_nat_into (B m) (p m ka)) ∈ B m› for ka
by (metis atLeastLessThan0 card.empty f12 f6 from_nat_into h9(1) h9(4)
nth_subdegree_zero_iff sum.empty)
then have ‹subdegree (from_nat_into (B m) (p m k)) = m› for k
unfolding B_def f_def sublead_coeff_set_def subdeg_poly_set
by (smt (verit, best) "*" h9 mem_Collect_eq nth_less_subdegree_zero someI_ex)
then have f32:‹subdegree ((fps_X^(m'-m))*from_nat_into (B m) (p m k)) = m'› for k
using fps_subdegree_mult_fps_X_power(1)
by (metis f30 f22 f5 h9(3) h9(4) le_add_diff_inverse nth_subdegree_zero_iff)
have f31:
‹fps_nth ((fps_X^(m'-m))*from_nat_into (B m) (p m k)) m' = fps_nth (from_nat_into (B m) (p m k)) m›
for k
by (metis diff_diff_cancel diff_le_self fps_X_power_mult_nth h9(3) h9(4) linorder_not_less)
then have f31b:‹fps_nth (fps_const (s k)*(fps_X^(m'-m))*from_nat_into (B m) (p m k)) m' =
fps_nth (fps_const (s k)*from_nat_into (B m) (p m k)) m› for k
by (simp add: mult.assoc)
then have f33:‹fps_nth f m' = fps_nth (∑k=0..<card (B m). (fps_const (s k))*(fps_X^(m'-m))*
from_nat_into (B m) (p m k)) m'›
apply(subst fps_sum_nth)
apply(subst f31b)
apply(subst fps_mult_left_const_nth)
by (simp add: f14 fps_sum_nth)
then have f36:‹fps_nth ((f - (∑k=0..<card (B m). (fps_const (s k))*(fps_X^(m'-m))*
from_nat_into (B m) (p m k)))) m' = 0›
by auto
have ‹from_nat_into (B m) (p m k) ∈ I'› for k
using f22 unfolding I'_def genideal_def
using h9 by blast
then have f23:‹(fps_const (s k))*from_nat_into (B m) (p m k) ∈ I'› for k
by (metis FPS_ring_def I'_def UNIV_I ideal.I_l_closed monoid.select_convs(1)
partial_object.select_convs(1) ring.genideal_ideal ring_FPS subset_UNIV)
then have f23:‹(fps_const (s k))*fps_X^(m'-m)*from_nat_into (B m) (p m k) ∈ I'› for k
by (metis (no_types, lifting) FPS_ring_def Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum I'_def UNIV_I ‹⋀k. from_nat_into (B m) (p m k) ∈ I'›
f62 ideal.I_l_closed monoid.select_convs(1) partial_object.select_convs(1))
have f24:‹(∑k=0..<r. (fps_const (s k))*fps_X^(m'-m)*from_nat_into (B m) (p m k)) ∈ I'›
for r
using f22
apply(induct r)
apply(simp)
apply (metis (full_types) Formal_Power_Series_Ring.FPS_ring_def I'_def additive_subgroup.zero_closed
ideal_def partial_object.select_convs(1) ring.genideal_ideal ring.simps(1) ring_FPS top_greatest)
apply(subst sum.atLeast0_lessThan_Suc)
unfolding I'_def
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def I'_def
additive_subgroup.a_closed f23 ideal.axioms(1) partial_object.select_convs(1)
ring.genideal_ideal ring_FPS ring_record_simps(12) subset_UNIV)
then have f26:
‹(f - (∑k=0..<card (B m). (fps_const (s k))*fps_X^(m'-m)*from_nat_into (B m) (p m k))) = 0 ⟹ False›
(is ‹f - ?A = 0⟹False›) using h9 by auto
have ‹∀i<m'. fps_nth ((fps_const (s k))*(fps_X^(m'-m))*from_nat_into (B m) (p m k)) i = 0›
for k
using f32
by (metis ab_semigroup_mult_class.mult_ac(1) fps_mult_nth_outside_subdegrees(2))
then have f34:‹∀i<m'. fps_nth (?A) i = 0›
apply(subst fps_sum_nth)
by(auto)
then have f35:‹subdegree ?A = m'›
by (metis (no_types, lifting) f33 h9(1) h9(4) nth_subdegree_nonzero subdegreeI)
have ‹x∈I' ⟹ -x∈I'› for x
unfolding I'_def FPS_ring_def
by (metis (no_types, lifting) Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum UNIV_I f62
ideal.I_l_closed monoid.select_convs(1) mult_1s(3) partial_object.select_convs(1))
have f39:‹subdegree (- ?A) ≥ m›
using subdegree_uminus[of ?A] f35 h9 by argo
have ‹subdegree (f - (∑k=0..<card (B m).
(fps_const (s k))*(fps_X^(m'-m))*from_nat_into (B m) (p m k))) > m'›
using h9 f33
by (metis (no_types, lifting) f36 f35 diff_zero f26 fps_sub_nth le_neq_implies_less
nth_subdegree_nonzero subdegree_leI)
then have ‹∃g. ∃s. g=- (∑k=0..<card (B m). (fps_const (s k))*(fps_X^(m'-m))*
from_nat_into (B m) (p m k)) ∧ subdegree (f + g) > m' ∧ (f +g) ≠ 0 ∧ g ∈ I' ∧ subdegree (g) ≥ m›
using f26 f24 ‹⋀x. x ∈ I' ⟹ - x ∈ I'› f39
by (metis (no_types, lifting) add_uminus_conv_diff)
}note thrd=this
have in_I':‹x∈I' ⟹ -x∈I'› for x
unfolding I'_def FPS_ring_def
by (metis (no_types, lifting) Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum UNIV_I ‹⋃ (B ` {..m}) ⊆ I ∧ finite (⋃ (B ` {..m}))›
ideal.I_l_closed monoid.select_convs(1) mult_1s(3) partial_object.select_convs(1))
have ‹I⊆I'›
proof(safe, rule ccontr)
fix f
assume h10:‹f∈I› ‹f∉I'›
then have f40:‹f≠0›
by (metis FPS_ring_def I'_def additive_subgroup.zero_closed ideal.axioms(1)
partial_object.select_convs(1) ring.genideal_ideal ring.simps(1) ring_FPS subset_UNIV)
have ‹ ∃g∈I'. subdegree (f + g) ≥ m ∧ f+g≠0›
using snd[OF f40 h10 ]
by (metis Formal_Power_Series_Ring.FPS_ring_def Formal_Power_Series_Ring.ring_FPS I'_def
add.right_neutral additive_subgroup.zero_closed f40 ideal.axioms(1) linorder_not_less
order_refl partial_object.select_convs(1) ring.genideal_ideal ring.simps(1) subset_UNIV)
then obtain g where f41:‹g∈I' ∧ subdegree (f + g) ≥ m ∧ f+g≠0› by blast
then have hyps:‹f+g≠0› ‹f+g ∈ I› ‹subdegree(f+g)≥m› ‹(f+g)∉I'›
proof -
show ‹f + g ≠ 0› ‹m ≤ subdegree (f + g)› using f41 by auto
have ‹g∈I›
using ‹I' ⊆ I› f41 by blast
then show ‹f + g ∈ I›
by (metis FPS_ring_def additive_subgroup.a_closed h1 h10(1) ideal_def ring_record_simps(12))
show ‹f + g ∉ I'›
proof(rule ccontr)
assume ‹¬f+g ∉ I'›
have ‹-g ∈ I'›
unfolding I'_def FPS_ring_def
by (metis Formal_Power_Series_Ring.FPS_ring_def Formal_Power_Series_Ring.ring_R I'_def
f41 ideal.I_l_closed iso_tuple_UNIV_I monoid.select_convs(1) mult_minus1
partial_object.select_convs(1) ring.genideal_ideal subset_UNIV)
then have ‹f+g-g ∈ I'›
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def
Formal_Power_Series_Ring.genideal_sum_rep Formal_Power_Series_Ring.idl_sum I'_def
f62 ‹¬ f + g ∉ I'› add_stable_FPS_ring uminus_add_conv_diff)
then have ‹f∈I'› by auto
then show False
using h10(2) by blast
qed
qed
define the_s where ‹the_s ≡ rec_nat (f+g)
(λn sn. sn + (SOME g. ∃s. g = -(∑k=0..<card (B m). (fps_const (s k))*(fps_X^(subdegree sn - m))
*from_nat_into (B m) (p m k))
∧ subdegree (sn + g) > subdegree sn ∧ (sn +g) ≠ 0 ∧ g∈I' ∧ subdegree g ≥m))›
have subst_rec:‹ the_s (Suc n) = the_s n + (SOME g. ∃s. g = - (∑k=0..<card (B m).
(fps_const (s k))*(fps_X^(subdegree (the_s (n)) - m))*from_nat_into (B m) (p m k))
∧ subdegree ((the_s (n)) + g) > subdegree (the_s (n)) ∧ ((the_s (n)) + g) ≠ 0
∧ g∈I'∧subdegree g ≥m)› for n
unfolding the_s_def
apply(induct n)
by (meson old.nat.simps(7))+
have hyps_thes:‹the_s n ≠ 0∧the_s n ∈ I∧subdegree(the_s n)≥m∧(the_s n)∉I'› for n
proof(induct n)
case 0
then show ?case unfolding the_s_def using hyps by auto
next
case (Suc n)
then have y1:‹the_s n ≠ 0› and y2: ‹the_s n ∈ I› and y3:‹m ≤ subdegree (the_s n)›
and y4:‹the_s n ∉ I'›
by auto
have f50:‹ ∃g. ∃s. g = - (∑k = 0..<card (B m). fps_const (s k) * fps_X ^
(subdegree (the_s n) - m) * from_nat_into (B m) (p m k)) ∧ subdegree (the_s n) <
subdegree (the_s n + g) ∧ the_s n + g ≠ 0 ∧ g∈I'∧subdegree g ≥m›
using thrd[OF y1 y2 y3 _ y4, of ‹subdegree (the_s n)›] by auto
let ?g = ‹(SOME g. ∃s. g = - (∑k = 0..<card (B m). fps_const (s k) * fps_X ^
(subdegree (the_s n) - m) * from_nat_into (B m) (p m k)) ∧ subdegree (the_s n) <
subdegree (the_s n + g) ∧the_s n + g ≠ 0 ∧ g∈I'∧subdegree g ≥m)›
have ‹the_s (Suc n) ∉ I'›
proof(subst subst_rec, rule ccontr)
assume h100: ‹¬the_s n+?g ∉ I'›
have ‹?g∈I'›
by(smt someI_ex f50)
then have ‹-?g ∈ I'›
using in_I' by auto
then have ‹the_s n+?g-?g ∈ I'›
by (metis (no_types, lifting) Formal_Power_Series_Ring.FPS_ring_def
Formal_Power_Series_Ring.genideal_sum_rep Formal_Power_Series_Ring.idl_sum I'_def
f62 h100 add_stable_FPS_ring add_uminus_conv_diff)
then have ‹the_s n∈I'› by auto
then show False
using y4 by blast
qed
have ‹the_s (Suc n) ∈ I›
proof(subst subst_rec)
have ‹?g∈I'›
by(smt someI_ex f50)
then show ‹the_s n + ?g ∈ I›
using ‹I' ⊆ I› add_stable_FPS_ring h1 y2 by blast
qed
have f51:‹the_s (Suc n) ≠ 0›
apply(subst subst_rec)
by (smt someI_ex f50)
have ‹m ≤ subdegree (the_s (Suc n))›
proof(subst subst_rec)
have ‹subdegree ?g ≥m›
by (smt someI_ex f50)
then show ‹m≤subdegree (the_s n + ?g)›
using f51 apply(subst (asm) subst_rec)
by (smt (verit) add_diff_cancel_left' dual_order.trans f50 linorder_le_less_linear
subdegree_diff_eq1 subdegree_diff_eq2 y1)
qed
then show ?case
using ‹the_s (Suc n) ∈ I› ‹the_s (Suc n) ∉ I'› f51 by blast
qed
have f53:‹∀n. ∃g. ∃s. g = - (∑k=0..<card (B m). (fps_const (s k))*
(fps_X^(subdegree (the_s (n)) - m))*from_nat_into (B m) (p m k))
∧ subdegree ((the_s (n)) + g) > subdegree (the_s (n))
∧ ((the_s (n)) + g) ≠ 0 ∧ g∈I'∧subdegree g ≥m›
using thrd hyps_thes by blast
then have f53':‹∀ n. ∃g. ∃s. the_s (Suc n) = the_s n + g ∧ g = - (∑k=0..<card (B m).
(fps_const (s k))*(fps_X^(subdegree (the_s (n)) - m))*from_nat_into (B m) (p m k)) ∧
subdegree ((the_s (n)) + g) > subdegree (the_s (n)) ∧ ((the_s (n)) + g) ≠ 0 ∧ g∈I'∧subdegree g ≥m›
apply(subst subst_rec)
by (smt (z3) tfl_some)
from f53 have ‹subdegree (the_s n) < subdegree (the_s (Suc n))› for n
apply(subst subst_rec)
by (smt someI_ex f53 sum.cong)
then have f56:‹strict_mono (λn. subdegree (the_s n))›
using strict_mono_Suc_iff by blast
have f70:‹strict_mono (λk. subdegree(the_s k) - m)›
using f56 unfolding strict_mono_def
using diff_less_mono hyps_thes by presburger
let ?f =‹λk. subdegree (the_s k) - m›
have ‹bij_betw ?f UNIV (range ?f)›
by (simp add: ‹strict_mono ?f› bij_betw_imageI strict_mono_on_imp_inj_on)
from f56 have f80:‹the_s ⇢ 0›
using subdeg_inf_imp_s_tendsto_zero by blast
have f54:‹∃g' s'. ∀n. g' n = -(∑k=0..<card (B m). (fps_const (s' n k))*
(fps_X^(subdegree (the_s n) - m))*from_nat_into (B m) (p m k))
∧ subdegree ((the_s n) + (g' n)) > subdegree (the_s n) ∧ ((the_s n) +g' n) ≠ 0 ∧ g' n∈I'
∧ subdegree (g' n) ≥m›
using f53 by meson
have ‹∃g' s'. ∀n. the_s (Suc n) = the_s n + g' n ∧ g' n = -(∑k=0..<card (B m).
(fps_const (s' n k))*(fps_X^(subdegree (the_s n) - m))*from_nat_into (B m) (p m k))
∧ subdegree ((the_s n) + (g' n)) > subdegree (the_s n) ∧ ((the_s n) +g' n) ≠ 0 ∧ g' n∈I'
∧ subdegree (g' n) ≥m›
using f53' by meson
then obtain g' s' where f55:‹∀n. the_s (Suc n) = the_s n + g' n ∧ g' n = -(∑k=0..<card (B m).
(fps_const (s' n k))*(fps_X^(subdegree (the_s n) - m))*from_nat_into (B m) (p m k))
∧ subdegree ((the_s n) + (g' n)) > subdegree (the_s n) ∧ ((the_s n) +g' n) ≠ 0 ∧ g' n∈I'
∧ subdegree (g' n) ≥m›
by blast
then have ‹∀n. ∃s. ∀k. s' n k = s (subdegree (the_s n) - m) k›
by force
have ‹the_s n = f+g + (∑k<n. (the_s (Suc k) - the_s k))› for n
apply(induct n)
apply(subst subst_rec[rule_format])
apply (simp add: the_s_def)
by simp
then have t1:‹f+g = the_s n - (∑k<n. (the_s (Suc k) - the_s k))› for n
by (metis (no_types, lifting) add_diff_cancel_right')
then have ‹f+g = the_s n - (∑k<n. g' k)› for n
by (simp add: f55)
then have ‹f+g = the_s n - (∑k<n. -(∑i=0..<card (B m). (fps_const (s' k i))*
(fps_X^(subdegree (the_s k) - m))*from_nat_into (B m) (p m i)))›for n
by(simp add:f55)
then have f87:‹f+g = the_s n + (∑k<n. (∑i=0..<card (B m). (fps_const (s' k i))*
(fps_X^(subdegree (the_s k) - m))*from_nat_into (B m) (p m i)))›
for n
by (simp add: sum_negf)
then have ‹f+g = the_s n + ((∑i=0..<card (B m). ∑k<n. (fps_const (s' k i))*
(fps_X^(subdegree (the_s k) - m))*from_nat_into (B m) (p m i)))› for n
proof -
assume "⋀n. f + g = the_s n + (∑k<n. ∑i = 0..<card (B m). fps_const
(s' k i) * fps_X ^ (subdegree (the_s k) - m) * from_nat_into (B m) (p m i))"
then have "f + g = the_s n + (∑n = 0..<n. ∑na = 0..<card (B m).
fps_const (s' n na) * fps_X ^ (subdegree (the_s n) - m) * from_nat_into (B m) (p m na))"
using atLeast0LessThan by moura
then show ?thesis
using atLeast0LessThan sum.swap by force
qed
then have f57:‹f+g = the_s n + ((∑i=0..<card (B m). (∑k<n. (fps_const (s' k i))*
(fps_X^(subdegree (the_s k) - m)))*from_nat_into (B m) (p m i)))›
for n
by(auto simp:sum_distrib_right)
have ‹(λn. (f+g)) - the_s = (λn. (f+g) + (-the_s n))›
by(auto simp:fun_eq_iff)
have ‹- the_s ⇢ 0›
apply(rule metric_LIMSEQ_I)
using f80
apply(drule metric_LIMSEQ_D)
unfolding dist_fps_def
by fastforce
then have f58:‹(λn. (f+g)) - the_s ⇢ f + g›
proof -
have "∀n. f + g + (- the_s) n = ((λn. f + g) - the_s) n"
by auto
then show ?thesis
by (metis (no_types) ‹- the_s ⇢ 0› LIMSEQ_add_fps[of ‹(λn. f + g)› ‹f+g› ‹-the_s› 0]
add.right_neutral lim_sequentially tendsto_const)
qed
then have ‹f+g = lim (λn. the_s n + ((∑i=0..<card (B m). (∑k<n. (fps_const (s' k i))*(fps_X^(subdegree (the_s k) - m)))*from_nat_into (B m) (p m i)))) ›
using f57 by auto
have ‹(λn. f+g) - the_s = (λn. (∑i=0..<card (B m). (∑k<n. (fps_const (s' k i))*(fps_X^(subdegree (the_s k) - m)))*from_nat_into (B m) (p m i)))›
using f57 apply(subst fun_eq_iff, safe)
by (smt (verit, best) add_diff_cancel_left' minus_apply)
then have ‹(λn. (∑i=0..<card (B m). (∑k<n. (fps_const (s' k i))*(fps_X^(subdegree (the_s k)
- m)))*from_nat_into (B m) (p m i))) ⇢ f+g›
(is ‹?S ⇢ f+g›) using f58 by presburger
then have f84:‹f+g = lim ?S›
by (simp add: limI)
have f63: ‹finite (⋃ (B ` {..m}))›
using f62 by fastforce
have ‹strict_mono (λk. subdegree ((∑i=0..<card (B m). (fps_const (s' k i))*
(fps_X^(subdegree (the_s k) - m))*from_nat_into (B m) (p m i))))›
apply(rule monotone_onI)
apply(insert f55 f56 hyps_thes)
by (smt (verit, ccfv_threshold) f87 add.commute add_left_cancel diff_add_cancel
strict_monoD subdeg_inf_imp_s_tendsto_zero subdegree_diff_eq2 subdegree_uminus sum_negf)
then have ‹(λk. (∑i=0..<card (B m). (fps_const (s' k i))*(fps_X^(subdegree (the_s k) - m))*
from_nat_into (B m) (p m i))) ⇢ 0›
using subdeg_inf_imp_s_tendsto_zero by presburger
define fct where ‹fct =?f›
then have f71:‹strict_mono fct› using f70 by auto
have ‹∀k. ∃s. ∀n. (∑i<n. (fps_const (s' i k))*(fps_X^(fct i))) =
(∑i<fct n. (fps_const (s i))*(fps_X^(i)))›
using exists_seq_all'[OF f71, of ‹λi. s' i k› for k]
by meson
then obtain s where f72:‹∀n k. (∑i<n. (fps_const (s' i k))*(fps_X^(fct i))) =
(∑i<fct n. (fps_const (s i k))*(fps_X^(i)))›
by meson
then have f85: ‹(λn. ∑i<fct n. (fps_const (s i k))*(fps_X^(i))) ⇢ Abs_fps (λi. s i k)› for k
by (simp add: Formal_Power_Series_Ring.tendsto_f_seq f71)
then have f86: ‹(λn. (∑i<n. (fps_const (s' i k))*(fps_X^(subdegree (the_s i) - m))))
= (λn. ∑i<fct n. (fps_const (s i k))*(fps_X^(i)))›
for k
using f72 fct_def by(auto simp:fun_eq_iff)
then have ‹(λn. (∑k<n. (fps_const (s' k i))*(fps_X^(subdegree (the_s k) - m))))
⇢ Abs_fps (λk. s k i)› for i
using f85 by presburger
then have f82:‹(λn. (∑i=0..<r. (∑k<n. (fps_const (s' k i))*(fps_X^(subdegree (the_s k) - m)))
*from_nat_into (B m) (p m i))) ⇢ (∑i=0..<r. Abs_fps (λk. s k i)*from_nat_into (B m) (p m i))›
for r
proof(induct r)
case 0
then show ?case by simp
next
case 1:(Suc r)
have ‹(λn. (∑k<n. fps_const (s' k r) * fps_X ^ (subdegree (the_s k) - m)) *
from_nat_into (B m) (p m r)) ⇢ Abs_fps (λk. s k r) * from_nat_into (B m) (p m r)›
proof -
have "(λn. from_nat_into (B m) (p m r) * (∑n<n. fps_const (s' n r) *
fps_X ^ (subdegree (the_s n) - m))) ⇢ from_nat_into (B m) (p m r) * Abs_fps (λn. s n r)"
using LIMSEQ_cmult_fps f85 f86 by presburger
then show ?thesis
by (simp add: mult.commute)
qed
then show ?case
apply(subst atLeast0_lessThan_Suc)
by (simp add: "1" LIMSEQ_add_fps add.commute)
qed
have f83:‹(∑i=0..<r. Abs_fps (λk. s k i)*from_nat_into (B m) (p m i)) ∈ I'› for r
proof(induct r)
case 0
then show ?case
by (metis (full_types) FPS_ring_def I'_def add_stable_FPS_ring atLeastLessThan0 diff_0
diff_add_cancel f53 in_I' partial_object.select_convs(1) ring.genideal_ideal ring_FPS subset_UNIV sum.empty)
next
case 1:(Suc r)
have ‹ from_nat_into (B m) (p m r) ∈ I'›
unfolding I'_def genideal_def apply(clarify)
by (metis (no_types, lifting) UN_subset_iff ab_group_add_class.ab_diff_conv_add_uminus add.right_neutral
add_diff_cancel_left' atLeastLessThan0 atMost_iff card.empty f53 from_nat_into in_mono less_irrefl_nat order_refl sum.empty)
with 1 show ?case apply(clarsimp)
by (metis (no_types, lifting) "1" FPS_ring_def Formal_Power_Series_Ring.genideal_sum_rep
Formal_Power_Series_Ring.idl_sum I'_def UNIV_I
add_stable_FPS_ring f62 ideal.I_l_closed monoid.select_convs(1) partial_object.select_convs(1))
qed
then have ‹f+g ∈ I'›
proof -
have "⋀n. lim (λna. ∑n = 0..<n. (∑na<na. fps_const (s' na n) * fps_X ^ (subdegree (the_s na) - m))
* from_nat_into (B m) (p m n)) = (∑n = 0..<n. Abs_fps (λna. s na n) * from_nat_into (B m) (p m n))"
by (smt (z3) f82 limI)
then show ?thesis
using f83 f84 by presburger
qed
then show False
using hyps(4) by force
qed
then have ‹I = I'›
using ‹I' ⊆ I› by fastforce
then show ‹∃A⊆carrier local.FPS_ring. finite A ∧ I = Idl⇘local.FPS_ring⇙ A›
by (metis FPS_ring_def I'_def f62 partial_object.select_convs(1) subset_UNIV)
qed
qed
end
end