lemma cCons_Cons_eq [simp]: "x ## y # ys = x # y # ys" by (simp add: cCons_def)
lemma cCons_append_Cons_eq [simp]: "x ## xs @ y # ys = x # xs @ y # ys" by (simp add: cCons_def)
lemma cCons_not_0_eq [simp]: "x ≠ 0 ==> x ## xs = x # xs" by (simp add: cCons_def)
lemma strip_while_not_0_Cons_eq [simp]: "strip_while (λx. x = 0) (x # xs) = x ## strip_while (λx. x = 0) xs" proof (cases "x = 0") case False thenshow ?thesis by simp next case True show ?thesis proof (induct xs rule: rev_induct) case Nil with True show ?caseby simp next case (snoc y ys) thenshow ?case by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons) qed qed
typedef (overloaded) 'a poly = "{f :: nat ==> 'a::zero. ∀🪙∞ n. f n = 0}" morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
setup_lifting type_definition_poly
lemma poly_eq_iff: "p = q ⟷ (∀n. coeff p n = coeff q n)" by (simp add: coeff_inject [symmetric] fun_eq_iff)
lemma poly_eqI: "(∧n. coeff p n = coeff q n) ==> p = q" by (simp add: poly_eq_iff)
lemma MOST_coeff_eq_0: "∀🪙∞ n. coeff p n = 0" using coeff [of p] by simp
lemma coeff_Abs_poly: assumes"∧i. i > n ==> f i = 0" shows"coeff (Abs_poly f) = f" proof (rule Abs_poly_inverse, clarify) have"eventually (λi. i > n) cofinite" by (auto simp: MOST_nat) thus"eventually (λi. f i = 0) cofinite" by eventually_elim (use assms in auto) qed
subsection‹Degree of a polynomial›
definition degree :: "'a::zero poly ==> nat" where"degree p = (LEAST n. ∀i>n. coeff p i = 0)"
lemma degree_cong: assumes"∧i. coeff p i = 0 ⟷ coeff q i = 0" shows"degree p = degree q" proof - have"(λn. ∀i>n. poly.coeff p i = 0) = (λn. ∀i>n. poly.coeff q i = 0)" using assms by (auto simp: fun_eq_iff) thus ?thesis by (simp only: degree_def) qed
lemma coeff_Abs_poly_If_le: "coeff (Abs_poly (λi. if i ≤ n then f i else 0)) = (λi. if i ≤ n then f i else 0)" proof (rule Abs_poly_inverse, clarify) have"eventually (λi. i > n) cofinite" by (auto simp: MOST_nat) thus"eventually (λi. (if i ≤ n then f i else 0) = 0) cofinite" by eventually_elim auto qed
lemma coeff_eq_0: assumes"degree p < n" shows"coeff p n = 0" proof - have"∃n. ∀i>n. coeff p i = 0" using MOST_coeff_eq_0 by (simp add: MOST_nat) thenhave"∀i>degree p. coeff p i = 0" unfolding degree_def by (rule LeastI_ex) with assms show ?thesis by simp qed
lemma le_degree: "coeff p n ≠ 0 ==> n ≤ degree p" using coeff_eq_0 linorder_le_less_linear by blast
lemma degree_le: "∀i>n. coeff p i = 0 ==> degree p ≤ n" unfolding degree_def by (erule Least_le)
lemma less_degree_imp: "n < degree p ==>∃i>n. coeff p i ≠ 0" unfolding degree_def by (drule not_less_Least, simp)
lemma poly_eqI2: assumes"degree p = degree q"and"∧i. i ≤ degree p ==> coeff p i = coeff q i" shows"p = q" by (metis assms le_degree poly_eqI)
lemma leading_coeff_neq_0: assumes"p ≠ 0" shows"coeff p (degree p) ≠ 0" proof (cases "degree p") case 0 from‹p ≠ 0›obtain n where"coeff p n ≠ 0" by (auto simp add: poly_eq_iff) thenhave"n ≤ degree p" by (rule le_degree) with‹coeff p n ≠ 0›and‹degree p = 0›show"coeff p (degree p) ≠ 0" by simp next case (Suc n) from‹degree p = Suc n›have"n < degree p" by simp thenhave"∃i>n. coeff p i ≠ 0" by (rule less_degree_imp) thenobtain i where"n < i"and"coeff p i ≠ 0" by blast from‹degree p = Suc n›and‹n 🚫›have"degree p ≤ i" by simp alsofrom‹coeff p i ≠ 0›have"i ≤ degree p" by (rule le_degree) finallyhave"degree p = i" . with‹coeff p i ≠ 0›show"coeff p (degree p) ≠ 0"by simp qed
lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 ⟷ p = 0" by (cases "p = 0") (simp_all add: leading_coeff_neq_0)
lemma degree_lessI: assumes"p ≠ 0 ∨ n > 0""∀k≥n. coeff p k = 0" shows"degree p < n" proof (cases "p = 0") case False show ?thesis proof (rule ccontr) assume *: "¬(degree p < n)"
define d where"d = degree p" from‹p ≠ 0›have"coeff p d ≠ 0" by (auto simp: d_def) moreoverhave"coeff p d = 0" using assms(2) * by (auto simp: not_less) ultimatelyshow False by contradiction qed qed (use assms in auto)
lemma eq_zero_or_degree_less: assumes"degree p ≤ n"and"coeff p n = 0" shows"p = 0 ∨ degree p < n" proof (cases n) case 0 with‹degree p ≤ n›and‹coeff p n = 0›have"coeff p (degree p) = 0" by simp thenhave"p = 0"by simp thenshow ?thesis .. next case (Suc m) from‹degree p ≤ n›have"∀i>n. coeff p i = 0" by (simp add: coeff_eq_0) with‹coeff p n = 0›have"∀i≥n. coeff p i = 0" by (simp add: le_less) with‹n = Suc m›have"∀i>m. coeff p i = 0" by (simp add: less_eq_Suc_le) thenhave"degree p ≤ m" by (rule degree_le) with‹n = Suc m›have"degree p < n" by (simp add: less_Suc_eq_le) thenshow ?thesis .. qed
lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 ==> degree rrr ≤ dr ==> degree rrr≤ dr - 1" using eq_zero_or_degree_less by fastforce
subsection‹List-style constructor for polynomials›
lift_definition pCons :: "'a::zero ==> 'a poly ==> 'a poly" is"λa p. case_nat a (coeff p)" by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)
lemmas coeff_pCons = pCons.rep_eq
lemma coeff_pCons': "poly.coeff (pCons c p) n = (if n = 0 then c else poly.coeff p (n - 1))" by transfer'(auto split: nat.splits)
lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a" by transfer simp
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) ≤ Suc (degree p)" by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)
lemma degree_pCons_eq: "p ≠ 0 ==> degree (pCons a p) = Suc (degree p)" by (simp add: degree_pCons_le le_antisym le_degree)
lemma degree_pCons_0: "degree (pCons a 0) = 0" proof - have"degree (pCons a 0) ≤ Suc 0" by (metis (no_types) degree_0 degree_pCons_le) thenshow ?thesis by (metis coeff_0 coeff_pCons_Suc degree_0 eq_zero_or_degree_less less_Suc0) qed
lemma degree_pCons_eq_if [simp]: "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" by (simp add: degree_pCons_0 degree_pCons_eq)
lemma pCons_eq_iff [simp]: "pCons a p = pCons b q ⟷ a = b ∧ p = q" proof safe assume"pCons a p = pCons b q" thenhave"coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp thenshow"a = b" by simp next assume"pCons a p = pCons b q" thenhave"coeff (pCons a p) (Suc n) = coeff (pCons b q) (Suc n)"for n by simp thenshow"p = q" by (simp add: poly_eq_iff) qed
lemma pCons_eq_0_iff [simp]: "pCons a p = 0 ⟷ a = 0 ∧ p = 0" using pCons_eq_iff [of a p 0 0] by 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 (λn. coeff p (Suc n)))" by transfer
(simp_all add: MOST_inj[where f=Suc and P="λn. p n = 0"for p] fun_eq_iff Abs_poly_inverse
split: nat.split) qed
lemma pCons_induct [case_names 0 pCons, induct type: poly]: assumes zero: "P 0" assumes pCons: "∧a p. a ≠ 0 ∨ p ≠ 0 ==> P p ==> 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 thenshow"P q"by (simp add: zero) next case False thenhave"degree (pCons a q) = Suc (degree q)" by (rule degree_pCons_eq) with‹p = pCons a q›have"degree q < degree p" by simp thenshow"P q" by (rule less.hyps) qed have"P (pCons a q)" proof (cases "a ≠ 0 ∨ q ≠ 0") case True with‹P q›show ?thesis by (auto intro: pCons) next case False with zero show ?thesis by simp qed with‹p = pCons a q›show ?case by simp qed
lemma degree_eq_zeroE: fixes p :: "'a::zero poly" assumes"degree p = 0" obtains a where"p = pCons a 0" proof - obtain a q where p: "p = pCons a q" by (cases p) with assms have"q = 0" by (cases "q = 0") simp_all with p have"p = pCons a 0" by simp thenshow thesis .. qed
syntax "_poly" :: "args ==> 'a poly" (‹(‹indent=2 notation=‹mixfix polynomial enumeration›\›[:_:])›)
syntax_consts "_poly"⇌ pCons translations "[:x, xs:]"⇌"CONST pCons x [:xs:]" "[:x:]"⇌"CONST pCons x 0"
lemma degree_0_id: assumes"degree p = 0" shows"[: coeff p 0 :] = p" by (metis assms coeff_pCons_0 degree_eq_zeroE)
lemma degree0_coeffs: "degree p = 0 ==>∃ a. p = [: a :]" by (meson degree_eq_zeroE)
lemma degree1_coeffs: fixes p :: "'a::zero poly" assumes"degree p = 1" obtains a b where"p = [: b, a :]""a ≠ 0" proof - obtain b a q where"p = pCons b q""q = pCons a 0" by (metis assms degree0_coeffs degree_0 degree_pCons_eq_if lessI less_one pCons_cases) thenshow thesis using assms that by force qed
lemma degree2_coeffs: fixes p :: "'a::zero poly" assumes"degree p = 2" obtains a b c where"p = [: c, b, a :]""a ≠ 0" proof - obtain c q where"p = pCons c q""degree q = 1" by (metis One_nat_def assms degree_0 degree_pCons_eq_if fact_0 fact_2 nat.inject numeral_2_eq_2 pCons_cases) thenshow thesis by (metis degree1_coeffs that) qed
subsection‹Representation of polynomials by lists of coefficients›
primrec Poly :: "'a::zero list ==> 'a poly" where
[code_post]: "Poly [] = 0"
| [code_post]: "Poly (a # as) = pCons a (Poly as)"
lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0" by (induct n) simp_all
lemma Poly_eq_0: "Poly as = 0 ⟷ (∃n. as = replicate n 0)" by (induct as) (auto simp add: Cons_replicate_eq)
lemma Poly_append_replicate_zero [simp]: "Poly (as @ replicate n 0) = Poly as" by (induct as) simp_all
lemma Poly_snoc_zero [simp]: "Poly (as @ [0]) = Poly as" using Poly_append_replicate_zero [of as 1] by simp
lemma Poly_cCons_eq_pCons_Poly [simp]: "Poly (a ## p) = pCons a (Poly p)" by (simp add: cCons_def)
lemma Poly_on_rev_starting_with_0 [simp]: "hd as = 0 ==> Poly (rev (tl as)) = Poly (rev as)" by (cases as) simp_all
definition coeffs :: "'a poly ==> 'a::zero list" where"coeffs p = (if p = 0 then [] else map (λi. coeff p i) [0 ..< Suc (degree p)])"
lemma coeffs_eq_Nil [simp]: "coeffs p = [] ⟷ p = 0" by (simp add: coeffs_def)
lemma not_0_coeffs_not_Nil: "p ≠ 0 ==> coeffs p ≠ []" by simp
lemma coeffs_0_eq_Nil [simp]: "coeffs 0 = []" by simp
lemma coeffs_pCons_eq_cCons [simp]: "coeffs (pCons a p) = a ## coeffs p" proof - have *: "∀m∈set ms. m > 0 ==> map (case_nat x f) ms = map f (map (λn. n - 1) ms)" for ms :: "nat list"and f :: "nat ==> 'a"and x :: "'a" by (induct ms) (auto split: nat.split) show ?thesis by (simp add: * coeffs_def upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc) qed
lemma length_coeffs: "p ≠ 0 ==> length (coeffs p) = degree p + 1" by (simp add: coeffs_def)
lemma coeffs_nth: "p ≠ 0 ==> n ≤ degree p ==> coeffs p ! n = coeff p n" by (auto simp: coeffs_def simp del: upt_Suc)
lemma coeff_in_coeffs: "p ≠ 0 ==> n ≤ degree p ==> coeff p n ∈ set (coeffs p)" using coeffs_nth [of p n, symmetric] by (simp add: length_coeffs)
lemma not_0_cCons_eq [simp]: "p ≠ 0 ==> a ## coeffs p = a # coeffs p" by (simp add: cCons_def)
lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p" by (induct p) auto
lemma coeffs_Poly [simp]: "coeffs (Poly as) = strip_while (HOL.eq 0) as" proof (induct as) case Nil thenshow ?caseby simp next case (Cons a as) from replicate_length_same [of as 0] have"(∀n. as ≠ replicate n 0) ⟷ (∃a∈set as. a ≠0)" by (auto dest: sym [of _ as]) with Cons show ?caseby auto qed
lemma no_trailing_coeffs [simp]: "no_trailing (HOL.eq 0) (coeffs p)" by (induct p) auto
lemma [code]: "coeff p = nth_default 0 (coeffs p)" by (simp add: nth_default_coeffs_eq)
lemma coeffs_eqI: assumes coeff: "∧n. coeff p n = nth_default 0 xs n" assumes zero: "no_trailing (HOL.eq 0) xs" shows"coeffs p = xs" proof - from coeff have"p = Poly xs" by (simp add: poly_eq_iff) with zero show ?thesis by simp qed
lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1" by (simp add: coeffs_def)
lemma forall_coeffs_conv: "(∀n. P (coeff p n)) ⟷ (∀c ∈ set (coeffs p). P c)"if"P 0" using that by (auto simp add: coeffs_def)
(metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)
instantiation poly :: ("{zero, equal}") equal begin
definition fold_coeffs :: "('a::zero ==> 'b ==> 'b) ==> 'a poly ==> 'b ==> 'b" where"fold_coeffs f p = foldr f (coeffs p)"
lemma fold_coeffs_0_eq [simp]: "fold_coeffs f 0 = id" by (simp add: fold_coeffs_def)
lemma fold_coeffs_pCons_eq [simp]: "f 0 = id ==> fold_coeffs f (pCons a p) = f a ∘fold_coeffs f p" by (simp add: fold_coeffs_def cCons_def fun_eq_iff)
lemma fold_coeffs_pCons_0_0_eq [simp]: "fold_coeffs f (pCons 0 0) = id" by (simp add: fold_coeffs_def)
lemma fold_coeffs_pCons_coeff_not_0_eq [simp]: "a ≠ 0 ==> fold_coeffs f (pCons a p) = f a ∘ fold_coeffs f p" by (simp add: fold_coeffs_def)
lemma fold_coeffs_pCons_not_0_0_eq [simp]: "p ≠ 0 ==> fold_coeffs f (pCons a p) = f a ∘ fold_coeffs f p" by (simp add: fold_coeffs_def)
subsection‹Canonical morphism on polynomials -- evaluation›
definition poly :: ‹'a::comm_semiring_0 poly ==> 'a ==> 'a› where‹poly p a = horner_sum id a (coeffs p)›
lemma poly_eq_fold_coeffs: ‹poly p = fold_coeffs (λa f x. a + x * f x) p (λx. 0)› by (induction p) (auto simp add: fun_eq_iff poly_def)
lemma poly_0 [simp]: "poly 0 x = 0" by (simp add: poly_def)
lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" by (cases "p = 0 ∧ a = 0") (auto simp add: poly_def)
lemma poly_altdef: "poly p x = (∑i≤degree p. coeff p i * x ^ i)" for x :: "'a::{comm_semiring_0,semiring_1}" proof (induction p rule: pCons_induct) case 0 thenshow ?case by simp next case (pCons a p) show ?case proof (cases "p = 0") case True thenshow ?thesis by simp next case False let ?p' = "pCons a p" note poly_pCons[of a p x] alsonote pCons.IH alsohave"a + x * (∑i≤degree p. coeff p i * x ^ i) = coeff ?p' 0 * x^0 + (∑i≤degree p. coeff ?p' (Suc i) * x^Suc i)" by (simp add: field_simps sum_distrib_left coeff_pCons) alsonote sum.atMost_Suc_shift[symmetric] alsonote degree_pCons_eq[OF ‹p ≠ 0›, of a, symmetric] finallyshow ?thesis . qed qed
lemma poly_0_coeff_0: "poly p 0 = coeff p 0" by (cases p) (auto simp: poly_altdef)
lemma poly_zero: fixes p :: "'a :: comm_ring_1 poly" assumes x: "poly p x = 0"shows"p = 0 ⟷ degree p = 0" proof assume degp: "degree p = 0" hence"poly p x = coeff p (degree p)"by(subst degree_0_id[OF degp,symmetric], simp) hence"coeff p (degree p) = 0"using x by auto thus"p = 0"by auto qed auto
subsection‹Monomials›
lift_definition monom :: "'a ==> nat ==> 'a::zero poly" is"λa m n. if m = n then a else 0" by (simp add: MOST_iff_cofinite)
lemma coeff_monom [simp]: "coeff (monom a m) n = (if m = n then a else 0)" by transfer rule
lemma monom_0: "monom a 0 = [:a:]" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
lemma monom_eq_0 [simp]: "monom 0 n = 0" by (rule poly_eqI) simp
lemma monom_eq_0_iff [simp]: "monom a n = 0 ⟷ a = 0" by (simp add: poly_eq_iff)
lemma monom_eq_iff [simp]: "monom a n = monom b n ⟷ a = b" by (simp add: poly_eq_iff)
lemma degree_monom_le: "degree (monom a n) ≤ n" by (rule degree_le, simp)
lemma degree_monom_eq: "a ≠ 0 ==> degree (monom a n) = n" by (metis coeff_monom leading_coeff_0_iff)
lemma coeffs_monom [code abstract]: "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])" by (induct n) (simp_all add: monom_0 monom_Suc)
lemma fold_coeffs_monom [simp]: "a ≠ 0 ==> fold_coeffs f (monom a n) = f 0 ^^ n ∘ f a" by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)
lemma poly_monom: "poly (monom a n) x = a * x ^ n" for a x :: "'a::comm_semiring_1" by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_eq_fold_coeffs)
lemma monom_eq_iff': "monom c n = monom d m ⟷ c = d ∧ (c = 0 ∨ n = m)" by (auto simp: poly_eq_iff)
lemma monom_eq_const_iff: "monom c n = [:d:] ⟷ c = d ∧ (c = 0 ∨ n = 0)" using monom_eq_iff'[of c n d 0] by (simp add: monom_0)
subsection‹Leading coefficient›
abbreviation lead_coeff:: "'a::zero poly ==> 'a" where"lead_coeff p ≡ coeff p (degree p)"
lemma lead_coeff_pCons[simp]: "p ≠ 0 ==> lead_coeff (pCons a p) = lead_coeff p" "p = 0 ==> lead_coeff (pCons a p) = a" by auto
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c" by (cases "c = 0") (simp_all add: degree_monom_eq)
lemma last_coeffs_eq_coeff_degree: "last (coeffs p) = lead_coeff p"if"p ≠ 0" using that by (simp add: coeffs_def)
lemma lead_coeff_list_def: "lead_coeff p = (if coeffs p=[] then 0 else last (coeffs p))" by (simp add: last_coeffs_eq_coeff_degree)
subsection‹Addition and subtraction›
instantiation poly :: (comm_monoid_add) comm_monoid_add begin
lift_definition plus_poly :: "'a poly ==> 'a poly ==> 'a poly" is"λp q n. coeff p n + coeff q n" proof - fix q p :: "'a poly" show"∀🪙∞n. coeff p n + coeff q n = 0" using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp qed
lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n" by (simp add: plus_poly.rep_eq)
instance proof fix p q r :: "'a poly" show"(p + q) + r = p + (q + r)" by (simp add: poly_eq_iff add.assoc) show"p + q = q + p" by (simp add: poly_eq_iff add.commute) show"0 + p = p" by (simp add: poly_eq_iff) qed
end
instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add begin
lift_definition minus_poly :: "'a poly ==> 'a poly ==> 'a poly" is"λp q n. coeff p n - coeff q n" proof - fix q p :: "'a poly" show"∀🪙∞n. coeff p n - coeff q n = 0" using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp qed
lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n" by (simp add: minus_poly.rep_eq)
instance proof fix p q r :: "'a poly" show"p + q - p = q" by (simp add: poly_eq_iff) show"p - q - r = p - (q + r)" by (simp add: poly_eq_iff diff_diff_eq) qed
end
instantiation poly :: (ab_group_add) ab_group_add begin
lift_definition uminus_poly :: "'a poly ==> 'a poly" is"λp n. - coeff p n" proof - fix p :: "'a poly" show"∀🪙∞n. - coeff p n = 0" using MOST_coeff_eq_0 by simp qed
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n" by (simp add: uminus_poly.rep_eq)
instance proof fix p q :: "'a poly" show"- p + p = 0" by (simp add: poly_eq_iff) show"p - q = p + - q" by (simp add: poly_eq_iff) qed
end
lemma add_pCons [simp]: "pCons a p + pCons b q = pCons (a + b) (p + q)" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
lemma minus_pCons [simp]: "- pCons a p = pCons (- a) (- p)" by (rule poly_eqI) (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_eqI) (simp add: coeff_pCons split: nat.split)
lemma degree_add_le_max: "degree (p + q) ≤ max (degree p) (degree q)" by (rule degree_le) (auto simp add: coeff_eq_0)
lemma degree_add_le: "degree p ≤ n ==> degree q ≤ n ==> degree (p + q) ≤ n" by (auto intro: order_trans degree_add_le_max)
lemma degree_add_less: "degree p < n ==> degree q < n ==> degree (p + q) < n" by (auto intro: le_less_trans degree_add_le_max)
lemma degree_add_eq_right: assumes"degree p < degree q"shows"degree (p + q) = degree q" proof (cases "q = 0") case False show ?thesis proof (rule order_antisym) show"degree (p + q) ≤ degree q" by (simp add: assms degree_add_le order.strict_implies_order) show"degree q ≤ degree (p + q)" by (simp add: False assms coeff_eq_0 le_degree) qed qed (use assms in auto)
lemma degree_add_eq_left: "degree q < degree p ==> degree (p + q) = degree p" using degree_add_eq_right [of q p] by (simp add: add.commute)
lemma degree_diff_le_max: "degree (p - q) ≤ max (degree p) (degree q)" for p q :: "'a::ab_group_add poly" using degree_add_le [where p=p and q="-q"] by simp
lemma degree_diff_le: "degree p ≤ n ==> degree q ≤ n ==> degree (p - q) ≤ n" for p q :: "'a::ab_group_add poly" using degree_add_le [of p n "- q"] by simp
lemma degree_diff_less: "degree p < n ==> degree q < n ==> degree (p - q) < n" for p q :: "'a::ab_group_add poly" using degree_add_less [of p n "- q"] by simp
lemma add_monom: "monom a n + monom b n = monom (a + b) n" by (rule poly_eqI) simp
lemma diff_monom: "monom a n - monom b n = monom (a - b) n" by (rule poly_eqI) simp
lemma minus_monom: "- monom a n = monom (- a) n" by (rule poly_eqI) simp
lemma coeff_sum: "coeff (∑x∈A. p x) i = (∑x∈A. coeff (p x) i)" by (induct A rule: infinite_finite_induct) simp_all
lemma monom_sum: "monom (∑x∈A. a x) n = (∑x∈A. monom (a x) n)" by (rule poly_eqI) (simp add: coeff_sum)
fun plus_coeffs :: "'a::comm_monoid_add list ==> 'a list ==> 'a list" where "plus_coeffs xs [] = xs"
| "plus_coeffs [] ys = ys"
| "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"
lemma coeffs_plus_eq_plus_coeffs [code abstract]: "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)" proof - have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" for xs ys :: "'a list"and n proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) case (3 x xs y ys n) thenshow ?case by (cases n) (auto simp add: cCons_def) qed simp_all have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)" if"no_trailing (HOL.eq 0) xs"and"no_trailing (HOL.eq 0) ys" for xs ys :: "'a list" using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def) show ?thesis by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **) qed
lemma coeffs_uminus [code abstract]: "coeffs (- p) = map uminus (coeffs p)" proof - have eq_0: "HOL.eq 0 ∘ uminus = HOL.eq (0::'a)" by (simp add: fun_eq_iff) show ?thesis by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0) qed
lemma [code]: "p - q = p + - q" for p q :: "'a::ab_group_add poly" by (fact diff_conv_add_uminus)
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" proof (induction p arbitrary: q) case (pCons a p) thenshow ?case by (cases q) (simp add: algebra_simps) qed auto
lemma poly_minus [simp]: "poly (- p) x = - poly p x" for x :: "'a::comm_ring" by (induct p) simp_all
lemma poly_diff [simp]: "poly (p - q) x = poly p x - poly q x" for x :: "'a::comm_ring" using poly_add [of p "- q" x] by simp
lemma poly_sum: "poly (∑k∈A. p k) x = (∑k∈A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all
lemma poly_sum_list: "poly (∑p←ps. p) y = (∑p←ps. poly p y)" by (induction ps) auto
lemma poly_sum_mset: "poly (∑x∈#A. p x) y = (∑x∈#A. poly (p x) y)" by (induction A) auto
lemma degree_sum_le: "finite S ==> (∧p. p ∈ S ==> degree (f p) ≤ n) ==> degree (sum f S) ≤ n" proof (induct S rule: finite_induct) case empty thenshow ?caseby simp next case (insert p S) thenhave"degree (sum f S) ≤ n""degree (f p) ≤ n" by auto thenshow ?case unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le) qed
lemma degree_sum_less: assumes"∧x. x ∈ A ==> degree (f x) < n""n > 0" shows"degree (sum f A) < n" using assms by (induction rule: infinite_finite_induct) (auto intro!: degree_add_less)
lemma poly_as_sum_of_monoms': assumes"degree p ≤ n" shows"(∑i≤n. monom (coeff p i) i) = p" proof - have eq: "∧i. {..n} ∩ {i} = (if i ≤ n then {i} else {})" by auto from assms show ?thesis by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq
if_distrib[where f="λx. x * a"for a]) qed
lemma poly_as_sum_of_monoms: "(∑i≤degree p. monom (coeff p i) i) = p" by (intro poly_as_sum_of_monoms' order_refl)
subsection‹Multiplication by a constant, polynomial multiplication and the unit polynomial›
lift_definition smult :: "'a::comm_semiring_0 ==> 'a poly ==> 'a poly" is"λa p n. a * coeff p n" proof - fix a :: 'a and p :: "'a poly" show"∀🪙∞ i. a * coeff p i = 0" using MOST_coeff_eq_0[of p] by eventually_elim simp qed
lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n" by (simp add: smult.rep_eq)
lemma degree_smult_le: "degree (smult a p) ≤ degree p" by (rule degree_le) (simp add: coeff_eq_0)
lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" by (rule poly_eqI) (simp add: mult.assoc)
lemma smult_0_right [simp]: "smult a 0 = 0" by (rule poly_eqI) simp
lemma smult_0_left [simp]: "smult 0 p = 0" by (rule poly_eqI) simp
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" by (rule poly_eqI) simp
lemma smult_add_right: "smult a (p + q) = smult a p + smult a q" by (rule poly_eqI) (simp add: algebra_simps)
lemma smult_add_left: "smult (a + b) p = smult a p + smult b p" by (rule poly_eqI) (simp add: algebra_simps)
lemma smult_minus_right [simp]: "smult a (- p) = - smult a p" for a :: "'a::comm_ring" by (rule poly_eqI) simp
lemma smult_minus_left [simp]: "smult (- a) p = - smult a p" for a :: "'a::comm_ring" by (rule poly_eqI) simp
lemma smult_diff_right: "smult a (p - q) = smult a p - smult a q" for a :: "'a::comm_ring" by (rule poly_eqI) (simp add: algebra_simps)
lemma smult_diff_left: "smult (a - b) p = smult a p - smult b p" for a b :: "'a::comm_ring" by (rule poly_eqI) (simp add: algebra_simps)
lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)" by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)
lemma smult_monom: "smult a (monom b n) = monom (a * b) n" by (induct n) (simp_all add: monom_0 monom_Suc)
lemma smult_Poly: "smult c (Poly xs) = Poly (map ((*) c) xs)" by (auto simp: poly_eq_iff nth_default_def)
lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)" for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" by (cases "a = 0") (simp_all add: degree_def)
lemma smult_eq_0_iff [simp]: "smult a p = 0 ⟷ a = 0 ∨ p = 0" for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" by (simp add: poly_eq_iff)
lemma coeffs_smult [code abstract]: "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof - have eq_0: "HOL.eq 0 ∘ times a = HOL.eq (0::'a)"if"a ≠ 0" using that by (simp add: fun_eq_iff) show ?thesis by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0) qed
lemma smult_eq_iff: fixes b :: "'a :: field" assumes"b ≠ 0" shows"smult a p = smult b q ⟷ smult (a / b) p = q"
(is"?lhs ⟷ ?rhs") proof assume ?lhs alsofrom assms have"smult (inverse b) … = q" by simp finallyshow ?rhs by (simp add: field_simps) next assume ?rhs with assms show ?lhs by auto qed
lemma smult_cancel: fixes p::"'a::idom poly" assumes"c≠0"and smult: "smult c p = smult c q" shows"p=q" proof - have"smult c (p-q) = 0"using smult by (metis diff_self smult_diff_right) thus ?thesis using‹c≠0›by auto qed
instantiation poly :: (comm_semiring_0) comm_semiring_0 begin
definition"p * q = fold_coeffs (λa p. smult a q + pCons 0 p) p 0"
lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" by (induct p) (simp_all add: mult_poly_0 smult_add_right)
lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" by (induct q) (simp_all add: mult_poly_0 smult_add_right)
lemma mult_poly_add_left: "(p + q) * r = p * r + q * r" for p q r :: "'a poly" by (induct r) (simp_all add: mult_poly_0 smult_distribs algebra_simps)
instance proof fix p q r :: "'a poly" show 0: "0 * p = 0" by (rule mult_poly_0_left) show"p * 0 = 0" by (rule mult_poly_0_right) show"(p + q) * r = p * r + q * r" by (rule mult_poly_add_left) show"(p * q) * r = p * (q * r)" by (induct p) (simp_all add: mult_poly_0 mult_poly_add_left) show"p * q = q * p" by (induct p) (simp_all add: mult_poly_0) qed
end
lemma coeff_mult_degree_sum: "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)" by (induct p) (simp_all add: coeff_eq_0)
instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors proof fix p q :: "'a poly" assume"p ≠ 0"and"q ≠ 0" have"coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)" by (rule coeff_mult_degree_sum) alsofrom‹p ≠ 0›‹q ≠ 0›have"coeff p (degree p) * coeff q (degree q) ≠ 0" by simp finallyhave"∃n. coeff (p * q) n ≠ 0" .. thenshow"p * q ≠ 0" by (simp add: poly_eq_iff) qed
lemma coeff_mult: "coeff (p * q) n = (∑i≤n. coeff p i * coeff q (n-i))" proof (induct p arbitrary: n) case 0 show ?caseby simp next case (pCons a p n) thenshow ?case by (cases n) (simp_all add: sum.atMost_Suc_shift del: sum.atMost_Suc) qed
lemma coeff_mult_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0" by (simp add: coeff_mult)
lemma degree_mult_le: "degree (p * q) ≤ degree p + degree q" proof (rule degree_le) show"∀i>degree p + degree q. coeff (p * q) i = 0" by (induct p) (simp_all add: coeff_eq_0 coeff_pCons split: nat.split) qed
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)
instantiation poly :: (comm_semiring_1) comm_semiring_1 begin
lemma monom_eq_1_iff: "monom c n = 1 ⟷ c = 1 ∧ n = 0" using monom_eq_const_iff [of c n 1] by auto
lemma monom_altdef: "monom c n = smult c ([:0, 1:] ^ n)" by (induct n) (simp_all add: monom_0 monom_Suc)
lemma degree_sum_list_le: "(∧ p . p ∈ set ps ==> degree p ≤ n) ==> degree (sum_list ps) ≤ n" proof (induct ps) case (Cons p ps) hence"degree (sum_list ps) ≤ n""degree p ≤ n"by auto thus ?caseunfolding sum_list.Cons by (metis degree_add_le) qed simp
lemma degree_prod_list_le: "degree (prod_list ps) ≤ sum_list (map degree ps)" proof (induct ps) case (Cons p ps) show ?caseunfolding prod_list.Cons by (rule order.trans[OF degree_mult_le], insert Cons, auto) qed simp
lemma prod_smult: "(∏x∈A. smult (c x) (p x)) = smult (prod c A) (prod p A)" by (induction A rule: infinite_finite_induct) (auto simp: mult_ac)
lemma degree_power_le: "degree (p ^ n) ≤ degree p * n" by (induct n) (auto intro: order_trans degree_mult_le)
lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n" by (induct n) (simp_all add: coeff_mult)
lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" by (induct p) (simp_all add: algebra_simps)
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" by (induct p) (simp_all add: algebra_simps)
lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n" for p :: "'a::comm_semiring_1 poly" by (induct n) simp_all
lemma poly_prod: "poly (∏k∈A. p k) x = (∏k∈A. poly (p k) x)" by (induct A rule: infinite_finite_induct) simp_all
lemma poly_prod_list: "poly (∏p←ps. p) y = (∏p←ps. poly p y)" by (induction ps) auto
lemma poly_prod_mset: "poly (∏x∈#A. p x) y = (∏x∈#A. poly (p x) y)" by (induction A) auto
lemma poly_const_pow: "[: c :] ^ n = [: c ^ n :]" by (induction n) (auto simp: algebra_simps)
lemma monom_power: "monom c n ^ k = monom (c ^ k) (n * k)" by (induction k) (auto simp: mult_monom)
lemma degree_prod_sum_le: "finite S ==> degree (prod f S) ≤ sum (degree ∘ f) S" proof (induct S rule: finite_induct) case empty thenshow ?caseby simp next case (insert a S) show ?case unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] by (rule le_trans[OF degree_mult_le]) (use insert in auto) qed
lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (λp. coeff p 0) xs)" by (induct xs) (simp_all add: coeff_mult)
lemma coeff_monom_mult: "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))" proof - have"coeff (monom c n * p) k = (∑i≤k. (if n = i then c else 0) * coeff p (k - i))" by (simp add: coeff_mult) alsohave"… = (∑i≤k. (if n = i then c * coeff p (k - i) else 0))" by (intro sum.cong) simp_all alsohave"… = (if k < n then 0 else c * coeff p (k - n))" by simp finallyshow ?thesis . qed
lemma coeff_monom_Suc: "coeff (monom a (Suc d) * p) (Suc i) = coeff (monom a d * p) i" by (simp add: monom_Suc)
lemma monom_1_dvd_iff': "monom 1 n dvd p ⟷ (∀k proof assume"monom 1 n dvd p" thenobtain r where"p = monom 1 n * r" by (rule dvdE) thenshow"∀k by (simp add: coeff_mult) next assume zero: "(∀k
define r where"r = Abs_poly (λk. coeff p (k + n))" have"∀🪙∞k. coeff p (k + n) = 0" by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg,
subst cofinite_eq_sequentially [symmetric]) transfer thenhave coeff_r [simp]: "coeff r k = coeff p (k + n)"for k unfolding r_def by (subst poly.Abs_poly_inverse) simp_all have"p = monom 1 n * r" by (rule poly_eqI, subst coeff_monom_mult) (simp_all add: zero) thenshow"monom 1 n dvd p"by simp qed
lemma coeff_sum_monom: assumes n: "n ≤ d" shows"coeff (∑i≤d. monom (f i) i) n = f n" (is"?l = _") proof - have"?l = (∑i≤d. coeff (monom (f i) i) n)" (is"_ = sum ?cmf _") using coeff_sum. alsohave"{..d} = insert n ({..d}-{n})"using n by auto hence"sum ?cmf {..d} = sum ?cmf ..."by auto alsohave"... = sum ?cmf ({..d}-{n}) + ?cmf n"by (subst sum.insert,auto) alsohave"sum ?cmf ({..d}-{n}) = 0"by (subst sum.neutral, auto) finallyshow ?thesis by simp qed
subsection‹Mapping polynomials›
definition map_poly :: "('a :: zero ==> 'b :: zero) ==> 'a poly ==> 'b poly" where"map_poly f p = Poly (map f (coeffs p))"
lemma map_poly_0 [simp]: "map_poly f 0 = 0" by (simp add: map_poly_def)
lemma map_poly_1: "map_poly f 1 = [:f 1:]" by (simp add: map_poly_def)
lemma map_poly_1' [simp]: "f 1 = 1 ==> map_poly f 1 = 1" by (simp add: map_poly_def one_pCons)
lemma coeff_map_poly: assumes"f 0 = 0" shows"coeff (map_poly f p) n = f (coeff p n)" by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0
simp del: upt_Suc)
lemma lead_coeff_map_poly_nz: assumes"f (lead_coeff p) ≠ 0""f 0 = 0" shows"lead_coeff (map_poly f p) = f (lead_coeff p)" by (metis (no_types, lifting) antisym assms coeff_0 coeff_map_poly le_degree leading_coeff_0_iff)
lemma coeffs_map_poly [code abstract]: "coeffs (map_poly f p) = strip_while ((=) 0) (map f (coeffs p))" by (simp add: map_poly_def)
lemma coeffs_map_poly': assumes"∧x. x ≠ 0 ==> f x ≠ 0" shows"coeffs (map_poly f p) = map f (coeffs p)" using assms by (auto simp add: coeffs_map_poly strip_while_idem_iff
last_coeffs_eq_coeff_degree no_trailing_unfold last_map)
lemma set_coeffs_map_poly: "(∧x. f x = 0 ⟷ x = 0) ==> set (coeffs (map_poly f p)) = f ` set (coeffs p)" by (simp add: coeffs_map_poly')
lemma degree_map_poly: assumes"∧x. x ≠ 0 ==> f x ≠ 0" shows"degree (map_poly f p) = degree p" by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
lemma map_poly_eq_0_iff: assumes"f 0 = 0""∧x. x ∈ set (coeffs p) ==> x ≠ 0 ==> f x ≠ 0" shows"map_poly f p = 0 ⟷ p = 0" proof - have"(coeff (map_poly f p) n = 0) = (coeff p n = 0)"for n proof - have"coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms) alsohave"… = 0 ⟷ coeff p n = 0" proof (cases "n < length (coeffs p)") case True thenhave"coeff p n ∈ set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc) with assms show"f (coeff p n) = 0 ⟷ coeff p n = 0" by auto next case False thenshow ?thesis by (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) qed finallyshow ?thesis . qed thenshow ?thesis by (auto simp: poly_eq_iff) qed
lemma map_poly_smult: assumes"f 0 = 0""∧c x. f (c * x) = f c * f x" shows"map_poly f (smult c p) = smult (f c) (map_poly f p)" by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
lemma map_poly_pCons: assumes"f 0 = 0" shows"map_poly f (pCons c p) = pCons (f c) (map_poly f p)" by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
lemma map_poly_map_poly: assumes"f 0 = 0""g 0 = 0" shows"map_poly f (map_poly g p) = map_poly (f ∘ g) p" by (intro poly_eqI) (simp add: coeff_map_poly assms)
lemma map_poly_id [simp]: "map_poly id p = p" by (simp add: map_poly_def)
lemma map_poly_id' [simp]: "map_poly (λx. x) p = p" by (simp add: map_poly_def)
lemma map_poly_cong: assumes"(∧x. x ∈ set (coeffs p) ==> f x = g x)" shows"map_poly f p = map_poly g p" proof - from assms have"map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all thenshow ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly) qed
lemma map_poly_monom: "f 0 = 0 ==> map_poly f (monom c n) = monom (f c) n" by (intro poly_eqI) (simp_all add: coeff_map_poly)
lemma map_poly_idI: assumes"∧x. x ∈ set (coeffs p) ==> f x = x" shows"map_poly f p = p" using map_poly_cong[OF assms, of _ id] by simp
lemma map_poly_idI': assumes"∧x. x ∈ set (coeffs p) ==> f x = x" shows"p = map_poly f p" using map_poly_cong[OF assms, of _ id] by simp
lemma smult_conv_map_poly: "smult c p = map_poly (λx. c * x) p" by (intro poly_eqI) (simp_all add: coeff_map_poly)
lemma poly_cnj: "cnj (poly p z) = poly (map_poly cnj p) (cnj z)" by (simp add: poly_altdef degree_map_poly coeff_map_poly)
lemma poly_cnj_real: assumes"∧n. poly.coeff p n ∈ℝ" shows"cnj (poly p z) = poly p (cnj z)" proof - from assms have"map_poly cnj p = p" by (intro poly_eqI) (auto simp: coeff_map_poly Reals_cnj_iff) with poly_cnj[of p z] show ?thesis by simp qed
lemma real_poly_cnj_root_iff: assumes"∧n. poly.coeff p n ∈ℝ" shows"poly p (cnj z) = 0 ⟷ poly p z = 0" proof - have"poly p (cnj z) = cnj (poly p z)" by (simp add: poly_cnj_real assms) alsohave"… = 0 ⟷ poly p z = 0"by simp finallyshow ?thesis . qed
lemma sum_to_poly: "(∑x∈A. [:f x:]) = [:∑x∈A. f x:]" by (induction A rule: infinite_finite_induct) auto
lemma coeff_linear_poly_power: fixes c :: "'a :: semiring_1" assumes"i ≤ n" shows"coeff ([:a, b:] ^ n) i = of_nat (n choose i) * b ^ i * a ^ (n - i)" proof - have"[:a, b:] = monom b 1 + [:a:]" by (simp add: monom_altdef) alsohave"coeff (… ^ n) i = (∑k≤n. a^(n-k) * of_nat (n choose k) * (if k = i then b ^ k else 0))" by (subst binomial_ring) (simp add: coeff_sum of_nat_poly monom_power poly_const_pow mult_ac) alsohave"… = (∑k∈{i}. a ^ (n - i) * b ^ i * of_nat (n choose k))" using assms by (intro sum.mono_neutral_cong_right) (auto simp: mult_ac) finallyshow *: ?thesis by (simp add: mult_ac) qed
subsection‹Lemmas about divisibility›
lemma dvd_smult: assumes"p dvd q" shows"p dvd smult a q" proof - from assms obtain k where"q = p * k" .. thenhave"smult a q = p * smult a k"by simp thenshow"p dvd smult a q" .. qed
lemma dvd_smult_cancel: "p dvd smult a q ==> a ≠ 0 ==> p dvd q" for a :: "'a::field" by (drule dvd_smult [where a="inverse a"]) simp
lemma dvd_smult_iff: "a ≠ 0 ==> p dvd smult a q ⟷ p dvd q" for a :: "'a::field" by (safe elim!: dvd_smult dvd_smult_cancel)
lemma smult_dvd_cancel: assumes"smult a p dvd q" shows"p dvd q" proof - from assms obtain k where"q = smult a p * k" .. thenhave"q = p * smult a k"by simp thenshow"p dvd q" .. qed
lemma smult_dvd: "p dvd q ==> a ≠ 0 ==> smult a p dvd q" for a :: "'a::field" by (rule smult_dvd_cancel [where a="inverse a"]) simp
lemma smult_dvd_iff: "smult a p dvd q ⟷ (if a = 0 then q = 0 else p dvd q)" for a :: "'a::field" by (auto elim: smult_dvd smult_dvd_cancel)
lemma is_unit_smult_iff: "smult c p dvd 1 ⟷ c dvd 1 ∧ p dvd 1" proof - have"smult c p = [:c:] * p"by simp alsohave"… dvd 1 ⟷ c dvd 1 ∧ p dvd 1" proof safe assume *: "[:c:] * p dvd 1" thenshow"p dvd 1" by (rule dvd_mult_right) from * obtain q where q: "1 = [:c:] * p * q" by (rule dvdE) have"c dvd c * (coeff p 0 * coeff q 0)" by simp alsohave"… = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult) alsonote q [symmetric] finallyhave"c dvd coeff 1 0" . thenshow"c dvd 1"by simp next assume"c dvd 1""p dvd 1" from this(1) obtain d where"1 = c * d" by (rule dvdE) thenhave"1 = [:c:] * [:d:]" by (simp add: one_pCons ac_simps) thenhave"[:c:] dvd 1" by (rule dvdI) from mult_dvd_mono[OF this ‹p dvd 1›] show"[:c:] * p dvd 1" by simp qed finallyshow ?thesis . qed
subsection‹Polynomials form an integral domain›
instance poly :: (idom) idom ..
instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0 by standard (auto simp add: of_nat_poly intro: injI)
instance poly :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char by (rule semiring_prime_charI) auto instance poly :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char by standard instance poly :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char by standard instance poly :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char by standard
lemma degree_mult_eq: "p ≠ 0 ==> q ≠ 0 ==> degree (p * q) = degree p + degree q" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)
lemma degree_prod_sum_eq: "(∧x. x ∈ A ==> f x ≠ 0) ==> degree (prod f A :: 'a :: idom poly) = (∑x∈A. degree (f x))" by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)
lemma dvd_imp_degree: ‹degree x ≤ degree y›if‹x dvd y›‹x ≠ 0›‹y ≠ 0› for x y :: ‹'a::{comm_semiring_1,semiring_no_zero_divisors} poly› proof - from‹x dvd y›obtain z where‹y = x * z› .. with‹x ≠ 0›‹y ≠ 0›show ?thesis by (simp add: degree_mult_eq) qed
lemma degree_prod_eq_sum_degree: fixes A :: "'a set" and f :: "'a ==> 'b::idom poly" assumes f0: "∀i∈A. f i ≠ 0" shows"degree (∏i∈A. (f i)) = (∑i∈A. degree (f i))" using assms by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)
lemma degree_mult_eq_0: "degree (p * q) = 0 ⟷ p = 0 ∨ q = 0 ∨ (p ≠ 0 ∧ q ≠ 0 ∧ degree p = 0 ∧ degree q = 0)" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" by (auto simp: degree_mult_eq)
lemma degree_power_eq: "p ≠ 0 ==> degree ((p :: 'a :: idom poly) ^ n) = n * degree p" by (induction n) (simp_all add: degree_mult_eq)
lemma degree_mult_right_le: fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" assumes"q ≠ 0" shows"degree p ≤ degree (p * q)" using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
lemma coeff_degree_mult: "coeff (p * q) (degree (p * q)) = coeff q (degree q) * coeff p (degree p)" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" by (cases "p = 0 ∨ q = 0") (auto simp: degree_mult_eq coeff_mult_degree_sum mult_ac)
lemma dvd_imp_degree_le: "p dvd q ==> q ≠ 0 ==> degree p ≤ degree q" for p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" by (erule dvdE, hypsubst, subst degree_mult_eq) auto
lemma divides_degree: fixes p q :: "'a ::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes"p dvd q" shows"degree p ≤ degree q ∨ q = 0" by (metis dvd_imp_degree_le assms)
lemma const_poly_dvd_iff: fixes c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}" shows"[:c:] dvd p ⟷ (∀n. c dvd coeff p n)" proof (cases "c = 0 ∨ p = 0") case True thenshow ?thesis by (auto intro!: poly_eqI) next case False show ?thesis proof assume"[:c:] dvd p" thenshow"∀n. c dvd coeff p n" by (auto simp: coeffs_def) next assume *: "∀n. c dvd coeff p n"
define mydiv where"mydiv x y = (SOME z. x = y * z)"for x y :: 'a have mydiv: "x = y * mydiv x y"if"y dvd x"for x y using that unfolding mydiv_def dvd_def by (rule someI_ex)
define q where"q = Poly (map (λa. mydiv a c) (coeffs p))" from False * have"p = q * [:c:]" by (intro poly_eqI)
(auto simp: q_def nth_default_def not_less length_coeffs_degree coeffs_nth
intro!: coeff_eq_0 mydiv) thenshow"[:c:] dvd p" by (simp only: dvd_triv_right) qed qed
lemma const_poly_dvd_const_poly_iff [simp]: "[:a:] dvd [:b:] ⟷ a dvd b" for a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors}" by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)
lemma lead_coeff_mult: "lead_coeff (p * q) = lead_coeff p * lead_coeff q" for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly" by (cases "p = 0 ∨ q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq)
lemma lead_coeff_prod: "lead_coeff (prod f A) = (∏x∈A. lead_coeff (f x))" for f :: "'a ==> 'b::{comm_semiring_1, semiring_no_zero_divisors} poly" by (induction A rule: infinite_finite_induct) (auto simp: lead_coeff_mult)
lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p" for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof - have"smult c p = [:c:] * p"by simp alsohave"lead_coeff … = c * lead_coeff p" by (subst lead_coeff_mult) simp_all finallyshow ?thesis . qed
lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1" by simp
lemma lead_coeff_power: "lead_coeff (p ^ n) = lead_coeff p ^ n" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" by (induct n) (simp_all add: lead_coeff_mult)
subsection‹Polynomials form an ordered integral domain›
definition pos_poly :: "'a::linordered_semidom poly ==> bool" where"pos_poly p ⟷ 0 < coeff p (degree p)"
lemma pos_poly_pCons: "pos_poly (pCons a p) ⟷ pos_poly p ∨ (p = 0 ∧ 0 < a)" by (simp add: pos_poly_def)
lemma not_pos_poly_0 [simp]: "¬ pos_poly 0" by (simp add: pos_poly_def)
lemma pos_poly_add: "pos_poly p ==> pos_poly q ==> pos_poly (p + q)" proof (induction p arbitrary: q) case (pCons a p) thenshow ?case by (cases q; force simp add: pos_poly_pCons add_pos_pos) qed auto
lemma pos_poly_mult: "pos_poly p ==> pos_poly q ==> pos_poly (p * q)" by (simp add: pos_poly_def coeff_degree_mult)
lemma pos_poly_total: "p = 0 ∨ pos_poly p ∨ pos_poly (- p)" for p :: "'a::linordered_idom poly" by (induct p) (auto simp: pos_poly_pCons)
lemma pos_poly_coeffs [code]: "pos_poly p ⟷ (let as = coeffs p in as ≠ [] ∧ last as > 0)"
(is"?lhs ⟷ ?rhs") proof assume ?rhs thenshow ?lhs by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree) next assume ?lhs thenhave *: "0 < coeff p (degree p)" by (simp add: pos_poly_def) thenhave"p ≠ 0" by auto with * show ?rhs by (simp add: last_coeffs_eq_coeff_degree) qed
instantiation poly :: (linordered_idom) linordered_idom begin
definition"x < y ⟷ pos_poly (y - x)"
definition"x ≤ y ⟷ x = y ∨ pos_poly (y - x)"
definition"∣x::'a poly∣ = (if x < 0 then - x else x)"
definition"sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
instance proof fix x y z :: "'a poly" show"x < y ⟷ x ≤ y ∧¬ y ≤ x" unfolding less_eq_poly_def less_poly_def using pos_poly_add by force thenshow"x ≤ y ==> y ≤ x ==> x = y" using less_eq_poly_def less_poly_def by force show"x ≤ x" by (simp add: less_eq_poly_def) show"x ≤ y ==> y ≤ z ==> x ≤ z" using less_eq_poly_def pos_poly_add by fastforce show"x ≤ y ==> z + x ≤ z + y" by (simp add: less_eq_poly_def) show"x ≤ y ∨ y ≤ x" unfolding less_eq_poly_def using pos_poly_total [of "x - y"] by auto show"x < y ==> 0 < z ==> z * x < z * y" by (simp add: less_poly_def right_diff_distrib [symmetric] pos_poly_mult) show"∣x∣ = (if x < 0 then - x else x)" by (rule abs_poly_def) show"sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" by (rule sgn_poly_def) qed
end
text‹TODO: Simplification rules for comparisons›
subsection‹Synthetic division and polynomial roots›
subsubsection ‹Synthetic division›
text‹Synthetic division is simply division by the linear polynomial 🍋‹x - c›.›
definition synthetic_divmod :: "'a::comm_semiring_0 poly ==> 'a ==> 'a poly × 'a" where"synthetic_divmod p c = fold_coeffs (λa (q, r). (pCons r q, a + c * r)) p (0, 0)"
definition synthetic_div :: "'a::comm_semiring_0 poly ==> 'a ==> 'a poly" where"synthetic_div p c = fst (synthetic_divmod p c)"
lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)" by (simp add: synthetic_divmod_def)
lemma synthetic_divmod_pCons [simp]: "synthetic_divmod (pCons a p) c = (λ(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" by (cases "p = 0 ∧ a = 0") (auto simp add: synthetic_divmod_def)
lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0" by (simp add: synthetic_div_def)
lemma synthetic_div_unique_lemma: "smult c p = pCons a p ==> p = 0" by (induct p arbitrary: a) simp_all
lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c" by (induct p) (simp_all add: split_def)
lemma synthetic_div_pCons [simp]: "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)" by (simp add: synthetic_div_def split_def snd_synthetic_divmod)
lemma synthetic_div_eq_0_iff: "synthetic_div p c = 0 ⟷ degree p = 0" proof (induct p) case 0 thenshow ?caseby simp next case (pCons a p) thenshow ?caseby (cases p) simp qed
lemma degree_synthetic_div: "degree (synthetic_div p c) = degree p - 1" by (induct p) (simp_all add: synthetic_div_eq_0_iff)
lemma synthetic_div_correct: "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)" by (induct p) simp_all
lemma synthetic_div_unique: "p + smult c q = pCons r q ==> r = poly p c ∧ q = synthetic_div p c" proof (induction p arbitrary: q r) case 0 thenshow ?case using synthetic_div_unique_lemma by fastforce next case (pCons a p) thenshow ?case by (cases q; force) qed
lemma synthetic_div_correct': "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" for c :: "'a::comm_ring_1" using synthetic_div_correct [of p c] by (simp add: algebra_simps)
subsubsection ‹Polynomial roots›
lemma poly_eq_0_iff_dvd: "poly p c = 0 ⟷ [:- c, 1:] dvd p"
(is"?lhs ⟷ ?rhs") for c :: "'a::comm_ring_1" proof assume ?lhs with synthetic_div_correct' [of c p] have"p = [:-c, 1:] * synthetic_div p c"by simp thenshow ?rhs .. next assume ?rhs thenobtain k where"p = [:-c, 1:] * k"by (rule dvdE) thenshow ?lhs by simp qed
lemma dvd_iff_poly_eq_0: "[:c, 1:] dvd p ⟷ poly p (- c) = 0" for c :: "'a::comm_ring_1" by (simp add: poly_eq_0_iff_dvd)
lemma poly_roots_finite: "p ≠ 0 ==> finite {x. poly p x = 0}" for p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" proof (induct n ≡"degree p" arbitrary: p) case 0 thenobtain a where"a ≠ 0"and"p = [:a:]" by (cases p) (simp split: if_splits) thenshow"finite {x. poly p x = 0}" by simp next case (Suc n) show"finite {x. poly p x = 0}" proof (cases "∃x. poly p x = 0") case False thenshow"finite {x. poly p x = 0}"by simp next case True thenobtain a where"poly p a = 0" .. thenhave"[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) thenobtain k where k: "p = [:-a, 1:] * k" .. with‹p ≠ 0›have"k ≠ 0" by auto with k have"degree p = Suc (degree k)" by (simp add: degree_mult_eq del: mult_pCons_left) with‹Suc n = degree p›have"n = degree k" by simp from this ‹k ≠ 0›have"finite {x. poly k x = 0}" by (rule Suc.hyps) thenhave"finite (insert a {x. poly k x = 0})" by simp thenshow"finite {x. poly p x = 0}" by (simp add: k Collect_disj_eq del: mult_pCons_left) qed qed
lemma poly_eq_poly_eq_iff: "poly p = poly q ⟷ p = q"
(is"?lhs ⟷ ?rhs") for p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly" proof assume ?rhs thenshow ?lhs by simp next assume ?lhs have"poly p = poly 0 ⟷ p = 0"for p :: "'a poly" proof (cases "p = 0") case False thenshow ?thesis by (auto simp add: infinite_UNIV_char_0 dest: poly_roots_finite) qed auto from‹?lhs›and this [of "p - q"] show ?rhs by auto qed
text‹A nice extension rule for polynomials.› lemma poly_ext: fixes p q :: "'a :: {ring_char_0, idom} poly" assumes"∧x. poly p x = poly q x"shows"p = q" unfolding poly_eq_poly_eq_iff[symmetric] using assms by (rule ext)
text‹Copied from non-negative variants.› lemma coeff_linear_power_neg[simp]: fixes a :: "'a::comm_ring_1" shows"coeff ([:a, -1:] ^ n) n = (-1)^n" proof (induct n) case 0 thenshow ?caseby simp next case (Suc n) thenhave"degree ([:a, - 1:] ^ n) < Suc n" by (auto intro: le_less_trans degree_power_le) with Suc show ?case by (simp add: coeff_eq_0) qed
lemma degree_linear_power_neg[simp]: fixes a :: "'a::{idom,comm_ring_1}" shows"degree ([:a, -1:] ^ n) = n" by (simp add: degree_power_eq)
lemma poly_all_0_iff_0: "(∀x. poly p x = 0) ⟷ p = 0" for p :: "'a::{ring_char_0,comm_ring_1,ring_no_zero_divisors} poly" by (auto simp add: poly_eq_poly_eq_iff [symmetric])
lemma card_poly_roots_bound: fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly" assumes"p ≠ 0" shows"card {x. poly p x = 0} ≤ degree p" using assms proof (induction"degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "∃x. poly p x = 0") case False hence"{x. poly p x = 0} = {}"by blast thus ?thesis by simp next case True thenobtain x where x: "poly p x = 0"by blast hence"[:-x, 1:] dvd p"by (subst (asm) poly_eq_0_iff_dvd) thenobtain q where q: "p = [:-x, 1:] * q"by (auto simp: dvd_def) with‹p ≠ 0›have [simp]: "q ≠ 0"by auto have deg: "degree p = Suc (degree q)" by (subst q, subst degree_mult_eq) auto have"card {x. poly p x = 0} ≤ card (insert x {x. poly q x = 0})" by (intro card_mono) (auto intro: poly_roots_finite simp: q) alsohave"…≤ Suc (card {x. poly q x = 0})" by (rule card_insert_le_m1) auto alsofrom deg have"card {x. poly q x = 0} ≤ degree q" using‹p ≠ 0›and q by (intro less) auto alsohave"Suc … = degree p"by (simp add: deg) finallyshow ?thesis by - simp_all qed qed
lemma poly_eqI_degree: fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" assumes"∧x. x ∈ A ==> poly p x = poly q x" assumes"card A > degree p""card A > degree q" shows"p = q" proof (rule ccontr) assume neq: "p ≠ q" have"degree (p - q) ≤ max (degree p) (degree q)" by (rule degree_diff_le_max) alsofrom assms have"… < card A"by linarith alsohave"…≤ card {x. poly (p - q) x = 0}" using neq and assms by (intro card_mono poly_roots_finite) auto finallyhave"degree (p - q) < card {x. poly (p - q) x = 0}" . moreoverhave"degree (p - q) ≥ card {x. poly (p - q) x = 0}" using neq by (intro card_poly_roots_bound) auto ultimatelyshow False by linarith qed
lemma poly_eqI_degree_lead_coeff: fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly" assumes"poly.coeff p n = poly.coeff q n""card A ≥ n""degree p ≤ n""degree q ≤ n" assumes"∧z. z ∈ A ==> poly p z = poly q z" shows"p = q" proof (rule ccontr) assume"p ≠ q"
have"n > 0" proof (rule ccontr) assume"¬(n > 0)" thus False using assms ‹p ≠ q›by (auto elim!: degree_eq_zeroE) qed
have"n ≤ card A" by fact alsohave"card A ≤ card {x. poly (p - q) x = 0}" by (intro card_mono poly_roots_finite) (use‹p ≠ q› assms in auto) alsohave"card {x. poly (p - q) x = 0} ≤ degree (p - q)" by (rule card_poly_roots_bound) (use‹p ≠ q›in auto) alsohave"degree (p - q) < n" proof (intro degree_lessI allI impI) fix k assume"k ≥ n" show"poly.coeff (p - q) k = 0" proof (cases "k = n") case False hence"poly.coeff p k = 0""poly.coeff q k = 0" using assms ‹k ≥ n›by (auto simp: coeff_eq_0) thus ?thesis by simp qed (use assms in auto) qed (use‹n > 0›in auto) finallyshow False by simp qed
subsubsection ‹Order of polynomial roots›
definition order :: "'a::idom ==> 'a poly ==> nat" where"order a p = (LEAST n. ¬ [:-a, 1:] ^ Suc n dvd p)"
lemma coeff_linear_power: "coeff ([:a, 1:] ^ n) n = 1" for a :: "'a::comm_semiring_1" proof (induct n) case (Suc n) have"degree ([:a, 1:] ^ n) ≤ 1 * n" by (metis One_nat_def degree_pCons_eq_if degree_power_le one_neq_zero one_pCons) thenhave"coeff ([:a, 1:] ^ n) (Suc n) = 0" by (simp add: coeff_eq_0) thenshow ?case using Suc.hyps by fastforce qed auto
lemma degree_linear_power: "degree ([:a, 1:] ^ n) = n" for a :: "'a::comm_semiring_1" proof (rule order_antisym) show"degree ([:a, 1:] ^ n) ≤ n" by (metis One_nat_def degree_pCons_eq_if degree_power_le mult.left_neutral one_neq_zero one_pCons) qed (simp add: coeff_linear_power le_degree)
lemma order_1: "[:-a, 1:] ^ order a p dvd p" proof (cases "p = 0") case False show ?thesis proof (cases "order a p") case (Suc n) thenshow ?thesis by (metis lessI not_less_Least order_def) qed auto qed auto
lemma order_2: assumes"p ≠ 0" shows"¬ [:-a, 1:] ^ Suc (order a p) dvd p" proof - have False if"[:- a, 1:] ^ Suc (degree p) dvd p" using dvd_imp_degree_le [OF that] by (metis Suc_n_not_le_n assms degree_linear_power) thenshow ?thesis unfolding order_def by (metis (no_types, lifting) LeastI) qed
lemma order: "p ≠ 0 ==> [:-a, 1:] ^ order a p dvd p ∧¬ [:-a, 1:] ^ Suc (order a p) dvd p" by (rule conjI [OF order_1 order_2])
lemma order_degree: assumes p: "p ≠ 0" shows"order a p ≤ degree p" proof - have"order a p = degree ([:-a, 1:] ^ order a p)" by (simp only: degree_linear_power) alsofrom order_1 p have"…≤ degree p" by (rule dvd_imp_degree_le) finallyshow ?thesis . qed
lemma order_root: "poly p a = 0 ⟷ p = 0 ∨ order a p ≠ 0" (is"?lhs = ?rhs") proof show"?lhs ==> ?rhs" by (metis One_nat_def order_2 poly_eq_0_iff_dvd power_one_right) show"?rhs ==> ?lhs" by (meson dvd_power dvd_trans neq0_conv order_1 poly_0 poly_eq_0_iff_dvd) qed
lemma order_0I: "poly p a ≠ 0 ==> order a p = 0" by (subst (asm) order_root) auto
lemma order_unique_lemma: fixes p :: "'a::idom poly" assumes"[:-a, 1:] ^ n dvd p""¬ [:-a, 1:] ^ Suc n dvd p" shows"order a p = n" unfolding Polynomial.order_def by (metis (mono_tags, lifting) Least_equality assms not_less_eq_eq power_le_dvd)
lemma order_mult: assumes"p * q ≠ 0"shows"order a (p * q) = order a p + order a q" proof -
define i where"i ≡ order a p"
define j where"j ≡ order a q"
define t where"t ≡ [:-a, 1:]" have t_dvd_iff: "∧u. t dvd u ⟷ poly u a = 0" by (simp add: t_def dvd_iff_poly_eq_0) have dvd: "t ^ i dvd p""t ^ j dvd q"and"¬ t ^ Suc i dvd p""¬ t ^ Suc j dvd q" using assms i_def j_def order_1 order_2 t_def by auto thenhave"¬ t ^ Suc(i + j) dvd p * q" by (elim dvdE) (simp add: power_add t_dvd_iff) moreoverhave"t ^ (i + j) dvd p * q" using dvd by (simp add: mult_dvd_mono power_add) ultimatelyshow"order a (p * q) = i + j" using order_unique_lemma t_def by blast qed
lemma order_smult: assumes"c ≠ 0" shows"order x (smult c p) = order x p" proof (cases "p = 0") case True thenshow ?thesis by simp next case False have"smult c p = [:c:] * p"by simp alsofrom assms False have"order x … = order x [:c:] + order x p" by (subst order_mult) simp_all alsohave"order x [:c:] = 0" by (rule order_0I) (use assms in auto) finallyshow ?thesis by simp qed
lemma order_gt_0_iff: "p ≠ 0 ==> order x p > 0 ⟷ poly p x = 0" by (subst order_root) auto
lemma order_eq_0_iff: "p ≠ 0 ==> order x p = 0 ⟷ poly p x ≠ 0" by (subst order_root) auto
text‹Next three lemmas contributed by Wenda Li› lemma order_1_eq_0 [simp]:"order x 1 = 0" by (metis order_root poly_1 zero_neq_one)
lemma order_uminus[simp]: "order x (-p) = order x p" by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left)
lemma order_power_n_n: "order a ([:-a,1:]^n)=n" proof (induct n) (*might be proved more concisely using nat_less_induct*) case 0 thenshow ?case by (metis order_root poly_1 power_0 zero_neq_one) next case (Suc n) have"order a ([:- a, 1:] ^ Suc n) = order a ([:- a, 1:] ^ n) + order a [:-a,1:]" by (metis (no_types, opaque_lifting) One_nat_def add_Suc_right monoid_add_class.add.right_neutral
one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right) moreoverhave"order a [:-a,1:] = 1" unfolding order_def proof (rule Least_equality, rule notI) assume"[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" thenhave"degree ([:- a, 1:] ^ Suc 1) ≤ degree ([:- a, 1:])" by (rule dvd_imp_degree_le) auto thenshow False by auto next fix y assume *: "¬ [:- a, 1:] ^ Suc y dvd [:- a, 1:]" show"1 ≤ y" proof (rule ccontr) assume"¬ 1 ≤ y" thenhave"y = 0"by auto thenhave"[:- a, 1:] ^ Suc y dvd [:- a, 1:]"by auto with * show False by auto qed qed ultimatelyshow ?case using Suc by auto qed
lemma order_0_monom [simp]: "c ≠ 0 ==> order 0 (monom c n) = n" using order_power_n_n[of 0 n] by (simp add: monom_altdef order_smult)
lemma dvd_imp_order_le: "q ≠ 0 ==> p dvd q ==> Polynomial.order a p ≤ Polynomial.order a q" by (auto simp: order_mult)
text‹Now justify the standard squarefree decomposition, i.e. ‹f / gcd f f'›.\<close>
lemma order_divides: "[:-a, 1:] ^ n dvd p ⟷ p = 0 ∨ n ≤ order a p" by (meson dvd_0_right not_less_eq_eq order_1 order_2 power_le_dvd)
lemma order_decomp: assumes"p ≠ 0" shows"∃q. p = [:- a, 1:] ^ order a p * q ∧¬ [:- a, 1:] dvd q" proof - from assms have *: "[:- a, 1:] ^ order a p dvd p" and **: "¬ [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order) from * obtain q where q: "p = [:- a, 1:] ^ order a p * q" .. with ** have"¬ [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q" by simp thenhave"¬ [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q" by simp with idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p""[:- a, 1:]" q] have"¬ [:- a, 1:] dvd q"by auto with q show ?thesis by blast qed
lemma monom_1_dvd_iff: "p ≠ 0 ==> monom 1 n dvd p ⟷ n ≤ order 0 p" using order_divides[of 0 n p] by (simp add: monom_altdef)
lemma poly_root_order_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes"P 0""∧p. (∧x. poly p x ≠ 0) ==> P p" "∧p x n. n > 0 ==> poly p x ≠ 0 ==> P p ==> P ([:-x, 1:] ^ n * p)" shows"P p" proof (induction"degree p" arbitrary: p rule: less_induct) case (less p)
consider "p = 0" | "p ≠ 0""∃x. poly p x = 0" | "∧x. poly p x ≠ 0"by blast thus ?case proof cases case 3 with assms(2)[of p] show ?thesis by simp next case 2 thenobtain x where x: "poly p x = 0"by auto have"[:-x, 1:] ^ order x p dvd p"by (intro order_1) thenobtain q where q: "p = [:-x, 1:] ^ order x p * q"by (auto simp: dvd_def) with 2 have [simp]: "q ≠ 0"by auto have order_pos: "order x p > 0" using‹p ≠ 0›and x by (auto simp: order_root) have"order x p = order x p + order x q" by (subst q, subst order_mult) (auto simp: order_power_n_n) hence [simp]: "order x q = 0"by simp have deg: "degree p = order x p + degree q" by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq) with order_pos have"degree q < degree p"by simp hence"P q"by (rule less) with order_pos have"P ([:-x, 1:] ^ order x p * q)" by (intro assms(3)) (auto simp: order_root) with q show ?thesis by simp qed (simp_all add: assms(1)) qed
context includes multiset.lifting begin
lift_definition proots :: "('a :: idom) poly ==> 'a multiset"is "λ(p :: 'a poly) (x :: 'a). if p = 0 then 0 else order x p" proof - fix p :: "'a poly" show"finite {x. 0 < (if p = 0 then 0 else order x p)}" by (cases "p = 0")
(auto simp: order_gt_0_iff intro: finite_subset[OF _ poly_roots_finite[of p]]) qed
lemma proots_0 [simp]: "proots (0 :: 'a :: idom poly) = {#}" by transfer' auto
lemma proots_1 [simp]: "proots (1 :: 'a :: idom poly) = {#}" by transfer' auto
lemma proots_const [simp]: "proots [: x :] = 0" by transfer' (auto split: if_splits simp: fun_eq_iff order_eq_0_iff)
lemma proots_mult: assumes"p ≠ 0""q ≠ 0" shows"proots (p * q) = proots p + proots q" using assms by (intro multiset_eqI) (auto simp: order_mult)
lemma proots_prod: assumes"∧x. x ∈ A ==> f x ≠ 0" shows"proots (∏x∈A. f x) = (∑x∈A. proots (f x))" using assms by (induction A rule: infinite_finite_induct) (auto simp: proots_mult)
lemma proots_prod_mset: assumes"0 ∉# A" shows"proots (∏p∈#A. p) = (∑p∈#A. proots p)" using assms by (induction A) (auto simp: proots_mult)
lemma proots_prod_list: assumes"0 ∉ set ps" shows"proots (∏p←ps. p) = (∑p←ps. proots p)" using assms by (induction ps) (auto simp: proots_mult prod_list_zero_iff)
lemma proots_power: "proots (p ^ n) = repeat_mset n (proots p)" proof (cases "p = 0") case False thus ?thesis by (induction n) (auto simp: proots_mult) qed (auto simp: power_0_left)
lemma proots_linear_factor [simp]: "proots [:x, 1:] = {#-x#}" proof - have"order (-x) [:x, 1:] > 0" by (subst order_gt_0_iff) auto moreoverhave"order (-x) [:x, 1:] ≤ degree [:x, 1:]" by (rule order_degree) auto moreoverhave"order y [:x, 1:] = 0"if"y ≠ -x"for y by (rule order_0I) (use that in‹auto simp: add_eq_0_iff›) ultimatelyshow ?thesis by (intro multiset_eqI) auto qed
lemma size_proots_le: "size (proots p) ≤ degree p" proof (induction p rule: poly_root_order_induct) case (no_roots p) hence"proots p = 0" by (simp add: multiset_eqI order_root) thus ?caseby simp next case (root p x n) have [simp]: "p ≠ 0" using root.hyps by auto from root.IH show ?case by (auto simp: proots_mult proots_power degree_mult_eq degree_power_eq) qed auto
end
subsection‹Additional induction rules on polynomials›
text‹ An induction rule for induction over the roots of a polynomial with a certain property. (e.g. all positive roots) › lemma poly_root_induct [case_names 0 no_roots root]: fixes p :: "'a :: idom poly" assumes"Q 0" and"∧p. (∧a. P a ==> poly p a ≠ 0) ==> Q p" and"∧a p. P a ==> Q p ==> Q ([:a, -1:] * p)" shows"Q p" proof (induction"degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "p = 0") case True with assms(1) show ?thesis by simp next case False show ?thesis proof (cases "∃a. P a ∧ poly p a = 0") case False thenshow ?thesis by (intro assms(2)) blast next case True thenobtain a where a: "P a""poly p a = 0" by blast thenhave"-[:-a, 1:] dvd p" by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd) thenobtain q where q: "p = [:a, -1:] * q"by (elim dvdE) simp with False have"q ≠ 0"by auto have"degree p = Suc (degree q)" by (subst q, subst degree_mult_eq) (simp_all add: ‹q ≠ 0›) thenhave"Q q"by (intro less) simp with a(1) have"Q ([:a, -1:] * q)" by (rule assms(3)) with q show ?thesis by simp qed qed qed
lemma dropWhile_replicate_append: "dropWhile ((=) a) (replicate n a @ ys) = dropWhile ((=) a) ys" by (induct n) simp_all
lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs" by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
text‹ An induction rule for simultaneous induction over two polynomials, prepending one coefficient in each step. › lemma poly_induct2 [case_names 0 pCons]: assumes"P 0 0""∧a p b q. P p q ==> P (pCons a p) (pCons b q)" shows"P p q" proof -
define n where"n = max (length (coeffs p)) (length (coeffs q))"
define xs where"xs = coeffs p @ (replicate (n - length (coeffs p)) 0)"
define ys where"ys = coeffs q @ (replicate (n - length (coeffs q)) 0)" have"length xs = length ys" by (simp add: xs_def ys_def n_def) thenhave"P (Poly xs) (Poly ys)" by (induct rule: list_induct2) (simp_all add: assms) alsohave"Poly xs = p" by (simp add: xs_def Poly_append_replicate_0) alsohave"Poly ys = q" by (simp add: ys_def Poly_append_replicate_0) finallyshow ?thesis . qed
subsection‹Composition of polynomials›
(* Several lemmas contributed by René Thiemann and Akihisa Yamada *)
definition pcompose :: "'a::comm_semiring_0 poly ==> 'a poly ==> 'a poly" where"pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0"
lemma pcompose_pCons: "pcompose (pCons a p) q = [:a:] + q * pcompose p q" by (cases "p = 0 ∧ a = 0") (auto simp add: pcompose_def)
lemma pcompose_altdef: "pcompose p q = poly (map_poly (λx. [:x:]) p) q" by (induction p) (simp_all add: map_poly_pCons pcompose_pCons)
lemma coeff_pcompose_0 [simp]: "coeff (pcompose p q) 0 = poly p (coeff q 0)" by (induction p) (simp_all add: coeff_mult_0 pcompose_pCons)
lemma pcompose_1: "pcompose 1 p = 1" for p :: "'a::comm_semiring_1 poly" by (auto simp: one_pCons pcompose_pCons)
lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)" by (induct p) (simp_all add: pcompose_pCons)
lemma degree_pcompose_le: "degree (pcompose p q) ≤ degree p * degree q" proof (induction p) case (pCons a p) thenshow ?case proof (clarsimp simp add: pcompose_pCons) assume"degree (p ∘🪙p q) ≤ degree p * degree q""p ≠ 0" thenhave"degree (q * p ∘🪙p q) ≤ degree q + degree p * degree q" by (meson add_le_cancel_left degree_mult_le dual_order.trans pCons.IH) thenshow"degree ([:a:] + q * p ∘🪙p q) ≤ degree q + degree p * degree q" by (simp add: degree_add_le) qed qed auto
lemma pcompose_add: "pcompose (p + q) r = pcompose p r + pcompose q r" for p q r :: "'a::{comm_semiring_0, ab_semigroup_add} poly" proof (induction p q rule: poly_induct2) case 0 thenshow ?caseby simp next case (pCons a p b q) have"pcompose (pCons a p + pCons b q) r = [:a + b:] + r * pcompose p r + r * pcompose q r" by (simp_all add: pcompose_pCons pCons.IH algebra_simps) alsohave"[:a + b:] = [:a:] + [:b:]"by simp alsohave"… + r * pcompose p r + r * pcompose q r = pcompose (pCons a p) r + pcompose (pCons b q) r" by (simp only: pcompose_pCons add_ac) finallyshow ?case . qed
lemma pcompose_uminus: "pcompose (-p) r = -pcompose p r" for p r :: "'a::comm_ring poly" by (induct p) (simp_all add: pcompose_pCons)
lemma pcompose_diff: "pcompose (p - q) r = pcompose p r - pcompose q r" for p q r :: "'a::comm_ring poly" using pcompose_add[of p "-q"] by (simp add: pcompose_uminus)
lemma pcompose_smult: "pcompose (smult a p) r = smult a (pcompose p r)" for p r :: "'a::comm_semiring_0 poly" by (induct p) (simp_all add: pcompose_pCons pcompose_add smult_add_right)
lemma pcompose_mult: "pcompose (p * q) r = pcompose p r * pcompose q r" for p q r :: "'a::comm_semiring_0 poly" by (induct p arbitrary: q) (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps)
lemma pcompose_assoc: "pcompose p (pcompose q r) = pcompose (pcompose p q) r" for p q r :: "'a::comm_semiring_0 poly" by (induct p arbitrary: q) (simp_all add: pcompose_pCons pcompose_add pcompose_mult)
lemma pcompose_idR[simp]: "pcompose p [: 0, 1 :] = p" for p :: "'a::comm_semiring_1 poly" by (induct p) (simp_all add: pcompose_pCons)
lemma pcompose_sum: "pcompose (sum f A) p = sum (λi. pcompose (f i) p) A" by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_add)
lemma pcompose_prod: "pcompose (prod f A) p = prod (λi. pcompose (f i) p) A" by (induct A rule: infinite_finite_induct) (simp_all add: pcompose_1 pcompose_mult)
lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]" by (induct p) (auto simp add: pcompose_pCons)
lemma pcompose_coeff_0: "coeff (pcompose p q) 0 = poly p (coeff q 0)" by (metis poly_0_coeff_0 poly_pcompose)
lemma pcompose_pCons_0: "pcompose p [:a:] = [:poly p a:]" by (metis (no_types, lifting) coeff_pCons_0 pcompose_0' pcompose_assoc poly_0_coeff_0 poly_pcompose)
lemma degree_pcompose: "degree (pcompose p q) = degree p * degree q" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof (induct p) case 0 thenshow ?caseby auto next case (pCons a p)
consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0" by blast thenshow ?case proof cases case prems: 1 show ?thesis proof (cases "p = 0") case True thenshow ?thesis by auto next case False from prems have"degree q = 0 ∨ pcompose p q = 0" by (auto simp add: degree_mult_eq_0) moreoverhave False if"pcompose p q = 0""degree q ≠ 0" proof - from pCons.hyps(2) that have"degree p = 0" by auto thenobtain a1 where"p = [:a1:]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) with‹pcompose p q = 0›‹p ≠ 0›show False by auto qed ultimatelyhave"degree (pCons a p) * degree q = 0" by auto moreoverhave"degree (pcompose (pCons a p) q) = 0" proof - from prems have"0 = max (degree [:a:]) (degree (q * pcompose p q))" by simp alsohave"…≥ degree ([:a:] + q * pcompose p q)" by (rule degree_add_le_max) finallyshow ?thesis by (auto simp add: pcompose_pCons) qed ultimatelyshow ?thesis by simp qed next case prems: 2 thenhave"p ≠ 0""q ≠ 0""pcompose p q ≠ 0" by auto from prems degree_add_eq_right [of "[:a:]"] have"degree (pcompose (pCons a p) q) = degree (q * pcompose p q)" by (auto simp: pcompose_pCons) with pCons.hyps(2) degree_mult_eq[OF ‹q≠0›‹pcompose p q≠0›] show ?thesis by auto qed qed
lemma pcompose_eq_0: fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" assumes"pcompose p q = 0""degree q > 0" shows"p = 0" proof - from assms degree_pcompose [of p q] have"degree p = 0" by auto thenobtain a where"p = [:a:]" by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases) with assms(1) have"a = 0" by auto with‹p = [:a:]›show ?thesis by simp qed
lemma pcompose_eq_0_iff: fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" assumes"degree q > 0" shows"pcompose p q = 0 ⟷ p = 0" using pcompose_eq_0[OF _ assms] by auto
lemma coeff_pcompose_linear: "coeff (pcompose p [:0, a :: 'a :: comm_semiring_1:]) i = a ^ i * coeff p i" by (induction p arbitrary: i) (auto simp: pcompose_pCons coeff_pCons mult_ac split: nat.splits)
lemma lead_coeff_comp: fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes"degree q > 0" shows"lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)" proof (induct p) case 0 thenshow ?caseby auto next case (pCons a p)
consider "degree (q * pcompose p q) = 0" | "degree (q * pcompose p q) > 0" by blast thenshow ?case proof cases case prems: 1 thenhave"pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv) with pcompose_eq_0[OF _ ‹degree q > 0›] have"p = 0" by simp thenshow ?thesis by auto next case prems: 2 thenhave"degree [:a:] < degree (q * pcompose p q)" by simp thenhave"lead_coeff ([:a:] + q * p ∘🪙p q) = lead_coeff (q * p ∘🪙p q)" by (rule lead_coeff_add_le) thenhave"lead_coeff (pcompose (pCons a p) q) = lead_coeff (q * pcompose p q)" by (simp add: pcompose_pCons) alsohave"… = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)" using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp alsohave"… = lead_coeff p * lead_coeff q ^ (degree p + 1)" by (auto simp: mult_ac) finallyshow ?thesis by auto qed qed
lemma coeff_pcompose_monom_linear [simp]: fixes p :: "'a :: comm_ring_1 poly" shows"coeff (pcompose p (monom c (Suc 0))) k = c ^ k * coeff p k" by (induction p arbitrary: k)
(auto simp: coeff_pCons coeff_monom_mult pcompose_pCons split: nat.splits)
lemma of_nat_mult_conv_smult: "of_nat n * P = smult (of_nat n) P" by (simp add: monom_0 of_nat_monom)
lemma numeral_mult_conv_smult: "numeral n * P = smult (numeral n) P" by (simp add: numeral_poly)
lemma sum_order_le_degree: assumes"p ≠ 0" shows"(∑x | poly p x = 0. order x p) ≤ degree p" using assms proof (induction"degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "∃x. poly p x = 0") case False thus ?thesis by auto next case True thenobtain x where x: "poly p x = 0" by auto have"[:-x, 1:] ^ order x p dvd p" by (simp add: order_1) thenobtain q where q: "p = [:-x, 1:] ^ order x p * q" by (elim dvdE) have [simp]: "q ≠ 0" using q less.prems by auto have"order x p = order x p + order x q" by (subst q, subst order_mult) (auto simp: order_power_n_n) hence"order x q = 0" by auto hence [simp]: "poly q x ≠ 0" by (simp add: order_root) have deg_p: "degree p = degree q + order x p" by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq) moreoverhave"order x p > 0" using x less.prems by (simp add: order_root) ultimatelyhave"degree q < degree p" by linarith hence"(∑x | poly q x = 0. order x q) ≤ degree q" by (intro less.hyps) auto hence"order x p + (∑x | poly q x = 0. order x q) ≤ degree p" by (simp add: deg_p) alsohave"{y. poly q y = 0} = {y. poly p y = 0} - {x}" by (subst q) auto alsohave"(∑y ∈ {y. poly p y = 0} - {x}. order y q) = (∑y ∈ {y. poly p y = 0} - {x}. order y p)" by (intro sum.cong refl, subst q)
(auto simp: order_mult order_power_n_n intro!: order_0I) alsohave"order x p + … = (∑y ∈ insert x ({y. poly p y = 0} - {x}). order y p)" using‹p ≠ 0›by (subst sum.insert) (auto simp: poly_roots_finite) alsohave"insert x ({y. poly p y = 0} - {x}) = {y. poly p y = 0}" using‹poly p x = 0›by auto finallyshow ?thesis . qed qed
subsection‹Closure properties of coefficients›
context fixes R :: "'a :: comm_semiring_1 set" assumes R_0: "0 ∈ R" assumes R_plus: "∧x y. x ∈ R ==> y ∈ R ==> x + y ∈ R" assumes R_mult: "∧x y. x ∈ R ==> y ∈ R ==> x * y ∈ R" begin
lemma coeff_mult_semiring_closed: assumes"∧i. coeff p i ∈ R""∧i. coeff q i ∈ R" shows"coeff (p * q) i ∈ R" proof - have R_sum: "sum f A ∈ R"if"∧x. x ∈ A ==> f x ∈ R"for A and f :: "nat ==> 'a" using that by (induction A rule: infinite_finite_induct) (auto intro: R_0 R_plus) show ?thesis unfolding coeff_mult by (auto intro!: R_sum R_mult assms) qed
lemma coeff_pcompose_semiring_closed: assumes"∧i. coeff p i ∈ R""∧i. coeff q i ∈ R" shows"coeff (pcompose p q) i ∈ R" using assms(1) proof (induction p arbitrary: i) case (pCons a p i) have [simp]: "a ∈ R" using pCons.prems[of 0] by auto have"coeff p i ∈ R"for i using pCons.prems[of "Suc i"] by auto hence"coeff (p ∘🪙p q) i ∈ R"for i using pCons.prems by (intro pCons.IH) thus ?case by (auto simp: pcompose_pCons coeff_pCons split: nat.splits
intro!: assms R_plus coeff_mult_semiring_closed) qed auto
end
subsection‹Shifting polynomials›
definition poly_shift :: "nat ==> 'a::zero poly ==> 'a poly" where"poly_shift n p = Abs_poly (λi. coeff p (i + n))"
lemma nth_default_drop: "nth_default x (drop n xs) m = nth_default x xs (m + n)" by (auto simp add: nth_default_def add_ac)
lemma nth_default_take: "nth_default x (take n xs) m = (if m < n then nth_default x xs m else x)" by (auto simp add: nth_default_def add_ac)
lemma coeff_poly_shift: "coeff (poly_shift n p) i = coeff p (i + n)" proof - from MOST_coeff_eq_0[of p] obtain m where"∀k>m. coeff p k = 0" by (auto simp: MOST_nat) thenhave"∀k>m. coeff p (k + n) = 0" by auto thenhave"∀🪙∞k. coeff p (k + n) = 0" by (auto simp: MOST_nat) thenshow ?thesis by (simp add: poly_shift_def poly.Abs_poly_inverse) qed
lemma poly_shift_0 [simp]: "poly_shift n 0 = 0" by (simp add: poly_eq_iff coeff_poly_shift)
lemma poly_shift_1: "poly_shift n 1 = (if n = 0 then 1 else 0)" by (simp add: poly_eq_iff coeff_poly_shift)
lemma poly_shift_monom: "poly_shift n (monom c m) = (if m ≥ n then monom c (m - n) else 0)" by (auto simp add: poly_eq_iff coeff_poly_shift)
lemma coeffs_shift_poly [code abstract]: "coeffs (poly_shift n p) = drop n (coeffs p)" proof (cases "p = 0") case True thenshow ?thesis by simp next case False thenshow ?thesis by (intro coeffs_eqI)
(simp_all add: coeff_poly_shift nth_default_drop nth_default_coeffs_eq) qed
subsection‹Truncating polynomials›
definition poly_cutoff where"poly_cutoff n p = Abs_poly (λk. if k < n then coeff p k else 0)"
lemma coeff_poly_cutoff: "coeff (poly_cutoff n p) k = (if k < n then coeff p k else 0)" unfolding poly_cutoff_def by (subst poly.Abs_poly_inverse) (auto simp: MOST_nat intro: exI[of _ n])
lemma poly_cutoff_0 [simp]: "poly_cutoff n 0 = 0" by (simp add: poly_eq_iff coeff_poly_cutoff)
lemma poly_cutoff_1 [simp]: "poly_cutoff n 1 = (if n = 0 then 0 else 1)" by (simp add: poly_eq_iff coeff_poly_cutoff)
lemma coeffs_poly_cutoff [code abstract]: "coeffs (poly_cutoff n p) = strip_while ((=) 0) (take n (coeffs p))" proof (cases "strip_while ((=) 0) (take n (coeffs p)) = []") case True thenhave"coeff (poly_cutoff n p) k = 0"for k unfolding coeff_poly_cutoff by (auto simp: nth_default_coeffs_eq [symmetric] nth_default_def set_conv_nth) thenhave"poly_cutoff n p = 0" by (simp add: poly_eq_iff) thenshow ?thesis by (subst True) simp_all next case False have"no_trailing ((=) 0) (strip_while ((=) 0) (take n (coeffs p)))" by simp with False have"last (strip_while ((=) 0) (take n (coeffs p))) ≠ 0" unfolding no_trailing_unfold by auto thenshow ?thesis by (intro coeffs_eqI)
(simp_all add: coeff_poly_cutoff nth_default_take nth_default_coeffs_eq) qed
subsection‹Reflecting polynomials›
definition reflect_poly :: "'a::zero poly ==> 'a poly" where"reflect_poly p = Poly (rev (coeffs p))"
lemma coeff_reflect_poly: "coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))" by (cases "p = 0")
(auto simp add: reflect_poly_def nth_default_def
rev_nth degree_eq_length_coeffs coeffs_nth not_less
dest: le_imp_less_Suc)
lemma coeff_0_reflect_poly_0_iff [simp]: "coeff (reflect_poly p) 0 = 0 ⟷ p = 0" by (simp add: coeff_reflect_poly)
lemma reflect_poly_at_0_eq_0_iff [simp]: "poly (reflect_poly p) 0 = 0 ⟷ p = 0" by (simp add: coeff_reflect_poly poly_0_coeff_0)
lemma reflect_poly_pCons': "p ≠ 0 ==> reflect_poly (pCons c p) = reflect_poly p + monom c (Suc (degree p))" by (intro poly_eqI)
(auto simp: coeff_reflect_poly coeff_pCons not_less Suc_diff_le split: nat.split)
lemma reflect_poly_const [simp]: "reflect_poly [:a:] = [:a:]" by (cases "a = 0") (simp_all add: reflect_poly_def)
lemma poly_reflect_poly_nz: "x ≠ 0 ==> poly (reflect_poly p) x = x ^ degree p * poly p (inverse x)" for x :: "'a::field" by (induct rule: pCons_induct) (simp_all add: field_simps reflect_poly_pCons' poly_monom)
lemma reflect_poly_pCons: "a ≠ 0 ==> reflect_poly (pCons a p) = Poly (rev (a # coeffs p))" by (subst coeffs_eq_iff) (simp add: coeffs_reflect_poly)
lemma degree_reflect_poly_eq [simp]: "coeff p 0 ≠ 0 ==> degree (reflect_poly p) = degree p" by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
lemma reflect_poly_eq_0_iff [simp]: "reflect_poly p = 0 ⟷ p = 0" using coeff_0_reflect_poly_0_iff by fastforce
(* TODO: does this work with zero divisors as well? Probably not. *) lemma reflect_poly_mult: "reflect_poly (p * q) = reflect_poly p * reflect_poly q" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof (cases "p = 0 ∨ q = 0") case False thenhave [simp]: "p ≠ 0""q ≠ 0"by auto show ?thesis proof (rule poly_eqI) show"coeff (reflect_poly (p * q)) i = coeff (reflect_poly p * reflect_poly q) i"for i proof (cases "i ≤ degree (p * q)") case True
define A where"A = {..i} ∩ {i - degree q..degree p}"
define B where"B = {..degree p} ∩ {degree p - i..degree (p*q) - i}" let ?f = "λj. degree p - j"
from True have"coeff (reflect_poly (p * q)) i = coeff (p * q) (degree (p * q) - i)" by (simp add: coeff_reflect_poly) alsohave"… = (∑j≤degree (p * q) - i. coeff p j * coeff q (degree (p * q) - i - j))" by (simp add: coeff_mult) alsohave"… = (∑j∈B. coeff p j * coeff q (degree (p * q) - i - j))" by (intro sum.mono_neutral_right) (auto simp: B_def degree_mult_eq not_le coeff_eq_0) alsofrom True have"… = (∑j∈A. coeff p (degree p - j) * coeff q (degree q - (i - j)))" by (intro sum.reindex_bij_witness[of _ ?f ?f])
(auto simp: A_def B_def degree_mult_eq add_ac) alsohave"… = (∑j≤i. if j ∈ {i - degree q..degree p} then coeff p (degree p - j) * coeff q (degree q - (i - j)) else 0)" by (subst sum.inter_restrict [symmetric]) (simp_all add: A_def) alsohave"… = coeff (reflect_poly p * reflect_poly q) i" by (fastforce simp: coeff_mult coeff_reflect_poly intro!: sum.cong) finallyshow ?thesis . qed (auto simp: coeff_mult coeff_reflect_poly coeff_eq_0 degree_mult_eq intro!: sum.neutral) qed qed auto
lemma reflect_poly_smult: "reflect_poly (smult c p) = smult c (reflect_poly p)" for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" using reflect_poly_mult[of "[:c:]" p] by simp
lemma reflect_poly_power: "reflect_poly (p ^ n) = reflect_poly p ^ n" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" by (induct n) (simp_all add: reflect_poly_mult)
lemma reflect_poly_prod: "reflect_poly (prod f A) = prod (λx. reflect_poly (f x)) A" for f :: "_ ==> _::{comm_semiring_0,semiring_no_zero_divisors} poly" by (induct A rule: infinite_finite_induct) (simp_all add: reflect_poly_mult)
function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly ==> 'a poly" where"pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))" by (auto intro: pCons_cases)
termination pderiv by (relation "measure degree") simp_all
declare pderiv.simps[simp del]
lemma pderiv_0 [simp]: "pderiv 0 = 0" using pderiv.simps [of 0 0] by simp
lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)" by (simp add: pderiv.simps)
lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0" and pderiv_numeral [simp]: "pderiv (numeral m) = 0" by (simp_all add: of_nat_poly numeral_poly pderiv_pCons)
lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" by (induct p arbitrary: n)
(auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
fun pderiv_coeffs_code :: "'a::{comm_semiring_1,semiring_no_zero_divisors} ==> 'a list ==> 'a list" where "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
| "pderiv_coeffs_code f [] = []"
definition pderiv_coeffs :: "'a::{comm_semiring_1,semiring_no_zero_divisors} list ==> 'a list" where"pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
(* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *) lemma pderiv_coeffs_code: "nth_default 0 (pderiv_coeffs_code f xs) n = (f + of_nat n) * nth_default 0 xs n" proof (induct xs arbitrary: f n) case Nil thenshow ?caseby simp next case (Cons x xs) show ?case proof (cases n) case 0 thenshow ?thesis by (cases "pderiv_coeffs_code (f + 1) xs = [] ∧ f * x = 0") (auto simp: cCons_def) next case n: (Suc m) show ?thesis proof (cases "pderiv_coeffs_code (f + 1) xs = [] ∧ f * x = 0") case False thenhave"nth_default 0 (pderiv_coeffs_code f (x # xs)) n = nth_default 0 (pderiv_coeffs_code (f + 1) xs) m" by (auto simp: cCons_def n) alsohave"… = (f + of_nat n) * nth_default 0 xs m" by (simp add: Cons n add_ac) finallyshow ?thesis by (simp add: n) next case True have empty: "pderiv_coeffs_code g xs = [] ==> g + of_nat m = 0 ∨ nth_default 0 xs m = 0"for g proof (induct xs arbitrary: g m) case Nil thenshow ?caseby simp next case (Cons x xs) from Cons(2) have empty: "pderiv_coeffs_code (g + 1) xs = []"and g: "g = 0 ∨ x = 0" by (auto simp: cCons_def split: if_splits) note IH = Cons(1)[OF empty] from IH[of m] IH[of "m - 1"] g show ?case by (cases m) (auto simp: field_simps) qed from True have"nth_default 0 (pderiv_coeffs_code f (x # xs)) n = 0" by (auto simp: cCons_def n) moreoverfrom True have"(f + of_nat n) * nth_default 0 (x # xs) n = 0" by (simp add: n) (use empty[of "f+1"] in‹auto simp: field_simps›) ultimatelyshow ?thesis by simp qed qed qed
lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)" unfolding pderiv_coeffs_def proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases) case (1 n) have id: "coeff p (Suc n) = nth_default 0 (map (λi. coeff p (Suc i)) [0.. by (cases "n < degree p") (auto simp: nth_default_def coeff_eq_0) show ?case unfolding coeffs_def map_upt_Suc by (auto simp: id) next case 2 obtain n :: 'a and xs wheredefs: "tl (coeffs p) = xs""1 = n" by simp from 2 show ?case unfoldingdefsby (induct xs arbitrary: n) (auto simp: cCons_def) qed
lemma pderiv_eq_0_iff: "pderiv p = 0 ⟷ degree p = 0" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" proof (cases "degree p") case 0 thenshow ?thesis by (metis degree_eq_zeroE pderiv.simps) next case (Suc n) thenshow ?thesis using coeff_0 coeff_pderiv degree_0 leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff by (metis coeff_0 coeff_pderiv degree_0 leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff) qed
lemma degree_pderiv: "degree (pderiv p) = degree p - 1" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" proof - have"degree p - 1 ≤ degree (pderiv p)" proof (cases "degree p") case (Suc n) thenshow ?thesis by (metis coeff_pderiv degree_0 diff_Suc_1 le_degree leading_coeff_0_iff mult_eq_0_iff nat.distinct(1) of_nat_eq_0_iff) qed auto moreoverhave"∀i>degree p - 1. coeff (pderiv p) i = 0" by (simp add: coeff_eq_0 coeff_pderiv) ultimatelyshow ?thesis using order_antisym [OF degree_le] by blast qed
lemma not_dvd_pderiv: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" assumes"degree p ≠ 0" shows"¬ p dvd pderiv p" proof assume dvd: "p dvd pderiv p" thenobtain q where p: "pderiv p = p * q" unfolding dvd_def by auto from dvd have le: "degree p ≤ degree (pderiv p)" by (simp add: assms dvd_imp_degree_le pderiv_eq_0_iff) from assms and this [unfolded degree_pderiv] show False by auto qed
lemma dvd_pderiv_iff [simp]: "p dvd pderiv p ⟷ degree p = 0" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" using not_dvd_pderiv[of p] by (auto simp: pderiv_eq_0_iff [symmetric])
lemma pderiv_monom: "pderiv (monom c n) = monom (of_nat n * c) (n - 1)" by (cases n)
(simp_all add: monom_altdef pderiv_power_Suc pderiv_smult pderiv_pCons mult_ac del: power_Suc)
lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q" by (induction p rule: pCons_induct)
(auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
lemma pderiv_prod: "pderiv (prod f (as)) = (∑a∈as. prod f (as - {a}) * pderiv (f a))" proof (induct as rule: infinite_finite_induct) case (insert a as) thenhave id: "prod f (insert a as) = f a * prod f as" "∧g. sum g (insert a as) = g a + sum g as" "insert a as - {a} = as" by auto have"prod f (insert a as - {b}) = f a * prod f (as - {b})"if"b ∈ as"for b proof - from‹a ∉ as› that have *: "insert a as - {b} = insert a (as - {b})" by auto show ?thesis unfolding * by (subst prod.insert) (use insert in auto) qed thenshow ?case unfolding id pderiv_mult insert(3) sum_distrib_left by (auto simp add: ac_simps intro!: sum.cong) qed auto
lemma coeff_higher_pderiv: "coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)" by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)
lemma higher_pderiv_add: "(pderiv ^^ n) (p + q) = (pderiv ^^ n) p + (pderiv ^^ n) q" by (induction n arbitrary: p q) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_add)
lemma higher_pderiv_smult: "(pderiv ^^ n) (smult c p) = smult c ((pderiv ^^ n) p)" by (induction n arbitrary: p) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_smult)
lemma higher_pderiv_monom: "m ≤ n + 1 ==> (pderiv ^^ m) (monom c n) = monom (pochhammer (int n - int m + 1) m * c) (n - m)" proof (induction m arbitrary: c n) case (Suc m) thus ?case by (cases n)
(simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH) qed simp_all
lemma higher_pderiv_monom_eq_zero: "m > n + 1 ==> (pderiv ^^ m) (monom c n) = 0" proof (induction m arbitrary: c n) case (Suc m) thus ?case by (cases n)
(simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH) qed simp_all
lemma higher_pderiv_sum: "(pderiv ^^ n) (sum f A) = (∑x∈A. (pderiv ^^ n) (f x))" by (induction A rule: infinite_finite_induct) (simp_all add: higher_pderiv_add)
lemma higher_pderiv_sum_mset: "(pderiv ^^ n) (sum_mset A) = (∑p∈#A. (pderiv ^^ n) p)" by (induction A) (simp_all add: higher_pderiv_add)
lemma degree_higher_pderiv: "Polynomial.degree ((pderiv ^^ n) p) = Polynomial.degree p - n" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors,semiring_char_0} poly" by (induction n) (auto simp: degree_pderiv)
lemma DERIV_pow2: "DERIV (λx. x ^ Suc n) x :> real (Suc n) * (x ^ n)" by (rule DERIV_cong, rule DERIV_pow) simp declare DERIV_pow2 [simp] DERIV_pow [simp]
lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (λx. a + f x :: 'a::real_normed_field) x :> D" by (rule DERIV_cong, rule DERIV_add) auto
lemma poly_DERIV [simp]: "DERIV (λx. poly p x) x :> poly (pderiv p) x" by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
lemma poly_isCont[simp]: fixes x::"'a::real_normed_field" shows"isCont (λx. poly p x) x" by (rule poly_DERIV [THEN DERIV_isCont])
lemma tendsto_poly [tendsto_intros]: "(f ---> a) F ==> ((λx. poly p (f x)) ---> poly p a) F" for f :: "_ ==> 'a::real_normed_field" by (rule isCont_tendsto_compose [OF poly_isCont])
lemma continuous_within_poly: "continuous (at z within s) (poly p)" for z :: "'a::{real_normed_field}" by (simp add: continuous_within tendsto_poly)
lemma continuous_poly [continuous_intros]: "continuous F f ==> continuous F (λx. poly p (f x))" for f :: "_ ==> 'a::real_normed_field" unfolding continuous_def by (rule tendsto_poly)
lemma continuous_on_poly [continuous_intros]: fixes p :: "'a :: {real_normed_field} poly" assumes"continuous_on A f" shows"continuous_on A (λx. poly p (f x))" by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
text‹Consequences of the derivative theorem above.›
lemma poly_differentiable[simp]: "(λx. poly p x) differentiable (at x)" for x :: real by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
lemma poly_IVT_pos: "a < b ==> poly p a < 0 ==> 0 < poly p b ==>∃x. a < x ∧ x < b ∧ poly p x = 0" for a b :: real using IVT [of "poly p" a 0 b] by (auto simp add: order_le_less)
lemma poly_IVT_neg: "a < b ==> 0 < poly p a ==> poly p b < 0 ==>∃x. a < x ∧ x < b ∧ poly p x = 0" for a b :: real using poly_IVT_pos [where p = "- p"] by simp
lemma poly_IVT: "a < b ==> poly p a * poly p b < 0 ==>∃x>a. x < b ∧ poly p x = 0" for p :: "real poly" by (metis less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
lemma poly_MVT: "a < b ==>∃x. a < x ∧ x < b ∧ poly p b - poly p a = (b - a) * poly (pderiv p) x" for a b :: real by (simp add: MVT2)
lemma poly_MVT': fixes a b :: real assumes"{min a b..max a b} ⊆ A" shows"∃x∈A. poly p b - poly p a = (b - a) * poly (pderiv p) x" proof (cases a b rule: linorder_cases) case less from poly_MVT[OF less, of p] obtain x where"a < x""x < b""poly p b - poly p a = (b - a) * poly (pderiv p) x" by auto thenshow ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms]) next case greater from poly_MVT[OF greater, of p] obtain x where"b < x""x < a""poly p a - poly p b = (a - b) * poly (pderiv p) x"by auto thenshow ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms]) qed (use assms in auto)
lemma poly_pinfty_gt_lc: fixes p :: "real poly" assumes"lead_coeff p > 0" shows"∃n. ∀ x ≥ n. poly p x ≥ lead_coeff p" using assms proof (induct p) case 0 thenshow ?caseby auto next case (pCons a p) from this(1) consider "a ≠ 0""p = 0" | "p ≠ 0"by auto thenshow ?case proof cases case 1 thenshow ?thesis by auto next case 2 with pCons obtain n1 where gte_lcoeff: "∀x≥n1. lead_coeff p ≤ poly p x" by auto from pCons(3) ‹p ≠ 0›have gt_0: "lead_coeff p > 0"by auto
define n where"n = max n1 (1 + ∣a∣ / lead_coeff p)" have"lead_coeff (pCons a p) ≤ poly (pCons a p) x"if"n ≤ x"for x proof - from gte_lcoeff that have"lead_coeff p ≤ poly p x" by (auto simp: n_def) with gt_0 have"∣a∣ / lead_coeff p ≥∣a∣ / poly p x"and"poly p x > 0" by (auto intro: frac_le) with‹n ≤ x›[unfolded n_def] have"x ≥ 1 + ∣a∣ / poly p x" by auto with‹lead_coeff p ≤ poly p x›‹poly p x > 0›‹p ≠ 0› show"lead_coeff (pCons a p) ≤ poly (pCons a p) x" by (auto simp: field_simps) qed thenshow ?thesis by blast qed qed
lemma dvd_monic: fixes p q:: "'a :: idom poly" assumes monic:"lead_coeff p=1"and"p dvd (smult c q)"and"c≠0" shows"p dvd q"using assms proof (cases "q=0 ∨ degree p=0") case True thus ?thesis using assms by (auto elim!: degree_eq_zeroE simp add: const_poly_dvd_iff) next case False hence"q≠0"and"degree p≠0"by auto obtain k where k:"smult c q = p*k"using assms dvd_def by metis hence"k≠0"by (metis False assms(3) mult_zero_right smult_eq_0_iff) hence deg_eq:"degree q=degree p + degree k" by (metis False assms(3) degree_0 degree_mult_eq degree_smult_eq k) have c_dvd:"∀n≤degree k. c dvd coeff k (degree k - n)" proof (rule,rule) fix n assume"n ≤ degree k " thus"c dvd coeff k (degree k - n)" proof (induct n rule:nat_less_induct) case (1 n)
define T where"T≡(λi. coeff p i * coeff k (degree p+degree k - n - i))" have"c * coeff q (degree q - n) = (∑i≤degree q - n. coeff p i * coeff k (degree q - n - i))" using coeff_mult[of p k "degree q - n"] k coeff_smult[of c q "degree q -n"] by auto alsohave"...=(∑i≤degree p+degree k - n. T i)" using deg_eq unfolding T_def by auto alsohave"...=(∑i∈{0.. sum T {degree p + 1..degree p + degree k - n}" proof -
define C where"C≡{{0.. have"∀A∈C. finite A"unfolding C_def by auto moreoverhave"∀A∈C. ∀B∈C. A ≠ B ⟶ A ∩ B = {}" unfolding C_def by auto ultimatelyhave"sum T (∪C) = sum (sum T) C" using sum.Union_disjoint by auto moreoverhave"∪C={..degree p + degree k - n}" using‹n ≤ degree k›unfolding C_def by auto moreoverhave"sum (sum T) C= sum T {0.. sum T {degree p + 1..degree p + degree k - n}" proof - have"{0..≠{degree p}" by (metis atLeast0LessThan insertI1 lessThan_iff less_imp_not_eq) moreoverhave"{degree p}≠{degree p + 1..degree p + degree k - n}" by (metis add.commute add_diff_cancel_right' atLeastAtMost_singleton_iff
diff_self_eq_0 eq_imp_le not_one_le_zero) moreoverhave"{0..≠{degree p + 1..degree p + degree k - n}" using‹degree k≥n›‹degree p≠0›by fastforce ultimatelyshow ?thesis unfolding C_def by auto qed ultimatelyshow ?thesis by auto qed alsohave"...=(∑i∈{0.. proof - have"∀x∈{degree p + 1..degree p + degree k - n}. T x=0" using coeff_eq_0[of p] unfolding T_def by simp hence"sum T {degree p + 1..degree p + degree k - n}=0"by auto moreoverhave"T (degree p)=coeff k (degree k - n)" using monic by (simp add: T_def) ultimatelyshow ?thesis by auto qed finallyhave c_coeff: "c * coeff q (degree q - n) = sum T {0.. + coeff k (degree k - n)" . moreoverhave"n≠0==>c dvd sum T {0.. proof (rule dvd_sum) fix i assume i:"i ∈ {0..and"n≠0" hence"(n+i-degree p)≤degree k"using‹n ≤ degree k›by auto moreoverhave"n + i - degree p using i ‹n≠0›by auto ultimatelyhave"c dvd coeff k (degree k - (n+i-degree p))" using 1(1) by auto hence"c dvd coeff k (degree p + degree k - n - i)" by (metis add_diff_cancel_left' deg_eq diff_diff_left dvd_0_right le_degree
le_diff_conv add.commute ordered_cancel_comm_monoid_diff_class.diff_diff_right) thus"c dvd T i"unfolding T_def by auto qed moreoverhave"n=0 ==>?case" proof - assume"n=0" hence"∀i∈{0.. using coeff_eq_0[of k] by simp hence"c * coeff q (degree q - n) = coeff k (degree k - n)" using c_coeff unfolding T_def by auto thus ?thesis by (metis dvdI) qed ultimatelyshow ?caseby (metis dvd_add_right_iff dvd_triv_left) qed qed hence"∀n. c dvd coeff k n" by (metis diff_diff_cancel dvd_0_right le_add2 le_add_diff_inverse le_degree) thenobtain f where f:"∀n. c * f n=coeff k n"unfolding dvd_def by metis have" ∀🪙∞ n. f n = 0 " by (metis (mono_tags, lifting) MOST_coeff_eq_0 MOST_mono assms(3) f mult_eq_0_iff) hence"smult c (Abs_poly f)=k" using f smult.abs_eq[of c "Abs_poly f"] Abs_poly_inverse[of f] coeff_inverse[of k] by simp hence"q=p* Abs_poly f"using k ‹c≠0› smult_cancel by auto thus ?thesis unfolding dvd_def by auto qed
lemma lemma_order_pderiv1: "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" unfolding pderiv_mult pderiv_power_Suc by (simp del: power_Suc of_nat_Suc add: pderiv_pCons)
lemma order_pderiv: fixes p::"'a::{idom,semiring_char_0} poly" assumes"p≠0""poly p x = 0" shows"order x p = Suc (order x (pderiv p))"using assms proof -
define xx op where"xx=[:- x, 1:]"and"op = order x p" have"op ≠ 0"unfolding op_def using assms order_root by blast obtain pp where pp:"p = xx ^ op * pp""¬ xx dvd pp" using order_decomp[OF ‹p≠0›,of x,folded xx_def op_def] by auto have p_der:"pderiv p = smult (of_nat op) (xx^(op -1)) * pp + xx^op*pderiv pp" unfolding pp(1) by (auto simp:pderiv_mult pderiv_power xx_def algebra_simps pderiv_pCons) have"xx^(op -1) dvd (pderiv p)" unfolding p_der by (metis ‹op ≠ 0› dvd_add_left_iff dvd_mult2 dvd_refl dvd_smult dvd_triv_right
power_eq_if) moreoverhave"¬ xx^op dvd (pderiv p)" proof assume"xx ^ op dvd pderiv p" thenhave"xx ^ op dvd smult (of_nat op) (xx^(op -1) * pp)" unfolding p_der by (simp add: dvd_add_left_iff) thenhave"xx ^ op dvd (xx^(op -1)) * pp" apply (elim dvd_monic[rotated]) using‹op≠0›by (auto simp:lead_coeff_power xx_def) thenhave"xx ^ (op-1) * xx dvd (xx^(op -1))" using‹¬ xx dvd pp›by (simp add: ‹op ≠ 0› mult.commute power_eq_if) thenhave"xx dvd 1" using assms(1) pp(1) by auto thenshow False unfolding xx_def by (meson assms(1) dvd_trans one_dvd order_decomp) qed ultimatelyhave"op - 1 = order x (pderiv p)" using order_unique_lemma[of x "op-1""pderiv p",folded xx_def] ‹op≠0› by auto thenshow ?thesis using‹op≠0›unfolding op_def by auto qed
lemma lemma_order_pderiv: fixes p :: "'a :: field_char_0 poly" assumes n: "0 < n" and pd: "pderiv p ≠ 0" and pe: "p = [:- a, 1:] ^ n * q" and nd: "¬ [:- a, 1:] dvd q" shows"n = Suc (order a (pderiv p))" by (metis add.right_neutral gr0_conv_Suc n nat.case nd order_mult order_pderiv
order_power_n_n order_root pd pderiv_0 pe poly_eq_0_iff_dvd)
lemma poly_squarefree_decomp_order: fixes p :: "'a::field_char_0 poly" assumes"pderiv p ≠ 0" and p: "p = q * d" and p': "pderiv p = e * d" and d: "d = r * p + s * pderiv p" shows"order a q = (if order a p = 0 then 0 else 1)" proof (rule classical) assume 1: "¬ ?thesis" from‹pderiv p ≠ 0›have"p ≠ 0"by auto with p have"order a p = order a q + order a d" by (simp add: order_mult) with 1 have"order a p ≠ 0" by (auto split: if_splits) from‹pderiv p ≠ 0›‹pderiv p = e * d›have oapp: "order a (pderiv p) = order a e + order a d" by (simp add: order_mult) from‹pderiv p ≠ 0›‹order a p ≠ 0›have oap: "order a p = Suc (order a (pderiv p))" using‹p ≠ 0› order_pderiv order_root by blast from‹p ≠ 0›‹p = q * d›have"d ≠ 0" by simp have"[:- a, 1:] ^ order a (pderiv p) dvd r * p" by (metis dvd_trans dvd_triv_right oap order_1 power_Suc) thenhave"([:-a, 1:] ^ (order a (pderiv p))) dvd d" by (simp add: d order_1) with‹d ≠ 0›have"order a (pderiv p) ≤ order a d" by (simp add: order_divides) show ?thesis using‹order a p = order a q + order a d› and oapp oap and‹order a (pderiv p) ≤ order a d› by auto qed
lemma poly_squarefree_decomp_order2: "pderiv p ≠ 0 ==> p = q * d ==> pderiv p = e * d ==> d = r * p + s * pderiv p ==>∀a. order a q = (if order a p = 0 then 0 else 1)" for p :: "'a::field_char_0 poly" by (blast intro: poly_squarefree_decomp_order)
lemma order_pderiv2: "pderiv p ≠ 0 ==> order a p ≠ 0 ==> order a (pderiv p) = n ⟷ order a p = Suc n" for p :: "'a::field_char_0 poly" by (metis nat.inject order_pderiv order_root pderiv_0)
definition rsquarefree :: "'a::idom poly ==> bool" where"rsquarefree p ⟷ p ≠ 0 ∧ (∀a. order a p = 0 ∨ order a p = 1)"
lemma pderiv_iszero: "pderiv p = 0 ==>∃h. p = [:h:]" for p :: "'a::{semidom,semiring_char_0} poly" by (cases p) (auto simp: pderiv_eq_0_iff split: if_splits)
lemma rsquarefree_roots: "rsquarefree p ⟷ (∀a. ¬ (poly p a = 0 ∧ poly (pderiv p) a = 0))" for p :: "'a::field_char_0 poly" proof (cases "p = 0") case False show ?thesis proof (cases "pderiv p = 0") case True with‹p ≠ 0› pderiv_iszero show ?thesis by (force simp add: order_0I rsquarefree_def) next case False with‹p ≠ 0› order_pderiv2 show ?thesis by (force simp add: rsquarefree_def order_root) qed qed (simp add: rsquarefree_def)
lemma rsquarefree_root_order: assumes"rsquarefree p""poly p z = 0""p ≠ 0" shows"order z p = 1" proof - from assms have"order z p ∈ {0, 1}"by (auto simp: rsquarefree_def) moreoverfrom assms have"order z p > 0"by (auto simp: order_root) ultimatelyshow"order z p = 1"by auto qed
lemma poly_squarefree_decomp: fixes p :: "'a::field_char_0 poly" assumes"pderiv p ≠ 0" and"p = q * d" and"pderiv p = e * d" and"d = r * p + s * pderiv p" shows"rsquarefree q ∧ (∀a. poly q a = 0 ⟷ poly p a = 0)" proof - from‹pderiv p ≠ 0›have"p ≠ 0"by auto with‹p = q * d›have"q ≠ 0"by simp from assms have"∀a. order a q = (if order a p = 0 then 0 else 1)" by (rule poly_squarefree_decomp_order2) with‹p ≠ 0›‹q ≠ 0›show ?thesis by (simp add: rsquarefree_def order_root) qed
lemma has_field_derivative_poly [derivative_intros]: assumes"(f has_field_derivative f') (at x within A)" shows"((λx. poly p (f x)) has_field_derivative (f' * poly (pderiv p) (f x))) (at x within A)" using DERIV_chain[OF poly_DERIV assms, of p] by (simp add: o_def mult_ac)
subsection‹Algebraic numbers›
lemma intpolyE: assumes"∧i. poly.coeff p i ∈ℤ" obtains q where"p = map_poly of_int q" proof - have"∀i∈{..Polynomial.degree p}. ∃x. poly.coeff p i = of_int x" using assms by (auto simp: Ints_def) from bchoice[OF this] obtain f where f: "∧i. i ≤ Polynomial.degree p ==> poly.coeff p i = of_int (f i)"by blast
define q where"q = Poly (map f [0.. have"p = map_poly of_int q" by (intro poly_eqI)
(auto simp: coeff_map_poly q_def nth_default_def f coeff_eq_0 simp del: upt_Suc) with that show ?thesis by blast qed
lemma ratpolyE: assumes"∧i. poly.coeff p i ∈ℚ" obtains q where"p = map_poly of_rat q" proof - have"∀i∈{..Polynomial.degree p}. ∃x. poly.coeff p i = of_rat x" using assms by (auto simp: Rats_def) from bchoice[OF this] obtain f where f: "∧i. i ≤ Polynomial.degree p ==> poly.coeff p i = of_rat (f i)"by blast
define q where"q = Poly (map f [0.. have"p = map_poly of_rat q" by (intro poly_eqI)
(auto simp: coeff_map_poly q_def nth_default_def f coeff_eq_0 simp del: upt_Suc) with that show ?thesis by blast qed
text‹ Algebraic numbers can be defined in two equivalent ways: all real numbers that are roots of rational polynomials or of integer polynomials. The Algebraic-Numbers AFP entry uses the rational definition, but we need the integer definition. The equivalence is obvious since any rational polynomial can be multiplied with the LCM of its coefficients, yielding an integer polynomial with the same roots. ›
definition algebraic :: "'a :: field_char_0 ==> bool" where"algebraic x ⟷ (∃p. (∀i. coeff p i ∈ℤ) ∧ p ≠ 0 ∧ poly p x = 0)"
lemma algebraicI: "(∧i. coeff p i ∈ℤ) ==> p ≠ 0 ==> poly p x = 0 ==> algebraic x" unfolding algebraic_def by blast
lemma algebraicE: assumes"algebraic x" obtains p where"∧i. coeff p i ∈ℤ""p ≠ 0""poly p x = 0" using assms unfolding algebraic_def by blast
lemma algebraic_altdef: "algebraic x ⟷ (∃p. (∀i. coeff p i ∈ℚ) ∧ p ≠ 0 ∧ poly p x = 0)" for p :: "'a::field_char_0 poly" proof safe fix p assume rat: "∀i. coeff p i ∈ℚ"and root: "poly p x = 0"and nz: "p ≠ 0"
define cs where"cs = coeffs p" from rat have"∀c∈range (coeff p). ∃c'. c = of_rat c'" unfolding Rats_def by blast thenobtain f where f: "coeff p i = of_rat (f (coeff p i))"for i by (subst (asm) bchoice_iff) blast
define cs' where"cs' = map (quotient_of ∘ f) (coeffs p)"
define d where"d = Lcm (set (map snd cs'))"
define p' where"p' = smult (of_int d) p"
have"coeff p' n ∈ℤ"for n proof (cases "n ≤ degree p") case True
define c where"c = coeff p n"
define a where"a = fst (quotient_of (f (coeff p n)))"
define b where"b = snd (quotient_of (f (coeff p n)))" have b_pos: "b > 0" unfolding b_def using quotient_of_denom_pos' by simp have"coeff p' n = of_int d * coeff p n" by (simp add: p'_def) alsohave"coeff p n = of_rat (of_int a / of_int b)" unfolding a_def b_def by (subst quotient_of_div [of "f (coeff p n)", symmetric]) (simp_all add: f [symmetric]) alsohave"of_int d * … = of_rat (of_int (a*d) / of_int b)" by (simp add: of_rat_mult of_rat_divide) alsofrom nz True have"b ∈ snd ` set cs'" by (force simp: cs'_def o_def b_def coeffs_def simp del: upt_Suc) thenhave"b dvd (a * d)" by (simp add: d_def) thenhave"of_int (a * d) / of_int b ∈ (ℤ :: rat set)" by (rule of_int_divide_in_Ints) thenhave"of_rat (of_int (a * d) / of_int b) ∈ℤ"by (elim Ints_cases) auto finallyshow ?thesis . next case False thenshow ?thesis by (auto simp: p'_def not_le coeff_eq_0) qed moreoverhave"set (map snd cs') ⊆ {0<..}" unfolding cs'_defusing quotient_of_denom_pos' by (auto simp: coeffs_def simp del: upt_Suc) thenhave"d ≠ 0" unfolding d_def by (induct cs') simp_all with nz have"p' ≠ 0"by (simp add: p'_def) moreoverfrom root have"poly p' x = 0" by (simp add: p'_def) ultimatelyshow"algebraic x" unfolding algebraic_def by blast next assume"algebraic x" thenobtain p where p: "coeff p i ∈ℤ""poly p x = 0""p ≠ 0"for i by (force simp: algebraic_def) moreoverhave"coeff p i ∈ℤ==> coeff p i ∈ℚ"for i by (elim Ints_cases) simp ultimatelyshow"∃p. (∀i. coeff p i ∈ℚ) ∧ p ≠ 0 ∧ poly p x = 0"by auto qed
lemma algebraicI': "(∧i. coeff p i ∈ℚ) ==> p ≠ 0 ==> poly p x = 0 ==> algebraic x" unfolding algebraic_altdef by blast
lemma algebraicE': assumes"algebraic (x :: 'a :: field_char_0)" obtains p where"p ≠ 0""poly (map_poly of_int p) x = 0" proof - from assms obtain q where q: "∧i. coeff q i ∈ℤ""q ≠ 0""poly q x = 0" by (erule algebraicE) moreoverfrom this(1) obtain q' where q': "q = map_poly of_int q'"by (erule intpolyE) moreoverhave"q' ≠ 0" using q' q by auto ultimatelyshow ?thesis by (intro that[of q']) simp_all qed
lemma algebraicE'_nonzero: assumes"algebraic (x :: 'a :: field_char_0)""x ≠ 0" obtains p where"p ≠ 0""coeff p 0 ≠ 0""poly (map_poly of_int p) x = 0" proof - from assms(1) obtain p where p: "p ≠ 0""poly (map_poly of_int p) x = 0" by (erule algebraicE')
define n :: nat where"n = order 0 p" have"monom 1 n dvd p"by (simp add: monom_1_dvd_iff p n_def) thenobtain q where q: "p = monom 1 n * q"by (erule dvdE) have [simp]: "map_poly of_int (monom 1 n * q) = monom (1 :: 'a) n * map_poly of_int q" by (induction n) (auto simp: monom_0 monom_Suc map_poly_pCons) from p have"q ≠ 0""poly (map_poly of_int q) x = 0"by (auto simp: q poly_monom assms(2)) moreoverfrom this have"order 0 p = n + order 0 q"by (simp add: q order_mult) hence"order 0 q = 0"by (simp add: n_def) with‹q ≠ 0›have"poly q 0 ≠ 0"by (simp add: order_root) ultimatelyshow ?thesis using that[of q] by (auto simp: poly_0_coeff_0) qed
lemma rat_imp_algebraic: "x ∈ℚ==> algebraic x" proof (rule algebraicI') show"poly [:-x, 1:] x = 0" by simp qed (auto simp: coeff_pCons split: nat.splits)
lemma algebraic_0 [simp, intro]: "algebraic 0" and algebraic_1 [simp, intro]: "algebraic 1" and algebraic_numeral [simp, intro]: "algebraic (numeral n)" and algebraic_of_nat [simp, intro]: "algebraic (of_nat k)" and algebraic_of_int [simp, intro]: "algebraic (of_int m)" by (simp_all add: rat_imp_algebraic)
lemma algebraic_ii [simp, intro]: "algebraic i" proof (rule algebraicI) show"poly [:1, 0, 1:] i = 0" by simp qed (auto simp: coeff_pCons split: nat.splits)
lemma algebraic_minus [intro]: assumes"algebraic x" shows"algebraic (-x)" proof - from assms obtain p where p: "∀i. coeff p i ∈ℤ""poly p x = 0""p ≠ 0" by (elim algebraicE) auto
define s where"s = (if even (degree p) then 1 else -1 :: 'a)"
define q where"q = Polynomial.smult s (pcompose p [:0, -1:])" have"poly q (-x) = 0" using p by (auto simp: q_def poly_pcompose s_def) moreoverhave"q ≠ 0" using p by (auto simp: q_def s_def pcompose_eq_0_iff) find_theorems"pcompose _ _ = 0" moreoverhave"coeff q i ∈ℤ"for i proof - have"coeff (pcompose p [:0, -1:]) i ∈ℤ" using p by (intro coeff_pcompose_semiring_closed) (auto simp: coeff_pCons split: nat.splits) thus ?thesis by (simp add: q_def s_def) qed ultimatelyshow ?thesis by (auto simp: algebraic_def) qed
lemma algebraic_minus_iff [simp]: "algebraic (-x) ⟷ algebraic (x :: 'a :: field_char_0)" using algebraic_minus[of x] algebraic_minus[of "-x"] by auto
lemma algebraic_inverse [intro]: assumes"algebraic x" shows"algebraic (inverse x)" proof (cases "x = 0") case [simp]: False from assms obtain p where p: "∀i. coeff p i ∈ℤ""poly p x = 0""p ≠ 0" by (elim algebraicE) auto show ?thesis proof (rule algebraicI) show"poly (reflect_poly p) (inverse x) = 0" using assms p by (simp add: poly_reflect_poly_nz) qed (use assms p in‹auto simp: coeff_reflect_poly›) qed auto
lemma algebraic_root: assumes"algebraic y" and"poly p x = y"and"∀i. coeff p i ∈ℤ"and"lead_coeff p = 1"and"degree p > 0" shows"algebraic x" proof - from assms obtain q where q: "poly q y = 0""∀i. coeff q i ∈ℤ""q ≠ 0" by (elim algebraicE) auto show ?thesis proof (rule algebraicI) from assms q show"pcompose q p ≠ 0" by (auto simp: pcompose_eq_0_iff) from assms q show"coeff (pcompose q p) i ∈ℤ"for i by (intro allI coeff_pcompose_semiring_closed) auto show"poly (pcompose q p) x = 0" using assms q by (simp add: poly_pcompose) qed qed
lemma algebraic_nth_root_real [intro]: assumes"algebraic x" shows"algebraic (root n x)" proof (cases "n = 0") case False show ?thesis proof (rule algebraic_root) show"poly (monom 1 n) (root n x) = (if even n then ∣x∣ else x)" using sgn_power_root[of n x] False by (auto simp add: poly_monom sgn_if split: if_splits) qed (use False assms in‹auto simp: degree_monom_eq›) qed auto
lemma algebraic_sqrt [intro]: "algebraic x ==> algebraic (sqrt x)" by (auto simp: sqrt_def)
lemma algebraic_csqrt [intro]: "algebraic x ==> algebraic (csqrt x)" by (rule algebraic_root[where p = "monom 1 2"])
(auto simp: poly_monom degree_monom_eq)
lemma algebraic_cnj [intro]: assumes"algebraic x" shows"algebraic (cnj x)" proof - from assms obtain p where p: "poly p x = 0""∀i. coeff p i ∈ℤ""p ≠ 0" by (elim algebraicE) auto show ?thesis proof (rule algebraicI) show"poly (map_poly cnj p) (cnj x) = 0" using p by simp show"map_poly cnj p ≠ 0" using p by (auto simp: map_poly_eq_0_iff) show"coeff (map_poly cnj p) i ∈ℤ"for i using p by (auto simp: coeff_map_poly) qed qed
lemma algebraic_cnj_iff [simp]: "algebraic (cnj x) ⟷ algebraic x" using algebraic_cnj[of x] algebraic_cnj[of "cnj x"] by auto
lemma algebraic_of_real [intro]: assumes"algebraic x" shows"algebraic (of_real x)" proof - from assms obtain p where p: "p ≠ 0""poly (map_poly of_int p) x = 0"by (erule algebraicE') have 1: "map_poly of_int p ≠ (0 :: 'a poly)" using p by (metis coeff_0 coeff_map_poly leading_coeff_0_iff of_int_eq_0_iff)
have"poly (map_poly of_int p) (of_real x :: 'a) = of_real (poly (map_poly of_int p) x)" by (simp add: poly_altdef degree_map_poly coeff_map_poly) alsonote p(2) finallyhave 2: "poly (map_poly of_int p) (of_real x :: 'a) = 0" by simp
from 1 2 show"algebraic (of_real x :: 'a)" by (intro algebraicI[of "map_poly of_int p"]) (auto simp: coeff_map_poly) qed
lemma algebraic_of_real_iff [simp]: "algebraic (of_real x :: 'a :: {real_algebra_1,field_char_0}) ⟷ algebraic x" proof assume"algebraic (of_real x :: 'a)" thenobtain p where p: "p ≠ 0""poly (map_poly of_int p) (of_real x :: 'a) = 0" by (erule algebraicE') have 1: "(map_poly of_int p :: real poly) ≠ 0" using p by (metis coeff_0 coeff_map_poly leading_coeff_0_iff of_int_0 of_int_eq_iff)
note p(2) alsohave"poly (map_poly of_int p) (of_real x :: 'a) = of_real (poly (map_poly of_int p) x)" by (simp add: poly_altdef degree_map_poly coeff_map_poly) alsohave"… = 0 ⟷ poly (map_poly of_int p) x = 0" using of_real_eq_0_iff by blast finallyhave 2: "poly (map_poly real_of_int p) x = 0" .
from 1 and 2 show"algebraic x" by (intro algebraicI[of "map_poly of_int p"]) (auto simp: coeff_map_poly) qed auto
subsection‹Algebraic integers›
inductive algebraic_int :: "'a :: field ==> bool"where "[lead_coeff p = 1; ∀i. coeff p i ∈ℤ; poly p x = 0]==> algebraic_int x"
lemma algebraic_int_altdef_ipoly: fixes x :: "'a :: field_char_0" shows"algebraic_int x ⟷ (∃p. poly (map_poly of_int p) x = 0 ∧ lead_coeff p = 1)" proof assume"algebraic_int x" thenobtain p where p: "lead_coeff p = 1""∀i. coeff p i ∈ℤ""poly p x = 0" by (auto elim: algebraic_int.cases)
define the_int where"the_int = (λx::'a. THE r. x = of_int r)"
define p' where"p' = map_poly the_int p" have of_int_the_int: "of_int (the_int x) = x"if"x ∈ℤ"for x unfolding the_int_def by (rule sym, rule theI') (insert that, auto simp: Ints_def) have the_int_0_iff: "the_int x = 0 ⟷ x = 0"if"x ∈ℤ"for x using of_int_the_int[OF that] by auto have [simp]: "the_int 0 = 0" by (subst the_int_0_iff) auto have"map_poly of_int p' = map_poly (of_int ∘ the_int) p" by (simp add: p'_def map_poly_map_poly) alsofrom p of_int_the_int have"… = p" by (subst poly_eq_iff) (auto simp: coeff_map_poly) finallyhave p_p': "map_poly of_int p' = p" .
show"(∃p. poly (map_poly of_int p) x = 0 ∧ lead_coeff p = 1)" proof (intro exI conjI notI) from p show"poly (map_poly of_int p') x = 0"by (simp add: p_p') next show"lead_coeff p' = 1" using p by (simp flip: p_p' add: degree_map_poly coeff_map_poly) qed next assume"∃p. poly (map_poly of_int p) x = 0 ∧ lead_coeff p = 1" thenobtain p where p: "poly (map_poly of_int p) x = 0""lead_coeff p = 1" by auto
define p' where"p' = (map_poly of_int p :: 'a poly)" from p have"lead_coeff p' = 1""poly p' x = 0""∀i. coeff p' i ∈ℤ" by (auto simp: p'_def coeff_map_poly degree_map_poly) thus"algebraic_int x" by (intro algebraic_int.intros) qed
theorem rational_algebraic_int_is_int: assumes"algebraic_int x"and"x ∈ℚ" shows"x ∈ℤ" proof - from assms(2) obtain a b where ab: "b > 0""Rings.coprime a b"and x_eq: "x = of_int a / of_int b" by (auto elim: Rats_cases') from‹b > 0›have [simp]: "b ≠ 0" by auto from assms(1) obtain p where p: "lead_coeff p = 1""∀i. coeff p i ∈ℤ""poly p x = 0" by (auto simp: algebraic_int.simps)
define q :: "'a poly"where"q = [:-of_int a, of_int b:]" have"poly q x = 0""q ≠ 0""∀i. coeff q i ∈ℤ" by (auto simp: x_eq q_def coeff_pCons split: nat.splits)
define n where"n = degree p" have"n > 0" using p by (intro Nat.gr0I) (auto simp: n_def elim!: degree_eq_zeroE) have"(∑i∈ℤ" using p by auto thenobtain R where R: "of_int R = (∑i by (auto simp: Ints_def) have [simp]: "coeff p n = 1" using p by (auto simp: n_def)
have"0 = poly p x * of_int b ^ n" using p by simp alsohave"… = (∑i≤n. coeff p i * x ^ i * of_int b ^ n)" by (simp add: poly_altdef n_def sum_distrib_right) alsohave"… = (∑i≤n. coeff p i * of_int (a ^ i * b ^ (n - i)))" by (intro sum.cong) (auto simp: x_eq field_simps simp flip: power_add) alsohave"{..n} = insert n {.. using‹n > 0›by auto alsohave"(∑i∈…. coeff p i * of_int (a ^ i * b ^ (n - i))) = coeff p n * of_int (a ^ n) + (∑i by (subst sum.insert) auto alsohave"(∑i (∑i by (intro sum.cong) (auto simp flip: power_add power_Suc simp: Suc_diff_Suc) alsohave"… = of_int (b * R)" by (simp add: R sum_distrib_left sum_distrib_right mult_ac) finallyhave"of_int (a ^ n) = (-of_int (b * R) :: 'a)" by (auto simp: add_eq_0_iff) hence"a ^ n = -b * R" by (simp flip: of_int_mult of_int_power of_int_minus) hence"b dvd a ^ n" by simp with‹Rings.coprime a b›have"b dvd 1" by (meson coprime_power_left_iff dvd_refl not_coprimeI) with x_eq and‹b > 0›show ?thesis by auto qed
lemma algebraic_int_imp_algebraic [dest]: "algebraic_int x ==> algebraic x" by (auto simp: algebraic_int.simps algebraic_def)
lemma int_imp_algebraic_int: assumes"x ∈ℤ" shows"algebraic_int x" proof show"∀i. coeff [:-x, 1:] i ∈ℤ" using assms by (auto simp: coeff_pCons split: nat.splits) qed auto
lemma algebraic_int_0 [simp, intro]: "algebraic_int 0" and algebraic_int_1 [simp, intro]: "algebraic_int 1" and algebraic_int_numeral [simp, intro]: "algebraic_int (numeral n)" and algebraic_int_of_nat [simp, intro]: "algebraic_int (of_nat k)" and algebraic_int_of_int [simp, intro]: "algebraic_int (of_int m)" by (simp_all add: int_imp_algebraic_int)
lemma algebraic_int_ii [simp, intro]: "algebraic_int i" proof show"poly [:1, 0, 1:] i = 0" by simp qed (auto simp: coeff_pCons split: nat.splits)
lemma algebraic_int_minus [intro]: assumes"algebraic_int x" shows"algebraic_int (-x)" proof - from assms obtain p where p: "lead_coeff p = 1""∀i. coeff p i ∈ℤ""poly p x = 0" by (auto simp: algebraic_int.simps)
define s where"s = (if even (degree p) then 1 else -1 :: 'a)"
define q where"q = Polynomial.smult s (pcompose p [:0, -1:])" have"lead_coeff q = s * lead_coeff (pcompose p [:0, -1:])" by (simp add: q_def) alsohave"lead_coeff (pcompose p [:0, -1:]) = lead_coeff p * (- 1) ^ degree p" by (subst lead_coeff_comp) auto finallyhave"poly q (-x) = 0"and"lead_coeff q = 1" using p by (auto simp: q_def poly_pcompose s_def) moreoverhave"coeff q i ∈ℤ"for i proof - have"coeff (pcompose p [:0, -1:]) i ∈ℤ" using p by (intro coeff_pcompose_semiring_closed) (auto simp: coeff_pCons split: nat.splits) thus ?thesis by (simp add: q_def s_def) qed ultimatelyshow ?thesis by (auto simp: algebraic_int.simps) qed
lemma algebraic_int_minus_iff [simp]: "algebraic_int (-x) ⟷ algebraic_int (x :: 'a :: field_char_0)" using algebraic_int_minus[of x] algebraic_int_minus[of "-x"] by auto
lemma algebraic_int_inverse [intro]: assumes"poly p x = 0"and"∀i. coeff p i ∈ℤ"and"coeff p 0 = 1" shows"algebraic_int (inverse x)" proof from assms have [simp]: "x ≠ 0" by (auto simp: poly_0_coeff_0) show"poly (reflect_poly p) (inverse x) = 0" using assms by (simp add: poly_reflect_poly_nz) qed (use assms in‹auto simp: coeff_reflect_poly›)
lemma algebraic_int_root: assumes"algebraic_int y" and"poly p x = y"and"∀i. coeff p i ∈ℤ"and"lead_coeff p = 1"and"degree p > 0" shows"algebraic_int x" proof - from assms obtain q where q: "poly q y = 0""∀i. coeff q i ∈ℤ""lead_coeff q = 1" by (auto simp: algebraic_int.simps) show ?thesis proof from assms q show"lead_coeff (pcompose q p) = 1" by (subst lead_coeff_comp) auto from assms q show"∀i. coeff (pcompose q p) i ∈ℤ" by (intro allI coeff_pcompose_semiring_closed) auto show"poly (pcompose q p) x = 0" using assms q by (simp add: poly_pcompose) qed qed
lemma algebraic_int_nth_root_real [intro]: assumes"algebraic_int x" shows"algebraic_int (root n x)" proof (cases "n = 0") case False show ?thesis proof (rule algebraic_int_root) show"poly (monom 1 n) (root n x) = (if even n then ∣x∣ else x)" using sgn_power_root[of n x] False by (auto simp add: poly_monom sgn_if split: if_splits) qed (use False assms in‹auto simp: degree_monom_eq›) qed auto
lemma algebraic_int_sqrt [intro]: "algebraic_int x ==> algebraic_int (sqrt x)" by (auto simp: sqrt_def)
lemma algebraic_int_csqrt [intro]: "algebraic_int x ==> algebraic_int (csqrt x)" by (rule algebraic_int_root[where p = "monom 1 2"])
(auto simp: poly_monom degree_monom_eq)
lemma algebraic_int_cnj [intro]: assumes"algebraic_int x" shows"algebraic_int (cnj x)" proof - from assms obtain p where p: "lead_coeff p = 1""∀i. coeff p i ∈ℤ""poly p x = 0" by (auto simp: algebraic_int.simps) show ?thesis proof show"poly (map_poly cnj p) (cnj x) = 0" using p by simp show"lead_coeff (map_poly cnj p) = 1" using p by (simp add: coeff_map_poly degree_map_poly) show"∀i. coeff (map_poly cnj p) i ∈ℤ" using p by (auto simp: coeff_map_poly) qed qed
lemma algebraic_int_cnj_iff [simp]: "algebraic_int (cnj x) ⟷ algebraic_int x" using algebraic_int_cnj[of x] algebraic_int_cnj[of "cnj x"] by auto
lemma algebraic_int_of_real [intro]: assumes"algebraic_int x" shows"algebraic_int (of_real x)" proof - from assms obtain p where p: "poly p x = 0""∀i. coeff p i ∈ℤ""lead_coeff p = 1" by (auto simp: algebraic_int.simps) show"algebraic_int (of_real x :: 'a)" proof have"poly (map_poly of_real p) (of_real x) = (of_real (poly p x) :: 'a)" by (induction p) (auto simp: map_poly_pCons) thus"poly (map_poly of_real p) (of_real x) = (0 :: 'a)" using p by simp qed (use p in‹auto simp: coeff_map_poly degree_map_poly›) qed
lemma algebraic_int_of_real_iff [simp]: "algebraic_int (of_real x :: 'a :: {field_char_0, real_algebra_1}) ⟷ algebraic_int x" proof assume"algebraic_int (of_real x :: 'a)" thenobtain p where p: "poly (map_poly of_int p) (of_real x :: 'a) = 0""lead_coeff p = 1" by (auto simp: algebraic_int_altdef_ipoly) show"algebraic_int x" unfolding algebraic_int_altdef_ipoly proof (intro exI[of _ p] conjI) have"of_real (poly (map_poly real_of_int p) x) = poly (map_poly of_int p) (of_real x :: 'a)" by (induction p) (auto simp: map_poly_pCons) alsonote p(1) finallyshow"poly (map_poly real_of_int p) x = 0"by simp qed (use p in auto) qed auto
subsection‹Division of polynomials›
subsubsection ‹Division in general›
instantiation poly :: (idom_divide) idom_divide begin
fun divide_poly_main :: "'a ==> 'a poly ==> 'a poly ==> 'a poly ==> nat ==> nat ==> 'a poly" where "divide_poly_main lc q r d dr (Suc n) = (let cr = coeff r dr; a = cr div lc; mon = monom a n in if False ∨ a * lc = cr then 🍋‹‹False ∨› is only because of problem in function-package› divide_poly_main lc (q + mon) (r - mon * d) d (dr - 1) n else 0)"
| "divide_poly_main lc q r d dr 0 = q"
definition divide_poly :: "'a poly ==> 'a poly ==> 'a poly" where"divide_poly f g = (if g = 0 then 0 else divide_poly_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)))"
lemma divide_poly_main: assumes d: "d ≠ 0""lc = coeff d (degree d)" and"degree (d * r) ≤ dr""divide_poly_main lc q (d * r) d dr n = q'" and"n = 1 + dr - degree d ∨ dr = 0 ∧ n = 0 ∧ d * r = 0" shows"q' = q + r" using assms(3-) proof (induct n arbitrary: q r dr) case (Suc n) let ?rr = "d * r" let ?a = "coeff ?rr dr" let ?qq = "?a div lc"
define b where [simp]: "b = monom ?qq n" let ?rrr = "d * (r - b)" let ?qqq = "q + b" note res = Suc(3) from Suc(4) have dr: "dr = n + degree d"by auto from d have lc: "lc ≠ 0"by auto have"coeff (b * d) dr = coeff b n * coeff d (degree d)" proof (cases "?qq = 0") case True thenshow ?thesis by simp next case False thenhave n: "n = degree b" by (simp add: degree_monom_eq) show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum) qed alsohave"… = lc * coeff b n" by (simp add: d) finallyhave c2: "coeff (b * d) dr = lc * coeff b n" . have rrr: "?rrr = ?rr - b * d" by (simp add: field_simps) have c1: "coeff (d * r) dr = lc * coeff r n" proof (cases "degree r = n") case True with Suc(2) show ?thesis unfolding dr using coeff_mult_degree_sum[of d r] d by (auto simp: ac_simps) next case False from dr Suc(2) have"degree r ≤ n" by auto
(metis add.commute add_le_cancel_left d(1) degree_0 degree_mult_eq
diff_is_0_eq diff_zero le_cases) with False have r_n: "degree r < n" by auto thenhave right: "lc * coeff r n = 0" by (simp add: coeff_eq_0) have"coeff (d * r) dr = coeff (d * r) (degree d + n)" by (simp add: dr ac_simps) alsofrom r_n have"… = 0" by (metis False Suc.prems(1) add.commute add_left_imp_eq coeff_degree_mult coeff_eq_0
coeff_mult_degree_sum degree_mult_le dr le_eq_less_or_eq) finallyshow ?thesis by (simp only: right) qed have c0: "coeff ?rrr dr = 0" and id: "lc * (coeff (d * r) dr div lc) = coeff (d * r) dr" unfolding rrr coeff_diff c2 unfolding b_def coeff_monom coeff_smult c1 using lc by auto from res[unfolded divide_poly_main.simps[of lc q] Let_def] id have res: "divide_poly_main lc ?qqq ?rrr d (dr - 1) n = q'" by (simp del: divide_poly_main.simps add: field_simps) note IH = Suc(1)[OF _ res] from Suc(4) have dr: "dr = n + degree d"by auto from Suc(2) have deg_rr: "degree ?rr ≤ dr"by auto have deg_bd: "degree (b * d) ≤ dr" unfolding dr b_def by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le) have"degree ?rrr ≤ dr" unfolding rrr by (rule degree_diff_le[OF deg_rr deg_bd]) with c0 have deg_rrr: "degree ?rrr ≤ (dr - 1)" by (rule coeff_0_degree_minus_1) have"n = 1 + (dr - 1) - degree d ∨ dr - 1 = 0 ∧ n = 0 ∧ ?rrr = 0" proof (cases dr) case 0 with Suc(4) have 0: "dr = 0""n = 0""degree d = 0" by auto with deg_rrr have"degree ?rrr = 0" by simp from degree_eq_zeroE[OF this] obtain a where rrr: "?rrr = [:a:]" by metis show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp next case _: Suc with Suc(4) show ?thesis by auto qed from IH[OF deg_rrr this] show ?case by simp next case 0 show ?case proof (cases "r = 0") case True with 0 show ?thesis by auto next case False from d False have"degree (d * r) = degree d + degree r" by (subst degree_mult_eq) auto with 0 d show ?thesis by auto qed qed
lemma divide_poly_main_0: "divide_poly_main 0 0 r d dr n = 0" proof (induct n arbitrary: r d dr) case 0 thenshow ?caseby simp next case Suc show ?case unfolding divide_poly_main.simps[of _ _ r] Let_def by (simp add: Suc del: divide_poly_main.simps) qed
lemma divide_poly: assumes g: "g ≠ 0" shows"(f * g) div g = (f :: 'a poly)" proof - have len: "length (coeffs f) = Suc (degree f)"if"f ≠ 0"for f :: "'a poly" using that unfolding degree_eq_length_coeffs by auto have"divide_poly_main (coeff g (degree g)) 0 (g * f) g (degree (g * f)) (1 + length (coeffs (g * f)) - length (coeffs g)) = (f * g) div g" by (simp add: divide_poly_def Let_def ac_simps) note main = divide_poly_main[OF g refl le_refl this] have"(f * g) div g = 0 + f" proof (rule main, goal_cases) case 1 show ?case proof (cases "f = 0") case True with g show ?thesis by (auto simp: degree_eq_length_coeffs) next case False with g have fg: "g * f ≠ 0"by auto show ?thesis unfolding len[OF fg] len[OF g] by auto qed qed thenshow ?thesis by simp qed
lemma divide_poly_0: "f div 0 = 0" for f :: "'a poly" by (simp add: divide_poly_def Let_def divide_poly_main_0)
instance by standard (auto simp: divide_poly divide_poly_0)
lemma div_const_poly_conv_map_poly: assumes"[:c:] dvd p" shows"p div [:c:] = map_poly (λx. x div c) p" proof (cases "c = 0") case True thenshow ?thesis by (auto intro!: poly_eqI simp: coeff_map_poly) next case False from assms obtain q where p: "p = [:c:] * q"by (rule dvdE) moreover { have"smult c q = [:c:] * q" by simp alsohave"… div [:c:] = q" by (rule nonzero_mult_div_cancel_left) (use False in auto) finallyhave"smult c q div [:c:] = q" .
} ultimatelyshow ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False) qed
lemma is_unit_monom_0: fixes a :: "'a::field" assumes"a ≠ 0" shows"is_unit (monom a 0)" proof from assms show"1 = monom a 0 * monom (inverse a) 0" by (simp add: mult_monom) qed
lemma is_unit_triv: "a ≠ 0 ==> is_unit [:a:]" for a :: "'a::field" by (simp add: is_unit_monom_0 monom_0 [symmetric])
lemma is_unit_iff_degree: fixes p :: "'a::field poly" assumes"p ≠ 0" shows"is_unit p ⟷ degree p = 0"
(is"?lhs ⟷ ?rhs") proof assume ?rhs thenobtain a where"p = [:a:]" by (rule degree_eq_zeroE) with assms show ?lhs by (simp add: is_unit_triv) next assume ?lhs thenobtain q where"q ≠ 0""p * q = 1" .. thenhave"degree (p * q) = degree 1" by simp with‹p ≠ 0›‹q ≠ 0›have"degree p + degree q = 0" by (simp add: degree_mult_eq) thenshow ?rhs by simp qed
lemma is_unit_pCons_iff: "is_unit (pCons a p) ⟷ p = 0 ∧ a ≠ 0" for p :: "'a::field poly" by (cases "p = 0") (auto simp: is_unit_triv is_unit_iff_degree)
lemma is_unit_monom_trivial: "is_unit p ==> monom (coeff p (degree p)) 0 = p" for p :: "'a::field poly" by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
lemma is_unit_const_poly_iff: "[:c:] dvd 1 ⟷ c dvd 1" for c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}" by (auto simp: one_pCons)
lemma is_unit_polyE: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes"p dvd 1" obtains c where"p = [:c:]""c dvd 1" proof - from assms obtain q where"1 = p * q" by (rule dvdE) thenhave"p ≠ 0"and"q ≠ 0" by auto from‹1 = p * q›have"degree 1 = degree (p * q)" by simp alsofrom‹p ≠ 0›and‹q ≠ 0›have"… = degree p + degree q" by (simp add: degree_mult_eq) finallyhave"degree p = 0"by simp with degree_eq_zeroE obtain c where c: "p = [:c:]" . with‹p dvd 1›have"c dvd 1" by (simp add: is_unit_const_poly_iff) with c show thesis .. qed
lemma is_unit_polyE': fixes p :: "'a::field poly" assumes"is_unit p" obtains a where"p = monom a 0"and"a ≠ 0" proof - obtain a q where"p = pCons a q" by (cases p) with assms have"p = [:a:]"and"a ≠ 0" by (simp_all add: is_unit_pCons_iff) with that show thesis by (simp add: monom_0) qed
lemma is_unit_poly_iff: "p dvd 1 ⟷ (∃c. p = [:c:] ∧ c dvd 1)" for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
lemma coprime_poly_0: "poly p x ≠ 0 ∨ poly q x ≠ 0"if"coprime p q" for x :: "'a :: field" proof (rule ccontr) assume" ¬ (poly p x ≠ 0 ∨ poly q x ≠ 0)" thenhave"[:-x, 1:] dvd p""[:-x, 1:] dvd q" by (simp_all add: poly_eq_0_iff_dvd) with that have"is_unit [:-x, 1:]" by (rule coprime_common_divisor) thenshow False by (auto simp add: is_unit_pCons_iff) qed
lemma root_imp_reducible_poly: fixes x :: "'a :: field" assumes"poly p x = 0"and"degree p > 1" shows"¬irreducible p" proof - from assms have"p ≠ 0" by auto
define q where"q = [:-x, 1:]" have"q dvd p" using assms by (simp add: poly_eq_0_iff_dvd q_def) thenobtain r where p_eq: "p = q * r" by (elim dvdE) have [simp]: "q ≠ 0""r ≠ 0" using‹p ≠ 0›by (auto simp: p_eq) have"degree p = Suc (degree r)" unfolding p_eq by (subst degree_mult_eq) (auto simp: q_def) with assms(2) have"degree r > 0" by auto hence"¬r dvd 1" by (auto simp: is_unit_poly_iff) moreoverhave"¬q dvd 1" by (auto simp: is_unit_poly_iff q_def) ultimatelyshow ?thesis using p_eq by (auto simp: irreducible_def) qed
lemma reducible_polyI: fixes p :: "'a :: field poly" assumes"p = q * r""degree q > 0""degree r > 0" shows"¬irreducible p" using assms unfolding irreducible_def by (metis (no_types, opaque_lifting) is_unitE is_unit_iff_degree not_gr0)
subsubsection ‹Pseudo-Division›
text‹This part is by René Thiemann and Akihisa Yamada.›
fun pseudo_divmod_main :: "'a :: comm_ring_1 ==> 'a poly ==> 'a poly ==> 'a poly ==> nat ==> nat ==> 'a poly × 'a poly" where "pseudo_divmod_main lc q r d dr (Suc n) = (let rr = smult lc r; qq = coeff r dr; rrr = rr - monom qq n * d; qqq = smult lc q + monom qq n in pseudo_divmod_main lc qqq rrr d (dr - 1) n)"
| "pseudo_divmod_main lc q r d dr 0 = (q,r)"
definition pseudo_divmod :: "'a :: comm_ring_1 poly ==> 'a poly ==> 'a poly × 'a poly" where"pseudo_divmod p q ≡ if q = 0 then (0, p) else pseudo_divmod_main (coeff q (degree q)) 0 p q (degree p) (1 + length (coeffs p) - length (coeffs q))"
lemma pseudo_divmod_main: assumes d: "d ≠ 0""lc = coeff d (degree d)" and"degree r ≤ dr""pseudo_divmod_main lc q r d dr n = (q',r')" and"n = 1 + dr - degree d ∨ dr = 0 ∧ n = 0 ∧ r = 0" shows"(r' = 0 ∨ degree r' < degree d) ∧ smult (lc^n) (d * q + r) = d * q' + r'" using assms(3-) proof (induct n arbitrary: q r dr) case 0 thenshow ?caseby auto next case (Suc n) let ?rr = "smult lc r" let ?qq = "coeff r dr"
define b where [simp]: "b = monom ?qq n" let ?rrr = "?rr - b * d" let ?qqq = "smult lc q + b" note res = Suc(3) from res[unfolded pseudo_divmod_main.simps[of lc q] Let_def] have res: "pseudo_divmod_main lc ?qqq ?rrr d (dr - 1) n = (q',r')" by (simp del: pseudo_divmod_main.simps) from Suc(4) have dr: "dr = n + degree d"by auto have"coeff (b * d) dr = coeff b n * coeff d (degree d)" proof (cases "?qq = 0") case True thenshow ?thesis by auto next case False thenhave n: "n = degree b" by (simp add: degree_monom_eq) show ?thesis unfolding n dr by (simp add: coeff_mult_degree_sum) qed alsohave"… = lc * coeff b n"by (simp add: d) finallyhave"coeff (b * d) dr = lc * coeff b n" . moreoverhave"coeff ?rr dr = lc * coeff r dr" by simp ultimatelyhave c0: "coeff ?rrr dr = 0" by auto from Suc(4) have dr: "dr = n + degree d"by auto have deg_rr: "degree ?rr ≤ dr" using Suc(2) degree_smult_le dual_order.trans by blast have deg_bd: "degree (b * d) ≤ dr" unfolding dr by (rule order.trans[OF degree_mult_le]) (auto simp: degree_monom_le) have"degree ?rrr ≤ dr" using degree_diff_le[OF deg_rr deg_bd] by auto with c0 have deg_rrr: "degree ?rrr ≤ (dr - 1)" by (rule coeff_0_degree_minus_1) have"n = 1 + (dr - 1) - degree d ∨ dr - 1 = 0 ∧ n = 0 ∧ ?rrr = 0" proof (cases dr) case 0 with Suc(4) have 0: "dr = 0""n = 0""degree d = 0"by auto with deg_rrr have"degree ?rrr = 0"by simp thenhave"∃a. ?rrr = [:a:]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) from this obtain a where rrr: "?rrr = [:a:]" by auto show ?thesis unfolding 0 using c0 unfolding rrr 0 by simp next case _: Suc with Suc(4) show ?thesis by auto qed note IH = Suc(1)[OF deg_rrr res this] show ?case proof (intro conjI) from IH show"r' = 0 ∨ degree r' < degree d" by blast show"smult (lc ^ Suc n) (d * q + r) = d * q' + r'" unfolding IH[THEN conjunct2,symmetric] by (simp add: field_simps smult_add_right) qed qed
lemma pseudo_divmod: assumes g: "g ≠ 0" and *: "pseudo_divmod f g = (q,r)" shows"smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" (is?A) and"r = 0 ∨ degree r < degree g" (is ?B) proof - from *[unfolded pseudo_divmod_def Let_def] have"pseudo_divmod_main (coeff g (degree g)) 0 f g (degree f) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (auto simp: g) note main = pseudo_divmod_main[OF _ _ _ this, OF g refl le_refl] from g have"1 + length (coeffs f) - length (coeffs g) = 1 + degree f - degree g ∨ degree f = 0 ∧ 1 + length (coeffs f) - length (coeffs g) = 0 ∧ f = 0" by (cases "f = 0"; cases "coeffs g") (auto simp: degree_eq_length_coeffs) note main' = main[OF this] thenshow"r = 0 ∨ degree r < degree g"by auto show"smult (coeff g (degree g) ^ (Suc (degree f) - degree g)) f = g * q + r" by (subst main'[THEN conjunct2, symmetric], simp add: degree_eq_length_coeffs,
cases "f = 0"; cases "coeffs g", use g in auto) qed
definition"pseudo_mod_main lc r d dr n = snd (pseudo_divmod_main lc 0 r d dr n)"
lemma snd_pseudo_divmod_main: "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)" by (induct n arbitrary: q q' lc r d dr) (simp_all add: Let_def)
definition pseudo_mod :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly ==> 'a poly ==> 'a poly" where"pseudo_mod f g = snd (pseudo_divmod f g)"
lemma pseudo_mod: fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly" defines"r ≡ pseudo_mod f g" assumes g: "g ≠ 0" shows"∃a q. a ≠ 0 ∧ smult a f = g * q + r""r = 0 ∨ degree r < degree g" proof - let ?cg = "coeff g (degree g)" let ?cge = "?cg ^ (Suc (degree f) - degree g)"
define a where"a = ?cge" from r_def[unfolded pseudo_mod_def] obtain q where pdm: "pseudo_divmod f g = (q, r)" by (cases "pseudo_divmod f g") auto from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r"and"r = 0 ∨ degree r < degree g" by (auto simp: a_def) show"r = 0 ∨ degree r < degree g"by fact from g have"a ≠ 0" by (auto simp: a_def) with id show"∃a q. a ≠ 0 ∧ smult a f = g * q + r" by auto qed
lemma fst_pseudo_divmod_main_as_divide_poly_main: assumes d: "d ≠ 0" defines lc: "lc ≡ coeff d (degree d)" shows"fst (pseudo_divmod_main lc q r d dr n) = divide_poly_main lc (smult (lc^n) q) (smult (lc^n) r) d dr n" proof (induct n arbitrary: q r dr) case 0 thenshow ?caseby simp next case (Suc n) note lc0 = leading_coeff_neq_0[OF d, folded lc] thenhave"pseudo_divmod_main lc q r d dr (Suc n) = pseudo_divmod_main lc (smult lc q + monom (coeff r dr) n) (smult lc r - monom (coeff r dr) n * d) d (dr - 1) n" by (simp add: Let_def ac_simps) alsohave"fst … = divide_poly_main lc (smult (lc^n) (smult lc q + monom (coeff r dr) n)) (smult (lc^n) (smult lc r - monom (coeff r dr) n * d)) d (dr - 1) n" by (simp only: Suc[unfolded divide_poly_main.simps Let_def]) alsohave"… = divide_poly_main lc (smult (lc ^ Suc n) q) (smult (lc ^ Suc n) r) d dr (Suc n)" unfolding smult_monom smult_distribs mult_smult_left[symmetric] using lc0 by (simp add: Let_def ac_simps) finallyshow ?case . qed
subsubsection ‹Division in polynomials over fields›
lemma pseudo_divmod_field: fixes g :: "'a::field poly" assumes g: "g ≠ 0" and *: "pseudo_divmod f g = (q,r)" defines"c ≡ coeff g (degree g) ^ (Suc (degree f) - degree g)" shows"f = g * smult (1/c) q + smult (1/c) r" proof - from leading_coeff_neq_0[OF g] have c0: "c ≠ 0" by (auto simp: c_def) from pseudo_divmod(1)[OF g *, folded c_def] have"smult c f = g * q + r" by auto alsohave"smult (1 / c) … = g * smult (1 / c) q + smult (1 / c) r" by (simp add: smult_add_right) finallyshow ?thesis using c0 by auto qed
lemma divide_poly_main_field: fixes d :: "'a::field poly" assumes d: "d ≠ 0" defines lc: "lc ≡ coeff d (degree d)" shows"divide_poly_main lc q r d dr n = fst (pseudo_divmod_main lc (smult ((1 / lc)^n) q) (smult ((1 / lc)^n) r) d dr n)" unfolding lc by (subst fst_pseudo_divmod_main_as_divide_poly_main) (auto simp: d power_one_over)
lemma divide_poly_field: fixes f g :: "'a::field poly" defines"f' ≡ smult ((1 / coeff g (degree g)) ^ (Suc (degree f) - degree g)) f" shows"f div g = fst (pseudo_divmod f' g)" proof (cases "g = 0") case True show ?thesis unfolding divide_poly_def pseudo_divmod_def Let_def f'_def True by (simp add: divide_poly_main_0) next case False from leading_coeff_neq_0[OF False] have"degree f' = degree f" by (auto simp: f'_def) thenshow ?thesis using length_coeffs_degree[of f'] length_coeffs_degree[of f] unfolding divide_poly_def pseudo_divmod_def Let_def
divide_poly_main_field[OF False]
length_coeffs_degree[OF False]
f'_def by force qed
instantiation poly :: ("{semidom_divide_unit_factor,idom_divide}") normalization_semidom begin
definition unit_factor_poly :: "'a poly ==> 'a poly" where"unit_factor_poly p = [:unit_factor (lead_coeff p):]"
definition normalize_poly :: "'a poly ==> 'a poly" where"normalize p = p div [:unit_factor (lead_coeff p):]"
instance proof fix p :: "'a poly" show"unit_factor p * normalize p = p" proof (cases "p = 0") case True thenshow ?thesis by (simp add: unit_factor_poly_def normalize_poly_def) next case False thenhave"lead_coeff p ≠ 0" by simp thenhave *: "unit_factor (lead_coeff p) ≠ 0" using unit_factor_is_unit [of "lead_coeff p"] by auto thenhave"unit_factor (lead_coeff p) dvd 1" by (auto intro: unit_factor_is_unit) thenhave **: "unit_factor (lead_coeff p) dvd c"for c by (rule dvd_trans) simp have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c"forc proof - from ** obtain b where"c = unit_factor (lead_coeff p) * b" .. with False * show ?thesis by simp qed have"p div [:unit_factor (lead_coeff p):] = map_poly (λc. c div unit_factor (lead_coeff p)) p" by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **) thenshow ?thesis by (simp add: normalize_poly_def unit_factor_poly_def
smult_conv_map_poly map_poly_map_poly o_def ***) qed next fix p :: "'a poly" assume"is_unit p" thenobtain c where p: "p = [:c:]""c dvd 1" by (auto simp: is_unit_poly_iff) thenshow"unit_factor p = p" by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor) next fix p :: "'a poly" assume"p ≠ 0" thenshow"is_unit (unit_factor p)" by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit) next fix a b :: "'a poly"assume"is_unit a" thus"unit_factor (a * b) = a * unit_factor b" by (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult elim!: is_unit_polyE) qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
lemma normalize_poly_eq_map_poly: "normalize p = map_poly (λx. x div unit_factor (lead_coeff p)) p" proof - have"[:unit_factor (lead_coeff p):] dvd p" by (metis unit_factor_poly_def unit_factor_self) thenshow ?thesis by (simp add: normalize_poly_def div_const_poly_conv_map_poly) qed
lemma coeff_normalize [simp]: "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)" by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
class field_unit_factor = field + unit_factor + assumes unit_factor_field [simp]: "unit_factor = id" begin
subclass semidom_divide_unit_factor proof fix a assume"a ≠ 0" thenhave"1 = a * inverse a"by simp thenhave"a dvd 1" .. thenshow"unit_factor a dvd 1"by simp qed simp_all
end
lemma unit_factor_pCons: "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)" by (simp add: unit_factor_poly_def)
lemma normalize_monom [simp]: "normalize (monom a n) = monom (normalize a) n" by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
lemma unit_factor_monom [simp]: "unit_factor (monom a n) = [:unit_factor a:]" by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
lemma normalize_smult: fixes c :: "'a :: {normalization_semidom_multiplicative, idom_divide}" shows"normalize (smult c p) = smult (normalize c) (normalize p)" proof - have"smult c p = [:c:] * p"by simp alsohave"normalize … = smult (normalize c) (normalize p)" by (subst normalize_mult) (simp add: normalize_const_poly) finallyshow ?thesis . qed
instantiation poly :: (field) idom_modulo begin
definition modulo_poly :: "'a poly ==> 'a poly ==> 'a poly" where mod_poly_def: "f mod g = (if g = 0 then f else pseudo_mod (smult ((1 / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g)"
instance proof fix x y :: "'a poly" show"x div y * y + x mod y = x" proof (cases "y = 0") case True thenshow ?thesis by (simp add: divide_poly_0 mod_poly_def) next case False thenhave"pseudo_divmod (smult ((1 / lead_coeff y) ^ (Suc (degree x) - degree y)) x) y = (x div y, x mod y)" by (simp add: divide_poly_field mod_poly_def pseudo_mod_def) with False pseudo_divmod [OF False this] show ?thesis by (simp add: power_mult_distrib [symmetric] ac_simps) qed qed
end
lemma pseudo_divmod_eq_div_mod: ‹pseudo_divmod f g = (f div g, f mod g)›if‹lead_coeff g = 1› using that by (auto simp add: divide_poly_field mod_poly_def pseudo_mod_def)
lemma degree_mod_less_degree: ‹degree (x mod y) 🚫 y›if‹y ≠ 0›‹¬ y dvd x› proof - from pseudo_mod(2) [of y] ‹y ≠ 0› have *: ‹pseudo_mod f y ≠ 0 ==> degree (pseudo_mod f y) 🚫 y›for f by blast from‹¬ y dvd x›have‹x mod y ≠ 0› by blast with‹y ≠ 0›show ?thesis by (auto simp add: mod_poly_def intro: *) qed
instantiation poly :: (field) unique_euclidean_ring begin
definition euclidean_size_poly :: "'a poly ==> nat" where"euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
definition division_segment_poly :: "'a poly ==> 'a poly" where [simp]: "division_segment_poly p = 1"
instanceproof show‹(q * p + r) div p = q›if‹p ≠ 0› and‹euclidean_size r 🚫 p›for q p r :: ‹'a poly› proof (cases ‹r = 0›) case True with that show ?thesis by simp next case False with‹p ≠ 0›‹euclidean_size r 🚫 p› have‹degree r 🚫 p› by (simp add: euclidean_size_poly_def) with‹r ≠ 0›have‹¬ p dvd r› by (auto dest: dvd_imp_degree) have‹(q * p + r) div p = q ∧ (q * p + r) mod p = r› proof (rule ccontr) assume‹¬ ?thesis› moreoverhave *: ‹((q * p + r) div p - q) * p = r - (q * p + r) mod p› by (simp add: algebra_simps) ultimatelyhave‹(q * p + r) div p ≠ q›and‹(q * p + r) mod p ≠ r› using‹p ≠ 0›by auto from‹¬ p dvd r›have‹¬ p dvd (q * p + r)› by simp with‹p ≠ 0›have‹degree ((q * p + r) mod p) 🚫 p› by (rule degree_mod_less_degree) with‹degree r 🚫 p›‹(q * p + r) mod p ≠ r› have‹degree (r - (q * p + r) mod p) 🚫 p› by (auto intro: degree_diff_less) alsohave‹degree p ≤ degree ((q * p + r) div p - q) + degree p› by simp alsofrom‹(q * p + r) div p ≠ q›‹p ≠ 0› have‹… = degree (((q * p + r) div p - q) * p)› by (simp add: degree_mult_eq) alsofrom * have‹… = degree (r - (q * p + r) mod p)› by simp finallyhave‹degree (r - (q * p + r) mod p) 🚫 (r - (q * p + r) mod p)› . thenshow False by simp qed thenshow‹(q * p + r) div p = q› .. qed qed (auto simp: euclidean_size_poly_def degree_mult_eq power_add intro: degree_mod_less_degree)
end
lemma euclidean_relation_polyI [case_names by0 divides euclidean_relation]: ‹(x div y, x mod y) = (q, r)› if by0: ‹y = 0 ==> q = 0 ∧ r = x› and divides: ‹y ≠ 0 ==> y dvd x ==> r = 0 ∧ x = q * y› and euclidean_relation: ‹y ≠ 0 ==>¬ y dvd x ==> degree r 🚫 y ∧ x = q * y + r› by (rule euclidean_relationI)
(use that in‹simp_all add: euclidean_size_poly_def›)
lemma div_poly_eq_0_iff: ‹x div y = 0 ⟷ x = 0 ∨ y = 0 ∨ degree x 🚫 y›for x y :: ‹'a::field poly› by (simp add: unique_euclidean_semiring_class.div_eq_0_iff euclidean_size_poly_def)
lemma div_poly_less: ‹x div y = 0›if‹degree x 🚫 y›for x y :: ‹'a::field poly› using that by (simp add: div_poly_eq_0_iff)
lemma mod_poly_less: ‹x mod y = x›if‹degree x 🚫 y› using that by (simp add: mod_eq_self_iff_div_eq_0 div_poly_eq_0_iff)
lemma degree_div_less: ‹degree (x div y) 🚫 x› if‹degree x > 0›‹degree y > 0› for x y :: ‹'a::field poly› proof (cases ‹x div y = 0›) case True with‹degree x > 0›show ?thesis by simp next case False from that have‹x ≠ 0›‹y ≠ 0› and *: ‹degree (x div y * y + x mod y) > 0› by auto show ?thesis proof (cases ‹y dvd x›) case True thenobtain z where‹x = y * z› .. thenhave‹degree (x div y) 🚫 (x div y * y)› using‹y ≠ 0›‹x ≠ 0›‹degree y > 0›by (simp add: degree_mult_eq) with‹y dvd x›show ?thesis by simp next case False with‹y ≠ 0›have‹degree (x mod y) 🚫 y› by (rule degree_mod_less_degree) with‹y ≠ 0›‹x div y ≠ 0›have‹degree (x mod y) 🚫 (x div y * y)› by (simp add: degree_mult_eq) thenhave‹degree (x div y * y + x mod y) = degree (x div y * y)› by (rule degree_add_eq_left) with‹y ≠ 0›‹x div y ≠ 0›‹degree y > 0›show ?thesis by (simp add: degree_mult_eq) qed qed
lemma degree_mod_less': "b ≠ 0 ==> a mod b ≠ 0 ==> degree (a mod b) < degree b" by (rule degree_mod_less_degree) auto
lemma degree_mod_less: "y ≠ 0 ==> x mod y = 0 ∨ degree (x mod y) < degree y" using degree_mod_less' by blast
lemma div_smult_left: ‹smult a x div y = smult a (x div y)› (is ?Q) and mod_smult_left: ‹smult a x mod y = smult a (x mod y)› (is ?R) for x y :: ‹'a::field poly› proof - have‹(smult a x div y, smult a x mod y) = (smult a (x div y), smult a (x mod y))› proof (cases ‹a = 0›) case True thenshow ?thesis by simp next case False show ?thesis by (rule euclidean_relation_polyI)
(use False in‹simp_all add: dvd_smult_iff degree_mod_less_degree flip: smult_add_right›) qed thenshow ?Q and ?R by simp_all qed
lemma poly_div_minus_left [simp]: "(- x) div y = - (x div y)" for x y :: "'a::field poly" using div_smult_left [of "- 1::'a"] by simp
lemma poly_mod_minus_left [simp]: "(- x) mod y = - (x mod y)" for x y :: "'a::field poly" using mod_smult_left [of "- 1::'a"] by simp
lemma poly_div_add_left: ‹(x + y) div z = x div z + y div z› (is ?Q) and poly_mod_add_left: ‹(x + y) mod z = x mod z + y mod z› (is ?R) for x y z :: ‹'a::field poly› proof - have‹((x + y) div z, (x + y) mod z) = (x div z + y div z, x mod z + y mod z)› proof (induction rule: euclidean_relation_polyI) case by0 thenshow ?caseby simp next case divides thenobtain w where‹x + y = z * w› by blast thenhave y: ‹y = z * w - x› by (simp add: algebra_simps) from‹z ≠ 0›show ?case using mod_mult_self4 [of z w ‹- x›] div_mult_self4 [of z w ‹- x›] by (simp add: algebra_simps y) next case euclidean_relation thenhave‹degree (x mod z + y mod z) 🚫 z› using degree_mod_less_degree [of z x] degree_mod_less_degree [of z y]
dvd_add_right_iff [of z x y] dvd_add_left_iff [of z y x] by (cases ‹z dvd x ∨ z dvd y›) (auto intro: degree_add_less) moreoverhave‹x + y = (x div z + y div z) * z + (x mod z + y mod z)› by (simp add: algebra_simps) ultimatelyshow ?case by simp qed thenshow ?Q and ?R by simp_all qed
lemma poly_div_diff_left: "(x - y) div z = x div z - y div z" for x y z :: "'a::field poly" by (simp only: diff_conv_add_uminus poly_div_add_left poly_div_minus_left)
lemma poly_mod_diff_left: "(x - y) mod z = x mod z - y mod z" for x y z :: "'a::field poly" by (simp only: diff_conv_add_uminus poly_mod_add_left poly_mod_minus_left)
lemma div_smult_right: ‹x div smult a y = smult (inverse a) (x div y)› (is ?Q) and mod_smult_right: ‹x mod smult a y = (if a = 0 then x else x mod y)› (is ?R) proof - have‹(x div smult a y, x mod smult a y) = (smult (inverse a) (x div y), (if a = 0 then x else x mod y))› proof (induction rule: euclidean_relation_polyI) case by0 thenshow ?caseby auto next case divides moreover define w where‹w = x div y› ultimatelyhave‹x = y * w› by (simp add: smult_dvd_iff) with divides show ?case by simp next case euclidean_relation thenshow ?case by (simp add: smult_dvd_iff degree_mod_less_degree) qed thenshow ?Q and ?R by simp_all qed
lemma mod_mult_unit_eq: ‹x mod (z * y) = x mod y› if‹is_unit z› for x y z :: ‹'a::field poly› proof (cases ‹y = 0›) case True thenshow ?thesis by simp next case False moreoverhave‹z ≠ 0› using that by auto moreover define a where‹a = lead_coeff z› ultimatelyhave‹z = [:a:]›‹a ≠ 0› using that monom_0 [of a] by (simp_all add: is_unit_monom_trivial) thenshow ?thesis by (simp add: mod_smult_right) qed
lemma poly_div_minus_right [simp]: "x div (- y) = - (x div y)" for x y :: "'a::field poly" using div_smult_right [of _ "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)
lemma poly_mod_minus_right [simp]: "x mod (- y) = x mod y" for x y :: "'a::field poly" using mod_smult_right [of _ "- 1::'a"] by simp
lemma poly_div_mult_right: ‹x div (y * z) = (x div y) div z› (is ?Q) and poly_mod_mult_right: ‹x mod (y * z) = y * (x div y mod z) + x mod y› (is ?R) for x y z :: ‹'a::field poly› proof - have‹(x div (y * z), x mod (y * z)) = ((x div y) div z, y * (x div y mod z) + x mod y)› proof (induction rule: euclidean_relation_polyI) case by0 thenshow ?caseby auto next case divides thenshow ?caseby auto next case euclidean_relation thenhave‹y ≠ 0›‹z ≠ 0› by simp_all with‹¬ y * z dvd x›have‹degree (y * (x div y mod z) + x mod y) 🚫 (y * z)› using degree_mod_less_degree [of y x] degree_mod_less_degree [of z ‹x div y›]
degree_add_eq_left [of ‹x mod y›‹y * (x div y mod z)›] by (cases ‹z dvd x div y›; cases ‹y dvd x›)
(auto simp add: degree_mult_eq not_dvd_imp_mod_neq_0 dvd_div_iff_mult) moreoverhave‹x = x div y div z * (y * z) + (y * (x div y mod z) + x mod y)› by (simp add: field_simps flip: distrib_left) ultimatelyshow ?case by simp qed thenshow ?Q and ?R by simp_all qed
lemma dvd_pCons_imp_dvd_pCons_mod: ‹y dvd pCons a (x mod y)›if‹y dvd pCons a x› proof - have‹pCons a x = pCons a (x div y * y + x mod y)› by simp alsohave‹… = pCons 0 (x div y * y) + pCons a (x mod y)› by simp alsohave‹pCons 0 (x div y * y) = (x div y * monom 1 (Suc 0)) * y› by (simp add: monom_Suc) finallyshow‹y dvd pCons a (x mod y)› using‹y dvd pCons a x›by simp qed
lemma degree_less_if_less_eqI: ‹degree x 🚫 y›if‹degree x ≤ degree y›‹coeff x (degree y) = 0›‹x ≠ 0› proof (cases ‹degree x = degree y›) case True with‹coeff x (degree y) = 0›have‹lead_coeff x = 0› by simp thenhave‹x = 0› by simp with‹x ≠ 0›show ?thesis by simp next case False with‹degree x ≤ degree y›show ?thesis by simp qed
lemma div_pCons_eq: ‹pCons a p div q = (if q = 0 then 0 else pCons (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) (p div q))› (is ?Q) and mod_pCons_eq: ‹pCons a p mod q = (if q = 0 then pCons a p else pCons a (p mod q) - smult (coeff (pCons a (p mod q)) (degree q) / lead_coeff q) q)› (is ?R) for x y :: ‹'a::field poly› proof - have‹?Q›and‹?R›if‹q = 0› using that by simp_all moreoverhave‹?Q›and‹?R›if‹q ≠ 0› proof -
define b where‹b = coeff (pCons a (p mod q)) (degree q) / lead_coeff q› have‹(pCons a p div q, pCons a p mod q) = (pCons b (p div q), (pCons a (p mod q) - smult b q))› proof (induction rule: euclidean_relation_polyI) case by0 with‹q ≠ 0›show ?caseby simp next case divides show ?case proof (cases ‹pCons a (p mod q) = 0›) case True thenshow ?thesis by (auto simp add: b_def) next case False have‹q dvd pCons a (p mod q)› using‹q dvd pCons a p›by (rule dvd_pCons_imp_dvd_pCons_mod) thenobtain s where *: ‹pCons a (p mod q) = q * s› .. with False have‹s ≠ 0› by auto from‹q ≠ 0›have‹degree (pCons a (p mod q)) ≤ degree q› by (auto simp add: Suc_le_eq intro: degree_mod_less_degree) moreoverfrom‹s ≠ 0›have‹degree q ≤ degree (pCons a (p mod q))› by (simp add: degree_mult_right_le *) ultimatelyhave‹degree (pCons a (p mod q)) = degree q› by (rule order.antisym) with‹s ≠ 0›‹q ≠ 0›have‹degree s = 0› by (simp add: * degree_mult_eq) thenobtain c where‹s = [:c:]› by (rule degree_eq_zeroE) alsohave‹c = b› using‹q ≠ 0›by (simp add: b_def * ‹s = [:c:]›) finallyhave‹smult b q = pCons a (p mod q)› by (simp add: *) thenshow ?thesis by simp qed next case euclidean_relation thenhave‹degree q > 0› using is_unit_iff_degree by blast from‹q ≠ 0›have‹degree (pCons a (p mod q)) ≤ degree q› by (auto simp add: Suc_le_eq intro: degree_mod_less_degree) moreoverhave‹degree (smult b q) ≤ degree q› by (rule degree_smult_le) ultimatelyhave‹degree (pCons a (p mod q) - smult b q) ≤ degree q› by (rule degree_diff_le) moreoverhave‹coeff (pCons a (p mod q) - smult b q) (degree q) = 0› using‹degree q > 0›by (auto simp add: b_def) ultimatelyhave‹degree (pCons a (p mod q) - smult b q) 🚫 q› using‹degree q > 0› by (cases ‹pCons a (p mod q) = smult b q›)
(auto intro: degree_less_if_less_eqI) thenshow ?case by simp qed with‹q ≠ 0›show ?Q and ?R by (simp_all add: b_def) qed ultimatelyshow ?Q and ?R by simp_all qed
lemma div_mod_fold_coeffs: "(p div q, p mod q) = (if q = 0 then (0, p) else fold_coeffs (λa (s, r). let b = coeff (pCons a r) (degree q) / coeff q (degree q) in (pCons b s, pCons a r - smult b q)) p (0, 0))" by (rule sym, induct p) (auto simp: div_pCons_eq mod_pCons_eq Let_def)
lemma mod_pCons: fixes a :: "'a::field" and x y :: "'a::field poly" assumes y: "y ≠ 0" defines"b ≡ 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_def by (simp add: mod_pCons_eq)
subsubsection ‹List-based versions for fast implementation› (* Subsection by: Sebastiaan Joosten René Thiemann Akihisa Yamada *) fun minus_poly_rev_list :: "'a :: group_add list ==> 'a list ==> 'a list" where "minus_poly_rev_list (x # xs) (y # ys) = (x - y) # (minus_poly_rev_list xs ys)"
| "minus_poly_rev_list xs [] = xs"
| "minus_poly_rev_list [] (y # ys) = []"
fun pseudo_divmod_main_list :: "'a::comm_ring_1 ==> 'a list ==> 'a list ==> 'a list ==> nat ==> 'a list × 'a list" where "pseudo_divmod_main_list lc q r d (Suc n) = (let rr = map ((*) lc) r; a = hd r; qqq = cCons a (map ((*) lc) q); rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d)) in pseudo_divmod_main_list lc qqq rrr d n)"
| "pseudo_divmod_main_list lc q r d 0 = (q, r)"
fun pseudo_mod_main_list :: "'a::comm_ring_1 ==> 'a list ==> 'a list ==> nat ==> 'a list" where "pseudo_mod_main_list lc r d (Suc n) = (let rr = map ((*) lc) r; a = hd r; rrr = tl (if a = 0 then rr else minus_poly_rev_list rr (map ((*) a) d)) in pseudo_mod_main_list lc rrr d n)"
| "pseudo_mod_main_list lc r d 0 = r"
fun divmod_poly_one_main_list :: "'a::comm_ring_1 list ==> 'a list ==> 'a list ==> nat ==> 'a list × 'a list" where "divmod_poly_one_main_list q r d (Suc n) = (let a = hd r; qqq = cCons a q; rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d)) in divmod_poly_one_main_list qqq rr d n)"
| "divmod_poly_one_main_list q r d 0 = (q, r)"
fun mod_poly_one_main_list :: "'a::comm_ring_1 list ==> 'a list ==> nat ==> 'a list" where "mod_poly_one_main_list r d (Suc n) = (let a = hd r; rr = tl (if a = 0 then r else minus_poly_rev_list r (map ((*) a) d)) in mod_poly_one_main_list rr d n)"
| "mod_poly_one_main_list r d 0 = r"
definition pseudo_divmod_list :: "'a::comm_ring_1 list ==> 'a list ==> 'a list × 'a list" where"pseudo_divmod_list p q = (if q = [] then ([], p) else (let rq = rev q; (qu,re) = pseudo_divmod_main_list (hd rq) [] (rev p) rq (1 + length p - length q) in (qu, rev re)))"
definition pseudo_mod_list :: "'a::comm_ring_1 list ==> 'a list ==> 'a list" where"pseudo_mod_list p q = (if q = [] then p else (let rq = rev q; re = pseudo_mod_main_list (hd rq) (rev p) rq (1 + length p - length q) in rev re))"
lemma minus_zero_does_nothing: "minus_poly_rev_list x (map ((*) 0) y) = x" for x :: "'a::ring list" by (induct x y rule: minus_poly_rev_list.induct) auto
lemma length_minus_poly_rev_list [simp]: "length (minus_poly_rev_list xs ys) = length xs" by (induct xs ys rule: minus_poly_rev_list.induct) auto
lemma if_0_minus_poly_rev_list: "(if a = 0 then x else minus_poly_rev_list x (map ((*) a) y)) = minus_poly_rev_list x (map ((*) a) y)" for a :: "'a::ring" by(cases "a = 0") (simp_all add: minus_zero_does_nothing)
lemma Poly_append: "Poly (a @ b) = Poly a + monom 1 (length a) * Poly b" for a :: "'a::comm_semiring_1 list" by (induct a) (auto simp: monom_0 monom_Suc)
lemma minus_poly_rev_list: "length p ≥ length q ==> Poly (rev (minus_poly_rev_list (rev p) (rev q))) = Poly p - monom 1 (length p - length q) * Poly q" for p q :: "'a :: comm_ring_1 list" proof (induct "rev p""rev q" arbitrary: p q rule: minus_poly_rev_list.induct) case (1 x xs y ys) thenhave"length (rev q) ≤ length (rev p)" by simp from this[folded 1(2,3)] have ys_xs: "length ys ≤ length xs" by simp thenhave *: "Poly (rev (minus_poly_rev_list xs ys)) = Poly (rev xs) - monom 1 (length xs - length ys) * Poly (rev ys)" by (subst "1.hyps"(1)[of "rev xs""rev ys", unfolded rev_rev_ident length_rev]) auto have"Poly p - monom 1 (length p - length q) * Poly q = Poly (rev (rev p)) - monom 1 (length (rev (rev p)) - length (rev (rev q))) * Poly (rev (rev q))" by simp alsohave"… = Poly (rev (x # xs)) - monom 1 (length (x # xs) - length (y # ys)) * Poly (rev (y # ys))" unfolding 1(2,3) by simp alsofrom ys_xs have"… = Poly (rev xs) + monom x (length xs) - (monom 1 (length xs - length ys) * Poly (rev ys) + monom y (length xs))" by (simp add: Poly_append distrib_left mult_monom smult_monom) alsohave"… = Poly (rev (minus_poly_rev_list xs ys)) + monom (x - y) (length xs)" unfolding * diff_monom[symmetric] by simp finallyshow ?case by (simp add: 1(2,3)[symmetric] smult_monom Poly_append) qed auto
lemma smult_monom_mult: "smult a (monom b n * f) = monom (a * b) n * f" using smult_monom [of a _ n] by (metis mult_smult_left)
lemma head_minus_poly_rev_list: "length d ≤ length r ==> d ≠ [] ==> hd (minus_poly_rev_list (map ((*) (last d)) r) (map ((*) (hd r)) (rev d))) = 0" for d r :: "'a::comm_ring list" proof (induct r) case Nil thenshow ?caseby simp next case (Cons a rs) thenshow ?caseby (cases "rev d") (simp_all add: ac_simps) qed
lemma Poly_map: "Poly (map ((*) a) p) = smult a (Poly p)" proof (induct p) case Nil thenshow ?caseby simp next case (Cons x xs) thenshow ?caseby (cases "Poly xs = 0") auto qed
lemma pseudo_divmod_main_list_invar: assumes leading_nonzero: "last d ≠ 0" and lc: "last d = lc" and"d ≠ []" and"pseudo_divmod_main_list lc q (rev r) (rev d) n = (q', rev r')" and"n = 1 + length r - length d" shows"pseudo_divmod_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n = (Poly q', Poly r')" using assms(4-) proof (induct n arbitrary: r q) case (Suc n) from Suc.prems have *: "¬ Suc (length r) ≤ length d" by simp with‹d ≠ []›have"r ≠ []" using Suc_leI length_greater_0_conv list.size(3) by fastforce let ?a = "(hd (rev r))" let ?rr = "map ((*) lc) (rev r)" let ?rrr = "rev (tl (minus_poly_rev_list ?rr (map ((*) ?a) (rev d))))" let ?qq = "cCons ?a (map ((*) lc) q)" from * Suc(3) have n: "n = (1 + length r - length d - 1)" by simp from * have rr_val:"(length ?rrr) = (length r - 1)" by auto with‹r ≠ []› * have rr_smaller: "(1 + length r - length d - 1) = (1 + length ?rrr - length d)" by auto from * have id: "Suc (length r) - length d = Suc (length r - length d)" by auto from Suc.prems * have"pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) (1 + length r - length d - 1) = (q', rev r')" by (simp add: Let_def if_0_minus_poly_rev_list id) with n have v: "pseudo_divmod_main_list lc ?qq (rev ?rrr) (rev d) n = (q', rev r')" by auto from * have sucrr:"Suc (length r) - length d = Suc (length r - length d)" using Suc_diff_le not_less_eq_eq by blast from Suc(3) ‹r ≠ []›have n_ok : "n = 1 + (length ?rrr) - length d" by simp have cong: "∧x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 ==> x2 = y2 ==> x3 = y3 ==> x4 = y4 ==> pseudo_divmod_main lc x1 x2 x3 x4 n = pseudo_divmod_main lc y1 y2 y3 y4 n" by simp have hd_rev: "coeff (Poly r) (length r - Suc 0) = hd (rev r)" using last_coeff_is_hd[OF ‹r ≠ []›] by simp show ?case unfolding Suc.hyps(1)[OF v n_ok, symmetric] pseudo_divmod_main.simps Let_def proof (rule cong[OF _ _ refl], goal_cases) case 1 show ?case by (simp add: monom_Suc hd_rev[symmetric] smult_monom Poly_map) next case 2 show ?case proof (subst Poly_on_rev_starting_with_0, goal_cases) show"hd (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))) = 0" by (fold lc, subst head_minus_poly_rev_list, insert * ‹d ≠ []›, auto) from * have"length d ≤ length r" by simp thenshow"smult lc (Poly r) - monom (coeff (Poly r) (length r - 1)) n * Poly d = Poly (rev (minus_poly_rev_list (map ((*) lc) (rev r)) (map ((*) (hd (rev r))) (rev d))))" by (fold rev_map) (auto simp add: n smult_monom_mult Poly_map hd_rev [symmetric]
minus_poly_rev_list) qed qed simp qed simp
lemma pseudo_divmod_impl [code]: "pseudo_divmod f g = map_prod poly_of_list poly_of_list (pseudo_divmod_list (coeffs f) (coeffs g))" for f g :: "'a::comm_ring_1 poly" proof (cases "g = 0") case False thenhave"last (coeffs g) ≠ 0" and"last (coeffs g) = lead_coeff g" and"coeffs g ≠ []" by (simp_all add: last_coeffs_eq_coeff_degree) moreoverobtain q r where qr: "pseudo_divmod_main_list (last (coeffs g)) (rev []) (rev (coeffs f)) (rev (coeffs g)) (1 + length (coeffs f) - length (coeffs g)) = (q, rev (rev r))" by force ultimatelyhave"(Poly q, Poly (rev r)) = pseudo_divmod_main (lead_coeff g) 0 f g (length (coeffs f) - Suc 0) (Suc (length (coeffs f)) - length (coeffs g))" by (subst pseudo_divmod_main_list_invar [symmetric]) auto moreoverhave"pseudo_divmod_main_list (hd (rev (coeffs g))) [] (rev (coeffs f)) (rev (coeffs g)) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by (metis hd_rev qr rev.simps(1) rev_swap) ultimatelyshow ?thesis by (simp add: degree_eq_length_coeffs pseudo_divmod_def pseudo_divmod_list_def) next case True thenshow ?thesis by (auto simp add: pseudo_divmod_def pseudo_divmod_list_def) qed
lemma pseudo_mod_main_list: "snd (pseudo_divmod_main_list l q xs ys n) = pseudo_mod_main_list l xs ys n" by (induct n arbitrary: l q xs ys) (auto simp: Let_def)
lemma pseudo_mod_impl[code]: "pseudo_mod f g = poly_of_list (pseudo_mod_list (coeffs f) (coeffs g))" proof - have snd_case: "∧f g p. snd ((λ(x,y). (f x, g y)) p) = g (snd p)" by auto show ?thesis unfolding pseudo_mod_def pseudo_divmod_impl pseudo_divmod_list_def
pseudo_mod_list_def Let_def by (simp add: snd_case pseudo_mod_main_list) qed
subsubsection ‹Improved Code-Equations for Polynomial (Pseudo) Division›
lemma pdivmod_via_pseudo_divmod: ‹(f div g, f mod g) = (if g = 0 then (0, f) else let ilc = inverse (lead_coeff g); h = smult ilc g; (q,r) = pseudo_divmod f h in (smult ilc q, r))›
(is‹?l = ?r›) proof (cases ‹g = 0›) case True thenshow ?thesis by simp next case False
define ilc where‹ilc = inverse (lead_coeff g)›
define h where‹h = smult ilc g› from False have‹lead_coeff h = 1› and‹ilc ≠ 0› by (auto simp: h_def ilc_def)
define q r where‹q = f div h›and‹r = f mod h› with‹lead_coeff h = 1›have p: ‹pseudo_divmod f h = (q, r)› by (simp add: pseudo_divmod_eq_div_mod) from‹ilc ≠ 0›have‹(f div g, f mod g) = (smult ilc q, r)› by (auto simp: h_def div_smult_right mod_smult_right q_def r_def) alsohave‹(smult ilc q, r) = ?r› using‹g ≠ 0›by (auto simp: Let_def p simp flip: h_def ilc_def) finallyshow ?thesis . qed
lemma pdivmod_via_pseudo_divmod_list: "(f div g, f mod g) = (let cg = coeffs g in if cg = [] then (0, f) else let cf = coeffs f; ilc = inverse (last cg); ch = map ((*) ilc) cg; (q, r) = pseudo_divmod_main_list 1 [] (rev cf) (rev ch) (1 + length cf - length cg) in (poly_of_list (map ((*) ilc) q), poly_of_list (rev r)))" proof - note d = pdivmod_via_pseudo_divmod pseudo_divmod_impl pseudo_divmod_list_def show ?thesis proof (cases "g = 0") case True with d show ?thesis by auto next case False
define ilc where"ilc = inverse (coeff g (degree g))" from False have ilc: "ilc ≠ 0" by (auto simp: ilc_def) with False have id: "g = 0 ⟷ False""coeffs g = [] ⟷ False" "last (coeffs g) = coeff g (degree g)" "coeffs (smult ilc g) = [] ⟷ False" by (auto simp: last_coeffs_eq_coeff_degree) have id2: "hd (rev (coeffs (smult ilc g))) = 1" by (subst hd_rev, insert id ilc, auto simp: coeffs_smult, subst last_map, auto simp: id ilc_def) have id3: "length (coeffs (smult ilc g)) = length (coeffs g)" "rev (coeffs (smult ilc g)) = rev (map ((*) ilc) (coeffs g))" unfolding coeffs_smult using ilc by auto obtain q r where pair: "pseudo_divmod_main_list 1 [] (rev (coeffs f)) (rev (map ((*) ilc) (coeffs g))) (1 + length (coeffs f) - length (coeffs g)) = (q, r)" by force show ?thesis unfolding d Let_def id if_False ilc_def[symmetric] map_prod_def[symmetric] id2 unfolding id3 pair map_prod_def split by (auto simp: Poly_map) qed qed
lemma pseudo_divmod_main_list_1: "pseudo_divmod_main_list 1 = divmod_poly_one_main_list" proof (intro ext, goal_cases) case (1 q r d n) have *: "map ((*) 1) xs = xs"for xs :: "'a list" by (induct xs) auto show ?case by (induct n arbitrary: q r d) (auto simp: * Let_def) qed
fun divide_poly_main_list :: "'a::idom_divide ==> 'a list ==> 'a list ==> 'a list ==> nat ==> 'a list" where "divide_poly_main_list lc q r d (Suc n) = (let cr = hd r in if cr = 0 then divide_poly_main_list lc (cCons cr q) (tl r) d n else let a = cr div lc; qq = cCons a q; rr = minus_poly_rev_list r (map ((*) a) d) in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])"
| "divide_poly_main_list lc q r d 0 = q"
lemma divide_poly_main_list_simp [simp]: "divide_poly_main_list lc q r d (Suc n) = (let cr = hd r; a = cr div lc; qq = cCons a q; rr = minus_poly_rev_list r (map ((*) a) d) in if hd rr = 0 then divide_poly_main_list lc qq (tl rr) d n else [])" by (simp add: Let_def minus_zero_does_nothing)
declare divide_poly_main_list.simps(1)[simp del]
definition divide_poly_list :: "'a::idom_divide poly ==> 'a poly ==> 'a poly" where"divide_poly_list f g = (let cg = coeffs g in if cg = [] then g else let cf = coeffs f; cgr = rev cg in poly_of_list (divide_poly_main_list (hd cgr) [] (rev cf) cgr (1 + length cf - length cg)))"
lemma mod_poly_one_main_list: "snd (divmod_poly_one_main_list q r d n) = mod_poly_one_main_list r d n" by (induct n arbitrary: q r d) (auto simp: Let_def)
lemma mod_poly_code [code]: "f mod g = (let cg = coeffs g in if cg = [] then f else let cf = coeffs f; ilc = inverse (last cg); ch = map ((*) ilc) cg; r = mod_poly_one_main_list (rev cf) (rev ch) (1 + length cf - length cg) in poly_of_list (rev r))"
(is"_ = ?rhs") proof - have"snd (f div g, f mod g) = ?rhs" unfolding pdivmod_via_divmod_list Let_def mod_poly_one_main_list [symmetric, of _ _ _ Nil] by (auto split: prod.splits) thenshow ?thesis by simp qed
definition div_field_poly_impl :: "'a :: field poly ==> 'a poly ==> 'a poly" where"div_field_poly_impl f g = (let cg = coeffs g in if cg = [] then 0 else let cf = coeffs f; ilc = inverse (last cg); ch = map ((*) ilc) cg; q = fst (divmod_poly_one_main_list [] (rev cf) (rev ch) (1 + length cf - length cg)) in poly_of_list ((map ((*) ilc) q)))"
text‹We do not declare the following lemma as code equation, since then polynomial division on non-fields will no longer be executable. However, a code-unfold is possible, since ‹div_field_poly_impl›is a bit more efficient than the generic polynomial division.› lemma div_field_poly_impl[code_unfold]: "(div) = div_field_poly_impl" proof (intro ext) fix f g :: "'a poly" have"fst (f div g, f mod g) = div_field_poly_impl f g" unfolding div_field_poly_impl_def pdivmod_via_divmod_list Let_def by (auto split: prod.splits) thenshow"f div g = div_field_poly_impl f g" by simp qed
lemma divide_poly_main_list: assumes lc0: "lc ≠ 0" and lc: "last d = lc" and d: "d ≠ []" and"n = (1 + length r - length d)" shows"Poly (divide_poly_main_list lc q (rev r) (rev d) n) = divide_poly_main lc (monom 1 n * Poly q) (Poly r) (Poly d) (length r - 1) n" using assms(4-) proof (induct "n" arbitrary: r q) case (Suc n) from Suc.prems have ifCond: "¬ Suc (length r) ≤ length d" by simp with d have r: "r ≠ []" using Suc_leI length_greater_0_conv list.size(3) by fastforce thenobtain rr lcr where r: "r = rr @ [lcr]" by (cases r rule: rev_cases) auto from d lc obtain dd where d: "d = dd @ [lc]" by (cases d rule: rev_cases) auto from Suc(2) ifCond have n: "n = 1 + length rr - length d" by (auto simp: r) from ifCond have len: "length dd ≤ length rr" by (simp add: r d) show ?case proof (cases "lcr div lc * lc = lcr") case False with r d show ?thesis unfolding Suc(2)[symmetric] by (auto simp add: Let_def nth_default_append) next case True with r d have id: "?thesis ⟷ Poly (divide_poly_main_list lc (cCons (lcr div lc) q) (rev (rev (minus_poly_rev_list (rev rr) (rev (map ((*) (lcr div lc)) dd))))) (rev d) n) = divide_poly_main lc (monom 1 (Suc n) * Poly q + monom (lcr div lc) n) (Poly r - monom (lcr div lc) n * Poly d) (Poly d) (length rr - 1) n" by (cases r rule: rev_cases; cases "d" rule: rev_cases)
(auto simp add: Let_def rev_map nth_default_append) have cong: "∧x1 x2 x3 x4 y1 y2 y3 y4. x1 = y1 ==> x2 = y2 ==> x3 = y3 ==> x4 = y4 ==> divide_poly_main lc x1 x2 x3 x4 n = divide_poly_main lc y1 y2 y3 y4 n" by simp show ?thesis unfolding id proof (subst Suc(1), simp add: n,
subst minus_poly_rev_list, force simp: len, rule cong[OF _ _ refl], goal_cases) case 2 have"monom lcr (length rr) = monom (lcr div lc) (length rr - length dd) * monom lc (length dd)" by (simp add: mult_monom len True) thenshow ?caseunfolding r d Poly_append n ring_distribs by (auto simp: Poly_map smult_monom smult_monom_mult) qed (auto simp: len monom_Suc smult_monom) qed qed simp
lemma divide_poly_list[code]: "f div g = divide_poly_list f g" proof - note d = divide_poly_def divide_poly_list_def show ?thesis proof (cases "g = 0") case True show ?thesis by (auto simp: d True) next case False thenobtain cg lcg where cg: "coeffs g = cg @ [lcg]" by (cases "coeffs g" rule: rev_cases) auto with False have id: "(g = 0) = False""(cg @ [lcg] = []) = False" by auto from cg False have lcg: "coeff g (degree g) = lcg" using last_coeffs_eq_coeff_degree last_snoc by force with False have"lcg ≠ 0"by auto from cg Poly_coeffs [of g] have ltp: "Poly (cg @ [lcg]) = g" by auto show ?thesis unfolding d cg Let_def id if_False poly_of_list_def by (subst divide_poly_main_list, insert False cg ‹lcg ≠ 0›)
(auto simp: lcg ltp, simp add: degree_eq_length_coeffs) qed qed
lemma poly_mod: "poly (p mod q) x = poly p x"if"poly q x = 0" proof - from that have"poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x" by simp alsohave"… = poly p x" by (simp only: poly_add [symmetric]) simp finallyshow ?thesis . qed
subsection‹Primality and irreducibility in polynomial rings›
lemma prod_mset_const_poly: "(∏x∈#A. [:f x:]) = [:prod_mset (image_mset f A):]" by (induct A) (simp_all add: ac_simps)
lemma irreducible_const_poly_iff: fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" shows"irreducible [:c:] ⟷ irreducible c" proof assume A: "irreducible c" show"irreducible [:c:]" proof (rule irreducibleI) fix a b assume ab: "[:c:] = a * b" hence"degree [:c:] = degree (a * b)"by (simp only: ) alsofrom A ab have"a ≠ 0""b ≠ 0"by auto hence"degree (a * b) = degree a + degree b"by (simp add: degree_mult_eq) finallyhave"degree a = 0""degree b = 0"by auto thenobtain a' b' where ab': "a = [:a':]""b = [:b':]"by (auto elim!: degree_eq_zeroE) from ab have"coeff [:c:] 0 = coeff (a * b) 0"by (simp only: ) hence"c = a' * b'"by (simp add: ab' mult_ac) from A and this have"a' dvd 1 ∨ b' dvd 1"by (rule irreducibleD) with ab' show"a dvd 1 ∨ b dvd 1" by (auto simp add: is_unit_const_poly_iff) qed (insert A, auto simp: irreducible_def is_unit_poly_iff) next assume A: "irreducible [:c:]" thenhave"c ≠ 0"and"¬ c dvd 1" by (auto simp add: irreducible_def is_unit_const_poly_iff) thenshow"irreducible c" proof (rule irreducibleI) fix a b assume ab: "c = a * b" hence"[:c:] = [:a:] * [:b:]"by (simp add: mult_ac) from A and this have"[:a:] dvd 1 ∨ [:b:] dvd 1"by (rule irreducibleD) thenshow"a dvd 1 ∨ b dvd 1" by (auto simp add: is_unit_const_poly_iff) qed qed
lemma lift_prime_elem_poly: assumes"prime_elem (c :: 'a :: semidom)" shows"prime_elem [:c:]" proof (rule prime_elemI) fix a b assume *: "[:c:] dvd a * b" from * have dvd: "c dvd coeff (a * b) n"for n by (subst (asm) const_poly_dvd_iff) blast
{
define m where"m = (GREATEST m. ¬c dvd coeff b m)" assume"¬[:c:] dvd b" hence A: "∃i. ¬c dvd coeff b i"by (subst (asm) const_poly_dvd_iff) blast have B: "∧i. ¬c dvd coeff b i ==> i ≤ degree b" by (auto intro: le_degree) have coeff_m: "¬c dvd coeff b m"unfolding m_def by (rule GreatestI_ex_nat[OF A B]) have"i ≤ m"if"¬c dvd coeff b i"for i unfolding m_def by (metis (mono_tags, lifting) B Greatest_le_nat that) hence dvd_b: "c dvd coeff b i"if"i > m"for i using that by force
have"c dvd coeff a i"for i proof (induction i rule: nat_descend_induct[of "degree a"]) case (base i) thus ?caseby (simp add: coeff_eq_0) next case (descend i) let ?A = "{..i+m} - {i}" have"c dvd coeff (a * b) (i + m)"by (rule dvd) alsohave"coeff (a * b) (i + m) = (∑k≤i + m. coeff a k * coeff b (i + m - k))" by (simp add: coeff_mult) alsohave"{..i+m} = insert i ?A"by auto alsohave"(∑k∈…. coeff a k * coeff b (i + m - k)) = coeff a i * coeff b m + (∑k∈?A. coeff a k * coeff b (i + m - k))"
(is"_ = _ + ?S") by (subst sum.insert) simp_all finallyhave eq: "c dvd coeff a i * coeff b m + ?S" . moreoverhave"c dvd ?S" proof (rule dvd_sum) fix k assume k: "k ∈ {..i+m} - {i}" show"c dvd coeff a k * coeff b (i + m - k)" proof (cases "k < i") case False with k have"c dvd coeff a k"by (intro descend.IH) simp thus ?thesis by simp next case True hence"c dvd coeff b (i + m - k)"by (intro dvd_b) simp thus ?thesis by simp qed qed ultimatelyhave"c dvd coeff a i * coeff b m" by (simp add: dvd_add_left_iff) with assms coeff_m show"c dvd coeff a i" by (simp add: prime_elem_dvd_mult_iff) qed hence"[:c:] dvd a"by (subst const_poly_dvd_iff) blast
} thenshow"[:c:] dvd a ∨ [:c:] dvd b"by blast next from assms show"[:c:] ≠ 0"and"¬ [:c:] dvd 1" by (simp_all add: prime_elem_def is_unit_const_poly_iff) qed
lemma prime_elem_const_poly_iff: fixes c :: "'a :: semidom" shows"prime_elem [:c:] ⟷ prime_elem c" proof assume A: "prime_elem [:c:]" show"prime_elem c" proof (rule prime_elemI) fix a b assume"c dvd a * b" hence"[:c:] dvd [:a:] * [:b:]"by (simp add: mult_ac) from A and this have"[:c:] dvd [:a:] ∨ [:c:] dvd [:b:]"by (rule prime_elem_dvd_multD) thus"c dvd a ∨ c dvd b"by simp qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) qed (auto intro: lift_prime_elem_poly)
subsection‹Content and primitive part of a polynomial›
lemma const_poly_dvd_iff_dvd_content: "[:c:] dvd p ⟷ c dvd content p" for c :: "'a::semiring_gcd" proof (cases "p = 0") case True thenshow ?thesis by simp next case False have"[:c:] dvd p ⟷ (∀n. c dvd coeff p n)" by (rule const_poly_dvd_iff) alsohave"…⟷ (∀a∈set (coeffs p). c dvd a)" proof safe fix n :: nat assume"∀a∈set (coeffs p). c dvd a" thenshow"c dvd coeff p n" by (cases "n ≤ degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits) qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits) alsohave"…⟷ c dvd content p" by (simp add: content_def dvd_Gcd_fin_iff dvd_mult_unit_iff) finallyshow ?thesis . qed
lemma content_dvd [simp]: "[:content p:] dvd p" by (subst const_poly_dvd_iff_dvd_content) simp_all
lemma content_dvd_coeff [simp]: "content p dvd coeff p n" proof (cases "p = 0") case True thenshow ?thesis by simp next case False thenshow ?thesis by (cases "n ≤ degree p")
(auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd) qed
lemma content_dvd_coeffs: "c ∈ set (coeffs p) ==> content p dvd c" by (simp add: content_def Gcd_fin_dvd)
lemma content_times_primitive_part [simp]: "smult (content p) (primitive_part p) = p" for p :: "'a :: semiring_gcd poly" proof (cases "p = 0") case True thenshow ?thesis by simp next case False thenshow ?thesis unfolding primitive_part_def by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
intro: map_poly_idI) qed
lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 ⟷ p = 0" proof (cases "p = 0") case True thenshow ?thesis by simp next case False thenhave"primitive_part p = map_poly (λx. x div content p) p" by (simp add: primitive_part_def) alsofrom False have"… = 0 ⟷ p = 0" by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs) finallyshow ?thesis using False by simp qed
lemma content_primitive_part [simp]: fixes p :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly" assumes"p ≠ 0" shows"content (primitive_part p) = 1" proof - have"p = smult (content p) (primitive_part p)" by simp alsohave"content … = content (primitive_part p) * content p" by (simp del: content_times_primitive_part add: ac_simps) finallyhave"1 * content p = content (primitive_part p) * content p" by simp thenhave"1 * content p div content p = content (primitive_part p) * content p div content p" by simp with assms show ?thesis by simp qed
lemma content_decompose: obtains p' :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly" where"p = smult (content p) p'""content p' = 1" proof (cases "p = 0") case True thenhave"p = smult (content p) 1""content 1 = 1" by simp_all thenshow ?thesis .. next case False thenhave"p = smult (content p) (primitive_part p)""content (primitive_part p) = 1" by simp_all thenshow ?thesis .. qed
lemma content_dvd_contentI [intro]: "p dvd q ==> content p dvd content q" using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
lemma content_1_mult: fixes f g :: "'a :: {semiring_gcd, factorial_semiring} poly" assumes"content f = 1""content g = 1" shows"content (f * g) = 1" proof (cases "f * g = 0") case False from assms have"f ≠ 0""g ≠ 0"by auto
hence"f * g ≠ 0"by auto
{ assume"¬is_unit (content (f * g))" with False have"∃p. p dvd content (f * g) ∧ prime p" by (intro prime_divisor_exists) simp_all thenobtain p where"p dvd content (f * g)""prime p"by blast from‹p dvd content (f * g)›have"[:p:] dvd f * g" by (simp add: const_poly_dvd_iff_dvd_content) moreoverfrom‹prime p›have"prime_elem [:p:]"by (simp add: lift_prime_elem_poly) ultimatelyhave"[:p:] dvd f ∨ [:p:] dvd g" by (simp add: prime_elem_dvd_mult_iff) with assms have"is_unit p"by (simp add: const_poly_dvd_iff_dvd_content) with‹prime p›have False by simp
} hence"is_unit (content (f * g))"by blast hence"normalize (content (f * g)) = 1"by (simp add: is_unit_normalize del: normalize_content) thus ?thesis by simp qed (insert assms, auto)
lemma content_mult: fixes p q :: "'a :: {factorial_semiring, semiring_gcd, normalization_semidom_multiplicative} poly" shows"content (p * q) = content p * content q" proof (cases "p * q = 0") case False thenhave"p ≠ 0"and"q ≠ 0" by simp_all thenhave *: "content (primitive_part p * primitive_part q) = 1" by (auto intro: content_1_mult) have"p * q = smult (content p) (primitive_part p) * smult (content q) (primitive_part q)" by simp alsohave"… = smult (content p * content q) (primitive_part p * primitive_part q)" by (metis mult.commute mult_smult_right smult_smult) with * show ?thesis by (simp add: normalize_mult) next case True thenshow ?thesis by auto qed
end
lemma primitive_part_mult: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide, normalization_semidom_multiplicative} poly" shows"primitive_part (p * q) = primitive_part p * primitive_part q" proof - have"primitive_part (p * q) = p * q div [:content (p * q):]" by (simp add: primitive_part_def div_const_poly_conv_map_poly) alsohave"… = (p div [:content p:]) * (q div [:content q:])" by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac) alsohave"… = primitive_part p * primitive_part q" by (simp add: primitive_part_def div_const_poly_conv_map_poly) finallyshow ?thesis . qed
lemma primitive_part_smult: fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide, normalization_semidom_multiplicative} poly" shows"primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)" proof - have"smult a p = [:a:] * p"by simp alsohave"primitive_part … = smult (unit_factor a) (primitive_part p)" by (subst primitive_part_mult) simp_all finallyshow ?thesis . qed
lemma primitive_part_dvd_primitive_partI [intro]: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide, normalization_semidom_multiplicative} poly" shows"p dvd q ==> primitive_part p dvd primitive_part q" by (auto elim!: dvdE simp: primitive_part_mult)
lemma content_prod_mset: fixes A :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly multiset" shows"content (prod_mset A) = prod_mset (image_mset content A)" by (induction A) (simp_all add: content_mult mult_ac)
lemma content_prod_eq_1_iff: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly" shows"content (p * q) = 1 ⟷ content p = 1 ∧ content q = 1" proof safe assume A: "content (p * q) = 1"
{ fix p q :: "'a poly"assume"content p * content q = 1" hence"1 = content p * content q"by simp hence"content p dvd 1"by (rule dvdI) hence"content p = 1"by simp
} note B = this from A B[of p q] B [of q p] show"content p = 1""content q = 1" by (simp_all add: content_mult mult_ac) qed (auto simp: content_mult)
subsection‹A typeclass for algebraically closed fields›
(* TODO: Move! *)
text‹ Since the required sort constraints are not available inside the class, we have to resort to a somewhat awkward way of writing the definition of algebraically closed fields: › class alg_closed_field = field + assumes alg_closed: "n > 0 ==> f n ≠ 0 ==>∃x. (∑k≤n. f k * x ^ k) = 0"
text‹ We can then however easily show the equivalence to the proper definition: › lemma alg_closed_imp_poly_has_root: assumes"degree (p :: 'a :: alg_closed_field poly) > 0" shows"∃x. poly p x = 0" proof - have"∃x. (∑k≤degree p. coeff p k * x ^ k) = 0" using assms by (intro alg_closed) auto thus ?thesis by (simp add: poly_altdef) qed
lemma alg_closedI [Pure.intro]: assumes"∧p :: 'a poly. degree p > 0 ==> lead_coeff p = 1 ==>∃x. poly p x = 0" shows"OFCLASS('a :: field, alg_closed_field_class)" proof fix n :: nat and f :: "nat ==> 'a" assume n: "n > 0""f n ≠ 0"
define p where"p = Abs_poly (λk. if k ≤ n then f k else 0)" have coeff_p: "coeff p k = (if k ≤ n then f k else 0)"for k proof - have"eventually (λk. k > n) cofinite" by (auto simp: MOST_nat) hence"eventually (λk. (if k ≤ n then f k else 0) = 0) cofinite" by eventually_elim auto thus ?thesis unfolding p_def by (subst Abs_poly_inverse) auto qed
from n have"degree p ≥ n" by (intro le_degree) (auto simp: coeff_p) moreoverhave"degree p ≤ n" by (intro degree_le) (auto simp: coeff_p) ultimatelyhave deg_p: "degree p = n" by linarith from deg_p and n have [simp]: "p ≠ 0" by auto
define p' where"p' = smult (inverse (lead_coeff p)) p" have deg_p': "degree p' = degree p" by (auto simp: p'_def) have lead_coeff_p' [simp]: "lead_coeff p' = 1" by (auto simp: p'_def)
from deg_p and deg_p' and n have"degree p' > 0" by simp from assms[OF this] obtain x where"poly p' x = 0" by auto hence"poly p x = 0" by (simp add: p'_def) alsohave"poly p x = (∑k≤n. f k * x ^ k)" unfolding poly_altdef by (intro sum.cong) (auto simp: deg_p coeff_p) finallyshow"∃x. (∑k≤n. f k * x ^ k) = 0" .. qed
lemma (in alg_closed_field) nth_root_exists: assumes"n > 0" shows"∃y. y ^ n = (x :: 'a)" proof -
define f where"f = (λi. if i = 0 then -x else if i = n then 1 else 0)" have"∃x. (∑k≤n. f k * x ^ k) = 0" by (rule alg_closed) (use assms in‹auto simp: f_def›) alsohave"(λx. ∑k≤n. f k * x ^ k) = (λx. ∑k∈{0,n}. f k * x ^ k)" by (intro ext sum.mono_neutral_right) (auto simp: f_def) finallyshow"∃y. y ^ n = x" using assms by (simp add: f_def) qed
text‹ We can now prove by induction that every polynomial of degree ‹n› s ‹n› linear factors: › lemma alg_closed_imp_factorization: fixes p :: "'a :: alg_closed_field poly" assumes"p ≠ 0" shows"∃A. size A = degree p ∧ p = smult (lead_coeff p) (∏x∈#A. [:-x, 1:])" using assms proof (induction"degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "degree p = 0") case True thus ?thesis by (intro exI[of _ "{#}"]) (auto elim!: degree_eq_zeroE) next case False thenobtain x where x: "poly p x = 0" using alg_closed_imp_poly_has_root by blast hence"[:-x, 1:] dvd p" using poly_eq_0_iff_dvd by blast thenobtain q where p_eq: "p = [:-x, 1:] * q" by (elim dvdE) have"q ≠ 0" using less.prems p_eq by auto moreoverfrom this have deg: "degree p = Suc (degree q)" unfolding p_eq by (subst degree_mult_eq) auto ultimatelyobtain A where A: "size A = degree q""q = smult (lead_coeff q) (∏x∈#A. [:-x, 1:])" using less.hyps[of q] by auto have"smult (lead_coeff p) (∏y∈#add_mset x A. [:- y, 1:]) = [:- x, 1:] * smult (lead_coeff q) (∏y∈#A. [:- y, 1:])" unfolding p_eq lead_coeff_mult by simp alsonote A(2) [symmetric] alsonote p_eq [symmetric] finallyshow ?thesis using A(1) by (intro exI[of _ "add_mset x A"]) (auto simp: deg) qed qed
text‹ As an alternative characterisation of algebraic closure, one can also say that any polynomial of degree at least 2 splits into non-constant factors: › lemma alg_closed_imp_reducible: assumes"degree (p :: 'a :: alg_closed_field poly) > 1" shows"¬irreducible p" proof - have"degree p > 0" using assms by auto thenobtain z where z: "poly p z = 0" using alg_closed_imp_poly_has_root[of p] by blast thenhave dvd: "[:-z, 1:] dvd p" by (subst dvd_iff_poly_eq_0) auto thenobtain q where q: "p = [:-z, 1:] * q" by (erule dvdE) have [simp]: "q ≠ 0" using assms q by auto
show ?thesis proof (rule reducible_polyI) show"p = [:-z, 1:] * q" by fact next have"degree p = degree ([:-z, 1:] * q)" by (simp only: q) alsohave"… = degree q + 1" by (subst degree_mult_eq) auto finallyshow"degree q > 0" using assms by linarith qed auto qed
text‹ When proving algebraic closure through reducibility, we can assume w.l.o.g. that the polynomial is monic and has a non-zero constant coefficient: › lemma alg_closedI_reducible: assumes"∧p :: 'a poly. degree p > 1 ==> lead_coeff p = 1 ==> coeff p 0 ≠ 0 ==> ¬irreducible p" shows"OFCLASS('a :: field, alg_closed_field_class)" proof fix p :: "'a poly"assume p: "degree p > 0""lead_coeff p = 1" show"∃x. poly p x = 0" proof (cases "coeff p 0 = 0") case True hence"poly p 0 = 0" by (simp add: poly_0_coeff_0) thus ?thesis by blast next case False from p and this show ?thesis proof (induction"degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "degree p = 1") case True thenobtain a b where p: "p = [:a, b:]" by (cases p) (auto split: if_splits elim!: degree_eq_zeroE) from True have [simp]: "b ≠ 0" by (auto simp: p) have"poly p (-a/b) = 0" by (auto simp: p) thus ?thesis by blast next case False hence"degree p > 1" using less.prems by auto from assms[OF ‹degree p > 1›‹lead_coeff p = 1›‹coeff p 0 ≠ 0›] have"¬irreducible p"by auto thenobtain r s where rs: "degree r > 0""degree s > 0""p = r * s" using less.prems unfolding irreducible_def by (metis is_unit_iff_degree mult_not_zero zero_less_iff_neq_zero) hence"coeff r 0 ≠ 0" using‹coeff p 0 ≠ 0›by (auto simp: coeff_mult_0)
define r' where"r' = smult (inverse (lead_coeff r)) r" have [simp]: "degree r' = degree r" by (simp add: r'_def) have lc: "lead_coeff r' = 1" using rs by (auto simp: r'_def) have nz: "coeff r' 0 ≠ 0" using‹coeff r 0 ≠ 0›by (auto simp: r'_def)
have"degree r < degree r + degree s" using rs by linarith alsohave"… = degree (r * s)" using rs(3) less.prems by (subst degree_mult_eq) auto alsohave"r * s = p" using rs(3) by simp finallyhave"∃x. poly r' x = 0" by (intro less) (use lc rs nz in auto) thus ?thesis using rs(3) by (auto simp: r'_def) qed qed qed qed
text‹ Using a clever Tschirnhausen transformation mentioned e.g. in the article by Nowak~🍋‹"nowak2000"›, › lemma alg_closedI_reducible_coeff_deg_minus_one_eq_0: assumes"∧p :: 'a poly. degree p > 1 ==> lead_coeff p = 1 ==> coeff p (degree p - 1) = 0 ==> coeff p 0 ≠ 0 ==>¬irreducible p" shows"OFCLASS('a :: field_char_0, alg_closed_field_class)" proof (rule alg_closedI_reducible, goal_cases) case (1 p)
define n where [simp]: "n = degree p"
define a where"a = coeff p (n - 1)"
define r where"r = [: -a / of_nat n, 1 :]"
define s where"s = [: a / of_nat n, 1 :]"
define q where"q = pcompose p r"
have"n > 0" using 1 by simp have r_altdef: "r = monom 1 1 + [:-a / of_nat n:]" by (simp add: r_def monom_altdef) have deg_q: "degree q = n" by (simp add: q_def r_def degree_pcompose) have lc_q: "lead_coeff q = 1" unfolding q_def using 1 by (subst lead_coeff_comp) (simp_all add: r_def) have"q ≠ 0" using 1 deg_q by auto
have"coeff q (n - 1) = (∑i≤n. ∑k≤i. coeff p i * (of_nat (i choose k) * ((-a / of_nat n) ^ (i - k) * (if k = n - 1 then 1 else 0))))" unfolding q_def pcompose_altdef poly_altdef r_altdef by (simp_all add: degree_map_poly coeff_map_poly coeff_sum binomial_ring sum_distrib_left poly_const_pow
sum_distrib_right mult_ac monom_power coeff_monom_mult of_nat_poly cong: if_cong) alsohave"… = (∑i≤n. ∑k∈(if i ≥ n - 1 then {n-1} else {}). coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))" by (rule sum.cong [OF refl], rule sum.mono_neutral_cong_right) (auto split: if_splits) alsohave"… = (∑i∈{n-1,n}. ∑k∈(if i ≥ n - 1 then {n-1} else {}). coeff p i * (of_nat (i choose k) * (-a / of_nat n) ^ (i - k)))" by (rule sum.mono_neutral_right) auto alsohave"… = a - of_nat (n choose (n - 1)) * a / of_nat n" using 1 by (simp add: a_def) alsohave"n choose (n - 1) = n" using‹n > 0›by (subst binomial_symmetric) auto alsohave"a - of_nat n * a / of_nat n = 0" using‹n > 0›by simp finallyhave"coeff q (n - 1) = 0" .
show ?case proof (cases "coeff q 0 = 0") case True hence"poly p (- (a / of_nat (degree p))) = 0" by (auto simp: q_def r_def) thus ?thesis by (rule root_imp_reducible_poly) (use 1 in auto) next case False hence"¬irreducible q" using assms[of q] and lc_q and 1 and‹coeff q (n - 1) = 0› by (auto simp: deg_q) thenobtain u v where uv: "degree u > 0""degree v > 0""q = u * v" using‹q ≠ 0› 1 deg_q unfolding irreducible_def by (metis degree_mult_eq_0 is_unit_iff_degree n_def neq0_conv not_one_less_zero)
have"p = pcompose q s" by (simp add: q_def r_def s_def pcompose_pCons flip: pcompose_assoc) alsohave"q = u * v" by fact finallyhave"p = pcompose u s * pcompose v s" by (simp add: pcompose_mult) moreoverhave"degree (pcompose u s) > 0""degree (pcompose v s) > 0" using uv by (simp_all add: s_def degree_pcompose) ultimatelyshow"¬irreducible p" using 1 by (intro reducible_polyI) qed qed
text‹ As a consequence of the full factorisation lemma proven above, we can also show that any polynomial with at least two different roots splits into two non-constant coprime factors: › lemma alg_closed_imp_poly_splits_coprime: assumes"degree (p :: 'a :: {alg_closed_field} poly) > 1" assumes"poly p x = 0""poly p y = 0""x ≠ y" obtains r s where"degree r > 0""degree s > 0""coprime r s""p = r * s" proof -
define n where"n = order x p" have"n > 0" using assms by (metis degree_0 gr0I n_def not_one_less_zero order_root) have"[:-x, 1:] ^ n dvd p" unfolding n_def by (simp add: order_1) thenobtain q where p_eq: "p = [:-x, 1:] ^ n * q" by (elim dvdE) from assms have [simp]: "q ≠ 0" by (auto simp: p_eq) have"order x p = n + Polynomial.order x q" unfolding p_eq by (subst order_mult) (auto simp: order_power_n_n) hence"Polynomial.order x q = 0" by (simp add: n_def) hence"poly q x ≠ 0" by (simp add: order_root)
show ?thesis proof (rule that) show"coprime ([:-x, 1:] ^ n) q" proof (rule coprimeI) fix d assume d: "d dvd [:-x, 1:] ^ n""d dvd q" have"degree d = 0" proof (rule ccontr) assume"¬(degree d = 0)" thenobtain z where z: "poly d z = 0" using alg_closed_imp_poly_has_root by blast moreoverfrom this and d(1) have"poly ([:-x, 1:] ^ n) z = 0" using dvd_trans poly_eq_0_iff_dvd by blast ultimatelyhave"poly d x = 0" by auto with d(2) have"poly q x = 0" using dvd_trans poly_eq_0_iff_dvd by blast with‹poly q x ≠ 0›show False by contradiction qed thus"is_unit d"using d by (metis ‹q ≠ 0› dvd_0_left is_unit_iff_degree) qed next have"poly q y = 0" using‹poly p y = 0›‹x ≠ y›by (auto simp: p_eq) with‹q ≠ 0›show"degree q > 0" using order_degree order_gt_0_iff order_less_le_trans by blast qed (use‹n > 0›in‹simp_all add: p_eq degree_power_eq›) qed
subsection‹Polynomials and limits›
lemma filterlim_poly_at_infinity: fixes p::"'a::real_normed_field poly" assumes"degree p>0" shows"filterlim (poly p) at_infinity at_infinity" using assms proof (induct p) case 0 thenshow ?caseby auto next case (pCons a p) have ?case when "degree p=0" proof - obtain c where c_def:"p=[:c:]"using‹degree p = 0› degree_eq_zeroE by blast thenhave"c≠0"using‹0 🚫 (pCons a p)›by auto thenshow ?thesis unfolding c_def apply (auto intro!:tendsto_add_filterlim_at_infinity) apply (subst mult.commute) by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident) qed moreoverhave ?case when "degree p≠0" proof - have"filterlim (poly p) at_infinity at_infinity" using that by (auto intro:pCons) thenshow ?thesis by (auto intro!:tendsto_add_filterlim_at_infinity filterlim_at_infinity_times filterlim_ident) qed ultimatelyshow ?caseby auto qed
lemma poly_divide_tendsto_aux: fixes p::"'a::real_normed_field poly" shows"((λx. poly p x/x^(degree p)) ---> lead_coeff p) at_infinity" proof (induct p) case 0 thenshow ?caseby (auto intro:tendsto_eq_intros) next case (pCons a p) have ?case when "p=0" using that by auto moreoverhave ?case when "p≠0" proof -
define g where"g=(λx. a/(x*x^degree p))"
define f where"f=(λx. poly p x/x^degree p)" have"∀🪙Fx in at_infinity. poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume"norm x≥1" thenhave"x≠0"by auto thenshow"poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" using that unfolding g_def f_def by (auto simp add:field_simps) qed moreoverhave"((λx. g x+f x) ---> lead_coeff (pCons a p)) at_infinity" proof - have"(g ---> 0) at_infinity" unfolding g_def using filterlim_poly_at_infinity[of "monom 1 (Suc (degree p))"] apply (auto intro!:tendsto_intros tendsto_divide_0 simp add: degree_monom_eq) apply (subst filterlim_cong[where g="poly (monom 1 (Suc (degree p)))"]) by (auto simp add:poly_monom) moreoverhave"(f ---> lead_coeff (pCons a p)) at_infinity" using pCons ‹p≠0›unfolding f_def by auto ultimatelyshow ?thesis by (auto intro:tendsto_eq_intros) qed ultimatelyshow ?thesis by (auto dest:tendsto_cong) qed ultimatelyshow ?caseby auto qed
lemma filterlim_power_at_infinity: assumes"n≠0" shows"filterlim (λx::'a::real_normed_field. x^n) at_infinity at_infinity" using filterlim_poly_at_infinity[of "monom 1 n"] assms by (simp add: filterlim_ident filterlim_power_at_infinity)
lemma poly_divide_tendsto_0_at_infinity: fixes p::"'a::real_normed_field poly" assumes"degree p > degree q" shows"((λx. poly q x / poly p x) ---> 0 ) at_infinity" proof -
define pp where"pp ≡ (λx. x^(degree p) / poly p x)"
define qq where"qq ≡ (λx. poly q x/x^(degree q))"
define dd where"dd ≡ (λx::'a. 1/x^(degree p - degree q))" have"∀🪙Fx in at_infinity. poly q x / poly p x = qq x * pp x * dd x" proof (rule eventually_at_infinityI[of 1]) fix x::'a assume"norm x≥1" thenhave"x≠0"by auto thenshow"poly q x / poly p x = qq x * pp x * dd x" unfolding qq_def pp_def dd_def using assms by (auto simp add:field_simps divide_simps power_diff) qed moreoverhave"((λx. qq x * pp x * dd x) ---> 0) at_infinity" proof - have"(qq ---> lead_coeff q) at_infinity" unfolding qq_def using poly_divide_tendsto_aux[of q] . moreoverhave"(pp ---> 1/lead_coeff p) at_infinity" proof - have"p≠0"using assms by auto thenshow ?thesis unfolding pp_def using poly_divide_tendsto_aux[of p] apply (drule_tac tendsto_inverse) by (auto simp add:inverse_eq_divide) qed moreoverhave"(dd ---> 0) at_infinity" unfolding dd_def apply (rule tendsto_divide_0) by (auto intro!: filterlim_power_at_infinity simp add:assms) ultimatelyshow ?thesis by (auto intro:tendsto_eq_intros) qed ultimatelyshow ?thesis by (auto dest:tendsto_cong) qed
lemma poly_eventually_not_zero: fixes p::"real poly" assumes"p≠0" shows"eventually (λx. poly p x ≠ 0) at_infinity" proof (rule eventually_at_infinityI[of "Max (norm ` {x. poly p x = 0}) + 1"]) fix x::real assume🍋: "Max (norm ` {x. poly p x = 0}) + 1 ≤ norm x" have False when "poly p x = 0" proof -
define S where"S=norm `{x. poly p x = 0}" have"norm x∈S" using that unfolding S_def by auto moreoverhave"finite S" using‹p≠0› poly_roots_finite unfolding S_def by blast ultimatelyhave"norm x≤Max S" by simp moreoverhave"Max S + 1 ≤ norm x" using🍋unfolding S_def by simp ultimatelyshow False by argo qed thenshow"poly p x ≠ 0"by auto qed
no_notation cCons (infixr‹##› 65)
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.406 Sekunden
(vorverarbeitet am 2026-04-30)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.