Theory SNF_Uniqueness
section ‹Uniqueness of the Smith normal form›
theory SNF_Uniqueness
imports
Cauchy_Binet
Smith_Normal_Form_JNF
Admits_SNF_From_Diagonal_Iff_Bezout_Ring
begin
lemma dvd_associated1:
fixes a::"'a::comm_ring_1"
assumes "∃u. u dvd 1 ∧ a = u*b"
shows "a dvd b ∧ b dvd a"
using assms by auto
text ‹This is a key lemma. It demands the type class to be an integral domain. This means that
the uniqueness result will be obtained for GCD domains, instead of rings.›
lemma dvd_associated2:
fixes a::"'a::idom"
assumes ab: "a dvd b" and ba: "b dvd a" and a: "a≠0"
shows "∃u. u dvd 1 ∧ a = u*b"
proof -
obtain k where a_kb: "a = k*b" using ab unfolding dvd_def
by (metis Groups.mult_ac(2) ba dvdE)
obtain q where b_qa: "b = q*a" using ba unfolding dvd_def
by (metis Groups.mult_ac(2) ab dvdE)
have 1: "a = k*q*a" using a_kb b_qa by auto
hence "k*q = 1" using a by simp
thus ?thesis using 1 by (metis a_kb dvd_triv_left)
qed
corollary dvd_associated:
fixes a::"'a::idom"
assumes "a≠0"
shows "(a dvd b ∧ b dvd a) = (∃u. u dvd 1 ∧ a = u*b)"
using assms dvd_associated1 dvd_associated2 by metis
lemma exists_inj_ge_index:
assumes S: "S ⊆ {0..<n}" and Sk: "card S = k"
shows "∃f. inj_on f {0..<k} ∧ f`{0..<k} = S ∧ (∀i∈{0..<k}. i ≤ f i)"
proof -
have "∃h. bij_betw h {0..<k} S"
using S Sk ex_bij_betw_nat_finite subset_eq_atLeast0_lessThan_finite by blast
from this obtain g where inj_on_g: "inj_on g {0..<k}" and gk_S: "g`{0..<k} = S"
unfolding bij_betw_def by blast
let ?f = "strict_from_inj k g"
have "strict_mono_on {0..<k} ?f" by (rule strict_strict_from_inj[OF inj_on_g])
hence 1: "inj_on ?f {0..<k}" using strict_mono_on_imp_inj_on by blast
have 2: "?f`{0..<k} = S" by (simp add: strict_from_inj_image' inj_on_g gk_S)
have 3: "∀i∈{0..<k}. i ≤ ?f i"
proof
fix i assume i: "i ∈ {0..<k}"
let ?xs = "sorted_list_of_set (g`{0..<k})"
have "strict_from_inj k g i = ?xs ! i" unfolding strict_from_inj_def using i by auto
moreover have "i ≤ ?xs ! i"
proof (rule sorted_wrt_less_idx, rule sorted_distinct_imp_sorted_wrt)
show "sorted ?xs"
using sorted_sorted_list_of_set by blast
show "distinct ?xs" using distinct_sorted_list_of_set by blast
show "i < length ?xs"
by (metis S Sk atLeast0LessThan distinct_card distinct_sorted_list_of_set gk_S i
lessThan_iff set_sorted_list_of_set subset_eq_atLeast0_lessThan_finite)
qed
ultimately show "i ≤ ?f i" by auto
qed
show ?thesis using 1 2 3 by auto
qed
subsection ‹More specific results about submatrices›
lemma diagonal_imp_submatrix0:
assumes dA: "diagonal_mat A" and A_carrier: "A∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and r: "∀row_index ∈ I. row_index < n"
and c: "∀col_index ∈ J. col_index < m"
and a: "a<k" and b: "b<k"
shows "submatrix A I J $$ (a, b) = 0 ∨ submatrix A I J $$ (a,b) = A $$(pick I a, pick I a)"
proof (cases "submatrix A I J $$ (a, b) = 0")
case True
then show ?thesis by auto
next
case False note not0 = False
have aux: "submatrix A I J $$ (a, b) = A $$(pick I a, pick J b)"
proof (rule submatrix_index)
have "card {i. i < dim_row A ∧ i ∈ I} = k"
by (smt A_carrier Ik carrier_matD(1) equalityI mem_Collect_eq r subsetI)
moreover have "card {i. i < dim_col A ∧ i ∈ J} = k"
by (metis (no_types, lifting) A_carrier Jk c carrier_matD(2) carrier_mat_def
equalityI mem_Collect_eq subsetI)
ultimately show " a < card {i. i < dim_row A ∧ i ∈ I}"
and "b < card {i. i < dim_col A ∧ i ∈ J}" using a b by auto
qed
thus ?thesis
proof (cases "pick I a = pick J b")
case True
then show ?thesis using aux by auto
next
case False
then show ?thesis
by (metis aux A_carrier Ik Jk a b c carrier_matD dA diagonal_mat_def pick_in_set_le r)
qed
qed
lemma diagonal_imp_submatrix_element_not0:
assumes dA: "diagonal_mat A"
and A_carrier: "A ∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and I: "I ⊆ {0..<n}"
and J: "J ⊆ {0..<m}"
and b: "b < k"
and ex_not0: "∃i. i<k ∧ submatrix A I J $$ (i, b) ≠ 0"
shows "∃!i. i<k ∧ submatrix A I J $$ (i, b) ≠ 0"
proof -
have I_eq: "I = {i. i < dim_row A ∧ i ∈ I}" using I A_carrier unfolding carrier_mat_def by auto
have J_eq: "J = {i. i < dim_col A ∧ i ∈ J}" using J A_carrier unfolding carrier_mat_def by auto
obtain a where sub_ab: "submatrix A I J $$ (a, b) ≠ 0" and ak: "a < k" using ex_not0 by auto
moreover have "i = a" if sub_ib: "submatrix A I J $$ (i, b) ≠ 0" and ik: "i < k" for i
proof -
have 1: "pick I i < dim_row A"
using I_eq Ik ik pick_in_set_le by auto
have 2: "pick J b < dim_col A"
using J_eq Jk b pick_le by auto
have 3: "pick I a < dim_row A"
using I_eq Ik calculation(2) pick_le by auto
have "submatrix A I J $$ (i, b) = A $$ (pick I i, pick J b)"
by (rule submatrix_index, insert I_eq Ik ik J_eq Jk b, auto)
hence pick_Ii_Jb: "pick I i = pick J b" using dA sub_ib 1 2 unfolding diagonal_mat_def by auto
have "submatrix A I J $$ (a, b) = A $$ (pick I a, pick J b)"
by (rule submatrix_index, insert I_eq Ik ak J_eq Jk b, auto)
hence pick_Ia_Jb: "pick I a = pick J b" using dA sub_ab 3 2 unfolding diagonal_mat_def by auto
have pick_Ia_Ii: "pick I a = pick I i" using pick_Ii_Jb pick_Ia_Jb by simp
thus ?thesis by (metis Ik ak ik nat_neq_iff pick_mono_le)
qed
ultimately show ?thesis by auto
qed
lemma submatrix_index_exists:
assumes A_carrier: "A∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and a: "a ∈ I" and b: "b ∈ J" and k: "k > 0"
and I: "I ⊆ {0..<n}" and J: "J ⊆ {0..<m}"
shows "∃a' b'. a' < k ∧ b' < k ∧ submatrix A I J $$ (a',b') = A $$ (a,b)
∧ a = pick I a' ∧ b = pick J b'"
proof -
let ?xs = "sorted_list_of_set I"
let ?ys = "sorted_list_of_set J"
have finI: "finite I" and finJ: "finite J" using k Ik Jk card_ge_0_finite by metis+
have set_xs: "set ?xs = I" by (rule set_sorted_list_of_set[OF finI])
have set_ys: "set ?ys = J" by (rule set_sorted_list_of_set[OF finJ])
have a_in_xs: "a ∈ set ?xs" and b_in_ys: "b ∈ set ?ys" using set_xs a set_ys b by auto
have length_xs: "length ?xs = k" by (metis Ik distinct_card set_xs sorted_list_of_set(3))
have length_ys: "length ?ys = k" by (metis Jk distinct_card set_ys sorted_list_of_set(3))
obtain a' where a': "?xs ! a' = a" and a'_length: "a' < length ?xs"
by (meson a_in_xs in_set_conv_nth)
obtain b' where b': "?ys ! b' = b" and b'_length: "b' < length ?ys"
by (meson b_in_ys in_set_conv_nth)
have pick_a: "a = pick I a'" using a' a'_length finI sorted_list_of_set_eq_pick by auto
have pick_b: "b = pick J b'" using b' b'_length finJ sorted_list_of_set_eq_pick by auto
have I_rw: "I = {i. i < dim_row A ∧ i ∈ I}" and J_rw: "J = {i. i < dim_col A ∧ i ∈ J}"
using I A_carrier J by auto
have a'k: "a' < k" using a'_length length_xs by auto
moreover have b'k: "b'<k" using b'_length length_ys by auto
moreover have sub_eq: "submatrix A I J $$ (a', b') = A $$ (a, b)"
unfolding pick_a pick_b
by (rule submatrix_index, insert J_rw I_rw Ik Jk a'_length length_xs b'_length length_ys, auto)
ultimately show ?thesis using pick_a pick_b by auto
qed
lemma mat_delete_submatrix_insert:
assumes A_carrier: "A ∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and I: "I ⊆ {0..<n}" and J: "J ⊆ {0..<m}"
and a: "a < n" and b: "b < m"
and k: "k < min n m"
and a_notin_I: "a ∉ I" and b_notin_J: "b ∉ J"
and a'k: "a' < Suc k" and b'k: "b' < Suc k"
and a_def: "pick (insert a I) a' = a"
and b_def: "pick (insert b J) b' = b"
shows "mat_delete (submatrix A (insert a I) (insert b J)) a' b' = submatrix A I J" (is "?lhs = ?rhs")
proof (rule eq_matI)
have I_eq: "I = {i. i < dim_row A ∧ i ∈ I}"
using I A_carrier unfolding carrier_mat_def by auto
have J_eq: "J = {i. i < dim_col A ∧ i ∈ J}"
using J A_carrier unfolding carrier_mat_def by auto
have insert_I_eq: "insert a I = {i. i < dim_row A ∧ i ∈ insert a I}"
using I A_carrier a k unfolding carrier_mat_def by auto
have card_Suc_k: "card {i. i < dim_row A ∧ i ∈ insert a I} = Suc k"
using insert_I_eq Ik a_notin_I
by (metis I card_insert_disjoint finite_atLeastLessThan finite_subset)
have insert_J_eq: "insert b J = {i. i < dim_col A ∧ i ∈ insert b J}"
using J A_carrier b k unfolding carrier_mat_def by auto
have card_Suc_k': "card {i. i < dim_col A ∧ i ∈ insert b J} = Suc k"
using insert_J_eq Jk b_notin_J
by (metis J card_insert_disjoint finite_atLeastLessThan finite_subset)
show "dim_row ?lhs = dim_row ?rhs"
unfolding mat_delete_dim unfolding dim_submatrix using card_Suc_k I_eq Ik by auto
show "dim_col ?lhs = dim_col ?rhs"
unfolding mat_delete_dim unfolding dim_submatrix using card_Suc_k' J_eq Jk by auto
fix i j assume i: "i < dim_row (submatrix A I J)"
and j: "j < dim_col (submatrix A I J)"
have ik: "i < k" by (metis I_eq Ik dim_submatrix(1) i)
have jk: "j < k" by (metis J_eq Jk dim_submatrix(2) j)
show "?lhs $$ (i, j) = ?rhs $$ (i, j)"
proof -
have index_eq1: "pick (insert a I) (insert_index a' i) = pick I i"
by (rule pick_insert_index[OF Ik a_notin_I ik a_def], simp add: Ik a'k)
have index_eq2: "pick (insert b J) (insert_index b' j) = pick J j"
by (rule pick_insert_index[OF Jk b_notin_J jk b_def], simp add: Jk b'k)
have "?lhs $$ (i,j)
= (submatrix A (insert a I) (insert b J)) $$ (insert_index a' i, insert_index b' j)"
proof (rule mat_delete_index[symmetric, OF _ a'k b'k ik jk])
show "submatrix A (insert a I) (insert b J) ∈ carrier_mat (Suc k) (Suc k)"
by (metis card_Suc_k card_Suc_k' carrier_matI dim_submatrix(1) dim_submatrix(2))
qed
also have "... = A $$ (pick (insert a I) (insert_index a' i), pick (insert b J) (insert_index b' j))"
proof (rule submatrix_index)
show "insert_index a' i < card {i. i < dim_row A ∧ i ∈ insert a I}"
using card_Suc_k ik insert_index_def by auto
show "insert_index b' j < card {j. j < dim_col A ∧ j ∈ insert b J}"
using card_Suc_k' insert_index_def jk by auto
qed
also have "... = A $$ (pick I i, pick J j)" unfolding index_eq1 index_eq2 by auto
also have "... = submatrix A I J $$ (i,j)"
by (rule submatrix_index[symmetric], insert ik I_eq Ik Jk J_eq jk, auto)
finally show ?thesis .
qed
qed
subsection ‹On the minors of a diagonal matrix›
lemma det_minors_diagonal:
assumes dA: "diagonal_mat A" and A_carrier: "A ∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and r: "I ⊆ {0..<n}"
and c: "J ⊆ {0..<m}" and k: "k>0"
shows "det (submatrix A I J) = 0
∨ (∃xs. (det (submatrix A I J) = prod_list xs ∨ det (submatrix A I J) = - prod_list xs)
∧ set xs ⊆ {A$$(i,i)|i. i<min n m ∧ A$$(i,i)≠ 0} ∧ length xs = k)"
using Ik Jk r c k
proof (induct k arbitrary: I J)
case 0
then show ?case by auto
next
case (Suc k)
note cardI = Suc.prems(1)
note cardJ = Suc.prems(2)
note I = Suc.prems(3)
note J = Suc.prems(4)
have *: "{i. i < dim_row A ∧ i ∈ I} = I" using I Ik A_carrier carrier_mat_def by auto
have **: "{j. j < dim_col A ∧ j ∈ J} = J" using J Jk A_carrier carrier_mat_def by auto
show ?case
proof (cases "k = 0")
case True note k0 = True
from this obtain a where aI: "I = {a}" using True cardI card_1_singletonE by auto
from this obtain b where bJ: "J = {b}" using True cardJ card_1_singletonE by auto
have an: "a<n" using aI I by auto
have bm: "b<m" using bJ J by auto
have sub_carrier: "submatrix A {a} {b} ∈ carrier_mat 1 1"
unfolding carrier_mat_def submatrix_def
using * ** aI bJ by auto
have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)"
by (rule det_singleton[OF sub_carrier])
have 2: "... = A $$ (a,b)"
by (rule submatrix_singleton_index[OF A_carrier an bm])
show ?thesis
proof (cases "A $$ (a,b) ≠ 0")
let ?xs = "[submatrix A {a} {b} $$ (0,0)]"
case True
hence "a = b" using dA A_carrier an bm unfolding diagonal_mat_def carrier_mat_def by auto
hence "set ?xs ⊆ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0}"
using 2 True an bm by auto
moreover have "det (submatrix A {a} {b}) = prod_list ?xs" using 1 by auto
moreover have "length ?xs = Suc k" using k0 by auto
ultimately show ?thesis using an bm unfolding aI bJ by blast
next
case False
then show ?thesis using 1 2 aI bJ by auto
qed
next
case False
hence k0: "0 < k" by simp
have k: "k < min n m"
by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute
min_def not_less subset_eq_atLeast0_lessThan_card)
have subIJ_carrier: "(submatrix A I J) ∈ carrier_mat (Suc k) (Suc k)"
unfolding carrier_mat_def using * ** cardI cardJ
unfolding submatrix_def by auto
obtain b' where b'k: "b' < Suc k" by auto
let ?f="λi. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'"
have det_rw: "det (submatrix A I J)
= (∑i<Suc k. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b')"
by (rule laplace_expansion_column[OF subIJ_carrier b'k])
show ?thesis
proof (cases "∃a'<Suc k. submatrix A I J $$ (a',b') ≠ 0")
case True
obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') ≠ 0"
and a'k: "a' < Suc k"
and unique: "∀j. j<Suc k ∧ submatrix A I J $$ (j,b') ≠ 0 ⟶ j = a'"
using diagonal_imp_submatrix_element_not0[OF dA A_carrier cardI cardJ I J b'k True] by auto
have "submatrix A I J $$ (a', b') = A $$ (pick I a', pick J b')"
by (rule submatrix_index, auto simp add: "*" a'k cardI "**" b'k cardJ)
from this obtain a b where an: "a < n" and bm: "b < m"
and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)"
and pick_a: "pick I a' = a" and pick_b: "pick J b' = b"
using * ** A_carrier a'k b'k cardI cardJ pick_le by fastforce
obtain I' where aI': "I = insert a I'" and a_notin: "a ∉ I'"
by (metis Set.set_insert a'k cardI pick_a pick_in_set_le)
obtain J' where bJ': "J = insert b J'" and b_notin: "b ∉ J'"
by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le)
have Suc_k0: "0 < Suc k" by simp
have aI: "a ∈ I" using aI' by auto
have bJ: "b ∈ J" using bJ' by auto
have cardI': "card I' = k"
by (metis aI' a_notin cardI card.infinite card_insert_disjoint
finite_insert nat.inject nat.simps(3))
have cardJ': "card J' = k"
by (metis bJ' b_notin cardJ card.infinite card_insert_disjoint
finite_insert nat.inject nat.simps(3))
have I': "I' ⊆ {0..<n}" using I aI' by blast
have J': "J' ⊆ {0..<m}" using J bJ' by blast
have det_sub_I'J': "Determinant.det (submatrix A I' J') = 0 ∨
(∃xs. (det (submatrix A I' J') = prod_list xs ∨ det (submatrix A I' J') = - prod_list xs)
∧ set xs ⊆ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0} ∧ length xs = k)"
proof (rule Suc.hyps[OF cardI' cardJ' _ _ k0])
show "I' ⊆ {0..<n}" using I aI' by blast
show "J' ⊆ {0..<m}" using J bJ' by blast
qed
have mat_delete_sub:
"mat_delete (submatrix A (insert a I') (insert b J')) a' b' = submatrix A I' J'"
by (rule mat_delete_submatrix_insert[OF A_carrier cardI' cardJ' I' J' an bm k
a_notin b_notin a'k b'k],insert pick_a pick_b aI' bJ', auto)
have set_rw: "{0..<Suc k} = insert a' ({0..<Suc k}-{a'})"
by (simp add: a'k insert_absorb)
have rw0: "sum ?f ({0..<Suc k}-{a'}) = 0" by (rule sum.neutral, insert unique, auto)
have "det (submatrix A I J)
= (∑i<Suc k. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b')"
by (rule laplace_expansion_column[OF subIJ_carrier b'k])
also have "... = ?f a' + sum ?f ({0..<Suc k}-{a'})"
by (metis (no_types, lifting) Diff_iff atLeast0LessThan finite_atLeastLessThan
finite_insert set_rw singletonI sum.insert)
also have "... = ?f a'" using rw0 unfolding cofactor_def by auto
also have "... = submatrix A I J $$ (a', b') * ((-1) ^ (a' + b') * det (submatrix A I' J'))"
unfolding cofactor_def using mat_delete_sub aI' bJ' by simp
finally have det_submatrix_IJ: "det (submatrix A I J)
= A $$ (a, b) * ((- 1) ^ (a' + b') * det (submatrix A I' J'))" unfolding sub_index .
show ?thesis
proof (cases "det (submatrix A I' J') = 0")
case True
then show ?thesis using det_submatrix_IJ by auto
next
case False note det_not0 = False
from this obtain xs where prod_list_xs: "det (submatrix A I' J') = prod_list xs
∨ det (submatrix A I' J') = - prod_list xs"
and xs: "set xs ⊆ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0}"
and length_xs: "length xs = k"
using det_sub_I'J' by blast
let ?ys = "A$$(a,b) # xs"
have length_ys: "length ?ys = Suc k" using length_xs by auto
have a_eq_b: "a=b"
using A_carrier an bm sub_IJ_0 sub_index dA unfolding diagonal_mat_def by auto
have A_aa_in: "A$$(a,a) ∈ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0}"
using a_eq_b an bm sub_IJ_0 sub_index by auto
have ys: "set ?ys ⊆ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0}"
using xs A_aa_in a_eq_b by auto
show ?thesis
proof (cases "even (a'+b')")
case True
have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * det (submatrix A I' J')"
using det_submatrix_IJ True by auto
show ?thesis
proof (cases "det (submatrix A I' J') = prod_list xs")
case True
have "det (submatrix A I J) = prod_list ?ys"
using det_submatrix_IJ unfolding True by auto
then show ?thesis using ys length_ys by blast
next
case False
hence "det (submatrix A I' J') = - prod_list xs" using prod_list_xs by simp
hence "det (submatrix A I J) = - prod_list ?ys" using det_submatrix_IJ by auto
then show ?thesis using ys length_ys by blast
qed
next
case False
have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * - det (submatrix A I' J')"
using det_submatrix_IJ False by auto
show ?thesis
proof (cases "det (submatrix A I' J') = prod_list xs")
case True
have "det (submatrix A I J) = - prod_list ?ys"
using det_submatrix_IJ unfolding True by auto
then show ?thesis using ys length_ys by blast
next
case False
hence "det (submatrix A I' J') = - prod_list xs" using prod_list_xs by simp
hence "det (submatrix A I J) = prod_list ?ys" using det_submatrix_IJ by auto
then show ?thesis using ys length_ys by blast
qed
qed
qed
next
case False
have "sum ?f {0..<Suc k} = 0" by (rule sum.neutral, insert False, auto)
thus ?thesis using det_rw
by (simp add: atLeast0LessThan)
qed
qed
qed
definition "minors A k = {det (submatrix A I J)| I J. I ⊆ {0..<dim_row A}
∧ J ⊆ {0..<dim_col A} ∧ card I = k ∧ card J = k}"
lemma Gcd_minors_dvd:
fixes A::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes PAQ_B: "P * A * Q = B"
and P: "P ∈ carrier_mat m m"
and A: "A ∈ carrier_mat m n"
and Q: "Q ∈ carrier_mat n n"
and I: "I ⊆ {0..<dim_row A}" and J: "J ⊆ {0..<dim_col A}"
and Ik: "card I = k" and Jk: "card J = k"
shows "Gcd (minors A k) dvd det (submatrix B I J)"
proof -
let ?subPA = "submatrix (P * A) I UNIV"
let ?subQ = "submatrix Q UNIV J"
have subPA: "?subPA ∈ carrier_mat k n"
proof -
have "I = {i. i < dim_row P ∧ i ∈ I}" using P I A by auto
hence "card {i. i < dim_row P ∧ i ∈ I} = k" using Ik by auto
thus ?thesis using A unfolding submatrix_def by auto
qed
have subQ: "submatrix Q UNIV J ∈ carrier_mat n k"
proof -
have J_eq: "J = {j. j < dim_col Q ∧ j ∈ J}" using Q J A by auto
hence "card {j. j < dim_col Q ∧ j ∈ J} = k" using Jk by auto
moreover have "card {i. i < dim_row Q ∧ i ∈ UNIV} = n" using Q by auto
ultimately show ?thesis unfolding submatrix_def by auto
qed
have sub_sub_PA: "(submatrix ?subPA UNIV I') = submatrix (P * A) I I'" for I'
using submatrix_split2[symmetric] by auto
have det_subPA_rw: "det (submatrix (P * A) I I') =
(∑J' | J' ⊆ {0..<m} ∧ card J' = k. det ((submatrix P I J')) * det (submatrix A J' I'))"
if I'1: "I' ⊆ {0..<n}" and I'2: "card I' = k" for I'
proof -
have "submatrix (P * A) I I' = submatrix P I UNIV * submatrix A UNIV I'"
unfolding submatrix_mult ..
also have "det ... = (∑C | C ⊆ {0..<m} ∧ card C = k.
det (submatrix (submatrix P I UNIV) UNIV C) * det (submatrix (submatrix A UNIV I') C UNIV))"
proof (rule Cauchy_Binet)
have "I = {i. i < dim_row P ∧ i ∈ I}" using P I A by auto
thus "submatrix P I UNIV ∈ carrier_mat k m" using Ik P unfolding submatrix_def by auto
have "I' = {j. j < dim_col A ∧ j ∈ I'}" using I'1 A by auto
thus "submatrix A UNIV I' ∈ carrier_mat m k" using I'2 A unfolding submatrix_def by auto
qed
also have "... = (∑J' | J' ⊆ {0..<m} ∧ card J' = k.
det (submatrix P I J') * det (submatrix A J' I'))"
unfolding submatrix_split2[symmetric] submatrix_split[symmetric] by simp
finally show ?thesis .
qed
have "det (submatrix B I J) = det (submatrix (P*A*Q) I J)" using PAQ_B by simp
also have "... = det (?subPA * ?subQ)" unfolding submatrix_mult by auto
also have "... = (∑I' | I' ⊆ {0..<n} ∧ card I' = k. det (submatrix ?subPA UNIV I')
* det (submatrix ?subQ I' UNIV))"
by (rule Cauchy_Binet[OF subPA subQ])
also have "... = (∑I' | I' ⊆ {0..<n} ∧ card I' = k.
det (submatrix (P * A) I I') * det (submatrix Q I' J))"
using submatrix_split[symmetric, of Q] submatrix_split2[symmetric, of "P*A"] by presburger
also have "... = (∑I' | I' ⊆ {0..<n} ∧ card I' = k. ∑J' | J' ⊆ {0..<m} ∧ card J' = k.
det (submatrix P I J') * det (submatrix A J' I') * det (submatrix Q I' J))"
using det_subPA_rw by (simp add: semiring_0_class.sum_distrib_right)
finally have det_rw: "det (submatrix B I J) = (∑I' | I' ⊆ {0..<n} ∧ card I' = k.
∑J' | J' ⊆ {0..<m} ∧ card J' = k.
det (submatrix P I J') * det (submatrix A J' I') * det (submatrix Q I' J))" .
show ?thesis
proof (unfold det_rw, (rule dvd_sum)+)
fix I' J'
assume I': "I' ∈ {I'. I' ⊆ {0..<n} ∧ card I' = k}"
and J': "J' ∈ {J'. J' ⊆ {0..<m} ∧ card J' = k}"
have "Gcd (minors A k) dvd det (submatrix A J' I')"
by (rule Gcd_dvd, unfold minors_def, insert A I' J', auto)
then show "Gcd (minors A k) dvd det (submatrix P I J') * det (submatrix A J' I')
* det (submatrix Q I' J)" by auto
qed
qed
lemma det_minors_diagonal2:
assumes dA: "diagonal_mat A" and A_carrier: "A ∈ carrier_mat n m"
and Ik: "card I = k" and Jk: "card J = k"
and r: "I ⊆ {0..<n}"
and c: "J ⊆ {0..<m}" and k: "k>0"
shows "det (submatrix A I J) = 0 ∨ (∃S. S ⊆ {0..<min n m} ∧ card S = k ∧ S=I ∧
(det (submatrix A I J) = (∏i∈S. A $$ (i,i)) ∨ det (submatrix A I J) = - (∏i∈S. A $$ (i,i))))"
using Ik Jk r c k
proof (induct k arbitrary: I J)
case 0
then show ?case by auto
next
case (Suc k)
note cardI = Suc.prems(1)
note cardJ = Suc.prems(2)
note I = Suc.prems(3)
note J = Suc.prems(4)
have *: "{i. i < dim_row A ∧ i ∈ I} = I" using I Ik A_carrier carrier_mat_def by auto
have **: "{j. j < dim_col A ∧ j ∈ J} = J" using J Jk A_carrier carrier_mat_def by auto
show ?case
proof (cases "k = 0")
case True note k0 = True
from this obtain a where aI: "I = {a}" using True cardI card_1_singletonE by auto
from this obtain b where bJ: "J = {b}" using True cardJ card_1_singletonE by auto
have an: "a<n" using aI I by auto
have bm: "b<m" using bJ J by auto
have sub_carrier: "submatrix A {a} {b} ∈ carrier_mat 1 1"
unfolding carrier_mat_def submatrix_def
using * ** aI bJ by auto
have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)"
by (rule det_singleton[OF sub_carrier])
have 2: "... = A $$ (a,b)"
by (rule submatrix_singleton_index[OF A_carrier an bm])
show ?thesis
proof (cases "A $$ (a,b) ≠ 0")
let ?S="{a}"
case True
hence ab: "a = b" using dA A_carrier an bm unfolding diagonal_mat_def carrier_mat_def by auto
hence "?S ⊆ {0..<min n m}" using an bm by auto
moreover have "det (submatrix A {a} {b}) = (∏i∈?S. A $$ (i, i))" using 1 2 ab by auto
moreover have "card ?S = Suc k" using k0 by auto
ultimately show ?thesis using an bm unfolding aI bJ by blast
next
case False
then show ?thesis using 1 2 aI bJ by auto
qed
next
case False
hence k0: "0 < k" by simp
have k: "k < min n m"
by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute
min_def not_less subset_eq_atLeast0_lessThan_card)
have subIJ_carrier: "(submatrix A I J) ∈ carrier_mat (Suc k) (Suc k)"
unfolding carrier_mat_def using * ** cardI cardJ
unfolding submatrix_def by auto
obtain b' where b'k: "b' < Suc k" by auto
let ?f="λi. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'"
have det_rw: "det (submatrix A I J)
= (∑i<Suc k. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b')"
by (rule laplace_expansion_column[OF subIJ_carrier b'k])
show ?thesis
proof (cases "∃a'<Suc k. submatrix A I J $$ (a',b') ≠ 0")
case True
obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') ≠ 0"
and a'k: "a' < Suc k"
and unique: "∀j. j<Suc k ∧ submatrix A I J $$ (j,b') ≠ 0 ⟶ j = a'"
using diagonal_imp_submatrix_element_not0[OF dA A_carrier cardI cardJ I J b'k True] by auto
have "submatrix A I J $$ (a', b') = A $$ (pick I a', pick J b')"
by (rule submatrix_index, auto simp add: "*" a'k cardI "**" b'k cardJ)
from this obtain a b where an: "a < n" and bm: "b < m"
and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)"
and pick_a: "pick I a' = a" and pick_b: "pick J b' = b"
using * ** A_carrier a'k b'k cardI cardJ pick_le by fastforce
obtain I' where aI': "I = insert a I'" and a_notin: "a ∉ I'"
by (metis Set.set_insert a'k cardI pick_a pick_in_set_le)
obtain J' where bJ': "J = insert b J'" and b_notin: "b ∉ J'"
by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le)
have Suc_k0: "0 < Suc k" by simp
have aI: "a ∈ I" using aI' by auto
have bJ: "b ∈ J" using bJ' by auto
have cardI': "card I' = k"
by (metis aI' a_notin cardI card.infinite card_insert_disjoint
finite_insert nat.inject nat.simps(3))
have cardJ': "card J' = k"
by (metis bJ' b_notin cardJ card.infinite card_insert_disjoint
finite_insert nat.inject nat.simps(3))
have I': "I' ⊆ {0..<n}" using I aI' by blast
have J': "J' ⊆ {0..<m}" using J bJ' by blast
have det_sub_I'J': "det (submatrix A I' J') = 0 ∨ (∃S⊆{0..<min n m}. card S = k ∧ S=I'
∧ (det (submatrix A I' J') = (∏i∈S. A $$ (i, i))
∨ det (submatrix A I' J') = - (∏i∈S. A $$ (i, i))))"
proof (rule Suc.hyps[OF cardI' cardJ' _ _ k0])
show "I' ⊆ {0..<n}" using I aI' by blast
show "J' ⊆ {0..<m}" using J bJ' by blast
qed
have mat_delete_sub:
"mat_delete (submatrix A (insert a I') (insert b J')) a' b' = submatrix A I' J'"
by (rule mat_delete_submatrix_insert[OF A_carrier cardI' cardJ' I' J' an bm k
a_notin b_notin a'k b'k],insert pick_a pick_b aI' bJ', auto)
have set_rw: "{0..<Suc k} = insert a' ({0..<Suc k}-{a'})"
by (simp add: a'k insert_absorb)
have rw0: "sum ?f ({0..<Suc k}-{a'}) = 0" by (rule sum.neutral, insert unique, auto)
have "det (submatrix A I J)
= (∑i<Suc k. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b')"
by (rule laplace_expansion_column[OF subIJ_carrier b'k])
also have "... = ?f a' + sum ?f ({0..<Suc k}-{a'})"
by (metis (no_types, lifting) Diff_iff atLeast0LessThan finite_atLeastLessThan
finite_insert set_rw singletonI sum.insert)
also have "... = ?f a'" using rw0 unfolding cofactor_def by auto
also have "... = submatrix A I J $$ (a', b') * ((-1) ^ (a' + b') * det (submatrix A I' J'))"
unfolding cofactor_def using mat_delete_sub aI' bJ' by simp
finally have det_submatrix_IJ: "det (submatrix A I J)
= A $$ (a, b) * ((- 1) ^ (a' + b') * det (submatrix A I' J'))" unfolding sub_index .
show ?thesis
proof (cases "det (submatrix A I' J') = 0")
case True
then show ?thesis using det_submatrix_IJ by auto
next
case False note det_not0 = False
from this obtain xs where prod_list_xs: "det (submatrix A I' J') = (∏i∈xs. A $$ (i, i))
∨ det (submatrix A I' J') = - (∏i∈xs. A $$ (i, i))"
and xs: "xs⊆{0..<min n m}"
and length_xs: "card xs = k"
and xs_I': "xs=I'"
using det_sub_I'J' by blast
let ?ys = "insert a xs"
have a_notin_xs: "a ∉ xs"
by (simp add: xs_I' a_notin)
have length_ys: "card ?ys = Suc k"
using length_xs a_notin_xs by (simp add: card_ge_0_finite k0)
have a_eq_b: "a=b"
using A_carrier an bm sub_IJ_0 sub_index dA unfolding diagonal_mat_def by auto
have A_aa_in: "A$$(a,a) ∈ {A $$ (i, i) |i. i < min n m ∧ A $$ (i, i) ≠ 0}"
using a_eq_b an bm sub_IJ_0 sub_index by auto
show ?thesis
proof (cases "even (a'+b')")
case True
have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * det (submatrix A I' J')"
using det_submatrix_IJ True by auto
show ?thesis
proof (cases "det (submatrix A I' J') = (∏i∈xs. A $$ (i, i))")
case True
have "det (submatrix A I J) = (∏i∈?ys. A $$ (i, i))"
using det_submatrix_IJ unfolding True a_eq_b
by (metis (no_types, lifting) a_notin_xs a_eq_b
card_ge_0_finite k0 length_xs prod.insert)
then show ?thesis using length_ys
using a_eq_b an bm xs xs_I'
by (simp add: aI')
next
case False
hence "det (submatrix A I' J') = - (∏i∈xs. A $$ (i, i))" using prod_list_xs by simp
hence "det (submatrix A I J) = -(∏i∈?ys. A $$ (i, i))" using det_submatrix_IJ a_eq_b
by (metis (no_types, lifting) a_notin_xs card_ge_0_finite k0
length_xs mult_minus_right prod.insert)
then show ?thesis using length_ys
using a_eq_b an bm xs aI' xs_I' by force
qed
next
case False
have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * - det (submatrix A I' J')"
using det_submatrix_IJ False by auto
show ?thesis
proof (cases "det (submatrix A I' J') = (∏i∈xs. A $$ (i, i))")
case True
have "det (submatrix A I J) = - (∏i∈?ys. A $$ (i, i))"
using det_submatrix_IJ unfolding True
by (metis (no_types, lifting) a_eq_b a_notin_xs card_ge_0_finite k0
length_xs mult_minus_right prod.insert)
then show ?thesis using length_ys
using a_eq_b an bm xs aI' xs_I' by force
next
case False
hence "det (submatrix A I' J') = - (∏i∈xs. A $$ (i, i))" using prod_list_xs by simp
hence "det (submatrix A I J) = (∏i∈?ys. A $$ (i, i))" using det_submatrix_IJ
by (metis (mono_tags, lifting) a_eq_b a_notin_xs card_ge_0_finite
equation_minus_iff k0 length_xs prod.insert)
then show ?thesis using length_ys
using a_eq_b an bm xs aI' xs_I' by force
qed
qed
qed
next
case False
have "sum ?f {0..<Suc k} = 0" by (rule sum.neutral, insert False, auto)
thus ?thesis using det_rw
by (simp add: atLeast0LessThan)
qed
qed
qed
subsection ‹Relating minors and GCD›
lemma diagonal_dvd_Gcd_minors:
fixes A::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat n m"
and SNF_A: "Smith_normal_form_mat A"
shows "(∏i=0..<k. A $$ (i,i)) dvd Gcd (minors A k)"
proof (cases "k=0")
case True
then show ?thesis by auto
next
case False
hence k: "0<k" by simp
show ?thesis
proof (rule Gcd_greatest)
have diag_A: "diagonal_mat A"
using SNF_A unfolding Smith_normal_form_mat_def isDiagonal_mat_def diagonal_mat_def by auto
fix b assume b_in_minors: "b ∈ minors A k"
show "(∏i = 0..<k. A $$ (i, i)) dvd b"
proof (cases "b=0")
case True
then show ?thesis by auto
next
case False
obtain I J where b: "b = det (submatrix A I J)" and I: "I ⊆ {0..<dim_row A} "
and J: "J ⊆ {0..<dim_col A}" and Ik: "card I = k" and Jk: "card J = k"
using b_in_minors unfolding minors_def by blast
obtain S where S: "S ⊆ {0..<min n m}" and Sk: "card S = k"
and det_subS: "det (submatrix A I J) = (∏i∈S. A $$ (i,i))
∨ det (submatrix A I J) = -(∏i∈S. A $$ (i,i))"
using det_minors_diagonal2[OF diag_A A Ik Jk _ _ k] I J A False b by auto
obtain f where inj_f: "inj_on f {0..<k}" and fk_S: "f`{0..<k} = S"
and i_fi: " (∀i∈{0..<k}. i ≤ f i)" using exists_inj_ge_index[OF S Sk] by blast
have "(∏i = 0..<k. A $$ (i, i)) dvd (∏i∈{0..<k}. A $$ (f i,f i))"
by (rule prod_dvd_prod, rule SNF_divides_diagonal[OF A SNF_A], insert fk_S S i_fi, force+)
also have "... = (∏i∈f`{0..<k}. A $$ (i,i))"
by (rule prod.reindex[symmetric, unfolded o_def, OF inj_f])
also have "... = (∏i∈S. A $$ (i, i))" using fk_S by auto
finally have *: "(∏i = 0..<k. A $$ (i, i)) dvd (∏i∈S. A $$ (i, i))" .
show "(∏i = 0..<k. A $$ (i, i)) dvd b" using det_subS b * by auto
qed
qed
qed
lemma Gcd_minors_dvd_diagonal:
fixes A::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat n m"
and SNF_A: "Smith_normal_form_mat A"
and k: "k ≤ min n m"
shows "Gcd (minors A k) dvd (∏i=0..<k. A $$ (i,i))"
proof (rule Gcd_dvd)
define I where "I = {0..<k}"
have "(∏i = 0..<k. A $$ (i, i)) = det (submatrix A I I)"
proof -
have sub_eq: "submatrix A I I = mat k k (λ(i, j). A $$ (i, j))"
proof (rule eq_matI, auto)
have "I = {i. i < dim_row A ∧ i ∈ I}" unfolding I_def using A k by auto
hence ck: "card {i. i < dim_row A ∧ i ∈ I} = k"
unfolding I_def using card_atLeastLessThan by presburger
have "I = {i. i < dim_col A ∧ i ∈ I}" unfolding I_def using A k by auto
hence ck2: "card {j. j < dim_col A ∧ j ∈ I} = k"
unfolding I_def using card_atLeastLessThan by presburger
show dr: "dim_row (submatrix A I I) = k" using ck unfolding submatrix_def by auto
show dc: "dim_col (submatrix A I I) = k" using ck2 unfolding submatrix_def by auto
fix i j assume i: "i < k" and j: "j < k"
have p1: "pick I i = i"
proof -
have "{0..<i} = {a ∈ I. a < i}" using I_def i by auto
hence i_eq: "i = card {a ∈ I. a < i}"
by (metis card_atLeastLessThan diff_zero)
have "pick I i = pick I (card {a ∈ I. a < i})" using i_eq by simp
also have "... = i" by (rule pick_card_in_set, insert i I_def, simp)
finally show ?thesis .
qed
have p2: "pick I j = j"
proof -
have "{0..<j} = {a ∈ I. a < j}" using I_def j by auto
hence j_eq: "j = card {a ∈ I. a < j}"
by (metis card_atLeastLessThan diff_zero)
have "pick I j = pick I (card {a ∈ I. a < j})" using j_eq by simp
also have "... = j" by (rule pick_card_in_set, insert j I_def, simp)
finally show ?thesis .
qed
have "submatrix A I I $$ (i, j) = A $$ (pick I i, pick I j)"
proof (rule submatrix_index)
show "i < card {i. i < dim_row A ∧ i ∈ I}" by (metis dim_submatrix(1) dr i)
show "j < card {j. j < dim_col A ∧ j ∈ I}" by (metis dim_submatrix(2) dc j)
qed
also have "... = A $$ (i,j)" using p1 p2 by simp
finally show "submatrix A I I $$ (i, j) = A $$ (i, j)" .
qed
hence "det (submatrix A I I) = det (mat k k (λ(i, j). A $$ (i, j)))" by simp
also have "... = prod_list (diag_mat (mat k k (λ(i, j). A $$ (i, j))))"
proof (rule det_upper_triangular)
show "mat k k (λ(i, j). A $$ (i, j)) ∈ carrier_mat k k" by auto
show "upper_triangular (Matrix.mat k k (λ(i, j). A $$ (i, j)))"
using SNF_A A k unfolding Smith_normal_form_mat_def isDiagonal_mat_def by auto
qed
also have "... = (∏i = 0..<k. A $$ (i, i))"
by (metis (mono_tags, lifting) atLeastLessThan_iff dim_row_mat(1) index_mat(1)
prod.cong prod_list_diag_prod split_conv)
finally show ?thesis ..
qed
moreover have "I ⊆ {0..<dim_row A}" using k A I_def by auto
moreover have "I ⊆ {0..<dim_col A}" using k A I_def by auto
moreover have "card I = k" using I_def by auto
ultimately show "(∏i = 0..<k. A $$ (i, i)) ∈ minors A k" unfolding minors_def by auto
qed
lemma Gcd_minors_A_dvd_Gcd_minors_PAQ:
fixes A::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m" and Q: "Q ∈ carrier_mat n n"
shows "Gcd (minors A k) dvd Gcd (minors (P*A*Q) k)"
proof (rule Gcd_greatest)
let ?B="(P * A * Q)"
fix b assume "b ∈ minors ?B k"
from this obtain I J where b: "b = det (submatrix ?B I J)" and I: "I ⊆ {0..<dim_row ?B}"
and J: "J ⊆ {0..<dim_col ?B}" and Ik: "card I = k" and Jk: "card J = k"
unfolding minors_def by blast
have "Gcd (minors A k) dvd det (submatrix ?B I J)"
by (rule Gcd_minors_dvd[OF _ P A Q _ _ Ik Jk], insert A I J P Q, auto)
thus "Gcd (minors A k) dvd b" using b by simp
qed
lemma Gcd_minors_PAQ_dvd_Gcd_minors_A:
fixes A::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m"
and Q: "Q ∈ carrier_mat n n"
and inv_P: "invertible_mat P"
and inv_Q: "invertible_mat Q"
shows "Gcd (minors (P*A*Q) k) dvd Gcd (minors A k)"
proof (rule Gcd_greatest)
let ?B = "P * A * Q"
fix b assume "b ∈ minors A k"
from this obtain I J where b: "b = det (submatrix A I J)" and I: "I ⊆ {0..<dim_row A} "
and J: "J ⊆ {0..<dim_col A}" and Ik: "card I = k" and Jk: "card J = k"
unfolding minors_def by blast
obtain P' where PP': "inverts_mat P P'" and P'P: "inverts_mat P' P"
using inv_P unfolding invertible_mat_def by auto
obtain Q' where QQ': "inverts_mat Q Q'" and Q'Q: "inverts_mat Q' Q"
using inv_Q unfolding invertible_mat_def by auto
have P': "P' ∈ carrier_mat m m" using PP' P'P unfolding inverts_mat_def
by (metis P carrier_matD(1) carrier_matD(2) carrier_matI index_mult_mat(3) index_one_mat(3))
have Q': "Q' ∈ carrier_mat n n"
using QQ' Q'Q unfolding inverts_mat_def
by (metis Q carrier_matD(1) carrier_matD(2) carrier_matI index_mult_mat(3) index_one_mat(3))
have rw: "P' *?B *Q' = A"
proof -
have f1: "P' * P = 1⇩m m"
by (metis (no_types) P' P'P carrier_matD(1) inverts_mat_def)
have *: "P' * P * A = P' * (P * A)"
by (meson A P P' assoc_mult_mat)
have " P' * (P * A * Q) * Q' = P' * P * A * Q * Q'"
by (smt A P P' Q assoc_mult_mat mult_carrier_mat)
also have "... = P' * P * (A * Q * Q')"
using A P P' Q Q' f1 * by auto
also have "... = A * Q * Q'" using P'P A P' unfolding inverts_mat_def by auto
also have "... = A" using QQ' A Q' Q unfolding inverts_mat_def by auto
finally show ?thesis .
qed
have "Gcd (minors ?B k) dvd det (submatrix (P'*?B*Q') I J)"
by (rule Gcd_minors_dvd[OF _ P' _ Q' _ _ Ik Jk], insert P A Q I J, auto)
also have "... = det (submatrix A I J)" using rw by simp
finally show "Gcd (minors ?B k) dvd b" using b by simp
qed
lemma Gcd_minors_dvd_diag_PAQ:
fixes P A Q::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m"
and Q: "Q ∈ carrier_mat n n"
and SNF: "Smith_normal_form_mat (P*A*Q)"
and k: "k≤min m n"
shows "Gcd (minors A k) dvd (∏i=0..<k. (P * A * Q) $$ (i,i))"
proof -
have "Gcd (minors A k) dvd Gcd (minors (P * A * Q) k)"
by (rule Gcd_minors_A_dvd_Gcd_minors_PAQ[OF A P Q])
also have "... dvd (∏i=0..<k. (P*A*Q) $$ (i,i))"
by (rule Gcd_minors_dvd_diagonal[OF _ SNF k], insert P A Q, auto)
finally show ?thesis .
qed
lemma diag_PAQ_dvd_Gcd_minors:
fixes P A Q::"'a::{semiring_Gcd,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m"
and Q: "Q ∈ carrier_mat n n"
and inv_P: "invertible_mat P"
and inv_Q: "invertible_mat Q"
and SNF: "Smith_normal_form_mat (P*A*Q)"
shows "(∏i=0..<k. (P * A * Q) $$ (i,i)) dvd Gcd (minors A k)"
proof -
have "(∏i=0..<k. (P*A*Q) $$ (i,i)) dvd Gcd (minors (P * A * Q) k)"
by (rule diagonal_dvd_Gcd_minors[OF _ SNF], auto)
also have "... dvd Gcd (minors A k)"
by (rule Gcd_minors_PAQ_dvd_Gcd_minors_A[OF _ _ _ inv_P inv_Q], insert P A Q, auto)
finally show ?thesis .
qed
lemma Smith_prod_zero_imp_last_zero:
fixes A::"'a::{semidom,comm_ring_1} mat"
assumes A: "A ∈ carrier_mat m n"
and SNF: "Smith_normal_form_mat A"
and prod_0: "(∏j=0..<Suc i. A $$ (j,j)) = 0"
and i: "i<min m n"
shows "A $$(i,i) = 0"
proof -
obtain j where Ajj: "A$$(j,j) = 0" and j: "j<Suc i" using prod_0 prod_zero_iff by auto
show "A $$(i,i) = 0" by (rule Smith_zero_imp_zero[OF A SNF Ajj i], insert j, auto)
qed
subsection ‹Final theorem›
lemma Smith_normal_form_uniqueness_aux:
fixes P A Q::"'a::{idom,semiring_Gcd} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m"
and Q: "Q ∈ carrier_mat n n"
and inv_P: "invertible_mat P"
and inv_Q: "invertible_mat Q"
and PAQ_B: "P*A*Q = B"
and SNF: "Smith_normal_form_mat B"
and P': "P' ∈ carrier_mat m m"
and Q': "Q' ∈ carrier_mat n n"
and inv_P': "invertible_mat P'"
and inv_Q': "invertible_mat Q'"
and P'AQ'_B': "P'*A*Q' = B'"
and SNF_B': "Smith_normal_form_mat B'"
and k: "k<min m n"
shows "∀i≤k. B$$(i,i) dvd B'$$(i,i) ∧ B'$$(i,i) dvd B$$(i,i)"
proof (rule allI, rule impI)
fix i assume ik: "i ≤ k"
show " B $$ (i, i) dvd B' $$ (i, i) ∧ B' $$ (i, i) dvd B $$ (i, i)"
proof -
let ?ΠBi = "(∏i=0..<i. B $$ (i,i))"
let ?ΠB'i = "(∏i=0..<i. B' $$ (i,i))"
have "?ΠB'i dvd Gcd (minors A i)"
by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'],
insert P'AQ'_B' SNF_B' ik k, auto )
also have "... dvd ?ΠBi"
by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q],
insert PAQ_B SNF ik k, auto)
finally have B'_i_dvd_B_i: "?ΠB'i dvd ?ΠBi" .
have "?ΠBi dvd Gcd (minors A i)"
by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q],
insert PAQ_B SNF ik k, auto )
also have "... dvd ?ΠB'i"
by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'],
insert P'AQ'_B' SNF_B' ik k, auto)
finally have B_i_dvd_B'_i: "?ΠBi dvd ?ΠB'i" .
let ?ΠB_Suc = "(∏i=0..<Suc i. B $$ (i,i))"
let ?ΠB'_Suc = "(∏i=0..<Suc i. B' $$ (i,i))"
have "?ΠB'_Suc dvd Gcd (minors A (Suc i))"
by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'],
insert P'AQ'_B' SNF_B' ik k, auto )
also have "... dvd ?ΠB_Suc"
by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q],
insert PAQ_B SNF ik k, auto)
finally have 3: "?ΠB'_Suc dvd ?ΠB_Suc" .
have "?ΠB_Suc dvd Gcd (minors A (Suc i))"
by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q],
insert PAQ_B SNF ik k, auto )
also have "... dvd ?ΠB'_Suc"
by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'],
insert P'AQ'_B' SNF_B' ik k, auto)
finally have 4: "?ΠB_Suc dvd ?ΠB'_Suc" .
show ?thesis
proof (cases "?ΠB_Suc = 0")
case True
have True2: "?ΠB'_Suc = 0" using 4 True by fastforce
have "B$$(i,i) = 0"
by (rule Smith_prod_zero_imp_last_zero[OF _ SNF True], insert ik k PAQ_B P Q, auto)
moreover have "B'$$(i,i) = 0"
by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2],
insert ik k P'AQ'_B' P' Q', auto)
ultimately show ?thesis by auto
next
case False
have "∃u. u dvd 1 ∧ ?ΠB'i = u * ?ΠBi"
by (rule dvd_associated2[OF B'_i_dvd_B_i B_i_dvd_B'_i], insert False B'_i_dvd_B_i, force)
from this obtain u where eq1: "(∏i=0..<i. B' $$ (i,i)) = u * (∏i=0..<i. B $$ (i,i))"
and u_dvd_1: "u dvd 1" by blast
have "∃u. u dvd 1 ∧ ?ΠB_Suc = u * ?ΠB'_Suc"
by (rule dvd_associated2[OF 4 3 False])
from this obtain w where eq2: "(∏i=0..<Suc i. B $$ (i,i)) = w * (∏i=0..<Suc i. B' $$ (i,i))"
and w_dvd_1: "w dvd 1" by blast
have "B $$ (i, i) * (∏i=0..<i. B $$ (i,i)) = (∏i=0..<Suc i. B $$ (i,i))"
by (simp add: prod.atLeast0_lessThan_Suc ik)
also have "... = w * (∏i=0..<Suc i. B' $$ (i,i))" unfolding eq2 by auto
also have "... = w * (B' $$ (i,i) * (∏i=0..<i. B' $$ (i,i)))"
by (simp add: prod.atLeast0_lessThan_Suc ik)
also have "... = w * (B' $$ (i,i) * u * (∏i=0..<i. B $$ (i,i)))"
unfolding eq1 by auto
finally have "B $$ (i,i) = w * u * B' $$ (i,i)"
using False by auto
moreover have "w*u dvd 1" using u_dvd_1 w_dvd_1 by auto
ultimately have "∃u. is_unit u ∧ B $$ (i, i) = u * B' $$ (i, i)" by auto
thus ?thesis using dvd_associated2 by force
qed
qed
qed
lemma Smith_normal_form_uniqueness:
fixes P A Q::"'a::{idom,semiring_Gcd} mat"
assumes A: "A ∈ carrier_mat m n"
and P: "P ∈ carrier_mat m m"
and Q: "Q ∈ carrier_mat n n"
and inv_P: "invertible_mat P"
and inv_Q: "invertible_mat Q"
and PAQ_B: "P*A*Q = B"
and SNF: "Smith_normal_form_mat B"
and P': "P' ∈ carrier_mat m m"
and Q': "Q' ∈ carrier_mat n n"
and inv_P': "invertible_mat P'"
and inv_Q': "invertible_mat Q'"
and P'AQ'_B': "P'*A*Q' = B'"
and SNF_B': "Smith_normal_form_mat B'"
and i: "i < min m n"
shows "∃u. u dvd 1 ∧ B $$ (i,i) = u * B' $$ (i,i)"
proof (cases "B $$ (i,i) = 0")
case True
let ?ΠB_Suc = "(∏i=0..<Suc i. B $$ (i,i))"
let ?ΠB'_Suc = "(∏i=0..<Suc i. B' $$ (i,i))"
have "?ΠB_Suc dvd Gcd (minors A (Suc i))"
by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q],
insert PAQ_B SNF i, auto)
also have "... dvd ?ΠB'_Suc"
by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'],
insert P'AQ'_B' SNF_B' i, auto)
finally have 4: "?ΠB_Suc dvd ?ΠB'_Suc" .
have prod0: "?ΠB_Suc=0" using True by auto
have True2: "?ΠB'_Suc = 0" using 4 by (metis dvd_0_left_iff prod0)
have "B'$$(i,i) = 0"
by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2],
insert i P'AQ'_B' P' Q', auto)
thus ?thesis using True by auto
next
case False
have "∀a≤i. B$$(a,a) dvd B'$$(a,a) ∧ B'$$(a,a) dvd B$$(a,a)"
by (rule Smith_normal_form_uniqueness_aux[OF assms])
hence "B$$(i,i) dvd B'$$(i,i) ∧ B'$$(i,i) dvd B$$(i,i)" using i by auto
thus ?thesis using dvd_associated2 False by blast
qed
text ‹The final theorem, moved to HOL Analysis›
lemma Smith_normal_form_uniqueness_HOL_Analysis:
fixes A::"'a::{idom,semiring_Gcd}^'m::mod_type^'n::mod_type"
and P P'::"'a^'n::mod_type^'n::mod_type"
and Q Q'::"'a^'m::mod_type^'m::mod_type"
assumes
inv_P: "invertible P"
and inv_Q: "invertible Q"
and PAQ_B: "P**A**Q = B"
and SNF: "Smith_normal_form B"
and inv_P': "invertible P'"
and inv_Q': "invertible Q'"
and P'AQ'_B': "P'**A**Q' = B'"
and SNF_B': "Smith_normal_form B'"
and i: "i < min (nrows A) (ncols A)"
shows "∃u. u dvd 1 ∧ B $h Mod_Type.from_nat i $h Mod_Type.from_nat i
= u * B' $h Mod_Type.from_nat i $h Mod_Type.from_nat i"
proof -
let ?P = "Mod_Type_Connect.from_hma⇩m P"
let ?A = "Mod_Type_Connect.from_hma⇩m A"
let ?Q = "Mod_Type_Connect.from_hma⇩m Q"
let ?B = "Mod_Type_Connect.from_hma⇩m B"
let ?P' = "Mod_Type_Connect.from_hma⇩m P'"
let ?Q' = "Mod_Type_Connect.from_hma⇩m Q'"
let ?B' = "Mod_Type_Connect.from_hma⇩m B'"
let ?i = "(Mod_Type.from_nat i)::'n"
let ?i' = "(Mod_Type.from_nat i)::'m"
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?P P" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?A A" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?Q Q" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B B" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?P' P'" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?Q' Q'" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B' B'" by (simp add: Mod_Type_Connect.HMA_M_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I i ?i"
by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE
mod_type_class.to_nat_from_nat_id nrows_def)
have [transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'"
by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE
mod_type_class.to_nat_from_nat_id ncols_def)
have i2: "i < min CARD('m) CARD('n)" using i unfolding nrows_def ncols_def by auto
have "∃u. u dvd 1 ∧ ?B $$(i,i) = u * ?B' $$ (i,i)"
proof (rule Smith_normal_form_uniqueness[of _ "CARD('n)" "CARD('m)"])
show "?P*?A*?Q=?B" using PAQ_B by (transfer', auto)
show "Smith_normal_form_mat ?B" using SNF by (transfer', auto)
show "?P'*?A*?Q'=?B'" using P'AQ'_B' by (transfer', auto)
show "Smith_normal_form_mat ?B'" using SNF_B' by (transfer', auto)
show "invertible_mat ?P" using inv_P by (transfer, auto)
show "invertible_mat ?P'" using inv_P' by (transfer, auto)
show "invertible_mat ?Q" using inv_Q by (transfer, auto)
show "invertible_mat ?Q'" using inv_Q' by (transfer, auto)
qed (insert i2, auto)
hence "∃u. u dvd 1 ∧ (index_hma B ?i ?i') = u * (index_hma B' ?i ?i')" by (transfer', rule)
thus ?thesis unfolding index_hma_def by simp
qed
subsection ‹Uniqueness fixing a complete set of non-associates›
definition "Smith_normal_form_wrt A 𝒬 = (
(∀a b. Mod_Type.to_nat a = Mod_Type.to_nat b ∧ Mod_Type.to_nat a + 1 < nrows A
∧ Mod_Type.to_nat b + 1 < ncols A ⟶ A $h a $h b dvd A $h (a+1) $h (b+1))
∧ isDiagonal A ∧ Complete_set_non_associates 𝒬
∧ (∀a b. Mod_Type.to_nat a = Mod_Type.to_nat b ∧ Mod_Type.to_nat a < min (nrows A) (ncols A)
∧ Mod_Type.to_nat b < min (nrows A) (ncols A) ⟶ A $h a $h b ∈ 𝒬)
)"
lemma Smith_normal_form_wrt_uniqueness_HOL_Analysis:
fixes A::"'a::{idom,semiring_Gcd}^'m::mod_type^'n::mod_type"
and P P'::"'a^'n::mod_type^'n::mod_type"
and Q Q'::"'a^'m::mod_type^'m::mod_type"
assumes
P: "invertible P"
and Q: "invertible Q"
and PAQ_S: "P**A**Q = S"
and SNF: "Smith_normal_form_wrt S 𝒬"
and P': "invertible P'"
and Q': "invertible Q'"
and P'AQ'_S': "P'**A**Q' = S'"
and SNF_S': "Smith_normal_form_wrt S' 𝒬"
shows "S = S'"
proof -
have "S $h i $h j = S' $h i $h j" for i j
proof (cases "Mod_Type.to_nat i ≠ Mod_Type.to_nat j")
case True
then show ?thesis using SNF SNF_S' unfolding Smith_normal_form_wrt_def isDiagonal_def by auto
next
case False
let ?i = "Mod_Type.to_nat i"
let ?j = "Mod_Type.to_nat j"
have complete_set: "Complete_set_non_associates 𝒬"
using SNF_S' unfolding Smith_normal_form_wrt_def by simp
have ij: "?i = ?j" using False by auto
show ?thesis
proof (rule ccontr)
assume d: "S $h i $h j ≠ S' $h i $h j"
have n: "normalize (S $h i $h j) ≠ normalize (S' $h i $h j)"
proof (rule in_Ass_not_associated[OF complete_set _ _ d])
show "S $h i $h j ∈ 𝒬" using SNF unfolding Smith_normal_form_wrt_def
by (metis False min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def)
show "S' $h i $h j ∈ 𝒬" using SNF_S' unfolding Smith_normal_form_wrt_def
by (metis False min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def)
qed
have "∃u. u dvd 1 ∧ S $h i $h j = u * S' $h i $h j"
proof -
have "∃u. u dvd 1 ∧ S $h Mod_Type.from_nat ?i $h Mod_Type.from_nat ?i
= u * S' $h Mod_Type.from_nat ?i $h Mod_Type.from_nat ?i"
proof (rule Smith_normal_form_uniqueness_HOL_Analysis[OF P Q PAQ_S _ P' Q' P'AQ'_S' _])
show "Smith_normal_form S" and "Smith_normal_form S'"
using SNF SNF_S' Smith_normal_form_def Smith_normal_form_wrt_def by blast+
show "?i < min (nrows A) (ncols A)"
by (metis ij min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def)
qed
thus ?thesis using False by auto
qed
from this obtain u where "is_unit u" and "S $h i $h j = u * S' $h i $h j" by auto
thus False using n
by (simp add: normalize_1_iff normalize_mult)
qed
qed
thus ?thesis by vector
qed
end