Theory Factorize_Rat_Poly
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
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 ^ i)))" using sff'(1) by simp
also have "… = smult c (?rp (∏(a, i)∈set gs. a ^ i))" unfolding c by (simp add: hom_distribs)
also have "?rp (∏(a, i)∈set gs. a ^ i) = (∏(a, i)∈set fs. a ^ 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 ^ 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 sff'(2)[OF gi] show "0 < i" 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