Theory LLL_Factorization

theory LLL_Factorization
imports LLL_Factorization_Impl Factorize_Int_Poly
(*
    Authors:    Jose Divasón
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Correctness of the LLL factorization algorithm›

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

theory LLL_Factorization
  imports
    LLL_Factorization_Impl  
    Berlekamp_Zassenhaus.Factorize_Int_Poly
begin

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

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

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

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

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

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

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

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

declare choose_u.simps[simp del]


subsection ‹Facts about Sylvester matrices and norms›

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

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


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

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

lemma resultant_le_prod_sq_norm:
  fixes f g::"int poly"
  defines "n ≡ degree f" and "k ≡ degree g"
  shows "¦resultant f g¦ ≤ sqrt (of_int (∥f∥2^k * ∥g∥2^n))"
proof -
  let ?S = "sylvester_mat f g"
  let ?f = "sq_norm ∘ row ?S"
  have map_rw1: "map ?f [0..<degree g] = replicate k ∥f∥2"
  proof (rule nth_equalityI)
    let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [0..<degree g]"
    show "length ?M = length (replicate k ∥f∥2)" using k_def by auto
    show "?M ! i = replicate k ∥f∥2 ! i" if i: "i < length ?M" for i
    proof -
      have ik: "i<k" using i k_def by auto
      hence i_deg_g: "i < degree g" using k_def by auto
      have "replicate k ∥f∥2 ! i = ∥f∥2" by (rule nth_replicate[OF ik])
      also have "... = (sq_norm ∘ row (sylvester_mat f g)) (0 + i)"
        using sq_norm_row_sylvester_mat1 ik k_def by force      
      also have "... = ?M ! i" by (rule nth_map_upt[symmetric], simp add: i_deg_g)
      finally show "?M ! i = replicate k ∥f∥2 ! i" ..
    qed
  qed    
  have map_rw2: "map ?f [degree g..<degree f + degree g] = replicate n ∥g∥2"
  proof (rule nth_equalityI)
    let ?M = "map (sq_norm ∘ row (sylvester_mat f g)) [degree g..<degree f + degree g]"
    show "length ?M = length (replicate n ∥g∥2)" by (simp add: n_def)
    show "?M ! i = replicate n ∥g∥2 ! i" if "i<length ?M" for i
    proof -
      have i_n: "i<n" using n_def that by auto
      hence i_deg_f: "i < degree f" using n_def by auto
      have "replicate n ∥g∥2 ! i = ∥g∥2" by (rule nth_replicate[OF i_n])
      also have "... = (sq_norm ∘ row (sylvester_mat f g)) (degree g + i)"
        using i_n n_def
        by (simp add: sq_norm_row_sylvester_mat2)
      also have "... = ?M ! i"
        by (simp add: i_deg_f)
      finally show "?M ! i = replicate n ∥g∥2 ! i" ..
    qed
  qed
  have p1: "prod_list (map ?f [0..<degree g]) = ∥f∥2^k"
    unfolding map_rw1 by (rule prod_list_replicate)
  have p2: "prod_list (map ?f [degree g..<degree f + degree g]) = ∥g∥2^n"
    unfolding map_rw2 by (rule prod_list_replicate)
  have list_rw: "[0..<degree f + degree g] = [0..<degree g] @ [degree g..<degree f + degree g]"
    by (metis add.commute upt_add_eq_append zero_le)
  have "¦resultant f g¦ = ¦det ?S¦"  unfolding resultant_def ..
  also have "... ≤ sqrt (of_int (prod_list (map sq_norm (rows ?S))))"
    by (rule Hadamard's_inequality_int, auto)
  also have "map sq_norm (rows ?S) = map ?f [0..<degree f + degree g]"
    unfolding Matrix.rows_def by auto
  also have "... =  map ?f ([0..<degree g] @ [degree g..<degree f + degree g])"
    by (simp add: list_rw)
  also have "prod_list ... = prod_list (map ?f [0..<degree g])
    * prod_list (map ?f [degree g..<degree f + degree g])" by auto
  finally show ?thesis unfolding p1 p2 .
qed

subsection ‹Proof of the key lemma 16.20›
(* Lemma 16.20 *)
lemma common_factor_via_short:
  fixes f g u :: "int poly"
  defines "n ≡ degree f" and "k ≡ degree g"
  assumes n0: "n > 0" and k0: "k > 0"
      and monic: "monic u" and deg_u: "degree u > 0"
      and uf: "poly_mod.dvdm m u f" and ug: "poly_mod.dvdm m u g"
      and short: "∥f∥2^k * ∥g∥2^n < 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 (∥f∥2 ^ k * ∥g∥2 ^ n)"
        by (simp add: sq_norm_poly_ge_0)
      show "0 ≤ real_of_int m" using m by simp
      show "real_of_int (∥f∥2 ^ k * ∥g∥2 ^ n) < (real_of_int m)2"
        by (metis of_int_less_iff of_int_power short)
    qed
    finally show "¦resultant f g¦ < m" using of_int_less_iff by blast 
    qed
  have "¬ coprime f g" 
    by (rule resultant_zero_imp_common_factor, auto simp add: deg_f res0)
  thus ?thesis
    using res0 resultant_0_gcd by auto
qed  

subsection ‹Properties of the computed lattice and its connection with Sylvester matrices›

lemma factorization_lattice_as_sylvester:
  fixes p :: "'a :: semidom poly"
  assumes dj: "d ≤ j" and d: "degree p = d"   
  shows "mat_of_rows j (factorization_lattice p (j-d) m) = sylvester_mat_sub d (j-d) p [:m:]"
proof (cases "p=0")
  case True 
  have deg_p: "d = 0" using True d by simp
  show ?thesis
    by (auto simp add: factorization_lattice_def True deg_p mat_of_rows_def d)
next
  case p0: False
  note 1 = degree_mult_eq[OF p0, of "monom _ _", unfolded monom_eq_0_iff, OF one_neq_zero]
  from dj show ?thesis
    apply (cases "m = 0")
    apply (auto simp: mat_eq_iff d[symmetric] 1 coeff_mult_monom
 sylvester_mat_sub_index mat_of_rows_index nth_factorization_lattice vec_index_of_poly_n
 degree_monom_eq coeff_const)
    done
qed


context inj_comm_semiring_hom begin

lemma map_poly_hom_mult_monom [hom_distribs]:
  "map_poly hom (p * monom a n) = map_poly hom p * monom (hom a) n"
  by (auto intro!: poly_eqI simp:coeff_mult_monom hom_mult)

lemma hom_vec_of_poly_n [hom_distribs]:
  "map_vec hom (vec_of_poly_n p n) = vec_of_poly_n (map_poly hom p) n"
  by (auto simp: vec_index_of_poly_n)

lemma hom_factorization_lattice [hom_distribs]:
  shows "map (map_vec hom) (factorization_lattice u k m) = factorization_lattice (map_poly hom u) k (hom m)"
  by (auto intro!:arg_cong[of _ _ "λp. vec_of_poly_n p _"] simp: list_eq_iff_nth_eq nth_factorization_lattice hom_vec_of_poly_n map_poly_hom_mult_monom)

end

subsection ‹Proving that @{const factorization_lattice} returns a basis of the lattice›

context LLL
begin

sublocale idom_vec n "TYPE(int)".

(*In this context, "n" is fixed by the locale and corresponds to "j" in the book*)
lemma upper_triangular_factorization_lattice:
  fixes u :: "'a :: semidom poly" and d :: nat
  assumes d: "d ≤ n" and du: "d = degree u"
  shows "upper_triangular (mat_of_rows n (factorization_lattice u (n-d) k))"
    (is "upper_triangular ?M")
proof (intro upper_triangularI, unfold mat_of_rows_carrier length_factorization_lattice)
  fix i j
  assume ji: "j < i" and i: "i < degree u + (n - d)"
  with d du have jn: "j < n" by auto
  show "?M $$ (i,j) = 0"
  proof (cases "u=0")
    case True with ji i show ?thesis
      by (auto simp: factorization_lattice_def mat_of_rows_def)
next
  case False
  then show ?thesis
    using d ji i
    apply (simp add: du mat_of_rows_index nth_factorization_lattice)
    apply (auto simp: vec_index_of_poly_n[OF jn] degree_mult_eq degree_monom_eq)
    done
  qed
qed

lemma factorization_lattice_diag_nonzero:
  fixes u :: "'a :: semidom poly" and d
  assumes d: "d=degree u" 
    and dn: "d≤n"
    and u: "u≠0" 
    and m0: "k≠0"
    and i: "i<n"
  shows "(factorization_lattice u (n-d) k) ! i $ i ≠ 0"
proof-
  have 1: "monom (1::'a) (n - Suc (degree u + i)) ≠ 0" using m0 by auto
  have 2: "i < degree u + (n - d)" using i d by auto
  let ?p = "u * monom 1 (n - Suc (degree u + i))"
  have 3: "i < n - degree u ⟹ degree (?p) = n - Suc i"
    using assms by (auto simp: degree_mult_eq[OF _ 1] degree_monom_eq)
  show ?thesis
    apply (unfold nth_factorization_lattice[OF 2] vec_index_of_poly_n[OF 2])
    using assms leading_coeff_0_iff[of ?p]
    apply (cases "i < n - degree u", auto simp: d 3 degree_monom_eq)
    done
qed

corollary factorization_lattice_diag_nonzero_RAT: fixes d
  assumes "d=degree u" 
    and "d≤n"
    and "u≠0" 
    and "k≠0"
    and "i<n"
  shows "RAT (factorization_lattice u (n-d) k) ! i $ i ≠ 0"
  using factorization_lattice_diag_nonzero[OF assms] assms
  by (auto simp: nth_factorization_lattice)

sublocale gs: vec_space "TYPE(rat)" n.

lemma lin_indpt_list_factorization_lattice: fixes d
  assumes d: "d = degree u" and dn: "d ≤ n" and u: "u ≠ 0" and k: "k ≠ 0"
  shows "gs.lin_indpt_list (RAT (factorization_lattice u (n-d) k))" (is "gs.lin_indpt_list (RAT ?vs)")
proof-
  have 1: "rows (mat_of_rows n (map (map_vec rat_of_int) ?vs)) = map (map_vec rat_of_int) ?vs"
    using dn d
    by (subst rows_mat_of_rows, auto dest!: subsetD[OF set_factorization_lattice_in_carrier])
  note 2 = factorization_lattice_diag_nonzero_RAT[OF d dn u k]
  show ?thesis
    apply (intro gs.upper_triangular_imp_lin_indpt_list[of "mat_of_rows n (RAT ?vs)", unfolded 1])
    using assms 2 by (auto simp: diag_mat_def mat_of_rows_index hom_distribs intro!:upper_triangular_factorization_lattice)
 qed
  
end

subsection ‹Being in the lattice is being a multiple modulo›

lemma (in semiring_hom) hom_poly_of_vec: "map_poly hom (poly_of_vec v) = poly_of_vec (map_vec hom v)"
  by (auto simp add: coeff_poly_of_vec poly_eq_iff)

abbreviation "of_int_vec ≡ map_vec of_int"

context LLL
begin

lemma lincomb_to_dvd_modulo:
  fixes u d
  defines "d ≡ degree u"
  assumes d: "d ≤ n"
      and lincomb: "lincomb_list c (factorization_lattice u (n-d) k) = g" (is "?l = ?r")
  shows "poly_mod.dvdm k u (poly_of_vec g)"
proof- 
  let ?S = "sylvester_mat_sub d (n - d) u [:k:]"
  define q where "q ≡ poly_of_vec (vec_first (vec n c) (n - d))"
  define r where "r ≡ poly_of_vec (vec_last (vec n c) d)"
  have "?l = ?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: "k≠0"
      and monic_u: "monic u"
      and dim_g: "dim_vec g = n"
      and deg_u: "degree u > 0"      
  shows "∃c. lincomb_list c (factorization_lattice u (n-d) k) = g"
proof -
  interpret p: poly_mod k .
  have u_not0: "u ≠ 0" using monic_u by auto
  hence n[simp]: "0 < n" using d by auto
  obtain q' r' where g: "poly_of_vec g = q' * u + smult k r'"
    using p.dvdm_imp_div_mod[OF dvd] by auto
  obtain q'' r'' where r': "r' = q'' * u + r''" and deg_r'': "degree r''<degree u"
    using monic_imp_div_mod_int_poly_degree2[OF monic_u deg_u, of r'] by auto
  (*The following fact is explained in the paragraph below equation (6) in page 476 of the textbook*)
  have g1: "poly_of_vec g = (q' + smult k q'') * u + smult k r''" 
    unfolding g r'
    by (metis (no_types, lifting) combine_common_factor mult_smult_left smult_add_right)
  define q where q: "q = (q' + smult k q'')"
  define r where r: "r = r''"
  have degree_q: "q = 0 ∨ degree (q' + smult k q'') < n - d"
  proof (cases "q = 0",auto, rule degree_div_mod_smult[OF _ _ _ g1])
    show "degree (poly_of_vec g) < n" by (rule degree_poly_of_vec_less, auto simp add: dim_g)
    show "degree r'' < d" using deg_r'' unfolding d_def .
    assume "q≠0" thus "q' + smult k q'' ≠ 0" unfolding q .
    show "k ≠ 0" by fact
    show "degree u = d" using d_def by auto
  qed
  have g2: "(vec_of_poly_n (q*u) n) + (vec_of_poly_n (smult k r) n) = g" 
  proof -
    have "g = vec_of_poly_n (poly_of_vec g) n"
      by (rule vec_of_poly_n_poly_of_vec[symmetric], auto simp add: dim_g)
    also have "… = vec_of_poly_n ((q' + smult k q'') * u + smult k r'') n" 
      using g1 by auto
    also have "... = vec_of_poly_n (q * u + smult k r'') n" unfolding q by auto
    also have "... = vec_of_poly_n (q * u) n + vec_of_poly_n (smult k r'') n"
      by (rule vec_of_poly_n_add)
    finally show ?thesis unfolding r by simp
  qed
  let ?c = "λi. if i < n - d then coeff q  (n - d - 1 - i) else coeff r (n - Suc i)"
  let ?c1 = "λi. ?c i ⋅v factorization_lattice u (n-d) k ! i"
  show ?thesis
  proof (rule exI[of _ ?c]) 
    let ?part1 = "map (λi. vec_of_poly_n (u * monom 1 i) n) [n-d>..0]"  
    let ?part2 = "map (λi. vec_of_poly_n (monom k i) n) [d>..0]"
    have [simp]: "dim_vec (M.sumlist (map ?c1 [0..<n - d])) = n" 
      by (rule dim_sumlist, auto simp add: dim_factorization_lattice d_def)
    have [simp]: "dim_vec (M.sumlist (map ?c1 [n-d..<n])) = n"
      by (rule dim_sumlist, insert d, auto simp add: dim_factorization_lattice d_def)
    have [simp]: "factorization_lattice u (n-d) k ! x ∈ carrier_vec n" if x: "x < n" for x 
      using x dim_factorization_lattice_element nth_factorization_lattice[of x u "n-d"] d
      by (auto simp: d_def)
    have "[0..<length (factorization_lattice u (n-d) k)] = [0..<n]"
      using d by (simp add: d_def less_imp_le_nat)
    also have "... = [0..<n - d] @ [n-d..<n]"
      by (rule upt_minus_eq_append, auto)
    finally have list_rw: "[0..<length (factorization_lattice u (n-d) k)] = [0..<n - d] @ [n-d..<n]" . 
    have qu1: "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = q*u" 
    proof -
      have "poly_of_vec (M.sumlist (map ?c1 [0..<n - d])) = poly_of_vec (⨁Vi∈{0..<n-d}. ?c1 i)" 
        by (subst sumlist_map_as_finsum, auto)
      also have "... = poly_of_vec (⨁Vi∈set [0..<n-d]. ?c1 i)" by auto
      also have "... = sum (λi. poly_of_vec (?c1 i)) (set [0..<n-d])" 
        by (auto simp:poly_of_vec_finsum)
      also have "... = sum (λi. poly_of_vec (?c1 i)) {0..<n-d}" by auto
      also have "... = q*u"
      proof -
        have deg: "degree (u * monom 1 (n - Suc (d + i))) < n" if i: "i < n - d" for i
        proof -
          let ?m="monom (1::int) (n - Suc (d + i))"
          have monom_not0: "?m ≠ 0" using i by auto
          have deg_m: "degree ?m = n - Suc (d + i)" by (rule degree_monom_eq, auto)
          have "degree (u * ?m) = d + (n - Suc (d + i))"
            using degree_mult_eq[OF u_not0 monom_not0] d_def deg_m by auto
          also have "... < n" using i by auto
          finally show ?thesis .
        qed
        have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n" 
          if i: "i< n - d" for i apply (subst nth_factorization_lattice) using i by (auto simp:d_def)
        have q_rw: "q = (∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))"          
        proof (auto simp add: poly_eq_iff coeff_sum)
          fix j 
          let ?m = "n-d-1-j"
          let ?f = "λx. coeff q (n - Suc (d + x)) * (if n - Suc (d + x) = j then 1 else 0)"          
          have set_rw: "{0..<n-d} = insert ?m ({0..<n-d} - {?m})" using d by auto
          have sum0: "(∑x ∈ {0..<n-d} - {?m}. ?f x) = 0" by (rule sum.neutral, auto)
          have "(∑x = 0..<n - d. ?f x) = (∑x ∈ insert ?m ({0..<n-d} - {?m}). ?f x)" 
            using set_rw by presburger
          also have "... = ?f ?m + (∑x ∈ {0..<n-d} - {?m}. ?f x)" by (rule sum.insert, auto)
          also have "... = ?f ?m" unfolding sum0 by auto
          also have "... = coeff q j"
          proof (cases "j < n - d")
            case True
            then show ?thesis by auto
          next
            case False
            have "j>degree q" using degree_q q False d by auto
            then show ?thesis using coeff_eq_0 by auto
          qed            
          finally show "coeff q j = (∑i = 0..<n - d. coeff q (n - Suc (d + i)) 
            * (if n - Suc (d + i) = j then 1 else 0))" ..
        qed
        have "sum (λi. poly_of_vec (?c1 i)) {0..<n-d} 
        = (∑i = 0..<n - d. poly_of_vec (coeff q (n - Suc (d + i)) ⋅v factorization_lattice u (n-d) k ! i))"
          by (rule sum.cong, auto)
        also have "...  = (∑i = 0..<n - d. (poly_of_vec (coeff q (n - Suc (d + i)) 
          ⋅v (vec_of_poly_n (u * monom 1 (n - Suc (d + i))) n))))"
          by (rule sum.cong, auto simp add: lattice_rw)
        also have "... = (∑i = 0..<n - d. smult (coeff q (n - Suc (d + i))) (u * monom 1 (n - Suc (d + i))))"
          by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg])
        also have "... = (∑i = 0..<n - d. u*(smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" 
          by auto
        also have "... = u *(∑i = 0..<n - d. (smult (coeff q (n - Suc (d + i))) (monom 1 (n - Suc (d + i)))))" 
          by (rule sum_distrib_left[symmetric])
        also have "... = u * q" using q_rw by auto
        also have "... = q*u" by auto
        finally show ?thesis .
      qed
      finally show ?thesis .
    qed
    have qu: "M.sumlist (map ?c1 [0..<n - d]) = vec_of_poly_n (q*u) n"
    proof -
      have "vec_of_poly_n (q*u) n = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n" 
        using qu1 by auto
      also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [0..<n - d]))) n 
        = M.sumlist (map ?c1 [0..<n - d])"
        by (rule vec_of_poly_n_poly_of_vec, auto)
      finally show ?thesis ..
    qed
    have rm1: "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = smult k r"
    proof -      
      have "poly_of_vec (M.sumlist (map ?c1 [n-d..<n])) = poly_of_vec (⨁Vi∈{n-d..<n}. ?c1 i)" 
        by (subst sumlist_map_as_finsum, auto)
      also have "... = poly_of_vec (⨁Vi∈set [n-d..<n]. ?c1 i)" by auto
      also have "... = sum (λi. poly_of_vec (?c1 i)) {n-d..<n}" 
        by (auto simp: poly_of_vec_finsum)
      also have "... = smult k r"
      proof -
        have deg: "degree (monom k (n - Suc i)) < n" if i: "n-d≤i" and i2: "i<n" for i 
          using degree_monom_le i i2
          by (simp add: degree_monom_eq k_not0)
        have lattice_rw: "factorization_lattice u (n-d) k ! i = vec_of_poly_n (monom k (n - Suc i)) n" 
          if i: "n - d ≤ i" and i2: "i<n" for i
          using i2 i d d_def
          by (subst nth_factorization_lattice, auto)
        have r_rw: "r = (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))"
        proof (auto simp add: poly_eq_iff coeff_sum)
          fix j
          show "coeff r j = (∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0)"
          proof (cases "j<d")
            case True
            have j_eq: "n - Suc (n - 1 - j) = j" using d True by auto
            let ?i = "n-1-j"
            let ?f ="λi. if n - Suc i = j then coeff r (n - Suc i) else 0"
            have sum0: "sum ?f ({n-d..<n} - {?i}) = 0" by (rule sum.neutral, auto)
            have "{n-d..<n} = insert ?i ({n-d..<n} - {?i})" using True by auto
            hence "sum ?f {n - d..<n} = sum ?f (insert ?i ({n-d..<n} - {?i}))" by auto
            also have "... = ?f ?i + sum ?f ({n-d..<n} - {?i})"
              by (rule sum.insert, auto)
            also have "... = coeff r j" unfolding sum0 j_eq by simp
            finally show ?thesis ..
          next
            case False
            hence "(∑i = n - d..<n. if n - Suc i = j then coeff r (n - Suc i) else 0) = 0"
              by (intro sum.neutral ballI, insert False, simp, linarith) 
            also have "... = coeff r j" 
              by (rule coeff_eq_0[symmetric], insert False deg_r'' r d_def, auto)
            finally show ?thesis ..
          qed 
        qed
        have "sum (λi. poly_of_vec (?c1 i)) {n-d..<n} 
        = (∑i ∈ {n-d..<n}. poly_of_vec (coeff r (n - Suc i) ⋅v factorization_lattice u (n-d) k ! i))"
          by (rule sum.cong, auto)
        also have "...  = (∑i ∈ {n-d..<n}. (poly_of_vec (coeff r (n - Suc i) 
          ⋅v vec_of_poly_n (monom k (n - Suc i)) n)))"
          by (rule sum.cong, auto simp add: lattice_rw)
        also have "... = (∑i ∈ {n-d..<n}. smult (coeff r (n - Suc i)) (monom k (n - Suc i)))"
          by (rule sum.cong, auto simp add: poly_of_vec_scalar_mult[OF deg])
        also have "... = (∑i ∈ {n-d..<n}. smult k (monom (coeff r (n - Suc i)) (n - Suc i)))"
          by (rule sum.cong, auto simp add: smult_monom smult_sum2)
        also have "... = smult k (∑i ∈ {n-d..<n}. (monom (coeff r (n - Suc i)) (n - Suc i)))"
          by (simp add: smult_sum2)
        also have "... = smult k r" using r_rw by auto
        finally show ?thesis .
      qed
      finally show ?thesis .
    qed
    have rm: "(M.sumlist (map ?c1 [n-d..<n])) = vec_of_poly_n (smult k r) n"
    proof -
      have "vec_of_poly_n (smult k r) n 
        = vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n" 
        using rm1 by auto
      also have "vec_of_poly_n (poly_of_vec (M.sumlist (map ?c1 [n-d..<n]))) n 
        = M.sumlist (map ?c1 [n-d..<n])"
        by (rule vec_of_poly_n_poly_of_vec, auto)
      finally show ?thesis ..        
    qed
    have "lincomb_list ?c (factorization_lattice u (n-d) k) = M.sumlist (map ?c1 ([0..<n - d] @ [n-d..<n]))"
      unfolding lincomb_list_def list_rw by auto
    also have "... = M.sumlist (map ?c1 [0..<n - d] @ map ?c1 [n-d..<n])" by auto
    also have "... = M.sumlist (map ?c1 [0..<n - d]) + M.sumlist (map ?c1 [n-d..<n])" 
      using d by (auto simp add: d_def nth_factorization_lattice intro!: M.sumlist_append)
    also have "... = vec_of_poly_n (q*u) n + vec_of_poly_n (smult k r) n" 
      unfolding qu rm by auto
    also have "... = g" using g2 by simp
    finally show "lincomb_list ?c (factorization_lattice u (n-d) k) = g" .
  qed
qed

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

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

subsection ‹Soundness of the LLL factorization algorithm›

lemma LLL_short_polynomial: assumes deg_u_0: "degree u ≠ 0" and deg_le: "degree u ≤ n" 
  and pl1: "pl > 1" 
  and monic: "monic u" 
shows "degree (LLL_short_polynomial pl n u) < n" 
  and "LLL_short_polynomial pl n u ≠ 0"
  and "poly_mod.dvdm pl u (LLL_short_polynomial pl n u)" 
  and "degree u < n ⟹ f ≠ 0 ⟹
    poly_mod.dvdm pl u f ⟹ degree f < n ⟹ ∥LLL_short_polynomial pl n u∥2 ≤ 2 ^ (n - 1) * ∥f∥2" 
proof -
  interpret poly_mod_2 pl 
    by (unfold_locales, insert pl1, auto)
  from pl1 have pl0: "pl ≠ 0" by auto
  let ?d = "degree u"
  let ?u = "Mp u" 
  let ?iu = "inv_Mp ?u" 
  from Mp_inv_Mp_id[of ?u] have "?iu =m ?u" .
  also have "… =m u" by simp
  finally have iu_u: "?iu =m u" by simp
  have degu[simp]: "degree ?u = degree u" using monic by simp
  have mon: "monic ?u" using monic by (rule monic_Mp)
  have "degree ?iu = degree ?u" unfolding inv_Mp_def
    by (rule degree_map_poly, unfold mon, insert mon pl1, auto simp: inv_M_def)
  with degu have deg_iu: "degree ?iu = degree u" by simp
  have mon_iu: "monic ?iu" unfolding deg_iu unfolding inv_Mp_def Mp_def inv_M_def M_def
    by (insert pl1, auto simp: coeff_map_poly monic)
  let ?L = "factorization_lattice ?iu (n - ?d) pl" 
  let ?sv = "short_vector_hybrid 2 ?L" 
  from deg_u_0 deg_le have n: "n ≠ 0" by auto
  from deg_u_0 have u0: "u ≠ 0" by auto
  have id: "LLL_short_polynomial pl n u = poly_of_vec ?sv" 
    unfolding LLL_short_polynomial_def by blast
  have id': "∥?sv∥2 = ∥LLL_short_polynomial pl n u∥2" unfolding id by simp
  interpret vec_module "TYPE(int)" n.
  interpret L: LLL n n "?L" 2 .
  from deg_le deg_iu have deg_iu_le: "degree ?iu ≤ n" by simp
  have len: "length ?L = n" 
    unfolding factorization_lattice_def using deg_le deg_iu by auto
  from deg_u_0 deg_iu have deg_iu0: "degree ?iu ≠ 0" by auto
  hence iu0: "?iu ≠ 0" by auto
  from L.lin_indpt_list_factorization_lattice[OF refl deg_iu_le iu0 pl0]
  have *: "4/3 ≤ (2 :: rat)" "L.gs.lin_indpt_list (L.RAT ?L)" by (auto simp: deg_iu)
  interpret L: LLL_with_assms n n ?L 2
    by (unfold_locales, insert *, auto simp: deg_iu deg_le)
  note short = L.short_vector_hybrid[OF refl n, unfolded id' L.L_def]
  from short(2) have mem: "LLL_short_polynomial pl n u ∈ poly_of_vec ` lattice_of ?L" 
    unfolding id by auto
  note fact = L.factorization_lattice(1)[OF deg_iu0 pl0 deg_iu_le n, unfolded deg_iu, OF mem]
  show "degree (LLL_short_polynomial pl n u) < n" using fact by auto
  from fact have "?iu dvdm (LLL_short_polynomial pl n u)" by auto
  then obtain h where "LLL_short_polynomial pl n u =m ?iu * h" unfolding dvdm_def by auto
  also have "?iu * h =m Mp ?iu * h" unfolding mult_Mp by simp
  also have "Mp ?iu * h =m u * h" unfolding iu_u unfolding mult_Mp by simp
  finally show "u dvdm (LLL_short_polynomial pl n u)" unfolding dvdm_def by auto
  from short have sv1: "?sv ∈ carrier_vec n" by auto  
  from short have "?sv ≠ 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: "∥fv∥2 = ∥f∥2" 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 u∥2 ≤ rat_of_int (2 ^ (n - 1) * ∥f∥2)" by simp
  thus "∥LLL_short_polynomial pl n u∥2 ≤ 2 ^ (n - 1) * ∥f∥2" by linarith
qed

context LLL_implementation
begin

lemma LLL_reconstruction: assumes "LLL_reconstruction f us = fs"
  and "degree f ≠ 0"
  and "poly_mod.unique_factorization_m pl f (lead_coeff f, mset us)"
  and "f dvd F" 
  and "⋀ ui. ui ∈ set us ⟹ poly_mod.Mp pl ui = ui" 
  and F0: "F ≠ 0" 
  and cop: "coprime (lead_coeff F) p" 
  and sf: "poly_mod.square_free_m p F" 
  and pl1: "pl > 1" 
  and plp: "pl = p^l" 
  and p: "prime p" 
  and large: "2^(5 * (degree F - 1) * (degree F - 1)) * ∥F∥2^(2 * (degree F - 1)) < 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 "∥g∥2 ≤ 2 ^ (?n - 1) * ∥f1∥2" unfolding g_def
          by (rule short_main(4)[OF deg_uf _ uf1], insert deg, auto)
        also have "… ≤ 2 ^ (?n - 1) * (2 ^ (2 * degree f1) * ∥F∥2)" 
          by (rule mult_left_mono[OF sq_norm_factor_bound[OF f1F F0]], simp)
        also have "… = 2 ^ ((?n - 1) + 2 * degree f1) * ∥F∥2" 
          unfolding power_add by simp
        also have "… ≤ 2 ^ ((?n - 1) + 2 * (?n - 1)) * ∥F∥2" 
          by (rule mult_right_mono, insert deg(3), auto)
        also have "… = 2 ^ (3 * (?n - 1)) * ∥F∥2" by simp
        finally have ineq_g: "∥g∥2 ≤ 2 ^ (3 * (?n - 1)) * ∥F∥2" .
        from power_mono[OF this, of ?n1]
        have ineq1: "∥g∥2 ^ ?n1 ≤ (2 ^ (3 * (?n - 1)) * ∥F∥2)^?n1" by auto
        from F0 have normF: "∥F∥2 ≥ 1" using sq_norm_poly_pos[of F] by presburger
        from g0 have normg: "∥g∥2 ≥ 1" using sq_norm_poly_pos[of g] by presburger
        from f0 have normf: "∥f∥2 ≥ 1" using sq_norm_poly_pos[of f] by presburger
        from f1_0 have normf1: "∥f1∥2 ≥ 1" using sq_norm_poly_pos[of f1] by presburger
        from power_mono[OF sq_norm_factor_bound[OF f1F F0], of "degree g"]
        have ineq2: "∥f1∥2 ^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥2) ^ degree g" by auto
        also have "… ≤ (2 ^ (2 * ?n1) * ∥F∥2) ^ (?n - 1)"
          by (rule pow_mono_exp, insert deg_gf normF, auto)          
        finally have ineq2: "∥f1∥2 ^ degree g ≤ (2 ^ (2 * ?n1) * ∥F∥2) ^ (?n - 1)" .
        have nN: "?n ≤ ?N" using fF F0 by (metis dvd_imp_degree_le)
        from deg nN have n1N: "?n1 ≤ ?N - 1" by auto
        have "∥f1∥2 ^ degree g * ∥g∥2 ^ ?n1 ≤ 
          (2 ^ (2 * ?n1) * ∥F∥2) ^ (?n - 1) * (2 ^ (3 * (?n - 1)) * ∥F∥2)^?n1" 
          by (rule mult_mono[OF ineq2 ineq1], force+)
        also have "… ≤ (2 ^ (2 * (?N - 1)) * ∥F∥2) ^ (?N - 1) *
          (2 ^ (3 * (?N - 1)) * ∥F∥2) ^ (?N - 1)"
          by (rule mult_mono[OF power_both_mono[OF _ _ mult_mono] 
          power_both_mono], insert normF n1N nN, auto intro: power_both_mono mult_mono) 
        also have "… = 2 ^ (2 * (?N -1) * (?N - 1) + 3 * (?N - 1) * (?N - 1)) 
            * (∥F∥2)^((?N - 1) + (?N - 1))" 
          unfolding power_mult_distrib power_add power_mult by simp
        also have "2 * (?N - 1) * (?N - 1) + 3 * (?N - 1) * (?N - 1) = 5 * (?N - 1) * (?N - 1)" by simp
        also have "?N - 1 + (?N - 1) = 2 * (?N - 1)" by simp
        also have "2^(5 * (?N - 1) * (?N - 1)) * ∥F∥2^(2 * (?N - 1)) < pl^2" by (rule large)
        finally have large: "∥f1∥2 ^ degree g * ∥g∥2 ^ degree f1 < 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 "… ≤ ∥g∥2 ^ 1" using coeff_le_sq_norm[of g] by auto 
          also have "… ≤ ∥g∥2 ^ degree f1" 
            by (rule pow_mono_exp, insert deg normg, auto)
          also have "… = 1 * …" by simp
          also have "… ≤ ∥f1∥2 ^ degree g * ∥g∥2 ^ degree f1" 
            by (rule mult_right_mono, insert normf1, auto)
          also have "… < 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)) * ∥F∥2^(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: "∥F∥2 ≥ 1" using sq_norm_poly_pos[of F] by presburger
        have g0: "?g ≠ 0" using short(2) .
        from g0 have normg: "∥?g∥2 ≥ 1" using sq_norm_poly_pos[of "?g"] by presburger
        from f10 have normf1: "∥f1∥2 ≥ 1" using sq_norm_poly_pos[of f1] by presburger
        from fF f have f1F: "f1 dvd F" unfolding dvd_def by auto
        have pl_ge0: "pl ≥ 0" using pl.poly_mod_2_axioms poly_mod_2_def by auto
        from fF have "degree f ≤ degree F" using F0 f0 by (metis dvd_imp_degree_le)
        hence d2D2: "?d2 ≤ ?D2" by simp
        with deg12(3) have df1_D2: "degree f1 ≤ ?D2" by linarith
        from short(1) d2D2 have dg_D2: "degree (gg u) ≤ ?D2" by linarith
        have "∥f1∥2 ^ degree (gg u) * ∥gg u∥2 ^ degree f1
          ≤ ∥f1∥2 ^ ?D2 * ∥gg u∥2 ^ ?D2" 
          by (rule mult_mono[OF pow_mono_exp pow_mono_exp], 
              insert normf1 normg, auto intro: df1_D2 dg_D2)
        also have "… = (∥f1∥2 * ∥gg u∥2)^?D2" 
          by (simp add: power_mult_distrib)
        also have "… ≤ (∥f1∥2 * (2^?D2 * ∥f1∥2))^?D2" 
          by (rule power_mono[OF mult_left_mono[OF order.trans[OF short(4)[OF f10 u_f1]]]],
            insert deg12 d2D2, auto intro!: mult_mono)
        also have "… = ∥f1∥2 ^ (?D2 + ?D2) * 2^(?D2 * ?D2)"
          unfolding power_add power_mult_distrib power_mult by simp
        also have "… ≤ (2 ^ (2 * ?D2) * ∥F∥2) ^ (?D2 + ?D2) * 2^(?D2 * ?D2)" 
          by (rule mult_right_mono[OF order.trans[OF power_mono[OF sq_norm_factor_bound[OF f1F F0]]]], 
            auto intro!: power_mono mult_right_mono df1_D2)
        also have "… = 2 ^ (2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2) * ∥F∥2 ^ (?D2 + ?D2)" 
          unfolding power_mult_distrib power_mult power_add by simp
        also have "2 * ?D2 * (?D2 + ?D2) + ?D2 * ?D2 = 5 * ?D2 * ?D2" by simp
        also have "?D2 + ?D2 = 2 * ?D2" by simp
        finally have large: 
          "∥f1∥2 ^ degree (gg u) * ∥gg u∥2 ^ degree f1 < pl^2" using large by simp
        have "degree u ≤ degree (?g)" 
        proof (rule pl.dvdm_degree[OF mon_u short(3)], standard)
          assume "pl.Mp (?g) = 0" 
          from arg_cong[OF this, of "λ p. coeff p (degree ?g)"]
          have "pl.M (coeff ?g (degree ?g)) = 0" by (auto simp: pl.Mp_def coeff_map_poly)
          from this[unfolded pl.M_def] obtain c where lg: "lead_coeff ?g = pl * c" by auto
          with g0 have c0: "c ≠ 0" by auto
          hence "pl^2 ≤ (lead_coeff ?g)^2" unfolding lg abs_le_square_iff[symmetric]
            by (rule aux_abs_int)
          also have "… ≤ ∥?g∥2" using coeff_le_sq_norm[of ?g] by auto 
          also have "… = ∥?g∥2 ^ 1" by simp
          also have "… ≤ ∥?g∥2 ^ degree f1" 
            by (rule pow_mono_exp, insert deg12 normg, auto)
          also have "… = 1 * …" by simp
          also have "… ≤ ∥f1∥2 ^ degree ?g * ∥?g∥2 ^ degree f1" 
            by (rule mult_right_mono, insert normf1, auto)
          also have "… < 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 ≤ ∥f1∥2 ^ degree (gg u) * ∥gg u∥2 ^ degree f1" by linarith
        also have "… < pl^2" by (rule large)
        finally show False by simp
      qed
      thus ?thesis using fs_f by simp
    qed
  qed
qed

end

lemma LLL_factorization:
  assumes res: "LLL_factorization f = gs"
  and sff: "square_free f"
  and deg: "degree f ≠ 0" 
  shows "f = prod_list gs ∧ (∀g∈set gs. 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)) * ∥f∥2^(2 * (degree f - 1))"
  define N where "N = sqrt_int_ceiling K" 
  have K0: "K ≥ 0" unfolding K_def by fastforce
  have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 
    by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling)
  define n where "n = find_exponent p N" 
  note res = res[folded n_def[unfolded N_def K_def]]
  note n = find_exponent[OF p.m1, of N, folded n_def]
  note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)]
  from deg have f0: "f ≠ 0" by auto
  from n p.m1 have pn1: "p ^ n > 1" by auto
  note res = res[folded bh(1)]
  note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] 
  note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff]
  from res * **
  have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" 
    and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" 
    unfolding berlekamp_hensel_def fff split by auto
  have K: "K < (p ^ n)2" using n sqrt_int_ceiling_bound[OF K0] 
    by (smt N0 N_def n(1) power2_le_imp_le)
  show ?thesis
    by (rule LLL_implementation.LLL_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 
          refl prime K[unfolded K_def]]) 
qed

lemma LLL_many_factorization:
  assumes res: "LLL_many_factorization f = gs"
  and sff: "square_free f"
  and deg: "degree f ≠ 0" 
  shows "f = prod_list gs ∧ (∀g∈set gs. 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)) * ∥f∥2^(2 * (degree f div 2))"
  define N where "N = sqrt_int_ceiling K" 
  have K0: "K ≥ 0" unfolding K_def by fastforce
  have N0: "N ≥ 0" unfolding N_def sqrt_int_ceiling using K0 
    by (smt of_int_nonneg real_sqrt_ge_0_iff zero_le_ceiling)
  define n where "n = find_exponent p N" 
  note res = res[folded n_def[unfolded N_def K_def]]
  note n = find_exponent[OF p.m1, of N, folded n_def]
  note bh = p.berlekamp_and_hensel_separated(1)[OF cop sf refl fff n(2)]
  from deg have f0: "f ≠ 0" by auto
  from n p.m1 have pn1: "p ^ n > 1" by auto
  note res = res[folded bh(1)]
  note * = p.berlekamp_hensel_unique[OF cop sf bh n(2)] 
  note ** = p.berlekamp_hensel_main[OF n(2) bh cop sf fff]
  from res * **
  have uf: "poly_mod.unique_factorization_m (p ^ n) f (lead_coeff f, mset (berlekamp_hensel p n f))" 
    and norm: "⋀ui. ui ∈ set (berlekamp_hensel p n f) ⟹ poly_mod.Mp (p ^ n) ui = ui" 
    unfolding berlekamp_hensel_def fff split by auto
  have K: "K < (p ^ n)2" using n sqrt_int_ceiling_bound[OF K0] 
    by (smt N0 N_def n(1) power2_le_imp_le)
  show ?thesis
    by (rule LLL_implementation.LLL_many_reconstruction[OF res deg uf dvd_refl norm f0 cop sf pn1 
          refl prime K[unfolded K_def]]) 
qed

lift_definition one_lattice_LLL_factorization :: int_poly_factorization_algorithm
  is LLL_factorization using LLL_factorization by auto

lift_definition many_lattice_LLL_factorization :: int_poly_factorization_algorithm
  is LLL_many_factorization using LLL_many_factorization by auto

lemma LLL_factorization_primitive: assumes "LLL_factorization f = fs"
  "square_free f" 
  "0 < degree f" 
  "primitive f" 
shows "f = prod_list fs ∧ (∀fi∈set fs. irreducible fi ∧ 0 < degree fi ∧ primitive fi)" 
  using assms(1)
  by (intro int_poly_factorization_algorithm_irreducible[of one_lattice_LLL_factorization, 
      OF _ assms(2-)], transfer, auto)
 
thm factorize_int_poly[of one_lattice_LLL_factorization]
thm factorize_int_poly[of many_lattice_LLL_factorization]
end