[STATEMENT]
lemma id_upt_k_Gauss_Jordan:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A"
shows "id_upt_k (Gauss_Jordan A) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_upt_k (Gauss_Jordan A) k
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. id_upt_k (Gauss_Jordan A) 0
 2. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. id_upt_k (Gauss_Jordan A) 0
 2. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_upt_k (Gauss_Jordan A) 0
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. mod_type_class.to_nat i < 0 \<and> mod_type_class.to_nat j < 0 \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
id_upt_k (Gauss_Jordan A) 0

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
note id_k=Suc.hyps
[PROOF STATE]
proof (state)
this:
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
have rref_k: "reduced_row_echelon_form_upt_k (Gauss_Jordan A) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) k
[PROOF STEP]
using rref_implies_rref_upt[OF rref_Gauss_Jordan]
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k (Gauss_Jordan ?A1) ?k

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
have rref_suc_k: "reduced_row_echelon_form_upt_k (Gauss_Jordan A) (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
using rref_implies_rref_upt[OF rref_Gauss_Jordan]
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k (Gauss_Jordan ?A1) ?k

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k (Gauss_Jordan A) (Suc k)

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
have inv_gj: "invertible (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (Gauss_Jordan A)
[PROOF STEP]
by (metis inv_A invertible_Gauss_Jordan invertible_mult)
[PROOF STATE]
proof (state)
this:
invertible (Gauss_Jordan A)

goal (1 subgoal):
 1. \<And>k. id_upt_k (Gauss_Jordan A) k \<Longrightarrow> id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
show "id_upt_k (Gauss_Jordan A) (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_upt_k (Gauss_Jordan A) (Suc k)
[PROOF STEP]
proof (unfold id_upt_k_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
fix j::'n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
assume j_less_suc: "to_nat j < Suc k"
\<comment> \<open>First of all we prove a property which will be useful later\<close>
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < Suc k

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have greatest_prop: "j \<noteq> 0 \<Longrightarrow> to_nat j = k \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)
[PROOF STEP]
proof (rule Greatest_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k\<rbrakk> \<Longrightarrow> \<not> is_zero_row_upt_k (j - (1::'n)) k (Gauss_Jordan A)
 2. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
assume j_not_zero: "j \<noteq> 0" and j_eq_k: "to_nat j = k"
[PROOF STATE]
proof (state)
this:
j \<noteq> (0::'n)
mod_type_class.to_nat j = k

goal (2 subgoals):
 1. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k\<rbrakk> \<Longrightarrow> \<not> is_zero_row_upt_k (j - (1::'n)) k (Gauss_Jordan A)
 2. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
have j_minus_1: "to_nat (j - 1) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (j - (1::'n)) < k
[PROOF STEP]
by (metis (full_types) Suc_le' diff_add_cancel j_eq_k j_not_zero to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (j - (1::'n)) < k

goal (2 subgoals):
 1. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k\<rbrakk> \<Longrightarrow> \<not> is_zero_row_upt_k (j - (1::'n)) k (Gauss_Jordan A)
 2. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
show "\<not> is_zero_row_upt_k (j - 1) k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (j - (1::'n)) k (Gauss_Jordan A)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>ja. mod_type_class.to_nat ja < k \<longrightarrow> Gauss_Jordan A $ (j - (1::'n)) $ ja = (0::'a))
[PROOF STEP]
proof (auto, rule exI[of _ "j - 1"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat (j - (1::'n)) < k
 2. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
show "to_nat (j - 1) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (j - (1::'n)) < k
[PROOF STEP]
using j_minus_1
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (j - (1::'n)) < k

goal (1 subgoal):
 1. mod_type_class.to_nat (j - (1::'n)) < k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (j - (1::'n)) < k

goal (1 subgoal):
 1. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
show "Gauss_Jordan A $ (j - 1) $ (j - 1) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
using id_k
[PROOF STATE]
proof (prove)
using this:
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
using j_minus_1
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))
mod_type_class.to_nat (j - (1::'n)) < k

goal (1 subgoal):
 1. Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ (j - (1::'n)) $ (j - (1::'n)) \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (j - (1::'n)) k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
fix a::'n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
assume not_zero_a: "\<not> is_zero_row_upt_k a k (Gauss_Jordan A)"
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k a k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<And>y. \<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k; \<not> is_zero_row_upt_k y k (Gauss_Jordan A)\<rbrakk> \<Longrightarrow> y \<le> j - (1::'n)
[PROOF STEP]
show "a \<le> j - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> j - (1::'n)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> j - (1::'n) \<Longrightarrow> False
[PROOF STEP]
assume " \<not> a \<le> j - 1"
[PROOF STATE]
proof (state)
this:
\<not> a \<le> j - (1::'n)

goal (1 subgoal):
 1. \<not> a \<le> j - (1::'n) \<Longrightarrow> False
[PROOF STEP]
hence a_greater_i_minus_1: "a > j - 1"
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> j - (1::'n)

goal (1 subgoal):
 1. j - (1::'n) < a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j - (1::'n) < a

goal (1 subgoal):
 1. \<not> a \<le> j - (1::'n) \<Longrightarrow> False
[PROOF STEP]
have "is_zero_row_upt_k a k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k a k (Gauss_Jordan A)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
fix b::'n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
assume a: "to_nat b < k"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat b < k

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
have Least_eq: "(LEAST n. Gauss_Jordan A $ b $ n \<noteq> 0) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan A $ b $ b \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan A $ b $ y \<noteq> (0::'a) \<Longrightarrow> b \<le> y
[PROOF STEP]
show "Gauss_Jordan A $ b $ b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ b $ b \<noteq> (0::'a)
[PROOF STEP]
by (metis a id_k id_upt_k_def zero_neq_one)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ b $ b \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ b $ y \<noteq> (0::'a) \<Longrightarrow> b \<le> y
[PROOF STEP]
show "\<And>y. Gauss_Jordan A $ b $ y \<noteq> 0 \<Longrightarrow> b \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ b $ y \<noteq> (0::'a) \<Longrightarrow> b \<le> y
[PROOF STEP]
by (metis (opaque_lifting, no_types) a not_less_iff_gr_or_eq id_k id_upt_k_def less_trans not_less to_nat_mono)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ b $ ?y \<noteq> (0::'a) \<Longrightarrow> b \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
have "\<not> is_zero_row_upt_k b k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k b k (Gauss_Jordan A)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan A $ b $ j = (0::'a))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. mod_type_class.to_nat j < k \<and> Gauss_Jordan A $ b $ j \<noteq> (0::'a)
[PROOF STEP]
apply (rule exI[of _ b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat b < k \<and> Gauss_Jordan A $ b $ b \<noteq> (0::'a)
[PROOF STEP]
using a id_k
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat b < k
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. mod_type_class.to_nat b < k \<and> Gauss_Jordan A $ b $ b \<noteq> (0::'a)
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat b < k
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))

goal (1 subgoal):
 1. mod_type_class.to_nat b < k \<and> Gauss_Jordan A $ b $ b \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k b k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k b k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
have "a \<noteq> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
have "b < from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b < mod_type_class.from_nat k
[PROOF STEP]
by (metis a from_nat_to_nat_id j_eq_k not_less_iff_gr_or_eq to_nat_le)
[PROOF STATE]
proof (state)
this:
b < mod_type_class.from_nat k

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
b < mod_type_class.from_nat k

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
have "... = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
using j_eq_k to_nat_from_nat
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j = k
mod_type_class.to_nat ?j = ?k \<Longrightarrow> mod_type_class.from_nat ?k = ?j

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

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = j

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
have "... \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> a
[PROOF STEP]
using a_greater_i_minus_1
[PROOF STATE]
proof (prove)
using this:
j - (1::'n) < a

goal (1 subgoal):
 1. j \<le> a
[PROOF STEP]
by (metis diff_add_cancel le_Suc)
[PROOF STATE]
proof (state)
this:
j \<le> a

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
b < a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b < a

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. \<And>j. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ a $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b
\<not> is_zero_row_upt_k b k (Gauss_Jordan A)
a \<noteq> b
[PROOF STEP]
show "Gauss_Jordan A $ a $ b = 0"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b
\<not> is_zero_row_upt_k b k (Gauss_Jordan A)
a \<noteq> b

goal (1 subgoal):
 1. Gauss_Jordan A $ a $ b = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref_k]
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ b $ n \<noteq> (0::'a)) = b
\<not> is_zero_row_upt_k b k (Gauss_Jordan A)
a \<noteq> b
\<forall>i. \<not> is_zero_row_upt_k i k (Gauss_Jordan A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) = (0::'a))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k a k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> a \<le> j - (1::'n) \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k a k (Gauss_Jordan A)

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_zero_a
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k a k (Gauss_Jordan A)
\<not> is_zero_row_upt_k a k (Gauss_Jordan A)

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<le> j - (1::'n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>j \<noteq> (0::'n); mod_type_class.to_nat j = k\<rbrakk> \<Longrightarrow> (GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)

goal (2 subgoals):
 1. \<And>j. mod_type_class.to_nat j < Suc k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
show Gauss_jj_1: "Gauss_Jordan A $ j $ j = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
proof (cases "j=0")
\<comment> \<open>In case that j be zero, the result is trivial\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j = (0::'n)

goal (2 subgoals):
 1. j = (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
proof (unfold True, rule rref_first_element)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. reduced_row_echelon_form (Gauss_Jordan A)
 2. column (0::'n) (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
show "reduced_row_echelon_form (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form (Gauss_Jordan A)
[PROOF STEP]
by (rule rref_Gauss_Jordan)
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form (Gauss_Jordan A)

goal (1 subgoal):
 1. column (0::'n) (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
show "column 0 (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (0::'n) (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
by (metis det_zero_column inv_gj invertible_det_nz)
[PROOF STATE]
proof (state)
this:
column (0::'n) (Gauss_Jordan A) \<noteq> 0

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

goal (1 subgoal):
 1. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<noteq> (0::'n)

goal (1 subgoal):
 1. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
note j_not_zero = False
[PROOF STATE]
proof (state)
this:
j \<noteq> (0::'n)

goal (1 subgoal):
 1. j \<noteq> (0::'n) \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
proof (cases "to_nat j < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < k

goal (2 subgoals):
 1. mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
 2. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
using id_k
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < k
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < k
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
by presburger  \<comment> \<open>Easy due to the inductive hypothesis\<close>
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j = (1::'a)

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat j < k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
hence j_eq_k: "to_nat j = k"
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat j < k

goal (1 subgoal):
 1. mod_type_class.to_nat j = k
[PROOF STEP]
using j_less_suc
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat j < k
mod_type_class.to_nat j < Suc k

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
have j_minus_1: "to_nat (j - 1) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (j - (1::'n)) < k
[PROOF STEP]
by (metis (full_types) Suc_le' diff_add_cancel j_eq_k j_not_zero to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (j - (1::'n)) < k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
have "(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)
[PROOF STEP]
by (rule greatest_prop[OF j_not_zero j_eq_k])
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
hence zero_j_k: "is_zero_row_upt_k j k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)

goal (1 subgoal):
 1. is_zero_row_upt_k j k (Gauss_Jordan A)
[PROOF STEP]
by (metis not_le greatest_ge_nonzero_row j_eq_k j_minus_1 to_nat_mono')
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j = (1::'a)
[PROOF STEP]
proof (rule ccontr, cases "Gauss_Jordan A $ j $ j = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note gauss_jj_not_0 = False
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume gauss_jj_not_1: "Gauss_Jordan A $ j $ j \<noteq> 1"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (1::'a)

goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(LEAST n. Gauss_Jordan A $ j $ n \<noteq> 0) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "Gauss_Jordan A $ j $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
[PROOF STEP]
using gauss_jj_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "\<And>y. Gauss_Jordan A $ j $ y \<noteq> 0 \<Longrightarrow> j \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
by (metis le_less_linear is_zero_row_upt_k_def j_eq_k to_nat_mono zero_j_k)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ ?y \<noteq> (0::'a) \<Longrightarrow> j \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ j $ n \<noteq> 0) \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) \<noteq> (1::'a)
[PROOF STEP]
using gauss_jj_not_1
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
Gauss_Jordan A $ j $ j \<noteq> (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) \<noteq> (1::'a)
[PROOF STEP]
by auto \<comment> \<open>Contradiction with the second condition of rref\<close>
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) \<noteq> (1::'a)

goal (2 subgoals):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) \<noteq> (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis gauss_jj_not_0 is_zero_row_upt_k_def j_eq_k lessI rref_suc_k rref_upt_condition2)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j = (0::'a)

goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note gauss_jj_0 = True
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j = (0::'a)

goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have zero_j_suc_k: "is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)
[PROOF STEP]
by (rule is_zero_row_upt_k_suc[OF zero_j_k], metis gauss_jj_0 j_eq_k to_nat_from_nat)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)

goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<not> (\<exists>B. B ** (Gauss_Jordan A) = mat 1)" \<comment> \<open>This will be a contradiction\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>B. B ** Gauss_Jordan A = mat (1::'a)
[PROOF STEP]
proof (unfold matrix_left_invertible_independent_columns, simp,
                        rule exI[of _ "\<lambda>i. (if i < j then column j (Gauss_Jordan A) $ i else if i=j then -1 else 0)"], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i\<in>UNIV. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) *s column i (Gauss_Jordan A)) = 0
 2. \<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
show "(\<Sum>i\<in>UNIV. (if i < j then column j (Gauss_Jordan A) $ i else if i=j then -1 else 0) *s column i (Gauss_Jordan A)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>UNIV. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) *s column i (Gauss_Jordan A)) = 0
[PROOF STEP]
proof (unfold vec_eq_iff sum_component, auto)
                          \<comment> \<open>We write the column j in a linear combination of the previous ones, which is a contradiction (the matrix wouldn't be invertible)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
let ?f="\<lambda>i. (if i < j then column j (Gauss_Jordan A) $ i else if i=j then -1 else 0)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
let ?g="(\<lambda>x. ?f x * column x (Gauss_Jordan A) $ i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
show "sum ?g UNIV = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
proof (cases "i<j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
note i_less_j = True
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have sum_rw: "sum ?g (UNIV - {i}) = ?g j + sum ?g ((UNIV - {i}) - {j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)
[PROOF STEP]
proof (rule sum.remove)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (UNIV - {i})
 2. j \<in> UNIV - {i}
[PROOF STEP]
show "finite (UNIV - {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (UNIV - {i})
[PROOF STEP]
using finite_code
[PROOF STATE]
proof (prove)
using this:
finite ?A = True

goal (1 subgoal):
 1. finite (UNIV - {i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (UNIV - {i})

goal (1 subgoal):
 1. j \<in> UNIV - {i}
[PROOF STEP]
show "j \<in> UNIV - {i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<in> UNIV - {i}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. j \<in> UNIV - {i}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<in> UNIV - {i}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have sum_g0: "sum ?g (UNIV - {i} - {j}) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x \<noteq> i; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x \<noteq> i; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
assume a_not_j: "a \<noteq> j" and a_not_i: "a \<noteq> i" and a_less_j: "a < j" and column_a_not_zero: "column a (Gauss_Jordan A) $ i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
a \<noteq> j
a \<noteq> i
a < j
column a (Gauss_Jordan A) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x \<noteq> i; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
have "Gauss_Jordan A $ i $ a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
using id_k
[PROOF STATE]
proof (prove)
using this:
id_upt_k (Gauss_Jordan A) k

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
using a_less_j j_eq_k
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))
a < j
mod_type_class.to_nat j = k

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
using i_less_j a_not_i to_nat_mono
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))
a < j
mod_type_class.to_nat j = k
i < j
a \<noteq> i
?a < ?b \<Longrightarrow> mod_type_class.to_nat ?a < mod_type_class.to_nat ?b

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x \<noteq> i; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
thus "column j (Gauss_Jordan A) $ a = 0"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)

goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ a = (0::'a)
[PROOF STEP]
using column_a_not_zero
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)
column a (Gauss_Jordan A) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ a = (0::'a)
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)
(\<chi>i. Gauss_Jordan A $ i $ a) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<chi>i. Gauss_Jordan A $ i $ j) $ a = (0::'a)
[PROOF STEP]
by simp \<comment> \<open>Contradiction\<close>
[PROOF STATE]
proof (state)
this:
column j (Gauss_Jordan A) $ a = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have "sum ?g UNIV = ?g i + sum ?g (UNIV - {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)
[PROOF STEP]
by (rule sum.remove, simp_all)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have "... = ?g i + ?g j + sum ?g (UNIV - {i} - {j})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)
[PROOF STEP]
unfolding sum_rw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + ((if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have "... = ?g i + ?g j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i
[PROOF STEP]
unfolding sum_g0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (0::'a) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i + (\<Sum>x\<in>UNIV - {i} - {j}. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i = (0::'a)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i = (0::'a)
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (if i < j then (\<chi>i. Gauss_Jordan A $ i $ j) $ i else if i = j then - (1::'a) else (0::'a)) * (\<chi>ia. Gauss_Jordan A $ ia $ i) $ i + (if j < j then (\<chi>i. Gauss_Jordan A $ i $ j) $ j else if j = j then - (1::'a) else (0::'a)) * (\<chi>i. Gauss_Jordan A $ i $ j) $ i = (0::'a)
[PROOF STEP]
by (simp, metis id_k id_upt_k_def j_eq_k to_nat_mono)
[PROOF STATE]
proof (state)
this:
(if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) * column i (Gauss_Jordan A) $ i + (if j < j then column j (Gauss_Jordan A) $ j else if j = j then - (1::'a) else (0::'a)) * column j (Gauss_Jordan A) $ i = (0::'a)

goal (2 subgoals):
 1. i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
 2. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
have zero_i_suc_k: "is_zero_row_upt_k i (Suc k) (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) (Gauss_Jordan A)
[PROOF STEP]
by (metis False zero_j_suc_k linorder_cases rref_suc_k rref_upt_condition1)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i (Suc k) (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. column j (Gauss_Jordan A) $ i = (0::'a)
 2. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
show "column j (Gauss_Jordan A) $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ i = (0::'a)
[PROOF STEP]
using zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) (Gauss_Jordan A)

goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ i = (0::'a)
[PROOF STEP]
unfolding column_def is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)

goal (1 subgoal):
 1. (\<chi>i. Gauss_Jordan A $ i $ j) $ i = (0::'a)
[PROOF STEP]
by (metis j_eq_k lessI vec_lambda_beta)
[PROOF STATE]
proof (state)
this:
column j (Gauss_Jordan A) $ i = (0::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
assume a_not_j: "a \<noteq> j" and a_less_j: "a < j" and column_a_i: "column a (Gauss_Jordan A) $ i \<noteq> 0"
[PROOF STATE]
proof (state)
this:
a \<noteq> j
a < j
column a (Gauss_Jordan A) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
have "Gauss_Jordan A $ i $ a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
using zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) (Gauss_Jordan A)

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a = (0::'a)
[PROOF STEP]
by (metis (full_types) a_less_j j_eq_k less_SucI to_nat_mono)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ i $ a = (0::'a)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> j; x < j; column x (Gauss_Jordan A) $ i \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> column j (Gauss_Jordan A) $ x = (0::'a)
[PROOF STEP]
thus "column j (Gauss_Jordan A) $ a = 0"
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)

goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ a = (0::'a)
[PROOF STEP]
using column_a_i
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)
column a (Gauss_Jordan A) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. column j (Gauss_Jordan A) $ a = (0::'a)
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ i $ a = (0::'a)
(\<chi>i. Gauss_Jordan A $ i $ a) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<chi>i. Gauss_Jordan A $ i $ j) $ a = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
column j (Gauss_Jordan A) $ a = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>UNIV. (if x < j then column j (Gauss_Jordan A) $ x else if x = j then - (1::'a) else (0::'a)) * column x (Gauss_Jordan A) $ i) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>UNIV. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) *s column i (Gauss_Jordan A)) = 0

goal (1 subgoal):
 1. \<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
show "\<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then -1 else 0) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by (metis False j_eq_k neg_equal_0_iff_equal to_nat_mono zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<exists>i. (if i < j then column j (Gauss_Jordan A) $ i else if i = j then - (1::'a) else (0::'a)) \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nexists>B. B ** Gauss_Jordan A = mat (1::'a)

goal (1 subgoal):
 1. \<lbrakk>Gauss_Jordan A $ j $ j \<noteq> (1::'a); Gauss_Jordan A $ j $ j = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<nexists>B. B ** Gauss_Jordan A = mat (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using inv_gj
[PROOF STATE]
proof (prove)
using this:
\<nexists>B. B ** Gauss_Jordan A = mat (1::'a)
invertible (Gauss_Jordan A)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding invertible_def
[PROOF STATE]
proof (prove)
using this:
\<nexists>B. B ** Gauss_Jordan A = mat (1::'a)
\<exists>A'. Gauss_Jordan A ** A' = mat (1::'a) \<and> A' ** Gauss_Jordan A = mat (1::'a)

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

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

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

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
fix i::'n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
assume i_less_suc: "to_nat i < Suc k" and i_not_j: "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < Suc k
i \<noteq> j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>mod_type_class.to_nat i < Suc k; mod_type_class.to_nat j < Suc k; i \<noteq> j\<rbrakk> \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
show "Gauss_Jordan A $ i $ j = 0" \<comment> \<open>This result is proved making use of the 4th condition of rref\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
proof (cases "to_nat i < k \<and> to_nat j < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
using id_k i_not_j
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k
id_upt_k (Gauss_Jordan A) k
i \<noteq> j

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
unfolding id_upt_k_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k
\<forall>i j. mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k \<longrightarrow> (i = j \<longrightarrow> Gauss_Jordan A $ i $ j = (1::'a)) \<and> (i \<noteq> j \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a))
i \<noteq> j

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
by blast \<comment> \<open>Easy due to the inductive hypothesis\<close>
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ i $ j = (0::'a)

goal (1 subgoal):
 1. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k)

goal (1 subgoal):
 1. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
note i_or_j_ge_k = False
[PROOF STATE]
proof (state)
this:
\<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k)

goal (1 subgoal):
 1. \<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k) \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
proof (cases "to_nat i < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < k

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
hence j_eq_k: "to_nat j = k"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k

goal (1 subgoal):
 1. mod_type_class.to_nat j = k
[PROOF STEP]
using i_or_j_ge_k j_less_suc
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < k
\<not> (mod_type_class.to_nat i < k \<and> mod_type_class.to_nat j < k)
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. mod_type_class.to_nat j = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j = k

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have j_noteq_0: "j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<noteq> (0::'n)
[PROOF STEP]
by (metis True j_eq_k less_nat_zero_code to_nat_0)
[PROOF STATE]
proof (state)
this:
j \<noteq> (0::'n)

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have j_minus_1: "to_nat (j - 1) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (j - (1::'n)) < k
[PROOF STEP]
by (metis (full_types) Suc_le' diff_add_cancel j_eq_k j_noteq_0 to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (j - (1::'n)) < k

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have "(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)
[PROOF STEP]
by (rule greatest_prop[OF j_noteq_0 j_eq_k])
[PROOF STATE]
proof (state)
this:
(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
hence zero_j_k: "is_zero_row_upt_k j k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST m. \<not> is_zero_row_upt_k m k (Gauss_Jordan A)) = j - (1::'n)

goal (1 subgoal):
 1. is_zero_row_upt_k j k (Gauss_Jordan A)
[PROOF STEP]
by (metis (lifting, mono_tags) less_linear less_asym j_eq_k j_minus_1 not_greater_Greatest to_nat_mono)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k j k (Gauss_Jordan A)

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have Least_eq_j: "(LEAST n. Gauss_Jordan A $ j $ n \<noteq> 0) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "Gauss_Jordan A $ j $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
[PROOF STEP]
using Gauss_jj_1
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A $ j $ j = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "\<And>y. Gauss_Jordan A $ j $ y \<noteq> 0 \<Longrightarrow> j \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
by (metis True le_cases from_nat_to_nat_id i_or_j_ge_k is_zero_row_upt_k_def j_less_suc less_Suc_eq_le less_le to_nat_le zero_j_k)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ ?y \<noteq> (0::'a) \<Longrightarrow> j \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have "\<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>ja. mod_type_class.to_nat ja < Suc k \<longrightarrow> Gauss_Jordan A $ j $ ja = (0::'a))
[PROOF STEP]
by (metis Gauss_jj_1 j_less_suc zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)

goal (2 subgoals):
 1. mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref_suc_k] i_not_j
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j (Suc k) (Gauss_Jordan A)
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) (Gauss_Jordan A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) = (0::'a))
i \<noteq> j

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat i < k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
hence i_eq_k: "to_nat i = k"
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat i < k

goal (1 subgoal):
 1. mod_type_class.to_nat i = k
[PROOF STEP]
by (metis \<open>to_nat i < Suc k\<close> less_SucE)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i = k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
hence j_less_k: "to_nat j < k"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i = k

goal (1 subgoal):
 1. mod_type_class.to_nat j < k
[PROOF STEP]
by (metis i_not_j j_less_suc less_SucE to_nat_from_nat)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have "(LEAST n. Gauss_Jordan A $ j $ n \<noteq> 0) = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "Gauss_Jordan A $ j $ j \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ j $ j \<noteq> (0::'a)
[PROOF STEP]
by (metis Gauss_jj_1 zero_neq_one)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ j \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
show "\<And>y. Gauss_Jordan A $ j $ y \<noteq> 0 \<Longrightarrow> j \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan A $ j $ y \<noteq> (0::'a) \<Longrightarrow> j \<le> y
[PROOF STEP]
by (metis le_cases id_k id_upt_k_def j_less_k less_trans not_less to_nat_mono)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ j $ ?y \<noteq> (0::'a) \<Longrightarrow> j \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
have "\<not> is_zero_row_upt_k j k (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k j k (Gauss_Jordan A)
[PROOF STEP]
by (metis (full_types) Gauss_jj_1 is_zero_row_upt_k_def j_less_k zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k j k (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat i < k \<Longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j k (Gauss_Jordan A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j k (Gauss_Jordan A)

goal (1 subgoal):
 1. Gauss_Jordan A $ i $ j = (0::'a)
[PROOF STEP]
using rref_upt_condition4[OF rref_k] i_not_j
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ j $ n \<noteq> (0::'a)) = j
\<not> is_zero_row_upt_k j k (Gauss_Jordan A)
\<forall>i. \<not> is_zero_row_upt_k i k (Gauss_Jordan A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> Gauss_Jordan A $ j $ (LEAST n. Gauss_Jordan A $ i $ n \<noteq> (0::'a)) = (0::'a))
i \<noteq> j

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
id_upt_k (Gauss_Jordan A) (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invertible_implies_rref_id:
  fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
  assumes inv_A: "invertible A"
  shows "Gauss_Jordan A = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A = mat (1::'a)
[PROOF STEP]
using id_upt_k_Gauss_Jordan[OF inv_A, of "nrows (Gauss_Jordan A)"]
[PROOF STATE]
proof (prove)
using this:
id_upt_k (Gauss_Jordan A) (nrows (Gauss_Jordan A))

goal (1 subgoal):
 1. Gauss_Jordan A = mat (1::'a)
[PROOF STEP]
using id_upt_nrows_mat_1
[PROOF STATE]
proof (prove)
using this:
id_upt_k (Gauss_Jordan A) (nrows (Gauss_Jordan A))
id_upt_k ?A (nrows ?A) \<Longrightarrow> ?A = mat (1::?'a)

goal (1 subgoal):
 1. Gauss_Jordan A = mat (1::'a)
[PROOF STEP]
by fast


[STATEMENT]
lemma matrix_inv_Gauss:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A" and Gauss_eq: "Gauss_Jordan A = P ** A"
shows "matrix_inv A = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv A = P
[PROOF STEP]
proof (unfold matrix_inv_def, rule some1_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>!A'. A ** A' = mat (1::'a) \<and> A' ** A = mat (1::'a)
 2. A ** P = mat (1::'a) \<and> P ** A = mat (1::'a)
[PROOF STEP]
show "\<exists>!A'. A ** A' = mat 1 \<and> A' ** A = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!A'. A ** A' = mat (1::'a) \<and> A' ** A = mat (1::'a)
[PROOF STEP]
by (metis inv_A invertible_def matrix_inv_unique matrix_left_right_inverse)
[PROOF STATE]
proof (state)
this:
\<exists>!A'. A ** A' = mat (1::'a) \<and> A' ** A = mat (1::'a)

goal (1 subgoal):
 1. A ** P = mat (1::'a) \<and> P ** A = mat (1::'a)
[PROOF STEP]
show "A ** P = mat 1 \<and> P ** A = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ** P = mat (1::'a) \<and> P ** A = mat (1::'a)
[PROOF STEP]
by (metis Gauss_eq inv_A invertible_implies_rref_id matrix_left_right_inverse)
[PROOF STATE]
proof (state)
this:
A ** P = mat (1::'a) \<and> P ** A = mat (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_inv_Gauss_Jordan_PA:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes inv_A: "invertible A"
shows "matrix_inv A = fst (Gauss_Jordan_PA A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_inv A = fst (Gauss_Jordan_PA A)
[PROOF STEP]
by (metis Gauss_Jordan_PA_eq fst_Gauss_Jordan_PA inv_A matrix_inv_Gauss)


[STATEMENT]
lemma invertible_eq_full_rank[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "invertible A = (rank A = nrows A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible A = (rank A = nrows A)
[PROOF STEP]
by (metis full_rank_implies_invertible invertible_implies_full_rank)


[STATEMENT]
lemma the_inverse_matrix:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes "invertible A"
shows "the (inverse_matrix A) = P_Gauss_Jordan A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (inverse_matrix A) = P_Gauss_Jordan A
[PROOF STEP]
by (metis P_Gauss_Jordan_def assms inverse_matrix_def matrix_inv_Gauss_Jordan_PA option.sel)


[STATEMENT]
lemma inverse_matrix:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "inverse_matrix A = (if invertible A then Some (P_Gauss_Jordan A) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_matrix A = (if invertible A then Some (P_Gauss_Jordan A) else None)
[PROOF STEP]
by (metis inverse_matrix_def option.sel the_inverse_matrix)


[STATEMENT]
lemma inverse_matrix_code[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "inverse_matrix A = (let GJ = Gauss_Jordan_PA A;
                                rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1) in
                                if nrows A = rank_A then Some (fst(GJ)) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse_matrix A = (let GJ = Gauss_Jordan_PA A; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1 in if nrows A = rank_A then Some (fst GJ) else None)
[PROOF STEP]
unfolding inverse_matrix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if invertible A then Some (P_Gauss_Jordan A) else None) = (let GJ = Gauss_Jordan_PA A; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1 in if nrows A = rank_A then Some (fst GJ) else None)
[PROOF STEP]
unfolding invertible_eq_full_rank
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if rank A = nrows A then Some (P_Gauss_Jordan A) else None) = (let GJ = Gauss_Jordan_PA A; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1 in if nrows A = rank_A then Some (fst GJ) else None)
[PROOF STEP]
unfolding rank_Gauss_Jordan_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1) = nrows A then Some (P_Gauss_Jordan A) else None) = (let GJ = Gauss_Jordan_PA A; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1 in if nrows A = rank_A then Some (fst GJ) else None)
[PROOF STEP]
unfolding P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1) = nrows A then Some (fst (Gauss_Jordan_PA A)) else None) = (let GJ = Gauss_Jordan_PA A; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ) \<noteq> 0) + 1 in if nrows A = rank_A then Some (fst GJ) else None)
[PROOF STEP]
unfolding Let_def Gauss_Jordan_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) = nrows A then Some (fst (Gauss_Jordan_PA A)) else None) = (if nrows A = (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) then Some (fst (Gauss_Jordan_PA A)) else None)
[PROOF STEP]
by presburger


[STATEMENT]
lemma at_least_two_cars_exists:"\<exists>c d ::cars . c\<noteq>d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c d. c \<noteq> d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c d. c \<noteq> d
[PROOF STEP]
have "(0::nat) \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<noteq> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<noteq> 1

goal (1 subgoal):
 1. \<exists>c d. c \<noteq> d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<noteq> 1
[PROOF STEP]
have "Abs_cars (0::nat) \<noteq> Abs_cars(1) "
[PROOF STATE]
proof (prove)
using this:
0 \<noteq> 1

goal (1 subgoal):
 1. Abs_cars 0 \<noteq> Abs_cars 1
[PROOF STEP]
by (simp add:Abs_cars_inject)
[PROOF STATE]
proof (state)
this:
Abs_cars 0 \<noteq> Abs_cars 1

goal (1 subgoal):
 1. \<exists>c d. c \<noteq> d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Abs_cars 0 \<noteq> Abs_cars 1

goal (1 subgoal):
 1. \<exists>c d. c \<noteq> d
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c d. c \<noteq> d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_cars:"infinite {c::cars . True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {c. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {c. True}
[PROOF STEP]
have "infinite {n::nat. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {n. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite {n. True}

goal (1 subgoal):
 1. infinite {c. True}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite {n. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite {n. True}

goal (1 subgoal):
 1. infinite {c. True}
[PROOF STEP]
by (metis UNIV_def finite_imageI type_definition.Rep_range type_definition_cars)
[PROOF STATE]
proof (state)
this:
infinite {c. True}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Plus_ZeroL[simp]: "Plus Zero r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus Zero r = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
theorem Plus_ZeroR[simp]: "Plus r Zero = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r Zero = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
theorem Plus_comm: "Plus r s = Plus s r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r s = Plus s r
[PROOF STEP]
by (coinduction arbitrary: r s) auto


[STATEMENT]
lemma Plus_rotate: "Plus r (Plus s t) = Plus s (Plus r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r (Plus s t) = Plus s (Plus r t)
[PROOF STEP]
using Plus_assoc Plus_comm
[PROOF STATE]
proof (prove)
using this:
Plus (Plus ?r ?s) ?t = Plus ?r (Plus ?s ?t)
Plus ?r ?s = Plus ?s ?r

goal (1 subgoal):
 1. Plus r (Plus s t) = Plus s (Plus r t)
[PROOF STEP]
by metis


[STATEMENT]
theorem Plus_idem: "Plus r r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r r = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Plus_idem_assoc: "Plus r (Plus r s) = Plus r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Plus r (Plus r s) = Plus r s
[PROOF STEP]
by (metis Plus_assoc Plus_idem)


[STATEMENT]
lemma Plus_OneL[simp]: "\<oo> r \<Longrightarrow> Plus One r = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> r \<Longrightarrow> Plus One r = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma Plus_OneR[simp]: "\<oo> r \<Longrightarrow> Plus r One = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> r \<Longrightarrow> Plus r One = r
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma TimesLR_ZeroL[simp]: "TimesLR Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TimesLR Zero r = Zero
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
lemma TimesLR_ZeroR[simp]: "TimesLR r Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TimesLR r Zero = Zero
[PROOF STEP]
by (coinduction arbitrary: r) (auto intro: exI[of _ Zero])


[STATEMENT]
lemma TimesLR_PlusL[simp]: "TimesLR (Plus r s) t = Plus (TimesLR r t) (TimesLR s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TimesLR (Plus r s) t = Plus (TimesLR r t) (TimesLR s t)
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma TimesLR_PlusR[simp]: "TimesLR r (Plus s t) = Plus (TimesLR r s) (TimesLR r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TimesLR r (Plus s t) = Plus (TimesLR r s) (TimesLR r t)
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma Times_Plus_Zero[simp]: "Times_Plus Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus Zero = Zero
[PROOF STEP]
by coinduction simp


[STATEMENT]
lemma Times_Plus_Plus[simp]: "Times_Plus (Plus r s) = Plus (Times_Plus r) (Times_Plus s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (Plus r s) = Plus (Times_Plus r) (Times_Plus s)
[PROOF STEP]
proof (coinduction arbitrary: r s)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r s. \<oo> (Times_Plus (Plus r s)) = \<oo> (Plus (Times_Plus r) (Times_Plus s)) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (Times_Plus (Plus r s)) x = Times_Plus (Plus ra sa) \<and> \<dd> (Plus (Times_Plus r) (Times_Plus s)) x = Plus (Times_Plus ra) (Times_Plus sa)) \<or> \<dd> (Times_Plus (Plus r s)) x = \<dd> (Plus (Times_Plus r) (Times_Plus s)) x)
[PROOF STEP]
case (Lang r s)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>r s. \<oo> (Times_Plus (Plus r s)) = \<oo> (Plus (Times_Plus r) (Times_Plus s)) \<and> (\<forall>x. (\<exists>ra sa. \<dd> (Times_Plus (Plus r s)) x = Times_Plus (Plus ra sa) \<and> \<dd> (Plus (Times_Plus r) (Times_Plus s)) x = Plus (Times_Plus ra) (Times_Plus sa)) \<or> \<dd> (Times_Plus (Plus r s)) x = \<dd> (Plus (Times_Plus r) (Times_Plus s)) x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times_Plus (Plus r s)) = \<oo> (Plus (Times_Plus r) (Times_Plus s)) \<and> (\<forall>x. (\<exists>r s. \<dd> (Times_Plus (Plus r s)) x = Times_Plus (Plus r s) \<and> \<dd> (Plus (Times_Plus r) (Times_Plus s)) x = Plus (Times_Plus r) (Times_Plus s)) \<or> \<dd> (Times_Plus (Plus r s)) x = \<dd> (Plus (Times_Plus r) (Times_Plus s)) x)
[PROOF STEP]
unfolding Times_Plus.sel Plus.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<oo> r \<or> \<oo> s) = (\<oo> r \<or> \<oo> s) \<and> (\<forall>x. (\<exists>r s. Times_Plus (Plus (Plus (\<dd> r (x, True)) (\<dd> s (x, True))) (Plus (\<dd> r (x, False)) (\<dd> s (x, False)))) = Times_Plus (Plus r s) \<and> Plus (Times_Plus (Plus (\<dd> r (x, True)) (\<dd> r (x, False)))) (Times_Plus (Plus (\<dd> s (x, True)) (\<dd> s (x, False)))) = Plus (Times_Plus r) (Times_Plus s)) \<or> Times_Plus (Plus (Plus (\<dd> r (x, True)) (\<dd> s (x, True))) (Plus (\<dd> r (x, False)) (\<dd> s (x, False)))) = Plus (Times_Plus (Plus (\<dd> r (x, True)) (\<dd> r (x, False)))) (Times_Plus (Plus (\<dd> s (x, True)) (\<dd> s (x, False)))))
[PROOF STEP]
by (intro conjI[OF refl]) (metis Plus_comm Plus_rotate)
[PROOF STATE]
proof (state)
this:
\<oo> (Times_Plus (Plus r s)) = \<oo> (Plus (Times_Plus r) (Times_Plus s)) \<and> (\<forall>x. (\<exists>r s. \<dd> (Times_Plus (Plus r s)) x = Times_Plus (Plus r s) \<and> \<dd> (Plus (Times_Plus r) (Times_Plus s)) x = Plus (Times_Plus r) (Times_Plus s)) \<or> \<dd> (Times_Plus (Plus r s)) x = \<dd> (Plus (Times_Plus r) (Times_Plus s)) x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Times_Plus_TimesLR_One[simp]: "Times_Plus (TimesLR r One) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (TimesLR r One) = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
lemma Times_Plus_TimesLR_PlusL[simp]:
  "Times_Plus (TimesLR (Plus r s) t) = Plus (Times_Plus (TimesLR r t)) (Times_Plus (TimesLR s t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (TimesLR (Plus r s) t) = Plus (Times_Plus (TimesLR r t)) (Times_Plus (TimesLR s t))
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma Times_Plus_TimesLR_PlusR[simp]:
  "Times_Plus (TimesLR r (Plus s t)) = Plus (Times_Plus (TimesLR r s)) (Times_Plus (TimesLR r t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times_Plus (TimesLR r (Plus s t)) = Plus (Times_Plus (TimesLR r s)) (Times_Plus (TimesLR r t))
[PROOF STEP]
by (coinduction arbitrary: r s t) auto


[STATEMENT]
lemma \<oo>_Times[simp]:
  "\<oo> (Times r s) = (\<oo> r \<and> \<oo> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times r s) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
unfolding Times_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<oo> (Times_Plus (TimesLR r s)) = (\<oo> r \<and> \<oo> s)
[PROOF STEP]
by simp


[STATEMENT]
lemma \<dd>_Times[simp]:
  "\<dd> (Times r s) = (\<lambda>a. if \<oo> r then Plus (Times (\<dd> r a) s) (\<dd> s a) else Times (\<dd> r a) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (Times r s) = (\<lambda>a. if \<oo> r then Plus (Times (\<dd> r a) s) (\<dd> s a) else Times (\<dd> r a) s)
[PROOF STEP]
unfolding Times_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dd> (Times_Plus (TimesLR r s)) = (\<lambda>a. if \<oo> r then Plus (Times_Plus (TimesLR (\<dd> r a) s)) (\<dd> s a) else Times_Plus (TimesLR (\<dd> r a) s))
[PROOF STEP]
by auto


[STATEMENT]
theorem Times_ZeroL[simp]: "Times Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times Zero r = Zero
[PROOF STEP]
by coinduction simp


[STATEMENT]
theorem Times_ZeroR[simp]: "Times r Zero = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times r Zero = Zero
[PROOF STEP]
by (coinduction arbitrary: r) auto


[STATEMENT]
theorem Times_OneR[simp]: "Times r One = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times r One = r
[PROOF STEP]
by (coinduction arbitrary: r) simp


[STATEMENT]
lemma language_coinduct_upto_Plus[unfolded rel_fun_def, simplified, case_names Lang, consumes 1]:
  assumes R: "R L K" and hyp:
    "(\<And>L K. R L K \<Longrightarrow> \<oo> L = \<oo> K \<and> rel_fun (=) (Plus_cong R) (\<dd> L) (\<dd> K))"
  shows "L = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L = K
[PROOF STEP]
proof (coinduct rule: language.coinduct[of "Plus_cong R"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Plus_cong R L K
 2. \<And>language language'. Plus_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (Plus_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
fix L K
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Plus_cong R L K
 2. \<And>language language'. Plus_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (Plus_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
assume "Plus_cong R L K"
[PROOF STATE]
proof (state)
this:
Plus_cong R L K

goal (2 subgoals):
 1. Plus_cong R L K
 2. \<And>language language'. Plus_cong R language language' \<Longrightarrow> \<oo> language = \<oo> language' \<and> rel_fun (=) (Plus_cong R) (\<dd> language) (\<dd> language')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Plus_cong R L K
[PROOF STEP]
show "\<oo> L = \<oo> K \<and> rel_fun (=) (Plus_cong R) (\<dd> L) (\<dd> K)"
[PROOF STATE]
proof (prove)
using this:
Plus_cong R L K

goal (1 subgoal):
 1. \<oo> L = \<oo> K \<and> rel_fun (=) (Plus_cong R) (\<dd> L) (\<dd> K)
[PROOF STEP]
by (induct rule: Plus_cong.induct) (auto simp: rel_fun_def intro: Sym dest: hyp)
[PROOF STATE]
proof (state)
this:
\<oo> L = \<oo> K \<and> rel_fun (=) (Plus_cong R) (\<dd> L) (\<dd> K)

goal (1 subgoal):
 1. Plus_cong R L K
[PROOF STEP]
qed (intro Base R)


[STATEMENT]
theorem Times_PlusL[simp]: "Times (Plus r s) t = Plus (Times r t) (Times s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times (Plus r s) t = Plus (Times r t) (Times s t)
[PROOF STEP]
by (coinduction arbitrary: r s rule: language_coinduct_upto_Plus) auto


[STATEMENT]
theorem Times_PlusR[simp]: "Times r (Plus s t) = Plus (Times r s) (Times r t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Times r (Plus s t) = Plus (Times r s) (Times r t)
[PROOF STEP]
by (coinduction arbitrary: r s rule: language_coinduct_upto_Plus) fastforce


[STATEMENT]
lemma StarLR_Zero[simp]: "StarLR Zero r = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StarLR Zero r = Zero
[PROOF STEP]
by coinduction auto


[STATEMENT]
lemma StarLR_Plus[simp]: "StarLR (Plus r s) t = Plus (StarLR r t) (StarLR s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. StarLR (Plus r s) t = Plus (StarLR r t) (StarLR s t)
[PROOF STEP]
by (coinduction arbitrary: r s) (auto simp del: Plus_ACI Times_PlusR)