Theory Commuting_Hermitian

(*
Author: 
  Mnacho Echenim, Université Grenoble Alpes
*)

theory Commuting_Hermitian imports Spectral_Theory_Complements Commuting_Hermitian_Misc
"Projective_Measurements.Linear_Algebra_Complements" 
"Projective_Measurements.Projective_Measurements" begin 

section ‹Additional results on block decompositions of matrices›

subsection ‹Split block results›

lemma split_block_diag_carrier:
  assumes "D  carrier_mat n n"
  and "a  n"
  and "split_block D a a = (D1, D2, D3, D4)"
shows "D1 carrier_mat a a" "D4 carrier_mat (n-a) (n-a)"
proof -
  show "D1 carrier_mat a a" using assms unfolding split_block_def
    by (metis Pair_inject mat_carrier)
  show "D4  carrier_mat (n-a) (n-a)" using assms unfolding split_block_def
    by (metis Pair_inject carrier_matD(1) carrier_matD(2) mat_carrier)
qed

lemma split_block_diagonal:
  assumes "diagonal_mat D"
  and "D  carrier_mat n n"
and "a  n"
and "split_block D a a = (D1, D2, D3, D4)"
shows "diagonal_mat D1  diagonal_mat D4" unfolding diagonal_mat_def
proof (intro allI conjI impI)
  have "D1  carrier_mat a a" using assms unfolding split_block_def Let_def 
    by fastforce
  fix i j
  assume "i < dim_row D1"
  and "j < dim_col D1"
  and "i  j"
  have "D1 $$ (i,j) = D $$(i,j)" using assms unfolding split_block_def Let_def
    using i < dim_row D1 j < dim_col D1 by fastforce
  also have "... = 0" using assms i  j  D1  carrier_mat a a 
    i < dim_row D1 j < dim_col D1 unfolding diagonal_mat_def by fastforce
  finally show "D1 $$(i,j) = 0" .
next
  have "D4  carrier_mat (n-a) (n-a)" using assms 
    unfolding split_block_def Let_def by fastforce
  fix i j
  assume "i < dim_row D4"
  and "j < dim_col D4"
  and "i  j"
  have "D4 $$ (i,j) = D $$(i + a,j + a)" using assms unfolding split_block_def Let_def
    using i < dim_row D4 j < dim_col D4 by fastforce
  also have "... = 0" using assms i  j  D4  carrier_mat (n-a) (n-a) 
    i < dim_row D4 j < dim_col D4 unfolding diagonal_mat_def by fastforce
  finally show "D4 $$(i,j) = 0" .
qed

lemma split_block_times_diag_index:
  fixes B::"'a::comm_ring Matrix.mat"
  assumes "diagonal_mat D"
  and "D carrier_mat n n"
  and "B carrier_mat n n"
  and "a  n"
  and "split_block B a a = (B1, B2, B3, B4)"
  and "split_block D a a = (D1, D2, D3, D4)"
  and "i < dim_row (D4 * B4)"
  and "j < dim_col (D4 * B4)"
shows "(B4 * D4) $$ (i, j) = (B*D) $$ (i+a, j+a)"
      "(D4 * B4) $$ (i, j) = (D*B) $$ (i+a, j+a)"
proof -
  have d4: "D4  carrier_mat (n-a) (n-a)" using assms  
      split_block(4)[of D] by simp
  have b4: "B4  carrier_mat (n-a) (n-a)" using assms  
      split_block(4)[of B] by simp
  have "diagonal_mat D4" using assms split_block_diagonal[of D] by blast
  have "i < n-a" using i < dim_row (D4 * B4) b4 d4 by simp
  have "j < n-a" using j < dim_col (D4 * B4) b4 d4 by simp
  have "(B4 * D4) $$ (i, j) = D4 $$ (j,j) * B4 $$ (i,j)" 
  proof (rule  diagonal_mat_mult_index') 
    show "diagonal_mat D4" using diagonal_mat D4 .
    show "B4  carrier_mat (n-a) (n-a)" using b4 .
    show "D4  carrier_mat (n - a) (n - a)" using d4 .
    show "i < n-a" using i < n-a .
    show "j < n-a" using j < n-a .
  qed
  also have "... = D $$ (j+a, j+a) * B $$ (i+a, j+a)" 
    using assms i < n-a j < n-a 
    unfolding split_block_def Let_def by fastforce 
  also have "... = (B*D) $$ (i+a, j+a)" using diagonal_mat_mult_index' assms
    by (metis i < n - a j < n - a less_diff_conv)
  finally show "(B4 * D4) $$ (i, j) = (B*D) $$ (i+a, j+a)" .
  have "(D4 * B4) $$ (i, j) = D4 $$ (i,i) * B4 $$ (i,j)" 
    using diagonal_mat_mult_index diagonal_mat D4 i < n - a j < n - a b4 d4 
    by blast
  also have "... = D $$ (i+a, i+a) * B $$ (i+a, j+a)" 
    using assms i < n-a j < n-a 
    unfolding split_block_def Let_def by fastforce
  also have "... = (D*B) $$ (i+a, j+a)" using diagonal_mat_mult_index assms
    by (metis i < n - a j < n - a less_diff_conv)
  finally show "(D4 * B4) $$ (i, j) = (D*B) $$ (i+a, j+a)" .
qed

lemma split_block_commute_subblock:
  fixes B::"'a::comm_ring Matrix.mat"
  assumes "diagonal_mat D"
  and "D carrier_mat n n"
  and "B carrier_mat n n"
  and "a  n"
  and "split_block B a a = (B1, B2, B3, B4)"
  and "split_block D a a = (D1, D2, D3, D4)"
  and "B * D = D * B"
shows "B4 * D4 = D4 * B4"
proof
  have d4: "D4  carrier_mat (n-a) (n-a)" using assms  
      split_block(4)[of D] by simp
  have b4: "B4  carrier_mat (n-a) (n-a)" using assms  
      split_block(4)[of B] by simp
  have "diagonal_mat D4" using assms split_block_diagonal[of D] by blast
  show "dim_row (B4 * D4) = dim_row (D4 * B4)" using d4 b4 by simp
  show "dim_col (B4 * D4) = dim_col (D4 * B4)" using d4 b4 by simp
  fix i j
  assume "i < dim_row (D4 * B4)"
  and "j < dim_col (D4 * B4)"
  have "(B4*D4) $$(i,j) = (B*D) $$(i+a, j+a)"
    using split_block_times_diag_index[of D n B a] assms
      i < dim_row (D4 * B4) j < dim_col (D4 * B4) by blast
  also have "... = (D*B) $$ (i+a, j+a)" using assms by simp
  also have "... = (D4*B4) $$ (i, j)"
    using split_block_times_diag_index[of D n B a] assms
    by (metis i < dim_row (D4 * B4) j < dim_col (D4 * B4))
  finally show "(B4*D4) $$(i,j) = (D4*B4) $$ (i, j)" .
qed

lemma commute_diag_mat_zero_comp:
  fixes D::"'a::{field} Matrix.mat"
  assumes "diagonal_mat D"
  and "D carrier_mat n n"
  and "B carrier_mat n n"
  and" B* D = D * B"
  and "i < n"
  and "j < n"
  and "D$$(i,i)  D$$(j,j)"
shows "B $$(i,j) = 0"
proof -
  have "B$$(i,j) * D$$(j,j) = (B*D) $$(i,j)" 
    using diagonal_mat_mult_index'[of B n D] assms by simp
  also have "... = (D*B) $$ (i,j)" using assms by simp
  also have "... = B$$(i,j) * D$$(i,i)" 
    using diagonal_mat_mult_index  assms
    by (metis Groups.mult_ac(2))
  finally have "B$$(i,j) * D$$(j,j) = B$$(i,j) * D$$(i,i)" .
  hence "B$$(i,j) * (D$$(j,j) - D$$(i,i)) = 0" by auto
  thus "B$$(i,j) = 0" using assms by simp
qed

lemma commute_diag_mat_split_block:
  fixes D::"'a::{field} Matrix.mat"
  assumes "diagonal_mat D"
  and "D carrier_mat n n"
  and "B carrier_mat n n"
  and" B* D = D * B"
  and "k  n"
  and "i j. (i < k  k  j  j < n)  D$$(i,i)  D$$(j,j)"
  and "(B1, B2, B3, B4) = split_block B k k"
shows "B2 = 0m k (n-k)" "B3 = 0m (n-k) k"
proof (intro eq_matI)
  show "dim_row B2 = dim_row (0m k (n - k))" 
    using assms unfolding split_block_def Let_def by simp
  show "dim_col B2 = dim_col (0m k (n - k))" 
    using assms unfolding split_block_def Let_def by simp
  fix i j
  assume "i < dim_row (0m k (n - k))"
  and "j < dim_col (0m k (n - k))" note ijprop = this
  have "B2 $$ (i, j) = B $$ (i, j+k)" using assms ijprop 
    unfolding split_block_def Let_def by simp
  also have "... = 0" 
  proof (rule commute_diag_mat_zero_comp[of D n], (auto simp add: assms))
    show "i < n" using ijprop assms by simp
    show "j + k < n" using ijprop assms by simp
    show "D $$ (i, i) = D $$ (j + k, j + k)  False" using ijprop assms
      by (metis j + k < n index_zero_mat(2) le_add2)
  qed
  finally show "B2 $$ (i, j) = 0m k (n - k) $$ (i, j)" using ijprop by simp
next 
  show "B3 = 0m (n-k) k"
  proof (intro eq_matI)
    show "dim_row B3 = dim_row (0m (n - k) k)" 
      using assms unfolding split_block_def Let_def by simp
    show "dim_col B3 = dim_col (0m (n - k) k)" 
      using assms unfolding split_block_def Let_def by simp
    fix i j
    assume "i < dim_row (0m (n - k) k)"
    and "j < dim_col (0m (n - k) k)" note ijprop = this
    have "B3 $$ (i, j) = B $$ (i+k, j)" using assms ijprop 
      unfolding split_block_def Let_def by simp
    also have "... = 0" 
    proof (rule commute_diag_mat_zero_comp[of D n], (auto simp add: assms))
      show "i + k < n" using ijprop assms by simp
      show "j < n" using ijprop assms by simp
      show "D $$ (i+k, i+k) = D $$ (j, j)  False" using ijprop assms
        by (metis i + k < n index_zero_mat(3) le_add2)
    qed
    finally show "B3 $$ (i, j) = 0m (n - k) k $$ (i, j)" using ijprop by simp
  qed
qed

lemma split_block_hermitian_1:
  assumes "hermitian A"
  and "n  dim_row A"
and "(A1, A2, A3, A4) = split_block A n n"
shows "hermitian A1"  unfolding hermitian_def
proof (rule eq_matI, auto)
  have "dim_row A = dim_col A" using assms
    by (metis carrier_matD(2) hermitian_square) 
  show "dim_col A1 = dim_row A1" using assms unfolding split_block_def Let_def 
    by simp
  thus "dim_row A1 = dim_col A1" by simp
  show "i j. i < dim_row A1  j < dim_col A1  
    Complex_Matrix.adjoint A1 $$ (i, j) = A1 $$ (i, j)"
  proof -
    fix i j
    assume "i < dim_row A1" and "j < dim_col A1" note ij = this
    have r: "dim_row A1 = n" using assms unfolding split_block_def Let_def 
      by simp
    have c: "dim_col A1 = n" using assms unfolding split_block_def Let_def 
      by simp
    have "Complex_Matrix.adjoint A1 $$ (i, j) = conjugate (A1 $$ (j,i))"
      using ij r c unfolding Complex_Matrix.adjoint_def by simp
    also have "... = conjugate (A $$ (j,i))" using assms ij r c
      unfolding split_block_def Let_def by simp
    also have "... = A $$ (i,j)" using assms ij r c dim_row A = dim_col A
      unfolding hermitian_def Complex_Matrix.adjoint_def
      by (metis adjoint_eval assms(1) hermitian_def order_less_le_trans)
    also have "... = A1 $$(i,j)" using assms ij r c 
      unfolding split_block_def Let_def by simp
    finally show "Complex_Matrix.adjoint A1 $$ (i, j) = A1 $$ (i, j)" .
  qed
qed

lemma split_block_hermitian_4:
  assumes "hermitian A"
  and "n  dim_row A"
and "(A1, A2, A3, A4) = split_block A n n"
shows "hermitian A4"  unfolding hermitian_def
proof (rule eq_matI, auto)
  have arc: "dim_row A = dim_col A" using assms
    by (metis carrier_matD(2) hermitian_square) 
  thus "dim_col A4 = dim_row A4" using assms unfolding split_block_def Let_def 
    by simp
  thus "dim_row A4 = dim_col A4" by simp
  show "i j. i < dim_row A4  j < dim_col A4  
    Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)"
  proof -
    fix i j
    assume "i < dim_row A4" and "j < dim_col A4" note ij = this
    have r: "dim_row A4 = dim_row A - n" using assms 
      unfolding split_block_def Let_def by simp
    have c: "dim_col A4 = dim_col A - n" using assms 
      unfolding split_block_def Let_def by simp
    have "Complex_Matrix.adjoint A4 $$ (i, j) = conjugate (A4 $$ (j,i))"
      using ij r c arc unfolding Complex_Matrix.adjoint_def by simp
    also have "... = conjugate (A $$ (j +n ,i+n))" using assms ij r c arc
      unfolding split_block_def Let_def by simp
    also have "... = A $$ (i+n,j+n)" using assms ij r c arc 
      unfolding hermitian_def Complex_Matrix.adjoint_def
      by (metis index_mat(1) less_diff_conv split_conv)      
    also have "... = A4 $$(i,j)" using assms ij r c 
      unfolding split_block_def Let_def by simp
    finally show "Complex_Matrix.adjoint A4 $$ (i, j) = A4 $$ (i, j)" .
  qed
qed

lemma diag_block_split_block:
  assumes "B carrier_mat n n"
  and "k < n"
  and "(B1, B2, B3, B4) = split_block B k k"
  and "B2 = 0m k (n-k)" 
  and "B3 = 0m (n-k) k"
shows "B = diag_block_mat [B1,B4]"
proof -
  have dr: "dim_row B = k + (n-k)" using assms by simp
  have dc: "dim_col B = k + (n-k)" using assms by simp
  have c1: "B1  carrier_mat k k" using assms 
    split_block(1)[of B, OF _ dr dc] by metis
  have c4: "B4  carrier_mat (n-k) (n-k)" using assms 
    split_block(4)[of B, OF _ dr dc] by metis
  have d4: "diag_block_mat [B4] = B4" using diag_block_mat_singleton[of B4] 
    by simp
  have "B = four_block_mat B1 B2 B3 B4" using assms split_block(3)[of B k ]
    by (metis carrier_matD(1) carrier_matD(2) diff_is_0_eq 
        le_add_diff_inverse nat_le_linear semiring_norm(137) 
        split_block(5) zero_less_diff) 
  also have "... = four_block_mat B1 (0m k (n-k)) (0m (n-k) k) B4" 
    using assms by simp
  also have "... = four_block_mat B1 (0m k (n-k)) (0m (n-k) k) 
    (diag_block_mat [B4])" using diag_block_mat_singleton[of B4] by simp
  also have "... = diag_block_mat [B1, B4]" 
    using diag_block_mat.simps(2)[of B1 "[B4]"] c1 c4 
    unfolding Let_def by auto
  finally show ?thesis .
qed

subsection ‹Diagonal block matrices›

abbreviation four_block_diag where
"four_block_diag B1 B2 
  (four_block_mat B1 (0m (dim_row B1) (dim_col B2)) 
  (0m (dim_row B2) (dim_col B1)) B2)"

lemma four_block_diag_cong_comp:
  assumes "dim_row A1 = dim_row B1"
  and "dim_col A1 = dim_col B1"
  and "four_block_diag A1 A2 = four_block_diag B1 B2"
shows "A1 = B1"
proof (rule eq_matI, auto simp:assms)
  define A where "A = four_block_diag A1 A2"
  define B where "B = four_block_diag B1 B2"
  fix i j
  assume "i < dim_row B1" and "j<dim_col B1" note ij=this
  hence "i <dim_row A1" "j<dim_col A1" using assms by auto
  hence "A1$$(i,j) = A$$(i, j)" 
    unfolding A_def four_block_mat_def Let_def by force 
  also have "... = B$$(i, j)" using assms unfolding A_def B_def by simp
  also have "... = B1$$(i,j)" 
    using ij unfolding B_def four_block_mat_def Let_def by force 
  finally show "A1$$(i,j) = B1$$(i,j)" .
qed

lemma four_block_diag_cong_comp':
  assumes "dim_row A1 = dim_row B1"
  and "dim_col A1 = dim_col B1"
  and "four_block_diag A1 A2 = four_block_diag B1 B2"
shows "A2 = B2"
proof (rule eq_matI)
  define n where "n=dim_row A1"
  define m where "m = dim_col A1"
  define A where "A = four_block_diag A1 A2"
  define B where "B = four_block_diag B1 B2"
  show "dim_row A2 = dim_row B2" 
    using assms unfolding four_block_mat_def Let_def
    by (metis assms(3) diff_add_inverse index_mat_four_block(2)) 
  show "dim_col A2 = dim_col B2"
    using assms unfolding four_block_mat_def Let_def
    by (metis assms(3) diff_add_inverse index_mat_four_block(3))
  fix i j
  assume "i < dim_row B2" and "j<dim_col B2" note ij=this
  hence "i+n < dim_row A" 
    unfolding A_def n_def m_def four_block_mat_def Let_def
    by (simp add: dim_row A2 = dim_row B2)
  have "j+m < dim_col A"
    unfolding A_def n_def m_def four_block_mat_def Let_def
    by (simp add: dim_col A2 = dim_col B2 ij)
  {
    have "n  i+n" by simp
    have "m j+m" by simp
    have "i + n - n = i" by simp
    have "j + m - m = j" by simp
  } note ijeq = this
  have "A2$$(i,j) = A$$(i+n, j+m)" using ijeq
    using A_def i + n < dim_row A j + m < dim_col A m_def n_def by force 
  also have "... = B$$(i+n, j+m)" using assms unfolding A_def B_def by simp
  also have "... = B2$$(i,j)" using ijeq
    by (metis A_def B_def i + n < dim_row A j + m < dim_col A 
        add_implies_diff assms(1) assms(2) assms(3) index_mat_four_block(1) 
        index_mat_four_block(2) index_mat_four_block(3) m_def n_def 
        not_add_less2)
  finally show "A2$$(i,j) = B2$$(i,j)" .
qed

lemma four_block_mat_real_diag:
  assumes "i < dim_row B1. B1$$(i,i)  Reals"
  and "i < dim_row B2. B2$$(i,i)  Reals"
  and "dim_row B1 = dim_col B1"
  and "dim_row B2 = dim_col B2"
  and "i < dim_row (four_block_diag B1 B2)"
shows "(four_block_diag B1 B2) $$ (i,i)  Reals" 
proof (cases "i < dim_row B1")
  case True  
  then show ?thesis using assms  by simp
next
  case False
  then show ?thesis using assms by force
qed

lemma four_block_diagonal:
  assumes "dim_row B1 = dim_col B1"
  and "dim_row B2 = dim_col B2"
  and "diagonal_mat B1"
  and "diagonal_mat B2"
shows "diagonal_mat (four_block_diag B1 B2)" unfolding diagonal_mat_def 
proof (intro allI impI)
  fix i j
  assume "i < dim_row (four_block_diag B1 B2)"
  and "j < dim_col (four_block_diag B1 B2)"
  and "i  j" note ijprops = this
  show "(four_block_diag B1 B2) $$ (i,j) = 0" 
  proof (cases "i < dim_row B1")
    case True
    then show ?thesis 
      using assms(3) diagonal_mat_def ijprops(2) ijprops(3)
      by (metis add_less_imp_less_left  
          ijprops(1) index_mat_four_block(1) index_mat_four_block(2) 
          index_mat_four_block(3) index_zero_mat(1) 
          linordered_semidom_class.add_diff_inverse) 
  next
    case False
    then show ?thesis using ijprops 
      by (metis (no_types, lifting) add_less_cancel_left assms(1) 
          assms(4) diagonal_mat_def index_mat_four_block(1) 
          index_mat_four_block(2) index_mat_four_block(3) 
          index_zero_mat(1) linordered_semidom_class.add_diff_inverse)
  qed
qed

lemma four_block_diag_zero:
  assumes "B carrier_mat 0 0"
  shows "four_block_diag A B = A"
proof (rule eq_matI, auto)
  show "dim_row B = 0" using assms by simp
  show "dim_col B = 0" using assms by simp
qed

lemma four_block_diag_zero':
  assumes "B carrier_mat 0 0"
  shows "four_block_diag B A = A"
proof (rule eq_matI)
  show "dim_row (four_block_diag B A) = dim_row A" using assms by simp
  show "dim_col (four_block_diag B A) = dim_col A" using assms by simp
  fix i j
  assume "i < dim_row A" and "j < dim_col A"
  thus "four_block_diag B A $$ (i, j) = A $$ (i, j)"
    using dim_col (four_block_diag B A) = dim_col A 
      dim_row (four_block_diag B A) = dim_row A 
  by auto
qed

lemma mult_four_block_diag:
  assumes "A1  carrier_mat nr1 n1" "D1  carrier_mat nr2 n2" 
  and "A2  carrier_mat n1 nc1" "D2  carrier_mat n2 nc2"
shows "four_block_diag A1 D1 * 
  four_block_diag A2  D2
  = four_block_diag (A1 * A2) (D1 * D2)" 
proof -
  define fb1 where "fb1 = four_block_mat A1 (0m nr1 n2) (0m nr2 n1) D1"
  define fb2 where "fb2 = four_block_mat A2 (0m n1 nc2) (0m n2 nc1) D2"
  have "fb1 * fb2 = four_block_mat (A1 * A2 + 0m nr1 n2 * 0m n2 nc1) 
    (A1 * 0m n1 nc2 + 0m nr1 n2 * D2) (0m nr2 n1 * A2 + D1 * 0m n2 nc1)
    (0m nr2 n1 * 0m n1 nc2 + D1 * D2)" unfolding fb1_def fb2_def
  proof (rule mult_four_block_mat)
    show "A1  carrier_mat nr1 n1" using assms by simp
    show "D1  carrier_mat nr2 n2" using assms by simp
    show "A2  carrier_mat n1 nc1" "D2  carrier_mat n2 nc2" using assms by auto
  qed auto  
  also have "... = four_block_mat (A1 * A2) (0m nr1 nc2) (0m nr2 nc1) (D1 * D2)" 
    using assms by simp
  finally show ?thesis unfolding fb1_def fb2_def  
    using assms by simp
qed

lemma four_block_diag_adjoint:
  shows  "(Complex_Matrix.adjoint (four_block_diag A1 A2)) = 
    (four_block_diag (Complex_Matrix.adjoint A1) 
    (Complex_Matrix.adjoint A2))" 
    by (rule eq_matI, 
        auto simp: four_block_mat_adjoint zero_adjoint adjoint_eval)

lemma four_block_diag_unitary:
  assumes "unitary U1"
  and "unitary U2"
shows "unitary
  (four_block_diag U1 U2)"
(is "unitary ?fU")
  unfolding unitary_def
proof
  show "?fU  carrier_mat (dim_row ?fU) (dim_row ?fU)" 
    by (metis Complex_Matrix.unitary_def assms(1) assms(2) 
        four_block_carrier_mat index_mat_four_block(2))
  define n where "n = dim_row ?fU"
  show "inverts_mat ?fU (Complex_Matrix.adjoint ?fU)"
  proof -
    have "(Complex_Matrix.adjoint ?fU) = 
      (four_block_mat (Complex_Matrix.adjoint U1) 
      (0m (dim_col U1) (dim_row U2)) 
      (0m (dim_col U2) (dim_row U1)) 
      (Complex_Matrix.adjoint U2))" 
      by (rule eq_matI, 
          auto simp: four_block_mat_adjoint zero_adjoint adjoint_eval)
    hence "?fU * (Complex_Matrix.adjoint ?fU) = 
      ?fU * (four_block_diag (Complex_Matrix.adjoint U1) 
      (Complex_Matrix.adjoint U2))"  by simp
    also have "... = four_block_diag
      (U1 * (Complex_Matrix.adjoint U1))
      (U2 * (Complex_Matrix.adjoint U2))"
      by (rule mult_four_block_diag, (auto simp add: assms))
    also have "... = four_block_mat
      (1m (dim_row U1))
      (0m (dim_row U1)  (dim_row U2))
      (0m (dim_row U2)  (dim_row U1))
      (1m (dim_row U2))" using assms 
      unfolding unitary_def inverts_mat_def 
      by simp
    also have "... = 1m (dim_row U1 + dim_row U2)" by simp
    finally show ?thesis unfolding inverts_mat_def  by simp
  qed
qed

lemma four_block_diag_similar:
  assumes "unitarily_equiv A1 B1 U1"
  and "unitarily_equiv A2 B2 U2"
  and "dim_row A1 = dim_col A1"
  and "dim_row A2 = dim_col A2"
shows "similar_mat_wit 
  (four_block_diag A1 A2)
  (four_block_diag B1 B2)
  (four_block_diag U1 U2)
  (Complex_Matrix.adjoint (four_block_diag U1 U2))"
  unfolding similar_mat_wit_def
proof (simp add: Let_def, intro conjI)
  define n where "n = dim_row A1 + dim_row A2"
  show "four_block_diag A1 A2  carrier_mat n n" unfolding n_def using assms 
    by auto
  show "four_block_diag B1 B2  carrier_mat n n" unfolding n_def using assms
    by (metis carrier_matI four_block_carrier_mat unitarily_equiv_carrier(1))
  show u: "four_block_diag U1 U2  carrier_mat n n" unfolding n_def using assms
    by (metis carrier_matI four_block_carrier_mat unitarily_equiv_carrier(2))
  thus cu: "Complex_Matrix.adjoint (four_block_diag U1 U2)  carrier_mat n n" 
    unfolding n_def using adjoint_dim' by blast
  show "four_block_diag U1 U2*Complex_Matrix.adjoint (four_block_diag U1 U2) =
    1m n" unfolding n_def
    using u assms four_block_diag_unitary n_def 
      unitarily_equiv_def unitary_simps(2) by blast
  thus "Complex_Matrix.adjoint (four_block_diag U1 U2)*four_block_diag U1 U2 = 
    1m n"
    using cu mat_mult_left_right_inverse u by blast 
  have "four_block_diag A1 A2 = 
    four_block_diag (U1 * B1 * (Complex_Matrix.adjoint U1))
    (U2 * B2 * (Complex_Matrix.adjoint U2))"
    using assms unitarily_equiv_eq by blast
  also have "... = (four_block_diag (U1*B1) (U2*B2)) *
    (four_block_diag (Complex_Matrix.adjoint U1)
    (Complex_Matrix.adjoint U2))"  
  proof (rule mult_four_block_diag[symmetric])
    show "U1 * B1  carrier_mat (dim_row A1) (dim_row A1)"
      by (metis assms(1) assms(3) carrier_mat_triv mult_carrier_mat 
          unitarily_equiv_carrier(1) unitarily_equiv_carrier(2))
    show "U2 * B2  carrier_mat (dim_row A2) (dim_row A2)"
      by (metis assms(2) assms(4) carrier_mat_triv mult_carrier_mat 
          unitarily_equiv_carrier(1) unitarily_equiv_carrier(2))
    show "Complex_Matrix.adjoint U1  carrier_mat (dim_row A1) (dim_row A1)"
      by (metis Complex_Matrix.unitary_def adjoint_dim assms(1) 
          index_mult_mat(2) unitarily_equivD(1) unitarily_equiv_eq)
    show "Complex_Matrix.adjoint U2  carrier_mat (dim_row A2) (dim_row A2)"
      by (meson assms(2) carrier_mat_triv similar_mat_witD2(7) 
          unitarily_equiv_def)
  qed
  also have "... = four_block_diag U1 U2 * four_block_diag B1 B2 * 
    Complex_Matrix.adjoint (four_block_diag U1 U2)"
  proof -
    have "four_block_diag (U1*B1) (U2*B2) = 
      four_block_diag U1 U2 * four_block_diag B1 B2" 
    proof (rule mult_four_block_diag[symmetric])
      show "U1  carrier_mat (dim_row A1) (dim_row A1)"
        by (metis assms(1) assms(3) carrier_mat_triv 
            unitarily_equiv_carrier(2))
      show "B1  carrier_mat (dim_row A1) (dim_row A1)"
        by (metis assms(1) assms(3) carrier_mat_triv 
            unitarily_equiv_carrier(1))
      show "U2  carrier_mat (dim_row A2) (dim_row A2)"
        by (metis assms(2) assms(4) carrier_mat_triv 
            unitarily_equiv_carrier(2))
      show "B2  carrier_mat (dim_row A2) (dim_row A2)"
        by (metis assms(2) assms(4) carrier_mat_triv 
            unitarily_equiv_carrier(1))
    qed
    moreover have "four_block_diag (Complex_Matrix.adjoint U1)
     (Complex_Matrix.adjoint U2) = 
      Complex_Matrix.adjoint (four_block_diag U1 U2)" 
      by (rule four_block_diag_adjoint[symmetric])
    ultimately show ?thesis by simp
  qed
  finally show "four_block_diag A1 A2 = 
    four_block_diag U1 U2 * four_block_diag B1 B2 * 
    Complex_Matrix.adjoint (four_block_diag U1 U2)" .
qed

lemma four_block_unitarily_equiv:
  assumes "unitarily_equiv A1 B1 U1"
  and "unitarily_equiv A2 B2 U2"
  and "dim_row A1 = dim_col A1"
  and "dim_row A2 = dim_col A2"
shows "unitarily_equiv 
  (four_block_diag A1 A2)
  (four_block_diag B1 B2)
  (four_block_diag U1 U2)"
(is "unitarily_equiv ?fA ?fB ?fU")
  unfolding unitarily_equiv_def
proof 
  show "unitary ?fU" using four_block_diag_unitary assms unitarily_equivD(1) 
    by blast  
  show "similar_mat_wit ?fA ?fB ?fU (Complex_Matrix.adjoint ?fU)" 
    using assms four_block_diag_similar[of A1] by simp
qed

lemma four_block_unitary_diag:
  assumes "unitary_diag A1 B1 U1"
  and "unitary_diag A2 B2 U2"
  and "dim_row A1 = dim_col A1"
  and "dim_row A2 = dim_col A2"
shows "unitary_diag 
  (four_block_diag A1 A2)
  (four_block_diag B1 B2)
  (four_block_diag U1 U2)"
(is "unitary_diag ?fA ?fB ?fU")
  unfolding unitary_diag_def
proof
  show "unitarily_equiv ?fA ?fB ?fU" 
    using four_block_unitarily_equiv[of A1] assms by simp
  have "dim_row B1 = dim_col B1" unfolding unitary_diag_def
    by (metis assms(1) assms(3) carrier_matD(1) carrier_matD(2) 
          carrier_mat_triv unitary_diag_carrier(1))
  moreover have "dim_row B2 = dim_col B2"  unfolding unitary_diag_def
    by (metis assms(2) assms(4) carrier_matD(1) carrier_matD(2) 
        carrier_mat_triv unitary_diag_carrier(1))
  ultimately show "diagonal_mat ?fB" using four_block_diagonal assms 
    unfolding unitary_diag_def by blast
qed

lemma four_block_real_diag_decomp:
  assumes "real_diag_decomp A1 B1 U1"
  and "real_diag_decomp A2 B2 U2"
  and "dim_row A1 = dim_col A1"
  and "dim_row A2 = dim_col A2"
shows "real_diag_decomp 
  (four_block_diag A1 A2)
  (four_block_diag B1 B2)
  (four_block_diag U1 U2)"
(is "real_diag_decomp ?fA ?fB ?fU")
  unfolding real_diag_decomp_def
proof (intro conjI allI impI)
  show "unitary_diag ?fA ?fB ?fU" using four_block_unitary_diag assms 
    unfolding real_diag_decomp_def by blast
  fix i
  assume "i < dim_row ?fB" 
  show "?fB $$ (i,i)  Reals" 
  proof (rule four_block_mat_real_diag)
    show "i < dim_row ?fB" using i < dim_row ?fB .
    show "i<dim_row B1. B1 $$ (i, i)  " using assms 
      unfolding real_diag_decomp_def by simp
    show "i<dim_row B2. B2 $$ (i, i)  " using assms 
      unfolding real_diag_decomp_def by simp
    show "dim_row B1 = dim_col B1"  unfolding unitary_diag_def
      by (metis assms(1) assms(3) carrier_matD(1) carrier_matD(2) 
          carrier_mat_triv real_diag_decompD(1) unitary_diag_carrier(1))
    show "dim_row B2 = dim_col B2"  unfolding unitary_diag_def
      by (metis assms(2) assms(4) carrier_matD(1) carrier_matD(2) 
          carrier_mat_triv real_diag_decompD(1) unitary_diag_carrier(1))
  qed
qed

lemma diag_block_mat_mult:
  assumes "length Al = length Bl"
  and "i < length Al. dim_col (Al!i) = dim_row (Bl!i)"
shows "diag_block_mat Al * (diag_block_mat Bl) = 
  (diag_block_mat (map2 (*) Al Bl))" using assms
proof (induct Al arbitrary: Bl)
  case Nil
  then show ?case by simp
next
  case (Cons a Al)
  define A where "A = diag_block_mat Al"
  define B where "B = diag_block_mat (tl Bl)"
  have "0 < length Bl" using Cons by auto
  hence "Bl = hd Bl # (tl Bl)" by simp
  have "length (tl Bl) = length Al" using Cons by simp
  have dim: "i<length Al. dim_col (Al ! i) = dim_row (tl Bl ! i)"
  proof (intro allI impI)
    fix i
    assume "i < length Al"
    hence "dim_col (Al ! i) = dim_col ((a#Al)!(Suc i))" by simp
    also have "... = dim_row (Bl!(Suc i))" using Cons
      by (metis Suc_lessI i < length Al length_Cons less_Suc_eq)
    also have "... = dim_row (tl Bl!i)"
      by (metis Bl = hd Bl # tl Bl nth_Cons_Suc) 
    finally show "dim_col (Al ! i) = dim_row (tl Bl!i)" .
  qed
  define C where "C = map2 (*) (a # Al) Bl"
  have "hd C = a * hd Bl" using Bl = hd Bl # tl Bl unfolding C_def
    by (metis list.map(2) list.sel(1) prod.simps(2) zip_Cons_Cons)
  have "tl C = map2 (*) Al (tl Bl)"
    by (metis (no_types, lifting) C_def Bl = hd Bl # tl Bl list.sel(3) 
        map_tl zip_Cons_Cons)
  have "C = hd C # (tl C)" unfolding C_def
    by (metis Nil_eq_zip_iff Nil_is_map_conv Bl = hd Bl # tl Bl 
        list.exhaust_sel list.simps(3))
  have "dim_row B = sum_list (map dim_row (tl Bl))" unfolding B_def
    by (simp add: dim_diag_block_mat(1))
  also have "... = sum_list (map dim_col Al)" 
  proof (rule sum_list_cong)
    show "length (map dim_row (tl Bl)) = length (map dim_col Al)"  
      using  length (tl Bl) = length Al by simp
    show "i<length (map dim_row (tl Bl)). 
      map dim_row (tl Bl) ! i = map dim_col Al ! i"
      by (metis length (tl Bl) = length Al dim length_map nth_map)
  qed
  also have "... = dim_col A" unfolding A_def
    by (simp add: dim_diag_block_mat(2))
  finally have ba: "dim_row B = dim_col A" .  
  have "diag_block_mat (a#Al) * (diag_block_mat Bl) = 
    four_block_diag a A * (four_block_diag (hd Bl) B)" 
    using diag_block_mat.simps(2) Bl = hd Bl # (tl Bl) 
    unfolding Let_def A_def B_def by metis
  also have "... = four_block_diag (a * hd Bl) (A * B)"     
  proof (rule mult_four_block_diag)
    show "a carrier_mat (dim_row a) (dim_col a)" by simp 
    show "hd Bl  carrier_mat (dim_col a) (dim_col (hd Bl))"
      using Cons
      by (metis 0 < length Bl Bl = hd Bl # tl Bl carrier_mat_triv nth_Cons_0)
    show "A  carrier_mat (dim_row A) (dim_col A)" by simp
    show " B  carrier_mat (dim_col A) (dim_col B)" using ba by auto
  qed
  also have "... = four_block_diag (hd C) (diag_block_mat (tl C))" 
    unfolding A_def B_def 
    using C_def hd C = a * hd Bl length (tl Bl) = length Al 
      tl C = map2 (*) Al (tl Bl) dim local.Cons(1) 
    by presburger
  also have "... = diag_block_mat C" 
    using C = hd C#(tl C) diag_block_mat.simps(2) unfolding Let_def by metis
  finally show ?case unfolding C_def .
qed

lemma real_diag_decomp_block:
  fixes Al::"complex Matrix.mat list"
  assumes "Al  []"
  and "list_all (λA. 0 < dim_row A  hermitian A)  Al"
shows " Bl Ul. length Ul = length Al 
  (i < length Al. 
    Ul!i  carrier_mat (dim_row (Al!i)) (dim_col (Al!i))  unitary (Ul!i) 
    Bl!i  carrier_mat (dim_row (Al!i)) (dim_col (Al!i))) 
  real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul)"
  using assms
proof (induct Al)
  case Nil
  then show ?case by simp
next
  case (Cons A Al)
  hence "hermitian A" "0 < dim_row A" by auto
  hence "A  carrier_mat (dim_row A) (dim_row A)"
    by (simp add: hermitian_square)
  from this obtain B U where r: "real_diag_decomp A B U" 
    using hermitian_real_diag_decomp hermitian A 0 < dim_row A by blast
  have bcar: "B  carrier_mat (dim_row A) (dim_col A)" 
      using real_diag_decompD(1)
      by (metis A  carrier_mat (dim_row A) (dim_row A) carrier_matD(2) r 
          unitary_diag_carrier(1))
    have ucar: "U  carrier_mat (dim_row A) (dim_col A)" 
      using real_diag_decompD(1)
      by (metis A  carrier_mat (dim_row A) (dim_row A) carrier_matD(2) r 
          unitary_diag_carrier(2))
    have unit: "unitary U"
      by (meson r real_diag_decompD(1) unitary_diagD(3))
  show ?case
  proof (cases "Al = []")
    case True
    hence "diag_block_mat (Cons A Al) = A" by auto
    moreover have "diag_block_mat [B] = B" by auto
    moreover have "diag_block_mat [U] = U" by auto
    moreover have "unitary U"
      using r real_diag_decompD(1) unitary_diagD(3) by blast
    ultimately have 
      "real_diag_decomp (diag_block_mat (Cons A Al)) 
        (diag_block_mat [B]) (diag_block_mat [U])"
      using real_diag_decomp A B U by auto
    moreover have "(i<length (A # Al).
      [U]!i  carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)) 
      Complex_Matrix.unitary ([U] ! i)  [B] ! i  
      carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)))" using True
      by (simp add: bcar ucar unit)
    ultimately show ?thesis 
      using True Complex_Matrix.unitary U bcar  less_one ucar
      by (metis length_list_update list_update_code(2))
  next
    case False
    have "list_all (λA. 0 < dim_row A  hermitian A) Al" using Cons by auto
    hence "Bl Ul. length Ul = length Al 
       (i<length Al.
           Ul ! i  carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))  
           unitary (Ul!i)  
            Bl ! i  carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))) 
       real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul)"
      using Cons False by simp 
    from this obtain Bl Ul where "length Ul  =length Al" and  
      rl: "real_diag_decomp (diag_block_mat Al) 
      (diag_block_mat Bl) (diag_block_mat Ul)"
      and "i<length Al.
           Ul ! i  carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))  
            unitary (Ul!i)  
            Bl ! i  carrier_mat (dim_row (Al ! i)) (dim_col (Al ! i))"
      by auto note bu = this
    have "real_diag_decomp (diag_block_mat (A # Al)) 
      (diag_block_mat (B # Bl)) (diag_block_mat (U # Ul))" 
      using four_block_real_diag_decomp[OF r rl] 
      by (metis A  carrier_mat (dim_row A) (dim_row A) 
          carrier_matD(2) diag_block_mat.simps(2) hermitian_square 
          real_diag_decomp_hermitian rl)
    moreover have "length (U#Ul) = length (A#Al)" using bu by simp
    moreover have "i<length (A # Al).
           (U#Ul) ! i  carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i)) 
           unitary ((U#Ul)!i) 
           (B#Bl) ! i  carrier_mat (dim_row ((A # Al) ! i)) (dim_col ((A # Al) ! i))" 
    proof (intro allI impI)
      fix i
      assume "i < length (A#Al)"
      show "(U # Ul) ! i  carrier_mat (dim_row ((A # Al) ! i)) 
        (dim_col ((A # Al) ! i))  unitary ((U#Ul)!i) 
        (B # Bl) ! i  carrier_mat (dim_row ((A # Al) ! i)) 
        (dim_col ((A # Al) ! i))"
      proof (cases "i = 0")
        case True
        then show ?thesis by (simp add: bcar ucar unit) 
      next
        case False
        hence "j. i = Suc j" by (simp add: not0_implies_Suc)
        from this obtain j where j: "i = Suc j" by auto
        hence "j < length Al" using i < length (A#Al) by simp
        have "(A#Al)!i = Al!j" "(U # Ul) ! i = Ul!j" "(B#Bl) ! i = Bl!j" 
          using j by auto
        then show ?thesis using Cons j < length Al bu(3) by presburger
      qed
    qed
    ultimately show ?thesis by blast
  qed
qed

lemma diag_block_mat_adjoint:
  shows "Complex_Matrix.adjoint (diag_block_mat Al) =
    diag_block_mat (map Complex_Matrix.adjoint Al)"
proof (induct Al)
  case Nil
  then show ?case using zero_adjoint by simp
next
  case (Cons a Al)
  have "Complex_Matrix.adjoint (diag_block_mat (a # Al)) =
    Complex_Matrix.adjoint (four_block_diag a (diag_block_mat Al))" 
    using diag_block_mat.simps(2)[of a] unfolding Let_def by simp
  also have "... = four_block_diag (Complex_Matrix.adjoint a)
    (Complex_Matrix.adjoint (diag_block_mat Al))" 
    using four_block_diag_adjoint[of a] by simp
  also have "... = four_block_diag (Complex_Matrix.adjoint a)
    (diag_block_mat (map Complex_Matrix.adjoint Al))" using Cons by simp
  also have "... = diag_block_mat (map Complex_Matrix.adjoint (a#Al))" 
    using diag_block_mat.simps(2) unfolding Let_def 
    by (metis (no_types) diag_block_mat.simps(2) list.map(2))
  finally show ?case .
qed

lemma diag_block_mat_mat_conj:
  assumes "length Al = length Bl"
  and "i < length Al. dim_col (Al!i) = dim_row (Bl!i)"
  and "i < length Al. dim_row (Bl!i) = dim_col (Bl!i)"
  shows "mat_conj (diag_block_mat Al) (diag_block_mat Bl) =
    diag_block_mat (map2 mat_conj Al Bl)"
proof -
  have "mat_conj (diag_block_mat Al) (diag_block_mat Bl) =
    diag_block_mat Al * diag_block_mat Bl * 
    diag_block_mat (map Complex_Matrix.adjoint Al)" 
    using diag_block_mat_adjoint[of Al] unfolding mat_conj_def by simp
  also have "... = diag_block_mat (map2 (*) Al Bl) * 
    diag_block_mat (map Complex_Matrix.adjoint Al)" 
    using diag_block_mat_mult[OF assms(1) assms(2)] by simp
  also have "... = diag_block_mat (map2 (*) (map2 (*) Al Bl)
    (map Complex_Matrix.adjoint Al))"
  proof (rule diag_block_mat_mult)
    show "length (map2 (*) Al Bl) = length (map Complex_Matrix.adjoint Al)"
      by (simp add: assms(1))
    show "i<length (map2 (*) Al Bl). dim_col (map2 (*) Al Bl ! i) = 
      dim_row (map Complex_Matrix.adjoint Al ! i)"
      by (simp add: assms(2) assms(3))
  qed
  also have "... = diag_block_mat (map2 mat_conj Al Bl)" 
    using map2_mat_conj_exp[OF assms(1)] by simp
  finally show ?thesis .
qed

lemma diag_block_mat_commute:
  assumes "length Al = length Bl"
  and "i < length Al. Al!i * (Bl!i) = Bl!i * (Al!i)"
  and "i<length Al. dim_col (Al ! i) = dim_row (Bl ! i)"
  and "i<length Al. dim_col (Bl ! i) = dim_row (Al ! i)"
shows "diag_block_mat Al * (diag_block_mat Bl) = 
  diag_block_mat Bl * (diag_block_mat Al)"
proof -
  have "diag_block_mat Al * diag_block_mat Bl =
    diag_block_mat (map2 (*) Al Bl)" 
    using diag_block_mat_mult[of Al Bl] assms by simp
  also have "... = diag_block_mat (map2 (*) Bl Al)" 
  proof -
    have "map2 (*) Al Bl = map2 (*) Bl Al"     
      by (rule map2_commute, auto simp add: assms)
    thus ?thesis by simp
  qed
  also have "... = diag_block_mat Bl * (diag_block_mat Al)"
    using diag_block_mat_mult[of Bl Al] assms by simp
  finally show ?thesis .
qed

lemma diag_block_mat_length_1:
  assumes "length Al = 1"
  shows "diag_block_mat Al = Al!0" 
proof -
  have "Al = [Al!0]" using assms
    by (metis One_nat_def length_0_conv length_Suc_conv nth_Cons_0)
  thus ?thesis
    by (metis diag_block_mat_singleton) 
qed

lemma diag_block_mat_cong_hd:
  assumes "0 < length Al"
  and "length Al = length Bl"
  and "dim_row (hd Al) = dim_row (hd Bl)"
  and "dim_col (hd Al) = dim_col (hd Bl)"
  and "diag_block_mat Al = diag_block_mat Bl"
shows "hd Al = hd Bl" 
proof -
  have "Al  []" using assms by blast
  hence "Al = hd Al#(tl Al)" by simp
  hence da:"diag_block_mat Al = 
    four_block_diag (hd Al) (diag_block_mat (tl Al))"
    using diag_block_mat.simps(2)[of "hd Al" "tl Al"] unfolding Let_def by simp
  have  "Bl  []" using assms by simp
  hence "Bl = hd Bl#(tl Bl)" by simp
  hence "diag_block_mat Bl = four_block_diag (hd Bl) (diag_block_mat (tl Bl))"
    using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] unfolding Let_def by simp
  hence "four_block_diag (hd Al) (diag_block_mat (tl Al)) = 
    four_block_diag (hd Bl) (diag_block_mat (tl Bl))" using da assms by simp
  thus ?thesis using four_block_diag_cong_comp assms by metis
qed

lemma diag_block_mat_cong_tl:
  assumes "0 < length Al"
  and "length Al = length Bl"
  and "dim_row (hd Al) = dim_row (hd Bl)"
  and "dim_col (hd Al) = dim_col (hd Bl)"
  and "diag_block_mat Al = diag_block_mat Bl"
shows "diag_block_mat (tl Al) = diag_block_mat (tl Bl)" 
proof -
  have "Al  []" using assms by blast
  hence "Al = hd Al#(tl Al)" by simp
  hence da:"diag_block_mat Al = 
    four_block_diag (hd Al) (diag_block_mat (tl Al))"
    using diag_block_mat.simps(2)[of "hd Al" "tl Al"] unfolding Let_def by simp
  have  "Bl  []" using assms by simp
  hence "Bl = hd Bl#(tl Bl)" by simp
  hence "diag_block_mat Bl = four_block_diag (hd Bl) (diag_block_mat (tl Bl))"
    using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] unfolding Let_def by simp
  hence "four_block_diag (hd Al) (diag_block_mat (tl Al)) = 
    four_block_diag (hd Bl) (diag_block_mat (tl Bl))" using da assms by simp
  thus ?thesis using four_block_diag_cong_comp' assms by metis
qed

lemma diag_block_mat_cong_comp:
  assumes "length Al = length Bl"
  and "i<length Al. dim_row (Al ! i) = dim_row (Bl ! i)"
  and "i<length Al. dim_col (Al ! i) = dim_col (Bl ! i)"
  and "diag_block_mat Al = diag_block_mat Bl"
and "j < length Al"
shows "Al!j = Bl!j" using assms
proof (induct Al arbitrary: Bl j)
  case Nil
  then show ?case by simp
next
  case (Cons a Al)
  hence "0 <length Bl" by linarith
  hence "Bl = hd Bl#(tl Bl)" by simp
  then show ?case 
  proof (cases "j = 0")
    case True
    hence "(a#Al)!j = hd(a#Al)" by simp
    have "Bl!j= hd Bl" using j = 0
      by (metis Bl = hd Bl # tl Bl nth_Cons_0)
    have da: "diag_block_mat (a#Al) = four_block_diag a (diag_block_mat Al)"
      using diag_block_mat.simps(2)[of a Al] unfolding Let_def by simp
    have db: "diag_block_mat (hd Bl#(tl Bl)) = 
      four_block_diag (hd Bl) (diag_block_mat (tl Bl))"
      using diag_block_mat.simps(2)[of "hd Bl" "tl Bl"] 
      unfolding Let_def by simp
    have "hd (a#Al) = hd Bl"
    proof (rule diag_block_mat_cong_hd)
      show "0 < length (a # Al)" by simp
      show "length (a # Al) = length Bl" using Cons by simp
      show "diag_block_mat (a # Al) = diag_block_mat Bl" using Cons by simp
      show "dim_row (hd (a # Al)) = dim_row (hd Bl)"
        by (metis True 0 < length Bl Bl ! j = hd Bl list.sel(1) Cons(2) 
            Cons(3) nth_Cons_0)
      show "dim_col (hd (a # Al)) = dim_col (hd Bl)"
        by (metis True 0 < length Bl Bl ! j = hd Bl list.sel(1) Cons(2) 
            Cons(4) nth_Cons_0)
    qed
    thus "(a # Al) ! j = Bl ! j" using j = 0 Bl ! j = hd Bl by fastforce
  next
    case False
    hence "k. j = Suc k" by (simp add: not0_implies_Suc) 
    from this obtain k where "j = Suc k" by auto
    hence "(a#Al)!j = Al!k" by simp
    have "Bl!j = (tl Bl)!k" using j = Suc k Bl = hd Bl#(tl Bl)
      by (metis nth_Cons_Suc)
    have "Al!k = (tl Bl)!k"
    proof (rule Cons(1))
      show "length Al = length (tl Bl)" using Cons
        by (metis diff_Suc_1 length_Cons length_tl)
      show "k < length Al"
        by (metis Cons.prems(5) Suc_less_SucD j = Suc k length_Cons) 
      show "i<length Al. dim_row (Al ! i) = dim_row (tl Bl ! i)"
        by (metis Suc_less_eq length Al = length (tl Bl) length_Cons 
            local.Cons(3) nth_Cons_Suc nth_tl)
      show "i<length Al. dim_col (Al ! i) = dim_col (tl Bl ! i)"
        by (metis Suc_mono Bl = hd Bl # tl Bl length_Cons local.Cons(4) 
            nth_Cons_Suc)
      have "diag_block_mat (tl (a#Al)) = diag_block_mat (tl Bl)"
      proof (rule diag_block_mat_cong_tl)
        show "length (a # Al) = length Bl" using Cons by simp
        show "dim_row (hd (a # Al)) = dim_row (hd Bl)"
          by (metis Bl = hd Bl # tl Bl length_Cons list.sel(1) local.Cons(3) 
              nth_Cons_0 zero_less_Suc)
        show "dim_col (hd (a # Al)) = dim_col (hd Bl)"
          by (metis 0 < length Bl Bl = hd Bl # tl Bl list.sel(1) 
              local.Cons(2) local.Cons(4) nth_Cons_0)
        show "diag_block_mat (a # Al) = diag_block_mat Bl" using Cons by simp
        show "0 < length (a#Al)" by simp
      qed
      thus "diag_block_mat Al = diag_block_mat (tl Bl)" by simp
    qed
    then show ?thesis
      by (simp add: (a # Al) ! j = Al ! k Bl ! j = tl Bl ! k) 
  qed
qed

lemma diag_block_mat_commute_comp:
  assumes "length Al = length Bl"
  and "i<length Al. dim_row (Al ! i) = dim_col (Al ! i)"
  and "i<length Al. dim_row (Al ! i) = dim_row (Bl ! i)"
  and "i<length Al. dim_col (Al ! i) = dim_col (Bl ! i)"
  and "diag_block_mat Al * (diag_block_mat Bl) = 
    diag_block_mat Bl * (diag_block_mat Al)"
  and "i < length Al"
shows "Al!i * Bl!i = Bl!i * Al!i" 
proof -
  have "diag_block_mat (map2 (*) Al Bl)=diag_block_mat Al * diag_block_mat Bl"
    using diag_block_mat_mult[of Al] assms by simp
  also have "... = diag_block_mat Bl * diag_block_mat Al" using assms by simp
  also have "... = diag_block_mat (map2 (*) Bl Al)" 
    using diag_block_mat_mult[of Bl] assms by simp
  finally have eq: "diag_block_mat (map2 (*) Al Bl) = 
    diag_block_mat (map2 (*) Bl Al)" .
  have "(map2 (*) Al Bl)!i = (map2 (*) Bl Al)!i" 
  proof (rule diag_block_mat_cong_comp) 
    show "length (map2 (*) Al Bl) = length (map2 (*) Bl Al)" 
      using map2_length assms by metis
    show "i < length (map2 (*) Al Bl)" using map2_length assms by metis 
    show "diag_block_mat (map2 (*) Al Bl) = diag_block_mat (map2 (*) Bl Al)"
      using eq .
    show "i<length (map2 (*) Al Bl). dim_row (map2 (*) Al Bl ! i) = 
      dim_row (map2 (*) Bl Al ! i)"
      by (simp add: assms(3))
    show "i<length (map2 (*) Al Bl). dim_col (map2 (*) Al Bl ! i) = 
      dim_col (map2 (*) Bl Al ! i)"
      by (simp add: assms(4))
  qed
  moreover have "(map2 (*) Al Bl)!i = Al!i * Bl!i" using assms by simp
  moreover have "(map2 (*) Bl Al)!i = Bl!i * Al!i" using assms by simp
  ultimately show ?thesis by simp
qed

lemma diag_block_mat_dim_row_cong:
  assumes "length Ul = length Bl"
  and "i < length Bl. dim_row (Bl!i) = dim_row (Ul!i)"
  shows "dim_row (diag_block_mat Ul) = dim_row (diag_block_mat Bl)"
proof -
  have "dim_row (diag_block_mat Ul) = sum_list (map dim_row Ul)" 
    by (simp add: dim_diag_block_mat(1))
  also have "... = sum_list (map dim_row Bl)" using assms 
    by (metis nth_map_conv)
  also have "... = dim_row (diag_block_mat Bl)"
    by (simp add: dim_diag_block_mat(1))
  finally show ?thesis .
qed

lemma diag_block_mat_dim_col_cong:
  assumes "length Ul = length Bl"
  and "i < length Bl. dim_col (Bl!i) = dim_col (Ul!i)"
  shows "dim_col (diag_block_mat Ul) = dim_col (diag_block_mat Bl)"
proof -
  have "dim_col (diag_block_mat Ul) = sum_list (map dim_col Ul)" 
    by (simp add: dim_diag_block_mat(2))
  also have "... = sum_list (map dim_col Bl)" using assms 
    by (metis nth_map_conv)
  also have "... = dim_col (diag_block_mat Bl)"
    by (simp add: dim_diag_block_mat(2))
  finally show ?thesis .
qed

lemma diag_block_mat_dim_row_col_eq:
  assumes "i < length Al. dim_row (Al!i) = dim_col (Al!i)"
  shows "dim_row (diag_block_mat Al) = dim_col (diag_block_mat Al)"
proof -
  have "dim_row (diag_block_mat Al) = sum_list (map dim_row Al)"
    by (simp add:dim_diag_block_mat(1))
  also have "... = sum_list (map dim_col Al)" using assms
    by (metis nth_map_conv)
  also have "... = dim_col (diag_block_mat Al)"
    by (simp add:dim_diag_block_mat(2))
  finally show ?thesis .
qed

section ‹Block matrix decomposition›

subsection ‹Subdiagonal extraction›
text ‹\verb+extract_subdiags+ returns a list of diagonal sub-blocks, the sizes of which are
specified by the list of integers provided as parameters.›

fun extract_subdiags where
  "extract_subdiags B [] = []"
| "extract_subdiags B (x#xs) = 
    (let (B1, B2, B3, B4) = (split_block B x x) in 
      B1 # (extract_subdiags B4 xs))"

lemma extract_subdiags_not_emp:
  fixes x::nat and l::"nat list"
  assumes "(B1, B2, B3, B4) = (split_block B x x)"
  shows "hd (extract_subdiags B (x#l)) = B1" 
    "tl (extract_subdiags B (x#l)) = extract_subdiags B4 l" 
proof -
  show "hd (extract_subdiags B (x#l)) = B1" unfolding  Let_def 
    by (metis (no_types) assms extract_subdiags.simps(2) list.sel(1) split_conv) 
  show "tl (extract_subdiags B (x # l)) = extract_subdiags B4 l" 
    using assms extract_subdiags.simps(2) unfolding Let_def
    by (metis (no_types, lifting) list.sel(3) split_conv)
qed

lemma extract_subdiags_neq_Nil:
  shows "extract_subdiags B (a#l)  []" 
  using extract_subdiags.simps(2)[of B] 
  unfolding Let_def split_block_def by simp

lemma extract_subdiags_length:
  shows "length (extract_subdiags B l) = length l"
proof (induct l arbitrary: B)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  then show ?case using Cons extract_subdiags.simps(2)[of B a l] 
    unfolding Let_def by simp 
qed

lemma extract_subdiags_carrier:
  assumes "i < length l"
  shows "(extract_subdiags B l)!i  carrier_mat (l!i) (l!i)" using assms
proof (induct i arbitrary: l B)  
  case 0
  define B1 where "B1 = fst (split_block B (hd l) (hd l))"
  define B2 where "B2 = fst (snd (split_block B (hd l) (hd l)))"
  define B3 where "B3 = fst (snd (snd (split_block B (hd l) (hd l))))"
  define B4 where "B4 = snd (snd (snd (split_block B (hd l) (hd l))))"
  have sp: "split_block B (hd l) (hd l) = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  have "l = hd l # (tl l)" using 0 by auto
  have "(extract_subdiags B l)!0 = B1" 
    using extract_subdiags.simps(2)[of B "hd l" "tl l"] l = hd l # tl l sp
    unfolding Let_def by auto
  also have "...  carrier_mat (hd l) (hd l)" 
    unfolding B1_def split_block_def Let_def by simp
  finally show ?case
    by (metis l = hd l # tl l hd_conv_nth list.sel(2) not_Cons_self) 
next
  case (Suc i)  
  define B1 where "B1 = fst (split_block B (hd l) (hd l))"
  define B2 where "B2 = fst (snd (split_block B (hd l) (hd l)))"
  define B3 where "B3 = fst (snd (snd (split_block B (hd l) (hd l))))"
  define B4 where "B4 = snd (snd (snd (split_block B (hd l) (hd l))))"
  have sp: "split_block B (hd l) (hd l) = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  have "l = hd l # (tl l)" using Suc
    by (metis Cons_nth_drop_Suc drop_Nil list.exhaust_sel not_Cons_self)
  hence "l! Suc i = (tl l)!i" by (metis nth_Cons_Suc)
  have "tl (extract_subdiags B l) = extract_subdiags B4 (tl l)" 
    using extract_subdiags_not_emp(2)[OF sp[symmetric]] l = hd l # (tl l) 
    by metis
  hence "extract_subdiags B l = B1 # extract_subdiags B4 (tl l)" 
    using extract_subdiags_not_emp(1)[OF sp[symmetric]]
    by (metis l = hd l # tl l extract_subdiags_neq_Nil list.exhaust_sel)
  hence "extract_subdiags B l ! Suc i = (extract_subdiags B4 (tl l))!i" 
    using nth_Cons_Suc by simp
  also have "...  carrier_mat (tl l!i) (tl l!i)" using Suc
    by (metis l = hd l # tl l length_Cons not_less_eq)
  also have "... = carrier_mat (l!Suc i) (l! Suc i)" 
    using nth_Cons_Suc[of "hd l" "tl l" i] l = hd l # tl l by simp
  finally show ?case .
qed

lemma extract_subdiags_diagonal:
  assumes "diagonal_mat B"
  and "B  carrier_mat n n"
  and "l  []"
  and "sum_list l  n"
  and "i < length l"
shows "diagonal_mat ((extract_subdiags B l)!i)" using assms
proof (induct i arbitrary: l B n)
  case 0
  define a where "a = hd l"
  have "l = a#(tl l)" unfolding a_def using 0 by simp
  have "a  n" using 0 unfolding a_def
    by (metis a_def dual_order.strict_trans2 elem_le_sum_list 
        hd_conv_nth less_le_not_le nat_le_linear)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  hence "extract_subdiags B l!0 = B1" unfolding a_def 
    using hd_conv_nth 0 
    by (metis l = a # tl l sp extract_subdiags_neq_Nil 
        extract_subdiags_not_emp(1))
  moreover have "diagonal_mat B1" using sp split_block_diagonal assms a  n 0
    by blast
  ultimately show ?case by simp
next
  case (Suc i)
  show ?case
  proof (cases "length l = 1")
    case True
    hence "Suc i = 0" using Suc by presburger
    then show ?thesis by simp
  next
    case False
    define a where "a = hd l"
    have "l = a#(tl l)" unfolding a_def using Suc by simp
    have "a  n" using Suc unfolding a_def
      by (metis dual_order.trans elem_le_sum_list hd_conv_nth 
          length_greater_0_conv)
    define B1 where "B1 = fst (split_block B a a)"
    define B2 where "B2 = fst (snd (split_block B a a))"
    define B3 where "B3 = fst (snd (snd (split_block B a a)))"
    define B4 where "B4 = snd (snd (snd (split_block B a a)))"
    have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
      unfolding B1_def B2_def B3_def B4_def by simp
    have "extract_subdiags B l ! Suc i = 
      extract_subdiags B4 (tl l)! i"  using sp
      by (metis Suc(6) Suc_less_SucD l = a # tl l length_Cons nth_tl 
          extract_subdiags_length extract_subdiags_not_emp(2))
    moreover have "diagonal_mat (extract_subdiags B4 (tl l)! i)"
    proof (rule Suc(1))
      show "tl l  []" using False Suc
        by (metis l = a # tl l length_Cons list.size(3) numeral_nat(7)) 
      show "i < length (tl l)" using False Suc
        by (metis Suc_lessD l = a # tl l le_neq_implies_less length_Cons 
            less_Suc_eq_le)
      show "B4  carrier_mat (n-a) (n-a)" 
        using sp split_block_diag_carrier(2) Suc(3) a  n by blast 
      show "diagonal_mat B4" 
        using split_block_diagonal sp Suc a  n by blast
      show "sum_list (tl l)  n - a" using Suc(5) a  n sum_list_tl_leq
        by (simp add: Suc(4) a_def)
    qed
    ultimately show ?thesis by simp
  qed
qed

lemma extract_subdiags_diag_elem:
  fixes B::"complex Matrix.mat"
  assumes "B carrier_mat n n"
  and "0 < n"
  and "l  []"
  and "i < length l"
  and "j< l!i"
  and "sum_list l  n"
  and "j < length l. 0 < l!j"
  shows "extract_subdiags B l!i $$ (j,j) = 
    diag_mat B!(n_sum i l + j)" using assms
proof (induct i arbitrary: l B n)
  case 0
  define a where "a = hd l"
  have "l = a#(tl l)" unfolding a_def using 0 by simp
  have "a  n" using 0 unfolding a_def
    by (metis a_def dual_order.strict_trans2 elem_le_sum_list 
        hd_conv_nth less_le_not_le nat_le_linear)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  hence "extract_subdiags B l!0 = B1" 
    using  hd_conv_nth unfolding Let_def 
    by (metis l = a # tl l extract_subdiags_neq_Nil 
        extract_subdiags_not_emp(1))
  hence "extract_subdiags B l!0 $$ (j,j) = B$$ (j,j)" 
    using sp 0 unfolding split_block_def
    by (metis (no_types, lifting) carrier_matD(2) dim_col_mat(1) 
        index_mat(1) prod.sel(1) extract_subdiags_carrier)
  also have "... = diag_mat B!j" 
    using 0 a  n hd_conv_nth unfolding diag_mat_def a_def
    by fastforce
  also have "... = diag_mat B!(n_sum 0 l + j)" by simp
  finally show ?case .
next
  case (Suc i)
  show ?case
  proof (cases "length l = 1")
    case True
    hence "Suc i < 0" using Suc by simp
    then show ?thesis by simp
  next
    case False
    hence "1 < length l" using Suc by presburger
    define a where "a = hd l"
    have "l = a#(tl l)" unfolding a_def using Suc by simp
    have "a  n" using Suc unfolding a_def
      by (metis add_le_same_cancel1 elem_le_sum_list hd_conv_nth 
          le_add2 le_trans verit_comp_simplify1(3))
    define B1 where "B1 = fst (split_block B a a)"
    define B2 where "B2 = fst (snd (split_block B a a))"
    define B3 where "B3 = fst (snd (snd (split_block B a a)))"
    define B4 where "B4 = snd (snd (snd (split_block B a a)))"
    have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
      unfolding B1_def B2_def B3_def B4_def by simp
    have "B4  carrier_mat (n-a) (n-a)" 
      using sp split_block_diag_carrier(2) Suc a  n by blast
    have "B1  carrier_mat a a" 
      using sp split_block_diag_carrier(1) Suc a  n by blast
    have "n_sum (Suc i) l + j < n_sum (Suc (Suc i)) l" 
      using Suc  n_sum_last_lt by metis
    hence "a + n_sum i (tl l) + j < n_sum (Suc (Suc i)) l" 
      unfolding a_def by simp
    also have "...  sum_list l"
    proof (rule n_sum_sum_list)
      show "j<length l. 0  l ! j" using Suc by simp
      show "Suc (Suc i)  length l" using Suc by simp
    qed
    also have "...  n" using Suc by simp
    finally have "a + n_sum i (tl l) + j < n" .
    hence "n_sum i (tl l) +j < n - a" by simp
    have "extract_subdiags B l!(Suc i) = 
      extract_subdiags B4 (tl l)!i" 
      using sp l = a#(tl l) unfolding  Let_def 
      by (metis list.exhaust_sel nth_Cons_Suc extract_subdiags_neq_Nil 
          extract_subdiags_not_emp(2))
    hence "extract_subdiags B l!(Suc i) $$(j,j) = 
      extract_subdiags B4 (tl l)!i $$(j,j)" by simp
    also have "... = diag_mat B4!(n_sum i (tl l) + j)" 
    proof (rule Suc(1))
      show "tl l  []" using False Suc
        by (metis l = a # tl l length_Cons list.size(3) numeral_nat(7)) 
      show "i < length (tl l)" using False Suc
        by (metis Suc_lessD l = a # tl l le_neq_implies_less length_Cons 
            less_Suc_eq_le)
      show "B4  carrier_mat (n-a) (n-a)" 
        using B4  carrier_mat (n-a) (n-a) .
      show "sum_list (tl l)  n - a" using Suc(5) a  n sum_list_tl_leq
        by (simp add: Suc a_def)
      show "0 < n - a"
        by (metis Suc.prems(4) Suc.prems(7) i < length (tl l) 
            l = a # tl l sum_list (tl l)  n - a bot_nat_0.extremum_uniqueI
            elem_le_sum_list gr_zeroI nth_Cons_Suc)
      show "j<length (tl l). 0 < tl l ! j"
        by (simp add: Suc(8) nth_tl)
      show "j < tl l ! i"
        by (metis Suc(6) i < length (tl l) nth_tl)
    qed
    also have "... = B4$$(n_sum i (tl l)+j, n_sum i (tl l)+j)" 
    proof -
      have "n_sum i (tl l) +j < n - a" using n_sum i (tl l) +j < n - a .
      thus ?thesis 
        using B4  carrier_mat (n-a) (n-a)  
        unfolding diag_mat_def by simp
    qed
    also have "... = B$$(n_sum i (tl l) + j + a, n_sum i (tl l) + j + a)" 
      using sp B1  carrier_mat a a n_sum i (tl l) +j < n - a 
        B4  carrier_mat (n-a) (n-a) carrier_matD(2) dim_col_mat(1) Suc
        index_mat(1) prod.sel 
      unfolding split_block_def Let_def by force
    also have "... = diag_mat B!(n_sum i (tl l) + j + a)" 
    proof -
      have "n_sum i (tl l) + j + a < n" using n_sum i (tl l) +j < n - a 
        by simp
      thus ?thesis using Suc unfolding diag_mat_def by simp
    qed
    also have "... = diag_mat B ! (n_sum (Suc i) l + j)"
    proof -
      have "n_sum i (tl l) + a = n_sum (Suc i) l" unfolding a_def by simp
      thus ?thesis
        by (simp add: add.commute add.left_commute)
    qed
    finally show ?thesis .
  qed
qed

lemma hermitian_extract_subdiags:
  assumes "hermitian A"
  and "sum_list l  dim_row A"
  and "list_all (λa. 0 < a) l"
  shows "list_all (λB. 0 < dim_row B  hermitian B) (extract_subdiags A l)"
  using assms
proof (induct l arbitrary: A)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  define es where "es = extract_subdiags A (a#l)"
  define B1 where "B1 = fst (split_block A a a)"
  define B2 where "B2 = fst (snd (split_block A a a))"
  define B3 where "B3 = fst (snd (snd (split_block A a a)))"
  define B4 where "B4 = snd (snd (snd (split_block A a a)))"
  have sp: "split_block A a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  have "0 < a" using Cons by simp
  have "es  []" using extract_subdiags_neq_Nil[of A] 
    unfolding es_def by simp
  hence "es = hd es # (tl es)"  by simp 
  have "hd es = B1" unfolding es_def 
    using extract_subdiags_not_emp(1)[OF sp[symmetric]] by simp
  have "dim_row B1 = a" unfolding B1_def split_block_def Let_def by simp
  have "tl es = extract_subdiags B4 l" unfolding es_def
    using extract_subdiags_not_emp(2)[OF sp[symmetric]] by simp
  have "list_all (λB. 0 < dim_row B  hermitian B) (hd es # (tl es))"
  proof (rule list_all_simps(1)[THEN iffD2], intro conjI)
    show "hermitian (hd es)" 
    proof (rule split_block_hermitian_1)
      show "hermitian A" using Cons by simp
      show "(hd es, B2, B3, B4) = split_block A a a" using sp hd es = B1 
        by simp
      show "a  dim_row A" using Cons by simp
    qed
    have "list_all (λB. 0 < dim_row B  hermitian B) (extract_subdiags B4 l)" 
    proof (rule Cons(1))
      show "hermitian B4" 
      proof (rule split_block_hermitian_4)
        show "hermitian A" using Cons by simp
        show "a  dim_row A" using Cons by simp
        show "(B1, B2, B3, B4) = split_block A a a" using sp by simp
      qed
      show "sum_list l  dim_row B4" using Cons sp 
        unfolding split_block_def Let_def by force
      show "list_all ((<) 0) l" using Cons(4) by auto
    qed
    thus "list_all (λB. 0 < dim_row B  hermitian B) (tl es)" 
      using tl es = extract_subdiags B4 l by simp
    show "0 < dim_row (hd es)" 
      using hd es = B1 0 < a dim_row B1 = a by simp
  qed
  thus ?case using es = hd es # (tl es) unfolding es_def by metis
qed

subsection ‹Predicates on diagonal block matrices›
text ‹The predicate \verb+diag_compat+ ensures that the provided matrix, when decomposed
according to the list of integers provided as an input, is indeed a diagonal block matrix.›

fun diag_compat where
  "diag_compat B [] = (dim_row B = 0  dim_col B = 0)"
| "diag_compat B (x#xs) = 
    (x  dim_row B 
    (let n = dim_row B; (B1, B2, B3, B4) = (split_block B x x) in 
      B2 = (0m x (n - x))  B3 = (0m (n - x) x)  diag_compat B4 xs))"

text ‹When this is the case, the decomposition of a matrix leaves it unchanged.›

lemma diag_compat_extract_subdiag:
  assumes "B carrier_mat n n"
  and "diag_compat B l"
  shows "B = diag_block_mat (extract_subdiags B l)" using assms
proof (induct l arbitrary:B n)
  case Nil
  have "extract_subdiags B Nil = []" by simp
  have "B = 0m 0 0"
  proof (rule eq_matI, auto simp add: assms)
    show "dim_row B = 0" using Nil by simp
    show "dim_col B = 0" using Nil by simp
  qed
  then show ?case using diag_block_mat_singleton[of B] by simp
next
  case (Cons a l)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  have "a  n" using assms Cons by simp
  have "diag_compat B4 l" using sp Cons by (simp add: Let_def)
  have "B1  carrier_mat a a" using sp Cons split_block(1)[OF sp]
    by (metis a  n carrier_matD(1) carrier_matD(2) le_add_diff_inverse)
  have "B2  carrier_mat a (n-a)" using sp Cons by (simp add: Let_def)
  have "B3  carrier_mat (n-a) a" using sp Cons by (simp add: Let_def)
  have "B4  carrier_mat (n-a) (n-a)" using assms a  n Cons 
      split_block(4)[OF sp] by simp
  have b2: "0m (dim_row B1) (dim_col B4) = B2" 
    using diag_compat.simps(2)[THEN iffD1, OF diag_compat B (a#l)]     
    B4  carrier_mat (n-a) (n-a) B1  carrier_mat a a 
    B2  carrier_mat a (n-a) sp unfolding Let_def
    Cons(2) by force
  have b3: "0m (dim_row B4) (dim_col B1) = B3" 
    using diag_compat.simps(2)[THEN iffD1, OF diag_compat B (a#l)]     
    B4  carrier_mat (n-a) (n-a) B1  carrier_mat a a 
    B2  carrier_mat a (n-a) sp unfolding Let_def
    Cons(2) by force
  have "extract_subdiags B (a#l) = B1 # (extract_subdiags B4 l)" 
    using fst_conv snd_conv extract_subdiags.simps(2)[of B]
    unfolding B1_def B4_def Let_def by (simp add: split_def) 
  also have "diag_block_mat ... = 
    (let
     C = diag_block_mat (extract_subdiags B4 l)
     in four_block_mat B1 (0m (dim_row B1) (dim_col C)) 
        (0m (dim_row C) (dim_col B1)) C)" by simp
  also have "... = four_block_mat B1 (0m (dim_row B1) (dim_col B4)) 
    (0m (dim_row B4) (dim_col B1)) B4" using Cons diag_compat B4 l 
    B4  carrier_mat (n-a) (n-a) by (simp add:Let_def)
  also have "... = four_block_mat B1 B2 B3 B4" using b2 b3 by simp
  also have "... = B" using split_block(5)[OF sp, of "n-a" "n-a"] Cons by simp
  finally show ?case by simp
qed

text ‹Predicate \verb+diag_diff+ holds when the decomposition of the considered
matrix based on the list of integers provided as a parameter, is such that the diagonal
elements of separate components are pairwise distinct.›

fun diag_diff where
  "diag_diff D [] = (dim_row D = 0  dim_col D = 0)"
| "diag_diff D (x#xs) =
    (x  dim_row D  
      (let (D1, D2, D3, D4) = (split_block D x x) in 
        (i j. i < dim_row D1  j < dim_row D4  D1$$(i,i)  D4 $$ (j,j))  
        diag_diff D4 xs))"

lemma diag_diff_hd_diff:
  assumes "diag_diff D (a#xs)"
  and "D carrier_mat n n"
  and "i < a"
  and "a  j"
  and "j < n"
shows "D$$(i,i)  D $$ (j,j)"
proof -
  define D1 where "D1 = fst (split_block D a a)"
  define D2 where "D2 = fst (snd (split_block D a a))"
  define D3 where "D3 = fst (snd (snd (split_block D a a)))"
  define D4 where "D4 = snd (snd (snd (split_block D a a)))"
  have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv 
    unfolding D1_def D2_def D3_def D4_def by simp
  have c1: "D1  carrier_mat a a" using split_block(1)[OF spd, of "n-a" "n-a"] 
      assms by simp
  have c4: "D4  carrier_mat (n-a) (n-a)" using assms  
      split_block(4)[OF spd] by simp
  hence "j - a < dim_row D4" using assms by simp
  have "D $$ (i,i) = D1 $$ (i,i)" using assms spd 
    unfolding split_block_def Let_def by force
  moreover have "D $$ (j,j) = D4 $$ (j-a, j - a)" using assms spd 
    unfolding split_block_def Let_def by force
  moreover have "D1 $$ (i,i)  D4 $$ (j-a, j - a)" 
    using assms j - a < dim_row D4 spd c1 c4 
      diag_diff.simps(2)[THEN iffD1, OF assms(1)] unfolding Let_def by simp
  ultimately show ?thesis by simp
qed

lemma diag_compat_diagonal:
  assumes "B carrier_mat (dim_row B) (dim_row B)"
  and "diagonal_mat B"
  and "dim_row B = sum_list l"
shows "diag_compat B l" using assms
proof (induct l  arbitrary: B)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have sp: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  have "diagonal_mat B1  diagonal_mat B4"
  proof (rule split_block_diagonal)
    show "split_block B a a = (B1, B2, B3, B4)" using sp .
    show "diagonal_mat B" using Cons by simp
    show "B carrier_mat (dim_row B) (dim_row B)" using Cons by simp
    show "a  dim_row B" using Cons by simp
  qed
  define n where "n = dim_row B"
  have "diag_compat B4 l" 
  proof (rule Cons(1)) 
    show "diagonal_mat B4" using diagonal_mat B1  diagonal_mat B4 by simp
    show "B4  carrier_mat (dim_row B4) (dim_row B4)" using sp Cons 
      unfolding split_block_def Let_def by auto
    show "dim_row B4 = sum_list l" using Cons sp 
      unfolding split_block_def Let_def by auto
  qed
  have "B2 = 0m a (n - a)"
  proof (rule eq_matI, auto)
    show "dim_row B2 = a" using sp unfolding split_block_def Let_def n_def 
      by auto
    show "dim_col B2 = n-a" using sp Cons 
      unfolding split_block_def Let_def n_def by auto
    fix i j
    assume "i < a" and "j < n-a"
    thus "B2 $$(i,j) = 0" using sp Cons 
      unfolding split_block_def Let_def n_def diagonal_mat_def by force
  qed
  have "B3 = 0m (n - a) a" 
  proof (rule eq_matI, auto)
    show "dim_row B3 = n-a" using sp Cons 
      unfolding split_block_def Let_def n_def by auto
    show "dim_col B3 = a" using sp Cons 
      unfolding split_block_def Let_def n_def by auto
    fix i j
    assume "i < n-a" and "j < a" 
    thus "B3 $$(i,j) = 0" using sp Cons 
      unfolding split_block_def Let_def n_def diagonal_mat_def by force
  qed
  show ?case 
  proof (rule diag_compat.simps(2)[THEN iffD2], intro conjI)
    show "a  dim_row B" using Cons by simp
    show "let n = dim_row B; 
      (B1, B2, B3, B4) = split_block B a a in B2 = 0m a (n - a)  
      B3 = 0m (n - a) a  diag_compat B4 l" 
      using sp B3 = 0m (n - a) a B2 = 0m a (n - a) 
        diag_compat B4 l unfolding Let_def n_def by auto
  qed
qed

text ‹The following lemma provides a sufficient condition for the \verb+diag_compat+ predicate
to hold.›

lemma commute_diag_compat:
  fixes D::"'a::{field} Matrix.mat"
  assumes "diagonal_mat D"
  and "D carrier_mat n n"
  and "B carrier_mat n n"
  and "B* D = D * B"
  and "diag_diff D l"
shows "diag_compat B l" using assms
proof (induct l arbitrary: B D n)
  case Nil
  hence "D  carrier_mat 0 0" using assms by simp
  hence "n = 0" using assms using Nil(2) by auto 
  hence "B  carrier_mat 0 0" using Nil by simp 
  then show ?case by simp
next
  case (Cons a l)
  define B1 where "B1 = fst (split_block B a a)"
  define B2 where "B2 = fst (snd (split_block B a a))"
  define B3 where "B3 = fst (snd (snd (split_block B a a)))"
  define B4 where "B4 = snd (snd (snd (split_block B a a)))"
  have spb: "split_block B a a = (B1, B2, B3, B4)" using fst_conv snd_conv 
    unfolding B1_def B2_def B3_def B4_def by simp
  define D1 where "D1 = fst (split_block D a a)"
  define D2 where "D2 = fst (snd (split_block D a a))"
  define D3 where "D3 = fst (snd (snd (split_block D a a)))"
  define D4 where "D4 = snd (snd (snd (split_block D a a)))"
  have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv 
    unfolding D1_def D2_def D3_def D4_def by simp
  have "a  n" using Cons by simp
  moreover have "diag_compat B4 l" 
  proof (rule Cons(1)) 
    show "diagonal_mat D4" using spd Cons a  n 
      split_block_diagonal[of D n a] by blast
    show "D4 carrier_mat (n-a) (n-a)" using spd Cons(3) 
      unfolding split_block_def Let_def by fastforce
    show "diag_diff D4 l" using spd Cons by simp
    show "B4  carrier_mat (n - a) (n - a)" using spb Cons(4) 
      unfolding split_block_def Let_def by fastforce
    show "B4 * D4 = D4 * B4" using spb Cons a  n  
      split_block_commute_subblock[of D] by (meson spd)
  qed
  moreover have "B2 = 0m a (n - a)" 
  proof (rule commute_diag_mat_split_block(1)[of D n B a B1 B2 B3 B4], 
      (auto simp add: spb Cons a  n))
    fix i j
    assume "i < a" and "a  j" and "j < n"
    thus "D $$ (i, i) = D $$ (j, j)  False"
      using diag_diff_hd_diff[OF Cons(6) Cons(3), of i j] by simp 
  qed
  moreover have "B3 = 0m (n - a) a" 
  proof (rule commute_diag_mat_split_block(2)[of D n B a B1 B2 B3 B4], 
      (auto simp add: spb Cons a  n))
    fix i j
    assume "i < a" and "a  j" and "j < n"
    thus "D $$ (i, i) = D $$ (j, j)  False"
      using diag_diff_hd_diff[OF Cons(6) Cons(3), of i j] by simp 
  qed
  ultimately show ?case 
    using spb diag_compat.simps(2)[THEN iffD2, of a B l] Cons
    unfolding Let_def by force
qed

subsection ‹Counting similar neighbours in a list›
text ‹The function \verb+eq_comps+ takes a list as an input and counts the number of
adjacent elements that are identical.›

fun eq_comps where
  "eq_comps [] = []"
| "eq_comps [x] = [1]"
| "eq_comps (x#y#l) = (let tmp = (eq_comps (y#l)) in
    if x = y then Suc (hd tmp) # (tl tmp)
    else 1 # tmp)"

lemma eq_comps_not_empty:
  assumes "l []"
  shows "eq_comps l  []" using assms
proof (induct l rule: eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  then show ?case by (cases "x = y", (auto simp add: Let_def))
qed

lemma eq_comps_empty_if:
  assumes "eq_comps l = []"
  shows "l = []" 
proof (rule ccontr)
  assume "l []"
  hence "eq_comps l  []" using eq_comps_not_empty[of l] by simp
  thus False using assms by simp
qed

lemma eq_comps_hd_eq_tl:
  assumes "x = y"
  shows "tl (eq_comps (x#y#l)) = tl (eq_comps (y#l))" using assms by (simp add: Let_def)

lemma eq_comps_hd_neq_tl:
  assumes "x  y"
  shows "tl (eq_comps (x#y#l)) = eq_comps (y#l)" using assms by (simp add:Let_def)

lemma eq_comps_drop:
  assumes "x#xs = eq_comps l"
  shows "xs = eq_comps (drop x l)" using assms
proof (induct l arbitrary:x xs rule: eq_comps.induct)
case 1
  then show ?case by simp
next
  case (2 u)
  hence "x = 1" by simp
  hence "drop x [u] = []" by simp 
  then show ?case using "2" by fastforce 
next
  case (3 u v l)
  define ec where "ec = eq_comps (v#l)"
    have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "v#l"] unfolding ec_def 
      by simp
  show ?case
  proof (cases "u = v")
    case True   
    have "xs = tl ec" using 3 eq_comps_hd_eq_tl[OF True] ec_def
      by (metis list.sel(3))
    moreover have "x = Suc (hd ec)" using True 3 eq_comps.simps(3)[of u v ] 
      unfolding ec_def Let_def by simp
    hence "drop (hd ec) (v#l) = drop x (u#v#l)" by simp
    moreover have "tl ec = eq_comps (drop (hd ec) (v#l))" using 3 ec_def
      ec = hd ec # (tl ec) by simp
    ultimately show ?thesis using 3 by simp
  next
    case False
    hence "x = 1" using 3 unfolding Let_def by simp
    moreover have "xs = ec" using 3 eq_comps_hd_neq_tl[OF False] ec_def 
      by (metis list.sel(3))
    ultimately show ?thesis unfolding ec_def by simp
  qed
qed

lemma eq_comps_neq_0:
  assumes "a#m = eq_comps l"
  shows "a  0" using assms
proof (induct l rule:eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  then show ?case by (cases "x = y", (auto simp add: Let_def))
qed

lemma eq_comps_gt_0:
  assumes "l  []"
  shows "list_all (λa. 0 < a) (eq_comps l)"
proof (induct l rule:eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  then show ?case 
  proof (cases "x = y")
    case True
    then show ?thesis 
      using 3 eq_comps.simps(3)[of x y l] list_all_simps(1) unfolding Let_def
      by (metis eq_comps_not_empty hd_Cons_tl list.discI zero_less_Suc) 
  next
    case False
    then show ?thesis 
      using 3 eq_comps.simps(3)[of x y l] list_all_simps(1) unfolding Let_def 
      by auto
  qed
qed

lemma eq_comps_elem_le_length:
  assumes "a#m = eq_comps l"
  shows "a  length l" using assms
proof (induct l arbitrary: a rule:eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by auto
next
  case (3 x y l)
  then show ?case 
  proof (cases "x = y")
    case True
    define ec where "ec = eq_comps (y#l)"
    have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] unfolding ec_def 
      by simp
    have "a = Suc (hd ec)" using True 3 eq_comps.simps(3)[of x y] 
      unfolding ec_def Let_def by simp
    then show ?thesis using 3
      by (metis True ec = hd ec # tl ec ec_def eq_comps_hd_eq_tl length_Cons 
          list.sel(3) not_less_eq_eq) 
  next
    case False
    hence "a = 1" using 3 by (simp add: Let_def)
    then show ?thesis by simp
  qed
qed

lemma eq_comps_length:
  shows "length (eq_comps l)  length l"
proof (induct l rule:eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by auto
next
  case (3 x y l)
  define ec where "ec = eq_comps (y#l)"
    have ec: "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] unfolding ec_def 
      by simp
  then show ?case 
  proof (cases "x = y")
    case True    
    then show ?thesis using ec 3 eq_comps.simps(3) True unfolding Let_def
      by (metis ec_def le_SucI length_Cons)
  next
    case False
    then show ?thesis using ec 3 by simp
  qed
qed

lemma eq_comps_eq:
  assumes "a#m = eq_comps l"
  and "i < a"
shows "nth l i = hd l" using assms
proof (induct l arbitrary: a m i rule: eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 u)
  then show ?case by simp
next
  case (3 u v l)
  show ?case
  proof (cases "u = v")
    case False
    thus ?thesis using 3 by (simp add: Let_def)
  next
    case True
    define ec where "ec = eq_comps (v#l)"
    have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "v#l"] 
      unfolding ec_def by simp
    have "a = Suc (hd ec)" using True 3 eq_comps.simps(3)[of u v] 
      unfolding ec_def Let_def by simp
    hence "i  hd ec" using 3 by simp
    show ?thesis
    proof (cases "i = 0")
      case True
      thus ?thesis by simp
    next
      case False
      hence "i'. i = Suc i'"  by (simp add: not0_implies_Suc)
      from this obtain i' where "i = Suc i'" by auto
      hence "i' < hd ec" using i  hd ec by simp
      have "(u # v # l) ! i = (v#l) ! i'" using i = Suc i' by simp
      also have "... = v" using 3 ec = eq_comps (v#l) ec = hd ec # (tl ec)
        by (metis i' < hd ec list.sel(1)) 
      also have "... = hd (u#v#l)" using u = v by simp
      finally show ?thesis .
    qed
  qed
qed

lemma eq_comps_singleton:
  assumes "[a] = eq_comps l"
  shows "a = length l" using assms
proof (induct l arbitrary: a rule: eq_comps.induct)
case 1
then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  define ec where "ec = eq_comps (y#l)"
  have "ec = hd ec # (tl ec)" using eq_comps_not_empty[of "y#l"] 
    unfolding ec_def by simp
  show ?case
  proof (cases "x = y")
    case True
    hence "a = Suc (hd ec)" using 3 eq_comps.simps(3)[of x y] 
      unfolding ec_def Let_def by simp
    have "tl ec = []" using 3 True eq_comps.simps(3)[of x y] 
      unfolding ec_def Let_def by simp
    hence "ec = [hd ec]" using ec = hd ec # tl ec by simp
    hence "hd ec = length (y#l)" using 3 ec_def by simp
    then show ?thesis using a = Suc (hd ec) by simp
  next
    case False
    then show ?thesis using eq_comps_hd_neq_tl 3
      ec = hd ec # tl ec ec_def by fastforce 
  qed
qed

lemma eq_comps_leq:
  assumes "a#b#m = eq_comps l"
  and "sorted l"
shows "hd l < hd (drop a l)" using assms
proof (induct l arbitrary: a b m  rule: eq_comps.induct)
case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  show ?case
  proof (cases "x = y")
    case True
    hence "hd (x#y#l) = y" by simp
    define ec where "ec = eq_comps (y#l)"
    have "a = Suc (hd (ec))" using True ec_def 3
      eq_comps.simps(3)[of x y] unfolding Let_def by simp
    have "b#m = tl ec" using True ec_def 3
      eq_comps.simps(3)[of x y] unfolding Let_def by simp
    hence eceq: "ec = hd ec # (hd (tl ec)) # (tl (tl ec))" unfolding ec_def
      by (metis eq_comps_not_empty list.exhaust_sel list.simps(3))
    have dra: "drop a (x#y#l) = drop (hd ec) (y#l)" using a = Suc (hd (ec)) 
      by simp
    have "sorted (y#l)" using 3 by simp
    hence "y < hd (drop (hd ec) (y#l))" using 3(1) eceq unfolding ec_def
      by (metis list.sel(1))
    thus ?thesis using True dra by simp
  next
    case False
    hence "a = 1" using 3 by (simp add: Let_def)
    have "hd (x#y#l) = x" by simp
    moreover have "hd (drop a (x # y # l)) = y" using a = 1 by simp
    ultimately show ?thesis using False 3
      by (metis order_le_imp_less_or_eq sorted2_simps(2))
  qed
qed

lemma eq_comps_compare:
  assumes "sorted l"
  and "a#m = eq_comps l"
  and "i < a"
  and "a  j"
  and "j < length l"
shows "nth l i < nth l j" using assms
proof (cases "m =[]")
  case True
  hence "[a] = eq_comps l" using assms by simp
    hence "a = length l" using eq_comps_singleton[of a "l"] by simp
    then show ?thesis using assms by simp
next
  case False
  hence "m = hd m # (tl m)" by simp
  have "l!i = hd l" using assms eq_comps_eq by metis
  also have "... < hd (drop a l)" using eq_comps_leq assms m = hd m # (tl m) 
    by metis
  also have "...  l!j" using assms
    by (metis hd_drop_conv_nth le_less_trans sorted_nth_mono)
  finally show ?thesis .
qed

lemma eq_comps_singleton_elems:
  assumes "eq_comps l = [a]"
  shows "i < length l. l!i = l!0" using eq_comps_eq eq_comps_singleton
  by (metis assms bot_nat_0.not_eq_extremum eq_comps_neq_0)

lemma eq_comp_Re:
  assumes " z  set l. z  Reals"
  and "m = eq_comps l"
shows "m = eq_comps (map Re l)" using assms 
proof (induct l arbitrary:m rule:eq_comps.induct)
  case 1
  then show ?case by simp
next
  case (2 x)
  then show ?case by simp
next
  case (3 x y l)
  define ec where "ec = eq_comps (y#l)"
  have ecr: "ec = eq_comps (map Re (y # l))" using ec_def 3 by simp
  show ?case
  proof (cases "x = y")
    case True
    hence "Re x = Re y" by simp
    have "m = Suc (hd ec) # (tl ec)" using ec_def 3 True
      by (simp add: Let_def)
    also have "... = eq_comps (map Re (x#y # l))" using ecr Re x = Re y 
      by (simp add: Let_def)
    finally show ?thesis .
  next
    case False
    hence "Re x  Re y" using 3
      by (metis list.set_intros(1) list.set_intros(2) of_real_Re)
    have "m = 1#ec" using ec_def 3 False
      by (simp add: Let_def)
    also have "... = eq_comps (map Re (x#y # l))" using ecr Re x  Re y 
      by (simp add: Let_def)
    finally show ?thesis using ecr unfolding Let_def by simp
  qed
qed

lemma eq_comps_sum_list:
  shows "sum_list (eq_comps l) = length l" 
proof (induct l  rule: eq_comps.induct)
  case 1
  then show ?case unfolding diag_mat_def by simp
next
  case (2 x)
  have "eq_comps [x] = [1]" using eq_comps.simps(2)[of x] by simp
  then show ?case by simp
next
  case (3 x y l)
  then show ?case 
  proof (cases "x = y")
    case True
    then show ?thesis using eq_comps.simps(3)[of x y l] 3
      by (cases eq_comps (y # l)) simp_all
  next
    case False
    then show ?thesis using eq_comps.simps(3)[of x y l]  3 
      unfolding Let_def by simp
  qed
qed

lemma eq_comps_elem_lt:
  assumes "1 < length (eq_comps l)"
  shows "hd (eq_comps l) < length l"
proof -
  define a where "a = hd (eq_comps l)"
  define b where "b = hd (tl (eq_comps l))"
  define c where "c = tl (tl (eq_comps l))"
  have "eq_comps l = a#b#c" using assms unfolding a_def b_def c_def
    by (metis eq_comps.simps(2) eq_comps_singleton length_0_conv 
        less_irrefl_nat less_nat_zero_code list.exhaust_sel)
  hence "b#c = eq_comps (drop a l)" using eq_comps_drop by metis
  hence "0 < b" using eq_comps_neq_0 by auto 
  moreover have "0 < a" using eq_comps l = a#b#c eq_comps_neq_0
    by (metis gr0I) 
  moreover have "a+b  length l" using eq_comps_sum_list
    by (metis eq_comps l = a # b # c le_add1 nat_add_left_cancel_le 
        sum_list_simps(2))
  ultimately show ?thesis unfolding a_def by auto
qed

lemma eq_comp_sum_diag_mat:
  shows "sum_list (eq_comps (diag_mat A)) = dim_row A" 
  using eq_comps_sum_list[of "diag_mat A"] diag_mat_length by simp

lemma nsum_Suc_elem:
  assumes "1 < length (eq_comps l)"
  shows "l!(n_sum (Suc i) (eq_comps l)) = 
    (drop (hd (eq_comps l)) l)!(n_sum i (tl (eq_comps l)))" using assms
proof (induct i arbitrary: l)
  case 0
  hence "1 < length l" using eq_comps_length[of l] by presburger
  hence "l  []" by fastforce
  hence "l ! n_sum (Suc 0) (eq_comps l) = l ! hd (eq_comps l)"  
    by (simp add: "0.prems" eq_comps_not_empty hd_conv_nth)
  also have "... = hd (drop (hd (eq_comps l)) l)"
    by (metis "0.prems" eq_comps_elem_lt hd_drop_conv_nth)
  finally show ?case using 0
    by (metis (no_types, opaque_lifting) l ! hd (eq_comps l) = 
      hd (drop (hd (eq_comps l)) l) l  [] append_Nil2 
      eq_comps.simps(1) eq_comps_drop eq_comps_empty_if eq_comps_singleton 
      hd_conv_nth list.exhaust_sel n_sum.simps(1) nat_arith.rule0 
      nth_append_length_plus) 
next
  case (Suc i)
  have "l!(n_sum (Suc (Suc i)) (eq_comps l)) = 
    l!(hd (eq_comps l) + (n_sum (Suc i) (tl (eq_comps l))))" by simp
  also have "... = (drop (hd (eq_comps l)) l)!
    (n_sum (Suc i) (tl (eq_comps l)))" 
    using less_or_eq_imp_le
    by (metis Suc.prems eq_comps_elem_lt nth_drop)
  finally show ?case .
qed

lemma eq_comps_elems_eq:
  assumes "l[]"
  and "i < length (eq_comps l)"
  and "j < (eq_comps l)!i"
shows "l!(n_sum i (eq_comps l)) = l!(n_sum i (eq_comps l) + j)" using assms
proof (induct i arbitrary: l)
  case 0
  hence "eq_comps l = hd (eq_comps l)#(tl (eq_comps l))" by simp
  have "l ! n_sum 0 (eq_comps l) = hd l"
    by (simp add: "0"(1) hd_conv_nth)
  also have "... = l!j" using 0 eq_comps_eq
    by (metis eq_comps l = hd (eq_comps l) # tl (eq_comps l) nth_Cons_0)
  finally show ?case by simp
next
  case (Suc i)
  show ?case
  proof (cases "length (eq_comps l) = 1")
    case True
    hence "Suc i = 0" using Suc.prems(2) by fastforce 
    then show ?thesis by simp
  next
    case False
    hence "1 < length (eq_comps l)" using Suc eq_comps_not_empty[of l] 
      by presburger
    hence "l!(n_sum (Suc i) (eq_comps l)) = 
    (drop (hd (eq_comps l)) l)!(n_sum i (tl (eq_comps l)))"
      using nsum_Suc_elem by simp
    also have "... = (drop (hd (eq_comps l)) l)!
      (n_sum i (eq_comps (drop (hd (eq_comps l)) l)))" 
      using eq_comps_drop[of "hd (eq_comps l)"] eq_comps_empty_if list.collapse
      by fastforce
    also have "... = (drop (hd (eq_comps l)) l)!
      (n_sum i (eq_comps (drop (hd (eq_comps l)) l)) + j)" 
    proof (rule Suc(1))
      show "drop (hd (eq_comps l)) l  []"
        by (metis Cons_nth_drop_Suc 1 < length (eq_comps l) eq_comps_elem_lt 
            list.distinct(1)) 
      show "i < length (eq_comps (drop (hd (eq_comps l)) l))" using Suc
        by (metis (no_types, lifting) Suc_lessD eq_comps_drop 
            eq_comps_not_empty length_Suc_conv list.collapse 
            not_less_less_Suc_eq) 
      show "j < eq_comps (drop (hd (eq_comps l)) l) ! i" using Suc
        by (metis eq_comps_drop length_Suc_conv less_natE list.exhaust_sel 
            list.simps(3) nth_Cons_Suc) 
    qed
    also have "... = (drop (hd (eq_comps l)) l)!
      (n_sum i (tl (eq_comps l)) + j)"
      by (metis Suc(2) eq_comps_drop eq_comps_not_empty hd_Cons_tl) 
    also have "... = l!(n_sum (Suc i) (eq_comps l) + j)"
      by (metis (no_types, opaque_lifting) Groups.add_ac(2) 
          Groups.add_ac(3) 1 < length (eq_comps l) eq_comps_elem_lt 
          less_or_eq_imp_le n_sum.simps(2) nth_drop) 
    finally show ?thesis .
  qed
qed

text ‹When the diagonal block matrices are extracted using \verb+eq_comp+, each extracted 
matrix is a multiple of the identity.›

lemma extract_subdiags_eq_comp:
  fixes A::"complex Matrix.mat"
  assumes "diagonal_mat A"
  and "A carrier_mat n n"
  and "0 < n"
  and "i < length (eq_comps (diag_mat A))"
  shows "k. (extract_subdiags A (eq_comps (diag_mat A)))!i = 
    k m (1m ((eq_comps (diag_mat A))!i))"
proof 
  define l where "l = diag_mat A"
  define k where "k = l!(n_sum i (eq_comps l))"
  show "extract_subdiags A (eq_comps (diag_mat A)) ! i = 
    k m 1m (eq_comps (diag_mat A) ! i)"
  proof (rule eq_matI, auto simp add: assms)
    show dr: "dim_row (extract_subdiags A (eq_comps (diag_mat A)) ! i) = 
      eq_comps (diag_mat A) ! i" 
      using extract_subdiags_carrier assms carrier_matD(1) by blast
    show dc: "dim_col (extract_subdiags A (eq_comps (diag_mat A)) ! i) = 
      eq_comps (diag_mat A) ! i"
      using extract_subdiags_carrier assms carrier_matD by blast
    fix m np
    assume "m < eq_comps (diag_mat A)!i" and "np < eq_comps (diag_mat A)!i" 
      and "m np" note mnp=this
    have "diagonal_mat (extract_subdiags A (eq_comps (diag_mat A)) !i)"
    proof (rule extract_subdiags_diagonal)
      show "diagonal_mat A" using assms by simp
      show "A carrier_mat n n" using assms by simp
      show "eq_comps (diag_mat A)  []" using assms unfolding diag_mat_def
        by auto
      show "sum_list (eq_comps (diag_mat A))  n" 
        using assms eq_comps_sum_list unfolding diag_mat_def
        by (metis carrier_matD(1) carrier_matD(2) length_cols_mat_to_cols_list 
            length_map order.eq_iff)
      show "i < length (eq_comps (diag_mat A))" using assms by simp
    qed
    thus "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (m, np) = 0" 
      using mnp dr dc by (metis diagonal_mat_def)
  next
    fix p
    assume "p < eq_comps (diag_mat A) ! i"
    have "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (p, p) = 
      diag_mat A! (n_sum i (eq_comps (diag_mat A)) + p)" 
    proof (rule extract_subdiags_diag_elem)
      show "A carrier_mat n n" "0 < n" "i < length (eq_comps (diag_mat A))" 
        using assms by auto
      show ne: "eq_comps (diag_mat A)  []" using assms by auto
      show "p < eq_comps (diag_mat A) ! i" 
        using p < eq_comps (diag_mat A) ! i .
      show "sum_list (eq_comps (diag_mat A))  n" 
        using assms eq_comps_sum_list[of "diag_mat A"] 
        unfolding diag_mat_def by simp
      show "j<length (eq_comps (diag_mat A)). 0 < eq_comps (diag_mat A) ! j" 
        using eq_comps_gt_0 ne
        by (metis eq_comps.simps(1) list_all_length)
    qed 
    also have "... = k" unfolding k_def l_def 
    proof (rule eq_comps_elems_eq[symmetric])
      show "diag_mat A  []" using assms unfolding diag_mat_def by simp
      show "p < eq_comps (diag_mat A) ! i" 
        using p < eq_comps (diag_mat A) ! i .
      show "i < length (eq_comps (diag_mat A))" using assms by simp
    qed
    finally show 
      "extract_subdiags A (eq_comps (diag_mat A)) ! i $$ (p, p) = k" .
  qed
qed

lemma extract_subdiags_comp_commute:
  fixes A::"complex Matrix.mat"
  assumes "diagonal_mat A"
  and "A carrier_mat n n"
  and "0 < n"
  and "i < length (eq_comps (diag_mat A))"
  and "B  carrier_mat ((eq_comps (diag_mat A))!i) ((eq_comps (diag_mat A))!i)"
  shows "(extract_subdiags A (eq_comps (diag_mat A)))!i * B = 
    B * (extract_subdiags A (eq_comps (diag_mat A)))!i"
proof -
  define m where "m = (eq_comps (diag_mat A))!i" 
  have "k. (extract_subdiags A (eq_comps (diag_mat A)))!i = 
    k m (1m ((eq_comps (diag_mat A))!i))" 
    using assms extract_subdiags_eq_comp by simp
  from this obtain k where 
    "(extract_subdiags A (eq_comps (diag_mat A)))!i = 
    k m (1m m)" unfolding m_def by auto note kprop = this
  hence "(extract_subdiags A (eq_comps (diag_mat A)))!i * B =
    k m (1m m) * B" by simp
  also have "... = B * (k m (1m m))" using assms m_def
    by (metis left_mult_one_mat mult_smult_assoc_mat 
        mult_smult_distrib one_carrier_mat right_mult_one_mat)
  finally show ?thesis using kprop by simp
qed

text ‹In particular, extracting the diagonal sub-blocks of a diagonal matrix leaves
it unchanged. ›

lemma diagonal_extract_eq:
  assumes "B carrier_mat n n"
  and "diagonal_mat B"
shows "B = diag_block_mat (extract_subdiags B (eq_comps (diag_mat B)))" 
proof (rule diag_compat_extract_subdiag)
  define eqcl where "eqcl= eq_comps (diag_mat B)"
  show "B  carrier_mat n n" using assms by simp
  show  "diag_compat B eqcl" 
  proof (rule diag_compat_diagonal)
    show "B  carrier_mat (dim_row B) (dim_row B)" 
      using assms by simp
    show "diagonal_mat B" using assms by simp
    have "dim_row B = length (diag_mat B)" unfolding diag_mat_def by simp
    also have "... = sum_list eqcl" using eq_comps_sum_list[of "diag_mat B"] 
      unfolding eqcl_def by simp
    finally show "dim_row B = sum_list eqcl".
  qed
qed

fun lst_diff where
  "lst_diff l [] = (l = [])"
| "lst_diff  l (x#xs) = (x  length l 
    (i j. i < x  x  j  j < length l  nth l i < nth l j) 
    lst_diff (drop x l) xs)"

lemma sorted_lst_diff:
  assumes "sorted l"
  and "m = eq_comps l"
shows "lst_diff l m" using assms
proof (induct m arbitrary: l)
  case Nil
  hence "l = []" using eq_comps_empty_if[of l] by simp
  then show ?case by simp
next
  case (Cons a m)
  have "sorted (drop a l)" using Cons sorted_wrt_drop by simp
  moreover have "m = eq_comps (drop a l)" using eq_comps_drop Cons by simp
  ultimately have "lst_diff (drop a l) m" using Cons by simp
  have "a  length l" using eq_comps_elem_le_length Cons by simp
  have "(i j. i < a  a  j  j < length l  nth l i < nth l j)" 
    using Cons eq_comps_compare by blast 
  then show ?case using a  length l lst_diff (drop a l) m by fastforce
qed

lemma lst_diff_imp_diag_diff:
  fixes D::"'a::preorder Matrix.mat"
  assumes "D carrier_mat n n"
  and "lst_diff (diag_mat D) m"
  shows "diag_diff D m" using assms
proof (induct arbitrary: n rule:diag_diff.induct)
  case (1 D)
  hence "diag_mat D = []"  by simp
  hence "dim_row D = 0" unfolding diag_mat_def by simp
  hence "n= 0" using 1 by simp
  hence "dim_col D = 0" using 1 by simp
  then show ?case using dim_row D = 0 by simp
next
  case (2 D a xs)
  define D1 where "D1 = fst (split_block D a a)"
  define D2 where "D2 = fst (snd (split_block D a a))"
  define D3 where "D3 = fst (snd (snd (split_block D a a)))"
  define D4 where "D4 = snd (snd (snd (split_block D a a)))"
  have spd: "split_block D a a = (D1, D2, D3, D4)" using fst_conv snd_conv 
    unfolding D1_def D2_def D3_def D4_def by simp
  have "length (diag_mat D) = n" using 2 unfolding diag_mat_def by simp
  hence "a  n" using 2 by simp
  hence c1: "D1  carrier_mat a a" 
    using split_block(1)[OF spd, of "n-a" "n-a"] 2 by simp
  have c4: "D4  carrier_mat (n-a) (n-a)" 
    using 2  split_block(4)[OF spd] a  n by simp
  have "diag_mat D = diag_mat D1 @ (diag_mat D4)" 
    using diag_four_block_mat split_block(5)
    by (metis "2"(2) a  n c1 c4 carrier_matD(1) carrier_matD(2) 
        le_Suc_ex spd)
  have "length (diag_mat D1) = a" using c1 unfolding diag_mat_def by simp
  hence "diag_mat D4 = drop a (diag_mat D)" 
    using diag_mat D = diag_mat D1 @ (diag_mat D4) by simp
  hence "lst_diff (diag_mat D4) xs" using 2 by simp
  hence "diag_diff D4 xs" using 2(1)[OF spd[symmetric]] spd c4 
    by blast
  have  "(i j. i < dim_row D1  j < dim_row D4  D1$$(i,i) < D4 $$ (j,j))" 
  proof (intro allI impI)
    fix i j
    assume ijp: "i < dim_row D1  j < dim_row D4"
    hence "i < a" using c1 by simp
    have "j+a < n" using c4 ijp by (metis carrier_matD(1) less_diff_conv) 
    have "D1 $$ (i,i) = D $$ (i,i)" using spd i < a 
      unfolding split_block_def Let_def by force
    also have "... = (diag_mat D)!i" using i < a a  n 2 
      unfolding diag_mat_def by simp
    also have "... < (diag_mat D)!(j+a)" using 2 j+a < n
      by (metis i < a length (diag_mat D) = n 
          le_add2 lst_diff.simps(2))
    also have "... = D $$ (j+a, j+a)" using j+a < n 2 
      unfolding diag_mat_def by simp
    also have "... = D4 $$ (j,j)" using spd ijp 2
      unfolding split_block_def Let_def by force
    finally show "D1$$(i,i) < D4 $$ (j,j)" .
  qed
  hence "(i j. i < dim_row D1  j < dim_row D4  D1$$(i,i)  D4 $$ (j,j))"  
    by (metis order_less_irrefl)
  thus ?case using diag_diff D4 xs a  n 2 spd by simp
qed

lemma sorted_diag_diff:
  fixes D::"'a::linorder Matrix.mat"
  assumes "D carrier_mat n n"
  and "sorted (diag_mat D)"
shows "diag_diff D (eq_comps (diag_mat D))" 
proof (rule lst_diff_imp_diag_diff)
  show "D  carrier_mat n n" using assms by simp
  show "lst_diff (diag_mat D) (eq_comps (diag_mat D))"
    using sorted_lst_diff[of "diag_mat D"] assms by simp
qed

lemma Re_sorted_lst_diff:
  fixes l::"complex list"
  assumes " z  set l. z  Reals"
  and "sorted (map Re l)"
  and "m = eq_comps l"
shows "lst_diff l m" using assms 
proof (induct m arbitrary: l)
  case Nil
  hence "l = []" using eq_comps_empty_if[of l] by simp
  then show ?case by simp
next
  case (Cons a m)  
  have "sorted (map Re (drop a l))" using Cons sorted_wrt_drop
    by (metis drop_map)
  moreover have "m = eq_comps (drop a l)" using eq_comps_drop Cons by simp
  ultimately have "lst_diff (drop a l) m" using Cons
    by (metis in_set_dropD)
  have "a  length l" using eq_comps_elem_le_length Cons by simp
  have "(i j. i < a  a  j  j < length l  nth l i < nth l j)" 
  proof (intro allI impI)
    fix i j
    assume asm: "i < a  a  j  j < length l"
    hence "Re (l!i) < Re (l!j)"
      using Cons eq_comps_compare eq_comp_Re
      by (smt (z3) dual_order.strict_trans dual_order.strict_trans1 length_map 
          nth_map)
    moreover have "l!i  Reals" using asm Cons by simp
    moreover have "l!j  Reals" using asm Cons by simp
    ultimately show "nth l i < nth l j" using less_complex_def
      by (simp add: complex_is_Real_iff)
  qed
  then show ?case using a  length l lst_diff (drop a l) m by fastforce
qed

text ‹The following lemma states a sufficient condition for the \verb+diag_diff+ predicate
to hold.›

lemma cpx_sorted_diag_diff:
  fixes D::"complex Matrix.mat"
  assumes "D carrier_mat n n"
  and " i < n. D$$(i,i)  Reals"
  and "sorted (map Re (diag_mat D))"
shows "diag_diff D (eq_comps (diag_mat D))" 
proof (rule lst_diff_imp_diag_diff)
  show "D  carrier_mat n n" using assms by simp
  have "zset (diag_mat D). z  " using assms unfolding diag_mat_def by auto
  thus "lst_diff (diag_mat D) (eq_comps (diag_mat D))"
    using Re_sorted_lst_diff[of "diag_mat D"] assms by simp
qed

section ‹Sorted hermitian decomposition›
text ‹We prove that any Hermitian matrix $A$ can be decomposed into a product 
$U^\dagger \cdot B \cdot U$, where $U$ is a unitary matrix and $B$ is a diagonal matrix
containing only real components which are ordered along the diagonal.›

definition per_col where
"per_col A f = Matrix.mat (dim_row A) (dim_col A) (λ (i,j). A $$(i, (f j)))"

lemma per_col_carrier:
  assumes "A  carrier_mat n m"
  shows "per_col A f  carrier_mat n m" using assms unfolding per_col_def 
  by simp

lemma per_col_col:
  assumes "A  carrier_mat n m"
  and "j < m"  
shows "Matrix.col (per_col A f) j = Matrix.col A (f j)" 
proof
  show dim: "dim_vec (Matrix.col (per_col A f) j) = 
    dim_vec (Matrix.col A (f j))"
    using per_col_carrier by (metis assms(1) carrier_matD(1) dim_col)
  fix i
  assume "i < dim_vec (Matrix.col A (f j))"
  hence "i < dim_vec (Matrix.col (per_col A f) j)" using dim by simp
  hence "vec_index (Matrix.col (per_col A f) j) i = (per_col A f)$$(i,j)"
    unfolding Matrix.col_def by simp
  also have "... = A $$(i, (f j))" unfolding per_col_def
    using i < dim_vec (Matrix.col A (f j)) assms by fastforce
  also have "... = vec_index (Matrix.col A (f j)) i" unfolding Matrix.col_def
    using i < dim_vec (Matrix.col A (f j)) by auto
  finally show "vec_index (Matrix.col (per_col A f) j) i = 
    vec_index (Matrix.col A (f j)) i" .
qed

lemma per_col_adjoint_row:
  assumes "A  carrier_mat n n"
  and "i < n"  
  and "f i < n"
shows "Matrix.row (Complex_Matrix.adjoint (per_col A f)) i = 
  Matrix.row (Complex_Matrix.adjoint A) (f i)" 
proof -
  have "per_col A f  carrier_mat n n" using assms per_col_carrier[of A] 
    by simp
  hence "Matrix.row (Complex_Matrix.adjoint (per_col A f)) i = 
    conjugate (Matrix.col (per_col A f) i)" 
    using assms adjoint_row[of i "per_col A f"] by simp
  also have "... = conjugate (Matrix.col A (f i))" using assms per_col_col 
    by simp
  also have "... = Matrix.row (Complex_Matrix.adjoint A) (f i)" using assms 
    adjoint_row[of "f i" A] by simp
  finally show ?thesis .
qed

lemma per_col_mult_adjoint:
  assumes "A  carrier_mat n n"
  and "i < n"
  and "j < n"
  and "f i < n"
  and "f j < n"
shows "((Complex_Matrix.adjoint (per_col A f)) * (per_col A f))$$(i,j) = 
  ((Complex_Matrix.adjoint A) * A)$$(f i, f j)"
proof -
  have "((Complex_Matrix.adjoint (per_col A f)) * (per_col A f))$$(i,j) = 
    Matrix.scalar_prod (Matrix.row (Complex_Matrix.adjoint (per_col A f)) i)
      (Matrix.col A (f j))" using assms per_col_col unfolding times_mat_def
    by (metis adjoint_dim_row carrier_matD(2) dim_col_mat(1) index_mat(1) 
        old.prod.case per_col_def)
  also have "... = Matrix.scalar_prod 
      (Matrix.row (Complex_Matrix.adjoint A) (f i))
      (Matrix.col A (f j))" using assms per_col_adjoint_row by metis
  also have "... = ((Complex_Matrix.adjoint A) * A)$$(f i, f j)" using assms 
    unfolding times_mat_def by simp
  finally show ?thesis .
qed

lemma idty_index:
  assumes "bij_betw f {..< n} {..< n}"
  and "i < n"
  and "j < n"
shows "(1m n)$$(i,j) = (1m n)$$(f i, f j)"
proof -
  have "f i < n" "f j < n" using assms bij_betwE by auto
  show ?thesis
  proof (cases "i = j")
    case True
    then show ?thesis using f i < n assms by simp
  next
    case False
    hence "f i  f j" using assms
      by (metis bij_betw_iff_bijections lessThan_iff)
    then show ?thesis
      by (metis f i < n f j < n assms(2) assms(3) index_one_mat(1))
  qed
qed

lemma per_col_unitary:
  assumes "A carrier_mat n n"
  and "unitary A"
  and "bij_betw f {..< n} {..< n}"
shows "unitary (per_col A f)" unfolding unitary_def
proof
  show pc: "per_col A f  
    carrier_mat (dim_row (per_col A f)) (dim_row (per_col A f))"
    using assms per_col_carrier by (metis carrier_matD(1))
  have "dim_row (per_col A f) = n" using assms per_col_carrier
    by (metis carrier_matD(1))
  moreover have "(Complex_Matrix.adjoint (per_col A f)) * (per_col A f) = 1m n" 
  proof (rule eq_matI)
    show "dim_row (Complex_Matrix.adjoint (per_col A f) * per_col A f) = 
      dim_row (1m n)" using pc
      by (metis adjoint_dim_row calculation carrier_matD(2) index_mult_mat(2) 
          index_one_mat(2))
    thus "dim_col (Complex_Matrix.adjoint (per_col A f) * per_col A f) = 
      dim_col (1m n)" by auto
    fix i j
    assume "i < dim_row (1m n)" and "j < dim_col (1m n)" note ij = this
    have "(Complex_Matrix.adjoint (per_col A f) * per_col A f) $$ (i, j) = 
      (Complex_Matrix.adjoint A * A) $$ (f i, f j)"
    proof (rule per_col_mult_adjoint)
      show "A carrier_mat n n" using assms by simp
      show "i < n" "j < n" using ij by auto
      thus "f i < n" using assms by (meson bij_betw_apply lessThan_iff)
      show "f j < n" using j < n assms by (meson bij_betw_apply lessThan_iff)
    qed
    also have "... = (1m n) $$ (f i, f j)" using assms 
      unfolding Complex_Matrix.unitary_def 
      by (metis  assms(2) unitary_simps(1))
    also have "... = (1m n) $$ (i,j)" using idty_index[of f n i j] assms ij 
      by auto
    finally show "(Complex_Matrix.adjoint (per_col A f) * 
      per_col A f) $$ (i, j) = 1m n $$ (i, j)" .
  qed
  ultimately show "inverts_mat (per_col A f) 
    (Complex_Matrix.adjoint (per_col A f))" 
    using inverts_mat_symm inverts_mat_def
    by (metis (no_types, lifting) adjoint_dim_col adjoint_dim_row 
        carrier_mat_triv index_mult_mat(3) index_one_mat(3))
qed

definition per_diag where
"per_diag A f = Matrix.mat (dim_row A) (dim_col A) (λ (i,j). A $$(f i, (f j)))"

lemma per_diag_carrier:
  shows "per_diag A f  carrier_mat (dim_row A) (dim_col A)" 
  unfolding per_diag_def by simp

lemma per_diag_diagonal:
  assumes "D carrier_mat n n"
  and "diagonal_mat D"
  and "bij_betw f {..< n} {..< n}"
shows "diagonal_mat (per_diag D f)" unfolding diagonal_mat_def
proof (intro allI impI)
  fix i j
  assume  "i < dim_row (per_diag D f)" and "j < dim_col (per_diag D f)"
  and "i j" note asm = this
  hence "f i  f j" using assms
    by (metis bij_betw_iff_bijections carrier_matD(1) carrier_matD(2) 
        lessThan_iff per_diag_carrier) 
  moreover have "f i < n" using assms asm
    by (metis bij_betwE carrier_matD(1) lessThan_iff per_diag_carrier)
  moreover have "f j < n" using assms asm
    by (metis bij_betwE carrier_matD(2) lessThan_iff per_diag_carrier)
  ultimately show "per_diag D f $$ (i, j) = 0" using assms
    unfolding per_diag_def diagonal_mat_def
    by (metis asm(1) asm(2) carrier_matD(1) carrier_matD(2) 
        dim_col_mat(1) dim_row_mat(1) index_mat(1) old.prod.case per_diag_def) 
qed

lemma per_diag_diag_mat:
  assumes "A  carrier_mat n n"
  and "i < n"
  and "f i < n"
shows "diag_mat (per_diag A f)!i = diag_mat A ! (f i)" 
  using assms unfolding diag_mat_def per_diag_def by auto

lemma per_diag_diag_mat_Re:
  assumes "A  carrier_mat n n"
  and "i < n"
  and "f i < n"
shows "map Re (diag_mat (per_diag A f))!i = map Re (diag_mat A) ! (f i)" 
proof -
  have "map Re (diag_mat (per_diag A f))!i = Re (diag_mat (per_diag A f)!i)" 
  proof (rule nth_map)
    show "i < length (diag_mat (per_diag A f))" 
      using assms unfolding diag_mat_def
      by (metis carrier_matD(1) carrier_matD(2) length_cols_mat_to_cols_list 
          length_map per_diag_carrier)
  qed
  also have "... = Re (diag_mat A ! (f i))" using assms per_diag_diag_mat 
    by metis
  also have "... = map Re (diag_mat A) ! (f i)" unfolding diag_mat_def
    using assms by auto
  finally show ?thesis .
qed

lemma per_diag_real:
  fixes B::"complex Matrix.mat"
  assumes "B carrier_mat n n"
  and "i< n. B$$(i,i)  Reals"
  and "bij_betw f {..<n} {..<n}"
shows "j<n. (per_diag B f)$$(j,j)  Reals" 
proof (intro allI impI)
  fix j
  assume "j < n"
  hence "per_diag B f $$ (j,j) = B $$ (f j, f j)" 
    using assms unfolding per_diag_def by simp
  also have "...  Reals" using assms j < n bij_betwE by blast
  finally show "per_diag B f $$ (j,j)  Reals" .
qed

lemma per_col_mult_unitary:
  fixes A::"complex Matrix.mat"
  assumes "A  carrier_mat n n"
  and "unitary A"
  and "D carrier_mat n n"
  and "diagonal_mat D"
  and "0 < n"
  and "bij_betw f {..< n} {..< n}"
shows "A * D * (Complex_Matrix.adjoint A) = 
  (per_col A f) * (per_diag D f) * (Complex_Matrix.adjoint (per_col A f))" 
  (is "?L = ?R")
proof  -
  have row: "dim_row ?L = dim_row ?R" using per_col_carrier assms
    by (metis carrier_matD(1) index_mult_mat(2)) 
  have col: "dim_col ?L = dim_col ?R" using per_col_carrier assms
    by (metis adjoint_dim carrier_matD(2) index_mult_mat(3))
  define fc::"complex Matrix.mat set" where "fc = carrier_mat n n"
  interpret cpx_sq_mat n n fc 
  proof 
    show "0 < n" using assms by simp
  qed (auto simp add: fc_def)
  define h where 
    "h = (λi. (if i < n then diag_mat D ! i m rank_1_proj (Matrix.col A i) 
      else (0m n n)))"
  define g where
    "g = (λi. (if i < n 
      then diag_mat D ! (f i) m rank_1_proj (Matrix.col A (f i)) 
      else (0m n n)))"
  have "f ` {..<n} = {..<n}" using assms
    by (simp add: bij_betw_imp_surj_on)
  have g: "i. g i  fc" unfolding g_def fc_def
    by (metis adjoint_dim_col assms(1) carrier_matD(1) carrier_matI 
        dim_col fc_mats_carrier rank_1_proj_adjoint rank_1_proj_dim 
        smult_carrier_mat zero_mem)
  moreover have h:"i. h i  fc" unfolding h_def fc_def
    by (metis assms(1) carrier_matD(1) dim_col fc_mats_carrier 
        rank_1_proj_carrier smult_carrier_mat zero_mem)
  moreover have "inj_on f {..<n}" using assms(6) bij_betw_def by auto 
  moreover have "x. x  {..<n}  h (f x) = g x" unfolding h_def g_def
    by (meson assms(6) bij_betwE lessThan_iff)
  ultimately have "sum_mat g {..<n} = sum_mat h (f`{..<n})" 
    using sum_with_reindex_cong[of h g f "{..<n}"] 
    unfolding  sum_mat_def by simp
  also have "... = sum_mat h {..<n}" using f ` {..<n} = {..<n} by simp
  also have "... =sum_mat (λi. diag_mat D ! i m rank_1_proj (Matrix.col A i))
    {..<n}"
  proof (rule sum_mat_cong, (auto simp add:h h_def))
    show "i. i < n  diag_mat D ! i m rank_1_proj (Matrix.col A i)  fc"
      using assms unfolding fc_def by (metis fc_mats_carrier h h_def) 
    show "i. i < n  diag_mat D ! i m rank_1_proj (Matrix.col A i)  fc"
      using assms unfolding fc_def by (metis fc_mats_carrier h h_def) 
  qed
  also have "... = A * D * (Complex_Matrix.adjoint A)" 
    using weighted_sum_rank_1_proj_unitary assms unfolding fc_def by simp
  finally have sg: "sum_mat g {..<n} = A * D * (Complex_Matrix.adjoint A)" .
  have "(per_col A f) * (per_diag D f) * 
    (Complex_Matrix.adjoint (per_col A f)) = 
    sum_mat (λi. diag_mat (per_diag D f) ! i m 
    rank_1_proj (Matrix.col (per_col A f) i)) {..<n}"
  proof (rule weighted_sum_rank_1_proj_unitary[symmetric])
    show "per_col A f  fc" using per_col_carrier[of A] assms unfolding fc_def 
      by simp
    show "per_diag D f  fc" using per_diag_carrier[of D] assms
      unfolding fc_def by simp
    show "diagonal_mat (per_diag D f)" using assms per_diag_diagonal[of D] 
      by simp
    show "unitary (per_col A f)" using per_col_unitary[of A] assms by simp
  qed
  also have "... = sum_mat g {..<n}"
  proof (rule sum_mat_cong, (auto simp add: g_def))
    show "i. i < n  diag_mat (per_diag D f) ! i m 
      rank_1_proj (Matrix.col (per_col A f) i)  fc" 
    proof -
      fix i
      assume "i < n"
      have "dim_vec (Matrix.col (per_col A f) i) = n" using assms per_col_col
        by (metis carrier_matD(1) dim_col)
      hence "rank_1_proj (Matrix.col (per_col A f) i)  fc" unfolding fc_def
        using rank_1_proj_carrier by blast
      thus "diag_mat (per_diag D f) ! i m 
        rank_1_proj (Matrix.col (per_col A f) i)  fc" unfolding fc_def by simp
    qed
    show "i. i < n  diag_mat D ! f i m 
      rank_1_proj (Matrix.col A (f i))  fc"
    proof -
      fix i
      assume "i < n"
      hence "f i < n" using f ` {..<n} = {..<n} by auto 
      hence "dim_vec (Matrix.col A (f i)) = n" using assms 
        by (metis carrier_matD(1) dim_col)
      hence "rank_1_proj (Matrix.col A (f i))  fc" unfolding fc_def
        using rank_1_proj_carrier by blast
      thus "diag_mat D ! f i m rank_1_proj (Matrix.col A (f i))  fc"
        unfolding fc_def by simp
    qed
    show "i. i < n 
         diag_mat (per_diag D f) ! i m 
           rank_1_proj (Matrix.col (per_col A f) i) =
         diag_mat D ! f i m rank_1_proj (Matrix.col A (f i))"
    proof-
      fix i
      assume "i < n"
      hence "f i < n" using f ` {..<n} = {..<n} by auto 
      have "Matrix.col (per_col A f) i = Matrix.col A (f i)"
        using per_col_col assms i < n by simp
      hence "rank_1_proj (Matrix.col (per_col A f) i) = 
        rank_1_proj (Matrix.col A (f i))"  by simp
      thus "diag_mat (per_diag D f) ! i m 
        rank_1_proj (Matrix.col (per_col A f) i) =
        diag_mat D ! f i m rank_1_proj (Matrix.col A (f i))" 
        using assms per_diag_diag_mat[of D] i < n f i < n by simp
    qed
  qed
  also have "... = A * D * (Complex_Matrix.adjoint A)" using sg by simp
  finally have "(per_col A f) * (per_diag D f) * 
    (Complex_Matrix.adjoint (per_col A f)) = 
    A * D * (Complex_Matrix.adjoint A)" .
  thus ?thesis by simp
qed

lemma sort_permutation:
  assumes "m = sort l"
  obtains f where "bij_betw f {..<length l} {..<length l}  
    (i<length l. l ! f i = m ! i)"
proof -
  have "length l = length m" using assms by simp
   have "mset l = mset m" using assms by simp
  from this obtain p where "p permutes {..<length m}" "permute_list p l = m" 
    by (metis length l = length m mset_eq_permutation) note pprop = this
  have "bij_betw p {..<length l} {..<length l}" 
    using pprop length l = length m
    by (simp add: permutes_imp_bij)
  moreover have "i<length l. l ! p i = m ! i" using pprop
    by (metis length l = length m permute_list_nth)
  ultimately have "f. bij_betw f {..<length l} {..<length l}  
    (i<length l. l ! f i = m ! i)" by auto
  thus ?thesis using that by auto
qed

lemma per_diag_sorted_Re:
  fixes B::"complex Matrix.mat"
  assumes "B carrier_mat n n"
  obtains f where "bij_betw f {..< n} {..< n}  
    map Re (diag_mat (per_diag B f)) = sort (map Re (diag_mat B))"
proof -
  define m where "m = sort (map Re (diag_mat B))"
  have "length m = length (map Re (diag_mat B))" unfolding m_def by simp
  also have "... = length (diag_mat B)" by simp
  also have "... = n" using assms unfolding diag_mat_def by simp
  finally have "length m = n" .
  from this obtain f where "bij_betw f {..<n} {..<n}  
    (i<n. (map Re (diag_mat B)) ! f i = m ! i)" 
    using sort_permutation[of m "map Re (diag_mat B)"] m_def by auto
    note fprop = this
  have l: "length (diag_mat (per_diag B f)) = length m" 
      using per_diag_carrier assms length m = n unfolding diag_mat_def
      by (metis carrier_matD(1) length_map map_nth)
  have "map Re (diag_mat (per_diag B f)) = m" 
  proof (rule list_eq_iff_nth_eq[THEN iffD2], intro conjI)
    show "length (map Re (diag_mat (per_diag B f))) = length m" using l by simp
    have "i<n. (map Re (diag_mat (per_diag B f)))!i = m!i"
    proof (intro allI impI)
      fix i
      assume "i< n"
      have "(map Re (diag_mat (per_diag B f)))!i = (map Re (diag_mat B))!(f i)"
      proof (rule per_diag_diag_mat_Re)
        show "B carrier_mat n n" using assms by simp
        show "i < n" using i < n .
        thus "f i < n" using fprop bij_betwE by blast
      qed
      also have "... = m!i" using fprop i < n by simp
      finally show "(map Re (diag_mat (per_diag B f)))!i = m!i" .
    qed 
    thus "i<length (map Re (diag_mat (per_diag B f))). 
      (map Re (diag_mat (per_diag B f)))!i = m ! i" using l length m = n by simp
  qed 
  thus ?thesis using that fprop unfolding m_def by auto
qed

lemma bij_unitary_diag:
  fixes A::"complex Matrix.mat"
  assumes "unitary_diag A B U"
  and "A  carrier_mat  n n"
  and "bij_betw f {..<n} {..<n}"
  and "0 < n"
shows "unitary_diag A (per_diag B f) (per_col U f)" 
proof (intro unitary_diagI)
  show "unitary (per_col U f)" using assms unitary_diagD(1) 
    unitary_diagD(3) per_col_unitary by (metis similar_mat_witD2(6))
  show "diagonal_mat (per_diag B f)" 
    using assms unitary_diagD(2) per_diag_diagonal
    by (metis similar_mat_witD2(5) unitary_diagD(1))
  have "A = U *  B * (Complex_Matrix.adjoint U)" using assms
    unitary_diagD similar_mat_witD2(3) unitary_diagD(1) by blast
  also have "... = (per_col U f) * (per_diag B f)
    * (Complex_Matrix.adjoint (per_col U f))" using assms per_col_mult_unitary
    by (meson similar_mat_witD2(5) similar_mat_witD2(6) unitary_diagD(1) 
        unitary_diagD(2) unitary_diagD(3))
  finally have eq: "A = per_col U f * per_diag B f * 
    Complex_Matrix.adjoint (per_col U f)" .
  show "similar_mat_wit A (per_diag B f) (per_col U f) 
    (Complex_Matrix.adjoint (per_col U f))" 
    unfolding similar_mat_wit_def Let_def
  proof (intro conjI)
    have "A carrier_mat n n" using assms by simp
    moreover have "per_diag B f  carrier_mat n n" using assms unitary_diagD(1) 
      per_diag_carrier[of B]
      by (metis carrier_matD(1) carrier_matD(2) similar_mat_witD2(5))
    moreover have "per_col U f  carrier_mat n n" using assms unitary_diagD(1)
      per_col_carrier[of U]
      by (metis similar_mat_witD2(6))
    moreover hence "Complex_Matrix.adjoint (per_col U f)  carrier_mat n n"
      by (simp add: adjoint_dim) 
    ultimately show 
      "{A, per_diag B f, per_col U f, Complex_Matrix.adjoint (per_col U f)} 
      carrier_mat (dim_row A) (dim_row A)" by auto
    show "per_col U f * Complex_Matrix.adjoint (per_col U f) = 1m (dim_row A)"
      using Complex_Matrix.unitary (per_col U f) assms(2)
        per_col U f  carrier_mat n n by auto
    show "Complex_Matrix.adjoint (per_col U f) * per_col U f = 1m (dim_row A)"
      using Complex_Matrix.unitary (per_col U f) assms 
        per_col U f  carrier_mat n n  by auto
  qed (simp add: eq)
qed

lemma hermitian_real_diag_sorted:
  assumes "A  carrier_mat n n"
  and "0 < n"
  and "hermitian A"
  obtains Bs Us where "real_diag_decomp A Bs Us  sorted (map Re (diag_mat Bs))"
proof -
  obtain U1 B1 where "real_diag_decomp A B1 U1" 
    using hermitian_real_diag_decomp[of A] assms by auto note ubprop = this
  hence "B1  carrier_mat n n" using assms unfolding real_diag_decomp_def
    by (meson unitary_diag_carrier(1))
  from this obtain f where "bij_betw f {..< n} {..< n}  
      map Re (diag_mat (per_diag B1 f)) = sort (map Re (diag_mat B1))" 
    using per_diag_sorted_Re by auto note fprop = this
  define Bs where "Bs = per_diag B1 f"
  define Us where "Us = per_col U1 f"
  have "unitary_diag A Bs Us" unfolding Bs_def Us_def
  proof (rule bij_unitary_diag)
    show "unitary_diag A B1 U1" using ubprop unfolding real_diag_decomp_def 
      by simp
    show "A  carrier_mat n n" using assms by simp
    show "bij_betw f {..<n} {..<n}" using fprop by simp
    show "0 < n" using assms by simp
  qed
  have "real_diag_decomp A Bs Us" unfolding real_diag_decomp_def 
  proof (simp add: unitary_diag A Bs Us)
    show "i<dim_row Bs. Bs $$ (i, i)  " unfolding Bs_def 
    proof (rule per_diag_real)  
      show br: "B1  carrier_mat (dim_row (per_diag B1 f)) 
        (dim_row (per_diag B1 f))"
        by (metis B1  carrier_mat n n carrier_matD(1) per_diag_carrier)
      thus "i<dim_row (per_diag B1 f). B1 $$ (i, i)  " using ubprop by auto
      show "bij_betw f {..<dim_row (per_diag B1 f)} 
        {..<dim_row (per_diag B1 f)}" using fprop
        by (metis br B1  carrier_mat n n carrier_matD(1)) 
    qed
  qed
  moreover have "sorted (map Re (diag_mat Bs))" using fprop unfolding Bs_def 
    by simp
  ultimately show ?thesis using that by simp
qed

section ‹Commuting Hermitian families›
text ‹This part is devoted to the proof that a finite family of commuting Hermitian matrices
is simultaneously diagonalizable.›

subsection ‹Intermediate properties›

lemma real_diag_decomp_mult_dbm_unit:
  assumes "A  carrier_mat n n"
  and "real_diag_decomp A B U"
  and "B = diag_block_mat Bl"
  and "length Ul = length Bl"
  and "i < length Bl. dim_col (Bl!i) = dim_row (Bl!i)"
  and "i < length Bl. dim_row (Bl!i) = dim_row (Ul!i)"
  and "i < length Bl. dim_col (Bl!i) = dim_col (Ul!i)"
  and "unitary (diag_block_mat Ul)"
  and "i<length Ul. Ul ! i * Bl ! i = Bl ! i * Ul ! i" 
shows "real_diag_decomp A B (U * (diag_block_mat Ul))"
  unfolding real_diag_decomp_def
proof (intro conjI allI impI)
  have "B carrier_mat n n"
    by (meson assms(1) assms(2) real_diag_decompD(1) unitary_diag_carrier(1))
  have "dim_row (diag_block_mat Ul) = dim_row B" 
    using diag_block_mat_dim_row_cong assms by blast
  moreover have "dim_col (diag_block_mat Ul) = dim_col B" 
    using diag_block_mat_dim_col_cong assms by blast
  ultimately have "diag_block_mat Ul  carrier_mat n n" using assms
    by (metis B  carrier_mat n n carrier_matD(1) carrier_matD(2) 
        carrier_mat_triv) 
  define Uf where "Uf = U * (diag_block_mat Ul)"
  show "i. i < dim_row B  B $$ (i, i)  "
    using assms real_diag_decompD(2) B  carrier_mat n n by auto
  show "unitary_diag A B Uf" unfolding unitary_diag_def
  proof
    show "diagonal_mat B" using assms real_diag_decompD(2)
      real_diag_decompD(1) unitary_diagD(2) by blast
    show "unitarily_equiv A B Uf" unfolding Uf_def
    proof (rule conjugate_eq_unitarily_equiv)
      show "A carrier_mat n n" using assms by simp
      show "unitarily_equiv A B U" using assms real_diag_decompD(1) 
        unfolding unitary_diag_def by simp
      show "diag_block_mat Ul  carrier_mat n n"
        using diag_block_mat Ul  carrier_mat n n .
      show "unitary (diag_block_mat Ul)" using assms by simp
      have  "mat_conj (diag_block_mat Ul)  (diag_block_mat Bl) = 
        diag_block_mat Bl" 
      proof (rule mat_conj_unit_commute)
        show "unitary (diag_block_mat Ul)" using unitary (diag_block_mat Ul) .
        show "diag_block_mat Bl  carrier_mat n n" 
          using assms B  carrier_mat n n by simp
        show "diag_block_mat Ul  carrier_mat n n" 
          using diag_block_mat Ul  carrier_mat n n .
        show "diag_block_mat Ul * diag_block_mat Bl = 
          diag_block_mat Bl * diag_block_mat Ul"
        proof (rule diag_block_mat_commute)
          show "length Ul = length Bl" using assms
            by simp
          show comm: "i<length Ul. Ul ! i * Bl ! i = Bl ! i * Ul ! i" 
            using assms by simp
          show "i<length Ul. dim_col (Ul ! i) = dim_row (Bl ! i)"
            using assms by presburger  
          thus "i<length Ul. dim_col (Bl ! i) = dim_row (Ul ! i)"
            by (metis comm index_mult_mat(2) index_mult_mat(3))   
        qed
      qed
      thus "diag_block_mat Ul * B * 
        Complex_Matrix.adjoint (diag_block_mat Ul) = B" 
        using B = diag_block_mat Bl unfolding mat_conj_def by simp
    qed
  qed
qed

lemma real_diag_decomp_block_set:
  assumes "Als  {}"
  and "0 < n"
  and " Al  Als. length Al = n"
  and "i < n.  Al  Als. dim_row (Al!i) = dim_col (Al!i)"
  and "i < n. U.  Al  Als.  B. real_diag_decomp (Al!i) B U"
shows "Ul. (length Ul = n  (i <n. Al  Als. 
  (dim_row (Ul!i) = dim_row (Al!i)  dim_col (Ul!i) = dim_col (Al!i)))
  ( Al  Als. Bl. (length Bl = n  
  real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat Ul))))"  
  using assms
proof (induct n arbitrary: Als)
  case 0
  then show ?case by simp
next
  case (Suc n)
  hence "U.  Al  Als.  B. real_diag_decomp (Al!0) B U" by simp
  from this obtain U0 where " Al  Als.  B. real_diag_decomp (Al!0) B U0" 
    by auto note u0 = this
  have u0_dim: "AlAls. 
      dim_row ([U0] ! 0) = dim_row (Al ! 0)  
      dim_col ([U0] ! 0) = dim_col (Al ! 0)"
  proof (intro allI impI ballI)
    fix Al
    assume  "Al  Als"
    have "[U0]!0 = U0" by simp
    have "B. real_diag_decomp (Al!0) B U0" using u0 Al  Als 
      by simp
    from this obtain B where "real_diag_decomp (Al!0) B U0" by auto
    moreover have "dim_row (Al!0) = dim_col (Al!0)" using Al Als Suc 
      by simp
    ultimately have "dim_row U0 = dim_row (Al!0)" 
      using unitary_diag_carrier(2)
      by (metis carrier_matD(1) carrier_matI real_diag_decompD(1))
    moreover have "dim_col U0 = dim_col (Al!0)" 
      using real_diag_decomp (Al!0) B U0 dim_row (Al!0) = dim_col (Al!0)
      using real_diag_decompD(1) unitary_diag_carrier(2)
      by (metis carrier_matD(2) carrier_mat_triv)
    ultimately show "dim_row ([U0] ! 0) = dim_row (Al ! 0)  
      dim_col ([U0] ! 0) = dim_col (Al ! 0)"
      by simp
  qed
  show ?case
  proof (cases "n = 0")
    case True
    hence " Al  Als. diag_block_mat Al = Al!0" using Suc 
      by (simp add: diag_block_mat_length_1)
    have " Al  Als. Bl. (length Bl = 1 
      real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
      (diag_block_mat [U0]))"
    proof 
      fix Al
      assume "Al  Als"
      hence "B. real_diag_decomp (Al!0) B U0" using u0 by simp
      from this obtain B where "real_diag_decomp (Al!0) B U0" by auto
      hence "real_diag_decomp (diag_block_mat Al) (diag_block_mat [B]) 
        (diag_block_mat [U0])"
        by (metis Al  Als AlAls. diag_block_mat Al = Al ! 0 
            diag_block_mat_singleton)
      moreover have "length [B] = 1" by simp
      ultimately show "Bl. (length Bl = 1 
        real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
        (diag_block_mat [U0]))" 
        by blast
    qed
    moreover have "length [U0] = 1" by simp
    moreover have "i<Suc n. AlAls. 
      dim_row ([U0] ! i) = dim_row (Al ! i)  
      dim_col ([U0] ! i) = dim_col (Al ! i)"
      using u0_dim n = 0 by simp
    ultimately have "length [U0] = Suc 0  
      (i<Suc n. AlAls. dim_row ([U0] ! i) = dim_row (Al ! i)  
        dim_col ([U0] ! i) = dim_col (Al ! i))  
      (AlAls. Bl. length Bl = Suc n  real_diag_decomp 
        (diag_block_mat Al) (diag_block_mat Bl) (diag_block_mat [U0]))" 
      using n=0 One_nat_def by metis
    thus ?thesis by (metis True) 
  next
    case False
    hence "0 < n" by simp
    define tAls where "tAls = tl `Als"
    have tex: "tAl tAls. Al  Als. tAl = tl Al" unfolding tAls_def by auto
    have "Ul. length Ul = n  
      (i <n. Al  tAls. 
      (dim_row (Ul!i) = dim_row (Al!i)  dim_col (Ul!i) = dim_col (Al!i)))
        (AltAls. Bl. length Bl = n  
      real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
      (diag_block_mat Ul))" 
    proof (rule Suc(1))
      show "tAls  {}" "0 < n" unfolding tAls_def by (auto simp add: 0 < n Suc)
      show "tAltAls. length tAl = n"
        using Suc(4) tex by fastforce
      show "i<n. U. AltAls. B. real_diag_decomp (Al ! i) B U"
      proof (intro allI impI)
        fix i
        assume "i < n"
        hence "U. AlAls. B. real_diag_decomp (Al ! (Suc i)) B U" 
          using Suc Suc_mono by presburger
        from this obtain U where 
          tu: "AlAls. B. real_diag_decomp (Al ! (Suc i)) B U" by auto
        have "tAltAls. B. real_diag_decomp (tAl ! i) B U"
        proof 
          fix tAl
          assume "tAl  tAls"
          hence "Al  Als. tAl = tl Al" using tex by simp
          from this obtain Al where "Al  Als" and "tAl = tl Al" by auto
          hence "tAl!i = Al!(Suc i)" by (simp add: Suc(4) i < n nth_tl) 
          moreover have "B. real_diag_decomp (Al!(Suc i)) B U" 
            using tu Al  Als by simp
          ultimately show "B. real_diag_decomp (tAl ! i) B U" by simp
        qed
        thus "U. AltAls. B. real_diag_decomp (Al ! i) B U" by auto
      qed
      show "i < n. AltAls.  dim_row (Al!i) = dim_col (Al!i)"
        by (metis Suc(5) tAltAls. length tAl = n not_less_eq nth_tl tex)
    qed
    from this obtain Ul where "length Ul = n" and 
      "i <n. Al  tAls. 
        (dim_row (Ul!i) = dim_row (Al!i)  dim_col (Ul!i) = dim_col (Al!i))"
      "(AltAls. Bl. length Bl = n  
      real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
      (diag_block_mat Ul))" by auto note ulprop = this
    have "AlAls. Bl. length Bl = Suc n  
      real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
      (diag_block_mat (U0#Ul))" 
    proof
      fix Al
      assume "Al  Als"
      hence "0 < length Al" using Suc by simp
      hence "Al = hd Al # (tl Al)" by simp
      have "B. real_diag_decomp (Al!0) B U0" using u0 Al Als by simp
      from this obtain B0 where b0: "real_diag_decomp (Al!0) B0 U0" by auto
      hence "real_diag_decomp (hd Al) B0 U0"
        by (metis Al = hd Al # tl Al nth_Cons_0)
      have "tl Al  tAls" using Al  Als unfolding tAls_def by simp
      hence "Bl. length Bl = n  
        real_diag_decomp (diag_block_mat (tl Al)) (diag_block_mat Bl) 
        (diag_block_mat Ul)" using ulprop by simp 
      from this obtain Bl where "length Bl = n" and 
        rl: "real_diag_decomp (diag_block_mat (tl Al)) (diag_block_mat Bl) 
        (diag_block_mat Ul)" by auto
      have "dim_row (diag_block_mat (tl Al)) = dim_col (diag_block_mat (tl Al))" 
        using Suc Al  Als diag_block_mat_dim_row_col_eq
        by (metis (no_types, lifting) Al = hd Al # tl Al length_Cons lessI 
            less_trans_Suc nth_tl)
      moreover have "dim_row (Al ! 0) = dim_col (Al ! 0)" 
        using Suc Al  Als by simp
      ultimately have "real_diag_decomp (diag_block_mat ((hd Al)#(tl Al))) 
        (diag_block_mat (B0#Bl)) (diag_block_mat (U0#Ul))" 
        using  four_block_real_diag_decomp[OF rl b0] diag_block_mat.simps(2)  
          real_diag_decomp_hermitian
        by (metis Al = hd Al # tl Al b0 four_block_real_diag_decomp nth_Cons_0 rl)
      moreover have "length (B0#Bl) = Suc n" using length Bl = n by simp
      ultimately show "Bl. length Bl = Suc n  
      real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
      (diag_block_mat (U0#Ul))" using Al = hd Al # tl Al by metis
    qed
    moreover have "length (U0#Ul) = Suc n" using ulprop by simp
    moreover have "i<Suc n. AlAls. dim_row ((U0#Ul) ! i) = dim_row (Al ! i)  
      dim_col ((U0#Ul) ! i) = dim_col (Al ! i)"
    proof (intro allI impI ballI)
      fix i Al
      assume "i < Suc n" and "Al  Als"
      show "dim_row ((U0 # Ul) ! i) = dim_row (Al ! i)  
        dim_col ((U0 # Ul) ! i) = dim_col (Al ! i)"
      proof (cases "i = 0")
        case True
        then show ?thesis using Al  Als u0_dim by simp
      next
        case False
        hence "j. i = Suc j" by (simp add: not0_implies_Suc)
        from this obtain j where "i = Suc j" by auto
        hence "(U0#Ul)!i = Ul!j" by simp
        have "tl Al  tAls" using Al  Als unfolding tAls_def by simp
        moreover have "Al!i = (tl Al)!j" using i = Suc j
          by (metis Suc.prems(3) Zero_not_Suc Al  Als diag_block_mat.cases 
              list.sel(3) list.size(3) nth_Cons_Suc) 
        ultimately show ?thesis using (U0#Ul)!i = Ul!j
          by (metis Suc_less_SucD i < Suc n i = Suc j ulprop(2)) 
      qed
    qed
    ultimately show ?thesis by blast
  qed
qed

lemma real_diag_decomp_eq_comps_props:
  assumes "Ap carrier_mat n n"
  and "0 < n"
  and "real_diag_decomp Ap Bs Us  sorted (map Re (diag_mat Bs))"
shows "Bs  carrier_mat n n" "diagonal_mat Bs" "unitary Us"
  "Us  carrier_mat n n" "diag_diff Bs (eq_comps (diag_mat Bs))"
  "eq_comps (diag_mat Bs)  []" "diag_mat Bs  []"
proof -
  show  "Bs  carrier_mat n n" 
    using assms real_diag_decompD(1) unitary_diag_carrier(1) 
    by blast
  thus "diag_mat Bs  []" using 0 < n unfolding diag_mat_def by simp
  show "diagonal_mat Bs" using assms
    using real_diag_decompD(1) unitary_diagD(2) by blast
  show "unitary Us" 
    using  unitary_diagD(3) assms unfolding real_diag_decomp_def by auto
  show "Us  carrier_mat n n" 
    using assms real_diag_decompD(1) unitary_diag_carrier(2)      
    by blast 
  define eqcl where "eqcl = eq_comps (diag_mat Bs)"
  show "diag_diff Bs eqcl" unfolding eqcl_def
  proof (rule cpx_sorted_diag_diff)
    show "Bs  carrier_mat n n" using Bs  carrier_mat n n .
    show "sorted (map Re (diag_mat Bs))" using assms by simp
    show "i<n. Bs $$ (i, i)  " 
      using assms real_diag_decompD(2) Bs  carrier_mat n n by auto
  qed  
  show "eqcl  []" using eq_comps_not_empty[of "diag_mat Bs"] 
    Bs  carrier_mat n n assms 
    unfolding eqcl_def diag_mat_def
    by (simp add: assms)
qed

lemma commuting_conj_mat_set_props:
  fixes As::"'a::conjugatable_field Matrix.mat set" 
    and U::"'a Matrix.mat"
  assumes "finite As"
  and "card As  i"
  and "A As. hermitian A  A carrier_mat n n"
  and " A As.  B  As. A*B = B*A"
  and "unitary U"
  and "U  carrier_mat n n"
  and "CjA = (λA2. mat_conj (Complex_Matrix.adjoint U) A2)`As"
shows "finite CjA" "card CjA  i"
  "A CjA. A carrier_mat n n  hermitian A" 
  " C1 CjA. C2 CjA. C1*C2 = C2*C1"
proof -
  define Cj where "Cj = (λA2. mat_conj (Complex_Matrix.adjoint U) A2)"
  have "CjA = Cj`As" using assms unfolding Cj_def by simp
  show "finite CjA"  using assms  by simp
  show "card CjA  i"  
    using card As  i finite As card_image_le dual_order.trans assms
     by blast
  show "A CjA. A carrier_mat n n  hermitian A" 
  proof(intro ballI conjI)
    fix A
    assume "A CjA"
    hence "nA  As. A = Cj nA" using assms unfolding Cj_def by auto
    from this obtain nA where "nA As" and "A = Cj nA" by auto
    have "hermitian nA" using assms nA  As by auto
    thus "hermitian A"  
      using assms A = Cj nA hermitian_mat_conj'[of nA n U] nA As Cj_def
        mat_conj_adjoint by fastforce       
    show "A carrier_mat n n" using nA As A = Cj nA unfolding Cj_def
      by (metis hermitian A adjoint_dim_row assms(6) carrier_matD(2) 
          hermitian_square index_mult_mat(2) mat_conj_adjoint)
  qed
  show " C1 CjA. C2 CjA. C1*C2 = C2*C1"
  proof (intro ballI)
    fix C1 C2
    assume "C1  CjA" and "C2 CjA"
    hence " A1 As. C1 = mat_conj (Complex_Matrix.adjoint U) A1" 
      using assms unfolding Cj_def by auto
    from this obtain A1 where "A1 As" and
      "C1 = mat_conj (Complex_Matrix.adjoint U) A1" 
      by auto
    have " A2 As. C2 = mat_conj (Complex_Matrix.adjoint U) A2" 
      using C2 CjA assms unfolding  Cj_def by auto
    from this obtain A2 where "A2 As" and
      "C2 = mat_conj (Complex_Matrix.adjoint U) A2" 
      by auto
    have "mat_conj (Complex_Matrix.adjoint U) A1 * 
      mat_conj (Complex_Matrix.adjoint U) A2 =
      mat_conj (Complex_Matrix.adjoint U) A2 * 
      mat_conj (Complex_Matrix.adjoint U) A1"
    proof (rule mat_conj_commute)
      show "unitary U" using unitary U .
      show "A1 carrier_mat n n" using A1 As assms by simp
      show "A2 carrier_mat n n" using A2 As assms by simp
      show "U  carrier_mat n n" using U  carrier_mat n n .
      show "A1 * A2 = A2 * A1" using A1 As A2 As assms by simp
    qed
    thus "C1 * C2 = C2 * C1"
      using C1 = mat_conj (Complex_Matrix.adjoint U) A1
        C2 = mat_conj (Complex_Matrix.adjoint U) A2
      by simp
  qed
qed

lemma commute_extract_diag_block_eq:
  fixes Ap::"complex Matrix.mat"
  assumes "Ap carrier_mat n n"
  and "0 < n"
  and "real_diag_decomp Ap Bs Us  sorted (map Re (diag_mat Bs))"
  and "finite Afp"
  and "card Afp  i"
  and "AAfp. hermitian A  A  carrier_mat n n"
  and "AAfp. BAfp. A * B = B * A"
  and "A Afp. Ap * A = A * Ap"
  and "CjA = (λA2. mat_conj (Complex_Matrix.adjoint Us) A2)`Afp"
  and "eqcl = eq_comps (diag_mat Bs)"
  shows  "C  CjA. C = diag_block_mat (extract_subdiags C eqcl)"
proof
  note ubprops = real_diag_decomp_eq_comps_props[OF assms(1) assms(2) assms(3)]
  note cjprops = commuting_conj_mat_set_props[OF assms(4) assms(5) assms(6) 
      assms(7) ubprops(3) ubprops(4) assms(9)]
  fix C
  assume "C CjA"
  hence "Ac  Afp. C = mat_conj (Complex_Matrix.adjoint Us) Ac" 
    using assms by auto
  from this obtain Ac where "Ac  Afp" and 
    "C = mat_conj (Complex_Matrix.adjoint Us) Ac" by auto
  show "C = diag_block_mat (extract_subdiags C eqcl)" 
  proof (rule diag_compat_extract_subdiag)
    show "C  carrier_mat n n" using cjprops C CjA by simp
    show  "diag_compat C eqcl" 
    proof (rule commute_diag_compat)
      show "Bs  carrier_mat n n" using Bs  carrier_mat n n .
      show "diag_diff Bs eqcl" using ubprops assms by simp
      show "diagonal_mat Bs" using diagonal_mat Bs .
      show "C  carrier_mat n n" using C  carrier_mat n n .
      have "Bs * (Complex_Matrix.adjoint Us * Ac * Us) = 
        Complex_Matrix.adjoint Us * Ac * Us * Bs"
      proof (rule unitarily_equiv_commute)
        show "unitarily_equiv Ap Bs Us" using assms real_diag_decompD(1)
          by simp
        show "Ap * Ac = Ac * Ap" using assms Ac  Afp by simp
      qed
      thus "C * Bs = Bs * C" 
        using C = mat_conj (Complex_Matrix.adjoint Us) Ac
        by (metis mat_conj_adjoint)
    qed
  qed
qed

lemma extract_dbm_eq_component_commute:
  assumes "CCs. C = diag_block_mat (extract_subdiags C l)"
  and "C1Cs. C2Cs. C1 * C2 = C2 * C1"
  and "ExC = (λA. extract_subdiags A l)`Cs"
  and "j < length l"
  and "Exi = (λA. (A!j))` ExC"
  and "Al  Exi"
  and "Bl Exi"
  shows "Al * Bl = Bl * Al" 
proof -
  define ncl where "ncl = length l"
  have "AlExC. length Al = ncl"
    by (simp add: assms extract_subdiags_length ncl_def)
  have "Ea  ExC. Al = Ea!j" using assms by auto
  from this obtain Ea where "Ea ExC" and "Al = Ea!j" by auto
  have "Eb  ExC. Bl = Eb!j" using assms by auto
  from this obtain Eb where "Eb ExC" and "Bl = Eb!j" by auto
  have "j<ncl. EExC. E ! j  carrier_mat (l ! j) (l ! j)"
    by (metis (no_types, lifting) assms(3) extract_subdiags_carrier 
        imageE ncl_def)
  hence "i < ncl. AlExC. dim_row (Al ! i) = dim_col (Al ! i)"
    by (metis carrier_matD(1) carrier_matD(2))
  have "Ea!j * Eb!j = Eb!j * Ea!j" 
  proof (rule diag_block_mat_commute_comp)
    show "length Ea = length Eb"
      by (simp add: Ea  ExC Eb  ExC AlExC. length Al = ncl)
    show "j < length Ea"
      by (metis Eb  ExC AlExC. length Al = ncl j < length l 
          ncl_def length Ea = length Eb)
    show "i<length Ea. dim_row (Ea ! i) = dim_col (Ea ! i)"
      by (simp add: Ea  ExC AlExC. length Al = ncl 
          i < ncl. AlExC. dim_row (Al ! i) = dim_col (Al ! i))
    show "i<length Ea. dim_row (Ea ! i) = dim_row (Eb ! i)"
      by (metis Ea  ExC Eb  ExC AlExC. length Al = ncl 
          j<ncl. EExC. E ! j  carrier_mat (l ! j) (l ! j) 
          carrier_matD(1))
    show "i<length Ea. dim_col (Ea ! i) = dim_col (Eb ! i)"
      using Ea  ExC Eb  ExC AlExC. length Al = ncl 
        i<length Ea. dim_row (Ea ! i) = dim_row (Eb ! i) 
        i<ncl. AlExC. dim_row (Al ! i) = dim_col (Al ! i) by auto
    have "Cea  Cs. Ea = extract_subdiags Cea l" 
      using Ea  ExC assms by auto
    from this obtain Cea where "Cea Cs" and 
      "Ea = extract_subdiags Cea l" by auto
    hence cea: "Cea = diag_block_mat Ea"
      by (simp add: CCs. C = 
        diag_block_mat (extract_subdiags C l))
    have "Ceb  Cs. Eb = extract_subdiags Ceb l" 
      using Eb  ExC assms by auto
    from this obtain Ceb where "Ceb Cs" and 
      "Eb = extract_subdiags Ceb l" by auto
    hence "Ceb = diag_block_mat Eb"
      by (simp add: CCs. C = 
        diag_block_mat (extract_subdiags C l))
    moreover have "Cea * Ceb = Ceb * Cea"
      by (simp add: Cea  Cs Ceb  Cs 
          C1Cs. C2Cs. C1 * C2 = C2 * C1)
    ultimately show "diag_block_mat Ea * diag_block_mat Eb = 
      diag_block_mat Eb * diag_block_mat Ea" using cea by simp
  qed
  thus "Al * Bl = Bl * Al" using Al = Ea!j Bl = Eb!j by simp
qed

lemma extract_comm_real_diag_decomp:
  fixes CjA::"complex Matrix.mat set"
  assumes "(Af::complex Matrix.mat set) n . finite Af 
    card Af  i 
    Af  {} 
    (A. A  Af  A  carrier_mat n n) 
    0 < n  (A. A  Af  hermitian A)  
    (A B. A  Af  B  Af  A * B = B * A)  
    U. AAf. B. real_diag_decomp A B U"
  and "finite CjA"
  and "CjA  {}"
  and "card CjA  i"
  and "CCjA. C = diag_block_mat (extract_subdiags C eqcl)"
  and "C1CjA. C2CjA. C1 * C2 = C2 * C1"
  and "Exc = (λA. extract_subdiags A eqcl)`CjA"
  and " E Exc. list_all (λB. 0 < dim_row B  hermitian B) E"
  and "i < length eqcl. 0 < eqcl!i"
  shows "i<length eqcl. U. AlExc. B. real_diag_decomp (Al ! i) B U"
proof (intro allI impI)
  define ncl where "ncl = length eqcl"
  fix j
  assume "j < ncl"
  define Exi where "Exi = (λl. l!j)`Exc"
  have "finite Exi" using assms unfolding Exi_def by simp
  have "card Exi  i" using assms unfolding Exi_def
    by (metis card_image_le image_image le_trans)
  have exfl: "Ej  Exi. Fj  CjA. Ej = (extract_subdiags Fj eqcl)!j"
  proof
    fix Ej
    assume "Ej  Exi"
    hence "El  Exc. Ej = El!j" unfolding Exi_def by auto
    from this obtain El where "El  Exc" and "Ej = El!j" by auto
    hence "Fl  CjA. El = extract_subdiags Fl eqcl" 
      using assms by auto
    from this obtain Fl where "Fl  CjA" and 
      "El = extract_subdiags Fl eqcl" by auto
    thus "Fj  CjA. Ej = (extract_subdiags Fj eqcl)!j" using Ej = El!j 
      by auto
  qed
  have "U. AlExi. B. real_diag_decomp (Al) B U" 
  proof (rule assms(1))
    show "finite Exi" using finite Exi .
    show "card Exi  i" using card Exi <= i .
    show "Exi  {}" using CjA  {} using assms unfolding Exi_def by auto
    show "0 < eqcl!j" using j < ncl ncl_def assms by simp
    show "Al. Al  Exi  Al  carrier_mat (eqcl ! j) (eqcl ! j)" 
    proof -
      fix Al
      assume "Al  Exi"              
      hence "Fl  CjA. Al = (extract_subdiags Fl eqcl)!j" using exfl 
        by simp
      from this obtain Fl where "Fl  CjA" and 
        "Al = (extract_subdiags Fl eqcl)!j" by auto
      thus "Al  carrier_mat (eqcl ! j) (eqcl ! j)"
        using extract_subdiags_carrier[of j eqcl] j < ncl 
        unfolding Exi_def ncl_def by simp
    qed
    show "Al. Al  Exi  hermitian Al"
    proof -
      fix Al 
      assume "Al Exi"
      hence "El  Exc. Al = El!j" unfolding Exi_def by auto
      from this obtain El where "El  Exc" and "Al = El!j" by auto
      thus "hermitian Al" using assms j < ncl ncl_def
        by (metis (no_types, lifting) extract_subdiags_length image_iff 
            list_all_length) 
    qed
    show "Al Bl. Al  Exi  Bl  Exi  Al * Bl = Bl * Al" 
    proof -
      fix Al Bl
      assume "Al  Exi" and "Bl  Exi"
      show "Al*Bl = Bl * Al" 
      proof (rule extract_dbm_eq_component_commute[of CjA eqcl])
        show "Al  Exi" using Al  Exi .
        show "Bl  Exi" using Bl  Exi .
        show "CCjA. C = diag_block_mat (extract_subdiags C eqcl)"
          using CCjA. C = diag_block_mat (extract_subdiags C eqcl) .
        show "C1CjA. C2CjA. C1 * C2 = C2 * C1" 
          using C1CjA. C2CjA. C1 * C2 = C2 * C1 .
        show "j < length eqcl" using j < ncl ncl_def by simp
        show "Exi = (λA. A ! j) ` Exc" using Exi_def by simp
        show "Exc = (λA. extract_subdiags A eqcl) ` CjA" 
          using assms by simp
      qed
    qed
  qed
  thus "U. AlExc. B. real_diag_decomp (Al ! j) B U" unfolding Exi_def
    by simp
qed

subsection ‹The main result›

theorem commuting_hermitian_family_diag:
  fixes Af::"complex Matrix.mat set"
  assumes "finite Af"
  and "Af  {}"
  and "A. A Af  A carrier_mat n n"
  and "0 < n"
  and "A. A  Af  hermitian A"
  and "A B. A  Af  B Af  A * B = B * A"
shows " U.  A Af. B. real_diag_decomp A B U" using assms
proof -
  define i where "i = card Af"
  have "card Af  i"
    by (simp add: i_def)
  from assms(1) this assms(2-) show ?thesis
  proof (induct i arbitrary: Af n)
    case 0
    then have "Af = {}" by simp
    then show ?case using 0 by simp
  next
    case (Suc i)
    hence " A. A Af" by blast
    from this obtain Ap where "Ap  Af" by auto
    define Afp where "Afp = Af - {Ap}"
    have "finite Afp" using Suc unfolding Afp_def by simp
    have "card Afp  i" using card Af  Suc i Ap  Af 
      unfolding Afp_def by simp
    have "AAfp. hermitian A  A  carrier_mat n n" using Suc
      by (metis Afp_def Diff_subset subset_iff)
    have "AAfp. BAfp. A * B = B * A" using Suc 
      by (metis Afp_def Diff_subset subset_iff)
    have "A Afp. Ap * A = A * Ap" using Suc
      by (simp add: Afp_def Ap  Af)
    have "hermitian Ap" "Ap carrier_mat n n" "0 < n" using Ap  Af Suc by auto
    from this obtain Bs Us where rd: "real_diag_decomp Ap Bs Us  
      sorted (map Re (diag_mat Bs))"
      using hermitian_real_diag_sorted[of Ap] by auto note ub = this
    note ubprops = real_diag_decomp_eq_comps_props[OF Ap  carrier_mat n n 0 < n ub]   
    define eqcl where "eqcl = eq_comps (diag_mat Bs)"
    have "diag_diff Bs eqcl" using ubprops unfolding eqcl_def by simp
    have "eqcl  []" using ubprops unfolding eqcl_def by simp
    hence "eqcl = hd eqcl # (tl eqcl)" by simp
    define esubB where "esubB = extract_subdiags Bs eqcl"
    have ebcar: "i < length esubB. esubB ! i  carrier_mat (eqcl!i) (eqcl!i)" 
      using extract_subdiags_carrier[of _ eqcl Bs]
      by (simp add: esubB_def extract_subdiags_length)
    have "Bs = diag_block_mat esubB" unfolding esubB_def eqcl_def
    proof (rule diagonal_extract_eq)
      show "Bs  carrier_mat n n" using Bs  carrier_mat n n .
      show "diagonal_mat Bs" using ubprops real_diag_decompD(2)
          real_diag_decompD(1) unitary_diagD(2) by blast
    qed
    show ?case
    proof (cases "Afp = {}")
      case True
      hence "Af = {Ap}" using Afp = Af - {Ap}
        by (simp add: Suc(4) subset_singleton_iff)     
      then show ?thesis using rd Af = {Ap} by auto 
    next
      case False   
      define Cj where "Cj = (λA2. mat_conj (Complex_Matrix.adjoint Us) A2)"
      define CjA where "CjA = Cj`Afp"
      have "CjA = (λA2. (mat_conj (Complex_Matrix.adjoint Us) A2)) ` Afp" 
        using CjA_def Cj_def by simp
      note cjprops = commuting_conj_mat_set_props[OF finite Afp card Afp  i
        AAfp. hermitian A  A  carrier_mat n n 
        AAfp. BAfp. A * B = B * A
        unitary Us Us  carrier_mat n n
        CjA = (λA2. mat_conj (Complex_Matrix.adjoint Us) A2) ` Afp]    
      have "C  CjA. C = diag_block_mat (extract_subdiags C eqcl)" 
      proof (rule commute_extract_diag_block_eq[OF Ap carrier_mat n n 
            0 < n rd finite Afp _ 
            AAfp. hermitian A  A  carrier_mat n n], 
            auto simp add: eqcl_def CjA_def Cj_def)
        show "A B. A  Afp  B  Afp  A * B = B * A"
          by (simp add: AAfp. BAfp. A * B = B * A)
        show "A. A  Afp  Ap * A = A * Ap" 
          using  A  Afp. Ap * A = A * Ap by simp
      qed
      define Ex where "Ex = (λA. extract_subdiags A eqcl)`CjA"
      have "finite Ex" using finite CjA unfolding Ex_def by simp
      have "Ex  {}" using False unfolding Ex_def CjA_def by simp
      have "card Ex  i" using card CjA  i unfolding Ex_def
        by (metis finite CjA basic_trans_rules(23) card_image_le)
      have exall: " E Ex. list_all (λB. 0 < dim_row B  hermitian B) E"
      proof
        fix E
        assume "E Ex"
        hence "nA  CjA. E = extract_subdiags nA eqcl" unfolding Ex_def by auto
        from this obtain nA where "nA CjA" and "E = extract_subdiags nA eqcl" 
          by auto
        have "list_all (λB. 0 < dim_row B  hermitian B) 
          (extract_subdiags nA eqcl)"
        proof (rule hermitian_extract_subdiags)
          show "hermitian nA" using A CjA. A  carrier_mat n n  hermitian A 
              nA CjA by simp
          show "list_all ((<) 0) eqcl" unfolding eqcl_def
            by (metis eqcl  [] eq_comps.simps(1) eq_comps_gt_0 eqcl_def)
          show "sum_list eqcl  dim_row nA" 
            using A CjA. A  carrier_mat n n  hermitian A 
              nA CjA unfolding eqcl_def
            by (metis Bs  carrier_mat n n carrier_matD(1) 
                eq_comp_sum_diag_mat le_refl)
        qed
        thus "list_all (λB. 0 < dim_row B  hermitian B) E" 
          using E = extract_subdiags nA eqcl by simp
      qed      
      define ncl where "ncl = length eqcl"
      have "j < ncl. E  Ex. E!j  carrier_mat (eqcl!j) (eqcl!j)"
      proof (intro allI impI ballI)
        fix E j
        assume "j < ncl" and "E  Ex"
        thus "E ! j  carrier_mat (eqcl ! j) (eqcl ! j)" unfolding Ex_def
          using extract_subdiags_carrier ncl_def by blast
      qed
      have "Ul. (length Ul = ncl 
        (i <ncl. Al  Ex. 
        (dim_row (Ul!i) = dim_row (Al!i)  dim_col (Ul!i) = dim_col (Al!i)))
        ( Al  Ex. Bl. (length Bl = ncl  
        real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
        (diag_block_mat Ul))))" 
      proof (rule real_diag_decomp_block_set)
        show "Ex  {}" using Afp  {} unfolding Ex_def CjA_def by auto
        show "0 < ncl" unfolding ncl_def using eqcl [] by simp
        show "AlEx. length Al = ncl" unfolding ncl_def Ex_def
          by (simp add: extract_subdiags_length)
        show "i<ncl. AlEx. dim_row (Al ! i) = dim_col (Al ! i)"
        proof (intro allI impI ballI)
          fix i Al
          assume "i < ncl" and "Al  Ex"
          thus "dim_row (Al ! i) = dim_col (Al ! i)" using exall
            by (metis (mono_tags, lifting) AlEx. length Al = ncl 
                carrier_matD(2) hermitian_square list_all_length)
        qed
        show " i<ncl. U. AlEx. B. real_diag_decomp (Al ! i) B U" unfolding ncl_def 
        proof (rule extract_comm_real_diag_decomp[of i CjA, OF Suc(1)], 
            auto simp add: exall Ex_def)
          show "finite CjA" using finite CjA .
          show "card CjA  i" using card CjA  i .
          show "C. C  CjA  C = diag_block_mat (extract_subdiags C eqcl)"
            using C  CjA. C = diag_block_mat (extract_subdiags C eqcl) by simp
          show "C1 C2. C1  CjA  C2  CjA  C1 * C2 = C2 * C1" 
            using cjprops by simp
          show "i. i < length eqcl  0 < eqcl!i" 
          proof -
            fix il
            assume "il < length eqcl"
            thus "0 < eqcl!il" using eq_comps_gt_0[OF diag_mat Bs  []]
                list_all_length[of "(<) 0" "eq_comps (diag_mat Bs)"] 
              unfolding eqcl_def by simp 
          qed
          show "CjA = {}  False" by (simp add: CjA_def False)
        qed
      qed
      from this obtain Ul where "length Ul = ncl" and 
        dimul: "(i <ncl. Al  Ex. 
        (dim_row (Ul!i) = dim_row (Al!i)  dim_col (Ul!i) = dim_col (Al!i)))" and
        ul: " Al  Ex. Bl. (length Bl = ncl  
          real_diag_decomp (diag_block_mat Al) (diag_block_mat Bl) 
          (diag_block_mat Ul))" 
        by auto
      define Uf where "Uf = Us * (diag_block_mat Ul)"
      have afp:"A  Afp. Bl. real_diag_decomp A (diag_block_mat Bl) Uf"
      proof
        fix A
        assume "A Afp"
        define Ca where "Ca = mat_conj (Complex_Matrix.adjoint Us) A"
        define Eca where "Eca = extract_subdiags Ca eqcl"
        have "Ca  CjA" using A Afp
          unfolding Ca_def CjA_def Cj_def by simp
        hence "Ca = diag_block_mat Eca" unfolding Eca_def
          using C CjA. C = diag_block_mat (extract_subdiags C eqcl) by simp
        have "Eca  Ex" unfolding Ex_def Eca_def using Ca  CjA by simp
        hence "Bl. (length Bl = ncl  
          real_diag_decomp (diag_block_mat Eca) (diag_block_mat Bl) 
          (diag_block_mat Ul))" using ul by simp
        from this obtain Ecb where "length Ecb = ncl" and
          "real_diag_decomp (diag_block_mat Eca) (diag_block_mat Ecb) 
          (diag_block_mat Ul)" by auto
        hence "real_diag_decomp Ca (diag_block_mat Ecb) 
          (diag_block_mat Ul)" using Ca = diag_block_mat Eca by simp
        have "real_diag_decomp A (diag_block_mat Ecb) Uf" unfolding Uf_def
        proof (rule unitary_conjugate_real_diag_decomp)
          show "A carrier_mat n n" using A Afp unfolding Afp_def
            by (simp add: Suc(5))
          show "Us  carrier_mat n n" using Us  carrier_mat n n .
          show "unitary Us" using unitary Us .
          show "real_diag_decomp (mat_conj (Complex_Matrix.adjoint Us) A) 
            (diag_block_mat Ecb) (diag_block_mat Ul)"
            using real_diag_decomp Ca (diag_block_mat Ecb) 
              (diag_block_mat Ul) unfolding Ca_def by simp
        qed
        thus "Bl. real_diag_decomp A (diag_block_mat Bl) Uf" by blast
      qed
      have "real_diag_decomp Ap Bs Uf" unfolding Uf_def
      proof (rule real_diag_decomp_mult_dbm_unit)
        show "Ap carrier_mat n n" using Ap carrier_mat n n .
        show "real_diag_decomp Ap Bs Us" using ub by simp
        show "Bs = diag_block_mat esubB" using Bs = diag_block_mat esubB .
        show "length Ul = length esubB" using length Ul = ncl
          by (simp add: esubB_def extract_subdiags_length ncl_def) 
        show "i<length esubB. dim_col (esubB ! i) = dim_row (esubB ! i)"
          by (metis carrier_matD(1) carrier_matD(2) ebcar)
        have "length esubB = ncl" using length Ul = length esubB 
              length Ul = ncl ncl_def by auto
        show roweq:"i<length esubB. dim_row (esubB ! i) = dim_row (Ul ! i)" 
          using ebcar dimul length esubB = ncl  Ex {}
            j < ncl. E  Ex. E!j  carrier_mat (eqcl!j) (eqcl!j)           
          by (metis all_not_in_conv carrier_matD(1))        
        show coleq:"i<length esubB. dim_col (esubB ! i) = dim_col (Ul ! i)"
          using ebcar dimul length esubB = ncl  Ex {}
            j < ncl. E  Ex. E!j  carrier_mat (eqcl!j) (eqcl!j)           
          by (metis all_not_in_conv carrier_matD(2))
        show "unitary (diag_block_mat Ul)" using ul
          by (metis CjA_def False all_not_in_conv image_is_empty Ex_def 
              real_diag_decompD(1) unitary_diagD(3))  
        show "i<length Ul. Ul ! i * esubB ! i = esubB ! i * Ul ! i"
        proof (intro allI impI)
          fix i
          assume "i < length Ul"
          show "Ul ! i * esubB ! i = esubB ! i * Ul ! i" 
            unfolding esubB_def eqcl_def 
          proof (rule extract_subdiags_comp_commute[symmetric])
            show "diagonal_mat Bs" using diagonal_mat Bs .
            show "Bs carrier_mat n n" using Bs  carrier_mat n n .
            show "0 < n" using 0 < n .
            show "i < length (eq_comps (diag_mat Bs))" 
              using i < length Ul length Ul = length esubB 
                extract_subdiags_length 
              unfolding esubB_def eqcl_def by metis
            show "Ul ! i  carrier_mat (eq_comps (diag_mat Bs) ! i) 
              (eq_comps (diag_mat Bs) ! i)"
              using dimul j < ncl. E  Ex. E!j  carrier_mat (eqcl!j) (eqcl!j) 
              Ex {} unfolding ncl_def eqcl_def
              by (metis coleq roweq 
                  i<length esubB. dim_col (esubB ! i) = dim_row (esubB ! i)  
                  i < length Ul length Ul = length esubB carrier_matD(2) 
                  carrier_matI ebcar eqcl_def)
          qed
        qed
      qed
      hence "B. real_diag_decomp Ap B Uf" by blast
      hence " A Af. B. real_diag_decomp A B Uf" using afp 
        unfolding Afp_def by auto
      thus "U. AAf. B. real_diag_decomp A B U" by blast
    qed
  qed
qed

end