[STATEMENT]
lemma gauss_jordan_carrier: assumes A: "(A :: 'a :: field mat) \<in> carrier_mat nr nc"
  and B: "B \<in> carrier_mat nr nc'"
  and res: "gauss_jordan A B = (A',B')"
  shows "A' \<in> carrier_mat nr nc" "B' \<in> carrier_mat nr nc'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<in> carrier_mat nr nc &&& B' \<in> carrier_mat nr nc'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A' \<in> carrier_mat nr nc
 2. B' \<in> carrier_mat nr nc'
[PROOF STEP]
from gauss_jordan_transform[OF A B res, of undefined]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr undefined). A' = P * A \<and> B' = P * B
[PROOF STEP]
obtain P where P: "P \<in> Units (ring_mat TYPE('a) nr undefined)"
    and id: "A' = P * A" "B' = P * B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr undefined). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) nr undefined); A' = P * A; B' = P * B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) nr undefined)
A' = P * A
B' = P * B

goal (2 subgoals):
 1. A' \<in> carrier_mat nr nc
 2. B' \<in> carrier_mat nr nc'
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
P \<in> Units (ring_mat TYPE('a) nr undefined)
[PROOF STEP]
have P: "P \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
P \<in> Units (ring_mat TYPE('a) nr undefined)

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
unfolding Units_def ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {y \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = undefined\<rparr>\<^esub>}

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr nr

goal (2 subgoals):
 1. A' \<in> carrier_mat nr nc
 2. B' \<in> carrier_mat nr nc'
[PROOF STEP]
show "A' \<in> carrier_mat nr nc" "B' \<in> carrier_mat nr nc'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<in> carrier_mat nr nc &&& B' \<in> carrier_mat nr nc'
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * A \<in> carrier_mat nr nc &&& P * B \<in> carrier_mat nr nc'
[PROOF STEP]
using P A B
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
B \<in> carrier_mat nr nc'

goal (1 subgoal):
 1. P * A \<in> carrier_mat nr nc &&& P * B \<in> carrier_mat nr nc'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' \<in> carrier_mat nr nc
B' \<in> carrier_mat nr nc'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_funI: assumes d: "dim_row A = nr"
  and *: "\<And> i. i < nr \<Longrightarrow> f i \<le> nc"
      "\<And> i j. i < nr \<Longrightarrow> j < f i \<Longrightarrow> A $$ (i,j) = 0"
      "\<And> i. i < nr \<Longrightarrow> Suc i < nr \<Longrightarrow> f (Suc i) > f i \<or> f (Suc i) = nc"
      "\<And> i. i < nr \<Longrightarrow> f i < nc \<Longrightarrow> A $$ (i, f i) = 1"
      "\<And> i i'. i < nr \<Longrightarrow> f i < nc \<Longrightarrow> i' < nr \<Longrightarrow> i' \<noteq> i \<Longrightarrow> A $$ (i',f i) = 0"
  shows "pivot_fun A f nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun A f nc
[PROOF STEP]
unfolding pivot_fun_def Let_def d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<nr. f i \<le> nc \<and> (f i < nc \<longrightarrow> A $$ (i, f i) = (1::'a) \<and> (\<forall>i'<nr. i' \<noteq> i \<longrightarrow> A $$ (i', f i) = (0::'a))) \<and> (\<forall>j<f i. A $$ (i, j) = (0::'a)) \<and> (Suc i < nr \<longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> f ?i \<le> nc
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = nc
\<lbrakk>?i < nr; f ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. \<forall>i<nr. f i \<le> nc \<and> (f i < nc \<longrightarrow> A $$ (i, f i) = (1::'a) \<and> (\<forall>i'<nr. i' \<noteq> i \<longrightarrow> A $$ (i', f i) = (0::'a))) \<and> (\<forall>j<f i. A $$ (i, j) = (0::'a)) \<and> (Suc i < nr \<longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc)
[PROOF STEP]
by blast


[STATEMENT]
lemma pivot_funD: assumes d: "dim_row A = nr"
  and p: "pivot_fun A f nc"
  shows "\<And> i. i < nr \<Longrightarrow> f i \<le> nc"
      "\<And> i j. i < nr \<Longrightarrow> j < f i \<Longrightarrow> A $$ (i,j) = 0"
      "\<And> i. i < nr \<Longrightarrow> Suc i < nr \<Longrightarrow> f (Suc i) > f i \<or> f (Suc i) = nc"
      "\<And> i. i < nr \<Longrightarrow> f i < nc \<Longrightarrow> A $$ (i, f i) = 1"
      "\<And> i i'. i < nr \<Longrightarrow> f i < nc \<Longrightarrow> i' < nr \<Longrightarrow> i' \<noteq> i \<Longrightarrow> A $$ (i',f i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>i. i < nr \<Longrightarrow> f i \<le> nc) &&& (\<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a))) &&& (\<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc) &&& (\<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)) &&& (\<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a))
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
pivot_fun A f nc

goal (1 subgoal):
 1. ((\<And>i. i < nr \<Longrightarrow> f i \<le> nc) &&& (\<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a))) &&& (\<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc) &&& (\<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)) &&& (\<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a))
[PROOF STEP]
unfolding pivot_fun_def Let_def d
[PROOF STATE]
proof (prove)
using this:
\<forall>i<nr. f i \<le> nc \<and> (f i < nc \<longrightarrow> A $$ (i, f i) = (1::'a) \<and> (\<forall>i'<nr. i' \<noteq> i \<longrightarrow> A $$ (i', f i) = (0::'a))) \<and> (\<forall>j<f i. A $$ (i, j) = (0::'a)) \<and> (Suc i < nr \<longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc)

goal (1 subgoal):
 1. ((\<And>i. i < nr \<Longrightarrow> f i \<le> nc) &&& (\<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a))) &&& (\<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc) &&& (\<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)) &&& (\<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a))
[PROOF STEP]
by blast+


[STATEMENT]
lemma pivot_fun_multrow: assumes p: "pivot_fun A f jj"
  and d: "dim_row A = nr" "dim_col A = nc"
  and fi: "f i0 = jj"
  and jj: "jj \<le> nc"
  shows "pivot_fun (multrow i0 a A) f jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
note p = pivot_funD[OF d(1) p]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
let ?A = "multrow i0 a A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
have "dim_row ?A = nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (multrow i0 a A) = nr
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
dim_row A = nr
dim_col A = nc

goal (1 subgoal):
 1. dim_row (multrow i0 a A) = nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row (multrow i0 a A) = nr

goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_row (multrow i0 a A) = nr

goal (1 subgoal):
 1. pivot_fun (multrow i0 a A) f jj
[PROOF STEP]
proof (rule pivot_funI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
assume i: "i < nr"
[PROOF STATE]
proof (state)
this:
i < nr

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
note p = p[OF i]
[PROOF STATE]
proof (state)
this:
f i \<le> jj
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
f i < jj \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < jj; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
show "f i \<le> jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i \<le> jj
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f i \<le> jj

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 3. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
show "Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
assume *: "f i < jj" "i' < nr" "i' \<noteq> i"
[PROOF STATE]
proof (state)
this:
f i < jj
i' < nr
i' \<noteq> i

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
from p(5)[OF this]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i', f i) = (0::'a)
[PROOF STEP]
show "?A $$ (i', f i) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i', f i) = (0::'a)

goal (1 subgoal):
 1. multrow i0 a A $$ (i', f i) = (0::'a)
[PROOF STEP]
by (subst index_mat_multrow(1), insert * d jj, auto)
[PROOF STATE]
proof (state)
this:
multrow i0 a A $$ (i', f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i < jj; ?i'2 < nr; ?i'2 \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (?i'2, f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i < jj; ?i'2 < nr; ?i'2 \<noteq> i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (?i'2, f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
assume *: "f i < jj"
[PROOF STATE]
proof (state)
this:
f i < jj

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
from p(4)[OF this]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, f i) = (1::'a)
[PROOF STEP]
have A: "A $$ (i, f i) = 1"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. A $$ (i, f i) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, f i) = (1::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
show "?A $$ (i, f i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multrow i0 a A $$ (i, f i) = (1::'a)
[PROOF STEP]
by (subst index_mat_multrow(1), insert * d i A jj fi, auto)
[PROOF STATE]
proof (state)
this:
multrow i0 a A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f i < jj \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f i < jj \<Longrightarrow> multrow i0 a A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
assume j: "j < f i"
[PROOF STATE]
proof (state)
this:
j < f i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
from p(2)[OF j]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
[PROOF STEP]
show "?A $$ (i, j) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. multrow i0 a A $$ (i, j) = (0::'a)
[PROOF STEP]
by (subst index_mat_multrow(1), insert j d i p jj fi, auto)
[PROOF STATE]
proof (state)
this:
multrow i0 a A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j2 < f i \<Longrightarrow> multrow i0 a A $$ (i, ?j2) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun (multrow i0 a A) f jj

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_fun_swaprows: assumes p: "pivot_fun A f jj"
  and d: "dim_row A = nr" "dim_col A = nc"
  and flk: "f l = jj" "f k = jj"
  and nr: "l < nr" "k < nr"
  and jj: "jj \<le> nc"
  shows "pivot_fun (swaprows l k A) f jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
note pivot = pivot_funD[OF d(1) p]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
let ?A = "swaprows l k A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
have "dim_row ?A = nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (swaprows l k A) = nr
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
dim_row A = nr
dim_col A = nc

goal (1 subgoal):
 1. dim_row (swaprows l k A) = nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row (swaprows l k A) = nr

goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_row (swaprows l k A) = nr

goal (1 subgoal):
 1. pivot_fun (swaprows l k A) f jj
[PROOF STEP]
proof (rule pivot_funI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
assume i: "i < nr"
[PROOF STATE]
proof (state)
this:
i < nr

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
note p = pivot[OF i]
[PROOF STATE]
proof (state)
this:
f i \<le> jj
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
f i < jj \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < jj; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> jj
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 4. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
show "f i \<le> jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f i \<le> jj
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f i \<le> jj

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
 3. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
show "Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = jj

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
assume *: "f i < jj" "i' < nr" "i' \<noteq> i"
[PROOF STATE]
proof (state)
this:
f i < jj
i' < nr
i' \<noteq> i

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
from *(1) flk
[PROOF STATE]
proof (chain)
picking this:
f i < jj
f l = jj
f k = jj
[PROOF STEP]
have diff: "l \<noteq> i" "k \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
f i < jj
f l = jj
f k = jj

goal (1 subgoal):
 1. l \<noteq> i &&& k \<noteq> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<noteq> i
k \<noteq> i

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; f i < jj; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
from p(5)[OF *] p(5)[OF *(1) nr(1) diff(1)] p(5)[OF *(1) nr(2) diff(2)]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i', f i) = (0::'a)
A $$ (l, f i) = (0::'a)
A $$ (k, f i) = (0::'a)
[PROOF STEP]
show "?A $$ (i', f i) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i', f i) = (0::'a)
A $$ (l, f i) = (0::'a)
A $$ (k, f i) = (0::'a)

goal (1 subgoal):
 1. swaprows l k A $$ (i', f i) = (0::'a)
[PROOF STEP]
by (subst index_mat_swaprows(1), insert * d jj, auto)
[PROOF STATE]
proof (state)
this:
swaprows l k A $$ (i', f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i < jj; ?i'2 < nr; ?i'2 \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (?i'2, f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>f i < jj; ?i'2 < nr; ?i'2 \<noteq> i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (?i'2, f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
assume *: "f i < jj"
[PROOF STATE]
proof (state)
this:
f i < jj

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
from p(4)[OF this]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, f i) = (1::'a)
[PROOF STEP]
have A: "A $$ (i, f i) = 1"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. A $$ (i, f i) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, f i) = (1::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; f i < jj\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
show "?A $$ (i, f i) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows l k A $$ (i, f i) = (1::'a)
[PROOF STEP]
by (subst index_mat_swaprows(1), insert * d i A jj flk, auto)
[PROOF STATE]
proof (state)
this:
swaprows l k A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f i < jj \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f i < jj \<Longrightarrow> swaprows l k A $$ (i, f i) = (1::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
assume j: "j < f i"
[PROOF STATE]
proof (state)
this:
j < f i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
with p(1) flk
[PROOF STATE]
proof (chain)
picking this:
f i \<le> jj
f l = jj
f k = jj
j < f i
[PROOF STEP]
have le: "j < f l" "j < f k"
[PROOF STATE]
proof (prove)
using this:
f i \<le> jj
f l = jj
f k = jj
j < f i

goal (1 subgoal):
 1. j < f l &&& j < f k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < f l
j < f k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
from p(2)[OF j] pivot(2)[OF nr(1) le(1)] pivot(2)[OF nr(2) le(2)]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
A $$ (l, j) = (0::'a)
A $$ (k, j) = (0::'a)
[PROOF STEP]
show "?A $$ (i, j) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
A $$ (l, j) = (0::'a)
A $$ (k, j) = (0::'a)

goal (1 subgoal):
 1. swaprows l k A $$ (i, j) = (0::'a)
[PROOF STEP]
by (subst index_mat_swaprows(1), insert j d i p jj, auto)
[PROOF STATE]
proof (state)
this:
swaprows l k A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j2 < f i \<Longrightarrow> swaprows l k A $$ (i, ?j2) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun (swaprows l k A) f jj

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_fun_eliminate_entries: assumes p: "pivot_fun A f jj"
  and d: "dim_row A = nr" "dim_col A = nc"
  and fl: "f l = jj"
  and nr: "l < nr"
  and jj: "jj \<le> nc"
shows "pivot_fun (eliminate_entries vs A l j) f jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
note pD = pivot_funD[OF d(1) p]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
assume *: "i < nr" "j < f i"
[PROOF STATE]
proof (state)
this:
i < nr
j < f i

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
from pD(1)[OF this(1)] this(2) jj
[PROOF STATE]
proof (chain)
picking this:
f i \<le> jj
j < f i
jj \<le> nc
[PROOF STEP]
have j: "j < nc"
[PROOF STATE]
proof (prove)
using this:
f i \<le> jj
j < f i
jj \<le> nc

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

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
from pD nr fl * j
[PROOF STATE]
proof (chain)
picking this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)
l < nr
f l = jj
i < nr
j < f i
j < nc
[PROOF STEP]
have "A $$ (l, j) = 0"
[PROOF STATE]
proof (prove)
using this:
?i < nr \<Longrightarrow> f ?i \<le> jj
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = jj
\<lbrakk>?i < nr; f ?i < jj\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < jj; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)
l < nr
f l = jj
i < nr
j < f i
j < nc

goal (1 subgoal):
 1. A $$ (l, j) = (0::'a)
[PROOF STEP]
by (meson less_le_trans)
[PROOF STATE]
proof (state)
this:
A $$ (l, j) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
note j this
[PROOF STATE]
proof (state)
this:
j < nc
A $$ (l, j) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?ja2 < f ?i2\<rbrakk> \<Longrightarrow> ?ja2 < nc
\<lbrakk>?i2 < nr; ?ja2 < f ?i2\<rbrakk> \<Longrightarrow> A $$ (l, ?ja2) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
note hint = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < nr; ?ja2 < f ?i2\<rbrakk> \<Longrightarrow> ?ja2 < nc
\<lbrakk>?i2 < nr; ?ja2 < f ?i2\<rbrakk> \<Longrightarrow> A $$ (l, ?ja2) = (0::'a)

goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (eliminate_entries vs A l j) f jj
[PROOF STEP]
by (rule pivot_funI, insert fl nr jj pD, auto simp: eliminate_entries_gen_def d hint)
[PROOF STATE]
proof (state)
this:
pivot_fun (eliminate_entries vs A l j) f jj

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pivot_fun_init: "pivot_fun A (\<lambda> _. 0) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun A (\<lambda>_. 0) 0
[PROOF STEP]
by (rule pivot_funI, auto)