(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) subsection ‹Factoring Rational Polynomials› text ‹We combine the factorization algorithm for integer polynomials with Gauss Lemma to a factorization algorithm for rational polynomials.› theory Factorize_Rat_Poly imports Factorize_Int_Poly begin (*TODO: Move*) interpretation content_hom: monoid_mult_hom "content::'a::{factorial_semiring, semiring_gcd, normalization_semidom_multiplicative} poly ⇒ _" by (unfold_locales, auto simp: content_mult) lemma prod_dvd_1_imp_all_dvd_1: assumes "finite X" and "prod f X dvd 1" and "x ∈ X" shows "f x dvd 1" proof (insert assms, induct rule:finite_induct) case IH: (insert x' X) show ?case proof (cases "x = x'") case True with IH show ?thesis using dvd_trans[of "f x'" "f x' * _" 1] by (metis dvd_triv_left prod.insert) next case False then show ?thesis using IH by (auto intro!: IH(3) dvd_trans[of "prod f X" "_ * prod f X" 1]) qed qed simp context fixes alg :: int_poly_factorization_algorithm begin definition factorize_rat_poly_generic :: "rat poly ⇒ rat × (rat poly × nat) list" where "factorize_rat_poly_generic f = (case rat_to_normalized_int_poly f of (c,g) ⇒ case factorize_int_poly_generic alg g of (d,fs) ⇒ (c * rat_of_int d, map (λ (fi,i). (map_poly rat_of_int fi, i)) fs))" lemma factorize_rat_poly_0[simp]: "factorize_rat_poly_generic 0 = (0,[])" unfolding factorize_rat_poly_generic_def rat_to_normalized_int_poly_def by simp lemma factorize_rat_poly: assumes res: "factorize_rat_poly_generic f = (c,fs)" shows "square_free_factorization f (c,fs)" and "(fi,i) ∈ set fs ⟹ irreducible fi" proof(atomize(full), cases "f=0", goal_cases) case 1 with res show ?case by (auto simp: square_free_factorization_def) next case 2 show ?case proof (unfold square_free_factorization_def split, intro conjI impI allI) let ?r = rat_of_int let ?rp = "map_poly ?r" obtain d g where ri: "rat_to_normalized_int_poly f = (d,g)" by force obtain e gs where fi: "factorize_int_poly_generic alg g = (e,gs)" by force from res[unfolded factorize_rat_poly_generic_def ri fi split] have c: "c = d * ?r e" and fs: "fs = map (λ (fi,i). (?rp fi, i)) gs" by auto from factorize_int_poly[OF fi] have irr: "(fi, i) ∈ set gs ⟹ irreducible fi ∧ content fi = 1" for fi i using irreducible_imp_primitive[of fi] by auto note sff = factorize_int_poly(1)[OF fi] note sff' = square_free_factorizationD[OF sff] { fix n f have "?rp (f ^ n) = (?rp f) ^ n" by (induct n, auto simp: hom_distribs) } note exp = this show dist: "distinct fs" using sff'(5) unfolding fs distinct_map inj_on_def by auto interpret mh: map_poly_inj_idom_hom rat_of_int.. have "f = smult d (?rp g)" using rat_to_normalized_int_poly[OF ri] by auto also have "… = smult d (?rp (smult e (∏(a, i)∈set gs. a ^ Suc i)))" using sff'(1) by simp also have "… = smult c (?rp (∏(a, i)∈set gs. a ^ Suc i))" unfolding c by (simp add: hom_distribs) also have "?rp (∏(a, i)∈set gs. a ^ Suc i) = (∏(a, i)∈set fs. a ^ Suc i)" unfolding prod.distinct_set_conv_list[OF sff'(5)] prod.distinct_set_conv_list[OF dist] unfolding fs by (insert exp, auto intro!: arg_cong[of _ _ "λx. prod_list (map x gs)"] simp: hom_distribs of_int_poly_hom.hom_prod_list) finally show f: "f = smult c (∏(a, i)∈set fs. a ^ Suc i)" by auto { fix a i assume ai: "(a,i) ∈ set fs" from ai obtain A where a: "a = ?rp A" and A: "(A,i) ∈ set gs" unfolding fs by auto fix b j assume "(b,j) ∈ set fs" and diff: "(a,i) ≠ (b,j)" from this(1) obtain B where b: "b = ?rp B" and B: "(B,j) ∈ set gs" unfolding fs by auto from diff[unfolded a b] have "(A,i) ≠ (B,j)" by auto from sff'(3)[OF A B this] show "Rings.coprime a b" by (auto simp add: coprime_iff_gcd_eq_1 gcd_rat_to_gcd_int a b) } { fix fi i assume "(fi,i) ∈ set fs" then obtain gi where fi: "fi = ?rp gi" and gi: "(gi,i) ∈ set gs" unfolding fs by auto from irr[OF gi] have cf_gi: "primitive gi" by auto then have "primitive (?rp gi)" by (auto simp: content_field_poly) note [simp] = irreducible_primitive_connect[OF cf_gi] irreducible_primitive_connect[OF this] show "irreducible fi" using irr[OF gi] fi irreducible⇩_{d}_int_rat[of gi,simplified] by auto then show "degree fi > 0" "square_free fi" unfolding fi by (auto intro: irreducible_imp_square_free) } { assume "f = 0" with ri have *: "d = 1" "g = 0" unfolding rat_to_normalized_int_poly_def by auto with sff'(4)[OF *(2)] show "c = 0" "fs = []" unfolding c fs by auto } qed qed end abbreviation factorize_rat_poly where "factorize_rat_poly ≡ factorize_rat_poly_generic berlekamp_zassenhaus_factorization_algorithm" end