# Theory Storjohann_Mod_Operation

section ‹Storjohann's Lemma 13›

text ‹This theory contains the result that one can always perform a mod-operation on
the entries of the $d\mu$-matrix.›

theory Storjohann_Mod_Operation
imports
LLL_Basis_Reduction.LLL_Certification
Signed_Modulo
begin

lemma map_vec_map_vec: "map_vec f (map_vec g v) = map_vec (f o g) v"
by (intro eq_vecI, auto)

context semiring_hom
begin

(* TODO: move *)
lemma mat_hom_add: assumes A: "A  carrier_mat nr nc" and B: "B  carrier_mat nr nc"
shows "math (A + B) = math A + math B"
by (intro eq_matI, insert A B, auto simp: hom_add)
end

text ‹We now start to prove lemma 13 of Storjohann's paper.›
context
fixes A I :: "'a :: field mat" and n :: nat
assumes A: "A  carrier_mat n n"
and det: "det A  0"
and I: "I = the (mat_inverse A)"
begin
lemma inverse_via_det: "I * A = 1m n" "A * I = 1m n" "I  carrier_mat n n"
"I = mat n n (λ (i,j). det (replace_col A (unit_vec n j) i) / det A)"
proof -
from det_non_zero_imp_unit[OF A det]
have Unit: "A  Units (ring_mat TYPE('a) n n)" .
from mat_inverse(1)[OF A, of n] Unit I have "mat_inverse A = Some I"
by (cases "mat_inverse A", auto)
from mat_inverse(2)[OF A this]
show left: "I * A = 1m n" and right: "A * I = 1m n" and I: "I  carrier_mat n n"
by blast+
{
fix i j
assume i: "i < n" and j: "j < n"
from I i j have cI: "col I j $i = I $$(i,j)" by simp from j have uv: "unit_vec n j carrier_vec n" by auto from j I have col: "col I j carrier_vec n" by auto from col_mult2[OF A I j, unfolded right] j have "A *v col I j = unit_vec n j" by simp from cramer_lemma_mat[OF A col i, unfolded this cI] have "I$$ (i,j) = det (replace_col A (unit_vec n j) i) / det A" using det by simp } thus "I = mat n n (λ (i,j). det (replace_col A (unit_vec n j) i) / det A)" by (intro eq_matI, use I in auto) qed lemma matrix_for_singleton_entry: assumes i: "i < n" and j: "j < n" and Rdef: "R = mat n n ( λ ij. if ij = (i,j) then c :: 'a else 0)" shows "mat n n (λ(i', j'). if i' = i then c * det (replace_col A (unit_vec n j') j) / det A else 0) * A = R" proof - note I = inverse_via_det(3) have R: "R carrier_mat n n" unfolding Rdef by auto have "(R * I) * A = R * (I * A)" using I A R by auto also have "I * A = 1m n" unfolding inverse_via_det(1) .. also have "R * = R" using R by simp also have "R * I = mat n n (λ (i',j'). row R i' col I j')" using I R unfolding times_mat_def by simp also have " = mat n n ( λ (i',j'). if i' = i then c * I $$(j, j') else 0)" (is "mat n n ?f = mat n n ?g") proof - { fix i' j' assume i': "i' < n" and j': "j' < n" have "?f (i',j') = ?g (i',j')" proof (cases "i' = i") case False hence "row R i' = 0v n" unfolding Rdef using i' by (intro eq_vecI, auto simp: Matrix.row_def) thus ?thesis using False i' j' I by simp next case True hence "row R i' = c v unit_vec n j" unfolding Rdef using i' j' i j by (intro eq_vecI, auto simp: Matrix.row_def) with True show ?thesis using i' j' I j by simp qed } thus ?thesis by auto qed finally show ?thesis unfolding inverse_via_det(4) using j by (auto intro!: arg_cong[of _ _ "λ x. x * A"]) qed end lemma (in gram_schmidt_fs_Rn) det_M_1: "det (M m) = 1" proof - have "det (M m) = prod_list (diag_mat (M m))" by (rule det_lower_triangular[of m], auto simp: μ.simps) also have " = 1" by (rule prod_list_neutral, auto simp: diag_mat_def μ.simps) finally show ?thesis . qed context gram_schmidt_fs_int begin lemma assumes IM: "IM = the (mat_inverse (M m))" shows inv_mu_lower_triangular: " k i. k < i i < m IM$$ (k, i) = 0" and inv_mu_diag: " k. k < m IM $$(k, k) = 1" and d_inv_mu_integer: " i j. i < m j < m d i * IM$$ (i,j) " and inv_mu_inverse: "IM * M m = 1m m" "M m * IM = 1m m" "IM carrier_mat m m" proof - note * = inverse_via_det[OF M_dim(3) _ IM, unfolded det_M_1] from * show inv: "IM * M m = 1m m" "M m * IM = 1m m" and IM: "IM carrier_mat m m" by auto from * have IM_det: "IM = mat m m (λ(i, j). det (replace_col (M m) ((unit_vec m) j) i))" by auto from matrix_equality have "IM * FF = IM * ((M m) * Fs)" by simp also have " = (IM * M m) * Fs" using M_dim(3) IM Fs_dim(3) by (metis assoc_mult_mat) also have " = Fs" unfolding inv using Fs_dim(3) by simp finally have equality: "IM * FF = Fs" . { fix i k assume i: "k < i" "i < m" show "IM $$(k, i) = 0" using i M_dim unfolding IM_det by (simp, subst det_lower_triangular[of m], auto simp: replace_col_def μ.simps diag_mat_def) } note IM_lower_triag = this { fix k assume k: "k < m" show "IM$$ (k,k) = 1" using k M_dim unfolding IM_det by (simp, subst det_lower_triangular[of m], auto simp: replace_col_def μ.simps diag_mat_def intro!: prod_list_neutral) } note IM_diag_1 = this { fix k assume k: "k < m" let ?f = "λ i. IM $$(k, i) v fs ! i" let ?sum = "M.sumlist (map ?f [0..<m])" let ?sumk = "M.sumlist (map ?f [0..<k])" have set: "set (map ?f [0..<m]) carrier_vec n" using fs_carrier by auto hence sum: "?sum carrier_vec n" by simp from set k have setk: "set (map ?f [0..<k]) carrier_vec n" by auto hence sumk: "?sumk carrier_vec n" by simp from sum have dim_sum: "dim_vec ?sum = n" by simp have "gso k = row Fs k" using k by auto also have " = row (IM * FF) k" unfolding equality .. also have "IM * FF = mat m n (λ (i,j). row IM i col FF j)" unfolding times_mat_def using IM FF_dim by auto also have "row k = vec n (λ j. row IM k col FF j)" unfolding Matrix.row_def using IM FF_dim k by auto also have " = vec n (λ j. i < m. IM$$ (k, i) * fs ! i$ j)"
by (intro eq_vecI, insert IM k, auto simp: scalar_prod_def Matrix.row_def intro!: sum.cong)
also have " = ?sum"
by (intro eq_vecI, insert IM, unfold dim_sum, subst sumlist_vec_index,
auto simp: o_def sum_list_sum_nth intro!: sum.cong)
also have "[0..<m] = [0..<k] @ [k] @ [Suc k ..<m]" using k
also have "M.sumlist (map ?f ) = ?sumk +
(?f k + M.sumlist (map ?f [Suc k ..< m]))"
unfolding map_append
by (subst M.sumlist_append; (subst M.sumlist_append)?, insert k fs_carrier, auto)
also have "M.sumlist (map ?f [Suc k ..< m]) = 0v n"
by (rule sumlist_neutral, insert IM_lower_triag, auto)
also have "IM $$(k,k) = 1" using IM_diag_1[OF k] . finally have gso: "gso k = ?sumk + fs ! k" using k by simp define b where "b = vec k (λ j. fs ! j fs ! k)" { fix j assume jk: "j < k" with k have j: "j < m" by auto have "fs ! j gso k = fs ! j (?sumk + fs ! k)" unfolding gso by simp also have "fs ! j gso k = 0" using jk k by (simp add: fi_scalar_prod_gso gram_schmidt_fs.μ.simps) also have "fs ! j (?sumk + fs ! k) = fs ! j ?sumk + fs ! j fs ! k" by (rule scalar_prod_add_distrib[OF _ sumk], insert j k, auto) also have "fs ! j fs ! k = b  j" unfolding b_def using jk by simp finally have "b  j = - (fs ! j ?sumk)" by linarith } note b_index = this let ?x = "vec k (λ i. - IM$$ (k, i))"
have x: "?x  carrier_vec k" by auto
from k have km: "k  m" by simp
have bGx: "b = Gramian_matrix fs k *v (vec k (λ i. - IM $$(k, i)))" unfolding Gramian_matrix_alt_alt_def[OF km] proof (rule eq_vecI; simp) fix i assume i: "i < k" have "b  i = - (x[0..<k]. fs ! i (IM$$ (k, x) v fs ! x))"
unfolding b_index[OF i]
by (subst scalar_prod_right_sum_distrib, insert setk i k, auto simp: o_def)
also have " = vec k (λj. fs ! i  fs ! j)  vec k (λi. - IM $$(k, i))" by (subst (3) scalar_prod_def, insert i k, auto simp: o_def sum_list_sum_nth simp flip: sum_negf intro!: sum.cong) finally show "b  i = vec k (λj. fs ! i fs ! j) vec k (λi. - IM$$ (k, i))" .
have G: "Gramian_matrix fs k  carrier_mat k k"
unfolding Gramian_matrix_alt_alt_def[OF km] by simp
from cramer_lemma_mat[OF G x, folded bGx Gramian_determinant_def]
have "i < k
d k * IM $$(k, i) = - det (replace_col (Gramian_matrix fs k) (vec k (λ j. fs ! j fs ! k)) i)" for i unfolding b_def by simp } note IM_lower_values = this { fix i j assume i: "i < m" and j: "j < m" from i have im: "i m" by auto consider (1) "j < i" | (2) "j = i" | (3) "i < j" by linarith thus "d i * IM$$ (i,j)  "
proof cases
case 1
show ?thesis unfolding IM_lower_values[OF i 1] replace_col_def Gramian_matrix_alt_alt_def[OF im]
by (intro Ints_minus Ints_det, insert i j, auto intro!: Ints_scalar_prod[of _ n] fs_int)
next
case 3
show ?thesis unfolding IM_lower_triag[OF 3 j] by simp
next
case 2
show ?thesis unfolding IM_diag_1[OF i] 2 using i unfolding Gramian_determinant_def
Gramian_matrix_alt_alt_def[OF im]
by (intro Ints_mult Ints_det, insert i j, auto intro!: Ints_scalar_prod[of _ n] fs_int)
qed
}
qed

definition inv_mu_ij_mat :: "nat  nat  int  int mat" where
"inv_mu_ij_mat i j c = (let
B = mat m m (λ ij. if ij = (i,j) then c else 0);
C = mat m m (λ (i,j). the_inv (of_int :: _  'a) (d i * the (mat_inverse (M m)) $$(i,j))) in B * C + 1m m)" lemma inv_mu_ij_mat: assumes i: "i < m" and ji: "j < i" shows (* Effect on μ *) "map_mat of_int (inv_mu_ij_mat i j c) * M m = mat m m (λij. if ij = (i, j) then of_int c * d j else 0) + M m" (* only change value of μ_ij *) (* Effect on A *) "A carrier_mat m n c mod p = 0 map_mat (λ x. x mod p) (inv_mu_ij_mat i j c * A) = (map_mat (λ x. x mod p) A)" (* no change (mod p) *) (* The transformation-matrix is ... *) "inv_mu_ij_mat i j c carrier_mat m m" (* ... of dimension m*m *) "i' < j' j' < m inv_mu_ij_mat i j c$$ (i',j') = 0" (* ... lower triangular *)
"k < m  inv_mu_ij_mat i j c $$(k,k) = 1" (* ... with diagonal all 1 *) proof - obtain IM where IM: "IM = the (mat_inverse (M m))" by auto let ?oi = "of_int :: _ 'a" let ?C = "mat m m (λ ij. if ij = (i,j) then ?oi c else 0)" let ?D = "mat m m (λ (i,j). d i * IM$$ (i,j))"
have oi: "inj ?oi" unfolding inj_on_def by auto
have C: "?C  carrier_mat m m" by auto
from i ji have j: "j < m" by auto
from j have jm: "{0..<m} = {0..<j}  {j}  {Suc j..<m}" by auto
note IM_props = d_inv_mu_integer[OF IM] inv_mu_inverse[OF IM]
have mat_oi: "map_mat ?oi (inv_mu_ij_mat i j c) = ?C * ?D + 1m m" (is "?MM = _")
unfolding inv_mu_ij_mat_def Let_def IM[symmetric]
apply (rule arg_cong2[of _ _ _ _ ""])
apply (subst of_int_hom.mat_hom_mult, force, force)
apply (rule arg_cong2[of _ _ _ _ ""])
apply force
apply (rule eq_matI, (auto)[3], goal_cases)
proof -
case (1 i j)
from IM_props(1)[OF 1]
show ?case unfolding Ints_def using the_inv_f_f[OF oi] by auto
qed auto
have "map_mat ?oi (inv_mu_ij_mat i j c) * M m = (?C * ?D) * M m + M m" unfolding mat_oi
by (subst add_mult_distrib_mat[of _ m m], auto)
also have "(?C * ?D) * M m = ?C * (?D * M m)"
by (rule assoc_mult_mat, auto)
also have "?D = mat m m (λ (i,j). if i = j then d j else 0) * IM" (is "_ = ?E * _")
proof (rule eq_matI, insert IM_props(4), auto simp: scalar_prod_def, goal_cases)
case (1 i j)
hence id: "{0..<m} = {0..<i}  {i}  {Suc i ..<m}"
show ?case unfolding id
by (auto simp: sum.union_disjoint)
qed
also have " * M m = ?E * (IM * M m)"
by (rule assoc_mult_mat[of _ m m], insert IM_props, auto)
also have "IM * M m = 1m m" by fact
also have "?E * 1m m = ?E" by simp
also have "?C * ?E = mat m m (λ ij. if ij = (i,j) then ?oi c * d j else 0)"
by (rule eq_matI, auto simp: scalar_prod_def, auto simp: jm sum.union_disjoint)
finally show "map_mat ?oi (inv_mu_ij_mat i j c) * M m =
mat m m (λ ij. if ij = (i,j) then ?oi c * d j else 0) + M m" .
show carr: "inv_mu_ij_mat i j c  carrier_mat m m"
unfolding inv_mu_ij_mat_def by auto
{
assume k: "k < m"
have "of_int (inv_mu_ij_mat i j c $$(k,k)) = ?MM$$ (k,k)"
using carr k by auto
also have " = (?C * ?D) $$(k,k) + 1" unfolding mat_oi using k by simp also have "(?C * ?D)$$ (k,k) = 0" using k
by (auto simp: scalar_prod_def, auto simp: jm sum.union_disjoint
inv_mu_lower_triangular[OF IM ji i])
finally show "inv_mu_ij_mat i j c $$(k,k) = 1" by simp } { assume ij': "i' < j'" "j' < m" have "of_int (inv_mu_ij_mat i j c$$ (i',j')) = ?MM $$(i',j')" using carr ij' by auto also have " = (?C * ?D)$$ (i',j')" unfolding mat_oi using ij' by simp
also have "(?C * ?D) $$(i',j') = (if i' = i then ?oi c * (d j * IM$$ (j, j')) else 0)"
using ij' i j by (auto simp: scalar_prod_def, auto simp: jm sum.union_disjoint)
also have " = 0" using inv_mu_lower_triangular[OF IM _ ij'(2), of j] ij' i ji by auto
finally show "inv_mu_ij_mat i j c $$(i',j') = 0" by simp } { assume A: "A carrier_mat m n" and c: "c mod p = 0" let ?mod = "map_mat (λ x. x mod p)" let ?C = "mat m m (λ ij. if ij = (i,j) then c else 0)" let ?D = "mat m m (λ ij. if ij = (i,j) then 1 else (0 :: int))" define B where "B = mat m m (λ (i,j). the_inv ?oi (d i * the (mat_inverse (M m))$$ (i,j)))"
have B: "B  carrier_mat m m" unfolding B_def by auto
define BA where "BA = B * A"
have BA: "BA  carrier_mat m n" unfolding BA_def using A B by auto
define DBA where "DBA = ?D * BA"
have DBA: "DBA  carrier_mat m n" unfolding DBA_def using BA by auto
have "?mod (inv_mu_ij_mat i j c * A) =
?mod ((?C * B + 1m m) * A)"
unfolding inv_mu_ij_mat_def B_def by simp
also have "(?C * B + 1m m) * A = ?C * B * A + A"
by (subst add_mult_distrib_mat, insert A B, auto)
also have "?C * B * A = ?C * BA"
unfolding BA_def
by (rule assoc_mult_mat, insert A B, auto)
also have "?C = c m ?D"
by (rule eq_matI, auto)
also have " * BA = c m DBA" using BA unfolding DBA_def by auto
also have "?mod ( + A) = ?mod A"
by (rule eq_matI, insert DBA A c, auto simp: mult.assoc)
finally show "?mod (inv_mu_ij_mat i j c * A) = ?mod A" .
}
qed
end

lemma Gramian_determinant_of_int: assumes fs: "set fs  carrier_vec n"
and j: "j  length fs"
shows
proof -
from j have j: "k < j  k < length fs" for k by auto
show ?thesis
unfolding gram_schmidt.Gramian_determinant_def
by (subst of_int_hom.hom_det[symmetric], rule arg_cong[of _ _ ],
unfold gram_schmidt.Gramian_matrix_def Let_def, subst of_int_hom.mat_hom_mult, force, force,
unfold map_mat_transpose[symmetric],
rule arg_cong2[of _ _ _ _ "λ x y. x  y"], insert fs[unfolded set_conv_nth]
j, (fastforce intro!: eq_matI)+)
qed

context LLL
begin

(* this lemma might also be useful for swap/add-operation *)
lemma multiply_invertible_mat: assumes lin: "lin_indep fs"
and len: "length fs = m"
and A: "A  carrier_mat m m"
and A_invertible: " B. B  carrier_mat m m  B * A = 1m m"
and fs'_prod: "fs' = Matrix.rows (A * mat_of_rows n fs)"
shows "lattice_of fs' = lattice_of fs"
"lin_indep fs'"
"length fs' = m"
proof -
let ?Mfs = "mat_of_rows n fs"
let ?Mfs' = "mat_of_rows n fs'"
from A_invertible obtain B where B: "B  carrier_mat m m" and inv: "B * A = 1m m" by auto
from lin have fs: "set fs  carrier_vec n" unfolding gs.lin_indpt_list_def by auto
with len have Mfs: "?Mfs  carrier_mat m n" by auto
from A Mfs have prod: "A * ?Mfs  carrier_mat m n" by auto
hence fs': "length fs' = m" "set fs'  carrier_vec n" unfolding fs'_prod
by (auto simp: Matrix.rows_def Matrix.row_def)
have Mfs_prod': "?Mfs' = A * ?Mfs"
unfolding arg_cong[OF fs'_prod, of "mat_of_rows n"]
by (intro eq_matI, auto simp: mat_of_rows_def)
have "B * ?Mfs' = B * (A * ?Mfs)"
unfolding Mfs_prod' by simp
also have " = (B * A) * ?Mfs"
by (subst assoc_mult_mat[OF _ A Mfs], insert B, auto)
also have "B * A = 1m m" by fact
also have " * ?Mfs = ?Mfs" using Mfs by auto
finally have Mfs_prod: "?Mfs = B * ?Mfs'" ..
interpret LLL: LLL_with_assms n m fs 2
by (unfold_locales, auto simp: len lin)
from LLL.LLL_change_basis[OF fs'(2,1) B A Mfs_prod Mfs_prod']
show latt': "lattice_of fs' = lattice_of fs" and lin': "gs.lin_indpt_list (RAT fs')"
and len': "length fs' = m"
qed

text ‹This is the key lemma.›
lemma change_single_element: assumes lin: "lin_indep fs"
and len: "length fs = m"
and i: "i < m" and ji: "j < i"
and A:     ― ‹the transformation matrix A›
and fs'_prod: "fs' = Matrix.rows (A i j c * mat_of_rows n fs)" ― ‹fs' is the new basis›
and latt: "lattice_of fs = L"
shows "lattice_of fs' = L"
"c mod p = 0  map (map_vec (λ x. x mod p)) fs' = map (map_vec (λ x. x mod p)) fs"
"lin_indep fs'"
"length fs' = m"
" k. k < m  gso fs' k = gso fs k"
" k. k  m  d fs' k = d fs k"
"i' < m  j' < m
μ fs' i' j' = (if (i',j') = (i,j) then rat_of_int (c * d fs j) + μ fs i' j' else μ fs i' j')"
"i' < m  j' < m
fs' i' j' = (if (i',j') = (i,j) then c * d fs j * d fs (Suc j) +  fs i' j' else  fs i' j')"
proof -
let ?A = "A i j c"
let ?Mfs = "mat_of_rows n fs"
let ?Mfs' = "mat_of_rows n fs'"
from lin have fs: "set fs  carrier_vec n" unfolding gs.lin_indpt_list_def by auto
with len have Mfs: "?Mfs  carrier_mat m n" by auto
interpret gsi: gram_schmidt_fs_int n "RAT fs"
rewrites  using lin unfolding A
by (unfold_locales, insert lin[unfolded gs.lin_indpt_list_def], auto simp: set_conv_nth)
note A = gsi.inv_mu_ij_mat[unfolded length_map len, OF i ji, where c = c]
from A(3) Mfs have prod: "?A * ?Mfs  carrier_mat m n" by auto
hence fs': "length fs' = m" "set fs'  carrier_vec n" unfolding fs'_prod
by (auto simp: Matrix.rows_def Matrix.row_def)
have Mfs_prod': "?Mfs' = ?A * ?Mfs"
unfolding arg_cong[OF fs'_prod, of "mat_of_rows n"]
by (intro eq_matI, auto simp: mat_of_rows_def)
have detA: "det ?A = 1"
by (subst det_lower_triangular[OF A(4) A(3)], insert A, auto intro!: prod_list_neutral
simp: diag_mat_def)
have " B. B  carrier_mat m m  B * ?A = 1m m"
by (intro exI[of _ "adj_mat ?A"], insert adj_mat[OF A(3)], auto simp: detA)
from multiply_invertible_mat[OF lin len A(3) this fs'_prod] latt
show latt': "lattice_of fs' = L" and lin': "gs.lin_indpt_list (RAT fs')"
and len': "length fs' = m" by auto
interpret LLL: LLL_with_assms n m fs 2
by (unfold_locales, auto simp: len lin)
interpret fs: fs_int_indpt n fs
by (standard, auto simp: lin)
interpret fs': fs_int_indpt n fs'
by (standard, auto simp: lin')
{
assume c: "c mod p = 0"
have id: "rows (map_mat f A) = map (map_vec f) (rows A)" for f A
unfolding rows_def by auto
have rows_id: "set fs  carrier_vec n  rows (mat_of_rows n fs) = fs" for fs
unfolding mat_of_rows_def rows_def
by (force simp: Matrix.row_def set_conv_nth intro!: nth_equalityI)
from A(2)[OF Mfs c]
have "rows (map_mat (λx. x mod p) ?Mfs') = rows (map_mat (λx. x mod p) ?Mfs)" unfolding Mfs_prod'
by simp
from this[unfolded id rows_id[OF fs] rows_id[OF fs'(2)]]
show "map (map_vec (λ x. x mod p)) fs' = map (map_vec (λ x. x mod p)) fs" .
}
{
define B where "B = ?A"
have gs_eq: "k < m  gso fs' k = gso fs k" for k
proof(induct rule: nat_less_induct)
case (1 k)
then show ?case
proof(cases "k = 0")
case True
then show ?thesis
proof -
have "row ?Mfs' 0 = row ?Mfs 0"
proof -
have 2: "0 {0..<m}" and 3: "{1..<m} = {0..<m} - {0}"
and 4: "finite {0..<m}" using 1 by auto
have "row ?Mfs' 0 = vec n (λj. row B 0  col ?Mfs j)"
using row_mult A(3) Mfs 1 Mfs_prod' unfolding B_def by simp
also have " = vec n (λj. (l{0..<m}. B $$(0, l) * ?Mfs$$ (l, j)))"
using Mfs A(3) len 1 B_def unfolding scalar_prod_def by auto
also have " = vec n (λj. B $$(0, 0) * ?Mfs$$ (0, j) +
(l{1..<m}. B $$(0, l) * ?Mfs$$ (l, j)))"
by (simp add: g. sum g {0..<m} = g 0 + sum g ({0..<m} - {0}))
also have " = row ?Mfs 0"
using A(4-) 1 unfolding B_def[symmetric] by (simp add: row_def)
finally show ?thesis by (simp add: B_def Mfs_prod')
qed
then show ?thesis using True 1 fs'.f_carrier fs.f_carrier
fs'.gs.fs0_gso0 len' len gsi.fs0_gso0 by auto
qed
next
case False
then show ?thesis
proof -
have gso0kcarr:
using 1(2) gsi.gso_carrier len by auto
hence gsospancarr: "gs.span(gsi.gso  {0 ..<k})  carrier_vec n "
using span_is_subset2 by auto

have fs'_gs_diff_span:
"(RAT fs') !  k - fs'.gs.gso k  gs.span (gsi.gso  {0 ..<k})"
proof -
define gs'sum where "gs'sum =
gs.M.sumlist (map (λja. fs'.gs.μ k ja v fs'.gs.gso ja) [0..<k])"
define gssum where "gssum =
gs.M.sumlist (map (λja. fs'.gs.μ k ja v gsi.gso ja) [0..<k])"
have "set (map (λja. fs'.gs.μ k ja v gsi.gso ja) [0..<k])
gs.span(gsi.gso  {0 ..<k})" using 1(2) gs.span_mem gso0kcarr
by auto
hence gssumspan: "gssum  gs.span(gsi.gso  {0 ..<k})"
using atLeastLessThan_iff gso0kcarr imageE set_map set_upt
vec_space.sumlist_in_span
unfolding gssum_def by (smt subsetD)
hence gssumcarr: "gssum  carrier_vec n"
using gsospancarr gssum_def by blast
have sumid: "gs'sum = gssum"
proof -
have "map (λja. fs'.gs.μ k ja v fs'.gs.gso ja) [0..<k] =
map (λja. fs'.gs.μ k ja v gsi.gso ja) [0..<k]"
using 1 by simp
thus ?thesis unfolding gs'sum_def gssum_def by argo
qed
have "(RAT fs') !  k = fs'.gs.gso k + gssum"
using fs'.gs.fs_by_gso_def len' False 1 sumid
unfolding gs'sum_def by auto
hence "(RAT fs') !  k - fs'.gs.gso k = gssum"
using gssumcarr 1(2) len' by auto
thus ?thesis using gssumspan by simp
qed

define v2 where "v2 = sumlist (map (λja. B $$(k, ja) v fs ! ja) [0..< k])" have v2carr: "v2 carrier_vec n" proof - have "set (map (λja. B$$ (k, ja) v fs ! ja) [0..< k])  carrier_vec n"
using len 1(2) fs.f_carrier by auto
thus ?thesis unfolding v2_def by simp
qed
define ratv2 where "ratv2 = (map_vec rat_of_int v2)"
have ratv2carr: "ratv2  carrier_vec n"
unfolding ratv2_def using v2carr by simp
have fs'id: "(RAT fs') ! k = (RAT fs) ! k + ratv2"
proof -
have zkm: "[0..<m] = [0..<(Suc k)] @ [(Suc k)..<m]" using 1(2)
by (metis Suc_lessI append_Nil2 upt_append upt_rec zero_less_Suc)
have prep: "set (map (λja. B $$(k, ja) v fs ! ja) [0..<m]) carrier_vec n" using len fs.f_carrier by auto have "fs' ! k = vec n (λj. row B k col ?Mfs j)" using 1(2) Mfs B_def A(3) fs'_prod by simp also have " = sumlist (map (λja. B$$ (k, ja) v fs ! ja) [0..<m])"
proof -
{
fix i
assume i: "i < n"
have "(vec n (λj. row B k  col ?Mfs j)) $i = row B k col ?Mfs i" using i by auto also have " = (j = 0..<m. B $$(k, j) * ?Mfs$$ (j,i))" using A(3) unfolding B_def[symmetric] by (smt 1(2) Mfs R.finsum_cong' i atLeastLessThan_iff carrier_matD dim_col index_col index_row(1) scalar_prod_def) also have " = (j = 0..<m. B $$(k, j) * (fs ! j i))" by (metis (no_types, lifting) R.finsum_cong' atLeastLessThan_iff i len mat_of_rows_index) also have " = (j = 0..<m. (map (λja. B$$ (k, ja) v fs ! ja) [0..<m]) ! j$ i)"
proof -
have "j<m. i<n. B $$(k, j) * (fs ! j  i) = (map (λja. B$$ (k, ja) v fs ! ja) [0..<m]) ! j $i" using 1(2) i A(3) len fs.f_carrier unfolding B_def[symmetric] by auto then show ?thesis using i by auto qed also have " = sumlist (map (λja. B $$(k, ja) v fs ! ja) [0..<m]) i" using sumlist_nth i fs.f_carrier carrier_vecD len by simp finally have "(vec n (λj. row B k col ?Mfs j)) i = sumlist (map (λja. B$$ (k, ja) v fs ! ja) [0..<m])$ i" by auto
}
then show ?thesis using fs.f_carrier len dim_sumlist by auto
qed
also have " = sumlist (map (λja. B $$(k, ja) v fs ! ja) ([0..<(Suc k)] @ [(Suc k)..<m]))" using zkm by simp also have " = sumlist (map (λja. B$$ (k, ja) v fs ! ja) [0..<(Suc k)]) +
sumlist (map (λja. B $$(k, ja) v fs ! ja) [(Suc k)..<m])" (is " = ?L2 + ?L3") using fs.f_carrier len dim_sumlist sumlist_append prep zkm by auto also have "?L3 = 0v n" using A(4) fs.f_carrier len sumlist_nth carrier_vecD sumlist_carrier prep zkm unfolding B_def[symmetric] by auto also have "?L2 = sumlist (map (λja. B$$ (k, ja) v fs ! ja) [0..<k]) +
B $$(k, k) v fs ! k" using prep zkm sumlist_snoc by simp also have " = sumlist (map (λja. B$$ (k, ja) v fs ! ja) [0..<k]) + fs ! k"
using A(5) 1(2) unfolding B_def[symmetric] by simp
finally have "fs' ! k = fs ! k +
sumlist (map (λja. B $$(k, ja) v fs ! ja) [0..<k])" using prep zkm by (simp add: M.add.m_comm) then have "fs' ! k = fs ! k + v2" unfolding v2_def by simp then show ?thesis using v2carr 1(2) len len' ratv2_def by force qed have ratv2span: "ratv2 gs.span (gsi.gso  {0 ..<k})" proof - have rat: "ratv2 = gs.M.sumlist (map (λj. of_int (B$$ (k, j)) v (RAT fs) ! j) [0..<k])"
proof -
have "set (map (λj. of_int (B $$(k, j)) v (RAT fs) ! j) [0..<k]) carrier_vec n" using fs.f_carrier 1(2) len by auto hence carr: "gs.M.sumlist (map (λj. of_int (B$$ (k, j)) v (RAT fs) ! j) [0..<k])  carrier_vec n"
by auto
have "set (map (λj. B $$(k, j) v fs ! j) [0..<k]) carrier_vec n" using fs.f_carrier 1(2) len by auto hence "i j. i < n j < k of_int ((B$$ (k, j) v fs ! j) $i) = (of_int (B $$(k, j)) v (RAT fs) ! j) i" using 1(2) len by fastforce hence "i. i < n ratv2 i = gs.M.sumlist (map (λj. (of_int (B$$ (k, j)) v (RAT fs) ! j)) [0..<k])$ i"
using fs.f_carrier 1(2) len v2carr gs.sumlist_nth sumlist_nth
ratv2_def v2_def by simp
then show ?thesis using ratv2carr carr by auto
qed
have "i. i < k  (RAT fs) ! i =
gs.M.sumlist (map (λ j. gsi.μ i j v gsi.gso j) [0 ..< Suc i])"
using gsi.fi_is_sum_of_mu_gso len 1(2) by auto
moreover have "i. i < k  (λ j. gsi.μ i j v gsi.gso j)  {0 ..< Suc i}
gs.span (gsi.gso  {0 ..<k})"
using gs.span_mem gso0kcarr by auto
ultimately have "i. i < k  (RAT fs) ! i  gs.span (gsi.gso  {0 ..<k})"
using gso0kcarr set_map set_upt vec_space.sumlist_in_span subsetD by smt
then show ?thesis using rat atLeastLessThan_iff set_upt gso0kcarr imageE
set_map gs.smult_in_span vec_space.sumlist_in_span by smt
qed
have fs_gs_diff_span:
"(RAT fs) !  k - fs'.gs.gso k  gs.span (gsi.gso  {0 ..<k})"
proof -
from fs'_gs_diff_span obtain v3 where sp: "v3  gs.span (gsi.gso  {0 ..<k})"
and eq: "(RAT fs) ! k - fs'.gs.gso k = v3 - ratv2"
using fs'.gs.gso_carrier len' 1(2) ratv2carr fs'id by fastforce
have "v3+(-ratv2)  gs.span(gsi.gso  {0 ..<k})"
by (metis sp gs.span_add1 gso0kcarr gram_schmidt.inv_in_span
gso0kcarr ratv2span)
moreover have "v3+(-ratv2) = v3-ratv2" using ratv2carr by auto
ultimately have "v3 - ratv2  gs.span (gsi.gso  {0 ..<k})" by simp
then show ?thesis using eq by auto
qed
{
fix i
assume i: "i < k"
hence  using 1(2) fs'.gs.orthogonal len' by auto
hence  using 1 i by simp
}
hence "x. x  gsi.gso ` {0..<k}  fs'.gs.gso k  x = 0" by auto

then show ?thesis
using gsi.oc_projection_unique len len' fs_gs_diff_span 1(2) by auto
qed
qed
qed

have " i' j'. i' < m  j' < m  μ fs' i' j' =
(map_mat of_int (A i j c) * gsi.M m) $$(i',j')" and " k. k < m gso fs' k = gso fs k" proof - define rB where "rB = map_mat rat_of_int B" have rBcarr: "rB carrier_mat m m" using A(3) unfolding rB_def B_def by simp define rfs where "rfs = mat_of_rows n (RAT fs)" have rfscarr: "rfs carrier_mat m n" using Mfs unfolding rfs_def by simp { fix i' fix j' assume i': "i' < m" assume j': "j' < m" have prep: "of_int_hom.vec_hom (row (B * mat_of_rows n fs) i') = row (rB * rfs) i'" using len i' B_def A(3) rB_def rfs_def by (auto simp: scalar_prod_def) have prep2: "row (rB * rfs) i' = vec n (λl. row rB i' col rfs l)" using len fs.f_carrier i' B_def A(3) scalar_prod_def rB_def unfolding rfs_def by auto have prep3: "(vec m (λ j1. row rfs j1 gsi.gso j' / gsi.gso j'2)) = (vec m (λ j1. (gsi.M m)$$ (j1, j')))"
proof -
{
fix x y
assume x: "x < m" and y: "y < m"
have "(gsi.M m) $$(x,y) = (if y < x then map of_int_hom.vec_hom fs ! x fs'.gs.gso y / fs'.gs.gso y2 else if x = y then 1 else 0)" using gsi.μ.simps x y j' len gs_eq gsi.M_index by auto hence "row rfs x gsi.gso y / gsi.gso y2 = (gsi.M m)$$ (x,y)"
unfolding rfs_def
by (metis carrier_matD(1) divide_eq_eq fs'.gs.β_zero fs'.gs.gso_norm_beta
gs_eq gsi.μ.simps gsi.fi_scalar_prod_gso gsi.fs_carrier len len'
length_map nth_rows rfs_def rfscarr rows_mat_of_rows x y)
}
then show ?thesis using j' by auto
qed
have prep4: "(1 / gsi.gso j'2) v (vec m (λj1. row rfs j1  gsi.gso j')) =
(vec m (λj1. row rfs j1  gsi.gso j' / gsi.gso j'2))" by auto

have
using gs_eq j' by simp
also have " = row (rB * rfs) i'  gsi.gso j' / gsi.gso j'2"
using prep i' len' unfolding rB_def B_def by (simp add: fs'_prod)
also have " =
(vec n (λl. row rB i'  col rfs l))  gsi.gso j' / gsi.gso j'2"
using prep2 by auto
also have "vec n (λl. row rB i'  col rfs l) =
(vec n (λl. (j1=0..<m. (row rB i') $j1 * (col rfs l)$ j1)))"
using gsi.gso_carrier
by (metis (no_types) carrier_matD(1) col_def dim_vec rfscarr scalar_prod_def)
also have " =
(vec n (λl. (j1=0..<m. rB $$(i', j1) * rfs$$ (j1, l))))"
using rBcarr rfscarr i' by auto
also have "  gsi.gso j' =
(j2=0..<n. (vec n
(λl. (j1=0..<m. rB $$(i', j1) * rfs$$ (j1, l)))) $j2 * (gsi.gso j')$ j2)"
using gsi.gso_carrier len j' scalar_prod_def
by (smt gs.R.finsum_cong' gsi.gso_dim length_map)
also have " = (j2=0..<n.
(j1=0..<m. rB $$(i', j1) * rfs$$ (j1, j2)) * (gsi.gso j') $j2)" using gsi.gso_carrier len j' by simp also have " = (j2=0..<n. (j1=0..<m. rB $$(i', j1) * rfs$$ (j1, j2) * (gsi.gso j')$ j2))"
by (smt gs.R.finsum_cong' sum_distrib_right)
also have " = (j1=0..<m. (j2=0..<n.
rB $$(i', j1) * rfs$$ (j1, j2) * (gsi.gso j') $j2))" using sum.swap by auto also have " = (j1=0..<m. rB $$(i', j1) * (j2=0..<n. rfs$$ (j1, j2) * (gsi.gso j')$ j2))"
using gs.R.finsum_cong' sum_distrib_left by (smt gs.m_assoc)
also have " = row rB i'  (vec m (λ j1. (j2=0..<n.
rfs $$(j1, j2) * (gsi.gso j')  j2)))" using rBcarr rfscarr i' scalar_prod_def by (smt atLeastLessThan_iff carrier_matD(1) carrier_matD(2) dim_vec gs.R.finsum_cong' index_row(1) index_vec) also have "(vec m (λ j1. (j2=0..<n. rfs$$ (j1, j2) * (gsi.gso j') $j2))) = (vec m (λ j1. row rfs j1 gsi.gso j'))" using rfscarr gsi.gso_carrier len j' rfscarr by (auto simp add: scalar_prod_def) also have "row rB i' / gsi.gso j'2 = row rB i' vec m (λ j1. row rfs j1 gsi.gso j' / gsi.gso j'2)" using prep4 scalar_prod_smult_right rBcarr carrier_matD(2) dim_vec row_def by (smt gs.l_one times_divide_eq_left) also have " = (rB * (gsi.M m)) $$(i', j')" using rBcarr i' j' prep3 gsi.M_def by (simp add: col_def) finally have "map of_int_hom.vec_hom fs' ! i' fs'.gs.gso j' / fs'.gs.gso j'2 = (rB * (gsi.M m))$$ (i', j')" by auto } then show " i' j'. i' < m j' < m μ fs' i' j' = (map_mat of_int (A i j c) * gsi.M m) $$(i',j')" using B_def fs'.gs.β_zero fs'.gs.fi_scalar_prod_gso fs'.gs.gso_norm_beta len' rB_def by auto show " k. k < m gso fs' k = gso fs k" using gs_eq by auto qed } note mu_gso = this show " k. k < m gso fs' k = gso fs k" by fact { fix k have "k m rat_of_int (d fs' k) = rat_of_int (d fs k)" for k proof (induct k) case 0 show ?case by (simp add: d_def) next case (Suc k) hence k: "k m" "k < m" by auto show ?case by (subst (1 2) LLL_d_Suc[OF _ k(2)], auto simp: Suc(1)[OF k(1)] mu_gso(2)[OF k(2)] LLL_invariant_weak_def lin lin' len len' latt latt') qed thus "k m d fs' k = d fs k" by simp } note d = this { assume i': "i' < m" and j': "j' < m" have "μ fs' i' j' = (of_int_hom.mat_hom (A i j c) * gsi.M m)$$ (i',j')" by (rule mu_gso(1)[OF i' j']) also have " = (if (i',j') = (i,j) then of_int c * gsi.d j else 0) + gsi.M m $$(i',j')" unfolding A(1) using i' j' by (auto simp: gsi.M_def) also have "gsi.M m$$ (i',j') = μ fs i' j'" unfolding gsi.M_def using i' j' by simp also have "gsi.d j = of_int (d fs j)" unfolding d_def by (subst Gramian_determinant_of_int[OF fs], insert ji i len, auto) finally show mu: "μ fs' i' j' = (if (i',j') = (i,j) then rat_of_int (c * d fs j) + μ fs i' j' else μ fs i' j')" by simp let ?d = "d fs (Suc j')" have d_fs: "of_int ( fs i' j') = rat_of_int ?d * μ fs i' j'" unfolding dμ_def using fs.fs_int_mu_d_Z_m_m[unfolded len, OF i' j'] by (metis LLL.LLL.d_def assms(2) fs.fs_int_mu_d_Z_m_m fs_int.d_def i' int_of_rat(2) j') have "rat_of_int ( fs' i' j') = rat_of_int (d fs' (Suc j')) * μ fs' i' j'" unfolding dμ_def using fs'.fs_int_mu_d_Z_m_m[unfolded len', OF i' j'] using LLL.LLL.d_def fs'(1) fs'.dμ fs'.dμ_def fs_int.d_def i' j' by auto also have "d fs' (Suc j') = ?d" by (rule d, insert j', auto) also have "rat_of_int * μ fs' i' j' = (if (i',j') = (i,j) then rat_of_int (c * d fs j * ?d) else 0) + of_int ( fs i' j')" unfolding mu d_fs by (simp add: field_simps) also have " = rat_of_int ((if (i',j') = (i,j) then c * d fs j * ?d else 0) + fs i' j')" by simp also have " = rat_of_int ((if (i',j') = (i,j) then c * d fs j * d fs (Suc j) + fs i' j' else fs i' j'))" by simp finally show " fs' i' j' = (if (i',j') = (i,j) then c * d fs j * d fs (Suc j) + fs i' j' else fs i' j')" by simp } qed text ‹Eventually: Lemma 13 of Storjohann's paper.› lemma mod_single_element: assumes lin: "lin_indep fs" and len: "length fs = m" and i: "i < m" and ji: "j < i" and latt: "lattice_of fs = L" and pgtz: "p > 0" shows " fs'. lattice_of fs' = L map (map_vec (λ x. x mod p)) fs' = map (map_vec (λ x. x mod p)) fs map (map_vec (λ x. x symmod p)) fs' = map (map_vec (λ x. x symmod p)) fs lin_indep fs' length fs' = m ( k < m. gso fs' k = gso fs k) ( k m. d fs' k = d fs k) ( i' < m. j' < m. fs' i' j' = (if (i',j') = (i,j) then fs i j' symmod (p * d fs j' * d fs (Suc j')) else fs i' j'))" proof - have inv: "LLL_invariant_weak fs" using LLL_invariant_weak_def assms by simp let ?mult = "d fs j * d fs (Suc j)" define M where "M = ?mult" define pM where "pM = p * M" then have pMgtz: "pM > 0" using pgtz unfolding pM_def M_def using LLL_d_pos[OF inv] i ji by simp let ?d = " fs i j" define c where "c = - (?d symdiv pM)" have d_mod: "?d symmod pM = c * pM + ?d" unfolding c_def using pMgtz sym_mod_sym_div by simp define A where define fs' where fs': "fs' = Matrix.rows (A i j (c * p) * mat_of_rows n fs)" note main = change_single_element[OF lin len i ji A_def fs' latt] have "map (map_vec (λx. x mod p)) fs' = map (map_vec (λx. x mod p)) fs" by (intro main, auto) from arg_cong[OF this, of "map (map_vec (poly_mod.inv_M p))"] have id: "map (map_vec (λx. x symmod p)) fs' = map (map_vec (λx. x symmod p)) fs" unfolding map_map o_def sym_mod_def map_vec_map_vec . show ?thesis proof (intro exI[of _ fs'] conjI main allI impI id) fix i' j' assume ij: "i' < m" "j' < m" have " fs' i' j' = (if (i', j') = (i, j) then (c * p) * M + ?d else fs i' j')" unfolding main(8)[OF ij] M_def by simp also have "(c * p) * M + ?d = ?d symmod pM" unfolding d_mod by (simp add: pM_def) finally show " fs' i' j' = (if (i',j') = (i,j) then fs i j' symmod (p * d fs j' * d fs (Suc j')) else fs i' j')" by (auto simp: pM_def M_def ac_simps) qed auto qed text ‹A slight generalization to perform modulo on arbitrary set of indices$I\$.›
lemma mod_finite_set: assumes lin: "lin_indep fs"
and len: "length fs = m"
and I: "I  {(i,j). i < m  j < i}"
and latt: "lattice_of fs = L"
and pgtz: "p > 0"
shows " fs'. lattice_of fs' = L
map (map_vec (λ x. x mod p)) fs' = map (map_vec (λ x. x mod p)) fs
map (map_vec (λ x. x symmod p)) fs' = map (map_vec (λ x. x symmod p)) fs
lin_indep fs'
length fs' = m
( k < m. gso fs' k = gso fs k)
( k  m. d fs' k = d fs k)
( i' < m.  j' < m.  fs' i' j' =
(if (i',j')  I then  fs i' j' symmod (p * d fs j' * d fs (Suc j')) else  fs i' j'))"
proof -
let ?exp = "λ fs' I i' j'.
fs' i' j' = (if (i',j')  I then  fs i' j' symmod (p * d fs j' * d fs (Suc j')) else  fs i' j')"
let ?prop = "λ fs fs'. lattice_of fs' = L
map (map_vec (λ x. x mod p)) fs' = map (map_vec (λ x. x mod p)) fs
map (map_vec (λ x. x symmod p)) fs' = map (map_vec (λ x. x symmod p)) fs
lin_indep fs'
length fs' = m
( k < m. gso fs' k = gso fs k)
( k  m. d fs' k = d fs k)"
have "finite I"
proof (rule finite_subset[OF I], rule finite_subset)
show "{(i, j). i < m  j < i}  {0..m} × {0..m}" by auto
qed auto
from this I have " fs'. ?prop fs fs'  ( i' < m.  j' < m. ?exp fs' I i' j')"
proof (induct I)
case empty
show ?case
by (intro exI[of _ fs], insert assms, auto)
next
case (insert ij I)
obtain i j where ij: "ij = (i,j)" by force
from ij insert(4) have i: "i < m" "j < i" by auto
from insert(3,4) obtain gs where gs: "?prop fs gs"
and exp: " i' j'. i' < m  j' < m  ?exp gs I i' j'" by auto
from gs have "lin_indep gs" "lattice_of gs = L" "length gs = m" by auto
from mod_single_element[OF this(1,3) i this(2), of p]
obtain hs where hs: "?prop gs hs"
and exp': " i' j'. i' < m  j' < m
hs i' j' = (if (i', j') = (i, j)
then  gs i j' symmod (p * d gs j' * d gs (Suc j')) else  gs i' j')"
using pgtz by auto
from gs i have id: "d gs j = d fs j" "d gs (Suc j) = d fs (Suc j)" by auto
show ?case
proof (intro exI[of _ hs], rule conjI; (intro allI impI)?)
show "?prop fs hs" using gs hs by auto
fix i' j'
assume *: "i' < m" "j' < m"
show "?exp hs (insert ij I) i' j'" unfolding exp'[OF *] ij using exp * i
by (auto simp: id)
qed
qed
thus ?thesis by auto
qed

end

end