(* Author: René Thiemann Sebastiaan Joosten Akihisa Yamada License: BSD *) section ‹Algebraic Numbers -- Excluding Addition and Multiplication› text ‹This theory contains basic definition and results on algebraic numbers, namely that algebraic numbers are closed under negation, inversion, $n$-th roots, and that every rational number is algebraic. For all of these closure properties, corresponding polynomial witnesses are available. Moreover, this theory contains the uniqueness result, that for every algebraic number there is exactly one content-free irreducible polynomial with positive leading coefficient for it. This result is stronger than similar ones which you find in many textbooks. The reason is that here we do not require a least degree construction. This is essential, since given some content-free irreducible polynomial for x, how should we check whether the degree is optimal. In the formalized result, this is not required. The result is proven via GCDs, and that the GCD does not change when executed on the rational numbers or on the reals or complex numbers, and that the GCD of a rational polynomial can be expressed via the GCD of integer polynomials.› text ‹Many results are taken from the textbook \<^cite>‹‹pages 317ff› in "AlgNumbers"›.› theory Algebraic_Numbers_Prelim imports "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Polynomial_Interpolation.Newton_Interpolation (* for lemma smult_1 *) Polynomial_Factorization.Gauss_Lemma Berlekamp_Zassenhaus.Unique_Factorization_Poly Polynomial_Factorization.Square_Free_Factorization begin lemma primitive_imp_unit_iff: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes pr: "primitive p" shows "p dvd 1 ⟷ degree p = 0" proof assume "degree p = 0" from degree0_coeffs[OF this] obtain p0 where p: "p = [:p0:]" by auto then have "∀c ∈ set (coeffs p). p0 dvd c" by (simp add: cCons_def) with pr have "p0 dvd 1" by (auto dest: primitiveD) with p show "p dvd 1" by auto next assume "p dvd 1" then show "degree p = 0" by (auto simp: poly_dvd_1) qed lemma dvd_all_coeffs_imp_dvd: assumes "∀a ∈ set (coeffs p). c dvd a" shows "[:c:] dvd p" proof (insert assms, induct p) case 0 then show ?case by simp next case (pCons a p) have "pCons a p = [:a:] + pCons 0 p" by simp also have "[:c:] dvd ..." proof (rule dvd_add) from pCons show "[:c:] dvd [:a:]" by (auto simp: cCons_def) from pCons have "[:c:] dvd p" by auto from Rings.dvd_mult[OF this] show "[:c:] dvd pCons 0 p" by (subst pCons_0_as_mult) qed finally show ?case. qed lemma irreducible_content: fixes p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly" assumes "irreducible p" shows "degree p = 0 ∨ primitive p" proof(rule ccontr) assume not: "¬?thesis" then obtain c where c1: "¬c dvd 1" and "∀a ∈ set (coeffs p). c dvd a" by (auto elim: not_primitiveE) from dvd_all_coeffs_imp_dvd[OF this(2)] obtain r where p: "p = r * [:c:]" by (elim dvdE, auto) from irreducibleD[OF assms this] have "r dvd 1 ∨ [:c:] dvd 1" by auto with c1 have "r dvd 1" unfolding const_poly_dvd_1 by auto then have "degree r = 0" unfolding poly_dvd_1 by auto with p have "degree p = 0" by auto with not show False by auto qed (* TODO: move *) lemma linear_irreducible_field: fixes p :: "'a :: field poly" assumes deg: "degree p = 1" shows "irreducible p" proof (intro irreducibleI) from deg show p0: "p ≠ 0" by auto from deg show "¬ p dvd 1" by (auto simp: poly_dvd_1) fix a b assume p: "p = a * b" with p0 have a0: "a ≠ 0" and b0: "b ≠ 0" by auto from degree_mult_eq[OF this, folded p] assms consider "degree a = 1" "degree b = 0" | "degree a = 0" "degree b = 1" by force then show "a dvd 1 ∨ b dvd 1" by (cases; insert a0 b0, auto simp: primitive_imp_unit_iff) qed (* TODO: move *) lemma linear_irreducible_int: fixes p :: "int poly" assumes deg: "degree p = 1" and cp: "content p dvd 1" shows "irreducible p" proof (intro irreducibleI) from deg show p0: "p ≠ 0" by auto from deg show "¬ p dvd 1" by (auto simp: poly_dvd_1) fix a b assume p: "p = a * b" note * = cp[unfolded p is_unit_content_iff, unfolded content_mult] have a1: "content a dvd 1" and b1: "content b dvd 1" using content_ge_0_int[of a] pos_zmult_eq_1_iff_lemma[OF *] * by (auto simp: abs_mult) with p0 have a0: "a ≠ 0" and b0: "b ≠ 0" by auto from degree_mult_eq[OF this, folded p] assms consider "degree a = 1" "degree b = 0" | "degree a = 0" "degree b = 1" by force then show "a dvd 1 ∨ b dvd 1" by (cases; insert a1 b1, auto simp: primitive_imp_unit_iff) qed lemma irreducible_connect_rev: fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly" assumes irr: "irreducible p" and deg: "degree p > 0" shows "irreducible⇩_{d}p" proof(intro irreducible⇩_{d}I deg) fix q r assume degq: "degree q > 0" and diff: "degree q < degree p" and p: "p = q * r" from degq have nu: "¬ q dvd 1" by (auto simp: poly_dvd_1) from irreducibleD[OF irr p] nu have "r dvd 1" by auto then have "degree r = 0" by (auto simp: poly_dvd_1) with degq diff show False unfolding p using degree_mult_le[of q r] by auto qed subsection ‹Polynomial Evaluation of Integer and Rational Polynomials in Fields.› abbreviation ipoly where "ipoly f x ≡ poly (of_int_poly f) x" lemma poly_map_poly_code[code_unfold]: "poly (map_poly h p) x = fold_coeffs (λ a b. h a + x * b) p 0" by (induct p, auto) abbreviation real_of_int_poly :: "int poly ⇒ real poly" where "real_of_int_poly ≡ of_int_poly" abbreviation real_of_rat_poly :: "rat poly ⇒ real poly" where "real_of_rat_poly ≡ map_poly of_rat" lemma of_rat_of_int[simp]: "of_rat ∘ of_int = of_int" by auto lemma ipoly_of_rat[simp]: "ipoly p (of_rat y) = of_rat (ipoly p y)" proof- have id: "of_int = of_rat o of_int" unfolding comp_def by auto show ?thesis by (subst id, subst map_poly_map_poly[symmetric], auto) qed lemma ipoly_of_real[simp]: "ipoly p (of_real x :: 'a :: {field,real_algebra_1}) = of_real (ipoly p x)" proof - have id: "of_int = of_real o of_int" unfolding comp_def by auto show ?thesis by (subst id, subst map_poly_map_poly[symmetric], auto) qed lemma finite_ipoly_roots: assumes "p ≠ 0" shows "finite {x :: real. ipoly p x = 0}" proof - let ?p = "real_of_int_poly p" from assms have "?p ≠ 0" by auto thus ?thesis by (rule poly_roots_finite) qed subsection ‹Algebraic Numbers -- Definition, Inverse, and Roots› text ‹A number @{term "x :: 'a :: field"} is algebraic iff it is the root of an integer polynomial. Whereas the Isabelle distribution this is defined via the embedding of integers in an field via @{const Ints}, we work with integer polynomials of type @{type int} and then use @{const ipoly} for evaluating the polynomial at a real or complex point.› lemma algebraic_altdef_ipoly: shows "algebraic x ⟷ (∃p. ipoly p x = 0 ∧ p ≠ 0)" unfolding algebraic_def proof (safe, goal_cases) case (1 p) 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 ∈ ℤ" using of_int_the_int[OF that] by auto have "map_poly of_int p' = map_poly (of_int ∘ the_int) p" by (simp add: p'_def map_poly_map_poly) also from 1 of_int_the_int have "… = p" by (subst poly_eq_iff) (auto simp: coeff_map_poly) finally have p_p': "map_poly of_int p' = p" . show ?case proof (intro exI conjI notI) from 1 show "ipoly p' x = 0" by (simp add: p_p') next assume "p' = 0" hence "p = 0" by (simp add: p_p' [symmetric]) with ‹p ≠ 0› show False by contradiction qed next case (2 p) thus ?case by (intro exI[of _ "map_poly of_int p"], auto) qed text ‹Definition of being algebraic with explicit witness polynomial.› definition represents :: "int poly ⇒ 'a :: field_char_0 ⇒ bool" (infix "represents" 51) where "p represents x = (ipoly p x = 0 ∧ p ≠ 0)" lemma representsI[intro]: "ipoly p x = 0 ⟹ p ≠ 0 ⟹ p represents x" unfolding represents_def by auto lemma representsD: assumes "p represents x" shows "p ≠ 0" and "ipoly p x = 0" using assms unfolding represents_def by auto lemma representsE: assumes "p represents x" and "p ≠ 0 ⟹ ipoly p x = 0 ⟹ thesis" shows thesis using assms unfolding represents_def by auto lemma represents_imp_degree: fixes x :: "'a :: field_char_0" assumes "p represents x" shows "degree p ≠ 0" proof- from assms have "p ≠ 0" and px: "ipoly p x = 0" by (auto dest:representsD) then have "(of_int_poly p :: 'a poly) ≠ 0" by auto then have "degree (of_int_poly p :: 'a poly) ≠ 0" by (fold poly_zero[OF px]) then show ?thesis by auto qed lemma representsE_full[elim]: assumes rep: "p represents x" and main: "p ≠ 0 ⟹ ipoly p x = 0 ⟹ degree p ≠ 0 ⟹ thesis" shows thesis by (rule main, insert represents_imp_degree[OF rep] rep, auto elim: representsE) lemma represents_of_rat[simp]: "p represents (of_rat x) = p represents x" by (auto elim!:representsE) lemma represents_of_real[simp]: "p represents (of_real x) = p represents x" by (auto elim!:representsE) lemma algebraic_iff_represents: "algebraic x ⟷ (∃ p. p represents x)" unfolding algebraic_altdef_ipoly represents_def .. lemma represents_irr_non_0: assumes irr: "irreducible p" and ap: "p represents x" and x0: "x ≠ 0" shows "poly p 0 ≠ 0" proof have nu: "¬ [:0,1::int:] dvd 1" by (auto simp: poly_dvd_1) assume "poly p 0 = 0" hence dvd: "[: 0, 1 :] dvd p" by (unfold dvd_iff_poly_eq_0, simp) then obtain q where pq: "p = [:0,1:] * q" by (elim dvdE) from irreducibleD[OF irr this] nu have "q dvd 1" by auto from this obtain r where "q = [:r:]" "r dvd 1" by (auto simp add: poly_dvd_1 dest: degree0_coeffs) with pq have "p = [:0,r:]" by auto with ap have "x = 0" by (auto simp: of_int_hom.map_poly_pCons_hom) with x0 show False by auto qed text ‹The polynomial encoding a rational number.› definition poly_rat :: "rat ⇒ int poly" where "poly_rat x = (case quotient_of x of (n,d) ⇒ [:-n,d:])" definition abs_int_poly:: "int poly ⇒ int poly" where "abs_int_poly p ≡ if lead_coeff p < 0 then -p else p" lemma pos_poly_abs_poly[simp]: shows "lead_coeff (abs_int_poly p) > 0 ⟷ p ≠ 0" proof- have "p ≠ 0 ⟷ lead_coeff p * sgn (lead_coeff p) > 0" by (fold abs_sgn, auto) then show ?thesis by (auto simp: abs_int_poly_def mult.commute) qed lemma abs_int_poly_0[simp]: "abs_int_poly 0 = 0" by (auto simp: abs_int_poly_def) lemma abs_int_poly_eq_0_iff[simp]: "abs_int_poly p = 0 ⟷ p = 0" by (auto simp: abs_int_poly_def sgn_eq_0_iff) lemma degree_abs_int_poly[simp]: "degree (abs_int_poly p) = degree p" by (auto simp: abs_int_poly_def sgn_eq_0_iff) lemma abs_int_poly_dvd[simp]: "abs_int_poly p dvd q ⟷ p dvd q" by (unfold abs_int_poly_def, auto) (*TODO: move & generalize *) lemma (in idom) irreducible_uminus[simp]: "irreducible (-x) ⟷ irreducible x" proof- have "-x = -1 * x" by simp also have "irreducible ... ⟷ irreducible x" by (rule irreducible_mult_unit_left, auto) finally show ?thesis. qed lemma irreducible_abs_int_poly[simp]: "irreducible (abs_int_poly p) ⟷ irreducible p" by (unfold abs_int_poly_def, auto) lemma coeff_abs_int_poly[simp]: "coeff (abs_int_poly p) n = (if lead_coeff p < 0 then - coeff p n else coeff p n)" by (simp add: abs_int_poly_def) lemma lead_coeff_abs_int_poly[simp]: "lead_coeff (abs_int_poly p) = abs (lead_coeff p)" by auto lemma ipoly_abs_int_poly_eq_zero_iff[simp]: "ipoly (abs_int_poly p) (x :: 'a :: comm_ring_1) = 0 ⟷ ipoly p x = 0" by (auto simp: abs_int_poly_def sgn_eq_0_iff of_int_poly_hom.hom_uminus) lemma abs_int_poly_represents[simp]: "abs_int_poly p represents x ⟷ p represents x" by (auto elim!:representsE) (* TODO: Move *) lemma content_pCons[simp]: "content (pCons a p) = gcd a (content p)" by (unfold content_def coeffs_pCons_eq_cCons cCons_def, auto) lemma content_uminus[simp]: fixes p :: "'a :: ring_gcd poly" shows "content (-p) = content p" by (induct p, auto) lemma primitive_abs_int_poly[simp]: "primitive (abs_int_poly p) ⟷ primitive p" by (auto simp: abs_int_poly_def) lemma abs_int_poly_inv[simp]: "smult (sgn (lead_coeff p)) (abs_int_poly p) = p" by (cases "lead_coeff p > 0", auto simp: abs_int_poly_def) definition cf_pos :: "int poly ⇒ bool" where "cf_pos p = (content p = 1 ∧ lead_coeff p > 0)" definition cf_pos_poly :: "int poly ⇒ int poly" where "cf_pos_poly f = (let c = content f; d = (sgn (lead_coeff f) * c) in sdiv_poly f d)" lemma sgn_is_unit[intro!]: fixes x :: "'a :: linordered_idom" (* find/make better class *) assumes "x ≠ 0" shows "sgn x dvd 1" using assms by(cases x "0::'a" rule:linorder_cases, auto) lemma cf_pos_poly_0[simp]: "cf_pos_poly 0 = 0" by (unfold cf_pos_poly_def sdiv_poly_def, auto) lemma cf_pos_poly_eq_0[simp]: "cf_pos_poly f = 0 ⟷ f = 0" proof(cases "f = 0") case True thus ?thesis unfolding cf_pos_poly_def Let_def by (simp add: sdiv_poly_def) next case False then have lc0: "lead_coeff f ≠ 0" by auto then have s0: "sgn (lead_coeff f) ≠ 0" (is "?s ≠ 0") and "content f ≠ 0" (is "?c ≠ 0") by (auto simp: sgn_0_0) then have sc0: "?s * ?c ≠ 0" by auto { fix i from content_dvd_coeff sgn_is_unit[OF lc0] have "?s * ?c dvd coeff f i" by (auto simp: unit_dvd_iff) then have "coeff f i div (?s * ?c) = 0 ⟷ coeff f i = 0" by (auto simp:dvd_div_eq_0_iff) } note * = this show ?thesis unfolding cf_pos_poly_def Let_def sdiv_poly_def poly_eq_iff by (auto simp: coeff_map_poly *) qed lemma shows cf_pos_poly_main: "smult (sgn (lead_coeff f) * content f) (cf_pos_poly f) = f" (is ?g1) and content_cf_pos_poly[simp]: "content (cf_pos_poly f) = (if f = 0 then 0 else 1)" (is ?g2) and lead_coeff_cf_pos_poly[simp]: "lead_coeff (cf_pos_poly f) > 0 ⟷ f ≠ 0" (is ?g3) and cf_pos_poly_dvd[simp]: "cf_pos_poly f dvd f" (is ?g4) proof(atomize(full), (cases "f = 0"; intro conjI)) case True then show ?g1 ?g2 ?g3 ?g4 by simp_all next case f0: False let ?s = "sgn (lead_coeff f)" have s: "?s ∈ {-1,1}" using f0 unfolding sgn_if by auto define g where "g ≡ smult ?s f" define d where "d ≡ ?s * content f" have "content g = content ([:?s:] * f)" unfolding g_def by simp also have "… = content [:?s:] * content f" unfolding content_mult by simp also have "content [:?s:] = 1" using s by (auto simp: content_def) finally have cg: "content g = content f" by simp from f0 have d: "cf_pos_poly f = sdiv_poly f d" by (auto simp: cf_pos_poly_def Let_def d_def) let ?g = "primitive_part g" define ng where "ng = primitive_part g" note d also have "sdiv_poly f d = sdiv_poly g (content g)" unfolding cg unfolding g_def d_def by (rule poly_eqI, unfold coeff_sdiv_poly coeff_smult, insert s, auto simp: div_minus_right) finally have fg: "cf_pos_poly f = primitive_part g" unfolding primitive_part_alt_def . have "lead_coeff f ≠ 0" using f0 by auto hence lg: "lead_coeff g > 0" unfolding g_def lead_coeff_smult by (meson linorder_neqE_linordered_idom sgn_greater sgn_less zero_less_mult_iff) hence g0: "g ≠ 0" by auto from f0 content_primitive_part[OF this] show ?g2 unfolding fg by auto from g0 have "content g ≠ 0" by simp with arg_cong[OF content_times_primitive_part[of g], of lead_coeff, unfolded lead_coeff_smult] lg content_ge_0_int[of g] have lg': "lead_coeff ng > 0" unfolding ng_def by (metis dual_order.antisym dual_order.strict_implies_order zero_less_mult_iff) with f0 show ?g3 unfolding fg ng_def by auto have d0: "d ≠ 0" using s f0 by (force simp add: d_def) have "smult d (cf_pos_poly f) = smult ?s (smult (content f) (sdiv_poly (smult ?s f) (content f)))" unfolding fg primitive_part_alt_def cg by (simp add: g_def d_def) also have "sdiv_poly (smult ?s f) (content f) = smult ?s (sdiv_poly f (content f))" using s by (metis cg g_def primitive_part_alt_def primitive_part_smult_int sgn_sgn) finally have "smult d (cf_pos_poly f) = smult (content f) (primitive_part f)" unfolding primitive_part_alt_def using s by auto also have "… = f" by (rule content_times_primitive_part) finally have df: "smult d (cf_pos_poly f) = f" . with d0 show ?g1 by (auto simp: d_def) from df have *: "f = cf_pos_poly f * [:d:]" by simp from dvdI[OF this] show ?g4. qed (* TODO: remove *) lemma irreducible_connect_int: fixes p :: "int poly" assumes ir: "irreducible⇩_{d}p" and c: "content p = 1" shows "irreducible p" using c primitive_iff_content_eq_1 ir irreducible_primitive_connect by blast lemma fixes x :: "'a :: {idom,ring_char_0}" shows ipoly_cf_pos_poly_eq_0[simp]: "ipoly (cf_pos_poly p) x = 0 ⟷ ipoly p x = 0" and degree_cf_pos_poly[simp]: "degree (cf_pos_poly p) = degree p" and cf_pos_cf_pos_poly[intro]: "p ≠ 0 ⟹ cf_pos (cf_pos_poly p)" proof- show "degree (cf_pos_poly p) = degree p" by (subst(3) cf_pos_poly_main[symmetric], auto simp:sgn_eq_0_iff) { assume p: "p ≠ 0" show "cf_pos (cf_pos_poly p)" using cf_pos_poly_main p by (auto simp: cf_pos_def) have "(ipoly (cf_pos_poly p) x = 0) = (ipoly p x = 0)" apply (subst(3) cf_pos_poly_main[symmetric]) by (auto simp: sgn_eq_0_iff hom_distribs) } then show "(ipoly (cf_pos_poly p) x = 0) = (ipoly p x = 0)" by (cases "p = 0", auto) qed lemma cf_pos_poly_eq_1: "cf_pos_poly f = 1 ⟷ degree f = 0 ∧ f ≠ 0" (is "?l ⟷ ?r") proof(intro iffI conjI) assume ?r then have df0: "degree f = 0" and f0: "f ≠ 0" by auto from degree0_coeffs[OF df0] obtain f0 where f: "f = [:f0:]" by auto show "cf_pos_poly f = 1" using f0 unfolding f cf_pos_poly_def Let_def sdiv_poly_def by (auto simp: content_def mult_sgn_abs) next assume l: ?l then have "degree (cf_pos_poly f) = 0" by auto then show "degree f = 0" by simp from l have "cf_pos_poly f ≠ 0" by auto then show "f ≠ 0" by simp qed lemma irr_cf_poly_rat[simp]: "irreducible (poly_rat x)" "lead_coeff (poly_rat x) > 0" "primitive (poly_rat x)" proof - obtain n d where x: "quotient_of x = (n,d)" by force hence id: "poly_rat x = [:-n,d:]" by (auto simp: poly_rat_def) from quotient_of_denom_pos[OF x] have d: "d > 0" by auto show "lead_coeff (poly_rat x) > 0" "primitive (poly_rat x)" unfolding id cf_pos_def using d quotient_of_coprime[OF x] by (auto simp: content_def) from this[unfolded cf_pos_def] show irr: "irreducible (poly_rat x)" unfolding id using d by (auto intro!: linear_irreducible_int) qed lemma poly_rat[simp]: "ipoly (poly_rat x) (of_rat x :: 'a :: field_char_0) = 0" "ipoly (poly_rat x) x = 0" "poly_rat x ≠ 0" "ipoly (poly_rat x) y = 0 ⟷ y = (of_rat x :: 'a)" proof - from irr_cf_poly_rat(1)[of x] show "poly_rat x ≠ 0" unfolding Factorial_Ring.irreducible_def by auto obtain n d where x: "quotient_of x = (n,d)" by force hence id: "poly_rat x = [:-n,d:]" by (auto simp: poly_rat_def) from quotient_of_denom_pos[OF x] have d: "d ≠ 0" by auto have "y * of_int d = of_int n ⟹ y = of_int n / of_int d" using d by (simp add: eq_divide_imp) with d id show "ipoly (poly_rat x) (of_rat x) = 0" "ipoly (poly_rat x) x = 0" "ipoly (poly_rat x) y = 0 ⟷ y = (of_rat x :: 'a)" by (auto simp: of_rat_minus of_rat_divide simp: quotient_of_div[OF x]) qed lemma poly_rat_represents_of_rat: "(poly_rat x) represents (of_rat x)" by auto lemma ipoly_smult_0_iff: assumes c: "c ≠ 0" shows "(ipoly (smult c p) x = (0 :: real)) = (ipoly p x = 0)" using c by (simp add: hom_distribs) (* TODO *) lemma not_irreducibleD: assumes "¬ irreducible x" and "x ≠ 0" and "¬ x dvd 1" shows "∃y z. x = y * z ∧ ¬ y dvd 1 ∧ ¬ z dvd 1" using assms apply (unfold Factorial_Ring.irreducible_def) by auto lemma cf_pos_poly_represents[simp]: "(cf_pos_poly p) represents x ⟷ p represents x" unfolding represents_def by auto lemma coprime_prod: (* TODO: move *) "a ≠ 0 ⟹ c ≠ 0 ⟹ coprime (a * b) (c * d) ⟹ coprime b (d::'a::{semiring_gcd})" by auto lemma smult_prod: (* TODO: move or find corresponding lemma *) "smult a b = monom a 0 * b" by (simp add: monom_0) lemma degree_map_poly_2: assumes "f (lead_coeff p) ≠ 0" shows "degree (map_poly f p) = degree p" proof (cases "p=0") case False thus ?thesis unfolding degree_eq_length_coeffs Polynomial.coeffs_map_poly using assms by (simp add:coeffs_def) qed auto lemma irreducible_cf_pos_poly: assumes irr: "irreducible p" and deg: "degree p ≠ 0" shows "irreducible (cf_pos_poly p)" (is "irreducible ?p") proof (unfold irreducible_altdef, intro conjI allI impI) from irr show "?p ≠ 0" by auto from deg have "degree ?p ≠ 0" by simp then show "¬ ?p dvd 1" unfolding poly_dvd_1 by auto fix b assume "b dvd cf_pos_poly p" also note cf_pos_poly_dvd finally have "b dvd p". with irr[unfolded irreducible_altdef] have "p dvd b ∨ b dvd 1" by auto then show "?p dvd b ∨ b dvd 1" by (auto dest: dvd_trans[OF cf_pos_poly_dvd]) qed locale dvd_preserving_hom = comm_semiring_1_hom + assumes hom_eq_mult_hom_imp: "hom x = hom y * hz ⟹ ∃z. hz = hom z ∧ x = y * z" begin lemma hom_dvd_hom_iff[simp]: "hom x dvd hom y ⟷ x dvd y" proof assume "hom x dvd hom y" then obtain hz where "hom y = hom x * hz" by (elim dvdE) from hom_eq_mult_hom_imp[OF this] obtain z where "hz = hom z" and mult: "y = x * z" by auto then show "x dvd y" by auto qed auto sublocale unit_preserving_hom proof unfold_locales fix x assume "hom x dvd 1" then have "hom x dvd hom 1" by simp then show "x dvd 1" by (unfold hom_dvd_hom_iff) qed sublocale zero_hom_0 proof (unfold_locales) fix a :: 'a assume "hom a = 0" then have "hom 0 dvd hom a" by auto then have "0 dvd a" by (unfold hom_dvd_hom_iff) then show "a = 0" by auto qed end lemma smult_inverse_monom:"p ≠ 0 ⟹ smult (inverse c) (p::rat poly) = 1 ⟷ p = [: c :]" proof (cases "c=0") case True thus "p ≠ 0 ⟹ ?thesis" by auto next case False thus ?thesis by (metis left_inverse right_inverse smult_1 smult_1_left smult_smult) qed lemma of_int_monom:"of_int_poly p = [:rat_of_int c:] ⟷ p = [: c :]" by (induct p, auto) lemma degree_0_content: fixes p :: "int poly" assumes deg: "degree p = 0" shows "content p = abs (coeff p 0)" proof- from deg obtain a where p: "p = [:a:]" by (auto dest: degree0_coeffs) show ?thesis by (auto simp: p) qed lemma prime_elem_imp_gcd_eq: fixes x::"'a:: ring_gcd" shows "prime_elem x ⟹ gcd x y = normalize x ∨ gcd x y = 1" using prime_elem_imp_coprime [of x y] by (auto simp add: gcd_proj1_iff intro: coprime_imp_gcd_eq_1) lemma irreducible_pos_gcd: fixes p :: "int poly" assumes ir: "irreducible p" and pos: "lead_coeff p > 0" shows "gcd p q ∈ {1,p}" proof- from pos have "[:sgn (lead_coeff p):] = 1" by auto with prime_elem_imp_gcd_eq[of p, unfolded prime_elem_iff_irreducible, OF ir, of q] show ?thesis by (auto simp: normalize_poly_def) qed lemma irreducible_pos_gcd_twice: fixes p q :: "int poly" assumes p: "irreducible p" "lead_coeff p > 0" and q: "irreducible q" "lead_coeff q > 0" shows "gcd p q = 1 ∨ p = q" proof (cases "gcd p q = 1") case False note pq = this have "p = gcd p q" using irreducible_pos_gcd [OF p, of q] pq by auto also have "… = q" using irreducible_pos_gcd [OF q, of p] pq by (auto simp add: ac_simps) finally show ?thesis by auto qed simp interpretation of_rat_hom: field_hom_0' of_rat.. lemma poly_zero_imp_not_unit: assumes "poly p x = 0" shows "¬ p dvd 1" proof (rule notI) assume "p dvd 1" from poly_hom.hom_dvd_1[OF this] have "poly p x dvd 1" by auto with assms show False by auto qed lemma poly_prod_mset_zero_iff: fixes x :: "'a :: idom" shows "poly (prod_mset F) x = 0 ⟷ (∃f ∈# F. poly f x = 0)" by (induct F, auto simp: poly_mult_zero_iff) lemma algebraic_imp_represents_irreducible: fixes x :: "'a :: field_char_0" assumes "algebraic x" shows "∃p. p represents x ∧ irreducible p" proof - from assms obtain p where px0: "ipoly p x = 0" and p0: "p ≠ 0" unfolding algebraic_altdef_ipoly by auto from poly_zero_imp_not_unit[OF px0] have "¬ p dvd 1" by (auto dest: of_int_poly_hom.hom_dvd_1[where 'a = 'a]) from mset_factors_exist[OF p0 this] obtain F where F: "mset_factors F p" by auto then have "p = prod_mset F" by auto also have "(of_int_poly ... :: 'a poly) = prod_mset (image_mset of_int_poly F)" by simp finally have "poly ... x = 0" using px0 by auto from this[unfolded poly_prod_mset_zero_iff] obtain f where "f ∈# F" and fx0: "ipoly f x = 0" by auto with F have "irreducible f" by auto with fx0 show ?thesis by auto qed lemma algebraic_imp_represents_irreducible_cf_pos: assumes "algebraic (x::'a::field_char_0)" shows "∃p. p represents x ∧ irreducible p ∧ lead_coeff p > 0 ∧ primitive p" proof - from algebraic_imp_represents_irreducible[OF assms(1)] obtain p where px: "p represents x" and irr: "irreducible p" by auto let ?p = "cf_pos_poly p" from px irr represents_imp_degree have 1: "?p represents x" and 2: "irreducible ?p" and 3: "cf_pos ?p" by (auto intro: irreducible_cf_pos_poly) then show ?thesis by (auto intro: exI[of _ ?p] simp: cf_pos_def) qed lemma gcd_of_int_poly: "gcd (of_int_poly f) (of_int_poly g :: 'a :: {field_char_0,field_gcd} poly) = smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))" proof - let ?ia = "of_int_poly :: _ ⇒ 'a poly" let ?ir = "of_int_poly :: _ ⇒ rat poly" let ?ra = "map_poly of_rat :: _ ⇒ 'a poly" have id: "?ia x = ?ra (?ir x)" for x by (subst map_poly_map_poly, auto) show ?thesis unfolding id unfolding of_rat_hom.map_poly_gcd[symmetric] unfolding gcd_rat_to_gcd_int by (auto simp: hom_distribs) qed lemma algebraic_imp_represents_unique: fixes x :: "'a :: {field_char_0,field_gcd}" assumes "algebraic x" shows "∃! p. p represents x ∧ irreducible p ∧ lead_coeff p > 0" (is "Ex1 ?p") proof - from assms obtain p where p: "?p p" and cfp: "cf_pos p" by (auto simp: cf_pos_def dest: algebraic_imp_represents_irreducible_cf_pos) show ?thesis proof (rule ex1I) show "?p p" by fact fix q assume q: "?p q" then have "q represents x" by auto from represents_imp_degree[OF this] q irreducible_content[of q] have cfq: "cf_pos q" by (auto simp: cf_pos_def) show "q = p" proof (rule ccontr) let ?ia = "map_poly of_int :: int poly ⇒ 'a poly" assume "q ≠ p" with irreducible_pos_gcd_twice[of p q] p q cfp cfq have gcd: "gcd p q = 1" by auto from p q have rt: "ipoly p x = 0" "ipoly q x = 0" unfolding represents_def by auto define c :: 'a where "c = inverse (of_int (lead_coeff (gcd p q)))" have rt: "poly (?ia p) x = 0" "poly (?ia q) x = 0" using rt by auto hence "[:-x,1:] dvd ?ia p" "[:-x,1:] dvd ?ia q" unfolding poly_eq_0_iff_dvd by auto hence "[:-x,1:] dvd gcd (?ia p) (?ia q)" by (rule gcd_greatest) also have "… = smult c (?ia (gcd p q))" unfolding gcd_of_int_poly c_def .. also have "?ia (gcd p q) = 1" by (simp add: gcd) also have "smult c 1 = [: c :]" by simp finally show False using c_def gcd by (simp add: dvd_iff_poly_eq_0) qed qed qed lemma ipoly_poly_compose: fixes x :: "'a :: idom" shows "ipoly (p ∘⇩_{p}q) x = ipoly p (ipoly q x)" proof (induct p) case (pCons a p) have "ipoly ((pCons a p) ∘⇩_{p}q) x = of_int a + ipoly (q * p ∘⇩_{p}q) x" by (simp add: hom_distribs) also have "ipoly (q * p ∘⇩_{p}q) x = ipoly q x * ipoly (p ∘⇩_{p}q) x" by (simp add: hom_distribs) also have "ipoly (p ∘⇩_{p}q) x = ipoly p (ipoly q x)" unfolding pCons(2) .. also have "of_int a + ipoly q x * … = ipoly (pCons a p) (ipoly q x)" unfolding map_poly_pCons[OF pCons(1)] by simp finally show ?case . qed simp lemma algebraic_0[simp]: "algebraic 0" unfolding algebraic_altdef_ipoly by (intro exI[of _ "[:0,1:]"], auto) lemma algebraic_1[simp]: "algebraic 1" unfolding algebraic_altdef_ipoly by (intro exI[of _ "[:-1,1:]"], auto) text ‹Polynomial for unary minus.› definition poly_uminus :: "'a :: ring_1 poly ⇒ 'a poly" where [code del]: "poly_uminus p ≡ ∑i≤degree p. monom ((-1)^i * coeff p i) i" lemma poly_uminus_pCons_pCons[simp]: "poly_uminus (pCons a (pCons b p)) = pCons a (pCons (-b) (poly_uminus p))" (is "?l = ?r") proof(cases "p = 0") case False then have deg: "degree (pCons a (pCons b p)) = Suc (Suc (degree p))" by simp show ?thesis by (unfold poly_uminus_def deg sum.atMost_Suc_shift monom_Suc monom_0 sum_pCons_0_commute, simp) next case True then show ?thesis by (auto simp add: poly_uminus_def monom_0 monom_Suc) qed fun poly_uminus_inner :: "'a :: ring_1 list ⇒ 'a poly" where "poly_uminus_inner [] = 0" | "poly_uminus_inner [a] = [:a:]" | "poly_uminus_inner (a#b#cs) = pCons a (pCons (-b) (poly_uminus_inner cs))" lemma poly_uminus_code[code,simp]: "poly_uminus p = poly_uminus_inner (coeffs p)" proof- have "poly_uminus (Poly as) = poly_uminus_inner as" for as :: "'a list" proof (induct "length as" arbitrary:as rule: less_induct) case less show ?case proof(cases as) case Nil then show ?thesis by (simp add: poly_uminus_def) next case [simp]: (Cons a bs) show ?thesis proof (cases bs) case Nil then show ?thesis by (simp add: poly_uminus_def monom_0) next case [simp]: (Cons b cs) show ?thesis by (simp add: less) qed qed qed from this[of "coeffs p"] show ?thesis by simp qed lemma poly_uminus_inner_0[simp]: "poly_uminus_inner as = 0 ⟷ Poly as = 0" by (induct as rule: poly_uminus_inner.induct, auto) lemma degree_poly_uminus_inner[simp]: "degree (poly_uminus_inner as) = degree (Poly as)" by (induct as rule: poly_uminus_inner.induct, auto) lemma ipoly_uminus_inner[simp]: "ipoly (poly_uminus_inner as) (x::'a::comm_ring_1) = ipoly (Poly as) (-x)" by (induct as rule: poly_uminus_inner.induct, auto simp: hom_distribs ring_distribs) lemma represents_uminus: assumes alg: "p represents x" shows "(poly_uminus p) represents (-x)" proof - from representsD[OF alg] have "p ≠ 0" and rp: "ipoly p x = 0" by auto hence 0: "poly_uminus p ≠ 0" by simp show ?thesis by (rule representsI[OF _ 0], insert rp, auto) qed lemma content_poly_uminus_inner[simp]: fixes as :: "'a :: ring_gcd list" shows "content (poly_uminus_inner as) = content (Poly as)" by (induct as rule: poly_uminus_inner.induct, auto) text ‹Multiplicative inverse is represented by @{const reflect_poly}.› lemma inverse_pow_minus: assumes "x ≠ (0 :: 'a :: field)" and "i ≤ n" shows "inverse x ^ n * x ^ i = inverse x ^ (n - i)" using assms by (simp add: field_class.field_divide_inverse power_diff power_inverse) lemma (in inj_idom_hom) reflect_poly_hom: "reflect_poly (map_poly hom p) = map_poly hom (reflect_poly p)" proof - obtain xs where xs: "rev (coeffs p) = xs" by auto show ?thesis unfolding reflect_poly_def coeffs_map_poly_hom rev_map xs by (induct xs, auto simp: hom_distribs) qed lemma ipoly_reflect_poly: assumes x: "(x :: 'a :: field_char_0) ≠ 0" shows "ipoly (reflect_poly p) x = x ^ (degree p) * ipoly p (inverse x)" (is "?l = ?r") proof - let ?or = "of_int :: int ⇒ 'a" have hom: "inj_idom_hom ?or" .. show ?thesis using poly_reflect_poly_nz[OF x, of "map_poly ?or p"] by (simp add: inj_idom_hom.reflect_poly_hom[OF hom]) qed lemma represents_inverse: assumes x: "x ≠ 0" and alg: "p represents x" shows "(reflect_poly p) represents (inverse x)" proof (intro representsI) from representsD[OF alg] have "p ≠ 0" and rp: "ipoly p x = 0" by auto then show "reflect_poly p ≠ 0" by (metis reflect_poly_0 reflect_poly_at_0_eq_0_iff) show "ipoly (reflect_poly p) (inverse x) = 0" by (subst ipoly_reflect_poly, insert x, auto simp:rp) qed lemma inverse_roots: assumes x: "(x :: 'a :: field_char_0) ≠ 0" shows "ipoly (reflect_poly p) x = 0 ⟷ ipoly p (inverse x) = 0" using x by (auto simp: ipoly_reflect_poly) context fixes n :: nat begin text ‹Polynomial for n-th root.› definition poly_nth_root :: "'a :: idom poly ⇒ 'a poly" where "poly_nth_root p = p ∘⇩_{p}monom 1 n" lemma ipoly_nth_root: fixes x :: "'a :: idom" shows "ipoly (poly_nth_root p) x = ipoly p (x ^ n)" unfolding poly_nth_root_def ipoly_poly_compose by (simp add: map_poly_monom poly_monom) context assumes n: "n ≠ 0" begin lemma poly_nth_root_0[simp]: "poly_nth_root p = 0 ⟷ p = 0" unfolding poly_nth_root_def by (rule pcompose_eq_0, insert n, auto simp: degree_monom_eq) lemma represents_nth_root: assumes y: "y^n = x" and alg: "p represents x" shows "(poly_nth_root p) represents y" proof - from representsD[OF alg] have "p ≠ 0" and rp: "ipoly p x = 0" by auto hence 0: "poly_nth_root p ≠ 0" by simp show ?thesis by (rule representsI[OF _ 0], unfold ipoly_nth_root y rp, simp) qed lemma represents_nth_root_odd_real: assumes alg: "p represents x" and odd: "odd n" shows "(poly_nth_root p) represents (root n x)" by (rule represents_nth_root[OF odd_real_root_pow[OF odd] alg]) lemma represents_nth_root_pos_real: assumes alg: "p represents x" and pos: "x > 0" shows "(poly_nth_root p) represents (root n x)" proof - from n have id: "Suc (n - 1) = n" by auto show ?thesis proof (rule represents_nth_root[OF _ alg]) show "root n x ^ n = x" using id pos by auto qed qed lemma represents_nth_root_neg_real: assumes alg: "p represents x" and neg: "x < 0" shows "(poly_uminus (poly_nth_root (poly_uminus p))) represents (root n x)" proof - have rt: "root n x = - root n (-x)" unfolding real_root_minus by simp show ?thesis unfolding rt by (rule represents_uminus[OF represents_nth_root_pos_real[OF represents_uminus[OF alg]]], insert neg, auto) qed end end lemma represents_csqrt: assumes alg: "p represents x" shows "(poly_nth_root 2 p) represents (csqrt x)" by (rule represents_nth_root[OF _ _ alg], auto) lemma represents_sqrt: assumes alg: "p represents x" and pos: "x ≥ 0" shows "(poly_nth_root 2 p) represents (sqrt x)" by (rule represents_nth_root[OF _ _ alg], insert pos, auto) lemma represents_degree: assumes "p represents x" shows "degree p ≠ 0" proof assume "degree p = 0" from degree0_coeffs[OF this] obtain c where p: "p = [:c:]" by auto from assms[unfolded represents_def p] show False by auto qed text ‹Polynomial for multiplying a rational number with an algebraic number.› definition poly_mult_rat_main where "poly_mult_rat_main n d (f :: 'a :: idom poly) = (let fs = coeffs f; k = length fs in poly_of_list (map (λ (fi, i). fi * d ^ i * n ^ (k - Suc i)) (zip fs [0 ..< k])))" definition poly_mult_rat :: "rat ⇒ int poly ⇒ int poly" where "poly_mult_rat r p ≡ case quotient_of r of (n,d) ⇒ poly_mult_rat_main n d p" lemma coeff_poly_mult_rat_main: "coeff (poly_mult_rat_main n d f) i = coeff f i * n ^ (degree f - i) * d ^ i" proof - have id: "coeff (poly_mult_rat_main n d f) i = (coeff f i * d ^ i) * n ^ (length (coeffs f) - Suc i)" unfolding poly_mult_rat_main_def Let_def poly_of_list_def coeff_Poly unfolding nth_default_coeffs_eq[symmetric] unfolding nth_default_def by auto show ?thesis unfolding id by (simp add: degree_eq_length_coeffs) qed lemma degree_poly_mult_rat_main: "n ≠ 0 ⟹ degree (poly_mult_rat_main n d f) = (if d = 0 then 0 else degree f)" proof (cases "d = 0") case True thus ?thesis unfolding degree_def unfolding coeff_poly_mult_rat_main by simp next case False hence id: "(d = 0) = False" by simp show "n ≠ 0 ⟹ ?thesis" unfolding degree_def coeff_poly_mult_rat_main id by (simp add: id) qed lemma ipoly_mult_rat_main: fixes x :: "'a :: {field,ring_char_0}" assumes "d ≠ 0" and "n ≠ 0" shows "ipoly (poly_mult_rat_main n d p) x = of_int n ^ degree p * ipoly p (x * of_int d / of_int n)" proof - from assms have d: "(if d = 0 then t else f) = f" for t f :: 'b by simp show ?thesis unfolding poly_altdef of_int_hom.coeff_map_poly_hom mult.assoc[symmetric] of_int_mult[symmetric] sum_distrib_left unfolding of_int_hom.degree_map_poly_hom degree_poly_mult_rat_main[OF assms(2)] d proof (rule sum.cong[OF refl]) fix i assume "i ∈ {..degree p}" hence i: "i ≤ degree p" by auto hence id: "of_int n ^ (degree p - i) = (of_int n ^ degree p / of_int n ^ i :: 'a)" by (simp add: assms(2) power_diff) thus "of_int (coeff (poly_mult_rat_main n d p) i) * x ^ i = of_int n ^ degree p * of_int (coeff p i) * (x * of_int d / of_int n) ^ i" unfolding coeff_poly_mult_rat_main by (simp add: field_simps) qed qed lemma degree_poly_mult_rat[simp]: assumes "r ≠ 0" shows "degree (poly_mult_rat r p) = degree p" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" by auto with assms r have n0: "n ≠ 0" by simp from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p" unfolding poly_mult_rat_def by simp show ?thesis unfolding id degree_poly_mult_rat_main[OF n0] using d by simp qed lemma ipoly_mult_rat: assumes r0: "r ≠ 0" shows "ipoly (poly_mult_rat r p) x = of_int (fst (quotient_of r)) ^ degree p * ipoly p (x * inverse (of_rat r))" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" by auto from r r0 have n: "n ≠ 0" by simp from r d n have inv: "of_int d / of_int n = inverse r" by simp from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p" unfolding poly_mult_rat_def by simp show ?thesis unfolding id ipoly_mult_rat_main[OF d n] quot fst_conv of_rat_inverse[symmetric] inv[symmetric] by (simp add: of_rat_divide) qed lemma poly_mult_rat_main_0[simp]: assumes "n ≠ 0" "d ≠ 0" shows "poly_mult_rat_main n d p = 0 ⟷ p = 0" proof assume "p = 0" thus "poly_mult_rat_main n d p = 0" by (simp add: poly_mult_rat_main_def) next assume 0: "poly_mult_rat_main n d p = 0" { fix i from 0 have "coeff (poly_mult_rat_main n d p) i = 0" by simp hence "coeff p i = 0" unfolding coeff_poly_mult_rat_main using assms by simp } thus "p = 0" by (intro poly_eqI, auto) qed lemma poly_mult_rat_0[simp]: assumes r0: "r ≠ 0" shows "poly_mult_rat r p = 0 ⟷ p = 0" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" by auto from r r0 have n: "n ≠ 0" by simp from quot have id: "poly_mult_rat r p = poly_mult_rat_main n d p" unfolding poly_mult_rat_def by simp show ?thesis unfolding id using n d by simp qed lemma represents_mult_rat: assumes r: "r ≠ 0" and "p represents x" shows "(poly_mult_rat r p) represents (of_rat r * x)" using assms unfolding represents_def ipoly_mult_rat[OF r] by (simp add: field_simps) text ‹Polynomial for adding a rational number on an algebraic number. Again, we do not have to factor afterwards.› definition poly_add_rat :: "rat ⇒ int poly ⇒ int poly" where "poly_add_rat r p ≡ case quotient_of r of (n,d) ⇒ (poly_mult_rat_main d 1 p ∘⇩_{p}[:-n,d:])" lemma poly_add_rat_code[code]: "poly_add_rat r p ≡ case quotient_of r of (n,d) ⇒ let p' = (let fs = coeffs p; k = length fs in poly_of_list (map (λ(fi, i). fi * d ^ (k - Suc i)) (zip fs [0..<k]))); p'' = p' ∘⇩_{p}[:-n,d:] in p''" unfolding poly_add_rat_def poly_mult_rat_main_def Let_def by simp lemma degree_poly_add_rat[simp]: "degree (poly_add_rat r p) = degree p" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" "d > 0" by auto show ?thesis unfolding poly_add_rat_def quot split by (simp add: degree_poly_mult_rat_main d) qed lemma ipoly_add_rat: "ipoly (poly_add_rat r p) x = (of_int (snd (quotient_of r)) ^ degree p) * ipoly p (x - of_rat r)" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" "d > 0" by auto have id: "ipoly [:- n, 1:] (x / of_int d :: 'a) = - of_int n + x / of_int d" by simp show ?thesis unfolding poly_add_rat_def quot split by (simp add: ipoly_mult_rat_main ipoly_poly_compose d r degree_poly_mult_rat_main field_simps id of_rat_divide) qed lemma poly_add_rat_0[simp]: "poly_add_rat r p = 0 ⟷ p = 0" proof - obtain n d where quot: "quotient_of r = (n,d)" by force from quotient_of_div[OF quot] have r: "r = of_int n / of_int d" by auto from quotient_of_denom_pos[OF quot] have d: "d ≠ 0" "d > 0" by auto show ?thesis unfolding poly_add_rat_def quot split by (simp add: d pcompose_eq_0) qed lemma add_rat_roots: "ipoly (poly_add_rat r p) x = 0 ⟷ ipoly p (x - of_rat r) = 0" unfolding ipoly_add_rat using quotient_of_nonzero by auto lemma represents_add_rat: assumes "p represents x" shows "(poly_add_rat r p) represents (of_rat r + x)" using assms unfolding represents_def ipoly_add_rat by simp (* TODO: move? *) lemmas pos_mult[simplified,simp] = mult_less_cancel_left_pos[of _ 0] mult_less_cancel_left_pos[of _ _ 0] lemma ipoly_add_rat_pos_neg: "ipoly (poly_add_rat r p) (x::'a::linordered_field) < 0 ⟷ ipoly p (x - of_rat r) < 0" "ipoly (poly_add_rat r p) (x::'a::linordered_field) > 0 ⟷ ipoly p (x - of_rat r) > 0" using quotient_of_nonzero unfolding ipoly_add_rat by auto lemma sgn_ipoly_add_rat[simp]: "sgn (ipoly (poly_add_rat r p) (x::'a::linordered_field)) = sgn (ipoly p (x - of_rat r))" (is "sgn ?l = sgn ?r") using ipoly_add_rat_pos_neg[of r p x] by (cases ?r "0::'a" rule: linorder_cases,auto simp: sgn_1_pos sgn_1_neg sgn_eq_0_iff) lemma deg_nonzero_represents: assumes deg: "degree p ≠ 0" shows "∃ x :: complex. p represents x" proof - let ?p = "of_int_poly p :: complex poly" from fundamental_theorem_algebra_factorized[of ?p] obtain as c where id: "smult c (∏a←as. [:- a, 1:]) = ?p" and len: "length as = degree ?p" by blast have "degree ?p = degree p" by simp with deg len obtain b bs where as: "as = b # bs" by (cases as, auto) have "p represents b" unfolding represents_def id[symmetric] as using deg by auto thus ?thesis by blast qed end