[STATEMENT]
lemma sub1_det:
  assumes A: "A \<in> carrier_mat n n"
  and sub1: "sub1 q k l (r,A) = (r'',A'')"
  and r0: "r \<noteq> 0"
  and All0: "q \<noteq> 0"
  and l: "l + k < n"
  shows "r * det A'' = r'' * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * det A'' = r'' * det A
[PROOF STEP]
using sub1 l
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r'', A'')
l + k < n

goal (1 subgoal):
 1. r * det A'' = r'' * det A
[PROOF STEP]
proof (induction k arbitrary: A'' r'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A'' r''. \<lbrakk>sub1 q 0 l (r, A) = (r'', A''); l + 0 < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
sub1 q 0 l (r, A) = (r'', A'')
l + 0 < n

goal (2 subgoals):
 1. \<And>A'' r''. \<lbrakk>sub1 q 0 l (r, A) = (r'', A''); l + 0 < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub1 q 0 l (r, A) = (r'', A'')
l + 0 < n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sub1 q 0 l (r, A) = (r'', A'')
l + 0 < n

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. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 q k l (r, A) = (?r'', ?A''); l + k < n\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub1 q (Suc k) l (r, A) = (r'', A'')
l + Suc k < n

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
let ?rA' = "sub1 q k l (r,A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
obtain r' A' where rA':"?rA' = (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 (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have A':"A' \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<in> carrier_mat n n
[PROOF STEP]
using sub1_closed[OF rA'] A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat ?m ?n \<Longrightarrow> A' \<in> carrier_mat ?m ?n
A \<in> carrier_mat n n

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

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have IH: "r * det A' = r' * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
using Suc assms rA'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub1 q k l (r, A) = (?r'', ?A''); l + k < n\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub1 q (Suc k) l (r, A) = (r'', A'')
l + Suc k < n
A \<in> carrier_mat n n
sub1 q k l (r, A) = (r'', A'')
r \<noteq> (0::'a)
q \<noteq> (0::'a)
l + k < n
sub1 q k l (r, A) = (r', A')

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. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det 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 (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub1 q (Suc k) l (r, A) = (r'', A'')
[PROOF STEP]
have rA'':"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 (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
hence lem: "r' * det A'' = r'' * det A'"
[PROOF STATE]
proof (prove)
using this:
mute q (Suc (l + k)) l (r', A') = (r'', A'')

goal (1 subgoal):
 1. r' * det A'' = r'' * det A'
[PROOF STEP]
using assms Suc A' mute_det[OF A' rA'']
[PROOF STATE]
proof (prove)
using this:
mute q (Suc (l + k)) l (r', A') = (r'', A'')
A \<in> carrier_mat n n
sub1 q k l (r, A) = (r'', A'')
r \<noteq> (0::'a)
q \<noteq> (0::'a)
l + k < n
\<lbrakk>sub1 q k l (r, A) = (?r'', ?A''); l + k < n\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub1 q (Suc k) l (r, A) = (r'', A'')
l + Suc k < n
A' \<in> carrier_mat n n
\<lbrakk>Suc (l + k) < n; l < n; Suc (l + k) \<noteq> l\<rbrakk> \<Longrightarrow> r' * det A'' = r'' * det A'

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. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
hence "r * r' * det A'' = r * r'' * det A'"
[PROOF STATE]
proof (prove)
using this:
r' * det A'' = r'' * det A'

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

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r * r' * det A'' = r * r'' * det A'

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
r * det A' = r' * det A
[PROOF STEP]
have "... = r'' * r' * det A"
[PROOF STATE]
proof (prove)
using this:
r * det A' = r' * det A

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

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r * r' * det A'' = r'' * r' * det A
[PROOF STEP]
have *: "r * r' * det A'' = r'' * r' * det A"
[PROOF STATE]
proof (prove)
using this:
r * r' * det A'' = r'' * r' * det A

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

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r * r' * det A'' = r'' * r' * det A
[PROOF STEP]
have "r * r' * det A'' div r' = r'' * r' * det A div r'"
[PROOF STATE]
proof (prove)
using this:
r * r' * det A'' = r'' * r' * det A

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

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r * r' * det A'' div r' = r'' * r' * det A div r'

goal (1 subgoal):
 1. \<And>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' \<noteq> (0::'a)
[PROOF STEP]
using r0 sub1_divisor[OF rA'] All0 Suc A
[PROOF STATE]
proof (prove)
using this:
r \<noteq> (0::'a)
\<lbrakk>r \<noteq> (0::'a); q \<noteq> (0::'a); k + l < dim_row A; l < dim_col A\<rbrakk> \<Longrightarrow> r' \<noteq> (0::'a)
q \<noteq> (0::'a)
\<lbrakk>sub1 q k l (r, A) = (?r'', ?A''); l + k < n\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub1 q (Suc k) l (r, A) = (r'', A'')
l + Suc k < n
A \<in> carrier_mat n n

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>k A'' r''. \<lbrakk>\<And>A'' r''. \<lbrakk>sub1 q k l (r, A) = (r'', A''); l + k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub1 q (Suc k) l (r, A) = (r'', A''); l + Suc k < n\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r * r' * det A'' div r' = r'' * r' * det A div r'
r' \<noteq> (0::'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r * r' * det A'' div r' = r'' * r' * det A div r'
r' \<noteq> (0::'a)

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

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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub2_det:
  assumes A: "A \<in> carrier_mat d d"
  and rA': "sub2 d l (r,A) = (r',A')"
  and r0: "r \<noteq> 0"
  and ld: "l < d"
  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 "find_non0 l A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_non0 l A = None \<Longrightarrow> r * det A' = r' * det A
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det 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> r * det A' = r' * det A
 2. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det 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. r * det A' = r' * det A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None
A \<in> carrier_mat d d
sub2 d l (r, A) = (r', A')
r \<noteq> (0::'a)
l < d

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. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det 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> r * det A' = r' * det 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> r * det A' = r' * det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = Some m
[PROOF STEP]
have lm: "l < m" and md: "m < d"
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = Some m

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

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

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
hence "m \<noteq> l"
[PROOF STATE]
proof (prove)
using this:
l < m
m < d

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

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det 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> r * det A' = r' * det A
[PROOF STEP]
have rA'2: "sub1 (?A'' $$ (l,l)) (d - Suc l) l (-r, ?A'') = (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> r * det A' = r' * det A
[PROOF STEP]
have A'': "?A'' \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. swaprows m l A \<in> carrier_mat d d
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat d d

goal (1 subgoal):
 1. swaprows m l A \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
swaprows m l A \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
hence A''ll0: "?A'' $$ (l,l) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
swaprows m l A \<in> carrier_mat d d

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

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 (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
hence "-r * det A' = r' * det ?A''"
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (l, l) \<noteq> (0::'a)

goal (1 subgoal):
 1. - r * det A' = r' * det (swaprows m l A)
[PROOF STEP]
using sub1_det[OF A'' rA'2] ld A r0
[PROOF STATE]
proof (prove)
using this:
swaprows m l A $$ (l, l) \<noteq> (0::'a)
\<lbrakk>- r \<noteq> (0::'a); swaprows m l A $$ (l, l) \<noteq> (0::'a); l + (d - Suc l) < d\<rbrakk> \<Longrightarrow> - r * det A' = r' * det (swaprows m l A)
l < d
A \<in> carrier_mat d d
r \<noteq> (0::'a)

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

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- r * det A' = r' * det (swaprows m l A)

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
have "r * ... = -r * r' * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * (r' * det (swaprows m l A)) = - r * r' * det A
[PROOF STEP]
using det_swaprows[OF md ld \<open>m\<noteq>l\<close> A]
[PROOF STATE]
proof (prove)
using this:
det (swaprows m l A) = - det A

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

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r * (- r * det A') = - r * r' * det A
[PROOF STEP]
have "r * -r * det A' = -r * r' * det A"
[PROOF STATE]
proof (prove)
using this:
r * (- r * det A') = - r * r' * det A

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

goal (1 subgoal):
 1. \<And>a. find_non0 l A = Some a \<Longrightarrow> r * det A' = r' * det A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r * - r * det A' = - r * r' * det A

goal (1 subgoal):
 1. r * det A' = r' * det A
[PROOF STEP]
using r0
[PROOF STATE]
proof (prove)
using this:
r * - r * det A' = - r * r' * det A
r \<noteq> (0::'a)

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:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r * det A' = r' * det A

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. r * det A'' = r'' * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat d d; sub3 d l (r, A) = (r'', A''); r \<noteq> (0::'a); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have d: "d = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d = dim_row A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat d d

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

goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat d d; sub3 d l (r, A) = (r'', A''); r \<noteq> (0::'a); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
show "sub3 d l (r,A) = (r'',A'') \<Longrightarrow> l \<le> d \<Longrightarrow> r * det A'' = r'' * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det 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\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
let ?rA' = "sub3 d l (r,A)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
obtain r' A' where rA':"?rA' = (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 (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub3 d l (r, A) = (r', A')
[PROOF STEP]
have rA'': "sub2 d l (r',A') = (r'',A'')"
[PROOF STATE]
proof (prove)
using this:
sub3 d l (r, A) = (r', A')

goal (1 subgoal):
 1. sub2 d l (r', A') = (r'', A'')
[PROOF STEP]
using 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\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d

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

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have A': "A' \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<in> carrier_mat d d
[PROOF STEP]
using A rA' rA''
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat d d
sub3 d l (r, A) = (r', A')
sub2 d l (r', A') = (r'', A'')

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

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

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>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have "r' * det A'' = r'' * det A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r' * det A'' = r'' * det A'
[PROOF STEP]
using Suc r'0 A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub3 d l (r, A) = (?r'', ?A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det ?A'' = ?r'' * det A
sub3 d (Suc l) (r, A) = (r'', A'')
Suc l \<le> d
r' \<noteq> (0::'a)
A \<in> carrier_mat d d

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

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r' * det A'' = r'' * det A'

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have "r * ... = r'' * (r * det A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * (r'' * det A') = r'' * (r * det A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r * (r'' * det A') = r'' * (r * det A')

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r * (r'' * det A') = r'' * (r * det A')

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

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 (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r * det A' = r' * det A

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
have "r'' * ... div r' = r'' * r' * det A div r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r'' * (r' * det A) div r' = r'' * r' * det A div r'
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
r'' * (r' * det A) div r' = r'' * r' * det A div r'

goal (2 subgoals):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
 2. \<And>l r'' A''. \<lbrakk>\<And>r'' A''. \<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A; sub3 d (Suc l) (r, A) = (r'', A''); Suc l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r * (r' * det A'') div r' = r'' * r' * det A div r'
[PROOF STEP]
show "r * det A'' = r'' * det A"
[PROOF STATE]
proof (prove)
using this:
r * (r' * det A'') div r' = r'' * r' * det A div r'

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

goal (1 subgoal):
 1. r * det A'' = r'' * det A
[PROOF STEP]
by (metis \<open>r * det A' = r' * det A\<close> \<open>r' * det A'' = r'' * det A'\<close>
          mult.left_commute mult_cancel_left)
[PROOF STATE]
proof (state)
this:
r * det A'' = r'' * det A

goal (1 subgoal):
 1. \<And>r'' A''. \<lbrakk>sub3 d 0 (r, A) = (r'', A''); 0 \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub3 d l (r, A) = (r'', A''); l \<le> d\<rbrakk> \<Longrightarrow> r * det A'' = r'' * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem triangulize_det:
  assumes A: "A \<in> carrier_mat d d"
  and rA': "triangulize A = (r',A')"
  shows "det A * r' = det A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A * r' = det A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det A * r' = det A'
[PROOF STEP]
have rA'2: "sub3 d d (1,A) = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub3 d d (1::'a, A) = (r', A')
[PROOF STEP]
using A rA'
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat d d
local.triangulize A = (r', A')

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

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

goal (1 subgoal):
 1. det A * r' = det A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A * r' = det A'
[PROOF STEP]
proof (cases "d = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d = 0 \<Longrightarrow> det A * r' = det A'
 2. d \<noteq> 0 \<Longrightarrow> det A * r' = det A'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
d = 0

goal (2 subgoals):
 1. d = 0 \<Longrightarrow> det A * r' = det A'
 2. d \<noteq> 0 \<Longrightarrow> det A * r' = det A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d = 0
[PROOF STEP]
have A': "A' \<in> carrier_mat 0 0"
[PROOF STATE]
proof (prove)
using this:
d = 0

goal (1 subgoal):
 1. A' \<in> carrier_mat 0 0
[PROOF STEP]
using A rA'2
[PROOF STATE]
proof (prove)
using this:
d = 0
A \<in> carrier_mat d d
sub3 d d (1::'a, A) = (r', A')

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

goal (2 subgoals):
 1. d = 0 \<Longrightarrow> det A * r' = det A'
 2. d \<noteq> 0 \<Longrightarrow> det A * r' = det A'
[PROOF STEP]
have rA'3: "(r',A') = (1,A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r', A') = (1::'a, A)
[PROOF STEP]
using True rA'2
[PROOF STATE]
proof (prove)
using this:
d = 0
sub3 d d (1::'a, A) = (r', A')

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

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

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

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

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

goal (1 subgoal):
 1. det A * r' = det A'
[PROOF STEP]
using sub3_det[OF A rA'2] assms
[PROOF STATE]
proof (prove)
using this:
d \<noteq> 0
\<lbrakk>(1::'a) \<noteq> (0::'a); d \<le> d\<rbrakk> \<Longrightarrow> (1::'a) * det A' = r' * det A
A \<in> carrier_mat d d
local.triangulize A = (r', A')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det A * r' = det A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_code[simp]: assumes sel_fun: "det_selection_fun sel_fun"
  and mf: "mute_fun mf"
  shows "det_code A = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.det_code A = det A
[PROOF STEP]
using det_code_def[simp]
[PROOF STATE]
proof (prove)
using this:
local.det_code ?A = (if dim_row ?A = dim_col ?A then case local.triangulize ?A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a))

goal (1 subgoal):
 1. local.det_code A = det A
[PROOF STEP]
proof (cases "dim_row A = dim_col A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dim_row A = dim_col A

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dim_row A = dim_col A
[PROOF STEP]
have A: "A \<in> carrier_mat (dim_row A) (dim_row A)"
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A

goal (1 subgoal):
 1. A \<in> carrier_mat (dim_row A) (dim_row A)
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
using this:
dim_row A = dim_col A

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
obtain r' A' where rA': "triangulize A = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r' A'. local.triangulize A = (r', A') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
local.triangulize A = (r', A')

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
from triangulize_divisor[OF mf sel_fun A] rA'
[PROOF STATE]
proof (chain)
picking this:
local.triangulize A = (?r', ?A') \<Longrightarrow> ?r' \<noteq> (0::'a)
local.triangulize A = (r', A')
[PROOF STEP]
have r'0: "r' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
local.triangulize A = (?r', ?A') \<Longrightarrow> ?r' \<noteq> (0::'a)
local.triangulize A = (r', 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. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
from triangulize_det[OF mf sel_fun A rA']
[PROOF STATE]
proof (chain)
picking this:
det A * r' = det A'
[PROOF STEP]
have det': "det A * r' = det A'"
[PROOF STATE]
proof (prove)
using this:
det A * r' = det A'

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
from triangulized[OF mf sel_fun A, unfolded rA']
[PROOF STATE]
proof (chain)
picking this:
(r', A') = (?r', ?A') \<Longrightarrow> upper_triangular ?A'
[PROOF STEP]
have tri': "upper_triangular A'"
[PROOF STATE]
proof (prove)
using this:
(r', A') = (?r', ?A') \<Longrightarrow> upper_triangular ?A'

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
have A': "A' \<in> carrier_mat (dim_row A') (dim_row A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' \<in> carrier_mat (dim_row A') (dim_row A')
[PROOF STEP]
using triangulize_closed[OF rA' A]
[PROOF STATE]
proof (prove)
using this:
A' \<in> carrier_mat (dim_row A) (dim_row A)

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
from tri'
[PROOF STATE]
proof (chain)
picking this:
upper_triangular A'
[PROOF STEP]
have tr: "triangular_to (dim_row A') A'"
[PROOF STATE]
proof (prove)
using this:
upper_triangular A'

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
have "det_code A = prod_list (diag_mat A') div r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.det_code A = prod_list (diag_mat A') div r'
[PROOF STEP]
using rA' True
[PROOF STATE]
proof (prove)
using this:
local.triangulize A = (r', A')
dim_row A = dim_col A

goal (1 subgoal):
 1. local.det_code A = prod_list (diag_mat A') div r'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.det_code A = prod_list (diag_mat A') div r'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.det_code A = prod_list (diag_mat A') div r'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
have "prod_list (diag_mat A') = det A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (diag_mat A') = det A'
[PROOF STEP]
unfolding det_upper_triangular[OF tri' A']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (diag_mat A') = prod_list (diag_mat A')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
prod_list (diag_mat A') = det A'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_list (diag_mat A') = det A'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
have "\<dots> = det A * r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A' = det A * r'
[PROOF STEP]
by (simp add: det')
[PROOF STATE]
proof (state)
this:
det A' = det A * r'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det A' = det A * r'

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
have "\<dots> div r' = det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A * r' div r' = det A
[PROOF STEP]
using r'0
[PROOF STATE]
proof (prove)
using this:
r' \<noteq> (0::'a)

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

goal (2 subgoals):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A = dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
 2. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.det_code A = det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.det_code A = det A

goal (1 subgoal):
 1. local.det_code A = det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.det_code A = det A

goal (1 subgoal):
 1. \<lbrakk>\<And>A. local.det_code A = (if dim_row A = dim_col A then case local.triangulize A of (m, A') \<Rightarrow> prod_list (diag_mat A') div m else (0::'a)); dim_row A \<noteq> dim_col A\<rbrakk> \<Longrightarrow> local.det_code A = det A
[PROOF STEP]
qed (simp add: det_def)


[STATEMENT]
lemma trivial_mute_fun[simp,intro]: "mute_fun trivial_mute_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mute_fun trivial_mute_fun
[PROOF STEP]
unfolding mute_fun_def trivial_mute_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y x' y' g. (x, y, 1::'a) = (x', y', g) \<longrightarrow> y \<noteq> (0::'a) \<longrightarrow> x = x' * g \<and> y * x' = x * y'
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_sel_fun[simp]: "det_selection_fun fst_sel_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_selection_fun fst_sel_fun
[PROOF STEP]
unfolding det_selection_fun_def fst_sel_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. xs \<noteq> [] \<longrightarrow> fst (hd xs) \<in> fst ` set xs
[PROOF STEP]
by auto


[STATEMENT]
lemma select_min[simp]: "det_selection_fun select_min"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_selection_fun local.select_min
[PROOF STEP]
unfolding det_selection_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. xs \<noteq> [] \<longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
fix xs :: "(nat \<times> 'a)list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
assume "xs \<noteq> []"
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
[PROOF STEP]
obtain i p ys where xs: "xs = ((i,p) # ys)"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>i p ys. xs = (i, p) # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases xs, auto)
[PROOF STATE]
proof (state)
this:
xs = (i, p) # ys

goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xs = (i, p) # ys
[PROOF STEP]
obtain m where id: "select_min xs = select_min_main m i ys"
[PROOF STATE]
proof (prove)
using this:
xs = (i, p) # ys

goal (1 subgoal):
 1. (\<And>m. local.select_min xs = select_min_main m i ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding select_min_def
[PROOF STATE]
proof (prove)
using this:
xs = (i, p) # ys

goal (1 subgoal):
 1. (\<And>m. (case xs of (i, p) # ys \<Rightarrow> select_min_main (measure p) i ys) = select_min_main m i ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.select_min xs = select_min_main m i ys

goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
have "i \<in> fst ` set xs" "set ys \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> fst ` set xs &&& set ys \<subseteq> set xs
[PROOF STEP]
unfolding xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> fst ` set ((i, p) # ys) &&& set ys \<subseteq> set ((i, p) # ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> fst ` set xs
set ys \<subseteq> set xs

goal (1 subgoal):
 1. \<And>xs. xs \<noteq> [] \<Longrightarrow> local.select_min xs \<in> fst ` set xs
[PROOF STEP]
thus "select_min xs \<in> fst ` set xs"
[PROOF STATE]
proof (prove)
using this:
i \<in> fst ` set xs
set ys \<subseteq> set xs

goal (1 subgoal):
 1. local.select_min xs \<in> fst ` set xs
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
i \<in> fst ` set xs
set ys \<subseteq> set xs

goal (1 subgoal):
 1. select_min_main m i ys \<in> fst ` set xs
[PROOF STEP]
proof (induct ys arbitrary: m i )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m i. \<lbrakk>i \<in> fst ` set xs; set [] \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i [] \<in> fst ` set xs
 2. \<And>a ys m i. \<lbrakk>\<And>m i. \<lbrakk>i \<in> fst ` set xs; set ys \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i ys \<in> fst ` set xs; i \<in> fst ` set xs; set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i (a # ys) \<in> fst ` set xs
[PROOF STEP]
case (Cons jp ys m i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i5 \<in> fst ` set xs; set ys \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main ?m5 ?i5 ys \<in> fst ` set xs
i \<in> fst ` set xs
set (jp # ys) \<subseteq> set xs

goal (2 subgoals):
 1. \<And>m i. \<lbrakk>i \<in> fst ` set xs; set [] \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i [] \<in> fst ` set xs
 2. \<And>a ys m i. \<lbrakk>\<And>m i. \<lbrakk>i \<in> fst ` set xs; set ys \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i ys \<in> fst ` set xs; i \<in> fst ` set xs; set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i (a # ys) \<in> fst ` set xs
[PROOF STEP]
obtain j p where jp: "jp = (j,p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j p. jp = (j, p) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
jp = (j, p)

goal (2 subgoals):
 1. \<And>m i. \<lbrakk>i \<in> fst ` set xs; set [] \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i [] \<in> fst ` set xs
 2. \<And>a ys m i. \<lbrakk>\<And>m i. \<lbrakk>i \<in> fst ` set xs; set ys \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i ys \<in> fst ` set xs; i \<in> fst ` set xs; set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i (a # ys) \<in> fst ` set xs
[PROOF STEP]
obtain k n where res: "select_min_main m i (jp # ys) = select_min_main n k ys"
      and k: "k \<in> fst ` set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n k. \<lbrakk>select_min_main m i (jp # ys) = select_min_main n k ys; k \<in> fst ` set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons(2-)
[PROOF STATE]
proof (prove)
using this:
i \<in> fst ` set xs
set (jp # ys) \<subseteq> set xs

goal (1 subgoal):
 1. (\<And>n k. \<lbrakk>select_min_main m i (jp # ys) = select_min_main n k ys; k \<in> fst ` set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding jp
[PROOF STATE]
proof (prove)
using this:
i \<in> fst ` set xs
set ((j, p) # ys) \<subseteq> set xs

goal (1 subgoal):
 1. (\<And>n k. \<lbrakk>select_min_main m i ((j, p) # ys) = select_min_main n k ys; k \<in> fst ` set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "measure p < m"; force simp: Let_def)
[PROOF STATE]
proof (state)
this:
select_min_main m i (jp # ys) = select_min_main n k ys
k \<in> fst ` set xs

goal (2 subgoals):
 1. \<And>m i. \<lbrakk>i \<in> fst ` set xs; set [] \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i [] \<in> fst ` set xs
 2. \<And>a ys m i. \<lbrakk>\<And>m i. \<lbrakk>i \<in> fst ` set xs; set ys \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i ys \<in> fst ` set xs; i \<in> fst ` set xs; set (a # ys) \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i (a # ys) \<in> fst ` set xs
[PROOF STEP]
from Cons(1)[OF k, of n] Cons(3)
[PROOF STATE]
proof (chain)
picking this:
set ys \<subseteq> set xs \<Longrightarrow> select_min_main n k ys \<in> fst ` set xs
set (jp # ys) \<subseteq> set xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs \<Longrightarrow> select_min_main n k ys \<in> fst ` set xs
set (jp # ys) \<subseteq> set xs

goal (1 subgoal):
 1. select_min_main m i (jp # ys) \<in> fst ` set xs
[PROOF STEP]
unfolding res
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs \<Longrightarrow> select_min_main n k ys \<in> fst ` set xs
set (jp # ys) \<subseteq> set xs

goal (1 subgoal):
 1. select_min_main n k ys \<in> fst ` set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
select_min_main m i (jp # ys) \<in> fst ` set xs

goal (1 subgoal):
 1. \<And>m i. \<lbrakk>i \<in> fst ` set xs; set [] \<subseteq> set xs\<rbrakk> \<Longrightarrow> select_min_main m i [] \<in> fst ` set xs
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
local.select_min xs \<in> fst ` set xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_code_fst_sel_fun[code]: "det A = det_code fst_sel_fun trivial_mute_fun A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = det_code fst_sel_fun trivial_mute_fun A
[PROOF STEP]
by simp


[STATEMENT]
lemma field_mute_fun[simp,intro]: "mute_fun field_mute_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mute_fun field_mute_fun
[PROOF STEP]
unfolding mute_fun_def field_mute_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y x' y' g. (x / y, 1::'a, y) = (x', y', g) \<longrightarrow> y \<noteq> (0::'a) \<longrightarrow> x = x' * g \<and> y * x' = x * y'
[PROOF STEP]
by auto


[STATEMENT]
lemma det_field[simp]: "det_field = det"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_field = det
[PROOF STEP]
by (intro ext, auto simp: det_field_def)


[STATEMENT]
lemma gcd_mute_fun[simp,intro]: "mute_fun gcd_mute_fun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mute_fun gcd_mute_fun
[PROOF STEP]
unfolding mute_fun_def gcd_mute_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y x' y' g. (let g = gcd x y in (x div g, y div g, g)) = (x', y', g) \<longrightarrow> y \<noteq> (0::'a) \<longrightarrow> x = x' * g \<and> y * x' = x * y'
[PROOF STEP]
by (auto simp: Let_def div_mult_swap mult.commute)


[STATEMENT]
lemma det_int[simp]: "det_int = det"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_int = det
[PROOF STEP]
by (intro ext, auto simp: det_int_def)


[STATEMENT]
lemma det_field_poly[simp]: "det_field_poly = det"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_field_poly = det
[PROOF STEP]
by (intro ext, auto simp: det_field_poly_def)


[STATEMENT]
lemma sin_arcsin_abs: "\<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arcsin y) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>y\<bar> \<le> 1 \<Longrightarrow> sin (arcsin y) = y
[PROOF STEP]
by (simp add: abs_le_iff)


[STATEMENT]
lemma arccos_lbound_abs [simp]:
  "\<bar>y\<bar> \<le> 1 \<Longrightarrow> 0 \<le> arccos y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>y\<bar> \<le> 1 \<Longrightarrow> 0 \<le> arccos y
[PROOF STEP]
by (simp add: arccos_lbound)


[STATEMENT]
lemma arccos_ubound_abs [simp]:
  "\<bar>y\<bar> \<le> 1 \<Longrightarrow> arccos y \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>y\<bar> \<le> 1 \<Longrightarrow> arccos y \<le> pi
[PROOF STEP]
by (simp add: arccos_ubound)


[STATEMENT]
lemma sin_ge_zero_iff:
  assumes "0 \<le> x" "x < 2 * pi"
  shows "0 \<le> sin x \<longleftrightarrow> x \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> sin x) = (x \<le> pi)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> sin x \<Longrightarrow> x \<le> pi
 2. x \<le> pi \<Longrightarrow> 0 \<le> sin x
[PROOF STEP]
assume "0 \<le> sin x"
[PROOF STATE]
proof (state)
this:
0 \<le> sin x

goal (2 subgoals):
 1. 0 \<le> sin x \<Longrightarrow> x \<le> pi
 2. x \<le> pi \<Longrightarrow> 0 \<le> sin x
[PROOF STEP]
show "x \<le> pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> pi
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x \<le> pi \<Longrightarrow> False
[PROOF STEP]
assume "\<not> x \<le> pi"
[PROOF STATE]
proof (state)
this:
\<not> x \<le> pi

goal (1 subgoal):
 1. \<not> x \<le> pi \<Longrightarrow> False
[PROOF STEP]
from this \<open>x < 2 * pi\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> x \<le> pi
x < 2 * pi
[PROOF STEP]
have "sin x < 0"
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> pi
x < 2 * pi

goal (1 subgoal):
 1. sin x < 0
[PROOF STEP]
using sin_lt_zero
[PROOF STATE]
proof (prove)
using this:
\<not> x \<le> pi
x < 2 * pi
\<lbrakk>pi < ?x; ?x < 2 * pi\<rbrakk> \<Longrightarrow> sin ?x < 0

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

goal (1 subgoal):
 1. \<not> x \<le> pi \<Longrightarrow> False
[PROOF STEP]
from this \<open>0 \<le> sin x\<close>
[PROOF STATE]
proof (chain)
picking this:
sin x < 0
0 \<le> sin x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
sin x < 0
0 \<le> sin x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<le> pi

goal (1 subgoal):
 1. x \<le> pi \<Longrightarrow> 0 \<le> sin x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> pi \<Longrightarrow> 0 \<le> sin x
[PROOF STEP]
assume "x \<le> pi"
[PROOF STATE]
proof (state)
this:
x \<le> pi

goal (1 subgoal):
 1. x \<le> pi \<Longrightarrow> 0 \<le> sin x
[PROOF STEP]
from this \<open>0 \<le> x\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<le> pi
0 \<le> x
[PROOF STEP]
show "0 \<le> sin x"
[PROOF STATE]
proof (prove)
using this:
x \<le> pi
0 \<le> x

goal (1 subgoal):
 1. 0 \<le> sin x
[PROOF STEP]
by (simp add: sin_ge_zero)
[PROOF STATE]
proof (state)
this:
0 \<le> sin x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sin_less_zero_iff:
  assumes "0 \<le> x" "x < 2 * pi"
  shows "sin x < 0 \<longleftrightarrow> pi < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sin x < 0) = (pi < x)
[PROOF STEP]
using assms sin_ge_zero_iff
[PROOF STATE]
proof (prove)
using this:
0 \<le> x
x < 2 * pi
\<lbrakk>0 \<le> ?x; ?x < 2 * pi\<rbrakk> \<Longrightarrow> (0 \<le> sin ?x) = (?x \<le> pi)

goal (1 subgoal):
 1. (sin x < 0) = (pi < x)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma axis_nth_eq_0 [simp]:
  assumes "i \<noteq> j"
  shows "axis i x $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. axis i x $ j = (0::'b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. axis i x $ j = (0::'b)
[PROOF STEP]
unfolding axis_def
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. (\<chi>ia. if ia = i then x else (0::'b)) $ j = (0::'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_axis:
  fixes x :: real
  shows "norm (axis i x) = abs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (axis i x) = \<bar>x\<bar>
[PROOF STEP]
by (simp add: norm_eq_sqrt_inner inner_axis_axis)


[STATEMENT]
lemma norm_eq_on_real_2_vec:
  fixes x :: "real ^ 2"
  shows "norm x = sqrt ((x $ 1) ^ 2 + (x $ 2) ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm x = sqrt ((x $ 1)\<^sup>2 + (x $ 2)\<^sup>2)
[PROOF STEP]
by (simp add: norm_eq_sqrt_inner inner_vec_def UNIV_2 power2_eq_square)


[STATEMENT]
lemma dist_eq_on_real_2_vec:
  fixes a b :: "real ^ 2"
  shows "dist a b = sqrt ((a $ 1 - b $ 1) ^ 2 + (a $ 2 - b $ 2) ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a b = sqrt ((a $ 1 - b $ 1)\<^sup>2 + (a $ 2 - b $ 2)\<^sup>2)
[PROOF STEP]
unfolding dist_norm norm_eq_on_real_2_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (((a - b) $ 1)\<^sup>2 + ((a - b) $ 2)\<^sup>2) = sqrt ((a $ 1 - b $ 1)\<^sup>2 + (a $ 2 - b $ 2)\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma nth_of_radiant_1 [simp]:
  "of_radiant \<omega> $ 1 = cos \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant \<omega> $ 1 = cos \<omega>
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (axis 1 (cos \<omega>) + axis 2 (sin \<omega>)) $ 1 = cos \<omega>
[PROOF STEP]
by simp


[STATEMENT]
lemma nth_of_radiant_2 [simp]:
  "of_radiant \<omega> $ 2 = sin \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant \<omega> $ 2 = sin \<omega>
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (axis 1 (cos \<omega>) + axis 2 (sin \<omega>)) $ 2 = sin \<omega>
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_of_radiant:
  "norm (of_radiant \<omega>) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_radiant \<omega>) = 1
[PROOF STEP]
unfolding of_radiant_def norm_eq_on_real_2_vec
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (((axis 1 (cos \<omega>) + axis 2 (sin \<omega>)) $ 1)\<^sup>2 + ((axis 1 (cos \<omega>) + axis 2 (sin \<omega>)) $ 2)\<^sup>2) = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma of_radiant_plus_2pi:
  "of_radiant (\<omega> + 2 * pi) = of_radiant \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (\<omega> + 2 * pi) = of_radiant \<omega>
[PROOF STEP]
unfolding of_radiant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. axis 1 (cos (\<omega> + 2 * pi)) + axis 2 (sin (\<omega> + 2 * pi)) = axis 1 (cos \<omega>) + axis 2 (sin \<omega>)
[PROOF STEP]
by simp


[STATEMENT]
lemma of_radiant_minus_2pi:
  "of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
have "of_radiant (\<omega> - 2 * pi) = of_radiant (\<omega> - 2 * pi + 2 * pi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant (\<omega> - 2 * pi + 2 * pi)
[PROOF STEP]
by (simp only: of_radiant_plus_2pi)
[PROOF STATE]
proof (state)
this:
of_radiant (\<omega> - 2 * pi) = of_radiant (\<omega> - 2 * pi + 2 * pi)

goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_radiant (\<omega> - 2 * pi) = of_radiant (\<omega> - 2 * pi + 2 * pi)

goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
have "\<dots> = of_radiant \<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi + 2 * pi) = of_radiant \<omega>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_radiant (\<omega> - 2 * pi + 2 * pi) = of_radiant \<omega>

goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>

goal (1 subgoal):
 1. of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
of_radiant (\<omega> - 2 * pi) = of_radiant \<omega>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normalize_eq:
  "norm p *\<^sub>R normalize p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm p *\<^sub>R normalize p = p
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm p *\<^sub>R (if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) = p
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_normalize:
  "norm (normalize p) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (normalize p) = 1
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) = 1
[PROOF STEP]
by (auto simp add: norm_axis)


[STATEMENT]
lemma nth_normalize [simp]:
  "\<bar>normalize p $ i\<bar> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>normalize p $ i\<bar> \<le> 1
[PROOF STEP]
using norm_normalize component_le_norm_cart
[PROOF STATE]
proof (prove)
using this:
norm (normalize ?p) = 1
\<bar>?x $ ?i\<bar> \<le> norm ?x

goal (1 subgoal):
 1. \<bar>normalize p $ i\<bar> \<le> 1
[PROOF STEP]
by metis


[STATEMENT]
lemma normalize_square:
  "(normalize p $ 1)\<^sup>2 + (normalize p $ 2)\<^sup>2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (normalize p $ 1)\<^sup>2 + (normalize p $ 2)\<^sup>2 = 1
[PROOF STEP]
using dot_square_norm[of "normalize p"]
[PROOF STATE]
proof (prove)
using this:
normalize p \<bullet> normalize p = (norm (normalize p))\<^sup>2

goal (1 subgoal):
 1. (normalize p $ 1)\<^sup>2 + (normalize p $ 2)\<^sup>2 = 1
[PROOF STEP]
by (simp add: inner_vec_def UNIV_2 power2_eq_square norm_normalize)


[STATEMENT]
lemma nth_normalize_ge_zero_iff:
  "0 \<le> normalize p $ i \<longleftrightarrow> 0 \<le> p $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> normalize p $ i) = (0 \<le> p $ i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> normalize p $ i \<Longrightarrow> 0 \<le> p $ i
 2. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
assume "0 \<le> normalize p $ i"
[PROOF STATE]
proof (state)
this:
0 \<le> normalize p $ i

goal (2 subgoals):
 1. 0 \<le> normalize p $ i \<Longrightarrow> 0 \<le> p $ i
 2. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 \<le> normalize p $ i
[PROOF STEP]
show "0 \<le> p $ i"
[PROOF STATE]
proof (prove)
using this:
0 \<le> normalize p $ i

goal (1 subgoal):
 1. 0 \<le> p $ i
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> (if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) $ i

goal (1 subgoal):
 1. 0 \<le> p $ i
[PROOF STEP]
by (auto split: if_split_asm simp add: zero_le_divide_iff)
[PROOF STATE]
proof (state)
this:
0 \<le> p $ i

goal (1 subgoal):
 1. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
assume "0 \<le> p $ i"
[PROOF STATE]
proof (state)
this:
0 \<le> p $ i

goal (1 subgoal):
 1. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
have "0 \<le> axis 1 (1 :: real) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> axis 1 1 $ i
[PROOF STEP]
using exhaust_2[of i]
[PROOF STATE]
proof (prove)
using this:
i = 1 \<or> i = 2

goal (1 subgoal):
 1. 0 \<le> axis 1 1 $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> axis 1 1 $ i

goal (1 subgoal):
 1. 0 \<le> p $ i \<Longrightarrow> 0 \<le> normalize p $ i
[PROOF STEP]
from this \<open>0 \<le> p $ i\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> axis 1 1 $ i
0 \<le> p $ i
[PROOF STEP]
show "0 \<le> normalize p $ i"
[PROOF STATE]
proof (prove)
using this:
0 \<le> axis 1 1 $ i
0 \<le> p $ i

goal (1 subgoal):
 1. 0 \<le> normalize p $ i
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> axis 1 1 $ i
0 \<le> p $ i

goal (1 subgoal):
 1. 0 \<le> (if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> normalize p $ i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_normalize_less_zero_iff:
  "normalize p $ i < 0 \<longleftrightarrow> p $ i < 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (normalize p $ i < 0) = (p $ i < 0)
[PROOF STEP]
using nth_normalize_ge_zero_iff leD leI
[PROOF STATE]
proof (prove)
using this:
(0 \<le> normalize ?p $ ?i) = (0 \<le> ?p $ ?i)
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
\<not> ?x < ?y \<Longrightarrow> ?y \<le> ?x

goal (1 subgoal):
 1. (normalize p $ i < 0) = (p $ i < 0)
[PROOF STEP]
by metis


[STATEMENT]
lemma normalize_boundary_iff:
  "\<bar>normalize p $ 1\<bar> = 1 \<longleftrightarrow> p $ 2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<bar>normalize p $ 1\<bar> = 1) = (p $ 2 = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bar>normalize p $ 1\<bar> = 1 \<Longrightarrow> p $ 2 = 0
 2. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
assume "\<bar>normalize p $ 1\<bar> = 1"
[PROOF STATE]
proof (state)
this:
\<bar>normalize p $ 1\<bar> = 1

goal (2 subgoals):
 1. \<bar>normalize p $ 1\<bar> = 1 \<Longrightarrow> p $ 2 = 0
 2. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
have 1: "(p $ 1) ^ 2 = norm p ^ 2"
[PROOF STATE]
proof (prove)
using this:
\<bar>normalize p $ 1\<bar> = 1

goal (1 subgoal):
 1. (p $ 1)\<^sup>2 = (norm p)\<^sup>2
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
using this:
\<bar>(if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) $ 1\<bar> = 1

goal (1 subgoal):
 1. (p $ 1)\<^sup>2 = (norm p)\<^sup>2
[PROOF STEP]
by (auto split: if_split_asm simp add: power2_eq_iff)
[PROOF STATE]
proof (state)
this:
(p $ 1)\<^sup>2 = (norm p)\<^sup>2

goal (2 subgoals):
 1. \<bar>normalize p $ 1\<bar> = 1 \<Longrightarrow> p $ 2 = 0
 2. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(p $ 1)\<^sup>2 = (norm p)\<^sup>2

goal (2 subgoals):
 1. \<bar>normalize p $ 1\<bar> = 1 \<Longrightarrow> p $ 2 = 0
 2. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
have "(p $ 1) ^ 2 + (p $ 2) ^ 2 = norm p ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p $ 1)\<^sup>2 + (p $ 2)\<^sup>2 = (norm p)\<^sup>2
[PROOF STEP]
using norm_eq_on_real_2_vec
[PROOF STATE]
proof (prove)
using this:
norm ?x = sqrt ((?x $ 1)\<^sup>2 + (?x $ 2)\<^sup>2)

goal (1 subgoal):
 1. (p $ 1)\<^sup>2 + (p $ 2)\<^sup>2 = (norm p)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p $ 1)\<^sup>2 + (p $ 2)\<^sup>2 = (norm p)\<^sup>2

goal (2 subgoals):
 1. \<bar>normalize p $ 1\<bar> = 1 \<Longrightarrow> p $ 2 = 0
 2. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(p $ 1)\<^sup>2 = (norm p)\<^sup>2
(p $ 1)\<^sup>2 + (p $ 2)\<^sup>2 = (norm p)\<^sup>2
[PROOF STEP]
show "p $ 2 = 0"
[PROOF STATE]
proof (prove)
using this:
(p $ 1)\<^sup>2 = (norm p)\<^sup>2
(p $ 1)\<^sup>2 + (p $ 2)\<^sup>2 = (norm p)\<^sup>2

goal (1 subgoal):
 1. p $ 2 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p $ 2 = 0

goal (1 subgoal):
 1. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
assume "p $ 2 = 0"
[PROOF STATE]
proof (state)
this:
p $ 2 = 0

goal (1 subgoal):
 1. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p $ 2 = 0
[PROOF STEP]
have "\<bar>p $ 1\<bar> = norm p"
[PROOF STATE]
proof (prove)
using this:
p $ 2 = 0

goal (1 subgoal):
 1. \<bar>p $ 1\<bar> = norm p
[PROOF STEP]
by (auto simp add: norm_eq_on_real_2_vec)
[PROOF STATE]
proof (state)
this:
\<bar>p $ 1\<bar> = norm p

goal (1 subgoal):
 1. p $ 2 = 0 \<Longrightarrow> \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<bar>p $ 1\<bar> = norm p
[PROOF STEP]
show "\<bar>normalize p $ 1\<bar> = 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>p $ 1\<bar> = norm p

goal (1 subgoal):
 1. \<bar>normalize p $ 1\<bar> = 1
[PROOF STEP]
unfolding normalize_def
[PROOF STATE]
proof (prove)
using this:
\<bar>p $ 1\<bar> = norm p

goal (1 subgoal):
 1. \<bar>(if p = 0 then axis 1 1 else (1 / norm p) *\<^sub>R p) $ 1\<bar> = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>normalize p $ 1\<bar> = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma between_normalize_if_distant_from_0:
  assumes "norm p \<ge> 1"
  shows "between (0, p) (normalize p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. between (0, p) (normalize p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> norm p

goal (1 subgoal):
 1. between (0, p) (normalize p)
[PROOF STEP]
by (auto simp add: between_mem_segment closed_segment_def normalize_def)


[STATEMENT]
lemma between_normalize_if_near_0:
  assumes "norm p \<le> 1"
  shows "between (0, normalize p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
have "0 \<le> norm p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> norm p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> norm p

goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
norm p \<le> 1
[PROOF STEP]
have "p = (norm p / norm p) *\<^sub>R p \<and> 0 \<le> norm p \<and> norm p \<le> 1"
[PROOF STATE]
proof (prove)
using this:
norm p \<le> 1

goal (1 subgoal):
 1. p = (norm p / norm p) *\<^sub>R p \<and> 0 \<le> norm p \<and> norm p \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = (norm p / norm p) *\<^sub>R p \<and> 0 \<le> norm p \<and> norm p \<le> 1

goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p = (norm p / norm p) *\<^sub>R p \<and> 0 \<le> norm p \<and> norm p \<le> 1
[PROOF STEP]
have "\<exists>u. p = (u / norm p) *\<^sub>R p \<and> 0 \<le> u \<and> u \<le> 1"
[PROOF STATE]
proof (prove)
using this:
p = (norm p / norm p) *\<^sub>R p \<and> 0 \<le> norm p \<and> norm p \<le> 1

goal (1 subgoal):
 1. \<exists>u. p = (u / norm p) *\<^sub>R p \<and> 0 \<le> u \<and> u \<le> 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>u. p = (u / norm p) *\<^sub>R p \<and> 0 \<le> u \<and> u \<le> 1

goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. p = (u / norm p) *\<^sub>R p \<and> 0 \<le> u \<and> u \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>u. p = (u / norm p) *\<^sub>R p \<and> 0 \<le> u \<and> u \<le> 1

goal (1 subgoal):
 1. between (0, normalize p) p
[PROOF STEP]
by (auto simp add: between_mem_segment closed_segment_def normalize_def)
[PROOF STATE]
proof (state)
this:
between (0, normalize p) p

goal:
No subgoals!
[PROOF STEP]
qed