# Theory Factors_of_Int_Poly

```section ‹Getting Small Representative Polynomials via Factorization›

text ‹In this theory we import a factorization algorithm for
integer polynomials to turn a representing polynomial of some algebraic number into
a list of irreducible polynomials where exactly one list element
represents the same number. Moreover, we prove
that the certain polynomial operations preserve irreducibility, so that
no factorization is required.›

theory Factors_of_Int_Poly
imports
Berlekamp_Zassenhaus.Factorize_Int_Poly
Algebraic_Numbers_Prelim
begin

lemma degree_of_gcd: "degree (gcd q r) ≠ 0 ⟷
degree (gcd (of_int_poly q :: 'a :: {field_char_0, field_gcd} poly) (of_int_poly r)) ≠ 0"
proof -
let ?r = "of_rat :: rat ⇒ 'a"
interpret rpoly: field_hom' ?r
by (unfold_locales, auto simp: of_rat_add of_rat_mult)
{
fix p
have "of_int_poly p = map_poly (?r o of_int) p" unfolding o_def
by auto
also have "… = map_poly ?r (map_poly of_int p)"
by (subst map_poly_map_poly, auto)
finally have "of_int_poly p = map_poly ?r (map_poly of_int p)" .
} note id = this
show ?thesis unfolding id by (fold hom_distribs, simp add: gcd_rat_to_gcd_int)
qed

definition factors_of_int_poly :: "int poly ⇒ int poly list" where
"factors_of_int_poly p = map (abs_int_poly o fst) (snd (factorize_int_poly p))"

lemma factors_of_int_poly_const: assumes "degree p = 0"
shows "factors_of_int_poly p = []"
proof -
from degree0_coeffs[OF assms] obtain a where p: "p = [: a :]" by auto
show ?thesis unfolding p factors_of_int_poly_def
factorize_int_poly_generic_def x_split_def
by (cases "a = 0", auto simp add: Let_def factorize_int_last_nz_poly_def)
qed

lemma factors_of_int_poly:
defines "rp ≡ ipoly :: int poly ⇒ 'a :: {field_gcd,field_char_0} ⇒ 'a"
assumes "factors_of_int_poly p = qs"
shows "⋀ q. q ∈ set qs ⟹ irreducible q ∧ lead_coeff q > 0 ∧ degree q ≤ degree p ∧ degree q ≠ 0"
"p ≠ 0 ⟹ rp p x = 0 ⟷ (∃ q ∈ set qs. rp q x = 0)"
"p ≠ 0 ⟹ rp p x = 0 ⟹ ∃! q ∈ set qs. rp q x = 0"
"distinct qs"
proof -
obtain c qis where factt: "factorize_int_poly p = (c,qis)" by force
from assms[unfolded factors_of_int_poly_def factt]
have qs: "qs = map (abs_int_poly ∘ fst) (snd (c, qis))" by auto
note fact = factorize_int_poly(1)[OF factt]
note fact_mem = factorize_int_poly(2,3)[OF factt]
have sqf: "square_free_factorization p (c, qis)" by (rule fact(1))
note sff = square_free_factorizationD[OF sqf]
have sff': "p = Polynomial.smult c (∏(a, i)← qis. a ^ Suc i)"
unfolding sff(1) prod.distinct_set_conv_list[OF sff(5)] ..
{
fix q
assume q: "q ∈ set qs"
then obtain r i where qi: "(r,i) ∈ set qis" and qr: "q = abs_int_poly r" unfolding qs by auto
from split_list[OF qi] obtain qis1 qis2 where qis: "qis = qis1 @ (r,i) # qis2" by auto
have dvd: "r dvd p" unfolding sff' qis dvd_def
by (intro exI[of _ "smult c (r ^ i * (∏(a, i)←qis1 @  qis2. a ^ Suc i))"], auto)
from fact_mem[OF qi] have r0: "r ≠ 0" by auto
from qi factt have p: "p ≠ 0" by (cases p, auto)
with dvd have deg: "degree r ≤ degree p" by (metis dvd_imp_degree_le)
with fact_mem[OF qi] r0
show "irreducible q ∧ lead_coeff q > 0 ∧ degree q ≤ degree p ∧ degree q ≠ 0"
} note * = this
show "distinct qs" unfolding distinct_conv_nth
proof (intro allI impI)
fix i j
assume "i < length qs" "j < length qs" and diff: "i ≠ j"
hence ij: "i < length qis" "j < length qis"
and id: "qs ! i = abs_int_poly (fst (qis ! i))" "qs ! j = abs_int_poly (fst (qis ! j))" unfolding qs by auto
obtain qi I where qi: "qis ! i = (qi, I)" by force
obtain qj J where qj: "qis ! j = (qj, J)" by force
from sff(5)[unfolded distinct_conv_nth, rule_format, OF ij diff] qi qj
have diff: "(qi, I) ≠ (qj, J)" by auto
from ij qi qj have "(qi, I) ∈ set qis" "(qj, J) ∈ set qis" unfolding set_conv_nth by force+
from sff(3)[OF this diff] sff(2) this
have cop: "coprime qi qj" "degree qi ≠ 0" "degree qj ≠ 0" by auto
note i = cf_pos_poly_main[of qi, unfolded smult_prod monom_0]
note j = cf_pos_poly_main[of qj, unfolded smult_prod monom_0]
from cop(2) i have deg: "degree (qs ! i) ≠ 0" by (auto simp: id qi)
have cop: "coprime (qs ! i) (qs ! j)"
unfolding id qi qj fst_conv
using cop
unfolding i j by (auto simp: sgn_eq_0_iff)
show "qs ! i ≠ qs ! j"
proof
assume id: "qs ! i = qs ! j"
have "degree (gcd (qs ! i) (qs ! j)) = degree (qs ! i)"  unfolding id by simp
also have "… ≠ 0" using deg by simp
finally show False using cop by simp
qed
qed
assume p: "p ≠ 0"
from fact(1) p have c: "c ≠ 0" using sff(1) by auto
let ?r = "of_int :: int ⇒ 'a"
let ?rp = "map_poly ?r"
have rp: "⋀ x p. rp p x = 0 ⟷ poly (?rp p) x = 0" unfolding rp_def ..
have "rp p x = 0 ⟷ rp (∏(x, y)←qis. x ^ Suc y) x = 0" unfolding sff'(1)
unfolding rp hom_distribs using c by simp
also have "… = (∃ (q,i) ∈set qis. poly (?rp (q ^ Suc i)) x = 0)"
unfolding qs rp of_int_poly_hom.hom_prod_list poly_prod_list_zero_iff set_map by fastforce
also have "… = (∃ (q,i) ∈set qis. poly (?rp q) x = 0)"
unfolding of_int_poly_hom.hom_power poly_power_zero_iff by auto
also have "… = (∃ q ∈ fst ` set qis. poly (?rp q) x = 0)" by force
also have "… = (∃ q ∈ set qs. rp q x = 0)" unfolding rp qs snd_conv o_def bex_simps set_map
by simp
finally show iff: "rp p x = 0 ⟷ (∃ q ∈ set qs. rp q x = 0)" by auto
assume "rp p x = 0"
with iff obtain q where q: "q ∈ set qs" and rtq: "rp q x = 0" by auto
then obtain i q' where qi: "(q',i) ∈ set qis" and qq': "q = abs_int_poly q'" unfolding qs by auto
show "∃! q ∈ set qs. rp q x = 0"
proof (intro ex1I, intro conjI, rule q, rule rtq, clarify)
fix r
assume "r ∈ set qs" and rtr: "rp r x = 0"
then obtain j r' where rj: "(r',j) ∈ set qis" and rr': "r = abs_int_poly r'" unfolding qs by auto
from rtr rtq have rtr: "rp r' x = 0" and rtq: "rp q' x = 0"
unfolding rp rr' qq' by auto
from rtr rtq have "[:-x,1:] dvd ?rp q'" "[:-x,1:] dvd ?rp r'" unfolding rp
by (auto simp: poly_eq_0_iff_dvd)
hence "[:-x,1:] dvd gcd (?rp q') (?rp r')" by simp
hence "gcd (?rp q') (?rp r') = 0 ∨ degree (gcd (?rp q') (?rp r')) ≠ 0"
by (metis is_unit_gcd_iff is_unit_iff_degree is_unit_pCons_iff one_poly_eq_simps(1))
hence "gcd q' r' = 0 ∨ degree (gcd q' r') ≠ 0"
unfolding gcd_eq_0_iff degree_of_gcd[of q' r',symmetric] by auto
hence "¬ coprime q' r'" by auto
with sff(3)[OF qi rj] have "q' = r'" by auto
thus "r = q" unfolding rr' qq' by simp
qed
qed

lemma factors_int_poly_represents:
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes p: "p represents x"
shows "∃ q ∈ set (factors_of_int_poly p).
q represents x ∧ irreducible q ∧ lead_coeff q > 0  ∧ degree q ≤ degree p"
proof -
from representsD[OF p] have p: "p ≠ 0" and rt: "ipoly p x = 0" by auto
note fact = factors_of_int_poly[OF refl]
from fact(2)[OF p, of x] rt obtain q where q: "q ∈ set (factors_of_int_poly p)" and
rt: "ipoly q x = 0" by auto
from fact(1)[OF q] rt show ?thesis
by (intro bexI[OF _ q], auto simp: represents_def irreducible_def)
qed

corollary irreducible_represents_imp_degree:
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes "irreducible f" and "f represents x" and "g represents x"
shows "degree f ≤ degree g"
proof -
from factors_of_int_poly(1)[OF refl, of _ g] factors_of_int_poly(3)[OF refl, of g x]
assms(3) obtain h where *: "h represents x" "degree h ≤ degree g" "irreducible h"
by blast
let ?af = "abs_int_poly f"
let ?ah = "abs_int_poly h"
from assms have af: "irreducible ?af" "?af represents x" "lead_coeff ?af > 0" by fastforce+
from * have ah: "irreducible ?ah" "?ah represents x" "lead_coeff ?ah > 0" by fastforce+
from algebraic_imp_represents_unique[of x] af ah have id: "?af = ?ah"
unfolding algebraic_iff_represents by blast
show ?thesis using arg_cong[OF id, of degree] ‹degree h ≤ degree g› by simp
qed

lemma irreducible_preservation:
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes irr: "irreducible p"
and x: "p represents x"
and y: "q represents y"
and deg: "degree p ≥ degree q"
and f: "⋀ q. q represents y ⟹ (f q) represents x ∧ degree (f q) ≤ degree q"
and pr: "primitive q"
shows "irreducible q"
proof (rule ccontr)
define pp where "pp = abs_int_poly p"
have dp: "degree p ≠ 0" using x by (rule represents_degree)
have dq: "degree q ≠ 0" using y by (rule represents_degree)
from dp have p0: "p ≠ 0" by auto
from x deg irr p0
have irr: "irreducible pp" and x: "pp represents x" and
deg: "degree pp ≥ degree q" and cf_pos: "lead_coeff pp > 0"
unfolding pp_def lead_coeff_abs_int_poly by (auto intro!: representsI)
from x have ax: "algebraic x" unfolding algebraic_altdef_ipoly represents_def by blast
assume "¬ ?thesis"
from this irreducible_connect_int[of q] pr have "¬ irreducible⇩d q" by auto
from this dq obtain r where
r: "degree r ≠ 0" "degree r < degree q" and "r dvd q" by auto
then obtain rr where q: "q = r * rr" unfolding dvd_def by auto
have "degree q = degree r + degree rr" using dq unfolding q
by (subst degree_mult_eq, auto)
with r have rr: "degree rr ≠ 0" "degree rr < degree q" by auto
from representsD(2)[OF y, unfolded q hom_distribs]
have "ipoly r y = 0 ∨ ipoly rr y = 0" by auto
with r rr have "r represents y ∨ rr represents y" unfolding represents_def by auto
with r rr obtain r where r: "r represents y" "degree r < degree q" by blast
from f[OF r(1)] deg r(2) obtain r where r: "r represents x" "degree r < degree pp" by auto
from factors_int_poly_represents[OF r(1)] r(2) obtain r where
r: "r represents x" "irreducible r" "lead_coeff r > 0" and deg: "degree r < degree pp" by force
from algebraic_imp_represents_unique[OF ax] r irr cf_pos x have "r = pp" by auto
with deg show False by auto
qed

declare irreducible_const_poly_iff [simp]

lemma poly_uminus_irreducible:
assumes p: "irreducible (p :: int poly)" and deg: "degree p ≠ 0"
shows "irreducible (poly_uminus p)"
proof-
from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto
from represents_uminus[OF x]
have y: "poly_uminus p represents (- x)" .
show ?thesis
proof (rule irreducible_preservation[OF p x y], force)
from deg irreducible_imp_primitive[OF p] have "primitive p" by auto
then show "primitive (poly_uminus p)" by simp
fix q
assume "q represents (- x)"
from represents_uminus[OF this] have "(poly_uminus q) represents x" by simp
thus "(poly_uminus q) represents x ∧ degree (poly_uminus q) ≤ degree q" by auto
qed
qed

lemma reflect_poly_irreducible:
fixes x :: "'a :: {field_char_0,field_gcd}"
assumes p: "irreducible p" and x: "p represents x" and x0: "x ≠ 0"
shows "irreducible (reflect_poly p)"
proof -
from represents_inverse[OF x0 x]
have y: "(reflect_poly p) represents (inverse x)" by simp
from x0 have ix0: "inverse x ≠ 0" by auto
show ?thesis
proof (rule irreducible_preservation[OF p x y])
from x irreducible_imp_primitive[OF p]
show "primitive (reflect_poly p)" by (auto simp: content_reflect_poly)
fix q
assume "q represents (inverse x)"
from represents_inverse[OF ix0 this] have "(reflect_poly q) represents x" by simp
with degree_reflect_poly_le
show "(reflect_poly q) represents x ∧ degree (reflect_poly q) ≤ degree q" by auto
qed (insert p, auto simp: degree_reflect_poly_le)
qed

assumes p: "irreducible p" and deg: "degree p ≠ 0"
shows "irreducible (cf_pos_poly (poly_add_rat r p))"
proof -
from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto
have y: "cf_pos_poly (poly_add_rat r p) represents (of_rat r + x)" by simp
show ?thesis
proof (rule irreducible_preservation[OF p x y], force)
fix q
assume "q represents (of_rat r + x)"
from represents_add_rat[OF this, of "- r"] have "(poly_add_rat (- r) q) represents x" by (simp add: of_rat_minus)
thus "(poly_add_rat (- r) q) represents x ∧ degree (poly_add_rat (- r) q) ≤ degree q" by auto
qed (insert p, auto)
qed

lemma poly_mult_rat_irreducible:
assumes p: "irreducible p" and deg: "degree p ≠ 0" and r: "r ≠ 0"
shows "irreducible (cf_pos_poly (poly_mult_rat r p))"
proof -
from deg_nonzero_represents[OF deg] obtain x :: complex where x: "p represents x" by auto
from represents_mult_rat[OF r x]
have y: "cf_pos_poly (poly_mult_rat r p) represents (of_rat r * x)" by simp
show ?thesis
proof (rule irreducible_preservation[OF p x y], force simp: r)
fix q
from r have r': "inverse r ≠ 0" by simp
assume "q represents (of_rat r * x)"
from represents_mult_rat[OF r' this] have "(poly_mult_rat (inverse r) q) represents x" using r