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]
      unfolding index_add_vec(1)[OF i2]
      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 " = (xset 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 " = (xset lst. (f x v x) $ i)"
      apply(rule sum.cong[OF refl],subst index_smult_vec) using i slc by auto
    also have " = (Vvset 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 "aset ws")
    case True    
    have g_length: "?g (length ws) = 0v 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]) @ [0v n]" using g_length by simp
    finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0v 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]) + 0v n "
      by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
    also have "... = M.sumlist (map ?g [0..<length ws] @ [0v 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] @ [0v 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 "... = (Vvset (a # ws). f v v v)" unfolding lincomb_def ..
    also have "... = (Vv insert a (set ws). f v v v)" by simp    
    also have "... = (f a v a) + (Vv (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) = {ycarrier_vec (dim_row A). xcarrier_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 "xcarrier_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 = {ycarrier_vec n. xcarrier_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 _ "1m 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. xcarrier_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. xcarrier_vec (length gs)  (mat_of_cols n gs) *v x = fs ! j"
      have "?xcarrier_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 - 1m n) = 0m n n and hence (?Q' * ?Q - 1m 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. xcarrier_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. xcarrier_vec (length fs)  (mat_of_cols n fs) *v x = gs ! j"
        have "?xcarrier_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 "0m 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 * 1m n"
        using fs_carrier by auto
      also have "... = mat_of_cols n fs * (?Q' * ?Q) - mat_of_cols n fs * 1m n"
        using Q Q' fs_carrier by auto
      also have "... = mat_of_cols n fs * (?Q' * ?Q - 1m n)"
        by (rule mult_minus_distrib_mat[symmetric, OF fs_carrier Q'Q], auto)      
      finally have "mat_of_cols n fs * (?Q' * ?Q - 1m n) = 0m 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 QT" by (simp add: inv_Q invertible_mat_transpose)
  moreover have "mat_of_rows n fs = QT * 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 "QT  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
          linordered_semidom_class.add_diff_inverse row_append_rows2)
    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: "am" 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: "k1m" and k2: "k2n"
  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: "k1m" and kn: "k2n" 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: "k1m" and kn: "k2n" 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 = 1m n" and BA: "B * A = 1m n" and B: "B  carrier_mat n n"
      by (metis assms carrier_matD(1) inverts_mat_def obtain_inverse_matrix)
    hence "xcarrier (ring_mat TYPE('a) n b). x ring_mat TYPE('a) n bA = 𝟭ring_mat TYPE('a) n b A ring_mat TYPE('a) n bx = 𝟭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 
          linordered_semidom_class.add_diff_inverse mat_of_rows_carrier(2))
    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  (0v n)"
proof (rule ccontr)
  assume " ¬ col A 0  0v n" hence col_A0: "col A 0 = 0v 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: "km" and kn: "kn" 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: "km" and kn: "kn" 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 = (1m 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) = 0v 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) <