Quelle  Syzygy.thy

(* Author: Alexander Maletzky *)

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 ==>₀ 'a) ==> 'b"
  where "rep r = (∑v∈keys r. lookup r v *s v)"

definition represents :: "'b set ==> ('b ==>₀ 'a) ==> 'b ==> bool"
  where "represents B r x ⟷ (keys r ⊆ B ∧ local.rep r = x)"

definition syzygy_module :: "'b set ==> ('b ==>₀ '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 (* module *)

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 (* term_powerprod *)

subsection ‹Polynomial Mappings on List-Indices›

definition pm_of_idx_pm :: "('a list) ==> (nat ==>₀ 'b) ==> 'a ==>₀ '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 ==>₀ 'b) ==> nat ==>₀ '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 (* ordered_term *)

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 ==>₀ 'b) ==> nat ==> ('t ==>₀ '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 ==>₀ 'b) ==> ('t ==>₀ '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 ==>₀ 'b) ==> ('a ==>₀ 'b::semiring_1) list"
  where "cofactor_list_syz n b = map (λi. proj_poly i b) [0..<n]"

definition init_syzygy_list :: "('t ==>₀ 'b) list ==> ('t ==>₀ 'b::semiring_1) list"
  where "init_syzygy_list bs = map_idx (lift_poly_syz (length bs)) bs 0"

definition proj_orig_basis :: "nat ==> ('t ==>₀ 'b) list ==> ('t ==>₀ 'b::semiring_1) list"
  where "proj_orig_basis n bs = map (proj_poly_syz n) bs"

definition filter_syzygy_basis :: "nat ==> ('t ==>₀ 'b) list ==> ('t ==>₀ 'b::semiring_1) list"
  where "filter_syzygy_basis n bs = [b←bs. component_of_term ` keys b ⊆ {0..<n}]"

definition syzygy_module_list :: "('t ==>₀ 'b) list ==> ('t ==>₀ '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 ==><sub>0</sub> '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 ==>₀ '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 ==>₀ '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<sub>t</sub> 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 ==>₀ '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 (* gd_inf_term *)

end (* theory *)