Theory Column_Operations

theory Column_Operations
imports Gauss_Jordan_Elimination
(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
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 = 1m n" by (rule addrow_mat_inv[OF kl])
  show "?P * ?Q = 1m 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 = 1m n" by (rule multrow_mat_inv[OF ak])
  show "?P * ?Q = 1m 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 = 1m n" by (rule swaprows_mat_inv[OF kl])
  show "?P * ?P = 1m 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

(* THIS LINE SEPARATES AFP-ENTRY FROM NEWER DEVELOPMENTS *)

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