[STATEMENT]
lemma Unit_prod_eliminate_entries: "i < nr \<Longrightarrow> (\<And> a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i)
  \<Longrightarrow> \<exists> P \<in> Units (ring_mat TYPE('a :: comm_ring_1) nr b) . \<forall> B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B
[PROOF STEP]
proof (induct "is")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set [] \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i [] = P * B
 2. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
i < nr
(?a, ?i') \<in> set [] \<Longrightarrow> ?i' < nr \<and> ?i' \<noteq> i

goal (2 subgoals):
 1. \<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set [] \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i [] = P * B
 2. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i < nr
(?a, ?i') \<in> set [] \<Longrightarrow> ?i' < nr \<and> ?i' \<noteq> i

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i [] = P * B
[PROOF STEP]
by (intro bexI[of _ "1\<^sub>m nr"], auto simp: Units_def ring_mat_def)
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i [] = P * B

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
case (Cons ai' "is")
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B
i < nr
(?a, ?i') \<in> set (ai' # is) \<Longrightarrow> ?i' < nr \<and> ?i' \<noteq> i

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
obtain a i' where ai': "ai' = (a,i')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a i'. ai' = (a, i') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ai' = (a, i')

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
let ?U = "Units (ring_mat TYPE('a) nr b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[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. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
from Cons(1)[OF Cons(2-3)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a i'. (a, i') \<in> set is \<Longrightarrow> (?a a i', i') \<in> set (ai' # is)) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B
[PROOF STEP]
obtain P where P: "P \<in> ?U" and id: "\<And> B nc . B \<in> carrier_mat nr nc \<Longrightarrow>
    eliminate_entries_rec B i is = P * B"
[PROOF STATE]
proof (prove)
using this:
(\<And>a i'. (a, i') \<in> set is \<Longrightarrow> (?a a i', i') \<in> set (ai' # is)) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) nr b); \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i is = P * B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) nr b)
?B \<in> carrier_mat nr ?nc \<Longrightarrow> eliminate_entries_rec ?B i is = P * ?B

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
let ?Add = "addrow_mat nr a i' i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
have Add: "?Add \<in> ?U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
by (rule addrow_mat_Unit, insert Cons ai', auto)
[PROOF STATE]
proof (state)
this:
addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
from m.Units_m_closed[OF P Add]
[PROOF STATE]
proof (chain)
picking this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
have PI: "P * ?Add \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P * addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>\<^esub> addrow_mat nr a i' i \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P * addrow_mat nr a i' i \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P * addrow_mat nr a i' i \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
from m.Units_closed[OF P]
[PROOF STATE]
proof (chain)
picking this:
P \<in> carrier (ring_mat TYPE('a) nr b)
[PROOF STEP]
have P: "P \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr nr

goal (1 subgoal):
 1. \<And>a is. \<lbrakk>\<lbrakk>i < nr; \<And>a i'. (a, i') \<in> set is \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i is = P * B; i < nr; \<And>aa i'. (aa, i') \<in> set (a # is) \<Longrightarrow> i' < nr \<and> i' \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (a # is) = P * B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (ai' # is) = P * B
[PROOF STEP]
proof (rule bexI[OF _ PI], intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
fix B :: "'a mat" and nc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
assume BB: "B \<in> carrier_mat nr nc"
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat nr nc

goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
let ?B = "addrow a i' i B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
from BB
[PROOF STATE]
proof (chain)
picking this:
B \<in> carrier_mat nr nc
[PROOF STEP]
have B: "?B \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
using this:
B \<in> carrier_mat nr nc

goal (1 subgoal):
 1. addrow a i' i B \<in> carrier_mat nr nc
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
addrow a i' i B \<in> carrier_mat nr nc

goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
from id[OF B]
[PROOF STATE]
proof (chain)
picking this:
eliminate_entries_rec (addrow a i' i B) i is = P * addrow a i' i B
[PROOF STEP]
have id: "eliminate_entries_rec ?B i is = P * ?B"
[PROOF STATE]
proof (prove)
using this:
eliminate_entries_rec (addrow a i' i B) i is = P * addrow a i' i B

goal (1 subgoal):
 1. eliminate_entries_rec (addrow a i' i B) i is = P * addrow a i' i B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec (addrow a i' i B) i is = P * addrow a i' i B

goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
have id2: "eliminate_entries_rec B i (ai' # is) = eliminate_entries_rec ?B i is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B i (ai' # is) = eliminate_entries_rec (addrow a i' i B) i is
[PROOF STEP]
unfolding ai'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B i ((a, i') # is) = eliminate_entries_rec (addrow a i' i B) i is
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B i (ai' # is) = eliminate_entries_rec (addrow a i' i B) i is

goal (1 subgoal):
 1. \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
show "eliminate_entries_rec B i (ai' # is) = P * ?Add * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B
[PROOF STEP]
unfolding id2 id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * addrow a i' i B = P * addrow_mat nr a i' i * B
[PROOF STEP]
unfolding addrow_mat[OF BB Cons(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * (addrow_mat nr a i' i * B) = P * addrow_mat nr a i' i * B
[PROOF STEP]
by (rule assoc_mult_mat[symmetric, OF P _ BB], auto)
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B i (ai' # is) = P * addrow_mat nr a i' i * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (ai' # is) = P * B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_transform: assumes A: "A \<in> carrier_mat nr nc" and B: "B \<in> carrier_mat nr nc'"
  and res: "gauss_jordan (A :: 'a :: field mat) B = (A',B')"
  shows "\<exists> P \<in> Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?U = "Units (ring_mat TYPE('a) nr b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
fix i j :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
assume "gauss_jordan_main A B i j = (A',B')"
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
with A B
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
B \<in> carrier_mat nr nc'
gauss_jordan_main A B i j = (A', B')
[PROOF STEP]
have "\<exists> P \<in> ?U. A' = P * A \<and> B' = P * B"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc
B \<in> carrier_mat nr nc'
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
proof (induction A B i j rule: gauss_jordan_main.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
case (1 A B i j)
[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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
\<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; swaprows i ?x21.0 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i ?x21.0 A \<and> B' = P * swaprows i ?x21.0 B
\<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; eliminate_entries ?xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries ?xb A i j \<and> B' = P * eliminate_entries ?xb B i j
\<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; multrow i ?xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i ?xb A \<and> B' = P * multrow i ?xb B
A \<in> carrier_mat nr nc
B \<in> carrier_mat nr nc'
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
note B = 1(6)
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat nr nc'

goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
hence dimB: "dim_row B = nr" "dim_col B = nc'"
[PROOF STATE]
proof (prove)
using this:
B \<in> carrier_mat nr nc'

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

goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
\<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; swaprows i ?x21.0 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i ?x21.0 A \<and> B' = P * swaprows i ?x21.0 B
\<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; eliminate_entries ?xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries ?xb A i j \<and> B' = P * eliminate_entries ?xb B i j
\<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; multrow i ?xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i ?xb A \<and> B' = P * multrow i ?xb B

goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
note res = 1(7)
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B i j = (A', B')

goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?g = "gauss_jordan_main A B i j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B i j. \<lbrakk>\<And>x xa xaa. \<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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B; \<And>x xa xaa x21 x22. \<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; swaprows i x21 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i x21 A) (swaprows i x21 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i x21 A \<and> B' = P * swaprows i x21 B; \<And>x xa xaa xb. \<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; eliminate_entries xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries xb A i j \<and> B' = P * eliminate_entries xb B i j; \<And>x xa xaa xb. \<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; multrow i xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i xb A) (multrow i xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i xb A \<and> B' = P * multrow i xb B; A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
proof (cases "i < nr \<and> j < nc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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 res: "A' = A" "B' = B"
[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 &&& B' = B
[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 &&& B' = B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' = A
B' = B

goal (2 subgoals):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<not> (i < nr \<and> j < nc) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
unfolding res
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A = P * A \<and> B = P * B
[PROOF STEP]
by (rule bexI[of _ "1\<^sub>m nr"], insert A B, auto simp: Units_def ring_mat_def)
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < nr \<and> j < nc

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
\<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; swaprows i ?x21.0 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i ?x21.0 A \<and> B' = P * swaprows i ?x21.0 B
\<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; eliminate_entries ?xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries ?xb A i j \<and> B' = P * eliminate_entries ?xb B i j
\<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; multrow i ?xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i ?xb A \<and> B' = P * multrow i ?xb B

goal (1 subgoal):
 1. i < nr \<and> j < nc \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
proof (cases "A $$ (i,j) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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; eliminate_entries ?xb B 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')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries ?xb A i j \<and> B' = P * eliminate_entries ?xb B i j
\<lbrakk>A $$ (i, j) \<noteq> (1::'a); ?xb = inverse (A $$ (i, j)); multrow i ?xb A \<in> carrier_mat nr nc; multrow i ?xb B \<in> carrier_mat nr nc'; gauss_jordan_main (multrow i ?xb A) (multrow i ?xb B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i ?xb A \<and> B' = P * multrow i ?xb B

goal (2 subgoals):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
proof (cases "A $$ (i,j) = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?inv = "inverse (A $$ (i,j))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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 "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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
note IH = IH(2)[OF nO refl, unfolded multrow_carrier, OF A B this]
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i (inverse (A $$ (i, j))) A \<and> B' = P * multrow i (inverse (A $$ (i, j))) B

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i (inverse (A $$ (i, j))) A \<and> B' = P * multrow i (inverse (A $$ (i, j))) B
[PROOF STEP]
obtain P where P: "P \<in> ?U" and
              id: "A' = P * multrow i ?inv A" "B' = P * multrow i ?inv B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * multrow i (inverse (A $$ (i, j))) A \<and> B' = P * multrow i (inverse (A $$ (i, j))) B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) nr b); A' = P * multrow i (inverse (A $$ (i, j))) A; B' = P * multrow i (inverse (A $$ (i, j))) B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) nr b)
A' = P * multrow i (inverse (A $$ (i, j))) A
B' = P * multrow i (inverse (A $$ (i, j))) B

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?Inv = "multrow_mat nr i ?inv"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from nZ valid
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc
[PROOF STEP]
have "i < nr" "?inv \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) \<noteq> (0::'a)
i < nr \<and> j < nc

goal (1 subgoal):
 1. i < nr &&& inverse (A $$ (i, j)) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < nr
inverse (A $$ (i, j)) \<noteq> (0::'a)

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from multrow_mat_Unit[OF this]
[PROOF STATE]
proof (chain)
picking this:
multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr ?b)
[PROOF STEP]
have Inv: "?Inv \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr ?b)

goal (1 subgoal):
 1. multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_m_closed[OF P Inv]
[PROOF STATE]
proof (chain)
picking this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
have PI: "P * ?Inv \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P * multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>\<^esub> multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P * multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P * multrow_mat nr i (inverse (A $$ (i, j))) \<in> Units (ring_mat TYPE('a) nr b)

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_closed[OF P]
[PROOF STATE]
proof (chain)
picking this:
P \<in> carrier (ring_mat TYPE('a) nr b)
[PROOF STEP]
have P: "P \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr nr

goal (2 subgoals):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. A $$ (i, j) \<noteq> (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa\<in>Units (ring_mat TYPE('a) nr b). P * multrow i (inverse (A $$ (i, j))) A = Pa * A \<and> P * multrow i (inverse (A $$ (i, j))) B = Pa * B
[PROOF STEP]
unfolding multrow_mat[OF A] multrow_mat[OF B]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa\<in>Units (ring_mat TYPE('a) nr b). P * (multrow_mat nr i (inverse (A $$ (i, j))) * A) = Pa * A \<and> P * (multrow_mat nr i (inverse (A $$ (i, j))) * B) = Pa * B
[PROOF STEP]
by (rule bexI[OF _ PI], intro conjI,
                rule assoc_mult_mat[symmetric, OF P _ A], simp,
                rule assoc_mult_mat[symmetric, OF P _ B], simp)
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (1::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?is = "filter (\<lambda> i'. i' \<noteq> i) [0 ..< nr]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?ais = "map (\<lambda> i'. (-A $$ (i',j), i')) ?is"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?EE = "\<lambda> B. eliminate_entries_rec B i ?ais"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?A = "?E A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?B = "?E B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?AA = "?EE A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?BB = "?EE B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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 ?A ?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 (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]
unfolding 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 (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')

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
note IH = IH(1)[OF O refl carrier_eliminate_entries(1)[OF A] carrier_eliminate_entries(1)[OF B] this]
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j \<and> B' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j \<and> B' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j
[PROOF STEP]
obtain P where P: "P \<in> ?U" and id: "A' = P * ?A" "B' = P * ?B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j \<and> B' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) nr b); A' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j; B' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) nr b)
A' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j
B' = P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
have *: "j < dim_col A" "i < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < dim_col A &&& i < dim_row A
[PROOF STEP]
by (auto simp add: dim valid)
[PROOF STATE]
proof (state)
this:
j < dim_col A
i < dim_row A

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
have "\<exists>P\<in>?U. \<forall> B nc. B \<in> carrier_mat nr nc \<longrightarrow> ?EE B = P * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = P * B
[PROOF STEP]
by (rule Unit_prod_eliminate_entries, insert valid, auto)
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = P * B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = P * B
[PROOF STEP]
obtain Q where Q: "Q \<in> ?U" and QQ: "\<And> B nc. B \<in> carrier_mat nr nc \<Longrightarrow> ?EE B = Q * B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). \<forall>B nc. B \<in> carrier_mat nr nc \<longrightarrow> eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = P * B

goal (1 subgoal):
 1. (\<And>Q. \<lbrakk>Q \<in> Units (ring_mat TYPE('a) nr b); \<And>B nc. B \<in> carrier_mat nr nc \<Longrightarrow> eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<in> Units (ring_mat TYPE('a) nr b)
?B \<in> carrier_mat nr ?nc \<Longrightarrow> eliminate_entries_rec ?B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * ?B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Q \<in> Units (ring_mat TYPE('a) nr b)
?B \<in> carrier_mat nr ?nc \<Longrightarrow> eliminate_entries_rec ?B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * ?B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
fix B :: "'a mat" and nc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
assume B: "B \<in> carrier_mat nr nc"
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat nr nc

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
with dim
[PROOF STATE]
proof (chain)
picking this:
dim_row A = nr
dim_col A = nc
B \<in> carrier_mat nr nc
[PROOF STEP]
have "dim_row B = dim_row A"
[PROOF STATE]
proof (prove)
using this:
dim_row A = nr
dim_col A = nc
B \<in> carrier_mat nr nc

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

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
from eliminate_entries_convert[OF * this]
[PROOF STATE]
proof (chain)
picking this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i. (- A $$ (i, j), i)) (filter (\<lambda>i. i \<noteq> i) [0..<dim_row A]))
[PROOF STEP]
have "?E B = ?EE B"
[PROOF STATE]
proof (prove)
using this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i. (- A $$ (i, j), i)) (filter (\<lambda>i. i \<noteq> i) [0..<dim_row A]))

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr]))
[PROOF STEP]
using dim
[PROOF STATE]
proof (prove)
using this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i. (- A $$ (i, j), i)) (filter (\<lambda>i. i \<noteq> i) [0..<dim_row A]))
dim_row A = nr
dim_col A = nc

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr]))

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr]))

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
have "\<dots> = Q * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * B
[PROOF STEP]
using QQ[OF B]
[PROOF STATE]
proof (prove)
using this:
eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * B

goal (1 subgoal):
 1. eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eliminate_entries_rec B i (map (\<lambda>i'. (- A $$ (i', j), i')) (filter (\<lambda>i'. i' \<noteq> i) [0..<nr])) = Q * B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B
[PROOF STEP]
have "?E B = Q * B"
[PROOF STATE]
proof (prove)
using this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B

goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * Ba__
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Bb2 \<in> carrier_mat nr ?nca2 \<Longrightarrow> eliminate_entries (\<lambda>i. A $$ (i, j)) ?Bb2 i j = Q * ?Bb2

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
note QQ = this
[PROOF STATE]
proof (state)
this:
?Bb2 \<in> carrier_mat nr ?nca2 \<Longrightarrow> eliminate_entries (\<lambda>i. A $$ (i, j)) ?Bb2 i j = Q * ?Bb2

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
have id3: "?A = Q * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) A i j = Q * A
[PROOF STEP]
by (rule QQ[OF A])
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, j)) A i j = Q * A

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
have id4: "?B = Q * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B
[PROOF STEP]
by (rule QQ[OF B])
[PROOF STATE]
proof (state)
this:
eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Q * B

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_closed[OF P]
[PROOF STATE]
proof (chain)
picking this:
P \<in> carrier (ring_mat TYPE('a) nr b)
[PROOF STEP]
have Pc: "P \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr nr

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_closed[OF Q]
[PROOF STATE]
proof (chain)
picking this:
Q \<in> carrier (ring_mat TYPE('a) nr b)
[PROOF STEP]
have Qc: "Q \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
Q \<in> carrier (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. Q \<in> carrier_mat nr nr
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. Q \<in> carrier_mat nr nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q \<in> carrier_mat nr nr

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_m_closed[OF P Q]
[PROOF STATE]
proof (chain)
picking this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> Q \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
have PQ: "P * Q \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> Q \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P * Q \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>\<^esub> Q \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P * Q \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P * Q \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. A $$ (i, j) = (1::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa\<in>Units (ring_mat TYPE('a) nr b). P * eliminate_entries (\<lambda>i. A $$ (i, j)) A i j = Pa * A \<and> P * eliminate_entries (\<lambda>i. A $$ (i, j)) B i j = Pa * B
[PROOF STEP]
unfolding id3 id4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa\<in>Units (ring_mat TYPE('a) nr b). P * (Q * A) = Pa * A \<and> P * (Q * B) = Pa * B
[PROOF STEP]
by (rule bexI[OF _ PQ], rule conjI,
              rule assoc_mult_mat[symmetric, OF Pc Qc A],
              rule assoc_mult_mat[symmetric, OF Pc Qc B])
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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; B \<in> carrier_mat nr nc'; gauss_jordan_main A B i (Suc j) = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
\<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; swaprows i ?x21.0 B \<in> carrier_mat nr nc'; gauss_jordan_main (swaprows i ?x21.0 A) (swaprows i ?x21.0 B) i j = (A', B')\<rbrakk> \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i ?x21.0 A \<and> B' = P * swaprows i ?x21.0 B

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a) \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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 (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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
 2. \<And>a list. concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = a # list \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from IH(1)[OF Nil A B this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[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 (swaprows i i' A) (swaprows i i' 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from IH(2)[OF Cons, unfolded swaprows_carrier, OF A B this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i i' A \<and> B' = P * swaprows i i' B
[PROOF STEP]
obtain P where P: "P \<in> ?U" and
              id: "A' = P * swaprows i i' A" "B' = P * swaprows i i' B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * swaprows i i' A \<and> B' = P * swaprows i i' B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) nr b); A' = P * swaprows i i' A; B' = P * swaprows i i' B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) nr b)
A' = P * swaprows i i' A
B' = P * swaprows i i' 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
let ?Swap = "swaprows_mat nr i i'"
[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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = i' # iis
[PROOF STEP]
have "i' \<in> set ?is"
[PROOF STATE]
proof (prove)
using this:
concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]) = i' # iis

goal (1 subgoal):
 1. i' \<in> set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' \<in> set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
with valid
[PROOF STATE]
proof (chain)
picking this:
i < nr \<and> j < nc
i' \<in> set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]))
[PROOF STEP]
have i': "i < nr" "i' < nr"
[PROOF STATE]
proof (prove)
using this:
i < nr \<and> j < nc
i' \<in> set (concat (map (\<lambda>i'. if A $$ (i', j) \<noteq> (0::'a) then [i'] else []) [Suc i..<nr]))

goal (1 subgoal):
 1. i < nr &&& i' < nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < nr
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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from swaprows_mat_Unit[OF this]
[PROOF STATE]
proof (chain)
picking this:
swaprows_mat nr i i' \<in> Units (ring_mat TYPE(?'a) nr ?b)
[PROOF STEP]
have Swap: "?Swap \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
swaprows_mat nr i i' \<in> Units (ring_mat TYPE(?'a) nr ?b)

goal (1 subgoal):
 1. swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_m_closed[OF P Swap]
[PROOF STATE]
proof (chain)
picking this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
have PI: "P * ?Swap \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) nr b\<^esub> swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P * swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr b)
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>\<^esub> swaprows_mat nr i i' \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P * swaprows_mat nr i i' \<in> Units \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P * swaprows_mat nr i i' \<in> Units (ring_mat TYPE('a) nr 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from m.Units_closed[OF P]
[PROOF STATE]
proof (chain)
picking this:
P \<in> carrier (ring_mat TYPE('a) nr b)
[PROOF STEP]
have P: "P \<in> carrier_mat nr nr"
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier (ring_mat TYPE('a) nr b)

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
unfolding ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+), \<dots> = b\<rparr>

goal (1 subgoal):
 1. P \<in> carrier_mat nr nr
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr 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> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
unfolding id swaprows_mat[OF A i'] swaprows_mat[OF B i']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Pa\<in>Units (ring_mat TYPE('a) nr b). P * (swaprows_mat nr i i' * A) = Pa * A \<and> P * (swaprows_mat nr i i' * B) = Pa * B
[PROOF STEP]
by (rule bexI[OF _ PI], rule conjI,
              rule assoc_mult_mat[symmetric, OF P _ A], simp,
              rule assoc_mult_mat[symmetric, OF P _ B], simp)
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
gauss_jordan_main A B ?i2 ?j2 = (A', B') \<Longrightarrow> \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
from this[of 0 0, folded gauss_jordan_def, OF res]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. \<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>Units (ring_mat TYPE('a) nr b). A' = P * A \<and> B' = P * B

goal:
No subgoals!
[PROOF STEP]
qed