Theory Syzygy
section ‹Syzygies of Multivariate Polynomials›
theory Syzygy
imports Groebner_Bases More_MPoly_Type_Class
begin
text ‹In this theory we first introduce the general concept of @{emph ‹syzygies›} in modules, and
then provide a method for computing Gr\"obner bases of syzygy modules of lists of multivariate
vector-polynomials. Since syzygies in this context are themselves represented by vector-polynomials,
this method can be applied repeatedly to compute bases of syzygy modules of syzygies, and so on.›
instance nat :: comm_powerprod ..
subsection ‹Syzygy Modules Generated by Sets›
context module
begin
definition rep :: "('b ⇒⇩0 'a) ⇒ 'b"
where "rep r = (∑v∈keys r. lookup r v *s v)"
definition represents :: "'b set ⇒ ('b ⇒⇩0 'a) ⇒ 'b ⇒ bool"
where "represents B r x ⟷ (keys r ⊆ B ∧ local.rep r = x)"
definition syzygy_module :: "'b set ⇒ ('b ⇒⇩0 'a) set"
where "syzygy_module B = {s. local.represents B s 0}"
end
hide_const (open) real_vector.rep real_vector.represents real_vector.syzygy_module
context module
begin
lemma rep_monomial [simp]: "rep (monomial c x) = c *s x"
proof -
have sub: "keys (monomial c x) ⊆ {x}" by simp
have "rep (monomial c x) = (∑v∈{x}. lookup (monomial c x) v *s v)" unfolding rep_def
by (rule sum.mono_neutral_left, simp, fact sub, simp)
also have "... = c *s x" by simp
finally show ?thesis .
qed
lemma rep_zero [simp]: "rep 0 = 0"
by (simp add: rep_def)
lemma rep_uminus [simp]: "rep (- r) = - rep r"
by (simp add: keys_uminus sum_negf rep_def)
lemma rep_plus: "rep (r + s) = rep r + rep s"
proof -
from finite_keys finite_keys have fin: "finite (keys r ∪ keys s)" by (rule finite_UnI)
from fin have eq1: "(∑v∈keys r ∪ keys s. lookup r v *s v) = (∑v∈keys r. lookup r v *s v)"
proof (rule sum.mono_neutral_right)
show "∀v∈keys r ∪ keys s - keys r. lookup r v *s v = 0" by (simp add: in_keys_iff)
qed simp
from fin have eq2: "(∑v∈keys r ∪ keys s. lookup s v *s v) = (∑v∈keys s. lookup s v *s v)"
proof (rule sum.mono_neutral_right)
show "∀v∈keys r ∪ keys s - keys s. lookup s v *s v = 0" by (simp add: in_keys_iff)
qed simp
have "rep (r + s) = (∑v∈keys (r + s). lookup (r + s) v *s v)" by (simp only: rep_def)
also have "... = (∑v∈keys r ∪ keys s. lookup (r + s) v *s v)"
proof (rule sum.mono_neutral_left)
show "∀i∈keys r ∪ keys s - keys (r + s). lookup (r + s) i *s i = 0" by (simp add: in_keys_iff)
qed (auto simp: Poly_Mapping.keys_add)
also have "... = (∑v∈keys r ∪ keys s. lookup r v *s v) + (∑v∈keys r ∪ keys s. lookup s v *s v)"
by (simp add: lookup_add scale_left_distrib sum.distrib)
also have "... = rep r + rep s" by (simp only: eq1 eq2 rep_def)
finally show ?thesis .
qed
lemma rep_minus: "rep (r - s) = rep r - rep s"
proof -
from finite_keys finite_keys have fin: "finite (keys r ∪ keys s)" by (rule finite_UnI)
from fin have eq1: "(∑v∈keys r ∪ keys s. lookup r v *s v) = (∑v∈keys r. lookup r v *s v)"
proof (rule sum.mono_neutral_right)
show "∀v∈keys r ∪ keys s - keys r. lookup r v *s v = 0" by (simp add: in_keys_iff)
qed simp
from fin have eq2: "(∑v∈keys r ∪ keys s. lookup s v *s v) = (∑v∈keys s. lookup s v *s v)"
proof (rule sum.mono_neutral_right)
show "∀v∈keys r ∪ keys s - keys s. lookup s v *s v = 0" by (simp add: in_keys_iff)
qed simp
have "rep (r - s) = (∑v∈keys (r - s). lookup (r - s) v *s v)" by (simp only: rep_def)
also from fin keys_minus have "... = (∑v∈keys r ∪ keys s. lookup (r - s) v *s v)"
proof (rule sum.mono_neutral_left)
show "∀i∈keys r ∪ keys s - keys (r - s). lookup (r - s) i *s i = 0" by (simp add: in_keys_iff)
qed
also have "... = (∑v∈keys r ∪ keys s. lookup r v *s v) - (∑v∈keys r ∪ keys s. lookup s v *s v)"
by (simp add: lookup_minus scale_left_diff_distrib sum_subtractf)
also have "... = rep r - rep s" by (simp only: eq1 eq2 rep_def)
finally show ?thesis .
qed
lemma rep_smult: "rep (monomial c 0 * r) = c *s rep r"
proof -
have l: "lookup (monomial c 0 * r) v = c * (lookup r v)" for v
unfolding mult_map_scale_conv_mult[symmetric] by (rule map_lookup, simp)
have sub: "keys (monomial c 0 * r) ⊆ keys r"
by (metis l lookup_not_eq_zero_eq_in_keys mult_zero_right subsetI)
have "rep (monomial c 0 * r) = (∑v∈keys (monomial c 0 * r). lookup (monomial c 0 * r) v *s v)"
by (simp only: rep_def)
also from finite_keys sub have "... = (∑v∈keys r. lookup (monomial c 0 * r) v *s v)"
proof (rule sum.mono_neutral_left)
show "∀v∈keys r - keys (monomial c 0 * r). lookup (monomial c 0 * r) v *s v = 0" by (simp add: in_keys_iff)
qed
also have "... = c *s (∑v∈keys r. lookup r v *s v)" by (simp add: l scale_sum_right)
also have "... = c *s rep r" by (simp add: rep_def)
finally show ?thesis .
qed
lemma rep_in_span: "rep r ∈ span (keys r)"
unfolding rep_def by (fact sum_in_spanI)
lemma spanE_rep:
assumes "x ∈ span B"
obtains r where "keys r ⊆ B" and "x = rep r"
proof -
from assms obtain A q where "finite A" and "A ⊆ B" and x: "x = (∑a∈A. q a *s a)" by (rule spanE)
define r where "r = Abs_poly_mapping (λk. q k when k ∈ A)"
have 1: "lookup r = (λk. q k when k ∈ A)" unfolding r_def
by (rule Abs_poly_mapping_inverse, simp add: ‹finite A›)
have 2: "keys r ⊆ A" by (auto simp: in_keys_iff 1)
show ?thesis
proof
have "x = (∑a∈A. lookup r a *s a)" unfolding x by (rule sum.cong, simp_all add: 1)
also from ‹finite A› 2 have "... = (∑a∈keys r. lookup r a *s a)"
proof (rule sum.mono_neutral_right)
show "∀a∈A - keys r. lookup r a *s a = 0" by (simp add: in_keys_iff)
qed
finally show "x = rep r" by (simp only: rep_def)
next
from 2 ‹A ⊆ B› show "keys r ⊆ B" by (rule subset_trans)
qed
qed
lemma representsI:
assumes "keys r ⊆ B" and "rep r = x"
shows "represents B r x"
unfolding represents_def using assms by blast
lemma representsD1:
assumes "represents B r x"
shows "keys r ⊆ B"
using assms unfolding represents_def by blast
lemma representsD2:
assumes "represents B r x"
shows "x = rep r"
using assms unfolding represents_def by blast
lemma represents_mono:
assumes "represents B r x" and "B ⊆ A"
shows "represents A r x"
proof (rule representsI)
from assms(1) have "keys r ⊆ B" by (rule representsD1)
thus "keys r ⊆ A" using assms(2) by (rule subset_trans)
next
from assms(1) have "x = rep r" by (rule representsD2)
thus "rep r = x" by (rule HOL.sym)
qed
lemma represents_self: "represents {x} (monomial 1 x) x"
proof -
have sub: "keys (monomial (1::'a) x) ⊆ {x}" by simp
moreover have "rep (monomial (1::'a) x) = x" by simp
ultimately show ?thesis by (rule representsI)
qed
lemma represents_zero: "represents B 0 0"
by (rule representsI, simp_all)
lemma represents_plus:
assumes "represents A r x" and "represents B s y"
shows "represents (A ∪ B) (r + s) (x + y)"
proof -
from assms(1) have r: "keys r ⊆ A" and x: "x = rep r" by (rule representsD1, rule representsD2)
from assms(2) have s: "keys s ⊆ B" and y: "y = rep s" by (rule representsD1, rule representsD2)
show ?thesis
proof (rule representsI)
from r s have "keys r ∪ keys s ⊆ A ∪ B" by blast
thus "keys (r + s) ⊆ A ∪ B"
by (meson Poly_Mapping.keys_add subset_trans)
qed (simp add: rep_plus x y)
qed
lemma represents_uminus:
assumes "represents B r x"
shows "represents B (- r) (- x)"
proof -
from assms have r: "keys r ⊆ B" and x: "x = rep r" by (rule representsD1, rule representsD2)
show ?thesis
proof (rule representsI)
from r show "keys (- r) ⊆ B" by (simp only: keys_uminus)
qed (simp add: x)
qed
lemma represents_minus:
assumes "represents A r x" and "represents B s y"
shows "represents (A ∪ B) (r - s) (x - y)"
proof -
from assms(1) have r: "keys r ⊆ A" and x: "x = rep r" by (rule representsD1, rule representsD2)
from assms(2) have s: "keys s ⊆ B" and y: "y = rep s" by (rule representsD1, rule representsD2)
show ?thesis
proof (rule representsI)
from r s have "keys r ∪ keys s ⊆ A ∪ B" by blast
with keys_minus show "keys (r - s) ⊆ A ∪ B" by (rule subset_trans)
qed (simp only: rep_minus x y)
qed
lemma represents_scale:
assumes "represents B r x"
shows "represents B (monomial c 0 * r) (c *s x)"
proof -
from assms have r: "keys r ⊆ B" and x: "x = rep r" by (rule representsD1, rule representsD2)
show ?thesis
proof (rule representsI)
have l: "lookup (monomial c 0 * r) v = c * (lookup r v)" for v
unfolding mult_map_scale_conv_mult[symmetric] by (rule map_lookup, simp)
have sub: "keys (monomial c 0 * r) ⊆ keys r"
by (metis l lookup_not_eq_zero_eq_in_keys mult_zero_right subsetI)
thus "keys (monomial c 0 * r) ⊆ B" using r by (rule subset_trans)
qed (simp only: rep_smult x)
qed
lemma represents_in_span:
assumes "represents B r x"
shows "x ∈ span B"
proof -
from assms have r: "keys r ⊆ B" and x: "x = rep r" by (rule representsD1, rule representsD2)
have "x ∈ span (keys r)" unfolding x by (fact rep_in_span)
also from r have "... ⊆ span B" by (rule span_mono)
finally show ?thesis .
qed
lemma syzygy_module_iff: "s ∈ syzygy_module B ⟷ represents B s 0"
by (simp add: syzygy_module_def)
lemma syzygy_moduleI:
assumes "represents B s 0"
shows "s ∈ syzygy_module B"
unfolding syzygy_module_iff using assms .
lemma syzygy_moduleD:
assumes "s ∈ syzygy_module B"
shows "represents B s 0"
using assms unfolding syzygy_module_iff .
lemma zero_in_syzygy_module: "0 ∈ syzygy_module B"
using represents_zero by (rule syzygy_moduleI)
lemma syzygy_module_closed_plus:
assumes "s1 ∈ syzygy_module B" and "s2 ∈ syzygy_module B"
shows "s1 + s2 ∈ syzygy_module B"
proof -
from assms(1) have "represents B s1 0" by (rule syzygy_moduleD)
moreover from assms(2) have "represents B s2 0" by (rule syzygy_moduleD)
ultimately have "represents (B ∪ B) (s1 + s2) (0 + 0)" by (rule represents_plus)
hence "represents B (s1 + s2) 0" by simp
thus ?thesis by (rule syzygy_moduleI)
qed
lemma syzygy_module_closed_minus:
assumes "s1 ∈ syzygy_module B" and "s2 ∈ syzygy_module B"
shows "s1 - s2 ∈ syzygy_module B"
proof -
from assms(1) have "represents B s1 0" by (rule syzygy_moduleD)
moreover from assms(2) have "represents B s2 0" by (rule syzygy_moduleD)
ultimately have "represents (B ∪ B) (s1 - s2) (0 - 0)" by (rule represents_minus)
hence "represents B (s1 - s2) 0" by simp
thus ?thesis by (rule syzygy_moduleI)
qed
lemma syzygy_module_closed_times_monomial:
assumes "s ∈ syzygy_module B"
shows "monomial c 0 * s ∈ syzygy_module B"
proof -
from assms(1) have "represents B s 0" by (rule syzygy_moduleD)
hence "represents B (monomial c 0 * s) (c *s 0)" by (rule represents_scale)
hence "represents B (monomial c 0 * s) 0" by simp
thus ?thesis by (rule syzygy_moduleI)
qed
end
context term_powerprod
begin
lemma keys_rep_subset:
assumes "u ∈ keys (pmdl.rep r)"
obtains t v where "t ∈ Keys (Poly_Mapping.range r)" and "v ∈ Keys (keys r)" and "u = t ⊕ v"
proof -
note assms
also have "keys (pmdl.rep r) ⊆ (⋃v∈keys r. keys (lookup r v ⊙ v))"
by (simp add: pmdl.rep_def keys_sum_subset)
finally obtain v0 where "v0 ∈ keys r" and "u ∈ keys (lookup r v0 ⊙ v0)" ..
from this(2) obtain t v where "t ∈ keys (lookup r v0)" and "v ∈ keys v0" and "u = t ⊕ v"
by (rule in_keys_mult_scalarE)
show ?thesis
proof
from ‹v0 ∈ keys r› have "lookup r v0 ∈ Poly_Mapping.range r" by (rule in_keys_lookup_in_range)
with ‹t ∈ keys (lookup r v0)› show "t ∈ Keys (Poly_Mapping.range r)" by (rule in_KeysI)
next
from ‹v ∈ keys v0› ‹v0 ∈ keys r› show "v ∈ Keys (keys r)" by (rule in_KeysI)
qed fact
qed
lemma rep_mult_scalar: "pmdl.rep (punit.monom_mult c 0 r) = c ⊙ pmdl.rep r"
unfolding punit.mult_scalar_monomial[symmetric] punit_mult_scalar by (fact pmdl.rep_smult)
lemma represents_mult_scalar:
assumes "pmdl.represents B r x"
shows "pmdl.represents B (punit.monom_mult c 0 r) (c ⊙ x)"
unfolding punit.mult_scalar_monomial[symmetric] punit_mult_scalar using assms
by (rule pmdl.represents_scale)
lemma syzygy_module_closed_map_scale: "s ∈ pmdl.syzygy_module B ⟹ c ⋅ s ∈ pmdl.syzygy_module B"
unfolding map_scale_eq_times by (rule pmdl.syzygy_module_closed_times_monomial)
lemma phull_syzygy_module: "phull (pmdl.syzygy_module B) = pmdl.syzygy_module B"
unfolding phull.span_eq_iff
apply (rule phull.subspaceI)
subgoal by (fact pmdl.zero_in_syzygy_module)
subgoal by (fact pmdl.syzygy_module_closed_plus)
subgoal by (fact syzygy_module_closed_map_scale)
done
end
subsection ‹Polynomial Mappings on List-Indices›
definition pm_of_idx_pm :: "('a list) ⇒ (nat ⇒⇩0 'b) ⇒ 'a ⇒⇩0 'b::zero"
where "pm_of_idx_pm xs f = Abs_poly_mapping (λx. lookup f (Min {i. i < length xs ∧ xs ! i = x}) when x ∈ set xs)"
definition idx_pm_of_pm :: "('a list) ⇒ ('a ⇒⇩0 'b) ⇒ nat ⇒⇩0 'b::zero"
where "idx_pm_of_pm xs f = Abs_poly_mapping (λi. lookup f (xs ! i) when i < length xs)"
lemma lookup_pm_of_idx_pm:
"lookup (pm_of_idx_pm xs f) = (λx. lookup f (Min {i. i < length xs ∧ xs ! i = x}) when x ∈ set xs)"
unfolding pm_of_idx_pm_def by (rule Abs_poly_mapping_inverse, simp)
lemma lookup_pm_of_idx_pm_distinct:
assumes "distinct xs" and "i < length xs"
shows "lookup (pm_of_idx_pm xs f) (xs ! i) = lookup f i"
proof -
from assms have "{j. j < length xs ∧ xs ! j = xs ! i} = {i}"
using distinct_Ex1 nth_mem by fastforce
moreover from assms(2) have "xs ! i ∈ set xs" by (rule nth_mem)
ultimately show ?thesis by (simp add: lookup_pm_of_idx_pm)
qed
lemma keys_pm_of_idx_pm_subset: "keys (pm_of_idx_pm xs f) ⊆ set xs"
proof
fix t
assume "t ∈ keys (pm_of_idx_pm xs f)"
hence "lookup (pm_of_idx_pm xs f) t ≠ 0" by (simp add: in_keys_iff)
thus "t ∈ set xs" by (simp add: lookup_pm_of_idx_pm)
qed
lemma range_pm_of_idx_pm_subset: "Poly_Mapping.range (pm_of_idx_pm xs f) ⊆ lookup f ` {0..<length xs} - {0}"
proof
fix c
assume "c ∈ Poly_Mapping.range (pm_of_idx_pm xs f)"
then obtain t where t: "t ∈ keys (pm_of_idx_pm xs f)" and c: "c = lookup (pm_of_idx_pm xs f) t"
by (metis DiffE imageE insertCI not_in_keys_iff_lookup_eq_zero range.rep_eq)
from t keys_pm_of_idx_pm_subset have "t ∈ set xs" ..
hence c1: "c = lookup f (Min {i. i < length xs ∧ xs ! i = t})" by (simp add: lookup_pm_of_idx_pm c)
show "c ∈ lookup f ` {0..<length xs} - {0}"
proof (intro DiffI image_eqI)
from ‹t ∈ set xs› obtain i where "i < length xs" and "t = xs ! i" by (metis in_set_conv_nth)
have "finite {i. i < length xs ∧ xs ! i = t}" by simp
moreover from ‹i < length xs› ‹t = xs ! i› have "{i. i < length xs ∧ xs ! i = t} ≠ {}" by auto
ultimately have "Min {i. i < length xs ∧ xs ! i = t} ∈ {i. i < length xs ∧ xs ! i = t}"
by (rule Min_in)
thus "Min {i. i < length xs ∧ xs ! i = t} ∈ {0..<length xs}" by simp
next
from t show "c ∉ {0}" by (simp add: c in_keys_iff)
qed (fact c1)
qed
corollary range_pm_of_idx_pm_subset': "Poly_Mapping.range (pm_of_idx_pm xs f) ⊆ Poly_Mapping.range f"
using range_pm_of_idx_pm_subset
proof (rule subset_trans)
show "lookup f ` {0..<length xs} - {0} ⊆ Poly_Mapping.range f" by (transfer, auto)
qed
lemma pm_of_idx_pm_zero [simp]: "pm_of_idx_pm xs 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm)
lemma pm_of_idx_pm_plus: "pm_of_idx_pm xs (f + g) = pm_of_idx_pm xs f + pm_of_idx_pm xs g"
by (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm lookup_add when_def)
lemma pm_of_idx_pm_uminus: "pm_of_idx_pm xs (- f) = - pm_of_idx_pm xs f"
by (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm when_def)
lemma pm_of_idx_pm_minus: "pm_of_idx_pm xs (f - g) = pm_of_idx_pm xs f - pm_of_idx_pm xs g"
by (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm lookup_minus when_def)
lemma pm_of_idx_pm_monom_mult: "pm_of_idx_pm xs (punit.monom_mult c 0 f) = punit.monom_mult c 0 (pm_of_idx_pm xs f)"
by (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm punit.lookup_monom_mult_zero when_def)
lemma pm_of_idx_pm_monomial:
assumes "distinct xs"
shows "pm_of_idx_pm xs (monomial c i) = (monomial c (xs ! i) when i < length xs)"
proof -
from assms have *: "{i. i < length xs ∧ xs ! i = xs ! j} = {j}" if "j < length xs" for j
using distinct_Ex1 nth_mem that by fastforce
show ?thesis
proof (cases "i < length xs")
case True
have "pm_of_idx_pm xs (monomial c i) = monomial c (xs ! i)"
proof (rule poly_mapping_eqI)
fix k
show "lookup (pm_of_idx_pm xs (monomial c i)) k = lookup (monomial c (xs ! i)) k"
proof (cases "xs ! i = k")
case True
with ‹i < length xs› have "k ∈ set xs" by auto
thus ?thesis by (simp add: lookup_pm_of_idx_pm lookup_single *[OF ‹i < length xs›] True[symmetric])
next
case False
have "lookup (pm_of_idx_pm xs (monomial c i)) k = 0"
proof (cases "k ∈ set xs")
case True
then obtain j where "j < length xs" and "k = xs ! j" by (metis in_set_conv_nth)
with False have "i ≠ Min {i. i < length xs ∧ xs ! i = k}"
by (auto simp: ‹k = xs ! j› *[OF ‹j < length xs›])
thus ?thesis by (simp add: lookup_pm_of_idx_pm True lookup_single)
next
case False
thus ?thesis by (simp add: lookup_pm_of_idx_pm)
qed
with False show ?thesis by (simp add: lookup_single)
qed
qed
with True show ?thesis by simp
next
case False
have "pm_of_idx_pm xs (monomial c i) = 0"
proof (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm when_def, rule)
fix k
assume "k ∈ set xs"
then obtain j where "j < length xs" and "k = xs ! j" by (metis in_set_conv_nth)
with False have "i ≠ Min {i. i < length xs ∧ xs ! i = k}"
by (auto simp: ‹k = xs ! j› *[OF ‹j < length xs›])
thus "lookup (monomial c i) (Min {i. i < length xs ∧ xs ! i = k}) = 0"
by (simp add: lookup_single)
qed
with False show ?thesis by simp
qed
qed
lemma pm_of_idx_pm_take:
assumes "keys f ⊆ {0..<j}"
shows "pm_of_idx_pm (take j xs) f = pm_of_idx_pm xs f"
proof (rule poly_mapping_eqI)
fix i
let ?xs = "take j xs"
let ?A = "{k. k < length xs ∧ xs ! k = i}"
let ?B = "{k. k < length xs ∧ k < j ∧ xs ! k = i}"
have A_fin: "finite ?A" and B_fin: "finite ?B" by fastforce+
have A_ne: "i ∈ set xs ⟹ ?A ≠ {}" by (simp add: in_set_conv_nth)
have B_ne: "i ∈ set ?xs ⟹ ?B ≠ {}" by (auto simp add: in_set_conv_nth)
define m1 where "m1 = Min ?A"
define m2 where "m2 = Min ?B"
have m1: "m1 ∈ ?A" if "i ∈ set xs"
unfolding m1_def by (rule Min_in, fact A_fin, rule A_ne, fact that)
have m2: "m2 ∈ ?B" if "i ∈ set ?xs"
unfolding m2_def by (rule Min_in, fact B_fin, rule B_ne, fact that)
show "lookup (pm_of_idx_pm (take j xs) f) i = lookup (pm_of_idx_pm xs f) i"
proof (cases "i ∈ set ?xs")
case True
hence "i ∈ set xs" using set_take_subset ..
hence "m1 ∈ ?A" by (rule m1)
hence "m1 < length xs" and "xs ! m1 = i" by simp_all
from True have "m2 ∈ ?B" by (rule m2)
hence "m2 < length xs" and "m2 < j" and "xs ! m2 = i" by simp_all
hence "m2 ∈ ?A" by simp
with A_fin have "m1 ≤ m2" unfolding m1_def by (rule Min_le)
with ‹m2 < j› have "m1 < j" by simp
with ‹m1 < length xs› ‹xs ! m1 = i› have "m1 ∈ ?B" by simp
with B_fin have "m2 ≤ m1" unfolding m2_def by (rule Min_le)
with ‹m1 ≤ m2› have "m1 = m2" by (rule le_antisym)
with True ‹i ∈ set xs› show ?thesis by (simp add: lookup_pm_of_idx_pm m1_def m2_def cong: conj_cong)
next
case False
thus ?thesis
proof (simp add: lookup_pm_of_idx_pm when_def m1_def[symmetric], intro impI)
assume "i ∈ set xs"
hence "m1 ∈ ?A" by (rule m1)
hence "m1 < length xs" and "xs ! m1 = i" by simp_all
have "m1 ∉ keys f"
proof
assume "m1 ∈ keys f"
hence "m1 ∈ {0..<j}" using assms ..
hence "m1 < j" by simp
with ‹m1 < length xs› have "m1 < length ?xs" by simp
hence "?xs ! m1 ∈ set ?xs" by (rule nth_mem)
with ‹m1 < j› have "i ∈ set ?xs" by (simp add: ‹xs ! m1 = i›)
with False show False ..
qed
thus "lookup f m1 = 0" by (simp add: in_keys_iff)
qed
qed
qed
lemma lookup_idx_pm_of_pm: "lookup (idx_pm_of_pm xs f) = (λi. lookup f (xs ! i) when i < length xs)"
unfolding idx_pm_of_pm_def by (rule Abs_poly_mapping_inverse, simp)
lemma keys_idx_pm_of_pm_subset: "keys (idx_pm_of_pm xs f) ⊆ {0..<length xs}"
proof
fix i
assume "i ∈ keys (idx_pm_of_pm xs f)"
hence "lookup (idx_pm_of_pm xs f) i ≠ 0" by (simp add: in_keys_iff)
thus "i ∈ {0..<length xs}" by (simp add: lookup_idx_pm_of_pm)
qed
lemma idx_pm_of_pm_zero [simp]: "idx_pm_of_pm xs 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_idx_pm_of_pm)
lemma idx_pm_of_pm_plus: "idx_pm_of_pm xs (f + g) = idx_pm_of_pm xs f + idx_pm_of_pm xs g"
by (rule poly_mapping_eqI, simp add: lookup_idx_pm_of_pm lookup_add when_def)
lemma idx_pm_of_pm_minus: "idx_pm_of_pm xs (f - g) = idx_pm_of_pm xs f - idx_pm_of_pm xs g"
by (rule poly_mapping_eqI, simp add: lookup_idx_pm_of_pm lookup_minus when_def)
lemma pm_of_idx_pm_of_pm:
assumes "keys f ⊆ set xs"
shows "pm_of_idx_pm xs (idx_pm_of_pm xs f) = f"
proof (rule poly_mapping_eqI, simp add: lookup_pm_of_idx_pm when_def, intro conjI impI)
fix k
assume "k ∈ set xs"
define i where "i = Min {i. i < length xs ∧ xs ! i = k}"
have "finite {i. i < length xs ∧ xs ! i = k}" by simp
moreover from ‹k ∈ set xs› have "{i. i < length xs ∧ xs ! i = k} ≠ {}"
by (simp add: in_set_conv_nth)
ultimately have "i ∈ {i. i < length xs ∧ xs ! i = k}" unfolding i_def by (rule Min_in)
hence "i < length xs" and "xs ! i = k" by simp_all
thus "lookup (idx_pm_of_pm xs f) i = lookup f k" by (simp add: lookup_idx_pm_of_pm)
next
fix k
assume "k ∉ set xs"
with assms show "lookup f k = 0" by (auto simp: in_keys_iff)
qed
lemma idx_pm_of_pm_of_idx_pm:
assumes "distinct xs" and "keys f ⊆ {0..<length xs}"
shows "idx_pm_of_pm xs (pm_of_idx_pm xs f) = f"
proof (rule poly_mapping_eqI)
fix i
show "lookup (idx_pm_of_pm xs (pm_of_idx_pm xs f)) i = lookup f i"
proof (cases "i < length xs")
case True
with assms(1) show ?thesis by (simp add: lookup_idx_pm_of_pm lookup_pm_of_idx_pm_distinct)
next
case False
hence "i ∉ {0..<length xs}" by simp
with assms(2) have "i ∉ keys f" by blast
with False show ?thesis by (simp add: in_keys_iff lookup_idx_pm_of_pm)
qed
qed
subsection ‹POT Orders›
context ordered_term
begin
definition is_pot_ord :: bool
where "is_pot_ord ⟷ (∀u v. component_of_term u < component_of_term v ⟶ u ≺⇩t v)"
lemma is_pot_ordI:
assumes "⋀u v. component_of_term u < component_of_term v ⟹ u ≺⇩t v"
shows "is_pot_ord"
unfolding is_pot_ord_def using assms by blast
lemma is_pot_ordD:
assumes "is_pot_ord" and "component_of_term u < component_of_term v"
shows "u ≺⇩t v"
using assms unfolding is_pot_ord_def by blast
lemma is_pot_ordD2:
assumes "is_pot_ord" and "u ≼⇩t v"
shows "component_of_term u ≤ component_of_term v"
proof (rule ccontr)
assume "¬ component_of_term u ≤ component_of_term v"
hence "component_of_term v < component_of_term u" by simp
with assms(1) have "v ≺⇩t u" by (rule is_pot_ordD)
with assms(2) show False by simp
qed
lemma is_pot_ord:
assumes "is_pot_ord"
shows "u ≼⇩t v ⟷ (component_of_term u < component_of_term v ∨
(component_of_term u = component_of_term v ∧ pp_of_term u ≼ pp_of_term v))" (is "?l ⟷ ?r")
proof
assume ?l
with assms have "component_of_term u ≤ component_of_term v" by (rule is_pot_ordD2)
hence "component_of_term u < component_of_term v ∨ component_of_term u = component_of_term v"
by (simp add: order_class.le_less)
thus ?r
proof
assume "component_of_term u < component_of_term v"
thus ?r ..
next
assume 1: "component_of_term u = component_of_term v"
moreover have "pp_of_term u ≼ pp_of_term v"
proof (rule ccontr)
assume "¬ pp_of_term u ≼ pp_of_term v"
hence 2: "pp_of_term v ≼ pp_of_term u" and 3: "pp_of_term u ≠ pp_of_term v" by simp_all
from 1 have "component_of_term v ≤ component_of_term u" by simp
with 2 have "v ≼⇩t u" by (rule ord_termI)
with ‹?l› have "u = v" by simp
with 3 show False by simp
qed
ultimately show ?r by simp
qed
next
assume ?r
thus ?l
proof
assume "component_of_term u < component_of_term v"
with assms have "u ≺⇩t v" by (rule is_pot_ordD)
thus ?l by simp
next
assume "component_of_term u = component_of_term v ∧ pp_of_term u ≼ pp_of_term v"
hence "pp_of_term u ≼ pp_of_term v" and "component_of_term u ≤ component_of_term v" by simp_all
thus ?l by (rule ord_termI)
qed
qed
definition map_component :: "('k ⇒ 'k) ⇒ 't ⇒ 't"
where "map_component f v = term_of_pair (pp_of_term v, f (component_of_term v))"
lemma pair_of_map_component [term_simps]:
"pair_of_term (map_component f v) = (pp_of_term v, f (component_of_term v))"
by (simp add: map_component_def pair_term)
lemma pp_of_map_component [term_simps]: "pp_of_term (map_component f v) = pp_of_term v"
by (simp add: pp_of_term_def pair_of_map_component)
lemma component_of_map_component [term_simps]:
"component_of_term (map_component f v) = f (component_of_term v)"
by (simp add: component_of_term_def pair_of_map_component)
lemma map_component_term_of_pair [term_simps]:
"map_component f (term_of_pair (t, k)) = term_of_pair (t, f k)"
by (simp add: map_component_def term_simps)
lemma map_component_comp: "map_component f (map_component g x) = map_component (λk. f (g k)) x"
by (simp add: map_component_def term_simps)
lemma map_component_id [term_simps]: "map_component (λk. k) x = x"
by (simp add: map_component_def term_simps)
lemma map_component_inj:
assumes "inj f" and "map_component f u = map_component f v"
shows "u = v"
proof -
from assms(2) have "term_of_pair (pp_of_term u, f (component_of_term u)) =
term_of_pair (pp_of_term v, f (component_of_term v))"
by (simp only: map_component_def)
hence "(pp_of_term u, f (component_of_term u)) = (pp_of_term v, f (component_of_term v))"
by (rule term_of_pair_injective)
hence 1: "pp_of_term u = pp_of_term v" and "f (component_of_term u) = f (component_of_term v)" by simp_all
from assms(1) this(2) have "component_of_term u = component_of_term v" by (rule injD)
with 1 show ?thesis by (metis term_of_pair_pair)
qed
end
subsection ‹Gr\"obner Bases of Syzygy Modules›
locale gd_inf_term =
gd_term pair_of_term term_of_pair ord ord_strict ord_term ord_term_strict
for pair_of_term::"'t ⇒ ('a::graded_dickson_powerprod × nat)"
and term_of_pair::"('a × nat) ⇒ 't"
and ord::"'a ⇒ 'a ⇒ bool" (infixl "≼" 50)
and ord_strict (infixl "≺" 50)
and ord_term::"'t ⇒ 't ⇒ bool" (infixl "≼⇩t" 50)
and ord_term_strict::"'t ⇒ 't ⇒ bool" (infixl "≺⇩t" 50)
begin
text ‹In order to compute a Gr\"obner basis of the syzygy module of a list ‹bs› of polynomials, one
first needs to ``lift'' ‹bs› to a new list ‹bs'› by adding further components, compute a Gr\"obner
basis ‹gs› of ‹bs'›, and then filter out those elements of ‹gs› whose only non-zero components are
those that were newly added to ‹bs›.
Function ‹init_syzygy_list› takes care of constructing ‹bs'›, and function ‹filter_syzygy_basis›
does the filtering. Function ‹proj_orig_basis›, finally, projects the Gr\"obner basis ‹gs› of ‹bs'›
to a Gr\"obner basis of the original list ‹bs›.›
definition lift_poly_syz :: "nat ⇒ ('t ⇒⇩0 'b) ⇒ nat ⇒ ('t ⇒⇩0 'b::semiring_1)"
where "lift_poly_syz n b i = Abs_poly_mapping
(λx. if pair_of_term x = (0, i) then 1
else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x)
else 0)"
definition proj_poly_syz :: "nat ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b::semiring_1)"
where "proj_poly_syz n b = Poly_Mapping.map_key (λx. map_component (λk. k + n) x) b"
definition cofactor_list_syz :: "nat ⇒ ('t ⇒⇩0 'b) ⇒ ('a ⇒⇩0 'b::semiring_1) list"
where "cofactor_list_syz n b = map (λi. proj_poly i b) [0..<n]"
definition init_syzygy_list :: "('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::semiring_1) list"
where "init_syzygy_list bs = map_idx (lift_poly_syz (length bs)) bs 0"
definition proj_orig_basis :: "nat ⇒ ('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::semiring_1) list"
where "proj_orig_basis n bs = map (proj_poly_syz n) bs"
definition filter_syzygy_basis :: "nat ⇒ ('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::semiring_1) list"
where "filter_syzygy_basis n bs = [b←bs. component_of_term ` keys b ⊆ {0..<n}]"
definition syzygy_module_list :: "('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::comm_ring_1) set"
where "syzygy_module_list bs = atomize_poly ` idx_pm_of_pm bs ` pmdl.syzygy_module (set bs)"
subsubsection ‹@{const lift_poly_syz}›
lemma keys_lift_poly_syz_aux:
"{x. (if pair_of_term x = (0, i) then 1
else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x)
else 0) ≠ 0} ⊆ insert (term_of_pair (0, i)) (map_component (λk. k + n) ` keys b)"
(is "?l ⊆ ?r") for b::"'t ⇒⇩0 'b::semiring_1"
proof
fix x::'t
assume "x ∈ ?l"
hence "(if pair_of_term x = (0, i) then 1 else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x) else 0) ≠ 0"
by simp
hence "pair_of_term x = (0, i) ∨ (n ≤ component_of_term x ∧ lookup b (map_component (λk. k - n) x) ≠ 0)"
by (simp split: if_split_asm)
thus "x ∈ ?r"
proof
assume "pair_of_term x = (0, i)"
hence "(0, i) = pair_of_term x" by (rule sym)
hence "x = term_of_pair (0, i)" by (simp add: term_pair)
thus ?thesis by simp
next
assume "n ≤ component_of_term x ∧ lookup b (map_component (λk. k - n) x) ≠ 0"
hence "n ≤ component_of_term x" and 2: "map_component (λk. k - n) x ∈ keys b"
by (auto simp: in_keys_iff)
from this(1) have 3: "map_component (λk. k - n + n) x = x" by (simp add: map_component_def term_simps)
from 2 have "map_component (λk. k + n) (map_component (λk. k - n) x) ∈ map_component (λk. k + n) ` keys b"
by (rule imageI)
with 3 have "x ∈ map_component (λk. k + n) ` keys b" by (simp add: map_component_comp)
thus ?thesis by simp
qed
qed
lemma lookup_lift_poly_syz:
"lookup (lift_poly_syz n b i) =
(λx. if pair_of_term x = (0, i) then 1 else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x) else 0)"
unfolding lift_poly_syz_def
proof (rule Abs_poly_mapping_inverse)
from finite_keys have "finite (map_component (λk. k + n) ` keys b)" ..
hence "finite (insert (term_of_pair (0, i)) (map_component (λk. k + n) ` keys b))" by (rule finite.insertI)
with keys_lift_poly_syz_aux
have "finite {x. (if pair_of_term x = (0, i) then 1
else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x)
else 0) ≠ 0}"
by (rule finite_subset)
thus "(λx. if pair_of_term x = (0, i) then 1
else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x)
else 0) ∈
{f. finite {x. f x ≠ 0}}" by simp
qed
corollary lookup_lift_poly_syz_alt:
"lookup (lift_poly_syz n b i) (term_of_pair (t, j)) =
(if (t, j) = (0, i) then 1 else if n ≤ j then lookup b (term_of_pair (t, j - n)) else 0)"
by (simp only: lookup_lift_poly_syz term_simps)
lemma keys_lift_poly_syz:
"keys (lift_poly_syz n b i) = insert (term_of_pair (0, i)) (map_component (λk. k + n) ` keys b)"
proof
have "keys (lift_poly_syz n b i) ⊆
{x. (if pair_of_term x = (0, i) then 1
else if n ≤ component_of_term x then lookup b (map_component (λk. k - n) x)
else 0) ≠ 0}"
(is "_ ⊆ ?A")
proof
fix x
assume "x ∈ keys (lift_poly_syz n b i)"
hence "lookup (lift_poly_syz n b i) x ≠ 0" by (simp add: in_keys_iff)
thus "x ∈ ?A" by (simp add: lookup_lift_poly_syz)
qed
also note keys_lift_poly_syz_aux
finally show "keys (lift_poly_syz n b i) ⊆ insert (term_of_pair (0, i)) (map_component (λk. k + n) ` keys b)" .
next
show "insert (term_of_pair (0, i)) (map_component (λk. k + n) ` keys b) ⊆ keys (lift_poly_syz n b i)"
proof (simp, rule)
have "lookup (lift_poly_syz n b i) (term_of_pair (0, i)) ≠ 0" by (simp add: lookup_lift_poly_syz_alt)
thus "term_of_pair (0, i) ∈ keys (lift_poly_syz n b i)" by (simp add: in_keys_iff)
next
show "map_component (λk. k + n) ` keys b ⊆ keys (lift_poly_syz n b i)"
proof (rule, elim imageE, simp)
fix x
assume "x ∈ keys b"
hence "lookup (lift_poly_syz n b i) (map_component (λk. k + n) x) ≠ 0"
by (simp add: in_keys_iff lookup_lift_poly_syz_alt map_component_def term_simps)
thus "map_component (λk. k + n) x ∈ keys (lift_poly_syz n b i)" by (simp add: in_keys_iff)
qed
qed
qed
subsubsection ‹@{const proj_poly_syz}›
lemma inj_map_component_plus: "inj (map_component (λk. k + n))"
proof (rule injI)
fix x y
have "inj (λk::nat. k + n)" by (simp add: inj_def)
moreover assume "map_component (λk. k + n) x = map_component (λk. k + n) y"
ultimately show "x = y" by (rule map_component_inj)
qed
lemma lookup_proj_poly_syz: "lookup (proj_poly_syz n p) x = lookup p (map_component (λk. k + n) x)"
by (simp add: proj_poly_syz_def map_key.rep_eq[OF inj_map_component_plus])
lemma lookup_proj_poly_syz_alt:
"lookup (proj_poly_syz n p) (term_of_pair (t, i)) = lookup p (term_of_pair (t, i + n))"
by (simp add: lookup_proj_poly_syz map_component_term_of_pair)
lemma keys_proj_poly_syz: "keys (proj_poly_syz n p) = map_component (λk. k + n) -` keys p"
by (simp add: proj_poly_syz_def keys_map_key[OF inj_map_component_plus])
lemma proj_poly_syz_zero [simp]: "proj_poly_syz n 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly_syz)
lemma proj_poly_syz_plus: "proj_poly_syz n (p + q) = proj_poly_syz n p + proj_poly_syz n q"
by (simp add: proj_poly_syz_def map_key_plus[OF inj_map_component_plus])
lemma proj_poly_syz_sum: "proj_poly_syz n (sum f A) = (∑a∈A. proj_poly_syz n (f a))"
by (rule fun_sum_commute, simp_all add: proj_poly_syz_plus)
lemma proj_poly_syz_sum_list: "proj_poly_syz n (sum_list xs) = sum_list (map (proj_poly_syz n) xs)"
by (rule fun_sum_list_commute, simp_all add: proj_poly_syz_plus)
lemma proj_poly_syz_monom_mult:
"proj_poly_syz n (monom_mult c t p) = monom_mult c t (proj_poly_syz n p)"
by (rule poly_mapping_eqI,
simp add: lookup_proj_poly_syz lookup_monom_mult term_simps adds_pp_def sminus_def)
lemma proj_poly_syz_mult_scalar:
"proj_poly_syz n (mult_scalar q p) = mult_scalar q (proj_poly_syz n p)"
by (rule fun_mult_scalar_commute, simp_all add: proj_poly_syz_plus proj_poly_syz_monom_mult)
lemma proj_poly_syz_lift_poly_syz:
assumes "i < n"
shows "proj_poly_syz n (lift_poly_syz n p i) = p"
proof (rule poly_mapping_eqI, simp add: lookup_proj_poly_syz lookup_lift_poly_syz term_simps map_component_comp,
rule, elim conjE)
fix x::'t
assume "component_of_term x + n = i"
hence "n ≤ i" by simp
with assms show "lookup p x = 1" by simp
qed
lemma proj_poly_syz_eq_zero_iff: "proj_poly_syz n p = 0 ⟷ (component_of_term ` keys p ⊆ {0..<n})"
unfolding keys_eq_empty[symmetric] keys_proj_poly_syz
proof
assume "map_component (λk. k + n) -` keys p = {}" (is "?A = {}")
show "component_of_term ` keys p ⊆ {0..<n}"
proof (rule, rule ccontr)
fix i
assume "i ∈ component_of_term ` keys p"
then obtain x where x: "x ∈ keys p" and i: "i = component_of_term x" ..
assume "i ∉ {0..<n}"
hence "i - n + n = i" by simp
hence 1: "map_component (λk. k - n + n) x = x" by (simp add: map_component_def i term_simps)
have "map_component (λk. k - n) x ∈ ?A" by (rule vimageI2, simp add: map_component_comp x 1)
thus False by (simp add: ‹?A = {}›)
qed
next
assume a: "component_of_term ` keys p ⊆ {0..<n}"
show "map_component (λk. k + n) -` keys p = {}" (is "?A = {}")
proof (rule ccontr)
assume "?A ≠ {}"
then obtain x where "x ∈ ?A" by blast
hence "map_component (λk. k + n) x ∈ keys p" by (rule vimageD)
with a have "component_of_term (map_component (λk. k + n) x) ∈ {0..<n}" by blast
thus False by (simp add: term_simps)
qed
qed
lemma component_of_lt_ge:
assumes "is_pot_ord" and "proj_poly_syz n p ≠ 0"
shows "n ≤ component_of_term (lt p)"
proof -
from assms(2) have "¬ component_of_term ` keys p ⊆ {0..<n}" by (simp add: proj_poly_syz_eq_zero_iff)
then obtain i where "i ∈ component_of_term ` keys p" and "i ∉ {0..<n}" by fastforce
from this(1) obtain x where "x ∈ keys p" and i: "i = component_of_term x" ..
from this(1) have "x ≼⇩t lt p" by (rule lt_max_keys)
with assms(1) have "component_of_term x ≤ component_of_term (lt p)" by (rule is_pot_ordD2)
with ‹i ∉ {0..<n}› show ?thesis by (simp add: i)
qed
lemma lt_proj_poly_syz:
assumes "is_pot_ord" and "proj_poly_syz n p ≠ 0"
shows "lt (proj_poly_syz n p) = map_component (λk. k - n) (lt p)" (is "_ = ?l")
proof -
from component_of_lt_ge[OF assms]
have "component_of_term (lt p) - n + n = component_of_term (lt p)" by simp
hence eq: "map_component (λk. k - n + n) (lt p) = lt p" by (simp add: map_component_def term_simps)
show ?thesis
proof (rule lt_eqI)
have "lookup (proj_poly_syz n p) ?l = lc p"
by (simp add: lc_def lookup_proj_poly_syz term_simps map_component_comp eq)
also have "... ≠ 0"
proof (rule lc_not_0, rule)
assume "p = 0"
hence "proj_poly_syz n p = 0" by simp
with assms(2) show False ..
qed
finally show "lookup (proj_poly_syz n p) ?l ≠ 0" .
next
fix x
assume "lookup (proj_poly_syz n p) x ≠ 0"
hence "map_component (λk. k + n) x ∈ keys p" by (simp add: in_keys_iff lookup_proj_poly_syz)
hence "map_component (λk. k + n) x ≼⇩t lt p" by (rule lt_max_keys)
with assms(1) show "x ≼⇩t ?l" by (auto simp add: is_pot_ord term_simps)
qed
qed
lemma proj_proj_poly_syz: "proj_poly k (proj_poly_syz n p) = proj_poly (k + n) p"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_proj_poly_syz_alt)
lemma poly_mapping_eqI_proj_syz:
assumes "proj_poly_syz n p = proj_poly_syz n q"
and "⋀k. k < n ⟹ proj_poly k p = proj_poly k q"
shows "p = q"
proof (rule poly_mapping_eqI_proj)
fix k
show "proj_poly k p = proj_poly k q"
proof (cases "k < n")
case True
thus ?thesis by (rule assms(2))
next
case False
have "proj_poly (k - n + n) p = proj_poly (k - n + n) q"
by (simp only: proj_proj_poly_syz[symmetric] assms(1))
with False show ?thesis by simp
qed
qed
subsubsection ‹@{const cofactor_list_syz}›
lemma length_cofactor_list_syz [simp]: "length (cofactor_list_syz n p) = n"
by (simp add: cofactor_list_syz_def)
lemma cofactor_list_syz_nth:
assumes "i < n"
shows "(cofactor_list_syz n p) ! i = proj_poly i p"
by (simp add: cofactor_list_syz_def map_idx_nth assms)
lemma cofactor_list_syz_zero [simp]: "cofactor_list_syz n 0 = replicate n 0"
by (rule nth_equalityI, simp_all add: cofactor_list_syz_nth proj_zero)
lemma cofactor_list_syz_plus:
"cofactor_list_syz n (p + q) = map2 (+) (cofactor_list_syz n p) (cofactor_list_syz n q)"
by (rule nth_equalityI, simp_all add: cofactor_list_syz_nth proj_plus)
subsubsection ‹@{const init_syzygy_list}›
lemma length_init_syzygy_list [simp]: "length (init_syzygy_list bs) = length bs"
by (simp add: init_syzygy_list_def)
lemma init_syzygy_list_nth:
assumes "i < length bs"
shows "(init_syzygy_list bs) ! i = lift_poly_syz (length bs) (bs ! i) i"
by (simp add: init_syzygy_list_def map_idx_nth[OF assms])
lemma Keys_init_syzygy_list:
"Keys (set (init_syzygy_list bs)) =
map_component (λk. k + length bs) ` Keys (set bs) ∪ (λi. term_of_pair (0, i)) ` {0..<length bs}"
proof -
have eq1: "(⋃b∈set bs. map_component (λk. k + length bs) ` keys b) =
(⋃i∈{0..<length bs}. map_component (λk. k + length bs) ` keys (bs ! i))"
by (fact UN_upt[symmetric])
have eq2: "(λi. term_of_pair (0, i)) ` {0..<length bs} = (⋃i∈{0..<length bs}. {term_of_pair (0, i)})"
by auto
show ?thesis
by (simp add: init_syzygy_list_def set_map_idx Keys_def keys_lift_poly_syz image_UN
eq1 eq2 UN_Un_distrib[symmetric])
qed
lemma pp_of_Keys_init_syzygy_list_subset:
"pp_of_term ` Keys (set (init_syzygy_list bs)) ⊆ insert 0 (pp_of_term ` Keys (set bs))"
by (auto simp add: Keys_init_syzygy_list image_Un rev_image_eqI term_simps)
lemma pp_of_Keys_init_syzygy_list_superset:
"pp_of_term ` Keys (set bs) ⊆ pp_of_term ` Keys (set (init_syzygy_list bs))"
by (simp add: Keys_init_syzygy_list image_Un term_simps image_image)
lemma pp_of_Keys_init_syzygy_list:
assumes "bs ≠ []"
shows "pp_of_term ` Keys (set (init_syzygy_list bs)) = insert 0 (pp_of_term ` Keys (set bs))"
proof
show "insert 0 (pp_of_term ` Keys (set bs)) ⊆ pp_of_term ` Keys (set (init_syzygy_list bs))"
proof (simp add: pp_of_Keys_init_syzygy_list_superset)
from assms have "{0..<length bs} ≠ {}" by auto
hence "Pair 0 ` {0..<length bs} ≠ {}" by blast
then obtain x::'t where x: "x ∈ (λi. term_of_pair (0, i)) ` {0..<length bs}" by blast
hence "pp_of_term ` (λi. term_of_pair (0, i)) ` {0..<length bs} = {pp_of_term x}"
using image_subset_iff by (auto simp: term_simps)
also from x have "... = {0}" using pp_of_term_of_pair by auto
finally show "0 ∈ pp_of_term ` Keys (set (init_syzygy_list bs))"
by (simp add: Keys_init_syzygy_list image_Un)
qed
qed (fact pp_of_Keys_init_syzygy_list_subset)
lemma component_of_Keys_init_syzygy_list:
"component_of_term ` Keys (set (init_syzygy_list bs)) =
(+) (length bs) ` component_of_term ` Keys (set bs) ∪ {0..<length bs}"
by (simp add: Keys_init_syzygy_list image_Un image_comp o_def ac_simps term_simps)
lemma proj_lift_poly_syz:
assumes "j < n"
shows "proj_poly j (lift_poly_syz n p i) = (1 when j = i)"
proof (simp add: when_def, intro conjI impI)
assume "j = i"
with assms have "¬ n ≤ i" by simp
show "proj_poly i (lift_poly_syz n p i) = 1"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_lift_poly_syz_alt ‹¬ n ≤ i› lookup_one)
next
assume "j ≠ i"
from assms have "¬ n ≤ j" by simp
show "proj_poly j (lift_poly_syz n p i) = 0"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_lift_poly_syz_alt ‹¬ n ≤ j› ‹j ≠ i›)
qed
subsubsection ‹@{const proj_orig_basis}›
lemma length_proj_orig_basis [simp]: "length (proj_orig_basis n bs) = length bs"
by (simp add: proj_orig_basis_def)
lemma proj_orig_basis_nth:
assumes "i < length bs"
shows "(proj_orig_basis n bs) ! i = proj_poly_syz n (bs ! i)"
by (simp add: proj_orig_basis_def assms)
lemma proj_orig_basis_init_syzygy_list [simp]:
"proj_orig_basis (length bs) (init_syzygy_list bs) = bs"
by (rule nth_equalityI, simp_all add: init_syzygy_list_nth proj_orig_basis_nth proj_poly_syz_lift_poly_syz)
lemma set_proj_orig_basis: "set (proj_orig_basis n bs) = proj_poly_syz n ` set bs"
by (simp add: proj_orig_basis_def)
text ‹The following lemma could be generalized from @{const proj_poly_syz} to arbitrary module homomorphisms,
i.\,e. functions respecting ‹0›, addition and scalar multiplication.›
lemma pmdl_proj_orig_basis':
"pmdl (set (proj_orig_basis n bs)) = proj_poly_syz n ` pmdl (set bs)" (is "?A = ?B")
proof
show "?A ⊆ ?B"
proof
fix p
assume "p ∈ pmdl (set (proj_orig_basis n bs))"
thus "p ∈ proj_poly_syz n ` pmdl (set bs)"
proof (induct rule: pmdl_induct)
case module_0
have "0 = proj_poly_syz n 0" by simp
also from pmdl.span_zero have "... ∈ proj_poly_syz n ` pmdl (set bs)" by (rule imageI)
finally show ?case .
next
case (module_plus p b c t)
from module_plus(2) obtain q where "q ∈ pmdl (set bs)" and p: "p = proj_poly_syz n q" ..
from module_plus(3) obtain a where "a ∈ set bs" and b: "b = proj_poly_syz n a"
unfolding set_proj_orig_basis ..
have "p + monom_mult c t b = proj_poly_syz n (q + monom_mult c t a)"
by (simp add: p b proj_poly_syz_monom_mult proj_poly_syz_plus)
also have "... ∈ proj_poly_syz n ` pmdl (set bs)"
proof (rule imageI, rule pmdl.span_add)
show "monom_mult c t a ∈ pmdl (set bs)"
by (rule pmdl_closed_monom_mult, rule pmdl.span_base, fact)
qed fact
finally show ?case .
qed
qed
next
show "?B ⊆ ?A"
proof
fix p
assume "p ∈ proj_poly_syz n ` pmdl (set bs)"
then obtain q where "q ∈ pmdl (set bs)" and p: "p = proj_poly_syz n q" ..
from this(1) show "p ∈ pmdl (set (proj_orig_basis n bs))" unfolding p
proof (induct rule: pmdl_induct)
case module_0
have "proj_poly_syz n 0 = 0" by simp
also have "... ∈ pmdl (set (proj_orig_basis n bs))" by (fact pmdl.span_zero)
finally show ?case .
next
case (module_plus q b c t)
have "proj_poly_syz n (q + monom_mult c t b) =
proj_poly_syz n q + monom_mult c t (proj_poly_syz n b)"
by (simp add: proj_poly_syz_plus proj_poly_syz_monom_mult)
also have "... ∈ pmdl (set (proj_orig_basis n bs))"
proof (rule pmdl.span_add)
show "monom_mult c t (proj_poly_syz n b) ∈ pmdl (set (proj_orig_basis n bs))"
proof (rule pmdl_closed_monom_mult, rule pmdl.span_base)
show "proj_poly_syz n b ∈ set (proj_orig_basis n bs)"
by (simp add: set_proj_orig_basis, rule imageI, fact)
qed
qed fact
finally show ?case .
qed
qed
qed
subsubsection ‹@{const filter_syzygy_basis}›
lemma filter_syzygy_basis_alt: "filter_syzygy_basis n bs = [b←bs. proj_poly_syz n b = 0]"
by (simp add: filter_syzygy_basis_def proj_poly_syz_eq_zero_iff)
lemma set_filter_syzygy_basis:
"set (filter_syzygy_basis n bs) = {b∈set bs. proj_poly_syz n b = 0}"
by (simp add: filter_syzygy_basis_alt)
subsubsection ‹@{const syzygy_module_list}›
lemma syzygy_module_listI:
assumes "s' ∈ pmdl.syzygy_module (set bs)" and "s = atomize_poly (idx_pm_of_pm bs s')"
shows "s ∈ syzygy_module_list bs"
unfolding assms(2) syzygy_module_list_def by (intro imageI, fact assms(1))
lemma syzygy_module_listE:
assumes "s ∈ syzygy_module_list bs"
obtains s' where "s' ∈ pmdl.syzygy_module (set bs)" and "s = atomize_poly (idx_pm_of_pm bs s')"
using assms unfolding syzygy_module_list_def by (elim imageE, simp)
lemma monom_mult_atomize:
"monom_mult c t (atomize_poly p) = atomize_poly (MPoly_Type_Class.punit.monom_mult (monomial c t) 0 p)"
by (rule poly_mapping_eqI_proj, simp add: proj_monom_mult proj_atomize_poly
MPoly_Type_Class.punit.lookup_monom_mult times_monomial_left)
lemma punit_monom_mult_monomial_idx_pm_of_pm:
"MPoly_Type_Class.punit.monom_mult (monomial c t) (0::nat) (idx_pm_of_pm bs s) =
idx_pm_of_pm bs (MPoly_Type_Class.punit.monom_mult (monomial c t) (0::'t ⇒⇩0 'b::ring_1) s)"
by (rule poly_mapping_eqI, simp add: MPoly_Type_Class.punit.lookup_monom_mult lookup_idx_pm_of_pm when_def)
lemma syzygy_module_list_closed_monom_mult:
assumes "s ∈ syzygy_module_list bs"
shows "monom_mult c t s ∈ syzygy_module_list bs"
proof -
from assms obtain s' where s': "s' ∈ pmdl.syzygy_module (set bs)"
and s: "s = atomize_poly (idx_pm_of_pm bs s')" by (rule syzygy_module_listE)
show ?thesis unfolding s
proof (rule syzygy_module_listI)
from s' show "(monomial c t) ⋅ s' ∈ pmdl.syzygy_module (set bs)"
by (rule syzygy_module_closed_map_scale)
next
show "monom_mult c t (atomize_poly (idx_pm_of_pm bs s')) =
atomize_poly (idx_pm_of_pm bs ((monomial c t) ⋅ s'))"
by (simp add: monom_mult_atomize punit_monom_mult_monomial_idx_pm_of_pm
MPoly_Type_Class.punit.map_scale_eq_monom_mult)
qed
qed
lemma pmdl_syzygy_module_list [simp]: "pmdl (syzygy_module_list bs) = syzygy_module_list bs"
proof (rule pmdl_idI)
show "0 ∈ syzygy_module_list bs"
by (rule syzygy_module_listI, fact pmdl.zero_in_syzygy_module, simp add: atomize_zero)
next
fix s1 s2
assume "s1 ∈ syzygy_module_list bs"
then obtain s1' where s1': "s1' ∈ pmdl.syzygy_module (set bs)"
and s1: "s1 = atomize_poly (idx_pm_of_pm bs s1')" by (rule syzygy_module_listE)
assume "s2 ∈ syzygy_module_list bs"
then obtain s2' where s2': "s2' ∈ pmdl.syzygy_module (set bs)"
and s2: "s2 = atomize_poly (idx_pm_of_pm bs s2')" by (rule syzygy_module_listE)
show "s1 + s2 ∈ syzygy_module_list bs"
proof (rule syzygy_module_listI)
from s1' s2' show "s1' + s2' ∈ pmdl.syzygy_module (set bs)"
by (rule pmdl.syzygy_module_closed_plus)
next
show "s1 + s2 = atomize_poly (idx_pm_of_pm bs (s1' + s2'))"
by (simp add: idx_pm_of_pm_plus atomize_plus s1 s2)
qed
qed (fact syzygy_module_list_closed_monom_mult)
text ‹The following lemma also holds without the distinctness constraint on ‹bs›, but then the
proof becomes more difficult.›
lemma syzygy_module_listI':
assumes "distinct bs" and "sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) bs) = 0"
and "component_of_term ` keys s ⊆ {0..<length bs}"
shows "s ∈ syzygy_module_list bs"
proof (rule syzygy_module_listI)
show "pm_of_idx_pm bs (vectorize_poly s) ∈ pmdl.syzygy_module (set bs)"
proof (rule pmdl.syzygy_moduleI, rule pmdl.representsI)
have "(∑v∈keys (pm_of_idx_pm bs (vectorize_poly s)).
mult_scalar (lookup (pm_of_idx_pm bs (vectorize_poly s)) v) v) =
(∑b∈set bs. mult_scalar (lookup (pm_of_idx_pm bs (vectorize_poly s)) b) b)"
by (rule sum.mono_neutral_left, fact finite_set, fact keys_pm_of_idx_pm_subset, simp add: in_keys_iff)
also have "... = sum_list (map (λb. mult_scalar (lookup (pm_of_idx_pm bs (vectorize_poly s)) b) b) bs)"
by (simp only: sum_code distinct_remdups_id[OF assms(1)])
also have "... = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) bs)"
proof (rule arg_cong[of _ _ sum_list], rule nth_equalityI, simp_all)
fix i
assume "i < length bs"
with assms(1) have "lookup (pm_of_idx_pm bs (vectorize_poly s)) (bs ! i) =
cofactor_list_syz (length bs) s ! i"
by (simp add: lookup_pm_of_idx_pm_distinct[OF assms(1)] cofactor_list_syz_nth lookup_vectorize_poly)
thus "mult_scalar (lookup (pm_of_idx_pm bs (vectorize_poly s)) (bs ! i)) (bs ! i) =
mult_scalar (cofactor_list_syz (length bs) s ! i) (bs ! i)" by (simp only:)
qed
also have "... = 0" by (fact assms(2))
finally show "pmdl.rep (pm_of_idx_pm bs (vectorize_poly s)) = 0" by (simp only: pmdl.rep_def)
qed (fact keys_pm_of_idx_pm_subset)
next
from assms(3) have "keys (vectorize_poly s) ⊆ {0..<length bs}" by (simp add: keys_vectorize_poly)
with assms(1) have "idx_pm_of_pm bs (pm_of_idx_pm bs (vectorize_poly s)) = vectorize_poly s"
by (rule idx_pm_of_pm_of_idx_pm)
thus "s = atomize_poly (idx_pm_of_pm bs (pm_of_idx_pm bs (vectorize_poly s)))"
by (simp add: atomize_vectorize_poly)
qed
lemma component_of_syzygy_module_list:
assumes "s ∈ syzygy_module_list bs"
shows "component_of_term ` keys s ⊆ {0..<length bs}"
proof -
from assms obtain s' where s: "s = atomize_poly (idx_pm_of_pm bs s')"
by (rule syzygy_module_listE)
have "component_of_term ` keys s ⊆ (⋃x∈{0..<length bs}. {x})"
by (simp only: s keys_atomize_poly image_UN, rule UN_mono, fact keys_idx_pm_of_pm_subset, auto simp: term_simps)
also have "... = {0..<length bs}" by simp
finally show ?thesis .
qed
lemma map2_mult_scalar_proj_poly_syz:
"map2 mult_scalar xs (map (proj_poly_syz n) ys) =
map (proj_poly_syz n ∘ (λ(x, y). mult_scalar x y)) (zip xs ys)"
by (rule nth_equalityI, simp_all add: proj_poly_syz_mult_scalar)
lemma map2_times_proj:
"map2 (*) xs (map (proj_poly k) ys) = map (proj_poly k ∘ (λ(x, y). x ⊙ y)) (zip xs ys)"
by (rule nth_equalityI, simp_all add: proj_mult_scalar)
text ‹Probably the following lemma also holds without the distinctness constraint on ‹bs›.›
lemma syzygy_module_list_subset:
assumes "distinct bs"
shows "syzygy_module_list bs ⊆ pmdl (set (init_syzygy_list bs))"
proof
let ?as = "init_syzygy_list bs"
fix s
assume "s ∈ syzygy_module_list bs"
then obtain s' where s': "s' ∈ pmdl.syzygy_module (set bs)"
and s: "s = atomize_poly (idx_pm_of_pm bs s')" by (rule syzygy_module_listE)
from s' have "pmdl.represents (set bs) s' 0" by (rule pmdl.syzygy_moduleD)
hence "keys s' ⊆ set bs" and 1: "0 = pmdl.rep s'"
by (rule pmdl.representsD1, rule pmdl.representsD2)
have "s = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) (init_syzygy_list bs))"
(is "_ = ?r")
proof (rule poly_mapping_eqI_proj_syz)
have "proj_poly_syz (length bs) ?r =
sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s)
(map (proj_poly_syz (length bs)) (init_syzygy_list bs)))"
by (simp add: proj_poly_syz_sum_list map2_mult_scalar_proj_poly_syz)
also have "... = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) bs)"
by (simp add: proj_orig_basis_def[symmetric])
also have "... = sum_list (map (λb. mult_scalar (lookup s' b) b) bs)"
proof (rule arg_cong[of _ _ sum_list], rule nth_equalityI, simp_all)
fix i
assume "i < length bs"
with assms(1) have "lookup s' (bs ! i) = cofactor_list_syz (length bs) s ! i"
by (simp add: s cofactor_list_syz_nth lookup_idx_pm_of_pm proj_atomize_poly)
thus "mult_scalar (cofactor_list_syz (length bs) s ! i) (bs ! i) =
mult_scalar (lookup s' (bs ! i)) (bs ! i)" by (simp only:)
qed
also have "... = (∑b∈set bs. mult_scalar (lookup s' b) b)"
by (simp only: sum_code distinct_remdups_id[OF assms])
also have "... = (∑v∈keys s'. mult_scalar (lookup s' v) v)"
by (rule sum.mono_neutral_right, fact finite_set, fact, simp add: in_keys_iff)
also have "... = 0" by (simp add: 1 pmdl.rep_def)
finally have eq: "proj_poly_syz (length bs) ?r = 0" .
show "proj_poly_syz (length bs) s = proj_poly_syz (length bs) ?r"
by (simp add: eq ‹s ∈ syzygy_module_list bs› proj_poly_syz_eq_zero_iff component_of_syzygy_module_list)
next
fix k
assume "k < length bs"
have "proj_poly k s = map2 (*) (cofactor_list_syz (length bs) s) (map (proj_poly k)
(init_syzygy_list bs)) ! k"
by (simp add: ‹k < length bs› init_syzygy_list_nth proj_lift_poly_syz cofactor_list_syz_nth)
also have "... = sum_list (map2 (*) (cofactor_list_syz (length bs) s)
(map (proj_poly k) (init_syzygy_list bs)))"
by (rule sum_list_eq_nthI[symmetric],
simp_all add: ‹k < length bs› init_syzygy_list_nth proj_lift_poly_syz)
also have "... = proj_poly k ?r"
by (simp add: proj_sum_list map2_times_proj)
finally show "proj_poly k s = proj_poly k ?r" .
qed
also have "… ∈ pmdl (set (init_syzygy_list bs))" by (fact pmdl.span_listI)
finally show "s ∈ pmdl (set (init_syzygy_list bs))" .
qed
subsubsection ‹Cofactors›
lemma map2_mult_scalar_plus:
"map2 (⊙) (map2 (+) xs ys) zs = map2 (+) (map2 (⊙) xs zs) (map2 (⊙) ys zs)"
by (rule nth_equalityI, simp_all add: mult_scalar_distrib_right)
lemma syz_cofactors:
assumes "p ∈ pmdl (set (init_syzygy_list bs))"
shows "proj_poly_syz (length bs) p = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) p) bs)"
using assms
proof (induct rule: pmdl_induct)
case module_0
show ?case by (simp, rule sum_list_zeroI', simp)
next
case (module_plus p b c t)
from this(3) obtain i where i: "i < length bs" and b: "b = (init_syzygy_list bs) ! i"
unfolding length_init_syzygy_list[symmetric, of bs] by (metis in_set_conv_nth)
have "proj_poly_syz (length bs) (p + monom_mult c t b) =
proj_poly_syz (length bs) p + monom_mult c t (bs ! i)"
by (simp only: proj_poly_syz_plus proj_poly_syz_monom_mult b init_syzygy_list_nth[OF i]
proj_poly_syz_lift_poly_syz[OF i])
also have "... = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) p) bs) +
monom_mult c t (bs ! i)" by (simp only: module_plus(2))
also have "... = sum_list (map2 mult_scalar (cofactor_list_syz (length bs) (p + monom_mult c t b)) bs)"
proof (simp add: cofactor_list_syz_plus map2_mult_scalar_plus sum_list_map2_plus)
have proj_b: "j < length bs ⟹ proj_poly j b = (1 when j = i)" for j
by (simp add: b init_syzygy_list_nth i proj_lift_poly_syz)
have eq: "j < length bs ⟹ (map2 mult_scalar (cofactor_list_syz (length bs) (monom_mult c t b)) bs) ! j =
(monom_mult c t (bs ! i) when j = i)" for j
by (simp add: cofactor_list_syz_nth proj_monom_mult proj_b mult_scalar_monom_mult when_def)
have "sum_list (map2 mult_scalar (cofactor_list_syz (length bs) (monom_mult c t b)) bs) =
(map2 mult_scalar (cofactor_list_syz (length bs) (monom_mult c t b)) bs) ! i"
by (rule sum_list_eq_nthI, simp add: i, simp add: eq del: nth_zip nth_map)
also have "... = mult_scalar (punit.monom_mult c t (proj_poly i b)) (bs ! i)"
by (simp add: i cofactor_list_syz_nth proj_monom_mult)
also have "... = monom_mult c t (bs ! i)"
by (simp add: proj_b i mult_scalar_monomial times_monomial_left[symmetric])
finally show "monom_mult c t (bs ! i) =
sum_list (map2 mult_scalar (cofactor_list_syz (length bs) (monom_mult c t b)) bs)"
by (simp only:)
qed
finally show ?case .
qed
subsubsection ‹Modules›
lemma pmdl_proj_orig_basis:
assumes "pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
shows "pmdl (set (proj_orig_basis (length bs) gs)) = pmdl (set bs)"
by (simp add: pmdl_proj_orig_basis' assms,
simp only: pmdl_proj_orig_basis'[symmetric] proj_orig_basis_init_syzygy_list)
lemma pmdl_filter_syzygy_basis_subset:
assumes "distinct bs" and "pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
shows "pmdl (set (filter_syzygy_basis (length bs) gs)) ⊆ pmdl (syzygy_module_list bs)"
proof (rule pmdl.span_mono, rule)
fix s
assume "s ∈ set (filter_syzygy_basis (length bs) gs)"
hence "s ∈ set gs" and eq: "proj_poly_syz (length bs) s = 0"
by (simp_all add: set_filter_syzygy_basis)
from this(1) have "s ∈ pmdl (set gs)" by (rule pmdl.span_base)
hence "s ∈ pmdl (set (init_syzygy_list bs))" by (simp only: assms)
hence "proj_poly_syz (length bs) s =
sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) bs)"
by (rule syz_cofactors)
hence "distinct bs" and "sum_list (map2 mult_scalar (cofactor_list_syz (length bs) s) bs) = 0"
by (simp_all only: eq assms(1))
moreover from eq have "component_of_term ` keys s ⊆ {0..<length bs}" by (simp only: proj_poly_syz_eq_zero_iff)
ultimately show "s ∈ syzygy_module_list bs" by (rule syzygy_module_listI')
qed
lemma ex_filter_syzygy_basis_adds_lt:
assumes "is_pot_ord" and "distinct bs" and "is_Groebner_basis (set gs)"
and "pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
and "f ∈ pmdl (syzygy_module_list bs)" and "f ≠ 0"
shows "∃g∈set (filter_syzygy_basis (length bs) gs). g ≠ 0 ∧ lt g adds⇩t lt f"
proof -
from assms(5) have "f ∈ syzygy_module_list bs" by simp
also from assms(2) have "... ⊆ pmdl (set (init_syzygy_list bs))"
by (rule syzygy_module_list_subset)
also have "... = pmdl (set gs)" by (simp only: assms(4))
finally have "f ∈ pmdl (set gs)" .
with assms(3, 6) obtain g where "g ∈ set gs" and "g ≠ 0"
and adds: "lt g adds⇩t lt f" unfolding GB_alt_3_finite[OF finite_set] by blast
show ?thesis
proof (intro bexI conjI)
show "g ∈ set (filter_syzygy_basis (length bs) gs)"
proof (simp add: set_filter_syzygy_basis, rule)
show "proj_poly_syz (length bs) g = 0"
proof (rule ccontr)
assume "proj_poly_syz (length bs) g ≠ 0"
with assms(1) have "length bs ≤ component_of_term (lt g)" by (rule component_of_lt_ge)
also from adds have "... = component_of_term (lt f)" by (simp add: adds_term_def)
also have "... < length bs"
proof -
from ‹f ≠ 0› have "lt f ∈ keys f" by (rule lt_in_keys)
hence "component_of_term (lt f) ∈ component_of_term ` keys f" by (rule imageI)
also from ‹f ∈ syzygy_module_list bs› have "... ⊆ {0..<length bs}"
by (rule component_of_syzygy_module_list)
finally show "component_of_term (lt f) < length bs" by simp
qed
finally show False ..
qed
qed fact
qed fact+
qed
lemma pmdl_filter_syzygy_basis:
fixes bs::"('t ⇒⇩0 'b::field) list"
assumes "is_pot_ord" and "distinct bs" and "is_Groebner_basis (set gs)" and
"pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
shows "pmdl (set (filter_syzygy_basis (length bs) gs)) = syzygy_module_list bs"
proof -
from finite_set
have "pmdl (set (filter_syzygy_basis (length bs) gs)) = pmdl (syzygy_module_list bs)"
proof (rule pmdl_eqI_adds_lt_finite)
from assms(2, 4)
show "pmdl (set (filter_syzygy_basis (length bs) gs)) ⊆ pmdl (syzygy_module_list bs)"
by (rule pmdl_filter_syzygy_basis_subset)
next
fix f
assume "f ∈ pmdl (syzygy_module_list bs)" and "f ≠ 0"
with assms show "∃g∈set (filter_syzygy_basis (length bs) gs). g ≠ 0 ∧ lt g adds⇩t lt f"
by (rule ex_filter_syzygy_basis_adds_lt)
qed
thus ?thesis by simp
qed
subsubsection ‹Gr\"obner Bases›
lemma proj_orig_basis_isGB:
assumes "is_pot_ord" and "is_Groebner_basis (set gs)" and "pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
shows "is_Groebner_basis (set (proj_orig_basis (length bs) gs))"
unfolding GB_alt_3_finite[OF finite_set]
proof (intro ballI impI)
fix f
assume "f ∈ pmdl (set (proj_orig_basis (length bs) gs))"
also have "... = proj_poly_syz (length bs) ` pmdl (set gs)" by (fact pmdl_proj_orig_basis')
finally obtain h where "h ∈ pmdl (set gs)" and f: "f = proj_poly_syz (length bs) h" ..
assume "f ≠ 0"
with assms(1) have ltf: "lt f = map_component (λk. k - length bs) (lt h)" unfolding f
by (rule lt_proj_poly_syz)
from ‹f ≠ 0› have "h ≠ 0" by (auto simp add: f)
with assms(2) ‹h ∈ pmdl (set gs)› obtain g where "g ∈ set gs" and "g ≠ 0"
and "lt g adds⇩t lt h" unfolding GB_alt_3_finite[OF finite_set] by blast
from this(3) have 1: "component_of_term (lt g) = component_of_term (lt h)"
and 2: "pp_of_term (lt g) adds pp_of_term (lt h)" by (simp_all add: adds_term_def)
let ?g = "proj_poly_syz (length bs) g"
have "?g ≠ 0"
proof (simp add: proj_poly_syz_eq_zero_iff, rule)
assume "component_of_term ` keys g ⊆ {0..<length bs}"
from assms(1) ‹f ≠ 0› have "length bs ≤ component_of_term (lt h)"
unfolding f by (rule component_of_lt_ge)
hence "component_of_term (lt g) ∉ {0..<length bs}" by (simp add: 1)
moreover from ‹g ≠ 0› have "lt g ∈ keys g" by (rule lt_in_keys)
ultimately show False using ‹component_of_term ` keys g ⊆ {0..<length bs}› by blast
qed
with assms(1) have ltg: "lt ?g = map_component (λk. k - length bs) (lt g)" by (rule lt_proj_poly_syz)
show "∃g∈set (proj_orig_basis (length bs) gs). g ≠ 0 ∧ lt g adds⇩t lt f"
proof (intro bexI conjI)
show "lt ?g adds⇩t lt f" by (simp add: ltf ltg adds_term_def 1 2 term_simps)
next
show "?g ∈ set (proj_orig_basis (length bs) gs)"
unfolding set_proj_orig_basis using ‹g ∈ set gs› by (rule imageI)
qed fact
qed
lemma filter_syzygy_basis_isGB:
assumes "is_pot_ord" and "distinct bs" and "is_Groebner_basis (set gs)"
and "pmdl (set gs) = pmdl (set (init_syzygy_list bs))"
shows "is_Groebner_basis (set (filter_syzygy_basis (length bs) gs))"
unfolding GB_alt_3_finite[OF finite_set]
proof (intro ballI impI)
fix f::"'t ⇒⇩0 'b"
assume "f ≠ 0"
assume "f ∈ pmdl (set (filter_syzygy_basis (length bs) gs))"
also from assms have "... = syzygy_module_list bs" by (rule pmdl_filter_syzygy_basis)
finally have "f ∈ pmdl (syzygy_module_list bs)" by simp
from assms this ‹f ≠ 0›
show "∃g∈set (filter_syzygy_basis (length bs) gs). g ≠ 0 ∧ lt g adds⇩t lt f"
by (rule ex_filter_syzygy_basis_adds_lt)
qed
end
end