[STATEMENT]
lemma non_pivot_base:
  defines pp: "pp \<equiv> pivot_positions A"
  assumes qj: "qj < nc" "qj \<notin> snd ` set pp"
  shows "non_pivot_base A pp qj \<in> carrier_vec nc"
    "non_pivot_base A pp qj $ qj = 1"
    "A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr"
    "\<And> qj'. qj' < nc \<Longrightarrow> qj' \<notin> snd ` set pp \<Longrightarrow> qj \<noteq> qj' \<Longrightarrow> non_pivot_base A pp qj $ qj' = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (non_pivot_base A pp qj \<in> carrier_vec nc &&& non_pivot_base A pp qj $ qj = (1::'a)) &&& A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr &&& (\<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
[PROOF STEP]
have dim: "dim_row A = nr" "dim_col A = nc"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. dim_row A = nr &&& dim_col A = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = nr
dim_col A = nc

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
from ref[unfolded row_echelon_form_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. pivot_fun A f (dim_col A)
[PROOF STEP]
obtain p
  where pivot: "pivot_fun A p nc"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p nc \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)
dim_row A = nr
dim_col A = nc

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p nc \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pivot_fun A p nc

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
note pivot' = pivot_funD[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> p ?i \<le> nc
\<lbrakk>?i < nr; ?j < p ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> p ?i < p (Suc ?i) \<or> p (Suc ?i) = nc
\<lbrakk>?i < nr; p ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, p ?i) = (1::'a)
\<lbrakk>?i < nr; p ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', p ?i) = (0::'a)

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
note pp = pivot_positions[OF A pivot, folded pp]
[PROOF STATE]
proof (state)
this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
distinct (map fst pp)
distinct (map snd pp)
length pp = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?p = "\<lambda> i. i < nr \<and> p i = nc \<or> i = nr"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?spp = "map prod.swap pp"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?map = "map_of ?spp"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
define I where "I = (\<lambda> i. case map_of (map prod.swap pp) i of Some j \<Rightarrow> - A $$ (j,qj) | None \<Rightarrow> 0)"
[PROOF STATE]
proof (state)
this:
I = (\<lambda>i. case map_of (map prod.swap pp) i of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj))

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
have d: "non_pivot_base A pp qj = vec nc (\<lambda> i. if i = qj then 1 else I i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_pivot_base A pp qj = vec nc (\<lambda>i. if i = qj then 1::'a else I i)
[PROOF STEP]
unfolding non_pivot_base_def Let_def dim I_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else case map_of (map prod.swap pp) i of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj)) = vec nc (\<lambda>i. if i = qj then 1::'a else case map_of (map prod.swap pp) i of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj = vec nc (\<lambda>i. if i = qj then 1::'a else I i)

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
from pp
[PROOF STATE]
proof (chain)
picking this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
distinct (map fst pp)
distinct (map snd pp)
length pp = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}
[PROOF STEP]
have dist: "distinct (map fst ?spp)"
[PROOF STATE]
proof (prove)
using this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
distinct (map fst pp)
distinct (map snd pp)
length pp = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal (1 subgoal):
 1. distinct (map fst (map prod.swap pp))
[PROOF STEP]
unfolding map_map o_def prod.swap_def
[PROOF STATE]
proof (prove)
using this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
distinct (map fst pp)
distinct (map snd pp)
length pp = card {i. i < nr \<and> row A i \<noteq> 0\<^sub>v nc}

goal (1 subgoal):
 1. distinct (map (\<lambda>x. fst (snd x, fst x)) pp)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (map fst (map prod.swap pp))

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?r = "set (map snd pp)"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
have r: "?r = p ` {0 ..< nr} - {nc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map snd pp) = p ` {0..<nr} - {nc}
[PROOF STEP]
unfolding set_map pp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` {(i, p i) |i. i < nr \<and> p i \<noteq> nc} = p ` {0..<nr} - {nc}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
set (map snd pp) = p ` {0..<nr} - {nc}

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?l = "set (map fst pp)"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
from qj
[PROOF STATE]
proof (chain)
picking this:
qj < nc
qj \<notin> snd ` set pp
[PROOF STEP]
have qj': "qj \<notin> p ` {0 ..< nr}"
[PROOF STATE]
proof (prove)
using this:
qj < nc
qj \<notin> snd ` set pp

goal (1 subgoal):
 1. qj \<notin> p ` {0..<nr}
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
qj < nc
qj \<notin> snd ` set pp
set (map snd pp) = p ` {0..<nr} - {nc}

goal (1 subgoal):
 1. qj \<notin> p ` {0..<nr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qj \<notin> p ` {0..<nr}

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?v = "non_pivot_base A pp qj"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
let ?P = "p ` {0 ..< nr}"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
have dimv: "dim_vec ?v = nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (non_pivot_base A pp qj) = nc
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec nc (\<lambda>i. if i = qj then 1::'a else I i)) = nc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (non_pivot_base A pp qj) = nc

goal (4 subgoals):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
 2. non_pivot_base A pp qj $ qj = (1::'a)
 3. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 4. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
thus "?v \<in> carrier_vec nc"
[PROOF STATE]
proof (prove)
using this:
dim_vec (non_pivot_base A pp qj) = nc

goal (1 subgoal):
 1. non_pivot_base A pp qj \<in> carrier_vec nc
[PROOF STEP]
unfolding carrier_vec_def
[PROOF STATE]
proof (prove)
using this:
dim_vec (non_pivot_base A pp qj) = nc

goal (1 subgoal):
 1. non_pivot_base A pp qj \<in> {v. dim_vec v = nc}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj \<in> carrier_vec nc

goal (3 subgoals):
 1. non_pivot_base A pp qj $ qj = (1::'a)
 2. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 3. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
show vqj: "?v $ qj = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_pivot_base A pp qj $ qj = (1::'a)
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ qj = (1::'a)
[PROOF STEP]
using qj
[PROOF STATE]
proof (prove)
using this:
qj < nc
qj \<notin> snd ` set pp

goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ qj = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ qj = (1::'a)

goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ qj = (1::'a)

goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
fix qj'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
assume *: "qj' < nc" "qj \<noteq> qj'" "qj' \<notin> snd ` set pp"
[PROOF STATE]
proof (state)
this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp

goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
hence "?map qj' = None"
[PROOF STATE]
proof (prove)
using this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp

goal (1 subgoal):
 1. map_of (map prod.swap pp) qj' = None
[PROOF STEP]
unfolding map_of_eq_None_iff
[PROOF STATE]
proof (prove)
using this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp

goal (1 subgoal):
 1. qj' \<notin> fst ` set (map prod.swap pp)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
map_of (map prod.swap pp) qj' = None

goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
hence "I qj' = 0"
[PROOF STATE]
proof (prove)
using this:
map_of (map prod.swap pp) qj' = None

goal (1 subgoal):
 1. I qj' = (0::'a)
[PROOF STEP]
unfolding I_def
[PROOF STATE]
proof (prove)
using this:
map_of (map prod.swap pp) qj' = None

goal (1 subgoal):
 1. (case map_of (map prod.swap pp) qj' of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj)) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I qj' = (0::'a)

goal (2 subgoals):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
 2. \<And>qj'. \<lbrakk>qj' < nc; qj' \<notin> snd ` set pp; qj \<noteq> qj'\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp
I qj' = (0::'a)
[PROOF STEP]
show "non_pivot_base A pp qj $ qj' = 0"
[PROOF STATE]
proof (prove)
using this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp
I qj' = (0::'a)

goal (1 subgoal):
 1. non_pivot_base A pp qj $ qj' = (0::'a)
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
using this:
qj' < nc
qj \<noteq> qj'
qj' \<notin> snd ` set pp
I qj' = (0::'a)

goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ qj' = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ qj' = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?qj'2 < nc; qj \<noteq> ?qj'2; ?qj'2 \<notin> snd ` set pp\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ ?qj'2 = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?qj'2 < nc; qj \<noteq> ?qj'2; ?qj'2 \<notin> snd ` set pp\<rbrakk> \<Longrightarrow> non_pivot_base A pp qj $ ?qj'2 = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
assume i: "i < nr"
[PROOF STATE]
proof (state)
this:
i < nr

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
let ?I = "{j. ?map j = Some i}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
have "row A i \<bullet> ?v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have id: "({0..<nc} \<inter> ?P) \<union> ({0..<nc} - ?P) = {0..<nc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<nc} \<inter> p ` {0..<nr} \<union> ({0..<nc} - p ` {0..<nr}) = {0..<nc}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<nc} \<inter> p ` {0..<nr} \<union> ({0..<nc} - p ` {0..<nr}) = {0..<nc}

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
let ?e = "\<lambda> j. row A i $ j * ?v $ j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
let ?e' = "\<lambda> j. (if ?map j = Some i then - A $$ (i, qj) else 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
assume j: "j < nc" "j \<in> ?P"
[PROOF STATE]
proof (state)
this:
j < nc
j \<in> p ` {0..<nr}

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < nc
j \<in> p ` {0..<nr}
[PROOF STEP]
obtain ii where ii: "ii < nr" and jpi: "j = p ii" and pii: "p ii < nc"
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<in> p ` {0..<nr}

goal (1 subgoal):
 1. (\<And>ii. \<lbrakk>ii < nr; j = p ii; p ii < nc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ii < nr
j = p ii
p ii < nc

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
hence mem: "(ii,j) \<in> set pp" and "(j,ii) \<in> set ?spp"
[PROOF STATE]
proof (prove)
using this:
ii < nr
j = p ii
p ii < nc

goal (1 subgoal):
 1. (ii, j) \<in> set pp &&& (j, ii) \<in> set (map prod.swap pp)
[PROOF STEP]
by (auto simp: pp)
[PROOF STATE]
proof (state)
this:
(ii, j) \<in> set pp
(j, ii) \<in> set (map prod.swap pp)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
from map_of_is_SomeI[OF dist this(2)]
[PROOF STATE]
proof (chain)
picking this:
map_of (map prod.swap pp) j = Some ii
[PROOF STEP]
have map: "?map j = Some ii"
[PROOF STATE]
proof (prove)
using this:
map_of (map prod.swap pp) j = Some ii

goal (1 subgoal):
 1. map_of (map prod.swap pp) j = Some ii
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_of (map prod.swap pp) j = Some ii

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
from mem j qj
[PROOF STATE]
proof (chain)
picking this:
(ii, j) \<in> set pp
j < nc
j \<in> p ` {0..<nr}
qj < nc
qj \<notin> snd ` set pp
[PROOF STEP]
have jqj: "j \<noteq> qj"
[PROOF STATE]
proof (prove)
using this:
(ii, j) \<in> set pp
j < nc
j \<in> p ` {0..<nr}
qj < nc
qj \<notin> snd ` set pp

goal (1 subgoal):
 1. j \<noteq> qj
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
j \<noteq> qj

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
note p = pivot'(4-5)[OF ii pii]
[PROOF STATE]
proof (state)
this:
A $$ (ii, p ii) = (1::'a)
\<lbrakk>?i' < nr; ?i' \<noteq> ii\<rbrakk> \<Longrightarrow> A $$ (?i', p ii) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
define start where "start = ?e j"
[PROOF STATE]
proof (state)
this:
start = row A i $ j * non_pivot_base A pp qj $ j

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "start = A $$ (i,j) * ?v $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. start = A $$ (i, j) * non_pivot_base A pp qj $ j
[PROOF STEP]
using j i A
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<in> p ` {0..<nr}
i < nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. start = A $$ (i, j) * non_pivot_base A pp qj $ j
[PROOF STEP]
by (auto simp: start_def)
[PROOF STATE]
proof (state)
this:
start = A $$ (i, j) * non_pivot_base A pp qj $ j

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
start = A $$ (i, j) * non_pivot_base A pp qj $ j

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "A $$ (i,j) = A $$ (i, p ii)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, j) = A $$ (i, p ii)
[PROOF STEP]
unfolding jpi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, p ii) = A $$ (i, p ii)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = A $$ (i, p ii)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = A $$ (i, p ii)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "\<dots> = (if i = ii then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, p ii) = (if i = ii then 1::'a else (0::'a))
[PROOF STEP]
using p(1) p(2)[OF i]
[PROOF STATE]
proof (prove)
using this:
A $$ (ii, p ii) = (1::'a)
i \<noteq> ii \<Longrightarrow> A $$ (i, p ii) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, p ii) = (if i = ii then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, p ii) = (if i = ii then 1::'a else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (i, p ii) = (if i = ii then 1::'a else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "\<dots> * ?v $ j = (if i = ii then ?v $ j else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = ii then 1::'a else (0::'a)) * non_pivot_base A pp qj $ j = (if i = ii then non_pivot_base A pp qj $ j else (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i = ii then 1::'a else (0::'a)) * non_pivot_base A pp qj $ j = (if i = ii then non_pivot_base A pp qj $ j else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if i = ii then 1::'a else (0::'a)) * non_pivot_base A pp qj $ j = (if i = ii then non_pivot_base A pp qj $ j else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "?v $ j = I j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_pivot_base A pp qj $ j = I j
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ j = I j
[PROOF STEP]
using j jqj A
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<in> p ` {0..<nr}
j \<noteq> qj
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ j = I j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ j = I j

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ j = I j

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "I j = - A $$ (ii, qj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I j = - A $$ (ii, qj)
[PROOF STEP]
unfolding I_def map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case Some ii of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj)) = - A $$ (ii, qj)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I j = - A $$ (ii, qj)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
start = (if i = ii then - A $$ (ii, qj) else (0::'a))
[PROOF STEP]
have "?e j = ?e' j"
[PROOF STATE]
proof (prove)
using this:
start = (if i = ii then - A $$ (ii, qj) else (0::'a))

goal (1 subgoal):
 1. row A i $ j * non_pivot_base A pp qj $ j = (if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))
[PROOF STEP]
unfolding start_def map
[PROOF STATE]
proof (prove)
using this:
row A i $ j * non_pivot_base A pp qj $ j = (if i = ii then - A $$ (ii, qj) else (0::'a))

goal (1 subgoal):
 1. row A i $ j * non_pivot_base A pp qj $ j = (if Some ii = Some i then - A $$ (i, qj) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row A i $ j * non_pivot_base A pp qj $ j = (if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j2 < nc; ?j2 \<in> p ` {0..<nr}\<rbrakk> \<Longrightarrow> row A i $ ?j2 * non_pivot_base A pp qj $ ?j2 = (if map_of (map prod.swap pp) ?j2 = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
note piv = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j2 < nc; ?j2 \<in> p ` {0..<nr}\<rbrakk> \<Longrightarrow> row A i $ ?j2 * non_pivot_base A pp qj $ ?j2 = (if map_of (map prod.swap pp) ?j2 = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "row A i \<bullet> ?v = (\<Sum> j = 0..<nc. ?e j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j)
[PROOF STEP]
unfolding row_def scalar_prod_def dimv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<nc. vec (dim_col A) (\<lambda>j. A $$ (i, j)) $ ia * non_pivot_base A pp qj $ ia) = (\<Sum>j = 0..<nc. vec (dim_col A) (\<lambda>j. A $$ (i, j)) $ j * non_pivot_base A pp qj $ j)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
row A i \<bullet> non_pivot_base A pp qj = (\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row A i \<bullet> non_pivot_base A pp qj = (\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "\<dots> = sum ?e ({0..<nc} \<inter> ?P) + sum ?e ({0..<nc} - ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j)
[PROOF STEP]
by (subst sum.union_disjoint[symmetric], auto simp: id)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<nc. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e ({0..<nc} - ?P) = ?e qj + sum ?e ({0 ..<nc} - ?P - {qj})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = row A i $ qj * non_pivot_base A pp qj $ qj + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j)
[PROOF STEP]
by (rule sum.remove, insert qj qj', auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = row A i $ qj * non_pivot_base A pp qj $ qj + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} - p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = row A i $ qj * non_pivot_base A pp qj $ qj + (\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "?e qj = row A i $ qj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i $ qj * non_pivot_base A pp qj $ qj = row A i $ qj
[PROOF STEP]
unfolding vqj
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i $ qj * (1::'a) = row A i $ qj
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row A i $ qj * non_pivot_base A pp qj $ qj = row A i $ qj

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row A i $ qj * non_pivot_base A pp qj $ qj = row A i $ qj

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "row A i $ qj = A $$ (i, qj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A i $ qj = A $$ (i, qj)
[PROOF STEP]
using i A qj
[PROOF STATE]
proof (prove)
using this:
i < nr
A \<in> carrier_mat nr nc
qj < nc
qj \<notin> snd ` set pp

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

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row A i $ qj = A $$ (i, qj)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e ({0 ..<nc} - ?P - {qj}) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
assume "j \<in> {0 ..<nc} - ?P - {qj}"
[PROOF STATE]
proof (state)
this:
j \<in> {0..<nc} - p ` {0..<nr} - {qj}

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
hence j: "j < nc" "j \<notin> ?P" "j \<noteq> qj" "j \<notin> ?r"
[PROOF STATE]
proof (prove)
using this:
j \<in> {0..<nc} - p ` {0..<nr} - {qj}

goal (1 subgoal):
 1. (j < nc &&& j \<notin> p ` {0..<nr}) &&& j \<noteq> qj &&& j \<notin> set (map snd pp)
[PROOF STEP]
unfolding r
[PROOF STATE]
proof (prove)
using this:
j \<in> {0..<nc} - p ` {0..<nr} - {qj}

goal (1 subgoal):
 1. (j < nc &&& j \<notin> p ` {0..<nr}) &&& j \<noteq> qj &&& j \<notin> p ` {0..<nr} - {nc}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < nc
j \<notin> p ` {0..<nr}
j \<noteq> qj
j \<notin> set (map snd pp)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
hence id: "map_of ?spp j = None"
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<notin> p ` {0..<nr}
j \<noteq> qj
j \<notin> set (map snd pp)

goal (1 subgoal):
 1. map_of (map prod.swap pp) j = None
[PROOF STEP]
unfolding map_of_eq_None_iff
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<notin> p ` {0..<nr}
j \<noteq> qj
j \<notin> set (map snd pp)

goal (1 subgoal):
 1. j \<notin> fst ` set (map prod.swap pp)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
map_of (map prod.swap pp) j = None

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
have "?v $ j = I j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_pivot_base A pp qj $ j = I j
[PROOF STEP]
unfolding d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ j = I j
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
j < nc
j \<notin> p ` {0..<nr}
j \<noteq> qj
j \<notin> set (map snd pp)

goal (1 subgoal):
 1. vec nc (\<lambda>i. if i = qj then 1::'a else I i) $ j = I j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ j = I j

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
non_pivot_base A pp qj $ j = I j

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I j = (0::'a)
[PROOF STEP]
unfolding I_def id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case None of None \<Rightarrow> 0::'a | Some j \<Rightarrow> - A $$ (j, qj)) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
I j = (0::'a)

goal (1 subgoal):
 1. \<And>x. x \<in> {0..<nc} - p ` {0..<nr} - {qj} \<Longrightarrow> row A i $ x * non_pivot_base A pp qj $ x = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
non_pivot_base A pp qj $ j = (0::'a)
[PROOF STEP]
show "row A i $ j * ?v $ j = 0"
[PROOF STATE]
proof (prove)
using this:
non_pivot_base A pp qj $ j = (0::'a)

goal (1 subgoal):
 1. row A i $ j * non_pivot_base A pp qj $ j = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
row A i $ j * non_pivot_base A pp qj $ j = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} - p ` {0..<nr} - {qj}. row A i $ j * non_pivot_base A pp qj $ j) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "A $$ (i, qj) + 0 = A $$ (i, qj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, qj) + (0::'a) = A $$ (i, qj)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A $$ (i, qj) + (0::'a) = A $$ (i, qj)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (i, qj) + (0::'a) = A $$ (i, qj)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e ({0..<nc} \<inter> ?P) = sum ?e' ({0..<nc} \<inter> ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))
[PROOF STEP]
by (rule sum.cong, insert piv, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. row A i $ j * non_pivot_base A pp qj $ j) = (\<Sum>j\<in>{0..<nc} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "{0..<nc} \<inter> ?P = {0..<nc} \<inter> ?I \<inter> ?P \<union> ({0..<nc} - ?I) \<inter> ?P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<nc} \<inter> p ` {0..<nr} = {0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<nc} \<inter> p ` {0..<nr} = {0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{0..<nc} \<inter> p ` {0..<nr} = {0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e' ({0..<nc} \<inter> ?I \<inter> ?P \<union> ({0..<nc} - ?I) \<inter> ?P)
        = sum ?e' ({0..<nc} \<inter> ?I \<inter> ?P) + sum ?e' (({0..<nc} - ?I) \<inter> ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) + (\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))
[PROOF STEP]
by (rule sum.union_disjoint, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) + (\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} \<union> ({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) + (\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e' (({0..<nc} - ?I) \<inter> ?P) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>({0..<nc} - {j. map_of (map prod.swap pp) j = Some i}) \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum ?e' ({0..<nc} \<inter> ?I \<inter> ?P) =
        sum (\<lambda> _. - A $$ (i, qj)) ({0..<nc} \<inter> ?I \<inter> ?P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. if map_of (map prod.swap pp) j = Some i then - A $$ (i, qj) else (0::'a)) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "\<dots> + 0 = \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + (0::'a) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + (0::'a) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + (0::'a) = (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj))

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
have "sum (\<lambda> _. - A $$ (i, qj)) ({0..<nc} \<inter> ?I \<inter> ?P) + A $$ (i, qj) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
proof (cases "i \<in> ?l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
 2. i \<notin> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<notin> set (map fst pp)

goal (2 subgoals):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
 2. i \<notin> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
with pp(1) i
[PROOF STATE]
proof (chain)
picking this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
i < nr
i \<notin> set (map fst pp)
[PROOF STEP]
have "p i = nc"
[PROOF STATE]
proof (prove)
using this:
set pp = {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
i < nr
i \<notin> set (map fst pp)

goal (1 subgoal):
 1. p i = nc
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
p i = nc

goal (2 subgoals):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
 2. i \<notin> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
from pivot'(2)[OF i, unfolded this, OF qj(1)]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, qj) = (0::'a)
[PROOF STEP]
have z: "A $$ (i, qj) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, qj) = (0::'a)

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

goal (2 subgoals):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
 2. i \<notin> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
by (subst sum.neutral, auto simp: z)
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i \<in> set (map fst pp)

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (map fst pp)
[PROOF STEP]
obtain j where mem: "(i,j) \<in> set pp" and id: "(j,i) \<in> set ?spp"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (map fst pp)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>(i, j) \<in> set pp; (j, i) \<in> set (map prod.swap pp)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, j) \<in> set pp
(j, i) \<in> set (map prod.swap pp)

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
from map_of_is_SomeI[OF dist this(2)]
[PROOF STATE]
proof (chain)
picking this:
map_of (map prod.swap pp) j = Some i
[PROOF STEP]
have map: "?map j = Some i"
[PROOF STATE]
proof (prove)
using this:
map_of (map prod.swap pp) j = Some i

goal (1 subgoal):
 1. map_of (map prod.swap pp) j = Some i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map_of (map prod.swap pp) j = Some i

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
from pivot'(1)[OF i]
[PROOF STATE]
proof (chain)
picking this:
p i \<le> nc
[PROOF STEP]
have pi: "p i \<le> nc"
[PROOF STATE]
proof (prove)
using this:
p i \<le> nc

goal (1 subgoal):
 1. p i \<le> nc
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p i \<le> nc

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
with mem[unfolded pp]
[PROOF STATE]
proof (chain)
picking this:
(i, j) \<in> {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
p i \<le> nc
[PROOF STEP]
have j: "j = p i" "j < nc"
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
p i \<le> nc

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

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
j = p i
j < nc

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
fix j'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
assume "j' \<in> ?I"
[PROOF STATE]
proof (state)
this:
j' \<in> {j. map_of (map prod.swap pp) j = Some i}

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
hence "?map j' = Some i"
[PROOF STATE]
proof (prove)
using this:
j' \<in> {j. map_of (map prod.swap pp) j = Some i}

goal (1 subgoal):
 1. map_of (map prod.swap pp) j' = Some i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_of (map prod.swap pp) j' = Some i

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
from map_of_SomeD[OF this]
[PROOF STATE]
proof (chain)
picking this:
(j', i) \<in> set (map prod.swap pp)
[PROOF STEP]
have "(i, j') \<in> set pp"
[PROOF STATE]
proof (prove)
using this:
(j', i) \<in> set (map prod.swap pp)

goal (1 subgoal):
 1. (i, j') \<in> set pp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, j') \<in> set pp

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
with mem pp(2)
[PROOF STATE]
proof (chain)
picking this:
(i, j) \<in> set pp
distinct (map fst pp)
(i, j') \<in> set pp
[PROOF STEP]
have "j' = j"
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> set pp
distinct (map fst pp)
(i, j') \<in> set pp

goal (1 subgoal):
 1. j' = j
[PROOF STEP]
using map_of_is_SomeI
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> set pp
distinct (map fst pp)
(i, j') \<in> set pp
\<lbrakk>distinct (map fst ?xys); (?x, ?y) \<in> set ?xys\<rbrakk> \<Longrightarrow> map_of ?xys ?x = Some ?y

goal (1 subgoal):
 1. j' = j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
j' = j

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j'2 \<in> {j. map_of (map prod.swap pp) j = Some i} \<Longrightarrow> ?j'2 = j

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
with map
[PROOF STATE]
proof (chain)
picking this:
map_of (map prod.swap pp) j = Some i
?j'2 \<in> {j. map_of (map prod.swap pp) j = Some i} \<Longrightarrow> ?j'2 = j
[PROOF STEP]
have II: "?I = {j}"
[PROOF STATE]
proof (prove)
using this:
map_of (map prod.swap pp) j = Some i
?j'2 \<in> {j. map_of (map prod.swap pp) j = Some i} \<Longrightarrow> ?j'2 = j

goal (1 subgoal):
 1. {j. map_of (map prod.swap pp) j = Some i} = {j}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{j. map_of (map prod.swap pp) j = Some i} = {j}

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
have II: "{0..<nc} \<inter> ?I \<inter> ?P = {j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} = {j}
[PROOF STEP]
unfolding II
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<nc} \<inter> {j} \<inter> p ` {0..<nr} = {j}
[PROOF STEP]
using mem[unfolded pp] i j
[PROOF STATE]
proof (prove)
using this:
(i, j) \<in> {(i, p i) |i. i < nr \<and> p i \<noteq> nc}
i < nr
j = p i
j < nc

goal (1 subgoal):
 1. {0..<nc} \<inter> {j} \<inter> p ` {0..<nr} = {j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr} = {j}

goal (1 subgoal):
 1. i \<in> set (map fst pp) \<Longrightarrow> (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
unfolding II
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>{j}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>{0..<nc} \<inter> {j. map_of (map prod.swap pp) j = Some i} \<inter> p ` {0..<nr}. - A $$ (i, qj)) + A $$ (i, qj) = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
show "row A i \<bullet> ?v = 0"
[PROOF STATE]
proof (prove)
using this:
row A i \<bullet> non_pivot_base A pp qj = (0::'a)

goal (1 subgoal):
 1. row A i \<bullet> non_pivot_base A pp qj = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
row A i \<bullet> non_pivot_base A pp qj = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row A i \<bullet> non_pivot_base A pp qj = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < nr \<Longrightarrow> row A ?i2 \<bullet> non_pivot_base A pp qj = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
?i2 < nr \<Longrightarrow> row A ?i2 \<bullet> non_pivot_base A pp qj = (0::'a)

goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
show "A *\<^sub>v ?v = 0\<^sub>v nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr
[PROOF STEP]
by (rule eq_vecI, auto simp: dim main)
[PROOF STATE]
proof (state)
this:
A *\<^sub>v non_pivot_base A pp qj = 0\<^sub>v nr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_base_vector: assumes "snd ` set (pivot_positions A) \<noteq> {0 ..< nc}"
  shows
    "find_base_vector A \<in> carrier_vec nc"
    "find_base_vector A \<noteq> 0\<^sub>v nc"
    "A *\<^sub>v find_base_vector A = 0\<^sub>v nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_base_vector A \<in> carrier_vec nc &&& find_base_vector A \<noteq> 0\<^sub>v nc &&& A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
define cands where "cands = filter (\<lambda> j. j \<notin> snd ` set (pivot_positions A)) [0 ..< nc]"
[PROOF STATE]
proof (state)
this:
cands = filter (\<lambda>j. j \<notin> snd ` set (pivot_positions A)) [0..<nc]

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
[PROOF STEP]
have dim: "dim_row A = nr" "dim_col A = nc"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. dim_row A = nr &&& dim_col A = nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = nr
dim_col A = nc

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
from ref[unfolded row_echelon_form_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. pivot_fun A f (dim_col A)
[PROOF STEP]
obtain p
  where pivot: "pivot_fun A p nc"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p nc \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)
dim_row A = nr
dim_col A = nc

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p nc \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pivot_fun A p nc

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
note piv = pivot_funD[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> p ?i \<le> nc
\<lbrakk>?i < nr; ?j < p ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> p ?i < p (Suc ?i) \<or> p (Suc ?i) = nc
\<lbrakk>?i < nr; p ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, p ?i) = (1::'a)
\<lbrakk>?i < nr; p ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', p ?i) = (0::'a)

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
have "set cands \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set cands \<noteq> {}
[PROOF STEP]
using assms piv
[PROOF STATE]
proof (prove)
using this:
snd ` set (pivot_positions A) \<noteq> {0..<nc}
?i < nr \<Longrightarrow> p ?i \<le> nc
\<lbrakk>?i < nr; ?j < p ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> p ?i < p (Suc ?i) \<or> p (Suc ?i) = nc
\<lbrakk>?i < nr; p ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, p ?i) = (1::'a)
\<lbrakk>?i < nr; p ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', p ?i) = (0::'a)

goal (1 subgoal):
 1. set cands \<noteq> {}
[PROOF STEP]
unfolding cands_def  pivot_positions[OF A pivot]
[PROOF STATE]
proof (prove)
using this:
snd ` {(i, p i) |i. i < nr \<and> p i \<noteq> nc} \<noteq> {0..<nc}
?i < nr \<Longrightarrow> p ?i \<le> nc
\<lbrakk>?i < nr; ?j < p ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> p ?i < p (Suc ?i) \<or> p (Suc ?i) = nc
\<lbrakk>?i < nr; p ?i < nc\<rbrakk> \<Longrightarrow> A $$ (?i, p ?i) = (1::'a)
\<lbrakk>?i < nr; p ?i < nc; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', p ?i) = (0::'a)

goal (1 subgoal):
 1. set (filter (\<lambda>j. j \<notin> snd ` {(i, p i) |i. i < nr \<and> p i \<noteq> nc}) [0..<nc]) \<noteq> {}
[PROOF STEP]
by (auto simp: le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
set cands \<noteq> {}

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set cands \<noteq> {}
[PROOF STEP]
obtain c cs where cands: "cands = c # cs"
[PROOF STATE]
proof (prove)
using this:
set cands \<noteq> {}

goal (1 subgoal):
 1. (\<And>c cs. cands = c # cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases cands, auto)
[PROOF STATE]
proof (state)
this:
cands = c # cs

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
hence res: "find_base_vector A = non_pivot_base A (pivot_positions A) c"
[PROOF STATE]
proof (prove)
using this:
cands = c # cs

goal (1 subgoal):
 1. find_base_vector A = non_pivot_base A (pivot_positions A) c
[PROOF STEP]
unfolding find_base_vector_def Let_def cands_def dim
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>j. j \<notin> snd ` set (pivot_positions A)) [0..<nc] = c # cs

goal (1 subgoal):
 1. non_pivot_base A (pivot_positions A) (hd (filter (\<lambda>j. j \<notin> set (map snd (pivot_positions A))) [0..<nc])) = non_pivot_base A (pivot_positions A) c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_base_vector A = non_pivot_base A (pivot_positions A) c

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
from cands
[PROOF STATE]
proof (chain)
picking this:
cands = c # cs
[PROOF STEP]
have "c \<in> set cands"
[PROOF STATE]
proof (prove)
using this:
cands = c # cs

goal (1 subgoal):
 1. c \<in> set cands
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> set cands

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
hence c: "c < nc" "c \<notin> snd ` set (pivot_positions A)"
[PROOF STATE]
proof (prove)
using this:
c \<in> set cands

goal (1 subgoal):
 1. c < nc &&& c \<notin> snd ` set (pivot_positions A)
[PROOF STEP]
unfolding cands_def
[PROOF STATE]
proof (prove)
using this:
c \<in> set (filter (\<lambda>j. j \<notin> snd ` set (pivot_positions A)) [0..<nc])

goal (1 subgoal):
 1. c < nc &&& c \<notin> snd ` set (pivot_positions A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c < nc
c \<notin> snd ` set (pivot_positions A)

goal (3 subgoals):
 1. find_base_vector A \<in> carrier_vec nc
 2. find_base_vector A \<noteq> 0\<^sub>v nc
 3. A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
from non_pivot_base[OF this, folded res] c
[PROOF STATE]
proof (chain)
picking this:
find_base_vector A \<in> carrier_vec nc
find_base_vector A $ c = (1::'a)
A *\<^sub>v find_base_vector A = 0\<^sub>v nr
\<lbrakk>?qj' < nc; ?qj' \<notin> snd ` set (pivot_positions A); c \<noteq> ?qj'\<rbrakk> \<Longrightarrow> find_base_vector A $ ?qj' = (0::'a)
c < nc
c \<notin> snd ` set (pivot_positions A)
[PROOF STEP]
show
    "find_base_vector A \<in> carrier_vec nc"
    "find_base_vector A \<noteq> 0\<^sub>v nc"
    "A *\<^sub>v find_base_vector A = 0\<^sub>v nr"
[PROOF STATE]
proof (prove)
using this:
find_base_vector A \<in> carrier_vec nc
find_base_vector A $ c = (1::'a)
A *\<^sub>v find_base_vector A = 0\<^sub>v nr
\<lbrakk>?qj' < nc; ?qj' \<notin> snd ` set (pivot_positions A); c \<noteq> ?qj'\<rbrakk> \<Longrightarrow> find_base_vector A $ ?qj' = (0::'a)
c < nc
c \<notin> snd ` set (pivot_positions A)

goal (1 subgoal):
 1. find_base_vector A \<in> carrier_vec nc &&& find_base_vector A \<noteq> 0\<^sub>v nc &&& A *\<^sub>v find_base_vector A = 0\<^sub>v nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_base_vector A \<in> carrier_vec nc
find_base_vector A \<noteq> 0\<^sub>v nc
A *\<^sub>v find_base_vector A = 0\<^sub>v nr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_echelon_form_imp_1_or_0_row: assumes A: "A \<in> carrier_mat n n"
  and row: "row_echelon_form A"
  shows "A = 1\<^sub>m n \<or> (n > 0 \<and> row A (n - 1) = 0\<^sub>v n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have dim: "dim_row A = n" "dim_col A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n &&& dim_col A = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n
dim_col A = n

goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from row[unfolded row_echelon_form_def] A
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. pivot_fun A f (dim_col A)
A \<in> carrier_mat n n
[PROOF STEP]
obtain f where pivot: "pivot_fun A f n"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)
A \<in> carrier_mat n n

goal (1 subgoal):
 1. (\<And>f. pivot_fun A f n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pivot_fun A f n

goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
note p = pivot_funD[OF dim(1) this]
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> f ?i \<le> n
\<lbrakk>?i < n; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < n; Suc ?i < n\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = n
\<lbrakk>?i < n; f ?i < n\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < n; f ?i < n; ?i' < n; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
proof (cases "\<exists> i < n. f i \<noteq> i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>i<n. f i \<noteq> i

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i<n. f i \<noteq> i
[PROOF STEP]
obtain i where i: "i < n" and fi: "f i \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
\<exists>i<n. f i \<noteq> i

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; f i \<noteq> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n
f i \<noteq> i

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
note pb = pivot_bound[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i + ?j < n \<Longrightarrow> f (?i + ?j) = n \<or> ?j + f ?i \<le> f (?i + ?j)

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from pb[of 0 i] i
[PROOF STATE]
proof (chain)
picking this:
0 + i < n \<Longrightarrow> f (0 + i) = n \<or> i + f 0 \<le> f (0 + i)
i < n
[PROOF STEP]
have "f i = n \<or> i \<le> f i"
[PROOF STATE]
proof (prove)
using this:
0 + i < n \<Longrightarrow> f (0 + i) = n \<or> i + f 0 \<le> f (0 + i)
i < n

goal (1 subgoal):
 1. f i = n \<or> i \<le> f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i = n \<or> i \<le> f i

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
with fi
[PROOF STATE]
proof (chain)
picking this:
f i \<noteq> i
f i = n \<or> i \<le> f i
[PROOF STEP]
have fi: "f i = n \<or> i < f i"
[PROOF STATE]
proof (prove)
using this:
f i \<noteq> i
f i = n \<or> i \<le> f i

goal (1 subgoal):
 1. f i = n \<or> i < f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f i = n \<or> i < f i

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < n
[PROOF STEP]
have n: "n - 1 = i + (n - i - 1)"
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. n - 1 = i + (n - i - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - 1 = i + (n - i - 1)

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from pb[of i "n - i - 1", folded n] fi i p(1)[of "n - 1"]
[PROOF STATE]
proof (chain)
picking this:
n - 1 < n \<Longrightarrow> f (n - 1) = n \<or> n - i - 1 + f i \<le> f (n - 1)
f i = n \<or> i < f i
i < n
n - 1 < n \<Longrightarrow> f (n - 1) \<le> n
[PROOF STEP]
have fn: "f (n - 1) = n"
[PROOF STATE]
proof (prove)
using this:
n - 1 < n \<Longrightarrow> f (n - 1) = n \<or> n - i - 1 + f i \<le> f (n - 1)
f i = n \<or> i < f i
i < n
n - 1 < n \<Longrightarrow> f (n - 1) \<le> n

goal (1 subgoal):
 1. f (n - 1) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (n - 1) = n

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < n
[PROOF STEP]
have n0: "n > 0" and n1: "n - 1 < n"
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. 0 < n &&& n - 1 < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n
n - 1 < n

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from p(2)[OF n1, unfolded fn]
[PROOF STATE]
proof (chain)
picking this:
?j < n \<Longrightarrow> A $$ (n - 1, ?j) = (0::'a)
[PROOF STEP]
have zero: "\<And> j. j < n \<Longrightarrow> A $$ (n - 1, j) = 0"
[PROOF STATE]
proof (prove)
using this:
?j < n \<Longrightarrow> A $$ (n - 1, ?j) = (0::'a)

goal (1 subgoal):
 1. \<And>j. j < n \<Longrightarrow> A $$ (n - 1, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?j < n \<Longrightarrow> A $$ (n - 1, ?j) = (0::'a)

goal (2 subgoals):
 1. \<exists>i<n. f i \<noteq> i \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
 2. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
by (rule disjI2[OF conjI[OF n0]], rule eq_vecI, insert zero A, auto)
[PROOF STATE]
proof (state)
this:
A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i<n. f i \<noteq> i)

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i<n. f i \<noteq> i)

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
assume j: "j < n"
[PROOF STATE]
proof (state)
this:
j < n

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>i<n. f i \<noteq> i)
j < n
[PROOF STEP]
have id: "f j = j"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>i<n. f i \<noteq> i)
j < n

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

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
note pj = p[OF j, unfolded id]
[PROOF STATE]
proof (state)
this:
j \<le> n
?j < j \<Longrightarrow> A $$ (j, ?j) = (0::'a)
Suc j < n \<Longrightarrow> j < f (Suc j) \<or> f (Suc j) = n
j < n \<Longrightarrow> A $$ (j, j) = (1::'a)
\<lbrakk>j < n; ?i' < n; ?i' \<noteq> j\<rbrakk> \<Longrightarrow> A $$ (?i', j) = (0::'a)

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
from pj(5)[OF j] pj(4)[OF j]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i' < n; ?i' \<noteq> j\<rbrakk> \<Longrightarrow> A $$ (?i', j) = (0::'a)
A $$ (j, j) = (1::'a)
[PROOF STEP]
have "\<And> i. i < n \<Longrightarrow> A $$ (i,j) = (if i = j then 1 else 0)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i' < n; ?i' \<noteq> j\<rbrakk> \<Longrightarrow> A $$ (?i', j) = (0::'a)
A $$ (j, j) = (1::'a)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> A $$ (i, j) = (if i = j then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> A $$ (?i, j) = (if ?i = j then 1::'a else (0::'a))

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j3 < n; ?i < n\<rbrakk> \<Longrightarrow> A $$ (?i, ?j3) = (if ?i = ?j3 then 1::'a else (0::'a))

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
note id = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j3 < n; ?i < n\<rbrakk> \<Longrightarrow> A $$ (?i, ?j3) = (if ?i = ?j3 then 1::'a else (0::'a))

goal (1 subgoal):
 1. \<not> (\<exists>i<n. f i \<noteq> i) \<Longrightarrow> A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
by (rule disjI1, rule eq_matI, subst id, insert A, auto)
[PROOF STATE]
proof (state)
this:
A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_base_vector_not_1_pivot_positions: "snd ` set (pivot_positions A) \<noteq> {0 ..< n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` set (pivot_positions A) \<noteq> {0..<n}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
let ?pp = "pivot_positions A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
assume id: "snd ` set ?pp = {0 ..< n}"
[PROOF STATE]
proof (state)
this:
snd ` set (pivot_positions A) = {0..<n}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have dim: "dim_row A = n" "dim_col A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. dim_row A = n &&& dim_col A = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = n
dim_col A = n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
let ?n = "n - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
from row_echelon_form_imp_1_or_0_row[OF A ref] 1
[PROOF STATE]
proof (chain)
picking this:
A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
A \<noteq> 1\<^sub>m n
[PROOF STEP]
have *: "0 < n" and row: "row A ?n = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
A = 1\<^sub>m n \<or> 0 < n \<and> row A (n - 1) = 0\<^sub>v n
A \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. 0 < n &&& row A (n - 1) = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < n
row A (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
from ref[unfolded row_echelon_form_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. pivot_fun A f (dim_col A)
[PROOF STEP]
obtain p
    where pivot: "pivot_fun A p n"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
\<exists>f. pivot_fun A f (dim_col A)
dim_row A = n
dim_col A = n

goal (1 subgoal):
 1. (\<And>p. pivot_fun A p n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pivot_fun A p n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
note pp = pivot_positions[OF A pivot]
[PROOF STATE]
proof (state)
this:
set (pivot_positions A) = {(i, p i) |i. i < n \<and> p i \<noteq> n}
distinct (map fst (pivot_positions A))
distinct (map snd (pivot_positions A))
length (pivot_positions A) = card {i. i < n \<and> row A i \<noteq> 0\<^sub>v n}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
note piv = pivot_funD[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < n \<Longrightarrow> p ?i \<le> n
\<lbrakk>?i < n; ?j < p ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < n; Suc ?i < n\<rbrakk> \<Longrightarrow> p ?i < p (Suc ?i) \<or> p (Suc ?i) = n
\<lbrakk>?i < n; p ?i < n\<rbrakk> \<Longrightarrow> A $$ (?i, p ?i) = (1::'a)
\<lbrakk>?i < n; p ?i < n; ?i' < n; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', p ?i) = (0::'a)

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
have n: "?n < n"
[PROOF STATE]
proof (prove)
using this:
0 < n

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

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n - 1 < n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
assume "p ?n < n"
[PROOF STATE]
proof (state)
this:
p (n - 1) < n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
with piv(4)[OF n this] row n A
[PROOF STATE]
proof (chain)
picking this:
A $$ (n - 1, p (n - 1)) = (1::'a)
row A (n - 1) = 0\<^sub>v n
n - 1 < n
A \<in> carrier_mat n n
p (n - 1) < n
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A $$ (n - 1, p (n - 1)) = (1::'a)
row A (n - 1) = 0\<^sub>v n
n - 1 < n
A \<in> carrier_mat n n
p (n - 1) < n

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis dim index_row(1) index_zero_vec(1) zero_neq_one)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
p (n - 1) < n \<Longrightarrow> False

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
with piv(1)[OF n]
[PROOF STATE]
proof (chain)
picking this:
p (n - 1) \<le> n
p (n - 1) < n \<Longrightarrow> False
[PROOF STEP]
have pn: "p ?n = n"
[PROOF STATE]
proof (prove)
using this:
p (n - 1) \<le> n
p (n - 1) < n \<Longrightarrow> False

goal (1 subgoal):
 1. p (n - 1) = n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p (n - 1) = n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
hence "?n \<notin> fst ` set ?pp"
[PROOF STATE]
proof (prove)
using this:
p (n - 1) = n

goal (1 subgoal):
 1. n - 1 \<notin> fst ` set (pivot_positions A)
[PROOF STEP]
unfolding pp
[PROOF STATE]
proof (prove)
using this:
p (n - 1) = n

goal (1 subgoal):
 1. n - 1 \<notin> fst ` {(i, p i) |i. i < n \<and> p i \<noteq> n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - 1 \<notin> fst ` set (pivot_positions A)

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
hence "fst ` set ?pp \<subseteq> {0 ..< n} - {?n}"
[PROOF STATE]
proof (prove)
using this:
n - 1 \<notin> fst ` set (pivot_positions A)

goal (1 subgoal):
 1. fst ` set (pivot_positions A) \<subseteq> {0..<n} - {n - 1}
[PROOF STEP]
unfolding pp
[PROOF STATE]
proof (prove)
using this:
n - 1 \<notin> fst ` {(i, p i) |i. i < n \<and> p i \<noteq> n}

goal (1 subgoal):
 1. fst ` {(i, p i) |i. i < n \<and> p i \<noteq> n} \<subseteq> {0..<n} - {n - 1}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst ` set (pivot_positions A) \<subseteq> {0..<n} - {n - 1}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fst ` set (pivot_positions A) \<subseteq> {0..<n} - {n - 1}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<subseteq> {0 ..< n - 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<n} - {n - 1} \<subseteq> {0..<n - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..<n} - {n - 1} \<subseteq> {0..<n - 1}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fst ` set (pivot_positions A) \<subseteq> {0..<n - 1}
[PROOF STEP]
have "card (fst ` set ?pp) \<le> card {0 ..< n - 1}"
[PROOF STATE]
proof (prove)
using this:
fst ` set (pivot_positions A) \<subseteq> {0..<n - 1}

goal (1 subgoal):
 1. card (fst ` set (pivot_positions A)) \<le> card {0..<n - 1}
[PROOF STEP]
using card_mono
[PROOF STATE]
proof (prove)
using this:
fst ` set (pivot_positions A) \<subseteq> {0..<n - 1}
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. card (fst ` set (pivot_positions A)) \<le> card {0..<n - 1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (fst ` set (pivot_positions A)) \<le> card {0..<n - 1}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (fst ` set (pivot_positions A)) \<le> card {0..<n - 1}

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {0..<n - 1} = n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {0..<n - 1} = n - 1

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {0..<n - 1} = n - 1

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
have "card (fst ` set ?pp) = card (snd ` set ?pp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (fst ` set (pivot_positions A)) = card (snd ` set (pivot_positions A))
[PROOF STEP]
unfolding set_map[symmetric] distinct_card[OF pp(2)] distinct_card[OF pp(3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map fst (pivot_positions A)) = length (map snd (pivot_positions A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (fst ` set (pivot_positions A)) = card (snd ` set (pivot_positions A))

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (fst ` set (pivot_positions A)) = card (snd ` set (pivot_positions A))

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (snd ` set (pivot_positions A)) = n
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {0..<n} = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (snd ` set (pivot_positions A)) = n

goal (1 subgoal):
 1. snd ` set (pivot_positions A) = {0..<n} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n \<le> n - 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<le> n - 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n \<le> n - 1
n - 1 < n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_base_vector_not_1:
    "find_base_vector A \<in> carrier_vec n"
    "find_base_vector A \<noteq> 0\<^sub>v n"
    "A *\<^sub>v find_base_vector A = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_base_vector A \<in> carrier_vec n &&& find_base_vector A \<noteq> 0\<^sub>v n &&& A *\<^sub>v find_base_vector A = 0\<^sub>v n
[PROOF STEP]
using find_base_vector[OF ref A find_base_vector_not_1_pivot_positions]
[PROOF STATE]
proof (prove)
using this:
find_base_vector A \<in> carrier_vec n
find_base_vector A \<noteq> 0\<^sub>v n
A *\<^sub>v find_base_vector A = 0\<^sub>v n

goal (1 subgoal):
 1. find_base_vector A \<in> carrier_vec n &&& find_base_vector A \<noteq> 0\<^sub>v n &&& A *\<^sub>v find_base_vector A = 0\<^sub>v n
[PROOF STEP]
.