[STATEMENT]
lemma det_Gauss_Jordan_in_ij:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}" and i j::"'n"
defines A': "A'== mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) $ i $ j)"
shows "det (Gauss_Jordan_in_ij A i j) = det A' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
have nrows_eq: "nrows A' = nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows A' = nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('n) = CARD('n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nrows A' = nrows A

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
have "row_add_iterate A' (nrows A - 1) i j  =  Gauss_Jordan_in_ij A i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j
[PROOF STEP]
using row_add_iterate_eq_Gauss_Jordan_in_ij
[PROOF STATE]
proof (prove)
using this:
row_add_iterate (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j)) (nrows ?A - 1) ?i ?j = Gauss_Jordan_in_ij ?A ?i ?j

goal (1 subgoal):
 1. row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j
[PROOF STEP]
unfolding A'
[PROOF STATE]
proof (prove)
using this:
row_add_iterate (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j)) (nrows ?A - 1) ?i ?j = Gauss_Jordan_in_ij ?A ?i ?j

goal (1 subgoal):
 1. row_add_iterate (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) (nrows A - 1) i j = Gauss_Jordan_in_ij A i j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
hence "det (Gauss_Jordan_in_ij A i j) = det (row_add_iterate A' (nrows A - 1) i j)"
[PROOF STATE]
proof (prove)
using this:
row_add_iterate A' (nrows A - 1) i j = Gauss_Jordan_in_ij A i j

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det (row_add_iterate A' (nrows A - 1) i j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det (row_add_iterate A' (nrows A - 1) i j)

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det (row_add_iterate A' (nrows A - 1) i j)

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
have "... = det A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add_iterate A' (nrows A - 1) i j) = det A'
[PROOF STEP]
by (rule det_row_add_iterate[of A', unfolded nrows_eq])
[PROOF STATE]
proof (state)
this:
det (row_add_iterate A' (nrows A - 1) i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_Gauss_Jordan_in_ij_1:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}" and i j::"'n"
defines A': "A'== mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) $ i $ j)"
assumes i: "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) = i"
shows "det (Gauss_Jordan_in_ij A i j) = 1/(A$i$j) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
have "det (Gauss_Jordan_in_ij A i j) = det A' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
using det_Gauss_Jordan_in_ij
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij ?A ?i ?j) = det (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j))

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
unfolding A'
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij ?A ?i ?j) = det (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j))

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
have "... = 1/(A$i$j) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A' = (1::'a) / A $ i $ j * det A
[PROOF STEP]
unfolding A' det_mult_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * det (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
unfolding i det_interchange_rows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i i $ i $ j * (of_int (if i = i then 1 else - 1) * det A) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det A' = (1::'a) / A $ i $ j * det A

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_Gauss_Jordan_in_ij_2:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}" and i j::"'n"
defines A': "A'== mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) $ i $ j)"
assumes i: "(LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) \<noteq> i"
shows "det (Gauss_Jordan_in_ij A i j) = - 1/(A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
have "det (Gauss_Jordan_in_ij A i j) = det A' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
using det_Gauss_Jordan_in_ij
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij ?A ?i ?j) = det (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j))

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det A'
[PROOF STEP]
unfolding A'
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij ?A ?i ?j) = det (mult_row (interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n)) ?i ((1::?'a) / interchange_rows ?A ?i (LEAST n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n) $ ?i $ ?j))

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = det (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = det A'

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
have "... = - 1/(A$ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $j) * det A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A' = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
unfolding A' det_mult_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * det (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
unfolding det_interchange_rows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * (of_int (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then 1 else - 1) * det A) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<noteq> i

goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * (of_int (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then 1 else - 1) * det A) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det A' = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A

goal (1 subgoal):
 1. det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Gauss_Jordan_in_ij_det_P_code[code]:
shows "Gauss_Jordan_in_ij_det_P A i j =
    (let n = (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n);
         interchange_A = interchange_rows A i n;
         A' = mult_row interchange_A i (1 / interchange_A $ i $ j) in (if i = n then 1/(A $ i $ j) else - 1/(A $ n $ j), Gauss_Jordan_wrapper i j A' interchange_A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij_det_P A i j = (let n = LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'a) / interchange_A $ i $ j) in (if i = n then (1::'a) / A $ i $ j else - (1::'a) / A $ n $ j, Gauss_Jordan_wrapper i j A' interchange_A))
[PROOF STEP]
unfolding Gauss_Jordan_in_ij_det_P_def Gauss_Jordan_in_ij_def Gauss_Jordan_wrapper_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j, \<chi>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ s $ j) $ s) = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j, \<chi>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ s $ j) $ s)
[PROOF STEP]
by auto


[STATEMENT]
lemma det_Gauss_Jordan_in_ij_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}" and i j::"'n"
shows "(fst (Gauss_Jordan_in_ij_det_P A i j)) * det A  = det (snd (Gauss_Jordan_in_ij_det_P A i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det A = det (snd (Gauss_Jordan_in_ij_det_P A i j))
[PROOF STEP]
unfolding Gauss_Jordan_in_ij_det_P_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det A = det (Gauss_Jordan_in_ij A i j)
[PROOF STEP]
using det_Gauss_Jordan_in_ij_1[of A j i]
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = i \<Longrightarrow> det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A

goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det A = det (Gauss_Jordan_in_ij A i j)
[PROOF STEP]
using det_Gauss_Jordan_in_ij_2[of A j i]
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) = i \<Longrightarrow> det (Gauss_Jordan_in_ij A i j) = (1::'a) / A $ i $ j * det A
(LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<noteq> i \<Longrightarrow> det (Gauss_Jordan_in_ij A i j) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det A

goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det A = det (Gauss_Jordan_in_ij A i j)
[PROOF STEP]
by auto


[STATEMENT]
lemma det_Gauss_Jordan_column_k_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
assumes det: "det_P * det B = det A"
shows "(fst (Gauss_Jordan_column_k_det_P (det_P,i,A) k)) * det B = det (snd (snd (Gauss_Jordan_column_k_det_P (det_P,i,A) k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_column_k_det_P (det_P, i, A) k) * det B = det (snd (snd (Gauss_Jordan_column_k_det_P (det_P, i, A) k)))
[PROOF STEP]
proof (unfold Gauss_Jordan_column_k_det_P_def Let_def, auto simp add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det_P * det B = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det_P * det B = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
assume i_not_nrows: "i \<noteq> nrows A"
and i_less_m: "from_nat i \<le> m"
and Amk_not_0: "A $ m $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
i \<noteq> nrows A
mod_type_class.from_nat i \<le> m
A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>i \<noteq> nrows A; mod_type_class.from_nat i \<le> m; A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det_P * det B = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
show  "fst (Gauss_Jordan_in_ij_det_P A (from_nat i) (from_nat k)) * det_P * det B =
        det (snd (Gauss_Jordan_in_ij_det_P A (from_nat i) (from_nat k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det_P * det B = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
unfolding mult.assoc det
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det A = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
unfolding det_Gauss_Jordan_in_ij_det_P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k))) = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det_P * det B = det (snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_Gauss_Jordan_upt_k_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "(fst (Gauss_Jordan_upt_k_det_P A k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k))
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) * det A = det (snd (Gauss_Jordan_upt_k_det_P A 0))
 2. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) * det A = det (snd (Gauss_Jordan_upt_k_det_P A 0))
 2. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A 0) * det A = det (snd (Gauss_Jordan_upt_k_det_P A 0))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]))) * det A = det (snd (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]))))
[PROOF STEP]
unfolding fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0]) * det A = det (snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc 0])))
[PROOF STEP]
by (simp add:det_Gauss_Jordan_column_k_det_P)
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A 0) * det A = det (snd (Gauss_Jordan_upt_k_det_P A 0))

goal (1 subgoal):
 1. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k))

goal (1 subgoal):
 1. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
have suc_rw: "[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]

goal (1 subgoal):
 1. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
have fold_expand: "(foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])
= (fst (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k]), fst (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])),
  snd (snd (foldl Gauss_Jordan_column_k_det_P (1, 0, A) [0..<Suc k])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k] = (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]), fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k] = (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]), fst (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k])))

goal (1 subgoal):
 1. \<And>k. fst (Gauss_Jordan_upt_k_det_P A k) * det A = det (snd (Gauss_Jordan_upt_k_det_P A k)) \<Longrightarrow> fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))
[PROOF STEP]
unfolding Gauss_Jordan_upt_k_det_P_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]))) * det A = det (snd (fst (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]), snd (snd (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc (Suc k)]))))
[PROOF STEP]
unfolding suc_rw foldl_append List.foldl.simps fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k)) * det A = det (snd (snd (Gauss_Jordan_column_k_det_P (foldl Gauss_Jordan_column_k_det_P (1::'a, 0, A) [0..<Suc k]) (Suc k))))
[PROOF STEP]
by(subst (1 2) fold_expand, rule det_Gauss_Jordan_column_k_det_P, rule Suc.hyps[unfolded Gauss_Jordan_upt_k_det_P_def Let_def fst_conv snd_conv])
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_upt_k_det_P A (Suc k)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (Suc k)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_Gauss_Jordan_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "(fst (Gauss_Jordan_det_P A)) * det A = det (snd (Gauss_Jordan_det_P A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_det_P A) * det A = det (snd (Gauss_Jordan_det_P A))
[PROOF STEP]
using det_Gauss_Jordan_upt_k_det_P
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_upt_k_det_P ?A ?k) * det ?A = det (snd (Gauss_Jordan_upt_k_det_P ?A ?k))

goal (1 subgoal):
 1. fst (Gauss_Jordan_det_P A) * det A = det (snd (Gauss_Jordan_det_P A))
[PROOF STEP]
unfolding Gauss_Jordan_det_P_def
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_upt_k_det_P ?A ?k) * det ?A = det (snd (Gauss_Jordan_upt_k_det_P ?A ?k))

goal (1 subgoal):
 1. fst (Gauss_Jordan_upt_k_det_P A (ncols A - 1)) * det A = det (snd (Gauss_Jordan_upt_k_det_P A (ncols A - 1)))
[PROOF STEP]
by simp


[STATEMENT]
lemma upper_triangular_upt_imp_upper_triangular:
assumes "upper_triangular_upt_k A (nrows A)"
shows "upper_triangular A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
upper_triangular_upt_k A (nrows A)

goal (1 subgoal):
 1. upper_triangular A
[PROOF STEP]
unfolding upper_triangular_upt_k_def upper_triangular_def nrows_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. j < i \<and> mod_type_class.to_nat j < CARD('b) \<longrightarrow> A $ i $ j = (0::'a)

goal (1 subgoal):
 1. \<forall>i j. j < i \<longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
using to_nat_less_card[where ?'a='b]
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. j < i \<and> mod_type_class.to_nat j < CARD('b) \<longrightarrow> A $ i $ j = (0::'a)
mod_type_class.to_nat ?j < CARD('b)

goal (1 subgoal):
 1. \<forall>i j. j < i \<longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_imp_upper_triagular_upt:
fixes A::"'a::{one, zero}^'n::{mod_type}^'n::{mod_type}"
assumes "reduced_row_echelon_form A"
shows "upper_triangular_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular_upt_k A k
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. upper_triangular_upt_k A 0
 2. \<And>k. upper_triangular_upt_k A k \<Longrightarrow> upper_triangular_upt_k A (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

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

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

goal (1 subgoal):
 1. \<And>k. upper_triangular_upt_k A k \<Longrightarrow> upper_triangular_upt_k A (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular_upt_k A (Suc k)
[PROOF STEP]
unfolding upper_triangular_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. j < i \<and> mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < i; mod_type_class.to_nat j < Suc k\<rbrakk> \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
fix i j::'n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < i; mod_type_class.to_nat j < Suc k\<rbrakk> \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
assume j_less_i: "j < i" and j_less_suc_k: "to_nat j < Suc k"
[PROOF STATE]
proof (state)
this:
j < i
mod_type_class.to_nat j < Suc k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < i; mod_type_class.to_nat j < Suc k\<rbrakk> \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
show "A $ i $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ j = (0::'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> A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'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> A $ i $ j = (0::'a)
 2. \<not> mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < k
upper_triangular_upt_k A k

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

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

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

goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> mod_type_class.to_nat j < k \<Longrightarrow> A $ i $ j = (0::'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> A $ i $ j = (0::'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_k
[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 simp
[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> A $ i $ j = (0::'a)
[PROOF STEP]
have rref_suc: "reduced_row_echelon_form_upt_k A (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A (Suc k)
[PROOF STEP]
by (metis assms rref_implies_rref_upt)
[PROOF STATE]
proof (state)
this:
reduced_row_echelon_form_upt_k A (Suc k)

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

goal (2 subgoals):
 1. A $ i $ mod_type_class.from_nat k = (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
 2. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have "from_nat k = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
by (metis from_nat_to_nat_id j_eq_k)
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = j

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

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat k = j
A $ i $ mod_type_class.from_nat k = (0::'a)

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

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

goal (1 subgoal):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have zero_i_k: "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k 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> A $ i $ j = (0::'a)
[PROOF STEP]
by (metis (opaque_lifting, mono_tags) Suc.hyps leD le_less_linear less_imp_le j_eq_k j_less_i le_trans to_nat_mono' upper_triangular_upt_k_def)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i (Suc k) 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 < Suc k \<longrightarrow> A $ i $ j = (0::'a))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'a))
[PROOF STEP]
by (metis j_eq_k lessI to_nat_from_nat)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i (Suc k) A

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

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

goal (1 subgoal):
 1. \<And>y. A $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show "\<And>y. A $ i $ y \<noteq> 0 \<Longrightarrow> from_nat k \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. A $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
by (metis (full_types) is_zero_row_upt_k_def not_le_imp_less to_nat_le zero_i_k)
[PROOF STATE]
proof (state)
this:
A $ i $ ?y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> ?y

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

goal (1 subgoal):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
have i_not_k: "i \<noteq> from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> mod_type_class.from_nat k
[PROOF STEP]
by (metis less_irrefl from_nat_to_nat_id j_eq_k j_less_i)
[PROOF STATE]
proof (state)
this:
i \<noteq> mod_type_class.from_nat k

goal (1 subgoal):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a) \<Longrightarrow> A $ i $ j = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
using rref_upt_condition4_explicit[OF rref_suc not_zero_i_suc_k i_not_k]
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat k $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
unfolding Least_eq
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat k $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
using rref_upt_condition1_explicit[OF rref_suc]
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat k $ mod_type_class.from_nat k = (0::'a)
\<lbrakk>is_zero_row_upt_k ?i (Suc k) A; ?i < ?j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) A

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
using Suc.hyps
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat k $ mod_type_class.from_nat k = (0::'a)
\<lbrakk>is_zero_row_upt_k ?i (Suc k) A; ?i < ?j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) A
upper_triangular_upt_k A k

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
unfolding upper_triangular_upt_k_def
[PROOF STATE]
proof (prove)
using this:
A $ mod_type_class.from_nat k $ mod_type_class.from_nat k = (0::'a)
\<lbrakk>is_zero_row_upt_k ?i (Suc k) A; ?i < ?j\<rbrakk> \<Longrightarrow> is_zero_row_upt_k ?j (Suc k) A
\<forall>i j. j < i \<and> mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)

goal (1 subgoal):
 1. A $ i $ j = (0::'a)
[PROOF STEP]
by (metis (mono_tags) leD not_le_imp_less is_zero_row_upt_k_def is_zero_row_upt_k_suc j_eq_k j_less_i not_zero_i_suc_k to_nat_from_nat to_nat_mono')
[PROOF STATE]
proof (state)
this:
A $ i $ j = (0::'a)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rref_imp_upper_triagular:
assumes "reduced_row_echelon_form A"
shows "upper_triangular A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular A
[PROOF STEP]
by (metis assms rref_imp_upper_triagular_upt upper_triangular_upt_imp_upper_triangular)


[STATEMENT]
lemma det_Gauss_Jordan[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "det (Gauss_Jordan A) = prod (\<lambda>i. (Gauss_Jordan A)$i$i) (UNIV:: 'n set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (Gauss_Jordan A) = (\<Prod>i\<in>UNIV. Gauss_Jordan A $ i $ i)
[PROOF STEP]
using det_upperdiagonal rref_imp_upper_triagular[OF rref_Gauss_Jordan[of A]]
[PROOF STATE]
proof (prove)
using this:
(\<And>i j. j < i \<Longrightarrow> ?A $ i $ j = (0::?'a)) \<Longrightarrow> det ?A = (\<Prod>i\<in>UNIV. ?A $ i $ i)
upper_triangular (Gauss_Jordan A)

goal (1 subgoal):
 1. det (Gauss_Jordan A) = (\<Prod>i\<in>UNIV. Gauss_Jordan A $ i $ i)
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
(\<And>i j. j < i \<Longrightarrow> ?A $ i $ j = (0::?'a)) \<Longrightarrow> det ?A = (\<Prod>i\<in>UNIV. ?A $ i $ i)
\<forall>i j. j < i \<longrightarrow> Gauss_Jordan A $ i $ j = (0::'a)

goal (1 subgoal):
 1. det (Gauss_Jordan A) = (\<Prod>i\<in>UNIV. Gauss_Jordan A $ i $ i)
[PROOF STEP]
by blast


[STATEMENT]
lemma snd_Gauss_Jordan_in_ij_det_P_is_snd_Gauss_Jordan_in_ij_PA:
shows "snd (Gauss_Jordan_in_ij_det_P A i j) = snd (Gauss_Jordan_in_ij_PA (P,A) i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_in_ij_det_P A i j) = snd (Gauss_Jordan_in_ij_PA (P, A) i j)
[PROOF STEP]
unfolding Gauss_Jordan_in_ij_det_P_def Gauss_Jordan_in_ij_PA_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (let n = LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n in (if i = n then (1::'a) / A $ i $ j else - (1::'a) / A $ n $ j, Gauss_Jordan_in_ij A i j)) = snd (let Pa = fst (P, A); A = snd (P, A); n = LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n; interchange_A = interchange_rows A i n; interchange_P = interchange_rows Pa i n; P' = mult_row interchange_P i ((1::'a) / interchange_A $ i $ j) in (\<chi>s. if s = i then P' $ s else row_add P' s i (- interchange_A $ s $ j) $ s, Gauss_Jordan_in_ij A i j))
[PROOF STEP]
unfolding  Gauss_Jordan_in_ij_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ s $ j) $ s) = (\<chi>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ s $ j) $ s)
[PROOF STEP]
..


[STATEMENT]
lemma snd_Gauss_Jordan_column_k_det_P_is_snd_Gauss_Jordan_column_k_PA:
shows "snd (Gauss_Jordan_column_k_det_P (n,i,A) k) = snd (Gauss_Jordan_column_k_PA (P,i,A) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_column_k_det_P (n, i, A) k) = snd (Gauss_Jordan_column_k_PA (P, i, A) k)
[PROOF STEP]
unfolding Gauss_Jordan_column_k_det_P_def Gauss_Jordan_column_k_PA_def Let_def snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (fst (i, A)). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> fst (i, A) = nrows A then (fst (n, i, A), fst (i, A), A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat (fst (i, A))) (mod_type_class.from_nat k)) * fst (n, i, A), fst (i, A) + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat (fst (i, A))) (mod_type_class.from_nat k)))) = snd (if (\<forall>m\<ge>mod_type_class.from_nat (fst (i, A)). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> fst (i, A) = nrows A then (fst (P, i, A), fst (i, A), A) else (fst (Gauss_Jordan_in_ij_PA (fst (P, i, A), A) (mod_type_class.from_nat (fst (i, A))) (mod_type_class.from_nat k)), fst (i, A) + 1, snd (Gauss_Jordan_in_ij_PA (fst (P, i, A), A) (mod_type_class.from_nat (fst (i, A))) (mod_type_class.from_nat k))))
[PROOF STEP]
unfolding fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (n, i, A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * n, i + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))) = snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (P, i, A) else (fst (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)), i + 1, snd (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k))))
[PROOF STEP]
using snd_Gauss_Jordan_in_ij_det_P_is_snd_Gauss_Jordan_in_ij_PA
[PROOF STATE]
proof (prove)
using this:
snd (Gauss_Jordan_in_ij_det_P ?A ?i ?j) = snd (Gauss_Jordan_in_ij_PA (?P, ?A) ?i ?j)

goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (n, i, A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * n, i + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))) = snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (P, i, A) else (fst (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)), i + 1, snd (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k))))
[PROOF STEP]
by auto


[STATEMENT]
lemma det_fst_row_add_iterate_PA:
fixes A::"'a::{comm_ring_1}^'n::{mod_type}^'n::{mod_type}"
assumes n: "n<nrows A"
shows "det (fst (row_add_iterate_PA (P,A) n i j)) = det P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) n i j)) = det P
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) n i j)) = det P
[PROOF STEP]
proof (induct n arbitrary: P A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P A. 0 < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) 0 i j)) = det P
 2. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A

goal (2 subgoals):
 1. \<And>P A. 0 < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) 0 i j)) = det P
 2. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) 0 i j)) = det P
[PROOF STEP]
unfolding row_add_iterate_PA.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (if i = (0::'n) then (P, A) else (row_add P (0::'n) i (- A $ (0::'n) $ j), row_add A (0::'n) i (- A $ (0::'n) $ j)))) = det P
[PROOF STEP]
using det_row_add'[of 0 i P]
[PROOF STATE]
proof (prove)
using this:
(0::'n) \<noteq> i \<Longrightarrow> det (row_add P (0::'n) i ?q) = det P

goal (1 subgoal):
 1. det (fst (if i = (0::'n) then (P, A) else (row_add P (0::'n) i (- A $ (0::'n) $ j), row_add A (0::'n) i (- A $ (0::'n) $ j)))) = det P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) 0 i j)) = det P

goal (1 subgoal):
 1. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n < nrows ?A \<Longrightarrow> det (fst (row_add_iterate_PA (?P, ?A) n i j)) = det ?P
Suc n < nrows A

goal (1 subgoal):
 1. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
have n: "n<nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows A
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A

goal (1 subgoal):
 1. n < nrows A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < nrows A

goal (1 subgoal):
 1. \<And>n P A. \<lbrakk>\<And>P A. n < nrows A \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) n i j)) = det P; Suc n < nrows A\<rbrakk> \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
unfolding row_add_iterate_PA.simps if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) n i j)) = det P
[PROOF STEP]
using Suc.hyps[OF n]
[PROOF STATE]
proof (prove)
using this:
det (fst (row_add_iterate_PA (?P, A) n i j)) = det ?P

goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) n i j)) = det P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
define P' where "P' = row_add P (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
P' = row_add P (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
define A' where "A' = row_add A (from_nat (Suc n)) i (- A $ from_nat (Suc n) $ j)"
[PROOF STATE]
proof (state)
this:
A' = row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
have n2: "n< nrows A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows A'
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. n < nrows A'
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
n < CARD('n)

goal (1 subgoal):
 1. n < CARD('n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
n < nrows A'

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
have "det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det (fst (row_add_iterate_PA (P', A') n i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det (fst (row_add_iterate_PA (P', A') n i j))
[PROOF STEP]
unfolding row_add_iterate_PA.simps if_not_P[OF False] P'_def A'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (row_add P (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j), row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j)) = det (fst (row_add_iterate_PA (row_add P (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j), row_add A (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) n i j))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det (fst (row_add_iterate_PA (P', A') n i j))

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det (fst (row_add_iterate_PA (P', A') n i j))

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
have "... = det P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P', A') n i j)) = det P'
[PROOF STEP]
using Suc.hyps[OF n2]
[PROOF STATE]
proof (prove)
using this:
det (fst (row_add_iterate_PA (?P, A') n i j)) = det ?P

goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P', A') n i j)) = det P'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P', A') n i j)) = det P'

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P', A') n i j)) = det P'

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
have "... = det P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det P' = det P
[PROOF STEP]
unfolding P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (row_add P (mod_type_class.from_nat (Suc n)) i (- A $ mod_type_class.from_nat (Suc n) $ j)) = det P
[PROOF STEP]
proof (rule det_row_add', rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
assume "from_nat (Suc n) = i"
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (Suc n) = i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
hence "to_nat (from_nat (Suc n)::'n) = to_nat i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat (Suc n) = i

goal (1 subgoal):
 1. mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
hence "(Suc n) = to_nat i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat (Suc n)) = mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n = mod_type_class.to_nat i
[PROOF STEP]
unfolding to_nat_from_nat_id[OF Suc.prems[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n = mod_type_class.to_nat i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.from_nat (Suc n) = i \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i

goal (1 subgoal):
 1. False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i
Suc n \<noteq> mod_type_class.to_nat i

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:
det P' = det P

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P

goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P, A) (Suc n) i j)) = det P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_fst_Gauss_Jordan_in_ij_PA_eq_fst_Gauss_Jordan_in_ij_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P,A) i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
define P' where "P' = mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j)"
[PROOF STATE]
proof (state)
this:
P' = mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
define A' where "A' = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j)"
[PROOF STATE]
proof (state)
this:
A' = mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
have "det (fst (Gauss_Jordan_in_ij_PA (P,A) i j)) = det (fst (row_add_iterate_PA (P',A') (nrows A - 1) i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (Gauss_Jordan_in_ij_PA (P, A) i j)) = det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j))
[PROOF STEP]
unfolding fst_row_add_iterate_PA_eq_fst_Gauss_Jordan_in_ij_PA[symmetric] A'_def P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j), mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) (nrows A - 1) i j)) = det (fst (row_add_iterate_PA (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j), mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) (nrows A - 1) i j))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det (fst (Gauss_Jordan_in_ij_PA (P, A) i j)) = det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j))

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (fst (Gauss_Jordan_in_ij_PA (P, A) i j)) = det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j))

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
have "...= det P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j)) = det P'
[PROOF STEP]
by (rule det_fst_row_add_iterate_PA, simp add: nrows_def)
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j)) = det P'

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (fst (row_add_iterate_PA (P', A') (nrows A - 1) i j)) = det P'

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
have "... = (if i = (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) then 1 / A $ i $ j else - 1 / A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j) * det P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
proof (cases "i = (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
 2. i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)

goal (2 subgoals):
 1. i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
 2. i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
unfolding if_P[OF True] P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) = (1::'a) / A $ i $ j * det P
[PROOF STEP]
unfolding True[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row (interchange_rows P i i) i ((1::'a) / interchange_rows A i i $ i $ j)) = (1::'a) / A $ i $ j * det P
[PROOF STEP]
unfolding interchange_same_rows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row P i ((1::'a) / A $ i $ j)) = (1::'a) / A $ i $ j * det P
[PROOF STEP]
unfolding det_mult_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / A $ i $ j * det P = (1::'a) / A $ i $ j * det P
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P

goal (1 subgoal):
 1. i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)

goal (1 subgoal):
 1. i \<noteq> (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) \<Longrightarrow> det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P
[PROOF STEP]
unfolding if_not_P[OF False] P'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) i ((1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j)) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det P
[PROOF STEP]
unfolding det_mult_row
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * det (interchange_rows P i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n)) = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det P
[PROOF STEP]
unfolding det_interchange_different_rows[OF False]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ i $ j * - det P = - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j * det P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det P' = (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
have "... = fst (Gauss_Jordan_in_ij_det_P A i j) * det P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P = fst (Gauss_Jordan_in_ij_det_P A i j) * det P
[PROOF STEP]
unfolding Gauss_Jordan_in_ij_det_P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P = fst (let n = LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n in (if i = n then (1::'a) / A $ i $ j else - (1::'a) / A $ n $ j, Gauss_Jordan_in_ij A i j)) * det P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if i = (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) then (1::'a) / A $ i $ j else - (1::'a) / A $ (LEAST n. A $ n $ j \<noteq> (0::'a) \<and> i \<le> n) $ j) * det P = fst (Gauss_Jordan_in_ij_det_P A i j) * det P

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (fst (Gauss_Jordan_in_ij_PA (P, A) i j)) = fst (Gauss_Jordan_in_ij_det_P A i j) * det P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (fst (Gauss_Jordan_in_ij_PA (P, A) i j)) = fst (Gauss_Jordan_in_ij_det_P A i j) * det P

goal (1 subgoal):
 1. fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
fst (Gauss_Jordan_in_ij_det_P A i j) * det P = det (fst (Gauss_Jordan_in_ij_PA (P, A) i j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_fst_Gauss_Jordan_column_k_PA_eq_fst_Gauss_Jordan_column_k_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "fst (Gauss_Jordan_column_k_det_P (det P,i,A) k) = det (fst (Gauss_Jordan_column_k_PA (P,i,A) k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_column_k_det_P (det P, i, A) k) = det (fst (Gauss_Jordan_column_k_PA (P, i, A) k))
[PROOF STEP]
unfolding Gauss_Jordan_column_k_det_P_def Gauss_Jordan_column_k_PA_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (det P, i, A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det P, i + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))) = det (fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (P, i, A) else (fst (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)), i + 1, snd (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)))))
[PROOF STEP]
using det_fst_Gauss_Jordan_in_ij_PA_eq_fst_Gauss_Jordan_in_ij_det_P
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_in_ij_det_P ?A ?i ?j) * det ?P = det (fst (Gauss_Jordan_in_ij_PA (?P, ?A) ?i ?j))

goal (1 subgoal):
 1. fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (det P, i, A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * det P, i + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)))) = det (fst (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (P, i, A) else (fst (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)), i + 1, snd (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)))))
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_snd_Gauss_Jordan_column_k_det_P_eq_fst_snd_Gauss_Jordan_column_k_PA:
shows "fst (snd (Gauss_Jordan_column_k_det_P (n,i,A) k)) = fst (snd (Gauss_Jordan_column_k_PA (P,i,A) k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (Gauss_Jordan_column_k_det_P (n, i, A) k)) = fst (snd (Gauss_Jordan_column_k_PA (P, i, A) k))
[PROOF STEP]
unfolding Gauss_Jordan_column_k_det_P_def Gauss_Jordan_column_k_PA_def Let_def snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (n, i, A) else (fst (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k)) * n, i + 1, snd (Gauss_Jordan_in_ij_det_P A (mod_type_class.from_nat i) (mod_type_class.from_nat k))))) = fst (snd (if (\<forall>m\<ge>mod_type_class.from_nat i. A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> i = nrows A then (P, i, A) else (fst (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)), i + 1, snd (Gauss_Jordan_in_ij_PA (P, A) (mod_type_class.from_nat i) (mod_type_class.from_nat k)))))
[PROOF STEP]
by auto


[STATEMENT]
lemma snd_Gauss_Jordan_det_P_is_Gauss_Jordan:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "snd (Gauss_Jordan_det_P A) = (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_det_P A) = Gauss_Jordan A
[PROOF STEP]
unfolding Gauss_Jordan_det_P_def Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Gauss_Jordan_upt_k_det_P A (ncols A - 1)) = Gauss_Jordan_upt_k A (ncols A - 1)
[PROOF STEP]
unfolding snd_Gauss_Jordan_upt_k_det_P_is_snd_Gauss_Jordan_upt_k_PA
snd_Gauss_Jordan_upt_k_PA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_upt_k A (ncols A - 1) = Gauss_Jordan_upt_k A (ncols A - 1)
[PROOF STEP]
..


[STATEMENT]
lemma det_snd_Gauss_Jordan_det_P[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "det (snd (Gauss_Jordan_det_P A)) = prod (\<lambda>i. (snd (Gauss_Jordan_det_P A))$i$i) (UNIV:: 'n set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (snd (Gauss_Jordan_det_P A)) = (\<Prod>i\<in>UNIV. snd (Gauss_Jordan_det_P A) $ i $ i)
[PROOF STEP]
unfolding snd_Gauss_Jordan_det_P_is_Gauss_Jordan det_Gauss_Jordan
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i\<in>UNIV. Gauss_Jordan A $ i $ i) = (\<Prod>i\<in>UNIV. Gauss_Jordan A $ i $ i)
[PROOF STEP]
..


[STATEMENT]
lemma det_fst_Gauss_Jordan_PA_eq_fst_Gauss_Jordan_det_P:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "fst (Gauss_Jordan_det_P A) = det (fst (Gauss_Jordan_PA A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_det_P A) = det (fst (Gauss_Jordan_PA A))
[PROOF STEP]
by (unfold Gauss_Jordan_det_P_def Gauss_Jordan_PA_def, rule det_fst_Gauss_Jordan_upt_k_PA_eq_fst_Gauss_Jordan_upt_k_det_P)


[STATEMENT]
lemma fst_Gauss_Jordan_det_P_not_0:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "fst (Gauss_Jordan_det_P A) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Gauss_Jordan_det_P A) \<noteq> (0::'a)
[PROOF STEP]
unfolding det_fst_Gauss_Jordan_PA_eq_fst_Gauss_Jordan_det_P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (fst (Gauss_Jordan_PA A)) \<noteq> (0::'a)
[PROOF STEP]
by (metis (mono_tags) det_I det_mul invertible_fst_Gauss_Jordan_PA matrix_inv_right mult_zero_left zero_neq_one)


[STATEMENT]
lemma det_code_equation[code_unfold]:
fixes A::"'a::{field}^'n::{mod_type}^'n::{mod_type}"
shows "det A = (let A' = Gauss_Jordan_det_P A in prod (\<lambda>i. (snd (A'))$i$i) (UNIV::'n set)/(fst (A')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (let A' = Gauss_Jordan_det_P A in (\<Prod>i\<in>UNIV. snd A' $ i $ i) / fst A')
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det A = (\<Prod>i\<in>UNIV. snd (Gauss_Jordan_det_P A) $ i $ i) / fst (Gauss_Jordan_det_P A)
[PROOF STEP]
using det_Gauss_Jordan_det_P[of A]
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_det_P A) * det A = det (snd (Gauss_Jordan_det_P A))

goal (1 subgoal):
 1. det A = (\<Prod>i\<in>UNIV. snd (Gauss_Jordan_det_P A) $ i $ i) / fst (Gauss_Jordan_det_P A)
[PROOF STEP]
unfolding det_snd_Gauss_Jordan_det_P
[PROOF STATE]
proof (prove)
using this:
fst (Gauss_Jordan_det_P A) * det A = (\<Prod>i\<in>UNIV. snd (Gauss_Jordan_det_P A) $ i $ i)

goal (1 subgoal):
 1. det A = (\<Prod>i\<in>UNIV. snd (Gauss_Jordan_det_P A) $ i $ i) / fst (Gauss_Jordan_det_P A)
[PROOF STEP]
by (simp add: fst_Gauss_Jordan_det_P_not_0 nonzero_eq_divide_eq ac_simps)


[STATEMENT]
lemma enat_in_Inf:
  fixes S :: "enat set"
  assumes "Inf S \<noteq> top"
  shows "Inf S \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf S \<in> S
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
assume A: "~?thesis"
[PROOF STATE]
proof (state)
this:
Inf S \<notin> S

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
obtain n where Inf_conv: "Inf S = enat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. Inf S = enat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Inf S \<noteq> top

goal (1 subgoal):
 1. (\<And>n. Inf S = enat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: top_enat_def)
[PROOF STATE]
proof (state)
this:
Inf S = enat n

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Inf S = enat n

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
assume "s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
have "Inf S \<le> s"
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. Inf S \<le> s
[PROOF STEP]
by (rule complete_lattice_class.Inf_lower)
[PROOF STATE]
proof (state)
this:
Inf S \<le> s

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Inf S \<le> s

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
have "Inf S \<noteq> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf S \<noteq> s
[PROOF STEP]
using A \<open>s \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
Inf S \<notin> S
s \<in> S

goal (1 subgoal):
 1. Inf S \<noteq> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf S \<noteq> s

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Inf S \<le> s
Inf S \<noteq> s
[PROOF STEP]
have "Inf S < s"
[PROOF STATE]
proof (prove)
using this:
Inf S \<le> s
Inf S \<noteq> s

goal (1 subgoal):
 1. Inf S < s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Inf S < s

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
with Inf_conv
[PROOF STATE]
proof (chain)
picking this:
Inf S = enat n
Inf S < s
[PROOF STEP]
have "enat (Suc n) \<le> s"
[PROOF STATE]
proof (prove)
using this:
Inf S = enat n
Inf S < s

goal (1 subgoal):
 1. enat (Suc n) \<le> s
[PROOF STEP]
by (cases s) auto
[PROOF STATE]
proof (state)
this:
enat (Suc n) \<le> s

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s2 \<in> S \<Longrightarrow> enat (Suc n) \<le> ?s2

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?s2 \<in> S \<Longrightarrow> enat (Suc n) \<le> ?s2
[PROOF STEP]
have "enat (Suc n) \<le> Inf S"
[PROOF STATE]
proof (prove)
using this:
?s2 \<in> S \<Longrightarrow> enat (Suc n) \<le> ?s2

goal (1 subgoal):
 1. enat (Suc n) \<le> Inf S
[PROOF STEP]
by (simp add: le_Inf_iff)
[PROOF STATE]
proof (state)
this:
enat (Suc n) \<le> Inf S

goal (1 subgoal):
 1. Inf S \<notin> S \<Longrightarrow> False
[PROOF STEP]
with Inf_conv
[PROOF STATE]
proof (chain)
picking this:
Inf S = enat n
enat (Suc n) \<le> Inf S
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Inf S = enat n
enat (Suc n) \<le> Inf S

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enat_in_INF:
  fixes f :: "'a \<Rightarrow> enat"
  assumes "(INF x\<in> S. f x) \<noteq> top"
  obtains x where "x \<in> S" and "(INF x\<in> S. f x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; Inf (f ` S) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; Inf (f ` S) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Inf (f ` S) \<noteq> top
[PROOF STEP]
have "(INF x\<in> S. f x) \<in> f ` S"
[PROOF STATE]
proof (prove)
using this:
Inf (f ` S) \<noteq> top

goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
using enat_in_Inf [of "f ` S"]
[PROOF STATE]
proof (prove)
using this:
Inf (f ` S) \<noteq> top
Inf (f ` S) \<noteq> top \<Longrightarrow> Inf (f ` S) \<in> f ` S

goal (1 subgoal):
 1. Inf (f ` S) \<in> f ` S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf (f ` S) \<in> f ` S

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; Inf (f ` S) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf (f ` S) \<in> f ` S
[PROOF STEP]
obtain x where "x \<in> S" "(INF x\<in> S. f x) = f x"
[PROOF STATE]
proof (prove)
using this:
Inf (f ` S) \<in> f ` S

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; Inf (f ` S) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> S
Inf (f ` S) = f x

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; Inf (f ` S) = f x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> S
Inf (f ` S) = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> S
Inf (f ` S) = f x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enat_less_INF_I:
  fixes f :: "'a \<Rightarrow> enat"
  assumes not_inf: "x \<noteq> \<infinity>" and less: "\<And>y. y \<in> S \<Longrightarrow> x < f y"
  shows "x < (INF y\<in>S. f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < Inf (f ` S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> \<infinity>
?y \<in> S \<Longrightarrow> x < f ?y

goal (1 subgoal):
 1. x < Inf (f ` S)
[PROOF STEP]
by (auto simp: Suc_ile_eq[symmetric] INF_greatest)


[STATEMENT]
lemma enat_le_Sup_iff:
  "enat k \<le> Sup M \<longleftrightarrow> k = 0 \<or> (\<exists>m \<in> M. enat k \<le> m)" (is "?L \<longleftrightarrow> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
 2. \<not> ?P \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
assume "k = 0"
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
 2. \<not> ?P \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0

goal (1 subgoal):
 1. (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
by (auto simp: enat_0)
[PROOF STATE]
proof (state)
this:
(enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
assume "k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat k \<le> Sup M \<Longrightarrow> k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
 2. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
assume ?L
[PROOF STATE]
proof (state)
this:
enat k \<le> Sup M

goal (2 subgoals):
 1. enat k \<le> Sup M \<Longrightarrow> k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
 2. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat k \<le> Sup M
[PROOF STEP]
have "\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m"
[PROOF STATE]
proof (prove)
using this:
enat k \<le> Sup M

goal (1 subgoal):
 1. \<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m
[PROOF STEP]
by (metis Max_in Sup_enat_def finite_enat_bounded linorder_linear)
[PROOF STATE]
proof (state)
this:
\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m

goal (2 subgoals):
 1. enat k \<le> Sup M \<Longrightarrow> k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
 2. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
with \<open>k \<noteq> 0\<close> and \<open>?L\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0
enat k \<le> Sup M
\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m
[PROOF STEP]
show ?R
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
enat k \<le> Sup M
\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m

goal (1 subgoal):
 1. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
[PROOF STEP]
unfolding Sup_enat_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
enat k \<le> (if M = {} then 0 else if finite M then Max M else \<infinity>)
\<lbrakk>enat k \<le> (if finite M then Max M else \<infinity>); M \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>m\<in>M. enat k \<le> m

goal (1 subgoal):
 1. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
[PROOF STEP]
by (cases "M={}") (auto simp add: enat_0[symmetric])
[PROOF STATE]
proof (state)
this:
k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)

goal (1 subgoal):
 1. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
assume ?R
[PROOF STATE]
proof (state)
this:
k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)

goal (1 subgoal):
 1. k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m) \<Longrightarrow> enat k \<le> Sup M
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m)

goal (1 subgoal):
 1. enat k \<le> Sup M
[PROOF STEP]
by (auto simp: enat_0 intro: complete_lattice_class.Sup_upper2)
[PROOF STATE]
proof (state)
this:
enat k \<le> Sup M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(enat k \<le> Sup M) = (k = 0 \<or> (\<exists>m\<in>M. enat k \<le> m))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma enat_neq_zero_cancel_iff[simp]:
  "0 \<noteq> enat n \<longleftrightarrow> 0 \<noteq> n"
  "enat n \<noteq> 0 \<longleftrightarrow> n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<noteq> enat n) = (0 \<noteq> n) &&& (enat n \<noteq> 0) = (n \<noteq> 0)
[PROOF STEP]
by (auto simp: enat_0[symmetric])


[STATEMENT]
lemma natceiling_lessD: "nat(ceiling x) < n \<Longrightarrow> x < real n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>x\<rceil> < n \<Longrightarrow> x < real n
[PROOF STEP]
by linarith


[STATEMENT]
lemma le_natceiling_iff:
  fixes n :: nat and r :: real
  shows "n \<le> r \<Longrightarrow> n \<le> nat(ceiling r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n \<le> r \<Longrightarrow> n \<le> nat \<lceil>r\<rceil>
[PROOF STEP]
by linarith


[STATEMENT]
lemma natceiling_le_iff:
  fixes n :: nat and r :: real
  shows "r \<le> n \<Longrightarrow> nat(ceiling r) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<le> real n \<Longrightarrow> nat \<lceil>r\<rceil> \<le> n
[PROOF STEP]
by linarith


[STATEMENT]
lemma dist_real_noabs_less:
  fixes a b c :: real assumes "dist a b < c" shows "a - b < c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - b < c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
dist a b < c

goal (1 subgoal):
 1. a - b < c
[PROOF STEP]
by (simp add: dist_real_def)


[STATEMENT]
lemma n_choose_2_nat:
  fixes n :: nat shows "(n choose 2) = (n * (n - 1)) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose 2 = n * (n - 1) div 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n choose 2 = n * (n - 1) div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose 2 = n * (n - 1) div 2
[PROOF STEP]
proof (cases "2 \<le> n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
 2. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 \<le> n

goal (2 subgoals):
 1. 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
 2. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> n
[PROOF STEP]
obtain m where "n = Suc (Suc m)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> n

goal (1 subgoal):
 1. (\<And>m. n = Suc (Suc m) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis add_Suc le_Suc_ex numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
n = Suc (Suc m)

goal (2 subgoals):
 1. 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
 2. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n = Suc (Suc m)

goal (2 subgoals):
 1. 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
 2. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
have "(n choose 2) = (fact n div fact (n - 2)) div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n choose 2 = fact n div fact (n - 2) div 2
[PROOF STEP]
using \<open>2 \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
2 \<le> n

goal (1 subgoal):
 1. n choose 2 = fact n div fact (n - 2) div 2
[PROOF STEP]
by (simp add: binomial_altdef_nat
        div_mult2_eq[symmetric] mult.commute numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
n choose 2 = fact n div fact (n - 2) div 2

goal (2 subgoals):
 1. 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
 2. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n = Suc (Suc m)
n choose 2 = fact n div fact (n - 2) div 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = Suc (Suc m)
n choose 2 = fact n div fact (n - 2) div 2

goal (1 subgoal):
 1. n choose 2 = n * (n - 1) div 2
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
n choose 2 = n * (n - 1) div 2

goal (1 subgoal):
 1. \<not> 2 \<le> n \<Longrightarrow> n choose 2 = n * (n - 1) div 2
[PROOF STEP]
qed (auto simp: binomial_eq_0)
[PROOF STATE]
proof (state)
this:
n choose 2 = n * (n - 1) div 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_less_one:
  fixes x::real
  assumes "1 < x" "y < 0"
  shows "x powr y < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr y < 1
[PROOF STEP]
using assms less_log_iff
[PROOF STATE]
proof (prove)
using this:
1 < x
y < 0
\<lbrakk>1 < ?b; 0 < ?x\<rbrakk> \<Longrightarrow> (?y < log ?b ?x) = (?b powr ?y < ?x)

goal (1 subgoal):
 1. x powr y < 1
[PROOF STEP]
by force


[STATEMENT]
lemma powr_le_one_le: "\<And>x y::real. 0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> y \<Longrightarrow> x powr y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
fix x y :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
assume "0 < x" "x \<le> 1" "1 \<le> y"
[PROOF STATE]
proof (state)
this:
0 < x
x \<le> 1
1 \<le> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
have "x powr y = (1 / (1 / x)) powr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr y = (1 / (1 / x)) powr y
[PROOF STEP]
using \<open>0 < x\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. x powr y = (1 / (1 / x)) powr y
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x powr y = (1 / (1 / x)) powr y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x powr y = (1 / (1 / x)) powr y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
have "\<dots> = 1 / (1 / x) powr y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / (1 / x)) powr y = 1 / (1 / x) powr y
[PROOF STEP]
using \<open>0 < x\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. (1 / (1 / x)) powr y = 1 / (1 / x) powr y
[PROOF STEP]
by (simp add: powr_divide)
[PROOF STATE]
proof (state)
this:
(1 / (1 / x)) powr y = 1 / (1 / x) powr y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 / (1 / x)) powr y = 1 / (1 / x) powr y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
have "\<dots> \<le> 1 / (1 / x) powr 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1
[PROOF STEP]
have "1 \<le> 1 / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 1 / x
[PROOF STEP]
using \<open>0 < x\<close> \<open>x \<le> 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x
x \<le> 1

goal (1 subgoal):
 1. 1 \<le> 1 / x
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> 1 / x

goal (1 subgoal):
 1. 1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> 1 / x
[PROOF STEP]
have "(1 / x) powr 1  \<le> (1 / x) powr y"
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 / x

goal (1 subgoal):
 1. (1 / x) powr 1 \<le> (1 / x) powr y
[PROOF STEP]
using \<open>0 < x\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 / x
0 < x

goal (1 subgoal):
 1. (1 / x) powr 1 \<le> (1 / x) powr y
[PROOF STEP]
using \<open>1 \<le> y\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> 1 / x
0 < x
1 \<le> y

goal (1 subgoal):
 1. (1 / x) powr 1 \<le> (1 / x) powr y
[PROOF STEP]
by ( simp only: powr_mono)
[PROOF STATE]
proof (state)
this:
(1 / x) powr 1 \<le> (1 / x) powr y

goal (1 subgoal):
 1. 1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(1 / x) powr 1 \<le> (1 / x) powr y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(1 / x) powr 1 \<le> (1 / x) powr y

goal (1 subgoal):
 1. 1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1
[PROOF STEP]
by (metis \<open>1 \<le> 1 / x\<close> \<open>1 \<le> y\<close> neg_le_iff_le powr_minus_divide powr_mono)
[PROOF STATE]
proof (state)
this:
1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / (1 / x) powr y \<le> 1 / (1 / x) powr 1

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
have "\<dots> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (1 / x) powr 1 \<le> x
[PROOF STEP]
using \<open>0 < x\<close>
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. 1 / (1 / x) powr 1 \<le> x
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
1 / (1 / x) powr 1 \<le> x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>0 < x; x \<le> 1; 1 \<le> y\<rbrakk> \<Longrightarrow> x powr y \<le> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x powr y \<le> x
[PROOF STEP]
show "?thesis x y"
[PROOF STATE]
proof (prove)
using this:
x powr y \<le> x

goal (1 subgoal):
 1. x powr y \<le> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x powr y \<le> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_set_tl: "x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set (tl xs) \<Longrightarrow> x \<in> set xs
[PROOF STEP]
by (cases xs) auto