Theory Monomial_Module
section ‹Monomial Modules›
theory Monomial_Module
imports Groebner_Bases.Reduced_GB
begin
text ‹Properties of modules generated by sets of monomials, and (reduced) Gr\"obner bases thereof.›
subsection ‹Sets of Monomials›
definition is_monomial_set :: "('a ⇒⇩0 'b::zero) set ⇒ bool"
where "is_monomial_set A ⟷ (∀p∈A. is_monomial p)"
lemma is_monomial_setI: "(⋀p. p ∈ A ⟹ is_monomial p) ⟹ is_monomial_set A"
by (simp add: is_monomial_set_def)
lemma is_monomial_setD: "is_monomial_set A ⟹ p ∈ A ⟹ is_monomial p"
by (simp add: is_monomial_set_def)
lemma is_monomial_set_subset: "is_monomial_set B ⟹ A ⊆ B ⟹ is_monomial_set A"
by (auto simp: is_monomial_set_def)
lemma is_monomial_set_Un: "is_monomial_set (A ∪ B) ⟷ (is_monomial_set A ∧ is_monomial_set B)"
by (auto simp: is_monomial_set_def)
subsection ‹Modules›
context term_powerprod
begin
lemma monomial_pmdl:
assumes "is_monomial_set B" and "p ∈ pmdl B"
shows "monomial (lookup p v) v ∈ pmdl B"
using assms(2)
proof (induct p rule: pmdl_induct)
case base: module_0
show ?case by (simp add: pmdl.span_zero)
next
case step: (module_plus p b c t)
have eq: "monomial (lookup (p + monom_mult c t b) v) v =
monomial (lookup p v) v + monomial (lookup (monom_mult c t b) v) v"
by (simp only: single_add lookup_add)
from assms(1) step.hyps(3) have "is_monomial b" by (rule is_monomial_setD)
then obtain d u where b: "b = monomial d u" by (rule is_monomial_monomial)
have "monomial (lookup (monom_mult c t b) v) v ∈ pmdl B"
proof (simp add: b monom_mult_monomial lookup_single when_def pmdl.span_zero, intro impI)
assume "t ⊕ u = v"
hence "monomial (c * d) v = monom_mult c t b" by (simp add: b monom_mult_monomial)
also from step.hyps(3) have "… ∈ pmdl B" by (rule monom_mult_in_pmdl)
finally show "monomial (c * d) v ∈ pmdl B" .
qed
with step.hyps(2) show ?case unfolding eq by (rule pmdl.span_add)
qed
lemma monomial_pmdl_field:
assumes "is_monomial_set B" and "p ∈ pmdl B" and "v ∈ keys (p::_ ⇒⇩0 'b::field)"
shows "monomial c v ∈ pmdl B"
proof -
from assms(1, 2) have "monomial (lookup p v) v ∈ pmdl B" by (rule monomial_pmdl)
hence "monom_mult (c / lookup p v) 0 (monomial (lookup p v) v) ∈ pmdl B"
by (rule pmdl_closed_monom_mult)
with assms(3) show ?thesis by (simp add: monom_mult_monomial splus_zero in_keys_iff)
qed
end
context ordered_term
begin
lemma keys_monomial_pmdl:
assumes "is_monomial_set F" and "p ∈ pmdl F" and "t ∈ keys p"
obtains f where "f ∈ F" and "f ≠ 0" and "lt f adds⇩t t"
using assms(2) assms(3)
proof (induct arbitrary: thesis rule: pmdl_induct)
case module_0
from this(2) show ?case by simp
next
case step: (module_plus p f0 c s)
from assms(1) step(3) have "is_monomial f0" unfolding is_monomial_set_def ..
hence "keys f0 = {lt f0}" and "f0 ≠ 0" by (rule keys_monomial, rule monomial_not_0)
from Poly_Mapping.keys_add step(6) have "t ∈ keys p ∪ keys (monom_mult c s f0)" ..
thus ?case
proof
assume "t ∈ keys p"
from step(2)[OF _ this] obtain f where "f ∈ F" and "f ≠ 0" and "lt f adds⇩t t" by blast
thus ?thesis by (rule step(5))
next
assume "t ∈ keys (monom_mult c s f0)"
with keys_monom_mult_subset have "t ∈ (⊕) s ` keys f0" ..
hence "t = s ⊕ lt f0" by (simp add: ‹keys f0 = {lt f0}›)
hence "lt f0 adds⇩t t" by (simp add: term_simps)
with ‹f0 ∈ F› ‹f0 ≠ 0› show ?thesis by (rule step(5))
qed
qed
lemma image_lt_monomial_lt: "lt ` monomial (1::'b::zero_neq_one) ` lt ` F = lt ` F"
by (auto simp: lt_monomial intro!: image_eqI)
subsection ‹Reduction›
lemma red_setE2:
assumes "red B p q"
obtains b where "b ∈ B" and "b ≠ 0" and "red {b} p q"
proof -
from assms obtain b t where "b ∈ B" and "red_single p q b t" by (rule red_setE)
from this(2) have "b ≠ 0" by (simp add: red_single_def)
have "red {b} p q" by (rule red_setI, simp, fact)
show ?thesis by (rule, fact+)
qed
lemma red_monomial_keys:
assumes "is_monomial r" and "red {r} p q"
shows "card (keys p) = Suc (card (keys q))"
proof -
from assms(2) obtain s where rs: "red_single p q r s" unfolding red_singleton ..
hence cp0: "lookup p (s ⊕ lt r) ≠ 0" and q_def0: "q = p - monom_mult (lookup p (s ⊕ lt r) / lc r) s r"
unfolding red_single_def by simp_all
from assms(1) obtain c t where "c ≠ 0" and r_def: "r = monomial c t" by (rule is_monomial_monomial)
have ltr: "lt r = t" unfolding r_def by (rule lt_monomial, fact)
have lcr: "lc r = c" unfolding r_def by (rule lc_monomial)
define u where "u = s ⊕ t"
from q_def0 have "q = p - monom_mult (lookup p u / c) s r" unfolding u_def ltr lcr .
also have "... = p - monomial ((lookup p u / c) * c) u" unfolding u_def r_def monom_mult_monomial ..
finally have q_def: "q = p - monomial (lookup p u) u" using ‹c ≠ 0› by simp
from cp0 have "lookup p u ≠ 0" unfolding u_def ltr .
hence "u ∈ keys p" by (simp add: in_keys_iff)
have "keys q = keys p - {u}" unfolding q_def
proof (rule, rule)
fix x
assume "x ∈ keys (p - monomial (lookup p u) u)"
hence "lookup (p - monomial (lookup p u) u) x ≠ 0" by (simp add: in_keys_iff)
hence a: "lookup p x - lookup (monomial (lookup p u) u) x ≠ 0" unfolding lookup_minus .
hence "x ≠ u" unfolding lookup_single by auto
with a have "lookup p x ≠ 0" unfolding lookup_single by auto
show "x ∈ keys p - {u}"
proof
from ‹lookup p x ≠ 0› show "x ∈ keys p" by (simp add: in_keys_iff)
next
from ‹x ≠ u› show "x ∉ {u}" by simp
qed
next
show "keys p - {u} ⊆ keys (p - monomial (lookup p u) u)"
proof
fix x
assume "x ∈ keys p - {u}"
hence "x ∈ keys p" and "x ≠ u" by auto
from ‹x ∈ keys p› have "lookup p x ≠ 0" by (simp add: in_keys_iff)
with ‹x ≠ u› have "lookup (p - monomial (lookup p u) u) x ≠ 0" by (simp add: lookup_minus lookup_single)
thus "x ∈ keys (p - monomial (lookup p u) u)" by (simp add: in_keys_iff)
qed
qed
have "Suc (card (keys q)) = card (keys p)" unfolding ‹keys q = keys p - {u}›
by (rule card_Suc_Diff1, rule finite_keys, fact)
thus ?thesis by simp
qed
lemma red_monomial_monomial_setD:
assumes "is_monomial p" and "is_monomial_set B" and "red B p q"
shows "q = 0"
proof -
from assms(3) obtain b where "b ∈ B" and "b ≠ 0" and *: "red {b} p q" by (rule red_setE2)
from assms(2) this(1) have "is_monomial b" by (rule is_monomial_setD)
hence "card (keys p) = Suc (card (keys q))" using * by (rule red_monomial_keys)
with assms(1) show ?thesis by (simp add: is_monomial_def)
qed
corollary is_red_monomial_monomial_setD:
assumes "is_monomial p" and "is_monomial_set B" and "is_red B p"
shows "red B p 0"
proof -
from assms(3) obtain q where "red B p q" by (rule is_redE)
moreover from assms(1, 2) this have "q = 0" by (rule red_monomial_monomial_setD)
ultimately show ?thesis by simp
qed
corollary is_red_monomial_monomial_set_in_pmdl:
"is_monomial p ⟹ is_monomial_set B ⟹ is_red B p ⟹ p ∈ pmdl B"
by (intro red_rtranclp_0_in_pmdl r_into_rtranclp is_red_monomial_monomial_setD)
corollary red_rtrancl_monomial_monomial_set_cases:
assumes "is_monomial p" and "is_monomial_set B" and "(red B)⇧*⇧* p q"
obtains "q = p" | "q = 0"
using assms(3)
proof (induct q arbitrary: thesis rule: rtranclp_induct)
case base
from refl show ?case by (rule base)
next
case (step y z)
show ?case
proof (rule step.hyps)
assume "y = p"
with step.hyps(2) have "red B p z" by simp
with assms(1, 2) have "z = 0" by (rule red_monomial_monomial_setD)
thus ?thesis by (rule step.prems)
next
assume "y = 0"
from step.hyps(2) have "is_red B 0" unfolding ‹y = 0› by (rule is_redI)
with irred_0 show ?thesis ..
qed
qed
lemma is_red_monomial_lt:
assumes "0 ∉ B"
shows "is_red (monomial (1::'b::field) ` lt ` B) = is_red B"
proof
fix p
let ?B = "monomial (1::'b) ` lt ` B"
show "is_red ?B p ⟷ is_red B p"
proof
assume "is_red ?B p"
then obtain f v where "f ∈ ?B" and "v ∈ keys p" and adds: "lt f adds⇩t v" by (rule is_red_addsE)
from this(1) have "lt f ∈ lt ` ?B" by (rule imageI)
also have "… = lt ` B" by (fact image_lt_monomial_lt)
finally obtain b where "b ∈ B" and eq: "lt f = lt b" ..
note this(1)
moreover from this assms have "b ≠ 0" by blast
moreover note ‹v ∈ keys p›
moreover from adds have "lt b adds⇩t v" by (simp only: eq)
ultimately show "is_red B p" by (rule is_red_addsI)
next
assume "is_red B p"
then obtain b v where "b ∈ B" and "v ∈ keys p" and adds: "lt b adds⇩t v" by (rule is_red_addsE)
from this(1) have "lt b ∈ lt ` B" by (rule imageI)
also from image_lt_monomial_lt have "… = lt ` ?B" by (rule sym)
finally obtain f where "f ∈ ?B" and eq: "lt b = lt f" ..
note this(1)
moreover from this have "f ≠ 0" by (auto simp: monomial_0_iff)
moreover note ‹v ∈ keys p›
moreover from adds have "lt f adds⇩t v" by (simp only: eq)
ultimately show "is_red ?B p" by (rule is_red_addsI)
qed
qed
end
subsection ‹Gr\"obner Bases›
context gd_term
begin
lemma monomial_set_is_GB:
assumes "is_monomial_set G"
shows "is_Groebner_basis G"
unfolding GB_alt_1
proof
fix f
assume "f ∈ pmdl G"
thus "(red G)⇧*⇧* f 0"
proof (induct f rule: poly_mapping_plus_induct)
case 1
show ?case ..
next
case (2 f c t)
let ?f = "monomial c t + f"
from 2(1) have "t ∈ keys (monomial c t)" by simp
from this 2(2) have "t ∈ keys ?f" by (rule in_keys_plusI1)
with assms ‹?f ∈ pmdl G› obtain g where "g ∈ G" and "g ≠ 0" and "lt g adds⇩t t"
by (rule keys_monomial_pmdl)
from this(1) have "red G ?f f"
proof (rule red_setI)
from ‹lt g adds⇩t t› have "component_of_term (lt g) = component_of_term t" and "lp g adds pp_of_term t"
by (simp_all add: adds_term_def)
from this have eq: "(pp_of_term t - lp g) ⊕ lt g = t"
by (simp add: adds_minus splus_def term_of_pair_pair)
moreover from 2(2) have "lookup ?f t = c" by (simp add: lookup_add in_keys_iff)
ultimately show "red_single (monomial c t + f) f g (pp_of_term t - lp g)"
proof (simp add: red_single_def ‹g ≠ 0› ‹t ∈ keys ?f› 2(1))
from ‹g ≠ 0› have "lc g ≠ 0" by (rule lc_not_0)
hence "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) (monomial (lc g) (lt g))"
by (simp add: monom_mult_monomial eq)
moreover from assms ‹g ∈ G› have "is_monomial g" unfolding is_monomial_set_def ..
ultimately show "monomial c t = monom_mult (c / lc g) (pp_of_term t - lp g) g"
by (simp only: monomial_eq_itself)
qed
qed
have "f ∈ pmdl G" by (rule pmdl_closed_red, fact subset_refl, fact+)
hence "(red G)⇧*⇧* f 0" by (rule 2(3))
with ‹red G ?f f› show ?case by simp
qed
qed
context
fixes d
assumes dgrad: "dickson_grading (d::'a ⇒ nat)"
begin
context
fixes F m
assumes fin_comps: "finite (component_of_term ` Keys F)"
and F_sub: "F ⊆ dgrad_p_set d m"
and F_monom: "is_monomial_set (F::(_ ⇒⇩0 'b::field) set)"
begin
text ‹The proof of the following lemma could be simplified, analogous to homogeneous ideals.›
lemma reduced_GB_subset_monic_dgrad_p_set: "reduced_GB F ⊆ monic ` F"
proof -
from subset_refl obtain F' where "F' ⊆ F - {0}" and "lt ` (F - {0}) = lt ` F'" and "inj_on lt F'"
by (rule subset_imageE_inj)
define G where "G = {f ∈ F'. ∀f'∈F'. lt f' adds⇩t lt f ⟶ f' = f}"
have "G ⊆ F'" by (simp add: G_def)
hence "G ⊆ F - {0}" using ‹F' ⊆ F - {0}› by (rule subset_trans)
also have "… ⊆ F" by blast
finally have "G ⊆ F" .
have 1: thesis if "f ∈ F" and "f ≠ 0" and "⋀g. g ∈ G ⟹ lt g adds⇩t lt f ⟹ thesis" for thesis f
proof -
let ?K = "component_of_term ` Keys F"
let ?A = "{t. pp_of_term t ∈ dgrad_set d m ∧ component_of_term t ∈ ?K}"
let ?Q = "{f' ∈ F'. lt f' adds⇩t lt f}"
from dgrad fin_comps have "almost_full_on (adds⇩t) ?A" by (rule Dickson_term)
moreover have "transp_on ?A (adds⇩t)" by (auto intro: transp_onI dest: adds_term_trans)
ultimately have "wfp_on (strict (adds⇩t)) ?A" by (rule af_trans_imp_wf)
moreover have "lt f ∈ lt ` ?Q"
proof -
from that(1, 2) have "f ∈ F - {0}" by simp
hence "lt f ∈ lt ` (F - {0})" by (rule imageI)
also have "… = lt ` F'" by fact
finally have "lt f ∈ lt ` F'" .
with adds_term_refl show ?thesis by fastforce
qed
moreover have "lt ` ?Q ⊆ ?A"
proof
fix s
assume "s ∈ lt ` ?Q"
then obtain q where "q ∈ ?Q" and s: "s = lt q" ..
from this(1) have "q ∈ F'" by simp
hence "q ∈ F - {0}" using ‹F' ⊆ F - {0}› ..
hence "q ∈ F" and "q ≠ 0" by simp_all
from this(1) F_sub have "q ∈ dgrad_p_set d m" ..
from ‹q ≠ 0› have "lt q ∈ keys q" by (rule lt_in_keys)
hence "pp_of_term (lt q) ∈ pp_of_term ` keys q" by (rule imageI)
also from ‹q ∈ dgrad_p_set d m› have "… ⊆ dgrad_set d m" by (simp add: dgrad_p_set_def)
finally have 1: "pp_of_term s ∈ dgrad_set d m" by (simp only: s)
from ‹lt q ∈ keys q› ‹q ∈ F› have "lt q ∈ Keys F" by (rule in_KeysI)
hence "component_of_term s ∈ ?K" unfolding s by (rule imageI)
with 1 show "s ∈ ?A" by simp
qed
ultimately obtain t where "t ∈ lt ` ?Q" and t_min: "⋀s. strict (adds⇩t) s t ⟹ s ∉ lt ` ?Q"
by (rule wfp_onE_min) blast
from this(1) obtain g where "g ∈ ?Q" and t: "t = lt g" ..
from this(1) have "g ∈ F'" and adds: "lt g adds⇩t lt f" by simp_all
show ?thesis
proof (rule that)
{
fix f'
assume "f' ∈ F'"
assume "lt f' adds⇩t lt g"
hence "lt f' adds⇩t lt f" using adds by (rule adds_term_trans)
with ‹f' ∈ F'› have "f' ∈ ?Q" by simp
hence "lt f' ∈ lt ` ?Q" by (rule imageI)
with t_min have "¬ strict (adds⇩t) (lt f') (lt g)" unfolding t by blast
with ‹lt f' adds⇩t lt g› have "lt g adds⇩t lt f'" by blast
with ‹lt f' adds⇩t lt g› have "lt f' = lt g" by (rule adds_term_antisym)
with ‹inj_on lt F'› have "f' = g" using ‹f' ∈ F'› ‹g ∈ F'› by (rule inj_onD)
}
with ‹g ∈ F'› show "g ∈ G" by (simp add: G_def)
qed fact
qed
have 2: "is_red G q" if "q ∈ pmdl F" and "q ≠ 0" for q
proof -
from that(2) have "keys q ≠ {}" by simp
then obtain t where "t ∈ keys q" by blast
with F_monom that(1) obtain f where "f ∈ F" and "f ≠ 0" and *: "lt f adds⇩t t"
by (rule keys_monomial_pmdl)
from this(1, 2) obtain g where "g ∈ G" and "lt g adds⇩t lt f" by (rule 1)
from this(2) have **: "lt g adds⇩t t" using * by (rule adds_term_trans)
from ‹g ∈ G› ‹G ⊆ F - {0}› have "g ∈ F - {0}" ..
hence "g ≠ 0" by simp
with ‹g ∈ G› show ?thesis using ‹t ∈ keys q› ** by (rule is_red_addsI)
qed
from ‹G ⊆ F - {0}› have "G ⊆ F" by blast
hence "pmdl G ⊆ pmdl F" by (rule pmdl.span_mono)
note dgrad fin_comps F_sub
moreover have "is_reduced_GB (monic ` G)" unfolding is_reduced_GB_def GB_image_monic
proof (intro conjI image_monic_is_auto_reduced image_monic_is_monic_set)
from dgrad show "is_Groebner_basis G"
proof (rule isGB_I_is_red)
from ‹G ⊆ F› F_sub show "G ⊆ dgrad_p_set d m" by (rule subset_trans)
next
fix f
assume "f ∈ pmdl G"
hence "f ∈ pmdl F" using ‹pmdl G ⊆ pmdl F› ..
moreover assume "f ≠ 0"
ultimately show "is_red G f" by (rule 2)
qed
next
show "is_auto_reduced G" unfolding is_auto_reduced_def
proof (intro ballI notI)
fix g
assume "g ∈ G"
hence "g ∈ F" using ‹G ⊆ F› ..
with F_monom have "is_monomial g" by (rule is_monomial_setD)
hence keys_g: "keys g = {lt g}" by (rule keys_monomial)
assume "is_red (G - {g}) g"
then obtain g' t where "g' ∈ G - {g}" and "t ∈ keys g" and adds: "lt g' adds⇩t t" by (rule is_red_addsE)
from this(1) have "g' ∈ F'" and "g' ≠ g" by (simp_all add: G_def)
from ‹t ∈ keys g› have "t = lt g" by (simp add: keys_g)
with ‹g ∈ G› ‹g' ∈ F'› adds have "g' = g" by (simp add: G_def)
with ‹g' ≠ g› show False ..
qed
next
show "0 ∉ monic ` G"
proof
assume "0 ∈ monic ` G"
then obtain g where "0 = monic g" and "g ∈ G" ..
moreover from this(2) ‹G ⊆ F - {0}› have "g ≠ 0" by blast
ultimately show False by (simp add: monic_0_iff)
qed
qed
moreover have "pmdl (monic ` G) = pmdl F" unfolding pmdl_image_monic
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)
note dgrad
moreover from ‹G ⊆ F› F_sub have "G ⊆ dgrad_p_set d m" by (rule subset_trans)
moreover note ‹pmdl G ⊆ pmdl F› 2 ‹f ∈ pmdl F›
moreover from ‹f ∈ F› F_sub have "f ∈ dgrad_p_set d m" ..
ultimately have "(red G)⇧*⇧* f 0" by (rule is_red_implies_0_red_dgrad_p_set)
thus "f ∈ pmdl G" by (rule red_rtranclp_0_in_pmdl)
qed
qed fact
ultimately have "reduced_GB F = monic ` G" by (rule reduced_GB_unique_dgrad_p_set)
also from ‹G ⊆ F› have "… ⊆ monic ` F" by (rule image_mono)
finally show ?thesis .
qed
corollary reduced_GB_is_monomial_set_dgrad_p_set: "is_monomial_set (reduced_GB F)"
proof (rule is_monomial_setI)
fix g
assume "g ∈ reduced_GB F"
also have "… ⊆ monic ` F" by (fact reduced_GB_subset_monic_dgrad_p_set)
finally obtain f where "f ∈ F" and g: "g = monic f" ..
from F_monom this(1) have "is_monomial f" by (rule is_monomial_setD)
hence "card (keys f) = 1" by (simp only: is_monomial_def)
hence "f ≠ 0" by auto
hence "lc f ≠ 0" by (rule lc_not_0)
hence "1 / lc f ≠ 0" by simp
hence "keys g = (⊕) 0 ` keys f" by (simp add: keys_monom_mult monic_def g)
also from refl have "… = (λx. x) ` keys f" by (rule image_cong) (simp only: splus_zero)
finally show "is_monomial g" using ‹card (keys f) = 1› by (simp only: is_monomial_def image_ident)
qed
end
lemma is_red_reduced_GB_monomial_dgrad_set:
assumes "finite (component_of_term ` S)" and "pp_of_term ` S ⊆ dgrad_set d m"
shows "is_red (reduced_GB (monomial 1 ` S)) = is_red (monomial (1::'b::field) ` S)"
proof
fix p
let ?F = "monomial (1::'b) ` S"
from assms(1) have 1: "finite (component_of_term ` Keys ?F)" by (simp add: Keys_def)
moreover from assms(2) have 2: "?F ⊆ dgrad_p_set d m" by (auto simp: dgrad_p_set_def)
moreover have "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial)
ultimately have "reduced_GB ?F ⊆ monic ` ?F" by (rule reduced_GB_subset_monic_dgrad_p_set)
also have "… = ?F" by (auto simp: monic_def intro!: image_eqI)
finally have 3: "reduced_GB ?F ⊆ ?F" .
show "is_red (reduced_GB ?F) p ⟷ is_red ?F p"
proof
assume "is_red (reduced_GB ?F) p"
thus "is_red ?F p" using 3 by (rule is_red_subset)
next
assume "is_red ?F p"
then obtain f v where "f ∈ ?F" and "v ∈ keys p" and "f ≠ 0" and adds1: "lt f adds⇩t v"
by (rule is_red_addsE)
from this(1) have "f ∈ pmdl ?F" by (rule pmdl.span_base)
from dgrad 1 2 have "is_Groebner_basis (reduced_GB ?F)" by (rule reduced_GB_is_GB_dgrad_p_set)
moreover from ‹f ∈ pmdl ?F› dgrad 1 2 have "f ∈ pmdl (reduced_GB ?F)"
by (simp only: reduced_GB_pmdl_dgrad_p_set)
ultimately obtain g where "g ∈ reduced_GB ?F" and "g ≠ 0" and "lt g adds⇩t lt f"
using ‹f ≠ 0› by (rule GB_adds_lt)
from this(3) adds1 have "lt g adds⇩t v" by (rule adds_term_trans)
with ‹g ∈ reduced_GB ?F› ‹g ≠ 0› ‹v ∈ keys p› show "is_red (reduced_GB ?F) p"
by (rule is_red_addsI)
qed
qed
corollary is_red_reduced_GB_monomial_lt_GB_dgrad_p_set:
assumes "finite (component_of_term ` Keys G)" and "G ⊆ dgrad_p_set d m" and "0 ∉ G"
shows "is_red (reduced_GB (monomial (1::'b::field) ` lt ` G)) = is_red G"
proof -
let ?S = "lt ` G"
let ?G = "monomial (1::'b) ` ?S"
from assms(3) have "?S ⊆ Keys G" by (auto intro: lt_in_keys in_KeysI)
hence "component_of_term ` ?S ⊆ component_of_term ` Keys G"
and *: "pp_of_term ` ?S ⊆ pp_of_term ` Keys G" by (rule image_mono)+
from this(1) have "finite (component_of_term ` ?S)" using assms(1) by (rule finite_subset)
moreover from * have "pp_of_term ` ?S ⊆ dgrad_set d m"
proof (rule subset_trans)
from assms(2) show "pp_of_term ` Keys G ⊆ dgrad_set d m" by (auto simp: dgrad_p_set_def Keys_def)
qed
ultimately have "is_red (reduced_GB ?G) = is_red ?G" by (rule is_red_reduced_GB_monomial_dgrad_set)
also from assms(3) have "… = is_red G" by (rule is_red_monomial_lt)
finally show ?thesis .
qed
lemma reduced_GB_monomial_lt_reduced_GB_dgrad_p_set:
assumes "finite (component_of_term ` Keys F)" and "F ⊆ dgrad_p_set d m"
shows "reduced_GB (monomial 1 ` lt ` reduced_GB F) = monomial (1::'b::field) ` lt ` reduced_GB F"
proof (rule reduced_GB_unique)
let ?G = "reduced_GB F"
let ?F = "monomial (1::'b) ` lt ` ?G"
from dgrad assms have "0 ∉ ?G" and ar: "is_auto_reduced ?G" and "finite ?G"
by (rule reduced_GB_nonzero_dgrad_p_set, rule reduced_GB_is_auto_reduced_dgrad_p_set,
rule finite_reduced_GB_dgrad_p_set)
from this(3) show "finite ?F" by (intro finite_imageI)
show "is_reduced_GB ?F" unfolding is_reduced_GB_def
proof (intro conjI monomial_set_is_GB)
show "is_monomial_set ?F" by (auto intro!: is_monomial_setI monomial_is_monomial)
next
show "is_monic_set ?F" by (simp add: is_monic_set_def)
next
show "0 ∉ ?F" by (auto simp: monomial_0_iff)
next
show "is_auto_reduced ?F" unfolding is_auto_reduced_def
proof (intro ballI notI)
fix f
assume "f ∈ ?F"
then obtain g where "g ∈ ?G" and f: "f = monomial 1 (lt g)" by blast
assume "is_red (?F - {f}) f"
then obtain f' v where "f' ∈ ?F - {f}" and "v ∈ keys f" and "f' ≠ 0" and adds1: "lt f' adds⇩t v"
by (rule is_red_addsE)
from this(1) have "f' ∈ ?F" and "f' ≠ f" by simp_all
from this(1) obtain g' where "g' ∈ ?G" and f': "f' = monomial 1 (lt g')" by blast
from ‹v ∈ keys f› have v: "v = lt g" by (simp add: f)
from ar ‹g ∈ ?G› have "¬ is_red (?G - {g}) g" by (rule is_auto_reducedD)
moreover have "is_red (?G - {g}) g"
proof (rule is_red_addsI)
from ‹g' ∈ ?G› ‹f' ≠ f› show "g' ∈ ?G - {g}" by (auto simp: f f')
next
from ‹g' ∈ ?G› ‹0 ∉ ?G› show "g' ≠ 0" by blast
next
from ‹g ∈ ?G› ‹0 ∉ ?G› have "g ≠ 0" by blast
thus "lt g ∈ keys g" by (rule lt_in_keys)
next
from adds1 show adds2: "lt g' adds⇩t lt g" by (simp add: v f' lt_monomial)
qed
ultimately show False ..
qed
qed
qed (fact refl)
end
end
end