diff --git a/thys/Commuting_Hermitian/Commuting_Hermitian.thy b/thys/Commuting_Hermitian/Commuting_Hermitian.thy --- a/thys/Commuting_Hermitian/Commuting_Hermitian.thy +++ b/thys/Commuting_Hermitian/Commuting_Hermitian.thy @@ -1,3721 +1,3719 @@ (* 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 = 0\<^sub>m k (n-k)" "B3 = 0\<^sub>m (n-k) k" proof (intro eq_matI) show "dim_row B2 = dim_row (0\<^sub>m k (n - k))" using assms unfolding split_block_def Let_def by simp show "dim_col B2 = dim_col (0\<^sub>m k (n - k))" using assms unfolding split_block_def Let_def by simp fix i j assume "i < dim_row (0\<^sub>m k (n - k))" and "j < dim_col (0\<^sub>m 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) = 0\<^sub>m k (n - k) $$ (i, j)" using ijprop by simp next show "B3 = 0\<^sub>m (n-k) k" proof (intro eq_matI) show "dim_row B3 = dim_row (0\<^sub>m (n - k) k)" using assms unfolding split_block_def Let_def by simp show "dim_col B3 = dim_col (0\<^sub>m (n - k) k)" using assms unfolding split_block_def Let_def by simp fix i j assume "i < dim_row (0\<^sub>m (n - k) k)" and "j < dim_col (0\<^sub>m (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) = 0\<^sub>m (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 = 0\<^sub>m k (n-k)" and "B3 = 0\<^sub>m (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 (0\<^sub>m k (n-k)) (0\<^sub>m (n-k) k) B4" using assms by simp also have "... = four_block_mat B1 (0\<^sub>m k (n-k)) (0\<^sub>m (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 (0\<^sub>m (dim_row B1) (dim_col B2)) (0\<^sub>m (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 "jdim_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 (0\<^sub>m nr1 n2) (0\<^sub>m nr2 n1) D1" define fb2 where "fb2 = four_block_mat A2 (0\<^sub>m n1 nc2) (0\<^sub>m n2 nc1) D2" have "fb1 * fb2 = four_block_mat (A1 * A2 + 0\<^sub>m nr1 n2 * 0\<^sub>m n2 nc1) (A1 * 0\<^sub>m n1 nc2 + 0\<^sub>m nr1 n2 * D2) (0\<^sub>m nr2 n1 * A2 + D1 * 0\<^sub>m n2 nc1) (0\<^sub>m nr2 n1 * 0\<^sub>m 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) (0\<^sub>m nr1 nc2) (0\<^sub>m 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) (0\<^sub>m (dim_col U1) (dim_row U2)) (0\<^sub>m (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 (1\<^sub>m (dim_row U1)) (0\<^sub>m (dim_row U1) (dim_row U2)) (0\<^sub>m (dim_row U2) (dim_row U1)) (1\<^sub>m (dim_row U2))" using assms unfolding unitary_def inverts_mat_def by simp also have "... = 1\<^sub>m (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) = 1\<^sub>m 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 = 1\<^sub>m 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 \" using assms unfolding real_diag_decomp_def by simp show "\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: "\ii < 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 "\ilength (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 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 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 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 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 "\ii < length Al. Al!i * (Bl!i) = Bl!i * (Al!i)" and "\ii []" 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 "\iij = 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 "\ilength Al = length (tl Bl)\ length_Cons local.Cons(3) nth_Cons_Suc nth_tl) show "\iBl = 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 "\iiiiii < 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 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 "\ji < 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 = (0\<^sub>m x (n - x)) \ B3 = (0\<^sub>m (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 = 0\<^sub>m 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: "0\<^sub>m (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: "0\<^sub>m (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 (0\<^sub>m (dim_row B1) (dim_col C)) (0\<^sub>m (dim_row C) (dim_col B1)) C)" by simp also have "... = four_block_mat B1 (0\<^sub>m (dim_row B1) (dim_col B4)) (0\<^sub>m (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 = 0\<^sub>m 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 = 0\<^sub>m (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 = 0\<^sub>m a (n - a) \ B3 = 0\<^sub>m (n - a) a \ diag_compat B4 l" using sp \B3 = 0\<^sub>m (n - a) a\ \B2 = 0\<^sub>m 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 = 0\<^sub>m 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 = 0\<^sub>m (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 - unfolding Let_def - by (metis eq_comps_not_empty hd_Cons_tl length_Cons list.discI - semiring_norm(164) sum_list.Cons) + 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 \\<^sub>m (1\<^sub>m ((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 \\<^sub>m 1\<^sub>m (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 []" 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 \\<^sub>m (1\<^sub>m ((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 \\<^sub>m (1\<^sub>m m)" unfolding m_def by auto note kprop = this hence "(extract_subdiags A (eq_comps (diag_mat A)))!i * B = k \\<^sub>m (1\<^sub>m m) * B" by simp also have "... = B * (k \\<^sub>m (1\<^sub>m 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_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_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 "\z\set (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 "(1\<^sub>m n)$$(i,j) = (1\<^sub>m 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) = 1\<^sub>m n" proof (rule eq_matI) show "dim_row (Complex_Matrix.adjoint (per_col A f) * per_col A f) = dim_row (1\<^sub>m 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 (1\<^sub>m n)" by auto fix i j assume "i < dim_row (1\<^sub>m n)" and "j < dim_col (1\<^sub>m 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 "... = (1\<^sub>m n) $$ (f i, f j)" using assms unfolding Complex_Matrix.unitary_def by (metis assms(2) unitary_simps(1)) also have "... = (1\<^sub>m 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) = 1\<^sub>m 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 {..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 \\<^sub>m rank_1_proj (Matrix.col A i) else (0\<^sub>m n n)))" define g where "g = (\i. (if i < n then diag_mat D ! (f i) \\<^sub>m rank_1_proj (Matrix.col A (f i)) else (0\<^sub>m n n)))" have "f ` {..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 {..x. x \ {.. h (f x) = g x" unfolding h_def g_def by (meson assms(6) bij_betwE lessThan_iff) ultimately have "sum_mat g {..f ` {.. by simp also have "... =sum_mat (\i. diag_mat D ! i \\<^sub>m rank_1_proj (Matrix.col A i)) {..i. i < n \ diag_mat D ! i \\<^sub>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 \\<^sub>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 {..i. diag_mat (per_diag D f) ! i \\<^sub>m rank_1_proj (Matrix.col (per_col A f) i)) {.. 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 {..i. i < n \ diag_mat (per_diag D f) ! i \\<^sub>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 \\<^sub>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 \\<^sub>m rank_1_proj (Matrix.col A (f i)) \ fc" proof - fix i assume "i < n" hence "f i < n" using \f ` {.. 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 \\<^sub>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 \\<^sub>m rank_1_proj (Matrix.col (per_col A f) i) = diag_mat D ! f i \\<^sub>m rank_1_proj (Matrix.col A (f i))" proof- fix i assume "i < n" hence "f i < n" using \f ` {.. 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 \\<^sub>m rank_1_proj (Matrix.col (per_col A f) i) = diag_mat D ! f i \\<^sub>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 {.. (\ilength l = length m\ mset_eq_permutation) note pprop = this have "bij_betw p {..length l = length m\ by (simp add: permutes_imp_bij) moreover have "\ilength l = length m\ permute_list_nth) ultimately have "\f. bij_betw f {.. (\i 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 {.. (\ilength 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 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 "\ilength 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 {.. 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) = 1\<^sub>m (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 = 1\<^sub>m (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 {..unitary_diag A Bs Us\) show "\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 \" using ubprop by auto show "bij_betw f {..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 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: "\iiiB = 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 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: "\Al\Als. 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\ \\Al\Als. 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 "\iAl\Als. 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 \ (\iAl\Als. dim_row ([U0] ! i) = dim_row (Al ! i) \ dim_col ([U0] ! i) = dim_col (Al ! i)) \ (\Al\Als. \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 Al \ tAls. (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i)))\ (\Al\tAls. \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 "\tAl\tAls. length tAl = n" using Suc(4) tex by fastforce show "\iU. \Al\tAls. \B. real_diag_decomp (Al ! i) B U" proof (intro allI impI) fix i assume "i < n" hence "\U. \Al\Als. \B. real_diag_decomp (Al ! (Suc i)) B U" using Suc Suc_mono by presburger from this obtain U where tu: "\Al\Als. \B. real_diag_decomp (Al ! (Suc i)) B U" by auto have "\tAl\tAls. \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. \Al\tAls. \B. real_diag_decomp (Al ! i) B U" by auto qed show "\i < n. \Al\tAls. dim_row (Al!i) = dim_col (Al!i)" by (metis Suc(5) \\tAl\tAls. length tAl = n\ not_less_eq nth_tl tex) qed from this obtain Ul where "length Ul = n" and "\i Al \ tAls. (dim_row (Ul!i) = dim_row (Al!i) \ dim_col (Ul!i) = dim_col (Al!i))" "(\Al\tAls. \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 "\Al\Als. \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 "\iAl\Als. 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 \" 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 "\A\Afp. hermitian A \ A \ carrier_mat n n" and "\A\Afp. \B\Afp. 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 "\C\Cs. C = diag_block_mat (extract_subdiags C l)" and "\C1\Cs. \C2\Cs. 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 "\Al\ExC. 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 "\jE\ExC. E ! j \ carrier_mat (l ! j) (l ! j)" by (metis (no_types, lifting) assms(3) extract_subdiags_carrier imageE ncl_def) hence "\i < ncl. \Al\ExC. 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\ \\Al\ExC. length Al = ncl\) show "j < length Ea" by (metis \Eb \ ExC\ \\Al\ExC. length Al = ncl\ \j < length l\ ncl_def \length Ea = length Eb\) show "\iEa \ ExC\ \\Al\ExC. length Al = ncl\ \\i < ncl. \Al\ExC. dim_row (Al ! i) = dim_col (Al ! i)\) show "\iEa \ ExC\ \Eb \ ExC\ \\Al\ExC. length Al = ncl\ \\jE\ExC. E ! j \ carrier_mat (l ! j) (l ! j)\ carrier_matD(1)) show "\iEa \ ExC\ \Eb \ ExC\ \\Al\ExC. length Al = ncl\ \\i \\iAl\ExC. 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: \\C\Cs. 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: \\C\Cs. C = diag_block_mat (extract_subdiags C l)\) moreover have "Cea * Ceb = Ceb * Cea" by (simp add: \Cea \ Cs\ \Ceb \ Cs\ \\C1\Cs. \C2\Cs. 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. \A\Af. \B. real_diag_decomp A B U" and "finite CjA" and "CjA \ {}" and "card CjA \ i" and "\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)" and "\C1\CjA. \C2\CjA. 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 "\iU. \Al\Exc. \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. \Al\Exi. \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 "\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)" using \\C\CjA. C = diag_block_mat (extract_subdiags C eqcl)\ . show "\C1\CjA. \C2\CjA. C1 * C2 = C2 * C1" using \\C1\CjA. \C2\CjA. 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. \Al\Exc. \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 "\A\Afp. hermitian A \ A \ carrier_mat n n" using Suc by (metis Afp_def Diff_subset subset_iff) have "\A\Afp. \B\Afp. 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\ \\A\Afp. hermitian A \ A \ carrier_mat n n\ \\A\Afp. \B\Afp. 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\ _ \\A\Afp. 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: \\A\Afp. \B\Afp. 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 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 "\Al\Ex. length Al = ncl" unfolding ncl_def Ex_def by (simp add: extract_subdiags_length) show "\iAl\Ex. 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) \\Al\Ex. length Al = ncl\ carrier_matD(2) hermitian_square list_all_length) qed show " \iU. \Al\Ex. \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 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 "\ilength Ul = length esubB\ \length Ul = ncl\ ncl_def by auto show roweq:"\ilength 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:"\ilength 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 "\idiagonal_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 \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. \A\Af. \B. real_diag_decomp A B U" by blast qed qed qed end \ No newline at end of file