[STATEMENT]
lemma rank_eq_suc_to_nat_greatest:
assumes A_not_0: "A \<noteq> 0"
shows "rank A = to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have rref: "reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
[PROOF STEP]
using rref_Gauss_Jordan
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form (Gauss_Jordan ?A)

goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))
[PROOF STEP]
unfolding reduced_row_echelon_form_def
[PROOF STATE]
proof (prove)
using this:
reduced_row_echelon_form_upt_k (Gauss_Jordan ?A) (ncols (Gauss_Jordan ?A))

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

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have not_all_zero: "\<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))
[PROOF STEP]
unfolding is_zero_row_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>a. is_zero_row a (Gauss_Jordan A))
[PROOF STEP]
using Gauss_Jordan_not_0[OF A_not_0]
[PROOF STATE]
proof (prove)
using this:
Gauss_Jordan A \<noteq> 0

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

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

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have "rank A = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
unfolding rank_Gauss_Jordan[of A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank (Gauss_Jordan A) = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
unfolding rref_rank[OF rref_Gauss_Jordan]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0} = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rank A = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rank A = card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have "... = card {i. i\<le>(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0} = card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
proof (rule bij_betw_same_card[symmetric, of "\<lambda>i. row i (Gauss_Jordan A)"], unfold bij_betw_def, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (\<lambda>i. row i (Gauss_Jordan A)) {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
 2. (\<lambda>i. row i (Gauss_Jordan A)) ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
show "inj_on (\<lambda>i. row i (Gauss_Jordan A)) {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>i. row i (Gauss_Jordan A)) {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
proof (unfold inj_on_def, auto, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); y \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); row x (Gauss_Jordan A) = row y (Gauss_Jordan A); x \<noteq> y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); y \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); row x (Gauss_Jordan A) = row y (Gauss_Jordan A); x \<noteq> y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume x: "x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))" and y: "y \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
         and xy_eq_row: "row x (Gauss_Jordan A) = row y (Gauss_Jordan A)" and x_not_y: "x \<noteq> y"
[PROOF STATE]
proof (state)
this:
x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
y \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
row x (Gauss_Jordan A) = row y (Gauss_Jordan A)
x \<noteq> y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); y \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)); row x (Gauss_Jordan A) = row y (Gauss_Jordan A); x \<noteq> y\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "x<y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> False
 2. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> False
 2. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
have "(LEAST n. (Gauss_Jordan A) $ x $ n \<noteq> 0) < (LEAST n. (Gauss_Jordan A) $ y $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ x $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan A $ y $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule rref_condition3_equiv[OF rref_Gauss_Jordan True])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row x (Gauss_Jordan A)
 2. \<not> is_zero_row y (Gauss_Jordan A)
[PROOF STEP]
show "\<not> is_zero_row x (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row x (Gauss_Jordan A)
[PROOF STEP]
by (unfold is_zero_row_def,
                    rule greatest_ge_nonzero_row'[OF rref x[unfolded is_zero_row_def] not_all_zero])
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row x (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> is_zero_row y (Gauss_Jordan A)
[PROOF STEP]
show "\<not> is_zero_row y (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row y (Gauss_Jordan A)
[PROOF STEP]
by (unfold is_zero_row_def, rule greatest_ge_nonzero_row'[OF rref y[unfolded is_zero_row_def] not_all_zero])
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row y (Gauss_Jordan A)

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

goal (2 subgoals):
 1. x < y \<Longrightarrow> False
 2. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ x $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan A $ y $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis less_irrefl row_def vec_nth_inverse xy_eq_row)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
hence x_ge_y: "x>y"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y

goal (1 subgoal):
 1. y < x
[PROOF STEP]
using x_not_y
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
x \<noteq> y

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

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
have "(LEAST n. (Gauss_Jordan A) $ y $ n \<noteq> 0) < (LEAST n. (Gauss_Jordan A) $ x $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. Gauss_Jordan A $ y $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan A $ x $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule rref_condition3_equiv[OF rref_Gauss_Jordan x_ge_y])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_zero_row y (Gauss_Jordan A)
 2. \<not> is_zero_row x (Gauss_Jordan A)
[PROOF STEP]
show "\<not> is_zero_row x (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row x (Gauss_Jordan A)
[PROOF STEP]
by (unfold is_zero_row_def, rule greatest_ge_nonzero_row'[OF rref x[unfolded is_zero_row_def] not_all_zero])
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row x (Gauss_Jordan A)

goal (1 subgoal):
 1. \<not> is_zero_row y (Gauss_Jordan A)
[PROOF STEP]
show "\<not> is_zero_row y (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row y (Gauss_Jordan A)
[PROOF STEP]
by (unfold is_zero_row_def, rule greatest_ge_nonzero_row'[OF rref y[unfolded is_zero_row_def] not_all_zero])
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row y (Gauss_Jordan A)

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

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. Gauss_Jordan A $ y $ n \<noteq> (0::'a)) < (LEAST n. Gauss_Jordan A $ x $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis less_irrefl row_def vec_nth_inverse xy_eq_row)
[PROOF STATE]
proof (state)
this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>i. row i (Gauss_Jordan A)) {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. (\<lambda>i. row i (Gauss_Jordan A)) ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
show "(\<lambda>i. row i (Gauss_Jordan A)) ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. row i (Gauss_Jordan A)) ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}
[PROOF STEP]
proof (unfold image_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>i. row xa (Gauss_Jordan A) = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0
 2. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>i. row xa (Gauss_Jordan A) = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0
 2. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
assume  xa: "xa \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (state)
this:
xa \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (2 subgoals):
 1. \<And>xa. xa \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>i. row xa (Gauss_Jordan A) = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0
 2. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
show "\<exists>i. row xa (Gauss_Jordan A) = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. row xa (Gauss_Jordan A) = row i (Gauss_Jordan A) \<and> row i (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
proof (rule exI[of _ xa], simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. row xa (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
have "\<not> is_zero_row xa (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row xa (Gauss_Jordan A)
[PROOF STEP]
by (unfold is_zero_row_def, rule greatest_ge_nonzero_row'[OF rref xa[unfolded is_zero_row_def] not_all_zero])
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row xa (Gauss_Jordan A)

goal (1 subgoal):
 1. row xa (Gauss_Jordan A) \<noteq> 0
[PROOF STEP]
thus "row xa (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row xa (Gauss_Jordan A)

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

goal (1 subgoal):
 1. vec_lambda (($) (Gauss_Jordan A $ xa)) \<noteq> 0
[PROOF STEP]
by (metis vec_nth_inverse zero_index)
[PROOF STATE]
proof (state)
this:
row xa (Gauss_Jordan A) \<noteq> 0

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

goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
assume  "row i (Gauss_Jordan A) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
row i (Gauss_Jordan A) \<noteq> 0

goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
hence "\<not> is_zero_row i (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
using this:
row i (Gauss_Jordan A) \<noteq> 0

goal (1 subgoal):
 1. \<not> is_zero_row i (Gauss_Jordan A)
[PROOF STEP]
unfolding row_def is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
vec_lambda (($) (Gauss_Jordan A $ i)) \<noteq> 0

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

goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
hence "i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i (Gauss_Jordan A)

goal (1 subgoal):
 1. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
[PROOF STEP]
using Greatest_ge
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i (Gauss_Jordan A)
?P ?k \<Longrightarrow> ?k \<le> (GREATEST x. ?P x)

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

goal (1 subgoal):
 1. \<And>i. row i (Gauss_Jordan A) \<noteq> 0 \<Longrightarrow> \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
thus "\<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
using this:
i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. \<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). row i (Gauss_Jordan A) = row x (Gauss_Jordan A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>i. row i (Gauss_Jordan A)) ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0} = card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {row i (Gauss_Jordan A) |i. row i (Gauss_Jordan A) \<noteq> 0} = card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have "... = card {i. i \<le> to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = card {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
proof (rule bij_betw_same_card[of "\<lambda>i. to_nat i"], unfold bij_betw_def, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on mod_type_class.to_nat {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
 2. mod_type_class.to_nat ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
show "inj_on to_nat {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on mod_type_class.to_nat {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
using bij_to_nat
[PROOF STATE]
proof (prove)
using this:
bij_betw mod_type_class.to_nat UNIV {0..<CARD(?'a)}

goal (1 subgoal):
 1. inj_on mod_type_class.to_nat {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
by (metis bij_betw_imp_inj_on subset_inj_on top_greatest)
[PROOF STATE]
proof (state)
this:
inj_on mod_type_class.to_nat {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. mod_type_class.to_nat ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
show "to_nat ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {i. i \<le> to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}
[PROOF STEP]
proof (unfold image_def, auto simp add: to_nat_mono')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
assume x: "x \<le> to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (state)
this:
x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
hence "from_nat x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
using this:
x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

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

goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
have "x < CARD('c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < CARD('c)
[PROOF STEP]
using x bij_to_nat[where ?'a='b]
[PROOF STATE]
proof (prove)
using this:
x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
bij_betw mod_type_class.to_nat UNIV {0..<CARD('b)}

goal (1 subgoal):
 1. x < CARD('c)
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
inj mod_type_class.to_nat \<and> range mod_type_class.to_nat = {0..<CARD('b)}

goal (1 subgoal):
 1. x < CARD('c)
[PROOF STEP]
by (metis less_le_trans not_le to_nat_less_card)
[PROOF STATE]
proof (state)
this:
x < CARD('c)

goal (1 subgoal):
 1. \<And>x. x \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) \<Longrightarrow> \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mod_type_class.from_nat x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
x < CARD('c)
[PROOF STEP]
show "\<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = to_nat xa"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
x < CARD('c)

goal (1 subgoal):
 1. \<exists>xa\<le>GREATEST a. \<not> is_zero_row a (Gauss_Jordan A). x = mod_type_class.to_nat xa
[PROOF STEP]
using to_nat_from_nat_id
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat x \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))
x < CARD('c)
?x < CARD(?'a) \<Longrightarrow> mod_type_class.to_nat (mod_type_class.from_nat ?x) = ?x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat ` {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = card {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card {i. i \<le> (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = card {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))}

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
have "... = to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
unfolding card_Collect_le_nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))) = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. i \<le> mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))} = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1

goal (1 subgoal):
 1. rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
rank A = mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_less_row_i_imp_i_is_zero:
assumes rank_less_i: "to_nat i \<ge> rank A"
shows "Gauss_Jordan A $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i = 0
[PROOF STEP]
proof (cases "A=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
 2. A \<noteq> 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = 0

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

goal (1 subgoal):
 1. Gauss_Jordan A $ i = 0
[PROOF STEP]
by (metis A_0_imp_Gauss_Jordan_0 zero_index)
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ i = 0

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

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
[PROOF STEP]
have "to_nat i \<ge> to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1 \<le> mod_type_class.to_nat i
[PROOF STEP]
using rank_less_i
[PROOF STATE]
proof (prove)
using this:
rank A \<le> mod_type_class.to_nat i

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

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

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
[PROOF STEP]
hence "i>(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) + 1 \<le> mod_type_class.to_nat i

goal (1 subgoal):
 1. (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < i
[PROOF STEP]
by (metis One_nat_def add.commute add_strict_increasing
    add_strict_increasing2 le0 lessI neq_iff not_le to_nat_mono)
[PROOF STATE]
proof (state)
this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < i

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
[PROOF STEP]
hence "is_zero_row i (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < i

goal (1 subgoal):
 1. is_zero_row i (Gauss_Jordan A)
[PROOF STEP]
using not_greater_Greatest
[PROOF STATE]
proof (prove)
using this:
(GREATEST a. \<not> is_zero_row a (Gauss_Jordan A)) < i
(GREATEST x. ?P x) < ?k \<Longrightarrow> \<not> ?P ?k

goal (1 subgoal):
 1. is_zero_row i (Gauss_Jordan A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_zero_row i (Gauss_Jordan A)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> Gauss_Jordan A $ i = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row i (Gauss_Jordan A)

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

goal (1 subgoal):
 1. \<forall>ia. Gauss_Jordan A $ i $ ia = 0 $ ia
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A $ i = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rank_Gauss_Jordan_eq:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = (let A'=(Gauss_Jordan A) in card {row i A' |i. row i A' \<noteq> 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = (let A' = Gauss_Jordan A in card {row i A' |i. row i A' \<noteq> 0})
[PROOF STEP]
by (metis (mono_tags) rank_Gauss_Jordan rref_Gauss_Jordan rref_rank)


[STATEMENT]
lemma [code abstract]:
shows "vec_nth (Gauss_Jordan_in_ij A i j) = (let n = (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n);
  interchange_A = (interchange_rows A i n);
  A' = mult_row interchange_A i (1/interchange_A$i$j) in
  (% s. if s=i then A' $ s else (row_add A' s i (-(interchange_A$s$j))) $ s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (Gauss_Jordan_in_ij A i j) = (let n = LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n; interchange_A = interchange_rows A i n; A' = mult_row interchange_A i ((1::'b) / interchange_A $ i $ j) in (\<lambda>s. if s = i then A' $ s else row_add A' s i (- interchange_A $ s $ j) $ s))
[PROOF STEP]
unfolding Gauss_Jordan_in_ij_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n)) i ((1::'b) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n)) i ((1::'b) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ s $ j) $ s) = (\<lambda>s. if s = i then mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n)) i ((1::'b) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ i $ j) $ s else row_add (mult_row (interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n)) i ((1::'b) / interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ i $ j)) s i (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> (0::'b) \<and> i \<le> n) $ s $ j) $ s)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma rank_Gauss_Jordan_code[code]:
  fixes A::"'a::{field}^'n::{mod_type}^'m::{mod_type}"
  shows "rank A = (if A = 0 then 0 else (let A'=(Gauss_Jordan A) in to_nat (GREATEST a. row a A' \<noteq> 0) + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
proof (cases "A = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
 2. A \<noteq> 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = 0

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
 2. A \<noteq> 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
unfolding if_P[OF True]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = 0
[PROOF STEP]
unfolding True  rank_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
A \<noteq> 0

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
unfolding if_not_P[OF False]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = (let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)
[PROOF STEP]
unfolding rank_eq_suc_to_nat_greatest[OF False] Let_def is_zero_row_eq_row_zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1 = mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
rank A = (if A = 0 then 0 else let A' = Gauss_Jordan A in mod_type_class.to_nat (GREATEST a. row a A' \<noteq> 0) + 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_null_space[code_unfold]:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  shows "vec.dim (null_space A) = (vec.dimension TYPE('a) TYPE('cols)) - rank (A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (null_space A) = finite_dimensional_vector_space.dimension cart_basis - rank A
[PROOF STEP]
apply (rule add_implies_diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (null_space A) + rank A = finite_dimensional_vector_space.dimension cart_basis
[PROOF STEP]
using rank_nullity_theorem_matrices
[PROOF STATE]
proof (prove)
using this:
ncols ?A = vec.dim (null_space ?A) + vec.dim (col_space ?A)

goal (1 subgoal):
 1. vec.dim (null_space A) + rank A = finite_dimensional_vector_space.dimension cart_basis
[PROOF STEP]
unfolding rank_eq_dim_col_space[of A]
[PROOF STATE]
proof (prove)
using this:
ncols ?A = vec.dim (null_space ?A) + vec.dim (col_space ?A)

goal (1 subgoal):
 1. vec.dim (null_space A) + vec.dim (col_space A) = finite_dimensional_vector_space.dimension cart_basis
[PROOF STEP]
unfolding dimension_vector ncols_def
[PROOF STATE]
proof (prove)
using this:
CARD(?'cols) = vec.dim (null_space ?A) + vec.dim (col_space ?A)

goal (1 subgoal):
 1. vec.dim (null_space A) + vec.dim (col_space A) = CARD('cols)
[PROOF STEP]
..


[STATEMENT]
lemma rank_eq_dim_col_space'[code_unfold]:
 fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
 shows "vec.dim (col_space A) = rank A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (col_space A) = rank A
[PROOF STEP]
unfolding  rank_eq_dim_col_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (col_space A) = vec.dim (col_space A)
[PROOF STEP]
..


[STATEMENT]
lemma dim_left_null_space[code_unfold]:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  shows "vec.dim (left_null_space A) = (vec.dimension TYPE('a) TYPE('rows)) - rank (A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (left_null_space A) = finite_dimensional_vector_space.dimension cart_basis - rank A
[PROOF STEP]
unfolding left_null_space_eq_null_space_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (null_space (Finite_Cartesian_Product.transpose A)) = finite_dimensional_vector_space.dimension cart_basis - rank A
[PROOF STEP]
unfolding dim_null_space
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_dimensional_vector_space.dimension cart_basis - rank (Finite_Cartesian_Product.transpose A) = finite_dimensional_vector_space.dimension cart_basis - rank A
[PROOF STEP]
unfolding rank_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_dimensional_vector_space.dimension cart_basis - rank A = finite_dimensional_vector_space.dimension cart_basis - rank A
[PROOF STEP]
..


[STATEMENT]
lemma matrix_to_iarray_bezout_matrix:
  shows "matrix_to_iarray (bezout_matrix A a b j bezout)
  = bezout_matrix_iarrays (matrix_to_iarray A) (to_nat a) (to_nat b) (to_nat j) bezout"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have n: "nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> from_nat) [0..<CARD('b)]))
    = CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)])) = CARD('b)
[PROOF STEP]
unfolding nrows_iarray_def vec_to_iarray_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray.length (IArray (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)])) = CARD('b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)])) = CARD('b)

goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have rw1:"(map (\<lambda>x. IArray.of_fun
    (\<lambda>i. A $ from_nat x $ from_nat i) CARD('c)) [0..<CARD('b)] ! to_nat a !! to_nat j) = A $ a $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat a !! mod_type_class.to_nat j = A $ a $ j
[PROOF STEP]
by (metis (erased, lifting) from_nat_to_nat_id length_upt minus_nat.diff_0 nth_map
      nth_upt of_fun_nth plus_nat.add_0 to_nat_less_card)
[PROOF STATE]
proof (state)
this:
map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat a !! mod_type_class.to_nat j = A $ a $ j

goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have rw2: "(map (\<lambda>x. IArray.of_fun
    (\<lambda>i. A $ from_nat x $ from_nat i) CARD('c)) [0..<CARD('b)] ! to_nat b !! to_nat j) = (A $ b $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat b !! mod_type_class.to_nat j = A $ b $ j
[PROOF STEP]
by (metis (erased, lifting) from_nat_to_nat_id length_upt minus_nat.diff_0 nth_map
      nth_upt of_fun_nth plus_nat.add_0 to_nat_less_card)
[PROOF STATE]
proof (state)
this:
map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat b !! mod_type_class.to_nat j = A $ b $ j

goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have rw3: "IArray (map (\<lambda>x. IArray.of_fun
    (\<lambda>i. A $ from_nat x $ from_nat i) CARD('c)) [0..<CARD('b)]) !! to_nat a !! to_nat j = A $ a $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)]) !! mod_type_class.to_nat a !! mod_type_class.to_nat j = A $ a $ j
[PROOF STEP]
by (metis IArray.sub_def list_of.simps rw1)
[PROOF STATE]
proof (state)
this:
IArray (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)]) !! mod_type_class.to_nat a !! mod_type_class.to_nat j = A $ a $ j

goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
have rw4: "IArray (map (\<lambda>x. IArray.of_fun
    (\<lambda>i. A $ from_nat x $ from_nat i) CARD('c)) [0..<CARD('b)]) !! to_nat b !! to_nat j = A $ b $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)]) !! mod_type_class.to_nat b !! mod_type_class.to_nat j = A $ b $ j
[PROOF STEP]
by (metis IArray.sub_def list_of.simps rw2)
[PROOF STATE]
proof (state)
this:
IArray (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)]) !! mod_type_class.to_nat b !! mod_type_class.to_nat j = A $ b $ j

goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout
[PROOF STEP]
unfolding matrix_to_iarray_def bezout_matrix_iarrays_def tabulate2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IArray (map (vec_to_iarray \<circ> ($) (bezout_matrix A a b j bezout) \<circ> mod_type_class.from_nat) [0..<CARD('b)]) = IArray.of_fun (\<lambda>i. IArray.of_fun ((let (p, q, u, v, d) = bezout (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)]) !! mod_type_class.to_nat a !! mod_type_class.to_nat j) (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)]) !! mod_type_class.to_nat b !! mod_type_class.to_nat j) in (\<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a))) i) (nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)])))) (nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)])))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (vec_to_iarray \<circ> ($) (bezout_matrix A a b j bezout) \<circ> mod_type_class.from_nat) [0..<CARD('b)] = map (\<lambda>i. IArray (map ((case bezout (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat a) ! mod_type_class.to_nat j) (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat b) ! mod_type_class.to_nat j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) i) [0..<nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)]))])) [0..<nrows_iarray (IArray (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)]))]
[PROOF STEP]
unfolding n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (vec_to_iarray \<circ> ($) (bezout_matrix A a b j bezout) \<circ> mod_type_class.from_nat) [0..<CARD('b)] = map (\<lambda>i. IArray (map ((case bezout (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat a) ! mod_type_class.to_nat j) (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat b) ! mod_type_class.to_nat j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) i) [0..<CARD('b)])) [0..<CARD('b)]
[PROOF STEP]
apply (rule map_ext, auto simp add: bezout_matrix_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < CARD('b) \<Longrightarrow> vec_to_iarray (\<chi>y. case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> y = a then p else if mod_type_class.from_nat x = a \<and> y = b then q else if mod_type_class.from_nat x = b \<and> y = a then u else if mod_type_class.from_nat x = b \<and> y = b then v else if mod_type_class.from_nat x = y then 1::'a else (0::'a)) = IArray (map ((case bezout (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat a) ! mod_type_class.to_nat j) (IArray.list_of (map (vec_to_iarray \<circ> ($) A \<circ> mod_type_class.from_nat) [0..<CARD('b)] ! mod_type_class.to_nat b) ! mod_type_class.to_nat j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x) [0..<CARD('b)])
[PROOF STEP]
unfolding o_def vec_to_iarray_def  Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < CARD('b) \<Longrightarrow> IArray.of_fun (\<lambda>i. (\<chi>y. case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> y = a then p else if mod_type_class.from_nat x = a \<and> y = b then q else if mod_type_class.from_nat x = b \<and> y = a then u else if mod_type_class.from_nat x = b \<and> y = b then v else if mod_type_class.from_nat x = y then 1::'a else (0::'a)) $ mod_type_class.from_nat i) CARD('b) = IArray (map ((case bezout (IArray.list_of (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat a) ! mod_type_class.to_nat j) (IArray.list_of (map (\<lambda>x. IArray.of_fun (\<lambda>i. A $ mod_type_class.from_nat x $ mod_type_class.from_nat i) CARD('c)) [0..<CARD('b)] ! mod_type_class.to_nat b) ! mod_type_class.to_nat j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x) [0..<CARD('b)])
[PROOF STEP]
unfolding IArray.sub_def[symmetric] rw1 rw2 rw3 rw4
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < CARD('b) \<Longrightarrow> IArray.of_fun (\<lambda>i. (\<chi>y. case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> y = a then p else if mod_type_class.from_nat x = a \<and> y = b then q else if mod_type_class.from_nat x = b \<and> y = a then u else if mod_type_class.from_nat x = b \<and> y = b then v else if mod_type_class.from_nat x = y then 1::'a else (0::'a)) $ mod_type_class.from_nat i) CARD('b) = IArray (map ((case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x) [0..<CARD('b)])
[PROOF STEP]
unfolding IArray.of_fun_def iarray.inject
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x < CARD('b) \<Longrightarrow> map (\<lambda>i. (\<chi>y. case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> y = a then p else if mod_type_class.from_nat x = a \<and> y = b then q else if mod_type_class.from_nat x = b \<and> y = a then u else if mod_type_class.from_nat x = b \<and> y = b then v else if mod_type_class.from_nat x = y then 1::'a else (0::'a)) $ mod_type_class.from_nat i) [0..<CARD('b)] = map ((case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x) [0..<CARD('b)]
[PROOF STEP]
apply (rule map_ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. x < CARD('b) \<Longrightarrow> xa \<in> set [0..<CARD('b)] \<longrightarrow> (\<chi>y. case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> y = a then p else if mod_type_class.from_nat x = a \<and> y = b then q else if mod_type_class.from_nat x = b \<and> y = a then u else if mod_type_class.from_nat x = b \<and> y = b then v else if mod_type_class.from_nat x = y then 1::'a else (0::'a)) $ mod_type_class.from_nat xa = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
unfolding vec_lambda_beta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. x < CARD('b) \<Longrightarrow> xa \<in> set [0..<CARD('b)] \<longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
fix x xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
assume x: "x < CARD('b)"
[PROOF STATE]
proof (state)
this:
x < CARD('b)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
assume "xa \<in> set [0..<CARD('b)]"
[PROOF STATE]
proof (state)
this:
xa \<in> set [0..<CARD('b)]

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
hence xa: "xa < CARD('b)"
[PROOF STATE]
proof (prove)
using this:
xa \<in> set [0..<CARD('b)]

goal (1 subgoal):
 1. xa < CARD('b)
[PROOF STEP]
using atLeast_upt
[PROOF STATE]
proof (prove)
using this:
xa \<in> set [0..<CARD('b)]
{..<?n} = set [0..<?n]

goal (1 subgoal):
 1. xa < CARD('b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xa < CARD('b)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have rw5: "(from_nat x = a) = (x = to_nat a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.from_nat x = a) = (x = mod_type_class.to_nat a)
[PROOF STEP]
using x from_nat_not_eq from_nat_to_nat_id
[PROOF STATE]
proof (prove)
using this:
x < CARD('b)
\<lbrakk>?a \<noteq> mod_type_class.to_nat ?b; ?a < CARD(?'a)\<rbrakk> \<Longrightarrow> mod_type_class.from_nat ?a \<noteq> ?b
mod_type_class.from_nat (mod_type_class.to_nat ?x) = ?x

goal (1 subgoal):
 1. (mod_type_class.from_nat x = a) = (x = mod_type_class.to_nat a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(mod_type_class.from_nat x = a) = (x = mod_type_class.to_nat a)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have rw6: "(from_nat x = b) = (x = to_nat b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.from_nat x = b) = (x = mod_type_class.to_nat b)
[PROOF STEP]
by (metis x from_nat_to_nat_id to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
(mod_type_class.from_nat x = b) = (x = mod_type_class.to_nat b)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have rw7: "(from_nat xa = b) = (xa = to_nat b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.from_nat xa = b) = (xa = mod_type_class.to_nat b)
[PROOF STEP]
by (metis xa from_nat_to_nat_id to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
(mod_type_class.from_nat xa = b) = (xa = mod_type_class.to_nat b)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have rw8: "((from_nat x::'b) = (from_nat xa::'b)) = (x = xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.from_nat x = mod_type_class.from_nat xa) = (x = xa)
[PROOF STEP]
by (metis from_nat_not_eq x xa)
[PROOF STATE]
proof (state)
this:
(mod_type_class.from_nat x = mod_type_class.from_nat xa) = (x = xa)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have rw9: "(from_nat xa = a) = (xa = to_nat a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mod_type_class.from_nat xa = a) = (xa = mod_type_class.to_nat a)
[PROOF STEP]
by (metis from_nat_to_nat_id to_nat_from_nat_id xa)
[PROOF STATE]
proof (state)
this:
(mod_type_class.from_nat xa = a) = (xa = mod_type_class.to_nat a)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have cond01: "(from_nat x = a \<and> from_nat xa = a) == (x = to_nat a \<and> xa = to_nat a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a
[PROOF STEP]
using rw5 rw9
[PROOF STATE]
proof (prove)
using this:
(mod_type_class.from_nat x = a) = (x = mod_type_class.to_nat a)
(mod_type_class.from_nat xa = a) = (xa = mod_type_class.to_nat a)

goal (1 subgoal):
 1. mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have cond02: "(from_nat x = a \<and> from_nat xa = b) == (x = to_nat a \<and> xa = to_nat b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b
[PROOF STEP]
using rw5 rw7
[PROOF STATE]
proof (prove)
using this:
(mod_type_class.from_nat x = a) = (x = mod_type_class.to_nat a)
(mod_type_class.from_nat xa = b) = (xa = mod_type_class.to_nat b)

goal (1 subgoal):
 1. mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have cond03: "(from_nat x = b \<and> from_nat xa = a) == (x = to_nat b \<and> xa = to_nat a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a
[PROOF STEP]
using rw6 rw9
[PROOF STATE]
proof (prove)
using this:
(mod_type_class.from_nat x = b) = (x = mod_type_class.to_nat b)
(mod_type_class.from_nat xa = a) = (xa = mod_type_class.to_nat a)

goal (1 subgoal):
 1. mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have cond04: "(from_nat x = b \<and> from_nat xa = b) == (x = to_nat b \<and> xa = to_nat b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b
[PROOF STEP]
using rw6 rw7
[PROOF STATE]
proof (prove)
using this:
(mod_type_class.from_nat x = b) = (x = mod_type_class.to_nat b)
(mod_type_class.from_nat xa = b) = (xa = mod_type_class.to_nat b)

goal (1 subgoal):
 1. mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b \<equiv> x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
have cond05: "((from_nat x::'b) = (from_nat xa::'b)) == (x = xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat x = mod_type_class.from_nat xa \<equiv> x = xa
[PROOF STEP]
using rw8
[PROOF STATE]
proof (prove)
using this:
(mod_type_class.from_nat x = mod_type_class.from_nat xa) = (x = xa)

goal (1 subgoal):
 1. mod_type_class.from_nat x = mod_type_class.from_nat xa \<equiv> x = xa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat x = mod_type_class.from_nat xa \<equiv> x = xa

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < CARD('b); xa \<in> set [0..<CARD('b)]\<rbrakk> \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
show "(case bezout (A $ a $ j) (A $ b $ j) of
             (p, q, u, v, d) \<Rightarrow>
               if from_nat x = a \<and> from_nat xa = a then p
               else if from_nat x = a \<and> from_nat xa = b then q
                    else if from_nat x = b \<and> from_nat xa = a then u
                         else if from_nat x = b \<and> from_nat xa = b then v
                              else if (from_nat x::'b) = from_nat xa then 1 else 0) =
            (case bezout (A $ a $ j) (A $ b $ j) of
             (p, q, u, v, d) \<Rightarrow>
               \<lambda>x y. if x = to_nat a \<and> y = to_nat a then p
                     else if x = to_nat a \<and> y = to_nat b then q
                          else if x = to_nat b \<and> y = to_nat a then u
                               else if x = to_nat b \<and> y = to_nat b then v
                                    else if x = y then 1 else 0)
             x xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
proof (cases "bezout (A $ a $ j) (A $ b $ j)")
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa ba c d e. bezout (A $ a $ j) (A $ b $ j) = (aa, ba, c, d, e) \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
fix p q u v d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa ba c d e. bezout (A $ a $ j) (A $ b $ j) = (aa, ba, c, d, e) \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
assume b: "bezout (A $ a $ j) (A $ b $ j) = (p, q, u, v, d)"
[PROOF STATE]
proof (state)
this:
bezout (A $ a $ j) (A $ b $ j) = (p, q, u, v, d)

goal (1 subgoal):
 1. \<And>aa ba c d e. bezout (A $ a $ j) (A $ b $ j) = (aa, ba, c, d, e) \<Longrightarrow> (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
unfolding b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (p, q, u, v, d) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case (p, q, u, v, d) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
unfolding cond01
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
unfolding cond02
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
unfolding cond03
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
unfolding cond04
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
unfolding cond05
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a)) = (if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> xa = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> xa = mod_type_class.to_nat b then v else if x = xa then 1::'a else (0::'a))
[PROOF STEP]
by (rule refl)
[PROOF STATE]
proof (state)
this:
(case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = a then p else if mod_type_class.from_nat x = a \<and> mod_type_class.from_nat xa = b then q else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = a then u else if mod_type_class.from_nat x = b \<and> mod_type_class.from_nat xa = b then v else if mod_type_class.from_nat x = mod_type_class.from_nat xa then 1::'a else (0::'a)) = (case bezout (A $ a $ j) (A $ b $ j) of (p, q, u, v, d) \<Rightarrow> \<lambda>x y. if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat a then p else if x = mod_type_class.to_nat a \<and> y = mod_type_class.to_nat b then q else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat a then u else if x = mod_type_class.to_nat b \<and> y = mod_type_class.to_nat b then v else if x = y then 1::'a else (0::'a)) x xa

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (bezout_matrix A a b j bezout) = bezout_matrix_iarrays (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat b) (mod_type_class.to_nat j) bezout

goal:
No subgoals!
[PROOF STEP]
qed