(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) subsection ‹Result is Unique› text ‹We combine the finite field factorization algorithm with Hensel-lifting to obtain factorizations mod $p^n$. Moreover, we prove results on unique-factorizations in mod $p^n$ which admit to extend the uniqueness result for binary Hensel-lifting to the general case. As a consequence, our factorization algorithm will produce unique factorizations mod $p^n$.› theory Berlekamp_Hensel imports Finite_Field_Factorization_Record_Based Hensel_Lifting begin hide_const coeff monom definition berlekamp_hensel :: "int ⇒ nat ⇒ int poly ⇒ int poly list" where "berlekamp_hensel p n f = (case finite_field_factorization_int p f of (_,fs) ⇒ hensel_lifting p n f fs)" text ‹Finite field factorization in combination with Hensel-lifting delivers factorization modulo $p^k$ where factors are irreducible modulo $p$. Assumptions: input polynomial is square-free modulo $p$.› context poly_mod_prime begin lemma berlekamp_hensel_main: assumes n: "n ≠ 0" and res: "berlekamp_hensel p n f = gs" and cop: "coprime (lead_coeff f) p" and sf: "square_free_m f" and berl: "finite_field_factorization_int p f = (c,fs)" shows "poly_mod.factorization_m (p ^ n) f (lead_coeff f, mset gs) ― ‹factorization mod ‹p^n››" and "sort (map degree fs) = sort (map degree gs)" and "⋀ g. g ∈ set gs ⟹ monic g ∧ poly_mod.Mp (p^n) g = g ∧ ― ‹monic and normalized› poly_mod.irreducible_m p g ∧ ― ‹irreducibility even mod ‹p›› poly_mod.degree_m p g = degree g ― ‹mod ‹p› does not change degree of ‹g››" proof - from res[unfolded berlekamp_hensel_def berl split] have hen: "hensel_lifting p n f fs = gs" . note bh = finite_field_factorization_int[OF sf berl] from bh have "poly_mod.factorization_m p f (c, mset fs)" "c ∈ {0..<p}" "(∀fi∈set fs. set (coeffs fi) ⊆ {0..<p})" by (auto simp: poly_mod.unique_factorization_m_alt_def) note hen = hensel_lifting[OF n hen cop sf, OF this] show "poly_mod.factorization_m (p ^ n) f (lead_coeff f, mset gs)" "sort (map degree fs) = sort (map degree gs)" "⋀ g. g ∈ set gs ⟹ monic g ∧ poly_mod.Mp (p^n) g = g ∧ poly_mod.irreducible_m p g ∧ poly_mod.degree_m p g = degree g" using hen by auto qed theorem berlekamp_hensel: assumes cop: "coprime (lead_coeff f) p" and sf: "square_free_m f" and res: "berlekamp_hensel p n f = gs" and n: "n ≠ 0" shows "poly_mod.factorization_m (p^n) f (lead_coeff f, mset gs) ― ‹factorization mod ‹p^n››" and "⋀ g. g ∈ set gs ⟹ poly_mod.Mp (p^n) g = g ∧ poly_mod.irreducible_m p g ― ‹normalized and ‹irreducible› even mod ‹p››" proof - obtain c fs where "finite_field_factorization_int p f = (c,fs)" by force from berlekamp_hensel_main[OF n res cop sf this] show "poly_mod.factorization_m (p^n) f (lead_coeff f, mset gs)" "⋀ g. g ∈ set gs ⟹ poly_mod.Mp (p^n) g = g ∧ poly_mod.irreducible_m p g" by auto qed lemma berlekamp_and_hensel_separated: assumes cop: "coprime (lead_coeff f) p" and sf: "square_free_m f" and res: "hensel_lifting p n f fs = gs" and berl: "finite_field_factorization_int p f = (c,fs)" and n: "n ≠ 0" shows "berlekamp_hensel p n f = gs" and "sort (map degree fs) = sort (map degree gs)" proof - show "berlekamp_hensel p n f = gs" unfolding res[symmetric] berlekamp_hensel_def hensel_lifting_def berl split Let_def .. from berlekamp_hensel_main[OF n this cop sf berl] show "sort (map degree fs) = sort (map degree gs)" by auto qed end lemma prime_cop_exp_poly_mod: assumes prime: "prime p" and cop: "coprime c p" and n: "n ≠ 0" shows "poly_mod.M (p^n) c ∈ {1 ..< p^n}" proof - from prime have p1: "p > 1" by (simp add: prime_int_iff) interpret poly_mod_2 "p^n" unfolding poly_mod_2_def using p1 n by simp from cop p1 m1 have "M c ≠ 0" by (auto simp add: M_def) moreover have "M c < p^n" "M c ≥ 0" unfolding M_def using m1 by auto ultimately show ?thesis by auto qed context poly_mod_2 begin context fixes p :: int assumes prime: "prime p" begin interpretation p: poly_mod_prime p using prime by unfold_locales lemma coprime_lead_coeff_factor: assumes "coprime (lead_coeff (f * g)) p" shows "coprime (lead_coeff f) p" "coprime (lead_coeff g) p" proof - { fix f g assume cop: "coprime (lead_coeff (f * g)) p" from this[unfolded lead_coeff_mult] have "coprime (lead_coeff f) p" using prime by simp } from this[OF assms] this[of g f] assms show "coprime (lead_coeff f) p" "coprime (lead_coeff g) p" by (auto simp: ac_simps) qed lemma unique_factorization_m_factor: assumes uf: "unique_factorization_m (f * g) (c,hs)" and cop: "coprime (lead_coeff (f * g)) p" and sf: "p.square_free_m (f * g)" and n: "n ≠ 0" and m: "m = p^n" shows "∃ fs gs. unique_factorization_m f (lead_coeff f,fs) ∧ unique_factorization_m g (lead_coeff g,gs) ∧ Mf (c,hs) = Mf (lead_coeff f * lead_coeff g, fs + gs) ∧ image_mset Mp fs = fs ∧ image_mset Mp gs = gs" proof - from prime have p1: "1 < p" by (simp add: prime_int_iff) interpret p: poly_mod_2 p by (standard, rule p1) note sf = p.square_free_m_factor[OF sf] note cop = coprime_lead_coeff_factor[OF cop] from cop have copm: "coprime (lead_coeff f) m" "coprime (lead_coeff g) m" by (simp_all add: m) have df: "degree_m f = degree f" by (rule degree_m_eq[OF _ m1], insert copm(1) m1, auto) have dg: "degree_m g = degree g" by (rule degree_m_eq[OF _ m1], insert copm(2) m1, auto) define fs where "fs ≡ mset (berlekamp_hensel p n f)" define gs where "gs ≡ mset (berlekamp_hensel p n g)" from p.berlekamp_hensel[OF cop(1) sf(1) refl n, folded m] have f: "factorization_m f (lead_coeff f,fs)" and f_id: "⋀ f. f ∈# fs ⟹ Mp f = f" unfolding fs_def by auto from p.berlekamp_hensel[OF cop(2) sf(2) refl n, folded m] have g: "factorization_m g (lead_coeff g,gs)" and g_id: "⋀ f. f ∈# gs ⟹ Mp f = f" unfolding gs_def by auto from factorization_m_prod[OF f g] uf[unfolded unique_factorization_m_alt_def] have eq: "Mf (lead_coeff f * lead_coeff g, fs + gs) = Mf (c,hs)" by blast have uff: "unique_factorization_m f (lead_coeff f,fs)" proof (rule unique_factorization_mI[OF f]) fix e ks assume "factorization_m f (e,ks)" from factorization_m_prod[OF this g] uf[unfolded unique_factorization_m_alt_def] factorization_m_lead_coeff[OF this, unfolded degree_m_eq_lead_coeff[OF df]] have "Mf (e * lead_coeff g, ks + gs) = Mf (c,hs)" and e: "M (lead_coeff f) = M e" by blast+ from this[folded eq, unfolded Mf_def split] have ks: "image_mset Mp ks = image_mset Mp fs" by auto show "Mf (e, ks) = Mf (lead_coeff f, fs)" unfolding Mf_def split ks e by simp qed have idf: "image_mset Mp fs = fs" using f_id by (induct fs, auto) have idg: "image_mset Mp gs = gs" using g_id by (induct gs, auto) have ufg: "unique_factorization_m g (lead_coeff g,gs)" proof (rule unique_factorization_mI[OF g]) fix e ks assume "factorization_m g (e,ks)" from factorization_m_prod[OF f this] uf[unfolded unique_factorization_m_alt_def] factorization_m_lead_coeff[OF this, unfolded degree_m_eq_lead_coeff[OF dg]] have "Mf (lead_coeff f * e, fs + ks) = Mf (c,hs)" and e: "M (lead_coeff g) = M e" by blast+ from this[folded eq, unfolded Mf_def split] have ks: "image_mset Mp ks = image_mset Mp gs" by auto show "Mf (e, ks) = Mf (lead_coeff g, gs)" unfolding Mf_def split ks e by simp qed from uff ufg eq[symmetric] idf idg show ?thesis by auto qed lemma unique_factorization_factorI: assumes ufact: "unique_factorization_m (f * g) FG" and cop: "coprime (lead_coeff (f * g)) p" and sf: "poly_mod.square_free_m p (f * g)" and n: "n ≠ 0" and m: "m = p^n" shows "factorization_m f F ⟹ unique_factorization_m f F" and "factorization_m g G ⟹ unique_factorization_m g G" proof - obtain c fg where FG: "FG = (c,fg)" by force from unique_factorization_m_factor[OF ufact[unfolded FG] cop sf n m] obtain fs gs where ufact: "unique_factorization_m f (lead_coeff f, fs)" "unique_factorization_m g (lead_coeff g, gs)" by auto from ufact(1) show "factorization_m f F ⟹ unique_factorization_m f F" by (metis unique_factorization_m_alt_def) from ufact(2) show "factorization_m g G ⟹ unique_factorization_m g G" by (metis unique_factorization_m_alt_def) qed end lemma monic_Mp_prod_mset: assumes fs: "⋀ f. f ∈# fs ⟹ monic (Mp f)" shows "monic (Mp (prod_mset fs))" proof - have "monic (prod_mset (image_mset Mp fs))" by (rule monic_prod_mset, insert fs, auto) from monic_Mp[OF this] have "monic (Mp (prod_mset (image_mset Mp fs)))" . also have "Mp (prod_mset (image_mset Mp fs)) = Mp (prod_mset fs)" by (rule Mp_prod_mset) finally show ?thesis . qed lemma degree_Mp_mult_monic: assumes "monic f" "monic g" shows "degree (Mp (f * g)) = degree f + degree g" by (metis zero_neq_one assms degree_monic_mult leading_coeff_0_iff monic_degree_m monic_mult) lemma factorization_m_degree: assumes "factorization_m f (c,fs)" and 0: "Mp f ≠ 0" shows "degree_m f = sum_mset (image_mset degree_m fs)" proof - note a = assms[unfolded factorization_m_def split] hence deg: "degree_m f = degree_m (smult c (prod_mset fs))" and fs: "⋀ f. f ∈# fs ⟹ monic (Mp f)" by auto define gs where "gs ≡ Mp (prod_mset fs)" from monic_Mp_prod_mset[OF fs] have mon_gs: "monic gs" unfolding gs_def . have d:"degree (Mp (Polynomial.smult c gs)) = degree gs" proof - have f1: "0 ≠ c" by (metis "0" Mp_0 a(1) smult_eq_0_iff) then have "M c ≠ 0" by (metis (no_types) "0" assms(1) factorization_m_lead_coeff leading_coeff_0_iff) then show "degree (Mp (Polynomial.smult c gs)) = degree gs" unfolding monic_degree_m[OF mon_gs,symmetric] using f1 by (metis coeff_smult degree_m_eq degree_smult_eq m1 mon_gs monic_degree_m mult_cancel_left1 poly_mod.M_def) qed note deg also have "degree_m (smult c (prod_mset fs)) = degree_m (smult c gs)" unfolding gs_def by simp also have "… = degree gs" using d. also have "… = sum_mset (image_mset degree_m fs)" unfolding gs_def using fs proof (induct fs) case (add f fs) have mon: "monic (Mp f)" "monic (Mp (prod_mset fs))" using monic_Mp_prod_mset[of fs] add(2) by auto have "degree (Mp (prod_mset (add_mset f fs))) = degree (Mp (Mp f * Mp (prod_mset fs)))" by (auto simp: ac_simps) also have "… = degree (Mp f) + degree (Mp (prod_mset fs))" by (rule degree_Mp_mult_monic[OF mon]) also have "degree (Mp (prod_mset fs)) = sum_mset (image_mset degree_m fs)" by (rule add(1), insert add(2), auto) finally show ?case by (simp add: ac_simps) qed simp finally show ?thesis . qed lemma degree_m_mult_le: "degree_m (f * g) ≤ degree_m f + degree_m g" using degree_m_mult_le by auto lemma degree_m_prod_mset_le: "degree_m (prod_mset fs) ≤ sum_mset (image_mset degree_m fs)" proof (induct fs) case empty show ?case by simp next case (add f fs) then show ?case using degree_m_mult_le[of f "prod_mset fs"] by auto qed end context poly_mod_prime begin lemma unique_factorization_m_factor_partition: assumes l0: "l ≠ 0" and uf: "poly_mod.unique_factorization_m (p^l) f (lead_coeff f, mset gs)" and f: "f = f1 * f2" and cop: "coprime (lead_coeff f) p" and sf: "square_free_m f" and part: "List.partition (λgi. gi dvdm f1) gs = (gs1, gs2)" shows "poly_mod.unique_factorization_m (p^l) f1 (lead_coeff f1, mset gs1)" "poly_mod.unique_factorization_m (p^l) f2 (lead_coeff f2, mset gs2)" proof - interpret pl: poly_mod_2 "p^l" by (standard, insert m1 l0, auto) let ?I = "image_mset pl.Mp" note Mp_pow [simp] = Mp_Mp_pow_is_Mp[OF l0 m1] have [simp]: "pl.Mp x dvdm u = (x dvdm u)" for x u unfolding dvdm_def using Mp_pow[of x] by (metis poly_mod.mult_Mp(1)) have gs_split: "set gs = set gs1 ∪ set gs2" using part by auto from pl.unique_factorization_m_factor[OF prime uf[unfolded f] _ _ l0 refl, folded f, OF cop sf] obtain hs1 hs2 where uf': "pl.unique_factorization_m f1 (lead_coeff f1, hs1)" "pl.unique_factorization_m f2 (lead_coeff f2, hs2)" and gs_hs: "?I (mset gs) = hs1 + hs2" unfolding pl.Mf_def split by auto have gs_gs: "?I (mset gs) = ?I (mset gs1) + ?I (mset gs2)" using part by (auto, induct gs arbitrary: gs1 gs2, auto) with gs_hs have gs_hs12: "?I (mset gs1) + ?I (mset gs2) = hs1 + hs2" by auto note pl_dvdm_imp_p_dvdm = pl_dvdm_imp_p_dvdm[OF l0] note fact = pl.unique_factorization_m_imp_factorization[OF uf] have gs1: "?I (mset gs1) = {#x ∈# ?I (mset gs). x dvdm f1#}" using part by (auto, induct gs arbitrary: gs1 gs2, auto) also have "… = {#x ∈# hs1. x dvdm f1#} + {#x ∈# hs2. x dvdm f1#}" unfolding gs_hs by simp also have "{#x ∈# hs2. x dvdm f1#} = {#}" proof (rule ccontr) assume "¬ ?thesis" then obtain x where x: "x ∈# hs2" and dvd: "x dvdm f1" by fastforce from x gs_hs have "x ∈# ?I (mset gs)" by auto with fact[unfolded pl.factorization_m_def] have xx: "pl.irreducible⇩_{d}_m x" "monic x" by auto from square_free_m_prod_imp_coprime_m[OF sf[unfolded f]] have cop_h_f: "coprime_m f1 f2" by auto from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf'(2)], of x] x have "pl.dvdm x f2" by auto hence "x dvdm f2" by (rule pl_dvdm_imp_p_dvdm) from cop_h_f[unfolded coprime_m_def, rule_format, OF dvd this] have "x dvdm 1" by auto from dvdm_imp_degree_le[OF this xx(2) _ m1] have "degree x = 0" by auto with xx show False unfolding pl.irreducible⇩_{d}_m_def by auto qed also have "{#x ∈# hs1. x dvdm f1#} = hs1" proof (rule ccontr) assume "¬ ?thesis" from filter_mset_inequality[OF this] obtain x where x: "x ∈# hs1" and dvd: "¬ x dvdm f1" by blast from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf'(1)], of x] x dvd have "pl.dvdm x f1" by auto from pl_dvdm_imp_p_dvdm[OF this] dvd show False by auto qed finally have gs_hs1: "?I (mset gs1) = hs1" by simp with gs_hs12 have "?I (mset gs2) = hs2" by auto with uf' gs_hs1 have "pl.unique_factorization_m f1 (lead_coeff f1, ?I (mset gs1))" "pl.unique_factorization_m f2 (lead_coeff f2, ?I (mset gs2))" by auto thus "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)" "pl.unique_factorization_m f2 (lead_coeff f2, mset gs2)" unfolding pl.unique_factorization_m_def by (auto simp: pl.Mf_def image_mset.compositionality o_def) qed lemma factorization_pn_to_factorization_p: assumes fact: "poly_mod.factorization_m (p^n) C (c,fs)" and sf: "square_free_m C" and n: "n ≠ 0" shows "factorization_m C (c,fs)" proof - let ?q = "p^n" from n m1 have q: "?q > 1" by simp interpret q: poly_mod_2 ?q by (standard, insert q, auto) from fact[unfolded q.factorization_m_def] have eq: "q.Mp C = q.Mp (Polynomial.smult c (prod_mset fs))" and irr: "⋀ f. f ∈# fs ⟹ q.irreducible⇩_{d}_m f" and mon: "⋀ f. f ∈# fs ⟹ monic (q.Mp f)" by auto from arg_cong[OF eq, of Mp] have eq: "eq_m C (smult c (prod_mset fs))" by (simp add: Mp_Mp_pow_is_Mp m1 n) show ?thesis unfolding factorization_m_def split proof (rule conjI[OF eq], intro ballI conjI) fix f assume f: "f ∈# fs" from mon[OF this] have mon_qf: "monic (q.Mp f)" . hence lc: "lead_coeff (q.Mp f) = 1" by auto from mon_qf show mon_f: "monic (Mp f)" by (metis Mp_Mp_pow_is_Mp m1 monic_Mp n) from irr[OF f] have irr: "q.irreducible⇩_{d}_m f" . hence "q.degree_m f ≠ 0" unfolding q.irreducible⇩_{d}_m_def by auto also have "q.degree_m f = degree_m f" using mon[OF f] by (metis Mp_Mp_pow_is_Mp m1 monic_degree_m n) finally have deg: "degree_m f ≠ 0" by auto from f obtain gs where fs: "fs = {#f#} + gs" by (metis mset_subset_eq_single subset_mset.add_diff_inverse) from eq[unfolded fs] have "Mp C = Mp (f * smult c (prod_mset gs))" by auto from square_free_m_factor[OF square_free_m_cong[OF sf this]] have sf_f: "square_free_m f" by simp have sf_Mf: "square_free_m (q.Mp f)" by (rule square_free_m_cong[OF sf_f], auto simp: Mp_Mp_pow_is_Mp n m1) have "coprime (lead_coeff (q.Mp f)) p" using mon[OF f] prime by simp from berlekamp_hensel[OF this sf_Mf refl n, unfolded lc] obtain gs where qfact: "q.factorization_m (q.Mp f) (1, mset gs)" and "⋀ g. g ∈ set gs ⟹ irreducible_m g" by blast hence fact: "q.Mp f = q.Mp (prod_list gs)" and gs: "⋀ g. g∈ set gs ⟹ irreducible⇩_{d}_m g ∧ q.irreducible⇩_{d}_m g ∧ monic (q.Mp g)" unfolding q.factorization_m_def by auto from q.factorization_m_degree[OF qfact] have deg: "q.degree_m (q.Mp f) = sum_mset (image_mset q.degree_m (mset gs))" using mon_qf by fastforce from irr[unfolded q.irreducible⇩_{d}_m_def] have "sum_mset (image_mset q.degree_m (mset gs)) ≠ 0" by (fold deg, auto) then obtain g gs' where gs1: "gs = g # gs'" by (cases gs, auto) { assume "gs' ≠ []" then obtain h hs where gs2: "gs' = h # hs" by (cases gs', auto) from deg gs[unfolded q.irreducible⇩_{d}_m_def] have small: "q.degree_m g < q.degree_m f" "q.degree_m h + sum_mset (image_mset q.degree_m (mset hs)) < q.degree_m f" unfolding gs1 gs2 by auto have "q.eq_m f (g * (h * prod_list hs))" using fact unfolding gs1 gs2 by simp with irr[unfolded q.irreducible⇩_{d}_m_def, THEN conjunct2, rule_format, of g "h * prod_list hs"] small(1) have "¬ q.degree_m (h * prod_list hs) < q.degree_m f" by auto hence "q.degree_m f ≤ q.degree_m (h * prod_list hs)" by simp also have "… = q.degree_m (prod_mset ({#h#} + mset hs))" by simp also have "… ≤ sum_mset (image_mset q.degree_m ({#h#} + mset hs))" by (rule q.degree_m_prod_mset_le) also have "… < q.degree_m f" using small(2) by simp finally have False by simp } hence gs1: "gs = [g]" unfolding gs1 by (cases gs', auto) with fact have "q.Mp f = q.Mp g" by auto from arg_cong[OF this, of Mp] have eq: "Mp f = Mp g" by (simp add: Mp_Mp_pow_is_Mp m1 n) from gs[unfolded gs1] have g: "irreducible⇩_{d}_m g" by auto with eq show "irreducible⇩_{d}_m f" unfolding irreducible⇩_{d}_m_def by auto qed qed lemma unique_monic_hensel_factorization: assumes ufact: "unique_factorization_m C (1,Fs)" and C: "monic C" "square_free_m C" and n: "n ≠ 0" shows "∃ Gs. poly_mod.unique_factorization_m (p^n) C (1, Gs)" using ufact C proof (induct Fs arbitrary: C rule: wf_induct[OF wf_measure[of size]]) case (1 Fs C) let ?q = "p^n" from n m1 have q: "?q > 1" by simp interpret q: poly_mod_2 ?q by (standard, insert q, auto) note [simp] = Mp_Mp_pow_is_Mp[OF n m1] note IH = 1(1)[rule_format] note ufact = 1(2) hence fact: "factorization_m C (1, Fs)" unfolding unique_factorization_m_alt_def by auto note monC = 1(3) note sf = 1(4) let ?n = "size Fs" { fix d gs assume qfact: "q.factorization_m C (d,gs)" from q.factorization_m_lead_coeff[OF this] q.monic_Mp[OF monC] have d1: "q.M d = 1" by auto from factorization_pn_to_factorization_p[OF qfact sf n] have "factorization_m C (d,gs)" . with ufact d1 have "q.M d = 1" "M d = 1" "image_mset Mp gs = image_mset Mp Fs" unfolding unique_factorization_m_alt_def Mf_def by auto } note pre_unique = this show ?case proof (cases Fs) case empty with fact C have "Mp C = 1" unfolding factorization_m_def by auto hence "degree (Mp C) = 0" by simp with degree_m_eq_monic[OF monC m1] have "degree C = 0" by simp with monC have C1: "C = 1" using monic_degree_0 by blast with fact have fact: "q.factorization_m C (1,{#})" by (auto simp: q.factorization_m_def) show ?thesis proof (rule exI, rule q.unique_factorization_mI[OF fact]) fix d gs assume fact: "q.factorization_m C (d,gs)" from pre_unique[OF this, unfolded empty] show "q.Mf (d, gs) = q.Mf (1, {#})" by (auto simp: q.Mf_def) qed next case (add D H) note FDH = this let ?D = "Mp D" let ?H = "Mp (prod_mset H)" from fact have monFs: "⋀ F. F ∈# Fs ⟹ monic (Mp F)" and prod: "eq_m C (prod_mset Fs)" unfolding factorization_m_def by auto hence monD: "monic ?D" unfolding FDH by auto from square_free_m_cong[OF sf, of "D * prod_mset H"] prod[unfolded FDH] have "square_free_m (D * prod_mset H)" by (auto simp: ac_simps) from square_free_m_prod_imp_coprime_m[OF this] have "coprime_m D (prod_mset H)" . hence cop': "coprime_m ?D ?H" unfolding coprime_m_def dvdm_def Mp_Mp by simp from fact have eq': "eq_m (?D * ?H) C" unfolding FDH by (simp add: factorization_m_def ac_simps) note unique_hensel_binary[OF prime cop' eq' Mp_Mp Mp_Mp monD n] from ex1_implies_ex[OF this] this obtain A B where CAB: "q.eq_m (A * B) C" and monA: "monic A" and DA: "eq_m ?D A" and HB: "eq_m ?H B" and norm: "q.Mp A = A" "q.Mp B = B" and unique: "⋀ D' H'. q.eq_m (D' * H') C ⟹ monic D' ⟹ eq_m (Mp D) D' ⟹ eq_m (Mp (prod_mset H)) H' ⟹ q.Mp D' = D' ⟹ q.Mp H' = H' ⟹ D' = A ∧ H' = B" by blast note hensel_bin_wit = CAB monA DA HB norm from monA have monA': "monic (q.Mp A)" by (rule q.monic_Mp) from q.monic_Mp[OF monC] CAB have monicP:"monic (q.Mp (A * B))" by auto have f4: "⋀p. coeff (A * p) (degree (A * p)) = coeff p (degree p)" by (simp add: coeff_degree_mult monA) have f2: "⋀p n i. coeff p n mod i = coeff (poly_mod.Mp i p) n" using poly_mod.M_def poly_mod.Mp_coeff by presburger hence "coeff B (degree B) = 0 ∨ monic B" using monicP f4 by (metis (no_types) norm(2) q.degree_m_eq q.m1) hence monB: "monic B" using f4 monicP by (metis norm(2) leading_coeff_0_iff) from monA monB have lcAB: "lead_coeff (A * B) = 1" by (rule monic_mult) hence copAB: "coprime (lead_coeff (A * B)) p" by auto from arg_cong[OF CAB, of Mp] have CAB': "eq_m C (A * B)" by auto from sf CAB' have sfAB: "square_free_m (A * B)" using square_free_m_cong by blast from CAB' ufact have ufact: "unique_factorization_m (A * B) (1, Fs)" using unique_factorization_m_cong by blast have "(1 :: nat) ≠ 0" "p = p ^ 1" by auto note u_factor = unique_factorization_factorI[OF prime ufact copAB sfAB this] from fact DA have "irreducible⇩_{d}_m D" "eq_m A D" unfolding add factorization_m_def by auto hence "irreducible⇩_{d}_m A" using Mp_irreducible⇩_{d}_m by fastforce from irreducible⇩_{d}_lifting[OF n _ this] have irrA: "q.irreducible⇩_{d}_m A" using monA by (simp add: m1 poly_mod.degree_m_eq_monic q.m1) from add have lenH: "(H,Fs) ∈ measure size" by auto from HB fact have factB: "factorization_m B (1, H)" unfolding FDH factorization_m_def by auto from u_factor(2)[OF factB] have ufactB: "unique_factorization_m B (1, H)" . from sfAB have sfB: "square_free_m B" by (rule square_free_m_factor) from IH[OF lenH ufactB monB sfB] obtain Bs where IH2: "q.unique_factorization_m B (1, Bs)" by auto from CAB have "q.Mp C = q.Mp (q.Mp A * q.Mp B)" by simp also have "q.Mp A * q.Mp B = q.Mp A * q.Mp (prod_mset Bs)" using IH2 unfolding q.unique_factorization_m_alt_def q.factorization_m_def by auto also have "q.Mp … = q.Mp (A * prod_mset Bs)" by simp finally have factC: "q.factorization_m C (1, {# A #} + Bs)" using IH2 monA' irrA by (auto simp: q.unique_factorization_m_alt_def q.factorization_m_def) show ?thesis proof (rule exI, rule q.unique_factorization_mI[OF factC]) fix d gs assume dgs: "q.factorization_m C (d,gs)" from pre_unique[OF dgs, unfolded add] have d1: "q.M d = 1" and gs_fs: "image_mset Mp gs = {# Mp D #} + image_mset Mp H" by (auto simp: ac_simps) have "∀f m p ma. image_mset f m ≠ add_mset (p::int poly) ma ∨ (∃mb pa. m = add_mset (pa::int poly) mb ∧ f pa = p ∧ image_mset f mb = ma)" by (simp add: msed_map_invR) then obtain g hs where gs: "gs = {# g #} + hs" and gD: "Mp g = Mp D" and hsH: "image_mset Mp hs = image_mset Mp H" using gs_fs by (metis add_mset_add_single union_commute) from dgs[unfolded q.factorization_m_def split] have eq: "q.Mp C = q.Mp (smult d (prod_mset gs))" and irr_mon: "⋀ g. g∈#gs ⟹ q.irreducible⇩_{d}_m g ∧ monic (q.Mp g)" using d1 by auto note eq also have "q.Mp (smult d (prod_mset gs)) = q.Mp (smult (q.M d) (prod_mset gs))" by simp also have "… = q.Mp (prod_mset gs)" unfolding d1 by simp finally have eq: "q.eq_m (q.Mp g * q.Mp (prod_mset hs)) C" unfolding gs by simp from gD have Dg: "eq_m (Mp D) (q.Mp g)" by simp have "Mp (prod_mset H) = Mp (prod_mset (image_mset Mp H))" by simp also have "… = Mp (prod_mset hs)" unfolding hsH[symmetric] by simp finally have Hhs: "eq_m (Mp (prod_mset H)) (q.Mp (prod_mset hs))" by simp from irr_mon[of g, unfolded gs] have mon_g: "monic (q.Mp g)" by auto from unique[OF eq mon_g Dg Hhs q.Mp_Mp q.Mp_Mp] have gA: "q.Mp g = A" and hsB: "q.Mp (prod_mset hs) = B" by auto have "q.factorization_m B (1, hs)" unfolding q.factorization_m_def split by (simp add: hsB norm irr_mon[unfolded gs]) with IH2 have hsBs: "q.Mf (1,hs) = q.Mf (1,Bs)" unfolding q.unique_factorization_m_alt_def by blast show "q.Mf (d, gs) = q.Mf (1, {# A #} + Bs)" using gA hsBs d1 unfolding gs q.Mf_def by auto qed qed qed theorem berlekamp_hensel_unique: assumes cop: "coprime (lead_coeff f) p" and sf: "poly_mod.square_free_m p f" and res: "berlekamp_hensel p n f = gs" and n: "n ≠ 0" shows "poly_mod.unique_factorization_m (p^n) f (lead_coeff f, mset gs) ― ‹unique factorization mod ‹p^n››" "⋀ g. g ∈ set gs ⟹ poly_mod.Mp (p^n) g = g ― ‹normalized›" proof - let ?q = "p^n" interpret q: poly_mod_2 ?q unfolding poly_mod_2_def using m1 n by simp from berlekamp_hensel[OF assms] have bh_fact: "q.factorization_m f (lead_coeff f, mset gs)" by auto from berlekamp_hensel[OF assms] show "⋀ g. g ∈ set gs ⟹ poly_mod.Mp (p^n) g = g" by blast from prime have p1: "p > 1" by (simp add: prime_int_iff) let ?lc = "coeff f (degree f)" define ilc where "ilc ≡ inverse_mod ?lc (p ^ n)" from cop p1 n have inv: "q.M (ilc * ?lc) = 1" by (auto simp add: q.M_def ilc_def inverse_mod_pow) hence ilc0: "ilc ≠ 0" by (cases "ilc = 0", auto) { fix q assume "ilc * ?lc = ?q * q" from arg_cong[OF this, of q.M] have "q.M (ilc * ?lc) = 0" unfolding q.M_def by auto with inv have False by auto } note not_dvd = this let ?in = "q.Mp (smult ilc f)" have mon: "monic ?in" unfolding q.Mp_coeff coeff_smult by (subst q.degree_m_eq[OF _ q.m1], insert not_dvd, auto simp: inv ilc0) have "q.Mp f = q.Mp (smult (q.M (?lc * ilc)) f)" using inv by (simp add: ac_simps) also have "… = q.Mp (smult ?lc (smult ilc f))" by simp finally have f: "q.Mp f = q.Mp (smult ?lc (smult ilc f))" . from arg_cong[OF f, of Mp] have "Mp f = Mp (smult ?lc (smult ilc f))" by (simp add: Mp_Mp_pow_is_Mp n p1) from arg_cong[OF this, of square_free_m, unfolded Mp_square_free_m] sf have "square_free_m (smult (coeff f (degree f)) (smult ilc f))" by simp from square_free_m_smultD[OF this] have sf: "square_free_m (smult ilc f)" . have Mp_in: "Mp ?in = Mp (smult ilc f)" by (simp add: Mp_Mp_pow_is_Mp n p1) from Mp_square_free_m[of ?in, unfolded Mp_in] sf have sf: "square_free_m ?in" unfolding Mp_square_free_m by simp obtain a b where "finite_field_factorization_int p ?in = (a,b)" by force from finite_field_factorization_int[OF sf this] have ufact: "unique_factorization_m ?in (a, mset b)" by auto from unique_factorization_m_imp_factorization[OF this] have fact: "factorization_m ?in (a, mset b)" . from factorization_m_lead_coeff[OF this] monic_Mp[OF mon] have "M a = 1" by auto with ufact have "unique_factorization_m ?in (1, mset b)" unfolding unique_factorization_m_def Mf_def by auto from unique_monic_hensel_factorization[OF this mon sf n] obtain hs where "q.unique_factorization_m ?in (1, hs)" by auto hence unique: "q.unique_factorization_m (smult ilc f) (1, hs)" unfolding unique_factorization_m_def Mf_def by auto from q.factorization_m_smult[OF q.unique_factorization_m_imp_factorization[OF unique], of ?lc] have "q.factorization_m (smult (ilc * ?lc) f) (?lc, hs)" by (simp add: ac_simps) moreover have "q.Mp (smult (q.M (ilc * ?lc)) f) = q.Mp f" unfolding inv by simp ultimately have fact: "q.factorization_m f (?lc, hs)" unfolding q.factorization_m_def by auto have "q.unique_factorization_m f (?lc, hs)" proof (rule q.unique_factorization_mI[OF fact]) fix d us assume other_fact: "q.factorization_m f (d,us)" from q.factorization_m_lead_coeff[OF this] have lc: "q.M d = lead_coeff (q.Mp f)" .. have lc: "q.M d = q.M ?lc" unfolding lc by (metis bh_fact q.factorization_m_lead_coeff) from q.factorization_m_smult[OF other_fact, of ilc] unique have eq: "q.Mf (d * ilc, us) = q.Mf (1, hs)" unfolding q.unique_factorization_m_def by auto thus "q.Mf (d, us) = q.Mf (?lc, hs)" using lc unfolding q.Mf_def by auto qed with bh_fact show "q.unique_factorization_m f (lead_coeff f, mset gs)" unfolding q.unique_factorization_m_alt_def by metis qed lemma hensel_lifting_unique: assumes n: "n ≠ 0" and res: "hensel_lifting p n f fs = gs" ― ‹result of hensel is fact. ‹gs›› and cop: "coprime (lead_coeff f) p" and sf: "poly_mod.square_free_m p f" and fact: "poly_mod.factorization_m p f (c, mset fs)" ― ‹input is fact. ‹fs mod p›› and c: "c ∈ {0..<p}" and norm: "(∀fi∈set fs. set (coeffs fi) ⊆ {0..<p})" shows "poly_mod.unique_factorization_m (p^n) f (lead_coeff f, mset gs)" ― ‹unique factorization mod ‹p^n›› "sort (map degree fs) = sort (map degree gs)" ― ‹degrees stay the same› "⋀ g. g ∈ set gs ⟹ monic g ∧ poly_mod.Mp (p^n) g = g ∧ ― ‹monic and normalized› poly_mod.irreducible_m p g ∧ ― ‹irreducibility even mod ‹p›› poly_mod.degree_m p g = degree g ― ‹mod ‹p› does not change degree of ‹g››" proof - note hensel = hensel_lifting[OF assms] show "sort (map degree fs) = sort (map degree gs)" "⋀ g. g ∈ set gs ⟹ monic g ∧ poly_mod.Mp (p^n) g = g ∧ poly_mod.irreducible_m p g ∧ poly_mod.degree_m p g = degree g" using hensel by auto from berlekamp_hensel_unique[OF cop sf refl n] have "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" by auto with hensel(1) show "poly_mod.unique_factorization_m (p^n) f (lead_coeff f, mset gs)" by (metis poly_mod.unique_factorization_m_alt_def) qed end end