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 "… = (∑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 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: "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 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 ≠ (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) ⊆<