diff --git a/thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy b/thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy --- a/thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy +++ b/thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy @@ -1,702 +1,644 @@ (* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) theory Square_Free_Factorization_Int imports Square_Free_Int_To_Square_Free_GFp Suitable_Prime Code_Abort_Gcd Gcd_Finite_Field_Impl begin definition yun_wrel :: "int poly \ rat \ rat poly \ bool" where "yun_wrel F c f = (map_poly rat_of_int F = smult c f)" definition yun_rel :: "int poly \ rat \ rat poly \ bool" where "yun_rel F c f = (yun_wrel F c f \ content F = 1 \ lead_coeff F > 0 \ monic f)" definition yun_erel :: "int poly \ rat poly \ bool" where "yun_erel F f = (\ c. yun_rel F c f)" lemma yun_wrelD: assumes "yun_wrel F c f" shows "map_poly rat_of_int F = smult c f" using assms unfolding yun_wrel_def by auto lemma yun_relD: assumes "yun_rel F c f" shows "yun_wrel F c f" "map_poly rat_of_int F = smult c f" "degree F = degree f" "F \ 0" "lead_coeff F > 0" "monic f" "f = 1 \ F = 1" "content F = 1" proof - note * = assms[unfolded yun_rel_def yun_wrel_def, simplified] then have "degree (map_poly rat_of_int F) = degree f" by auto then show deg: "degree F = degree f" by simp show "F \ 0" "lead_coeff F > 0" "monic f" "content F = 1" "map_poly rat_of_int F = smult c f" "yun_wrel F c f" using * by (auto simp: yun_wrel_def) { assume "f = 1" with deg have "degree F = 0" by auto from degree0_coeffs[OF this] obtain c where F: "F = [:c:]" and c: "c = lead_coeff F" by auto from c * have c0: "c > 0" by auto hence cF: "content F = c" unfolding F content_def by auto with * have "c = 1" by auto with F have "F = 1" by simp } moreover { assume "F = 1" with deg have "degree f = 0" by auto with \monic f\ have "f = 1" using monic_degree_0 by blast } ultimately show "(f = 1) \ (F = 1)" by auto qed lemma yun_erel_1_eq: assumes "yun_erel F f" shows "(F = 1) \ (f = 1)" proof - from assms[unfolded yun_erel_def] obtain c where "yun_rel F c f" by auto from yun_relD[OF this] show ?thesis by simp qed lemma yun_rel_1[simp]: "yun_rel 1 1 1" by (auto simp: yun_rel_def yun_wrel_def content_def) lemma yun_erel_1[simp]: "yun_erel 1 1" unfolding yun_erel_def using yun_rel_1 by blast lemma yun_rel_mult: "yun_rel F c f \ yun_rel G d g \ yun_rel (F * G) (c * d) (f * g)" unfolding yun_rel_def yun_wrel_def content_mult lead_coeff_mult by (auto simp: monic_mult hom_distribs) lemma yun_erel_mult: "yun_erel F f \ yun_erel G g \ yun_erel (F * G) (f * g)" unfolding yun_erel_def using yun_rel_mult[of F _ f G _ g] by blast lemma yun_rel_pow: assumes "yun_rel F c f" shows "yun_rel (F^n) (c^n) (f^n)" by (induct n, insert assms yun_rel_mult, auto) lemma yun_erel_pow: "yun_erel F f \ yun_erel (F^n) (f^n)" using yun_rel_pow unfolding yun_erel_def by blast lemma yun_wrel_pderiv: assumes "yun_wrel F c f" shows "yun_wrel (pderiv F) c (pderiv f)" by (unfold yun_wrel_def, simp add: yun_wrelD[OF assms] pderiv_smult hom_distribs) lemma yun_wrel_minus: assumes "yun_wrel F c f" "yun_wrel G c g" shows "yun_wrel (F - G) c (f - g)" using assms unfolding yun_wrel_def by (auto simp: smult_diff_right hom_distribs) -lemma gcd_smult_left: assumes "c \ 0" - shows "gcd (smult c f) g = gcd f (g :: 'b :: {field_gcd} poly)" -proof - - from assms have "normalize c = 1" - by (meson dvd_field_iff is_unit_normalize) - then show ?thesis - by (metis (no_types) Polynomial.normalize_smult gcd.commute gcd.left_commute gcd_left_idem gcd_self smult_1_left) -qed - -lemma gcd_smult_right: "c \ 0 \ gcd f (smult c g) = gcd f (g :: 'b :: {field_gcd} poly)" - using gcd_smult_left[of c g f] by (simp add: gcd.commute) - -lemma gcd_rat_to_gcd_int: "gcd (of_int_poly f :: rat poly) (of_int_poly g) = - smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))" -proof (cases "f = 0 \ g = 0") - case True - thus ?thesis by simp -next - case False - let ?r = rat_of_int - let ?rp = "map_poly ?r" - from False have gcd0: "gcd f g \ 0" by auto - hence lc0: "lead_coeff (gcd f g) \ 0" by auto - hence inv: "inverse (?r (lead_coeff (gcd f g))) \ 0" by auto - show ?thesis - proof (rule sym, rule gcdI, goal_cases) - case 1 - have "gcd f g dvd f" by auto - then obtain h where f: "f = gcd f g * h" unfolding dvd_def by auto - show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF f, of ?rp], simp add: hom_distribs) - next - case 2 - have "gcd f g dvd g" by auto - then obtain h where g: "g = gcd f g * h" unfolding dvd_def by auto - show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF g, of ?rp], simp add: hom_distribs) - next - case (3 h) - show ?case - proof (rule dvd_smult) - obtain ch ph where h: "rat_to_normalized_int_poly h = (ch, ph)" by force - from 3 obtain ff where f: "?rp f = h * ff" unfolding dvd_def by auto - from 3 obtain gg where g: "?rp g = h * gg" unfolding dvd_def by auto - from rat_to_int_factor_explicit[OF f h] obtain f' where f: "f = ph * f'" by blast - from rat_to_int_factor_explicit[OF g h] obtain g' where g: "g = ph * g'" by blast - from f g have "ph dvd gcd f g" by auto - then obtain gg where gcd: "gcd f g = ph * gg" unfolding dvd_def by auto - note * = rat_to_normalized_int_poly[OF h] - show "h dvd ?rp (gcd f g)" unfolding gcd *(1) - by (rule smult_dvd, insert *(2), auto) - qed - next - case 4 - show ?case unfolding normalize_poly_def - by (rule poly_eqI) (simp add: one_poly_def [symmetric]) - qed -qed - - lemma yun_wrel_div: assumes f: "yun_wrel F c f" and g: "yun_wrel G d g" and dvd: "G dvd F" "g dvd f" and G0: "G \ 0" shows "yun_wrel (F div G) (c / d) (f div g)" proof - let ?r = "rat_of_int" let ?rp = "map_poly ?r" from dvd obtain H h where fgh: "F = G * H" "f = g * h" unfolding dvd_def by auto from G0 yun_wrelD[OF g] have g0: "g \ 0" and d0: "d \ 0" by auto from arg_cong[OF fgh(1), of "\ x. x div G"] have H: "H = F div G" using G0 by simp from arg_cong[OF fgh(1), of ?rp] have "?rp F = ?rp G * ?rp H" by (auto simp: hom_distribs) from arg_cong[OF this, of "\ x. x div ?rp G"] G0 have id: "?rp H = ?rp F div ?rp G" by auto have "?rp (F div G) = ?rp F div ?rp G" unfolding H[symmetric] id by simp also have "\ = smult c f div smult d g" using f g unfolding yun_wrel_def by auto also have "\ = smult (c / d) (f div g)" unfolding div_smult_right[OF d0] div_smult_left by (simp add: field_simps) finally show ?thesis unfolding yun_wrel_def by simp qed lemma yun_rel_div: assumes f: "yun_rel F c f" and g: "yun_rel G d g" and dvd: "G dvd F" "g dvd f" shows "yun_rel (F div G) (c / d) (f div g)" proof - note ff = yun_relD[OF f] note gg = yun_relD[OF g] show ?thesis unfolding yun_rel_def proof (intro conjI) from yun_wrel_div[OF ff(1) gg(1) dvd gg(4)] show "yun_wrel (F div G) (c / d) (f div g)" by auto from dvd have fg: "f = g * (f div g)" by auto from arg_cong[OF fg, of monic] ff(6) gg(6) show "monic (f div g)" using monic_factor by blast from dvd have FG: "F = G * (F div G)" by auto from arg_cong[OF FG, of content, unfolded content_mult] ff(8) gg(8) show "content (F div G) = 1" by simp from arg_cong[OF FG, of lead_coeff, unfolded lead_coeff_mult] ff(5) gg(5) show "lead_coeff (F div G) > 0" by (simp add: zero_less_mult_iff) qed qed lemma yun_wrel_gcd: assumes "yun_wrel F c' f" "yun_wrel G c g" and c: "c' \ 0" "c \ 0" and d: "d = rat_of_int (lead_coeff (gcd F G))" "d \ 0" shows "yun_wrel (gcd F G) d (gcd f g)" proof - let ?r = "rat_of_int" let ?rp = "map_poly ?r" have "smult d (gcd f g) = smult d (gcd (smult c' f) (smult c g))" by (simp add: c gcd_smult_left gcd_smult_right) also have "\ = smult d (gcd (?rp F) (?rp G))" using assms(1-2)[unfolded yun_wrel_def] by simp also have "\ = smult (d * inverse d) (?rp (gcd F G))" unfolding gcd_rat_to_gcd_int d by simp also have "d * inverse d = 1" using d by auto finally show ?thesis unfolding yun_wrel_def by simp qed lemma yun_rel_gcd: assumes f: "yun_rel F c f" and g: "yun_wrel G c' g" and c': "c' \ 0" and d: "d = rat_of_int (lead_coeff (gcd F G))" shows "yun_rel (gcd F G) d (gcd f g)" unfolding yun_rel_def proof (intro conjI) note ff = yun_relD[OF f] from ff have c0: "c \ 0" by auto from ff d have d0: "d \ 0" by auto from yun_wrel_gcd[OF ff(1) g c0 c' d d0] show "yun_wrel (gcd F G) d (gcd f g)" by auto from ff have "gcd f g \ 0" by auto thus "monic (gcd f g)" by (simp add: poly_gcd_monic) obtain H where H: "gcd F G = H" by auto obtain lc where lc: "coeff H (degree H) = lc" by auto from ff have "gcd F G \ 0" by auto hence "H \ 0" "lc \ 0" unfolding H[symmetric] lc[symmetric] by auto thus "0 < lead_coeff (gcd F G)" unfolding arg_cong[OF normalize_gcd[of F G], of lead_coeff, symmetric] unfolding normalize_poly_eq_map_poly H by (auto, subst Polynomial.coeff_map_poly, auto, subst Polynomial.degree_map_poly, auto simp: sgn_if) have "H dvd F" unfolding H[symmetric] by auto then obtain K where F: "F = H * K" unfolding dvd_def by auto from arg_cong[OF this, of content, unfolded content_mult ff(8)] content_ge_0_int[of H] have "content H = 1" by (auto simp add: zmult_eq_1_iff) thus "content (gcd F G) = 1" unfolding H . qed lemma yun_factorization_main_int: assumes f: "f = p div gcd p (pderiv p)" and "g = pderiv p div gcd p (pderiv p)" "monic p" and "yun_gcd.yun_factorization_main gcd f g i hs = res" and "yun_gcd.yun_factorization_main gcd F G i Hs = Res" and "yun_rel F c f" "yun_wrel G c g" "list_all2 (rel_prod yun_erel (=)) Hs hs" shows "list_all2 (rel_prod yun_erel (=)) Res res" proof - let ?P = "\ f g. \ i hs res F G Hs Res c. yun_gcd.yun_factorization_main gcd f g i hs = res \ yun_gcd.yun_factorization_main gcd F G i Hs = Res \ yun_rel F c f \ yun_wrel G c g \ list_all2 (rel_prod yun_erel (=)) Hs hs \ list_all2 (rel_prod yun_erel (=)) Res res" note simps = yun_gcd.yun_factorization_main.simps note rel = yun_relD let ?rel = "\ F f. map_poly rat_of_int F = smult (rat_of_int (lead_coeff F)) f" show ?thesis proof (induct rule: yun_factorization_induct[of ?P, rule_format, OF _ _ assms]) case (1 f g i hs res F G Hs Res c) from rel[OF 1(4)] 1(1) have "f = 1" "F = 1" by auto from 1(2-3)[unfolded simps[of _ 1] this] have "res = hs" "Res = Hs" by auto with 1(6) show ?case by simp next case (2 f g i hs res F G Hs Res c) define d where "d = g - pderiv f" define a where "a = gcd f d" define D where "D = G - pderiv F" define A where "A = gcd F D" note f = 2(5) note g = 2(6) note hs = 2(7) note f1 = 2(1) from f1 rel[OF f] have *: "(f = 1) = False" "(F = 1) = False" and c: "c \ 0" by auto note res = 2(3)[unfolded simps[of _ f] * if_False Let_def, folded d_def a_def] note Res = 2(4)[unfolded simps[of _ F] * if_False Let_def, folded D_def A_def] note IH = 2(2)[folded d_def a_def, OF res Res] obtain c' where c': "c' = rat_of_int (lead_coeff (gcd F D))" by auto show ?case proof (rule IH) from yun_wrel_minus[OF g yun_wrel_pderiv[OF rel(1)[OF f]]] have d: "yun_wrel D c d" unfolding D_def d_def . have a: "yun_rel A c' a" unfolding A_def a_def by (rule yun_rel_gcd[OF f d c c']) hence "yun_erel A a" unfolding yun_erel_def by auto thus "list_all2 (rel_prod yun_erel (=)) ((A, i) # Hs) ((a, i) # hs)" using hs by auto have A0: "A \ 0" by (rule rel(4)[OF a]) have "A dvd D" "a dvd d" unfolding A_def a_def by auto from yun_wrel_div[OF d rel(1)[OF a] this A0] show "yun_wrel (D div A) (c / c') (d div a)" . have "A dvd F" "a dvd f" unfolding A_def a_def by auto from yun_rel_div[OF f a this] show "yun_rel (F div A) (c / c') (f div a)" . qed qed qed lemma yun_monic_factorization_int_yun_rel: assumes res: "yun_gcd.yun_monic_factorization gcd f = res" and Res: "yun_gcd.yun_monic_factorization gcd F = Res" and f: "yun_rel F c f" shows "list_all2 (rel_prod yun_erel (=)) Res res" proof - note ff = yun_relD[OF f] let ?g = "gcd f (pderiv f)" let ?yf = "yun_gcd.yun_factorization_main gcd (f div ?g) (pderiv f div ?g) 0 []" let ?G = "gcd F (pderiv F)" let ?yF = "yun_gcd.yun_factorization_main gcd (F div ?G) (pderiv F div ?G) 0 []" obtain r R where r: "?yf = r" and R: "?yF = R" by blast from res[unfolded yun_gcd.yun_monic_factorization_def Let_def r] have res: "res = [(a, i)\r . a \ 1]" by simp from Res[unfolded yun_gcd.yun_monic_factorization_def Let_def R] have Res: "Res = [(A, i)\R . A \ 1]" by simp from yun_wrel_pderiv[OF ff(1)] have f': "yun_wrel (pderiv F) c (pderiv f)" . from ff have c: "c \ 0" by auto from yun_rel_gcd[OF f f' c refl] obtain d where g: "yun_rel ?G d ?g" .. from yun_rel_div[OF f g] have 1: "yun_rel (F div ?G) (c / d) (f div ?g)" by auto from yun_wrel_div[OF f' yun_relD(1)[OF g] _ _ yun_relD(4)[OF g]] have 2: "yun_wrel (pderiv F div ?G) (c / d) (pderiv f div ?g)" by auto from yun_factorization_main_int[OF refl refl ff(6) r R 1 2] have "list_all2 (rel_prod yun_erel (=)) R r" by simp thus ?thesis unfolding res Res by (induct R r rule: list_all2_induct, auto dest: yun_erel_1_eq) qed lemma yun_rel_same_right: assumes "yun_rel f c G" "yun_rel g d G" shows "f = g" proof - note f = yun_relD[OF assms(1)] note g = yun_relD[OF assms(2)] let ?r = "rat_of_int" let ?rp = "map_poly ?r" from g have d: "d \ 0" by auto obtain a b where quot: "quotient_of (c / d) = (a,b)" by force from quotient_of_nonzero[of "c/d", unfolded quot] have b: "b \ 0" by simp note f(2) also have "smult c G = smult (c / d) (smult d G)" using d by (auto simp: field_simps) also have "smult d G = ?rp g" using g(2) by simp also have cd: "c / d = (?r a / ?r b)" using quotient_of_div[OF quot] . finally have fg: "?rp f = smult (?r a / ?r b) (?rp g)" by simp from f have "c \ 0" by auto with cd d have a: "a \ 0" by auto from arg_cong[OF fg, of "\ x. smult (?r b) x"] have "smult (?r b) (?rp f) = smult (?r a) (?rp g)" using b by auto hence "?rp (smult b f) = ?rp (smult a g)" by (auto simp: hom_distribs) then have fg: "[:b:] * f = [:a:] * g" by auto from arg_cong[OF this, of content, unfolded content_mult f(8) g(8)] have "content [: b :] = content [: a :]" by simp hence abs: "abs a = abs b" unfolding content_def using b a by auto from arg_cong[OF fg, of "\ x. lead_coeff x > 0", unfolded lead_coeff_mult] f(5) g(5) a b have "(a > 0) = (b > 0)" by (simp add: zero_less_mult_iff) with a b abs have "a = b" by auto with arg_cong[OF fg, of "\ x. x div [:b:]"] b show ?thesis by (metis nonzero_mult_div_cancel_left pCons_eq_0_iff) qed definition square_free_factorization_int_main :: "int poly \ (int poly \ nat) list" where "square_free_factorization_int_main f = (case square_free_heuristic f of None \ yun_gcd.yun_monic_factorization gcd f | Some p \ [(f,0)])" lemma square_free_factorization_int_main: assumes res: "square_free_factorization_int_main f = fs" and ct: "content f = 1" and lc: "lead_coeff f > 0" and deg: "degree f \ 0" shows "square_free_factorization f (1,fs) \ (\ fi i. (fi, i) \ set fs \ content fi = 1 \ lead_coeff fi > 0) \ distinct (map snd fs)" proof (cases "square_free_heuristic f") case None from lc have f0: "f \ 0" by auto from res None have fs: "yun_gcd.yun_monic_factorization gcd f = fs" unfolding square_free_factorization_int_main_def by auto let ?r = "rat_of_int" let ?rp = "map_poly ?r" define G where "G = smult (inverse (lead_coeff (?rp f))) (?rp f)" have "?rp f \ 0" using f0 by auto hence mon: "monic G" unfolding G_def coeff_smult by simp obtain Fs where Fs: "yun_gcd.yun_monic_factorization gcd G = Fs" by blast from lc have lg: "lead_coeff (?rp f) \ 0" by auto let ?c = "lead_coeff (?rp f)" define c where "c = ?c" have rp: "?rp f = smult c G" unfolding G_def c_def by (simp add: field_simps) have in_rel: "yun_rel f c G" unfolding yun_rel_def yun_wrel_def using rp mon lc ct by auto from yun_monic_factorization_int_yun_rel[OF Fs fs in_rel] have out_rel: "list_all2 (rel_prod yun_erel (=)) fs Fs" by auto from yun_monic_factorization[OF Fs mon] have "square_free_factorization G (1, Fs)" and dist: "distinct (map snd Fs)" by auto note sff = square_free_factorizationD[OF this(1)] from out_rel have "map snd fs = map snd Fs" by (induct fs Fs rule: list_all2_induct, auto) with dist have dist': "distinct (map snd fs)" by auto have main: "square_free_factorization f (1, fs) \ (\ fi i. (fi, i) \ set fs \ content fi = 1 \ lead_coeff fi > 0)" unfolding square_free_factorization_def split proof (intro conjI allI impI) from ct have "f \ 0" by auto thus "f = 0 \ 1 = 0" "f = 0 \ fs = []" by auto from dist' show "distinct fs" by (simp add: distinct_map) { fix a i assume a: "(a,i) \ set fs" with out_rel obtain bj where "bj \ set Fs" and "rel_prod yun_erel (=) (a,i) bj" unfolding list_all2_conv_all_nth set_conv_nth by fastforce then obtain b where b: "(b,i) \ set Fs" and ab: "yun_erel a b" by (cases bj, auto simp: rel_prod.simps) from sff(2)[OF b] have b': "square_free b" "degree b \ 0" by auto from ab obtain c where rel: "yun_rel a c b" unfolding yun_erel_def by auto note aa = yun_relD[OF this] from aa have c0: "c \ 0" by auto from b' aa(3) show "degree a > 0" by simp from square_free_smult[OF c0 b'(1), folded aa(2)] show "square_free a" unfolding square_free_def by (force simp: dvd_def hom_distribs) show cnt: "content a = 1" and lc: "lead_coeff a > 0" using aa by auto fix A I assume A: "(A,I) \ set fs" and diff: "(a,i) \ (A,I)" from a[unfolded set_conv_nth] obtain k where k: "fs ! k = (a,i)" "k < length fs" by auto from A[unfolded set_conv_nth] obtain K where K: "fs ! K = (A,I)" "K < length fs" by auto from diff k K have kK: "k \ K" by auto from dist'[unfolded distinct_conv_nth length_map, rule_format, OF k(2) K(2) kK] have iI: "i \ I" using k K by simp from A out_rel obtain Bj where "Bj \ set Fs" and "rel_prod yun_erel (=) (A,I) Bj" unfolding list_all2_conv_all_nth set_conv_nth by fastforce then obtain B where B: "(B,I) \ set Fs" and AB: "yun_erel A B" by (cases Bj, auto simp: rel_prod.simps) then obtain C where Rel: "yun_rel A C B" unfolding yun_erel_def by auto note AA = yun_relD[OF this] from iI have "(b,i) \ (B,I)" by auto from sff(3)[OF b B this] have cop: "coprime b B" by simp from AA have C: "C \ 0" by auto from yun_rel_gcd[OF rel AA(1) C refl] obtain c where "yun_rel (gcd a A) c (gcd b B)" by auto note rel = yun_relD[OF this] from rel(2) cop have "?rp (gcd a A) = [: c :]" by simp from arg_cong[OF this, of degree] have "degree (gcd a A) = 0" by simp from degree0_coeffs[OF this] obtain c where gcd: "gcd a A = [: c :]" by auto from rel(8) rel(5) show "Rings.coprime a A" by (auto intro!: gcd_eq_1_imp_coprime simp add: gcd) } let ?prod = "\ fs. (\(a, i)\set fs. a ^ Suc i)" let ?pr = "\ fs. (\(a, i)\fs. a ^ Suc i)" define pr where "pr = ?prod fs" from \distinct fs\ have pfs: "?prod fs = ?pr fs" by (rule prod.distinct_set_conv_list) from \distinct Fs\ have pFs: "?prod Fs = ?pr Fs" by (rule prod.distinct_set_conv_list) from out_rel have "yun_erel (?prod fs) (?prod Fs)" unfolding pfs pFs proof (induct fs Fs rule: list_all2_induct) case (Cons ai fs Ai Fs) obtain a i where ai: "ai = (a,i)" by force from Cons(1) ai obtain A where Ai: "Ai = (A,i)" and rel: "yun_erel a A" by (cases Ai, auto simp: rel_prod.simps) show ?case unfolding ai Ai using yun_erel_mult[OF yun_erel_pow[OF rel, of "Suc i"] Cons(3)] by auto qed simp also have "?prod Fs = G" using sff(1) by simp finally obtain d where rel: "yun_rel pr d G" unfolding yun_erel_def pr_def by auto with in_rel have "f = pr" by (rule yun_rel_same_right) thus "f = smult 1 (?prod fs)" unfolding pr_def by simp qed from main dist' show ?thesis by auto next case (Some p) from res[unfolded square_free_factorization_int_main_def Some] have fs: "fs = [(f,0)]" by auto from lc have f0: "f \ 0" by auto from square_free_heuristic[OF Some] poly_mod_prime.separable_impl(1)[of p f] square_free_mod_imp_square_free[of p f] deg show ?thesis unfolding fs by (auto simp: ct lc square_free_factorization_def f0 poly_mod_prime_def) qed definition square_free_factorization_int' :: "int poly \ int \ (int poly \ nat)list" where "square_free_factorization_int' f = (if degree f = 0 then (lead_coeff f,[]) else (let \ \content factorization\ c = content f; d = (sgn (lead_coeff f) * c); g = sdiv_poly f d \ \and \square_free\ factorization\ in (d, square_free_factorization_int_main g)))" lemma square_free_factorization_int': assumes res: "square_free_factorization_int' f = (d, fs)" shows "square_free_factorization f (d,fs)" "(fi, i) \ set fs \ content fi = 1 \ lead_coeff fi > 0" "distinct (map snd fs)" proof - note res = res[unfolded square_free_factorization_int'_def Let_def] have "square_free_factorization f (d,fs) \ ((fi, i) \ set fs \ content fi = 1 \ lead_coeff fi > 0) \ distinct (map snd fs)" proof (cases "degree f = 0") case True from degree0_coeffs[OF True] obtain c where f: "f = [: c :]" by auto thus ?thesis using res by (simp add: square_free_factorization_def) next case False let ?s = "sgn (lead_coeff f)" have s: "?s \ {-1,1}" using False unfolding sgn_if by auto define g where "g = smult ?s f" let ?d = "?s * content f" have "content g = content ([:?s:] * f)" unfolding g_def by simp also have "\ = content [:?s:] * content f" unfolding content_mult by simp also have "content [:?s:] = 1" using s by (auto simp: content_def) finally have cg: "content g = content f" by simp from False res have d: "d = ?d" and fs: "fs = square_free_factorization_int_main (sdiv_poly f ?d)" by auto let ?g = "primitive_part g" define ng where "ng = primitive_part g" note fs also have "sdiv_poly f ?d = sdiv_poly g (content g)" unfolding cg unfolding g_def by (rule poly_eqI, unfold coeff_sdiv_poly coeff_smult, insert s, auto simp: div_minus_right) finally have fs: "square_free_factorization_int_main ng = fs" unfolding primitive_part_alt_def ng_def by simp have "lead_coeff f \ 0" using False by auto hence lg: "lead_coeff g > 0" unfolding g_def lead_coeff_smult by (meson linorder_neqE_linordered_idom sgn_greater sgn_less zero_less_mult_iff) hence g0: "g \ 0" by auto from g0 have "content g \ 0" by simp from arg_cong[OF content_times_primitive_part[of g], of lead_coeff, unfolded lead_coeff_smult] lg content_ge_0_int[of g] have lg': "lead_coeff ng > 0" unfolding ng_def by (metis \content g \ 0\ dual_order.antisym dual_order.strict_implies_order zero_less_mult_iff) from content_primitive_part[OF g0] have c_ng: "content ng = 1" unfolding ng_def . have "degree ng = degree f" using \content [:sgn (lead_coeff f):] = 1\ g_def ng_def by (auto simp add: sgn_eq_0_iff) with False have "degree ng \ 0" by auto note main = square_free_factorization_int_main[OF fs c_ng lg' this] show ?thesis proof (intro conjI impI) { assume "(fi, i) \ set fs" with main show "content fi = 1" "0 < lead_coeff fi" by auto } have d0: "d \ 0" using \content [:?s:] = 1\ d by (auto simp:sgn_eq_0_iff) have "smult d ng = smult ?s (smult (content g) (primitive_part g))" unfolding ng_def d cg by simp also have "smult (content g) (primitive_part g) = g" using content_times_primitive_part . also have "smult ?s g = f" unfolding g_def using s by auto finally have id: "smult d ng = f" . from main have "square_free_factorization ng (1, fs)" by auto from square_free_factorization_smult[OF d0 this] show "square_free_factorization f (d,fs)" unfolding id by simp show "distinct (map snd fs)" using main by auto qed qed thus "square_free_factorization f (d,fs)" "(fi, i) \ set fs \ content fi = 1 \ lead_coeff fi > 0" "distinct (map snd fs)" by auto qed definition x_split :: "'a :: semiring_0 poly \ nat \ 'a poly" where "x_split f = (let fs = coeffs f; zs = takeWhile ((=) 0) fs in case zs of [] \ (0,f) | _ \ (length zs, poly_of_list (dropWhile ((=) 0) fs)))" lemma x_split: assumes "x_split f = (n, g)" shows "f = monom 1 n * g" "n \ 0 \ f \ 0 \ \ monom 1 1 dvd g" proof - define zs where "zs = takeWhile ((=) 0) (coeffs f)" note res = assms[unfolded zs_def[symmetric] x_split_def Let_def] have "f = monom 1 n * g \ ((n \ 0 \ f \ 0) \ \ (monom 1 1 dvd g))" (is "_ \ (_ \ \ (?x dvd _))") proof (cases "f = 0") case True with res have "n = 0" "g = 0" unfolding zs_def by auto thus ?thesis using True by auto next case False note f = this show ?thesis proof (cases "zs = []") case True hence choice: "coeff f 0 \ 0" using f unfolding zs_def coeff_f_0_code poly_compare_0_code by (cases "coeffs f", auto) have dvd: "?x dvd h \ coeff h 0 = 0" for h by (simp add: monom_1_dvd_iff') from True choice res f show ?thesis unfolding dvd by auto next case False define ys where "ys = dropWhile ((=) 0) (coeffs f)" have dvd: "?x dvd h \ coeff h 0 = 0" for h by (simp add: monom_1_dvd_iff') from res False have n: "n = length zs" and g: "g = poly_of_list ys" unfolding ys_def by (cases zs, auto)+ obtain xx where xx: "coeffs f = xx" by auto have "coeffs f = zs @ ys" unfolding zs_def ys_def by auto also have "zs = replicate n 0" unfolding zs_def n xx by (induct xx, auto) finally have ff: "coeffs f = replicate n 0 @ ys" by auto from f have "lead_coeff f \ 0" by auto then have nz: "coeffs f \ []" "last (coeffs f) \ 0" by (simp_all add: last_coeffs_eq_coeff_degree) have ys: "ys \ []" using nz[unfolded ff] by auto with ys_def have hd: "hd ys \ 0" by (metis (full_types) hd_dropWhile) hence "coeff (poly_of_list ys) 0 \ 0" unfolding poly_of_list_def coeff_Poly using ys by (cases ys, auto) moreover have "coeffs (Poly ys) = ys" by (simp add: ys_def strip_while_dropWhile_commute) then have "coeffs (monom_mult n (Poly ys)) = replicate n 0 @ ys" by (simp add: coeffs_eq_iff monom_mult_def [symmetric] ff ys monom_mult_code) ultimately show ?thesis unfolding dvd g by (auto simp add: coeffs_eq_iff monom_mult_def [symmetric] ff) qed qed thus "f = monom 1 n * g" "n \ 0 \ f \ 0 \ \ monom 1 1 dvd g" by auto qed definition square_free_factorization_int :: "int poly \ int \ (int poly \ nat)list" where "square_free_factorization_int f = (case x_split f of (n,g) \ \extract \x^n\\ \ case square_free_factorization_int' g of (d,fs) \ if n = 0 then (d,fs) else (d, (monom 1 1, n - 1) # fs))" lemma square_free_factorization_int: assumes res: "square_free_factorization_int f = (d, fs)" shows "square_free_factorization f (d,fs)" "(fi, i) \ set fs \ primitive fi \ lead_coeff fi > 0" proof - obtain n g where xs: "x_split f = (n,g)" by force obtain c hs where sf: "square_free_factorization_int' g = (c,hs)" by force from res[unfolded square_free_factorization_int_def xs sf split] have d: "d = c" and fs: "fs = (if n = 0 then hs else (monom 1 1, n - 1) # hs)" by (cases n, auto) note sff = square_free_factorization_int'(1-2)[OF sf] note xs = x_split[OF xs] let ?x = "monom 1 1 :: int poly" have x: "primitive ?x \ lead_coeff ?x = 1 \ degree ?x = 1" by (auto simp add: degree_monom_eq content_def monom_Suc) thus "(fi, i) \ set fs \ primitive fi \ lead_coeff fi > 0" using sff(2) unfolding fs by (cases n, auto) show "square_free_factorization f (d,fs)" proof (cases n) case 0 with d fs sff xs show ?thesis by auto next case (Suc m) with xs have fg: "f = monom 1 (Suc m) * g" and dvd: "\ ?x dvd g" by auto from Suc have fs: "fs = (?x,m) # hs" unfolding fs by auto have degx: "degree ?x = 1" by code_simp from irreducible\<^sub>d_square_free[OF linear_irreducible\<^sub>d[OF this]] have sfx: "square_free ?x" by auto have fg: "f = ?x ^ n * g" unfolding fg Suc by (metis x_pow_n) have eq0: "?x ^ n * g = 0 \ g = 0" by simp note sf = square_free_factorizationD[OF sff(1)] { fix a i assume ai: "(a,i) \ set hs" with sf(4) have g0: "g \ 0" by auto from split_list[OF ai] obtain ys zs where hs: "hs = ys @ (a,i) # zs" by auto have "a dvd g" unfolding square_free_factorization_prod_list[OF sff(1)] hs by (rule dvd_smult, simp add: ac_simps) moreover have "\ ?x dvd g" using xs[unfolded Suc] by auto ultimately have dvd: "\ ?x dvd a" using dvd_trans by blast from sf(2)[OF ai] have "a \ 0" by auto have "1 = gcd ?x a" proof (rule gcdI) fix d assume d: "d dvd ?x" "d dvd a" from content_dvd_contentI[OF d(1)] x have cnt: "is_unit (content d)" by auto show "is_unit d" proof (cases "degree d = 1") case False with divides_degree[OF d(1), unfolded degx] have "degree d = 0" by auto from degree0_coeffs[OF this] obtain c where dc: "d = [:c:]" by auto from cnt[unfolded dc] have "is_unit c" by (auto simp: content_def, cases "c = 0", auto) hence "d * d = 1" unfolding dc by (cases "c = -1"; cases "c = 1", auto) thus "is_unit d" by (metis dvd_triv_right) next case True from d(1) obtain e where xde: "?x = d * e" unfolding dvd_def by auto from arg_cong[OF this, of degree] degx have "degree d + degree e = 1" by (metis True add.right_neutral degree_0 degree_mult_eq one_neq_zero) with True have "degree e = 0" by auto from degree0_coeffs[OF this] xde obtain e where xde: "?x = [:e:] * d" by auto from arg_cong[OF this, of content, unfolded content_mult] x have "content [:e:] * content d = 1" by auto also have "content [:e :] = abs e" by (auto simp: content_def, cases "e = 0", auto) finally have "\e\ * content d = 1" . from pos_zmult_eq_1_iff_lemma[OF this] have "e * e = 1" by (cases "e = 1"; cases "e = -1", auto) with arg_cong[OF xde, of "smult e"] have "d = ?x * [:e:]" by auto hence "?x dvd d" unfolding dvd_def by blast with d(2) have "?x dvd a" by (metis dvd_trans) with dvd show ?thesis by auto qed qed auto hence "coprime ?x a" by (simp add: gcd_eq_1_imp_coprime) note this dvd } note hs_dvd_x = this from hs_dvd_x[of ?x m] have nmem: "(?x,m) \ set hs" by auto hence eq: "?x ^ n * g = smult c (\(a, i)\set fs. a ^ Suc i)" unfolding sf(1) unfolding fs Suc by simp show ?thesis unfolding fg d unfolding square_free_factorization_def split eq0 unfolding eq proof (intro conjI allI impI, rule refl) fix a i assume ai: "(a,i) \ set fs" thus "square_free a" "degree a > 0" using sf(2) sfx degx unfolding fs by auto fix b j assume bj: "(b,j) \ set fs" and diff: "(a,i) \ (b,j)" consider (hs_hs) "(a,i) \ set hs" "(b,j) \ set hs" | (hs_x) "(a,i) \ set hs" "b = ?x" | (x_hs) "(b,j) \ set hs" "a = ?x" using ai bj diff unfolding fs by auto then show "Rings.coprime a b" proof cases case hs_hs from sf(3)[OF this diff] show ?thesis . next case hs_x from hs_dvd_x(1)[OF hs_x(1)] show ?thesis unfolding hs_x(2) by (simp add: ac_simps) next case x_hs from hs_dvd_x(1)[OF x_hs(1)] show ?thesis unfolding x_hs(2) by simp qed next show "g = 0 \ c = 0" using sf(4) by auto show "g = 0 \ fs = []" using sf(4) xs Suc by auto show "distinct fs" using sf(5) nmem unfolding fs by auto qed qed qed end diff --git a/thys/Polynomial_Factorization/Gauss_Lemma.thy b/thys/Polynomial_Factorization/Gauss_Lemma.thy --- a/thys/Polynomial_Factorization/Gauss_Lemma.thy +++ b/thys/Polynomial_Factorization/Gauss_Lemma.thy @@ -1,451 +1,510 @@ (* Author: René Thiemann Akihisa Yamada License: BSD *) (*TODO: Rename! *) section \Gauss Lemma\ text \We formalized Gauss Lemma, that the content of a product of two polynomials $p$ and $q$ is the product of the contents of $p$ and $q$. As a corollary we provide an algorithm to convert a rational factor of an integer polynomial into an integer factor. In contrast to the theory on unique factorization domains -- where Gauss Lemma is also proven in a more generic setting -- we are here in an executable setting and do not use the unspecified $some-gcd$ function. Moreover, there is a slight difference in the definition of content: in this theory it is only defined for integer-polynomials, whereas in the UFD theory, the content is defined for polynomials in the fraction field.\ theory Gauss_Lemma imports "HOL-Computational_Algebra.Primes" + "HOL-Computational_Algebra.Field_as_Ring" Polynomial_Interpolation.Ring_Hom_Poly Missing_Polynomial_Factorial begin lemma primitive_part_alt_def: "primitive_part p = sdiv_poly p (content p)" by (simp add: primitive_part_def sdiv_poly_def) definition common_denom :: "rat list \ int \ int list" where "common_denom xs \ let nds = map quotient_of xs; denom = list_lcm (map snd nds); ints = map (\ (n,d). n * denom div d) nds in (denom, ints)" definition rat_to_int_poly :: "rat poly \ int \ int poly" where "rat_to_int_poly p \ let ais = coeffs p; d = fst (common_denom ais) in (d, map_poly (\ x. case quotient_of x of (p,q) \ p * d div q) p)" definition rat_to_normalized_int_poly :: "rat poly \ rat \ int poly" where "rat_to_normalized_int_poly p \ if p = 0 then (1,0) else case rat_to_int_poly p of (s,q) \ (of_int (content q) / of_int s, primitive_part q)" lemma rat_to_normalized_int_poly_code[code]: "rat_to_normalized_int_poly p = (if p = 0 then (1,0) else case rat_to_int_poly p of (s,q) \ let c = content q in (of_int c / of_int s, sdiv_poly q c))" unfolding Let_def rat_to_normalized_int_poly_def primitive_part_alt_def .. lemma common_denom: assumes cd: "common_denom xs = (dd,ys)" shows "xs = map (\ i. of_int i / of_int dd) ys" "dd > 0" "\x. x \ set xs \ rat_of_int (case quotient_of x of (n, x) \ n * dd div x) / rat_of_int dd = x" proof - let ?nds = "map quotient_of xs" define nds where "nds = ?nds" let ?denom = "list_lcm (map snd nds)" let ?ints = "map (\ (n,d). n * dd div d) nds" from cd[unfolded common_denom_def Let_def] have dd: "dd = ?denom" and ys: "ys = ?ints" unfolding nds_def by auto show dd0: "dd > 0" unfolding dd by (intro list_lcm_pos(3), auto simp: nds_def quotient_of_nonzero) { fix x assume x: "x \ set xs" obtain p q where quot: "quotient_of x = (p,q)" by force from x have "(p,q) \ set nds" unfolding nds_def using quot by force hence "q \ set (map snd nds)" by force from list_lcm[OF this] have q: "q dvd dd" unfolding dd . show "rat_of_int (case quotient_of x of (n, x) \ n * dd div x) / rat_of_int dd = x" unfolding quot split unfolding quotient_of_div[OF quot] proof - have f1: "q * (dd div q) = dd" using dvd_mult_div_cancel q by blast have "rat_of_int (dd div q) \ 0" using dd0 dvd_mult_div_cancel q by fastforce thus "rat_of_int (p * dd div q) / rat_of_int dd = rat_of_int p / rat_of_int q" using f1 by (metis (no_types) div_mult_swap mult_divide_mult_cancel_right of_int_mult q) qed } note main = this show "xs = map (\ i. of_int i / of_int dd) ys" unfolding ys map_map o_def nds_def by (rule sym, rule map_idI, rule main) qed lemma rat_to_int_poly: assumes "rat_to_int_poly p = (d,q)" shows "p = smult (inverse (of_int d)) (map_poly of_int q)" "d > 0" proof - let ?f = "\ x. case quotient_of x of (pa, x) \ pa * d div x" define f where "f = ?f" from assms[unfolded rat_to_int_poly_def Let_def] obtain xs where cd: "common_denom (coeffs p) = (d,xs)" and q: "q = map_poly f p" unfolding f_def by (cases "common_denom (coeffs p)", auto) from common_denom[OF cd] have d: "d > 0" and id: "\ x. x \ set (coeffs p) \ rat_of_int (f x) / rat_of_int d = x" unfolding f_def by auto have f0: "f 0 = 0" unfolding f_def by auto have id: "rat_of_int (f (coeff p n)) / rat_of_int d = coeff p n" for n using id[of "coeff p n"] f0 range_coeff by (cases "coeff p n = 0", auto) show "d > 0" by fact show "p = smult (inverse (of_int d)) (map_poly of_int q)" unfolding q smult_as_map_poly using id f0 by (intro poly_eqI, auto simp: field_simps coeff_map_poly) qed lemma content_ge_0_int: "content p \ (0 :: int)" unfolding content_def by (cases "coeffs p", auto) lemma abs_content_int[simp]: fixes p :: "int poly" shows "abs (content p) = content p" using content_ge_0_int[of p] by auto lemma content_smult_int: fixes p :: "int poly" shows "content (smult a p) = abs a * content p" by simp lemma normalize_non_0_smult: "\ a. (a :: 'a :: semiring_gcd) \ 0 \ smult a (primitive_part p) = p" by (cases "p = 0", rule exI[of _ 1], simp, rule exI[of _ "content p"], auto) lemma rat_to_normalized_int_poly: assumes "rat_to_normalized_int_poly p = (d,q)" shows "p = smult d (map_poly of_int q)" "d > 0" "p \ 0 \ content q = 1" "degree q = degree p" proof - have "p = smult d (map_poly of_int q) \ d > 0 \ (p \ 0 \ content q = 1)" proof (cases "p = 0") case True thus ?thesis using assms unfolding rat_to_normalized_int_poly_def by (auto simp: eval_poly_def) next case False hence p0: "p \ 0" by auto obtain s r where id: "rat_to_int_poly p = (s,r)" by force let ?cr = "rat_of_int (content r)" let ?s = "rat_of_int s" let ?q = "map_poly rat_of_int q" from rat_to_int_poly[OF id] have p: "p = smult (inverse ?s) (map_poly of_int r)" and s: "s > 0" by auto let ?q = "map_poly rat_of_int q" from p0 assms[unfolded rat_to_normalized_int_poly_def id split] have d: "d = ?cr / ?s" and q: "q = primitive_part r" by auto from content_times_primitive_part[of r, folded q] have qr: "smult (content r) q = r" . have "smult d ?q = smult (?cr / ?s) ?q" unfolding d by simp also have "?cr / ?s = ?cr * inverse ?s" by (rule divide_inverse) also have "\ = inverse ?s * ?cr" by simp also have "smult (inverse ?s * ?cr) ?q = smult (inverse ?s) (smult ?cr ?q)" by simp also have "smult ?cr ?q = map_poly of_int (smult (content r) q)" by (simp add: hom_distribs) also have "\ = map_poly of_int r" unfolding qr .. finally have pq: "p = smult d ?q" unfolding p by simp from p p0 have r0: "r \ 0" by auto from content_eq_zero_iff[of r] content_ge_0_int[of r] r0 have cr: "?cr > 0" by linarith with s have d0: "d > 0" unfolding d by auto from content_primitive_part[OF r0] have cq: "content q = 1" unfolding q . from pq d0 cq show ?thesis by auto qed thus p: "p = smult d (map_poly of_int q)" and d: "d > 0" and "p \ 0 \ content q = 1" by auto show "degree q = degree p" unfolding p smult_as_map_poly by (rule sym, subst map_poly_map_poly, force+, rule degree_map_poly, insert d, auto) qed lemma content_dvd_1: "content g = 1" if "content f = (1 :: 'a :: semiring_gcd)" "g dvd f" proof - from \g dvd f\ have "content g dvd content f" by (rule content_dvd_contentI) with \content f = 1\ show ?thesis by simp qed lemma dvd_smult_int: fixes c :: int assumes c: "c \ 0" and dvd: "q dvd (smult c p)" shows "primitive_part q dvd p" proof (cases "p = 0") case True thus ?thesis by auto next case False note p0 = this let ?cp = "smult c p" from p0 c have cp0: "?cp \ 0" by auto from dvd obtain r where prod: "?cp = q * r" unfolding dvd_def by auto from prod cp0 have q0: "q \ 0" and r0: "r \ 0" by auto let ?c = "content :: int poly \ int" let ?n = "primitive_part :: int poly \ int poly" let ?pn = "\ p. smult (?c p) (?n p)" have cq: "(?c q = 0) = False" using content_eq_zero_iff q0 by auto from prod have id1: "?cp = ?pn q * ?pn r" unfolding content_times_primitive_part by simp from arg_cong[OF this, of content, unfolded content_smult_int content_mult content_primitive_part[OF r0] content_primitive_part[OF q0], symmetric] p0[folded content_eq_zero_iff] c have "abs c dvd ?c q * ?c r" unfolding dvd_def by auto hence "c dvd ?c q * ?c r" by auto then obtain d where id: "?c q * ?c r = c * d" unfolding dvd_def by auto have "?cp = ?pn q * ?pn r" by fact also have "\ = smult (c * d) (?n q * ?n r)" unfolding id [symmetric] by (metis content_mult content_times_primitive_part primitive_part_mult) finally have id: "?cp = smult c (?n q * smult d (?n r))" by (simp add: mult.commute) interpret map_poly_inj_zero_hom "(*) c" using c by (unfold_locales, auto) have "p = ?n q * smult d (?n r)" using id[unfolded smult_as_map_poly[of c]] by auto thus dvd: "?n q dvd p" unfolding dvd_def by blast qed lemma irreducible\<^sub>d_primitive_part: fixes p :: "int poly" (* can be relaxed but primitive_part_mult has bad type constraint *) shows "irreducible\<^sub>d (primitive_part p) \ irreducible\<^sub>d p" (is "?l \ ?r") proof (rule iffI, rule irreducible\<^sub>dI) assume l: ?l show "degree p > 0" using l by auto have dpp: "degree (primitive_part p) = degree p" by simp fix q r assume deg: "degree q < degree p" "degree r < degree p" and "p = q * r" then have pp: "primitive_part p = primitive_part q * primitive_part r" by (simp add: primitive_part_mult) have "\ irreducible\<^sub>d (primitive_part p)" apply (intro reducible\<^sub>dI, rule exI[of _ "primitive_part q"], rule exI[of _ "primitive_part r"], unfold dpp) using deg pp by auto with l show False by auto next show "?r \ ?l" by (metis irreducible\<^sub>d_smultI normalize_non_0_smult) qed lemma irreducible\<^sub>d_smult_int: fixes c :: int assumes c: "c \ 0" shows "irreducible\<^sub>d (smult c p) = irreducible\<^sub>d p" (is "?l = ?r") using irreducible\<^sub>d_primitive_part[of "smult c p", unfolded primitive_part_smult] c apply (cases "c < 0", simp) apply (metis add.inverse_inverse add.inverse_neutral c irreducible\<^sub>d_smultI normalize_non_0_smult smult_1_left smult_minus_left) apply (simp add: irreducible\<^sub>d_primitive_part) done lemma irreducible\<^sub>d_as_irreducible: fixes p :: "int poly" shows "irreducible\<^sub>d p \ irreducible (primitive_part p)" using irreducible_primitive_connect[of "primitive_part p"] by (cases "p = 0", auto simp: irreducible\<^sub>d_primitive_part) lemma rat_to_int_factor_content_1: fixes p :: "int poly" assumes cp: "content p = 1" and pgh: "map_poly rat_of_int p = g * h" and g: "rat_to_normalized_int_poly g = (r,rg)" and h: "rat_to_normalized_int_poly h = (s,sh)" and p: "p \ 0" shows "p = rg * sh" proof - let ?r = "rat_of_int" let ?rp = "map_poly ?r" from p have rp0: "?rp p \ 0" by simp with pgh have g0: "g \ 0" and h0: "h \ 0" by auto from rat_to_normalized_int_poly[OF g] g0 have r: "r > 0" "r \ 0" and g: "g = smult r (?rp rg)" and crg: "content rg = 1" by auto from rat_to_normalized_int_poly[OF h] h0 have s: "s > 0" "s \ 0" and h: "h = smult s (?rp sh)" and csh: "content sh = 1" by auto let ?irs = "inverse (r * s)" from r s have irs0: "?irs \ 0" by (auto simp: field_simps) have "?rp (rg * sh) = ?rp rg * ?rp sh" by (simp add: hom_distribs) also have "\ = smult ?irs (?rp p)" unfolding pgh g h using r s by (simp add: field_simps) finally have id: "?rp (rg * sh) = smult ?irs (?rp p)" by auto have rsZ: "?irs \ \" proof (rule ccontr) assume not: "\ ?irs \ \" obtain n d where irs': "quotient_of ?irs = (n,d)" by force from quotient_of_denom_pos[OF irs'] have "d > 0" . from not quotient_of_div[OF irs'] have "d \ 1" "d \ 0" and irs: "?irs = ?r n / ?r d" by auto with irs0 have n0: "n \ 0" by auto from \d > 0\ \d \ 1\ have "d \ 2" and "\ d dvd 1" by auto with content_iff[of d p, unfolded cp] obtain c where c: "c \ set (coeffs p)" and dc: "\ d dvd c" by auto from c range_coeff[of p] obtain i where "c = coeff p i" by auto from arg_cong[OF id, of "\ p. coeff p i", unfolded coeff_smult of_int_hom.coeff_map_poly_hom this[symmetric] irs] have "?r n / ?r d * ?r c \ \" by (metis Ints_of_int) also have "?r n / ?r d * ?r c = ?r (n * c) / ?r d" by simp finally have inZ: "?r (n * c) / ?r d \ \" . have cop: "coprime n d" by (rule quotient_of_coprime[OF irs']) (* now there comes tedious reasoning that `coprime n d` `\ d dvd c` ` nc / d \ \` yields a contradiction *) define prod where "prod = ?r (n * c) / ?r d" obtain n' d' where quot: "quotient_of prod = (n',d')" by force have qr: "\ x. quotient_of (?r x) = (x, 1)" using Rat.of_int_def quotient_of_int by auto from quotient_of_denom_pos[OF quot] have "d' > 0" . with quotient_of_div[OF quot] inZ[folded prod_def] have "d' = 1" by (metis Ints_cases Rat.of_int_def old.prod.inject quot quotient_of_int) with quotient_of_div[OF quot] have "prod = ?r n'" by auto from arg_cong[OF this, of quotient_of, unfolded prod_def rat_divide_code qr Let_def split] have "Rat.normalize (n * c, d) = (n',1)" by simp from normalize_crossproduct[OF \d \ 0\, of 1 "n * c" n', unfolded this] have id: "n * c = n' * d" by auto from quotient_of_coprime[OF irs'] have "coprime n d" . with id have "d dvd c" by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right) with dc show False .. qed then obtain irs where irs: "?irs = ?r irs" unfolding Ints_def by blast from id[unfolded irs, folded hom_distribs, unfolded of_int_poly_hom.eq_iff] have p: "rg * sh = smult irs p" by auto have "content (rg * sh) = 1" unfolding content_mult crg csh by auto from this[unfolded p content_smult_int cp] have "abs irs = 1" by simp hence "abs ?irs = 1" using irs by auto with r s have "?irs = 1" by auto with irs have "irs = 1" by auto with p show p: "p = rg * sh" by auto qed lemma rat_to_int_factor_explicit: fixes p :: "int poly" assumes pgh: "map_poly rat_of_int p = g * h" and g: "rat_to_normalized_int_poly g = (r,rg)" shows "\ r. p = rg * smult (content p) r" proof - show ?thesis proof (cases "p = 0") case True show ?thesis unfolding True by (rule exI[of _ 0], auto simp: degree_monom_eq) next case False hence p: "p \ 0" by auto let ?r = "rat_of_int" let ?rp = "map_poly ?r" define q where "q = primitive_part p" from content_times_primitive_part[of p, folded q_def] content_eq_zero_iff[of p] p obtain a where a: "a \ 0" and pq: "p = smult a q" and acp: "content p = a" by metis from a pq p have ra: "?r a \ 0" and q0: "q \ 0" by auto from content_primitive_part[OF p, folded q_def] have cq: "content q = 1" by auto obtain s sh where h: "rat_to_normalized_int_poly (smult (inverse (?r a)) h) = (s,sh)" by force from arg_cong[OF pgh[unfolded pq], of "smult (inverse (?r a))"] ra have "?rp q = g * smult (inverse (?r a)) h" by (auto simp: hom_distribs) from rat_to_int_factor_content_1[OF cq this g h q0] have qrs: "q = rg * sh" . show ?thesis unfolding acp unfolding pq qrs by (rule exI[of _ sh], auto) qed qed lemma rat_to_int_factor: fixes p :: "int poly" assumes pgh: "map_poly rat_of_int p = g * h" shows "\ g' h'. p = g' * h' \ degree g' = degree g \ degree h' = degree h" proof(cases "p = 0") case True with pgh have "g = 0 \ h = 0" by auto then show ?thesis by (metis True degree_0 mult_hom.hom_zero mult_zero_left rat_to_normalized_int_poly(4) surj_pair) next case False obtain r rg where ri: "rat_to_normalized_int_poly (smult (1 / of_int (content p)) g) = (r,rg)" by force obtain q qh where ri2: "rat_to_normalized_int_poly h = (q,qh)" by force show ?thesis proof (intro exI conjI) have "of_int_poly (primitive_part p) = smult (1 / of_int (content p)) (g * h)" apply (auto simp: primitive_part_def pgh[symmetric] smult_map_poly map_poly_map_poly o_def intro!: map_poly_cong) by (metis (no_types, lifting) content_dvd_coeffs div_by_0 dvd_mult_div_cancel floor_of_int nonzero_mult_div_cancel_left of_int_hom.hom_zero of_int_mult) also have "\ = smult (1 / of_int (content p)) g * h" by simp finally have "of_int_poly (primitive_part p) = \". note main = rat_to_int_factor_content_1[OF _ this ri ri2, simplified, OF False] show "p = smult (content p) rg * qh" by (simp add: main[symmetric]) from ri2 show "degree qh = degree h" by (fact rat_to_normalized_int_poly) from rat_to_normalized_int_poly(4)[OF ri] False show "degree (smult (content p) rg) = degree g" by auto qed qed lemma rat_to_int_factor_normalized_int_poly: fixes p :: "rat poly" assumes pgh: "p = g * h" and p: "rat_to_normalized_int_poly p = (i,ip)" shows "\ g' h'. ip = g' * h' \ degree g' = degree g" proof - from rat_to_normalized_int_poly[OF p] have p: "p = smult i (map_poly rat_of_int ip)" and i: "i \ 0" by auto from arg_cong[OF p, of "smult (inverse i)", unfolded pgh] i have "map_poly rat_of_int ip = g * smult (inverse i) h" by auto from rat_to_int_factor[OF this] show ?thesis by auto qed (* TODO: move *) lemma irreducible_smult [simp]: fixes c :: "'a :: field" shows "irreducible (smult c p) \ irreducible p \ c \ 0" using irreducible_mult_unit_left[of "[:c:]", simplified] by force text \A polynomial with integer coefficients is irreducible over the rationals, if it is irreducible over the integers.\ theorem irreducible\<^sub>d_int_rat: fixes p :: "int poly" assumes p: "irreducible\<^sub>d p" shows "irreducible\<^sub>d (map_poly rat_of_int p)" proof (rule irreducible\<^sub>dI) from irreducible\<^sub>dD[OF p] have p: "degree p \ 0" and irr: "\ q r. degree q < degree p \ degree r < degree p \ p \ q * r" by auto let ?r = "rat_of_int" let ?rp = "map_poly ?r" from p show rp: "degree (?rp p) > 0" by auto from p have p0: "p \ 0" by auto fix g h :: "rat poly" assume deg: "degree g > 0" "degree g < degree (?rp p)" "degree h > 0" "degree h < degree (?rp p)" and pgh: "?rp p = g * h" from rat_to_int_factor[OF pgh] obtain g' h' where p: "p = g' * h'" and dg: "degree g' = degree g" "degree h' = degree h" by auto from irr[of g' h'] deg[unfolded dg] show False using degree_mult_eq[of g' h'] by (auto simp: p dg) qed corollary irreducible\<^sub>d_rat_to_normalized_int_poly: assumes rp: "rat_to_normalized_int_poly rp = (a, ip)" and ip: "irreducible\<^sub>d ip" shows "irreducible\<^sub>d rp" proof - from rat_to_normalized_int_poly[OF rp] have rp: "rp = smult a (map_poly rat_of_int ip)" and a: "a \ 0" by auto with irreducible\<^sub>d_int_rat[OF ip] show ?thesis by auto qed lemma dvd_content_dvd: assumes dvd: "content f dvd content g" "primitive_part f dvd primitive_part g" shows "f dvd g" proof - let ?cf = "content f" let ?nf = "primitive_part f" let ?cg = "content g" let ?ng = "primitive_part g" have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" unfolding content_times_primitive_part by auto from dvd(1) obtain ch where cg: "?cg = ?cf * ch" unfolding dvd_def by auto from dvd(2) obtain nh where ng: "?ng = ?nf * nh" unfolding dvd_def by auto have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" unfolding content_times_primitive_part[of f] content_times_primitive_part[of g] by auto also have "\ = (smult ?cf ?nf dvd smult ?cf ?nf * smult ch nh)" unfolding cg ng by (metis mult.commute mult_smult_right smult_smult) also have "\" by (rule dvd_triv_left) finally show ?thesis . qed lemma sdiv_poly_smult: "c \ 0 \ sdiv_poly (smult c f) c = f" by (intro poly_eqI, unfold coeff_sdiv_poly coeff_smult, auto) lemma primitive_part_smult_int: fixes f :: "int poly" shows "primitive_part (smult d f) = smult (sgn d) (primitive_part f)" proof (cases "d = 0 \ f = 0") case False obtain cf where cf: "content f = cf" by auto with False have 0: "d \ 0" "f \ 0" "cf \ 0" by auto show ?thesis proof (rule poly_eqI, unfold primitive_part_alt_def coeff_sdiv_poly content_smult_int coeff_smult cf) fix n consider (pos) "d > 0" | (neg) "d < 0" using 0(1) by linarith thus "d * coeff f n div (\d\ * cf) = sgn d * (coeff f n div cf)" proof cases case neg hence "?thesis = (d * coeff f n div - (d * cf) = - (coeff f n div cf))" by auto also have "d * coeff f n div - (d * cf) = - (d * coeff f n div (d * cf))" by (subst dvd_div_neg, insert 0(1), auto simp: cf[symmetric]) also have "d * coeff f n div (d * cf) = coeff f n div cf" using 0(1) by auto finally show ?thesis by simp qed auto qed qed auto +lemma gcd_smult_left: assumes "c \ 0" + shows "gcd (smult c f) g = gcd f (g :: 'b :: {field_gcd} poly)" +proof - + from assms have "normalize c = 1" + by (meson dvd_field_iff is_unit_normalize) + then show ?thesis + by (metis (no_types) Polynomial.normalize_smult gcd.commute gcd.left_commute gcd_left_idem gcd_self smult_1_left) +qed + +lemma gcd_smult_right: "c \ 0 \ gcd f (smult c g) = gcd f (g :: 'b :: {field_gcd} poly)" + using gcd_smult_left[of c g f] by (simp add: gcd.commute) + +lemma gcd_rat_to_gcd_int: "gcd (of_int_poly f :: rat poly) (of_int_poly g) = + smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))" +proof (cases "f = 0 \ g = 0") + case True + thus ?thesis by simp +next + case False + let ?r = rat_of_int + let ?rp = "map_poly ?r" + from False have gcd0: "gcd f g \ 0" by auto + hence lc0: "lead_coeff (gcd f g) \ 0" by auto + hence inv: "inverse (?r (lead_coeff (gcd f g))) \ 0" by auto + show ?thesis + proof (rule sym, rule gcdI, goal_cases) + case 1 + have "gcd f g dvd f" by auto + then obtain h where f: "f = gcd f g * h" unfolding dvd_def by auto + show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF f, of ?rp], simp add: hom_distribs) + next + case 2 + have "gcd f g dvd g" by auto + then obtain h where g: "g = gcd f g * h" unfolding dvd_def by auto + show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF g, of ?rp], simp add: hom_distribs) + next + case (3 h) + show ?case + proof (rule dvd_smult) + obtain ch ph where h: "rat_to_normalized_int_poly h = (ch, ph)" by force + from 3 obtain ff where f: "?rp f = h * ff" unfolding dvd_def by auto + from 3 obtain gg where g: "?rp g = h * gg" unfolding dvd_def by auto + from rat_to_int_factor_explicit[OF f h] obtain f' where f: "f = ph * f'" by blast + from rat_to_int_factor_explicit[OF g h] obtain g' where g: "g = ph * g'" by blast + from f g have "ph dvd gcd f g" by auto + then obtain gg where gcd: "gcd f g = ph * gg" unfolding dvd_def by auto + note * = rat_to_normalized_int_poly[OF h] + show "h dvd ?rp (gcd f g)" unfolding gcd *(1) + by (rule smult_dvd, insert *(2), auto) + qed + next + case 4 + have [simp]: "[:1:] = 1" by simp + show ?case unfolding normalize_poly_def + by (rule poly_eqI, simp) + qed +qed + end