Theory Jordan_Normal_Form_Existence

theory Jordan_Normal_Form_Existence
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 (Aij / (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 (-Aik) (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 = "0m ?si m"
          have UR: "UR = ?UR"
          proof (rule eq_matI)
            fix ia j
            assume ij: "ia < dim_row (0m (Suc i) m)" "j < dim_col (0m (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) = 0m (Suc i) m $$ (ia, j)"            
              using diff[of ia "?si + j", unfolded Ablock] ij nsi carr by auto
          qed (insert carr, auto)
          let ?LL = "0m m ?si"
          have LL: "LL = ?LL"
          proof (rule eq_matI)
            fix ia j
            show "ia < dim_row (0m m (Suc i)) ⟹ j < dim_col (0m m (Suc i)) ⟹ LL $$ (ia, j) = 0m 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 (0m (dim_row Bb) (dim_col Cc)) (0m (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