Theory Groebner_Bases
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
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'" .
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
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
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
end