Theory LLL

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

section ‹The LLL Algorithm›

text ‹Soundness of the LLL algorithm is proven in four steps. 
  In the basic version, we do recompute the Gram-Schmidt ortogonal (GSO) basis 
  in every step. This basic version will have a full functional soundness proof, 
  i.e., termination and the property that the returned basis is reduced.
  Then in LLL-Number-Bounds we will strengthen the invariant and prove that
  all intermediate numbers stay polynomial in size.
  Moreover, in LLL-Impl we will refine the basic version, so that
  the GSO does not need to be recomputed in every step. 
  Finally, in LLL-Complexity, we develop an cost-annotated version
  of the refined algorithm and prove a polynomial upper bound on the 
  number of arithmetic operations.› 


text ‹This theory provides a basic implementation and a soundness proof of the LLL algorithm
      to compute a "short" vector in a lattice.› 

theory LLL
  imports 
    Gram_Schmidt_2 
    Missing_Lemmas 
    Jordan_Normal_Form.Determinant 
    "Abstract-Rewriting.SN_Order_Carrier"
begin

subsection ‹Core Definitions, Invariants, and Theorems for Basic Version›

(* Note/TODO by Max Haslbeck:
  Up to here I refactored the code in Gram_Schmidt_2 and Gram_Schmidt_Int which now makes heavy
  use of locales. In the future I would also like to do this here (instead of using LLL_invariant
  everywhere). *)

locale LLL =
  fixes n :: nat (* n-dimensional vectors, *)
    and m :: nat (* number of vectors *)
    and fs_init :: "int vec list" (* initial basis *)
    and α :: rat (* approximation factor *)

begin

sublocale vec_module "TYPE(int)" n.




abbreviation RAT where "RAT  map (map_vec rat_of_int)" 
abbreviation SRAT where "SRAT xs  set (RAT xs)" 
abbreviation Rn where "Rn  carrier_vec n :: rat vec set" 

sublocale gs: gram_schmidt_fs n "RAT fs_init" .

abbreviation lin_indep where "lin_indep fs  gs.lin_indpt_list (RAT fs)" 
abbreviation gso where "gso fs  gram_schmidt_fs.gso n (RAT fs)"
abbreviation μ where "μ fs  gram_schmidt_fs.μ n (RAT fs)"

abbreviation reduced where "reduced fs  gram_schmidt_fs.reduced n (RAT fs) α" 
abbreviation weakly_reduced where "weakly_reduced fs  gram_schmidt_fs.weakly_reduced n (RAT fs) α" 
  
text ‹lattice of initial basis›
definition "L = lattice_of fs_init" 

text ‹maximum squared norm of initial basis›
definition "N = max_list (map (nat  sq_norm) fs_init)" 

text ‹maximum absolute value in initial basis›
definition "M = Max ({abs (fs_init ! i $ j) | i j. i < m  j < n}  {0})" 

text ‹This is the core invariant which enables to prove functional correctness.›

definition "μ_small fs i = ( j < i. abs (μ fs i j)  1/2)" 

definition LLL_invariant_weak :: "int vec list  bool" where
  "LLL_invariant_weak fs = (
    gs.lin_indpt_list (RAT fs)  
    lattice_of fs = L 
    length fs = m)"

lemma LLL_inv_wD: assumes "LLL_invariant_weak fs"
  shows 
  "lin_indep fs" 
  "length (RAT fs) = m" 
  "set fs  carrier_vec n"
  " i. i < m  fs ! i  carrier_vec n" 
  " i. i < m  gso fs i  carrier_vec n" 
  "length fs = m"
  "lattice_of fs = L" 
proof (atomize (full), goal_cases)
  case 1
  interpret gs': gram_schmidt_fs_lin_indpt n "RAT fs"
    by (standard) (use assms LLL_invariant_weak_def gs.lin_indpt_list_def in auto)
  show ?case
    using assms gs'.fs_carrier gs'.f_carrier gs'.gso_carrier
    by (auto simp add: LLL_invariant_weak_def gram_schmidt_fs.reduced_def)
qed

lemma LLL_inv_wI: assumes  
  "set fs  carrier_vec n"
  "length fs = m"
  "lattice_of fs = L" 
  "lin_indep fs" 
shows "LLL_invariant_weak fs" 
  unfolding LLL_invariant_weak_def Let_def using assms by auto

definition LLL_invariant :: "bool  nat  int vec list  bool" where 
  "LLL_invariant upw i fs = ( 
    gs.lin_indpt_list (RAT fs)  
    lattice_of fs = L 
    reduced fs i 
    i  m  
    length fs = m 
    (upw  μ_small fs i)    
  )" 

lemma LLL_inv_imp_w: "LLL_invariant upw i fs  LLL_invariant_weak fs" 
  unfolding LLL_invariant_def LLL_invariant_weak_def by blast 

lemma LLL_invD: assumes "LLL_invariant upw i fs"
  shows 
  "lin_indep fs" 
  "length (RAT fs) = m" 
  "set fs  carrier_vec n"
  " i. i < m  fs ! i  carrier_vec n" 
  " i. i < m  gso fs i  carrier_vec n" 
  "length fs = m"
  "lattice_of fs = L" 
  "weakly_reduced fs i"
  "i  m"
  "reduced fs i" 
  "upw  μ_small fs i"
proof (atomize (full), goal_cases)
  case 1
  interpret gs': gram_schmidt_fs_lin_indpt n "RAT fs"
    by (standard) (use assms LLL_invariant_def gs.lin_indpt_list_def in auto)
  show ?case
    using assms gs'.fs_carrier gs'.f_carrier gs'.gso_carrier
    by (auto simp add: LLL_invariant_def gram_schmidt_fs.reduced_def)
qed

lemma LLL_invI: assumes  
  "set fs  carrier_vec n"
  "length fs = m"
  "lattice_of fs = L" 
  "i  m"
  "lin_indep fs" 
  "reduced fs i" 
  "upw  μ_small fs i" 
shows "LLL_invariant upw i fs" 
  unfolding LLL_invariant_def Let_def split using assms by auto



end

locale fs_int' =
  fixes n m fs_init fs 
  assumes LLL_inv: "LLL.LLL_invariant_weak n m fs_init fs"

sublocale fs_int'  fs_int_indpt
   using LLL_inv unfolding LLL.LLL_invariant_weak_def by (unfold_locales) blast

context LLL
begin

lemma gso_cong: assumes " i. i  x  f1 ! i = f2 ! i"
   "x < length f1" "x < length f2" 
  shows "gso f1 x = gso f2 x"
  by (rule gs.gso_cong, insert assms, auto)
  
lemma μ_cong: assumes " k. j < i  k  j  f1 ! k = f2 ! k"
  and i: "i < length f1" "i < length f2" 
  and "j < i  f1 ! i = f2 ! i" 
  shows "μ f1 i j = μ f2 i j"
  by (rule gs.μ_cong, insert assms, auto)
    
definition reduction where "reduction = (4+α)/(4*α)"


definition d :: "int vec list  nat  int" where "d fs k = gs.Gramian_determinant fs k"
definition D :: "int vec list  nat" where "D fs = nat ( i < m. d fs i)" 

definition " gs i j = int_of_rat (of_int (d gs (Suc j)) * μ gs i j)" 

definition logD :: "int vec list  nat"
  where "logD fs = (if α = 4/3 then (D fs) else nat (floor (log (1 / of_rat reduction) (D fs))))" 

definition LLL_measure :: "nat  int vec list  nat" where 
  "LLL_measure i fs = (2 * logD fs + m - i)" 

context
  fixes fs
  assumes Linv: "LLL_invariant_weak fs"
begin

interpretation fs: fs_int' n m fs_init fs
  by (standard) (use Linv in auto)

lemma Gramian_determinant:
  assumes k: "k  m" 
shows "of_int (gs.Gramian_determinant fs k) = ( j<k. sq_norm (gso fs j))" (is ?g1)
  "gs.Gramian_determinant fs k > 0" (is ?g2)
  using assms fs.Gramian_determinant LLL_inv_wD[OF Linv]  by auto
   
lemma LLL_d_pos [intro]: assumes k: "k  m" 
shows "d fs k > 0"
  unfolding d_def using fs.Gramian_determinant k LLL_inv_wD[OF Linv] by auto

lemma LLL_d_Suc: assumes k: "k < m" 
shows "of_int (d fs (Suc k)) = sq_norm (gso fs k) * of_int (d fs k)" 
  using assms fs.fs_int_d_Suc  LLL_inv_wD[OF Linv] unfolding fs.d_def d_def by auto

lemma LLL_D_pos:
  shows "D fs > 0"
  using fs.fs_int_D_pos LLL_inv_wD[OF Linv] unfolding D_def fs.D_def fs.d_def d_def by auto
end

text ‹Condition when we can increase the value of $i$›

lemma increase_i:
  assumes Linv: "LLL_invariant upw i fs"
  assumes i: "i < m" 
  and upw: "upw  i = 0" 
  and red_i: "i  0  sq_norm (gso fs (i - 1))  α * sq_norm (gso fs i)"
shows "LLL_invariant True (Suc i) fs" "LLL_measure i fs > LLL_measure (Suc i) fs" 
proof -
  note inv = LLL_invD[OF Linv]
  from inv(8,10) have red: "weakly_reduced fs i" 
    and sred: "reduced fs i" by (auto)
  from red red_i i have red: "weakly_reduced fs (Suc i)" 
    unfolding gram_schmidt_fs.weakly_reduced_def
    by (intro allI impI, rename_tac ii, case_tac "Suc ii = i", auto)
  from inv(11) upw have sred_i: " j. j < i  ¦μ fs i j¦  1 / 2" 
    unfolding μ_small_def by auto
  from sred sred_i have sred: "reduced fs (Suc i)"
    unfolding gram_schmidt_fs.reduced_def
    by (intro conjI[OF red] allI impI, rename_tac ii j, case_tac "ii = i", auto)
  show "LLL_invariant True (Suc i) fs" 
    by (intro LLL_invI, insert inv red sred i, auto)
  show "LLL_measure i fs > LLL_measure (Suc i) fs" unfolding LLL_measure_def using i by auto
qed

text ‹Standard addition step which makes $\mu_{i,j}$ small›

definition "μ_small_row i fs j = ( j'. j  j'  j' < i  abs (μ fs i j')  inverse 2)"

lemma basis_reduction_add_row_main: assumes Linv: "LLL_invariant_weak fs"
  and i: "i < m"  and j: "j < i" 
  and fs': "fs' = fs[ i := fs ! i - c v fs ! j]" 
shows "LLL_invariant_weak fs'" 
  "LLL_invariant True i fs  LLL_invariant True i fs'"
  "c = round (μ fs i j)  μ_small_row i fs (Suc j)  μ_small_row i fs' j" (* mu-value at position i j gets small *)
  "c = round (μ fs i j)  abs (μ fs' i j)  1/2" (* mu-value at position i j gets small *)
  "LLL_measure i fs' = LLL_measure i fs" 
  (* new values of gso: no change *)
  " i. i < m  gso fs' i = gso fs i" 
  (* new values of mu *)
  " i' j'. i' < m  j' < m        
     μ fs' i' j' = (if i' = i  j'  j then μ fs i j' - of_int c * μ fs j j' else μ fs i' j')"
  (* new values of d *)
  " ii. ii  m  d fs' ii = d fs ii" 
proof -
  define bnd :: rat where bnd: "bnd = 4 ^ (m - 1 - Suc j) * of_nat (N ^ (m - 1) * m)" 
  define M where "M = map (λi. map (μ fs i) [0..<m]) [0..<m]"
  note inv = LLL_inv_wD[OF Linv]
  note Gr = inv(1)
  have ji: "j  i" "j < m" and jstrict: "j < i" 
    and add: "set fs  carrier_vec n" "i < length fs" "j < length fs" "i  j" 
    and len: "length fs = m" 
    and indep: "lin_indep fs" 
    using inv j i by auto 
  let ?R = rat_of_int
  let ?RV = "map_vec ?R"   
  from inv i j
  have Fij: "fs ! i  carrier_vec n" "fs ! j  carrier_vec n" by auto
  let ?x = "fs ! i - c v fs ! j"  
  let ?g = "gso fs"
  let ?g' = "gso fs'"
  let ?mu = "μ fs"
  let ?mu' = "μ fs'"
  from inv j i 
  have Fi:" i. i < length (RAT fs)  (RAT fs) ! i  carrier_vec n"
    and gs_carr: "?g j  carrier_vec n"
                "?g i  carrier_vec n"
                " i. i < j  ?g i  carrier_vec n"
                " j. j < i  ?g j  carrier_vec n" 
    and len': "length (RAT fs) = m"
    and add':"set (map ?RV fs)  carrier_vec n"
    by auto 
  have RAT_F1: "RAT fs' = (RAT fs)[i := (RAT fs) ! i - ?R c v (RAT fs) ! j]" 
    unfolding fs'
  proof (rule nth_equalityI[rule_format], goal_cases)
    case (2 k)
    show ?case 
    proof (cases "k = i")
      case False
      thus ?thesis using 2 by auto
    next
      case True
      hence "?thesis = (?RV (fs ! i - c v fs ! j) =
          ?RV (fs ! i) - ?R c v ?RV (fs ! j))" 
        using 2 add by auto
      also have "" by (rule eq_vecI, insert Fij, auto)
      finally show ?thesis by simp
    qed
  qed auto
  hence RAT_F1_i:"RAT fs' ! i = (RAT fs) ! i - ?R c v (RAT fs) ! j" (is "_ = _ - ?mui")
    using i len by auto
  have uminus: "fs ! i - c v fs ! j = fs ! i + -c v fs ! j" 
    by (subst minus_add_uminus_vec, insert Fij, auto)
  have "lattice_of fs' = lattice_of fs" unfolding fs' uminus
    by (rule lattice_of_add[OF add, of _ "- c"], auto)
  with inv have lattice: "lattice_of fs' = L" by auto
  from add len
  have "k < length fs  ¬ k  i  fs' ! k  carrier_vec n" for k
    unfolding fs'
    by (metis (no_types, lifting) nth_list_update nth_mem subset_eq carrier_dim_vec index_minus_vec(2) 
        index_smult_vec(2))
  hence "k < length fs  fs' ! k  carrier_vec n" for k
    unfolding fs' using add len by (cases "k  i",auto)
  with len have F1: "set fs'  carrier_vec n" "length fs' = m" unfolding fs' by (auto simp: set_conv_nth)
  hence F1': "length (RAT fs') = m" "SRAT fs'  Rn" by auto
  from indep have dist: "distinct (RAT fs)" by (auto simp: gs.lin_indpt_list_def)
  have Fij': "(RAT fs) ! i  Rn" "(RAT fs) ! j  Rn" using add'[unfolded set_conv_nth] i j < m len by auto
  have uminus': "(RAT fs) ! i - ?R c v (RAT fs) ! j = (RAT fs) ! i + - ?R c v (RAT fs) ! j" 
    by (subst minus_add_uminus_vec[where n = n], insert Fij', auto) 
  have span_F_F1: "gs.span (SRAT fs) = gs.span (SRAT fs')" unfolding RAT_F1 uminus' 
    by (rule gs.add_vec_span, insert len add, auto)
  have **: "?RV (fs ! i) + - ?R c v (RAT fs) ! j =  ?RV (fs ! i - c v fs ! j)"
    by (rule eq_vecI, insert Fij len i j, auto)
  from i j len have "j < length (RAT fs)" "i < length (RAT fs)" "i  j" by auto
  from gs.lin_indpt_list_add_vec[OF this indep, of "- of_int c"]
  have "gs.lin_indpt_list ((RAT fs) [i := (RAT fs) ! i + - ?R c v (RAT fs) ! j])" (is "gs.lin_indpt_list ?F1") .
  also have "?F1 = RAT fs'" unfolding fs' using i len Fij' **
    by (auto simp: map_update)
  finally have indep_F1: "lin_indep fs'" .
  have conn1: "set (RAT fs)  carrier_vec n"  "length (RAT fs) = m" "distinct (RAT fs)"
    "gs.lin_indpt (set (RAT fs))"
    using inv unfolding gs.lin_indpt_list_def by auto
  have conn2: "set (RAT fs')  carrier_vec n"  "length (RAT fs') = m" "distinct (RAT fs')"
    "gs.lin_indpt (set (RAT fs'))"
    using indep_F1 F1' unfolding gs.lin_indpt_list_def by auto
  interpret gs1: gram_schmidt_fs_lin_indpt n "RAT fs"
    by (standard) (use inv gs.lin_indpt_list_def in auto)
  interpret gs2: gram_schmidt_fs_lin_indpt n "RAT fs'"
    by (standard) (use indep_F1 F1' gs.lin_indpt_list_def in auto)
  let ?G = "map ?g [0 ..< m]" 
  let ?G' = "map ?g' [0 ..< m]" 
  from gs1.span_gso gs2.span_gso gs1.gso_carrier gs2.gso_carrier conn1 conn2 span_F_F1 len 
  have span_G_G1: "gs.span (set ?G) = gs.span (set ?G')"
   and lenG: "length ?G = m" 
   and Gi: "i < length ?G  ?G ! i  Rn"
   and G1i: "i < length ?G'  ?G' ! i  Rn" for i
    by auto
  have eq: "x  i  RAT fs' ! x = (RAT fs) ! x" for x unfolding RAT_F1 by auto
  hence eq_part: "x < i  ?g' x = ?g x" for x
    by (intro gs.gso_cong, insert len, auto)
  have G: "i < m  (RAT fs) ! i  Rn"
       "i < m  fs ! i  carrier_vec n" for i by(insert add len', auto)
  note carr1[intro] = this[OF i] this[OF ji(2)]
  have "x < m  ?g x  Rn" 
       "x < m  ?g' x  Rn"
       "x < m  dim_vec (gso fs x) = n"
       "x < m  dim_vec (gso fs' x) = n"
       for x using inv G1i by (auto simp:o_def Gi G1i)
  hence carr2[intro!]:"?g i  Rn" "?g' i  Rn"
                 "?g ` {0..<i}  Rn"
                 "?g ` {0..<Suc i}  Rn" using i by auto
  have F1_RV: "?RV (fs' ! i) = RAT fs' ! i" using i F1 by auto
  have F_RV: "?RV (fs ! i) = (RAT fs) ! i" using i len by auto
  from eq_part 
  have span_G1_G: "gs.span (?g' ` {0..<i}) = gs.span (?g ` {0..<i})" (is "?ls = ?rs")
    apply(intro cong[OF refl[of "gs.span"]],rule image_cong[OF refl]) using eq by auto
  have "(RAT fs') ! i - ?g' i = ((RAT fs) ! i - ?g' i) - ?mui"
    unfolding RAT_F1_i using carr1 carr2
    by (intro eq_vecI, auto)
  hence in1:"((RAT fs) ! i - ?g' i) - ?mui  ?rs"
    using gs2.oc_projection_exist[of i] conn2 i unfolding span_G1_G by auto
  from j < i have Gj_mem: "(RAT fs) ! j  (λ x. ((RAT fs) ! x)) ` {0 ..< i}" by auto  
  have id1: "set (take i (RAT fs)) = (λx. ?RV (fs ! x)) ` {0..<i}"
    using i < m len
    by (subst nth_image[symmetric], force+)
  have "(RAT fs) ! j  ?rs  (RAT fs) ! j  gs.span ((λx. ?RV (fs ! x)) ` {0..<i})"
    using gs1.partial_span  i < m id1 inv by auto
  also have "(λx. ?RV (fs ! x)) ` {0..<i} = (λx. ((RAT fs) ! x)) ` {0..<i}" using i < m len by force
  also have "(RAT fs) ! j  gs.span "
    by (rule gs.span_mem[OF _ Gj_mem], insert i < m G, auto)
  finally have "(RAT fs) ! j  ?rs" .
  hence in2:"?mui  ?rs"
    apply(intro gs.prod_in_span) by force+
  have ineq:"((RAT fs) ! i - ?g' i) + ?mui - ?mui = ((RAT fs) ! i - ?g' i)"
    using carr1 carr2 by (intro eq_vecI, auto)
  have cong': "A = B  A  C  B  C" for A B :: "'a vec" and C by auto
  have *: "?g ` {0..<i}  Rn" by auto
  have in_span: "(RAT fs) ! i - ?g' i  ?rs"
    by (rule cong'[OF eq_vecI gs.span_add1[OF * in1 in2,unfolded ineq]], insert carr1 carr2, auto)
  { 
    fix x assume x:"x < i" hence "x < m" "i  x" using i by auto
    from gs2.orthogonal this inv assms
    have "?g' i  ?g' x = 0" by auto
  }
  hence G1_G: "?g' i = ?g i"
    by (intro gs1.oc_projection_unique) (use inv i eq_part in_span in auto)
  show eq_fs:"x < m  ?g' x = ?g x"
    for x proof(induct x rule:nat_less_induct[rule_format])
    case (1 x)
    hence ind: "m < x  ?g' m = ?g m"
       for m by auto
    { assume "x > i"
      hence ?case unfolding gs2.gso.simps[of x] gs1.gso.simps[of x] unfolding gs1.μ.simps gs2.μ.simps
        using ind eq by (auto intro: cong[OF _ cong[OF refl[of "gs.sumlist"]]])
    } note eq_rest = this
    show ?case by (rule linorder_class.linorder_cases[of x i],insert G1_G eq_part eq_rest,auto)
  qed
  hence Hs:"?G' = ?G" by (auto simp:o_def)
  have red: "weakly_reduced fs i  weakly_reduced fs' i" using eq_fs i < m
    unfolding gram_schmidt_fs.weakly_reduced_def by simp
  let ?Mi = "M ! i ! j"  
  have Gjn: "dim_vec (fs ! j) = n" using Fij(2) carrier_vecD by blast
  define E where "E = addrow_mat m (- ?R c) i j"
  define M' where "M' = gs1.M m"
  define N' where "N' = gs2.M m"
  have E: "E  carrier_mat m m" unfolding E_def by simp
  have M: "M'  carrier_mat m m" unfolding gs1.M_def M'_def by auto
  have N: "N'  carrier_mat m m" unfolding gs2.M_def N'_def by auto
  let ?mat = "mat_of_rows n" 
  let ?GsM = "?mat ?G" 
  have Gs: "?GsM  carrier_mat m n" by auto
  hence GsT: "?GsMT  carrier_mat n m" by auto
  have Gnn: "?mat (RAT fs)  carrier_mat m n" unfolding mat_of_rows_def using len by auto
  have "?mat (RAT fs') = addrow (- ?R c) i j (?mat (RAT fs))" 
    unfolding RAT_F1 by (rule eq_matI, insert Gjn ji(2), auto simp: len mat_of_rows_def)
  also have " = E * ?mat (RAT fs)" unfolding E_def
    by (rule addrow_mat, insert j i, auto simp: mat_of_rows_def len)
  finally have HEG: "?mat (RAT fs') = E * ?mat (RAT fs)" . (* lemma 16.12(i), part 1 *)
  have "(E * M') * ?mat ?G = E * (M' * ?mat ?G)" 
    by (rule assoc_mult_mat[OF E M Gs])
  also have "M' * ?GsM = ?mat (RAT fs)" using gs1.matrix_equality conn1 M'_def by simp
  also have "E *  = ?mat (RAT fs')" unfolding HEG ..
  also have " = N' * ?mat ?G'" using gs2.matrix_equality conn2 unfolding N'_def by simp
  also have "?mat ?G' = ?GsM" unfolding Hs ..
  finally have "(E * M') * ?GsM = N' * ?GsM" .
  from arg_cong[OF this, of "λ x. x * ?GsMT"] E M N 
  have EMN: "(E * M') * (?GsM * ?GsMT) = N' * (?GsM * ?GsMT)" 
    by (subst (1 2) assoc_mult_mat[OF _ Gs GsT, of _ m, symmetric], auto)
  have "det (?GsM * ?GsMT) = gs.Gramian_determinant ?G m" 
    unfolding gs.Gramian_determinant_def
    by (subst gs.Gramian_matrix_alt_def, auto simp: Let_def)
  also have " > 0" 
  proof -
    have 1: "gs.lin_indpt_list ?G"
      using conn1 gs1.orthogonal_gso gs1.gso_carrier by (intro gs.orthogonal_imp_lin_indpt_list) (auto)
    interpret G: gram_schmidt_fs_lin_indpt n ?G
      by  (standard) (use 1 gs.lin_indpt_list_def in auto)
    show ?thesis
      by (intro G.Gramian_determinant) auto
  qed
  finally have "det (?GsM * ?GsMT)  0" by simp
  from vec_space.det_nonzero_congruence[OF EMN this _ _ N] Gs E M
  have EMN: "E * M' = N'" by auto (* lemma 16.12(i), part 2 *) 
  {
    fix i' j'
    assume ij: "i' < m" "j' < m" and choice: "i'  i  j < j'" 
    have "?mu' i' j' 
      = N' $$ (i',j')" using ij F1 unfolding N'_def gs2.M_def by auto
    also have " = addrow (- ?R c) i j M' $$ (i',j')" unfolding EMN[symmetric] E_def
      by (subst addrow_mat[OF M], insert ji, auto)
    also have " = (if i = i' then - ?R c * M' $$ (j, j') + M' $$ (i', j') else M' $$ (i', j'))" 
      by (rule index_mat_addrow, insert ij M, auto)
    also have " = M' $$ (i', j')"
    proof (cases "i = i'")
      case True
      with choice have jj: "j < j'" by auto
      have "M' $$ (j, j') = ?mu j j'" 
        using ij ji len unfolding M'_def gs1.M_def by auto
      also have " = 0" unfolding gs1.μ.simps using jj by auto
      finally show ?thesis using True by auto
    qed auto
    also have " = ?mu i' j'"
      using ij len unfolding M'_def gs1.M_def by auto
    also note calculation
  } note mu_no_change = this
  {
    fix j'
    assume jj': "j'  j" with j i have j': "j' < m" by auto
    have "?mu' i j' 
      = N' $$ (i,j')" using jj' j i F1 unfolding N'_def gs2.M_def by auto
    also have " = addrow (- ?R c) i j M' $$ (i,j')" unfolding EMN[symmetric] E_def
      by (subst addrow_mat[OF M], insert ji, auto)
    also have " = - ?R c * M' $$ (j, j') + M' $$ (i, j')" 
      by (rule index_mat_addrow, insert j' i M, auto)
    also have " = M' $$ (i, j') - ?R c * M' $$ (j, j')" by simp
    also have "M' $$ (i, j') = ?mu i j'"
      using i j' len unfolding M'_def gs1.M_def by auto
    also have "M' $$ (j, j') = ?mu j j'" 
      using i j j' len unfolding M'_def gs1.M_def by auto
    finally have "?mu' i j' = ?mu i j' - ?R c * ?mu j j'" by auto
  } note mu_change = this  
  show mu_update: "i' < m  j' < m  
    ?mu' i' j' = (if i' = i  j'  j then ?mu i j' - ?R c * ?mu j j' else ?mu i' j')" 
    for i' j' using mu_change[of j'] mu_no_change[of i' j']
    by auto
  {
    assume "LLL_invariant True i fs"
    from LLL_invD[OF this] have "weakly_reduced fs i" and sred: "reduced fs i" by auto
    from red[OF this(1)] have red: "weakly_reduced fs' i" .
    have sred: "reduced fs' i"
      unfolding gram_schmidt_fs.reduced_def 
    proof (intro conjI[OF red] impI allI, goal_cases)
      case (1 i' j)
      with mu_no_change[of i' j] sred[unfolded gram_schmidt_fs.reduced_def, THEN conjunct2, rule_format, of i' j] i 
      show ?case by auto
    qed
    show "LLL_invariant True i fs'" 
      by (intro LLL_invI[OF F1 lattice i  m indep_F1 sred], auto)
  } 
  show Linv': "LLL_invariant_weak fs'" 
    by (intro LLL_inv_wI[OF F1 lattice indep_F1])

  have mudiff:"?mu i j - of_int c = ?mu' i j"
    by (subst mu_change, auto simp: gs1.μ.simps)
  have lin_indpt_list_fs: "gs.lin_indpt_list (RAT fs')"
    unfolding gs.lin_indpt_list_def using conn2 by auto
  { 
    assume c: "c = round (μ fs i j)" 
    have small: "abs (?mu i j - of_int c)  inverse 2" unfolding j c
      using of_int_round_abs_le by (auto simp add: abs_minus_commute)
    from this[unfolded mudiff] 
    show mu'_2: "abs (?mu' i j)  1 / 2" by simp
    assume mu_small: "μ_small_row i fs (Suc j)" 

    show "μ_small_row i fs' j" 
      unfolding μ_small_row_def 
    proof (intro allI, goal_cases)
      case (1 j')
      show ?case using mu'_2 mu_small[unfolded μ_small_row_def, rule_format, of j'] 
        by (cases "j' > j", insert mu_update[of i j'] i, auto)
    qed
  }

  {
    fix i
    assume i: "i  m"
    have "rat_of_int (d fs' i) = of_int (d fs i)" 
      unfolding d_def Gramian_determinant(1)[OF Linv i] Gramian_determinant(1)[OF Linv' i]
      by (rule prod.cong[OF refl], subst eq_fs, insert i, auto)
    thus "d fs' i = d fs i" by simp
  } note d = this 
  have D: "D fs' = D fs" 
    unfolding D_def
    by (rule arg_cong[of _ _ nat], rule prod.cong[OF refl], auto simp: d)
  show "LLL_measure i fs' = LLL_measure i fs" 
    unfolding LLL_measure_def logD_def D ..
qed

text ‹Addition step which can be skipped since $\mu$-value is already small›

lemma basis_reduction_add_row_main_0: assumes Linv: "LLL_invariant_weak fs"
  and i: "i < m"  and j: "j < i" 
  and 0: "round (μ fs i j) = 0" 
  and mu_small: "μ_small_row i fs (Suc j)"
shows "μ_small_row i fs j" (is ?g1)
proof -
  note inv = LLL_inv_wD[OF Linv]
  from inv(5)[OF i] inv(5)[of j] i j
  have id: "fs[i := fs ! i - 0 v fs ! j] = fs" 
    by (intro nth_equalityI, insert inv i, auto)
  show ?g1
    using basis_reduction_add_row_main[OF Linv i j _, of fs] 0 id mu_small by auto
qed

lemma μ_small_row_refl: "μ_small_row i fs i" 
  unfolding μ_small_row_def by auto

lemma basis_reduction_add_row_done: assumes Linv: "LLL_invariant True i fs"
  and i: "i < m" 
  and mu_small: "μ_small_row i fs 0" 
shows "LLL_invariant False i fs"
proof -
  note inv = LLL_invD[OF Linv]
  from mu_small 
  have mu_small: "μ_small fs i" unfolding μ_small_row_def μ_small_def by auto
  show ?thesis
    using i mu_small by (intro LLL_invI[OF inv(3,6,7,9,1,10)], auto)
qed     

(* lemma 16.16 (ii), one case *)
lemma d_swap_unchanged: assumes len: "length F1 = m" 
  and i0: "i  0" and i: "i < m" and ki: "k  i" and km: "k  m"   
  and swap: "F2 = F1[i := F1 ! (i - 1), i - 1 := F1 ! i]"
shows "d F1 k = d F2 k"
proof -
  let ?F1_M = "mat k n (λ(i, y). F1 ! i $ y)" 
  let ?F2_M = "mat k n (λ(i, y). F2 ! i $ y)" 
  have " P. P  carrier_mat k k  det P  {-1, 1}  ?F2_M = P * ?F1_M" 
  proof cases
    assume ki: "k < i" 
    hence H: "?F2_M = ?F1_M" unfolding swap
      by (intro eq_matI, auto)
    let ?P = "1m k" 
    have "?P  carrier_mat k k" "det ?P  {-1, 1}" "?F2_M = ?P * ?F1_M" unfolding H by auto
    thus ?thesis by blast
  next
    assume "¬ k < i" 
    with ki have ki: "k > i" by auto
    let ?P = "swaprows_mat k i (i - 1)" 
    from i0 ki have neq: "i  i - 1" and kmi: "i - 1 < k" by auto
    have *: "?P  carrier_mat k k" "det ?P  {-1, 1}" using det_swaprows_mat[OF ki kmi neq] ki by auto
    from i len have iH: "i < length F1" "i - 1 < length F1" by auto 
    have "?P * ?F1_M = swaprows i (i - 1) ?F1_M" 
      by (subst swaprows_mat[OF _ ki kmi], auto)
    also have " = ?F2_M" unfolding swap
      by (intro eq_matI, rename_tac ii jj, 
          case_tac "ii = i", (insert iH, simp add: nth_list_update)[1],
          case_tac "ii = i - 1", insert iH neq ki, auto simp: nth_list_update)
    finally show ?thesis using * by metis
  qed
  then obtain P where P: "P  carrier_mat k k" and detP: "det P  {-1, 1}" and H': "?F2_M = P * ?F1_M" by auto
  have "d F2 k = det (gs.Gramian_matrix F2 k)" 
    unfolding d_def gs.Gramian_determinant_def by simp
  also have " = det (?F2_M * ?F2_MT)" unfolding gs.Gramian_matrix_def Let_def by simp
  also have "?F2_M * ?F2_MT = ?F2_M * (?F1_MT * PT)" unfolding H'
    by (subst transpose_mult[OF P], auto)
  also have " = P * (?F1_M * (?F1_MT * PT))" unfolding H' 
    by (subst assoc_mult_mat[OF P], auto)
  also have "det  = det P * det (?F1_M * (?F1_MT * PT))" 
    by (rule det_mult[OF P], insert P, auto)
  also have "?F1_M * (?F1_MT * PT) = (?F1_M * ?F1_MT) * PT" 
    by (subst assoc_mult_mat, insert P, auto)
  also have "det  = det (?F1_M * ?F1_MT) * det P" 
    by (subst det_mult, insert P, auto simp: det_transpose)
  also have "det (?F1_M * ?F1_MT) = det (gs.Gramian_matrix F1 k)" unfolding gs.Gramian_matrix_def Let_def by simp
  also have " = d F1 k" 
    unfolding d_def gs.Gramian_determinant_def by simp
  finally have "d F2 k = (det P * det P) * d F1 k" by simp
  also have "det P * det P = 1" using detP by auto
  finally show "d F1 k = d F2 k" by simp
qed

definition base where "base = real_of_rat ((4 * α) / (4 + α))" 

definition g_bound :: "int vec list  bool" where 
  "g_bound fs = ( i < m. sq_norm (gso fs i)  of_nat N)" 

end

locale LLL_with_assms = LLL + 
  assumes α: "α  4/3"
    and lin_dep: "lin_indep fs_init" 
    and len: "length fs_init = m" 
begin
lemma α0: "α > 0" "α  0" 
  using α by auto

lemma fs_init: "set fs_init  carrier_vec n" 
  using lin_dep[unfolded gs.lin_indpt_list_def] by auto


lemma reduction: "0 < reduction" "reduction  1" 
  "α > 4/3  reduction < 1" 
  "α = 4/3  reduction = 1" 
  using α unfolding reduction_def by auto

lemma base: "α > 4/3  base > 1" using reduction(1,3) unfolding reduction_def base_def by auto

lemma basis_reduction_swap_main: assumes Linvw: "LLL_invariant_weak fs"
  and small: "LLL_invariant False i fs  abs (μ fs i (i - 1))  1/2" 
  and i: "i < m"
  and i0: "i  0" 
  and norm_ineq: "sq_norm (gso fs (i - 1)) > α * sq_norm (gso fs i)" 
  and fs'_def: "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]" 
shows "LLL_invariant_weak fs'" 
  and "LLL_invariant False i fs  LLL_invariant False (i - 1) fs'" 
  and "LLL_measure i fs > LLL_measure (i - 1) fs'" 
  (* new values of gso *)
  and " k. k < m  gso fs' k = (if k = i - 1 then
         gso fs i + μ fs i (i - 1) v gso fs (i - 1) 
      else if k = i then
         gso fs (i - 1) - (RAT fs ! (i - 1)  gso fs' (i - 1) / sq_norm (gso fs' (i - 1))) v gso fs' (i - 1)
      else gso fs k)" (is " k. _  _ = ?newg k")
  (* new values of norms of gso *)
  and " k. k < m  sq_norm (gso fs' k) = (if k = i - 1 then
          sq_norm (gso fs i) + (μ fs i (i - 1) * μ fs i (i - 1)) * sq_norm (gso fs (i - 1))
      else if k = i then
         sq_norm (gso fs i) * sq_norm (gso fs (i - 1)) / sq_norm (gso fs' (i - 1))
      else sq_norm (gso fs k))" (is " k. _  _ = ?new_norm k")
  (* new values of μ-values *)
  and " ii j. ii < m  j < ii  μ fs' ii j = (
        if ii = i - 1 then 
           μ fs i j
        else if ii = i then 
          if j = i - 1 then 
             μ fs i (i - 1) * sq_norm (gso fs (i - 1)) / sq_norm (gso fs' (i - 1))
          else 
             μ fs (i - 1) j
        else if ii > i  j = i then
           μ fs ii (i - 1) - μ fs i (i - 1) * μ fs ii i
        else if ii > i  j = i - 1 then 
           μ fs ii (i - 1) * μ fs' i (i - 1) + μ fs ii i * sq_norm (gso fs i) / sq_norm (gso fs' (i - 1))
        else μ fs ii j)" (is " ii j. _  _  _ = ?new_mu ii j")
  (* new d-values *)
  and " ii. ii  m  of_int (d fs' ii) = (if ii = i then 
       sq_norm (gso fs' (i - 1)) / sq_norm (gso fs (i - 1)) * of_int (d fs i)
       else of_int (d fs ii))" 
proof -
  note inv = LLL_inv_wD[OF Linvw]
  interpret fs: fs_int' n m fs_init fs
    by (standard) (use Linvw in auto)
  let ?mu1 = "μ fs" 
  let ?mu2 = "μ fs'" 
  let ?g1 = "gso fs" 
  let ?g2 = "gso fs'" 
  have m12: "¦?mu1 i (i - 1)¦  inverse 2" using small
  proof 
    assume "LLL_invariant False i fs" 
    from LLL_invD(11)[OF this] i0 show ?thesis unfolding μ_small_def by auto
  qed auto
  note d = d_def  
  note Gd = Gramian_determinant(1)
  note Gd12 = Gd[OF Linvw]
  let ?x = "?g1 (i - 1)" let ?y = "?g1 i" 
  let ?cond = "α * sq_norm ?y < sq_norm ?x" 
  from inv have len: "length fs = m" and HC: "set fs  carrier_vec n" 
    and L: "lattice_of fs = L" 
    using i by auto 
  from i0 inv i have swap: "set fs  carrier_vec n" "i < length fs" "i - 1 < length fs" "i  i - 1" 
    unfolding Let_def by auto
  have RAT_fs': "RAT fs' = (RAT fs)[i := (RAT fs) ! (i - 1), i - 1 := (RAT fs) ! i]" 
    unfolding fs'_def using swap by (intro nth_equalityI, auto simp: nth_list_update)
  have span': "gs.span (SRAT fs) = gs.span (SRAT fs')" unfolding fs'_def
    by (rule arg_cong[of _ _ gs.span], insert swap, auto)
  have lfs': "lattice_of fs' = lattice_of fs" unfolding fs'_def
    by (rule lattice_of_swap[OF swap refl])
  with inv have lattice: "lattice_of fs' = L" by auto
  have len': "length fs' = m" using inv unfolding fs'_def by auto
  have fs': "set fs'  carrier_vec n" using swap unfolding fs'_def set_conv_nth
    by (auto, rename_tac k, case_tac "k = i", force, case_tac "k = i - 1", auto)
  let ?rv = "map_vec rat_of_int" 
  from inv(1) have indepH: "lin_indep fs" .
  from i i0 len have "i < length (RAT fs)" "i - 1 < length (RAT fs)" by auto
  with distinct_swap[OF this] len have "distinct (RAT fs') = distinct (RAT fs)" unfolding RAT_fs'
    by (auto simp: map_update)
  with len' fs' span' indepH have indepH': "lin_indep fs'" unfolding fs'_def using i i0
    by (auto simp: gs.lin_indpt_list_def)
  have lenR': "length (RAT fs') = m" using len' by auto
  have conn1: "set (RAT fs)  carrier_vec n"  "length (RAT fs) = m" "distinct (RAT fs)"
    "gs.lin_indpt (set (RAT fs))"
    using inv unfolding gs.lin_indpt_list_def by auto
  have conn2: "set (RAT fs')  carrier_vec n"  "length (RAT fs') = m" "distinct (RAT fs')"
    "gs.lin_indpt (set (RAT fs'))"
    using indepH' lenR'  unfolding gs.lin_indpt_list_def by auto
  interpret gs2: gram_schmidt_fs_lin_indpt n "RAT fs'"
    by (standard) (use indepH' lenR' gs.lin_indpt_list_def in auto)
  have fs'_fs: "k < i - 1  fs' ! k = fs ! k" for k unfolding fs'_def by auto
  { 
    fix k
    assume ki: "k < i - 1" 
    with i have kn: "k < m" by simp
    have "?g2 k = ?g1 k" 
      by (rule gs.gso_cong, insert ki kn len, auto simp: fs'_def)
  } note G2_G = this
  have take_eq: "take (Suc i - 1 - 1) fs' = take (Suc i - 1 - 1) fs" 
    by (intro nth_equalityI, insert len len' i swap(2-), auto intro!: fs'_fs) 
  have i1n: "i - 1 < m" using i by auto
  let ?R = rat_of_int
  let ?RV = "map_vec ?R"  
  let ?f1 = "λ i. RAT fs ! i"
  let ?f2 = "λ i. RAT fs' ! i" 
  let ?n1 = "λ i. sq_norm (?g1 i)" 
  let ?n2 = "λ i. sq_norm (?g2 i)" 
  have heq:"fs ! (i - 1) = fs' ! i" "take (i-1) fs = take (i-1) fs'"
           "?f2 (i - 1) = ?f1 i" "?f2 i = ?f1 (i - 1)"
    unfolding fs'_def using i len i0 by auto
  have norm_pos2: "j < m  ?n2 j > 0" for j 
    using gs2.sq_norm_pos len' by simp
  have norm_pos1: "j < m  ?n1 j > 0" for j 
    using fs.gs.sq_norm_pos inv by simp
  have norm_zero2: "j < m  ?n2 j  0" for j using norm_pos2[of j] by linarith
  have norm_zero1: "j < m  ?n1 j  0" for j using norm_pos1[of j] by linarith
  have gs: " j. j < m  ?g1 j  Rn" using inv by blast
  have gs2: " j. j < m  ?g2 j  Rn" using fs.gs.gso_carrier conn2 by auto
  have g: " j. j < m  ?f1 j  Rn" using inv by auto
  have g2: " j. j < m  ?f2 j  Rn" using gs2.f_carrier conn2 by blast
  let ?fs1 = "?f1 ` {0..< (i - 1)}" 
  have G: "?fs1  Rn" using g i by auto
  let ?gs1 = "?g1 ` {0..< (i - 1)}" 
  have G': "?gs1  Rn" using gs i by auto
  let ?S = "gs.span ?fs1" 
  let ?S' = "gs.span ?gs1" 
  have S'S: "?S' = ?S" 
    by (rule fs.gs.partial_span', insert conn1 i, auto)
  have "gs.is_oc_projection (?g2 (i - 1)) (gs.span (?g2 ` {0..< (i - 1)})) (?f2 (i - 1))" 
    using i len' by (intro  gs2.gso_oc_projection_span(2)) auto
  also have "?f2 (i - 1) = ?f1 i" unfolding fs'_def using len i by auto
  also have "gs.span (?g2 ` {0 ..< (i - 1)}) = gs.span (?f2 ` {0 ..< (i - 1)})" 
    using i len' by (intro gs2.partial_span') auto
  also have "?f2 ` {0 ..< (i - 1)} = ?fs1" 
    by (rule image_cong[OF refl], insert len i, auto simp: fs'_def)
  finally have claim1: "gs.is_oc_projection (?g2 (i - 1)) ?S (?f1 i)" .
  have list_id: "[0..<Suc (i - 1)] = [0..< i - 1] @ [i - 1]" 
    "[0..< Suc i] = [0..< i] @ [i]" "map f [x] = [f x]" for f x using i by auto
  (* f1i_sum is claim 2 *)
  have f1i_sum: "?f1 i = gs.sumlist (map (λj. ?mu1 i j v ?g1 j) [0 ..< i]) + ?g1 i" (is "_ = ?sum + _") 
    apply(subst fs.gs.fi_is_sum_of_mu_gso, insert len i, force)
    unfolding map_append list_id
    by (subst gs.M.sumlist_snoc, insert i gs conn1, auto simp: fs.gs.μ.simps)
  have f1im1_sum: "?f1 (i - 1) = gs.sumlist (map (λj. ?mu1 (i - 1) j v ?g1 j) [0..<i - 1]) + ?g1 (i - 1)" (is "_ = ?sum1 + _")
    apply(subst fs.gs.fi_is_sum_of_mu_gso, insert len i, force)
    unfolding map_append list_id
    by (subst gs.M.sumlist_snoc, insert i gs, auto simp: fs.gs.μ.simps)

  have sum: "?sum  Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
  have sum1: "?sum1  Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
  from gs.span_closed[OF G] have S: "?S  Rn" by auto
  from gs i have gs': " j. j < i - 1  ?g1 j  Rn" and gsi: "?g1 (i - 1)  Rn" by auto
  have "[0 ..< i] = [0 ..< Suc (i - 1)]" using i0 by simp
  also have " = [0 ..< i - 1] @ [i - 1]" by simp
  finally have list: "[0 ..< i] = [0 ..< i - 1] @ [i - 1]" .

  { (* d does not change for k ≠ i *)
    fix k
    assume kn: "k  m" and ki: "k  i" 
    from d_swap_unchanged[OF len i0 i ki kn fs'_def]  
    have "d fs k = d fs' k" by simp
  } note d = this

  (* new value of g (i-1) *)
  have g2_im1: "?g2 (i - 1) = ?g1 i + ?mu1 i (i - 1) v ?g1 (i - 1)" (is "_ = _ + ?mu_f1")
  proof (rule gs.is_oc_projection_eq[OF  claim1 _ S g[OF i]])
    show "gs.is_oc_projection (?g1 i + ?mu_f1) ?S (?f1 i)" unfolding gs.is_oc_projection_def
    proof (intro conjI allI impI)
      let ?sum' = "gs.sumlist (map (λj. ?mu1 i j v ?g1 j) [0 ..< i - 1])" 
      have sum': "?sum'  Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
      show inRn: "(?g1 i + ?mu_f1)  Rn" using gs[OF i] gsi i by auto
      have carr: "?sum  Rn" "?g1 i  Rn" "?mu_f1  Rn" "?sum'  Rn" using sum' sum gs[OF i] gsi i by auto
      have "?f1 i - (?g1 i + ?mu_f1) = (?sum + ?g1 i) - (?g1 i + ?mu_f1)"
        unfolding f1i_sum by simp
      also have " = ?sum - ?mu_f1" using carr by auto
      also have "?sum = gs.sumlist (map (λj. ?mu1 i j v ?g1 j) [0 ..< i - 1] @ [?mu_f1])" 
        unfolding list by simp 
      also have " = ?sum' + ?mu_f1" 
        by (subst gs.sumlist_append, insert gs' gsi, auto)
      also have " - ?mu_f1 = ?sum'" using sum' gsi by auto
      finally have id: "?f1 i - (?g1 i + ?mu_f1) = ?sum'" .
      show "?f1 i - (?g1 i + ?mu_f1)  gs.span ?S" unfolding id gs.span_span[OF G]
      proof (rule gs.sumlist_in_span[OF G])
        fix v
        assume "v  set (map (λj. ?mu1 i j v ?g1 j) [0 ..< i - 1])" 
        then obtain j where j: "j < i - 1" and v: "v = ?mu1 i j v ?g1 j" by auto
        show "v  ?S" unfolding v
          by (rule gs.smult_in_span[OF G], unfold S'S[symmetric], rule gs.span_mem, insert gs i j, auto)
      qed
      fix x
      assume "x  ?S"
      hence x: "x  ?S'" using S'S by simp
      show "(?g1 i + ?mu_f1)  x = 0"
      proof (rule gs.orthocompl_span[OF _ G' inRn x])
        fix x
        assume "x  ?gs1"
        then obtain j where j: "j < i - 1" and x_id: "x = ?g1 j" by auto
        from j i x_id gs[of j] have x: "x  Rn" by auto
        {
          fix k
          assume k: "k > j" "k < m" 
          have "?g1 k  x = 0" unfolding x_id 
            by (rule fs.gs.orthogonal, insert conn1 k, auto)
        }
        from this[of i] this[of "i - 1"] j i 
        have main: "?g1 i  x = 0" "?g1 (i - 1)  x = 0" by auto
        have "(?g1 i + ?mu_f1)  x = ?g1 i  x + ?mu_f1  x" 
          by (rule add_scalar_prod_distrib[OF gs[OF i] _ x], insert gsi, auto)
        also have " = 0" using main
          by (subst smult_scalar_prod_distrib[OF gsi x], auto)
        finally show "(?g1 i + ?mu_f1)  x = 0" .
      qed
    qed
  qed
  { (* 16.13 (i): for g, only g_i and g_{i-1} can change *)
    fix k
    assume kn: "k < m" 
      and ki: "k  i" "k  i - 1"
    have "?g2 k = gs.oc_projection (gs.span (?g2 ` {0..<k})) (?f2 k)" 
      by (rule gs2.gso_oc_projection_span, insert kn conn2, auto)
    also have "gs.span (?g2 ` {0..<k}) = gs.span (?f2 ` {0..<k})" 
      by (rule gs2.partial_span', insert conn2 kn, auto)
    also have "?f2 ` {0..<k} = ?f1 ` {0..<k}"
    proof(cases "ki")
      case True hence "k < i - 1" using ki by auto
      then show ?thesis apply(intro image_cong) unfolding fs'_def using len i by auto
    next
      case False 
      have "?f2 ` {0..<k} = (?f1  transpose i (i - 1)) ` {0..<k}"
        unfolding transpose_def fs'_def o_def using len i 
        by (intro image_cong, insert len kn, force+)
      also have " = ?f1 ` {0..<k}"
        apply(rule swap_image_eq) using False by auto
      finally show ?thesis.
    qed
    also have "gs.span  = gs.span (?g1 ` {0..<k})" 
      by (rule sym, rule fs.gs.partial_span', insert conn1 kn, auto)
    also have "?f2 k = ?f1 k" using ki kn len unfolding fs'_def by auto
    also have "gs.oc_projection (gs.span (?g1 ` {0..<k}))  = ?g1 k" 
      by (subst fs.gs.gso_oc_projection_span, insert kn conn1, auto)
    finally have "?g2 k = ?g1 k" . 
  } note g2_g1_identical = this

  (* calculation of new mu-values *)
  { (* no change of mu for lines before line i - 1 *)
    fix jj ii
    assume ii: "ii < i - 1"  
    have "?mu2 ii jj = ?mu1 ii jj" using ii i len
      by (subst gs.μ_cong[of _ _ "RAT fs" "RAT fs'"], auto simp: fs'_def)
  } note mu'_mu_small_i = this
  { (* swap of mu-values in lines i - 1 and i for j < i - 1 *)
    fix jj
    assume jj: "jj < i - 1"  
    hence id1: "jj < i - 1  True" "jj < i  True" by auto
    have id2: "?g2 jj = ?g1 jj" by (subst g2_g1_identical, insert jj i, auto)       
    have "?mu2 i jj = ?mu1 (i - 1) jj" "?mu2 (i - 1) jj = ?mu1 i jj" 
      unfolding gs2.μ.simps fs.gs.μ.simps id1 id2 if_True using len i i0 by (auto simp: fs'_def)
  } note mu'_mu_i_im1_j = this

  have im1: "i - 1 < m" using i by auto

  (* calculation of new value of g_i *)
  let ?g2_im1 = "?g2 (i - 1)" 
  have g2_im1_Rn: "?g2_im1  Rn" using i conn2 by (auto intro!: fs.gs.gso_carrier)
  {
    let ?mu2_f2 = "λ j. - ?mu2 i j v ?g2 j" 
    let ?sum = "gs.sumlist (map (λj. - ?mu1 (i - 1) j v ?g1 j) [0 ..< i - 1])" 
    have mhs: "?mu2_f2 (i - 1)  Rn" using i conn2 by (auto intro!: fs.gs.gso_carrier)
    have sum': "?sum  Rn" by (rule gs.sumlist_carrier, insert gs i, auto)
    have gim1: "?f1 (i - 1)  Rn" using g i by auto
    have "?g2 i = ?f2 i + gs.sumlist (map ?mu2_f2 [0 ..< i-1] @ [?mu2_f2 (i-1)])" 
      unfolding gs2.gso.simps[of i] list by simp
    also have "?f2 i = ?f1 (i - 1)" unfolding fs'_def using len i i0 by auto
    also have "map ?mu2_f2 [0 ..< i-1] = map (λj. - ?mu1 (i - 1) j v ?g1 j) [0 ..< i - 1]"
      by (rule map_cong[OF refl], subst g2_g1_identical, insert i, auto simp: mu'_mu_i_im1_j)
    also have "gs.sumlist ( @ [?mu2_f2 (i - 1)]) = ?sum + ?mu2_f2 (i - 1)" 
      by (subst gs.sumlist_append, insert gs i mhs, auto)
    also have "?f1 (i - 1) +  = (?f1 (i - 1) + ?sum) + ?mu2_f2 (i - 1)"
      using gim1 sum' mhs by auto
    also have "?f1 (i - 1) + ?sum = ?g1 (i - 1)" unfolding fs.gs.gso.simps[of "i - 1"] by simp
    also have "?mu2_f2 (i - 1) = - (?f2 i  ?g2_im1 / sq_norm ?g2_im1) v ?g2_im1" unfolding gs2.μ.simps using i0 by simp
    also have " = - ((?f2 i  ?g2_im1 / sq_norm ?g2_im1) v ?g2_im1)" by auto
    also have "?g1 (i - 1) +  = ?g1 (i - 1) - ((?f2 i  ?g2_im1 / sq_norm ?g2_im1) v ?g2_im1)"
      by (rule sym, rule minus_add_uminus_vec[of _ n], insert gsi g2_im1_Rn, auto)
    also have "?f2 i = ?f1 (i - 1)" by fact
    finally have "?g2 i = ?g1 (i - 1) - (?f1 (i - 1)  ?g2 (i - 1) / sq_norm (?g2 (i - 1))) v ?g2 (i - 1)" .
  } note g2_i = this

  let ?n1 = "λ i. sq_norm (?g1 i)" 
  let ?n2 = "λ i. sq_norm (?g2 i)" 

  (* calculation of new norms *)
  { (* norm of g (i - 1) *)
    have "?n2 (i - 1) = sq_norm (?g1 i + ?mu_f1)" unfolding g2_im1 by simp
    also have " = (?g1 i + ?mu_f1)  (?g1 i + ?mu_f1)" 
      by (simp add: sq_norm_vec_as_cscalar_prod)
    also have " = (?g1 i + ?mu_f1)  ?g1 i + (?g1 i + ?mu_f1)  ?mu_f1" 
      by (rule scalar_prod_add_distrib, insert gs i, auto)
    also have "(?g1 i + ?mu_f1)  ?g1 i = ?g1 i  ?g1 i + ?mu_f1  ?g1 i" 
      by (rule add_scalar_prod_distrib, insert gs i, auto)
    also have "(?g1 i + ?mu_f1)  ?mu_f1 = ?g1 i  ?mu_f1 + ?mu_f1  ?mu_f1" 
      by (rule add_scalar_prod_distrib, insert gs i, auto)
    also have "?mu_f1  ?g1 i = ?g1 i  ?mu_f1"
      by (rule comm_scalar_prod, insert gs i, auto)
    also have "?g1 i  ?g1 i = sq_norm (?g1 i)" 
      by (simp add: sq_norm_vec_as_cscalar_prod)
    also have "?g1 i  ?mu_f1 = ?mu1 i (i - 1) * (?g1 i  ?g1 (i - 1))" 
      by (rule scalar_prod_smult_right, insert gs[OF i] gs[OF i - 1 < m], auto)
    also have "?g1 i  ?g1 (i - 1) = 0" 
      using orthogonalD[OF fs.gs.orthogonal_gso, of i "i - 1"] i len i0  
      by (auto simp: o_def)
    also have "?mu_f1  ?mu_f1 = ?mu1 i (i - 1) * (?mu_f1  ?g1 (i - 1))" 
      by (rule scalar_prod_smult_right, insert gs[OF i] gs[OF i - 1 < m], auto)
    also have "?mu_f1  ?g1 (i - 1) = ?mu1 i (i - 1) * (?g1 (i - 1)  ?g1 (i - 1))" 
      by (rule scalar_prod_smult_left, insert gs[OF i] gs[OF i - 1 < m], auto)
    also have "?g1 (i - 1)  ?g1 (i - 1) = sq_norm (?g1 (i - 1))" 
      by (simp add: sq_norm_vec_as_cscalar_prod)
    finally have "?n2 (i - 1) = ?n1 i + (?mu1 i (i - 1) * ?mu1 i (i - 1)) * ?n1 (i - 1)" 
      by (simp add: ac_simps o_def)
  } note sq_norm_g2_im1 = this

  from norm_pos1[OF i] norm_pos1[OF im1] norm_pos2[OF i] norm_pos2[OF im1]
  have norm0: "?n1 i  0" "?n1 (i - 1)  0" "?n2 i  0" "?n2 (i - 1)  0" by auto
  hence norm0': "?n2 (i - 1)  0" using i by auto

  { (* new norm of g i *)
    have si: "Suc i  m" and im1: "i - 1  m" using i by auto
    have det1: "gs.Gramian_determinant (RAT fs) (Suc i) = (j<Suc i. fs.gs.gso j2)"
      using fs.gs.Gramian_determinant si len by auto
    have det2: "gs.Gramian_determinant (RAT fs') (Suc i) = (j<Suc i. gs2.gso j2)"
      using gs2.Gramian_determinant si len' by auto
    from norm_zero1[OF less_le_trans[OF _ im1]] have 0: "(j < i-1. ?n1 j)  0" 
      by (subst prod_zero_iff, auto)
    have "rat_of_int (d fs' (Suc i)) = rat_of_int (d fs (Suc i))" 
      using d_swap_unchanged[OF len i0 i _ si fs'_def] by auto
    also have "rat_of_int (d fs' (Suc i)) = gs.Gramian_determinant (RAT fs') (Suc i)" unfolding d_def 
      by (subst fs.of_int_Gramian_determinant[symmetric], insert conn2 i g fs', auto simp: set_conv_nth)
    also have " = (j<Suc i. ?n2 j)" unfolding det2 by (rule prod.cong, insert i, auto)
    also have "rat_of_int (d fs (Suc i)) = gs.Gramian_determinant (RAT fs) (Suc i)" unfolding d_def 
      by (subst fs.of_int_Gramian_determinant[symmetric], insert conn1 i g, auto)
    also have " = (j<Suc i. ?n1 j)" unfolding det1 by (rule prod.cong, insert i, auto)
    also have "{..<Suc i} = insert i (insert (i-1) {..<i-1})" (is "_ = ?set") by auto
    also have "(j ?set. ?n2 j) = ?n2 i * ?n2 (i - 1) * (j < i-1. ?n2 j)" using i0
      by (subst prod.insert; (subst prod.insert)?; auto)
    also have "(j ?set. ?n1 j) = ?n1 i * ?n1 (i - 1) * (j < i-1. ?n1 j)" using i0
      by (subst prod.insert; (subst prod.insert)?; auto)
    also have "(j < i-1. ?n2 j) = (j < i-1. ?n1 j)" 
      by (rule prod.cong, insert G2_G, auto)
    finally have "?n2 i = ?n1 i * ?n1 (i - 1) / ?n2 (i - 1)" 
      using 0 norm0' by (auto simp: field_simps)
  } note sq_norm_g2_i = this

  (* mu values in rows > i do not change with j ∉ {i, i - 1} *)
  {
    fix ii j
    assume ii: "ii > i" "ii < m" 
     and ji: "j  i" "j  i - 1" 
    {
      assume j: "j < ii" 
      have "?mu2 ii j = (?f2 ii  ?g2 j) / sq_norm (?g2 j)" 
        unfolding gs2.μ.simps using j by auto
      also have "?f2 ii = ?f1 ii" using ii len unfolding fs'_def by auto
      also have "?g2 j = ?g1 j" using g2_g1_identical[of j] j ii ji by auto
      finally have "?mu2 ii j = ?mu1 ii j" 
        unfolding fs.gs.μ.simps using j by auto
    }
    hence "?mu2 ii j = ?mu1 ii j" by (cases "j < ii", auto simp: gs2.μ.simps fs.gs.μ.simps)
  } note mu_no_change_large_row = this

  { (* the new value of mu i (i - 1) *)
    have "?mu2 i (i - 1) = (?f2 i  ?g2 (i - 1)) / ?n2 (i - 1)" 
      unfolding gs2.μ.simps using i0 by auto
    also have "?f2 i  ?g2 (i - 1) = ?f1 (i - 1)  ?g2 (i - 1)" 
      using len i i0 unfolding fs'_def by auto
    also have " = ?f1 (i - 1)  (?g1 i + ?mu1 i (i - 1) v ?g1 (i - 1))" 
      unfolding g2_im1 by simp
    also have " = ?f1 (i - 1)  ?g1 i + ?f1 (i - 1)  (?mu1 i (i - 1) v ?g1 (i - 1))" 
      by (rule scalar_prod_add_distrib[of _ n], insert i gs g, auto)
    also have "?f1 (i - 1)  ?g1 i = 0" 
      by (subst fs.gs.fi_scalar_prod_gso, insert conn1 im1 i i0, auto simp: fs.gs.μ.simps fs.gs.μ.simps)
    also have "?f1 (i - 1)  (?mu1 i (i - 1) v ?g1 (i - 1)) = 
       ?mu1 i (i - 1) * (?f1 (i - 1)  ?g1 (i - 1))"  
      by (rule scalar_prod_smult_distrib, insert gs g i, auto)
    also have "?f1 (i - 1)  ?g1 (i - 1) = ?n1 (i - 1)" 
      by (subst fs.gs.fi_scalar_prod_gso, insert conn1 im1, auto simp: fs.gs.μ.simps)
    finally 
    have "?mu2 i (i - 1) = ?mu1 i (i - 1) * ?n1 (i - 1) / ?n2 (i - 1)" 
      by (simp add: sq_norm_vec_as_cscalar_prod)
  } note mu'_mu_i_im1 = this

  { (* the new values of mu ii (i - 1) for ii > i *)
    fix ii assume iii: "ii > i" and ii: "ii < m" 
    hence iii1: "i - 1 < ii" by auto
    have "?mu2 ii (i - 1) = (?f2 ii  ?g2 (i - 1)) / ?n2 (i - 1)" 
      unfolding gs2.μ.simps using i0 iii1 by auto
    also have "?f2 ii  ?g2 (i-1) = ?f1 ii  ?g2 (i - 1)" 
      using len i i0 iii ii unfolding fs'_def by auto
    also have " = ?f1 ii  (?g1 i + ?mu1 i (i - 1) v ?g1 (i - 1))" 
      unfolding g2_im1 by simp
    also have " = ?f1 ii  ?g1 i + ?f1 ii  (?mu1 i (i - 1) v ?g1 (i - 1))" 
      by (rule scalar_prod_add_distrib[of _ n], insert i ii gs g, auto)
    also have "?f1 ii  ?g1 i = ?mu1 ii i * ?n1 i" 
      by (rule fs.gs.fi_scalar_prod_gso, insert conn1 ii i, auto)
    also have "?f1 ii  (?mu1 i (i - 1) v ?g1 (i - 1)) = 
       ?mu1 i (i - 1) * (?f1 ii  ?g1 (i - 1))"  
      by (rule scalar_prod_smult_distrib, insert gs g i ii, auto)
    also have "?f1 ii  ?g1 (i - 1) = ?mu1 ii (i - 1) * ?n1 (i - 1)" 
      by (rule fs.gs.fi_scalar_prod_gso, insert conn1 ii im1, auto)
    finally have "?mu2 ii (i - 1) = ?mu1 ii (i - 1) * ?mu2 i (i - 1) + ?mu1 ii i * ?n1 i / ?n2 (i - 1)" 
      unfolding mu'_mu_i_im1 using norm0 by (auto simp: field_simps)
  } note mu'_mu_large_row_im1 = this    

  { (* the new values of mu ii i for ii > i *)
    fix ii assume iii: "ii > i" and ii: "ii < m" 
    have "?mu2 ii i = (?f2 ii  ?g2 i) / ?n2 i" 
      unfolding gs2.μ.simps using i0 iii by auto
    also have "?f2 ii  ?g2 i = ?f1 ii  ?g2 i" 
      using len i i0 iii ii unfolding fs'_def by auto
    also have " = ?f1 ii  (?g1 (i - 1) - (?f1 (i - 1)  ?g2 (i - 1) / ?n2 (i - 1)) v ?g2 (i - 1))" 
      unfolding g2_i by simp
    also have "?f1 (i - 1) = ?f2 i" using i i0 len unfolding fs'_def by auto
    also have "?f2 i  ?g2 (i - 1) / ?n2 (i - 1) = ?mu2 i (i - 1)" 
      unfolding gs2.μ.simps using i i0 by auto
    also have "?f1 ii  (?g1 (i - 1) - ?mu2 i (i - 1) v ?g2 (i - 1))
       = ?f1 ii  ?g1 (i - 1) - ?f1 ii  (?mu2 i (i - 1) v ?g2 (i - 1))" 
      by (rule scalar_prod_minus_distrib[OF g gs], insert gs2 ii i, auto)
    also have "?f1 ii  ?g1 (i - 1) = ?mu1 ii (i - 1) * ?n1 (i - 1)" 
      by (rule fs.gs.fi_scalar_prod_gso, insert conn1 ii im1, auto)
    also have "?f1 ii  (?mu2 i (i - 1) v ?g2 (i - 1)) = 
       ?mu2 i (i - 1) * (?f1 ii  ?g2 (i - 1))" 
      by (rule scalar_prod_smult_distrib, insert gs gs2 g i ii, auto)
    also have "?f1 ii  ?g2 (i - 1) = (?f1 ii  ?g2 (i - 1) / ?n2 (i - 1)) * ?n2 (i - 1)" 
      using norm0 by (auto simp: field_simps)
    also have "?f1 ii  ?g2 (i - 1) = ?f2 ii  ?g2 (i - 1)" 
      using len ii iii unfolding fs'_def by auto
    also have " / ?n2 (i - 1) = ?mu2 ii (i - 1)" unfolding gs2.μ.simps using iii by auto
    finally 
    have "?mu2 ii i = 
       (?mu1 ii (i - 1) * ?n1 (i - 1) - ?mu2 i (i - 1) * ?mu2 ii (i - 1) * ?n2 (i - 1)) / ?n2 i" by simp
    also have " = (?mu1 ii (i - 1) - ?mu1 i (i - 1) * ?mu2 ii (i - 1)) * ?n2 (i - 1) / ?n1 i" 
      unfolding sq_norm_g2_i mu'_mu_i_im1 using norm0 by (auto simp: field_simps)
    also have " = (?mu1 ii (i - 1) * ?n2 (i - 1) - 
      ?mu1 i (i - 1) * ((?mu1 ii i * ?n1 i + ?mu1 i (i - 1) * ?mu1 ii (i - 1) * ?n1 (i - 1)))) / ?n1 i" 
      unfolding mu'_mu_large_row_im1[OF iii ii] mu'_mu_i_im1 using norm0 by (auto simp: field_simps)
    also have " = ?mu1 ii (i - 1) - ?mu1 i (i - 1) * ?mu1 ii i" 
      unfolding sq_norm_g2_im1 using norm0 by (auto simp: field_simps)
    finally have "?mu2 ii i = ?mu1 ii (i - 1) - ?mu1 i (i - 1) * ?mu1 ii i" .
  } note mu'_mu_large_row_i = this


  {
    fix k assume k: "k < m" 
    show "?g2 k = ?newg k" 
      unfolding g2_i[symmetric] 
      unfolding g2_im1[symmetric]
      using g2_g1_identical[OF k] by auto
    show "?n2 k = ?new_norm k" 
      unfolding sq_norm_g2_i[symmetric]
      unfolding sq_norm_g2_im1[symmetric]
      using g2_g1_identical[OF k] by auto
    fix j assume jk: "j < k" hence j: "j < m" using k by auto
    have "k < i - 1  k = i - 1  k = i  k > i" by linarith
    thus "?mu2 k j = ?new_mu k j" 
      unfolding mu'_mu_i_im1[symmetric]
      using
        mu'_mu_large_row_i[OF _ k]
        mu'_mu_large_row_im1 [OF _ k]
        mu_no_change_large_row[OF _ k, of j]
        mu'_mu_small_i
        mu'_mu_i_im1_j jk j k
      by auto
  } note new_g = this

  { (* 16.13 (ii) : norm of g (i - 1) decreases by reduction factor *)
    note sq_norm_g2_im1
    also have "?n1 i + (?mu1 i (i - 1) * ?mu1 i (i - 1)) * ?n1 (i - 1)
      < 1/α * (?n1 (i - 1)) + (1/2 * 1/2) * (?n1 (i - 1))"
    proof (rule add_less_le_mono[OF _ mult_mono])
      from norm_ineq[unfolded mult.commute[of α],
          THEN linordered_field_class.mult_imp_less_div_pos[OF α0(1)]]
      show "?n1 i < 1/α * ?n1 (i - 1)" using len i by auto
      from m12 have abs: "abs (?mu1 i (i - 1))  1/2" by auto
      have "?mu1 i (i - 1) * ?mu1 i (i - 1)  abs (?mu1 i (i - 1)) * abs (?mu1 i (i - 1))" by auto
      also have "  1/2 * 1/2" using mult_mono[OF abs abs] by auto
      finally show "?mu1 i (i - 1) * ?mu1 i (i - 1)  1/2 * 1/2" by auto
    qed auto
    also have " = reduction * sq_norm (?g1 (i - 1))" unfolding reduction_def  
      using α0 by (simp add: ring_distribs add_divide_distrib)
    finally have "?n2 (i - 1) < reduction * ?n1 (i - 1)" .
  } note g_reduction = this (* Lemma 16.13 (ii) *)

  have lin_indpt_list_fs': "gs.lin_indpt_list (RAT fs')"
    unfolding gs.lin_indpt_list_def using conn2 by auto

  {
  (* stay reduced *)
    assume "LLL_invariant False i fs" 
    note inv = LLL_invD[OF this] 
    from inv have "weakly_reduced fs i" by auto
    hence "weakly_reduced fs (i - 1)" unfolding gram_schmidt_fs.weakly_reduced_def by auto
    hence red: "weakly_reduced fs' (i - 1)"
      unfolding gram_schmidt_fs.weakly_reduced_def using i G2_G by simp
    from inv have sred: "reduced fs i" by auto
    have sred: "reduced fs' (i - 1)"
      unfolding gram_schmidt_fs.reduced_def
    proof (intro conjI[OF red] allI impI, goal_cases)
      case (1 i' j)
      with sred have "¦?mu1 i' j¦  1 / 2" unfolding gram_schmidt_fs.reduced_def by auto
      thus ?case using mu'_mu_small_i[OF 1(1)] by simp
    qed
    have mu_small: "μ_small fs' (i - 1)" 
      unfolding μ_small_def
    proof (intro allI impI, goal_cases)
      case (1 j)
      thus ?case using inv(11) unfolding mu'_mu_i_im1_j[OF 1] μ_small_def by auto
    qed      
    show "LLL_invariant False (i - 1) fs'"
      by (rule LLL_invI, insert lin_indpt_list_fs' conn2 mu_small span' lattice fs' sred i, auto)
  } 

      
  (* invariant is established *)
  show newInvw: "LLL_invariant_weak fs'"
    by (rule LLL_inv_wI, insert lin_indpt_list_fs' conn2 span' lattice fs', auto)

  (* show decrease in measure *)
  { (* 16.16 (ii), the decreasing case *)
    have ile: "i  m" using i by auto
    from Gd[OF newInvw, folded d_def, OF ile] 
    have "?R (d fs' i) = (j<i. ?n2 j )" by auto
    also have " = prod ?n2 ({0 ..< i-1}  {i - 1})" 
      by (rule sym, rule prod.cong, (insert i0, auto)[1], insert i, auto)
    also have " = ?n2 (i - 1) * prod ?n2 ({0 ..< i-1})" 
      by simp
    also have "prod ?n2 ({0 ..< i-1}) = prod ?n1 ({0 ..< i-1})" 
      by (rule prod.cong[OF refl], subst g2_g1_identical, insert i, auto)
    also have " = (prod ?n1 ({0 ..< i-1}  {i - 1})) / ?n1 (i - 1)" 
      by (subst prod.union_disjoint, insert norm_pos1[OF im1], auto)
    also have "prod ?n1 ({0 ..< i-1}  {i - 1}) = prod ?n1 {0..<i}"
      by (rule arg_cong[of _ _ "prod ?n1"], insert i0, auto)
    also have " = (j<i. ?n1 j)"
      by (rule prod.cong, insert i0, auto)
    also have " = ?R (d fs i)" unfolding d_def Gd[OF Linvw ile]
      by (rule prod.cong[OF refl], insert i, auto)
    finally have new_di: "?R (d fs' i) = ?n2 (i - 1) / ?n1 (i - 1) * ?R (d fs i)" by simp
    also have " < (reduction * ?n1 (i - 1)) / ?n1 (i - 1) * ?R (d fs i)"
      by (rule mult_strict_right_mono[OF divide_strict_right_mono[OF g_reduction norm_pos1[OF im1]]],
        insert LLL_d_pos[OF Linvw] i, auto)  
    also have " = reduction * ?R (d fs i)" using norm_pos1[OF im1] by auto
    finally have "d fs' i < real_of_rat reduction * d fs i" 
      using of_rat_less of_rat_mult of_rat_of_int_eq by metis
    note this new_di
  } note d_i = this
  show "ii  m  ?R (d fs' ii) = (if ii = i then ?n2 (i - 1) / ?n1 (i - 1) * ?R (d fs i) else ?R (d fs ii))" 
    for ii using d_i d by auto
  have pos: "k < m  0 < d fs' k" "k < m  0  d fs' k" for k 
    using LLL_d_pos[OF newInvw, of k] by auto
  have prodpos:"0< (i<m. d fs' i)" apply (rule prod_pos)
    using LLL_d_pos[OF newInvw] by auto
  have prod_pos':"0 < (x{0..<m} - {i}. real_of_int (d fs' x))" apply (rule prod_pos)
    using LLL_d_pos[OF newInvw] pos by auto
  have prod_nonneg:"0  (x{0..<m} - {i}. real_of_int (d fs' x))" apply (rule prod_nonneg)
    using LLL_d_pos[OF newInvw] pos by auto
  have prodpos2:"0<(ia<m. d fs ia)" apply (rule prod_pos)
    using LLL_d_pos[OF Linvw] by auto
  have "D fs' = real_of_int (i<m. d fs' i)" unfolding D_def using prodpos by simp
  also have "(i<m. d fs' i) = ( j  {0 ..< m} - {i}  {i}. d fs' j)"
    by (rule prod.cong, insert i, auto)
  also have "real_of_int  = real_of_int ( j  {0 ..< m} - {i}. d fs' j) * real_of_int (d fs' i)" 
    by (subst prod.union_disjoint, auto)
  also have " < ( j  {0 ..< m} - {i}. d fs' j) * (of_rat reduction * d fs i)"
    by(rule mult_strict_left_mono[OF d_i(1)],insert prod_pos',auto)
  also have "( j  {0 ..< m} - {i}. d fs' j) = ( j  {0 ..< m} - {i}. d fs j)"
    by (rule prod.cong, insert d, auto)
  also have " * (of_rat reduction * d fs i) 
    = of_rat reduction * ( j  {0 ..< m} - {i}  {i}. d fs j)" 
    by (subst prod.union_disjoint, auto)
  also have "( j  {0 ..< m} - {i}  {i}. d fs j) = ( j<m. d fs j)" 
    by (subst prod.cong, insert i, auto)
  finally have D: "D fs' < real_of_rat reduction * D fs"
    unfolding D_def using prodpos2 by auto
  have logD: "logD fs' < logD fs" 
  proof (cases "α = 4/3")
    case True
    show ?thesis using D unfolding reduction(4)[OF True] logD_def unfolding True by simp
  next
    case False
    hence False': "α = 4/3  False" by simp
    from False α have "α > 4/3" by simp
    with reduction have reduction1: "reduction < 1" by simp
    let ?new = "real (D fs')" 
    let ?old = "real (D fs)" 
    let ?log = "log (1/of_rat reduction)" 
    note pos = LLL_D_pos[OF newInvw] LLL_D_pos[OF Linvw]
    from reduction have "real_of_rat reduction > 0" by auto
    hence gediv:"1/real_of_rat reduction > 0" by auto
    have "(1/of_rat reduction) * ?new  ((1/of_rat reduction) * of_rat reduction) * ?old"
      unfolding mult.assoc mult_le_cancel_left_pos[OF gediv] using D by simp
    also have "(1/of_rat reduction) * of_rat reduction = 1" using reduction by auto
    finally have "(1/of_rat reduction) * ?new  ?old" by auto
    hence "?log ((1/of_rat reduction) * ?new)  ?log ?old"
      by (subst log_le_cancel_iff, auto simp: pos reduction1 reduction)
    hence "floor (?log ((1/of_rat reduction) * ?new))  floor (?log ?old)" 
      by (rule floor_mono)
    hence "nat (floor (?log ((1/of_rat reduction) * ?new)))  nat (floor (?log ?old))" by simp
    also have " = logD fs" unfolding logD_def False' by simp
    also have "?log ((1/of_rat reduction) * ?new) = 1 + ?log ?new" 
      by (subst log_mult, insert reduction reduction1, auto simp: pos )
    also have "floor (1 + ?log ?new) = 1 + floor (?log ?new)" by simp
    also have "nat (1 + floor (?log ?new)) = 1 + nat (floor (?log ?new))" 
      by (subst nat_add_distrib, insert pos reduction reduction1, auto)
    also have "nat (floor (?log ?new)) = logD fs'" unfolding logD_def False' by simp
    finally show "logD fs' < logD fs" by simp
  qed
  show "LLL_measure i fs > LLL_measure (i - 1) fs'" unfolding LLL_measure_def 
    using i logD by simp
qed

lemma LLL_inv_initial_state: "LLL_invariant True 0 fs_init" 
proof - 
  from lin_dep[unfolded gs.lin_indpt_list_def]
  have "set (RAT fs_init)  Rn" by auto
  hence fs_init: "set fs_init  carrier_vec n" by auto
  show ?thesis 
    by (rule LLL_invI[OF fs_init len _ _ lin_dep], auto simp: L_def gs.reduced_def gs.weakly_reduced_def)
qed

lemma LLL_inv_m_imp_reduced: assumes "LLL_invariant True m fs" 
  shows "reduced fs m" 
  using LLL_invD[OF assms] by blast

lemma basis_reduction_short_vector: assumes LLL_inv: "LLL_invariant True m fs" 
  and v: "v = hd fs" 
  and m0: "m  0"
shows "v  carrier_vec n"
  "v  L - {0v n}"  
  "h  L - {0v n}  rat_of_int (sq_norm v)  α ^ (m - 1) * rat_of_int (sq_norm h)" 
  "v  0v j" 
proof -
  let ?L = "lattice_of fs_init" 
  have a1: "α  1" using α by auto 
  from LLL_invD[OF LLL_inv] have
    L: "lattice_of fs = L" 
    and red: "gram_schmidt_fs.weakly_reduced n (RAT fs) α (length (RAT fs))" 
    and basis: "lin_indep fs" 
    and lenH: "length fs = m" 
    and H: "set fs  carrier_vec n" 
    by (auto simp: gs.lin_indpt_list_def gs.reduced_def)
  from lin_dep have G: "set fs_init  carrier_vec n" unfolding gs.lin_indpt_list_def by auto
  with m0 len have "dim_vec (hd fs_init) = n" by (cases fs_init, auto)
  from v m0 lenH v have v: "v = fs ! 0" by (cases fs, auto)
  interpret gs1: gram_schmidt_fs_lin_indpt n "RAT fs"
    by (standard) (use assms LLL_invariant_def gs.lin_indpt_list_def in auto)
  let ?r = "rat_of_int" 
  let ?rv = "map_vec ?r" 
  let ?F = "RAT fs" 
  let ?h = "?rv h" 
  { assume h:"h  L - {0v n}" (is ?h_req)
    from h[folded L] have h: "h  lattice_of fs" "h  0v n" by auto
    {
      assume f: "?h = 0v n" 
      have "?h = ?rv (0v n)" unfolding f by (intro eq_vecI, auto)
      hence "h = 0v n"
        using of_int_hom.vec_hom_zero_iff[of h] of_int_hom.vec_hom_inj by auto
      with h have False by simp
    } hence h0: "?h  0v n" by auto
    with lattice_of_of_int[OF H h(1)]
    have "?h  gs.lattice_of ?F - {0v n}" by auto
  } 
  from gs1.weakly_reduced_imp_short_vector[OF red this a1] lenH
  show "h  L - {0v n}  ?r (sq_norm v)  α ^ (m - 1) * ?r (sq_norm h)"
    using basis unfolding L v gs.lin_indpt_list_def  by (auto simp: sq_norm_of_int)
  from m0 H lenH show vn: "v  carrier_vec n" unfolding v by (cases fs, auto)
  have vL: "v  L" unfolding L[symmetric] v using m0 H lenH
    by (intro basis_in_latticeI, cases fs, auto)
  {
    assume "v = 0v n" 
    hence "hd ?F = 0v n" unfolding v using m0 lenH by (cases fs, auto)
    with gs.lin_indpt_list_nonzero[OF basis] have False using m0 lenH by (cases fs, auto)
  }
  with vL show v: "v  L - {0v n}" by auto
  have jn:"0v j  carrier_vec n  j = n" unfolding zero_vec_def carrier_vec_def by auto
  with v vn show "v  0v j" by auto
qed


lemma LLL_mu_d_Z: assumes inv: "LLL_invariant_weak fs" 
  and j: "j  ii" and ii: "ii < m" 
shows "of_int (d fs (Suc j)) * μ fs ii j  "
proof -
  interpret fs: fs_int' n m fs_init fs
    by standard (use inv in auto)
  show ?thesis
    using assms fs.fs_int_mu_d_Z LLL_inv_wD[OF inv] unfolding d_def fs.d_def by auto
qed

context fixes fs
  assumes Linv: "LLL_invariant_weak fs" and gbnd: "g_bound fs" 
begin

interpretation gs1: gram_schmidt_fs_lin_indpt n "RAT fs"
  by (standard) (use Linv LLL_invariant_weak_def gs.lin_indpt_list_def in auto)

lemma LLL_inv_N_pos: assumes m: "m  0" 
shows "N > 0" 
proof -
  let ?r = rat_of_int
  note inv = LLL_inv_wD[OF Linv]
  from inv have F: "RAT fs ! 0  Rn" "fs ! 0  carrier_vec n" using m by auto
  from m have upt: "[0..< m] = 0 # [1 ..< m]" using upt_add_eq_append[of 0 1 "m - 1"] by auto
  from inv(6) m have "map_vec ?r (fs ! 0)  0v n" using gs.lin_indpt_list_nonzero[OF inv(1)]
    unfolding set_conv_nth by force
  hence F0: "fs ! 0  0v n" by auto
  hence "sq_norm (fs ! 0)  0" using F by simp
  hence 1: "sq_norm (fs ! 0)  1" using sq_norm_vec_ge_0[of "fs ! 0"] by auto
  from gbnd m have "sq_norm (gso fs 0)  of_nat N" unfolding g_bound_def by auto
  also have "gso fs 0 = RAT fs ! 0" unfolding upt using F by (simp add: gs1.gso.simps[of 0])
  also have "RAT fs ! 0 = map_vec ?r (fs ! 0)" using inv(6) m by auto
  also have "sq_norm  = ?r (sq_norm (fs ! 0))" by (simp add: sq_norm_of_int)
  finally show ?thesis using 1 by (cases N, auto)
qed


(* equation (3) in front of Lemma 16.18 *)
lemma d_approx_main: assumes i: "ii  m" "m  0" 
shows "rat_of_int (d fs ii)  rat_of_nat (N^ii)" 
proof -
  note inv = LLL_inv_wD[OF Linv]
  from LLL_inv_N_pos i have A: "0 < N" by auto
  note main = inv(2)[unfolded gram_schmidt_int_def gram_schmidt_wit_def]
  have "rat_of_int (d fs ii) = (j<ii. gso fs j2)" unfolding d_def using i
    by (auto simp: Gramian_determinant [OF Linv])
  also have "  (j<ii. of_nat N)" using i
    by (intro prod_mono ballI conjI prod_nonneg, insert gbnd[unfolded g_bound_def], auto)
  also have " = (of_nat N)^ii" unfolding prod_constant by simp
  also have " = of_nat (N^ii)" by simp
  finally show ?thesis by simp
qed

lemma d_approx: assumes i: "ii < m"  
  shows "rat_of_int (d fs ii)  rat_of_nat (N^ii)" 
  using d_approx_main[of ii] assms by auto


lemma d_bound: assumes i: "ii < m" 
  shows "d fs ii  N^ii" 
  using d_approx[OF assms] unfolding d_def by linarith


lemma D_approx: "D fs  N ^ (m * m)" 
proof - 
  note inv = LLL_inv_wD[OF Linv]
  from LLL_inv_N_pos have N: "m  0  0 < N" by auto
  note main = inv(2)[unfolded gram_schmidt_int_def gram_schmidt_wit_def]
  have "rat_of_int (i<m. d fs i) = (i<m. rat_of_int (d fs i))" by simp
  also have "  (i<m. (of_nat N) ^ i)" 
    by (rule prod_mono, insert d_approx LLL_d_pos[OF Linv], auto simp: less_le)
  also have "  (i<m. (of_nat N ^ m))" 
    by (rule prod_mono, insert N, auto intro: pow_mono_exp)
  also have " = (of_nat N)^(m * m)" unfolding prod_constant power_mult by simp
  also have " = of_nat (N ^ (m * m))" by simp
  finally have "(i<m. d fs i)  N ^ (m * m)" by linarith
  also have "(i<m. d fs i) = D fs" unfolding D_def 
    by (subst nat_0_le, rule prod_nonneg, insert LLL_d_pos[OF Linv], auto simp: le_less)  
  finally show "D fs  N ^ (m * m)" by linarith 
qed


lemma LLL_measure_approx: assumes "α > 4/3" "m  0" 
shows "LLL_measure i fs  m + 2 * m * m * log base N"
proof -   
  have b1: "base > 1" using base assms by auto
  have id: "base = 1 / real_of_rat reduction" unfolding base_def reduction_def using α0 by
    (auto simp: field_simps of_rat_divide)
  from LLL_D_pos[OF Linv] have D1: "real (D fs)  1" by auto
  note invD = LLL_inv_wD[OF Linv]  
  from invD
  have F: "set fs  carrier_vec n" and len: "length fs = m" by auto
  have N0: "N > 0" using LLL_inv_N_pos[OF assms(2)] .
  from D_approx 
  have D: "D fs  N ^ (m * m)" .
  hence "real (D fs)  real (N ^ (m * m))" by linarith
  also have " = real N ^ (m * m)" by simp
  finally have log: "log base (real (D fs))  log base (real N ^ (m * m))"   
    by (subst log_le_cancel_iff[OF b1], insert D1 N0, auto)

  have "real (logD fs) = real (nat log base (real (D fs)))" 
    unfolding logD_def id using assms by auto
  also have "  log base (real (D fs))" using b1 D1 by auto
  also have "  log base (real N ^ (m * m))" by fact
  also have " = (m * m) * log base (real N)" 
    by (rule log_nat_power, insert N0, auto)
  finally have main: "logD fs  m * m * log base N" by simp

  have "real (LLL_measure i fs) = real (2 * logD fs + m - i)"
    unfolding LLL_measure_def split invD(1) by simp
  also have "  2 * real (logD fs) + m" using invD by simp
  also have "  2 * (m * m * log base N) + m" using main by auto
  finally show ?thesis by simp
qed
end

lemma g_bound_fs_init: "g_bound fs_init" 
proof -
  {
    fix i
    assume i: "i < m" 
    let ?N = "map (nat o sq_norm) fs_init"
    let ?r = rat_of_int
    from i have mem: "nat (sq_norm (fs_init ! i))  set ?N" using fs_init len unfolding set_conv_nth by force
    interpret gs: gram_schmidt_fs_lin_indpt n "RAT fs_init"
      by (standard) (use len lin_dep LLL_invariant_def gs.lin_indpt_list_def in auto)
    from mem_set_imp_le_max_list[OF _ mem]
    have FN: "nat (sq_norm (fs_init ! i))  N" unfolding N_def by force
    hence "fs_init ! i2  int N" using i by auto
    also have "  int (N * m)" using i by fastforce
    finally have f_bnd:  "fs_init ! i2  int (N * m)" .
    from FN have "rat_of_nat (nat (sq_norm (fs_init ! i)))  rat_of_nat N" by simp
    also have "rat_of_nat (nat (sq_norm (fs_init ! i))) = ?r (sq_norm (fs_init ! i))" 
      using sq_norm_vec_ge_0[of "fs_init ! i"] by auto
    also have " = sq_norm (RAT fs_init ! i)" unfolding sq_norm_of_int[symmetric] using fs_init len i by auto
    finally have "sq_norm (RAT fs_init ! i)  rat_of_nat N" .
    with gs.sq_norm_gso_le_f i len lin_dep
    have g_bnd: "gs.gso i2  rat_of_nat N"
      unfolding gs.lin_indpt_list_def by fastforce
    note f_bnd g_bnd
  }
  thus "g_bound fs_init" unfolding g_bound_def by auto
qed

lemma LLL_measure_approx_fs_init: 
  "LLL_invariant upw i fs_init  4 / 3 < α  m  0  
  real (LLL_measure i fs_init)  real m + real (2 * m * m) * log base (real N)" 
  using LLL_measure_approx[OF LLL_inv_imp_w g_bound_fs_init] .

lemma N_le_MMn: assumes m0: "m  0" 
  shows "N  nat M * nat M * n" 
  unfolding N_def
proof (rule max_list_le, unfold set_map o_def)
  fix ni
  assume "ni  (λx. nat x2) ` set fs_init" 
  then obtain fi where ni: "ni = nat (fi2)" and fi: "fi  set fs_init" by auto
  from fi len obtain i where fii: "fi = fs_init ! i" and i: "i < m" unfolding set_conv_nth by auto
  from fi fs_init have fi: "fi  carrier_vec n" by auto
  let ?set = "{¦fs_init ! i $ j¦ |i j. i < m  j < n}  {0}" 
  have id: "?set = (λ (i,j). abs (fs_init ! i $ j)) ` ({0..<m} × {0..<n})  {0}" 
    by force
  have fin: "finite ?set" unfolding id by auto
  { 
    fix j assume "j < n" 
    hence "M  ¦fs_init ! i $ j¦" unfolding M_def using i
      by (intro Max_ge[of _ "abs (fs_init ! i $ j)"], intro fin, auto)
  } note M = this
  from Max_ge[OF fin, of 0] have M0: "M  0" unfolding M_def by auto
  have "ni = nat (fi2)" unfolding ni by auto
  also have "  nat (int n * fi2)" using sq_norm_vec_le_linf_norm[OF fi]
    by (intro nat_mono, auto)
  also have " = n * nat (fi2)"
    by (simp add: nat_mult_distrib)
  also have "  n * nat (M^2)" 
  proof (rule mult_left_mono[OF nat_mono])
    have fi: "fi  M" unfolding linf_norm_vec_def    
    proof (rule max_list_le, unfold set_append set_map, rule ccontr)
      fix x
      assume "x  abs ` set (list_of_vec fi)  set [0]" and xM: "¬ x  M"  
      with M0 obtain fij where fij: "fij  set (list_of_vec fi)" and x: "x = abs fij" by auto
      from fij fi obtain j where j: "j < n" and fij: "fij = fi $ j" 
        unfolding set_list_of_vec vec_set_def by auto
      from M[OF j] xM[unfolded x fij fii] show False by auto
    qed auto                
    show "fi2  M^2" unfolding abs_le_square_iff[symmetric] using fi 
      using linf_norm_vec_ge_0[of fi] by auto
  qed auto
  finally show "ni  nat M * nat M * n" using M0 
    by (subst nat_mult_distrib[symmetric], auto simp: power2_eq_square ac_simps)
qed (insert m0 len, auto)



subsection ‹Basic LLL implementation based on previous results›

text ‹We now assemble a basic implementation of the LLL algorithm,
  where only the lattice basis is updated, and where the GSO and the $\mu$-values
  are always computed from scratch. This enables a simple soundness proof 
  and permits to separate an efficient implementation from the soundness reasoning.›

fun basis_reduction_add_rows_loop where
  "basis_reduction_add_rows_loop i fs 0 = fs" 
| "basis_reduction_add_rows_loop i fs (Suc j) = (
     let c = round (μ fs i j);
         fs' = (if c = 0 then fs else fs[ i := fs ! i - c v fs ! j])
      in basis_reduction_add_rows_loop i fs' j)" 

definition basis_reduction_add_rows where
  "basis_reduction_add_rows upw i fs = 
     (if upw then basis_reduction_add_rows_loop i fs i else fs)" 

definition basis_reduction_swap where
  "basis_reduction_swap i fs = (False, i - 1, fs[i := fs ! (i - 1), i - 1 := fs ! i])" 

definition basis_reduction_step where
  "basis_reduction_step upw i fs = (if i = 0 then (True, Suc i, fs)
     else let 
       fs' = basis_reduction_add_rows upw i fs
     in if sq_norm (gso fs' (i - 1))  α * sq_norm (gso fs' i) then
          (True, Suc i, fs') 
        else basis_reduction_swap i fs')" 

function basis_reduction_main where
  "basis_reduction_main (upw,i,fs) = (if i < m  LLL_invariant upw i fs
     then basis_reduction_main (basis_reduction_step upw i fs) else
     fs)"
  by pat_completeness auto

definition "reduce_basis = basis_reduction_main (True, 0, fs_init)" 

definition "short_vector = hd reduce_basis" 

text ‹Soundness of this implementation is easily proven›

lemma basis_reduction_add_rows_loop: assumes 
  inv: "LLL_invariant True i fs" 
  and mu_small: "μ_small_row i fs j"
  and res: "basis_reduction_add_rows_loop i fs j = fs'" 
  and i: "i < m" 
  and j: "j  i" 
shows "LLL_invariant False i fs'" "LLL_measure i fs' = LLL_measure i fs" 
proof (atomize(full), insert assms, induct j arbitrary: fs)
  case (0 fs)
  thus ?case using basis_reduction_add_row_done[of i fs] by auto
next
  case (Suc j fs)
  hence j: "j < i" by auto
  let ?c = "round (μ fs i j)" 
  show ?case
  proof (cases "?c = 0")
    case True
    thus ?thesis using Suc(1)[OF Suc(2) basis_reduction_add_row_main_0[OF LLL_inv_imp_w[OF Suc(2)] i j True Suc(3)]]
      Suc(2-) by auto
  next
    case False
    note step = basis_reduction_add_row_main(2-)[OF LLL_inv_imp_w[OF Suc(2)] i j refl]
    note step = step(1)[OF Suc(2)] step(2-)
    show ?thesis using Suc(1)[OF step(1-2)] False Suc(2-) step(4) by simp
  qed
qed

lemma basis_reduction_add_rows: assumes 
  inv: "LLL_invariant upw i fs" 
  and res: "basis_reduction_add_rows upw i fs = fs'" 
  and i: "i < m" 
shows "LLL_invariant False i fs'" "LLL_measure i fs' = LLL_measure i fs" 
proof (atomize(full), goal_cases)
  case 1
  note def = basis_reduction_add_rows_def
  show ?case
  proof (cases upw)
    case False
    with res inv show ?thesis by (simp add: def)
  next
    case True
    with inv have "LLL_invariant True i fs" by auto
    note start = this μ_small_row_refl[of i fs]
    from res[unfolded def] True have "basis_reduction_add_rows_loop i fs i = fs'" by auto
    from basis_reduction_add_rows_loop[OF start this i]
    show ?thesis by auto
  qed
qed

lemma basis_reduction_swap: assumes 
  inv: "LLL_invariant False i fs" 
  and res: "basis_reduction_swap i fs = (upw',i',fs')" 
  and cond: "sq_norm (gso fs (i - 1)) > α * sq_norm (gso fs i)" 
  and i: "i < m" "i  0" 
shows "LLL_invariant upw' i' fs'" (is ?g1)
  "LLL_measure i' fs' < LLL_measure i fs" (is ?g2)
proof -
  note invw = LLL_inv_imp_w[OF inv]
  note def = basis_reduction_swap_def
  from res[unfolded basis_reduction_swap_def]
  have id: "upw' = False" "i' = i - 1" "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]" by auto
  from basis_reduction_swap_main(2-3)[OF invw _ i cond id(3)] inv show ?g1 ?g2 unfolding id by auto
qed

lemma basis_reduction_step: assumes 
  inv: "LLL_invariant upw i fs" 
  and res: "basis_reduction_step upw i fs = (upw',i',fs')" 
  and i: "i < m" 
shows "LLL_invariant upw' i' fs'" "LLL_measure i' fs' < LLL_measure i fs" 
proof (atomize(full), goal_cases)
  case 1
  note def = basis_reduction_step_def
  note invw = LLL_inv_imp_w[OF inv]
  obtain fs'' where fs'': "basis_reduction_add_rows upw i fs = fs''" by auto
  show ?case
  proof (cases "i = 0")
    case True
    from increase_i[OF inv i] True
      res show ?thesis by (auto simp: def)
  next
    case False
    hence id: "(i = 0) = False" by auto
    note res = res[unfolded def id if_False fs'' Let_def]
    let ?x = "sq_norm (gso fs'' (i - 1))" 
    let ?y = "α * sq_norm (gso fs'' i)" 
    from basis_reduction_add_rows[OF inv fs'' i]
    have inv: "LLL_invariant False i fs''"
      and meas: "LLL_measure i fs'' = LLL_measure i fs" by auto
    note invw = LLL_inv_imp_w[OF inv]
    show ?thesis
    proof (cases "?x  ?y")
      case True
      from increase_i[OF inv i] id True res meas
      show ?thesis by simp
    next
      case gt: False
      hence "?x > ?y" by auto
      from basis_reduction_swap[OF inv _ this i False] gt res meas
      show ?thesis by auto
    qed
  qed
qed

termination by (relation "measure (λ (upw,i,fs). LLL_measure i fs)", insert basis_reduction_step, auto split: prod.splits)

declare basis_reduction_main.simps[simp del]

lemma basis_reduction_main: assumes "LLL_invariant upw i fs" 
  and res: "basis_reduction_main (upw,i,fs) = fs'" 
shows "LLL_invariant True m fs'" 
  using assms
proof (induct "LLL_measure i fs" arbitrary: i fs upw rule: less_induct)
  case (less i fs upw)
  have id: "LLL_invariant upw i fs = True" using less by auto
  note res = less(3)[unfolded basis_reduction_main.simps[of upw i fs] id]
  note inv = less(2)
  note IH = less(1)
  show ?case
  proof (cases "i < m")
    case i: True
    obtain i' fs' upw' where step: "basis_reduction_step upw i fs = (upw',i',fs')" 
      (is "?step = _") by (cases ?step, auto)
    from IH[OF basis_reduction_step(2,1)[OF inv step i]] res[unfolded step] i
    show ?thesis by auto
  next
    case False
    with LLL_invD[OF inv] have i: "i = m" by auto
    with False res inv have "LLL_invariant upw m fs'" by auto
    thus "LLL_invariant True m fs'" unfolding LLL_invariant_def by auto
  qed
qed

lemma reduce_basis_inv: assumes res: "reduce_basis = fs" 
  shows "LLL_invariant True m fs" 
  using basis_reduction_main[OF LLL_inv_initial_state res[unfolded reduce_basis_def]] .

lemma reduce_basis: assumes res: "reduce_basis = fs"
  shows "lattice_of fs = L" 
  "reduced fs m" 
  "lin_indep fs" 
  "length fs = m" 
  using LLL_invD[OF reduce_basis_inv[OF res]] by blast+
  
lemma short_vector: assumes res: "short_vector = v" 
  and m0: "m  0"
shows "v  carrier_vec n"
  "v  L - {0v n}"  
  "h  L - {0v n}  rat_of_int (sq_norm v)  α ^ (m - 1) * rat_of_int (sq_norm h)" 
  "v  0v j" 
  using basis_reduction_short_vector[OF reduce_basis_inv[OF refl] res[symmetric, unfolded short_vector_def] m0] 
  by blast+
end

end