[STATEMENT]
lemma Abs_lst_fcb2:
  fixes as bs :: "atom list"
    and x y :: "'b :: fs"
    and c::"'c::fs"
  assumes eq: "[as]lst. x = [bs]lst. y"
  and fcb1: "(set as) \<sharp>* f as x c"
  and fresh1: "set as \<sharp>* c"
  and fresh2: "set bs \<sharp>* c"
  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
  shows "f as x c = f bs y c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "supp (as, x, c) supports (f as x c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (as, x, c) supports f as x c
[PROOF STEP]
unfolding  supports_def fresh_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. a \<sharp> (as, x, c) \<and> b \<sharp> (as, x, c) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> f as x c = f as x c
[PROOF STEP]
by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)
[PROOF STATE]
proof (state)
this:
supp (as, x, c) supports f as x c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (as, x, c) supports f as x c
[PROOF STEP]
have fin1: "finite (supp (f as x c))"
[PROOF STATE]
proof (prove)
using this:
supp (as, x, c) supports f as x c

goal (1 subgoal):
 1. finite (supp (f as x c))
[PROOF STEP]
by (auto intro: supports_finite simp add: finite_supp)
[PROOF STATE]
proof (state)
this:
finite (supp (f as x c))

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "supp (bs, y, c) supports (f bs y c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (bs, y, c) supports f bs y c
[PROOF STEP]
unfolding  supports_def fresh_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. a \<sharp> (bs, y, c) \<and> b \<sharp> (bs, y, c) \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> f bs y c = f bs y c
[PROOF STEP]
by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)
[PROOF STATE]
proof (state)
this:
supp (bs, y, c) supports f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
supp (bs, y, c) supports f bs y c
[PROOF STEP]
have fin2: "finite (supp (f bs y c))"
[PROOF STATE]
proof (prove)
using this:
supp (bs, y, c) supports f bs y c

goal (1 subgoal):
 1. finite (supp (f bs y c))
[PROOF STEP]
by (auto intro: supports_finite simp add: finite_supp)
[PROOF STATE]
proof (state)
this:
finite (supp (f bs y c))

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
obtain q::"perm" where
    fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and
    fr2: "supp q \<sharp>* Abs_lst as x" and
    inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c); supp q \<sharp>* ([as]lst. x); supp q \<subseteq> set as \<union> q \<bullet> set as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"]
      fin1 fin2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (set as); finite (supp (x, c, f as x c, f bs y c)); finite (supp ([as]lst. x)); set as \<sharp>* ([as]lst. x)\<rbrakk> \<Longrightarrow> \<exists>p. (p \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c) \<and> supp ([as]lst. x) \<sharp>* p \<and> supp p = set as \<union> p \<bullet> set as
finite (supp (f as x c))
finite (supp (f bs y c))

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c); supp q \<sharp>* ([as]lst. x); supp q \<subseteq> set as \<union> q \<bullet> set as\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
[PROOF STATE]
proof (state)
this:
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)
supp q \<sharp>* ([as]lst. x)
supp q \<subseteq> set as \<union> q \<bullet> set as

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q \<bullet> as]lst. q \<bullet> x = q \<bullet> ([as]lst. x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q \<bullet> as]lst. q \<bullet> x = q \<bullet> ([as]lst. x)

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[q \<bullet> as]lst. q \<bullet> x = q \<bullet> ([as]lst. x)

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "\<dots> = Abs_lst as x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<bullet> ([as]lst. x) = [as]lst. x
[PROOF STEP]
by (simp only: fr2 perm_supp_eq)
[PROOF STATE]
proof (state)
this:
q \<bullet> ([as]lst. x) = [as]lst. x

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[q \<bullet> as]lst. q \<bullet> x = [as]lst. x
[PROOF STEP]
have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y"
[PROOF STATE]
proof (prove)
using this:
[q \<bullet> as]lst. q \<bullet> x = [as]lst. x

goal (1 subgoal):
 1. [q \<bullet> as]lst. q \<bullet> x = [bs]lst. y
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
[q \<bullet> as]lst. q \<bullet> x = [as]lst. x
[as]lst. x = [bs]lst. y

goal (1 subgoal):
 1. [q \<bullet> as]lst. q \<bullet> x = [bs]lst. y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q \<bullet> as]lst. q \<bullet> x = [bs]lst. y

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q \<bullet> as]lst. q \<bullet> x = [bs]lst. y
[PROOF STEP]
obtain r::perm where
    qq1: "q \<bullet> x = r \<bullet> y" and
    qq2: "q \<bullet> as = r \<bullet> bs" and
    qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs"
[PROOF STATE]
proof (prove)
using this:
[q \<bullet> as]lst. q \<bullet> x = [bs]lst. y

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>q \<bullet> x = r \<bullet> y; q \<bullet> as = r \<bullet> bs; supp r \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(drule_tac sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrakk>q \<bullet> x = r \<bullet> y; q \<bullet> as = r \<bullet> bs; supp r \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis; [bs]lst. y = [q \<bullet> as]lst. q \<bullet> x\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(simp only: Abs_eq_iff2 alphas)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrakk>q \<bullet> x = r \<bullet> y; q \<bullet> as = r \<bullet> bs; supp r \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis; \<exists>p. (supp y - set bs = supp (q \<bullet> x) - set (q \<bullet> as) \<and> (supp y - set bs) \<sharp>* p \<and> p \<bullet> y = q \<bullet> x \<and> p \<bullet> bs = q \<bullet> as) \<and> supp p \<subseteq> set bs \<union> set (q \<bullet> as)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>r. \<lbrakk>q \<bullet> x = r \<bullet> y; q \<bullet> as = r \<bullet> bs; supp r \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis; (supp y - set bs = supp (q \<bullet> x) - set (q \<bullet> as) \<and> (supp y - set bs) \<sharp>* p \<and> p \<bullet> y = q \<bullet> x \<and> p \<bullet> bs = q \<bullet> as) \<and> supp p \<subseteq> set bs \<union> set (q \<bullet> as)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>r. \<lbrakk>q \<bullet> x = r \<bullet> y; q \<bullet> as = r \<bullet> bs; supp r \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis; supp p \<subseteq> set bs \<union> set (q \<bullet> as); supp y - set bs = supp (q \<bullet> x) - set (q \<bullet> as); (supp y - set bs) \<sharp>* p; p \<bullet> y = q \<bullet> x; p \<bullet> bs = q \<bullet> as\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(drule_tac x="p" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>supp p \<subseteq> set bs \<union> set (q \<bullet> as); supp y - set bs = supp (q \<bullet> x) - set (q \<bullet> as); (supp y - set bs) \<sharp>* p; p \<bullet> y = q \<bullet> x; p \<bullet> bs = q \<bullet> as; \<lbrakk>q \<bullet> x = p \<bullet> y; q \<bullet> as = p \<bullet> bs; supp p \<subseteq> q \<bullet> set as \<union> set bs\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(simp add: set_eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>supp p \<subseteq> set bs \<union> set (q \<bullet> as); supp y - set bs = supp (q \<bullet> x) - set (q \<bullet> as); (supp (q \<bullet> x) - set (q \<bullet> as)) \<sharp>* p; p \<bullet> y = q \<bullet> x; p \<bullet> bs = q \<bullet> as; supp p \<subseteq> set (q \<bullet> as) \<union> set bs \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
q \<bullet> x = r \<bullet> y
q \<bullet> as = r \<bullet> bs
supp r \<subseteq> q \<bullet> set as \<union> set bs

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "(set as) \<sharp>* f as x c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set as \<sharp>* f as x c
[PROOF STEP]
by (rule fcb1)
[PROOF STATE]
proof (state)
this:
set as \<sharp>* f as x c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set as \<sharp>* f as x c
[PROOF STEP]
have "q \<bullet> ((set as) \<sharp>* f as x c)"
[PROOF STATE]
proof (prove)
using this:
set as \<sharp>* f as x c

goal (1 subgoal):
 1. q \<bullet> set as \<sharp>* f as x c
[PROOF STEP]
by (simp add: permute_bool_def)
[PROOF STATE]
proof (state)
this:
q \<bullet> set as \<sharp>* f as x c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q \<bullet> set as \<sharp>* f as x c
[PROOF STEP]
have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
[PROOF STATE]
proof (prove)
using this:
q \<bullet> set as \<sharp>* f as x c

goal (1 subgoal):
 1. set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
apply(simp only: fresh_star_eqvt set_eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (q \<bullet> as) \<sharp>* (q \<bullet> f as x c) \<Longrightarrow> set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
apply(subst (asm) perm1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. supp q \<sharp>* c
 2. set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c \<Longrightarrow> set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
using inc fresh1 fr1
[PROOF STATE]
proof (prove)
using this:
supp q \<subseteq> set as \<union> q \<bullet> set as
set as \<sharp>* c
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)

goal (2 subgoals):
 1. supp q \<sharp>* c
 2. set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c \<Longrightarrow> set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
apply(auto simp add: fresh_star_def fresh_Pair)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c"
[PROOF STATE]
proof (prove)
using this:
set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c

goal (1 subgoal):
 1. set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c
[PROOF STEP]
using qq1 qq2
[PROOF STATE]
proof (prove)
using this:
set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c
q \<bullet> x = r \<bullet> y
q \<bullet> as = r \<bullet> bs

goal (1 subgoal):
 1. set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c
[PROOF STEP]
have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
[PROOF STATE]
proof (prove)
using this:
set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c

goal (1 subgoal):
 1. r \<bullet> set bs \<sharp>* f bs y c
[PROOF STEP]
apply(simp only: fresh_star_eqvt set_eqvt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c \<Longrightarrow> set (r \<bullet> bs) \<sharp>* (r \<bullet> f bs y c)
[PROOF STEP]
apply(subst (asm) perm2[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. supp r \<sharp>* c
 2. set (r \<bullet> bs) \<sharp>* (r \<bullet> f bs y c) \<Longrightarrow> set (r \<bullet> bs) \<sharp>* (r \<bullet> f bs y c)
[PROOF STEP]
using qq3 fresh2 fr1
[PROOF STATE]
proof (prove)
using this:
supp r \<subseteq> q \<bullet> set as \<union> set bs
set bs \<sharp>* c
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)

goal (2 subgoals):
 1. supp r \<sharp>* c
 2. set (r \<bullet> bs) \<sharp>* (r \<bullet> f bs y c) \<Longrightarrow> set (r \<bullet> bs) \<sharp>* (r \<bullet> f bs y c)
[PROOF STEP]
apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
r \<bullet> set bs \<sharp>* f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<bullet> set bs \<sharp>* f bs y c
[PROOF STEP]
have fcb2: "(set bs) \<sharp>* f bs y c"
[PROOF STATE]
proof (prove)
using this:
r \<bullet> set bs \<sharp>* f bs y c

goal (1 subgoal):
 1. set bs \<sharp>* f bs y c
[PROOF STEP]
by (simp add: permute_bool_def)
[PROOF STATE]
proof (state)
this:
set bs \<sharp>* f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "f as x c = q \<bullet> (f as x c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f as x c = q \<bullet> f as x c
[PROOF STEP]
apply(rule perm_supp_eq[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp q \<sharp>* f as x c
[PROOF STEP]
using inc fcb1 fr1
[PROOF STATE]
proof (prove)
using this:
supp q \<subseteq> set as \<union> q \<bullet> set as
set as \<sharp>* f as x c
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)

goal (1 subgoal):
 1. supp q \<sharp>* f as x c
[PROOF STEP]
by (auto simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
f as x c = q \<bullet> f as x c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f as x c = q \<bullet> f as x c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<bullet> f as x c = f (q \<bullet> as) (q \<bullet> x) c
[PROOF STEP]
apply(rule perm1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp q \<sharp>* c
[PROOF STEP]
using inc fresh1 fr1
[PROOF STATE]
proof (prove)
using this:
supp q \<subseteq> set as \<union> q \<bullet> set as
set as \<sharp>* c
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)

goal (1 subgoal):
 1. supp q \<sharp>* c
[PROOF STEP]
by (auto simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
q \<bullet> f as x c = f (q \<bullet> as) (q \<bullet> x) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
q \<bullet> f as x c = f (q \<bullet> as) (q \<bullet> x) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (q \<bullet> as) (q \<bullet> x) c = f (r \<bullet> bs) (r \<bullet> y) c
[PROOF STEP]
using qq1 qq2
[PROOF STATE]
proof (prove)
using this:
q \<bullet> x = r \<bullet> y
q \<bullet> as = r \<bullet> bs

goal (1 subgoal):
 1. f (q \<bullet> as) (q \<bullet> x) c = f (r \<bullet> bs) (r \<bullet> y) c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (q \<bullet> as) (q \<bullet> x) c = f (r \<bullet> bs) (r \<bullet> y) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (q \<bullet> as) (q \<bullet> x) c = f (r \<bullet> bs) (r \<bullet> y) c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "\<dots> = r \<bullet> (f bs y c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (r \<bullet> bs) (r \<bullet> y) c = r \<bullet> f bs y c
[PROOF STEP]
apply(rule perm2[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp r \<sharp>* c
[PROOF STEP]
using qq3 fresh2 fr1
[PROOF STATE]
proof (prove)
using this:
supp r \<subseteq> q \<bullet> set as \<union> set bs
set bs \<sharp>* c
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)

goal (1 subgoal):
 1. supp r \<sharp>* c
[PROOF STEP]
by (auto simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
f (r \<bullet> bs) (r \<bullet> y) c = r \<bullet> f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (r \<bullet> bs) (r \<bullet> y) c = r \<bullet> f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
have "... = f bs y c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<bullet> f bs y c = f bs y c
[PROOF STEP]
apply(rule perm_supp_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp r \<sharp>* f bs y c
[PROOF STEP]
using qq3 fr1 fcb2
[PROOF STATE]
proof (prove)
using this:
supp r \<subseteq> q \<bullet> set as \<union> set bs
(q \<bullet> set as) \<sharp>* (x, c, f as x c, f bs y c)
set bs \<sharp>* f bs y c

goal (1 subgoal):
 1. supp r \<sharp>* f bs y c
[PROOF STEP]
by (auto simp add: fresh_star_def)
[PROOF STATE]
proof (state)
this:
r \<bullet> f bs y c = f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f as x c = f bs y c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f as x c = f bs y c

goal (1 subgoal):
 1. f as x c = f bs y c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f as x c = f bs y c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Abs_lst1_fcb2:
  fixes a b :: "atom"
    and x y :: "'b :: fs"
    and c::"'c :: fs"
  assumes e: "[[a]]lst. x = [[b]]lst. y"
  and fcb1: "a \<sharp> f a x c"
  and fresh: "{a, b} \<sharp>* c"
  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c"
  shows "f a x c = f b y c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a x c = f b y c
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
[[a]]lst. x = [[b]]lst. y

goal (1 subgoal):
 1. f a x c = f b y c
[PROOF STEP]
apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. set [a] \<sharp>* f (hd [a]) x c
 2. set [a] \<sharp>* c
 3. set [b] \<sharp>* c
 4. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (hd [a]) x c = f (hd (p \<bullet> [a])) (p \<bullet> x) c
 5. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (hd [b]) y c = f (hd (p \<bullet> [b])) (p \<bullet> y) c
 6. f (hd [a]) x c = f (hd [b]) y c \<Longrightarrow> f a x c = f b y c
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. {a} \<sharp>* f a x c
 2. {a} \<sharp>* c
 3. {b} \<sharp>* c
 4. \<And>p. supp p \<sharp>* c \<Longrightarrow> (p \<bullet> f) (p \<bullet> a) (p \<bullet> x) (p \<bullet> c) = f (p \<bullet> a) (p \<bullet> x) c
 5. \<And>p. supp p \<sharp>* c \<Longrightarrow> (p \<bullet> f) (p \<bullet> b) (p \<bullet> y) (p \<bullet> c) = f (p \<bullet> b) (p \<bullet> y) c
[PROOF STEP]
using fcb1 fresh perm1 perm2
[PROOF STATE]
proof (prove)
using this:
a \<sharp> f a x c
{a, b} \<sharp>* c
supp ?p \<sharp>* c \<Longrightarrow> ?p \<bullet> f a x c = f (?p \<bullet> a) (?p \<bullet> x) c
supp ?p \<sharp>* c \<Longrightarrow> ?p \<bullet> f b y c = f (?p \<bullet> b) (?p \<bullet> y) c

goal (5 subgoals):
 1. {a} \<sharp>* f a x c
 2. {a} \<sharp>* c
 3. {b} \<sharp>* c
 4. \<And>p. supp p \<sharp>* c \<Longrightarrow> (p \<bullet> f) (p \<bullet> a) (p \<bullet> x) (p \<bullet> c) = f (p \<bullet> a) (p \<bullet> x) c
 5. \<And>p. supp p \<sharp>* c \<Longrightarrow> (p \<bullet> f) (p \<bullet> b) (p \<bullet> y) (p \<bullet> c) = f (p \<bullet> b) (p \<bullet> y) c
[PROOF STEP]
apply(simp_all add: fresh_star_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Abs_lst1_fcb2':
  fixes a b :: "'a::at_base"
    and x y :: "'b :: fs"
    and c::"'c :: fs"
  assumes e: "[[atom a]]lst. x = [[atom b]]lst. y"
  and fcb1: "atom a \<sharp> f a x c"
  and fresh: "{atom a, atom b} \<sharp>* c"
  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c"
  shows "f a x c = f b y c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a x c = f b y c
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
[[atom a]]lst. x = [[atom b]]lst. y

goal (1 subgoal):
 1. f a x c = f b y c
[PROOF STEP]
apply(drule_tac Abs_lst1_fcb2[where c="c" and f="\<lambda>a . f ((inv atom) a)"])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. atom a \<sharp> f (inv atom (atom a)) x c
 2. {atom a, atom b} \<sharp>* c
 3. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (inv atom (atom a)) x c = f (inv atom (p \<bullet> atom a)) (p \<bullet> x) c
 4. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (inv atom (atom b)) y c = f (inv atom (p \<bullet> atom b)) (p \<bullet> y) c
 5. f (inv atom (atom a)) x c = f (inv atom (atom b)) y c \<Longrightarrow> f a x c = f b y c
[PROOF STEP]
using  fcb1 fresh perm1 perm2
[PROOF STATE]
proof (prove)
using this:
atom a \<sharp> f a x c
{atom a, atom b} \<sharp>* c
supp ?p \<sharp>* c \<Longrightarrow> ?p \<bullet> f a x c = f (?p \<bullet> a) (?p \<bullet> x) c
supp ?p \<sharp>* c \<Longrightarrow> ?p \<bullet> f b y c = f (?p \<bullet> b) (?p \<bullet> y) c

goal (5 subgoals):
 1. atom a \<sharp> f (inv atom (atom a)) x c
 2. {atom a, atom b} \<sharp>* c
 3. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (inv atom (atom a)) x c = f (inv atom (p \<bullet> atom a)) (p \<bullet> x) c
 4. \<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> f (inv atom (atom b)) y c = f (inv atom (p \<bullet> atom b)) (p \<bullet> y) c
 5. f (inv atom (atom a)) x c = f (inv atom (atom b)) y c \<Longrightarrow> f a x c = f b y c
[PROOF STEP]
apply(simp_all add: fresh_star_def inv_f_f inj_on_def atom_eqvt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_zero_row_upt_ncols:
  fixes A::"'a::{zero}^'columns::{mod_type}^'rows"
  shows "is_zero_row_upt_k i (ncols A) A = (\<forall>j::'columns. A $ i $ j = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i (ncols A) A = (\<forall>j. A $ i $ j = (0::'a))
[PROOF STEP]
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j. mod_type_class.to_nat j < CARD('columns) \<longrightarrow> A $ i $ j = (0::'a)) = (\<forall>j. A $ i $ j = (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma is_zero_row_eq_row_zero: "is_zero_row a A = (row a A = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row a A = (row a A = 0)
[PROOF STEP]
unfolding is_zero_row_def' row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j. A $ a $ j = (0::'b)) = (vec_lambda (($) (A $ a)) = 0)
[PROOF STEP]
unfolding vec_nth_inverse
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j. A $ a $ j = (0::'b)) = (A $ a = 0)
[PROOF STEP]
unfolding vec_eq_iff zero_index
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>j. A $ a $ j = (0::'b)) = (\<forall>i. A $ a $ i = (0::'b))
[PROOF STEP]
..


[STATEMENT]
lemma not_is_zero_row_upt_suc:
  assumes "\<not> is_zero_row_upt_k i (Suc k) A"
  and "\<forall>i. A $ i $ (from_nat k) = 0"
  shows "\<not> is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using assms from_nat_to_nat_id
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i (Suc k) A
\<forall>i. A $ i $ mod_type_class.from_nat k = (0::'b)
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
using is_zero_row_upt_k_def less_SucE
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k i (Suc k) A
\<forall>i. A $ i $ mod_type_class.from_nat k = (0::'b)
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x
is_zero_row_upt_k ?i ?k ?A = (\<forall>j. mod_type_class.to_nat j < ?k \<longrightarrow> ?A $ ?i $ j = (0::?'a))
\<lbrakk>?m < Suc ?n; ?m < ?n \<Longrightarrow> ?P; ?m = ?n \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i k A
[PROOF STEP]
by metis


[STATEMENT]
lemma is_zero_row_upt_k_suc:
  assumes "is_zero_row_upt_k i k A"
  and "A $ i $ (from_nat k) = 0"
  shows "is_zero_row_upt_k i (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A
A $ i $ mod_type_class.from_nat k = (0::'b)

goal (1 subgoal):
 1. is_zero_row_upt_k i (Suc k) 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> A $ i $ j = (0::'b)
A $ i $ mod_type_class.from_nat k = (0::'b)

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'b)
[PROOF STEP]
using less_SucE to_nat_from_nat
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)
A $ i $ mod_type_class.from_nat k = (0::'b)
\<lbrakk>?m < Suc ?n; ?m < ?n \<Longrightarrow> ?P; ?m = ?n \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
mod_type_class.to_nat ?j = ?k \<Longrightarrow> mod_type_class.from_nat ?k = ?j

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'b)
[PROOF STEP]
by metis


[STATEMENT]
lemma is_zero_row_utp_0:
  shows "is_zero_row_upt_k m 0 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k m 0 A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ m $ j = (0::'b)
[PROOF STEP]
by fast


[STATEMENT]
lemma is_zero_row_utp_0':
  shows "\<forall>m. is_zero_row_upt_k m 0 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m. is_zero_row_upt_k m 0 A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ m $ j = (0::'b)
[PROOF STEP]
by fast


[STATEMENT]
lemma is_zero_row_upt_k_le:
  assumes "is_zero_row_upt_k i (Suc k) A"
  shows "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i (Suc k) A

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

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_zero_row_imp_is_zero_row_upt:
assumes "is_zero_row i A"
shows "is_zero_row_upt_k i k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k i k A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_zero_row i A

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

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_upt_0: "reduced_row_echelon_form_upt_k A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A 0
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. (\<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ i $ j = (0::'a)) \<longrightarrow> \<not> (\<exists>j>i. \<not> (\<forall>ja. mod_type_class.to_nat ja < 0 \<longrightarrow> A $ j $ ja = (0::'a)))) \<and> (\<forall>i. \<not> (\<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ i $ j = (0::'a)) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ i $ j = (0::'a)) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ (i + (1::'c)) $ j = (0::'a)) \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> (\<forall>j. mod_type_class.to_nat j < 0 \<longrightarrow> A $ i $ j = (0::'a)) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))
[PROOF STEP]
by auto


[STATEMENT]
lemma rref_upt_condition1:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j. j>i \<and> \<not> is_zero_row_upt_k j k A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_upt_condition2:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(\<forall>i. \<not> (is_zero_row_upt_k i k A) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_upt_condition3:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows "(\<forall>i. i<i+1 \<and> \<not> (is_zero_row_upt_k i k A) \<and> \<not> (is_zero_row_upt_k (i+1) k A) \<longrightarrow> ((LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i+1) $ n \<noteq> 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_upt_condition4:
  assumes r: "reduced_row_echelon_form_upt_k A k"
  shows " (\<forall>i. \<not> (is_zero_row_upt_k i k A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_upt_condition1_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "is_zero_row_upt_k i k A"
and "j>i"
shows "is_zero_row_upt_k j k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k j k A
[PROOF STEP]
using assms rref_upt_condition1
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k
is_zero_row_upt_k i k A
i < j
reduced_row_echelon_form_upt_k ?A ?k \<Longrightarrow> \<forall>i. is_zero_row_upt_k i ?k ?A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j ?k ?A)

goal (1 subgoal):
 1. is_zero_row_upt_k j k A
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_upt_condition2_explicit:
assumes rref_A: "reduced_row_echelon_form_upt_k A k"
and "\<not> is_zero_row_upt_k i k A"
shows "A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2 assms
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k ?A ?k \<Longrightarrow> \<forall>i. \<not> is_zero_row_upt_k i ?k ?A \<longrightarrow> ?A $ i $ (LEAST k. ?A $ i $ k \<noteq> (0::?'a)) = (1::?'a)
reduced_row_echelon_form_upt_k A k
\<not> is_zero_row_upt_k i k A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_upt_condition3_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "i < i + 1"
and "\<not> is_zero_row_upt_k i k A"
and "\<not> is_zero_row_upt_k (i + 1) k A "
shows "(LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
using assms rref_upt_condition3
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k
i < i + (1::'c)
\<not> is_zero_row_upt_k i k A
\<not> is_zero_row_upt_k (i + (1::'c)) k A
reduced_row_echelon_form_upt_k ?A ?k \<Longrightarrow> \<forall>i. i < i + (1::?'c) \<and> \<not> is_zero_row_upt_k i ?k ?A \<and> \<not> is_zero_row_upt_k (i + (1::?'c)) ?k ?A \<longrightarrow> (LEAST n. ?A $ i $ n \<noteq> (0::?'a)) < (LEAST n. ?A $ (i + (1::?'c)) $ n \<noteq> (0::?'a))

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_upt_condition4_explicit:
assumes "reduced_row_echelon_form_upt_k A k"
and "\<not> is_zero_row_upt_k i k A"
and "i \<noteq> j"
shows "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using assms rref_upt_condition4
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k A k
\<not> is_zero_row_upt_k i k A
i \<noteq> j
reduced_row_echelon_form_upt_k ?A ?k \<Longrightarrow> \<forall>i. \<not> is_zero_row_upt_k i ?k ?A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> ?A $ j $ (LEAST n. ?A $ i $ n \<noteq> (0::?'a)) = (0::?'a))

goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma reduced_row_echelon_form_upt_k_intro:
  assumes "(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j. j>i \<and> \<not> is_zero_row_upt_k j k A))"
  and "(\<forall>i. \<not> (is_zero_row_upt_k i k A) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1)"
  and "(\<forall>i. i<i+1 \<and> \<not> (is_zero_row_upt_k i k A) \<and> \<not> (is_zero_row_upt_k (i+1) k A) \<longrightarrow> ((LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i+1) $ n \<noteq> 0)))"
  and "(\<forall>i. \<not> (is_zero_row_upt_k i k A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0))"
  shows "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
unfolding reduced_row_echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'b)) = (1::'b)) \<and> (\<forall>i. i < i + (1::'a) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'a)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'b)) < (LEAST n. A $ (i + (1::'a)) $ n \<noteq> (0::'b))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (0::'b)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'b)) = (1::'b)
\<forall>i. i < i + (1::'a) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'a)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'b)) < (LEAST n. A $ (i + (1::'a)) $ n \<noteq> (0::'b))
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (0::'b))

goal (1 subgoal):
 1. (\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'b)) = (1::'b)) \<and> (\<forall>i. i < i + (1::'a) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'a)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'b)) < (LEAST n. A $ (i + (1::'a)) $ n \<noteq> (0::'b))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (0::'b)))
[PROOF STEP]
by fast


[STATEMENT]
lemma rref_suc_imp_rref:
  fixes A::"'a::{semiring_1}^'n::{mod_type}^'m::{mod_type}"
  assumes r: "reduced_row_echelon_form_upt_k A (Suc k)"
  and k_le_card: "Suc k < ncols A"
  shows "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
proof (rule reduced_row_echelon_form_upt_k_intro)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 4. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_upt_condition2[OF r] less_SucI
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
?m < ?n \<Longrightarrow> ?m < Suc ?n

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

goal (1 subgoal):
 1. \<forall>i. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<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 (3 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
 3. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. i < i + 1 \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + 1) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
[PROOF STEP]
using rref_upt_condition3[OF r] less_SucI
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
?m < ?n \<Longrightarrow> ?m < Suc ?n

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

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'m) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ (i + (1::'m)) $ j = (0::'a)) \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
using rref_upt_condition4[OF r] less_SucI
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row_upt_k i (Suc k) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
?m < ?n \<Longrightarrow> ?m < Suc ?n

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

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

goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
show "\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
proof (clarify, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume zero_i: "is_zero_row_upt_k i k A"
      and i_less_j: "i < j"
      and not_zero_j: "\<not> is_zero_row_upt_k j k A"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A
i < j
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have not_zero_j_suc: "\<not> is_zero_row_upt_k j (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k j (Suc k) A
[PROOF STEP]
using not_zero_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k j k A

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

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence not_zero_i_suc: "\<not> is_zero_row_upt_k i (Suc k) A"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k j (Suc k) A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i (Suc k) A
[PROOF STEP]
using rref_upt_condition1[OF r] i_less_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k j (Suc k) A
\<forall>i. is_zero_row_upt_k i (Suc k) A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j (Suc k) A)
i < j

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i (Suc k) A
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i (Suc k) A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have not_zero_i_plus_suc: "\<not> is_zero_row_upt_k (i+1) (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
proof (cases "j=i+1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j = i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
 2. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j = i + (1::'m)

goal (2 subgoals):
 1. j = i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
 2. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j = i + (1::'m)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
using not_zero_j_suc
[PROOF STATE]
proof (prove)
using this:
j = i + (1::'m)
\<not> is_zero_row_upt_k j (Suc k) A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal (1 subgoal):
 1. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<noteq> i + (1::'m)

goal (1 subgoal):
 1. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
have "i+1<j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + (1::'m) < j
[PROOF STEP]
by (rule Suc_less[OF i_less_j False[symmetric]])
[PROOF STATE]
proof (state)
this:
i + (1::'m) < j

goal (1 subgoal):
 1. j \<noteq> i + (1::'m) \<Longrightarrow> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i + (1::'m) < j

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
using rref_upt_condition1[OF r] not_zero_j_suc
[PROOF STATE]
proof (prove)
using this:
i + (1::'m) < j
\<forall>i. is_zero_row_upt_k i (Suc k) A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j (Suc k) A)
\<not> is_zero_row_upt_k j (Suc k) A

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
[PROOF STEP]
obtain n where a: "A $ (i+1) $ n \<noteq> 0" and n_less_suc: "to_nat n < Suc k"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>A $ (i + (1::'m)) $ n \<noteq> (0::'a); mod_type_class.to_nat n < Suc 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 < Suc k \<longrightarrow> A $ (i + (1::'m)) $ j = (0::'a))

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(LEAST n. A $ (i+1) $ n \<noteq> 0) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> n
[PROOF STEP]
by (rule Least_le, simp add: a)
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> n

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "... \<le> from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> mod_type_class.from_nat k
[PROOF STEP]
by (metis Suc_lessD from_nat_mono' from_nat_to_nat_id k_le_card less_Suc_eq_le n_less_suc ncols_def)
[PROOF STATE]
proof (state)
this:
n \<le> mod_type_class.from_nat k

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> mod_type_class.from_nat k
[PROOF STEP]
have least_le: "(LEAST n. A $ (i + 1) $ n \<noteq> 0) \<le> from_nat k"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> mod_type_class.from_nat k

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

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

goal (1 subgoal):
 1. A $ 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:
\<not> (\<forall>j. mod_type_class.to_nat j < Suc k \<longrightarrow> A $ i $ j = (0::'a))
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)

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

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

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have i_less: "i<i+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < i + (1::'m)
[PROOF STEP]
proof (rule Suc_le', rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i + (1::'m) \<noteq> (0::'m) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> i + 1 \<noteq> 0"
[PROOF STATE]
proof (state)
this:
\<not> i + (1::'m) \<noteq> (0::'m)

goal (1 subgoal):
 1. \<not> i + (1::'m) \<noteq> (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "i+1=0"
[PROOF STATE]
proof (prove)
using this:
\<not> i + (1::'m) \<noteq> (0::'m)

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

goal (1 subgoal):
 1. \<not> i + (1::'m) \<noteq> (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "i=-1"
[PROOF STATE]
proof (prove)
using this:
i + (1::'m) = (0::'m)

goal (1 subgoal):
 1. i = - (1::'m)
[PROOF STEP]
using diff_0 diff_add_cancel diff_minus_eq_add
[PROOF STATE]
proof (prove)
using this:
i + (1::'m) = (0::'m)
(0::?'a) - ?a = - ?a
?a - ?b + ?b = ?a
?a - - ?b = ?a + ?b

goal (1 subgoal):
 1. i = - (1::'m)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i = - (1::'m)

goal (1 subgoal):
 1. \<not> i + (1::'m) \<noteq> (0::'m) \<Longrightarrow> False
[PROOF STEP]
hence "j <= i"
[PROOF STATE]
proof (prove)
using this:
i = - (1::'m)

goal (1 subgoal):
 1. j \<le> i
[PROOF STEP]
using Greatest_is_minus_1
[PROOF STATE]
proof (prove)
using this:
i = - (1::'m)
\<forall>a. a \<le> - (1::?'a)

goal (1 subgoal):
 1. j \<le> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j \<le> i

goal (1 subgoal):
 1. \<not> i + (1::'m) \<noteq> (0::'m) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
j \<le> i

goal (1 subgoal):
 1. False
[PROOF STEP]
using i_less_j
[PROOF STATE]
proof (prove)
using this:
j \<le> i
i < j

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < i + (1::'m)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "from_nat k < (LEAST n. A $ (i+1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
[PROOF STEP]
using rref_upt_condition3[OF r] i_less not_zero_i_suc not_zero_i_plus_suc least_eq_k
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'m) \<and> \<not> is_zero_row_upt_k i (Suc k) A \<and> \<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
i < i + (1::'m)
\<not> is_zero_row_upt_k i (Suc k) A
\<not> is_zero_row_upt_k (i + (1::'m)) (Suc k) A
(LEAST n. A $ i $ n \<noteq> (0::'a)) = mod_type_class.from_nat k

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A; \<not> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat k < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. False
[PROOF STEP]
using least_le
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat k < (LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a))
(LEAST n. A $ (i + (1::'m)) $ n \<noteq> (0::'a)) \<le> mod_type_class.from_nat k

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduced_row_echelon_if_all_zero:
  assumes all_zero: "\<forall>n. is_zero_row_upt_k n k A"
  shows "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>n. is_zero_row_upt_k n k A

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

goal (1 subgoal):
 1. (\<forall>i. (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)) \<longrightarrow> \<not> (\<exists>j>i. \<not> (\<forall>ja. mod_type_class.to_nat ja < k \<longrightarrow> A $ j $ ja = (0::'b)))) \<and> (\<forall>i. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'b)) = (1::'b)) \<and> (\<forall>i. i < i + (1::'a) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)) \<and> \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ (i + (1::'a)) $ j = (0::'b)) \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'b)) < (LEAST n. A $ (i + (1::'a)) $ n \<noteq> (0::'b))) \<and> (\<forall>i. \<not> (\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'b)) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'b)) = (0::'b)))
[PROOF STEP]
by auto


[STATEMENT]
lemma reduced_row_echelon_form_def':
"reduced_row_echelon_form A =
  (
    (\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j. j>i \<and> \<not> is_zero_row j A)) \<and>
    (\<forall>i. \<not> (is_zero_row i A) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1) \<and>
    (\<forall>i. i<i+1 \<and> \<not> (is_zero_row i A) \<and> \<not> (is_zero_row (i+1) A) \<longrightarrow> ((LEAST k. A $ i $ k \<noteq> 0) < (LEAST k. A $ (i+1) $ k \<noteq> 0))) \<and>
    (\<forall>i. \<not> (is_zero_row i A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> 0) = 0))
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form A = ((\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a))))
[PROOF STEP]
unfolding reduced_row_echelon_form_def reduced_row_echelon_form_upt_k_def is_zero_row_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i. is_zero_row_upt_k i (ncols A) A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j (ncols A) A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i (ncols A) A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i (ncols A) A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) (ncols A) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i (ncols A) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)))) = ((\<forall>i. is_zero_row_upt_k i (ncols A) A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j (ncols A) A)) \<and> (\<forall>i. \<not> is_zero_row_upt_k i (ncols A) A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row_upt_k i (ncols A) A \<and> \<not> is_zero_row_upt_k (i + (1::'c)) (ncols A) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row_upt_k i (ncols A) A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a))))
[PROOF STEP]
..


[STATEMENT]
lemma rref_condition1:
  assumes r: "reduced_row_echelon_form A"
  shows "(\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j. j>i \<and> \<not> is_zero_row j A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

goal (1 subgoal):
 1. \<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
[PROOF STEP]
unfolding reduced_row_echelon_form_def'
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_condition2:
  assumes r: "reduced_row_echelon_form A"
  shows " (\<forall>i. \<not> (is_zero_row i A) \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
unfolding reduced_row_echelon_form_def'
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_condition3:
  assumes r: "reduced_row_echelon_form A"
  shows "(\<forall>i. i<i+1 \<and> \<not> (is_zero_row i A) \<and> \<not> (is_zero_row (i+1) A) \<longrightarrow> ((LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i+1) $ n \<noteq> 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding reduced_row_echelon_form_def'
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_condition4:
  assumes r: "reduced_row_echelon_form A"
  shows " (\<forall>i. \<not> (is_zero_row i A) \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
unfolding reduced_row_echelon_form_def'
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)) \<and> (\<forall>i. i < i + (1::'c) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'c)) A \<longrightarrow> (LEAST k. A $ i $ k \<noteq> (0::'a)) < (LEAST k. A $ (i + (1::'c)) $ k \<noteq> (0::'a))) \<and> (\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (0::'a)))

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma rref_condition1_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "is_zero_row i A"
shows "\<forall>j>i. is_zero_row j A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j>i. is_zero_row j A
[PROOF STEP]
using rref_condition1 assms
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. is_zero_row i ?A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j ?A)
reduced_row_echelon_form A
is_zero_row i A

goal (1 subgoal):
 1. \<forall>j>i. is_zero_row j A
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_condition2_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "\<not> is_zero_row i A"
shows "A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_condition2 assms
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. \<not> is_zero_row i ?A \<longrightarrow> ?A $ i $ (LEAST k. ?A $ i $ k \<noteq> (0::?'a)) = (1::?'a)
reduced_row_echelon_form A
\<not> is_zero_row i A

goal (1 subgoal):
 1. A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_condition3_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and i_le: "i < i + 1"
and "\<not> is_zero_row i A" and "\<not> is_zero_row (i + 1) A"
shows "(LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
using rref_condition3 assms
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. i < i + (1::?'c) \<and> \<not> is_zero_row i ?A \<and> \<not> is_zero_row (i + (1::?'c)) ?A \<longrightarrow> (LEAST n. ?A $ i $ n \<noteq> (0::?'a)) < (LEAST n. ?A $ (i + (1::?'c)) $ n \<noteq> (0::?'a))
reduced_row_echelon_form A
i < i + (1::'c)
\<not> is_zero_row i A
\<not> is_zero_row (i + (1::'c)) A

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'c)) $ n \<noteq> (0::'a))
[PROOF STEP]
by blast


[STATEMENT]
lemma rref_condition4_explicit:
assumes rref_A: "reduced_row_echelon_form A"
and "\<not> is_zero_row i A"
and "i \<noteq> j"
shows "A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a)
[PROOF STEP]
using rref_condition4 assms
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form ?A \<Longrightarrow> \<forall>i. \<not> is_zero_row i ?A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> ?A $ j $ (LEAST n. ?A $ i $ n \<noteq> (0::?'a)) = (0::?'a))
reduced_row_echelon_form A
\<not> is_zero_row i A
i \<noteq> j

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


[STATEMENT]
lemma rref_condition3_equiv1:
fixes A::"'a::{one, zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and i_less_j: "i<j"
and j_less_nrows: "j<nrows A"
and not_zero_i: "\<not> is_zero_row (from_nat i) A"
and not_zero_j: "\<not> is_zero_row (from_nat j) A"
shows "(LEAST n. A $ (from_nat i) $ n \<noteq> 0) < (LEAST n. A $ (from_nat j) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a))
[PROOF STEP]
using i_less_j not_zero_j j_less_nrows
[PROOF STATE]
proof (prove)
using this:
i < j
\<not> is_zero_row (mod_type_class.from_nat j) A
j < nrows A

goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a))
[PROOF STEP]
proof (induct j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i < 0; \<not> is_zero_row (mod_type_class.from_nat 0) A; 0 < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat 0 $ n \<noteq> (0::'a))
 2. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
i < 0
\<not> is_zero_row (mod_type_class.from_nat 0) A
0 < nrows A

goal (2 subgoals):
 1. \<lbrakk>i < 0; \<not> is_zero_row (mod_type_class.from_nat 0) A; 0 < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat 0 $ n \<noteq> (0::'a))
 2. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat 0 $ n \<noteq> (0::'a))
[PROOF STEP]
using "0.prems"(1)
[PROOF STATE]
proof (prove)
using this:
i < 0

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

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
assume hyp: "i < j \<Longrightarrow> \<not> is_zero_row (from_nat j) A \<Longrightarrow> j < nrows A \<Longrightarrow> (LEAST n. A $ from_nat i $ n \<noteq> 0) < (LEAST n. A $ from_nat j $ n \<noteq> 0)"
and i_less_suc_j: "i < Suc j"
and not_zero_suc_j: "\<not> is_zero_row (from_nat (Suc j)) A"
and Suc_j_less_nrows: "Suc j < nrows A"
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a))
i < Suc j
\<not> is_zero_row (mod_type_class.from_nat (Suc j)) A
Suc j < nrows A

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
have j_less: "(from_nat j::'rows) < from_nat (j+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)
[PROOF STEP]
by (rule from_nat_mono, auto simp add: Suc_j_less_nrows[unfolded nrows_def])
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
hence not_zero_j: "\<not> is_zero_row (from_nat j) A"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
using rref_condition1[OF rref] not_zero_suc_j
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)
\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
\<not> is_zero_row (mod_type_class.from_nat (Suc j)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
unfolding Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)
\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
\<not> is_zero_row (mod_type_class.from_nat (j + 1)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<lbrakk>i < j; \<not> is_zero_row (mod_type_class.from_nat j) A; j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)); i < Suc j; \<not> is_zero_row (mod_type_class.from_nat (Suc j)) A; Suc j < nrows A\<rbrakk> \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
show "(LEAST n. A $ from_nat i $ n \<noteq> 0) < (LEAST n. A $ from_nat (Suc j) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (cases "i=j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
 2. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
 2. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (unfold True Suc_eq_plus1 from_nat_suc, rule rref_condition3_explicit)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. reduced_row_echelon_form A
 2. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
 3. \<not> is_zero_row (mod_type_class.from_nat j) A
 4. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "reduced_row_echelon_form A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form A
[PROOF STEP]
using rref
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

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

goal (3 subgoals):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
 2. \<not> is_zero_row (mod_type_class.from_nat j) A
 3. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "(from_nat j::'rows) < from_nat j + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
using j_less
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)

goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
unfolding from_nat_suc
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)

goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)

goal (2 subgoals):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
 2. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "\<not> is_zero_row (from_nat j) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
using not_zero_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "\<not> is_zero_row (from_nat j + 1) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
using not_zero_suc_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat (Suc j)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
unfolding Suc_eq_plus1 from_nat_suc
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A

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

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

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
have "(LEAST n. A $ from_nat i $ n \<noteq> 0) < (LEAST n. A $ from_nat j $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule hyp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i < j
 2. \<not> is_zero_row (mod_type_class.from_nat j) A
 3. j < nrows A
[PROOF STEP]
show "i < j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j
[PROOF STEP]
using False i_less_suc_j
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
i < Suc j

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

goal (2 subgoals):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
 2. j < nrows A
[PROOF STEP]
show "\<not> is_zero_row (from_nat j) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
using not_zero_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. j < nrows A
[PROOF STEP]
show "j < nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < nrows A
[PROOF STEP]
using Suc_j_less_nrows
[PROOF STATE]
proof (prove)
using this:
Suc j < nrows A

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

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

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
have "... < (LEAST n. A $ from_nat (j+1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat j $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (j + 1) $ n \<noteq> (0::'a))
[PROOF STEP]
proof (unfold from_nat_suc, rule rref_condition3_explicit)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. reduced_row_echelon_form A
 2. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
 3. \<not> is_zero_row (mod_type_class.from_nat j) A
 4. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "reduced_row_echelon_form A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form A
[PROOF STEP]
using rref
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form A

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

goal (3 subgoals):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
 2. \<not> is_zero_row (mod_type_class.from_nat j) A
 3. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "(from_nat j::'rows) < from_nat j + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
using j_less
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat (j + 1)

goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
unfolding from_nat_suc
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)

goal (1 subgoal):
 1. mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat j < mod_type_class.from_nat j + (1::'rows)

goal (2 subgoals):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
 2. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "\<not> is_zero_row (from_nat j) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
using not_zero_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
show "\<not> is_zero_row (from_nat j + 1) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
using not_zero_suc_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat (Suc j)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
unfolding Suc_eq_plus1 from_nat_suc
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A

goal (1 subgoal):
 1. \<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (mod_type_class.from_nat j + (1::'rows)) A

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

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (j + 1) $ n \<noteq> (0::'a))
[PROOF STEP]
show "(LEAST n. A $ from_nat i $ n \<noteq> 0) < (LEAST n. A $ from_nat (Suc j) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (j + 1) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding Suc_eq_plus1
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (j + 1) $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. (LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (j + 1) $ n \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ mod_type_class.from_nat i $ n \<noteq> (0::'a)) < (LEAST n. A $ mod_type_class.from_nat (Suc j) $ n \<noteq> (0::'a))

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

goal:
No subgoals!
[PROOF STEP]
qed