Session LLL_Factorization

Theory Factor_Bound_2

(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Factor bound›

text ‹This theory extends the work about factor bounds which was carried out 
  in the Berlekamp-Zassenhaus development.› 

theory Factor_Bound_2
imports Berlekamp_Zassenhaus.Factor_Bound
   LLL_Basis_Reduction.Norms
begin

lemma norm_1_bound_mignotte: "norm1 f  2^(degree f) * mahler_measure f"
proof (cases "f = 0")
  case f0: False
  have cf: "coeffs f = map (λ i. coeff f i) [0 ..< Suc( degree f)]" unfolding coeffs_def 
    using f0 by auto
  have "real_of_int (sum_list (map abs (coeffs f))) 
    = (idegree 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 "  (idegree 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 f2)" 
  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 "h2  2 ^ (2 * degree h) * f2" 
proof - 
  let ?r = real_of_int
  have h21: "?r h2  (?r (norm1 h))^2" using norm2_le_norm1_int[of h]
    by (metis of_int_le_iff of_int_power)
  also have "  (2^(degree h) * mahler_measure h)^2" 
    using power_mono[OF norm_1_bound_mignotte[of h], of 2] 
    by (auto simp: norm1_ge_0)
  also have " = 2^(2 * degree h) * (mahler_measure h)^2"
    by (simp add: power_even_eq power_mult_distrib)
  also have "  2^(2 * degree h) * (mahler_measure f)^2" 
    by (rule mult_left_mono[OF power_mono], auto simp: mahler_measure_ge_0
    mahler_measure_dvd[OF f0 dvd])
  also have "  2^(2 * degree h) * ?r (f2)"
  proof (rule mult_left_mono)
    have "?r (f2)  0" by auto
    from real_sqrt_pow2[OF this]
    show "(mahler_measure f)2  ?r (f2)" 
      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) * f2)" 
    by (simp add: ac_simps)
  finally show "h2  2 ^ (2 * degree h) * f2" unfolding of_int_le_iff .
qed

end

Theory Missing_Dvd_Int_Poly

(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Executable dvdm operation›

text ‹This theory contains some results about division of integer polynomials which are not part of 
  Polynomial\_Factorization.Dvd\_Int\_Poly.thy. 

  Essentially, we give an executable implementation of division modulo m.
› 

theory Missing_Dvd_Int_Poly
imports 
  Berlekamp_Zassenhaus.Poly_Mod_Finite_Field
  Berlekamp_Zassenhaus.Polynomial_Record_Based
  Berlekamp_Zassenhaus.Hensel_Lifting (* for thm pdivmod_monic, should be moved *)
  Subresultants.Subresultant (* for abbreviation pdivmod *)
  Perron_Frobenius.Cancel_Card_Constraint
begin

(*In mathematics, this lemma also works if q = 0 since degree 0 = -∞, but in Isabelle degree 0 = 0.*)
lemma degree_div_mod_smult:
  fixes g::"int poly"
  assumes g: "degree g < j"
  and r: "degree r < d"
  and u: "degree u = d"
  and g1: "g = q * u + smult m r" 
  and q: "q  0" and m_not0: "m  0"
shows "degree q < j - d"
proof -
  have u_not0: "u0" using u r by auto
  have d_uq: "d  degree (u*q)" using u degree_mult_right_le[OF q] by auto
  have j: "j > degree (q* u + smult m r)" using g1 g by auto
  have "degree (smult m r) < d" using degree_smult_eq m_not0 r by auto
  also have "...  degree (u*q)" using d_uq by auto
  finally have deg_mr_uq: "degree (smult m r) < degree (q*u)"
    by (simp add: mult.commute)
  have j2: "degree (q* u + smult m r) = degree (q*u)"
    by (rule degree_add_eq_left[OF deg_mr_uq])
  also have "... = degree q + degree u" 
    by (rule degree_mult_eq[OF q u_not0])
  finally have "degree q = degree g - degree u" using g1 by auto
  thus ?thesis 
    using j j2 ‹degree (q * u) = degree q + degree u u 
    by linarith
qed

subsection ‹Uniqueness of division algorithm for polynomials›

lemma uniqueness_algorithm_division_poly:
  fixes f::"'a::{comm_ring,semiring_1_no_zero_divisors} poly"
  assumes f1: "f = g * q1 + r1"
      and f2: "f = g * q2 + r2"
      and g: "g  0"
      and r1: "r1 = 0  degree r1 < degree g"
      and r2: "r2 = 0  degree r2 < degree g"
    shows "q1 = q2  r1 = r2"
proof -
  have "0 =  g * q1 + r1 - (g * q2 + r2)" using f1 f2 by auto
  also have "... = g * (q1 - q2) + r1 - r2"
    by (simp add: right_diff_distrib)
  finally have eq: "g * (q1 - q2) = r2 - r1" by auto
  have q_eq: "q1 = q2" 
  proof (rule ccontr)
    assume q1_not_q2: "q1  q2" 
    hence nz: "g * (q1 - q2)  0" using g by auto
    hence "degree (g * (q1 - q2))  degree g"      
      by (simp add: degree_mult_right_le)
    moreover have "degree (r2 - r1) < degree g"
      using eq nz degree_diff_less r1 r2 by auto
    ultimately show False using eq by auto
  qed
  moreover have "r1 = r2" using eq q_eq by auto
  ultimately show ?thesis by simp
qed

lemma pdivmod_eq_pdivmod_monic:
  assumes g: "monic g"
  shows "pdivmod f g = pdivmod_monic f g"
proof -
  obtain q r where qr: "pdivmod f g = (q,r)" by simp
  obtain Q R where QR: "pdivmod_monic f g = (Q,R)" by (meson surj_pair)
  have g0: "g  0" using g by auto
  have f1: "f = g * q + r"
    by (metis Pair_inject mult_div_mod_eq qr)
  have r: "r=0  degree r < degree g"
    by (metis Pair_inject assms degree_mod_less leading_coeff_0_iff qr zero_neq_one)
  have f2: "f = g * Q + R"    
    by (simp add: QR assms pdivmod_monic(1))
  have R: "R=0  degree R < degree g" 
    by (rule pdivmod_monic[OF g QR])  
  have "q=Q  r=R" by (rule uniqueness_algorithm_division_poly[OF f1 f2 g0 r R])
  thus ?thesis using qr QR by auto
qed

context poly_mod
begin

definition "pdivmod2 f g = (if Mp g = 0 then (0, f)
 else let ilc = inverse_p m ((lead_coeff (Mp g))); 
      h = Polynomial.smult ilc (Mp g); (q, r) = pseudo_divmod (Mp f) (Mp h) 
      in (Polynomial.smult ilc q, r))"
end

context poly_mod_prime_type
begin

lemma dvdm_iff_pdivmod0:
  assumes f: "(F :: 'a mod_ring poly) = of_int_poly f"
  and g: "(G :: 'a mod_ring poly) = of_int_poly g"
  shows "g dvdm f = (snd (pdivmod F G) = 0)"
proof -  
  have [transfer_rule]: "MP_Rel f F" unfolding MP_Rel_def
    by (simp add: Mp_f_representative f)  
  have [transfer_rule]: "MP_Rel g G" unfolding MP_Rel_def
    by (simp add: Mp_f_representative g)  
  have "(snd (pdivmod F G) = 0) = (G dvd F)"
    unfolding dvd_eq_mod_eq_0 by auto
  from this [untransferred] show ?thesis by simp
qed

lemma of_int_poly_Mp_0[simp]: "(of_int_poly (Mp a) = (0:: 'a mod_ring poly)) = (Mp a = 0)"
  by (auto, metis Mp_f_representative map_poly_0 poly_mod.Mp_Mp)

lemma uniqueness_algorithm_division_of_int_poly:
  assumes g0: "Mp g  0"
  and f: "(F :: 'a mod_ring poly) = of_int_poly f"
  and g: "(G :: 'a mod_ring poly) = of_int_poly g"
  and F: "F = G * Q + R"
  and R: "R = 0  degree R < degree G"
  and Mp_f: "Mp f = Mp g * q + r"
  and r: "r = 0  degree r < degree (Mp g)"
shows "Q = of_int_poly q  R = of_int_poly r"
proof (rule uniqueness_algorithm_division_poly[OF F _ _ R])
  have f': "Mp f = to_int_poly F" unfolding f 
    by (simp add: Mp_f_representative)
  have g': "Mp g = to_int_poly G" unfolding g
    by (simp add: Mp_f_representative)
  have f'': "of_int_poly (Mp f) = F"
    by (metis (no_types, lifting) Dp_Mp_eq Mp_f_representative 
        Mp_smult_m_0 add_cancel_left_right f map_poly_zero of_int_hom.map_poly_hom_add 
        to_int_mod_ring_hom.hom_zero to_int_mod_ring_hom.injectivity)
  have g'': "of_int_poly (Mp g) = G"
    by (metis (no_types, lifting) Dp_Mp_eq Mp_f_representative 
        Mp_smult_m_0 add_cancel_left_right g map_poly_zero of_int_hom.map_poly_hom_add 
        to_int_mod_ring_hom.hom_zero to_int_mod_ring_hom.injectivity)
  have "F = of_int_poly (Mp g * q + r)" using Mp_f  f'' by auto
  also have "... = G * of_int_poly q + of_int_poly r"
    by (simp add: g'' of_int_poly_hom.hom_add of_int_poly_hom.hom_mult)
  finally show "F = G * of_int_poly q + of_int_poly r" .    
  show "of_int_poly r = 0  degree (of_int_poly r::'a mod_ring poly) < degree G"
  proof (cases "r = 0")
    case True
    hence "of_int_poly r = 0" by auto
    then show ?thesis by auto
  next
    case False
    have "degree (of_int_poly r::'a mod_ring poly)  degree (r)" 
    by (simp add: degree_map_poly_le)
    also have "... < degree (Mp g)" using r False by auto
    also have "... = degree G" by (simp add: g')    
    finally show ?thesis by auto
  qed
  show "G  0" using g0 unfolding g''[symmetric] by simp    
qed

corollary uniqueness_algorithm_division_to_int_poly:
  assumes g0: "Mp g  0"
  and f: "(F :: 'a mod_ring poly) = of_int_poly f"
  and g: "(G :: 'a mod_ring poly) = of_int_poly g"
  and F: "F = G * Q + R"
  and R: "R = 0  degree R < degree G"
  and Mp_f: "Mp f = Mp g * q + r"
  and r: "r = 0  degree r < degree (Mp g)"
  shows "Mp q = to_int_poly Q  Mp r = to_int_poly R"
  using uniqueness_algorithm_division_of_int_poly[OF assms]
  by (auto simp add: Mp_f_representative)

lemma uniqueness_algorithm_division_Mp_Rel: 
  assumes monic_Mpg: "monic (Mp g)"
    and f: "(F :: 'a mod_ring poly) = of_int_poly f"
  and g: "(G :: 'a mod_ring poly) = of_int_poly g"
  and qr: "pseudo_divmod (Mp f) (Mp g) = (q,r)"
  and QR: "pseudo_divmod F G = (Q,R)"
shows "MP_Rel q Q  MP_Rel r R "
proof (unfold MP_Rel_def, rule uniqueness_algorithm_division_to_int_poly[OF _ f g])
  show f_gq_r: "Mp f = Mp g * q + r" 
    by (rule pdivmod_monic(1)[OF monic_Mpg], simp add: pdivmod_monic_pseudo_divmod qr monic_Mpg)
  have monic_G: "monic G" using monic_Mpg
    using Mp_f_representative g by auto
  show "F = G * Q + R" 
    by (rule pdivmod_monic(1)[OF monic_G], simp add: pdivmod_monic_pseudo_divmod QR monic_G)
  show "Mp g  0" using monic_Mpg by auto
  show "R = 0  degree R < degree G"
    by (rule pdivmod_monic(2)[OF monic_G], 
        auto simp add: pdivmod_monic_pseudo_divmod monic_G intro: QR)
  show "r = 0  degree r < degree (Mp g)"
    by (rule pdivmod_monic(2)[OF monic_Mpg], 
        auto simp add: pdivmod_monic_pseudo_divmod monic_Mpg intro: qr)
qed

definition "MP_Rel_Pair A B  (let (a,b) = A; (c,d) = B in MP_Rel a c  MP_Rel b d)"

lemma pdivmod2_rel[transfer_rule]: 
  "(MP_Rel ===> MP_Rel ===> MP_Rel_Pair) (pdivmod2) (pdivmod)"
proof (auto simp add: rel_fun_def MP_Rel_Pair_def)
  interpret pm: prime_field m 
    using m unfolding prime_field_def mod_ring_locale_def by auto
  have p: "prime_field TYPE('a) m" 
    using m unfolding prime_field_def mod_ring_locale_def by auto
  fix f F g G a b 
  assume 1[transfer_rule]: "MP_Rel f F" 
     and 2[transfer_rule]: "MP_Rel g G" 
     and 3: "pdivmod2 f g = (a, b)"
  have "MP_Rel a (F div G)  MP_Rel b (F mod G)"
  proof (cases "Mp g  0")
    case True note Mp_g = True    
    have G: "G  0" using Mp_g 2 unfolding MP_Rel_def by auto
    have gG[transfer_rule]: "pm.mod_ring_rel (lead_coeff (Mp g)) (lead_coeff G)" 
      using 2 
      unfolding pm.mod_ring_rel_def MP_Rel_def
      by auto  
    have [transfer_rule]: "(pm.mod_ring_rel ===> pm.mod_ring_rel) (inverse_p m) inverse"
      by (rule prime_field.mod_ring_inverse[OF p])
    hence rel_inverse_p[transfer_rule]: 
      "pm.mod_ring_rel (inverse_p m ((lead_coeff (Mp g)))) (inverse (lead_coeff G))" 
      using gG unfolding rel_fun_def by auto
    let ?h= "(Polynomial.smult (inverse_p m (lead_coeff (Mp g))) g)"
    define h where h: "h = Polynomial.smult (inverse_p m (lead_coeff (Mp g))) (Mp g)"
    define H where H: "H = Polynomial.smult (inverse (lead_coeff G)) G"
    have hH': "MP_Rel ?h H" unfolding MP_Rel_def unfolding H 
      by (metis (mono_tags, hide_lams) "2" MP_Rel_def M_to_int_mod_ring Mp_f_representative 
         rel_inverse_p functional_relation left_total_MP_Rel of_int_hom.map_poly_hom_smult 
         pm.mod_ring_rel_def right_unique_MP_Rel to_int_mod_ring_hom.injectivity to_int_mod_ring_of_int_M)
     have "Mp (Polynomial.smult (inverse_p m (lead_coeff (Mp g))) g) 
      = Mp (Polynomial.smult (inverse_p m (lead_coeff (Mp g))) (Mp g))" by simp
    hence hH: "MP_Rel h H" using hH' h unfolding MP_Rel_def by auto   
    obtain q x where pseudo_fh: "pseudo_divmod (Mp f) (Mp h) = (q, x)" by (meson surj_pair)  
    hence lc_G: "(lead_coeff G)  0" using G by auto
    have a: "a = Polynomial.smult (inverse_p m ((lead_coeff (Mp g)))) q" 
      using 3 pseudo_fh Mp_g 
      unfolding pdivmod2_def Let_def h by auto
    have b: "b = x" using 3 pseudo_fh Mp_g 
      unfolding pdivmod2_def Let_def h by auto  
    have Mp_Rel_FH: "MP_Rel q (F div H)  MP_Rel x (F mod H)"
    proof (rule uniqueness_algorithm_division_Mp_Rel)
      show "monic (Mp h)" 
      proof -        
        have aux: "(inverse_p m (lead_coeff (Mp g))) = to_int_mod_ring (inverse (lead_coeff G))"
          using rel_inverse_p unfolding pm.mod_ring_rel_def by auto
        hence "M (inverse_p m (M (poly.coeff g (degree (Mp g))))) 
          = to_int_mod_ring (inverse (lead_coeff G))"
          by (simp add: M_to_int_mod_ring Mp_coeff)  
        thus ?thesis unfolding h unfolding Mp_coeff by auto
          (metis (no_types, lifting) "2" H MP_Rel_def Mp_coeff aux degree_smult_eq gG hH' 
          inverse_zero_imp_zero lc_G left_inverse pm.mod_ring_rel_def to_int_mod_ring_hom.degree_map_poly_hom
          to_int_mod_ring_hom.hom_one to_int_mod_ring_times)
      qed
      hence monic_H: "monic H" using hH H lc_G by auto
      show f: "F = of_int_poly f" 
        using 1 unfolding MP_Rel_def
        by (simp add: Mp_f_representative poly_eq_iff)
      have "pdivmod F H = pdivmod_monic F H" 
        by (rule pdivmod_eq_pdivmod_monic[OF monic_H])
      also have "... = pseudo_divmod F H" 
        by (rule pdivmod_monic_pseudo_divmod[OF monic_H])
      finally show "pseudo_divmod F H = (F div H, F mod H)" by simp
      show "H = of_int_poly h"
        by (meson MP_Rel_def Mp_f_representative hH right_unique_MP_Rel right_unique_def)
      show "pseudo_divmod (Mp f) (Mp h) = (q, x)" by (rule pseudo_fh)
    qed
    hence Mp_Rel_F_div_H: "MP_Rel q (F div H)" and Mp_Rel_F_mod_H: "MP_Rel x (F mod H)" by auto  
    have "F div H = Polynomial.smult (lead_coeff G) (F div G)" 
      unfolding H using div_smult_right[OF lc_G] inverse_inverse_eq
      by (metis div_smult_right inverse_zero)
    hence F_div_G: "(F div G) = Polynomial.smult (inverse (lead_coeff G)) (F div H)"
      using lc_G by auto
    have "MP_Rel a (F div G)" 
    proof -
      have "of_int_poly (Polynomial.smult (inverse_p m ((lead_coeff (Mp g)))) q) 
        = smult (inverse (lead_coeff G)) (F div H)" 
        by (metis (mono_tags) MP_Rel_def M_to_int_mod_ring Mp_Rel_F_div_H Mp_f_representative 
            of_int_hom.map_poly_hom_smult pm.mod_ring_rel_def rel_inverse_p right_unique_MP_Rel 
            right_unique_def to_int_mod_ring_hom.injectivity to_int_mod_ring_of_int_M)
      thus ?thesis 
      using Mp_Rel_F_div_H
      unfolding MP_Rel_def a F_div_G Mp_f_representative by auto
    qed
    moreover have "MP_Rel b (F mod G)" 
      using Mp_Rel_F_mod_H b H inverse_zero_imp_zero lc_G    
      by (metis mod_smult_right)
    ultimately show ?thesis by auto
  next
    assume Mp_g_0: "¬ Mp g  0"
    hence "pdivmod2 f g = (0, f)" unfolding pdivmod2_def by auto
    hence a: "a = 0" and b: "b = f" using 3 by auto
    have G0: "G = 0" using Mp_g_0 2 unfolding MP_Rel_def by auto
    have "MP_Rel a (F div G)" unfolding MP_Rel_def G0 a by auto
    moreover have "MP_Rel b (F mod G)" using 1 unfolding MP_Rel_def G0 a b by auto
    ultimately show ?thesis by simp
  qed
  thus "MP_Rel a (F div G)" and "MP_Rel b (F mod G)" by auto
qed

subsection ‹Executable division operation modulo $m$ for polynomials›

lemma dvdm_iff_Mp_pdivmod2:
  shows "g dvdm f = (Mp (snd (pdivmod2 f g)) = 0)"  
proof -  
  let ?F="(of_int_poly f)::'a mod_ring poly"
  let ?G="(of_int_poly g)::'a mod_ring poly"
  have a[transfer_rule]: "MP_Rel f ?F"
    by (simp add: MP_Rel_def Mp_f_representative)
  have b[transfer_rule]: "MP_Rel g ?G" 
    by (simp add: MP_Rel_def Mp_f_representative)
  have "MP_Rel_Pair (pdivmod2 f g) (pdivmod ?F ?G)" 
    using pdivmod2_rel unfolding rel_fun_def using a b by auto
  hence "MP_Rel (snd (pdivmod2 f g)) (snd (pdivmod ?F ?G))" 
    unfolding MP_Rel_Pair_def by auto
  hence "(Mp (snd (pdivmod2 f g)) = 0) = (snd (pdivmod ?F ?G) = 0)" 
    unfolding MP_Rel_def by auto
  thus ?thesis using dvdm_iff_pdivmod0 by auto
qed
   
end

lemmas (in poly_mod_prime) dvdm_pdivmod = poly_mod_prime_type.dvdm_iff_Mp_pdivmod2
  [unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, 
   unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty]

lemma (in poly_mod) dvdm_code:
   "g dvdm f = (if prime m then Mp (snd (pdivmod2 f g)) = 0 
    else Code.abort (STR ''dvdm error: m is not a prime number'') (λ _. g dvdm f))"
  using poly_mod_prime.dvdm_pdivmod[unfolded poly_mod_prime_def]
  by auto

declare poly_mod.pdivmod2_def[code]
declare poly_mod.dvdm_code[code]

end

Theory LLL_Factorization_Impl

(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹The LLL factorization algorithm›

text ‹This theory contains an implementation of a polynomial time factorization algorithm. 
  It first constructs a modular factorization. Afterwards it recursively 
  invokes the LLL basis reduction algorithm on one lattice to either split a polynomial into  
  two non-trivial factors, or to deduce irreducibility.›

theory LLL_Factorization_Impl
  imports LLL_Basis_Reduction.LLL_Certification
    Factor_Bound_2
    Missing_Dvd_Int_Poly
    Berlekamp_Zassenhaus.Berlekamp_Zassenhaus
begin

hide_const (open) up_ring.coeff up_ring.monom
  Unique_Factorization.factors Divisibility.factors
  Unique_Factorization.factor Divisibility.factor 
  Divisibility.prime

(*
  Implementation of a polynomial-time factoring algorithm for ℤ[X], based on the book 
  "Modern Computer Algebra", second edition, pages 477-480.
*)

(*The following function obtains the generators of the lattice L ⊆ Z^j
 - L = {ux^i: 0≤i≤j-d}∪{mx^i: 0≤i≤d}
 - d = degree u.
 - We have to complete with zeroes up to dimension j
*)
definition factorization_lattice where "factorization_lattice u k m 
    map (λi. vec_of_poly_n (u * monom 1 i) (degree u + k)) [k>..0] @
    map (λi. vec_of_poly_n (monom m i) (degree u + k)) [degree u >..0]"

fun min_degree_poly :: "int poly  int poly  int poly"
  where "min_degree_poly a b = (if degree a  degree b then a else b)"

fun choose_u :: "int poly list  int poly"
  where "choose_u [] = undefined"
  | "choose_u [gi] = gi" 
  | "choose_u (gi # gj # gs) = min_degree_poly gi (choose_u (gj # gs))"

lemma factorization_lattice_code[code]: "factorization_lattice u k m = (
  let n = degree u in
 map 
  (λi. vec_of_poly_n (monom_mult i u) (n+k)) [k>..0] 
  @ map (λi. vec_of_poly_n (monom m i) (n+k)) [n>..0]
)" unfolding factorization_lattice_def monom_mult_def
  by (auto simp: ac_simps Let_def)

text ‹Optimization: directly try to minimize coefficients of polynomial $u$.›
definition LLL_short_polynomial where
  "LLL_short_polynomial pl n u = poly_of_vec (short_vector_hybrid 2 (factorization_lattice 
     (poly_mod.inv_Mp pl (poly_mod.Mp pl u)) (n - degree u) pl))" 

locale LLL_implementation =
  fixes p pl :: int
begin

function LLL_many_reconstruction where 
  "LLL_many_reconstruction f us = (let 
     d = degree f;
     d2 = d div 2;
     f2_opt = find_map_filter 
        (λ u. gcd f (LLL_short_polynomial pl (Suc d2) u)) 
        (λ f2. let deg = degree f2 in deg > 0  deg < d)
        (filter (λ u. degree u  d2) us)
    in case f2_opt of None  [f] 
    | Some f2  let f1 = f div f2;
       (us1, us2) = List.partition (λ gi. poly_mod.dvdm p gi f1) us
       in LLL_many_reconstruction f1 us1 @ LLL_many_reconstruction f2 us2)"
  by pat_completeness auto

termination
proof (relation "measure (λ (f,us). degree f)", goal_cases)
  case (3 f us d d2 f2_opt f2 f1 pair us1 us2)
  from find_map_filter_Some[OF 3(4)[unfolded 3(3) Let_def]] 3(1,5)
  show ?case by auto
next
  case (2 f us d d2 f2_opt f2 f1 pair us1 us2)
  from find_map_filter_Some[OF 2(4)[unfolded 2(3) Let_def]] 2(1,5)
  have f: "f = f1 * f2" and f0: "f  0" 
    and deg: "degree f2 > 0" "degree f2 < degree f" by auto
  have "degree f = degree f1 + degree f2" using f0 unfolding f
    by (subst degree_mult_eq, auto)
  with deg show ?case by auto
qed auto

function LLL_reconstruction where 
  "LLL_reconstruction f us = (let 
     d = degree f;
     u = choose_u us;
     g = LLL_short_polynomial pl d u;
     f2 = gcd f g;
     deg = degree f2
    in if deg = 0  deg  d then [f] 
      else let f1 = f div f2;
       (us1, us2) = List.partition (λ gi. poly_mod.dvdm p gi f1) us
       in LLL_reconstruction f1 us1 @ LLL_reconstruction f2 us2)"
  by pat_completeness auto

termination
proof (relation "measure (λ (f,us). degree f)", goal_cases)
  case (2 f us d u g f2 deg f1 pair us1 us2)
  hence f: "f = f1 * f2" and f0: "f  0" by auto
  have deg: "degree f = degree f1 + degree f2" using f0 unfolding f
    by (subst degree_mult_eq, auto)
  from 2 have "degree f2 > 0" "degree f2 < degree f" by auto
  thus ?case using deg by auto
qed auto
end

declare LLL_implementation.LLL_reconstruction.simps[code]
declare LLL_implementation.LLL_many_reconstruction.simps[code]

definition LLL_factorization :: "int poly  int poly list" where
  "LLL_factorization f = (let 
     ― ‹find suitable prime›
     p = suitable_prime_bz f;
     ― ‹compute finite field factorization›
     (_, fs) = finite_field_factorization_int p f;
     ― ‹determine exponent l and B›
     n = degree f;
     no = f2;
     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 = f2;
     B = sqrt_int_ceiling (2^(5 * (n div 2) * (n div 2)) * no^(2 * (n div 2)));
     l = find_exponent p B;
     ― ‹perform hensel lifting to lift factorization to mod $p^l$›
     us = hensel_lifting p l f fs;
     ― ‹reconstruct integer factors via LLL algorithm›
     pl = p^l
   in LLL_implementation.LLL_many_reconstruction p pl f us)"

end

Theory LLL_Factorization

(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Correctness of the LLL factorization algorithm›

text ‹This theory connects short vectors of lattices and factors of polynomials. 
  From this connection, we derive soundness of the lattice based factorization algorithm. 
› 

theory LLL_Factorization
  imports
    LLL_Factorization_Impl  
    Berlekamp_Zassenhaus.Factorize_Int_Poly
begin

subsection ‹Basic facts about the auxiliary functions›
hide_const (open) module.smult

lemma nth_factorization_lattice:
  fixes u and d
  defines "n  degree u"
  assumes "i < n + d"
  shows "factorization_lattice u d m ! i =
    vec_of_poly_n (if i < d then u * monom 1 (d - Suc i) else monom m (n+d-Suc i)) (n+d)"
  using assms
  by (unfold factorization_lattice_def, auto simp: nth_append smult_monom Let_def not_less)

lemma length_factorization_lattice[simp]: 
  shows "length (factorization_lattice u d m) = degree u + d"
  by (auto simp: factorization_lattice_def Let_def)

lemma dim_factorization_lattice:
  assumes "x < degree u + d" 
  shows "dim_vec (factorization_lattice u d m ! x) = degree u + d"
  unfolding factorization_lattice_def using assms nth_append
  by (simp add: nth_append Let_def)

lemma dim_factorization_lattice_element: 
  assumes "x  set (factorization_lattice u d m)" shows "dim_vec x = degree u + d" 
  using assms by (auto simp: factorization_lattice_def Let_def)

lemma set_factorization_lattice_in_carrier[simp]: "set (factorization_lattice u d m)  carrier_vec (degree u + d)" 
  using dim_factorization_lattice by (auto simp: factorization_lattice_def Let_def) 

lemma choose_u_Cons: "choose_u (x#xs) = 
  (if xs = [] then x else min_degree_poly x (choose_u xs))"
  by (cases xs, auto)

lemma choose_u_member: "xs  []  choose_u xs  set xs"
  by (induct xs, auto simp: choose_u_Cons)

declare choose_u.simps[simp del]


subsection ‹Facts about Sylvester matrices and norms›

lemma (in LLL) lattice_is_span [simp]: "lattice_of xs = span_list xs"
  by (unfold lattice_of_def span_list_def lincomb_list_def image_def, auto)

lemma sq_norm_row_sylvester_mat1:
  fixes f g :: "'a :: conjugatable_ring poly"
  assumes i: "i < degree g"
  shows "(row (sylvester_mat f g) i)2 = f2"
proof (cases "f = 0")
  case True
  thus ?thesis
    by (auto simp add: sylvester_mat_def row_def sq_norm_vec_def o_def
        interv_sum_list_conv_sum_set_nat i intro!: sum_list_zero)
next
  case False note f = False         
  let ?f = "λj. if i  j  j - i  degree f then coeff f (degree f + i - j) else 0"
  let ?h = "λj. j + i"
  let ?row = "vec (degree f + degree g) ?f "
  let ?g = "λj. degree f - j"
  have image_g: "?g ` {0..<Suc (degree f)} = {0..<Suc (degree f)}" 
    by (auto simp add: image_def) 
       (metis (no_types, hide_lams) Nat.add_diff_assoc add.commute add_diff_cancel_left' 
        atLeastLessThan_iff diff_Suc_Suc diff_Suc_less less_Suc_eq_le zero_le)
  have bij_h: "bij_betw ?h {0..<Suc (degree f)} {i..< Suc (degree f + i)}"
    unfolding bij_betw_def image_def
    by (auto, metis atLeastLessThan_iff le_add_diff_inverse2 
        less_diff_conv linorder_not_less not_less_eq zero_order(3))
  have "row (sylvester_mat f g) i2 = ?row2" 
    by (rule arg_cong[of _ _ "sq_norm_vec"], insert i, 
        auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def)
  also have "... = sum_list (map (sq_norm  ?f) [0..<degree f + degree g])" 
    unfolding sq_norm_vec_def by auto
  also have "... = sum (sq_norm  ?f) {0..<degree f + degree g}"
    unfolding interv_sum_list_conv_sum_set_nat by auto
  also have "... = sum (sq_norm  ?f) {i..< Suc (degree f + i)}" 
    by (rule sum.mono_neutral_right, insert i, auto)
  also have "... = sum ((sq_norm  ?f)  ?h) {0..<Suc (degree f)}" 
    by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h])
  also have "... = sum (λj. sq_norm (coeff f (degree f - j))) {0..<Suc (degree f)}" 
    by (rule sum.cong, auto)
  also have "... = sum ((λj. sq_norm (coeff f j))  ?g) {0..<Suc (degree f)}" 
    unfolding o_def ..  
  also have "... = sum (λj. sq_norm (coeff f j)) (?g ` {0..<Suc (degree f)})"
    by (rule sum.reindex[symmetric], auto simp add: inj_on_def)
  also have "... = sum (sq_norm  coeff f) {0..<Suc (degree f)}" unfolding image_g by simp
  also have "... = sum_list (map sq_norm (coeffs f))" 
     unfolding coeffs_def using f 
     by (simp add: interv_sum_list_conv_sum_set_nat)
  finally show ?thesis unfolding sq_norm_poly_def by auto
qed


lemma sq_norm_row_sylvester_mat2:
  fixes f g :: "'a :: conjugatable_ring poly"
  assumes i1: "degree g  i" and i2: "i < degree f + degree g"
  shows "row (sylvester_mat f g) i2 = g2"
proof -
  let ?f = "λj. if i - degree g  j  j  i then coeff g (i - j) else 0"
  let ?row = "vec (degree f + degree g) ?f"
  let ?h = "λj. j + i - degree g"
  let ?g = "λj. degree g - j"
  have image_g: "?g ` {0..<Suc (degree g)} = {0..<Suc (degree g)}" 
    by (auto simp add: image_def)
       (metis atLeastLessThan_iff diff_diff_cancel diff_le_self less_Suc_eq_le zero_le)
  have x: "x - (i - degree g)  degree g" if x: "x < Suc i" for x using x by auto
  have bij_h: "bij_betw ?h {0..<Suc (degree g)} {i - degree g..<Suc i}" 
    unfolding bij_betw_def inj_on_def using i1 i2 unfolding image_def
    by (auto, metis (no_types) Nat.add_diff_assoc atLeastLessThan_iff x less_Suc_eq_le 
        less_eq_nat.simps(1) ordered_cancel_comm_monoid_diff_class.diff_add)  
  have "row (sylvester_mat f g) i2 = ?row2" 
    by (rule arg_cong[of _ _ "sq_norm_vec"], insert i1 i2, 
        auto simp add: row_def sylvester_mat_def sylvester_mat_sub_def)
  also have "... = sum_list (map (sq_norm  ?f) [0..<degree f + degree g])" 
    unfolding sq_norm_vec_def by auto
  also have "... = sum (sq_norm  ?f) {0..<degree f + degree g}"
    unfolding interv_sum_list_conv_sum_set_nat by auto
  also have "... = sum (sq_norm  ?f) {i - degree g..< Suc i}" 
    by (rule sum.mono_neutral_right, insert i2, auto)
  also have "... = sum ((sq_norm  ?f)  ?h) {0..<Suc (degree g)}"
    by (unfold o_def, rule sum.reindex_bij_betw[symmetric, OF bij_h])
  also have "... = sum (λj. sq_norm (coeff g (degree g - j))) {0..<Suc (degree g)}" 
    by (rule sum.cong, insert i1, auto)
  also have "... = sum ((λj. sq_norm (coeff g j))  ?g) {0..<Suc (degree g)}" 
    unfolding o_def ..  
  also have "... = sum (λj. sq_norm (coeff g j)) (?g ` {0..<Suc (degree g)})"
    by (rule sum.reindex[symmetric], auto simp add: inj_on_def)
  also have "... = sum (sq_norm  coeff g) {0..<Suc (degree g)}" unfolding image_g by simp
  also have "... = sum_list (map sq_norm (coeffs g))" 
     unfolding coeffs_def
     by (simp add: interv_sum_list_conv_sum_set_nat)
  finally show ?thesis unfolding sq_norm_poly_def by auto
qed

lemma Hadamard's_inequality_int:
  fixes A::"int mat"
  assumes A: "A  carrier_mat n n" 
  shows "¦det A¦  sqrt (of_int (prod_list (map sq_norm (rows A))))"
proof -
  let ?A = "map_mat real_of_int A" 
  have "¦det A¦ = ¦det ?A¦" unfolding of_int_hom.hom_det by simp
  also have "  sqrt (prod_list (map sq_norm (rows ?A)))" 
    by (rule Hadamard's_inequality[of ?A n], insert A, auto)
  also have " = sqrt (of_int (prod_list (map sq_norm (rows A))))" unfolding of_int_hom.hom_prod_list map_map
    by (rule arg_cong[of _ _ "λ x. sqrt (prod_list x)"], rule nth_equalityI, force, 
      auto simp: sq_norm_of_int[symmetric] row_def intro!: arg_cong[of _ _ sq_norm_vec])
  finally show ?thesis .
qed

lemma resultant_le_prod_sq_norm:
  fixes f g::"int poly"
  defines "n  degree f" and "k  degree g"
  shows "¦resultant f g¦  sqrt (of_int (f2^k * g2^n))"
proof -
  let ?S = "sylvester_mat f g"
  let ?f = "sq_norm  row ?S"
  have map_rw1: "map ?f [0..<degree g] = replicate k f2"
  proof (rule nth_equalityI)
    let ?M = "map (sq_norm  row (sylvester_mat f g)) [0..<degree g]"
    show "length ?M = length (replicate k f2)" using k_def by auto
    show "?M ! i = replicate k f2 ! 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 f2 ! i = f2" 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 f2 ! i" ..
    qed
  qed    
  have map_rw2: "map ?f [degree g..<degree f + degree g] = replicate n g2"
  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 g2)" by (simp add: n_def)
    show "?M ! i = replicate n g2 ! 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 g2 ! i = g2" by (rule nth_replicate[OF i_n])
      also have "... = (sq_norm  row (sylvester_mat f g)) (degree g + i)"
        using i_n n_def
        by (simp add: sq_norm_row_sylvester_mat2)
      also have "... = ?M ! i"
        by (simp add: i_deg_f)
      finally show "?M ! i = replicate n g2 ! i" ..
    qed
  qed
  have p1: "prod_list (map ?f [0..<degree g]) = f2^k"
    unfolding map_rw1 by (rule prod_list_replicate)
  have p2: "prod_list (map ?f [degree g..<degree f + degree g]) = g2^n"
    unfolding map_rw2 by (rule prod_list_replicate)
  have list_rw: "[0..<degree f + degree g] = [0..<degree g] @ [degree g..<degree f + degree g]"
    by (metis add.commute upt_add_eq_append zero_le)
  have "¦resultant f g¦ = ¦det ?S¦"  unfolding resultant_def ..
  also have "...  sqrt (of_int (prod_list (map sq_norm (rows ?S))))"
    by (rule Hadamard's_inequality_int, auto)
  also have "map sq_norm (rows ?S) = map ?f [0..<degree f + degree g]"
    unfolding Matrix.rows_def by auto
  also have "... =  map ?f ([0..<degree g] @ [degree g..<degree f + degree g])"
    by (simp add: list_rw)
  also have "prod_list ... = prod_list (map ?f [0..<degree g])
    * prod_list (map ?f [degree g..<degree f + degree g])" by auto
  finally show ?thesis unfolding p1 p2 .
qed

subsection ‹Proof of the key lemma 16.20›
(* Lemma 16.20 *)
lemma common_factor_via_short:
  fixes f g u :: "int poly"
  defines "n  degree f" and "k  degree g"
  assumes n0: "n > 0" and k0: "k > 0"
      and monic: "monic u" and deg_u: "degree u > 0"
      and uf: "poly_mod.dvdm m u f" and ug: "poly_mod.dvdm m u g"
      and short: "f2^k * g2^n < m2" 
      and m: "m  0"
    shows "degree (gcd f g) > 0"
proof -
  interpret poly_mod m .
  have f_not0: "f  0" and g_not0: "g  0"
    using n0 k0 k_def n_def by auto
  have deg_f: "degree f > 0" using n0 n_def by simp
  have deg_g: "degree g > 0" using k0 k_def by simp
  obtain s t where deg_s: "degree s < degree g" and deg_t: "degree t < degree f" 
    and res_eq: "[:resultant f g:] = s * f + t * g" and s_not0: "s  0" and t_not0: "t  0"
    using resultant_as_nonzero_poly[OF deg_f deg_g] by auto
  have res_eq_modulo: "[:resultant f g:] =m s * f + t * g" using res_eq
    by simp 
  have u_dvdm_res: "u dvdm [:resultant f g:]"
  proof (unfold res_eq, rule dvdm_add)
    show "u dvdm s * f"
      using dvdm_factor[OF uf, of s]
      unfolding mult.commute[of f s] by auto
    show "u dvdm t * g"
      using dvdm_factor[OF ug, of t] 
      unfolding mult.commute[of g t] by auto    
  qed
  have res_0_mod: "resultant f g mod m = 0"
    by (rule monic_dvdm_constant[OF u_dvdm_res monic deg_u])
  have res0: "resultant f g = 0"
  proof (rule mod_0_abs_less_imp_0)
    show "[resultant f g = 0] (mod m)" using res_0_mod unfolding cong_def by auto
    have "¦resultant f g¦  sqrt ((sq_norm_poly f)^k * (sq_norm_poly g)^n)" 
      unfolding k_def n_def
      by (rule resultant_le_prod_sq_norm)
    also have "... < m"
    proof (rule real_less_lsqrt)
      show "0  real_of_int (f2 ^ k * g2 ^ n)"
        by (simp add: sq_norm_poly_ge_0)
      show "0  real_of_int m" using m by simp
      show "real_of_int (f2 ^ k * g2 ^ 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: "dn"
    and u: "u0" 
    and m0: "k0"
    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 "dn"
    and "u0" 
    and "k0"
    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 = ?ST *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: "k0"
      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 "q0" thus "q' + smult k q''  0" unfolding q .
    show "k  0" by fact
    show "degree u = d" using d_def by auto
  qed
  have g2: "(vec_of_poly_n (q*u) n) + (vec_of_poly_n (smult k r) n) = g" 
  proof -
    have "g = vec_of_poly_n (poly_of_vec g) n"
      by (rule vec_of_poly_n_poly_of_vec[symmetric], auto simp add: dim_g)
    also have " = vec_of_poly_n ((q' + smult k q'') * u + smult k r'') n" 
      using g1 by auto
    also have "... = vec_of_poly_n (q * u + smult k r'') n" unfolding q by auto
    also have "... = vec_of_poly_n (q * u) n + vec_of_poly_n (smult k r'') n"
      by (rule vec_of_poly_n_add)
    finally show ?thesis unfolding r by simp
  qed
  let ?c = "λi. if i < n - d then coeff q  (n - d - 1 - i) else coeff r (n - Suc i)"
  let ?c1 = "λi. ?c i v factorization_lattice u (n-d) k ! i"
  show ?thesis
  proof (rule exI[of _ ?c]) 
    let ?part1 = "map (λi. vec_of_poly_n (u * monom 1 i) n) [n-d>..0]"  
    let ?part2 = "map (λi. vec_of_poly_n (monom k i) n) [d>..0]"
    have [simp]: "dim_vec (M.sumlist (map ?c1 [0..<n - d])) = n" 
      by (rule dim_sumlist, auto simp add: dim_factorization_lattice d_def)
    have [simp]: "dim_vec (M.sumlist (map ?c1 [n-d..<n])) = n"
      by (rule dim_sumlist, insert d, auto simp add: dim_factorization_lattice d_def)
    have [simp]: "factorization_lattice u (n-d) k ! x  carrier_vec n" if x: "x < n" for x 
      using x dim_factorization_lattice_element nth_factorization_lattice[of x u "n-d"] d
      by (auto simp: d_def)
    have "[0..<length (factorization_lattice u (n-d) k)] = [0..<n]"
      using d by (simp add: d_def less_imp_le_nat)
    also have "... = [0..<n - d] @ [n-d..<n]"
      by (rule upt_minus_eq_append, auto)
    finally have list_rw: "[0..<length (factorization_lattice u (n-d) k)] = [0..<n - d] @ [n-d..<n]" . 
    have qu1: "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = q*u" 
    proof -
      have "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = poly_of_vec (Vi{0..<n-d}. ?c1 i)" 
        by (subst sumlist_map_as_finsum, auto)
      also have "... = poly_of_vec (Viset [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 (Vi{n-d..<n}. ?c1 i)" 
        by (subst sumlist_map_as_finsum, auto)
      also have "... = poly_of_vec (Viset [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-di" and i2: "i<n" for i 
          using degree_monom_le i i2
          by (simp add: degree_monom_eq k_not0)
        have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (monom k (n - Suc i)) n" 
          if i: "n - d  i" and i2: "i<n" for i
          using i2 i d d_def
          by (subst nth_factorization_lattice, auto)
        have r_rw: "r = (i  {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))"
        proof (auto simp add: poly_eq_iff coeff_sum)
          fix j
          show "coeff r j = (i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0)"
          proof (cases "j<d")
            case True
            have j_eq: "n - Suc (n - 1 - j) = j" using d True by auto
            let ?i = "n-1-j"
            let ?f ="λi. if n - Suc i = j then coeff r (n - Suc i) else 0"
            have sum0: "sum ?f ({n-d..<n} - {?i}) = 0" by (rule sum.neutral, auto)
            have "{n-d..<n} = insert ?i ({n-d..<n} - {?i})" using True by auto
            hence "sum ?f {n - d..<n} = sum ?f (insert ?i ({n-d..<n} - {?i}))" by auto
            also have "... = ?f ?i + sum ?f ({n-d..<n} - {?i})"
              by (rule sum.insert, auto)
            also have "... = coeff r j" unfolding sum0 j_eq by simp
            finally show ?thesis ..
          next
            case False
            hence "(i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0) = 0"
              by (intro sum.neutral ballI, insert False, simp, linarith) 
            also have "... = coeff r j" 
              by (rule coeff_eq_0[symmetric], insert False deg_r'' r d_def, auto)
            finally show ?thesis ..
          qed 
        qed
        have "sum (λi. poly_of_vec (?c1 i)) {n-d..<n} 
        = (i  {n-d..<n}. poly_of_vec (coeff r (n - Suc i) v factorization_lattice u (n-d) k ! i))"
          by (rule sum.cong, auto)
        also have "...  = (i  {n-d..<n}. (poly_of_vec (coeff r (n - Suc i) 
          v vec_of_poly_n (monom k (n - Suc i)) n)))"
          by (rule sum.cong, auto simp add: lattice_rw)
        also have "... = (i  {n-d..<n}. smult (coeff r (n - Suc i)) (monom k (n - Suc i)))"
          by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg])
        also have "... = (i  {n-d..<n}. smult k (monom (coeff r (n - Suc i)) (n - Suc i)))"
          by (rule sum.cong, auto simp add: smult_monom smult_sum2)
        also have "... = smult k (i  {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))"
          by (simp add: smult_sum2)
        also have "... = smult k r" using r_rw by auto
        finally show ?thesis .
      qed
      finally show ?thesis .
    qed
    have rm: "(M.sumlist (map ?c1 [n-d..<n])) = vec_of_poly_n (smult k r) n"
    proof -
      have "vec_of_poly_n (smult k r) n 
        = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n" 
        using rm1 by auto
      also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n 
        = M.sumlist (map ?c1 [n-d..<n])"
        by (rule vec_of_poly_n_poly_of_vec, auto)
      finally show ?thesis ..        
    qed
    have "lincomb_list ?c (factorization_lattice u (n-d) k) = M.sumlist (map ?c1 ([0..<n - d] @ [n-d..<n]))"
      unfolding lincomb_list_def list_rw by auto
    also have "... = M.sumlist (map ?c1 [0..<n - d] @ map ?c1 [n-d..<n])" by auto
    also have "... = M.sumlist (map ?c1 [0..<n - d]) + M.sumlist (map ?c1 [n-d..<n])" 
      using d by (auto simp add: d_def nth_factorization_lattice intro!: M.sumlist_append)
    also have "... = vec_of_poly_n (q*u) n + vec_of_poly_n (smult k r) n" 
      unfolding qu rm by auto
    also have "... = g" using g2 by simp
    finally show "lincomb_list ?c (factorization_lattice u (n-d) k) = g" .
  qed
qed

text ‹The factorization lattice precisely characterises the polynomials of a certain
  degree which divide $u$ modulo $M$.›

lemma factorization_lattice: fixes M assumes  
  deg_u: "degree u  0"  and M: "M  0" 
shows "degree u  n  n  0  f  poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M)  
  degree f < n  poly_mod.dvdm M u f" 
  "monic u  degree u < n  
  degree f < n  poly_mod.dvdm M u f  f  poly_of_vec ` lattice_of (factorization_lattice u (n - degree u) M)" 
proof -
  from deg_u have deg_u: "degree u > 0" by auto
  let ?L = "factorization_lattice u (n - degree u) M" 
  {
    assume deg: "degree f < n" and dvd: "poly_mod.dvdm M u f" and mon: "monic u" 
      and deg_u_lt: "degree u < n"
    define fv where "fv = vec n (λ i. (coeff f (n - Suc i)))" 
    have f: "f = poly_of_vec fv" unfolding fv_def poly_of_vec_def Let_def using deg 
      by (auto intro!: poly_eqI coeff_eq_0 simp: coeff_sum) 
    have dim_fv: "dim_vec fv = n" unfolding fv_def by simp
    from dvd_modulo_to_lincomb[OF deg_u_lt _ M mon _ deg_u(1), of fv, folded f, OF dvd dim_fv]
    obtain c where gv: "fv = lincomb_list c ?L" by auto
    have "fv  lattice_of ?L" unfolding gv lattice_is_span by (auto simp: in_span_listI)
    thus "f  poly_of_vec ` lattice_of ?L" unfolding f by auto
  }
  moreover
  {
    assume "f  poly_of_vec ` lattice_of ?L" and deg_u: "degree u  n" and n: "n  0" 
    then obtain fv where f: "f = poly_of_vec fv" and fv: "fv  lattice_of ?L" by auto
    from in_span_listE[OF fv[unfolded lattice_is_span]] 
    obtain c where fv: "fv = lincomb_list c ?L" by auto    
    from lincomb_to_dvd_modulo[OF _ fv[symmetric]] deg_u f
    have dvd: "poly_mod.dvdm M u f" by auto
    have "set ?L  carrier_vec n" unfolding factorization_lattice_def using deg_u by auto
    hence "fv  carrier_vec n" unfolding fv by (metis lincomb_list_carrier)
    hence "degree f < n" unfolding f using degree_poly_of_vec_less[of fv n] using n by auto
    with dvd show "degree f < n  poly_mod.dvdm M u f" by auto
  }
qed
end

subsection ‹Soundness of the LLL factorization algorithm›

lemma LLL_short_polynomial: assumes deg_u_0: "degree u  0" and deg_le: "degree u  n" 
  and pl1: "pl > 1" 
  and monic: "monic u" 
shows "degree (LLL_short_polynomial pl n u) < n" 
  and "LLL_short_polynomial pl n u  0"
  and "poly_mod.dvdm pl u (LLL_short_polynomial pl n u)" 
  and "degree u < n  f  0 
    poly_mod.dvdm pl u f  degree f < n  LLL_short_polynomial pl n u2  2 ^ (n - 1) * f2" 
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': "?sv2 = LLL_short_polynomial pl n u2" 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  0v 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: "fv2 = f2" unfolding f by simp
  have fv0: "fv  0v n" using f0 unfolding f by auto
  with fv have fvL: "fv  lattice_of ?L - {0v n}" by auto
  from short(3)[OF this, unfolded norm]
  have "rat_of_int LLL_short_polynomial pl n u2  rat_of_int (2 ^ (n - 1) * f2)" by simp
  thus "LLL_short_polynomial pl n u2  2 ^ (n - 1) * f2" 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)) * F2^(2 * (degree F - 1)) < pl2"
shows "f = prod_list fs  ( fi  set fs. irreducibled fi)" 
proof -
  interpret p: poly_mod_prime p by (standard, rule p)
  interpret pl: poly_mod_2 "pl" by (standard, rule pl1)
  from pl1 plp have l0: "l  0" by (cases l, auto)
  show ?thesis using assms(1-5)
  proof (induct f us arbitrary: fs rule: LLL_reconstruction.induct)
    case (1 f us fs)
    define u where "u = choose_u us" 
    define g where "g = LLL_short_polynomial pl (degree f) u" 
    define k where "k = gcd f g" 
    note res = 1(3)
    note degf = 1(4)
    note uf = 1(5)
    note fF = 1(6)
    note norm = 1(7)
    note to_fact = pl.unique_factorization_m_imp_factorization
    note fact = to_fact[OF uf]
    have mon_gs: "ui  set us  monic ui" for ui using norm fact
      unfolding pl.factorization_m_def by auto
    from p.coprime_lead_coeff_factor[OF p.prime] fF cop 
    have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast
    have plf0: "pl.Mp f  0" 
      using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce
    have "degree f = pl.degree_m f" 
      by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], 
          insert cop p, simp add: l0 p.coprime_exp_mod plp)
    also have " =  sum_mset (image_mset pl.degree_m (mset us))"
      unfolding pl.factorization_m_degree[OF fact plf0] ..
    also have " = sum_list (map pl.degree_m us)" 
      unfolding sum_mset_sum_list[symmetric] by auto
    also have " = sum_list (map degree us)" 
      by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto)
    finally have degf_gs: "degree f = sum_list (map degree us)" by auto
    hence gs: "us  []" using degf by (cases us, auto)
    from choose_u_member[OF gs] have u_gs: "u  set us" unfolding u_def by auto
    from fact u_gs have irred: "pl.irreducibled_m u" unfolding pl.factorization_m_def by auto
    hence deg_u: "degree u  0" unfolding pl.irreducibled_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: "irreducibled f" 
      proof (rule ccontr)
        assume "¬ irreducibled f" 
        from reducibledE[OF this] degf obtain f1 f2 where 
          f: "f = f1 * f2" and
          deg12: "degree f1  0" "degree f2  0" "degree f1 < degree f" "degree f2 < degree f" 
          by (simp, metis)
        from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp]
        obtain us1 us2 where 
          uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)"
            "pl.unique_factorization_m f2 (lead_coeff f2, us2)"
          and gs: "mset us = us1 + us2"
          and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1"
          unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def)
        note norm_u = norm[OF u_gs]
        from u_gs have u_gs': "u ∈# mset us" by auto
        with pl.factorization_m_mem_dvdm[OF fact, of u] 
        have u_f: "pl.dvdm u f" by auto
        from u_gs'[unfolded gs] have "u ∈# us1  u ∈# us2" by auto
        with pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(1)], of u] 
             pl.factorization_m_mem_dvdm[OF to_fact[OF uf12(2)], of u] 
        have "pl.dvdm u f1  pl.dvdm u f2" unfolding norm12 norm_u by auto
        from this have " f1 f2. f = f1 * f2  
          degree f1  0  degree f2  0  degree f1 < degree f  degree f2 < degree f  
          pl.dvdm u f1" 
        proof 
          assume "pl.dvdm u f1" thus ?thesis using f deg12 by auto
        next
          from f have f: "f = f2 * f1" by auto
          assume "pl.dvdm u f2" thus ?thesis using f deg12 by auto
        qed
        then obtain f1 f2 where prod: "f = f1 * f2" 
          and deg: "degree f1  0" "degree f2  0" "degree f1 < degree f" "degree f2 < degree f" 
          and uf1: "pl.dvdm u f1" by auto
        from pl.unique_factorization_m_factor[OF p uf[unfolded prod], folded prod, OF cop sf l0 plp]
        obtain us1 where fact_f1: "pl.unique_factorization_m f1 (lead_coeff f1, us1)" by auto
        have plf1: "pl.Mp f1  0" 
          using to_fact[OF fact_f1] pl.factorization_m_lead_coeff 
            pl.unique_factorization_m_zero fact_f1 by fastforce
        have "degree u  degree f1"
          by (rule pl.dvdm_degree[OF mon_u uf1 plf1])
        with deg have deg_uf: "degree u < degree f" by auto
        have pl0: "pl  0" using pl.m1 plp by linarith
        let ?n = "degree f"
        let ?n1 = "degree f1" 
        let ?d = "degree u" 
        from prod fF have f1F: "f1 dvd F" unfolding dvd_def by auto
        from deg_uf have deg_uf': "?d  ?n" by auto
        from deg have f1_0: "f1  0" by auto
        have ug: "pl.dvdm u g" using short_main(3) unfolding g_def .
        have g0: "g  0" using short_main(2) unfolding g_def .
        have deg_gf: "degree g < degree f" using short_main(1) unfolding g_def .
        let ?N = "degree F" 
        from fF prod have f1F: "f1 dvd F" unfolding dvd_def by auto
        have "g2  2 ^ (?n - 1) * f12" unfolding g_def
          by (rule short_main(4)[OF deg_uf _ uf1], insert deg, auto)
        also have "  2 ^ (?n - 1) * (2 ^ (2 * degree f1) * F2)" 
          by (rule mult_left_mono[OF sq_norm_factor_bound[OF f1F F0]], simp)
        also have " = 2 ^ ((?n - 1) + 2 * degree f1) * F2" 
          unfolding power_add by simp
        also have "  2 ^ ((?n - 1) + 2 * (?n - 1)) * F2" 
          by (rule mult_right_mono, insert deg(3), auto)
        also have " = 2 ^ (3 * (?n - 1)) * F2" by simp
        finally have ineq_g: "g2  2 ^ (3 * (?n - 1)) * F2" .
        from power_mono[OF this, of ?n1]
        have ineq1: "g2 ^ ?n1  (2 ^ (3 * (?n - 1)) * F2)^?n1" by auto
        from F0 have normF: "F2  1" using sq_norm_poly_pos[of F] by presburger
        from g0 have normg: "g2  1" using sq_norm_poly_pos[of g] by presburger
        from f0 have normf: "f2  1" using sq_norm_poly_pos[of f] by presburger
        from f1_0 have normf1: "f12  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: "f12 ^ degree g  (2 ^ (2 * ?n1) * F2) ^ degree g" by auto
        also have "  (2 ^ (2 * ?n1) * F2) ^ (?n - 1)"
          by (rule pow_mono_exp, insert deg_gf normF, auto)          
        finally have ineq2: "f12 ^ degree g  (2 ^ (2 * ?n1) * F2) ^ (?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 "f12 ^ degree g * g2 ^ ?n1  
          (2 ^ (2 * ?n1) * F2) ^ (?n - 1) * (2 ^ (3 * (?n - 1)) * F2)^?n1" 
          by (rule mult_mono[OF ineq2 ineq1], force+)
        also have "  (2 ^ (2 * (?N - 1)) * F2) ^ (?N - 1) *
          (2 ^ (3 * (?N - 1)) * F2) ^ (?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)) 
            * (F2)^((?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)) * F2^(2 * (?N - 1)) < pl^2" by (rule large)
        finally have large: "f12 ^ degree g * g2 ^ degree f1 < pl2" .
        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 "  g2 ^ 1" using coeff_le_sq_norm[of g] by auto 
          also have "  g2 ^ degree f1" 
            by (rule pow_mono_exp, insert deg normg, auto)
          also have " = 1 * " by simp
          also have "  f12 ^ degree g * g2 ^ degree f1" 
            by (rule mult_right_mono, insert normf1, auto)
          also have " < pl2" 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)) * F2^(2 * (degree F div 2)) < pl2"
shows "f = prod_list fs  ( fi  set fs. irreducibled fi)" 
proof -
  interpret p: poly_mod_prime p by (standard, rule p)
  interpret pl: poly_mod_2 "pl" by (standard, rule pl1)
  from pl1 plp have l0: "l  0" by (cases l, auto)
  show ?thesis using assms(1-5)
  proof (induct f us arbitrary: fs rule: LLL_many_reconstruction.induct)
    case (1 f us fs)
    note res = 1(3)
    note degf = 1(4)
    note uf = 1(5)
    note fF = 1(6)
    note norm = 1(7)
    note to_fact = pl.unique_factorization_m_imp_factorization
    note fact = to_fact[OF uf]
    have mon_gs: "ui  set us  monic ui" for ui using norm fact
      unfolding pl.factorization_m_def by auto
    from p.coprime_lead_coeff_factor[OF p.prime] fF cop 
    have cop: "coprime (lead_coeff f) p" unfolding dvd_def by blast
    have plf0: "pl.Mp f  0" 
      using fact pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf by fastforce
    have "degree f = pl.degree_m f" 
      by (rule sym, rule poly_mod.degree_m_eq[OF _ pl.m1], 
          insert cop p, simp add: l0 p.coprime_exp_mod plp)
    also have " =  sum_mset (image_mset pl.degree_m (mset us))"
      unfolding pl.factorization_m_degree[OF fact plf0] ..
    also have " = sum_list (map pl.degree_m us)" 
      unfolding sum_mset_sum_list[symmetric] by auto
    also have " = sum_list (map degree us)" 
      by (rule arg_cong[OF map_cong, OF refl], rule pl.monic_degree_m, insert mon_gs, auto)
    finally have degf_gs: "degree f = sum_list (map degree us)" by auto
    hence gs: "us  []" using degf by (cases us, auto)
    from 1(4) have f0: "f  0" and df0: "degree f  0" by auto
    from norm have norm': "image_mset pl.Mp (mset us) = mset us" by (induct us, auto)
    have pl0: "pl  0" using pl1 by auto

    let ?D2 = "degree F div 2" 
    let ?d2 = "degree f div 2" 
    define gg where "gg = LLL_short_polynomial pl (Suc ?d2)" 
    let ?us = "filter (λu. degree u  ?d2) us" 
    note res = res[unfolded LLL_many_reconstruction.simps[of f us], unfolded Let_def,
        folded gg_def]
    let ?f2_opt = "find_map_filter (λu. gcd f (gg u)) 
      (λf2. 0 < degree f2  degree f2 < degree f) ?us" 
    show ?case
    proof (cases ?f2_opt)
      case (Some f2)
      from find_map_filter_Some[OF this]
      obtain g where deg_f2: "degree f2  0" "degree f2 < degree f"
        and dvd: "f2 dvd f" and gcd: "f2 = gcd f g" by auto
      note res = res[unfolded Some option.simps]

      define f1 where "f1 = f div f2" 
      have f: "f = f1 * f2" unfolding f1_def using dvd by auto
      with arg_cong[OF this, of degree] f0 have deg_sum: "degree f = degree f1 + degree f2" 
        by (auto simp: degree_mult_eq)
      with deg_f2 have deg_f1: "degree f1  0" "degree f1 < degree f" by auto
      from f fF have dvd: "f1 dvd F" "f2 dvd F" unfolding dvd_def by auto
      obtain gs1 gs2 where part: "List.partition (λgi. p.dvdm gi f1) us = (gs1, gs2)" by force  
      note IH = 1(1-2)[OF refl refl refl, unfolded Let_def, folded gg_def, OF Some f1_def part[symmetric] refl] 
      obtain fs1 where fs1: "LLL_many_reconstruction f1 gs1 = fs1" by blast
      obtain fs2 where fs2: "LLL_many_reconstruction f2 gs2 = fs2" by blast
      from res[folded f1_def, unfolded part split fs1 fs2] 
      have fs: "fs = fs1 @ fs2" by auto
      have sf_f: "p.square_free_m f" using sf fF p.square_free_m_factor unfolding dvd_def by blast
      from p.unique_factorization_m_factor_partition[OF l0 uf[unfolded plp] f cop sf_f part]
      have uf: "pl.unique_factorization_m f1 (lead_coeff f1, mset gs1)"  
          "pl.unique_factorization_m f2 (lead_coeff f2, mset gs2)" by (auto simp: plp)
      have "set us = set gs1  set gs2" using part by auto
      with norm have norm_12: "gi  set gs1  gi  set gs2  pl.Mp gi = gi" for gi by auto
      note IH1 = IH(1)[OF fs1 deg_f1(1) uf(1) dvd(1) norm_12]
      note IH2 = IH(2)[OF fs2 deg_f2(1) uf(2) dvd(2) norm_12]
      show ?thesis unfolding fs f using IH1 IH2 by auto
    next
      case None
      from res[unfolded None option.simps] have fs_f: "fs = [f]" by simp
      from sf fF have sf: "p.square_free_m f" 
        using p.square_free_m_factor(1)[of f] unfolding dvd_def by auto
      have "irreducibled f" 
      proof (rule ccontr)
        assume "¬ irreducibled f"
        from reducibledE[OF this] degf obtain f1 f2 where 
          f: "f = f1 * f2" and
          deg12: "degree f1  0" "degree f2  0" "degree f1 < degree f" "degree f2 < degree f" 
          by (simp, metis)
        from f0 have "degree f = degree f1 + degree f2" unfolding f
          by (auto simp: degree_mult_eq)
        hence "degree f1  degree f div 2  degree f2  degree f div 2" by auto
        then obtain f1 f2 where 
          f: "f = f1 * f2" and
          deg12: "degree f1  0" "degree f2  0" "degree f1  degree f div 2" "degree f2 < degree f" 
        proof (standard, goal_cases) 
          case 1
          from 1(1)[of f1 f2] 1(2) f deg12 show ?thesis by auto
        next  
          case 2
          from 2(1)[of f2 f1] 2(2) f deg12 show ?thesis by auto
        qed
        from f0 f have f10: "f1  0" by auto
        from sf f have sf1: "p.square_free_m f1" 
          using p.square_free_m_factor(1)[of f1] by auto
        from p.coprime_lead_coeff_factor[OF p.prime cop[unfolded f]] 
        have cop1: "coprime (lead_coeff f1) p" by auto
        have deg_m1: "pl.degree_m f1 = degree f1" 
          by (rule poly_mod.degree_m_eq[OF _ pl.m1], 
            insert cop1 p, simp add: l0 p.coprime_exp_mod plp)
        from pl.unique_factorization_m_factor[OF p uf[unfolded f], folded f, OF cop sf l0 plp]
        obtain us1 us2 where 
          uf12: "pl.unique_factorization_m f1 (lead_coeff f1, us1)"
            "pl.unique_factorization_m f2 (lead_coeff f2, us2)"
          and gs: "mset us = us1 + us2"
          and norm12: "image_mset pl.Mp us2 = us2" "image_mset pl.Mp us1 = us1"
          unfolding pl.Mf_def norm' split by (auto simp: pl.Mf_def)
        from gs have "x ∈# us1  x ∈# mset us" for x by auto
        hence sub1: "x ∈# us1  x  set us" for x by auto
        from to_fact[OF uf12(1)]
        have fact1: "pl.factorization_m f1 (lead_coeff f1, us1)" .
        have plf10: "pl.Mp f1  0" 
          using fact1 pl.factorization_m_lead_coeff pl.unique_factorization_m_zero uf12(1) by fastforce
        have "degree f1 = pl.degree_m f1" using deg_m1 by simp
        also have " = sum_mset (image_mset pl.degree_m us1)"
          unfolding pl.factorization_m_degree[OF fact1 plf10] ..
        also have " = sum_mset (image_mset degree us1)"
          by (rule arg_cong[of _ _ sum_mset], rule image_mset_cong,
            rule pl.monic_degree_m, rule mon_gs, rule sub1) 
        finally have degf1_sum: "degree f1 = sum_mset (image_mset degree us1)" by auto
        with deg12 have "us1  {#}" by auto
        then obtain u us11 where us1: "us1 = {#u#} + us11" 
          by (cases us1, auto)        
        hence u1: "u ∈# us1" by auto
        hence u: "u  set us" by (rule sub1)
        let ?g = "gg u" 
        from pl.factorization_m_mem_dvdm[OF fact1, of u] u1 have u_f1: "pl.dvdm u f1" by auto
        note norm_u = norm[OF u]
        from fact u have irred: "pl.irreducibled_m u" unfolding pl.factorization_m_def by auto
        hence deg_u: "degree u  0" unfolding pl.irreducibled_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: "F2  1" using sq_norm_poly_pos[of F] by presburger
        have g0: "?g  0" using short(2) .
        from g0 have normg: "?g2  1" using sq_norm_poly_pos[of "?g"] by presburger
        from f10 have normf1: "f12  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 "f12 ^ degree (gg u) * gg u2 ^ degree f1
           f12 ^ ?D2 * gg u2 ^ ?D2" 
          by (rule mult_mono[OF pow_mono_exp pow_mono_exp], 
              insert normf1 normg, auto intro: df1_D2 dg_D2)
        also have " = (f12 * gg u2)^?D2" 
          by (simp add: power_mult_distrib)
        also have "  (f12 * (2^?D2 * f12))^?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 " = f12 ^ (?D2 + ?D2) * 2^(?D2 * ?D2)"
          unfolding power_add power_mult_distrib power_mult by simp
        also have "  (2 ^ (2 * ?D2) * F2) ^ (?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) * F2 ^ (?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: 
          "f12 ^ degree (gg u) * gg u2 ^ 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 "  ?g2" using coeff_le_sq_norm[of ?g] by auto 
          also have " = ?g2 ^ 1" by simp
          also have "  ?g2 ^ degree f1" 
            by (rule pow_mono_exp, insert deg12 normg, auto)
          also have " = 1 * " by simp
          also have "  f12 ^ degree ?g * ?g2 ^ degree f1" 
            by (rule mult_right_mono, insert normf1, auto)
          also have " < pl2" 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  f12 ^ degree (gg u) * gg u2 ^ 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  (gset gs. irreducibled g)"
proof -
  let ?lc = "lead_coeff f" 
  define p where "p  suitable_prime_bz f" 
  obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force
  let ?degs = "map degree gs" 
  note res = res[unfolded LLL_factorization_def Let_def, folded p_def,
    unfolded fff split, folded]
  from suitable_prime_bz[OF sff refl]
  have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" 
    unfolding p_def by auto
  note res
  from prime interpret p: poly_mod_prime p by unfold_locales
  define K where "K = 2^(5 * (degree f - 1) * (degree f - 1)) * f2^(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  (gset gs. irreducibled g)"
proof -
  let ?lc = "lead_coeff f" 
  define p where "p  suitable_prime_bz f" 
  obtain c gs where fff: "finite_field_factorization_int p f = (c,gs)" by force
  let ?degs = "map degree gs" 
  note res = res[unfolded LLL_many_factorization_def Let_def, folded p_def,
    unfolded fff split, folded]
  from suitable_prime_bz[OF sff refl]
  have prime: "prime p" and cop: "coprime ?lc p" and sf: "poly_mod.square_free_m p f" 
    unfolding p_def by auto
  note res
  from prime interpret p: poly_mod_prime p by unfold_locales
  define K where "K = 2^(5 * (degree f div 2) * (degree f div 2)) * f2^(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  (fiset fs. irreducible fi  0 < degree fi  primitive fi)" 
  using assms(1)
  by (intro int_poly_factorization_algorithm_irreducible[of one_lattice_LLL_factorization, 
      OF _ assms(2-)], transfer, auto)
 
thm factorize_int_poly[of one_lattice_LLL_factorization]
thm factorize_int_poly[of many_lattice_LLL_factorization]
end

Theory Sub_Sums

(*
    Author:     René Thiemann
    License:    BSD
*)
section ‹Calculating All Possible Sums of Sub-Multisets›
theory Sub_Sums
  imports 
    Main 
    "HOL-Library.Multiset"
begin

fun sub_mset_sums :: "'a :: comm_monoid_add list  'a set" where
  "sub_mset_sums [] = {0}"
| "sub_mset_sums (x # xs) = (let S = sub_mset_sums xs in S  ( (+) x) ` S)" 

lemma subset_add_mset: "ys ⊆# add_mset x zs  (ys ⊆# zs  ( xs. xs ⊆# zs  ys = add_mset x xs))" 
  (is "?l = ?r")
proof 
  have sub: "ys ⊆# zs  ys ⊆# add_mset x zs"
    by (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)
  assume ?r
  thus ?l using sub by auto
next
  assume l: ?l
  show ?r
  proof (cases "x ∈# ys")
    case True
    define xs where "xs = (ys - {# x #})" 
    from True have ys: "ys = add_mset x xs" unfolding xs_def by auto 
    from l[unfolded ys] have "xs ⊆# zs" by auto
    thus ?r unfolding ys by auto
  next
    case False
    with l have "ys ⊆# zs" by (simp add: subset_mset.le_iff_sup)
    thus ?thesis by auto
  qed
qed

lemma sub_mset_sums[simp]: "sub_mset_sums xs = sum_mset ` { ys. ys ⊆# mset xs }" 
proof (induct xs)
  case (Cons x xs)
  have id: "{ys. ys ⊆# mset (x # xs)} = {ys. ys ⊆# mset xs}  {add_mset x ys | ys. ys ⊆# mset xs}" 
    unfolding mset.simps subset_add_mset by auto
  show ?case unfolding sub_mset_sums.simps Let_def Cons id image_Un 
    by force
qed auto

end

Theory Factorization_Algorithm_16_22

(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Implementation and soundness of a modified version of Algorithm 16.22›

text ‹Algorithm 16.22 is quite similar to the LLL factorization algorithm that was verified
in the previous section. Its main difference is that it has an inner loop where each inner loop
iteration has one invocation of the LLL basis reduction algorithm. Algorithm 16.22 of the textbook
is therefore closer to the factorization algorithm as it is described by Lenstra, Lenstra, and
Lov{\'a}sz \cite{LLL}, which also uses an inner loop.

The advantage of the inner loop is that it can find factors earlier, 
and then small lattices suffice where without the inner loop one
invokes the basis reduction algorithm on a large lattice. The disadvantage of the inner loop
is that if the input is irreducible, then one cannot find any factor early, so that all but the
last iteration have been useless: only the last iteration will prove irreducibility.›

text ‹We will describe the modifications w.r.t.\ the original Algorithm 16.22 of the textbook
later in this theory.›
theory Factorization_Algorithm_16_22
  imports 
    LLL_Factorization
    Sub_Sums
begin

subsection ‹Previous lemmas obtained using local type definitions›

context poly_mod_prime_type
begin                           

lemma irreducible_m_dvdm_prod_list_connect:
  assumes irr: "irreducible_m a"
  and dvd: "a dvdm (prod_list xs)"
shows " b  set xs. a dvdm b"
proof -
  let ?A="(of_int_poly a)::'a mod_ring poly"
  let ?XS="(map of_int_poly xs)::'a mod_ring poly list"
  let ?XS1 = "(of_int_poly (prod_list xs))::'a mod_ring poly"
  have [transfer_rule]: "MP_Rel a ?A"
    by (simp add: MP_Rel_def Mp_f_representative)
  have [transfer_rule]: "MP_Rel (prod_list xs) ?XS1"
    by (simp add: MP_Rel_def Mp_f_representative)
  have [transfer_rule]: "list_all2 MP_Rel xs ?XS"
    by (simp add: MP_Rel_def Mp_f_representative list_all2_conv_all_nth)
  have A: "?A dvd ?XS1" using dvd by transfer
  have " b  set ?XS. ?A dvd b" 
    by (rule irreducible_dvd_prod_list, insert irr, transfer, auto simp add: A)
  from this[untransferred] show ?thesis .
qed

end

lemma (in poly_mod_prime) irreducible_m_dvdm_prod_list:
  assumes irr: "irreducible_m a"
  and dvd: "a dvdm (prod_list xs)"
  shows " b  set xs. a dvdm b"
  by (rule poly_mod_prime_type.irreducible_m_dvdm_prod_list_connect[unfolded poly_mod_type_simps, 
        internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, 
        cancel_type_definition, OF non_empty irr dvd])


subsection ‹The modified version of Algorithm 16.22›

    (* Implementation of the for loop of step 8. The loop will finishes in two cases:
      - If j>n'
      - If a divisor is found *)

definition B2_LLL :: "int poly  int" where
  "B2_LLL f = 2 ^ (2 * degree f) * f2" 

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 (f2 ^ (2 * j') * 2 ^ (5 * j' * j')); 
      ll' = find_exponent p n in if ll' < l then ll' else l);
  ― ‹optimization: dynamically adjust the modulus›
      pl = p^ll;
      g' = LLL_short_polynomial pl j u 
  ― ‹fix: forbid multiples of $p^l$ as short vector, unclear whether this is really required›
  in if abs (lead_coeff g')  pl then None else 
  let ppg = primitive_part g'
  in
  ― ‹slight deviation from textbook: we check divisibility instead of norm-inequality›
  case div_int_poly f ppg of Some f' 
    ― ‹fix: consider modular factors of ppg and not of g'›
    Some (filter (λgi. ¬ poly_mod.dvdm p gi ppg) gs, lead_coeff f', f', ppg)  
  | None  None"


function LLL_reconstruction_inner_loop where
 "LLL_reconstruction_inner_loop j =
  (if j > degree f then ([],1,1,f)
   else case LLL_reconstruction_inner j
     of Some tuple  tuple
     |  None  LLL_reconstruction_inner_loop (j+1))"
  by auto
termination by (relation "measure (λ j. Suc (degree f) - j)", auto)

end
(*The main loop (line 6)*)

partial_function (tailrec) LLL_reconstruction'' where [code]:
 "LLL_reconstruction'' gs b f factors =
  (if gs = [] then factors
   else
     let u = choose_u gs;
         d = degree u;
         gs' = remove1 u gs;
         degs = map degree gs';
         Degs = ((+) d) ` sub_mset_sums degs;
         (gs', b', f', factor) = LLL_reconstruction_inner_loop gs f u Degs (d+1)
     in LLL_reconstruction'' gs' b' f' (factor#factors)
   )"

definition "reconstruction_of_algorithm_16_22 gs f 
  let G = [];
      b = lead_coeff f
  in LLL_reconstruction'' gs b f G"

end

definition factorization_algorithm_16_22 :: "int poly  int poly list" where
  "factorization_algorithm_16_22 f = (let 
     ― ‹find suitable prime›
     p = suitable_prime_bz f;
     ― ‹compute finite field factorization›
     (_, fs) = finite_field_factorization_int p f;
     ― ‹determine l and B›
     n = degree f;
     ― ‹bound improved according to textbook, which uses $no = (n + 1) * (max-norm f)^2$›
     no = f2;
     ― ‹possible improvement: $B = sqrt (2 ^{5 * n * (n - 1)} * no ^ {2 * n - 1}$, cf. @{const LLL_factorization}
     B = sqrt_int_ceiling (2 ^ (5 * n * n) * no ^ (2 * n));
     l = find_exponent p B;
     ― ‹perform hensel lifting to lift factorization to mod $p^l$›
     vs = hensel_lifting p l f fs
     ― ‹reconstruct integer factors›
   in reconstruction_of_algorithm_16_22 p l vs f)"


subsection ‹Soundness proof›

subsubsection ‹Starting the proof›

text ‹Key lemma to show that forbidding values of $p^l$ or larger suffices to find correct factors.›

lemma (in poly_mod_prime) Mp_smult_p_removal: "poly_mod.Mp (p * p ^ k) (smult p f) = 0  poly_mod.Mp (p^k) f = 0"
  by (smt add.left_neutral m1 poly_mod.Dp_Mp_eq poly_mod.Mp_smult_m_0 sdiv_poly_smult smult_smult)

lemma (in poly_mod_prime) eq_m_smult_p_removal: "poly_mod.eq_m (p * p ^ k) (smult p f) (smult p g) 
   poly_mod.eq_m (p^k) f g" using Mp_smult_p_removal[of k "f - g"]
  by (metis add_diff_cancel_left' diff_add_cancel diff_self poly_mod.Mp_0 poly_mod.minus_Mp(2) smult_diff_right)

lemma content_le_lead_coeff: "abs (content (f :: int poly))  abs (lead_coeff f)"
proof (cases "f = 0")
  case False
  from content_dvd_coeff[of f "degree f"] have "abs (content f) dvd abs (lead_coeff f)" by auto
  moreover have "abs (lead_coeff f)  0" using False by auto
  ultimately show ?thesis by (smt dvd_imp_le_int)
qed auto

lemma poly_mod_dvd_drop_smult: assumes u: "monic u" and p: "prime p" and c: "c  0" "¦c¦ < p^l"
  and dvd: "poly_mod.dvdm (p^l) u (smult c f)" 
shows "poly_mod.dvdm p u f" 
  using c dvd
proof (induct l arbitrary: c rule: less_induct)
  case (less l c)
  interpret poly_mod_prime p by (unfold_locales, insert p, auto)
  note c = less(2-3)
  note dvd = less(4)
  note IH = less(1)
  show ?case
  proof (cases "l = 0")
    case True
    thus ?thesis using c dvd by auto
  next
    case l0: False
    interpret pl: poly_mod_2 "p^l" by (unfold_locales, insert m1 l0, auto)
    show ?thesis
    proof (cases "p dvd c")
      case False
      let ?i = "inverse_mod c (p ^ l)" 
      have "gcd c p = 1" using p False
        by (metis Primes.prime_int_iff gcd_ge_0_int semiring_gcd_class.gcd_dvd1 semiring_gcd_class.gcd_dvd2)
      hence "coprime c p" by (metis dvd_refl gcd_dvd_1)
      from pl.inverse_mod_coprime_exp[OF refl p l0 this] 
      have id: "pl.M (?i * c) = 1" .
      have "pl.Mp (smult ?i (smult c f)) = pl.Mp (smult (pl.M (?i * c)) f)" by simp
      also have " = pl.Mp f" unfolding id by simp
      finally have "pl.dvdm u f" using pl.dvdm_smult[OF dvd, of ?i] unfolding pl.dvdm_def by simp
      thus "u dvdm f" using l0 pl_dvdm_imp_p_dvdm by blast 
    next
      case True
      then obtain d where cpd: "c = p * d" unfolding dvd_def by auto
      from cpd c have d0: "d  0" by auto
      note to_p = Mp_Mp_pow_is_Mp[OF l0 m1]
      from dvd obtain v where eq: "pl.eq_m (u * v) (smult p (smult d f))" 
        unfolding pl.dvdm_def cpd by auto
      from arg_cong[OF this, of Mp, unfolded to_p] 
      have "Mp (u * v) = 0" unfolding Mp_smult_m_0 .
      with u have "Mp v = 0"
        by (metis Mp_0 add_eq_0_iff_both_eq_0 degree_0 
            degree_m_mult_eq monic_degree_0 monic_degree_m mult_cancel_right2)
      from Mp_0_smult_sdiv_poly[OF this]
      obtain w where v: "v = smult p w" by metis
      with eq have eq: "pl.eq_m (smult p (u * w)) (smult p (smult d f))" by simp
      from l0 obtain ll where "l = Suc ll" by (cases l, auto)
      hence pl: "p^l = p * p^ll" and ll: "ll < l" by auto
      from c(2) have d_small: "¦d¦ < p^ll" unfolding pl cpd abs_mult
        using mult_less_cancel_left_pos[of p d "p^ll"] m1 by auto
      from eq_m_smult_p_removal[OF eq[unfolded pl]] 
      have "poly_mod.eq_m (p^ll) (u * w) (smult d f)" .
      hence dvd: "poly_mod.dvdm (p^ll) u (smult d f)" unfolding poly_mod.dvdm_def by metis
      show ?thesis by (rule IH[OF ll d0 d_small dvd])
    qed
  qed
qed

context
  fixes p :: int
    and F :: "int poly"
    and N :: nat
    and l :: nat
  defines [simp]: "N  degree F"
  assumes p: "prime p"
      and N0: "N > 0"
      and bound_l: "2 ^ N2 * B2_LLL F ^ (2 * N)  (p^l)2"
begin

private lemma F0: "F0" 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 "F2  0" by simp
  hence F1: "F2  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 ^ N2 * 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: "nN" 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.irreducibled_m f  monic f" by auto   
  from norm_gs have norm_gs: "image_mset pl.Mp (mset gs) = mset gs" by (induct gs, auto) 
  from assms obtain h where f: "f = g * h" unfolding dvd_def by auto
  from pl.unique_factorization_m_factor[OF p.prime f_gs[unfolded f] _ _ l0 refl, folded f, 
      OF cop sf, unfolded pl.Mf_def split] norm_gs
  obtain hs fs where uf: "pl.unique_factorization_m h (lead_coeff h, hs)" 
      "pl.unique_factorization_m g (lead_coeff g, fs)" 
     and id: "mset gs = fs + hs" 
     and norm: "image_mset pl.Mp fs = fs" "image_mset pl.Mp hs = hs" by auto
  from p.square_free_m_prod_imp_coprime_m[OF sf[unfolded f]] 
  have cop_h_f: "p.coprime_m g h" by auto  
  show "pl.dvdm u g"
  proof (cases "u ∈# fs")
    case True
    hence "pl.Mp u ∈# image_mset pl.Mp fs" by auto
    from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf(2)] this]
    show ?thesis .
  next
    case False
    from u_gs have "u ∈# mset gs" by auto
    from this[unfolded id] False have "u ∈# hs" by auto
    hence "pl.Mp u ∈# image_mset pl.Mp hs" by auto
    from pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization[OF uf(1)] this]
    have "pl.dvdm u h" by auto
    from pl_dvdm_imp_p_dvdm[OF this] 
    have "p.dvdm u h" by auto
    from cop_h_f[unfolded p.coprime_m_def, rule_format, OF dvd this]
    have "p.dvdm u 1" .
    from p.dvdm_imp_degree_le[OF this u _ p.m1] have "degree u = 0" by auto
    with deg_u show ?thesis by auto
  qed
qed

private lemma uf: "pl.dvdm u f" using dvdm_power[OF dvd_refl] u_f by simp

lemma exists_reconstruction: "h0. irreducibled 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_irreducibled[OF refl sf_F deg_f]
  obtain fs where f_fs: "f = prod_list fs"
    and c: "(fiset fs. irreducibled 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 "irreducibled h0" using c h0 by auto
  ultimately show ?thesis by blast
qed

lemma factor_dvd_f_0: assumes "factor dvd f" 
  shows "pl.Mp factor  0"
proof -
  from assms obtain h where f: "f = factor * h" unfolding dvd_def ..
  from arg_cong[OF this, of pl.Mp] have "0  pl.Mp (pl.Mp factor * h)" 
    using Mpf0 by auto
  thus ?thesis by fastforce
qed

lemma degree_factor_ge_degree_u:
  assumes u_dvdm_factor: "p.dvdm u factor" 
    and factor_dvd: "factor dvd f" shows "degree u  degree factor"
proof - 
  from factor_dvd_f_0[OF factor_dvd] have factor0: "pl.Mp factor  0" .  
  from u_dvdm_factor[unfolded dvdm_power[OF factor_dvd] pl.dvdm_def] obtain v where
    *: "pl.Mp factor = pl.Mp (u * pl.Mp v)" by auto
  with factor0 have v0: "pl.Mp v  0" by fastforce
  hence "0  lead_coeff (pl.Mp v)" by auto
  also have "lead_coeff (pl.Mp v) = pl.M (lead_coeff (pl.Mp v))" 
    by (auto simp: pl.Mp_def coeff_map_poly)
  finally have **: "lead_coeff (pl.Mp v)  p ^ l * r" for r by (auto simp: pl.M_def) 
  from * have "degree factor  pl.degree_m (u * pl.Mp v)" using pl.degree_m_le[of factor] by auto
  also have "pl.degree_m (u * pl.Mp v) = degree (u * pl.Mp v)" 
    by (rule pl.degree_m_eq, unfold lead_coeff_mult, insert u pl.m1 **, auto)
  also have " = degree u + degree (pl.Mp v)" 
    by (rule degree_mult_eq, insert v0 u, auto)
  finally show ?thesis by auto
qed

subsubsection ‹Inner loop›

context
  fixes j' :: nat
  assumes dj': "d  j'"
      and j'n: "j' < n"
      and deg: "factor. p.dvdm u factor  factor dvd f  degree factor  j'"
begin

private abbreviation (input) "j  Suc j'"

private lemma jn: "j  n" using j'n by auto
    
private lemma factor_irreducibledI: assumes hf: "h dvd f" 
  and puh: "p.dvdm u h" 
  and degh: "degree h > 0" 
  and degh_j: "degree h  j'"
shows "irreducibled 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 irreducibledI degh)
    fix q r
    assume deg_q: "degree q > 0" "degree q < degree h"
      and deg_r: "degree r > 0" "degree r < degree h"
      and h: "h = q * r"
    then have "r dvd h" by auto
    with h dvd_trans[OF _ hf] have 1: "q dvd f" "r dvd f" by auto
    from cop[unfolded f] have cop: "coprime (lead_coeff h) p"
      using p.prime pl.coprime_lead_coeff_factor(1) by blast
    from sf[unfolded f] have sf: "p.square_free_m h" using p.square_free_m_factor by metis
    have norm_gs1: "image_mset pl.Mp (mset gs1) = mset gs1" using norm_gs unfolding gs1
      by (induct gs, auto)
    from pl.unique_factorization_m_factor[OF p uf_h[unfolded h], folded h, OF cop sf l0 refl]
    obtain fs gs where uf_q: "pl.unique_factorization_m q (lead_coeff q, fs)"
     and uf_r: "pl.unique_factorization_m r (lead_coeff r, gs)"
     and id: "mset gs1 = fs + gs"
      unfolding pl.Mf_def split using norm_gs1 by auto
    from degh degh_j deg_q deg_r have qj': "degree q < j'" and rj': "degree r < j'" by auto
    have intro: "u ∈# r  pl.Mp u ∈# image_mset pl.Mp r" for r by auto 
    note dvdI = pl.factorization_m_mem_dvdm[OF pl.unique_factorization_m_imp_factorization intro]
    from u_gs1 id have "u ∈# fs  u ∈# gs" unfolding in_multiset_in_set[symmetric] by auto
    with dvdI[OF uf_q] dvdI[OF uf_r] have "pl.dvdm u q  pl.dvdm u r" by auto
    hence "p.dvdm u q  p.dvdm u r" using pl_dvdm_imp_p_dvdm by blast
    with 1 qj' rj' show False
      by (elim disjE, auto dest!: deg)
  qed
qed

private definition "ll = (let n = sqrt_int_ceiling (f2 ^ (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'  g2  2 ^ j' * h2" 
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 ([gigs . ¬ 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: "g2  1" using sq_norm_poly_pos[of g] by presburger
  from f0 have normf: "f2  1" using sq_norm_poly_pos[of f] by presburger
  from factor0 have normf1: "factor2  1" using sq_norm_poly_pos[of factor] by presburger
  from F0 have normF: "F2  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 "factor2 ^ degree g * g2 ^ degree factor  factor2 ^ j' * g2 ^ j'"
    by (rule mult_mono[OF power_increasing], insert normg normf1 deg_g, auto)
  also have " = (factor2 * g2)^j'" by (simp add: power_mult_distrib)
  also have "  (factor2 * (2 ^ j' * factor2))^j'"
    by (rule power_mono[OF mult_left_mono], insert LLL(4), auto)
  also have " = factor2 ^ (2 * j') * 2 ^ (j' * j')" 
    unfolding power_mult_distrib power_mult power_add mult_2 by simp
  finally have approx_part_1: "factor2 ^ degree g * g2 ^ degree factor  factor2 ^ (2 * j') * 2 ^ (j' * j')" .
  {
    fix f :: "int poly" 
    assume *: "factor dvd f" "f  0" 
    note approx_part_1
    also have "factor2 ^ (2 * j') * 2 ^ (j' * j')  (2^(2*j') * f2) ^ (2 * j') * 2 ^ (j' * j')" 
      by (rule mult_right_mono[OF power_mono], insert sq_norm_factor_bound[OF *], auto)
    also have " = f2 ^ (2 * j') * 2 ^ (2*j' * 2*j' + j' * j')" 
      unfolding power_mult_distrib power_add by (simp add: power_mult[symmetric])
    also have "2*j' * 2*j' + j' * j' = 5 * j' * j'" by simp
    finally have "factor2 ^ degree g * g2 ^ degree factor  f2 ^ (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: "factor2 ^ degree g * g2 ^ degree factor < (p^ll)2" 
  proof (cases "ll = l")
    case False
    let ?n = "f2 ^ (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 "F2 ^ (2 * j') * 2 ^ (5 * j' * j') 
          = 2 ^ (2 * j' * j' + 3 * j' * j') * F2 ^ (j' + j')" 
        unfolding mult_2 by simp 
      also have " < 2 ^ (N2 + 4 * N*N) * F2 ^ (2 * N)" 
      proof (rule mult_less_le_imp_less[OF power_strict_increasing pow_mono_exp])
        show "1  F2" 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 < F2 ^ (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 " = N2 + 4 * N * N" by (simp add: power2_eq_square) 
        finally show "2 * j' * j' + 3 * j' * j' < N2 + 4 * N * N" .
      qed auto
      also have " = 2 ^ N2 * (2 ^ (2 * N) * F2) ^ (2 * N)"
        unfolding power_mult_distrib power_add by (simp add: power_mult[symmetric])
      finally show "F2 ^ (2 * j') * 2 ^ (5 * j' * j') < 2 ^ N2 * B2_LLL F ^ (2 * N)" 
        unfolding B2_LLL_def by simp
    qed
  qed
  have "(¦lead_coeff g¦)^2 < (p^ll)^2" 
  proof (rule le_less_trans[OF _ large])
    have "1 * (¦lead_coeff g¦2)^1  factor2 ^ degree g * g2 ^ 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  factor2 ^ degree g * g2 ^ 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 "  g2" using coeff_le_sq_norm[of g] by auto 
    also have " = g2 ^ 1" by simp
    also have "  g2 ^ degree factor" 
      by (rule pow_mono_exp, insert deg_f normg j'0, auto)
    also have " = 1 * " by simp
    also have "  factor2 ^ degree g * g2 ^ 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: "irreducibled factor" 
    by (rule factor_irreducibledI[OF factor_f pu_factor deg_factor], simp)
  from gcd_factor obtain h where factor: "factor = ?g * h" unfolding dvd_def by auto
  from irreducibledD(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 "irreducibled h" (is "?g2")
    and "b' = lead_coeff f'" (is "?g3")
    and "pl.unique_factorization_m f' (lead_coeff f', mset gs')" (is "?g4")
    and "p.dvdm u h" (is ?g5)
    and "degree h = j'" (is ?g6)
    and "length gs' < length gs" (is ?g7)
    and "set gs'  set gs" (is ?g8)
    and "gs'  []" (is ?g9) 
proof -
  let ?ppg = "primitive_part g" 
  note ret = ret[unfolded LLL_reconstruction_inner_simps]   
  from ret have lc: "abs (lead_coeff g) < p^ll" by (auto split: if_splits)
  from ret obtain rest where rest: "div_int_poly f (primitive_part g) = Some rest" 
    by (auto split: if_splits option.splits)
  from ret[unfolded this] div_int_then_rqp[OF this] lc
  have out [simp]: "h = ?ppg" "gs' = filter (λ gi. ¬ p.dvdm gi ?ppg) gs" 
    "f' = rest" "b' = lead_coeff rest"
   and f: "f = ?ppg * rest" by (auto split: if_splits)
  with div_int_then_rqp[OF rest] show ?g1 ?g3 by auto
  from ?g1 f0 have h0: "h  0" by auto
  let ?c = "content g" 
  from g0 have ct0: "?c  0" by auto
  have "¦?c¦  ¦lead_coeff g¦" by (rule content_le_lead_coeff)
  also have " < p^ll" by fact
  finally have ct_pl: "¦?c¦ < p^ll" .
  from ug have "pll.dvdm u (smult ?c ?ppg)" by simp
  from poly_mod_dvd_drop_smult[OF u p ct0 ct_pl this]
  show puh: "p.dvdm u h" by simp
  with dvdm_power[of h] f
  have uh: "pl.dvdm u h" by (auto simp: dvd_def)
  from f have hf: "h dvd f" by (auto intro:dvdI)
  have degh: "degree h > 0"
    by (metis d_def deg deg_u puh dj' hf le_neq_implies_less not_less0 neq0_conv)
  show irr_h: ?g2
    by (intro factor_irreducibledI degh hf puh, insert deg_g_j, simp)
  show deg_h: ?g6 using deg deg_g_j g_def hf le_less_Suc_eq puh degree_primitive_part by force
  show ?g7 unfolding out 
    by (rule length_filter_less[of u], insert pl_dvdm_imp_p_dvdm[OF uh] u_gs, auto)
  show ?g8 by auto
  from f out have fh: "f = h * f'" and gs': "gs' = [gi  gs. ¬ p.dvdm gi h]" by auto
  note [simp del] = out
  let ?fs = "filter (λgi. p.dvdm gi h) gs" 
  have part: "List.partition (λgi. p.dvdm gi h) gs = (?fs, gs')" 
    unfolding gs' by (auto simp: o_def)
  from p.unique_factorization_m_factor_partition[OF l0 f_gs fh cop sf part]
  show uf: "pl.unique_factorization_m f' (lead_coeff f', mset gs')" by auto
  show ?g9
  proof
    assume "gs' = []" 
    with pl.unique_factorization_m_imp_factorization[OF uf, unfolded pl.factorization_m_def]
    have "pl.Mp f' = pl.Mp (smult (lead_coeff f') 1)" by auto
    from arg_cong[OF this, of degree] pl.degree_m_le[of "smult (lead_coeff f') 1"] 
    have "pl.degree_m f' = 0" by simp 
    also have "pl.degree_m f' = degree f'" 
    proof (rule poly_mod.degree_m_eq[OF _ pl.m1])
      have "coprime (lead_coeff f') p" 
        by (rule  p.coprime_lead_coeff_factor[OF p.prime cop[unfolded fh]])
      thus "lead_coeff f' mod p ^ l  0" using l0 p.prime by fastforce
    qed
    finally have degf': "degree f' = 0" by auto
    from degree0_coeffs[OF this] f0 fh obtain c where "f' = [:c:]" and c: "c  0" and fch: "f = smult c h"
      by auto
    from ‹irreducibled h have irr_f: "irreducibled f" 
      using irreducibled_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 "jn"
  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: "dj" and jn: "jn"
  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 "irreducibled f" 
proof - 
  obtain factor 
    where irreducible_factor: "irreducibled 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 irreducibled_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: "irreducibled 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 "ji" 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: "irreducibled 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 irreducibled_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 "¬ irreducibled f" 
    by (rule reducibledI, 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 "jn")
    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: "irreducibled 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: "jn" and f: "¬ irreducibled 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 "irreducibled f"
          by(rule LLL_reconstruction_inner_all_None_imp_irreducible[OF i2])
        thus ?thesis using f by simp
      next
        case False
        have "?inner n = Some (gs', b', f', factor)" 
          using False 1 j_eq_n by auto
        moreover have "i{d + 1..<n}. ?inner i = None" 
          using 2 j_eq_n by simp
        moreover have "d < n" using 1 2 jn j_eq_n
          using False  dn nat_less_le
          using d_def dj by auto
        ultimately show ?thesis using j_eq_n by fastforce
      qed    
    next
      case False
      have "j'j + 1. j'  n  d < j' 
                 ?inner j' = Some (gs', b', f', factor) 
                 (i{d + 1..<j'}. ?inner i = None)"
      proof (rule hyp)
        show "¬ degree f < j" using jn by auto
        show "?inner j = None" using True by auto
        show "?innerl (j + 1) = (gs', b', f', factor)" 
          using 1 True jn by auto
        show "i{d + 1..<j + 1}. ?inner i = None"        
          by (metis "2" One_nat_def True add.comm_neutral add_Suc_right atLeastLessThan_iff 
              le_neq_implies_less less_Suc_eq_le)      
        show "d < j + 1" using dj by auto
        show " j + 1  n" using jn False by auto
      qed
      from this obtain j' where a1: "j'j + 1" and a2: "j'  n" and a3: "d < j'"
        and a4: "?inner j' = Some (gs', b', f', factor)"
        and a5: "(i{d + 1..<j'}. ?inner i = None)" by auto
      moreover have "j'j" using a1 by auto
      ultimately show ?thesis by fastforce
    qed
  next
    case False    
    have 1: "?inner j = Some (gs', b', f', factor)" 
      using False 1 jn by auto
    moreover have 2: "(i{d + 1..<j}. ?inner i = None)" 
      by (rule 2)
    moreover have 3: "j  n" using jn by auto
    moreover have 4: "d < j" using 2 False dj jn
      using le_neq_implies_less by fastforce
    ultimately show ?thesis by auto
  qed
qed  

(* TODO: move *)
lemma unique_factorization_m_1: "pl.unique_factorization_m 1 (1, {#})"
proof (intro pl.unique_factorization_mI)
  fix d gs
  assume pl: "pl.factorization_m 1 (d,gs)" 
  from pl.factorization_m_degree[OF this] have deg0: " g. g ∈# gs  pl.degree_m g = 0" by auto
  {
    assume "gs  {#}" 
    then obtain g hs where gs: "gs = {# g #} + hs" by (cases gs, auto)
    with pl have *: "pl.irreducibled_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.irreducibled_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 "irreducibled 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 "irreducibled 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 "irreducibled 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 "irreducibled 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 "irreducibled 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: "jn" 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  irreducibled 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.irreducibled_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'. irreducibled 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.irreducibled_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