(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Square Free Factorization› text ‹We implemented Yun's algorithm to perform a square-free factorization of a polynomial. We further show properties of a square-free factorization, namely that the exponents in the square-free factorization are exactly the orders of the roots. We also show that factorizing the result of square-free factorization further will again result in a square-free factorization, and that square-free factorizations can be lifted homomorphically.› theory Square_Free_Factorization imports Matrix.Utility Polynomial_Irreducibility Order_Polynomial Fundamental_Theorem_Algebra_Factorized Polynomial_Interpolation.Ring_Hom_Poly begin definition square_free :: "'a :: comm_semiring_1 poly ⇒ bool" where "square_free p = (p ≠ 0 ∧ (∀ q. degree q > 0 ⟶ ¬ (q * q dvd p)))" lemma square_freeI: assumes "⋀ q. degree q > 0 ⟹ q ≠ 0 ⟹ q * q dvd p ⟹ False" and p: "p ≠ 0" shows "square_free p" unfolding square_free_def proof (intro allI conjI[OF p] impI notI, goal_cases) case (1 q) from assms(1)[OF 1(1) _ 1(2)] 1(1) show False by (cases "q = 0", auto) qed lemma square_free_multD: assumes sf: "square_free (f * g)" shows "h dvd f ⟹ h dvd g ⟹ degree h = 0" "square_free f" "square_free g" proof - from sf[unfolded square_free_def] have 0: "f ≠ 0" "g ≠ 0" and dvd: "⋀ q. q * q dvd f * g ⟹ degree q = 0" by auto then show "square_free f" "square_free g" by (auto simp: square_free_def) assume "h dvd f" "h dvd g" then have "h * h dvd f * g" by (rule mult_dvd_mono) from dvd[OF this] show "degree h = 0". qed lemma irreducible⇩_{d}_square_free: fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly" shows "irreducible⇩_{d}p ⟹ square_free p" by (metis degree_0 degree_mult_eq degree_mult_eq_0 irreducible⇩_{d}D(1) irreducible⇩_{d}D(2) irreducible⇩_{d}_dvd_smult irreducible⇩_{d}_smultI less_add_same_cancel2 not_gr_zero square_free_def) lemma square_free_factor: assumes dvd: "a dvd p" and sf: "square_free p" shows "square_free a" proof (intro square_freeI) fix q assume q: "degree q > 0" and "q * q dvd a" hence "q * q dvd p" using dvd dvd_trans sf square_free_def by blast with sf[unfolded square_free_def] q show False by auto qed (insert dvd sf, auto simp: square_free_def) lemma square_free_prod_list_distinct: assumes sf: "square_free (prod_list us :: 'a :: idom poly)" and us: "⋀ u. u ∈ set us ⟹ degree u > 0" shows "distinct us" proof (rule ccontr) assume "¬ distinct us" from not_distinct_decomp[OF this] obtain xs ys zs u where "us = xs @ u # ys @ u # zs" by auto hence dvd: "u * u dvd prod_list us" and u: "u ∈ set us" by auto from dvd us[OF u] sf have "prod_list us = 0" unfolding square_free_def by auto hence "0 ∈ set us" by (simp add: prod_list_zero_iff) from us[OF this] show False by auto qed definition separable where "separable f = coprime f (pderiv f)" lemma separable_imp_square_free: assumes sep: "separable (f :: 'a::{field, factorial_ring_gcd, semiring_gcd_mult_normalize} poly)" shows "square_free f" proof (rule ccontr) note sep = sep[unfolded separable_def] from sep have f0: "f ≠ 0" by (cases f, auto) assume "¬ square_free f" then obtain g where g: "degree g ≠ 0" and "g * g dvd f" using f0 unfolding square_free_def by auto then obtain h where f: "f = g * (g * h)" unfolding dvd_def by (auto simp: ac_simps) have "pderiv f = g * ((g * pderiv h + h * pderiv g) + h * pderiv g)" unfolding f pderiv_mult[of g] by (simp add: field_simps) hence "g dvd pderiv f" unfolding dvd_def by blast moreover have "g dvd f" unfolding f dvd_def by blast ultimately have dvd: "g dvd (gcd f (pderiv f))" by simp have "gcd f (pderiv f) ≠ 0" using f0 by simp with g dvd have "degree (gcd f (pderiv f)) ≠ 0" by (simp add: sep poly_dvd_1) hence "¬ coprime f (pderiv f)" by auto with sep show False by simp qed lemma square_free_rsquarefree: assumes f: "square_free f" shows "rsquarefree f" unfolding rsquarefree_def proof (intro conjI allI) fix x show "order x f = 0 ∨ order x f = 1" proof (rule ccontr) assume "¬ ?thesis" then obtain n where ord: "order x f = Suc (Suc n)" by (cases "order x f"; cases "order x f - 1"; auto) define p where "p = [:-x,1:]" from order_divides[of x "Suc (Suc 0)" f, unfolded ord] have "p * p dvd f" "degree p ≠ 0" unfolding p_def by auto hence "¬ square_free f" using f(1) unfolding square_free_def by auto with assms show False by auto qed qed (insert f, auto simp: square_free_def) lemma square_free_prodD: fixes fs :: "'a :: {field,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly set" assumes sf: "square_free (∏ fs)" and fin: "finite fs" and f: "f ∈ fs" and g: "g ∈ fs" and fg: "f ≠ g" shows "coprime f g" proof - have "(∏ fs) = f * (∏ (fs - {f}))" by (rule prod.remove[OF fin f]) also have "(∏ (fs - {f})) = g * (∏ (fs - {f} - {g}))" by (rule prod.remove, insert fin g fg, auto) finally obtain k where sf: "square_free (f * g * k)" using sf by (simp add: ac_simps) from sf[unfolded square_free_def] have 0: "f ≠ 0" "g ≠ 0" and dvd: "⋀ q. q * q dvd f * g * k ⟹ degree q = 0" by auto have "gcd f g * gcd f g dvd f * g * k" by (simp add: mult_dvd_mono) from dvd[OF this] have "degree (gcd f g) = 0" . moreover have "gcd f g ≠ 0" using 0 by auto ultimately show "coprime f g" using is_unit_gcd[of f g] is_unit_iff_degree[of "gcd f g"] by simp qed lemma rsquarefree_square_free_complex: assumes "rsquarefree (p :: complex poly)" shows "square_free p" proof (rule square_freeI) fix q assume d: "degree q > 0" and dvd: "q * q dvd p" from d have "¬ constant (poly q)" by (simp add: constant_degree) from fundamental_theorem_of_algebra[OF this] obtain x where "poly q x = 0" by auto hence "[:-x,1:] dvd q" by (simp add: poly_eq_0_iff_dvd) then obtain k where q: "q = [:-x,1:] * k" unfolding dvd_def by auto from dvd obtain l where p: "p = q * q * l" unfolding dvd_def by auto from p[unfolded q] have "p = [:-x,1:]^2 * (k * k * l)" by algebra hence "[:-x,1:]^2 dvd p" unfolding dvd_def by blast from this[unfolded order_divides] have "p = 0 ∨ ¬ order x p ≤ 1" by auto thus False using assms unfolding rsquarefree_def' by auto qed (insert assms, auto simp: rsquarefree_def) lemma square_free_separable_main: fixes f :: "'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes "square_free f" and sep: "¬ separable f" shows "∃ g k. f = g * k ∧ degree g ≠ 0 ∧ pderiv g = 0" proof - note cop = sep[unfolded separable_def] from assms have f: "f ≠ 0" unfolding square_free_def by auto let ?g = "gcd f (pderiv f)" define G where "G = ?g" from poly_gcd_monic[of f "pderiv f"] f have mon: "monic ?g" by auto have deg: "degree G > 0" proof (cases "degree G") case 0 from degree0_coeffs[OF this] cop mon show ?thesis by (auto simp: G_def coprime_iff_gcd_eq_1) qed auto have gf: "G dvd f" unfolding G_def by auto have gf': "G dvd pderiv f" unfolding G_def by auto from irreducible⇩_{d}_factor[OF deg] obtain g r where g: "irreducible g" and G: "G = g * r" by auto from gf have gf: "g dvd f" unfolding G by (rule dvd_mult_left) from gf' have gf': "g dvd pderiv f" unfolding G by (rule dvd_mult_left) have g0: "degree g ≠ 0" using g unfolding irreducible⇩_{d}_def by auto from gf obtain k where fgk: "f = g * k" unfolding dvd_def by auto have id1: "pderiv f = g * pderiv k + k * pderiv g" unfolding fgk pderiv_mult by simp from gf' obtain h where "pderiv f = g * h" unfolding dvd_def by auto from id1[unfolded this] have "k * pderiv g = g * (h - pderiv k)" by (simp add: field_simps) hence dvd: "g dvd k * pderiv g" unfolding dvd_def by auto { assume "g dvd k" then obtain h where k: "k = g * h" unfolding dvd_def by auto with fgk have "g * g dvd f" by auto with g0 have "¬ square_free f" unfolding square_free_def using f by auto with assms have False by simp } with g dvd have "g dvd pderiv g" by auto from divides_degree[OF this] degree_pderiv_le[of g] g0 have "pderiv g = 0" by linarith with fgk g0 show ?thesis by auto qed lemma square_free_imp_separable: fixes f :: "'a :: {field_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes "square_free f" shows "separable f" proof (rule ccontr) assume "¬ separable f" from square_free_separable_main[OF assms this] obtain g k where *: "f = g * k" "degree g ≠ 0" "pderiv g = 0" by auto hence "g dvd pderiv g" by auto thus False unfolding dvd_pderiv_iff using * by auto qed lemma square_free_iff_separable: "square_free (f :: 'a :: {field_char_0,factorial_ring_gcd,semiring_gcd_mult_normalize} poly) = separable f" using separable_imp_square_free[of f] square_free_imp_separable[of f] by auto context assumes "SORT_CONSTRAINT('a::{field,factorial_ring_gcd})" begin lemma square_free_smult: "c ≠ 0 ⟹ square_free (f :: 'a poly) ⟹ square_free (smult c f)" by (unfold square_free_def, insert dvd_smult_cancel[of _ c], auto) lemma square_free_smult_iff[simp]: "c ≠ 0 ⟹ square_free (smult c f) = square_free (f :: 'a poly)" using square_free_smult[of c f] square_free_smult[of "inverse c" "smult c f"] by auto end context assumes "SORT_CONSTRAINT('a::factorial_ring_gcd)" begin definition square_free_factorization :: "'a poly ⇒ 'a × ('a poly × nat) list ⇒ bool" where "square_free_factorization p cbs ≡ case cbs of (c,bs) ⇒ (p = smult c (∏(a, i)∈ set bs. a ^ i)) ∧ (p = 0 ⟶ c = 0 ∧ bs = []) ∧ (∀ a i. (a,i) ∈ set bs ⟶ square_free a ∧ degree a > 0 ∧ i > 0) ∧ (∀ a i b j. (a,i) ∈ set bs ⟶ (b,j) ∈ set bs ⟶ (a,i) ≠ (b,j) ⟶ coprime a b) ∧ distinct bs" lemma square_free_factorizationD: assumes "square_free_factorization p (c,bs)" shows "p = smult c (∏(a, i)∈ set bs. a ^ i)" "(a,i) ∈ set bs ⟹ square_free a ∧ degree a ≠ 0 ∧ i > 0" "(a,i) ∈ set bs ⟹ (b,j) ∈ set bs ⟹ (a,i) ≠ (b,j) ⟹ coprime a b" "p = 0 ⟹ c = 0 ∧ bs = []" "distinct bs" using assms unfolding square_free_factorization_def split by blast+ lemma square_free_factorization_prod_list: assumes "square_free_factorization p (c,bs)" shows "p = smult c (prod_list (map (λ (a,i). a ^ i) bs))" proof - note sff = square_free_factorizationD[OF assms] show ?thesis unfolding sff(1) by (simp add: prod.distinct_set_conv_list[OF sff(5)]) qed end subsection ‹Yun's factorization algorithm› locale yun_gcd = fixes Gcd :: "'a :: factorial_ring_gcd poly ⇒ 'a poly ⇒ 'a poly" begin partial_function (tailrec) yun_factorization_main :: "'a poly ⇒ 'a poly ⇒ nat ⇒ ('a poly × nat)list ⇒ ('a poly × nat)list" where [code]: "yun_factorization_main bn cn i sqr = ( if bn = 1 then sqr else ( let dn = cn - pderiv bn; an = Gcd bn dn in yun_factorization_main (bn div an) (dn div an) (Suc i) ((an,Suc i) # sqr)))" definition yun_monic_factorization :: "'a poly ⇒ ('a poly × nat)list" where "yun_monic_factorization p = (let pp = pderiv p; u = Gcd p pp; b0 = p div u; c0 = pp div u in (filter (λ (a,i). a ≠ 1) (yun_factorization_main b0 c0 0 [])))" definition square_free_monic_poly :: "'a poly ⇒ 'a poly" where "square_free_monic_poly p = (p div (Gcd p (pderiv p)))" end declare yun_gcd.yun_monic_factorization_def [code] declare yun_gcd.yun_factorization_main.simps [code] declare yun_gcd.square_free_monic_poly_def [code] context fixes Gcd :: "'a :: {field_char_0,euclidean_ring_gcd} poly ⇒ 'a poly ⇒ 'a poly" begin interpretation yun_gcd Gcd . definition square_free_poly :: "'a poly ⇒ 'a poly" where "square_free_poly p = (if p = 0 then 0 else square_free_monic_poly (smult (inverse (coeff p (degree p))) p))" definition yun_factorization :: "'a poly ⇒ 'a × ('a poly × nat)list" where "yun_factorization p = (if p = 0 then (0,[]) else (let c = coeff p (degree p); q = smult (inverse c) p in (c, yun_monic_factorization q)))" lemma yun_factorization_0[simp]: "yun_factorization 0 = (0,[])" unfolding yun_factorization_def by simp end locale monic_factorization = fixes as :: "('a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly × nat) set" and p :: "'a poly" assumes p: "p = prod (λ (a,i). a ^ Suc i) as" and fin: "finite as" assumes as_distinct: "⋀ a i b j. (a,i) ∈ as ⟹ (b,j) ∈ as ⟹ (a,i) ≠ (b,j) ⟹ a ≠ b" and as_irred: "⋀ a i. (a,i) ∈ as ⟹ irreducible⇩_{d}a" and as_monic: "⋀ a i. (a,i) ∈ as ⟹ monic a" begin lemma poly_exp_expand: "p = (prod (λ (a,i). a ^ i) as) * prod (λ (a,i). a) as" unfolding p prod.distrib[symmetric] by (rule prod.cong, auto) lemma pderiv_exp_prod: "pderiv p = (prod (λ (a,i). a ^ i) as * sum (λ (a,i). prod (λ (b,j). b) (as - {(a,i)}) * smult (of_nat (Suc i)) (pderiv a)) as)" unfolding p pderiv_prod sum_distrib_left proof (rule sum.cong[OF refl]) fix x assume "x ∈ as" then obtain a i where x: "x = (a,i)" and mem: "(a,i) ∈ as" by (cases x, auto) let ?si = "smult (of_nat (Suc i)) :: 'a poly ⇒ 'a poly" show "(∏(a, i)∈as - {x}. a ^ Suc i) * pderiv (case x of (a, i) ⇒ a ^ Suc i) = (∏(a, i)∈as. a ^ i) * (case x of (a, i) ⇒ (∏(a, i)∈as - {(a, i)}. a) * smult (of_nat (Suc i)) (pderiv a))" unfolding x split pderiv_power_Suc proof - let ?prod = "∏(a, i)∈as - {(a, i)}. a ^ Suc i" let ?l = "?prod * (?si (a ^ i) * pderiv a)" let ?r = "(∏(a, i)∈as. a ^ i) * ((∏(a, i)∈as - {(a, i)}. a) * ?si (pderiv a))" have "?r = a ^ i * ((∏(a, i)∈as - {(a, i)}. a ^ i) * (∏(a, i)∈as - {(a, i)}. a) * ?si (pderiv a))" unfolding prod.remove[OF fin mem] by (simp add: ac_simps) also have "(∏(a, i)∈as - {(a, i)}. a ^ i) * (∏(a, i)∈as - {(a, i)}. a) = ?prod" unfolding prod.distrib[symmetric] by (rule prod.cong[OF refl], auto) finally show "?l = ?r" by (simp add: ac_simps) qed qed lemma monic_gen: assumes "bs ⊆ as" shows "monic (∏ (a, i) ∈ bs. a)" by (rule monic_prod, insert assms as_monic, auto) lemma nonzero_gen: assumes "bs ⊆ as" shows "(∏ (a, i) ∈ bs. a) ≠ 0" using monic_gen[OF assms] by auto lemma monic_Prod: "monic ((∏(a, i)∈as. a ^ i))" by (rule monic_prod, insert as_monic, auto intro: monic_power) lemma coprime_generic: assumes bs: "bs ⊆ as" and f: "⋀ a i. (a,i) ∈ bs ⟹ f i > 0" shows "coprime (∏(a, i) ∈ bs. a) (∑(a, i)∈ bs. (∏(b, j)∈ bs - {(a, i)} . b) * smult (of_nat (f i)) (pderiv a))" (is "coprime ?single ?onederiv") proof - have single: "?single ≠ 0" by (rule nonzero_gen[OF bs]) show ?thesis proof (rule gcd_eq_1_imp_coprime, rule gcdI [symmetric]) fix k assume dvd: "k dvd ?single" "k dvd ?onederiv" note bs_monic = as_monic[OF subsetD[OF bs]] from dvd(1) single have k: "k ≠ 0" by auto show "k dvd 1" proof (cases "degree k > 0") case False with k obtain c where "k = [:c:]" by (auto dest: degree0_coeffs) with k have "c ≠ 0" by auto with ‹k = [:c:]› show "is_unit k" using dvdI [of 1 "[:c:]" "[:1 / c:]"] by auto next case True from irreducible⇩_{d}_factor[OF this] obtain p q where k: "k = p * q" and p: "irreducible p" by auto from k dvd have dvd: "p dvd ?single" "p dvd ?onederiv" unfolding dvd_def by auto from irreducible_dvd_prod[OF p dvd(1)] obtain a i where ai: "(a,i) ∈ bs" and pa: "p dvd a" by force then obtain q where a: "a = p * q" unfolding dvd_def by auto from p[unfolded irreducible⇩_{d}_def] have p0: "degree p > 0" by auto from irreducible⇩_{d}_dvd_smult[OF p0 as_irred pa] ai bs obtain c where c: "c ≠ 0" and ap: "a = smult c p" by auto hence ap': "p = smult (1/c) a" by auto let ?prod = "λ a i. (∏(b, j)∈bs - {(a, i)}. b) * smult (of_nat (f i)) (pderiv a)" let ?prod' = "λ aa ii a i. (∏(b, j)∈bs - {(a, i),(aa,ii)}. b) * smult (of_nat (f i)) (pderiv a)" define factor where "factor = sum (λ (b,j). ?prod' a i b j ) (bs - {(a,i)})" define fac where "fac = q * factor" from fin finite_subset[OF bs] have fin: "finite bs" by auto have "?onederiv = ?prod a i + sum (λ (b,j). ?prod b j) (bs - {(a,i)})" by (subst sum.remove[OF fin ai], auto) also have "sum (λ (b,j). ?prod b j) (bs - {(a,i)}) = a * factor" unfolding factor_def sum_distrib_left proof (rule sum.cong[OF refl]) fix bj assume mem: "bj ∈ bs - {(a,i)}" obtain b j where bj: "bj = (b,j)" by force from mem bj ai have ai: "(a,i) ∈ bs - {(b,j)}" by auto have id: "bs - {(b, j)} - {(a, i)} = bs - {(b,j),(a,i)}" by auto show "(λ (b,j). ?prod b j) bj = a * (λ (b,j). ?prod' a i b j) bj" unfolding bj split by (subst prod.remove[OF _ ai], insert fin, auto simp: id ac_simps) qed finally have "?onederiv = ?prod a i + p * fac" unfolding fac_def a by simp from dvd(2)[unfolded this] have "p dvd ?prod a i" by algebra from this[unfolded field_poly_irreducible_dvd_mult[OF p]] have False proof assume "p dvd (∏(b, j)∈bs - {(a, i)}. b)" from irreducible_dvd_prod[OF p this] obtain b j where bj': "(b,j) ∈ bs - {(a,i)}" and pb: "p dvd b" by auto hence bj: "(b,j) ∈ bs" by auto from as_irred bj bs have "irreducible⇩_{d}b" by auto from irreducible⇩_{d}_dvd_smult[OF p0 this pb] obtain d where d: "d ≠ 0" and b: "b = smult d p" by auto with ap c have id: "smult (c/d) b = a" and deg: "degree a = degree b" by auto from coeff_smult[of "c/d" b "degree b", unfolded id] deg bs_monic[OF ai] bs_monic[OF bj] have "c / d = 1" by simp from id[unfolded this] have "a = b" by simp with as_distinct[OF subsetD[OF bs ai] subsetD[OF bs bj]] bj' show False by auto next from f[OF ai] obtain k where fi: "f i = Suc k" by (cases "f i", auto) assume "p dvd smult (of_nat (f i)) (pderiv a)" hence "p dvd (pderiv a)" unfolding fi using dvd_smult_cancel of_nat_eq_0_iff by blast from this[unfolded ap] have "p dvd pderiv p" using c by (metis ‹p dvd pderiv a› ap' dvd_trans dvd_triv_right mult.left_neutral pderiv_smult smult_dvd_cancel) with not_dvd_pderiv p0 show False by auto qed thus "k dvd 1" by simp qed qed (insert ‹?single ≠ 0›, auto) qed lemma pderiv_exp_gcd: "gcd p (pderiv p) = (∏(a, i)∈as. a ^ i)" (is "_ = ?prod") proof - let ?sum = "(∑(a, i)∈as. (∏(b, j)∈as - {(a, i)}. b) * smult (of_nat (Suc i)) (pderiv a))" let ?single = "(∏(a, i)∈as. a)" let ?prd = "λ a i. (∏(b, j)∈as - {(a, i)}. b) * smult (of_nat (Suc i)) (pderiv a)" let ?onederiv = "∑(a, i)∈as. ?prd a i" have pp: "pderiv p = ?prod * ?sum" by (rule pderiv_exp_prod) have p: "p = ?prod * ?single" by (rule poly_exp_expand) have monic: "monic ?prod" by (rule monic_Prod) have gcd: "coprime ?single ?onederiv" by (rule coprime_generic, auto) then have gcd: "gcd ?single ?onederiv = 1" by simp show ?thesis unfolding pp unfolding p poly_gcd_monic_factor [OF monic] gcd by simp qed lemma p_div_gcd_p_pderiv: "p div (gcd p (pderiv p)) = (∏(a, i)∈as. a)" unfolding pderiv_exp_gcd unfolding poly_exp_expand by (rule nonzero_mult_div_cancel_left, insert monic_Prod, auto) fun A B C D :: "nat ⇒ 'a poly" where "A n = gcd (B n) (D n)" | "B 0 = p div (gcd p (pderiv p))" | "B (Suc n) = B n div A n" | "C 0 = pderiv p div (gcd p (pderiv p))" | "C (Suc n) = D n div A n" | "D n = C n - pderiv (B n)" lemma A_B_C_D: "A n = (∏ (a, i) ∈ as ∩ UNIV × {n}. a)" "B n = (∏ (a, i) ∈ as - UNIV × {0 ..< n}. a)" "C n = (∑(a, i)∈as - UNIV × {0 ..< n}. (∏(b, j)∈as - UNIV × {0 ..< n} - {(a, i)}. b) * smult (of_nat (Suc i - n)) (pderiv a))" "D n = (∏ (a, i) ∈ as ∩ UNIV × {n}. a) * (∑ (a,i)∈as - UNIV × {0 ..< Suc n}. (∏(b, j)∈ as - UNIV × {0 ..< Suc n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a)))" proof (induct n and n and n and n rule: A_B_C_D.induct) case (1 n) (* A *) note Bn = 1(1) note Dn = 1(2) have "(∏(a, i)∈as - UNIV × {0..< n}. a) = (∏(a, i)∈as ∩ UNIV × {n}. a) * (∏(a, i)∈as - UNIV × {0..<Suc n}. a)" by (subst prod.union_disjoint[symmetric], auto, insert fin, auto intro: prod.cong) note Bn' = Bn[unfolded this] let ?an = "(∏ (a, i) ∈ as ∩ UNIV × {n}. a)" let ?bn = "(∏(a, i)∈as - UNIV × {0..<Suc n}. a)" show "A n = ?an" unfolding A.simps proof (rule gcdI[symmetric, OF _ _ _ normalize_monic[OF monic_gen]]) have monB1: "monic (B n)" unfolding Bn by (rule monic_gen, auto) hence "B n ≠ 0" by auto let ?dn = "(∑ (a,i)∈as - UNIV × {0 ..< Suc n}. (∏(b, j)∈ as - UNIV × {0 ..< Suc n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a)))" have Dn: "D n = ?an * ?dn" unfolding Dn by auto show dvd1: "?an dvd B n" unfolding Bn' dvd_def by blast show dvd2: "?an dvd D n" unfolding Dn dvd_def by blast { fix k assume "k dvd B n" "k dvd D n" from dvd_gcd_mult[OF this[unfolded Bn' Dn]] have "k dvd ?an * (gcd ?bn ?dn)" . moreover have "coprime ?bn ?dn" by (rule coprime_generic, auto) ultimately show "k dvd ?an" by simp } qed auto next case 2 (* B 0 *) have as: "as - UNIV × {0..<0} = as" by auto show ?case unfolding B.simps as p_div_gcd_p_pderiv by auto next case (3 n) (* B n *) have id: "(∏(a, i)∈as - UNIV × {0..< n}. a) = (∏(a, i)∈as - UNIV × {0..<Suc n}. a) * (∏(a, i)∈as ∩ UNIV × {n}. a)" by (subst prod.union_disjoint[symmetric], auto, insert fin, auto intro: prod.cong) show ?case unfolding B.simps 3 id by (subst nonzero_mult_div_cancel_right[OF nonzero_gen], auto) next case 4 (* C 0 *) have as: "as - UNIV × {0..<0} = as" "⋀ i. Suc i - 0 = Suc i" by auto show ?case unfolding C.simps pderiv_exp_gcd unfolding pderiv_exp_prod as by (rule nonzero_mult_div_cancel_left, insert monic_Prod, auto) next case (5 n) (* C n *) show ?case unfolding C.simps 5 by (subst nonzero_mult_div_cancel_left, rule nonzero_gen, auto) next case (6 n) (* D n *) let ?f = "λ (a,i). (∏(b, j)∈as - UNIV × {0 ..< n} - {(a, i)}. b) * (smult (of_nat (i - n)) (pderiv a))" have "D n = (∑ (a,i)∈as - UNIV × {0 ..< n}. (∏(b, j)∈as - UNIV × {0 ..< n} - {(a, i)}. b) * (smult (of_nat (Suc i - n)) (pderiv a) - pderiv a))" unfolding D.simps 6 pderiv_prod sum_subtractf[symmetric] right_diff_distrib by (rule sum.cong, auto) also have "… = sum ?f (as - UNIV × {0 ..< n})" proof (rule sum.cong[OF refl]) fix x assume "x ∈ as - UNIV × {0 ..< n}" then obtain a i where x: "x = (a,i)" and i: "Suc i > n" by (cases x, auto) hence id: "Suc i - n = Suc (i - n)" by arith have id: "of_nat (Suc i - n) = of_nat (i - n) + (1 :: 'a)" unfolding id by simp have id: "smult (of_nat (Suc i - n)) (pderiv a) - pderiv a = smult (of_nat (i - n)) (pderiv a)" unfolding id smult_add_left by auto have cong: "⋀ x y z :: 'a poly. x = y ⟹ x * z = y * z" by auto show "(case x of (a, i) ⇒ (∏(b, j)∈as - UNIV × {0..<n} - {(a, i)}. b) * (smult (of_nat (Suc i - n)) (pderiv a) - pderiv a)) = (case x of (a, i) ⇒ (∏(b, j)∈as - UNIV × {0..<n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a))" unfolding x split id by (rule cong, auto) qed also have "… = sum ?f (as - UNIV × {0 ..< Suc n}) + sum ?f (as ∩ UNIV × {n})" by (subst sum.union_disjoint[symmetric], insert fin, auto intro: sum.cong) also have "sum ?f (as ∩ UNIV × {n}) = 0" by (rule sum.neutral, auto) finally have id: "D n = sum ?f (as - UNIV × {0 ..< Suc n})" by simp show ?case unfolding id sum_distrib_left proof (rule sum.cong[OF refl]) fix x assume mem: "x ∈ as - UNIV × {0 ..< Suc n}" obtain a i where x: "x = (a,i)" by force with mem have i: "i > n" by auto have cong: "⋀ x y z v :: 'a poly. x = y * v ⟹ x * z = y * (v * z)" by auto show "(case x of (a, i) ⇒ (∏(b, j)∈as - UNIV × {0..<n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a)) = (∏(a, i)∈as ∩ UNIV × {n}. a) * (case x of (a, i) ⇒ (∏(b, j)∈as - UNIV × {0..<Suc n} - {(a, i)}. b) * smult (of_nat (i - n)) (pderiv a))" unfolding x split by (rule cong, subst prod.union_disjoint[symmetric], insert fin, (auto)[3], rule prod.cong, insert i, auto) qed qed lemmas A = A_B_C_D(1) lemmas B = A_B_C_D(2) lemmas ABCD_simps = A.simps B.simps C.simps D.simps declare ABCD_simps[simp del] lemma prod_A: "(∏i = 0..< n. A i ^ Suc i) = (∏(a, i)∈ as ∩ UNIV × {0 ..< n}. a ^ Suc i)" proof (induct n) case (Suc n) have id: "{0 ..< Suc n} = insert n {0 ..< n}" by auto have id2: "as ∩ UNIV × {0 ..< Suc n} = as ∩ UNIV × {n} ∪ as ∩ UNIV × {0 ..< n}" by auto have cong: "⋀ x y z. x = y ⟹ x * z = y * z" by auto show ?case unfolding id2 unfolding id proof (subst prod.insert; (subst prod.union_disjoint)?; (unfold Suc)?; (unfold A, rule cong)?) show "(∏(a, i)∈as ∩ UNIV × {n}. a) ^ Suc n = (∏(a, i)∈as ∩ UNIV × {n}. a ^ Suc i)" unfolding prod_power_distrib by (rule prod.cong, auto) qed (insert fin, auto) qed simp lemma prod_A_is_p_unknown: assumes "⋀ a i. (a,i) ∈ as ⟹ i < n" shows "p = (∏i = 0..< n. A i ^ Suc i)" proof - have "p = (∏(a, i)∈as. a ^ Suc i)" by (rule p) also have "… = (∏i = 0..< n. A i ^ Suc i)" unfolding prod_A by (rule prod.cong, insert assms, auto) finally show ?thesis . qed definition bound :: nat where "bound = Suc (Max (snd ` as))" lemma bound: assumes m: "m ≥ bound" shows "B m = 1" proof - let ?set = "as - UNIV × {0..<m}" { fix a i assume ai: "(a,i) ∈ ?set" hence "i ∈ snd ` as" by force from Max_ge[OF _ this] fin have "i ≤ Max (snd ` as)" by auto with ai m[unfolded bound_def] have False by auto } hence id: "?set = {}" by force show "B m = 1" unfolding B id by simp qed lemma coprime_A_A: assumes "i ≠ j" shows "coprime (A i) (A j)" proof (rule coprimeI) fix k assume dvd: "k dvd A i" "k dvd A j" have Ai: "A i ≠ 0" unfolding A by (rule nonzero_gen, auto) with dvd have k: "k ≠ 0" by auto show "is_unit k" proof (cases "degree k > 0") case False then obtain c where kc: "k = [: c :]" by (auto dest: degree0_coeffs) with k have "1 = k * [:1 / c:]" by simp thus ?thesis unfolding dvd_def by blast next case True from irreducible_monic_factor[OF this] obtain q r where k: "k = q * r" and q: "irreducible q" and mq: "monic q" by auto with dvd have dvd: "q dvd A i" "q dvd A j" unfolding dvd_def by auto from q have q0: "degree q > 0" unfolding irreducible⇩_{d}_def by auto from irreducible_dvd_prod[OF q dvd(1)[unfolded A]] obtain a where ai: "(a,i) ∈ as" and qa: "q dvd a" by auto from irreducible_dvd_prod[OF q dvd(2)[unfolded A]] obtain b where bj: "(b,j) ∈ as" and qb: "q dvd b" by auto from as_distinct[OF ai bj] assms have neq: "a ≠ b" by auto from irreducible⇩_{d}_dvd_smult[OF q0 as_irred[OF ai] qa] irreducible⇩_{d}_dvd_smult[OF q0 as_irred[OF bj] qb] obtain c d where "c ≠ 0" "d ≠ 0" "a = smult c q" "b = smult d q" by auto hence ab: "a = smult (c / d) b" and "c / d ≠ 0" by auto with as_monic[OF bj] as_monic[OF ai] arg_cong[OF ab, of "λ p. coeff p (degree p)"] have "a = b" unfolding coeff_smult degree_smult_eq by auto with neq show ?thesis by auto qed qed lemma A_monic: "monic (A i)" unfolding A by (rule monic_gen, auto) lemma A_square_free: "square_free (A i)" proof (rule square_freeI) fix q k have mon: "monic (A i)" by (rule A_monic) hence Ai: "A i ≠ 0" by auto assume q: "degree q > 0" and dvd: "q * q dvd A i" from irreducible_monic_factor[OF q] obtain r s where q: "q = r * s" and irr: "irreducible r" and mr: "monic r" by auto from dvd[unfolded q] have dvd2: "r * r dvd A i" and dvd1: "r dvd A i" unfolding dvd_def by auto from irreducible_dvd_prod[OF irr dvd1[unfolded A]] obtain a where ai: "(a,i) ∈ as" and ra: "r dvd a" by auto let ?rem = "(∏(a, i)∈as ∩ UNIV × {i} - {(a,i)}. a)" have a: "irreducible⇩_{d}a" by (rule as_irred[OF ai]) from irreducible⇩_{d}_dvd_smult[OF _ a ra] irr obtain c where ar: "a = smult c r" and "c ≠ 0" by force with mr as_monic[OF ai] arg_cong[OF ar, of "λ p. coeff p (degree p)"] have "a = r" unfolding coeff_smult degree_smult_eq by auto with dvd2 have dvd: "a * a dvd A i" by simp have id: "A i = a * ?rem" unfolding A by (subst prod.remove[of _ "(a,i)"], insert ai fin, auto) with dvd have "a dvd ?rem" using a id Ai by auto from irreducible_dvd_prod[OF _ this] a obtain b where bi: "(b,i) ∈ as" and neq: "b ≠ a" and ab: "a dvd b" by auto from as_irred[OF bi] have b: "irreducible⇩_{d}b" . from irreducible⇩_{d}_dvd_smult[OF _ b ab] a[unfolded irreducible⇩_{d}_def] obtain c where "c ≠ 0" and ba: "b = smult c a" by auto with as_monic[OF bi] as_monic[OF ai] arg_cong[OF ba, of "λ p. coeff p (degree p)"] have "a = b" unfolding coeff_smult degree_smult_eq by auto with neq show False by auto qed (insert A_monic[of i], auto) lemma prod_A_is_p_B_bound: assumes "B n = 1" shows "p = (∏i = 0..< n. A i ^ Suc i)" proof (rule prod_A_is_p_unknown) fix a i assume ai: "(a,i) ∈ as" let ?rem = "(∏(a, i)∈as - UNIV × {0..<n} - {(a,i)}. a)" have rem: "?rem ≠ 0" by (rule nonzero_gen, auto) have "irreducible⇩_{d}a" using as_irred[OF ai] . hence a: "a ≠ 0" "degree a ≠ 0" unfolding irreducible⇩_{d}_def by auto show "i < n" proof (rule ccontr) assume "¬ ?thesis" hence "i ≥ n" by auto with ai have mem: "(a,i) ∈ as - UNIV × {0 ..< n}" by auto have "0 = degree (∏(a, i)∈as - UNIV × {0..<n}. a)" using assms unfolding B by simp also have "… = degree (a * ?rem)" by (subst prod.remove[OF _ mem], insert fin, auto) also have "… = degree a + degree ?rem" by (rule degree_mult_eq[OF a(1) rem]) finally show False using a(2) by auto qed qed interpretation yun_gcd gcd . lemma square_free_monic_poly: "(poly (square_free_monic_poly p) x = 0) = (poly p x = 0)" proof - show ?thesis unfolding square_free_monic_poly_def unfolding p_div_gcd_p_pderiv unfolding p poly_prod prod_zero_iff[OF fin] by force qed lemma yun_factorization_induct: assumes base: "⋀ bn cn. bn = 1 ⟹ P bn cn" and step: "⋀ bn cn. bn ≠ 1 ⟹ P (bn div (gcd bn (cn - pderiv bn))) ((cn - pderiv bn) div (gcd bn (cn - pderiv bn))) ⟹ P bn cn" and id: "bn = p div gcd p (pderiv p)" "cn = pderiv p div gcd p (pderiv p)" shows "P bn cn" proof - define n where "n = (0 :: nat)" let ?m = "λ n. bound - n" have "P (B n) (C n)" proof (induct n rule: wf_induct[OF wf_measure[of ?m]]) case (1 n) note IH = 1(1)[rule_format] show ?case proof (cases "B n = 1") case True with base show ?thesis by auto next case False note Bn = this with bound[of n] have "¬ bound ≤ n" by auto hence "(Suc n, n) ∈ measure ?m" by auto note IH = IH[OF this] show ?thesis by (rule step[OF Bn], insert IH, simp add: D.simps C.simps B.simps A.simps) qed qed thus ?thesis unfolding id n_def B.simps C.simps . qed lemma yun_factorization_main: assumes "yun_factorization_main (B n) (C n) n bs = cs" "set bs = {(A i, Suc i) | i. i < n}" "distinct (map snd bs)" shows "∃ m. set cs = {(A i, Suc i) | i. i < m} ∧ B m = 1 ∧ distinct (map snd cs)" using assms proof - let ?m = "λ n. bound - n" show ?thesis using assms proof (induct n arbitrary: bs rule: wf_induct[OF wf_measure[of ?m]]) case (1 n) note IH = 1(1)[rule_format] have res: "yun_factorization_main (B n) (C n) n bs = cs" by fact note res = res[unfolded yun_factorization_main.simps[of "B n"]] have bs: "set bs = {(A i, Suc i) |i. i < n}" "distinct (map snd bs)" by fact+ show ?case proof (cases "B n = 1") case True with res have "bs = cs" by auto with True bs show ?thesis by auto next case False note Bn = this with bound[of n] have "¬ bound ≤ n" by auto hence "(Suc n, n) ∈ measure ?m" by auto note IH = IH[OF this] from Bn res[unfolded Let_def, folded D.simps C.simps B.simps A.simps] have res: "yun_factorization_main (B (Suc n)) (C (Suc n)) (Suc n) ((A n, Suc n) # bs) = cs" by simp note IH = IH[OF this] { fix i assume "i < Suc n" "¬ i < n" hence "n = i" by arith } note missing = this have "set ((A n, Suc n) # bs) = {(A i, Suc i) |i. i < Suc n}" unfolding list.simps bs by (auto, subst missing, auto) note IH = IH[OF this] from bs have "distinct (map snd ((A n, Suc n) # bs))" by auto note IH = IH[OF this] show ?thesis by (rule IH) qed qed qed lemma yun_monic_factorization_res: assumes res: "yun_monic_factorization p = bs" shows "∃ m. set bs = {(A i, Suc i) | i. i < m ∧ A i ≠ 1} ∧ B m = 1 ∧ distinct (map snd bs)" proof - from res[unfolded yun_monic_factorization_def Let_def, folded B.simps C.simps] obtain cs where yun: "yun_factorization_main (B 0) (C 0) 0 [] = cs" and bs: "bs = filter (λ (a,i). a ≠ 1) cs" by auto from yun_factorization_main[OF yun] obtain m where "set cs = {(A i, Suc i) |i. i < m}" "B m = 1" "distinct (map snd cs)" by auto thus ?thesis unfolding bs by (auto simp: distinct_map_filter) qed lemma yun_monic_factorization: assumes yun: "yun_monic_factorization p = bs" shows "square_free_factorization p (1,bs)" "(b,i) ∈ set bs ⟹ monic b" "distinct (map snd bs)" proof - from yun_monic_factorization_res[OF yun] obtain m where bs: "set bs = {(A i, Suc i) | i. i < m ∧ A i ≠ 1}" and B: "B m = 1" and dist: "distinct (map snd bs)" by auto have id: "{0 ..< m} = {i. i < m ∧ A i = 1} ∪ {i. i < m ∧ A i ≠ 1}" (is "_ = ?ignore ∪ _") by auto have "p = (∏i = 0..<m. A i ^ Suc i)" by (rule prod_A_is_p_B_bound[OF B]) also have "… = prod (λ i. A i ^ Suc i) {i. i < m ∧ A i ≠ 1}" unfolding id by (subst prod.union_disjoint, (force+)[3], subst prod.neutral[of ?ignore], auto) also have "… = (∏(a, i)∈ set bs. a ^ i)" unfolding bs by (rule prod.reindex_cong[of "(λ n. n - 1) o snd"], auto simp: inj_on_def, force) finally have 1: "p = (∏(a, i)∈ set bs. a ^ i)" . { fix a i assume "(a,i) ∈ set bs" then obtain j where A: "a = A j" "A j ≠ 1" and i: "i ≠ 0" unfolding bs by auto with A_square_free[of j] A_monic[of j] have "square_free a ∧ degree a ≠ 0" "monic a" "i ≠ 0" by (auto simp: monic_degree_0) } note 2 = this { fix a i b j assume ai: "(a,i) ∈ set bs" and bj: "(b,j) ∈ set bs" and neq: "(a,i) ≠ (b,j)" then obtain i' j' where a: "a = A i'" and b: "b = A j'" and ij': "i = Suc i'" "j = Suc j'" unfolding bs by auto from neq dist ai bj have neq: "i' ≠ j'" using a b ij' by blast from coprime_A_A [OF neq] have "coprime a b" unfolding a b . } note 3 = this have "monic p" unfolding p by (rule monic_prod, insert as_monic, auto intro: monic_power monic_mult) hence 4: "p ≠ 0" by auto from dist have 5: "distinct bs" unfolding distinct_map .. show "square_free_factorization p (1,bs)" unfolding square_free_factorization_def using 1 2 3 4 5 by auto show "(b,i) ∈ set bs ⟹ monic b" using 2 by auto show "distinct (map snd bs)" by fact qed end lemma monic_factorization: assumes "monic p" shows "∃ as. monic_factorization as p" proof - from monic_irreducible_factorization[OF assms] obtain as f where fin: "finite as" and p: "p = (∏a∈as. a ^ Suc (f a))" and as: "as ⊆ {q. irreducible⇩_{d}q ∧ monic q}" by auto define cs where "cs = {(a, f a) | a. a ∈ as}" show ?thesis proof (rule exI, standard) show "finite cs" unfolding cs_def using fin by auto { fix a i assume "(a,i) ∈ cs" thus "irreducible⇩_{d}a" "monic a" unfolding cs_def using as by auto } note irr = this show "⋀a i b j. (a, i) ∈ cs ⟹ (b, j) ∈ cs ⟹ (a, i) ≠ (b, j) ⟹ a ≠ b" unfolding cs_def by auto show "p = (∏(a, i)∈cs. a ^ Suc i)" unfolding p cs_def by (rule prod.reindex_cong, auto, auto simp: inj_on_def) qed qed lemma square_free_monic_poly: assumes "monic (p :: 'a :: {field_char_0, euclidean_ring_gcd,semiring_gcd_mult_normalize} poly)" shows "(poly (yun_gcd.square_free_monic_poly gcd p) x = 0) = (poly p x = 0)" proof - from monic_factorization[OF assms] obtain as where "monic_factorization as p" .. from monic_factorization.square_free_monic_poly[OF this] show ?thesis . qed lemma yun_factorization_induct: assumes base: "⋀ bn cn. bn = 1 ⟹ P bn cn" and step: "⋀ bn cn. bn ≠ 1 ⟹ P (bn div (gcd bn (cn - pderiv bn))) ((cn - pderiv bn) div (gcd bn (cn - pderiv bn))) ⟹ P bn cn" and id: "bn = p div gcd p (pderiv p)" "cn = pderiv p div gcd p (pderiv p)" and monic: "monic (p :: 'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly)" shows "P bn cn" proof - from monic_factorization[OF monic] obtain as where "monic_factorization as p" .. from monic_factorization.yun_factorization_induct[OF this base step id] show ?thesis . qed lemma square_free_poly: "(poly (square_free_poly gcd p) x = 0) = (poly p x = 0)" proof (cases "p = 0") case True thus ?thesis unfolding square_free_poly_def by auto next case False let ?c = "coeff p (degree p)" let ?ic = "inverse ?c" have id: "square_free_poly gcd p = yun_gcd.square_free_monic_poly gcd (smult ?ic p)" unfolding square_free_poly_def using False by auto from False have mon: "monic (smult ?ic p)" and ic: "?ic ≠ 0" by auto show ?thesis unfolding id square_free_monic_poly[OF mon] using ic by simp qed lemma yun_monic_factorization: fixes p :: "'a :: {field_char_0,euclidean_ring_gcd,semiring_gcd_mult_normalize} poly" assumes res: "yun_gcd.yun_monic_factorization gcd p = bs" and monic: "monic p" shows "square_free_factorization p (1,bs)" "(b,i) ∈ set bs ⟹ monic b" "distinct (map snd bs)" proof - from monic_factorization[OF monic] obtain as where "monic_factorization as p" .. from "monic_factorization.yun_monic_factorization"[OF this res] show "square_free_factorization p (1,bs)" "(b,i) ∈ set bs ⟹ monic b" "distinct (map snd bs)" by auto qed lemma square_free_factorization_smult: assumes c: "c ≠ 0" and sf: "square_free_factorization p (d,bs)" shows "square_free_factorization (smult c p) (c * d, bs)" proof - from sf[unfolded square_free_factorization_def split] have p: "p = smult d (∏(a, i)∈set bs. a ^ i)" and eq: "p = 0 ⟶ d = 0 ∧ bs = []" by blast+ from eq c have eq: "smult c p = 0 ⟶ c * d = 0 ∧ bs = []" by auto from p have p: "smult c p = smult (c * d) (∏(a, i)∈set bs. a ^ i)" by auto from eq p sf show ?thesis unfolding square_free_factorization_def by blast qed lemma yun_factorization: assumes res: "yun_factorization gcd p = c_bs" shows "square_free_factorization p c_bs" "(b,i) ∈ set (snd c_bs) ⟹ monic b" proof - interpret yun_gcd gcd . note res = res[unfolded yun_factorization_def Let_def] have "square_free_factorization p c_bs ∧ ((b,i) ∈ set (snd c_bs) ⟶ monic b)" proof (cases "p = 0") case True with res have "c_bs = (0, [])" by auto thus ?thesis unfolding True by (auto simp: square_free_factorization_def) next case False let ?c = "coeff p (degree p)" let ?ic = "inverse ?c" obtain c bs where cbs: "c_bs = (c,bs)" by force with False res have c: "c = ?c" "?c ≠ 0" and fact: "yun_monic_factorization (smult ?ic p) = bs" by auto from False have mon: "monic (smult ?ic p)" by auto from yun_monic_factorization[OF fact mon] have sff: "square_free_factorization (smult ?ic p) (1, bs)" "(b, i) ∈ set bs ⟹ monic b" by auto have id: "smult ?c (smult ?ic p) = p" using False by auto from square_free_factorization_smult[OF c(2) sff(1), unfolded id] sff show ?thesis unfolding cbs c by simp qed thus "square_free_factorization p c_bs" "(b,i) ∈ set (snd c_bs) ⟹ monic b" by blast+ qed lemma prod_list_pow: "(∏x←bs. (x :: 'a :: comm_monoid_mult) ^ i) = prod_list bs ^ i" by (induct bs, auto simp: field_simps) declare irreducible_linear_field_poly[intro!] context assumes "SORT_CONSTRAINT('a :: {field, factorial_ring_gcd,semiring_gcd_mult_normalize})" begin lemma square_free_factorization_order_root_mem: assumes sff: "square_free_factorization p (c,bs)" and p: "p ≠ (0 :: 'a poly)" and ai: "(a,i) ∈ set bs" and rt: "poly a x = 0" shows "order x p = i" proof - note sff = square_free_factorizationD[OF sff] let ?prod = "(∏(a, i)∈set bs. a ^ i)" from sff have pf: "p = smult c ?prod" by blast with p have c: "c ≠ 0" by auto have ord: "order x p = order x ?prod" unfolding pf using order_smult[OF c] by auto define q where "q = [: -x, 1 :]" have q0: "q ≠ 0" unfolding q_def by auto have iq: "irreducible q" by (auto simp: q_def) from rt have qa: "q dvd a" unfolding q_def poly_eq_0_iff_dvd . then obtain b where aqb: "a = q * b" unfolding dvd_def by auto from sff(2)[OF ai] have sq: "square_free a" and mon: "degree a ≠ 0" by auto let ?rem = "(∏(a, i)∈set bs - {(a,i)}. a ^ i)" have p0: "?prod ≠ 0" using p pf by auto have "?prod = a ^ i * ?rem" by (subst prod.remove[OF _ ai], auto) also have "a ^ i = q ^ i * b ^ i" unfolding aqb by (simp add: field_simps) finally have id: "?prod = q ^ i * (b ^ i * ?rem)" by simp hence dvd: "q ^ i dvd ?prod" by auto { assume "q ^ Suc i dvd ?prod" hence "q dvd ?prod div q ^ i" by (metis dvd dvd_0_left_iff dvd_div_iff_mult p0 power_Suc) also have "?prod div q ^ i = b ^ i * ?rem" unfolding id by (rule nonzero_mult_div_cancel_left, insert q0, auto) finally have "q dvd b ∨ q dvd ?rem" using iq irreducible_dvd_pow[OF iq] by auto hence False proof assume "q dvd b" with aqb have "q * q dvd a" by auto with sq[unfolded square_free_def] mon iq show False unfolding irreducible⇩_{d}_def by auto next assume "q dvd ?rem" from irreducible_dvd_prod[OF iq this] obtain b j where bj: "(b,j) ∈ set bs" and neq: "(a,i) ≠ (b,j)" and dvd: "q dvd b ^ j" by auto from irreducible_dvd_pow[OF iq dvd] have qb: "q dvd b" . from sff(3)[OF ai bj neq] have gcd: "coprime a b" . from qb qa have "q dvd gcd a b" by simp from dvd_imp_degree_le[OF this[unfolded gcd]] iq q0 show False using gcd by auto qed } hence ndvd: "¬ q ^ Suc i dvd ?prod" by blast with dvd have "order x ?prod = i" unfolding q_def by (metis order_unique_lemma) thus ?thesis unfolding ord . qed lemma square_free_factorization_order_root_no_mem: assumes sff: "square_free_factorization p (c,bs)" and p: "p ≠ (0 :: 'a poly)" and no_root: "⋀ a i. (a,i) ∈ set bs ⟹ poly a x ≠ 0" shows "order x p = 0" proof (rule ccontr) assume o0: "order x p ≠ 0" with order_root[of p x] p have 0: "poly p x = 0" by auto note sff = square_free_factorizationD[OF sff] let ?prod = "(∏(a, i)∈set bs. a ^ i)" from sff have pf: "p = smult c ?prod" by blast with p have c: "c ≠ 0" by auto with 0 have 0: "poly ?prod x = 0" unfolding pf by auto define q where "q = [: -x, 1 :]" from 0 have dvd: "q dvd ?prod" unfolding poly_eq_0_iff_dvd by (simp add: q_def) have q0: "q ≠ 0" unfolding q_def by auto have iq: "irreducible q" by (unfold q_def, auto intro:) from irreducible_dvd_prod[OF iq dvd] obtain a i where ai: "(a,i) ∈ set bs" and dvd: "q dvd a ^ Suc i" by auto from irreducible_dvd_pow[OF iq dvd] have dvd: "q dvd a" . hence "poly a x = 0" unfolding q_def by (simp add: poly_eq_0_iff_dvd q_def) with no_root[OF ai] show False by simp qed lemma square_free_factorization_order_root: assumes sff: "square_free_factorization p (c,bs)" and p: "p ≠ (0 :: 'a poly)" shows "order x p = i ⟷ (i = 0 ∧ (∀ a j. (a,j) ∈ set bs ⟶ poly a x ≠ 0) ∨ (∃ a j. (a,j) ∈ set bs ∧ poly a x = 0 ∧ i = j))" (is "?l = (?r1 ∨ ?r2)") proof - note mem = square_free_factorization_order_root_mem[OF sff p] note no_mem = square_free_factorization_order_root_no_mem[OF sff p] show ?thesis proof assume "?r1 ∨ ?r2" thus ?l proof assume ?r2 then obtain a j where aj: "(a,j) ∈ set bs" "poly a x = 0" and i: "i = j" by auto from mem[OF aj] i show ?l by simp next assume ?r1 with no_mem[of x] show ?l by auto qed next assume ?l show "?r1 ∨ ?r2" proof (cases "∃a j. (a, j) ∈ set bs ∧ poly a x = 0") case True then obtain a j where "(a, j) ∈ set bs" "poly a x = 0" by auto with mem[OF this] ‹?l› have ?r2 by auto thus ?thesis .. next case False with no_mem[of x] ‹?l› have ?r1 by auto thus ?thesis .. qed qed qed lemma square_free_factorization_root: assumes sff: "square_free_factorization p (c,bs)" and p: "p ≠ (0 :: 'a poly)" shows "{x. poly p x