[STATEMENT]
lemma matrix_to_iarray_bezout_iterate:
  assumes n: "n<nrows A"
  shows "matrix_to_iarray (bezout_iterate A n i j bezout)
  = bezout_iterate_iarrays (matrix_to_iarray A) n (to_nat i) (to_nat j) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A 0 i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A

goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A 0 i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A 0 i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding bezout_iterate_iarrays.simps bezout_iterate.simps
[PROOF STATE]
proof (prove)
using this:
0 < nrows A

goal (1 subgoal):
 1. matrix_to_iarray A = matrix_to_iarray A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A 0 i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n < nrows ?A \<Longrightarrow> matrix_to_iarray (bezout_iterate ?A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray ?A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
Suc n < nrows A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (bezout_iterate A n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
proof (cases "Suc n \<le> to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
 2. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n \<le> mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
 2. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding bezout_iterate.simps bezout_iterate_iarrays.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = (if Suc n \<le> mod_type_class.to_nat i then matrix_to_iarray A else bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
Suc n \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. matrix_to_iarray (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = (if Suc n \<le> mod_type_class.to_nat i then matrix_to_iarray A else bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc n \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
let ?B="(bezout_matrix_iarrays (matrix_to_iarray A) (to_nat i) (Suc n) (to_nat j) bezout
      **i matrix_to_iarray A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
let ?B2="matrix_to_iarray (bezout_matrix A i (from_nat (Suc n)) j bezout ** A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have "matrix_to_iarray (bezout_iterate A (Suc n) i j bezout)
      = matrix_to_iarray (bezout_iterate (bezout_matrix A i (from_nat (Suc n)) j bezout ** A) n i j bezout)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout)
[PROOF STEP]
unfolding bezout_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> Suc n \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. matrix_to_iarray (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout)

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout)

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have "... = bezout_iterate_iarrays ?B2 n (to_nat i) (to_nat j) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
proof (rule Suc.hyps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)
[PROOF STEP]
show "n < nrows (bezout_matrix A i (from_nat (Suc n)) j bezout ** A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A

goal (1 subgoal):
 1. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n < CARD('c)

goal (1 subgoal):
 1. n < CARD('c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A) n i j bezout) = bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have "... = bezout_iterate_iarrays ?B n (to_nat i) (to_nat j) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding matrix_to_iarray_matrix_matrix_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout) **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding matrix_to_iarray_bezout_matrix[of A i "from_nat (Suc n)" j bezout]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (mod_type_class.to_nat (mod_type_class.from_nat (Suc n))) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding to_nat_from_nat_id[OF Suc.prems[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bezout_iterate_iarrays (matrix_to_iarray (bezout_matrix A i (mod_type_class.from_nat (Suc n)) j bezout ** A)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have "... = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (to_nat i) (to_nat j) bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding bezout_iterate_iarrays.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = (if Suc n \<le> mod_type_class.to_nat i then matrix_to_iarray A else bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> Suc n \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = (if Suc n \<le> mod_type_class.to_nat i then matrix_to_iarray A else bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bezout_iterate_iarrays (bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat i) (Suc n) (mod_type_class.to_nat j) bezout **i matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. \<not> Suc n \<le> mod_type_class.to_nat i \<Longrightarrow> matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal (1 subgoal):
 1. matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_iterate A (Suc n) i j bezout) = bezout_iterate_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) bezout

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_vector_all_zero_from_index2:
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows::{mod_type}"
  shows "(\<forall>m>i. A $ m $ k = 0) = vector_all_zero_from_index ((to_nat i)+1, vec_to_iarray (column k A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
proof (cases "to_nat i = nrows A - 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat i = nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
 2. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i = nrows A - 1

goal (2 subgoals):
 1. mod_type_class.to_nat i = nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
 2. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
have "(\<forall>m>i. A $ m $ k = 0) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = True
[PROOF STEP]
by (metis One_nat_def Suc_pred True not_less_eq nrows_def to_nat_0 to_nat_less_card to_nat_mono)
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = True

goal (2 subgoals):
 1. mod_type_class.to_nat i = nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
 2. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = True

goal (2 subgoals):
 1. mod_type_class.to_nat i = nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
 2. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
have "... = vector_all_zero_from_index ((to_nat i)+1, vec_to_iarray (column k A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
unfolding vector_all_zero_from_index_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True = IArray.all (\<lambda>x. snd (mod_type_class.to_nat i + 1, vec_to_iarray (column k A)) !! x = (0::'a)) (IArray [fst (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))..<IArray.length (snd (mod_type_class.to_nat i + 1, vec_to_iarray (column k A)))])
[PROOF STEP]
unfolding vec_to_iarray_def column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True = IArray.all (\<lambda>x. snd (mod_type_class.to_nat i + 1, IArray.of_fun (\<lambda>i. (\<chi>i. A $ i $ k) $ mod_type_class.from_nat i) CARD('rows)) !! x = (0::'a)) (IArray [fst (mod_type_class.to_nat i + 1, IArray.of_fun (\<lambda>i. (\<chi>i. A $ i $ k) $ mod_type_class.from_nat i) CARD('rows))..<IArray.length (snd (mod_type_class.to_nat i + 1, IArray.of_fun (\<lambda>i. (\<chi>i. A $ i $ k) $ mod_type_class.from_nat i) CARD('rows)))])
[PROOF STEP]
by (auto, metis True nrows_def One_nat_def Suc_pred not_le zero_less_card_finite)
[PROOF STATE]
proof (state)
this:
True = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal (2 subgoals):
 1. mod_type_class.to_nat i = nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
 2. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<noteq> nrows A - 1

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
have i_le: "i<i+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < i + (1::'rows)
[PROOF STEP]
by (metis False Suc_le' add_diff_cancel_right' nrows_def suc_not_zero)
[PROOF STATE]
proof (state)
this:
i < i + (1::'rows)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
hence "(\<forall>m>i. A $ m $ k = 0) = (\<forall>m\<ge>i+1. A $ m $ k = 0)"
[PROOF STATE]
proof (prove)
using this:
i < i + (1::'rows)

goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = (\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a))
[PROOF STEP]
using i_le le_Suc
[PROOF STATE]
proof (prove)
using this:
i < i + (1::'rows)
i < i + (1::'rows)
?a < ?b \<Longrightarrow> ?a + (1::?'a) \<le> ?b

goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = (\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = (\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = (\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
have "... = vector_all_zero_from_index ((to_nat i)+1, vec_to_iarray (column k A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
unfolding matrix_vector_all_zero_from_index
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (mod_type_class.to_nat (i + (1::'rows)), vec_to_iarray (column k A)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) from_nat_suc from_nat_to_nat_id i_le not_less0
      to_nat_0 to_nat_from_nat_id to_nat_mono to_nat_plus_one_less_card)
[PROOF STATE]
proof (state)
this:
(\<forall>m\<ge>i + (1::'rows). A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal (1 subgoal):
 1. mod_type_class.to_nat i \<noteq> nrows A - 1 \<Longrightarrow> (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal (1 subgoal):
 1. (\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<forall>m>i. A $ m $ k = (0::'a)) = vector_all_zero_from_index (mod_type_class.to_nat i + 1, vec_to_iarray (column k A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_echelon_form_of_column_k:
  fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes k: "k<ncols A"
  and i: "i\<le>nrows A"
  shows "matrix_to_iarray (fst ((echelon_form_of_column_k bezout) (A,i) k))
  = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
proof (cases "i<nrows A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
 2. \<not> i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < nrows A

goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
 2. \<not> i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
have i_eq: "i=nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = nrows A
[PROOF STEP]
by (metis False le_imp_less_or_eq i)
[PROOF STATE]
proof (state)
this:
i = nrows A

goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
 2. \<not> i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
show "matrix_to_iarray (fst ((echelon_form_of_column_k bezout) (A,i) k))
    = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
unfolding echelon_form_of_column_k_efficient echelon_form_of_column_k_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (case (A, i) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
unfolding echelon_form_of_column_k_iarrays_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (case (A, i) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
unfolding matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (case (A, i) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows_iarray (matrix_to_iarray A) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
unfolding i_eq matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (case (A, nrows_iarray (matrix_to_iarray A)) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows_iarray (matrix_to_iarray A) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, nrows_iarray (matrix_to_iarray A), bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < nrows A

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
let ?interchange="(interchange_rows A (from_nat i)
    (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> from_nat i \<le> n))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
have all_zero: "(\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = 0)
    = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_vector_all_zero_from_index
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (mod_type_class.to_nat (mod_type_class.from_nat i), vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_column'[OF k]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
have all_zero2: " (\<forall>m>from_nat i. A $ m $ mod_type_class.from_nat k = 0)
    = (vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_vector_all_zero_from_index2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (mod_type_class.to_nat (mod_type_class.from_nat i) + 1, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i + 1, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_column'[OF k]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
have n: "(nrows_iarray (matrix_to_iarray A) - Suc 0) < nrows ?interchange"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows_iarray (matrix_to_iarray A) - Suc 0 < nrows (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))
[PROOF STEP]
unfolding matrix_to_iarray_nrows[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows A - Suc 0 < nrows (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('rows) - Suc 0 < CARD('rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nrows_iarray (matrix_to_iarray A) - Suc 0 < nrows (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
unfolding echelon_form_of_column_k_efficient echelon_form_of_column_k_def Let_def split_beta
[PROOF STATE]
proof (prove)
using this:
i < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (fst (if (\<forall>m\<ge>mod_type_class.from_nat (snd (A, i)). fst (A, i) $ m $ mod_type_class.from_nat k = (0::'a)) \<or> snd (A, i) = nrows (fst (A, i)) then (fst (A, i), snd (A, i)) else if \<forall>m>mod_type_class.from_nat (snd (A, i)). fst (A, i) $ m $ mod_type_class.from_nat k = (0::'a) then (fst (A, i), snd (A, i) + 1) else (bezout_iterate (interchange_rows (fst (A, i)) (mod_type_class.from_nat (snd (A, i))) (LEAST n. fst (A, i) $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat (snd (A, i)) \<le> n)) (nrows (fst (A, i)) - 1) (mod_type_class.from_nat (snd (A, i))) (mod_type_class.from_nat k) bezout, snd (A, i) + 1))) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)
[PROOF STEP]
unfolding echelon_form_of_column_k_iarrays_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
using this:
i < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
unfolding matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
using this:
i < nrows_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. matrix_to_iarray (fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows_iarray (matrix_to_iarray A) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
unfolding all_zero all_zero2
[PROOF STATE]
proof (prove)
using this:
i < nrows_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. matrix_to_iarray (fst (if vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)) \<or> i = nrows_iarray (matrix_to_iarray A) then (A, i) else if vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1))) = fst (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - Suc 0) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout) = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
unfolding matrix_to_iarray_bezout_iterate[OF n]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (matrix_to_iarray (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) (mod_type_class.to_nat (mod_type_class.from_nat i)) (mod_type_class.to_nat (mod_type_class.from_nat k)) bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
unfolding matrix_to_iarray_interchange_rows
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) (mod_type_class.to_nat (mod_type_class.from_nat i)) (mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) (mod_type_class.to_nat (mod_type_class.from_nat i)) (mod_type_class.to_nat (mod_type_class.from_nat k)) bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
using vec_to_iarray_least_non_zero_position_of_vector_from_index'[of "from_nat i" "from_nat k" A]
[PROOF STATE]
proof (prove)
using this:
\<not> vector_all_zero_from_index (mod_type_class.to_nat (mod_type_class.from_nat i), vec_to_iarray (column (mod_type_class.from_nat k) A)) \<Longrightarrow> least_non_zero_position_of_vector_from_index (vec_to_iarray (column (mod_type_class.from_nat k) A)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) (mod_type_class.to_nat (mod_type_class.from_nat i)) (mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) (mod_type_class.to_nat (mod_type_class.from_nat i)) (mod_type_class.to_nat (mod_type_class.from_nat k)) bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
using this:
\<not> vector_all_zero_from_index (i, vec_to_iarray (column (mod_type_class.from_nat k) A)) \<Longrightarrow> least_non_zero_position_of_vector_from_index (vec_to_iarray (column (mod_type_class.from_nat k) A)) i = mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) i (mod_type_class.to_nat (mod_type_class.from_nat k)) bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
unfolding to_nat_from_nat_id[OF k[unfolded ncols_def]]
[PROOF STATE]
proof (prove)
using this:
\<not> vector_all_zero_from_index (i, vec_to_iarray (column (mod_type_class.from_nat k) A)) \<Longrightarrow> least_non_zero_position_of_vector_from_index (vec_to_iarray (column (mod_type_class.from_nat k) A)) i = mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
unfolding vec_to_iarray_column'[OF k]
[PROOF STATE]
proof (prove)
using this:
\<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)) \<Longrightarrow> least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i = mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)

goal (2 subgoals):
 1. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> matrix_to_iarray A = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
 2. \<lbrakk>i < nrows_iarray (matrix_to_iarray A); \<not> vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)); \<not> vector_all_zero_from_index (Suc i, column_iarray k (matrix_to_iarray A))\<rbrakk> \<Longrightarrow> bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (mod_type_class.to_nat (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n))) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout = bezout_iterate_iarrays (interchange_rows_iarray (matrix_to_iarray A) i (least_non_zero_position_of_vector_from_index (column_iarray k (matrix_to_iarray A)) i)) (nrows_iarray (matrix_to_iarray A) - Suc 0) i k bezout
[PROOF STEP]
by (auto, metis Suc_eq_plus1 all_zero all_zero2 less_le)
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (fst (echelon_form_of_column_k bezout (A, i) k)) = fst (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_matrix_to_iarray_echelon_form_of_column_k:
  fixes A::"'a::{bezout_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes k: "k<ncols A"
  and i: "i\<le>nrows A"
  shows "snd ((echelon_form_of_column_k bezout) (A,i) k)
  = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
proof (cases "i<nrows A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
 2. \<not> i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < nrows A

goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
 2. \<not> i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
have i_eq: "i=nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = nrows A
[PROOF STEP]
by (metis False le_imp_less_or_eq i)
[PROOF STATE]
proof (state)
this:
i = nrows A

goal (2 subgoals):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
 2. \<not> i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
show "snd ((echelon_form_of_column_k bezout) (A,i) k)
    = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
unfolding echelon_form_of_column_k_efficient echelon_form_of_column_k_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (A, i) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
unfolding echelon_form_of_column_k_iarrays_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (A, i) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout)))
[PROOF STEP]
unfolding i_eq matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (case (A, nrows_iarray (matrix_to_iarray A)) of (A, i) \<Rightarrow> if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows_iarray (matrix_to_iarray A) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (case (matrix_to_iarray A, nrows_iarray (matrix_to_iarray A), bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < nrows A

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
let ?interchange="(interchange_rows A (from_nat i)
    (LEAST n. A $ n $ from_nat k \<noteq> 0 \<and> from_nat i \<le> n))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
have all_zero: "(\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = 0)
    = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_vector_all_zero_from_index
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (mod_type_class.to_nat (mod_type_class.from_nat i), vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_column'[OF k]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i, column_iarray k (matrix_to_iarray A))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
have all_zero2: " (\<forall>m>from_nat i. A $ m $ mod_type_class.from_nat k = 0)
    = (vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding matrix_vector_all_zero_from_index2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (mod_type_class.to_nat (mod_type_class.from_nat i) + 1, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i + 1, vec_to_iarray (column (mod_type_class.from_nat k) A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_column'[OF k]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) = vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A))

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
have Aik: "A $ from_nat i $ from_nat k = matrix_to_iarray A !! i !! k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k
[PROOF STEP]
by (metis True k matrix_to_iarray_nth ncols_def nrows_def to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. i < nrows A \<Longrightarrow> snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
using True Aik
[PROOF STATE]
proof (prove)
using this:
i < nrows A
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
unfolding echelon_form_of_column_k_efficient
[PROOF STATE]
proof (prove)
using this:
i < nrows A
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (echelon_form_of_column_k_efficient bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
unfolding echelon_form_of_column_k_efficient_def Let_def split_beta
[PROOF STATE]
proof (prove)
using this:
i < nrows A
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (if snd (A, i) = nrows (fst (A, i)) \<or> fst (A, i) $ mod_type_class.from_nat (snd (A, i)) $ mod_type_class.from_nat k = (0::'a) \<and> (\<forall>m>mod_type_class.from_nat (snd (A, i)). fst (A, i) $ m $ mod_type_class.from_nat k = (0::'a)) then (fst (A, i), snd (A, i)) else if \<forall>m>mod_type_class.from_nat (snd (A, i)). fst (A, i) $ m $ mod_type_class.from_nat k = (0::'a) then (fst (A, i), snd (A, i) + 1) else (bezout_iterate (interchange_rows (fst (A, i)) (mod_type_class.from_nat (snd (A, i))) (LEAST n. fst (A, i) $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat (snd (A, i)) \<le> n)) (nrows (fst (A, i)) - 1) (mod_type_class.from_nat (snd (A, i))) (mod_type_class.from_nat k) bezout, snd (A, i) + 1)) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))
[PROOF STEP]
unfolding echelon_form_of_column_k_iarrays_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
using this:
i < nrows A
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (if i = nrows A \<or> A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = (0::'a) \<and> (\<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) then (A, i) else if \<forall>m>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout)))
[PROOF STEP]
unfolding all_zero all_zero2
[PROOF STATE]
proof (prove)
using this:
i < nrows A
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (if i = nrows A \<or> A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) then (A, i) else if vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows A - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout)))
[PROOF STEP]
unfolding matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
using this:
i < nrows_iarray (matrix_to_iarray A)
A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = matrix_to_iarray A !! i !! k

goal (1 subgoal):
 1. snd (if i = nrows_iarray (matrix_to_iarray A) \<or> A $ mod_type_class.from_nat i $ mod_type_class.from_nat k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) then (A, i) else if vector_all_zero_from_index (i + 1, column_iarray k (matrix_to_iarray A)) then (A, i + 1) else (bezout_iterate (interchange_rows A (mod_type_class.from_nat i) (LEAST n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> mod_type_class.from_nat i \<le> n)) (nrows_iarray (matrix_to_iarray A) - 1) (mod_type_class.from_nat i) (mod_type_class.from_nat k) bezout, i + 1)) = fst (snd (case (matrix_to_iarray A, i, bezout) of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! k = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray k A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray k A) i)) (nrows_iarray A - 1) i k bezout, i + 1, bezout)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (echelon_form_of_column_k bezout (A, i) k) = fst (snd (echelon_form_of_column_k_iarrays (matrix_to_iarray A, i, bezout) k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma snd_snd_foldl_echelon_form_of_column_k_iarrays:
  "snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k]))
  = bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<0])) = bezout
 2. \<And>k. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout \<Longrightarrow> snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<0])) = bezout
 2. \<And>k. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout \<Longrightarrow> snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<0])) = bezout
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<0])) = bezout

goal (1 subgoal):
 1. \<And>k. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout \<Longrightarrow> snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout \<Longrightarrow> snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout

goal (1 subgoal):
 1. \<And>k. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout \<Longrightarrow> snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout

goal (1 subgoal):
 1. snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
unfolding echelon_form_of_column_k_iarrays_def
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl (\<lambda>a b. let (A, i, bezout) = a; nrows_A = nrows_iarray A; column_Ak = column_iarray b A; all_zero_below_i = vector_all_zero_from_index (i + 1, column_Ak) in if i = nrows_A \<or> A !! i !! b = (0::'a) \<and> all_zero_below_i then (A, i, bezout) else if all_zero_below_i then (A, i + 1, bezout) else let n = least_non_zero_position_of_vector_from_index column_Ak i; interchange_A = interchange_rows_iarray A i n in (bezout_iterate_iarrays interchange_A (nrows_A - 1) i b bezout, i + 1, bezout)) (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout

goal (1 subgoal):
 1. snd (snd (foldl (\<lambda>a b. let (A, i, bezout) = a; nrows_A = nrows_iarray A; column_Ak = column_iarray b A; all_zero_below_i = vector_all_zero_from_index (i + 1, column_Ak) in if i = nrows_A \<or> A !! i !! b = (0::'a) \<and> all_zero_below_i then (A, i, bezout) else if all_zero_below_i then (A, i + 1, bezout) else let n = least_non_zero_position_of_vector_from_index column_Ak i; interchange_A = interchange_rows_iarray A i n in (bezout_iterate_iarrays interchange_A (nrows_A - 1) i b bezout, i + 1, bezout)) (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl (\<lambda>a aa. case a of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! aa = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray aa A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray aa A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray aa A) i)) (nrows_iarray A - 1) i aa bezout, i + 1, bezout)) (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout

goal (1 subgoal):
 1. snd (snd (foldl (\<lambda>a aa. case a of (A, i, bezout) \<Rightarrow> if i = nrows_iarray A \<or> A !! i !! aa = (0::'a) \<and> vector_all_zero_from_index (i + 1, column_iarray aa A) then (A, i, bezout) else if vector_all_zero_from_index (i + 1, column_iarray aa A) then (A, i + 1, bezout) else (bezout_iterate_iarrays (interchange_rows_iarray A i (least_non_zero_position_of_vector_from_index (column_iarray aa A) i)) (nrows_iarray A - 1) i aa bezout, i + 1, bezout)) (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
unfolding split_beta
[PROOF STATE]
proof (prove)
using this:
snd (snd (foldl (\<lambda>a b. if fst (snd a) = nrows_iarray (fst a) \<or> fst a !! fst (snd a) !! b = (0::'a) \<and> vector_all_zero_from_index (fst (snd a) + 1, column_iarray b (fst a)) then (fst a, fst (snd a), snd (snd a)) else if vector_all_zero_from_index (fst (snd a) + 1, column_iarray b (fst a)) then (fst a, fst (snd a) + 1, snd (snd a)) else (bezout_iterate_iarrays (interchange_rows_iarray (fst a) (fst (snd a)) (least_non_zero_position_of_vector_from_index (column_iarray b (fst a)) (fst (snd a)))) (nrows_iarray (fst a) - 1) (fst (snd a)) b (snd (snd a)), fst (snd a) + 1, snd (snd a))) (matrix_to_iarray A, 0, bezout) [0..<k])) = bezout

goal (1 subgoal):
 1. snd (snd (foldl (\<lambda>a b. if fst (snd a) = nrows_iarray (fst a) \<or> fst a !! fst (snd a) !! b = (0::'a) \<and> vector_all_zero_from_index (fst (snd a) + 1, column_iarray b (fst a)) then (fst a, fst (snd a), snd (snd a)) else if vector_all_zero_from_index (fst (snd a) + 1, column_iarray b (fst a)) then (fst a, fst (snd a) + 1, snd (snd a)) else (bezout_iterate_iarrays (interchange_rows_iarray (fst a) (fst (snd a)) (least_non_zero_position_of_vector_from_index (column_iarray b (fst a)) (fst (snd a)))) (nrows_iarray (fst a) - 1) (fst (snd a)) b (snd (snd a)), fst (snd a) + 1, snd (snd a))) (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (snd (foldl echelon_form_of_column_k_iarrays (matrix_to_iarray A, 0, bezout) [0..<Suc k])) = bezout

goal:
No subgoals!
[PROOF STEP]
qed