[STATEMENT]
lemma step_symb_dest: "step_symb q q' \<Longrightarrow> q \<in> SQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb q q' \<Longrightarrow> q \<in> SQ
[PROOF STEP]
by (auto simp add: step_symb_def)


[STATEMENT]
lemma L_infinity_space:
  "space\<^sub>N (\<LL> \<infinity> M) = {f \<in> borel_measurable M. \<exists>C. AE x in M. \<bar>f x\<bar> \<le> C}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space\<^sub>N (\<LL> \<infinity> M) = {f \<in> borel_measurable M. \<exists>C. AE x in M. \<bar>f x\<bar> \<le> C}
[PROOF STEP]
proof (auto simp del: infinity_ennreal_def)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 3. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 3. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
assume H: "f \<in> space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (3 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> x \<in> borel_measurable M
 2. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 3. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
show "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
using this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
unfolding space\<^sub>N_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f. eNorm (\<LL> \<infinity> M) f < \<infinity>}

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using L_infinity(1)[of M] top.not_eq_extremum
[PROOF STATE]
proof (prove)
using this:
f \<in> {f. eNorm (\<LL> \<infinity> M) f < \<infinity>}
eNorm (\<LL> \<infinity> M) ?f = (if ?f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>?f x\<bar>)) else \<infinity>)
(?a \<noteq> \<top>) = (?a < \<top>)

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M

goal (2 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 2. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
[PROOF STEP]
have *: "esssup M (\<lambda>x. \<bar>f x\<bar>) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) < \<infinity>
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
f \<in> space\<^sub>N (\<LL> \<infinity> M)

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) < \<infinity>
[PROOF STEP]
unfolding space\<^sub>N_def L_infinity(1)[of M]
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
f \<in> {f. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) < \<infinity>}

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) < \<infinity>
[PROOF STEP]
by (auto simp add: e2ennreal_infty)
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) < \<infinity>

goal (2 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 2. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
define C where "C = real_of_ereal(esssup M (\<lambda>x. \<bar>f x\<bar>))"
[PROOF STATE]
proof (state)
this:
C = real_of_ereal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>))

goal (2 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 2. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
have "AE x in M. ereal \<bar>f x\<bar> \<le> ereal C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
proof (cases "emeasure M (space M) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. emeasure M (space M) = 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
 2. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
emeasure M (space M) = 0

goal (2 subgoals):
 1. emeasure M (space M) = 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
 2. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = 0

goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
using emeasure_0_AE
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = 0
emeasure ?M (space ?M) = 0 \<Longrightarrow> almost_everywhere ?M ?P

goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. ereal \<bar>f x\<bar> \<le> ereal C

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
emeasure M (space M) \<noteq> 0

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) \<noteq> 0
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) \<noteq> 0

goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
using esssup_mono[of "\<lambda>x. 0" M "(\<lambda>x. \<bar>f x\<bar>)"] esssup_const[OF False, of "0::ereal"]
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) \<noteq> 0
\<lbrakk>(\<lambda>x. 0) \<in> borel_measurable M; \<And>x. 0 \<le> ereal \<bar>f x\<bar>\<rbrakk> \<Longrightarrow> esssup M (\<lambda>x. 0) \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
esssup M (\<lambda>x. 0) = 0

goal (1 subgoal):
 1. 0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) = ereal C"
[PROOF STATE]
proof (prove)
using this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal C
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal (real_of_ereal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)))
[PROOF STEP]
using * ereal_real
[PROOF STATE]
proof (prove)
using this:
0 \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) < \<infinity>
ereal (real_of_ereal ?x) = (if \<bar>?x\<bar> = \<infinity> then 0 else ?x)

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal (real_of_ereal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal C

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal C

goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
using esssup_AE[of "(\<lambda>x. ereal \<bar>f x\<bar>)" M]
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) = ereal C
AE x in M. ereal \<bar>f x\<bar> \<le> esssup M (\<lambda>x. ereal \<bar>f x\<bar>)

goal (1 subgoal):
 1. AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. ereal \<bar>f x\<bar> \<le> ereal C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE x in M. ereal \<bar>f x\<bar> \<le> ereal C

goal (2 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 2. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. ereal \<bar>f x\<bar> \<le> ereal C
[PROOF STEP]
have "AE x in M. \<bar>f x\<bar> \<le> C"
[PROOF STATE]
proof (prove)
using this:
AE x in M. ereal \<bar>f x\<bar> \<le> ereal C

goal (1 subgoal):
 1. AE x in M. \<bar>f x\<bar> \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. \<bar>f x\<bar> \<le> C

goal (2 subgoals):
 1. \<And>x. x \<in> space\<^sub>N (\<LL> \<infinity> M) \<Longrightarrow> \<exists>C. AE xa in M. \<bar>x xa\<bar> \<le> C
 2. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. \<bar>f x\<bar> \<le> C
[PROOF STEP]
show "\<exists>C. AE x in M. \<bar>f x\<bar> \<le> C"
[PROOF STATE]
proof (prove)
using this:
AE x in M. \<bar>f x\<bar> \<le> C

goal (1 subgoal):
 1. \<exists>C. AE x in M. \<bar>f x\<bar> \<le> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>C. AE x in M. \<bar>f x\<bar> \<le> C

goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
fix f::"'a \<Rightarrow> real" and C::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
assume H: "f \<in> borel_measurable M" "AE x in M. \<bar>f x\<bar> \<le> C"
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C

goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
[PROOF STEP]
have "esssup M (\<lambda>x. \<bar>f x\<bar>) \<le> C"
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
using esssup_I
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable M
AE x in M. \<bar>f x\<bar> \<le> C
\<lbrakk>?f \<in> borel_measurable ?M; AE x in ?M. ?f x \<le> ?c\<rbrakk> \<Longrightarrow> esssup ?M ?f \<le> ?c

goal (1 subgoal):
 1. esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
[PROOF STEP]
have "eNorm (\<LL> \<infinity> M) f \<le> C"
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. eNorm (\<LL> \<infinity> M) f \<le> ennreal C
[PROOF STEP]
unfolding L_infinity(1)
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> ennreal C
[PROOF STEP]
using H(1)
[PROOF STATE]
proof (prove)
using this:
esssup M (\<lambda>x. ereal \<bar>f x\<bar>) \<le> ereal C
f \<in> borel_measurable M

goal (1 subgoal):
 1. (if f \<in> borel_measurable M then e2ennreal (esssup M (\<lambda>x. ereal \<bar>f x\<bar>)) else \<infinity>) \<le> ennreal C
[PROOF STEP]
by auto (metis e2ennreal_ereal e2ennreal_mono)
[PROOF STATE]
proof (state)
this:
eNorm (\<LL> \<infinity> M) f \<le> ennreal C

goal (1 subgoal):
 1. \<And>x C. \<lbrakk>x \<in> borel_measurable M; AE xa in M. \<bar>x xa\<bar> \<le> C\<rbrakk> \<Longrightarrow> x \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm (\<LL> \<infinity> M) f \<le> ennreal C
[PROOF STEP]
show "f \<in> space\<^sub>N (\<LL> \<infinity> M)"
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f \<le> ennreal C

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
using spaceN_iff le_less_trans
[PROOF STATE]
proof (prove)
using this:
eNorm (\<LL> \<infinity> M) f \<le> ennreal C
(?x \<in> space\<^sub>N ?N) = (eNorm ?N ?x < \<infinity>)
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. f \<in> space\<^sub>N (\<LL> \<infinity> M)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<in> space\<^sub>N (\<LL> \<infinity> M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma member_bulkload [simp]:
  "member (bulkload xs) (x :: 'a) \<longleftrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. member (bulkload xs) x = (x \<in> set xs)
[PROOF STEP]
by transfer (auto simp add: linorder.rbt_lookup_rbt_bulkload[OF set_linorder] rbt_comps map_of_map_Pair_const split: if_split_asm)


[STATEMENT]
lemma condition_2_part_5:
  fixes A::"'a::{field}^'columns::{mod_type}^'rows::{mod_type}" and k::nat
  defines ia:"ia\<equiv>(if \<forall>m. is_zero_row_upt_k m k A then 0 else to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
  defines B:"B\<equiv>(snd (Gauss_Jordan_column_k (ia,A) k))"
  assumes rref: "reduced_row_echelon_form_upt_k A k"
  and not_zero_i_suc_k: "\<not> is_zero_row_upt_k i (Suc k) B"
  and not_zero_m: "\<not> is_zero_row_upt_k m k A"
  and greatest_noteq_card: "Suc (to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A"
  and greatest_less_ma: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> ma"
  and A_ma_k_not_zero: "A $ ma $ from_nat k \<noteq> 0"
  shows "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $
  (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have ia2: "ia=to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
unfolding ia
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
using not_zero_m
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k m k A

goal (1 subgoal):
 1. (if \<forall>m. is_zero_row_upt_k m k A then 0 else mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
ia = mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have B_eq_Gauss: "B=Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
unfolding B Gauss_Jordan_column_k_def Let_def fst_conv snd_conv ia2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if (\<forall>m\<ge>mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1). A $ m $ mod_type_class.from_nat k = (0::'a)) \<or> mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 = nrows A then (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1, A) else (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 + 1, Gauss_Jordan_in_ij A (mod_type_class.from_nat (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)) (mod_type_class.from_nat k))) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>m\<ge>mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A))). A $ m $ mod_type_class.from_nat k = (0::'a)) \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> ((\<exists>m\<ge>mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A))). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A (mod_type_class.from_nat (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)))) (mod_type_class.from_nat k) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
unfolding from_nat_to_nat_greatest
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)) \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> ((\<exists>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
using greatest_noteq_card A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. ((\<forall>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k = (0::'a)) \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> (Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) = nrows A \<longrightarrow> A = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)) \<and> ((\<exists>m\<ge>(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows). A $ m $ mod_type_class.from_nat k \<noteq> (0::'a)) \<and> Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have greatest_plus_one_not_zero: "(GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
using suc_not_zero greatest_noteq_card
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> nrows A

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat ?a + 1 \<noteq> CARD(?'a) \<Longrightarrow> ?a + (1::?'a) \<noteq> (0::?'a)
Suc (mod_type_class.to_nat (GREATEST n. \<not> is_zero_row_upt_k n k A)) \<noteq> CARD('rows)

goal (1 subgoal):
 1. (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<noteq> (0::'rows)

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

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
hence not_zero_iB: "is_zero_row_upt_k i k B"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A

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

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

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero]
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k B

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
hence Gauss_Jordan_i_not_0: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k B

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using not_zero_i_suc_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k B
\<not> is_zero_row_upt_k i (Suc k) B

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
unfolding B_eq_Gauss
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))
\<not> is_zero_row_upt_k i (Suc k) (Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a)
\<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a))

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using from_nat_to_nat_id less_Suc_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a)
\<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ j = (0::'a))
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ n $ j = (0::'a))) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by (metis (lifting, no_types))
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have "i = ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
assume i_not_greatest: "i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (state)
this:
i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
have "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)
[PROOF STEP]
proof (rule Gauss_Jordan_in_ij_0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
 2. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
show "\<exists>n. A $ n $ from_nat k \<noteq> 0 \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. \<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. A $ n $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> n

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
show "i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
using i_not_greatest
[PROOF STATE]
proof (prove)
using this:
i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. i \<noteq> (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Gauss_Jordan_i_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (0::'a)
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
hence Gauss_Jordan_i_1: "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (from_nat k) = 1"
[PROOF STATE]
proof (prove)
using this:
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_1
[PROOF STATE]
proof (prove)
using this:
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
\<exists>n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n \<Longrightarrow> Gauss_Jordan_in_ij ?A ?i ?j $ ?i $ ?j = (1::?'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
i = (GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)
\<exists>n. ?A $ n $ ?j \<noteq> (0::?'a) \<and> ?i \<le> n \<Longrightarrow> Gauss_Jordan_in_ij ?A ?i ?j $ ?i $ ?j = (1::?'a)
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have Least_eq_k: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) = from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_i_not_0
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
show  "\<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0 \<Longrightarrow> from_nat k \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
using B_eq_Gauss is_zero_row_upt_k_def not_less not_zero_iB to_nat_le
[PROOF STATE]
proof (prove)
using this:
B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
is_zero_row_upt_k ?i ?k ?A = (\<forall>j. mod_type_class.to_nat j < ?k \<longrightarrow> ?A $ ?i $ j = (0::?'a))
(\<not> ?x < ?y) = (?y \<le> ?x)
is_zero_row_upt_k i k B
?y < mod_type_class.from_nat ?k \<Longrightarrow> mod_type_class.to_nat ?y < ?k

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> mod_type_class.from_nat k \<le> y
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ 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 ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = mod_type_class.from_nat k

goal (2 subgoals):
 1. is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
 2. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using Gauss_Jordan_i_1
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding Least_eq_k
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ mod_type_class.from_nat k = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
obtain j where Aij_not_0: "A $ i $ j \<noteq> 0" and j_le_k: "to_nat j < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>A $ i $ j \<noteq> (0::'a); mod_type_class.to_nat j < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $ i $ j \<noteq> (0::'a)
mod_type_class.to_nat j < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have least_le_k: "to_nat (LEAST ka. A $ i $ ka \<noteq> 0) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
[PROOF STEP]
by (metis (lifting, mono_tags) Aij_not_0 j_le_k less_trans linorder_cases not_less_Least to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have least_le_j: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) \<le> j
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero j_le_k]
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j

goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) \<le> j
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) \<le> j
[PROOF STEP]
using Aij_not_0 False not_le_imp_less not_less_Least
[PROOF STATE]
proof (prove)
using this:
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ j = A $ ?i $ j
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
A $ i $ j \<noteq> (0::'a)
\<not> is_zero_row_upt_k i k A
\<not> ?y \<le> ?x \<Longrightarrow> ?x < ?y
?k < (LEAST x. ?P x) \<Longrightarrow> \<not> ?P ?k

goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) \<le> j
[PROOF STEP]
by (metis (mono_tags))
[PROOF STATE]
proof (state)
this:
(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) \<le> j

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have Least_eq: "(LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0)
      = (LEAST ka. A $ i $ ka \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (LEAST ka. A $ i $ ka \<noteq> (0::'a))
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
 2. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> 0) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref False _ greatest_plus_one_not_zero] least_le_k False rref_upt_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
\<not> is_zero_row_upt_k i k A
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using  A_ma_k_not_zero B_eq_Gauss greatest_less_ma zero_neq_one
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
\<not> is_zero_row_upt_k i k A
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
B = Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma
(0::?'a) \<noteq> (1::?'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
assume Gauss_Jordan_y:"Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a) \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
show "(LEAST ka. A $ i $ ka \<noteq> 0) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
proof (cases "to_nat y < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> mod_type_class.to_nat y < k

goal (2 subgoals):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
 2. \<not> mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat y < k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
using least_le_k less_trans not_le_imp_less to_nat_from_nat to_nat_le
[PROOF STATE]
proof (prove)
using this:
\<not> mod_type_class.to_nat y < k
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
\<lbrakk>?x < ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
\<not> ?y \<le> ?x \<Longrightarrow> ?x < ?y
mod_type_class.to_nat ?j = ?k \<Longrightarrow> mod_type_class.from_nat ?k = ?j
?y < mod_type_class.from_nat ?k \<Longrightarrow> mod_type_class.to_nat ?y < ?k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat y < k

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
have "A $ i $ y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_y
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref not_zero_m _ greatest_plus_one_not_zero True]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y

goal (1 subgoal):
 1. A $ i $ y \<noteq> (0::'a)
[PROOF STEP]
using A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ y \<noteq> (0::'a)
\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ y = A $ ?i $ y
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

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

goal (1 subgoal):
 1. mod_type_class.to_nat y < k \<Longrightarrow> (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
using Least_le
[PROOF STATE]
proof (prove)
using this:
A $ i $ y \<noteq> (0::'a)
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. (LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST ka. A $ i $ ka \<noteq> (0::'a)) \<le> y

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

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
have "A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + 1) (from_nat k) $ i $ ka \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding Least_eq
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i k A
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding Least_eq
[PROOF STATE]
proof (prove)
using this:
A $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using Gauss_Jordan_in_ij_preserves_previous_elements[OF rref False _ greatest_plus_one_not_zero]
[PROOF STATE]
proof (prove)
using this:
A $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using least_le_k A_ma_k_not_zero greatest_less_ma
[PROOF STATE]
proof (prove)
using this:
A $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
\<lbrakk>\<exists>m. A $ m $ mod_type_class.from_nat k \<noteq> (0::'a) \<and> (GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows) \<le> m; mod_type_class.to_nat ?j < k\<rbrakk> \<Longrightarrow> Gauss_Jordan_in_ij A ((GREATEST m. \<not> is_zero_row_upt_k m k A) + (1::'rows)) (mod_type_class.from_nat k) $ ?i $ ?j = A $ ?i $ ?j
mod_type_class.to_nat (LEAST ka. A $ i $ ka \<noteq> (0::'a)) < k
A $ ma $ mod_type_class.from_nat k \<noteq> (0::'a)
(GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows) \<le> ma

goal (1 subgoal):
 1. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. A $ i $ ka \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ (LEAST ka. Gauss_Jordan_in_ij A ((GREATEST n. \<not> is_zero_row_upt_k n k A) + (1::'rows)) (mod_type_class.from_nat k) $ i $ ka \<noteq> (0::'a)) = (1::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prodag_pOp:"\<forall>k\<in>I. aGroup (A k) \<Longrightarrow>
                  pop (prodag I A) = prod_pOp I A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<in>I. aGroup (A k) \<Longrightarrow> (\<plusminus>\<^bsub>a\<Pi>\<^bsub>I\<^esub> A\<^esub>) = prod_pOp I A
[PROOF STEP]
apply (simp add:prodag_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma permChainFresh[simp]:
  fixes x    :: name
  and   xvec :: "name list"
  and   yvec :: "name list"
  and   p    :: "'a::pt_name"

  assumes "x \<sharp> xvec"
  and     "x \<sharp> yvec"
  and     "length xvec = length yvec"

  shows "x \<sharp> [xvec yvec] \<bullet>\<^sub>v p = x \<sharp> p"
  and   "x \<sharp> [xvec yvec]\<^sup>- \<bullet>\<^sub>v p = x \<sharp> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v p = x \<sharp> p &&& x \<sharp> [xvec yvec]\<^sup>- \<bullet>\<^sub>v p = x \<sharp> p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> xvec
x \<sharp> yvec
length xvec = length yvec

goal (1 subgoal):
 1. x \<sharp> [xvec yvec] \<bullet>\<^sub>v p = x \<sharp> p &&& x \<sharp> [xvec yvec]\<^sup>- \<bullet>\<^sub>v p = x \<sharp> p
[PROOF STEP]
by(auto simp add: fresh_left calcChainAtomRev calcChainAtom)


[STATEMENT]
lemma establish_convergence_static_subset :
  "set T \<subseteq> set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define \<alpha> where \<alpha>: "\<alpha> = V (t_source t)"
[PROOF STATE]
proof (state)
this:
\<alpha> = V (t_source t)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define xy where xy: "xy = (t_input t, t_output t)"
[PROOF STATE]
proof (state)
this:
xy = (t_input t, t_output t)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define \<beta> where \<beta>: "\<beta> = V (t_target t)"
[PROOF STATE]
proof (state)
this:
\<beta> = V (t_target t)

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define qSource where qSource: "qSource = (after_initial M (V (t_source t)))"
[PROOF STATE]
proof (state)
this:
qSource = after_initial M (V (t_source t))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define qTarget where qTarget: "qTarget = (after_initial M (V (t_target t)))"
[PROOF STATE]
proof (state)
this:
qTarget = after_initial M (V (t_target t))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define k where k: "k = m - size_r M"
[PROOF STATE]
proof (state)
this:
k = m - size_r M

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define ttc where ttc : "ttc = [] # traces_to_check M qTarget k"
[PROOF STATE]
proof (state)
this:
ttc = [] # traces_to_check M qTarget k

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
define handleTrace where handleTrace: "handleTrace = (\<lambda> (T,G) u .
          if is_in_language M qTarget u
            then let
                qu = FSM.after M qTarget u;
                ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu);
                appendDistTrace = (\<lambda> (T,G) w . let
                                                  (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u@w) False (append_heuristic_input M)
                                                in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u@w) False (append_heuristic_input M))
                in foldl appendDistTrace (T,G) ws
            else let
                (T',G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy#u) False (append_heuristic_input M)
                in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))"
[PROOF STATE]
proof (state)
this:
handleTrace = (\<lambda>(T, G) u. if is_in_language M qTarget u then let qu = FSM.after M qTarget u; ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
have *:"establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T,G) ttc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T, G) ttc
[PROOF STEP]
unfolding establish_convergence_static.simps \<alpha> xy \<beta> qSource qTarget k ttc handleTrace Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>(T, G) u. if is_in_language M (after_initial M (V (t_target t))) u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M (after_initial M (V (t_target t))) u))) else case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) u False (append_heuristic_input M)) (T, G) ([] # traces_to_check M (after_initial M (V (t_target t))) (m - size_r M)) = foldl (\<lambda>(T, G) u. if is_in_language M (after_initial M (V (t_target t))) u then foldl (\<lambda>(T, G) w. case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u @ w) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) (u @ w) False (append_heuristic_input M)) (T, G) (sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) (FSM.after M (after_initial M (V (t_target t))) u))) else case distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u) False (append_heuristic_input M) of (T', G') \<Rightarrow> distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) u False (append_heuristic_input M)) (T, G) ([] # traces_to_check M (after_initial M (V (t_target t))) (m - size_r M))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t = foldl handleTrace (T, G) ttc

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) ttc))
[PROOF STEP]
proof (induction ttc rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) []))
 2. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) []))
 2. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) []))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) []))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
case (snoc io ttc)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) ttc))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
have *:"foldl handleTrace (T, G) (ttc@[io]) = handleTrace (foldl handleTrace (T,G) ttc) io"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl handleTrace (T, G) (ttc @ [io]) = handleTrace (foldl handleTrace (T, G) ttc) io
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
foldl handleTrace (T, G) (ttc @ [io]) = handleTrace (foldl handleTrace (T, G) ttc) io

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
have "\<And> u T G . set T \<subseteq> set (fst (handleTrace (T,G) u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
using handleTrace_subset_helper[of handleTrace] handleTrace
[PROOF STATE]
proof (prove)
using this:
handleTrace = (\<lambda>(T, G) u. if is_in_language ?M ?qTarget u then let qu = FSM.after ?M ?qTarget u; ws = sorted_list_of_maximal_sequences_in_tree (?dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension ?M T G ?cg_lookup ?cg_insert ?\<alpha> (?xy # u @ w) False (append_heuristic_input ?M) in distribute_extension ?M T' G' ?cg_lookup ?cg_insert ?\<beta> (u @ w) False (append_heuristic_input ?M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension ?M T G ?cg_lookup ?cg_insert ?\<alpha> (?xy # u) False (append_heuristic_input ?M) in distribute_extension ?M T' G' ?cg_lookup ?cg_insert ?\<beta> u False (append_heuristic_input ?M)) \<Longrightarrow> Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))
handleTrace = (\<lambda>(T, G) u. if is_in_language M qTarget u then let qu = FSM.after M qTarget u; ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> (u @ w) False (append_heuristic_input M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension M T G cg_lookup cg_insert \<alpha> (xy # u) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert \<beta> u False (append_heuristic_input M))

goal (1 subgoal):
 1. \<And>u T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
unfolding \<alpha> xy \<beta> qSource qTarget k ttc
[PROOF STATE]
proof (prove)
using this:
handleTrace = (\<lambda>(T, G) u. if is_in_language ?M ?qTarget u then let qu = FSM.after ?M ?qTarget u; ws = sorted_list_of_maximal_sequences_in_tree (?dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension ?M T G ?cg_lookup ?cg_insert ?\<alpha> (?xy # u @ w) False (append_heuristic_input ?M) in distribute_extension ?M T' G' ?cg_lookup ?cg_insert ?\<beta> (u @ w) False (append_heuristic_input ?M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension ?M T G ?cg_lookup ?cg_insert ?\<alpha> (?xy # u) False (append_heuristic_input ?M) in distribute_extension ?M T' G' ?cg_lookup ?cg_insert ?\<beta> u False (append_heuristic_input ?M)) \<Longrightarrow> Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))
handleTrace = (\<lambda>(T, G) u. if is_in_language M (after_initial M (V (t_target t))) u then let qu = FSM.after M (after_initial M (V (t_target t))) u; ws = sorted_list_of_maximal_sequences_in_tree (dist_fun (Suc (length u)) qu); appendDistTrace = \<lambda>(T, G) w. let (T', G') = distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u @ w) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) (u @ w) False (append_heuristic_input M) in foldl appendDistTrace (T, G) ws else let (T', G') = distribute_extension M T G cg_lookup cg_insert (V (t_source t)) ((t_input t, t_output t) # u) False (append_heuristic_input M) in distribute_extension M T' G' cg_lookup cg_insert (V (t_target t)) u False (append_heuristic_input M))

goal (1 subgoal):
 1. \<And>u T G. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (T, G) u))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. \<And>x xs. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) xs)) \<Longrightarrow> Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (ttc @ [io])))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
Prefix_Tree.set ?T \<subseteq> Prefix_Tree.set (fst (handleTrace (?T, ?G) ?u))

goal (1 subgoal):
 1. Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (handleTrace (foldl handleTrace (T, G) ttc) io))
[PROOF STEP]
by (metis (no_types, opaque_lifting) snoc.IH dual_order.trans fst_conv old.prod.exhaust)
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (foldl handleTrace (T, G) (ttc @ [io])))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Prefix_Tree.set T \<subseteq> Prefix_Tree.set (fst (establish_convergence_static dist_fun M V T G cg_insert cg_lookup m t))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_result1_saturating':
  assumes "eval r_result1 [t, i, x] \<down>= Suc v"
  shows "eval r_result1 [t + d, i, x] \<down>= Suc v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_result1 [t + d, i, x] \<down>= Suc v
[PROOF STEP]
using assms r_result1 r_result_saturating r_phi''
[PROOF STATE]
proof (prove)
using this:
eval r_result1 [t, i, x] \<down>= Suc v
eval r_result1 [?t, ?i, ?x] = eval r_result [?t, ?i, singleton_encode ?x]
eval r_result [?t, ?i, ?x] \<down>= Suc ?v \<Longrightarrow> eval r_result [?t + ?d, ?i, ?x] \<down>= Suc ?v
eval r_phi [?i, ?x] = eval r_univ [?i, singleton_encode ?x]

goal (1 subgoal):
 1. eval r_result1 [t + d, i, x] \<down>= Suc v
[PROOF STEP]
by simp


[STATEMENT]
lemma r_inconsist_recfn: "recfn 2 r_inconsist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 r_inconsist
[PROOF STEP]
unfolding r_inconsist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (let f = Cn 2 r_length [recf.Id 2 1]; g = Cn 4 r_ifless [recf.Id 4 1, Cn 4 r_length [recf.Id 4 3], recf.Id 4 1, Cn 4 r_ifeq [Cn 4 r_phi [recf.Id 4 2, recf.Id 4 0], Cn 4 r_nth [recf.Id 4 3, recf.Id 4 0], recf.Id 4 1, recf.Id 4 0]] in Cn 2 (Pr 2 f g) [Cn 2 r_length [recf.Id 2 1], recf.Id 2 0, recf.Id 2 1])
[PROOF STEP]
by simp


[STATEMENT]
lemma ind_in_set_mono:
  fixes a b :: nat and A :: "nat set"
  assumes "a \<in> A" "b \<in> A" "a < b"
  shows "ind_in_set A a < ind_in_set A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ind_in_set A a < ind_in_set A b
[PROOF STEP]
unfolding ind_in_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i \<in> A. i < a} < card {i \<in> A. i < b}
[PROOF STEP]
apply (rule psubset_card_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {i \<in> A. i < b}
 2. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i \<in> A. i < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
have "x \<in> {i \<in> A. i < b}" if "x \<in> {i \<in> A. i < a}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {i \<in> A. i < b}
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> A
a < b
x \<in> {i \<in> A. i < a}

goal (1 subgoal):
 1. x \<in> {i \<in> A. i < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> {i \<in> A. i < a} \<Longrightarrow> ?x \<in> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?x \<in> {i \<in> A. i < a} \<Longrightarrow> ?x \<in> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
have "a \<in> {i \<in> A. i < b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {i \<in> A. i < b}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> A
a < b

goal (1 subgoal):
 1. a \<in> {i \<in> A. i < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
have "b \<notin> {i \<in> A. i < b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<notin> {i \<in> A. i < b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<notin> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?x \<in> {i \<in> A. i < a} \<Longrightarrow> ?x \<in> {i \<in> A. i < b}
a \<in> {i \<in> A. i < b}
b \<notin> {i \<in> A. i < b}
[PROOF STEP]
show "{i \<in> A. i < a} \<subset> {i \<in> A. i < b}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> {i \<in> A. i < a} \<Longrightarrow> ?x \<in> {i \<in> A. i < b}
a \<in> {i \<in> A. i < b}
b \<notin> {i \<in> A. i < b}

goal (1 subgoal):
 1. {i \<in> A. i < a} \<subset> {i \<in> A. i < b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{i \<in> A. i < a} \<subset> {i \<in> A. i < b}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nths_assoc_three_A:
  fixes A B C :: "nat set"
  assumes "A \<inter> B = {}"
    and "(A \<union> B) \<inter> C = {}"
  shows "nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` A)
       = nths xs (ind_in_set (A \<union> B \<union> C) ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nths (nths xs (ind_in_set (A \<union> B \<union> C) ` (A \<union> B))) (ind_in_set (A \<union> B) ` A) = nths xs (ind_in_set (A \<union> B \<union> C) ` A)
[PROOF STEP]
apply (rule nths_reencode_eq3)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A \<subseteq> A \<union> B
 2. A \<union> B \<subseteq> A \<union> B \<union> C
[PROOF STEP]
by auto


[STATEMENT]
lemma small_Un:
  assumes X: "small X" and Y: "small Y"
  shows "small (X \<union> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small (X \<union> Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. small (X \<union> Y)
[PROOF STEP]
obtain x y where "elts x \<approx> X" "elts y \<approx> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>elts x \<approx> X; elts y \<approx> Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms small_eqpoll)
[PROOF STATE]
proof (state)
this:
elts x \<approx> X
elts y \<approx> Y

goal (1 subgoal):
 1. small (X \<union> Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
elts x \<approx> X
elts y \<approx> Y
[PROOF STEP]
have "X \<union> Y \<lesssim> Inl ` (elts x) \<union> Inr ` (elts y)"
[PROOF STATE]
proof (prove)
using this:
elts x \<approx> X
elts y \<approx> Y

goal (1 subgoal):
 1. X \<union> Y \<lesssim> ZFC_Cardinals.Inl ` elts x \<union> ZFC_Cardinals.Inr ` elts y
[PROOF STEP]
by (metis (mono_tags, lifting) Inr_Inl_iff Un_lepoll_mono disjnt_iff eqpoll_imp_lepoll eqpoll_sym f_inv_into_f inj_on_Inl inj_on_Inr inj_on_image_lepoll_2)
[PROOF STATE]
proof (state)
this:
X \<union> Y \<lesssim> ZFC_Cardinals.Inl ` elts x \<union> ZFC_Cardinals.Inr ` elts y

goal (1 subgoal):
 1. small (X \<union> Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<union> Y \<lesssim> ZFC_Cardinals.Inl ` elts x \<union> ZFC_Cardinals.Inr ` elts y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<union> Y \<lesssim> ZFC_Cardinals.Inl ` elts x \<union> ZFC_Cardinals.Inr ` elts y

goal (1 subgoal):
 1. small (X \<union> Y)
[PROOF STEP]
by (metis lepoll_iff replacement small_elts small_sup_iff smaller_than_small)
[PROOF STATE]
proof (state)
this:
small (X \<union> Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app_subst_id_type_scheme [simp]:
  "$ id_subst = (\<lambda>sch::type_scheme. sch)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $ id_subst = (\<lambda>sch. sch)
[PROOF STEP]
using id_subst_def subst_TVar_scheme
[PROOF STATE]
proof (prove)
using this:
id_subst = TVar
$ TVar ?sch = ?sch

goal (1 subgoal):
 1. $ id_subst = (\<lambda>sch. sch)
[PROOF STEP]
by auto

\<comment> \<open>application of @{text id_subst} does not change list of type expressions\<close>


[STATEMENT]
lemma fmember_implies_member: "e |\<in>| f \<Longrightarrow> e \<in> fset f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e |\<in>| f \<Longrightarrow> e \<in> fset f
[PROOF STEP]
by (simp add: fmember_def)


[STATEMENT]
lemma Mapping_size_transfer [transfer_rule]:
  includes lifting_syntax
  shows "(pcr_mapping (=) (=) ===> (=)) (card \<circ> dom) Mapping.size"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pcr_mapping (=) (=) ===> (=)) (card \<circ> dom) Mapping.size
[PROOF STEP]
apply(rule rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. pcr_mapping (=) (=) x y \<Longrightarrow> (card \<circ> dom) x = Mapping.size y
[PROOF STEP]
apply(case_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>pcr_mapping (=) (=) x y; y = Mapping ya; ya \<in> UNIV\<rbrakk> \<Longrightarrow> (card \<circ> dom) x = Mapping.size y
[PROOF STEP]
apply(simp add: Mapping.size_def Mapping.keys.rep_eq Mapping_inverse mapping.pcr_cr_eq cr_mapping_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma it_dfs_correct: "it_dfs \<le> SPEC (\<lambda>s. DFS_invar G param s \<and> \<not>cond s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_dfs \<le> SPEC (\<lambda>s. DFS_invar G param s \<and> \<not> cond s)
[PROOF STEP]
by (simp add: it_dfs_eq_spec)


[STATEMENT]
lemma infinite_rangeIt:
  assumes inj: "inj f"
  and x: "\<forall>y. x \<noteq> f y"
  shows "\<not> finite (rangeIt x f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (rangeIt x f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (rangeIt x f)
[PROOF STEP]
have "inj (\<lambda>n. (f ^^ n) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>n. (f ^^ n) x)
[PROOF STEP]
proof(rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. (f ^^ xa) x = (f ^^ y) x \<Longrightarrow> xa = y
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa y. (f ^^ xa) x = (f ^^ y) x \<Longrightarrow> xa = y
[PROOF STEP]
assume "(f ^^ n) x = (f ^^ m) x"
[PROOF STATE]
proof (state)
this:
(f ^^ n) x = (f ^^ m) x

goal (1 subgoal):
 1. \<And>xa y. (f ^^ xa) x = (f ^^ y) x \<Longrightarrow> xa = y
[PROOF STEP]
thus "n = m"
[PROOF STATE]
proof (prove)
using this:
(f ^^ n) x = (f ^^ m) x

goal (1 subgoal):
 1. n = m
[PROOF STEP]
proof(induct n arbitrary: m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. (f ^^ 0) x = (f ^^ m) x \<Longrightarrow> 0 = m
 2. \<And>n m. \<lbrakk>\<And>m. (f ^^ n) x = (f ^^ m) x \<Longrightarrow> n = m; (f ^^ Suc n) x = (f ^^ m) x\<rbrakk> \<Longrightarrow> Suc n = m
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(f ^^ 0) x = (f ^^ m) x

goal (2 subgoals):
 1. \<And>m. (f ^^ 0) x = (f ^^ m) x \<Longrightarrow> 0 = m
 2. \<And>n m. \<lbrakk>\<And>m. (f ^^ n) x = (f ^^ m) x \<Longrightarrow> n = m; (f ^^ Suc n) x = (f ^^ m) x\<rbrakk> \<Longrightarrow> Suc n = m
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(f ^^ 0) x = (f ^^ m) x

goal (1 subgoal):
 1. 0 = m
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(f ^^ 0) x = (f ^^ m) x
\<forall>y. x \<noteq> f y

goal (1 subgoal):
 1. 0 = m
[PROOF STEP]
by(cases m)(auto intro: sym)
[PROOF STATE]
proof (state)
this:
0 = m

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. (f ^^ n) x = (f ^^ m) x \<Longrightarrow> n = m; (f ^^ Suc n) x = (f ^^ m) x\<rbrakk> \<Longrightarrow> Suc n = m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. (f ^^ n) x = (f ^^ m) x \<Longrightarrow> n = m; (f ^^ Suc n) x = (f ^^ m) x\<rbrakk> \<Longrightarrow> Suc n = m
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(f ^^ n) x = (f ^^ ?m) x \<Longrightarrow> n = ?m
(f ^^ Suc n) x = (f ^^ m) x

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>\<And>m. (f ^^ n) x = (f ^^ m) x \<Longrightarrow> n = m; (f ^^ Suc n) x = (f ^^ m) x\<rbrakk> \<Longrightarrow> Suc n = m
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(f ^^ n) x = (f ^^ ?m) x \<Longrightarrow> n = ?m
(f ^^ Suc n) x = (f ^^ m) x

goal (1 subgoal):
 1. Suc n = m
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(f ^^ n) x = (f ^^ ?m) x \<Longrightarrow> n = ?m
(f ^^ Suc n) x = (f ^^ m) x
\<forall>y. x \<noteq> f y

goal (1 subgoal):
 1. Suc n = m
[PROOF STEP]
by(cases m)(auto intro: sym dest: injD[OF inj])
[PROOF STATE]
proof (state)
this:
Suc n = m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj (\<lambda>n. (f ^^ n) x)

goal (1 subgoal):
 1. infinite (rangeIt x f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inj (\<lambda>n. (f ^^ n) x)

goal (1 subgoal):
 1. infinite (rangeIt x f)
[PROOF STEP]
by(auto simp add: rangeIt_def dest: finite_imageD)
[PROOF STATE]
proof (state)
this:
infinite (rangeIt x f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma standard_rules_mono:
  assumes "C\<^sub>1 \<subseteq> C\<^sub>2" "L\<^sub>1 \<subseteq> L\<^sub>2"
  shows "standard_rules C\<^sub>1 L\<^sub>1 \<subseteq> standard_rules C\<^sub>2 L\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. standard_rules C\<^sub>1 L\<^sub>1 \<subseteq> standard_rules C\<^sub>2 L\<^sub>2
[PROOF STEP]
using constant_rules_mono[OF assms(1)] identity_rules_mono[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
constant_rules C\<^sub>1 \<subseteq> constant_rules C\<^sub>2
identity_rules L\<^sub>1 \<subseteq> identity_rules L\<^sub>2

goal (1 subgoal):
 1. standard_rules C\<^sub>1 L\<^sub>1 \<subseteq> standard_rules C\<^sub>2 L\<^sub>2
[PROOF STEP]
unfolding standard_rules_def
[PROOF STATE]
proof (prove)
using this:
constant_rules C\<^sub>1 \<subseteq> constant_rules C\<^sub>2
identity_rules L\<^sub>1 \<subseteq> identity_rules L\<^sub>2

goal (1 subgoal):
 1. constant_rules C\<^sub>1 \<union> identity_rules L\<^sub>1 \<union> {top_rule S_Top, nonempty_rule} \<subseteq> constant_rules C\<^sub>2 \<union> identity_rules L\<^sub>2 \<union> {top_rule S_Top, nonempty_rule}
[PROOF STEP]
by auto