Theory Groebner_Bases

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Gr\"obner Bases and Buchberger's Theorem›

theory Groebner_Bases
imports Reduction
begin

text ‹This theory provides the main results about Gr\"obner bases for modules of multivariate polynomials.›

context gd_term
begin

definition crit_pair :: "('t ⇒⇩0 'b::field) ⇒ ('t ⇒⇩0 'b) ⇒ (('t ⇒⇩0 'b) × ('t ⇒⇩0 'b))"
  where "crit_pair p q =
          (if component_of_term (lt p) = component_of_term (lt q) then
            (monom_mult (1 / lc p) ((lcs (lp p) (lp q)) - (lp p)) (tail p),
            monom_mult (1 / lc q) ((lcs (lp p) (lp q)) - (lp q)) (tail q))
          else (0, 0))"

definition crit_pair_cbelow_on :: "('a ⇒ nat) ⇒ nat ⇒ ('t ⇒⇩0 'b::field) set ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b) ⇒ bool"
  where "crit_pair_cbelow_on d m F p q ⟷
                cbelow_on (dgrad_p_set d m) (≺⇩p)
                          (monomial 1 (term_of_pair (lcs (lp p) (lp q), component_of_term (lt p))))
                          (λa b. red F a b ∨ red F b a) (fst (crit_pair p q)) (snd (crit_pair p q))"

definition spoly :: "('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b::field)"
  where "spoly p q = (let v1 = lt p; v2 = lt q in
                      if component_of_term v1 = component_of_term v2 then
                        let t1 = pp_of_term v1; t2 = pp_of_term v2; l = lcs t1 t2 in
                        (monom_mult (1 / lookup p v1) (l - t1) p) - (monom_mult (1 / lookup q v2) (l - t2) q)
                      else 0)"

definition (in ordered_term) is_Groebner_basis :: "('t ⇒⇩0 'b::field) set ⇒ bool"
  where "is_Groebner_basis F ≡ relation.is_ChurchRosser (red F)"

subsection ‹Critical Pairs and S-Polynomials›

lemma crit_pair_same: "fst (crit_pair p p) = snd (crit_pair p p)"
  by (simp add: crit_pair_def)

lemma crit_pair_swap: "crit_pair p q = (snd (crit_pair q p), fst (crit_pair q p))"
  by (simp add: crit_pair_def lcs_comm)

lemma crit_pair_zero [simp]: "fst (crit_pair 0 q) = 0" and "snd (crit_pair p 0) = 0"
  by (simp_all add: crit_pair_def)

lemma dgrad_p_set_le_crit_pair_zero: "dgrad_p_set_le d {fst (crit_pair p 0)} {p}"
proof (simp add: crit_pair_def lt_def[of 0] lcs_comm lcs_zero dgrad_p_set_le_def Keys_insert
      min_term_def term_simps, intro conjI impI dgrad_set_leI)
  fix s
  assume "s ∈ pp_of_term ` keys (monom_mult (1 / lc p) 0 (tail p))"
  then obtain v where "v ∈ keys (monom_mult (1 / lc p) 0 (tail p))" and "s = pp_of_term v" ..
  from this(1) keys_monom_mult_subset have "v ∈ (⊕) 0 ` keys (tail p)" ..
  hence "v ∈ keys (tail p)" by (simp add: image_iff term_simps)
  hence "v ∈ keys p" by (simp add: keys_tail)
  hence "s ∈ pp_of_term ` keys p" by (simp add: ‹s = pp_of_term v›)
  moreover have "d s ≤ d s" ..
  ultimately show "∃t∈pp_of_term ` keys p. d s ≤ d t" ..
qed simp

lemma dgrad_p_set_le_fst_crit_pair:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d {fst (crit_pair p q)} {p, q}"
proof (cases "q = 0")
  case True
  have "dgrad_p_set_le d {fst (crit_pair p q)} {p}" unfolding True
    by (fact dgrad_p_set_le_crit_pair_zero)
  also have "dgrad_p_set_le d ... {p, q}" by (rule dgrad_p_set_le_subset, simp)
  finally show ?thesis .
next
  case False
  show ?thesis
  proof (cases "p = 0")
    case True
    have "dgrad_p_set_le d {fst (crit_pair p q)} {q}"
      by (simp add: True dgrad_p_set_le_def dgrad_set_le_def)
    also have "dgrad_p_set_le d ... {p, q}" by (rule dgrad_p_set_le_subset, simp)
    finally show ?thesis .
  next
    case False
    show ?thesis
    proof (simp add: dgrad_p_set_le_def Keys_insert crit_pair_def, intro conjI impI)
      define t where "t = lcs (lp p) (lp q) - lp p"
      let ?m = "monom_mult (1 / lc p) t (tail p)"
      from assms have "dgrad_set_le d (pp_of_term ` keys ?m) (insert t (pp_of_term ` keys (tail p)))"
        by (rule dgrad_set_le_monom_mult)
      also have "dgrad_set_le d ... (pp_of_term ` (keys p ∪ keys q))"
      proof (rule dgrad_set_leI, simp)
        fix s
        assume "s = t ∨ s ∈ pp_of_term ` keys (tail p)"
        thus "∃v∈keys p ∪ keys q. d s ≤ d (pp_of_term v)"
        proof
          assume "s = t"
          from assms have "d s ≤ ord_class.max (d (lp p)) (d (lp q))"
            unfolding ‹s = t› t_def by (rule dickson_grading_lcs_minus)
          hence "d s ≤ d (lp p) ∨ d s ≤ d (lp q)" by auto
          thus ?thesis
          proof
            from ‹p ≠ 0› have "lt p ∈ keys p" by (rule lt_in_keys)
            hence "lt p ∈ keys p ∪ keys q" by simp
            moreover assume "d s ≤ d (lp p)"
            ultimately show ?thesis ..
          next
            from ‹q ≠ 0› have "lt q ∈ keys q" by (rule lt_in_keys)
            hence "lt q ∈ keys p ∪ keys q" by simp
            moreover assume "d s ≤ d (lp q)"
            ultimately show ?thesis ..
          qed
        next
          assume "s ∈ pp_of_term ` keys (tail p)"
          hence "s ∈ pp_of_term ` (keys p ∪ keys q)" by (auto simp: keys_tail)
          then obtain v where "v ∈ keys p ∪ keys q" and "s = pp_of_term v" ..
          note this(1)
          moreover have "d s ≤ d (pp_of_term v)" by (simp add: ‹s = pp_of_term v›)
          ultimately show ?thesis ..
        qed
      qed
      finally show "dgrad_set_le d (pp_of_term ` keys ?m) (pp_of_term ` (keys p ∪ keys q))" .
    qed (rule dgrad_set_leI, simp)
  qed
qed

lemma dgrad_p_set_le_snd_crit_pair:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d {snd (crit_pair p q)} {p, q}"
  by (simp add: crit_pair_swap[of p] insert_commute[of p q], rule dgrad_p_set_le_fst_crit_pair, fact)

lemma dgrad_p_set_closed_fst_crit_pair:
  assumes "dickson_grading d" and "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m"
  shows "fst (crit_pair p q) ∈ dgrad_p_set d m"
proof -
  from dgrad_p_set_le_fst_crit_pair[OF assms(1)] have "{fst (crit_pair p q)} ⊆ dgrad_p_set d m"
  proof (rule dgrad_p_set_le_dgrad_p_set)
    from assms(2, 3) show "{p, q} ⊆ dgrad_p_set d m" by simp
  qed
  thus ?thesis by simp
qed

lemma dgrad_p_set_closed_snd_crit_pair:
  assumes "dickson_grading d" and "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m"
  shows "snd (crit_pair p q) ∈ dgrad_p_set d m"
  by (simp add: crit_pair_swap[of p q], rule dgrad_p_set_closed_fst_crit_pair, fact+)

lemma fst_crit_pair_below_lcs:
  "fst (crit_pair p q) ≺⇩p monomial 1 (term_of_pair (lcs (lp p) (lp q), component_of_term (lt p)))"
proof (cases "tail p = 0")
  case True
  thus ?thesis by (simp add: crit_pair_def ord_strict_p_monomial_iff)
next
  case False
  let ?t1 = "lp p"
  let ?t2 = "lp q"
  from False have "p ≠ 0" by auto
  hence "lc p ≠ 0" by (rule lc_not_0)
  hence "1 / lc p ≠ 0" by simp
  from this False have "lt (monom_mult (1 / lc p) (lcs ?t1 ?t2 - ?t1) (tail p)) =
                        (lcs ?t1 ?t2 - ?t1) ⊕ lt (tail p)"
    by (rule lt_monom_mult)
  also from lt_tail[OF False] have "... ≺⇩t (lcs ?t1 ?t2 - ?t1) ⊕ lt p"
    by (rule splus_mono_strict)
  also from adds_lcs have "... = term_of_pair (lcs ?t1 ?t2, component_of_term (lt p))"
    by (simp add: adds_lcs adds_minus splus_def)
  finally show ?thesis by (auto simp add: crit_pair_def ord_strict_p_monomial_iff)
qed

lemma snd_crit_pair_below_lcs:
  "snd (crit_pair p q) ≺⇩p monomial 1 (term_of_pair (lcs (lp p) (lp q), component_of_term (lt p)))"
proof (cases "component_of_term (lt p) = component_of_term (lt q)")
  case True
  show ?thesis
    by (simp add: True crit_pair_swap[of p] lcs_comm[of "lp p"], fact fst_crit_pair_below_lcs)
next
  case False
  show ?thesis by (simp add: crit_pair_def False ord_strict_p_monomial_iff)
qed

lemma crit_pair_cbelow_same:
  assumes "dickson_grading d" and "p ∈ dgrad_p_set d m"
  shows "crit_pair_cbelow_on d m F p p"
proof (simp add: crit_pair_cbelow_on_def crit_pair_same cbelow_on_def term_simps, intro disjI1 conjI)
  from assms(1) assms(2) assms(2) show "snd (crit_pair p p) ∈ dgrad_p_set d m"
    by (rule dgrad_p_set_closed_snd_crit_pair)
next
  from snd_crit_pair_below_lcs[of p p] show "snd (crit_pair p p) ≺⇩p monomial 1 (lt p)"
    by (simp add: term_simps)
qed

lemma crit_pair_cbelow_distinct_component:
  assumes "component_of_term (lt p) ≠ component_of_term (lt q)"
  shows "crit_pair_cbelow_on d m F p q"
  by (simp add: crit_pair_cbelow_on_def crit_pair_def assms cbelow_on_def
      ord_strict_p_monomial_iff zero_in_dgrad_p_set)

lemma crit_pair_cbelow_sym:
  assumes "crit_pair_cbelow_on d m F p q"
  shows "crit_pair_cbelow_on d m F q p"
proof (cases "component_of_term (lt q) = component_of_term (lt p)")
  case True
  from assms show ?thesis
  proof (simp add: crit_pair_cbelow_on_def crit_pair_swap[of p q] lcs_comm True,
         elim cbelow_on_symmetric)
    show "symp (λa b. red F a b ∨ red F b a)" by (simp add: symp_def)
  qed
next
  case False
  thus ?thesis by (rule crit_pair_cbelow_distinct_component)
qed

lemma crit_pair_cs_imp_crit_pair_cbelow_on:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m" and "p ∈ dgrad_p_set d m"
    and "q ∈ dgrad_p_set d m"
    and "relation.cs (red F) (fst (crit_pair p q)) (snd (crit_pair p q))"
  shows "crit_pair_cbelow_on d m F p q"
proof -
  from assms(1) have "relation_order (red F) (≺⇩p) (dgrad_p_set d m)" by (rule is_relation_order_red)
  moreover have "relation.dw_closed (red F) (dgrad_p_set d m)"
    by (rule relation.dw_closedI, rule dgrad_p_set_closed_red, rule assms(1), rule assms(2))
  moreover note assms(5)
  moreover from assms(1) assms(3) assms(4) have "fst (crit_pair p q) ∈ dgrad_p_set d m"
    by (rule dgrad_p_set_closed_fst_crit_pair)
  moreover from assms(1) assms(3) assms(4) have "snd (crit_pair p q) ∈ dgrad_p_set d m"
    by (rule dgrad_p_set_closed_snd_crit_pair)
  moreover note fst_crit_pair_below_lcs snd_crit_pair_below_lcs
  ultimately show ?thesis unfolding crit_pair_cbelow_on_def by (rule relation_order.cs_implies_cbelow_on)
qed

lemma crit_pair_cbelow_mono:
  assumes "crit_pair_cbelow_on d m F p q" and "F ⊆ G"
  shows "crit_pair_cbelow_on d m G p q"
  using assms(1) unfolding crit_pair_cbelow_on_def
proof (induct rule: cbelow_on_induct)
  case base
  show ?case by (simp add: cbelow_on_def, intro disjI1 conjI, fact+)
next
  case (step b c)
  from step(2) have "red G b c ∨ red G c b" using red_subset[OF _ assms(2)] by blast
  from step(5) step(3) this step(4) show ?case ..
qed

lemma lcs_red_single_fst_crit_pair:
  assumes "p ≠ 0" and "component_of_term (lt p) = component_of_term (lt q)"
  defines "t1 ≡ lp p"
  defines "t2 ≡ lp q"
  shows "red_single (monomial (- 1) (term_of_pair (lcs t1 t2, component_of_term (lt p))))
                    (fst (crit_pair p q)) p (lcs t1 t2 - t1)"
proof -
  let ?l = "term_of_pair (lcs t1 t2, component_of_term (lt p))"
  from assms(1) have "lc p ≠ 0" by (rule lc_not_0)
  have "lt p adds⇩t ?l" by (simp add: adds_lcs adds_term_def t1_def term_simps)
  hence eq1: "(lcs t1 t2 - t1) ⊕ lt p = ?l"
    by (simp add: adds_lcs adds_minus splus_def t1_def)
  with assms(1) show ?thesis
  proof (simp add: crit_pair_def red_single_def assms(2))
    have eq2: "monomial (- 1) ?l = monom_mult (- (1 / lc p)) (lcs t1 t2 - t1) (monomial (lc p) (lt p))"
      by (simp add: monom_mult_monomial eq1 ‹lc p ≠ 0›)
    show "monom_mult (1 / lc p) (lcs (lp p) (lp q) - lp p) (tail p) =
          monomial (- 1) (term_of_pair (lcs t1 t2, component_of_term (lt q))) - monom_mult (- (1 / lc p)) (lcs t1 t2 - t1) p"
      apply (simp add: t1_def t2_def monom_mult_dist_right_minus tail_alt_2 monom_mult_uminus_left)
      by (metis assms(2) eq2 monom_mult_uminus_left t1_def t2_def)
  qed
qed

corollary lcs_red_single_snd_crit_pair:
  assumes "q ≠ 0" and "component_of_term (lt p) = component_of_term (lt q)"
  defines "t1 ≡ lp p"
  defines "t2 ≡ lp q"
  shows "red_single (monomial (- 1) (term_of_pair (lcs t1 t2, component_of_term (lt p))))
                    (snd (crit_pair p q)) q (lcs t1 t2 - t2)"
  by (simp add: crit_pair_swap[of p q] lcs_comm[of "lp p"] assms(2) t1_def t2_def,
        rule lcs_red_single_fst_crit_pair, simp_all add: assms(1, 2))

lemma GB_imp_crit_pair_cbelow_dgrad_p_set:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m" and "is_Groebner_basis F"
  assumes "p ∈ F" and "q ∈ F" and "p ≠ 0" and "q ≠ 0"
  shows "crit_pair_cbelow_on d m F p q"
proof (cases "component_of_term (lt p) = component_of_term (lt q)")
  case True
  from assms(1, 2) show ?thesis
  proof (rule crit_pair_cs_imp_crit_pair_cbelow_on)
    from assms(4, 2) show "p ∈ dgrad_p_set d m" ..
  next
    from assms(5, 2) show "q ∈ dgrad_p_set d m" ..
  next
    let ?cp = "crit_pair p q"
    let ?l = "monomial (- 1) (term_of_pair (lcs (lp p) (lp q), component_of_term (lt p)))"
    from assms(4) lcs_red_single_fst_crit_pair[OF assms(6) True] have "red F ?l (fst ?cp)"
      by (rule red_setI)
    hence 1: "(red F)⇧*⇧* ?l (fst ?cp)" ..
    from assms(5) lcs_red_single_snd_crit_pair[OF assms(7) True] have "red F ?l (snd ?cp)"
      by (rule red_setI)
    hence 2: "(red F)⇧*⇧* ?l (snd ?cp)" ..
    from assms(3) have "relation.is_confluent_on (red F) UNIV"
      by (simp only: is_Groebner_basis_def relation.confluence_equiv_ChurchRosser[symmetric]
          relation.is_confluent_def)
    from this 1 2 show "relation.cs (red F) (fst ?cp) (snd ?cp)"
      by (simp add: relation.is_confluent_on_def)
  qed
next
  case False
  thus ?thesis by (rule crit_pair_cbelow_distinct_component)
qed

lemma spoly_alt:
  assumes "p ≠ 0" and "q ≠ 0"
  shows "spoly p q = fst (crit_pair p q) - snd (crit_pair p q)"
proof (cases "component_of_term (lt p) = component_of_term (lt q)")
  case ec: True
  show ?thesis
  proof (rule poly_mapping_eqI, simp only: lookup_minus)
    fix v
    define t1 where "t1 = lp p"
    define t2 where "t2 = lp q"
    let ?l = "lcs t1 t2"
    let ?lv = "term_of_pair (?l, component_of_term (lt p))"
    let ?cp = "crit_pair p q"
    let ?a = "λx. monom_mult (1 / lc p) (?l - t1) x"
    let ?b = "λx. monom_mult (1 / lc q) (?l - t2) x"
    have l_1: "(?l - t1) ⊕ lt p = ?lv" by (simp add: adds_lcs adds_minus splus_def t1_def)
    have l_2: "(?l - t2) ⊕ lt q = ?lv" by (simp add: ec adds_lcs_2 adds_minus splus_def t2_def)
    show "lookup (spoly p q) v = lookup (fst ?cp) v - lookup (snd ?cp) v"
    proof (cases "v = ?lv")
      case True
      have v_1: "v = (?l - t1) ⊕ lt p" by (simp add: True l_1)
      from ‹p ≠ 0› have "lt p ∈ keys p" by (rule lt_in_keys)
      hence v_2: "v = (?l - t2) ⊕ lt q" by (simp add: True l_2)
      from ‹q ≠ 0› have "lt q ∈ keys q" by (rule lt_in_keys)
      from ‹lt p ∈ keys p› have "lookup (?a p) v = 1"
        by (simp add: in_keys_iff v_1 lookup_monom_mult lc_def term_simps)
      also from ‹lt q ∈ keys q› have "... = lookup (?b q) v"
        by (simp add: in_keys_iff v_2 lookup_monom_mult lc_def term_simps)
      finally have "lookup (spoly p q) v = 0"
        by (simp add: spoly_def ec Let_def t1_def t2_def lookup_minus lc_def)
      moreover have "lookup (fst ?cp) v = 0"
        by (simp add: crit_pair_def ec v_1 lookup_monom_mult t1_def t2_def term_simps,
            simp only: not_in_keys_iff_lookup_eq_zero[symmetric] keys_tail, simp)
      moreover have "lookup (snd ?cp) v = 0"
        by (simp add: crit_pair_def ec v_2 lookup_monom_mult t1_def t2_def term_simps,
            simp only: not_in_keys_iff_lookup_eq_zero[symmetric] keys_tail, simp)
      ultimately show ?thesis by simp
    next
      case False
      have "lookup (?a (tail p)) v = lookup (?a p) v"
      proof (cases "?l - t1 adds⇩p v")
        case True
        then obtain u where v: "v = (?l - t1) ⊕ u" ..
        have "u ≠ lt p"
        proof
          assume "u = lt p"
          hence "v = ?lv" by (simp add: v l_1)
          with ‹v ≠ ?lv› show False ..
        qed
        thus ?thesis by (simp add: v lookup_monom_mult lookup_tail_2 term_simps)
      next
        case False
        thus ?thesis by (simp add: lookup_monom_mult)
      qed
      moreover have "lookup (?b (tail q)) v = lookup (?b q) v"
      proof (cases "?l - t2 adds⇩p v")
        case True
        then obtain u where v: "v = (?l - t2) ⊕ u" ..
        have "u ≠ lt q"
        proof
          assume "u = lt q"
          hence "v = ?lv" by (simp add: v l_2)
          with ‹v ≠ ?lv› show False ..
        qed
        thus ?thesis by (simp add: v lookup_monom_mult lookup_tail_2 term_simps)
      next
        case False
        thus ?thesis by (simp add: lookup_monom_mult)
      qed
      ultimately show ?thesis
        by (simp add: ec spoly_def crit_pair_def lookup_minus t1_def t2_def Let_def lc_def)
    qed
  qed
next
  case False
  show ?thesis by (simp add: spoly_def crit_pair_def False)
qed

lemma spoly_same: "spoly p p = 0"
  by (simp add: spoly_def)

lemma spoly_swap: "spoly p q = - spoly q p"
  by (simp add: spoly_def lcs_comm Let_def)

lemma spoly_red_zero_imp_crit_pair_cbelow_on:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m" and "p ∈ dgrad_p_set d m"
    and "q ∈ dgrad_p_set d m" and "p ≠ 0" and "q ≠ 0" and "(red F)⇧*⇧* (spoly p q) 0"
  shows "crit_pair_cbelow_on d m F p q"
proof -
  from assms(7) have "relation.cs (red F) (fst (crit_pair p q)) (snd (crit_pair p q))"
    unfolding spoly_alt[OF assms(5) assms(6)] by (rule red_diff_rtrancl_cs)
  with assms(1) assms(2) assms(3) assms(4) show ?thesis by (rule crit_pair_cs_imp_crit_pair_cbelow_on)
qed

lemma dgrad_p_set_le_spoly_zero: "dgrad_p_set_le d {spoly p 0} {p}"
proof (simp add: term_simps spoly_def lt_def[of 0] lcs_comm lcs_zero dgrad_p_set_le_def Keys_insert
      Let_def min_term_def lc_def[symmetric], intro conjI impI dgrad_set_leI)
  fix s
  assume "s ∈ pp_of_term ` keys (monom_mult (1 / lc p) 0 p)"
  then obtain u where "u ∈ keys (monom_mult (1 / lc p) 0 p)" and "s = pp_of_term u" ..
  from this(1) keys_monom_mult_subset have "u ∈ (⊕) 0 ` keys p" ..
  hence "u ∈ keys p" by (simp add: image_iff term_simps)
  hence "s ∈ pp_of_term ` keys p" by (simp add: ‹s = pp_of_term u›)
  moreover have "d s ≤ d s" ..
  ultimately show "∃t∈pp_of_term ` keys p. d s ≤ d t" ..
qed simp

lemma dgrad_p_set_le_spoly:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d {spoly p q} {p, q}"
proof (cases "p = 0")
  case True
  have "dgrad_p_set_le d {spoly p q} {spoly q 0}" unfolding True spoly_swap[of 0 q]
    by (fact dgrad_p_set_le_uminus)
  also have "dgrad_p_set_le d ... {q}" by (fact dgrad_p_set_le_spoly_zero)
  also have "dgrad_p_set_le d ... {p, q}" by (rule dgrad_p_set_le_subset, simp)
  finally show ?thesis .
next
  case False
  show ?thesis
  proof (cases "q = 0")
    case True
    have "dgrad_p_set_le d {spoly p q} {p}" unfolding True by (fact dgrad_p_set_le_spoly_zero)
    also have "dgrad_p_set_le d ... {p, q}" by (rule dgrad_p_set_le_subset, simp)
    finally show ?thesis .
  next
    case False
    have "dgrad_p_set_le d {spoly p q} {fst (crit_pair p q), snd (crit_pair p q)}"
      unfolding spoly_alt[OF ‹p ≠ 0› False] by (rule dgrad_p_set_le_minus)
    also have "dgrad_p_set_le d ... {p, q}"
    proof (rule dgrad_p_set_leI_insert)
      from assms show "dgrad_p_set_le d {fst (crit_pair p q)} {p, q}"
        by (rule dgrad_p_set_le_fst_crit_pair)
    next
      from assms show "dgrad_p_set_le d {snd (crit_pair p q)} {p, q}"
        by (rule dgrad_p_set_le_snd_crit_pair)
    qed
    finally show ?thesis .
  qed
qed

lemma dgrad_p_set_closed_spoly:
  assumes "dickson_grading d" and "p ∈ dgrad_p_set d m" and "q ∈ dgrad_p_set d m"
  shows "spoly p q ∈ dgrad_p_set d m"
proof -
  from dgrad_p_set_le_spoly[OF assms(1)] have "{spoly p q} ⊆ dgrad_p_set d m"
  proof (rule dgrad_p_set_le_dgrad_p_set)
    from assms(2, 3) show "{p, q} ⊆ dgrad_p_set d m" by simp
  qed
  thus ?thesis by simp
qed

lemma components_spoly_subset: "component_of_term ` keys (spoly p q) ⊆ component_of_term ` Keys {p, q}"
  unfolding spoly_def Let_def
proof (split if_split, intro conjI impI)
  define c where "c = (1 / lookup p (lt p))"
  define d where "d = (1 / lookup q (lt q))"
  define s where "s = lcs (lp p) (lp q) - lp p"
  define t where "t = lcs (lp p) (lp q) - lp q"
  show "component_of_term ` keys (monom_mult c s p - monom_mult d t q) ⊆ component_of_term ` Keys {p, q}"
  proof
    fix k
    assume "k ∈ component_of_term ` keys (monom_mult c s p - monom_mult d t q)"
    then obtain v where "v ∈ keys (monom_mult c s p - monom_mult d t q)" and k: "k = component_of_term v" ..
    from this(1) keys_minus have "v ∈ keys (monom_mult c s p) ∪ keys (monom_mult d t q)" ..
    thus "k ∈ component_of_term ` Keys {p, q}"
    proof
      assume "v ∈ keys (monom_mult c s p)"
      from this keys_monom_mult_subset have "v ∈ (⊕) s ` keys p" ..
      then obtain u where "u ∈ keys p" and v: "v = s ⊕ u" ..
      have "u ∈ Keys {p, q}" by (rule in_KeysI, fact, simp)
      moreover have "k = component_of_term u" by (simp add: v k term_simps)
      ultimately show ?thesis by simp
    next
      assume "v ∈ keys (monom_mult d t q)"
      from this keys_monom_mult_subset have "v ∈ (⊕) t ` keys q" ..
      then obtain u where "u ∈ keys q" and v: "v = t ⊕ u" ..
      have "u ∈ Keys {p, q}" by (rule in_KeysI, fact, simp)
      moreover have "k = component_of_term u" by (simp add: v k term_simps)
      ultimately show ?thesis by simp
    qed
  qed
qed simp

lemma pmdl_closed_spoly:
  assumes "p ∈ pmdl F" and "q ∈ pmdl F"
  shows "spoly p q ∈ pmdl F"
proof (cases "component_of_term (lt p) = component_of_term (lt q)")
  case True
  show ?thesis
    by (simp add: spoly_def True Let_def, rule pmdl.span_diff,
        (rule pmdl_closed_monom_mult, fact)+)
next
  case False
  show ?thesis by (simp add: spoly_def False pmdl.span_zero)
qed

subsection ‹Buchberger's Theorem›

text ‹Before proving the main theorem of Gr\"obner bases theory for S-polynomials, as is usually done
  in textbooks, we first prove it for critical pairs: a set ‹F› yields a confluent reduction
  relation if the critical pairs of all ‹p ∈ F› and ‹q ∈ F› can be connected below
  the least common sum of the leading power-products of ‹p› and ‹q›.
  The reason why we proceed in this way is that it becomes much easier to prove the correctness of
  Buchberger's second criterion for avoiding useless pairs.›

lemma crit_pair_cbelow_imp_confluent_dgrad_p_set:
  assumes dg: "dickson_grading d" and "F ⊆ dgrad_p_set d m"
  assumes main: "⋀p q. p ∈ F ⟹ q ∈ F ⟹ p ≠ 0 ⟹ q ≠ 0 ⟹ crit_pair_cbelow_on d m F p q"
  shows "relation.is_confluent_on (red F) (dgrad_p_set d m)"
proof -
  let ?A = "dgrad_p_set d m"
  let ?R = "red F"
  let ?RS = "λa b. red F a b ∨ red F b a"
  let ?ord = "(≺⇩p)"
  from dg have ro: "Confluence.relation_order ?R ?ord ?A"
    by (rule is_relation_order_red)
  have dw: "relation.dw_closed ?R ?A"
    by (rule relation.dw_closedI, rule dgrad_p_set_closed_red, rule dg, rule assms(2))
  show ?thesis
  proof (rule relation_order.loc_connectivity_implies_confluence, fact ro)
    show "is_loc_connective_on ?A ?ord ?R" unfolding is_loc_connective_on_def
    proof (intro ballI allI impI)
      fix a b1 b2 :: "'t ⇒⇩0 'b"
      assume "a ∈ ?A"
      assume "?R a b1 ∧ ?R a b2"
      hence "?R a b1" and "?R a b2" by simp_all
      hence "b1 ∈ ?A" and "b2 ∈ ?A" and "?ord b1 a" and "?ord b2 a"
        using red_ord dgrad_p_set_closed_red[OF dg assms(2) ‹a ∈ ?A›] by blast+
      from this(1) this(2) have "b1 - b2 ∈ ?A" by (rule dgrad_p_set_closed_minus)
      from ‹red F a b1› obtain f1 and t1 where "f1 ∈ F" and r1: "red_single a b1 f1 t1" by (rule red_setE)
      from ‹red F a b2› obtain f2 and t2 where "f2 ∈ F" and r2: "red_single a b2 f2 t2" by (rule red_setE)
      from r1 r2 have "f1 ≠ 0" and "f2 ≠ 0" by (simp_all add: red_single_def)
      hence lc1: "lc f1 ≠ 0" and lc2: "lc f2 ≠ 0" using lc_not_0 by auto
      show "cbelow_on ?A ?ord a (λa b. ?R a b ∨ ?R b a) b1 b2"
      proof (cases "t1 ⊕ lt f1 = t2 ⊕ lt f2")
        case False
        from confluent_distinct[OF r1 r2 False ‹f1 ∈ F› ‹f2 ∈ F›] obtain s
          where s1: "(red F)⇧*⇧* b1 s" and s2: "(red F)⇧*⇧* b2 s" .
        have "relation.cs ?R b1 b2" unfolding relation.cs_def by (intro exI conjI, fact s1, fact s2)
        from ro dw this ‹b1 ∈ ?A› ‹b2 ∈ ?A› ‹?ord b1 a› ‹?ord b2 a› show ?thesis
          by (rule relation_order.cs_implies_cbelow_on)
      next
        case True
        hence ec: "component_of_term (lt f1) = component_of_term (lt f2)"
          by (metis component_of_term_splus)
        let ?l1 = "lp f1"
        let ?l2 = "lp f2"
        define v where "v ≡ t2 ⊕ lt f2"
        define l where "l ≡ lcs ?l1 ?l2"
        define a' where "a' = except a {v}"
        define ma where "ma = monomial (lookup a v) v"
        have v_alt: "v = t1 ⊕ lt f1" by (simp only: True v_def)
        have "a = ma + a'" unfolding ma_def a'_def by (fact plus_except)
        have comp_f1: "component_of_term (lt f1) = component_of_term v" by (simp add: v_alt term_simps)

        have "?l1 adds l" unfolding l_def by (rule adds_lcs)
        have "?l2 adds l" unfolding l_def by (rule adds_lcs_2)
        have "?l1 adds⇩p (t1 ⊕ lt f1)" by (simp add: adds_pp_splus term_simps)
        hence "?l1 adds⇩p v" by (simp add: v_alt)
        have "?l2 adds⇩p v" by (simp add: v_def adds_pp_splus term_simps)
        from ‹?l1 adds⇩p v› ‹?l2 adds⇩p v› have "l adds⇩p v" by (simp add: l_def adds_pp_def lcs_adds)
        have "pp_of_term (v ⊖ ?l1) = t1" by (simp add: v_alt term_simps)
        with ‹l adds⇩p v› ‹?l1 adds l› have tf1': "pp_of_term ((l - ?l1) ⊕ (v ⊖ l)) = t1"
          by (simp add: minus_splus_sminus_cancel)
        hence tf1: "((pp_of_term v) - l) + (l - ?l1) = t1" by (simp add: add.commute term_simps)
        have "pp_of_term (v ⊖ ?l2) = t2" by (simp add: v_def term_simps)
        with ‹l adds⇩p v› ‹?l2 adds l› have tf2': "pp_of_term ((l - ?l2) ⊕ (v ⊖ l)) = t2"
          by (simp add: minus_splus_sminus_cancel)
        hence tf2: "((pp_of_term v) - l) + (l - ?l2) = t2" by (simp add: add.commute term_simps)
        let ?ca = "lookup a v"
        let ?v = "pp_of_term v - l"
        have "?v + l = pp_of_term v" using ‹l adds⇩p v› adds_minus adds_pp_def by blast
        from tf1' have "?v adds t1" unfolding pp_of_term_splus add.commute[of "l - ?l1"] pp_of_term_sminus
          using addsI by blast
        with dg have "d ?v ≤ d t1" by (rule dickson_grading_adds_imp_le)
        also from dg ‹a ∈ ?A› r1 have "... ≤ m" by (rule dgrad_p_set_red_single_pp)
        finally have "d ?v ≤ m" .
        from r2 have "?ca ≠ 0" by (simp add: red_single_def v_def)
        hence "- ?ca ≠ 0" by simp

        (* b1 *)
        from r1 have "b1 = a - monom_mult (?ca / lc f1) t1 f1" by (simp add: red_single_def v_alt)
        also have "... = monom_mult (- ?ca) ?v (fst (crit_pair f1 f2)) + a'"
        proof (simp add: a'_def ec crit_pair_def l_def[symmetric] monom_mult_assoc tf1,
              rule poly_mapping_eqI, simp add: lookup_add lookup_minus)
          fix u
          show "lookup a u - lookup (monom_mult (?ca / lc f1) t1 f1) u =
                lookup (monom_mult (- (?ca / lc f1)) t1 (tail f1)) u + lookup (except a {v}) u"
          proof (cases "u = v")
            case True
            show ?thesis
              by (simp add: True lookup_except v_alt lookup_monom_mult lookup_tail_2 lc_def[symmetric] lc1 term_simps)
          next
            case False
            hence "u ∉ {v}" by simp
            moreover
            {
              assume "t1 adds⇩p u"
              hence "t1 ⊕ (u ⊖ t1) = u" by (simp add: adds_pp_sminus)
              hence "u ⊖ t1 ≠ lt f1" using False v_alt by auto
              hence "lookup f1 (u ⊖ t1) = lookup (tail f1) (u ⊖ t1)" by (simp add: lookup_tail_2)
            }
            ultimately show ?thesis using False by (simp add: lookup_except lookup_monom_mult)
          qed
        qed
        finally have b1: "b1 = monom_mult (- ?ca) ?v (fst (crit_pair f1 f2)) + a'" .

        (* b2 *)
        from r2 have "b2 = a - monom_mult (?ca / lc f2) t2 f2"
          by (simp add: red_single_def v_def True)
        also have "... = monom_mult (- ?ca) ?v (snd (crit_pair f1 f2)) + a'"
        proof (simp add: a'_def ec crit_pair_def l_def[symmetric] monom_mult_assoc tf2,
              rule poly_mapping_eqI, simp add: lookup_add lookup_minus)
          fix u
          show "lookup a u - lookup (monom_mult (?ca / lc f2) t2 f2) u =
                lookup (monom_mult (- (?ca / lc f2)) t2 (tail f2)) u + lookup (except a {v}) u"
          proof (cases "u = v")
            case True
            show ?thesis
              by (simp add: True lookup_except v_def lookup_monom_mult lookup_tail_2 lc_def[symmetric] lc2 term_simps)
          next
            case False
            hence "u ∉ {v}" by simp
            moreover
            {
              assume "t2 adds⇩p u"
              hence "t2 ⊕ (u ⊖ t2) = u" by (simp add: adds_pp_sminus)
              hence "u ⊖ t2 ≠ lt f2" using False v_def by auto
              hence "lookup f2 (u ⊖ t2) = lookup (tail f2) (u ⊖ t2)" by (simp add: lookup_tail_2)
            }
            ultimately show ?thesis using False by (simp add: lookup_except lookup_monom_mult)
          qed
        qed
        finally have b2: "b2 = monom_mult (- ?ca) ?v (snd (crit_pair f1 f2)) + a'" .

        let ?lv = "term_of_pair (l, component_of_term (lt f1))"
        from ‹f1 ∈ F› ‹f2 ∈ F› ‹f1 ≠ 0› ‹f2 ≠ 0› have "crit_pair_cbelow_on d m F f1 f2" by (rule main)
        hence "cbelow_on ?A ?ord (monomial 1 ?lv) ?RS (fst (crit_pair f1 f2)) (snd (crit_pair f1 f2))"
          by (simp only: crit_pair_cbelow_on_def l_def)
        with dg assms (2) ‹d ?v ≤ m› ‹- ?ca ≠ 0›
        have "cbelow_on ?A ?ord (monom_mult (- ?ca) ?v (monomial 1 ?lv)) ?RS
              (monom_mult (- ?ca) ?v (fst (crit_pair f1 f2)))
              (monom_mult (- ?ca) ?v (snd (crit_pair f1 f2)))"
          by (rule cbelow_on_monom_mult)
        hence "cbelow_on ?A ?ord (monomial (- ?ca) v) ?RS
              (monom_mult (- ?ca) ?v (fst (crit_pair f1 f2)))
              (monom_mult (- ?ca) ?v (snd (crit_pair f1 f2)))"
          by (simp add: monom_mult_monomial ‹(pp_of_term v - l) + l = pp_of_term v› splus_def comp_f1 term_simps)
        with ‹?ca ≠ 0› have "cbelow_on ?A ?ord (monomial ?ca (0 ⊕ v)) ?RS
              (monom_mult (-?ca) ?v (fst (crit_pair f1 f2))) (monom_mult (-?ca) ?v (snd (crit_pair f1 f2)))"
          by (rule cbelow_on_monom_mult_monomial)
        hence "cbelow_on ?A ?ord ma ?RS
              (monom_mult (-?ca) ?v (fst (crit_pair f1 f2))) (monom_mult (-?ca) ?v (snd (crit_pair f1 f2)))"
          by (simp add: ma_def term_simps)
        with dg assms(2) _ _
        show "cbelow_on ?A ?ord a ?RS b1 b2" unfolding ‹a = ma + a'› b1 b2
        proof (rule cbelow_on_plus)
          show "a' ∈ ?A"
            by (rule, simp add: a'_def keys_except, erule conjE, intro dgrad_p_setD,
                rule ‹a ∈ dgrad_p_set d m›)
        next
          show "keys a' ∩ keys ma = {}" by (simp add: ma_def a'_def keys_except)
        qed
      qed
    qed
  qed fact
qed

corollary crit_pair_cbelow_imp_GB_dgrad_p_set:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m"
  assumes "⋀p q. p ∈ F ⟹ q ∈ F ⟹ p ≠ 0 ⟹ q ≠ 0 ⟹ crit_pair_cbelow_on d m F p q"
  shows "is_Groebner_basis F"
  unfolding is_Groebner_basis_def
proof (rule relation.confluence_implies_ChurchRosser,
      simp only: relation.is_confluent_def relation.is_confluent_on_def, intro ballI allI impI)
  fix a b1 b2
  assume a: "(red F)⇧*⇧* a b1 ∧ (red F)⇧*⇧* a b2"
  from assms(2) obtain n where "m ≤ n" and "a ∈ dgrad_p_set d n" and "F ⊆ dgrad_p_set d n"
    by (rule dgrad_p_set_insert)
  {
    fix p q
    assume "p ∈ F" and "q ∈ F" and "p ≠ 0" and "q ≠ 0"
    hence "crit_pair_cbelow_on d m F p q" by (rule assms(3))
    from this dgrad_p_set_subset[OF ‹m ≤ n›] have "crit_pair_cbelow_on d n F p q"
      unfolding crit_pair_cbelow_on_def by (rule cbelow_on_mono)
  }
  with assms(1) ‹F ⊆ dgrad_p_set d n› have "relation.is_confluent_on (red F) (dgrad_p_set d n)"
    by (rule crit_pair_cbelow_imp_confluent_dgrad_p_set)
  from this ‹a ∈ dgrad_p_set d n› have "∀b1 b2. (red F)⇧*⇧* a b1 ∧ (red F)⇧*⇧* a b2 ⟶ relation.cs (red F) b1 b2"
    unfolding relation.is_confluent_on_def ..
  with a show "relation.cs (red F) b1 b2" by blast
qed

corollary Buchberger_criterion_dgrad_p_set:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m"
  assumes "⋀p q. p ∈ F ⟹ q ∈ F ⟹ p ≠ 0 ⟹ q ≠ 0 ⟹ p ≠ q ⟹
                      component_of_term (lt p) = component_of_term (lt q) ⟹ (red F)⇧*⇧* (spoly p q) 0"
  shows "is_Groebner_basis F"
  using assms(1) assms(2)
proof (rule crit_pair_cbelow_imp_GB_dgrad_p_set)
  fix p q
  assume "p ∈ F" and "q ∈ F" and "p ≠ 0" and "q ≠ 0"
  from this(1, 2) assms(2) have p: "p ∈ dgrad_p_set d m" and q: "q ∈ dgrad_p_set d m" by auto
  show "crit_pair_cbelow_on d m F p q"
  proof (cases "p = q")
    case True
    from assms(1) q show ?thesis unfolding True by (rule crit_pair_cbelow_same)
  next
    case False
    show ?thesis
    proof (cases "component_of_term (lt p) = component_of_term (lt q)")
      case True
      from assms(1) assms(2) p q ‹p ≠ 0› ‹q ≠ 0› show "crit_pair_cbelow_on d m F p q"
      proof (rule spoly_red_zero_imp_crit_pair_cbelow_on)
        from ‹p ∈ F› ‹q ∈ F› ‹p ≠ 0› ‹q ≠ 0› ‹p ≠ q› True show "(red F)⇧*⇧* (spoly p q) 0"
          by (rule assms(3))
      qed
    next
      case False
      thus ?thesis by (rule crit_pair_cbelow_distinct_component)
    qed
  qed
qed

lemmas Buchberger_criterion_finite = Buchberger_criterion_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]

lemma (in ordered_term) GB_imp_zero_reducibility:
  assumes "is_Groebner_basis G" and "f ∈ pmdl G"
  shows "(red G)⇧*⇧* f 0"
proof -
  from in_pmdl_srtc[OF ‹f ∈ pmdl G›] ‹is_Groebner_basis G› have "relation.cs (red G) f 0"
    unfolding is_Groebner_basis_def relation.is_ChurchRosser_def by simp
  then obtain s where rfs: "(red G)⇧*⇧* f s" and r0s: "(red G)⇧*⇧* 0 s" unfolding relation.cs_def by auto
  from rtrancl_0[OF r0s] and rfs show ?thesis by simp
qed

lemma (in ordered_term) GB_imp_reducibility:
  assumes "is_Groebner_basis G" and "f ≠ 0" and "f ∈ pmdl G"
  shows "is_red G f"
  using assms by (meson GB_imp_zero_reducibility is_red_def relation.rtrancl_is_final)

lemma is_Groebner_basis_empty: "is_Groebner_basis {}"
  by (rule Buchberger_criterion_finite, rule, simp)

lemma is_Groebner_basis_singleton: "is_Groebner_basis {f}"
  by (rule Buchberger_criterion_finite, simp, simp add: spoly_same)

subsection ‹Buchberger's Criteria for Avoiding Useless Pairs›

text ‹Unfortunately, the product criterion is only applicable to scalar polynomials.›
lemma (in gd_powerprod) product_criterion:
  assumes "dickson_grading d" and "F ⊆ punit.dgrad_p_set d m" and "p ∈ F" and "q ∈ F"
    and "p ≠ 0" and "q ≠ 0" and "gcs (punit.lt p) (punit.lt q) = 0"
  shows "punit.crit_pair_cbelow_on d m F p q"
proof -
  let ?lt = "punit.lt p"
  let ?lq = "punit.lt q"
  let ?l = "lcs ?lt ?lq"
  define s where "s = punit.monom_mult (- 1 / (punit.lc p * punit.lc q)) 0 (punit.tail p * punit.tail q)"
  from assms(7) have "?l = ?lt + ?lq" by (metis add_cancel_left_left gcs_plus_lcs)
  hence "?l - ?lt = ?lq" and "?l - ?lq = ?lt" by simp_all

  have "(punit.red {q})⇧*⇧* (punit.tail p * (monomial (1 / punit.lc p) (punit.lt q)))
        (punit.monom_mult (- (1 / punit.lc p) / punit.lc q) 0 (punit.tail p * punit.tail q))"
    unfolding punit_mult_scalar[symmetric] using ‹q ≠ 0› by (rule punit.red_mult_scalar_lt)
  moreover have "punit.monom_mult (1 / punit.lc p) (punit.lt q) (punit.tail p) =
                  punit.tail p * (monomial (1 / punit.lc p) (punit.lt q))"
    by (simp add: times_monomial_left[symmetric])
  ultimately have "(punit.red {q})⇧*⇧* (fst (punit.crit_pair p q)) s"
    by (simp add: punit.crit_pair_def ‹?l - ?lt = ?lq› s_def)
  moreover from ‹q ∈ F› have "{q} ⊆ F" by simp
  ultimately have 1: "(punit.red F)⇧*⇧* (fst (punit.crit_pair p q)) s" by (rule punit.red_rtrancl_subset)

  have "(punit.red {p})⇧*⇧* (punit.tail q * (monomial (1 / punit.lc q) (punit.lt p)))
        (punit.monom_mult (- (1 / punit.lc q) / punit.lc p) 0 (punit.tail q * punit.tail p))"
    unfolding punit_mult_scalar[symmetric] using ‹p ≠ 0› by (rule punit.red_mult_scalar_lt)
  hence "(punit.red {p})⇧*⇧* (snd (punit.crit_pair p q)) s"
    by (simp add: punit.crit_pair_def ‹?l - ?lq = ?lt› s_def mult.commute flip: times_monomial_left)
  moreover from ‹p ∈ F› have "{p} ⊆ F" by simp
  ultimately have 2: "(punit.red F)⇧*⇧* (snd (punit.crit_pair p q)) s" by (rule punit.red_rtrancl_subset)

  note assms(1) assms(2)
  moreover from ‹p ∈ F› ‹F ⊆ punit.dgrad_p_set d m› have "p ∈ punit.dgrad_p_set d m" ..
  moreover from ‹q ∈ F› ‹F ⊆ punit.dgrad_p_set d m› have "q ∈ punit.dgrad_p_set d m" ..
  moreover from 1 2 have "relation.cs (punit.red F) (fst (punit.crit_pair p q)) (snd (punit.crit_pair p q))"
    unfolding relation.cs_def by blast
  ultimately show ?thesis by (rule punit.crit_pair_cs_imp_crit_pair_cbelow_on)
qed

lemma chain_criterion:
  assumes "dickson_grading d" and "F ⊆ dgrad_p_set d m" and "p ∈ F" and "q ∈ F"
    and "p ≠ 0" and "q ≠ 0" and "lp r adds lcs (lp p) (lp q)"
    and "component_of_term (lt r) = component_of_term (lt p)"
    and pr: "crit_pair_cbelow_on d m F p r" and rq: "crit_pair_cbelow_on d m F r q"
  shows "crit_pair_cbelow_on d m F p q"
proof (cases "component_of_term (lt p) = component_of_term (lt q)")
  case True
  with assms(8) have comp_r: "component_of_term (lt r) = component_of_term (lt q)" by simp
  let ?A = "dgrad_p_set d m"
  let ?RS = "λa b. red F a b ∨ red F b a"
  let ?lt = "lp p"
  let ?lq = "lp q"
  let ?lr = "lp r"
  let ?ltr = "lcs ?lt ?lr"
  let ?lrq = "lcs ?lr ?lq"
  let ?ltq = "lcs ?lt ?lq"

  from ‹p ∈ F› ‹F ⊆ dgrad_p_set d m› have "p ∈ dgrad_p_set d m" ..
  from this ‹p ≠ 0› have "d ?lt ≤ m" by (rule dgrad_p_setD_lp)
  from ‹q ∈ F› ‹F ⊆ dgrad_p_set d m› have "q ∈ dgrad_p_set d m" ..
  from this ‹q ≠ 0› have "d ?lq ≤ m" by (rule dgrad_p_setD_lp)
  from assms(1) have "d ?ltq ≤ ord_class.max (d ?lt) (d ?lq)" by (rule dickson_grading_lcs)
  also from ‹d ?lt ≤ m› ‹d ?lq ≤ m› have "... ≤ m" by simp
  finally have "d ?ltq ≤ m" .

  from adds_lcs ‹?lr adds ?ltq› have "?ltr adds ?ltq" by (rule lcs_adds)
  then obtain up where "?ltq = ?ltr + up" ..
  hence up1: "?ltq - ?lt = up + (?ltr - ?lt)" and up2: "up + (?ltr - ?lr) = ?ltq - ?lr"
    by (metis add.commute adds_lcs minus_plus, metis add.commute adds_lcs_2 minus_plus)
  have fst_pq: "fst (crit_pair p q) = monom_mult 1 up (fst (crit_pair p r))"
    by (simp add: crit_pair_def monom_mult_assoc up1 True comp_r)
  from assms(1) assms(2) _ _ pr
  have "cbelow_on ?A (≺⇩p) (monom_mult 1 up (monomial 1 (term_of_pair (?ltr, component_of_term (lt p))))) ?RS
                  (fst (crit_pair p q)) (monom_mult 1 up (snd (crit_pair p r)))"
    unfolding fst_pq crit_pair_cbelow_on_def
  proof (rule cbelow_on_monom_mult)
    from ‹d ?ltq ≤ m› show "d up ≤ m" by (simp add: ‹?ltq = ?ltr + up› dickson_gradingD1[OF assms(1)])
  qed simp
  hence 1: "cbelow_on ?A (≺⇩p) (monomial 1 (term_of_pair (?ltq, component_of_term (lt p)))) ?RS
                      (fst (crit_pair p q)) (monom_mult 1 up (snd (crit_pair p r)))"
    by (simp add: monom_mult_monomial ‹?ltq = ?ltr + up› add.commute splus_def term_simps)

  from ‹?lr adds ?ltq› adds_lcs_2 have "?lrq adds ?ltq" by (rule lcs_adds)
  then obtain uq where "?ltq = ?lrq + uq" ..
  hence uq1: "?ltq - ?lq = uq + (?lrq - ?lq)" and uq2: "uq + (?lrq - ?lr) = ?ltq - ?lr"
   by (metis add.commute adds_lcs_2 minus_plus, metis add.commute adds_lcs minus_plus)
  have eq: "monom_mult 1 uq (fst (crit_pair r q)) = monom_mult 1 up (snd (crit_pair p r))"
    by (simp add: crit_pair_def monom_mult_assoc up2 uq2 True comp_r)
  have snd_pq: "snd (crit_pair p q) = monom_mult 1 uq (snd (crit_pair r q))"
    by (simp add: crit_pair_def monom_mult_assoc uq1 True comp_r)
  from assms(1) assms(2) _ _ rq
  have "cbelow_on ?A (≺⇩p) (monom_mult 1 uq (monomial 1 (term_of_pair (?lrq, component_of_term (lt p))))) ?RS
                  (monom_mult 1 uq (fst (crit_pair r q))) (snd (crit_pair p q))"
    unfolding snd_pq crit_pair_cbelow_on_def assms(8)
  proof (rule cbelow_on_monom_mult)
    from ‹d ?ltq ≤ m› show "d uq ≤ m" by (simp add: ‹?ltq = ?lrq + uq› dickson_gradingD1[OF assms(1)])
  qed simp
  hence "cbelow_on ?A (≺⇩p) (monomial 1 (term_of_pair (?ltq, component_of_term (lt p)))) ?RS
                   (monom_mult 1 uq (fst (crit_pair r q))) (snd (crit_pair p q))"
    by (simp add: monom_mult_monomial ‹?ltq = ?lrq + uq› add.commute splus_def term_simps)
  hence "cbelow_on ?A (≺⇩p) (monomial 1 (term_of_pair (?ltq, component_of_term (lt p)))) ?RS
                   (monom_mult 1 up (snd (crit_pair p r))) (snd (crit_pair p q))"
    by (simp only: eq)
  
  with 1 show ?thesis unfolding crit_pair_cbelow_on_def by (rule cbelow_on_transitive)
next
  case False
  thus ?thesis by (rule crit_pair_cbelow_distinct_component)
qed

subsection ‹Weak and Strong Gr\"obner Bases›

lemma ord_p_wf_on:
  assumes "dickson_grading d"
  shows "wfp_on (≺⇩p) (dgrad_p_set d m)"
proof (rule wfp_onI_min)
  fix x::"'t ⇒⇩0 'b" and Q
  assume "x ∈ Q" and "Q ⊆ dgrad_p_set d m"
  with assms obtain z where "z ∈ Q" and *: "⋀y. y ≺⇩p z ⟹ y ∉ Q"
    by (rule ord_p_minimum_dgrad_p_set, blast)
  from this(1) show "∃z∈Q. ∀y∈dgrad_p_set d m. y ≺⇩p z ⟶ y ∉ Q"
  proof
    show "∀y∈dgrad_p_set d m. y ≺⇩p z ⟶ y ∉ Q" by (intro ballI impI *)
  qed
qed

(* TODO: Collect all "_dgrad_p_set"-facts in a locale? *)
lemma is_red_implies_0_red_dgrad_p_set:
  assumes "dickson_grading d" and "B ⊆ dgrad_p_set d m"
  assumes "pmdl B ⊆ pmdl A" and "⋀q. q ∈ pmdl A ⟹ q ∈ dgrad_p_set d m ⟹ q ≠ 0 ⟹ is_red B q"
    and "p ∈ pmdl A" and "p ∈ dgrad_p_set d m"
  shows "(red B)⇧*⇧* p 0"
proof -
  from ord_p_wf_on[OF assms(1)] assms(6, 5) show ?thesis
  proof (induction p rule: wfp_on_induct)
    case (less p)
    show ?case
    proof (cases "p = 0")
      case True
      thus ?thesis by simp
    next
      case False
      from assms(4)[OF less(3, 1) False] obtain q where redpq: "red B p q" unfolding is_red_alt ..
      with assms(1) assms(2) less(1) have "q ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_red)
      moreover from redpq have "q ≺⇩p p" by (rule red_ord)
      moreover from ‹pmdl B ⊆ pmdl A› ‹p ∈ pmdl A› ‹red B p q› have "q ∈ pmdl A"
        by (rule pmdl_closed_red)
      ultimately have "(red B)⇧*⇧* q 0" by (rule less(2))
      show ?thesis by (rule converse_rtranclp_into_rtranclp, rule redpq, fact)
    qed
  qed
qed

lemma is_red_implies_0_red_dgrad_p_set':
  assumes "dickson_grading d" and "B ⊆ dgrad_p_set d m"
  assumes "pmdl B ⊆ pmdl A" and "⋀q. q ∈ pmdl A ⟹ q ≠ 0 ⟹ is_red B q"
    and "p ∈ pmdl A"
  shows "(red B)⇧*⇧* p 0"
proof -
  from assms(2) obtain n where "m ≤ n" and "p ∈ dgrad_p_set d n" and B: "B ⊆ dgrad_p_set d n"
    by (rule dgrad_p_set_insert)
  from ord_p_wf_on[OF assms(1)] this(2) assms(5) show ?thesis
  proof (induction p rule: wfp_on_induct)
    case (less p)
    show ?case
    proof (cases "p = 0")
      case True
      thus ?thesis by simp
    next
      case False
      from assms(4)[OF ‹p ∈ (pmdl A)› False] obtain q where redpq: "red B p q" unfolding is_red_alt ..
      with assms(1) B ‹p ∈ dgrad_p_set d n› have "q ∈ dgrad_p_set d n" by (rule dgrad_p_set_closed_red)
      moreover from redpq have "q ≺⇩p p" by (rule red_ord)
      moreover from ‹pmdl B ⊆ pmdl A› ‹p ∈ pmdl A› ‹red B p q› have "q ∈ pmdl A"
        by (rule pmdl_closed_red)
      ultimately have "(red B)⇧*⇧* q 0" by (rule less(2))
      show ?thesis by (rule converse_rtranclp_into_rtranclp, rule redpq, fact)
    qed
  qed
qed

lemma pmdl_eqI_adds_lt_dgrad_p_set:
  fixes G::"('t ⇒⇩0 'b::field) set"
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m" and "B ⊆ dgrad_p_set d m" and "pmdl G ⊆ pmdl B"
  assumes "⋀f. f ∈ pmdl B ⟹ f ∈ dgrad_p_set d m ⟹ f ≠ 0 ⟹ (∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)"
  shows "pmdl G = pmdl B"
proof
  show "pmdl B ⊆ pmdl G"
  proof (rule pmdl.span_subset_spanI, rule)
    fix p
    assume "p ∈ B"
    hence "p ∈ pmdl B" and "p ∈ dgrad_p_set d m" by (rule pmdl.span_base, rule, intro assms(3))
    with assms(1, 2, 4) _ have "(red G)⇧*⇧* p 0"
    proof (rule is_red_implies_0_red_dgrad_p_set)
      fix f
      assume "f ∈ pmdl B" and "f ∈ dgrad_p_set d m" and "f ≠ 0"
      hence "(∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)" by (rule assms(5))
      then obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by blast
      thus "is_red G f" using ‹f ≠ 0› is_red_indI1 by blast
    qed
    thus "p ∈ pmdl G" by (rule red_rtranclp_0_in_pmdl)
  qed
qed fact

lemma pmdl_eqI_adds_lt_dgrad_p_set':
  fixes G::"('t ⇒⇩0 'b::field) set"
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m" and "pmdl G ⊆ pmdl B"
  assumes "⋀f. f ∈ pmdl B ⟹ f ≠ 0 ⟹ (∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)"
  shows "pmdl G = pmdl B"
proof
  show "pmdl B ⊆ pmdl G"
  proof
    fix p
    assume "p ∈ pmdl B"
    with assms(1, 2, 3) _ have "(red G)⇧*⇧* p 0"
    proof (rule is_red_implies_0_red_dgrad_p_set')
      fix f
      assume "f ∈ pmdl B" and "f ≠ 0"
      hence "(∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)" by (rule assms(4))
      then obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by blast
      thus "is_red G f" using ‹f ≠ 0› is_red_indI1 by blast
    qed
    thus "p ∈ pmdl G" by (rule red_rtranclp_0_in_pmdl)
  qed
qed fact

lemma GB_implies_unique_nf_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G"
  shows "∃! h. (red G)⇧*⇧* f h ∧ ¬ is_red G h"
proof -
  from assms(1) assms(2) have "wfP (red G)¯¯" by (rule red_wf_dgrad_p_set)
  then obtain h where ftoh: "(red G)⇧*⇧* f h" and irredh: "relation.is_final (red G) h"
    by (rule relation.wf_imp_nf_ex)
  show ?thesis
  proof
    from ftoh and irredh show "(red G)⇧*⇧* f h ∧ ¬ is_red G h" by (simp add: is_red_def)
  next
    fix h'
    assume "(red G)⇧*⇧* f h' ∧ ¬ is_red G h'"
    hence ftoh': "(red G)⇧*⇧* f h'" and irredh': "relation.is_final (red G) h'" by (simp_all add: is_red_def)
    show "h' = h"
    proof (rule relation.ChurchRosser_unique_final)
      from isGB show "relation.is_ChurchRosser (red G)" by (simp only: is_Groebner_basis_def)
    qed fact+
  qed
qed

lemma translation_property':
  assumes "p ≠ 0" and red_p_0: "(red F)⇧*⇧* p 0"
  shows "is_red F (p + q) ∨ is_red F q"
proof (rule disjCI)
  assume not_red: "¬ is_red F q"
  from red_p_0 ‹p ≠ 0› obtain f where "f ∈ F" and "f ≠ 0" and lt_adds: "lt f adds⇩t lt p"
    by (rule zero_reducibility_implies_lt_divisibility)
  show "is_red F (p + q)"
  proof (cases "q = 0")
    case True
    with is_red_indI1[OF ‹f ∈ F› ‹f ≠ 0› ‹p ≠ 0› lt_adds] show ?thesis by simp
  next
    case False
    from not_red is_red_addsI[OF ‹f ∈ F› ‹f ≠ 0› _ lt_adds, of q] have "¬ lt p ∈ (keys q)" by blast
    hence "lookup q (lt p) = 0" by (simp add: in_keys_iff)
    with lt_in_keys[OF ‹p ≠ 0›] have "lt p ∈ (keys (p + q))" unfolding in_keys_iff by (simp add: lookup_add)
    from is_red_addsI[OF ‹f ∈ F› ‹f ≠ 0› this lt_adds] show ?thesis .
  qed
qed
  
lemma translation_property:
  assumes "p ≠ q" and red_0: "(red F)⇧*⇧* (p - q) 0"
  shows "is_red F p ∨ is_red F q"
proof -
  from ‹p ≠ q› have "p - q ≠ 0" by simp
  from translation_property'[OF this red_0, of q] show ?thesis by simp
qed

lemma weak_GB_is_strong_GB_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes "⋀f. f ∈ pmdl G ⟹ f ∈ dgrad_p_set d m ⟹ (red G)⇧*⇧* f 0"
  shows "is_Groebner_basis G"
  using assms(1, 2)
proof (rule Buchberger_criterion_dgrad_p_set)
  fix p q
  assume "p ∈ G" and "q ∈ G"
  hence "p ∈ pmdl G" and "q ∈ pmdl G" by (auto intro: pmdl.span_base)
  hence "spoly p q ∈ pmdl G" by (rule pmdl_closed_spoly)
  thus "(red G)⇧*⇧* (spoly p q) 0"
  proof (rule assms(3))
    note assms(1)
    moreover from ‹p ∈ G› assms(2) have "p ∈ dgrad_p_set d m" ..
    moreover from ‹q ∈ G› assms(2) have "q ∈ dgrad_p_set d m" ..
    ultimately show "spoly p q ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_spoly)
  qed
qed

lemma weak_GB_is_strong_GB:
  assumes "⋀f. f ∈ (pmdl G) ⟹ (red G)⇧*⇧* f 0"
  shows "is_Groebner_basis G"
  unfolding is_Groebner_basis_def
proof (rule relation.confluence_implies_ChurchRosser,
      simp add: relation.is_confluent_def relation.is_confluent_on_def, intro allI impI, erule conjE)
  fix f p q
  assume "(red G)⇧*⇧* f p" and "(red G)⇧*⇧* f q"
  hence "relation.srtc (red G) p q"
    by (meson relation.rtc_implies_srtc relation.srtc_symmetric relation.srtc_transitive)
  hence "p - q ∈ pmdl G" by (rule srtc_in_pmdl)
  hence "(red G)⇧*⇧* (p - q) 0" by (rule assms)
  thus "relation.cs (red G) p q" by (rule red_diff_rtrancl_cs)
qed

corollary GB_alt_1_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  shows "is_Groebner_basis G ⟷ (∀f ∈ pmdl G. f ∈ dgrad_p_set d m ⟶ (red G)⇧*⇧* f 0)"
  using weak_GB_is_strong_GB_dgrad_p_set[OF assms] GB_imp_zero_reducibility by blast

corollary GB_alt_1: "is_Groebner_basis G ⟷ (∀f ∈ pmdl G. (red G)⇧*⇧* f 0)"
  using weak_GB_is_strong_GB GB_imp_zero_reducibility by blast

lemma isGB_I_is_red:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes "⋀f. f ∈ pmdl G ⟹ f ∈ dgrad_p_set d m ⟹ f ≠ 0 ⟹ is_red G f"
  shows "is_Groebner_basis G"
  unfolding GB_alt_1_dgrad_p_set[OF assms(1, 2)]
proof (intro ballI impI)
  fix f
  assume "f ∈ pmdl G" and "f ∈ dgrad_p_set d m"
  with assms(1, 2) subset_refl assms(3) show "(red G)⇧*⇧* f 0"
    by (rule is_red_implies_0_red_dgrad_p_set)
qed

lemma GB_alt_2_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  shows "is_Groebner_basis G ⟷ (∀f ∈ pmdl G. f ≠ 0 ⟶ is_red G f)"
proof
  assume "is_Groebner_basis G"
  show "∀f∈pmdl G. f ≠ 0 ⟶ is_red G f"
  proof (intro ballI, intro impI)
    fix f
    assume "f ∈ (pmdl G)" and "f ≠ 0"
    show "is_red G f" by (rule GB_imp_reducibility, fact+)
  qed
next
  assume a2: "∀f∈pmdl G. f ≠ 0 ⟶ is_red G f"
  show "is_Groebner_basis G" unfolding GB_alt_1
  proof
    fix f
    assume "f ∈ pmdl G"
    from assms show "(red G)⇧*⇧* f 0"
    proof (rule is_red_implies_0_red_dgrad_p_set')
      fix q
      assume "q ∈ pmdl G" and "q ≠ 0"
      thus "is_red G q" by (rule a2[rule_format])
    qed (fact subset_refl, fact)
  qed
qed
  
lemma GB_adds_lt:
  assumes "is_Groebner_basis G" and "f ∈ pmdl G" and "f ≠ 0"
  obtains g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f"
proof -
  from assms(1) assms(2) have "(red G)⇧*⇧* f 0" by (rule GB_imp_zero_reducibility)
  show ?thesis by (rule zero_reducibility_implies_lt_divisibility, fact+)
qed

lemma isGB_I_adds_lt:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes "⋀f. f ∈ pmdl G ⟹ f ∈ dgrad_p_set d m ⟹ f ≠ 0 ⟹ (∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)"
  shows "is_Groebner_basis G"
  using assms(1, 2)
proof (rule isGB_I_is_red)
  fix f
  assume "f ∈ pmdl G" and "f ∈ dgrad_p_set d m" and "f ≠ 0"
  hence "(∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)" by (rule assms(3))
  then obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by blast
  thus "is_red G f" using ‹f ≠ 0› is_red_indI1 by blast
qed

lemma GB_alt_3_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  shows "is_Groebner_basis G ⟷ (∀f ∈ pmdl G. f ≠ 0 ⟶ (∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f))"
    (is "?L ⟷ ?R")
proof
  assume ?L
  show ?R
  proof (intro ballI impI)
    fix f
    assume "f ∈ pmdl G" and "f ≠ 0"
    with ‹?L› obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by (rule GB_adds_lt)
    thus "∃g∈G. g ≠ 0 ∧ lt g adds⇩t lt f" by blast
  qed
next
  assume ?R
  show ?L unfolding GB_alt_2_dgrad_p_set[OF assms]
  proof (intro ballI impI)
    fix f
    assume "f ∈ pmdl G" and "f ≠ 0"
    with ‹?R› have "(∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt f)" by blast
    then obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by blast
    thus "is_red G f" using ‹f ≠ 0› is_red_indI1 by blast
  qed
qed
  
lemma GB_insert:
  assumes "is_Groebner_basis G" and "f ∈ pmdl G"
  shows "is_Groebner_basis (insert f G)"
  using assms unfolding GB_alt_1
  by (metis insert_subset pmdl.span_insert_idI red_rtrancl_subset subsetI)

lemma GB_subset:
  assumes "is_Groebner_basis G" and "G ⊆ G'" and "pmdl G' = pmdl G"
  shows "is_Groebner_basis G'"
  using assms(1) unfolding GB_alt_1 using assms(2) assms(3) red_rtrancl_subset by blast

lemma (in ordered_term) GB_remove_0_stable_GB:
  assumes "is_Groebner_basis G"
  shows "is_Groebner_basis (G - {0})"
  using assms by (simp only: is_Groebner_basis_def red_minus_singleton_zero)

lemmas is_red_implies_0_red_finite = is_red_implies_0_red_dgrad_p_set'[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_implies_unique_nf_finite = GB_implies_unique_nf_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_alt_2_finite = GB_alt_2_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_alt_3_finite = GB_alt_3_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas pmdl_eqI_adds_lt_finite = pmdl_eqI_adds_lt_dgrad_p_set'[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]

subsection ‹Alternative Characterization of Gr\"obner Bases via Representations of S-Polynomials›

definition spoly_rep :: "('a ⇒ nat) ⇒ nat ⇒ ('t ⇒⇩0 'b) set ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b::field) ⇒ bool"
  where "spoly_rep d m G g1 g2 ⟷ (∃q. spoly g1 g2 = (∑g∈G. q g ⊙ g) ∧
                (∀g. q g ∈ punit.dgrad_p_set d m ∧
                        (q g ⊙ g ≠ 0 ⟶ lt (q g ⊙ g) ≺⇩t term_of_pair (lcs (lp g1) (lp g2),
                                                                      component_of_term (lt g2)))))"

lemma spoly_repI:
  "spoly g1 g2 = (∑g∈G. q g ⊙ g) ⟹ (⋀g. q g ∈ punit.dgrad_p_set d m) ⟹
    (⋀g. q g ⊙ g ≠ 0 ⟹ lt (q g ⊙ g) ≺⇩t term_of_pair (lcs (lp g1) (lp g2),
                                                        component_of_term (lt g2))) ⟹
    spoly_rep d m G g1 g2"
  by (auto simp: spoly_rep_def)

lemma spoly_repI_zero:
  assumes "spoly g1 g2 = 0"
  shows "spoly_rep d m G g1 g2"
proof (rule spoly_repI)
  show "spoly g1 g2 = (∑g∈G. 0 ⊙ g)" by (simp add: assms)
qed (simp_all add: punit.zero_in_dgrad_p_set)

lemma spoly_repE:
  assumes "spoly_rep d m G g1 g2"
  obtains q where "spoly g1 g2 = (∑g∈G. q g ⊙ g)" and "⋀g. q g ∈ punit.dgrad_p_set d m"
    and "⋀g. q g ⊙ g ≠ 0 ⟹ lt (q g ⊙ g) ≺⇩t term_of_pair (lcs (lp g1) (lp g2),
                                                             component_of_term (lt g2))"
  using assms by (auto simp: spoly_rep_def)

corollary isGB_D_spoly_rep:
  assumes "dickson_grading d" and "is_Groebner_basis G" and "G ⊆ dgrad_p_set d m" and "finite G"
    and "g1 ∈ G" and "g2 ∈ G" and "g1 ≠ 0" and "g2 ≠ 0"
  shows "spoly_rep d m G g1 g2"
proof (cases "spoly g1 g2 = 0")
  case True
  thus ?thesis by (rule spoly_repI_zero)
next
  case False
  let ?v = "term_of_pair (lcs (lp g1) (lp g2), component_of_term (lt g1))"
  let ?h = "crit_pair g1 g2"
  from assms(7, 8) have eq: "spoly g1 g2 = fst ?h + (- snd ?h)" by (simp add: spoly_alt)
  have "fst ?h ≺⇩p monomial 1 ?v" by (fact fst_crit_pair_below_lcs)
  hence d1: "fst ?h = 0 ∨ lt (fst ?h) ≺⇩t ?v" by (simp only: ord_strict_p_monomial_iff)
  have "snd ?h ≺⇩p monomial 1 ?v" by (fact snd_crit_pair_below_lcs)
  hence d2: "snd ?h = 0 ∨ lt (- snd ?h) ≺⇩t ?v" by (simp only: ord_strict_p_monomial_iff lt_uminus)
  note assms(1)
  moreover from assms(5, 3) have "g1 ∈ dgrad_p_set d m" ..
  moreover from assms(6, 3) have "g2 ∈ dgrad_p_set d m" ..
  ultimately have "spoly g1 g2 ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_spoly)
  from assms(5) have "g1 ∈ pmdl G" by (rule pmdl.span_base)
  moreover from assms(6) have "g2 ∈ pmdl G" by (rule pmdl.span_base)
  ultimately have "spoly g1 g2 ∈ pmdl G" by (rule pmdl_closed_spoly)
  with assms(2) have "(red G)⇧*⇧* (spoly g1 g2) 0" by (rule GB_imp_zero_reducibility)
  with assms(1, 3, 4) ‹spoly _ _ ∈ dgrad_p_set _ _› obtain q
    where 1: "spoly g1 g2 = 0 + (∑g∈G. q g ⊙ g)" and 2: "⋀g. q g ∈ punit.dgrad_p_set d m"
      and "⋀g. lt (q g ⊙ g) ≼⇩t lt (spoly g1 g2)" by (rule red_rtrancl_repE) blast
  show ?thesis
  proof (rule spoly_repI)
    fix g
    note ‹lt (q g ⊙ g) ≼⇩t lt (spoly g1 g2)›
    also from d1 have "lt (spoly g1 g2) ≺⇩t ?v"
    proof
      assume "fst ?h = 0"
      hence eq: "spoly g1 g2 = - snd ?h" by (simp add: eq)
      also from d2 have "lt … ≺⇩t ?v"
      proof
        assume "snd ?h = 0"
        with False show ?thesis by (simp add: eq)
      qed
      finally show ?thesis .
    next
      assume *: "lt (fst ?h) ≺⇩t ?v"
      from d2 show ?thesis
      proof
        assume "snd ?h = 0"
        with * show ?thesis by (simp add: eq)
      next
        assume **: "lt (- snd ?h) ≺⇩t ?v"
        have "lt (spoly g1 g2) ≼⇩t ord_term_lin.max (lt (fst ?h)) (lt (- snd ?h))" unfolding eq
          by (fact lt_plus_le_max)
        also from * ** have "… ≺⇩t ?v" by (simp only: ord_term_lin.max_less_iff_conj)
        finally show ?thesis .
      qed
    qed
    also from False have "… = term_of_pair (lcs (lp g1) (lp g2), component_of_term (lt g2))"
      by (simp add: spoly_def Let_def split: if_split_asm)
    finally show "lt (q g ⊙ g) ≺⇩t term_of_pair (lcs (lp g1) (lp g2), component_of_term (lt g2))" .
  qed (simp_all add: 1 2)
qed

text ‹The finiteness assumption on ‹G› in the following theorem could be dropped, but it makes the
  proof a lot easier (although it is still fairly complicated).›

lemma isGB_I_spoly_rep:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m" and "finite G"
    and "⋀g1 g2. g1 ∈ G ⟹ g2 ∈ G ⟹ g1 ≠ 0 ⟹ g2 ≠ 0 ⟹ spoly g1 g2 ≠ 0 ⟹ spoly_rep d m G g1 g2"
  shows "is_Groebner_basis G"
proof (rule ccontr)
  assume "¬ is_Groebner_basis G"
  then obtain p where "p ∈ pmdl G" and p_in: "p ∈ dgrad_p_set d m" and "¬ (red G)⇧*⇧* p 0"
    by (auto simp: GB_alt_1_dgrad_p_set[OF assms(1, 2)])
  from ‹¬ is_Groebner_basis G› have "G ≠ {}" by (auto simp: is_Groebner_basis_empty)

  obtain r where p_red: "(red G)⇧*⇧* p r" and r_irred: "¬ is_red G r"
  proof -
    define A where "A = {q. (red G)⇧*⇧* p q}"
    from assms(1, 2) have "wfP (red G)¯¯" by (rule red_wf_dgrad_p_set)
    moreover have "p ∈ A" by (simp add: A_def)
    ultimately obtain r where "r ∈ A" and r_min: "⋀z. (red G)¯¯ z r ⟹ z ∉ A"
      by (rule wfE_min[to_pred]) blast
    show ?thesis
    proof
      from ‹r ∈ A› show *: "(red G)⇧*⇧* p r" by (simp add: A_def)

      show "¬ is_red G r"
      proof
        assume "is_red G r"
        then obtain z where "(red G) r z" by (rule is_redE)
        hence "(red G)¯¯ z r" by simp
        hence "z ∉ A" by (rule r_min)
        hence "¬ (red G)⇧*⇧* p z" by (simp add: A_def)
        moreover from * ‹(red G) r z› have "(red G)⇧*⇧* p z" ..
        ultimately show False ..
      qed
    qed
  qed
  from assms(1, 2) p_in p_red have r_in: "r ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_red_rtrancl)
  from p_red ‹¬ (red G)⇧*⇧* p 0› have "r ≠ 0" by blast
  from p_red have "p - r ∈ pmdl G" by (rule red_rtranclp_diff_in_pmdl)
  with ‹p ∈ pmdl G› have "p - (p - r) ∈ pmdl G" by (rule pmdl.span_diff)
  hence "r ∈ pmdl G" by simp
  with assms(3) obtain q0 where r: "r = (∑g∈G. q0 g ⊙ g)" by (rule pmdl.span_finiteE)
  from assms(3) have "finite (q0 ` G)" by (rule finite_imageI)
  then obtain m0 where "q0 ` G ⊆ punit.dgrad_p_set d m0" by (rule punit.dgrad_p_set_exhaust)
  define m' where "m' = ord_class.max m m0"
  have "dgrad_p_set d m ⊆ dgrad_p_set d m'" by (rule dgrad_p_set_subset) (simp add: m'_def)
  with assms(2) have G_sub: "G ⊆ dgrad_p_set d m'" by (rule subset_trans)
  have "punit.dgrad_p_set d m0 ⊆ punit.dgrad_p_set d m'"
    by (rule punit.dgrad_p_set_subset) (simp add: m'_def)
  with ‹q0 ` G ⊆ _› have "q0 ` G ⊆ punit.dgrad_p_set d m'" by (rule subset_trans)

  define mlt where "mlt = (λq. ord_term_lin.Max (lt ` {q g ⊙ g | g. g ∈ G ∧ q g ⊙ g ≠ 0}))"
  define mnum where "mnum = (λq. card {g∈G. q g ⊙ g ≠ 0 ∧ lt (q g ⊙ g) = mlt q})"
  define rel where "rel = (λq1 q2. mlt q1 ≺⇩t mlt q2 ∨ (mlt q1 = mlt q2 ∧ mnum q1 < mnum q2))"
  define rel_dom where "rel_dom = {q. q ` G ⊆ punit.dgrad_p_set d m' ∧ r = (∑g∈G. q g ⊙ g)}"

  have mlt_in: "mlt q ∈ lt ` {q g ⊙ g | g. g ∈ G ∧ q g ⊙ g ≠ 0}" if "q ∈ rel_dom" for q
    unfolding mlt_def
  proof (rule ord_term_lin.Max_in, simp_all add: assms(3), rule ccontr)
    assume "∄g. g ∈ G ∧ q g ⊙ g ≠ 0"
    hence "q g ⊙ g = 0" if "g ∈ G" for g using that by simp
    with that have "r = 0" by (simp add: rel_dom_def)
    with ‹r ≠ 0› show False ..
  qed
  
  have rel_dom_dgrad_set: "pp_of_term ` mlt ` rel_dom ⊆ dgrad_set d m'"
  proof (rule subsetI, elim imageE)
    fix q v t
    assume "q ∈ rel_dom" and v: "v = mlt q" and t: "t = pp_of_term v"
    from this(1) have "v ∈ lt ` {q g ⊙ g | g. g ∈ G ∧ q g ⊙ g ≠ 0}" unfolding v by (rule mlt_in)
    then obtain g where "g ∈ G" and "q g ⊙ g ≠ 0" and v: "v = lt (q g ⊙ g)" by blast
    from this(2) have "q g ≠ 0" and "g ≠ 0" by auto
    hence "v = punit.lt (q g) ⊕ lt g" unfolding v by (rule lt_mult_scalar)
    hence "t = punit.lt (q g) + lp g" by (simp add: t pp_of_term_splus)
    also from assms(1) have "d … = ord_class.max (d (punit.lt (q g))) (d (lp g))"
      by (rule dickson_gradingD1)
    also have "… ≤ m'"
    proof (rule max.boundedI)
      from ‹g ∈ G› ‹q ∈ rel_dom› have "q g ∈ punit.dgrad_p_set d m'" by (auto simp: rel_dom_def)
      moreover from ‹q g ≠ 0› have "punit.lt (q g) ∈ keys (q g)" by (rule punit.lt_in_keys)
      ultimately show "d (punit.lt (q g)) ≤ m'" by (rule punit.dgrad_p_setD[simplified])
    next
      from ‹g ∈ G› G_sub have "g ∈ dgrad_p_set d m'" ..
      moreover from ‹g ≠ 0› have "lt g ∈ keys g" by (rule lt_in_keys)
      ultimately show "d (lp g) ≤ m'" by (rule dgrad_p_setD)
    qed
    finally show "t ∈ dgrad_set d m'" by (simp add: dgrad_set_def)
  qed

  obtain q where "q ∈ rel_dom" and q_min: "⋀q'. rel q' q ⟹ q' ∉ rel_dom"
  proof -
    from ‹q0 ` G ⊆ punit.dgrad_p_set d m'› have "q0 ∈ rel_dom" by (simp add: rel_dom_def r)
    hence "mlt q0 ∈ mlt ` rel_dom" by (rule imageI)
    with assms(1) obtain u where "u ∈ mlt ` rel_dom" and u_min: "⋀w. w ≺⇩t u ⟹ w ∉ mlt ` rel_dom"
      using rel_dom_dgrad_set by (rule ord_term_minimum_dgrad_set) blast
    from this(1) obtain q' where "q' ∈ rel_dom" and u: "u = mlt q'" ..
    hence "q' ∈ rel_dom ∩ {q. mlt q = u}" (is "_ ∈ ?A") by simp
    hence "mnum q' ∈ mnum ` ?A" by (rule imageI)
    with wf[to_pred] obtain k where "k ∈ mnum ` ?A" and k_min: "⋀l. l < k ⟹ l ∉ mnum ` ?A"
      by (rule wfE_min[to_pred]) blast
    from this(1) obtain q'' where "q'' ∈ rel_dom" and mlt'': "mlt q'' = u" and k: "k = mnum q''"
      by blast
    from this(1) show ?thesis
    proof
      fix q0
      assume "rel q0 q''"
      show "q0 ∉ rel_dom"
      proof
        assume "q0 ∈ rel_dom"
        from ‹rel q0 q''› show False unfolding rel_def
        proof (elim disjE conjE)
          assume "mlt q0 ≺⇩t mlt q''"
          hence "mlt q0 ∉ mlt ` rel_dom" unfolding mlt'' by (rule u_min)
          moreover from ‹q0 ∈ rel_dom› have "mlt q0 ∈ mlt ` rel_dom" by (rule imageI)
          ultimately show ?thesis ..
        next
          assume "mlt q0 = mlt q''"
          with ‹q0 ∈ rel_dom› have "q0 ∈ ?A" by (simp add: mlt'')
          assume "mnum q0 < mnum q''"
          hence "mnum q0 ∉ mnum ` ?A" unfolding k[symmetric] by (rule k_min)
          with ‹q0 ∈ ?A› show ?thesis by blast
        qed
      qed
    qed
  qed
  from this(1) have q_in: "⋀g. g ∈ G ⟹ q g ∈ punit.dgrad_p_set d m'"
    and r: "r = (∑g∈G. q g ⊙ g)" by (auto simp: rel_dom_def)

  define v where "v = mlt q"
  from ‹q ∈ rel_dom› have "v ∈ lt ` {q g ⊙ g | g. g ∈ G ∧ q g ⊙ g ≠ 0}" unfolding v_def
    by (rule mlt_in)
  then obtain g1 where "g1 ∈ G" and "q g1 ⊙ g1 ≠ 0" and v1: "v = lt (q g1 ⊙ g1)" by blast
  moreover define M where "M = {g∈G. q g ⊙ g ≠ 0 ∧ lt (q g ⊙ g) = v}"
  ultimately have "g1 ∈ M" by simp
  have v_max: "lt (q g ⊙ g) ≺⇩t v" if "g ∈ G" and "g ∉ M" and "q g ⊙ g ≠ 0" for g
  proof -
    from that have "lt (q g ⊙ g) ≠ v" by (auto simp: M_def)
    moreover have "lt (q g ⊙ g) ≼⇩t v" unfolding v_def mlt_def
      by (rule ord_term_lin.Max_ge) (auto simp: assms(3) ‹q g ⊙ g ≠ 0› intro!: imageI ‹g ∈ G›)
    ultimately show ?thesis by simp
  qed
  from ‹q g1 ⊙ g1 ≠ 0› have "q g1 ≠ 0" and "g1 ≠ 0" by auto
  hence v1': "v = punit.lt (q g1) ⊕ lt g1" unfolding v1 by (rule lt_mult_scalar)
  have "M - {g1} ≠ {}"
  proof
    assume "M - {g1} = {}"
    have "v ∈ keys (q g1 ⊙ g1)" unfolding v1 using ‹q g1 ⊙ g1 ≠ 0› by (rule lt_in_keys)
    moreover have "v ∉ keys (∑g∈G-{g1}. q g ⊙ g)"
    proof
      assume "v ∈ keys (∑g∈G-{g1}. q g ⊙ g)"
      also have "… ⊆ (⋃g∈G-{g1}. keys (q g ⊙ g))" by (fact keys_sum_subset)
      finally obtain g where "g ∈ G - {g1}" and "v ∈ keys (q g ⊙ g)" ..
      from this(2) have "q g ⊙ g ≠ 0" and "v ≼⇩t lt (q g ⊙ g)" by (auto intro: lt_max_keys)
      from ‹g ∈ G - {g1}› ‹M - {g1} = {}› have "g ∈ G" and "g ∉ M" by blast+
      hence "lt (q g ⊙ g) ≺⇩t v" by (rule v_max) fact
      with ‹v ≼⇩t _› show False by simp
    qed
    ultimately have "v ∈ keys (q g1 ⊙ g1 + (∑g∈G-{g1}. q g ⊙ g))" by (rule in_keys_plusI1)
    also from ‹g1 ∈ G› assms(3) have "… = keys r" by (simp add: r sum.remove)
    finally have "v ∈ keys r" .
    with ‹g1 ∈ G› ‹g1 ≠ 0› have "is_red G r" by (rule is_red_addsI) (simp add: v1' term_simps)
    with r_irred show False ..
  qed
  then obtain g2 where "g2 ∈ M" and "g1 ≠ g2" by blast
  from this(1) have "g2 ∈ G" and "q g2 ⊙ g2 ≠ 0" and v2: "v = lt (q g2 ⊙ g2)" by (simp_all add: M_def)
  from this(2) have "q g2 ≠ 0" and "g2 ≠ 0" by auto
  hence v2': "v = punit.lt (q g2) ⊕ lt g2" unfolding v2 by (rule lt_mult_scalar)
  hence "component_of_term (punit.lt (q g1) ⊕ lt g1) = component_of_term (punit.lt (q g2) ⊕ lt g2)"
    by (simp only: v1' flip: v2')
  hence cmp_eq: "component_of_term (lt g1) = component_of_term (lt g2)" by (simp add: term_simps)

  have "M ⊆ G" by (simp add: M_def)
  have "r = q g1 ⊙ g1 + (∑g∈G - {g1}. q g ⊙ g)"
    using assms(3) ‹g1 ∈ G› by (simp add: r sum.remove)
  also have "… = q g1 ⊙ g1 + q g2 ⊙ g2 + (∑g∈G - {g1} - {g2}. q g ⊙ g)"
    using assms(3) ‹g2 ∈ G› ‹g1 ≠ g2›
    by (metis (no_types, lifting) add.assoc finite_Diff insert_Diff insert_Diff_single insert_iff
                sum.insert_remove)
  finally have r: "r = q g1 ⊙ g1 + q g2 ⊙ g2 + (∑g∈G - {g1, g2}. q g ⊙ g)"
    by (simp flip: Diff_insert2)

  let ?l = "lcs (lp g1) (lp g2)"
  let ?v = "term_of_pair (?l, component_of_term (lt g2))"
  have "lp g1 adds lp (q g1 ⊙ g1)" by (simp add: v1' pp_of_term_splus flip: v1)
  moreover have "lp g2 adds lp (q g1 ⊙ g1)" by (simp add: v2' pp_of_term_splus flip: v1)
  ultimately have l_adds: "?l adds lp (q g1 ⊙ g1)" by (rule lcs_adds)

  have "spoly_rep d m G g1 g2"
  proof (cases "spoly g1 g2 = 0")
    case True
    thus ?thesis by (rule spoly_repI_zero)
  next
    case False
    with ‹g1 ∈ G› ‹g2 ∈ G› ‹g1 ≠ 0› ‹g2 ≠ 0› show ?thesis by (rule assms(4))
  qed
  then obtain q' where spoly: "spoly g1 g2 = (∑g∈G. q' g ⊙ g)"
    and "⋀g. q' g ∈ punit.dgrad_p_set d m" and "⋀g. q' g ⊙ g ≠ 0 ⟹ lt (q' g ⊙ g) ≺⇩t ?v"
    by (rule spoly_repE) blast
  note this(2)
  also have "punit.dgrad_p_set d m ⊆ punit.dgrad_p_set d m'"
    by (rule punit.dgrad_p_set_subset) (simp add: m'_def)
  finally have q'_in: "⋀g. q' g ∈ punit.dgrad_p_set d m'" .

  define mu where "mu = monomial (lc (q g1 ⊙ g1)) (lp (q g1 ⊙ g1) - ?l)"
  define mu1 where "mu1 = monomial (1 / lc g1) (?l - lp g1)"
  define mu2 where "mu2 = monomial (1 / lc g2) (?l - lp g2)"
    define q'' where "q'' = (λg. q g + mu * q' g)
                              (g1:=punit.tail (q g1) + mu * q' g1, g2:=q g2 + mu * q' g2 + mu * mu2)"
  from ‹q g1 ⊙ g1 ≠ 0› have "mu ≠ 0" by (simp add: mu_def monomial_0_iff lc_eq_zero_iff)
  from ‹g1 ≠ 0› l_adds have mu_times_mu1: "mu * mu1 = monomial (punit.lc (q g1)) (punit.lt (q g1))"
    by (simp add: mu_def mu1_def times_monomial_monomial lc_mult_scalar lc_eq_zero_iff
              minus_plus_minus_cancel adds_lcs v1' pp_of_term_splus flip: v1)
  from l_adds have mu_times_mu2: "mu * mu2 = monomial (lc (q g1 ⊙ g1) / lc g2) (punit.lt (q g2))"
    by (simp add: mu_def mu2_def times_monomial_monomial lc_mult_scalar minus_plus_minus_cancel
              adds_lcs_2 v2' pp_of_term_splus flip: v1)
  have "mu1 ⊙ g1 - mu2 ⊙ g2 = spoly g1 g2"
    by (simp add: spoly_def Let_def cmp_eq lc_def mult_scalar_monomial mu1_def mu2_def)
  also have "… = q' g1 ⊙ g1 + (∑g∈G - {g1}. q' g ⊙ g)"
    using assms(3) ‹g1 ∈ G› by (simp add: spoly sum.remove)
  also have "… = q' g1 ⊙ g1 + q' g2 ⊙ g2 + (∑g∈G - {g1} - {g2}. q' g ⊙ g)"
    using assms(3) ‹g2 ∈ G› ‹g1 ≠ g2›
    by (metis (no_types, lifting) add.assoc finite_Diff insert_Diff insert_Diff_single insert_iff
                sum.insert_remove)
  finally have "(q' g1 - mu1) ⊙ g1 + (q' g2 + mu2) ⊙ g2 + (∑g∈G - {g1, g2}. q' g ⊙ g) = 0"
    by (simp add: algebra_simps flip: Diff_insert2)
  hence "0 = mu ⊙ ((q' g1 - mu1) ⊙ g1 + (q' g2 + mu2) ⊙ g2 + (∑g∈G - {g1, g2}. q' g ⊙ g))" by simp
  also have "… = (mu * q' g1 - mu * mu1) ⊙ g1 + (mu * q' g2 + mu * mu2) ⊙ g2 +
                    (∑g∈G - {g1, g2}. (mu * q' g) ⊙ g)"
    by (simp add: mult_scalar_distrib_left sum_mult_scalar_distrib_left distrib_left right_diff_distrib
            flip: mult_scalar_assoc)
  finally have "r = r + (mu * q' g1 - mu * mu1) ⊙ g1 + (mu * q' g2 + mu * mu2) ⊙ g2 +
                          (∑g∈G - {g1, g2}. (mu * q' g) ⊙ g)" by simp
  also have "… = (q g1 - mu * mu1 + mu * q' g1) ⊙ g1 + (q g2 + mu * q' g2 + mu * mu2) ⊙ g2 +
                    (∑g∈G - {g1, g2}. (q g + mu * q' g) ⊙ g)"
    by (simp add: r algebra_simps flip: sum.distrib)
  also have "q g1 - mu * mu1 = punit.tail (q g1)"
    by (simp only: mu_times_mu1 punit.leading_monomial_tail diff_eq_eq add.commute[of "punit.tail (q g1)"])
  finally have "r = q'' g1 ⊙ g1 + q'' g2 ⊙ g2 + (∑g∈G - {g1} - {g2}. q'' g ⊙ g)"
    using ‹g1 ≠ g2› by (simp add: q''_def flip: Diff_insert2)
  also from ‹finite G› ‹g1 ≠ g2› ‹g1 ∈ G› ‹g2 ∈ G› have "… = (∑g∈G. q'' g ⊙ g)"
    by (simp add: sum.remove) (metis (no_types, lifting) finite_Diff insert_Diff insert_iff sum.remove)
  finally have r: "r = (∑g∈G. q'' g ⊙ g)" .

  have 1: "lt ((mu * q' g) ⊙ g) ≺⇩t v" if "(mu * q' g) ⊙ g ≠ 0" for g
  proof -
    from that have "q' g ⊙ g ≠ 0" by (auto simp: mult_scalar_assoc)
    hence *: "lt (q' g ⊙ g) ≺⇩t ?v" by fact
    from ‹q' g ⊙ g ≠ 0› ‹mu ≠ 0› have "lt ((mu * q' g) ⊙ g) = (lp (q g1 ⊙ g1) - ?l) ⊕ lt (q' g ⊙ g)"
      by (simp add: mult_scalar_assoc lt_mult_scalar) (simp add: mu_def punit.lt_monomial monomial_0_iff)
    also from * have "… ≺⇩t (lp (q g1 ⊙ g1) - ?l) ⊕ ?v" by (rule splus_mono_strict)
    also from l_adds have "… = v" by (simp add: splus_def minus_plus term_simps v1' flip: cmp_eq v1)
    finally show ?thesis .
  qed

  have 2: "lt (q'' g1 ⊙ g1) ≺⇩t v" if "q'' g1 ⊙ g1 ≠ 0" using that
  proof (rule lt_less)
    fix u
    assume "v ≼⇩t u"
    have "u ∉ keys (q'' g1 ⊙ g1)"
    proof
      assume "u ∈ keys (q'' g1 ⊙ g1)"
      also from ‹g1 ≠ g2› have "… = keys ((punit.tail (q g1) + mu * q' g1) ⊙ g1)"
        by (simp add: q''_def)
      also have "… ⊆ keys (punit.tail (q g1) ⊙ g1) ∪ keys ((mu * q' g1) ⊙ g1)"
        unfolding mult_scalar_distrib_right by (fact Poly_Mapping.keys_add)
      finally show False
      proof
        assume "u ∈ keys (punit.tail (q g1) ⊙ g1)"
        hence "u ≼⇩t lt (punit.tail (q g1) ⊙ g1)" by (rule lt_max_keys)
        also have "… ≼⇩t punit.lt (punit.tail (q g1)) ⊕ lt g1"
          by (metis in_keys_mult_scalar_le lt_def lt_in_keys min_term_min)
        also have "… ≺⇩t punit.lt (q g1) ⊕ lt g1"
        proof (intro splus_mono_strict_left punit.lt_tail notI)
          assume "punit.tail (q g1) = 0"
          with ‹u ∈ keys (punit.tail (q g1) ⊙ g1)› show False by simp
        qed
        also have "… = v" by (simp only: v1')
        finally show ?thesis using ‹v ≼⇩t u› by simp
      next
        assume "u ∈ keys ((mu * q' g1) ⊙ g1)"
        hence "(mu * q' g1) ⊙ g1 ≠ 0" and "u ≼⇩t lt ((mu * q' g1) ⊙ g1)" by (auto intro: lt_max_keys)
        note this(2)
        also from ‹(mu * q' g1) ⊙ g1 ≠ 0› have "lt ((mu * q' g1) ⊙ g1) ≺⇩t v" by (rule 1)
        finally show ?thesis using ‹v ≼⇩t u› by simp
      qed
    qed
    thus "lookup (q'' g1 ⊙ g1) u = 0" by (simp add: in_keys_iff)
  qed

  have 3: "lt (q'' g2 ⊙ g2) ≼⇩t v"
  proof (rule lt_le)
    fix u
    assume "v ≺⇩t u"
    have "u ∉ keys (q'' g2 ⊙ g2)"
    proof
      assume "u ∈ keys (q'' g2 ⊙ g2)"
      also have "… = keys ((q g2 + mu * q' g2 + mu * mu2) ⊙ g2)" by (simp add: q''_def)
      also have "… ⊆ keys (q g2 ⊙ g2 + (mu * q' g2) ⊙ g2) ∪ keys ((mu * mu2) ⊙ g2)"
        unfolding mult_scalar_distrib_right by (fact Poly_Mapping.keys_add)
      finally show False
      proof
        assume "u ∈ keys (q g2 ⊙ g2 + (mu * q' g2) ⊙ g2)"
        also have "… ⊆ keys (q g2 ⊙ g2) ∪ keys ((mu * q' g2) ⊙ g2)" by (fact Poly_Mapping.keys_add)
        finally show ?thesis
        proof
          assume "u ∈ keys (q g2 ⊙ g2)"
          hence "u ≼⇩t lt (q g2 ⊙ g2)" by (rule lt_max_keys)
          with ‹v ≺⇩t u› show ?thesis by (simp add: v2)
        next
          assume "u ∈ keys ((mu * q' g2) ⊙ g2)"
          hence "(mu * q' g2) ⊙ g2 ≠ 0" and "u ≼⇩t lt ((mu * q' g2) ⊙ g2)" by (auto intro: lt_max_keys)
          note this(2)
          also from ‹(mu * q' g2) ⊙ g2 ≠ 0› have "lt ((mu * q' g2) ⊙ g2) ≺⇩t v" by (rule 1)
          finally show ?thesis using ‹v ≺⇩t u› by simp
        qed
      next
        assume "u ∈ keys ((mu * mu2) ⊙ g2)"
        hence "(mu * mu2) ⊙ g2 ≠ 0" and "u ≼⇩t lt ((mu * mu2) ⊙ g2)" by (auto intro: lt_max_keys)
        from this(1) have "(mu * mu2) ≠ 0" by auto
        note ‹u ≼⇩t _›
        also from ‹mu * mu2 ≠ 0› ‹g2 ≠ 0› have "lt ((mu * mu2) ⊙ g2) = punit.lt (q g2) ⊕ lt g2"
          by (simp add: lt_mult_scalar) (simp add: mu_times_mu2 punit.lt_monomial monomial_0_iff)
        finally show ?thesis using ‹v ≺⇩t u› by (simp add: v2')
      qed
    qed
    thus "lookup (q'' g2 ⊙ g2) u = 0" by (simp add: in_keys_iff)
  qed

  have 4: "lt (q'' g ⊙ g) ≼⇩t v" if "g ∈ M" for g
  proof (cases "g ∈ {g1, g2}")
    case True
    hence "g = g1 ∨ g = g2" by simp
    thus ?thesis
    proof
      assume "g = g1"
      show ?thesis
      proof (cases "q'' g1 ⊙ g1 = 0")
        case True
        thus ?thesis by (simp add: ‹g = g1› min_term_min)
      next
        case False
        hence "lt (q'' g ⊙ g) ≺⇩t v" unfolding ‹g = g1› by (rule 2)
        thus ?thesis by simp
      qed
    next
      assume "g = g2"
      with 3 show ?thesis by simp
    qed
  next
    case False
    hence q'': "q'' g = q g + mu * q' g" by (simp add: q''_def)
    show ?thesis
    proof (rule lt_le)
      fix u
      assume "v ≺⇩t u"
      have "u ∉ keys (q'' g ⊙ g)"
      proof
        assume "u ∈ keys (q'' g ⊙ g)"
        also have "… ⊆ keys (q g ⊙ g) ∪ keys ((mu * q' g) ⊙ g)"
          unfolding q'' mult_scalar_distrib_right by (fact Poly_Mapping.keys_add)
        finally show False
        proof
          assume "u ∈ keys (q g ⊙ g)"
          hence "u ≼⇩t lt (q g ⊙ g)" by (rule lt_max_keys)
          with ‹g ∈ M› ‹v ≺⇩t u› show ?thesis by (simp add: M_def)
        next
          assume "u ∈ keys ((mu * q' g) ⊙ g)"
          hence "(mu * q' g) ⊙ g ≠ 0" and "u ≼⇩t lt ((mu * q' g) ⊙ g)" by (auto intro: lt_max_keys)
          note this(2)
          also from ‹(mu * q' g) ⊙ g ≠ 0› have "lt ((mu * q' g) ⊙ g) ≺⇩t v" by (rule 1)
          finally show ?thesis using ‹v ≺⇩t u› by simp
        qed
      qed
      thus "lookup (q'' g ⊙ g) u = 0" by (simp add: in_keys_iff)
    qed
  qed

  have 5: "lt (q'' g ⊙ g) ≺⇩t v" if "g ∈ G" and "g ∉ M" and "q'' g ⊙ g ≠ 0" for g using that(3)
  proof (rule lt_less)
    fix u
    assume "v ≼⇩t u"
    from that(2) ‹g1 ∈ M› ‹g2 ∈ M› have "g ≠ g1" and "g ≠ g2" by blast+
    hence q'': "q'' g = q g + mu * q' g" by (simp add: q''_def)
    have "u ∉ keys (q'' g ⊙ g)"
    proof
      assume "u ∈ keys (q'' g ⊙ g)"
      also have "… ⊆ keys (q g ⊙ g) ∪ keys ((mu * q' g) ⊙ g)"
        unfolding q'' mult_scalar_distrib_right by (fact Poly_Mapping.keys_add)
      finally show False
      proof
        assume "u ∈ keys (q g ⊙ g)"
        hence "q g ⊙ g ≠ 0" and "u ≼⇩t lt (q g ⊙ g)" by (auto intro: lt_max_keys)
        note this(2)
        also from that(1, 2) ‹q g ⊙ g ≠ 0› have "… ≺⇩t v" by (rule v_max)
        finally show ?thesis using ‹v ≼⇩t u› by simp
      next
        assume "u ∈ keys ((mu * q' g) ⊙ g)"
        hence "(mu * q' g) ⊙ g ≠ 0" and "u ≼⇩t lt ((mu * q' g) ⊙ g)" by (auto intro: lt_max_keys)
        note this(2)
        also from ‹(mu * q' g) ⊙ g ≠ 0› have "lt ((mu * q' g) ⊙ g) ≺⇩t v" by (rule 1)
        finally show ?thesis using ‹v ≼⇩t u› by simp
      qed
    qed
    thus "lookup (q'' g ⊙ g) u = 0" by (simp add: in_keys_iff)
  qed

  define u where "u = mlt q''"
  have u_in: "u ∈ lt ` {q'' g ⊙ g | g. g ∈ G ∧ q'' g ⊙ g ≠ 0}" unfolding u_def mlt_def
  proof (rule ord_term_lin.Max_in, simp_all add: assms(3), rule ccontr)
    assume "∄g. g ∈ G ∧ q'' g ⊙ g ≠ 0"
    hence "q'' g ⊙ g = 0" if "g ∈ G" for g using that by simp
    hence "r = 0" by (simp add: r)
    with ‹r ≠ 0› show False ..
  qed
  have u_max: "lt (q'' g ⊙ g) ≼⇩t u" if "g ∈ G" for g
  proof (cases "q'' g ⊙ g = 0")
    case True
    thus ?thesis by (simp add: min_term_min)
  next
    case False
    show ?thesis unfolding u_def mlt_def
      by (rule ord_term_lin.Max_ge) (auto simp: assms(3) False intro!: imageI ‹g ∈ G›)
  qed
  have "q'' ∈ rel_dom"
  proof (simp add: rel_dom_def r, intro subsetI, elim imageE)
    fix g
    assume "g ∈ G"
    from assms(1) l_adds have "d (lp (q g1 ⊙ g1) - ?l) ≤ d (lp (q g1 ⊙ g1))"
      by (rule dickson_grading_minus)
    also have "… = d (punit.lt (q g1) + lp g1)" by (simp add: v1' term_simps flip: v1)
    also from assms(1) have "… = ord_class.max (d (punit.lt (q g1))) (d (lp g1))"
      by (rule dickson_gradingD1)
    also have "… ≤ m'"
    proof (rule max.boundedI)
      from ‹g1 ∈ G› have "q g1 ∈ punit.dgrad_p_set d m'" by (rule q_in)
      moreover from ‹q g1 ≠ 0› have "punit.lt (q g1) ∈ keys (q g1)" by (rule punit.lt_in_keys)
      ultimately show "d (punit.lt (q g1)) ≤ m'" by (rule punit.dgrad_p_setD[simplified])
    next
      from ‹g1 ∈ G› G_sub have "g1 ∈ dgrad_p_set d m'" ..
      moreover from ‹g1 ≠ 0› have "lt g1 ∈ keys g1" by (rule lt_in_keys)
      ultimately show "d (lp g1) ≤ m'" by (rule dgrad_p_setD)
    qed
    finally have d1: "d (lp (q g1 ⊙ g1) - ?l) ≤ m'" .
    have "d (?l - lp g2) ≤ ord_class.max (d (lp g2)) (d (lp g1))"
      unfolding lcs_comm[of "lp g1"] using assms(1) by (rule dickson_grading_lcs_minus)
    also have "… ≤ m'"
    proof (rule max.boundedI)
      from ‹g2 ∈ G› G_sub have "g2 ∈ dgrad_p_set d m'" ..
      moreover from ‹g2 ≠ 0› have "lt g2 ∈ keys g2" by (rule lt_in_keys)
      ultimately show "d (lp g2) ≤ m'" by (rule dgrad_p_setD)
    next
      from ‹g1 ∈ G› G_sub have "g1 ∈ dgrad_p_set d m'" ..
      moreover from ‹g1 ≠ 0› have "lt g1 ∈ keys g1" by (rule lt_in_keys)
      ultimately show "d (lp g1) ≤ m'" by (rule dgrad_p_setD)
    qed
    finally have mu2: "mu2 ∈ punit.dgrad_p_set d m'"
      by (simp add: mu2_def punit.dgrad_p_set_def dgrad_set_def)
    fix z
    assume z: "z = q'' g"
    have "g = g1 ∨ g = g2 ∨ (g ≠ g1 ∧ g ≠ g2)" by blast
    thus "z ∈ punit.dgrad_p_set d m'"
    proof (elim disjE conjE)
      assume "g = g1"
      with ‹g1 ≠ g2› have "q'' g = punit.tail (q g1) + mu * q' g1" by (simp add: q''_def)
      also have "… ∈ punit.dgrad_p_set d m'" unfolding mu_def times_monomial_left
        by (intro punit.dgrad_p_set_closed_plus punit.dgrad_p_set_closed_tail
                punit.dgrad_p_set_closed_monom_mult d1 assms(1) q_in q'_in ‹g1 ∈ G›)
      finally show ?thesis by (simp only: z)
    next
      assume "g = g2"
      hence "q'' g = q g2 + mu * q' g2 + mu * mu2" by (simp add: q''_def)
      also have "… ∈ punit.dgrad_p_set d m'" unfolding mu_def times_monomial_left
        by (intro punit.dgrad_p_set_closed_plus punit.dgrad_p_set_closed_monom_mult
                d1 mu2 q_in q'_in assms(1) ‹g2 ∈ G›)
      finally show ?thesis by (simp only: z)
    next
      assume "g ≠ g1" and "g ≠ g2"
      hence "q'' g = q g + mu * q' g" by (simp add: q''_def)
      also have "… ∈ punit.dgrad_p_set d m'" unfolding mu_def times_monomial_left
        by (intro punit.dgrad_p_set_closed_plus punit.dgrad_p_set_closed_monom_mult
                d1 assms(1) q_in q'_in ‹g ∈ G›)
      finally show ?thesis by (simp only: z)
    qed
  qed
  with q_min have "¬ rel q'' q" by blast
  hence "v ≼⇩t u" and "u ≠ v ∨ mnum q ≤ mnum q''" by (auto simp: v_def u_def rel_def)
  moreover have "u ≼⇩t v"
  proof -
    from u_in obtain g where "g ∈ G" and "q'' g ⊙ g ≠ 0" and u: "u = lt (q'' g ⊙ g)" by blast
    show ?thesis
    proof (cases "g ∈ M")
      case True
      thus ?thesis unfolding u by (rule 4)
    next
      case False
      with ‹g ∈ G› have "lt (q'' g ⊙ g) ≺⇩t v" using ‹q'' g ⊙ g ≠ 0› by (rule 5)
      thus ?thesis by (simp add: u)
    qed
  qed
  ultimately have u_v: "u = v" and "mnum q ≤ mnum q''" by simp_all
  note this(2)
  also have "mnum q'' < card M" unfolding mnum_def
  proof (rule psubset_card_mono)
    from ‹M ⊆ G› ‹finite G› show "finite M" by (rule finite_subset)
  next
    have "{g∈G. q'' g ⊙ g ≠ 0 ∧ lt (q'' g ⊙ g) = v} ⊆ M - {g1}"
    proof
      fix g
      assume "g ∈ {g∈G. q'' g ⊙ g ≠ 0 ∧ lt (q'' g ⊙ g) = v}"
      hence "g ∈ G" and "q'' g ⊙ g ≠ 0" and "lt (q'' g ⊙ g) = v" by simp_all
      with 2 5 show "g ∈ M - {g1}" by blast
    qed
    also from ‹g1 ∈ M› have "… ⊂ M" by blast
    finally show "{g∈G. q'' g ⊙ g ≠ 0 ∧ lt (q'' g ⊙ g) = mlt q''} ⊂ M"
      by (simp only: u_v flip: u_def)
  qed
  also have "… = mnum q" by (simp only: M_def mnum_def v_def)
  finally show False ..
qed

subsection ‹Replacing Elements in Gr\"obner Bases›

lemma replace_in_dgrad_p_set:
  assumes "G ⊆ dgrad_p_set d m"
  obtains n where "q ∈ dgrad_p_set d n" and "G ⊆ dgrad_p_set d n"
    and "insert q (G - {p}) ⊆ dgrad_p_set d n"
proof -
  from assms obtain n where "m ≤ n" and 1: "q ∈ dgrad_p_set d n" and 2: "G ⊆ dgrad_p_set d n"
    by (rule dgrad_p_set_insert)
  from this(2, 3) have "insert q (G - {p}) ⊆ dgrad_p_set d n" by auto
  with 1 2 show ?thesis ..
qed

lemma GB_replace_lt_adds_stable_GB_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "q ≠ 0" and q: "q ∈ (pmdl G)" and "lt q adds⇩t lt p"
  shows "is_Groebner_basis (insert q (G - {p}))" (is "is_Groebner_basis ?G'")
proof -
  from assms(2) obtain n where 1: "G ⊆ dgrad_p_set d n" and 2: "?G' ⊆ dgrad_p_set d n"
    by (rule replace_in_dgrad_p_set)
  from isGB show ?thesis unfolding GB_alt_3_dgrad_p_set[OF assms(1) 1] GB_alt_3_dgrad_p_set[OF assms(1) 2]
  proof (intro ballI impI)
    fix f
    assume f1: "f ∈ (pmdl ?G')" and "f ≠ 0"
      and a1: "∀f∈pmdl G. f ≠ 0 ⟶ (∃g∈G. g ≠ 0 ∧ lt g adds⇩t lt f)"
    from f1 pmdl.replace_span[OF q, of p] have "f ∈ pmdl G" ..
    from a1[rule_format, OF this ‹f ≠ 0›] obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt f" by auto
    show "∃g∈?G'. g ≠ 0 ∧ lt g adds⇩t lt f"
    proof (cases "g = p")
      case True
      show ?thesis
      proof
        from ‹lt q adds⇩t lt p› have "lt q adds⇩t lt g" unfolding True .
        also have "... adds⇩t lt f" by fact
        finally have "lt q adds⇩t lt f" .
        with ‹q ≠ 0› show "q ≠ 0 ∧ lt q adds⇩t lt f" ..
      next
        show "q ∈ ?G'" by simp
      qed
    next
      case False
      show ?thesis
      proof
        show "g ≠ 0 ∧ lt g adds⇩t lt f" by (rule, fact+)
      next
        from ‹g ∈ G› False show "g ∈ ?G'" by blast
      qed
    qed
  qed
qed
  
lemma GB_replace_lt_adds_stable_pmdl_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "q ≠ 0" and "q ∈ pmdl G" and "lt q adds⇩t lt p"
  shows "pmdl (insert q (G - {p})) = pmdl G" (is "pmdl ?G' = pmdl G")
proof (rule, rule pmdl.replace_span, fact, rule)
  fix f
  assume "f ∈ pmdl G"
  note assms(1)
  moreover from assms(2) obtain n where "?G' ⊆ dgrad_p_set d n" by (rule replace_in_dgrad_p_set)
  moreover have "is_Groebner_basis ?G'" by (rule GB_replace_lt_adds_stable_GB_dgrad_p_set, fact+)
  ultimately have "∃! h. (red ?G')⇧*⇧* f h ∧ ¬ is_red ?G' h" by (rule GB_implies_unique_nf_dgrad_p_set)
  then obtain h where ftoh: "(red ?G')⇧*⇧* f h" and irredh: "¬ is_red ?G' h" by auto
  have "¬ is_red G h"
  proof
    assume "is_red G h"
    have "is_red ?G' h" by (rule replace_lt_adds_stable_is_red, fact+)
    with irredh show False ..
  qed
  have "f - h ∈ pmdl ?G'" by (rule red_rtranclp_diff_in_pmdl, rule ftoh)
  have "f - h ∈ pmdl G" by (rule, fact, rule pmdl.replace_span, fact)
  from pmdl.span_diff[OF this ‹f ∈ pmdl G›] have "-h ∈ pmdl G" by simp
  from pmdl.span_neg[OF this] have "h ∈ pmdl G" by simp
  with isGB ‹¬ is_red G h› have "h = 0" using GB_imp_reducibility by auto
  with ftoh have "(red ?G')⇧*⇧* f 0" by simp
  thus "f ∈ pmdl ?G'" by (simp add: red_rtranclp_0_in_pmdl)
qed
  
lemma GB_replace_red_stable_GB_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "p ∈ G" and q: "red (G - {p}) p q"
  shows "is_Groebner_basis (insert q (G - {p}))" (is "is_Groebner_basis ?G'")
proof -
  from assms(2) obtain n where 1: "G ⊆ dgrad_p_set d n" and 2: "?G' ⊆ dgrad_p_set d n"
    by (rule replace_in_dgrad_p_set)
  from isGB show ?thesis unfolding GB_alt_2_dgrad_p_set[OF assms(1) 1] GB_alt_2_dgrad_p_set[OF assms(1) 2]
  proof (intro ballI impI)
    fix f
    assume f1: "f ∈ (pmdl ?G')" and "f ≠ 0"
      and a1: "∀f∈pmdl G. f ≠ 0 ⟶ is_red G f"
    have "q ∈ pmdl G"
    proof (rule pmdl_closed_red, rule pmdl.span_mono)
      from pmdl.span_superset ‹p ∈ G› show "p ∈ pmdl G" ..
    next
      show "G - {p} ⊆ G" by (rule Diff_subset)
    qed (rule q)
    from f1 pmdl.replace_span[OF this, of p] have "f ∈ pmdl G" ..
    have "is_red G f" by (rule a1[rule_format], fact+)
    show "is_red ?G' f" by (rule replace_red_stable_is_red, fact+)
  qed
qed

lemma GB_replace_red_stable_pmdl_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "p ∈ G" and ptoq: "red (G - {p}) p q"
  shows "pmdl (insert q (G - {p})) = pmdl G" (is "pmdl ?G' = _")
proof -
  from ‹p ∈ G› pmdl.span_superset have "p ∈ pmdl G" ..
  have "q ∈ pmdl G"
    by (rule pmdl_closed_red, rule pmdl.span_mono, rule Diff_subset, rule ‹p ∈ pmdl G›, rule ptoq)
  show ?thesis
  proof (rule, rule pmdl.replace_span, fact, rule)
    fix f
    assume "f ∈ pmdl G"
    note assms(1)
    moreover from assms(2) obtain n where "?G' ⊆ dgrad_p_set d n" by (rule replace_in_dgrad_p_set)
    moreover have "is_Groebner_basis ?G'" by (rule GB_replace_red_stable_GB_dgrad_p_set, fact+)
    ultimately have "∃! h. (red ?G')⇧*⇧* f h ∧ ¬ is_red ?G' h" by (rule GB_implies_unique_nf_dgrad_p_set)
    then obtain h where ftoh: "(red ?G')⇧*⇧* f h" and irredh: "¬ is_red ?G' h" by auto
    have "¬ is_red G h"
    proof
      assume "is_red G h"
      have "is_red ?G' h" by (rule replace_red_stable_is_red, fact+)
      with irredh show False ..
    qed
    have "f - h ∈ pmdl ?G'" by (rule red_rtranclp_diff_in_pmdl, rule ftoh)
    have "f - h ∈ pmdl G" by (rule, fact, rule pmdl.replace_span, fact)
    from pmdl.span_diff[OF this ‹f ∈ pmdl G›] have "-h ∈ pmdl G" by simp
    from pmdl.span_neg[OF this] have "h ∈ pmdl G" by simp
    with isGB ‹¬ is_red G h› have "h = 0" using GB_imp_reducibility by auto
    with ftoh have "(red ?G')⇧*⇧* f 0" by simp
    thus "f ∈ pmdl ?G'" by (simp add: red_rtranclp_0_in_pmdl)
  qed
qed
  
lemma GB_replace_red_rtranclp_stable_GB_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "p ∈ G" and ptoq: "(red (G - {p}))⇧*⇧* p q"
  shows "is_Groebner_basis (insert q (G - {p}))"
  using ptoq
proof (induct q rule: rtranclp_induct)
  case base
  from isGB ‹p ∈ G› show ?case by (simp add: insert_absorb)
next
  case (step y z)
  show ?case
  proof (cases "y = p")
    case True
    from assms(1) assms(2) isGB ‹p ∈ G› show ?thesis
    proof (rule GB_replace_red_stable_GB_dgrad_p_set)
      from ‹red (G - {p}) y z› show "red (G - {p}) p z" unfolding True .
    qed
  next
    case False
    show ?thesis
      proof (cases "y ∈ G")
        case True
        with ‹y ≠ p› have "y ∈ G - {p}" (is "_ ∈ ?G'") by blast
        hence "insert y (G - {p}) = ?G'" by auto
        with step(3) have "is_Groebner_basis ?G'" by simp
        from ‹y ∈ ?G'› pmdl.span_superset have "y ∈ pmdl ?G'" ..
        have "z ∈ pmdl ?G'" by (rule pmdl_closed_red, rule subset_refl, fact+)
        show "is_Groebner_basis (insert z ?G')" by (rule GB_insert, fact+)
      next
        case False
        from assms(2) obtain n where "insert y (G - {p}) ⊆ dgrad_p_set d n"
            by (rule replace_in_dgrad_p_set)
        from assms(1) this step(3) have "is_Groebner_basis (insert z (insert y (G - {p}) - {y}))"
        proof (rule GB_replace_red_stable_GB_dgrad_p_set)
          from ‹red (G - {p}) y z› False show "red ((insert y (G - {p})) - {y}) y z" by simp
        qed simp
        moreover from False have "... = (insert z (G - {p}))" by simp
        ultimately show ?thesis by simp
      qed
  qed
qed

lemma GB_replace_red_rtranclp_stable_pmdl_dgrad_p_set:
  assumes "dickson_grading d" and "G ⊆ dgrad_p_set d m"
  assumes isGB: "is_Groebner_basis G" and "p ∈ G" and ptoq: "(red (G - {p}))⇧*⇧* p q"
  shows "pmdl (insert q (G - {p})) = pmdl G"
  using ptoq
proof (induct q rule: rtranclp_induct)
  case base
  from ‹p ∈ G› show ?case by (simp add: insert_absorb)
next
  case (step y z)
  show ?case
  proof (cases "y = p")
    case True
    from assms(1) assms(2) isGB ‹p ∈ G› step(2) show ?thesis unfolding True
      by (rule GB_replace_red_stable_pmdl_dgrad_p_set)
  next
    case False
    have gb: "is_Groebner_basis (insert y (G - {p}))"
      by (rule GB_replace_red_rtranclp_stable_GB_dgrad_p_set, fact+)
    show ?thesis
    proof (cases "y ∈ G")
      case True
      with ‹y ≠ p› have "y ∈ G - {p}" (is "_ ∈ ?G'") by blast
      hence eq: "insert y ?G' = ?G'" by auto
      from ‹y ∈ ?G'› have "y ∈ pmdl ?G'" by (rule pmdl.span_base)
      have "z ∈ pmdl ?G'" by (rule pmdl_closed_red, rule subset_refl, fact+)
      hence "pmdl (insert z ?G') = pmdl ?G'" by (rule pmdl.span_insert_idI)
      also from step(3) have "... = pmdl G" by (simp only: eq)
      finally show ?thesis .
    next
      case False
      from assms(2) obtain n where 1: "insert y (G - {p}) ⊆ dgrad_p_set d n"
        by (rule replace_in_dgrad_p_set)
      from False have "pmdl (insert z (G - {p})) = pmdl (insert z (insert y (G - {p}) - {y}))"
        by auto
      also from assms(1) 1 gb have "... = pmdl (insert y (G - {p}))"
      proof (rule GB_replace_red_stable_pmdl_dgrad_p_set)
        from step(2) False show "red ((insert y (G - {p})) - {y}) y z" by simp
      qed simp
      also have "... = pmdl G" by fact
      finally show ?thesis .
    qed
  qed
qed

lemmas GB_replace_lt_adds_stable_GB_finite =
  GB_replace_lt_adds_stable_GB_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_replace_lt_adds_stable_pmdl_finite =
  GB_replace_lt_adds_stable_pmdl_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_replace_red_stable_GB_finite =
  GB_replace_red_stable_GB_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_replace_red_stable_pmdl_finite =
  GB_replace_red_stable_pmdl_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_replace_red_rtranclp_stable_GB_finite =
  GB_replace_red_rtranclp_stable_GB_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]
lemmas GB_replace_red_rtranclp_stable_pmdl_finite =
  GB_replace_red_rtranclp_stable_pmdl_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]

subsection ‹An Inconstructive Proof of the Existence of Finite Gr\"obner Bases›

lemma ex_finite_GB_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
  obtains G where "G ⊆ dgrad_p_set d m" and "finite G" and "is_Groebner_basis G" and "pmdl G = pmdl F"
proof -
  define S where "S = {lt f | f. f ∈ pmdl F ∧ f ∈ dgrad_p_set d m ∧ f ≠ 0}"
  note assms(1)
  moreover from _ assms(2) have "finite (component_of_term ` S)"
  proof (rule finite_subset)
    have "component_of_term ` S ⊆ component_of_term ` Keys (pmdl F)"
      by (rule image_mono, rule, auto simp add: S_def intro!: in_KeysI lt_in_keys)
    thus "component_of_term ` S ⊆ component_of_term ` Keys F" by (simp only: components_pmdl)
  qed
  moreover have "pp_of_term ` S ⊆ dgrad_set d m"
  proof
    fix s
    assume "s ∈ pp_of_term ` S"
    then obtain u where "u ∈ S" and "s = pp_of_term u" ..
    from this(1) obtain f where "f ∈ pmdl F ∧ f ∈ dgrad_p_set d m ∧ f ≠ 0" and u: "u = lt f"
      unfolding S_def by blast
    from this(1) have "f ∈ dgrad_p_set d m" and "f ≠ 0" by simp_all
    have "u ∈ keys f" unfolding u by (rule lt_in_keys, fact)
    with ‹f ∈ dgrad_p_set d m› have "d (pp_of_term u) ≤ m" unfolding u by (rule dgrad_p_setD)
    thus "s ∈ dgrad_set d m" by (simp add: ‹s = pp_of_term u› dgrad_set_def)
  qed
  ultimately obtain T where "finite T" and "T ⊆ S" and *: "⋀s. s ∈ S ⟹ (∃t∈T. t adds⇩t s)"
    by (rule ex_finite_adds_term, blast)
  define crit where "crit = (λt f. f ∈ pmdl F ∧ f ∈ dgrad_p_set d m ∧ f ≠ 0 ∧ t = lt f)"
  have ex_crit: "t ∈ T ⟹ (∃f. crit t f)" for t
  proof -
    assume "t ∈ T"
    from this ‹T ⊆ S› have "t ∈ S" ..
    then obtain f where "f ∈ pmdl F ∧ f ∈ dgrad_p_set d m ∧ f ≠ 0" and "t = lt f"
      unfolding S_def by blast
    thus "∃f. crit t f" unfolding crit_def by blast
  qed
  define G where "G = (λt. SOME g. crit t g) ` T"
  have G: "g ∈ G ⟹ g ∈ pmdl F ∧ g ∈ dgrad_p_set d m ∧ g ≠ 0" for g
  proof -
    assume "g ∈ G"
    then obtain t where "t ∈ T" and g: "g = (SOME h. crit t h)" unfolding G_def ..
    have "crit t g" unfolding g by (rule someI_ex, rule ex_crit, fact)
    thus "g ∈ pmdl F ∧ g ∈ dgrad_p_set d m ∧ g ≠ 0" by (simp add: crit_def)
  qed
  have **: "t ∈ T ⟹ (∃g∈G. lt g = t)" for t
  proof -
    assume "t ∈ T"
    define g where "g = (SOME h. crit t h)"
    from ‹t ∈ T› have "g ∈ G" unfolding g_def G_def by blast
    thus "∃g∈G. lt g = t"
    proof
      have "crit t g" unfolding g_def by (rule someI_ex, rule ex_crit, fact)
      thus "lt g = t" by (simp add: crit_def)
    qed
  qed
  have adds: "f ∈ pmdl F ⟹ f ∈ dgrad_p_set d m ⟹ f ≠ 0 ⟹ (∃g∈G. g ≠ 0 ∧ lt g adds⇩t lt f)" for f
  proof -
    assume "f ∈ pmdl F" and "f ∈ dgrad_p_set d m" and "f ≠ 0"
    hence "lt f ∈ S" unfolding S_def by blast
    hence "∃t∈T. t adds⇩t (lt f)" by (rule *)
    then obtain t where "t ∈ T" and "t adds⇩t (lt f)" ..
    from this(1) have "∃g∈G. lt g = t" by (rule **)
    then obtain g where "g ∈ G" and "lt g = t" ..
    show "∃g∈G. g ≠ 0 ∧ lt g adds⇩t lt f"
    proof (intro bexI conjI)
      from G[OF ‹g ∈ G›] show "g ≠ 0" by (elim conjE)
    next
      from ‹t adds⇩t lt f› show "lt g adds⇩t lt f" by (simp only: ‹lt g = t›)
    qed fact
  qed
  have sub1: "pmdl G ⊆ pmdl F"
  proof (rule pmdl.span_subset_spanI, rule)
    fix g
    assume "g ∈ G"
    from G[OF this] show "g ∈ pmdl F" ..
  qed
  have sub2: "G ⊆ dgrad_p_set d m"
  proof
    fix g
    assume "g ∈ G"
    from G[OF this] show "g ∈ dgrad_p_set d m" by (elim conjE)
  qed
  show ?thesis
  proof
    from ‹finite T› show "finite G" unfolding G_def ..
  next
    from assms(1) sub2 adds show "is_Groebner_basis G"
    proof (rule isGB_I_adds_lt)
      fix f
      assume "f ∈ pmdl G"
      from this sub1 show "f ∈ pmdl F" ..
    qed
  next
    show "pmdl G = pmdl F"
    proof
      show "pmdl F ⊆ pmdl G"
      proof (rule pmdl.span_subset_spanI, rule)
        fix f
        assume "f ∈ F"
        hence "f ∈ pmdl F" by (rule pmdl.span_base)
        from ‹f ∈ F› assms(3) have "f ∈ dgrad_p_set d m" ..
        with assms(1) sub2 sub1 _ ‹f ∈ pmdl F› have "(red G)⇧*⇧* f 0"
        proof (rule is_red_implies_0_red_dgrad_p_set)
          fix q
          assume "q ∈ pmdl F" and "q ∈ dgrad_p_set d m" and "q ≠ 0"
          hence "(∃g ∈ G. g ≠ 0 ∧ lt g adds⇩t lt q)" by (rule adds)
          then obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t lt q" by blast
          thus "is_red G q" using ‹q ≠ 0› is_red_indI1 by blast
        qed
        thus "f ∈ pmdl G" by (rule red_rtranclp_0_in_pmdl)
      qed
    qed fact
  next
    show "G ⊆ dgrad_p_set d m"
    proof
      fix g
      assume "g ∈ G"
      hence "g ∈ pmdl F ∧ g ∈ dgrad_p_set d m ∧ g ≠ 0" by (rule G)
      thus "g ∈ dgrad_p_set d m" by (elim conjE)
    qed
  qed
qed

text ‹The preceding lemma justifies the following definition.›

definition some_GB :: "('t ⇒⇩0 'b) set ⇒ ('t ⇒⇩0 'b::field) set"
  where "some_GB F = (SOME G. finite G ∧ is_Groebner_basis G ∧ pmdl G = pmdl F)"

lemma some_GB_props_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
  shows "finite (some_GB F) ∧ is_Groebner_basis (some_GB F) ∧ pmdl (some_GB F) = pmdl F"
proof -
  from assms obtain G where "finite G" and "is_Groebner_basis G" and "pmdl G = pmdl F"
    by (rule ex_finite_GB_dgrad_p_set)
  hence "finite G ∧ is_Groebner_basis G ∧ pmdl G = pmdl F" by simp
  thus "finite (some_GB F) ∧ is_Groebner_basis (some_GB F) ∧ pmdl (some_GB F) = pmdl F"
    unfolding some_GB_def by (rule someI)
qed

lemma finite_some_GB_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
  shows "finite (some_GB F)"
  using some_GB_props_dgrad_p_set[OF assms] ..

lemma some_GB_isGB_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
  shows "is_Groebner_basis (some_GB F)"
  using some_GB_props_dgrad_p_set[OF assms] by (elim conjE)

lemma some_GB_pmdl_dgrad_p_set:
  assumes "dickson_grading d" and "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
  shows "pmdl (some_GB F) = pmdl F"
  using some_GB_props_dgrad_p_set[OF assms] by (elim conjE)

lemma finite_imp_finite_component_Keys:
  assumes "finite F"
  shows "finite (component_of_term ` Keys F)"
  by (rule finite_imageI, rule finite_Keys, fact)

lemma finite_some_GB_finite: "finite F ⟹ finite (some_GB F)"
  by (rule finite_some_GB_dgrad_p_set, rule dickson_grading_dgrad_dummy,
      erule finite_imp_finite_component_Keys, erule dgrad_p_set_exhaust_expl)

lemma some_GB_isGB_finite: "finite F ⟹ is_Groebner_basis (some_GB F)"
  by (rule some_GB_isGB_dgrad_p_set, rule dickson_grading_dgrad_dummy,
      erule finite_imp_finite_component_Keys, erule dgrad_p_set_exhaust_expl)

lemma some_GB_pmdl_finite: "finite F ⟹ pmdl (some_GB F) = pmdl F"
  by (rule some_GB_pmdl_dgrad_p_set, rule dickson_grading_dgrad_dummy,
      erule finite_imp_finite_component_Keys, erule dgrad_p_set_exhaust_expl)

text ‹Theory ‹Buchberger› implements an algorithm for effectively computing Gr\"obner bases.›

subsection ‹Relation ‹red_supset››

text ‹The following relation is needed for proving the termination of Buchberger's algorithm (i.\,e.
  function ‹gb_schema_aux›).›

definition red_supset::"('t ⇒⇩0 'b::field) set ⇒ ('t ⇒⇩0 'b) set ⇒ bool" (infixl ‹⊐p› 50)
  where "red_supset A B ≡ (∃p. is_red A p ∧ ¬ is_red B p) ∧ (∀p. is_red B p ⟶ is_red A p)"

lemma red_supsetE:
  assumes "A ⊐p B"
  obtains p where "is_red A p" and "¬ is_red B p"
proof -
  from assms have "∃p. is_red A p ∧ ¬ is_red B p" by (simp add: red_supset_def)
  from this obtain p where "is_red A p" and " ¬ is_red B p" by auto
  thus ?thesis ..
qed

lemma red_supsetD:
  assumes a1: "A ⊐p B" and a2: "is_red B p"
  shows "is_red A p"
proof -
  from assms have "∀p. is_red B p ⟶ is_red A p" by (simp add: red_supset_def)
  hence "is_red B p ⟶ is_red A p" ..
  from a2 this show ?thesis by simp
qed

lemma red_supsetI [intro]:
  assumes "⋀q. is_red B q ⟹ is_red A q" and "is_red A p" and "¬ is_red B p"
  shows "A ⊐p B"
  unfolding red_supset_def using assms by auto

lemma red_supset_insertI:
  assumes "x ≠ 0" and "¬ is_red A x"
  shows "(insert x A) ⊐p A"
proof
  fix q
  assume "is_red A q"
  thus "is_red (insert x A) q" unfolding is_red_alt
  proof
    fix a
    assume "red A q a"
    from red_unionI2[OF this, of "{x}"] have "red (insert x A) q a" by simp
    show "∃qa. red (insert x A) q qa"
    proof
      show "red (insert x A) q a" by fact
    qed
  qed
next
  show "is_red (insert x A) x" unfolding is_red_alt
  proof
    from red_unionI1[OF red_self[OF ‹x ≠ 0›], of A] show "red (insert x A) x 0" by simp
  qed
next
  show "¬ is_red A x" by fact
qed

lemma red_supset_transitive:
  assumes "A ⊐p B" and "B ⊐p C"
  shows "A ⊐p C"
proof -
  from assms(2) obtain p where "is_red B p" and "¬ is_red C p" by (rule red_supsetE)
  show ?thesis
  proof
    fix q
    assume "is_red C q"
    with assms(2) have "is_red B q" by (rule red_supsetD)
    with assms(1) show "is_red A q" by (rule red_supsetD)
  next
    from assms(1) ‹is_red B p› show "is_red A p" by (rule red_supsetD)
  qed fact
qed

lemma red_supset_wf_on:
  assumes "dickson_grading d" and "finite K"
  shows "wfp_on (⊐p) (Pow (dgrad_p_set d m) ∩ {F. component_of_term ` Keys F ⊆ K})"
proof (rule wfp_onI_chain, rule, erule exE)
  let ?A = "dgrad_p_set d m"
  fix f::"nat ⇒ (('t ⇒⇩0 'b) set)"
  assume "∀i. f i ∈ Pow ?A ∩ {F. component_of_term ` Keys F ⊆ K} ∧ f (Suc i) ⊐p f i"
  hence a1_subset: "f i ⊆ ?A" and comp_sub: "component_of_term ` Keys (f i) ⊆ K"
    and a1: "f (Suc i) ⊐p f i" for i by simp_all

  have a1_trans: "i < j ⟹ f j ⊐p f i" for i j
  proof -
    assume "i < j"
    thus "f j ⊐p f i"
    proof (induct j)
      case 0
      thus ?case by simp
    next
      case (Suc j)
      from Suc(2) have "i = j ∨ i < j" by auto
      thus ?case
      proof
        assume "i = j"
        show ?thesis unfolding ‹i = j› by (fact a1)
      next
        assume "i < j"
        from a1 have "f (Suc j) ⊐p f j" .
        also from ‹i < j› have "... ⊐p f i" by (rule Suc(1))
        finally(red_supset_transitive) show ?thesis .
      qed
    qed
  qed

  have a2: "∃p ∈ f (Suc i). ∃q. is_red {p} q ∧ ¬ is_red (f i) q" for i
  proof -
    from a1 have "f (Suc i) ⊐p f i" .
    then obtain q where red: "is_red (f (Suc i)) q" and irred: "¬ is_red (f i) q"
      by (rule red_supsetE)
    from red obtain p where "p ∈ f (Suc i)" and "is_red {p} q" by (rule is_red_singletonI)
    show "∃p∈f (Suc i). ∃q. is_red {p} q ∧ ¬ is_red (f i) q"
    proof
      show "∃q. is_red {p} q ∧ ¬ is_red (f i) q"
      proof (intro exI, intro conjI)
        show "is_red {p} q" by fact
      qed (fact)
    next
      show "p ∈ f (Suc i)" by fact
    qed
  qed

  let ?P = "λi p. p ∈ (f (Suc i)) ∧ (∃q. is_red {p} q ∧ ¬ is_red (f i) q)"
  define g where "g ≡ λi::nat. (SOME p. ?P i p)"
  have a3: "?P i (g i)" for i
  proof -
    from a2[of i] obtain gi where "gi ∈ f (Suc i)" and "∃q. is_red {gi} q ∧ ¬ is_red (f i) q" ..
    show ?thesis unfolding g_def by (rule someI[of _ gi], intro conjI, fact+)
  qed

  have a4: "i < j ⟹ ¬ lt (g i) adds⇩t (lt (g j))" for i j
  proof
    assume "i < j" and adds: "lt (g i) adds⇩t lt (g j)"
    from a3 have "∃q. is_red {g j} q ∧ ¬ is_red (f j) q" ..
    then obtain q where redj: "is_red {g j} q" and "¬ is_red (f j) q" by auto
    have *: "¬ is_red (f (Suc i)) q"
    proof -
      from ‹i < j› have "i + 1 < j ∨ i + 1 = j" by auto
      thus ?thesis
      proof
        assume "i + 1 < j"
        from red_supsetD[OF a1_trans[rule_format, OF this], of q] ‹¬ is_red (f j) q›
          show ?thesis by auto
      next
        assume "i + 1 = j"
        thus ?thesis using ‹¬ is_red (f j) q› by simp
      qed
    qed
    from a3 have "g i ∈ f (i + 1)" and redi: "∃q. is_red {g i} q ∧ ¬ is_red (f i) q" by simp_all
    have "¬ is_red {g i} q"
    proof
      assume "is_red {g i} q"
      from is_red_singletonD[OF this ‹g i ∈ f (i + 1)›] * show False by simp
    qed
    have "g i ≠ 0"
    proof -
      from redi obtain q0 where "is_red {g i} q0" by auto
      from is_red_singleton_not_0[OF this] show ?thesis .
    qed
    from ‹¬ is_red {g i} q› is_red_singleton_trans[OF redj adds ‹g i ≠ 0›] show False by simp
  qed

  from _ assms(2) have a5: "finite (component_of_term ` range (lt ∘ g))"
  proof (rule finite_subset)
    show "component_of_term ` range (lt ∘ g) ⊆ K"
    proof (rule, elim imageE, simp)
      fix i
      from a3 have "g i ∈ f (Suc i)" and "∃q. is_red {g i} q ∧ ¬ is_red (f i) q" by simp_all
      from this(2) obtain q where "is_red {g i} q" by auto
      hence "g i ≠ 0" by (rule is_red_singleton_not_0)
      hence "lt (g i) ∈ keys (g i)" by (rule lt_in_keys)
      hence "component_of_term (lt (g i)) ∈ component_of_term ` keys (g i)" by simp
      also have "... ⊆ component_of_term ` Keys (f (Suc i))"
        by (rule image_mono, rule keys_subset_Keys, fact)
      also have "... ⊆ K" by (fact comp_sub)
      finally show "component_of_term (lt (g i)) ∈ K" .
    qed
  qed

  have a6: "pp_of_term ` range (lt ∘ g) ⊆ dgrad_set d m"
  proof (rule, elim imageE, simp)
    fix i
    from a3 have "g i ∈ f (Suc i)" and "∃q. is_red {g i} q ∧ ¬ is_red (f i) q" by simp_all
    from this(2) obtain q where "is_red {g i} q" by auto
    hence "g i ≠ 0" by (rule is_red_singleton_not_0)
    from a1_subset ‹g i ∈ f (Suc i)› have "g i ∈ ?A" ..
    from this ‹g i ≠ 0› have "d (lp (g i)) ≤ m" by (rule dgrad_p_setD_lp)
    thus "lp (g i) ∈ dgrad_set d m" by (rule dgrad_setI)
  qed

  from assms(1) a5 a6 obtain i j where "i < j" and "(lt ∘ g) i adds⇩t (lt ∘ g) j" by (rule Dickson_termE)
  from this a4[OF ‹i < j›] show False by simp
qed

end (* gd_term *)

lemma in_lex_prod_alt:
  "(x, y) ∈ r <*lex*> s ⟷ (((fst x), (fst y)) ∈ r ∨ (fst x = fst y ∧ ((snd x), (snd y)) ∈ s))"
  by (metis in_lex_prod prod.collapse prod.inject surj_pair)

subsection ‹Context @{locale od_term}›

context od_term
begin

lemmas red_wf = red_wf_dgrad_p_set[OF dickson_grading_zero subset_dgrad_p_set_zero]
lemmas Buchberger_criterion = Buchberger_criterion_dgrad_p_set[OF dickson_grading_zero subset_dgrad_p_set_zero]

end (* od_term *)

end (* theory *)