header{*Solving systems of equations using the Gauss Jordan algorithm*}
theory System_Of_Equations
imports
Gauss_Jordan_PA
Bases_Of_Fundamental_Subspaces
begin
subsection{*Definitions*}
text{*Given a system of equations @{term "A *v x = b"}, the following function returns the pair @{term "(P ** A,P *v b)"}, where P is the matrix
which states @{term "Gauss_Jordan A = P ** A"}. That matrix is computed by means of @{term "Gauss_Jordan_PA"}.*}
definition solve_system :: "('a::{field}^'cols::{mod_type}^'rows::{mod_type}) => ('a^'rows::{mod_type})
=> (('a^'cols::{mod_type}^'rows::{mod_type}) × ('a^'rows::{mod_type}))"
where "solve_system A b = (let A' = Gauss_Jordan_PA A in (snd A', (fst A') *v b))"
definition "is_solution x A b = (A *v x = b)"
subsection{*Relationship between @{term "is_solution_def"} and @{term "solve_system_def"}*}
lemma is_solution_imp_solve_system:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes xAb:"is_solution x A b"
shows "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
proof -
have "(fst (Gauss_Jordan_PA A)*v(A *v x) = fst (Gauss_Jordan_PA A) *v b)"
using xAb unfolding is_solution_def by fast
hence "(snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b)"
unfolding matrix_vector_mul_assoc
unfolding fst_Gauss_Jordan_PA[of A] .
thus "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
unfolding is_solution_def solve_system_def Let_def by simp
qed
lemma solve_system_imp_is_solution:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
assumes xAb: "is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
shows "is_solution x A b"
proof -
have "fst (solve_system A b) *v x = snd (solve_system A b)" using xAb unfolding is_solution_def .
hence "snd (Gauss_Jordan_PA A) *v x = fst (Gauss_Jordan_PA A) *v b" unfolding solve_system_def Let_def fst_conv snd_conv .
hence "(fst (Gauss_Jordan_PA A) ** A) *v x = fst (Gauss_Jordan_PA A) *v b" unfolding fst_Gauss_Jordan_PA .
hence "fst (Gauss_Jordan_PA A) *v (A *v x) = fst (Gauss_Jordan_PA A) *v b" unfolding matrix_vector_mul_assoc .
hence "matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v (A *v x)) = matrix_inv (fst (Gauss_Jordan_PA A)) *v (fst (Gauss_Jordan_PA A) *v b)" by simp
hence "(A *v x) = b"
unfolding matrix_vector_mul_assoc[of "matrix_inv (fst (Gauss_Jordan_PA A))"]
unfolding matrix_inv_left[OF invertible_fst_Gauss_Jordan_PA]
unfolding matrix_vector_mul_lid .
thus ?thesis unfolding is_solution_def .
qed
lemma is_solution_solve_system:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "is_solution x A b = is_solution x (fst (solve_system A b)) (snd (solve_system A b))"
using solve_system_imp_is_solution is_solution_imp_solve_system by blast
subsection{*Consistent and inconsistent systems of equations*}
definition consistent :: "real^'cols::{mod_type}^'rows::{mod_type} => real^'rows::{mod_type} => bool"
where "consistent A b = (∃x. is_solution x A b)"
definition "inconsistent A b = (¬ (consistent A b))"
lemma inconsistent: "inconsistent A b = (¬ (∃x. is_solution x A b))"
unfolding inconsistent_def consistent_def by simp
text{*The following function will be use to solve consistent systems which are already in the reduced row echelon form.*}
definition solve_consistent_rref :: "real^'cols::{mod_type}^'rows::{mod_type} => real^'rows::{mod_type} => real^'cols::{mod_type}"
where "solve_consistent_rref A b = (χ j. if (∃i. A $ i $ j = 1 ∧ j=(LEAST n. A $ i $ n ≠ 0)) then b $ (THE i. A $ i $ j = 1) else 0)"
lemma solve_consistent_rref_code[code abstract]:
shows "vec_nth (solve_consistent_rref A b) = (% j. if (∃i. A $ i $ j = 1 ∧ j=(LEAST n. A $ i $ n ≠ 0)) then b $ (THE i. A $ i $ j = 1) else 0)"
unfolding solve_consistent_rref_def by auto
lemma rank_ge_imp_is_solution:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes con: "rank A ≥ (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0)
then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0)"
shows "is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b"
proof -
have "is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) (Gauss_Jordan A) (P_Gauss_Jordan A *v b)"
proof (unfold is_solution_def solve_consistent_rref_def, subst matrix_vector_mult_def, vector, auto)
fix a
let ?f="λj. Gauss_Jordan A $ a $ j *
(if ∃i. Gauss_Jordan A $ i $ j = 1 ∧ j = (LEAST n. Gauss_Jordan A $ i $ n ≠ 0) then (P_Gauss_Jordan A *v b) $ (THE i. Gauss_Jordan A $ i $ j = 1) else 0)"
show "setsum ?f UNIV = (P_Gauss_Jordan A *v b) $ a"
proof (cases "A=0")
case True
hence rank_A_eq_0:"rank A = 0" using rank_0 by simp
have "(P_Gauss_Jordan A *v b) = 0"
proof (rule ccontr)
assume not_zero: "P_Gauss_Jordan A *v b ≠ 0"
hence ex_a: "∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0" by (metis vec_eq_iff zero_index)
show False using con unfolding if_P[OF ex_a] unfolding rank_A_eq_0 by auto
qed
thus ?thesis unfolding A_0_imp_Gauss_Jordan_0[OF True] by force
next
case False note A_not_zero=False
def not_zero_positions_row_a≡"{j. Gauss_Jordan A $ a $ j ≠ 0}"
def zero_positions_row_a≡"{j. Gauss_Jordan A $ a $ j = 0}"
have UNIV_rw: "UNIV = not_zero_positions_row_a ∪ zero_positions_row_a" unfolding zero_positions_row_a_def not_zero_positions_row_a_def by auto
have disj: "not_zero_positions_row_a ∩ zero_positions_row_a = {}" unfolding zero_positions_row_a_def not_zero_positions_row_a_def by fastforce
have setsum_zero: "(setsum ?f zero_positions_row_a) = 0" by (unfold zero_positions_row_a_def, rule setsum_0', fastforce)
have "setsum ?f (UNIV::'cols set)=setsum ?f (not_zero_positions_row_a ∪ zero_positions_row_a)" unfolding UNIV_rw ..
also have "... = setsum ?f (not_zero_positions_row_a) + (setsum ?f zero_positions_row_a)" by (rule setsum.union_disjoint[OF _ _ disj], simp+)
also have "... = setsum ?f (not_zero_positions_row_a)" unfolding setsum_zero by simp
also have "... = (P_Gauss_Jordan A *v b) $ a"
proof (cases "not_zero_positions_row_a = {}")
case True note zero_row_a=True
show ?thesis
proof (cases "∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0")
case False hence "(P_Gauss_Jordan A *v b) $ a = 0" by simp
thus ?thesis unfolding True by auto
next
case True
have rank_not_0: "rank A ≠ 0" by (metis A_not_zero less_not_refl3 rank_Gauss_Jordan rank_greater_zero)
have greatest_less_a: "(GREATEST' a. ¬ is_zero_row a (Gauss_Jordan A)) < a"
proof (unfold is_zero_row_def, rule greatest_less_zero_row)
show " reduced_row_echelon_form_upt_k (Gauss_Jordan A) (ncols (Gauss_Jordan A))" using rref_Gauss_Jordan unfolding reduced_row_echelon_form_def .
show "is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A)"
unfolding is_zero_row_def[symmetric] by (metis (mono_tags) zero_row_a emptyE is_zero_row_def' mem_Collect_eq not_zero_positions_row_a_def)
show "¬ (∀a. is_zero_row_upt_k a (ncols (Gauss_Jordan A)) (Gauss_Jordan A))"
unfolding is_zero_row_def[symmetric] using A_not_zero
by (metis Gauss_Jordan_not_0 is_zero_row_def' vec_eq_iff zero_index)
qed
hence "to_nat (GREATEST' a. ¬ is_zero_row a (Gauss_Jordan A)) < to_nat a" using to_nat_mono by fast
hence rank_le_to_nat_a: "rank A ≤ to_nat a" unfolding rank_eq_suc_to_nat_greatest[OF A_not_zero] by simp
have "to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) < to_nat a" using con unfolding consistent_def unfolding if_P[OF True] using rank_le_to_nat_a by simp
hence "(GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) < a" by (metis not_le to_nat_mono')
hence "(P_Gauss_Jordan A *v b) $ a = 0" using not_greater_Greatest' by blast
thus ?thesis unfolding zero_row_a by simp
qed
next
case False note not_empty=False
have not_zero_positions_row_a_rw: "not_zero_positions_row_a = {LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0} ∪ (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0})"
unfolding not_zero_positions_row_a_def
by (metis (mono_tags) Collect_cong False LeastI_ex bot_set_def empty_iff insert_Diff_single insert_absorb insert_is_Un mem_Collect_eq not_zero_positions_row_a_def)
have setsum_zero': "setsum ?f (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0}) = 0"
by (rule setsum_0', auto, metis is_zero_row_def' rref_Gauss_Jordan rref_condition4_explicit zero_neq_one)
have "setsum ?f (not_zero_positions_row_a) = setsum ?f {LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0} + setsum ?f (not_zero_positions_row_a - {LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0})"
by (subst not_zero_positions_row_a_rw, rule setsum.union_disjoint[OF _ _ _], simp+)
also have "... = ?f (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0)" using setsum_zero' by force
also have "... = (P_Gauss_Jordan A *v b) $ a"
proof (cases "∃i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = 1 ∧ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = (LEAST n. (Gauss_Jordan A) $ i $ n ≠ 0)")
case True
have A_least_eq_1: "(Gauss_Jordan A) $ a $ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = 1"
by (metis (mono_tags) empty_Collect_eq is_zero_row_def' not_empty not_zero_positions_row_a_def rref_Gauss_Jordan rref_condition2_explicit)
moreover have "(THE i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = 1) = a"
proof (rule the_equality)
show "(Gauss_Jordan A) $ a $ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = 1" using A_least_eq_1 .
show "!!i. (Gauss_Jordan A) $ i $ (LEAST j. (Gauss_Jordan A) $ a $ j ≠ 0) = 1 ==> i = a"
by (metis calculation is_zero_row_def' rref_Gauss_Jordan rref_condition4_explicit zero_neq_one)
qed
ultimately show ?thesis unfolding if_P[OF True] by simp
next
case False
have "is_zero_row a (Gauss_Jordan A)" using False rref_Gauss_Jordan rref_condition2 by blast
hence "(P_Gauss_Jordan A *v b) $ a = 0"
by (metis (mono_tags) IntI disj empty_iff insert_compr insert_is_Un is_zero_row_def' mem_Collect_eq not_zero_positions_row_a_rw zero_positions_row_a_def)
thus ?thesis unfolding if_not_P[OF False] by fastforce
qed
finally show ?thesis .
qed
finally show "setsum ?f UNIV = (P_Gauss_Jordan A *v b) $ a" .
qed
qed
thus ?thesis apply (subst is_solution_solve_system)
unfolding solve_system_def Let_def snd_conv fst_conv unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def .
qed
corollary rank_ge_imp_consistent:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes "rank A ≥ (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0) then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0)"
shows "consistent A b"
using rank_ge_imp_is_solution assms unfolding consistent_def by auto
lemma inconsistent_imp_rank_less:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes inc: "inconsistent A b"
shows "rank A < (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0) then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0)"
proof (rule ccontr)
assume "¬ rank A < (if ∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0 then to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1 else 0)"
hence "(if ∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0 then to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1 else 0) ≤ rank A" by simp
hence "consistent A b" using rank_ge_imp_consistent by auto
thus False using inc unfolding inconsistent_def by contradiction
qed
lemma rank_less_imp_inconsistent:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes inc: "rank A < (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0) then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0)"
shows "inconsistent A b"
proof (rule ccontr)
def i≡"(GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0)"
def j≡"(GREATEST' a. ¬ is_zero_row a (Gauss_Jordan A))"
assume "¬ inconsistent A b"
hence ex_solution: "∃x. is_solution x A b" unfolding inconsistent_def consistent_def by auto
from this obtain x where "is_solution x A b" by auto
hence is_solution_solve: "is_solution x (Gauss_Jordan A) (P_Gauss_Jordan A *v b)"
using is_solution_solve_system
by (metis Gauss_Jordan_PA_eq P_Gauss_Jordan_def fst_conv snd_conv solve_system_def)
show False
proof (cases "A=0")
case True
hence rank_eq_0: "rank A = 0" using rank_0 by simp
hence exists_not_0:"(∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0)"
using inc unfolding inconsistent
using to_nat_plus_1_set[of "(GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0)"]
by presburger
show False
by (metis True exists_not_0 ex_solution is_solution_def matrix_vector_zero norm_equivalence transpose_vector vector_matrix_zero' zero_index)
next
case False
have j_less_i: "j<i"
proof -
have rank_less_greatest_i: "rank A < to_nat i + 1"
using inc unfolding i_def inconsistent by presburger
moreover have rank_eq_greatest_A: "rank A = to_nat j + 1" unfolding j_def by (rule rank_eq_suc_to_nat_greatest[OF False])
ultimately have "to_nat j + 1 < to_nat i + 1" by simp
hence "to_nat j < to_nat i" by auto
thus "j<i" by (metis (full_types) not_le to_nat_mono')
qed
have is_zero_i: "is_zero_row i (Gauss_Jordan A)" by (metis (full_types) j_def j_less_i not_greater_Greatest')
have "(Gauss_Jordan A *v x) $ i = 0"
proof (unfold matrix_vector_mult_def, auto, rule setsum_0',clarify)
fix a::'cols
show "Gauss_Jordan A $ i $ a * x $ a = 0" using is_zero_i unfolding is_zero_row_def' by simp
qed
moreover have "(Gauss_Jordan A *v x) $ i ≠ 0"
proof -
have "Gauss_Jordan A *v x = P_Gauss_Jordan A *v b" using is_solution_def is_solution_solve by blast
also have "... $ i ≠ 0"
unfolding i_def
proof (rule Greatest'I_ex)
show "∃x. (P_Gauss_Jordan A *v b) $ x ≠ 0" using inc unfolding i_def inconsistent by presburger
qed
finally show ?thesis .
qed
ultimately show "False" by contradiction
qed
qed
corollary consistent_imp_rank_ge:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes "consistent A b"
shows "rank A ≥ (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0) then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0)"
using rank_less_imp_inconsistent by (metis assms inconsistent_def not_less)
lemma inconsistent_eq_rank_less:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
shows "inconsistent A b = (rank A < (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0)
then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0))"
using inconsistent_imp_rank_less rank_less_imp_inconsistent by blast
lemma consistent_eq_rank_ge:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
shows "consistent A b = (rank A ≥ (if (∃a. (P_Gauss_Jordan A *v b) $ a ≠ 0)
then (to_nat (GREATEST' a. (P_Gauss_Jordan A *v b) $ a ≠ 0) + 1) else 0))"
using consistent_imp_rank_ge rank_ge_imp_consistent by blast
corollary consistent_imp_is_solution:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes "consistent A b"
shows "is_solution (solve_consistent_rref (Gauss_Jordan A) (P_Gauss_Jordan A *v b)) A b"
by (rule rank_ge_imp_is_solution[OF assms[unfolded consistent_eq_rank_ge]])
corollary consistent_imp_is_solution':
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes "consistent A b"
shows "is_solution (solve_consistent_rref (fst (solve_system A b)) (snd (solve_system A b))) A b"
using consistent_imp_is_solution[OF assms] unfolding solve_system_def Let_def snd_conv fst_conv
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def .
text{*Code equations optimized using Lets*}
lemma inconsistent_eq_rank_less_code[code]:
fixes A::"real^'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) ≠ 0) + 1) in (rank_A < (if (∃a. P_mult_b $ a ≠ 0)
then (to_nat (GREATEST' a. P_mult_b $ a ≠ 0) + 1) else 0)))"
unfolding inconsistent_eq_rank_less Let_def rank_Gauss_Jordan_code
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def ..
lemma consistent_eq_rank_ge_code[code]:
fixes A::"real^'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) ≠ 0) + 1) in (rank_A ≥ (if (∃a. P_mult_b $ a ≠ 0)
then (to_nat (GREATEST' a. P_mult_b $ a ≠ 0) + 1) else 0)))"
unfolding consistent_eq_rank_ge Let_def rank_Gauss_Jordan_code
unfolding Gauss_Jordan_PA_eq P_Gauss_Jordan_def ..
subsection{*Solution set of a system of equations. Dependent and independent systems.*}
definition "solution_set A b = {x. is_solution x A b}"
lemma null_space_eq_solution_set:
shows "null_space A = solution_set A 0" unfolding null_space_def solution_set_def is_solution_def ..
corollary dim_solution_set_homogeneous_eq_dim_null_space[code_unfold]:
shows "dim (solution_set A 0) = dim (null_space A)" using null_space_eq_solution_set[of A] by simp
lemma zero_is_solution_homogeneous_system:
shows "0 ∈ (solution_set A 0)"
unfolding solution_set_def is_solution_def
using matrix_vector_zero by fast
lemma homogeneous_solution_set_subspace:
fixes A::"'a::{real_algebra,semiring_1}^'n^'rows"
shows "subspace (solution_set A 0)"
using subspace_null_space[of A] unfolding null_space_eq_solution_set .
lemma solution_set_rel:
fixes A::"'a::{real_vector, semiring_1}^'n^'rows"
assumes p: "is_solution p A b"
shows "solution_set A b = {p} + (solution_set A 0)"
proof (unfold set_plus_def, auto)
fix ba
assume ba: "ba ∈ solution_set A 0"
have "A *v (p + ba) = (A *v p) + (A *v ba)" unfolding matrix_vector_right_distrib ..
also have "... = b" using p ba unfolding solution_set_def is_solution_def by simp
finally show "p + ba ∈ solution_set A b" unfolding solution_set_def is_solution_def by simp
next
fix x
assume x: "x ∈ solution_set A b"
show "∃b∈solution_set A 0. x = p + b"
proof (rule bexI[of _ "x-p"], simp)
have "A *v (x - p) = (A *v x) - (A *v p)" by (metis (no_types) add_diff_cancel diff_add_cancel matrix_vector_right_distrib)
also have "... = 0" using x p unfolding solution_set_def is_solution_def by simp
finally show "x - p ∈ solution_set A 0" unfolding solution_set_def is_solution_def by simp
qed
qed
lemma independent_and_consistent_imp_uniqueness_solution:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes dim_0: "dim (solution_set A 0) = 0"
and con: "consistent A b"
shows "∃!x. is_solution x A b"
proof -
obtain p where p: "is_solution p A b" using con unfolding consistent_def by blast
have solution_set_0: "solution_set A 0 = {0}"
using dim_zero_eq[OF dim_0] zero_is_solution_homogeneous_system by blast
show "∃!x. is_solution x A b"
proof (rule ex_ex1I)
show "∃x. is_solution x A b" using p by auto
fix x y assume x: "is_solution x A b" and y: "is_solution y A b"
have "solution_set A b = {p} + (solution_set A 0)" unfolding solution_set_rel[OF p] ..
also have "... = {p}" unfolding solution_set_0 set_plus_def by force
finally show "x = y" using x y unfolding solution_set_def by (metis (full_types) mem_Collect_eq singleton_iff)
qed
qed
corollary independent_and_consistent_imp_card_1:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes dim_0: "dim (solution_set A 0) = 0"
and con: "consistent A b"
shows "card (solution_set A b) = 1"
using independent_and_consistent_imp_uniqueness_solution[OF assms] unfolding solution_set_def using card_1_exists by auto
lemma uniqueness_solution_imp_independent:
fixes A::"'a::{euclidean_space, semiring_1}^'n^'rows"
assumes ex1_sol: "∃!x. is_solution x A b"
shows "dim (solution_set A 0) = 0"
proof -
obtain x where x: "is_solution x A b" using ex1_sol by blast
have solution_set_homogeneous_zero: "solution_set A 0 = {0}"
proof (rule ccontr)
assume not_zero_set: "solution_set A 0 ≠ {0}"
have homogeneous_not_empty: "solution_set A 0 ≠ {}" by (metis empty_iff zero_is_solution_homogeneous_system)
obtain y where y: "y ∈ solution_set A 0" and y_not_0: "y ≠ 0" using not_zero_set homogeneous_not_empty by blast
have "{x} = solution_set A b" unfolding solution_set_def using x ex1_sol by blast
also have "... = {x} + solution_set A 0" unfolding solution_set_rel[OF x] ..
finally show False
by (metis (hide_lams, mono_tags) add_left_cancel comm_monoid_add_class.add.right_neutral empty_iff insert_iff set_plus_intro y y_not_0)
qed
thus ?thesis using dim_zero_eq' by blast
qed
corollary uniqueness_solution_eq_independent_and_consistent:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "(∃!x. is_solution x A b) = (consistent A b ∧ dim (solution_set A 0) = 0)"
using independent_and_consistent_imp_uniqueness_solution uniqueness_solution_imp_independent consistent_def
by metis
lemma consistent_homogeneous:
shows "consistent A 0" unfolding consistent_def is_solution_def using matrix_vector_zero by fast
lemma dim_solution_set_0:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "(dim (solution_set A 0) = 0) = (solution_set A 0 = {0})"
proof (auto)
show "dim {0::real^'n::{mod_type}} = 0" using dim_zero_eq'[of "{0::real^'n::{mod_type}}"] by fast
fix x assume dim0: "dim (solution_set A 0) = 0"
show "0 ∈ solution_set A 0" using zero_is_solution_homogeneous_system .
assume x: "x ∈ solution_set A 0"
show "x = 0"
using independent_and_consistent_imp_uniqueness_solution[OF dim0 consistent_homogeneous] zero_is_solution_homogeneous_system x unfolding solution_set_def by blast
qed
lemma dim_solution_set_not_zero_imp_infinite_solutions_homogeneous:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes dim_not_zero: "dim (solution_set A 0) > 0"
shows "infinite (solution_set A 0)"
proof -
have "solution_set A 0 ≠ {0}" using dim_zero_subspace_eq[of "solution_set A 0"] dim_not_zero by (metis less_numeral_extra(3) subspace_trivial)
from this obtain x where x: "x ∈ solution_set A 0" and x_not_0: "x ≠ 0" using subspace_0[OF homogeneous_solution_set_subspace, of A] by auto
def f≡"λn::nat. n *⇩R x"
show ?thesis
proof (unfold infinite_iff_countable_subset, rule exI[of _ f], rule conjI)
show "inj f" unfolding inj_on_def unfolding f_def using x_not_0 by force
show "range f ⊆ solution_set A 0" using homogeneous_solution_set_subspace using x unfolding subspace_def image_def f_def by fast
qed
qed
lemma infinite_solutions_homogeneous_imp_dim_solution_set_not_zero:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes i: "infinite (solution_set A 0)"
shows "dim (solution_set A 0) > 0"
proof (rule ccontr, simp)
assume "dim (solution_set A 0) = 0"
hence "solution_set A 0 = {0}" using dim_solution_set_0 by auto
hence "finite (solution_set A 0)" by simp
thus False using i by contradiction
qed
corollary infinite_solution_set_homogeneous_eq:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "infinite (solution_set A 0) = (dim (solution_set A 0) > 0)"
using infinite_solutions_homogeneous_imp_dim_solution_set_not_zero
using dim_solution_set_not_zero_imp_infinite_solutions_homogeneous by metis
corollary infinite_solution_set_homogeneous_eq':
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "(∃⇩∞x. is_solution x A 0) = (dim (solution_set A 0) > 0)"
unfolding infinite_solution_set_homogeneous_eq[symmetric] INFM_iff_infinite unfolding solution_set_def ..
lemma infinite_solution_set_imp_consistent:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes i: "infinite (solution_set A b)"
shows "consistent A b"
proof -
have "(∃⇩∞x. is_solution x A b)" using i unfolding solution_set_def INFM_iff_infinite .
thus ?thesis unfolding consistent_def by (metis (full_types) INFM_MOST_simps(1) INFM_mono)
qed
lemma dim_solution_set_not_zero_imp_infinite_solutions_no_homogeneous:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes dim_not_0: "dim (solution_set A 0) > 0"
and con: "consistent A b"
shows "infinite (solution_set A b)"
proof -
have "solution_set A 0 ≠ {0}" using dim_zero_subspace_eq[of "solution_set A 0"] dim_not_0 by (metis less_numeral_extra(3) subspace_trivial)
from this obtain x where x: "x ∈ solution_set A 0" and x_not_0: "x ≠ 0" using subspace_0[OF homogeneous_solution_set_subspace, of A] by auto
obtain y where y: "is_solution y A b" using con unfolding consistent_def by blast
def f≡"λn::nat. y + n *⇩R x"
show ?thesis
proof (unfold infinite_iff_countable_subset, rule exI[of _ f], rule conjI)
show "inj f" unfolding inj_on_def unfolding f_def using x_not_0 by force
show "range f ⊆ solution_set A b"
unfolding solution_set_rel[OF y]
using homogeneous_solution_set_subspace using x unfolding subspace_def image_def f_def by fast
qed
qed
lemma infinite_solutions_no_homogeneous_imp_dim_solution_set_not_zero_imp:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
assumes i: "infinite (solution_set A b)"
shows "dim (solution_set A 0) > 0"
proof (rule ccontr, simp)
have "(∃⇩∞x. is_solution x A b)" using i unfolding solution_set_def INFM_iff_infinite .
from this obtain x where x: "is_solution x A b" by (metis (full_types) INFM_MOST_simps(1) INFM_mono)
assume "dim (solution_set A 0) = 0"
hence "solution_set A 0 = {0}" using dim_solution_set_0 by auto
hence "solution_set A b = {x} + {0}" unfolding solution_set_rel[OF x] by simp
also have "... = {x}" unfolding set_plus_def by force
finally show False using i by simp
qed
corollary infinite_solution_set_no_homogeneous_eq:
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "infinite (solution_set A b) = (consistent A b ∧ dim (solution_set A 0) > 0)"
using dim_solution_set_not_zero_imp_infinite_solutions_no_homogeneous
using infinite_solutions_no_homogeneous_imp_dim_solution_set_not_zero_imp
using infinite_solution_set_imp_consistent by blast
corollary infinite_solution_set_no_homogeneous_eq':
fixes A::"real^'n::{mod_type}^'rows::{mod_type}"
shows "(∃⇩∞x. is_solution x A b) = (consistent A b ∧ dim (solution_set A 0) > 0)"
unfolding infinite_solution_set_no_homogeneous_eq[symmetric] INFM_iff_infinite unfolding solution_set_def ..
definition "independent_and_consistent A b = (consistent A b ∧ dim (solution_set A 0) = 0)"
definition "dependent_and_consistent A b = (consistent A b ∧ dim (solution_set A 0) > 0)"
subsection{*Solving systems of linear equations*}
text{*The following function will solve any system of linear equations. Given a matrix @{text "A"} and a vector @{text "b"},
Firstly it makes use of the funcion @{term "solve_system"} to transform the original matrix @{text "A"} and the vector @{text "b"}
into another ones in reduced row echelon form. Then, that system will have the same solution than the original one but it is easier to be solved.
So we make use of the function @{term "solve_consistent_rref"} to obtain one solution of the system.
We will prove that any solution of the system can be rewritten as a linear combination of elements of a basis of the null space plus a particular solution of the system.
So the function @{term "solve"} will return an option type, depending on the consistency of the system:
\begin{itemize}
\item If the system is consistent (so there exists at least one solution), the function will return the @{text "Some"} of a pair.
In the first component of that pair will be one solution of the system and the second one will be a basis of the null space of the matrix. Hence:
\begin{enumerate}
\item If the system is consistent and independent (so there exists one and only one solution), the pair will consist of the solution and the empty set (this empty set is
the basis of the null space).
\item If the system is consistent and dependent (so there exists an infinite number of solutions),
the pair will consist of one particular solution and a basis of the null space (which will not be the empty set).
\end{enumerate}
\item If the system is inconsistent (so there exists no solution), the function will return @{text "None"}.
\end{itemize}
*}
definition "solve A b = (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)"
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) ≠ 0) + 1);
consistent_Ab = (rank_A ≥ (if (∃a. (P_times_b) $ a ≠ 0) then (to_nat (GREATEST' a. (P_times_b) $ a ≠ 0) + 1) else 0));
GJ_transpose = Gauss_Jordan_PA (transpose A);
basis = {row i (fst GJ_transpose) | i. to_nat i ≥ rank_A}
in (if consistent_Ab then Some (solve_consistent_rref (snd GJ_P) P_times_b,basis) else None))"
unfolding Let_def solve_def
unfolding consistent_eq_rank_ge_code[unfolded Let_def,symmetric]
unfolding basis_null_space_def Let_def
unfolding P_Gauss_Jordan_def
unfolding rank_Gauss_Jordan_code Let_def Gauss_Jordan_PA_eq
unfolding solve_system_def Let_def fst_conv snd_conv
unfolding Gauss_Jordan_PA_eq ..
lemma consistent_imp_is_solution_solve:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes con: "consistent A b"
shows "is_solution (fst (the (solve A b))) A b"
unfolding solve_def unfolding if_P[OF con] the.simps fst_conv using consistent_imp_is_solution'[OF con] .
corollary consistent_eq_solution_solve:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
shows "consistent A b = is_solution (fst (the (solve A b))) A b"
by (metis consistent_def consistent_imp_is_solution_solve)
lemma inconsistent_imp_solve_eq_none:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes con: "inconsistent A b"
shows "solve A b = None" unfolding solve_def unfolding if_not_P[OF con[unfolded inconsistent_def]] ..
corollary inconsistent_eq_solve_eq_none:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
shows "inconsistent A b = (solve A b = None)"
unfolding solve_def unfolding inconsistent_def by force
text{*We demonstrate that all solutions of a system of linear equations can be expressed as a linear combination of the basis of the null space plus a particular solution
obtained. The basis and the particular solution are obtained by means of the function @{term "solve A b"}*}
lemma solution_set_rel_solve:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes con: "consistent A b"
shows "solution_set A b = {fst (the (solve A b))} + span (snd (the (solve A b)))"
proof -
have s: "is_solution (fst (the (solve A b))) A b" using consistent_imp_is_solution_solve[OF con] by simp
have "solution_set A b = {fst (the (solve A b))} + solution_set A 0" using solution_set_rel[OF s] .
also have "... = {fst (the (solve A b))} + span (snd (the (solve A b)))" unfolding set_plus_def solve_def unfolding if_P[OF con] the.simps snd_conv fst_conv
proof (auto)
fix b assume "b ∈ solution_set A 0"
thus "b ∈ span (basis_null_space A)" unfolding null_space_eq_solution_set[symmetric] using basis_null_space by fast
next
fix b
assume b: "b ∈ span (basis_null_space A)"
thus "b ∈ solution_set A 0" unfolding null_space_eq_solution_set[symmetric] using basis_null_space by blast
qed
finally show "solution_set A b = {fst (the (solve A b))} + span (snd (the (solve A b)))" .
qed
lemma is_solution_eq_in_span_solve:
fixes A::"real^'cols::{mod_type}^'rows::{mod_type}"
assumes con: "consistent A b"
shows "(is_solution x A b) = (x ∈ {fst (the (solve A b))} + span (snd (the (solve A b))))"
using solution_set_rel_solve[OF con] unfolding solution_set_def by auto
end