# Theory Factor_Bound_2

(*
Authors:    Jose Divasón
Sebastiaan Joosten
René Thiemann
*)

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"
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)"
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
*)

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)"
have j2: "degree (q* u + smult m r) = degree (q*u)"
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"
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"
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
have [transfer_rule]: "MP_Rel g G" unfolding MP_Rel_def
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
have g': "Mp g = to_int_poly G" unfolding g
have f'': "of_int_poly (Mp f) = F"
by (metis (no_types, lifting) Dp_Mp_eq Mp_f_representative
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
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"
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)"
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]

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
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]:
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)))))
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
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"
have b[transfer_rule]: "MP_Rel g ?G"
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
*)

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
*)

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

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)}"
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
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
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)}"
(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
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
finally show ?thesis unfolding sq_norm_poly_def by auto
qed

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
also have "... = ?M ! i"
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]"
have "¦resultant f g¦ = ¦det ?S¦"  unfolding resultant_def ..
also have "... ≤ sqrt (of_int (prod_list (map sq_norm (rows ?S))))"
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])"
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:]"
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)"
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"
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
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)))"
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
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⇩dE[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)"
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"
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"
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
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⇩dE[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
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)"
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"
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 -
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 -
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
*)
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"
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}"
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
*)

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"
have [transfer_rule]: "MP_Rel (prod_list xs) ?XS1"
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 = [];
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"]

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"
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)"
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
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⇩dI: 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⇩dI 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"
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')"
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)"
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
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⇩dI[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⇩dD(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
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⇩dI 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])
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⇩dI, 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"
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