Theory Jordan_Normal_Form_Existence
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› in "PO07"› where this algorithm was not
explicitly specified but only applied on an example. We further introduced step 2
which does not occur in the textbook description.
\begin{enumerate}
\item[1.] Eliminate entries within blocks besides EV $a$ and above EV $b$ for $a \neq b$:
for $A_{ij}$ with EV $a$ left of it, and EV $b$ below of it, perform
@{term "add_col_sub_row (A⇩i⇩j / (b - a)) i j"}.
The iteration should be by first increasing $j$ and the inner loop by decreasing $i$.
\item[2.] Move rows of same EV together, can only be done after 1.,
otherwise triangular-property is lost.
Say both rows $i$ and $j$ ($i < j$) contain EV $a$, but all rows between $i$ and $j$ have different EV.
Then perform
@{term "swap_cols_rows (i+1) j"},
@{term "swap_cols_rows (i+2) j"},
\ldots
@{term "swap_cols_rows (j-1) j"}.
Afterwards row $j$ will be at row $i+1$, and rows $i+1,\ldots,j-1$ will be moved to $i+2,\ldots,j$.
The global iteration works by increasing $j$.
\item[3.] Transform each EV-block into JNF, do this for increasing upper $n \times k$ matrices,
where each new column $k$ will be treated as follows.
\begin{enumerate}
\item[a)] Eliminate entries $A_{ik}$ in rows of form $0 \ldots 0\ ev\ 1\ 0 \ldots 0\ A_{ik}$:
@{term "add_col_sub_row (-A⇩i⇩k) (i+1) k"}.
Perform elimination by increasing $i$.
\item[b)] Figure out largest JB (of $n-1 \times n-1$ sub-matrix) with lowest row of form $0 \ldots 0\ ev\ 0 \ldots 0\ A_{lk}$
where $A_{lk} \neq 0$, and set $x := A_{lk}$.
\item[c)] If such a JB does not exist, continue with next column.
Otherwise, eliminate all other non-zero-entries $y := A_{ik}$ via row $l$:
@{term "add_col_sub_row (y/x) i l"},
@{term "add_col_sub_row (y/x) (i-1) (l-1)"},
@{term "add_col_sub_row (y/x) (i-2) (l-2)"}, \ldots
where the number of steps is determined by the size of the JB left-above of $A_{ik}$.
Perform an iteration over $i$.
\item[d)] Normalize value in row $l$ to 1:
@{term "mult_col_div_row (1/x) k"}.
\item[e)] Move the 1 down from row $l$ to row $k-1$:
@{term "swap_cols_rows (l+1) k"},
@{term "swap_cols_rows (l+2) k"},
\ldots,
@{term "swap_cols_rows (k-1) k"}.
\end{enumerate}
\end{enumerate}
›
subsection ‹Real Algorithm›
fun lookup_ev :: "'a ⇒ nat ⇒ 'a mat ⇒ nat option" where
"lookup_ev ev 0 A = None"
| "lookup_ev ev (Suc i) A = (if A $$ (i,i) = ev then Some i else lookup_ev ev i A)"
function swap_cols_rows_block :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"swap_cols_rows_block i j A = (if i < j then
swap_cols_rows_block (Suc i) j (swap_cols_rows i j A) else A)"
by pat_completeness auto
termination by (relation "measure (λ (i,j,A). j - i)") auto
fun identify_block :: "'a :: one mat ⇒ nat ⇒ nat" where
"identify_block A 0 = 0"
| "identify_block A (Suc i) = (if A $$ (i,Suc i) = 1 then
identify_block A i else (Suc i))"
function identify_blocks_main :: "'a :: ring_1 mat ⇒ nat ⇒ (nat × nat) list ⇒ (nat × nat) list" where
"identify_blocks_main A 0 list = list"
| "identify_blocks_main A (Suc i_end) list = (
let i_begin = identify_block A i_end
in identify_blocks_main A i_begin ((i_begin, i_end) # list)
)"
by pat_completeness auto
definition identify_blocks :: "'a :: ring_1 mat ⇒ nat ⇒ (nat × nat)list" where
"identify_blocks A i = identify_blocks_main A i []"
fun find_largest_block :: "nat × nat ⇒ (nat × nat)list ⇒ nat × nat" where
"find_largest_block block [] = block"
| "find_largest_block (m_start,m_end) ((i_start,i_end) # blocks) =
(if i_end - i_start ≥ m_end - m_start then
find_largest_block (i_start,i_end) blocks else
find_largest_block (m_start,m_end) blocks)"
fun lookup_other_ev :: "'a ⇒ nat ⇒ 'a mat ⇒ nat option" where
"lookup_other_ev ev 0 A = None"
| "lookup_other_ev ev (Suc i) A = (if A $$ (i,i) ≠ ev then Some i else lookup_other_ev ev i A)"
partial_function (tailrec) partition_ev_blocks :: "'a mat ⇒ 'a mat list ⇒ 'a mat list" where
[code]: "partition_ev_blocks A bs = (let n = dim_row A in
if n = 0 then bs
else (case lookup_other_ev (A $$ (n-1, n-1)) (n-1) A of
None ⇒ A # bs
| Some i ⇒ case split_block A (Suc i) (Suc i) of (UL,_,_,LR) ⇒ partition_ev_blocks UL (LR # bs)))"
context
fixes n :: nat
and ty :: "'a :: field itself"
begin
function step_1_main :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"step_1_main i j A = (if j ≥ n then A else if i = 0 then step_1_main (j+1) (j+1) A
else let
i' = i - 1;
ev_left = A $$ (i',i');
ev_below = A $$ (j,j);
aij = A $$ (i',j);
B = if (ev_left ≠ ev_below ∧ aij ≠ 0) then add_col_sub_row (aij / (ev_below - ev_left)) i' j A else A
in step_1_main i' j B)"
by pat_completeness auto
termination by (relation "measures [λ (i,j,A). n - j, λ (i,j,A). i]") auto
function step_2_main :: "nat ⇒ 'a mat ⇒ 'a mat" where
"step_2_main j A = (if j ≥ n then A
else
let ev = A $$ (j,j);
B = (case lookup_ev ev j A of
None ⇒ A
| Some i ⇒ swap_cols_rows_block (Suc i) j A
)
in step_2_main (Suc j) B)"
by pat_completeness auto
termination by (relation "measure (λ (j,A). n - j)") auto
fun step_3_a :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"step_3_a 0 j A = A"
| "step_3_a (Suc i) j A = (let
aij = A $$ (i,j);
B = (if A $$ (i,i+1) = 1 ∧ aij ≠ 0
then add_col_sub_row (- aij) (Suc i) j A else A)
in step_3_a i j B)"
fun step_3_c_inner_loop :: "'a ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"step_3_c_inner_loop val l i 0 A = A"
| "step_3_c_inner_loop val l i (Suc k) A = step_3_c_inner_loop val (l - 1) (i - 1) k
(add_col_sub_row val i l A)"
fun step_3_c :: "'a ⇒ nat ⇒ nat ⇒ (nat × nat)list ⇒ 'a mat ⇒ 'a mat" where
"step_3_c x l k [] A = A"
| "step_3_c x l k ((i_begin,i_end) # blocks) A = (
let
B = (if i_end = l then A else
step_3_c_inner_loop (A $$ (i_end,k) / x) l i_end (Suc i_end - i_begin) A)
in step_3_c x l k blocks B)"
function step_3_main :: "nat ⇒ 'a mat ⇒ 'a mat" where
"step_3_main k A = (if k ≥ n then A
else let
B = step_3_a (k-1) k A;
all_blocks = identify_blocks B k;
blocks = filter (λ block. B $$ (snd block,k) ≠ 0) all_blocks;
F = (if blocks = []
then B
else let
(l_start,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)
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
definition uppert :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where
"uppert A i j ≡ j < i ⟶ A $$ (i,j) = 0"
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"
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.›
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)"
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)"
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)"
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))))"
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)
⟹ x = A $$ (l,k)
⟹ x ≠ 0
⟹ inv_all uppert (step_3_c x l k bs A)
∧ same_diag A (step_3_c x l k bs A)
∧ same_upto k A (step_3_c x l k bs A)
∧ inv_at (single_non_zero l k x) (step_3_c x l k bs A) k"
proof (induct bs arbitrary: A)
case (Nil A)
note inv = Nil(4-7)
from inv_from_upto_at_all_ev_block[OF inv(1-4) _ ‹k < n›]
have "inv_all uppert A" unfolding one_zero_def diff_ev_def uppert_def by auto
moreover
have "inv_at (single_non_zero l k x) A k" unfolding single_non_zero_def inv_at_def
by (intro allI impI conjI, insert Nil, auto)
ultimately show ?case by auto
next
case (Cons p bs A)
obtain i_begin i_end where p: "p = (i_begin, i_end)" by force
note Cons = Cons[unfolded p]
note IH = Cons(1)
note A = Cons(2)
note kn = Cons(3)
note lbl = Cons(4)
note inv = Cons(5-8)
note blocks = Cons(9-11)
note x = Cons(12-13)
from identify_blocks[OF lbl] kn have lk: "l < k" and ln: "l < n" and "lb ≤ l" by auto
define B where "B = step_3_c_inner_loop (A $$ (i_end,k) / x) l i_end (Suc i_end - i_begin) A"
show ?case
proof (cases "i_end = l")
case True
hence id: "step_3_c x l k (p # bs) A = step_3_c x l k bs A" unfolding p by simp
show ?thesis unfolding id
by (rule IH[OF A kn lbl inv _ blocks(2-3) x], insert blocks(1), auto simp: p True)
next
case False note il = this
hence id: "step_3_c x l k (p # bs) A = step_3_c x l k bs B" unfolding B_def p by simp
from blocks[unfolded p] have
ib_block: "(i_begin,i_end) ∈ set (identify_blocks A k)" and large: "i_end - i_begin ≤ l - lb" by auto
from identify_blocks[OF this(1)]
have ibe: "i_begin ≤ i_end" "i_end < k" by auto
have B: "B = mat n n (λ (i,j). if (i,j) = (i_end,k) then 0 else
if i_begin ≤ i ∧ i ≤ i_end ∧ j > k then A $$ (i,j) - A $$ (i_end,k) / x * A $$ (l + i - i_end,j) else A $$ (i,j))"
unfolding B_def x
by (rule step_3_c_inner_result[OF inv kn A lbl ib_block il large], insert x, auto)
have Bn: "B ∈ carrier_mat n n" unfolding B by auto
have sdAB: "same_diag A B" unfolding B same_diag_def using ibe by auto
have suAB: "same_upto k A B" using A kn unfolding B same_upto_def by auto
have inv_ev: "ev_block n B" using same_diag_ev_block[OF sdAB inv(4)] .
have inv_jb: "inv_upto jb B k" using same_upto_inv_upto_jb[OF suAB inv(1)] .
have ib: "identify_blocks A k = identify_blocks B k" using identify_blocks_cong[OF kn sdAB suAB] .
have inv_ut: "inv_from uppert B k" using inv(2) ibe unfolding B inv_from_def uppert_def by auto
from x il ibe kn lk have xB: "x = B $$ (l,k)" by (auto simp: B)
{
fix be
assume *: "be ∉ snd ` set bs" "be ∉ {l, k}" "be < n"
hence "B $$ (be, k) = 0" using kn blocks(2)[of be] unfolding B
by (cases "be = i_end", auto)
} note blocksB = this
have bs: "set bs ⊆ set (identify_blocks A k)" using blocks(1) by auto
have inv_oz: "inv_at one_zero B k" using inv(3) ibe kn unfolding B inv_at_def one_zero_def by simp
show ?thesis unfolding id
using IH[OF Bn kn, folded ib, OF lbl inv_jb inv_ut inv_oz inv_ev bs blocksB blocks(3) xB x(2)]
using same_diag_trans[OF sdAB] same_upto_trans[OF suAB]
by auto
qed
qed
lemma step_3_main_inv: "A ∈ carrier_mat n n
⟹ k > 0
⟹ inv_all uppert A
⟹ ev_block n A
⟹ inv_upto jb A k
⟹ inv_all jb (step_3_main n k A) ∧ same_diag A (step_3_main n k A)"
proof (induct k A taking: n rule: step_3_main.induct)
case (1 k A)
from 1(2-) have A: "A ∈ carrier_mat n n" and k: "k > 0" and
inv: "inv_all uppert A" "ev_block n A" "inv_upto jb A k" by auto
note [simp] = step_3_main.simps[of n k A]
show ?case
proof (cases "k ≥ n")
case True
thus ?thesis using inv_uptoD[OF inv(3)]
by (intro conjI inv_allI, auto)
next
case False
hence kn: "k < n" by simp
obtain B where B: "B = step_3_a (k - 1) k A" by auto
note IH = 1(1)[OF False B]
from A have Bn: "B ∈ carrier_mat n n" unfolding B carrier_mat_def by simp
from k have "k - 1 < k" by simp
{
fix i
assume "i < k"
with ev_blockD[OF inv(2) _ ‹k < n›, of i] ‹k < n› have "A $$ (i,i) = A $$ (k,k)" by auto
}
hence "inv_from_bot (λA i. one_zero A i k) A (k - 1)"
using inv_all_uppertD[OF inv(1), of k]
unfolding inv_from_bot_def one_zero_def by auto
from step_3_a_inv[OF A ‹k - 1 < k› ‹k < n› inv(3) inv_all_imp_inv_from[OF inv(1)]
this inv(2)] same_diag_ev_block[OF _ inv(2)]
have inv: "inv_from uppert B k" "ev_block n B" "inv_upto jb B k"
"inv_at one_zero B k" and sd: "same_diag A B" unfolding B by auto
note evb = ev_blockD[OF inv(2)]
obtain all_blocks where ab: "all_blocks = identify_blocks B k" by simp
obtain blocks where blocks: "blocks = filter (λ block. B $$ (snd block, k) ≠ 0) all_blocks" by simp
obtain F where F: "F = (if blocks = [] then B
else let (l_begin,l) = find_largest_block (hd blocks) (tl blocks); x = B $$ (l, k); C = step_3_c x l k blocks B;
D = mult_col_div_row (inverse x) k C; E = swap_cols_rows_block (Suc l) k D
in E)" by simp
note IH = IH[OF ab blocks F]
have Fn: "F ∈ carrier_mat n n" unfolding F Let_def carrier_mat_def using Bn
by (simp split: prod.splits)
have inv: "inv_all uppert F ∧ same_diag A F ∧ inv_upto jb F (Suc k)"
proof (cases "blocks = []")
case True
hence F: "F = B" unfolding F by simp
have lo: "inv_at (lower_one k) B k"
proof
fix i
assume i: "i < n"
note lower_one_def[simp]
show "lower_one k B i k"
proof (cases "B $$ (i,k) = 0")
case False note nz = this
note oz = inv_atD[OF inv(4) i, unfolded one_zero_def]
from nz oz have "i ≤ k" by auto
show ?thesis
proof (cases "i = k")
case False
with ‹i ≤ k› have "i < k" by auto
with nz oz have ev: "B $$ (i,i) = B $$ (k,k)" unfolding diff_ev_def by auto
have "(identify_block B i, i) ∈ set all_blocks" unfolding ab
proof (rule identify_blocks_rev[OF _ ‹k < n›])
show "B $$ (i, Suc i) = 0 ∧ Suc i < k ∨ Suc i = k"
proof (cases "Suc i = k")
case False
with ‹i < k› ‹k < n› have "Suc i < k" "Suc i < n" by simp_all
with nz oz have "B $$ (i, Suc i) ≠ 1" by simp
with inv_uptoD[OF inv(3) ‹i < n› ‹Suc i < n› ‹Suc i < k›, unfolded jb_def]
have "B $$ (i, Suc i) = 0" by simp
thus ?thesis using ‹Suc i < k› by simp
qed simp
qed
with arg_cong[OF ‹blocks = []›[unfolded blocks], of set] have "B $$ (i,k) = 0" by auto
with nz show ?thesis by auto
qed auto
qed auto
qed
have inv_jb: "inv_upto jb B (Suc k)"
proof (rule inv_upto_Suc[OF inv(3)])
fix i
assume "i < n"
from inv_atD[OF lo ‹i < n›, unfolded lower_one_def]
show "jb B i k" unfolding jb_def by auto
qed
from inv_from_upto_at_all_ev_block[OF inv(3,1) lo inv(2) _ ‹k < n›] lower_one_diff_uppert
have "inv_all uppert B" by auto
with inv inv_jb sd
show ?thesis unfolding F by simp
next
case False
obtain l_start l where l: "find_largest_block (hd blocks) (tl blocks) = (l_start, l)" by force
obtain x where x: "x = B $$ (l,k)" by simp
obtain C where C: "C = step_3_c x l k blocks B" by simp
obtain D where D: "D = mult_col_div_row (inverse x) k C" by auto
obtain E where E: "E = swap_cols_rows_block (Suc l) k D" by auto
from find_largest_block[OF False l] have lb: "(l_start,l) ∈ set blocks"
and llarge: "⋀ i_begin i_end. (i_begin,i_end) ∈ set blocks ⟹ l - l_start ≥ i_end - i_begin" by auto
from lb have x0: "x ≠ 0" unfolding blocks x by simp
{
fix i_start i_end
assume "(i_start,i_end) ∈ set blocks"
hence "(i_start,i_end) ∈ set (identify_blocks B k)" unfolding blocks ab by simp
with identify_blocks[OF this]
have "i_end < k" "(i_start,i_end) ∈ set (identify_blocks B k)" by auto
} note block_bound = this
from block_bound[OF lb]
have lk: "l < k" and lblock: "(l_start, l) ∈ set (identify_blocks B k)" by auto
from lk ‹k < n› have ln: "l < n" by simp
from evb[OF ‹l < n› ‹k < n›]
have Bll: "B $$ (l,l) = B $$ (k,k)" .
from False have F: "F = E" unfolding E D C x F l Let_def by simp
from Bn have Cn: "C ∈ carrier_mat n n" unfolding C carrier_mat_def by simp
{
fix be
assume nmem: "be ∉ snd ` set blocks" and belk: "be ∉ {l, k}" and be: "be < n"
have "B $$ (be, k) = 0"
proof (rule ccontr)
assume nz: "¬ ?thesis"
note oz = inv_atD[OF inv(4) be, unfolded one_zero_def]
from belk oz be nz have "be < k" by auto
obtain bb where ib: "identify_block B be = bb" by force
note ib_inv = identify_block[OF ib]
have "B $$ (be, Suc be) = 0 ∧ Suc be < k ∨ Suc be = k"
proof (cases "Suc be = k")
case False
with ‹be < k› have sbek: "Suc be < k" by auto
from inv_uptoD[OF inv(3) ‹be < n› _ sbek] sbek kn have "jb B be (Suc be)" by auto
from this[unfolded jb_def] have 01: "B $$ (be, Suc be) ∈ {0,1}" by auto
from 01 oz sbek nz have "B $$ (be, Suc be) = 0" by auto
with sbek show ?thesis by auto
qed auto
from identify_blocks_rev[OF this kn]
nz nmem show False unfolding ab blocks by force
qed
}
note inv3 = step_3_c_inv[OF Bn ‹k < n› lblock inv(3,1,4,2) _ this llarge x x0, of blocks, folded C,
unfolded ab blocks]
from inv3 have sdC: "same_diag B C" and suC: "same_upto k B C" by auto
note sd = same_diag_trans[OF sd sdC]
from Bll sdC ln ‹k < n›
have Cll: "C $$ (l,l) = C $$ (k,k)" unfolding same_diag_def by auto
from same_diag_ev_block[OF sdC inv(2)] same_upto_inv_upto_jb[OF suC inv(3)] inv3
have inv: "inv_all uppert C" "ev_block n C"
"inv_upto jb C k" "inv_at (single_non_zero l k x) C k" by auto
from x0 have "inverse x ≠ 0" by simp
from Cn have Dn: "D ∈ carrier_mat n n" unfolding D carrier_mat_def by simp
{
fix i j
assume i: "i < n" and j: "j < n"
with Cn have dC: "i < dim_row C" "i < dim_col C" "j < dim_row C" "j < dim_col C" by auto
let ?c = "C $$ (i,j)"
let ?x = "inverse x"
have "D $$ (i,j) = (if i = l ∧ j = k then 1 else if i = k ∧ j ≠ k then x * ?c else ?c)"
unfolding D
proof (subst mult_col_div_index_row[OF dC ‹inverse x ≠ 0›], unfold inverse_inverse_eq)
note at = inv_atD[OF inv(4) ‹i < n›, unfolded single_non_zero_def]
show "(if i = k ∧ j ≠ i then x * ?c
else if j = k ∧ j ≠ i then ?x * ?c else ?c) =
(if i = l ∧ j = k then 1 else if i = k ∧ j ≠ k then x * ?c else ?c)" (is "?l = ?r")
proof (cases "(i,j) = (l,k)")
case True
with lk have "?l = ?x * ?c" by auto
also have "… = 1" using at True ‹inverse x ≠ 0› by auto
finally show ?thesis using True by simp
next
case False note neq = this
have "?l = (if i = k ∧ j ≠ k then x * ?c else ?c)"
proof (cases "i = k ∧ j ≠ k ∨ j = k ∧ i ≠ k")
case True
thus ?thesis
proof
assume *: "i = k ∧ j ≠ k"
hence l: "?l = x * ?c" by simp
show ?thesis using * neq unfolding l by simp
next
assume *: "j = k ∧ i ≠ k"
hence "?l = ?x * ?c" using lk by auto
from * neq have "i ≠ l" and **: "¬ (i = k ∧ j ≠ k)" by auto
from at ‹i ≠ l› * have "?c = 0" by auto
with ‹?l = ?x * ?c› ** show ?thesis by auto
qed
qed auto
also have "… = ?r" using False by auto
finally show ?thesis .
qed
qed
} note D = this
have sD[simp]: "⋀ i. i < n ⟹ D $$ (i,i) = C $$ (i,i)" using lk by (auto simp: D)
from ‹C $$ (l,l) = C $$ (k,k)› ‹l < n› ‹k < n›
have Dll: "D $$ (l,l) = D $$ (k,k)" by simp
have sdD: "same_diag C D" unfolding same_diag_def by simp
note sd = same_diag_trans[OF sd sdD]
from same_diag_ev_block[OF sdD inv(2)] have invD: "ev_block n D" .
note inv = inv_uptoD[OF inv(3), unfolded jb_def] inv_all_uppertD[OF inv(1)]
inv_atD[OF inv(4), unfolded single_non_zero_def]
moreover have "inv_all uppert D"
by (intro inv_allI, insert inv(2) lk, auto simp: uppert_def D)
moreover have suD: "same_upto k C D"
proof
fix i j
assume i: "i < n" and j: "j < k"
with kn have jn: "j < n" by simp
show "C $$ (i, j) = D $$ (i, j)"
unfolding D[OF i jn] using j k
inv(1)[OF i jn j] i j by auto
qed
from same_upto_inv_upto_jb[OF suD ‹inv_upto jb C k›]
have "inv_upto jb D k" .
moreover
let ?single_one = "single_one l k"
have "inv_at ?single_one D k"
by (intro inv_atI, insert inv(3) D[OF _ ‹k < n›] ln, auto simp: single_one_def)
ultimately
have inv: "inv_all uppert D" "ev_block n D"
"inv_upto jb D k" "inv_at ?single_one D k" using invD by blast+
note inv = inv_uptoD[OF inv(3), unfolded jb_def]
inv_all_uppertD[OF inv(1)]
inv_atD[OF inv(4), unfolded single_one_def]
ev_blockD[OF inv(2)]
from suC suD have suD: "same_upto k B D" unfolding same_upto_def by auto
let ?I = "λ j. if j = Suc l then k else if Suc l < j ∧ j ≤ k then j - 1 else j"
let ?I' = "λ j. if j = Suc l then k else j - 1"
{
fix i j
assume i: "i < n" and j: "j < n"
with Dn lk ‹k < n›
have dims: "i < dim_row D" "i < dim_col D" "j < dim_row D" "j < dim_col D"
"Suc l ≤ k" "k < dim_row D" "k < dim_col D" by auto
have "E $$ (i,j) = D $$ (?I i, ?I j)"
unfolding E by (rule subst swap_cols_rows_block_index[OF dims])
} note E = this
{
fix i
assume i: "i < n"
from ‹l < k› have "l ≤ Suc l" "Suc l ≤ k" by auto
have "E $$ (i,i) = D $$ (i,i)" unfolding E[OF i i]
by (rule inv(4), insert i ‹k < n›, auto)
} note Ed = this
from Ed have ed: "same_diag D E" unfolding same_diag_def by auto
note sd = same_diag_trans[OF sd ed]
have "ev_block n E" using same_diag_ev_block[OF ed ‹ev_block n D›] by auto
moreover have Eut: "inv_all uppert E"
proof (intro inv_allI, unfold uppert_def, intro impI)
fix i j
assume i: "i < n" and j: "j < n" and ji: "j < i"
have "?I i < n" using i ‹k < n› by auto
show "E $$ (i,j) = 0"
proof (cases "?I j < ?I i")
case True
from inv(2)[OF this ‹?I i < n›] show ?thesis unfolding E[OF i j] .
next
case False
have "?I i ≠ ?I j" using ji lk by (auto split: if_splits)
with False have ij: "?I i < ?I j" by simp
from ij ji have jl: "j = Suc l" using lk by (auto split: if_splits)
with ji ij have il: "i > Suc l" "i ≤ k" by (auto split: if_splits)
from jl il have Eij: "E $$ (i,j) = D $$ (i-1,k)" unfolding E[OF i j] by simp
have "i - 1 < n" "i - 1 ∉ {k, l}" using i il by auto
with inv(3)[of "i-1"] have D: "D $$ (i-1,k) = 0" by auto
show ?thesis unfolding Eij D by simp
qed
qed
moreover
from same_diag_trans[OF ‹same_diag B C› ‹same_diag C D›] have "same_diag B D" .
from identify_blocks_cong[OF ‹k < n› this suD]
have idb: "identify_blocks B k = identify_blocks D k" .
have "inv_upto jb E (Suc k)"
proof (intro inv_uptoI)
fix i j
assume i: "i < n" and j: "j < n" and "j < Suc k"
hence jk: "j ≤ k" by simp
show "jb E i j"
proof (cases "E $$ (i,j) = 0 ∨ j = i")
case True
thus ?thesis unfolding jb_def by auto
next
case False note enz = this
from inv(4)[OF i j] have same_ev: "D $$ (i,i) = D $$ (j,j)" .
note inv2 = inv_all_uppertD[OF Eut _ i, of j]
from False inv2 have "¬ j < i" by auto
with False have ji: "j > i" by auto
have "E $$ (i,j) ∈ {0,1} ∧ (j ≠ Suc i ⟶ E $$ (i,j) = 0)"
proof (cases "j ≤ l")
case True note jl = this
with ji lk have il: "i ≤ l" and jk: "j < k" by auto
have id: "E $$ (i,j) = D $$ (i,j)" unfolding E[OF i j] using jl il by simp
from inv(1)[OF i j jk] ji
show ?thesis unfolding id by auto
next
case False note jl = this
show ?thesis
proof (cases "j = Suc l")
case True note jl = this
with ji lk have il: "i ≤ l" "i ≠ k" by auto
have id: "E $$ (i,j) = D $$ (i,k)" unfolding E[OF i j] using jl il by auto
from inv(3)[OF i] jl il
show ?thesis unfolding id by (cases "i = l", auto)
next
case False
with jl jk kn have jl: "j > Suc l" and jk: "j - 1 < k" and jn: "j - 1 < n" by auto
with jk have id: "?I j = j - 1" by auto
note jb = inv(1)[OF _ jn jk]
show ?thesis
proof (cases "i < Suc l")
case True note il = this
with id have id: "E $$ (i,j) = D $$ (i,j - 1)" unfolding E[OF i j] by auto
show ?thesis
proof (cases "i = j - 2")
case False
thus ?thesis unfolding id using jb[OF i] il jl by auto
next
case True
with il jl have *: "j = Suc (Suc l)" "i = l" by auto
with id have id: "E $$ (i,j) = D $$ (l,Suc l)" by auto
from * jl jk have neq: "Suc l ≠ k" by auto
from lblock[unfolded idb] have "(l_start, l) ∈ set (identify_blocks D k)" .
from this[unfolded identify_blocks_iff[OF kn]] neq
have "D $$ (l, Suc l) ≠ 1" by auto
with jb[OF i] il jl ji * have "D $$ (l, Suc l) = 0" by auto
thus ?thesis unfolding id by simp
qed
next
case False note il = this
show ?thesis
proof (cases "i = Suc l")
case True
with id have id: "E $$ (i,j) = D $$ (k,j - 1)" unfolding E[OF i j] by auto
from inv(2)[OF jk kn] show ?thesis unfolding id by simp
next
case False
with il jl ji jk kn have il: "i > Suc l" and ik: "i < k" and i_n: "i - 1 < n" by auto
with id have id: "E $$ (i,j) = D $$ (i - 1, j - 1)" unfolding E[OF i j] by auto
show ?thesis unfolding id using jb[OF i_n] il jl ji by auto
qed
qed
qed
qed
thus "jb E i j" unfolding jb_def Ed[OF i] Ed[OF j] same_ev by auto
qed
qed
ultimately show ?thesis using sd unfolding F by simp
qed
hence inv: "inv_all uppert F" "ev_block n F" "inv_upto jb F (Suc k)"
and sd: "same_diag A F" using same_diag_ev_block[OF _ ‹ev_block n A›] by auto
have "0 < Suc k" by simp
note IH = IH[OF Fn this inv(1-3)]
have id: "step_3_main n k A = step_3_main n (Suc k) F" using kn
by (simp add: F Let_def blocks ab B)
from same_diag_trans[OF sd] IH
show ?thesis unfolding id by auto
qed
qed
lemma step_1_2_inv:
assumes A: "A ∈ carrier_mat n n"
and upper_t: "upper_triangular A"
and Bid: "B = step_2 (step_1 A)"
shows "inv_all uppert B" "inv_all diff_ev B" "ev_blocks B"
proof -
from A have d: "dim_row A = n" by simp
let ?B = "step_2 (step_1 A)"
from upper_triangularD[OF upper_t] have inv: "inv_all uppert A"
unfolding inv_all_def uppert_def using A by auto
from upper_t have inv2: "inv_part diff_ev A 0 0"
unfolding inv_part_def diff_ev_def by auto
have inv3: "ev_blocks_part 0 (step_1 A)"
by (rule ev_blocks_partI, auto)
have A1: "step_1 A ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto
from A1 have d1: "dim_row (step_1 A) = n" unfolding carrier_mat_def by simp
have B: "?B ∈ carrier_mat n n" using A unfolding carrier_mat_def by auto
from B have d2: "dim_row ?B = n" unfolding carrier_mat_def by simp
have "inv_all uppert (step_1 A) ∧ inv_all diff_ev (step_1 A)" unfolding step_1_def d
by (rule step_1_main_inv[OF _ A inv inv2], simp)
hence "inv_all uppert (step_1 A)" and "inv_all diff_ev (step_1 A)" by auto
from step_2_main_inv[OF A1 this inv3]
show "inv_all uppert B" "inv_all diff_ev B" "ev_blocks B"
unfolding step_2_def d d1 Bid by auto
qed
definition inv_all' :: "('a mat ⇒ nat ⇒ nat ⇒ bool) ⇒ 'a mat ⇒ bool" where
"inv_all' p A ≡ ∀ i j. i < dim_row A ⟶ j < dim_row A ⟶ p A i j"
private lemma lookup_other_ev_None: assumes "lookup_other_ev ev k A = None"
and "i < k"
shows "A $$ (i,i) = ev"
using assms by (induct ev k A rule: lookup_other_ev.induct, auto split: if_splits)
(insert less_antisym, blast)
private lemma lookup_other_ev_Some: assumes "lookup_other_ev ev k A = Some i"
shows "i < k ∧ A $$ (i,i) ≠ ev ∧ (∀ j. i < j ∧ j < k ⟶ A $$ (j,j) = ev)"
using assms by (induct ev k A rule: lookup_other_ev.induct, auto split: if_splits)
(insert less_SucE, blast)
lemma partition_jb: assumes A: "(A :: 'a mat) ∈ carrier_mat n n"
and inv: "inv_all uppert A" "inv_all diff_ev A" "ev_blocks A"
and part: "partition_ev_blocks A [] = bs"
shows "A = diag_block_mat bs" "⋀ B. B ∈ set bs ⟹ inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B"
proof -
have diag: "diag_block_mat [A] = A" using A by auto
{
fix cs
assume *: "⋀ C. C ∈ set cs ⟹ dim_row C = dim_col C ∧ inv_all' uppert C ∧ ev_block (dim_col C) C" "partition_ev_blocks A cs = bs"
from inv have inv: "inv_all' uppert A" "inv_all' diff_ev A" "ev_blocks_part n A"
unfolding inv_all_def inv_all'_def ev_blocks_def using A by auto
hence "diag_block_mat (A # cs) = diag_block_mat bs ∧ (∀ B ∈ set bs. inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B)"
using A *
proof (induct n arbitrary: A cs bs rule: less_induct)
case (less n A cs bs)
from less(5) have A: "A ∈ carrier_mat n n" by auto
hence dim: "dim_row A = n" "dim_col A = n" by auto
let ?dim = "sum_list (map dim_col cs)"
let ?C = "diag_block_mat cs"
define C where "C = ?C"
from less(6) have cs: "⋀ C. C ∈ set cs ⟹ inv_all' uppert C ∧ ev_block (dim_col C) C ∧ dim_row C = dim_col C" by auto
hence dimcs[simp]: "sum_list (map dim_row cs) = ?dim" by (induct cs, auto)
from dim_diag_block_mat[of cs, unfolded dimcs] obtain nc where C: "?C ∈ carrier_mat nc nc" unfolding carrier_mat_def by auto
hence dimC: "dim_row C = nc" "dim_col C = nc" unfolding C_def by auto
note bs = less(7)[unfolded partition_ev_blocks.simps[of A cs] Let_def dim, symmetric]
show ?case
proof (cases "n = 0")
case True
hence bs: "bs = cs" unfolding bs by simp
thus ?thesis using cs A by (auto simp: Let_def True)
next
case False
let ?n1 = "n - 1"
let ?look = "lookup_other_ev (A $$ (?n1, ?n1)) ?n1 A"
show ?thesis
proof (cases ?look)
case None
from False None have bs: "bs = A # cs" unfolding bs by auto
have ut: "inv_all' uppert A" using less(2) by auto
from lookup_other_ev_None[OF None] have "⋀ i. i < n ⟹ A $$ (i,i) = A $$ (?n1, ?n1)"
by (case_tac "i = ?n1", auto)
hence evb: "ev_block n A" unfolding ev_block_def dim by metis
from cs A ut evb show ?thesis unfolding bs by auto
next
case (Some i)
let ?si = "Suc i"
from lookup_other_ev_Some[OF Some] have i: "i < ?n1" and neq: "A $$ (i,i) ≠ A $$ (?n1, ?n1)"
and between: "⋀j. i < j ⟹ j < ?n1 ⟹ A $$ (j,j) = A $$ (?n1, ?n1)" by auto
define m where "m = n - ?si"
from i False have si: "?si < n" by auto
from False i have nsi: "n = ?si + m" unfolding m_def by auto
obtain UL UR LL LR where split: "split_block A ?si ?si = (UL, UR, LL, LR)" by (rule prod_cases4)
from split_block[OF split dim[unfolded nsi]]
have carr: "UL ∈ carrier_mat ?si ?si" "UR ∈ carrier_mat ?si m" "LL ∈ carrier_mat m ?si" "LR ∈ carrier_mat m m"
and Ablock: "A = four_block_mat UL UR LL LR" by auto
hence dimLR: "dim_row LR = m" "dim_col LR = m" and dimUL: "dim_col UL = ?si" "dim_row UL = ?si" by auto
from less(3)[unfolded inv_all'_def diff_ev_def] dim
have diff: "⋀ i j. i < n ⟹ j < n ⟹ i < j ⟹ A $$ (i, i) ≠ A $$ (j, j) ⟹ A $$ (i, j) = 0" by auto
from less(2)[unfolded inv_all'_def uppert_def] dim
have ut: "⋀ i j. i < n ⟹ j < n ⟹ j < i ⟹ A $$ (i, j) = 0" by auto
let ?UR = "0⇩m ?si m"
have UR: "UR = ?UR"
proof (rule eq_matI)
fix ia j
assume ij: "ia < dim_row (0⇩m (Suc i) m)" "j < dim_col (0⇩m (Suc i) m)"
let ?j = "?si + j"
have "UL $$ (ia,ia) = A $$ (ia,ia)" using ij carr unfolding Ablock by auto
also have "… ≠ A $$ (?j, ?j)"
proof
assume eq: "A $$ (ia,ia) = A $$ (?j, ?j)"
from ij have rel: "ia ≤ i" "i ≤ ?j" "?j < n" using nsi i by auto
from ev_blocks_part_leD[OF less(4) this eq[symmetric]] eq
have eq: "A $$ (i,i) = A $$ (?j,?j)" by auto
also have "… = A $$ (?n1, ?n1)" using between[of ?j] rel by (cases "?j = ?n1", auto)
finally show False using neq by auto
qed
also have "A $$ (?si + j, ?si + j) = LR $$ (j,j)" using ij carr unfolding Ablock by auto
finally show "UR $$ (ia, j) = 0⇩m (Suc i) m $$ (ia, j)"
using diff[of ia "?si + j", unfolded Ablock] ij nsi carr by auto
qed (insert carr, auto)
let ?LL = "0⇩m m ?si"
have LL: "LL = ?LL"
proof (rule eq_matI)
fix ia j
show "ia < dim_row (0⇩m m (Suc i)) ⟹ j < dim_col (0⇩m m (Suc i)) ⟹ LL $$ (ia, j) = 0⇩m m (Suc i) $$ (ia, j)"
using ut[of "?si + ia" j, unfolded Ablock] nsi carr by auto
qed (insert carr, auto)
have utUL: "inv_all' uppert UL"unfolding inv_all'_def uppert_def
proof (intro allI impI)
fix i j
show "i < dim_row UL ⟹ j < dim_row UL ⟹ j < i ⟹ UL $$ (i, j) = 0"
using ut[of i j, unfolded Ablock] using nsi carr by auto
qed
have diffUL: "inv_all' diff_ev UL"unfolding inv_all'_def diff_ev_def
proof (intro allI impI)
fix i j
show "i < dim_row UL ⟹ j < dim_row UL ⟹ i < j ⟹ UL $$ (i, i) ≠ UL $$ (j, j) ⟹ UL $$ (i, j) = 0"
using diff[of i j, unfolded Ablock] using nsi carr by auto
qed
have evbUL: "ev_blocks_part ?si UL"unfolding ev_blocks_part_def
proof (intro allI impI)
fix ia j k
show "ia < j ⟹ j < k ⟹ k < Suc i ⟹ UL $$ (k, k) = UL $$ (ia, ia) ⟹ UL $$ (j, j) = UL $$ (ia, ia)"
using less(4)[unfolded Ablock ev_blocks_part_def, rule_format, of ia j k] using nsi carr by auto
qed
have utLR: "inv_all' uppert LR" unfolding inv_all'_def uppert_def
proof (intro allI impI)
fix i j
show "i < dim_row LR ⟹ j < dim_row LR ⟹ j < i ⟹ LR $$ (i, j) = 0"
using ut[of "?si + i" "?si + j", unfolded Ablock] nsi carr by auto
qed
have evbLR: "ev_block (dim_row LR) LR" unfolding ev_block_def
proof (intro allI impI)
fix i j
show "i < dim_row LR ⟹ j < dim_row LR ⟹ LR $$ (i, i) = LR $$ (j, j)"
using between[of "?si + i"] between[of "?si + j"] carr nsi
unfolding Ablock by auto (metis One_nat_def Suc_lessI diff_Suc_1)
qed
from False Some split have bs: "partition_ev_blocks UL (LR # cs) = bs" unfolding bs by auto
have IH: "diag_block_mat (UL # LR # cs) = diag_block_mat bs ∧ (∀B∈set bs. inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B)"
by (rule less(1)[OF si utUL diffUL evbUL carr(1) _ bs], insert dimLR evbLR utLR cs, auto)
have "diag_block_mat (A # cs) = diag_block_mat (UL # LR # cs)"
unfolding diag_block_mat.simps dim C_def[symmetric] dimC dimLR dimUL Let_def
index_mat_four_block(2-3) Ablock UR LL
using assoc_four_block_mat[of UL LR C] dimC carr by simp
with IH show ?thesis by auto
qed
qed
qed
}
from this[of Nil, OF _ part] show "A = diag_block_mat bs" "⋀ B. B ∈ set bs ⟹ inv_all' uppert B ∧ ev_block (dim_col B) B ∧ dim_row B = dim_col B"
unfolding diag by fastforce+
qed
lemma uppert_to_jb: assumes ut: "inv_all uppert A" and "A ∈ carrier_mat n n"
shows "inv_upto jb A 1"
proof (rule inv_uptoI)
fix i j
assume "i < n" "j < n" and "j < 1"
hence j: "j = 0" and jn: "0 < n" by auto
show "jb A i j" unfolding jb_def j using inv_all_uppertD[OF ut _ ‹i < n›, of 0]
by auto
qed
lemma jnf_vector: assumes A: "A ∈ carrier_mat n n"
and jb: "⋀ i j. i < n ⟹ j < n ⟹ jb A i j"
and evb: "ev_block n A"
shows "jordan_matrix (jnf_vector A) = (A :: 'a mat)"
"0 ∉ fst ` set (jnf_vector A)"
proof -
from A have "dim_row A = n" by simp
hence id: "jnf_vector A = jnf_vector_main n A" unfolding jnf_vector_def by auto
let ?map = "map (λ(n, a). jordan_block n (a :: 'a))"
let ?B = "λ k. diag_block_mat (?map (jnf_vector_main k A))"
{
fix k
assume "k ≤ n"
hence "(∀ i j. i < k ⟶ j < k ⟶ ?B k $$ (i,j) = A $$ (i,j))
∧ diag_block_mat (?map (jnf_vector_main k A)) ∈ carrier_mat k k
∧ 0 ∉ fst ` set (jnf_vector_main k A)"
proof (induct k rule: less_induct)
case (less sk)
show ?case
proof (cases sk)
case (Suc k)
obtain b where ib: "identify_block A k = b" by force
let ?ev = "A $$ (b,b)"
from ib have id: "jnf_vector_main sk A = jnf_vector_main b A @ [(Suc k - b, ?ev)]" unfolding Suc by simp
let ?c = "Suc k - b"
define B where "B = ?B b"
define C where "C = jordan_block ?c ?ev"
have C: "C ∈ carrier_mat ?c ?c" unfolding C_def by auto
let ?FB = "λ Bb Cc. four_block_mat Bb (0⇩m (dim_row Bb) (dim_col Cc)) (0⇩m (dim_row Cc) (dim_col Bb)) Cc"
from identify_block_le'[OF ib] have bk: "b ≤ k" .
with Suc less(2) have "b < sk" "b ≤ n" by auto
note IH = less(1)[OF this, folded B_def]
have B: "B ∈ carrier_mat b b" using IH by simp
from bk Suc have sk: "sk = b + ?c" by auto
show ?thesis unfolding id map_append list.simps diag_block_mat_last split B_def[symmetric] C_def[symmetric] Let_def
proof (intro allI conjI impI)
show "?FB B C ∈ carrier_mat sk sk" unfolding sk using four_block_carrier_mat[OF B C] .
fix i j
assume i: "i < sk" and j: "j < sk"
with jb ‹sk ≤ n›
have jb: "jb A i j" by auto
have ut: "uppert A i j" by (rule jb_imp_uppert[OF jb])
have de: "diff_ev A i j" by (rule jb_imp_diff_ev[OF jb])
from B C have dim: "dim_row B = b" "dim_col B = b" "dim_col C = ?c" "dim_row C = ?c" by auto
from sk B C i j have "i < dim_row B + dim_row C" "j < dim_col B + dim_col C" by auto
note id = index_mat_four_block(1)[OF this, unfolded dim]
have id: "?FB B C $$ (i,j) =
(if i < b then if j < b then B $$ (i, j) else 0
else if j < b then 0 else C $$ (i - b, j - b))"
unfolding id dim using i j sk by auto
show "?FB B C $$ (i,j) = A $$ (i,j)"
proof (cases "i < b ∧ j < b")
case True
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
hence id: "?FB B C $$ (i,j) = 0" unfolding id by auto
show ?thesis
proof (cases "j < i")
case True
with ut show ?thesis unfolding id uppert_def by auto
next
case False
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
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_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