Theory Gauss_Jordan
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)"
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: "∀m≥from_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: "∀m≥from_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: "∀m≥0. 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:
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_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 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 "(LEAST n. A $ i $ n ≠ 0) < (LEAST n. A $ (i + 1) $ n ≠ 0)"
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
have rref_suc: "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 rref .
show "¬ (∀a. is_zero_row_upt_k a k A)" using not_zero_m by fast
show "∀a>GREATEST m. ¬ is_zero_row_upt_k m k A. is_zero_row_upt_k a (Suc k) A"
proof (clarify)
fix a::'rows assume greatest_less_a: "(GREATEST m. ¬ is_zero_row_upt_k m k A) < a"
show "is_zero_row_upt_k a (Suc k) A"
proof (rule is_zero_row_upt_k_suc)
show "is_zero_row_upt_k a k A" using greatest_less_a row_greater_greatest_is_zero by fast
show "A $ a $ from_nat k = 0" using le_Suc[OF greatest_less_a] zero_below_greatest by fast
qed
qed
qed
show ?thesis using rref_upt_condition3[OF rref_suc] i_le not_zero_i_suc_k not_zero_suc_i_suc_k unfolding B_eq_A by blast
qed
lemma condition_3_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 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 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 "(LEAST n. A $ i $ n ≠ 0) < (LEAST n. A $ (i + 1) $ n ≠ 0)"
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 by simp
have greatest_eq_minus_1: "(GREATEST n. ¬ is_zero_row_upt_k n k A) = -1"
using a_eq_minus_1 greatest_eq_card to_nat_plus_one_less_card unfolding nrows_def by fastforce
have rref_suc: "reduced_row_echelon_form_upt_k A (Suc k)"
proof (rule rref_suc_if_all_rows_not_zero)
show "reduced_row_echelon_form_upt_k A k" using rref .
show "∀n. ¬ is_zero_row_upt_k n k A" using Greatest_is_minus_1 greatest_eq_minus_1 greatest_ge_nonzero_row'[OF rref _] not_zero_m by metis
qed
show ?thesis using rref_upt_condition3[OF rref_suc] i_le not_zero_i_suc_k not_zero_suc_i_suc_k unfolding B_eq_A by blast
qed
lemma condition_3_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 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 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 "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n ≠ 0)
< (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i + 1) $ n ≠ 0)"
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
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)
have suc_greatest_not_zero: "(GREATEST n. ¬ is_zero_row_upt_k n k A) + 1 ≠ 0"
using Suc_eq_plus1 suc_not_zero greatest_not_card unfolding nrows_def by auto
show ?thesis
proof (cases "is_zero_row_upt_k (i + 1) k A")
case True
have zero_i_plus_one_k_B: "is_zero_row_upt_k (i+1) k B"
by (unfold B_eq_Gauss, rule is_zero_after_Gauss[OF True not_zero_m rref greatest_less_ma A_ma_k_not_zero])
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+1) $ (from_nat k) ≠ 0"
using not_zero_suc_i_suc_k unfolding B_eq_Gauss using is_zero_row_upt_k_suc by blast
have i_plus_one_eq: "i + 1 = ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1)"
proof (rule ccontr)
assume i_not_greatest: "i + 1 ≠ (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 + 1) $ (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 greatest_less_ma A_ma_k_not_zero by blast
show "i + 1 ≠ (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 i_eq_greatest: "i=(GREATEST n. ¬ is_zero_row_upt_k n k A)" using add_right_cancel by simp
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+1) $ 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+1) $ from_nat k ≠ 0" by (metis Gauss_Jordan_i_not_0)
fix y assume "Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ (i+1) $ y ≠ 0"
thus "from_nat k ≤ y" using zero_i_plus_one_k_B unfolding i_eq_greatest B_eq_Gauss by (metis is_zero_row_upt_k_def not_less to_nat_le)
qed
have not_zero_i_A: "¬ is_zero_row_upt_k i k A" using greatest_less_zero_row[OF rref] not_zero_m unfolding i_eq_greatest by fast
from this obtain j where Aij_not_0: "A $ i $ j ≠ 0" and j_le_k: "to_nat j < k" unfolding is_zero_row_upt_k_def by blast
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_eq: " (LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n ≠ 0) =
(LEAST n. A $ i $ n ≠ 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 not_zero_i_A _ suc_greatest_not_zero least_le_k] greatest_less_ma A_ma_k_not_zero
using rref_upt_condition2[OF rref] not_zero_i_A 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 by (metis not_le least_le_k less_trans to_nat_mono)
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 _ suc_greatest_not_zero True]
using A_ma_k_not_zero greatest_less_ma by fastforce
thus ?thesis using Least_le by fastforce
qed
qed
also have "... < from_nat k" by (metis is_zero_row_upt_k_def is_zero_row_upt_k_suc le_less_linear le_less_trans least_le_k not_zero_suc_i_suc_k to_nat_mono' zero_i_plus_one_k_B)
finally show ?thesis unfolding Least_eq_k .
next
case False
have not_zero_i_A: "¬ is_zero_row_upt_k i k A" using rref_upt_condition1[OF rref] False i_le by blast
from this obtain j where Aij_not_0: "A $ i $ j ≠ 0" and j_le_k: "to_nat j < k" unfolding is_zero_row_upt_k_def by blast
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_i_eq: "(LEAST n. Gauss_Jordan_in_ij A ((GREATEST n. ¬ is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ n ≠ 0)
= (LEAST n. A $ i $ n ≠ 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 not_zero_i_A _ suc_greatest_not_zero least_le_k] greatest_less_ma A_ma_k_not_zero
using rref_upt_condition2[OF rref] not_zero_i_A 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 by (metis not_le not_less_iff_gr_or_eq le_less_trans least_le_k to_nat_mono)
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 _ suc_greatest_not_zero True]
using A_ma_k_not_zero greatest_less_ma by fastforce
thus ?thesis using Least_le by fastforce
qed
qed
from False obtain s