# Theory Factor_Bound_2

(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Factor bound› text ‹This theory extends the work about factor bounds which was carried out in the Berlekamp-Zassenhaus development.› theory Factor_Bound_2 imports Berlekamp_Zassenhaus.Factor_Bound LLL_Basis_Reduction.Norms begin lemma norm_1_bound_mignotte: "norm1 f ≤ 2^(degree f) * mahler_measure f" proof (cases "f = 0") case f0: False have cf: "coeffs f = map (λ i. coeff f i) [0 ..< Suc( degree f)]" unfolding coeffs_def using f0 by auto have "real_of_int (sum_list (map abs (coeffs f))) = (∑i≤degree f. real_of_int ¦poly.coeff f i¦)" unfolding cf of_int_hom.hom_sum_list unfolding sum_list_sum_nth by (rule sum.cong, force, auto simp: o_def nth_append) also have "… ≤ (∑i≤degree f. real (degree f choose i) * mahler_measure f)" by (rule sum_mono, rule Mignotte_bound) also have "… = real (sum (λ i. (degree f choose i)) {..degree f}) * mahler_measure f" unfolding sum_distrib_right[symmetric] by auto also have "… = 2^(degree f) * mahler_measure f" unfolding choose_row_sum by auto finally show ?thesis unfolding norm1_def . qed (auto simp: mahler_measure_ge_0 norm1_def) lemma mahler_measure_l2norm: "mahler_measure f ≤ sqrt (of_int ∥f∥⇧^{2})" using Landau_inequality_mahler_measure[of f] unfolding sq_norm_poly_def by (auto simp: power2_eq_square) lemma sq_norm_factor_bound: fixes f h :: "int poly" assumes dvd: "h dvd f" and f0: "f ≠ 0" shows "∥h∥⇧^{2}≤ 2 ^ (2 * degree h) * ∥f∥⇧^{2}" proof - let ?r = real_of_int have h21: "?r ∥h∥⇧^{2}≤ (?r (norm1 h))^2" using norm2_le_norm1_int[of h] by (metis of_int_le_iff of_int_power) also have "… ≤ (2^(degree h) * mahler_measure h)^2" using power_mono[OF norm_1_bound_mignotte[of h], of 2] by (auto simp: norm1_ge_0) also have "… = 2^(2 * degree h) * (mahler_measure h)^2" by (simp add: power_even_eq power_mult_distrib) also have "… ≤ 2^(2 * degree h) * (mahler_measure f)^2" by (rule mult_left_mono[OF power_mono], auto simp: mahler_measure_ge_0 mahler_measure_dvd[OF f0 dvd]) also have "… ≤ 2^(2 * degree h) * ?r (∥f∥⇧^{2})" proof (rule mult_left_mono) have "?r (∥f∥⇧^{2}) ≥ 0" by auto from real_sqrt_pow2[OF this] show "(mahler_measure f)⇧^{2}≤ ?r (∥f∥⇧^{2})" using power_mono[OF mahler_measure_l2norm[of f], of 2] by (auto simp: mahler_measure_ge_0) qed auto also have "… = ?r (2^(2*degree h) * ∥f∥⇧^{2})" by (simp add: ac_simps) finally show "∥h∥⇧^{2}≤ 2 ^ (2 * degree h) * ∥f∥⇧^{2}" unfolding of_int_le_iff . qed end

# Theory Missing_Dvd_Int_Poly

(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Executable dvdm operation› text ‹This theory contains some results about division of integer polynomials which are not part of Polynomial\_Factorization.Dvd\_Int\_Poly.thy. Essentially, we give an executable implementation of division modulo m. › theory Missing_Dvd_Int_Poly imports Berlekamp_Zassenhaus.Poly_Mod_Finite_Field Berlekamp_Zassenhaus.Polynomial_Record_Based Berlekamp_Zassenhaus.Hensel_Lifting (* for thm pdivmod_monic, should be moved *) Subresultants.Subresultant (* for abbreviation pdivmod *) Perron_Frobenius.Cancel_Card_Constraint begin (*In mathematics, this lemma also works if q = 0 since degree 0 = -∞, but in Isabelle degree 0 = 0.*) lemma degree_div_mod_smult: fixes g::"int poly" assumes g: "degree g < j" and r: "degree r < d" and u: "degree u = d" and g1: "g = q * u + smult m r" and q: "q ≠ 0" and m_not0: "m ≠ 0" shows "degree q < j - d" proof - have u_not0: "u≠0" using u r by auto have d_uq: "d ≤ degree (u*q)" using u degree_mult_right_le[OF q] by auto have j: "j > degree (q* u + smult m r)" using g1 g by auto have "degree (smult m r) < d" using degree_smult_eq m_not0 r by auto also have "... ≤ degree (u*q)" using d_uq by auto finally have deg_mr_uq: "degree (smult m r) < degree (q*u)" by (simp add: mult.commute) have j2: "degree (q* u + smult m r) = degree (q*u)" by (rule degree_add_eq_left[OF deg_mr_uq]) also have "... = degree q + degree u" by (rule degree_mult_eq[OF q u_not0]) finally have "degree q = degree g - degree u" using g1 by auto thus ?thesis using j j2 ‹degree (q * u) = degree q + degree u› u by linarith qed subsection ‹Uniqueness of division algorithm for polynomials› lemma uniqueness_algorithm_division_poly: fixes f::"'a::{comm_ring,semiring_1_no_zero_divisors} poly" assumes f1: "f = g * q1 + r1" and f2: "f = g * q2 + r2" and g: "g ≠ 0" and r1: "r1 = 0 ∨ degree r1 < degree g" and r2: "r2 = 0 ∨ degree r2 < degree g" shows "q1 = q2 ∧ r1 = r2" proof - have "0 = g * q1 + r1 - (g * q2 + r2)" using f1 f2 by auto also have "... = g * (q1 - q2) + r1 - r2" by (simp add: right_diff_distrib) finally have eq: "g * (q1 - q2) = r2 - r1" by auto have q_eq: "q1 = q2" proof (rule ccontr) assume q1_not_q2: "q1 ≠ q2" hence nz: "g * (q1 - q2) ≠ 0" using g by auto hence "degree (g * (q1 - q2)) ≥ degree g" by (simp add: degree_mult_right_le) moreover have "degree (r2 - r1) < degree g" using eq nz degree_diff_less r1 r2 by auto ultimately show False using eq by auto qed moreover have "r1 = r2" using eq q_eq by auto ultimately show ?thesis by simp qed lemma pdivmod_eq_pdivmod_monic: assumes g: "monic g" shows "pdivmod f g = pdivmod_monic f g" proof - obtain q r where qr: "pdivmod f g = (q,r)" by simp obtain Q R where QR: "pdivmod_monic f g = (Q,R)" by (meson surj_pair) have g0: "g ≠ 0" using g by auto have f1: "f = g * q + r" by (metis Pair_inject mult_div_mod_eq qr) have r: "r=0 ∨ degree r < degree g" by (metis Pair_inject assms degree_mod_less leading_coeff_0_iff qr zero_neq_one) have f2: "f = g * Q + R" by (simp add: QR assms pdivmod_monic(1)) have R: "R=0 ∨ degree R < degree g" by (rule pdivmod_monic[OF g QR]) have "q=Q ∧ r=R" by (rule uniqueness_algorithm_division_poly[OF f1 f2 g0 r R]) thus ?thesis using qr QR by auto qed context poly_mod begin definition "pdivmod2 f g = (if Mp g = 0 then (0, f) else let ilc = inverse_p m ((lead_coeff (Mp g))); h = Polynomial.smult ilc (Mp g); (q, r) = pseudo_divmod (Mp f) (Mp h) in (Polynomial.smult ilc q, r))" end context poly_mod_prime_type begin lemma dvdm_iff_pdivmod0: assumes f: "(F :: 'a mod_ring poly) = of_int_poly f" and g: "(G :: 'a mod_ring poly) = of_int_poly g" shows "g dvdm f = (snd (pdivmod F G) = 0)" proof - have [transfer_rule]: "MP_Rel f F" unfolding MP_Rel_def by (simp add: Mp_f_representative f) have [transfer_rule]: "MP_Rel g G" unfolding MP_Rel_def by (simp add: Mp_f_representative g) have "(snd (pdivmod F G) = 0) = (G dvd F)" unfolding dvd_eq_mod_eq_0 by auto from this [untransferred] show ?thesis by simp qed lemma of_int_poly_Mp_0[simp]: "(of_int_poly (Mp a) = (0:: 'a mod_ring poly)) = (Mp a = 0)" by (auto, metis Mp_f_representative map_poly_0 poly_mod.Mp_Mp) lemma uniqueness_algorithm_division_of_int_poly: assumes g0: "Mp g ≠ 0" and f: "(F :: 'a mod_ring poly) = of_int_poly f" and g: "(G :: 'a mod_ring poly) = of_int_poly g" and F: "F = G * Q + R" and R: "R = 0 ∨ degree R < degree G" and Mp_f: "Mp f = Mp g * q + r" and r: "r = 0 ∨ degree r < degree (Mp g)" shows "Q = of_int_poly q ∧ R = of_int_poly r" proof (rule uniqueness_algorithm_division_poly[OF F _ _ R]) have f': "Mp f = to_int_poly F" unfolding f by (simp add: Mp_f_representative) have g': "Mp g = to_int_poly G" unfolding g by (simp add: Mp_f_representative) have f'': "of_int_poly (Mp f) = F" by (metis (no_types, lifting) Dp_Mp_eq Mp_f_representative Mp_smult_m_0 add_cancel_left_right f map_poly_zero of_int_hom.map_poly_hom_add to_int_mod_ring_hom.hom_zero to_int_mod_ring_hom.injectivity) have g'': "of_int_poly (Mp g) = G" by (metis (no_types, lifting) Dp_Mp_eq Mp_f_representative Mp_smult_m_0 add_cancel_left_right g map_poly_zero of_int_hom.map_poly_hom_add to_int_mod_ring_hom.hom_zero to_int_mod_ring_hom.injectivity) have "F = of_int_poly (Mp g * q + r)" using Mp_f f'' by auto also have "... = G * of_int_poly q + of_int_poly r" by (simp add: g'' of_int_poly_hom.hom_add of_int_poly_hom.hom_mult) finally show "F = G * of_int_poly q + of_int_poly r" . show "of_int_poly r = 0 ∨ degree (of_int_poly r::'a mod_ring poly) < degree G" proof (cases "r = 0") case True hence "of_int_poly r = 0" by auto then show ?thesis by auto next case False have "degree (of_int_poly r::'a mod_ring poly) ≤ degree (r)" by (simp add: degree_map_poly_le) also have "... < degree (Mp g)" using r False by auto also have "... = degree G" by (simp add: g') finally show ?thesis by auto qed show "G ≠ 0" using g0 unfolding g''[symmetric] by simp qed corollary uniqueness_algorithm_division_to_int_poly: assumes g0: "Mp g ≠ 0" and f: "(F :: 'a mod_ring poly) = of_int_poly f" and g: "(G :: 'a mod_ring poly) = of_int_poly g" and F: "F = G * Q + R" and R: "R = 0 ∨ degree R < degree G" and Mp_f: "Mp f = Mp g * q + r" and r: "r = 0 ∨ degree r < degree (Mp g)" shows "Mp q = to_int_poly Q ∧ Mp r = to_int_poly R" using uniqueness_algorithm_division_of_int_poly[OF assms] by (auto simp add: Mp_f_representative) lemma uniqueness_algorithm_division_Mp_Rel: assumes monic_Mpg: "monic (Mp g)" and f: "(F :: 'a mod_ring poly) = of_int_poly f" and g: "(G :: 'a mod_ring poly) = of_int_poly g" and qr: "pseudo_divmod (Mp f) (Mp g) = (q,r)" and QR: "pseudo_divmod F G = (Q,R)" shows "MP_Rel q Q ∧ MP_Rel r R " proof (unfold MP_Rel_def, rule uniqueness_algorithm_division_to_int_poly[OF _ f g]) show f_gq_r: "Mp f = Mp g * q + r" by (rule pdivmod_monic(1)[OF monic_Mpg], simp add: pdivmod_monic_pseudo_divmod qr monic_Mpg) have monic_G: "monic G" using monic_Mpg using Mp_f_representative g by auto show "F = G * Q + R" by (rule pdivmod_monic(1)[OF monic_G], simp add: pdivmod_monic_pseudo_divmod QR monic_G) show "Mp g ≠ 0" using monic_Mpg by auto show "R = 0 ∨ degree R < degree G" by (rule pdivmod_monic(2)[OF monic_G], auto simp add: pdivmod_monic_pseudo_divmod monic_G intro: QR) show "r = 0 ∨ degree r < degree (Mp g)" by (rule pdivmod_monic(2)[OF monic_Mpg], auto simp add: pdivmod_monic_pseudo_divmod monic_Mpg intro: qr) qed definition "MP_Rel_Pair A B ≡ (let (a,b) = A; (c,d) = B in MP_Rel a c ∧ MP_Rel b d)" lemma pdivmod2_rel[transfer_rule]: "(MP_Rel ===> MP_Rel ===> MP_Rel_Pair) (pdivmod2) (pdivmod)" proof (auto simp add: rel_fun_def MP_Rel_Pair_def) interpret pm: prime_field m using m unfolding prime_field_def mod_ring_locale_def by auto have p: "prime_field TYPE('a) m" using m unfolding prime_field_def mod_ring_locale_def by auto fix f F g G a b assume 1[transfer_rule]: "MP_Rel f F" and 2[transfer_rule]: "MP_Rel g G" and 3: "pdivmod2 f g = (a, b)" have "MP_Rel a (F div G) ∧ MP_Rel b (F mod G)" proof (cases "Mp g ≠ 0") case True note Mp_g = True have G: "G ≠ 0" using Mp_g 2 unfolding MP_Rel_def by auto have gG[transfer_rule]: "pm.mod_ring_rel (lead_coeff (Mp g)) (lead_coeff G)" using 2 unfolding pm.mod_ring_rel_def MP_Rel_def by auto have [transfer_rule]: "(pm.mod_ring_rel ===> pm.mod_ring_rel) (inverse_p m) inverse" by (rule prime_field.mod_ring_inverse[OF p]) hence rel_inverse_p[transfer_rule]: "pm.mod_ring_rel (inverse_p m ((lead_coeff (Mp g)))) (inverse (lead_coeff G))" using gG unfolding rel_fun_def by auto let ?h= "(Polynomial.smult (inverse_p m (lead_coeff (Mp g))) g)" define h where h: "h = Polynomial.smult (inverse_p m (lead_coeff (Mp g))) (Mp g)" define H where H: "H = Polynomial.smult (inverse (lead_coeff G)) G" have hH': "MP_Rel ?h H" unfolding MP_Rel_def unfolding H by (metis (mono_tags, hide_lams) "2" MP_Rel_def M_to_int_mod_ring Mp_f_representative rel_inverse_p functional_relation left_total_MP_Rel of_int_hom.map_poly_hom_smult pm.mod_ring_rel_def right_unique_MP_Rel to_int_mod_ring_hom.injectivity to_int_mod_ring_of_int_M) have "Mp (Polynomial.smult (inverse_p m (lead_coeff (Mp g))) g) = Mp (Polynomial.smult (inverse_p m (lead_coeff (Mp g))) (Mp g))" by simp hence hH: "MP_Rel h H" using hH' h unfolding MP_Rel_def by auto obtain q x where pseudo_fh: "pseudo_divmod (Mp f) (Mp h) = (q, x)" by (meson surj_pair) hence lc_G: "(lead_coeff G) ≠ 0" using G by auto have a: "a = Polynomial.smult (inverse_p m ((lead_coeff (Mp g)))) q" using 3 pseudo_fh Mp_g unfolding pdivmod2_def Let_def h by auto have b: "b = x" using 3 pseudo_fh Mp_g unfolding pdivmod2_def Let_def h by auto have Mp_Rel_FH: "MP_Rel q (F div H) ∧ MP_Rel x (F mod H)" proof (rule uniqueness_algorithm_division_Mp_Rel) show "monic (Mp h)" proof - have aux: "(inverse_p m (lead_coeff (Mp g))) = to_int_mod_ring (inverse (lead_coeff G))" using rel_inverse_p unfolding pm.mod_ring_rel_def by auto hence "M (inverse_p m (M (poly.coeff g (degree (Mp g))))) = to_int_mod_ring (inverse (lead_coeff G))" by (simp add: M_to_int_mod_ring Mp_coeff) thus ?thesis unfolding h unfolding Mp_coeff by auto (metis (no_types, lifting) "2" H MP_Rel_def Mp_coeff aux degree_smult_eq gG hH' inverse_zero_imp_zero lc_G left_inverse pm.mod_ring_rel_def to_int_mod_ring_hom.degree_map_poly_hom to_int_mod_ring_hom.hom_one to_int_mod_ring_times) qed hence monic_H: "monic H" using hH H lc_G by auto show f: "F = of_int_poly f" using 1 unfolding MP_Rel_def by (simp add: Mp_f_representative poly_eq_iff) have "pdivmod F H = pdivmod_monic F H" by (rule pdivmod_eq_pdivmod_monic[OF monic_H]) also have "... = pseudo_divmod F H" by (rule pdivmod_monic_pseudo_divmod[OF monic_H]) finally show "pseudo_divmod F H = (F div H, F mod H)" by simp show "H = of_int_poly h" by (meson MP_Rel_def Mp_f_representative hH right_unique_MP_Rel right_unique_def) show "pseudo_divmod (Mp f) (Mp h) = (q, x)" by (rule pseudo_fh) qed hence Mp_Rel_F_div_H: "MP_Rel q (F div H)" and Mp_Rel_F_mod_H: "MP_Rel x (F mod H)" by auto have "F div H = Polynomial.smult (lead_coeff G) (F div G)" unfolding H using div_smult_right[OF lc_G] inverse_inverse_eq by (metis div_smult_right inverse_zero) hence F_div_G: "(F div G) = Polynomial.smult (inverse (lead_coeff G)) (F div H)" using lc_G by auto have "MP_Rel a (F div G)" proof - have "of_int_poly (Polynomial.smult (inverse_p m ((lead_coeff (Mp g)))) q) = smult (inverse (lead_coeff G)) (F div H)" by (metis (mono_tags) MP_Rel_def M_to_int_mod_ring Mp_Rel_F_div_H Mp_f_representative of_int_hom.map_poly_hom_smult pm.mod_ring_rel_def rel_inverse_p right_unique_MP_Rel right_unique_def to_int_mod_ring_hom.injectivity to_int_mod_ring_of_int_M) thus ?thesis using Mp_Rel_F_div_H unfolding MP_Rel_def a F_div_G Mp_f_representative by auto qed moreover have "MP_Rel b (F mod G)" using Mp_Rel_F_mod_H b H inverse_zero_imp_zero lc_G by (metis mod_smult_right) ultimately show ?thesis by auto next assume Mp_g_0: "¬ Mp g ≠ 0" hence "pdivmod2 f g = (0, f)" unfolding pdivmod2_def by auto hence a: "a = 0" and b: "b = f" using 3 by auto have G0: "G = 0" using Mp_g_0 2 unfolding MP_Rel_def by auto have "MP_Rel a (F div G)" unfolding MP_Rel_def G0 a by auto moreover have "MP_Rel b (F mod G)" using 1 unfolding MP_Rel_def G0 a b by auto ultimately show ?thesis by simp qed thus "MP_Rel a (F div G)" and "MP_Rel b (F mod G)" by auto qed subsection ‹Executable division operation modulo $m$ for polynomials› lemma dvdm_iff_Mp_pdivmod2: shows "g dvdm f = (Mp (snd (pdivmod2 f g)) = 0)" proof - let ?F="(of_int_poly f)::'a mod_ring poly" let ?G="(of_int_poly g)::'a mod_ring poly" have a[transfer_rule]: "MP_Rel f ?F" by (simp add: MP_Rel_def Mp_f_representative) have b[transfer_rule]: "MP_Rel g ?G" by (simp add: MP_Rel_def Mp_f_representative) have "MP_Rel_Pair (pdivmod2 f g) (pdivmod ?F ?G)" using pdivmod2_rel unfolding rel_fun_def using a b by auto hence "MP_Rel (snd (pdivmod2 f g)) (snd (pdivmod ?F ?G))" unfolding MP_Rel_Pair_def by auto hence "(Mp (snd (pdivmod2 f g)) = 0) = (snd (pdivmod ?F ?G) = 0)" unfolding MP_Rel_def by auto thus ?thesis using dvdm_iff_pdivmod0 by auto qed end lemmas (in poly_mod_prime) dvdm_pdivmod = poly_mod_prime_type.dvdm_iff_Mp_pdivmod2 [unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty] lemma (in poly_mod) dvdm_code: "g dvdm f = (if prime m then Mp (snd (pdivmod2 f g)) = 0 else Code.abort (STR ''dvdm error: m is not a prime number'') (λ _. g dvdm f))" using poly_mod_prime.dvdm_pdivmod[unfolded poly_mod_prime_def] by auto declare poly_mod.pdivmod2_def[code] declare poly_mod.dvdm_code[code] end

# Theory LLL_Factorization_Impl

(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹The LLL factorization algorithm› text ‹This theory contains an implementation of a polynomial time factorization algorithm. It first constructs a modular factorization. Afterwards it recursively invokes the LLL basis reduction algorithm on one lattice to either split a polynomial into two non-trivial factors, or to deduce irreducibility.› theory LLL_Factorization_Impl imports LLL_Basis_Reduction.LLL_Certification Factor_Bound_2 Missing_Dvd_Int_Poly Berlekamp_Zassenhaus.Berlekamp_Zassenhaus begin hide_const (open) up_ring.coeff up_ring.monom Unique_Factorization.factors Divisibility.factors Unique_Factorization.factor Divisibility.factor Divisibility.prime (* Implementation of a polynomial-time factoring algorithm for ℤ[X], based on the book "Modern Computer Algebra", second edition, pages 477-480. *) (*The following function obtains the generators of the lattice L ⊆ Z^j - L = {ux^i: 0≤i≤j-d}∪{mx^i: 0≤i≤d} - d = degree u. - We have to complete with zeroes up to dimension j *) definition factorization_lattice where "factorization_lattice u k m ≡ map (λi. vec_of_poly_n (u * monom 1 i) (degree u + k)) [k>..0] @ map (λi. vec_of_poly_n (monom m i) (degree u + k)) [degree u >..0]" fun min_degree_poly :: "int poly ⇒ int poly ⇒ int poly" where "min_degree_poly a b = (if degree a ≤ degree b then a else b)" fun choose_u :: "int poly list ⇒ int poly" where "choose_u [] = undefined" | "choose_u [gi] = gi" | "choose_u (gi # gj # gs) = min_degree_poly gi (choose_u (gj # gs))" lemma factorization_lattice_code[code]: "factorization_lattice u k m = ( let n = degree u in map (λi. vec_of_poly_n (monom_mult i u) (n+k)) [k>..0] @ map (λi. vec_of_poly_n (monom m i) (n+k)) [n>..0] )" unfolding factorization_lattice_def monom_mult_def by (auto simp: ac_simps Let_def) text ‹Optimization: directly try to minimize coefficients of polynomial $u$.› definition LLL_short_polynomial where "LLL_short_polynomial pl n u = poly_of_vec (short_vector_hybrid 2 (factorization_lattice (poly_mod.inv_Mp pl (poly_mod.Mp pl u)) (n - degree u) pl))" locale LLL_implementation = fixes p pl :: int begin function LLL_many_reconstruction where "LLL_many_reconstruction f us = (let d = degree f; d2 = d div 2; f2_opt = find_map_filter (λ u. gcd f (LLL_short_polynomial pl (Suc d2) u)) (λ f2. let deg = degree f2 in deg > 0 ∧ deg < d) (filter (λ u. degree u ≤ d2) us) in case f2_opt of None ⇒ [f] | Some f2 ⇒ let f1 = f div f2; (us1, us2) = List.partition (λ gi. poly_mod.dvdm p gi f1) us in LLL_many_reconstruction f1 us1 @ LLL_many_reconstruction f2 us2)" by pat_completeness auto termination proof (relation "measure (λ (f,us). degree f)", goal_cases) case (3 f us d d2 f2_opt f2 f1 pair us1 us2) from find_map_filter_Some[OF 3(4)[unfolded 3(3) Let_def]] 3(1,5) show ?case by auto next case (2 f us d d2 f2_opt f2 f1 pair us1 us2) from find_map_filter_Some[OF 2(4)[unfolded 2(3) Let_def]] 2(1,5) have f: "f = f1 * f2" and f0: "f ≠ 0" and deg: "degree f2 > 0" "degree f2 < degree f" by auto have "degree f = degree f1 + degree f2" using f0 unfolding f by (subst degree_mult_eq, auto) with deg show ?case by auto qed auto function LLL_reconstruction where "LLL_reconstruction f us = (let d = degree f; u = choose_u us; g = LLL_short_polynomial pl d u; f2 = gcd f g; deg = degree f2 in if deg = 0 ∨ deg ≥ d then [f] else let f1 = f div f2; (us1, us2) = List.partition (λ gi. poly_mod.dvdm p gi f1) us in LLL_reconstruction f1 us1 @ LLL_reconstruction f2 us2)" by pat_completeness auto termination proof (relation "measure (λ (f,us). degree f)", goal_cases) case (2 f us d u g f2 deg f1 pair us1 us2) hence f: "f = f1 * f2" and f0: "f ≠ 0" by auto have deg: "degree f = degree f1 + degree f2" using f0 unfolding f by (subst degree_mult_eq, auto) from 2 have "degree f2 > 0" "degree f2 < degree f" by auto thus ?case using deg by auto qed auto end declare LLL_implementation.LLL_reconstruction.simps[code] declare LLL_implementation.LLL_many_reconstruction.simps[code] definition LLL_factorization :: "int poly ⇒ int poly list" where "LLL_factorization f = (let ― ‹find suitable prime› p = suitable_prime_bz f; ― ‹compute finite field factorization› (_, fs) = finite_field_factorization_int p f; ― ‹determine exponent l and B› n = degree f; no = ∥f∥⇧^{2}; B = sqrt_int_ceiling (2^(5 * (n - 1) * (n - 1)) * no^(2 * (n - 1))); l = find_exponent p B; ― ‹perform hensel lifting to lift factorization to mod $p^l$› us = hensel_lifting p l f fs; ― ‹reconstruct integer factors via LLL algorithm› pl = p^l in LLL_implementation.LLL_reconstruction p pl f us)" definition LLL_many_factorization :: "int poly ⇒ int poly list" where "LLL_many_factorization f = (let ― ‹find suitable prime› p = suitable_prime_bz f; ― ‹compute finite field factorization› (_, fs) = finite_field_factorization_int p f; ― ‹determine exponent l and B› n = degree f; no = ∥f∥⇧^{2}; B = sqrt_int_ceiling (2^(5 * (n div 2) * (n div 2)) * no^(2 * (n div 2))); l = find_exponent p B; ― ‹perform hensel lifting to lift factorization to mod $p^l$› us = hensel_lifting p l f fs; ― ‹reconstruct integer factors via LLL algorithm› pl = p^l in LLL_implementation.LLL_many_reconstruction p pl f us)" end

# Theory LLL_Factorization

(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Correctness of the LLL factorization algorithm› text ‹This theory connects short vectors of lattices and factors of polynomials. From this connection, we derive soundness of the lattice based factorization algorithm. › theory LLL_Factorization imports LLL_Factorization_Impl Berlekamp_Zassenhaus.Factorize_Int_Poly begin subsection ‹Basic facts about the auxiliary functions› hide_const (open) module.smult lemma nth_factorization_lattice: fixes u and d defines "n ≡ degree u" assumes "i < n + d" shows "factorization_lattice u d m ! i = vec_of_poly_n (if i < d then u * monom 1 (d - Suc i) else monom m (n+d-Suc i)) (n+d)" using assms by (unfold factorization_lattice_def, auto simp: nth_append smult_monom Let_def not_less) lemma length_factorization_lattice[simp]: shows "length (factorization_lattice u d m) = degree u + d" by (auto simp: factorization_lattice_def Let_def) lemma dim_factorization_lattice: assumes "x < degree u + d" shows "dim_vec (factorization_lattice u d m ! x) = degree u + d" unfolding factorization_lattice_def using assms nth_append by (simp add: nth_append Let_def) lemma dim_factorization_lattice_element: assumes "x ∈ set (factorization_lattice u d m)" shows "dim_vec x = degree u + d" using assms by (auto simp: factorization_lattice_def Let_def) lemma set_factorization_lattice_in_carrier[simp]: "set (factorization_lattice u d m) ⊆ carrier_vec (degree u + d)" using dim_factorization_lattice by (auto simp: factorization_lattice_def Let_def) lemma choose_u_Cons: "choose_u (x#xs) = (if xs = [] then x else min_degree_poly x (choose_u xs))" by (cases xs, auto) lemma choose_u_member: "xs ≠ [] ⟹ choose_u xs ∈ set xs" by (induct xs, auto simp: choose_u_Cons) declare choose_u.simps[simp del] subsection ‹Facts about Sylvester matrices and norms› lemma (in LLL) lattice_is_span [simp]: "lattice_of xs = span_list xs" by (unfold lattice_of_def span_list_def lincomb_list_def image_def, auto) lemma sq_norm_row_sylvester_mat1: fixes f g :: "'a :: conjugatable_ring poly" assumes i: "i < degree g" shows "∥(row (sylvester_mat f g) i)∥⇧^{2}= ∥f∥⇧^{2}" proof (cases "f = 0") case True thus ?thesis by (auto simp add: sylvester_mat_def row_def sq_norm_vec_def o_def interv_sum_list_conv_sum_set_nat i intro!: sum_list_zero) next case False note f = False let ?f = "λj. if i ≤ j ∧ j - i ≤ degree f then coeff f (degree f + i - j) else 0" let ?h = "λj. j + i" let ?row = "vec (degree f + degree g) ?f " let ?g = "λj. degree f - j" have image_g: "?g ` {0..<Suc (degree f)} = {0..<Suc (degree f)}" by (auto simp add: image_def) (metis (no_types, hide_lams) Nat.add_diff_assoc add.commute add_diff_cancel_left' atLeastLessThan_iff diff_Suc_Suc diff_Suc_less less_Suc_eq_le zero_le) have bij_h: "bij_betw ?h {0..<Suc (degree f)} {i..< Suc (degree f + i)}" unfolding bij_betw_def image_def by (auto, metis atLeastLessThan_iff le_add_diff_inverse2 less_diff_conv linorder_not_less not_less_eq zero_order(3)) have "∥row (sylvester_mat f g) i∥⇧^{2}= ∥?row∥⇧^{2}" by (rule arg_cong[of _ _ "sq_norm_vec"], insert i, auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def) also have "... = sum_list (map (sq_norm ∘ ?f) [0..<degree f + degree g])" unfolding sq_norm_vec_def by auto also have "... = sum (sq_norm ∘ ?f) {0..<degree f + degree g}" unfolding interv_sum_list_conv_sum_set_nat by auto also have "... = sum (sq_norm ∘ ?f) {i..< Suc (degree f + i)}" by (rule sum.mono_neutral_right, insert i, auto) also have "... = sum ((sq_norm ∘ ?f) ∘ ?h) {0..<Suc (degree f)}" by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h]) also have "... = sum (λj. sq_norm (coeff f (degree f - j))) {0..<Suc (degree f)}" by (rule sum.cong, auto) also have "... = sum ((λj. sq_norm (coeff f j)) ∘ ?g) {0..<Suc (degree f)}" unfolding o_def .. also have "... = sum (λj. sq_norm (coeff f j)) (?g ` {0..<Suc (degree f)})" by (rule sum.reindex[symmetric], auto simp add: inj_on_def) also have "... = sum (sq_norm ∘ coeff f) {0..<Suc (degree f)}" unfolding image_g by simp also have "... = sum_list (map sq_norm (coeffs f))" unfolding coeffs_def using f by (simp add: interv_sum_list_conv_sum_set_nat) finally show ?thesis unfolding sq_norm_poly_def by auto qed lemma sq_norm_row_sylvester_mat2: fixes f g :: "'a :: conjugatable_ring poly" assumes i1: "degree g ≤ i" and i2: "i < degree f + degree g" shows "∥row (sylvester_mat f g) i∥⇧^{2}= ∥g∥⇧^{2}" proof - let ?f = "λj. if i - degree g ≤ j ∧ j ≤ i then coeff g (i - j) else 0" let ?row = "vec (degree f + degree g) ?f" let ?h = "λj. j + i - degree g" let ?g = "λj. degree g - j" have image_g: "?g ` {0..<Suc (degree g)} = {0..<Suc (degree g)}" by (auto simp add: image_def) (metis atLeastLessThan_iff diff_diff_cancel diff_le_self less_Suc_eq_le zero_le) have x: "x - (i - degree g) ≤ degree g" if x: "x < Suc i" for x using x by auto have bij_h: "bij_betw ?h {0..<Suc (degree g)} {i - degree g..<Suc i}" unfolding bij_betw_def inj_on_def using i1 i2 unfolding image_def by (auto, metis (no_types) Nat.add_diff_assoc atLeastLessThan_iff x less_Suc_eq_le less_eq_nat.simps(1) ordered_cancel_comm_monoid_diff_class.diff_add) have "∥row (sylvester_mat f g) i∥⇧^{2}= ∥?row∥⇧^{2}" by (rule arg_cong[of _ _ "sq_norm_vec"], insert i1 i2, auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def) also have "... = sum_list (map (sq_norm ∘ ?f) [0..<degree f + degree g])" unfolding sq_norm_vec_def by auto also have "... = sum (sq_norm ∘ ?f) {0..<degree f + degree g}" unfolding interv_sum_list_conv_sum_set_nat by auto also have "... = sum (sq_norm ∘ ?f) {i - degree g..< Suc i}" by (rule sum.mono_neutral_right, insert i2, auto) also have "... = sum ((sq_norm ∘ ?f) ∘ ?h) {0..<Suc (degree g)}" by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h]) also have "... = sum (λj. sq_norm (coeff g (degree g - j))) {0..<Suc (degree g)}" by (rule sum.cong, insert i1, auto) also have "... = sum ((λj. sq_norm (coeff g j)) ∘ ?g) {0..<Suc (degree g)}" unfolding o_def .. also have "... = sum (λj. sq_norm (coeff g j)) (?g ` {0..<Suc (degree g)})" by (rule sum.reindex[symmetric], auto simp add: inj_on_def) also have "... = sum (sq_norm ∘ coeff g) {0..<Suc (degree g)}" unfolding image_g by simp also have "... = sum_list (map sq_norm (coeffs g))" unfolding coeffs_def by (simp add: interv_sum_list_conv_sum_set_nat) finally show ?thesis unfolding sq_norm_poly_def by auto qed lemma Hadamard's_inequality_int: fixes A::"int mat" assumes A: "A ∈ carrier_mat n n" shows "¦det A¦ ≤ sqrt (of_int (prod_list (map sq_norm (rows A))))" proof - let ?A = "map_mat real_of_int A" have "¦det A¦ = ¦det ?A¦" unfolding of_int_hom.hom_det by simp also have "… ≤ sqrt (prod_list (map sq_norm (rows ?A)))" by (rule Hadamard's_inequality[of ?A n], insert A, auto) also have "… = sqrt (of_int (prod_list (map sq_norm (rows A))))" unfolding of_int_hom.hom_prod_list map_map by (rule arg_cong[of _ _ "λ x. sqrt (prod_list x)"], rule nth_equalityI, force, auto simp: sq_norm_of_int[symmetric] row_def intro!: arg_cong[of _ _ sq_norm_vec]) finally show ?thesis . qed lemma resultant_le_prod_sq_norm: fixes f g::"int poly" defines "n ≡ degree f" and "k ≡ degree g" shows "¦resultant f g¦ ≤ sqrt (of_int (∥f∥⇧^{2}^k * ∥g∥⇧^{2}^n))" proof - let ?S = "sylvester_mat f g" let ?f = "sq_norm ∘ row ?S" have map_rw1: "map ?f [0..<degree g] = replicate k ∥f∥⇧^{2}" proof (rule nth_equalityI) let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [0..<degree g]" show "length ?M = length (replicate k ∥f∥⇧^{2})" using k_def by auto show "?M ! i = replicate k ∥f∥⇧^{2}! i" if i: "i < length ?M" for i proof - have ik: "i<k" using i k_def by auto hence i_deg_g: "i < degree g" using k_def by auto have "replicate k ∥f∥⇧^{2}! i = ∥f∥⇧^{2}" by (rule nth_replicate[OF ik]) also have "... = (sq_norm ∘ row (sylvester_mat f g)) (0 + i)" using sq_norm_row_sylvester_mat1 ik k_def by force also have "... = ?M ! i" by (rule nth_map_upt[symmetric], simp add: i_deg_g) finally show "?M ! i = replicate k ∥f∥⇧^{2}! i" .. qed qed have map_rw2: "map ?f [degree g..<degree f + degree g] = replicate n ∥g∥⇧^{2}" proof (rule nth_equalityI) let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [degree g..<degree f + degree g]" show "length ?M = length (replicate n ∥g∥⇧^{2})" by (simp add: n_def) show "?M ! i = replicate n ∥g∥⇧^{2}! i" if "i<length ?M" for i proof - have i_n: "i<n" using n_def that by auto hence i_deg_f: "i < degree f" using n_def by auto have "replicate n ∥g∥⇧^{2}! i = ∥g∥⇧^{2}" by (rule nth_replicate[OF i_n]) also have "... = (sq_norm ∘ row (sylvester_mat f g)) (degree g + i)" using i_n n_def by (simp add: sq_norm_row_sylvester_mat2) also have "... = ?M ! i" by (simp add: i_deg_f) finally show "?M ! i = replicate n ∥g∥⇧^{2}! i" .. qed qed have p1: "prod_list (map ?f [0..<degree g]) = ∥f∥⇧^{2}^k" unfolding map_rw1 by (rule prod_list_replicate) have p2: "prod_list (map ?f [degree g..<degree f + degree g]) = ∥g∥⇧^{2}^n" unfolding map_rw2 by (rule prod_list_replicate) have list_rw: "[0..<degree f + degree g] = [0..<degree g] @ [degree g..<degree f + degree g]" by (metis add.commute upt_add_eq_append zero_le) have "¦resultant f g¦ = ¦det ?S¦" unfolding resultant_def .. also have "... ≤ sqrt (of_int (prod_list (map sq_norm (rows ?S))))" by (rule Hadamard's_inequality_int, auto) also have "map sq_norm (rows ?S) = map ?f [0..<degree f + degree g]" unfolding Matrix.rows_def by auto also have "... = map ?f ([0..<degree g] @ [degree g..<degree f + degree g])" by (simp add: list_rw) also have "prod_list ... = prod_list (map ?f [0..<degree g]) * prod_list (map ?f [degree g..<degree f + degree g])" by auto finally show ?thesis unfolding p1 p2 . qed subsection ‹Proof of the key lemma 16.20› (* Lemma 16.20 *) lemma common_factor_via_short: fixes f g u :: "int poly" defines "n ≡ degree f" and "k ≡ degree g" assumes n0: "n > 0" and k0: "k > 0" and monic: "monic u" and deg_u: "degree u > 0" and uf: "poly_mod.dvdm m u f" and ug: "poly_mod.dvdm m u g" and short: "∥f∥⇧^{2}^k * ∥g∥⇧^{2}^n < m⇧^{2}" and m: "m ≥ 0" shows "degree (gcd f g) > 0" proof - interpret poly_mod m . have f_not0: "f ≠ 0" and g_not0: "g ≠ 0" using n0 k0 k_def n_def by auto have deg_f: "degree f > 0" using n0 n_def by simp have deg_g: "degree g > 0" using k0 k_def by simp obtain s t where deg_s: "degree s < degree g" and deg_t: "degree t < degree f" and res_eq: "[:resultant f g:] = s * f + t * g" and s_not0: "s ≠ 0" and t_not0: "t ≠ 0" using resultant_as_nonzero_poly[OF deg_f deg_g] by auto have res_eq_modulo: "[:resultant f g:] =m s * f + t * g" using res_eq by simp have u_dvdm_res: "u dvdm [:resultant f g:]" proof (unfold res_eq, rule dvdm_add) show "u dvdm s * f" using dvdm_factor[OF uf, of s] unfolding mult.commute[of f s] by auto show "u dvdm t * g" using dvdm_factor[OF ug, of t] unfolding mult.commute[of g t] by auto qed have res_0_mod: "resultant f g mod m = 0" by (rule monic_dvdm_constant[OF u_dvdm_res monic deg_u]) have res0: "resultant f g = 0" proof (rule mod_0_abs_less_imp_0) show "[resultant f g = 0] (mod m)" using res_0_mod unfolding cong_def by auto have "¦resultant f g¦ ≤ sqrt ((sq_norm_poly f)^k * (sq_norm_poly g)^n)" unfolding k_def n_def by (rule resultant_le_prod_sq_norm) also have "... < m" proof (rule real_less_lsqrt) show "0 ≤ real_of_int (∥f∥⇧^{2}^ k * ∥g∥⇧^{2}^ n)" by (simp add: sq_norm_poly_ge_0) show "0 ≤ real_of_int m" using m by simp show "real_of_int (∥f∥⇧^{2}^ k * ∥g∥⇧^{2}^ n) < (real_of_int m)⇧^{2}" by (metis of_int_less_iff of_int_power short) qed finally show "¦resultant f g¦ < m" using of_int_less_iff by blast qed have "¬ coprime f g" by (rule resultant_zero_imp_common_factor, auto simp add: deg_f res0) thus ?thesis using res0 resultant_0_gcd by auto qed subsection ‹Properties of the computed lattice and its connection with Sylvester matrices› lemma factorization_lattice_as_sylvester: fixes p :: "'a :: semidom poly" assumes dj: "d ≤ j" and d: "degree p = d" shows "mat_of_rows j (factorization_lattice p (j-d) m) = sylvester_mat_sub d (j-d) p [:m:]" proof (cases "p=0") case True have deg_p: "d = 0" using True d by simp show ?thesis by (auto simp add: factorization_lattice_def True deg_p mat_of_rows_def d) next case p0: False note 1 = degree_mult_eq[OF p0, of "monom _ _", unfolded monom_eq_0_iff, OF one_neq_zero] from dj show ?thesis apply (cases "m = 0") apply (auto simp: mat_eq_iff d[symmetric] 1 coeff_mult_monom sylvester_mat_sub_index mat_of_rows_index nth_factorization_lattice vec_index_of_poly_n degree_monom_eq coeff_const) done qed context inj_comm_semiring_hom begin lemma map_poly_hom_mult_monom [hom_distribs]: "map_poly hom (p * monom a n) = map_poly hom p * monom (hom a) n" by (auto intro!: poly_eqI simp:coeff_mult_monom hom_mult) lemma hom_vec_of_poly_n [hom_distribs]: "map_vec hom (vec_of_poly_n p n) = vec_of_poly_n (map_poly hom p) n" by (auto simp: vec_index_of_poly_n) lemma hom_factorization_lattice [hom_distribs]: shows "map (map_vec hom) (factorization_lattice u k m) = factorization_lattice (map_poly hom u) k (hom m)" by (auto intro!:arg_cong[of _ _ "λp. vec_of_poly_n p _"] simp: list_eq_iff_nth_eq nth_factorization_lattice hom_vec_of_poly_n map_poly_hom_mult_monom) end subsection ‹Proving that @{const factorization_lattice} returns a basis of the lattice› context LLL begin sublocale idom_vec n "TYPE(int)". (*In this context, "n" is fixed by the locale and corresponds to "j" in the book*) lemma upper_triangular_factorization_lattice: fixes u :: "'a :: semidom poly" and d :: nat assumes d: "d ≤ n" and du: "d = degree u" shows "upper_triangular (mat_of_rows n (factorization_lattice u (n-d) k))" (is "upper_triangular ?M") proof (intro upper_triangularI, unfold mat_of_rows_carrier length_factorization_lattice) fix i j assume ji: "j < i" and i: "i < degree u + (n - d)" with d du have jn: "j < n" by auto show "?M $$ (i,j) = 0" proof (cases "u=0") case True with ji i show ?thesis by (auto simp: factorization_lattice_def mat_of_rows_def) next case False then show ?thesis using d ji i apply (simp add: du mat_of_rows_index nth_factorization_lattice) apply (auto simp: vec_index_of_poly_n[OF jn] degree_mult_eq degree_monom_eq) done qed qed lemma factorization_lattice_diag_nonzero: fixes u :: "'a :: semidom poly" and d assumes d: "d=degree u" and dn: "d≤n" and u: "u≠0" and m0: "k≠0" and i: "i<n" shows "(factorization_lattice u (n-d) k) ! i $ i ≠ 0" proof- have 1: "monom (1::'a) (n - Suc (degree u + i)) ≠ 0" using m0 by auto have 2: "i < degree u + (n - d)" using i d by auto let ?p = "u * monom 1 (n - Suc (degree u + i))" have 3: "i < n - degree u ⟹ degree (?p) = n - Suc i" using assms by (auto simp: degree_mult_eq[OF _ 1] degree_monom_eq) show ?thesis apply (unfold nth_factorization_lattice[OF 2] vec_index_of_poly_n[OF 2]) using assms leading_coeff_0_iff[of ?p] apply (cases "i < n - degree u", auto simp: d 3 degree_monom_eq) done qed corollary factorization_lattice_diag_nonzero_RAT: fixes d assumes "d=degree u" and "d≤n" and "u≠0" and "k≠0" and "i<n" shows "RAT (factorization_lattice u (n-d) k) ! i $ i ≠ 0" using factorization_lattice_diag_nonzero[OF assms] assms by (auto simp: nth_factorization_lattice) sublocale gs: vec_space "TYPE(rat)" n. lemma lin_indpt_list_factorization_lattice: fixes d assumes d: "d = degree u" and dn: "d ≤ n" and u: "u ≠ 0" and k: "k ≠ 0" shows "gs.lin_indpt_list (RAT (factorization_lattice u (n-d) k))" (is "gs.lin_indpt_list (RAT ?vs)") proof- have 1: "rows (mat_of_rows n (map (map_vec rat_of_int) ?vs)) = map (map_vec rat_of_int) ?vs" using dn d by (subst rows_mat_of_rows, auto dest!: subsetD[OF set_factorization_lattice_in_carrier]) note 2 = factorization_lattice_diag_nonzero_RAT[OF d dn u k] show ?thesis apply (intro gs.upper_triangular_imp_lin_indpt_list[of "mat_of_rows n (RAT ?vs)", unfolded 1]) using assms 2 by (auto simp: diag_mat_def mat_of_rows_index hom_distribs intro!:upper_triangular_factorization_lattice) qed end subsection ‹Being in the lattice is being a multiple modulo› lemma (in semiring_hom) hom_poly_of_vec: "map_poly hom (poly_of_vec v) = poly_of_vec (map_vec hom v)" by (auto simp add: coeff_poly_of_vec poly_eq_iff) abbreviation "of_int_vec ≡ map_vec of_int" context LLL begin lemma lincomb_to_dvd_modulo: fixes u d defines "d ≡ degree u" assumes d: "d ≤ n" and lincomb: "lincomb_list c (factorization_lattice u (n-d) k) = g" (is "?l = ?r") shows "poly_mod.dvdm k u (poly_of_vec g)" proof- let ?S = "sylvester_mat_sub d (n - d) u [:k:]" define q where "q ≡ poly_of_vec (vec_first (vec n c) (n - d))" define r where "r ≡ poly_of_vec (vec_last (vec n c) d)" have "?l = ?S⇧^{T}*⇩_{v}vec n c" apply (subst lincomb_list_as_mat_mult) using d d_def apply (force simp:factorization_lattice_def) apply (fold transpose_mat_of_rows) using d d_def by (simp add: factorization_lattice_as_sylvester) also have "poly_of_vec … = q * u + smult k r" apply (subst sylvester_sub_poly) using d_def d q_def r_def by auto finally have "… = poly_of_vec g" unfolding lincomb of_int_hom.hom_poly_of_vec by auto then have "poly_of_vec g = q * u + Polynomial.smult k r" by auto then have "poly_mod.Mp k (poly_of_vec g) = poly_mod.Mp k (q * u + Polynomial.smult k r)" by auto also have "... = poly_mod.Mp k (q * u + poly_mod.Mp k (Polynomial.smult k r))" using poly_mod.plus_Mp(2) by auto also have "... = poly_mod.Mp k (q * u)" using poly_mod.plus_Mp(2) unfolding poly_mod.Mp_smult_m_0 by simp also have "... = poly_mod.Mp k (u * q)" by (simp add: mult.commute) finally show ?thesis unfolding poly_mod.dvdm_def by auto qed (* There is a typo in the textbook (page 476). The book states q' = q'' * u + r'' and the correct fact is r' = q'' * u+r'' *) lemma dvd_modulo_to_lincomb: fixes u :: "int poly" and d defines "d ≡ degree u" assumes d: "d < n" and dvd: "poly_mod.dvdm k u (poly_of_vec g)" and k_not0: "k≠0" and monic_u: "monic u" and dim_g: "dim_vec g = n" and deg_u: "degree u > 0" shows "∃c. lincomb_list c (factorization_lattice u (n-d) k) = g" proof - interpret p: poly_mod k . have u_not0: "u ≠ 0" using monic_u by auto hence n[simp]: "0 < n" using d by auto obtain q' r' where g: "poly_of_vec g = q' * u + smult k r'" using p.dvdm_imp_div_mod[OF dvd] by auto obtain q'' r'' where r': "r' = q'' * u + r''" and deg_r'': "degree r''<degree u" using monic_imp_div_mod_int_poly_degree2[OF monic_u deg_u, of r'] by auto (*The following fact is explained in the paragraph below equation (6) in page 476 of the textbook*) have g1: "poly_of_vec g = (q' + smult k q'') * u + smult k r''" unfolding g r' by (metis (no_types, lifting) combine_common_factor mult_smult_left smult_add_right) define q where q: "q = (q' + smult k q'')" define r where r: "r = r''" have degree_q: "q = 0 ∨ degree (q' + smult k q'') < n - d" proof (cases "q = 0",auto, rule degree_div_mod_smult[OF _ _ _ g1]) show "degree (poly_of_vec g) < n" by (rule degree_poly_of_vec_less, auto simp add: dim_g) show "degree r'' < d" using deg_r'' unfolding d_def . assume "q≠0" thus "q' + smult k q'' ≠ 0" unfolding q . show "k ≠ 0" by fact show "degree u = d" using d_def by auto qed have g2: "(vec_of_poly_n (q*u) n) + (vec_of_poly_n (smult k r) n) = g" proof - have "g = vec_of_poly_n (poly_of_vec g) n" by (rule vec_of_poly_n_poly_of_vec[symmetric], auto simp add: dim_g) also have "… = vec_of_poly_n ((q' + smult k q'') * u + smult k r'') n" using g1 by auto also have "... = vec_of_poly_n (q * u + smult k r'') n" unfolding q by auto also have "... = vec_of_poly_n (q * u) n + vec_of_poly_n (smult k r'') n" by (rule vec_of_poly_n_add) finally show ?thesis unfolding r by simp qed let ?c = "λi. if i < n - d then coeff q (n - d - 1 - i) else coeff r (n - Suc i)" let ?c1 = "λi. ?c i ⋅⇩_{v}factorization_lattice u (n-d) k ! i" show ?thesis proof (rule exI[of _ ?c]) let ?part1 = "map (λi. vec_of_poly_n (u * monom 1 i) n) [n-d>..0]" let ?part2 = "map (λi. vec_of_poly_n (monom k i) n) [d>..0]" have [simp]: "dim_vec (M.sumlist (map ?c1 [0..<n - d])) = n" by (rule dim_sumlist, auto simp add: dim_factorization_lattice d_def) have [simp]: "dim_vec (M.sumlist (map ?c1 [n-d..<n])) = n" by (rule dim_sumlist, insert d, auto simp add: dim_factorization_lattice d_def) have [simp]: "factorization_lattice u (n-d) k ! x ∈ carrier_vec n" if x: "x < n" for x using x dim_factorization_lattice_element nth_factorization_lattice[of x u "n-d"] d by (auto simp: d_def) have "[0..<length (factorization_lattice u (n-d) k)] = [0..<n]" using d by (simp add: d_def less_imp_le_nat) also have "... = [0..<n - d] @ [n-d..<n]" by (rule upt_minus_eq_append, auto) finally have list_rw: "[0..<length (factorization_lattice u (n-d) k)] = [0..<n - d] @ [n-d..<n]" . have qu1: "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = q*u" proof - have "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = poly_of_vec (⨁⇘_{V}⇙i∈{0..<n-d}. ?c1 i)" by (subst sumlist_map_as_finsum, auto) also have "... = poly_of_vec (⨁⇘_{V}⇙i∈set [0..<n-d]. ?c1 i)" by auto also have "... = sum (λi. poly_of_vec (?c1 i)) (set [0..<n-d])" by (auto simp:poly_of_vec_finsum) also have "... = sum (λi. poly_of_vec (?c1 i)) {0..<n-d}" by auto also have "... = q*u" proof - have deg: "degree (u * monom 1 (n - Suc (d + i))) < n" if i: "i < n - d" for i proof - let ?m="monom (1::int) (n - Suc (d + i))" have monom_not0: "?m ≠ 0" using i by auto have deg_m: "degree ?m = n - Suc (d + i)" by (rule degree_monom_eq, auto) have "degree (u * ?m) = d + (n - Suc (d + i))" using degree_mult_eq[OF u_not0 monom_not0] d_def deg_m by auto also have "... < n" using i by auto finally show ?thesis . qed have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n" if i: "i< n - d" for i apply (subst nth_factorization_lattice) using i by (auto simp:d_def) have q_rw: "q = (∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" proof (auto simp add: poly_eq_iff coeff_sum) fix j let ?m = "n-d-1-j" let ?f = "λx. coeff q (n - Suc (d + x)) * (if n - Suc (d + x) = j then 1 else 0)" have set_rw: "{0..<n-d} = insert ?m ({0..<n-d} - {?m})" using d by auto have sum0: "(∑x ∈ {0..<n-d} - {?m}. ?f x) = 0" by (rule sum.neutral, auto) have "(∑x = 0..<n - d. ?f x) = (∑x ∈ insert ?m ({0..<n-d} - {?m}). ?f x)" using set_rw by presburger also have "... = ?f ?m + (∑x ∈ {0..<n-d} - {?m}. ?f x)" by (rule sum.insert, auto) also have "... = ?f ?m" unfolding sum0 by auto also have "... = coeff q j" proof (cases "j < n - d") case True then show ?thesis by auto next case False have "j>degree q" using degree_q q False d by auto then show ?thesis using coeff_eq_0 by auto qed finally show "coeff q j = (∑i = 0..<n - d. coeff q (n - Suc (d + i)) * (if n - Suc (d + i) = j then 1 else 0))" .. qed have "sum (λi. poly_of_vec (?c1 i)) {0..<n-d} = (∑i = 0..<n - d. poly_of_vec (coeff q (n - Suc (d + i)) ⋅⇩_{v}factorization_lattice u (n-d) k ! i))" by (rule sum.cong, auto) also have "... = (∑i = 0..<n - d. (poly_of_vec (coeff q (n - Suc (d + i)) ⋅⇩_{v}(vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n))))" by (rule sum.cong, auto simp add: lattice_rw) also have "... = (∑i = 0..<n - d. smult (coeff q (n - Suc (d + i))) (u * monom 1 (n - Suc (d + i))))" by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg]) also have "... = (∑i = 0..<n - d. u*(smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" by auto also have "... = u *(∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" by (rule sum_distrib_left[symmetric]) also have "... = u * q" using q_rw by auto also have "... = q*u" by auto finally show ?thesis . qed finally show ?thesis . qed have qu: "M.sumlist (map ?c1 [0..<n - d]) = vec_of_poly_n (q*u) n" proof - have "vec_of_poly_n (q*u) n = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n" using qu1 by auto also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n = M.sumlist (map ?c1 [0..<n - d])" by (rule vec_of_poly_n_poly_of_vec, auto) finally show ?thesis .. qed have rm1: "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = smult k r" proof - have "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = poly_of_vec (⨁⇘_{V}⇙i∈{n-d..<n}. ?c1 i)" by (subst sumlist_map_as_finsum, auto) also have "... = poly_of_vec (⨁⇘_{V}⇙i∈set [n-d..<n]. ?c1 i)" by auto also have "... = sum (λi. poly_of_vec (?c1 i)) {n-d..<n}" by (auto simp: poly_of_vec_finsum) also have "... = smult k r" proof - have deg: "degree (monom k (n - Suc i)) < n" if i: "n-d≤i" and i2: "i<n" for i using degree_monom_le i i2 by (simp add: degree_monom_eq k_not0) have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (monom k (n - Suc i)) n" if i: "n - d ≤ i" and i2: "i<n" for i using i2 i d d_def by (subst nth_factorization_lattice, auto) have r_rw: "r = (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))" proof (auto simp add: poly_eq_iff coeff_sum) fix j show "coeff r j = (∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0)" proof (cases "j<d") case True have j_eq: "n - Suc (n - 1 - j) = j" using d True by auto let ?i = "n-1-j" let ?f ="λi. if n - Suc i = j then coeff r (n - Suc i) else 0" have sum0: "sum ?f ({n-d..<n} - {?i}) = 0" by (rule sum.neutral, auto) have "{n-d..<n} = insert ?i ({n-d..<n} - {?i})" using True by auto hence "sum ?f {n - d..<n} = sum ?f (insert ?i ({n-d..<n} - {?i}))" by auto also have "... = ?f ?i + sum ?f ({n-d..<n} - {?i})" by (rule sum.insert, auto) also have "... = coeff r j" unfolding sum0 j_eq by simp finally show ?thesis .. next case False hence "(∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0) = 0" by (intro sum.neutral ballI, insert False, simp, linarith) also have "... = coeff r j" by (rule coeff_eq_0[symmetric], insert False deg_r'' r d_def, auto) finally show ?thesis .. qed qed have "sum (λi. poly_of_vec (?c1 i)) {n-d..<n} = (∑i ∈ {n-d..<n}. poly_of_vec (coeff r (n - Suc i) ⋅⇩_{v}factorization_lattice u (n-d) k ! i))" by (rule sum.cong, auto) also have "... = (∑i ∈ {n-d..<n}. (poly_of_vec (coeff r (n - Suc i) ⋅⇩_{v}vec_of_poly_n (monom k (n - Suc i)) n)))" by (rule sum.cong, auto simp add: lattice_rw) also have "... = (∑i ∈ {n-d..<n}. smult (coeff r (n - Suc i)) (monom k (n - Suc i)))" by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg]) also have "... = (∑i ∈ {n-d..<n}. smult k (monom (coeff r (n - Suc i)) (n - Suc i)))" by (rule sum.cong, auto simp add: smult_monom smult_sum2) also have "... = smult k (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))" by (simp add: smult_sum2) also have "... = smult k r" using r_rw by auto finally show ?thesis . qed finally show ?thesis . qed have rm: "(M.sumlist (map ?c1 [n-d..<n])) = vec_of_poly_n (smult k r) n" proof - have "vec_of_poly_n (smult k r) n = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n" using rm1 by auto also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n = M.sumlist (map ?c1 [n-d..<n])" by (rule vec_of_poly_n_poly_of_vec, auto) finally show ?thesis .. qed have "lincomb_list ?c (factorization_lattice u (n-d) k) = M.sumlist (map ?c1 ([0..<n - d] @ [n-d..<n]))" unfolding lincomb_list_def list_rw by auto also have "... = M.sumlist (map ?c1 [0..<n - d] @ map ?c1 [n-d..<n])" by auto also have "... = M.sumlist (map ?c1 [0..<n - d]) + M.sumlist (map ?c1 [n-d..<n])" using d by (auto simp add: d_def nth_factorization_lattice intro!: M.sumlist_append) also have "... = vec_of_poly_n (q*u) n + vec_of_poly_n (smult k r) n" unfolding qu rm by auto also have "... = g" using g2 by simp finally show "lincomb_list ?c (factorization_lattice u (n-d) k) = g" . qed qed text ‹The factorization lattice precisely characterises the polynomials of a certain degree which divide $u$ modulo $M$.› lemma factorization_lattice: fixes M assumes deg_u: "degree u ≠ 0" and M: "M ≠ 0" shows "degree u ≤ n ⟹ n ≠ 0 ⟹ f ∈ poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M) ⟹ degree f < n ∧ poly_mod.dvdm M u f" "monic u ⟹ degree u < n ⟹ degree f < n ⟹ poly_mod.dvdm M u f ⟹ f ∈ poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M)" proof - from deg_u have deg_u: "degree u > 0" by auto let ?L = "factorization_lattice u (n - degree u) M" { assume deg: "degree f < n" and dvd: "poly_mod.dvdm M u f" and mon: "monic u" and deg_u_lt: "degree u < n" define fv where "fv = vec n (λ i. (coeff f (n - Suc i)))" have f: "f = poly_of_vec fv" unfolding fv_def poly_of_vec_def Let_def using deg by (auto intro!: poly_eqI coeff_eq_0 simp: coeff_sum) have dim_fv: "dim_vec fv = n" unfolding fv_def by simp from dvd_modulo_to_lincomb[OF deg_u_lt _ M mon _ deg_u(1), of fv, folded f, OF dvd dim_fv] obtain c where gv: "fv = lincomb_list c ?L" by auto have "fv ∈ lattice_of ?L" unfolding gv lattice_is_span by (auto simp: in_span_listI) thus "f ∈ poly_of_vec ` lattice_of ?L" unfolding f by auto } moreover { assume "f ∈ poly_of_vec ` lattice_of ?L" and deg_u: "degree u ≤ n" and n: "n ≠ 0" then obtain fv where f: "f = poly_of_vec fv" and fv: "fv ∈ lattice_of ?L" by auto from in_span_listE[OF fv[unfolded lattice_is_span]] obtain c where fv: "fv = lincomb_list c ?L" by auto from lincomb_to_dvd_modulo[OF _ fv[symmetric]] deg_u f have dvd: "poly_mod.dvdm M u f" by auto have "set ?L ⊆ carrier_vec n" unfolding factorization_lattice_def using deg_u by auto hence "fv ∈ carrier_vec n" unfolding fv by (metis lincomb_list_carrier) hence "degree f < n" unfolding f using degree_poly_of_vec_less[of fv n] using n by auto with dvd show "degree f < n ∧ poly_mod.dvdm M u f" by auto } qed end subsection ‹Soundness of the LLL factorization algorithm› lemma LLL_short_polynomial: assumes deg_u_0: "degree u ≠ 0" and deg_le: "degree u ≤ n" and pl1: "pl > 1" and monic: "monic u" shows "degree (LLL_short_polynomial pl n u) < n" and "LLL_short_polynomial pl n u ≠ 0" and "poly_mod.dvdm pl u (LLL_short_polynomial pl n u)" and "degree u < n ⟹ f ≠ 0 ⟹ poly_mod.dvdm pl u f ⟹ degree f < n ⟹ ∥LLL_short_polynomial pl n u∥⇧^{2}≤ 2 ^ (n - 1) * ∥f∥⇧^{2}" proof - interpret poly_mod_2 pl by (unfold_locales, insert pl1, auto) from pl1 have pl0: "pl ≠ 0" by auto let ?d = "degree u" let ?u = "Mp u" let ?iu = "inv_Mp ?u" from Mp_inv_Mp_id[of ?u] have "?iu =m ?u" . also have "… =m u" by simp finally have iu_u: "?iu =m u" by simp have degu[simp]: "degree ?u = degree u" using monic by simp have mon: "monic ?u" using monic by (rule monic_Mp) have "degree ?iu = degree ?u" unfolding inv_Mp_def by (rule degree_map_poly, unfold mon, insert mon pl1, auto simp: inv_M_def) with degu have deg_iu: "degree ?iu = degree u" by simp have mon_iu: "monic ?iu" unfolding deg_iu unfolding inv_Mp_def Mp_def inv_M_def M_def by (insert pl1, auto simp: coeff_map_poly monic) let ?L = "factorization_lattice ?iu (n - ?d) pl" let ?sv = "short_vector_hybrid 2 ?L" from deg_u_0 deg_le have n: "n ≠ 0" by auto from deg_u_0 have u0: "u ≠ 0" by auto have id: "LLL_short_polynomial pl n u = poly_of_vec ?sv" unfolding LLL_short_polynomial_def by blast have id': "∥?sv∥⇧^{2}= ∥LLL_short_polynomial pl n u∥⇧^{2}" unfolding id by simp interpret vec_module "TYPE(int)" n. interpret L: LLL n n "?L" 2 . from deg_le deg_iu have deg_iu_le: "degree ?iu ≤ n" by simp have len: "length ?L = n" unfolding factorization_lattice_def using deg_le deg_iu by auto from deg_u_0 deg_iu have deg_iu0: "degree ?iu ≠ 0" by auto hence iu0: "?iu ≠ 0" by auto from L.lin_indpt_list_factorization_lattice[OF refl deg_iu_le iu0 pl0] have *: "4/3 ≤ (2 :: rat)" "L.gs.lin_indpt_list (L.RAT ?L)" by (auto simp: deg_iu) interpret L: LLL_with_assms n n ?L 2 by (unfold_locales, insert *, auto simp: deg_iu deg_le) note short = L.short_vector_hybrid[OF refl n, unfolded id' L.L_def] from short(2) have mem: "LLL_short_polynomial pl n u ∈ poly_of_vec ` lattice_of ?L" unfolding id by auto note fact = L.factorization_lattice(1)[OF deg_iu0 pl0 deg_iu_le n, unfolded deg_iu, OF mem] show "degree (LLL_short_polynomial pl n u) < n" using fact by auto from fact have "?iu dvdm (LLL_short_polynomial pl n u)" by auto then obtain h where "LLL_short_polynomial pl n u =m ?iu * h" unfolding dvdm_def by auto also have "?iu * h =m Mp ?iu * h" unfolding mult_Mp by simp also have "Mp ?iu * h =m u * h" unfolding iu_u unfolding mult_Mp by simp finally show "u dvdm (LLL_short_polynomial pl n u)" unfolding dvdm_def by auto from short have sv1: "?sv ∈ carrier_vec n" by auto from short have "?sv ≠ 0⇩_{v}j" for j by auto thus "LLL_short_polynomial pl n u ≠ 0" unfolding id by simp assume degu: "degree u < n" and dvd: "u dvdm f" and degf: "degree f < n" and f0: "f ≠ 0" from dvd obtain h where "f =m u * h" unfolding dvdm_def by auto also have "u * h =m Mp u * h" unfolding mult_Mp by simp also have "Mp u * h =m Mp ?iu * h" unfolding iu_u by simp also have "Mp ?iu * h =m ?iu * h" unfolding mult_Mp by simp finally have dvd: "?iu dvdm f" unfolding dvdm_def by auto from degu deg_iu have deg_iun: "degree ?iu < n" by auto from L.factorization_lattice(2)[OF deg_iu0 pl0 mon_iu deg_iun degf dvd] have "f ∈ poly_of_vec ` lattice_of ?L" using deg_iu by auto then obtain fv where f: "f = poly_of_vec fv" and fv: "fv ∈ lattice_of ?L" by auto have norm: "∥fv∥⇧^{2}= ∥f∥⇧^{2}" unfolding f by simp have fv0: "fv ≠ 0⇩_{v}n" using f0 unfolding f by auto with fv have fvL: "fv ∈ lattice_of ?L - {0⇩_{v}n}" by auto from short(3)[OF this, unfolded norm] have "rat_of_int ∥LLL_short_polynomial pl n u∥⇧^{2}≤ rat_of_int (2 ^ (n - 1) * ∥f∥⇧^{2})" by simp thus "∥LLL_short_polynomial pl n u∥⇧^{2}≤ 2 ^ (n - 1) * ∥f∥⇧^{2}" by linarith qed context LLL_implementation begin lemma LLL_reconstruction: assumes "LLL_reconstruction f us = fs" and "degree f ≠ 0" and "poly_mod.unique_factorization_m pl f (lead_coeff f, mset us)" and "f dvd F" and "⋀ ui. ui ∈ set us ⟹ poly_mod.Mp pl ui = ui" and F0: "F ≠ 0" and cop: "coprime (lead_coeff F) p" and sf: "poly_mod.square_free_m p F" and pl1: "pl > 1" and plp: "pl = p^l" and p: "prime p" and large: "2^(5 * (degree F - 1) * (degree F - 1)) * ∥F∥⇧^{2}^(2 * (degree F - 1)) < pl⇧^{2}" shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩_{d}fi)" proof - interpret p: poly_mod_prime p by (standard, rule p) interpret pl: poly_mod_2 "pl" by (standard, rule pl1) from pl1 plp have l0: "l ≠ 0" by (cases l, auto) show ?thesis using assms(1-5) proof (induct f us arbitrary: fs rule: LLL_reconstruction.induct) case (1 f us fs) define u where "u = choose_u us" define g where "g = LLL_short_polynomial pl (degree f) u" define k where "k = gcd f g" note res = 1(3) note degf = 1(4) note uf = 1(5) note fF = 1(6) note norm = 1(7) note to_fact = pl.unique_factorization_m_imp_factorization note fact = to_fact[OF uf] have mon_gs: "ui ∈ set us ⟹ monic ui" for ui using norm fact unfolding pl.factorization_m_def by auto from p.coprime_lead_coeff_factor[OF p.prime] fF cop have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast have plf0: "pl.Mp f ≠ 0" using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce have "degree f = pl.degree_m f" by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop p, simp add: l0 p.coprime_exp_mod plp) also have "… = sum_mset (image_mset pl.degree_m (mset us))" unfolding pl.factorization_m_degree[OF fact plf0] .. also have "… = sum_list (map pl.degree_m us)" unfolding sum_mset_sum_list[symmetric] by auto also have "… = sum_list (map degree us)" by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto) finally have degf_gs: "degree f = sum_list (map degree us)" by auto hence gs: "us ≠ []" using degf by (cases us, auto) from choose_u_member[OF gs] have u_gs: "u ∈ set us" unfolding u_def by auto from fact u_gs have irred: "pl.irreducible⇩_{d}_m u" unfolding pl.factorization_m_def by auto hence deg_u: "degree u ≠ 0" unfolding pl.irreducible⇩_{d}_m_def norm[OF u_gs] by auto have deg_uf: "degree u ≤ degree f" unfolding degf_gs using split_list[OF u_gs] by auto from mon_gs[OF u_gs] have mon_u: "monic u" and u0: "u ≠ 0" by auto have f0: "f ≠ 0" using degf by auto from norm have norm': "image_mset pl.Mp (mset us) = mset us" by (induct us, auto) have pl0: "pl ≠ 0" using pl1 by auto note short_main = LLL_short_polynomial[OF deg_u deg_uf pl1 mon_u] from short_main(1-2)[folded g_def] have "degree k < degree f" unfolding k_def by (smt Suc_leI Suc_less_eq degree_gcd1 gcd.commute le_imp_less_Suc le_trans) hence deg_fk: "(degree k = 0 ∨ degree f ≤ degree k) = (degree k = 0)" by auto note res = res[unfolded LLL_reconstruction.simps[of f us] Let_def, folded u_def, folded g_def, folded k_def, unfolded deg_fk] show ?case proof (cases "degree k = 0") case True with res have fs: "fs = [f]" by auto from sf fF have sf: "p.square_free_m f" using p.square_free_m_factor(1)[of f] unfolding dvd_def by auto have irr: "irreducible⇩_{d}f" proof (rule ccontr) assume "¬ irreducible⇩_{d}f" from reducible⇩_{d}E[OF this] degf obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" by (simp, metis) from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp] obtain us1 us2 where uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" "pl.unique_factorization_m f2 (lead_coeff f2, us2)" and gs: "mset us = us1 + us2" and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1" unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def) note norm_u = norm[OF u_gs] from u_gs have u_gs': "u ∈# mset us" by auto with pl.factorization_m_mem_dvdm[OF fact, of u] have u_f: "pl.dvdm u f" by auto from u_gs'[unfolded gs] have "u ∈# us1 ∨ u ∈# us2" by auto with pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(1)], of u] pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(2)], of u] have "pl.dvdm u f1 ∨ pl.dvdm u f2" unfolding norm12 norm_u by auto from this have "∃ f1 f2. f = f1 * f2 ∧ degree f1 ≠ 0 ∧ degree f2 ≠ 0 ∧ degree f1 < degree f ∧ degree f2 < degree f ∧ pl.dvdm u f1" proof assume "pl.dvdm u f1" thus ?thesis using f deg12 by auto next from f have f: "f = f2 * f1" by auto assume "pl.dvdm u f2" thus ?thesis using f deg12 by auto qed then obtain f1 f2 where prod: "f = f1 * f2" and deg: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" and uf1: "pl.dvdm u f1" by auto from pl.unique_factorization_m_factor[OF p uf[unfolded prod], folded prod, OF cop sf l0 plp] obtain us1 where fact_f1: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" by auto have plf1: "pl.Mp f1 ≠ 0" using to_fact[OF fact_f1] pl.factorization_m_lead_coeff pl.unique_factorization_m_zero fact_f1 by fastforce have "degree u ≤ degree f1" by (rule pl.dvdm_degree[OF mon_u uf1 plf1]) with deg have deg_uf: "degree u < degree f" by auto have pl0: "pl ≠ 0" using pl.m1 plp by linarith let ?n = "degree f" let ?n1 = "degree f1" let ?d = "degree u" from prod fF have f1F: "f1 dvd F" unfolding dvd_def by auto from deg_uf have deg_uf': "?d ≤ ?n" by auto from deg have f1_0: "f1 ≠ 0" by auto have ug: "pl.dvdm u g" using short_main(3) unfolding g_def . have g0: "g ≠ 0" using short_main(2) unfolding g_def . have deg_gf: "degree g < degree f" using short_main(1) unfolding g_def . let ?N = "degree F" from fF prod have f1F: "f1 dvd F" unfolding dvd_def by auto have "∥g∥⇧^{2}≤ 2 ^ (?n - 1) * ∥f1∥⇧^{2}" unfolding g_def by (rule short_main(4)[OF deg_uf _ uf1], insert deg, auto) also have "… ≤ 2 ^ (?n - 1) * (2 ^ (2 * degree f1) * ∥F∥⇧^{2})" by (rule mult_left_mono[OF sq_norm_factor_bound[OF f1F F0]], simp) also have "… = 2 ^ ((?n - 1) + 2 * degree f1) * ∥F∥⇧^{2}" unfolding power_add by simp also have "… ≤ 2 ^ ((?n - 1) + 2 * (?n - 1)) * ∥F∥⇧^{2}" by (rule mult_right_mono, insert deg(3), auto) also have "… = 2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2}" by simp finally have ineq_g: "∥g∥⇧^{2}≤ 2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2}" . from power_mono[OF this, of ?n1] have ineq1: "∥g∥⇧^{2}^ ?n1 ≤ (2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2})^?n1" by auto from F0 have normF: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] by presburger from g0 have normg: "∥g∥⇧^{2}≥ 1" using sq_norm_poly_pos[of g] by presburger from f0 have normf: "∥f∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f] by presburger from f1_0 have normf1: "∥f1∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f1] by presburger from power_mono[OF sq_norm_factor_bound[OF f1F F0], of "degree g"] have ineq2: "∥f1∥⇧^{2}^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ degree g" by auto also have "… ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1)" by (rule pow_mono_exp, insert deg_gf normF, auto) finally have ineq2: "∥f1∥⇧^{2}^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1)" . have nN: "?n ≤ ?N" using fF F0 by (metis dvd_imp_degree_le) from deg nN have n1N: "?n1 ≤ ?N - 1" by auto have "∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ ?n1 ≤ (2 ^ (2 * ?n1) * ∥F∥⇧^{2}) ^ (?n - 1) * (2 ^ (3 * (?n - 1)) * ∥F∥⇧^{2})^?n1" by (rule mult_mono[OF ineq2 ineq1], force+) also have "… ≤ (2 ^ (2 * (?N - 1)) * ∥F∥⇧^{2}) ^ (?N - 1) * (2 ^ (3 * (?N - 1)) * ∥F∥⇧^{2}) ^ (?N - 1)" by (rule mult_mono[OF power_both_mono[OF _ _ mult_mono] power_both_mono], insert normF n1N nN, auto intro: power_both_mono mult_mono) also have "… = 2 ^ (2 * (?N -1) * (?N - 1) + 3 * (?N - 1) * (?N - 1)) * (∥F∥⇧^{2})^((?N - 1) + (?N - 1))" unfolding power_mult_distrib power_add power_mult by simp also have "2 * (?N - 1) * (?N - 1) + 3 * (?N - 1) * (?N - 1) = 5 * (?N - 1) * (?N - 1)" by simp also have "?N - 1 + (?N - 1) = 2 * (?N - 1)" by simp also have "2^(5 * (?N - 1) * (?N - 1)) * ∥F∥⇧^{2}^(2 * (?N - 1)) < pl^2" by (rule large) finally have large: "∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree f1 < pl⇧^{2}" . have deg_ug: "degree u ≤ degree g" proof (rule pl.dvdm_degree[OF mon_u ug], standard) assume "pl.Mp g = 0" from arg_cong[OF this, of "λ p. coeff p (degree g)"] have "pl.M (coeff g (degree g)) = 0" by (auto simp: pl.Mp_def coeff_map_poly) from this[unfolded pl.M_def] obtain c where lg: "lead_coeff g = pl * c" by auto with g0 have c0: "c ≠ 0" by auto hence "pl^2 ≤ (lead_coeff g)^2" unfolding lg abs_le_square_iff[symmetric] by (rule aux_abs_int) also have "… ≤ ∥g∥⇧^{2}^ 1" using coeff_le_sq_norm[of g] by auto also have "… ≤ ∥g∥⇧^{2}^ degree f1" by (rule pow_mono_exp, insert deg normg, auto) also have "… = 1 * …" by simp also have "… ≤ ∥f1∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree f1" by (rule mult_right_mono, insert normf1, auto) also have "… < pl⇧^{2}" by (rule large) finally show False by auto qed from deg deg_u deg_ug have "degree f1 > 0" "degree g > 0" by auto from common_factor_via_short[OF this mon_u _ uf1 ug large] deg_u pl.m1 have "0 < degree (gcd f1 g)" by auto moreover from True[unfolded k_def] have "degree (gcd f g) = 0" . moreover have dvd: "gcd f1 g dvd gcd f g" using f0 unfolding prod by simp ultimately show False using divides_degree[OF dvd] using f0 by simp qed show ?thesis unfolding fs using irr by auto next case False define f1 where "f1 = f div k" have f: "f = f1 * k" unfolding f1_def k_def by auto with arg_cong[OF this, of degree] f0 have deg_f1k: "degree f = degree f1 + degree k" by (auto simp: degree_mult_eq) from f fF have dvd: "f1 dvd F" "k dvd F" unfolding dvd_def by auto obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi f1) us = (gs1, gs2)" by force note IH = 1(1-2)[OF refl u_def g_def k_def refl, unfolded deg_fk, OF False f1_def part[symmetric] refl] obtain fs1 where fs1: "LLL_reconstruction f1 gs1 = fs1" by auto obtain fs2 where fs2: "LLL_reconstruction k gs2 = fs2" by auto from False res[folded f1_def, unfolded part split fs1 fs2] have fs: "fs = fs1 @ fs2" by auto from short_main(1) have deg_gf: "degree g < degree f" unfolding g_def by auto from short_main(2) have g0: "g ≠ 0" unfolding g_def by auto have deg_kg: "degree k ≤ degree g" unfolding k_def gcd.commute[of f g] by (rule degree_gcd1[OF g0]) from deg_gf deg_kg have deg_kf: "degree k < degree f" by auto with deg_f1k have deg_f1: "degree f1 ≠ 0" by auto have sf_f: "p.square_free_m f" using sf fF p.square_free_m_factor unfolding dvd_def by blast from p.unique_factorization_m_factor_partition[OF l0 uf[unfolded plp] f cop sf_f part] have uf: "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)" "pl.unique_factorization_m k (lead_coeff k, mset gs2)" by (auto simp: plp) have "set us = set gs1 ∪ set gs2" using part by auto with norm have norm_12: "gi ∈ set gs1 ∨ gi ∈ set gs2 ⟹ pl.Mp gi = gi" for gi by auto note IH1 = IH(1)[OF fs1 deg_f1 uf(1) dvd(1) norm_12] note IH2 = IH(2)[OF fs2 False uf(2) dvd(2) norm_12] show ?thesis unfolding fs f using IH1 IH2 by auto qed qed qed lemma LLL_many_reconstruction: assumes "LLL_many_reconstruction f us = fs" and "degree f ≠ 0" and "poly_mod.unique_factorization_m pl f (lead_coeff f, mset us)" and "f dvd F" and "⋀ ui. ui ∈ set us ⟹ poly_mod.Mp pl ui = ui" and F0: "F ≠ 0" and cop: "coprime (lead_coeff F) p" and sf: "poly_mod.square_free_m p F" and pl1: "pl > 1" and plp: "pl = p^l" and p: "prime p" and large: "2^(5 * (degree F div 2) * (degree F div 2)) * ∥F∥⇧^{2}^(2 * (degree F div 2)) < pl⇧^{2}" shows "f = prod_list fs ∧ (∀ fi ∈ set fs. irreducible⇩_{d}fi)" proof - interpret p: poly_mod_prime p by (standard, rule p) interpret pl: poly_mod_2 "pl" by (standard, rule pl1) from pl1 plp have l0: "l ≠ 0" by (cases l, auto) show ?thesis using assms(1-5) proof (induct f us arbitrary: fs rule: LLL_many_reconstruction.induct) case (1 f us fs) note res = 1(3) note degf = 1(4) note uf = 1(5) note fF = 1(6) note norm = 1(7) note to_fact = pl.unique_factorization_m_imp_factorization note fact = to_fact[OF uf] have mon_gs: "ui ∈ set us ⟹ monic ui" for ui using norm fact unfolding pl.factorization_m_def by auto from p.coprime_lead_coeff_factor[OF p.prime] fF cop have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast have plf0: "pl.Mp f ≠ 0" using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce have "degree f = pl.degree_m f" by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop p, simp add: l0 p.coprime_exp_mod plp) also have "… = sum_mset (image_mset pl.degree_m (mset us))" unfolding pl.factorization_m_degree[OF fact plf0] .. also have "… = sum_list (map pl.degree_m us)" unfolding sum_mset_sum_list[symmetric] by auto also have "… = sum_list (map degree us)" by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto) finally have degf_gs: "degree f = sum_list (map degree us)" by auto hence gs: "us ≠ []" using degf by (cases us, auto) from 1(4) have f0: "f ≠ 0" and df0: "degree f ≠ 0" by auto from norm have norm': "image_mset pl.Mp (mset us) = mset us" by (induct us, auto) have pl0: "pl ≠ 0" using pl1 by auto let ?D2 = "degree F div 2" let ?d2 = "degree f div 2" define gg where "gg = LLL_short_polynomial pl (Suc ?d2)" let ?us = "filter (λu. degree u ≤ ?d2) us" note res = res[unfolded LLL_many_reconstruction.simps[of f us], unfolded Let_def, folded gg_def] let ?f2_opt = "find_map_filter (λu. gcd f (gg u)) (λf2. 0 < degree f2 ∧ degree f2 < degree f) ?us" show ?case proof (cases ?f2_opt) case (Some f2) from find_map_filter_Some[OF this] obtain g where deg_f2: "degree f2 ≠ 0" "degree f2 < degree f" and dvd: "f2 dvd f" and gcd: "f2 = gcd f g" by auto note res = res[unfolded Some option.simps] define f1 where "f1 = f div f2" have f: "f = f1 * f2" unfolding f1_def using dvd by auto with arg_cong[OF this, of degree] f0 have deg_sum: "degree f = degree f1 + degree f2" by (auto simp: degree_mult_eq) with deg_f2 have deg_f1: "degree f1 ≠ 0" "degree f1 < degree f" by auto from f fF have dvd: "f1 dvd F" "f2 dvd F" unfolding dvd_def by auto obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi f1) us = (gs1, gs2)" by force note IH = 1(1-2)[OF refl refl refl, unfolded Let_def, folded gg_def, OF Some f1_def part[symmetric] refl] obtain fs1 where fs1: "LLL_many_reconstruction f1 gs1 = fs1" by blast obtain fs2 where fs2: "LLL_many_reconstruction f2 gs2 = fs2" by blast from res[folded f1_def, unfolded part split fs1 fs2] have fs: "fs = fs1 @ fs2" by auto have sf_f: "p.square_free_m f" using sf fF p.square_free_m_factor unfolding dvd_def by blast from p.unique_factorization_m_factor_partition[OF l0 uf[unfolded plp] f cop sf_f part] have uf: "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)" "pl.unique_factorization_m f2 (lead_coeff f2, mset gs2)" by (auto simp: plp) have "set us = set gs1 ∪ set gs2" using part by auto with norm have norm_12: "gi ∈ set gs1 ∨ gi ∈ set gs2 ⟹ pl.Mp gi = gi" for gi by auto note IH1 = IH(1)[OF fs1 deg_f1(1) uf(1) dvd(1) norm_12] note IH2 = IH(2)[OF fs2 deg_f2(1) uf(2) dvd(2) norm_12] show ?thesis unfolding fs f using IH1 IH2 by auto next case None from res[unfolded None option.simps] have fs_f: "fs = [f]" by simp from sf fF have sf: "p.square_free_m f" using p.square_free_m_factor(1)[of f] unfolding dvd_def by auto have "irreducible⇩_{d}f" proof (rule ccontr) assume "¬ irreducible⇩_{d}f" from reducible⇩_{d}E[OF this] degf obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 < degree f" "degree f2 < degree f" by (simp, metis) from f0 have "degree f = degree f1 + degree f2" unfolding f by (auto simp: degree_mult_eq) hence "degree f1 ≤ degree f div 2 ∨ degree f2 ≤ degree f div 2" by auto then obtain f1 f2 where f: "f = f1 * f2" and deg12: "degree f1 ≠ 0" "degree f2 ≠ 0" "degree f1 ≤ degree f div 2" "degree f2 < degree f" proof (standard, goal_cases) case 1 from 1(1)[of f1 f2] 1(2) f deg12 show ?thesis by auto next case 2 from 2(1)[of f2 f1] 2(2) f deg12 show ?thesis by auto qed from f0 f have f10: "f1 ≠ 0" by auto from sf f have sf1: "p.square_free_m f1" using p.square_free_m_factor(1)[of f1] by auto from p.coprime_lead_coeff_factor[OF p.prime cop[unfolded f]] have cop1: "coprime (lead_coeff f1) p" by auto have deg_m1: "pl.degree_m f1 = degree f1" by (rule poly_mod.degree_m_eq[OF _ pl.m1], insert cop1 p, simp add: l0 p.coprime_exp_mod plp) from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp] obtain us1 us2 where uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" "pl.unique_factorization_m f2 (lead_coeff f2, us2)" and gs: "mset us = us1 + us2" and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1" unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def) from gs have "x ∈# us1 ⟹ x ∈# mset us" for x by auto hence sub1: "x ∈# us1 ⟹ x ∈ set us" for x by auto from to_fact[OF uf12(1)] have fact1: "pl.factorization_m f1 (lead_coeff f1, us1)" . have plf10: "pl.Mp f1 ≠ 0" using fact1 pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf12(1) by fastforce have "degree f1 = pl.degree_m f1" using deg_m1 by simp also have "… = sum_mset (image_mset pl.degree_m us1)" unfolding pl.factorization_m_degree[OF fact1 plf10] .. also have "… = sum_mset (image_mset degree us1)" by (rule arg_cong[of _ _ sum_mset], rule image_mset_cong, rule pl.monic_degree_m, rule mon_gs, rule sub1) finally have degf1_sum: "degree f1 = sum_mset (image_mset degree us1)" by auto with deg12 have "us1 ≠ {#}" by auto then obtain u us11 where us1: "us1 = {#u#} + us11" by (cases us1, auto) hence u1: "u ∈# us1" by auto hence u: "u ∈ set us" by (rule sub1) let ?g = "gg u" from pl.factorization_m_mem_dvdm[OF fact1, of u] u1 have u_f1: "pl.dvdm u f1" by auto note norm_u = norm[OF u] from fact u have irred: "pl.irreducible⇩_{d}_m u" unfolding pl.factorization_m_def by auto hence deg_u: "degree u ≠ 0" unfolding pl.irreducible⇩_{d}_m_def norm[OF u] by auto have "degree u ≤ degree f1" unfolding degf1_sum unfolding us1 by simp also have "… ≤ degree f div 2" by fact finally have deg_uf: "degree u ≤ degree f div 2" . hence deg_uf': "degree u ≤ Suc (degree f div 2)" "degree u < Suc (degree f div 2)" by auto from mon_gs[OF u] have mon_u: "monic u" . note short = LLL_short_polynomial[OF deg_u deg_uf'(1) pl1 mon_u, folded gg_def] note short = short(1-3) short(4)[OF deg_uf'(2)] from short(1,2) deg12(1,3) f10 have "degree (gcd f ?g) ≤ degree f div 2" by (metis Suc_leI Suc_le_mono degree_gcd1 gcd.commute le_trans) also have "… < degree f" using degf by simp finally have "degree (gcd f ?g) < degree f" by simp with find_map_filter_None[OF None, simplified, rule_format, of u] deg_uf u have deg_gcd: "degree (gcd f (?g)) = 0" by (auto simp: gcd.commute) have "gcd f1 (?g) dvd gcd f (?g)" using f0 unfolding f by simp from divides_degree[OF this, unfolded deg_gcd] f0 have deg_gcd1: "degree (gcd f1 (?g)) = 0" by auto from F0 have normF: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] by presburger have g0: "?g ≠ 0" using short(2) . from g0 have normg: "∥?g∥⇧^{2}≥ 1" using sq_norm_poly_pos[of "?g"] by presburger from f10 have normf1: "∥f1∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f1] by presburger from fF f have f1F: "f1 dvd F" unfolding dvd_def by auto have pl_ge0: "pl ≥ 0" using pl.poly_mod_2_axioms poly_mod_2_def by auto from fF have "degree f ≤ degree F" using F0 f0 by (metis dvd_imp_degree_le) hence d2D2: "?d2 ≤ ?D2" by simp with deg12(3) have df1_D2: "degree f1 ≤ ?D2" by linarith from short(1) d2D2 have dg_D2: "degree (gg u) ≤ ?D2" by linarith have "∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1 ≤ ∥f1∥⇧^{2}^ ?D2 * ∥gg u∥⇧^{2}^ ?D2" by (rule mult_mono[OF pow_mono_exp pow_mono_exp], insert normf1 normg, auto intro: df1_D2 dg_D2) also have "… = (∥f1∥⇧^{2}* ∥gg u∥⇧^{2})^?D2" by (simp add: power_mult_distrib) also have "… ≤ (∥f1∥⇧^{2}* (2^?D2 * ∥f1∥⇧^{2}))^?D2" by (rule power_mono[OF mult_left_mono[OF order.trans[OF short(4)[OF f10 u_f1]]]], insert deg12 d2D2, auto intro!: mult_mono) also have "… = ∥f1∥⇧^{2}^ (?D2 + ?D2) * 2^(?D2 * ?D2)" unfolding power_add power_mult_distrib power_mult by simp also have "… ≤ (2 ^ (2 * ?D2) * ∥F∥⇧^{2}) ^ (?D2 + ?D2) * 2^(?D2 * ?D2)" by (rule mult_right_mono[OF order.trans[OF power_mono[OF sq_norm_factor_bound[OF f1F F0]]]], auto intro!: power_mono mult_right_mono df1_D2) also have "… = 2 ^ (2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2) * ∥F∥⇧^{2}^ (?D2 + ?D2)" unfolding power_mult_distrib power_mult power_add by simp also have "2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2 = 5 * ?D2 * ?D2" by simp also have "?D2 + ?D2 = 2 * ?D2" by simp finally have large: "∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1 < pl^2" using large by simp have "degree u ≤ degree (?g)" proof (rule pl.dvdm_degree[OF mon_u short(3)], standard) assume "pl.Mp (?g) = 0" from arg_cong[OF this, of "λ p. coeff p (degree ?g)"] have "pl.M (coeff ?g (degree ?g)) = 0" by (auto simp: pl.Mp_def coeff_map_poly) from this[unfolded pl.M_def] obtain c where lg: "lead_coeff ?g = pl * c" by auto with g0 have c0: "c ≠ 0" by auto hence "pl^2 ≤ (lead_coeff ?g)^2" unfolding lg abs_le_square_iff[symmetric] by (rule aux_abs_int) also have "… ≤ ∥?g∥⇧^{2}" using coeff_le_sq_norm[of ?g] by auto also have "… = ∥?g∥⇧^{2}^ 1" by simp also have "… ≤ ∥?g∥⇧^{2}^ degree f1" by (rule pow_mono_exp, insert deg12 normg, auto) also have "… = 1 * …" by simp also have "… ≤ ∥f1∥⇧^{2}^ degree ?g * ∥?g∥⇧^{2}^ degree f1" by (rule mult_right_mono, insert normf1, auto) also have "… < pl⇧^{2}" by (rule large) finally show False by auto qed with deg_u have deg_g: "0 < degree (gg u)" by auto have pl_ge0: "pl ≥ 0" using pl.poly_mod_2_axioms poly_mod_2_def by auto from fF have "degree f ≤ degree F" using F0 f0 by (metis dvd_imp_degree_le) hence d2D2: "?d2 ≤ ?D2" by simp with deg12(3) have df1_D2: "degree f1 ≤ ?D2" by linarith from short(1) d2D2 have dg_D2: "degree (gg u) ≤ ?D2" by linarith have "0 < degree f1" "0 < degree u" using deg12 deg_u by auto from common_factor_via_short[of f1 "gg u", OF this(1) deg_g mon_u this(2) u_f1 short(3) _ pl_ge0] deg_gcd1 have "pl^2 ≤ ∥f1∥⇧^{2}^ degree (gg u) * ∥gg u∥⇧^{2}^ degree f1" by linarith also have "… < pl^2" by (rule large) finally show False by simp qed thus ?thesis using fs_f by simp qed qed qed end lemma LLL_factorization: assumes res: "LLL_factorization f = gs" and sff: "square_free f" and deg: "degree f ≠ 0" shows "f = prod_list gs ∧ (∀g∈set gs. irreducible⇩_{d}g)" proof - let ?lc = "lead_coeff f" define p where "p ≡ suitable_prime_bz f" obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force let ?degs = "map degree gs" note res = res[unfolded LLL_factorization_def Let_def, folded p_def, unfolded fff split, folded] from suitable_prime_bz[OF sff refl] have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" unfolding p_def by auto note res from prime interpret p: poly_mod_prime p by unfold_locales define K where "K = 2^(5 * (degree f - 1) * (degree f - 1)) * ∥f∥⇧^{2}^(2 * (degree f - 1))" define N where "N = sqrt_int_ceiling K" have K0: "K ≥ 0" unfolding K_def by fastforce have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling) define n where "n = find_exponent p N" note res = res[folded n_def[unfolded N_def K_def]] note n = find_exponent[OF p.m1, of N, folded n_def] note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)] from deg have f0: "f ≠ 0" by auto from n p.m1 have pn1: "p ^ n > 1" by auto note res = res[folded bh(1)] note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff] from res * ** have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" unfolding berlekamp_hensel_def fff split by auto have K: "K < (p ^ n)⇧^{2}" using n sqrt_int_ceiling_bound[OF K0] by (smt N0 N_def n(1) power2_le_imp_le) show ?thesis by (rule LLL_implementation.LLL_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 refl prime K[unfolded K_def]]) qed lemma LLL_many_factorization: assumes res: "LLL_many_factorization f = gs" and sff: "square_free f" and deg: "degree f ≠ 0" shows "f = prod_list gs ∧ (∀g∈set gs. irreducible⇩_{d}g)" proof - let ?lc = "lead_coeff f" define p where "p ≡ suitable_prime_bz f" obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force let ?degs = "map degree gs" note res = res[unfolded LLL_many_factorization_def Let_def, folded p_def, unfolded fff split, folded] from suitable_prime_bz[OF sff refl] have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" unfolding p_def by auto note res from prime interpret p: poly_mod_prime p by unfold_locales define K where "K = 2^(5 * (degree f div 2) * (degree f div 2)) * ∥f∥⇧^{2}^(2 * (degree f div 2))" define N where "N = sqrt_int_ceiling K" have K0: "K ≥ 0" unfolding K_def by fastforce have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling) define n where "n = find_exponent p N" note res = res[folded n_def[unfolded N_def K_def]] note n = find_exponent[OF p.m1, of N, folded n_def] note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)] from deg have f0: "f ≠ 0" by auto from n p.m1 have pn1: "p ^ n > 1" by auto note res = res[folded bh(1)] note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff] from res * ** have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" unfolding berlekamp_hensel_def fff split by auto have K: "K < (p ^ n)⇧^{2}" using n sqrt_int_ceiling_bound[OF K0] by (smt N0 N_def n(1) power2_le_imp_le) show ?thesis by (rule LLL_implementation.LLL_many_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 refl prime K[unfolded K_def]]) qed lift_definition one_lattice_LLL_factorization :: int_poly_factorization_algorithm is LLL_factorization using LLL_factorization by auto lift_definition many_lattice_LLL_factorization :: int_poly_factorization_algorithm is LLL_many_factorization using LLL_many_factorization by auto lemma LLL_factorization_primitive: assumes "LLL_factorization f = fs" "square_free f" "0 < degree f" "primitive f" shows "f = prod_list fs ∧ (∀fi∈set fs. irreducible fi ∧ 0 < degree fi ∧ primitive fi)" using assms(1) by (intro int_poly_factorization_algorithm_irreducible[of one_lattice_LLL_factorization, OF _ assms(2-)], transfer, auto) thm factorize_int_poly[of one_lattice_LLL_factorization] thm factorize_int_poly[of many_lattice_LLL_factorization] end

# Theory Sub_Sums

(* Author: René Thiemann License: BSD *) section ‹Calculating All Possible Sums of Sub-Multisets› theory Sub_Sums imports Main "HOL-Library.Multiset" begin fun sub_mset_sums :: "'a :: comm_monoid_add list ⇒ 'a set" where "sub_mset_sums [] = {0}" | "sub_mset_sums (x # xs) = (let S = sub_mset_sums xs in S ∪ ( (+) x) ` S)" lemma subset_add_mset: "ys ⊆# add_mset x zs ⟷ (ys ⊆# zs ∨ (∃ xs. xs ⊆# zs ∧ ys = add_mset x xs))" (is "?l = ?r") proof have sub: "ys ⊆# zs ⟹ ys ⊆# add_mset x zs" by (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans) assume ?r thus ?l using sub by auto next assume l: ?l show ?r proof (cases "x ∈# ys") case True define xs where "xs = (ys - {# x #})" from True have ys: "ys = add_mset x xs" unfolding xs_def by auto from l[unfolded ys] have "xs ⊆# zs" by auto thus ?r unfolding ys by auto next case False with l have "ys ⊆# zs" by (simp add: subset_mset.le_iff_sup) thus ?thesis by auto qed qed lemma sub_mset_sums[simp]: "sub_mset_sums xs = sum_mset ` { ys. ys ⊆# mset xs }" proof (induct xs) case (Cons x xs) have id: "{ys. ys ⊆# mset (x # xs)} = {ys. ys ⊆# mset xs} ∪ {add_mset x ys | ys. ys ⊆# mset xs}" unfolding mset.simps subset_add_mset by auto show ?case unfolding sub_mset_sums.simps Let_def Cons id image_Un by force qed auto end

# Theory Factorization_Algorithm_16_22

(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada License: BSD *) section ‹Implementation and soundness of a modified version of Algorithm 16.22› text ‹Algorithm 16.22 is quite similar to the LLL factorization algorithm that was verified in the previous section. Its main difference is that it has an inner loop where each inner loop iteration has one invocation of the LLL basis reduction algorithm. Algorithm 16.22 of the textbook is therefore closer to the factorization algorithm as it is described by Lenstra, Lenstra, and Lov{\'a}sz \cite{LLL}, which also uses an inner loop. The advantage of the inner loop is that it can find factors earlier, and then small lattices suffice where without the inner loop one invokes the basis reduction algorithm on a large lattice. The disadvantage of the inner loop is that if the input is irreducible, then one cannot find any factor early, so that all but the last iteration have been useless: only the last iteration will prove irreducibility.› text ‹We will describe the modifications w.r.t.\ the original Algorithm 16.22 of the textbook later in this theory.› theory Factorization_Algorithm_16_22 imports LLL_Factorization Sub_Sums begin subsection ‹Previous lemmas obtained using local type definitions› context poly_mod_prime_type begin lemma irreducible_m_dvdm_prod_list_connect: assumes irr: "irreducible_m a" and dvd: "a dvdm (prod_list xs)" shows "∃ b ∈ set xs. a dvdm b" proof - let ?A="(of_int_poly a)::'a mod_ring poly" let ?XS="(map of_int_poly xs)::'a mod_ring poly list" let ?XS1 = "(of_int_poly (prod_list xs))::'a mod_ring poly" have [transfer_rule]: "MP_Rel a ?A" by (simp add: MP_Rel_def Mp_f_representative) have [transfer_rule]: "MP_Rel (prod_list xs) ?XS1" by (simp add: MP_Rel_def Mp_f_representative) have [transfer_rule]: "list_all2 MP_Rel xs ?XS" by (simp add: MP_Rel_def Mp_f_representative list_all2_conv_all_nth) have A: "?A dvd ?XS1" using dvd by transfer have "∃ b ∈ set ?XS. ?A dvd b" by (rule irreducible_dvd_prod_list, insert irr, transfer, auto simp add: A) from this[untransferred] show ?thesis . qed end lemma (in poly_mod_prime) irreducible_m_dvdm_prod_list: assumes irr: "irreducible_m a" and dvd: "a dvdm (prod_list xs)" shows "∃ b ∈ set xs. a dvdm b" by (rule poly_mod_prime_type.irreducible_m_dvdm_prod_list_connect[unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty irr dvd]) subsection ‹The modified version of Algorithm 16.22› (* Implementation of the for loop of step 8. The loop will finishes in two cases: - If j>n' - If a divisor is found *) definition B2_LLL :: "int poly ⇒ int" where "B2_LLL f = 2 ^ (2 * degree f) * ∥f∥⇧^{2}" hide_const (open) factors hide_const (open) factors hide_const (open) factor hide_const (open) factor context fixes p :: int and l :: nat begin context fixes gs :: "int poly list" and f :: "int poly" and u :: "int poly" and Degs :: "nat set" begin text ‹This is the critical inner loop. In the textbook there is a bug, namely that the filter is applied to $g'$ and not to the primitive part of $g'$. (Problems occur if the content of $g'$ is divisible by $p$.) We have fixed this problem in the obvious way. However, there also is a second problem, namely it is only guaranteed that $g'$ is divisible by $u$ modulo $p^l$. However, for soundness we need to know that then also the primitive part of $g'$ is divisible by $u$ modulo $p^l$. This is not necessary true, e.g., if $g' = p^l$, then the primitive part is $1$ which is not divisible by $u$ modulo $p^l$. It is open, whether such a large $g'$ can actually occur. Therefore, the current fix is to manually test whether the leading coefficient of $g'$ is strictly smaller than $p^l$. With these two modifications, Algorithm 16.22 will become sound as proven below.› definition "LLL_reconstruction_inner j ≡ let j' = j - 1 in ― ‹optimization: check whether degree j' is possible› if j' ∉ Degs then None else ― ‹short vector computation› let ll = (let n = sqrt_int_ceiling (∥f∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j')); ll' = find_exponent p n in if ll' < l then ll' else l); ― ‹optimization: dynamically adjust the modulus› pl = p^ll; g' = LLL_short_polynomial pl j u ― ‹fix: forbid multiples of $p^l$ as short vector, unclear whether this is really required› in if abs (lead_coeff g') ≥ pl then None else let ppg = primitive_part g' in ― ‹slight deviation from textbook: we check divisibility instead of norm-inequality› case div_int_poly f ppg of Some f' ⇒ ― ‹fix: consider modular factors of ppg and not of g'› Some (filter (λgi. ¬ poly_mod.dvdm p gi ppg) gs, lead_coeff f', f', ppg) | None ⇒ None" function LLL_reconstruction_inner_loop where "LLL_reconstruction_inner_loop j = (if j > degree f then ([],1,1,f) else case LLL_reconstruction_inner j of Some tuple ⇒ tuple | None ⇒ LLL_reconstruction_inner_loop (j+1))" by auto termination by (relation "measure (λ j. Suc (degree f) - j)", auto) end (*The main loop (line 6)*) partial_function (tailrec) LLL_reconstruction'' where [code]: "LLL_reconstruction'' gs b f factors = (if gs = [] then factors else let u = choose_u gs; d = degree u; gs' = remove1 u gs; degs = map degree gs'; Degs = ((+) d) ` sub_mset_sums degs; (gs', b', f', factor) = LLL_reconstruction_inner_loop gs f u Degs (d+1) in LLL_reconstruction'' gs' b' f' (factor#factors) )" definition "reconstruction_of_algorithm_16_22 gs f ≡ let G = []; b = lead_coeff f in LLL_reconstruction'' gs b f G" end definition factorization_algorithm_16_22 :: "int poly ⇒ int poly list" where "factorization_algorithm_16_22 f = (let ― ‹find suitable prime› p = suitable_prime_bz f; ― ‹compute finite field factorization› (_, fs) = finite_field_factorization_int p f; ― ‹determine l and B› n = degree f; ― ‹bound improved according to textbook, which uses $no = (n + 1) * (max-norm f)^2$› no = ∥f∥⇧^{2}; ― ‹possible improvement: $B = sqrt (2 ^{5 * n * (n - 1)} * no ^ {2 * n - 1}$, cf. @{const LLL_factorization}› B = sqrt_int_ceiling (2 ^ (5 * n * n) * no ^ (2 * n)); l = find_exponent p B; ― ‹perform hensel lifting to lift factorization to mod $p^l$› vs = hensel_lifting p l f fs ― ‹reconstruct integer factors› in reconstruction_of_algorithm_16_22 p l vs f)" subsection ‹Soundness proof› subsubsection ‹Starting the proof› text ‹Key lemma to show that forbidding values of $p^l$ or larger suffices to find correct factors.› lemma (in poly_mod_prime) Mp_smult_p_removal: "poly_mod.Mp (p * p ^ k) (smult p f) = 0 ⟹ poly_mod.Mp (p^k) f = 0" by (smt add.left_neutral m1 poly_mod.Dp_Mp_eq poly_mod.Mp_smult_m_0 sdiv_poly_smult smult_smult) lemma (in poly_mod_prime) eq_m_smult_p_removal: "poly_mod.eq_m (p * p ^ k) (smult p f) (smult p g) ⟹ poly_mod.eq_m (p^k) f g" using Mp_smult_p_removal[of k "f - g"] by (metis add_diff_cancel_left' diff_add_cancel diff_self poly_mod.Mp_0 poly_mod.minus_Mp(2) smult_diff_right) lemma content_le_lead_coeff: "abs (content (f :: int poly)) ≤ abs (lead_coeff f)" proof (cases "f = 0") case False from content_dvd_coeff[of f "degree f"] have "abs (content f) dvd abs (lead_coeff f)" by auto moreover have "abs (lead_coeff f) ≠ 0" using False by auto ultimately show ?thesis by (smt dvd_imp_le_int) qed auto lemma poly_mod_dvd_drop_smult: assumes u: "monic u" and p: "prime p" and c: "c ≠ 0" "¦c¦ < p^l" and dvd: "poly_mod.dvdm (p^l) u (smult c f)" shows "poly_mod.dvdm p u f" using c dvd proof (induct l arbitrary: c rule: less_induct) case (less l c) interpret poly_mod_prime p by (unfold_locales, insert p, auto) note c = less(2-3) note dvd = less(4) note IH = less(1) show ?case proof (cases "l = 0") case True thus ?thesis using c dvd by auto next case l0: False interpret pl: poly_mod_2 "p^l" by (unfold_locales, insert m1 l0, auto) show ?thesis proof (cases "p dvd c") case False let ?i = "inverse_mod c (p ^ l)" have "gcd c p = 1" using p False by (metis Primes.prime_int_iff gcd_ge_0_int semiring_gcd_class.gcd_dvd1 semiring_gcd_class.gcd_dvd2) hence "coprime c p" by (metis dvd_refl gcd_dvd_1) from pl.inverse_mod_coprime_exp[OF refl p l0 this] have id: "pl.M (?i * c) = 1" . have "pl.Mp (smult ?i (smult c f)) = pl.Mp (smult (pl.M (?i * c)) f)" by simp also have "… = pl.Mp f" unfolding id by simp finally have "pl.dvdm u f" using pl.dvdm_smult[OF dvd, of ?i] unfolding pl.dvdm_def by simp thus "u dvdm f" using l0 pl_dvdm_imp_p_dvdm by blast next case True then obtain d where cpd: "c = p * d" unfolding dvd_def by auto from cpd c have d0: "d ≠ 0" by auto note to_p = Mp_Mp_pow_is_Mp[OF l0 m1] from dvd obtain v where eq: "pl.eq_m (u * v) (smult p (smult d f))" unfolding pl.dvdm_def cpd by auto from arg_cong[OF this, of Mp, unfolded to_p] have "Mp (u * v) = 0" unfolding Mp_smult_m_0 . with u have "Mp v = 0" by (metis Mp_0 add_eq_0_iff_both_eq_0 degree_0 degree_m_mult_eq monic_degree_0 monic_degree_m mult_cancel_right2) from Mp_0_smult_sdiv_poly[OF this] obtain w where v: "v = smult p w" by metis with eq have eq: "pl.eq_m (smult p (u * w)) (smult p (smult d f))" by simp from l0 obtain ll where "l = Suc ll" by (cases l, auto) hence pl: "p^l = p * p^ll" and ll: "ll < l" by auto from c(2) have d_small: "¦d¦ < p^ll" unfolding pl cpd abs_mult using mult_less_cancel_left_pos[of p d "p^ll"] m1 by auto from eq_m_smult_p_removal[OF eq[unfolded pl]] have "poly_mod.eq_m (p^ll) (u * w) (smult d f)" . hence dvd: "poly_mod.dvdm (p^ll) u (smult d f)" unfolding poly_mod.dvdm_def by metis show ?thesis by (rule IH[OF ll d0 d_small dvd]) qed qed qed context fixes p :: int and F :: "int poly" and N :: nat and l :: nat defines [simp]: "N ≡ degree F" assumes p: "prime p" and N0: "N > 0" and bound_l: "2 ^ N⇧^{2}* B2_LLL F ^ (2 * N) ≤ (p^l)⇧^{2}" begin private lemma F0: "F≠0" using N0 by fastforce private lemma p1: "p > 1" using p prime_gt_1_int by auto interpretation p: poly_mod_prime p using p by unfold_locales interpretation pl: poly_mod "p^l". lemma B2_2: "2 ≤ B2_LLL F" proof - from F0 have "∥F∥⇧^{2}≠ 0" by simp hence F1: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] F0 by linarith have "(2 :: int) = 2^1 * 1" by simp also have "… ≤ B2_LLL F" unfolding B2_LLL_def by (intro mult_mono power_increasing F1, insert N0, auto) finally show "2 ≤ B2_LLL F" . qed lemma l_gt_0: "l > 0" proof (cases l) case 0 have "1 * 2 ≤ 2 ^ N⇧^{2}* B2_LLL F ^ (2 * N)" proof (rule mult_mono) have "2 * 1 ≤ (2 :: int) * (2 ^ (2*N - 1))" by (rule mult_left_mono, auto) also have "… = 2 ^ (2 * N)" using N0 by (cases N, auto) also have "… ≤ B2_LLL F ^ (2 * N)" by (rule power_mono[OF B2_2], force) finally show "2 ≤ B2_LLL F ^ (2 * N)" by simp qed auto also have "… ≤ 1" using bound_l[unfolded 0] by auto finally show ?thesis by auto qed auto lemma l0: "l ≠ 0" using l_gt_0 by auto lemma pl_not0: "p ^ l ≠ 0" using p1 l0 by auto interpretation pl: poly_mod_2 "p^l" by (standard, insert p1 l0, auto) private lemmas pl_dvdm_imp_p_dvdm = p.pl_dvdm_imp_p_dvdm[OF l0] lemma p_Mp_pl_Mp[simp]: "p.Mp (pl.Mp k) = p.Mp k" using Mp_Mp_pow_is_Mp[OF l0 p.m1] . context fixes u :: "int poly" and d and f and n and gs :: "int poly list" and Degs :: "nat set" defines [simp]: "d ≡ degree u" assumes d0: "d > 0" and u: "monic u" and irred_u: "p.irreducible_m u" and u_f: "p.dvdm u f" and f_dvd_F: "f dvd F" and [simp]: "n == degree f" and f_gs: "pl.unique_factorization_m f (lead_coeff f, mset gs)" and cop: "coprime (lead_coeff f) p" and sf: "p.square_free_m f" and sf_F: "square_free f" and u_gs: "u ∈ set gs" and norm_gs: "map pl.Mp gs = gs" and Degs: "⋀ factor. factor dvd f ⟹ p.dvdm u factor ⟹ degree factor ∈ Degs" begin interpretation pl: poly_mod_2 "p^l" using l0 p1 by (unfold_locales, auto) private lemma f0: "f ≠ 0" using sf_F unfolding square_free_def by fastforce private lemma Mpf0: "pl.Mp f ≠ 0" by (metis p.square_free_m_def p_Mp_pl_Mp sf) private lemma pMpf0: "p.Mp f ≠ 0" using p.square_free_m_def sf by auto private lemma dn: "d ≤ n" using p.dvdm_imp_degree_le[OF u_f u pMpf0 p1] by auto private lemma n0: "n > 0" using d0 dn by auto private lemma B2_0[intro!]: "B2_LLL F > 0" using B2_2 by auto private lemma deg_u: "degree u > 0" using d0 d_def by auto private lemma n_le_N: "n≤N" by (simp add: dvd_imp_degree_le[OF f_dvd_F F0]) lemma dvdm_power: assumes "g dvd f" shows "p.dvdm u g ⟷ pl.dvdm u g" proof assume "pl.dvdm u g" thus "p.dvdm u g" by (rule pl_dvdm_imp_p_dvdm) next assume dvd: "p.dvdm u g" from norm_gs have norm_gsp: "⋀ f. f ∈ set gs ⟹ pl.Mp f = f" by (induct gs, auto) with f_gs[unfolded pl.unique_factorization_m_alt_def pl.factorization_m_def split] have gs_irred_mon: "⋀ f. f ∈# mset gs ⟹ pl.irreducible⇩_{d}_m f ∧ monic f" by auto from norm_gs have norm_gs: "image_mset pl.Mp (mset gs) = mset gs" by (induct gs, auto) from assms obtain h where f: "f = g * h" unfolding dvd_def by auto from pl.unique_factorization_m_factor[OF p.prime f_gs[unfolded f] _ _ l0 refl, folded f, OF cop sf, unfolded pl.Mf_def split] norm_gs obtain hs fs where uf: "pl.unique_factorization_m h (lead_coeff h, hs)" "pl.unique_factorization_m g (lead_coeff g, fs)" and id: "mset gs = fs + hs" and norm: "image_mset pl.Mp fs = fs" "image_mset pl.Mp hs = hs" by auto from p.square_free_m_prod_imp_coprime_m[OF sf[unfolded f]] have cop_h_f: "p.coprime_m g h" by auto show "pl.dvdm u g" proof (cases "u ∈# fs") case True hence "pl.Mp u ∈# image_mset pl.Mp fs" by auto from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf(2)] this] show ?thesis . next case False from u_gs have "u ∈# mset gs" by auto from this[unfolded id] False have "u ∈# hs" by auto hence "pl.Mp u ∈# image_mset pl.Mp hs" by auto from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf(1)] this] have "pl.dvdm u h" by auto from pl_dvdm_imp_p_dvdm[OF this] have "p.dvdm u h" by auto from cop_h_f[unfolded p.coprime_m_def, rule_format, OF dvd this] have "p.dvdm u 1" . from p.dvdm_imp_degree_le[OF this u _ p.m1] have "degree u = 0" by auto with deg_u show ?thesis by auto qed qed private lemma uf: "pl.dvdm u f" using dvdm_power[OF dvd_refl] u_f by simp lemma exists_reconstruction: "∃h0. irreducible⇩_{d}h0 ∧ p.dvdm u h0 ∧ h0 dvd f" proof - have deg_f: "degree f > 0" using ‹n ≡ degree f› n0 by blast from berlekamp_zassenhaus_factorization_irreducible⇩_{d}[OF refl sf_F deg_f] obtain fs where f_fs: "f = prod_list fs" and c: "(∀fi∈set fs. irreducible⇩_{d}fi ∧ 0 < degree fi )" by blast have "pl.dvdm u (prod_list fs)" using uf f_fs by simp hence "p.dvdm u (prod_list fs)" by (rule pl_dvdm_imp_p_dvdm) from this obtain h0 where h0: "h0 ∈ set fs" and dvdm_u_h0: "p.dvdm u h0" using p.irreducible_m_dvdm_prod_list[OF irred_u] by auto moreover have "h0 dvd f" by (unfold f_fs, rule prod_list_dvd[OF h0]) moreover have "irreducible⇩_{d}h0" using c h0 by auto ultimately show ?thesis by blast qed lemma factor_dvd_f_0: assumes "factor dvd f" shows "pl.Mp factor ≠ 0" proof - from assms obtain h where f: "f = factor * h" unfolding dvd_def .. from arg_cong[OF this, of pl.Mp] have "0 ≠ pl.Mp (pl.Mp factor * h)" using Mpf0 by auto thus ?thesis by fastforce qed lemma degree_factor_ge_degree_u: assumes u_dvdm_factor: "p.dvdm u factor" and factor_dvd: "factor dvd f" shows "degree u ≤ degree factor" proof - from factor_dvd_f_0[OF factor_dvd] have factor0: "pl.Mp factor ≠ 0" . from u_dvdm_factor[unfolded dvdm_power[OF factor_dvd] pl.dvdm_def] obtain v where *: "pl.Mp factor = pl.Mp (u * pl.Mp v)" by auto with factor0 have v0: "pl.Mp v ≠ 0" by fastforce hence "0 ≠ lead_coeff (pl.Mp v)" by auto also have "lead_coeff (pl.Mp v) = pl.M (lead_coeff (pl.Mp v))" by (auto simp: pl.Mp_def coeff_map_poly) finally have **: "lead_coeff (pl.Mp v) ≠ p ^ l * r" for r by (auto simp: pl.M_def) from * have "degree factor ≥ pl.degree_m (u * pl.Mp v)" using pl.degree_m_le[of factor] by auto also have "pl.degree_m (u * pl.Mp v) = degree (u * pl.Mp v)" by (rule pl.degree_m_eq, unfold lead_coeff_mult, insert u pl.m1 **, auto) also have "… = degree u + degree (pl.Mp v)" by (rule degree_mult_eq, insert v0 u, auto) finally show ?thesis by auto qed subsubsection ‹Inner loop› context fixes j' :: nat assumes dj': "d ≤ j'" and j'n: "j' < n" and deg: "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ degree factor ≥ j'" begin private abbreviation (input) "j ≡ Suc j'" private lemma jn: "j ≤ n" using j'n by auto private lemma factor_irreducible⇩_{d}I: assumes hf: "h dvd f" and puh: "p.dvdm u h" and degh: "degree h > 0" and degh_j: "degree h ≤ j'" shows "irreducible⇩_{d}h" proof - from dvdm_power[OF hf] puh have pluh: "pl.dvdm u h" by simp note uf_partition = p.unique_factorization_m_factor_partition[OF l0] obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi h) gs = (gs1, gs2)" by force from part u_gs puh have u_gs1: "u ∈ set gs1" unfolding p by auto have gs1: "gs1 = filter (λ gi. p.dvdm gi h) gs" using part by auto obtain k where f: "f = h * k" using hf unfolding dvd_def by auto from uf_partition[OF f_gs f cop sf part] have uf_h: "pl.unique_factorization_m h (lead_coeff h, mset gs1)" by auto show ?thesis proof (intro irreducible⇩_{d}I degh) fix q r assume deg_q: "degree q > 0" "degree q < degree h" and deg_r: "degree r > 0" "degree r < degree h" and h: "h = q * r" then have "r dvd h" by auto with h dvd_trans[OF _ hf] have 1: "q dvd f" "r dvd f" by auto from cop[unfolded f] have cop: "coprime (lead_coeff h) p" using p.prime pl.coprime_lead_coeff_factor(1) by blast from sf[unfolded f] have sf: "p.square_free_m h" using p.square_free_m_factor by metis have norm_gs1: "image_mset pl.Mp (mset gs1) = mset gs1" using norm_gs unfolding gs1 by (induct gs, auto) from pl.unique_factorization_m_factor[OF p uf_h[unfolded h], folded h, OF cop sf l0 refl] obtain fs gs where uf_q: "pl.unique_factorization_m q (lead_coeff q, fs)" and uf_r: "pl.unique_factorization_m r (lead_coeff r, gs)" and id: "mset gs1 = fs + gs" unfolding pl.Mf_def split using norm_gs1 by auto from degh degh_j deg_q deg_r have qj': "degree q < j'" and rj': "degree r < j'" by auto have intro: "u ∈# r ⟹ pl.Mp u ∈# image_mset pl.Mp r" for r by auto note dvdI = pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization intro] from u_gs1 id have "u ∈# fs ∨ u ∈# gs" unfolding in_multiset_in_set[symmetric] by auto with dvdI[OF uf_q] dvdI[OF uf_r] have "pl.dvdm u q ∨ pl.dvdm u r" by auto hence "p.dvdm u q ∨ p.dvdm u r" using pl_dvdm_imp_p_dvdm by blast with 1 qj' rj' show False by (elim disjE, auto dest!: deg) qed qed private definition "ll = (let n = sqrt_int_ceiling (∥f∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j')); ll' = find_exponent p n in if ll' < l then ll' else l)" lemma ll: "ll ≤ l" unfolding ll_def Let_def by auto lemma ll0: "ll ≠ 0" using l0 find_exponent[OF p.m1] unfolding ll_def Let_def by auto lemma pll1: "p^ll > 1" using ll0 p.m1 by auto interpretation pll: poly_mod_2 "p^ll" using ll0 p.m1 by (unfold_locales, auto) lemma pll0: "p^ll ≠ 0" using p by auto lemma dvdm_l_ll: assumes "pl.dvdm a b" shows "pll.dvdm a b" proof - have id: "p^l = p^ll * p ^ (l - ll)" using ll unfolding power_add[symmetric] by auto from assms[unfolded pl.dvdm_def] obtain c where eq: "pl.eq_m b (a * c)" by blast from pll.Mp_shrink_modulus[OF eq[unfolded id]] p have "pll.eq_m b (a * c)" by auto thus ?thesis unfolding pll.dvdm_def .. qed private definition "g ≡ LLL_short_polynomial (p^ll) j u" lemma deg_g_j: "degree g < j" and g0: "g ≠ 0" and ug :"pll.dvdm u g" and short_g: "h ≠ 0 ⟹ pll.dvdm u h ⟹ degree h ≤ j' ⟹ ∥g∥⇧^{2}≤ 2 ^ j' * ∥h∥⇧^{2}" proof (atomize(full), goal_cases) case 1 from deg_u have degu0: "degree u ≠ 0" by auto have ju: "j ≥ degree u" using d_def dj' le_Suc_eq by blast have ju': "j > degree u" using d_def dj' by auto note short = LLL_short_polynomial[OF degu0 ju pll1 u, folded g_def] from short(1-3) short(4)[OF ju'] show ?case by auto qed lemma LLL_reconstruction_inner_simps: "LLL_reconstruction_inner p l gs f u Degs j = (if j' ∉ Degs then None else if p ^ ll ≤ ¦lead_coeff g¦ then None else case div_int_poly f (primitive_part g) of None ⇒ None | Some f' ⇒ Some ([gi←gs . ¬ p.dvdm gi (primitive_part g)], lead_coeff f', f', primitive_part g))" proof - have Suc: "Suc j' - 1 = j'" by simp show ?thesis unfolding LLL_reconstruction_inner_def Suc Let_def ll_def[unfolded Let_def, symmetric] g_def[unfolded Let_def, symmetric] by simp qed lemma LLL_reconstruction_inner_complete: assumes ret: "LLL_reconstruction_inner p l gs f u Degs j = None" shows "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ degree factor ≥ j" proof (rule ccontr) fix factor assume pu_factor: "p.dvdm u factor" and factor_f: "factor dvd f" and deg_factor2: "¬ j ≤ degree factor" with deg[OF this(1,2)] have deg_factor_j [simp]: "degree factor = j'" and deg_factor_lt_j: "degree factor < j" by auto from Degs[OF factor_f pu_factor] have Degs: "(j' ∉ Degs) = False" by auto from dvdm_power[OF factor_f] pu_factor have u_factor: "pl.dvdm u factor" by auto from dvdm_l_ll[OF u_factor] have pll_u_factor: "pll.dvdm u factor" by auto have deg_factor: "degree factor > 0" using d0 deg_factor_j dj' by linarith from f0 deg_factor divides_degree[OF factor_f] have deg_f: "degree f > 0" by auto from deg_factor have j'0: "j' > 0" by simp from factor_f f0 have factor0: "factor ≠ 0" by auto from factor_f obtain f2 where f: "f = factor * f2" unfolding dvd_def by auto from deg_u have deg_u0: "degree u ≠ 0" by auto from pu_factor u have u_j': "degree u ≤ j'" unfolding deg_factor_j[symmetric] using d_def deg_factor_j dj' by blast hence u_j: "degree u ≤ j" "degree u < j" by auto note LLL = LLL_short_polynomial[OF deg_u0 u_j(1) pll1 u, folded g_def] note ret = ret[unfolded LLL_reconstruction_inner_simps Degs if_False] note LLL = LLL(1-3) LLL(4)[OF u_j(2) factor0 pll_u_factor deg_factor_lt_j] hence deg_g: "degree g ≤ j'" by simp from LLL(2) have normg: "∥g∥⇧^{2}≥ 1" using sq_norm_poly_pos[of g] by presburger from f0 have normf: "∥f∥⇧^{2}≥ 1" using sq_norm_poly_pos[of f] by presburger from factor0 have normf1: "∥factor∥⇧^{2}≥ 1" using sq_norm_poly_pos[of factor] by presburger from F0 have normF: "∥F∥⇧^{2}≥ 1" using sq_norm_poly_pos[of F] by presburger from factor_f ‹f dvd F› have factor_F: "factor dvd F" by (rule dvd_trans) have "∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor ≤ ∥factor∥⇧^{2}^ j' * ∥g∥⇧^{2}^ j'" by (rule mult_mono[OF power_increasing], insert normg normf1 deg_g, auto) also have "… = (∥factor∥⇧^{2}* ∥g∥⇧^{2})^j'" by (simp add: power_mult_distrib) also have "… ≤ (∥factor∥⇧^{2}* (2 ^ j' * ∥factor∥⇧^{2}))^j'" by (rule power_mono[OF mult_left_mono], insert LLL(4), auto) also have "… = ∥factor∥⇧^{2}^ (2 * j') * 2 ^ (j' * j')" unfolding power_mult_distrib power_mult power_add mult_2 by simp finally have approx_part_1: "∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor ≤ ∥factor∥⇧^{2}^ (2 * j') * 2 ^ (j' * j')" . { fix f :: "int poly" assume *: "factor dvd f" "f ≠ 0" note approx_part_1 also have "∥factor∥⇧^{2}^ (2 * j') * 2 ^ (j' * j') ≤ (2^(2*j') * ∥f∥⇧^{2}) ^ (2 * j') * 2 ^ (j' * j')" by (rule mult_right_mono[OF power_mono], insert sq_norm_factor_bound[OF *], auto) also have "… = ∥f∥⇧^{2}^ (2 * j') * 2 ^ (2*j' * 2*j' + j' * j')" unfolding power_mult_distrib power_add by (simp add: power_mult[symmetric]) also have "2*j' * 2*j' + j' * j' = 5 * j' * j'" by simp finally have "∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor ≤ ∥f∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j')" . } note approx = this note approx_1 = approx[OF factor_f f0] note approx_2_part = approx[OF factor_F F0] have large: "∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor < (p^ll)⇧^{2}" proof (cases "ll = l") case False let ?n = "∥f∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j')" have n: "?n ≥ 0" by auto let ?s = "sqrt_int_ceiling ?n" from False have "ll = find_exponent p ?s" unfolding ll_def Let_def by auto hence spll: "?s < p^ll" using find_exponent(1)[OF p.m1] by auto have "sqrt ?n ≥ 0" by auto hence sqrt: "sqrt ?n > -1" by linarith have ns: "?n ≤ ?s^2" using sqrt_int_ceiling_bound[OF n] . also have "… < (p^ll)^2" by (rule power_strict_mono[OF spll], insert sqrt, auto) finally show ?thesis using approx_1 by auto next case True hence ll: "p^ll = p^l" by simp show ?thesis unfolding ll proof (rule less_le_trans[OF le_less_trans[OF approx_2_part] bound_l]) have "∥F∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j') = 2 ^ (2 * j' * j' + 3 * j' * j') * ∥F∥⇧^{2}^ (j' + j')" unfolding mult_2 by simp also have "… < 2 ^ (N⇧^{2}+ 4 * N*N) * ∥F∥⇧^{2}^ (2 * N)" proof (rule mult_less_le_imp_less[OF power_strict_increasing pow_mono_exp]) show "1 ≤ ∥F∥⇧^{2}" by (rule normF) have jN': "j' < N" and jN: "j' ≤ N" using jn divides_degree[OF ‹f dvd F›] F0 by auto have "j' + j' ≤ j' + j'" using deg_g j'n by auto also have "… = 2 * j'" by auto also have "… ≤ 2 * N" using jN by auto finally show "j' + j' ≤ 2 * N" . show "0 < ∥F∥⇧^{2}^ (j' + j')" by (rule zero_less_power, insert normF, auto) have "2 * j' * j' + 3 * j' * j' ≤ 2 * j' * j' + 3 * j' * j'" by auto also have "… = 5 * (j' * j')" by auto also have "… < 5 * (N * N)" by (rule mult_strict_left_mono[OF mult_strict_mono], insert jN', auto) also have "… = N⇧^{2}+ 4 * N * N" by (simp add: power2_eq_square) finally show "2 * j' * j' + 3 * j' * j' < N⇧^{2}+ 4 * N * N" . qed auto also have "… = 2 ^ N⇧^{2}* (2 ^ (2 * N) * ∥F∥⇧^{2}) ^ (2 * N)" unfolding power_mult_distrib power_add by (simp add: power_mult[symmetric]) finally show "∥F∥⇧^{2}^ (2 * j') * 2 ^ (5 * j' * j') < 2 ^ N⇧^{2}* B2_LLL F ^ (2 * N)" unfolding B2_LLL_def by simp qed qed have "(¦lead_coeff g¦)^2 < (p^ll)^2" proof (rule le_less_trans[OF _ large]) have "1 * (¦lead_coeff g¦⇧^{2})^1 ≤ ∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor" by (rule mult_mono[OF _ order.trans[OF power_mono pow_mono_exp]], insert normg normf1 deg_f g0 coeff_le_sq_norm[of g] j'0, auto intro: pow_mono_one) thus "¦lead_coeff g¦⇧^{2}≤ ∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor" by simp qed hence "(lead_coeff g)^2 < (p^ll)^2" by simp hence "¦lead_coeff g¦ < p^ll" using p.m1 abs_le_square_iff[of "p^ll" "lead_coeff g"] by auto hence "(p^ll ≤ ¦lead_coeff g¦) = False" by auto note ret = ret[unfolded this if_False] have deg_f: "degree f > 0" using n0 by auto have deg_ug: "degree u ≤ degree g" proof (rule pll.dvdm_degree[OF u LLL(3)], standard) assume "pll.Mp g = 0" from arg_cong[OF this, of "λ p. coeff p (degree g)"] have "pll.M (coeff g (degree g)) = 0" by (auto simp: pll.Mp_def coeff_map_poly) from this[unfolded pll.M_def] obtain c where lg: "lead_coeff g = p^ll * c" by auto with LLL(2) have c0: "c ≠ 0" by auto hence "(p^ll)^2 ≤ (lead_coeff g)^2" unfolding lg abs_le_square_iff[symmetric] by (rule aux_abs_int) also have "… ≤ ∥g∥⇧^{2}" using coeff_le_sq_norm[of g] by auto also have "… = ∥g∥⇧^{2}^ 1" by simp also have "… ≤ ∥g∥⇧^{2}^ degree factor" by (rule pow_mono_exp, insert deg_f normg j'0, auto) also have "… = 1 * …" by simp also have "… ≤ ∥factor∥⇧^{2}^ degree g * ∥g∥⇧^{2}^ degree factor" by (rule mult_right_mono, insert normf1, auto) also have "… < (p^ll)⇧^{2}" by (rule large) finally show False by auto qed with deg_u have deg_g: "degree g > 0" by simp from j'0 have deg_factor: "degree factor > 0" by simp let ?g = "gcd factor g" from common_factor_via_short[OF deg_factor deg_g u deg_u pll_u_factor LLL(3) large] pll.m1 have gcd: "0 < degree ?g" by auto have gcd_factor: "?g dvd factor" by auto from dvd_trans[OF this factor_f] have gcd_f: "?g dvd f" . from deg_g have g0: "g ≠ 0" by auto have gcd_g: "degree ?g ≤ degree g" using g0 using divides_degree by blast from gcd_g LLL(1) have hj': "degree ?g ≤ j'" by auto let ?pp = "primitive_part g" from ret have "div_int_poly f ?pp = None" by (auto split: option.splits) from div_int_poly[of f ?pp, unfolded this] g0 have ppf: "¬ ?pp dvd f" unfolding dvd_def by (auto simp: ac_simps) have irr_f1: "irreducible⇩_{d}factor" by (rule factor_irreducible⇩_{d}I[OF factor_f pu_factor deg_factor], simp) from gcd_factor obtain h where factor: "factor = ?g * h" unfolding dvd_def by auto from irreducible⇩_{d}D(2)[OF irr_f1, of ?g h, folded factor] have "¬ (degree ?g < j' ∧ degree h < j')" by auto moreover have "j' = degree ?g + degree h" using factor0 arg_cong[OF factor, of degree] by (subst (asm) degree_mult_eq, insert j'0, auto) ultimately have "degree h = 0" using gcd by linarith from degree0_coeffs[OF this] factor factor0 obtain c where h: "h = [:c:]" and c: "c ≠ 0" by fastforce from arg_cong[OF factor, of degree] have id: "degree ?g = degree factor" unfolding h using c by auto moreover have "degree ?g ≤ degree g" by (subst gcd.commute, rule degree_gcd1[OF g0]) ultimately have "degree g ≥ degree factor" by auto with id deg_factor2 deg_g_j have deg: "degree ?g = degree g" and "degree g = degree factor" by auto have "?g dvd g" by auto then obtain q where g: "g = ?g * q" unfolding dvd_def by auto from arg_cong[OF this, of degree] deg have "degree q = 0" by (subst (asm) degree_mult_eq, insert g g0, force, force) simp from degree0_coeffs[OF this] g g0 obtain d where p: "q = [:d:]" and d: "d ≠ 0" by fastforce from arg_cong[OF factor, of "(*) q"] have "q * factor = h * g" by (subst g, auto simp: ac_simps) hence "smult d factor = h * g" unfolding p h by auto hence "g dvd smult d factor" by simp from dvd_smult_int[OF d this] have "primitive_part g dvd factor" . from dvd_trans[OF this factor_f] ppf show False by auto qed lemma LLL_reconstruction_inner_sound: assumes ret: "LLL_reconstruction_inner p l gs f u Degs j = Some (gs',b',f',h)" shows "f = f' * h" (is "?g1") and "irreducible⇩_{d}h" (is "?g2") and "b' = lead_coeff f'" (is "?g3") and "pl.unique_factorization_m f' (lead_coeff f', mset gs')" (is "?g4") and "p.dvdm u h" (is ?g5) and "degree h = j'" (is ?g6) and "length gs' < length gs" (is ?g7) and "set gs' ⊆ set gs" (is ?g8) and "gs' ≠ []" (is ?g9) proof - let ?ppg = "primitive_part g" note ret = ret[unfolded LLL_reconstruction_inner_simps] from ret have lc: "abs (lead_coeff g) < p^ll" by (auto split: if_splits) from ret obtain rest where rest: "div_int_poly f (primitive_part g) = Some rest" by (auto split: if_splits option.splits) from ret[unfolded this] div_int_then_rqp[OF this] lc have out [simp]: "h = ?ppg" "gs' = filter (λ gi. ¬ p.dvdm gi ?ppg) gs" "f' = rest" "b' = lead_coeff rest" and f: "f = ?ppg * rest" by (auto split: if_splits) with div_int_then_rqp[OF rest] show ?g1 ?g3 by auto from ‹?g1› f0 have h0: "h ≠ 0" by auto let ?c = "content g" from g0 have ct0: "?c ≠ 0" by auto have "¦?c¦ ≤ ¦lead_coeff g¦" by (rule content_le_lead_coeff) also have "… < p^ll" by fact finally have ct_pl: "¦?c¦ < p^ll" . from ug have "pll.dvdm u (smult ?c ?ppg)" by simp from poly_mod_dvd_drop_smult[OF u p ct0 ct_pl this] show puh: "p.dvdm u h" by simp with dvdm_power[of h] f have uh: "pl.dvdm u h" by (auto simp: dvd_def) from f have hf: "h dvd f" by (auto intro:dvdI) have degh: "degree h > 0" by (metis d_def deg deg_u puh dj' hf le_neq_implies_less not_less0 neq0_conv) show irr_h: ?g2 by (intro factor_irreducible⇩_{d}I degh hf puh, insert deg_g_j, simp) show deg_h: ?g6 using deg deg_g_j g_def hf le_less_Suc_eq puh degree_primitive_part by force show ?g7 unfolding out by (rule length_filter_less[of u], insert pl_dvdm_imp_p_dvdm[OF uh] u_gs, auto) show ?g8 by auto from f out have fh: "f = h * f'" and gs': "gs' = [gi ← gs. ¬ p.dvdm gi h]" by auto note [simp del] = out let ?fs = "filter (λgi. p.dvdm gi h) gs" have part: "List.partition (λgi. p.dvdm gi h) gs = (?fs, gs')" unfolding gs' by (auto simp: o_def) from p.unique_factorization_m_factor_partition[OF l0 f_gs fh cop sf part] show uf: "pl.unique_factorization_m f' (lead_coeff f', mset gs')" by auto show ?g9 proof assume "gs' = []" with pl.unique_factorization_m_imp_factorization[OF uf, unfolded pl.factorization_m_def] have "pl.Mp f' = pl.Mp (smult (lead_coeff f') 1)" by auto from arg_cong[OF this, of degree] pl.degree_m_le[of "smult (lead_coeff f') 1"] have "pl.degree_m f' = 0" by simp also have "pl.degree_m f' = degree f'" proof (rule poly_mod.degree_m_eq[OF _ pl.m1]) have "coprime (lead_coeff f') p" by (rule p.coprime_lead_coeff_factor[OF p.prime cop[unfolded fh]]) thus "lead_coeff f' mod p ^ l ≠ 0" using l0 p.prime by fastforce qed finally have degf': "degree f' = 0" by auto from degree0_coeffs[OF this] f0 fh obtain c where "f' = [:c:]" and c: "c ≠ 0" and fch: "f = smult c h" by auto from ‹irreducible⇩_{d}h› have irr_f: "irreducible⇩_{d}f" using irreducible⇩_{d}_smult_int[OF c, of h] unfolding fch by auto have "degree f = j'" using hf irr_h deg_h using irr_f ‹n ≡ degree f› degh j'n by (metis add.right_neutral degf' degree_mult_eq f0 fh mult_not_zero) thus "False" using j'n by auto qed qed end interpretation LLL d . lemma LLL_reconstruction_inner_None_upt_j': assumes ij: "∀i∈{d+1..j}. LLL_reconstruction_inner p l gs f u Degs i = None" and dj: "d<j" and "j≤n" shows "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ degree factor ≥ j" using assms proof (induct j) case (Suc j) show ?case proof (rule LLL_reconstruction_inner_complete) show "⋀factor2. p.dvdm u factor2 ⟹ factor2 dvd f ⟹ j ≤ degree factor2" proof (cases "d = j") case False show "⋀factor2. p.dvdm u factor2 ⟹ factor2 dvd f ⟹ j ≤ degree factor2" by (rule Suc.hyps, insert Suc.prems False, auto) next case True then show "⋀factor2. p.dvdm u factor2 ⟹ factor2 dvd f ⟹ j ≤ degree factor2" using degree_factor_ge_degree_u by auto qed qed (insert Suc.prems, auto) qed auto corollary LLL_reconstruction_inner_None_upt_j: assumes ij: "∀i∈{d+1..j}. LLL_reconstruction_inner p l gs f u Degs i = None" and dj: "d≤j" and jn: "j≤n" shows "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ degree factor ≥ j" proof (cases "d=j") case True then show "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ d = j ⟹ j ≤ degree factor" using degree_factor_ge_degree_u by auto next case False hence dj2: "d<j" using dj by auto then show "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ d ≠ j ⟹ j ≤ degree factor" using LLL_reconstruction_inner_None_upt_j'[OF ij dj2 jn] by auto qed lemma LLL_reconstruction_inner_all_None_imp_irreducible: assumes i: "∀i∈{d+1..n}. LLL_reconstruction_inner p l gs f u Degs i = None" shows "irreducible⇩_{d}f" proof - obtain factor where irreducible_factor: "irreducible⇩_{d}factor" and dvdp_u_factor: "p.dvdm u factor" and factor_dvd_f: "factor dvd f" using exists_reconstruction by blast have f0: "f ≠ 0" using n0 by auto have deg_factor1: "degree u ≤ degree factor" by (rule degree_factor_ge_degree_u[OF dvdp_u_factor factor_dvd_f]) hence factor_not0: "factor ≠ 0" using d0 by auto hence deg_factor2: "degree factor ≤ degree f" using divides_degree[OF factor_dvd_f] f0 by auto let ?j = "degree factor" show ?thesis proof (cases "degree factor = degree f") case True from factor_dvd_f obtain g where f_factor: "f = factor * g" unfolding dvd_def by auto from True[unfolded f_factor] f0[unfolded f_factor] have "degree g = 0" "g ≠ 0" by (subst (asm) degree_mult_eq, auto) from degree0_coeffs[OF this(1)] this(2) obtain c where "g = [:c:]" and c: "c ≠ 0" by auto with f_factor have fc: "f = smult c factor" by auto from irreducible_factor irreducible⇩_{d}_smult_int[OF c, of factor, folded fc] show ?thesis by simp next case False hence Suc_j: "Suc ?j ≤ degree f" using deg_factor2 by auto have "Suc ?j ≤ degree factor" proof (rule LLL_reconstruction_inner_None_upt_j[OF _ _ _ dvdp_u_factor factor_dvd_f]) show "d ≤ Suc ?j" using deg_factor1 by auto show "∀i∈{d + 1..(Suc ?j)}. LLL_reconstruction_inner p l gs f u Degs i = None" using Suc_j i by auto show "Suc ?j ≤ n" using Suc_j by simp qed then show ?thesis by auto qed qed lemma irreducible_imp_LLL_reconstruction_inner_all_None: assumes irr_f: "irreducible⇩_{d}f" shows "∀i∈{d+1..n}. LLL_reconstruction_inner p l gs f u Degs i = None" proof (rule ccontr) let ?LLL_inner = "λi. LLL_reconstruction_inner p l gs f u Degs i" let ?G ="{j. j ∈ {d + 1..n} ∧ ?LLL_inner j ≠ None}" assume "¬ (∀i∈{d + 1..n}. ?LLL_inner i = None)" hence G_not_empty: "?G ≠ {}" by auto define j where "j = Min ?G" have j_in_G: "j ∈ ?G" by (unfold j_def, rule Min_in[OF _ G_not_empty], simp) hence j: "j ∈ {d + 1..n}" and LLL_not_None: "?LLL_inner j ≠ None" using j_in_G by auto have "∀i∈{d+1..<j}. ?LLL_inner i = None" proof (rule ccontr) assume "¬ (∀i∈{d + 1..<j}. ?LLL_inner i = None)" from this obtain i where i: "i ∈ {d + 1..<j}" and LLL_i: "?LLL_inner i ≠ None" by auto hence iG: "i ∈ ?G" using j_def G_not_empty by auto have "i<j" using i by auto moreover have "j≤i" using iG j_def by auto ultimately show False by linarith qed hence all_None: "∀i∈{d+1..j-1}. ?LLL_inner i = None" by auto obtain gs' b' f' factor where LLL_inner_eq: "?LLL_inner j = Some (gs', b', f', factor)" using LLL_not_None by force have Suc_j1_eq: "Suc (j - 1) = j" using j d0 by auto have jn: "j - 1 < n" using j by auto have dj: "d ≤ j-1" using j d0 by auto have degree: "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ j - 1 ≤ degree factor" by (rule LLL_reconstruction_inner_None_upt_j[OF all_None dj], insert jn, auto) have LLL_inner_Some: "?LLL_inner (Suc (j - 1)) = Some (gs', b', f', factor)" using LLL_inner_eq Suc_j1_eq by auto have deg_factor: "degree factor = j-1" and ff': "f = f' * factor" and irreducible_factor: "irreducible⇩_{d}factor" using LLL_reconstruction_inner_sound[OF dj jn degree LLL_inner_Some] by (metis+) have "degree f' = n - (j - 1)" using arg_cong[OF ff', of degree] by (subst (asm) degree_mult_eq, insert f0 ff' deg_factor, auto) also have "… < n" using irreducible_factor jn unfolding irreducible⇩_{d}_def deg_factor by auto finally have deg_f': "degree f' < degree f" by auto from ff' have factor_dvd_f: "factor dvd f" by auto have "¬ irreducible⇩_{d}f" by (rule reducible⇩_{d}I, rule exI[of _ f'], rule exI[of _ factor], intro conjI ff', insert deg_factor jn deg_f', auto) thus False using irr_f by contradiction qed lemma LLL_reconstruction_inner_all_None: assumes i: "∀i∈{d+1..n}. LLL_reconstruction_inner p l gs f u Degs i = None" and dj: "d<j" shows "LLL_reconstruction_inner_loop p l gs f u Degs j = ([],1,1,f)" using dj proof (induct j rule: LLL_reconstruction_inner_loop.induct[of f p l gs u Degs]) case (1 j) let ?innerl = "LLL_reconstruction_inner_loop p l gs f u Degs" let ?inner = "LLL_reconstruction_inner p l gs f u Degs" note hyp = "1.hyps" note dj = "1.prems"(1) show ?case proof (cases "j≤n") case True note jn = True have step: "?inner j = None" by (cases "d=j", insert i jn dj, auto) have "?innerl j = ?innerl (j+1)" using jn step by auto also have "... = ([], 1, 1, f)" by (rule hyp[OF _ step], insert jn dj, auto simp add: jn dj) finally show ?thesis . qed auto qed corollary irreducible_imp_LLL_reconstruction_inner_loop_f: assumes irr_f: "irreducible⇩_{d}f" and dj: "d<j" shows "LLL_reconstruction_inner_loop p l gs f u Degs j = ([],1,1,f)" using irreducible_imp_LLL_reconstruction_inner_all_None[OF irr_f] using LLL_reconstruction_inner_all_None[OF _ dj] by auto lemma exists_index_LLL_reconstruction_inner_Some: assumes inner_loop: "LLL_reconstruction_inner_loop p l gs f u Degs j = (gs',b',f',factor)" and i: "∀i∈{d+1..<j}. LLL_reconstruction_inner p l gs f u Degs i = None" and dj: "d<j" and jn: "j≤n" and f: "¬ irreducible⇩_{d}f" shows "∃j'. j ≤ j' ∧ j'≤n ∧ d<j' ∧ (LLL_reconstruction_inner p l gs f u Degs j' = Some (gs', b', f', factor)) ∧ (∀i∈{d+1..<j'}. LLL_reconstruction_inner p l gs f u Degs i = None)" using inner_loop i dj jn proof (induct j rule: LLL_reconstruction_inner_loop.induct[of f p l gs u Degs]) case (1 j) let ?innerl = "LLL_reconstruction_inner_loop p l gs f u Degs" let ?inner = "LLL_reconstruction_inner p l gs f u Degs" note hyp = "1.hyps" note 1 = "1.prems"(1) note 2 = "1.prems"(2) note dj = "1.prems"(3) note jn = "1.prems"(4) show ?case proof (cases "?inner j = None") case True show ?thesis proof (cases "j=n") case True note j_eq_n = True show ?thesis proof (cases "?inner n = None") case True have i2: "∀i∈{d + 1..n}. ?inner i = None" using 2 j_eq_n True by auto have "irreducible⇩_{d}f" by(rule LLL_reconstruction_inner_all_None_imp_irreducible[OF i2]) thus ?thesis using f by simp next case False have "?inner n = Some (gs', b', f', factor)" using False 1 j_eq_n by auto moreover have "∀i∈{d + 1..<n}. ?inner i = None" using 2 j_eq_n by simp moreover have "d < n" using 1 2 jn j_eq_n using False dn nat_less_le using d_def dj by auto ultimately show ?thesis using j_eq_n by fastforce qed next case False have "∃j'≥j + 1. j' ≤ n ∧ d < j' ∧ ?inner j' = Some (gs', b', f', factor) ∧ (∀i∈{d + 1..<j'}. ?inner i = None)" proof (rule hyp) show "¬ degree f < j" using jn by auto show "?inner j = None" using True by auto show "?innerl (j + 1) = (gs', b', f', factor)" using 1 True jn by auto show "∀i∈{d + 1..<j + 1}. ?inner i = None" by (metis "2" One_nat_def True add.comm_neutral add_Suc_right atLeastLessThan_iff le_neq_implies_less less_Suc_eq_le) show "d < j + 1" using dj by auto show " j + 1 ≤ n" using jn False by auto qed from this obtain j' where a1: "j'≥j + 1" and a2: "j' ≤ n" and a3: "d < j'" and a4: "?inner j' = Some (gs', b', f', factor)" and a5: "(∀i∈{d + 1..<j'}. ?inner i = None)" by auto moreover have "j'≥j" using a1 by auto ultimately show ?thesis by fastforce qed next case False have 1: "?inner j = Some (gs', b', f', factor)" using False 1 jn by auto moreover have 2: "(∀i∈{d + 1..<j}. ?inner i = None)" by (rule 2) moreover have 3: "j ≤ n" using jn by auto moreover have 4: "d < j" using 2 False dj jn using le_neq_implies_less by fastforce ultimately show ?thesis by auto qed qed (* TODO: move *) lemma unique_factorization_m_1: "pl.unique_factorization_m 1 (1, {#})" proof (intro pl.unique_factorization_mI) fix d gs assume pl: "pl.factorization_m 1 (d,gs)" from pl.factorization_m_degree[OF this] have deg0: "⋀ g. g ∈# gs ⟹ pl.degree_m g = 0" by auto { assume "gs ≠ {#}" then obtain g hs where gs: "gs = {# g #} + hs" by (cases gs, auto) with pl have *: "pl.irreducible⇩_{d}_m (pl.Mp g)" "monic (pl.Mp g)" by (auto simp: pl.factorization_m_def) with deg0[of g, unfolded gs] have False by (auto simp: pl.irreducible⇩_{d}_m_def) } hence "gs = {#}" by auto with pl show "pl.Mf (d, gs) = pl.Mf (1, {#})" by (cases "d = 0", auto simp: pl.factorization_m_def pl.Mf_def pl.Mp_def) qed (auto simp: pl.factorization_m_def) lemma LLL_reconstruction_inner_loop_j_le_n: assumes ret: "LLL_reconstruction_inner_loop p l gs f u Degs j = (gs',b',f',factor)" and ij: "∀i∈{d+1..<j}. LLL_reconstruction_inner p l gs f u Degs i = None" and n: "n = degree f" and jn: "j ≤ n" and dj: "d < j" shows "f = f' * factor" (is "?g1") and "irreducible⇩_{d}factor" (is "?g2") and "b' = lead_coeff f'" (is "?g3") and "pl.unique_factorization_m f' (b', mset gs')" (is "?g4") and "p.dvdm u factor" (is ?g5) and "gs ≠ [] ⟶ length gs' < length gs" (is ?g6) and "factor dvd f" (is ?g7) and "f' dvd f" (is ?g8) and "set gs' ⊆ set gs" (is ?g9) and "gs' = [] ⟶ f' = 1" (is ?g10) using ret ij jn dj proof (atomize(full), induct j) case 0 then show ?case using deg_u by auto next case (Suc j) let ?innerl = "LLL_reconstruction_inner_loop p l gs f u Degs" let ?inner = "LLL_reconstruction_inner p l gs f u Degs" have ij: "∀i∈{d+1..j}. ?inner i = None" using Suc.prems by auto have dj: "d ≤ j" using Suc.prems by auto have jn: "j<n" using Suc.prems by auto have deg: "Suc j ≤ degree f" using Suc.prems by auto have c: "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ j ≤ degree factor" by (rule LLL_reconstruction_inner_None_upt_j[OF ij dj], insert n jn, auto) have 1: "?innerl (Suc j) = (gs', b', f', factor)" using Suc.prems by auto show ?case proof (cases "?inner (Suc j) = None") case False have LLL_rw: "?inner (Suc j) = Some (gs', b', f', factor)" using False deg Suc.prems by auto show ?thesis using LLL_reconstruction_inner_sound[OF dj jn c LLL_rw] by fastforce next case True note Suc_j_None = True show ?thesis proof (cases "d = j") case False have nj: "j ≤ degree f" using Suc.prems False by auto moreover have dj2: "d < j" using Suc.prems False by auto ultimately show ?thesis using Suc.prems Suc.hyps by fastforce next case True note d_eq_j = True show ?thesis proof (cases "irreducible⇩_{d}f") case True have pl_Mp_1: "pl.Mp 1 = 1" by auto have d_Suc_j: "d < Suc j" using Suc.prems by auto have "?innerl (Suc j) = ([],1,1,f)" by (rule irreducible_imp_LLL_reconstruction_inner_loop_f[OF True d_Suc_j]) hence result_eq: "([],1,1,f) = (gs', b', f', factor)" using Suc.prems by auto moreover have thesis1: "p.dvdm u factor" using u_f result_eq by auto moreover have thesis2: "f' = pl.Mp (Polynomial.smult b' (prod_list gs'))" using result_eq pl_Mp_1 by auto ultimately show ?thesis using True by (auto simp: unique_factorization_m_1) next case False note irreducible_f = False have "∃j'. Suc j ≤ j' ∧ j'≤n ∧ d<j' ∧ (?inner j' = Some (gs', b', f', factor)) ∧ (∀i∈{d+1..<j'}. ?inner i = None)" proof (rule exists_index_LLL_reconstruction_inner_Some[OF _ _ _ _ False]) show "?innerl (Suc j) = (gs', b', f', factor)" using Suc.prems by auto show "∀i ∈ {d + 1..<Suc j}. ?inner i = None" using Suc.prems by auto show "Suc j ≤ n" using jn by auto show "d < Suc j " using Suc.prems by auto qed from this obtain a where da: "d < a" and an: "a ≤ n" and ja: "j ≤ a" and a1: "?inner a = Some (gs', b', f', factor)" and a2: "∀i∈{d+1..<a}. ?inner i = None" by auto define j' where j'[simp]: "j'≡a-1" have dj': "d ≤ j'" using da by auto have j': "j' ≠ 0" using dj' d0 by auto hence j'n: "j' < n" using an by auto have LLL: "?inner (Suc j') = Some (gs', b', f', factor)" using a1 j' by auto have prev_None: "∀i∈{d+1..j'}. ?inner i = None" using a2 j' by auto have Suc_rw: "Suc (j'- 1) = j'" using j' by auto have c: "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ Suc (j' - 1) ≤ degree factor" by (rule LLL_reconstruction_inner_None_upt_j, insert dj' Suc_rw j'n prev_None, auto) hence c2: "⋀factor. p.dvdm u factor ⟹ factor dvd f ⟹ j' ≤ degree factor" using j' by force show ?thesis using LLL_reconstruction_inner_sound[OF dj' j'n c2 LLL] by fastforce qed qed qed qed lemma LLL_reconstruction_inner_loop_j_ge_n: assumes ret: "LLL_reconstruction_inner_loop p l gs f u Degs j = (gs',b',f',factor)" and ij: "∀i∈{d+1..n}. LLL_reconstruction_inner p l gs f u Degs i = None" and dj: "d < j" and jn: "j>n" shows "f = f' * factor" (is "?g1") and "irreducible⇩_{d}factor" (is "?g2") and "b' = lead_coeff f'" (is "?g3") and "pl.unique_factorization_m f' (b', mset gs')" (is "?g4") and "p.dvdm u factor" (is ?g5) and "gs ≠ [] ⟶ length gs' < length gs" (is ?g6) and "factor dvd f" (is ?g7) and "f' dvd f" (is ?g8) and "set gs' ⊆ set gs" (is ?g9) and "f' = 1" (is ?g10) proof - have "LLL_reconstruction_inner_loop p l gs f u Degs j = ([],1,1,f)" using jn by auto hence gs': "gs'=[]" and b': "b'=1" and f': "f' = 1" and factor: "factor = f" using ret by auto have "irreducible⇩_{d}f" by (rule LLL_reconstruction_inner_all_None_imp_irreducible[OF ij]) thus ?g1 ?g2 ?g3 ?g4 ?g5 ?g6 ?g7 ?g8 ?g9 ?g10 using f' factor b' gs' u_f by (auto simp: unique_factorization_m_1) qed lemma LLL_reconstruction_inner_loop: assumes ret: "LLL_reconstruction_inner_loop p l gs f u Degs j = (gs',b',f',factor)" and ij: "∀i∈{d+1..<j}. LLL_reconstruction_inner p l gs f u Degs i = None" and n: "n = degree f" and dj: "d < j" shows "f = f' * factor" (is "?g1") and "irreducible⇩_{d}factor" (is "?g2") and "b' = lead_coeff f'" (is "?g3") and "pl.unique_factorization_m f' (b', mset gs')" (is "?g4") and "p.dvdm u factor" (is ?g5) and "gs ≠ [] ⟶ length gs' < length gs" (is ?g6) and "factor dvd f" (is ?g7) and "f' dvd f" (is ?g8) and "set gs' ⊆ set gs" (is ?g9) and "gs' = [] ⟶ f' = 1" (is ?g10) proof (atomize(full),(cases "j>n"; intro conjI)) case True have ij2: "∀i∈{d + 1..n}. LLL_reconstruction_inner p l gs f u Degs i = None" using ij True by auto show ?g1 ?g2 ?g3 ?g4 ?g5 ?g6 ?g7 ?g8 ?g9 ?g10 using LLL_reconstruction_inner_loop_j_ge_n[OF ret ij2 dj True] by blast+ next case False hence jn: "j≤n" by simp show ?g1 ?g2 ?g3 ?g4 ?g5 ?g6 ?g7 ?g8 ?g9 ?g10 using LLL_reconstruction_inner_loop_j_le_n[OF ret ij n jn dj] by blast+ qed end subsubsection ‹Outer loop› lemma LLL_reconstruction'': assumes 1: "LLL_reconstruction'' p l gs b f G = G'" and irreducible_G: "⋀factor. factor ∈ set G ⟹ irreducible⇩_{d}factor" and 3: "F = f * prod_list G" and 4: "pl.unique_factorization_m f (lead_coeff f, mset gs)" and 5: "gs ≠ []" and 6: "⋀ gi. gi ∈ set gs ⟹ pl.Mp gi = gi" and 7: "⋀ gi. gi ∈ set gs ⟹ p.irreducible⇩_{d}_m gi" and 8: "p.square_free_m f" and 9: "coprime (lead_coeff f) p" and sf_F: "square_free F" shows "(∀g ∈ set G'. irreducible⇩_{d}g) ∧ F = prod_list G'" using 1 irreducible_G 3 4 5 6 7 8 9 proof (induction gs arbitrary: b f G G' rule: length_induct) case (1 gs) note LLL_f' = "1.prems"(1) note irreducible_G = "1.prems"(2) note F_f_G = "1.prems" (3) note f_gs_factor = "1.prems" (4) note gs_not_empty = "1.prems" (5) note norm = "1.prems"(6) note irred_p = "1.prems"(7) note sf = "1.prems"(8) note cop = "1.prems"(9) obtain u where choose_u_result: "choose_u gs = u" by auto from choose_u_member[OF gs_not_empty, unfolded choose_u_result] have u_gs: "u ∈ set gs" by auto define d n where [simp]: "d = degree u" "n = degree f" hence n_def: "n = degree f" "n ≡ degree f" by auto define gs'' where "gs'' = remove1 u gs" define degs where "degs = map degree gs''" define Degs where "Degs = (+) d ` sub_mset_sums degs" obtain gs' b' h factor where inner_loop_result: "LLL_reconstruction_inner_loop p l gs f u Degs (d+1) = (gs',b',h,factor)" by (metis prod_cases4) have a1: "LLL_reconstruction_inner_loop p l gs f u Degs (d+1) = (gs', b', h, factor)" using inner_loop_result by auto have a2: "∀i∈{degree u + 1..<(d+1)}. LLL_reconstruction_inner p l gs f u Degs i = None" by auto have "LLL_reconstruction'' p l gs b f G = LLL_reconstruction'' p l gs' b' h (factor # G)" unfolding LLL_reconstruction''.simps[of p l gs] using gs_not_empty unfolding Let_def using choose_u_result inner_loop_result unfolding Degs_def degs_def gs''_def by auto hence LLL_eq: "LLL_reconstruction'' p l gs' b' h (factor # G) = G'" using LLL_f' by auto from pl.unique_factorization_m_imp_factorization[OF f_gs_factor, unfolded pl.factorization_m_def] norm have f_gs: "pl.eq_m f (smult (lead_coeff f) (prod_mset (mset gs)))" and mon: "g ∈ set gs ⟹ monic g" and irred: "g ∈ set gs ⟹ pl.irreducible⇩_{d}_m g" for g by auto { from split_list[OF u_gs] obtain gs1 gs2 where gs: "gs = gs1 @ u # gs2" by auto from f_gs[unfolded gs] have "pl.dvdm u f" unfolding pl.dvdm_def by (intro exI[of _ "smult (lead_coeff f) (prod_mset (mset (gs1 @ gs2)))"], auto) } note pl_uf = this hence p_uf: "p.dvdm u f" by (rule pl_dvdm_imp_p_dvdm) have monic_u: "monic u" using mon[OF u_gs] . have irred_u: "p.irreducible_m u" using irred_p[OF u_gs] by auto have degree_m_u: "p.degree_m u = degree u" using monic_u by simp have degree_u[simp]: "0 < degree u" using irred_u by (fold degree_m_u, auto simp add: p.irreducible_degree) have deg_u_d: "degree u < d + 1" by auto from F_f_G have f_dvd_F: "f dvd F" by auto from square_free_factor[OF f_dvd_F sf_F] have sf_f: "square_free f" . from norm have norm_map: "map pl.Mp gs = gs" by (induct gs, auto) { fix factor assume factor_f: "factor dvd f" and u_factor: "p.dvdm u factor" from factor_f obtain h where f: "f = factor * h" unfolding dvd_def by auto obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi factor) gs = (gs1, gs2)" by force from p.unique_factorization_m_factor_partition[OF l0 f_gs_factor f cop sf part] have factor: "pl.unique_factorization_m factor (lead_coeff factor