Theory Jordan_Normal_Form.DL_Submatrix

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section ‹Submatrices›

theory DL_Submatrix
imports Matrix DL_Missing_Sublist
begin


section "Submatrix"

definition submatrix :: "'a mat  nat set  nat set  'a mat" where
"submatrix A I J = mat (card {i. i<dim_row A  iI}) (card {j. j<dim_col A  jJ}) (λ(i,j). A $$ (pick I i, pick J j))"

lemma dim_submatrix: "dim_row (submatrix A I J) = card {i. i<dim_row A  iI}"
                     "dim_col (submatrix A I J) = card {j. j<dim_col A  jJ}"
  unfolding submatrix_def by simp_all

lemma submatrix_index:
assumes "i<card {i. i<dim_row A  iI}"
assumes "j<card {j. j<dim_col A  jJ}"
shows "submatrix A I J $$ (i,j) = A $$ (pick I i, pick J j)"
  unfolding submatrix_def by (simp add: assms(1) assms(2))

lemma set_le_in:"{a. a < n  a  I} = {a  I. a < n}" by meson

lemma submatrix_index_card:
assumes "i<dim_row A" "j<dim_col A" "iI" "jJ"
shows "submatrix A I J $$ (card {aI. a < i}, card {aJ. a < j}) = A $$ (i, j)"
proof -
  have "i = pick I (card {aI. a < i})"
       "j = pick J (card {aJ. a < j})" using pick_card_in_set assms by auto
  have "{aI. a < i}  {i. i < dim_row A  i  I}"
       "{aJ. a < j}  {j. j < dim_col A  j  J}"
    unfolding set_le_in using i<dim_row A j<dim_col A Collect_mono less_imp_le less_le_trans iI jJ by auto
  then have "card {aI. a < i} < card {i. i < dim_row A  i  I}"
            "card {aJ. a < j} < card {j. j < dim_col A  j  J}" by (simp_all add: psubset_card_mono)
  then show ?thesis
    using i = pick I (card {a  I. a < i}) j = pick J (card {a  J. a < j}) submatrix_index by fastforce
qed

lemma submatrix_split: "submatrix A I J = submatrix (submatrix A UNIV J) I UNIV"
proof (rule eq_matI)
  show "dim_row (submatrix A I J) = dim_row (submatrix (submatrix A UNIV J) I UNIV)"
    by (simp add: dim_submatrix(1))
  show "dim_col (submatrix A I J) = dim_col (submatrix (submatrix A UNIV J) I UNIV)"
    by (simp add: dim_submatrix(2))
  fix i j assume ij_le:"i < dim_row (submatrix (submatrix A UNIV J) I UNIV)" "j < dim_col (submatrix (submatrix A UNIV J) I UNIV)"
  then have ij_le1:"i<card {i. i < dim_row A  i  I}" "j<card {i. i < dim_col A  i  J}"
    by (simp_all add: dim_submatrix)
  then have ij_le2:"i<card {i. i < dim_row (submatrix A UNIV J)  i  I}" "j<card {i. i < dim_col (submatrix A UNIV J)  i  UNIV}"
    by (simp_all add: dim_submatrix)
  then have i_le3:"pick I i<card {i. i < dim_row A  i  UNIV}"
    using ij_le1(1) pick_le by auto
  have j_le3: "pick UNIV j<card {i. i < dim_col A  i  J}" unfolding pick_UNIV by (simp add: ij_le1(2))
  then show "submatrix A I J $$ (i, j) = submatrix (submatrix A UNIV J) I UNIV $$ (i, j)"
    unfolding submatrix_index[OF ij_le1] submatrix_index[OF ij_le2] submatrix_index[OF i_le3 j_le3]
    unfolding pick_UNIV by metis
qed

end