[STATEMENT]
lemma sub2_preserves_dimensions[simp]:
  assumes rA': "sub2 d l (r,A) = (r',A')"
  shows "dim_row A' = dim_row A \<and> dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
proof (cases "find_non0 l A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
find_non0 l A = None

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None

goal (1 subgoal):
 1. dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
using rA'
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None
sub2 d l (r, A) = (r', A')

goal (1 subgoal):
 1. dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A' = dim_row A \<and> dim_col A' = dim_col A

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
case (Some m)
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = Some m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = Some m

goal (1 subgoal):
 1. dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
using rA'
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = Some m
sub2 d l (r, A) = (r', A')

goal (1 subgoal):
 1. dim_row A' = dim_row A \<and> dim_col A' = dim_col A
[PROOF STEP]
by (cases "m = l", auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
dim_row A' = dim_row A \<and> dim_col A' = dim_col A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub2_closed [simp]:
  "sub2 d l (r,A) = (r',A') \<Longrightarrow> A \<in> carrier_mat m n \<Longrightarrow> A' \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub2 d l (r, A) = (r', A'); A \<in> carrier_mat m n\<rbrakk> \<Longrightarrow> A' \<in> carrier_mat m n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub2 d l (r, A) = (r', A'); A \<in> {ma. dim_row ma = m \<and> dim_col ma = n}\<rbrakk> \<Longrightarrow> A' \<in> {ma. dim_row ma = m \<and> dim_col ma = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma sub2_preserves_triangle:
  assumes rA': "sub2 d l (r,A) = (r',A')"
  and tri: "triangular_to l A"
  and lc: "l < dim_col A"
  and ld: "l < d"
  and dr: "d \<le> dim_row A"
  shows "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
have lr: "l < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < dim_row A
[PROOF STEP]
using ld dr
[PROOF STATE]
proof (prove)
using this:
l < d
d \<le> dim_row A

goal (1 subgoal):
 1. l < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < dim_row A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
proof (cases "find_non0 l A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_to l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
find_non0 l A = None

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_to l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using rA' tri
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None
sub2 d l (r, A) = (r', A')
local.triangular_to l A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
case (Some m)
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have lm : "l < m" and mr : "m < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < m &&& m < dim_row A
[PROOF STEP]
using find_non0[OF sel_fun Some]
[PROOF STATE]
proof (prove)
using this:
A $$ (m, l) \<noteq> (0::'a)
l < m
m < dim_row A

goal (1 subgoal):
 1. l < m &&& m < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < m
m < dim_row A

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
let ?A1 = "swaprows m l A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have tri'': "triangular_to l ?A1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l (swaprows m l A)
[PROOF STEP]
proof (intro triangular_toI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
assume jl:"j < l" and ji:"j < i" and ir1: "i < dim_row ?A1"
[PROOF STATE]
proof (state)
this:
j < l
j < i
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have jm: "j < m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < m
[PROOF STEP]
using jl lm
[PROOF STATE]
proof (prove)
using this:
j < l
l < m

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have ir: "i < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
using ir1
[PROOF STATE]
proof (prove)
using this:
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_row A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have jc: "j < dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < dim_col A
[PROOF STEP]
using jl lc
[PROOF STATE]
proof (prove)
using this:
j < l
l < dim_col A

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show "?A1 $$ (i, j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (cases "m=i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
m = i

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
m = i

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = i
[PROOF STEP]
have li: "l \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
m = i

goal (1 subgoal):
 1. l \<noteq> i
[PROOF STEP]
using lm
[PROOF STATE]
proof (prove)
using this:
m = i
l < m

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

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
hence "?A1 $$ (i,j) = A $$ (l,j)"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (l, j)
[PROOF STEP]
using ir jc \<open>m=i\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i
i < dim_row A
j < dim_col A
m = i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (l, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (l, j)

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (l, j)

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (l, j) = (0::'a)
[PROOF STEP]
using tri jl lr
[PROOF STATE]
proof (prove)
using this:
local.triangular_to l A
j < l
l < dim_row A

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

goal (2 subgoals):
 1. m = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = (0::'a)

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

goal (1 subgoal):
 1. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
m \<noteq> i

goal (1 subgoal):
 1. m \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (cases "l=i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
l = i

goal (2 subgoals):
 1. l = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l = i

goal (2 subgoals):
 1. l = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = i
[PROOF STEP]
have "?A1 $$ (i,j) = A $$ (m,j)"
[PROOF STATE]
proof (prove)
using this:
l = i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (m, j)
[PROOF STEP]
using ir jc \<open>m\<noteq>i\<close>
[PROOF STATE]
proof (prove)
using this:
l = i
i < dim_row A
j < dim_col A
m \<noteq> i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (m, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (m, j)

goal (2 subgoals):
 1. l = i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
thus "?A1 $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (m, j)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
using tri jl jm mr
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (m, j)
local.triangular_to l A
j < l
j < m
m < dim_row A

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

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
l \<noteq> i

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l \<noteq> i

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> i
[PROOF STEP]
have "?A1 $$ (i,j) = A $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (i, j)
[PROOF STEP]
using ir jc \<open>m\<noteq>i\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> i
i < dim_row A
j < dim_col A
m \<noteq> i

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (i, j)

goal (1 subgoal):
 1. l \<noteq> i \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
thus "?A1 $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (i, j)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
using tri jl ji ir
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (i, j)
local.triangular_to l A
j < l
j < i
i < dim_row A

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

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.triangular_to l (swaprows m l A)

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
let ?rA3 = "sub1 (?A1 $$ (l,l)) (d - Suc l) l (-r,?A1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have [simp]: "dim_row ?A1 = dim_row A \<and> dim_col ?A1 = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (swaprows m l A) = dim_row A \<and> dim_col (swaprows m l A) = dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row (swaprows m l A) = dim_row A \<and> dim_col (swaprows m l A) = dim_col A

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have rA'2: "?rA3 = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (d - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
using rA' Some
[PROOF STATE]
proof (prove)
using this:
sub2 d l (r, A) = (r', A')
find_non0 l A = Some m

goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (d - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
sub1 (swaprows m l A $$ (l, l)) (d - Suc l) l (- r, swaprows m l A) = (r', A')

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have "l + (d - Suc l) < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l + (d - Suc l) < dim_row A
[PROOF STEP]
using ld dr
[PROOF STATE]
proof (prove)
using this:
l < d
d \<le> dim_row A

goal (1 subgoal):
 1. l + (d - Suc l) < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l + (d - Suc l) < dim_row A

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l + (d - Suc l) < dim_row A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using sub1_preserves_triangle[OF rA'2 tri''] lr lc rA'
[PROOF STATE]
proof (prove)
using this:
l + (d - Suc l) < dim_row A
\<lbrakk>l < dim_row (swaprows m l A); l < dim_col (swaprows m l A); l + (d - Suc l) < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> local.triangular_to l A'
l < dim_row A
l < dim_col A
sub2 d l (r, A) = (r', A')

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub2_grows_triangle:
  assumes mf: "mute_fun mf"
  and rA': "sub2 (dim_row A) l (r,A) = (r',A')"
  and tri: "triangular_to l A"
  and lc: "l < dim_col A"
  and lr: "l < dim_row A"
  shows "triangular_to (Suc l) A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
proof (rule triangle_growth)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.triangular_to l A'
 2. local.triangular_column l A'
[PROOF STEP]
show "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using sub2_preserves_triangle[OF rA' tri lc lr]
[PROOF STATE]
proof (prove)
using this:
dim_row A \<le> dim_row A \<Longrightarrow> local.triangular_to l A'

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
have r0: "0 < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dim_row A
[PROOF STEP]
using lr
[PROOF STATE]
proof (prove)
using this:
l < dim_row A

goal (1 subgoal):
 1. 0 < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < dim_row A

goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
show "triangular_column l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
proof (cases "find_non0 l A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
find_non0 l A = None

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_non0 l A = None

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = None
[PROOF STEP]
have "A' = A"
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None

goal (1 subgoal):
 1. A' = A
[PROOF STEP]
using rA'
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None
sub2 (dim_row A) l (r, A) = (r', A')

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

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A' = A

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
have "triangular_column l A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column l A
[PROOF STEP]
using find_non0_all0[OF None]
[PROOF STATE]
proof (prove)
using this:
local.triangular_column l A

goal (1 subgoal):
 1. local.triangular_column l A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.triangular_column l A

goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A'
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A' = A
local.triangular_column l A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A' = A
local.triangular_column l A

goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
case (Some m)
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
have lm: "l < m" and mr: "m < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < m &&& m < dim_row A
[PROOF STEP]
using find_non0[OF sel_fun Some]
[PROOF STATE]
proof (prove)
using this:
A $$ (m, l) \<noteq> (0::'a)
l < m
m < dim_row A

goal (1 subgoal):
 1. l < m &&& m < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < m
m < dim_row A

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
let ?A = "swaprows m l A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
have tri2: "triangular_to l ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l (swaprows m l A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
assume jl: "j < l" and ji:"j < i" and ir: "i < dim_row ?A"
[PROOF STATE]
proof (state)
this:
j < l
j < i
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row (swaprows m l A)\<rbrakk> \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show "?A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (cases "i = m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = m

goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i = m

goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = m
[PROOF STEP]
have "?A $$ (i,j) = A $$ (l,j)"
[PROOF STATE]
proof (prove)
using this:
i = m

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (l, j)
[PROOF STEP]
using jl lc ir
[PROOF STATE]
proof (prove)
using this:
i = m
j < l
l < dim_col A
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (l, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (l, j)

goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (l, j)

goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (l, j) = (0::'a)
[PROOF STEP]
using triangular_toD[OF tri jl jl] lr
[PROOF STATE]
proof (prove)
using this:
l < dim_row A \<Longrightarrow> A $$ (l, j) = (0::'a)
l < dim_row A

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

goal (2 subgoals):
 1. i = m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = (0::'a)

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

goal (1 subgoal):
 1. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> m

goal (1 subgoal):
 1. i \<noteq> m \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
proof (cases "i = l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = l

goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i = l

goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = l
[PROOF STEP]
have "?A $$ (i,j) = A $$ (m,j)"
[PROOF STATE]
proof (prove)
using this:
i = l

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (m, j)
[PROOF STEP]
using jl lc ir
[PROOF STATE]
proof (prove)
using this:
i = l
j < l
l < dim_col A
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (m, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (m, j)

goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (m, j)

goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (m, j) = (0::'a)
[PROOF STEP]
using triangular_toD[OF tri jl] jl lm mr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>j < ?i; ?i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (?i, j) = (0::'a)
j < l
l < m
m < dim_row A

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

goal (2 subgoals):
 1. i = l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
 2. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = (0::'a)

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

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> l
[PROOF STEP]
have "?A $$ (i,j) = A $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> l

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (i, j)
[PROOF STEP]
using \<open>i \<noteq> m\<close> jl lc ir
[PROOF STATE]
proof (prove)
using this:
i \<noteq> l
i \<noteq> m
j < l
l < dim_col A
i < dim_row (swaprows m l A)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = A $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = A $$ (i, j)

goal (1 subgoal):
 1. i \<noteq> l \<Longrightarrow> swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (i, j)

goal (1 subgoal):
 1. swaprows m l A $$ (i, j) = (0::'a)
[PROOF STEP]
using tri jl ji ir
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (i, j) = A $$ (i, j)
local.triangular_to l A
j < l
j < i
i < dim_row (swaprows m l A)

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

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.triangular_to l (swaprows m l A)

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
have rA'2: "sub1 (?A $$ (l,l)) (dim_row ?A - Suc l) l (-r, ?A) = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (dim_row (swaprows m l A) - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
using lm Some rA'
[PROOF STATE]
proof (prove)
using this:
l < m
find_non0 l A = Some m
sub2 (dim_row A) l (r, A) = (r', A')

goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (dim_row (swaprows m l A) - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
sub1 (swaprows m l A $$ (l, l)) (dim_row (swaprows m l A) - Suc l) l (- r, swaprows m l A) = (r', A')

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> local.triangular_column l A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
using sub1_triangulizes_column[OF mf rA'2 tri2] r0 lr lc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < dim_row (swaprows m l A); l < dim_row (swaprows m l A); l < dim_col (swaprows m l A)\<rbrakk> \<Longrightarrow> local.triangular_column l A'
0 < dim_row A
l < dim_row A
l < dim_col A

goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub3_preserves_dimensions[simp]:
  "sub3 d l (r,A) = (r',A') \<Longrightarrow> dim_row A' = dim_row A"
  "sub3 d l (r,A) = (r',A') \<Longrightarrow> dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A) &&& (sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A)
[PROOF STEP]
proof (induction l arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
sub3 d l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub3 d l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A

goal (4 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
obtain r' A' where rA': "sub3 d l (r, A) = (r', A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub3 d l (r, A) = (r', A')

goal (4 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
fix r'' A''
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
assume rA'': "sub3 d (Suc l) (r, A) = (r'', A'')"
[PROOF STATE]
proof (state)
this:
sub3 d (Suc l) (r, A) = (r'', A'')

goal (4 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>l r' A'. \<lbrakk>\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub3 d (Suc l) (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub3 d (Suc l) (r, A) = (r'', A'')
[PROOF STEP]
show "dim_row A'' = dim_row A" "dim_col A'' = dim_col A"
[PROOF STATE]
proof (prove)
using this:
sub3 d (Suc l) (r, A) = (r'', A'')

goal (1 subgoal):
 1. dim_row A'' = dim_row A &&& dim_col A'' = dim_col A
[PROOF STEP]
using Suc rA'
[PROOF STATE]
proof (prove)
using this:
sub3 d (Suc l) (r, A) = (r'', A'')
sub3 d l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub3 d l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A
sub3 d l (r, A) = (r', A')

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

goal (2 subgoals):
 1. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub3 d 0 (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
qed auto


[STATEMENT]
lemma sub3_closed[simp]:
  "sub3 k l (r,A) = (r',A') \<Longrightarrow> A \<in> carrier_mat m n \<Longrightarrow> A' \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub3 k l (r, A) = (r', A'); A \<in> carrier_mat m n\<rbrakk> \<Longrightarrow> A' \<in> carrier_mat m n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub3 k l (r, A) = (r', A'); A \<in> {ma. dim_row ma = m \<and> dim_col ma = n}\<rbrakk> \<Longrightarrow> A' \<in> {ma. dim_row ma = m \<and> dim_col ma = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma sub3_makes_triangle:
  assumes mf: "mute_fun mf"
  and sel_fun: "det_selection_fun sel_fun"
  and "sub3 (dim_row A) l (r,A) = (r',A')"
  and "l \<le> dim_row A"
  and "l \<le> dim_col A"
  shows "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mute_fun mf
det_selection_fun sel_fun
sub3 (dim_row A) l (r, A) = (r', A')
l \<le> dim_row A
l \<le> dim_col A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>mute_fun mf; det_selection_fun sel_fun; sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
show "sub3 (dim_row A) l (r,A) = (r',A') \<Longrightarrow> l \<le> dim_row A \<Longrightarrow> l \<le> dim_col A \<Longrightarrow>
    triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
proof (induction l arbitrary:r' A')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 (dim_row A) l (r, A) = (?r', ?A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
Suc l \<le> dim_row A
Suc l \<le> dim_col A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>sub3 (dim_row A) l (r, A) = (?r', ?A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
Suc l \<le> dim_row A
Suc l \<le> dim_col A
[PROOF STEP]
have Slr: "Suc l \<le> dim_row A" and Slc: "Suc l \<le> dim_col A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub3 (dim_row A) l (r, A) = (?r', ?A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
Suc l \<le> dim_row A
Suc l \<le> dim_col A

goal (1 subgoal):
 1. Suc l \<le> dim_row A &&& Suc l \<le> dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc l \<le> dim_row A
Suc l \<le> dim_col A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
hence lr: "l < dim_row A" and lc: "l < dim_col A"
[PROOF STATE]
proof (prove)
using this:
Suc l \<le> dim_row A
Suc l \<le> dim_col A

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

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l < dim_row A
l < dim_col A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
obtain r'' A''
        where rA'': "sub3 (dim_row A) l (r,A) = (r'',A'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'' A''. sub3 (dim_row A) l (r, A) = (r'', A'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub3 (dim_row A) l (r, A) = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l < dim_row A
l < dim_col A
sub3 (dim_row A) l (r, A) = (r'', A'')
[PROOF STEP]
have IH: "triangular_to l A''"
[PROOF STATE]
proof (prove)
using this:
l < dim_row A
l < dim_col A
sub3 (dim_row A) l (r, A) = (r'', A'')

goal (1 subgoal):
 1. local.triangular_to l A''
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
l < dim_row A
l < dim_col A
sub3 (dim_row A) l (r, A) = (r'', A'')
\<lbrakk>sub3 (dim_row A) l (r, A) = (?r', ?A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
Suc l \<le> dim_row A
Suc l \<le> dim_col A

goal (1 subgoal):
 1. local.triangular_to l A''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A''

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
have [simp]:"dim_row A'' = dim_row A" and [simp]:"dim_col A'' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A'' = dim_row A &&& dim_col A'' = dim_col A
[PROOF STEP]
using Slr Slc rA''
[PROOF STATE]
proof (prove)
using this:
Suc l \<le> dim_row A
Suc l \<le> dim_col A
sub3 (dim_row A) l (r, A) = (r'', A'')

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

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
fix r' A'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
assume "sub3 (dim_row A) (Suc l) (r, A) = (r', A')"
[PROOF STATE]
proof (state)
this:
sub3 (dim_row A) (Suc l) (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
[PROOF STEP]
have rA': "sub2 (dim_row A'') l (r'',A'') = (r',A')"
[PROOF STATE]
proof (prove)
using this:
sub3 (dim_row A) (Suc l) (r, A) = (r', A')

goal (1 subgoal):
 1. sub2 (dim_row A'') l (r'', A'') = (r', A')
[PROOF STEP]
using rA''
[PROOF STATE]
proof (prove)
using this:
sub3 (dim_row A) (Suc l) (r, A) = (r', A')
sub3 (dim_row A) l (r, A) = (r'', A'')

goal (1 subgoal):
 1. sub2 (dim_row A'') l (r'', A'') = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub2 (dim_row A'') l (r'', A'') = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
 2. \<And>l r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub3 (dim_row A) (Suc l) (r, A) = (r', A'); Suc l \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
[PROOF STEP]
show "triangular_to (Suc l) A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
using sub2_grows_triangle[OF sel_fun mf rA'] lr lc rA'' IH
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>local.triangular_to l A''; l < dim_col A''; l < dim_row A''\<rbrakk> \<Longrightarrow> local.triangular_to (Suc l) A'
l < dim_row A
l < dim_col A
sub3 (dim_row A) l (r, A) = (r'', A'')
local.triangular_to l A''

goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to (Suc l) A'

goal (1 subgoal):
 1. \<And>r' A'. \<lbrakk>sub3 (dim_row A) 0 (r, A) = (r', A'); 0 \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to 0 A'
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 (dim_row A) l (r, A) = (r', A'); l \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to l A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma triangulize_preserves_dimensions[simp]:
  "triangulize A = (r',A') \<Longrightarrow> dim_row A' = dim_row A"
  "triangulize A = (r',A') \<Longrightarrow> dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.triangulize A = (r', A') \<Longrightarrow> dim_row A' = dim_row A) &&& (local.triangulize A = (r', A') \<Longrightarrow> dim_col A' = dim_col A)
[PROOF STEP]
unfolding triangulize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A) &&& (sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A)
[PROOF STEP]
by auto


[STATEMENT]
lemma triangulize_closed[simp]:
  "triangulize A = (r',A') \<Longrightarrow> A \<in> carrier_mat m n \<Longrightarrow> A' \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.triangulize A = (r', A'); A \<in> carrier_mat m n\<rbrakk> \<Longrightarrow> A' \<in> carrier_mat m n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.triangulize A = (r', A'); A \<in> {ma. dim_row ma = m \<and> dim_col ma = n}\<rbrakk> \<Longrightarrow> A' \<in> {ma. dim_row ma = m \<and> dim_col ma = n}
[PROOF STEP]
by auto


[STATEMENT]
theorem triangulized:
  assumes "A \<in> carrier_mat n n"
  and "triangulize A = (r',A')"
  shows "upper_triangular A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular A'
[PROOF STEP]
proof (cases "0<n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> upper_triangular A'
 2. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> upper_triangular A'
 2. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
have rA': "sub3 (dim_row A) (dim_row A) (1,A) = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
local.triangulize A = (r', A')

goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')
[PROOF STEP]
unfolding triangulize_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')

goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> upper_triangular A'
 2. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
have nr:"n = dim_row A" and nc:"n = dim_col A" and nr':"n = dim_row A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = dim_row A &&& n = dim_col A &&& n = dim_row A'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
local.triangulize A = (r', A')

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

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> upper_triangular A'
 2. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = dim_row A
n = dim_col A
n = dim_row A'

goal (1 subgoal):
 1. upper_triangular A'
[PROOF STEP]
unfolding triangular_to_triangular
[PROOF STATE]
proof (prove)
using this:
n = dim_row A
n = dim_col A
n = dim_row A'

goal (1 subgoal):
 1. local.triangular_to (dim_row A') A'
[PROOF STEP]
using sub3_makes_triangle[OF mf sel_fun rA'] True
[PROOF STATE]
proof (prove)
using this:
n = dim_row A
n = dim_col A
n = dim_row A'
\<lbrakk>dim_row A \<le> dim_row A; dim_row A \<le> dim_col A\<rbrakk> \<Longrightarrow> local.triangular_to (dim_row A) A'
0 < n

goal (1 subgoal):
 1. local.triangular_to (dim_row A') A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upper_triangular A'

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 < n

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 < n
[PROOF STEP]
have nr':"dim_row A' = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n

goal (1 subgoal):
 1. dim_row A' = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < n
A \<in> carrier_mat n n
local.triangulize A = (r', A')

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

goal (1 subgoal):
 1. \<not> 0 < n \<Longrightarrow> upper_triangular A'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_row A' = 0

goal (1 subgoal):
 1. upper_triangular A'
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
dim_row A' = 0

goal (1 subgoal):
 1. \<forall>i<dim_row A'. \<forall>j<i. A' $$ (i, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upper_triangular A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_divisor [simp]:
  assumes rA': "sub1 q k l (r, A) = (r',A')"
  and r0: "r \<noteq> 0"
  and All: "q \<noteq> 0"
  and "k + l < dim_row A "
  and lc: "l < dim_col A"
  shows "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r', A')
r \<noteq> (0::'a)
q \<noteq> (0::'a)
k + l < dim_row A
l < dim_col A

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); r \<noteq> (0::'a); q \<noteq> (0::'a); k + l < dim_row A; l < dim_col A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
show "sub1 q k l (r,A) = (r',A') \<Longrightarrow> k + l < dim_row A \<Longrightarrow> r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
proof (induction k arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> ?r' \<noteq> (0::'a)
sub1 q (Suc k) l (r, A) = (r', A')
Suc k + l < dim_row A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
obtain r'' A'' where rA'': "sub1 q k l (r, A) = (r'', A'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'' A''. sub1 q k l (r, A) = (r'', A'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub1 q k l (r, A) = (r'', A'')
[PROOF STEP]
have IH: "r'' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r'', A'')

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r'', A'')
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> ?r' \<noteq> (0::'a)
sub1 q (Suc k) l (r, A) = (r', A')
Suc k + l < dim_row A

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r'' \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
obtain q' l' g where mf_id: "mf q (A'' $$ (Suc (l + k), l)) = (q',l',g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q' l' g. mf q (A'' $$ (Suc (l + k), l)) = (q', l', g) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule prod_cases3)
[PROOF STATE]
proof (state)
this:
mf q (A'' $$ (Suc (l + k), l)) = (q', l', g)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
define fact where "fact = (if A'' $$ (Suc (l+k),l) = 0 then 1 else q')"
[PROOF STATE]
proof (state)
this:
fact = (if A'' $$ (Suc (l + k), l) = (0::'a) then 1::'a else q')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
note mf = mf[unfolded mute_fun_def, rule_format, OF mf_id]
[PROOF STATE]
proof (state)
this:
A'' $$ (Suc (l + k), l) \<noteq> (0::'a) \<Longrightarrow> q = q' * g \<and> A'' $$ (Suc (l + k), l) * q' = q * l'

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
have All: "q \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<noteq> (0::'a)
[PROOF STEP]
using sub1_preserves_diagnal[OF rA'' lc] All Suc
[PROOF STATE]
proof (prove)
using this:
k + l < dim_row A \<Longrightarrow> A'' $$ (l, l) = A $$ (l, l)
q \<noteq> (0::'a)
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> ?r' \<noteq> (0::'a)
sub1 q (Suc k) l (r, A) = (r', A')
Suc k + l < dim_row A

goal (1 subgoal):
 1. q \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
have "fact \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact \<noteq> (0::'a)
[PROOF STEP]
unfolding fact_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if A'' $$ (Suc (l + k), l) = (0::'a) then 1::'a else q') \<noteq> (0::'a)
[PROOF STEP]
using All mf
[PROOF STATE]
proof (prove)
using this:
q \<noteq> (0::'a)
A'' $$ (Suc (l + k), l) \<noteq> (0::'a) \<Longrightarrow> q = q' * g \<and> A'' $$ (Suc (l + k), l) * q' = q * l'

goal (1 subgoal):
 1. (if A'' $$ (Suc (l + k), l) = (0::'a) then 1::'a else q') \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fact \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fact \<noteq> (0::'a)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
assume "sub1 q (Suc k) l (r,A) = (r',A')"
[PROOF STATE]
proof (state)
this:
sub1 q (Suc k) l (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub1 q (Suc k) l (r, A) = (r', A')
[PROOF STEP]
have "mute q (Suc (l + k)) l (r'',A'') = (r',A')"
[PROOF STATE]
proof (prove)
using this:
sub1 q (Suc k) l (r, A) = (r', A')

goal (1 subgoal):
 1. mute q (Suc (l + k)) l (r'', A'') = (r', A')
[PROOF STEP]
using rA''
[PROOF STATE]
proof (prove)
using this:
sub1 q (Suc k) l (r, A) = (r', A')
sub1 q k l (r, A) = (r'', A'')

goal (1 subgoal):
 1. mute q (Suc (l + k)) l (r'', A'') = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mute q (Suc (l + k)) l (r'', A'') = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
hence "r'' * fact = r'"
[PROOF STATE]
proof (prove)
using this:
mute q (Suc (l + k)) l (r'', A'') = (r', A')

goal (1 subgoal):
 1. r'' * fact = r'
[PROOF STEP]
unfolding mute.simps fact_def Let_def mf_id
[PROOF STATE]
proof (prove)
using this:
(if A'' $$ (Suc (l + k), l) = (0::'a) then (r'', A'') else case (q', l', g) of (q', p', g) \<Rightarrow> (r'' * q', addrow (- p') (Suc (l + k)) l (multrow (Suc (l + k)) q' A''))) = (r', A')

goal (1 subgoal):
 1. r'' * (if A'' $$ (Suc (l + k), l) = (0::'a) then 1::'a else q') = r'
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
(if A'' $$ (Suc (l + k), l) = (0::'a) then (r'', A'') else case (q', l', g) of (q', p', g) \<Rightarrow> (r'' * q', addrow (- p') (Suc (l + k)) l (multrow (Suc (l + k)) q' A''))) = (r', A')
r'' \<noteq> (0::'a)

goal (1 subgoal):
 1. r'' * (if A'' $$ (Suc (l + k), l) = (0::'a) then 1::'a else q') = r'
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
r'' * fact = r'

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a); sub1 q (Suc k) l (r, A) = (r', A'); Suc k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> (0::'a)
fact \<noteq> (0::'a)
r'' * fact = r'
[PROOF STEP]
show "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> (0::'a)
fact \<noteq> (0::'a)
r'' * fact = r'

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
q \<noteq> (0::'a)
fact \<noteq> (0::'a)
r'' * fact = r'
r'' \<noteq> (0::'a)

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); 0 + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
qed (insert r0, simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 q k l (r, A) = (r', A'); k + l < dim_row A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub2_divisor [simp]:
  assumes rA': "sub2 k l (r, A) = (r',A')"
  and lk: "l < k"
  and kr: "k \<le> dim_row A"
  and lc: "l < dim_col A"
  and r0: "r \<noteq> 0"
  shows "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub2 k l (r, A) = (r', A')
l < k
k \<le> dim_row A
l < dim_col A
r \<noteq> (0::'a)

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
proof (cases "find_non0 l A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
case (Some m)
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some m

goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = Some m
[PROOF STEP]
have Aml0: "A $$ (m,l) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = Some m

goal (1 subgoal):
 1. A $$ (m, l) \<noteq> (0::'a)
[PROOF STEP]
using find_non0[OF sel_fun]
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = Some m
find_non0 ?l ?A = Some ?m \<Longrightarrow> ?A $$ (?m, ?l) \<noteq> (0::'a)
find_non0 ?l ?A = Some ?m \<Longrightarrow> ?l < ?m
find_non0 ?l ?A = Some ?m \<Longrightarrow> ?m < dim_row ?A

goal (1 subgoal):
 1. A $$ (m, l) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (m, l) \<noteq> (0::'a)

goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
have md: "m < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < dim_row A
[PROOF STEP]
using find_non0[OF sel_fun Some] lk kr
[PROOF STATE]
proof (prove)
using this:
A $$ (m, l) \<noteq> (0::'a)
l < m
m < dim_row A
l < k
k \<le> dim_row A

goal (1 subgoal):
 1. m < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < dim_row A

goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
let ?A'' = "swaprows m l A"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
have rA'2: "sub1 (?A'' $$ (l,l)) (k - Suc l) l (-r, ?A'') = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (k - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
using rA' Some
[PROOF STATE]
proof (prove)
using this:
sub2 k l (r, A) = (r', A')
find_non0 l A = Some m

goal (1 subgoal):
 1. sub1 (swaprows m l A $$ (l, l)) (k - Suc l) l (- r, swaprows m l A) = (r', A')
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
sub1 (swaprows m l A $$ (l, l)) (k - Suc l) l (- r, swaprows m l A) = (r', A')

goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
have All0: "?A'' $$ (l,l) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A $$ (l, l) \<noteq> (0::'a)
[PROOF STEP]
using Aml0 md lk kr lc
[PROOF STATE]
proof (prove)
using this:
A $$ (m, l) \<noteq> (0::'a)
m < dim_row A
l < k
k \<le> dim_row A
l < dim_col A

goal (1 subgoal):
 1. swaprows m l A $$ (l, l) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A $$ (l, l) \<noteq> (0::'a)

goal (2 subgoals):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
 2. \<And>a. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = Some a\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using sub1_divisor[OF rA'2 _ All0] r0 lk kr lc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>- r \<noteq> (0::'a); k - Suc l + l < dim_row (swaprows m l A); l < dim_col (swaprows m l A)\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
r \<noteq> (0::'a)
l < k
k \<le> dim_row A
l < dim_col A

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
find_non0 l A = Some ?m2 \<Longrightarrow> r' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<lbrakk>sub2 k l (r, A) = (r', A'); l < k; k \<le> dim_row A; l < dim_col A; r \<noteq> (0::'a); find_non0 l A = None\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
qed auto


[STATEMENT]
lemma sub3_divisor [simp]:
  assumes "sub3 d l (r,A) = (r'',A'')"
  and "l \<le> d"
  and "d \<le> dim_row A"
  and "l \<le> dim_col A"
  and r0: "r \<noteq> 0"
  shows "r'' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r'', A'')
l \<le> d
d \<le> dim_row A
l \<le> dim_col A
r \<noteq> (0::'a)

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A; r \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
show
    "sub3 d l (r,A) = (r'',A'') \<Longrightarrow>
     l \<le> d \<Longrightarrow> d \<le> dim_row A \<Longrightarrow> l \<le> dim_col A \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
proof (induction l arbitrary: r'' A'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d; d \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
sub3 d 0 (r, A) = (r'', A'')
0 \<le> d
d \<le> dim_row A
0 \<le> dim_col A

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d; d \<le> dim_row A; 0 \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub3 d 0 (r, A) = (r'', A'')
0 \<le> d
d \<le> dim_row A
0 \<le> dim_col A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sub3 d 0 (r, A) = (r'', A'')
0 \<le> d
d \<le> dim_row A
0 \<le> dim_col A

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
using r0
[PROOF STATE]
proof (prove)
using this:
sub3 d 0 (r, A) = (r'', A'')
0 \<le> d
d \<le> dim_row A
0 \<le> dim_col A
r \<noteq> (0::'a)

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r'' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> ?r'' \<noteq> (0::'a)
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d
d \<le> dim_row A
Suc l \<le> dim_col A

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
obtain r' A' where rA': "sub3 d l (r,A) = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r' A'. sub3 d l (r, A) = (r', A') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub3 d l (r, A) = (r', A')

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub3 d l (r, A) = (r', A')
[PROOF STEP]
have [simp]:"dim_row A' = dim_row A" and [simp]:"dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r', A')

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

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
from rA'
[PROOF STATE]
proof (chain)
picking this:
sub3 d l (r, A) = (r', A')
[PROOF STEP]
have "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r', A')

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using Suc r0
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r', A')
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> ?r'' \<noteq> (0::'a)
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d
d \<le> dim_row A
Suc l \<le> dim_col A
r \<noteq> (0::'a)

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r' \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
have "sub2 d l (r',A') = (r'',A'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2 d l (r', A') = (r'', A'')
[PROOF STEP]
using rA' Suc
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r', A')
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> ?r'' \<noteq> (0::'a)
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d
d \<le> dim_row A
Suc l \<le> dim_col A

goal (1 subgoal):
 1. sub2 d l (r', A') = (r'', A'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sub2 d l (r', A') = (r'', A'')

goal (1 subgoal):
 1. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a); sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d; d \<le> dim_row A; Suc l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r' \<noteq> (0::'a)
sub2 d l (r', A') = (r'', A'')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> (0::'a)
sub2 d l (r', A') = (r'', A'')

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
using sub2_divisor
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> (0::'a)
sub2 d l (r', A') = (r'', A'')
\<lbrakk>sub2 ?k ?l (?r, ?A) = (?r', ?A'); ?l < ?k; ?k \<le> dim_row ?A; ?l < dim_col ?A; ?r \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> ?r' \<noteq> (0::'a)

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> (0::'a)
sub2 d l (r', A') = (r'', A'')
\<lbrakk>sub2 ?k ?l (?r, ?A) = (?r', ?A'); ?l < ?k; ?k \<le> dim_row ?A; ?l < dim_col ?A; ?r \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> ?r' \<noteq> (0::'a)
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> ?r'' \<noteq> (0::'a)
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d
d \<le> dim_row A
Suc l \<le> dim_col A

goal (1 subgoal):
 1. r'' \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r'' \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d; d \<le> dim_row A; l \<le> dim_col A\<rbrakk> \<Longrightarrow> r'' \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem triangulize_divisor:
  assumes A: "A \<in> carrier_mat d d"
  shows "triangulize A = (r',A') \<Longrightarrow> r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangulize A = (r', A') \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
unfolding triangulize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A') \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A') \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
assume rA': "sub3 (dim_row A) (dim_row A) (1, A) = (r', A')"
[PROOF STATE]
proof (state)
this:
sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A')

goal (1 subgoal):
 1. sub3 (dim_row A) (dim_row A) (1::'a, A) = (r', A') \<Longrightarrow> r' \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using sub3_divisor[OF rA'] A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dim_row A \<le> dim_row A; dim_row A \<le> dim_row A; dim_row A \<le> dim_col A; (1::'a) \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
A \<in> carrier_mat d d

goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r' \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mute_det:
  assumes "A \<in> carrier_mat n n"
  and rA': "mute q k l (r,A) = (r',A')"
  and "k < n"
  and "l < n"
  and "k \<noteq> l"
  shows "r * det A' = r' * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
proof (cases "A $$ (k,l) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (k, l) = (0::'a) \<Longrightarrow> r * det A' = r' * det A
 2. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (k, l) = (0::'a)

goal (2 subgoals):
 1. A $$ (k, l) = (0::'a) \<Longrightarrow> r * det A' = r' * det A
 2. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (k, l) = (0::'a)

goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A $$ (k, l) = (0::'a)
A \<in> carrier_mat n n
mute q k l (r, A) = (r', A')
k < n
l < n
k \<noteq> l

goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r * det A' = r' * det A

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A $$ (k, l) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
obtain p' q' g where mf_id: "mf q (A $$ (k,l)) = (q',p',g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q' p' g. mf q (A $$ (k, l)) = (q', p', g) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule prod_cases3)
[PROOF STATE]
proof (state)
this:
mf q (A $$ (k, l)) = (q', p', g)

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
let ?All = "q'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
let ?Akl = "- p'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
let ?B = "multrow k ?All A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
let ?C = "addrow ?Akl k l ?B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have "r * det A' = r * det ?C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * det A' = r * det (addrow (- p') k l (multrow k q' A))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
mute q k l (r, A) = (r', A')
k < n
l < n
k \<noteq> l

goal (1 subgoal):
 1. r * det A' = r * det (addrow (- p') k l (multrow k q' A))
[PROOF STEP]
by (simp add: Let_def mf_id False)
[PROOF STATE]
proof (state)
this:
r * det A' = r * det (addrow (- p') k l (multrow k q' A))

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r * det A' = r * det (addrow (- p') k l (multrow k q' A))

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have "det ?C = det ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (addrow (- p') k l (multrow k q' A)) = det (multrow k q' A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
mute q k l (r, A) = (r', A')
k < n
l < n
k \<noteq> l

goal (1 subgoal):
 1. det (addrow (- p') k l (multrow k q' A)) = det (multrow k q' A)
[PROOF STEP]
by (auto simp: det_addrow)
[PROOF STATE]
proof (state)
this:
det (addrow (- p') k l (multrow k q' A)) = det (multrow k q' A)

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (addrow (- p') k l (multrow k q' A)) = det (multrow k q' A)

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have "\<dots> = ?All * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (multrow k q' A) = q' * det A
[PROOF STEP]
using assms det_multrow
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
mute q k l (r, A) = (r', A')
k < n
l < n
k \<noteq> l
\<lbrakk>?k < ?n; ?A \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> det (multrow ?k ?a ?A) = ?a * det ?A

goal (1 subgoal):
 1. det (multrow k q' A) = q' * det A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (multrow k q' A) = q' * det A

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (multrow k q' A) = q' * det A

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have "r * \<dots> = (r * ?All) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * (q' * det A) = r * q' * det A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r * (q' * det A) = r * q' * det A

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r * (q' * det A) = r * q' * det A

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have r: "r * ?All = r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * q' = r'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
mute q k l (r, A) = (r', A')
k < n
l < n
k \<noteq> l

goal (1 subgoal):
 1. r * q' = r'
[PROOF STEP]
by (simp add: Let_def mf_id False)
[PROOF STATE]
proof (state)
this:
r * q' = r'

goal (1 subgoal):
 1. A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r * det A' = r' * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r * det A' = r' * det A

goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
r * det A' = r' * det A

goal:
No subgoals!
[PROOF STEP]
qed