[STATEMENT]
lemma gauss_jordan_main_row_echelon:
  assumes
    "A \<in> carrier_mat nr nc"
    "gauss_jordan_main A B i j = (A',B')"
    "pivot_fun A f j"
    "\<And> i'. i' < i \<Longrightarrow> f i' < j" "\<And> i'. i' \<ge> i \<Longrightarrow> f i' = j"
    "i \<le> nr" "j \<le> nc"
  shows "row_echelon_form A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
interpret m: ring "ring_mat TYPE('a) nr b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (ring_mat TYPE('a) nr b)
[PROOF STEP]
by (rule ring_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc
gauss_jordan_main A B i j = (A', B')
pivot_fun A f j
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
i \<le> nr
j \<le> nc

goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
proof (induct A B i j arbitrary: f rule: gauss_jordan_main.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
case (1 A B i j f)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = dim_row A; ?xa = dim_col A; i < ?x \<and> j < ?xa; ?xaa = A $$ (i, j); ?xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<?x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A ?f (Suc j); \<And>i'. i' < i \<Longrightarrow> ?f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>?x = dim_row A; ?xa = dim_col A; i < ?x \<and> j < ?xa; ?xaa = A $$ (i, j); ?xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<?x]) = ?x21.0 # ?x22.0; swaprows i ?x21.0 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B'); pivot_fun (swaprows i ?x21.0 A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>?x = dim_row A; ?xa = dim_col A; i < ?x \<and> j < ?xa; ?xaa = A $$ (i, j); ?xaa \<noteq> (0::'a); ?xaa = (1::'a); ?xb = (\<lambda>i. A $$ (i, j)); eliminate_entries ?xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries ?xb A i j) (eliminate_entries ?xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries ?xb A i j) ?f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> ?f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> ?f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>?x = dim_row A; ?xa = dim_col A; i < ?x \<and> j < ?xa; ?xaa = A $$ (i, j); ?xaa \<noteq> (0::'a); ?xaa \<noteq> (1::'a); ?xb = inverse ?xaa; multrow i ?xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B'); pivot_fun (multrow i ?xb A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
A \<in> carrier_mat nr nc
gauss_jordan_main A B i j = (A', B')
pivot_fun A f j
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
i \<le> nr
j \<le> nc

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note A = 1(5)
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
hence dim: "dim_row A = nr" "dim_col A = nc"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

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

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note res = 1(6)
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note pivot = 1(7)
[PROOF STATE]
proof (state)
this:
pivot_fun A f j

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note f = 1(8-9)
[PROOF STATE]
proof (state)
this:
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note ij = 1(10-11)
[PROOF STATE]
proof (state)
this:
i \<le> nr
j \<le> nc

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = 1(1-4)[OF dim[symmetric]]
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr \<and> j < nc; ?xaa = A $$ (i, j); ?xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A ?f (Suc j); \<And>i'. i' < i \<Longrightarrow> ?f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>i < nr \<and> j < nc; ?xaa = A $$ (i, j); ?xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = ?x21.0 # ?x22.0; swaprows i ?x21.0 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B'); pivot_fun (swaprows i ?x21.0 A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>i < nr \<and> j < nc; ?xaa = A $$ (i, j); ?xaa \<noteq> (0::'a); ?xaa = (1::'a); ?xb = (\<lambda>i. A $$ (i, j)); eliminate_entries ?xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries ?xb A i j) (eliminate_entries ?xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries ?xb A i j) ?f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> ?f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> ?f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>i < nr \<and> j < nc; ?xaa = A $$ (i, j); ?xaa \<noteq> (0::'a); ?xaa \<noteq> (1::'a); ?xb = inverse ?xaa; multrow i ?xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B'); pivot_fun (multrow i ?xb A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note simp = gauss_jordan_main.simps[of A B i j] Let_def
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B i j = (let nr = dim_row A; nc = dim_col A in if i < nr \<and> j < nc then let aij = A $$ (i, j) in if aij = (0::'a) then case concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if aij = (1::'a) then let v = \<lambda>i. A $$ (i, j) in gauss_jordan_main (eliminate_entries v A i j) (eliminate_entries v B i j) (Suc i) (Suc j) else let iaij = inverse aij in gauss_jordan_main (multrow i iaij A) (multrow i iaij B) i j else (A, B))
Let ?s ?f \<equiv> ?f ?s

goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?g = "gauss_jordan_main A B i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B i j f. \<lbrakk>\<And>x xa xaa f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A f (Suc j); \<And>i'. i' < i \<Longrightarrow> f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa x21 x22 f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<x]) = x21 # x22; swaprows i x21 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B'); pivot_fun (swaprows i x21 A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa = (1::'a); xb = (\<lambda>i. A $$ (i, j)); eliminate_entries xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries xb A i j) (eliminate_entries xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries xb A i j) f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; \<And>x xa xaa xb f. \<lbrakk>x = dim_row A; xa = dim_col A; i < x \<and> j < xa; xaa = A $$ (i, j); xaa \<noteq> (0::'a); xaa \<noteq> (1::'a); xb = inverse xaa; multrow i xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B'); pivot_fun (multrow i xb A) f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'; A \<in> carrier_mat nr nc; gauss_jordan_main A B i j = (A', B'); pivot_fun A f j; \<And>i'. i' < i \<Longrightarrow> f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
proof (cases "i < nr \<and> j < nc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (i < nr \<and> j < nc)

goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note nij = this
[PROOF STATE]
proof (state)
this:
\<not> (i < nr \<and> j < nc)

goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
gauss_jordan_main A B i j = (A', B')
\<not> (i < nr \<and> j < nc)
[PROOF STEP]
have id: "A' = A"
[PROOF STATE]
proof (prove)
using this:
gauss_jordan_main A B i j = (A', B')
\<not> (i < nr \<and> j < nc)

goal (1 subgoal):
 1. A' = A
[PROOF STEP]
unfolding simp dim
[PROOF STATE]
proof (prove)
using this:
(if i < nr \<and> j < nc then if A $$ (i, j) = (0::'a) then case concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if A $$ (i, j) = (1::'a) then gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) else gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j else (A, B)) = (A', B')
\<not> (i < nr \<and> j < nc)

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

goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "pivot_fun A f nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun A f nc
[PROOF STEP]
proof (cases "j \<ge> nc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nc \<le> j \<Longrightarrow> pivot_fun A f nc
 2. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
nc \<le> j

goal (2 subgoals):
 1. nc \<le> j \<Longrightarrow> pivot_fun A f nc
 2. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
with ij
[PROOF STATE]
proof (chain)
picking this:
i \<le> nr
j \<le> nc
nc \<le> j
[PROOF STEP]
have j: "j = nc"
[PROOF STATE]
proof (prove)
using this:
i \<le> nr
j \<le> nc
nc \<le> j

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

goal (2 subgoals):
 1. nc \<le> j \<Longrightarrow> pivot_fun A f nc
 2. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
with pivot
[PROOF STATE]
proof (chain)
picking this:
pivot_fun A f j
j = nc
[PROOF STEP]
show "pivot_fun A f nc"
[PROOF STATE]
proof (prove)
using this:
pivot_fun A f j
j = nc

goal (1 subgoal):
 1. pivot_fun A f nc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pivot_fun A f nc

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> nc \<le> j

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
hence j: "j < nc"
[PROOF STATE]
proof (prove)
using this:
\<not> nc \<le> j

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

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
from False nij ij
[PROOF STATE]
proof (chain)
picking this:
\<not> nc \<le> j
\<not> (i < nr \<and> j < nc)
i \<le> nr
j \<le> nc
[PROOF STEP]
have i: "i = nr"
[PROOF STATE]
proof (prove)
using this:
\<not> nc \<le> j
\<not> (i < nr \<and> j < nc)
i \<le> nr
j \<le> nc

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

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
note f = f[unfolded i]
[PROOF STATE]
proof (state)
this:
?i' < nr \<Longrightarrow> f ?i' < j
nr \<le> ?i' \<Longrightarrow> f ?i' = j

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
note p = pivot_funD[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> j
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = j
\<lbrakk>?i < nr; f ?i < j\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < j; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. \<not> nc \<le> j \<Longrightarrow> pivot_fun A f nc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun A f nc
[PROOF STEP]
proof (rule pivot_funI[OF dim(1)])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> nc
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 4. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> nc
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 4. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
assume i: "i < nr"
[PROOF STATE]
proof (state)
this:
i < nr

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> nc
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 4. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
note p = p[OF i]
[PROOF STATE]
proof (state)
this:
f i \<le> j
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)
Suc i < nr \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = j
f i < j \<Longrightarrow> A $$ (i, f i) = (1::'a)
\<lbrakk>f i < j; ?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> f i \<le> nc
 2. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 4. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
from p(1) j
[PROOF STATE]
proof (chain)
picking this:
f i \<le> j
j < nc
[PROOF STEP]
show "f i \<le> nc"
[PROOF STATE]
proof (prove)
using this:
f i \<le> j
j < nc

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

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 3. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
from f(1)[OF i]
[PROOF STATE]
proof (chain)
picking this:
f i < j
[PROOF STEP]
have fij: "f i < j"
[PROOF STATE]
proof (prove)
using this:
f i < j

goal (1 subgoal):
 1. f i < j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f i < j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 3. \<And>i. \<lbrakk>i < nr; f i < nc\<rbrakk> \<Longrightarrow> A $$ (i, f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
from p(4)[OF fij]
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, f i) = (1::'a)
[PROOF STEP]
show "A $$ (i, f i) = 1"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, f i) = (1::'a)

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

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
 3. \<And>i i'. \<lbrakk>i < nr; f i < nc; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
from p(5)[OF fij]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)
[PROOF STEP]
show "\<And> i'. i' < nr \<Longrightarrow> i' \<noteq> i \<Longrightarrow> A $$ (i', f i) = 0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (1 subgoal):
 1. \<And>i'. \<lbrakk>i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', f i) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i' < nr; ?i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (?i', f i) = (0::'a)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < f i\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
[PROOF STEP]
show "\<And> j. j < f i \<Longrightarrow> A $$ (i, j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < f i \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
by (rule p(2))
[PROOF STATE]
proof (state)
this:
?j < f i \<Longrightarrow> A $$ (i, ?j) = (0::'a)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
[PROOF STEP]
assume "Suc i < nr"
[PROOF STATE]
proof (state)
this:
Suc i < nr

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> f i < f (Suc i) \<or> f (Suc i) = nc
[PROOF STEP]
with p(3)[OF this] f
[PROOF STATE]
proof (chain)
picking this:
f i < f (Suc i) \<or> f (Suc i) = j
?i' < nr \<Longrightarrow> f ?i' < j
nr \<le> ?i' \<Longrightarrow> f ?i' = j
Suc i < nr
[PROOF STEP]
show "f i < f (Suc i) \<or> f (Suc i) = nc"
[PROOF STATE]
proof (prove)
using this:
f i < f (Suc i) \<or> f (Suc i) = j
?i' < nr \<Longrightarrow> f ?i' < j
nr \<le> ?i' \<Longrightarrow> f ?i' = j
Suc i < nr

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun A f nc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun A f nc

goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pivot_fun A f nc

goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
using pivot
[PROOF STATE]
proof (prove)
using this:
pivot_fun A f nc
pivot_fun A f j

goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
unfolding id row_echelon_form_def dim
[PROOF STATE]
proof (prove)
using this:
pivot_fun A f nc
pivot_fun A f j

goal (1 subgoal):
 1. \<exists>f. pivot_fun A f nc
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < nr \<and> j < nc

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note valid = this
[PROOF STATE]
proof (state)
this:
i < nr \<and> j < nc

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
hence sij: "Suc i \<le> nr" "Suc j \<le> nc"
[PROOF STATE]
proof (prove)
using this:
i < nr \<and> j < nc

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

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH[OF valid refl]
[PROOF STATE]
proof (state)
this:
\<lbrakk>A $$ (i, j) = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A ?f (Suc j); \<And>i'. i' < i \<Longrightarrow> ?f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>A $$ (i, j) = (0::'a); concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = ?x21.0 # ?x22.0; swaprows i ?x21.0 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B'); pivot_fun (swaprows i ?x21.0 A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>A $$ (i, j) \<noteq> (0::'a); A $$ (i, j) = (1::'a); ?xb = (\<lambda>i. A $$ (i, j)); eliminate_entries ?xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries ?xb A i j) (eliminate_entries ?xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries ?xb A i j) ?f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> ?f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> ?f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>A $$ (i, j) \<noteq> (0::'a); A $$ (i, j) \<noteq> (1::'a); ?xb = inverse (A $$ (i, j)); multrow i ?xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B'); pivot_fun (multrow i ?xb A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'

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

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

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(3-4)[OF nZ]
[PROOF STATE]
proof (state)
this:
\<lbrakk>A $$ (i, j) = (1::'a); ?xb = (\<lambda>i. A $$ (i, j)); eliminate_entries ?xb A i j \<in> carrier_mat nr nc; gauss_jordan_main (eliminate_entries ?xb A i j) (eliminate_entries ?xb B i j) (Suc i) (Suc j) = (A', B'); pivot_fun (eliminate_entries ?xb A i j) ?f (Suc j); \<And>i'. i' < Suc i \<Longrightarrow> ?f i' < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> ?f i' = Suc j; Suc i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>A $$ (i, j) \<noteq> (1::'a); ?xb = inverse (A $$ (i, j)); multrow i ?xb A \<in> carrier_mat nr nc; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B'); pivot_fun (multrow i ?xb A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'

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

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note nO = this
[PROOF STATE]
proof (state)
this:
A $$ (i, j) \<noteq> (1::'a)

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?inv = "inverse (A $$ (i,j))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?A = "multrow i ?inv A"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from nO nZ valid res
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) \<noteq> (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')
[PROOF STEP]
have id: "gauss_jordan_main (multrow i ?inv A) (multrow i ?inv B) i j = (A', B')"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) \<noteq> (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j = (A', B')
[PROOF STEP]
unfolding simp dim
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) \<noteq> (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
(if i < nr \<and> j < nc then if A $$ (i, j) = (0::'a) then case concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if A $$ (i, j) = (1::'a) then gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) else gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j else (A, B)) = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j = (A', B')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j = (A', B')

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "pivot_fun ?A f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (multrow i (inverse (A $$ (i, j))) A) f j
[PROOF STEP]
by (rule pivot_fun_multrow[OF pivot dim f(2) ij(2)], auto)
[PROOF STATE]
proof (state)
this:
pivot_fun (multrow i (inverse (A $$ (i, j))) A) f j

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(2)[OF nO refl, unfolded multrow_carrier, OF A id this f ij]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i'. i' < i \<Longrightarrow> i' < i; \<And>i'. i \<le> i' \<Longrightarrow> i \<le> i'\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i'. i' < i \<Longrightarrow> i' < i; \<And>i'. i \<le> i' \<Longrightarrow> i \<le> i'\<rbrakk> \<Longrightarrow> row_echelon_form A'

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

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

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note O = this
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (1::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?E = "\<lambda> B. eliminate_entries (\<lambda> i. A $$ (i,j)) B i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?A = "?E A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?B = "?E B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
define E where "E = ?A"
[PROOF STATE]
proof (state)
this:
E = eliminate_entries (\<lambda>i. A $$ (i, j)) A i j

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?f = "\<lambda> i'. if i' = i then j else if i' > i then Suc j else f i'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have pivot: "pivot_fun E f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun E f j
[PROOF STEP]
unfolding E_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) f j
[PROOF STEP]
by (rule pivot_fun_eliminate_entries[OF pivot dim f(2)], insert valid, auto)
[PROOF STATE]
proof (state)
this:
pivot_fun E f j

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
pivot_fun E f j

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
assume i': "i' < nr"
[PROOF STATE]
proof (state)
this:
i' < nr

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "E $$ (i', j) = (if i' = i then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E $$ (i', j) = (if i' = i then 1::'a else (0::'a))
[PROOF STEP]
unfolding E_def eliminate_entries_gen_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (dim_row A) (dim_col A) (\<lambda>(i, j). if i \<noteq> i then A $$ (i, j) - A $$ (i, j) * A $$ (i, j) else A $$ (i, j)) $$ (i', j) = (if i' = i then 1::'a else (0::'a))
[PROOF STEP]
using dim O i' valid
[PROOF STATE]
proof (prove)
using this:
dim_row A = nr
dim_col A = nc
A $$ (i, j) = (1::'a)
i' < nr
i < nr \<and> j < nc

goal (1 subgoal):
 1. mat (dim_row A) (dim_col A) (\<lambda>(i, j). if i \<noteq> i then A $$ (i, j) - A $$ (i, j) * A $$ (i, j) else A $$ (i, j)) $$ (i', j) = (if i' = i then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E $$ (i', j) = (if i' = i then 1::'a else (0::'a))

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i'2 < nr \<Longrightarrow> E $$ (?i'2, j) = (if ?i'2 = i then 1::'a else (0::'a))

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note Ej = this
[PROOF STATE]
proof (state)
this:
?i'2 < nr \<Longrightarrow> E $$ (?i'2, j) = (if ?i'2 = i then 1::'a else (0::'a))

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have E: "E \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<in> carrier_mat nr nc
[PROOF STEP]
unfolding E_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) A i j \<in> carrier_mat nr nc
[PROOF STEP]
by (rule carrier_eliminate_entries[OF A])
[PROOF STATE]
proof (state)
this:
E \<in> carrier_mat nr nc

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
hence dimE: "dim_row E = nr" "dim_col E = nc"
[PROOF STATE]
proof (prove)
using this:
E \<in> carrier_mat nr nc

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

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note pivot = pivot_funD[OF dimE(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> j
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> E $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = j
\<lbrakk>?i < nr; f ?i < j\<rbrakk> \<Longrightarrow> E $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < j; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> E $$ (?i', f ?i) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "pivot_fun E ?f (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun E (\<lambda>i'. if i' = i then j else if i < i' then Suc j else f i') (Suc j)
[PROOF STEP]
proof (rule pivot_funI[OF dimE(1)])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
fix ii
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
assume ii: "ii < nr"
[PROOF STATE]
proof (state)
this:
ii < nr

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
note p = pivot[OF ii]
[PROOF STATE]
proof (state)
this:
f ii \<le> j
?j < f ii \<Longrightarrow> E $$ (ii, ?j) = (0::'a)
Suc ii < nr \<Longrightarrow> f ii < f (Suc ii) \<or> f (Suc ii) = j
f ii < j \<Longrightarrow> E $$ (ii, f ii) = (1::'a)
\<lbrakk>f ii < j; ?i' < nr; ?i' \<noteq> ii\<rbrakk> \<Longrightarrow> E $$ (?i', f ii) = (0::'a)

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
show "?f ii \<le> Suc j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ii = i then j else if i < ii then Suc j else f ii) \<le> Suc j
[PROOF STEP]
using p(1)
[PROOF STATE]
proof (prove)
using this:
f ii \<le> j

goal (1 subgoal):
 1. (if ii = i then j else if i < ii then Suc j else f ii) \<le> Suc j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) \<le> Suc j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) \<le> Suc j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
fix jj
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
assume jj: "jj < ?f ii"
[PROOF STATE]
proof (state)
this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i = i then j else if i < i then Suc j else f i)\<rbrakk> \<Longrightarrow> E $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
show "E $$ (ii,jj) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
proof (cases "ii < i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ii < i

goal (2 subgoals):
 1. ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
ii < i
[PROOF STEP]
have "jj < f ii"
[PROOF STATE]
proof (prove)
using this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
ii < i

goal (1 subgoal):
 1. jj < f ii
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
jj < f ii

goal (2 subgoals):
 1. ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
from p(2)[OF this]
[PROOF STATE]
proof (chain)
picking this:
E $$ (ii, jj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E $$ (ii, jj) = (0::'a)

goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ii < i

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
note ge = this
[PROOF STATE]
proof (state)
this:
\<not> ii < i

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
\<not> ii < i
[PROOF STEP]
have fiij: "f ii = j"
[PROOF STATE]
proof (prove)
using this:
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
\<not> ii < i

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

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
proof (cases "i < ii")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < ii

goal (2 subgoals):
 1. i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
i < ii
[PROOF STEP]
have jj: "jj \<le> j"
[PROOF STATE]
proof (prove)
using this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
i < ii

goal (1 subgoal):
 1. jj \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
jj \<le> j

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

goal (2 subgoals):
 1. jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
 2. \<not> jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with p(2)[of jj] fiij
[PROOF STATE]
proof (chain)
picking this:
jj < f ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
f ii = j
jj < j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
jj < f ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
f ii = j
jj < j

goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal (1 subgoal):
 1. \<not> jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> jj < j

goal (1 subgoal):
 1. \<not> jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj \<le> j
\<not> jj < j
[PROOF STEP]
have jj: "jj = j"
[PROOF STATE]
proof (prove)
using this:
jj \<le> j
\<not> jj < j

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

goal (1 subgoal):
 1. \<not> jj < j \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with Ej[OF ii] True
[PROOF STATE]
proof (chain)
picking this:
E $$ (ii, j) = (if ii = i then 1::'a else (0::'a))
i < ii
jj = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E $$ (ii, j) = (if ii = i then 1::'a else (0::'a))
i < ii
jj = j

goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal (1 subgoal):
 1. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < ii

goal (1 subgoal):
 1. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with ge
[PROOF STATE]
proof (chain)
picking this:
\<not> ii < i
\<not> i < ii
[PROOF STEP]
have ii: "ii = i"
[PROOF STATE]
proof (prove)
using this:
\<not> ii < i
\<not> i < ii

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

goal (1 subgoal):
 1. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
ii = i
[PROOF STEP]
have jj: "jj < j"
[PROOF STATE]
proof (prove)
using this:
jj < (if ii = i then j else if i < ii then Suc j else f ii)
ii = i

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

goal (1 subgoal):
 1. \<not> i < ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
[PROOF STEP]
from p(2)[of jj] ii jj fiij
[PROOF STATE]
proof (chain)
picking this:
jj < f ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
ii = i
jj < j
f ii = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
jj < f ii \<Longrightarrow> E $$ (ii, jj) = (0::'a)
ii = i
jj < j
f ii = j

goal (1 subgoal):
 1. E $$ (ii, jj) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E $$ (ii, jj) = (0::'a)

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?jj2 < (if ii = i then j else if i < ii then Suc j else f ii) \<Longrightarrow> E $$ (ii, ?jj2) = (0::'a)

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?jj2 < (if ii = i then j else if i < ii then Suc j else f ii) \<Longrightarrow> E $$ (ii, ?jj2) = (0::'a)

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
assume "Suc ii < nr"
[PROOF STATE]
proof (state)
this:
Suc ii < nr

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i = i then j else if i < i then Suc j else f i) < (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) \<or> (if Suc i = i then j else if i < Suc i then Suc j else f (Suc i)) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
from p(3)[OF this] f
[PROOF STATE]
proof (chain)
picking this:
f ii < f (Suc ii) \<or> f (Suc ii) = j
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
[PROOF STEP]
show "?f (Suc ii) > ?f ii \<or> ?f (Suc ii) = Suc j"
[PROOF STATE]
proof (prove)
using this:
f ii < f (Suc ii) \<or> f (Suc ii) = j
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j

goal (1 subgoal):
 1. (if ii = i then j else if i < ii then Suc j else f ii) < (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) \<or> (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) = Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) < (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) \<or> (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Suc ii < nr \<Longrightarrow> (if ii = i then j else if i < ii then Suc j else f ii) < (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) \<or> (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc ii < nr \<Longrightarrow> (if ii = i then j else if i < ii then Suc j else f ii) < (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) \<or> (if Suc ii = i then j else if i < Suc ii then Suc j else f (Suc ii)) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
assume fii: "?f ii < Suc j"
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j\<rbrakk> \<Longrightarrow> E $$ (i, if i = i then j else if i < i then Suc j else f i) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
show "E $$ (ii, ?f ii) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
proof (cases "ii = i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ii = i

goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
with Ej[of i] valid
[PROOF STATE]
proof (chain)
picking this:
i < nr \<Longrightarrow> E $$ (i, j) = (if i = i then 1::'a else (0::'a))
i < nr \<and> j < nc
ii = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i < nr \<Longrightarrow> E $$ (i, j) = (if i = i then 1::'a else (0::'a))
i < nr \<and> j < nc
ii = i

goal (1 subgoal):
 1. E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)

goal (1 subgoal):
 1. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ii \<noteq> i

goal (1 subgoal):
 1. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
with fii
[PROOF STATE]
proof (chain)
picking this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j
ii \<noteq> i
[PROOF STEP]
have ii: "ii < i"
[PROOF STATE]
proof (prove)
using this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j
ii \<noteq> i

goal (1 subgoal):
 1. ii < i
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
ii < i

goal (1 subgoal):
 1. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
from f(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
f ii < j
[PROOF STEP]
have "f ii < j"
[PROOF STATE]
proof (prove)
using this:
f ii < j

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

goal (1 subgoal):
 1. ii \<noteq> i \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
from p(4)[OF this] ii
[PROOF STATE]
proof (chain)
picking this:
E $$ (ii, f ii) = (1::'a)
ii < i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E $$ (ii, f ii) = (1::'a)
ii < i

goal (1 subgoal):
 1. E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j \<Longrightarrow> E $$ (ii, if ii = i then j else if i < ii then Suc j else f ii) = (1::'a)

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
assume *: "?f ii < Suc j" "i' < nr" "i' \<noteq> ii"
[PROOF STATE]
proof (state)
this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j
i' < nr
i' \<noteq> ii

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i = i then j else if i < i then Suc j else f i) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> E $$ (i', if i = i then j else if i < i then Suc j else f i) = (0::'a)
[PROOF STEP]
show "E $$ (i', ?f ii) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
proof (cases "ii = i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ii \<noteq> i

goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
with *(1)
[PROOF STATE]
proof (chain)
picking this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j
ii \<noteq> i
[PROOF STEP]
have iii: "ii < i"
[PROOF STATE]
proof (prove)
using this:
(if ii = i then j else if i < ii then Suc j else f ii) < Suc j
ii \<noteq> i

goal (1 subgoal):
 1. ii < i
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
ii < i

goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
from f(1)[OF this]
[PROOF STATE]
proof (chain)
picking this:
f ii < j
[PROOF STEP]
have "f ii < j"
[PROOF STATE]
proof (prove)
using this:
f ii < j

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

goal (2 subgoals):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
 2. ii \<noteq> i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
from p(5)[OF this *(2-3)]
[PROOF STATE]
proof (chain)
picking this:
E $$ (i', f ii) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E $$ (i', f ii) = (0::'a)

goal (1 subgoal):
 1. E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
using iii
[PROOF STATE]
proof (prove)
using this:
E $$ (i', f ii) = (0::'a)
ii < i

goal (1 subgoal):
 1. E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)

goal (1 subgoal):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ii = i

goal (1 subgoal):
 1. ii = i \<Longrightarrow> E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)
[PROOF STEP]
with *(2-3) Ej[of i']
[PROOF STATE]
proof (chain)
picking this:
i' < nr
i' \<noteq> ii
i' < nr \<Longrightarrow> E $$ (i', j) = (if i' = i then 1::'a else (0::'a))
ii = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i' < nr
i' \<noteq> ii
i' < nr \<Longrightarrow> E $$ (i', j) = (if i' = i then 1::'a else (0::'a))
ii = i

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
E $$ (i', if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(if ii = i then j else if i < ii then Suc j else f ii) < Suc j; ?i'2 < nr; ?i'2 \<noteq> ii\<rbrakk> \<Longrightarrow> E $$ (?i'2, if ii = i then j else if i < ii then Suc j else f ii) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun E (\<lambda>i'. if i' = i then j else if i < i' then Suc j else f i') (Suc j)

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(1)[OF O refl, folded E_def, OF E _ this _ _ sij]
[PROOF STATE]
proof (state)
this:
\<lbrakk>gauss_jordan_main E (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) = (A', B'); \<And>i'. i' < Suc i \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from O nZ valid res
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')
[PROOF STEP]
have "gauss_jordan_main E ?B (Suc i) (Suc j) = (A', B')"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main E (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) = (A', B')
[PROOF STEP]
unfolding E_def simp dim
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (1::'a)
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
(if i < nr \<and> j < nc then if A $$ (i, j) = (0::'a) then case concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if A $$ (i, j) = (1::'a) then gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) else gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j else (A, B)) = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) = (A', B')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_jordan_main E (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) = (A', B')

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH[OF this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i'. i' < Suc i \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') < Suc j; \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
proof (rule IH)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i'. i' < Suc i \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') < Suc j
 2. \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i'. i' < Suc i \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') < Suc j
 2. \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j
[PROOF STEP]
assume "i' < Suc i"
[PROOF STATE]
proof (state)
this:
i' < Suc i

goal (2 subgoals):
 1. \<And>i'. i' < Suc i \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') < Suc j
 2. \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j
[PROOF STEP]
thus "?f i' < Suc j"
[PROOF STATE]
proof (prove)
using this:
i' < Suc i

goal (1 subgoal):
 1. (if i' = i then j else if i < i' then Suc j else f i') < Suc j
[PROOF STEP]
using f[of i']
[PROOF STATE]
proof (prove)
using this:
i' < Suc i
i' < i \<Longrightarrow> f i' < j
i \<le> i' \<Longrightarrow> f i' = j

goal (1 subgoal):
 1. (if i' = i then j else if i < i' then Suc j else f i') < Suc j
[PROOF STEP]
by (cases "i' < i", auto)
[PROOF STATE]
proof (state)
this:
(if i' = i then j else if i < i' then Suc j else f i') < Suc j

goal (1 subgoal):
 1. \<And>i'. Suc i \<le> i' \<Longrightarrow> (if i' = i then j else if i < i' then Suc j else f i') = Suc j
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

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

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

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(1-2)[OF Z]
[PROOF STATE]
proof (state)
this:
\<lbrakk>concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = []; A \<in> carrier_mat nr nc; gauss_jordan_main A B i (Suc j) = (A', B'); pivot_fun A ?f (Suc j); \<And>i'. i' < i \<Longrightarrow> ?f i' < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = Suc j; i \<le> nr; Suc j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'
\<lbrakk>concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = ?x21.0 # ?x22.0; swaprows i ?x21.0 A \<in> carrier_mat nr nc; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B'); pivot_fun (swaprows i ?x21.0 A) ?f j; \<And>i'. i' < i \<Longrightarrow> ?f i' < j; \<And>i'. i \<le> i' \<Longrightarrow> ?f i' = j; i \<le> nr; j \<le> nc\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?is = "[ i' . i' <- [Suc i ..< nr],  A $$ (i',j) \<noteq> 0]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
proof (cases ?is)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = []

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = []

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
assume "i \<le> i'" and "i' < nr"
[PROOF STATE]
proof (state)
this:
i \<le> i'
i' < nr

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
hence "i' = i \<or> i' \<in> {Suc i ..< nr}"
[PROOF STATE]
proof (prove)
using this:
i \<le> i'
i' < nr

goal (1 subgoal):
 1. i' = i \<or> i' \<in> {Suc i..<nr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' = i \<or> i' \<in> {Suc i..<nr}

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from this arg_cong[OF Nil, of set] Z
[PROOF STATE]
proof (chain)
picking this:
i' = i \<or> i' \<in> {Suc i..<nr}
set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr])) = set []
A $$ (i, j) = (0::'a)
[PROOF STEP]
have "A $$ (i',j) = 0"
[PROOF STATE]
proof (prove)
using this:
i' = i \<or> i' \<in> {Suc i..<nr}
set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr])) = set []
A $$ (i, j) = (0::'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 (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> A $$ (?i'2, j) = (0::'a)

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note zero = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> ?i'2; ?i'2 < nr\<rbrakk> \<Longrightarrow> A $$ (?i'2, j) = (0::'a)

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?f = "\<lambda> i'. if i' < i then f i' else Suc j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note p = pivot_funD[OF dim(1) pivot]
[PROOF STATE]
proof (state)
this:
?i < nr \<Longrightarrow> f ?i \<le> j
\<lbrakk>?i < nr; ?j < f ?i\<rbrakk> \<Longrightarrow> A $$ (?i, ?j) = (0::'a)
\<lbrakk>?i < nr; Suc ?i < nr\<rbrakk> \<Longrightarrow> f ?i < f (Suc ?i) \<or> f (Suc ?i) = j
\<lbrakk>?i < nr; f ?i < j\<rbrakk> \<Longrightarrow> A $$ (?i, f ?i) = (1::'a)
\<lbrakk>?i < nr; f ?i < j; ?i' < nr; ?i' \<noteq> ?i\<rbrakk> \<Longrightarrow> A $$ (?i', f ?i) = (0::'a)

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "pivot_fun A ?f (Suc j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun A (\<lambda>i'. if i' < i then f i' else Suc j) (Suc j)
[PROOF STEP]
proof (rule pivot_funI[OF dim(1)])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i < i then f i else Suc j) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
fix ii
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i < i then f i else Suc j) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
assume ii: "ii < nr"
[PROOF STATE]
proof (state)
this:
ii < nr

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i < i then f i else Suc j) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
note p = p[OF this]
[PROOF STATE]
proof (state)
this:
f ii \<le> j
?j < f ii \<Longrightarrow> A $$ (ii, ?j) = (0::'a)
Suc ii < nr \<Longrightarrow> f ii < f (Suc ii) \<or> f (Suc ii) = j
f ii < j \<Longrightarrow> A $$ (ii, f ii) = (1::'a)
\<lbrakk>f ii < j; ?i' < nr; ?i' \<noteq> ii\<rbrakk> \<Longrightarrow> A $$ (?i', f ii) = (0::'a)

goal (5 subgoals):
 1. \<And>i. i < nr \<Longrightarrow> (if i < i then f i else Suc j) \<le> Suc j
 2. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 3. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 4. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 5. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
show "?f ii \<le> Suc j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ii < i then f ii else Suc j) \<le> Suc j
[PROOF STEP]
using p(1)
[PROOF STATE]
proof (prove)
using this:
f ii \<le> j

goal (1 subgoal):
 1. (if ii < i then f ii else Suc j) \<le> Suc j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if ii < i then f ii else Suc j) \<le> Suc j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(if ii < i then f ii else Suc j) \<le> Suc j

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
fix jj
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
assume jj: "jj < ?f ii"
[PROOF STATE]
proof (state)
this:
jj < (if ii < i then f ii else Suc j)

goal (4 subgoals):
 1. \<And>i j. \<lbrakk>i < nr; j < (if i < i then f i else Suc j)\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
 2. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 3. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 4. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
show "A $$ (ii,jj) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (ii, jj) = (0::'a)
[PROOF STEP]
proof (cases "ii < i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ii < i

goal (2 subgoals):
 1. ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj < (if ii < i then f ii else Suc j)
ii < i
[PROOF STEP]
have "jj < f ii"
[PROOF STATE]
proof (prove)
using this:
jj < (if ii < i then f ii else Suc j)
ii < i

goal (1 subgoal):
 1. jj < f ii
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
jj < f ii

goal (2 subgoals):
 1. ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
 2. \<not> ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
from p(2)[OF this]
[PROOF STATE]
proof (chain)
picking this:
A $$ (ii, jj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (ii, jj) = (0::'a)

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

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

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jj
[PROOF STATE]
proof (chain)
picking this:
jj < (if ii < i then f ii else Suc j)
\<not> ii < i
[PROOF STEP]
have ii': "ii \<ge> i" and jjj: "jj \<le> j"
[PROOF STATE]
proof (prove)
using this:
jj < (if ii < i then f ii else Suc j)
\<not> ii < i

goal (1 subgoal):
 1. i \<le> ii &&& jj \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> ii
jj \<le> j

goal (1 subgoal):
 1. \<not> ii < i \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
from zero[OF ii' ii]
[PROOF STATE]
proof (chain)
picking this:
A $$ (ii, j) = (0::'a)
[PROOF STEP]
have Az: "A $$ (ii,j) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (ii, j) = (0::'a)

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

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

goal (2 subgoals):
 1. jj < j \<Longrightarrow> A $$ (ii, jj) = (0::'a)
 2. \<not> jj < j \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
with jjj
[PROOF STATE]
proof (chain)
picking this:
jj \<le> j
\<not> jj < j
[PROOF STEP]
have "jj = j"
[PROOF STATE]
proof (prove)
using this:
jj \<le> j
\<not> jj < j

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

goal (2 subgoals):
 1. jj < j \<Longrightarrow> A $$ (ii, jj) = (0::'a)
 2. \<not> jj < j \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
with Az
[PROOF STATE]
proof (chain)
picking this:
A $$ (ii, j) = (0::'a)
jj = j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (ii, j) = (0::'a)
jj = j

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

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

goal (1 subgoal):
 1. jj < j \<Longrightarrow> A $$ (ii, jj) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (ii, jj) = (0::'a)
[PROOF STEP]
by (rule p(2), insert True False f, auto)
[PROOF STATE]
proof (state)
this:
A $$ (ii, jj) = (0::'a)

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

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

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?jj2 < (if ii < i then f ii else Suc j) \<Longrightarrow> A $$ (ii, ?jj2) = (0::'a)

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?jj2 < (if ii < i then f ii else Suc j) \<Longrightarrow> A $$ (ii, ?jj2) = (0::'a)

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
assume sii: "Suc ii < nr"
[PROOF STATE]
proof (state)
this:
Suc ii < nr

goal (3 subgoals):
 1. \<And>i. \<lbrakk>i < nr; Suc i < nr\<rbrakk> \<Longrightarrow> (if i < i then f i else Suc j) < (if Suc i < i then f (Suc i) else Suc j) \<or> (if Suc i < i then f (Suc i) else Suc j) = Suc j
 2. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 3. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
show "?f ii < ?f (Suc ii) \<or> ?f (Suc ii) = Suc j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ii < i then f ii else Suc j) < (if Suc ii < i then f (Suc ii) else Suc j) \<or> (if Suc ii < i then f (Suc ii) else Suc j) = Suc j
[PROOF STEP]
using p(3)[OF sii] f
[PROOF STATE]
proof (prove)
using this:
f ii < f (Suc ii) \<or> f (Suc ii) = j
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j

goal (1 subgoal):
 1. (if ii < i then f ii else Suc j) < (if Suc ii < i then f (Suc ii) else Suc j) \<or> (if Suc ii < i then f (Suc ii) else Suc j) = Suc j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if ii < i then f ii else Suc j) < (if Suc ii < i then f (Suc ii) else Suc j) \<or> (if Suc ii < i then f (Suc ii) else Suc j) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Suc ii < nr \<Longrightarrow> (if ii < i then f ii else Suc j) < (if Suc ii < i then f (Suc ii) else Suc j) \<or> (if Suc ii < i then f (Suc ii) else Suc j) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc ii < nr \<Longrightarrow> (if ii < i then f ii else Suc j) < (if Suc ii < i then f (Suc ii) else Suc j) \<or> (if Suc ii < i then f (Suc ii) else Suc j) = Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
assume fii: "?f ii < Suc j"
[PROOF STATE]
proof (state)
this:
(if ii < i then f ii else Suc j) < Suc j

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j\<rbrakk> \<Longrightarrow> A $$ (i, if i < i then f i else Suc j) = (1::'a)
 2. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
thus "A $$ (ii, ?f ii) = 1"
[PROOF STATE]
proof (prove)
using this:
(if ii < i then f ii else Suc j) < Suc j

goal (1 subgoal):
 1. A $$ (ii, if ii < i then f ii else Suc j) = (1::'a)
[PROOF STEP]
using p(4) f
[PROOF STATE]
proof (prove)
using this:
(if ii < i then f ii else Suc j) < Suc j
f ii < j \<Longrightarrow> A $$ (ii, f ii) = (1::'a)
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j

goal (1 subgoal):
 1. A $$ (ii, if ii < i then f ii else Suc j) = (1::'a)
[PROOF STEP]
by (cases "ii < i", auto)
[PROOF STATE]
proof (state)
this:
A $$ (ii, if ii < i then f ii else Suc j) = (1::'a)

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
fix i'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
assume "i' < nr" "i' \<noteq> ii"
[PROOF STATE]
proof (state)
this:
i' < nr
i' \<noteq> ii

goal (1 subgoal):
 1. \<And>i i'. \<lbrakk>i < nr; (if i < i then f i else Suc j) < Suc j; i' < nr; i' \<noteq> i\<rbrakk> \<Longrightarrow> A $$ (i', if i < i then f i else Suc j) = (0::'a)
[PROOF STEP]
from p(5)[OF _ this] f fii
[PROOF STATE]
proof (chain)
picking this:
f ii < j \<Longrightarrow> A $$ (i', f ii) = (0::'a)
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
(if ii < i then f ii else Suc j) < Suc j
[PROOF STEP]
show "A $$ (i', ?f ii) = 0"
[PROOF STATE]
proof (prove)
using this:
f ii < j \<Longrightarrow> A $$ (i', f ii) = (0::'a)
?i' < i \<Longrightarrow> f ?i' < j
i \<le> ?i' \<Longrightarrow> f ?i' = j
(if ii < i then f ii else Suc j) < Suc j

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

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(if ii < i then f ii else Suc j) < Suc j; ?i'2 < nr; ?i'2 \<noteq> ii\<rbrakk> \<Longrightarrow> A $$ (?i'2, if ii < i then f ii else Suc j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pivot_fun A (\<lambda>i'. if i' < i then f i' else Suc j) (Suc j)

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(1)[OF Nil A _ this _ _ ij(1) sij(2)]
[PROOF STATE]
proof (state)
this:
\<lbrakk>gauss_jordan_main A B i (Suc j) = (A', B'); \<And>i'. i' < i \<Longrightarrow> (if i' < i then f i' else Suc j) < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> (if i' < i then f i' else Suc j) = Suc j\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from Z valid res
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')
[PROOF STEP]
have "gauss_jordan_main A B i (Suc j) = (A',B')"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main A B i (Suc j) = (A', B')
[PROOF STEP]
unfolding simp dim Nil
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
(if i < nr \<and> j < nc then if A $$ (i, j) = (0::'a) then case [] of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if A $$ (i, j) = (1::'a) then gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) else gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j else (A, B)) = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main A B i (Suc j) = (A', B')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B i (Suc j) = (A', B')

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH[OF this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i'. i' < i \<Longrightarrow> (if i' < i then f i' else Suc j) < Suc j; \<And>i'. i \<le> i' \<Longrightarrow> (if i' < i then f i' else Suc j) = Suc j\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (2 subgoals):
 1. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = [] \<Longrightarrow> row_echelon_form A'
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
by (rule IH, insert f, force+)
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
case (Cons i' iis)
[PROOF STATE]
proof (state)
this:
concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = i' # iis

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from arg_cong[OF this, of set]
[PROOF STATE]
proof (chain)
picking this:
set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr])) = set (i' # iis)
[PROOF STEP]
have i': "i' \<ge> Suc i" "i' < nr"
[PROOF STATE]
proof (prove)
using this:
set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr])) = set (i' # iis)

goal (1 subgoal):
 1. Suc i \<le> i' &&& i' < nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc i \<le> i'
i' < nr

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from f[of i] f[of "i'"] i'
[PROOF STATE]
proof (chain)
picking this:
i < i \<Longrightarrow> f i < j
i \<le> i \<Longrightarrow> f i = j
i' < i \<Longrightarrow> f i' < j
i \<le> i' \<Longrightarrow> f i' = j
Suc i \<le> i'
i' < nr
[PROOF STEP]
have fij: "f i = j" "f i' = j"
[PROOF STATE]
proof (prove)
using this:
i < i \<Longrightarrow> f i < j
i \<le> i \<Longrightarrow> f i = j
i' < i \<Longrightarrow> f i' < j
i \<le> i' \<Longrightarrow> f i' = j
Suc i \<le> i'
i' < nr

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

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?A = "swaprows i i' A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
let ?B = "swaprows i i' B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
have "pivot_fun ?A f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pivot_fun (swaprows i i' A) f j
[PROOF STEP]
by (rule pivot_fun_swaprows[OF pivot dim fij], insert i' ij, auto)
[PROOF STATE]
proof (state)
this:
pivot_fun (swaprows i i' A) f j

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH(2)[OF Cons, unfolded swaprows_carrier, OF A _ this f ij]
[PROOF STATE]
proof (state)
this:
\<lbrakk>gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j = (A', B'); \<And>i'. i' < i \<Longrightarrow> i' < i; \<And>i'. i \<le> i' \<Longrightarrow> i \<le> i'\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
from Z valid res
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')
[PROOF STEP]
have id: "gauss_jordan_main ?A ?B i j = (A', B')"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j = (A', B')
[PROOF STEP]
unfolding simp dim Cons
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
i < nr \<and> j < nc
(if i < nr \<and> j < nc then if A $$ (i, j) = (0::'a) then case i' # iis of [] \<Rightarrow> gauss_jordan_main A B i (Suc j) | i' # x \<Rightarrow> gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j else if A $$ (i, j) = (1::'a) then gauss_jordan_main (eliminate_entries (\<lambda>i. A $$ (i, j)) A i j) (eliminate_entries (\<lambda>i. A $$ (i, j)) B i j) (Suc i) (Suc j) else gauss_jordan_main (multrow i (inverse (A $$ (i, j))) A) (multrow i (inverse (A $$ (i, j))) B) i j else (A, B)) = (A', B')

goal (1 subgoal):
 1. gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j = (A', B')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_jordan_main (swaprows i i' A) (swaprows i i' B) i j = (A', B')

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
note IH = IH[OF this]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i'. i' < i \<Longrightarrow> i' < i; \<And>i'. i \<le> i' \<Longrightarrow> i \<le> i'\<rbrakk> \<Longrightarrow> row_echelon_form A'

goal (1 subgoal):
 1. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> row_echelon_form A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_echelon_form A'
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i'. i' < i \<Longrightarrow> i' < i; \<And>i'. i \<le> i' \<Longrightarrow> i \<le> i'\<rbrakk> \<Longrightarrow> row_echelon_form A'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
row_echelon_form A'

goal:
No subgoals!
[PROOF STEP]
qed