[STATEMENT]
lemma vec_to_iarray_greatest_not_zero:
assumes ex_b: "(\<exists>b. A $ b \<noteq> 0)"
shows "greatest_not_zero (vec_to_iarray A) = to_nat (GREATEST b. A $ b \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
let ?P="(\<lambda>n. (vec_to_iarray A) !! n \<noteq> 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
let ?xs="(rev [0..<IArray.length (vec_to_iarray A)])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
have "\<exists>a. (List.find ?P ?xs) = Some a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a
[PROOF STEP]
proof(rule ccontr, simp, unfold find_None_iff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<exists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
\<nexists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b)

goal (1 subgoal):
 1. \<nexists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b)

goal (1 subgoal):
 1. False
[PROOF STEP]
using ex_b
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set (rev [0..<length (IArray.list_of (vec_to_iarray A))]) \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b)
\<exists>b. A $ b \<noteq> (0::'b)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding set_rev
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set [0..<length (IArray.list_of (vec_to_iarray A))] \<and> IArray.list_of (vec_to_iarray A) ! x \<noteq> (0::'b)
\<exists>b. A $ b \<noteq> (0::'b)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto, unfold IArray.length_def[symmetric] IArray.sub_def[symmetric] length_vec_to_iarray,metis to_nat_less_card vec_to_iarray_nth')
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a
[PROOF STEP]
obtain a where a: "(List.find ?P ?xs) = Some a"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a

goal (1 subgoal):
 1. (\<And>a. find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a
[PROOF STEP]
obtain ia where ia_less_length: "ia<length ?xs"
and P_xs_ia: "?P (?xs!ia)" and a_eq: "a = ?xs!ia" and all_zero: "(\<forall>j<ia. \<not> ?P (?xs!j))"
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>n. vec_to_iarray A !! n \<noteq> (0::'b)) (rev [0..<IArray.length (vec_to_iarray A)]) = Some a

goal (1 subgoal):
 1. (\<And>ia. \<lbrakk>ia < length (rev [0..<IArray.length (vec_to_iarray A)]); vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ia) \<noteq> (0::'b); a = rev [0..<IArray.length (vec_to_iarray A)] ! ia; \<forall>j<ia. \<not> vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! j) \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding find_Some_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>i<length (rev [0..<IArray.length (vec_to_iarray A)]). vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! i) \<noteq> (0::'b) \<and> a = rev [0..<IArray.length (vec_to_iarray A)] ! i \<and> (\<forall>j<i. \<not> vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! j) \<noteq> (0::'b))

goal (1 subgoal):
 1. (\<And>ia. \<lbrakk>ia < length (rev [0..<IArray.length (vec_to_iarray A)]); vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ia) \<noteq> (0::'b); a = rev [0..<IArray.length (vec_to_iarray A)] ! ia; \<forall>j<ia. \<not> vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! j) \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ia < length (rev [0..<IArray.length (vec_to_iarray A)])
vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ia) \<noteq> (0::'b)
a = rev [0..<IArray.length (vec_to_iarray A)] ! ia
\<forall>j<ia. \<not> vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! j) \<noteq> (0::'b)

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
have ia_less_card: "ia < CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < CARD('a)
[PROOF STEP]
using ia_less_length
[PROOF STATE]
proof (prove)
using this:
ia < length (rev [0..<IArray.length (vec_to_iarray A)])

goal (1 subgoal):
 1. ia < CARD('a)
[PROOF STEP]
by (metis diff_zero length_rev length_upt length_vec_to_iarray)
[PROOF STATE]
proof (state)
this:
ia < CARD('a)

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
have ia_less_length': "ia < length ([0..<IArray.length (vec_to_iarray A)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
using ia_less_length
[PROOF STATE]
proof (prove)
using this:
ia < length (rev [0..<IArray.length (vec_to_iarray A)])

goal (1 subgoal):
 1. ia < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
unfolding length_rev
[PROOF STATE]
proof (prove)
using this:
ia < length [0..<IArray.length (vec_to_iarray A)]

goal (1 subgoal):
 1. ia < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ia < length [0..<IArray.length (vec_to_iarray A)]

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
have a_less_card: "a < CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < CARD('a)
[PROOF STEP]
unfolding a_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<IArray.length (vec_to_iarray A)] ! ia < CARD('a)
[PROOF STEP]
unfolding rev_nth[OF ia_less_length']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) < CARD('a)
[PROOF STEP]
using nth_upt[of 0 "(length [0..<IArray.length (vec_to_iarray A)] - Suc ia)" "(length [0..<IArray.length (vec_to_iarray A)])" ]
[PROOF STATE]
proof (prove)
using this:
0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) < length [0..<IArray.length (vec_to_iarray A)] \<Longrightarrow> [0..<length [0..<IArray.length (vec_to_iarray A)]] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)

goal (1 subgoal):
 1. [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) < CARD('a)
[PROOF STEP]
by (metis diff_less length_upt length_vec_to_iarray minus_nat.diff_0 plus_nat.add_0 zero_less_Suc zero_less_card_finite)
[PROOF STATE]
proof (state)
this:
a < CARD('a)

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
have "(GREATEST b. A $ b \<noteq> 0) = from_nat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST b. A $ b \<noteq> (0::'b)) = mod_type_class.from_nat a
[PROOF STEP]
proof (rule Greatest_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ mod_type_class.from_nat a \<noteq> (0::'b)
 2. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
have "A $ from_nat a = (vec_to_iarray A) !! a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ mod_type_class.from_nat a = vec_to_iarray A !! a
[PROOF STEP]
by (rule vec_to_iarray_nth[symmetric,OF a_less_card])
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat a = vec_to_iarray A !! a

goal (2 subgoals):
 1. A $ mod_type_class.from_nat a \<noteq> (0::'b)
 2. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat a = vec_to_iarray A !! a

goal (2 subgoals):
 1. A $ mod_type_class.from_nat a \<noteq> (0::'b)
 2. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
have "... \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray A !! a \<noteq> (0::'b)
[PROOF STEP]
using P_xs_ia
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ia) \<noteq> (0::'b)

goal (1 subgoal):
 1. vec_to_iarray A !! a \<noteq> (0::'b)
[PROOF STEP]
unfolding a_eq[symmetric]
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray A !! a \<noteq> (0::'b)

goal (1 subgoal):
 1. vec_to_iarray A !! a \<noteq> (0::'b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vec_to_iarray A !! a \<noteq> (0::'b)

goal (2 subgoals):
 1. A $ mod_type_class.from_nat a \<noteq> (0::'b)
 2. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $ mod_type_class.from_nat a \<noteq> (0::'b)
[PROOF STEP]
show "A $ from_nat a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat a \<noteq> (0::'b)

goal (1 subgoal):
 1. A $ mod_type_class.from_nat a \<noteq> (0::'b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat a \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
assume Ay: "A $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
A $ y \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>y. A $ y \<noteq> (0::'b) \<Longrightarrow> y \<le> mod_type_class.from_nat a
[PROOF STEP]
show "y \<le> from_nat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> mod_type_class.from_nat a
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
assume "\<not> y \<le> from_nat a"
[PROOF STATE]
proof (state)
this:
\<not> y \<le> mod_type_class.from_nat a

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
hence y_greater_a: "y > from_nat a"
[PROOF STATE]
proof (prove)
using this:
\<not> y \<le> mod_type_class.from_nat a

goal (1 subgoal):
 1. mod_type_class.from_nat a < y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat a < y

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have y_greater_a': "to_nat y > a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < mod_type_class.to_nat y
[PROOF STEP]
using y_greater_a
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat a < y

goal (1 subgoal):
 1. a < mod_type_class.to_nat y
[PROOF STEP]
using to_nat_mono[of "from_nat a" y]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat a < y
mod_type_class.from_nat a < y \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat a) < mod_type_class.to_nat y

goal (1 subgoal):
 1. a < mod_type_class.to_nat y
[PROOF STEP]
using to_nat_from_nat_id
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat a < y
mod_type_class.from_nat a < y \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat a) < mod_type_class.to_nat y
?x < CARD(?'a) \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat ?x) = ?x

goal (1 subgoal):
 1. a < mod_type_class.to_nat y
[PROOF STEP]
by (metis a_less_card)
[PROOF STATE]
proof (state)
this:
a < mod_type_class.to_nat y

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "a = ?xs ! ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = rev [0..<IArray.length (vec_to_iarray A)] ! ia
[PROOF STEP]
using a_eq
[PROOF STATE]
proof (prove)
using this:
a = rev [0..<IArray.length (vec_to_iarray A)] ! ia

goal (1 subgoal):
 1. a = rev [0..<IArray.length (vec_to_iarray A)] ! ia
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = rev [0..<IArray.length (vec_to_iarray A)] ! ia

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a = rev [0..<IArray.length (vec_to_iarray A)] ! ia

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<IArray.length (vec_to_iarray A)] ! ia = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)
[PROOF STEP]
by (rule rev_nth[OF ia_less_length'])
[PROOF STATE]
proof (state)
this:
rev [0..<IArray.length (vec_to_iarray A)] ! ia = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rev [0..<IArray.length (vec_to_iarray A)] ! ia = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)
[PROOF STEP]
apply (rule nth_upt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) < IArray.length (vec_to_iarray A)
[PROOF STEP]
using ia_less_length'
[PROOF STATE]
proof (prove)
using this:
ia < length [0..<IArray.length (vec_to_iarray A)]

goal (1 subgoal):
 1. 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) < IArray.length (vec_to_iarray A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = length [0..<IArray.length (vec_to_iarray A)] - Suc ia
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ia) = length [0..<IArray.length (vec_to_iarray A)] - Suc ia

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a = length [0..<IArray.length (vec_to_iarray A)] - Suc ia
[PROOF STEP]
have "a = (length [0..<IArray.length (vec_to_iarray A)] - Suc ia)"
[PROOF STATE]
proof (prove)
using this:
a = length [0..<IArray.length (vec_to_iarray A)] - Suc ia

goal (1 subgoal):
 1. a = length [0..<IArray.length (vec_to_iarray A)] - Suc ia
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = length [0..<IArray.length (vec_to_iarray A)] - Suc ia

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
hence ia_eq: "ia = length [0..<IArray.length (vec_to_iarray A)] - (Suc a)"
[PROOF STATE]
proof (prove)
using this:
a = length [0..<IArray.length (vec_to_iarray A)] - Suc ia

goal (1 subgoal):
 1. ia = length [0..<IArray.length (vec_to_iarray A)] - Suc a
[PROOF STEP]
by (metis Suc_diff_Suc Suc_eq_plus1_left diff_diff_cancel less_imp_le ia_less_length length_rev)
[PROOF STATE]
proof (state)
this:
ia = length [0..<IArray.length (vec_to_iarray A)] - Suc a

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
define ja where "ja = length [0..<IArray.length (vec_to_iarray A)] - to_nat y - 1"
[PROOF STATE]
proof (state)
this:
ja = length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have ja_less_length: "ja < length [0..<IArray.length (vec_to_iarray A)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ja < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
unfolding ja_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1 < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
using ia_eq ia_less_length'
[PROOF STATE]
proof (prove)
using this:
ia = length [0..<IArray.length (vec_to_iarray A)] - Suc a
ia < length [0..<IArray.length (vec_to_iarray A)]

goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1 < length [0..<IArray.length (vec_to_iarray A)]
[PROOF STEP]
by (simp add: algebra_simps )
[PROOF STATE]
proof (state)
this:
ja < length [0..<IArray.length (vec_to_iarray A)]

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have suc_i_le: "IArray.length (vec_to_iarray A)\<ge>Suc (to_nat y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat y) \<le> IArray.length (vec_to_iarray A)
[PROOF STEP]
unfolding vec_to_iarray_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat y) \<le> IArray.length (IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat i) CARD('a))
[PROOF STEP]
using to_nat_less_card[of y]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat y < CARD('a)

goal (1 subgoal):
 1. Suc (mod_type_class.to_nat y) \<le> IArray.length (IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat i) CARD('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (mod_type_class.to_nat y) \<le> IArray.length (vec_to_iarray A)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "?xs ! ja = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev [0..<IArray.length (vec_to_iarray A)] ! ja = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)
[PROOF STEP]
unfolding rev_nth[OF ja_less_length]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rev [0..<IArray.length (vec_to_iarray A)] ! ja = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rev [0..<IArray.length (vec_to_iarray A)] ! ja = [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)
[PROOF STEP]
apply (rule nth_upt, auto simp del: IArray.length_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (vec_to_iarray A) - Suc ja < IArray.length (vec_to_iarray A)
[PROOF STEP]
unfolding ja_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (vec_to_iarray A) - Suc (length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1) < IArray.length (vec_to_iarray A)
[PROOF STEP]
by (metis diff_Suc_less ia_less_length' length_upt less_nat_zero_code minus_nat.diff_0 neq0_conv)
[PROOF STATE]
proof (state)
this:
[0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[0..<IArray.length (vec_to_iarray A)] ! (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = (length [0..<IArray.length (vec_to_iarray A)] - Suc ja)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = length [0..<IArray.length (vec_to_iarray A)] - Suc ja
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = length [0..<IArray.length (vec_to_iarray A)] - Suc ja

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 + (length [0..<IArray.length (vec_to_iarray A)] - Suc ja) = length [0..<IArray.length (vec_to_iarray A)] - Suc ja

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have "... = to_nat y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - Suc ja = mod_type_class.to_nat y
[PROOF STEP]
unfolding ja_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - Suc (length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1) = mod_type_class.to_nat y
[PROOF STEP]
using suc_i_le
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat y) \<le> IArray.length (vec_to_iarray A)

goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - Suc (length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1) = mod_type_class.to_nat y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
length [0..<IArray.length (vec_to_iarray A)] - Suc ja = mod_type_class.to_nat y

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rev [0..<IArray.length (vec_to_iarray A)] ! ja = mod_type_class.to_nat y
[PROOF STEP]
have xs_ja_eq_y: "?xs ! ja = to_nat y"
[PROOF STATE]
proof (prove)
using this:
rev [0..<IArray.length (vec_to_iarray A)] ! ja = mod_type_class.to_nat y

goal (1 subgoal):
 1. rev [0..<IArray.length (vec_to_iarray A)] ! ja = mod_type_class.to_nat y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rev [0..<IArray.length (vec_to_iarray A)] ! ja = mod_type_class.to_nat y

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
have ja_less_ia: "ja < ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ja < ia
[PROOF STEP]
unfolding ja_def ia_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [0..<IArray.length (vec_to_iarray A)] - mod_type_class.to_nat y - 1 < length [0..<IArray.length (vec_to_iarray A)] - Suc a
[PROOF STEP]
by (auto simp del: IArray.length_def, metis Suc_leI suc_i_le diff_less_mono2 le_imp_less_Suc less_le_trans y_greater_a')
[PROOF STATE]
proof (state)
this:
ja < ia

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
hence eq_0: "vec_to_iarray A !! (?xs ! ja) = 0"
[PROOF STATE]
proof (prove)
using this:
ja < ia

goal (1 subgoal):
 1. vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ja) = (0::'b)
[PROOF STEP]
using all_zero
[PROOF STATE]
proof (prove)
using this:
ja < ia
\<forall>j<ia. \<not> vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! j) \<noteq> (0::'b)

goal (1 subgoal):
 1. vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ja) = (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ja) = (0::'b)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
hence "A $ y = 0"
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ja) = (0::'b)

goal (1 subgoal):
 1. A $ y = (0::'b)
[PROOF STEP]
using vec_to_iarray_nth'[of A y]
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray A !! (rev [0..<IArray.length (vec_to_iarray A)] ! ja) = (0::'b)
vec_to_iarray A !! mod_type_class.to_nat y = A $ y

goal (1 subgoal):
 1. A $ y = (0::'b)
[PROOF STEP]
unfolding xs_ja_eq_y
[PROOF STATE]
proof (prove)
using this:
vec_to_iarray A !! mod_type_class.to_nat y = (0::'b)
vec_to_iarray A !! mod_type_class.to_nat y = A $ y

goal (1 subgoal):
 1. A $ y = (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ y = (0::'b)

goal (1 subgoal):
 1. \<not> y \<le> mod_type_class.from_nat a \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
A $ y = (0::'b)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Ay
[PROOF STATE]
proof (prove)
using this:
A $ y = (0::'b)
A $ y \<noteq> (0::'b)

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<le> mod_type_class.from_nat a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(GREATEST b. A $ b \<noteq> (0::'b)) = mod_type_class.from_nat a

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(GREATEST b. A $ b \<noteq> (0::'b)) = mod_type_class.from_nat a

goal (1 subgoal):
 1. greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
unfolding greatest_not_zero_def a
[PROOF STATE]
proof (prove)
using this:
(GREATEST b. A $ b \<noteq> (0::'b)) = mod_type_class.from_nat a

goal (1 subgoal):
 1. the (Some a) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
unfolding to_nat_eq[symmetric]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b)) = mod_type_class.to_nat (mod_type_class.from_nat a)

goal (1 subgoal):
 1. the (Some a) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF a_less_card]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b)) = a

goal (1 subgoal):
 1. the (Some a) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
greatest_not_zero (vec_to_iarray A) = mod_type_class.to_nat (GREATEST b. A $ b \<noteq> (0::'b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_consistent[code]: "consistent A b = consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent A b = consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding consistent_eq_rank_ge_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let GJ_P = Gauss_Jordan_PA A; P_mult_b = fst GJ_P *v b in Let (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1) ((\<le>) (if \<exists>a. P_mult_b $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. P_mult_b $ a \<noteq> (0::'a)) + 1 else 0))) = consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding consistent_iarrays_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1)) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))))
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1)) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))))
[PROOF STEP]
unfolding rank_Gauss_Jordan_code[symmetric, unfolded Let_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))))))
[PROOF STEP]
unfolding snd_Gauss_Jordan_iarrays_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A)))))
[PROOF STEP]
unfolding rank_iarrays_code[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_to_iarray_rank
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A)) = ((if \<not> is_zero_iarray (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) then greatest_not_zero (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) *iv vec_to_iarray b) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_to_iarray_fst_Gauss_Jordan_PA[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A)) = ((if \<not> is_zero_iarray (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b) then greatest_not_zero (matrix_to_iarray (fst (Gauss_Jordan_PA A)) *iv vec_to_iarray b) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_matrix_matrix_mult[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A)) = ((if \<not> is_zero_iarray (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) then greatest_not_zero (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding not_is_zero_iarray_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<not> is_zero_iarray (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A)) = ((if \<not> is_zero_iarray (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) then greatest_not_zero (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
using vec_to_iarray_greatest_not_zero[unfolded not_is_zero_iarray_eq_iff]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_iarray (vec_to_iarray ?A) \<Longrightarrow> greatest_not_zero (vec_to_iarray ?A) = mod_type_class.to_nat (GREATEST b. ?A $ b \<noteq> (0::?'b))

goal (1 subgoal):
 1. ((if \<not> is_zero_iarray (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A)) = ((if \<not> is_zero_iarray (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) then greatest_not_zero (vec_to_iarray (fst (Gauss_Jordan_PA A) *v b)) + 1 else 0) \<le> rank_iarray (matrix_to_iarray A))
[PROOF STEP]
by force


[STATEMENT]
lemma matrix_to_iarray_inconsistent[code]: "inconsistent A b = inconsistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsistent A b = inconsistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)
[PROOF STEP]
unfolding inconsistent_def inconsistent_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> consistent A b) = (\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b))
[PROOF STEP]
unfolding matrix_to_iarray_consistent
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b)) = (\<not> consistent_iarrays (matrix_to_iarray A) (vec_to_iarray b))
[PROOF STEP]
..


[STATEMENT]
lemma exists_solve_consistent_rref:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
shows "(\<exists>i. A $ i $ j = 1 \<and> j = (LEAST n. A $ i $ n \<noteq> 0))
  = (IArray.exists (\<lambda>i. (matrix_to_iarray A) !! i !! (to_nat j) = 1
  \<and> (to_nat j)=least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray[0..<nrows_iarray (matrix_to_iarray A)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))) = IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])
[PROOF STEP]
proof (rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])
 2. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
assume "\<exists>i. A $ i $ j = 1 \<and> j = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])
 2. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
obtain i where Aij: "A $ i $ j = 1" and j_eq: "j = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ j = (1::'a); j = (LEAST n. A $ i $ n \<noteq> (0::'a))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ j = (1::'a)
j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a)) \<Longrightarrow> IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])
 2. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
show "IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! to_nat j = 1 \<and> to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A)))
     (IArray [0..<nrows_iarray (matrix_to_iarray A)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding IArray.exists_def find_Some_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>set (IArray.list_of (IArray [0..<nrows_iarray (matrix_to_iarray A)])). matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))
[PROOF STEP]
apply (rule bexI[of _ "to_nat i"])+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
 2. mod_type_class.to_nat i \<in> set (IArray.list_of (IArray [0..<nrows_iarray (matrix_to_iarray A)]))
[PROOF STEP]
proof (auto, unfold IArray.sub_def[symmetric])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
 3. mod_type_class.to_nat i < nrows_iarray (matrix_to_iarray A)
[PROOF STEP]
show "to_nat i < nrows_iarray (matrix_to_iarray A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i < nrows_iarray (matrix_to_iarray A)
[PROOF STEP]
unfolding matrix_to_iarray_nrows[symmetric] nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i < CARD('rows)
[PROOF STEP]
using to_nat_less_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?j < CARD(?'a)

goal (1 subgoal):
 1. mod_type_class.to_nat i < CARD('rows)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < nrows_iarray (matrix_to_iarray A)

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
have "to_nat j = to_nat (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat j = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding j_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a)) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ i $ n \<noteq> 0 \<and> 0\<le>n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a)) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)
[PROOF STEP]
by (metis least_mod_type)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a)) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a)) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
have "...= least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (to_nat (0::'cols))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (mod_type_class.to_nat (0::'cols))
[PROOF STEP]
proof (rule vec_to_iarray_least_non_zero_position_of_vector_from_index''[symmetric, of "0::'cols" i A])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row i A))
[PROOF STEP]
show "\<not> vector_all_zero_from_index (to_nat (0::'cols), vec_to_iarray (row i A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row i A))
[PROOF STEP]
unfolding vector_all_zero_from_index_eq[symmetric, of "0::'cols" "row i A"]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. row i A $ m = (0::'a))
[PROOF STEP]
unfolding row_def vec_nth_inverse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. A $ i $ m = (0::'a))
[PROOF STEP]
using Aij least_mod_type[of j]
[PROOF STATE]
proof (prove)
using this:
A $ i $ j = (1::'a)
(0::'cols) \<le> j

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. A $ i $ m = (0::'a))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row i A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (mod_type_class.to_nat (0::'cols))

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (mod_type_class.to_nat (0::'cols))

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
have "... = least_non_zero_position_of_vector (row_iarray (to_nat i) (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (mod_type_class.to_nat (0::'cols)) = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_row least_non_zero_position_of_vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A)) (mod_type_class.to_nat (0::'cols)) = least_non_zero_position_of_vector_from_index (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A)) 0
[PROOF STEP]
unfolding to_nat_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A)) 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (row i A)) (mod_type_class.to_nat (0::'cols)) = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))

goal (2 subgoals):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
 2. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
show "to_nat j = least_non_zero_position_of_vector (row_iarray (to_nat i) (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))

goal (1 subgoal):
 1. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray (mod_type_class.to_nat i) (matrix_to_iarray A))

goal (1 subgoal):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
[PROOF STEP]
show "matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)
[PROOF STEP]
unfolding matrix_to_iarray_nth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ j = (1::'a)
[PROOF STEP]
using Aij
[PROOF STATE]
proof (prove)
using this:
A $ i $ j = (1::'a)

goal (1 subgoal):
 1. A $ i $ j = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])

goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
assume ex_eq: "IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! to_nat j = 1 \<and> to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A)))
     (IArray [0..<nrows_iarray (matrix_to_iarray A)])"
[PROOF STATE]
proof (state)
this:
IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])

goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
have "\<exists>y. List.find (\<lambda>i. matrix_to_iarray A !! i !! to_nat j = 1 \<and> to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A)))
         [0..<nrows_iarray (matrix_to_iarray A)] = Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y
[PROOF STEP]
proof (rule ccontr, simp del: IArray.length_def IArray.sub_def, unfold find_None_iff)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A)) \<Longrightarrow> False
[PROOF STEP]
assume" \<not> (\<exists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and>
            matrix_to_iarray A !! x !! mod_type_class.to_nat j = 1 \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A)))"
[PROOF STATE]
proof (state)
this:
\<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A))

goal (1 subgoal):
 1. \<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A)) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A))

goal (1 subgoal):
 1. False
[PROOF STEP]
using ex_eq
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A))
IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)])

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding IArray.exists_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>x. x \<in> set [0..<nrows_iarray (matrix_to_iarray A)] \<and> matrix_to_iarray A !! x !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray x (matrix_to_iarray A))
\<exists>i\<in>set (IArray.list_of (IArray [0..<nrows_iarray (matrix_to_iarray A)])). matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y. find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y

goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y
[PROOF STEP]
obtain y where y: "List.find (\<lambda>i. matrix_to_iarray A !! i !! to_nat j = 1 \<and> to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A)))
         [0..<nrows_iarray (matrix_to_iarray A)] = Some y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y

goal (1 subgoal):
 1. (\<And>y. find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y

goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y
[PROOF STEP]
obtain i where i_less_length: "i<length [0..<nrows_iarray (matrix_to_iarray A)]" and
     Aij_1: "matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! to_nat j = 1"
and j_eq: "to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))" and
  y_eq: "y = [0..<nrows_iarray (matrix_to_iarray A)] ! i"
    and least: "(\<forall>ja<i. \<not> (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) !! to_nat j = 1 \<and>
                to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) (matrix_to_iarray A))))"
[PROOF STATE]
proof (prove)
using this:
find (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) [0..<nrows_iarray (matrix_to_iarray A)] = Some y

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length [0..<nrows_iarray (matrix_to_iarray A)]; matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! mod_type_class.to_nat j = (1::'a); mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A)); y = [0..<nrows_iarray (matrix_to_iarray A)] ! i; \<forall>ja<i. \<not> (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) (matrix_to_iarray A)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding find_Some_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>i<length [0..<nrows_iarray (matrix_to_iarray A)]. (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))) \<and> y = [0..<nrows_iarray (matrix_to_iarray A)] ! i \<and> (\<forall>ja<i. \<not> (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) (matrix_to_iarray A))))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length [0..<nrows_iarray (matrix_to_iarray A)]; matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! mod_type_class.to_nat j = (1::'a); mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A)); y = [0..<nrows_iarray (matrix_to_iarray A)] ! i; \<forall>ja<i. \<not> (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) (matrix_to_iarray A)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < length [0..<nrows_iarray (matrix_to_iarray A)]
matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! mod_type_class.to_nat j = (1::'a)
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))
y = [0..<nrows_iarray (matrix_to_iarray A)] ! i
\<forall>ja<i. \<not> (matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! ja) (matrix_to_iarray A)))

goal (1 subgoal):
 1. IArray.exists (\<lambda>i. matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a) \<and> mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray i (matrix_to_iarray A))) (IArray [0..<nrows_iarray (matrix_to_iarray A)]) \<Longrightarrow> \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
show "\<exists>i. A $ i $ j = 1 \<and> j = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule exI[of _ "from_nat i"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
 2. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have i_rw: "[0..<nrows_iarray (matrix_to_iarray A)] ! i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<nrows_iarray (matrix_to_iarray A)] ! i = i
[PROOF STEP]
using nth_upt[of 0 i "nrows_iarray (matrix_to_iarray A)"]
[PROOF STATE]
proof (prove)
using this:
0 + i < nrows_iarray (matrix_to_iarray A) \<Longrightarrow> [0..<nrows_iarray (matrix_to_iarray A)] ! i = 0 + i

goal (1 subgoal):
 1. [0..<nrows_iarray (matrix_to_iarray A)] ! i = i
[PROOF STEP]
using i_less_length
[PROOF STATE]
proof (prove)
using this:
0 + i < nrows_iarray (matrix_to_iarray A) \<Longrightarrow> [0..<nrows_iarray (matrix_to_iarray A)] ! i = 0 + i
i < length [0..<nrows_iarray (matrix_to_iarray A)]

goal (1 subgoal):
 1. [0..<nrows_iarray (matrix_to_iarray A)] ! i = i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[0..<nrows_iarray (matrix_to_iarray A)] ! i = i

goal (2 subgoals):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
 2. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have i_less_card: "i < CARD ('rows)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
using i_less_length
[PROOF STATE]
proof (prove)
using this:
i < length [0..<nrows_iarray (matrix_to_iarray A)]

goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
unfolding nrows_iarray_def matrix_to_iarray_def
[PROOF STATE]
proof (prove)
using this:
i < length [0..<IArray.length (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('rows)]))]

goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < CARD('rows)

goal (2 subgoals):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
 2. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
show A_ij: "A $ from_nat i $ j = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
[PROOF STEP]
using Aij_1
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray A !! ([0..<nrows_iarray (matrix_to_iarray A)] ! i) !! mod_type_class.to_nat j = (1::'a)

goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
[PROOF STEP]
unfolding i_rw
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a)

goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
[PROOF STEP]
using matrix_to_iarray_nth[of A "from_nat i" j]
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a)
matrix_to_iarray A !! mod_type_class.to_nat (mod_type_class.from_nat i) !! mod_type_class.to_nat j = A $ mod_type_class.from_nat i $ j

goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
[PROOF STEP]
unfolding to_nat_from_nat_id[OF i_less_card]
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray A !! i !! mod_type_class.to_nat j = (1::'a)
matrix_to_iarray A !! i !! mod_type_class.to_nat j = A $ mod_type_class.from_nat i $ j

goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ j = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat i $ j = (1::'a)

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have "to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))
[PROOF STEP]
using j_eq
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))

goal (1 subgoal):
 1. mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have "... = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A)) = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0
[PROOF STEP]
unfolding least_non_zero_position_of_vector_def i_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A)) = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (row_iarray ([0..<nrows_iarray (matrix_to_iarray A)] ! i) (matrix_to_iarray A)) = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have "... = least_non_zero_position_of_vector_from_index (vec_to_iarray (row (from_nat i) A)) (to_nat (0::'cols))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols))
[PROOF STEP]
unfolding vec_to_iarray_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (row_iarray (mod_type_class.to_nat (mod_type_class.from_nat i)) (matrix_to_iarray A)) (mod_type_class.to_nat (0::'cols))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF i_less_card]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) (mod_type_class.to_nat (0::'cols))
[PROOF STEP]
unfolding to_nat_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (row_iarray i (matrix_to_iarray A)) 0 = least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ (from_nat i) $ n \<noteq> 0 \<and> 0 \<le> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols)) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)
[PROOF STEP]
proof (rule vec_to_iarray_least_non_zero_position_of_vector_from_index'')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row (mod_type_class.from_nat i) A))
[PROOF STEP]
show "\<not> vector_all_zero_from_index (to_nat (0::'cols), vec_to_iarray (row (from_nat i) A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row (mod_type_class.from_nat i) A))
[PROOF STEP]
unfolding vector_all_zero_from_index_eq[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. row (mod_type_class.from_nat i) A $ m = (0::'a))
[PROOF STEP]
using A_ij
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat i $ j = (1::'a)

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. row (mod_type_class.from_nat i) A $ m = (0::'a))
[PROOF STEP]
by (metis iarray_to_vec_vec_to_iarray least_mod_type vec_matrix vec_to_iarray_row' zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (row (mod_type_class.from_nat i) A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols)) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (row (mod_type_class.from_nat i) A)) (mod_type_class.to_nat (0::'cols)) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ (from_nat i) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
using least_mod_type
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mod_type_class.to_nat j = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
show "j = (LEAST n. A $ from_nat i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j = mod_type_class.to_nat (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding to_nat_eq
[PROOF STATE]
proof (prove)
using this:
j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
j = (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_nat_the_solve_consistent_rref:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and exists: "(\<exists>i. A $ i $ j = 1 \<and> j = (LEAST n. A $ i $ n \<noteq> 0))"
shows "to_nat (THE i. A $ i $ j = 1) = least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
obtain i where Aij: "A $ i $ j = 1" and j:"j = (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ j = (1::'a); j = (LEAST n. A $ i $ n \<noteq> (0::'a))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using exists
[PROOF STATE]
proof (prove)
using this:
\<exists>i. A $ i $ j = (1::'a) \<and> j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ j = (1::'a); j = (LEAST n. A $ i $ n \<noteq> (0::'a))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ j = (1::'a)
j = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)) =
    least_non_zero_position_of_vector (vec_to_iarray (column j A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = least_non_zero_position_of_vector (vec_to_iarray (column j A))
[PROOF STEP]
unfolding vec_to_iarray_column
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = least_non_zero_position_of_vector (vec_to_iarray (column j A))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = least_non_zero_position_of_vector (vec_to_iarray (column j A))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "... = least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (to_nat (0::'rows))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (vec_to_iarray (column j A)) = least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows))
[PROOF STEP]
unfolding least_non_zero_position_of_vector_def to_nat_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) 0 = least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (vec_to_iarray (column j A)) = least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (vec_to_iarray (column j A)) = least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ n $ j \<noteq> 0 \<and> 0 \<le> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n)
[PROOF STEP]
proof (rule vec_to_iarray_least_non_zero_position_of_vector_from_index')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'rows), vec_to_iarray (column j A))
[PROOF STEP]
show "\<not> vector_all_zero_from_index (to_nat (0::'rows), vec_to_iarray (column j A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'rows), vec_to_iarray (column j A))
[PROOF STEP]
unfolding vector_all_zero_from_index_eq[symmetric] column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'rows. (\<chi>i. A $ i $ j) $ m = (0::'a))
[PROOF STEP]
using Aij least_mod_type[of i]
[PROOF STATE]
proof (prove)
using this:
A $ i $ j = (1::'a)
(0::'rows) \<le> i

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'rows. (\<chi>i. A $ i $ j) $ m = (0::'a))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'rows), vec_to_iarray (column j A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n)

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (column j A)) (mod_type_class.to_nat (0::'rows)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n)

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ n $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
using least_mod_type
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> (0::'rows) \<le> n) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
have least_eq: "least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)) = to_nat (LEAST n. A $ n $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have i_eq_least: "i=(LEAST n. A $ n $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality[symmetric])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ i $ j \<noteq> (0::'a)
 2. \<And>y. A $ y $ j \<noteq> (0::'a) \<Longrightarrow> i \<le> y
[PROOF STEP]
show "A $ i $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ j \<noteq> (0::'a)
[PROOF STEP]
by (metis Aij zero_neq_one)
[PROOF STATE]
proof (state)
this:
A $ i $ j \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. A $ y $ j \<noteq> (0::'a) \<Longrightarrow> i \<le> y
[PROOF STEP]
show "\<And>y. A $ y $ j \<noteq> 0 \<Longrightarrow> i \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. A $ y $ j \<noteq> (0::'a) \<Longrightarrow> i \<le> y
[PROOF STEP]
by (metis (mono_tags) Aij is_zero_row_def' j order_refl rref rref_condition4 zero_neq_one)
[PROOF STATE]
proof (state)
this:
A $ ?y $ j \<noteq> (0::'a) \<Longrightarrow> i \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have the_eq_least_pos: "(THE i. A $ i $ j = 1) = from_nat (least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE i. A $ i $ j = (1::'a)) = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
proof (rule the_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))) $ j = (1::'a)
 2. \<And>i. A $ i $ j = (1::'a) \<Longrightarrow> i = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
show " A $ from_nat (least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A))) $ j = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))) $ j = (1::'a)
[PROOF STEP]
unfolding least_eq from_nat_to_nat_id i_eq_least[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ j = (1::'a)
[PROOF STEP]
using Aij
[PROOF STATE]
proof (prove)
using this:
A $ i $ j = (1::'a)

goal (1 subgoal):
 1. A $ i $ j = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))) $ j = (1::'a)

goal (1 subgoal):
 1. \<And>i. A $ i $ j = (1::'a) \<Longrightarrow> i = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A $ i $ j = (1::'a) \<Longrightarrow> i = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
assume a: "A $ a $ j = 1"
[PROOF STATE]
proof (state)
this:
A $ a $ j = (1::'a)

goal (1 subgoal):
 1. \<And>i. A $ i $ j = (1::'a) \<Longrightarrow> i = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
show "a = from_nat (least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))
[PROOF STEP]
unfolding least_eq from_nat_to_nat_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
by (metis Aij a i_eq_least is_zero_row_def' j rref rref_condition4_explicit zero_neq_one)
[PROOF STATE]
proof (state)
this:
a = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(THE i. A $ i $ j = (1::'a)) = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "to_nat (THE i. A $ i $ j = 1) = to_nat (from_nat (least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)))::'rows)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))))
[PROOF STEP]
using the_eq_least_pos
[PROOF STATE]
proof (prove)
using this:
(THE i. A $ i $ j = (1::'a)) = mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "... = (least_non_zero_position_of_vector (column_iarray (to_nat j) (matrix_to_iarray A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
by (rule to_nat_from_nat_id, unfold least_eq, simp add: to_nat_less_card)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat (least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)))) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
have "... = to_nat (LEAST n. A $ n $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
unfolding least_eq from_nat_to_nat_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
have "(THE i. A $ i $ j = 1) = (LEAST n. A $ n $ j \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. (THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
unfolding to_nat_eq
[PROOF STATE]
proof (prove)
using this:
(THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. (THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))
[PROOF STEP]
unfolding least_eq from_nat_to_nat_id
[PROOF STATE]
proof (prove)
using this:
(THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = mod_type_class.to_nat (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
unfolding to_nat_eq
[PROOF STATE]
proof (prove)
using this:
(THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))

goal (1 subgoal):
 1. (THE i. A $ i $ j = (1::'a)) = (LEAST n. A $ n $ j \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (THE i. A $ i $ j = (1::'a)) = least_non_zero_position_of_vector (column_iarray (mod_type_class.to_nat j) (matrix_to_iarray A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iarray_exhaust2:
"(xs = ys) = (IArray.list_of xs = IArray.list_of ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs = ys) = (IArray.list_of xs = IArray.list_of ys)
[PROOF STEP]
by (metis iarray.exhaust list_of.simps)