Theory Polynomial_Interpolation.Missing_Polynomial
section ‹Missing Polynomial›
text ‹The theory contains some basic results on polynomials which have not been detected in
the distribution, especially on linear factors and degrees.›
theory Missing_Polynomial
imports
"HOL-Computational_Algebra.Polynomial_Factorial"
Missing_Unsorted
begin
text ‹A nice extension rule for polynomials.›
declare poly_ext[intro]
subsection ‹Basic Properties›
lemma degree_lcoeff_sum: assumes deg: "degree (f q) = n"
and fin: "finite S" and q: "q ∈ S" and degle: "⋀ p . p ∈ S - {q} ⟹ degree (f p) < n"
and cong: "coeff (f q) n = c"
shows "degree (sum f S) = n ∧ coeff (sum f S) n = c"
proof (cases "S = {q}")
case True
thus ?thesis using deg cong by simp
next
case False
with q obtain p where "p ∈ S - {q}" by auto
from degle[OF this] have n: "n > 0" by auto
have "degree (sum f S) = degree (f q + sum f (S - {q}))"
unfolding sum.remove[OF fin q] ..
also have "… = degree (f q)"
proof (rule degree_add_eq_left)
have "degree (sum f (S - {q})) ≤ n - 1"
proof (rule degree_sum_le)
fix p
show "p ∈ S - {q} ⟹ degree (f p) ≤ n - 1"
using degle[of p] by auto
qed (insert fin, auto)
also have "… < n" using n by simp
finally show "degree (sum f (S - {q})) < degree (f q)" unfolding deg .
qed
finally show ?thesis unfolding deg[symmetric] cong[symmetric]
proof
have id: "(∑x∈S - {q}. coeff (f x) (degree (f q))) = 0"
by (rule sum.neutral, rule ballI, rule coeff_eq_0[OF degle[folded deg]])
show "coeff (sum f S) (degree (f q)) = coeff (f q) (degree (f q))"
unfolding coeff_sum
by (subst sum.remove[OF _ q], unfold id, insert fin, auto)
qed
qed
subsection ‹Polynomial Composition›
lemmas [simp] = pcompose_pCons
declare degree_pcompose[simp]
subsection ‹Monic Polynomials›
abbreviation monic where "monic p ≡ coeff p (degree p) = 1"
lemma unit_factor_field [simp]:
"unit_factor (x :: 'a :: {field,normalization_semidom}) = x"
by (cases "is_unit x") (auto simp: is_unit_unit_factor dvd_field_iff)
lemma poly_gcd_monic:
fixes p :: "'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
assumes "p ≠ 0 ∨ q ≠ 0"
shows "monic (gcd p q)"
by (metis assms gcd_eq_0_iff gcd_unique lead_coeff_normalize_field)
lemma normalize_monic: "monic p ⟹ normalize p = p"
by (simp add: normalize_poly_eq_map_poly is_unit_unit_factor)
lemma lcoeff_monic_mult:
assumes monic: "monic (p :: 'a :: comm_semiring_1 poly)"
shows "coeff (p * q) (degree p + degree q) = coeff q (degree q)"
proof -
let ?pqi = "λ i. coeff p i * coeff q (degree p + degree q - i)"
have "coeff (p * q) (degree p + degree q) =
(∑i≤degree p + degree q. ?pqi i)"
unfolding coeff_mult by simp
also have "… = ?pqi (degree p) + (sum ?pqi ({.. degree p + degree q} - {degree p}))"
by (subst sum.remove[of _ "degree p"], auto)
also have "?pqi (degree p) = coeff q (degree q)" unfolding monic by simp
also have "(sum ?pqi ({.. degree p + degree q} - {degree p})) = 0"
proof (rule sum.neutral, intro ballI)
fix d
assume d: "d ∈ {.. degree p + degree q} - {degree p}"
show "?pqi d = 0"
proof (cases "d < degree p")
case True
hence "degree p + degree q - d > degree q" by auto
hence "coeff q (degree p + degree q - d) = 0" by (rule coeff_eq_0)
thus ?thesis by simp
next
case False
with d have "d > degree p" by auto
hence "coeff p d = 0" by (rule coeff_eq_0)
thus ?thesis by simp
qed
qed
finally show ?thesis by simp
qed
lemma degree_monic_mult:
fixes p :: "'a :: comm_semiring_1 poly"
assumes "monic p" and "q ≠ 0"
shows "degree (p * q) = degree p + degree q"
by (simp add: coeff_mult_degree_sum degree_mult_le le_antisym le_degree assms)
lemma degree_prod_sum_monic:
assumes S: "finite S"
and nzd: "0 ∉ (degree o f) ` S"
and monic: "(⋀ a . a ∈ S ⟹ monic (f a))"
shows "degree (prod f S) = (sum (degree o f) S) ∧ coeff (prod f S) (sum (degree o f) S) = 1"
proof -
from S nzd monic
have "degree (prod f S) = sum (degree ∘ f) S
∧ (S ≠ {} ⟶ degree (prod f S) ≠ 0 ∧ prod f S ≠ 0) ∧ coeff (prod f S) (sum (degree o f) S) = 1"
proof (induct S rule: finite_induct)
case (insert a S)
have IH1: "degree (prod f S) = sum (degree o f) S"
using insert by auto
have IH2: "coeff (prod f S) (degree (prod f S)) = 1"
using insert by auto
have id: "degree (prod f (insert a S)) = sum (degree ∘ f) (insert a S)
∧ coeff (prod f (insert a S)) (sum (degree o f) (insert a S)) = 1"
proof (cases "S = {}")
case False
with insert have nz: "prod f S ≠ 0" by auto
from insert have monic: "coeff (f a) (degree (f a)) = 1" by auto
have id: "(degree ∘ f) a = degree (f a)" by simp
show ?thesis unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] id
unfolding degree_monic_mult[OF monic nz]
unfolding IH1[symmetric]
unfolding lcoeff_monic_mult[OF monic] IH2 by simp
qed (insert insert, auto)
show ?case using id unfolding sum.insert[OF insert(1-2)] using insert by auto
qed simp
thus ?thesis by auto
qed
lemma degree_prod_monic:
assumes "⋀ i. i < n ⟹ degree (f i :: 'a :: comm_semiring_1 poly) = 1"
and "⋀ i. i < n ⟹ coeff (f i) 1 = 1"
shows "degree (prod f {0 ..< n}) = n ∧ coeff (prod f {0 ..< n}) n = 1"
using assms degree_prod_sum_monic[of "{0 ..< n}" f] by force
lemma degree_prod_sum_lt_n:
assumes "⋀ i. i < n ⟹ degree (f i :: 'a :: comm_semiring_1 poly) ≤ 1"
and i: "i < n" and fi: "degree (f i) = 0"
shows "degree (prod f {0 ..< n}) < n"
proof -
have "degree (prod f {0 ..< n}) ≤ sum (degree o f) {0 ..< n}"
by (rule degree_prod_sum_le, auto)
also have "sum (degree o f) {0 ..< n} = (degree o f) i + sum (degree o f) ({0 ..< n} - {i})"
by (rule sum.remove, insert i, auto)
also have "(degree o f) i = 0" using fi by simp
also have "sum (degree o f) ({0 ..< n} - {i}) ≤ sum (λ _. 1) ({0 ..< n} - {i})"
by (rule sum_mono, insert assms, auto)
also have "… = n - 1" using i by simp
also have "… < n" using i by simp
finally show ?thesis by simp
qed
lemma degree_linear_factors: "degree (∏ a ← as. [: f a, 1:]) = length as"
proof (induct as)
case (Cons b as) note IH = this
have id: "(∏a←b # as. [:f a, 1:]) = [:f b,1 :] * (∏a←as. [:f a, 1:])" by simp
show ?case unfolding id
by (subst degree_monic_mult, insert IH, auto)
qed simp
lemma monic_mult:
fixes p q :: "'a :: idom poly"
assumes "monic p" "monic q"
shows "monic (p * q)"
by (simp add: assms coeff_degree_mult)
lemma monic_factor:
fixes p q :: "'a :: idom poly"
assumes "monic (p * q)" "monic p"
shows "monic q"
by (metis assms coeff_degree_mult mult.comm_neutral)
lemma monic_prod:
fixes f :: "'a ⇒ 'b :: idom poly"
assumes "⋀ a. a ∈ as ⟹ monic (f a)"
shows "monic (prod f as)" using assms
proof (induct as rule: infinite_finite_induct)
case (insert a as)
hence id: "prod f (insert a as) = f a * prod f as"
and *: "monic (f a)" "monic (prod f as)" by auto
show ?case unfolding id by (rule monic_mult[OF *])
qed auto
lemma monic_prod_list:
fixes as :: "'a :: idom poly list"
assumes "⋀ a. a ∈ set as ⟹ monic a"
shows "monic (prod_list as)" using assms
by (induct as, auto intro: monic_mult)
lemma monic_power:
assumes "monic (p :: 'a :: idom poly)"
shows "monic (p ^ n)"
by (simp add: assms lead_coeff_power)
lemma monic_prod_list_pow: "monic (∏(x::'a::idom, i)←xis. [:- x, 1:] ^ Suc i)"
proof (rule monic_prod_list, goal_cases)
case (1 a)
then obtain x i where a: "a = [:-x, 1:]^Suc i" by force
show "monic a" unfolding a
by (rule monic_power, auto)
qed
lemma monic_degree_0: "monic p ⟹ (degree p = 0) = (p = 1)"
using le_degree poly_eq_iff by force
subsection ‹Roots›
text ‹The following proof structure is completely similar to the one
of @{thm poly_roots_finite}.›
lemma poly_root_factor: "(poly ([: r, 1:] * q) (k :: 'a :: idom) = 0) = (k = -r ∨ poly q k = 0)" (is ?one)
"(poly (q * [: r, 1:]) k = 0) = (k = -r ∨ poly q k = 0)" (is ?two)
"(poly [: r, 1 :] k = 0) = (k = -r)" (is ?three)
proof -
have [simp]: "r + k = 0 ⟹ k = - r" by (simp add: minus_unique)
show ?one unfolding poly_mult by auto
show ?two unfolding poly_mult by auto
show ?three by auto
qed
lemma poly_root_constant: "c ≠ 0 ⟹ (poly (p * [:c:]) (k :: 'a :: idom) = 0) = (poly p k = 0)"
unfolding poly_mult by auto
lemma poly_linear_exp_linear_factors_rev:
"([:b,1:])^(length (filter ((=) b) as)) dvd (∏ (a :: 'a :: comm_ring_1) ← as. [: a, 1:])"
proof (induct as)
case (Cons a as)
let ?ls = "length (filter ((=) b) (a # as))"
let ?l = "length (filter ((=) b) as)"
have prod: "(∏ a ← Cons a as. [: a, 1:]) = [: a, 1 :] * (∏ a ← as. [: a, 1:])" by simp
show ?case
proof (cases "a = b")
case False
hence len: "?ls = ?l" by simp
show ?thesis unfolding prod len using Cons by (rule dvd_mult)
next
case True
hence len: "[: b, 1 :] ^ ?ls = [: a, 1 :] * [: b, 1 :] ^ ?l" by simp
show ?thesis unfolding prod len using Cons using dvd_refl mult_dvd_mono by blast
qed
qed simp
lemma order_max: assumes dvd: "[: -a, 1 :] ^ k dvd p" and p: "p ≠ 0"
shows "k ≤ order a p"
using dvd order_divides p by blast
text ‹Degree based version of irreducibility.›
definition irreducible⇩d :: "'a :: comm_semiring_1 poly ⇒ bool" where
"irreducible⇩d p = (degree p > 0 ∧ (∀ q r. degree q < degree p ⟶ degree r < degree p ⟶ p ≠ q * r))"
lemma irreducible⇩dI [intro]:
assumes 1: "degree p > 0"
and 2: "⋀q r. degree q > 0 ⟹ degree q < degree p ⟹ degree r > 0 ⟹ degree r < degree p ⟹ p = q * r ⟹ False"
shows "irreducible⇩d p"
proof (unfold irreducible⇩d_def, intro conjI allI impI notI 1)
fix q r
assume "degree q < degree p" and "degree r < degree p" and "p = q * r"
with degree_mult_le[of q r]
show False by (intro 2, auto)
qed
lemma irreducible⇩dI2:
fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes deg: "degree p > 0" and ndvd: "⋀ q. degree q > 0 ⟹ degree q ≤ degree p div 2 ⟹ ¬ q dvd p"
shows "irreducible⇩d p"
proof (rule ccontr)
assume "¬ ?thesis"
from this[unfolded irreducible⇩d_def] deg obtain q r where dq: "degree q < degree p" and dr: "degree r < degree p"
and p: "p = q * r" by auto
from deg have p0: "p ≠ 0" by auto
with p have "q ≠ 0" "r ≠ 0" by auto
from degree_mult_eq[OF this] p have dp: "degree p = degree q + degree r" by simp
show False
proof (cases "degree q ≤ degree p div 2")
case True
from ndvd[OF _ True] dq dr dp p show False by auto
next
case False
with dp have dr: "degree r ≤ degree p div 2" by auto
from p have dvd: "r dvd p" by auto
from ndvd[OF _ dr] dvd dp dq show False by auto
qed
qed
lemma reducible⇩dI:
assumes "degree p > 0 ⟹ ∃q r. degree q < degree p ∧ degree r < degree p ∧ p = q * r"
shows "¬ irreducible⇩d p"
using assms by (auto simp: irreducible⇩d_def)
lemma irreducible⇩dE [elim]:
assumes "irreducible⇩d p"
and "degree p > 0 ⟹ (⋀q r. degree q < degree p ⟹ degree r < degree p ⟹ p ≠ q * r) ⟹ thesis"
shows thesis
using assms by (auto simp: irreducible⇩d_def)
lemma reducible⇩dE [elim]:
assumes "¬ irreducible⇩d p"
and "degree p = 0 ⟹ thesis"
and "⋀q r. degree q > 0 ⟹ degree q < degree p ⟹ degree r > 0 ⟹ degree r < degree p ⟹ p = q * r ⟹ thesis"
shows thesis
using assms by blast
lemma irreducible⇩dD:
assumes "irreducible⇩d p"
shows "degree p > 0" "⋀q r. degree q < degree p ⟹ degree r < degree p ⟹ p ≠ q * r"
using assms unfolding irreducible⇩d_def by auto
theorem irreducible⇩d_factorization_exists:
assumes "degree p > 0"
shows "∃fs. fs ≠ [] ∧ (∀f ∈ set fs. irreducible⇩d f ∧ degree f ≤ degree p) ∧ p = prod_list fs"
and "¬irreducible⇩d p ⟹ ∃fs. length fs > 1 ∧ (∀f ∈ set fs. irreducible⇩d f ∧ degree f < degree p) ∧ p = prod_list fs"
proof (atomize(full), insert assms, induct "degree p" arbitrary:p rule: less_induct)
case less
then have deg_f: "degree p > 0" by auto
show ?case
proof (cases "irreducible⇩d p")
case True
then have "set [p] ⊆ Collect irreducible⇩d" "p = prod_list [p]" by auto
with True show ?thesis by (auto intro: exI[of _ "[p]"])
next
case False
with deg_f obtain g h
where deg_g: "degree g < degree p" "degree g > 0"
and deg_h: "degree h < degree p" "degree h > 0"
and f_gh: "p = g * h" by auto
from less.hyps[OF deg_g] less.hyps[OF deg_h]
obtain gs hs
where emp: "length gs > 0" "length hs > 0"
and "∀f ∈ set gs. irreducible⇩d f ∧ degree f ≤ degree g" "g = prod_list gs"
and "∀f ∈ set hs. irreducible⇩d f ∧ degree f ≤ degree h" "h = prod_list hs" by auto
with f_gh deg_g deg_h
have len: "length (gs@hs) > 1"
and mem: "∀f ∈ set (gs@hs). irreducible⇩d f ∧ degree f < degree p"
and p: "p = prod_list (gs@hs)" by (auto simp del: length_greater_0_conv)
with False show ?thesis by (auto intro!: exI[of _ "gs@hs"] simp: less_imp_le)
qed
qed
lemma irreducible⇩d_factor:
fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes "degree p > 0"
shows "∃ q r. irreducible⇩d q ∧ p = q * r ∧ degree r < degree p" using assms
proof (induct "degree p" arbitrary: p rule: less_induct)
case (less p)
show ?case
proof (cases "irreducible⇩d p")
case False
with less(2) obtain q r
where q: "degree q < degree p" "degree q > 0"
and r: "degree r < degree p" "degree r > 0"
and p: "p = q * r"
by auto
from less(1)[OF q] obtain s t where IH: "irreducible⇩d s" "q = s * t" by auto
from p have p: "p = s * (t * r)" unfolding IH by (simp add: ac_simps)
from less(2) have "p ≠ 0" by auto
hence "degree p = degree s + (degree (t * r))" unfolding p
by (subst degree_mult_eq, insert p, auto)
with irreducible⇩dD[OF IH(1)] have "degree p > degree (t * r)" by auto
with p IH show ?thesis by auto
next
case True
show ?thesis
by (rule exI[of _ p], rule exI[of _ 1], insert True less(2), auto)
qed
qed
context mult_zero begin
definition zero_divisor where "zero_divisor a ≡ ∃b. b ≠ 0 ∧ a * b = 0"
lemma zero_divisorI[intro]:
assumes "b ≠ 0" and "a * b = 0" shows "zero_divisor a"
using assms by (auto simp: zero_divisor_def)
lemma zero_divisorE[elim]:
assumes "zero_divisor a"
and "⋀b. b ≠ 0 ⟹ a * b = 0 ⟹ thesis"
shows thesis
using assms by (auto simp: zero_divisor_def)
end
lemma zero_divisor_0[simp]:
"zero_divisor (0::'a::{mult_zero,zero_neq_one})"
by (auto intro!: zero_divisorI[of 1])
lemma not_zero_divisor_1:
"¬ zero_divisor (1 :: 'a :: {monoid_mult,mult_zero})"
by auto
lemma zero_divisor_iff_eq_0[simp]:
fixes a :: "'a :: {semiring_no_zero_divisors, zero_neq_one}"
shows "zero_divisor a ⟷ a = 0" by auto
lemma mult_eq_0_not_zero_divisor_left[simp]:
fixes a b :: "'a :: mult_zero"
assumes "¬ zero_divisor a"
shows "a * b = 0 ⟷ b = 0"
using assms unfolding zero_divisor_def by force
lemma mult_eq_0_not_zero_divisor_right[simp]:
fixes a b :: "'a :: {ab_semigroup_mult,mult_zero}"
assumes "¬ zero_divisor b"
shows "a * b = 0 ⟷ a = 0"
using assms unfolding zero_divisor_def by (force simp: ac_simps)
lemma degree_smult_not_zero_divisor_left[simp]:
assumes "¬ zero_divisor c"
shows "degree (smult c p) = degree p"
proof(cases "p = 0")
case False
then have "coeff (smult c p) (degree p) ≠ 0" using assms by auto
from le_degree[OF this] degree_smult_le[of c p]
show ?thesis by auto
qed auto
lemma degree_smult_not_zero_divisor_right[simp]:
assumes "¬ zero_divisor (lead_coeff p)"
shows "degree (smult c p) = (if c = 0 then 0 else degree p)"
proof(cases "c = 0")
case False
then have "coeff (smult c p) (degree p) ≠ 0" using assms by auto
from le_degree[OF this] degree_smult_le[of c p]
show ?thesis by auto
qed auto
lemma irreducible⇩d_smult_not_zero_divisor_left:
assumes c0: "¬ zero_divisor c"
assumes L: "irreducible⇩d (smult c p)"
shows "irreducible⇩d p"
proof (intro irreducible⇩dI)
from L have "degree (smult c p) > 0" by auto
also note degree_smult_le
finally show "degree p > 0" by auto
fix q r
assume §: "degree q < degree p" "degree r < degree p" and "p = q * r"
then have 1: "smult c p = smult c q * r" by auto
with § degree_smult_le[of c q] show False
by (metis L c0 degree_smult_not_zero_divisor_left reducible⇩dI)
qed
lemmas irreducible⇩d_smultI =
irreducible⇩d_smult_not_zero_divisor_left
[where 'a = "'a :: {comm_semiring_1,semiring_no_zero_divisors}", simplified]
lemma irreducible⇩d_smult_not_zero_divisor_right:
assumes p0: "¬ zero_divisor (lead_coeff p)" and L: "irreducible⇩d (smult c p)"
shows "irreducible⇩d p"
proof-
from L have "c ≠ 0" by auto
with p0 have [simp]: "degree (smult c p) = degree p" by simp
show "irreducible⇩d p"
proof (intro iffI irreducible⇩dI conjI)
from L show "degree p > 0" by auto
fix q r
assume deg_q: "degree q < degree p"
and deg_r: "degree r < degree p"
and p_qr: "p = q * r"
then have 1: "smult c p = smult c q * r" by auto
note degree_smult_le[of c q]
also note deg_q
finally have 2: "degree (smult c q) < degree (smult c p)" by simp
from deg_r have 3: "degree r < …" by simp
from irreducible⇩dD(2)[OF L 2 3] 1 show False by auto
qed
qed
lemma zero_divisor_mult_left:
fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}"
assumes "zero_divisor a"
shows "zero_divisor (a * b)"
proof-
from assms obtain c where c0: "c ≠ 0" and [simp]: "a * c = 0" by auto
have "a * b * c = a * c * b" by (simp only: ac_simps)
with c0 show ?thesis by auto
qed
lemma zero_divisor_mult_right:
fixes a b :: "'a :: {semigroup_mult, mult_zero}"
assumes "zero_divisor b"
shows "zero_divisor (a * b)"
by (metis assms mult.assoc mult_zero_right zero_divisor_def)
lemma not_zero_divisor_mult:
fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}"
assumes "¬ zero_divisor (a * b)"
shows "¬ zero_divisor a" and "¬ zero_divisor b"
using assms zero_divisor_mult_left zero_divisor_mult_right by blast+
lemma zero_divisor_smult_left:
assumes "zero_divisor a"
shows "zero_divisor (smult a f)"
proof-
from assms obtain b where b0: "b ≠ 0" and "a * b = 0" by auto
then have "smult a f * [:b:] = 0" by (simp add: ac_simps)
with b0 show ?thesis by (auto intro!: zero_divisorI[of "[:b:]"])
qed
lemma unit_not_zero_divisor:
fixes a :: "'a :: {comm_monoid_mult, mult_zero}"
assumes "a dvd 1"
shows "¬zero_divisor a"
proof
from assms obtain b where ab: "1 = a * b" by (elim dvdE)
assume "zero_divisor a"
then have "zero_divisor (1::'a)" by (unfold ab, intro zero_divisor_mult_left)
then show False by auto
qed
lemma linear_irreducible⇩d: assumes "degree p = 1"
shows "irreducible⇩d p"
by (rule irreducible⇩dI, insert assms, auto)
lemma irreducible⇩d_dvd_smult:
fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes "degree p > 0" "irreducible⇩d q" "p dvd q"
shows "∃ c. c ≠ 0 ∧ q = smult c p"
proof -
from assms obtain r where q: "q = p * r" by (elim dvdE, auto)
from degree_mult_eq[of p r] assms(1) q
obtain "¬ degree p < degree q" and nz: "p ≠ 0" "q ≠ 0"
by (metis assms(2) degree_0 less_add_same_cancel2 less_irrefl reducible⇩dI)
hence deg: "degree p ≥ degree q" by auto
from ‹p dvd q› obtain k where q: "q = k * p" unfolding dvd_def by (auto simp: ac_simps)
with nz have "k ≠ 0" by auto
from deg[unfolded q degree_mult_eq[OF ‹k ≠ 0› ‹p ≠ 0› ]] have "degree k = 0"
unfolding q by auto
then obtain c where k: "k = [: c :]"
using degree_eq_zeroE by blast
with ‹k ≠ 0› have "c ≠ 0" by auto
have "q = smult c p" unfolding q k by simp
with ‹c ≠ 0› show ?thesis by auto
qed
subsection ‹Map over Polynomial Coefficients›
lemma map_poly_simps:
shows "map_poly f (pCons c p) =
(if c = 0 ∧ p = 0 then 0 else pCons (f c) (map_poly f p))"
proof (cases "c = 0")
case True note c0 = this show ?thesis
proof (cases "p = 0")
case True thus ?thesis using c0 unfolding map_poly_def by simp
next case False thus ?thesis
unfolding map_poly_def by auto
qed
next case False thus ?thesis
unfolding map_poly_def by auto
qed
lemma map_poly_pCons[simp]:
assumes "c ≠ 0 ∨ p ≠ 0"
shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
unfolding map_poly_simps using assms by auto
lemma map_poly_map_poly:
assumes f0: "f 0 = 0"
shows "map_poly f (map_poly g p) = map_poly (f ∘ g) p"
proof (induct p)
case (pCons a p) show ?case
proof(cases "g a ≠ 0 ∨ map_poly g p ≠ 0")
case True show ?thesis
unfolding map_poly_pCons[OF pCons(1)]
unfolding map_poly_pCons[OF True]
unfolding pCons(2)
by simp
next
case False then show ?thesis
unfolding map_poly_pCons[OF pCons(1)]
unfolding pCons(2)[symmetric]
by (simp add: f0)
qed
qed simp
lemma map_poly_zero:
assumes f: "∀c. f c = 0 ⟶ c = 0"
shows [simp]: "map_poly f p = 0 ⟷ p = 0"
by (induct p; auto simp: map_poly_simps f)
lemma map_poly_add:
assumes h0: "h 0 = 0"
and h_add: "∀p q. h (p + q) = h p + h q"
shows "map_poly h (p + q) = map_poly h p + map_poly h q"
proof (induct p arbitrary: q)
case (pCons a p) note pIH = this
show ?case
proof(induct "q")
case (pCons b q) note qIH = this
show ?case
unfolding map_poly_pCons[OF qIH(1)]
unfolding map_poly_pCons[OF pIH(1)]
unfolding add_pCons
unfolding pIH(2)[symmetric]
unfolding h_add[rule_format,symmetric]
unfolding map_poly_simps using h0 by auto
qed auto
qed auto
subsection ‹Misc›
fun expand_powers :: "(nat × 'a)list ⇒ 'a list" where
"expand_powers [] = []"
| "expand_powers ((Suc n, a) # ps) = a # expand_powers ((n,a) # ps)"
| "expand_powers ((0,a) # ps) = expand_powers ps"
lemma expand_powers: fixes f :: "'a ⇒ 'b :: comm_ring_1"
shows "(∏ (n,a) ← n_as. f a ^ n) = (∏ a ← expand_powers n_as. f a)"
by (rule sym, induct n_as rule: expand_powers.induct, auto)
lemma poly_smult_zero_iff: fixes x :: "'a :: idom"
shows "(poly (smult a p) x = 0) = (a = 0 ∨ poly p x = 0)"
by simp
lemma poly_prod_list_zero_iff:
fixes x :: "'a :: idom"
shows "(poly (prod_list ps) x = 0) = (∃ p ∈ set ps. poly p x = 0)"
by (induct ps, auto)
lemma poly_mult_zero_iff:
fixes x :: "'a :: idom"
shows "(poly (p * q) x = 0) = (poly p x = 0 ∨ poly q x = 0)"
by simp
lemma poly_power_zero_iff:
fixes x :: "'a :: idom"
shows "(poly (p^n) x = 0) = (n ≠ 0 ∧ poly p x = 0)"
by auto
lemma sum_monom_0_iff: assumes fin: "finite S"
and g: "⋀ i j. g i = g j ⟹ i = j"
shows "sum (λ i. monom (f i) (g i)) S = 0 ⟷ (∀ i ∈ S. f i = 0)" (is "?l = ?r")
proof -
{
assume "¬ ?r"
then obtain i where i: "i ∈ S" and fi: "f i ≠ 0" by auto
let ?g = "λ i. monom (f i) (g i)"
have "coeff (sum ?g S) (g i) = f i + sum (λ j. coeff (?g j) (g i)) (S - {i})"
by (unfold sum.remove[OF fin i], simp add: coeff_sum)
also have "sum (λ j. coeff (?g j) (g i)) (S - {i}) = 0"
by (rule sum.neutral, insert g, auto)
finally have "coeff (sum ?g S) (g i) ≠ 0" using fi by auto
hence "¬ ?l" by auto
}
thus ?thesis by auto
qed
lemma degree_prod_list_eq: assumes "⋀ p. p ∈ set ps ⟹ (p :: 'a :: idom poly) ≠ 0"
shows "degree (prod_list ps) = sum_list (map degree ps)" using assms
proof (induct ps)
case (Cons p ps)
show ?case unfolding prod_list.Cons
by (subst degree_mult_eq, insert Cons, auto simp: prod_list_zero_iff)
qed simp
lemma degree_power_eq: assumes p: "p ≠ 0"
shows "degree (p ^ n) = degree (p :: 'a :: idom poly) * n"
proof (induct n)
case (Suc n)
from p have pn: "p ^ n ≠ 0" by auto
show ?case using degree_mult_eq[OF p pn] Suc by auto
qed simp
lemma coeff_Poly: "coeff (Poly xs) i = (nth_default 0 xs i)"
unfolding nth_default_coeffs_eq[of "Poly xs", symmetric] coeffs_Poly by simp
lemma rsquarefree_def': "rsquarefree p = (p ≠ 0 ∧ (∀a. order a p ≤ 1))"
proof -
have "⋀ a. order a p ≤ 1 ⟷ order a p = 0 ∨ order a p = 1" by linarith
thus ?thesis unfolding rsquarefree_def by auto
qed
lemma order_prod_list: "(⋀ p. p ∈ set ps ⟹ p ≠ 0) ⟹ order x (prod_list ps) = sum_list (map (order x) ps)"
by (induct ps, auto, subst order_mult, auto simp: prod_list_zero_iff)
lemma irreducible⇩d_dvd_eq:
fixes a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
assumes "irreducible⇩d a" and "irreducible⇩d b"
and "a dvd b"
and "monic a" and "monic b"
shows "a = b"
using assms
by (metis (no_types, lifting) coeff_smult degree_smult_eq irreducible⇩dD(1) irreducible⇩d_dvd_smult
mult.right_neutral smult_1_left)
lemma monic_gcd_dvd:
assumes fg: "f dvd g" and mon: "monic f" and gcd: "gcd g h ∈ {1, g}"
shows "gcd f h ∈ {1, f}"
proof (cases "coprime g h")
case True
with dvd_refl have "coprime f h"
using fg by (blast intro: coprime_divisors)
then show ?thesis
by simp
next
case False
with gcd have gcd: "gcd g h = g"
by (simp add: coprime_iff_gcd_eq_1)
with fg have "f dvd gcd g h"
by simp
then have "f dvd h"
by simp
then have "gcd f h = normalize f"
by (simp add: gcd_proj1_iff)
also have "normalize f = f"
using mon by (rule normalize_monic)
finally show ?thesis
by simp
qed
lemma monom_power: "(monom a b)^n = monom (a^n) (b*n)"
by (induct n, auto simp add: mult_monom)
lemma poly_const_pow: "[:a:]^b = [:a^b:]"
by (metis Groups.mult_ac(2) monom_0 monom_power mult_zero_right)
lemma degree_pderiv_le: "degree (pderiv f) ≤ degree f - 1"
proof (rule ccontr)
assume "¬ ?thesis"
hence ge: "degree (pderiv f) ≥ Suc (degree f - 1)" by auto
hence "pderiv f ≠ 0" by auto
hence "coeff (pderiv f) (degree (pderiv f)) ≠ 0" by auto
from this[unfolded coeff_pderiv]
have "coeff f (Suc (degree (pderiv f))) ≠ 0" by auto
moreover have "Suc (degree (pderiv f)) > degree f" using ge by auto
ultimately show False by (simp add: coeff_eq_0)
qed
lemma map_div_is_smult_inverse: "map_poly (λx. x / (a :: 'a :: field)) p = smult (inverse a) p"
unfolding smult_conv_map_poly
by (simp add: divide_inverse_commute)
lemma normalize_poly_old_def:
"normalize (f :: 'a :: {normalization_semidom,field} poly) = smult (inverse (unit_factor (lead_coeff f))) f"
by (simp add: normalize_poly_eq_map_poly map_div_is_smult_inverse)
lemma poly_dvd_antisym:
fixes p q :: "'b::idom poly"
assumes coeff: "coeff p (degree p) = coeff q (degree q)"
assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
proof (cases "p = 0")
case True with coeff show "p = q" by simp
next
case False with coeff have "q ≠ 0" by auto
have degree: "degree p = degree q"
using ‹p dvd q› ‹q dvd p› ‹p ≠ 0› ‹q ≠ 0›
by (intro order_antisym dvd_imp_degree_le)
from ‹p dvd q› obtain a where a: "q = p * a" ..
with ‹q ≠ 0› have "a ≠ 0" by auto
with degree a ‹p ≠ 0› have "degree a = 0"
by (simp add: degree_mult_eq)
with coeff a show "p = q"
by (cases a, auto split: if_splits)
qed
lemma coeff_f_0_code[code_unfold]: "coeff f 0 = (case coeffs f of [] ⇒ 0 | x # _ ⇒ x)"
by (cases f, auto simp: cCons_def)
lemma poly_compare_0_code[code_unfold]: "(f = 0) = (case coeffs f of [] ⇒ True | _ ⇒ False)"
using coeffs_eq_Nil list.disc_eq_case(1) by blast
text ‹Getting more efficient code for abbreviation @{term lead_coeff}"›
definition leading_coeff
where [code_abbrev, simp]: "leading_coeff = lead_coeff"
lemma leading_coeff_code [code]:
"leading_coeff f = (let xs = coeffs f in if xs = [] then 0 else last xs)"
by (simp add: last_coeffs_eq_coeff_degree)
lemma nth_coeffs_coeff: "i < length (coeffs f) ⟹ coeffs f ! i = coeff f i"
by (metis nth_default_coeffs_eq nth_default_def)
definition monom_mult :: "nat ⇒ 'a :: comm_semiring_1 poly ⇒ 'a poly"
where "monom_mult n f = monom 1 n * f"
lemma monom_mult_unfold [code_unfold]:
"monom 1 n * f = monom_mult n f"
"f * monom 1 n = monom_mult n f"
by (auto simp: monom_mult_def ac_simps)
lemma monom_mult_code [code abstract]:
"coeffs (monom_mult n f) = (let xs = coeffs f in
if xs = [] then xs else replicate n 0 @ xs)"
by (rule coeffs_eqI)
(auto simp add: Let_def monom_mult_def coeff_monom_mult nth_default_append nth_default_coeffs_eq)
lemma coeff_pcompose_monom: fixes f :: "'a :: comm_ring_1 poly"
assumes n: "j < n"
shows "coeff (f ∘⇩p monom 1 n) (n * i + j) = (if j = 0 then coeff f i else 0)"
proof (induct f arbitrary: i)
case (pCons a f i)
note d = pcompose_pCons coeff_add coeff_monom_mult coeff_pCons
show ?case
proof (cases i)
case 0
show ?thesis unfolding d 0 using n by (cases j, auto)
next
case (Suc ii)
have id: "n * Suc ii + j - n = n * ii + j" using n by (simp add: diff_mult_distrib2)
have id1: "(n ≤ n * Suc ii + j) = True" by auto
have id2: "(case n * Suc ii + j of 0 ⇒ a | Suc x ⇒ coeff 0 x) = 0" using n
by (cases "n * Suc ii + j", auto)
show ?thesis unfolding d Suc id id1 id2 pCons(2) if_True by auto
qed
qed auto
lemma coeff_pcompose_x_pow_n: fixes f :: "'a :: comm_ring_1 poly"
assumes n: "n ≠ 0"
shows "coeff (f ∘⇩p monom 1 n) (n * i) = coeff f i"
using coeff_pcompose_monom[of 0 n f i] n by auto
lemma dvd_dvd_smult: "a dvd b ⟹ f dvd g ⟹ smult a f dvd smult b g"
unfolding dvd_def by (metis mult_smult_left mult_smult_right smult_smult)
definition sdiv_poly :: "'a :: idom_divide poly ⇒ 'a ⇒ 'a poly" where
"sdiv_poly p a = (map_poly (λ c. c div a) p)"
lemma smult_map_poly: "smult a = map_poly ((*) a)"
by (rule ext, rule poly_eqI, subst coeff_map_poly, auto)
lemma smult_exact_sdiv_poly: assumes "⋀ c. c ∈ set (coeffs p) ⟹ a dvd c"
shows "smult a (sdiv_poly p a) = p"
unfolding smult_map_poly sdiv_poly_def
by (subst map_poly_map_poly,simp,rule map_poly_idI, insert assms, auto)
lemma coeff_sdiv_poly: "coeff (sdiv_poly f a) n = coeff f n div a"
unfolding sdiv_poly_def by (rule coeff_map_poly, auto)
lemma poly_pinfty_ge:
fixes p :: "real poly"
assumes "lead_coeff p > 0" "degree p ≠ 0"
shows "∃n. ∀ x ≥ n. poly p x ≥ b"
proof -
let ?p = "p - [:b - lead_coeff p :]"
have id: "lead_coeff ?p = lead_coeff p" using assms(2)
by (cases p, auto)
with assms(1) have "lead_coeff ?p > 0" by auto
from poly_pinfty_gt_lc[OF this, unfolded id] obtain n
where "⋀ x. x ≥ n ⟹ 0 ≤ poly p x - b" by auto
thus ?thesis by auto
qed
lemma pderiv_sum: "pderiv (sum f I) = sum (λ i. (pderiv (f i))) I"
by (induct I rule: infinite_finite_induct, auto simp: pderiv_add)
lemma smult_sum2: "smult m (∑i ∈ S. f i) = (∑i ∈ S. smult m (f i))"
by (induct S rule: infinite_finite_induct, auto simp add: smult_add_right)
lemma degree_mult_not_eq:
"degree (f * g) ≠ degree f + degree g ⟹ lead_coeff f * lead_coeff g = 0"
by (rule ccontr, auto simp: coeff_mult_degree_sum degree_mult_le le_antisym le_degree)
lemma irreducible⇩d_multD:
fixes a b :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
assumes l: "irreducible⇩d (a*b)"
shows "degree a = 0 ∧ a ≠ 0 ∧ irreducible⇩d b ∨ degree b = 0 ∧ b ≠ 0 ∧ irreducible⇩d a"
proof-
from l have a0: "a ≠ 0" and b0: "b ≠ 0" by auto
note [simp] = degree_mult_eq[OF this]
from l have "degree a = 0 ∨ degree b = 0" apply (unfold irreducible⇩d_def) by force
then show ?thesis
proof(elim disjE)
assume a: "degree a = 0"
with l a0 have "irreducible⇩d b"
by (simp add: irreducible⇩d_def)
(metis degree_mult_eq degree_mult_eq_0 mult.left_commute plus_nat.add_0)
with a a0 show ?thesis by auto
next
assume b: "degree b = 0"
with l b0 have "irreducible⇩d a"
unfolding irreducible⇩d_def
by (smt (verit) add_cancel_left_right degree_mult_eq degree_mult_eq_0 neq0_conv semiring_normalization_rules(16))
with b b0 show ?thesis by auto
qed
qed
lemma irreducible_connect_field[simp]:
fixes f :: "'a :: field poly"
shows "irreducible⇩d f = irreducible f" (is "?l = ?r")
proof
show "?r ⟹ ?l"
by (metis irreducible_altdef is_unit_iff_degree reducible⇩dE reducible_polyI)
next
assume l: ?l
show ?r
by (metis irreducible⇩d_multD is_unit_iff_degree l mult_zero_right not_irreducibleE not_less0 reducible⇩dI)
qed
lemma is_unit_field_poly[simp]:
fixes p :: "'a::field poly"
shows "is_unit p ⟷ p ≠ 0 ∧ degree p = 0"
by (metis is_unit_iff_degree not_is_unit_0)
lemma irreducible_smult_field[simp]:
fixes c :: "'a :: field"
shows "irreducible (smult c p) ⟷ c ≠ 0 ∧ irreducible p" (is "?L ⟷ ?R")
proof (intro iffI conjI irreducible⇩d_smult_not_zero_divisor_left[of c p, simplified])
assume "irreducible (smult c p)"
then show "c ≠ 0" by auto
next
assume ?R
then have c0: "c ≠ 0" and irr: "irreducible p" by auto
show ?L
proof (fold irreducible_connect_field, intro irreducible⇩dI, unfold degree_smult_eq if_not_P[OF c0])
show "degree p > 0" using irr by auto
fix q r
from c0 have "p = smult (1/c) (smult c p)" by simp
also assume "smult c p = q * r"
finally have [simp]: "p = smult (1/c) …".
assume main: "degree q < degree p" "degree r < degree p"
have "¬irreducible⇩d p" by (rule reducible⇩dI, rule exI[of _ "smult (1/c) q"], rule exI[of _ r], insert irr c0 main, simp)
with irr show False by auto
qed
qed auto
lemma irreducible_monic_factor: fixes p :: "'a :: field poly"
assumes "degree p > 0"
shows "∃ q r. irreducible q ∧ p = q * r ∧ monic q"
proof -
from irreducible⇩d_factorization_exists[OF assms]
obtain fs where "fs ≠ []" and "set fs ⊆ Collect irreducible" and "p = prod_list fs" by auto
then have q: "irreducible (hd fs)" and p: "p = hd fs * prod_list (tl fs)" by (atomize(full), cases fs, auto)
define c where "c = coeff (hd fs) (degree (hd fs))"
from q have c: "c ≠ 0" unfolding c_def irreducible⇩d_def by auto
show ?thesis
by (rule exI[of _ "smult (1/c) (hd fs)"], rule exI[of _ "smult c (prod_list (tl fs))"], unfold p,
insert q c, auto simp: c_def)
qed
lemma monic_irreducible_factorization: fixes p :: "'a :: field poly"
shows "monic p ⟹
∃ as f. finite as ∧ p = prod (λ a. a ^ Suc (f a)) as ∧ as ⊆ {q. irreducible q ∧ monic q}"
proof (induct "degree p" arbitrary: p rule: less_induct)
case (less p)
show ?case
proof (cases "degree p > 0")
case False
with less(2) have "p = 1" by (simp add: coeff_eq_0 poly_eq_iff)
thus ?thesis by (intro exI[of _ "{}"], auto)
next
case True
from irreducible⇩d_factor[OF this] obtain q r where p: "p = q * r"
and q: "irreducible q" and deg: "degree r < degree p" by auto
hence q0: "q ≠ 0" by auto
define c where "c = coeff q (degree q)"
let ?q = "smult (1/c) q"
let ?r = "smult c r"
from q0 have c: "c ≠ 0" "1 / c ≠ 0" unfolding c_def by auto
hence p: "p = ?q * ?r" unfolding p by auto
have deg: "degree ?r < degree p" using c deg by auto
let ?Q = "{q. irreducible q ∧ monic (q :: 'a poly)}"
have mon: "monic ?q" unfolding c_def using q0 by auto
from monic_factor[OF ‹monic p›[unfolded p] this] have "monic ?r" .
from less(1)[OF deg this] obtain f as
where as: "finite as" "?r = (∏ a ∈as. a ^ Suc (f a))"
"as ⊆ ?Q" by blast
from q c have irred: "irreducible ?q" by simp
show ?thesis
proof (cases "?q ∈ as")
case False
let ?as = "insert ?q as"
let ?f = "λ a. if a = ?q then 0 else f a"
have "p = ?q * (∏ a ∈as. a ^ Suc (f a))" unfolding p as by simp
also have "(∏ a ∈as. a ^ Suc (f a)) = (∏ a ∈as. a ^ Suc (?f a))"
by (rule prod.cong, insert False, auto)
also have "?q * … = (∏ a ∈ ?as. a ^ Suc (?f a))"
by (subst prod.insert, insert as False, auto)
finally have p: "p = (∏ a ∈ ?as. a ^ Suc (?f a))" .
from as(1) have fin: "finite ?as" by auto
from as mon irred have Q: "?as ⊆ ?Q" by auto
from fin p Q show ?thesis
by(intro exI[of _ ?as] exI[of _ ?f], auto)
next
case True
let ?f = "λ a. if a = ?q then Suc (f a) else f a"
have "p = ?q * (∏ a ∈as. a ^ Suc (f a))" unfolding p as by simp
also have "(∏ a ∈as. a ^ Suc (f a)) = ?q ^ Suc (f ?q) * (∏ a ∈(as - {?q}). a ^ Suc (f a))"
by (subst prod.remove[OF _ True], insert as, auto)
also have "(∏ a ∈(as - {?q}). a ^ Suc (f a)) = (∏ a ∈(as - {?q}). a ^ Suc (?f a))"
by (rule prod.cong, auto)
also have "?q * (?q ^ Suc (f ?q) * … ) = ?q ^ Suc (?f ?q) * …"
by (simp add: ac_simps)
also have "… = (∏ a ∈ as. a ^ Suc (?f a))"
by (subst prod.remove[OF _ True], insert as, auto)
finally have "p = (∏ a ∈ as. a ^ Suc (?f a))" .
with as show ?thesis
by (intro exI[of _ as] exI[of _ ?f], auto)
qed
qed
qed
lemma monic_irreducible_gcd:
"monic (f::'a::{field,euclidean_ring_gcd,semiring_gcd_mult_normalize,
normalization_euclidean_semiring_multiplicative} poly) ⟹
irreducible f ⟹ gcd f u ∈ {1,f}"
by (metis gcd_dvd1 irreducible_altdef insertCI is_unit_gcd_iff poly_dvd_antisym poly_gcd_monic)
end