[STATEMENT]
lemma echelon_form_JNF_imp_upper_triangular:
  assumes eA: "echelon_form_JNF A" 
  shows "upper_triangular' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular' A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
assume ji: "j<i" and i: "i<dim_row A" and j: "j<dim_col A"
[PROOF STATE]
proof (state)
this:
j < i
i < dim_row A
j < dim_col A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < dim_col A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
have A: "A \<in> carrier_mat (dim_row A) (dim_col A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat (dim_row A) (dim_col A)

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

goal (2 subgoals):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<not> is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
have "i\<le> (LEAST n. A $$(i,n) \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
[PROOF STEP]
by (rule echelon_form_JNF_least_position_ge_diagonal[OF eA A False i])
[PROOF STATE]
proof (state)
this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))

goal (2 subgoals):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<not> is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using ji not_less_Least order.strict_trans2
[PROOF STATE]
proof (prove)
using this:
i \<le> (LEAST n. A $$ (i, n) \<noteq> (0::'a))
j < i
?k < (LEAST x. ?P x) \<Longrightarrow> \<not> ?P ?k
\<lbrakk>?a < ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a < ?c

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

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

goal (1 subgoal):
 1. is_zero_row_JNF i A \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_zero_row_JNF i A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row_JNF i A

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
unfolding is_zero_row_JNF_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j<dim_col A. A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
\<forall>j<dim_col A. A $$ (i, j) = (0::'a)
j < dim_col A

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

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

goal:
No subgoals!
[PROOF STEP]
qed