(* Author: René Thiemann Akihisa Yamada Contributors: Manuel Eberl (algebraic integers) License: BSD *) section ‹Algebraic Numbers: Addition and Multiplication› text ‹This theory contains the remaining field operations for algebraic numbers, namely addition and multiplication.› theory Algebraic_Numbers imports Algebraic_Numbers_Prelim Resultant Polynomial_Factorization.Polynomial_Irreducibility begin interpretation coeff_hom: monoid_add_hom "λp. coeff p i" by (unfold_locales, auto) interpretation coeff_hom: comm_monoid_add_hom "λp. coeff p i".. interpretation coeff_hom: group_add_hom "λp. coeff p i".. interpretation coeff_hom: ab_group_add_hom "λp. coeff p i".. interpretation coeff_0_hom: monoid_mult_hom "λp. coeff p 0" by (unfold_locales, auto simp: coeff_mult) interpretation coeff_0_hom: semiring_hom "λp. coeff p 0".. interpretation coeff_0_hom: comm_monoid_mult_hom "λp. coeff p 0".. interpretation coeff_0_hom: comm_semiring_hom "λp. coeff p 0".. subsection ‹Addition of Algebraic Numbers› definition "x_y ≡ [: [: 0, 1 :], -1 :]" definition "poly_x_minus_y p = poly_lift p ∘⇩_{p}x_y" lemma coeff_xy_power: assumes "k ≤ n" shows "coeff (x_y ^ n :: 'a :: comm_ring_1 poly poly) k = monom (of_nat (n choose (n - k)) * (- 1) ^ k) (n - k)" proof - define X :: "'a poly poly" where "X = monom (monom 1 1) 0" define Y :: "'a poly poly" where "Y = monom (-1) 1" have [simp]: "monom 1 b * (-1) ^ k = monom ((-1)^k :: 'a) b" for b k by (auto simp: monom_altdef minus_one_power_iff) have "(X + Y) ^ n = (∑i≤n. of_nat (n choose i) * X ^ i * Y ^ (n - i))" by (subst binomial_ring) auto also have "… = (∑i≤n. of_nat (n choose i) * monom (monom ((-1) ^ (n - i)) i) (n - i))" by (simp add: X_def Y_def monom_power mult_monom mult.assoc) also have "… = (∑i≤n. monom (monom (of_nat (n choose i) * (-1) ^ (n - i)) i) (n - i))" by (simp add: of_nat_poly smult_monom) also have "coeff … k = (∑i≤n. if n - i = k then monom (of_nat (n choose i) * (- 1) ^ (n - i)) i else 0)" by (simp add: of_nat_poly coeff_sum) also have "… = (∑i∈{n-k}. monom (of_nat (n choose i) * (- 1) ^ (n - i)) i)" using ‹k ≤ n› by (intro sum.mono_neutral_cong_right) auto also have "X + Y = x_y" by (simp add: X_def Y_def x_y_def monom_altdef) finally show ?thesis using ‹k ≤ n› by simp qed text ‹The following polynomial represents the sum of two algebraic numbers.› definition poly_add :: "'a :: comm_ring_1 poly ⇒ 'a poly ⇒ 'a poly" where "poly_add p q = resultant (poly_x_minus_y p) (poly_lift q)" subsubsection ‹@{term poly_add} has desired root› interpretation poly_x_minus_y_hom: comm_ring_hom poly_x_minus_y by (unfold_locales; simp add: poly_x_minus_y_def hom_distribs) lemma poly2_x_y[simp]: fixes x :: "'a :: comm_ring_1" shows "poly2 x_y x y = x - y" unfolding poly2_def by (simp add: x_y_def) lemma degree_poly_x_minus_y[simp]: fixes p :: "'a::idom poly" shows "degree (poly_x_minus_y p) = degree p" unfolding poly_x_minus_y_def x_y_def by auto lemma poly_x_minus_y_pCons[simp]: "poly_x_minus_y (pCons a p) = [:[: a :]:] + poly_x_minus_y p * x_y" unfolding poly_x_minus_y_def x_y_def by simp lemma poly_poly_poly_x_minus_y[simp]: fixes p :: "'a :: comm_ring_1 poly" shows "poly (poly (poly_x_minus_y p) q) x = poly p (x - poly q x)" by (induct p; simp add: ring_distribs x_y_def) lemma poly2_poly_x_minus_y[simp]: fixes p :: "'a :: comm_ring_1 poly" shows "poly2 (poly_x_minus_y p) x y = poly p (x-y)" unfolding poly2_def by simp interpretation x_y_mult_hom: zero_hom_0 "λp :: 'a :: comm_ring_1 poly poly. x_y * p" proof (unfold_locales) fix p :: "'a poly poly" assume "x_y * p = 0" then show "p = 0" apply (simp add: x_y_def) by (metis eq_neg_iff_add_eq_0 minus_equation_iff minus_pCons synthetic_div_unique_lemma) qed lemma x_y_nonzero[simp]: "x_y ≠ 0" by (simp add: x_y_def) lemma degree_x_y[simp]: "degree x_y = 1" by (simp add: x_y_def) interpretation x_y_mult_hom: inj_comm_monoid_add_hom "λp :: 'a :: idom poly poly. x_y * p" proof (unfold_locales) show "x_y * p = x_y * q ⟹ p = q" for p q :: "'a poly poly" proof (induct p arbitrary:q) case 0 then show ?case by simp next case p: (pCons a p) from p(3)[unfolded mult_pCons_right] have "x_y * (monom a 0 + pCons 0 1 * p) = x_y * q" apply (subst(asm) pCons_0_as_mult) apply (subst(asm) smult_prod) by (simp only: field_simps distrib_left) then have "monom a 0 + pCons 0 1 * p = q" by simp then show "pCons a p = q" using pCons_as_add by (simp add: monom_0 monom_Suc) qed qed interpretation poly_x_minus_y_hom: inj_idom_hom poly_x_minus_y proof fix p :: "'a poly" assume 0: "poly_x_minus_y p = 0" then have "poly_lift p ∘⇩_{p}x_y = 0" by (simp add: poly_x_minus_y_def) then show "p = 0" proof (induct p) case 0 then show ?case by simp next case (pCons a p) note p = this[unfolded poly_lift_pCons pcompose_pCons] show ?case proof (cases "a=0") case a0: True with p have "x_y * poly_lift p ∘⇩_{p}x_y = 0" by simp then have "poly_lift p ∘⇩_{p}x_y = 0" by simp then show ?thesis using p by simp next case a0: False with p have p0: "p ≠ 0" by auto from p have "[:[:a:]:] = - x_y * poly_lift p ∘⇩_{p}x_y" by (simp add: eq_neg_iff_add_eq_0) then have "degree [:[:a:]:] = degree (x_y * poly_lift p ∘⇩_{p}x_y)" by simp also have "... = degree (x_y::'a poly poly) + degree (poly_lift p ∘⇩_{p}x_y)" apply (subst degree_mult_eq) apply simp apply (subst pcompose_eq_0) apply (simp add: x_y_def) apply (simp add: p0) apply simp done finally have False by simp then show ?thesis.. qed qed qed lemma poly_add: fixes p q :: "'a ::comm_ring_1 poly" assumes q0: "q ≠ 0" and x: "poly p x = 0" and y: "poly q y = 0" shows "poly (poly_add p q) (x+y) = 0" proof (unfold poly_add_def, rule poly_resultant_zero[OF disjI2]) have "degree q > 0" using poly_zero q0 y by auto thus degq: "degree (poly_lift q) > 0" by auto qed (insert x y, simp_all) subsubsection ‹@{const poly_add} is nonzero› text ‹ We first prove that @{const poly_lift} preserves factorization. The result will be essential also in the next section for division of algebraic numbers. › interpretation poly_lift_hom: unit_preserving_hom "poly_lift :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly ⇒ _" proof fix x :: "'a poly" assume "poly_lift x dvd 1" then have "poly_y_x (poly_lift x) dvd poly_y_x 1" by simp then show "x dvd 1" by (auto simp add: poly_y_x_poly_lift) qed interpretation poly_lift_hom: factor_preserving_hom "poly_lift::'a::idom poly ⇒ 'a poly poly" proof unfold_locales fix p :: "'a poly" assume p: "irreducible p" show "irreducible (poly_lift p)" proof(rule ccontr) from p have p0: "p ≠ 0" and "¬ p dvd 1" by (auto dest: irreducible_not_unit) with poly_lift_hom.hom_dvd[of p 1] have p1: "¬ poly_lift p dvd 1" by auto assume "¬ irreducible (poly_lift p)" from this[unfolded irreducible_altdef,simplified] p0 p1 obtain q where "q dvd poly_lift p" and pq: "¬ poly_lift p dvd q" and q: "¬ q dvd 1" by auto then obtain r where "q * r = poly_lift p" by (elim dvdE, auto) then have "poly_y_x (q * r) = poly_y_x (poly_lift p)" by auto also have "... = [:p:]" by (auto simp: poly_y_x_poly_lift monom_0) also have "poly_y_x (q * r) = poly_y_x q * poly_y_x r" by (auto simp: hom_distribs) finally have "... = [:p:]" by auto then have qp: "poly_y_x q dvd [:p:]" by (metis dvdI) from dvd_const[OF this] p0 have "degree (poly_y_x q) = 0" by auto from degree_0_id[OF this,symmetric] obtain s where qs: "poly_y_x q = [:s:]" by auto have "poly_lift s = poly_y_x (poly_y_x (poly_lift s))" by auto also have "... = poly_y_x [:s:]" by (auto simp: poly_y_x_poly_lift monom_0) also have "... = q" by (auto simp: qs[symmetric]) finally have sq: "poly_lift s = q" by auto from qp[unfolded qs] have sp: "s dvd p" by (auto simp: const_poly_dvd) from irreducibleD'[OF p this] sq q pq show False by auto qed qed text ‹ We now show that @{const poly_x_minus_y} is a factor-preserving homomorphism. This is essential for this section. This is easy since @{const poly_x_minus_y} can be represented as the composition of two factor-preserving homomorphisms. › lemma poly_x_minus_y_as_comp: "poly_x_minus_y = (λp. p ∘⇩_{p}x_y) ∘ poly_lift" by (intro ext, unfold poly_x_minus_y_def, auto) context idom_isom begin sublocale comm_semiring_isom.. end interpretation poly_x_minus_y_hom: factor_preserving_hom "poly_x_minus_y :: 'a :: idom poly ⇒ 'a poly poly" proof - have ‹p ∘⇩_{p}x_y ∘⇩_{p}x_y = p› for p :: ‹'a poly poly› proof (induction p) case 0 show ?case by simp next case (pCons a p) then show ?case by (unfold x_y_def hom_distribs pcompose_pCons) simp qed then interpret x_y_hom: bijective "λp :: 'a poly poly. p ∘⇩_{p}x_y" by (unfold bijective_eq_bij) (rule involuntory_imp_bij) interpret x_y_hom: idom_isom "λp :: 'a poly poly. p ∘⇩_{p}x_y" by standard simp_all have ‹factor_preserving_hom (λp :: 'a poly poly. p ∘⇩_{p}x_y)› and ‹factor_preserving_hom (poly_lift :: 'a poly ⇒ 'a poly poly)› .. then show "factor_preserving_hom (poly_x_minus_y :: 'a poly ⇒ _)" by (unfold poly_x_minus_y_as_comp) (rule factor_preserving_hom_comp) qed text ‹ Now we show that results of @{const poly_x_minus_y} and @{const poly_lift} are coprime. › lemma poly_y_x_const[simp]: "poly_y_x [:[:a:]:] = [:[:a:]:]" by (simp add: poly_y_x_def monom_0) context begin private abbreviation "y_x == [: [: 0, -1 :], 1 :]" lemma poly_y_x_x_y[simp]: "poly_y_x x_y = y_x" by (simp add: x_y_def poly_y_x_def monom_Suc monom_0) private lemma y_x[simp]: fixes x :: "'a :: comm_ring_1" shows "poly2 y_x x y = y - x" unfolding poly2_def by simp private definition "poly_y_minus_x p ≡ poly_lift p ∘⇩_{p}y_x" private lemma poly_y_minus_x_0[simp]: "poly_y_minus_x 0 = 0" by (simp add: poly_y_minus_x_def) private lemma poly_y_minus_x_pCons[simp]: "poly_y_minus_x (pCons a p) = [:[: a :]:] + poly_y_minus_x p * y_x" by (simp add: poly_y_minus_x_def) private lemma poly_y_x_poly_x_minus_y: fixes p :: "'a :: idom poly" shows "poly_y_x (poly_x_minus_y p) = poly_y_minus_x p" apply (induct p, simp) apply (unfold poly_x_minus_y_pCons hom_distribs) by simp lemma degree_poly_y_minus_x[simp]: fixes p :: "'a :: idom poly" shows "degree (poly_y_x (poly_x_minus_y p)) = degree p" by (simp add: poly_y_minus_x_def poly_y_x_poly_x_minus_y) end lemma dvd_all_coeffs_iff: fixes x :: "'a :: comm_semiring_1" (* No addition needed! *) shows "(∀pi ∈ set (coeffs p). x dvd pi) ⟷ (∀i. x dvd coeff p i)" (is "?l = ?r") proof- have "?r = (∀i∈{..degree p} ∪ {Suc (degree p)..}. x dvd coeff p i)" by auto also have "... = (∀i≤degree p. x dvd coeff p i)" by (auto simp add: ball_Un coeff_eq_0) also have "... = ?l" by (auto simp: coeffs_def) finally show ?thesis.. qed lemma primitive_imp_no_constant_factor: fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly" assumes pr: "primitive p" and F: "mset_factors F p" and fF: "f ∈# F" shows "degree f ≠ 0" proof from F fF have irr: "irreducible f" and fp: "f dvd p" by (auto dest: mset_factors_imp_dvd) assume deg: "degree f = 0" then obtain f0 where f0: "f = [:f0:]" by (auto dest: degree0_coeffs) with fp have "[:f0:] dvd p" by simp then have "f0 dvd coeff p i" for i by (simp add: const_poly_dvd_iff) with primitiveD[OF pr] dvd_all_coeffs_iff have "f0 dvd 1" by (auto simp: coeffs_def) with f0 irr show False by auto qed lemma coprime_poly_x_minus_y_poly_lift: fixes p q :: "'a :: ufd poly" assumes degp: "degree p > 0" and degq: "degree q > 0" and pr: "primitive p" shows "coprime (poly_x_minus_y p) (poly_lift q)" proof(rule ccontr) from degp have p: "¬ p dvd 1" by (auto simp: dvd_const) from degp have p0: "p ≠ 0" by auto from mset_factors_exist[of p, OF p0 p] obtain F where F: "mset_factors F p" by auto with poly_x_minus_y_hom.hom_mset_factors have pF: "mset_factors (image_mset poly_x_minus_y F) (poly_x_minus_y p)" by auto from degq have q: "¬ q dvd 1" by (auto simp: dvd_const) from degq have q0: "q ≠ 0" by auto from mset_factors_exist[OF q0 q] obtain G where G: "mset_factors G q" by auto with poly_lift_hom.hom_mset_factors have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto assume "¬ coprime (poly_x_minus_y p) (poly_lift q)" from this[unfolded not_coprime_iff_common_factor] obtain r where rp: "r dvd (poly_x_minus_y p)" and rq: "r dvd (poly_lift q)" and rU: "¬ r dvd 1" by auto note poly_lift_hom.hom_dvd from rp p0 have r0: "r ≠ 0" by auto from mset_factors_exist[OF r0 rU] obtain H where H: "mset_factors H r" by auto then have "H ≠ {#}" by auto then obtain h where hH: "h ∈# H" by fastforce with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto from hr rp have "h dvd (poly_x_minus_y p)" by (rule dvd_trans) from irreducible_dvd_imp_factor[OF this h pF] p0 obtain f where f: "f ∈# F" and fh: "poly_x_minus_y f ddvd h" by auto from hr rq have "h dvd (poly_lift q)" by (rule dvd_trans) from irreducible_dvd_imp_factor[OF this h pG] q0 obtain g where g: "g ∈# G" and gh: "poly_lift g ddvd h" by auto from fh gh have "poly_x_minus_y f ddvd poly_lift g" using ddvd_trans by auto then have "poly_y_x (poly_x_minus_y f) ddvd poly_y_x (poly_lift g)" by simp also have "poly_y_x (poly_lift g) = [:g:]" unfolding poly_y_x_poly_lift monom_0 by auto finally have ddvd: "poly_y_x (poly_x_minus_y f) ddvd [:g:]" by auto then have "degree (poly_y_x (poly_x_minus_y f)) = 0" by (metis degree_pCons_0 dvd_0_left_iff dvd_const) then have "degree f = 0" by simp with primitive_imp_no_constant_factor[OF pr F f] show False by auto qed lemma poly_add_nonzero: fixes p q :: "'a :: ufd poly" assumes p0: "p ≠ 0" and q0: "q ≠ 0" and x: "poly p x = 0" and y: "poly q y = 0" and pr: "primitive p" shows "poly_add p q ≠ 0" proof have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I) have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I) assume 0: "poly_add p q = 0" from resultant_zero_imp_common_factor[OF _ this[unfolded poly_add_def]] degp and coprime_poly_x_minus_y_poly_lift[OF degp degq pr] show False by auto qed subsubsection ‹Summary for addition› text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.› lemma (in comm_ring_hom) map_poly_x_minus_y: "map_poly (map_poly hom) (poly_x_minus_y p) = poly_x_minus_y (map_poly hom p)" proof- interpret mp: map_poly_comm_ring_hom hom.. interpret mmp: map_poly_comm_ring_hom "map_poly hom".. show ?thesis apply (induct p, simp) apply(unfold x_y_def hom_distribs poly_x_minus_y_pCons, simp) done qed lemma (in comm_ring_hom) hom_poly_lift[simp]: "map_poly (map_poly hom) (poly_lift q) = poly_lift (map_poly hom q)" proof - show ?thesis unfolding poly_lift_def unfolding map_poly_map_poly[of coeff_lift,OF coeff_lift_hom.hom_zero] unfolding map_poly_coeff_lift_hom by simp qed lemma lead_coeff_poly_x_minus_y: fixes p :: "'a::idom poly" shows "lead_coeff (poly_x_minus_y p) = [:lead_coeff p * ((- 1) ^ degree p):]" (is "?l = ?r") proof- have "?l = Polynomial.smult (lead_coeff p) ((- 1) ^ degree p)" by (unfold poly_x_minus_y_def, subst lead_coeff_comp; simp add: x_y_def) also have "... = ?r" by (unfold hom_distribs, simp add: smult_as_map_poly[symmetric]) finally show ?thesis. qed lemma degree_coeff_poly_x_minus_y: fixes p q :: "'a :: {idom, semiring_char_0} poly" shows "degree (coeff (poly_x_minus_y p) i) = degree p - i" proof - consider "i = degree p" | "i > degree p" | "i < degree p" by force thus ?thesis proof cases assume "i > degree p" thus ?thesis by (subst coeff_eq_0) auto next assume "i = degree p" thus ?thesis using lead_coeff_poly_x_minus_y[of p] by (simp add: lead_coeff_poly_x_minus_y) next assume "i < degree p" define n where "n = degree p" have "degree (coeff (poly_x_minus_y p) i) = degree (∑j≤n. [:coeff p j:] * coeff (x_y ^ j) i)" (is "_ = degree (sum ?f _)") by (simp add: poly_x_minus_y_def pcompose_conv_poly poly_altdef coeff_sum n_def) also have "{..n} = insert n {..<n}" by auto also have "sum ?f … = ?f n + sum ?f {..<n}" by (subst sum.insert) auto also have "degree … = n - i" proof - have "degree (?f n) = n - i" using ‹i < degree p› by (simp add: n_def coeff_xy_power degree_monom_eq) moreover have "degree (sum ?f {..<n}) < n - i" proof (intro degree_sum_smaller) fix j assume "j ∈ {..<n}" have "degree ([:coeff p j:] * coeff (x_y ^ j) i) ≤ j - i" proof (cases "i ≤ j") case True thus ?thesis by (auto simp: n_def coeff_xy_power degree_monom_eq) next case False hence "coeff (x_y ^ j :: 'a poly poly) i = 0" by (subst coeff_eq_0) (auto simp: degree_power_eq) thus ?thesis by simp qed also have "… < n - i" using ‹j ∈ {..<n}› ‹i < degree p› by (auto simp: n_def) finally show "degree ([:coeff p j:] * coeff (x_y ^ j) i) < n - i" . qed (use ‹i < degree p› in ‹auto simp: n_def›) ultimately show ?thesis by (subst degree_add_eq_left) auto qed finally show ?thesis by (simp add: n_def) qed qed lemma coeff_0_poly_x_minus_y [simp]: "coeff (poly_x_minus_y p) 0 = p" by (induction p) (auto simp: poly_x_minus_y_def x_y_def) lemma (in idom_hom) poly_add_hom: assumes p0: "hom (lead_coeff p) ≠ 0" and q0: "hom (lead_coeff q) ≠ 0" shows "map_poly hom (poly_add p q) = poly_add (map_poly hom p) (map_poly hom q)" proof - interpret mh: map_poly_idom_hom.. show ?thesis unfolding poly_add_def apply (subst mh.resultant_map_poly(1)[symmetric]) apply (subst degree_map_poly_2) apply (unfold lead_coeff_poly_x_minus_y, unfold hom_distribs, simp add: p0) apply simp apply (subst degree_map_poly_2) apply (simp_all add: q0 map_poly_x_minus_y) done qed lemma(in zero_hom) hom_lead_coeff_nonzero_imp_map_poly_hom: assumes "hom (lead_coeff p) ≠ 0" shows "map_poly hom p ≠ 0" proof assume "map_poly hom p = 0" then have "coeff (map_poly hom p) (degree p) = 0" by simp with assms show False by simp qed lemma ipoly_poly_add: fixes x y :: "'a :: idom" assumes p0: "(of_int (lead_coeff p) :: 'a) ≠ 0" and q0: "(of_int (lead_coeff q) :: 'a) ≠ 0" and x: "ipoly p x = 0" and y: "ipoly q y = 0" shows "ipoly (poly_add p q) (x+y) = 0" using assms of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom[OF q0] by (auto intro: poly_add simp: of_int_hom.poly_add_hom[OF p0 q0]) lemma (in comm_monoid_gcd) gcd_list_eq_0_iff[simp]: "listgcd xs = 0 ⟷ (∀x ∈ set xs. x = 0)" by (induct xs, auto) lemma primitive_field_poly[simp]: "primitive (p :: 'a :: field poly) ⟷ p ≠ 0" by (unfold primitive_iff_some_content_dvd_1,auto simp: dvd_field_iff coeffs_def) lemma ipoly_poly_add_nonzero: fixes x y :: "'a :: field" assumes "p ≠ 0" and "q ≠ 0" and "ipoly p x = 0" and "ipoly q y = 0" and "(of_int (lead_coeff p) :: 'a) ≠ 0" and "(of_int (lead_coeff q) :: 'a) ≠ 0" shows "poly_add p q ≠ 0" proof- from assms have "(of_int_poly (poly_add p q) :: 'a poly) ≠ 0" apply (subst of_int_hom.poly_add_hom,simp,simp) by (rule poly_add_nonzero, auto dest:of_int_hom.hom_lead_coeff_nonzero_imp_map_poly_hom) then show ?thesis by auto qed lemma represents_add: assumes x: "p represents x" and y: "q represents y" shows "(poly_add p q) represents (x + y)" using assms by (intro representsI ipoly_poly_add ipoly_poly_add_nonzero, auto) subsection ‹Division of Algebraic Numbers› definition poly_x_mult_y where [code del]: "poly_x_mult_y p ≡ (∑ i ≤ degree p. monom (monom (coeff p i) i) i)" lemma coeff_poly_x_mult_y: shows "coeff (poly_x_mult_y p) i = monom (coeff p i) i" (is "?l = ?r") proof(cases "degree p < i") case i: False have "?l = sum (λj. if j = i then (monom (coeff p j) j) else 0) {..degree p}" (is "_ = sum ?f ?A") by (simp add: poly_x_mult_y_def coeff_sum) also have "... = sum ?f {i}" using i by (intro sum.mono_neutral_right, auto) also have "... = ?f i" by simp also have "... = ?r" by auto finally show ?thesis. next case True then show ?thesis by (auto simp: poly_x_mult_y_def coeff_eq_0 coeff_sum) qed lemma poly_x_mult_y_code[code]: "poly_x_mult_y p = (let cs = coeffs p in poly_of_list (map (λ (i, ai). monom ai i) (zip [0 ..< length cs] cs)))" unfolding Let_def poly_of_list_def proof (rule poly_eqI, unfold coeff_poly_x_mult_y) fix n let ?xs = "zip [0..<length (coeffs p)] (coeffs p)" let ?f = "(λ(i, ai). monom ai i)" show "monom (coeff p n) n = coeff (Poly (map ?f ?xs)) n" proof (cases "n < length (coeffs p)") case True hence n: "n < length (map ?f ?xs)" and nn: "n < length ?xs" unfolding degree_eq_length_coeffs by auto show ?thesis unfolding coeff_Poly nth_default_nth[OF n] nth_map[OF nn] using True by (simp add: nth_coeffs_coeff) next case False hence id: "coeff (Poly (map ?f ?xs)) n = 0" unfolding coeff_Poly by (subst nth_default_beyond, auto) from False have "n > degree p ∨ p = 0" unfolding degree_eq_length_coeffs by (cases n, auto) hence "monom (coeff p n) n = 0" using coeff_eq_0[of p n] by auto thus ?thesis unfolding id by simp qed qed definition poly_div :: "'a :: comm_ring_1 poly ⇒ 'a poly ⇒ 'a poly" where "poly_div p q = resultant (poly_x_mult_y p) (poly_lift q)" text ‹@{const poly_div} has desired roots.› lemma poly2_poly_x_mult_y: fixes p :: "'a :: comm_ring_1 poly" shows "poly2 (poly_x_mult_y p) x y = poly p (x * y)" apply (subst(3) poly_as_sum_of_monoms[symmetric]) apply (unfold poly_x_mult_y_def hom_distribs) by (auto simp: poly2_monom poly_monom power_mult_distrib ac_simps) lemma poly_div: fixes p q :: "'a ::field poly" assumes q0: "q ≠ 0" and x: "poly p x = 0" and y: "poly q y = 0" and y0: "y ≠ 0" shows "poly (poly_div p q) (x/y) = 0" proof (unfold poly_div_def, rule poly_resultant_zero[OF disjI2]) have "degree q > 0" using poly_zero q0 y by auto thus degq: "degree (poly_lift q) > 0" by auto qed (insert x y y0, simp_all add: poly2_poly_x_mult_y) text ‹@{const poly_div} is nonzero.› interpretation poly_x_mult_y_hom: ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly ⇒ _" by (unfold_locales, auto intro: poly2_ext simp: poly2_poly_x_mult_y hom_distribs) interpretation poly_x_mult_y_hom: inj_ring_hom "poly_x_mult_y :: 'a :: {idom,ring_char_0} poly ⇒ _" proof let ?h = poly_x_mult_y fix f :: "'a poly" assume "?h f = 0" then have "poly2 (?h f) x 1 = 0" for x by simp from this[unfolded poly2_poly_x_mult_y] show "f = 0" by auto qed lemma degree_poly_x_mult_y[simp]: fixes p :: "'a :: {idom, ring_char_0} poly" shows "degree (poly_x_mult_y p) = degree p" (is "?l = ?r") proof(rule antisym) show "?r ≤ ?l" by (cases "p=0", auto intro: le_degree simp: coeff_poly_x_mult_y) show "?l ≤ ?r" unfolding poly_x_mult_y_def by (auto intro: degree_sum_le le_trans[OF degree_monom_le]) qed interpretation poly_x_mult_y_hom: unit_preserving_hom "poly_x_mult_y :: 'a :: field_char_0 poly ⇒ _" proof(unfold_locales) let ?h = "poly_x_mult_y :: 'a poly ⇒ _" fix f :: "'a poly" assume unit: "?h f dvd 1" then have "degree (?h f) = 0" and "coeff (?h f) 0 dvd 1" unfolding poly_dvd_1 by auto then have deg: "degree f = 0" by (auto simp add: degree_monom_eq) with unit show "f dvd 1" by(cases "f = 0", auto) qed lemmas poly_y_x_o_poly_lift = o_def[of poly_y_x poly_lift, unfolded poly_y_x_poly_lift] lemma irreducible_dvd_degree: assumes "(f::'a::field poly) dvd g" "irreducible g" "degree f > 0" shows "degree f = degree g" using assms by (metis irreducible_altdef degree_0 dvd_refl is_unit_field_poly linorder_neqE_nat poly_divides_conv0) lemma coprime_poly_x_mult_y_poly_lift: fixes p q :: "'a :: field_char_0 poly" assumes degp: "degree p > 0" and degq: "degree q > 0" and nz: "poly p 0 ≠ 0 ∨ poly q 0 ≠ 0" shows "coprime (poly_x_mult_y p) (poly_lift q)" proof(rule ccontr) from degp have p: "¬ p dvd 1" by (auto simp: dvd_const) from degp have p0: "p ≠ 0" by auto from mset_factors_exist[of p, OF p0 p] obtain F where F: "mset_factors F p" by auto then have pF: "prod_mset (image_mset poly_x_mult_y F) = poly_x_mult_y p" by (auto simp: hom_distribs) from degq have q: "¬ is_unit q" by (auto simp: dvd_const) from degq have q0: "q ≠ 0" by auto from mset_factors_exist[OF q0 q] obtain G where G: "mset_factors G q" by auto with poly_lift_hom.hom_mset_factors have pG: "mset_factors (image_mset poly_lift G) (poly_lift q)" by auto from poly_y_x_hom.hom_mset_factors[OF this] have pG: "mset_factors (image_mset coeff_lift G) [:q:]" by (auto simp: poly_y_x_poly_lift monom_0 image_mset.compositionality poly_y_x_o_poly_lift) assume "¬ coprime (poly_x_mult_y p) (poly_lift q)" then have "¬ coprime (poly_y_x (poly_x_mult_y p)) (poly_y_x (poly_lift q))" by (simp del: coprime_iff_coprime) from this[unfolded not_coprime_iff_common_factor] obtain r where rp: "r dvd poly_y_x (poly_x_mult_y p)" and rq: "r dvd poly_y_x (poly_lift q)" and rU: "¬ r dvd 1" by auto from rp p0 have r0: "r ≠ 0" by auto from mset_factors_exist[OF r0 rU] obtain H where H: "mset_factors H r" by auto then have "H ≠ {#}" by auto then obtain h where hH: "h ∈# H" by fastforce with H mset_factors_imp_dvd have hr: "h dvd r" and h: "irreducible h" by auto from irreducible_not_unit[OF h] have hU: "¬ h dvd 1" by auto from hr rp have "h dvd poly_y_x (poly_x_mult_y p)" by (rule dvd_trans) note this[folded pF,unfolded poly_y_x_hom.hom_prod_mset image_mset.compositionality] from prime_elem_dvd_prod_mset[OF h[folded prime_elem_iff_irreducible] this] obtain f where f: "f ∈# F" and hf: "h dvd poly_y_x (poly_x_mult_y f)" by auto have irrF: "irreducible f" using f F by blast from dvd_trans[OF hr rq] have "h dvd [:q:]" by (simp add: poly_y_x_poly_lift monom_0) from irreducible_dvd_imp_factor[OF this h pG] q0 obtain g where g: "g ∈# G" and gh: "[:g:] dvd h" by auto from dvd_trans[OF gh hf] have *: "[:g:] dvd poly_y_x (poly_x_mult_y f)" using dvd_trans by auto show False proof (cases "poly f 0 = 0") case f_0: False from poly_hom.hom_dvd[OF *] have "g dvd poly (poly_y_x (poly_x_mult_y f)) [:0:]" by simp also have "... = [:poly f 0:]" by (intro poly_ext, fold poly2_def, simp add: poly2_poly_x_mult_y) also have "... dvd 1" using f_0 by auto finally have "g dvd 1". with g G show False by (auto elim!: mset_factorsE dest!: irreducible_not_unit) next case True hence "[:0,1:] dvd f" by (unfold dvd_iff_poly_eq_0, simp) from irreducible_dvd_degree[OF this irrF] have "degree f = 1" by auto from degree1_coeffs[OF this] True obtain c where c: "c ≠ 0" and f: "f = [:0,c:]" by auto from g G have irrG: "irreducible g" by auto from poly_hom.hom_dvd[OF *] have "g dvd poly (poly_y_x (poly_x_mult_y f)) 1" by simp also have "… = f" by (auto simp: f poly_x_mult_y_code Let_def c poly_y_x_pCons map_poly_monom poly_monom poly_lift_def) also have "… dvd [:0,1:]" unfolding f dvd_def using c by (intro exI[of _ "[: inverse c :]"], auto) finally have g01: "g dvd [:0,1:]" . from divides_degree[OF this] irrG have "degree g = 1" by auto from degree1_coeffs[OF this] obtain a b where g: "g = [:b,a:]" and a: "a ≠ 0" by auto from g01[unfolded dvd_def] g obtain k where id: "[:0,1:] = g * k" by auto from id have 0: "g ≠ 0" "k ≠ 0" by auto from arg_cong[OF id, of degree] have "degree k = 0" unfolding degree_mult_eq[OF 0] unfolding g using a by auto from degree0_coeffs[OF this] obtain kk where k: "k = [:kk:]" by auto from id[unfolded g k] a have "b = 0" by auto hence "poly g 0 = 0" by (auto simp: g) from True this nz ‹f ∈# F› ‹g ∈# G› F G show False by (auto dest!:mset_factors_imp_dvd elim:dvdE) qed qed lemma poly_div_nonzero: fixes p q :: "'a :: field_char_0 poly" assumes p0: "p ≠ 0" and q0: "q ≠ 0" and x: "poly p x = 0" and y: "poly q y = 0" and p_0: "poly p 0 ≠ 0 ∨ poly q 0 ≠ 0" shows "poly_div p q ≠ 0" proof have degp: "degree p > 0" using le_0_eq order_degree order_root p0 x by (metis gr0I) have degq: "degree q > 0" using le_0_eq order_degree order_root q0 y by (metis gr0I) assume 0: "poly_div p q = 0" from resultant_zero_imp_common_factor[OF _ this[unfolded poly_div_def]] degp and coprime_poly_x_mult_y_poly_lift[OF degp degq] p_0 show False by auto qed subsubsection ‹Summary for division› text ‹Now we lift the results to one that uses @{const ipoly}, by showing some homomorphism lemmas.› lemma (in inj_comm_ring_hom) poly_x_mult_y_hom: "poly_x_mult_y (map_poly hom p) = map_poly (map_poly hom) (poly_x_mult_y p)" proof - interpret mh: map_poly_inj_comm_ring_hom.. interpret mmh: map_poly_inj_comm_ring_hom "map_poly hom".. show ?thesis unfolding poly_x_mult_y_def by (simp add: hom_distribs) qed lemma (in inj_comm_ring_hom) poly_div_hom: "map_poly hom (poly_div p q) = poly_div (map_poly hom p) (map_poly hom q)" proof - have zero: "∀x. hom x = 0 ⟶ x = 0" by simp interpret mh: map_poly_inj_comm_ring_hom.. show ?thesis unfolding poly_div_def mh.resultant_hom[symmetric] by (simp add: poly_x_mult_y_hom) qed lemma ipoly_poly_div: fixes x y :: "'a :: field_char_0" assumes "q ≠ 0" and "ipoly p x = 0" and "ipoly q y = 0" and "y ≠ 0" shows "ipoly (poly_div p q) (x/y) = 0" by (unfold of_int_hom.poly_div_hom, rule poly_div, insert assms, auto) lemma ipoly_poly_div_nonzero: fixes x y :: "'a :: field_char_0" assumes "p ≠ 0" and "q ≠ 0" and "ipoly p x = 0" and "ipoly q y = 0" and "poly p 0 ≠ 0 ∨ poly q 0 ≠ 0" shows "poly_div p q ≠ 0" proof- from assms have "(of_int_poly (poly_div p q) :: 'a poly) ≠ 0" using of_int_hom.poly_map_poly[of p] by (subst of_int_hom.poly_div_hom, subst poly_div_nonzero, auto) then show ?thesis by auto qed lemma represents_div: fixes x y :: "'a :: field_char_0" assumes "p represents x" and "q represents y" and "poly q 0 ≠ 0" shows "(poly_div p q) represents (x / y)" using assms by (intro representsI ipoly_poly_div ipoly_poly_div_nonzero, auto) subsection ‹Multiplication of Algebraic Numbers› definition poly_mult where "poly_mult p q ≡ poly_div p (reflect_poly q)" lemma represents_mult: assumes px: "p represents x" and qy: "q represents y" and q_0: "poly q 0 ≠ 0" shows "(poly_mult p q) represents (x * y)" proof- from q_0 qy have y0: "y ≠ 0" by auto from represents_inverse[OF y0 qy] y0 px q_0 have "poly_mult p q represents x / (inverse y)" unfolding poly_mult_def by (intro represents_div, auto) with y0 show ?thesis by (simp add: field_simps) qed subsection ‹Summary: Closure Properties of Algebraic Numbers› lemma algebraic_representsI: "p represents x ⟹ algebraic x" unfolding represents_def algebraic_altdef_ipoly by auto lemma algebraic_of_rat: "algebraic (of_rat x)" by (rule algebraic_representsI[OF poly_rat_represents_of_rat]) lemma algebraic_uminus: "algebraic x ⟹ algebraic (-x)" by (auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_uminus) lemma algebraic_inverse: "algebraic x ⟹ algebraic (inverse x)" using algebraic_of_rat[of 0] by (cases "x = 0", auto dest: algebraic_imp_represents_irreducible intro: algebraic_representsI represents_inverse) lemma algebraic_plus: "algebraic x ⟹ algebraic y ⟹ algebraic (x + y)" by (auto dest!: algebraic_imp_represents_irreducible_cf_pos intro!: algebraic_representsI[OF represents_add]) lemma algebraic_div: assumes x: "algebraic x" and y: "algebraic y" shows "algebraic (x/y)" proof(cases "y = 0 ∨ x = 0") case True then show ?thesis using algebraic_of_rat[of 0] by auto next case False then have x0: "x ≠ 0" and y0: "y ≠ 0" by auto from x y obtain p q where px: "p represents x" and irr: "irreducible q" and qy: "q represents y" by (auto dest!: algebraic_imp_represents_irreducible) show ?thesis using False px represents_irr_non_0[OF irr qy] by (auto intro!: algebraic_representsI[OF represents_div] qy) qed lemma algebraic_times: "algebraic x ⟹ algebraic y ⟹ algebraic (x * y)" using algebraic_div[OF _ algebraic_inverse, of x y] by (simp add: field_simps) lemma algebraic_root: "algebraic x ⟹ algebraic (root n x)" proof - assume "algebraic x" then obtain p where p: "p represents x" by (auto dest: algebraic_imp_represents_irreducible_cf_pos) from algebraic_representsI[OF represents_nth_root_neg_real[OF _ this, of n]] algebraic_representsI[OF represents_nth_root_pos_real[OF _ this, of n]] algebraic_of_rat[of 0] show ?thesis by (cases "n = 0", force, cases "n > 0", force, cases "n < 0", auto) qed lemma algebraic_nth_root: "n ≠ 0 ⟹ algebraic x ⟹ y^n = x ⟹ algebraic y" by (auto dest: algebraic_imp_represents_irreducible_cf_pos intro: algebraic_representsI represents_nth_root) subsection ‹More on algebraic integers› (* TODO: this is actually equal to @{term "(-1)^(m*n)"}, but we need a bit more theory on permutations to show this with a reasonable amount of effort. *) definition poly_add_sign :: "nat ⇒ nat ⇒ 'a :: comm_ring_1" where "poly_add_sign m n = signof (λi. if i < n then m + i else if i < m + n then i - n else i)" lemma lead_coeff_poly_add: fixes p q :: "'a :: {idom, semiring_char_0} poly" defines "m ≡ degree p" and "n ≡ degree q" assumes "lead_coeff p = 1" "lead_coeff q = 1" "m > 0" "n > 0" shows "lead_coeff (poly_add p q :: 'a poly) = poly_add_sign m n" proof - from assms have [simp]: "p ≠ 0" "q ≠ 0" by auto define M where "M = sylvester_mat (poly_x_minus_y p) (poly_lift q)" define π :: "nat ⇒ nat" where "π = (λi. if i < n then m + i else if i < m + n then i - n else i)" have π: "π permutes {0..<m+n}" by (rule inj_on_nat_permutes) (auto simp: π_def inj_on_def) have nz: "M $$ (i, π i) ≠ 0" if "i < m + n" for i using that by (auto simp: M_def π_def sylvester_index_mat m_def n_def) (* have "{(i,j). i ∈ {..<m+n} ∧ j ∈ {..<m+n} ∧ i < j ∧ π i > π j} = {..<n} × {n..<m+n}" (is "?lhs = ?rhs") proof (intro equalityI subsetI) fix ij assume "ij ∈ ?lhs" thus "ij ∈ ?rhs" by (simp add: π_def split: prod.splits if_splits) auto qed (auto simp: π_def) hence "inversions_on {..<m+n} π = n * m" by (simp add: inversions_on_def) hence "signof π = (-1)^(m*n)" using π by (simp add: signof_def sign_def evenperm_iff_even_inversions) *) have indices_eq: "{0..<m+n} = {..<n} ∪ (+) n ` {..<m}" by (auto simp flip: atLeast0LessThan) define f where "f = (λ σ. signof σ * (∏i=0..<m+n. M $$ (i, σ i)))" have "degree (f π) = degree (∏i=0..<m + n. M $$ (i, π i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "… = (∑i=0..<m+n. degree (M $$ (i, π i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "… = (∑i<n. degree (M $$ (i, π i))) + (∑i<m. degree (M $$ (n + i, π (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(∑i<n. degree (M $$ (i, π i))) = (∑i<n. m)" by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def) also have "(∑i<m. degree (M $$ (n + i, π (n + i)))) = (∑i<m. 0)" by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def) finally have deg_f1: "degree (f π) = m * n" by simp have deg_f2: "degree (f σ) < m * n" if "σ permutes {0..<m+n}" "σ ≠ π" for σ proof (cases "∃i∈{0..<m+n}. M $$ (i, σ i) = 0") case True hence *: "(∏i = 0..<m + n. M $$ (i, σ i)) = 0" by auto show ?thesis using ‹m > 0› ‹n > 0› by (simp add: f_def *) next case False note nz = this from that have σ_less: "σ i < m + n" if "i < m + n" for i using permutes_in_image[OF ‹σ permutes _›] that by auto have "degree (f σ) = degree (∏i=0..<m + n. M $$ (i, σ i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "… = (∑i=0..<m+n. degree (M $$ (i, σ i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "… = (∑i<n. degree (M $$ (i, σ i))) + (∑i<m. degree (M $$ (n + i, σ (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(∑i<m. degree (M $$ (n + i, σ (n + i)))) = (∑i<m. 0)" using σ_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat π_def m_def n_def) also have "(∑i<n. degree (M $$ (i, σ i))) < (∑i<n. m)" proof (rule sum_strict_mono_ex1) show "∀x∈{..<n}. degree (M $$ (x, σ x)) ≤ m" using σ_less by (auto simp: M_def sylvester_index_mat π_def m_def n_def degree_coeff_poly_x_minus_y) next have "∃i<n. σ i ≠ π i" proof (rule ccontr) assume nex: "~(∃i<n. σ i ≠ π i)" have "∀i≥m+n-k. σ i = π i" if "k ≤ m" for k using that proof (induction k) case 0 thus ?case using ‹π permutes _› ‹σ permutes _› by (fastforce simp: permutes_def) next case (Suc k) have IH: "σ i = π i" if "i ≥ m+n-k" for i using Suc.prems Suc.IH that by auto from nz have "M $$ (m + n - Suc k, σ (m + n - Suc k)) ≠ 0" using Suc.prems by auto moreover have "m + n - Suc k ≥ n" using Suc.prems by auto ultimately have "σ (m+n-Suc k) ≥ m-Suc k" using assms σ_less[of "m+n-Suc k"] Suc.prems by (auto simp: M_def sylvester_index_mat m_def n_def split: if_splits) have "¬(σ (m+n-Suc k) > m - Suc k)" proof assume *: "σ (m+n-Suc k) > m - Suc k" have less: "σ (m+n-Suc k) < m" proof (rule ccontr) assume *: "¬σ (m + n - Suc k) < m" define j where "j = σ (m + n - Suc k) - m" have "σ (m + n - Suc k) = m + j" using * by (simp add: j_def) moreover { have "j < n" using σ_less[of "m+n-Suc k"] ‹m > 0› ‹n > 0› by (simp add: j_def) hence "σ j = π j" using nex by auto with ‹j < n› have "σ j = m + j" by (auto simp: π_def) } ultimately have "σ (m + n - Suc k) = σ j" by simp hence "m + n - Suc k = j" using permutes_inj[OF ‹σ permutes _›] unfolding inj_def by blast thus False using ‹n ≤ m + n - Suc k› σ_less[of "m+n-Suc k"] ‹n > 0› unfolding j_def by linarith qed define j where "j = σ (m+n-Suc k) - (m - Suc k)" from * have j: "σ (m+n-Suc k) = m - Suc k + j" "j > 0" by (auto simp: j_def) have "σ (m+n-Suc k + j) = π (m+n - Suc k + j)" using * by (intro IH) (auto simp: j_def) also { have "j < Suc k" using less by (auto simp: j_def algebra_simps) hence "m + n - Suc k + j < m + n" using ‹m > 0› ‹n > 0› Suc.prems by linarith hence "π (m +n - Suc k + j) = m - Suc k + j" unfolding π_def using Suc.prems by (simp add: π_def) } finally have "σ (m + n - Suc k + j) = σ (m + n - Suc k)" using j by simp hence "m + n - Suc k + j = m + n - Suc k" using permutes_inj[OF ‹σ permutes _›] unfolding inj_def by blast thus False using ‹j > 0› by simp qed with ‹σ (m+n-Suc k) ≥ m-Suc k› have eq: "σ (m+n-Suc k) = m - Suc k" by linarith show ?case proof safe fix i :: nat assume i: "i ≥ m + n - Suc k" show "σ i = π i" using eq Suc.prems ‹m > 0› IH i proof (cases "i = m + n - Suc k") case True thus ?thesis using eq Suc.prems ‹m > 0› by (auto simp: π_def) qed (use IH i in auto) qed qed from this[of m] and nex have "σ i = π i" for i by (cases "i ≥ n") auto hence "σ = π" by force thus False using ‹σ ≠ π› by contradiction qed then obtain i where i: "i < n" "σ i ≠ π i" by auto have "σ i < m + n" using i by (intro σ_less) auto moreover have "π i = m + i" using i by (auto simp: π_def) ultimately have "degree (M $$ (i, σ i)) < m" using i ‹m > 0› by (auto simp: M_def m_def n_def sylvester_index_mat degree_coeff_poly_x_minus_y) thus "∃i∈{..<n}. degree (M $$ (i, σ i)) < m" using i by blast qed auto finally show "degree (f σ) < m * n" by (simp add: mult_ac) qed have "lead_coeff (f π) = poly_add_sign m n" proof - have "lead_coeff (f π) = signof π * (∏i=0..<m + n. lead_coeff (M $$ (i, π i)))" by (simp add: f_def sign_def lead_coeff_prod) also have "(∏i=0..<m + n. lead_coeff (M $$ (i, π i))) = (∏i<n. lead_coeff (M $$ (i, π i))) * (∏i<m. lead_coeff (M $$ (n + i, π (n + i))))" by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex) also have "(∏i<n. lead_coeff (M $$ (i, π i))) = (∏i<n. lead_coeff p)" by (intro prod.cong) (auto simp: M_def m_def n_def π_def sylvester_index_mat) also have "(∏i<m. lead_coeff (M $$ (n + i, π (n + i)))) = (∏i<m. lead_coeff q)" by (intro prod.cong) (auto simp: M_def m_def n_def π_def sylvester_index_mat) also have "signof π = poly_add_sign m n" by (simp add: π_def poly_add_sign_def m_def n_def cong: if_cong) finally show ?thesis using assms by simp qed have "lead_coeff (poly_add p q) = lead_coeff (det (sylvester_mat (poly_x_minus_y p) (poly_lift q)))" by (simp add: poly_add_def resultant_def) also have "det (sylvester_mat (poly_x_minus_y p) (poly_lift q)) = (∑π | π permutes {0..<m+n}. f π)" by (simp add: det_def m_def n_def M_def f_def) also have "{π. π permutes {0..<m+n}} = insert π ({π. π permutes {0..<m+n}} - {π})" using π by auto also have "(∑σ∈…. f σ) = (∑σ∈{σ. σ permutes {0..<m+n}}-{π}. f σ) + f π" by (subst sum.insert) (auto simp: finite_permutations) also have "lead_coeff … = lead_coeff (f π)" proof - have "degree (∑σ∈{σ. σ permutes {0..<m+n}}-{π}. f σ) < m * n" using assms by (intro degree_sum_smaller deg_f2) (auto simp: m_def n_def finite_permutations) with deg_f1 show ?thesis by (subst lead_coeff_add_le) auto qed finally show ?thesis using ‹lead_coeff (f π) = _› by simp qed lemma lead_coeff_poly_mult: fixes p q :: "'a :: {idom, ring_char_0} poly" defines "m ≡ degree p" and "n ≡ degree q" assumes "lead_coeff p = 1" "lead_coeff q = 1" "m > 0" "n > 0" assumes "coeff q 0 ≠ 0" shows "lead_coeff (poly_mult p q :: 'a poly) = 1" proof - from assms have [simp]: "p ≠ 0" "q ≠ 0" by auto have [simp]: "degree (reflect_poly q) = n" using assms by (subst degree_reflect_poly_eq) (auto simp: n_def) define M where "M = sylvester_mat (poly_x_mult_y p) (poly_lift (reflect_poly q))" have nz: "M $$ (i, i) ≠ 0" if "i < m + n" for i using that by (auto simp: M_def sylvester_index_mat m_def n_def coeff_poly_x_mult_y) have indices_eq: "{0..<m+n} = {..<n} ∪ (+) n ` {..<m}" by (auto simp flip: atLeast0LessThan) define f where "f = (λ σ. signof σ * (∏i=0..<m+n. M $$ (i, σ i)))" have "degree (f id) = degree (∏i=0..<m + n. M $$ (i, i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "… = (∑i=0..<m+n. degree (M $$ (i, i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "… = (∑i<n. degree (M $$ (i, i))) + (∑i<m. degree (M $$ (n + i, n + i)))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(∑i<n. degree (M $$ (i, i))) = (∑i<n. m)" by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def coeff_poly_x_mult_y degree_monom_eq) also have "(∑i<m. degree (M $$ (n + i, n + i))) = (∑i<m. 0)" by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def) finally have deg_f1: "degree (f id) = m * n" by (simp add: mult_ac id_def) have deg_f2: "degree (f σ) < m * n" if "σ permutes {0..<m+n}" "σ ≠ id" for σ proof (cases "∃i∈{0..<m+n}. M $$ (i, σ i) = 0") case True hence *: "(∏i = 0..<m + n. M $$ (i, σ i)) = 0" by auto show ?thesis using ‹m > 0› ‹n > 0› by (simp add: f_def *) next case False note nz = this from that have σ_less: "σ i < m + n" if "i < m + n" for i using permutes_in_image[OF ‹σ permutes _›] that by auto have "degree (f σ) = degree (∏i=0..<m + n. M $$ (i, σ i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "… = (∑i=0..<m+n. degree (M $$ (i, σ i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "… = (∑i<n. degree (M $$ (i, σ i))) + (∑i<m. degree (M $$ (n + i, σ (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(∑i<m. degree (M $$ (n + i, σ (n + i)))) = (∑i<m. 0)" using σ_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def) also have "(∑i<n. degree (M $$ (i, σ i))) < (∑i<n. m)" proof (rule sum_strict_mono_ex1) show "∀x∈{..<n}. degree (M $$ (x, σ x)) ≤ m" using σ_less by (auto simp: M_def sylvester_index_mat m_def n_def degree_coeff_poly_x_minus_y coeff_poly_x_mult_y intro: order.trans[OF degree_monom_le]) next have "∃i<n. σ i ≠ i" proof (rule ccontr) assume nex: "¬(∃i<n. σ i ≠ i)" have "σ i = i" for i using that proof (induction i rule: less_induct) case (less i) consider "i < n" | "i ∈ {n..<m+n}" | "i ≥ m + n" by force thus ?case proof cases assume "i < n" thus ?thesis using nex by auto next assume "i ≥ m + n" thus ?thesis using ‹σ permutes _› by (auto simp: permutes_def) next assume i: "i ∈ {n..<m+n}" have IH: "σ j = j" if "j < i" for j using that less.prems by (intro less.IH) auto from nz have "M $$ (i, σ i) ≠ 0" using i by auto hence "σ i ≤ i" using i σ_less[of i] by (auto simp: M_def sylvester_index_mat m_def n_def) moreover have "σ i ≥ i" proof (rule ccontr) assume *: "¬σ i ≥ i" from * have "σ (σ i) = σ i" by (subst IH) auto hence "σ i = i" using permutes_inj[OF ‹σ permutes _›] unfolding inj_def by blast with * show False by simp qed ultimately show ?case by simp qed qed hence "σ = id" by force with ‹σ ≠ id› show False by contradiction qed then obtain i where i: "i < n" "σ i ≠ i" by auto have "σ i < m + n" using i by (intro σ_less) auto hence "degree (M $$ (i, σ i)) < m" using i ‹m > 0› by (auto simp: M_def m_def n_def sylvester_index_mat degree_coeff_poly_x_minus_y coeff_poly_x_mult_y intro: le_less_trans[OF degree_monom_le]) thus "∃i∈{..<n}. degree (M $$ (i, σ i)) < m" using i by blast qed auto finally show "degree (f σ) < m * n" by (simp add: mult_ac) qed have "lead_coeff (f id) = 1" proof - have "lead_coeff (f id) = (∏i=0..<m + n. lead_coeff (M $$ (i, i)))" by (simp add: f_def lead_coeff_prod) also have "(∏i=0..<m + n. lead_coeff (M $$ (i, i))) = (∏i<n. lead_coeff (M $$ (i, i))) * (∏i<m. lead_coeff (M $$ (n + i, n + i)))" by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex) also have "(∏i<n. lead_coeff (M $$ (i, i))) = (∏i<n. lead_coeff p)" using assms by (intro prod.cong) (auto simp: M_def m_def n_def sylvester_index_mat coeff_poly_x_mult_y degree_monom_eq) also have "(∏i<m. lead_coeff (M $$ (n + i, n + i))) = (∏i<m. lead_coeff q)" by (intro prod.cong) (auto simp: M_def m_def n_def sylvester_index_mat) finally show ?thesis using assms by (simp add: id_def) qed have "lead_coeff (poly_mult p q) = lead_coeff (det M)" by (simp add: poly_mult_def resultant_def M_def poly_div_def) also have "det M = (∑π | π permutes {0..<m+n}. f π)" by (simp add: det_def m_def n_def M_def f_def) also have "{π. π permutes {0..<m+n}} = insert id ({π. π permutes {0..<m+n}}