Theory SNF_Missing_Lemmas

(*
  Author: Jose Divasón
  Email:  jose.divason@unirioja.es
*)

section ‹Missing results›

theory SNF_Missing_Lemmas
  imports
    Hermite.Hermite
    Mod_Type_Connect
    Jordan_Normal_Form.DL_Rank_Submatrix
    "List-Index.List_Index"
begin

text ‹This theory presents some missing lemmas that are required for the Smith normal form
development. Some of them could be added to different AFP entries, such as the Jordan Normal
Form AFP entry by Ren\'e Thiemann and Akihisa Yamada.

However, not all the lemmas can be added directly, since some imports are required.›

hide_const (open) C
hide_const (open) measure

subsection ‹Miscellaneous lemmas›

lemma sum_two_rw: "(i = 0..<2. f i) = (i  {0,1::nat}. f i)"
  by (rule sum.cong, auto)

lemma sum_common_left:
  fixes f::"'a  'b::comm_ring_1"
  assumes "finite A"
  shows "sum (λi. c * f i) A = c * sum f A"
  by (simp add: mult_hom.hom_sum)

lemma prod3_intro:
  assumes "fst A = a" and "fst (snd A) = b" and "snd (snd A) = c"
  shows "A = (a,b,c)" using assms by auto


subsection ‹Transfer rules for the HMA\_Connect file of the Perron-Frobenius development›

hide_const (open) HMA_M HMA_I to_hmam from_hmam
hide_fact (open) from_hmam_def from_hma_to_hmam HMA_M_def HMA_I_def dim_row_transfer_rule
                  dim_col_transfer_rule

context
  includes lifting_syntax
begin

lemma HMA_invertible_matrix[transfer_rule]:
  "((HMA_Connect.HMA_M :: _  'a :: comm_ring_1 ^ 'n ^ 'n  _) ===> (=)) invertible_mat invertible"
proof (intro rel_funI, goal_cases)
  case (1 x y)
  note rel_xy[transfer_rule] = "1"
  have eq_dim: "dim_col x = dim_row x"
    using HMA_Connect.dim_col_transfer_rule HMA_Connect.dim_row_transfer_rule rel_xy
    by fastforce
  moreover have "A'. y ** A' = Finite_Cartesian_Product.mat 1  A' ** y = Finite_Cartesian_Product.mat 1"
    if xB: "x * B = 1m (dim_row x)" and Bx: "B * x = 1m (dim_row B)" for B
  proof -
    let ?A' = "HMA_Connect.to_hmam B:: 'a :: comm_ring_1 ^ 'n ^ 'n"
    have rel_BA[transfer_rule]: "HMA_M B ?A'"
      by (metis (no_types, lifting) Bx HMA_M_def eq_dim carrier_mat_triv dim_col_mat(1)
          from_hmam_def from_hma_to_hmam index_mult_mat(3) index_one_mat(3) rel_xy xB)
    have [simp]: "dim_row B = CARD('n)" using dim_row_transfer_rule rel_BA by blast
    have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast
    have "y ** ?A' = Finite_Cartesian_Product.mat 1" using xB by (transfer, simp)
    moreover have "?A' ** y  = Finite_Cartesian_Product.mat 1" using Bx by (transfer, simp)
    ultimately show ?thesis by blast
  qed
  moreover have "B. x * B = 1m (dim_row x)  B * x = 1m (dim_row B)"
    if yA: "y ** A' = Finite_Cartesian_Product.mat 1" and Ay: "A' ** y = Finite_Cartesian_Product.mat 1" for A'
  proof -
    let ?B = "(from_hmam A')"
    have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast
    have [transfer_rule]: "HMA_M ?B A'" by (simp add: HMA_M_def)
    hence [simp]: "dim_row ?B = CARD('n)" using dim_row_transfer_rule by auto
    have "x * ?B = 1m (dim_row x)" using yA by (transfer', auto)
    moreover have "?B * x = 1m (dim_row ?B)" using Ay by (transfer', auto)
    ultimately show ?thesis by auto
  qed
  ultimately show ?case unfolding invertible_mat_def invertible_def inverts_mat_def by auto
qed
end

subsection ‹Lemmas obtained from HOL Analysis using local type definitions›

thm Cartesian_Space.invertible_mult (*In HOL Analysis*)
thm invertible_iff_is_unit (*In HOL Analysis*)
thm det_non_zero_imp_unit (*In JNF, but only for fields*)
thm mat_mult_left_right_inverse (*In JNF, but only for fields*)

lemma invertible_mat_zero:
  assumes A: "A  carrier_mat 0 0"
  shows "invertible_mat A"
  using A unfolding invertible_mat_def inverts_mat_def one_mat_def times_mat_def scalar_prod_def
    Matrix.row_def col_def carrier_mat_def
  by (auto, metis (no_types, lifting) cong_mat not_less_zero)

lemma invertible_mult_JNF:
  fixes A::"'a::comm_ring_1 mat"
  assumes A: "Acarrier_mat n n" and B: "Bcarrier_mat n n"
    and inv_A: "invertible_mat A" and inv_B: "invertible_mat B"
shows "invertible_mat (A*B)"
proof (cases "n = 0")
  case True
  then show ?thesis using assms
    by (simp add: invertible_mat_zero)
next
  case False
  then show ?thesis using
      invertible_mult[where ?'a="'a::comm_ring_1", where ?'b="'n::finite", where ?'c="'n::finite",
      where ?'d="'n::finite", untransferred, cancel_card_constraint, OF assms] by auto
qed

lemma invertible_iff_is_unit_JNF:
  assumes A: "A  carrier_mat n n"
  shows "invertible_mat A  (Determinant.det A) dvd 1"
proof (cases "n=0")
  case True
  then show ?thesis using det_dim_zero invertible_mat_zero A by auto
next
  case False
  then show ?thesis using invertible_iff_is_unit[untransferred, cancel_card_constraint] A by auto
qed


subsection ‹Lemmas about matrices, submatrices and determinants›

(*This is a generalization of thm mat_mult_left_right_inverse*)
thm mat_mult_left_right_inverse
lemma mat_mult_left_right_inverse:
  fixes A :: "'a::comm_ring_1 mat"
  assumes A: "A  carrier_mat n n"
    and B: "B  carrier_mat n n" and AB: "A * B = 1m n"
  shows "B * A = 1m n"
proof -
  have "Determinant.det (A * B) = Determinant.det (1m n)" using AB by auto
  hence "Determinant.det A * Determinant.det B = 1"
    using Determinant.det_mult[OF A B] det_one by auto
  hence det_A: "(Determinant.det A) dvd 1" and det_B: "(Determinant.det B) dvd 1"
    using dvd_triv_left dvd_triv_right by metis+
  hence inv_A: "invertible_mat A" and inv_B: "invertible_mat B"
    using A B invertible_iff_is_unit_JNF by blast+
  obtain B' where inv_BB': "inverts_mat B B'" and inv_B'B: "inverts_mat B' B"
    using inv_B unfolding invertible_mat_def by auto
  have B'_carrier: "B'  carrier_mat n n"
    by (metis B inv_B'B inv_BB' carrier_matD(1) carrier_matD(2) carrier_mat_triv
        index_mult_mat(3) index_one_mat(3) inverts_mat_def)
  have "B * A * B = B" using A AB B by auto
  hence "B * A * (B * B') = B * B'"
    by (smt (verit, best) A B B'_carrier assoc_mult_mat mult_carrier_mat)
  thus ?thesis
    by (metis A B carrier_matD(1) carrier_matD(2) index_mult_mat(3) inv_BB'
        inverts_mat_def right_mult_one_mat')
qed

context comm_ring_1
begin

lemma col_submatrix_UNIV:
assumes "j < card {i. i < dim_col A  i  J}"
shows "col (submatrix A UNIV J) j = col A (pick J j)"
proof (rule eq_vecI)
  show dim_eq:"dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))"
    by (simp add: dim_submatrix(1))
  fix i assume "i < dim_vec (col A (pick J j))"
  show "col (submatrix A UNIV J) j $v i = col A (pick J j) $v i"
    by (smt (verit) Collect_cong assms col_def dim_col dim_eq dim_submatrix(1)
        eq_vecI index_vec pick_UNIV submatrix_index)
qed

lemma submatrix_split2: "submatrix A I J = submatrix (submatrix A I UNIV) UNIV J" (is "?lhs = ?rhs")
proof (rule eq_matI)
  show dr: "dim_row ?lhs = dim_row ?rhs"
    by (simp add: dim_submatrix(1))
  show dc: "dim_col ?lhs = dim_col ?rhs"
    by (simp add: dim_submatrix(2))
  fix i j assume i: "i < dim_row ?rhs"
    and j: "j < dim_col ?rhs"
  have "?rhs $$ (i, j) = (submatrix A I UNIV) $$ (pick UNIV i, pick J j)"
  proof (rule submatrix_index)
    show "i < card {i. i < dim_row (submatrix A I UNIV)  i  UNIV}"
      by (metis (full_types) dim_submatrix(1) i)
    show "j < card {j. j < dim_col (submatrix A I UNIV)  j  J}"
      by (metis (full_types) dim_submatrix(2) j)
  qed
  also have "... = A $$ (pick I (pick UNIV i), pick UNIV (pick J j))"
  proof (rule submatrix_index)
    show "pick UNIV i < card {i. i < dim_row A  i  I}"
      by (metis (full_types) dr dim_submatrix(1) i pick_UNIV)
    show "pick J j < card {j. j < dim_col A  j  UNIV}"
      by (metis (full_types) dim_submatrix(2) j pick_le)
  qed
  also have "... = ?lhs $$ (i,j)"
  proof (unfold pick_UNIV, rule submatrix_index[symmetric])
    show "i < card {i. i < dim_row A  i  I}"
      by (metis (full_types) dim_submatrix(1) dr i)
    show "j < card {j. j < dim_col A  j  J}"
      by (metis (full_types) dim_submatrix(2) dc j)
  qed
  finally show "?lhs $$ (i, j) = ?rhs $$ (i, j)" ..
qed

lemma submatrix_mult:
  "submatrix (A*B) I J = submatrix A I UNIV * submatrix B UNIV J" (is "?lhs = ?rhs")
proof (rule eq_matI)
  show "dim_row ?lhs = dim_row ?rhs" unfolding submatrix_def by auto
  show "dim_col ?lhs = dim_col ?rhs" unfolding submatrix_def by auto
  fix i j assume i: "i < dim_row ?rhs" and j: "j < dim_col ?rhs"
  have i1: "i < card {i. i < dim_row (A * B)  i  I}"
    by (metis (full_types) dim_submatrix(1) i index_mult_mat(2))
  have j1: "j < card {j. j < dim_col (A * B)  j  J}"
    by (metis dim_submatrix(2) index_mult_mat(3) j)
  have pi: "pick I i < dim_row A" using i1 pick_le by auto
  have pj: "pick J j < dim_col B" using j1 pick_le by auto
  have row_rw: "Matrix.row (submatrix A I UNIV) i = Matrix.row A (pick I i)"
    using i1 row_submatrix_UNIV by auto
  have col_rw: "col (submatrix B UNIV J) j = col B (pick J j)" using j1 col_submatrix_UNIV by auto
  have "?lhs $$ (i,j) =  (A*B) $$ (pick I i, pick J j)" by (rule submatrix_index[OF i1 j1])
  also have "... = Matrix.row A (pick I i)  col B (pick J j)" by (rule index_mult_mat(1)[OF pi pj])
  also have "... = Matrix.row (submatrix A I UNIV) i  col (submatrix B UNIV J) j"
    using row_rw col_rw by simp
  also have "... = (?rhs) $$ (i,j)" by (rule index_mult_mat[symmetric], insert i j, auto)
  finally show "?lhs $$ (i, j) = ?rhs $$ (i, j)" .
qed

lemma det_singleton:
  assumes A: "A  carrier_mat 1 1"
  shows "det A = A $$ (0,0)"
  using A unfolding carrier_mat_def Determinant.det_def by auto

lemma submatrix_singleton_index:
  assumes A: "A  carrier_mat n m"
    and an: "a < n" and bm: "b < m"
    shows "submatrix A {a} {b} $$ (0,0) = A $$ (a,b)"
proof -
  have a: "{i. i = a  i < dim_row A} = {a}" using an A unfolding carrier_mat_def by auto
  have b: "{i. i = b  i < dim_col A} = {b}" using bm A unfolding carrier_mat_def by auto
  have "submatrix A {a} {b} $$ (0,0) = A $$ (pick {a} 0,pick {b} 0)"
    by (rule submatrix_index, insert a b, auto)
  moreover have "pick {a} 0 = a" by (auto, metis (full_types) LeastI)
  moreover have "pick {b} 0 = b" by (auto, metis (full_types) LeastI)
  ultimately show ?thesis by simp
qed
end

lemma det_not_inj_on:
  assumes not_inj_on: "¬ inj_on f {0..<n}"
  shows "det (matr n n (λi. Matrix.row B (f i))) = 0"
proof -
  obtain i j where i: "i<n" and j: "j<n" and fi_fj: "f i = f j" and ij: "ij"
    using not_inj_on unfolding inj_on_def by auto
  show ?thesis
  proof (rule det_identical_rows[OF _ ij i j])
    let ?B="(matr n n (λi. row B (f i)))"
    show "row ?B i = row ?B j"
    proof (rule eq_vecI, auto)
      fix ia assume ia: "ia < n"
      have "row ?B i $ ia = ?B $$ (i, ia)" by (rule index_row(1), insert i ia, auto)
      also have "... = ?B $$ (j, ia)" by (simp add: fi_fj i ia j)
      also have "... = row ?B j $ ia" by (rule index_row(1)[symmetric], insert j ia, auto)
      finally show "row ?B i $ ia = row (matr n n (λi. row B (f i))) j $ ia" by simp
    qed
    show "matr n n (λi. Matrix.row B (f i))  carrier_mat n n" by auto
  qed
qed



lemma mat_row_transpose: "(matr nr nc f)T = mat nc nr (λ(i,j). vec_index (f j) i)"
  by (rule eq_matI, auto)


lemma obtain_inverse_matrix:
  assumes A: "A  carrier_mat n n" and i: "invertible_mat A"
  obtains B where "inverts_mat A B" and "inverts_mat B A" and "B  carrier_mat n n"
proof -
  have "(B. inverts_mat A B  inverts_mat B A)" using i unfolding invertible_mat_def by auto
  from this obtain B where AB: "inverts_mat A B" and BA: "inverts_mat B A" by auto
  moreover have "B  carrier_mat n n" using A AB BA unfolding carrier_mat_def inverts_mat_def
    by (auto, metis index_mult_mat(3) index_one_mat(3))+
  ultimately show ?thesis using that by blast
qed


lemma invertible_mat_smult_mat:
  fixes A :: "'a::comm_ring_1 mat"
  assumes inv_A: "invertible_mat A" and k: "k dvd 1"
  shows "invertible_mat (k m A)"
proof -
  obtain n where A: "A  carrier_mat n n" using inv_A unfolding invertible_mat_def by auto
  have det_dvd_1: "Determinant.det A dvd 1" using inv_A invertible_iff_is_unit_JNF[OF A] by auto
  have "Determinant.det (k m A) = k ^ dim_col A * Determinant.det A" by simp
  also have "... dvd 1" by (rule unit_prod, insert k det_dvd_1 dvd_power_same, force+)
  finally show ?thesis using invertible_iff_is_unit_JNF by (metis A smult_carrier_mat)
qed

lemma invertible_mat_one[simp]: "invertible_mat (1m n)"
  unfolding invertible_mat_def using inverts_mat_def by fastforce

lemma four_block_mat_dim0:
  assumes A: "A  carrier_mat n n"
  and B: "B  carrier_mat n 0"
  and C: "C  carrier_mat 0 n"
  and D: "D  carrier_mat 0 0"
shows "four_block_mat A B C D = A"
  unfolding four_block_mat_def using assms by auto


lemma det_four_block_mat_lower_right_id:
  assumes A: "A  carrier_mat m m"
and B: "B = 0m m (n-m)"
and C: "C = 0m (n-m) m"
and D: "D = 1m (n-m)"
and "n>m"
shows "Determinant.det (four_block_mat A B C D) = Determinant.det A"
  using assms
proof (induct n arbitrary: A B C D)
  case 0
  then show ?case by auto
next
  case (Suc n)
  let ?block = "(four_block_mat A B C D)"
  let ?B = "Matrix.mat m (n-m) (λ(i,j). 0)"
  let ?C = "Matrix.mat (n-m) m (λ(i,j). 0)"
  let ?D = "1m (n-m)"
  have mat_eq: "(mat_delete ?block n n) = four_block_mat A ?B ?C ?D" (is "?lhs = ?rhs")
  proof (rule eq_matI)
    fix i j assume i: "i < dim_row (four_block_mat A ?B ?C ?D)"
      and j: "j < dim_col (four_block_mat A ?B ?C ?D)"
    let ?f = " (if i < dim_row A then if j < dim_col A then A $$ (i, j) else B $$ (i, j - dim_col A)
     else if j < dim_col A then C $$ (i - dim_row A, j) else D $$ (i - dim_row A, j - dim_col A))"
    let ?g = "(if i < dim_row A then if j < dim_col A then A $$ (i, j) else ?B $$ (i, j - dim_col A)
     else if j < dim_col A then ?C $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))"
    have "(mat_delete ?block n n) $$ (i,j) = ?block $$ (i,j)"
      using i j Suc.prems unfolding mat_delete_def by auto
    also have "... = ?f"
      by (rule index_mat_four_block, insert Suc.prems i j, auto)
    also have "... = ?g" using i j Suc.prems by auto
    also have "... = four_block_mat A ?B ?C ?D $$ (i,j)"
      by (rule index_mat_four_block[symmetric], insert Suc.prems i j, auto)
    finally show "?lhs $$ (i,j) = ?rhs $$ (i,j)" .
  qed (insert Suc.prems, auto)
  have nn_1: "?block $$ (n, n) = 1" using Suc.prems by auto
  have rw0: "(i<n. ?block $$ (i,n) * Determinant.cofactor ?block i n) = 0"
  proof (rule sum.neutral, rule)
    fix x assume x: "x  {..<n}"
    have block_index: "?block $$ (x,n) = (if x < dim_row A then if n < dim_col A then A $$ (x, n)
      else B $$ (x, n - dim_col A) else if n < dim_col A then C $$ (x - dim_row A, n)
      else D $$ (x - dim_row A, n - dim_col A))"
      by (rule index_mat_four_block, insert Suc.prems x, auto)
    have "four_block_mat A B C D $$ (x,n) = 0" using x Suc.prems by auto
    thus "four_block_mat A B C D $$ (x, n) * Determinant.cofactor (four_block_mat A B C D) x n = 0"
      by simp
  qed
  have "Determinant.det ?block = (i<Suc n. ?block $$ (i, n) * Determinant.cofactor ?block i n)"
    by (rule laplace_expansion_column, insert Suc.prems, auto)
  also have "... = ?block $$ (n, n) * Determinant.cofactor ?block n n
    + (i<n. ?block $$ (i,n) * Determinant.cofactor ?block i n)"
    by simp
  also have "... = ?block $$ (n, n) * Determinant.cofactor ?block n n" using rw0 by auto
  also have "... = Determinant.cofactor ?block n n" using nn_1 by simp
  also have "... = Determinant.det (mat_delete ?block n n)" unfolding cofactor_def by auto
  also have "... = Determinant.det (four_block_mat A ?B ?C ?D)" using mat_eq by simp
  also have "... = Determinant.det A" (is "Determinant.det ?lhs = Determinant.det ?rhs")
  proof (cases "n = m")
    case True
    have "?lhs = ?rhs" by (rule four_block_mat_dim0, insert Suc.prems True, auto)
    then show ?thesis by simp
  next
    case False
    show ?thesis by (rule Suc.hyps, insert Suc.prems False, auto)
  qed
  finally show ?case .
qed


lemma mult_eq_first_row:
  assumes A: "A  carrier_mat 1 n"
  and B: "B  carrier_mat m n"
  and m0: "m  0"
  and r: "Matrix.row A 0 = Matrix.row B 0"
shows "Matrix.row (A * V) 0 = Matrix.row (B * V) 0"
proof (rule eq_vecI)
  show "dim_vec (Matrix.row (A * V) 0) = dim_vec (Matrix.row (B * V) 0)" using A B r by auto
  fix i assume i: "i < dim_vec (Matrix.row (B * V) 0)"
  have "Matrix.row (A * V) 0 $v i = (A * V) $$ (0,i)" by (rule index_row, insert i A, auto)
  also have "... = Matrix.row A 0  col V i" by (rule index_mult_mat, insert A i, auto)
  also have "... = Matrix.row B 0  col V i" using r by auto
  also have "... = (B * V) $$ (0,i)" by (rule index_mult_mat[symmetric], insert m0 B i, auto)
  also have "... = Matrix.row (B * V) 0 $v i" by (rule index_row[symmetric], insert i B m0, auto)
  finally show "Matrix.row (A * V) 0 $v i = Matrix.row (B * V) 0 $v i" .
qed


lemma smult_mat_mat_one_element:
  assumes A: "A  carrier_mat 1 1" and B: "B  carrier_mat 1 n"
  shows "A * B = A $$ (0,0) m B"
proof (rule eq_matI)
  fix i j assume i: "i < dim_row (A $$ (0, 0) m B)" and j: "j < dim_col (A $$ (0, 0) m B)"
  have i0: "i = 0" using A B i by auto
  have "(A * B) $$ (i, j) =  Matrix.row A i  col B j"
    by (rule index_mult_mat, insert i j A B, auto)
  also have "... =  Matrix.row A i $v 0 * col B j $v 0" unfolding scalar_prod_def using B by auto
  also have "... = A$$(i,i) * B$$(i,j)" using A i i0 j by auto
  also have "... = (A $$ (i, i) m B) $$ (i, j)"
    unfolding i by (rule index_smult_mat[symmetric], insert i j B, auto)
  finally show "(A * B) $$ (i, j) = (A $$ (0, 0) m B) $$ (i, j)" using i0 by simp
qed (insert A B, auto)

lemma determinant_one_element:
  assumes A: "A  carrier_mat 1 1" shows "Determinant.det A = A $$ (0,0)"
proof -
  have "Determinant.det A = prod_list (diag_mat A)"
    by (rule det_upper_triangular[OF _ A], insert A, unfold upper_triangular_def, auto)
  also have "... = A $$ (0,0)" using A unfolding diag_mat_def by auto
  finally show ?thesis .
qed



lemma invertible_mat_transpose:
  assumes inv_A: "invertible_mat (A::'a::comm_ring_1 mat)"
  shows "invertible_mat AT"
proof -
  obtain n where A: "A  carrier_mat n n"
    using inv_A unfolding invertible_mat_def square_mat.simps by auto
  hence At: "AT  carrier_mat n n" by simp
  have "Determinant.det AT = Determinant.det A"
    by (metis Determinant.det_def Determinant.det_transpose carrier_matI
        index_transpose_mat(2) index_transpose_mat(3))
  also have "... dvd 1" using invertible_iff_is_unit_JNF[OF A] inv_A by simp
  finally show ?thesis  using invertible_iff_is_unit_JNF[OF At] by auto
qed

lemma dvd_elements_mult_matrix_left:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and P: "P  carrier_mat m m"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
  shows "(i j. i<m  j<n  x dvd (P*A)$$(i,j))"
proof -
  have "x dvd (P * A) $$ (i, j)" if i: "i < m" and j: "j < n" for i j
  proof -
    have "(P * A) $$ (i, j) =  (ia = 0..<m. Matrix.row P i $v ia * col A j $v ia)"
      unfolding times_mat_def scalar_prod_def using A P j i by auto
    also have "... = (ia = 0..<m. Matrix.row P i $v ia *  A $$ (ia,j))"
      by (rule sum.cong, insert A j, auto)
    also have "x dvd ..." using x by (meson atLeastLessThan_iff dvd_mult dvd_sum j)
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed


lemma dvd_elements_mult_matrix_right:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and Q: "Q  carrier_mat n n"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
  shows "(i j. i<m  j<n  x dvd (A*Q)$$(i,j))"
proof -
  have "x dvd (A*Q) $$ (i, j)" if i: "i < m" and j: "j < n" for i j
  proof -
    have "(A*Q) $$ (i, j) =  (ia = 0..<n. Matrix.row A i $v ia * col Q j $v ia)"
      unfolding times_mat_def scalar_prod_def using A Q j i by auto
    also have "... = (ia = 0..<n. A $$ (i, ia) * col Q j $v ia)"
      by (rule sum.cong, insert A Q i, auto)
    also have "x dvd ..." using x
      by (meson atLeastLessThan_iff dvd_mult2 dvd_sum i)
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed


lemma dvd_elements_mult_matrix_left_right:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m n"
  and P: "P  carrier_mat m m"
  and Q: "Q  carrier_mat n n"
  and x: "(i j. i<m  j<n  x dvd A$$(i,j))"
shows "(i j. i<m  j<n  x dvd (P*A*Q)$$(i,j))"
  using dvd_elements_mult_matrix_left[OF A P x]
  by (meson P A Q dvd_elements_mult_matrix_right mult_carrier_mat)


definition append_cols :: "'a :: zero mat  'a mat  'a mat" (infixr "@c" 65)where
  "A @c B = four_block_mat A B (0m 0 (dim_col A)) (0m 0 (dim_col B))"

lemma append_cols_carrier[simp,intro]:
  "A  carrier_mat n a  B  carrier_mat n b  (A @c B)  carrier_mat n (a+b)"
  unfolding append_cols_def by auto

lemma append_cols_mult_left:
  assumes A: "A  carrier_mat n a"
  and B: "B  carrier_mat n b"
  and P: "P  carrier_mat n n"
shows "P * (A @c B) = (P*A) @c (P*B)"
proof -
  let ?P = "four_block_mat P (0m n 0) (0m 0 n) (0m 0 0)"
  have "P = ?P" by (rule eq_matI, auto)
  hence "P * (A @c B) = ?P * (A @c B)" by simp
  also have "?P * (A @c B) = four_block_mat (P * A + 0m n 0 * 0m 0 (dim_col A))
  (P * B + 0m n 0 * 0m 0 (dim_col B)) (0m 0 n * A + 0m 0 0 * 0m 0 (dim_col A))
  (0m 0 n * B + 0m 0 0 * 0m 0 (dim_col B))" unfolding append_cols_def
    by (rule mult_four_block_mat, insert A B P, auto)
  also have "... = four_block_mat (P * A) (P * B) (0m 0 (dim_col (P*A))) (0m 0 (dim_col (P*B)))"
    by (rule cong_four_block_mat, insert P, auto)
  also have "... = (P*A) @c (P*B)" unfolding append_cols_def by auto
  finally show ?thesis .
qed

lemma append_cols_mult_right_id:
  assumes A: "(A::'a::semiring_1 mat)  carrier_mat n 1"
  and B: "B  carrier_mat n (m-1)"
  and C: "C = four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) D"
  and D: "D  carrier_mat (m-1) (m-1)"
shows "(A @c B) * C = A @c (B * D)"
proof -
  let ?C = "four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) D"
  have "(A @c B) * C = (A @c B) * ?C" unfolding C by auto
  also have "... = four_block_mat A B (0m 0 (dim_col A)) (0m 0 (dim_col B)) * ?C"
    unfolding append_cols_def by auto
  also have "... = four_block_mat (A * 1m 1 + B * 0m (m - 1) 1) (A * 0m 1 (m - 1) + B * D)
    (0m 0 (dim_col A) * 1m 1 + 0m 0 (dim_col B) * 0m (m - 1) 1)
    (0m 0 (dim_col A) * 0m 1 (m - 1) + 0m 0 (dim_col B) * D)"
    by (rule mult_four_block_mat, insert assms, auto)
  also have "... = four_block_mat A (B * D) (0m 0 (dim_col A)) (0m 0 (dim_col (B*D)))"
    by (rule cong_four_block_mat, insert assms, auto)
  also have "... = A @c (B * D)" unfolding append_cols_def by auto
  finally show ?thesis .
qed


lemma append_cols_mult_right_id2:
 assumes A: "(A::'a::semiring_1 mat)  carrier_mat n a"
   and B: "B  carrier_mat n b"
   and C: "C = four_block_mat D (0m a b) (0m b a) (1m b)"
   and D: "D  carrier_mat a a"
shows "(A @c B) * C = (A * D) @c B"
proof -
  let ?C = "four_block_mat D (0m a b) (0m b a) (1m b)"
  have "(A @c B) * C = (A @c B) * ?C" unfolding C by auto
  also have "... = four_block_mat A B (0m 0 a) (0m 0 b) * ?C"
    unfolding append_cols_def using A B by auto
  also have "... = four_block_mat (A * D + B * 0m b a) (A * 0m a b + B * 1m b)
    (0m 0 a * D + 0m 0 b * 0m b a) (0m 0 a * 0m a b + 0m 0 b * 1m b)"
    by (rule mult_four_block_mat, insert A B C D, auto)
  also have "... = four_block_mat (A * D) B (0m 0 (dim_col (A*D))) (0m 0 (dim_col B))"
    by (rule cong_four_block_mat, insert assms, auto)
  also have "... = (A * D) @c B" unfolding append_cols_def by auto
  finally show ?thesis .
qed


lemma append_cols_nth:
  assumes A: "A  carrier_mat n a"
  and B: "B  carrier_mat n b"
  and i: "i<n" and j: "j < a + b"
shows "(A @c B) $$ (i, j) = (if j < dim_col A then A $$(i,j) else B$$(i,j-a))" (is "?lhs = ?rhs")
proof -
  let ?C = "(0m 0 (dim_col A))"
  let ?D = "(0m 0 (dim_col B))"
  have i2: "i < dim_row A + dim_row ?D" using i A by auto
  have j2: "j < dim_col A + dim_col (0m 0 (dim_col B))" using j B A by auto
  have "(A @c B) $$ (i, j) = four_block_mat A B ?C ?D $$ (i, j)"
    unfolding append_cols_def by auto
  also have "... = (if i < dim_row A then if j < dim_col A then A $$ (i, j)
  else B $$ (i, j - dim_col A) else if j < dim_col A then ?C $$ (i - dim_row A, j)
  else 0m 0 (dim_col B) $$ (i - dim_row A, j - dim_col A))"
    by (rule index_mat_four_block(1)[OF i2 j2])
  also have "... = ?rhs" using i A by auto
  finally show ?thesis .
qed

lemma append_cols_split:
  assumes d: "dim_col A > 0"
  shows "A = mat_of_cols (dim_row A) [col A 0] @c
             mat_of_cols (dim_row A) (map (col A) [1..<dim_col A])" (is "?lhs = ?A1 @c ?A2")
proof (rule eq_matI)
  fix i j assume i: "i < dim_row (?A1 @c ?A2)" and j: "j < dim_col (?A1 @c ?A2)"
  have "(?A1 @c ?A2) $$ (i, j) = (if j < dim_col ?A1 then ?A1 $$(i,j) else ?A2$$(i,j-(dim_col ?A1)))"
    by (rule append_cols_nth, insert i j, auto simp add: append_cols_def)
  also have "... = A $$ (i,j)"
  proof (cases "j< dim_col ?A1")
    case True
    then show ?thesis
      by (metis One_nat_def Suc_eq_plus1 add.right_neutral append_cols_def col_def i
          index_mat_four_block(2) index_vec index_zero_mat(2) less_one list.size(3) list.size(4)
          mat_of_cols_Cons_index_0 mat_of_cols_carrier(2) mat_of_cols_carrier(3))
  next
    case False
    then show ?thesis
      by (metis (no_types, lifting) Suc_eq_plus1 Suc_less_eq Suc_pred add_diff_cancel_right' append_cols_def
          diff_zero i index_col index_mat_four_block(2) index_mat_four_block(3) index_zero_mat(2)
          index_zero_mat(3) j length_map length_upt linordered_semidom_class.add_diff_inverse list.size(3)
          list.size(4) mat_of_cols_carrier(2) mat_of_cols_carrier(3) mat_of_cols_index nth_map_upt
          plus_1_eq_Suc upt_0)
  qed
  finally show "A $$ (i, j) = (?A1 @c ?A2) $$ (i, j)" ..
qed (auto simp add: append_cols_def d)


lemma append_rows_nth:
  assumes A: "A  carrier_mat a n"
  and B: "B  carrier_mat b n"
  and i: "i<a+b" and j: "j < n"
shows "(A @r B) $$ (i, j) = (if i < dim_row A then A $$(i,j) else B$$(i-a,j))" (is "?lhs = ?rhs")
proof -
  let ?C = "(0m (dim_row A) 0)"
  let ?D = "(0m (dim_row B) 0)"
  have i2: "i < dim_row A + dim_row ?D" using i j A B by auto
  have j2: "j < dim_col A + dim_col ?D" using i j A B by auto
  have "(A @r B) $$ (i, j) = four_block_mat A ?C B ?D $$ (i, j)"
    unfolding append_rows_def by auto
  also have "... =  (if i < dim_row A then if j < dim_col A then A $$ (i, j) else ?C $$ (i, j - dim_col A)
   else if j < dim_col A then B $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))"
    by (rule index_mat_four_block(1)[OF i2 j2])
  also have "... = ?rhs" using i A j B by auto
  finally show ?thesis .
qed

lemma append_rows_split:
  assumes k: "kdim_row A"
  shows "A = (mat_of_rows (dim_col A) [Matrix.row A i. i  [0..<k]]) @r
             (mat_of_rows (dim_col A) [Matrix.row A i. i  [k..<dim_row A]])" (is "?lhs = ?A1 @r ?A2")
proof (rule eq_matI)
  have "(?A1 @r ?A2)  carrier_mat (k + (dim_row A-k)) (dim_col A)"
    by (rule carrier_append_rows, insert k, auto)
  hence A1_A2: "(?A1 @r ?A2)  carrier_mat (dim_row A) (dim_col A)" using k by simp
  thus "dim_row A = dim_row (?A1 @r ?A2)" and "dim_col A = dim_col (?A1 @r ?A2)" by auto
  fix i j assume i: "i < dim_row (?A1 @r ?A2)" and j: "j < dim_col (?A1 @r ?A2)"
  have "(?A1 @r ?A2) $$ (i, j) = (if i < dim_row ?A1 then ?A1 $$(i,j) else ?A2$$(i-(dim_row ?A1),j))"
    by (rule append_rows_nth, insert k i j, auto simp add: append_rows_def)
  also have "... = A $$ (i,j)"
  proof (cases "i<dim_row ?A1")
    case True
    then show ?thesis
      by (metis (no_types, lifting) Matrix.row_def add.left_neutral add.right_neutral append_rows_def
          index_mat(1) index_mat_four_block(3) index_vec index_zero_mat(3) j length_map length_upt
          mat_of_rows_carrier(2,3) mat_of_rows_def nth_map_upt prod.simps(2))
  next
    case False
    let ?xs = "(map (Matrix.row A) [k..<dim_row A])"
    have dim_row_A1: "dim_row ?A1 = k" by auto
    have "?A2 $$ (i-k,j) = ?xs ! (i-k) $v j"
      by (rule mat_of_rows_index, insert i k False A1_A2 j, auto)
    also have "... = A $$ (i,j)" using A1_A2 False i j by auto
    finally show ?thesis using A1_A2 False i j by auto
  qed
  finally show " A $$ (i, j) = (?A1 @r ?A2) $$ (i,j)" by simp
qed



lemma transpose_mat_append_rows:
 assumes A: "A  carrier_mat a n" and B: "B  carrier_mat b n"
 shows "(A @r B)T = AT @c BT"
proof -
  have "(four_block_mat A (0m a n) B (0m b n))T = four_block_mat AT BT (0m a n)T (0m b n)T" for n
    by (meson assms(1) assms(2) transpose_four_block_mat zero_carrier_mat)
  then show ?thesis
    by (metis Matrix.transpose_transpose append_cols_def append_rows_def assms(1) assms(2)
        carrier_matD(2) index_transpose_mat(2) transpose_carrier_mat zero_transpose_mat)
qed

lemma transpose_mat_append_cols:
 assumes A: "A  carrier_mat n a" and B: "B  carrier_mat n b"
 shows "(A @c B)T = AT @r BT"
  by (smt (verit, ccfv_threshold) Matrix.transpose_transpose assms(1) assms(2)
      transpose_carrier_mat transpose_mat_append_rows)

lemma append_rows_mult_right:
  assumes A: "(A::'a::comm_semiring_1 mat)  carrier_mat a n" and B: "B  carrier_mat b n"
    and Q: "Q carrier_mat n n"
  shows "(A @r B) * Q = (A * Q) @r (B*Q)"
proof -
  have "transpose_mat ((A @r B) * Q) = QT * (A @r B)T"
    by (rule transpose_mult, insert A B Q, auto)
  also have "... = QT * (AT @c BT)" using transpose_mat_append_rows assms by metis
  also have "... = QT * AT @c QT * BT"
    using append_cols_mult_left assms by (metis transpose_carrier_mat)
  also have "transpose_mat ... = (A * Q) @r (B*Q)"
    by (smt (verit, ccfv_threshold) A B Matrix.transpose_mult Matrix.transpose_transpose
        append_cols_def append_rows_def assms(3) carrier_matD(1) index_mult_mat(2)
        index_transpose_mat(3) mult_carrier_mat transpose_four_block_mat zero_carrier_mat
        zero_transpose_mat)
  finally show ?thesis by simp
qed

lemma append_rows_mult_left_id:
  assumes A: "(A::'a::comm_semiring_1 mat)  carrier_mat 1 n"
    and B: "B  carrier_mat (m-1) n"
    and C: "C = four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) D"
    and D: "D  carrier_mat (m-1) (m-1)"
  shows "C * (A @r B) = A @r (D * B)"
proof -
  have "transpose_mat (C * (A @r B)) = (A @r B)T * CT"
    by (metis (no_types, lifting) B C D Matrix.transpose_mult append_rows_def A carrier_matD
        carrier_mat_triv index_mat_four_block(2,3) index_zero_mat(2) one_carrier_mat)
  also have "... = (AT @c BT) * CT" using transpose_mat_append_rows[OF A B] by auto
  also have "... = AT @c (BT * DT)" by (rule append_cols_mult_right_id) (use A B C D in auto)
  also have "transpose_mat ... = A @r (D * B)" using A
    by (metis (no_types, opaque_lifting)
        Matrix.transpose_mult Matrix.transpose_transpose assms(2) assms(4)
        mult_carrier_mat transpose_mat_append_rows)
  finally show ?thesis by auto
qed

lemma append_rows_mult_left_id2:
 assumes A: "(A::'a::comm_semiring_1 mat)  carrier_mat a n"
   and B: "B  carrier_mat b n"
   and C: "C = four_block_mat D (0m a b) (0m b a) (1m b)"
   and D: "D  carrier_mat a a"
 shows "C * (A @r B) = (D * A) @r B"
proof -
  have "(C * (A @r B))T = (A @r B)T * CT" by (rule transpose_mult, insert assms, auto)
  also have "... = (AT @c BT) * CT" by (metis A B transpose_mat_append_rows)
  also have "... = (AT * DT @c BT)" by (rule append_cols_mult_right_id2, insert assms, auto)
  also have "...T = (D * A) @r B"
    by (metis A B D transpose_mult transpose_transpose mult_carrier_mat transpose_mat_append_rows)
  finally show ?thesis by simp
qed

lemma four_block_mat_preserves_column:
  assumes A: "(A::'a::semiring_1 mat)  carrier_mat n m"
    and B: "B = four_block_mat (1m 1) (0m 1 (m - 1)) (0m (m - 1) 1) C"
  and C: "C  carrier_mat (m-1) (m-1)"
  and i: "i<n" and m: "0<m"
shows "(A*B) $$ (i,0) = A $$ (i,0)"
proof -
  let ?A1 = "mat_of_cols n [col A 0]"
  let ?A2 = "mat_of_cols n (map (col A) [1..<dim_col A])"
  have n2: "dim_row A = n" using A by auto
  have "A = ?A1 @c ?A2" by (rule append_cols_split[of A, unfolded n2], insert m A, auto)
  hence "A * B = (?A1 @c ?A2) * B" by simp
  also have "... = ?A1 @c (?A2 * C)" by (rule append_cols_mult_right_id[OF _ _ B C], insert A, auto)
  also have "... $$ (i,0) = ?A1 $$ (i,0)" using append_cols_nth by (simp add: append_cols_def i)
  also have "... = A $$ (i,0)"
    by (metis A i carrier_matD(1) col_def index_vec mat_of_cols_Cons_index_0)
  finally show ?thesis .
qed


definition "lower_triangular A = (i j. i < j  i < dim_row A  j < dim_col A  A $$ (i,j) = 0)"

lemma lower_triangular_index:
  assumes "lower_triangular A" "i<j" "i < dim_row A" "j < dim_col A"
  shows "A $$ (i,j) = 0"
  using assms unfolding lower_triangular_def by auto

lemma commute_multiples_identity:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat n n"
  shows "A * (k m (1m n)) = (k m (1m n)) * A"
proof -
  have "(ia = 0..<n. A $$ (i, ia) * (k * (if ia = j then 1 else 0)))
    = (ia = 0..<n. k * (if i = ia then 1 else 0) * A $$ (ia, j))" (is "?lhs=?rhs")
    if i: "i<n" and j: "j<n" for i j
  proof -
    let ?f = "λia. A $$ (i, ia) * (k * (if ia = j then 1 else 0))"
    let ?g = "λia. k * (if i = ia then 1 else 0) * A $$ (ia, j)"
    have rw0: "(ia  ({0..<n}-{j}). ?f ia) = 0" by (rule sum.neutral, auto)
    have rw0': "(ia  ({0..<n}-{i}). ?g ia) = 0" by (rule sum.neutral, auto)
    have "?lhs = ?f j + (ia  ({0..<n}-{j}). ?f ia)"
      by (smt (verit, del_insts) atLeast0LessThan finite_atLeastLessThan
          lessThan_iff sum.remove that(2))
    also have "... = A $$ (i, j) * k" using rw0 by auto
    also have "... = ?g i + (ia  ({0..<n}-{i}). ?g ia)" using rw0' by auto
    also have "... = ?rhs"
      by (smt (verit, ccfv_SIG) atLeast0LessThan finite_lessThan lessThan_iff sum.remove that(1))
    finally show ?thesis .
  qed
  thus ?thesis using A
    by (metis (no_types, lifting) left_mult_one_mat mult_smult_assoc_mat mult_smult_distrib
        one_carrier_mat right_mult_one_mat)
qed

(*This lemma is obtained using Mod_Type_Connect, otherwise we cannot prove HMA_I 0 0.
The lelma could also be obtained with no use of transfer rules, proving it directly.*)
lemma det_2:
  assumes A: "A  carrier_mat 2 2"
  shows "Determinant.det A = A$$(0,0) * A $$ (1,1) - A$$(0,1)*A$$(1,0)"
proof -
  let ?A = "(Mod_Type_Connect.to_hmam A)::'a^2^2"
  have [transfer_rule]: "Mod_Type_Connect.HMA_M A ?A"
    unfolding Mod_Type_Connect.HMA_M_def using from_hma_to_hmam A by auto
  have [transfer_rule]: "Mod_Type_Connect.HMA_I 0 0"
    unfolding Mod_Type_Connect.HMA_I_def by (simp add: to_nat_0)
  have [transfer_rule]: "Mod_Type_Connect.HMA_I 1 1"
    unfolding Mod_Type_Connect.HMA_I_def by (simp add: to_nat_1)
  have "Determinant.det A = Determinants.det ?A" by (transfer, simp)
  also have "... = ?A $h 1 $h 1 * ?A $h 2 $h 2 - ?A $h 1 $h 2 * ?A $h 2 $h 1" unfolding det_2 by simp
  also have "... = ?A $h 0 $h 0 * ?A $h 1 $h 1 - ?A $h 0 $h 1 * ?A $h 1 $h 0"
    by (smt (verit, ccfv_SIG) Groups.mult_ac(2) exhaust_2 semiring_norm(160))
  also have "... = A$$(0,0) * A $$ (1,1) - A$$(0,1)*A$$(1,0)"
    unfolding index_hma_def[symmetric] by (transfer, auto)
  finally show ?thesis .
qed

lemma mat_diag_smult: "mat_diag n (λ x. (k::'a::comm_ring_1)) = (k m 1m n)"
proof -
  have "mat_diag n (λ x. k) = mat_diag n (λ x. k * 1)" by auto
  also have "... = mat_diag n (λ x. k) * mat_diag n (λ x. 1)" using mat_diag_diag
    by (simp add: mat_diag_def)
  also have "... = mat_diag n (λ x. k) * (1m n)" by auto  thm mat_diag_mult_left
  also have "... = Matrix.mat n n (λ(i, j). k * (1m n) $$ (i, j))" by (rule mat_diag_mult_left, auto)
  also have "... = (k m 1m n)" unfolding smult_mat_def by auto
  finally show ?thesis .
qed

lemma invertible_mat_four_block_mat_lower_right:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat n n" and inv_A: "invertible_mat A"
  shows "invertible_mat (four_block_mat (1m 1) (0m 1 n) (0m n 1) A)"
proof -
  let ?I = "(four_block_mat (1m 1) (0m 1 n) (0m n 1) A)"
  have "Determinant.det ?I = Determinant.det (1m 1) * Determinant.det A"
    by (rule det_four_block_mat_lower_left_zero_col, insert assms, auto)
  also have "... = Determinant.det A" by auto
  finally have "Determinant.det ?I = Determinant.det A" .
  thus ?thesis
    by (metis (no_types, lifting) assms carrier_matD(1) carrier_matD(2) carrier_mat_triv
        index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3)
        invertible_iff_is_unit_JNF)
qed


lemma invertible_mat_four_block_mat_lower_right_id:
  assumes A: "(A::'a::comm_ring_1 mat)  carrier_mat m m" and B: "B = 0m m (n-m)" and C: "C = 0m (n-m) m"
    and D: "D = 1m (n-m)" and "n>m" and inv_A: "invertible_mat A"
  shows "invertible_mat (four_block_mat A B C D)"
proof -
  have "Determinant.det (four_block_mat A B C D) = Determinant.det A"
    by (rule det_four_block_mat_lower_right_id, insert assms, auto)
  thus ?thesis using inv_A
    by (metis (no_types, lifting) assms(1) assms(4) carrier_matD(1) carrier_matD(2) carrier_mat_triv
        index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3)
        invertible_iff_is_unit_JNF)
qed

lemma split_block4_decreases_dim_row:
  assumes E: "(A,B,C,D) = split_block E 1 1"
    and E1: "dim_row E > 1" and E2: "dim_col E > 1"
  shows "dim_row D < dim_row E"
proof -
  have "D  carrier_mat (1 + (dim_row E - 2)) (1 + (dim_col E - 2))"
    by (rule split_block(4)[OF E[symmetric]], insert E1 E2, auto)
  hence "D  carrier_mat (dim_row E - 1) (dim_col E - 1)" using E1 E2 by auto
  thus ?thesis using E1 by auto
qed


lemma inv_P'PAQQ':
  assumes A: "A  carrier_mat n n"
    and P: "P  carrier_mat n n"
    and inv_P: "inverts_mat P' P"
    and inv_Q: "inverts_mat Q Q'"
    and Q: "Q  carrier_mat n n"
    and P': "P'  carrier_mat n n"
    and Q': "Q'  carrier_mat n n"
shows  "(P'*(P*A*Q)*Q') = A"
proof -
  have "(P'*(P*A*Q)*Q') = (P'*(P*A*Q*Q'))"
    by (meson P P' Q Q' assms(1) assoc_mult_mat mult_carrier_mat)
  also have "... = ((P'*P)*A*(Q*Q'))"
    by (smt (verit, ccfv_SIG) P' Q' assms(1) assms(2) assms(5) assoc_mult_mat mult_carrier_mat)
  finally show ?thesis
    by (metis P' Q A inv_P inv_Q carrier_matD(1) inverts_mat_def
        left_mult_one_mat right_mult_one_mat)
qed

lemma
  assumes "U  carrier_mat 2 2" and "V  carrier_mat 2 2" and "A = U * V"
shows mat_mult2_00: "A $$ (0,0) = U $$ (0,0)*V $$ (0,0) + U $$ (0,1)*V $$ (1,0)"
  and mat_mult2_01: "A $$ (0,1) = U $$ (0,0)*V $$ (0,1) + U $$ (0,1)*V $$ (1,1)"
  and mat_mult2_10: "A $$ (1,0) = U $$ (1,0)*V $$ (0,0) + U $$ (1,1)*V $$ (1,0)"
  and mat_mult2_11: "A $$ (1,1) = U $$ (1,0)*V $$ (0,1) + U $$ (1,1)*V $$ (1,1)"
    using assms unfolding times_mat_def Matrix.row_def col_def scalar_prod_def
    using sum_two_rw by auto


subsection‹Lemmas about @{text "sorted lists"}, @{text "insort"} and @{text "pick"}


lemma sorted_distinct_imp_sorted_wrt:
  assumes "sorted xs" and "distinct xs"
  shows "sorted_wrt (<) xs"
  using assms
  by (induct xs, insert le_neq_trans, auto)


lemma sorted_map_strict:
  assumes "strict_mono_on {0..<n} g"
  shows "sorted (map g [0..<n])"
  using assms
  by (induct n, auto simp add: sorted_append strict_mono_on_def less_imp_le)


lemma sorted_list_of_set_map_strict:
  assumes "strict_mono_on {0..<n} g"
  shows "sorted_list_of_set (g ` {0..<n}) = map g [0..<n]"
  using assms
  proof (induct n)
  case 0
  then show ?case by auto
next
  case (Suc n)
  note sg = Suc.prems
  have sg_n: "strict_mono_on {0..<n} g" using sg unfolding strict_mono_on_def by auto
  have g_image_rw: "g ` {0..<Suc n} = insert (g n) (g ` {0..<n})"
    by (simp add: set_upt_Suc)
  have "sorted_list_of_set (g ` {0..<Suc n}) = sorted_list_of_set (insert (g n) (g ` {0..<n}))"
    using g_image_rw by simp
  also have "... = insort (g n) (sorted_list_of_set (g ` {0..<n}))"
  proof (rule sorted_list_of_set_insert)
    have "inj_on g {0..<Suc n}" using sg strict_mono_on_imp_inj_on by blast
    thus "g n  g ` {0..<n}" unfolding inj_on_def by fastforce
  qed (simp)
  also have "... = insort (g n) (map g [0..<n])"
    using Suc.hyps sg unfolding strict_mono_on_def by auto
  also have "... = map g [0..<Suc n]"
  proof (simp, rule sorted_insort_is_snoc)
    show "sorted (map g [0..<n])" by (rule sorted_map_strict[OF sg_n])
    show "xset (map g [0..<n]). x  g n" using sg unfolding strict_mono_on_def
      by (simp add: less_imp_le)
  qed
  finally show ?case .
qed


lemma sorted_nth_strict_mono:
  "sorted xs  distinct xs i < j  j < length xs  xs!i < xs!j"
  by (simp add: less_le nth_eq_iff_index_eq sorted_iff_nth_mono_less)


lemma sorted_list_of_set_0_LEAST:
  assumes finI: "finite I" and I: "I  {}"
  shows "sorted_list_of_set I ! 0 = (LEAST n. nI)"
proof (rule Least_equality[symmetric])
  show "sorted_list_of_set I ! 0  I"
    by (metis I Max_in finI gr_zeroI in_set_conv_nth not_less_zero set_sorted_list_of_set)
  fix y assume "y  I"
  thus "sorted_list_of_set I ! 0  y"
    by (metis eq_iff finI in_set_conv_nth neq0_conv sorted_iff_nth_mono_less
        sorted_list_of_set(1) sorted_sorted_list_of_set)
qed

lemma sorted_list_of_set_eq_pick:
  assumes i: "i < length (sorted_list_of_set I)"
  shows "sorted_list_of_set I ! i = pick I i"
proof -
  have finI: "finite I"
  proof (rule ccontr)
    assume "infinite I"
    hence "length (sorted_list_of_set I) = 0" by auto
    thus False using i by simp
  qed
  show ?thesis
  using i
proof (induct i)
  case 0
  have I: "I  {}" using "0.prems" sorted_list_of_set_empty by blast
  show ?case unfolding pick.simps by (rule sorted_list_of_set_0_LEAST[OF finI I])
next
  case (Suc i)
  note x_less = Suc.prems
  show ?case
  proof (unfold pick.simps, rule Least_equality[symmetric], rule conjI)
    show 1: "pick I i < sorted_list_of_set I ! Suc i"
      by (metis Suc.hyps Suc.prems Suc_lessD distinct_sorted_list_of_set find_first_unique lessI
          nat_less_le sorted_sorted_list_of_set sorted_wrt_nth_less)
    show "sorted_list_of_set I ! Suc i  I"
      using Suc.prems finI nth_mem set_sorted_list_of_set by blast
    have rw: "sorted_list_of_set I ! i = pick I i"
      using Suc.hyps Suc_lessD x_less by blast
    have sorted_less: "sorted_list_of_set I ! i < sorted_list_of_set I ! Suc i"
      by (simp add: 1 rw)
    fix y assume y: "y  I  pick I i < y"
    show "sorted_list_of_set I ! Suc i  y"
      by (smt (verit) antisym_conv finI in_set_conv_nth less_Suc_eq less_Suc_eq_le nat_neq_iff rw
          sorted_iff_nth_mono_less sorted_list_of_set(1) sorted_sorted_list_of_set x_less y)
  qed
qed
qed

text‹$b$ is the position where we add, $a$ the element to be added and $i$ the position
  that is checked›

lemma insort_nth':
  assumes "j<b. xs ! j < a" and "sorted xs" and "a  set xs"
    and "i < length xs + 1" and "i < b"
    and "xs  []" and "b < length xs"
  shows "insort a xs ! i = xs ! i"
  using assms
proof (induct xs arbitrary: a b i)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  note less = Cons.prems(1)
  note sorted = Cons.prems(2)
  note a_notin = Cons.prems(3)
  note i_length = Cons.prems(4)
  note i_b = Cons.prems(5)
  note b_length = Cons.prems(7)
  show ?case
  proof (cases "a  x")
    case True
    have "insort a (x # xs) ! i = (a # x # xs) ! i" using True by simp
    also have "... =  (x # xs) ! i"
      using Cons.prems(1) Cons.prems(5) True by force
    finally show ?thesis .
  next
    case False note x_less_a = False
    have "insort a (x # xs) ! i = (x # insort a xs) ! i" using False by simp
    also have "... = (x # xs) ! i"
    proof (cases "i = 0")
      case True
      then show ?thesis by auto
    next
      case False
      have "(x # insort a xs) ! i = (insort a xs) ! (i-1)"
        by (simp add: False nth_Cons')
      also have "... = xs ! (i-1)"
      proof (rule Cons.hyps)
        show "sorted xs" using sorted by simp
        show "a  set xs" using a_notin by simp
        show "i - 1 < length xs + 1" using i_length False by auto
        show "xs  []" using i_b b_length by force
        show "i - 1 < b - 1" by (simp add: False diff_less_mono i_b leI)
        show "b - 1 < length xs" using b_length i_b by auto
        show "j<b - 1. xs ! j < a" using less less_diff_conv by auto
      qed
      also have "... = (x # xs) ! i" by (simp add: False nth_Cons')
      finally show ?thesis .
    qed
    finally show ?thesis .
  qed
qed


lemma insort_nth:
  assumes  "sorted xs" and "a  set xs"
    and "i < index (insort a xs) a"
    and "xs  []"
  shows "insort a xs ! i = xs ! i"
  using assms
proof (induct xs arbitrary: a i)
case Nil
  then show ?case by auto
next
  case (Cons x xs)
  note sorted = Cons.prems(1)
  note a_notin = Cons.prems(2)
  note i_index = Cons.prems(3)
  show ?case
  proof (cases "a  x")
    case True
    have "insort a (x # xs) ! i = (a # x # xs) ! i" using True by simp
    also have "... = (x # xs) ! i"
      using Cons.prems(1) Cons.prems(3) True by force
    finally show ?thesis .
  next
    case False note x_less_a = False
    show ?thesis
    proof (cases "xs = []")
      case True
      have "x  a" using False by auto
      then show ?thesis  using True i_index False by auto
    next
      case False note xs_not_empty = False
      have "insort a (x # xs) ! i = (x # insort a xs) ! i" using x_less_a by simp
      also have "... = (x # xs) ! i"
      proof (cases "i = 0")
        case True
        then show ?thesis by auto
      next
        case False note i0 = False
        have "(x # insort a xs) ! i = (insort a xs) ! (i-1)"
          by (simp add: False nth_Cons')
        also have "... = xs ! (i-1)"
        proof (rule Cons.hyps[OF _ _ _ xs_not_empty])
          show "sorted xs" using sorted by simp
          show "a  set xs" using a_notin by simp
          have "index (insort a (x # xs)) a = index ((x # insort a xs)) a"
            using x_less_a by auto
          also have "... = index (insort a xs) a + 1"
            unfolding index_Cons using x_less_a by simp
          finally show "i - 1 < index (insort a xs) a" using False i_index by linarith
        qed
        also have "... = (x # xs) ! i" by (simp add: False nth_Cons')
        finally show ?thesis .
      qed
      finally show ?thesis .
    qed
  qed
qed

lemma insort_nth2:
  assumes "sorted xs" and "a  set xs"
    and "i < length xs" and "i  index (insort a xs) a"
    and "xs  []"
  shows "insort a xs ! (Suc i) = xs ! i"
  using assms
proof (induct xs arbitrary: a i)
  case Nil
  then show ?case by auto
next
  case (Cons x xs)
  note sorted = Cons.prems(1)
  note a_notin = Cons.prems(2)
  note i_length = Cons.prems(3)
  note index_i = Cons.prems(4)
  show ?case
  proof (cases "a  x")
    case True
    have "insort a (x # xs) ! (Suc i) = (a # x # xs) ! (Suc i)" using True by simp
    also have "... =  (x # xs) ! i"
      using Cons.prems(1) Cons.prems(5) True by force
    finally show ?thesis .
  next
    case False note x_less_a = False
    have "insort a (x # xs) ! (Suc i) = (x # insort a xs) ! (Suc i)" using False by simp
    also have "... = (x # xs) ! i"
    proof (cases "i = 0")
        case True
        then show ?thesis using index_i linear x_less_a by fastforce
      next
        case False note i0 = False
        show ?thesis
        proof -
          have Suc_i: "Suc (i - 1) = i"
            using i0 by auto
          have "(x # insort a xs) ! (Suc i) = (insort a xs) ! i"
            by (simp add: nth_Cons')
          also have "... = (insort a xs) ! Suc (i - 1)" using Suc_i by simp
          also have "... = xs ! (i - 1)"
          proof (rule Cons.hyps)
            show "sorted xs" using sorted by simp
            show "a  set xs" using a_notin by simp
            show "i - 1 < length xs" using i_length using Suc_i by auto
            thus "xs  []" by auto
            have "index (insort a (x # xs)) a = index ((x # insort a xs)) a" using x_less_a by simp
            also have "... = index (insort a xs) a + 1" unfolding index_Cons using x_less_a by simp
            finally show "index (insort a xs) a  i - 1" using index_i i0 by auto
          qed
          also have "... = (x # xs) ! i" using Suc_i by auto
          finally show ?thesis .
        qed
      qed
      finally show ?thesis .
    qed
qed

lemma pick_index:
  assumes a: "a  I" and a'_card: "a' < card I"
  shows "(pick I a' = a) = (index (sorted_list_of_set I) a = a')"
proof -
  have finI: "finite I" using a'_card card.infinite by force
  have length_I: "length (sorted_list_of_set I) = card I"
    by (metis a'_card card.infinite distinct_card distinct_sorted_list_of_set
        not_less_zero set_sorted_list_of_set)
  let ?i = "index (sorted_list_of_set I) a"
  have "(sorted_list_of_set I) ! a' = pick I a'"
    by (rule sorted_list_of_set_eq_pick, auto simp add: finI a'_card length_I)
  moreover have "(sorted_list_of_set I) ! ?i = a"
    by (rule nth_index, simp add: a finI)
  ultimately show ?thesis
    by (metis a'_card distinct_sorted_list_of_set index_nth_id length_I)
qed

end