(* Author: René Thiemann Akihisa Yamada Jose Divason License: BSD *) section ‹Missing Polynomial› text ‹The theory contains some basic results on polynomials which have not been detected in the distribution, especially on linear factors and degrees.› theory Missing_Polynomial imports "HOL-Computational_Algebra.Polynomial_Factorial" Missing_Unsorted begin subsection ‹Basic Properties› lemma degree_0_id: assumes "degree p = 0" shows "[: coeff p 0 :] = p" proof - have "⋀ x. 0 ≠ Suc x" by auto thus ?thesis using assms by (metis coeff_pCons_0 degree_pCons_eq_if pCons_cases) qed lemma degree0_coeffs: "degree p = 0 ⟹ ∃ a. p = [: a :]" by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases) lemma degree1_coeffs: "degree p = 1 ⟹ ∃ a b. p = [: b, a :] ∧ a ≠ 0" by (metis One_nat_def degree_pCons_eq_if nat.inject old.nat.distinct(2) pCons_0_0 pCons_cases) lemma degree2_coeffs: "degree p = 2 ⟹ ∃ a b c. p = [: c, b, a :] ∧ a ≠ 0" by (metis Suc_1 Suc_neq_Zero degree1_coeffs degree_pCons_eq_if nat.inject pCons_cases) 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 lemma coeff_monom_Suc: "coeff (monom a (Suc d) * p) (Suc i) = coeff (monom a d * p) i" by (simp add: monom_Suc) 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. also have "{..d} = insert n ({..d}-{n})" using n by auto hence "sum ?cmf {..d} = sum ?cmf ..." by auto also have "... = sum ?cmf ({..d}-{n}) + ?cmf n" by (subst sum.insert,auto) also have "sum ?cmf ({..d}-{n}) = 0" by (subst sum.neutral, auto) finally show ?thesis by simp qed lemma linear_poly_root: "(a :: 'a :: comm_ring_1) ∈ set as ⟹ poly (∏ a ← as. [: - a, 1:]) a = 0" proof (induct as) case (Cons b as) show ?case proof (cases "a = b") case False with Cons have "a ∈ set as" by auto from Cons(1)[OF this] show ?thesis by simp qed simp qed simp lemma degree_lcoeff_sum: assumes deg: "degree (f q) = n" and fin: "finite S" and q: "q ∈ S" and degle: "⋀ p . p ∈ S - {q} ⟹ degree (f p) < n" and cong: "coeff (f q) n = c" shows "degree (sum f S) = n ∧ coeff (sum f S) n = c" proof (cases "S = {q}") case True thus ?thesis using deg cong by simp next case False with q obtain p where "p ∈ S - {q}" by auto from degle[OF this] have n: "n > 0" by auto have "degree (sum f S) = degree (f q + sum f (S - {q}))" unfolding sum.remove[OF fin q] .. also have "… = degree (f q)" proof (rule degree_add_eq_left) have "degree (sum f (S - {q})) ≤ n - 1" proof (rule degree_sum_le) fix p show "p ∈ S - {q} ⟹ degree (f p) ≤ n - 1" using degle[of p] by auto qed (insert fin, auto) also have "… < n" using n by simp finally show "degree (sum f (S - {q})) < degree (f q)" unfolding deg . qed finally show ?thesis unfolding deg[symmetric] cong[symmetric] proof (rule conjI) have id: "(∑x∈S - {q}. coeff (f x) (degree (f q))) = 0" by (rule sum.neutral, rule ballI, rule coeff_eq_0[OF degle[folded deg]]) show "coeff (sum f S) (degree (f q)) = coeff (f q) (degree (f q))" unfolding coeff_sum by (subst sum.remove[OF _ q], unfold id, insert fin, auto) qed qed 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 ?case unfolding 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 ?case unfolding prod_list.Cons by (rule order.trans[OF degree_mult_le], insert Cons, auto) qed simp lemma smult_sum: "smult (∑i ∈ S. f i) p = (∑i ∈ S. smult (f i) p)" by (induct S rule: infinite_finite_induct, auto simp: smult_add_left) lemma range_coeff: "range (coeff p) = insert 0 (set (coeffs p))" by (metis nth_default_coeffs_eq range_nth_default) lemma smult_power: "(smult a p) ^ n = smult (a ^ n) (p ^ n)" by (induct n, auto simp: field_simps) lemma poly_sum_list: "poly (sum_list ps) x = sum_list (map (λ p. poly p x) ps)" by (induct ps, auto) lemma poly_prod_list: "poly (prod_list ps) x = prod_list (map (λ p. poly p x) ps)" by (induct ps, auto) lemma sum_list_neutral: "(⋀ x. x ∈ set xs ⟹ x = 0) ⟹ sum_list xs = 0" by (induct xs, auto) lemma prod_list_neutral: "(⋀ x. x ∈ set xs ⟹ x = 1) ⟹ prod_list xs = 1" by (induct xs, auto) lemma (in comm_monoid_mult) prod_list_map_remove1: "x ∈ set xs ⟹ prod_list (map f xs) = f x * prod_list (map f (remove1 x xs))" by (induct xs) (auto simp add: ac_simps) lemma poly_as_sum: fixes p :: "'a::comm_semiring_1 poly" shows "poly p x = (∑i≤degree p. x ^ i * coeff p i)" unfolding poly_altdef by (simp add: ac_simps) lemma poly_prod_0: "finite ps ⟹ poly (prod f ps) x = (0 :: 'a :: field) ⟷ (∃ p ∈ ps. poly (f p) x = 0)" by (induct ps rule: finite_induct, auto) lemma coeff_monom_mult: shows "coeff (monom a d * p) i = (if d ≤ i then a * coeff p (i-d) else 0)" (is "?l = ?r") proof (cases "d ≤ i") case False thus ?thesis unfolding coeff_mult by simp next case True let ?f = "λj. coeff (monom a d) j * coeff p (i - j)" have "⋀j. j ∈ {0..i} - {d} ⟹ ?f j = 0" by auto hence "0 = (∑j ∈ {0..i} - {d}. ?f j)" by auto also have "... + ?f d = (∑j ∈ insert d ({0..i} - {d}). ?f j)" by(subst sum.insert, auto) also have "... = (∑j ∈ {0..i}. ?f j)" by (subst insert_Diff, insert True, auto) also have "... = (∑j≤i. ?f j)" by (rule sum.cong, auto) also have "... = ?l" unfolding coeff_mult .. finally show ?thesis using True by auto qed lemma poly_eqI2: assumes "degree p = degree q" and "⋀i. i ≤ degree p ⟹ coeff p i = coeff q i" shows "p = q" apply(rule poly_eqI) by (metis assms le_degree) text ‹A nice extension rule for polynomials.› lemma poly_ext[intro]: 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" apply (induct n, simp_all) apply (subst coeff_eq_0) apply (auto intro: le_less_trans degree_power_le) done lemma degree_linear_power_neg[simp]: fixes a :: "'a::{idom,comm_ring_1}" shows "degree ([:a, -1:] ^ n) = n" apply (rule order_antisym) apply (rule ord_le_eq_trans [OF degree_power_le], simp) apply (rule le_degree) unfolding coeff_linear_power_neg apply (auto) done subsection ‹Polynomial Composition› lemmas [simp] = pcompose_pCons lemma pcompose_eq_0: fixes q :: "'a :: idom poly" assumes q: "degree q ≠ 0" shows "p ∘⇩_{p}q = 0 ⟷ p = 0" proof (induct p) case 0 show ?case by auto next case (pCons a p) have id: "(pCons a p) ∘⇩_{p}q = [:a:] + q * (p ∘⇩_{p}q)" by simp show ?case proof (cases "p = 0") case True show ?thesis unfolding id unfolding True by simp next case False with pCons(2) have "p ∘⇩_{p}q ≠ 0" by auto from degree_mult_eq[OF _ this, of q] q have "degree (q * (p ∘⇩_{p}q)) ≠ 0" by force hence deg: "degree ([:a:] + q * (p ∘⇩_{p}q)) ≠ 0" by (subst degree_add_eq_right, auto) show ?thesis unfolding id using False deg by auto qed qed declare degree_pcompose[simp] subsection ‹Monic Polynomials› abbreviation monic where "monic p ≡ coeff p (degree p) = 1" lemma unit_factor_field [simp]: "unit_factor (x :: 'a :: {field,normalization_semidom}) = x" by (cases "is_unit x") (auto simp: is_unit_unit_factor dvd_field_iff) lemma poly_gcd_monic: fixes p :: "'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes "p ≠ 0 ∨ q ≠ 0" shows "monic (gcd p q)" proof - from assms have "1 = unit_factor (gcd p q)" by (auto simp: unit_factor_gcd) also have "… = [:lead_coeff (gcd p q):]" unfolding unit_factor_poly_def by (simp add: monom_0) finally show ?thesis by (metis coeff_pCons_0 degree_1 lead_coeff_1) qed lemma normalize_monic: "monic p ⟹ normalize p = p" by (simp add: normalize_poly_eq_map_poly is_unit_unit_factor) lemma lcoeff_monic_mult: assumes monic: "monic (p :: 'a :: comm_semiring_1 poly)" shows "coeff (p * q) (degree p + degree q) = coeff q (degree q)" proof - let ?pqi = "λ i. coeff p i * coeff q (degree p + degree q - i)" have "coeff (p * q) (degree p + degree q) = (∑i≤degree p + degree q. ?pqi i)" unfolding coeff_mult by simp also have "… = ?pqi (degree p) + (sum ?pqi ({.. degree p + degree q} - {degree p}))" by (subst sum.remove[of _ "degree p"], auto) also have "?pqi (degree p) = coeff q (degree q)" unfolding monic by simp also have "(sum ?pqi ({.. degree p + degree q} - {degree p})) = 0" proof (rule sum.neutral, intro ballI) fix d assume d: "d ∈ {.. degree p + degree q} - {degree p}" show "?pqi d = 0" proof (cases "d < degree p") case True hence "degree p + degree q - d > degree q" by auto hence "coeff q (degree p + degree q - d) = 0" by (rule coeff_eq_0) thus ?thesis by simp next case False with d have "d > degree p" by auto hence "coeff p d = 0" by (rule coeff_eq_0) thus ?thesis by simp qed qed finally show ?thesis by simp qed lemma degree_monic_mult: assumes monic: "monic (p :: 'a :: comm_semiring_1 poly)" and q: "q ≠ 0" shows "degree (p * q) = degree p + degree q" proof - have "degree p + degree q ≥ degree (p * q)" by (rule degree_mult_le) also have "degree p + degree q ≤ degree (p * q)" proof - from q have cq: "coeff q (degree q) ≠ 0" by auto hence "coeff (p * q) (degree p + degree q) ≠ 0" unfolding lcoeff_monic_mult[OF monic] . thus "degree (p * q) ≥ degree p + degree q" by (rule le_degree) qed finally show ?thesis . qed lemma degree_prod_sum_monic: assumes S: "finite S" and nzd: "0 ∉ (degree o f) ` S" and monic: "(⋀ a . a ∈ S ⟹ monic (f a))" shows "degree (prod f S) = (sum (degree o f) S) ∧ coeff (prod f S) (sum (degree o f) S) = 1" proof - from S nzd monic have "degree (prod f S) = sum (degree ∘ f) S ∧ (S ≠ {} ⟶ degree (prod f S) ≠ 0 ∧ prod f S ≠ 0) ∧ coeff (prod f S) (sum (degree o f) S) = 1" proof (induct S rule: finite_induct) case (insert a S) have IH1: "degree (prod f S) = sum (degree o f) S" using insert by auto have IH2: "coeff (prod f S) (degree (prod f S)) = 1" using insert by auto have id: "degree (prod f (insert a S)) = sum (degree ∘ f) (insert a S) ∧ coeff (prod f (insert a S)) (sum (degree o f) (insert a S)) = 1" proof (cases "S = {}") case False with insert have nz: "prod f S ≠ 0" by auto from insert have monic: "coeff (f a) (degree (f a)) = 1" by auto have id: "(degree ∘ f) a = degree (f a)" by simp show ?thesis unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)] id unfolding degree_monic_mult[OF monic nz] unfolding IH1[symmetric] unfolding lcoeff_monic_mult[OF monic] IH2 by simp qed (insert insert, auto) show ?case using id unfolding sum.insert[OF insert(1-2)] using insert by auto qed simp thus ?thesis by auto qed lemma degree_prod_monic: assumes "⋀ i. i < n ⟹ degree (f i :: 'a :: comm_semiring_1 poly) = 1" and "⋀ i. i < n ⟹ coeff (f i) 1 = 1" shows "degree (prod f {0 ..< n}) = n ∧ coeff (prod f {0 ..< n}) n = 1" proof - from degree_prod_sum_monic[of "{0 ..< n}" f] show ?thesis using assms by force qed lemma degree_prod_sum_lt_n: assumes "⋀ i. i < n ⟹ degree (f i :: 'a :: comm_semiring_1 poly) ≤ 1" and i: "i < n" and fi: "degree (f i) = 0" shows "degree (prod f {0 ..< n}) < n" proof - have "degree (prod f {0 ..< n}) ≤ sum (degree o f) {0 ..< n}" by (rule degree_prod_sum_le, auto) also have "sum (degree o f) {0 ..< n} = (degree o f) i + sum (degree o f) ({0 ..< n} - {i})" by (rule sum.remove, insert i, auto) also have "(degree o f) i = 0" using fi by simp also have "sum (degree o f) ({0 ..< n} - {i}) ≤ sum (λ _. 1) ({0 ..< n} - {i})" by (rule sum_mono, insert assms, auto) also have "… = n - 1" using i by simp also have "… < n" using i by simp finally show ?thesis by simp qed lemma degree_linear_factors: "degree (∏ a ← as. [: f a, 1:]) = length as" proof (induct as) case (Cons b as) note IH = this have id: "(∏a←b # as. [:f a, 1:]) = [:f b,1 :] * (∏a←as. [:f a, 1:])" by simp show ?case unfolding id by (subst degree_monic_mult, insert IH, auto) qed simp lemma monic_mult: fixes p q :: "'a :: idom poly" assumes "monic p" "monic q" shows "monic (p * q)" proof - from assms have nz: "p ≠ 0" "q ≠ 0" by auto show ?thesis unfolding degree_mult_eq[OF nz] coeff_mult_degree_sum using assms by simp qed lemma monic_factor: fixes p q :: "'a :: idom poly" assumes "monic (p * q)" "monic p" shows "monic q" proof - from assms have nz: "p ≠ 0" "q ≠ 0" by auto from assms[unfolded degree_mult_eq[OF nz] coeff_mult_degree_sum ‹monic p›] show ?thesis by simp qed lemma monic_prod: fixes f :: "'a ⇒ 'b :: idom poly" assumes "⋀ a. a ∈ as ⟹ monic (f a)" shows "monic (prod f as)" using assms proof (induct as rule: infinite_finite_induct) case (insert a as) hence id: "prod f (insert a as) = f a * prod f as" and *: "monic (f a)" "monic (prod f as)" by auto show ?case unfolding id by (rule monic_mult[OF *]) qed auto lemma monic_prod_list: fixes as :: "'a :: idom poly list" assumes "⋀ a. a ∈ set as ⟹ monic a" shows "monic (prod_list as)" using assms by (induct as, auto intro: monic_mult) lemma monic_power: assumes "monic (p :: 'a :: idom poly)" shows "monic (p ^ n)" by (induct n, insert assms, auto intro: monic_mult) lemma monic_prod_list_pow: "monic (∏(x::'a::idom, i)←xis. [:- x, 1:] ^ Suc i)" proof (rule monic_prod_list, goal_cases) case (1 a) then obtain x i where a: "a = [:-x, 1:]^Suc i" by force show "monic a" unfolding a by (rule monic_power, auto) qed lemma monic_degree_0: "monic p ⟹ (degree p = 0) = (p = 1)" using le_degree poly_eq_iff by force subsection ‹Roots› text ‹The following proof structure is completely similar to the one of @{thm poly_roots_finite}.› lemma poly_roots_degree: fixes p :: "'a::idom poly" shows "p ≠ 0 ⟹ card {x. poly p x = 0} ≤ degree p" proof (induct n ≡ "degree p" arbitrary: p) case (0 p) then obtain a where "a ≠ 0" and "p = [:a:]" by (cases p, simp split: if_splits) then show ?case by simp next case (Suc n p) show ?case proof (cases "∃x. poly p x = 0") case True then obtain a where a: "poly p a = 0" .. then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) then obtain 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 Suc.hyps(1)[OF this ‹k ≠ 0›] have le: "card {x. poly k x = 0} ≤ degree k" . have "card {x. poly p x = 0} = card {x. poly ([:-a, 1:] * k) x = 0}" unfolding k .. also have "{x. poly ([:-a, 1:] * k) x = 0} = insert a {x. poly k x = 0}" by auto also have "card … ≤ Suc (card {x. poly k x = 0})" unfolding card_insert_if[OF poly_roots_finite[OF ‹k ≠ 0›]] by simp also have "… ≤ Suc (degree k)" using le by auto finally show ?thesis using ‹degree p = Suc (degree k)› by simp qed simp qed lemma poly_root_factor: "(poly ([: r, 1:] * q) (k :: 'a :: idom) = 0) = (k = -r ∨ poly q k = 0)" (is ?one) "(poly (q * [: r, 1:]) k = 0) = (k = -r ∨ poly q k = 0)" (is ?two) "(poly [: r, 1 :] k = 0) = (k = -r)" (is ?three) proof - have [simp]: "r + k = 0 ⟹ k = - r" by (simp add: minus_unique) show ?one unfolding poly_mult by auto show ?two unfolding poly_mult by auto show ?three by auto qed lemma poly_root_constant: "c ≠ 0 ⟹ (poly (p * [:c:]) (k :: 'a :: idom) = 0) = (poly p k = 0)" unfolding poly_mult by auto lemma poly_linear_exp_linear_factors_rev: "([:b,1:])^(length (filter ((=) b) as)) dvd (∏ (a :: 'a :: comm_ring_1) ← as. [: a, 1:])" proof (induct as) case (Cons a as) let ?ls = "length (filter ((=) b) (a # as))" let ?l = "length (filter ((=) b) as)" have prod: "(∏ a ← Cons a as. [: a, 1:]) = [: a, 1 :] * (∏ a ← as. [: a, 1:])" by simp show ?case proof (cases "a = b") case False hence len: "?ls = ?l" by simp show ?thesis unfolding prod len using Cons by (rule dvd_mult) next case True hence len: "[: b, 1 :] ^ ?ls = [: a, 1 :] * [: b, 1 :] ^ ?l" by simp show ?thesis unfolding prod len using Cons using dvd_refl mult_dvd_mono by blast qed qed simp lemma order_max: assumes dvd: "[: -a, 1 :] ^ k dvd p" and p: "p ≠ 0" shows "k ≤ order a p" proof (rule ccontr) assume "¬ ?thesis" hence "∃ j. k = Suc (order a p + j)" by arith then obtain j where k: "k = Suc (order a p + j)" by auto have "[: -a, 1 :] ^ Suc (order a p) dvd p" by (rule power_le_dvd[OF dvd[unfolded k]], simp) with order_2[OF p, of a] show False by blast qed subsection ‹Divisibility› context assumes "SORT_CONSTRAINT('a :: idom)" begin lemma poly_linear_linear_factor: assumes dvd: "[:b,1:] dvd (∏ (a :: 'a) ← as. [: a, 1:])" shows "b ∈ set as" proof - let ?p = "λ as. (∏ a ← as. [: a, 1:])" let ?b = "[:b,1:]" from assms[unfolded dvd_def] obtain p where id: "?p as = ?b * p" .. from arg_cong[OF id, of "λ p. poly p (-b)"] have "poly (?p as) (-b) = 0" by simp thus ?thesis proof (induct as) case (Cons a as) have "?p (a # as) = [:a,1:] * ?p as" by simp from Cons(2)[unfolded this] have "poly (?p as) (-b) = 0 ∨ (a - b) = 0" by simp with Cons(1) show ?case by auto qed simp qed lemma poly_linear_exp_linear_factors: assumes dvd: "([:b,1:])^n dvd (∏ (a :: 'a) ← as. [: a, 1:])" shows "length (filter ((=) b) as) ≥ n" proof - let ?p = "λ as. (∏ a ← as. [: a, 1:])" let ?b = "[:b,1:]" from dvd show ?thesis proof (induct n arbitrary: as) case (Suc n as) have bs: "?b ^ Suc n = ?b * ?b ^ n" by simp from poly_linear_linear_factor[OF dvd_mult_left[OF Suc(2)[unfolded bs]], unfolded in_set_conv_decomp] obtain as1 as2 where as: "as = as1 @ b # as2" by auto have "?p as = [:b,1:] * ?p (as1 @ as2)" unfolding as proof (induct as1) case (Cons a as1) have "?p (a # as1 @ b # as2) = [:a,1:] * ?p (as1 @ b # as2)" by simp also have "?p (as1 @ b # as2) = [:b,1:] * ?p (as1 @ as2)" unfolding Cons by simp also have "[:a,1:] * … = [:b,1:] * ([:a,1:] * ?p (as1 @ as2))" by (metis (no_types, lifting) mult.left_commute) finally show ?case by simp qed simp from Suc(2)[unfolded bs this dvd_mult_cancel_left] have "?b ^ n dvd ?p (as1 @ as2)" by simp from Suc(1)[OF this] show ?case unfolding as by simp qed simp qed end lemma const_poly_dvd: "([:a:] dvd [:b:]) = (a dvd b)" proof assume "a dvd b" then obtain c where "b = a * c" unfolding dvd_def by auto hence "[:b:] = [:a:] * [: c:]" by (auto simp: ac_simps) thus "[:a:] dvd [:b:]" unfolding dvd_def by blast next assume "[:a:] dvd [:b:]" then obtain pc where "[:b:] = [:a:] * pc" unfolding dvd_def by blast from arg_cong[OF this, of "λ p. coeff p 0", unfolded coeff_mult] have "b = a * coeff pc 0" by auto thus "a dvd b" unfolding dvd_def by blast qed lemma const_poly_dvd_1 [simp]: "[:a:] dvd 1 ⟷ a dvd 1" by (metis const_poly_dvd one_poly_eq_simps(2)) lemma poly_dvd_1: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" shows "p dvd 1 ⟷ degree p = 0 ∧ coeff p 0 dvd 1" proof (cases "degree p = 0") case False with divides_degree[of p 1] show ?thesis by auto next case True from degree0_coeffs[OF this] obtain a where p: "p = [:a:]" by auto show ?thesis unfolding p by auto qed text ‹Degree based version of irreducibility.› definition irreducible⇩_{d}:: "'a :: comm_semiring_1 poly ⇒ bool" where "irreducible⇩_{d}p = (degree p > 0 ∧ (∀ q r. degree q < degree p ⟶ degree r < degree p ⟶ p ≠ q * r))" lemma irreducible⇩_{d}I [intro]: assumes 1: "degree p > 0" and 2: "⋀q r. degree q > 0 ⟹ degree q < degree p ⟹ degree r > 0 ⟹ degree r < degree p ⟹ p = q * r ⟹ False" shows "irreducible⇩_{d}p" proof (unfold irreducible⇩_{d}_def, intro conjI allI impI notI 1) fix q r assume "degree q < degree p" and "degree r < degree p" and "p = q * r" with degree_mult_le[of q r] show False by (intro 2, auto) qed lemma irreducible⇩_{d}I2: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes deg: "degree p > 0" and ndvd: "⋀ q. degree q > 0 ⟹ degree q ≤ degree p div 2 ⟹ ¬ q dvd p" shows "irreducible⇩_{d}p" proof (rule ccontr) assume "¬ ?thesis" from this[unfolded irreducible⇩_{d}_def] deg obtain q r where dq: "degree q < degree p" and dr: "degree r < degree p" and p: "p = q * r" by auto from deg have p0: "p ≠ 0" by auto with p have "q ≠ 0" "r ≠ 0" by auto from degree_mult_eq[OF this] p have dp: "degree p = degree q + degree r" by simp show False proof (cases "degree q ≤ degree p div 2") case True from ndvd[OF _ True] dq dr dp p show False by auto next case False with dp have dr: "degree r ≤ degree p div 2" by auto from p have dvd: "r dvd p" by auto from ndvd[OF _ dr] dvd dp dq show False by auto qed qed lemma reducible⇩_{d}I: assumes "degree p > 0 ⟹ ∃q r. degree q < degree p ∧ degree r < degree p ∧ p = q * r" shows "¬ irreducible⇩_{d}p" using assms by (auto simp: irreducible⇩_{d}_def) lemma irreducible⇩_{d}E [elim]: assumes "irreducible⇩_{d}p" and "degree p > 0 ⟹ (⋀q r. degree q < degree p ⟹ degree r < degree p ⟹ p ≠ q * r) ⟹ thesis" shows thesis using assms by (auto simp: irreducible⇩_{d}_def) lemma reducible⇩_{d}E [elim]: assumes red: "¬ irreducible⇩_{d}p" and 1: "degree p = 0 ⟹ thesis" and 2: "⋀q r. degree q > 0 ⟹ degree q < degree p ⟹ degree r > 0 ⟹ degree r < degree p ⟹ p = q * r ⟹ thesis" shows thesis using red[unfolded irreducible⇩_{d}_def de_Morgan_conj not_not not_all not_imp] proof (elim disjE exE conjE) show "¬degree p > 0 ⟹ thesis" using 1 by auto next fix q r assume "degree q < degree p" and "degree r < degree p" and "p = q * r" with degree_mult_le[of q r] show thesis by (intro 2, auto) qed lemma irreducible⇩_{d}D: assumes "irreducible⇩_{d}p" shows "degree p > 0" "⋀q r. degree q < degree p ⟹ degree r < degree p ⟹ p ≠ q * r" using assms unfolding irreducible⇩_{d}_def by auto theorem irreducible⇩_{d}_factorization_exists: assumes "degree p > 0" shows "∃fs. fs ≠ [] ∧ (∀f ∈ set fs. irreducible⇩_{d}f ∧ degree f ≤ degree p) ∧ p = prod_list fs" and "¬irreducible⇩_{d}p ⟹ ∃fs. length fs > 1 ∧ (∀f ∈ set fs. irreducible⇩_{d}f ∧ degree f < degree p) ∧ p = prod_list fs" proof (atomize(full), insert assms, induct "degree p" arbitrary:p rule: less_induct) case less then have deg_f: "degree p > 0" by auto show ?case proof (cases "irreducible⇩_{d}p") case True then have "set [p] ⊆ Collect irreducible⇩_{d}" "p = prod_list [p]" by auto with True show ?thesis by (auto intro: exI[of _ "[p]"]) next case False with deg_f obtain g h where deg_g: "degree g < degree p" "degree g > 0" and deg_h: "degree h < degree p" "degree h > 0" and f_gh: "p = g * h" by auto from less.hyps[OF deg_g] less.hyps[OF deg_h] obtain gs hs where emp: "length gs > 0" "length hs > 0" and "∀f ∈ set gs. irreducible⇩_{d}f ∧ degree f ≤ degree g" "g = prod_list gs" and "∀f ∈ set hs. irreducible⇩_{d}f ∧ degree f ≤ degree h" "h = prod_list hs" by auto with f_gh deg_g deg_h have len: "length (gs@hs) > 1" and mem: "∀f ∈ set (gs@hs). irreducible⇩_{d}f ∧ degree f < degree p" and p: "p = prod_list (gs@hs)" by (auto simp del: length_greater_0_conv) with False show ?thesis by (auto intro!: exI[of _ "gs@hs"] simp: less_imp_le) qed qed lemma irreducible⇩_{d}_factor: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "degree p > 0" shows "∃ q r. irreducible⇩_{d}q ∧ p = q * r ∧ degree r < degree p" using assms proof (induct "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "irreducible⇩_{d}p") case False with less(2) obtain q r where q: "degree q < degree p" "degree q > 0" and r: "degree r < degree p" "degree r > 0" and p: "p = q * r" by auto from less(1)[OF q] obtain s t where IH: "irreducible⇩_{d}s" "q = s * t" by auto from p have p: "p = s * (t * r)" unfolding IH by (simp add: ac_simps) from less(2) have "p ≠ 0" by auto hence "degree p = degree s + (degree (t * r))" unfolding p by (subst degree_mult_eq, insert p, auto) with irreducible⇩_{d}D[OF IH(1)] have "degree p > degree (t * r)" by auto with p IH show ?thesis by auto next case True show ?thesis by (rule exI[of _ p], rule exI[of _ 1], insert True less(2), auto) qed qed context mult_zero begin (* least class with times and zero *) definition zero_divisor where "zero_divisor a ≡ ∃b. b ≠ 0 ∧ a * b = 0" lemma zero_divisorI[intro]: assumes "b ≠ 0" and "a * b = 0" shows "zero_divisor a" using assms by (auto simp: zero_divisor_def) lemma zero_divisorE[elim]: assumes "zero_divisor a" and "⋀b. b ≠ 0 ⟹ a * b = 0 ⟹ thesis" shows thesis using assms by (auto simp: zero_divisor_def) end lemma zero_divisor_0[simp]: "zero_divisor (0::'a::{mult_zero,zero_neq_one})" (* No need for one! *) by (auto intro!: zero_divisorI[of 1]) lemma not_zero_divisor_1: "¬ zero_divisor (1 :: 'a :: {monoid_mult,mult_zero})" (* No need for associativity! *) by auto lemma zero_divisor_iff_eq_0[simp]: fixes a :: "'a :: {semiring_no_zero_divisors, zero_neq_one}" shows "zero_divisor a ⟷ a = 0" by auto lemma mult_eq_0_not_zero_divisor_left[simp]: fixes a b :: "'a :: mult_zero" assumes "¬ zero_divisor a" shows "a * b = 0 ⟷ b = 0" using assms unfolding zero_divisor_def by force lemma mult_eq_0_not_zero_divisor_right[simp]: fixes a b :: "'a :: {ab_semigroup_mult,mult_zero}" (* No need for associativity! *) assumes "¬ zero_divisor b" shows "a * b = 0 ⟷ a = 0" using assms unfolding zero_divisor_def by (force simp: ac_simps) lemma degree_smult_not_zero_divisor_left[simp]: assumes "¬ zero_divisor c" shows "degree (smult c p) = degree p" proof(cases "p = 0") case False then have "coeff (smult c p) (degree p) ≠ 0" using assms by auto from le_degree[OF this] degree_smult_le[of c p] show ?thesis by auto qed auto lemma degree_smult_not_zero_divisor_right[simp]: assumes "¬ zero_divisor (lead_coeff p)" shows "degree (smult c p) = (if c = 0 then 0 else degree p)" proof(cases "c = 0") case False then have "coeff (smult c p) (degree p) ≠ 0" using assms by auto from le_degree[OF this] degree_smult_le[of c p] show ?thesis by auto qed auto lemma irreducible⇩_{d}_smult_not_zero_divisor_left: assumes c0: "¬ zero_divisor c" assumes L: "irreducible⇩_{d}(smult c p)" shows "irreducible⇩_{d}p" proof (intro irreducible⇩_{d}I) from L have "degree (smult c p) > 0" by auto also note degree_smult_le finally show "degree p > 0" by auto fix q r assume deg_q: "degree q < degree p" and deg_r: "degree r < degree p" and p_qr: "p = q * r" then have 1: "smult c p = smult c q * r" by auto note degree_smult_le[of c q] also note deg_q finally have 2: "degree (smult c q) < degree (smult c p)" using c0 by auto from deg_r have 3: "degree r < …" using c0 by auto from irreducible⇩_{d}D(2)[OF L 2 3] 1 show False by auto qed lemmas irreducible⇩_{d}_smultI = irreducible⇩_{d}_smult_not_zero_divisor_left [where 'a = "'a :: {comm_semiring_1,semiring_no_zero_divisors}", simplified] lemma irreducible⇩_{d}_smult_not_zero_divisor_right: assumes p0: "¬ zero_divisor (lead_coeff p)" and L: "irreducible⇩_{d}(smult c p)" shows "irreducible⇩_{d}p" proof- from L have "c ≠ 0" by auto with p0 have [simp]: "degree (smult c p) = degree p" by simp show "irreducible⇩_{d}p" proof (intro iffI irreducible⇩_{d}I conjI) from L show "degree p > 0" by auto fix q r assume deg_q: "degree q < degree p" and deg_r: "degree r < degree p" and p_qr: "p = q * r" then have 1: "smult c p = smult c q * r" by auto note degree_smult_le[of c q] also note deg_q finally have 2: "degree (smult c q) < degree (smult c p)" by simp from deg_r have 3: "degree r < …" by simp from irreducible⇩_{d}D(2)[OF L 2 3] 1 show False by auto qed qed lemma zero_divisor_mult_left: fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}" assumes "zero_divisor a" shows "zero_divisor (a * b)" proof- from assms obtain c where c0: "c ≠ 0" and [simp]: "a * c = 0" by auto have "a * b * c = a * c * b" by (simp only: ac_simps) with c0 show ?thesis by auto qed lemma zero_divisor_mult_right: fixes a b :: "'a :: {semigroup_mult, mult_zero}" assumes "zero_divisor b" shows "zero_divisor (a * b)" proof- from assms obtain c where c0: "c ≠ 0" and [simp]: "b * c = 0" by auto have "a * b * c = a * (b * c)" by (simp only: ac_simps) with c0 show ?thesis by auto qed lemma not_zero_divisor_mult: fixes a b :: "'a :: {ab_semigroup_mult, mult_zero}" assumes "¬ zero_divisor (a * b)" shows "¬ zero_divisor a" and "¬ zero_divisor b" using assms by (auto dest: zero_divisor_mult_right zero_divisor_mult_left) lemma zero_divisor_smult_left: assumes "zero_divisor a" shows "zero_divisor (smult a f)" proof- from assms obtain b where b0: "b ≠ 0" and "a * b = 0" by auto then have "smult a f * [:b:] = 0" by (simp add: ac_simps) with b0 show ?thesis by (auto intro!: zero_divisorI[of "[:b:]"]) qed lemma unit_not_zero_divisor: fixes a :: "'a :: {comm_monoid_mult, mult_zero}" assumes "a dvd 1" shows "¬zero_divisor a" proof from assms obtain b where ab: "1 = a * b" by (elim dvdE) assume "zero_divisor a" then have "zero_divisor (1::'a)" by (unfold ab, intro zero_divisor_mult_left) then show False by auto qed lemma linear_irreducible⇩_{d}: assumes "degree p = 1" shows "irreducible⇩_{d}p" by (rule irreducible⇩_{d}I, insert assms, auto) lemma irreducible⇩_{d}_dvd_smult: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "degree p > 0" "irreducible⇩_{d}q" "p dvd q" shows "∃ c. c ≠ 0 ∧ q = smult c p" proof - from assms obtain r where q: "q = p * r" by (elim dvdE, auto) from degree_mult_eq[of p r] assms(1) q have "¬ degree p < degree q" and nz: "p ≠ 0" "q ≠ 0" apply (metis assms(2) degree_mult_eq_0 gr_implies_not_zero irreducible⇩_{d}D(2) less_add_same_cancel2) using assms by auto hence deg: "degree p ≥ degree q" by auto from ‹p dvd q› obtain k where q: "q = k * p" unfolding dvd_def by (auto simp: ac_simps) with nz have "k ≠ 0" by auto from deg[unfolded q degree_mult_eq[OF ‹k ≠ 0› ‹p ≠ 0› ]] have "degree k = 0" unfolding q by auto then obtain c where k: "k = [: c :]" by (metis degree_0_id) with ‹k ≠ 0› have "c ≠ 0" by auto have "q = smult c p" unfolding q k by simp with ‹c ≠ 0› show ?thesis by auto qed subsection ‹Map over Polynomial Coefficients› lemma map_poly_simps: shows "map_poly f (pCons c p) = (if c = 0 ∧ p = 0 then 0 else pCons (f c) (map_poly f p))" proof (cases "c = 0") case True note c0 = this show ?thesis proof (cases "p = 0") case True thus ?thesis using c0 unfolding map_poly_def by simp next case False thus ?thesis unfolding map_poly_def by auto qed next case False thus ?thesis unfolding map_poly_def by auto qed lemma map_poly_pCons[simp]: assumes "c ≠ 0 ∨ p ≠ 0" shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" unfolding map_poly_simps using assms by auto lemma map_poly_map_poly: assumes f0: "f 0 = 0" shows "map_poly f (map_poly g p) = map_poly (f ∘ g) p" proof (induct p) case (pCons a p) show ?case proof(cases "g a ≠ 0 ∨ map_poly g p ≠ 0") case True show ?thesis unfolding map_poly_pCons[OF pCons(1)] unfolding map_poly_pCons[OF True] unfolding pCons(2) by simp next case False then show ?thesis unfolding map_poly_pCons[OF pCons(1)] unfolding pCons(2)[symmetric] by (simp add: f0) qed qed simp lemma map_poly_zero: assumes f: "∀c. f c = 0 ⟶ c = 0" shows [simp]: "map_poly f p = 0 ⟷ p = 0" by (induct p; auto simp: map_poly_simps f) lemma map_poly_add: assumes h0: "h 0 = 0" and h_add: "∀p q. h (p + q) = h p + h q" shows "map_poly h (p + q) = map_poly h p + map_poly h q" proof (induct p arbitrary: q) case (pCons a p) note pIH = this show ?case proof(induct "q") case (pCons b q) note qIH = this show ?case unfolding map_poly_pCons[OF qIH(1)] unfolding map_poly_pCons[OF pIH(1)] unfolding add_pCons unfolding pIH(2)[symmetric] unfolding h_add[rule_format,symmetric] unfolding map_poly_simps using h0 by auto qed auto qed auto subsection ‹Morphismic properties of @{term "pCons 0"}› lemma monom_pCons_0_monom: "monom (pCons 0 (monom a n)) d = map_poly (pCons 0) (monom (monom a n) d)" apply (induct d) unfolding monom_0 unfolding map_poly_simps apply simp unfolding monom_Suc map_poly_simps by auto lemma pCons_0_add: "pCons 0 (p + q) = pCons 0 p + pCons 0 q" by auto lemma sum_pCons_0_commute: "sum (λi. pCons 0 (f i)) S = pCons 0 (sum f S)" by(induct S rule: infinite_finite_induct;simp) lemma pCons_0_as_mult: fixes p:: "'a :: comm_semiring_1 poly" shows "pCons 0 p = [:0,1:] * p" by auto subsection ‹Misc› fun expand_powers :: "(nat × 'a)list ⇒ 'a list" where "expand_powers [] = []" | "expand_powers ((Suc n, a) # ps) = a # expand_powers ((n,a) # ps)" | "expand_powers ((0,a) # ps) = expand_powers ps" lemma expand_powers: fixes f :: "'a ⇒ 'b :: comm_ring_1" shows "(∏ (n,a) ← n_as. f a ^ n) = (∏ a ← expand_powers n_as. f a)" by (rule sym, induct n_as rule: expand_powers.induct, auto) lemma poly_smult_zero_iff: fixes x :: "'a :: idom" shows "(poly (smult a p) x = 0) = (a = 0 ∨ poly p x = 0)" by simp lemma poly_prod_list_zero_iff: fixes x :: "'a :: idom" shows "(poly (prod_list ps) x = 0) = (∃ p ∈ set ps. poly p x = 0)" by (induct ps, auto) lemma poly_mult_zero_iff: fixes x :: "'a :: idom" shows "(poly (p * q) x = 0) = (poly p x = 0 ∨ poly q x = 0)" by simp lemma poly_power_zero_iff: fixes x :: "'a :: idom" shows "(poly (p^n) x = 0) = (n ≠ 0 ∧ poly p x = 0)" by (cases n, auto) lemma sum_monom_0_iff: assumes fin: "finite S" and g: "⋀ i j. g i = g j ⟹ i = j" shows "sum (λ i. monom (f i) (g i)) S = 0 ⟷ (∀ i ∈ S. f i = 0)" (is "?l = ?r") proof - { assume "¬ ?r" then obtain i where i: "i ∈ S" and fi: "f i ≠ 0" by auto let ?g = "λ i. monom (f i) (g i)" have "coeff (sum ?g S) (g i) = f i + sum (λ j. coeff (?g j) (g i)) (S - {i})" by (unfold sum.remove[OF fin i], simp add: coeff_sum) also have "sum (λ j. coeff (?g j) (g i)) (S - {i}) = 0" by (rule sum.neutral, insert g, auto) finally have "coeff (sum ?g S) (g i) ≠ 0" using fi by auto hence "¬ ?l" by auto } thus ?thesis by auto qed lemma degree_prod_list_eq: assumes "⋀ p. p ∈ set ps ⟹ (p :: 'a :: idom poly) ≠ 0" shows "degree (prod_list ps) = sum_list (map degree ps)" using assms proof (induct ps) case (Cons p ps) show ?case unfolding prod_list.Cons by (subst degree_mult_eq, insert Cons, auto simp: prod_list_zero_iff) qed simp lemma degree_power_eq: assumes p: "p ≠ 0" shows "degree (p ^ n) = degree (p :: 'a :: idom poly) * n" proof (induct n) case (Suc n) from p have pn: "p ^ n ≠ 0" by auto show ?case using degree_mult_eq[OF p pn] Suc by auto qed simp lemma coeff_Poly: "coeff (Poly xs) i = (nth_default 0 xs i)" unfolding nth_default_coeffs_eq[of "Poly xs", symmetric] coeffs_Poly by simp lemma rsquarefree_def': "rsquarefree p = (p ≠ 0 ∧ (∀a. order a p ≤ 1))" proof - have "⋀ a. order a p ≤ 1 ⟷ order a p = 0 ∨ order a p = 1" by linarith thus ?thesis unfolding rsquarefree_def by auto qed lemma order_prod_list: "(⋀ p. p ∈ set ps ⟹ p ≠ 0) ⟹ order x (prod_list ps) = sum_list (map (order x) ps)" by (induct ps, auto, subst order_mult, auto simp: prod_list_zero_iff) lemma irreducible⇩_{d}_dvd_eq: fixes a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "irreducible⇩_{d}a" and "irreducible⇩_{d}b" and "a dvd b" and "monic a" and "monic b" shows "a = b" using assms by (metis (no_types, lifting) coeff_smult degree_smult_eq irreducible⇩_{d}D(1) irreducible⇩_{d}_dvd_smult mult.right_neutral smult_1_left) lemma monic_gcd_dvd: assumes fg: "f dvd g" and mon: "monic f" and gcd: "gcd g h ∈ {1, g}" shows "gcd f h ∈ {1, f}" proof (cases "coprime g h") case True with dvd_refl have "coprime f h" using fg by (blast intro: coprime_divisors) then show ?thesis by simp next case False with gcd have gcd: "gcd g h = g" by (simp add: coprime_iff_gcd_eq_1) with fg have "f dvd gcd g h" by simp then have "f dvd h" by simp then have "gcd f h = normalize f" by (simp add: gcd_proj1_iff) also have "normalize f = f" using mon by (rule normalize_monic) finally show ?thesis by simp qed lemma monom_power: "(monom a b)^n = monom (a^n) (b*n)" by (induct n, auto simp add: mult_monom) lemma poly_const_pow: "[:a:]^b = [:a^b:]" by (metis Groups.mult_ac(2) monom_0 monom_power mult_zero_right) lemma degree_pderiv_le: "degree (pderiv f) ≤ degree f - 1" proof (rule ccontr) assume "¬ ?thesis" hence ge: "degree (pderiv f) ≥ Suc (degree f - 1)" by auto hence "pderiv f ≠ 0" by auto hence "coeff (pderiv f) (degree (pderiv f)) ≠ 0" by auto from this[unfolded coeff_pderiv] have "coeff f (Suc (degree (pderiv f))) ≠ 0" by auto moreover have "Suc (degree (pderiv f)) > degree f" using ge by auto ultimately show False by (simp add: coeff_eq_0) qed lemma map_div_is_smult_inverse: "map_poly (λx. x / (a :: 'a :: field)) p = smult (inverse a) p" unfolding smult_conv_map_poly by (simp add: divide_inverse_commute) lemma normalize_poly_old_def: "normalize (f :: 'a :: {normalization_semidom,field} poly) = smult (inverse (unit_factor (lead_coeff f))) f" by (simp add: normalize_poly_eq_map_poly map_div_is_smult_inverse) (* was in Euclidean_Algorithm in Number_Theory before, but has been removed *) lemma poly_dvd_antisym: fixes p q :: "'b::idom poly" assumes coeff: "coeff p (degree p) = coeff q (degree q)" assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" proof (cases "p = 0") case True with coeff show "p = q" by simp next case False with coeff have "q ≠ 0" by auto have degree: "degree p = degree q" using ‹p dvd q› ‹q dvd p› ‹p ≠ 0› ‹q ≠ 0› by (intro order_antisym dvd_imp_degree_le) from ‹p dvd q› obtain a where a: "q = p * a" .. with ‹q ≠ 0› have "a ≠ 0" by auto with degree a ‹p ≠ 0› have "degree a = 0" by (simp add: degree_mult_eq) with coeff a show "p = q" by (cases a, auto split: if_splits) qed lemma coeff_f_0_code[code_unfold]: "coeff f 0 = (case coeffs f of [] ⇒ 0 | x # _ ⇒ x)" by (cases f, auto simp: cCons_def) lemma poly_compare_0_code[code_unfold]: "(f = 0) = (case coeffs f of [] ⇒ True | _ ⇒ False)" using coeffs_eq_Nil list.disc_eq_case(1) by blast text ‹Getting more efficient code for abbreviation @{term lead_coeff}"› definition leading_coeff where [code_abbrev, simp]: "leading_coeff = lead_coeff" lemma leading_coeff_code [code]: "leading_coeff f = (let xs = coeffs f in if xs = [] then 0 else last xs)" by (simp add: last_coeffs_eq_coeff_degree) lemma nth_coeffs_coeff: "i < length (coeffs f) ⟹ coeffs f ! i = coeff f i" by (metis nth_default_coeffs_eq nth_default_def) definition monom_mult :: "nat ⇒ 'a :: comm_semiring_1 poly ⇒ 'a poly" where "monom_mult n f = monom 1 n * f" lemma monom_mult_unfold [code_unfold]: "monom 1 n * f = monom_mult n f" "f * monom 1 n = monom_mult n f" by (auto simp: monom_mult_def ac_simps) lemma monom_mult_code [code abstract]: "coeffs (monom_mult n f) = (let xs = coeffs f in if xs = [] then xs else replicate n 0 @ xs)" by (rule coeffs_eqI) (auto simp add: Let_def monom_mult_def coeff_monom_mult nth_default_append nth_default_coeffs_eq) lemma coeff_pcompose_monom: fixes f :: "'a :: comm_ring_1 poly" assumes n: "j < n" shows "coeff (f ∘⇩_{p}monom 1 n) (n * i + j) = (if j = 0 then coeff f i else 0)" proof (induct f arbitrary: i) case (pCons a f i) note d = pcompose_pCons coeff_add coeff_monom_mult coeff_pCons show ?case proof (cases i) case 0 show ?thesis unfolding d 0 using n by (cases j, auto) next case (Suc ii) have id: "n * Suc ii + j - n = n * ii + j" using n by (simp add: diff_mult_distrib2) have id1: "(n ≤ n * Suc ii + j) = True" by auto have id2: "(case n * Suc ii + j of 0 ⇒ a | Suc x ⇒ coeff 0 x) = 0" using n by (cases "n * Suc ii + j", auto) show ?thesis unfolding d Suc id id1 id2 pCons(2) if_True by auto qed qed auto lemma coeff_pcompose_x_pow_n: fixes f :: "'a :: comm_ring_1 poly" assumes n: "n ≠ 0" shows "coeff (f ∘⇩_{p}monom 1 n) (n * i) = coeff f i" using coeff_pcompose_monom[of 0 n f i] n by auto lemma dvd_dvd_smult: "a dvd b ⟹ f dvd g ⟹ smult a f dvd smult b g" unfolding dvd_def by (metis mult_smult_left mult_smult_right smult_smult) definition sdiv_poly :: "'a :: idom_divide poly ⇒ 'a ⇒ 'a poly" where "sdiv_poly p a = (map_poly (λ c. c div a) p)" lemma smult_map_poly: "smult a = map_poly ((*) a)" by (rule ext, rule poly_eqI, subst coeff_map_poly, auto) lemma smult_exact_sdiv_poly: assumes "⋀ c. c ∈ set (coeffs p) ⟹ a dvd c" shows "smult a (sdiv_poly p a) = p" unfolding smult_map_poly sdiv_poly_def by (subst map_poly_map_poly,simp,rule map_poly_idI, insert assms, auto) lemma coeff_sdiv_poly: "coeff (sdiv_poly f a) n = coeff f n div a" unfolding sdiv_poly_def by (rule coeff_map_poly, auto) lemma poly_pinfty_ge: fixes p :: "real poly" assumes "lead_coeff p > 0" "degree p ≠ 0" shows "∃n. ∀ x ≥ n. poly p x ≥ b" proof - let ?p = "p - [:b - lead_coeff p :]" have id: "lead_coeff ?p = lead_coeff p" using assms(2) by (cases p, auto) with assms(1) have "lead_coeff ?p > 0" by auto from poly_pinfty_gt_lc[OF this, unfolded id] obtain n where "⋀ x. x ≥ n ⟹ 0 ≤ poly p x - b" by auto thus ?thesis by auto qed lemma pderiv_sum: "pderiv (sum f I) = sum (λ i. (pderiv (f i))) I" by (induct I rule: infinite_finite_induct, auto simp: pderiv_add) lemma smult_sum2: "smult m (∑i ∈ S. f i) = (∑i ∈ S. smult m (f i))" by (induct S rule: infinite_finite_induct, auto simp add: smult_add_right) lemma degree_mult_not_eq: "degree (f * g) ≠ degree f + degree g ⟹ lead_coeff f * lead_coeff g = 0" by (rule ccontr, auto simp: coeff_mult_degree_sum degree_mult_le le_antisym le_degree) lemma irreducible⇩_{d}_multD: fixes a b :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes l: "irreducible⇩_{d}(a*b)" shows "degree a = 0 ∧ a ≠ 0 ∧ irreducible⇩_{d}b ∨ degree b = 0 ∧ b ≠ 0 ∧ irreducible⇩_{d}a" proof- from l have a0: "a ≠ 0" and b0: "b ≠ 0" by auto note [simp] = degree_mult_eq[OF this] from l have "degree a = 0 ∨ degree b = 0" apply (unfold irreducible⇩_{d}_def) by force then show ?thesis proof(elim disjE) assume a: "degree a = 0" with l a0 have "irreducible⇩_{d}b" by (simp add: irreducible⇩_{d}_def) (metis degree_mult_eq degree_mult_eq_0 mult.left_commute plus_nat.add_0) with a a0 show ?thesis by auto next assume b: "degree b = 0" with l b0 have "irreducible⇩_{d}a" unfolding irreducible⇩_{d}_def by (smt add_cancel_left_right degree_mult_eq degree_mult_eq_0 neq0_conv semiring_normalization_rules(16)) with b b0 show ?thesis by auto qed qed lemma irreducible_connect_field[simp]: fixes f :: "'a :: field poly" shows "irreducible⇩_{d}f = irreducible f" (is "?l = ?r") proof show "?r ⟹ ?l" apply (intro irreducible⇩_{d}I, force simp:is_unit_iff_degree) by (auto dest!: irreducible_multD simp: poly_dvd_1) next assume l: ?l show ?r proof (rule irreducibleI) from l show "f ≠ 0" "¬ is_unit f" by (auto simp: poly_dvd_1) fix a b assume "f = a * b" from l[unfolded this] show "a dvd 1 ∨ b dvd 1" by (auto dest!: irreducible⇩_{d}_multD simp:is_unit_iff_degree) qed qed lemma is_unit_field_poly[simp]: fixes p :: "'a::field poly" shows "is_unit p ⟷ p ≠ 0 ∧ degree p = 0" by (cases "p=0", auto simp: is_unit_iff_degree) lemma irreducible_smult_field[simp]: fixes c :: "'a :: field" shows "irreducible (smult c p) ⟷ c ≠ 0 ∧ irreducible p" (is "?L ⟷ ?R") proof (intro iffI conjI irreducible⇩_{d}_smult_not_zero_divisor_left[of c p, simplified]) assume "irreducible (smult c p)" then show "c ≠ 0" by auto next assume ?R then have c0: "c ≠ 0" and irr: "irreducible p" by auto show ?L proof (fold irreducible_connect_field, intro irreducible⇩_{d}I, unfold degree_smult_eq if_not_P[OF c0]) show "degree p > 0" using irr by auto fix q r from c0 have "p = smult (1/c) (smult c p)" by simp also assume "smult c p = q * r" finally have [simp]: "p = smult (1/c) …". assume main: "degree q < degree p" "degree r < degree p" have "¬irreducible⇩_{d}p" by (rule reducible⇩_{d}I, rule exI[of _ "smult (1/c) q"], rule exI[of _ r], insert irr c0 main, simp) with irr show False by auto qed qed auto lemma irreducible_monic_factor: fixes p :: "'a :: field poly" assumes "degree p > 0" shows "∃ q r. irreducible q ∧ p = q * r ∧ monic q" proof - from irreducible⇩_{d}_factorization_exists[OF assms] obtain fs where "fs ≠ []" and "set fs ⊆ Collect irreducible" and "p = prod_list fs" by auto then have q: "irreducible (hd fs)" and p: "p = hd fs * prod_list (tl fs)" by (atomize(full), cases fs, auto) define c where "c = coeff (hd fs) (degree (hd fs))" from q have c: "c ≠ 0" unfolding c_def irreducible⇩_{d}_def by auto show ?thesis by (rule exI[of _ "smult (1/c) (hd fs)"], rule exI[of _ "smult c (prod_list (tl fs))"], unfold p, insert q c, auto simp: c_def) qed lemma monic_irreducible_factorization: fixes p :: "'a :: field poly" shows "monic p ⟹ ∃ as f. finite as ∧ p = prod (λ a. a ^ Suc (f a)) as ∧ as ⊆ {q. irreducible q ∧ monic q}" proof (induct "degree p" arbitrary: p rule: less_induct) case (less p) show ?case proof (cases "degree p > 0") case False with less(2) have "p = 1" by (simp add: coeff_eq_0 poly_eq_iff) thus ?thesis by (intro exI[of _ "{}"], auto) next case True from irreducible⇩_{d}_factor[OF this] obtain q r where p: "p = q * r" and q: "irreducible q" and deg: "degree r < degree p" by auto hence q0: "q ≠ 0" by auto define c where "c = coeff q (degree q)" let ?q = "smult (1/c) q" let ?r = "smult c r" from q0 have c: "c ≠ 0" "1 / c ≠ 0" unfolding c_def by auto hence p: "p = ?q * ?r" unfolding p by auto have deg: "degree ?r < degree p" using c deg by auto let ?Q = "{q. irreducible q ∧ monic (q :: 'a poly)}" have mon: "monic ?q" unfolding c_def using q0 by auto from monic_factor[OF ‹monic p›[unfolded p] this] have "monic ?r" . from less(1)[OF deg this] obtain f as where as: "finite as" "?r = (∏ a ∈as. a ^ Suc (f a))" "as ⊆ ?Q" by blast from q c have irred: "irreducible ?q" by simp show ?thesis proof (cases "?q ∈ as") case False let ?as = "insert ?q as" let ?f = "λ a. if a = ?q then 0 else f a" have "p = ?q * (∏ a ∈as. a ^ Suc (f a))" unfolding p as by simp also have "(∏ a ∈as. a ^ Suc (f a)) = (∏ a ∈as. a ^ Suc (?f a))" by (rule prod.cong, insert False, auto) also have "?q * … = (∏ a ∈ ?as. a ^ Suc (?f a))" by (subst prod.insert, insert as False, auto) finally have p: "p = (∏ a ∈ ?as. a ^ Suc (?f a))" . from as(1) have fin: "finite ?as" by auto from as mon irred have Q: "?as ⊆ ?Q" by auto from fin p Q show ?thesis by(intro exI[of _ ?as] exI[of _ ?f], auto) next case True let ?f = "λ a. if a = ?q then Suc (f a) else f a" have "p = ?q * (∏ a ∈as. a ^ Suc (f a))" unfolding p as by simp also have "(∏ a ∈as. a ^ Suc (f a)) = ?q ^ Suc (f ?q) * (∏ a ∈(as - {?q}). a ^ Suc (f a))" by (subst prod.remove[OF _ True], insert as, auto) also have "(∏ a ∈(as - {?q}). a ^ Suc (f a)) = (∏ a ∈(as - {?q}).