Theory Gauss_Jordan.Elementary_Operations

(*  
    Title:      Elementary_Operations.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

section‹Elementary Operations over matrices›

theory Elementary_Operations
imports 
  Rank_Nullity_Theorem.Fundamental_Subspaces
  Code_Matrix
begin

subsection‹Some previous results:›

lemma mat_1_fun: "mat 1 $ a $ b = (λi j. if i=j then 1 else 0) a b" unfolding mat_def by auto

lemma mat1_sum_eq:
  shows "(kUNIV. mat (1::'a::{semiring_1}) $ s $ k * mat 1 $ k $ t) = mat 1 $ s $ t"
proof (unfold mat_def, auto)
  let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))"
  have univ_eq: "UNIV = (UNIV - {t})  {t}" by fast
  have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
  also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
  also have "... = 0 + sum ?f {t}" by auto
  also have "... = sum ?f {t}" by simp
  also have "... = 1" by simp
  finally show "sum ?f UNIV = 1" .
next
  assume s_not_t: "s  t"
  let ?g="λk. (if s = k then 1::'a else 0) * (if k = t then 1 else 0)"
  have "sum ?g UNIV = sum (λk. 0::'a) (UNIV::'b set)" by (rule sum.cong, auto simp add: s_not_t)
  also have "... = 0" by simp
  finally show "sum ?g UNIV = 0" .
qed


lemma invertible_mat_n:
  fixes n::"'a::{field}"
  assumes n: "n  0"
  shows "invertible ((mat n)::'a^'n^'n)"
proof (unfold invertible_def, rule exI[of _ "mat (inverse n)"], rule conjI)
  show "mat n ** mat (inverse n) = (mat 1::'a^'n^'n)"
  proof (unfold matrix_matrix_mult_def mat_def, vector, auto)
    fix ia::'n
    let ?f="(λk. (if ia = k then n else 0) * (if k = ia then inverse n else 0))"
    have UNIV_rw: "(UNIV::'n set) = insert ia (UNIV-{ia})" by auto
    have "(k(UNIV::'n set). (if ia = k then n else 0) * (if k = ia then inverse n else 0)) = 
      (kinsert ia (UNIV-{ia}). (if ia = k then n else 0) * (if k = ia then inverse n else 0))" using UNIV_rw by simp
    also have "... = ?f ia + sum ?f (UNIV-{ia})"
    proof (rule sum.insert)
      show "finite (UNIV - {ia})"  using finite_UNIV by fastforce
      show "ia  UNIV - {ia}" by fast
    qed
    also have "... = 1" using right_inverse[OF n] by simp
    finally show " (k(UNIV::'n set). (if ia = k then n else 0) * (if k = ia then inverse n else 0)) = (1::'a)" .
    fix i::'n
    assume i_not_ia: "i  ia"
    show "(k(UNIV::'n set). (if i = k then n else 0) * (if k = ia then inverse n else 0)) = 0" by (rule sum.neutral, simp add: i_not_ia)
  qed
next
  show "mat (inverse n) ** mat n = ((mat 1)::'a^'n^'n)"
  proof (unfold matrix_matrix_mult_def mat_def, vector, auto)
    fix ia::'n
    let ?f=" (λk. (if ia = k then inverse n else 0) * (if k = ia then n else 0))"
    have UNIV_rw: "(UNIV::'n set) = insert ia (UNIV-{ia})" by auto
    have "(k(UNIV::'n set). (if ia = k then inverse n else 0) * (if k = ia then n else 0)) = 
      (kinsert ia (UNIV-{ia}). (if ia = k then inverse n else 0) * (if k = ia then n else 0))" using UNIV_rw by simp
    also have "... = ?f ia + sum ?f (UNIV-{ia})"
    proof (rule sum.insert)
      show "finite (UNIV - {ia})"  using finite_UNIV by fastforce
      show "ia  UNIV - {ia}" by fast
    qed
    also have "... = 1" using left_inverse[OF n] by simp
    finally show " (k(UNIV::'n set). (if ia = k then inverse n else 0) * (if k = ia then n else 0)) = (1::'a)" .
    fix i::'n
    assume i_not_ia: "i  ia"
    show "(k(UNIV::'n set). (if i = k then inverse n else 0) * (if k = ia then n else 0)) = 0" by (rule sum.neutral, simp add: i_not_ia)
  qed
qed

corollary invertible_mat_1:
  shows "invertible (mat (1::'a::{field}))" by (metis invertible_mat_n zero_neq_one)

subsection‹Definitions of elementary row and column operations›

text‹Definitions of elementary row operations›

definition interchange_rows :: "'a ^'n^'m => 'm => 'm  'a ^'n^'m"
  where "interchange_rows A a b = (χ i j. if i=a then A $ b $ j else if i=b then A $ a $ j else A $ i $ j)"

definition mult_row :: "('a::times) ^'n^'m => 'm => 'a  'a ^'n^'m"
  where "mult_row A a q = (χ i j. if i=a then q*(A $ a $ j) else A $ i $ j)"

definition row_add :: "('a::{plus, times}) ^'n^'m => 'm => 'm  'a  'a ^'n^'m"
  where "row_add A a b q = (χ i j. if i=a then (A $ a $ j) + q*(A $ b $ j) else A $ i $ j)"

text‹Definitions of elementary column operations›

definition interchange_columns :: "'a ^'n^'m => 'n => 'n  'a ^'n^'m"
  where "interchange_columns A n m = (χ i j. if j=n then A $ i $ m else if j=m then A $ i $ n else A $ i $ j)"

definition mult_column :: "('a::times) ^'n^'m => 'n => 'a  'a ^'n^'m"
  where " mult_column A n q = (χ i j. if j=n then (A $ i $ j)*q else A $ i $ j)"

definition column_add :: "('a::{plus, times}) ^'n^'m => 'n => 'n  'a  'a ^'n^'m"
  where "column_add A n m q = (χ i j. if j=n then ((A $ i $ n) + (A $ i $ m)*q) else A $ i $ j)"

subsection‹Properties about elementary row operations›
subsubsection‹Properties about interchanging rows›

text‹Properties about @{term "interchange_rows"}

lemma interchange_same_rows: "interchange_rows A a a = A"
  unfolding interchange_rows_def by vector

lemma interchange_rows_i[simp]: "interchange_rows A i j $ i = A $ j"
  unfolding interchange_rows_def by vector

lemma interchange_rows_j[simp]: "interchange_rows A i j $ j = A $ i"
  unfolding interchange_rows_def by vector

lemma interchange_rows_preserves:
  assumes "i  a" and "j  a"
  shows "interchange_rows A i j $ a = A $ a"
  using assms unfolding interchange_rows_def by vector

lemma interchange_rows_mat_1:
  shows "interchange_rows (mat 1) a b ** A = interchange_rows A a b"
proof (unfold matrix_matrix_mult_def interchange_rows_def, vector, auto)
  fix ia
  let ?f="(λk. mat (1::'a) $ a $ k * A $ k $ ia)"
  have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
  have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
  also have "... = sum ?f (UNIV-{a}) + sum ?f {a}"
  proof (rule sum.union_disjoint)
    show "finite (UNIV - {a})" by (metis finite_code) 
    show "finite {a}" by simp
    show "(UNIV - {a})  {a} = {}" by simp
  qed
  also have "... = sum ?f {a}" unfolding mat_def by auto
  also have "... = ?f a" by auto
  also have "... = A $ a $ ia" unfolding mat_def by auto
  finally show "(kUNIV. mat (1::'a) $ a $ k * A $ k $ ia) = A $ a $ ia" .
  assume i: " a  b"
  let ?g= "λk. mat (1::'a) $ b $ k * A $ k $ ia"
  have univ_rw':"UNIV = (UNIV-{b})  {b}" by auto
  have "sum ?g UNIV = sum ?g ((UNIV-{b})  {b})" using univ_rw' by auto
  also have "... = sum ?g (UNIV-{b}) + sum ?g {b}" by (rule sum.union_disjoint, auto)
  also have "... = sum ?g {b}"  unfolding mat_def by auto
  also have "... = ?g b" by simp
  finally show "(kUNIV. mat (1::'a) $ b $ k * A $ k $ ia) = A $ b $ ia" unfolding mat_def by simp
next
  fix i j
  assume ib: "i  b" and ia:"i  a"
  let ?h="λk. mat (1::'a) $ i $ k * A $ k $ j"
  have univ_rw'':"UNIV = (UNIV-{i})  {i}" by auto
  have "sum ?h UNIV = sum ?h ((UNIV-{i})  {i})" using univ_rw'' by auto
  also have "... = sum ?h (UNIV-{i}) + sum ?h {i}"  by (rule sum.union_disjoint, auto)
  also have "... =  sum ?h {i}" unfolding mat_def by auto  
  also have "... = ?h i" by simp
  finally show " (kUNIV. mat (1::'a) $ i $ k * A $ k $ j) = A $ i $ j" unfolding mat_def by auto
qed

lemma invertible_interchange_rows: "invertible (interchange_rows (mat 1) a b)"
proof (unfold invertible_def, rule exI[of _ "interchange_rows (mat 1) a b"], simp, unfold matrix_matrix_mult_def, vector, clarify, 
    unfold interchange_rows_def, vector, unfold mat_1_fun, auto+) 
  fix s t::"'b"   
  assume s_not_t: "s  t"
  show " (k::'bUNIV. (if s = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a))) = (0::'a)"
    by (rule sum.neutral, simp add: s_not_t)
  assume b_not_t: "b  t"
  show "(kUNIV. (if s = b then if t = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
    (if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a))) =
    (0::'a)" by (rule sum.neutral, simp)
  assume a_not_t: "a  t"
  show "(kUNIV. (if s = a then if b = k then 1::'a else (0::'a) else if s = b then if a = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
    (if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a))) =
    (0::'a)" by (rule sum.neutral, auto simp add: s_not_t)
next
  fix s t::"'b"
  assume a_noteq_t: "at" and s_noteq_t: "s  t"
  show " (kUNIV. (if s = a then if t = k then 1::'a else (0::'a) else if s = t then if a = k then 1::'a else (0::'a) else if s = k then 1::'a else (0::'a)) *
    (if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))) =
    (0::'a)" apply (rule sum.neutral) using s_noteq_t by fastforce
next
  fix s t::"'b"
  show "(kUNIV. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
  proof - 
    let ?f="(λk. (if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else if k = t then 1::'a else if k = t then 1::'a else (0::'a)))"
    have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
    have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
    also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
    also have "... = 0 + sum ?f {t}" by auto
    also have "... = sum ?f {t}" by simp
    also have "... = 1" by simp
    finally show ?thesis .
  qed
next
  fix s t::"'b"
  assume b_noteq_t: "b  t"
  show " (kUNIV. (if b = k then 1::'a else (0::'a)) * (if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="(λk. (if b = k then 1::'a else (0::'a)) * (if k = t then 0::'a else if k = b then 1::'a else if k = t then 1::'a else (0::'a)))"
    have univ_eq: "UNIV = ((UNIV - {b})  {b})" by auto
    have "sum ?f UNIV = sum ?f ((UNIV - {b})  {b}) " using univ_eq by simp
    also have "... = sum ?f (UNIV - {b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
    also have "... = 0 + sum ?f {b}" by auto
    also have "... = sum ?f {b}" by simp
    also have "... = 1" using b_noteq_t by simp
    finally show ?thesis .
  qed
  assume a_noteq_t: "at"
  show " (kUNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="(λk.  (if t = k then 1::'a else (0::'a)) * (if k = a then 0::'a else if k = b then 0::'a else if k = t then 1::'a else (0::'a)))"
    have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
    have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
    also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
    also have "... = 0 + sum ?f {t}" by auto
    also have "... = sum ?f {t}" by simp
    also have "... = 1" using b_noteq_t a_noteq_t by simp
    finally show ?thesis .
  qed
next
  fix s t::"'b"
  assume a_noteq_t: "at"
  show "(kUNIV. (if a = k then 1::'a else (0::'a)) * (if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="λk.  (if a = k then 1::'a else (0::'a)) * (if k = a then 1::'a else if k = t then 0::'a else if k = t then 1::'a else (0::'a))"
    have univ_eq: "UNIV = ((UNIV - {a})  {a})" by auto
    have "sum ?f UNIV = sum ?f ((UNIV - {a})  {a}) " using univ_eq by simp
    also have "... = sum ?f (UNIV - {a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
    also have "... = 0 + sum ?f {a}" by auto
    also have "... = sum ?f {a}" by simp
    also have "... = 1" using a_noteq_t by simp
    finally show ?thesis .    
  qed
qed

subsubsection‹Properties about multiplying a row by a constant›
text‹Properties about @{term "mult_row"}

lemma mult_row_mat_1: "mult_row (mat 1) a q ** A = mult_row A a q"
proof (unfold matrix_matrix_mult_def mult_row_def, vector, auto)
  fix ia
  let ?f="λk. q * mat (1::'a) $ a $ k * A $ k $ ia"
  have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
  have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
  also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
  also have "... = sum ?f {a}" unfolding mat_def by auto  
  also have "... = ?f a" by auto
  also have "... = q * A $ a $ ia" unfolding mat_def by auto
  finally show  "(kUNIV. q * mat (1::'a) $ a $ k * A $ k $ ia) = q * A $ a $ ia" .
  fix i
  assume i: "i  a"
  let ?g="λk. mat (1::'a) $ i $ k * A $ k $ ia"
  have univ_rw'':"UNIV = (UNIV-{i})  {i}" by auto
  have "sum ?g UNIV = sum ?g ((UNIV-{i})  {i})" using univ_rw'' by auto
  also have "... = sum ?g (UNIV-{i}) + sum ?g {i}"  by (rule sum.union_disjoint, auto)
  also have "... =  sum ?g {i}" unfolding mat_def by auto 
  also have "... = ?g i" by simp
  finally show "(kUNIV. mat (1::'a) $ i $ k * A $ k $ ia) = A $ i $ ia" unfolding mat_def by simp
qed

lemma invertible_mult_row:
  assumes qk: "q * k = 1" and kq: "k*q=1"
  shows "invertible (mult_row (mat 1) a q)"
proof (unfold invertible_def, rule exI[of _ "mult_row (mat 1) a k"],rule conjI)
  show "mult_row (mat (1::'a)) a q ** mult_row (mat (1::'a)) a k = mat (1::'a)"
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_row_def, vector, unfold mat_1_fun, auto)
    show "(kaUNIV. q * (if a = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λka. q * (if a = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else (0::'a)) "
      have univ_eq: "UNIV = ((UNIV - {a})  {a})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {a})  {a}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {a}" by auto
      also have "... = sum ?f {a}" by simp
      also have "... = 1" using qk by simp
      finally show ?thesis .        
    qed
  next
    fix s
    assume s_noteq_a: "sa"
    show "(kaUNIV. (if s = ka then 1::'a else (0::'a)) * (if ka = a then k * (1::'a) else if ka = a then 1::'a else 0)) = 0"
      by (rule sum.neutral, simp add: s_noteq_a)
  next
    fix t
    assume a_noteq_t: "at"
    show "(kaUNIV. (if t = ka then 1::'a else (0::'a)) * (if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λka. (if t = ka then 1::'a else (0::'a)) * (if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a)) "
      have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {t}" by simp
      also have "... = 1" using a_noteq_t by auto
      finally show ?thesis .
    qed            
    fix s
    assume s_not_t: "st"
    show "(kaUNIV. (if s = a then q * (if a = ka then 1::'a else (0::'a)) else if s = ka then 1::'a else (0::'a)) *
      (if ka = a then k * (0::'a) else if ka = t then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, simp add: s_not_t a_noteq_t)
  qed            
  show "mult_row (mat (1::'a)) a k ** mult_row (mat (1::'a)) a q = mat (1::'a)"
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_row_def, vector, unfold mat_1_fun, auto)
    show "(kaUNIV. k * (if a = ka then 1::'a else (0::'a)) * (if ka = a then q * (1::'a) else if ka = a then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λka. k * (if a = ka then 1::'a else (0::'a)) * (if ka = a then q * (1::'a) else if ka = a then 1::'a else (0::'a)) "
      have univ_eq: "UNIV = ((UNIV - {a})  {a})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {a})  {a}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {a}" by auto
      also have "... = sum ?f {a}" by simp
      also have "... = 1" using kq by simp
      finally show ?thesis .        
    qed
  next
    fix s
    assume s_not_a: "sa"
    show "(kUNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then q * (1::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, simp add: s_not_a)
  next
    fix t
    assume a_not_t: "at"
    show "(kUNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then q * (0::'a) else if k = t then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {t}" by simp
      also have "... = 1" using a_not_t by simp
      finally show ?thesis .
    qed
    fix s
    assume s_not_t: "st"
    show " (kaUNIV. (if s = a then k * (if a = ka then 1::'a else (0::'a)) else if s = ka then 1::'a else (0::'a)) *
      (if ka = a then q * (0::'a) else if ka = t then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, simp add: s_not_t)    
  qed
qed

corollary invertible_mult_row':
  assumes q_not_zero: "q  0"
  shows "invertible (mult_row (mat (1::'a::{field})) a q)"
  by (simp add: invertible_mult_row[of q "inverse q"] q_not_zero)

subsubsection‹Properties about adding a row multiplied by a constant to another row›
text‹Properties about @{term "row_add"}

lemma row_add_mat_1: "row_add (mat 1) a b q ** A = row_add A a b q"
proof (unfold matrix_matrix_mult_def row_add_def, vector, auto)
  fix j
  let ?f=" (λk. (mat (1::'a) $ a $ k + q * mat (1::'a) $ b $ k) * A $ k $ j)"
  show "sum ?f UNIV = A $ a $ j + q * A $ b $ j"
  proof (cases "a=b")
    case False
    have univ_rw: "UNIV = {a}  ({b}  (UNIV - {a} - {b}))" by auto
    have sum_rw: "sum ?f ({b}  (UNIV - {a} - {b})) = sum ?f {b} + sum ?f (UNIV - {a} - {b})" by (rule sum.union_disjoint, auto simp add: False)
    have "sum ?f UNIV = sum ?f ({a}  ({b}  (UNIV - {a} - {b})))" using univ_rw by simp
    also have "... = sum ?f {a} + sum ?f ({b}  (UNIV - {a} - {b}))" by (rule sum.union_disjoint, auto simp add: False)
    also have "... = sum ?f {a} + sum ?f {b} + sum ?f (UNIV - {a} - {b})" unfolding sum_rw add.assoc ..
    also have "... = sum ?f {a} + sum ?f {b}"
    proof -
      have "sum ?f (UNIV - {a} - {b}) = sum (λk. 0) (UNIV - {a} - {b})" unfolding mat_def by (rule sum.cong, auto)
      also have "... = 0" unfolding sum.neutral_const ..
      finally show ?thesis by simp
    qed
    also have "... = A $ a $ j + q * A $ b $ j" using False unfolding mat_def by simp
    finally show ?thesis .
  next
    case True
    have univ_rw: "UNIV = {b}  (UNIV - {b})" by auto
    have "sum ?f UNIV = sum ?f ({b}  (UNIV - {b}))" using univ_rw by simp
    also have "... = sum ?f {b} + sum ?f (UNIV  - {b})" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {b}"
    proof -
      have "sum ?f (UNIV - {b}) = sum (λk. 0) (UNIV - {b})" using True unfolding mat_def by auto
      also have "... = 0" unfolding sum.neutral_const ..
      finally show ?thesis by simp
    qed
    also have "... = A $ a $ j + q * A $ b $ j" 
      by (unfold True mat_def, simp, metis (opaque_lifting, no_types) vector_add_component vector_sadd_rdistrib vector_smult_component vector_smult_lid)
    finally show ?thesis .
  qed
  fix i assume i: "ia"
  let ?g="λk.  mat (1::'a) $ i $ k * A $ k $ j"
  have univ_rw: "UNIV = {i}  (UNIV - {i})" by auto
  have "sum ?g UNIV = sum ?g ({i}  (UNIV - {i}))" using univ_rw by simp
  also have "... = sum ?g {i} + sum ?g (UNIV - {i})" by (rule sum.union_disjoint, auto)
  also have "... = sum ?g {i}"
  proof -
    have "sum ?g (UNIV - {i}) = sum (λk. 0) (UNIV - {i})" unfolding mat_def by auto
    also have "... = 0" unfolding sum.neutral_const ..
    finally show ?thesis by simp
  qed
  also have "... =  A $ i $ j" unfolding mat_def by simp
  finally show "(kUNIV. mat (1::'a) $ i $ k * A $ k $ j) = A $ i $ j" .
qed

lemma invertible_row_add:
  assumes a_noteq_b: "ab"
  shows "invertible (row_add (mat (1::'a::{ring_1})) a b q)"
proof (unfold invertible_def, rule exI[of _ "(row_add (mat 1) a b (-q))"], rule conjI)
  show "row_add (mat (1::'a)) a b q ** row_add (mat (1::'a)) a b (- q) = mat (1::'a)" using a_noteq_b
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold row_add_def, vector, unfold mat_1_fun, auto)
    show " (k::'bUNIV. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {b})  {b})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {b})  {b}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {b}" by auto
      also have "... = sum ?f {b}" by simp
      also have "... = 1" using a_noteq_b by simp
      finally show ?thesis .
    qed
    show "(k::'bUNIV. ((if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a))) * (if k = a then (1::'a) + - 
      q * (0::'a) else if k = a then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk.  ((if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a))) * (if k = a then (1::'a) + - 
        q * (0::'a) else if k = a then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {a})  {a})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {a})  {a}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {a}" by auto
      also have "... = sum ?f {a}" by simp
      also have "... = 1" using a_noteq_b by simp
      finally show ?thesis .
    qed
  next
    fix s
    assume s_not_a: "s  a"
    show "(k::'bUNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then (1::'a) + - q * (0::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, auto simp add: s_not_a)       
  next
    fix t
    assume b_not_t: "b  t" and a_not_t: "a  t"
    show "(kUNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a)) "
      have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {t}" by auto
      also have "... = sum ?f {t}" by simp
      also have "... = 1" using b_not_t a_not_t by simp
      finally show ?thesis .
    qed
  next     
    fix s t
    assume  b_not_t: "b  t" and a_not_t: "a  t" and  s_not_t: "s  t"
    show " (kUNIV. (if s = a then (if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
      (if k = a then (0::'a) + - q * (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)" by (rule sum.neutral, auto simp add: b_not_t a_not_t s_not_t)     
  next         
    fix s
    assume s_not_b: "sb"
    let ?f="λk. (if s = a then (if a = k then 1::'a else (0::'a)) + q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
      (if k = a then (0::'a) + - q * (1::'a) else if k = b then 1::'a else (0::'a))"
    show "sum ?f UNIV = (0::'a)"         
    proof (cases "s=a")         
      case False
      show ?thesis by (rule sum.neutral, auto simp add: False s_not_b a_noteq_b)
    next         
      case True ― ‹This case is different from the other cases›                  
      have univ_eq: "UNIV = ((UNIV - {a}- {b})  ({b}  {a}))" by auto
      have sum_a: "sum ?f {a} = -q"  unfolding True using s_not_b using a_noteq_b by auto
      have sum_b: "sum ?f {b} = q" unfolding True using s_not_b using a_noteq_b by auto
      have sum_rest: "sum ?f (UNIV - {a} - {b}) = 0"  by (rule sum.neutral, auto simp add: True s_not_b a_noteq_b)
      have "sum ?f UNIV = sum ?f ((UNIV - {a}- {b})  ({b}  {a}))"  using univ_eq by simp
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f ({b}  {a})" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f {b} + sum ?f {a}" by (auto simp add: sum.union_disjoint a_noteq_b)     
      also have "... = 0" unfolding sum_a sum_b sum_rest by simp
      finally show ?thesis .
    qed
  qed
next
  show "row_add (mat (1::'a)) a b (- q) ** row_add (mat (1::'a)) a b q = mat (1::'a)" using a_noteq_b
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold row_add_def, vector, unfold mat_1_fun, auto)     
    show "(kUNIV. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if b = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {b})  {b})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {b})  {b}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {b}" by auto
      also have "... = sum ?f {b}" by simp
      also have "... = 1" using a_noteq_b by simp
      finally show ?thesis .
    qed
  next
    show "(kUNIV. ((if a = k then 1 else 0) - q * (if b = k then 1 else 0)) * (if k = a then 1 + q * 0 else if k = a then 1 else 0)) = 1"
    proof -
      let ?f="λk. ((if a = k then 1::'a else (0::'a)) + - (q * (if b = k then 1::'a else (0::'a)))) * (if k = a then (1::'a) + q * (0::'a) else if k = a then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {a})  {a})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {a})  {a}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {a}" by auto
      also have "... = sum ?f {a}" by simp
      also have "... = 1" using a_noteq_b by simp
      finally show ?thesis by simp
    qed
  next
    fix s
    assume s_not_a: "sa"
    show "(kUNIV. (if s = k then 1::'a else (0::'a)) * (if k = a then (1::'a) + q * (0::'a) else if k = a then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, auto simp add: s_not_a)
  next 
    fix t
    assume b_not_t: "b  t" and a_not_t: "a  t"
    show "(kUNIV. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if t = k then 1::'a else (0::'a)) * (if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {t})  {t})" by auto
      have "sum ?f UNIV = sum ?f ((UNIV - {t})  {t}) " using univ_eq by simp
      also have "... = sum ?f (UNIV - {t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = 0 + sum ?f {t}" by auto
      also have "... = sum ?f {t}" by simp
      also have "... = 1" using b_not_t a_not_t by simp
      finally show ?thesis .
    qed
  next
    fix s t
    assume b_not_t: "b  t" and a_not_t: "a  t" and s_not_t: "s  t"     
    show "(kUNIV. (if s = a then (if a = k then 1::'a else (0::'a)) + - q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) *
      (if k = a then (0::'a) + q * (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, auto simp add: b_not_t a_not_t s_not_t)
  next
    fix s
    assume s_not_b: "sb"
    let ?f="λk.(if s = a then (if a = k then 1::'a else (0::'a)) + - q * (if b = k then 1::'a else (0::'a)) else if s = k then 1::'a else (0::'a)) 
      * (if k = a then (0::'a) + q * (1::'a) else if k = b then 1::'a else (0::'a))"
    show "sum ?f UNIV = 0"
    proof (cases "s=a")         
      case False
      show ?thesis by (rule sum.neutral, auto simp add: False s_not_b a_noteq_b)
    next         
      case True ― ‹This case is different from the other cases›                  
      have univ_eq: "UNIV = ((UNIV - {a}- {b})  ({b}  {a}))" by auto
      have sum_a: "sum ?f {a} = q"  unfolding True using s_not_b using a_noteq_b by auto
      have sum_b: "sum ?f {b} = -q" unfolding True using s_not_b using a_noteq_b by auto
      have sum_rest: "sum ?f (UNIV - {a} - {b}) = 0"  by (rule sum.neutral, auto simp add: True s_not_b a_noteq_b)
      have "sum ?f UNIV = sum ?f ((UNIV - {a}- {b})  ({b}  {a}))"  using univ_eq by simp
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f ({b}  {a})" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f {b} + sum ?f {a}" by (auto simp add: sum.union_disjoint a_noteq_b)
      also have "... = 0" unfolding sum_a sum_b sum_rest by simp
      finally show ?thesis .
    qed
  qed
qed

subsection‹Properties about elementary column operations›
subsubsection‹Properties about interchanging columns›
text‹Properties about @{term "interchange_columns"}

lemma interchange_columns_mat_1: "A ** interchange_columns (mat 1) a b = interchange_columns A a b"
proof (unfold matrix_matrix_mult_def, unfold interchange_columns_def, vector, auto) 
  fix i  
  show "(kUNIV. A $ i $ k * mat (1::'a) $ k $ a) = A $ i $ a"
  proof -
    let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ a)"
    have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {a}" unfolding mat_def by auto
    finally show ?thesis unfolding mat_def by simp
  qed    
  assume a_not_b: "ab"
  show " (kUNIV. A $ i $ k * mat (1::'a) $ k $ b) = A $ i $ b"
  proof -
    let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ b)"
    have univ_rw:"UNIV = (UNIV-{b})  {b}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{b})  {b})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {b}" unfolding mat_def by auto
    finally show ?thesis unfolding mat_def by simp
  qed
next
  fix i j
  assume j_not_b: "j  b" and j_not_a: "j  a"
  show "(kUNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
  proof -
    let ?f="(λk. A $ i $ k * mat (1::'a) $ k $ j)"
    have univ_rw:"UNIV = (UNIV-{j})  {j}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{j})  {j})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{j}) + sum ?f {j}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {j}" unfolding mat_def using j_not_b j_not_a by auto
    finally show ?thesis unfolding mat_def by simp
  qed
qed

lemma invertible_interchange_columns: "invertible (interchange_columns (mat 1) a b)"
proof (unfold invertible_def, rule exI[of _ "interchange_columns (mat 1) a b"], simp, unfold matrix_matrix_mult_def, vector, clarify, 
    unfold interchange_columns_def, vector, unfold mat_1_fun, auto+) 
  show "(kUNIV. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="(λk. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a)))"
    have univ_rw:"UNIV = (UNIV-{b})  {b}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{b})  {b})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {b}" by auto
    finally show ?thesis by simp
  qed
  assume a_not_b: "a  b"
  show "(kUNIV. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="λk. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
    have univ_rw:"UNIV = (UNIV-{b})  {b}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{b})  {b})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {b}" using a_not_b by simp
    finally show ?thesis using a_not_b by auto
  qed
next
  fix t
  assume b_not_t: "b  t"
  show " (kUNIV. (if k = b then 1::'a else if k = b then 1::'a else if b = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))) = (0::'a)"
    apply (rule sum.neutral) using b_not_t by auto
  assume b_not_a: "b  a"
  show "(kUNIV. (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) *
    (if t = a then if k = b then 1::'a else (0::'a) else if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) =
    (0::'a)" apply (rule sum.neutral) using b_not_t by auto
next
  fix t
  assume a_not_b: "a  b" and a_not_t: "a  t"
  show "(kUNIV. (if k = a then 0::'a else if k = b then 1::'a else if a = k then 1::'a else (0::'a)) *
    (if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) = (0::'a)"
    by (rule sum.neutral, auto simp add: a_not_b a_not_t)
next
  assume b_not_a: "b  a"
  show "(kUNIV. (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) * (if k = a then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="λk.  (if k = a then 1::'a else if k = b then 0::'a else if b = k then 1::'a else (0::'a)) * (if k = a then 1::'a else (0::'a))"
    have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {a}" using b_not_a by simp
    finally show ?thesis using b_not_a by auto
  qed
next
  fix t
  assume t_not_a: "t  a" and t_not_b: "t  b"
  show "(kUNIV. (if k = a then 0::'a else if k = b then 0::'a else if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))) = (1::'a)"
  proof -
    let ?f="λk. (if k = a then 0::'a else if k = b then 0::'a else if t = k then 1::'a else (0::'a)) * (if k = t then 1::'a else (0::'a))"
    have univ_rw:"UNIV = (UNIV-{t})  {t}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{t})  {t})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {t}" using t_not_a t_not_b by simp
    also have "... = 1"  using t_not_a t_not_b by simp
    finally show ?thesis .
  qed
next
  fix s t
  assume s_not_a: "s  a" and s_not_b: "s  b" and s_not_t: "s  t"
  show "(kUNIV. (if k = a then 0::'a else if k = b then 0::'a else if s = k then 1::'a else (0::'a)) *
    (if t = a then if k = b then 1::'a else (0::'a) else if t = b then if k = a then 1::'a else (0::'a) else if k = t then 1::'a else (0::'a))) =
    (0::'a)"
    by (rule sum.neutral, auto simp add: s_not_a s_not_b s_not_t)
qed

subsubsection‹Properties about multiplying a column by a constant›
text‹Properties about @{term "mult_column"}

lemma mult_column_mat_1: "A ** mult_column (mat 1) a q = mult_column A a q"
proof (unfold matrix_matrix_mult_def, unfold mult_column_def, vector, auto)
  fix i
  show "(kUNIV. A $ i $ k * (mat (1::'a) $ k $ a * q)) = A $ i $ a * q"
  proof -
    let ?f="λk.  A $ i $ k * (mat (1::'a) $ k $ a * q)"
    have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {a}" unfolding mat_def by auto
    also have "... = A $ i $ a * q" unfolding mat_def by auto
    finally show ?thesis .
  qed
  fix j
  show "(kUNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
  proof -
    let ?f="λk. A $ i $ k * mat (1::'a) $ k $ j"
    have univ_rw:"UNIV = (UNIV-{j})  {j}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{j})  {j})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{j}) + sum ?f {j}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {j}" unfolding mat_def by auto
    also have "... = A $ i $ j" unfolding mat_def by auto
    finally show ?thesis .
  qed
qed

lemma invertible_mult_column:
  assumes qk: "q * k = 1" and kq: "k * q = 1"
  shows "invertible (mult_column (mat 1) a q)"
proof (unfold invertible_def, rule exI[of _ "mult_column (mat 1) a k"], rule conjI)  
  show "mult_column (mat 1) a q ** mult_column (mat 1) a k = mat 1" 
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_column_def, vector, unfold mat_1_fun, auto)
    fix t    
    show "(kaUNIV. (if ka = a then (if t = ka then 1::'a else (0::'a)) * q else if t = ka then 1::'a else (0::'a)) *
      (if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))) =
      (1::'a)"
    proof -
      let ?f=" λka. (if ka = a then (if t = ka then 1::'a else (0::'a)) * q else if t = ka then 1::'a else (0::'a)) *
        (if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{t})  {t}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{t})  {t})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {t}" by auto
      also have "... = 1" using qk by auto
      finally show ?thesis .     
    qed   
    fix s
    assume s_not_t: "s  t"
    show "(kaUNIV. (if ka = a then (if s = ka then 1::'a else (0::'a)) * q else if s = ka then 1::'a else (0::'a)) *
      (if t = a then (if ka = t then 1::'a else (0::'a)) * k else if ka = t then 1::'a else (0::'a))) =
      (0::'a)"
      apply (rule sum.neutral) using s_not_t by auto
  qed       
  show "mult_column (mat (1::'a)) a k ** mult_column (mat (1::'a)) a q = mat (1::'a)"
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold mult_column_def, vector, unfold mat_1_fun, auto)
    fix t
    show "(kaUNIV. (if ka = a then (if t = ka then 1::'a else (0::'a)) * k else if t = ka then 1::'a else (0::'a)) *
      (if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f=" λka. (if ka = a then (if t = ka then 1::'a else (0::'a)) * k else if t = ka then 1::'a else (0::'a)) *
        (if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{t})  {t}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{t})  {t})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{t}) + sum ?f {t}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {t}" by auto
      also have "... = 1" using kq by auto
      finally show ?thesis .
    qed   
    fix s assume s_not_t: "s  t"
    show "(kaUNIV. (if ka = a then (if s = ka then 1::'a else (0::'a)) * k else if s = ka then 1::'a else (0::'a)) *
      (if t = a then (if ka = t then 1::'a else (0::'a)) * q else if ka = t then 1::'a else (0::'a))) = 0"
      apply (rule sum.neutral) using s_not_t by auto
  qed
qed

corollary invertible_mult_column':  
  assumes q_not_zero: "q  0"
  shows "invertible (mult_column (mat (1::'a::{field})) a q)"
  by (simp add: invertible_mult_column[of q "inverse q"] q_not_zero)

subsubsection‹Properties about adding a column multiplied by a constant to another column›
text‹Properties about @{term "column_add"}

lemma column_add_mat_1: "A ** column_add (mat 1) a b q = column_add A a b q"
proof (unfold matrix_matrix_mult_def, 
    unfold column_add_def, vector, auto)
  fix i
  let ?f="λk. A $ i $ k * (mat (1::'a) $ k $ a + mat (1::'a) $ k $ b * q)"
  show "sum ?f UNIV =  A $ i $ a + A $ i $ b * q"
  proof (cases "a=b")
    case True
    have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {a}" unfolding mat_def True by auto
    also have "... = ?f a" by auto
    also have "... = A $ i $ a + A $ i $ b * q" using True unfolding mat_1_fun using distrib_left[of "A $ i $ b" 1 q] by auto
    finally show ?thesis .
  next
    case False
    have univ_rw: "UNIV = {a}  ({b}  (UNIV - {a} - {b}))" by auto
    have sum_rw: "sum ?f ({b}  (UNIV - {a} - {b})) = sum ?f {b} + sum ?f (UNIV - {a} - {b})" by (rule sum.union_disjoint, auto simp add: False)
    have "sum ?f UNIV = sum ?f ({a}  ({b}  (UNIV - {a} - {b})))" using univ_rw by simp
    also have "... = sum ?f {a} + sum ?f ({b}  (UNIV - {a} - {b}))" by (rule sum.union_disjoint, auto simp add: False)
    also have "... = sum ?f {a} + sum ?f {b} + sum ?f (UNIV - {a} - {b})" 
      unfolding sum_rw add.assoc[symmetric] ..
    also have "... = sum ?f {a} + sum ?f {b}" unfolding mat_def by auto    
    also have "... =  A $ i $ a + A $ i $ b * q" using False unfolding mat_def by simp
    finally show ?thesis .
  qed    
  fix j
  assume j_noteq_a: "ja"
  show "(kUNIV. A $ i $ k * mat (1::'a) $ k $ j) = A $ i $ j"
  proof -
    let ?f="λk. A $ i $ k * mat (1::'a) $ k $ j"
    have univ_rw:"UNIV = (UNIV-{j})  {j}" by auto
    have "sum ?f UNIV = sum ?f ((UNIV-{j})  {j})" using univ_rw by auto
    also have "... = sum ?f (UNIV-{j}) + sum ?f {j}" by (rule sum.union_disjoint, auto)
    also have "... = sum ?f {j}" unfolding mat_def by auto
    also have "... =  A $ i $ j" unfolding mat_def by simp
    finally show ?thesis .
  qed
qed


lemma invertible_column_add:
  assumes a_noteq_b: "ab"
  shows "invertible (column_add (mat (1::'a::{ring_1})) a b q)"
proof (unfold invertible_def, rule exI[of _ "(column_add (mat 1) a b (-q))"], rule conjI)
  show " column_add (mat (1::'a)) a b q ** column_add (mat (1::'a)) a b (- q) = mat (1::'a)"  using a_noteq_b
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold column_add_def, vector, unfold mat_1_fun, auto)
    show " (kUNIV. (if k = a then (0::'a) + (1::'a) * q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk.  (if k = a then (0::'a) + (1::'a) * q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{b})  {b}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{b})  {b})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {b}" by auto 
      also have "... =  1" using a_noteq_b by simp
      finally show ?thesis .
    qed
    show "(kUNIV. (if k = a then 1 + 0 * q else if a = k then 1 else 0) * ((if k = a then 1 else 0) - (if k = b then 1 else 0) * q)) = 1"
    proof -
      let ?f="λk. (if k = a then (1::'a) + (0::'a) * q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + - ((if k = b then 1::'a else (0::'a)) * q))"
      have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {a}" by auto 
      also have "... =  1" using a_noteq_b by simp
      finally show ?thesis by simp
    qed  
    fix i j
    assume i_not_b: "i  b" and i_not_a: "i  a" and i_not_j: "i  j"
    show "(kUNIV. (if k = a then (0::'a) + (0::'a) * q else if i = k then 1::'a else (0::'a)) *
      (if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * - q else if k = j then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, auto simp add: i_not_b i_not_a i_not_j)
  next
    fix j
    assume a_not_j: "aj"
    show " (kUNIV. (if k = a then (1::'a) + (0::'a) * q else if a = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (0::'a)"
      apply (rule sum.neutral) using a_not_j a_noteq_b by auto
  next
    fix j
    assume j_not_b: "j  b" and j_not_a: "j  a"
    show " (kUNIV. (if k = a then (0::'a) + (0::'a) * q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if k = a then (0::'a) + (0::'a) * q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{j})  {j}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{j})  {j})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{j}) + sum ?f {j}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {j}" using j_not_b j_not_a by auto 
      also have "... =  1" using j_not_b j_not_a by auto 
      finally show ?thesis .
    qed
  next
    fix j
    assume b_not_j: "b  j"
    show "(kUNIV. (if k = a then 0 + 1 * q else if b = k then 1 else 0) *
      (if j = a then (if k = a then 1 else 0) + (if k = b then 1 else 0) * - q else if k = j then 1 else 0)) = 0"
    proof (cases "j=a")
      case False
      show ?thesis by (rule sum.neutral, auto simp add: False b_not_j)
    next
      case True ― ‹This case is different from the other cases›
      let ?f="λk. (if k = a then 0 + 1 * q else if b = k then 1 else 0) *
        (if j = a then (if k = a then 1 else 0) + (if k = b then 1 else 0) * - q else if k = j then 1 else 0)"
      have univ_eq: "UNIV = ((UNIV - {a}- {b})  ({b}  {a}))" by auto
      have sum_a: "sum ?f {a} = q"  unfolding True using b_not_j using a_noteq_b by auto
      have sum_b: "sum ?f {b} = -q" unfolding True using b_not_j using a_noteq_b by auto
      have sum_rest: "sum ?f (UNIV - {a} - {b}) = 0"  by (rule sum.neutral, auto simp add: True b_not_j a_noteq_b)
      have "sum ?f UNIV = sum ?f ((UNIV - {a}- {b})  ({b}  {a}))"  using univ_eq by simp
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f ({b}  {a})" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f {b} + sum ?f {a}" by (auto simp add: sum.union_disjoint a_noteq_b)     
      also have "... = 0" unfolding sum_a sum_b sum_rest by simp
      finally show ?thesis .
    qed                        
  qed
next
  show " column_add (mat (1::'a)) a b (- q) ** column_add (mat (1::'a)) a b q = mat (1::'a)" using a_noteq_b
  proof (unfold matrix_matrix_mult_def, vector, clarify, unfold column_add_def, vector, unfold mat_1_fun, auto)
    show "(kUNIV. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) * (if k = b then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{b})  {b}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{b})  {b})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{b}) + sum ?f {b}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {b}" by auto 
      also have "... =  1" using a_noteq_b by auto
      finally show ?thesis .
    qed
  next
    show "(kUNIV. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q)) =
      (1::'a)"
    proof -
      let ?f="λk. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * ((if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q) "
      have univ_rw:"UNIV = (UNIV-{a})  {a}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{a})  {a})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{a}) + sum ?f {a}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {a}" by auto 
      also have "... =  1" using a_noteq_b by auto
      finally show ?thesis .
    qed
  next
    fix j
    assume a_not_j: "a  j" show "(kUNIV. (if k = a then (1::'a) + (0::'a) * - q else if a = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (0::'a)"
      apply (rule sum.neutral) using a_not_j by auto
  next
    fix j
    assume j_not_b: "j  b" and j_not_a: "j  a" 
    show "(kUNIV. (if k = a then (0::'a) + (0::'a) * - q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))) = (1::'a)"
    proof -
      let ?f="λk.(if k = a then (0::'a) + (0::'a) * - q else if j = k then 1::'a else (0::'a)) * (if k = j then 1::'a else (0::'a))"
      have univ_rw:"UNIV = (UNIV-{j})  {j}" by auto
      have "sum ?f UNIV = sum ?f ((UNIV-{j})  {j})" using univ_rw by auto
      also have "... = sum ?f (UNIV-{j}) + sum ?f {j}" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f {j}" by auto 
      also have "... =  1" using a_noteq_b j_not_b j_not_a by auto
      finally show ?thesis .
    qed
  next
    fix i j
    assume i_not_b: "i  b" and i_not_a: "i  a" and i_not_j: "i  j"
    show "(kUNIV. (if k = a then (0::'a) + (0::'a) * - q else if i = k then 1::'a else (0::'a)) *
      (if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))) = (0::'a)"
      by (rule sum.neutral, auto simp add: i_not_b i_not_a i_not_j)
  next
    fix j
    assume b_not_j: "b  j"
    show "(kUNIV. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) *
      (if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))) = 0"
    proof (cases "j=a")
      case False
      show ?thesis by (rule sum.neutral, auto simp add: False b_not_j)
    next
      case True ― ‹This case is different from the other cases›
      let ?f="λk. (if k = a then (0::'a) + (1::'a) * - q else if b = k then 1::'a else (0::'a)) *
        (if j = a then (if k = a then 1::'a else (0::'a)) + (if k = b then 1::'a else (0::'a)) * q else if k = j then 1::'a else (0::'a))"
      have univ_eq: "UNIV = ((UNIV - {a}- {b})  ({b}  {a}))" by auto
      have sum_a: "sum ?f {a} = -q"  unfolding True using b_not_j using a_noteq_b by auto
      have sum_b: "sum ?f {b} = q" unfolding True using b_not_j using a_noteq_b by auto
      have sum_rest: "sum ?f (UNIV - {a} - {b}) = 0"  by (rule sum.neutral, auto simp add: True b_not_j a_noteq_b)
      have "sum ?f UNIV = sum ?f ((UNIV - {a}- {b})  ({b}  {a}))"  using univ_eq by simp
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f ({b}  {a})" by (rule sum.union_disjoint, auto)
      also have "... = sum ?f (UNIV - {a} - {b}) + sum ?f {b} + sum ?f {a}" by (auto simp add: sum.union_disjoint a_noteq_b)     
      also have "... = 0" unfolding sum_a sum_b sum_rest by simp
      finally show ?thesis .
    qed                   
  qed
qed

subsection‹Relationships amongst the definitions›

text‹Relationships between @{term "interchange_rows"} and @{term "interchange_columns"}

lemma interchange_rows_transpose:
  shows "interchange_rows (transpose A) a b = transpose (interchange_columns A a b)"
  unfolding interchange_rows_def interchange_columns_def transpose_def by vector

lemma interchange_rows_transpose':
  shows "interchange_rows A a b = transpose (interchange_columns (transpose A) a b)"
  unfolding interchange_rows_def interchange_columns_def transpose_def by vector

lemma interchange_columns_transpose:
  shows "interchange_columns (transpose A) a b = transpose (interchange_rows A a b)"
  unfolding interchange_rows_def interchange_columns_def transpose_def by vector

lemma interchange_columns_transpose':
  shows "interchange_columns A a b = transpose (interchange_rows (transpose A) a b)"
  unfolding interchange_rows_def interchange_columns_def transpose_def by vector

subsection‹Code Equations›
text‹Code equations for @{thm interchange_rows_def}, @{thm interchange_columns_def}, @{thm row_add_def}, @{thm column_add_def}, 
@{thm mult_row_def} and @{thm mult_column_def}:›

definition interchange_rows_row 
  where "interchange_rows_row A a b i = vec_lambda (%j. if i = a then A $ b $ j else if i = b then A $ a $ j else A $ i $ j)"

lemma interchange_rows_code [code abstract]:
  "vec_nth (interchange_rows_row A a b i) = (%j. if i = a then A $ b $ j else if i = b then A $ a $ j else A $ i $ j)"
  unfolding interchange_rows_row_def by auto 

lemma interchange_rows_code_nth [code abstract]: "vec_nth (interchange_rows A a b) = interchange_rows_row A a b"
  unfolding interchange_rows_def unfolding interchange_rows_row_def[abs_def]
  by auto

definition interchange_columns_row 
  where "interchange_columns_row A n m i = vec_lambda (%j.  if j = n then A $ i $ m else if j = m then A $ i $ n else A $ i $ j)"

lemma interchange_columns_code [code abstract]:
  "vec_nth (interchange_columns_row A n m i) = (%j.  if j = n then A $ i $ m else if j = m then A $ i $ n else A $ i $ j)"
  unfolding interchange_columns_row_def by auto 

lemma interchange_columns_code_nth [code abstract]: "vec_nth (interchange_columns A a b) = interchange_columns_row A a b"
  unfolding interchange_columns_def unfolding interchange_columns_row_def[abs_def]
  by auto

definition row_add_row 
  where "row_add_row A a b q i = vec_lambda (%j. if i = a then A $ a $ j + q * A $ b $ j else A $ i $ j)"

lemma row_add_code [code abstract]:
  "vec_nth (row_add_row A a b q i) =  (%j. if i = a then A $ a $ j + q * A $ b $ j else A $ i $ j)"
  unfolding row_add_row_def by auto 

lemma row_add_code_nth [code abstract]: "vec_nth (row_add A a b q) = row_add_row A a b q"
  unfolding row_add_def unfolding row_add_row_def[abs_def]
  by auto

definition column_add_row 
  where "column_add_row  A n m q i = vec_lambda (%j. if j = n then A $ i $ n + A $ i $ m * q else A $ i $ j)"

lemma column_add_code [code abstract]:
  "vec_nth (column_add_row A n m q i) =  (%j. if j = n then A $ i $ n + A $ i $ m * q else A $ i $ j)"
  unfolding column_add_row_def by auto

lemma column_add_code_nth [code abstract]: "vec_nth (column_add A a b q) = column_add_row A a b q"
  unfolding column_add_def unfolding column_add_row_def[abs_def]
  by auto

definition mult_row_row 
  where "mult_row_row A a q i = vec_lambda (%j. if i = a then q * A $ a $ j else A $ i $ j)"

lemma mult_row_code [code abstract]:
  "vec_nth (mult_row_row A a q i) = (%j. if i = a then q * A $ a $ j else A $ i $ j)"
  unfolding mult_row_row_def by auto

lemma mult_row_code_nth [code abstract]: "vec_nth (mult_row A a q) = mult_row_row A a q"
  unfolding mult_row_def unfolding mult_row_row_def[abs_def]
  by auto

definition mult_column_row 
  where "mult_column_row A n q i = vec_lambda (%j. if j = n then A $ i $ j * q else A $ i $ j)"

lemma mult_column_code [code abstract]:
  "vec_nth (mult_column_row A n q i) = (%j. if j = n then A $ i $ j * q else A $ i $ j)"
  unfolding mult_column_row_def by auto

lemma mult_column_code_nth [code abstract]: "vec_nth (mult_column A a q) = mult_column_row A a q"
  unfolding mult_column_def unfolding mult_column_row_def[abs_def]
  by auto


end