Theory Syzygy

(* 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 0 'a)  'b"
  where "rep r = (vkeys 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: "(vkeys r  keys s. lookup r v *s v) = (vkeys r. lookup r v *s v)"
  proof (rule sum.mono_neutral_right)
    show "vkeys r  keys s - keys r. lookup r v *s v = 0" by (simp add: in_keys_iff)
  qed simp
  from fin have eq2: "(vkeys r  keys s. lookup s v *s v) = (vkeys s. lookup s v *s v)"
  proof (rule sum.mono_neutral_right)
    show "vkeys r  keys s - keys s. lookup s v *s v = 0" by (simp add: in_keys_iff)
  qed simp
  have "rep (r + s) = (vkeys (r + s). lookup (r + s) v *s v)" by (simp only: rep_def)
  also have "... = (vkeys r  keys s. lookup (r + s) v *s v)"
  proof (rule sum.mono_neutral_left)
    show "ikeys 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 "... = (vkeys r  keys s. lookup r v *s v) + (vkeys 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: "(vkeys r  keys s. lookup r v *s v) = (vkeys r. lookup r v *s v)"
  proof (rule sum.mono_neutral_right)
    show "vkeys r  keys s - keys r. lookup r v *s v = 0" by (simp add: in_keys_iff)
  qed simp
  from fin have eq2: "(vkeys r  keys s. lookup s v *s v) = (vkeys s. lookup s v *s v)"
  proof (rule sum.mono_neutral_right)
    show "vkeys r  keys s - keys s. lookup s v *s v = 0" by (simp add: in_keys_iff)
  qed simp
  have "rep (r - s) = (vkeys (r - s). lookup (r - s) v *s v)" by (simp only: rep_def)
  also from fin keys_minus have "... = (vkeys r  keys s. lookup (r - s) v *s v)"
  proof (rule sum.mono_neutral_left)
    show "ikeys r  keys s - keys (r - s). lookup (r - s) i *s i = 0" by (simp add: in_keys_iff)
  qed
  also have "... = (vkeys r  keys s. lookup r v *s v) - (vkeys 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) = (vkeys (monomial c 0 * r). lookup (monomial c 0 * r) v *s v)"
    by (simp only: rep_def)
  also from finite_keys sub have "... = (vkeys r. lookup (monomial c 0 * r) v *s v)"
  proof (rule sum.mono_neutral_left)
    show "vkeys 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 (vkeys 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 = (aA. 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 = (aA. lookup r a *s a)" unfolding x by (rule sum.cong, simp_all add: 1)
    also from finite A 2 have "... = (akeys r. lookup r a *s a)"
    proof (rule sum.mono_neutral_right)
      show "aA - 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)  (vkeys 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 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 (* 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 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 = [bbs. 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) = (aA. 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: "(bset 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 = [bbs. 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) = {bset 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 "(vkeys (pm_of_idx_pm bs (vectorize_poly s)).
              mult_scalar (lookup (pm_of_idx_pm bs (vectorize_poly s)) v) v) =
          (bset 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 "... = (bset bs. mult_scalar (lookup s' b) b)"
      by (simp only: sum_code distinct_remdups_id[OF assms])
    also have "... = (vkeys 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 "gset (filter_syzygy_basis (length bs) gs). g  0  lt g addst 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 addst 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 "gset (filter_syzygy_basis (length bs) gs). g  0  lt g addst 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 addst 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 "gset (proj_orig_basis (length bs) gs). g  0  lt g addst lt f"
  proof (intro bexI conjI)
    show "lt ?g addst 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 "gset (filter_syzygy_basis (length bs) gs). g  0  lt g addst lt f"
    by (rule ex_filter_syzygy_basis_adds_lt)
qed

end (* gd_inf_term *)

end (* theory *)