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)

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 = (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

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 (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)

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))⇧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"
  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 ≤ 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

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 ≤ 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