Theory Jordan_Normal_Form.Column_Operations
section ‹Elementary Column Operations›
text ‹We define elementary column operations and also combine them with elementary
row operations. These combined operations are the basis to perform operations which
preserve similarity of matrices. They are applied later on to convert upper triangular
matrices into Jordan normal form.›
theory Column_Operations
imports
Gauss_Jordan_Elimination
begin
definition mat_multcol :: "nat ⇒ 'a :: semiring_1 ⇒ 'a mat ⇒ 'a mat" (‹multcol›) where
"multcol k a A = mat (dim_row A) (dim_col A)
(λ (i,j). if k = j then a * A $$ (i,j) else A $$ (i,j))"
definition mat_swapcols :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" (‹swapcols›)where
"swapcols k l A = mat (dim_row A) (dim_col A)
(λ (i,j). if k = j then A $$ (i,l) else if l = j then A $$ (i,k) else A $$ (i,j))"
definition mat_addcol_vec :: "nat ⇒ 'a :: plus vec ⇒ 'a mat ⇒ 'a mat" where
"mat_addcol_vec k v A = mat (dim_row A) (dim_col A)
(λ (i,j). if k = j then v $ i + A $$ (i,j) else A $$ (i,j))"
definition mat_addcol :: "'a :: semiring_1 ⇒ nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" (‹addcol›) where
"addcol a k l A = mat (dim_row A) (dim_col A)
(λ (i,j). if k = j then a * A $$ (i,l) + A $$ (i,j) else A $$ (i,j))"
lemma index_mat_multcol[simp]:
"i < dim_row A ⟹ j < dim_col A ⟹ multcol k a A $$ (i,j) = (if k = j then a * A $$ (i,j) else A $$ (i,j))"
"i < dim_row A ⟹ j < dim_col A ⟹ multcol j a A $$ (i,j) = a * A $$ (i,j)"
"i < dim_row A ⟹ j < dim_col A ⟹ k ≠ j ⟹ multcol k a A $$ (i,j) = A $$ (i,j)"
"dim_row (multcol k a A) = dim_row A" "dim_col (multcol k a A) = dim_col A"
unfolding mat_multcol_def by auto
lemma index_mat_swapcols[simp]:
"i < dim_row A ⟹ j < dim_col A ⟹ swapcols k l A $$ (i,j) = (if k = j then A $$ (i,l) else
if l = j then A $$ (i,k) else A $$ (i,j))"
"dim_row (swapcols k l A) = dim_row A" "dim_col (swapcols k l A) = dim_col A"
unfolding mat_swapcols_def by auto
lemma index_mat_addcol[simp]:
"i < dim_row A ⟹ j < dim_col A ⟹ addcol a k l A $$ (i,j) = (if k = j then
a * A $$ (i,l) + A $$ (i,j) else A $$ (i,j))"
"i < dim_row A ⟹ j < dim_col A ⟹ addcol a j l A $$ (i,j) = a * A $$(i,l) + A$$(i,j)"
"i < dim_row A ⟹ j < dim_col A ⟹ k ≠ j ⟹ addcol a k l A $$ (i,j) = A $$(i,j)"
"dim_row (addcol a k l A) = dim_row A" "dim_col (addcol a k l A) = dim_col A"
unfolding mat_addcol_def by auto
text ‹Each column-operation can be seen as a multiplication of
an elementary matrix from the right›
lemma col_addrow:
"l ≠ i ⟹ i < n ⟹ col (addrow_mat n a k l) i = unit_vec n i"
"k < n ⟹ l < n ⟹ col (addrow_mat n a k l) l = a ⋅⇩v unit_vec n k + unit_vec n l"
by (rule eq_vecI, auto)
lemma col_addcol[simp]:
"k < dim_col A ⟹ l < dim_col A ⟹ col (addcol a k l A) k = a ⋅⇩v col A l + col A k"
by (rule eq_vecI;simp)
lemma addcol_mat: assumes A: "A ∈ carrier_mat nr n"
and k: "k < n"
shows "addcol (a :: 'a :: comm_semiring_1) l k A = A * addrow_mat n a k l"
by (rule eq_matI, insert A k, auto simp: col_addrow
scalar_prod_add_distrib[of _ n] scalar_prod_smult_distrib[of _ n])
lemma col_multrow: "k ≠ i ⟹ i < n ⟹ col (multrow_mat n k a) i = unit_vec n i"
"k < n ⟹ col (multrow_mat n k a) k = a ⋅⇩v unit_vec n k"
by (rule eq_vecI, auto)
lemma multcol_mat: assumes A: "(A :: 'a :: comm_ring_1 mat) ∈ carrier_mat nr n"
shows "multcol k a A = A * multrow_mat n k a"
by (rule eq_matI, insert A, auto simp: col_multrow smult_scalar_prod_distrib[of _ n])
lemma col_swaprows:
"l < n ⟹ col (swaprows_mat n l l) l = unit_vec n l"
"i ≠ k ⟹ i ≠ l ⟹ i < n ⟹ col (swaprows_mat n k l) i = unit_vec n i"
"k < n ⟹ l < n ⟹ col (swaprows_mat n k l) l = unit_vec n k"
"k < n ⟹ l < n ⟹ col (swaprows_mat n k l) k = unit_vec n l"
by (rule eq_vecI, auto)
lemma swapcols_mat: assumes A: "A ∈ carrier_mat nr n" and k: "k < n" "l < n"
shows "swapcols k l A = A * swaprows_mat n k l"
by (rule eq_matI, insert A k, auto simp: col_swaprows)
text ‹Combining row and column-operations yields similarity transformations.›
definition add_col_sub_row :: "'a :: ring_1 ⇒ nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"add_col_sub_row a k l A = addrow (- a) k l (addcol a l k A)"
definition mult_col_div_row :: "'a :: field ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"mult_col_div_row a k A = multrow k (inverse a) (multcol k a A)"
definition swap_cols_rows :: "nat ⇒ nat ⇒ 'a mat ⇒ 'a mat" where
"swap_cols_rows k l A = swaprows k l (swapcols k l A)"
lemma add_col_sub_row_carrier[simp]:
"dim_row (add_col_sub_row a k l A) = dim_row A"
"dim_col (add_col_sub_row a k l A) = dim_col A"
"A ∈ carrier_mat n n ⟹ add_col_sub_row a k l A ∈ carrier_mat n n"
unfolding add_col_sub_row_def carrier_mat_def by auto
lemma add_col_sub_index_row[simp]:
"i < dim_row A ⟹ i < dim_col A ⟹ j < dim_row A ⟹ j < dim_col A ⟹ l < dim_row A
⟹ add_col_sub_row a k l A $$ (i,j) = (if
i = k ∧ j = l then A $$ (i, j) + a * A $$ (i, i) - a * a * A $$ (j, i) - a * A $$ (j, j) else if
i = k ∧ j ≠ l then A $$ (i, j) - a * A $$ (l, j) else if
i ≠ k ∧ j = l then A $$ (i, j) + a * A $$ (i, k) else A $$ (i,j))"
unfolding add_col_sub_row_def by (auto simp: field_simps)
lemma mult_col_div_index_row[simp]:
"i < dim_row A ⟹ i < dim_col A ⟹ j < dim_row A ⟹ j < dim_col A ⟹ a ≠ 0
⟹ mult_col_div_row a k A $$ (i,j) = (if
i = k ∧ j ≠ i then inverse a * A $$ (i, j) else if
j = k ∧ j ≠ i then a * A $$ (i, j) else A $$ (i,j))"
unfolding mult_col_div_row_def by auto
lemma mult_col_div_row_carrier[simp]:
"dim_row (mult_col_div_row a k A) = dim_row A"
"dim_col (mult_col_div_row a k A) = dim_col A"
"A ∈ carrier_mat n n ⟹ mult_col_div_row a k A ∈ carrier_mat n n"
unfolding mult_col_div_row_def carrier_mat_def by auto
lemma swap_cols_rows_carrier[simp]:
"dim_row (swap_cols_rows k l A) = dim_row A"
"dim_col (swap_cols_rows k l A) = dim_col A"
"A ∈ carrier_mat n n ⟹ swap_cols_rows k l A ∈ carrier_mat n n"
unfolding swap_cols_rows_def carrier_mat_def by auto
lemma swap_cols_rows_index[simp]:
"i < dim_row A ⟹ i < dim_col A ⟹ j < dim_row A ⟹ j < dim_col A ⟹ a < dim_row A ⟹ b < dim_row A
⟹ swap_cols_rows a b A $$ (i,j) = A $$ (if i = a then b else if i = b then a else i,
if j = a then b else if j = b then a else j)"
unfolding swap_cols_rows_def
by auto
lemma add_col_sub_row_similar: assumes A: "A ∈ carrier_mat n n" and kl: "k < n" "l < n" "k ≠ l"
shows "similar_mat (add_col_sub_row a k l A) (A :: 'a :: comm_ring_1 mat)"
proof (rule similar_matI)
let ?P = "addrow_mat n (-a) k l"
let ?Q = "addrow_mat n a k l"
let ?B = "add_col_sub_row a k l A"
show carr: "{?B, A, ?P, ?Q} ⊆ carrier_mat n n" using A by auto
show "?Q * ?P = 1⇩m n" by (rule addrow_mat_inv[OF kl])
show "?P * ?Q = 1⇩m n" using addrow_mat_inv[OF kl, of "-a"] by simp
have col: "addcol a l k A = A * ?Q"
by (rule addcol_mat[OF A kl(1)])
have "?B = ?P * (A * ?Q)" unfolding add_col_sub_row_def col
by (rule addrow_mat[OF _ kl(2), of _ n], insert A, simp)
thus "?B = ?P * A * ?Q" using carr by (simp add: assoc_mult_mat[of _ n n _ n _ n])
qed
lemma mult_col_div_row_similar: assumes A: "A ∈ carrier_mat n n" and ak: "k < n" "a ≠ 0"
shows "similar_mat (mult_col_div_row a k A) A"
proof (rule similar_matI)
let ?P = "multrow_mat n k (inverse a)"
let ?Q = "multrow_mat n k a"
let ?B = "mult_col_div_row a k A"
show carr: "{?B, A, ?P, ?Q} ⊆ carrier_mat n n" using A by auto
show "?Q * ?P = 1⇩m n" by (rule multrow_mat_inv[OF ak])
show "?P * ?Q = 1⇩m n" using multrow_mat_inv[OF ak(1), of "inverse a"] ak(2) by simp
have col: "multcol k a A = A * ?Q"
by (rule multcol_mat[OF A])
have "?B = ?P * (A * ?Q)" unfolding mult_col_div_row_def col
by (rule multrow_mat[of _ n n], insert A, simp)
thus "?B = ?P * A * ?Q" using carr by (simp add: assoc_mult_mat[of _ n n _ n _ n])
qed
lemma swap_cols_rows_similar: assumes A: "A ∈ carrier_mat n n" and kl: "k < n" "l < n"
shows "similar_mat (swap_cols_rows k l A) A"
proof (rule similar_matI)
let ?P = "swaprows_mat n k l"
let ?B = "swap_cols_rows k l A"
show carr: "{?B, A, ?P, ?P} ⊆ carrier_mat n n" using A by auto
show "?P * ?P = 1⇩m n" by (rule swaprows_mat_inv[OF kl])
show "?P * ?P = 1⇩m n" by fact
have col: "swapcols k l A = A * ?P"
by (rule swapcols_mat[OF A kl])
have "?B = ?P * (A * ?P)" unfolding swap_cols_rows_def col
by (rule swaprows_mat[of _ n n ], insert A kl, auto)
thus "?B = ?P * A * ?P" using carr by (simp add: assoc_mult_mat[of _ n n _ n _ n])
qed
lemma swapcols_carrier[simp]: "(swapcols l k A ∈ carrier_mat n m) = (A ∈ carrier_mat n m)"
unfolding mat_swapcols_def carrier_mat_def by auto
fun swap_row_to_front :: "'a mat ⇒ nat ⇒ 'a mat" where
"swap_row_to_front A 0 = A"
| "swap_row_to_front A (Suc I) = swap_row_to_front (swaprows I (Suc I) A) I"
fun swap_col_to_front :: "'a mat ⇒ nat ⇒ 'a mat" where
"swap_col_to_front A 0 = A"
| "swap_col_to_front A (Suc I) = swap_col_to_front (swapcols I (Suc I) A) I"
lemma swap_row_to_front_result: "A ∈ carrier_mat n m ⟹ I < n ⟹ swap_row_to_front A I =
mat n m (λ (i,j). if i = 0 then A $$ (I,j)
else if i ≤ I then A $$ (i - 1, j) else A $$ (i,j))"
proof (induct I arbitrary: A)
case 0
thus ?case
by (intro eq_matI, auto)
next
case (Suc I A)
from Suc(3) have I: "I < n" by auto
let ?I = "Suc I"
let ?A = "swaprows I ?I A"
have AA: "?A ∈ carrier_mat n m" using Suc(2) by simp
have "swap_row_to_front A (Suc I) = swap_row_to_front ?A I" by simp
also have "… = mat n m
(λ(i, j). if i = 0 then ?A $$ (I, j)
else if i ≤ I then ?A $$ (i - 1, j) else ?A $$ (i, j))"
using Suc(1)[OF AA I] by simp
also have "… = mat n m
(λ(i, j). if i = 0 then A $$ (?I, j)
else if i ≤ ?I then A $$ (i - 1, j) else A $$ (i, j))"
by (rule eq_matI, insert I Suc(2), auto)
finally show ?case .
qed
lemma swap_col_to_front_result: "A ∈ carrier_mat n m ⟹ J < m ⟹ swap_col_to_front A J =
mat n m (λ (i,j). if j = 0 then A $$ (i,J)
else if j ≤ J then A $$ (i, j-1) else A $$ (i,j))"
proof (induct J arbitrary: A)
case 0
thus ?case
by (intro eq_matI, auto)
next
case (Suc J A)
from Suc(3) have J: "J < m" by auto
let ?J = "Suc J"
let ?A = "swapcols J ?J A"
have AA: "?A ∈ carrier_mat n m" using Suc(2) by simp
have "swap_col_to_front A (Suc J) = swap_col_to_front ?A J" by simp
also have "… = mat n m
(λ(i, j). if j = 0 then ?A $$ (i, J)
else if j ≤ J then ?A $$ (i, j - 1) else ?A $$ (i, j))"
using Suc(1)[OF AA J] by simp
also have "… = mat n m
(λ(i, j). if j = 0 then A $$ (i, ?J)
else if j ≤ ?J then A $$ (i, j - 1) else A $$ (i, j))"
by (rule eq_matI, insert J Suc(2), auto)
finally show ?case .
qed
lemma swapcols_is_transp_swap_rows: assumes A: "A ∈ carrier_mat n m" "k < m" "l < m"
shows "swapcols k l A = transpose_mat (swaprows k l (transpose_mat A))"
using assms by (intro eq_matI, auto)
end