Theory Degree_Bound_Utils
section ‹Utility Definitions and Lemmas about Degree Bounds for Gr\"obner Bases›
theory Degree_Bound_Utils
imports Groebner_Bases.Groebner_PM
begin
context pm_powerprod
begin
definition is_GB_cofactor_bound :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set ⇒ nat ⇒ bool"
where "is_GB_cofactor_bound F b ⟷
(∃G. punit.is_Groebner_basis G ∧ ideal G = ideal F ∧ (UN g:G. indets g) ⊆ (UN f:F. indets f) ∧
(∀g∈G. ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)))"
definition is_hom_GB_bound :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set ⇒ nat ⇒ bool"
where "is_hom_GB_bound F b ⟷ ((∀f∈F. homogeneous f) ⟶ (∀g∈punit.reduced_GB F. poly_deg g ≤ b))"
lemma is_GB_cofactor_boundI:
assumes "punit.is_Groebner_basis G" and "ideal G = ideal F" and "⋃(indets ` G) ⊆ ⋃(indets ` F)"
and "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)"
shows "is_GB_cofactor_bound F b"
unfolding is_GB_cofactor_bound_def using assms by blast
lemma is_GB_cofactor_boundE:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "⋃(indets ` G) ⊆ ⋃(indets ` F)"
and "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. indets (q f) ⊆ ⋃(indets ` F) ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
proof -
let ?X = "⋃(indets ` F)"
from assms obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "⋃(indets ` G) ⊆ ?X"
and 1: "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)"
by (auto simp: is_GB_cofactor_bound_def)
from this(1, 2, 3) show ?thesis
proof
fix g
assume "g ∈ G"
show "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. indets (q f) ⊆ ?X ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
proof (cases "g = 0")
case True
define q where "q = (λf::('x ⇒⇩0 nat) ⇒⇩0 'b. 0::('x ⇒⇩0 nat) ⇒⇩0 'b)"
show ?thesis
proof (intro exI conjI allI)
show "g = (∑f∈{}. q f * f)" by (simp add: True q_def)
qed (simp_all add: q_def)
next
case False
let ?X = "⋃(indets ` F)"
from ‹g ∈ G› have "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)"
by (rule 1)
then obtain F' q0 where "finite F'" and "F' ⊆ F" and g: "g = (∑f∈F'. q0 f * f)"
and q0: "⋀f. f ∈ F' ⟹ poly_deg (q0 f * f) ≤ b" by blast
define sub where "sub = (λx::'x. if x ∈ ?X then
monomial (1::'b) (Poly_Mapping.single x (1::nat))
else 1)"
have 1: "sub x = monomial 1 (monomial 1 x)" if "x ∈ indets g" for x
proof (simp add: sub_def, rule)
from that ‹g ∈ G› have "x ∈ ⋃(indets ` G)" by blast
also have "… ⊆ ?X" by fact
finally obtain f where "f ∈ F" and "x ∈ indets f" ..
assume "∀f∈F. x ∉ indets f"
hence "x ∉ indets f" using ‹f ∈ F› ..
thus "monomial 1 (monomial (Suc 0) x) = 1" using ‹x ∈ indets f› ..
qed
have 2: "sub x = monomial 1 (monomial 1 x)" if "f ∈ F'" and "x ∈ indets f" for f x
proof (simp add: sub_def, rule)
assume "∀f∈F. x ∉ indets f"
moreover from that(1) ‹F' ⊆ F› have "f ∈ F" ..
ultimately have "x ∉ indets f" ..
thus "monomial 1 (monomial (Suc 0) x) = 1" using that(2) ..
qed
have 3: "poly_subst sub f = f" if "f ∈ F'" for f by (rule poly_subst_id, rule 2, rule that)
define q where "q = (λf. if f ∈ F' then poly_subst sub (q0 f) else 0)"
show ?thesis
proof (intro exI allI conjI impI)
from 1 have "g = poly_subst sub g" by (rule poly_subst_id[symmetric])
also have "… = (∑f∈F'. q f * (poly_subst sub f))"
by (simp add: g poly_subst_sum poly_subst_times q_def cong: sum.cong)
also from refl have "… = (∑f∈F'. q f * f)"
proof (rule sum.cong)
fix f
assume "f ∈ F'"
hence "poly_subst sub f = f" by (rule 3)
thus "q f * poly_subst sub f = q f * f" by simp
qed
finally show "g = (∑f∈F'. q f * f)" .
next
fix f
have "indets (q f) ⊆ ?X ∧ poly_deg (q f * f) ≤ b"
proof (cases "f ∈ F'")
case True
hence qf: "q f = poly_subst sub (q0 f)" by (simp add: q_def)
show ?thesis
proof
show "indets (q f) ⊆ ?X"
proof
fix x
assume "x ∈ indets (q f)"
then obtain y where "x ∈ indets (sub y)" unfolding qf by (rule in_indets_poly_substE)
hence y: "y ∈ ?X" and "x ∈ indets (monomial (1::'b) (monomial (1::nat) y))"
by (simp_all add: sub_def split: if_splits)
from this(2) have "x = y" by (simp add: indets_monomial)
with y show "x ∈ ?X" by (simp only:)
qed
next
from ‹f ∈ F'› have "poly_subst sub f = f" by (rule 3)
hence "poly_deg (q f * f) = poly_deg (q f * poly_subst sub f)" by (simp only:)
also have "… = poly_deg (poly_subst sub (q0 f * f))" by (simp only: qf poly_subst_times)
also have "… ≤ poly_deg (q0 f * f)"
proof (rule poly_deg_poly_subst_le)
fix x
show "poly_deg (sub x) ≤ 1" by (simp add: sub_def poly_deg_monomial deg_pm_single)
qed
also from ‹f ∈ F'› have "… ≤ b" by (rule q0)
finally show "poly_deg (q f * f) ≤ b" .
qed
next
case False
thus ?thesis by (simp add: q_def)
qed
thus "indets (q f) ⊆ ?X" and "poly_deg (q f * f) ≤ b" by simp_all
assume "f ∉ F'"
thus "q f = 0" by (simp add: q_def)
qed fact+
qed
qed
qed
lemma is_GB_cofactor_boundE_Polys:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b" and "F ⊆ P[X]"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
proof -
let ?X = "⋃(indets ` F)"
have "?X ⊆ X"
proof
fix x
assume "x ∈ ?X"
then obtain f where "f ∈ F" and "x ∈ indets f" ..
from this(1) assms(2) have "f ∈ P[X]" ..
hence "indets f ⊆ X" by (rule PolysD)
with ‹x ∈ indets f› show "x ∈ X" ..
qed
from assms(1) obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F"
and 1: "⋃(indets ` G) ⊆ ?X"
and 2: "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. indets (q f) ⊆ ?X ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule is_GB_cofactor_boundE) blast
from this(1, 2) show ?thesis
proof
show "G ⊆ P[X]"
proof
fix g
assume "g ∈ G"
hence "indets g ⊆ ⋃(indets ` G)" by blast
also have "… ⊆ ?X" by fact
also have "… ⊆ X" by fact
finally show "g ∈ P[X]" by (rule PolysI_alt)
qed
next
fix g
assume "g ∈ G"
hence "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. indets (q f) ⊆ ?X ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule 2)
then obtain F' q where "finite F'" and "F' ⊆ F" and "g = (∑f∈F'. q f * f)"
and "⋀f. indets (q f) ⊆ ?X" and "⋀f. poly_deg (q f * f) ≤ b" and "⋀f. f ∉ F' ⟹ q f = 0"
by blast
show "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
proof (intro exI allI conjI impI)
fix f
from ‹indets (q f) ⊆ ?X› ‹?X ⊆ X› have "indets (q f) ⊆ X" by (rule subset_trans)
thus "q f ∈ P[X]" by (rule PolysI_alt)
qed fact+
qed
qed
lemma is_GB_cofactor_boundE_finite_Polys:
fixes F :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::field) set"
assumes "is_GB_cofactor_bound F b" and "finite F" and "F ⊆ P[X]"
obtains G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and "⋀g. g ∈ G ⟹ ∃q. g = (∑f∈F. q f * f) ∧ (∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b)"
proof -
from assms(1, 3) obtain G where "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[X]"
and 1: "⋀g. g ∈ G ⟹ ∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule is_GB_cofactor_boundE_Polys) blast
from this(1, 2, 3) show ?thesis
proof
fix g
assume "g ∈ G"
hence "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧
(∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b ∧ (f ∉ F' ⟶ q f = 0))"
by (rule 1)
then obtain F' q where "F' ⊆ F" and g: "g = (∑f∈F'. q f * f)"
and "⋀f. q f ∈ P[X]" and "⋀f. poly_deg (q f * f) ≤ b" and 2: "⋀f. f ∉ F' ⟹ q f = 0" by blast
show "∃q. g = (∑f∈F. q f * f) ∧ (∀f. q f ∈ P[X] ∧ poly_deg (q f * f) ≤ b)"
proof (intro exI conjI impI allI)
from assms(2) ‹F' ⊆ F› have "(∑f∈F'. q f * f) = (∑f∈F. q f * f)"
proof (intro sum.mono_neutral_left ballI)
fix f
assume "f ∈ F - F'"
hence "f ∉ F'" by simp
hence "q f = 0" by (rule 2)
thus "q f * f = 0" by simp
qed
thus "g = (∑f∈F. q f * f)" by (simp only: g)
qed fact+
qed
qed
lemma is_GB_cofactor_boundI_subset_zero:
assumes "F ⊆ {0}"
shows "is_GB_cofactor_bound F b"
using punit.is_Groebner_basis_empty
proof (rule is_GB_cofactor_boundI)
from assms show "ideal {} = ideal F" by (metis ideal.span_empty ideal_eq_zero_iff)
qed simp_all
lemma is_hom_GB_boundI:
"(⋀g. (⋀f. f ∈ F ⟹ homogeneous f) ⟹ g ∈ punit.reduced_GB F ⟹ poly_deg g ≤ b) ⟹ is_hom_GB_bound F b"
unfolding is_hom_GB_bound_def by blast
lemma is_hom_GB_boundD:
"is_hom_GB_bound F b ⟹ (⋀f. f ∈ F ⟹ homogeneous f) ⟹ g ∈ punit.reduced_GB F ⟹ poly_deg g ≤ b"
unfolding is_hom_GB_bound_def by blast
text ‹The following is the main theorem in this theory. It shows that a bound for Gr\"obner bases of
homogenized input sets is always also a cofactor bound for the original input sets.›
lemma (in extended_ord_pm_powerprod) hom_GB_bound_is_GB_cofactor_bound:
assumes "finite X" and "F ⊆ P[X]" and "extended_ord.is_hom_GB_bound (homogenize None ` extend_indets ` F) b"
shows "is_GB_cofactor_bound F b"
proof -
let ?F = "homogenize None ` extend_indets ` F"
define Y where "Y = ⋃ (indets ` F)"
define G where "G = restrict_indets ` (extended_ord.punit.reduced_GB ?F)"
have "Y ⊆ X"
proof
fix x
assume "x ∈ Y"
then obtain f where "f ∈ F" and "x ∈ indets f" unfolding Y_def ..
from this(1) assms(2) have "f ∈ P[X]" ..
hence "indets f ⊆ X" by (rule PolysD)
with ‹x ∈ indets f› show "x ∈ X" ..
qed
hence "finite Y" using assms(1) by (rule finite_subset)
moreover have "F ⊆ P[Y]" by (auto simp: Y_def Polys_alt)
ultimately have "punit.is_Groebner_basis G" and "ideal G = ideal F" and "G ⊆ P[Y]"
unfolding G_def by (rule restrict_indets_reduced_GB)+
from this(1, 2) show ?thesis
proof (rule is_GB_cofactor_boundI)
from ‹G ⊆ P[Y]› show "⋃ (indets ` G) ⊆ ⋃ (indets ` F)" by (auto simp: Y_def Polys_alt)
next
fix g
assume "g ∈ G"
then obtain g' where g': "g' ∈ extended_ord.punit.reduced_GB ?F"
and g: "g = restrict_indets g'" unfolding G_def ..
have "f ∈ ?F ⟹ homogeneous f" for f by (auto simp: homogeneous_homogenize)
with assms(3) have "poly_deg g' ≤ b" using g' by (rule extended_ord.is_hom_GB_boundD)
from g' have "g' ∈ ideal (extended_ord.punit.reduced_GB ?F)" by (rule ideal.span_base)
also have "… = ideal ?F"
proof (rule extended_ord.reduced_GB_ideal_Polys)
from ‹finite Y› show "finite (insert None (Some ` Y))" by simp
next
show "?F ⊆ P[insert None (Some ` Y)]"
proof
fix f0
assume "f0 ∈ ?F"
then obtain f where "f ∈ F" and f0: "f0 = homogenize None (extend_indets f)" by blast
from this(1) ‹F ⊆ P[Y]› have "f ∈ P[Y]" ..
hence "extend_indets f ∈ P[Some ` Y]" by (auto simp: indets_extend_indets Polys_alt)
thus "f0 ∈ P[insert None (Some ` Y)]" unfolding f0 by (rule homogenize_in_Polys)
qed
qed
finally have "g' ∈ ideal ?F" .
with ‹⋀f. f ∈ ?F ⟹ homogeneous f› obtain F0 q where "finite F0" and "F0 ⊆ ?F"
and g': "g' = (∑f∈F0. q f * f)" and deg_le: "⋀f. poly_deg (q f * f) ≤ poly_deg g'"
by (rule homogeneous_idealE) blast+
from this(2) obtain F' where "F' ⊆ F" and F0: "F0 = homogenize None ` extend_indets ` F'"
and inj_on: "inj_on (homogenize None ∘ extend_indets) F'"
unfolding image_comp by (rule subset_imageE_inj)
show "∃F' q. finite F' ∧ F' ⊆ F ∧ g = (∑f∈F'. q f * f) ∧ (∀f∈F'. poly_deg (q f * f) ≤ b)"
proof (intro exI conjI ballI)
from inj_on ‹finite F0› show "finite F'" by (simp only: finite_image_iff F0 image_comp)
next
from inj_on show "g = (∑f∈F'. (restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f)"
by (simp add: g g' F0 restrict_indets_sum restrict_indets_times sum.reindex image_comp o_def)
next
fix f
assume "f ∈ F'"
have "poly_deg ((restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f) =
poly_deg (restrict_indets (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f)))"
by (simp add: restrict_indets_times)
also have "… ≤ poly_deg (q (homogenize None (extend_indets f)) * homogenize None (extend_indets f))"
by (rule poly_deg_restrict_indets_le)
also have "… ≤ poly_deg g'" by (rule deg_le)
also have "… ≤ b" by fact
finally show "poly_deg ((restrict_indets ∘ q ∘ homogenize None ∘ extend_indets) f * f) ≤ b" .
qed fact
qed
qed
end
end