Session Gauss_Jordan

Theory Rref

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

section‹Reduced row echelon form›

theory Rref
imports
  Rank_Nullity_Theorem.Mod_Type
  Rank_Nullity_Theorem.Miscellaneous
begin

subsection‹Defining the concept of Reduced Row Echelon Form›

subsubsection‹Previous definitions and properties›
text‹This function returns True if each position lesser than k in a column contains a zero.›
definition is_zero_row_upt_k :: "'rows => nat =>'a::{zero}^'columns::{mod_type}^'rows => bool"
  where "is_zero_row_upt_k i k A = (j::'columns. (to_nat j) < k  A $ i $ j = 0)"

definition is_zero_row :: "'rows =>'a::{zero}^'columns::{mod_type}^'rows => bool"
  where "is_zero_row i A = is_zero_row_upt_k i (ncols A) A"

lemma is_zero_row_upt_ncols:
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows"
  shows "is_zero_row_upt_k i (ncols A) A = (j::'columns. A $ i $ j = 0)" unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def by auto

corollary is_zero_row_def':
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows"
  shows "is_zero_row i A = (j::'columns. A $ i $ j = 0)" using is_zero_row_upt_ncols unfolding is_zero_row_def ncols_def .

lemma is_zero_row_eq_row_zero: "is_zero_row a A = (row a A = 0)"
  unfolding is_zero_row_def' row_def
  unfolding vec_nth_inverse
  unfolding vec_eq_iff zero_index ..

lemma not_is_zero_row_upt_suc:
  assumes "¬ is_zero_row_upt_k i (Suc k) A"
  and "i. A $ i $ (from_nat k) = 0"
  shows "¬ is_zero_row_upt_k i k A"
  using assms from_nat_to_nat_id 
  using is_zero_row_upt_k_def less_SucE 
  by metis

lemma is_zero_row_upt_k_suc:
  assumes "is_zero_row_upt_k i k A"
  and "A $ i $ (from_nat k) = 0"
  shows "is_zero_row_upt_k i (Suc k) A"
  using assms unfolding is_zero_row_upt_k_def using less_SucE to_nat_from_nat by metis

lemma is_zero_row_utp_0:
  shows "is_zero_row_upt_k m 0 A" unfolding is_zero_row_upt_k_def by fast

lemma is_zero_row_utp_0':
  shows "m. is_zero_row_upt_k m 0 A" unfolding is_zero_row_upt_k_def by fast

lemma is_zero_row_upt_k_le:
  assumes "is_zero_row_upt_k i (Suc k) A"
  shows "is_zero_row_upt_k i k A"
  using assms unfolding is_zero_row_upt_k_def by simp

lemma is_zero_row_imp_is_zero_row_upt:
assumes "is_zero_row i A"
shows "is_zero_row_upt_k i k A"
using assms unfolding  is_zero_row_def is_zero_row_upt_k_def ncols_def by simp

subsubsection‹Definition of reduced row echelon form up to a column›

text‹This definition returns True if a matrix is in reduced row echelon form up to the column k (not included), otherwise False.›

(*In the third condition, i<i+1 is assumed to avoid that row i can be the last row (in that case, i+1 would be the first row):*)

definition reduced_row_echelon_form_upt_k :: "'a::{zero, one}^'m::{mod_type}^'n::{finite, ord, plus, one} => nat => bool"
  where "reduced_row_echelon_form_upt_k A k = 
  (
    (i. is_zero_row_upt_k i k A  ¬ (j. j>i  ¬ is_zero_row_upt_k j k A)) 
    (i. ¬ (is_zero_row_upt_k i k A)  A $ i $ (LEAST k. A $ i $ k  0) = 1) 
    (i. i<i+1  ¬ (is_zero_row_upt_k i k A)  ¬ (is_zero_row_upt_k (i+1) k A)  ((LEAST n. A $ i $ n  0) < (LEAST n. A $ (i+1) $ n  0)))  
    (i. ¬ (is_zero_row_upt_k i k A)  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0))
  )"


lemma rref_upt_0: "reduced_row_echelon_form_upt_k A 0"
  unfolding reduced_row_echelon_form_upt_k_def is_zero_row_upt_k_def by auto

lemma rref_upt_condition1:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(i. is_zero_row_upt_k i k A  ¬ (j. j>i  ¬ is_zero_row_upt_k j k A))"
  using r unfolding reduced_row_echelon_form_upt_k_def by simp

lemma rref_upt_condition2:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(i. ¬ (is_zero_row_upt_k i k A)  A $ i $ (LEAST k. A $ i $ k  0) = 1)"
  using r unfolding reduced_row_echelon_form_upt_k_def by simp

lemma rref_upt_condition3:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(i. i<i+1  ¬ (is_zero_row_upt_k i k A)  ¬ (is_zero_row_upt_k (i+1) k A)  ((LEAST n. A $ i $ n  0) < (LEAST n. A $ (i+1) $ n  0)))"
  using r unfolding reduced_row_echelon_form_upt_k_def by simp

lemma rref_upt_condition4:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows " (i. ¬ (is_zero_row_upt_k i k A)  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0))"
  using r unfolding reduced_row_echelon_form_upt_k_def by simp

text‹Explicit lemmas for each condition›

lemma rref_upt_condition1_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "is_zero_row_upt_k i k A"
and "j>i"
shows "is_zero_row_upt_k j k A"
using assms rref_upt_condition1 by blast

lemma rref_upt_condition2_explicit:
assumes rref_A: "reduced_row_echelon_form_upt_k A k"
and "¬ is_zero_row_upt_k i k A"
shows "A $ i $ (LEAST k. A $ i $ k  0) = 1"
using rref_upt_condition2 assms by blast

lemma rref_upt_condition3_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "i < i + 1"  
and "¬ is_zero_row_upt_k i k A"
and "¬ is_zero_row_upt_k (i + 1) k A "
shows "(LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)"
using assms rref_upt_condition3 by blast

lemma rref_upt_condition4_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "¬ is_zero_row_upt_k i k A"
and "i  j"
shows "A $ j $ (LEAST n. A $ i $ n  0) = 0"
using assms rref_upt_condition4 by auto

text‹Intro lemma and general properties›

lemma reduced_row_echelon_form_upt_k_intro:
  assumes "(i. is_zero_row_upt_k i k A  ¬ (j. j>i  ¬ is_zero_row_upt_k j k A))"
  and "(i. ¬ (is_zero_row_upt_k i k A)  A $ i $ (LEAST k. A $ i $ k  0) = 1)"
  and "(i. i<i+1  ¬ (is_zero_row_upt_k i k A)  ¬ (is_zero_row_upt_k (i+1) k A)  ((LEAST n. A $ i $ n  0) < (LEAST n. A $ (i+1) $ n  0)))"
  and "(i. ¬ (is_zero_row_upt_k i k A)  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0))"
  shows "reduced_row_echelon_form_upt_k A k"
  unfolding reduced_row_echelon_form_upt_k_def using assms by fast

lemma rref_suc_imp_rref:
  fixes A::"'a::{semiring_1}^'n::{mod_type}^'m::{mod_type}"
  assumes r: "reduced_row_echelon_form_upt_k A (Suc k)"
  and k_le_card: "Suc k < ncols A"
  shows "reduced_row_echelon_form_upt_k A k"
proof (rule reduced_row_echelon_form_upt_k_intro)
  show "i. ¬ is_zero_row_upt_k i k A  A $ i $ (LEAST k. A $ i $ k  0) = 1" 
    using rref_upt_condition2[OF r] less_SucI unfolding is_zero_row_upt_k_def by blast
  show "i. i < i + 1  ¬ is_zero_row_upt_k i k A  ¬ is_zero_row_upt_k (i + 1) k A  (LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)"
    using rref_upt_condition3[OF r] less_SucI unfolding is_zero_row_upt_k_def by blast
  show "i. ¬ is_zero_row_upt_k i k A  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0)"
    using rref_upt_condition4[OF r] less_SucI unfolding is_zero_row_upt_k_def by blast
  show "i. is_zero_row_upt_k i k A  ¬ (j>i. ¬ is_zero_row_upt_k j k A)"
  proof (clarify, rule ccontr)
    fix i j
    assume zero_i: "is_zero_row_upt_k i k A"
      and i_less_j: "i < j"
      and not_zero_j: "¬ is_zero_row_upt_k j k A"
    have not_zero_j_suc: "¬ is_zero_row_upt_k j (Suc k) A"
      using not_zero_j unfolding is_zero_row_upt_k_def by fastforce
    hence not_zero_i_suc: "¬ is_zero_row_upt_k i (Suc k) A"
      using rref_upt_condition1[OF r] i_less_j by fast
    have not_zero_i_plus_suc: "¬ is_zero_row_upt_k (i+1) (Suc k) A"
    proof (cases "j=i+1")
      case True thus ?thesis using not_zero_j_suc by simp
    next
      case False
      have "i+1<j" by (rule Suc_less[OF i_less_j False[symmetric]])
      thus ?thesis  using rref_upt_condition1[OF r] not_zero_j_suc by blast
    qed
    from this obtain n where a: "A $ (i+1) $ n  0" and n_less_suc: "to_nat n < Suc k"
      unfolding is_zero_row_upt_k_def by blast
    have "(LEAST n. A $ (i+1) $ n  0)  n" by (rule Least_le, simp add: a)
    also have "...  from_nat k" by (metis Suc_lessD from_nat_mono' from_nat_to_nat_id k_le_card less_Suc_eq_le n_less_suc ncols_def)
    finally have least_le: "(LEAST n. A $ (i + 1) $ n  0)  from_nat k" .
    have least_eq_k: "(LEAST n. A $ i $ n  0) = from_nat k"
    proof (rule Least_equality)
      show "A $ i $ from_nat k  0" using not_zero_i_suc zero_i unfolding is_zero_row_upt_k_def by (metis from_nat_to_nat_id less_SucE)
      show "y. A $ i $ y  0  from_nat k  y" by (metis is_zero_row_upt_k_def not_le_imp_less to_nat_le zero_i)
    qed
    have i_less: "i<i+1"
    proof (rule Suc_le', rule ccontr)
      assume "¬ i + 1  0" hence "i+1=0" by simp
      hence "i=-1" using diff_0 diff_add_cancel diff_minus_eq_add by metis
      hence "j <= i" using Greatest_is_minus_1 by blast
      thus False using i_less_j by fastforce
    qed
    have "from_nat k < (LEAST n. A $ (i+1) $ n  0)"
      using rref_upt_condition3[OF r] i_less not_zero_i_suc not_zero_i_plus_suc least_eq_k by fastforce
    thus False using least_le by simp
  qed
qed

lemma reduced_row_echelon_if_all_zero:
  assumes all_zero: "n. is_zero_row_upt_k n k A"
  shows "reduced_row_echelon_form_upt_k A k"
  using assms unfolding reduced_row_echelon_form_upt_k_def is_zero_row_upt_k_def by auto

subsubsection‹The definition of reduced row echelon form›

text‹Definition of reduced row echelon form, based on reduced_row_echelon_form_upt_k_def›
definition reduced_row_echelon_form :: "'a::{zero, one}^'m::{mod_type}^'n::{finite, ord, plus, one} => bool"
  where "reduced_row_echelon_form A = reduced_row_echelon_form_upt_k A (ncols A)"

text‹Equivalence between our definition of reduced row echelon form and the one presented
in Steven Roman's book: Advanced Linear Algebra.›

lemma reduced_row_echelon_form_def': 
"reduced_row_echelon_form A = 
  (
    (i. is_zero_row i A  ¬ (j. j>i  ¬ is_zero_row j A)) 
    (i. ¬ (is_zero_row i A)  A $ i $ (LEAST k. A $ i $ k  0) = 1) 
    (i. i<i+1  ¬ (is_zero_row i A)  ¬ (is_zero_row (i+1) A)  ((LEAST k. A $ i $ k  0) < (LEAST k. A $ (i+1) $ k  0))) 
    (i. ¬ (is_zero_row i A)  (j. i  j  A $ j $ (LEAST k. A $ i $ k  0) = 0))
  )" unfolding reduced_row_echelon_form_def reduced_row_echelon_form_upt_k_def is_zero_row_def ..

subsection‹Properties of the reduced row echelon form of a matrix›

lemma rref_condition1:
  assumes r: "reduced_row_echelon_form A"
  shows "(i. is_zero_row i A  ¬ (j. j>i  ¬ is_zero_row j A))" using r unfolding reduced_row_echelon_form_def' by simp

lemma rref_condition2:
  assumes r: "reduced_row_echelon_form A"
  shows " (i. ¬ (is_zero_row i A)  A $ i $ (LEAST k. A $ i $ k  0) = 1)" using r unfolding reduced_row_echelon_form_def' by simp

lemma rref_condition3:
  assumes r: "reduced_row_echelon_form A"
  shows "(i. i<i+1  ¬ (is_zero_row i A)  ¬ (is_zero_row (i+1) A)  ((LEAST n. A $ i $ n  0) < (LEAST n. A $ (i+1) $ n  0)))"
  using r unfolding reduced_row_echelon_form_def' by simp

lemma rref_condition4:
  assumes r: "reduced_row_echelon_form A"
  shows " (i. ¬ (is_zero_row i A)  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0))"
  using r unfolding reduced_row_echelon_form_def' by simp

text‹Explicit lemmas for each condition›

lemma rref_condition1_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "is_zero_row i A" 
shows "j>i. is_zero_row j A"
using rref_condition1 assms by blast

lemma rref_condition2_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "¬ is_zero_row i A"
shows "A $ i $ (LEAST k. A $ i $ k  0) = 1"
using rref_condition2 assms by blast

lemma rref_condition3_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and i_le: "i < i + 1"
and "¬ is_zero_row i A" and "¬ is_zero_row (i + 1) A"
shows "(LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)"
using rref_condition3 assms by blast

lemma rref_condition4_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "¬ is_zero_row i A" 
and "i  j"
shows "A $ j $ (LEAST n. A $ i $ n  0) = 0"
using rref_condition4 assms by blast

text‹Other properties and equivalences›

lemma rref_condition3_equiv1:
fixes A::"'a::{one, zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and i_less_j: "i<j"
and j_less_nrows: "j<nrows A"
and not_zero_i: "¬ is_zero_row (from_nat i) A"
and not_zero_j: "¬ is_zero_row (from_nat j) A"
shows "(LEAST n. A $ (from_nat i) $ n  0) < (LEAST n. A $ (from_nat j) $ n  0)"
using i_less_j not_zero_j j_less_nrows
proof (induct j)
case 0
show ?case using "0.prems"(1) by simp
next
fix j
assume hyp: "i < j  ¬ is_zero_row (from_nat j) A  j < nrows A  (LEAST n. A $ from_nat i $ n  0) < (LEAST n. A $ from_nat j $ n  0)"
and i_less_suc_j: "i < Suc j"
and not_zero_suc_j: "¬ is_zero_row (from_nat (Suc j)) A"
and Suc_j_less_nrows: "Suc j < nrows A"
have j_less: "(from_nat j::'rows) < from_nat (j+1)" by (rule from_nat_mono, auto simp add: Suc_j_less_nrows[unfolded nrows_def])
hence not_zero_j: "¬ is_zero_row (from_nat j) A" using rref_condition1[OF rref] not_zero_suc_j unfolding Suc_eq_plus1 by blast
show "(LEAST n. A $ from_nat i $ n  0) < (LEAST n. A $ from_nat (Suc j) $ n  0)"
proof (cases "i=j")
case True 
show ?thesis 
 proof (unfold True Suc_eq_plus1 from_nat_suc, rule rref_condition3_explicit)
     show "reduced_row_echelon_form A" using rref .
     show "(from_nat j::'rows) < from_nat j + 1" using j_less unfolding from_nat_suc .
     show "¬ is_zero_row (from_nat j) A" using not_zero_j .
     show "¬ is_zero_row (from_nat j + 1) A" using not_zero_suc_j unfolding Suc_eq_plus1 from_nat_suc .
  qed
next
case False 
have "(LEAST n. A $ from_nat i $ n  0) < (LEAST n. A $ from_nat j $ n  0)"
  proof (rule hyp)
     show "i < j" using False i_less_suc_j by simp
     show "¬ is_zero_row (from_nat j) A" using not_zero_j .
     show "j < nrows A" using Suc_j_less_nrows by simp
  qed
also have "... < (LEAST n. A $ from_nat (j+1) $ n  0)"
  proof (unfold from_nat_suc, rule rref_condition3_explicit)
     show "reduced_row_echelon_form A" using rref .
     show "(from_nat j::'rows) < from_nat j + 1" using j_less unfolding from_nat_suc .
     show "¬ is_zero_row (from_nat j) A" using not_zero_j .
     show "¬ is_zero_row (from_nat j + 1) A" using not_zero_suc_j unfolding Suc_eq_plus1 from_nat_suc .
  qed
finally show "(LEAST n. A $ from_nat i $ n  0) < (LEAST n. A $ from_nat (Suc j) $ n  0)" unfolding Suc_eq_plus1 .
qed 
qed

corollary rref_condition3_equiv:
fixes A::"'a::{one, zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and i_less_j: "i<j"
and i: "¬ is_zero_row i A"
and j: "¬ is_zero_row j A"
shows "(LEAST n. A $ i $ n  0) < (LEAST n. A $ j $ n  0)"
proof (rule rref_condition3_equiv1[of A "to_nat i" "to_nat j", unfolded from_nat_to_nat_id])
 show "reduced_row_echelon_form A" using rref .
 show "to_nat i < to_nat j" by (rule to_nat_mono[OF i_less_j])
 show "to_nat j < nrows A" using to_nat_less_card unfolding nrows_def .
 show "¬ is_zero_row i A" using i .
 show "¬ is_zero_row j A" using j .
qed


lemma rref_implies_rref_upt:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
shows "reduced_row_echelon_form_upt_k A k"
proof (rule reduced_row_echelon_form_upt_k_intro)
  show "i. ¬ is_zero_row_upt_k i k A  A $ i $ (LEAST k. A $ i $ k  0) = 1"
    using rref_condition2[OF rref] is_zero_row_imp_is_zero_row_upt by blast
  show "i. i < i + 1  ¬ is_zero_row_upt_k i k A  ¬ is_zero_row_upt_k (i + 1) k A  (LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)"
    using rref_condition3[OF rref] is_zero_row_imp_is_zero_row_upt by blast
  show "i. ¬ is_zero_row_upt_k i k A  (j. i  j  A $ j $ (LEAST n. A $ i $ n  0) = 0)"
    using rref_condition4[OF rref] is_zero_row_imp_is_zero_row_upt by blast
show "i. is_zero_row_upt_k i k A  ¬ (j>i. ¬ is_zero_row_upt_k j k A)"
proof (auto, rule ccontr)
fix i j assume zero_i_k: "is_zero_row_upt_k i k A" and i_less_j: "i < j"
and not_zero_j_k:"¬ is_zero_row_upt_k j k A"
have not_zero_j: "¬ is_zero_row j A" using is_zero_row_imp_is_zero_row_upt not_zero_j_k by blast
hence not_zero_i: "¬ is_zero_row i A" using rref_condition1[OF rref] i_less_j by blast
have Least_less: "(LEAST n. A $ i $ n  0) < (LEAST n. A $ j $ n  0)" by (rule rref_condition3_equiv[OF rref i_less_j not_zero_i not_zero_j])
moreover have "(LEAST n. A $ j $ n  0) < (LEAST n. A $ i $ n  0)"
  proof (rule LeastI2_ex)   
     show "a. A $ i $ a  0" using not_zero_i unfolding is_zero_row_def is_zero_row_upt_k_def by fast
     fix x assume Aix_not_0: "A $ i $ x  0"
     have k_less_x: "k  to_nat x"  using zero_i_k Aix_not_0 unfolding is_zero_row_upt_k_def by force
     hence k_less_ncols: "k < ncols A" unfolding ncols_def using to_nat_less_card[of x] by simp
     obtain s where Ajs_not_zero: "A $ j $ s  0" and s_less_k: "to_nat s < k" using not_zero_j_k unfolding is_zero_row_upt_k_def by blast
     have "(LEAST n. A $ j $ n  0)  s" using Ajs_not_zero Least_le by fast
     also have "... = from_nat (to_nat s)" unfolding from_nat_to_nat_id ..
     also have "... < from_nat k" by (rule from_nat_mono[OF s_less_k k_less_ncols[unfolded ncols_def]])
     also have "...  x" using k_less_x leD not_le_imp_less to_nat_le by fast
     finally show "(LEAST n. A $ j $ n  0) < x" .
  qed
ultimately show False by fastforce
qed
qed


lemma rref_first_position_zero_imp_column_0:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and A_00: "A $ 0 $ 0 = 0"
shows "column 0 A = 0"
proof (unfold column_def, vector, clarify)
fix i
have "is_zero_row_upt_k 0 1 A" unfolding is_zero_row_upt_k_def using A_00 by (metis One_nat_def less_Suc0 to_nat_eq_0)
hence "is_zero_row_upt_k i 1 A" using rref_upt_condition1[OF rref_implies_rref_upt[OF rref]] using least_mod_type less_le by metis
thus "A $ i $ 0 = 0" unfolding is_zero_row_upt_k_def using to_nat_eq_0 by blast
qed


lemma rref_first_element:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and column_not_0: "column 0 A  0"
shows "A $ 0 $ 0 = 1"
proof (rule ccontr)
have A_00_not_0: "A $ 0 $ 0  0"
  proof (rule ccontr, simp)
    assume A_00: "A $ 0 $ 0 = 0"
    from this obtain i where Ai0: "A $ i $ 0  0" and i: "i>0" using column_not_0 unfolding column_def by (metis column_def rref rref_first_position_zero_imp_column_0)
    have "is_zero_row_upt_k 0 1 A" unfolding is_zero_row_upt_k_def using A_00 by (metis One_nat_def less_Suc0 to_nat_eq_0)
    moreover have "¬ is_zero_row_upt_k i 1 A" using Ai0 by (metis is_zero_row_upt_k_def to_nat_0 zero_less_one)
    ultimately have "¬ reduced_row_echelon_form A" by (metis A_00 column_not_0 rref_first_position_zero_imp_column_0)
    thus False using rref by contradiction
qed
assume A_00_not_1: "A $ 0 $ 0  1"
have Least_eq_0: "(LEAST n. A $ 0 $ n  0) = 0"
  proof (rule Least_equality)
     show "A $ 0 $ 0  0" by (rule A_00_not_0)
     show "y. A $ 0 $ y  0  0  y" using least_mod_type .
  qed
moreover have "¬ is_zero_row 0 A" unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def using A_00_not_0 by auto
ultimately have "A $ 0 $ (LEAST n. A $ 0 $ n  0) = 1" using rref_condition2[OF rref] by fast
thus False unfolding Least_eq_0 using A_00_not_1 by contradiction
qed

end

Theory Code_Set

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

section "Code set"

theory Code_Set
imports
  "HOL-Library.Cardinality"
begin

text‹The following setup could help to get code generation for List.coset, 
  but it neither works correctly it complains that code
  equations for remove are missed, even when List.coset should be rewritten
  to an enum:›

declare minus_coset_filter [code del]
declare remove_code(2) [code del]
declare insert_code(2) [code del]
declare inter_coset_fold [code del]
declare compl_coset[code del]
declare Cardinality.card'_code(2)[code del]

code_datatype set

text‹The following code equation could be useful to avoid the problem of
  code generation for List.coset []:›

lemma [code]: "List.coset (l::'a::enum list) = set (enum_class.enum) - set l"
  by (metis Compl_eq_Diff_UNIV coset_def enum_UNIV)

text‹Now the following examples work:›

value "UNIV::bool set"
value "List.coset ([]::bool list)"
value "UNIV::Enum.finite_2 set"
value "List.coset ([]::Enum.finite_2 list)"
value "List.coset ([]::Enum.finite_5 list)"

end

Theory Code_Matrix

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

section‹Code generation for vectors and matrices›

theory Code_Matrix
imports 
  Rank_Nullity_Theorem.Miscellaneous
  Code_Set
begin

text‹In this file the code generator is set up properly to allow the execution of matrices 
      represented as funcions over finite types.›

lemmas vec.vec_nth_inverse[code abstype]

lemma [code abstract]: "vec_nth 0 = (%x. 0)" by (metis zero_index)
lemma [code abstract]: "vec_nth 1 = (%x. 1)" by (metis one_index)
lemma [code abstract]: "vec_nth (a + b) =  (%i. a$i + b$i)" by (metis vector_add_component)
lemma [code abstract]: "vec_nth (a - b) =  (%i. a$i - b$i)" by (metis vector_minus_component)
lemma [code abstract]: "vec_nth (vec n) = (λi. n)" unfolding vec_def by fastforce
lemma [code abstract]: "vec_nth (a * b) =  (%i. a$i * b$i)" unfolding vector_mult_component by auto
lemma [code abstract]: "vec_nth (c *s x) = (λi. c * (x$i))" unfolding vector_scalar_mult_def by auto
lemma [code abstract]: "vec_nth (a - b) =  (%i. a$i - b$i)" by (metis vector_minus_component)

definition mat_mult_row 
  where "mat_mult_row m m' f = vec_lambda (%c. sum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"

lemma mat_mult_row_code [code abstract]:
  "vec_nth (mat_mult_row m m' f) = (%c. sum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"
  by(simp add: mat_mult_row_def fun_eq_iff)

lemma mat_mult [code abstract]: "vec_nth (m ** m') = mat_mult_row m m'"
  unfolding matrix_matrix_mult_def mat_mult_row_def[abs_def]
  using vec_lambda_beta by auto

lemma matrix_vector_mult_code [code abstract]:
  "vec_nth (A *v x) = (%i. (jUNIV. A $ i $ j * x $ j))" unfolding matrix_vector_mult_def by fastforce

lemma vector_matrix_mult_code [code abstract]:
  "vec_nth (x v* A) = (%j. (iUNIV. A $ i $ j * x $ i))" unfolding vector_matrix_mult_def by fastforce

definition mat_row
  where "mat_row k i = vec_lambda (%j. if i = j then k else 0)"

lemma mat_row_code [code abstract]:
  "vec_nth (mat_row k i) = (%j. if i = j then k else 0)" unfolding mat_row_def by auto

lemma [code abstract]: "vec_nth (mat k) = mat_row k"
  unfolding mat_def unfolding mat_row_def[abs_def] by auto

definition transpose_row
   where "transpose_row A i = vec_lambda (%j. A $ j $ i)"

lemma transpose_row_code [code abstract]:
  "vec_nth (transpose_row A i) = (%j.  A $ j $ i)" by (metis transpose_row_def vec_lambda_beta)

lemma transpose_code[code abstract]:
  "vec_nth (transpose A) = transpose_row A"
  by (auto simp: transpose_def transpose_row_def)

lemma [code abstract]: "vec_nth (row i A) =  (($) (A $ i))" unfolding row_def by fastforce
lemma [code abstract]: "vec_nth (column j A) = (%i. A $ i $ j)" unfolding column_def by fastforce

definition "rowvector_row v i = vec_lambda (%j. (v$j))"

lemma rowvector_row_code [code abstract]:
  "vec_nth (rowvector_row v i) = (%j. (v$j))" unfolding rowvector_row_def by auto

lemma [code abstract]: "vec_nth (rowvector v) = rowvector_row v"
  unfolding rowvector_def unfolding rowvector_row_def[abs_def] by auto

definition "columnvector_row v i = vec_lambda (%j. (v$i))"

lemma columnvector_row_code [code abstract]:
  "vec_nth (columnvector_row v i) = (%j. (v$i))" unfolding columnvector_row_def by auto

lemma [code abstract]: "vec_nth (columnvector v) = columnvector_row v"
  unfolding columnvector_def unfolding columnvector_row_def[abs_def] by auto

end

Theory 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 (hide_lams, 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

Theory Rank

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

section‹Rank of a matrix›

theory Rank
imports 
      Rank_Nullity_Theorem.Dim_Formula
begin

subsection‹Row rank, column rank and rank›

text‹Definitions of row rank, column rank and rank›

definition row_rank :: "'a::{field}^'n^'m=>nat"
  where "row_rank A = vec.dim (row_space A)"

definition col_rank :: "'a::{field}^'n^'m=>nat"
  where "col_rank A = vec.dim (col_space A)"

lemma rank_def: "rank A = row_rank A"
  by (auto simp: row_rank_def row_rank_def_gen row_space_def)

subsection‹Properties›

lemma rrk_is_preserved:
fixes A::"'a::{field}^'cols^'rows::{finite, wellorder}"
  and P::"'a::{field}^'rows::{finite, wellorder}^'rows::{finite, wellorder}"
assumes inv_P: "invertible P"
shows "row_rank A = row_rank (P**A)"
by (metis row_space_is_preserved row_rank_def inv_P)

lemma crk_is_preserved:
fixes A::"'a::{field}^'cols::{finite, wellorder}^'rows"
  and P::"'a::{field}^'rows^'rows"
assumes inv_P: "invertible P"
shows "col_rank A = col_rank (P**A)"
  using rank_nullity_theorem_matrices unfolding ncols_def 
  by (metis col_rank_def inv_P add_left_cancel null_space_is_preserved) 

end

Theory Gauss_Jordan

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

section‹Gauss Jordan algorithm over abstract matrices›

theory Gauss_Jordan
imports
  Rref
  Elementary_Operations
  Rank  
begin

subsection‹The Gauss-Jordan Algorithm›

text‹Now, a computable version of the Gauss-Jordan algorithm is presented. The output will be a matrix in reduced row echelon form.
We present an algorithm in which the reduction is applied by columns›

text‹Using this definition, zeros are made in the column j of a matrix A placing the pivot entry (a nonzero element) in the position (i,j).
For that, a suitable row interchange is made to achieve a non-zero entry in position (i,j). Then, this pivot entry is multiplied by its inverse
to make the pivot entry equals to 1. After that, are other entries of the j-th column are eliminated by subtracting suitable multiples of the
i-th row from the other rows.›

definition Gauss_Jordan_in_ij :: "'a::{semiring_1, inverse, one, uminus}^'m^'n::{finite, ord}=> 'n=>'m=>'a^'m^'n::{finite, ord}"
where "Gauss_Jordan_in_ij A i j = (let n = (LEAST n. A $ n $ j  0  i  n); 
                                interchange_A = (interchange_rows A i n); 
                                A' = mult_row interchange_A i (1/interchange_A$i$j) in 
                                vec_lambda(% s. if s=i then A' $ s else (row_add A' s i (-(interchange_A$s$j))) $ s))"

lemma Gauss_Jordan_in_ij_unfold:
  assumes "n. A $ n $ j  0  i  n"
  obtains n :: "'n::{finite, wellorder}" and interchange_A and A'
  where
    "(LEAST n. A $ n $ j  0  i  n) = n"
    and "A $ n $ j  0"
    and "i  n"
    and "interchange_A = interchange_rows A i n"
    and "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)"
    and "Gauss_Jordan_in_ij A i j = vec_lambda (λs. if s = i then A' $ s 
      else (row_add A' s i (- (interchange_A $ s $ j))) $ s)"
proof -
  from assms obtain m where Anj: "A $ m $ j  0  i  m" ..
  moreover define n where "n = (LEAST n. A $ n $ j  0  i  n)"
  then have P1: "(LEAST n. A $ n $ j  0  i  n) = n" by simp
  ultimately have P2: "A $ n $ j  0" and P3: "i  n"
    using LeastI [of "λn. A $ n $ j  0  i  n" m] by simp_all
  define interchange_A where "interchange_A = interchange_rows A i n"
  then have P4: "interchange_A = interchange_rows A i n" by simp
  define A' where "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)"
  then have P5: "A' = mult_row interchange_A i (1 / interchange_A $ i $ j)" by simp
  have P6: "Gauss_Jordan_in_ij A i j = vec_lambda (λs. if s = i then A' $ s 
    else (row_add A' s i (- (interchange_A $ s $ j))) $ s)"
    by (simp only: Gauss_Jordan_in_ij_def P1 P4 [symmetric] P5 [symmetric] Let_def)
  from P1 P2 P3 P4 P5 P6 that show thesis by blast
qed
                                
text‹The following definition makes the step of Gauss-Jordan in a column. This function receives two input parameters: the column k
where the step of Gauss-Jordan must be applied and a pair (which consists of the row where the pivot should be placed in the column k and the original matrix).›

definition Gauss_Jordan_column_k :: "(nat × ('a::{zero,inverse,uminus,semiring_1}^'m::{mod_type}^'n::{mod_type})) 
=> nat => (nat × ('a^'m::{mod_type}^'n::{mod_type}))"
where "Gauss_Jordan_column_k A' k = (let i=fst A'; A=(snd A'); from_nat_i=(from_nat i::'n); from_nat_k=(from_nat k::'m) in 
        if (m(from_nat_i). A $ m $(from_nat_k)=0)  (i = nrows A) then (i,A) else (i+1, (Gauss_Jordan_in_ij A (from_nat_i) (from_nat_k))))"

text‹The following definition applies the Gauss-Jordan step from the first column up to the k one (included).›

definition Gauss_Jordan_upt_k :: "'a::{inverse,uminus,semiring_1}^'columns::{mod_type}^'rows::{mod_type} => nat 
=> 'a^'columns::{mod_type}^'rows::{mod_type}"
 where "Gauss_Jordan_upt_k A k = snd (foldl Gauss_Jordan_column_k (0,A) [0..<Suc k])"

text‹Gauss-Jordan is to apply the @{term "Gauss_Jordan_column_k"} in all columns.›
definition Gauss_Jordan :: "'a::{inverse,uminus,semiring_1}^'columns::{mod_type}^'rows::{mod_type}  
=> 'a^'columns::{mod_type}^'rows::{mod_type}"
 where "Gauss_Jordan A = Gauss_Jordan_upt_k A ((ncols A) - 1)"


subsection‹Properties about rref and the greatest nonzero row.›

lemma greatest_plus_one_eq_0:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A)) = nrows A"
  shows "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1 = 0"
proof -
  have "to_nat (GREATEST R. ¬ is_zero_row_upt_k R k A) + 1 = card (UNIV::'rows set)"
    using assms unfolding nrows_def by fastforce
  thus "(GREATEST n. ¬ is_zero_row_upt_k n k A) + (1::'rows) = (0::'rows)"
    using to_nat_plus_one_less_card by fastforce
qed

lemma from_nat_to_nat_greatest:
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows::{mod_type}"
  shows "from_nat (Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A))) = (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1"
  unfolding Suc_eq_plus1
  unfolding to_nat_1[where ?'a='rows, symmetric]
  unfolding add_to_nat_def ..

lemma greatest_less_zero_row:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and zero_i: "is_zero_row_upt_k i k A"
  and not_all_zero: "¬ (a. is_zero_row_upt_k a k A)"
  shows "(GREATEST m. ¬ is_zero_row_upt_k m k A) < i"
proof (rule ccontr)
  assume not_less_i: "¬ (GREATEST m. ¬ is_zero_row_upt_k m k A) < i"
  have i_less_greatest: "i < (GREATEST m. ¬ is_zero_row_upt_k m k A)"
    by (metis (mono_tags, lifting) GreatestI neqE not_all_zero not_less_i zero_i) 
  have "is_zero_row_upt_k (GREATEST m. ¬ is_zero_row_upt_k m k A) k A"
    using r zero_i i_less_greatest unfolding reduced_row_echelon_form_upt_k_def by blast
  thus False using GreatestI_ex not_all_zero by fast
qed

lemma rref_suc_if_zero_below_greatest:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and not_all_zero: "¬ (a. is_zero_row_upt_k a k A)" (*This premisse is necessary to assure the existence of the Greatest*)
  and all_zero_below_greatest: "a. a>(GREATEST m. ¬ is_zero_row_upt_k m k A)  is_zero_row_upt_k a (Suc k) A"
  shows "reduced_row_echelon_form_upt_k A (Suc k)"
proof (rule reduced_row_echelon_form_upt_k_intro, auto)
  fix i j assume zero_i_suc: "is_zero_row_upt_k i (Suc k) A" and i_le_j: "i < j"
  have zero_i: "is_zero_row_upt_k i k A" using zero_i_suc unfolding is_zero_row_upt_k_def by simp
  have "i>(GREATEST m. ¬ is_zero_row_upt_k m k A)" by (rule greatest_less_zero_row[OF r zero_i not_all_zero])
  hence "j>(GREATEST m. ¬ is_zero_row_upt_k m k A)" using i_le_j by simp
  thus "is_zero_row_upt_k j (Suc k) A" using all_zero_below_greatest by fast
next
  fix i assume not_zero_i: "¬ is_zero_row_upt_k i (Suc k) A"
  show "A $ i $ (LEAST k. A $ i $ k  0) = 1" 
    using  greatest_less_zero_row[OF r _ not_all_zero] not_zero_i r all_zero_below_greatest
    unfolding reduced_row_echelon_form_upt_k_def 
    by fast
next
  fix i
  assume i: "i < i + 1" and not_zero_i: "¬ is_zero_row_upt_k i (Suc k) A" and not_zero_suc_i: "¬ is_zero_row_upt_k (i + 1) (Suc k) A"
  have not_zero_i_k: "¬ is_zero_row_upt_k i k A"
  using all_zero_below_greatest greatest_less_zero_row[OF r _ not_all_zero] not_zero_i by blast
  have not_zero_suc_i: "¬ is_zero_row_upt_k (i+1) k A"
     using all_zero_below_greatest greatest_less_zero_row[OF r _ not_all_zero] not_zero_suc_i by blast
  have aux:"(i j. i + 1 = j  i < j  ¬ is_zero_row_upt_k i k A  ¬ is_zero_row_upt_k j k A  (LEAST n. A $ i $ n  0) < (LEAST n. A $ j $ n  0))"
    using r unfolding reduced_row_echelon_form_upt_k_def by fast
  show "(LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)" using aux not_zero_i_k not_zero_suc_i i by simp
next
  fix i j assume "¬ is_zero_row_upt_k i (Suc k) A" and "i  j"
  thus "A $ j $ (LEAST n. A $ i $ n  0) = 0"
    using all_zero_below_greatest greatest_less_zero_row not_all_zero r rref_upt_condition4 by blast
qed

lemma rref_suc_if_all_rows_not_zero:
  fixes A::"'a::{one, zero}^'n::{mod_type}^'m::{finite,one,plus,linorder}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and all_not_zero: "n. ¬ is_zero_row_upt_k n k A"
  shows "reduced_row_echelon_form_upt_k A (Suc k)"
proof (rule rref_suc_if_zero_below_greatest)
  show "reduced_row_echelon_form_upt_k A k" using r .
  show "¬ (a. is_zero_row_upt_k a k A)" using all_not_zero by auto
  show "a>GREATEST m. ¬ is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
    using all_not_zero not_greater_Greatest by blast
qed


lemma greatest_ge_nonzero_row:
  fixes A::"'a::{zero}^'n::{mod_type}^'m::{finite,linorder}"
  assumes "¬ is_zero_row_upt_k i k A"
  shows "i  (GREATEST m. ¬ is_zero_row_upt_k m k A)" using Greatest_ge[of "(λm. ¬ is_zero_row_upt_k m k A)", OF assms] .

lemma greatest_ge_nonzero_row':
  fixes A::"'a::{zero, one}^'n::{mod_type}^'m::{finite, linorder, one, plus}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and i: "i  (GREATEST m. ¬ is_zero_row_upt_k m k A)"
  and not_all_zero: "¬ (a. is_zero_row_upt_k a k A)"
  shows "¬ is_zero_row_upt_k i k A"
  using greatest_less_zero_row[OF r] i not_all_zero by fastforce

corollary row_greater_greatest_is_zero:
  fixes A::"'a::{zero}^'n::{mod_type}^'m::{finite,linorder}"
  assumes "(GREATEST m. ¬ is_zero_row_upt_k m k A) < i"
  shows "is_zero_row_upt_k i k A" using greatest_ge_nonzero_row assms by fastforce

subsection‹The proof of its correctness›

text‹Properties of @{term "Gauss_Jordan_in_ij"}

lemma Gauss_Jordan_in_ij_1:
  fixes A::"'a::{field}^'m^'n::{finite, ord, wellorder}"
  assumes ex: "n. A $ n $ j  0  i  n"
  shows "(Gauss_Jordan_in_ij A i j) $ i $ j = 1"
proof (unfold Gauss_Jordan_in_ij_def Let_def mult_row_def interchange_rows_def, vector)
  obtain n where Anj: "A $ n $ j  0  i  n" using ex by blast
  show "A $ (LEAST n. A $ n $ j  0  i  n) $ j  0" using LeastI[of "λn. A $ n $ j  0  i  n" n, OF Anj] by simp 
qed

lemma Gauss_Jordan_in_ij_0:
  fixes A::"'a::{field}^'m^'n::{finite, ord, wellorder}"
  assumes ex: "n. A $ n $ j  0  i  n" and a: "a  i"
  shows "(Gauss_Jordan_in_ij A i j) $ a $ j = 0"
using ex apply (rule Gauss_Jordan_in_ij_unfold) using a by (simp add: mult_row_def interchange_rows_def row_add_def)

corollary Gauss_Jordan_in_ij_0':
  fixes A::"'a::{field}^'m^'n::{finite, ord, wellorder}"
  assumes ex: "n. A $ n $ j  0  i  n"
  shows "a. a  i  (Gauss_Jordan_in_ij A i j) $ a $ j = 0" using assms Gauss_Jordan_in_ij_0 by blast

lemma Gauss_Jordan_in_ij_preserves_previous_elements:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}"
  assumes r: "reduced_row_echelon_form_upt_k A k"
  and not_zero_a: "¬ is_zero_row_upt_k a k A"
  and exists_m: "m. A $ m $ (from_nat k)  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  m"
  and Greatest_plus_1: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  0"
  and j_le_k: "to_nat j < k"
  shows "Gauss_Jordan_in_ij A ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) (from_nat k) $ i $ j = A $ i $ j"
proof (unfold Gauss_Jordan_in_ij_def Let_def interchange_rows_def mult_row_def row_add_def, auto)
  define last_nonzero_row where "last_nonzero_row = (GREATEST m. ¬ is_zero_row_upt_k m k A)"
  have "last_nonzero_row < (last_nonzero_row + 1)" by (rule  Suc_le'[of last_nonzero_row], auto simp add: last_nonzero_row_def Greatest_plus_1)  
  hence zero_row: "is_zero_row_upt_k (last_nonzero_row + 1) k A"
    using not_le greatest_ge_nonzero_row last_nonzero_row_def by fastforce
  hence A_greatest_0: "A $ (last_nonzero_row + 1) $ j = 0" unfolding is_zero_row_upt_k_def last_nonzero_row_def using j_le_k by auto
  then show "A $ (last_nonzero_row + 1) $ j / A $ (last_nonzero_row + 1) $ from_nat k = A $ (last_nonzero_row + 1) $ j"
    by simp
  show zero: "A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ j = 0"
  proof -
    define least_n where "least_n = (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n)"
    have "n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n" by (metis exists_m)
    from this obtain n where n1: "A $ n $ from_nat k  0"  and n2: "(GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n" by blast
    have "(GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  least_n"
      by (metis (lifting, full_types) LeastI_ex least_n_def n1 n2)
    hence "is_zero_row_upt_k least_n k A" using last_nonzero_row_def less_le rref_upt_condition1[OF r] zero_row by metis
    thus "A $ least_n $ j = 0" unfolding is_zero_row_upt_k_def using j_le_k by simp
  qed
  show "A $ ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) $ j -
    A $ ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) $ from_nat k *
    A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ j /
    A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ from_nat k =
    A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ j"
    unfolding last_nonzero_row_def[symmetric] unfolding A_greatest_0 unfolding last_nonzero_row_def unfolding zero by fastforce
  show "A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ j /
    A $ (LEAST n. A $ n $ from_nat k  0  (GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  n) $ from_nat k =
    A $ ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) $ j" unfolding zero using A_greatest_0 unfolding last_nonzero_row_def by simp
qed



lemma Gauss_Jordan_in_ij_preserves_previous_elements':
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}"
  assumes all_zero: "n. is_zero_row_upt_k n k A"
  and j_le_k: "to_nat j < k"
  and A_nk_not_zero: "A $ n $ (from_nat k)  0"
  shows "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ j = A $ i $ j"
proof (unfold Gauss_Jordan_in_ij_def Let_def mult_row_def interchange_rows_def row_add_def, auto)
  have A_0_j: "A $ 0 $ j = 0"  using all_zero is_zero_row_upt_k_def j_le_k by blast
  then show "A $ 0 $ j / A $ 0 $ from_nat k = A $ 0 $ j" by simp
  show A_least_j: "A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ j = 0" using all_zero is_zero_row_upt_k_def j_le_k by blast
  show "A $ 0 $ j -
    A $ 0 $ from_nat k * A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ j /
    A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ from_nat k =
    A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ j" unfolding A_0_j A_least_j by fastforce
  show "A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ j / A $ (LEAST n. A $ n $ from_nat k  0  0  n) $ from_nat k = A $ 0 $ j"
    unfolding A_least_j A_0_j by simp
qed

lemma is_zero_after_Gauss:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  assumes zero_a: "is_zero_row_upt_k a k A"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and r: "reduced_row_echelon_form_upt_k A k"
  and greatest_less_ma: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k  0"
  shows "is_zero_row_upt_k a k (Gauss_Jordan_in_ij A ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) (from_nat k))"
proof (subst is_zero_row_upt_k_def, clarify)
  fix j::'n assume j_less_k: "to_nat j < k"
  have not_zero_g: "(GREATEST m. ¬ is_zero_row_upt_k m k A) + 1  0"
  proof (rule ccontr, simp)
    assume "(GREATEST m. ¬ is_zero_row_upt_k m k A) + 1 = 0"
    hence "(GREATEST m. ¬ is_zero_row_upt_k m k A) = -1" using a_eq_minus_1 by blast
    hence "a(GREATEST m. ¬ is_zero_row_upt_k m k A)" using Greatest_is_minus_1 by auto
    hence "¬ is_zero_row_upt_k a k A" using greatest_less_zero_row[OF r] not_zero_m by fastforce
    thus False using zero_a by contradiction
  qed
  have "Gauss_Jordan_in_ij A ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) (from_nat k) $ a $ j = A $ a $ j"
    by (rule Gauss_Jordan_in_ij_preserves_previous_elements[OF r not_zero_m _ not_zero_g j_less_k], auto intro!: A_ma_k_not_zero greatest_less_ma)
  also have "... = 0" 
    using zero_a j_less_k unfolding is_zero_row_upt_k_def by blast
  finally show "Gauss_Jordan_in_ij A ((GREATEST m. ¬ is_zero_row_upt_k m k A) + 1) (from_nat k) $ a $ j = 0" .
qed


lemma all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes all_zero: "n. is_zero_row_upt_k n k A"
  and not_zero_i: "¬ is_zero_row_upt_k i (Suc k) B"
  and Amk_zero: "A $ m $ from_nat k  0"
  shows "i=0"
proof (rule ccontr)
  assume i_not_0: "i  0"
  have ia2: "ia = 0" using ia all_zero by simp
  have B_eq_Gauss: "B = Gauss_Jordan_in_ij A 0 (from_nat k)"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2 
    using all_zero Amk_zero least_mod_type unfolding from_nat_0 nrows_def by auto
  also have "...$ i $ (from_nat k) = 0" proof (rule Gauss_Jordan_in_ij_0)
    show "n. A $ n $ from_nat k  0  0  n" using Amk_zero least_mod_type by blast
    show "i  0" using i_not_0 .
  qed
  finally have "B $ i $ from_nat k = 0" .
  hence "is_zero_row_upt_k i (Suc k) B"
    unfolding B_eq_Gauss
    using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero _ Amk_zero]
    by (metis all_zero is_zero_row_upt_k_def less_SucE to_nat_from_nat)
  thus False using not_zero_i by contradiction
qed

text‹Here we start to prove that 
      the output of @{term "Gauss Jordan A"} is a matrix in reduced row echelon form.›

lemma condition_1_part_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes zero_column_k: "mfrom_nat 0. A $ m $ from_nat k = 0"
  and all_zero: "m. is_zero_row_upt_k m k A"
  shows "is_zero_row_upt_k j (Suc k) A"
  unfolding is_zero_row_upt_k_def apply clarify
proof -
  fix ja::'columns assume ja_less_suc_k: "to_nat ja < Suc k"
  show "A $ j $ ja = 0"
  proof (cases "to_nat ja < k")
    case True thus ?thesis using all_zero unfolding is_zero_row_upt_k_def by blast
  next
    case False hence ja_eq_k: "k = to_nat ja " using ja_less_suc_k by simp
    show ?thesis using zero_column_k unfolding ja_eq_k from_nat_to_nat_id from_nat_0 using least_mod_type by blast
  qed
qed

lemma condition_1_part_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes j_not_zero: "j  0"
  and all_zero: "m. is_zero_row_upt_k m k A" 
  and Amk_not_zero: "A $ m $ from_nat k  0"
  shows "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A (from_nat 0) (from_nat k))"
proof (unfold is_zero_row_upt_k_def, clarify)
  fix ja::'columns
  assume ja_less_suc_k: "to_nat ja < Suc k"
  show "Gauss_Jordan_in_ij A (from_nat 0) (from_nat k) $ j $ ja = 0"
  proof (cases "to_nat ja < k")
    case True 
    have "Gauss_Jordan_in_ij A (from_nat 0) (from_nat k) $ j $ ja = A $ j $ ja"
      unfolding from_nat_0 using Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero True Amk_not_zero] .
    also have "... = 0" using all_zero True unfolding is_zero_row_upt_k_def by blast
    finally show ?thesis .
  next
    case False hence k_eq_ja: "k = to_nat ja"
      using ja_less_suc_k by simp
    show "Gauss_Jordan_in_ij A (from_nat 0) (from_nat k) $ j $ ja = 0"
      unfolding k_eq_ja from_nat_to_nat_id
    proof (rule Gauss_Jordan_in_ij_0)
      show "n. A $ n $ ja  0  from_nat 0  n"
        using least_mod_type Amk_not_zero
        unfolding k_eq_ja from_nat_to_nat_id from_nat_0 by blast
      show "j  from_nat 0" using j_not_zero unfolding from_nat_0 .
    qed
  qed
qed

lemma condition_1_part_3:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B (snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and i_less_j: "i<j"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and zero_below_greatest: "m(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B"
  shows "is_zero_row_upt_k j (Suc k) A"
proof (unfold is_zero_row_upt_k_def, auto)
  fix ja::'columns
  assume ja_less_suc_k: "to_nat ja < Suc k"
  have ia2: "ia=to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" unfolding ia using not_zero_m by presburger
  have B_eq_A: "B=A"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
    apply simp
    unfolding from_nat_to_nat_greatest using zero_below_greatest by blast
  have zero_ikA: "is_zero_row_upt_k i k A" using zero_i_suc_k unfolding B_eq_A is_zero_row_upt_k_def by fastforce
  hence zero_jkA: "is_zero_row_upt_k j k A" using rref_upt_condition1[OF rref] i_less_j by blast
  show "A $ j $ ja = 0"
  proof (cases "to_nat ja < k")
    case True
    thus ?thesis using zero_jkA unfolding is_zero_row_upt_k_def by blast
  next
    case False
    hence k_eq_ja:"k = to_nat ja" using ja_less_suc_k by auto
    have "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  j"
    proof (rule le_Suc, rule GreatestI2)
      show "¬ is_zero_row_upt_k m k A" using not_zero_m .
      fix x assume not_zero_xkA: "¬ is_zero_row_upt_k x k A" show "x < j"
        using rref_upt_condition1[OF rref] not_zero_xkA zero_jkA neq_iff by blast
    qed     
    thus ?thesis using zero_below_greatest unfolding k_eq_ja from_nat_to_nat_id is_zero_row_upt_k_def by blast
  qed
qed

lemma condition_1_part_4:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B (snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B" 
  and i_less_j: "i<j"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and greatest_eq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A)) = nrows A"
  shows "is_zero_row_upt_k j (Suc k) A"
proof -
  have ia2: "ia=to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" unfolding ia using not_zero_m by presburger
  have B_eq_A: "B=A"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
    unfolding from_nat_to_nat_greatest using greatest_eq_card nrows_def by force
  have rref_Suc: "reduced_row_echelon_form_upt_k A (Suc k)" 
  proof (rule rref_suc_if_zero_below_greatest[OF rref])
    show "a>GREATEST m. ¬ is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
      using greatest_eq_card not_less_eq to_nat_less_card to_nat_mono nrows_def by metis
    show "¬ (a. is_zero_row_upt_k a k A)" using not_zero_m by fast
  qed
  show ?thesis using zero_i_suc_k unfolding B_eq_A using rref_upt_condition1[OF rref_Suc] i_less_j by fast
qed


lemma condition_1_part_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B (snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B" 
  and i_less_j: "i<j"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and greatest_not_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A))  nrows A"
  and greatest_less_ma: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k  0"
  shows "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k))"
proof (subst (1) is_zero_row_upt_k_def, clarify)
  fix ja::'columns assume ja_less_suc_k: "to_nat ja < Suc k"
  have ia2: "ia=to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" unfolding ia using not_zero_m by presburger
  have B_eq_Gauss_ij: "B = Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k)"
    unfolding B Gauss_Jordan_column_k_def 
    unfolding ia2 Let_def fst_conv snd_conv
    using greatest_not_card greatest_less_ma A_ma_k_not_zero
    by (auto simp add: from_nat_to_nat_greatest nrows_def)
  have zero_ikA: "is_zero_row_upt_k i k A" 
  proof (unfold is_zero_row_upt_k_def, clarify)
    fix a::'columns
    assume a_less_k: "to_nat a < k"
    have "A $ i $ a = Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ a" 
    proof (rule Gauss_Jordan_in_ij_preserves_previous_elements[symmetric])
      show "reduced_row_echelon_form_upt_k A k" using rref .
      show "¬ is_zero_row_upt_k m k A" using not_zero_m .
      show "n. A $ n $ from_nat k  0  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  n" using A_ma_k_not_zero greatest_less_ma by blast
      show "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  0" using suc_not_zero greatest_not_card unfolding nrows_def by simp
      show "to_nat a < k" using a_less_k .
    qed
    also have "... = 0" unfolding B_eq_Gauss_ij[symmetric] using zero_i_suc_k a_less_k unfolding is_zero_row_upt_k_def by simp
    finally show "A $ i $ a = 0" .
  qed
  hence zero_jkA: "is_zero_row_upt_k j k A" using rref_upt_condition1[OF rref] i_less_j by blast
  show "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $ ja = 0"
  proof (cases "to_nat ja < k")
    case True
    have "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ j $ ja = A $ j $ ja" 
    proof (rule Gauss_Jordan_in_ij_preserves_previous_elements)
      show "reduced_row_echelon_form_upt_k A k" using rref .
      show "¬ is_zero_row_upt_k m k A" using not_zero_m .
      show "n. A $ n $ from_nat k  0  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  n" using A_ma_k_not_zero greatest_less_ma by blast
      show "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  0" using suc_not_zero greatest_not_card unfolding nrows_def by simp       
      show "to_nat ja < k" using True .
    qed
    also have "... = 0" using zero_jkA True unfolding is_zero_row_upt_k_def by fast
    finally show ?thesis .
  next
    case False hence k_eq_ja: "k = to_nat ja" using ja_less_suc_k by simp
    show ?thesis 
    proof (unfold k_eq_ja from_nat_to_nat_id, rule Gauss_Jordan_in_ij_0)
      show "n. A $ n $ ja  0  (GREATEST n. ¬ is_zero_row_upt_k n (to_nat ja) A) + 1  n"
        using A_ma_k_not_zero greatest_less_ma k_eq_ja to_nat_from_nat by auto
      show "j  (GREATEST n. ¬ is_zero_row_upt_k n (to_nat ja) A) + 1" 
      proof (unfold k_eq_ja[symmetric], rule ccontr)
        assume "¬ j  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1"
        hence j_eq: "j = (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" by fast
        hence "i < (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" using i_less_j by force
        hence i_le_greatest: "i  (GREATEST n. ¬ is_zero_row_upt_k n k A)" using le_Suc not_less by auto
        hence "¬ is_zero_row_upt_k i k A" using greatest_ge_nonzero_row'[OF rref] not_zero_m by fast
        thus "False" using zero_ikA by contradiction
      qed
    qed
  qed
qed


lemma condition_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and zero_i_suc_k: "is_zero_row_upt_k i (Suc k) B" and i_less_j: "i < j"
  shows "is_zero_row_upt_k j (Suc k) B"
proof (unfold B Gauss_Jordan_column_k_def ia Let_def fst_conv snd_conv, auto, unfold from_nat_to_nat_greatest)
  assume zero_k: "mfrom_nat 0. A $ m $ from_nat k = 0"  and all_zero: "m. is_zero_row_upt_k m k A"
  show "is_zero_row_upt_k j (Suc k) A"
    using condition_1_part_1[OF zero_k all_zero] .
next
  fix m
  assume all_zero: "m. is_zero_row_upt_k m k A" and Amk_not_zero: "A $ m $ from_nat k  0"
  have j_not_0: "j  0" using i_less_j least_mod_type not_le by blast
  show "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A (from_nat 0) (from_nat k))"
    using condition_1_part_2[OF j_not_0 all_zero Amk_not_zero] .
next
  fix m assume not_zero_mkA: "¬ is_zero_row_upt_k m k A"
    and zero_below_greatest: "m(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  show "is_zero_row_upt_k j (Suc k) A" using condition_1_part_3[OF rref i_less_j not_zero_mkA zero_below_greatest] zero_i_suc_k
    unfolding B ia .
next
  fix m assume not_zero_m: "¬ is_zero_row_upt_k m k A"
    and greatest_eq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A)) =  nrows A"
  show "is_zero_row_upt_k j (Suc k) A"
    using condition_1_part_4[OF rref _ i_less_j not_zero_m greatest_eq_card] zero_i_suc_k unfolding B ia nrows_def .
next
  fix m ma
  assume not_zero_m: "¬ is_zero_row_upt_k m k A"
    and greatest_not_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A))  nrows A"
and greatest_less_ma: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  ma"
    and A_ma_k_not_zero: "A $ ma $ from_nat k  0"
  show "is_zero_row_upt_k j (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k))"
    using condition_1_part_5[OF rref _ i_less_j not_zero_m greatest_not_card greatest_less_ma A_ma_k_not_zero]
    using zero_i_suc_k
    unfolding B ia .
qed



lemma condition_2_part_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and all_zero: "m. is_zero_row_upt_k m k A"
  and all_zero_k: "m. A $ m $ from_nat k = 0"
  shows "A $ i $ (LEAST k. A $ i $ k  0) = 1"
proof -
  have ia2: "ia = 0" using ia all_zero by simp
  have B_eq_A: "B=A" unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2 using all_zero_k by fastforce
  show ?thesis  using all_zero_k condition_1_part_1[OF _ all_zero] not_zero_i_suc_k unfolding B_eq_A by presburger
qed


lemma condition_2_part_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and all_zero: "m. is_zero_row_upt_k m k A"
  and Amk_not_zero: "A $ m $ from_nat k  0"
  shows "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ ka  0) = 1"
proof -
  have ia2: "ia = 0" unfolding ia using all_zero by simp
  have B_eq: "B = Gauss_Jordan_in_ij A 0 (from_nat k)" unfolding B Gauss_Jordan_column_k_def unfolding ia2 Let_def fst_conv snd_conv
    using Amk_not_zero least_mod_type unfolding from_nat_0 nrows_def by auto
  have i_eq_0: "i=0" using Amk_not_zero B_eq all_zero condition_1_part_2 from_nat_0 not_zero_i_suc_k by metis
  have Least_eq: "(LEAST ka. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ ka  0) = from_nat k"
  proof (rule Least_equality)
    have "Gauss_Jordan_in_ij A 0 (from_nat k) $ 0 $ from_nat k = 1" using Gauss_Jordan_in_ij_1 Amk_not_zero least_mod_type by blast
    thus "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ from_nat k  0" unfolding i_eq_0 by simp
    fix y assume not_zero_gauss: "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ y  0"
    show "from_nat k  y"
    proof (rule ccontr)
      assume "¬ from_nat k  y" hence y: "y < from_nat k" by force
      have "Gauss_Jordan_in_ij A 0 (from_nat k) $ 0 $ y = A $ 0 $ y"
        by (rule Gauss_Jordan_in_ij_preserves_previous_elements'[OF all_zero to_nat_le[OF y] Amk_not_zero])
      also have "... = 0" using all_zero to_nat_le[OF y] unfolding is_zero_row_upt_k_def by blast
      finally show "False" using not_zero_gauss unfolding i_eq_0 by contradiction
    qed
  qed
  show ?thesis unfolding Least_eq unfolding i_eq_0 by (rule Gauss_Jordan_in_ij_1, auto intro!: Amk_not_zero least_mod_type)
qed




lemma condition_2_part_3:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and zero_below_greatest: "m(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0"
  shows "A $ i $ (LEAST k. A $ i $ k  0) = 1"
proof -
  have ia2: "ia=to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" unfolding ia using not_zero_m by presburger
  have B_eq_A: "B=A"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
    apply simp
    unfolding from_nat_to_nat_greatest using zero_below_greatest by blast
  show ?thesis
  proof (cases "to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1 < CARD('rows)")
    case True
    have "¬ is_zero_row_upt_k i k A"
    proof -
      have "i<(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1"
      proof (rule ccontr)
        assume "¬ i < (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1"
        hence i: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  i" by simp
        hence "(GREATEST n. ¬ is_zero_row_upt_k n k A) < i" using le_Suc' True by simp
        hence zero_i: "is_zero_row_upt_k i k A" using not_greater_Greatest by blast
        hence "is_zero_row_upt_k i (Suc k) A" 
        proof (unfold is_zero_row_upt_k_def, clarify)
          fix j::'columns 
          assume "to_nat j < Suc k"
          thus "A $ i $ j = 0"
            using zero_i unfolding is_zero_row_upt_k_def using zero_below_greatest i 
            by (metis from_nat_to_nat_id le_neq_implies_less not_le not_less_eq_eq)
        qed        
        thus False using not_zero_i_suc_k unfolding B_eq_A by contradiction
      qed
      hence "i(GREATEST n. ¬ is_zero_row_upt_k n k A)" using not_le le_Suc by metis
      thus ?thesis using greatest_ge_nonzero_row'[OF rref] not_zero_m by fast
    qed
    thus ?thesis using rref_upt_condition2[OF rref] by blast
  next
    case False
    have greatest_plus_one_eq_0: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1 = 0"
      using to_nat_plus_one_less_card False by blast
    have "¬ is_zero_row_upt_k i k A"
    proof (rule not_is_zero_row_upt_suc)
      show "¬ is_zero_row_upt_k i (Suc k) A" using not_zero_i_suc_k unfolding B_eq_A .
      show "i. A $ i $ from_nat k = 0"
        using zero_below_greatest
        unfolding greatest_plus_one_eq_0 using least_mod_type by blast
    qed
    thus ?thesis using rref_upt_condition2[OF rref] by blast
  qed
qed

lemma condition_2_part_4:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and greatest_eq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A)) = nrows A"
  shows "A $ i $ (LEAST k. A $ i $ k  0) = 1"
proof -
  have "¬ is_zero_row_upt_k i k A"
  proof (rule ccontr, simp)
    assume zero_i: "is_zero_row_upt_k i k A"
    hence zero_minus_1: "is_zero_row_upt_k (-1) k A"
      using rref_upt_condition1[OF rref]
      using Greatest_is_minus_1 neq_le_trans by metis 
    have "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1 = 0" using greatest_plus_one_eq_0[OF greatest_eq_card] .
    hence greatest_eq_minus_1: "(GREATEST n. ¬ is_zero_row_upt_k n k A) = -1" using a_eq_minus_1 by fast
    have "¬ is_zero_row_upt_k (GREATEST n. ¬ is_zero_row_upt_k n k A) k A"
      by (rule greatest_ge_nonzero_row'[OF rref _ ], auto intro!: not_zero_m)
    thus "False" using zero_minus_1 unfolding greatest_eq_minus_1 by contradiction
  qed
  thus ?thesis using rref_upt_condition2[OF rref] by blast
qed


lemma condition_2_part_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and not_zero_m: "¬ is_zero_row_upt_k m k A"
  and greatest_noteq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A))  nrows A"
  and greatest_less_ma: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k  0"
  shows "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $
  (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0) = 1"
proof -
  have ia2: "ia=to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" unfolding ia using not_zero_m by presburger
  have B_eq_Gauss: "B=Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k)"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
    apply simp
    unfolding from_nat_to_nat_greatest using greatest_noteq_card A_ma_k_not_zero greatest_less_ma by blast
  have greatest_plus_one_not_zero: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  0"
    using suc_not_zero greatest_noteq_card unfolding nrows_def by auto
  show ?thesis
  proof (cases "is_zero_row_upt_k i k A")
    case True
    hence not_zero_iB: "is_zero_row_upt_k i k B" unfolding is_zero_row_upt_k_def unfolding B_eq_Gauss
      using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero]
      using A_ma_k_not_zero greatest_less_ma by fastforce
    hence Gauss_Jordan_i_not_0: "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k)  0"
      using not_zero_i_suc_k unfolding B_eq_Gauss unfolding is_zero_row_upt_k_def using from_nat_to_nat_id less_Suc_eq by (metis (lifting, no_types))
    have "i = ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
    proof (rule ccontr)
      assume i_not_greatest: "i  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1"
      have "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 0"
      proof (rule Gauss_Jordan_in_ij_0)
        show "n. A $ n $ from_nat k  0  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  n" using A_ma_k_not_zero greatest_less_ma by blast
        show "i  (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1" using i_not_greatest .
      qed
      thus False using Gauss_Jordan_i_not_0 by contradiction
    qed
    hence Gauss_Jordan_i_1: "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 1"
      using Gauss_Jordan_in_ij_1 using A_ma_k_not_zero greatest_less_ma by blast
    have Least_eq_k: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0) = from_nat k"
    proof (rule Least_equality)
      show "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ from_nat k  0" using Gauss_Jordan_i_not_0 .
      show  "y. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y  0  from_nat k  y"
        using B_eq_Gauss is_zero_row_upt_k_def not_less not_zero_iB to_nat_le by fast
    qed
    show ?thesis using Gauss_Jordan_i_1 unfolding Least_eq_k .
  next
    case False
    obtain j where Aij_not_0: "A $ i $ j  0" and j_le_k: "to_nat j < k" using False unfolding is_zero_row_upt_k_def by auto
    have least_le_k: "to_nat (LEAST ka. A $ i $ ka  0) < k"
      by (metis (lifting, mono_tags) Aij_not_0 j_le_k less_trans linorder_cases not_less_Least to_nat_mono)
    have least_le_j: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0)  j"
      using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero j_le_k] using A_ma_k_not_zero greatest_less_ma
      using Aij_not_0 False not_le_imp_less not_less_Least by (metis (mono_tags))
    have Least_eq: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0) 
      = (LEAST ka. A $ i $ ka  0)"
    proof (rule Least_equality)
      show "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (LEAST ka. A $ i $ ka  0)  0" 
        using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref False _ greatest_plus_one_not_zero] least_le_k False rref_upt_condition2[OF rref]
        using  A_ma_k_not_zero B_eq_Gauss greatest_less_ma zero_neq_one by fastforce
      fix y assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y  0"
      show "(LEAST ka. A $ i $ ka  0)  y"
      proof (cases "to_nat y < k")
        case False 
        thus ?thesis
          using least_le_k less_trans not_le_imp_less to_nat_from_nat to_nat_le by metis
      next
        case True
        have "A $ i $ y  0" using Gauss_Jordan_y using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero True]
          using A_ma_k_not_zero greatest_less_ma by fastforce
        thus ?thesis using Least_le by fastforce
      qed
    qed
    have "A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0) = 1"
      using False using rref_upt_condition2[OF rref] unfolding Least_eq by blast   
    thus ?thesis unfolding Least_eq using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref False _ greatest_plus_one_not_zero]
      using least_le_k A_ma_k_not_zero greatest_less_ma by fastforce
  qed
qed


lemma condition_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  shows "B $ i $ (LEAST k. B $ i $ k  0) = 1"
proof (unfold B Gauss_Jordan_column_k_def ia Let_def fst_conv snd_conv, auto, unfold from_nat_to_nat_greatest from_nat_0)
  assume all_zero: "m. is_zero_row_upt_k m k A" and all_zero_k: "m0. A $ m $ from_nat k = 0"
  show "A $ i $ (LEAST k. A $ i $ k  0) = 1"
    using condition_2_part_1[OF _ all_zero] not_zero_i_suc_k all_zero_k least_mod_type unfolding B ia by blast
next
  fix m assume all_zero: "m. is_zero_row_upt_k m k A"
    and Amk_not_zero: "A $ m $ from_nat k  0"
  show "Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ ka  0) = 1"
    using condition_2_part_2[OF _ all_zero Amk_not_zero] not_zero_i_suc_k unfolding B ia .
next
  fix m
  assume not_zero_m: "¬ is_zero_row_upt_k m k A"
    and zero_below_greatest: "m(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1. A $ m $ from_nat k = 0" 
  show "A $ i $ (LEAST k. A $ i $ k  0) = 1" using condition_2_part_3[OF rref _ not_zero_m zero_below_greatest] not_zero_i_suc_k unfolding B ia .
next
  fix m 
  assume not_zero_m: "¬ is_zero_row_upt_k m k A"
    and greatest_eq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A)) = nrows A"
  show "A $ i $ (LEAST k. A $ i $ k  0) = 1" using condition_2_part_4[OF rref not_zero_m greatest_eq_card] .
next
  fix m ma
  assume not_zero_m: "¬ is_zero_row_upt_k m k A"
    and greatest_noteq_card: "Suc (to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A))  nrows A"
    and greatest_less_ma: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1  ma"
    and A_ma_k_not_zero: "A $ ma $ from_nat k  0"
  show "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i 
    $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka  0) = 1"
    using condition_2_part_5[OF rref _ not_zero_m greatest_noteq_card greatest_less_ma A_ma_k_not_zero] not_zero_i_suc_k unfolding B ia .
qed


lemma condition_3_part_1:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and all_zero: "m. is_zero_row_upt_k m k A"
  and all_zero_k: "m. A $ m $ from_nat k = 0"
  shows "(LEAST n. A $ i $ n  0) < (LEAST n. A $ (i + 1) $ n  0)"
proof -
  have ia2: "ia = 0" using ia all_zero by simp
  have B_eq_A: "B=A" unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2 using all_zero_k by fastforce
  have "is_zero_row_upt_k i (Suc k) B"  using all_zero all_zero_k unfolding B_eq_A is_zero_row_upt_k_def by (metis less_SucE to_nat_from_nat)
  thus ?thesis using not_zero_i_suc_k by contradiction
qed



lemma condition_3_part_2:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia(if m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
  defines B:"B(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes i_le: "i < i + 1"
  and not_zero_i_suc_k: "¬ is_zero_row_upt_k i (Suc k) B"
  and not_zero_suc_i_suc_k: "¬ is_zero_row_upt_k (i + 1) (Suc k) B"
  and all_zero: "m. is_zero_row_upt_k m k A"
  and Amk_notzero: "A $ m $ from_nat k  0"
  shows "(LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ i $ n  0) < (LEAST n. Gauss_Jordan_in_ij A 0 (from_nat k) $ (i + 1) $ n  0)"
proof -
  have ia2: "ia = 0" using ia all_zero by simp
  have B_eq_Gauss: "B = Gauss_Jordan_in_ij A 0 (from_nat k)"
    unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2 
    using all_zero Amk_notzero least_mod_type unfolding from_nat_0 by auto
  have "i=0" using all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0[OF all_zero _ Amk_notzero] not_zero_i_suc_k unfolding B ia .
  moreover have "i+1=0" using all_zero_imp_Gauss_Jordan_column_not_zero_in_row_0[OF all_zero _ Amk_notzero] not_zero_suc_i_suc_k unfolding B ia .
  ultimately show ?thesis using i_le by auto
qed



lemma condition_3_part_3: