# 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  0m nr nc *v x = 0v 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

(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]:
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 = (AT @r BT)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]:
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 (0v n) m = 0v 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]:
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]:  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)

lemma add_diff_eq_vec: fixes y :: "'a :: group_add vec"
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]:
unfolding mat_of_col_def by auto

lemma mat_of_col_dim[simp]:
"dim_col (mat_of_col 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))TT"
by auto
also have "((A @c B) * mat_of_col (v1 @v v2))T =
(mat_of_row (v1 @v v2))TT * (AT @r BT)TT"
unfolding append_cols_def mat_of_col_def
proof (rule transpose_mult, force, unfold transpose_carrier_mat, rule mat_of_row_carrier)
have "AT  carrier_mat nc1 nr" using A by auto
moreover have "BT  carrier_mat nc2 nr" using B by auto
ultimately have "AT @r BT  carrier_mat (nc1 + nc2) nr" by auto
hence "dim_row (AT @r BT) = nc1 + nc2" by auto
thus "v1 @v v2  carrier_vec (dim_row (AT @r BT))" using v1 v2 by auto
qed
also have " = (mat_of_row (v1 @v v2)) * (AT @r BT)" by auto
also have " = mat_of_row v1 * AT + mat_of_row v2 * BT"
using mat_of_row_mult_append_rows[OF v1 v2] A B by auto
also have "T = (mat_of_row v1 * AT)T + (mat_of_row v2 * BT)T"
using transpose_add A B by auto
also have "(mat_of_row v1 * AT)T = ATT * ((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 * BT)T = BTT * ((mat_of_row v2)T)"
using transpose_mult B v2 transpose_carrier_mat mat_of_row_carrier(1)
by metis
also have "ATT * ((mat_of_row v1)T) + BTT * ((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  0v (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
unfolding append_rows_def using assms by fastforce
show
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 AT n)T"

definition "mat_col_last A n  (mat_row_last AT 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 "AT"] 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"

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
by (auto simp add: scalar_prod_def)

lemma smult_pos_vec[simp]: fixes l :: "'a :: linordered_ring_strict"
assumes l: "l > 0"
shows "(l v v  0v n) = (v  0v 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

lemma vec_add_mono: fixes a ::
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  0v n"
shows "l v v  0v 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 "  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 "x1carrier_vec n. x2carrier_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