diff --git a/thys/Algebraic_Numbers/Algebraic_Numbers.thy b/thys/Algebraic_Numbers/Algebraic_Numbers.thy --- a/thys/Algebraic_Numbers/Algebraic_Numbers.thy +++ b/thys/Algebraic_Numbers/Algebraic_Numbers.thy @@ -1,1348 +1,1348 @@ (* 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_Divisibility + 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 \\<^sub>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 \\<^sub>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 \\<^sub>p x_y = 0" by simp then have "poly_lift p \\<^sub>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 \\<^sub>p x_y" by (simp add: eq_neg_iff_add_eq_0) then have "degree [:[:a:]:] = degree (x_y * poly_lift p \\<^sub>p x_y)" by simp also have "... = degree (x_y::'a poly poly) + degree (poly_lift p \\<^sub>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 \\<^sub>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 \\<^sub>p x_y \\<^sub>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 \\<^sub>p x_y" by (unfold bijective_eq_bij) (rule involuntory_imp_bij) interpret x_y_hom: idom_isom "\p :: 'a poly poly. p \\<^sub>p x_y" by standard simp_all have \factor_preserving_hom (\p :: 'a poly poly. p \\<^sub>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 \\<^sub>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 {.. = ?f n + sum ?f {.. = 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 {.. {.. 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 \ {.. \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.. 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.._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 \ {.. j \ {.. i < j \ \ i > \ j} = {.. {n.. ?lhs" thus "ij \ ?rhs" by (simp add: \_def split: prod.splits if_splits) auto qed (auto simp: \_def) hence "inversions_on {.. = 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.. (+) n ` {.. \. signof \ * (\i=0.. i)))" have "degree (f \) = degree (\i=0.. i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "\ = (\i=0.. i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "\ = (\i i))) + (\i (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(\i i))) = (\i_def m_def n_def) also have "(\i (n + i)))) = (\i_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.. \ \" for \ proof (cases "\i\{0.. i) = 0") case True hence *: "(\i = 0.. 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.. i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "\ = (\i=0.. i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "\ = (\i i))) + (\i (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(\i (n + i)))) = (\i_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat \_def m_def n_def) also have "(\i i))) < (\ix\{.. 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 i \ \ i" proof (rule ccontr) assume nex: "~(\i 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\{.. 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.. i)))" by (simp add: f_def sign_def lead_coeff_prod) also have "(\i=0.. i))) = (\i i))) * (\i (n + i))))" by (subst indices_eq, subst prod.union_disjoint) (auto simp: prod.reindex) also have "(\i i))) = (\i_def sylvester_index_mat) also have "(\i (n + i)))) = (\i_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..)" by (simp add: det_def m_def n_def M_def f_def) also have "{\. \ permutes {0.. ({\. \ permutes {0..})" using \ by auto also have "(\\\\. f \) = (\\\{\. \ permutes {0..}. f \) + f \" by (subst sum.insert) (auto simp: finite_permutations) also have "lead_coeff \ = lead_coeff (f \)" proof - have "degree (\\\{\. \ permutes {0..}. 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.. (+) n ` {.. \. signof \ * (\i=0.. i)))" have "degree (f id) = degree (\i=0.. = (\i=0.. = (\iiiiii) < m * n" if "\ permutes {0.. \ id" for \ proof (cases "\i\{0.. i) = 0") case True hence *: "(\i = 0.. 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.. i))" using nz by (auto simp: f_def degree_mult_eq sign_def) also have "\ = (\i=0.. i)))" using nz by (subst degree_prod_eq_sum_degree) auto also have "\ = (\i i))) + (\i (n + i))))" by (subst indices_eq, subst sum.union_disjoint) (auto simp: sum.reindex) also have "(\i (n + i)))) = (\i_less by (intro sum.cong) (auto simp: M_def sylvester_index_mat m_def n_def) also have "(\i i))) < (\ix\{.. 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 i \ i" proof (rule ccontr) assume nex: "\(\i 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" 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.. 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\{.. 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..i=0..iiiiii\ | \ permutes {0..)" by (simp add: det_def m_def n_def M_def f_def) also have "{\. \ permutes {0... \ permutes {0..\\\. f \) = (\\\{\. \ permutes {0..) + f id" by (subst sum.insert) (auto simp: finite_permutations) also have "lead_coeff \ = lead_coeff (f id)" proof - have "degree (\\\{\. \ permutes {0..) < 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 id) = 1\ by simp qed lemma algebraic_int_plus [intro]: fixes x y :: "'a :: field_char_0" assumes "algebraic_int x" "algebraic_int y" shows "algebraic_int (x + y)" proof - from assms(1) obtain p where p: "lead_coeff p = 1" "ipoly p x = 0" by (auto simp: algebraic_int_altdef_ipoly) from assms(2) obtain q where q: "lead_coeff q = 1" "ipoly q y = 0" by (auto simp: algebraic_int_altdef_ipoly) have deg_pos: "degree p > 0" "degree q > 0" using p q by (auto intro!: Nat.gr0I elim!: degree_eq_zeroE) define r where "r = poly_add_sign (degree p) (degree q) * poly_add p q" have "lead_coeff r = 1" using p q deg_pos by (simp add: r_def lead_coeff_mult poly_add_sign_def sign_def lead_coeff_poly_add) moreover have "ipoly r (x + y) = 0" using p q by (simp add: ipoly_poly_add r_def of_int_poly_hom.hom_mult) ultimately show ?thesis by (auto simp: algebraic_int_altdef_ipoly) qed lemma algebraic_int_times [intro]: fixes x y :: "'a :: field_char_0" assumes "algebraic_int x" "algebraic_int y" shows "algebraic_int (x * y)" proof (cases "y = 0") case [simp]: False from assms(1) obtain p where p: "lead_coeff p = 1" "ipoly p x = 0" by (auto simp: algebraic_int_altdef_ipoly) from assms(2) obtain q where q: "lead_coeff q = 1" "ipoly q y = 0" by (auto simp: algebraic_int_altdef_ipoly) have deg_pos: "degree p > 0" "degree q > 0" using p q by (auto intro!: Nat.gr0I elim!: degree_eq_zeroE) have [simp]: "q \ 0" using q by auto define n where "n = Polynomial.order 0 q" have "monom 1 n dvd q" by (simp add: n_def monom_1_dvd_iff) then obtain q' where q_split: "q = q' * monom 1 n" by auto have "Polynomial.order 0 q = Polynomial.order 0 q' + n" using \q \ 0\ unfolding q_split by (subst order_mult) auto hence "poly q' 0 \ 0" unfolding n_def using \q \ 0\ by (simp add: q_split order_root) have q': "ipoly q' y = 0" "lead_coeff q' = 1" using q_split q by (auto simp: of_int_poly_hom.hom_mult poly_monom lead_coeff_mult degree_monom_eq) from this have deg_pos': "degree q' > 0" by (intro Nat.gr0I) (auto elim!: degree_eq_zeroE) from \poly q' 0 \ 0\ have [simp]: "coeff q' 0 \ 0" by (auto simp: monom_1_dvd_iff' poly_0_coeff_0) have "p represents x" "q' represents y" using p q' by (auto simp: represents_def) hence "poly_mult p q' represents x * y" by (rule represents_mult) (simp add: poly_0_coeff_0) moreover have "lead_coeff (poly_mult p q') = 1" using p deg_pos q' deg_pos' by (simp add: lead_coeff_mult lead_coeff_poly_mult) ultimately show ?thesis by (auto simp: algebraic_int_altdef_ipoly represents_def) qed auto lemma algebraic_int_power [intro]: "algebraic_int (x :: 'a :: field_char_0) \ algebraic_int (x ^ n)" by (induction n) auto lemma algebraic_int_diff [intro]: fixes x y :: "'a :: field_char_0" assumes "algebraic_int x" "algebraic_int y" shows "algebraic_int (x - y)" using algebraic_int_plus[OF assms(1) algebraic_int_minus[OF assms(2)]] by simp lemma algebraic_int_sum [intro]: "(\x. x \ A \ algebraic_int (f x :: 'a :: field_char_0)) \ algebraic_int (sum f A)" by (induction A rule: infinite_finite_induct) auto lemma algebraic_int_prod [intro]: "(\x. x \ A \ algebraic_int (f x :: 'a :: field_char_0)) \ algebraic_int (prod f A)" by (induction A rule: infinite_finite_induct) auto lemma algebraic_int_nth_root_real_iff: "algebraic_int (root n x) \ n = 0 \ algebraic_int x" proof - have "algebraic_int x" if "algebraic_int (root n x)" "n \ 0" proof - from that(1) have "algebraic_int (root n x ^ n)" by auto also have "root n x ^ n = (if even n then \x\ else x)" using sgn_power_root[of n x] that(2) by (auto simp: sgn_if split: if_splits) finally show ?thesis by (auto split: if_splits) qed thus ?thesis by auto qed lemma algebraic_int_power_iff: "algebraic_int (x ^ n :: 'a :: field_char_0) \ n = 0 \ algebraic_int x" proof - have "algebraic_int x" if "algebraic_int (x ^ n)" "n > 0" proof (rule algebraic_int_root) show "poly (monom 1 n) x = x ^ n" by (auto simp: poly_monom) qed (use that in \auto simp: degree_monom_eq\) thus ?thesis by auto qed lemma algebraic_int_power_iff' [simp]: "n > 0 \ algebraic_int (x ^ n :: 'a :: field_char_0) \ algebraic_int x" by (subst algebraic_int_power_iff) auto lemma algebraic_int_sqrt_iff [simp]: "algebraic_int (sqrt x) \ algebraic_int x" by (simp add: sqrt_def algebraic_int_nth_root_real_iff) lemma algebraic_int_csqrt_iff [simp]: "algebraic_int (csqrt x) \ algebraic_int x" proof assume "algebraic_int (csqrt x)" hence "algebraic_int (csqrt x ^ 2)" by (rule algebraic_int_power) thus "algebraic_int x" by simp qed auto lemma algebraic_int_norm_complex [intro]: assumes "algebraic_int (z :: complex)" shows "algebraic_int (norm z)" proof - from assms have "algebraic_int (z * cnj z)" by auto also have "z * cnj z = of_real (norm z ^ 2)" by (rule complex_norm_square [symmetric]) finally show ?thesis by simp qed hide_const (open) x_y end diff --git a/thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy b/thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy --- a/thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy +++ b/thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy @@ -1,258 +1,258 @@ (* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) subsection \Chinese Remainder Theorem for Polynomials\ text \We prove the Chinese Remainder Theorem, and strengthen it by showing uniqueness\ theory Chinese_Remainder_Poly imports "HOL-Number_Theory.Residues" - Polynomial_Factorization.Polynomial_Divisibility + Polynomial_Factorization.Polynomial_Irreducibility Polynomial_Interpolation.Missing_Polynomial begin lemma cong_add_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \ [c = d] (mod m) \ [a + c = b + d] (mod m)" by (fact cong_add) lemma cong_mult_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \ [c = d] (mod m) \ [a * c = b * d] (mod m)" by (fact cong_mult) lemma cong_mult_self_poly: "[(a::'b::{field_gcd} poly) * m = 0] (mod m)" by (fact cong_mult_self_right) lemma cong_scalar2_poly: "[(a::'b::{field_gcd} poly)= b] (mod m) \ [k * a = k * b] (mod m)" by (fact cong_scalar_left) lemma cong_sum_poly: "(\x. x \ A \ [((f x)::'b::{field_gcd} poly) = g x] (mod m)) \ [(\x\A. f x) = (\x\A. g x)] (mod m)" by (rule cong_sum) lemma cong_iff_lin_poly: "([(a::'b::{field_gcd} poly) = b] (mod m)) = (\k. b = a + m * k)" using cong_diff_iff_cong_0 [of b a m] by (auto simp add: cong_0_iff dvd_def algebra_simps dest: cong_sym) lemma cong_solve_poly: "(a::'b::{field_gcd} poly) \ 0 \ \x. [a * x = gcd a n] (mod n)" proof (cases "n = 0") case True note n0=True show ?thesis proof (cases "monic a") case True have n: "normalize a = a" by (rule normalize_monic[OF True]) show ?thesis by (rule exI[of _ 1], auto simp add: n0 n cong_def) next case False show ?thesis by (auto simp add: True cong_def normalize_poly_old_def map_div_is_smult_inverse) (metis mult.right_neutral mult_smult_right) qed next case False note n_not_0 = False show ?thesis using bezout_coefficients_fst_snd [of a n, symmetric] by (auto simp add: cong_iff_lin_poly mult.commute [of a] mult.commute [of n]) qed lemma cong_solve_coprime_poly: assumes coprime_an:"coprime (a::'b::{field_gcd} poly) n" shows "\x. [a * x = 1] (mod n)" proof (cases "a = 0") case True show ?thesis unfolding cong_def using True coprime_an by auto next case False show ?thesis using coprime_an cong_solve_poly[OF False, of n] unfolding cong_def by presburger qed lemma cong_dvd_modulus_poly: "[x = y] (mod m) \ n dvd m \ [x = y] (mod n)" for x y :: "'b::{field_gcd} poly" by (auto simp add: cong_iff_lin_poly elim!: dvdE) lemma chinese_remainder_aux_poly: fixes A :: "'a set" and m :: "'a \ 'b::{field_gcd} poly" assumes fin: "finite A" and cop: "\i \ A. (\j \ A. i \ j \ coprime (m i) (m j))" shows "\b. (\i \ A. [b i = 1] (mod m i) \ [b i = 0] (mod (\j \ A - {i}. m j)))" proof (rule finite_set_choice, rule fin, rule ballI) fix i assume "i : A" with cop have "coprime (\j \ A - {i}. m j) (m i)" by (auto intro: prod_coprime_left) then have "\x. [(\j \ A - {i}. m j) * x = 1] (mod m i)" by (elim cong_solve_coprime_poly) then obtain x where "[(\j \ A - {i}. m j) * x = 1] (mod m i)" by auto moreover have "[(\j \ A - {i}. m j) * x = 0] (mod (\j \ A - {i}. m j))" by (subst mult.commute, rule cong_mult_self_poly) ultimately show "\a. [a = 1] (mod m i) \ [a = 0] (mod prod m (A - {i}))" by blast qed (*The Chinese Remainder Theorem for polynomials: *) lemma chinese_remainder_poly: fixes A :: "'a set" and m :: "'a \ 'b::{field_gcd} poly" and u :: "'a \ 'b poly" assumes fin: "finite A" and cop: "\i\A. (\j\A. i \ j \ coprime (m i) (m j))" shows "\x. (\i\A. [x = u i] (mod m i))" proof - from chinese_remainder_aux_poly [OF fin cop] obtain b where bprop: "\i\A. [b i = 1] (mod m i) \ [b i = 0] (mod (\j \ A - {i}. m j))" by blast let ?x = "\i\A. (u i) * (b i)" show "?thesis" proof (rule exI, clarify) fix i assume a: "i : A" show "[?x = u i] (mod m i)" proof - from fin a have "?x = (\j \ {i}. u j * b j) + (\j \ A - {i}. u j * b j)" by (subst sum.union_disjoint [symmetric], auto intro: sum.cong) then have "[?x = u i * b i + (\j \ A - {i}. u j * b j)] (mod m i)" unfolding cong_def by auto also have "[u i * b i + (\j \ A - {i}. u j * b j) = u i * 1 + (\j \ A - {i}. u j * 0)] (mod m i)" apply (rule cong_add_poly) apply (rule cong_scalar2_poly) using bprop a apply blast apply (rule cong_sum) apply (rule cong_scalar2_poly) using bprop apply auto apply (rule cong_dvd_modulus_poly) apply (drule (1) bspec) apply (erule conjE) apply assumption apply rule using fin a apply auto done thus ?thesis by (metis (no_types, lifting) a add.right_neutral fin mult_cancel_left1 mult_cancel_right1 sum.not_neutral_contains_not_neutral sum.remove) qed qed qed (*********************** Now we try to prove the uniqueness **********************) lemma cong_trans_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \ [b = c] (mod m) \ [a = c] (mod m)" by (fact cong_trans) lemma cong_mod_poly: "(n::'b::{field_gcd} poly) ~= 0 \ [a mod n = a] (mod n)" by auto lemma cong_sym_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) \ [b = a] (mod m)" by (fact cong_sym) lemma cong_1_poly: "[(a::'b::{field_gcd} poly) = b] (mod 1)" by (fact cong_1) lemma coprime_cong_mult_poly: assumes "[(a::'b::{field_gcd} poly) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n" shows "[a = b] (mod m * n)" using divides_mult assms by (metis (no_types, opaque_lifting) cong_dvd_modulus_poly cong_iff_lin_poly dvd_mult2 dvd_refl minus_add_cancel mult.right_neutral) lemma coprime_cong_prod_poly: "(\i\A. (\j\A. i \ j \ coprime (m i) (m j))) \ (\i\A. [(x::'b::{field_gcd} poly) = y] (mod m i)) \ [x = y] (mod (\i\A. m i))" apply (induct A rule: infinite_finite_induct) apply auto apply (metis coprime_cong_mult_poly prod_coprime_right) done lemma cong_less_modulus_unique_poly: "[(x::'b::{field_gcd} poly) = y] (mod m) \ degree x < degree m \ degree y < degree m \ x = y" by (simp add: cong_def mod_poly_less) lemma chinese_remainder_unique_poly: fixes A :: "'a set" and m :: "'a \ 'b::{field_gcd} poly" and u :: "'a \ 'b poly" assumes nz: "\i\A. (m i) \ 0" and cop: "\i\A. (\j\A. i \ j \ coprime (m i) (m j))" (*The following assumption should not be necessary, but I need it since in Isabelle degree 0 is 0 instead of -\*) and not_constant: "0 < degree (prod m A)" shows "\!x. degree x < (\i\A. degree (m i)) \ (\i\A. [x = u i] (mod m i))" proof - from not_constant have fin: "finite A" by (metis degree_1 gr_implies_not0 prod.infinite) from chinese_remainder_poly [OF fin cop] obtain y where one: "(\i\A. [y = u i] (mod m i))" by blast let ?x = "y mod (\i\A. m i)" have degree_prod_sum: "degree (prod m A) = (\i\A. degree (m i))" by (rule degree_prod_eq_sum_degree[OF nz]) from fin nz have prodnz: "(\i\A. (m i)) \ 0" by auto (*This would hold without the premise not_constant if degree 0 = -\*) have less: "degree ?x < (\i\A. degree (m i))" unfolding degree_prod_sum[symmetric] using degree_mod_less[OF prodnz, of y] using not_constant by auto have cong: "\i\A. [?x = u i] (mod m i)" apply auto apply (rule cong_trans_poly) prefer 2 using one apply auto apply (rule cong_dvd_modulus_poly) apply (rule cong_mod_poly) using prodnz apply auto apply rule apply (rule fin) apply assumption done have unique: "\z. degree z < (\i\A. degree (m i)) \ (\i\A. [z = u i] (mod m i)) \ z = ?x" proof (clarify) fix z::"'b poly" assume zless: "degree z < (\i\A. degree (m i))" assume zcong: "(\i\A. [z = u i] (mod m i))" have deg1: "degree z < degree (prod m A)" using degree_prod_sum zless by simp have deg2: "degree ?x < degree (prod m A)" by (metis deg1 degree_0 degree_mod_less gr0I gr_implies_not0) have "\i\A. [?x = z] (mod m i)" apply clarify apply (rule cong_trans_poly) using cong apply (erule bspec) apply (rule cong_sym_poly) using zcong by auto with fin cop have "[?x = z] (mod (\i\A. m i))" by (intro coprime_cong_prod_poly) auto with zless show "z = ?x" apply (intro cong_less_modulus_unique_poly) apply (erule cong_sym_poly) apply (auto simp add: deg1 deg2) done qed from less cong unique show ?thesis by blast qed end diff --git a/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy b/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy --- a/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy +++ b/thys/Berlekamp_Zassenhaus/Unique_Factorization.thy @@ -1,971 +1,971 @@ theory Unique_Factorization imports Polynomial_Interpolation.Ring_Hom_Poly - Polynomial_Factorization.Polynomial_Divisibility + Polynomial_Factorization.Polynomial_Irreducibility "HOL-Combinatorics.Permutations" "HOL-Computational_Algebra.Euclidean_Algorithm" Containers.Containers_Auxiliary (* only for a lemma *) More_Missing_Multiset "HOL-Algebra.Divisibility" begin hide_const(open) Divisibility.prime Divisibility.irreducible hide_fact(open) Divisibility.irreducible_def Divisibility.irreducibleI Divisibility.irreducibleD Divisibility.irreducibleE hide_const (open) Rings.coprime lemma irreducible_uminus [simp]: fixes a::"'a::idom" shows "irreducible (-a) \ irreducible a" using irreducible_mult_unit_left[of "-1::'a"] by auto context comm_monoid_mult begin definition coprime :: "'a \ 'a \ bool" where coprime_def': "coprime p q \ \r. r dvd p \ r dvd q \ r dvd 1" lemma coprimeI: assumes "\r. r dvd p \ r dvd q \ r dvd 1" shows "coprime p q" using assms by (auto simp: coprime_def') lemma coprimeE: assumes "coprime p q" and "(\r. r dvd p \ r dvd q \ r dvd 1) \ thesis" shows thesis using assms by (auto simp: coprime_def') lemma coprime_commute [ac_simps]: "coprime p q \ coprime q p" by (auto simp add: coprime_def') lemma not_coprime_iff_common_factor: "\ coprime p q \ (\r. r dvd p \ r dvd q \ \ r dvd 1)" by (auto simp add: coprime_def') end lemma (in algebraic_semidom) coprime_iff_coprime [simp, code]: "coprime = Rings.coprime" by (simp add: fun_eq_iff coprime_def coprime_def') lemma (in comm_semiring_1) coprime_0 [simp]: "coprime p 0 \ p dvd 1" "coprime 0 p \ p dvd 1" by (auto intro: coprimeI elim: coprimeE dest: dvd_trans) (**** until here ****) (* TODO: move or...? *) lemma dvd_rewrites: "dvd.dvd ((*)) = (dvd)" by (unfold dvd.dvd_def dvd_def, rule) subsection \Interfacing UFD properties\ hide_const (open) Divisibility.irreducible context comm_monoid_mult_isom begin lemma coprime_hom[simp]: "coprime (hom x) y' \ coprime x (Hilbert_Choice.inv hom y')" proof- show ?thesis by (unfold coprime_def', fold ball_UNIV, subst surj[symmetric], simp) qed lemma coprime_inv_hom[simp]: "coprime (Hilbert_Choice.inv hom x') y \ coprime x' (hom y)" proof- interpret inv: comm_monoid_mult_isom "Hilbert_Choice.inv hom".. show ?thesis by simp qed end subsubsection \Original part\ lemma dvd_dvd_imp_smult: fixes p q :: "'a :: idom poly" assumes pq: "p dvd q" and qp: "q dvd p" shows "\c. p = smult c q" proof (cases "p = 0") case True then show ?thesis by auto next case False from qp obtain r where r: "p = q * r" by (elim dvdE, auto) with False qp have r0: "r \ 0" and q0: "q \ 0" by auto with divides_degree[OF pq] divides_degree[OF qp] False have "degree p = degree q" by auto with r degree_mult_eq[OF q0 r0] have "degree r = 0" by auto from degree_0_id[OF this] obtain c where "r = [:c:]" by metis from r[unfolded this] show ?thesis by auto qed lemma dvd_const: assumes pq: "(p::'a::semidom poly) dvd q" and q0: "q \ 0" and degq: "degree q = 0" shows "degree p = 0" proof- from dvdE[OF pq] obtain r where *: "q = p * r". with q0 have "p \ 0" "r \ 0" by auto from degree_mult_eq[OF this] degq * show "degree p = 0" by auto qed context Rings.dvd begin abbreviation ddvd (infix "ddvd" 40) where "x ddvd y \ x dvd y \ y dvd x" lemma ddvd_sym[sym]: "x ddvd y \ y ddvd x" by auto end context comm_monoid_mult begin lemma ddvd_trans[trans]: "x ddvd y \ y ddvd z \ x ddvd z" using dvd_trans by auto lemma ddvd_transp: "transp (ddvd)" by (intro transpI, fact ddvd_trans) end context comm_semiring_1 begin definition mset_factors where "mset_factors F p \ F \ {#} \ (\f. f \# F \ irreducible f) \ p = prod_mset F" lemma mset_factorsI[intro!]: assumes "\f. f \# F \ irreducible f" and "F \ {#}" and "prod_mset F = p" shows "mset_factors F p" unfolding mset_factors_def using assms by auto lemma mset_factorsD: assumes "mset_factors F p" shows "f \# F \ irreducible f" and "F \ {#}" and "prod_mset F = p" using assms[unfolded mset_factors_def] by auto lemma mset_factorsE[elim]: assumes "mset_factors F p" and "(\f. f \# F \ irreducible f) \ F \ {#} \ prod_mset F = p \ thesis" shows thesis using assms[unfolded mset_factors_def] by auto lemma mset_factors_imp_not_is_unit: assumes "mset_factors F p" shows "\ p dvd 1" proof(cases F) case empty with assms show ?thesis by auto next case (add f F) with assms have "\ f dvd 1" "p = f * prod_mset F" by (auto intro!: irreducible_not_unit) then show ?thesis by auto qed definition primitive_poly where "primitive_poly f \ \d. (\i. d dvd coeff f i) \ d dvd 1" end lemma(in semidom) mset_factors_imp_nonzero: assumes "mset_factors F p" shows "p \ 0" proof assume "p = 0" moreover from assms have "prod_mset F = p" by auto ultimately obtain f where "f \# F" "f = 0" by auto with assms show False by auto qed class ufd = idom + assumes mset_factors_exist: "\x. x \ 0 \ \ x dvd 1 \ \F. mset_factors F x" and mset_factors_unique: "\x F G. mset_factors F x \ mset_factors G x \ rel_mset (ddvd) F G" subsubsection \Connecting to HOL/Divisibility\ context comm_semiring_1 begin abbreviation "mk_monoid \ \carrier = UNIV - {0}, mult = (*), one = 1\" lemma carrier_0[simp]: "x \ carrier mk_monoid \ x \ 0" by auto lemmas mk_monoid_simps = carrier_0 monoid.simps abbreviation irred where "irred \ Divisibility.irreducible mk_monoid" abbreviation factor where "factor \ Divisibility.factor mk_monoid" abbreviation factors where "factors \ Divisibility.factors mk_monoid" abbreviation properfactor where "properfactor \ Divisibility.properfactor mk_monoid" lemma factors: "factors fs y \ prod_list fs = y \ Ball (set fs) irred" proof - have "prod_list fs = foldr (*) fs 1" by (induct fs, auto) thus ?thesis unfolding factors_def by auto qed lemma factor: "factor x y \ (\z. z \ 0 \ x * z = y)" unfolding factor_def by auto lemma properfactor_nz: shows "(y :: 'a) \ 0 \ properfactor x y \ x dvd y \ \ y dvd x" by (auto simp: properfactor_def factor_def dvd_def) lemma mem_Units[simp]: "y \ Units mk_monoid \ y dvd 1" unfolding dvd_def Units_def by (auto simp: ac_simps) end context idom begin lemma irred_0[simp]: "irred (0::'a)" by (unfold Divisibility.irreducible_def, auto simp: factor properfactor_def) lemma factor_idom[simp]: "factor (x::'a) y \ (if y = 0 then x = 0 else x dvd y)" by (cases "y = 0"; auto intro: exI[of _ 1] elim: dvdE simp: factor) lemma associated_connect[simp]: "(\\<^bsub>mk_monoid\<^esub>) = (ddvd)" by (intro ext, unfold associated_def, auto) lemma essentially_equal_connect[simp]: "essentially_equal mk_monoid fs gs \ rel_mset (ddvd) (mset fs) (mset gs)" by (auto simp: essentially_equal_def rel_mset_via_perm) lemma irred_idom_nz: assumes x0: "(x::'a) \ 0" shows "irred x \ irreducible x" using x0 by (auto simp: irreducible_altdef Divisibility.irreducible_def properfactor_nz) lemma dvd_dvd_imp_unit_mult: assumes xy: "x dvd y" and yx: "y dvd x" shows "\z. z dvd 1 \ y = x * z" proof(cases "x = 0") case True with xy show ?thesis by (auto intro: exI[of _ 1]) next case x0: False from xy obtain z where z: "y = x * z" by (elim dvdE, auto) from yx obtain w where w: "x = y * w" by (elim dvdE, auto) from z w have "x * (z * w) = x" by (auto simp: ac_simps) then have "z * w = 1" using x0 by auto with z show ?thesis by (auto intro: exI[of _ z]) qed lemma irred_inner_nz: assumes x0: "x \ 0" shows "(\b. b dvd x \ \ x dvd b \ b dvd 1) \ (\a b. x = a * b \ a dvd 1 \ b dvd 1)" (is "?l \ ?r") proof (intro iffI allI impI) assume l: ?l fix a b assume xab: "x = a * b" then have ax: "a dvd x" and bx: "b dvd x" by auto { assume a1: "\ a dvd 1" with l ax have xa: "x dvd a" by auto from dvd_dvd_imp_unit_mult[OF ax xa] obtain z where z1: "z dvd 1" and xaz: "x = a * z" by auto from xab x0 have "a \ 0" by auto with xab xaz have "b = z" by auto with z1 have "b dvd 1" by auto } then show "a dvd 1 \ b dvd 1" by auto next assume r: ?r fix b assume bx: "b dvd x" and xb: "\ x dvd b" then obtain a where xab: "x = a * b" by (elim dvdE, auto simp: ac_simps) with r consider "a dvd 1" | "b dvd 1" by auto then show "b dvd 1" proof(cases) case 2 then show ?thesis by auto next case 1 then obtain c where ac1: "a * c = 1" by (elim dvdE, auto) from xab have "x * c = b * (a * c)" by (auto simp: ac_simps) with ac1 have "x * c = b" by auto then have "x dvd b" by auto with xb show ?thesis by auto qed qed lemma irred_idom[simp]: "irred x \ x = 0 \ irreducible x" by (cases "x = 0"; simp add: irred_idom_nz irred_inner_nz irreducible_def) lemma assumes "x \ 0" and "factors fs x" and "f \ set fs" shows "f \ 0" using assms by (auto simp: factors) lemma factors_as_mset_factors: assumes x0: "x \ 0" and x1: "x \ 1" shows "factors fs x \ mset_factors (mset fs) x" using assms by (auto simp: factors prod_mset_prod_list) end context ufd begin interpretation comm_monoid_cancel: comm_monoid_cancel "mk_monoid::'a monoid" apply (unfold_locales) apply simp_all using mult_left_cancel apply (auto simp: ac_simps) done lemma factors_exist: assumes "a \ 0" and "\ a dvd 1" shows "\fs. set fs \ UNIV - {0} \ factors fs a" proof- from mset_factors_exist[OF assms] obtain F where "mset_factors F a" by auto also from ex_mset obtain fs where "F = mset fs" by metis finally have fs: "mset_factors (mset fs) a". then have "factors fs a" using assms by (subst factors_as_mset_factors, auto) moreover have "set fs \ UNIV - {0}" using fs by (auto elim!: mset_factorsE) ultimately show ?thesis by auto qed lemma factors_unique: assumes fs: "factors fs a" and gs: "factors gs a" and a0: "a \ 0" and a1: "\ a dvd 1" shows "rel_mset (ddvd) (mset fs) (mset gs)" proof- from a1 have "a \ 1" by auto with a0 fs gs have "mset_factors (mset fs) a" "mset_factors (mset gs) a" by (unfold factors_as_mset_factors) from mset_factors_unique[OF this] show ?thesis. qed lemma factorial_monoid: "factorial_monoid (mk_monoid :: 'a monoid)" by (unfold_locales; auto simp add: factors_exist factors_unique) end lemma (in idom) factorial_monoid_imp_ufd: assumes "factorial_monoid (mk_monoid :: 'a monoid)" shows "class.ufd ((*) :: 'a \ _) 1 (+) 0 (-) uminus" proof (unfold_locales) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact assms) { fix x assume x: "x \ 0" "\ x dvd 1" note * = factors_exist[simplified, OF this] with x show "\F. mset_factors F x" by (subst(asm) factors_as_mset_factors, auto) } fix x F G assume FG: "mset_factors F x" "mset_factors G x" with mset_factors_imp_not_is_unit have x1: "\ x dvd 1" by auto from FG(1) have x0: "x \ 0" by (rule mset_factors_imp_nonzero) obtain fs gs where fsgs: "F = mset fs" "G = mset gs" using ex_mset by metis note FG = FG[unfolded this] then have 0: "0 \ set fs" "0 \ set gs" by (auto elim!: mset_factorsE) from x1 have "x \ 1" by auto note FG[folded factors_as_mset_factors[OF x0 this]] from factors_unique[OF this, simplified, OF x0 x1, folded fsgs] 0 show "rel_mset (ddvd) F G" by auto qed subsection \Preservation of Irreducibility\ locale comm_semiring_1_hom = comm_monoid_mult_hom hom + zero_hom hom for hom :: "'a :: comm_semiring_1 \ 'b :: comm_semiring_1" locale irreducibility_hom = comm_semiring_1_hom + assumes irreducible_imp_irreducible_hom: "irreducible a \ irreducible (hom a)" begin lemma hom_mset_factors: assumes F: "mset_factors F p" shows "mset_factors (image_mset hom F) (hom p)" proof (unfold mset_factors_def, intro conjI allI impI) from F show "hom p = prod_mset (image_mset hom F)" "image_mset hom F \ {#}" by (auto simp: hom_distribs) fix f' assume "f' \# image_mset hom F" then obtain f where f: "f \# F" and f'f: "f' = hom f" by auto with F irreducible_imp_irreducible_hom show "irreducible f'" unfolding f'f by auto qed end locale unit_preserving_hom = comm_semiring_1_hom + assumes is_unit_hom_if: "\x. hom x dvd 1 \ x dvd 1" begin lemma is_unit_hom_iff[simp]: "hom x dvd 1 \ x dvd 1" using is_unit_hom_if hom_dvd by force lemma irreducible_hom_imp_irreducible: assumes irr: "irreducible (hom a)" shows "irreducible a" proof (intro irreducibleI) from irr show "a \ 0" by auto from irr show "\ a dvd 1" by (auto dest: irreducible_not_unit) fix b c assume "a = b * c" then have "hom a = hom b * hom c" by (simp add: hom_distribs) with irr have "hom b dvd 1 \ hom c dvd 1" by (auto dest: irreducibleD) then show "b dvd 1 \ c dvd 1" by simp qed end locale factor_preserving_hom = unit_preserving_hom + irreducibility_hom begin lemma irreducible_hom[simp]: "irreducible (hom a) \ irreducible a" using irreducible_hom_imp_irreducible irreducible_imp_irreducible_hom by metis end lemma factor_preserving_hom_comp: assumes f: "factor_preserving_hom f" and g: "factor_preserving_hom g" shows "factor_preserving_hom (f o g)" proof- interpret f: factor_preserving_hom f by (rule f) interpret g: factor_preserving_hom g by (rule g) show ?thesis by (unfold_locales, auto simp: hom_distribs) qed context comm_semiring_isom begin sublocale unit_preserving_hom by (unfold_locales, auto) sublocale factor_preserving_hom proof (standard) fix a :: 'a assume "irreducible a" note a = this[unfolded irreducible_def] show "irreducible (hom a)" proof (rule ccontr) assume "\ irreducible (hom a)" from this[unfolded Factorial_Ring.irreducible_def,simplified] a obtain hb hc where eq: "hom a = hb * hc" and nu: "\ hb dvd 1" "\ hc dvd 1" by auto from bij obtain b where hb: "hb = hom b" by (elim bij_pointE) from bij obtain c where hc: "hc = hom c" by (elim bij_pointE) from eq[unfolded hb hc, folded hom_mult] have "a = b * c" by auto with nu hb hc have "a = b * c" "\ b dvd 1" "\ c dvd 1" by auto with a show False by auto qed qed end subsubsection\Back to divisibility\ lemma(in comm_semiring_1) mset_factors_mult: assumes F: "mset_factors F a" and G: "mset_factors G b" shows "mset_factors (F+G) (a*b)" proof(intro mset_factorsI) fix f assume "f \# F + G" then consider "f \# F" | "f \# G" by auto then show "irreducible f" by(cases, insert F G, auto) qed (insert F G, auto) lemma(in ufd) dvd_imp_subset_factors: assumes ab: "a dvd b" and F: "mset_factors F a" and G: "mset_factors G b" shows "\G'. G' \# G \ rel_mset (ddvd) F G'" proof- from F G have a0: "a \ 0" and b0: "b \ 0" by (simp_all add: mset_factors_imp_nonzero) from ab obtain c where c: "b = a * c" by (elim dvdE, auto) with b0 have c0: "c \ 0" by auto show ?thesis proof(cases "c dvd 1") case True show ?thesis proof(cases F) case empty with F show ?thesis by auto next case (add f F') with F have a: "f * prod_mset F' = a" and F': "\f. f \# F' \ irreducible f" and irrf: "irreducible f" by auto from irrf have f0: "f \ 0" and f1: "\f dvd 1" by (auto dest: irreducible_not_unit) from a c have "(f * c) * prod_mset F' = b" by (auto simp: ac_simps) moreover { have "irreducible (f * c)" using True irrf by (subst irreducible_mult_unit_right) with F' irrf have "\f'. f' \# F' + {#f * c#} \ irreducible f'" by auto } ultimately have "mset_factors (F' + {#f * c#}) b" by (intro mset_factorsI, auto) from mset_factors_unique[OF this G] have F'G: "rel_mset (ddvd) (F' + {#f * c#}) G". from True add have FF': "rel_mset (ddvd) F (F' + {#f * c#})" by (auto simp add: multiset.rel_refl intro!: rel_mset_Plus) have "rel_mset (ddvd) F G" apply(rule transpD[OF multiset.rel_transp[OF transpI] FF' F'G]) using ddvd_trans. then show ?thesis by auto qed next case False from mset_factors_exist[OF c0 this] obtain H where H: "mset_factors H c" by auto from c mset_factors_mult[OF F H] have "mset_factors (F + H) b" by auto note mset_factors_unique[OF this G] from rel_mset_split[OF this] obtain G1 G2 where "G = G1 + G2" "rel_mset (ddvd) F G1" "rel_mset (ddvd) H G2" by auto then show ?thesis by (intro exI[of _ "G1"], auto) qed qed lemma(in idom) irreducible_factor_singleton: assumes a: "irreducible a" shows "mset_factors F a \ F = {#a#}" proof(cases F) case empty with mset_factorsD show ?thesis by auto next case (add f F') show ?thesis proof assume F: "mset_factors F a" from add mset_factorsD[OF F] have *: "a = f * prod_mset F'" by auto then have fa: "f dvd a" by auto from * a have f0: "f \ 0" by auto from add have "f \# F" by auto with F have f: "irreducible f" by auto from add have "F' \# F" by auto then have unitemp: "prod_mset F' dvd 1 \ F' = {#}" proof(induct F') case empty then show ?case by auto next case (add f F') from add have "f \# F" by (simp add: mset_subset_eq_insertD) with F irreducible_not_unit have "\ f dvd 1" by auto then have "\ (prod_mset F' * f) dvd 1" by simp with add show ?case by auto qed show "F = {#a#}" proof(cases "a dvd f") case True then obtain r where "f = a * r" by (elim dvdE, auto) with * have "f = (r * prod_mset F') * f" by (auto simp: ac_simps) with f0 have "r * prod_mset F' = 1" by auto then have "prod_mset F' dvd 1" by (metis dvd_triv_right) with unitemp * add show ?thesis by auto next case False with fa a f show ?thesis by (auto simp: irreducible_altdef) qed qed (insert a, auto) qed lemma(in ufd) irreducible_dvd_imp_factor: assumes ab: "a dvd b" and a: "irreducible a" and G: "mset_factors G b" shows "\g \# G. a ddvd g" proof- from a have "mset_factors {#a#} a" by auto from dvd_imp_subset_factors[OF ab this G] obtain G' where G'G: "G' \# G" and rel: "rel_mset (ddvd) {#a#} G'" by auto with rel_mset_size size_1_singleton_mset size_single obtain g where gG': "G' = {#g#}" by fastforce from rel[unfolded this rel_mset_def] have "a ddvd g" by auto with gG' G'G show ?thesis by auto qed lemma(in idom) prod_mset_remove_units: "prod_mset F ddvd prod_mset {# f \# F. \f dvd 1 #}" proof(induct F) case (add f F) then show ?case by (cases "f = 0", auto) qed auto lemma(in comm_semiring_1) mset_factors_imp_dvd: assumes "mset_factors F x" and "f \# F" shows "f dvd x" using assms by (simp add: dvd_prod_mset mset_factors_def) lemma(in ufd) prime_elem_iff_irreducible[iff]: "prime_elem x \ irreducible x" proof (intro iffI, fact prime_elem_imp_irreducible, rule prime_elemI) assume r: "irreducible x" then show x0: "x \ 0" and x1: "\ x dvd 1" by (auto dest: irreducible_not_unit) from irreducible_factor_singleton[OF r] have *: "mset_factors {#x#} x" by auto fix a b assume "x dvd a * b" then obtain c where abxc: "a * b = x * c" by (elim dvdE, auto) show "x dvd a \ x dvd b" proof(cases "c = 0 \ a = 0 \ b = 0") case True with abxc show ?thesis by auto next case False then have a0: "a \ 0" and b0: "b \ 0" and c0: "c \ 0" by auto from x0 c0 have xc0: "x * c \ 0" by auto from x1 have xc1: "\ x * c dvd 1" by auto show ?thesis proof (cases "a dvd 1 \ b dvd 1") case False then have a1: "\ a dvd 1" and b1: "\ b dvd 1" by auto from mset_factors_exist[OF a0 a1] obtain F where Fa: "mset_factors F a" by auto then have F0: "F \ {#}" by auto from mset_factors_exist[OF b0 b1] obtain G where Gb: "mset_factors G b" by auto then have G0: "G \ {#}" by auto from mset_factors_mult[OF Fa Gb] have FGxc: "mset_factors (F + G) (x * c)" by (simp add: abxc) show ?thesis proof (cases "c dvd 1") case True from r irreducible_mult_unit_right[OF this] have "irreducible (x*c)" by simp note irreducible_factor_singleton[OF this] FGxc with F0 G0 have False by (cases F; cases G; auto) then show ?thesis by auto next case False from mset_factors_exist[OF c0 this] obtain H where "mset_factors H c" by auto with * have xHxc: "mset_factors (add_mset x H) (x * c)" by force note rel = mset_factors_unique[OF this FGxc] obtain hs where "mset hs = H" using ex_mset by auto then have "mset (x#hs) = add_mset x H" by auto from rel_mset_free[OF rel this] obtain jjs where jjsGH: "mset jjs = F + G" and rel: "list_all2 (ddvd) (x # hs) jjs" by auto then obtain j js where jjs: "jjs = j # js" by (cases jjs, auto) with rel have xj: "x ddvd j" by auto from jjs jjsGH have j: "j \ set_mset (F + G)" by (intro union_single_eq_member, auto) from j consider "j \# F" | "j \# G" by auto then show ?thesis proof(cases) case 1 with Fa have "j dvd a" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd a" by auto then show ?thesis by auto next case 2 with Gb have "j dvd b" by (auto intro: mset_factors_imp_dvd) with xj dvd_trans have "x dvd b" by auto then show ?thesis by auto qed qed next case True then consider "a dvd 1" | "b dvd 1" by auto then show ?thesis proof(cases) case 1 then obtain d where ad: "a * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = a * d * b" by (auto simp: ac_simps) finally have "x dvd b" by (intro dvdI, auto simp: ad) then show ?thesis by auto next case 2 then obtain d where bd: "b * d = 1" by (elim dvdE, auto) from abxc have "x * (c * d) = a * b * d" by (auto simp: ac_simps) also have "... = (b * d) * a" by (auto simp: ac_simps) finally have "x dvd a" by (intro dvdI, auto simp:bd) then show ?thesis by auto qed qed qed qed subsection\Results for GCDs etc.\ lemma prod_list_remove1: "(x :: 'b :: comm_monoid_mult) \ set xs \ prod_list (remove1 x xs) * x = prod_list xs" by (induct xs, auto simp: ac_simps) (* Isabelle 2015-style and generalized gcd-class without normalization and factors *) class comm_monoid_gcd = gcd + comm_semiring_1 + assumes gcd_dvd1[iff]: "gcd a b dvd a" and gcd_dvd2[iff]: "gcd a b dvd b" and gcd_greatest: "c dvd a \ c dvd b \ c dvd gcd a b" begin lemma gcd_0_0[simp]: "gcd 0 0 = 0" using gcd_greatest[OF dvd_0_right dvd_0_right, of 0] by auto lemma gcd_zero_iff[simp]: "gcd a b = 0 \ a = 0 \ b = 0" proof assume "gcd a b = 0" from gcd_dvd1[of a b, unfolded this] gcd_dvd2[of a b, unfolded this] show "a = 0 \ b = 0" by auto qed auto lemma gcd_zero_iff'[simp]: "0 = gcd a b \ a = 0 \ b = 0" using gcd_zero_iff by metis lemma dvd_gcd_0_iff[simp]: shows "x dvd gcd 0 a \ x dvd a" (is ?g1) and "x dvd gcd a 0 \ x dvd a" (is ?g2) proof- have "a dvd gcd a 0" "a dvd gcd 0 a" by (auto intro: gcd_greatest) with dvd_refl show ?g1 ?g2 by (auto dest: dvd_trans) qed lemma gcd_dvd_1[simp]: "gcd a b dvd 1 \ coprime a b" using dvd_trans[OF gcd_greatest[of _ a b], of _ 1] by (cases "a = 0 \ b = 0") (auto intro!: coprimeI elim: coprimeE) lemma dvd_imp_gcd_dvd_gcd: "b dvd c \ gcd a b dvd gcd a c" by (meson gcd_dvd1 gcd_dvd2 gcd_greatest dvd_trans) definition listgcd :: "'a list \ 'a" where "listgcd xs = foldr gcd xs 0" lemma listgcd_simps[simp]: "listgcd [] = 0" "listgcd (x # xs) = gcd x (listgcd xs)" by (auto simp: listgcd_def) lemma listgcd: "x \ set xs \ listgcd xs dvd x" proof (induct xs) case (Cons y ys) show ?case proof (cases "x = y") case False with Cons have dvd: "listgcd ys dvd x" by auto thus ?thesis unfolding listgcd_simps using dvd_trans by blast next case True thus ?thesis unfolding listgcd_simps using dvd_trans by blast qed qed simp lemma listgcd_greatest: "(\ x. x \ set xs \ y dvd x) \ y dvd listgcd xs" by (induct xs arbitrary:y, auto intro: gcd_greatest) end context Rings.dvd begin definition "is_gcd x a b \ x dvd a \ x dvd b \ (\y. y dvd a \ y dvd b \ y dvd x)" definition "some_gcd a b \ SOME x. is_gcd x a b" lemma is_gcdI[intro!]: assumes "x dvd a" "x dvd b" "\y. y dvd a \ y dvd b \ y dvd x" shows "is_gcd x a b" by (insert assms, auto simp: is_gcd_def) lemma is_gcdE[elim!]: assumes "is_gcd x a b" and "x dvd a \ x dvd b \ (\y. y dvd a \ y dvd b \ y dvd x) \ thesis" shows thesis by (insert assms, auto simp: is_gcd_def) lemma is_gcd_some_gcdI: assumes "\x. is_gcd x a b" shows "is_gcd (some_gcd a b) a b" by (unfold some_gcd_def, rule someI_ex[OF assms]) end context comm_semiring_1 begin lemma some_gcd_0[intro!]: "is_gcd (some_gcd a 0) a 0" "is_gcd (some_gcd 0 b) 0 b" by (auto intro!: is_gcd_some_gcdI intro: exI[of _ a] exI[of _ b]) lemma some_gcd_0_dvd[intro!]: "some_gcd a 0 dvd a" "some_gcd 0 b dvd b" using some_gcd_0 by auto lemma dvd_some_gcd_0[intro!]: "a dvd some_gcd a 0" "b dvd some_gcd 0 b" using some_gcd_0[of a] some_gcd_0[of b] by auto end context idom begin lemma is_gcd_connect: assumes "a \ 0" "b \ 0" shows "isgcd mk_monoid x a b \ is_gcd x a b" using assms by (force simp: isgcd_def) lemma some_gcd_connect: assumes "a \ 0" and "b \ 0" shows "somegcd mk_monoid a b = some_gcd a b" using assms by (auto intro!: arg_cong[of _ _ Eps] simp: is_gcd_connect some_gcd_def somegcd_def) end context comm_monoid_gcd begin lemma is_gcd_gcd: "is_gcd (gcd a b) a b" using gcd_greatest by auto lemma is_gcd_some_gcd: "is_gcd (some_gcd a b) a b" by (insert is_gcd_gcd, auto intro!: is_gcd_some_gcdI) lemma gcd_dvd_some_gcd: "gcd a b dvd some_gcd a b" using is_gcd_some_gcd by auto lemma some_gcd_dvd_gcd: "some_gcd a b dvd gcd a b" using is_gcd_some_gcd by (auto intro: gcd_greatest) lemma some_gcd_ddvd_gcd: "some_gcd a b ddvd gcd a b" by (auto intro: gcd_dvd_some_gcd some_gcd_dvd_gcd) lemma some_gcd_dvd: "some_gcd a b dvd d \ gcd a b dvd d" "d dvd some_gcd a b \ d dvd gcd a b" using some_gcd_ddvd_gcd[of a b] by (auto dest:dvd_trans) end class idom_gcd = comm_monoid_gcd + idom begin interpretation raw: comm_monoid_cancel "mk_monoid :: 'a monoid" by (unfold_locales, auto intro: mult_commute mult_assoc) interpretation raw: gcd_condition_monoid "mk_monoid :: 'a monoid" by (unfold_locales, auto simp: is_gcd_connect intro!: exI[of _ "gcd _ _"] dest: gcd_greatest) lemma gcd_mult_ddvd: "d * gcd a b ddvd gcd (d * a) (d * b)" proof (cases "d = 0") case True then show ?thesis by auto next case d0: False show ?thesis proof (cases "a = 0 \ b = 0") case False note some_gcd_ddvd_gcd[of a b] with d0 have "d * gcd a b ddvd d * some_gcd a b" by auto also have "d * some_gcd a b ddvd some_gcd (d * a) (d * b)" using False d0 raw.gcd_mult by (simp add: some_gcd_connect) also note some_gcd_ddvd_gcd finally show ?thesis. next case True with d0 show ?thesis apply (elim disjE) apply (rule ddvd_trans[of _ "d * b"]; force) apply (rule ddvd_trans[of _ "d * a"]; force) done qed qed lemma gcd_greatest_mult: assumes cad: "c dvd a * d" and cbd: "c dvd b * d" shows "c dvd gcd a b * d" proof- from gcd_greatest[OF assms] have c: "c dvd gcd (d * a) (d * b)" by (auto simp: ac_simps) note gcd_mult_ddvd[of d a b] then have "gcd (d * a) (d * b) dvd gcd a b * d" by (auto simp: ac_simps) from dvd_trans[OF c this] show ?thesis . qed lemma listgcd_greatest_mult: "(\ x :: 'a. x \ set xs \ y dvd x * z) \ y dvd listgcd xs * z" proof (induct xs) case (Cons x xs) from Cons have "y dvd x * z" "y dvd listgcd xs * z" by auto thus ?case unfolding listgcd_simps by (rule gcd_greatest_mult) qed (simp) lemma dvd_factor_mult_gcd: assumes dvd: "k dvd p * q" "k dvd p * r" and q0: "q \ 0" and r0: "r \ 0" shows "k dvd p * gcd q r" proof - from dvd gcd_greatest[of k "p * q" "p * r"] have "k dvd gcd (p * q) (p * r)" by simp also from gcd_mult_ddvd[of p q r] have "... dvd (p * gcd q r)" by auto finally show ?thesis . qed lemma coprime_mult_cross_dvd: assumes coprime: "coprime p q" and eq: "p' * p = q' * q" shows "p dvd q'" (is ?g1) and "q dvd p'" (is ?g2) proof (atomize(full), cases "p = 0 \ q = 0") case True then show "?g1 \ ?g2" proof assume p0: "p = 0" with coprime have "q dvd 1" by auto with eq p0 show ?thesis by auto next assume q0: "q = 0" with coprime have "p dvd 1" by auto with eq q0 show ?thesis by auto qed next case False { fix p q r p' q' :: 'a assume cop: "coprime p q" and eq: "p' * p = q' * q" and p: "p \ 0" and q: "q \ 0" and r: "r dvd p" "r dvd q" let ?gcd = "gcd q p" from eq have "p' * p dvd q' * q" by auto hence d1: "p dvd q' * q" by (rule dvd_mult_right) have d2: "p dvd q' * p" by auto from dvd_factor_mult_gcd[OF d1 d2 q p] have 1: "p dvd q' * ?gcd" . from q p have 2: "?gcd dvd q" by auto from q p have 3: "?gcd dvd p" by auto from cop[unfolded coprime_def', rule_format, OF 3 2] have "?gcd dvd 1" . from 1 dvd_mult_unit_iff[OF this] have "p dvd q'" by auto } note main = this from main[OF coprime eq,of 1] False coprime coprime_commute main[OF _ eq[symmetric], of 1] show "?g1 \ ?g2" by auto qed end subclass (in ring_gcd) idom_gcd by (unfold_locales, auto) lemma coprime_rewrites: "comm_monoid_mult.coprime ((*)) 1 = coprime" apply (intro ext) apply (subst comm_monoid_mult.coprime_def') apply (unfold_locales) apply (unfold dvd_rewrites) apply (fold coprime_def') .. (* TODO: incorporate into the default class hierarchy *) locale gcd_condition = fixes ty :: "'a :: idom itself" assumes gcd_exists: "\a b :: 'a. \x. is_gcd x a b" begin sublocale idom_gcd "(*)" "1 :: 'a" "(+)" 0 "(-)" uminus some_gcd rewrites "dvd.dvd ((*)) = (dvd)" and "comm_monoid_mult.coprime ((*) ) 1 = Unique_Factorization.coprime" proof- have "is_gcd (some_gcd a b) a b" for a b :: 'a by (intro is_gcd_some_gcdI gcd_exists) from this[unfolded is_gcd_def] show "class.idom_gcd (*) (1 :: 'a) (+) 0 (-) uminus some_gcd" by (unfold_locales, auto simp: dvd_rewrites) qed (simp_all add: dvd_rewrites coprime_rewrites) end instance semiring_gcd \ comm_monoid_gcd by (intro_classes, auto) lemma listgcd_connect: "listgcd = gcd_list" proof (intro ext) fix xs :: "'a list" show "listgcd xs = gcd_list xs" by(induct xs, auto) qed interpretation some_gcd: gcd_condition "TYPE('a::ufd)" proof(unfold_locales, intro exI) interpret factorial_monoid "mk_monoid :: 'a monoid" by (fact factorial_monoid) note d = dvd.dvd_def some_gcd_def carrier_0 fix a b :: 'a show "is_gcd (some_gcd a b) a b" proof (cases "a = 0 \ b = 0") case True thus ?thesis using some_gcd_0 by auto next case False with gcdof_exists[of a b] show ?thesis by (auto intro!: is_gcd_some_gcdI simp add: is_gcd_connect some_gcd_connect) qed qed lemma some_gcd_listgcd_dvd_listgcd: "some_gcd.listgcd xs dvd listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) lemma listgcd_dvd_some_gcd_listgcd: "listgcd xs dvd some_gcd.listgcd xs" by (induct xs, auto simp:some_gcd_dvd intro:dvd_imp_gcd_dvd_gcd) context factorial_ring_gcd begin text \Do not declare the following as subclass, to avoid conflict in \field \ gcd_condition\ vs. \factorial_ring_gcd \ gcd_condition\. \ sublocale as_ufd: ufd proof(unfold_locales, goal_cases) case (1 x) from prime_factorization_exists[OF \x \ 0\] obtain F where f: "\f. f \# F \ prime_elem f" and Fx: "normalize (prod_mset F) = normalize x" by auto from associatedE2[OF Fx] obtain u where u: "is_unit u" "x = u * prod_mset F" by blast from \\ is_unit x\ Fx have "F \ {#}" by auto then obtain g G where F: "F = add_mset g G" by (cases F, auto) then have "g \# F" by auto with f[OF this]prime_elem_iff_irreducible irreducible_mult_unit_left[OF unit_factor_is_unit[OF \x \ 0\]] have g: "irreducible (u * g)" using u(1) by (subst irreducible_mult_unit_left) simp_all show ?case proof (intro exI conjI mset_factorsI) show "prod_mset (add_mset (u * g) G) = x" using \x \ 0\ by (simp add: F ac_simps u) fix f assume "f \# add_mset (u * g) G" with f[unfolded F] g prime_elem_iff_irreducible show "irreducible f" by auto qed auto next case (2 x F G) note transpD[OF multiset.rel_transp[OF ddvd_transp],trans] obtain fs where F: "F = mset fs" by (metis ex_mset) have "list_all2 (ddvd) fs (map normalize fs)" by (intro list_all2_all_nthI, auto) then have FH: "rel_mset (ddvd) F (image_mset normalize F)" by (unfold rel_mset_def F, force) also have FG: "image_mset normalize F = image_mset normalize G" proof (intro prime_factorization_unique'') from 2 have xF: "x = prod_mset F" and xG: "x = prod_mset G" by auto from xF have "normalize x = normalize (prod_mset (image_mset normalize F))" by (simp add: normalize_prod_mset_normalize) with xG have nFG: "\ = normalize (prod_mset (image_mset normalize G))" by (simp_all add: normalize_prod_mset_normalize) then show "normalize (\i\#image_mset normalize F. i) = normalize (\i\#image_mset normalize G. i)" by auto next from 2 prime_elem_iff_irreducible have "f \# F \ prime_elem f" "g \# G \ prime_elem g" for f g by (auto intro: prime_elemI) then show " Multiset.Ball (image_mset normalize F) prime" "Multiset.Ball (image_mset normalize G) prime" by auto qed also obtain gs where G: "G = mset gs" by (metis ex_mset) have "list_all2 ((ddvd)\\) gs (map normalize gs)" by (intro list_all2_all_nthI, auto) then have "rel_mset (ddvd) (image_mset normalize G) G" by (subst multiset.rel_flip[symmetric], unfold rel_mset_def G, force) finally show ?case. qed end instance int :: ufd by (intro ufd.intro_of_class as_ufd.ufd_axioms) instance int :: idom_gcd by (intro_classes, auto) instance field \ ufd by (intro_classes, auto simp: dvd_field_iff) end diff --git a/thys/Polynomial_Factorization/Polynomial_Divisibility.thy b/thys/Polynomial_Factorization/Polynomial_Divisibility.thy deleted file mode 100644 --- a/thys/Polynomial_Factorization/Polynomial_Divisibility.thy +++ /dev/null @@ -1,67 +0,0 @@ -(* - Author: René Thiemann - Akihisa Yamada - License: BSD -*) -section \Polynomial Divisibility\ - -text \We make a connection between irreducibility of Missing-Polynomial and Factorial-Ring.\ - - -theory Polynomial_Divisibility -imports - Polynomial_Interpolation.Missing_Polynomial -begin - -lemma dvd_gcd_mult: fixes p :: "'a :: semiring_gcd" - assumes dvd: "k dvd p * q" "k dvd p * r" - shows "k dvd p * gcd q r" - by (rule dvd_trans, rule gcd_greatest[OF dvd]) - (auto intro!: mult_dvd_mono simp: gcd_mult_left) - -lemma poly_gcd_monic_factor: - "monic p \ gcd (p * q) (p * r) = p * gcd q r" - by (rule gcdI [symmetric]) (simp_all add: normalize_mult normalize_monic dvd_gcd_mult) - -context - assumes "SORT_CONSTRAINT('a :: field)" -begin - -lemma field_poly_irreducible_dvd_mult[simp]: - assumes irr: "irreducible (p :: 'a poly)" - shows "p dvd q * r \ p dvd q \ p dvd r" - using field_poly_irreducible_imp_prime[OF irr] by (simp add: prime_elem_dvd_mult_iff) - -lemma irreducible_dvd_pow: - fixes p :: "'a poly" - assumes irr: "irreducible p" - shows "p dvd q ^ n \ p dvd q" - using field_poly_irreducible_imp_prime[OF irr] by (rule prime_elem_dvd_power) - -lemma irreducible_dvd_prod: fixes p :: "'a poly" - assumes irr: "irreducible p" - and dvd: "p dvd prod f as" - shows "\ a \ as. p dvd f a" - by (insert dvd, induct as rule: infinite_finite_induct, insert irr, auto) - -lemma irreducible_dvd_prod_list: fixes p :: "'a poly" - assumes irr: "irreducible p" - and dvd: "p dvd prod_list as" - shows "\ a \ set as. p dvd a" - by (insert dvd, induct as, insert irr, auto) - - -lemma dvd_mult_imp_degree: fixes p :: "'a poly" - assumes "p dvd q * r" - and "degree p > 0" -shows "\ s t. irreducible s \ p = s * t \ (s dvd q \ s dvd r)" -proof - - from irreducible\<^sub>d_factor[OF assms(2)] obtain s t - where irred: "irreducible s" and p: "p = s * t" by auto - from \p dvd q * r\ p have s: "s dvd q * r" unfolding dvd_def by auto - from s p irred show ?thesis by auto -qed - -end - -end diff --git a/thys/Polynomial_Factorization/Polynomial_Irreducibility.thy b/thys/Polynomial_Factorization/Polynomial_Irreducibility.thy new file mode 100644 --- /dev/null +++ b/thys/Polynomial_Factorization/Polynomial_Irreducibility.thy @@ -0,0 +1,67 @@ +(* + Author: René Thiemann + Akihisa Yamada + License: BSD +*) +section \Polynomial Divisibility\ + +text \We make a connection between irreducibility of Missing-Polynomial and Factorial-Ring.\ + + +theory Polynomial_Irreducibility +imports + Polynomial_Interpolation.Missing_Polynomial +begin + +lemma dvd_gcd_mult: fixes p :: "'a :: semiring_gcd" + assumes dvd: "k dvd p * q" "k dvd p * r" + shows "k dvd p * gcd q r" + by (rule dvd_trans, rule gcd_greatest[OF dvd]) + (auto intro!: mult_dvd_mono simp: gcd_mult_left) + +lemma poly_gcd_monic_factor: + "monic p \ gcd (p * q) (p * r) = p * gcd q r" + by (rule gcdI [symmetric]) (simp_all add: normalize_mult normalize_monic dvd_gcd_mult) + +context + assumes "SORT_CONSTRAINT('a :: field)" +begin + +lemma field_poly_irreducible_dvd_mult[simp]: + assumes irr: "irreducible (p :: 'a poly)" + shows "p dvd q * r \ p dvd q \ p dvd r" + using field_poly_irreducible_imp_prime[OF irr] by (simp add: prime_elem_dvd_mult_iff) + +lemma irreducible_dvd_pow: + fixes p :: "'a poly" + assumes irr: "irreducible p" + shows "p dvd q ^ n \ p dvd q" + using field_poly_irreducible_imp_prime[OF irr] by (rule prime_elem_dvd_power) + +lemma irreducible_dvd_prod: fixes p :: "'a poly" + assumes irr: "irreducible p" + and dvd: "p dvd prod f as" + shows "\ a \ as. p dvd f a" + by (insert dvd, induct as rule: infinite_finite_induct, insert irr, auto) + +lemma irreducible_dvd_prod_list: fixes p :: "'a poly" + assumes irr: "irreducible p" + and dvd: "p dvd prod_list as" + shows "\ a \ set as. p dvd a" + by (insert dvd, induct as, insert irr, auto) + + +lemma dvd_mult_imp_degree: fixes p :: "'a poly" + assumes "p dvd q * r" + and "degree p > 0" +shows "\ s t. irreducible s \ p = s * t \ (s dvd q \ s dvd r)" +proof - + from irreducible\<^sub>d_factor[OF assms(2)] obtain s t + where irred: "irreducible s" and p: "p = s * t" by auto + from \p dvd q * r\ p have s: "s dvd q * r" unfolding dvd_def by auto + from s p irred show ?thesis by auto +qed + +end + +end diff --git a/thys/Polynomial_Factorization/Square_Free_Factorization.thy b/thys/Polynomial_Factorization/Square_Free_Factorization.thy --- a/thys/Polynomial_Factorization/Square_Free_Factorization.thy +++ b/thys/Polynomial_Factorization/Square_Free_Factorization.thy @@ -1,1451 +1,1451 @@ (* 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_Divisibility + 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\<^sub>d_square_free: fixes p :: "'a :: {comm_semiring_1, semiring_no_zero_divisors} poly" shows "irreducible\<^sub>d p \ square_free p" by (metis degree_0 degree_mult_eq degree_mult_eq_0 irreducible\<^sub>dD(1) irreducible\<^sub>dD(2) irreducible\<^sub>d_dvd_smult irreducible\<^sub>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\<^sub>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\<^sub>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 ^ Suc i)) \ (p = 0 \ c = 0 \ bs = []) \ (\ a i. (a,i) \ set bs \ square_free a \ degree a > 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 ^ Suc i)" "(a,i) \ set bs \ square_free a \ degree a \ 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 ^ Suc 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,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\<^sub>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\<^sub>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\<^sub>d_def] have p0: "degree p > 0" by auto from irreducible\<^sub>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\<^sub>d b" by auto from irreducible\<^sub>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.. 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..(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.. (\(b, j)\as - UNIV \ {0.. = 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..(a, i)\as \ UNIV \ {n}. a) * (case x of (a, i) \ (\(b, j)\as - UNIV \ {0..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.. ?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\<^sub>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\<^sub>d_dvd_smult[OF q0 as_irred[OF ai] qa] irreducible\<^sub>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\<^sub>d a" by (rule as_irred[OF ai]) from irreducible\<^sub>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\<^sub>d b" . from irreducible\<^sub>d_dvd_smult[OF _ b ab] a[unfolded irreducible\<^sub>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.. 0" by (rule nonzero_gen, auto) have "irreducible\<^sub>d a" using as_irred[OF ai] . hence a: "a \ 0" "degree a \ 0" unfolding irreducible\<^sub>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.. = 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, i) | i. i < n}" "distinct (map snd bs)" shows "\ m. set cs = {(A i, 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, 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, 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, n) # bs) = {(A i, 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, 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, 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] show ?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, 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.. = 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 ^ Suc i)" unfolding bs by (rule prod.reindex_cong[of snd], auto simp: inj_on_def, force) finally have 1: "p = (\(a, i)\ set bs. a ^ Suc i)" . { fix a i assume "(a,i) \ set bs" hence A: "a = A i" "A i \ 1" unfolding bs by auto with A_square_free[of i] A_monic[of i] have "square_free a \ degree a \ 0" "monic a" 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)" hence a: "a = A i" and b: "b = A j" unfolding bs by auto from neq dist ai bj have neq: "i \ j" using a b 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\<^sub>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\<^sub>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 ^ Suc 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 ^ Suc 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_suc: "(\x\bs. (x :: 'a :: comm_monoid_mult) * x ^ i) = prod_list bs * 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 = Suc i" proof - note sff = square_free_factorizationD[OF sff] let ?prod = "(\(a, i)\set bs. a ^ Suc 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 ^ Suc i)" have p0: "?prod \ 0" using p pf by auto have "?prod = a ^ Suc i * ?rem" by (subst prod.remove[OF _ ai], auto) also have "a ^ Suc i = q ^ Suc i * b ^ Suc i" unfolding aqb by (simp add: field_simps) finally have id: "?prod = q ^ Suc i * (b ^ Suc i * ?rem)" by simp hence dvd: "q ^ Suc i dvd ?prod" by auto { assume "q ^ Suc (Suc i) dvd ?prod" hence "q dvd ?prod div q ^ Suc i" by (metis dvd dvd_0_left_iff dvd_div_iff_mult p0 power_Suc) also have "?prod div q ^ Suc i = b ^ Suc 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\<^sub>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 ^ Suc 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 (Suc i) dvd ?prod" by blast with dvd have "order x ?prod = Suc 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 ^ Suc 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 = Suc 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 = Suc 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 = 0} = {x. \ a i. (a,i) \ set bs \ poly a x = 0}" using square_free_factorization_order_root[OF sff p] p unfolding order_root by auto lemma square_free_factorizationD': fixes p :: "'a poly" assumes sf: "square_free_factorization p (c, bs)" shows "p = smult c (\(a, i) \ bs. a ^ Suc i)" and "square_free (prod_list (map fst bs))" and "\ b i. (b,i) \ set bs \ degree b \ 0" and "p = 0 \ c = 0 \ bs = []" proof - note sf = square_free_factorizationD[OF sf] show "p = smult c (\(a, i) \ bs. a ^ Suc i)" unfolding sf(1) using sf(5) by (simp add: prod.distinct_set_conv_list) show bs: "\ b i. (b,i) \ set bs \ degree b \ 0" using sf(2) by auto show "p = 0 \ c = 0 \ bs = []" using sf(4) . show "square_free (prod_list (map fst bs))" proof (rule square_freeI) from bs have "\ b. b \ set (map fst bs) \ b \ 0" by fastforce thus "prod_list (map fst bs) \ 0" unfolding prod_list_zero_iff by auto fix q assume "degree q > 0" "q * q dvd prod_list (map fst bs)" from irreducible\<^sub>d_factor[OF this(1)] this(2) obtain q where irr: "irreducible q" and dvd: "q * q dvd prod_list (map fst bs)" unfolding dvd_def by auto hence dvd': "q dvd prod_list (map fst bs)" unfolding dvd_def by auto from irreducible_dvd_prod_list[OF irr dvd'] obtain b i where mem: "(b,i) \ set bs" and dvd1: "q dvd b" by auto from dvd1 obtain k where b: "b = q * k" unfolding dvd_def by auto from split_list[OF mem] b obtain bs1 bs2 where bs: "bs = bs1 @ (b, i) # bs2" by auto from irr have q0: "q \ 0" and dq: "degree q > 0" unfolding irreducible\<^sub>d_def by auto from sf(2)[OF mem, unfolded b] have "square_free (q * k)" by auto from this[unfolded square_free_def, THEN conjunct2, rule_format, OF dq] have qk: "\ q dvd k" by simp from dvd[unfolded bs b] have "q * q dvd q * (k * prod_list (map fst (bs1 @ bs2)))" by (auto simp: ac_simps) with q0 have "q dvd k * prod_list (map fst (bs1 @ bs2))" by auto with irr qk have "q dvd prod_list (map fst (bs1 @ bs2))" by auto from irreducible_dvd_prod_list[OF irr this] obtain b' i' where mem': "(b',i') \ set (bs1 @ bs2)" and dvd2: "q dvd b'" by fastforce from dvd1 dvd2 have "q dvd gcd b b'" by auto with dq is_unit_iff_degree[OF q0] have cop: "\ coprime b b'" by force from mem' have "(b',i') \ set bs" unfolding bs by auto from sf(3)[OF mem this] cop have b': "(b',i') = (b,i)" by (auto simp add: coprime_iff_gcd_eq_1) with mem' sf(5)[unfolded bs] show False by auto qed qed lemma square_free_factorizationI': fixes p :: "'a poly" assumes prod: "p = smult c (\(a, i) \ bs. a ^ Suc i)" and sf: "square_free (prod_list (map fst bs))" and deg: "\ b i. (b,i) \ set bs \ degree b > 0" and 0: "p = 0 \ c = 0 \ bs = []" shows "square_free_factorization p (c, bs)" unfolding square_free_factorization_def split proof (intro conjI impI allI) show "p = 0 \ c = 0" "p = 0 \ bs = []" using 0 by auto { fix b i assume bi: "(b,i) \ set bs" from deg[OF this] show "degree b > 0" . have "b dvd prod_list (map fst bs)" by (intro prod_list_dvd, insert bi, force) from square_free_factor[OF this sf] show "square_free b" . } show dist: "distinct bs" proof (rule ccontr) assume "\ ?thesis" from not_distinct_decomp[OF this] obtain bs1 bs2 bs3 b i where bs: "bs = bs1 @ [(b,i)] @ bs2 @ [(b,i)] @ bs3" by force hence "b * b dvd prod_list (map fst bs)" by auto with sf[unfolded square_free_def, THEN conjunct2, rule_format, of b] have db: "degree b = 0" by auto from bs have "(b,i) \ set bs" by auto from deg[OF this] db show False by auto qed show "p = smult c (\(a, i)\set bs. a ^ Suc i)" unfolding prod using dist by (simp add: prod.distinct_set_conv_list) { fix a i b j assume ai: "(a, i) \ set bs" and bj: "(b, j) \ set bs" and diff: "(a, i) \ (b, j)" from split_list[OF ai] obtain bs1 bs2 where bs: "bs = bs1 @ (a,i) # bs2" by auto with bj diff have "(b,j) \ set (bs1 @ bs2)" by auto from split_list[OF this] obtain cs1 cs2 where cs: "bs1 @ bs2 = cs1 @ (b,j) # cs2" by auto have "prod_list (map fst bs) = a * prod_list (map fst (bs1 @ bs2))" unfolding bs by simp also have "\ = a * b * prod_list (map fst (cs1 @ cs2))" unfolding cs by simp finally obtain c where lp: "prod_list (map fst bs) = a * b * c" by auto from deg[OF ai] have 0: "gcd a b \ 0" by auto have gcd: "gcd a b * gcd a b dvd prod_list (map fst bs)" unfolding lp by (simp add: mult_dvd_mono) { assume "degree (gcd a b) > 0" from sf[unfolded square_free_def, THEN conjunct2, rule_format, OF this] gcd have False by simp } hence "degree (gcd a b) = 0" by auto with 0 show "coprime a b" using is_unit_gcd is_unit_iff_degree by blast } qed lemma square_free_factorization_def': fixes p :: "'a poly" shows "square_free_factorization p (c,bs) \ (p = smult c (\(a, i) \ bs. a ^ Suc i)) \ (square_free (prod_list (map fst bs))) \ (\ b i. (b,i) \ set bs \ degree b > 0) \ (p = 0 \ c = 0 \ bs = [])" using square_free_factorizationD'[of p c bs] square_free_factorizationI'[of p c bs] by blast lemma square_free_factorization_smult_prod_listI: fixes p :: "'a poly" assumes sff: "square_free_factorization p (c, bs1 @ (smult b (prod_list bs),i) # bs2)" and bs: "\ b. b \ set bs \ degree b > 0" shows "square_free_factorization p (c * b^(Suc i), bs1 @ map (\ b. (b,i)) bs @ bs2)" proof - from square_free_factorizationD'(3)[OF sff, of "smult b (prod_list bs)" i] have b: "b \ 0" by auto note sff = square_free_factorizationD'[OF sff] show ?thesis proof (intro square_free_factorizationI', goal_cases) case 1 thus ?case unfolding sff(1) by (simp add: o_def field_simps smult_power prod_list_pow_suc) next case 2 show ?case using sff(2) by (simp add: ac_simps o_def square_free_smult_iff[OF b]) next case 3 with sff(3) bs show ?case by auto next case 4 from sff(4)[OF this] show ?case by simp qed qed lemma square_free_factorization_further_factorization: fixes p :: "'a poly" assumes sff: "square_free_factorization p (c, bs)" and bs: "\ b i d fs. (b,i) \ set bs \ f b = (d,fs) \ b = smult d (prod_list fs) \ (\ f \ set fs. degree f > 0)" and h: "h = (\ (b,i). case f b of (d,fs) \ (d^Suc i,map (\ f. (f,i)) fs))" and gs: "gs = map h bs" and d: "d = c * prod_list (map fst gs)" and es: "es = concat (map snd gs)" shows "square_free_factorization p (d, es)" proof - note sff = square_free_factorizationD'[OF sff] show ?thesis proof (rule square_free_factorizationI') assume "p = 0" from sff(4)[OF this] show "d = 0 \ es = []" unfolding d es gs by auto next have id: "(\(a, i)\bs. a * a ^ i) = smult (prod_list (map fst gs)) (\(a, i)\es. a * a ^ i)" unfolding es gs h map_map o_def using bs proof (induct bs) case (Cons bi bs) obtain b i where bi: "bi = (b,i)" by force obtain d fs where f: "f b = (d,fs)" by force from Cons(2)[OF _ f, of i] have b: "b = smult d (prod_list fs)" unfolding bi by auto note IH = Cons(1)[OF Cons(2), of "\ _ i _ _ . i"] show ?case unfolding bi by (simp add: f o_def, simp add: b ac_simps, subst IH, auto simp: smult_power prod_list_pow_suc ac_simps) qed simp show "p = smult d (\(a, i)\es. a ^ Suc i)" unfolding sff(1) using id by (simp add: d) next fix fi i assume fi: "(fi, i) \ set es" from this[unfolded es] obtain G where G: "G \ snd ` set gs" and fi: "(fi,i) \ set G" by auto from G[unfolded gs] obtain b i where bi: "(b,i) \ set bs" and G: "G = snd (h (b,i))" by auto obtain d fs where f: "f b = (d,fs)" by force show "degree fi > 0" by (rule bs[THEN conjunct2, rule_format, OF bi f], insert fi G f, unfold h, auto) next have id: "\ c. prod_list (map fst bs) = smult c (prod_list (map fst es))" unfolding es gs map_map o_def using bs proof (induct bs) case (Cons bi bs) obtain b i where bi: "bi = (b,i)" by force obtain d fs where f: "f b = (d,fs)" by force from Cons(2)[OF _ f, of i] have b: "b = smult d (prod_list fs)" unfolding bi by auto have "\c. prod_list (map fst bs) = smult c (prod_list (map fst (concat (map (\x. snd (h x)) bs))))" by (rule Cons(1), rule Cons(2), auto) then obtain c where IH: "prod_list (map fst bs) = smult c (prod_list (map fst (concat (map (\x. snd (h x)) bs))))" by auto show ?case unfolding bi by (intro exI[of _ "c * d"], auto simp: b IH, auto simp: h f[unfolded b] o_def) qed (intro exI[of _ 1], auto) then obtain c where "prod_list (map fst bs) = smult c (prod_list (map fst es))" by blast from sff(2)[unfolded this] show "square_free (prod_list (map fst es))" by (metis smult_eq_0_iff square_free_def square_free_smult_iff) qed qed lemma square_free_factorization_prod_listI: fixes p :: "'a poly" assumes sff: "square_free_factorization p (c, bs1 @ ((prod_list bs),i) # bs2)" and bs: "\ b. b \ set bs \ degree b > 0" shows "square_free_factorization p (c, bs1 @ map (\ b. (b,i)) bs @ bs2)" using square_free_factorization_smult_prod_listI[of p c bs1 1 bs i bs2] sff bs by auto lemma square_free_factorization_factorI: fixes p :: "'a poly" assumes sff: "square_free_factorization p (c, bs1 @ (a,i) # bs2)" and r: "degree r \ 0" and s: "degree s \ 0" and a: "a = r * s" shows "square_free_factorization p (c, bs1 @ ((r,i) # (s,i) # bs2))" using square_free_factorization_prod_listI[of p c bs1 "[r,s]" i bs2] sff r s a by auto end lemma monic_square_free_irreducible_factorization: assumes mon: "monic (f :: 'b :: field poly)" and sf: "square_free f" shows "\ P. finite P \ f = \P \ P \ {q. irreducible q \ monic q}" proof - from mon have f0: "f \ 0" by auto from monic_irreducible_factorization[OF assms(1)] obtain P n where P: "finite P" "P \ {q. irreducible\<^sub>d q \ monic q}" and f: "f = (\a\P. a ^ Suc (n a))" by auto have *: "\ a \ P. n a = 0" proof (rule ccontr) assume "\ ?thesis" then obtain a where a: "a \ P" and n: "n a \ 0" by auto have "f = a ^ (Suc (n a)) * (\b\P - {a}. b ^ Suc (n b))" unfolding f by (rule prod.remove[OF P(1) a]) with n have "a * a dvd f" by (cases "n a", auto) with sf[unfolded square_free_def] f0 have "degree a = 0" by auto with a P(2)[unfolded irreducible\<^sub>d_def] show False by auto qed have "f = \ P" unfolding f by (rule prod.cong[OF refl], insert *, auto) with P show ?thesis by auto qed context assumes "SORT_CONSTRAINT('a :: {field, factorial_ring_gcd})" begin lemma monic_factorization_uniqueness: fixes P::"'a poly set" assumes finite_P: "finite P" and PQ: "\P = \Q" and P: "P \ {q. irreducible\<^sub>d q \ monic q}" and finite_Q: "finite Q" and Q: "Q \ {q. irreducible\<^sub>d q \ monic q}" shows "P = Q" proof (rule; rule subsetI) fix x assume x: "x \ P" have irr_x: "irreducible x" using x P by auto then have "\a\Q. x dvd id a" proof (rule irreducible_dvd_prod) show "x dvd prod id Q" using PQ x by (metis dvd_refl dvd_prod finite_P id_apply prod.cong) qed from this obtain a where a: "a\Q" and x_dvd_a: "x dvd a" unfolding id_def by blast have "x=a" using x P a Q irreducible\<^sub>d_dvd_eq[OF _ _ x_dvd_a] by fast thus "x \ Q" using a by simp next fix x assume x: "x \ Q" have irr_x: "irreducible x" using x Q by auto then have "\a\P. x dvd id a" proof (rule irreducible_dvd_prod) show "x dvd prod id P" using PQ x by (metis dvd_refl dvd_prod finite_Q id_apply prod.cong) qed from this obtain a where a: "a\P" and x_dvd_a: "x dvd a" unfolding id_def by blast have "x=a" using x P a Q irreducible\<^sub>d_dvd_eq[OF _ _ x_dvd_a] by fast thus "x \ P" using a by simp qed end subsection \Yun factorization and homomorphisms\ locale field_hom_0' = field_hom hom for hom :: "'a :: {field_char_0,field_gcd} \ 'b :: {field_char_0,field_gcd}" begin sublocale field_hom' .. end lemma (in field_hom_0') yun_factorization_main_hom: defines hp: "hp \ map_poly hom" defines hpi: "hpi \ map (\ (f,i). (hp f, i :: nat))" assumes monic: "monic p" and f: "f = p div gcd p (pderiv p)" and g: "g = pderiv p div gcd p (pderiv p)" shows "yun_gcd.yun_factorization_main gcd (hp f) (hp g) i (hpi as) = hpi (yun_gcd.yun_factorization_main gcd f g i as)" proof - let ?P = "\ f g. \ i as. yun_gcd.yun_factorization_main gcd (hp f) (hp g) i (hpi as) = hpi (yun_gcd.yun_factorization_main gcd f g i as)" note ind = yun_factorization_induct[OF _ _ f g monic, of ?P, rule_format] interpret map_poly_hom: map_poly_inj_comm_ring_hom.. interpret p: inj_comm_ring_hom hp unfolding hp.. note homs = map_poly_gcd[folded hp] map_poly_pderiv[folded hp] p.hom_minus map_poly_div[folded hp] show ?thesis proof (induct rule: ind) case (1 f g i as) show ?case unfolding yun_gcd.yun_factorization_main.simps[of _ "hp f"] yun_gcd.yun_factorization_main.simps[of _ f] unfolding 1 by simp next case (2 f g i as) have id: "\ f i fis. hpi ((f,i) # fis) = (hp f, i) # hpi fis" unfolding hpi by auto show ?case unfolding yun_gcd.yun_factorization_main.simps[of _ "hp f"] yun_gcd.yun_factorization_main.simps[of _ f] unfolding "p.hom_1_iff" unfolding Let_def unfolding homs[symmetric] id[symmetric] unfolding 2(2) by simp qed qed lemma square_free_square_free_factorization: "square_free (p :: 'a :: {field,factorial_ring_gcd,semiring_gcd_mult_normalize} poly) \ degree p \ 0 \ square_free_factorization p (1,[(p,0)])" by (intro square_free_factorizationI', auto) lemma constant_square_free_factorization: "degree p = 0 \ square_free_factorization p (coeff p 0,[])" by (drule degree0_coeffs [of p]) (auto simp: square_free_factorization_def) lemma (in field_hom_0') yun_monic_factorization: defines hp: "hp \ map_poly hom" defines hpi: "hpi \ map (\ (f,i). (hp f, i :: nat))" assumes monic: "monic f" shows "yun_gcd.yun_monic_factorization gcd (hp f) = hpi (yun_gcd.yun_monic_factorization gcd f)" proof - interpret map_poly_hom: map_poly_inj_comm_ring_hom.. interpret p: inj_ring_hom hp unfolding hp.. have hpiN: "hpi [] = []" unfolding hpi by simp obtain res where "res = yun_gcd.yun_factorization_main gcd (f div gcd f (pderiv f)) (pderiv f div gcd f (pderiv f)) 0 []" by auto note homs = map_poly_gcd[folded hp] map_poly_pderiv[folded hp] p.hom_minus map_poly_div[folded hp] yun_factorization_main_hom[folded hp, folded hpi, symmetric, OF monic refl refl, of _ Nil, unfolded hpiN] this show ?thesis unfolding yun_gcd.yun_monic_factorization_def Let_def unfolding homs[symmetric] unfolding hpi by (induct res, auto) qed lemma (in field_hom_0') yun_factorization_hom: defines hp: "hp \ map_poly hom" defines hpi: "hpi \ map (\ (f,i). (hp f, i :: nat))" shows "yun_factorization gcd (hp f) = map_prod hom hpi (yun_factorization gcd f)" using yun_monic_factorization[of "smult (inverse (coeff f (degree f))) f"] unfolding yun_factorization_def Let_def hp hpi by (auto simp: hom_distribs) lemma (in field_hom_0') square_free_map_poly: "square_free (map_poly hom f) = square_free f" proof - interpret map_poly_hom: map_poly_inj_comm_ring_hom.. show ?thesis unfolding square_free_iff_separable separable_def by (simp only: hom_distribs [symmetric] (*fold doesn't work!*)) (simp add: coprime_iff_gcd_eq_1 map_poly_gcd [symmetric]) qed end