Theory More_MPoly_Type_Class
section ‹Further Properties of Multivariate Polynomials›
theory More_MPoly_Type_Class
imports Polynomials.MPoly_Type_Class_Ordered General
begin
text ‹Some further general properties of (ordered) multivariate polynomials needed for Gr\"obner
bases. This theory is an extension of @{theory Polynomials.MPoly_Type_Class_Ordered}.›
subsection ‹Modules and Linear Hulls›
context module
begin
lemma span_listE:
assumes "p ∈ span (set bs)"
obtains qs where "length qs = length bs" and "p = sum_list (map2 (*s) qs bs)"
proof -
have "finite (set bs)" ..
from this assms obtain q where p: "p = (∑b∈set bs. (q b) *s b)" by (rule span_finiteE)
let ?qs = "map_dup q (λ_. 0) bs"
show ?thesis
proof
show "length ?qs = length bs" by simp
next
let ?zs = "zip (map q (remdups bs)) (remdups bs)"
have *: "distinct ?zs" by (rule distinct_zipI2, rule distinct_remdups)
have inj: "inj_on (λb. (q b, b)) (set bs)" by (rule, simp)
have "p = (∑(q, b)←?zs. q *s b)"
by (simp add: sum_list_distinct_conv_sum_set[OF *] set_zip_map1 p comm_monoid_add_class.sum.reindex[OF inj])
also have "... = (∑(q, b)←(filter (λ(q, b). q ≠ 0) ?zs). q *s b)"
by (rule monoid_add_class.sum_list_map_filter[symmetric], auto)
also have "... = (∑(q, b)←(filter (λ(q, b). q ≠ 0) (zip ?qs bs)). q *s b)"
by (simp only: filter_zip_map_dup_const)
also have "... = (∑(q, b)←zip ?qs bs. q *s b)"
by (rule monoid_add_class.sum_list_map_filter, auto)
finally show "p = (∑(q, b)←zip ?qs bs. q *s b)" .
qed
qed
lemma span_listI: "sum_list (map2 (*s) qs bs) ∈ span (set bs)"
proof (induct qs arbitrary: bs)
case Nil
show ?case by (simp add: span_zero)
next
case step: (Cons q qs)
show ?case
proof (simp add: zip_Cons1 span_zero split: list.split, intro allI impI)
fix a as
have "sum_list (map2 (*s) qs as) ∈ span (insert a (set as))" (is "?x ∈ ?A")
by (rule, fact step, rule span_mono, auto)
moreover have "a ∈ ?A" by (rule span_base) simp
ultimately show "q *s a + ?x ∈ ?A" by (intro span_add span_scale)
qed
qed
end
lemma (in term_powerprod) monomial_1_in_pmdlI:
assumes "(f::_ ⇒⇩0 'b::field) ∈ pmdl F" and "keys f = {t}"
shows "monomial 1 t ∈ pmdl F"
proof -
define c where "c ≡ lookup f t"
from assms(2) have f_eq: "f = monomial c t" unfolding c_def
by (metis (mono_tags, lifting) Diff_insert_absorb cancel_comm_monoid_add_class.add_cancel_right_right
plus_except insert_absorb insert_not_empty keys_eq_empty keys_except)
from assms(2) have "c ≠ 0"
unfolding c_def by auto
hence "monomial 1 t = monom_mult (1 / c) 0 f" by (simp add: f_eq monom_mult_monomial term_simps)
also from assms(1) have "... ∈ pmdl F" by (rule pmdl_closed_monom_mult)
finally show ?thesis .
qed
subsection ‹Ordered Polynomials›
context ordered_term
begin
subsubsection ‹Sets of Leading Terms and -Coefficients›
definition lt_set :: "('t, 'b::zero) poly_mapping set ⇒ 't set" where
"lt_set F = lt ` (F - {0})"
definition lc_set :: "('t, 'b::zero) poly_mapping set ⇒ 'b set" where
"lc_set F = lc ` (F - {0})"
lemma lt_setI:
assumes "f ∈ F" and "f ≠ 0"
shows "lt f ∈ lt_set F"
unfolding lt_set_def using assms by simp
lemma lt_setE:
assumes "t ∈ lt_set F"
obtains f where "f ∈ F" and "f ≠ 0" and "lt f = t"
using assms unfolding lt_set_def by auto
lemma lt_set_iff:
shows "t ∈ lt_set F ⟷ (∃f∈F. f ≠ 0 ∧ lt f = t)"
unfolding lt_set_def by auto
lemma lc_setI:
assumes "f ∈ F" and "f ≠ 0"
shows "lc f ∈ lc_set F"
unfolding lc_set_def using assms by simp
lemma lc_setE:
assumes "c ∈ lc_set F"
obtains f where "f ∈ F" and "f ≠ 0" and "lc f = c"
using assms unfolding lc_set_def by auto
lemma lc_set_iff:
shows "c ∈ lc_set F ⟷ (∃f∈F. f ≠ 0 ∧ lc f = c)"
unfolding lc_set_def by auto
lemma lc_set_nonzero:
shows "0 ∉ lc_set F"
proof
assume "0 ∈ lc_set F"
then obtain f where "f ∈ F" and "f ≠ 0" and "lc f = 0" by (rule lc_setE)
from ‹f ≠ 0› have "lc f ≠ 0" by (rule lc_not_0)
from this ‹lc f = 0› show False ..
qed
lemma lt_sum_distinct_eq_Max:
assumes "finite I" and "sum p I ≠ 0"
and "⋀i1 i2. i1 ∈ I ⟹ i2 ∈ I ⟹ p i1 ≠ 0 ⟹ p i2 ≠ 0 ⟹ lt (p i1) = lt (p i2) ⟹ i1 = i2"
shows "lt (sum p I) = ord_term_lin.Max (lt_set (p ` I))"
proof -
have "¬ p ` I ⊆ {0}"
proof
assume "p ` I ⊆ {0}"
hence "sum p I = 0" by (rule sum_poly_mapping_eq_zeroI)
with assms(2) show False ..
qed
from assms(1) this assms(3) show ?thesis
proof (induct I)
case empty
from empty(1) show ?case by simp
next
case (insert x I)
show ?case
proof (cases "p ` I ⊆ {0}")
case True
hence "p ` I - {0} = {}" by simp
have "p x ≠ 0"
proof
assume "p x = 0"
with True have " p ` insert x I ⊆ {0}" by simp
with insert(4) show False ..
qed
hence "insert (p x) (p ` I) - {0} = insert (p x) (p ` I - {0})" by auto
hence "lt_set (p ` insert x I) = {lt (p x)}" by (simp add: lt_set_def ‹p ` I - {0} = {}›)
hence eq1: "ord_term_lin.Max (lt_set (p ` insert x I)) = lt (p x)" by simp
have eq2: "sum p I = 0"
proof (rule ccontr)
assume "sum p I ≠ 0"
then obtain y where "y ∈ I" and "p y ≠ 0" by (rule sum.not_neutral_contains_not_neutral)
with True show False by auto
qed
show ?thesis by (simp only: eq1 sum.insert[OF insert(1) insert(2)], simp add: eq2)
next
case False
hence IH: "lt (sum p I) = ord_term_lin.Max (lt_set (p ` I))"
proof (rule insert(3))
fix i1 i2
assume "i1 ∈ I" and "i2 ∈ I"
hence "i1 ∈ insert x I" and "i2 ∈ insert x I" by simp_all
moreover assume "p i1 ≠ 0" and "p i2 ≠ 0" and "lt (p i1) = lt (p i2)"
ultimately show "i1 = i2" by (rule insert(5))
qed
show ?thesis
proof (cases "p x = 0")
case True
hence eq: "lt_set (p ` insert x I) = lt_set (p ` I)" by (simp add: lt_set_def)
show ?thesis by (simp only: eq, simp add: sum.insert[OF insert(1) insert(2)] True, fact IH)
next
case False
hence eq1: "lt_set (p ` insert x I) = insert (lt (p x)) (lt_set (p ` I))"
by (auto simp add: lt_set_def)
from insert(1) have "finite (lt_set (p ` I))" by (simp add: lt_set_def)
moreover from ‹¬ p ` I ⊆ {0}› have "lt_set (p ` I) ≠ {}" by (simp add: lt_set_def)
ultimately have eq2: "ord_term_lin.Max (insert (lt (p x)) (lt_set (p ` I))) =
ord_term_lin.max (lt (p x)) (ord_term_lin.Max (lt_set (p ` I)))"
by (rule ord_term_lin.Max_insert)
show ?thesis
proof (simp only: eq1, simp add: sum.insert[OF insert(1) insert(2)] eq2 IH[symmetric],
rule lt_plus_distinct_eq_max, rule)
assume *: "lt (p x) = lt (sum p I)"
have "lt (p x) ∈ lt_set (p ` I)" by (simp only: * IH, rule ord_term_lin.Max_in, fact+)
then obtain f where "f ∈ p ` I" and "f ≠ 0" and ltf: "lt f = lt (p x)" by (rule lt_setE)
from this(1) obtain y where "y ∈ I" and "f = p y" ..
from this(2) ‹f ≠ 0› ltf have "p y ≠ 0" and lt_eq: "lt (p y) = lt (p x)" by simp_all
from _ _ this(1) ‹p x ≠ 0› this(2) have "y = x"
proof (rule insert(5))
from ‹y ∈ I› show "y ∈ insert x I" by simp
next
show "x ∈ insert x I" by simp
qed
with ‹y ∈ I› have "x ∈ I" by simp
with ‹x ∉ I› show False ..
qed
qed
qed
qed
qed
lemma lt_sum_distinct_in_lt_set:
assumes "finite I" and "sum p I ≠ 0"
and "⋀i1 i2. i1 ∈ I ⟹ i2 ∈ I ⟹ p i1 ≠ 0 ⟹ p i2 ≠ 0 ⟹ lt (p i1) = lt (p i2) ⟹ i1 = i2"
shows "lt (sum p I) ∈ lt_set (p ` I)"
proof -
have "¬ p ` I ⊆ {0}"
proof
assume "p ` I ⊆ {0}"
hence "sum p I = 0" by (rule sum_poly_mapping_eq_zeroI)
with assms(2) show False ..
qed
have "lt (sum p I) = ord_term_lin.Max (lt_set (p ` I))"
by (rule lt_sum_distinct_eq_Max, fact+)
also have "... ∈ lt_set (p ` I)"
proof (rule ord_term_lin.Max_in)
from assms(1) show "finite (lt_set (p ` I))" by (simp add: lt_set_def)
next
from ‹¬ p ` I ⊆ {0}› show "lt_set (p ` I) ≠ {}" by (simp add: lt_set_def)
qed
finally show ?thesis .
qed
subsubsection ‹Monicity›
definition monic :: "('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b::field)" where
"monic p = monom_mult (1 / lc p) 0 p"
definition is_monic_set :: "('t ⇒⇩0 'b::field) set ⇒ bool" where
"is_monic_set B ≡ (∀b∈B. b ≠ 0 ⟶ lc b = 1)"
lemma lookup_monic: "lookup (monic p) v = (lookup p v) / lc p"
proof -
have "lookup (monic p) (0 ⊕ v) = (1 / lc p) * (lookup p v)" unfolding monic_def
by (rule lookup_monom_mult_plus)
thus ?thesis by (simp add: term_simps)
qed
lemma lookup_monic_lt:
assumes "p ≠ 0"
shows "lookup (monic p) (lt p) = 1"
unfolding monic_def
proof -
from assms have "lc p ≠ 0" by (rule lc_not_0)
hence "1 / lc p ≠ 0" by simp
let ?q = "monom_mult (1 / lc p) 0 p"
have "lookup ?q (0 ⊕ lt p) = (1 / lc p) * (lookup p (lt p))" by (rule lookup_monom_mult_plus)
also have "... = (1 / lc p) * lc p" unfolding lc_def ..
also have "... = 1" using ‹lc p ≠ 0› by simp
finally have "lookup ?q (0 ⊕ lt p) = 1" .
thus "lookup ?q (lt p) = 1" by (simp add: term_simps)
qed
lemma monic_0 [simp]: "monic 0 = 0"
unfolding monic_def by (rule monom_mult_zero_right)
lemma monic_0_iff: "(monic p = 0) ⟷ (p = 0)"
proof
assume "monic p = 0"
show "p = 0"
proof (rule ccontr)
assume "p ≠ 0"
hence "lookup (monic p) (lt p) = 1" by (rule lookup_monic_lt)
with ‹monic p = 0› have "lookup 0 (lt p) = (1::'b)" by simp
thus False by simp
qed
next
assume p0: "p = 0"
show "monic p = 0" unfolding p0 by (fact monic_0)
qed
lemma keys_monic [simp]: "keys (monic p) = keys p"
proof (cases "p = 0")
case True
show ?thesis unfolding True monic_0 ..
next
case False
hence "lc p ≠ 0" by (rule lc_not_0)
show ?thesis by (rule set_eqI, simp add: in_keys_iff lookup_monic ‹lc p ≠ 0›)
qed
lemma lt_monic [simp]: "lt (monic p) = lt p"
proof (cases "p = 0")
case True
show ?thesis unfolding True monic_0 ..
next
case False
have "lt (monom_mult (1 / lc p) 0 p) = 0 ⊕ lt p"
proof (rule lt_monom_mult)
from False have "lc p ≠ 0" by (rule lc_not_0)
thus "1 / lc p ≠ 0" by simp
qed fact
thus ?thesis by (simp add: monic_def term_simps)
qed
lemma lc_monic:
assumes "p ≠ 0"
shows "lc (monic p) = 1"
using assms by (simp add: lc_def lookup_monic_lt)
lemma mult_lc_monic:
assumes "p ≠ 0"
shows "monom_mult (lc p) 0 (monic p) = p" (is "?q = p")
proof (rule poly_mapping_eqI)
fix v
from assms have "lc p ≠ 0" by (rule lc_not_0)
have "lookup ?q (0 ⊕ v) = (lc p) * (lookup (monic p) v)" by (rule lookup_monom_mult_plus)
also have "... = (lc p) * ((lookup p v) / lc p)" by (simp add: lookup_monic)
also have "... = lookup p v" using ‹lc p ≠ 0› by simp
finally show "lookup ?q v = lookup p v" by (simp add: term_simps)
qed
lemma is_monic_setI:
assumes "⋀b. b ∈ B ⟹ b ≠ 0 ⟹ lc b = 1"
shows "is_monic_set B"
unfolding is_monic_set_def using assms by auto
lemma is_monic_setD:
assumes "is_monic_set B" and "b ∈ B" and "b ≠ 0"
shows "lc b = 1"
using assms unfolding is_monic_set_def by auto
lemma Keys_image_monic [simp]: "Keys (monic ` A) = Keys A"
by (simp add: Keys_def)
lemma image_monic_is_monic_set: "is_monic_set (monic ` A)"
proof (rule is_monic_setI)
fix p
assume pin: "p ∈ monic ` A" and "p ≠ 0"
from pin obtain p' where p_def: "p = monic p'" and "p' ∈ A" ..
from ‹p ≠ 0› have "p' ≠ 0" unfolding p_def monic_0_iff .
thus "lc p = 1" unfolding p_def by (rule lc_monic)
qed
lemma pmdl_image_monic [simp]: "pmdl (monic ` B) = pmdl B"
proof
show "pmdl (monic ` B) ⊆ pmdl B"
proof
fix p
assume "p ∈ pmdl (monic ` B)"
thus "p ∈ pmdl B"
proof (induct p rule: pmdl_induct)
case base: module_0
show ?case by (fact pmdl.span_zero)
next
case ind: (module_plus a b c t)
from ind(3) obtain b' where b_def: "b = monic b'" and "b' ∈ B" ..
have eq: "b = monom_mult (1 / lc b') 0 b'" by (simp only: b_def monic_def)
show ?case unfolding eq monom_mult_assoc
by (rule pmdl.span_add, fact, rule monom_mult_in_pmdl, fact)
qed
qed
next
show "pmdl B ⊆ pmdl (monic ` B)"
proof
fix p
assume "p ∈ pmdl B"
thus "p ∈ pmdl (monic ` B)"
proof (induct p rule: pmdl_induct)
case base: module_0
show ?case by (fact pmdl.span_zero)
next
case ind: (module_plus a b c t)
show ?case
proof (cases "b = 0")
case True
from ind(2) show ?thesis by (simp add: True)
next
case False
let ?b = "monic b"
from ind(3) have "?b ∈ monic ` B" by (rule imageI)
have "a + monom_mult c t (monom_mult (lc b) 0 ?b) ∈ pmdl (monic ` B)"
unfolding monom_mult_assoc
by (rule pmdl.span_add, fact, rule monom_mult_in_pmdl, fact)
thus ?thesis unfolding mult_lc_monic[OF False] .
qed
qed
qed
qed
end
end