imports Jordan_Normal_Form Schur_Decomposition

(* Author: RenĂ© Thiemann Akihisa Yamada License: BSD *) section ‹Computing Jordan Normal Forms› theory Jordan_Normal_Form_Existence imports Jordan_Normal_Form Column_Operations Schur_Decomposition begin hide_const (open) Coset.order text‹We prove existence of Jordan normal forms by means of first applying Schur's algorithm to convert a matrix into upper-triangular form, and then applying the following algorithm to convert a upper-triangular matrix into a Jordan normal form. It only consists of basic row- and column-operations.› subsection ‹Pseudo Code Algorithm› text ‹The following algorithm is used to compute JNFs from upper-triangular matrices. It was generalized from \cite[Sect.~11.1.4]{PO07} where this algorithm was not explicitly specified but only applied on an example. We further introduced step 2 which does not occur in the textbook description. \begin{enumerate} \item[1.] Eliminate entries within blocks besides EV $a$ and above EV $b$ for $a \neq b$: for $A_{ij}$ with EV $a$ left of it, and EV $b$ below of it, perform @{term "add_col_sub_row (A⇩_{i}⇩_{j}/ (b - a)) i j"}. The iteration should be by first increasing $j$ and the inner loop by decreasing $i$. \item[2.] Move rows of same EV together, can only be done after 1., otherwise triangular-property is lost. Say both rows $i$ and $j$ ($i < j$) contain EV $a$, but all rows between $i$ and $j$ have different EV. Then perform @{term "swap_cols_rows (i+1) j"}, @{term "swap_cols_rows (i+2) j"}, \ldots @{term "swap_cols_rows (j-1) j"}. Afterwards row $j$ will be at row $i+1$, and rows $i+1,\ldots,j-1$ will be moved to $i+2,\ldots,j$. The global iteration works by increasing $j$. \item[3.] Transform each EV-block into JNF, do this for increasing upper $n \times k$ matrices, where each new column $k$ will be treated as follows. \begin{enumerate} \item[a)] Eliminate entries $A_{ik}$ in rows of form $0 \ldots 0\ ev\ 1\ 0 \ldots 0\ A_{ik}$: @{term "add_col_sub_row (-A⇩_{i}⇩_{k}) (i+1) k"}. Perform elimination by increasing $i$. \item[b)] Figure out largest JB (of $n-1 \times n-1$ sub-matrix) with lowest row of form $0 \ldots 0\ ev\ 0 \ldots 0\ A_{lk}$ where $A_{lk} \neq 0$, and set $x := A_{lk}$. \item[c)] If such a JB does not exist, continue with next column. Otherwise, eliminate all other non-zero-entries $y := A_{ik}$ via row $l$: @{term "add_col_sub_row (y/x) i l"}, @{term "add_col_sub_row (y/x) (i-1) (l-1)"}, @{term "add_col_sub_row (y/x) (i-2) (l-2)"}, \ldots where the number of steps is determined by the size of the JB left-above of $A_{ik}$. Perform an iteration over $i$. \item[d)] Normalize value in row $l$ to 1: @{term "mult_col_div_row (1/x) k"}. \item[e)] Move the 1 down from row $l$ to row $k-1$: @{term "swap_cols_rows (l+1) k"}, @{term "swap_cols_rows (l+2) k"}, \ldots, @{term "swap_cols_rows (k-1) k"}. \end{enumerate} \end{enumerate} › subsection ‹Real Algorithm› fun lookup_ev :: "'a ⇒ nat ⇒ 'a mat ⇒ nat option" where "lookup_ev ev 0 A = None" | "lookup_ev ev (Suc i) A = (if A $$ (i,i) = ev then Some i else lookup_ev ev i A)" function swap_cols_rows_block :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "swap_cols_rows_block i j A = (if i < j then swap_cols_rows_block (Suc i) j (swap_cols_rows i j A) else A)" by pat_completeness auto termination by (relation "measure (λ (i,j,A). j - i)") auto fun identify_block :: "'a :: one mat ⇒ nat ⇒ nat" where "identify_block A 0 = 0" | "identify_block A (Suc i) = (if A $$ (i,Suc i) = 1 then identify_block A i else (Suc i))" function identify_blocks_main :: "'a :: ring_1 mat ⇒ nat ⇒ (nat × nat) list ⇒ (nat × nat) list" where "identify_blocks_main A 0 list = list" | "identify_blocks_main A (Suc i_end) list = ( let i_begin = identify_block A i_end in identify_blocks_main A i_begin ((i_begin, i_end) # list) )" by pat_completeness auto definition identify_blocks :: "'a :: ring_1 mat ⇒ nat ⇒ (nat × nat)list" where "identify_blocks A i = identify_blocks_main A i []" fun find_largest_block :: "nat × nat ⇒ (nat × nat)list ⇒ nat × nat" where "find_largest_block block [] = block" | "find_largest_block (m_start,m_end) ((i_start,i_end) # blocks) = (if i_end - i_start ≥ m_end - m_start then find_largest_block (i_start,i_end) blocks else find_largest_block (m_start,m_end) blocks)" fun lookup_other_ev :: "'a ⇒ nat ⇒ 'a mat ⇒ nat option" where "lookup_other_ev ev 0 A = None" | "lookup_other_ev ev (Suc i) A = (if A $$ (i,i) ≠ ev then Some i else lookup_other_ev ev i A)" partial_function (tailrec) partition_ev_blocks :: "'a mat ⇒ 'a mat list ⇒ 'a mat list" where [code]: "partition_ev_blocks A bs = (let n = dim_row A in if n = 0 then bs else (case lookup_other_ev (A $$ (n-1, n-1)) (n-1) A of None ⇒ A # bs | Some i ⇒ case split_block A (Suc i) (Suc i) of (UL,_,_,LR) ⇒ partition_ev_blocks UL (LR # bs)))" context fixes n :: nat and ty :: "'a :: field itself" begin function step_1_main :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "step_1_main i j A = (if j ≥ n then A else if i = 0 then step_1_main (j+1) (j+1) A else let i' = i - 1; ev_left = A $$ (i',i'); ev_below = A $$ (j,j); aij = A $$ (i',j); B = if (ev_left ≠ ev_below ∧ aij ≠ 0) then add_col_sub_row (aij / (ev_below - ev_left)) i' j A else A in step_1_main i' j B)" by pat_completeness auto termination by (relation "measures [λ (i,j,A). n - j, λ (i,j,A). i]") auto function step_2_main :: "nat ⇒ 'a mat ⇒ 'a mat" where "step_2_main j A = (if j ≥ n then A else let ev = A $$ (j,j); B = (case lookup_ev ev j A of None ⇒ A | Some i ⇒ swap_cols_rows_block (Suc i) j A ) in step_2_main (Suc j) B)" by pat_completeness auto termination by (relation "measure (λ (j,A). n - j)") auto fun step_3_a :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "step_3_a 0 j A = A" | "step_3_a (Suc i) j A = (let aij = A $$ (i,j); B = (if A $$ (i,i+1) = 1 ∧ aij ≠ 0 then add_col_sub_row (- aij) (Suc i) j A else A) in step_3_a i j B)" fun step_3_c_inner_loop :: "'a ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where "step_3_c_inner_loop val l i 0 A = A" | "step_3_c_inner_loop val l i (Suc k) A = step_3_c_inner_loop val (l - 1) (i - 1) k (add_col_sub_row val i l A)" fun step_3_c :: "'a ⇒ nat ⇒ nat ⇒ (nat × nat)list ⇒ 'a mat ⇒ 'a mat" where "step_3_c x l k [] A = A" | "step_3_c x l k ((i_begin,i_end) # blocks) A = ( let B = (if i_end = l then A else step_3_c_inner_loop (A $$ (i_end,k) / x) l i_end (Suc i_end - i_begin) A) in step_3_c x l k blocks B)" function step_3_main :: "nat ⇒ 'a mat ⇒ 'a mat" where "step_3_main k A = (if k ≥ n then A else let B = step_3_a (k-1) k A; ― ‹‹3_a›› all_blocks = identify_blocks B k; blocks = filter (λ block. B $$ (snd block,k) ≠ 0) all_blocks; F = (if blocks = [] ― ‹column ‹k› has only 0s› then B else let (l_start,l) = find_largest_block (hd blocks) (tl blocks); ― ‹‹3_b›› x = B $$ (l,k); C = step_3_c x l k blocks B; ― ‹‹3_c›› D = mult_col_div_row (inverse x) k C; ― ‹‹3_d›› E = swap_cols_rows_block (Suc l) k D ― ‹‹3_e›› in E) in step_3_main (Suc k) F)" by pat_completeness auto termination by (relation "measure (λ (k,A). n - k)") auto end definition step_1 :: "'a :: field mat ⇒ 'a mat" where "step_1 A = step_1_main (dim_row A) 0 0 A" definition step_2 :: "'a :: field mat ⇒ 'a mat" where "step_2 A = step_2_main (dim_row A) 0 A" definition step_3 :: "'a :: field mat ⇒ 'a mat" where "step_3 A = step_3_main (dim_row A) 1 A" declare swap_cols_rows_block.simps[simp del] declare step_1_main.simps[simp del] declare step_2_main.simps[simp del] declare step_3_main.simps[simp del] function jnf_vector_main :: "nat ⇒ 'a :: one mat ⇒ (nat × 'a) list" where "jnf_vector_main 0 A = []" | "jnf_vector_main (Suc i_end) A = (let i_start = identify_block A i_end in jnf_vector_main i_start A @ [(Suc i_end - i_start, A $$ (i_start,i_start))])" by pat_completeness auto definition jnf_vector :: "'a :: one mat ⇒ (nat × 'a) list" where "jnf_vector A = jnf_vector_main (dim_row A) A" definition triangular_to_jnf_vector :: "'a :: field mat ⇒ (nat × 'a) list" where "triangular_to_jnf_vector A ≡ let B = step_2 (step_1 A) in concat (map (jnf_vector o step_3) (partition_ev_blocks B []))" subsection ‹Preservation of Dimensions› lemma swap_cols_rows_block_dims_main: "dim_row (swap_cols_rows_block i j A) = dim_row A ∧ dim_col (swap_cols_rows_block i j A) = dim_col A" proof (induct i j A rule: swap_cols_rows_block.induct) case (1 i j A) thus ?case unfolding swap_cols_rows_block.simps[of i j A] by (auto split: if_splits) qed lemma swap_cols_rows_block_dims[simp]: "dim_row (swap_cols_rows_block i j A) = dim_row A" "dim_col (swap_cols_rows_block i j A) = dim_col A" "A ∈ carrier_mat n n ⟹ swap_cols_rows_block i j A ∈ carrier_mat n n" using swap_cols_rows_block_dims_main unfolding carrier_mat_def by auto lemma step_1_main_dims_main: "dim_row (step_1_main n i j A) = dim_row A ∧ dim_col (step_1_main n i j A) = dim_col A" proof (induct i j A taking: n rule: step_1_main.induct) case (1 i j A) thus ?case unfolding step_1_main.simps[of n i j A] by (auto split: if_splits simp: Let_def) qed lemma step_1_main_dims[simp]: "dim_row (step_1_main n i j A) = dim_row A" "dim_col (step_1_main n i j A) = dim_col A" using step_1_main_dims_main by blast+ lemma step_2_main_dims_main: "dim_row (step_2_main n j A) = dim_row A ∧ dim_col (step_2_main n j A) = dim_col A" proof (induct j A taking: n rule: step_2_main.induct) case (1 j A) thus ?case unfolding step_2_main.simps[of n j A] by (auto split: if_splits option.splits simp: Let_def) qed lemma step_2_main_dims[simp]: "dim_row (step_2_main n j A) = dim_row A" "dim_col (step_2_main n j A) = dim_col A" using step_2_main_dims_main by blast+ lemma step_3_a_dims_main: "dim_row (step_3_a i j A) = dim_row A ∧ dim_col (step_3_a i j A) = dim_col A" by (induct i j A rule: step_3_a.induct, auto split: if_splits simp: Let_def) lemma step_3_a_dims[simp]: "dim_row (step_3_a i j A) = dim_row A" "dim_col (step_3_a i j A) = dim_col A" using step_3_a_dims_main by blast+ lemma step_3_c_inner_loop_dims_main: "dim_row (step_3_c_inner_loop val l i j A) = dim_row A ∧ dim_col (step_3_c_inner_loop val l i j A) = dim_col A" by (induct val l i j A rule: step_3_c_inner_loop.induct, auto) lemma step_3_c_inner_loop_dims[simp]: "dim_row (step_3_c_inner_loop val l i j A) = dim_row A" "dim_col (step_3_c_inner_loop val l i j A) = dim_col A" using step_3_c_inner_loop_dims_main by blast+ lemma step_3_c_dims_main: "dim_row (step_3_c x l k i A) = dim_row A ∧ dim_col (step_3_c x l k i A) = dim_col A" by (induct x l k i A rule: step_3_c.induct, auto simp: Let_def) lemma step_3_c_dims[simp]: "dim_row (step_3_c x l k i A) = dim_row A" "dim_col (step_3_c x l k i A) = dim_col A" using step_3_c_dims_main by blast+ lemma step_3_main_dims_main: "dim_row (step_3_main n k A) = dim_row A ∧ dim_col (step_3_main n k A) = dim_col A" proof (induct k A taking: n rule: step_3_main.induct) case (1 k A) thus ?case unfolding step_3_main.simps[of n k A] by (auto split: if_splits prod.splits option.splits simp: Let_def) qed lemma step_3_main_dims[simp]: "dim_row (step_3_main n j A) = dim_row A" "dim_col (step_3_main n j A) = dim_col A" using step_3_main_dims_main by blast+ lemma triangular_to_jnf_steps_dims[simp]: "dim_row (step_1 A) = dim_row A" "dim_col (step_1 A) = dim_col A" "dim_row (step_2 A) = dim_row A" "dim_col (step_2 A) = dim_col A" "dim_row (step_3 A) = dim_row A" "dim_col (step_3 A) = dim_col A" unfolding step_1_def step_2_def step_3_def o_def by auto subsection ‹Properties of Auxiliary Algorithms› lemma lookup_ev_Some: "lookup_ev ev j A = Some i ⟹ i < j ∧ A $$ (i,i) = ev ∧ (∀ k. i < k ⟶ k < j ⟶ A $$ (k,k) ≠ ev)" by (induct j, auto split: if_splits, case_tac "k = j", auto) lemma lookup_ev_None: "lookup_ev ev j A = None ⟹ i < j ⟹ A $$ (i,i) ≠ ev" by (induct j, auto split: if_splits, case_tac "i = j", auto) lemma swap_cols_rows_block_index[simp]: "i < dim_row A ⟹ i < dim_col A ⟹ j < dim_row A ⟹ j < dim_col A ⟹ low ≤ high ⟹ high < dim_row A ⟹ high < dim_col A ⟹ swap_cols_rows_block low high A $$ (i,j) = A $$ (if i = low then high else if i > low ∧ i ≤ high then i - 1 else i, if j = low then high else if j > low ∧ j ≤ high then j - 1 else j)" proof (induct low high A rule: swap_cols_rows_block.induct) case (1 low high A) let ?r = "dim_row A" let ?c = "dim_col A" let ?A = "swap_cols_rows_block low high A" let ?B = "swap_cols_rows low high A" let ?C = "swap_cols_rows_block (Suc low) high ?B" note [simp] = swap_cols_rows_block.simps[of low high A] from 1(2-) have lh: "low ≤ high" by simp show ?case proof (cases "low < high") case False with lh have lh: "low = high" by auto from False have "?A = A" by simp with lh show ?thesis by auto next case True hence A: "?A = ?C" by simp from True lh have "Suc low ≤ high" by simp note IH = 1(1)[unfolded swap_cols_rows_carrier, OF True 1(2-5) this 1(7-)] note * = 1(2-) let ?i = "if i = Suc low then high else if Suc low < i ∧ i ≤ high then i - 1 else i" let ?j = "if j = Suc low then high else if Suc low < j ∧ j ≤ high then j - 1 else j" have cong: "⋀ i j i' j'. i = i' ⟹ j = j' ⟹ A $$ (i,j) = A $$ (i',j')" by auto have ij: "?i < ?r" "?i < ?c" "?j < ?r" "?j < ?c" "low < ?r" "high < ?r" using * True by auto show ?thesis unfolding A IH by (subst swap_cols_rows_index[OF ij], rule cong, insert * True, auto) qed qed lemma find_largest_block_main: assumes "find_largest_block block blocks = (m_b, m_e)" shows "(m_b, m_e) ∈ insert block (set blocks) ∧ (∀ b ∈ insert block (set blocks). m_e - m_b ≥ snd b - fst b)" using assms proof (induct block blocks rule: find_largest_block.induct) case (2 m_start m_end i_start i_end blocks) let ?res = "find_largest_block (m_start,m_end) ((i_start,i_end) # blocks)" show ?case proof (cases "i_end - i_start ≥ m_end - m_start") case True with 2(3-) have "find_largest_block (i_start,i_end) blocks = (m_b, m_e)" by auto note IH = 2(1)[OF True this] thus ?thesis using True by auto next case False with 2(3-) have "find_largest_block (m_start,m_end) blocks = (m_b, m_e)" by auto note IH = 2(2)[OF False this] thus ?thesis using False by auto qed qed simp lemma find_largest_block: assumes bl: "blocks ≠ []" and find: "find_largest_block (hd blocks) (tl blocks) = (m_begin, m_end)" shows "(m_begin,m_end) ∈ set blocks" "⋀ i_begin i_end. (i_begin,i_end) ∈ set blocks ⟹ m_end - m_begin ≥ i_end - i_begin" proof - from bl have id: "insert (hd blocks) (set (tl blocks)) = set blocks" by (cases blocks, auto) from find_largest_block_main[OF find, unfolded id] show "(m_begin,m_end) ∈ set blocks" "⋀ i_begin i_end. (i_begin,i_end) ∈ set blocks ⟹ m_end - m_begin ≥ i_end - i_begin" by auto qed context fixes ev :: "'a :: one" and A :: "'a mat" begin lemma identify_block_main: assumes "identify_block A j = i" shows "i ≤ j ∧ (i = 0 ∨ A $$ (i - 1, i) ≠ 1) ∧ (∀ k. i ≤ k ⟶ k < j ⟶ A $$ (k, Suc k) = 1)" (is "?P j") using assms proof (induct j) case (Suc j) show ?case proof (cases "A $$ (j, Suc j) = 1") case False with Suc(2) show ?thesis by auto next case True with Suc(2) have "identify_block A j = i" by simp note IH = Suc(1)[OF this] { fix k assume "k ≥ i" and "k < Suc j" hence "A $$ (k, Suc k) = 1" proof (cases "k < j") case True with IH ‹k ≥ i› show ?thesis by auto next case False with ‹k < Suc j› have "k = j" by auto with True show ?thesis by auto qed } with IH show ?thesis by auto qed qed simp lemma identify_block_le: "identify_block A i ≤ i" using identify_block_main[OF refl] by blast end lemma identify_block: assumes "identify_block A j = i" shows "i ≤ j" "i = 0 ∨ A $$ (i - 1, i) ≠ 1" "i ≤ k ⟹ k < j ⟹ A $$ (k, Suc k) = 1" proof - let ?ev = "A $$ (j,j)" note main = identify_block_main[OF assms] from main show "i ≤ j" by blast from main show "i = 0 ∨ A $$ (i - 1, i) ≠ 1" by blast assume "i ≤ k" with main have main: "k < j ⟹ A $$ (k, Suc k) = 1" by blast thus "k < j ⟹ A $$ (k, Suc k) = 1" by blast qed lemmas identify_block_le' = identify_block(1) lemma identify_block_le_rev: "j = identify_block A i ⟹ j ≤ i" using identify_block_le'[of A i j] by auto termination identify_blocks_main by (relation "measure (λ (_,i,list). i)", auto simp: identify_block_le le_imp_less_Suc) termination jnf_vector_main by (relation "measure (λ (i,A). i)", auto simp: identify_block_le le_imp_less_Suc) lemma identify_blocks_main: assumes "(i_start,i_end) ∈ set (identify_blocks_main A i list)" and "⋀ i_s i_e. (i_s, i_e) ∈ set list ⟹ i_s ≤ i_e ∧ i_e < k" and "i ≤ k" shows "i_start ≤ i_end ∧ i_end < k" using assms proof (induct A i list rule: identify_blocks_main.induct) case (2 A i_e list) obtain i_b where id: "identify_block A i_e = i_b" by force note IH = 2(1)[OF id[symmetric]] let ?res = "identify_blocks_main A (Suc i_e) list" let ?rec = "identify_blocks_main A i_b ((i_b, i_e) # list)" have res: "?res = ?rec" using id by simp from 2(2)[unfolded res] have "(i_start, i_end) ∈ set ?rec" . note IH = IH[OF this] from 2(3-) have iek: "i_e < k" by simp from identify_block_le'[OF id] have ibe: "i_b ≤ i_e" . from ibe iek have "i_b ≤ k" by simp note IH = IH[OF _ this] show ?thesis by (rule IH, insert ibe iek 2(3-), auto) qed simp lemma identify_blocks: assumes "(i_start,i_end) ∈ set (identify_blocks B k)" shows "i_start ≤ i_end ∧ i_end < k" using identify_blocks_main[OF assms[unfolded identify_blocks_def]] by auto subsection ‹Proving Similarity› context begin private lemma swap_cols_rows_block_similar: assumes "A ∈ carrier_mat n n" and "j < n" and "i ≤ j" shows "similar_mat (swap_cols_rows_block i j A) A" using assms proof (induct i j A rule: swap_cols_rows_block.induct) case (1 i j A) hence A: "A ∈ carrier_mat n n" and jn: "j < n" and ij: "i ≤ j" by auto note [simp] = swap_cols_rows_block.simps[of i j] show ?case proof (cases "i < j") case False thus ?thesis using similar_mat_refl[OF A] by simp next case True note ij = this let ?B = "swap_cols_rows i j A" let ?C = "swap_cols_rows_block (Suc i) j ?B" from swap_cols_rows_similar[OF A _ jn, of i] ij jn have BA: "similar_mat ?B A" by auto have CB: "similar_mat ?C ?B" by (rule 1(1)[OF ij _ jn], insert ij A, auto) from similar_mat_trans[OF CB BA] show ?thesis using ij by simp qed qed private lemma step_1_main_similar: "i ≤ j ⟹ A ∈ carrier_mat n n ⟹ similar_mat (step_1_main n i j A) A" proof (induct i j A taking: n rule: step_1_main.induct) case (1 i j A) note [simp] = step_1_main.simps[of n i j A] from 1(3-) have ij: "i ≤ j" and A: "A ∈ carrier_mat n n" by auto show ?case proof (cases "j ≥ n") case True thus ?thesis using similar_mat_refl[OF A] by simp next case False hence jn: "j < n" by simp note IH = 1(1-2)[OF False] show ?thesis proof (cases "i = 0") case True from IH(1)[OF this _ A] show ?thesis using jn by (simp, simp add: True) next case False let ?evi = "A $$ (i - 1, i - 1)" let ?evj = "A $$ (j,j)" let ?B = "if ?evi ≠ ?evj ∧ A $$ (i - 1, j) ≠ 0 then add_col_sub_row (A $$ (i - 1, j) / (?evj - ?evi)) (i - 1) j A else A" obtain B where B: "B = ?B" by auto have Bn: "B ∈ carrier_mat n n" unfolding B using A by simp from False ij jn have *: "i - 1 < n" "j < n" "i - 1 ≠ j" by auto have BA: "similar_mat B A" unfolding B using similar_mat_refl[OF A] add_col_sub_row_similar[OF A *] by auto from ij have "i - 1 ≤ j" by simp note IH = IH(2)[OF False refl refl refl refl B this Bn] from False jn have id: "step_1_main n i j A = step_1_main n (i - 1) j B" unfolding B by (simp add: Let_def) show ?thesis unfolding id by (rule similar_mat_trans[OF IH BA]) qed qed qed private lemma step_2_main_similar: "A ∈ carrier_mat n n ⟹ similar_mat (step_2_main n j A) A" proof (induct j A taking: n rule: step_2_main.induct) case (1 j A) note [simp] = step_2_main.simps[of n j A] from 1(2) have A: "A ∈ carrier_mat n n" . show ?case proof (cases "j ≥ n") case True thus ?thesis using similar_mat_refl[OF A] by simp next case False hence jn: "j < n" by simp note IH = 1(1)[OF False] let ?look = "lookup_ev (A $$ (j,j)) j A" let ?B = "case ?look of None ⇒ A | Some i ⇒ swap_cols_rows_block (Suc i) j A" obtain B where B: "B = ?B" by auto have id: "step_2_main n j A = step_2_main n (Suc j) B" unfolding B using False by simp have Bn: "B ∈ carrier_mat n n" unfolding B using A by (auto split: option.splits) have BA: "similar_mat B A" proof (cases ?look) case None thus ?thesis unfolding B using similar_mat_refl[OF A] by simp next case (Some i) from lookup_ev_Some[OF this] show ?thesis unfolding B Some by (auto intro: swap_cols_rows_block_similar[OF A jn]) qed show ?thesis unfolding id by (rule similar_mat_trans[OF IH[OF refl B Bn] BA]) qed qed private lemma step_3_a_similar: "A ∈ carrier_mat n n ⟹ i < j ⟹ j < n ⟹ similar_mat (step_3_a i j A) A" proof (induct i j A rule: step_3_a.induct) case (1 j A) thus ?case by (simp add: similar_mat_refl) next case (2 i j A) from 2(2-) have A: "A ∈ carrier_mat n n" and ij: "Suc i < j" and j: "j < n" by auto let ?B = "if A $$ (i, i + 1) = 1 ∧ A $$ (i, j) ≠ 0 then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A" obtain B where B: "B = ?B" by auto from A have Bn: "B ∈ carrier_mat n n" unfolding B by simp note IH = 2(1)[OF refl B Bn _ j] have id: "step_3_a (Suc i) j A = step_3_a i j B" unfolding B by (simp add: Let_def) from ij j have *: "Suc i < n" "j < n" "Suc i ≠ j" by auto have BA: "similar_mat B A" unfolding B using similar_mat_refl[OF A] add_col_sub_row_similar[OF A *] by auto show ?case unfolding id by (rule similar_mat_trans[OF IH BA], insert ij, auto) qed private lemma step_3_c_inner_loop_similar: "A ∈ carrier_mat n n ⟹ l ≠ i ⟹ k - 1 ≤ l ⟹ k - 1 ≤ i ⟹ l < n ⟹ i < n ⟹ similar_mat (step_3_c_inner_loop val l i k A) A" proof (induct val l i k A rule: step_3_c_inner_loop.induct) case (1 val l i A) thus ?case using similar_mat_refl[of A] by simp next case (2 val l i k A) let ?res = "step_3_c_inner_loop val l i (Suc k) A" from 2(2-) have A: "A ∈ carrier_mat n n" and *: "l ≠ i" "k ≤ l" "k ≤ i" "l < n" "i < n" by auto let ?B = "add_col_sub_row val i l A" have BA: "similar_mat ?B A" by (rule add_col_sub_row_similar[OF A], insert *, auto) have B: "?B ∈ carrier_mat n n" using A unfolding carrier_mat_def by simp show ?case proof (cases k) case 0 hence id: "?res = ?B" by simp thus ?thesis using BA by simp next case (Suc kk) with * have "l - 1 ≠ i - 1" "k - 1 ≤ l - 1" "k - 1 ≤ i - 1" "l - 1 < n" "i - 1 < n" by auto note IH = 2(1)[OF B this] show ?thesis unfolding step_3_c_inner_loop.simps by (rule similar_mat_trans[OF IH BA]) qed qed private lemma step_3_c_similar: "A ∈ carrier_mat n n ⟹ l < k ⟹ k < n ⟹ (⋀ i_begin i_end. (i_begin, i_end) ∈ set blocks ⟹ i_end ≤ k ∧ i_end - i_begin ≤ l) ⟹ similar_mat (step_3_c x l k blocks A) A" proof (induct x l k blocks A rule: step_3_c.induct) case (1 x l k A) thus ?case using similar_mat_refl[OF 1(1)] by simp next case (2 x l k i_begin i_end blocks A) let ?res = "step_3_c x l k ((i_begin,i_end) # blocks) A" from 2(2-4) have A: "A ∈ carrier_mat n n" and lki: "l < k" "k < n" by auto from 2(5) have i: "i_end ≤ k" "i_end - i_begin ≤ l" by auto let ?y = "A $$ (i_end,k)" let ?inner = "step_3_c_inner_loop (?y / x) l i_end (Suc i_end - i_begin) A" obtain B where B: "B = (if i_end = l then A else ?inner)" by auto hence id: "?res = step_3_c x l k blocks B" by simp have BA: "similar_mat B A" proof (cases "i_end = l") case True thus ?thesis unfolding B using similar_mat_refl[OF A] by simp next case False hence B: "B = ?inner" and li: "l ≠ i_end" by (auto simp: B) show ?thesis unfolding B by (rule step_3_c_inner_loop_similar[OF A li], insert lki i, auto) qed have Bn: "B ∈ carrier_mat n n" using A unfolding B carrier_mat_def by simp note IH = 2(1)[OF B Bn lki(1-2) 2(5)] show ?case unfolding id by (rule similar_mat_trans[OF IH BA], auto) qed private lemma step_3_main_similar: "A ∈ carrier_mat n n ⟹ k > 0 ⟹ similar_mat (step_3_main n k A) A" proof (induct k A taking: n rule: step_3_main.induct) case (1 k A) from 1(2-) have A: "A ∈ carrier_mat n n" and k: "k > 0" by auto note [simp] = step_3_main.simps[of n k A] show ?case proof (cases "k ≥ n") case True thus ?thesis using similar_mat_refl[OF A] by simp next case False hence kn: "k < n" by simp obtain B where B: "B = step_3_a (k - 1) k A" by auto note IH = 1(1)[OF False B] from A have Bn: "B ∈ carrier_mat n n" unfolding B carrier_mat_def by simp from k have "k - 1 < k" by simp from step_3_a_similar[OF A this kn] have BA: "similar_mat B A" unfolding B . obtain all_blocks where ab: "all_blocks = identify_blocks B k" by simp obtain blocks where blocks: "blocks = filter (λ block. B $$ (snd block, k) ≠ 0) all_blocks" by simp obtain F where F: "F = (if blocks = [] then B else let (l_begin,l) = find_largest_block (hd blocks) (tl blocks); x = B $$ (l, k); C = step_3_c x l k blocks B; D = mult_col_div_row (inverse x) k C; E = swap_cols_rows_block (Suc l) k D in E)" by simp note IH = IH[OF ab blocks F] have Fn: "F ∈ carrier_mat n n" unfolding F Let_def carrier_mat_def using Bn by (simp split: prod.splits) have FB: "similar_mat F B" proof (cases "blocks = []") case True thus ?thesis unfolding F using similar_mat_refl[OF Bn] by simp next case False obtain l_start l where l: "find_largest_block (hd blocks) (tl blocks) = (l_start, l)" by force obtain x where x: "x = B $$ (l,k)" by simp obtain C where C: "C = step_3_c x l k blocks B" by simp obtain D where D: "D = mult_col_div_row (inverse x) k C" by auto obtain E where E: "E = swap_cols_rows_block (Suc l) k D" by auto from find_largest_block[OF False l] have lb: "(l_start,l) ∈ set blocks" and llarge: "⋀ i_begin i_end. (i_begin,i_end) ∈ set blocks ⟹ l - l_start ≥ i_end - i_begin" by auto from lb have x0: "x ≠ 0" unfolding blocks x by simp { fix i_start i_end assume "(i_start,i_end) ∈ set blocks" hence "(i_start,i_end) ∈ set (identify_blocks B k)" unfolding blocks ab by simp from identify_blocks[OF this] have "i_end < k" by simp } note block_bound = this from block_bound[OF lb] have lk: "l < k" . from False have F: "F = E" unfolding E D C x F l Let_def by simp from Bn have Cn: "C ∈ carrier_mat n n" unfolding C carrier_mat_def by simp have CB: "similar_mat C B" unfolding C proof (rule step_3_c_similar[OF Bn lk kn]) fix i_begin i_end assume i: "(i_begin, i_end) ∈ set blocks" from llarge[OF i] block_bound[OF i] show "i_end ≤ k ∧ i_end - i_begin ≤ l" by auto qed from x0 have "inverse x ≠ 0" by simp from mult_col_div_row_similar[OF Cn kn this] have DC: "similar_mat D C" unfolding D . from Cn have Dn: "D ∈ carrier_mat n n" unfolding D carrier_mat_def by simp from lk have "Suc l ≤ k" by auto from swap_cols_rows_block_similar[OF Dn kn this] have ED: "similar_mat E D" unfolding E . from similar_mat_trans[OF ED similar_mat_trans[OF DC similar_mat_trans[OF CB similar_mat_refl[OF Bn]]]] show ?thesis unfolding F . qed have "0 < Suc k" by simp note IH = IH[OF Fn this] have id: "step_3_main n k A = step_3_main n (Suc k) F" using kn by (simp add: F Let_def blocks ab B) show ?thesis unfolding id by (rule similar_mat_trans[OF IH similar_mat_trans[OF FB BA]]) qed qed lemma step_1_similar: "A ∈ carrier_mat n n ⟹ similar_mat (step_1 A) A" unfolding step_1_def by (rule step_1_main_similar, auto) lemma step_2_similar: "A ∈ carrier_mat n n ⟹ similar_mat (step_2 A) A" unfolding step_2_def by (rule step_2_main_similar, auto) lemma step_3_similar: "A ∈ carrier_mat n n ⟹ similar_mat (step_3 A) A" unfolding step_3_def by (rule step_3_main_similar, auto) end subsection ‹Invariants for Proving that Result is in JNF› context fixes n :: nat and ty :: "'a :: field itself" begin (* upper triangular, ensured by precondition and then maintained *) definition uppert :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where "uppert A i j ≡ j < i ⟶ A $$ (i,j) = 0" (* zeros at places where EVs differ, ensured by step 1 and then maintained *) definition diff_ev :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where "diff_ev A i j ≡ i < j ⟶ A $$ (i,i) ≠ A $$ (j,j) ⟶ A $$ (i,j) = 0" (* same EVs are grouped together, ensured by step 2 and then maintained *) definition ev_blocks_part :: "nat ⇒ 'a mat ⇒ bool" where "ev_blocks_part m A ≡ ∀ i j k. i < j ⟶ j < k ⟶ k < m ⟶ A $$ (k,k) = A $$ (i,i) ⟶ A $$ (j,j) = A $$ (i,i)" definition ev_blocks :: "'a mat ⇒ bool" where "ev_blocks ≡ ev_blocks_part n" text ‹In step 3, there is a separation at which iteration we are. The columns left of $k$ will be in JNF, the columns right of $k$ or equal to $k$ will satisfy @{const uppert}, @{const diff_ev}, and @{const ev_blocks}, and the column at $k$ will have one of the following properties, which are ensured in the different phases of step 3.› (* Left of a one is a zero: In a row of shape 0 ... 0 ev 1 0 ... 0 entry, the entry will be 0, ensured by step 3 a and then maintained *) private definition one_zero :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where "one_zero A i j ≡ (Suc i < j ⟶ A $$ (i,Suc i) = 1 ⟶ A $$ (i,j) = 0) ∧ (j < i ⟶ A $$ (i,j) = 0) ∧ (i < j ⟶ A $$ (i,i) ≠ A $$ (j,j) ⟶ A $$ (i,j) = 0)" (* There is exactly one row 0 ... 0 ev 0 ... 0 entry with entry != 0 and that entry is x, ensured by step 3 c and then maintained *) private definition single_non_zero :: "nat ⇒ nat ⇒ 'a ⇒ 'a mat ⇒ nat ⇒ nat ⇒ bool" where "single_non_zero ≡ λ l k x. (λ A i j. (i ∉ {k,l} ⟶ A $$ (i,k) = 0) ∧ A $$ (l,k) = x)" (* There is at exactly one row 0 ... 0 ev 0 ... 0 entry with entry != 0 and that entry is 1, ensured by step 3 d and then maintained *) private definition single_one :: "nat ⇒ nat ⇒ 'a mat ⇒ nat ⇒ nat ⇒ bool" where "single_one ≡ λ l k. (λ A i j. (i ∉ {k,l} ⟶ A $$ (i,k) = 0) ∧ A $$ (l,k) = 1)" (* there is at most one row 0 ... 0 ev 0 ... 0 entry with entry != 0 and that entry is 1 and there are no zeros between ev and the entry, ensured by step 3 e *) private definition lower_one :: "nat ⇒ 'a mat ⇒ nat ⇒ nat ⇒ bool" where "lower_one k A i j = (j = k ⟶ (A $$ (i,j) = 0 ∨ i = j ∨ (A $$ (i,j) = 1 ∧ j = Suc i ∧ A $$ (i,i) = A $$ (j,j))))" (* the desired property: we have a jordan block matrix *) definition jb :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where "jb A i j ≡ (Suc i = j ⟶ A $$ (i,j) ∈ {0,1}) ∧ (i ≠ j ⟶ (Suc i ≠ j ∨ A $$ (i,i) ≠ A $$ (j,j)) ⟶ A $$ (i,j) = 0)" text ‹The following properties are useful to easily ensure the above invariants just from invariants of other matrices. The properties are essential in showing that the blocks identified in step 3b are the same as one would identify for the matrices in the upcoming steps 3c and 3d.› definition same_diag :: "'a mat ⇒ 'a mat ⇒ bool" where "same_diag A B ≡ ∀ i < n. A $$ (i,i) = B $$ (i,i)" private definition same_upto :: "nat ⇒ 'a mat ⇒ 'a mat ⇒ bool" where "same_upto j A B ≡ ∀ i' j'. i' < n ⟶ j' < j ⟶ A $$ (i',j') = B $$ (i',j')" text ‹Definitions stating where the properties hold› definition inv_all :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ bool" where "inv_all p A ≡ ∀ i j. i < n ⟶ j < n ⟶ p A i j" private definition inv_part :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ nat ⇒ nat ⇒ bool" where "inv_part p A m_i m_j ≡ ∀ i j. i < n ⟶ j < n ⟶ j < m_j ∨ j = m_j ∧ i ≥ m_i ⟶ p A i j" private definition inv_upto :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ nat ⇒ bool" where "inv_upto p A m ≡ ∀ i j. i < n ⟶ j < n ⟶ j < m ⟶ p A i j" private definition inv_from :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ nat ⇒ bool" where "inv_from p A m ≡ ∀ i j. i < n ⟶ j < n ⟶ j > m ⟶ p A i j" private definition inv_at :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ nat ⇒ bool" where "inv_at p A m ≡ ∀ i. i < n ⟶ p A i m" private definition inv_from_bot :: "('a mat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ nat ⇒ bool" where "inv_from_bot p A mi ≡ ∀ i. i ≥ mi ⟶ i < n ⟶ p A i" text ‹Auxiliary Lemmas on Handling, Comparing, and Accessing Invariants› lemma jb_imp_uppert: "jb A i j ⟹ uppert A i j" unfolding jb_def uppert_def by auto private lemma ev_blocks_partD: "ev_blocks_part m A ⟹ i < j ⟹ j < k ⟹ k < m ⟹ A $$ (k,k) = A $$ (i,i) ⟹ A $$ (j,j) = A $$ (i,i)" unfolding ev_blocks_part_def by auto private lemma ev_blocks_part_leD: assumes "ev_blocks_part m A" "i ≤ j" "j ≤ k" "k < m" "A $$ (k,k) = A $$ (i,i)" shows "A $$ (j,j) = A $$ (i,i)" proof - show ?thesis proof (cases "i = j ∨ j = k") case False with assms(2-3) have "i < j" "j < k" by auto from ev_blocks_partD[OF assms(1) this assms(4-)] show ?thesis . next case True thus ?thesis using assms(5) by auto qed qed private lemma ev_blocks_partI: assumes "⋀ i j k. i < j ⟹ j < k ⟹ k < m ⟹ A $$ (k,k) = A $$ (i,i) ⟹ A $$ (j,j) = A $$ (i,i)" shows "ev_blocks_part m A" using assms unfolding ev_blocks_part_def by blast private lemma ev_blocksD: "ev_blocks A ⟹ i < j ⟹ j < k ⟹ k < n ⟹ A $$ (k,k) = A $$ (i,i) ⟹ A $$ (j,j) = A $$ (i,i)" unfolding ev_blocks_def by (rule ev_blocks_partD) private lemma ev_blocks_leD: "ev_blocks A ⟹ i ≤ j ⟹ j ≤ k ⟹ k < n ⟹ A $$ (k,k) = A $$ (i,i) ⟹ A $$ (j,j) = A $$ (i,i)" unfolding ev_blocks_def by (rule ev_blocks_part_leD) lemma inv_allD: "inv_all p A ⟹ i < n ⟹ j < n ⟹ p A i j" unfolding inv_all_def by auto private lemma inv_allI: assumes "⋀ i j. i < n ⟹ j < n ⟹ p A i j" shows "inv_all p A" using assms unfolding inv_all_def by blast private lemma inv_partI: assumes "⋀ i j. i < n ⟹ j < n ⟹ j < m_j ∨ j = m_j ∧ i ≥ m_i ⟹ p A i j" shows "inv_part p A m_i m_j" using assms unfolding inv_part_def by auto private lemma inv_partD: assumes "inv_part p A m_i m_j" "i < n" "j < n" shows "j < m_j ⟹ p A i j" and "j = m_j ⟹ i ≥ m_i ⟹ p A i j" and "j < m_j ∨ j = m_j ∧ i ≥ m_i ⟹ p A i j" using assms unfolding inv_part_def by auto private lemma inv_uptoI: assumes "⋀ i j. i < n ⟹ j < n ⟹ j < m ⟹ p A i j" shows "inv_upto p A m" using assms unfolding inv_upto_def by auto private lemma inv_uptoD: assumes "inv_upto p A m" "i < n" "j < n" "j < m" shows "p A i j" using assms unfolding inv_upto_def by auto private lemma inv_upto_Suc: assumes "inv_upto p A m" and "⋀ i. i < n ⟹ p A i m" shows "inv_upto p A (Suc m)" proof (intro inv_uptoI) fix i j assume "i < n" "j < n" "j < Suc m" thus "p A i j" using inv_uptoD[OF assms(1), of i j] assms(2)[of i] by (cases "j = m", auto) qed private lemma inv_upto_mono: assumes "⋀ i j. i < n ⟹ j < k ⟹ p A i j ⟹ q A i j" shows "inv_upto p A k ⟹ inv_upto q A k" using assms unfolding inv_upto_def by auto private lemma inv_fromI: assumes "⋀ i j. i < n ⟹ j < n ⟹ j > m ⟹ p A i j" shows "inv_from p A m" using assms unfolding inv_from_def by auto private lemma inv_fromD: assumes "inv_from p A m" "i < n" "j < n" "j > m" shows "p A i j" using assms unfolding inv_from_def by auto private lemma inv_atI[intro]: assumes "⋀ i. i < n ⟹ p A i m" shows "inv_at p A m" using assms unfolding inv_at_def by auto private lemma inv_atD: assumes "inv_at p A m" "i < n" shows "p A i m" using assms unfolding inv_at_def by auto private lemma inv_all_imp_inv_part: "m i ≤ n ⟹ m_j ≤ n ⟹ inv_all p A ⟹ inv_part p A m_i m_j" unfolding inv_all_def inv_part_def by auto private lemma inv_all_eq_inv_part: "inv_all p A = inv_part p A n n" unfolding inv_all_def inv_part_def by auto private lemma inv_part_0_Suc: "m_j < n ⟹ inv_part p A 0 m_j = inv_part p A n (Suc m_j)" unfolding inv_part_def by (auto, case_tac "j = m_j", auto) private lemma inv_all_uppertD: "inv_all uppert A ⟹ j < i ⟹ i < n ⟹ A $$ (i,j) = 0" unfolding inv_all_def uppert_def by auto private lemma inv_all_diff_evD: "inv_all diff_ev A ⟹ i < j ⟹ j < n ⟹ A $$ (i, i) ≠ A $$ (j, j) ⟹ A $$ (i,j) = 0" unfolding inv_all_def diff_ev_def by auto private lemma inv_all_diff_ev_uppertD: assumes "inv_all diff_ev A" "inv_all uppert A" "i < n" "j < n" and neg: "A $$ (i, i) ≠ A $$ (j, j)" shows "A $$ (i,j) = 0" proof - from neg have "i ≠ j" by auto hence "i < j ∨ j < i" by arith thus ?thesis proof assume "i < j" from inv_all_diff_evD[OF assms(1) this ‹j < n› neg] show ?thesis . next assume "j < i" from inv_all_uppertD[OF assms(2) this ‹i < n›] show ?thesis . qed qed private lemma inv_from_bot_step: "p A i ⟹ inv_from_bot p A (Suc i) ⟹ inv_from_bot p A i" unfolding inv_from_bot_def by (auto, case_tac "ia = i", auto) private lemma same_diag_refl[simp]: "same_diag A A" unfolding same_diag_def by auto private lemma same_diag_trans: "same_diag A B ⟹ same_diag B C ⟹ same_diag A C" unfolding same_diag_def by auto private lemma same_diag_ev_blocks: "same_diag A B ⟹ ev_blocks A ⟹ ev_blocks B" unfolding same_diag_def ev_blocks_def ev_blocks_part_def by auto private lemma same_uptoI[intro]: assumes "⋀ i' j'. i' < n ⟹ j' < j ⟹ A $$ (i',j') = B $$ (i',j')" shows "same_upto j A B" using assms unfolding same_upto_def by blast private lemma same_uptoD[dest]: assumes "same_upto j A B" "i' < n" "j' < j" shows "A $$ (i',j') = B $$ (i',j')" using assms unfolding same_upto_def by blast private lemma same_upto_refl[simp]: "same_upto j A A" unfolding same_upto_def by auto private lemma same_upto_trans: "same_upto j A B ⟹ same_upto j B C ⟹ same_upto j A C" unfolding same_upto_def by auto private lemma same_upto_inv_upto_jb: "same_upto j A B ⟹ inv_upto jb A j ⟹ inv_upto jb B j" unfolding inv_upto_def same_upto_def jb_def by auto lemma jb_imp_diff_ev: "jb A i j ⟹ diff_ev A i j" unfolding jb_def diff_ev_def by auto private lemma ev_blocks_diag: "same_diag A B ⟹ ev_blocks B ⟹ ev_blocks A" unfolding ev_blocks_def ev_blocks_part_def same_diag_def by auto private lemma inv_all_imp_inv_from: "inv_all p A ⟹ inv_from p A k" unfolding inv_all_def inv_from_def by auto private lemma inv_all_imp_inv_at: "inv_all p A ⟹ k < n ⟹ inv_at p A k" unfolding inv_all_def inv_at_def by auto private lemma inv_from_upto_at_all: assumes "inv_upto jb A k" "inv_from diff_ev A k" "inv_from uppert A k" "inv_at p A k" and "⋀ i. i < n ⟹ p A i k ⟹ diff_ev A i k ∧ uppert A i k" shows "inv_all diff_ev A" "inv_all uppert A" proof - { fix i j assume ij: "i < n" "j < n" have "diff_ev A i j ∧ uppert A i j" proof (cases "j < k") case True with assms(1) ij have "jb A i j" unfolding inv_upto_def by auto thus ?thesis using ij unfolding jb_def diff_ev_def uppert_def by auto next case False note ge = this show ?thesis proof (cases "j = k") case True with assms(4-) ij show ?thesis unfolding inv_at_def by auto next case False with ge have "j > k" by auto with assms(2-3) ij show ?thesis unfolding inv_from_def by auto qed qed } thus "inv_all diff_ev A" "inv_all uppert A" unfolding inv_all_def by auto qed private lemma lower_one_diff_uppert: "i < n ⟹ lower_one k B i k ⟹ diff_ev B i k ∧ uppert B i k" unfolding lower_one_def diff_ev_def uppert_def by auto definition ev_block :: "nat ⇒ 'a mat ⇒ bool" where "⋀ n. ev_block n A = (∀ i j. i < n ⟶ j < n ⟶ A $$ (i,i) = A $$ (j,j))" lemma ev_blockD: "⋀ n. ev_block n A ⟹ i < n ⟹ j < n ⟹ A $$ (i,i) = A $$ (j,j)" unfolding ev_block_def carrier_mat_def by blast lemma same_diag_ev_block: "same_diag A B ⟹ ev_block n A ⟹ ev_block n B" unfolding ev_block_def carrier_mat_def same_diag_def by metis subsection ‹Alternative Characterization of @{const identify_blocks} in Presence of @{const ev_block}› private lemma identify_blocks_main_iff: assumes *: "k ≤ k'" "k' ≠ k ⟶ k > 0 ⟶ A $$ (k - 1, k) ≠ 1" and "k' < n" shows "set (identify_blocks_main A k list) = set list ∪ {(i,j) | i j. i ≤ j ∧ j < k ∧ (∀ l. i ≤ l ⟶ l < j ⟶ A $$ (l, Suc l) = 1) ∧ (Suc j ≠ k' ⟶ A $$ (j, Suc j) ≠ 1) ∧ (i > 0 ⟶ A $$ (i - 1, i) ≠ 1)}" (is "_ = _ ∪ ?ss A k") using * proof (induct A k list rule: identify_blocks_main.induct) case 1 show ?case unfolding identify_blocks_main.simps by auto next case (2 A i_e list) let ?s = "?ss A" obtain i_b where id: "identify_block A i_e = i_b" by force note IH = 2(1)[OF id[symmetric]] let ?res = "identify_blocks_main A (Suc i_e) list" let ?rec = "identify_blocks_main A i_b ((i_b, i_e) # list)" note idb = identify_block[OF id] hence res: "?res = ?rec" using id by simp from 2(2-) have iek: "i_e < k'" by simp from identify_block_le'[OF id] have ibe: "i_b ≤ i_e" . from ibe iek have "i_b ≤ k'" by simp have "k' ≠ i_b ⟶ 0 < i_b ⟶ A $$ (i_b - 1, i_b) ≠ 1" using idb(2) by auto note IH = IH[OF ‹i_b ≤ k'› this] have cong: "⋀ a b c d. insert a c = d ⟹ set (a # b) ∪ c = set b ∪ d" by auto show ?case unfolding res IH proof (rule cong) from ibe have "?s i_b ⊆ ?s (Suc i_e)" by auto moreover have inter: "⋀l. i_b ≤ l ⟹ l < i_e ⟹ A $$ (l, Suc l) = 1" using idb by blast have last: "Suc i_e ≠ k' ⟹ A $$ (i_e, Suc i_e) ≠ 1" using 2(3) by auto have "(i_b, i_e) ∈ ?s (Suc i_e)" using ibe idb(2) inter last by blast ultimately have "insert (i_b, i_e) (?s i_b) ⊆ ?s (Suc i_e)" by auto moreover { fix i j assume ij: "(i,j) ∈ ?s (Suc i_e)" hence "(i,j) ∈ insert (i_b, i_e) (?s i_b)" proof (cases "j < i_b") case True with ij show ?thesis by blast next case False with ij have "i_b ≤ j" "j ≤ i_e" by auto { assume j: "j < i_e" from idb(3)[OF ‹i_b ≤ j› this] have 1: "A $$ (j, Suc j) = 1" . from j ‹Suc i_e ≤ k'› have "Suc j ≠ k'" by auto with ij 1 have False by auto } with ‹j ≤ i_e› have j: "j = i_e" by (cases "j = i_e", auto) { assume i: "i < i_b ∨ i > i_b" hence False proof assume "i < i_b" hence "i_b > 0" by auto with idb(2) have *: "A $$ (i_b - 1, i_b) ≠ 1" by auto from ‹i < i_b› ‹i_b ≤ i_e› ‹i_e < k'› have "i ≤ i_b - 1" "i_b - 1 ≤ k'" by auto from ‹i < i_b› ‹i_b ≤ i_e› j have **: "i ≤ i_b - 1" "i_b - 1 < j" "Suc (i_b - 1) = i_b" by auto from ij have "⋀ l. l≥i ⟹ l < j ⟹ A $$ (l, Suc l) = 1" by auto from this[OF **(1-2)] **(3) * show False by auto next assume "i > i_b" with ij j have "A $$ (i - 1, i) ≠ 1" and *: "i - 1 ≥ i_b" "i - 1 ≤ i_e" "i - 1 < i_e" "Suc (i - 1) = i" by auto with idb(3)[OF *(1,3)] show False by auto qed } hence i: "i = i_b" by arith show ?thesis unfolding i j by simp qed } hence "?s (Suc i_e) ⊆ insert (i_b, i_e) (?s i_b)" by blast ultimately show "insert (i_b, i_e) (?s i_b) = ?s (Suc i_e)" by blast qed qed private lemma identify_blocks_iff: assumes "k < n" shows "set (identify_blocks A k) = {(i,j) | i j. i ≤ j ∧ j < k ∧ (∀ l. i ≤ l ⟶ l < j ⟶ A $$ (l, Suc l) = 1) ∧ (Suc j ≠ k ⟶ A $$ (j, Suc j) ≠ 1) ∧ (i > 0 ⟶ A $$ (i - 1, i) ≠ 1)}" unfolding identify_blocks_def using identify_blocks_main_iff[OF le_refl _ ‹k < n›] by auto private lemma identify_blocksD: assumes "k < n" and "(i,j) ∈ set (identify_blocks A k)" shows "i ≤ j" "j < k" "⋀ l. i ≤ l ⟹ l < j ⟹ A $$ (l, Suc l) = 1" "Suc j ≠ k ⟹ A $$ (j, Suc j) ≠ 1" "i > 0 ⟹ A $$ (i - 1, i - 1) ≠ A $$ (k,k) ∨ A $$ (i - 1, i) ≠ 1" using assms unfolding identify_blocks_iff[OF assms(1)] by auto private lemma identify_blocksI: assumes inv: "k < n" "i ≤ j" "j < k" "⋀ l. i ≤ l ⟹ l < j ⟹ A $$ (l, Suc l) = 1" "Suc j ≠ k ⟹ A $$ (j, Suc j) ≠ 1" "i > 0 ⟹ A $$ (i - 1, i) ≠ 1" shows "(i,j) ∈ set (identify_blocks A k)" unfolding identify_blocks_iff[OF inv(1)] using inv by blast private lemma identify_blocks_rev: assumes "A $$ (i, Suc i) = 0 ∧ Suc i < k ∨ Suc i = k" and inv: "k < n" shows "(identify_block A i, i) ∈ set (identify_blocks A k)" proof - obtain j where id: "identify_block A i = j" by force note idb = identify_block[OF this] show ?thesis unfolding id by (rule identify_blocksI[OF inv], insert idb assms, auto) qed subsection ‹Proving the Invariants› private lemma add_col_sub_row_diag: assumes A: "A ∈ carrier_mat n n" and ut: "inv_all uppert A" and ijk: "i < j" "j < n" "k < n" shows "add_col_sub_row a i j A $$ (k,k) = A $$ (k,k)" proof - from inv_all_uppertD[OF ut] show ?thesis by (subst add_col_sub_index_row, insert A ijk, auto) qed private lemma add_col_sub_row_diff_ev_part_old: assumes A: "A ∈ carrier_mat n n" and ij: "i ≤ j" "i ≠ 0" "i < n" "j < n" "i' < n" "j' < n" and choice: "j' < j ∨ j' = j ∧ i' ≥ i" and old: "inv_part diff_ev A i j" and ut: "inv_all uppert A" shows "diff_ev (add_col_sub_row a (i - 1) j A) i' j'" unfolding diff_ev_def proof (intro impI) assume ij': "i' < j'" let ?A = "add_col_sub_row a (i - 1) j A" assume neq: "?A $$ (i',i') ≠ ?A $$ (j',j')" from A have dim: "dim_row A = n" "dim_col A = n" by auto note utd = inv_all_uppertD[OF ut] let ?i = "i - 1" have "?i < j" using ‹i ≤ j› ‹i ≠ 0› ‹i < n› by auto from utd[OF this ‹j < n›] have Aji: "A $$ (j,?i) = 0" by simp from add_col_sub_row_diag[OF A ut ‹?i < j› ‹j < n›] have diag: "⋀ k. k < n ⟹ ?A $$ (k,k) = A $$ (k,k)" . from neq[unfolded diag[OF ‹i' < n›] diag[OF ‹j' < n›]] have neq: "A $$ (i',i') ≠ A $$ (j',j')" by auto { from inv_partD(3)[OF old ‹i' < n› ‹j' < n› choice] have "diff_ev A i' j'" by auto with neq ij' have "A $$ (i',j') = 0" unfolding diff_ev_def by auto } note zero = this { assume "i' ≠ ?i" "j' = j" with ij' ij(1) choice have "i' > ?i" by auto from utd[OF this] ij have "A $$ (i', ?i) = 0" by auto } note 1 = this { assume "j' ≠ j" "i' = ?i" with ij' ij(1) choice have "j > j'" by auto from utd[OF this] ij have "A $$ (j, j') = 0" by auto } note 2 = this from ij' ij choice have "(i' = ?i ∧ j' = j) = False" by arith note id = add_col_sub_index_row[of i' A j' j a ?i, unfolded dim this if_False, OF ‹i' < n› ‹i' < n› ‹j' < n› ‹j' < n› ‹j < n›] show "?A $$ (i',j') = 0" unfolding id zero using 1 2 by auto qed private lemma add_col_sub_row_uppert: assumes "A ∈ carrier_mat n n" and "i < j" and "j < n" and inv: "inv_all uppert (A :: 'a mat)" shows "inv_all uppert (add_col_sub_row a i j A)" unfolding inv_all_def uppert_def proof (intro allI impI) fix i' j' assume *: "i' < n" "j' < n" "j' < i'" note inv = inv_allD[OF inv, unfolded uppert_def] show "add_col_sub_row a i j A $$ (i', j') = 0" by (subst add_col_sub_index_row, insert assms * inv, auto) qed private lemma step_1_main_inv: "i ≤ j ⟹ A ∈ carrier_mat n n ⟹ inv_all uppert A ⟹ inv_part diff_ev A i j ⟹ inv_all uppert (step_1_main n i j A) ∧ inv_all diff_ev (step_1_main n i j A)" proof (induct i j A taking: n rule: step_1_main.induct) case (1 i j A) let ?i = "i - 1" note [simp] = step_1_main.simps[of n i j A] from 1(3-) have ij: "i ≤ j" and A: "A ∈ carrier_mat n n" and inv: "inv_all uppert A" "inv_part diff_ev A i j" by auto show ?case proof (cases "j ≥ n") case True thus ?thesis using inv by (simp add: inv_all_eq_inv_part, auto simp: inv_part_def) next case False hence jn: "j < n" by simp note IH = 1(1-2)[OF False] show ?thesis proof (cases "i = 0") case True from inv[unfolded True inv_part_0_Suc[OF jn]] have inv2: "inv_part diff_ev A n (j + 1)" by simp have "inv_part diff_ev A (j + 1) (j + 1)" proof (intro inv_partI) fix i' j' assume ij: "i' < n" "j' < n" and choice: "j' < j + 1 ∨ j' = j + 1 ∧ j + 1 ≤ i'" from inv_partD[OF inv2 ij] choice show "diff_ev A i' j'" using jn unfolding diff_ev_def by auto qed from IH(1)[OF True _ A inv(1) this] show ?thesis using jn by (simp, simp add: True) next case False let ?evi = "A $$ (?i,?i)" let ?evj = "A $$ (j,j)" let ?choice = "?evi ≠ ?evj ∧ A $$ (?i, j) ≠ 0" let ?A = "add_col_sub_row (A $$ (?i, j) / (?evj - ?evi)) ?i j A" let ?B = "if ?choice then ?A else A" obtain B where B: "B = ?B" by auto have Bn: "B ∈ carrier_mat n n" unfolding B using A by simp from False ij jn have *: "?i < j" "j < n" "?i < n" by auto have inv1: "inv_all uppert B" unfolding B using inv add_col_sub_row_uppert[OF A *(1-2) inv(1)] by auto note inv2 = inv_partD[OF inv(2)] have inv2: "inv_part diff_ev B ?i j" proof (cases ?choice) case False hence B: "B = A" unfolding B by auto show ?thesis unfolding B proof (rule inv_partI) fix i' j' assume ij: "i' < n" "j' < n" and "j' < j ∨ j' = j ∧ ?i ≤ i'" hence choice: "(j' < j ∨ j' = j ∧ i ≤ i') ∨ j' = j ∧ i' = ?i" by auto note inv2 = inv2[OF ij] from choice show "diff_ev A i' j'" proof assume "j' < j ∨ j' = j ∧ i ≤ i'" from inv2(3)[OF this] show ?thesis . next assume "j' = j ∧ i' = ?i" thus ?thesis using False unfolding diff_ev_def by auto qed qed next case True hence B: "B = ?A" unfolding B by auto from * True have "i < n" by auto note old = add_col_sub_row_diff_ev_part_old[OF A ‹i ≤ j› ‹i ≠ 0› ‹i < n› ‹j < n› _ _ _ inv(2) inv(1)] show ?thesis unfolding B proof (rule inv_partI) fix i' j' assume ij: "i' < n" "j' < n" and "j' < j ∨ j' = j ∧ ?i ≤ i'" hence choice: "(j' < j ∨ j' = j ∧ i ≤ i') ∨ j' = j ∧ i' = ?i" by auto note inv2 = inv2[OF ij] from choice show "diff_ev ?A i' j'" proof assume "j' < j ∨ j' = j ∧ i ≤ i'" from old[OF ij this] show ?thesis . next assume "j' = j ∧ i' = ?i" hence ij': "j' = j" "i' = ?i" by auto note diag = add_col_sub_row_diag[OF A inv(1) ‹?i < j› ‹j < n›] show ?thesis unfolding ij' diff_ev_def diag[OF ‹j < n›] diag[OF ‹?i < n›] proof (intro impI) from True have neq: "?evi ≠ ?evj" by simp note ut = inv_all_uppertD[OF inv(1)] obtain i' where i': "i' = i - Suc 0" by auto obtain diff where diff: "diff = ?evj - A $$ (i',i')" by auto from neq have [simp]: "diff ≠ 0" unfolding diff i' by auto from ut[OF ‹?i < j› ‹j < n›] have [simp]: "A $$ (j,i') = 0" unfolding diff i' by simp have "?A $$ (?i, j) = A $$ (i', j) + (A $$ (i', j) * A $$ (i', i') - A $$ (i', j) * A $$ (j, j)) / diff" by (subst add_col_sub_index_row, insert A *, auto simp: diff[symmetric] i'[symmetric] field_simps) also have "A $$ (i', j) * A $$ (i', i') - A $$ (i', j) * A $$ (j, j) = - A $$ (i',j) * diff" by (simp add: diff i' field_simps) also have "… / diff = - A $$ (i',j)" by simp finally show "?A $$ (?i,j) = 0" by simp qed qed qed qed from ij have "i - 1 ≤ j" by simp note IH = IH(2)[OF False refl refl refl refl B this Bn inv1 inv2] from False jn have id: "step_1_main n i j A = step_1_main n (i - 1) j B" unfolding B by (simp add: Let_def) show ?thesis unfolding id by (rule IH) qed qed qed private lemma step_2_main_inv: "A ∈ carrier_mat n n ⟹ inv_all uppert A ⟹ inv_all diff_ev A ⟹ ev_blocks_part j A ⟹ inv_all uppert (step_2_main n j A) ∧ inv_all diff_ev (step_2_main n j A) ∧ ev_blocks (step_2_main n j A)" proof (induct j A taking: n rule: step_2_main.induct) case (1 j A) note [simp] = step_2_main.simps[of n j A] from 1(2-) have A: "A ∈ carrier_mat n n" and inv: "inv_all uppert A" "inv_all diff_ev A" "ev_blocks_part j A" by auto show ?case proof (cases "j ≥ n") case True with inv(3) have "ev_blocks A" unfolding ev_blocks_def ev_blocks_part_def by auto thus ?thesis using True inv(1-2) by auto next case False hence jn: "j < n" by simp note intro = ev_blocks_partI note dest = ev_blocks_partD note IH = 1(1)[OF False] let ?look = "lookup_ev (A $$ (j,j)) j A" let ?B = "case ?look of None ⇒ A | Some i ⇒ swap_cols_rows_block (Suc i) j A" obtain B where B: "B = ?B" by auto have id: "step_2_main n j A = step_2_main n (Suc j) B" unfolding B using False by simp have Bn: "B ∈ carrier_mat n n" unfolding B using A by (auto split: option.splits) have "inv_all uppert B ∧ inv_all diff_ev B ∧ ev_blocks_part (Suc j) B" proof (cases ?look) case None have "ev_blocks_part (Suc j) A" proof (intro intro) fix i' j' k' assume *: "i' < j'" "j' < k'" "k' < Suc j" "A $$ (k',k') = A $$ (i',i')" show "A $$ (j',j') = A $$ (i',i')" proof (cases "j = k'") case False with * have "k' < j" by auto from dest[OF inv(3) *(1-2) this *(4)] show ?thesis . next case True with lookup_ev_None[OF None, of i'] * have False by simp thus ?thesis .. qed qed with None show ?thesis unfolding B using inv by auto next case (Some i) from lookup_ev_Some[OF Some] have ij: "i < j" and id: "A $$ (i, i) = A $$ (j, j)" and neq: "⋀ k. i < k ⟹ k < j ⟹ A $$ (k,k) ≠ A $$ (j,j)" by auto let ?A = "swap_cols_rows_block (Suc i) j A" let ?perm = "λ i'. if i' = Suc i then j else if Suc i < i' ∧ i' ≤ j then i' - 1 else i'" from Some have B: "B = ?A" unfolding B by simp have Aind: "⋀ i' j'. i' < n ⟹ j' < n ⟹ ?A $$ (i', j') = A $$ (?perm i', ?perm j')" by (subst swap_cols_rows_block_index, insert False A ij, auto) have inv_ev: "ev_blocks_part (Suc j) ?A" proof (intro intro) fix i' j' k assume *: "i' < j'" "j' < k" "k < Suc j" and ki: "?A $$ (k,k) = ?A $$ (i',i')" from * jn have "j' < n" "i' < n" "k < n" by auto note id' = Aind[OF ‹j' < n› ‹j' < n›] Aind[OF ‹i' < n› ‹i' < n›] Aind[OF ‹k < n› ‹k < n›] note inv_ev = dest[OF inv(3)] show "?A $$ (j',j') = ?A $$ (i',i')" proof (cases "i' < Suc i") case True note i' = this hence pi: "?perm i' = i'" by simp show ?thesis proof (cases "j' < Suc i") case True note j' = this hence pj: "?perm j' = j'" by simp show ?thesis proof (cases "k < Suc i") case True note k = this hence pk: "?perm k = k" by simp from True ij have "k < j" by simp from inv_ev[OF *(1-2) this] ki show ?thesis unfolding id' pi pj pk by auto next case False note kf1 = this show ?thesis proof (cases "k = Suc i") case True note k = this hence pk: "?perm k = j" by simp from ki id have ii': "A $$ (i, i) = A $$ (i', i')" unfolding id' pi pj pk by simp have ji: "A $$ (j',j') = A $$ (i',i')" proof (cases "j' = i") case True with ii' show ?thesis by simp next case False with ‹j' < Suc i› have "j' < i" by auto from ki id inv_ev[OF ‹i' < j'› this ij] show ?thesis unfolding id' pi pj pk by simp qed thus ?thesis unfolding id' pi pj pk . next case False note kf2 = this with kf1 have k: "k > Suc i" by auto hence pk: "?perm k = k - 1" and kj: "k - 1 < j" using * ‹k < Suc j› by auto from k j' have "j' < k - 1" by auto from inv_ev[OF *(1) this kj] ki show ?thesis unfolding id' pi pj pk by simp qed qed next case False note j'f1 = this show ?thesis proof (cases "j' = Suc i") case True note j' = this hence pj: "?perm j' = j" by simp from j' * have k: "k > Suc i" by auto hence pk: "?perm k = k - 1" and kj: "k - 1 < j" using * ‹k < Suc j› by auto from ki[unfolded id' pi pj pk] have eq: "A $$ (k - 1, k - 1) = A $$ (i', i')" . from * i' k have le: "i' ≤ i" and lt: "i < k - 1" "k - 1 < j" by auto from inv_ev[OF _ lt eq] le have "A $$ (i, i) = A $$ (i', i')" by (cases "i = i'", auto) with id show ?thesis unfolding id' pi pj pk by simp next case False note j'f2 = this with j'f1 have "j' > Suc i" by auto hence pj: "?perm j' = j' - 1" and pk: "?perm k = k - 1" and kj: "i' < j' - 1" "j' - 1 < k - 1" "k - 1 < j" using * i' ‹k < Suc j› by auto from inv_ev[OF kj] ki show ?thesis unfolding id' pi pj pk by simp qed qed next case False note i'f1 = this show ?thesis proof (cases "i' = Suc i") case True note i' = this with * have gt: "i < k - 1" "k - 1 < j" and perm: "?perm i' = j" "?perm k = k - 1" by auto from ki[unfolded id' perm] neq[OF gt] have False by auto thus ?thesis .. next case False note i'f2 = this with i'f1 have "i' > Suc i" by auto with * have gt: "i' - 1 < j' - 1" "j' - 1 < k - 1" "k - 1 < j" and perm: "?perm i' = i' - 1" "?perm j' = j' - 1" "?perm k = k - 1" by auto show ?thesis using inv_ev[OF gt] ki unfolding id' perm by simp qed qed qed let ?both = "λ A i j. uppert A i j ∧ diff_ev A i j" have "inv_all ?both ?A" proof (intro inv_allI) fix ii jj assume ii: "ii < n" and jj: "jj < n" note id = Aind[OF ii ii] Aind[OF jj jj] Aind[OF ii jj] note ut = inv_all_uppertD[OF inv(1)] note diff = inv_all_diff_evD[OF inv(2)] have upper: "uppert ?A ii jj" unfolding uppert_def proof assume ji: "jj < ii" show "?A $$ (ii,jj) = 0" proof (cases "ii < Suc i") case True note i = this with ji have perm: "?perm ii = ii" "?perm jj = jj" by auto show ?thesis unfolding id perm using ut[OF ji ii] . next case False note if1 = this show ?thesis proof (cases "ii = Suc i") case True note i = this with ji ij have perm: "?perm ii = j" "?perm jj = jj" and jj: "jj < j" by auto show ?thesis unfolding id perm by (rule ut[OF jj jn]) next case False with if1 have if1: "ii > Suc i" by auto show ?thesis proof (cases "ii ≤ j") case True note i = this with if1 have pi: "?perm ii = ii - 1" by auto show ?thesis proof (cases "jj = Suc i") case True note j = this hence pj: "?perm jj = j" by simp from i ji if1 ii j have ij: "ii - 1 < j" and ii: "i < ii - 1" by auto show ?thesis unfolding id pi pj by (rule diff[OF ij jn neq[OF ii ij]]) next case False with i ji if1 ii have "?perm jj < ii - 1" "ii - 1 < n" by auto from ut[OF this] show ?thesis unfolding id pi . qed next case False hence i: "ii > j" by auto with if1 have pi: "?perm ii = ii" by simp from i ji if1 ii have "?perm jj < ii" by auto from ut[OF this ii] show ?thesis unfolding id pi . qed qed qed qed have diff: "diff_ev ?A ii jj" unfolding diff_ev_def proof (intro impI) assume ij': "ii < jj" and neq: "?A $$ (ii,ii) ≠ ?A $$ (jj,jj)" show "?A $$ (ii,jj) = 0" proof (cases "jj < Suc i") case True note j = this with ij' have perm: "?perm ii = ii" "?perm jj = jj" by auto show ?thesis using neq unfolding id perm using diff[OF ij' jj] by simp next case False note jf1 = this show ?thesis proof (cases "jj = Suc i") case True note j = this with ij' ij have perm: "?perm jj = j" "?perm ii = ii" and ii: "ii < j" by auto show ?thesis using neq unfolding id perm by (intro diff[OF ii jn]) next case False with jf1 have jf1: "jj > Suc i" by auto show ?thesis proof (cases "jj ≤ j") case True note j = this with jf1 have pj: "?perm jj = jj - 1" by auto show ?thesis proof (cases "ii = Suc i") case True note i = this hence pi: "?perm ii = j" by simp from i ij' jf1 jj j have ij: "jj - 1 < j" by auto show ?thesis unfolding id pi pj by (rule ut[OF ij jn]) next case False with j ij' jf1 jj have "?perm ii < jj - 1" "jj - 1 < n" by auto from diff[OF this] neq show ?thesis unfolding id pj . qed next case False hence j: "jj > j" by auto with jf1 have pj: "?perm jj = jj" by simp from j ij' jf1 jj have "?perm ii < jj" by auto from diff[OF this jj] neq show ?thesis unfolding id pj . qed qed qed qed from upper diff show "?both ?A ii jj" .. qed hence "inv_all diff_ev ?A" "inv_all uppert ?A" unfolding inv_all_def by blast+ with inv_ev show ?thesis unfolding B by auto qed with IH[OF refl B Bn] show ?thesis unfolding id by auto qed qed private lemma add_col_sub_row_same_upto: assumes "i < j" "j < n" "A ∈ carrier_mat n n" "inv_upto uppert A j" shows "same_upto j A (add_col_sub_row v i j A)" by (intro same_uptoI, subst add_col_sub_index_row, insert assms, auto simp: uppert_def inv_upto_def) private lemma add_col_sub_row_inv_from_uppert: assumes *: "inv_from uppert A j" and **: "A ∈ carrier_mat n n" "i < n" "i < j" "j < n" shows "inv_from uppert (add_col_sub_row v i j A) j" proof - note * = * ** let ?A = "add_col_sub_row v i j A" show "inv_from uppert ?A j" unfolding inv_from_def proof (intro allI impI) fix i' j' assume **: "i' < n" "j' < n" "j < j'" from * ** have "i' < dim_row A" "i' < dim_col A" "j' < dim_row A" "j' < dim_col A" "j < dim_row A" by auto note id2 = add_col_sub_index_row[OF this] show "uppert ?A i' j'" unfolding uppert_def proof (intro conjI impI) assume "j' < i'" with inv_fromD[OF ‹inv_from uppert A j›, unfolded uppert_def, of i' j'] * ** show "?A $$ (i',j') = 0" unfolding id2 using * ** ‹j' < i'› by simp qed qed qed private lemma step_3_a_inv: "A ∈ carrier_mat n n ⟹ i < j ⟹ j < n ⟹ inv_upto jb A j ⟹ inv_from uppert A j ⟹ inv_from_bot (λ A i. one_zero A i j) A i ⟹ ev_block n A ⟹ inv_from uppert (step_3_a i j A) j ∧ inv_upto jb (step_3_a i j A) j ∧ inv_at one_zero (step_3_a i j A) j ∧ same_diag A (step_3_a i j A)" proof (induct i j A rule: step_3_a.induct) case (1 j A) thus ?case by (simp add: inv_from_bot_def inv_at_def) next case (2 i j A) from 2(2-) have A: "A ∈ carrier_mat n n" and ij: "Suc i < j" "i < j" and j: "j < n" by auto let ?cond = "A $$ (i, i + 1) = 1 ∧ A $$ (i, j) ≠ 0" let ?B = "add_col_sub_row (- A $$ (i, j)) (Suc i) j A" obtain B where B: "B = (if ?cond then ?B else A)" by auto from A have Bn: "B ∈ carrier_mat n n" unfolding B by simp note IH = 2(1)[OF refl B Bn ij(2) j] have id: "step_3_a (Suc i) j A = step_3_a i j B" unfolding B by (simp add: Let_def) from ij j have *: "Suc i < n" "j < n" "Suc i ≠ j" by auto from 2(2-) have inv: "inv_upto jb A j" "inv_from uppert A j" "ev_block n A" "inv_from_bot (λA i. one_zero A i j) A (Suc i)" by auto note evbA = ev_blockD[OF inv(3)] show ?case proof (cases ?cond) case False hence B: "B = A" unfolding B by auto have inv2: "inv_from_bot (λA i. one_zero A i j) A i" by (rule inv_from_bot_step[OF _ inv(4)], insert False ij evbA[of i j] *, auto simp: one_zero_def) show ?thesis unfolding id B by (rule IH[unfolded B], insert inv inv2, auto) next case True hence B: "B = ?B" unfolding B by auto let ?C = "step_3_a i j B" from inv_uptoD[OF inv(1) j *(1) ij(1), unfolded jb_def] ij have Aji: "A $$ (j, Suc i) = 0" by auto have diag: "same_diag A B" unfolding same_diag_def by (intro allI impI, insert ij j A Aji B, auto) have upto: "same_upto j A B" unfolding B by (rule add_col_sub_row_same_upto[OF ‹Suc i < j› ‹j < n› A inv_upto_mono[OF jb_imp_uppert inv(1)]]) from add_col_sub_row_inv_from_uppert[OF inv(2) A ‹Suc i < n› ‹Suc i < j› ‹j < n›] have from_j: "inv_from uppert B j" unfolding B by blast have ev: "A $$ (Suc i, Suc i) = A $$ (j,j)" using evbA[of "Suc i" j] ij j by auto have evb_B: "ev_block n B" by (rule same_diag_ev_block[OF diag inv(3)]) note evbB = ev_blockD[OF evb_B] { fix k assume "k < n" with A * have k: "k < dim_row A" "k < dim_col A" "j < dim_row A" "j < dim_col A" "j < dim_row A" by auto note id = B add_col_sub_index_row[OF k] have "B $$ (k,j) = (if k = i then 0 else A $$ (k,j))" unfolding id using inv_uptoD[OF inv(1), of k "Suc i", unfolded jb_def] by (insert * Aji True ij ‹k < n›, auto simp: ev) } note id2 = this have "inv_from_bot (λA i. one_zero A i j) B i" unfolding inv_from_bot_def proof (intro allI impI) fix k assume "i ≤ k" "k < n" thus "one_zero B k j" using inv(4)[unfolded inv_from_bot_def] upto[unfolded same_upto_def] evbB[OF ‹k < n› ‹j < n›] unfolding one_zero_def id2[OF ‹k < n›] by auto qed from IH[OF same_upto_inv_upto_jb[OF upto inv(1)] from_j this evb_B] same_diag_trans[OF diag] show ?thesis unfolding id by blast qed qed private lemma identify_block_cong: assumes su: "same_upto k A B" and kn: "k < n" shows "i < k ⟹ identify_block A i = identify_block B i" proof (induct i) case (Suc i) hence "i < k" by auto note IH = Suc(1)[OF this] let ?c = "λ A. A $$ (i,Suc i) = 1" from same_uptoD[OF su, of i "Suc i"] kn Suc(2) have 1: "A $$ (i, Suc i) = B $$ (i, Suc i)" by auto from 1 have id: "?c A = ?c B" by simp show ?case proof (cases "?c A") case True with True[unfolded id] IH show ?thesis by simp next case False with False[unfolded id] show ?thesis by auto qed qed simp private lemma identify_blocks_main_cong: "k < n ⟹ same_upto k A B ⟹ identify_blocks_main A k xs = identify_blocks_main B k xs" proof (induct k arbitrary: xs rule: less_induct) case (less k list) show ?case proof (cases "k = 0") case False then obtain i_e where k: "k = Suc i_e" by (cases k, auto) obtain i_b where idA: "identify_block A i_e = i_b" by force from identify_block_le'[OF idA] have ibe: "i_b ≤ i_e" . have idB: "identify_block B i_e = i_b" unfolding idA[symmetric] by (rule sym, rule identify_block_cong, insert k less(2-3), auto) let ?I = "identify_blocks_main" let ?resA = "?I A (Suc i_e) list" let ?recA = "?I A i_b ((i_b, i_e) # list)" let ?resB = "?I B (Suc i_e) list" let ?recB = "?I B i_b ((i_b, i_e) # list)" have res: "?resA = ?recA" "?resB = ?recB" using idA idB by auto from k ibe have ibk: "i_b < k" by simp with less(3) have "same_upto i_b A B" unfolding same_upto_def by auto from less(1)[OF ibk _ this] ibk ‹k < n› have "?recA = ?recB" by auto thus ?thesis unfolding k res by simp qed simp qed private lemma identify_blocks_cong: "k < n ⟹ same_diag A B ⟹ same_upto k A B ⟹ identify_blocks A k = identify_blocks B k" unfolding identify_blocks_def by (intro identify_blocks_main_cong, auto simp: same_diag_def) private lemma inv_from_upto_at_all_ev_block: assumes jb: "inv_upto jb A k" and ut: "inv_from uppert A k" and at: "inv_at p A k" and evb: "ev_block n A" and p: "⋀ i. i < n ⟹ p A i k ⟹ uppert A i k" and k: "k < n" shows "inv_all uppert A" proof (rule inv_from_upto_at_all[OF jb _ ut at]) from ev_blockD[OF evb] show "inv_from diff_ev A k" unfolding inv_from_def diff_ev_def by blast fix i assume "i < n" "p A i k" with ev_blockD[OF evb k, of i] p[OF this] k show "diff_ev A i k ∧ uppert A i k" unfolding diff_ev_def by auto qed text ‹For step 3c, during the inner loop, the invariants are NOT preserved. However, at the end of the inner loop, the invariants are again preserved. Therefore, for the inner loop we prove how the resulting matrix looks like in each iteration.› private lemma step_3_c_inner_result: assumes inv: "inv_upto jb A k" "inv_from uppert A k" "inv_at one_zero A k" "ev_block n A" and k: "k < n" and A: "A ∈ carrier_mat n n" and lbl: "(lb,l) ∈ set (identify_blocks A k)" and ib_block: "(i_begin,i_end) ∈ set (identify_blocks A k)" and il: "i_end ≠ l" and large: "l - lb ≥ i_end - i_begin" and Alk: "A $$ (l,k) ≠ 0" shows "step_3_c_inner_loop (A $$ (i_end, k) / A $$ (l,k)) l i_end (Suc i_end - i_begin) A = mat n n (λ(i, j). if (i, j) = (i_end, k) then 0 else if i_begin ≤ i ∧ i ≤ i_end ∧ k < j then A $$ (i, j) - A $$ (i_end, k) / A $$ (l,k) * A $$ (l + i - i_end, j) else A $$ (i, j))" (is "?L = ?R") proof - let ?Alk = "A $$ (l,k)" let ?Aik = "A $$ (i_end,k)" define quot where "quot = ?Aik / ?Alk" let ?idiff = "i_end - i_begin" let ?m = "λ iter diff i j. if (i,j) = (i_end,k) then if diff = (Suc ?idiff) then ?Aik else 0 else if i ≥ i_begin + diff ∧ i ≤ i_end ∧ k < j then A $$ (i, j) - quot * A $$ (l + i - i_end, j) else if (i,j) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff} then quot else A $$ (i,j)" let ?mm = "λ iter diff i j. if (i,j) = (i_end,k) then 0 else if i ≥ i_begin + diff ∧ i ≤ i_end ∧ k < j then A $$ (i, j) - quot * A $$ (l + i - i_end, j) else if (i,j) = (i_end - Suc iter, l - iter) ∧ iter ≠ ?idiff then quot else A $$ (i,j)" let ?mat = "λ iter diff. mat n n (λ (i,j). ?m iter diff i j)" from identify_blocks[OF ib_block] have ib: "i_begin ≤ i_end" "i_end < k" by auto from identify_blocks[OF lbl] have lb: "lb ≤ l" "l < k" by auto have mend: "?mat 0 (Suc ?idiff) = A" by (rule eq_matI, insert A ib, auto) { fix ll ii diff iter assume "diff ≠ 0 ⟹ ii + iter = i_end" "diff ≠ 0 ⟹ ll + iter = l" "diff + iter = Suc ?idiff" hence "step_3_c_inner_loop quot ll ii diff (?mat iter diff) = ?R" proof (induct diff arbitrary: ii ll iter) case 0 hence iter: "iter = Suc ?idiff" by auto have "step_3_c_inner_loop quot ll ii 0 (?mat iter 0) = ?mat (Suc ?idiff) 0" unfolding iter step_3_c_inner_loop.simps .. also have "… = ?R" by (rule eq_matI, insert ib, auto simp: quot_def) finally show ?case . next case (Suc diff ii ll) note prems = Suc(2-) let ?B = "?mat iter (Suc diff)" have "step_3_c_inner_loop quot ll ii (Suc diff) ?B = step_3_c_inner_loop quot (ll - 1) (ii - 1) diff (add_col_sub_row quot ii ll ?B)" by simp also have "add_col_sub_row quot ii ll ?B = ?mat (Suc iter) diff" (is "?C = ?D") proof (rule eq_matI, unfold dim_row_mat dim_col_mat) fix i j assume i: "i < n" and j: "j < n" have ll: "ll < n" using prems lb k by auto from prems ib k have ii: "ii ≥ i_begin" "ii < n" "ii < k" "ii ≤ i_end" and eqs: "ii + iter = i_end" "ll + iter = l" "Suc diff + iter = Suc ?idiff" by auto from eqs have diff: "diff < Suc ?idiff" by auto from eqs lb ‹k < n› have "ll < k" "l < n" by auto note index = ib lb k i j ll il large ii this let ?Aij = "A $$ (i,j)" have D: "?D $$ (i,j) = ?mm iter diff i j" using diff i j by (auto split: if_splits) define B where "B = ?B" have BB: "⋀ i j. i < n ⟹ j < n ⟹ B $$ (i,j) = ?m iter (Suc diff) i j" unfolding B_def by auto have B: "B $$ (i,j) = ?m iter (Suc diff) i j" by (rule BB[OF i j]) have C: "?C $$ (i, j) = (if i = ii ∧ j = ll then B $$ (i, j) + quot * B $$ (i, i) - quot * quot * B $$ (j, i) - quot * B $$ (j, j) else if i = ii ∧ j ≠ ll then B $$ (i, j) - quot * B $$ (ll, j) else if i ≠ ii ∧ j = ll then B $$ (i, j) + quot * B $$ (i, ii) else B $$ (i, j))" unfolding B_def by (rule add_col_sub_index_row(1), insert i j ll, auto) from inv_from_upto_at_all_ev_block[OF inv(1-4) _ ‹k < n›] have invA: "inv_all uppert A" unfolding one_zero_def uppert_def by auto note ut = inv_all_uppertD[OF invA] note jb = inv_uptoD[OF inv(1), unfolded jb_def] note oz = inv_atD[OF inv(3), unfolded one_zero_def] note evb = ev_blockD[OF inv(4)] note iblock = identify_blocksD[OF ‹k < n›] note ibe = iblock[OF ib_block] let ?ev = "λ i. A $$ (i,i)" { fix i ib ie assume "(ib,ie) ∈ set (identify_blocks A k)" and i: "ib ≤ i" "i < ie" note ibe = iblock[OF this(1)] from ibe(3)[OF i] have id: "A $$ (i, Suc i) = 1" by auto from i ibe ‹k < n› have "i < n" "Suc i < k" by auto with oz[OF this(1)] id have "A $$ (i,k) = 0" by auto } note A_ik = this { fix i assume i: "i < n" and "¬ (i ≥ i_begin ∧ i ≤ i_end)" hence choice: "i > i_end ∨ i < i_begin" by auto note index = index i from index eqs choice have "i ≠ ii" by auto { assume 0: "A $$ (i,ii) ≠ 0" from 0 ut[of ii, OF _ i] ‹i ≠ ii› have "i < ii" by force from choice index eqs this have "i < i_begin" by auto with index have "i < k" by auto from jb[OF i ‹ii < n› ‹ii < k›] 0 ‹i ≠ ii› have *: "Suc i = ii" "A $$ (i,ii) = 1" "?ev i = ?ev ii" by auto with index ‹i < i_begin› have "ii = i_begin" by auto with evb[OF ‹i < n› ‹k < n›] ibe(5) * have False by auto } hence Aii: "A $$ (i,ii) = 0" by auto { fix j assume j: "j < n" have B: "B $$ (i,j) = ?m iter (Suc diff) i j" using i j unfolding B_def by simp from choice have id: "((i, j) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff}) = False" using ib index eqs by auto have "B $$ (i,j) = A $$ (i,j)" unfolding B id using choice ib index by auto } note Aii this } hence A_outside_ii: "⋀ i. i < n ⟹ ¬ (i_begin ≤ i ∧ i ≤ i_end) ⟹ A $$ (i, ii) = 0" and B_outside: "⋀ i j. i < n ⟹ j < n ⟹ ¬ (i_begin ≤ i ∧ i ≤ i_end) ⟹ B $$ (i, j) = A $$ (i, j)" by auto from diff eqs have iter: "iter ≠ Suc ?idiff" by auto { fix ib ie jb je assume i: "(ib,ie) ∈ set (identify_blocks A k)" and j: "(jb,je) ∈ set (identify_blocks A k)" and lt: "ie < je" note i = iblock[OF i] note j = iblock[OF j] from i j lt have "Suc ie < k" by auto with i have Aie: "A $$ (ie, Suc ie) ≠ 1" by auto have "ie < jb" proof (rule ccontr) assume "¬ ie < jb" hence "ie ≥ jb" by auto from j(3)[OF this lt] Aie show False by auto qed } note block_bounds = this { assume "i_end < l" from block_bounds[OF ib_block lbl this] have "i_end < lb" . } note i_less_l = this { assume "l < i_end" from block_bounds[OF lbl ib_block this] have "l < i_begin" . } note l_less_i = this { assume "i_end - iter = Suc l - iter" with iter large eqs have "i_end = Suc l" by auto with l_less_i have "l < i_begin" by auto with index ‹i_end = Suc l› have "i_begin = i_end" by auto } note block = this have Alie: "A $$ (l, i_end) = 0" proof (cases "l < i_end") case True { assume nz: "A $$ (l, i_end) ≠ 0" from l_less_i[OF True] index have "0 < i_begin" "l < i_begin" "i_end < n" "i_end < k" by auto from jb[OF ‹l < n› this(3-4)] il nz have "i_end = Suc l" "A $$ (l, Suc l) = 1" by auto with iblock[OF lbl] have "k = Suc l" by auto with ‹i_end = Suc l› ‹i_end < k› have False by auto } thus ?thesis by auto next case False with il have "i_end < l" by auto from ut[OF this ‹l < n›] show ?thesis . qed show "?C $$ (i,j) = ?D $$ (i,j)" proof (cases "i ≥ i_begin ∧ i ≤ i_end") case False hence choice: "i > i_end ∨ i < i_begin" by auto from choice have id: "((i, j) = (i_end - Suc iter, l - iter) ∧ iter ≠ ?idiff) = False" using ib index eqs by auto have D: "?D $$ (i,j) = ?Aij" unfolding D id using choice ib index by auto have B: "B $$ (i,j) = ?Aij" unfolding B_outside[OF i j False] .. from index eqs False have "i ≠ ii" by auto have Bii: "B $$ (i, ii) = A $$ (i,ii)" unfolding B_outside[OF i ‹ii < n› False] .. hence C: "?C $$ (i,j) = ?Aij" unfolding C B Bii using ‹i ≠ ii› A_outside_ii[OF i False] by auto show ?thesis unfolding D C .. next case True with index have "i_begin ≤ i" "i ≤ i_end" "i < k" by auto note index = index this show ?thesis proof (cases "j > k") case True note index = index this have D: "?D $$ (i,j) = (if i_begin + diff ≤ i then ?Aij - quot * A $$ (l + i - i_end, j) else ?Aij)" unfolding D using index by auto have B: "B $$ (i,j) = (if i_begin + Suc diff ≤ i then ?Aij - quot * A $$ (l + i - i_end, j) else ?Aij)" unfolding B using index by auto from index eqs have "j > ll" by auto hence C: "?C $$ (i,j) = (if i = ii then B $$ (i, j) - quot * B $$ (ll, j) else B $$ (i, j))" unfolding C using index by auto show ?thesis proof (cases "i_begin + Suc diff ≤ i ∨ ¬ (i_begin + diff ≤ i)") case True from True eqs index have "i ≠ ii" by auto from True have "?D $$ (i,j) = B $$ (i,j)" unfolding D B by auto also have "B $$ (i,j) = ?C $$ (i,j)" unfolding C using ‹i ≠ ii› by auto finally show ?thesis .. next case False hence i: "i = i_begin + diff" by simp with eqs index have ii: "ii = i" by auto from index eqs i ii have ll: "ll = l + i - i_end" by auto have not: "¬ (i_begin + Suc diff ≤ ll ∧ ll ≤ i_end)" proof from eqs have "ll ≤ l" by auto assume "i_begin + Suc diff ≤ ll ∧ ll ≤ i_end" hence "i_begin < ll" "ll ≤ i_end" by auto with ‹ll ≤ l› have "i_begin < l" by auto with l_less_i have "¬ l < i_end" by auto hence "l ≥ i_end" by simp with il i_less_l have "i_end < lb" by auto from index large eqs have "lb ≤ ll" by auto with ‹i_end < lb› have "i_end < ll" by auto with ‹ll ≤ i_end› show False by auto qed have D: "?D $$ (i,j) = ?Aij - quot * A $$ (ll, j)" unfolding D unfolding i ll by simp have C: "?C $$ (i,j) = ?Aij - quot * B $$ (ll, j)" unfolding C B unfolding ii i by simp have B: "B $$ (ll, j) = A $$ (ll, j)" unfolding BB[OF ‹ll < n› j] using index not by auto show ?thesis unfolding C D B unfolding ii i by (simp split: if_splits) qed next case False hence "j < k ∨ j = k" by auto thus ?thesis proof assume jk: "j = k" hence "j ≠ Suc l - Suc iter" using index by auto hence "?D $$ (i,j) = (if i = i_end then 0 else ?Aij)" unfolding D using jk by auto also have "… = 0" using A_ik[OF ib_block ‹i_begin ≤ i›] ‹i ≤ i_end› unfolding jk by auto finally have D: "?D $$ (i,j) = 0" . from jk index have "j ≠ ll" by auto hence C: "?C $$ (i,j) = (if i = ii then B $$ (i, j) - quot * B $$ (ll, j) else B $$ (i, j))" unfolding C unfolding jk by simp have C: "?C $$ (i,j) = 0" proof (cases "i = i_end") case False with index ii jk have i: "i_begin ≤ i" "i < i_end" by auto from A_ik[OF ib_block this] have Aij: "A $$ (i,j) = 0" unfolding jk . from index i jk have "¬ ((i, j) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff})" by auto hence Bij: "B $$ (i,j) = 0" unfolding B Aij using i jk by auto hence C: "?C $$ (i,j) = (if i = ii then - quot * B $$ (ll,j) else 0)" unfolding C by auto let ?l = "l - iter" from index eqs have ll: "ll = ?l" by auto show "?C $$ (i,j) = 0" proof (cases "i = ii") case True with index eqs i have l: "lb ≤ ?l" "?l < l" and diff: "Suc diff ≠ Suc ?idiff" by auto from A_ik[OF lbl l] have Alj: "A $$ (ll,j) = 0" unfolding jk ll . from index l jk eqs have "¬ ((ll, j) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff})" by auto hence Bij: "B $$ (ll,j) = 0" unfolding BB[OF ‹ll < n› j] Alj using l jk diff by auto thus ?thesis unfolding C by simp next case False thus ?thesis unfolding C by simp qed next case True note i = this hence Bij: "B $$ (i,j) = (if diff = ?idiff then A $$ (i_end, k) else 0)" unfolding B unfolding jk by auto show ?thesis proof (cases "i = ii") case True with i eqs have "diff = ?idiff" "ll = l" "iter = 0" by auto hence B: "B $$ (i,j) = A $$ (i_end,k)" unfolding Bij by auto have C: "?C $$ (i,j) = A $$ (i_end,k) - quot * B $$ (l, k)" unfolding C B unfolding True ‹ll =l› jk by simp also have "B $$ (l,k) = A $$ (l,k)" unfolding BB[OF ‹l < n› ‹k < n›] using il ‹iter = 0› by auto also have "A $$ (i_end,k) - quot * … = 0" unfolding quot_def using Alk by auto finally show ?thesis . next case False with i eqs have "diff ≠ ?idiff" by auto thus ?thesis unfolding C Bij using False by auto qed qed show ?thesis unfolding C D .. next assume jk: "j < k" from eqs il have "ii ≠ ll" by auto show ?thesis proof (cases "diff = 0 ∨ (i,j) ≠ (ii - 1,ll)") case False with eqs have **: "i = i_end - Suc iter" "j = l - iter" "iter ≠ ?idiff" and *: "diff ≠ 0" "i = ii - 1" "j = ll" "ii ≠ 0" "i ≠ ii" by auto hence D: "?D $$ (i,j) = quot" unfolding D using jk index by auto from * index eqs False jk have i: "ii = Suc i" "i < i_end" by auto from iblock(3)[OF ib_block ‹i_begin ≤ i› ‹i < i_end›] have Ai: "A $$ (i, ii) = 1" unfolding i . have "ii < k" "i ≠ i_end - iter" using index * ** eqs by (blast, force) hence Bi: "B $$ (i,ii) = 1" unfolding BB[OF ‹i < n› ‹ii < n›] Ai by auto have "B $$ (i,ll) = A $$ (i,ll)" unfolding BB[OF ‹i < n› ‹ll < n›] using ‹i ≠ i_end - iter› ‹ll < k› by auto also have "A $$ (i,ll) = 0" proof (rule ccontr) assume nz: "A $$ (i,ll) ≠ 0" from i eqs il have neq: "Suc i ≠ ll" by auto from jb[OF ‹i < n› ‹ll < n› ‹ll < k›] nz neq have "i = ll" by auto with i have "ii = Suc ll" by simp hence "i_end - iter = Suc l - iter" using eqs by auto from block[OF this] have "i_begin = i_end" by auto with large ib lb index have "i = ii" by auto with * show False by auto qed finally have C: "?C $$ (i,j) = quot" unfolding C using * Bi by auto show ?thesis unfolding C D .. next case True with eqs have "¬ ((i, j) = (i_end - Suc iter, l - iter) ∧ iter ≠ ?idiff)" and not: "¬ (i = ii - 1 ∧ j = ll ∧ iter ≠ ?idiff)" by auto from this(1) have D: "?D $$ (i,j) = ?Aij" unfolding D using jk index by auto { fix i assume "i < n" with index have id: "((i,i) = (i_end,k)) = False" "(i_begin + Suc diff ≤ i ∧ i ≤ i_end ∧ k < i) = False" by auto { assume *: "(i, i) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff}" hence "i_end - iter = Suc l - iter" by auto from block[OF this] * index large eqs have False by auto } hence "B $$ (i,i) = ?ev i" unfolding BB[OF ‹i < n› ‹i < n›] id if_False by auto } note Bdiag = this from eqs have ii: "ii = i_end - iter" "Suc l - iter = Suc ll" by auto have B: "B $$ (i,j) = (if (i, j) = (ii, Suc ll) ∧ iter ≠ 0 then quot else A $$ (i, j))" unfolding B using ii jk iter by auto have ll_i: "ll ≠ i_end - iter" using ‹ii ≠ ll› eqs by auto have "B $$ (ll,ii) = A $$ (ll,ii)" unfolding BB[OF ‹ll < n› ‹ii < n›] using ‹ii < k› ll_i by auto also have "… = 0" proof (rule ccontr) assume nz: "A $$ (ll,ii) ≠ 0" with jb[OF ‹ll < n› ‹ii < n› ‹ii < k›] ‹ii ≠ ll› have "Suc ll = ii" by auto with eqs have "i_end - iter = Suc l - iter" by auto from block[OF this] index eqs have "iter = 0" by auto with ii have "ll = l" "ii = i_end" by auto with Alie nz show False by auto qed finally have Bli: "B $$ (ll,ii) = 0" . have C: "?C $$ (i,j) = ?Aij" proof (cases "i = j") case True show ?thesis unfolding C unfolding Bdiag[OF ‹j < n›] True using ‹ii ≠ ll› Bli by auto next case False from lb eqs index large have "lb ≤ ll" "ll ≤ l" by auto note C = C[unfolded Bdiag[OF ‹i < n›] Bdiag[OF ‹j < n›]] show ?thesis proof (cases "(i, j) = (ii, Suc ll) ∧ iter ≠ 0") case True hence *: "i = ii" "j = Suc ll" "iter ≠ 0" by auto from * eqs index have "ll < l" "Suc ll < k" "Suc ll < n" by auto have B: "B $$ (i,j) = quot" unfolding B using * by auto have "¬ ((ll, j) = (i_end - iter, Suc l - iter) ∧ iter ∉ {0, Suc ?idiff})" using * index eqs by auto hence B': "B $$ (ll, j) = A $$ (ll, j)" unfolding BB[OF ‹ll < n› ‹j < n›] using jk by auto have "?C $$ (i,j) = quot - quot * A $$ (ll, Suc ll)" unfolding C B using * B' by auto with iblock(3)[OF lbl ‹lb ≤ ll› ‹ll < l›] have C: "?C $$ (i,j) = 0" by simp { assume "A $$ (ii, Suc ll) ≠ 0" with jb[OF ‹ii < n› ‹Suc ll < n› ‹Suc ll < k›] ‹ii ≠ ll› have "ii = Suc ll" by auto with eqs have "i_end - iter = Suc l - iter" by auto from block[OF this] ‹iter ≠ 0› ‹iter ≠ Suc ?idiff› eqs large have False by auto } hence "A $$ (ii,Suc ll) = 0" by auto thus ?thesis unfolding C unfolding * by simp next case False hence B: "B $$ (i,j) = ?Aij" unfolding B by auto from eqs index have "lb ≤ ll" "ll ≤ l" by auto note index = index this ll_i from evb[of ll k] index have evl: "?ev ll = ?ev k" by auto from evb[of i k] index have evi: "?ev i = ?ev k" by auto from not have not: "i ≠ ii - 1 ∨ j ≠ ll ∨ iter = ?idiff" by auto from False have not2: "i ≠ ii ∨ j ≠ Suc ll ∨ iter = 0" by auto show ?thesis proof (cases "i = ii") case True let ?diff = "if j = ll then 0 else - quot * A $$ (ll, j)" have Bli: "B $$ (ll, i) = 0" using True Bli by simp have Blj: "B $$ (ll, j) = A $$ (ll,j)" unfolding BB[OF ‹ll < n› ‹j < n›] using index jk by auto from True have C: "?C $$ (i,j) = ?Aij + ?diff" unfolding C B evi using Bli Blj evl by auto also have "?diff = 0" proof (rule ccontr) assume "?diff ≠ 0" hence jl: "j ≠ ll" and Alj: "A $$ (ll,j) ≠ 0" by (auto split: if_splits) with jb[OF ‹ll < n› ‹j < n› jk] have "j = Suc ll" "?ev ll = ?ev j" by auto with not2 True have "iter = 0" by auto with eqs index jk have id: "A $$ (ll, j) = A $$ (l, Suc l)" and "j = Suc l" "Suc l < k" "ll = l" unfolding ‹j = Suc ll› by auto from iblock[OF lbl] ‹Suc l < k› have "A $$ (l, Suc l) ≠ 1" by auto from jb[OF ‹l < n› ‹j < n› jk] Alj this show False unfolding ‹j = Suc l› ‹ll = l› by auto qed finally show ?thesis by simp next case False let ?diff = "if j = ll then quot * B $$ (i, ii) else 0" from False have C: "?C $$ (i,j) = ?Aij + ?diff" unfolding C B by auto also have "?diff = 0" proof (rule ccontr) assume "?diff ≠ 0" hence j: "j = ll" and Bi: "B $$ (i, ii) ≠ 0" by (auto split: if_splits) from eqs have ii: "i_end - iter = ii" by auto have Bii: "B $$ (i,ii) = A $$ (i, ii)" unfolding BB[OF ‹i < n› ‹ii < n›] using ‹ii < k› iter ii False by auto from Bi Bii have Ai: "A $$ (i,ii) ≠ 0" by auto from jb[OF ‹i < n› ‹ii < n› ‹ii < k›] False Ai have ii: "ii = Suc i" and Ai: "A $$ (i,ii) = 1" by auto from not ii j have iter: "iter = ?idiff" by auto with eqs index have "ii = i_begin" by auto with ii ‹i ≥ i_begin› show False by auto qed finally show ?thesis by simp qed qed qed show ?thesis unfolding D C .. qed qed qed qed qed auto also have "step_3_c_inner_loop quot (ll - 1) (ii - 1) diff … = ?R" by (rule Suc(1), insert prems large, auto) finally show ?case . qed } note main = this[of "Suc ?idiff" i_end 0 l] from ib have suc: "Suc i_end - i_begin = Suc ?idiff" by simp have "step_3_c_inner_loop (A $$ (i_end, k) / A $$ (l, k)) l i_end (Suc ?idiff) A = step_3_c_inner_loop quot l i_end (Suc ?idiff) (?mat 0 (Suc ?idiff))" unfolding mend unfolding quot_def .. also have "… = ?R" by (rule main, auto) finally show ?thesis unfolding suc . qed private lemma step_3_c_inv: "A ∈ carrier_mat n n ⟹ k < n ⟹ (lb,l) ∈ set (identify_blocks A k) ⟹ inv_upto jb A k ⟹ inv_from uppert A k ⟹ inv_at one_zero A k ⟹ ev_block n A ⟹ set bs ⊆ set (identify_blocks A k) ⟹ (⋀ be. be ∉ snd ` set bs ⟹ be ∉ {l,k} ⟹ be < n ⟹ A $$ (be,k) = 0) ⟹ (⋀ bb be. (bb,be) ∈ set bs ⟹ be - bb ≤ l - lb) ― ‹largest block› ⟹ x = A $$ (l,k) ⟹ x ≠ 0 ⟹ inv_all uppert (step_3_c x l k bs A) ∧ same_diag A (step_3_c x l k bs A) ∧ same_upto k A (step_3_c x l k bs A) ∧ inv_at (single_non_zero l k x) (step_3_c x l k bs A) k" proof (induct bs arbitrary: A) case (Nil A) note inv = Nil(4-7) from inv_from_upto_at_all_ev_block[OF inv(1-4) _ ‹k < n›] have "inv_all uppert A" unfolding one_zero_def diff_ev_def uppert_def by auto moreover have "inv_at (single_non_zero l k x) A k" unfolding single_non_zero_def inv_at_def by (intro allI impI conjI, insert Nil, auto) ultimately show ?case by auto next case (Cons p bs A) obtain i_begin i_end where p: "p = (i_begin, i_end)" by force note Cons = Cons[unfolded p] note IH = Cons(1) note A = Cons(2) note kn = Cons(3) note lbl = Cons(4) note inv = Cons(5-8) note blocks = Cons(9-11) note x = Cons(12-13) from identify_blocks[OF lbl] kn have lk: "l < k" and ln: "l < n" and "lb ≤ l" by auto define B where "B = step_3_c_inner_loop (A $$ (i_end,k) / x) l i_end (Suc i_end - i_begin) A" show ?case proof (cases "i_end = l") case True hence id: "step_3_c x l k (p # bs) A = step_3_c x l k bs A" unfolding p by simp show ?thesis unfolding id by (rule IH[OF A kn lbl inv _ blocks(2-3) x], insert blocks(1), auto simp: p True) next case False note il = this hence id: "step_3_c x l k (p # bs) A = step_3_c x l k bs B" unfolding B_def p by simp from blocks[unfolded p] have ib_block: "(i_begin,i_end) ∈ set (identify_blocks A k)" and large: "i_end - i_begin ≤ l - lb" by auto from identify_blocks[OF this(1)] have ibe: "i_begin ≤ i_end" "i_end < k" by auto have B: "B = mat n n (λ (i,j). if (i,j) = (i_end,k) then 0 else if i_begin ≤ i ∧ i ≤ i_end ∧ j > k then A $$ (i,j) - A $$ (i_end,k) / x * A $$ (l + i - i_end,j) else A $$ (i,j))" unfolding B_def x by (rule step_3_c_inner_result[OF inv kn A lbl ib_block il large], insert x, auto) have Bn: "B ∈ carrier_mat n n" unfolding B by auto have sdAB: "same_diag A B" unfolding B same_diag_def using ibe by auto have suAB: "same_upto k A B" using A kn unfolding B same_upto_def by auto have inv_ev: "ev_block n B" using same_diag_ev_block[OF sdAB inv(4)] . have inv_jb: "inv_upto jb B k" using same_upto_inv_upto_jb[OF suAB inv(1)] . have ib: "identify_blocks A k = identify_blocks B k" using identify_blocks_cong[OF kn sdAB suAB] . have inv_ut: "inv_from uppert B k" using inv(2) ibe unfolding B inv_from_def uppert_def by auto from x il ibe kn lk have xB: "x = B $$ (l,k)" by (auto simp: B) { fix be assume *: "be ∉ snd ` set bs" "be ∉ {l, k}" "be < n" hence "B $$ (be, k) = 0" using kn blocks(2)[of be] unfolding B by (cases "be = i_end", auto) } note blocksB = this have bs: "set bs ⊆ set (identify_blocks A k)" using blocks(1) by auto have inv_oz: "inv_at one_zero B k" using inv(3) ibe kn unfolding B inv_at_def one_zero_def by simp show ?thesis unfolding id using IH[OF Bn kn, folded ib, OF lbl inv_jb inv_ut inv_oz inv_ev bs blocksB blocks(3) xB x(2)] using same_diag_trans[OF sdAB] same_upto_trans[OF suAB] by auto qed qed lemma step_3_main_inv: "A ∈ carrier_mat n n ⟹ k > 0 ⟹ inv_all uppert A ⟹ ev_block n A ⟹ inv_upto jb A k ⟹ inv_all jb (step_3_main n k A) ∧ same_diag A (step_3_main n k A)" proof (induct k A taking: n rule: step_3_main.induct) case (1 k A) from 1(2-) have A: "A ∈ carrier_mat n n" and k: "k > 0" and inv: "inv_all uppert A" "ev_block n A" "inv_upto jb A k" by auto note [simp] = step_3_main.simps[of n k A] show ?case proof (cases "k ≥ n") case True thus ?thesis using inv_uptoD[OF inv(3)] by (intro conjI inv_allI, auto) next case False hence kn: "k < n" by simp obtain B where B: "B = step_3_a (k - 1) k A" by auto note IH = 1(1)[OF False B] from A have Bn: "B ∈ carrier_mat n n" unfolding B carrier_mat_def by simp from k have "k - 1 < k" by simp { fix i assume "i < k" with ev_blockD[OF inv(2) _ ‹k < n›, of i] ‹k < n› have "A $$ (i,i) = A $$ (k,k)" by auto } hence "inv_from_bot (λA i. one_zero A i k) A (k - 1)" using inv_all_uppertD[OF inv(1), of k] unfolding inv_from_bot_def one_zero_def by auto from step_3_a_inv[OF A ‹k - 1 < k› ‹k < n› inv(3) inv_all_imp_inv_from[OF inv(1)] this inv(2)] same_diag_ev_block[OF _ inv(2)] have inv: "inv_from uppert B k" "ev_block n B" "inv_upto jb B k" "inv_at one_zero B k" and sd: "same_diag A B" unfolding B by auto note evb = ev_blockD[OF inv(2)] obtain all_blocks where ab: "all_blocks = identify_blocks B k" by simp obtain blocks where blocks: "blocks = filter (λ block. B $$ (snd block, k) ≠ 0) all_blocks" by simp obtain F where F: "F = (if blocks = [] then B else let (l_begin,l) = find_largest_block (hd blocks) (tl blocks); x = B $$ (l, k); C = step_3_c x l k blocks B; D = mult_col_div_row (inverse x) k C; E = swap_cols_rows_block (Suc l) k D in E)" by simp note IH = IH[OF ab blocks F] have Fn: "F ∈ carrier_mat n n" unfolding F Let_def carrier_mat_def using Bn by (simp split: prod.splits) have inv: "inv_all uppert F ∧ same_diag A F ∧ inv_upto jb F (Suc k)" proof (cases "blocks = []") case True hence F: "F = B" unfolding F by simp have lo: "inv_at (lower_one k) B k" proof fix i assume i: "i < n" note lower_one_def[simp] show "lower_one k B i k" proof (cases "B $$ (i,k) = 0") case False note nz = this note oz = inv_atD[OF inv(4) i, unfolded one_zero_def] from nz oz have "i ≤ k" by auto show ?thesis proof (cases "i = k") case False with ‹i ≤ k› have "i < k" by auto with nz oz have ev: "B $$ (i,i) = B $$ (k,k)" unfolding diff_ev_def by auto have "(identify_block B i, i) ∈ set all_blocks" unfolding ab proof (rule identify_blocks_rev[OF _ ‹k < n›]) show "B $$ (i, Suc i) = 0 ∧ Suc i < k ∨ Suc i = k" proof (cases "Suc i = k") case False with ‹i < k› ‹k < n› have "Suc i < k" "Suc i < n" by simp_all with nz oz have "B $$ (i, Suc i) ≠ 1" by simp with inv_uptoD[OF inv(3) ‹i < n› ‹Suc i < n› ‹Suc i < k›, unfolded jb_def] have "B $$ (i, Suc i) = 0" by simp thus ?thesis using ‹Suc i < k› by simp qed simp qed with arg_cong[OF ‹blocks = []›[unfolded blocks], of set] have "B $$ (i,k) = 0" by auto with nz show ?thesis by auto qed auto qed auto qed have inv_jb: "inv_upto jb B (Suc k)" proof (rule inv_upto_Suc[OF inv(3)]) fix i assume "i < n" from inv_atD[OF lo ‹i < n›, unfolded lower_one_def] show "jb B i k" unfolding jb_def by auto qed from inv_from_upto_at_all_ev_block[OF inv(3,1) lo inv(2) _ ‹k < n›] lower_one_diff_uppert have "inv_all uppert B" by auto with inv inv_jb sd show ?thesis unfolding F by simp next case False obtain l_start l where l: "find_largest_block (hd blocks) (tl blocks) = (l_start, l)" by force obtain x where x: "x = B $$ (l,k)" by simp obtain C where C: "C = step_3_c x l k blocks B" by simp obtain D where D: "D = mult_col_div_row (inverse x) k C" by auto obtain E where E: "E = swap_cols_rows_block (Suc l) k D" by auto from find_largest_block[OF False l] have lb: "(l_start,l) ∈ set blocks" and llarge: "⋀ i_begin i_end. (i_begin,i_end) ∈ set blocks ⟹ l - l_start ≥ i_end - i_begin" by auto from lb have x0: "x ≠ 0" unfolding blocks x by simp { fix i_start i_end assume "(i_start,i_end) ∈ set blocks" hence "(i_start,i_end) ∈ set (identify_blocks B k)" unfolding blocks ab by simp with identify_blocks[OF this] have "i_end < k" "(i_start,i_end) ∈ set (identify_blocks B k)" by auto } note block_bound = this from block_bound[OF lb] have lk: "l < k" and lblock: "(l_start, l) ∈ set (identify_blocks B k)" by auto from lk ‹k < n› have ln: "l < n" by simp from evb[OF ‹l < n› ‹k < n›] have Bll: "B $$ (l,l) = B $$ (k,k)" . from False have F: "F = E" unfolding E D C x F l Let_def by simp from Bn have Cn: "C ∈ carrier_mat n n" unfolding C carrier_mat_def by simp { fix be assume nmem: "be ∉ snd ` set blocks" and belk: "be ∉ {l, k}" and be: "be < n" have "B $$ (be, k) = 0" proof (rule ccontr) assume nz: "¬ ?thesis" note oz = inv_atD[OF inv(4) be, unfolded one_zero_def] from belk oz be nz have "be < k" by auto obtain bb where ib: "identify_block B be = bb" by force note ib_inv = identify_block[OF ib] have "B $$ (be, Suc be) = 0 ∧ Suc be < k ∨ Suc be = k" proof (cases "Suc be = k") case False with ‹be < k› have sbek: "Suc be < k" by auto from inv_uptoD[OF inv(3) ‹be < n› _ sbek] sbek kn have "jb B be (Suc be)" by auto from this[unfolded jb_def] have 01: "B $$ (be, Suc be) ∈ {0,1}" by auto from 01 oz sbek nz have "B $$ (be, Suc be) = 0" by auto with sbek show ?thesis by auto qed auto from identify_blocks_rev[OF this kn] nz nmem show False unfolding ab blocks by force qed } note inv3 = step_3_c_inv[OF Bn ‹k < n› lblock inv(3,1,4,2) _ this llarge x x0, of blocks, folded C, unfolded ab blocks] from inv3 have sdC: "same_diag B C" and suC: "same_upto k B C" by auto note sd = same_diag_trans[OF sd sdC] from Bll sdC ln ‹k < n› have Cll: "C $$ (l,l) = C $$ (k,k)" unfolding same_diag_def by auto from same_diag_ev_block[OF sdC inv(2)] same_upto_inv_upto_jb[OF suC inv(3)] inv3 have inv: "inv_all uppert C" "ev_block n C" "inv_upto jb C k" "inv_at (single_non_zero l k x) C k" by auto from x0 have "inverse x ≠ 0" by simp from Cn have Dn: "D ∈ carrier_mat n n" unfolding D carrier_mat_def by simp { fix i j assume i: "i < n" and j: "j < n" with Cn have dC: "i < dim_row C" "i < dim_col C" "j < dim_row C" "j < dim_col C" by auto let ?c = "C $$ (i,j)" let ?x = "inverse x" have "D $$ (i,j) = (if i = l ∧ j = k then 1 else if i = k ∧ j ≠ k then x * ?c else ?c)" unfolding D proof (subst mult_col_div_index_row[OF dC ‹inverse x ≠ 0›], unfold inverse_inverse_eq) note at = inv_atD[OF inv(4) ‹i < n›, unfolded single_non_zero_def] show "(if i = k ∧ j ≠ i then x * ?c else if j = k ∧ j ≠ i then ?x * ?c else ?c) = (if i = l ∧ j = k then 1 else if i = k ∧ j ≠ k then x * ?c else ?c)" (is "?l = ?r") proof (cases "(i,j) = (l,k)") case True with lk have "?l = ?x * ?c" by auto also have "… = 1" using at True ‹inverse x ≠ 0› by auto finally show ?thesis using True by simp next case False note neq = this have "?l = (if i = k ∧ j ≠ k then x * ?c else ?c)" proof (cases "i = k ∧ j ≠ k ∨ j = k ∧ i ≠ k") case True thus ?thesis proof assume *: "i = k ∧ j ≠ k" hence l: "?l = x * ?c" by simp show ?thesis using * neq unfolding l by simp next assume *: "j = k ∧ i ≠ k" hence "?l = ?x * ?c" using lk by auto from * neq have "i ≠ l" and **: "¬ (i = k ∧ j ≠ k)" by auto from at ‹i ≠ l› * have "?c = 0" by auto with ‹?l = ?x * ?c› ** show ?thesis by auto qed qed auto also have "… = ?r" using False by auto finally show ?thesis . qed qed } note D = this have sD[simp]: "⋀ i. i < n ⟹ D $$ (i,i) = C $$ (i,i)" using lk by (auto simp: D) from ‹C $$ (l,l) = C $$ (k,k)› ‹l < n› ‹k < n› have Dll: "D $$ (l,l) = D $$ (k,k)" by simp have sdD: "same_diag C D" unfolding same_diag_def by simp note sd = same_diag_trans[OF sd sdD] from same_diag_ev_block[OF sdD inv(2)] have invD: "ev_block n D" . note inv = inv_uptoD[OF inv(3), unfolded jb_def] inv_all_uppertD[OF inv(1)] inv_atD[OF inv(4), unfolded single_non_zero_def] moreover have "inv_all uppert D" by (intro inv_allI, insert inv(2) lk, auto simp: uppert_def D) moreover have suD: "same_upto k C D" proof fix i j assume i: "i < n" and j: "j < k" with kn have jn: "j < n" by simp show "C $$ (i, j) = D $$ (i, j)" unfolding D[OF i jn] using j k inv(1)[OF i jn j] i j by auto qed from same_upto_inv_upto_jb[OF suD ‹inv_upto jb C k›] have "inv_upto jb D k" . moreover let ?single_one = "single_one l k" have "inv_at ?single_one D k" by (intro inv_atI, insert inv(3) D[OF _ ‹k < n›] ln, auto simp: single_one_def) ultimately have inv: "inv_all uppert D" "ev_block n D" "inv_upto jb D k" "inv_at ?single_one D k" using invD by blast+ note inv = inv_uptoD[OF inv(3), unfolded jb_def] inv_all_uppertD[OF inv(1)] inv_atD[OF inv(4), unfolded single_one_def] ev_blockD[OF inv(2)] from suC suD have suD: "same_upto k B D" unfolding same_upto_def by auto let ?I = "λ j. if j = Suc l then k else if Suc l < j ∧ j ≤ k then j - 1 else j" let ?I' = "λ j. if j = Suc l then k else j - 1" { fix i j assume i: "i < n" and j: "j < n" with Dn lk ‹k < n› have dims: "i < dim_row D" "i < dim_col D" "j < dim_row D" "j < dim_col D" "Suc l ≤ k" "k < dim_row D" "k < dim_col D" by auto have "E $$ (i,j) = D $$ (?I i, ?I j)" unfolding E by (rule subst swap_cols_rows_block_index[OF dims]) } note E = this { fix i assume i: "i < n" from ‹l < k› have "l ≤ Suc l" "Suc l ≤ k" by auto have "E $$ (i,i) = D $$ (i,i)" unfolding E[OF i i] by (rule inv(4), insert i ‹k < n›, auto) } note Ed = this from Ed have ed: "same_diag D E" unfolding same_diag_def by auto note sd = same_diag_trans[OF sd ed] have "ev_block n E" using same_diag_ev_block[OF ed ‹ev_block n D›] by auto moreover have Eut: "inv_all uppert E" proof (intro inv_allI, unfold uppert_def, intro impI) fix i j assume i: "i < n" and j: "j < n" and ji: "j < i" have "?I i < n" using i ‹k < n› by auto show "E $$ (i,j) = 0" proof (cases "?I j < ?I i") case True from inv(2)[OF this ‹?I i < n›] show ?thesis unfolding E[OF i j] . next case False have "?I i ≠ ?I j" using ji lk by (auto split: if_splits) with False have ij: "?I i < ?I j" by simp from ij ji have jl: "j = Suc l" using lk by (auto split: if_splits) with ji ij have il: "i > Suc l" "i ≤ k" by (auto split: if_splits) from jl il have Eij: "E $$ (i,j) = D $$ (i-1,k)" unfolding E[OF i j] by simp have "i - 1 < n" "i - 1 ∉ {k, l}" using i il by auto with inv(3)[of "i-1"] have D: "D $$ (i-1,k) = 0" by auto show ?thesis unfolding Eij D by simp qed qed moreover from same_diag_trans[OF ‹same_diag B C› ‹same_diag C D›] have "same_diag B D" . from identify_blocks_cong[OF ‹k < n› this suD] have idb: "identify_blocks B k = identify_blocks D k" . have "inv_upto jb E (Suc k)" proof (intro inv_uptoI) fix i j assume i: "i < n" and j: "j < n" and "j < Suc k" hence jk: "j ≤ k" by simp show "jb E i j" proof (cases "E $$ (i,j) = 0 ∨ j = i") case True thus ?thesis unfolding jb_def by auto next case False note enz = this from inv(4)[OF i j] have same_ev: "D $$ (i,i) = D $$ (j,j)" . note inv2 = inv_all_uppertD[OF Eut _ i, of j] from False inv2 have "¬ j < i" by auto with False have ji: "j > i" by auto have "E $$ (i,j) ∈ {0,1} ∧ (j ≠ Suc i ⟶ E $$ (i,j) = 0)" proof (cases "j ≤ l") case True note jl = this with ji lk have il: "i ≤ l" and jk: "j < k" by auto have id: "E $$ (i,j) = D $$ (i,j)" unfolding E[OF i j] using jl il by simp from inv(1)[OF i j jk] ji show ?thesis unfolding id by auto next case False note jl = this show ?thesis proof (cases "j = Suc l") case True note jl = this with ji lk have il: "i ≤ l" "i ≠ k" by auto have id: "E $$ (i,j) = D $$ (i,k)" unfolding E[OF i j] using jl il by auto from inv(3)[OF i] jl il show ?thesis unfolding id by (cases "i = l", auto) next case False with jl jk kn have jl: "j > Suc l" and jk: "j - 1 < k" and jn: "j - 1 < n" by auto with jk have id: "?I j = j - 1" by auto note jb = inv(1)[OF _ jn jk] show ?thesis proof (cases "i < Suc l") case True note il = this with id have id: "E $$ (i,j) = D $$ (i,j - 1)" unfolding E[OF i j] by auto show ?thesis proof (cases "i = j - 2") case False thus ?thesis unfolding id using jb[OF i] il jl by auto next case True with il jl have *: "j = Suc (Suc l)" "i = l" by auto with id have id: "E $$ (i,j) = D $$ (l,Suc l)" by auto from * jl jk have neq: "Suc l ≠ k" by auto from lblock[unfolded idb] have "(l_start, l) ∈ set (identify_blocks D k)" . from this[unfolded identify_blocks_iff[OF kn]] neq have "D $$ (l, Suc l) ≠ 1" by auto with jb[OF i] il jl ji * have "D $$ (l, Suc l) = 0" by auto thus ?thesis unfolding id by simp qed next case False note il = this show ?thesis proof (cases "i = Suc l") case True with id have id: "E $$ (i,j) = D $$ (k,j - 1)" unfolding E[OF i j] by auto from inv(2)[OF jk kn] show ?thesis unfolding id by simp next case False with il jl ji jk kn have il: "i > Suc l" and ik: "i < k" and i_n: "i - 1 < n" by auto with id have id: "E $$ (i,j) = D $$ (i - 1, j - 1)" unfolding E[OF i j] by auto show ?thesis unfolding id using jb[OF i_n] il jl ji by auto qed qed qed qed thus "jb E i j" unfolding jb_def Ed[OF i] Ed[OF j] same_ev by auto qed qed ultimately show ?thesis using sd unfolding F by simp qed hence inv: "inv_all uppert F" "ev_block n F" "inv_upto jb F (Suc k)" and sd: "same_diag A F" using same_diag_ev_block[OF _ ‹ev_block n A›] by auto have "0 < Suc k" by simp note IH = IH[OF Fn this inv(1-3)] have id: "step_3_main n k A = step_3_main n (Suc k) F" using kn by (simp add: F Let_def blocks ab B) from same_diag_trans[OF sd] IH show ?thesis unfolding id by auto qed qed lemma step_1_2_inv: assumes A: "A ∈ carrier_mat n n" and upper_t: "upper_triangular A" and Bid: "B = step_2 (step_1 A)" shows "inv_all uppert B" "inv_all diff_ev B" "ev_blocks B" proof - from A have d: "dim_row A = n" by simp let ?B = "step_2 (step_1 A)" from upper_triangularD[OF upper_t] have inv: "inv_all uppert A" unfolding inv_all_def uppert_def using A by auto from upper_t have inv2: "inv_part diff_ev A 0 0" unfolding inv_part_def diff_ev_def by auto have inv3: "ev_blocks_part 0 (step_1 A)" by (rule ev_blocks_partI, auto) have A1: "step_1 A ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto from A1 have d1: "dim_row (step_1 A) = n" unfolding carrier_mat_def by simp have B: "?B ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto from B have d2: "dim_row ?B = n" unfolding carrier_mat_def by simp have "inv_all uppert (step_1 A) ∧ inv_all diff_ev (step_1 A)" unfolding step_1_def d by (rule step_1_main_inv[OF _ A inv inv2], simp) hence "inv_all uppert (step_1 A)" and "inv_all diff_ev (step_1 A)" by auto from step_2_main_inv[OF A1 this inv3] show "inv_all uppert B" "inv_all diff_ev B" "ev_blocks B" unfolding step_2_def d d1 Bid by auto qed definition inv_all' :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ bool" where "inv_all' p A ≡ ∀ i j. i < dim_row A ⟶ j < dim_row A ⟶ p A i j" private lemma lookup_other_ev_None: assumes "lookup_other_ev ev k A = None" and "i < k" shows "A $$ (i,i) = ev" using assms by (induct ev k A rule: lookup_other_ev.induct, auto split: if_splits) (insert less_antisym, blast) private lemma lookup_other_ev_Some: assumes "lookup_other_ev ev k A = Some i" shows "i < k ∧ A $$ (i,i) ≠ ev ∧ (∀ j. i < j ∧ j < k ⟶ A $$ (j,j) = ev)" using assms by (induct ev k A rule: lookup_other_ev.induct, auto split: if_splits) (insert less_SucE, blast) lemma partition_jb: assumes A: "(A :: 'a mat) ∈ carrier_mat n n" and inv: "inv_all uppert A" "inv_all diff_ev A" "ev_blocks A" and part: "partition_ev_blocks A [] = bs" shows "A = diag_block_mat bs" "⋀ B. B ∈ set bs ⟹ inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B" proof - have diag: "diag_block_mat [A] = A" using A by auto { fix cs assume *: "⋀ C. C ∈ set cs ⟹ dim_row C = dim_col C ∧ inv_all' uppert C ∧ ev_block (dim_col C) C" "partition_ev_blocks A cs = bs" from inv have inv: "inv_all' uppert A" "inv_all' diff_ev A" "ev_blocks_part n A" unfolding inv_all_def inv_all'_def ev_blocks_def using A by auto hence "diag_block_mat (A # cs) = diag_block_mat bs ∧ (∀ B ∈ set bs. inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B)" using A * proof (induct n arbitrary: A cs bs rule: less_induct) case (less n A cs bs) from less(5) have A: "A ∈ carrier_mat n n" by auto hence dim: "dim_row A = n" "dim_col A = n" by auto let ?dim = "sum_list (map dim_col cs)" let ?C = "diag_block_mat cs" define C where "C = ?C" from less(6) have cs: "⋀ C. C ∈ set cs ⟹ inv_all' uppert C ∧ ev_block (dim_col C) C ∧ dim_row C = dim_col C" by auto hence dimcs[simp]: "sum_list (map dim_row cs) = ?dim" by (induct cs, auto) from dim_diag_block_mat[of cs, unfolded dimcs] obtain nc where C: "?C ∈ carrier_mat nc nc" unfolding carrier_mat_def by auto hence dimC: "dim_row C = nc" "dim_col C = nc" unfolding C_def by auto note bs = less(7)[unfolded partition_ev_blocks.simps[of A cs] Let_def dim, symmetric] show ?case proof (cases "n = 0") case True hence bs: "bs = cs" unfolding bs by simp thus ?thesis using cs A by (auto simp: Let_def True) next case False let ?n1 = "n - 1" let ?look = "lookup_other_ev (A $$ (?n1, ?n1)) ?n1 A" show ?thesis proof (cases ?look) case None from False None have bs: "bs = A # cs" unfolding bs by auto have ut: "inv_all' uppert A" using less(2) by auto from lookup_other_ev_None[OF None] have "⋀ i. i < n ⟹ A $$ (i,i) = A $$ (?n1, ?n1)" by (case_tac "i = ?n1", auto) hence evb: "ev_block n A" unfolding ev_block_def dim by metis from cs A ut evb show ?thesis unfolding bs by auto next case (Some i) let ?si = "Suc i" from lookup_other_ev_Some[OF Some] have i: "i < ?n1" and neq: "A $$ (i,i) ≠ A $$ (?n1, ?n1)" and between: "⋀j. i < j ⟹ j < ?n1 ⟹ A $$ (j,j) = A $$ (?n1, ?n1)" by auto define m where "m = n - ?si" from i False have si: "?si < n" by auto from False i have nsi: "n = ?si + m" unfolding m_def by auto obtain UL UR LL LR where split: "split_block A ?si ?si = (UL, UR, LL, LR)" by (rule prod_cases4) from split_block[OF split dim[unfolded nsi]] have carr: "UL ∈ carrier_mat ?si ?si" "UR ∈ carrier_mat ?si m" "LL ∈ carrier_mat m ?si" "LR ∈ carrier_mat m m" and Ablock: "A = four_block_mat UL UR LL LR" by auto hence dimLR: "dim_row LR = m" "dim_col LR = m" and dimUL: "dim_col UL = ?si" "dim_row UL = ?si" by auto from less(3)[unfolded inv_all'_def diff_ev_def] dim have diff: "⋀ i j. i < n ⟹ j < n ⟹ i < j ⟹ A $$ (i, i) ≠ A $$ (j, j) ⟹ A $$ (i, j) = 0" by auto from less(2)[unfolded inv_all'_def uppert_def] dim have ut: "⋀ i j. i < n ⟹ j < n ⟹ j < i ⟹ A $$ (i, j) = 0" by auto let ?UR = "0⇩_{m}?si m" have UR: "UR = ?UR" proof (rule eq_matI) fix ia j assume ij: "ia < dim_row (0⇩_{m}(Suc i) m)" "j < dim_col (0⇩_{m}(Suc i) m)" let ?j = "?si + j" have "UL $$ (ia,ia) = A $$ (ia,ia)" using ij carr unfolding Ablock by auto also have "… ≠ A $$ (?j, ?j)" proof assume eq: "A $$ (ia,ia) = A $$ (?j, ?j)" from ij have rel: "ia ≤ i" "i ≤ ?j" "?j < n" using nsi i by auto from ev_blocks_part_leD[OF less(4) this eq[symmetric]] eq have eq: "A $$ (i,i) = A $$ (?j,?j)" by auto also have "… = A $$ (?n1, ?n1)" using between[of ?j] rel by (cases "?j = ?n1", auto) finally show False using neq by auto qed also have "A $$ (?si + j, ?si + j) = LR $$ (j,j)" using ij carr unfolding Ablock by auto finally show "UR $$ (ia, j) = 0⇩_{m}(Suc i) m $$ (ia, j)" using diff[of ia "?si + j", unfolded Ablock] ij nsi carr by auto qed (insert carr, auto) let ?LL = "0⇩_{m}m ?si" have LL: "LL = ?LL" proof (rule eq_matI) fix ia j show "ia < dim_row (0⇩_{m}m (Suc i)) ⟹ j < dim_col (0⇩_{m}m (Suc i)) ⟹ LL $$ (ia, j) = 0⇩_{m}m (Suc i) $$ (ia, j)" using ut[of "?si + ia" j, unfolded Ablock] nsi carr by auto qed (insert carr, auto) have utUL: "inv_all' uppert UL"unfolding inv_all'_def uppert_def proof (intro allI impI) fix i j show "i < dim_row UL ⟹ j < dim_row UL ⟹ j < i ⟹ UL $$ (i, j) = 0" using ut[of i j, unfolded Ablock] using nsi carr by auto qed have diffUL: "inv_all' diff_ev UL"unfolding inv_all'_def diff_ev_def proof (intro allI impI) fix i j show "i < dim_row UL ⟹ j < dim_row UL ⟹ i < j ⟹ UL $$ (i, i) ≠ UL $$ (j, j) ⟹ UL $$ (i, j) = 0" using diff[of i j, unfolded Ablock] using nsi carr by auto qed have evbUL: "ev_blocks_part ?si UL"unfolding ev_blocks_part_def proof (intro allI impI) fix ia j k show "ia < j ⟹ j < k ⟹ k < Suc i ⟹ UL $$ (k, k) = UL $$ (ia, ia) ⟹ UL $$ (j, j) = UL $$ (ia, ia)" using less(4)[unfolded Ablock ev_blocks_part_def, rule_format, of ia j k] using nsi carr by auto qed have utLR: "inv_all' uppert LR" unfolding inv_all'_def uppert_def proof (intro allI impI) fix i j show "i < dim_row LR ⟹ j < dim_row LR ⟹ j < i ⟹ LR $$ (i, j) = 0" using ut[of "?si + i" "?si + j", unfolded Ablock] nsi carr by auto qed have evbLR: "ev_block (dim_row LR) LR" unfolding ev_block_def proof (intro allI impI) fix i j show "i < dim_row LR ⟹ j < dim_row LR ⟹ LR $$ (i, i) = LR $$ (j, j)" using between[of "?si + i"] between[of "?si + j"] carr nsi unfolding Ablock by auto (metis One_nat_def Suc_lessI diff_Suc_1) qed from False Some split have bs: "partition_ev_blocks UL (LR # cs) = bs" unfolding bs by auto have IH: "diag_block_mat (UL # LR # cs) = diag_block_mat bs ∧ (∀B∈set bs. inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B)" by (rule less(1)[OF si utUL diffUL evbUL carr(1) _ bs], insert dimLR evbLR utLR cs, auto) have "diag_block_mat (A # cs) = diag_block_mat (UL # LR # cs)" unfolding diag_block_mat.simps dim C_def[symmetric] dimC dimLR dimUL Let_def index_mat_four_block(2-3) Ablock UR LL using assoc_four_block_mat[of UL LR C] dimC carr by simp with IH show ?thesis by auto qed qed qed } from this[of Nil, OF _ part] show "A = diag_block_mat bs" "⋀ B. B ∈ set bs ⟹ inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B" unfolding diag by fastforce+ qed lemma uppert_to_jb: assumes ut: "inv_all uppert A" and "A ∈ carrier_mat n n" shows "inv_upto jb A 1" proof (rule inv_uptoI) fix i j assume "i < n" "j < n" and "j < 1" hence j: "j = 0" and jn: "0 < n" by auto show "jb A i j" unfolding jb_def j using inv_all_uppertD[OF ut _ ‹i < n›, of 0] by auto qed lemma jnf_vector: assumes A: "A ∈ carrier_mat n n" and jb: "⋀ i j. i < n ⟹ j < n ⟹ jb A i j" and evb: "ev_block n A" shows "jordan_matrix (jnf_vector A) = (A :: 'a mat)" "0 ∉ fst ` set (jnf_vector A)" proof - from A have "dim_row A = n" by simp hence id: "jnf_vector A = jnf_vector_main n A" unfolding jnf_vector_def by auto let ?map = "map (λ(n, a). jordan_block n (a :: 'a))" let ?B = "λ k. diag_block_mat (?map (jnf_vector_main k A))" { fix k assume "k ≤ n" hence "(∀ i j. i < k ⟶ j < k ⟶ ?B k $$ (i,j) = A $$ (i,j)) ∧ diag_block_mat (?map (jnf_vector_main k A)) ∈ carrier_mat k k ∧ 0 ∉ fst ` set (jnf_vector_main k A)" proof (induct k rule: less_induct) case (less sk) show ?case proof (cases sk) case (Suc k) obtain b where ib: "identify_block A k = b" by force let ?ev = "A $$ (b,b)" from ib have id: "jnf_vector_main sk A = jnf_vector_main b A @ [(Suc k - b, ?ev)]" unfolding Suc by simp let ?c = "Suc k - b" define B where "B = ?B b" define C where "C = jordan_block ?c ?ev" have C: "C ∈ carrier_mat ?c ?c" unfolding C_def by auto let ?FB = "λ Bb Cc. four_block_mat Bb (0⇩_{m}(dim_row Bb) (dim_col Cc)) (0⇩_{m}(dim_row Cc) (dim_col Bb)) Cc" from identify_block_le'[OF ib] have bk: "b ≤ k" . with Suc less(2) have "b < sk" "b ≤ n" by auto note IH = less(1)[OF this, folded B_def] have B: "B ∈ carrier_mat b b" using IH by simp from bk Suc have sk: "sk = b + ?c" by auto show ?thesis unfolding id map_append list.simps diag_block_mat_last split B_def[symmetric] C_def[symmetric] Let_def proof (intro allI conjI impI) show "?FB B C ∈ carrier_mat sk sk" unfolding sk using four_block_carrier_mat[OF B C] . fix i j assume i: "i < sk" and j: "j < sk" with jb ‹sk ≤ n› have jb: "jb A i j" by auto have ut: "uppert A i j" by (rule jb_imp_uppert[OF jb]) have de: "diff_ev A i j" by (rule jb_imp_diff_ev[OF jb]) from B C have dim: "dim_row B = b" "dim_col B = b" "dim_col C = ?c" "dim_row C = ?c" by auto from sk B C i j have "i < dim_row B + dim_row C" "j < dim_col B + dim_col C" by auto note id = index_mat_four_block(1)[OF this, unfolded dim] have id: "?FB B C $$ (i,j) = (if i < b then if j < b then B $$ (i, j) else 0 else if j < b then 0 else C $$ (i - b, j - b))" unfolding id dim using i j sk by auto show "?FB B C $$ (i,j) = A $$ (i,j)" proof (cases "i < b ∧ j < b") case True (* upper left *) hence "?FB B C $$ (i,j) = B $$ (i,j)" unfolding id by auto with IH True show ?thesis by auto next case False note not_ul = this note ib = identify_block[OF ib] show ?thesis proof (cases "¬ i < b ∧ j < b ∨ i < b ∧ ¬ j < b") case True (* not on main diagonal *) hence id: "?FB B C $$ (i,j) = 0" unfolding id by auto show ?thesis proof (cases "j < i") case True (* lower left *) with ut show ?thesis unfolding id uppert_def by auto next case False (* upper right *) with True have *: "j ≥ b" "i < b" "j > i" by auto have "A $$ (i,j) = 0" proof (rule ccontr) assume "A $$ (i,j) ≠ 0" with jb[unfolded jb_def] * have ji: "j = b" "i = b - 1" "b > 0" and no_border: "A $$ (i, i) = A $$ (j, j)" "A $$ (i,j) = 1" by auto from no_border[unfolded ji] ib(2) ‹b > 0› show False by auto qed thus ?thesis unfolding id by simp qed next case False (* lower right *) with not_ul have *: "¬ i < b" "¬ j < b" by auto hence id: "?FB B C $$ (i,j) = C $$ (i - b, j - b)" unfolding id by auto from * i j have ijc: "i - b < ?c" "j - b < ?c" unfolding sk by auto have id: "?FB B C $$ (i,j) = (if i - b = j - b then ?ev else if Suc (i - b) = j - b then 1 else 0)" unfolding id unfolding C_def jordan_block_index(1)[OF ijc] .. show ?thesis proof (cases "i - b = j - b") case True hence id: "?FB B C $$ (i,j) = ?ev" unfolding id by simp from True * have ij: "j = i" by auto have i_n: "i < n" using i ‹sk ≤ n› by auto have b_n: "b < n" using ‹b < sk› ‹sk ≤ n› by auto from ib(3)[of i] True * i j Suc ev_blockD[OF evb i_n b_n] have "A $$ (i,j) = ?ev" unfolding ij by auto with id show ?thesis by simp next case False note neq = this show ?thesis proof (cases "j - b = Suc (i - b)") case True hence id: "?FB B C $$ (i,j) = 1" unfolding id by simp from True * have ij: "j = Suc i" by auto from ib(3)[of i] True * i j Suc have "A $$ (i,j) = 1" unfolding ij by auto with id show ?thesis by simp next case False with neq have id: "?FB B C $$ (i,j) = 0" unfolding id by simp from * neq False have "i ≠ j" "Suc i ≠ j" by auto with jb[unfolded jb_def] have "A $$ (i,j) = 0" by auto with id show ?thesis by simp qed qed qed qed qed (insert bk IH, auto) qed auto qed } from this[OF le_refl] A show "jordan_matrix (jnf_vector A) = A" "0 ∉ fst ` set (jnf_vector A)" unfolding id jordan_matrix_def by auto qed end lemma triangular_to_jnf_vector: assumes A: "A ∈ carrier_mat n n" and upper_t: "upper_triangular A" shows "jordan_nf A (triangular_to_jnf_vector A)" proof - from A have d: "dim_row A = n" by simp let ?B = "step_2 (step_1 A)" let ?J = "triangular_to_jnf_vector A" have A1: "step_1 A ∈ carrier_mat n n" using A unfolding carrier_mat_def by simp from similar_mat_trans[OF step_2_similar step_1_similar, OF A1 A] have sim: "similar_mat ?B A" . have A1: "step_1 A ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto from A1 have d1: "dim_row (step_1 A) = n" unfolding carrier_mat_def by simp have B: "?B ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto from B have d2: "dim_row ?B = n" unfolding carrier_mat_def by simp define Cs where "Cs = partition_ev_blocks ?B []" from step_1_2_inv[OF A upper_t refl] have inv: "inv_all n uppert ?B" "inv_all n diff_ev ?B" "ev_blocks n ?B" by auto from partition_jb[OF B inv, of Cs] have BC: "?B = diag_block_mat Cs" and Cs: "⋀ C. C ∈ set Cs ⟹ inv_all' uppert C ∧ ev_block (dim_col C) C ∧ dim_row C = dim_col C" unfolding Cs_def by auto define D where "D = map step_3 Cs" let ?D = "diag_block_mat D" let ?CD = "map (λ C. (C, (jnf_vector o step_3) C)) Cs" { fix C D assume mem: "(C,D) ∈ set ?CD" hence DC: "D = jnf_vector (step_3 C)" and C: "C ∈ set Cs" by auto let ?D = "step_3 C" define n where "n = dim_col C" from Cs[OF C] have C: "inv_all n uppert C" "ev_block n C" "C ∈ carrier_mat n n" unfolding inv_all'_def inv_all_def n_def carrier_mat_def by auto from step_3_similar[OF C(3)] have sim: "similar_mat C ?D" by (rule similar_mat_sym) from similar_matD[OF sim] C have D: "?D ∈ carrier_mat n n" unfolding carrier_mat_def by auto from C(3) have dimC: "dim_row C = n" by auto from step_3_main_inv[OF C(3) _ C(1,2) uppert_to_jb[OF C(1) C(3)]] have "inv_all n jb (step_3 C)" and sd: "same_diag n C (step_3 C)" unfolding step_3_def dimC by auto hence jbD: "⋀ i j. i < n ⟹ j < n ⟹ jb ?D i j" unfolding inv_all_def DC by auto from same_diag_ev_block[OF sd C(2)] have "ev_block n (step_3 C)" by auto from jnf_vector[OF D jbD this] have "jordan_matrix D = ?D" "0 ∉ fst ` set D" unfolding DC by auto with sim have "jordan_nf C D" unfolding jordan_nf_def by simp } note jnf_blocks = this have id: "map fst ?CD = Cs" by (induct Cs, auto) have id2: "map snd ?CD = map (jnf_vector o step_3) Cs" by (induct Cs, auto) have J: "?J = concat (map (jnf_vector ∘ step_3) Cs)" unfolding triangular_to_jnf_vector_def Let_def Cs_def .. from jordan_nf_diag_block_mat[of ?CD, OF jnf_blocks, unfolded id id2] have jnf: "jordan_nf (diag_block_mat Cs) ?J" unfolding J . hence "similar_mat (diag_block_mat Cs) (jordan_matrix ?J)" unfolding jordan_nf_def by auto from similar_mat_sym[OF similar_mat_trans[OF similar_mat_sym[OF this] sim[unfolded BC]]] jnf show ?thesis unfolding jordan_nf_def by auto qed (* hide auxiliary definitions and functions *) hide_const lookup_ev find_largest_block swap_cols_rows_block identify_block identify_blocks_main identify_blocks inv_all inv_all' same_diag jb uppert diff_ev ev_blocks ev_block step_1_main step_1 step_2_main step_2 step_3_a step_3_c step_3_c_inner_loop step_3 jnf_vector_main subsection ‹Combination with Schur-decomposition› definition jordan_nf_via_factored_charpoly :: "'a :: conjugatable_ordered_field mat ⇒ 'a list ⇒ (nat × 'a)list" where "jordan_nf_via_factored_charpoly A es = triangular_to_jnf_vector (schur_upper_triangular A es)" lemma jordan_nf_via_factored_charpoly: assumes A: "A ∈ carrier_mat n n" and linear: "char_poly A = (∏ a ← es. [:- a, 1:])" shows "jordan_nf A (jordan_nf_via_factored_charpoly A es)" proof - let ?B = "schur_upper_triangular A es" let ?J = "jordan_nf_via_factored_charpoly A es" from schur_upper_triangular[OF A linear] have B: "?B ∈ carrier_mat n n" "upper_triangular ?B" and AB: "similar_mat A ?B" by auto from triangular_to_jnf_vector[OF B] have "jordan_nf ?B ?J" unfolding jordan_nf_via_factored_charpoly_def . with similar_mat_trans[OF AB] show "jordan_nf A ?J" unfolding jordan_nf_def by blast qed lemma jordan_nf_exists: assumes A: "A ∈ carrier_mat n n" and linear: "char_poly A = (∏ (a :: 'a :: conjugatable_ordered_field) ← as. [:- a, 1:])" shows "∃n_as. jordan_nf A n_as" using jordan_nf_via_factored_charpoly[OF A linear] by blast lemma jordan_nf_iff_linear_factorization: fixes A :: "'a :: conjugatable_ordered_field mat" assumes A: "A ∈ carrier_mat n n" shows "(∃ n_as. jordan_nf A n_as) = (∃ as. char_poly A = (∏ a ← as. [:- a, 1:]))" (is "?l = ?r") proof assume ?r thus ?l using jordan_nf_exists[OF A] by auto next assume ?l then obtain n_as where jnf: "jordan_nf A n_as" by auto show ?r unfolding jordan_nf_char_poly[OF jnf] expand_powers[of "λ a. [: -a, 1:]" n_as] by blast qed lemma similar_iff_same_jordan_nf: fixes A :: "complex mat" assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" shows "similar_mat A B = (jordan_nf A = jordan_nf B)" proof show "similar_mat A B ⟹ jordan_nf A = jordan_nf B" by (intro ext, auto simp: jordan_nf_def, insert similar_mat_trans similar_mat_sym, blast+) assume id: "jordan_nf A = jordan_nf B" from char_poly_factorized[OF A] obtain as where "char_poly A = (∏a←as. [:- a, 1:])" by auto from jordan_nf_exists[OF A this] obtain n_as where jnfA: "jordan_nf A n_as" .. with id have jnfB: "jordan_nf B n_as" by simp from jnfA jnfB show "similar_mat A B" unfolding jordan_nf_def using similar_mat_trans similar_mat_sym by blast qed lemma order_char_poly_smult: fixes A :: "complex mat" assumes A: "A ∈ carrier_mat n n" and k: "k ≠ 0" shows "order x (char_poly (k ⋅⇩_{m}A)) = order (x / k) (char_poly A)" proof - from char_poly_factorized[OF A] obtain as where "char_poly A = (∏a←as. [:- a, 1:])" by auto from jordan_nf_exists[OF A this] obtain n_as where jnf: "jordan_nf A n_as" .. show ?thesis unfolding jordan_nf_order[OF jnf] jordan_nf_order[OF jordan_nf_smult[OF jnf k]] by (induct n_as, auto simp: k) qed subsection ‹Application for Complexity› text ‹We can estimate the complexity via the multiplicity of the eigenvalues with norm 1.› lemma factored_char_poly_norm_bound_cof: assumes A: "A ∈ carrier_mat n n" and linear_factors: "char_poly A = (∏ (a :: 'a :: {conjugatable_ordered_field, real_normed_field}) ← as. [:- a, 1:])" and le_1: "⋀ a. a ∈ set as ⟹ norm a ≤ 1" and le_N: "⋀ a. a ∈ set as ⟹ norm a = 1 ⟹ length (filter ((=) a) as) ≤ N" shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩_{m}k) (c1 + c2 * of_nat k ^ (N - 1))" by (rule factored_char_poly_norm_bound[OF A linear_factors jordan_nf_exists[OF A linear_factors] le_1 le_N]) text ‹If we have an upper triangular matrix, then EVs are exactly the entries on the diagonal. So then we don't need to explicitly compute the characteristic polynomial.› lemma counting_ones_complexity: fixes A :: "'a :: real_normed_field mat" assumes A: "A ∈ carrier_mat n n" and upper_t: "upper_triangular A" and le_1: "⋀ a. a ∈ set (diag_mat A) ⟹ norm a ≤ 1" and le_N: "⋀ a. a ∈ set (diag_mat A) ⟹ norm a = 1 ⟹ length (filter ((=) a) (diag_mat A)) ≤ N" shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩_{m}k) (c1 + c2 * of_nat k ^ (N - 1))" proof - from triangular_to_jnf_vector[OF A upper_t] have jnf: "∃ n_as. jordan_nf A n_as" .. show ?thesis by (rule factored_char_poly_norm_bound[OF A char_poly_upper_triangular[OF A upper_t] jnf le_1 le_N]) qed text ‹If we have an upper triangular matrix $A$ then we can compute a JNF-vector of it. If this vector does not contain entries $(n,ev)$ with $ev$ being larger 1, then the growth rate of $A^k$ can be restricted by ${\cal O}(k^{N-1})$ where $N$ is the maximal value for $n$, where $(n,|ev| = 1)$ occurs in the vector, i.e., the size of the largest Jordan Block with Eigenvalue of norm 1. This method gives a precise complexity bound.› lemma compute_jnf_complexity: assumes A: "A ∈ carrier_mat n n" and upper_t: "upper_triangular (A :: 'a :: real_normed_field mat)" and le_1: "⋀ n a. (n,a) ∈ set (triangular_to_jnf_vector A) ⟹ norm a ≤ 1" and le_N: "⋀ n a. (n,a) ∈ set (triangular_to_jnf_vector A) ⟹ norm a = 1 ⟹ n ≤ N" shows "∃ c1 c2. ∀ k. norm_bound (A ^⇩_{m}k) (c1 + c2 * of_nat k ^ (N - 1))" proof - let ?jnf = "triangular_to_jnf_vector A" from triangular_to_jnf_vector[OF A upper_t] have jnf: "jordan_nf A ?jnf" . show ?thesis by (rule jordan_nf_matrix_poly_bound[OF A le_1 le_N jnf]) qed end