# Theory Missing_Matrix

```section ‹Missing Lemmas on Vectors and Matrices›

text ‹We provide some results on vector spaces which should be merged into Jordan-Normal-Form/Matrix.›
theory Missing_Matrix
imports Jordan_Normal_Form.Matrix
begin

lemma orthogonalD': assumes "orthogonal vs"
and "v ∈ set vs" and "w ∈ set vs"
shows "(v ∙ w = 0) = (v ≠ w)"
proof -
from assms(2) obtain i where v: "v = vs ! i" and i: "i < length vs" by (auto simp: set_conv_nth)
from assms(3) obtain j where w: "w = vs ! j" and j: "j < length vs" by (auto simp: set_conv_nth)
from orthogonalD[OF assms(1) i j, folded v w] orthogonalD[OF assms(1) i i, folded v v]
show ?thesis using v w by auto
qed

lemma zero_mat_mult_vector[simp]: "x ∈ carrier_vec nc ⟹ 0⇩m nr nc *⇩v x = 0⇩v nr"
by (intro eq_vecI, auto)

"a ∈ carrier_vec n ⟹ (b :: 'a :: cancel_ab_semigroup_add vec) ∈ carrier_vec n ⟹
(a + b) - b = a"
by (intro eq_vecI, auto)

lemma elements_four_block_mat_id:
assumes c: "A ∈ carrier_mat nr1 nc1" "B ∈ carrier_mat nr1 nc2"
"C ∈ carrier_mat nr2 nc1" "D ∈ carrier_mat nr2 nc2"
shows
"elements_mat (four_block_mat A B C D) =
elements_mat A ∪ elements_mat B ∪ elements_mat C ∪ elements_mat D"
(is "elements_mat ?four = ?X")
proof
show "elements_mat ?four ⊆ ?X"
by (rule elements_four_block_mat[OF c])
have 4: "?four ∈ carrier_mat (nr1 + nr2) (nc1 + nc2)" using c by auto
{
fix x
assume "x ∈ ?X"
then consider (A) "x ∈ elements_mat A"
| (B) "x ∈ elements_mat B"
| (C) "x ∈ elements_mat C"
| (D) "x ∈ elements_mat D" by auto
hence "x ∈ elements_mat ?four"
proof (cases)
case A
from elements_matD[OF this] obtain i j
where *: "i < nr1" "j < nc1" and x: "x = A \$\$ (i,j)"
using c by auto
from elements_matI[OF 4, of i j x] * c
show ?thesis unfolding x by auto
next
case B
from elements_matD[OF this] obtain i j
where *: "i < nr1" "j < nc2" and x: "x = B \$\$ (i,j)"
using c by auto
from elements_matI[OF 4, of i "nc1 + j" x] * c
show ?thesis unfolding x by auto
next
case C
from elements_matD[OF this] obtain i j
where *: "i < nr2" "j < nc1" and x: "x = C \$\$ (i,j)"
using c by auto
from elements_matI[OF 4, of "nr1 + i" j x] * c
show ?thesis unfolding x by auto
next
case D
from elements_matD[OF this] obtain i j
where *: "i < nr2" "j < nc2" and x: "x = D \$\$ (i,j)"
using c by auto
from elements_matI[OF 4, of "nr1 + i" "nc1 + j" x] * c
show ?thesis unfolding x by auto
qed
}
thus "elements_mat ?four ⊇ ?X" by blast
qed

lemma elements_mat_append_rows: "A ∈ carrier_mat nr n ⟹ B ∈ carrier_mat nr2 n ⟹
elements_mat (A @⇩r B) = elements_mat A ∪ elements_mat B"
unfolding append_rows_def
by (subst elements_four_block_mat_id, auto)

lemma elements_mat_uminus[simp]: "elements_mat (-A) = uminus ` elements_mat A"
unfolding elements_mat_def by auto

lemma vec_set_uminus[simp]: "vec_set (-A) = uminus ` vec_set A"
unfolding vec_set_def by auto

definition append_cols :: "'a :: zero mat ⇒ 'a mat ⇒ 'a mat"  (infixr "@⇩c" 65) where
"A @⇩c B = (A⇧T @⇩r B⇧T)⇧T"

lemma carrier_append_cols[simp, intro]:
"A ∈ carrier_mat nr nc1 ⟹
B ∈ carrier_mat nr nc2 ⟹ (A @⇩c B) ∈ carrier_mat nr (nc1 + nc2)"
unfolding append_cols_def by auto

lemma elements_mat_transpose_mat[simp]: "elements_mat (A⇧T) = elements_mat A"
unfolding elements_mat_def by auto

lemma elements_mat_append_cols: "A ∈ carrier_mat n nc ⟹ B ∈ carrier_mat n nc1
⟹ elements_mat (A @⇩c B) = elements_mat A ∪ elements_mat B"
unfolding append_cols_def elements_mat_transpose_mat
by (subst elements_mat_append_rows, auto)

lemma vec_first_index:
assumes v: "dim_vec v ≥ n"
and i: "i < n"
shows "(vec_first v n) \$ i = v \$ i"
unfolding vec_first_def using assms by simp

lemma vec_last_index:
assumes v: "v ∈ carrier_vec (n + m)"
and i: "i < m"
shows "(vec_last v m) \$ i = v \$ (n + i)"
unfolding vec_last_def using assms by simp

assumes "dim_vec x ≥ n"
and "dim_vec y ≥ n"
shows"vec_first (x + y) n = vec_first x n + vec_first y n"
unfolding vec_first_def using assms by auto

lemma vec_first_zero[simp]: "m ≤ n ⟹ vec_first (0⇩v n) m = 0⇩v m"
unfolding vec_first_def by auto

lemma vec_first_smult:
"⟦ m ≤ n; x ∈ carrier_vec n ⟧ ⟹ vec_first (c ⋅⇩v x) m = c ⋅⇩v vec_first x m"
unfolding vec_first_def by auto

lemma elements_mat_mat_of_row[simp]: "elements_mat (mat_of_row v) = vec_set v"
by (auto simp: mat_of_row_def elements_mat_def vec_set_def)

lemma vec_set_append_vec[simp]: "vec_set (v @⇩v w) = vec_set v ∪ vec_set w"
by (metis list_of_vec_append set_append set_list_of_vec)

lemma vec_set_vNil[simp]: "set⇩v vNil = {}" using set_list_of_vec by force

lemma diff_smult_distrib_vec: "((x :: 'a::ring) - y) ⋅⇩v v = x ⋅⇩v v - y ⋅⇩v v"
unfolding smult_vec_def minus_vec_def
by (rule eq_vecI, auto simp: left_diff_distrib)

shows "y ∈ carrier_vec n ⟹ x ∈ carrier_vec n ⟹ z ∈ carrier_vec n ⟹ y + (x - z) = y + x - z"
by (intro eq_vecI, auto simp: add_diff_eq)

definition "mat_of_col v = (mat_of_row v)⇧T"

lemma elements_mat_mat_of_col[simp]: "elements_mat (mat_of_col v) = vec_set v"
unfolding mat_of_col_def by auto

lemma mat_of_col_dim[simp]: "dim_row (mat_of_col v) = dim_vec v"
"dim_col (mat_of_col v) = 1"
"mat_of_col v ∈ carrier_mat (dim_vec v) 1"
unfolding mat_of_col_def by auto

lemma col_mat_of_col[simp]: "col (mat_of_col v) 0 = v"
unfolding mat_of_col_def by auto

lemma mult_mat_of_col: "A ∈ carrier_mat nr nc ⟹ v ∈ carrier_vec nc ⟹
A * mat_of_col v = mat_of_col (A *⇩v v)"
by (intro mat_col_eqI, auto)

lemma mat_mult_append_cols: fixes A :: "'a :: comm_semiring_0 mat"
assumes A: "A ∈ carrier_mat nr nc1"
and B: "B ∈ carrier_mat nr nc2"
and v1: "v1 ∈ carrier_vec nc1"
and v2: "v2 ∈ carrier_vec nc2"
shows "(A @⇩c B) *⇩v (v1 @⇩v v2) = A *⇩v v1 + B *⇩v v2"
proof -
have "(A @⇩c B) *⇩v (v1 @⇩v v2) = (A @⇩c B) *⇩v col (mat_of_col (v1 @⇩v v2)) 0" by auto
also have "… = col ((A @⇩c B) * mat_of_col (v1 @⇩v v2)) 0" by auto
also have "(A @⇩c B) * mat_of_col (v1 @⇩v v2) = ((A @⇩c B) * mat_of_col (v1 @⇩v v2))⇧T⇧T"
by auto
also have "((A @⇩c B) * mat_of_col (v1 @⇩v v2))⇧T =
(mat_of_row (v1 @⇩v v2))⇧T⇧T * (A⇧T @⇩r B⇧T)⇧T⇧T"
unfolding append_cols_def mat_of_col_def
proof (rule transpose_mult, force, unfold transpose_carrier_mat, rule mat_of_row_carrier)
have "A⇧T ∈ carrier_mat nc1 nr" using A by auto
moreover have "B⇧T ∈ carrier_mat nc2 nr" using B by auto
ultimately have "A⇧T @⇩r B⇧T ∈ carrier_mat (nc1 + nc2) nr" by auto
hence "dim_row (A⇧T @⇩r B⇧T) = nc1 + nc2" by auto
thus "v1 @⇩v v2 ∈ carrier_vec (dim_row (A⇧T @⇩r B⇧T))" using v1 v2 by auto
qed
also have "… = (mat_of_row (v1 @⇩v v2)) * (A⇧T @⇩r B⇧T)" by auto
also have "… = mat_of_row v1 * A⇧T + mat_of_row v2 * B⇧T"
using mat_of_row_mult_append_rows[OF v1 v2] A B by auto
also have "…⇧T = (mat_of_row v1 * A⇧T)⇧T + (mat_of_row v2 * B⇧T)⇧T"
using transpose_add A B by auto
also have "(mat_of_row v1 * A⇧T)⇧T = A⇧T⇧T * ((mat_of_row v1)⇧T)"
using transpose_mult A v1 transpose_carrier_mat mat_of_row_carrier(1)
by metis
also have "(mat_of_row v2 * B⇧T)⇧T = B⇧T⇧T * ((mat_of_row v2)⇧T)"
using transpose_mult B v2 transpose_carrier_mat mat_of_row_carrier(1)
by metis
also have "A⇧T⇧T * ((mat_of_row v1)⇧T) + B⇧T⇧T * ((mat_of_row v2)⇧T) =
A * mat_of_col v1 + B * mat_of_col v2"
unfolding mat_of_col_def by auto
also have "col … 0 = col (A * mat_of_col v1) 0 + col (B * mat_of_col v2) 0"
using assms by auto
also have "… = col (mat_of_col (A *⇩v v1)) 0 + col (mat_of_col (B *⇩v v2)) 0"
using mult_mat_of_col assms by auto
also have "… = A *⇩v v1 + B *⇩v v2" by auto
finally show ?thesis by auto
qed

lemma vec_first_append:
assumes "v ∈ carrier_vec n"
shows "vec_first (v @⇩v w) n = v"
proof -
have "v @⇩v w = vec_first (v @⇩v w) n @⇩v vec_last (v @⇩v w) (dim_vec w)"
using vec_first_last_append assms by simp
thus ?thesis using append_vec_eq[OF assms] by simp
qed

lemma vec_le_iff_diff_le_0: fixes a :: "'a :: ordered_ab_group_add vec"
shows "(a ≤ b) = (a - b ≤ 0⇩v (dim_vec a))"
unfolding less_eq_vec_def by auto

definition "mat_row_first A n ≡ mat n (dim_col A) (λ (i, j). A \$\$ (i, j))"

definition "mat_row_last A n ≡ mat n (dim_col A) (λ (i, j). A \$\$ (dim_row A - n + i, j))"

lemma mat_row_first_carrier[simp]: "mat_row_first A n ∈ carrier_mat n (dim_col A)"
unfolding mat_row_first_def by simp

lemma mat_row_first_dim[simp]:
"dim_row (mat_row_first A n) = n"
"dim_col (mat_row_first A n) = dim_col A"
unfolding mat_row_first_def by simp_all

lemma mat_row_last_carrier[simp]: "mat_row_last A n ∈ carrier_mat n (dim_col A)"
unfolding mat_row_last_def by simp

lemma mat_row_last_dim[simp]:
"dim_row (mat_row_last A n) = n"
"dim_col (mat_row_last A n) = dim_col A"
unfolding mat_row_last_def by simp_all

lemma mat_row_first_nth[simp]: "i < n ⟹ row (mat_row_first A n) i = row A i"
unfolding mat_row_first_def row_def by fastforce

lemma append_rows_nth:
assumes "A ∈ carrier_mat nr1 nc"
and "B ∈ carrier_mat nr2 nc"
shows "i < nr1 ⟹ row (A @⇩r B) i = row A i"
and "⟦ i ≥ nr1; i < nr1 + nr2 ⟧ ⟹ row (A @⇩r B) i = row B (i - nr1)"
unfolding append_rows_def using row_four_block_mat assms by auto

lemma mat_of_row_last_nth[simp]:
"i < n ⟹ row (mat_row_last A n) i = row A (dim_row A - n + i)"
unfolding mat_row_last_def row_def by auto

lemma mat_row_first_last_append:
assumes "dim_row A = m + n"
shows "(mat_row_first A m) @⇩r (mat_row_last A n) = A"
proof (rule eq_rowI)
show "dim_row (mat_row_first A m @⇩r mat_row_last A n) = dim_row A"
unfolding append_rows_def using assms by fastforce
show "dim_col (mat_row_first A m @⇩r mat_row_last A n) = dim_col A"
unfolding append_rows_def by fastforce
fix i
assume i: "i < dim_row A"
show "row (mat_row_first A m @⇩r mat_row_last A n) i = row A i"
proof cases
assume i: "i < m"
thus ?thesis using append_rows_nth(1)[OF mat_row_first_carrier[of A m]
mat_row_last_carrier[of A n] i] by simp
next
assume i': "¬ i < m"
thus ?thesis using append_rows_nth(2)[OF mat_row_first_carrier[of A m]
mat_row_last_carrier[of A n]] i assms by simp
qed
qed

definition "mat_col_first A n ≡ (mat_row_first A⇧T n)⇧T"

definition "mat_col_last A n ≡ (mat_row_last A⇧T n)⇧T"

lemma mat_col_first_carrier[simp]: "mat_col_first A n ∈ carrier_mat (dim_row A) n"
unfolding mat_col_first_def by fastforce

lemma mat_col_first_dim[simp]:
"dim_row (mat_col_first A n) = dim_row A"
"dim_col (mat_col_first A n) = n"
unfolding mat_col_first_def by simp_all

lemma mat_col_last_carrier[simp]: "mat_col_last A n ∈ carrier_mat (dim_row A) n"
unfolding mat_col_last_def by fastforce

lemma mat_col_last_dim[simp]:
"dim_row (mat_col_last A n) = dim_row A"
"dim_col (mat_col_last A n) = n"
unfolding mat_col_last_def by simp_all

lemma mat_col_first_nth[simp]:
"⟦ i < n; i < dim_col A ⟧ ⟹ col (mat_col_first A n) i = col A i"
unfolding mat_col_first_def by force

lemma append_cols_nth:
assumes "A ∈ carrier_mat nr nc1"
and "B ∈ carrier_mat nr nc2"
shows "i < nc1 ⟹ col (A @⇩c B) i = col A i"
and "⟦ i ≥ nc1; i < nc1 + nc2 ⟧ ⟹ col (A @⇩c B) i = col B (i - nc1)"
unfolding append_cols_def append_rows_def using row_four_block_mat assms
by auto

lemma mat_of_col_last_nth[simp]:
"⟦ i < n; i < dim_col A ⟧ ⟹ col (mat_col_last A n) i = col A (dim_col A - n + i)"
unfolding mat_col_last_def by auto

lemma mat_col_first_last_append:
assumes "dim_col A = m + n"
shows "(mat_col_first A m) @⇩c (mat_col_last A n) = A"
unfolding append_cols_def mat_col_first_def mat_col_last_def
using mat_row_first_last_append[of "A⇧T"] assms by simp

lemma mat_of_row_dim_row_1: "(dim_row A = 1) = (A = mat_of_row (row A 0))"
proof
show "dim_row A = 1 ⟹ A = mat_of_row (row A 0)" by force
show "A = mat_of_row (row A 0) ⟹ dim_row A = 1" using mat_of_row_dim(1) by metis
qed

lemma mat_of_col_dim_col_1: "(dim_col A = 1) = (A = mat_of_col (col A 0))"
proof
show "dim_col A = 1 ⟹ A = mat_of_col (col A 0)"
unfolding mat_of_col_def by auto
show "A = mat_of_col (col A 0) ⟹ dim_col A = 1" by (metis mat_of_col_dim(2))
qed

definition vec_of_scal :: "'a ⇒ 'a vec" where "vec_of_scal x ≡ vec 1 (λ i. x)"

lemma vec_of_scal_dim[simp]:
"dim_vec (vec_of_scal x) = 1"
"vec_of_scal x ∈ carrier_vec 1"
unfolding vec_of_scal_def by auto

lemma index_vec_of_scal[simp]: "(vec_of_scal x) \$ 0 = x"
unfolding vec_of_scal_def by auto

lemma row_mat_of_col[simp]: "i < dim_vec v ⟹ row (mat_of_col v) i = vec_of_scal (v \$ i)"
unfolding mat_of_col_def by auto

lemma vec_of_scal_dim_1: "(v ∈ carrier_vec 1) = (v = vec_of_scal (v \$ 0))"
by(standard, auto simp del: One_nat_def, metis vec_of_scal_dim(2))

lemma mult_mat_of_row_vec_of_scal: fixes x :: "'a :: comm_ring_1"
shows "mat_of_col v *⇩v vec_of_scal x = x ⋅⇩v v"

lemma smult_pos_vec[simp]: fixes l :: "'a :: linordered_ring_strict"
assumes l: "l > 0"
shows "(l ⋅⇩v v ≤ 0⇩v n) = (v ≤ 0⇩v n)"
proof (cases "dim_vec v = n")
case True
have "i < n ⟹ ((l ⋅⇩v v) \$ i ≤ 0) ⟷ v \$ i ≤ 0" for i using True
mult_le_cancel_left_pos[OF l, of _ 0] by simp
thus ?thesis using True unfolding less_eq_vec_def by auto
qed (auto simp: less_eq_vec_def)

lemma finite_elements_mat[simp]: "finite (elements_mat A)"
unfolding elements_mat_def by (rule finite_set)

lemma finite_vec_set[simp]: "finite (vec_set A)"
unfolding vec_set_def by auto

lemma lesseq_vecI: assumes "v ∈ carrier_vec n" "w ∈ carrier_vec n"
"⋀ i. i < n ⟹ v \$ i ≤ w \$ i"
shows "v ≤ w"
using assms unfolding less_eq_vec_def by auto

lemma lesseq_vecD: assumes "w ∈ carrier_vec n"
and "v ≤ w"
and "i < n"
shows "v \$ i ≤ w \$ i"
using assms unfolding less_eq_vec_def by auto

assumes dim: "dim_vec b = dim_vec d"
and ab: "a ≤ b"
and cd: "c ≤ d"
shows "a + c ≤ b + d"
proof -
have "⋀ i. i < dim_vec d ⟹ (a + c) \$ i ≤ (b + d) \$ i"
proof -
fix i
assume id: "i < dim_vec d"
have ic: "i < dim_vec c" using id cd unfolding less_eq_vec_def by auto
have ib: "i < dim_vec b" using id dim by auto
have ia: "i < dim_vec a" using ib ab unfolding less_eq_vec_def by auto
have "a \$ i ≤ b \$ i" using ab ia ib unfolding less_eq_vec_def by auto
moreover have "c \$ i ≤ d \$ i" using cd ic id unfolding less_eq_vec_def by auto
ultimately have abcdi: "a \$ i + c \$ i ≤ b \$ i + d \$ i" using add_mono by auto
have "(a + c) \$ i = a \$ i + c \$ i" using index_add_vec(1) ic by auto
also have "… ≤ b \$ i + d \$ i" using abcdi by auto
also have "b \$ i + d \$ i = (b + d) \$ i" using index_add_vec(1) id by auto
finally show "(a + c) \$ i ≤ (b + d) \$ i" by auto
qed
then show "a + c ≤ b + d" unfolding less_eq_vec_def
using dim index_add_vec(2) cd less_eq_vec_def by auto
qed

lemma smult_nneg_npos_vec: fixes l :: "'a :: ordered_semiring_0"
assumes l: "l ≥ 0"
and v: "v ≤ 0⇩v n"
shows "l ⋅⇩v v ≤ 0⇩v n"
proof -
{
fix i
assume i: "i < n"
then have vi: "v \$ i ≤ 0" using v unfolding less_eq_vec_def by simp
then have "(l ⋅⇩v v) \$ i = l * v \$ i" using v i unfolding less_eq_vec_def by auto
also have "l * v \$ i ≤ 0" by (rule mult_nonneg_nonpos[OF l vi])
finally have "(l ⋅⇩v v) \$ i ≤ 0" by auto
}
then show ?thesis using v unfolding less_eq_vec_def by auto
qed

lemma smult_vec_nonneg_eq: fixes c :: "'a :: field"
shows "c ≠ 0 ⟹ (c ⋅⇩v x = c ⋅⇩v y) = (x = y)"
proof -
have "c ≠ 0 ⟹ c ⋅⇩v x = c ⋅⇩v y ⟹ x = y"
by (metis smult_smult_assoc[of "1 / c" "c"] nonzero_divide_eq_eq one_smult_vec)
thus "c ≠ 0 ⟹ ?thesis" by auto
qed

lemma distinct_smult_nonneg: fixes c :: "'a :: field"
assumes c: "c ≠ 0"
shows "distinct lC ⟹ distinct (map ((⋅⇩v) c) lC)"
proof (induction lC)
case (Cons v lC)
from Cons.prems have "v ∉ set lC" by fastforce
hence "c ⋅⇩v v ∉ set (map ((⋅⇩v) c) lC)" using smult_vec_nonneg_eq[OF c] by fastforce
moreover have "map ((⋅⇩v) c) (v # lC) = c ⋅⇩v v # map ((⋅⇩v) c) lC" by simp
ultimately show ?case using Cons.IH Cons.prems by simp
qed auto

lemma exists_vec_append: "(∃ x ∈ carrier_vec (n + m). P x) ⟷ (∃ x1 ∈ carrier_vec n. ∃ x2 ∈ carrier_vec m. P (x1 @⇩v x2))"
proof
assume "∃x ∈ carrier_vec (n + m). P x"
from this obtain x where xcarr: "x ∈ carrier_vec (n+m)" and Px: "P x" by auto
have "x = vec n (λ i. x \$ i) @⇩v vec m (λ i. x \$ (n + i))"
by (rule eq_vecI, insert xcarr, auto)
hence "P x = P (vec n (λ i. x \$ i) @⇩v vec m (λ i. x \$ (n + i)))" by simp
also have 1: "…" using xcarr Px calculation by blast
finally show "∃x1∈carrier_vec n. ∃x2∈carrier_vec m. P (x1 @⇩v x2)" using 1 vec_carrier by blast
next
assume "(∃ x1 ∈ carrier_vec n. ∃ x2 ∈ carrier_vec m. P (x1 @⇩v x2))"
from this obtain x1 x2 where x1: "x1 ∈ carrier_vec n"
and x2: "x2 ∈ carrier_vec m" and P12: "P (x1 @⇩v x2)" by auto
define x where "x = x1 @⇩v x2"
have xcarr: "x ∈ carrier_vec (n+m)" using x1 x2 by (simp add: x_def)
have "P x" using P12 xcarr using x_def by blast
then show "(∃ x ∈ carrier_vec (n + m). P x)" using xcarr by auto
qed

end```