[STATEMENT]
lemma gauss_jordan: assumes A: "A \<in> carrier_mat nr nc"
  and B: "B \<in> carrier_mat nr nc2"
  and gauss: "gauss_jordan A B = (C,D)"
  shows "x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)" (is "_ \<Longrightarrow> ?l = ?r")
    "X \<in> carrier_mat nc nc2  \<Longrightarrow> (A * X = B) = (C * X = D)" (is " _ \<Longrightarrow> ?l2 = ?r2")
    "C \<in> carrier_mat nr nc"
    "D \<in> carrier_mat nr nc2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)) &&& (X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D))) &&& C \<in> carrier_mat nr nc &&& D \<in> carrier_mat nr nc2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
 3. C \<in> carrier_mat nr nc
 4. D \<in> carrier_mat nr nc2
[PROOF STEP]
from gauss_jordan_transform[OF A B gauss, unfolded ring_mat_def Units_def, simplified]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P. P \<in> carrier_mat nr nr \<and> (\<exists>x\<in>carrier_mat nr nr. x * P = 1\<^sub>m nr \<and> P * x = 1\<^sub>m nr) \<and> C = P * A \<and> D = P * B
[PROOF STEP]
obtain P Q where P: "P \<in> carrier_mat nr nr" and Q: "Q \<in> carrier_mat nr nr"
    and inv: "Q * P = 1\<^sub>m nr"
    and CPA: "C = P * A"
    and DPB: "D = P * B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P. P \<in> carrier_mat nr nr \<and> (\<exists>x\<in>carrier_mat nr nr. x * P = 1\<^sub>m nr \<and> P * x = 1\<^sub>m nr) \<and> C = P * A \<and> D = P * B

goal (1 subgoal):
 1. (\<And>P Q. \<lbrakk>P \<in> carrier_mat nr nr; Q \<in> carrier_mat nr nr; Q * P = 1\<^sub>m nr; C = P * A; D = P * B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat nr nr
Q \<in> carrier_mat nr nr
Q * P = 1\<^sub>m nr
C = P * A
D = P * B

goal (4 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
 3. C \<in> carrier_mat nr nc
 4. D \<in> carrier_mat nr nc2
[PROOF STEP]
from CPA P A
[PROOF STATE]
proof (chain)
picking this:
C = P * A
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
[PROOF STEP]
show C: "C \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
using this:
C = P * A
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc

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

goal (3 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
 3. D \<in> carrier_mat nr nc2
[PROOF STEP]
from DPB P B
[PROOF STATE]
proof (chain)
picking this:
D = P * B
P \<in> carrier_mat nr nr
B \<in> carrier_mat nr nc2
[PROOF STEP]
show D: "D \<in> carrier_mat nr nc2"
[PROOF STATE]
proof (prove)
using this:
D = P * B
P \<in> carrier_mat nr nr
B \<in> carrier_mat nr nc2

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

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
have "A = 1\<^sub>m nr * A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 1\<^sub>m nr * A
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. A = 1\<^sub>m nr * A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = 1\<^sub>m nr * A

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A = 1\<^sub>m nr * A

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
have "\<dots> = Q * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m nr * A = Q * C
[PROOF STEP]
unfolding inv[symmetric] CPA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q * P * A = Q * (P * A)
[PROOF STEP]
using Q P A
[PROOF STATE]
proof (prove)
using this:
Q \<in> carrier_mat nr nr
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. Q * P * A = Q * (P * A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1\<^sub>m nr * A = Q * C

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A = Q * C
[PROOF STEP]
have AQC: "A = Q * C"
[PROOF STATE]
proof (prove)
using this:
A = Q * C

goal (1 subgoal):
 1. A = Q * C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A = Q * C

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
have "B = 1\<^sub>m nr * B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = 1\<^sub>m nr * B
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
B \<in> carrier_mat nr nc2

goal (1 subgoal):
 1. B = 1\<^sub>m nr * B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B = 1\<^sub>m nr * B

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B = 1\<^sub>m nr * B

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
have "\<dots> = Q * D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m nr * B = Q * D
[PROOF STEP]
unfolding inv[symmetric] DPB
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q * P * B = Q * (P * B)
[PROOF STEP]
using Q P B
[PROOF STATE]
proof (prove)
using this:
Q \<in> carrier_mat nr nr
P \<in> carrier_mat nr nr
B \<in> carrier_mat nr nc2

goal (1 subgoal):
 1. Q * P * B = Q * (P * B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1\<^sub>m nr * B = Q * D

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B = Q * D
[PROOF STEP]
have BQD: "B = Q * D"
[PROOF STATE]
proof (prove)
using this:
B = Q * D

goal (1 subgoal):
 1. B = Q * D
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
B = Q * D

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
B = Q * D

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume x: "x \<in> carrier_vec nc"
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume ?l
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> v. P *\<^sub>v v"] P A x
[PROOF STATE]
proof (chain)
picking this:
P *\<^sub>v (A *\<^sub>v x) = P *\<^sub>v 0\<^sub>v nr
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc
[PROOF STEP]
have ?r
[PROOF STATE]
proof (prove)
using this:
P *\<^sub>v (A *\<^sub>v x) = P *\<^sub>v 0\<^sub>v nr
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc

goal (1 subgoal):
 1. C *\<^sub>v x = 0\<^sub>v nr
[PROOF STEP]
unfolding CPA
[PROOF STATE]
proof (prove)
using this:
P *\<^sub>v (A *\<^sub>v x) = P *\<^sub>v 0\<^sub>v nr
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
x \<in> carrier_vec nc

goal (1 subgoal):
 1. P * A *\<^sub>v x = 0\<^sub>v nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> C *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> C *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> C *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
C *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> v. Q *\<^sub>v v"] Q C x
[PROOF STATE]
proof (chain)
picking this:
Q *\<^sub>v (C *\<^sub>v x) = Q *\<^sub>v 0\<^sub>v nr
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
x \<in> carrier_vec nc
[PROOF STEP]
have ?l
[PROOF STATE]
proof (prove)
using this:
Q *\<^sub>v (C *\<^sub>v x) = Q *\<^sub>v 0\<^sub>v nr
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
x \<in> carrier_vec nc

goal (1 subgoal):
 1. A *\<^sub>v x = 0\<^sub>v nr
[PROOF STEP]
unfolding AQC
[PROOF STATE]
proof (prove)
using this:
Q *\<^sub>v (C *\<^sub>v x) = Q *\<^sub>v 0\<^sub>v nr
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
x \<in> carrier_vec nc

goal (1 subgoal):
 1. Q * C *\<^sub>v x = 0\<^sub>v nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
C *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> A *\<^sub>v x = 0\<^sub>v nr

goal (2 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> C *\<^sub>v x = 0\<^sub>v nr
C *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> A *\<^sub>v x = 0\<^sub>v nr
[PROOF STEP]
show "?l = ?r"
[PROOF STATE]
proof (prove)
using this:
A *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> C *\<^sub>v x = 0\<^sub>v nr
C *\<^sub>v x = 0\<^sub>v nr \<Longrightarrow> A *\<^sub>v x = 0\<^sub>v nr

goal (1 subgoal):
 1. (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume X: "X \<in> carrier_mat nc nc2"
[PROOF STATE]
proof (state)
this:
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume ?l2
[PROOF STATE]
proof (state)
this:
A * X = B

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> X. P * X"] P A X
[PROOF STATE]
proof (chain)
picking this:
P * (A * X) = P * B
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2
[PROOF STEP]
have ?r2
[PROOF STATE]
proof (prove)
using this:
P * (A * X) = P * B
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. C * X = D
[PROOF STEP]
unfolding CPA DPB
[PROOF STATE]
proof (prove)
using this:
P * (A * X) = P * B
P \<in> carrier_mat nr nr
A \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. P * A * X = P * B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C * X = D

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A * X = B \<Longrightarrow> C * X = D

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A * X = B \<Longrightarrow> C * X = D

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
A * X = B \<Longrightarrow> C * X = D

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
assume ?r2
[PROOF STATE]
proof (state)
this:
C * X = D

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> X. Q * X"] Q C X
[PROOF STATE]
proof (chain)
picking this:
Q * (C * X) = Q * D
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2
[PROOF STEP]
have ?l2
[PROOF STATE]
proof (prove)
using this:
Q * (C * X) = Q * D
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. A * X = B
[PROOF STEP]
unfolding AQC BQD
[PROOF STATE]
proof (prove)
using this:
Q * (C * X) = Q * D
Q \<in> carrier_mat nr nr
C \<in> carrier_mat nr nc
X \<in> carrier_mat nc nc2

goal (1 subgoal):
 1. Q * C * X = Q * D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A * X = B

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
C * X = D \<Longrightarrow> A * X = B

goal (1 subgoal):
 1. X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A * X = B \<Longrightarrow> C * X = D
C * X = D \<Longrightarrow> A * X = B
[PROOF STEP]
show "?l2 = ?r2"
[PROOF STATE]
proof (prove)
using this:
A * X = B \<Longrightarrow> C * X = D
C * X = D \<Longrightarrow> A * X = B

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

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
X \<in> carrier_mat nc nc2 \<Longrightarrow> (A * X = B) = (C * X = D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_single: assumes A: "A \<in> carrier_mat nr nc"
  and gauss: "gauss_jordan_single A = C"
  shows "x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)"
    "C \<in> carrier_mat nr nc"
    "row_echelon_form C"
    "\<exists> P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr" (is "?ex")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)) &&& C \<in> carrier_mat nr nc) &&& row_echelon_form C &&& \<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. C \<in> carrier_mat nr nc
 3. row_echelon_form C
 4. \<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr
[PROOF STEP]
from A gauss[unfolded gauss_jordan_single_def]
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat nr nc
fst (gauss_jordan A (0\<^sub>m (dim_row A) 0)) = C
[PROOF STEP]
obtain D where gauss: "gauss_jordan A (0\<^sub>m nr 0) = (C,D)"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc
fst (gauss_jordan A (0\<^sub>m (dim_row A) 0)) = C

goal (1 subgoal):
 1. (\<And>D. gauss_jordan A (0\<^sub>m nr 0) = (C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "gauss_jordan A (0\<^sub>m nr 0)", auto)
[PROOF STATE]
proof (state)
this:
gauss_jordan A (0\<^sub>m nr 0) = (C, D)

goal (4 subgoals):
 1. x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
 2. C \<in> carrier_mat nr nc
 3. row_echelon_form C
 4. \<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr
[PROOF STEP]
from gauss_jordan[OF A zero_carrier_mat gauss] gauss_jordan_row_echelon[OF A gauss]
    gauss_jordan_transform[OF A zero_carrier_mat gauss, of "()"]
[PROOF STATE]
proof (chain)
picking this:
?x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v ?x = 0\<^sub>v nr) = (C *\<^sub>v ?x = 0\<^sub>v nr)
?X \<in> carrier_mat nc 0 \<Longrightarrow> (A * ?X = 0\<^sub>m nr 0) = (C * ?X = D)
C \<in> carrier_mat nr nc
D \<in> carrier_mat nr 0
row_echelon_form C
\<exists>P\<in>Units (ring_mat TYPE('a) nr ()). C = P * A \<and> D = P * 0\<^sub>m nr 0
[PROOF STEP]
show "x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)"
    "C \<in> carrier_mat nr nc" "row_echelon_form C" ?ex
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v ?x = 0\<^sub>v nr) = (C *\<^sub>v ?x = 0\<^sub>v nr)
?X \<in> carrier_mat nc 0 \<Longrightarrow> (A * ?X = 0\<^sub>m nr 0) = (C * ?X = D)
C \<in> carrier_mat nr nc
D \<in> carrier_mat nr 0
row_echelon_form C
\<exists>P\<in>Units (ring_mat TYPE('a) nr ()). C = P * A \<and> D = P * 0\<^sub>m nr 0

goal (1 subgoal):
 1. ((x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)) &&& C \<in> carrier_mat nr nc) &&& row_echelon_form C &&& \<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr
[PROOF STEP]
unfolding Units_def ring_mat_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v ?x = 0\<^sub>v nr) = (C *\<^sub>v ?x = 0\<^sub>v nr)
?X \<in> carrier_mat nc 0 \<Longrightarrow> (A * ?X = 0\<^sub>m nr 0) = (C * ?X = D)
C \<in> carrier_mat nr nc
D \<in> carrier_mat nr 0
row_echelon_form C
\<exists>P\<in>{y \<in> carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat nr nr, monoid.mult = (*), one = 1\<^sub>m nr, zero = 0\<^sub>m nr nr, add = (+)\<rparr>\<^esub>}. C = P * A \<and> D = P * 0\<^sub>m nr 0

goal (1 subgoal):
 1. ((x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)) &&& C \<in> carrier_mat nr nc) &&& row_echelon_form C &&& \<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec nc \<Longrightarrow> (A *\<^sub>v x = 0\<^sub>v nr) = (C *\<^sub>v x = 0\<^sub>v nr)
C \<in> carrier_mat nr nc
row_echelon_form C
\<exists>P Q. C = P * A \<and> P \<in> carrier_mat nr nr \<and> Q \<in> carrier_mat nr nr \<and> P * Q = 1\<^sub>m nr \<and> Q * P = 1\<^sub>m nr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_inverse_one_direction:
  assumes A: "A \<in> carrier_mat n n" and B: "B \<in> carrier_mat n nc"
  and res: "gauss_jordan A B = (1\<^sub>m n, B')"
  shows "A \<in> Units (ring_mat TYPE('a :: field) n b)"
  "B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> Units (ring_mat TYPE('a) n b) &&& (B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
let ?R = "ring_mat TYPE('a) n b"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
let ?U = "Units ?R"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
interpret m: ring ?R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (ring_mat TYPE('a) n b)
[PROOF STEP]
by (rule ring_mat)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
from gauss_jordan_transform[OF A B res, of b]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) n b). 1\<^sub>m n = P * A \<and> B' = P * B
[PROOF STEP]
obtain P where P: "P \<in> ?U" and id: "P * A = 1\<^sub>m n" and B': "B' = P * B"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) n b). 1\<^sub>m n = P * A \<and> B' = P * B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) n b); P * A = 1\<^sub>m n; B' = P * B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) n b)
P * A = 1\<^sub>m n
B' = P * B

goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
P \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
have Pc: "P \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
P \<in> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. P \<in> carrier_mat n n
[PROOF STEP]
unfolding Units_def ring_mat_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {y \<in> carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub>}

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

goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b)
 2. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
from m.Units_one_side_I(1)[of A P] A P id
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>A \<in> carrier (ring_mat TYPE('a) n b); P \<in> Units (ring_mat TYPE('a) n b); P \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> A = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>\<rbrakk> \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
A \<in> carrier_mat n n
P \<in> Units (ring_mat TYPE('a) n b)
P * A = 1\<^sub>m n
[PROOF STEP]
show Au: "A \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>A \<in> carrier (ring_mat TYPE('a) n b); P \<in> Units (ring_mat TYPE('a) n b); P \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> A = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>\<rbrakk> \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
A \<in> carrier_mat n n
P \<in> Units (ring_mat TYPE('a) n b)
P * A = 1\<^sub>m n

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

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

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
assume B: "B = 1\<^sub>m n"
[PROOF STATE]
proof (state)
this:
B = 1\<^sub>m n

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
from B'[unfolded this] Pc
[PROOF STATE]
proof (chain)
picking this:
B' = P * 1\<^sub>m n
P \<in> carrier_mat n n
[PROOF STEP]
have B': "B' = P"
[PROOF STATE]
proof (prove)
using this:
B' = P * 1\<^sub>m n
P \<in> carrier_mat n n

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

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
show "A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
unfolding B'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * P = 1\<^sub>m n \<and> P * A = 1\<^sub>m n
[PROOF STEP]
using m.Units_inv_comm[OF _ P Au] id
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> A = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub> \<Longrightarrow> A \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> P = \<one>\<^bsub>ring_mat TYPE('a) n b\<^esub>
P * A = 1\<^sub>m n

goal (1 subgoal):
 1. A * P = 1\<^sub>m n \<and> P * A = 1\<^sub>m n
[PROOF STEP]
by (auto simp: ring_mat_def)
[PROOF STATE]
proof (state)
this:
A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_inverse_other_direction:
  assumes AU: "A \<in> Units (ring_mat TYPE('a :: field) n b)" and B: "B \<in> carrier_mat n nc"
  shows "fst (gauss_jordan A B) = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
let ?R = "ring_mat TYPE('a) n b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
let ?U = "Units ?R"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
interpret m: ring ?R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (ring_mat TYPE('a) n b)
[PROOF STEP]
by (rule ring_mat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
from AU
[PROOF STATE]
proof (chain)
picking this:
A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
have A: "A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. A \<in> carrier_mat n n
[PROOF STEP]
unfolding Units_def ring_mat_def
[PROOF STATE]
proof (prove)
using this:
A \<in> {y \<in> carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub>}

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

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
obtain A' B' where res: "gauss_jordan A B = (A',B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A' B'. gauss_jordan A B = (A', B') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
gauss_jordan A B = (A', B')

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
from gauss_jordan_transform[OF A B res, of b]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) n b). A' = P * A \<and> B' = P * B
[PROOF STEP]
obtain P where P: "P \<in> ?U" and id: "A' = P * A"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) n b). A' = P * A \<and> B' = P * B

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) n b); A' = P * A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) n b)
A' = P * A

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
from m.Units_m_closed[OF P AU]
[PROOF STATE]
proof (chain)
picking this:
P \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
have A': "A' \<in> ?U"
[PROOF STATE]
proof (prove)
using this:
P \<otimes>\<^bsub>ring_mat TYPE('a) n b\<^esub> A \<in> Units (ring_mat TYPE('a) n b)

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

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

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
hence A'c: "A' \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A' \<in> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. A' \<in> carrier_mat n n
[PROOF STEP]
unfolding Units_def ring_mat_def
[PROOF STATE]
proof (prove)
using this:
A' \<in> {y \<in> carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub>}

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

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
from A'[unfolded Units_def ring_mat_def]
[PROOF STATE]
proof (chain)
picking this:
A' \<in> {y \<in> carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub>}
[PROOF STEP]
obtain IA' where IA': "IA' \<in> carrier_mat n n"
    and IA: "A' * IA' = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
A' \<in> {y \<in> carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. \<exists>x\<in>carrier \<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>. x \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> y = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> \<and> y \<otimes>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub> x = \<one>\<^bsub>\<lparr>carrier = carrier_mat n n, monoid.mult = (*), one = 1\<^sub>m n, zero = 0\<^sub>m n n, add = (+), \<dots> = b\<rparr>\<^esub>}

goal (1 subgoal):
 1. (\<And>IA'. \<lbrakk>IA' \<in> carrier_mat n n; A' * IA' = 1\<^sub>m n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
IA' \<in> carrier_mat n n
A' * IA' = 1\<^sub>m n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
from row_echelon_form_imp_1_or_0_row[OF gauss_jordan_carrier(1)[OF A B res] gauss_jordan_row_echelon[OF A res]]
[PROOF STATE]
proof (chain)
picking this:
A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n
[PROOF STEP]
have choice: "A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
hence "A' = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
A' = 1\<^sub>m n \<or> 0 < n \<and> row A' (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. A' = 1\<^sub>m n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
let ?n = "n - 1"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
assume "0 < n \<and> row A' ?n = 0\<^sub>v n"
[PROOF STATE]
proof (state)
this:
0 < n \<and> row A' (n - 1) = 0\<^sub>v n

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
hence n: "?n < n" and row: "row A' ?n =  0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
0 < n \<and> row A' (n - 1) = 0\<^sub>v n

goal (1 subgoal):
 1. n - 1 < n &&& row A' (n - 1) = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - 1 < n
row A' (n - 1) = 0\<^sub>v n

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
have "1 = 1\<^sub>m n $$ (?n,?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'c) = 1\<^sub>m n $$ (n - 1, n - 1)
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n - 1 < n

goal (1 subgoal):
 1. (1::'c) = 1\<^sub>m n $$ (n - 1, n - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1::?'c1) = 1\<^sub>m n $$ (n - 1, n - 1)

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::?'c1) = 1\<^sub>m n $$ (n - 1, n - 1)

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
have "1\<^sub>m n = A' * IA'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m n = A' * IA'
[PROOF STEP]
unfolding IA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>m n = 1\<^sub>m n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
1\<^sub>m n = A' * IA'

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1\<^sub>m n = A' * IA'

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
have "(A' * IA') $$ (?n, ?n) = row A' ?n \<bullet> col IA' ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A' * IA') $$ (n - 1, n - 1) = row A' (n - 1) \<bullet> col IA' (n - 1)
[PROOF STEP]
using n IA' A'c
[PROOF STATE]
proof (prove)
using this:
n - 1 < n
IA' \<in> carrier_mat n n
A' \<in> carrier_mat n n

goal (1 subgoal):
 1. (A' * IA') $$ (n - 1, n - 1) = row A' (n - 1) \<bullet> col IA' (n - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(A' * IA') $$ (n - 1, n - 1) = row A' (n - 1) \<bullet> col IA' (n - 1)

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A' * IA') $$ (n - 1, n - 1) = row A' (n - 1) \<bullet> col IA' (n - 1)

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
have "row A' ?n = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row A' (n - 1) = 0\<^sub>v n
[PROOF STEP]
unfolding row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n = 0\<^sub>v n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
row A' (n - 1) = 0\<^sub>v n

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row A' (n - 1) = 0\<^sub>v n

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
have "0\<^sub>v n \<bullet> col IA' ?n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<bullet> col IA' (n - 1) = (0::'a)
[PROOF STEP]
using IA' n
[PROOF STATE]
proof (prove)
using this:
IA' \<in> carrier_mat n n
n - 1 < n

goal (1 subgoal):
 1. 0\<^sub>v n \<bullet> col IA' (n - 1) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0\<^sub>v n \<bullet> col IA' (n - 1) = (0::'a)

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(1::'a) = (0::'a)
[PROOF STEP]
have "1 = (0 :: 'a)"
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)

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

goal (2 subgoals):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
 2. 0 < n \<and> row A' (n - 1) = 0\<^sub>v n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(1::'a) = (0::'a)

goal (1 subgoal):
 1. A' = 1\<^sub>m n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A' = 1\<^sub>m n

goal (1 subgoal):
 1. A' = 1\<^sub>m n \<Longrightarrow> A' = 1\<^sub>m n
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A' = 1\<^sub>m n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
gauss_jordan A B = (A', B')
A' = 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A B = (A', B')
A' = 1\<^sub>m n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (gauss_jordan A B) = 1\<^sub>m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_compute_inverse:
  assumes A: "A \<in> carrier_mat n n"
  and res: "gauss_jordan A (1\<^sub>m n) = (1\<^sub>m n, B')"
  shows "A * B' = 1\<^sub>m n" "B' * A = 1\<^sub>m n" "B' \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * B' = 1\<^sub>m n &&& B' * A = 1\<^sub>m n &&& B' \<in> carrier_mat n n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. A * B' = 1\<^sub>m n
 2. B' * A = 1\<^sub>m n
 3. B' \<in> carrier_mat n n
[PROOF STEP]
from gauss_jordan_inverse_one_direction(2)[OF A _ res refl, of n]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>m n \<in> carrier_mat n n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n
[PROOF STEP]
show "A * B' = 1\<^sub>m n" "B' * A = 1\<^sub>m n"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m n \<in> carrier_mat n n \<Longrightarrow> A * B' = 1\<^sub>m n \<and> B' * A = 1\<^sub>m n

goal (1 subgoal):
 1. A * B' = 1\<^sub>m n &&& B' * A = 1\<^sub>m n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A * B' = 1\<^sub>m n
B' * A = 1\<^sub>m n

goal (1 subgoal):
 1. B' \<in> carrier_mat n n
[PROOF STEP]
from gauss_jordan_carrier(2)[OF A _ res, of n]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>m n \<in> carrier_mat n n \<Longrightarrow> B' \<in> carrier_mat n n
[PROOF STEP]
show "B' \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>m n \<in> carrier_mat n n \<Longrightarrow> B' \<in> carrier_mat n n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_jordan_check_invertable: assumes A: "A \<in> carrier_mat n n" and B: "B \<in> carrier_mat n nc"
  shows "(A \<in> Units (ring_mat TYPE('a :: field) n b)) \<longleftrightarrow> fst (gauss_jordan A B) = 1\<^sub>m n"
  (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<in> Units (ring_mat TYPE('a) n b)) = (fst (gauss_jordan A B) = 1\<^sub>m n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b) \<Longrightarrow> fst (gauss_jordan A B) = 1\<^sub>m n
 2. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
assume ?l
[PROOF STATE]
proof (state)
this:
A \<in> Units (ring_mat TYPE('a) n b)

goal (2 subgoals):
 1. A \<in> Units (ring_mat TYPE('a) n b) \<Longrightarrow> fst (gauss_jordan A B) = 1\<^sub>m n
 2. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
by (rule gauss_jordan_inverse_other_direction[OF \<open>?l\<close> B])
[PROOF STATE]
proof (state)
this:
fst (gauss_jordan A B) = 1\<^sub>m n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
let ?g = "gauss_jordan A B"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
fst (gauss_jordan A B) = 1\<^sub>m n

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (gauss_jordan A B) = 1\<^sub>m n
[PROOF STEP]
obtain B' where "?g = (1\<^sub>m n, B')"
[PROOF STATE]
proof (prove)
using this:
fst (gauss_jordan A B) = 1\<^sub>m n

goal (1 subgoal):
 1. (\<And>B'. gauss_jordan A B = (1\<^sub>m n, B') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ?g, auto)
[PROOF STATE]
proof (state)
this:
gauss_jordan A B = (1\<^sub>m n, B')

goal (1 subgoal):
 1. fst (gauss_jordan A B) = 1\<^sub>m n \<Longrightarrow> A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
from gauss_jordan_inverse_one_direction(1)[OF A B this]
[PROOF STATE]
proof (chain)
picking this:
A \<in> Units (ring_mat TYPE('a) n ?b)
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
A \<in> Units (ring_mat TYPE('a) n ?b)

goal (1 subgoal):
 1. A \<in> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A \<in> Units (ring_mat TYPE('a) n b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_inverse: assumes A: "A \<in> carrier_mat n n"
  shows "mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a :: field) n b)"
    "mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)) &&& (mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
let ?one = "1\<^sub>m n"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
obtain BB C where res: "gauss_jordan A ?one = (BB,C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>BB C. gauss_jordan A (1\<^sub>m n) = (BB, C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
gauss_jordan A (1\<^sub>m n) = (BB, C)

goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
gauss_jordan A (1\<^sub>m n) = (BB, C)

goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
assume "mat_inverse A = None"
[PROOF STATE]
proof (state)
this:
mat_inverse A = None

goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
with res
[PROOF STATE]
proof (chain)
picking this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
mat_inverse A = None
[PROOF STEP]
have "BB \<noteq> ?one"
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
mat_inverse A = None

goal (1 subgoal):
 1. BB \<noteq> 1\<^sub>m n
[PROOF STEP]
unfolding mat_inverse_def
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
(if dim_row A = dim_col A then let one = 1\<^sub>m (dim_row A) in case gauss_jordan A one of (B, C) \<Rightarrow> if B = one then Some C else None else None) = None

goal (1 subgoal):
 1. BB \<noteq> 1\<^sub>m n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
(if dim_row A = dim_col A then let one = 1\<^sub>m (dim_row A) in case gauss_jordan A one of (B, C) \<Rightarrow> if B = one then Some C else None else None) = None
A \<in> carrier_mat n n

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

goal (2 subgoals):
 1. mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)
 2. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
thus "A \<notin> Units (ring_mat TYPE('a :: field) n b)"
[PROOF STATE]
proof (prove)
using this:
BB \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. A \<notin> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
using gauss_jordan_check_invertable[OF A, of ?one n] res
[PROOF STATE]
proof (prove)
using this:
BB \<noteq> 1\<^sub>m n
1\<^sub>m n \<in> carrier_mat n n \<Longrightarrow> (A \<in> Units (ring_mat TYPE('a) n ?b)) = (fst (gauss_jordan A (1\<^sub>m n)) = 1\<^sub>m n)
gauss_jordan A (1\<^sub>m n) = (BB, C)

goal (1 subgoal):
 1. A \<notin> Units (ring_mat TYPE('a) n b)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
A \<notin> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mat_inverse A = None \<Longrightarrow> A \<notin> Units (ring_mat TYPE('a) n b)

goal (1 subgoal):
 1. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
assume "mat_inverse A = Some B"
[PROOF STATE]
proof (state)
this:
mat_inverse A = Some B

goal (1 subgoal):
 1. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
with res A
[PROOF STATE]
proof (chain)
picking this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
A \<in> carrier_mat n n
mat_inverse A = Some B
[PROOF STEP]
have "BB = ?one" "C = B"
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
A \<in> carrier_mat n n
mat_inverse A = Some B

goal (1 subgoal):
 1. BB = 1\<^sub>m n &&& C = B
[PROOF STEP]
unfolding mat_inverse_def
[PROOF STATE]
proof (prove)
using this:
gauss_jordan A (1\<^sub>m n) = (BB, C)
A \<in> carrier_mat n n
(if dim_row A = dim_col A then let one = 1\<^sub>m (dim_row A) in case gauss_jordan A one of (B, C) \<Rightarrow> if B = one then Some C else None else None) = Some B

goal (1 subgoal):
 1. BB = 1\<^sub>m n &&& C = B
[PROOF STEP]
by (auto split: if_splits option.splits)
[PROOF STATE]
proof (state)
this:
BB = 1\<^sub>m n
C = B

goal (1 subgoal):
 1. mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
from gauss_jordan_compute_inverse[OF A res[unfolded this]]
[PROOF STATE]
proof (chain)
picking this:
A * B = 1\<^sub>m n
B * A = 1\<^sub>m n
B \<in> carrier_mat n n
[PROOF STEP]
show "A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A * B = 1\<^sub>m n
B * A = 1\<^sub>m n
B \<in> carrier_mat n n

goal (1 subgoal):
 1. A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
mat_inverse A = Some B \<Longrightarrow> A * B = 1\<^sub>m n \<and> B * A = 1\<^sub>m n \<and> B \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_null_space_iarrays_eq:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "basis_null_space_iarrays (matrix_to_iarray A)
  = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [(rank_iarray (matrix_to_iarray A))..<(ncols_iarray (matrix_to_iarray A))])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_null_space_iarrays (matrix_to_iarray A) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding basis_null_space_iarrays_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding matrix_to_iarray_rank[symmetric, of A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank A..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding rank_transpose[symmetric, of A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank (Finite_Cartesian_Product.transpose A)..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding matrix_to_iarray_rank
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [rank_iarray (matrix_to_iarray (Finite_Cartesian_Product.transpose A))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding rank_iarrays_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray (Finite_Cartesian_Product.transpose A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding matrix_to_iarray_transpose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray (Finite_Cartesian_Product.transpose A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding snd_Gauss_Jordan_iarrays_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray (Finite_Cartesian_Product.transpose A)))))..<ncols_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray (Finite_Cartesian_Product.transpose A)))))..<ncols_iarray (matrix_to_iarray A)])
[PROOF STEP]
..


[STATEMENT]
lemma basis_row_space_iarrays_eq:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "basis_row_space_iarrays (matrix_to_iarray A) = set (map (\<lambda>i. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A))) [0..<(rank_iarray (matrix_to_iarray A))])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_row_space_iarrays (matrix_to_iarray A) = set (map (\<lambda>i. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A))) [0..<rank_iarray (matrix_to_iarray A)])
[PROOF STEP]
unfolding basis_row_space_iarrays_def Let_def rank_iarrays_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A))) [0..<length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A))))]) = set (map (\<lambda>i. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A))) [0..<length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (Gauss_Jordan_iarrays (matrix_to_iarray A))))])
[PROOF STEP]
..


[STATEMENT]
lemma basis_left_null_space_iarrays_eq:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "basis_left_null_space_iarrays (matrix_to_iarray A) = basis_null_space_iarrays (transpose_iarray (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_left_null_space_iarrays (matrix_to_iarray A) = basis_null_space_iarrays (transpose_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding basis_left_null_space_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let GJ = Gauss_Jordan_iarrays_PA (matrix_to_iarray A); rank_A = length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd GJ))) in set (map (\<lambda>i. row_iarray i (fst GJ)) [rank_A..<nrows_iarray (matrix_to_iarray A)])) = basis_null_space_iarrays (transpose_iarray (matrix_to_iarray A))
[PROOF STEP]
unfolding basis_null_space_iarrays_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (transpose_iarray (matrix_to_iarray A)))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (transpose_iarray (transpose_iarray (matrix_to_iarray A)))))))..<ncols_iarray (transpose_iarray (matrix_to_iarray A))])
[PROOF STEP]
unfolding matrix_to_iarray_transpose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose A)))))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose (Finite_Cartesian_Product.transpose A)))))))..<ncols_iarray (matrix_to_iarray (Finite_Cartesian_Product.transpose A))])
[PROOF STEP]
unfolding transpose_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols_iarray (matrix_to_iarray (Finite_Cartesian_Product.transpose A))])
[PROOF STEP]
unfolding matrix_to_iarray_ncols[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<ncols (Finite_Cartesian_Product.transpose A)])
[PROOF STEP]
unfolding ncols_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows A])
[PROOF STEP]
unfolding matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)]) = set (map (\<lambda>i. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))) [length (filter (\<lambda>x. \<not> is_zero_iarray x) (IArray.list_of (snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)))))..<nrows_iarray (matrix_to_iarray A)])
[PROOF STEP]
..


[STATEMENT]
lemma vec_to_iarray_basis_null_space[code_unfold]:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows  "vec_to_iarray` (basis_null_space A) = basis_null_space_iarrays (matrix_to_iarray A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray ` basis_null_space A = basis_null_space_iarrays (matrix_to_iarray A)
[PROOF STEP]
proof (unfold basis_null_space_def basis_null_space_iarrays_eq, auto, unfold image_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. rank A \<le> mod_type_class.to_nat i \<Longrightarrow> \<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
 2. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
fix i::'cols
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. rank A \<le> mod_type_class.to_nat i \<Longrightarrow> \<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
 2. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
assume rank_le_i: "rank A \<le> to_nat i"
[PROOF STATE]
proof (state)
this:
rank A \<le> mod_type_class.to_nat i

goal (2 subgoals):
 1. \<And>i. rank A \<le> mod_type_class.to_nat i \<Longrightarrow> \<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
 2. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
show "\<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}.
vec_to_iarray (row i (P_Gauss_Jordan (transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
[PROOF STEP]
proof (rule bexI[of _ "to_nat i"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
 2. mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}
[PROOF STEP]
show "to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}
[PROOF STEP]
unfolding matrix_to_iarray_ncols[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols A}
[PROOF STEP]
using rank_le_i to_nat_less_card[of i]
[PROOF STATE]
proof (prove)
using this:
rank A \<le> mod_type_class.to_nat i
mod_type_class.to_nat i < CARD('cols)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols A}
[PROOF STEP]
unfolding matrix_to_iarray_rank ncols_def
[PROOF STATE]
proof (prove)
using this:
rank_iarray (matrix_to_iarray A) \<le> mod_type_class.to_nat i
mod_type_class.to_nat i < CARD('cols)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<CARD('cols)}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<in> {rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}

goal (1 subgoal):
 1. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
[PROOF STEP]
show "vec_to_iarray (row i (P_Gauss_Jordan (transpose A)))
    = row_iarray (to_nat i) (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))
[PROOF STEP]
unfolding matrix_to_iarray_transpose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
unfolding matrix_to_iarray_fst_Gauss_Jordan_PA[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
unfolding P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A)))) = row_iarray (mod_type_class.to_nat i) (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
unfolding vec_to_iarray_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray (mod_type_class.to_nat i) (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A)))) = row_iarray (mod_type_class.to_nat i) (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray (mod_type_class.to_nat i) (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{rank_iarray (matrix_to_iarray A)..<ncols_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A))) = row_iarray x (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A))))

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
assume rank_le_i: "rank_iarray (matrix_to_iarray A) \<le> i"
        and i_less_nrows: "i < ncols_iarray (matrix_to_iarray A)"
[PROOF STATE]
proof (state)
this:
rank_iarray (matrix_to_iarray A) \<le> i
i < ncols_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
hence i_less_card:"i < CARD ('cols)"
[PROOF STATE]
proof (prove)
using this:
rank_iarray (matrix_to_iarray A) \<le> i
i < ncols_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. i < CARD('cols)
[PROOF STEP]
unfolding matrix_to_iarray_ncols[symmetric] ncols_def
[PROOF STATE]
proof (prove)
using this:
rank_iarray (matrix_to_iarray A) \<le> i
i < CARD('cols)

goal (1 subgoal):
 1. i < CARD('cols)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < CARD('cols)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>rank_iarray (matrix_to_iarray A) \<le> xa; xa < ncols_iarray (matrix_to_iarray A)\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray xa (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
show "\<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (transpose A)) \<and> rank A \<le> to_nat i) \<and>
            row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x
[PROOF STEP]
proof (rule exI[of _ "row (from_nat i) (P_Gauss_Jordan (transpose A))"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>ia. row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) = row ia (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat ia
 2. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))
[PROOF STEP]
show "\<exists>ia. row (from_nat i) (P_Gauss_Jordan (transpose A)) = row ia (P_Gauss_Jordan (transpose A)) \<and>
         rank A \<le> to_nat ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ia. row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) = row ia (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat ia
[PROOF STEP]
by (rule exI[of _ "from_nat i"],simp add: rank_le_i to_nat_from_nat_id[OF i_less_card] matrix_to_iarray_rank)
[PROOF STATE]
proof (state)
this:
\<exists>ia. row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) = row ia (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat ia

goal (1 subgoal):
 1. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))
[PROOF STEP]
show "row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) =
    vec_to_iarray (row (from_nat i) (P_Gauss_Jordan (transpose A)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))
[PROOF STEP]
unfolding matrix_to_iarray_transpose[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray (Finite_Cartesian_Product.transpose A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))
[PROOF STEP]
unfolding matrix_to_iarray_fst_Gauss_Jordan_PA[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))
[PROOF STEP]
unfolding P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
unfolding vec_to_iarray_row to_nat_from_nat_id[OF i_less_card]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A)))) = row_iarray i (matrix_to_iarray (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray (row (mod_type_class.from_nat i) (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. (\<exists>i. x = row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) \<and> rank A \<le> mod_type_class.to_nat i) \<and> row_iarray i (fst (Gauss_Jordan_iarrays_PA (transpose_iarray (matrix_to_iarray A)))) = vec_to_iarray x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_to_iarray_basis_row_space[code_unfold]:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows  "vec_to_iarray` (basis_row_space A) = basis_row_space_iarrays (matrix_to_iarray A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray ` basis_row_space A = basis_row_space_iarrays (matrix_to_iarray A)
[PROOF STEP]
proof (unfold basis_row_space_def basis_row_space_iarrays_eq, auto, unfold image_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))
 2. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))
 2. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
assume i: "row i (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
row i (Gauss_Jordan A) \<noteq> 0

goal (2 subgoals):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))
 2. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
show "\<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))
[PROOF STEP]
proof (rule bexI[of _ "to_nat i"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray (mod_type_class.to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A))
 2. mod_type_class.to_nat i \<in> {0..<rank_iarray (matrix_to_iarray A)}
[PROOF STEP]
show "vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray (to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray (mod_type_class.to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A))
[PROOF STEP]
unfolding vec_to_iarray_row matrix_to_iarray_Gauss_Jordan
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray (mod_type_class.to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A)) = row_iarray (mod_type_class.to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray (mod_type_class.to_nat i) (Gauss_Jordan_iarrays (matrix_to_iarray A))

goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {0..<rank_iarray (matrix_to_iarray A)}
[PROOF STEP]
show "to_nat i \<in> {0..<rank_iarray (matrix_to_iarray A)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i \<in> {0..<rank_iarray (matrix_to_iarray A)}
[PROOF STEP]
by (auto, unfold matrix_to_iarray_rank[symmetric],
      metis (full_types) i iarray_to_vec_vec_to_iarray not_less rank_less_row_i_imp_i_is_zero row_iarray_def vec_matrix vec_to_iarray_row)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<in> {0..<rank_iarray (matrix_to_iarray A)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{0..<rank_iarray (matrix_to_iarray A)}. vec_to_iarray (row i (Gauss_Jordan A)) = row_iarray x (Gauss_Jordan_iarrays (matrix_to_iarray A))

goal (1 subgoal):
 1. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
assume i: "i < rank_iarray (matrix_to_iarray A)"
[PROOF STATE]
proof (state)
this:
i < rank_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
hence i_less_rank: "i < rank A"
[PROOF STATE]
proof (prove)
using this:
i < rank_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. i < rank A
[PROOF STEP]
unfolding matrix_to_iarray_rank
[PROOF STATE]
proof (prove)
using this:
i < rank_iarray (matrix_to_iarray A)

goal (1 subgoal):
 1. i < rank_iarray (matrix_to_iarray A)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i < rank A

goal (1 subgoal):
 1. \<And>xa. xa < rank_iarray (matrix_to_iarray A) \<Longrightarrow> \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray xa (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
show "\<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x
[PROOF STEP]
proof (rule exI[of _ "row (from_nat i) (Gauss_Jordan A)"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>ia. row (mod_type_class.from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0
 2. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))
[PROOF STEP]
have not_zero_i: "\<not> is_zero_row (from_nat i) (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat i) (Gauss_Jordan A)
[PROOF STEP]
proof (unfold is_zero_row_def, rule greatest_ge_nonzero_row')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
 2. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
 3. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
show "reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
[PROOF STEP]
by (metis rref_Gauss_Jordan rref_implies_rref_upt)
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))

goal (2 subgoals):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
 2. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
have A_not_0: "A \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> 0
[PROOF STEP]
using i_less_rank
[PROOF STATE]
proof (prove)
using this:
i < rank A

goal (1 subgoal):
 1. A \<noteq> 0
[PROOF STEP]
by (metis less_nat_zero_code rank_0)
[PROOF STATE]
proof (state)
this:
A \<noteq> 0

goal (2 subgoals):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
 2. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
hence Gauss_not_0: "Gauss_Jordan A \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> 0

goal (1 subgoal):
 1. Gauss_Jordan A \<noteq> 0
[PROOF STEP]
by (metis Gauss_Jordan_not_0)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A \<noteq> 0

goal (2 subgoals):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
 2. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
have "i \<le> to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
[PROOF STEP]
using i_less_rank
[PROOF STATE]
proof (prove)
using this:
i < rank A

goal (1 subgoal):
 1. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
[PROOF STEP]
unfolding rank_eq_suc_to_nat_greatest[OF A_not_0]
[PROOF STATE]
proof (prove)
using this:
i < mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1

goal (1 subgoal):
 1. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (2 subgoals):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
 2. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
thus "from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
using this:
i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
unfolding is_zero_row_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row m (Gauss_Jordan A))
[PROOF STEP]
by (metis leD not_le_imp_less to_nat_le)
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat i \<le> (GREATEST m. \<not> is_zero_row_upt_k m (ncols (Gauss_Jordan A)) (Gauss_Jordan A))

goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
show "\<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
using Gauss_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
unfolding is_zero_row_def[symmetric] is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A \<noteq> 0

goal (1 subgoal):
 1. \<not> (\<forall>a j. Gauss_Jordan A $ a $ j = (0::'a))
[PROOF STEP]
by (metis vec_eq_iff zero_index)
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat i) (Gauss_Jordan A)

goal (2 subgoals):
 1. \<exists>ia. row (mod_type_class.from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0
 2. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))
[PROOF STEP]
have i_less_card: "i<CARD('rows)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
using i_less_rank rank_le_nrows[of A]
[PROOF STATE]
proof (prove)
using this:
i < rank A
rank A \<le> nrows A

goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
i < rank A
rank A \<le> CARD('rows)

goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < CARD('rows)

goal (2 subgoals):
 1. \<exists>ia. row (mod_type_class.from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0
 2. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))
[PROOF STEP]
show "\<exists>ia. row (from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ia. row (mod_type_class.from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
apply (rule exI[of _ "from_nat i"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (mod_type_class.from_nat i) (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
using not_zero_i
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat i) (Gauss_Jordan A)

goal (1 subgoal):
 1. row (mod_type_class.from_nat i) (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
unfolding row_def is_zero_row_def' vec_nth_inverse
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. Gauss_Jordan A $ mod_type_class.from_nat i $ j = (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan A $ mod_type_class.from_nat i \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ia. row (mod_type_class.from_nat i) (Gauss_Jordan A) = row ia (Gauss_Jordan A) \<and> row ia (Gauss_Jordan A) \<noteq> 0

goal (1 subgoal):
 1. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))
[PROOF STEP]
show "row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (from_nat i) (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))
[PROOF STEP]
unfolding matrix_to_iarray_Gauss_Jordan[symmetric] vec_to_iarray_row to_nat_from_nat_id[OF i_less_card]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_iarray i (matrix_to_iarray (Gauss_Jordan A)) = row_iarray i (matrix_to_iarray (Gauss_Jordan A))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray (row (mod_type_class.from_nat i) (Gauss_Jordan A))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. (\<exists>i. x = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0) \<and> row_iarray i (Gauss_Jordan_iarrays (matrix_to_iarray A)) = vec_to_iarray x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unfold_lesub_prod: "x \<sqsubseteq>(r\<^sub>A,r\<^sub>B) y = le r\<^sub>A r\<^sub>B x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x <=(r\<^sub>A,r\<^sub>B) y) = Product.le r\<^sub>A r\<^sub>B x y
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x <=(r\<^sub>A,r\<^sub>B) y) = Product.le r\<^sub>A r\<^sub>B x y
[PROOF STEP]
by (simp add: lesub_def)


[STATEMENT]
lemma le_prod_Pair_conv [iff]: "((a\<^sub>1,b\<^sub>1) \<sqsubseteq>(r\<^sub>A,r\<^sub>B) (a\<^sub>2,b\<^sub>2)) = (a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 & b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a\<^sub>1, b\<^sub>1) <=(r\<^sub>A,r\<^sub>B) (a\<^sub>2, b\<^sub>2)) = (a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a\<^sub>1, b\<^sub>1) <=(r\<^sub>A,r\<^sub>B) (a\<^sub>2, b\<^sub>2)) = (a\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>A\<^esub> a\<^sub>2 \<and> b\<^sub>1 \<sqsubseteq>\<^bsub>r\<^sub>B\<^esub> b\<^sub>2)
[PROOF STEP]
by (simp add: lesub_def le_def)