(* Author: René Thiemann Akihisa Yamada License: BSD *) 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