Theory Indexed_Poly
section ‹Polynomials in an Indexed Family of Indeterminates›
theory Indexed_Poly
imports Poly_Ring "HOL-Library.Multiset"
begin
text ‹
‹Poly_Ring› builds ‹R[X]› from finite-support functions @{typ "nat ⇒ 'a"}, the exponent of the
single indeterminate being the index. Here the indeterminates form an arbitrary family, indexed by
a type @{typ 'i}, and a monomial is therefore not a single exponent but a ∗‹multiset› over
@{typ 'i}: the monomial ‹X⇩i⇧2 X⇩j› is @{term "{# i, i, j #}"}. A polynomial is a finite-support
function @{typ "'i multiset ⇒ 'a"} with coefficients in the carrier, so the representation choice
is the same one ‹Poly_Ring› makes, with the exponent @{typ nat} replaced by a monomial. Addition
is pointwise and multiplication is the convolution
‹(p ⊗ q) m = (∑n ⊆# m. p n ⋅ q (m - n))›, the sum running over the submultisets of ‹m› --- the
monomial factorisations ‹m = n + (m - n)› --- exactly as the univariate convolution runs over
‹{..k}›, the factorisations ‹k = i + (k - i)›.
❙‹Why an indexed family, rather than iterating ‹Poly_Ring›.› Iteration gives ‹R[X][Y]› and so on,
which is ∗‹finitely› many indeterminates. The construction of an algebraic closure needs one
indeterminate for every polynomial over the base ring, all present at once, so that a maximal
extension has room for a root of each. That is what this theory supplies.
Three facts used below --- ‹fincomp_Sigma›, ‹fincomp_mult_distrib_left› and
‹fincomp_mult_distrib_right› --- live in ‹Poly_Ring› but are generic in the index type and say
nothing about polynomials.
›
subsection ‹Submultisets›
text ‹The convolution sums over the submultisets of a monomial, so that index set must be finite.
Each submultiset of @{term "add_mset x m"} either omits @{term x}, and is a submultiset of
@{term m}, or contains it, and is @{term x} added to one.›
lemma finite_submultisets: "finite {n. n ⊆# (m :: 'i multiset)}"
proof (induct m rule: multiset_induct)
case empty
have "{n. n ⊆# {#}} = {{#}}" by auto
then show ?case by simp
next
case (add x m)
have "{n. n ⊆# add_mset x m} ⊆ {n. n ⊆# m} ∪ add_mset x ` {n. n ⊆# m}"
proof
fix n assume "n ∈ {n. n ⊆# add_mset x m}"
then have n: "⋀y. count n y ≤ count (add_mset x m) y"
by (simp add: subseteq_mset_def)
show "n ∈ {n. n ⊆# m} ∪ add_mset x ` {n. n ⊆# m}"
proof (cases "x ∈# n")
case True
have "count (n - {#x#}) y ≤ count m y" for y
using n [of y] True by (cases "y = x") auto
moreover from True have "n = add_mset x (n - {#x#})" by simp
ultimately show ?thesis by (auto simp: subseteq_mset_def)
next
case False
have "count n y ≤ count m y" for y
using n [of y] False by (cases "y = x") (auto simp: not_in_iff)
then show ?thesis by (simp add: subseteq_mset_def)
qed
qed
moreover have "finite ({n. n ⊆# m} ∪ add_mset x ` {n. n ⊆# m})"
using add by blast
ultimately show ?case by (rule finite_subset)
qed
text ‹Monomial arithmetic for the convolution, all at the level of coefficient counts. The last
two are the identities that make the associativity reindexing below a bijection.›
lemma msub_diff_mono: "⟦ a ⊆# b; b ⊆# m ⟧ ⟹ b - a ⊆# m - a"
using subset_eq_diff_conv by fastforce
lemma msub_add_closed: "⟦ a ⊆# m; b ⊆# m - a ⟧ ⟹ a + b ⊆# m"
by (simp add: add.commute subset_mset.le_diff_conv2)
lemma msub_diff_diff: "⟦ a ⊆# b; b ⊆# m ⟧ ⟹ m - a - (b - a) = m - b"
by (simp add: subseteq_mset_def multiset_eq_iff)
text ‹Complementation is an involution of the submultisets of a monomial; this is what makes the
convolution symmetric when the coefficients commute.›
lemma msub_double_diff: "n ⊆# m ⟹ m - (m - n) = n"
by (simp add: subseteq_mset_def multiset_eq_iff)
context Ring
begin
subsection ‹Carrier and coefficients›
text ‹The polynomials over @{term R} in the indeterminates indexed by @{typ 'i}: finite support on
monomials, coefficients in the carrier.›
definition ipoly_carrier :: "('i multiset ⇒ 'a) set"
where "ipoly_carrier ≡ {p. finite {m. p m ≠ 𝟬} ∧ (∀m. p m ∈ R)}"
lemma ipoly_carrierI:
"⟦ finite {m. p m ≠ 𝟬}; ⋀m. p m ∈ R ⟧ ⟹ p ∈ ipoly_carrier"
unfolding ipoly_carrier_def by blast
lemma ipoly_carrier_finite: "p ∈ ipoly_carrier ⟹ finite {m. p m ≠ 𝟬}"
unfolding ipoly_carrier_def by blast
lemma ipoly_carrier_coeff_closed: "p ∈ ipoly_carrier ⟹ p m ∈ R"
unfolding ipoly_carrier_def by blast
subsection ‹Operations›
definition ipoly_zero :: "'i multiset ⇒ 'a" (‹𝟬⇩I›)
where "ipoly_zero ≡ (λm. 𝟬)"
text ‹The unit is the constant @{term 𝟭}, carried by the empty monomial.›
definition ipoly_one :: "'i multiset ⇒ 'a" (‹𝟭⇩I›)
where "ipoly_one ≡ (λm. if m = {#} then 𝟭 else 𝟬)"
definition ipoly_add :: "('i multiset ⇒ 'a) ⇒ ('i multiset ⇒ 'a) ⇒ ('i multiset ⇒ 'a)"
(infixl ‹⊕⇩I› 65)
where "ipoly_add p q ≡ (λm. p m + q m)"
definition ipoly_neg :: "('i multiset ⇒ 'a) ⇒ ('i multiset ⇒ 'a)" (‹⊖⇩I _› [66] 65)
where "ipoly_neg p ≡ (λm. - p m)"
text ‹The convolution: a coefficient of the product sums over the factorisations
‹m = n + (m - n)› of the monomial.›
definition ipoly_mult :: "('i multiset ⇒ 'a) ⇒ ('i multiset ⇒ 'a) ⇒ ('i multiset ⇒ 'a)"
(infixl ‹⊗⇩I› 70)
where "ipoly_mult p q ≡ (λm. additive.fincomp (λn. p n ⋅ q (m - n)) {n. n ⊆# m})"
subsection ‹Closure under the operations›
lemma ipoly_zero_closed: "𝟬⇩I ∈ ipoly_carrier"
by (rule ipoly_carrierI) (auto simp: ipoly_zero_def)
lemma ipoly_one_closed: "𝟭⇩I ∈ ipoly_carrier"
by (intro ipoly_carrierI) (auto simp: ipoly_one_def)
lemma ipoly_add_closed:
assumes "p ∈ ipoly_carrier" "q ∈ ipoly_carrier"
shows "p ⊕⇩I q ∈ ipoly_carrier"
proof (rule ipoly_carrierI)
have "{m. (p ⊕⇩I q) m ≠ 𝟬} ⊆ {m. p m ≠ 𝟬} ∪ {m. q m ≠ 𝟬}"
using additive.left_unit by (fastforce simp: additive.right_unit additive.unit_closed ipoly_add_def)
moreover have "finite ({m. p m ≠ 𝟬} ∪ {m. q m ≠ 𝟬})"
using assms by (simp add: ipoly_carrier_finite)
ultimately show "finite {m. (p ⊕⇩I q) m ≠ 𝟬}" by (rule finite_subset)
show "⋀m. (p ⊕⇩I q) m ∈ R"
using assms by (simp add: ipoly_add_def ipoly_carrier_coeff_closed)
qed
lemma ipoly_neg_closed:
assumes p: "p ∈ ipoly_carrier" shows "⊖⇩I p ∈ ipoly_carrier"
proof (rule ipoly_carrierI)
have "{m. (⊖⇩I p) m ≠ 𝟬} ⊆ {m. p m ≠ 𝟬}"
unfolding ipoly_neg_def using additive.inverse_unit by force
then show "finite {m. (⊖⇩I p) m ≠ 𝟬}"
using p ipoly_carrier_finite finite_subset by blast
show "⋀m. (⊖⇩I p) m ∈ R"
using p by (simp add: ipoly_neg_def ipoly_carrier_coeff_closed)
qed
lemma ipoly_mult_coeff_closed:
assumes "p ∈ ipoly_carrier" "q ∈ ipoly_carrier"
shows "(p ⊗⇩I q) m ∈ R"
by (simp add: assms ipoly_carrier_coeff_closed ipoly_mult_def)
text ‹A product coefficient can be nonzero only at a monomial that factors as a support monomial of
@{term p} times one of @{term q}, and there are finitely many such products. This replaces the
degree bound used in the univariate case, where the support is bounded by a single number.›
lemma ipoly_mult_support_bound:
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier"
shows "{m. (p ⊗⇩I q) m ≠ 𝟬} ⊆ (λ(a, b). a + b) ` ({m. p m ≠ 𝟬} × {m. q m ≠ 𝟬})"
proof
fix m assume "m ∈ {m. (p ⊗⇩I q) m ≠ 𝟬}"
then have nz: "(p ⊗⇩I q) m ≠ 𝟬" by simp
show "m ∈ (λ(a, b). a + b) ` ({m. p m ≠ 𝟬} × {m. q m ≠ 𝟬})"
proof (rule ccontr)
assume "m ∉ (λ(a, b). a + b) ` ({m. p m ≠ 𝟬} × {m. q m ≠ 𝟬})"
then have "p n ⋅ q (m - n) = 𝟬" if "n ∈ {n. n ⊆# m}" for n
using that assms
apply (simp add: image_iff ipoly_carrier_coeff_closed)
by (metis ipoly_carrier_coeff_closed left_zero right_zero subset_mset.add_diff_inverse)
then have "(p ⊗⇩I q) m = 𝟬"
unfolding ipoly_mult_def by (rule additive.fincomp_unit_eqI)
with nz show False by simp
qed
qed
lemma ipoly_mult_closed:
assumes "p ∈ ipoly_carrier" and "q ∈ ipoly_carrier"
shows "p ⊗⇩I q ∈ ipoly_carrier"
proof (rule ipoly_carrierI)
have "finite ({m. p m ≠ 𝟬} × {m. q m ≠ 𝟬})"
using assms by (simp add: ipoly_carrier_finite)
then show "finite {m. (p ⊗⇩I q) m ≠ 𝟬}"
using ipoly_mult_support_bound [OF assms] by (blast intro: finite_subset)
qed (simp add: ipoly_mult_coeff_closed assms)
subsection ‹Additive structure›
text ‹Addition is pointwise, so the abelian-group laws are those of @{term R} coefficientwise.›
lemma ipoly_add_assoc:
"⟦ p ∈ ipoly_carrier; q ∈ ipoly_carrier; r ∈ ipoly_carrier ⟧
⟹ (p ⊕⇩I q) ⊕⇩I r = p ⊕⇩I (q ⊕⇩I r)"
by (auto simp: ipoly_add_def additive.associative ipoly_carrier_coeff_closed)
lemma ipoly_add_comm:
"⟦ p ∈ ipoly_carrier; q ∈ ipoly_carrier ⟧ ⟹ p ⊕⇩I q = q ⊕⇩I p"
by (auto simp: ipoly_add_def additive.commutative ipoly_carrier_coeff_closed)
lemma ipoly_add_zero: "p ∈ ipoly_carrier ⟹ 𝟬⇩I ⊕⇩I p = p"
by (auto simp: ipoly_add_def ipoly_zero_def ipoly_carrier_coeff_closed)
lemma ipoly_add_neg: "p ∈ ipoly_carrier ⟹ (⊖⇩I p) ⊕⇩I p = 𝟬⇩I"
by (auto simp: ipoly_add_def ipoly_neg_def ipoly_zero_def ipoly_carrier_coeff_closed)
lemma ipoly_add_neg_right: "p ∈ ipoly_carrier ⟹ p ⊕⇩I (⊖⇩I p) = 𝟬⇩I"
using ipoly_add_comm ipoly_add_neg ipoly_neg_closed by force
subsection ‹Multiplicative unit›
text ‹Only the empty monomial contributes to a product with the unit.›
lemma ipoly_mult_one_left:
assumes p: "p ∈ ipoly_carrier"
shows "𝟭⇩I ⊗⇩I p = p"
proof
fix m
have "(𝟭⇩I ⊗⇩I p) m = additive.fincomp (λn. 𝟭⇩I n ⋅ p (m - n)) {n. n ⊆# m}"
by (simp add: ipoly_mult_def)
also have "… = additive.fincomp (λn. if n = {#} then (λ_. p m) n else 𝟬) {n. n ⊆# m}"
using p by (intro additive.fincomp_cong')
(auto simp: ipoly_one_def ipoly_carrier_coeff_closed)
also have "… = p m"
by (intro additive.fincomp_singleton_swap) (auto simp: finite_submultisets ipoly_carrier_coeff_closed p)
finally show "(𝟭⇩I ⊗⇩I p) m = p m" .
qed
lemma ipoly_mult_one_right:
assumes p: "p ∈ ipoly_carrier"
shows "p ⊗⇩I 𝟭⇩I = p"
proof
fix m
have "(p ⊗⇩I 𝟭⇩I) m = additive.fincomp (λn. p n ⋅ 𝟭⇩I (m - n)) {n. n ⊆# m}"
by (simp add: ipoly_mult_def)
also have "… = additive.fincomp (λn. if n = m then (λ_. p m) n else 𝟬) {n. n ⊆# m}"
using p
by (intro additive.fincomp_cong')
(auto simp: ipoly_one_def ipoly_carrier_coeff_closed Diff_eq_empty_iff_mset)
also have "… = p m"
by (intro additive.fincomp_singleton_swap) (auto simp: finite_submultisets ipoly_carrier_coeff_closed p)
finally show "(p ⊗⇩I 𝟭⇩I) m = p m" .
qed
subsection ‹Distributivity›
lemma ipoly_mult_add_distrib_left:
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier" and r: "r ∈ ipoly_carrier"
shows "p ⊗⇩I (q ⊕⇩I r) = (p ⊗⇩I q) ⊕⇩I (p ⊗⇩I r)"
proof
fix m
have pi: "⋀n. p n ∈ R" and qi: "⋀n. q n ∈ R" and ri: "⋀n. r n ∈ R"
using p q r by (auto simp: ipoly_carrier_coeff_closed)
have "(p ⊗⇩I (q ⊕⇩I r)) m
= additive.fincomp (λn. p n ⋅ (q (m - n) + r (m - n))) {n. n ⊆# m}"
by (simp add: ipoly_mult_def ipoly_add_def)
also have "… = additive.fincomp (λn. p n ⋅ q (m - n) + p n ⋅ r (m - n)) {n. n ⊆# m}"
using distributive(1) pi qi ri by presburger
also have "… = additive.fincomp (λn. p n ⋅ q (m - n)) {n. n ⊆# m}
+ additive.fincomp (λn. p n ⋅ r (m - n)) {n. n ⊆# m}"
by (rule additive.fincomp_comp) (use pi qi ri in auto)
also have "… = ((p ⊗⇩I q) ⊕⇩I (p ⊗⇩I r)) m"
by (simp add: ipoly_mult_def ipoly_add_def)
finally show "(p ⊗⇩I (q ⊕⇩I r)) m = ((p ⊗⇩I q) ⊕⇩I (p ⊗⇩I r)) m" .
qed
lemma ipoly_mult_add_distrib_right:
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier" and r: "r ∈ ipoly_carrier"
shows "(q ⊕⇩I r) ⊗⇩I p = (q ⊗⇩I p) ⊕⇩I (r ⊗⇩I p)"
proof
fix m
have pi: "⋀n. p n ∈ R" and qi: "⋀n. q n ∈ R" and ri: "⋀n. r n ∈ R"
using p q r by (auto simp: ipoly_carrier_coeff_closed)
have "((q ⊕⇩I r) ⊗⇩I p) m = additive.fincomp (λn. (q n + r n) ⋅ p (m - n)) {n. n ⊆# m}"
by (simp add: ipoly_mult_def ipoly_add_def)
also have "… = additive.fincomp (λn. q n ⋅ p (m - n) + r n ⋅ p (m - n)) {n. n ⊆# m}"
using distributive(2) pi qi ri by presburger
also have "… = additive.fincomp (λn. q n ⋅ p (m - n)) {n. n ⊆# m}
+ additive.fincomp (λn. r n ⋅ p (m - n)) {n. n ⊆# m}"
by (rule additive.fincomp_comp) (use pi qi ri in auto)
also have "… = ((q ⊗⇩I p) ⊕⇩I (r ⊗⇩I p)) m"
by (simp add: ipoly_mult_def ipoly_add_def)
finally show "((q ⊕⇩I r) ⊗⇩I p) m = ((q ⊗⇩I p) ⊕⇩I (r ⊗⇩I p)) m" .
qed
subsection ‹Associativity of the convolution›
text ‹Both sides are the sum of ‹p a ⋅ q b ⋅ r c› over the factorisations ‹m = a + b + c›. The two
nested sums present that set differently --- as pairs ‹(b + a, a)› on the left and ‹(a, b)› on the
right --- so the proof is a reindexing along ‹(b, a) ↦ (a, b - a)›, exactly as in the
univariate case, with monomial arithmetic in place of arithmetic on degrees.›
lemma ipoly_mult_assoc:
fixes p q r :: "'i multiset ⇒ 'a"
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier" and r: "r ∈ ipoly_carrier"
shows "(p ⊗⇩I q) ⊗⇩I r = p ⊗⇩I (q ⊗⇩I r)"
proof (rule ext)
fix m :: "'i multiset"
have pi: "⋀n. p n ∈ R" and qi: "⋀n. q n ∈ R" and ri: "⋀n. r n ∈ R"
using p q r by (auto simp: ipoly_carrier_coeff_closed)
let ?S1 = "Sigma {b. b ⊆# m} (λb :: 'i multiset. {a. a ⊆# b})"
let ?S2 = "Sigma {a. a ⊆# m} (λa :: 'i multiset. {b. b ⊆# m - a})"
have "((p ⊗⇩I q) ⊗⇩I r) m
= additive.fincomp
(λb. additive.fincomp (λa. p a ⋅ q (b - a)) {a. a ⊆# b} ⋅ r (m - b))
{b. b ⊆# m}"
by (simp add: ipoly_mult_def)
also have "… = additive.fincomp
(λb. additive.fincomp (λa. (p a ⋅ q (b - a)) ⋅ r (m - b)) {a. a ⊆# b})
{b. b ⊆# m}"
using pi qi ri
by (intro additive.fincomp_cong' fincomp_mult_distrib_right) auto
also have "… = additive.fincomp
(λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (m - fst x)) ?S1"
by (rule fincomp_Sigma) (use pi qi ri finite_submultisets in auto)
finally have LHS: "((p ⊗⇩I q) ⊗⇩I r) m
= additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (m - fst x)) ?S1" .
have "(p ⊗⇩I (q ⊗⇩I r)) m
= additive.fincomp
(λa. p a ⋅ additive.fincomp (λb. q b ⋅ r (m - a - b)) {b. b ⊆# m - a})
{a. a ⊆# m}"
by (simp add: ipoly_mult_def)
also have "… = additive.fincomp
(λa. additive.fincomp (λb. p a ⋅ (q b ⋅ r (m - a - b))) {b. b ⊆# m - a})
{a. a ⊆# m}"
using pi qi ri
by (intro additive.fincomp_cong' fincomp_mult_distrib_left) auto
also have "… = additive.fincomp
(λx. p (fst x) ⋅ (q (snd x) ⋅ r (m - fst x - snd x))) ?S2"
by (rule fincomp_Sigma) (use pi qi ri finite_submultisets in auto)
finally have RHS: "(p ⊗⇩I (q ⊗⇩I r)) m
= additive.fincomp (λx. p (fst x) ⋅ (q (snd x) ⋅ r (m - fst x - snd x))) ?S2" .
let ?h = "λx :: 'i multiset × 'i multiset. (snd x, fst x - snd x)"
let ?h' = "λx :: 'i multiset × 'i multiset. (fst x + snd x, fst x)"
have bij: "bij_betw ?h ?S1 ?S2"
proof (rule bij_betw_byWitness [where f' = ?h'])
show "?h ` ?S1 ⊆ ?S2"
by (auto simp: msub_diff_mono intro: subset_mset.order_trans)
qed (auto simp: subset_mset.add_diff_inverse msub_add_closed)
let ?F = "λx. p (fst x) ⋅ (q (snd x) ⋅ r (m - fst x - snd x))"
have "additive.fincomp ?F ?S2 = additive.fincomp ?F (?h ` ?S1)"
using bij bij_betw_imp_surj_on by fastforce
also have "… = additive.fincomp (λx. ?F (?h x)) ?S1"
proof (rule additive.fincomp_reindex)
show "?F ∈ ?h ` ?S1 → R" using pi qi ri by auto
show "inj_on ?h ?S1" using bij bij_betw_imp_inj_on by blast
qed
also have "… = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (m - fst x)) ?S1"
using pi qi ri multiplicative.associative
by (intro additive.fincomp_cong') (auto simp: msub_diff_diff)
finally show "((p ⊗⇩I q) ⊗⇩I r) m = (p ⊗⇩I (q ⊗⇩I r)) m"
using LHS RHS by simp
qed
subsection ‹The indexed polynomial ring›
theorem ipoly_ring: "Ring ipoly_carrier (⊕⇩I) (⊗⇩I) 𝟬⇩I 𝟭⇩I"
proof -
have add_grp: "Group ipoly_carrier (⊕⇩I) 𝟬⇩I"
proof (rule GroupI)
show "⋀p. p ∈ ipoly_carrier ⟹ p ⊕⇩I 𝟬⇩I = p"
by (metis ipoly_add_comm ipoly_add_zero ipoly_zero_closed)
show "⋀p. p ∈ ipoly_carrier ⟹ ∃q∈ipoly_carrier. p ⊕⇩I q = 𝟬⇩I ∧ q ⊕⇩I p = 𝟬⇩I"
using ipoly_add_neg ipoly_add_neg_right ipoly_neg_closed by blast
qed (auto simp: ipoly_add_closed ipoly_zero_closed ipoly_add_assoc ipoly_add_zero)
interpret add: Group ipoly_carrier "(⊕⇩I)" "𝟬⇩I" by (rule add_grp)
interpret add: Abelian_Group ipoly_carrier "(⊕⇩I)" "𝟬⇩I"
by unfold_locales (rule ipoly_add_comm)
interpret mult: Monoid ipoly_carrier "(⊗⇩I)" "𝟭⇩I"
by (simp add: Monoid.intro ipoly_mult_assoc ipoly_mult_closed ipoly_mult_one_left
ipoly_mult_one_right ipoly_one_closed)
show ?thesis
proof qed (use ipoly_mult_add_distrib_left ipoly_mult_add_distrib_right in auto)
qed
subsection ‹Constants and indeterminates›
text ‹A constant carries its value on the empty monomial. This is the embedding of the coefficient
ring, and it is what lets an extension of @{term R} be built inside this ring.›
definition ipoly_const :: "'a ⇒ ('i multiset ⇒ 'a)"
where "ipoly_const a ≡ (λm. if m = {#} then a else 𝟬)"
lemma ipoly_const_coeff [simp]: "ipoly_const a {#} = a"
by (simp add: ipoly_const_def)
lemma ipoly_const_closed: "a ∈ R ⟹ ipoly_const a ∈ ipoly_carrier"
by (auto simp: ipoly_mult_def ipoly_const_def ipoly_carrierI)
lemma ipoly_const_zero [simp]: "ipoly_const 𝟬 = 𝟬⇩I"
by (simp add: ipoly_const_def ipoly_zero_def fun_eq_iff)
lemma ipoly_const_one [simp]: "ipoly_const 𝟭 = 𝟭⇩I"
by (simp add: ipoly_const_def ipoly_one_def fun_eq_iff)
lemma ipoly_const_add:
assumes "a ∈ R" and "b ∈ R"
shows "ipoly_const (a + b) = (ipoly_const a :: 'i multiset ⇒ 'a) ⊕⇩I ipoly_const b"
using assms by (auto simp: ipoly_const_def ipoly_add_def fun_eq_iff additive.right_unit)
lemma ipoly_const_mult:
assumes "a ∈ R" "b ∈ R"
shows "ipoly_const (a ⋅ b) = (ipoly_const a :: 'i multiset ⇒ 'a) ⊗⇩I ipoly_const b"
using assms by (auto simp: ipoly_mult_def ipoly_const_def additive.fincomp_unit_eqI)
lemma ipoly_const_inj_on: "inj_on (ipoly_const :: 'a ⇒ 'i multiset ⇒ 'a) R"
using ipoly_const_coeff by (metis inj_on_def)
text ‹The indeterminate @{text "X⇩i"} is the monomial @{term "{#i#}"} with coefficient @{term 𝟭}.
Distinct indices give distinct indeterminates whenever the ring is nontrivial: note that
@{locale Ring} does not itself assume @{term "𝟭 ≠ 𝟬"}.›
definition ivar :: "'i ⇒ ('i multiset ⇒ 'a)"
where "ivar i ≡ (λm. if m = {#i#} then 𝟭 else 𝟬)"
lemma ivar_closed: "ivar i ∈ ipoly_carrier"
by (rule ipoly_carrierI) (auto simp: ivar_def)
lemma ivar_inj:
assumes "𝟭 ≠ 𝟬"
shows "inj (ivar :: 'i ⇒ 'i multiset ⇒ 'a)"
using assms by (auto simp: ivar_def inj_on_def fun_eq_iff)
subsection ‹Indeterminates a polynomial does not involve›
text ‹@{term 𝒫} does not involve the indeterminate @{term j} when no monomial containing @{term j}
carries a nonzero coefficient. An index that ∗‹no› element of an extension involves is what
supplies room for a new root: adjoining one is then guaranteed not to disturb what is there
already. This replaces the cardinality argument that a construction over an abstract type of
labels would need, and is the reason for choosing indexed polynomials as the ambient type.›
definition index_free :: "('i multiset ⇒ 'a) ⇒ 'i ⇒ bool"
where "index_free 𝒫 j ≡ (∀m. j ∈# m ⟶ 𝒫 m = 𝟬)"
lemma index_freeI: "(⋀m. j ∈# m ⟹ 𝒫 m = 𝟬) ⟹ index_free 𝒫 j"
by (simp add: index_free_def)
lemma index_freeD: "⟦ index_free 𝒫 j; j ∈# m ⟧ ⟹ 𝒫 m = 𝟬"
by (simp add: index_free_def)
text ‹Constants involve no indeterminate at all.›
lemma index_free_const [simp]: "index_free (ipoly_const a) j"
by (rule index_freeI) (auto simp: ipoly_const_def)
lemma index_free_zero [simp]: "index_free 𝟬⇩I j"
by (rule index_freeI) (simp add: ipoly_zero_def)
text ‹The indeterminate @{term "ivar j"} does involve @{term j}, provided the coefficient ring is
nontrivial --- @{locale Ring} does not itself assume @{term "𝟭 ≠ 𝟬"}.›
lemma not_index_free_ivar:
assumes "𝟭 ≠ 𝟬" shows "¬ index_free (ivar j) j"
using assms index_freeD ivar_def by (metis multi_member_last)
subsection ‹Monomials›
text ‹The monomial @{term "imonom a n"} carries the coefficient @{term a} on the monomial @{term n}.
Constants and indeterminates are the special cases @{term "n = {#}"} and @{term "a = 𝟭"} with
@{term n} a singleton.›
definition imonom :: "'a ⇒ 'i multiset ⇒ ('i multiset ⇒ 'a)"
where "imonom a n ≡ (λm. if m = n then a else 𝟬)"
lemma imonom_apply [simp]: "imonom a n n = a"
by (simp add: imonom_def)
lemma imonom_closed: "a ∈ R ⟹ imonom a n ∈ ipoly_carrier"
proof (rule ipoly_carrierI)
show "finite {m. imonom a n m ≠ 𝟬}"
by (rule finite_subset [where B = "{n}"]) (auto simp: imonom_def)
qed (simp add: imonom_def)
lemma ipoly_const_eq_imonom: "ipoly_const a = imonom a {#}"
by (simp add: ipoly_const_def imonom_def)
lemma ivar_eq_imonom: "ivar j = imonom 𝟭 {#j#}"
by (simp add: ivar_def imonom_def)
lemma imonom_mult:
fixes n n' :: "'i multiset"
assumes a: "a ∈ R" and b: "b ∈ R"
shows "imonom a n ⊗⇩I imonom b n' = imonom (a ⋅ b) (n + n')"
proof
fix m
show "(imonom a n ⊗⇩I imonom b n') m = imonom (a ⋅ b) (n + n') m"
proof (cases "m = n + n'")
case True
have nsub: "n ⊆# m" using True by simp
have "(imonom a n ⊗⇩I imonom b n') m
= additive.fincomp (λp. if p = n then (λ_. a ⋅ b) p else 𝟬) {p. p ⊆# m}"
unfolding ipoly_mult_def
using a b True by (intro additive.fincomp_cong') (auto simp: imonom_def)
also have "… = a ⋅ b"
using nsub a b
by (intro finite_submultisets additive.fincomp_singleton_swap) auto
finally show ?thesis using True by simp
next
case False
with a b have "imonom a n p ⋅ imonom b n' (m - p) = 𝟬" if "p ∈ {p. p ⊆# m}" for p
using that a b by (auto simp: imonom_def subset_mset.add_diff_inverse)
then have "(imonom a n ⊗⇩I imonom b n') m = 𝟬"
unfolding ipoly_mult_def by (rule additive.fincomp_unit_eqI)
then show ?thesis using False by (simp add: imonom_def)
qed
qed
lemma imonom_shift:
fixes n m :: "'i multiset"
assumes c: "c ∈ ipoly_carrier"
shows "(c ⊗⇩I imonom 𝟭 n) m = (if n ⊆# m then c (m - n) else 𝟬)"
proof (cases "n ⊆# m")
case True
then have unique: "(m - p = n) = (p = m - n)" if "p ⊆# m" for p
using that by (auto simp: msub_double_diff)
have §: "∀m. c m ∈ R"
by (meson Ring.ipoly_carrier_coeff_closed Ring_axioms c)
have "(c ⊗⇩I imonom 𝟭 n) m = additive.fincomp (λp. if p = m - n then (λp. c p) p else 𝟬) {p. p ⊆# m}"
unfolding ipoly_mult_def
using c by (intro additive.fincomp_cong')
(auto simp: imonom_def unique ipoly_carrier_coeff_closed)
also have "… = c (m - n)"
using § by (simp add: additive.fincomp_singleton_swap finite_submultisets)
finally show ?thesis using True by simp
next
case False
then have "c p ⋅ imonom 𝟭 n (m - p) = 𝟬" if "p ∈ {p. p ⊆# m}" for p
by (metis c imonom_def ipoly_carrier_coeff_closed right_zero diff_subset_eq_self)
then have "(c ⊗⇩I imonom 𝟭 n) m = 𝟬"
unfolding ipoly_mult_def by (rule additive.fincomp_unit_eqI)
then show ?thesis using False by simp
qed
text ‹A power of an indeterminate is the monomial with that exponent.›
lemma ivar_pow:
fixes j :: 'i
shows "Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k = imonom 𝟭 (replicate_mset k j)"
proof (induct k)
case 0
have "Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) 0 = 𝟭⇩I"
by (rule Ring.rpow_0 [OF ipoly_ring])
then show ?case
by (simp add: ipoly_one_def imonom_def)
next
case (Suc k)
have "Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) (Suc k) = ivar j ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k"
by (rule Ring.rpow_Suc [OF ipoly_ring])
then show ?case
using Suc by (simp add: ivar_eq_imonom imonom_mult)
qed
subsection ‹Reading a polynomial off its value at an indeterminate›
text ‹The point of the monomial lemmas above. A sum ‹∑⇩k c⇩k X⇩j⇧k› whose coefficients do not involve
‹X⇩j› determines those coefficients: its value on a monomial ‹m› is the coefficient indexed by the
multiplicity of ‹j› in ‹m›, evaluated at what remains of ‹m›. So such a sum is injective in the
coefficients, which is what makes the realisation of a quotient ‹M[X]/(Q)› inside this ring
faithful.›
lemma ipoly_add_cmonoid: "commutative_monoid ipoly_carrier (⊕⇩I) 𝟬⇩I"
using ipoly_ring by (meson Abelian_Group_def Ring_def)
text ‹Addition is pointwise, so a finite sum may be evaluated coefficientwise.›
lemma ipoly_fincomp_apply:
fixes m :: "'i multiset"
assumes f: "⋀k. f k ∈ ipoly_carrier"
shows "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I f A m = additive.fincomp (λk. f k m) A"
proof (induction A rule: infinite_finite_induct)
case empty
have "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I f {} = 𝟬⇩I"
by (rule commutative_monoid.fincomp_empty [OF ipoly_add_cmonoid])
then show ?case by (simp add: ipoly_zero_def)
next
case (insert a A)
have "f ∈ A → ipoly_carrier" "f a ∈ ipoly_carrier" using f by auto
then have "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I f (insert a A) m
= f a m + commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I f A m"
using commutative_monoid.fincomp_insert [OF ipoly_add_cmonoid] insert.hyps
by (smt (verit) ipoly_add_def)
also have "… = additive.fincomp (λk. f k m) (insert a A)"
using insert.IH by (simp add: f insert.hyps ipoly_carrier_coeff_closed)
finally show ?case .
next
case infinite
then show ?case
using additive.commutative_monoid_axioms ipoly_add_cmonoid ipoly_zero_def
by (metis commutative_monoid.fincomp_def)
qed
lemma replicate_mset_subseteq_count: "replicate_mset k j ⊆# m ⟷ k ≤ count m j"
by (auto simp: subseteq_mset_def split: if_split_asm)
text ‹The closed form: only the term whose exponent matches the multiplicity of @{term j} in
@{term m} survives, because every earlier coefficient is evaluated at a monomial that still
involves @{term j}, where it vanishes.›
theorem ieval_ivar:
fixes j :: 'i and m :: "'i multiset"
assumes c: "⋀k. c k ∈ ipoly_carrier" and free: "⋀k. index_free (c k) j"
shows "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..d} m
= (if count m j ≤ d then c (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
proof -
have cl: "c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k ∈ ipoly_carrier" for k
using c by (simp add: ivar_pow ipoly_mult_closed imonom_closed)
have term_eq: "(c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) m
= (if k = count m j
then c (count m j) (m - replicate_mset (count m j) j) else 𝟬)" for k
proof -
have "(c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) m
= (if replicate_mset k j ⊆# m then c k (m - replicate_mset k j) else 𝟬)"
by (simp add: ivar_pow imonom_shift [OF c])
also have "… = (if k = count m j then c (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
using index_freeD [OF free]
by (cases "k < count m j") (auto simp: in_diff_count replicate_mset_subseteq_count)
finally show ?thesis .
qed
have "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..d} m
= additive.fincomp (λk. (c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) m) {..d}"
by (rule ipoly_fincomp_apply [OF cl])
also have "… = additive.fincomp
(λk. if k = count m j
then (λ_. c (count m j) (m - replicate_mset (count m j) j)) k
else 𝟬) {..d}"
using term_eq by simp
also have "… = (if count m j ≤ d
then c (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
proof (cases "count m j ≤ d")
case True
then show ?thesis
using assms(1)
by (auto intro!: ipoly_carrier_coeff_closed additive.fincomp_singleton_swap)
next
case False then show ?thesis
by (force intro!: additive.fincomp_unit_eqI)
qed
finally show ?thesis .
qed
text ‹What the closed form is for: the coefficients can be recovered, so a polynomial in
@{term "ivar j"} with index-free coefficients determines them. Reading @{thm [source] ieval_ivar}
at the monomial @{term "n + replicate_mset k j"} isolates the @{term k}th coefficient at
@{term n} --- provided @{term n} itself avoids @{term j}, and where it does not, both coefficients
vanish anyway. This is the injectivity that lets a quotient be realised by normal forms: distinct
remainders go to distinct elements of the ambient ring.›
lemma ieval_ivar_inj:
fixes j :: 'i and D k :: nat
assumes c: "⋀k. c k ∈ ipoly_carrier" and cfree: "⋀k. index_free (c k) j"
and d: "⋀k. d k ∈ ipoly_carrier" and dfree: "⋀k. index_free (d k) j"
and eq: "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..D}
= commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. d k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..D}"
and k: "k ≤ D"
shows "c k = d k"
proof (rule ext)
fix n :: "'i multiset"
show "c k n = d k n"
proof (cases "j ∈# n")
case True
show ?thesis
using index_freeD [OF cfree True] index_freeD [OF dfree True] by simp
next
case False
define m where "m ≡ n + replicate_mset k j"
have cm: "count m j = k" using False by (simp add: m_def not_in_iff)
have mn: "m - replicate_mset k j = n" by (simp add: m_def)
have ceq: "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. c k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..D} m
= (if count m j ≤ D
then c (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
by (rule ieval_ivar [OF c cfree])
have deq: "commutative_monoid.fincomp ipoly_carrier (⊕⇩I) 𝟬⇩I
(λk. d k ⊗⇩I Ring.rpow (⊗⇩I) 𝟭⇩I (ivar j) k) {..D} m
= (if count m j ≤ D
then d (count m j) (m - replicate_mset (count m j) j) else 𝟬)"
by (rule ieval_ivar [OF d dfree])
from ceq deq eq cm mn k show ?thesis by simp
qed
qed
end
section ‹Polynomials over a Commutative Ring›
context commutative_ring
begin
text ‹When the coefficients commute so do the polynomials: the convolution is symmetric under the
involution @{text "n ↦ m - n"} of the submultisets of @{text m}.›
lemma ipoly_mult_comm:
fixes p q :: "'i multiset ⇒ 'a"
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier"
shows "p ⊗⇩I q = q ⊗⇩I p"
proof
fix m :: "'i multiset"
have pi: "⋀n. p n ∈ R" and qi: "⋀n. q n ∈ R"
using p q by (auto simp: ipoly_carrier_coeff_closed)
have bij: "bij_betw (λn :: 'i multiset. m - n) {n. n ⊆# m} {n. n ⊆# m}"
by (rule bij_betw_byWitness [where f' = "λn :: 'i multiset. m - n"])
(auto simp: msub_double_diff diff_subset_eq_self)
have "(p ⊗⇩I q) m = additive.fincomp (λn. q (m - n) ⋅ p n) {n. n ⊆# m}"
by (simp add: ipoly_mult_def multiplicative.commutative pi qi)
also have "… = additive.fincomp (λn. q (m - n) ⋅ p n)
((λn :: 'i multiset. m - n) ` {n. n ⊆# m})"
using bij bij_betw_imp_surj_on by fastforce
also have "… = additive.fincomp (λn. q (m - (m - n)) ⋅ p (m - n)) {n. n ⊆# m}"
by (rule additive.fincomp_reindex)
(use pi qi bij bij_betw_imp_inj_on in auto)
also have "… = additive.fincomp (λn. q n ⋅ p (m - n)) {n. n ⊆# m}"
using pi qi by (intro additive.fincomp_cong') (auto simp: msub_double_diff)
also have "… = (q ⊗⇩I p) m" by (simp add: ipoly_mult_def)
finally show "(p ⊗⇩I q) m = (q ⊗⇩I p) m" .
qed
theorem ipoly_commutative_ring:
"commutative_ring (ipoly_carrier :: ('i multiset ⇒ 'a) set) (⊕⇩I) (⊗⇩I) 𝟬⇩I 𝟭⇩I"
proof -
interpret P: Ring "ipoly_carrier :: ('i multiset ⇒ 'a) set" "(⊕⇩I)" "(⊗⇩I)" "𝟬⇩I" "𝟭⇩I"
by (rule ipoly_ring)
show ?thesis
proof qed (simp add: ipoly_mult_comm)
qed
end
section ‹The Univariate Case, as a Check on the Convolution›
text ‹With a single indeterminate --- index type @{typ unit} --- a monomial is determined by its
size, so the submultisets of @{text "X⇧k"} are exactly @{text "X⇧i"} for @{text "i ≤ k"}, and the
indexed convolution must reduce to the univariate one of ‹Poly_Ring›. This is an independent
check on both the index set of the convolution and the placement of @{text "m - n"} within it: a
sum over the wrong factorisations of a monomial would still build a ring, and would still satisfy
every law proved above, but it would not agree with ‹Poly_Ring› here.›
lemma unit_mset_eq_replicate: "(n :: unit multiset) = replicate_mset (count n ()) ()"
by (simp add: multiset_eq_iff)
lemma submultisets_replicate_unit:
"{n :: unit multiset. n ⊆# replicate_mset k ()} = (λi. replicate_mset i ()) ` {..k}"
using unit_mset_eq_replicate
by (auto simp: subseteq_mset_def image_iff)
lemma replicate_unit_diff:
"replicate_mset k () - replicate_mset i () = replicate_mset (k - i) ()"
by (simp add: multiset_eq_iff)
lemma inj_on_replicate_unit: "inj_on (λi. replicate_mset i ()) {..k}"
by (rule inj_on_inverseI [where g = "λn. count n ()"]) simp
context Ring
begin
theorem ipoly_mult_unit_index:
fixes p q :: "unit multiset ⇒ 'a"
assumes p: "p ∈ ipoly_carrier" and q: "q ∈ ipoly_carrier"
shows "(p ⊗⇩I q) (replicate_mset k ())
= ((λi. p (replicate_mset i ())) ⊗⇩P (λi. q (replicate_mset i ()))) k"
proof -
have pi: "⋀n. p n ∈ R" and qi: "⋀n. q n ∈ R"
using p q by (auto simp: ipoly_carrier_coeff_closed)
have "(p ⊗⇩I q) (replicate_mset k ())
= additive.fincomp (λn. p n ⋅ q (replicate_mset k () - n))
((λi. replicate_mset i ()) ` {..k})"
by (simp add: ipoly_mult_def submultisets_replicate_unit)
also have "… = additive.fincomp
(λi. p (replicate_mset i ())
⋅ q (replicate_mset k () - replicate_mset i ())) {..k}"
by (rule additive.fincomp_reindex) (use pi qi inj_on_replicate_unit in auto)
also have "… = ((λi. p (replicate_mset i ())) ⊗⇩P (λi. q (replicate_mset i ()))) k"
by (simp add: replicate_unit_diff poly_mult_def)
finally show ?thesis .
qed
end
end