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)

lemma add_diff_cancel_right_vec:
  "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 = (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]: "elements_mat (AT) = 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

lemma vec_first_add:
  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]: "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]: "setv 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)

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]: "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))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 "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 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"
  "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"
  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 :: "'a :: ordered_ab_semigroup_add vec"
  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 "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 "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