# [isabelle-dev] Polynomial theory

Brian Huffman brianh at cs.pdx.edu
Sun Jan 11 00:53:26 CET 2009

```Hi all,

Recently I was inspired by Mark Janney's comments on the Isabelle
users list to finish up the polynomial theory that started working on
a while ago. Basically, it is a heavily-reworked version of Clemens
Ballarin's theories from HOL/Abstract/poly in the distribution. It
includes most of the same operations: coefficients, monomials, degree,
scalar multiplication, and all the ring operations. It also includes
definitions for div and mod, and is fully integrated with the HOL
algebraic type class hierarchy.

If there are no objections, I would like to add this theory to the
main Isabelle/HOL source directory. Since the main HOL image already
includes a list-based formalization of polynomials (Univ_Poly.thy), I
think that a formalization using a real type constructor would be an
improvement; it probably wouldn't be too hard to adapt the other
theories to use the new polynomial type instead.

The source file is attached (it will probably only work with the
development snapshot).

- Brian

-------------- next part --------------
header {* Univariate Polynomials *}

theory Polynomial
imports Plain SetInterval
begin

subsection {* Definition of type @{text poly} *}

typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
morphisms coeff Abs_poly
by auto

lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
by (simp add: coeff_inject [symmetric] expand_fun_eq)

lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
by (simp add: expand_poly_eq)

subsection {* Degree of a polynomial *}

definition
degree :: "'a::zero poly \<Rightarrow> nat" where
"degree p = (LEAST n. \<forall>i>n. coeff p i = 0)"

lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0"
proof -
have "coeff p \<in> Poly"
by (rule coeff)
hence "\<exists>n. \<forall>i>n. coeff p i = 0"
unfolding Poly_def by simp
hence "\<forall>i>degree p. coeff p i = 0"
unfolding degree_def by (rule LeastI_ex)
moreover assume "degree p < n"
ultimately show ?thesis by simp
qed

lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p"
by (erule contrapos_np, rule coeff_eq_0, simp)

lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n"
unfolding degree_def by (erule Least_le)

lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0"
unfolding degree_def by (drule not_less_Least, simp)

subsection {* The zero polynomial *}

instantiation poly :: (zero) zero
begin

definition
zero_poly_def: "0 = Abs_poly (\<lambda>n. 0)"

instance ..
end

lemma coeff_0 [simp]: "coeff 0 n = 0"
unfolding zero_poly_def
by (simp add: Abs_poly_inverse Poly_def)

lemma degree_0 [simp]: "degree 0 = 0"
by (rule order_antisym [OF degree_le le0]) simp

assumes "p \<noteq> 0" shows "coeff p (degree p) \<noteq> 0"
proof (cases "degree p")
case 0
from `p \<noteq> 0` have "\<exists>n. coeff p n \<noteq> 0"
by (simp add: expand_poly_eq)
then obtain n where "coeff p n \<noteq> 0" ..
hence "n \<le> degree p" by (rule le_degree)
with `coeff p n \<noteq> 0` and `degree p = 0`
show "coeff p (degree p) \<noteq> 0" by simp
next
case (Suc n)
from `degree p = Suc n` have "n < degree p" by simp
hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp)
then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast
from `degree p = Suc n` and `n < i` have "degree p \<le> i" by simp
also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree)
finally have "degree p = i" .
with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp
qed

lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0"
by (cases "p = 0", simp, simp add: leading_coeff_neq_0)

subsection {* List-style constructor for polynomials *}

definition
pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
where
[code del]: "pCons a p = Abs_poly (nat_case a (coeff p))"

lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly"
unfolding Poly_def by (auto split: nat.split)

lemma coeff_pCons:
"coeff (pCons a p) = nat_case a (coeff p)"
unfolding pCons_def
by (simp add: Abs_poly_inverse Poly_nat_case coeff)

lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
by (simp add: coeff_pCons)

lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
by (simp add: coeff_pCons)

lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)"
by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split)

lemma degree_pCons_eq:
"p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)"
apply (rule order_antisym [OF degree_pCons_le])
apply (rule le_degree, simp)
done

lemma degree_pCons_0: "degree (pCons a 0) = 0"
apply (rule order_antisym [OF _ le0])
apply (rule degree_le, simp add: coeff_pCons split: nat.split)
done

lemma degree_pCons_eq_if:
"degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
apply (cases "p = 0", simp_all)
apply (rule order_antisym [OF _ le0])
apply (rule degree_le, simp add: coeff_pCons split: nat.split)
apply (rule order_antisym [OF degree_pCons_le])
apply (rule le_degree, simp)
done

lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma pCons_eq_iff [simp]:
"pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q"
proof (safe)
assume "pCons a p = pCons b q"
then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp
then show "a = b" by simp
next
assume "pCons a p = pCons b q"
then have "\<forall>n. coeff (pCons a p) (Suc n) =
coeff (pCons b q) (Suc n)" by simp
then show "p = q" by (simp add: expand_poly_eq)
qed

lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0"
using pCons_eq_iff [of a p 0 0] by simp

lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly"
unfolding Poly_def
by (clarify, rule_tac x=n in exI, simp)

lemma pCons_cases [cases type: poly]:
obtains (pCons) a q where "p = pCons a q"
proof
show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))"
by (rule poly_ext)
(simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons
split: nat.split)
qed

lemma pCons_induct [case_names 0 pCons, induct type: poly]:
assumes zero: "P 0"
assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)"
shows "P p"
proof (induct p rule: measure_induct_rule [where f=degree])
case (less p)
obtain a q where "p = pCons a q" by (rule pCons_cases)
have "P q"
proof (cases "q = 0")
case True
then show "P q" by (simp add: zero)
next
case False
then have "degree (pCons a q) = Suc (degree q)"
by (rule degree_pCons_eq)
then have "degree q < degree p"
using `p = pCons a q` by simp
then show "P q"
by (rule less.hyps)
qed
then have "P (pCons a q)"
by (rule pCons)
then show ?case
using `p = pCons a q` by simp
qed

subsection {* Monomials *}

definition
monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where
"monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)"

lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)"
unfolding monom_def
by (subst Abs_poly_inverse, auto simp add: Poly_def)

lemma monom_0: "monom a 0 = pCons a 0"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma monom_eq_0 [simp]: "monom 0 n = 0"
by (rule poly_ext) simp

lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0"
by (simp add: expand_poly_eq)

lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b"
by (simp add: expand_poly_eq)

lemma degree_monom_le: "degree (monom a n) \<le> n"
by (rule degree_le, simp)

lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n"
apply (rule order_antisym [OF degree_monom_le])
apply (rule le_degree, simp)
done

subsection {* Addition and subtraction *}

begin

definition
plus_poly_def [code del]:
"p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)"

fixes f g :: "nat \<Rightarrow> 'a"
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly"
unfolding Poly_def
apply (clarify, rename_tac m n)
apply (rule_tac x="max m n" in exI, simp)
done

"coeff (p + q) n = coeff p n + coeff q n"
unfolding plus_poly_def

instance proof
fix p q r :: "'a poly"
show "(p + q) + r = p + (q + r)"
show "p + q = q + p"
show "0 + p = p"
by (simp add: expand_poly_eq)
qed

end

begin

definition
uminus_poly_def [code del]:
"- p = Abs_poly (\<lambda>n. - coeff p n)"

definition
minus_poly_def [code del]:
"p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)"

lemma Poly_minus:
fixes f :: "nat \<Rightarrow> 'a"
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly"
unfolding Poly_def by simp

lemma Poly_diff:
fixes f g :: "nat \<Rightarrow> 'a"
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly"
unfolding diff_minus by (simp add: Poly_add Poly_minus)

lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
unfolding uminus_poly_def
by (simp add: Abs_poly_inverse coeff Poly_minus)

lemma coeff_diff [simp]:
"coeff (p - q) n = coeff p n - coeff q n"
unfolding minus_poly_def
by (simp add: Abs_poly_inverse coeff Poly_diff)

instance proof
fix p q :: "'a poly"
show "- p + p = 0"
by (simp add: expand_poly_eq)
show "p - q = p + - q"
by (simp add: expand_poly_eq diff_minus)
qed

end

"pCons a p + pCons b q = pCons (a + b) (p + q)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma minus_pCons [simp]:
"- pCons a p = pCons (- a) (- p)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma diff_pCons [simp]:
"pCons a p - pCons b q = pCons (a - b) (p - q)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma degree_add_le: "degree (p + q) \<le> max (degree p) (degree q)"
by (rule degree_le, auto simp add: coeff_eq_0)

"degree p < degree q \<Longrightarrow> degree (p + q) = degree q"
apply (cases "q = 0", simp)
apply (rule order_antisym)
apply (rule ord_le_eq_trans [OF degree_add_le])
apply simp
apply (rule le_degree)
apply (simp add: coeff_eq_0)
done

"degree q < degree p \<Longrightarrow> degree (p + q) = degree p"
using degree_add_eq_right [of q p]

lemma degree_minus [simp]: "degree (- p) = degree p"
unfolding degree_def by simp

lemma degree_diff_le: "degree (p - q) \<le> max (degree p) (degree q)"
using degree_add_le [where p=p and q="-q"]
by (simp add: diff_minus)

lemma add_monom: "monom a n + monom b n = monom (a + b) n"
by (rule poly_ext) simp

lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
by (rule poly_ext) simp

lemma minus_monom: "- monom a n = monom (-a) n"
by (rule poly_ext) simp

lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)"
by (cases "finite A", induct set: finite, simp_all)

lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)"
by (rule poly_ext) (simp add: coeff_setsum)

subsection {* Multiplication by a constant *}

definition
smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
"smult a p = Abs_poly (\<lambda>n. a * coeff p n)"

lemma Poly_smult:
fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0"
shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly"
unfolding Poly_def
by (clarify, rule_tac x=n in exI, simp)

lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
unfolding smult_def
by (simp add: Abs_poly_inverse Poly_smult coeff)

lemma degree_smult_le: "degree (smult a p) \<le> degree p"
by (rule degree_le, simp add: coeff_eq_0)

lemma smult_smult: "smult a (smult b p) = smult (a * b) p"
by (rule poly_ext, simp add: mult_assoc)

lemma smult_0_right [simp]: "smult a 0 = 0"
by (rule poly_ext, simp)

lemma smult_0_left [simp]: "smult 0 p = 0"
by (rule poly_ext, simp)

lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
by (rule poly_ext, simp)

"smult a (p + q) = smult a p + smult a q"
by (rule poly_ext, simp add: ring_simps)

"smult (a + b) p = smult a p + smult b p"
by (rule poly_ext, simp add: ring_simps)

lemma smult_minus_right:
"smult (a::'a::comm_ring) (- p) = - smult a p"
by (rule poly_ext, simp)

lemma smult_minus_left:
"smult (- a::'a::comm_ring) p = - smult a p"
by (rule poly_ext, simp)

lemma smult_diff_right:
"smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
by (rule poly_ext, simp add: ring_simps)

lemma smult_diff_left:
"smult (a - b::'a::comm_ring) p = smult a p - smult b p"
by (rule poly_ext, simp add: ring_simps)

lemma smult_pCons [simp]:
"smult a (pCons b p) = pCons (a * b) (smult a p)"
by (rule poly_ext, simp add: coeff_pCons split: nat.split)

lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
by (induct n, simp add: monom_0, simp add: monom_Suc)

subsection {* Multiplication of polynomials *}

lemma Poly_mult_lemma:
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0" and m n :: nat
assumes "\<forall>i>m. f i = 0"
assumes "\<forall>j>n. g j = 0"
shows "\<forall>k>m+n. (\<Sum>i\<le>k. f i * g (k-i)) = 0"
proof (clarify)
fix k :: nat
assume "m + n < k"
show "(\<Sum>i\<le>k. f i * g (k - i)) = 0"
proof (rule setsum_0' [rule_format])
fix i :: nat
assume "i \<in> {..k}" hence "i \<le> k" by simp
with `m + n < k` have "m < i \<or> n < k - i" by arith
thus "f i * g (k - i) = 0"
using prems by auto
qed
qed

lemma Poly_mult:
fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0"
shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i * g (n-i)) \<in> Poly"
unfolding Poly_def
by (safe, rule exI, rule Poly_mult_lemma)

lemma poly_mult_assoc_lemma:
fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>j\<le>k. \<Sum>i\<le>j. f i (j - i) (n - j)) =
(\<Sum>j\<le>k. \<Sum>i\<le>k - j. f j i (n - j - i))"
proof (induct k)
case 0 show ?case by simp
next
case (Suc k) thus ?case
cong: strong_setsum_cong)
qed

lemma poly_mult_commute_lemma:
fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>i\<le>n. f i (n - i)) = (\<Sum>i\<le>n. f (n - i) i)"
proof (rule setsum_reindex_cong)
show "inj_on (\<lambda>i. n - i) {..n}"
by (rule inj_onI) simp
show "{..n} = (\<lambda>i. n - i) ` {..n}"
by (auto, rule_tac x="n - x" in image_eqI, simp_all)
next
fix i assume "i \<in> {..n}"
hence "n - (n - i) = i" by simp
thus "f (n - i) i = f (n - i) (n - (n - i))" by simp
qed

text {* TODO: move to appropriate theory *}
lemma setsum_atMost_Suc_shift:
fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n) note IH = this
have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
by (rule setsum_atMost_Suc)
also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
by (rule IH)
also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
by (rule setsum_atMost_Suc [symmetric])
finally show ?case .
qed

instantiation poly :: (comm_semiring_0) comm_semiring_0
begin

definition
times_poly_def:
"p * q = Abs_poly (\<lambda>n. \<Sum>i\<le>n. coeff p i * coeff q (n-i))"

lemma coeff_mult:
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
unfolding times_poly_def
by (simp add: Abs_poly_inverse coeff Poly_mult)

instance proof
fix p q r :: "'a poly"
show 0: "0 * p = 0"
by (simp add: expand_poly_eq coeff_mult)
show "p * 0 = 0"
by (simp add: expand_poly_eq coeff_mult)
show "(p + q) * r = p * r + q * r"
by (simp add: expand_poly_eq coeff_mult left_distrib setsum_addf)
show "(p * q) * r = p * (q * r)"
proof (rule poly_ext)
fix n :: nat
have "(\<Sum>j\<le>n. \<Sum>i\<le>j. coeff p i * coeff q (j - i) * coeff r (n - j)) =
(\<Sum>j\<le>n. \<Sum>i\<le>n - j. coeff p j * coeff q i * coeff r (n - j - i))"
by (rule poly_mult_assoc_lemma)
thus "coeff ((p * q) * r) n = coeff (p * (q * r)) n"
by (simp add: coeff_mult setsum_right_distrib
setsum_left_distrib mult_assoc)
qed
show "p * q = q * p"
proof (rule poly_ext)
fix n :: nat
have "(\<Sum>i\<le>n. coeff p i * coeff q (n - i)) =
(\<Sum>i\<le>n. coeff p (n - i) * coeff q i)"
by (rule poly_mult_commute_lemma)
thus "coeff (p * q) n = coeff (q * p) n"
by (simp add: coeff_mult mult_commute)
qed
qed

end

lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
apply (rule degree_le, simp add: coeff_mult)
apply (rule Poly_mult_lemma)
apply (simp_all add: coeff_eq_0)
done

lemma mult_pCons_left [simp]:
"pCons a p * q = smult a q + pCons 0 (p * q)"
apply (rule poly_ext)
apply (case_tac n)
apply (simp add: coeff_mult)
apply (simp add: coeff_mult setsum_atMost_Suc_shift
del: setsum_atMost_Suc)
done

lemma mult_pCons_right [simp]:
"p * pCons a q = smult a p + pCons 0 (p * q)"
using mult_pCons_left [of a q p] by (simp add: mult_commute)

lemma mult_smult_left: "smult a p * q = smult a (p * q)"
by (induct p, simp, simp add: smult_add_right smult_smult)

lemma mult_smult_right: "p * smult a q = smult a (p * q)"
using mult_smult_left [of a q p] by (simp add: mult_commute)

lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)

subsection {* The unit polynomial and exponentiation *}

instantiation poly :: (comm_semiring_1) comm_semiring_1
begin

definition
one_poly_def:
"1 = pCons 1 0"

instance proof
fix p :: "'a poly" show "1 * p = p"
unfolding one_poly_def
by simp
next
show "0 \<noteq> (1::'a poly)"
unfolding one_poly_def by simp
qed

end

lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
unfolding one_poly_def
by (simp add: coeff_pCons split: nat.split)

lemma degree_1 [simp]: "degree 1 = 0"
unfolding one_poly_def
by (rule degree_pCons_0)

instantiation poly :: (comm_semiring_1) recpower
begin

primrec power_poly where
power_poly_0: "(p::'a poly) ^ 0 = 1"
| power_poly_Suc: "(p::'a poly) ^ (Suc n) = p * p ^ n"

instance
by default simp_all

end

instance poly :: (comm_ring) comm_ring ..

instance poly :: (comm_ring_1) comm_ring_1 ..

instantiation poly :: (comm_ring_1) number_ring
begin

definition
"number_of k = (of_int k :: 'a poly)"

instance
by default (rule number_of_poly_def)

end

subsection {* Polynomials form an integral domain *}

lemma coeff_mult_degree_sum:
"coeff (p * q) (degree p + degree q) =
coeff p (degree p) * coeff q (degree q)"
apply (simp add: coeff_mult)
apply (subst setsum_diff1' [where a="degree p"])
apply simp
apply simp
apply (subst setsum_0' [rule_format])
apply clarsimp
apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q - a")
apply (force simp add: coeff_eq_0)
apply arith
apply simp
done

instance poly :: (idom) idom
proof
fix p q :: "'a poly"
assume "p \<noteq> 0" and "q \<noteq> 0"
have "coeff (p * q) (degree p + degree q) =
coeff p (degree p) * coeff q (degree q)"
by (rule coeff_mult_degree_sum)
also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
using `p \<noteq> 0` and `q \<noteq> 0` by simp
finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
thus "p * q \<noteq> 0" by (simp add: expand_poly_eq)
qed

lemma degree_mult_eq:
fixes p q :: "'a::idom poly"
shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
apply (rule order_antisym [OF degree_mult_le le_degree])
apply (simp add: coeff_mult_degree_sum)
done

lemma dvd_imp_degree_le:
fixes p q :: "'a::idom poly"
shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
by (erule dvdE, simp add: degree_mult_eq)

subsection {* Polynomials form a Euclidean domain *}

definition
divmod_poly_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool"
where
"divmod_poly_rel x y q r \<longleftrightarrow>
x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)"

lemma divmod_poly_rel_0:
"divmod_poly_rel 0 y 0 0"
unfolding divmod_poly_rel_def by simp

lemma divmod_poly_rel_by_0:
"divmod_poly_rel x 0 0 x"
unfolding divmod_poly_rel_def by simp

lemma eq_zero_or_degree_less:
assumes "degree p \<le> n" and "coeff p n = 0"
shows "p = 0 \<or> degree p < n"
proof (cases n)
case 0
with `degree p \<le> n` and `coeff p n = 0`
have "coeff p (degree p) = 0" by simp
then have "p = 0" by simp
then show ?thesis ..
next
case (Suc m)
have "\<forall>i>n. coeff p i = 0"
using `degree p \<le> n` by (simp add: coeff_eq_0)
then have "\<forall>i\<ge>n. coeff p i = 0"
using `coeff p n = 0` by (simp add: le_less)
then have "\<forall>i>m. coeff p i = 0"
using `n = Suc m` by (simp add: less_eq_Suc_le)
then have "degree p \<le> m"
by (rule degree_le)
then have "degree p < n"
using `n = Suc m` by (simp add: less_Suc_eq_le)
then show ?thesis ..
qed

lemma divmod_poly_rel_pCons:
assumes rel: "divmod_poly_rel x y q r"
assumes y: "y \<noteq> 0"
assumes b: "b = coeff (pCons a r) (degree y) / coeff y (degree y)"
shows "divmod_poly_rel (pCons a x) y (pCons b q) (pCons a r - smult b y)"
(is "divmod_poly_rel ?x y ?q ?r")
proof -
have x: "x = q * y + r" and r: "r = 0 \<or> degree r < degree y"
using assms unfolding divmod_poly_rel_def by simp_all

have 1: "?x = ?q * y + ?r"
using b x by simp

have 2: "?r = 0 \<or> degree ?r < degree y"
proof (rule eq_zero_or_degree_less)
have "degree ?r \<le> max (degree (pCons a r)) (degree (smult b y))"
by (rule degree_diff_le)
also have "\<dots> \<le> degree y"
proof (rule min_max.le_supI)
show "degree (pCons a r) \<le> degree y"
using r by (auto simp add: degree_pCons_eq_if)
show "degree (smult b y) \<le> degree y"
by (rule degree_smult_le)
qed
finally show "degree ?r \<le> degree y" .
next
show "coeff ?r (degree y) = 0"
using `y \<noteq> 0` unfolding b by simp
qed

from 1 2 show ?thesis
unfolding divmod_poly_rel_def
using `y \<noteq> 0` by simp
qed

lemma divmod_poly_rel_exists: "\<exists>q r. divmod_poly_rel x y q r"
apply (cases "y = 0")
apply (fast intro!: divmod_poly_rel_by_0)
apply (induct x)
apply (fast intro!: divmod_poly_rel_0)
apply (fast intro!: divmod_poly_rel_pCons)
done

lemma divmod_poly_rel_unique:
assumes 1: "divmod_poly_rel x y q1 r1"
assumes 2: "divmod_poly_rel x y q2 r2"
shows "q1 = q2 \<and> r1 = r2"
proof (cases "y = 0")
assume "y = 0" with assms show ?thesis
by (simp add: divmod_poly_rel_def)
next
assume [simp]: "y \<noteq> 0"
from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
unfolding divmod_poly_rel_def by simp_all
from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
unfolding divmod_poly_rel_def by simp_all
from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
by (simp add: ring_simps)
from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
by (auto intro: le_less_trans [OF degree_diff_le])

show "q1 = q2 \<and> r1 = r2"
proof (rule ccontr)
assume "\<not> (q1 = q2 \<and> r1 = r2)"
with q3 have "q1 \<noteq> q2" and "r1 \<noteq> r2" by auto
with r3 have "degree (r2 - r1) < degree y" by simp
also have "degree y \<le> degree (q1 - q2) + degree y" by simp
also have "\<dots> = degree ((q1 - q2) * y)"
using `q1 \<noteq> q2` by (simp add: degree_mult_eq)
also have "\<dots> = degree (r2 - r1)"
using q3 by simp
finally have "degree (r2 - r1) < degree (r2 - r1)" .
then show "False" by simp
qed
qed

lemmas divmod_poly_rel_unique_div =
divmod_poly_rel_unique [THEN conjunct1, standard]

lemmas divmod_poly_rel_unique_mod =
divmod_poly_rel_unique [THEN conjunct2, standard]

instantiation poly :: (field) ring_div
begin

definition div_poly where
[code del]: "x div y = (THE q. \<exists>r. divmod_poly_rel x y q r)"

definition mod_poly where
[code del]: "x mod y = (THE r. \<exists>q. divmod_poly_rel x y q r)"

lemma div_poly_eq:
"divmod_poly_rel x y q r \<Longrightarrow> x div y = q"
unfolding div_poly_def
by (fast elim: divmod_poly_rel_unique_div)

lemma mod_poly_eq:
"divmod_poly_rel x y q r \<Longrightarrow> x mod y = r"
unfolding mod_poly_def
by (fast elim: divmod_poly_rel_unique_mod)

lemma divmod_poly_rel:
"divmod_poly_rel x y (x div y) (x mod y)"
proof -
from divmod_poly_rel_exists
obtain q r where "divmod_poly_rel x y q r" by fast
thus ?thesis
by (simp add: div_poly_eq mod_poly_eq)
qed

instance proof
fix x y :: "'a poly"
show "x div y * y + x mod y = x"
using divmod_poly_rel [of x y]
by (simp add: divmod_poly_rel_def)
next
fix x :: "'a poly"
have "divmod_poly_rel x 0 0 x"
by (rule divmod_poly_rel_by_0)
thus "x div 0 = 0"
by (rule div_poly_eq)
next
fix y :: "'a poly"
have "divmod_poly_rel 0 y 0 0"
by (rule divmod_poly_rel_0)
thus "0 div y = 0"
by (rule div_poly_eq)
next
fix x y z :: "'a poly"
assume "y \<noteq> 0"
hence "divmod_poly_rel (x + z * y) y (z + x div y) (x mod y)"
using divmod_poly_rel [of x y]
by (simp add: divmod_poly_rel_def left_distrib)
thus "(x + z * y) div y = z + x div y"
by (rule div_poly_eq)
qed

end

lemma degree_mod_less:
"y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
using divmod_poly_rel [of x y]
unfolding divmod_poly_rel_def by simp

lemma div_poly_less: "degree x < degree y \<Longrightarrow> x div y = 0"
proof -
assume "degree x < degree y"
hence "divmod_poly_rel x y 0 x"
by (simp add: divmod_poly_rel_def)
thus "x div y = 0" by (rule div_poly_eq)
qed

lemma mod_poly_less: "degree x < degree y \<Longrightarrow> x mod y = x"
proof -
assume "degree x < degree y"
hence "divmod_poly_rel x y 0 x"
by (simp add: divmod_poly_rel_def)
thus "x mod y = x" by (rule mod_poly_eq)
qed

lemma mod_pCons:
fixes a and x
assumes y: "y \<noteq> 0"
defines b: "b \<equiv> coeff (pCons a (x mod y)) (degree y) / coeff y (degree y)"
shows "(pCons a x) mod y = (pCons a (x mod y) - smult b y)"
unfolding b
apply (rule mod_poly_eq)
apply (rule divmod_poly_rel_pCons [OF divmod_poly_rel y refl])
done

subsection {* Evaluation of polynomials *}

definition
poly :: "'a::{comm_semiring_1,recpower} poly \<Rightarrow> 'a \<Rightarrow> 'a" where
"poly p = (\<lambda>x. \<Sum>n\<le>degree p. coeff p n * x ^ n)"

lemma poly_0 [simp]: "poly 0 x = 0"
unfolding poly_def by simp

lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
unfolding poly_def
by (simp add: degree_pCons_eq_if setsum_atMost_Suc_shift power_Suc
setsum_left_distrib setsum_right_distrib mult_ac
del: setsum_atMost_Suc)

lemma poly_1 [simp]: "poly 1 x = 1"
unfolding one_poly_def by simp

lemma poly_monom: "poly (monom a n) x = a * x ^ n"
by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)

lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
apply (induct p arbitrary: q, simp)
apply (case_tac q, simp, simp add: ring_simps)
done

lemma poly_minus [simp]:
fixes x :: "'a::{comm_ring_1,recpower}"
shows "poly (- p) x = - poly p x"
by (induct p, simp_all)

lemma poly_diff [simp]:
fixes x :: "'a::{comm_ring_1,recpower}"
shows "poly (p - q) x = poly p x - poly q x"
by (simp add: diff_minus)

lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
by (cases "finite A", induct set: finite, simp_all)

lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
by (induct p, simp, simp add: ring_simps)

lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
by (induct p, simp_all, simp add: ring_simps)

end
```