# Theory Polynomial_Factorization.Order_Polynomial

```(*
Author:      René Thiemann
*)
subsection ‹Order of Polynomial Roots›

text ‹We extend the collection of results on the order of roots of polynomials.
Moreover, we provide code-equations to compute the order for a given root and
polynomial.›

theory Order_Polynomial
imports
Polynomial_Interpolation.Missing_Polynomial
begin

lemma order_linear[simp]: "order a [:- a, 1:] = Suc 0" unfolding order_def
proof (rule Least_equality, intro notI)
assume "[:- a, 1:] ^ Suc (Suc 0) dvd [:- a, 1:]"
from dvd_imp_degree_le[OF this] show False by auto
next
fix n
assume *: "¬ [:- a, 1:] ^ Suc n dvd [:- a, 1:]"
thus "Suc 0 ≤ n"
by (cases n, auto)
qed

declare order_power_n_n[simp]

lemma linear_power_nonzero: "[: a, 1 :] ^ n ≠ 0"
proof
assume "[: a, 1 :]^n = 0"
with arg_cong[OF this, of degree, unfolded degree_linear_power]
show False by auto
qed

lemma order_linear_power': "order a ([: b, 1:]^Suc n) = (if b = -a then Suc n else 0)"
proof (cases "b = -a")
case True
thus ?thesis unfolding True order_power_n_n by simp
next
case False
let ?p = "[: b, 1:]^Suc n"
from linear_power_nonzero have "?p ≠ 0" .
have p: "?p = (∏a← replicate (Suc n) b. [:a, 1:])" by auto
{
assume "order a ?p ≠ 0"
then obtain m where ord: "order a ?p = Suc m" by (cases "order a ?p", auto)
from order[OF ‹?p ≠ 0›, of a, unfolded ord] have dvd: "[:- a, 1:] ^ Suc m dvd ?p" by auto
from poly_linear_exp_linear_factors[OF dvd[unfolded p]] False have False by auto
}
hence "order a ?p = 0" by auto
with False show ?thesis by simp
qed

lemma order_linear_power: "order a ([: b, 1:]^n) = (if b = -a then n else 0)"
proof (cases n)
case (Suc m)
show ?thesis unfolding Suc order_linear_power' by simp
qed simp

lemma order_linear': "order a [: b, 1:] = (if b = -a then 1 else 0)"
using order_linear_power'[of a b 0] by simp

lemma degree_div_less:
assumes p: "(p::'a::field poly) ≠ 0" and dvd: "r dvd p" and deg: "degree r ≠ 0"
shows "degree (p div r) < degree p"
proof -
from dvd obtain q where prq: "p = r * q" unfolding dvd_def by auto
have "degree p = degree r + degree q"
unfolding prq
by (rule degree_mult_eq, insert p prq, auto)
with deg have deg: "degree q < degree p" by auto
from prq have "q = p div r"
using deg p by auto
with deg show ?thesis by auto
qed

lemma order_sum_degree: assumes "p ≠ 0"
shows "sum (λ a. order a p) { a. poly p a = 0 } ≤ degree p"
proof -
define n where "n = degree p"
have "degree p ≤ n" unfolding n_def by auto
thus ?thesis using ‹p ≠ 0›
proof (induct n arbitrary: p)
case (0 p)
define a where "a = coeff p 0"
from 0 have "degree p = 0" by auto
hence p: "p = [: a :]" unfolding a_def
by (metis degree_0_id)
with 0 have "a ≠ 0" by auto
thus ?case unfolding p by auto
next
case (Suc m p)
note order = order[OF ‹p ≠ 0›]
show ?case
proof (cases "∃ a. poly p a = 0")
case True
then obtain a where root: "poly p a = 0" by auto
with order_root[of p a] Suc obtain n where orda: "order a p = Suc n"
by (cases "order a p", auto)
let ?a = "[: -a, 1 :] ^ Suc n"
from order_decomp[OF ‹p ≠ 0›, of a, unfolded orda]
obtain q where p: "p = ?a * q" and ndvd: "¬ [:- a, 1:] dvd q" by auto
from ‹p ≠ 0›[unfolded p] have nz: "?a ≠ 0" "q ≠ 0" by auto
hence deg: "degree p = degree ?a + degree q" unfolding p
by (subst degree_mult_eq, auto)
have ord: "⋀ a. order a p = order a ?a + order a q"
unfolding p
by (subst order_mult, insert nz, auto)
have roots: "{ a. poly p a = 0 } = insert a ({ a. poly q a = 0} - {a})" using root
unfolding p poly_mult by auto
have fin: "finite {a. poly q a = 0}" by (rule poly_roots_finite[OF ‹q ≠ 0›])
have "Suc n = order a p" using orda by simp
also have "… = Suc n + order a q" unfolding ord order_linear_power' by simp
finally have "order a q = 0" by auto
with order_root[of q a] ‹q ≠ 0› have qa: "poly q a ≠ 0" by auto
have "(∑a∈{a. poly q a = 0} - {a}. order a p) = (∑a∈{a. poly q a = 0} - {a}. order a q)"
proof (rule sum.cong[OF refl])
fix b
assume "b ∈ {a. poly q a = 0} - {a}"
hence "b ≠ a" by auto
hence "order b ?a = 0" unfolding order_linear_power' by simp
thus "order b p = order b q" unfolding ord by simp
qed
also have "… = (∑a∈{a. poly q a = 0}. order a q)" using qa by auto
also have "… ≤ degree q"
by (rule Suc(1)[OF _ ‹q ≠ 0›],
insert deg[unfolded degree_linear_power] Suc(2), auto)
finally have "(∑a∈{a. poly q a = 0} - {a}. order a p) ≤ degree q" .
thus ?thesis unfolding roots deg using fin
by (subst sum.insert, simp_all only: degree_linear_power, auto simp: orda)
qed auto
qed
qed

lemma order_code[code]: "order (a::'a::idom_divide) p =
(if p = 0 then Code.abort (STR ''order of polynomial 0 undefined'') (λ _. order a p)
else if poly p a ≠ 0 then 0 else Suc (order a (p div [: -a, 1 :])))"
proof (cases "p = 0")
case False note p = this
note order = order[OF p]
show ?thesis
proof (cases "poly p a = 0")
case True
with order_root[of p a] p obtain n where ord: "order a p = Suc n"
by (cases "order a p", auto)
from this(1) have "[: -a, 1 :] dvd p"
using True poly_eq_0_iff_dvd by blast
then obtain q where p: "p = [: -a, 1 :] * q" unfolding dvd_def by auto
have ord: "order a p = order a [: -a, 1 :] + order a q"
using p False order_mult[of "[: -a, 1 :]" q] by auto
have q: "p div [: -a, 1 :] = q" using False p
by (metis mult_zero_left nonzero_mult_div_cancel_left)
show ?thesis unfolding ord q using False True by auto
next
case False
with order_root[of p a] p show ?thesis by auto
qed
qed auto

end
```