swh:1:snp:6189000751ad63f2df385fc3e5a5fbd2996bc358
Tip revision: 63af9181d1c6300497afae5f57f0ce305d7e5c96 authored by Chelsea Edmonds on 12 July 2022, 11:18:18 UTC
Update README.md
Update README.md
Tip revision: 63af918
Linear_Bound_Argument.thy
(* Title: Linear_Bound_Argument.thy
Author: Chelsea Edmonds
*)
section \<open>Linear Bound Argument - General \<close>
text \<open>Lemmas to enable general reasoning using the linear bound argument for combinatorial proofs.
Jukna \cite{juknaExtremalCombinatorics2011} presents a good overview of the mathematical background
this theory is based on and applications \<close>
theory Linear_Bound_Argument imports Incidence_Matrices Jordan_Normal_Form.DL_Rank
Jordan_Normal_Form.Ring_Hom_Matrix
begin
subsection \<open>Vec Space Extensions\<close>
text \<open>Simple extensions to the existing vector space locale on linear independence \<close>
context vec_space
begin
lemma lin_indpt_set_card_lt_dim:
fixes A :: "'a vec set"
assumes "A \<subseteq> carrier_vec n"
assumes "lin_indpt A"
shows "card A \<le> dim"
using assms(1) assms(2) fin_dim li_le_dim(2) by blast
lemma lin_indpt_dim_col_lt_dim:
fixes A :: "'a mat"
assumes "A \<in> carrier_mat n nc"
assumes "distinct (cols A)"
assumes "lin_indpt (set (cols A))"
shows "nc \<le> dim"
proof -
have b: "card (set (cols A)) = dim_col A" using cols_length assms(2)
by (simp add: distinct_card)
have "set (cols A) \<subseteq> carrier_vec n" using assms(1) cols_dim by blast
thus ?thesis using lin_indpt_set_card_lt_dim assms b by auto
qed
lemma lin_comb_imp_lin_dep_fin:
fixes A :: "'a vec set"
assumes "finite A"
assumes "A \<subseteq> carrier_vec n"
assumes "lincomb c A = 0\<^sub>v n"
assumes "\<exists> a. a \<in> A \<and> c a \<noteq> 0"
shows "lin_dep A"
unfolding lin_dep_def using assms lincomb_as_lincomb_list_distinct sumlist_nth by auto
text \<open>While a trivial definition, this enables us to directly reference the definition outside
of a locale context, as @{term "lin_indpt"} is an inherited definition \<close>
definition lin_indpt_vs:: "'a vec set \<Rightarrow> bool" where
"lin_indpt_vs A \<longleftrightarrow> lin_indpt A"
lemma lin_comb_sum_lin_indpt:
fixes A :: "'a vec list"
assumes "set (A) \<subseteq> carrier_vec n"
assumes "distinct A"
assumes "\<And> f. lincomb_list (\<lambda>i. f (A ! i)) A = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
shows "lin_indpt (set A)"
by (rule finite_lin_indpt2, auto simp add: assms lincomb_as_lincomb_list_distinct)
lemma lin_comb_mat_lin_indpt:
fixes A :: "'a vec list"
assumes "set (A) \<subseteq> carrier_vec n"
assumes "distinct A"
assumes "\<And> f. mat_of_cols n A *\<^sub>v vec (length A) (\<lambda>i. f (A ! i)) = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
shows "lin_indpt (set A)"
proof (rule lin_comb_sum_lin_indpt, auto simp add: assms)
fix f v
have "\<And> v. v \<in> set A \<Longrightarrow> dim_vec v = n"
using assms by auto
then show "lincomb_list (\<lambda>i. f (A ! i)) A = 0\<^sub>v n \<Longrightarrow> v \<in> set A \<Longrightarrow> f v = 0"
using lincomb_list_as_mat_mult[of A "(\<lambda>i. f (A ! i))"] assms(3)[of f] by auto
qed
lemma lin_comb_mat_lin_indpt_vs:
fixes A :: "'a vec list"
assumes "set (A) \<subseteq> carrier_vec n"
assumes "distinct A"
assumes "\<And> f. mat_of_cols n A *\<^sub>v vec (length A) (\<lambda>i. f (A ! i)) = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
shows "lin_indpt_vs (set A)"
using lin_comb_mat_lin_indpt lin_indpt_vs_def assms by auto
end
subsection \<open>Linear Bound Argument Lemmas\<close>
text \<open>Three general representations of the linear bound argument, requiring a direct fact of
linear independence onthe rows of the vector space over either a set A of vectors, list xs of vectors
or a Matrix' columns \<close>
lemma lin_bound_arg_general_set:
fixes A ::"('a :: {field})vec set"
assumes "A \<subseteq> carrier_vec nr"
assumes "vec_space.lin_indpt_vs nr A"
shows "card A \<le> nr"
using vec_space.lin_indpt_set_card_lt_dim[of "A" "nr"] vec_space.lin_indpt_vs_def[of nr A]
vec_space.dim_is_n assms by metis
lemma lin_bound_arg_general_list:
fixes xs ::"('a :: {field})vec list"
assumes "distinct xs"
assumes "(set xs) \<subseteq> carrier_vec nr"
assumes "vec_space.lin_indpt_vs nr (set xs)"
shows "length (xs) \<le> nr"
using lin_bound_arg_general_set[of "set xs" nr] distinct_card assms
by force
lemma lin_bound_arg_general:
fixes A ::"('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A \<in> carrier_mat nr nc"
assumes "vec_space.lin_indpt_vs nr (set (cols A))"
shows "nc \<le> nr"
proof -
have ss: "set (cols A) \<subseteq> carrier_vec nr" using assms cols_dim by blast
have "length (cols A) = nc"
using assms(2) cols_length by blast
thus ?thesis using lin_bound_arg_general_list[of "cols A" "nr"] ss assms by simp
qed
text\<open>The linear bound argument lemma on a matrix requiring the lower level assumption on a linear
combination. This removes the need to directly refer to any aspect of the linear algebra libraries \<close>
lemma lin_bound_argument:
fixes A :: "('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A \<in> carrier_mat nr nc"
assumes "\<And> f. A *\<^sub>v vec nc (\<lambda>i. f (col A i)) = 0\<^sub>v nr \<Longrightarrow> \<forall>v\<in> (set (cols A)). f v = 0"
shows "nc \<le> nr"
proof (intro lin_bound_arg_general[of "A" nr nc] vec_space.lin_comb_mat_lin_indpt_vs, simp_all add: assms)
show "set (cols A) \<subseteq> carrier_vec nr" using assms cols_dim by blast
next
have mA: "mat_of_cols nr (cols A) = A" using mat_of_cols_def assms by auto
have "\<And> f. vec (dim_col A) (\<lambda>i. f (cols A ! i)) = vec nc (\<lambda>i. f (col A i))"
proof (intro eq_vecI, simp_all add: assms)
show "\<And>f i. i < nc \<Longrightarrow> vec (dim_col A) (\<lambda>i. f (cols A ! i)) $ i = f (col A i)"
using assms(2) by force
show "dim_col A = nc " using assms by simp
qed
then show "\<And>f. mat_of_cols nr (cols A) *\<^sub>v vec (dim_col A) (\<lambda>i. f (cols A ! i)) = 0\<^sub>v nr \<Longrightarrow>
\<forall>v\<in>set (cols A). f v = 0"
using mA assms(3) by metis
qed
text \<open>A further extension to present the linear combination directly as a sum. This manipulation from
vector product to a summation was found to commonly be repeated in proofs applying this rule \<close>
lemma lin_bound_argument2:
fixes A :: "('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A \<in> carrier_mat nr nc"
assumes "\<And> f. vec nr (\<lambda>i. \<Sum> j \<in> {0..<nc} . f (col A j) * (col A j) $ i) = 0\<^sub>v nr \<Longrightarrow>
\<forall>v\<in> (set (cols A)). f v = 0"
shows "nc \<le> nr"
proof (intro lin_bound_argument[of A nr nc], simp add: assms, simp add: assms)
fix f
have "A *\<^sub>v vec nc (\<lambda>i. f (col A i)) =
vec (dim_row A) (\<lambda>i. \<Sum> j \<in> {0..<nc} . (row A i $ j) * f (col A j))"
by (auto simp add: mult_mat_vec_def scalar_prod_def assms(2))
also have "... = vec (dim_row A) (\<lambda>i. \<Sum> j \<in> {0..<nc} . f (col A j) * (col A j $ i))"
using assms(2) by (intro eq_vecI, simp_all) (meson mult.commute)
finally show "A *\<^sub>v vec nc (\<lambda>i. f (col A i)) = 0\<^sub>v nr \<Longrightarrow> \<forall>v\<in>set (cols A). f v = 0"
using assms(3)[of f] assms(2) by fastforce
qed
end