# Theory HNF_Mod_Det_Soundness

```
subsection ‹Soundness of the algorithm›

theory HNF_Mod_Det_Soundness
imports
HNF_Mod_Det_Algorithm
Signed_Modulo
begin

hide_const(open) Determinants.det Determinants2.upper_triangular
Finite_Cartesian_Product.row Finite_Cartesian_Product.rows
Finite_Cartesian_Product.vec

subsubsection ‹Results connecting lattices and Hermite normal form›

text ‹The following results will also be useful for proving the soundness of the certification
approach.›

lemma of_int_mat_hom_int_id[simp]:
fixes A::"int mat"
shows "of_int_hom.mat_hom A = A" unfolding map_mat_def by auto

definition "is_sound_HNF algorithm associates res
= (∀A. let (P,H) = algorithm A; m = dim_row A; n = dim_col A in
P ∈ carrier_mat m m ∧ H ∈ carrier_mat m n ∧ invertible_mat P ∧ A = P * H
∧ Hermite_JNF associates res H)"

lemma HNF_A_eq_HNF_PA:
fixes A::"'a::{bezout_ring_div,normalization_euclidean_semiring,unique_euclidean_ring} mat"
assumes A: "A ∈ carrier_mat n n" and inv_A: "invertible_mat A"
and inv_P: "invertible_mat P" and P: "P ∈ carrier_mat n n"
and sound_HNF: "is_sound_HNF HNF associates res"
and P1_H1: "(P1,H1) = HNF (P*A)"
and P2_H2: "(P2,H2) = HNF A"
shows "H1 = H2"
proof -
obtain inv_P where P_inv_P: "inverts_mat P inv_P" and inv_P_P: "inverts_mat inv_P P"
and inv_P: "inv_P ∈ carrier_mat n n"
using P inv_P obtain_inverse_matrix by blast
have P1: "P1 ∈ carrier_mat n n"
using P1_H1 sound_HNF unfolding is_sound_HNF_def Let_def
by (metis (no_types, lifting) P carrier_matD(1) index_mult_mat(2) old.prod.case)
have H1: "H1 ∈ carrier_mat n n" using P1_H1 sound_HNF unfolding is_sound_HNF_def Let_def
by (metis (no_types, lifting) A P carrier_matD(1) carrier_matD(2) case_prodD index_mult_mat(2,3))
have invertible_inv_P: "invertible_mat inv_P"
using P_inv_P inv_P inv_P_P invertible_mat_def square_mat.simps by blast
have P_A_P1_H1: "P * A = P1 * H1" using P1_H1 sound_HNF unfolding is_sound_HNF_def Let_def
by (metis (mono_tags, lifting) case_prod_conv)
hence "A = inv_P * (P1 * H1)"
by (smt A P inv_P_P inv_P assoc_mult_mat carrier_matD(1) inverts_mat_def left_mult_one_mat)
hence A_inv_P_P1_H1: "A = (inv_P * P1) * H1"
by (smt P P1_H1 assoc_mult_mat carrier_matD(1) fst_conv index_mult_mat(2) inv_P
is_sound_HNF_def prod.sel(2) sound_HNF split_beta)
have A_P2_H2: "A = P2 * H2" using P2_H2 sound_HNF unfolding is_sound_HNF_def Let_def
by (metis (mono_tags, lifting) case_prod_conv)
have invertible_inv_P_P1: "invertible_mat (inv_P * P1)"
proof (rule invertible_mult_JNF[OF inv_P P1 invertible_inv_P])
show "invertible_mat P1"
by (smt P1_H1 is_sound_HNF_def prod.sel(1) sound_HNF split_beta)
qed
show ?thesis
proof (rule Hermite_unique_JNF[OF A _ H1 _ _ A_inv_P_P1_H1 A_P2_H2 inv_A invertible_inv_P_P1])
show "inv_P * P1 ∈ carrier_mat n n"
by (metis carrier_matD(1) carrier_matI index_mult_mat(2) inv_P
invertible_inv_P_P1 invertible_mat_def square_mat.simps)
show "P2 ∈ carrier_mat n n"
by (smt A P2_H2 carrier_matD(1) is_sound_HNF_def prod.sel(1) sound_HNF split_beta)
show "H2 ∈ carrier_mat n n"
by (smt A P2_H2 carrier_matD(1) carrier_matD(2) is_sound_HNF_def prod.sel(2) sound_HNF split_beta)
show "invertible_mat P2"
by (smt P2_H2 is_sound_HNF_def prod.sel(1) sound_HNF split_beta)
show "Hermite_JNF associates res H1"
by (smt P1_H1 is_sound_HNF_def prod.sel(2) sound_HNF split_beta)
show "Hermite_JNF associates res H2"
by (smt P2_H2 is_sound_HNF_def prod.sel(2) sound_HNF split_beta)
qed
qed

context vec_module
begin

lemma mat_mult_invertible_lattice_eq:
assumes fs: "set fs ⊆ carrier_vec n"
and gs: "set gs ⊆ carrier_vec n"
and P: "P ∈ carrier_mat m m" and invertible_P: "invertible_mat P"
and length_fs: "length fs = m" and length_gs: "length gs = m"
and prod: "mat_of_rows n fs = (map_mat of_int P) * mat_of_rows n gs"
shows "lattice_of fs = lattice_of gs"
proof thm mat_mult_sub_lattice
show "lattice_of fs ⊆ lattice_of gs"
by (rule mat_mult_sub_lattice[OF fs gs _ prod],simp add: length_fs length_gs P)
next
obtain inv_P where P_inv_P: "inverts_mat P inv_P" and inv_P_P: "inverts_mat inv_P P"
and inv_P: "inv_P ∈ carrier_mat m m"
using P invertible_P obtain_inverse_matrix by blast
have "of_int_hom.mat_hom (inv_P) * mat_of_rows n fs
= of_int_hom.mat_hom (inv_P) * ((map_mat of_int P) * mat_of_rows n gs)"
using prod by auto
also have "... = of_int_hom.mat_hom (inv_P) * (map_mat of_int P) * mat_of_rows n gs"
by (smt P assoc_mult_mat inv_P length_gs map_carrier_mat mat_of_rows_carrier(1))
also have "... = of_int_hom.mat_hom (inv_P * P) * mat_of_rows n gs"
by (metis P inv_P of_int_hom.mat_hom_mult)
also have "... = mat_of_rows n gs"
by (metis carrier_matD(1) inv_P inv_P_P inverts_mat_def left_mult_one_mat'
length_gs mat_of_rows_carrier(2) of_int_hom.mat_hom_one)
finally have prod: "mat_of_rows n gs = of_int_hom.mat_hom (inv_P) * mat_of_rows n fs" ..
show "lattice_of gs ⊆ lattice_of fs"
by (rule mat_mult_sub_lattice[OF gs fs _ prod], simp add: length_fs length_gs inv_P)
qed

end

context
fixes n :: nat
begin

interpretation vec_module "TYPE(int)" .

lemma lattice_of_HNF:
assumes sound_HNF: "is_sound_HNF HNF associates res"
and P1_H1: "(P,H) = HNF (mat_of_rows n fs)"
and fs: "set fs ⊆ carrier_vec n" and len: "length fs = m"
shows "lattice_of fs = lattice_of (rows H)"
proof (rule mat_mult_invertible_lattice_eq[OF fs])
have H: "H ∈ carrier_mat m n" using sound_HNF P1_H1 unfolding is_sound_HNF_def Let_def
by (metis (mono_tags, lifting) assms(4) mat_of_rows_carrier(2) mat_of_rows_carrier(3) prod.sel(2) split_beta)
have H_rw: "mat_of_rows n (Matrix.rows H) = H" using mat_of_rows_rows H by fast
have PH_fs_init: "mat_of_rows n fs = P * H" using sound_HNF P1_H1 unfolding is_sound_HNF_def Let_def
by (metis (mono_tags, lifting) case_prodD)
show "mat_of_rows n fs = of_int_hom.mat_hom P * mat_of_rows n (Matrix.rows H)"
unfolding H_rw of_int_mat_hom_int_id using PH_fs_init by simp
show "set (Matrix.rows H) ⊆ carrier_vec n" using H rows_carrier by blast
show "P ∈ carrier_mat m m" using sound_HNF P1_H1 unfolding is_sound_HNF_def Let_def
by (metis (no_types, lifting) len case_prodD mat_of_rows_carrier(2))
show "invertible_mat P" using sound_HNF P1_H1 unfolding is_sound_HNF_def Let_def
by (metis (no_types, lifting) case_prodD)
show "length fs = m" using len by simp
show "length (Matrix.rows H) = m" using H by auto
qed
end

context LLL_with_assms
begin

(*For this proof, it seems that is not necessary fs_init to be a list of independent vectors.
The context assumes it, though.*)
lemma certification_via_eq_HNF:
assumes sound_HNF: "is_sound_HNF HNF associates res"
and P1_H1: "(P1,H1) = HNF (mat_of_rows n fs_init)"
and P2_H2: "(P2,H2) = HNF (mat_of_rows n gs)"
and H1_H2: "H1 = H2" (*The HNF are equal*)
and gs: "set gs ⊆ carrier_vec n" and len_gs: "length gs = m"
shows "lattice_of gs = lattice_of fs_init" "LLL_with_assms n m gs α"
proof -
have "lattice_of fs_init = lattice_of (rows H1)"
by (rule lattice_of_HNF[OF sound_HNF P1_H1 fs_init], simp add: len)
also have "... = lattice_of (rows H2)" using H1_H2 by auto
also have "... = lattice_of gs"
by (rule lattice_of_HNF[symmetric, OF sound_HNF P2_H2 gs len_gs])
finally show "lattice_of gs = lattice_of fs_init" ..
have invertible_P1: "invertible_mat P1"
using sound_HNF P1_H1 unfolding is_sound_HNF_def
by (metis (mono_tags, lifting) case_prodD)
have invertible_P2: "invertible_mat P2"
using sound_HNF P2_H2 unfolding is_sound_HNF_def
by (metis (mono_tags, lifting) case_prodD)
have P2: "P2 ∈ carrier_mat m m"
using sound_HNF P2_H2 unfolding is_sound_HNF_def
by (metis (no_types, lifting) len_gs case_prodD mat_of_rows_carrier(2))
obtain inv_P2 where P2_inv_P2: "inverts_mat P2 inv_P2" and inv_P2_P2: "inverts_mat inv_P2 P2"
and inv_P2: "inv_P2 ∈ carrier_mat m m"
using P2 invertible_P2 obtain_inverse_matrix by blast
have P1: "P1 ∈ carrier_mat m m"
using sound_HNF P1_H1 unfolding is_sound_HNF_def
by (metis (no_types, lifting) len case_prodD mat_of_rows_carrier(2))
have H1: "H1 ∈ carrier_mat m n"
using sound_HNF P1_H1 unfolding is_sound_HNF_def
by (metis (no_types, lifting) case_prodD len mat_of_rows_carrier(2) mat_of_rows_carrier(3))
have H2: "H2 ∈ carrier_mat m n"
using sound_HNF P2_H2 unfolding is_sound_HNF_def
by (metis (no_types, lifting) len_gs case_prodD mat_of_rows_carrier(2) mat_of_rows_carrier(3))
have P2_H2: "P2 * H2 = mat_of_rows n gs"
by (smt P2_H2 sound_HNF case_prodD is_sound_HNF_def)
have P1_H1_fs: "P1 * H1 = mat_of_rows n fs_init"
by (smt P1_H1 sound_HNF case_prodD is_sound_HNF_def)
obtain inv_P1 where P1_inv_P1: "inverts_mat P1 inv_P1" and inv_P1_P1: "inverts_mat inv_P1 P1"
and inv_P1: "inv_P1 ∈ carrier_mat m m"
using P1 invertible_P1 obtain_inverse_matrix by blast
show "LLL_with_assms n m gs α"
proof (rule LLL_change_basis(2)[OF gs len_gs])
show "P1 * inv_P2 ∈ carrier_mat m m" using P1 inv_P2 by auto
have "mat_of_rows n fs_init = P1 * H1" using sound_HNF P2_H2 unfolding is_sound_HNF_def
by (metis (mono_tags, lifting) P1_H1 case_prodD)
also have "... = P1 * inv_P2 * P2 * H1"
by (smt P1 P2 assoc_mult_mat carrier_matD(1) inv_P2 inv_P2_P2 inverts_mat_def right_mult_one_mat)
also have "... = P1 * inv_P2 * P2 * H2" using H1_H2 by blast
also have "... = P1 * inv_P2 * (P2 * H2)"
using H2 P2 ‹P1 * inv_P2 ∈ carrier_mat m m› assoc_mult_mat by blast
also have "... = P1 * (inv_P2 * P2 * H2)"
by (metis H2 ‹P1 * H1 = P1 * inv_P2 * P2 * H1› ‹P1 * inv_P2 * P2 * H2 = P1 * inv_P2 * (P2 * H2)›
H1_H2 carrier_matD(1) inv_P2 inv_P2_P2 inverts_mat_def left_mult_one_mat)
also have "... = P1 * (inv_P2 * (P2 * H2))" using H2 P2 inv_P2 by auto
also have "... =  P1 * inv_P2 * mat_of_rows n gs"
using P2_H2 ‹P1 * (inv_P2 * P2 * H2) = P1 * (inv_P2 * (P2 * H2))›
‹P1 * inv_P2 * (P2 * H2) = P1 * (inv_P2 * P2 * H2)› by auto
finally show "mat_of_rows n fs_init = P1 * inv_P2 * mat_of_rows n gs" .
show "P2 * inv_P1 ∈ carrier_mat m m"
using P2 inv_P1 by auto
have "mat_of_rows n gs = P2 * H2" using sound_HNF P2_H2 unfolding is_sound_HNF_def by metis
also have "... = P2 * inv_P1 * P1 * H2"
by (smt P1 P2 assoc_mult_mat carrier_matD(1) inv_P1 inv_P1_P1 inverts_mat_def right_mult_one_mat)
also have "... = P2 * inv_P1 * P1 * H1" using H1_H2 by blast
also have "... = P2 * inv_P1 * (P1 * H1)"
using H1 P1 ‹P2 * inv_P1 ∈ carrier_mat m m› assoc_mult_mat by blast
also have "... = P2 * (inv_P1 * P1 * H1)"
by (metis H2 ‹P2 * H2 = P2 * inv_P1 * P1 * H2› ‹P2 * inv_P1 * P1 * H1 = P2 * inv_P1 * (P1 * H1)›
H1_H2 carrier_matD(1) inv_P1 inv_P1_P1 inverts_mat_def left_mult_one_mat)
also have "... = P2 * (inv_P1 * (P1 * H1))" using H1 P1 inv_P1 by auto
also have "... =  P2 * inv_P1 * mat_of_rows n fs_init"
using P1_H1_fs ‹P2 * (inv_P1 * P1 * H1) = P2 * (inv_P1 * (P1 * H1))›
‹P2 * inv_P1 * (P1 * H1) = P2 * (inv_P1 * P1 * H1)› by auto
finally show "mat_of_rows n gs = P2 * inv_P1 * mat_of_rows n fs_init" .
qed
qed

end

text ‹Now, we need to generalize some lemmas.›

context vec_module
begin

(*Generalized version of thm vec_space.finsum_index, now in vec_module*)
lemma finsum_index:
assumes i: "i < n"
and f: "f ∈ A → carrier_vec n"
and A: "A ⊆ carrier_vec n"
shows "finsum V f A \$ i = sum (λx. f x \$ i) A"
using A f
proof (induct A rule: infinite_finite_induct)
case empty
then show ?case using i by simp next
case (insert x X)
then have Xf: "finite X"
and xX: "x ∉ X"
and x: "x ∈ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and fx: "f x ∈ carrier_vec n"
and f: "f ∈ X → carrier_vec n" by auto
have i2: "i < dim_vec (finsum V f X)"
using i finsum_closed[OF f] by auto
have ix: "i < dim_vec x" using x i by auto
show ?case
unfolding finsum_insert[OF Xf xX f fx]
unfolding sum.insert[OF Xf xX]
using insert lincomb_def
by auto
qed (insert i, auto)

(*Generalized version of thm vec_space.mat_of_rows_mult_as_finsum, now in vec_module*)
lemma mat_of_rows_mult_as_finsum:
assumes "v ∈ carrier_vec (length lst)" "⋀ i. i < length lst ⟹ lst ! i ∈ carrier_vec n"
defines "f l ≡ sum (λ i. if l = lst ! i then v \$ i else 0) {0..<length lst}"
shows mat_of_cols_mult_as_finsum:"mat_of_cols n lst *⇩v v = lincomb f (set lst)"
proof -
from assms have "∀ i < length lst. lst ! i ∈ carrier_vec n" by blast
note an = all_nth_imp_all_set[OF this] hence slc:"set lst ⊆ carrier_vec n" by auto
hence dn [simp]:"⋀ x. x ∈ set lst ⟹ dim_vec x = n" by auto
have dl [simp]:"dim_vec (lincomb f (set lst)) = n" using an
by (simp add: slc)
show ?thesis proof
show "dim_vec (mat_of_cols n lst *⇩v v) = dim_vec (lincomb f (set lst))" using assms(1,2) by auto
fix i assume i:"i < dim_vec (lincomb f (set lst))" hence i':"i < n" by auto
with an have fcarr:"(λv. f v ⋅⇩v v) ∈ set lst → carrier_vec n" by auto
from i' have "(mat_of_cols n lst *⇩v v) \$ i = row (mat_of_cols n lst) i ∙ v" by auto
also have "… = (∑ia = 0..<dim_vec v. lst ! ia \$ i * v \$ ia)"
unfolding mat_of_cols_def row_def scalar_prod_def
apply(rule sum.cong[OF refl]) using i an assms(1) by auto
also have "… = (∑ia = 0..<length lst. lst ! ia \$ i * v \$ ia)" using assms(1) by auto
also have "… = (∑x∈set lst. f x * x \$ i)"
unfolding f_def sum_distrib_right apply (subst sum.swap)
apply(rule sum.cong[OF refl])
unfolding if_distrib if_distribR mult_zero_left sum.delta[OF finite_set] by auto
also have "… = (∑x∈set lst. (f x ⋅⇩v x) \$ i)"
apply(rule sum.cong[OF refl],subst index_smult_vec) using i slc by auto
also have "… = (⨁⇘V⇙v∈set lst. f v ⋅⇩v v) \$ i"
unfolding finsum_index[OF i' fcarr slc] by auto
finally show "(mat_of_cols n lst *⇩v v) \$ i = lincomb f (set lst) \$ i"
by (auto simp:lincomb_def)
qed
qed

lemma lattice_of_altdef_lincomb:
assumes "set fs ⊆ carrier_vec n"
shows "lattice_of fs = {y. ∃f. lincomb (of_int ∘ f) (set fs) = y}"
unfolding lincomb_def lattice_of_altdef[OF assms] image_def by auto

end

context vec_module
begin

(*Generalized version of thm idom_vec.lincomb_as_lincomb_list, now in vec_module*)
lemma lincomb_as_lincomb_list:
fixes ws f
assumes s: "set ws ⊆ carrier_vec n"
shows "lincomb f (set ws) = lincomb_list (λi. if ∃j<i. ws!i = ws!j then 0 else f (ws ! i)) ws"
using assms
proof (induct ws rule: rev_induct)
case (snoc a ws)
let ?f = "λi. if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)"
let ?g = "λi. (if ∃j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) ⋅⇩v (ws @ [a]) ! i"
let ?g2= "(λi. (if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)) ⋅⇩v ws ! i)"
have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using snoc.prems(1) by auto
then have ws: "set ws ⊆ carrier_vec n" by auto
have hyp: "lincomb f (set ws) = lincomb_list ?f ws"
by (intro snoc.hyps ws)
show ?case
proof (cases "a∈set ws")
case True
have g_length: "?g (length ws) = 0⇩v n" using True
by (auto, metis in_set_conv_nth nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [0⇩v n]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0⇩v n]" .
have "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
also have "... =  M.sumlist (map ?g [0..<length ws]) + 0⇩v n "
by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
also have "... = M.sumlist (map ?g [0..<length ws] @ [0⇩v n])"
by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append)
finally have summlist_rw: "M.sumlist (map ?g2 [0..<length ws])
= M.sumlist (map ?g [0..<length ws] @ [0⇩v n])" .
have "lincomb f (set (ws @ [a])) = lincomb f (set ws)" using True unfolding lincomb_def
by (simp add: insert_absorb)
thus ?thesis
unfolding hyp lincomb_list_def map_rw summlist_rw
by auto
next
case False
have g_length: "?g (length ws) = f a ⋅⇩v a" using False by (auto simp add: nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" .
have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
have "lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))" by auto
also have "... = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp
also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
proof (rule finsum_insert)
show "finite (set ws)" by auto
show "a ∉ set ws" using False by auto
show "(λv. f v ⋅⇩v v) ∈ set ws → carrier_vec n"
using snoc.prems(1) by auto
show "f a ⋅⇩v a ∈ carrier_vec n" using snoc.prems by auto
qed
also have "... = (f a ⋅⇩v a) + lincomb f (set ws)" unfolding lincomb_def ..
also have "... = (f a ⋅⇩v a) + lincomb_list ?f ws" using hyp by auto
also have "... =  lincomb_list ?f ws  + (f a ⋅⇩v a)"
using M.add.m_comm lincomb_list_carrier snoc.prems by auto
also have "... = lincomb_list (λi. if ∃j<i. (ws @ [a]) ! i
= (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) (ws @ [a])"
proof (unfold lincomb_list_def map_rw summlist_rw, rule M.sumlist_snoc[symmetric])
show "set (map ?g [0..<length ws]) ⊆ carrier_vec n" using snoc.prems
by (auto simp add: nth_append)
show "f a ⋅⇩v a ∈ carrier_vec n"
using snoc.prems by auto
qed
finally show ?thesis .
qed
qed auto
end

context
begin

interpretation vec_module "TYPE(int)" .

lemma lattice_of_cols_as_mat_mult:
assumes A: "A ∈ carrier_mat n nc" (*Integer matrix*)
shows "lattice_of (cols A) = {y∈carrier_vec (dim_row A). ∃x∈carrier_vec (dim_col A). A *⇩v x = y}"
proof -
let ?ws = "cols A"
have set_cols_in: "set (cols A) ⊆ carrier_vec n" using A unfolding cols_def by auto
have "lincomb (of_int ∘ f)(set  ?ws) ∈ carrier_vec (dim_row A)" for f
using lincomb_closed A
by (metis (full_types) carrier_matD(1) cols_dim lincomb_closed)
moreover have "∃x∈carrier_vec (dim_col A). A *⇩v x = lincomb (of_int ∘ f) (set (cols A))" for f
proof -
let ?g = "(λv. of_int (f v))"
let ?g' = "(λi. if ∃j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"
have "lincomb (of_int ∘ f) (set (cols A)) = lincomb ?g (set ?ws)" unfolding o_def by auto
also have "... = lincomb_list ?g' ?ws"
by (rule lincomb_as_lincomb_list[OF set_cols_in])
also have "... = mat_of_cols n ?ws *⇩v vec (length ?ws) ?g'"
by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
also have "... = A *⇩v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto
finally show ?thesis by auto
qed
moreover have "∃f. A *⇩v x = lincomb (of_int ∘ f) (set (cols A))"
if Ax: "A *⇩v x ∈ carrier_vec (dim_row A)" and x: "x ∈ carrier_vec (dim_col A)" for x
proof -
let ?c = "λi. x \$ i"
have x_vec: "vec (length ?ws) ?c = x" using x by auto
have "A *⇩v x = mat_of_cols n ?ws *⇩v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto
also have "... = lincomb_list ?c ?ws"
by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)"
by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)
finally show ?thesis by auto
qed
ultimately show ?thesis unfolding lattice_of_altdef_lincomb[OF set_cols_in]
by (metis (mono_tags, opaque_lifting))
qed

corollary lattice_of_as_mat_mult:
assumes fs: "set fs ⊆ carrier_vec n"
shows "lattice_of fs = {y∈carrier_vec n. ∃x∈carrier_vec (length fs). (mat_of_cols n fs) *⇩v x = y}"
proof -
have cols_eq: "cols (mat_of_cols n fs) = fs" using cols_mat_of_cols[OF fs] by simp
have m: "(mat_of_cols n fs) ∈ carrier_mat n (length fs)" using mat_of_cols_carrier(1) by auto
show ?thesis using lattice_of_cols_as_mat_mult[OF m] unfolding cols_eq using m by auto
qed
end

context vec_space
begin

lemma lin_indpt_cols_imp_det_not_0:
fixes A::"'a mat"
assumes A: "A ∈ carrier_mat n n" and li: "lin_indpt (set (cols A))" and d: "distinct (cols A)"
shows "det A ≠ 0"
using A li d det_rank_iff lin_indpt_full_rank by blast

corollary lin_indpt_rows_imp_det_not_0:
fixes A::"'a mat"
assumes A: "A ∈ carrier_mat n n" and li: "lin_indpt (set (rows A))" and d: "distinct (rows A)"
shows "det A ≠ 0"
using A li d det_rank_iff lin_indpt_full_rank
by (metis (full_types) Determinant.det_transpose cols_transpose transpose_carrier_mat)
end

context LLL
begin

lemma eq_lattice_imp_mat_mult_invertible_cols:
assumes fs: "set fs ⊆ carrier_vec n"
and gs: "set gs ⊆ carrier_vec n"  and ind_fs: "lin_indep fs" (*fs is a basis*)
and length_fs: "length fs = n" and length_gs: "length gs = n" (*For the moment, only valid for square matrices*)
and l: "lattice_of fs = lattice_of gs"
shows "∃Q ∈ carrier_mat n n. invertible_mat Q ∧ mat_of_cols n fs = mat_of_cols n gs * Q"
proof (cases "n=0")
case True
show ?thesis
by (rule bexI[of _ "1⇩m 0"], insert True assms, auto)
next
case False
hence n: "0<n" by simp
have ind_RAT_fs: "gs.lin_indpt (set (RAT fs))" using ind_fs
by (simp add: cof_vec_space.lin_indpt_list_def)
have fs_carrier: "mat_of_cols n fs ∈ carrier_mat n n" by (simp add: length_fs carrier_matI)
let ?f = "(λi. SOME x. x∈carrier_vec (length gs) ∧ (mat_of_cols n gs) *⇩v x = fs ! i)"
let ?cols_Q = "map ?f [0..<length fs]"
let ?Q = "mat_of_cols n ?cols_Q"
show ?thesis
proof (rule bexI[of _ ?Q], rule conjI)
show Q: "?Q ∈ carrier_mat n n" using length_fs by auto
show fs_gs_Q: "mat_of_cols n fs = mat_of_cols n gs * ?Q"
proof (rule mat_col_eqI)
fix j assume j: "j < dim_col (mat_of_cols n gs * ?Q)"
have j2: "j<n" using j Q length_gs by auto
have fs_j_in_gs: "fs ! j ∈ lattice_of gs" using fs l basis_in_latticeI j by auto
have fs_j_carrier_vec: "fs ! j ∈ carrier_vec n"
using fs_j_in_gs gs lattice_of_as_mat_mult by blast
let ?x = "SOME x. x∈carrier_vec (length gs) ∧ (mat_of_cols n gs) *⇩v x = fs ! j"
have "?x∈carrier_vec (length gs) ∧ (mat_of_cols n gs) *⇩v ?x = fs ! j"
by (rule someI_ex, insert fs_j_in_gs lattice_of_as_mat_mult[OF gs], auto)
hence x: "?x ∈ carrier_vec (length gs)"
and gs_x: "(mat_of_cols n gs) *⇩v ?x = fs ! j" by blast+
have "col ?Q j = ?cols_Q ! j"
proof (rule col_mat_of_cols)
show "j < length (map ?f [0..<length fs])" using length_fs j2 by auto
have "map ?f [0..<length fs] ! j = ?f ([0..<length fs] ! j)"
by (rule nth_map, insert j2 length_fs, auto)
also have "... = ?f j" by (simp add: length_fs j2)
also have "... ∈ carrier_vec n" using x length_gs by auto
finally show "map ?f [0..<length fs] ! j ∈ carrier_vec n" .
qed
also have "... = ?f ([0..<length fs] ! j)"
by (rule nth_map, insert j2 length_fs, auto)
also have "... = ?x" by (simp add: length_fs j2)
finally have col_Qj_x: "col ?Q j = ?x" .
have "col (mat_of_cols n fs) j = fs ! j"
by (metis (no_types, lifting) j Q fs length_fs carrier_matD(2) cols_mat_of_cols cols_nth
index_mult_mat(3) mat_of_cols_carrier(3))
also have "... = (mat_of_cols n gs) *⇩v ?x" using gs_x by auto
also have "... = (mat_of_cols n gs) *⇩v (col ?Q j)" unfolding col_Qj_x by simp
also have "... = col (mat_of_cols n gs * ?Q) j"
by (rule col_mult2[symmetric, OF _ Q j2], insert length_gs mat_of_cols_def, auto)
finally show "col (mat_of_cols n fs) j = col (mat_of_cols n gs * ?Q) j" .
qed (insert length_gs gs, auto)
show "invertible_mat ?Q"
(* Sketch of the proof:
1) fs = gs * Q, proved previously
2) gs = fs * Q', similar proof as the previous one.
3) fs = fs * Q' * Q
4) fs * (?Q' * ?Q - 1⇩m n) = 0⇩m n n and hence (?Q' * ?Q - 1⇩m n) = 0 since fs independent
5) det ?Q' = det ?Q = det 1 = 1, then det ?Q = ±1 and ?Q invertible since the determinant
divides a unit.
*)
proof -
let ?f' = "(λi. SOME x. x∈carrier_vec (length fs) ∧ (mat_of_cols n fs) *⇩v x = gs ! i)"
let ?cols_Q' = "map ?f' [0..<length gs]"
let ?Q' = "mat_of_cols n ?cols_Q'"
have Q': "?Q' ∈ carrier_mat n n" using length_gs by auto
have gs_fs_Q': "mat_of_cols n gs = mat_of_cols n fs * ?Q'"
proof (rule mat_col_eqI)
fix j assume j: "j < dim_col (mat_of_cols n fs * ?Q')"
have j2: "j<n" using j Q length_gs by auto
have gs_j_in_fs: "gs ! j ∈ lattice_of fs" using gs l basis_in_latticeI j by auto
have gs_j_carrier_vec: "gs ! j ∈ carrier_vec n"
using gs_j_in_fs fs lattice_of_as_mat_mult by blast
let ?x = "SOME x. x∈carrier_vec (length fs) ∧ (mat_of_cols n fs) *⇩v x = gs ! j"
have "?x∈carrier_vec (length fs) ∧ (mat_of_cols n fs) *⇩v ?x = gs ! j"
by (rule someI_ex, insert gs_j_in_fs lattice_of_as_mat_mult[OF fs], auto)
hence x: "?x ∈ carrier_vec (length fs)"
and fs_x: "(mat_of_cols n fs) *⇩v ?x = gs ! j" by blast+
have "col ?Q' j = ?cols_Q' ! j"
proof (rule col_mat_of_cols)
show "j < length (map ?f' [0..<length gs])" using length_gs j2 by auto
have "map ?f' [0..<length gs] ! j = ?f' ([0..<length gs] ! j)"
by (rule nth_map, insert j2 length_gs, auto)
also have "... = ?f' j" by (simp add: length_gs j2)
also have "... ∈ carrier_vec n" using x length_fs by auto
finally show "map ?f' [0..<length gs] ! j ∈ carrier_vec n" .
qed
also have "... = ?f' ([0..<length gs] ! j)"
by (rule nth_map, insert j2 length_gs, auto)
also have "... = ?x" by (simp add: length_gs j2)
finally have col_Qj_x: "col ?Q' j = ?x" .
have "col (mat_of_cols n gs) j = gs ! j" by (simp add: length_gs gs_j_carrier_vec j2)
also have "... = (mat_of_cols n fs) *⇩v ?x" using fs_x by auto
also have "... = (mat_of_cols n fs) *⇩v (col ?Q' j)" unfolding col_Qj_x by simp
also have "... = col (mat_of_cols n fs * ?Q') j"
by (rule col_mult2[symmetric, OF _ Q' j2], insert length_fs mat_of_cols_def, auto)
finally show "col (mat_of_cols n gs) j = col (mat_of_cols n fs * ?Q') j" .
qed (insert length_fs fs, auto)

have det_fs_not_zero: "rat_of_int (det (mat_of_cols n fs)) ≠ 0"
proof -
let ?A = "(of_int_hom.mat_hom (mat_of_cols n fs)):: rat mat"
have "rat_of_int (det (mat_of_cols n fs)) = det ?A"
by simp
moreover have "det ?A ≠ 0"
proof (rule gs.lin_indpt_cols_imp_det_not_0[of ?A])
have c_eq: "(set (cols ?A)) = set (RAT fs)"
by (metis assms(3) cof_vec_space.lin_indpt_list_def cols_mat_of_cols fs mat_of_cols_map)
show "?A ∈ carrier_mat n n" by (simp add: fs_carrier)
show "gs.lin_indpt (set (cols ?A))" using ind_RAT_fs c_eq by auto
show "distinct (cols ?A)"
by (metis ind_fs cof_vec_space.lin_indpt_list_def cols_mat_of_cols fs mat_of_cols_map)
qed
ultimately show ?thesis by auto
qed
have Q'Q: "?Q' * ?Q ∈ carrier_mat n n" using Q Q' mult_carrier_mat by blast
have fs_fs_Q'Q: "mat_of_cols n fs = mat_of_cols n fs * ?Q' * ?Q" using gs_fs_Q' fs_gs_Q by presburger
hence "0⇩m n n = mat_of_cols n fs * ?Q' * ?Q - mat_of_cols n fs" using length_fs by auto
also have "... = mat_of_cols n fs * ?Q' * ?Q - mat_of_cols n fs * 1⇩m n"
using fs_carrier by auto
also have "... = mat_of_cols n fs * (?Q' * ?Q) - mat_of_cols n fs * 1⇩m n"
using Q Q' fs_carrier by auto
also have "... = mat_of_cols n fs * (?Q' * ?Q - 1⇩m n)"
by (rule mult_minus_distrib_mat[symmetric, OF fs_carrier Q'Q], auto)
finally have "mat_of_cols n fs * (?Q' * ?Q - 1⇩m n) = 0⇩m n n" ..
have "det (?Q' * ?Q) = 1"
by (smt Determinant.det_mult Q Q' Q'Q fs_fs_Q'Q assoc_mult_mat det_fs_not_zero
fs_carrier mult_cancel_left2 of_int_code(2))
hence det_Q'_Q_1: "det ?Q * det ?Q' = 1"
by (metis (no_types, lifting) Determinant.det_mult Groups.mult_ac(2) Q Q')
hence "det ?Q = 1 ∨ det ?Q = -1" by (rule pos_zmult_eq_1_iff_lemma)
thus ?thesis using invertible_iff_is_unit_JNF[OF Q] by fastforce
qed
qed
qed

corollary eq_lattice_imp_mat_mult_invertible_rows:
assumes fs: "set fs ⊆ carrier_vec n"
and gs: "set gs ⊆ carrier_vec n"  and ind_fs: "lin_indep fs" (*fs is a basis*)
and length_fs: "length fs = n" and length_gs: "length gs = n" (*For the moment, only valid for square matrices*)
and l: "lattice_of fs = lattice_of gs"
shows "∃P ∈ carrier_mat n n. invertible_mat P ∧ mat_of_rows n fs = P * mat_of_rows n gs"
proof -
obtain Q where Q: "Q ∈ carrier_mat n n" and inv_Q: "invertible_mat Q"
and fs_gs_Q: "mat_of_cols n fs = mat_of_cols n gs * Q"
using eq_lattice_imp_mat_mult_invertible_cols[OF assms] by auto
have "invertible_mat Q⇧T" by (simp add: inv_Q invertible_mat_transpose)
moreover have "mat_of_rows n fs = Q⇧T * mat_of_rows n gs" using fs_gs_Q
by (metis Matrix.transpose_mult Q length_gs mat_of_cols_carrier(1) transpose_mat_of_cols)
moreover have "Q⇧T ∈ carrier_mat n n" using Q by auto
ultimately show ?thesis by blast
qed
end

subsubsection ‹Missing results›

text ‹This is a new definition for upper triangular matrix, valid for rectangular matrices.
This definition will allow us to prove that echelon form implies upper triangular for any matrix.›

definition "upper_triangular' A = (∀i < dim_row A. ∀ j<dim_col A. j < i ⟶ A \$\$ (i,j) = 0)"

lemma upper_triangular'D[elim] :
"upper_triangular' A ⟹ j<dim_col A ⟹ j < i ⟹ i < dim_row A ⟹ A \$\$ (i,j) = 0"
unfolding upper_triangular'_def by auto

lemma upper_triangular'I[intro] :
"(⋀i j. j<dim_col A ⟹ j < i ⟹ i < dim_row A ⟹ A \$\$ (i,j) = 0) ⟹ upper_triangular' A"
unfolding upper_triangular'_def by auto

lemma prod_list_abs(*[simp]?*):
fixes xs:: "int list"
shows "prod_list (map abs xs) = abs (prod_list xs)"
by (induct xs, auto simp add: abs_mult)

lemma euclid_ext2_works:
assumes "euclid_ext2 a b = (p,q,u,v,d)"
shows "p*a+q*b = d" and "d = gcd a b" and "gcd a b * u = -b" and "gcd a b * v = a"
and "u = -b div gcd a b" and "v = a div gcd a b"
using assms unfolding euclid_ext2_def
by (auto simp add: bezout_coefficients_fst_snd)

lemma res_function_euclidean2:
"res_function (λb n::'a::{unique_euclidean_ring}. n mod b)"
proof-
have "n mod b = n" if "b=0" for n b::"'a :: unique_euclidean_ring" using that by auto
hence "res_function_euclidean = (λb n::'a. n mod b)"
by (unfold fun_eq_iff res_function_euclidean_def, auto)
thus ?thesis using res_function_euclidean by auto
qed

lemma mult_row_1_id:
fixes A:: "'a::semiring_1^'n^'m"
shows "mult_row A b 1 = A" unfolding mult_row_def by vector

text ‹Results about appending rows›

lemma row_append_rows1:
assumes A: "A ∈ carrier_mat m n"
and B: "B ∈ carrier_mat p n"
assumes i: "i < dim_row A"
shows "Matrix.row (A @⇩r B) i = Matrix.row A i"
proof (rule eq_vecI)
have AB_carrier[simp]: "(A @⇩r B) ∈ carrier_mat (m+p) n" by (rule carrier_append_rows[OF A B])
thus "dim_vec (Matrix.row (A @⇩r B) i) = dim_vec (Matrix.row A i)"
using A B by (auto, insert carrier_matD(2), blast)
fix j assume j: "j < dim_vec (Matrix.row A i)"
have "Matrix.row (A @⇩r B) i \$v j = (A @⇩r B) \$\$ (i, j)"
by (metis AB_carrier Matrix.row_def j A carrier_matD(2) index_row(2) index_vec)
also have "... = (if i < dim_row A then A \$\$ (i, j) else B \$\$ (i - m, j))"
by (rule append_rows_nth, insert assms j, auto)
also have "... = A\$\$ (i,j)" using i by simp
finally show "Matrix.row (A @⇩r B) i \$v j = Matrix.row A i \$v j" using i j by simp
qed

lemma row_append_rows2:
assumes A: "A ∈ carrier_mat m n"
and B: "B ∈ carrier_mat p n"
assumes i: "i ∈ {m..<m+p}"
shows "Matrix.row (A @⇩r B) i = Matrix.row B (i - m)"
proof (rule eq_vecI)
have AB_carrier[simp]: "(A @⇩r B) ∈ carrier_mat (m+p) n" by (rule carrier_append_rows[OF A B])
thus "dim_vec (Matrix.row (A @⇩r B) i) = dim_vec (Matrix.row B (i-m))"
using A B by (auto, insert carrier_matD(2), blast)
fix j assume j: "j < dim_vec (Matrix.row B (i-m))"
have "Matrix.row (A @⇩r B) i \$v j = (A @⇩r B) \$\$ (i, j)"
by (metis AB_carrier Matrix.row_def j B carrier_matD(2) index_row(2) index_vec)
also have "... = (if i < dim_row A then A \$\$ (i, j) else B \$\$ (i - m, j))"
by (rule append_rows_nth, insert assms j, auto)
also have "... = B \$\$ (i - m, j)" using i A by simp
finally show "Matrix.row (A @⇩r B) i \$v j = Matrix.row B (i-m) \$v j" using i j A B by auto
qed

lemma rows_append_rows:
assumes A: "A ∈ carrier_mat m n"
and B: "B ∈ carrier_mat p n"
shows "Matrix.rows (A @⇩r B) = Matrix.rows A @ Matrix.rows B"
proof -
have AB_carrier: "(A @⇩r B) ∈ carrier_mat (m+p) n"
by (rule carrier_append_rows, insert A B, auto)
hence 1: "dim_row (A @⇩r B) = dim_row A + dim_row B" using A B by blast
moreover have "Matrix.row (A @⇩r B) i = (Matrix.rows A @ Matrix.rows B) ! i"
if i: "i < dim_row (A @⇩r B)" for i
proof (cases "i<dim_row A")
case True
have "Matrix.row (A @⇩r B) i = Matrix.row A i" using A True B row_append_rows1 by blast
also have "... = Matrix.rows A ! i" unfolding Matrix.rows_def using True by auto
also have "... = (Matrix.rows A @ Matrix.rows B) ! i" using True by (simp add: nth_append)
finally show ?thesis .
next
case False
have i_mp: "i < m + p" using AB_carrier A B i by fastforce
have "Matrix.row (A @⇩r B) i = Matrix.row B (i-m)" using A False B i row_append_rows2 i_mp
by (smt AB_carrier atLeastLessThan_iff carrier_matD(1) le_add1
also have "... = Matrix.rows B ! (i-m)" unfolding Matrix.rows_def using False i A 1 by auto
also have "... = (Matrix.rows A @ Matrix.rows B) ! (i-m+m)"
by (metis add_diff_cancel_right' A carrier_matD(1) length_rows not_add_less2 nth_append)
also have "... =  (Matrix.rows A @ Matrix.rows B) ! i" using False A by auto
finally show ?thesis .
qed
ultimately show ?thesis unfolding list_eq_iff_nth_eq by auto
qed

lemma append_rows_nth2:
assumes A': "A' ∈ carrier_mat m n"
and B: "B ∈ carrier_mat p n"
and A_def: "A = (A' @⇩r  B)"
and a: "a<m" and ap: "a < p" and j: "j<n"
shows "A \$\$ (a + m, j) = B \$\$ (a,j)"
proof -
have "A \$\$ (a + m, j) = (if a + m < dim_row A' then A' \$\$ (a + m, j) else B \$\$ (a + m - m, j))"
unfolding A_def by (rule append_rows_nth[OF A' B _ j], insert ap a, auto)
also have "... = B \$\$ (a,j)" using ap a A' by auto
finally show ?thesis .
qed

lemma append_rows_nth3:
assumes A': "A' ∈ carrier_mat m n"
and B: "B ∈ carrier_mat p n"
and A_def: "A = (A' @⇩r  B)"
and a: "a≥m" and ap: "a < m + p" and j: "j<n"
shows "A \$\$ (a, j) = B \$\$ (a-m,j)"
proof -
have "A \$\$ (a, j) = (if a < dim_row A' then A' \$\$ (a, j) else B \$\$ (a - m, j))"
unfolding A_def by (rule append_rows_nth[OF A' B _ j], insert ap a, auto)
also have "... = B \$\$ (a-m,j)" using ap a A' by auto
finally show ?thesis .
qed

text ‹Results about submatrices›

lemma pick_first_id: assumes i: "i<n" shows "pick {0..<n} i = i"
proof -
have "i = (card {a ∈ {0..<n}. a < i})" using i
by (auto, smt Collect_cong card_Collect_less_nat nat_SN.gt_trans)
thus ?thesis using pick_card_in_set i
by (metis atLeastLessThan_iff zero_order(1))
qed

lemma submatrix_index_id:
assumes H: "H ∈ carrier_mat m n" and i: "i<k1" and j: "j<k2"
and k1: "k1≤m" and k2: "k2≤n"
shows "(submatrix H {0..<k1} {0..<k2}) \$\$ (i,j) = H \$\$ (i,j)"
proof -
let ?I = "{0..<k1}"
let ?J = "{0..<k2}"
let ?H = "submatrix H ?I ?J"
have km: "k1≤m" and kn: "k2≤n" using k1 k2 by simp+
have card_mk: "card {i. i < m ∧ i < k1} = k1" using km
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have card_nk: "card {i. i < n ∧ i < k2} = k2" using kn
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
show ?thesis
proof-
have pick_j: "pick ?J j = j" by (rule pick_first_id[OF j])
have pick_i: "pick ?I i = i" by (rule pick_first_id[OF i])
have "submatrix H ?I ?J \$\$ (i, j) = H \$\$ (pick ?I i, pick ?J j)"
by (rule submatrix_index, insert H i j card_mk card_nk, auto)
also have "... = H \$\$ (i,j)" using pick_i pick_j by simp
finally show ?thesis .
qed
qed

lemma submatrix_carrier_first:
assumes H: "H ∈ carrier_mat m n"
and k1: "k1 ≤ m" and k2: "k2 ≤ n"
shows"submatrix H {0..<k1} {0..<k2} ∈ carrier_mat k1 k2"
proof -
have km: "k1≤m" and kn: "k2≤n" using k1 k2 by simp+
have card_mk: "card {i. i < m ∧ i < k1} = k1" using km
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have card_nk: "card {i. i < n ∧ i < k2} = k2" using kn
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
show ?thesis
by (smt Collect_cong H atLeastLessThan_iff card_mk card_nk carrier_matD
carrier_matI dim_submatrix zero_order(1))
qed

lemma Units_eq_invertible_mat:
assumes "A ∈ carrier_mat n n"
shows "A ∈ Group.Units (ring_mat TYPE('a::comm_ring_1) n b) = invertible_mat A" (is "?lhs = ?rhs")
proof -
interpret m: ring "ring_mat TYPE('a) n b" by (rule ring_mat)
show ?thesis
proof
assume "?lhs" thus "?rhs"
unfolding Group.Units_def
by (insert assms, auto simp add: ring_mat_def invertible_mat_def inverts_mat_def)
next
assume "?rhs"
from this obtain B where AB: "A * B = 1⇩m n" and BA: "B * A = 1⇩m n" and B: "B ∈ carrier_mat n n"
by (metis assms carrier_matD(1) inverts_mat_def obtain_inverse_matrix)
hence "∃x∈carrier (ring_mat TYPE('a) n b). x ⊗⇘ring_mat TYPE('a) n b⇙ A = 𝟭⇘ring_mat TYPE('a) n b⇙
∧ A ⊗⇘ring_mat TYPE('a) n b⇙ x = 𝟭⇘ring_mat TYPE('a) n b⇙"
unfolding ring_mat_def by auto
thus "?lhs" unfolding Group.Units_def using assms unfolding ring_mat_def by auto
qed
qed

lemma map_first_rows_index:
assumes "A ∈ carrier_mat M n" and "m ≤ M" and "i<m" and "ja<n"
shows "map (Matrix.row A) [0..<m] ! i \$v ja = A \$\$ (i, ja)"
using assms by auto

lemma matrix_append_rows_eq_if_preserves:
assumes A: "A ∈ carrier_mat (m+p) n" and B: "B ∈ carrier_mat p n"
and eq: "∀i∈{m..<m+p}.∀j<n. A\$\$(i,j) = B \$\$ (i-m,j)"
shows "A = mat_of_rows n [Matrix.row A i. i ← [0..<m]] @⇩r B" (is "_ = ?A' @⇩r _")
proof (rule eq_matI)
have A': "?A' ∈ carrier_mat m n" by (simp add: mat_of_rows_def)
hence A'B: "?A' @⇩r B ∈ carrier_mat (m+p) n" using B by blast
show "dim_row A = dim_row (?A' @⇩r B)" and "dim_col A = dim_col (?A' @⇩r B)" using A'B A by auto
fix i j assume i: "i < dim_row (?A' @⇩r B)"
and j: "j < dim_col (?A' @⇩r B)"
have jn: "j<n" using A
by (metis append_rows_def dim_col_mat(1) index_mat_four_block(3) index_zero_mat(3)
j mat_of_rows_def nat_arith.rule0)
let ?xs = "(map (Matrix.row A) [0..<m])"
show "A \$\$ (i, j) = (?A' @⇩r B) \$\$ (i, j)"
proof (cases "i<m")
case True
have "(?A' @⇩r B) \$\$ (i, j) = ?A' \$\$ (i,j)"
by (metis (no_types, lifting) Nat.add_0_right True append_rows_def diff_zero i
index_mat_four_block index_zero_mat(3) j length_map length_upt mat_of_rows_carrier(2))
also have "... = ?xs ! i \$v j"
by (rule mat_of_rows_index, insert i True j, auto simp add: append_rows_def)
also have "... = A \$\$ (i,j)"
by (rule map_first_rows_index, insert assms A True i jn, auto)
finally show ?thesis ..
next
case False
have "(?A' @⇩r B) \$\$ (i, j) = B \$\$ (i-m,j)"
by (smt (z3) A' carrier_matD(1) False append_rows_def i index_mat_four_block j jn length_map
length_upt mat_of_rows_carrier(2,3))
also have "... = A \$\$ (i,j)"
by (metis False append_rows_def B eq atLeastLessThan_iff carrier_matD(1) diff_zero i
index_mat_four_block(2) index_zero_mat(2) jn le_add1 length_map length_upt
finally show ?thesis ..
qed
qed

lemma invertible_mat_first_column_not0:
fixes A::"'a :: comm_ring_1 mat"
assumes A: "A ∈ carrier_mat n n" and inv_A: "invertible_mat A" and n0: "0<n"
shows "col A 0 ≠ (0⇩v n)"
proof (rule ccontr)
assume " ¬ col A 0 ≠ 0⇩v n" hence col_A0: "col A 0 = 0⇩v n" by simp
have "(det A dvd 1)" using inv_A invertible_iff_is_unit_JNF[OF A] by auto
hence 1: "det A ≠ 0" by auto
have "det A = (∑i<n. A \$\$ (i, 0) * Determinant.cofactor A i 0)"
by (rule laplace_expansion_column[OF A n0])
also have "... = 0"
by (rule sum.neutral, insert col_A0 n0 A, auto simp add: col_def,
metis Matrix.zero_vec_def index_vec mult_zero_left)
finally show False using 1 by contradiction
qed

lemma invertible_mat_mult_int:
assumes "A = P * B"
and "P ∈ carrier_mat n n"
and "B ∈ carrier_mat n n"
and "invertible_mat P"
and "invertible_mat (map_mat rat_of_int B)"
shows "invertible_mat (map_mat rat_of_int A)"
by (metis (no_types, opaque_lifting) assms dvd_field_iff
invertible_iff_is_unit_JNF invertible_mult_JNF map_carrier_mat not_is_unit_0
of_int_hom.hom_0 of_int_hom.hom_det of_int_hom.mat_hom_mult)

lemma echelon_form_JNF_intro:
assumes "(∀i<dim_row A. is_zero_row_JNF i A ⟶ ¬ (∃j. j < dim_row A ∧ j>i ∧ ¬ is_zero_row_JNF j A))"
and "(∀i j. i<j ∧ j<dim_row A ∧ ¬ (is_zero_row_JNF i A) ∧ ¬ (is_zero_row_JNF j A)
⟶ ((LEAST n. A \$\$ (i, n) ≠ 0) < (LEAST n. A \$\$ (j, n) ≠ 0)))"
shows "echelon_form_JNF A" using assms unfolding echelon_form_JNF_def by simp

lemma echelon_form_submatrix:
assumes ef_H: "echelon_form_JNF H" and H: "H ∈ carrier_mat m n"
and k: "k ≤ min m n"
shows "echelon_form_JNF (submatrix H {0..<k} {0..<k})"
proof -
let ?I = "{0..<k}"
let ?H = "submatrix H ?I ?I"
have km: "k≤m" and kn: "k≤n" using k by simp+
have card_mk: "card {i. i < m ∧ i < k} = k" using km
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have card_nk: "card {i. i < n ∧ i < k} = k" using kn
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have H_ij: "H \$\$ (i,j) = (submatrix H ?I ?I) \$\$ (i,j)"  if i: "i<k" and j: "j<k" for i j
proof-
have pick_j: "pick ?I j = j" by (rule pick_first_id[OF j])
have pick_i: "pick ?I i = i" by (rule pick_first_id[OF i])
have "submatrix H ?I ?I \$\$ (i, j) = H \$\$ (pick ?I i, pick ?I j)"
by (rule submatrix_index, insert H i j card_mk card_nk, auto)
also have "... = H \$\$ (i,j)" using pick_i pick_j by simp
finally show ?thesis ..
qed
have H'[simp]: "?H ∈ carrier_mat k k"
using H dim_submatrix[of H "{0..<k}" "{0..<k}"] card_mk card_nk by auto
show ?thesis
proof (rule echelon_form_JNF_intro, auto)
fix i j assume iH'_0: "is_zero_row_JNF i ?H" and ij: "i < j" and j: "j < dim_row ?H"
have jm: "j<m"
by (metis H' carrier_matD(1) j km le_eq_less_or_eq nat_SN.gt_trans)
show "is_zero_row_JNF j ?H"
proof (rule ccontr)
assume j_not0_H': "¬ is_zero_row_JNF j ?H"
define a where "a = (LEAST n. ?H \$\$ (j,n) ≠ 0)"
have H'_ja: "?H \$\$ (j,a) ≠ 0"
by (metis (mono_tags) LeastI j_not0_H' a_def is_zero_row_JNF_def)
have a: "a < dim_col ?H"
by (smt j_not0_H' a_def is_zero_row_JNF_def linorder_neqE_nat not_less_Least order_trans_rules(19))
have j_not0_H: "¬ is_zero_row_JNF j H"
by (metis H' H'_ja H_ij a assms(2) basic_trans_rules(19) carrier_matD is_zero_row_JNF_def j kn le_eq_less_or_eq)
hence i_not0_H: "¬ is_zero_row_JNF i H" using ef_H j ij unfolding echelon_form_JNF_def
by (metis H' ‹¬ is_zero_row_JNF j H› assms(2) carrier_matD(1) ij j km
not_less_iff_gr_or_eq order.strict_trans order_trans_rules(21))
hence least_ab: "(LEAST n. H \$\$ (i, n) ≠ 0) < (LEAST n. H \$\$ (j, n) ≠ 0)" using jm
using j_not0_H assms(2) echelon_form_JNF_def ef_H ij by blast
define b where "b = (LEAST n. H \$\$ (i, n) ≠ 0)"
have H_ib: "H \$\$ (i, b) ≠ 0"
by (metis (mono_tags, lifting) LeastI b_def i_not0_H is_zero_row_JNF_def)
have b: "b < dim_col ?H" using least_ab a unfolding a_def b_def
by (metis (mono_tags, lifting) H' H'_ja H_ij a_def carrier_matD dual_order.strict_trans j nat_neq_iff not_less_Least)
have H'_ib: "?H \$\$ (i,b) ≠ 0" using H_ib b H_ij H' ij j
by (metis H' carrier_matD dual_order.strict_trans ij j)
hence "¬ is_zero_row_JNF i ?H" using b is_zero_row_JNF_def by blast
thus False using iH'_0 by contradiction
qed
next
fix i j assume ij: "i < j" and j: "j < dim_row ?H"
have jm: "j<m"
by (metis H' carrier_matD(1) j km le_eq_less_or_eq nat_SN.gt_trans)
assume not0_iH': "¬ is_zero_row_JNF i ?H"
and not0_jH': "¬ is_zero_row_JNF j ?H"
define a where "a = (LEAST n. ?H \$\$ (i, n) ≠ 0)"
define b where "b = (LEAST n. ?H \$\$ (j, n) ≠ 0)"
have H'_ia: "?H \$\$ (i,a) ≠ 0"
by (metis (mono_tags) LeastI_ex a_def is_zero_row_JNF_def not0_iH')
have H'_jb: "?H \$\$ (j,b) ≠ 0"
by (metis (mono_tags) LeastI_ex b_def is_zero_row_JNF_def not0_jH')
have a: "a < dim_row ?H"
by (smt H' a_def carrier_matD is_zero_row_JNF_def less_trans linorder_neqE_nat not0_iH' not_less_Least)
have b: "b < dim_row ?H"
by (smt H' b_def carrier_matD is_zero_row_JNF_def less_trans linorder_neqE_nat not0_jH' not_less_Least)
have a_eq: "a = (LEAST n. H \$\$ (i, n) ≠ 0)"
by (smt H' H'_ia H_ij LeastI_ex a a_def carrier_matD(1) ij j linorder_neqE_nat not_less_Least order_trans_rules(19))
have b_eq: "b = (LEAST n. H \$\$ (j, n) ≠ 0)"
by (smt H' H'_jb H_ij LeastI_ex b b_def carrier_matD(1) ij j linorder_neqE_nat not_less_Least order_trans_rules(19))
have not0_iH: "¬ is_zero_row_JNF i H"
by (metis H' H'_ia H_ij a H carrier_matD ij is_zero_row_JNF_def j kn le_eq_less_or_eq order.strict_trans)
have not0_jH: "¬ is_zero_row_JNF j H"
by (metis H' H'_jb H_ij b H carrier_matD is_zero_row_JNF_def j kn le_eq_less_or_eq order.strict_trans)
show "(LEAST n. ?H \$\$ (i, n) ≠ 0) < (LEAST n. ?H \$\$ (j, n) ≠ 0)"
unfolding a_def[symmetric] b_def[symmetric] a_eq b_eq using not0_iH not0_jH ef_H ij jm H
unfolding echelon_form_JNF_def by auto
qed
qed

lemma HNF_submatrix:
assumes HNF_H: "Hermite_JNF associates res H" and H: "H ∈ carrier_mat m n"
and k: "k ≤ min m n"
shows "Hermite_JNF associates res (submatrix H {0..<k} {0..<k})"
proof -
let ?I = "{0..<k}"
let ?H = "submatrix H ?I ?I"
have km: "k≤m" and kn: "k≤n" using k by simp+
have card_mk: "card {i. i < m ∧ i < k} = k" using km
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have card_nk: "card {i. i < n ∧ i < k} = k" using kn
by (smt Collect_cong card_Collect_less_nat le_eq_less_or_eq nat_less_induct nat_neq_iff)
have H_ij: "H \$\$ (i,j) = (submatrix H ?I ?I) \$\$ (i,j)"  if i: "i<k" and j: "j<k" for i j
proof-
have pick_j: "pick ?I j = j" by (rule pick_first_id[OF j])
have pick_i: "pick ?I i = i" by (rule pick_first_id[OF i])
have "submatrix H ?I ?I \$\$ (i, j) = H \$\$ (pick ?I i, pick ?I j)"
by (rule submatrix_index, insert H i j card_mk card_nk, auto)
also have "... = H \$\$ (i,j)" using pick_i pick_j by simp
finally show ?thesis ..
qed
have H'[simp]: "?H ∈ carrier_mat k k"
using H dim_submatrix[of H "{0..<k}" "{0..<k}"] card_mk card_nk by auto
have CS_ass: "Complete_set_non_associates associates" using HNF_H unfolding Hermite_JNF_def by simp
moreover have CS_res: "Complete_set_residues res"  using HNF_H unfolding Hermite_JNF_def by simp
have ef_H: "echelon_form_JNF H" using HNF_H unfolding Hermite_JNF_def by auto
have ef_H': "echelon_form_JNF ?H"
by (rule echelon_form_submatrix[OF ef_H H k])
have HNF1: "?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0) ∈ associates"
and HNF2: "(∀j<i. ?H \$\$ (j, LEAST n. ?H \$\$ (i, n) ≠ 0)
∈ res (?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0)))"
if i: "i<dim_row ?H" and not0_iH': "¬ is_zero_row_JNF i ?H" for i
proof -
define a where "a = (LEAST n. ?H \$\$ (i, n) ≠ 0)"
have im: "i<m"
by (metis H' carrier_matD(1) km order.strict_trans2 that(1))
have H'_ia: "?H \$\$ (i,a) ≠ 0"
by (metis (mono_tags) LeastI_ex a_def is_zero_row_JNF_def not0_iH')
have a: "a < dim_row ?H"
by (smt H' a_def carrier_matD is_zero_row_JNF_def less_trans linorder_neqE_nat not0_iH' not_less_Least)
have a_eq: "a = (LEAST n. H \$\$ (i, n) ≠ 0)"
by (smt H' H'_ia H_ij LeastI_ex a a_def carrier_matD(1) i linorder_neqE_nat not_less_Least order_trans_rules(19))
have H'_ia_H_ia: "?H \$\$ (i, a) = H \$\$ (i, a)"  by (metis H' H_ij a carrier_matD(1) i)
have not'_iH: "¬ is_zero_row_JNF i H"
by (metis H' H'_ia H'_ia_H_ia a assms(2) carrier_matD(1) carrier_matD(2) is_zero_row_JNF_def kn order.strict_trans2)
thus "?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0) ∈ associates" using im
by (metis H'_ia_H_ia Hermite_JNF_def a_def a_eq HNF_H H carrier_matD(1))
show "(∀j<i. ?H \$\$ (j, LEAST n. ?H \$\$ (i, n) ≠ 0)
∈ res (?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0)))"
proof -
{ fix nn :: nat
have ff1: "∀n. ?H \$\$ (n, a) = H \$\$ (n, a) ∨ ¬ n < k"
by (metis (no_types) H' H_ij a carrier_matD(1))
have ff2: "i < k"
by (metis H' carrier_matD(1) that(1))
then have "H \$\$ (nn, a) ∈ res (H \$\$ (i, a)) ⟶ H \$\$ (nn, a) ∈ res (?H \$\$ (i, a))"
using ff1 by (metis (no_types))
moreover
{ assume "H \$\$ (nn, a) ∈ res (?H \$\$ (i, a))"
then have "?H \$\$ (nn, a) = H \$\$ (nn, a) ⟶ ?H \$\$ (nn, a) ∈ res (?H \$\$ (i, a))"
by presburger
then have "¬ nn < i ∨ ?H \$\$ (nn, LEAST n. ?H \$\$ (i, n) ≠ 0) ∈ res (?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0))"
using ff2 ff1 a_def order.strict_trans by blast }
ultimately have "¬ nn < i ∨ ?H \$\$ (nn, LEAST n. ?H \$\$ (i, n) ≠ 0) ∈ res (?H \$\$ (i, LEAST n. ?H \$\$ (i, n) ≠ 0))"
using Hermite_JNF_def a_eq assms(1) assms(2) im not'_iH by blast }
then show ?thesis
by meson
qed
qed
show ?thesis using HNF1 HNF2 ef_H' CS_res CS_ass unfolding Hermite_JNF_def by blast
qed

lemma HNF_of_HNF_id:
fixes H :: "int mat"
assumes HNF_H: "Hermite_JNF associates res H"
and H: "H ∈ carrier_mat n n"
and H_P1_H1: "H = P1 * H1"
and inv_P1: "invertible_mat P1"
and H1: "H1 ∈ carrier_mat n n"
and P1: "P1 ∈ carrier_mat n n"
and HNF_H1: "Hermite_JNF associates res H1"
and inv_H: "invertible_mat (map_mat rat_of_int H)"
shows "H1 = H"
proof (rule HNF_unique_generalized_JNF[OF H P1 H1 _ H H_P1_H1])
show "H = (1⇩m n) * H" using H by auto
qed (insert assms, auto)

(*Some of the following lemmas could be moved outside this context*)

context
fixes n :: nat
begin

interpretation vec_module "TYPE(int)" .

lemma lattice_is_monotone:
fixes S T
assumes S: "set S ⊆ carrier_vec n"
assumes T: "set T ⊆ carrier_vec n"
assumes subs: "set S ⊆ set T"
shows "lattice_of S ⊆ lattice_of T"
proof -
have "∃fa. lincomb fa (set T) = lincomb f (set S)" for f
proof -
let ?f = "λi. if i ∈ set T - set S then 0 else f i"
have set_T_eq: "set T = set S ∪ (set T - set S)" using subs by blast
have l0: "lincomb ?f (set T - set S) = 0⇩v n" by (rule lincomb_zero, insert T, auto)
have "lincomb ?f (set T) = lincomb ?f (set S ∪ (set T - set S))" using set_T_eq by simp
also have "... = lincomb ?f (set S) + lincomb ?f (set T - set S)"
by (rule lincomb_union, insert S T subs, auto)
also have "... = lincomb ?f (set S)" using l0 by (auto simp add: S)
also have "... = lincomb f (set S)" using S by fastforce
finally show ?thesis by blast
qed
thus ?thesis unfolding lattice_of_altdef_lincomb[OF S] lattice_of_altdef_lincomb[OF T]
by auto
qed

lemma lattice_of_append:
assumes fs: "set fs ⊆ carrier_vec n"
assumes gs: "set gs ⊆ carrier_vec n"
shows "lattice_of (fs @ gs) = lattice_of (gs @ fs)"
proof -
have fsgs: "set (fs @ gs) ⊆<```