[STATEMENT]
lemma rank_less_imp_inconsistent:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes inc: "rank A < (if (\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) then (to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1) else 0)"
  shows "inconsistent A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsistent A b
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
define i where "i = (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
i = (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
define j where "j = (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))"
[PROOF STATE]
proof (state)
this:
j = (GREATEST a. \<not> is_zero_row a (Gauss_Jordan A))

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
assume "\<not> inconsistent A b"
[PROOF STATE]
proof (state)
this:
\<not> inconsistent A b

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
hence ex_solution: "\<exists>x. is_solution x A b"
[PROOF STATE]
proof (prove)
using this:
\<not> inconsistent A b

goal (1 subgoal):
 1. \<exists>x. is_solution x A b
[PROOF STEP]
unfolding inconsistent_def consistent_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<nexists>x. is_solution x A b)

goal (1 subgoal):
 1. \<exists>x. is_solution x A b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. is_solution x A b

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. is_solution x A b
[PROOF STEP]
obtain x where "is_solution x A b"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. is_solution x A b

goal (1 subgoal):
 1. (\<And>x. is_solution x A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_solution x A b

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
hence is_solution_solve: "is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)"
[PROOF STATE]
proof (prove)
using this:
is_solution x A b

goal (1 subgoal):
 1. is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)
[PROOF STEP]
using is_solution_solve_system
[PROOF STATE]
proof (prove)
using this:
is_solution x A b
is_solution ?x ?A ?b = is_solution ?x (fst (solve_system ?A ?b)) (snd (solve_system ?A ?b))

goal (1 subgoal):
 1. is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)
[PROOF STEP]
by (metis Gauss_Jordan_PA_eq P_Gauss_Jordan_def fst_conv snd_conv solve_system_def)
[PROOF STATE]
proof (state)
this:
is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)

goal (1 subgoal):
 1. \<not> inconsistent A b \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "A=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = 0 \<Longrightarrow> False
 2. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = 0

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> False
 2. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence rank_eq_0: "rank A = 0"
[PROOF STATE]
proof (prove)
using this:
A = 0

goal (1 subgoal):
 1. rank A = 0
[PROOF STEP]
using rank_0
[PROOF STATE]
proof (prove)
using this:
A = 0
rank 0 = 0

goal (1 subgoal):
 1. rank A = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rank A = 0

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> False
 2. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence exists_not_0:"(\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)"
[PROOF STATE]
proof (prove)
using this:
rank A = 0

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
[PROOF STEP]
using inc
[PROOF STATE]
proof (prove)
using this:
rank A = 0
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
[PROOF STEP]
unfolding inconsistent
[PROOF STATE]
proof (prove)
using this:
rank A = 0
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
[PROOF STEP]
using to_nat_plus_1_set[of "(GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)"]
[PROOF STATE]
proof (prove)
using this:
rank A = 0
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)
mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 \<in> {1..<CARD('rows) + 1}

goal (1 subgoal):
 1. \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)

goal (2 subgoals):
 1. A = 0 \<Longrightarrow> False
 2. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using True \<open>is_solution x A b\<close> exists_not_0 is_solution_def
[PROOF STATE]
proof (prove)
using this:
A = 0
is_solution x A b
\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)
is_solution ?x ?A ?b = (?A *v ?x = ?b)

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

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

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have j_less_i: "j<i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j < i
[PROOF STEP]
have rank_less_greatest_i: "rank A < to_nat i + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A < mod_type_class.to_nat i + 1
[PROOF STEP]
using inc
[PROOF STATE]
proof (prove)
using this:
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. rank A < mod_type_class.to_nat i + 1
[PROOF STEP]
unfolding i_def inconsistent
[PROOF STATE]
proof (prove)
using this:
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. rank A < mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
rank A < mod_type_class.to_nat i + 1

goal (1 subgoal):
 1. j < i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rank A < mod_type_class.to_nat i + 1

goal (1 subgoal):
 1. j < i
[PROOF STEP]
have rank_eq_greatest_A: "rank A = to_nat j + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rank A = mod_type_class.to_nat j + 1
[PROOF STEP]
unfolding j_def
[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]
by (rule rank_eq_suc_to_nat_greatest[OF False])
[PROOF STATE]
proof (state)
this:
rank A = mod_type_class.to_nat j + 1

goal (1 subgoal):
 1. j < i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rank A < mod_type_class.to_nat i + 1
rank A = mod_type_class.to_nat j + 1
[PROOF STEP]
have "to_nat j + 1 < to_nat i + 1"
[PROOF STATE]
proof (prove)
using this:
rank A < mod_type_class.to_nat i + 1
rank A = mod_type_class.to_nat j + 1

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

goal (1 subgoal):
 1. j < i
[PROOF STEP]
hence "to_nat j < to_nat i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j + 1 < mod_type_class.to_nat i + 1

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

goal (1 subgoal):
 1. j < i
[PROOF STEP]
thus "j<i"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat j < mod_type_class.to_nat i

goal (1 subgoal):
 1. j < i
[PROOF STEP]
by (metis (full_types) not_le to_nat_mono')
[PROOF STATE]
proof (state)
this:
j < i

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

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have is_zero_i: "is_zero_row i (Gauss_Jordan A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row i (Gauss_Jordan A)
[PROOF STEP]
by (metis (full_types) j_def j_less_i not_greater_Greatest)
[PROOF STATE]
proof (state)
this:
is_zero_row i (Gauss_Jordan A)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "(Gauss_Jordan A *v x) $ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i = (0::'a)
[PROOF STEP]
proof (unfold matrix_vector_mult_def, auto, rule sum.neutral,clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> UNIV \<Longrightarrow> Gauss_Jordan A $ i $ xa * x $ xa = (0::'a)
[PROOF STEP]
fix a::'cols
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> UNIV \<Longrightarrow> Gauss_Jordan A $ i $ xa * x $ xa = (0::'a)
[PROOF STEP]
show "Gauss_Jordan A $ i $ a * x $ a = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A $ i $ a * x $ a = (0::'a)
[PROOF STEP]
using is_zero_i
[PROOF STATE]
proof (prove)
using this:
is_zero_row i (Gauss_Jordan A)

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

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

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

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Gauss_Jordan A *v x) $ i = (0::'a)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "(Gauss_Jordan A *v x) $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
have "Gauss_Jordan A *v x = P_Gauss_Jordan A *v b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Gauss_Jordan A *v x = P_Gauss_Jordan A *v b
[PROOF STEP]
using is_solution_def is_solution_solve
[PROOF STATE]
proof (prove)
using this:
is_solution ?x ?A ?b = (?A *v ?x = ?b)
is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)

goal (1 subgoal):
 1. Gauss_Jordan A *v x = P_Gauss_Jordan A *v b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A *v x = P_Gauss_Jordan A *v b

goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Gauss_Jordan A *v x = P_Gauss_Jordan A *v b

goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
have "... $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P_Gauss_Jordan A *v b) $ i \<noteq> (0::'a)
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P_Gauss_Jordan A *v b) $ (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
proof (rule GreatestI_ex)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> (0::'a)
[PROOF STEP]
show "\<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> (0::'a)
[PROOF STEP]
using inc
[PROOF STATE]
proof (prove)
using this:
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. \<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> (0::'a)
[PROOF STEP]
unfolding i_def inconsistent
[PROOF STATE]
proof (prove)
using this:
rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)

goal (1 subgoal):
 1. \<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> (0::'a)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<exists>x. (P_Gauss_Jordan A *v b) $ x \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P_Gauss_Jordan A *v b) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. (Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Gauss_Jordan A *v x) $ i \<noteq> (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Gauss_Jordan A *v x) $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. A \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Gauss_Jordan A *v x) $ i = (0::'a)
(Gauss_Jordan A *v x) $ i \<noteq> (0::'a)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
(Gauss_Jordan A *v x) $ i = (0::'a)
(Gauss_Jordan A *v x) $ i \<noteq> (0::'a)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inconsistent_eq_rank_less:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  shows "inconsistent A b = (rank A < (if (\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)
                                            then (to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1) else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsistent A b = (rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0))
[PROOF STEP]
using inconsistent_imp_rank_less rank_less_imp_inconsistent
[PROOF STATE]
proof (prove)
using this:
inconsistent ?A ?b \<Longrightarrow> rank ?A < (if \<exists>a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a)) + 1 else 0)
rank ?A < (if \<exists>a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a)) + 1 else 0) \<Longrightarrow> inconsistent ?A ?b

goal (1 subgoal):
 1. inconsistent A b = (rank A < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0))
[PROOF STEP]
by blast


[STATEMENT]
lemma consistent_eq_rank_ge:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  shows "consistent A b = (rank A \<ge> (if (\<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0)
                                            then (to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> 0) + 1) else 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent A b = ((if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A)
[PROOF STEP]
using consistent_imp_rank_ge rank_ge_imp_consistent
[PROOF STATE]
proof (prove)
using this:
consistent ?A ?b \<Longrightarrow> (if \<exists>a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a)) + 1 else 0) \<le> rank ?A
(if \<exists>a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan ?A *v ?b) $ a \<noteq> (0::?'a)) + 1 else 0) \<le> rank ?A \<Longrightarrow> consistent ?A ?b

goal (1 subgoal):
 1. consistent A b = ((if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank A)
[PROOF STEP]
by blast


[STATEMENT]
lemma inconsistent_eq_rank_less_code[code]:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "inconsistent A b = (let GJ_P=Gauss_Jordan_PA A;
                                P_mult_b = (fst(GJ_P) *v b);
                                rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1)  in (rank_A < (if (\<exists>a. P_mult_b $ a \<noteq> 0)
                                            then (to_nat (GREATEST a. P_mult_b $ a \<noteq> 0) + 1) else 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inconsistent A b = (let GJ_P = Gauss_Jordan_PA A; P_mult_b = fst GJ_P *v b; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1 in rank_A < (if \<exists>a. P_mult_b $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. P_mult_b $ a \<noteq> (0::'a)) + 1 else 0))
[PROOF STEP]
unfolding inconsistent_eq_rank_less Let_def rank_Gauss_Jordan_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) < (if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0)) = ((if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) < (if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0))
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) < (if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0)) = ((if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) < (if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0))
[PROOF STEP]
..


[STATEMENT]
lemma consistent_eq_rank_ge_code[code]:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "consistent A b = (let GJ_P=Gauss_Jordan_PA A;
                              P_mult_b = (fst(GJ_P) *v b);
                              rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1) in (rank_A \<ge> (if (\<exists>a. P_mult_b $ a \<noteq> 0)
                                            then (to_nat (GREATEST a. P_mult_b $ a \<noteq> 0) + 1) else 0)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent A b = (let GJ_P = Gauss_Jordan_PA A; P_mult_b = fst GJ_P *v b in Let (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1) ((\<le>) (if \<exists>a. P_mult_b $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. P_mult_b $ a \<noteq> (0::'a)) + 1 else 0)))
[PROOF STEP]
unfolding consistent_eq_rank_ge Let_def rank_Gauss_Jordan_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (P_Gauss_Jordan A *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1)) = ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1))
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1)) = ((if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1))
[PROOF STEP]
..


[STATEMENT]
lemma null_space_eq_solution_set:
shows "null_space A = solution_set A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null_space A = solution_set A 0
[PROOF STEP]
unfolding null_space_def solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. A *v x = 0} = {x. A *v x = 0}
[PROOF STEP]
..


[STATEMENT]
lemma zero_is_solution_homogeneous_system:
shows "0 \<in> (solution_set A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> solution_set A 0
[PROOF STEP]
unfolding solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> {x. A *v x = 0}
[PROOF STEP]
using matrix_vector_mult_0_right
[PROOF STATE]
proof (prove)
using this:
?A *v 0 = 0

goal (1 subgoal):
 1. 0 \<in> {x. A *v x = 0}
[PROOF STEP]
by fast


[STATEMENT]
lemma homogeneous_solution_set_subspace:
fixes A::"'a::{field}^'n^'rows"
shows "vec.subspace (solution_set A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.subspace (solution_set A 0)
[PROOF STEP]
using subspace_null_space[of A]
[PROOF STATE]
proof (prove)
using this:
vec.subspace (null_space A)

goal (1 subgoal):
 1. vec.subspace (solution_set A 0)
[PROOF STEP]
unfolding null_space_eq_solution_set
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set A 0)

goal (1 subgoal):
 1. vec.subspace (solution_set A 0)
[PROOF STEP]
.


[STATEMENT]
lemma solution_set_rel:
fixes A::"'a::{field}^'n^'rows"
assumes p: "is_solution p A b"
shows "solution_set A b = {p} + (solution_set A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A b = {p} + solution_set A 0
[PROOF STEP]
proof (unfold set_plus_def, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
fix ba
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
assume ba: "ba \<in> solution_set A 0"
[PROOF STATE]
proof (state)
this:
ba \<in> solution_set A 0

goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
have "A *v (p + ba) = (A *v p) + (A *v ba)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v (p + ba) = A *v p + A *v ba
[PROOF STEP]
unfolding matrix_vector_right_distrib
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v p + A *v ba = A *v p + A *v ba
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
A *v (p + ba) = A *v p + A *v ba

goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *v (p + ba) = A *v p + A *v ba

goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
have "... = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v p + A *v ba = b
[PROOF STEP]
using p ba
[PROOF STATE]
proof (prove)
using this:
is_solution p A b
ba \<in> solution_set A 0

goal (1 subgoal):
 1. A *v p + A *v ba = b
[PROOF STEP]
unfolding solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
using this:
A *v p = b
ba \<in> {x. A *v x = 0}

goal (1 subgoal):
 1. A *v p + A *v ba = b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A *v p + A *v ba = b

goal (2 subgoals):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
 2. \<And>ba. ba \<in> solution_set A 0 \<Longrightarrow> p + ba \<in> solution_set A b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A *v (p + ba) = b
[PROOF STEP]
show "p + ba \<in> solution_set A b"
[PROOF STATE]
proof (prove)
using this:
A *v (p + ba) = b

goal (1 subgoal):
 1. p + ba \<in> solution_set A b
[PROOF STEP]
unfolding solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
using this:
A *v (p + ba) = b

goal (1 subgoal):
 1. p + ba \<in> {x. A *v x = b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p + ba \<in> solution_set A b

goal (1 subgoal):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
[PROOF STEP]
assume x: "x \<in> solution_set A b"
[PROOF STATE]
proof (state)
this:
x \<in> solution_set A b

goal (1 subgoal):
 1. \<And>x. x \<in> solution_set A b \<Longrightarrow> \<exists>b\<in>solution_set A 0. x = p + b
[PROOF STEP]
show "\<exists>b\<in>solution_set A 0. x = p + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<in>solution_set A 0. x = p + b
[PROOF STEP]
proof (rule bexI[of _ "x-p"], simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x - p \<in> solution_set A 0
[PROOF STEP]
have "A *v (x - p) = (A *v x) - (A *v p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v (x - p) = A *v x - A *v p
[PROOF STEP]
by (metis (no_types) add_diff_cancel diff_add_cancel matrix_vector_right_distrib)
[PROOF STATE]
proof (state)
this:
A *v (x - p) = A *v x - A *v p

goal (1 subgoal):
 1. x - p \<in> solution_set A 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A *v (x - p) = A *v x - A *v p

goal (1 subgoal):
 1. x - p \<in> solution_set A 0
[PROOF STEP]
have "... = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *v x - A *v p = 0
[PROOF STEP]
using x p
[PROOF STATE]
proof (prove)
using this:
x \<in> solution_set A b
is_solution p A b

goal (1 subgoal):
 1. A *v x - A *v p = 0
[PROOF STEP]
unfolding solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x. A *v x = b}
A *v p = b

goal (1 subgoal):
 1. A *v x - A *v p = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A *v x - A *v p = 0

goal (1 subgoal):
 1. x - p \<in> solution_set A 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A *v (x - p) = 0
[PROOF STEP]
show  "x - p \<in> solution_set A 0"
[PROOF STATE]
proof (prove)
using this:
A *v (x - p) = 0

goal (1 subgoal):
 1. x - p \<in> solution_set A 0
[PROOF STEP]
unfolding solution_set_def is_solution_def
[PROOF STATE]
proof (prove)
using this:
A *v (x - p) = 0

goal (1 subgoal):
 1. x - p \<in> {x. A *v x = 0}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x - p \<in> solution_set A 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b\<in>solution_set A 0. x = p + b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma independent_and_consistent_imp_uniqueness_solution:
fixes A::"'a::{field}^'n::{mod_type}^'rows::{mod_type}"
assumes dim_0: "vec.dim (solution_set A 0) = 0"
and con: "consistent A b"
shows "\<exists>!x. is_solution x A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. is_solution x A b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!x. is_solution x A b
[PROOF STEP]
obtain p where p: "is_solution p A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. is_solution p A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using con
[PROOF STATE]
proof (prove)
using this:
consistent A b

goal (1 subgoal):
 1. (\<And>p. is_solution p A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. is_solution x A b

goal (1 subgoal):
 1. (\<And>p. is_solution p A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_solution p A b

goal (1 subgoal):
 1. \<exists>!x. is_solution x A b
[PROOF STEP]
have solution_set_0: "solution_set A 0 = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A 0 = {0}
[PROOF STEP]
using vec.dim_zero_eq[OF dim_0] zero_is_solution_homogeneous_system
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 = {} \<or> solution_set A 0 = {0}
0 \<in> solution_set ?A 0

goal (1 subgoal):
 1. solution_set A 0 = {0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
solution_set A 0 = {0}

goal (1 subgoal):
 1. \<exists>!x. is_solution x A b
[PROOF STEP]
show "\<exists>!x. is_solution x A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. is_solution x A b
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. is_solution x A b
 2. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "\<exists>x. is_solution x A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. is_solution x A b
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
is_solution p A b

goal (1 subgoal):
 1. \<exists>x. is_solution x A b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. is_solution x A b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume x: "is_solution x A b" and y: "is_solution y A b"
[PROOF STATE]
proof (state)
this:
is_solution x A b
is_solution y A b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "solution_set A b = {p} + (solution_set A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A b = {p} + solution_set A 0
[PROOF STEP]
unfolding solution_set_rel[OF p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p} + solution_set A 0 = {p} + solution_set A 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
solution_set A b = {p} + solution_set A 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
solution_set A b = {p} + solution_set A 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "... = {p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p} + solution_set A 0 = {p}
[PROOF STEP]
unfolding solution_set_0 set_plus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {c. \<exists>a\<in>{p}. \<exists>b\<in>{0}. c = a + b} = {p}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{p} + solution_set A 0 = {p}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_solution x A b; is_solution y A b\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
solution_set A b = {p}
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
using this:
solution_set A b = {p}

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
solution_set A b = {p}
is_solution x A b
is_solution y A b

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding solution_set_def
[PROOF STATE]
proof (prove)
using this:
{x. is_solution x A b} = {p}
is_solution x A b
is_solution y A b

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis (full_types) mem_Collect_eq singleton_iff)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!x. is_solution x A b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card s = 1) = (\<exists>!x. x \<in> s)
[PROOF STEP]
unfolding One_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (card s = Suc 0) = (\<exists>!x. x \<in> s)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. card s = Suc 0 \<Longrightarrow> \<exists>!x. x \<in> s
 2. \<exists>!x. x \<in> s \<Longrightarrow> card s = Suc 0
[PROOF STEP]
apply(drule card_eq_SucD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
 2. \<exists>!x. x \<in> s \<Longrightarrow> card s = Suc 0
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>!x. x \<in> s \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
apply(erule ex1E)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> s; \<forall>y. y \<in> s \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> s; \<forall>y. y \<in> s \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> s; \<forall>y. y \<in> s \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
[PROOF STATE]
proof (state)
this:
x \<in> s
\<forall>y. y \<in> s \<longrightarrow> y = x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> s; \<forall>y. y \<in> s \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
have *:"s = insert x {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = {x}
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = {x}
[PROOF STEP]
apply(rule,rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> s \<Longrightarrow> xa \<in> {x}
 2. {x} \<subseteq> s
[PROOF STEP]
unfolding singleton_iff
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<in> s \<Longrightarrow> xa = x
 2. {x} \<subseteq> s
[PROOF STEP]
apply(rule as(2)[rule_format])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> s \<Longrightarrow> x \<in> s
 2. {x} \<subseteq> s
[PROOF STEP]
using as(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> s

goal (2 subgoals):
 1. \<And>x. x \<in> s \<Longrightarrow> x \<in> s
 2. {x} \<subseteq> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = {x}

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> s; \<forall>y. y \<in> s \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> card s = Suc 0
 2. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
show "card s = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card s = Suc 0
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {x} = Suc 0
[PROOF STEP]
using card.insert_remove
[PROOF STATE]
proof (prove)
using this:
finite ?A \<Longrightarrow> card (insert ?x ?A) = Suc (card (?A - {?x}))

goal (1 subgoal):
 1. card {x} = Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card s = Suc 0

goal (1 subgoal):
 1. \<exists>b B. s = insert b B \<and> b \<notin> B \<and> card B = 0 \<and> (0 = 0 \<longrightarrow> B = {}) \<Longrightarrow> \<exists>!x. x \<in> s
[PROOF STEP]
qed auto


[STATEMENT]
lemma uniqueness_solution_imp_independent:
fixes A::"'a::{field}^'n^'rows"
assumes ex1_sol: "\<exists>!x. is_solution x A b"
shows "vec.dim (solution_set A 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
obtain x where x: "is_solution x A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. is_solution x A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex1_sol
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. is_solution x A b

goal (1 subgoal):
 1. (\<And>x. is_solution x A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_solution x A b

goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
have solution_set_homogeneous_zero: "solution_set A 0 = {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A 0 = {0}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
assume not_zero_set: "solution_set A 0 \<noteq> {0}"
[PROOF STATE]
proof (state)
this:
solution_set A 0 \<noteq> {0}

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
have homogeneous_not_empty: "solution_set A 0 \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A 0 \<noteq> {}
[PROOF STEP]
by (metis empty_iff zero_is_solution_homogeneous_system)
[PROOF STATE]
proof (state)
this:
solution_set A 0 \<noteq> {}

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
obtain y where y: "y \<in> solution_set A 0" and y_not_0: "y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> solution_set A 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using not_zero_set homogeneous_not_empty
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 \<noteq> {0}
solution_set A 0 \<noteq> {}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> solution_set A 0; y \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> solution_set A 0
y \<noteq> 0

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
have "{x} = solution_set A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} = solution_set A b
[PROOF STEP]
unfolding solution_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} = {x. is_solution x A b}
[PROOF STEP]
using x ex1_sol
[PROOF STATE]
proof (prove)
using this:
is_solution x A b
\<exists>!x. is_solution x A b

goal (1 subgoal):
 1. {x} = {x. is_solution x A b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{x} = solution_set A b

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x} = solution_set A b

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
have "... = {x} + solution_set A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A b = {x} + solution_set A 0
[PROOF STEP]
unfolding solution_set_rel[OF x]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} + solution_set A 0 = {x} + solution_set A 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
solution_set A b = {x} + solution_set A 0

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0} \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{x} = {x} + solution_set A 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
{x} = {x} + solution_set A 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (opaque_lifting, mono_tags) add_left_cancel monoid_add_class.add.right_neutral empty_iff insert_iff set_plus_intro y y_not_0)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
solution_set A 0 = {0}

goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 = {0}

goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
using vec.dim_zero_eq'
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 = {0}
?A = {} \<or> ?A = {0} \<Longrightarrow> vec.dim ?A = 0

goal (1 subgoal):
 1. vec.dim (solution_set A 0) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vec.dim (solution_set A 0) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma consistent_homogeneous:
shows "consistent A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent A 0
[PROOF STEP]
unfolding consistent_def is_solution_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. A *v x = 0
[PROOF STEP]
using matrix_vector_mult_0_right
[PROOF STATE]
proof (prove)
using this:
?A *v 0 = 0

goal (1 subgoal):
 1. \<exists>x. A *v x = 0
[PROOF STEP]
by fast


[STATEMENT]
lemma dim_solution_set_0:
  fixes A::"'a::{field}^'n::{mod_type}^'rows::{mod_type}"
  shows "(vec.dim (solution_set A 0) = 0) = (solution_set A 0 = {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vec.dim (solution_set A 0) = 0) = (solution_set A 0 = {0})
[PROOF STEP]
using homogeneous_solution_set_subspace vec.dim_zero_subspace_eq
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set ?A 0)
vec.subspace ?A \<Longrightarrow> (vec.dim ?A = 0) = (?A = {0})

goal (1 subgoal):
 1. (vec.dim (solution_set A 0) = 0) = (solution_set A 0 = {0})
[PROOF STEP]
by auto


[STATEMENT]
lemma dim_solution_set_not_zero_imp_infinite_solutions_homogeneous:
fixes A::"'a::{field, semiring_char_0}^'n::{mod_type}^'rows::{mod_type}"
assumes dim_not_zero: "vec.dim (solution_set A 0) > 0"
shows "infinite (solution_set A 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
have "solution_set A 0 \<noteq> {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0}
[PROOF STEP]
using vec.dim_zero_subspace_eq[of "solution_set A 0"] dim_not_zero
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set A 0) \<Longrightarrow> (vec.dim (solution_set A 0) = 0) = (solution_set A 0 = {0})
0 < vec.dim (solution_set A 0)

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0}
[PROOF STEP]
by (metis less_numeral_extra(3) vec.dim_zero_eq')
[PROOF STATE]
proof (state)
this:
solution_set A 0 \<noteq> {0}

goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
solution_set A 0 \<noteq> {0}
[PROOF STEP]
obtain x where x: "x \<in> solution_set A 0" and x_not_0: "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 \<noteq> {0}

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> solution_set A 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vec.subspace_0[OF homogeneous_solution_set_subspace, of A]
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 \<noteq> {0}
0 \<in> solution_set A 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> solution_set A 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> solution_set A 0
x \<noteq> 0

goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
define f where "f = (\<lambda>n::nat. (of_nat n) *s x)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>n. of_nat n *s x)

goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (solution_set A 0)
[PROOF STEP]
proof (unfold infinite_iff_countable_subset, rule exI[of _ f], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj f
 2. range f \<subseteq> solution_set A 0
[PROOF STEP]
show "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. f x = f y \<longrightarrow> x = y
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa\<in>UNIV. \<forall>y\<in>UNIV. of_nat xa *s x = of_nat y *s x \<longrightarrow> xa = y
[PROOF STEP]
using x_not_0
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<forall>xa\<in>UNIV. \<forall>y\<in>UNIV. of_nat xa *s x = of_nat y *s x \<longrightarrow> xa = y
[PROOF STEP]
by (auto simp: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. range f \<subseteq> solution_set A 0
[PROOF STEP]
show "range f \<subseteq> solution_set A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> solution_set A 0
[PROOF STEP]
using homogeneous_solution_set_subspace
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set ?A 0)

goal (1 subgoal):
 1. range f \<subseteq> solution_set A 0
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set ?A 0)
x \<in> solution_set A 0

goal (1 subgoal):
 1. range f \<subseteq> solution_set A 0
[PROOF STEP]
unfolding vec.subspace_def image_def f_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> solution_set ?A 0 \<and> (\<forall>x\<in>solution_set ?A 0. \<forall>y\<in>solution_set ?A 0. x + y \<in> solution_set ?A 0) \<and> (\<forall>c. \<forall>x\<in>solution_set ?A 0. c *s x \<in> solution_set ?A 0)
x \<in> solution_set A 0

goal (1 subgoal):
 1. {y. \<exists>xa\<in>UNIV. y = of_nat xa *s x} \<subseteq> solution_set A 0
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
range f \<subseteq> solution_set A 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infinite (solution_set A 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_solutions_homogeneous_imp_dim_solution_set_not_zero:
  fixes A::"'a::{field}^'n::{mod_type}^'rows::{mod_type}"
  assumes i: "infinite (solution_set A 0)"
  shows "vec.dim (solution_set A 0) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < vec.dim (solution_set A 0)
[PROOF STEP]
by (metis dim_solution_set_0 finite.simps gr0I i)


[STATEMENT]
lemma infinite_solution_set_imp_consistent:
  "infinite (solution_set A b) \<Longrightarrow> consistent A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (solution_set A b) \<Longrightarrow> consistent A b
[PROOF STEP]
by (auto dest!: infinite_imp_nonempty simp: solution_set_def consistent_def)


[STATEMENT]
lemma dim_solution_set_not_zero_imp_infinite_solutions_no_homogeneous:
fixes A::"'a::{field, semiring_char_0}^'n::{mod_type}^'rows::{mod_type}"
assumes dim_not_0: "vec.dim (solution_set A 0) > 0"
and con: "consistent A b"
shows "infinite (solution_set A b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
have "solution_set A 0 \<noteq> {0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0}
[PROOF STEP]
using vec.dim_zero_subspace_eq[of "solution_set A 0"] dim_not_0
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set A 0) \<Longrightarrow> (vec.dim (solution_set A 0) = 0) = (solution_set A 0 = {0})
0 < vec.dim (solution_set A 0)

goal (1 subgoal):
 1. solution_set A 0 \<noteq> {0}
[PROOF STEP]
by (metis less_numeral_extra(3) vec.dim_zero_eq')
[PROOF STATE]
proof (state)
this:
solution_set A 0 \<noteq> {0}

goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
solution_set A 0 \<noteq> {0}
[PROOF STEP]
obtain x where x: "x \<in> solution_set A 0" and x_not_0: "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 \<noteq> {0}

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> solution_set A 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vec.subspace_0[OF homogeneous_solution_set_subspace, of A]
[PROOF STATE]
proof (prove)
using this:
solution_set A 0 \<noteq> {0}
0 \<in> solution_set A 0

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> solution_set A 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> solution_set A 0
x \<noteq> 0

goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
obtain y where y: "is_solution y A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. is_solution y A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using con
[PROOF STATE]
proof (prove)
using this:
consistent A b

goal (1 subgoal):
 1. (\<And>y. is_solution y A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. is_solution x A b

goal (1 subgoal):
 1. (\<And>y. is_solution y A b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_solution y A b

goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
define f where "f = (\<lambda>n::nat. y + (of_nat n) *s x)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>n. y + of_nat n *s x)

goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (solution_set A b)
[PROOF STEP]
proof (unfold infinite_iff_countable_subset, rule exI[of _ f], rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj f
 2. range f \<subseteq> solution_set A b
[PROOF STEP]
show "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. f x = f y \<longrightarrow> x = y
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa\<in>UNIV. \<forall>ya\<in>UNIV. y + of_nat xa *s x = y + of_nat ya *s x \<longrightarrow> xa = ya
[PROOF STEP]
using x_not_0
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<forall>xa\<in>UNIV. \<forall>ya\<in>UNIV. y + of_nat xa *s x = y + of_nat ya *s x \<longrightarrow> xa = ya
[PROOF STEP]
by (auto simp: vec_eq_iff)
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. range f \<subseteq> solution_set A b
[PROOF STEP]
show "range f \<subseteq> solution_set A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> solution_set A b
[PROOF STEP]
unfolding solution_set_rel[OF y]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> {y} + solution_set A 0
[PROOF STEP]
using homogeneous_solution_set_subspace
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set ?A 0)

goal (1 subgoal):
 1. range f \<subseteq> {y} + solution_set A 0
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
vec.subspace (solution_set ?A 0)
x \<in> solution_set A 0

goal (1 subgoal):
 1. range f \<subseteq> {y} + solution_set A 0
[PROOF STEP]
unfolding vec.subspace_def image_def f_def
[PROOF STATE]
proof (prove)
using this:
0 \<in> solution_set ?A 0 \<and> (\<forall>x\<in>solution_set ?A 0. \<forall>y\<in>solution_set ?A 0. x + y \<in> solution_set ?A 0) \<and> (\<forall>c. \<forall>x\<in>solution_set ?A 0. c *s x \<in> solution_set ?A 0)
x \<in> solution_set A 0

goal (1 subgoal):
 1. {ya. \<exists>xa\<in>UNIV. ya = y + of_nat xa *s x} \<subseteq> {y} + solution_set A 0
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
range f \<subseteq> solution_set A b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infinite (solution_set A b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_solutions_no_homogeneous_imp_dim_solution_set_not_zero_imp:
  fixes A::"'a::{field}^'n::{mod_type}^'rows::{mod_type}"
  assumes i: "infinite (solution_set A b)"
  shows "vec.dim (solution_set A 0) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < vec.dim (solution_set A 0)
[PROOF STEP]
using i independent_and_consistent_imp_card_1 infinite_solution_set_imp_consistent
[PROOF STATE]
proof (prove)
using this:
infinite (solution_set A b)
\<lbrakk>vec.dim (solution_set ?A 0) = 0; consistent ?A ?b\<rbrakk> \<Longrightarrow> card (solution_set ?A ?b) = 1
infinite (solution_set ?A ?b) \<Longrightarrow> consistent ?A ?b

goal (1 subgoal):
 1. 0 < vec.dim (solution_set A 0)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma solve_code[code]:
  shows "solve A b = (let GJ_P=Gauss_Jordan_PA A;
                        P_times_b=fst(GJ_P) *v b;
                        rank_A = (if A = 0 then 0 else to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1);
                        consistent_Ab = (rank_A \<ge> (if (\<exists>a. (P_times_b) $ a \<noteq> 0) then (to_nat (GREATEST a. (P_times_b) $ a \<noteq> 0) + 1) else 0));
                        GJ_transpose = Gauss_Jordan_PA (transpose A);
                        basis = {row i (fst GJ_transpose) | i. to_nat i \<ge> rank_A}
                        in (if consistent_Ab then Some (solve_consistent_rref (snd GJ_P) P_times_b,basis) else None))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve A b = (let GJ_P = Gauss_Jordan_PA A; P_times_b = fst GJ_P *v b; rank_A = if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd GJ_P) \<noteq> 0) + 1; consistent_Ab = (if \<exists>a. P_times_b $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. P_times_b $ a \<noteq> (0::'a)) + 1 else 0) \<le> rank_A; GJ_transpose = Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A); basis = {row i (fst GJ_transpose) |i. rank_A \<le> mod_type_class.to_nat i} in if consistent_Ab then Some (solve_consistent_rref (snd GJ_P) P_times_b, basis) else None)
[PROOF STEP]
unfolding Let_def solve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None) = (if (if \<exists>a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a) then mod_type_class.to_nat (GREATEST a. (fst (Gauss_Jordan_PA A) *v b) $ a \<noteq> (0::'a)) + 1 else 0) \<le> (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) then Some (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding consistent_eq_rank_ge_code[unfolded Let_def,symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None) = (if consistent A b then Some (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding basis_null_space_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), {row i (P_Gauss_Jordan (Finite_Cartesian_Product.transpose A)) |i. rank A \<le> mod_type_class.to_nat i}) else None) = (if consistent A b then Some (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding P_Gauss_Jordan_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. rank A \<le> mod_type_class.to_nat i}) else None) = (if consistent A b then Some (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (snd (Gauss_Jordan_PA A)) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding rank_Gauss_Jordan_code Let_def Gauss_Jordan_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None) = (if consistent A b then Some (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding solve_system_def Let_def fst_conv snd_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (snd (Gauss_Jordan_PA A)) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None) = (if consistent A b then Some (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
unfolding Gauss_Jordan_PA_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None) = (if consistent A b then Some (solve_consistent_rref (Gauss_Jordan A) (fst (Gauss_Jordan_PA A) *v b), {row i (fst (Gauss_Jordan_PA (Finite_Cartesian_Product.transpose A))) |i. (if A = 0 then 0 else mod_type_class.to_nat (GREATEST a. row a (Gauss_Jordan A) \<noteq> 0) + 1) \<le> mod_type_class.to_nat i}) else None)
[PROOF STEP]
..


[STATEMENT]
lemma consistent_imp_is_solution_solve:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes con: "consistent A b"
  shows "is_solution (fst (the (solve A b))) A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (fst (the (solve A b))) A b
[PROOF STEP]
unfolding solve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (fst (the (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None))) A b
[PROOF STEP]
unfolding if_P[OF con] fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (fst (the (Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A)))) A b
[PROOF STEP]
using consistent_imp_is_solution'[OF con]
[PROOF STATE]
proof (prove)
using this:
is_solution (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) A b

goal (1 subgoal):
 1. is_solution (fst (the (Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A)))) A b
[PROOF STEP]
by simp


[STATEMENT]
lemma inconsistent_imp_solve_eq_none:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes con: "inconsistent A b"
  shows "solve A b = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solve A b = None
[PROOF STEP]
unfolding solve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None) = None
[PROOF STEP]
unfolding if_not_P[OF con[unfolded inconsistent_def]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. None = None
[PROOF STEP]
..


[STATEMENT]
lemma solution_set_rel_solve:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes con: "consistent A b"
  shows "solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
have s: "is_solution (fst (the (solve A b))) A b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution (fst (the (solve A b))) A b
[PROOF STEP]
using consistent_imp_is_solution_solve[OF con]
[PROOF STATE]
proof (prove)
using this:
is_solution (fst (the (solve A b))) A b

goal (1 subgoal):
 1. is_solution (fst (the (solve A b))) A b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_solution (fst (the (solve A b))) A b

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
have "solution_set A b = {fst (the (solve A b))} + solution_set A 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + solution_set A 0
[PROOF STEP]
using solution_set_rel[OF s]
[PROOF STATE]
proof (prove)
using this:
solution_set A b = {fst (the (solve A b))} + solution_set A 0

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + solution_set A 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
solution_set A b = {fst (the (solve A b))} + solution_set A 0

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
solution_set A b = {fst (the (solve A b))} + solution_set A 0

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
have "... = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fst (the (solve A b))} + solution_set A 0 = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
unfolding set_plus_def solve_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {c. \<exists>a\<in>{fst (the (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None))}. \<exists>b\<in>solution_set A 0. c = a + b} = {c. \<exists>a\<in>{fst (the (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None))}. \<exists>b\<in>vec.span (snd (the (if consistent A b then Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A) else None))). c = a + b}
[PROOF STEP]
unfolding if_P[OF con] snd_conv fst_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {c. \<exists>a\<in>{fst (the (Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A)))}. \<exists>b\<in>solution_set A 0. c = a + b} = {c. \<exists>a\<in>{fst (the (Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A)))}. \<exists>b\<in>vec.span (snd (the (Some (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b)), basis_null_space A)))). c = a + b}
[PROOF STEP]
proof (safe, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. b \<in> solution_set A 0 \<Longrightarrow> b \<in> vec.span (basis_null_space A)
 2. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. b \<in> solution_set A 0 \<Longrightarrow> b \<in> vec.span (basis_null_space A)
 2. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
assume "b \<in> solution_set A 0"
[PROOF STATE]
proof (state)
this:
b \<in> solution_set A 0

goal (2 subgoals):
 1. \<And>b. b \<in> solution_set A 0 \<Longrightarrow> b \<in> vec.span (basis_null_space A)
 2. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
thus "b \<in> vec.span (basis_null_space A)"
[PROOF STATE]
proof (prove)
using this:
b \<in> solution_set A 0

goal (1 subgoal):
 1. b \<in> vec.span (basis_null_space A)
[PROOF STEP]
unfolding null_space_eq_solution_set[symmetric]
[PROOF STATE]
proof (prove)
using this:
b \<in> null_space A

goal (1 subgoal):
 1. b \<in> vec.span (basis_null_space A)
[PROOF STEP]
using basis_null_space[of A]
[PROOF STATE]
proof (prove)
using this:
b \<in> null_space A
vec.independent (basis_null_space A) \<and> null_space A = vec.span (basis_null_space A)

goal (1 subgoal):
 1. b \<in> vec.span (basis_null_space A)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
b \<in> vec.span (basis_null_space A)

goal (1 subgoal):
 1. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
assume b: "b \<in> vec.span (basis_null_space A)"
[PROOF STATE]
proof (state)
this:
b \<in> vec.span (basis_null_space A)

goal (1 subgoal):
 1. \<And>b. b \<in> vec.span (basis_null_space A) \<Longrightarrow> b \<in> solution_set A 0
[PROOF STEP]
thus "b \<in> solution_set A 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> vec.span (basis_null_space A)

goal (1 subgoal):
 1. b \<in> solution_set A 0
[PROOF STEP]
unfolding null_space_eq_solution_set[symmetric]
[PROOF STATE]
proof (prove)
using this:
b \<in> vec.span (basis_null_space A)

goal (1 subgoal):
 1. b \<in> null_space A
[PROOF STEP]
using basis_null_space
[PROOF STATE]
proof (prove)
using this:
b \<in> vec.span (basis_null_space A)
vec.independent (basis_null_space ?A) \<and> null_space ?A = vec.span (basis_null_space ?A)

goal (1 subgoal):
 1. b \<in> null_space A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> solution_set A 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{fst (the (solve A b))} + solution_set A 0 = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
show "solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))"
[PROOF STATE]
proof (prove)
using this:
solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))

goal (1 subgoal):
 1. solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_solution_eq_in_span_solve:
  fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
  assumes con: "consistent A b"
  shows "(is_solution x A b) = (x \<in> {fst (the (solve A b))} + vec.span (snd (the (solve A b))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_solution x A b = (x \<in> {fst (the (solve A b))} + vec.span (snd (the (solve A b))))
[PROOF STEP]
using solution_set_rel_solve[OF con]
[PROOF STATE]
proof (prove)
using this:
solution_set A b = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))

goal (1 subgoal):
 1. is_solution x A b = (x \<in> {fst (the (solve A b))} + vec.span (snd (the (solve A b))))
[PROOF STEP]
unfolding solution_set_def
[PROOF STATE]
proof (prove)
using this:
{x. is_solution x A b} = {fst (the (solve A b))} + vec.span (snd (the (solve A b)))

goal (1 subgoal):
 1. is_solution x A b = (x \<in> {fst (the (solve A b))} + vec.span (snd (the (solve A b))))
[PROOF STEP]
by auto


[STATEMENT]
lemma rp_resample:
  assumes "B \<subseteq> A \<union> C" "A \<inter> C = {}" "C \<subseteq> B" and finB: "finite B"
  shows "bind_spmf (spmf_of_set B) (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
proof(cases "C = {} \<or> A \<inter> B = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (C = {} \<or> A \<inter> B = {})

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
define A' where "A' \<equiv> A \<inter> B"
[PROOF STATE]
proof (state)
this:
A' \<equiv> A \<inter> B

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> (C = {} \<or> A \<inter> B = {})
[PROOF STEP]
have C: "C \<noteq> {}" and A': "A' \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (C = {} \<or> A \<inter> B = {})

goal (1 subgoal):
 1. C \<noteq> {} &&& A' \<noteq> {}
[PROOF STEP]
by(auto simp add: A'_def)
[PROOF STATE]
proof (state)
this:
C \<noteq> {}
A' \<noteq> {}

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
have B: "B = A' \<union> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = A' \<union> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A \<union> C
A \<inter> C = {}
C \<subseteq> B
finite B

goal (1 subgoal):
 1. B = A' \<union> C
[PROOF STEP]
by(auto simp add: A'_def)
[PROOF STATE]
proof (state)
this:
B = A' \<union> C

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
with finB
[PROOF STATE]
proof (chain)
picking this:
finite B
B = A' \<union> C
[PROOF STEP]
have finA: "finite A'" and finC: "finite C"
[PROOF STATE]
proof (prove)
using this:
finite B
B = A' \<union> C

goal (1 subgoal):
 1. finite A' &&& finite C
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
finite A'
finite C

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> A \<union> C
A \<inter> C = {}
C \<subseteq> B
finite B
[PROOF STEP]
have A'C: "A' \<inter> C = {}"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A \<union> C
A \<inter> C = {}
C \<subseteq> B
finite B

goal (1 subgoal):
 1. A' \<inter> C = {}
[PROOF STEP]
by(auto simp add: A'_def)
[PROOF STATE]
proof (state)
this:
A' \<inter> C = {}

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
have "bind_spmf (spmf_of_set B) (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) =
        bind_spmf (spmf_of_set B) (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)
[PROOF STEP]
by(rule bind_spmf_cong[OF refl])(simp add: set_spmf_of_set finB A'_def)
[PROOF STATE]
proof (state)
this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
have "\<dots> = spmf_of_set C" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
proof(rule spmf_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i
[PROOF STEP]
have "(\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicator C i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i
[PROOF STEP]
using finA finC
[PROOF STATE]
proof (prove)
using this:
finite A'
finite C

goal (1 subgoal):
 1. (\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i
[PROOF STEP]
by(simp add: disjoint_notin1[OF A'C] indicator_single_Some sum_mult_indicator[of C "\<lambda>_. 1 :: real" "\<lambda>_. _" "\<lambda>x. x", simplified] split: split_indicator cong: conj_cong sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i

goal (1 subgoal):
 1. \<And>i. spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i
[PROOF STEP]
show "spmf ?lhs i = spmf ?rhs i"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i

goal (1 subgoal):
 1. spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i
[PROOF STEP]
using B finA finC A'C C A'
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>C. spmf (if x \<in> A' then spmf_of_set C else return_spmf x) i) = indicat_real C i
B = A' \<union> C
finite A'
finite C
A' \<inter> C = {}
C \<noteq> {}
A' \<noteq> {}

goal (1 subgoal):
 1. spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i
[PROOF STEP]
by(simp add: spmf_bind integral_spmf_of_set sum_Un spmf_of_set field_simps)(simp add: field_simps card_Un_disjoint)
[PROOF STATE]
proof (state)
this:
spmf (spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x)) i = spmf (spmf_of_set C) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A' then spmf_of_set C else return_spmf x) = spmf_of_set C

goal (2 subgoals):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
 2. \<not> (C = {} \<or> A \<inter> B = {}) \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C

goal (1 subgoal):
 1. spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C

goal (1 subgoal):
 1. C = {} \<or> A \<inter> B = {} \<Longrightarrow> spmf_of_set B \<bind> (\<lambda>x. if x \<in> A then spmf_of_set C else return_spmf x) = spmf_of_set C
[PROOF STEP]
qed(use assms in \<open>auto 4 3 cong: bind_spmf_cong_simp simp add: subsetD bind_spmf_const spmf_of_set_empty disjoint_notin1 intro!: arg_cong[where f=spmf_of_set]\<close>)


[STATEMENT]
lemma advantage_nonneg: "0 \<le> advantage \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> advantage \<A>
[PROOF STEP]
by(simp add: advantage_def)


[STATEMENT]
lemma advantage_le_1: "advantage \<A> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. advantage \<A> \<le> 1
[PROOF STEP]
by(auto simp add: advantage_def intro!: abs_leI)(metis diff_0_right diff_left_mono order_trans pmf_le_1 pmf_nonneg) +


[STATEMENT]
lemma outs_\<I>_\<I> [simp]: "outs_\<I> \<I> = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. outs_\<I> \<I> = A
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma responses_\<I>_\<I> [simp]: "responses_\<I> \<I> x = (if x \<in> A then A else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. responses_\<I> \<I> x = (if x \<in> A then A else {})
[PROOF STEP]
by transfer simp