[STATEMENT]
lemma step_3_a_inv: "A \<in> carrier_mat n n 
  \<Longrightarrow> i < j \<Longrightarrow> j < n 
  \<Longrightarrow> inv_upto jb A j 
  \<Longrightarrow> inv_from uppert A j 
  \<Longrightarrow> inv_from_bot (\<lambda> A i. one_zero A i j) A i 
  \<Longrightarrow> ev_block n A
  \<Longrightarrow> inv_from uppert (step_3_a i j A) j 
    \<and> inv_upto jb (step_3_a i j A) j 
    \<and> inv_at one_zero (step_3_a i j A) j \<and> same_diag A (step_3_a i j A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A i; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j A) j \<and> inv_upto local.jb (step_3_a i j A) j \<and> inv_at one_zero (step_3_a i j A) j \<and> local.same_diag A (step_3_a i j A)
[PROOF STEP]
proof (induct i j A rule: step_3_a.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j A. \<lbrakk>A \<in> carrier_mat n n; 0 < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A 0; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
 2. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case (1 j A)
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n
0 < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A 0
local.ev_block n A

goal (2 subgoals):
 1. \<And>j A. \<lbrakk>A \<in> carrier_mat n n; 0 < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A 0; local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
 2. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
0 < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A 0
local.ev_block n A

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)
[PROOF STEP]
by (simp add: inv_from_bot_def inv_at_def)
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a 0 j A) j \<and> inv_upto local.jb (step_3_a 0 j A) j \<and> inv_at one_zero (step_3_a 0 j A) j \<and> local.same_diag A (step_3_a 0 j A)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case (2 i j A)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = A $$ (i, j); ?xa = (if A $$ (i, i + 1) = (1::'a) \<and> ?x \<noteq> (0::'a) then add_col_sub_row (- ?x) (Suc i) j A else A); ?xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb ?xa j; inv_from local.uppert ?xa j; inv_from_bot (\<lambda>A i. one_zero A i j) ?xa i; local.ev_block n ?xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j ?xa) j \<and> inv_upto local.jb (step_3_a i j ?xa) j \<and> inv_at one_zero (step_3_a i j ?xa) j \<and> local.same_diag ?xa (step_3_a i j ?xa)
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from 2(2-)
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A
[PROOF STEP]
have A: "A \<in> carrier_mat n n" and ij: "Suc i < j" "i < j" and j: "j < n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

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

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?cond = "A $$ (i, i + 1) = 1 \<and> A $$ (i, j) \<noteq> 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?B = "add_col_sub_row (- A $$ (i, j)) (Suc i) j A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
obtain B where B: "B = (if ?cond then ?B else A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. B = (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have Bn: "B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. B \<in> carrier_mat n n
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat n n

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note IH = 2(1)[OF refl B Bn ij(2) j]
[PROOF STATE]
proof (state)
this:
\<lbrakk>inv_upto local.jb B j; inv_from local.uppert B j; inv_from_bot (\<lambda>A i. one_zero A i j) B i; local.ev_block n B\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have id: "step_3_a (Suc i) j A = step_3_a i j B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_3_a (Suc i) j A = step_3_a i j B
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_3_a (Suc i) j A = step_3_a i j (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A)
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
step_3_a (Suc i) j A = step_3_a i j B

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from ij j
[PROOF STATE]
proof (chain)
picking this:
Suc i < j
i < j
j < n
[PROOF STEP]
have *: "Suc i < n" "j < n" "Suc i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
Suc i < j
i < j
j < n

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

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from 2(2-)
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A
[PROOF STEP]
have inv: "inv_upto jb A j" "inv_from uppert A j" "ev_block n A"
    "inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < j
j < n
inv_upto local.jb A j
inv_from local.uppert A j
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
local.ev_block n A

goal (1 subgoal):
 1. (inv_upto local.jb A j &&& inv_from local.uppert A j) &&& local.ev_block n A &&& inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv_upto local.jb A j
inv_from local.uppert A j
local.ev_block n A
inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note evbA = ev_blockD[OF inv(3)]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> A $$ (?i, ?i) = A $$ (?j, ?j)

goal (1 subgoal):
 1. \<And>i j A. \<lbrakk>\<And>x xa. \<lbrakk>x = A $$ (i, j); xa = (if A $$ (i, i + 1) = (1::'a) \<and> x \<noteq> (0::'a) then add_col_sub_row (- x) (Suc i) j A else A); xa \<in> carrier_mat n n; i < j; j < n; inv_upto local.jb xa j; inv_from local.uppert xa j; inv_from_bot (\<lambda>A i. one_zero A i j) xa i; local.ev_block n xa\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a i j xa) j \<and> inv_upto local.jb (step_3_a i j xa) j \<and> inv_at one_zero (step_3_a i j xa) j \<and> local.same_diag xa (step_3_a i j xa); A \<in> carrier_mat n n; Suc i < j; j < n; inv_upto local.jb A j; inv_from local.uppert A j; inv_from_bot (\<lambda>A i. one_zero A i j) A (Suc i); local.ev_block n A\<rbrakk> \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
proof (cases ?cond)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
hence B: "B = A"
[PROOF STATE]
proof (prove)
using this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (1 subgoal):
 1. B = A
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
\<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a))

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = A

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have inv2: "inv_from_bot (\<lambda>A i. one_zero A i j) A i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from_bot (\<lambda>A i. one_zero A i j) A i
[PROOF STEP]
by (rule inv_from_bot_step[OF _ inv(4)],
      insert False ij evbA[of i j] *, auto simp: one_zero_def)
[PROOF STATE]
proof (state)
this:
inv_from_bot (\<lambda>A i. one_zero A i j) A i

goal (2 subgoals):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
 2. \<not> (A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
unfolding id B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from local.uppert (step_3_a i j A) j \<and> inv_upto local.jb (step_3_a i j A) j \<and> inv_at one_zero (step_3_a i j A) j \<and> local.same_diag A (step_3_a i j A)
[PROOF STEP]
by (rule IH[unfolded B], insert inv inv2, auto)
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
hence B: "B = ?B"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a)

goal (1 subgoal):
 1. (if A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) then add_col_sub_row (- A $$ (i, j)) (Suc i) j A else A) = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
let ?C = "step_3_a i j B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from inv_uptoD[OF inv(1) j *(1) ij(1), unfolded jb_def] ij
[PROOF STATE]
proof (chain)
picking this:
(Suc j = Suc i \<longrightarrow> A $$ (j, Suc i) \<in> {0::'a, 1::'a}) \<and> (j \<noteq> Suc i \<longrightarrow> Suc j \<noteq> Suc i \<or> A $$ (j, j) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (j, Suc i) = (0::'a))
Suc i < j
i < j
[PROOF STEP]
have Aji: "A $$ (j, Suc i) = 0"
[PROOF STATE]
proof (prove)
using this:
(Suc j = Suc i \<longrightarrow> A $$ (j, Suc i) \<in> {0::'a, 1::'a}) \<and> (j \<noteq> Suc i \<longrightarrow> Suc j \<noteq> Suc i \<or> A $$ (j, j) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (j, Suc i) = (0::'a))
Suc i < j
i < j

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

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have diag: "same_diag A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.same_diag A B
[PROOF STEP]
unfolding same_diag_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. A $$ (i, i) = B $$ (i, i)
[PROOF STEP]
by (intro allI impI, insert ij j A Aji B, auto)
[PROOF STATE]
proof (state)
this:
local.same_diag A B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have upto: "same_upto j A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_upto j A B
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. same_upto j A (add_col_sub_row (- A $$ (i, j)) (Suc i) j A)
[PROOF STEP]
by (rule add_col_sub_row_same_upto[OF \<open>Suc i < j\<close> \<open>j < n\<close> A inv_upto_mono[OF jb_imp_uppert inv(1)]])
[PROOF STATE]
proof (state)
this:
same_upto j A B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from add_col_sub_row_inv_from_uppert[OF inv(2) A \<open>Suc i < n\<close> \<open>Suc i < j\<close> \<open>j < n\<close>]
[PROOF STATE]
proof (chain)
picking this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j
[PROOF STEP]
have from_j: "inv_from uppert B j"
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j

goal (1 subgoal):
 1. inv_from local.uppert B j
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (add_col_sub_row ?v (Suc i) j A) j

goal (1 subgoal):
 1. inv_from local.uppert (add_col_sub_row (- A $$ (i, j)) (Suc i) j A) j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_from local.uppert B j

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have ev: "A $$ (Suc i, Suc i) = A $$ (j,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (Suc i, Suc i) = A $$ (j, j)
[PROOF STEP]
using evbA[of "Suc i" j] ij j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc i < n; j < n\<rbrakk> \<Longrightarrow> A $$ (Suc i, Suc i) = A $$ (j, j)
Suc i < j
i < j
j < n

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

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have evb_B: "ev_block n B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.ev_block n B
[PROOF STEP]
by (rule same_diag_ev_block[OF diag inv(3)])
[PROOF STATE]
proof (state)
this:
local.ev_block n B

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note evbB = ev_blockD[OF evb_B]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> B $$ (?i, ?i) = B $$ (?j, ?j)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < n; ?j < n\<rbrakk> \<Longrightarrow> B $$ (?i, ?i) = B $$ (?j, ?j)

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
assume "k < n"
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
with A *
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
Suc i < n
j < n
Suc i \<noteq> j
k < n
[PROOF STEP]
have k: "k < dim_row A" "k < dim_col A" "j < dim_row A" "j < dim_col A" "j < dim_row A"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n
Suc i < n
j < n
Suc i \<noteq> j
k < n

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

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note id = B add_col_sub_index_row[OF k]
[PROOF STATE]
proof (state)
this:
B = add_col_sub_row (- A $$ (i, j)) (Suc i) j A
add_col_sub_row ?a ?k j A $$ (k, j) = (if k = ?k \<and> j = j then A $$ (k, j) + ?a * A $$ (k, k) - ?a * ?a * A $$ (j, k) - ?a * A $$ (j, j) else if k = ?k \<and> j \<noteq> j then A $$ (k, j) - ?a * A $$ (j, j) else if k \<noteq> ?k \<and> j = j then A $$ (k, j) + ?a * A $$ (k, ?k) else A $$ (k, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have "B $$ (k,j) = (if k = i then 0 else A $$ (k,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $$ (k, j) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k = Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, k) - - A $$ (i, j) * - A $$ (i, j) * A $$ (j, k) - - A $$ (i, j) * A $$ (j, j) else if k = Suc i \<and> j \<noteq> j then A $$ (k, j) - - A $$ (i, j) * A $$ (j, j) else if k \<noteq> Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, Suc i) else A $$ (k, j)) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
using inv_uptoD[OF inv(1), of k "Suc i", unfolded jb_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k < n; Suc i < n; Suc i < j\<rbrakk> \<Longrightarrow> (Suc k = Suc i \<longrightarrow> A $$ (k, Suc i) \<in> {0::'a, 1::'a}) \<and> (k \<noteq> Suc i \<longrightarrow> Suc k \<noteq> Suc i \<or> A $$ (k, k) \<noteq> A $$ (Suc i, Suc i) \<longrightarrow> A $$ (k, Suc i) = (0::'a))

goal (1 subgoal):
 1. (if k = Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, k) - - A $$ (i, j) * - A $$ (i, j) * A $$ (j, k) - - A $$ (i, j) * A $$ (j, j) else if k = Suc i \<and> j \<noteq> j then A $$ (k, j) - - A $$ (i, j) * A $$ (j, j) else if k \<noteq> Suc i \<and> j = j then A $$ (k, j) + - A $$ (i, j) * A $$ (k, Suc i) else A $$ (k, j)) = (if k = i then 0::'a else A $$ (k, j))
[PROOF STEP]
by (insert * Aji True ij \<open>k < n\<close>, auto simp: ev)
[PROOF STATE]
proof (state)
this:
B $$ (k, j) = (if k = i then 0::'a else A $$ (k, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> B $$ (?k2, j) = (if ?k2 = i then 0::'a else A $$ (?k2, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
note id2 = this
[PROOF STATE]
proof (state)
this:
?k2 < n \<Longrightarrow> B $$ (?k2, j) = (if ?k2 = i then 0::'a else A $$ (?k2, j))

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
have "inv_from_bot (\<lambda>A i. one_zero A i j) B i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_from_bot (\<lambda>A i. one_zero A i j) B i
[PROOF STEP]
unfolding inv_from_bot_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<ge>i. i < n \<longrightarrow> one_zero B i j
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
assume "i \<le> k" "k < n"
[PROOF STATE]
proof (state)
this:
i \<le> k
k < n

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> i; i < n\<rbrakk> \<Longrightarrow> one_zero B i j
[PROOF STEP]
thus "one_zero B k j"
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n

goal (1 subgoal):
 1. one_zero B k j
[PROOF STEP]
using inv(4)[unfolded inv_from_bot_def]
        upto[unfolded same_upto_def] evbB[OF \<open>k < n\<close> \<open>j < n\<close>]
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n
\<forall>i\<ge>Suc i. i < n \<longrightarrow> one_zero A i j
\<forall>i' j'. i' < n \<longrightarrow> j' < j \<longrightarrow> A $$ (i', j') = B $$ (i', j')
B $$ (k, k) = B $$ (j, j)

goal (1 subgoal):
 1. one_zero B k j
[PROOF STEP]
unfolding one_zero_def id2[OF \<open>k < n\<close>]
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k < n
\<forall>i\<ge>Suc i. i < n \<longrightarrow> (Suc i < j \<longrightarrow> A $$ (i, Suc i) = (1::'a) \<longrightarrow> A $$ (i, j) = (0::'a)) \<and> (j < i \<longrightarrow> A $$ (i, j) = (0::'a)) \<and> (i < j \<longrightarrow> A $$ (i, i) \<noteq> A $$ (j, j) \<longrightarrow> A $$ (i, j) = (0::'a))
\<forall>i' j'. i' < n \<longrightarrow> j' < j \<longrightarrow> A $$ (i', j') = B $$ (i', j')
B $$ (k, k) = B $$ (j, j)

goal (1 subgoal):
 1. (Suc k < j \<longrightarrow> B $$ (k, Suc k) = (1::'a) \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a)) \<and> (j < k \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a)) \<and> (k < j \<longrightarrow> B $$ (k, k) \<noteq> B $$ (j, j) \<longrightarrow> (if k = i then 0::'a else A $$ (k, j)) = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_zero B k j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_from_bot (\<lambda>A i. one_zero A i j) B i

goal (1 subgoal):
 1. A $$ (i, i + 1) = (1::'a) \<and> A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
from IH[OF same_upto_inv_upto_jb[OF upto inv(1)] from_j this evb_B]
      same_diag_trans[OF diag]
[PROOF STATE]
proof (chain)
picking this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag B (step_3_a i j B)
local.same_diag B ?C \<Longrightarrow> local.same_diag A ?C

goal (1 subgoal):
 1. inv_from local.uppert (step_3_a i j B) j \<and> inv_upto local.jb (step_3_a i j B) j \<and> inv_at one_zero (step_3_a i j B) j \<and> local.same_diag A (step_3_a i j B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inv_from local.uppert (step_3_a (Suc i) j A) j \<and> inv_upto local.jb (step_3_a (Suc i) j A) j \<and> inv_at one_zero (step_3_a (Suc i) j A) j \<and> local.same_diag A (step_3_a (Suc i) j A)

goal:
No subgoals!
[PROOF STEP]
qed