Theory Factorize_Int_Poly
subsection ‹Factoring Arbitrary Integer Polynomials›
text ‹We combine the factorization algorithm for square-free integer polynomials
with a square-free factorization algorithm to
a factorization algorithm for integer polynomials which does not make
any assumptions.›
theory Factorize_Int_Poly
imports
Berlekamp_Zassenhaus
Square_Free_Factorization_Int
begin
hide_const coeff monom
lifting_forget poly.lifting
typedef int_poly_factorization_algorithm = "{alg.
∀ (f :: int poly) fs. square_free f ⟶ degree f > 0 ⟶ alg f = fs ⟶
(f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩d fi))}"
by (rule exI[of _ berlekamp_zassenhaus_factorization],
insert berlekamp_zassenhaus_factorization_irreducible⇩d, auto)
setup_lifting type_definition_int_poly_factorization_algorithm
lift_definition int_poly_factorization_algorithm :: "int_poly_factorization_algorithm ⇒
(int poly ⇒ int poly list)" is "λ x. x" .
lemma int_poly_factorization_algorithm_irreducible⇩d:
assumes "int_poly_factorization_algorithm alg f = fs"
and "square_free f"
and "degree f > 0"
shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩d fi)"
using assms by (transfer, auto)
corollary int_poly_factorization_algorithm_irreducible:
assumes res: "int_poly_factorization_algorithm alg f = fs"
and sf: "square_free f"
and deg: "degree f > 0"
and pr: "primitive f"
shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible fi ∧ degree fi > 0 ∧ primitive fi)"
proof (intro conjI ballI)
note * = int_poly_factorization_algorithm_irreducible⇩d[OF res sf deg]
from * show f: "f = prod_list fs" by auto
fix fi assume fi: "fi ∈ set fs"
with primitive_prod_list[OF pr[unfolded f]] show "primitive fi" by auto
from irreducible_primitive_connect[OF this] * pr[unfolded f] fi
show "irreducible fi" by auto
from * fi show "degree fi > 0" by (auto)
qed
lemma irreducible_imp_square_free:
assumes irr: "irreducible (p::'a::idom poly)" shows "square_free p"
proof(intro square_freeI)
from irr show p0: "p ≠ 0" by auto
fix a assume "a * a dvd p"
then obtain b where paab: "p = a * (a * b)" by (elim dvdE, auto)
assume "degree a > 0"
then have a1: "¬ a dvd 1" by (auto simp: poly_dvd_1)
then have ab1: "¬ a * b dvd 1" using dvd_mult_left by auto
from paab irr a1 ab1 show False by force
qed
lemma not_mem_set_dropWhileD: "x ∉ set (dropWhile P xs) ⟹ x ∈ set xs ⟹ P x"
by (metis dropWhile_append3 in_set_conv_decomp)
lemma primitive_reflect_poly:
fixes f :: "'a :: comm_semiring_1 poly"
shows "primitive (reflect_poly f) = primitive f"
proof-
have "(∀ a ∈ set (coeffs f). x dvd a) ⟷ (∀a ∈ set (dropWhile ((=) 0) (coeffs f)). x dvd a)" for x
by (auto dest: not_mem_set_dropWhileD set_dropWhileD)
then show ?thesis by (auto simp: primitive_def coeffs_reflect_poly)
qed
lemma gcd_list_sub:
assumes "set xs ⊆ set ys" shows "gcd_list ys dvd gcd_list xs"
by (metis Gcd_fin.subset assms semiring_gcd_class.gcd_dvd1)
lemma content_reflect_poly:
"content (reflect_poly f) = content f" (is "?l = ?r")
proof-
have l: "?l = gcd_list (dropWhile ((=) 0) (coeffs f))" (is "_ = gcd_list ?xs")
by (simp add: content_def reflect_poly_def)
have "set ?xs ⊆ set (coeffs f)" by (auto dest: set_dropWhileD)
from gcd_list_sub[OF this]
have "?r dvd gcd_list ?xs" by (simp add: content_def)
with l have rl: "?r dvd ?l" by auto
have "set (coeffs f) ⊆ set (0 # ?xs)" by (auto dest: not_mem_set_dropWhileD)
from gcd_list_sub[OF this]
have "gcd_list ?xs dvd ?r" by (simp add: content_def)
with l have lr: "?l dvd ?r" by auto
from rl lr show "?l = ?r" by (simp add: associated_eqI)
qed
lemma coeff_primitive_part: "content f * coeff (primitive_part f) i = coeff f i"
using arg_cong[OF content_times_primitive_part[of f], of "λf. coeff f _", unfolded coeff_smult].
lemma smult_cancel[simp]:
fixes c :: "'a :: idom"
shows "smult c f = smult c g ⟷ c = 0 ∨ f = g"
proof-
have l: "smult c f = [:c:] * f" by simp
have r: "smult c g = [:c:] * g" by simp
show ?thesis unfolding l r mult_cancel_left by simp
qed
lemma primitive_part_reflect_poly:
fixes f :: "'a :: {semiring_gcd,idom} poly"
shows "primitive_part (reflect_poly f) = reflect_poly (primitive_part f)" (is "?l = ?r")
using content_times_primitive_part[of "reflect_poly f"]
proof-
note content_reflect_poly[of f, symmetric]
also have "smult (content (reflect_poly f)) ?l = reflect_poly f" by simp
also have "... = reflect_poly (smult (content f) (primitive_part f))" by simp
finally show ?thesis unfolding reflect_poly_smult smult_cancel by auto
qed
lemma reflect_poly_eq_zero[simp]:
"reflect_poly f = 0 ⟷ f = 0"
proof
assume "reflect_poly f = 0"
then have "coeff (reflect_poly f) 0 = 0" by simp
then have "lead_coeff f = 0" by simp
then show "f = 0" by simp
qed simp
lemma irreducible⇩d_reflect_poly_main:
fixes f :: "'a :: {idom, semiring_gcd} poly"
assumes nz: "coeff f 0 ≠ 0"
and irr: "irreducible⇩d (reflect_poly f)"
shows "irreducible⇩d f"
proof
let ?r = reflect_poly
from irr degree_reflect_poly_eq[OF nz] show "degree f > 0" by auto
fix g h
assume deg: "degree g < degree f" "degree h < degree f" and fgh: "f = g * h"
from arg_cong[OF fgh, of "λ f. coeff f 0"] nz
have nz': "coeff g 0 ≠ 0" by (auto simp: coeff_mult_0)
note rfgh = arg_cong[OF fgh, of reflect_poly, unfolded reflect_poly_mult[of g h]]
from deg degree_reflect_poly_le[of g] degree_reflect_poly_le[of h] degree_reflect_poly_eq[OF nz]
have "degree (?r h) < degree (?r f)" "degree (?r g) < degree (?r f)" by auto
with irr rfgh show False by auto
qed
lemma irreducible⇩d_reflect_poly:
fixes f :: "'a :: {idom, semiring_gcd} poly"
assumes nz: "coeff f 0 ≠ 0"
shows "irreducible⇩d (reflect_poly f) = irreducible⇩d f"
proof
assume "irreducible⇩d (reflect_poly f)"
from irreducible⇩d_reflect_poly_main[OF nz this] show "irreducible⇩d f" .
next
from nz have nzr: "coeff (reflect_poly f) 0 ≠ 0" by auto
assume "irreducible⇩d f"
with nz have "irreducible⇩d (reflect_poly (reflect_poly f))" by simp
from irreducible⇩d_reflect_poly_main[OF nzr this]
show "irreducible⇩d (reflect_poly f)" .
qed
lemma irreducible_reflect_poly:
fixes f :: "'a :: {idom,semiring_gcd} poly"
assumes nz: "coeff f 0 ≠ 0"
shows "irreducible (reflect_poly f) = irreducible f" (is "?l = ?r")
proof (cases "degree f = 0")
case True then obtain f0 where "f = [:f0:]" by (auto dest: degree0_coeffs)
then show ?thesis by simp
next
case deg: False
show ?thesis
proof (cases "primitive f")
case False
with deg irreducible_imp_primitive[of f] irreducible_imp_primitive[of "reflect_poly f"] nz
show ?thesis unfolding primitive_reflect_poly by auto
next
case cf: True
let ?r = "reflect_poly"
from nz have nz': "coeff (?r f) 0 ≠ 0" by auto
let ?ir = irreducible⇩d
from irreducible⇩d_reflect_poly[OF nz] irreducible⇩d_reflect_poly[OF nz'] nz
have "?ir f ⟷ ?ir (reflect_poly f)" by auto
also have "... ⟷ irreducible (reflect_poly f)"
by (rule irreducible_primitive_connect, unfold primitive_reflect_poly, fact cf)
finally show ?thesis
by (unfold irreducible_primitive_connect[OF cf], auto)
qed
qed
lemma reflect_poly_dvd: "(f :: 'a :: idom poly) dvd g ⟹ reflect_poly f dvd reflect_poly g"
unfolding dvd_def by (auto simp: reflect_poly_mult)
lemma square_free_reflect_poly: fixes f :: "'a :: idom poly"
assumes sf: "square_free f"
and nz: "coeff f 0 ≠ 0"
shows "square_free (reflect_poly f)" unfolding square_free_def
proof (intro allI conjI impI notI)
let ?r = reflect_poly
from sf[unfolded square_free_def]
have f0: "f ≠ 0" and sf: "⋀ q. 0 < degree q ⟹ q * q dvd f ⟹ False" by auto
from f0 nz show "?r f = 0 ⟹ False" by auto
fix q
assume 0: "0 < degree q" and dvd: "q * q dvd ?r f"
from dvd have "q dvd ?r f" by auto
then obtain x where id: "?r f = q * x" by fastforce
{
assume "coeff q 0 = 0"
hence "coeff (?r f) 0 = 0" using id by (auto simp: coeff_mult)
with nz have False by auto
}
hence nzq: "coeff q 0 ≠ 0" by auto
from dvd have "?r (q * q) dvd ?r (?r f)" by (rule reflect_poly_dvd)
also have "?r (?r f) = f" using nz by auto
also have "?r (q * q) = ?r q * ?r q" by (rule reflect_poly_mult)
finally have "?r q * ?r q dvd f" .
from sf[OF _ this] 0 nzq show False by simp
qed
lemma gcd_reflect_poly: fixes f :: "'a :: {factorial_ring_gcd, semiring_gcd_mult_normalize} poly"
assumes nz: "coeff f 0 ≠ 0" "coeff g 0 ≠ 0"
shows "gcd (reflect_poly f) (reflect_poly g) = normalize (reflect_poly (gcd f g))"
proof (rule sym, rule gcdI)
have "gcd f g dvd f" by auto
from reflect_poly_dvd[OF this]
show "normalize (reflect_poly (gcd f g)) dvd reflect_poly f" by simp
have "gcd f g dvd g" by auto
from reflect_poly_dvd[OF this]
show "normalize (reflect_poly (gcd f g)) dvd reflect_poly g" by simp
show "normalize (normalize (reflect_poly (gcd f g))) = normalize (reflect_poly (gcd f g))" by auto
fix h
assume hf: "h dvd reflect_poly f" and hg: "h dvd reflect_poly g"
from hf obtain k where "reflect_poly f = h * k" unfolding dvd_def by auto
from arg_cong[OF this, of "λ f. coeff f 0", unfolded coeff_mult_0] nz(1) have h: "coeff h 0 ≠ 0" by auto
from reflect_poly_dvd[OF hf] reflect_poly_dvd[OF hg]
have "reflect_poly h dvd f" "reflect_poly h dvd g" using nz by auto
hence "reflect_poly h dvd gcd f g" by auto
from reflect_poly_dvd[OF this] h have "h dvd reflect_poly (gcd f g)" by auto
thus "h dvd normalize (reflect_poly (gcd f g))" by auto
qed
lemma linear_primitive_irreducible:
fixes f :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
assumes deg: "degree f = 1" and cf: "primitive f"
shows "irreducible f"
proof (intro irreducibleI)
fix a b assume fab: "f = a * b"
with deg have a0: "a ≠ 0" and b0: "b ≠ 0" by auto
from deg[unfolded fab] degree_mult_eq[OF this] have "degree a = 0 ∨ degree b = 0" by auto
then show "a dvd 1 ∨ b dvd 1"
proof
assume "degree a = 0"
then obtain a0 where a: "a = [:a0:]" by (auto dest:degree0_coeffs)
with fab have "c ∈ set (coeffs f) ⟹ a0 dvd c" for c by (cases "a0 = 0", auto simp: coeffs_smult)
with cf show ?thesis by (auto dest: primitiveD simp: a)
next
assume "degree b = 0"
then obtain b0 where b: "b = [:b0:]" by (auto dest:degree0_coeffs)
with fab have "c ∈ set (coeffs f) ⟹ b0 dvd c" for c by (cases "b0 = 0", auto simp: coeffs_smult)
with cf show ?thesis by (auto dest: primitiveD simp: b)
qed
qed (insert deg, auto simp: poly_dvd_1)
lemma square_free_factorization_last_coeff_nz:
assumes sff: "square_free_factorization f (a, fs)"
and mem: "(fi,i) ∈ set fs"
and nz: "coeff f 0 ≠ 0"
shows "coeff fi 0 ≠ 0"
proof
assume fi: "coeff fi 0 = 0"
note sff_list = square_free_factorization_prod_list[OF sff]
note sff = square_free_factorizationD[OF sff]
from sff_list have "coeff f 0 = a * coeff (∏(a, i)←fs. a ^ i) 0" by simp
with split_list[OF mem] fi sff(2)[OF mem] have "coeff f 0 = 0"
by (cases i, auto simp: coeff_mult)
with nz show False by simp
qed
context
fixes alg :: int_poly_factorization_algorithm
begin
definition main_int_poly_factorization :: "int poly ⇒ int poly list" where
"main_int_poly_factorization f = (let df = degree f
in if df = 1 then [f] else
if abs (coeff f 0) < abs (coeff f df)
then map reflect_poly (int_poly_factorization_algorithm alg (reflect_poly f))
else int_poly_factorization_algorithm alg f)"
definition internal_int_poly_factorization :: "int poly ⇒ int × (int poly × nat) list" where
"internal_int_poly_factorization f = (
case square_free_factorization_int f of
(a,gis) ⇒ (a, [ (h,i) . (g,i) ← gis, h ← main_int_poly_factorization g ])
)"
lemma internal_int_poly_factorization_code[code]: "internal_int_poly_factorization f = (
case square_free_factorization_int f of (a,gis) ⇒
(a, concat (map (λ (g,i). (map (λ f. (f,i)) (main_int_poly_factorization g))) gis)))"
unfolding internal_int_poly_factorization_def by auto
definition factorize_int_last_nz_poly :: "int poly ⇒ int × (int poly × nat) list" where
"factorize_int_last_nz_poly f = (let df = degree f
in if df = 0 then (coeff f 0, []) else if df = 1 then (content f,[(primitive_part f,1)]) else
internal_int_poly_factorization f)"
definition factorize_int_poly_generic :: "int poly ⇒ int × (int poly × nat) list" where
"factorize_int_poly_generic f = (case x_split f of (n,g)
⇒ if g = 0 then (0,[]) else case factorize_int_last_nz_poly g of (a,fs)
⇒ if n = 0 then (a,fs) else (a, (monom 1 1, n) # fs))"
lemma factorize_int_poly_0[simp]: "factorize_int_poly_generic 0 = (0,[])"
unfolding factorize_int_poly_generic_def x_split_def by simp
lemma main_int_poly_factorization:
assumes res: "main_int_poly_factorization f = fs"
and sf: "square_free f"
and df: "degree f > 0"
and nz: "coeff f 0 ≠ 0"
shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩d fi)"
proof (cases "degree f = 1")
case True
with res[unfolded main_int_poly_factorization_def Let_def]
have "fs = [f]" by auto
with True show ?thesis by auto
next
case False
hence *: "(if degree f = 1 then t :: int poly list else e) = e" for t e by auto
note res = res[unfolded main_int_poly_factorization_def Let_def *]
show ?thesis
proof (cases "abs (coeff f 0) < abs (coeff f (degree f))")
case False
with res have "int_poly_factorization_algorithm alg f = fs" by auto
from int_poly_factorization_algorithm_irreducible⇩d[OF this sf df] show ?thesis .
next
case True
let ?f = "reflect_poly f"
from square_free_reflect_poly[OF sf nz] have sf: "square_free ?f" .
from nz df have df: "degree ?f > 0" by simp
from True res obtain gs where fs: "fs = map reflect_poly gs"
and gs: "int_poly_factorization_algorithm alg (reflect_poly f) = gs"
by auto
from int_poly_factorization_algorithm_irreducible⇩d[OF gs sf df]
have id: "reflect_poly ?f = reflect_poly (prod_list gs)" "?f = prod_list gs"
and irr: "⋀ gi. gi ∈ set gs ⟹ irreducible⇩d gi" by auto
from id(1) have f_fs: "f = prod_list fs" unfolding fs using nz
by (simp add: reflect_poly_prod_list)
{
fix fi
assume "fi ∈ set fs"
from this[unfolded fs] obtain gi where gi: "gi ∈ set gs" and fi: "fi = reflect_poly gi" by auto
{
assume "coeff gi 0 = 0"
with id(2) split_list[OF gi] have "coeff ?f 0 = 0"
by (auto simp: coeff_mult)
with nz have False by auto
}
hence nzg: "coeff gi 0 ≠ 0" by auto
from irreducible⇩d_reflect_poly[OF nzg] irr[OF gi] have "irreducible⇩d fi" unfolding fi by simp
}
with f_fs show ?thesis by auto
qed
qed
lemma internal_int_poly_factorization_mem:
assumes f: "coeff f 0 ≠ 0"
and res: "internal_int_poly_factorization f = (c,fs)"
and mem: "(fi,i) ∈ set fs"
shows "irreducible fi" "irreducible⇩d fi" and "primitive fi" and "degree fi ≠ 0" "i ≠ 0"
proof -
obtain a psi where a_psi: "square_free_factorization_int f = (a, psi)"
by force
from square_free_factorization_int[OF this]
have sff: "square_free_factorization f (a, psi)"
and cnt: "⋀ fi i. (fi, i) ∈ set psi ⟹ primitive fi" by blast+
from square_free_factorization_last_coeff_nz[OF sff _ f]
have nz_fi: "⋀ fi i. (fi, i) ∈ set psi ⟹ coeff fi 0 ≠ 0" by auto
note res = res[unfolded internal_int_poly_factorization_def a_psi Let_def split]
obtain fact where fact: "fact = (λ (q,i :: nat). (map (λ f. (f,i)) (main_int_poly_factorization q)))" by auto
from res[unfolded split Let_def]
have c: "c = a" and fs: "fs = concat (map fact psi)"
unfolding fact by auto
note sff' = square_free_factorizationD[OF sff]
from mem[unfolded fs, simplified] obtain d j where psi: "(d,j) ∈ set psi"
and fi: "(fi, i) ∈ set (fact (d,j))" by auto
from square_free_factorizationD(2)[OF sff psi] have "j > 0" by auto
obtain hs where d: "main_int_poly_factorization d = hs" by force
from fi[unfolded split fact] have "j = i" by auto
with ‹j > 0› show "i ≠ 0" by auto
from fi[unfolded d split fact] have fi: "fi ∈ set hs" by auto
from main_int_poly_factorization[OF d _ _ nz_fi[OF psi]] sff'(2)[OF psi] cnt[OF psi]
have main: "d = prod_list hs" "⋀ fi. fi ∈ set hs ⟹ irreducible⇩d fi" by auto
from main split_list[OF fi] have "content fi dvd content d" by auto
with cnt[OF psi] show cnt: "primitive fi" by simp
from main(2)[OF fi] show irr: "irreducible⇩d fi" .
show "irreducible fi"
using irreducible_primitive_connect[OF cnt] irr by blast
from irr show "degree fi ≠ 0" by auto
qed
lemma internal_int_poly_factorization:
assumes f: "coeff f 0 ≠ 0"
and res: "internal_int_poly_factorization f = (c,fs)"
shows "square_free_factorization f (c,fs)"
proof -
obtain a psi where a_psi: "square_free_factorization_int f = (a, psi)"
by force
from square_free_factorization_int[OF this]
have sff: "square_free_factorization f (a, psi)"
and pr: "⋀ fi i. (fi, i) ∈ set psi ⟹ primitive fi" by blast+
obtain fact where fact: "fact = (λ (q,i :: nat). (map (λ f. (f,i)) (main_int_poly_factorization q)))" by auto
from res[unfolded split Let_def]
have c: "c = a" and fs: "fs = concat (map fact psi)"
unfolding fact internal_int_poly_factorization_def a_psi by auto
note sff' = square_free_factorizationD[OF sff]
show ?thesis unfolding square_free_factorization_def split
proof (intro conjI impI allI)
show "f = 0 ⟹ c = 0" "f = 0 ⟹ fs = []" using sff'(4) unfolding c fs by auto
{
fix a i
assume "(a,i) ∈ set fs"
from irreducible_imp_square_free internal_int_poly_factorization_mem[OF f res this]
show "square_free a" "degree a > 0" "i > 0" by auto
}
from square_free_factorization_last_coeff_nz[OF sff _ f]
have nz: "⋀ fi i. (fi, i) ∈ set psi ⟹ coeff fi 0 ≠ 0" by auto
have eq: "f = smult c (∏(a, i)←fs. a ^ i)" unfolding
prod.distinct_set_conv_list[OF sff'(5)]
sff'(1) c
proof (rule arg_cong[where f = "smult a"], unfold fs, insert sff'(2) nz, induct psi)
case (Cons pi psi)
obtain p i where pi: "pi = (p,i)" by force
obtain gs where gs: "main_int_poly_factorization p = gs" by auto
from Cons(2)[of p i] have p: "square_free p" "degree p > 0" unfolding pi by auto
from Cons(3)[of p i] have nz: "coeff p 0 ≠ 0" unfolding pi by auto
from main_int_poly_factorization[OF gs p nz] have pgs: "p = prod_list gs" by auto
have fact: "fact (p,i) = map (λ g. (g,i)) gs" unfolding fact split gs by auto
have cong: "⋀ x y X Y. x = X ⟹ y = Y ⟹ x * y = X * Y" by auto
show ?case unfolding pi list.simps prod_list.Cons split fact concat.simps prod_list.append
map_append
proof (rule cong)
show "p ^ i = (∏(a, i)←map (λg. (g, i)) gs. a ^ i)" unfolding pgs
by (induct gs, auto simp: ac_simps power_mult_distrib)
show "(∏(a, i)←psi. a ^ i) = (∏(a, i)←concat (map fact psi). a ^ i)"
by (rule Cons(1), insert Cons(2-3), auto)
qed
qed simp
{
fix i j l fi
assume *: "j < length psi" "l < length (fact (psi ! j))" "fact (psi ! j) ! l = (fi, i)"
from * have psi: "psi ! j ∈ set psi" by auto
obtain d k where dk: "psi ! j = (d,k)" by force
with * have psij: "psi ! j = (d,i)" unfolding fact split by auto
from sff'(2)[OF psi[unfolded psij]] have d: "square_free d" "degree d > 0" by auto
from nz[OF psi[unfolded psij]] have d0: "coeff d 0 ≠ 0" .
from * psij fact
have bz: "main_int_poly_factorization d = map fst (fact (psi ! j))" by (auto simp: o_def)
from main_int_poly_factorization[OF bz d d0] pr[OF psi[unfolded dk]]
have dhs: "d = prod_list (map fst (fact (psi ! j)))" by auto
from * have mem: "fi ∈ set (map fst (fact (psi ! j)))"
by (metis fst_conv image_eqI nth_mem set_map)
from mem dhs psij d have "∃ d. fi ∈ set (map fst (fact (psi ! j))) ∧
d = prod_list (map fst (fact (psi ! j))) ∧
psi ! j = (d, i) ∧
square_free d" by blast
} note deconstruct = this
{
fix k K fi i Fi I
assume k: "k < length fs" "K < length fs" and f: "fs ! k = (fi, i)" "fs ! K = (Fi, I)"
and diff: "k ≠ K"
from nth_concat_diff[OF k[unfolded fs] diff, folded fs, unfolded length_map]
obtain j l J L where diff: "(j, l) ≠ (J, L)"
and j: "j < length psi" "J < length psi"
and l: "l < length (map fact psi ! j)" "L < length (map fact psi ! J)"
and fs: "fs ! k = map fact psi ! j ! l" "fs ! K = map fact psi ! J ! L" by blast+
hence psij: "psi ! j ∈ set psi" by auto
from j have id: "map fact psi ! j = fact (psi ! j)" "map fact psi ! J = fact (psi ! J)" by auto
note l = l[unfolded id] note fs = fs[unfolded id]
from j have psi: "psi ! j ∈ set psi" "psi ! J ∈ set psi" by auto
from deconstruct[OF j(1) l(1) fs(1)[unfolded f, symmetric]]
obtain d where mem: "fi ∈ set (map fst (fact (psi ! j)))"
and d: "d = prod_list (map fst (fact (psi ! j)))" "psi ! j = (d, i)" "square_free d" by blast
from deconstruct[OF j(2) l(2) fs(2)[unfolded f, symmetric]]
obtain D where Mem: "Fi ∈ set (map fst (fact (psi ! J)))"
and D: "D = prod_list (map fst (fact (psi ! J)))" "psi ! J = (D, I)" "square_free D" by blast
from pr[OF psij[unfolded d(2)]] have cnt: "primitive d" .
have "coprime fi Fi"
proof (cases "J = j")
case False
from sff'(5) False j have "(d,i) ≠ (D,I)"
unfolding distinct_conv_nth d(2)[symmetric] D(2)[symmetric] by auto
from sff'(3)[OF psi[unfolded d(2) D(2)] this]
have cop: "coprime d D" by auto
from prod_list_dvd[OF mem, folded d(1)] have fid: "fi dvd d" by auto
from prod_list_dvd[OF Mem, folded D(1)] have FiD: "Fi dvd D" by auto
from coprime_divisors[OF fid FiD] cop show ?thesis by simp
next
case True note id = this
from id diff have diff: "l ≠ L" by auto
obtain bz where bz: "bz = map fst (fact (psi ! j))" by auto
from fs[unfolded f] l
have fi: "fi = bz ! l" "Fi = bz ! L"
unfolding id bz by (metis fst_conv nth_map)+
from d[folded bz] have sf: "square_free (prod_list bz)" by auto
from d[folded bz] cnt have cnt: "content (prod_list bz) = 1" by auto
from l have l: "l < length bz" "L < length bz" unfolding bz id by auto
from l fi have "fi ∈ set bz" by auto
from content_dvd_1[OF cnt prod_list_dvd[OF this]] have cnt: "content fi = 1" .
obtain g where g: "g = gcd fi Fi" by auto
have g': "g dvd fi" "g dvd Fi" unfolding g by auto
define bef where "bef = take l bz"
define aft where "aft = drop (Suc l) bz"
from id_take_nth_drop[OF l(1)] l have bz: "bz = bef @ fi # aft" and bef: "length bef = l"
unfolding bef_def aft_def fi by auto
with l diff have mem: "Fi ∈ set (bef @ aft)" unfolding fi(2) by (auto simp: nth_append)
from split_list[OF this] obtain Bef Aft where ba: "bef @ aft = Bef @ Fi # Aft" by auto
have "prod_list bz = fi * prod_list (bef @ aft)" unfolding bz by simp
also have "prod_list (bef @ aft) = Fi * prod_list (Bef @ Aft)" unfolding ba by auto
finally have "fi * Fi dvd prod_list bz" by auto
with g' have "g * g dvd prod_list bz" by (meson dvd_trans mult_dvd_mono)
with sf[unfolded square_free_def] have deg: "degree g = 0" by auto
from content_dvd_1[OF cnt g'(1)] have cnt: "content g = 1" .
from degree0_coeffs[OF deg] obtain c where gc: "g = [: c :]" by auto
from cnt[unfolded gc content_def, simplified] have "abs c = 1"
by (cases "c = 0", auto)
with g gc have "gcd fi Fi ∈ {1,-1}" by fastforce
thus "coprime fi Fi"
by (auto intro!: gcd_eq_1_imp_coprime)
(metis dvd_minus_iff dvd_refl is_unit_gcd_iff one_neq_neg_one)
qed
} note cop = this
show dist: "distinct fs" unfolding distinct_conv_nth
proof (intro impI allI)
fix k K
assume k: "k < length fs" "K < length fs" and diff: "k ≠ K"
obtain fi i Fi I where f: "fs ! k = (fi,i)" "fs ! K = (Fi,I)" by force+
from cop[OF k f diff] have cop: "coprime fi Fi" .
from k(1) f(1) have "(fi,i) ∈ set fs" unfolding set_conv_nth by force
from internal_int_poly_factorization_mem[OF assms(1) res this] have "degree fi > 0" by auto
hence "¬ is_unit fi" by (simp add: poly_dvd_1)
with cop coprime_id_is_unit[of fi] have "fi ≠ Fi" by auto
thus "fs ! k ≠ fs ! K" unfolding f by auto
qed
show "f = smult c (∏(a, i)∈set fs. a ^ i)" unfolding eq
prod.distinct_set_conv_list[OF dist] by simp
fix fi i Fi I
assume mem: "(fi, i) ∈ set fs" "(Fi,I) ∈ set fs" and diff: "(fi, i) ≠ (Fi, I)"
then obtain k K where k: "k < length fs" "K < length fs"
and f: "fs ! k = (fi, i)" "fs ! K = (Fi, I)" unfolding set_conv_nth by auto
with diff have diff: "k ≠ K" by auto
from cop[OF k f diff] show "Rings.coprime fi Fi" by auto
qed
qed
lemma factorize_int_last_nz_poly: assumes res: "factorize_int_last_nz_poly f = (c,fs)"
and nz: "coeff f 0 ≠ 0"
shows "square_free_factorization f (c,fs)"
"(fi,i) ∈ set fs ⟹ irreducible fi"
"(fi,i) ∈ set fs ⟹ degree fi ≠ 0"
proof (atomize(full))
from nz have lz: "lead_coeff f ≠ 0" by auto
note res = res[unfolded factorize_int_last_nz_poly_def Let_def]
consider (0) "degree f = 0"
| (1) "degree f = 1"
| (2) "degree f > 1" by linarith
then show "square_free_factorization f (c,fs) ∧ ((fi,i) ∈ set fs ⟶ irreducible fi) ∧ ((fi,i) ∈ set fs ⟶ degree fi ≠ 0)"
proof cases
case 0
from degree0_coeffs[OF 0] obtain a where f: "f = [:a:]" by auto
from res show ?thesis unfolding square_free_factorization_def f by auto
next
case 1
then have irr: "irreducible (primitive_part f)"
by (auto intro!: linear_primitive_irreducible content_primitive_part)
from irreducible_imp_square_free[OF irr] have sf: "square_free (primitive_part f)" .
from 1 have f0: "f ≠ 0" by auto
from res irr sf f0 show ?thesis unfolding square_free_factorization_def by (auto simp: 1)
next
case 2
with res have "internal_int_poly_factorization f = (c,fs)" by auto
from internal_int_poly_factorization[OF nz this] internal_int_poly_factorization_mem[OF nz this]
show ?thesis by auto
qed
qed
lemma factorize_int_poly: assumes res: "factorize_int_poly_generic f = (c,fs)"
shows "square_free_factorization f (c,fs)"
"(fi,i) ∈ set fs ⟹ irreducible fi"
"(fi,i) ∈ set fs ⟹ degree fi ≠ 0"
proof (atomize(full))
obtain n g where xs: "x_split f = (n,g)" by force
obtain d hs where fact: "factorize_int_last_nz_poly g = (d,hs)" by force
from res[unfolded factorize_int_poly_generic_def xs split fact]
have res: "(if g = 0 then (0, []) else if n = 0 then (d, hs) else (d, (monom 1 1, n) # hs)) = (c, fs)" .
note xs = x_split[OF xs]
show "square_free_factorization f (c,fs) ∧ ((fi,i) ∈ set fs ⟶ irreducible fi) ∧ ((fi,i) ∈ set fs ⟶ degree fi ≠ 0)"
proof (cases "g = 0")
case True
hence "f = 0" "c = 0" "fs = []" using res xs by auto
thus ?thesis unfolding square_free_factorization_def by auto
next
case False
with xs have "¬ monom 1 1 dvd g" by auto
hence "coeff g 0 ≠ 0" by (simp add: monom_1_dvd_iff')
note fact = factorize_int_last_nz_poly[OF fact this]
let ?x = "monom 1 1 :: int poly"
have x: "content ?x = 1 ∧ lead_coeff ?x = 1 ∧ degree ?x = 1"
by (auto simp add: degree_monom_eq monom_Suc content_def)
from res False have res: "(if n = 0 then (d, hs) else (d, (?x, n) # hs)) = (c, fs)" by auto
show ?thesis
proof (cases n)
case 0
with res xs have id: "fs = hs" "c = d" "f = g" by auto
from fact show ?thesis unfolding id by auto
next
case (Suc m)
with res have id: "c = d" "fs = (?x,Suc m) # hs" by auto
from Suc xs have fg: "f = monom 1 (Suc m) * g" and dvd: "¬ ?x dvd g" by auto
from x linear_primitive_irreducible[of ?x] have irr: "irreducible ?x" by auto
from irreducible_imp_square_free[OF this] have sfx: "square_free ?x" .
from irr fact have one: "(fi, i) ∈ set fs ⟶ irreducible fi ∧ degree fi ≠ 0" unfolding id by (auto simp: degree_monom_eq)
have fg: "f = ?x ^ n * g" unfolding fg Suc by (metis x_pow_n)
from x have degx: "degree ?x = 1" by simp
note sf = square_free_factorizationD[OF fact(1)]
{
fix a i
assume ai: "(a,i) ∈ set hs"
with sf(4) have g0: "g ≠ 0" by auto
from sf(2)[OF ai] have i: "i ≠ 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 fact(1)] hs
by (rule dvd_smult, insert i, cases i, auto 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 (auto, 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 "Suc m"]
have nmem: "(?x,Suc m) ∉ set hs" by auto
hence eq: "?x ^ n * g = smult d (∏(a, i)∈set fs. a ^ i)"
unfolding sf(1) unfolding id Suc by simp
have eq0: "?x ^ n * g = 0 ⟷ g = 0" by simp
have "square_free_factorization f (d,fs)" unfolding fg id(1) 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" "i > 0" using sf(2) sfx degx unfolding id 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 id by auto
thus "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 ⟹ d = 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 id by auto
qed
thus ?thesis using one unfolding id by auto
qed
qed
qed
end
lift_definition berlekamp_zassenhaus_factorization_algorithm :: int_poly_factorization_algorithm
is berlekamp_zassenhaus_factorization
using berlekamp_zassenhaus_factorization_irreducible⇩d by blast
abbreviation factorize_int_poly where
"factorize_int_poly ≡ factorize_int_poly_generic berlekamp_zassenhaus_factorization_algorithm"
end