(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Unique Factorization Domain for Polynomials› text ‹In this theory we prove that the polynomials over a unique factorization domain (UFD) form a UFD.› theory Unique_Factorization_Poly imports Unique_Factorization Polynomial_Factorization.Missing_Polynomial_Factorial Subresultants.More_Homomorphisms "HOL-Computational_Algebra.Field_as_Ring" begin hide_const (open) module.smult hide_const (open) Divisibility.irreducible instantiation fract :: (idom) "{normalization_euclidean_semiring, euclidean_ring}" begin definition [simp]: "normalize_fract ≡ (normalize_field :: 'a fract ⇒ _)" definition [simp]: "unit_factor_fract = (unit_factor_field :: 'a fract ⇒ _)" definition [simp]: "euclidean_size_fract = (euclidean_size_field :: 'a fract ⇒ _)" definition [simp]: "modulo_fract = (mod_field :: 'a fract ⇒ _)" instance by standard (simp_all add: dvd_field_iff divide_simps) end instantiation fract :: (idom) euclidean_ring_gcd begin definition gcd_fract :: "'a fract ⇒ 'a fract ⇒ 'a fract" where "gcd_fract ≡ Euclidean_Algorithm.gcd" definition lcm_fract :: "'a fract ⇒ 'a fract ⇒ 'a fract" where "lcm_fract ≡ Euclidean_Algorithm.lcm" definition Gcd_fract :: "'a fract set ⇒ 'a fract" where "Gcd_fract ≡ Euclidean_Algorithm.Gcd" definition Lcm_fract :: "'a fract set ⇒ 'a fract" where "Lcm_fract ≡ Euclidean_Algorithm.Lcm" instance by (standard, simp_all add: gcd_fract_def lcm_fract_def Gcd_fract_def Lcm_fract_def) end (*field + unique_euclidean_ring + euclidean_ring_gcd + normalization_semidom_multiplicative*) instantiation fract :: (idom) unique_euclidean_ring begin definition [simp]: "division_segment_fract (x :: 'a fract) = (1 :: 'a fract)" instance by standard (auto split: if_splits) end instance fract :: (idom) field_gcd by standard auto definition divides_ff :: "'a::idom fract ⇒ 'a fract ⇒ bool" where "divides_ff x y ≡ ∃ r. y = x * to_fract r" lemma ff_list_pairs: "∃ xs. X = map (λ (x,y). Fraction_Field.Fract x y) xs ∧ 0 ∉ snd ` set xs" proof (induct X) case (Cons a X) from Cons(1) obtain xs where X: "X = map (λ (x,y). Fraction_Field.Fract x y) xs" and xs: "0 ∉ snd ` set xs" by auto obtain x y where a: "a = Fraction_Field.Fract x y" and y: "y ≠ 0" by (cases a, auto) show ?case unfolding X a using xs y by (intro exI[of _ "(x,y) # xs"], auto) qed auto lemma divides_ff_to_fract[simp]: "divides_ff (to_fract x) (to_fract y) ⟷ x dvd y" unfolding divides_ff_def dvd_def by (simp add: to_fract_def eq_fract(1) mult.commute) lemma shows divides_ff_mult_cancel_left[simp]: "divides_ff (z * x) (z * y) ⟷ z = 0 ∨ divides_ff x y" and divides_ff_mult_cancel_right[simp]: "divides_ff (x * z) (y * z) ⟷ z = 0 ∨ divides_ff x y" unfolding divides_ff_def by auto definition gcd_ff_list :: "'a::ufd fract list ⇒ 'a fract ⇒ bool" where "gcd_ff_list X g = ( (∀ x ∈ set X. divides_ff g x) ∧ (∀ d. (∀ x ∈ set X. divides_ff d x) ⟶ divides_ff d g))" lemma gcd_ff_list_exists: "∃ g. gcd_ff_list (X :: 'a::ufd fract list) g" proof - interpret some_gcd: idom_gcd "(*)" "1 :: 'a" "(+)" 0 "(-)" uminus some_gcd rewrites "dvd.dvd ((*)) = (dvd)" by (unfold_locales, auto simp: dvd_rewrites) from ff_list_pairs[of X] obtain xs where X: "X = map (λ (x,y). Fraction_Field.Fract x y) xs" and xs: "0 ∉ snd ` set xs" by auto define r where "r ≡ prod_list (map snd xs)" have r: "r ≠ 0" unfolding r_def prod_list_zero_iff using xs by auto define ys where "ys ≡ map (λ (x,y). x * prod_list (remove1 y (map snd xs))) xs" { fix i assume "i < length X" hence i: "i < length xs" unfolding X by auto obtain x y where xsi: "xs ! i = (x,y)" by force with i have "(x,y) ∈ set xs" unfolding set_conv_nth by force hence y_mem: "y ∈ set (map snd xs)" by force with xs have y: "y ≠ 0" by force from i have id1: "ys ! i = x * prod_list (remove1 y (map snd xs))" unfolding ys_def using xsi by auto from i xsi have id2: "X ! i = Fraction_Field.Fract x y" unfolding X by auto have lp: "prod_list (remove1 y (map snd xs)) * y = r" unfolding r_def by (rule prod_list_remove1[OF y_mem]) have "ys ! i ∈ set ys" using i unfolding ys_def by auto moreover have "to_fract (ys ! i) = to_fract r * (X ! i)" unfolding id1 id2 to_fract_def mult_fract by (subst eq_fract(1), force, force simp: y, simp add: lp) ultimately have "ys ! i ∈ set ys" "to_fract (ys ! i) = to_fract r * (X ! i)" . } note ys = this define G where "G ≡ some_gcd.listgcd ys" define g where "g ≡ to_fract G * Fraction_Field.Fract 1 r" have len: "length X = length ys" unfolding X ys_def by auto show ?thesis proof (rule exI[of _ g], unfold gcd_ff_list_def, intro ballI conjI impI allI) fix x assume "x ∈ set X" then obtain i where i: "i < length X" and x: "x = X ! i" unfolding set_conv_nth by auto from ys[OF i] have id: "to_fract (ys ! i) = to_fract r * x" and ysi: "ys ! i ∈ set ys" unfolding x by auto from some_gcd.listgcd[OF ysi] have "G dvd ys ! i" unfolding G_def . then obtain d where ysi: "ys ! i = G * d" unfolding dvd_def by auto have "to_fract d * (to_fract G * Fraction_Field.Fract 1 r) = x * (to_fract r * Fraction_Field.Fract 1 r)" using id[unfolded ysi] by (simp add: ac_simps) also have "… = x" using r unfolding to_fract_def by (simp add: eq_fract One_fract_def) finally have "to_fract d * (to_fract G * Fraction_Field.Fract 1 r) = x" by simp thus "divides_ff g x" unfolding divides_ff_def g_def by (intro exI[of _ d], auto) next fix d assume "∀x ∈ set X. divides_ff d x" hence "Ball ((λ x. to_fract r * x) ` set X) ( divides_ff (to_fract r * d))" by simp also have "(λ x. to_fract r * x) ` set X = to_fract ` set ys" unfolding set_conv_nth using ys len by force finally have dvd: "Ball (set ys) (λ y. divides_ff (to_fract r * d) (to_fract y))" by auto obtain nd dd where d: "d = Fraction_Field.Fract nd dd" and dd: "dd ≠ 0" by (cases d, auto) { fix y assume "y ∈ set ys" hence "divides_ff (to_fract r * d) (to_fract y)" using dvd by auto from this[unfolded divides_ff_def d to_fract_def mult_fract] obtain ra where "Fraction_Field.Fract y 1 = Fraction_Field.Fract (r * nd * ra) dd" by auto hence "y * dd = ra * (r * nd)" by (simp add: eq_fract dd) hence "r * nd dvd y * dd" by auto } hence "r * nd dvd some_gcd.listgcd ys * dd" by (rule some_gcd.listgcd_greatest_mult) hence "divides_ff (to_fract r * d) (to_fract G)" unfolding to_fract_def d mult_fract G_def divides_ff_def by (auto simp add: eq_fract dd dvd_def) also have "to_fract G = to_fract r * g" unfolding g_def using r by (auto simp: to_fract_def eq_fract) finally show "divides_ff d g" using r by simp qed qed definition some_gcd_ff_list :: "'a :: ufd fract list ⇒ 'a fract" where "some_gcd_ff_list xs = (SOME g. gcd_ff_list xs g)" lemma some_gcd_ff_list: "gcd_ff_list xs (some_gcd_ff_list xs)" unfolding some_gcd_ff_list_def using gcd_ff_list_exists[of xs] by (rule someI_ex) lemma some_gcd_ff_list_divides: "x ∈ set xs ⟹ divides_ff (some_gcd_ff_list xs) x" using some_gcd_ff_list[of xs] unfolding gcd_ff_list_def by auto lemma some_gcd_ff_list_greatest: "(∀x ∈ set xs. divides_ff d x) ⟹ divides_ff d (some_gcd_ff_list xs)" using some_gcd_ff_list[of xs] unfolding gcd_ff_list_def by auto lemma divides_ff_refl[simp]: "divides_ff x x" unfolding divides_ff_def by (rule exI[of _ 1], auto simp: to_fract_def One_fract_def) lemma divides_ff_trans: "divides_ff x y ⟹ divides_ff y z ⟹ divides_ff x z" unfolding divides_ff_def by (auto simp del: to_fract_hom.hom_mult simp add: to_fract_hom.hom_mult[symmetric]) lemma divides_ff_mult_right: "a ≠ 0 ⟹ divides_ff (x * inverse a) y ⟹ divides_ff x (a * y)" unfolding divides_ff_def divide_inverse[symmetric] by auto definition eq_dff :: "'a :: ufd fract ⇒ 'a fract ⇒ bool" (infix "=dff" 50) where "x =dff y ⟷ divides_ff x y ∧ divides_ff y x" lemma eq_dffI[intro]: "divides_ff x y ⟹ divides_ff y x ⟹ x =dff y" unfolding eq_dff_def by auto lemma eq_dff_refl[simp]: "x =dff x" by (intro eq_dffI, auto) lemma eq_dff_sym: "x =dff y ⟹ y =dff x" unfolding eq_dff_def by auto lemma eq_dff_trans[trans]: "x =dff y ⟹ y =dff z ⟹ x =dff z" unfolding eq_dff_def using divides_ff_trans by auto lemma eq_dff_cancel_right[simp]: "x * y =dff x * z ⟷ x = 0 ∨ y =dff z" unfolding eq_dff_def by auto lemma eq_dff_mult_right_trans[trans]: "x =dff y * z ⟹ z =dff u ⟹ x =dff y * u" using eq_dff_trans by force lemma some_gcd_ff_list_smult: "a ≠ 0 ⟹ some_gcd_ff_list (map ((*) a) xs) =dff a * some_gcd_ff_list xs" proof let ?g = "some_gcd_ff_list (map ((*) a) xs)" show "divides_ff (a * some_gcd_ff_list xs) ?g" by (rule some_gcd_ff_list_greatest, insert some_gcd_ff_list_divides[of _ xs], auto simp: divides_ff_def) assume a: "a ≠ 0" show "divides_ff ?g (a * some_gcd_ff_list xs)" proof (rule divides_ff_mult_right[OF a some_gcd_ff_list_greatest], intro ballI) fix x assume x: "x ∈ set xs" have "divides_ff (?g * inverse a) x = divides_ff (inverse a * ?g) (inverse a * (a * x))" using a by (simp add: field_simps) also have "…" using a x by (auto intro: some_gcd_ff_list_divides) finally show "divides_ff (?g * inverse a) x" . qed qed definition content_ff :: "'a::ufd fract poly ⇒ 'a fract" where "content_ff p = some_gcd_ff_list (coeffs p)" lemma content_ff_iff: "divides_ff x (content_ff p) ⟷ (∀ c ∈ set (coeffs p). divides_ff x c)" (is "?l = ?r") proof assume ?l from divides_ff_trans[OF this, unfolded content_ff_def, OF some_gcd_ff_list_divides] show ?r .. next assume ?r thus ?l unfolding content_ff_def by (intro some_gcd_ff_list_greatest, auto) qed lemma content_ff_divides_ff: "x ∈ set (coeffs p) ⟹ divides_ff (content_ff p) x" unfolding content_ff_def by (rule some_gcd_ff_list_divides) lemma content_ff_0[simp]: "content_ff 0 = 0" using content_ff_iff[of 0 0] by (auto simp: divides_ff_def) lemma content_ff_0_iff[simp]: "(content_ff p = 0) = (p = 0)" proof (cases "p = 0") case False define a where "a ≡ last (coeffs p)" define xs where "xs ≡ coeffs p" from False have mem: "a ∈ set (coeffs p)" and a: "a ≠ 0" unfolding a_def last_coeffs_eq_coeff_degree[OF False] coeffs_def by auto from content_ff_divides_ff[OF mem] have "divides_ff (content_ff p) a" . with a have "content_ff p ≠ 0" unfolding divides_ff_def by auto with False show ?thesis by auto qed auto lemma content_ff_eq_dff_nonzero: "content_ff p =dff x ⟹ x ≠ 0 ⟹ p ≠ 0" using divides_ff_def eq_dff_def by force lemma content_ff_smult: "content_ff (smult (a::'a::ufd fract) p) =dff a * content_ff p" proof (cases "a = 0") case False note a = this have id: "coeffs (smult a p) = map ((*) a) (coeffs p)" unfolding coeffs_smult using a by (simp add: Polynomial.coeffs_smult) show ?thesis unfolding content_ff_def id using some_gcd_ff_list_smult[OF a] . qed simp definition normalize_content_ff where "normalize_content_ff (p::'a::ufd fract poly) ≡ smult (inverse (content_ff p)) p" lemma smult_normalize_content_ff: "smult (content_ff p) (normalize_content_ff p) = p" unfolding normalize_content_ff_def by (cases "p = 0", auto) lemma content_ff_normalize_content_ff_1: assumes p0: "p ≠ 0" shows "content_ff (normalize_content_ff p) =dff 1" proof - have "content_ff p = content_ff (smult (content_ff p) (normalize_content_ff p))" unfolding smult_normalize_content_ff .. also have "… =dff content_ff p * content_ff (normalize_content_ff p)" by (rule content_ff_smult) finally show ?thesis unfolding eq_dff_def divides_ff_def using p0 by auto qed lemma content_ff_to_fract: assumes "set (coeffs p) ⊆ range to_fract" shows "content_ff p ∈ range to_fract" proof - have "divides_ff 1 (content_ff p)" using assms unfolding content_ff_iff unfolding divides_ff_def[abs_def] by auto thus ?thesis unfolding divides_ff_def by auto qed lemma content_ff_map_poly_to_fract: "content_ff (map_poly to_fract (p :: 'a :: ufd poly)) ∈ range to_fract" by (rule content_ff_to_fract, subst coeffs_map_poly, auto) lemma range_coeffs_to_fract: assumes "set (coeffs p) ⊆ range to_fract" shows "∃ m. coeff p i = to_fract m" proof - from assms(1) to_fract_0 have "coeff p i ∈ range to_fract" using range_coeff [of p] by auto (metis contra_subsetD to_fract_hom.hom_zero insertE range_eqI) thus ?thesis by auto qed lemma divides_ff_coeff: assumes "set (coeffs p) ⊆ range to_fract" and "divides_ff (to_fract n) (coeff p i)" shows "∃ m. coeff p i = to_fract n * to_fract m" proof - from range_coeffs_to_fract[OF assms(1)] obtain k where pi: "coeff p i = to_fract k" by auto from assms(2)[unfolded this] have "n dvd k" by simp then obtain j where k: "k = n * j" unfolding Rings.dvd_def by auto show ?thesis unfolding pi k by auto qed definition inv_embed :: "'a :: ufd fract ⇒ 'a" where "inv_embed = the_inv to_fract" lemma inv_embed[simp]: "inv_embed (to_fract x) = x" unfolding inv_embed_def by (rule the_inv_f_f, auto simp: inj_on_def) lemma inv_embed_0[simp]: "inv_embed 0 = 0" unfolding to_fract_0[symmetric] inv_embed by simp lemma range_to_fract_embed_poly: assumes "set (coeffs p) ⊆ range to_fract" shows "p = map_poly to_fract (map_poly inv_embed p)" proof - have "p = map_poly (to_fract o inv_embed) p" by (rule sym, rule map_poly_idI, insert assms, auto) also have "… = map_poly to_fract (map_poly inv_embed p)" by (subst map_poly_map_poly, auto) finally show ?thesis . qed lemma content_ff_to_fract_coeffs_to_fract: assumes "content_ff p ∈ range to_fract" shows "set (coeffs p) ⊆ range to_fract" proof fix x assume "x ∈ set (coeffs p)" from content_ff_divides_ff[OF this] assms[unfolded eq_dff_def] show "x ∈ range to_fract" unfolding divides_ff_def by (auto simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) qed lemma content_ff_1_coeffs_to_fract: assumes "content_ff p =dff 1" shows "set (coeffs p) ⊆ range to_fract" proof fix x assume "x ∈ set (coeffs p)" from content_ff_divides_ff[OF this] assms[unfolded eq_dff_def] show "x ∈ range to_fract" unfolding divides_ff_def by (auto simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) qed lemma gauss_lemma: fixes p q :: "'a :: ufd fract poly" shows "content_ff (p * q) =dff content_ff p * content_ff q" proof (cases "p = 0 ∨ q = 0") case False hence p: "p ≠ 0" and q: "q ≠ 0" by auto let ?c = "content_ff :: 'a fract poly ⇒ 'a fract" { fix p q :: "'a fract poly" assume cp1: "?c p =dff 1" and cq1: "?c q =dff 1" define ip where "ip ≡ map_poly inv_embed p" define iq where "iq ≡ map_poly inv_embed q" interpret map_poly_hom: map_poly_comm_ring_hom to_fract.. from content_ff_1_coeffs_to_fract[OF cp1] have cp: "set (coeffs p) ⊆ range to_fract" . from content_ff_1_coeffs_to_fract[OF cq1] have cq: "set (coeffs q) ⊆ range to_fract" . have ip: "p = map_poly to_fract ip" unfolding ip_def by (rule range_to_fract_embed_poly[OF cp]) have iq: "q = map_poly to_fract iq" unfolding iq_def by (rule range_to_fract_embed_poly[OF cq]) have cpq0: "?c (p * q) ≠ 0" unfolding content_ff_0_iff using cp1 cq1 content_ff_eq_dff_nonzero[of _ 1] by auto have cpq: "set (coeffs (p * q)) ⊆ range to_fract" unfolding ip iq unfolding map_poly_hom.hom_mult[symmetric] to_fract_hom.coeffs_map_poly_hom by auto have ctnt: "?c (p * q) ∈ range to_fract" using content_ff_to_fract[OF cpq] . then obtain cpq where id: "?c (p * q) = to_fract cpq" by auto have dvd: "divides_ff 1 (?c (p * q))" using ctnt unfolding divides_ff_def by auto from cpq0[unfolded id] have cpq0: "cpq ≠ 0" unfolding to_fract_def Zero_fract_def by auto hence cpqM: "cpq ∈ carrier mk_monoid" by auto have "?c (p * q) =dff 1" proof (rule ccontr) assume "¬ ?c (p * q) =dff 1" with dvd have "¬ divides_ff (?c (p * q)) 1" unfolding eq_dff_def by auto from this[unfolded id divides_ff_def] have cpq: "⋀ r. cpq * r ≠ 1" by (auto simp: to_fract_def One_fract_def eq_fract) then have cpq1: "¬ cpq dvd 1" by (auto elim:dvdE simp:ac_simps) from mset_factors_exist[OF cpq0 cpq1] obtain F where F: "mset_factors F cpq" by auto have "F ≠ {#}" using F by auto then obtain f where f: "f ∈# F" by auto with F have irrf: "irreducible f" and f0: "f ≠ 0" by (auto dest: mset_factorsD) from irrf have pf: "prime_elem f" by simp note * = this[unfolded prime_elem_def] from * have no_unit: "¬ f dvd 1" by auto from * f0 have prime: "⋀ a b. f dvd a * b ⟹ f dvd a ∨ f dvd b" unfolding dvd_def by force let ?f = "to_fract f" from F f have fdvd: "f dvd cpq" by (auto intro:mset_factors_imp_dvd) hence "divides_ff ?f (to_fract cpq)" by simp from divides_ff_trans[OF this, folded id, OF content_ff_divides_ff] have dvd: "⋀ z. z ∈ set (coeffs (p * q)) ⟹ divides_ff ?f z" . { fix p :: "'a fract poly" assume cp: "?c p =dff 1" let ?P = "λ i. ¬ divides_ff ?f (coeff p i)" { assume "∀ c ∈ set (coeffs p). divides_ff ?f c" hence n: "divides_ff ?f (?c p)" unfolding content_ff_iff by auto from divides_ff_trans[OF this] cp[unfolded eq_dff_def] have "divides_ff ?f 1" by auto also have "1 = to_fract 1" by simp finally have "f dvd 1" by (unfold divides_ff_to_fract) hence False using no_unit unfolding dvd_def by (auto simp: ac_simps) } then obtain cp where cp: "cp ∈ set (coeffs p)" and ncp: "¬ divides_ff ?f cp" by auto hence "cp ∈ range (coeff p)" unfolding range_coeff by auto with ncp have "∃ i. ?P i" by auto from LeastI_ex[OF this] not_less_Least[of _ ?P] have "∃ i. ?P i ∧ (∀ j. j < i ⟶ divides_ff ?f (coeff p j))" by blast } note cont = this from cont[OF cp1] obtain r where r: "¬ divides_ff ?f (coeff p r)" and r': "⋀ i. i < r ⟹ divides_ff ?f (coeff p i)" by auto have "∀ i. ∃ k. i < r ⟶ coeff p i = ?f * to_fract k" using divides_ff_coeff[OF cp r'] by blast from choice[OF this] obtain rr where r': "⋀ i. i < r ⟹ coeff p i = ?f * to_fract (rr i)" by blast let ?r = "coeff p r" from cont[OF cq1] obtain s where s: "¬ divides_ff ?f (coeff q s)" and s': "⋀ i. i < s ⟹ divides_ff ?f (coeff q i)" by auto have "∀ i. ∃ k. i < s ⟶ coeff q i = ?f * to_fract k" using divides_ff_coeff[OF cq s'] by blast from choice[OF this] obtain ss where s': "⋀ i. i < s ⟹ coeff q i = ?f * to_fract (ss i)" by blast from range_coeffs_to_fract[OF cp] have "∀ i. ∃ m. coeff p i = to_fract m" .. from choice[OF this] obtain pi where pi: "⋀ i. coeff p i = to_fract (pi i)" by blast from range_coeffs_to_fract[OF cq] have "∀ i. ∃ m. coeff q i = to_fract m" .. from choice[OF this] obtain qi where qi: "⋀ i. coeff q i = to_fract (qi i)" by blast let ?s = "coeff q s" let ?g = "λ i. coeff p i * coeff q (r + s - i)" define a where "a = (∑i∈{..<r}. (rr i * qi (r + s - i)))" define b where "b = (∑ i ∈ {Suc r..r + s}. pi i * (ss (r + s - i)))" have "coeff (p * q) (r + s) = (∑i≤r + s. ?g i)" unfolding coeff_mult .. also have "{..r+s} = {..< r} ∪ {r .. r+s}" by auto also have "(∑i∈{..<r} ∪ {r..r + s}. ?g i) = (∑i∈{..<r}. ?g i) + (∑ i ∈ {r..r + s}. ?g i)" by (rule sum.union_disjoint, auto) also have "(∑i∈{..<r}. ?g i) = (∑i∈{..<r}. ?f * (to_fract (rr i) * to_fract (qi (r + s - i))))" by (rule sum.cong[OF refl], insert r' qi, auto) also have "… = to_fract (f * a)" by (simp add: a_def sum_distrib_left) also have "(∑ i ∈ {r..r + s}. ?g i) = ?g r + (∑ i ∈ {Suc r..r + s}. ?g i)" by (subst sum.remove[of _ r], auto intro: sum.cong) also have "(∑ i ∈ {Suc r..r + s}. ?g i) = (∑ i ∈ {Suc r..r + s}. ?f * (to_fract (pi i) * to_fract (ss (r + s - i))))" by (rule sum.cong[OF refl], insert s' pi, auto) also have "… = to_fract (f * b)" by (simp add: sum_distrib_left b_def) finally have cpq: "coeff (p * q) (r + s) = to_fract (f * (a + b)) + ?r * ?s" by (simp add: field_simps) { fix i from dvd[of "coeff (p * q) i"] have "divides_ff ?f (coeff (p * q) i)" using range_coeff[of "p * q"] by (cases "coeff (p * q) i = 0", auto simp: divides_ff_def) } from this[of "r + s", unfolded cpq] have "divides_ff ?f (to_fract (f * (a + b) + pi r * qi s))" unfolding pi qi by simp from this[unfolded divides_ff_to_fract] have "f dvd pi r * qi s" by (metis dvd_add_times_triv_left_iff mult.commute) from prime[OF this] have "f dvd pi r ∨ f dvd qi s" by auto with r s show False unfolding pi qi by auto qed } note main = this define n where "n ≡ normalize_content_ff :: 'a fract poly ⇒ 'a fract poly" let ?s = "λ p. smult (content_ff p) (n p)" have "?c (p * q) = ?c (?s p * ?s q)" unfolding smult_normalize_content_ff n_def by simp also have "?s p * ?s q = smult (?c p * ?c q) (n p * n q)" by (simp add: mult.commute) also have "?c (…) =dff (?c p * ?c q) * ?c (n p * n q)" by (rule content_ff_smult) also have "?c (n p * n q) =dff 1" unfolding n_def by (rule main, insert p q, auto simp: content_ff_normalize_content_ff_1) finally show ?thesis by simp qed auto abbreviation (input) "content_ff_ff p ≡ content_ff (map_poly to_fract p)" lemma factorization_to_fract: assumes q: "q ≠ 0" and factor: "map_poly to_fract (p :: 'a :: ufd poly) = q * r" shows "∃ q' r' c. c ≠ 0 ∧ q = smult c (map_poly to_fract q') ∧ r = smult (inverse c) (map_poly to_fract r') ∧ content_ff_ff q' =dff 1 ∧ p = q' * r'" proof - let ?c = content_ff let ?p = "map_poly to_fract p" interpret map_poly_inj_comm_ring_hom "to_fract :: 'a ⇒ _".. define cq where "cq ≡ normalize_content_ff q" define cr where "cr ≡ smult (content_ff q) r" define q' where "q' ≡ map_poly inv_embed cq" define r' where "r' ≡ map_poly inv_embed cr" from content_ff_map_poly_to_fract have cp_ff: "?c ?p ∈ range to_fract" by auto from smult_normalize_content_ff[of q] have cqs: "q = smult (content_ff q) cq" unfolding cq_def .. from content_ff_normalize_content_ff_1[OF q] have c_cq: "content_ff cq =dff 1" unfolding cq_def . from content_ff_1_coeffs_to_fract[OF this] have cq_ff: "set (coeffs cq) ⊆ range to_fract" . have factor: "?p = cq * cr" unfolding factor cr_def using cqs by (metis mult_smult_left mult_smult_right) from gauss_lemma[of cq cr] have cp: "?c ?p =dff ?c cq * ?c cr" unfolding factor . with c_cq have "?c ?p =dff ?c cr" by (metis eq_dff_mult_right_trans mult.commute mult.right_neutral) with cp_ff have "?c cr ∈ range to_fract" by (metis divides_ff_def to_fract_hom.hom_mult eq_dff_def image_iff range_eqI) from content_ff_to_fract_coeffs_to_fract[OF this] have cr_ff: "set (coeffs cr) ⊆ range to_fract" by auto have cq: "cq = map_poly to_fract q'" unfolding q'_def by (rule range_to_fract_embed_poly[OF cq_ff]) have cr: "cr = map_poly to_fract r'" unfolding r'_def by (rule range_to_fract_embed_poly[OF cr_ff]) from factor[unfolded cq cr] have p: "p = q' * r'" by (simp add: injectivity) from c_cq have ctnt: "content_ff_ff q' =dff 1" using cq q'_def by force from cqs have idq: "q = smult (?c q) (map_poly to_fract q')" unfolding cq . with q have cq: "?c q ≠ 0" by auto have "r = smult (inverse (?c q)) cr" unfolding cr_def using cq by auto also have "cr = map_poly to_fract r'" by (rule cr) finally have idr: "r = smult (inverse (?c q)) (map_poly to_fract r')" by auto from cq p ctnt idq idr show ?thesis by blast qed lemma irreducible_PM_M_PFM: assumes irr: "irreducible p" shows "degree p = 0 ∧ irreducible (coeff p 0) ∨ degree p ≠ 0 ∧ irreducible (map_poly to_fract p) ∧ content_ff_ff p =dff 1" proof- interpret map_poly_inj_idom_hom to_fract.. from irr[unfolded irreducible_altdef] have p0: "p ≠ 0" and irr: "¬ p dvd 1" "⋀ b. b dvd p ⟹ ¬ p dvd b ⟹ b dvd 1" by auto show ?thesis proof (cases "degree p = 0") case True from degree0_coeffs[OF True] obtain a where p: "p = [:a:]" by auto note irr = irr[unfolded p] from p p0 have a0: "a ≠ 0" by auto moreover have "¬ a dvd 1" using irr(1) by simp moreover { fix b assume "b dvd a" "¬ a dvd b" hence "[:b:] dvd [:a:]" "¬ [:a:] dvd [:b:]" unfolding const_poly_dvd . from irr(2)[OF this] have "b dvd 1" unfolding const_poly_dvd_1 . } ultimately have "irreducible a" unfolding irreducible_altdef by auto with True show ?thesis unfolding p by auto next case False let ?E = "map_poly to_fract" let ?p = "?E p" have dp: "degree ?p ≠ 0" using False by simp from p0 have p': "?p ≠ 0" by simp moreover have "¬ ?p dvd 1" proof assume "?p dvd 1" then obtain q where id: "?p * q = 1" unfolding dvd_def by auto have deg: "degree (?p * q) = degree ?p + degree q" by (rule degree_mult_eq, insert id, auto) from arg_cong[OF id, of degree, unfolded deg] dp show False by auto qed moreover { fix q assume "q dvd ?p" and ndvd: "¬ ?p dvd q" then obtain r where fact: "?p = q * r" unfolding dvd_def by auto with p' have q0: "q ≠ 0" by auto from factorization_to_fract[OF this fact] obtain q' r' c where *: "c ≠ 0" "q = smult c (?E q')" "r = smult (inverse c) (?E r')" "content_ff_ff q' =dff 1" "p = q' * r'" by auto hence "q' dvd p" unfolding dvd_def by auto note irr = irr(2)[OF this] have "¬ p dvd q'" proof assume "p dvd q'" then obtain u where q': "q' = p * u" unfolding dvd_def by auto from arg_cong[OF this, of "λ x. smult c (?E x)", unfolded *(2)[symmetric]] have "q = ?p * smult c (?E u)" by simp hence "?p dvd q" unfolding dvd_def by blast with ndvd show False .. qed from irr[OF this] have "q' dvd 1" . from divides_degree[OF this] have "degree q' = 0" by auto from degree0_coeffs[OF this] obtain a' where "q' = [:a':]" by auto from *(2)[unfolded this] obtain a where q: "q = [:a:]" by (simp add: to_fract_hom.map_poly_pCons_hom) with q0 have a: "a ≠ 0" by auto have "q dvd 1" unfolding q const_poly_dvd_1 using a unfolding dvd_def by (intro exI[of _ "inverse a"], auto) } ultimately have irr_p': "irreducible ?p" unfolding irreducible_altdef by auto let ?c = "content_ff" have "?c ?p ∈ range to_fract" by (rule content_ff_to_fract, unfold to_fract_hom.coeffs_map_poly_hom, auto) then obtain c where cp: "?c ?p = to_fract c" by auto from p' cp have c: "c ≠ 0" by auto have "?c ?p =dff 1" unfolding cp proof (rule ccontr) define cp where "cp = normalize_content_ff ?p" from smult_normalize_content_ff[of ?p] have cps: "?p = smult (to_fract c) cp" unfolding cp_def cp .. from content_ff_normalize_content_ff_1[OF p'] have c_cp: "content_ff cp =dff 1" unfolding cp_def . from range_to_fract_embed_poly[OF content_ff_1_coeffs_to_fract[OF c_cp]] obtain cp' where "cp = ?E cp'" by auto from cps[unfolded this] have "p = smult c cp'" by (simp add: injectivity) hence dvd: "[: c :] dvd p" unfolding dvd_def by auto have "¬ p dvd [: c :]" using divides_degree[of p "[: c :]"] c False by auto from irr(2)[OF dvd this] have "c dvd 1" by simp assume "¬ to_fract c =dff 1" from this[unfolded eq_dff_def One_fract_def to_fract_def[symmetric] divides_ff_def to_fract_mult] have c1: "⋀ r. 1 ≠ c * r" by (auto simp: ac_simps simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) with ‹c dvd 1› show False unfolding dvd_def by blast qed with False irr_p' show ?thesis by auto qed qed lemma irreducible_M_PM: fixes p :: "'a :: ufd poly" assumes 0: "degree p = 0" and irr: "irreducible (coeff p 0)" shows "irreducible p" proof (cases "p = 0") case True thus ?thesis using assms by auto next case False from degree0_coeffs[OF 0] obtain a where p: "p = [:a:]" by auto with False have a0: "a ≠ 0" by auto from p irr have "irreducible a" by auto from this[unfolded irreducible_altdef] have a1: "¬ a dvd 1" and irr: "⋀ b. b dvd a ⟹ ¬ a dvd b ⟹ b dvd 1" by auto { fix b assume *: "b dvd [:a:]" "¬ [:a:] dvd b" from divides_degree[OF this(1)] a0 have "degree b = 0" by auto from degree0_coeffs[OF this] obtain bb where b: "b = [: bb :]" by auto from * irr[of bb] have "b dvd 1" unfolding b const_poly_dvd by auto } with a0 a1 show ?thesis by (auto simp: irreducible_altdef p) qed lemma primitive_irreducible_imp_degree: "primitive (p::'a::{semiring_gcd,idom} poly) ⟹ irreducible p ⟹ degree p > 0" by (unfold irreducible_primitive_connect[symmetric], auto) lemma irreducible_degree_field: fixes p :: "'a :: field poly" assumes "irreducible p" shows "degree p > 0" proof- { assume "degree p = 0" from degree0_coeffs[OF this] assms obtain a where p: "p = [:a:]" and a: "a ≠ 0" by auto hence "1 = p * [:inverse a:]" by auto hence "p dvd 1" .. hence "p ∈ Units mk_monoid" by simp with assms have False unfolding irreducible_def by auto } then show ?thesis by auto qed lemma irreducible_PFM_PM: assumes irr: "irreducible (map_poly to_fract p)" and ct: "content_ff_ff p =dff 1" shows "irreducible p" proof - let ?E = "map_poly to_fract" let ?p = "?E p" from ct have p0: "p ≠ 0" by (auto simp: eq_dff_def divides_ff_def) moreover from irreducible_degree_field[OF irr] have deg: "degree p ≠ 0" by simp from irr[unfolded irreducible_altdef] have irr: "⋀ b. b dvd ?p ⟹ ¬ ?p dvd b ⟹ b dvd 1" by auto have "¬ p dvd 1" using deg divides_degree[of p 1] by auto moreover { fix q :: "'a poly" assume dvd: "q dvd p" and ndvd: "¬ p dvd q" from dvd obtain r where pqr: "p = q * r" .. from arg_cong[OF this, of ?E] have pqr': "?p = ?E q * ?E r" by simp from p0 pqr have q: "q ≠ 0" and r: "r ≠ 0" by auto have dp: "degree p = degree q + degree r" unfolding pqr by (subst degree_mult_eq, insert q r, auto) from eq_dff_trans[OF eq_dff_sym[OF gauss_lemma[of "?E q" "?E r", folded pqr']] ct] have ct: "content_ff (?E q) * content_ff (?E r) =dff 1" . from content_ff_map_poly_to_fract obtain cq where cq: "content_ff (?E q) = to_fract cq" by auto from content_ff_map_poly_to_fract obtain cr where cr: "content_ff (?E r) = to_fract cr" by auto note ct[unfolded cq cr to_fract_mult eq_dff_def divides_ff_def] from this[folded hom_distribs] obtain c where c: "cq * cr * c = 1" by (auto simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) hence one: "1 = cq * (c * cr)" "1 = cr * (c * cq)" by (auto simp: ac_simps) { assume *: "degree q ≠ 0 ∧ degree r ≠ 0" with dp have "degree q < degree p" by auto hence "degree (?E q) < degree (?E p)" by simp hence ndvd: "¬ ?p dvd ?E q" using divides_degree[of ?p "?E q"] q by auto have "?E q dvd ?p" unfolding pqr' by auto from irr[OF this ndvd] have "?E q dvd 1" . from divides_degree[OF this] * have False by auto } hence "degree q = 0 ∨ degree r = 0" by blast then have "q dvd 1" proof assume "degree q = 0" from degree0_coeffs[OF this] q obtain a where q: "q = [:a:]" and a: "a ≠ 0" by auto hence id: "set (coeffs (?E q)) = {to_fract a}" by auto have "divides_ff (to_fract a) (content_ff (?E q))" unfolding content_ff_iff id by auto from this[unfolded cq divides_ff_def, folded hom_distribs] obtain rr where cq: "cq = a * rr" by (auto simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) with one(1) have "1 = a * (rr * c * cr)" by (auto simp: ac_simps) hence "a dvd 1" .. thus ?thesis by (simp add: q) next assume "degree r = 0" from degree0_coeffs[OF this] r obtain a where r: "r = [:a:]" and a: "a ≠ 0" by auto hence id: "set (coeffs (?E r)) = {to_fract a}" by auto have "divides_ff (to_fract a) (content_ff (?E r))" unfolding content_ff_iff id by auto note this[unfolded cr divides_ff_def to_fract_mult] note this[folded hom_distribs] then obtain rr where cr: "cr = a * rr" by (auto simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) with one(2) have one: "1 = a * (rr * c * cq)" by (auto simp: ac_simps) from arg_cong[OF pqr[unfolded r], of "λ p. p * [:rr * c * cq:]"] have "p * [:rr * c * cq:] = q * [:a * (rr * c * cq):]" by (simp add: ac_simps) also have "… = q" unfolding one[symmetric] by auto finally obtain r where "q = p * r" by blast hence "p dvd q" .. with ndvd show ?thesis by auto qed } ultimately show ?thesis by (auto simp:irreducible_altdef) qed lemma irreducible_cases: "irreducible p ⟷ degree p = 0 ∧ irreducible (coeff p 0) ∨ degree p ≠ 0 ∧ irreducible (map_poly to_fract p) ∧ content_ff_ff p =dff 1" using irreducible_PM_M_PFM irreducible_M_PM irreducible_PFM_PM by blast lemma dvd_PM_iff: "p dvd q ⟷ divides_ff (content_ff_ff p) (content_ff_ff q) ∧ map_poly to_fract p dvd map_poly to_fract q" proof - interpret map_poly_inj_idom_hom to_fract.. let ?E = "map_poly to_fract" show ?thesis (is "?l = ?r") proof assume "p dvd q" then obtain r where qpr: "q = p * r" .. from arg_cong[OF this, of ?E] have dvd: "?E p dvd ?E q" by auto from content_ff_map_poly_to_fract obtain cq where cq: "content_ff_ff q = to_fract cq" by auto from content_ff_map_poly_to_fract obtain cp where cp: "content_ff_ff p = to_fract cp" by auto from content_ff_map_poly_to_fract obtain cr where cr: "content_ff_ff r = to_fract cr" by auto from gauss_lemma[of "?E p" "?E r", folded hom_distribs qpr, unfolded cq cp cr] have "divides_ff (content_ff_ff p) (content_ff_ff q)" unfolding cq cp eq_dff_def by (metis divides_ff_def divides_ff_trans) with dvd show ?r by blast next assume ?r show ?l proof (cases "q = 0") case True with ‹?r› show ?l by auto next case False note q = this hence q': "?E q ≠ 0" by auto from ‹?r› obtain rr where qpr: "?E q = ?E p * rr" unfolding dvd_def by auto with q have p: "p ≠ 0" and Ep: "?E p ≠ 0" and rr: "rr ≠ 0" by auto from gauss_lemma[of "?E p" rr, folded qpr] have ct: "content_ff_ff q =dff content_ff_ff p * content_ff rr" by auto from content_ff_map_poly_to_fract[of p] obtain cp where cp: "content_ff_ff p = to_fract cp" by auto from content_ff_map_poly_to_fract[of q] obtain cq where cq: "content_ff_ff q = to_fract cq" by auto from ‹?r›[unfolded cp cq] have "divides_ff (to_fract cp) (to_fract cq)" .. with ct[unfolded cp cq eq_dff_def] have "content_ff rr ∈ range to_fract" by (metis (no_types, lifting) Ep content_ff_0_iff cp divides_ff_def divides_ff_trans mult.commute mult_right_cancel range_eqI) from range_to_fract_embed_poly[OF content_ff_to_fract_coeffs_to_fract[OF this]] obtain r where rr: "rr = ?E r" by auto from qpr[unfolded rr, folded hom_distribs] have "q = p * r" by (rule injectivity) thus "p dvd q" .. qed qed qed lemma factorial_monoid_poly: "factorial_monoid (mk_monoid :: 'a :: ufd poly monoid)" proof (fold factorial_condition_one, intro conjI) interpret M: factorial_monoid "mk_monoid :: 'a monoid" by (fact factorial_monoid) interpret PFM: factorial_monoid "mk_monoid :: 'a fract poly monoid" by (rule as_ufd.factorial_monoid) interpret PM: comm_monoid_cancel "mk_monoid :: 'a poly monoid" by (unfold_locales, auto) let ?E = "map_poly to_fract" show "divisor_chain_condition_monoid (mk_monoid::'a poly monoid)" proof (unfold_locales, unfold mk_monoid_simps) let ?rel' = "{(x::'a poly, y). x ≠ 0 ∧ y ≠ 0 ∧ properfactor x y}" let ?rel'' = "{(x::'a, y). x ≠ 0 ∧ y ≠ 0 ∧ properfactor x y}" let ?relPM = "{(x, y). x ≠ 0 ∧ y ≠ 0 ∧ x dvd y ∧ ¬ y dvd (x :: 'a poly)}" let ?relM = "{(x, y). x ≠ 0 ∧ y ≠ 0 ∧ x dvd y ∧ ¬ y dvd (x :: 'a)}" have id: "?rel' = ?relPM" using properfactor_nz by auto have id': "?rel'' = ?relM" using properfactor_nz by auto have "wf ?rel''" using M.division_wellfounded by auto hence wfM: "wf ?relM" using id' by auto let ?c = "λ p. inv_embed (content_ff_ff p)" let ?f = "λ p. (degree p, ?c p)" note wf = wf_inv_image[OF wf_lex_prod[OF wf_less wfM], of ?f] show "wf ?rel'" unfolding id proof (rule wf_subset[OF wf], clarify) fix p q :: "'a poly" assume p: "p ≠ 0" and q: "q ≠ 0" and dvd: "p dvd q" and ndvd: "¬ q dvd p" from dvd obtain r where qpr: "q = p * r" .. from degree_mult_eq[of p r, folded qpr] q qpr have r: "r ≠ 0" and deg: "degree q = degree p + degree r" by auto show "(p,q) ∈ inv_image ({(x, y). x < y} <*lex*> ?relM) ?f" proof (cases "degree p = degree q") case False with deg have "degree p < degree q" by auto thus ?thesis by auto next case True with deg have "degree r = 0" by simp from degree0_coeffs[OF this] r obtain a where ra: "r = [:a:]" and a: "a ≠ 0" by auto from arg_cong[OF qpr, of "λ p. ?E p * [:inverse (to_fract a):]"] a have "?E p = ?E q * [:inverse (to_fract a):]" by (auto simp: ac_simps ra) hence "?E q dvd ?E p" .. with ndvd dvd_PM_iff have ndvd: "¬ divides_ff (content_ff_ff q) (content_ff_ff p)" by auto from content_ff_map_poly_to_fract obtain cq where cq: "content_ff_ff q = to_fract cq" by auto from content_ff_map_poly_to_fract obtain cp where cp: "content_ff_ff p = to_fract cp" by auto from ndvd[unfolded cp cq] have ndvd: "¬ cq dvd cp" by simp from iffD1[OF dvd_PM_iff,OF dvd,unfolded cq cp] have dvd: "cp dvd cq" by simp have c_p: "?c p = cp" unfolding cp by simp have c_q: "?c q = cq" unfolding cq by simp from q cq have cq0: "cq ≠ 0" by auto from p cp have cp0: "cp ≠ 0" by auto from ndvd cq0 cp0 dvd have "(?c p, ?c q) ∈ ?relM" unfolding c_p c_q by auto with True show ?thesis by auto qed qed qed show "primeness_condition_monoid (mk_monoid::'a poly monoid)" proof (unfold_locales, unfold mk_monoid_simps) fix p :: "'a poly" assume p: "p ≠ 0" and "irred p" then have irr: "irreducible p" by auto from p have p': "?E p ≠ 0" by auto from irreducible_PM_M_PFM[OF irr] have choice: "degree p = 0 ∧ irred (coeff p 0) ∨ degree p ≠ 0 ∧ irred (?E p) ∧ content_ff_ff p =dff 1" by auto show "Divisibility.prime mk_monoid p" proof (rule Divisibility.primeI, unfold mk_monoid_simps mem_Units) show "¬ p dvd 1" proof assume "p dvd 1" from divides_degree[OF this] have dp: "degree p = 0" by auto from degree0_coeffs[OF this] p obtain a where p: "p = [:a:]" and a: "a ≠ 0" by auto with choice have irr: "irreducible a" by auto from ‹p dvd 1›[unfolded p] have "a dvd 1" by auto with irr show False unfolding irreducible_def by auto qed fix q r :: "'a poly" assume q: "q ≠ 0" and r: "r ≠ 0" and "factor p (q * r)" from this[unfolded factor_idom] have "p dvd q * r" by auto from iffD1[OF dvd_PM_iff this] have dvd_ct: "divides_ff (content_ff_ff p) (content_ff (?E (q * r)))" and dvd_E: "?E p dvd ?E q * ?E r" by auto from gauss_lemma[of "?E q" "?E r"] divides_ff_trans[OF dvd_ct, of "content_ff_ff q * content_ff_ff r"] have dvd_ct: "divides_ff (content_ff_ff p) (content_ff_ff q * content_ff_ff r)" unfolding eq_dff_def by auto from choice have "p dvd q ∨ p dvd r" proof assume "degree p ≠ 0 ∧ irred (?E p) ∧ content_ff_ff p =dff 1" hence deg: "degree p ≠ 0" and irr: "irred (?E p)" and ct: "content_ff_ff p =dff 1" by auto from PFM.irreducible_prime[OF irr] p have prime: "Divisibility.prime mk_monoid (?E p)" by auto from q r have Eq: "?E q ∈ carrier mk_monoid" and Er: "?E r ∈ carrier mk_monoid" and q': "?E q ≠ 0" and r': "?E r ≠ 0" and qr': "?E q * ?E r ≠ 0" by auto from PFM.prime_divides[OF Eq Er prime] q' r' qr' dvd_E have dvd_E: "?E p dvd ?E q ∨ ?E p dvd ?E r" by simp from ct have ct: "divides_ff (content_ff_ff p) 1" unfolding eq_dff_def by auto moreover have "⋀ q. divides_ff 1 (content_ff_ff q)" using content_ff_map_poly_to_fract unfolding divides_ff_def by auto from divides_ff_trans[OF ct this] have ct: "⋀ q. divides_ff (content_ff_ff p) (content_ff_ff q)" . with dvd_E show ?thesis using dvd_PM_iff by blast next assume "degree p = 0 ∧ irred (coeff p 0)" hence deg: "degree p = 0" and irr: "irred (coeff p 0)" by auto from degree0_coeffs[OF deg] p obtain a where p: "p = [:a:]" and a: "a ≠ 0" by auto with irr have irr: "irred a" and aM: "a ∈ carrier mk_monoid" by auto from M.irreducible_prime[OF irr aM] have prime: "Divisibility.prime mk_monoid a" . from content_ff_map_poly_to_fract obtain cq where cq: "content_ff_ff q = to_fract cq" by auto from content_ff_map_poly_to_fract obtain cp where cp: "content_ff_ff p = to_fract cp" by auto from content_ff_map_poly_to_fract obtain cr where cr: "content_ff_ff r = to_fract cr" by auto have "divides_ff (to_fract a) (content_ff_ff p)" unfolding p content_ff_iff using a by auto from divides_ff_trans[OF this[unfolded cp] dvd_ct[unfolded cp cq cr]] have "divides_ff (to_fract a) (to_fract (cq * cr))" by simp hence dvd: "a dvd cq * cr" by (auto simp add: divides_ff_def simp del: to_fract_hom.hom_mult simp: to_fract_hom.hom_mult[symmetric]) from content_ff_divides_ff[of "to_fract a" "?E p"] have "divides_ff (to_fract cp) (to_fract a)" using cp a p by auto hence cpa: "cp dvd a" by simp from a q r cq cr have aM: "a ∈ carrier mk_monoid" and qM: "cq ∈ carrier mk_monoid" and rM: "cr ∈ carrier mk_monoid" and q': "cq ≠ 0" and r': "cr ≠ 0" and qr': "cq * cr ≠ 0" by auto from M.prime_divides[OF qM rM prime] q' r' qr' dvd have "a dvd cq ∨ a dvd cr" by simp with dvd_trans[OF cpa] have dvd: "cp dvd cq ∨ cp dvd cr" by auto have "⋀ q. ?E p * (smult (inverse (to_fract a)) q) = q" unfolding p using a by (auto simp: one_poly_def) hence Edvd: "⋀ q. ?E p dvd q" unfolding dvd_def by metis from dvd Edvd show ?thesis apply (subst(1 2) dvd_PM_iff) unfolding cp cq cr by auto qed thus "factor p q ∨ factor p r" unfolding factor_idom using p q r by auto qed qed qed instance poly :: (ufd) ufd by (intro ufd.intro_of_class factorial_monoid_imp_ufd factorial_monoid_poly) lemma primitive_iff_some_content_dvd_1: fixes f :: "'a :: ufd poly" (* gcd_condition suffices... *) shows "primitive f ⟷ some_gcd.listgcd (coeffs f) dvd 1" (is "_ ⟷ ?c dvd 1") proof(intro iffI primitiveI) fix x assume "(⋀y. y ∈ set (coeffs f) ⟹ x dvd y)" from some_gcd.listgcd_greatest[of "coeffs f", OF this] have "x dvd ?c" by simp also assume "?c dvd 1" finally show "x dvd 1". next assume "primitive f" from primitiveD[OF this some_gcd.listgcd[of _ "coeffs f"]] show "?c dvd 1" by auto qed end