Theory Incidence_Matrices
section ‹ Incidence Vectors and Matrices ›
text ‹Incidence Matrices are an important representation for any incidence set system. The majority
of basic definitions and properties proved in this theory are based on Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"›
and Colbourn \<^cite>‹"colbournHandbookCombinatorialDesigns2007"›.›
theory Incidence_Matrices imports "Design_Extras" Matrix_Vector_Extras "List-Index.List_Index"
"Design_Theory.Design_Isomorphisms"
begin
subsection ‹Incidence Vectors ›
text ‹A function which takes an ordered list of points, and a block,
returning a 0-1 vector $v$ where there is a 1 in the ith position if point i is in that block ›
definition inc_vec_of :: "'a list ⇒ 'a set ⇒ ('b :: {ring_1}) vec" where
"inc_vec_of Vs bl ≡ vec (length Vs) (λ i . if (Vs ! i) ∈ bl then 1 else 0)"
lemma inc_vec_one_zero_elems: "set⇩v (inc_vec_of Vs bl) ⊆ {0, 1}"
by (auto simp add: vec_set_def inc_vec_of_def)
lemma finite_inc_vec_elems: "finite (set⇩v (inc_vec_of Vs bl))"
using finite_subset inc_vec_one_zero_elems by blast
lemma inc_vec_elems_max_two: "card (set⇩v (inc_vec_of Vs bl)) ≤ 2"
using card_mono inc_vec_one_zero_elems finite.insertI card_0_eq card_2_iff
by (smt (verit) insert_absorb2 linorder_le_cases linordered_nonzero_semiring_class.zero_le_one
obtain_subset_with_card_n one_add_one subset_singletonD trans_le_add1)
lemma inc_vec_dim: "dim_vec (inc_vec_of Vs bl) = length Vs"
by (simp add: inc_vec_of_def)
lemma inc_vec_index: "i < length Vs ⟹ inc_vec_of Vs bl $ i = (if (Vs ! i) ∈ bl then 1 else 0)"
by (simp add: inc_vec_of_def)
lemma inc_vec_index_one_iff: "i < length Vs ⟹ inc_vec_of Vs bl $ i = 1 ⟷ Vs ! i ∈ bl"
by (auto simp add: inc_vec_of_def )
lemma inc_vec_index_zero_iff: "i < length Vs ⟹ inc_vec_of Vs bl $ i = 0 ⟷ Vs ! i ∉ bl"
by (auto simp add: inc_vec_of_def)
lemma inc_vec_of_bij_betw:
assumes "inj_on f (set Vs)"
assumes "bl ⊆ (set Vs)"
shows "inc_vec_of Vs bl = inc_vec_of (map f Vs) (f ` bl)"
proof (intro eq_vecI, simp_all add: inc_vec_dim)
fix i assume "i < length Vs"
then have "Vs ! i ∈ bl ⟷ (map f Vs) ! i ∈ (f ` bl)"
by (metis assms(1) assms(2) inj_on_image_mem_iff nth_map nth_mem)
then show "inc_vec_of Vs bl $ i = inc_vec_of (map f Vs) (f ` bl) $ i"
using inc_vec_index by (metis ‹i < length Vs› length_map)
qed
subsection ‹ Incidence Matrices ›
text ‹ A function which takes a list of points, and list of sets of points, and returns
a $v \times b$ 0-1 matrix $M$, where $v$ is the number of points, and $b$ the number of sets, such
that there is a 1 in the i, j position if and only if point i is in block j. The matrix has
type @{typ "('b :: ring_1) mat"} to allow for operations commonly used on matrices \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››
definition inc_mat_of :: "'a list ⇒ 'a set list ⇒ ('b :: {ring_1}) mat" where
"inc_mat_of Vs Bs ≡ mat (length Vs) (length Bs) (λ (i,j) . if (Vs ! i) ∈ (Bs ! j) then 1 else 0)"
text ‹ Basic lemmas on the @{term "inc_mat_of"} matrix result (elements/dimensions/indexing)›
lemma inc_mat_one_zero_elems: "elements_mat (inc_mat_of Vs Bs) ⊆ {0, 1}"
by (auto simp add: inc_mat_of_def elements_mat_def)
lemma fin_incidence_mat_elems: "finite (elements_mat (inc_mat_of Vs Bs))"
using finite_subset inc_mat_one_zero_elems by auto
lemma inc_matrix_elems_max_two: "card (elements_mat (inc_mat_of Vs Bs)) ≤ 2"
using inc_mat_one_zero_elems order_trans card_2_iff
by (smt (verit, del_insts) antisym bot.extremum card.empty insert_commute insert_subsetI
is_singletonI is_singleton_altdef linorder_le_cases not_one_le_zero one_le_numeral subset_insert)
lemma inc_mat_of_index [simp]: "i < dim_row (inc_mat_of Vs Bs) ⟹ j < dim_col (inc_mat_of Vs Bs) ⟹
inc_mat_of Vs Bs $$ (i, j) = (if (Vs ! i) ∈ (Bs ! j) then 1 else 0)"
by (simp add: inc_mat_of_def)
lemma inc_mat_dim_row: "dim_row (inc_mat_of Vs Bs) = length Vs"
by (simp add: inc_mat_of_def)
lemma inc_mat_dim_vec_row: "dim_vec (row (inc_mat_of Vs Bs) i) = length Bs"
by (simp add: inc_mat_of_def)
lemma inc_mat_dim_col: "dim_col (inc_mat_of Vs Bs) = length Bs"
by (simp add: inc_mat_of_def)
lemma inc_mat_dim_vec_col: "dim_vec (col (inc_mat_of Vs Bs) i) = length Vs"
by (simp add: inc_mat_of_def)
lemma inc_matrix_point_in_block_one: "i < length Vs ⟹ j < length Bs ⟹ Vs ! i ∈ Bs ! j
⟹ (inc_mat_of Vs Bs) $$ (i, j) = 1"
by (simp add: inc_mat_of_def)
lemma inc_matrix_point_not_in_block_zero: "i < length Vs ⟹ j < length Bs ⟹ Vs ! i ∉ Bs ! j ⟹
(inc_mat_of Vs Bs) $$ (i, j) = 0"
by(simp add: inc_mat_of_def)
lemma inc_matrix_point_in_block: "i < length Vs ⟹ j < length Bs ⟹ (inc_mat_of Vs Bs) $$ (i, j) = 1
⟹ Vs ! i ∈ Bs ! j"
using inc_matrix_point_not_in_block_zero by (metis zero_neq_one)
lemma inc_matrix_point_not_in_block: "i < length Vs ⟹ j < length Bs ⟹
(inc_mat_of Vs Bs) $$ (i, j) = 0 ⟹ Vs ! i ∉ Bs ! j"
using inc_matrix_point_in_block_one by (metis zero_neq_one)
lemma inc_matrix_point_not_in_block_iff: "i < length Vs ⟹ j < length Bs ⟹
(inc_mat_of Vs Bs) $$ (i, j) = 0 ⟷ Vs ! i ∉ Bs ! j"
using inc_matrix_point_not_in_block inc_matrix_point_not_in_block_zero by blast
lemma inc_matrix_point_in_block_iff: "i < length Vs ⟹ j < length Bs ⟹
(inc_mat_of Vs Bs) $$ (i, j) = 1 ⟷ Vs ! i ∈ Bs ! j"
using inc_matrix_point_in_block inc_matrix_point_in_block_one by blast
lemma inc_matrix_subset_implies_one:
assumes "I ⊆ {..< length Vs}"
assumes "j < length Bs"
assumes "(!) Vs ` I ⊆ Bs ! j"
assumes "i ∈ I"
shows "(inc_mat_of Vs Bs) $$ (i, j) = 1"
proof -
have iin: "Vs ! i ∈ Bs ! j" using assms(3) assms(4) by auto
have "i < length Vs" using assms(1) assms(4) by auto
thus ?thesis using iin inc_matrix_point_in_block_iff assms(2) by blast
qed
lemma inc_matrix_one_implies_membership: "I ⊆ {..< length Vs} ⟹ j < length Bs ⟹
(⋀ i. i∈I ⟹ (inc_mat_of Vs Bs) $$ (i, j) = 1) ⟹ i ∈ I ⟹ Vs ! i ∈ Bs ! j"
using inc_matrix_point_in_block subset_iff by blast
lemma inc_matrix_elems_one_zero: "i < length Vs ⟹ j < length Bs ⟹
(inc_mat_of Vs Bs) $$ (i, j) = 0 ∨ (inc_mat_of Vs Bs) $$ (i, j) = 1"
using inc_matrix_point_in_block_one inc_matrix_point_not_in_block_zero by blast
text ‹Reasoning on Rows/Columns of the incidence matrix ›
lemma inc_mat_col_def: "j < length Bs ⟹ i < length Vs ⟹
(col (inc_mat_of Vs Bs) j) $ i = (if (Vs ! i ∈ Bs ! j) then 1 else 0)"
by (simp add: inc_mat_of_def)
lemma inc_mat_col_list_map_elem: "j < length Bs ⟹ i < length Vs ⟹
col (inc_mat_of Vs Bs) j $ i = map_vec (λ x . if (x ∈ (Bs ! j)) then 1 else 0) (vec_of_list Vs) $ i"
by (simp add: inc_mat_of_def index_vec_of_list)
lemma inc_mat_col_list_map: "j < length Bs ⟹
col (inc_mat_of Vs Bs) j = map_vec (λ x . if (x ∈ (Bs ! j)) then 1 else 0) (vec_of_list Vs)"
by (intro eq_vecI)
(simp_all add: inc_mat_dim_row inc_mat_dim_col inc_mat_col_list_map_elem index_vec_of_list)
lemma inc_mat_row_def: "j < length Bs ⟹ i < length Vs ⟹
(row (inc_mat_of Vs Bs) i) $ j = (if (Vs ! i ∈ Bs ! j) then 1 else 0)"
by (simp add: inc_mat_of_def)
lemma inc_mat_row_list_map_elem: "j < length Bs ⟹ i < length Vs ⟹
row (inc_mat_of Vs Bs) i $ j = map_vec (λ bl . if ((Vs ! i) ∈ bl) then 1 else 0) (vec_of_list Bs) $ j"
by (simp add: inc_mat_of_def vec_of_list_index)
lemma inc_mat_row_list_map: "i < length Vs ⟹
row (inc_mat_of Vs Bs) i = map_vec (λ bl . if ((Vs ! i) ∈ bl) then 1 else 0) (vec_of_list Bs)"
by (intro eq_vecI)
(simp_all add: inc_mat_dim_row inc_mat_dim_col inc_mat_row_list_map_elem index_vec_of_list)
text ‹ Connecting @{term "inc_vec_of"} and @{term "inc_mat_of"} ›
lemma inc_mat_col_inc_vec: "j < length Bs ⟹ col (inc_mat_of Vs Bs) j = inc_vec_of Vs (Bs ! j)"
by (auto simp add: inc_mat_of_def inc_vec_of_def)
lemma inc_mat_of_cols_inc_vecs: "cols (inc_mat_of Vs Bs) = map (λ j . inc_vec_of Vs j) Bs"
proof (intro nth_equalityI)
have l1: "length (cols (inc_mat_of Vs Bs)) = length Bs"
using inc_mat_dim_col by simp
have l2: "length (map (λ j . inc_vec_of Vs j) Bs) = length Bs"
using length_map by simp
then show "length (cols (inc_mat_of Vs Bs)) = length (map (inc_vec_of Vs) Bs)"
using l1 l2 by simp
show "⋀ i. i < length (cols (inc_mat_of Vs Bs)) ⟹
(cols (inc_mat_of Vs Bs) ! i) = (map (λ j . inc_vec_of Vs j) Bs) ! i"
using inc_mat_col_inc_vec l1 by (metis cols_nth inc_mat_dim_col nth_map)
qed
lemma inc_mat_of_bij_betw:
assumes "inj_on f (set Vs)"
assumes "⋀ bl . bl ∈ (set Bs) ⟹ bl ⊆ (set Vs)"
shows "inc_mat_of Vs Bs = inc_mat_of (map f Vs) (map ((`) f) Bs)"
proof (intro eq_matI, simp_all add: inc_mat_dim_row inc_mat_dim_col, intro impI)
fix i j assume ilt: "i < length Vs" and jlt: " j < length Bs" and "Vs ! i ∉ Bs ! j"
then show "f (Vs ! i) ∉ f ` Bs ! j"
by (meson assms(1) assms(2) ilt inj_on_image_mem_iff jlt nth_mem)
qed
text ‹Definitions for the incidence matrix representation of common incidence system properties ›
definition non_empty_col :: "('a :: {zero_neq_one}) mat ⇒ nat ⇒ bool" where
"non_empty_col M j ≡ ∃ k. k ≠ 0 ∧ k ∈$ col M j"
definition proper_inc_mat :: "('a :: {zero_neq_one}) mat ⇒ bool" where
"proper_inc_mat M ≡ (dim_row M > 0 ∧ dim_col M > 0)"
text ‹Matrix version of the representation number property @{term "point_replication_number"}›
definition mat_rep_num :: "('a :: {zero_neq_one}) mat ⇒ nat ⇒ nat" where
"mat_rep_num M i ≡ count_vec (row M i) 1"
text ‹Matrix version of the points index property @{term "points_index"}›
definition mat_point_index :: "('a :: {zero_neq_one}) mat ⇒ nat set ⇒ nat" where
"mat_point_index M I ≡ card {j . j < dim_col M ∧ (∀ i ∈ I. M $$ (i, j) = 1)}"
definition mat_inter_num :: "('a :: {zero_neq_one}) mat ⇒ nat ⇒ nat ⇒ nat" where
"mat_inter_num M j1 j2 ≡ card {i . i < dim_row M ∧ M $$ (i, j1) = 1 ∧ M $$ (i, j2) = 1}"
text ‹Matrix version of the block size property›
definition mat_block_size :: "('a :: {zero_neq_one}) mat ⇒ nat ⇒ nat" where
"mat_block_size M j ≡ count_vec (col M j) 1"
lemma non_empty_col_obtains:
assumes "non_empty_col M j"
obtains i where "i < dim_row M" and "(col M j) $ i ≠ 0"
proof -
have d: "dim_vec (col M j) = dim_row M" by simp
from assms obtain k where "k ≠ 0" and "k ∈$ col M j"
by (auto simp add: non_empty_col_def)
thus ?thesis using vec_contains_obtains_index d
by (metis that)
qed
lemma non_empty_col_alt_def:
assumes "j < dim_col M"
shows "non_empty_col M j ⟷ (∃ i. i < dim_row M ∧ M $$ (i, j) ≠ 0)"
proof (intro iffI)
show "non_empty_col M j ⟹ ∃i<dim_row M. M $$ (i, j) ≠ 0"
by(metis assms index_col non_empty_col_obtains)
next
assume "∃i<dim_row M. M $$ (i, j) ≠ 0"
then obtain i where ilt: " i < dim_row M" and ne: "M $$ (i, j) ≠ 0" by blast
then have ilt2: " i < dim_vec (col M j)" by simp
then have "(col M j) $ i ≠ 0" using ne by (simp add: assms)
then obtain k where "(col M j) $ i = k" and "k ≠ 0"
by simp
then show "non_empty_col M j " using non_empty_col_def
by (metis ilt2 vec_setI)
qed
lemma proper_inc_mat_map: "proper_inc_mat M ⟹ proper_inc_mat (map_mat f M)"
by (simp add: proper_inc_mat_def)
lemma mat_point_index_alt: "mat_point_index M I = card {j ∈ {0..<dim_col M} . (∀ i ∈ I . M $$(i, j) = 1)}"
by (simp add: mat_point_index_def)
lemma mat_block_size_sum_alt:
fixes M :: "'a :: {ring_1} mat"
shows "elements_mat M ⊆ {0, 1} ⟹ j < dim_col M ⟹ of_nat (mat_block_size M j) = sum_vec (col M j)"
unfolding mat_block_size_def using count_vec_sum_ones_alt col_elems_subset_mat subset_trans
by metis
lemma mat_rep_num_sum_alt:
fixes M :: "'a :: {ring_1} mat"
shows "elements_mat M ⊆ {0, 1} ⟹ i < dim_row M ⟹ of_nat (mat_rep_num M i) = sum_vec (row M i)"
using count_vec_sum_ones_alt
by (metis mat_rep_num_def row_elems_subset_mat subset_trans)
lemma mat_point_index_two_alt:
assumes "i1 < dim_row M"
assumes "i2 < dim_row M"
shows "mat_point_index M {i1, i2} = card {j . j < dim_col M ∧ M $$(i1, j) = 1 ∧ M $$ (i2, j) = 1}"
proof -
let ?I = "{i1, i2}"
have ss: "{i1, i2} ⊆ {..<dim_row M}" using assms by blast
have filter: "⋀ j . j < dim_col M ⟹ (∀ i ∈ ?I . M $$(i, j) = 1) ⟷ M $$(i1, j) = 1 ∧ M $$ (i2, j) = 1"
by auto
have "?I ⊆ {..< dim_row M}" using assms(1) assms(2) by fastforce
thus ?thesis using filter ss unfolding mat_point_index_def
by meson
qed
text ‹ Transpose symmetries ›
lemma trans_mat_rep_block_size_sym: "j < dim_col M ⟹ mat_block_size M j = mat_rep_num M⇧T j"
"i < dim_row M ⟹ mat_rep_num M i = mat_block_size M⇧T i"
unfolding mat_block_size_def mat_rep_num_def by simp_all
lemma trans_mat_point_index_inter_sym:
"i1 < dim_row M ⟹ i2 < dim_row M ⟹ mat_point_index M {i1, i2} = mat_inter_num M⇧T i1 i2"
"j1 < dim_col M ⟹ j2 < dim_col M ⟹ mat_inter_num M j1 j2 = mat_point_index M⇧T {j1, j2}"
apply (simp_all add: mat_inter_num_def mat_point_index_two_alt)
apply (metis (no_types, lifting) index_transpose_mat(1))
by (metis (no_types, lifting) index_transpose_mat(1))
subsection ‹0-1 Matrices ›
text ‹Incidence matrices contain only two elements: 0 and 1. We define a locale which provides
a context to work in for matrices satisfying this condition for any @{typ "'b :: zero_neq_one"} type.›
locale zero_one_matrix =
fixes matrix :: "'b :: {zero_neq_one} mat" ("M")
assumes elems01: "elements_mat M ⊆ {0, 1}"
begin
text ‹ Row and Column Properties of the Matrix ›
lemma row_elems_ss01:"i < dim_row M ⟹ vec_set (row M i) ⊆ {0, 1}"
using row_elems_subset_mat elems01 by blast
lemma col_elems_ss01:
assumes "j < dim_col M"
shows "vec_set (col M j) ⊆ {0, 1}"
proof -
have "vec_set (col M j) ⊆ elements_mat M" using assms
by (simp add: col_elems_subset_mat assms)
thus ?thesis using elems01 by blast
qed
lemma col_nth_0_or_1_iff:
assumes "j < dim_col M"
assumes "i < dim_row M"
shows "col M j $ i = 0 ⟷ col M j $ i ≠ 1"
proof (intro iffI)
have dv: "i < dim_vec (col M j)" using assms by simp
have sv: "set⇩v (col M j) ⊆ {0, 1}" using col_elems_ss01 assms by simp
then show "col M j $ i = 0 ⟹ col M j $ i ≠ 1" using dv by simp
show "col M j $ i ≠ 1 ⟹ col M j $ i = 0" using dv sv
by (meson insertE singletonD subset_eq vec_setI)
qed
lemma row_nth_0_or_1_iff:
assumes "j < dim_col M"
assumes "i < dim_row M"
shows "row M i $ j = 0 ⟷ row M i $ j ≠ 1"
proof (intro iffI)
have dv: "j < dim_vec (row M i)" using assms by simp
have sv: "set⇩v (row M i) ⊆ {0, 1}" using row_elems_ss01 assms by simp
then show "row M i $ j = 0 ⟹ row M i $ j ≠ 1" by simp
show "row M i $ j ≠ 1 ⟹ row M i $ j = 0" using dv sv
by (meson insertE singletonD subset_eq vec_setI)
qed
lemma transpose_entries: "elements_mat (M⇧T) ⊆ {0, 1}"
using elems01 transpose_mat_elems by metis
lemma M_not_zero_simp: "j < dim_col M ⟹ i < dim_row M ⟹ M $$ (i, j) ≠ 0 ⟹ M $$ (i, j) = 1"
using elems01 by auto
lemma M_not_one_simp: "j < dim_col M ⟹ i < dim_row M ⟹ M $$ (i, j) ≠ 1 ⟹ M $$ (i, j) = 0"
using elems01 by auto
text ‹Definition for mapping a column to a block ›
definition map_col_to_block :: "'a :: {zero_neq_one} vec ⇒ nat set" where
"map_col_to_block c ≡ { i ∈ {..<dim_vec c} . c $ i = 1}"
lemma map_col_to_block_alt: "map_col_to_block c = {i . i < dim_vec c ∧ c$ i = 1}"
by (simp add: map_col_to_block_def)
lemma map_col_to_block_elem: "i < dim_vec c ⟹ i ∈ map_col_to_block c ⟷ c $ i = 1"
by (simp add: map_col_to_block_alt)
lemma in_map_col_valid_index: "i ∈ map_col_to_block c ⟹ i < dim_vec c"
by (simp add: map_col_to_block_alt)
lemma map_col_to_block_size: "j < dim_col M ⟹ card (map_col_to_block (col M j)) = mat_block_size M j"
unfolding mat_block_size_def map_col_to_block_alt using count_vec_alt[of "col M j" "1"] Collect_cong
by (metis (no_types, lifting))
lemma in_map_col_valid_index_M: "j < dim_col M ⟹ i ∈ map_col_to_block (col M j) ⟹ i < dim_row M"
using in_map_col_valid_index by (metis dim_col)
lemma map_col_to_block_elem_not: "c ∈ set (cols M) ⟹ i < dim_vec c ⟹ i ∉ map_col_to_block c ⟷ c $ i = 0"
apply (auto simp add: map_col_to_block_alt)
using elems01 by (metis col_nth_0_or_1_iff dim_col obtain_col_index)
lemma obtain_block_index_map_block_set:
assumes "bl ∈# {# map_col_to_block c . c ∈# mset (cols M)#}"
obtains j where "j < dim_col M" and "bl = map_col_to_block (col M j)"
proof -
obtain c where bleq: "bl = map_col_to_block c" and "c ∈# mset (cols M)"
using assms by blast
then have "c ∈ set (cols M)" by simp
thus ?thesis using bleq obtain_col_index
by (metis that)
qed
lemma mat_ord_inc_sys_point[simp]: "x < dim_row M ⟹ [0..<(dim_row M)] ! x = x"
by simp
lemma mat_ord_inc_sys_block[simp]: "j < dim_col M ⟹
(map (map_col_to_block) (cols M)) ! j = map_col_to_block (col M j)"
by auto
lemma ordered_to_mset_col_blocks:
"{# map_col_to_block c . c ∈# mset (cols M)#} = mset (map (map_col_to_block) (cols M))"
by simp
text ‹ Lemmas on incidence matrix properties ›
lemma non_empty_col_01:
assumes "j < dim_col M"
shows "non_empty_col M j ⟷ 1 ∈$ col M j"
proof (intro iffI)
assume "non_empty_col M j"
then obtain k where kn0: "k ≠ 0" and kin: "k ∈$ col M j" using non_empty_col_def
by blast
then have "k ∈ elements_mat M" using vec_contains_col_elements_mat assms
by metis
then have "k = 1" using kn0
using elems01 by blast
thus "1 ∈$ col M j" using kin by simp
next
assume "1 ∈$ col M j"
then show "non_empty_col M j" using non_empty_col_def
by (metis zero_neq_one)
qed
lemma mat_rep_num_alt:
assumes "i < dim_row M"
shows "mat_rep_num M i = card {j . j < dim_col M ∧ M $$ (i, j) = 1}"
proof (simp add: mat_rep_num_def)
have eq: "⋀ j. (j < dim_col M ∧ M $$ (i, j) = 1) = (row M i $ j = 1 ∧ j < dim_vec (row M i))"
using assms by auto
have "count_vec (row M i) 1 = card {j. (row M i) $ j = 1 ∧ j < dim_vec (row M i)}"
using count_vec_alt[of "row M i" "1"] by simp
thus "count_vec (row M i) 1 = card {j. j < dim_col M ∧ M $$ (i, j) = 1}"
using eq Collect_cong by simp
qed
lemma mat_rep_num_alt_col: "i < dim_row M ⟹ mat_rep_num M i = size {#c ∈# (mset (cols M)) . c $ i = 1#}"
using mat_rep_num_alt index_to_col_card_size_prop[of i M] by auto
text ‹ A zero one matrix is an incidence system ›
lemma map_col_to_block_wf: "⋀c. c ∈ set (cols M) ⟹ map_col_to_block c ⊆ {0..<dim_row M}"
by (auto simp add: map_col_to_block_def)(metis dim_col obtain_col_index)
lemma one_implies_block_nempty: "j < dim_col M ⟹ 1 ∈$ (col M j) ⟹ map_col_to_block (col M j) ≠ {}"
unfolding map_col_to_block_def using vec_setE by force
interpretation incidence_sys: incidence_system "{0..<dim_row M}"
"{# map_col_to_block c . c ∈# mset (cols M)#}"
using map_col_to_block_wf by (unfold_locales) auto
interpretation fin_incidence_sys: finite_incidence_system "{0..<dim_row M}"
"{# map_col_to_block c . c ∈# mset (cols M)#}"
by (unfold_locales) (simp)
lemma block_nempty_implies_all_zeros: "j < dim_col M ⟹ map_col_to_block (col M j) = {} ⟹
i < dim_row M ⟹ col M j $ i = 0"
by (metis col_nth_0_or_1_iff dim_col one_implies_block_nempty vec_setI)
lemma block_nempty_implies_no_one: "j < dim_col M ⟹ map_col_to_block (col M j) = {} ⟹ ¬ (1 ∈$ (col M j))"
using one_implies_block_nempty by blast
lemma mat_is_design:
assumes "⋀j. j < dim_col M⟹ 1 ∈$ (col M j)"
shows "design {0..<dim_row M} {# map_col_to_block c . c ∈# mset (cols M)#}"
proof (unfold_locales)
fix bl
assume "bl ∈# {# map_col_to_block c . c ∈# mset (cols M)#}"
then obtain j where "j < dim_col M" and map: "bl = map_col_to_block (col M j)"
using obtain_block_index_map_block_set by auto
thus "bl ≠ {}" using assms one_implies_block_nempty
by simp
qed
lemma mat_is_proper_design:
assumes "⋀j. j < dim_col M ⟹ 1 ∈$ (col M j)"
assumes "dim_col M > 0"
shows "proper_design {0..<dim_row M} {# map_col_to_block c . c ∈# mset (cols M)#}"
proof -
interpret des: design "{0..<dim_row M}" "{# map_col_to_block c . c ∈# mset (cols M)#}"
using mat_is_design assms by simp
show ?thesis proof (unfold_locales)
have "length (cols M) ≠ 0" using assms(2) by auto
then have "size {# map_col_to_block c . c ∈# mset (cols M)#} ≠ 0" by auto
then show "incidence_sys.𝖻 ≠ 0" by simp
qed
qed
text ‹ Show the 01 injective function preserves system properties ›
lemma inj_on_01_hom_index:
assumes "inj_on_01_hom f"
assumes "i < dim_row M" "j < dim_col M"
shows "M $$ (i, j) = 1 ⟷ (map_mat f M) $$ (i, j) = 1"
and "M $$ (i, j) = 0 ⟷ (map_mat f M) $$ (i, j) = 0"
proof -
interpret hom: inj_on_01_hom f using assms by simp
show "M $$ (i, j) = 1 ⟷ (map_mat f M) $$ (i, j) = 1"
using assms col_nth_0_or_1_iff
by (simp add: hom.inj_1_iff)
show "M $$ (i, j) = 0 ⟷ (map_mat f M) $$ (i, j) = 0"
using assms col_nth_0_or_1_iff
by (simp add: hom.inj_0_iff)
qed
lemma preserve_non_empty:
assumes "inj_on_01_hom f"
assumes "j < dim_col M"
shows "non_empty_col M j ⟷ non_empty_col (map_mat f M) j"
proof(simp add: non_empty_col_def, intro iffI)
interpret hom: inj_on_01_hom f using assms(1) by simp
assume "∃k. k ≠ 0 ∧ k ∈$ col M j"
then obtain k where kneq: "k ≠ 0" and kin: "k ∈$ col M j" by blast
then have "f k ∈$ col (map_mat f M) j" using vec_contains_img
by (metis assms(2) col_map_mat)
then have "f k ≠ 0" using assms(1) kneq kin assms(2) col_elems_ss01 hom.inj_0_iff by blast
thus "∃k. k ≠ 0 ∧ k ∈$ col (map_mat f M) j"
using ‹f k ∈$ col (map_mat f M) j› by blast
next
interpret hom: inj_on_01_hom f using assms(1) by simp
assume "∃k. k ≠ 0 ∧ k ∈$ col (map_mat f M) j"
then obtain k where kneq: "k ≠ 0" and kin: "k ∈$ col (map_mat f M) j" by blast
then have "k ∈$ map_vec f (col M j)" using assms(2) col_map_mat by simp
then have "k ∈ f ` set⇩v (col M j)"
by (smt (verit) image_eqI index_map_vec(1) index_map_vec(2) vec_setE vec_setI)
then obtain k' where keq: "k = f k'" and kin2: "k' ∈ set⇩v (col M j)"
by blast
then have "k' ≠ 0" using assms(1) kneq hom.inj_0_iff by blast
thus "∃k. k ≠ 0 ∧ k ∈$ col M j" using kin2 by auto
qed
lemma preserve_mat_rep_num:
assumes "inj_on_01_hom f"
assumes "i < dim_row M"
shows "mat_rep_num M i = mat_rep_num (map_mat f M) i"
unfolding mat_rep_num_def using injective_lim.lim_inj_hom_count_vec inj_on_01_hom_def row_map_mat
by (metis assms(1) assms(2) inj_on_01_hom.inj_1_iff insert_iff row_elems_ss01)
lemma preserve_mat_block_size:
assumes "inj_on_01_hom f"
assumes "j < dim_col M"
shows "mat_block_size M j = mat_block_size (map_mat f M) j"
unfolding mat_block_size_def using injective_lim.lim_inj_hom_count_vec inj_on_01_hom_def col_map_mat
by (metis assms(1) assms(2) inj_on_01_hom.inj_1_iff insert_iff col_elems_ss01)
lemma preserve_mat_point_index:
assumes "inj_on_01_hom f"
assumes "⋀ i. i ∈ I ⟹ i < dim_row M"
shows "mat_point_index M I = mat_point_index (map_mat f M) I"
proof -
have "⋀ i j. i ∈ I ⟹ j < dim_col M ∧ M $$ (i, j) = 1 ⟷
j < dim_col (map_mat f M) ∧ (map_mat f M) $$ (i, j) = 1"
using assms(2) inj_on_01_hom_index(1) assms(1) by (metis index_map_mat(3))
thus ?thesis unfolding mat_point_index_def
by (metis (no_types, opaque_lifting) index_map_mat(3))
qed
lemma preserve_mat_inter_num:
assumes "inj_on_01_hom f"
assumes "j1 < dim_col M" "j2 < dim_col M"
shows "mat_inter_num M j1 j2 = mat_inter_num (map_mat f M) j1 j2"
unfolding mat_inter_num_def using assms
by (metis (no_types, opaque_lifting) index_map_mat(2) inj_on_01_hom_index(1))
lemma lift_mat_01_index_iff:
"i < dim_row M ⟹ j < dim_col M ⟹ (lift_01_mat M) $$ (i, j) = 0 ⟷ M $$ (i, j) = 0"
"i < dim_row M ⟹ j < dim_col M ⟹ (lift_01_mat M) $$ (i, j) = 1 ⟷ M $$ (i, j) = 1"
by (simp) (metis col_nth_0_or_1_iff index_col lift_01_mat_simp(3) of_zero_neq_one_def zero_neq_one)
lemma lift_mat_elems: "elements_mat (lift_01_mat M) ⊆ {0, 1}"
proof -
have "elements_mat (lift_01_mat M) = of_zero_neq_one ` (elements_mat M)"
by (simp add: lift_01_mat_def map_mat_elements)
then have "elements_mat (lift_01_mat M) ⊆ of_zero_neq_one ` {0, 1}" using elems01
by fastforce
thus ?thesis
by simp
qed
lemma lift_mat_is_0_1: "zero_one_matrix (lift_01_mat M)"
using lift_mat_elems by (unfold_locales)
lemma lift_01_mat_distinct_cols: "distinct (cols M) ⟹ distinct (cols (lift_01_mat M))"
using of_injective_lim.mat_cols_hom_lim_distinct_iff lift_01_mat_def
by (metis elems01 map_vec_mat_cols)
end
text ‹Some properties must be further restricted to matrices having a @{typ "'a :: ring_1"} type ›
locale zero_one_matrix_ring_1 = zero_one_matrix M for M :: "'b :: {ring_1} mat"
begin
lemma map_col_block_eq:
assumes "c ∈ set(cols M)"
shows "inc_vec_of [0..<dim_vec c] (map_col_to_block c) = c"
proof (intro eq_vecI, simp add: map_col_to_block_def inc_vec_of_def, intro impI)
show "⋀i. i < dim_vec c ⟹ c $ i ≠ 1 ⟹ c $ i = 0"
using assms map_col_to_block_elem map_col_to_block_elem_not by auto
show "dim_vec (inc_vec_of [0..<dim_vec c] (map_col_to_block c)) = dim_vec c"
unfolding inc_vec_of_def by simp
qed
lemma inc_mat_of_map_rev: "inc_mat_of [0..<dim_row M] (map map_col_to_block (cols M)) = M"
proof (intro eq_matI, simp_all add: inc_mat_of_def, intro conjI impI)
show "⋀i j. i < dim_row M ⟹ j < dim_col M ⟹ i ∈ map_col_to_block (col M j) ⟹ M $$ (i, j) = 1"
by (simp add: map_col_to_block_elem)
show "⋀i j. i < dim_row M ⟹ j < dim_col M ⟹ i ∉ map_col_to_block (col M j) ⟹ M $$ (i, j) = 0"
by (metis col_nth_0_or_1_iff dim_col index_col map_col_to_block_elem)
qed
lemma M_index_square_itself: "j < dim_col M ⟹ i < dim_row M ⟹ (M $$ (i, j))^2 = M $$ (i, j)"
using M_not_zero_simp by (cases "M $$ (i, j) = 0")(simp_all, metis power_one)
lemma M_col_index_square_itself: "j < dim_col M ⟹ i < dim_row M ⟹ ((col M j) $ i)^2 = (col M j) $ i"
using index_col M_index_square_itself by auto
text ‹ Scalar Prod Alternative definitions for matrix properties ›
lemma scalar_prod_inc_vec_block_size_mat:
assumes "j < dim_col M"
shows "(col M j) ∙ (col M j) = of_nat (mat_block_size M j)"
proof -
have "(col M j) ∙ (col M j) = (∑ i ∈ {0..<dim_row M} . (col M j) $ i * (col M j) $ i)"
using assms scalar_prod_def sum.cong by (smt (verit, ccfv_threshold) dim_col)
also have "... = (∑ i ∈ {0..<dim_row M} . ((col M j) $ i)^2)"
by (simp add: power2_eq_square )
also have "... = (∑ i ∈ {0..<dim_row M} . ((col M j) $ i))"
using M_col_index_square_itself assms by auto
finally show ?thesis using sum_vec_def mat_block_size_sum_alt
by (metis assms dim_col elems01)
qed
lemma scalar_prod_inc_vec_mat_inter_num:
assumes "j1 < dim_col M" "j2 < dim_col M"
shows "(col M j1) ∙ (col M j2) = of_nat (mat_inter_num M j1 j2)"
proof -
have split: "{0..<dim_row M} = {i ∈ {0..<dim_row M} . (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1) } ∪
{i ∈ {0..<dim_row M} . M $$ (i, j1) = 0 ∨ M $$ (i, j2) = 0}" using assms M_not_zero_simp by auto
have inter: "{i ∈ {0..<dim_row M} . (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1) } ∩
{i ∈ {0..<dim_row M} . M $$ (i, j1) = 0 ∨ M $$ (i, j2) = 0} = {}" by auto
have "(col M j1) ∙ (col M j2) = (∑ i ∈ {0..<dim_row M} . (col M j1) $ i * (col M j2) $ i)"
using assms scalar_prod_def by (metis (full_types) dim_col)
also have "... = (∑ i ∈ {0..<dim_row M} . M $$ (i, j1) * M $$ (i, j2))"
using assms by simp
also have "... = (∑ i ∈ {i ∈ {0..<dim_row M} . (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1) } . M $$ (i, j1) * M $$ (i, j2))
+ (∑ i ∈ {i ∈ {0..<dim_row M} . M $$ (i, j1) = 0 ∨ M $$ (i, j2) = 0} . M $$ (i, j1) * M $$ (i, j2))"
using split inter sum.union_disjoint[of " {i ∈ {0..<dim_row M} . (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1)}"
"{i ∈ {0..<dim_row M} . M $$ (i, j1) = 0 ∨ M $$ (i, j2) = 0}" "λ i . M $$ (i, j1) * M $$ (i, j2)"]
by (metis (no_types, lifting) finite_Un finite_atLeastLessThan)
also have "... = (∑ i ∈ {i ∈ {0..<dim_row M} . (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1) } . 1)
+ (∑ i ∈ {i ∈ {0..<dim_row M} . M $$ (i, j1) = 0 ∨ M $$ (i, j2) = 0} . 0)"
using sum.cong mem_Collect_eq by (smt (z3) mult.right_neutral mult_not_zero)
finally have "(col M j1) ∙ (col M j2) =
of_nat (card {i . i < dim_row M ∧ (M $$ (i, j1) = 1) ∧ (M $$ (i, j2) = 1)})"
by simp
then show ?thesis using mat_inter_num_def[of M j1 j2] by simp
qed
end
text ‹ Any matrix generated by @{term "inc_mat_of"} is a 0-1 matrix.›
lemma inc_mat_of_01_mat: "zero_one_matrix_ring_1 (inc_mat_of Vs Bs)"
by (unfold_locales) (simp add: inc_mat_one_zero_elems)
subsection ‹Ordered Incidence Systems ›
text ‹We impose an arbitrary ordering on the point set and block collection to enable
matrix reasoning. Note that this is also common in computer algebra representations of designs ›
locale ordered_incidence_system =
fixes 𝒱s :: "'a list" and ℬs :: "'a set list"
assumes wf_list: "b ∈# (mset ℬs) ⟹ b ⊆ set 𝒱s"
assumes distinct: "distinct 𝒱s"
text ‹An ordered incidence system, as it is defined on lists, can only represent finite incidence systems ›
sublocale ordered_incidence_system ⊆ finite_incidence_system "set 𝒱s" "mset ℬs"
by(unfold_locales) (auto simp add: wf_list)
lemma ordered_incidence_sysI:
assumes "finite_incidence_system 𝒱 ℬ"
assumes "𝒱s ∈ permutations_of_set 𝒱" and "ℬs ∈ permutations_of_multiset ℬ"
shows "ordered_incidence_system 𝒱s ℬs"
proof -
have veq: "𝒱 = set 𝒱s" using assms permutations_of_setD(1) by auto
have beq: "ℬ = mset ℬs" using assms permutations_of_multisetD by auto
interpret fisys: finite_incidence_system "set 𝒱s" "mset ℬs" using assms(1) veq beq by simp
show ?thesis proof (unfold_locales)
show "⋀b. b ∈# mset ℬs ⟹ b ⊆ set 𝒱s" using fisys.wellformed
by simp
show "distinct 𝒱s" using assms permutations_of_setD(2) by auto
qed
qed
lemma ordered_incidence_sysII:
assumes "finite_incidence_system 𝒱 ℬ" and "set 𝒱s = 𝒱" and "distinct 𝒱s" and "mset ℬs = ℬ"
shows "ordered_incidence_system 𝒱s ℬs"
proof -
interpret fisys: finite_incidence_system "set 𝒱s" "mset ℬs" using assms by simp
show ?thesis using fisys.wellformed assms by (unfold_locales) (simp_all)
qed
context ordered_incidence_system
begin
text ‹For ease of notation, establish the same notation as for incidence systems ›
abbreviation "𝒱 ≡ set 𝒱s"
abbreviation "ℬ ≡ mset ℬs"
text ‹Basic properties on ordered lists ›
lemma points_indexing: "𝒱s ∈ permutations_of_set 𝒱"
by (simp add: permutations_of_set_def distinct)
lemma blocks_indexing: "ℬs ∈ permutations_of_multiset ℬ"
by (simp add: permutations_of_multiset_def)
lemma points_list_empty_iff: "𝒱s = [] ⟷ 𝒱 = {}"
using finite_sets points_indexing
by (simp add: elem_permutation_of_set_empty_iff)
lemma points_indexing_inj: "∀ i ∈ I . i < length 𝒱s ⟹ inj_on ((!) 𝒱s) I"
by (simp add: distinct inj_on_nth)
lemma blocks_list_empty_iff: "ℬs = [] ⟷ ℬ = {#}"
using blocks_indexing by (simp)
lemma blocks_list_nempty: "proper_design 𝒱 ℬ ⟹ ℬs ≠ []"
using mset.simps(1) proper_design.design_blocks_nempty by blast
lemma points_list_nempty: "proper_design 𝒱 ℬ ⟹ 𝒱s ≠ []"
using proper_design.design_points_nempty points_list_empty_iff by blast
lemma points_list_length: "length 𝒱s = 𝗏"
using points_indexing
by (simp add: length_finite_permutations_of_set)
lemma blocks_list_length: "length ℬs = 𝖻"
using blocks_indexing length_finite_permutations_of_multiset by blast
lemma valid_points_index: "i < 𝗏 ⟹ 𝒱s ! i ∈ 𝒱"
using points_list_length by simp
lemma valid_points_index_cons: "x ∈ 𝒱 ⟹ ∃ i. 𝒱s ! i = x ∧ i < 𝗏"
using points_list_length by (auto simp add: in_set_conv_nth)
lemma valid_points_index_obtains:
assumes "x ∈ 𝒱"
obtains i where "𝒱s ! i = x ∧ i < 𝗏"
using valid_points_index_cons assms by auto
lemma valid_blocks_index: "j < 𝖻 ⟹ ℬs ! j ∈# ℬ"
using blocks_list_length by (metis nth_mem_mset)
lemma valid_blocks_index_cons: "bl ∈# ℬ ⟹ ∃ j . ℬs ! j = bl ∧ j < 𝖻"
by (auto simp add: in_set_conv_nth)
lemma valid_blocks_index_obtains:
assumes "bl ∈# ℬ"
obtains j where "ℬs ! j = bl ∧ j < 𝖻"
using assms valid_blocks_index_cons by auto
lemma block_points_valid_point_index:
assumes "bl ∈# ℬ" "x ∈ bl"
obtains i where "i < length 𝒱s ∧ 𝒱s ! i = x"
using wellformed valid_points_index_obtains assms
by (metis points_list_length wf_invalid_point)
lemma points_set_index_img: "𝒱 = image(λ i . (𝒱s ! i)) ({..<𝗏})"
using valid_points_index_cons valid_points_index by auto
lemma blocks_mset_image: "ℬ = image_mset (λ i . (ℬs ! i)) (mset_set {..<𝖻})"
by (simp add: mset_list_by_index)
lemma incidence_cond_indexed[simp]: "i < 𝗏 ⟹ j < 𝖻 ⟹ incident (𝒱s ! i) (ℬs ! j) ⟷ (𝒱s ! i) ∈ (ℬs ! j)"
using incidence_alt_def valid_points_index valid_blocks_index by simp
lemma bij_betw_points_index: "bij_betw (λ i. 𝒱s ! i) {0..<𝗏} 𝒱"
proof (simp add: bij_betw_def, intro conjI)
show "inj_on ((!) 𝒱s) {0..<𝗏}"
by (simp add: points_indexing_inj points_list_length)
show "(!) 𝒱s ` {0..<𝗏} = 𝒱"
proof (intro subset_antisym subsetI)
fix x assume "x ∈ (!) 𝒱s ` {0..<𝗏}"
then obtain i where "x = 𝒱s ! i" and "i < 𝗏" by auto
then show "x ∈ 𝒱"
by (simp add: valid_points_index)
next
fix x assume "x ∈ 𝒱"
then obtain i where "𝒱s ! i = x" and "i <𝗏"
using valid_points_index_cons by auto
then show "x ∈ (!) 𝒱s ` {0..<𝗏}" by auto
qed
qed
text ‹Some lemmas on cardinality due to different set descriptor filters ›
lemma card_filter_point_indices: "card {i ∈ {0..<𝗏}. P (𝒱s ! i)} = card {v ∈ 𝒱 . P v }"
proof -
have "{v ∈ 𝒱 . P v }= (λ i. 𝒱s ! i) ` {i ∈ {0..<𝗏}. P (𝒱s ! i)}"
by (metis Compr_image_eq lessThan_atLeast0 points_set_index_img)
thus ?thesis using inj_on_nth points_list_length
by (metis (no_types, lifting) card_image distinct lessThan_atLeast0 lessThan_iff mem_Collect_eq)
qed
lemma card_block_points_filter:
assumes "j < 𝖻"
shows "card (ℬs ! j) = card {i ∈ {0..<𝗏} . (𝒱s ! i) ∈ (ℬs ! j)}"
proof -
obtain bl where "bl ∈# ℬ" and blis: "bl = ℬs ! j"
using assms by auto
then have cbl: "card bl = card {v ∈ 𝒱 . v ∈ bl}" using block_size_alt by simp
have "𝒱 = (λ i. 𝒱s ! i) ` {0..<𝗏}" using bij_betw_points_index
using lessThan_atLeast0 points_set_index_img by presburger
then have "Set.filter (λ v . v ∈ bl) 𝒱 = Set.filter (λ v . v ∈ bl) ((λ i. 𝒱s ! i) ` {0..<𝗏})"
by presburger
have "card {i ∈ {0..<𝗏} . (𝒱s ! i) ∈ bl} = card {v ∈ 𝒱 . v ∈ bl}"
using card_filter_point_indices by simp
thus ?thesis using cbl blis by simp
qed
lemma obtains_two_diff_block_indexes:
assumes "j1 < 𝖻"
assumes "j2 < 𝖻"
assumes "j1 ≠ j2"
assumes "𝖻 ≥ 2"
obtains bl1 bl2 where "bl1 ∈# ℬ" and "ℬs ! j1 = bl1" and "bl2 ∈# ℬ - {#bl1#}" and "ℬs ! j2 = bl2"
proof -
have j1lt: "min j1 (length ℬs) = j1" using assms by auto
obtain bl1 where bl1in: "bl1 ∈# ℬ" and bl1eq: "ℬs ! j1 = bl1"
using assms(1) valid_blocks_index by blast
then have split: "ℬs = take j1 ℬs @ ℬs!j1 # drop (Suc j1) ℬs"
using assms id_take_nth_drop by auto
then have lj1: "length (take j1 ℬs) = j1" using j1lt by (simp add: length_take[of j1 ℬs])
have "ℬ = mset (take j1 ℬs @ ℬs!j1 # drop (Suc j1) ℬs)" using split assms(1) by presburger
then have bsplit: "ℬ = mset (take j1 ℬs) + {#bl1#} + mset (drop (Suc j1) ℬs)" by (simp add: bl1eq)
then have btake: "ℬ - {#bl1#} = mset (take j1 ℬs) + mset (drop (Suc j1) ℬs)" by simp
thus ?thesis proof (cases "j2 < j1")
case True
then have "j2 < length (take j1 ℬs)" using lj1 by simp
then obtain bl2 where bl2eq: "bl2 = (take j1 ℬs) ! j2" by auto
then have bl2eq2: "bl2 = ℬs ! j2"
by (simp add: True)
then have "bl2 ∈# ℬ - {#bl1#}" using btake
by (metis bl2eq ‹j2 < length (take j1 ℬs)› nth_mem_mset union_iff)
then show ?thesis using bl2eq2 bl1in bl1eq that by auto
next
case False
then have j2gt: "j2 ≥ Suc j1" using assms by simp
then obtain i where ieq: "i = j2 - Suc j1"
by simp
then have j2eq: "j2 = (Suc j1) + i" using j2gt by presburger
have "length (drop (Suc j1) ℬs) = 𝖻 - (Suc j1)" using blocks_list_length by auto
then have "i < length (drop (Suc j1) ℬs)" using ieq assms blocks_list_length
using diff_less_mono j2gt by presburger
then obtain bl2 where bl2eq: "bl2 = (drop (Suc j1) ℬs) ! i" by auto
then have bl2in: "bl2 ∈# ℬ - {#bl1#}" using btake nth_mem_mset union_iff
by (metis ‹i < length (drop (Suc j1) ℬs)›)
then have "bl2 = ℬs ! j2" using bl2eq nth_drop blocks_list_length assms j2eq
by (metis Suc_leI)
then show ?thesis using bl1in bl1eq bl2in that by auto
qed
qed
lemma filter_size_blocks_eq_card_indexes: "size {# b ∈# ℬ . P b #} = card {j ∈ {..<(𝖻)}. P (ℬs ! j)}"
proof -
have "ℬ = image_mset (λ j . ℬs ! j) (mset_set {..<(𝖻)})"
using blocks_mset_image by simp
then have helper: "{# b ∈# ℬ . P b #} = image_mset (λ j . ℬs ! j) {# j ∈# (mset_set {..< 𝖻}). P (ℬs ! j) #} "
by (simp add: filter_mset_image_mset)
have "card {j ∈ {..<𝖻}. P (ℬs ! j)} = size {# j ∈# (mset_set {..< 𝖻}). P (ℬs ! j) #}"
using card_size_filter_eq [of "{..<𝖻}"] by simp
thus ?thesis using helper by simp
qed
lemma blocks_index_ne_belong:
assumes "i1 < length ℬs"
assumes "i2 < length ℬs"
assumes "i1 ≠ i2"
shows "ℬs ! i2 ∈# ℬ - {#(ℬs ! i1)#}"
proof (cases "ℬs ! i1 = ℬs ! i2")
case True
then have "count (mset ℬs) (ℬs ! i1) ≥ 2" using count_min_2_indices assms by fastforce
then have "count ((mset ℬs) - {#(ℬs ! i1)#}) (ℬs ! i1) ≥ 1"
by (metis Nat.le_diff_conv2 add_leD2 count_diff count_single nat_1_add_1)
then show ?thesis
by (metis True count_inI not_one_le_zero)
next
case False
have "ℬs ! i2 ∈# ℬ" using assms
by simp
then show ?thesis using False
by (metis in_remove1_mset_neq)
qed
lemma inter_num_points_filter_def:
assumes "j1 < 𝖻" "j2 < 𝖻" "j1 ≠ j2"
shows "card {x ∈ {0..<𝗏} . ((𝒱s ! x) ∈ (ℬs ! j1) ∧ (𝒱s ! x) ∈ (ℬs ! j2)) } = (ℬs ! j1) |∩| (ℬs ! j2)"
proof -
have inter: "⋀ v. v ∈ 𝒱 ⟹ v ∈ (ℬs ! j1) ∧ v ∈ (ℬs ! j2) ⟷ v ∈ (ℬs ! j1) ∩ (ℬs ! j2)"
by simp
obtain bl1 bl2 where bl1in: "bl1 ∈# ℬ" and bl1eq: "ℬs ! j1 = bl1" and bl2in: "bl2 ∈# ℬ - {#bl1#}"
and bl2eq: "ℬs ! j2 = bl2"
using assms obtains_two_diff_block_indexes
by (metis blocks_index_ne_belong size_mset valid_blocks_index)
have "card {x ∈ {0..<𝗏} . (𝒱s ! x) ∈ (ℬs ! j1) ∧ (𝒱s ! x) ∈ (ℬs ! j2) } =
card {v ∈ 𝒱 . v ∈ (ℬs ! j1) ∧ v ∈ (ℬs ! j2) }"
using card_filter_point_indices by simp
also have "... = card {v ∈ 𝒱 . v ∈ bl1 ∧ v ∈ bl2 }" using bl1eq bl2eq by simp
finally show ?thesis using points_inter_num_rep bl1in bl2in
by (simp add: bl1eq bl2eq)
qed
text ‹Define an incidence matrix for this ordering of an incidence system ›
abbreviation N :: "int mat" where
"N ≡ inc_mat_of 𝒱s ℬs"
sublocale zero_one_matrix_ring_1 "N"
using inc_mat_of_01_mat .
lemma N_alt_def_dim: "N = mat 𝗏 𝖻 (λ (i,j) . if (incident (𝒱s ! i) (ℬs ! j)) then 1 else 0) "
using incidence_cond_indexed inc_mat_of_def
by (intro eq_matI) (simp_all add: inc_mat_dim_row inc_mat_dim_col inc_matrix_point_in_block_one
inc_matrix_point_not_in_block_zero points_list_length)
text ‹Matrix Dimension related lemmas ›
lemma N_carrier_mat: "N ∈ carrier_mat 𝗏 𝖻"
by (simp add: N_alt_def_dim)
lemma dim_row_is_v[simp]: "dim_row N = 𝗏"
by (simp add: N_alt_def_dim)
lemma dim_col_is_b[simp]: "dim_col N = 𝖻"
by (simp add: N_alt_def_dim)
lemma dim_vec_row_N: "dim_vec (row N i) = 𝖻"
by (simp add: N_alt_def_dim)
lemma dim_vec_col_N: "dim_vec (col N i) = 𝗏" by simp
lemma dim_vec_N_col:
assumes "j < 𝖻"
shows "dim_vec (cols N ! j) = 𝗏"
proof -
have "cols N ! j = col N j" using assms dim_col_is_b by simp
then have "dim_vec (cols N ! j) = dim_vec (col N j)" by simp
thus ?thesis using dim_col assms by (simp)
qed
lemma N_carrier_mat_01_lift: "lift_01_mat N ∈ carrier_mat 𝗏 𝖻"
by auto
text ‹Transpose properties ›
lemma transpose_N_mult_dim: "dim_row (N * N⇧T) = 𝗏" "dim_col (N * N⇧T) = 𝗏"
by (simp_all)
lemma N_trans_index_val: "i < dim_col N ⟹ j < dim_row N ⟹
N⇧T $$ (i, j) = (if (𝒱s ! j) ∈ (ℬs ! i) then 1 else 0)"
by (simp add: inc_mat_of_def)
text ‹Matrix element and index related lemmas ›
lemma mat_row_elems: "i < 𝗏 ⟹ vec_set (row N i) ⊆ {0, 1}"
using points_list_length
by (simp add: row_elems_ss01)
lemma mat_col_elems: "j < 𝖻 ⟹ vec_set (col N j) ⊆ {0, 1}"
using blocks_list_length by (metis col_elems_ss01 dim_col_is_b)
lemma matrix_elems_one_zero: "i < 𝗏 ⟹ j < 𝖻 ⟹ N $$ (i, j) = 0 ∨ N $$ (i, j) = 1"
by (metis blocks_list_length inc_matrix_elems_one_zero points_list_length)
lemma matrix_point_in_block_one: "i < 𝗏 ⟹ j < 𝖻 ⟹ (𝒱s ! i)∈ (ℬs ! j) ⟹N $$ (i, j) = 1"
by (metis inc_matrix_point_in_block_one points_list_length blocks_list_length )
lemma matrix_point_not_in_block_zero: "i < 𝗏 ⟹ j < 𝖻 ⟹ 𝒱s ! i ∉ ℬs ! j ⟹ N $$ (i, j) = 0"
by(metis inc_matrix_point_not_in_block_zero points_list_length blocks_list_length)
lemma matrix_point_in_block: "i < 𝗏 ⟹ j < 𝖻 ⟹ N $$ (i, j) = 1 ⟹ 𝒱s ! i ∈ ℬs ! j"
by (metis blocks_list_length points_list_length inc_matrix_point_in_block)
lemma matrix_point_not_in_block: "i < 𝗏 ⟹ j < 𝖻 ⟹ N $$ (i, j) = 0 ⟹ 𝒱s ! i ∉ ℬs ! j"
by (metis blocks_list_length points_list_length inc_matrix_point_not_in_block)
lemma matrix_point_not_in_block_iff: "i < 𝗏 ⟹ j < 𝖻 ⟹ N $$ (i, j) = 0 ⟷ 𝒱s ! i ∉ ℬs ! j"
by (metis blocks_list_length points_list_length inc_matrix_point_not_in_block_iff)
lemma matrix_point_in_block_iff: "i < 𝗏 ⟹ j < 𝖻 ⟹ N $$ (i, j) = 1 ⟷ 𝒱s ! i ∈ ℬs ! j"
by (metis blocks_list_length points_list_length inc_matrix_point_in_block_iff)
lemma matrix_subset_implies_one: "I ⊆ {..< 𝗏} ⟹ j < 𝖻 ⟹ (!) 𝒱s ` I ⊆ ℬs ! j ⟹ i ∈ I ⟹
N $$ (i, j) = 1"
by (metis blocks_list_length points_list_length inc_matrix_subset_implies_one)
lemma matrix_one_implies_membership:
"I ⊆ {..< 𝗏} ⟹ j < size ℬ ⟹ ∀i∈I. N $$ (i, j) = 1 ⟹ i ∈ I ⟹ 𝒱s ! i ∈ ℬs ! j"
by (simp add: matrix_point_in_block_iff subset_iff)
text ‹Incidence Vector's of Incidence Matrix columns ›
lemma col_inc_vec_of: "j < length ℬs ⟹ inc_vec_of 𝒱s (ℬs ! j) = col N j"
by (simp add: inc_mat_col_inc_vec)
lemma inc_vec_eq_iff_blocks:
assumes "bl ∈# ℬ"
assumes "bl' ∈# ℬ"
shows "inc_vec_of 𝒱s bl = inc_vec_of 𝒱s bl' ⟷ bl = bl'"
proof (intro iffI eq_vecI, simp_all add: inc_vec_dim assms)
define v1 :: "'c :: {ring_1} vec" where "v1 = inc_vec_of 𝒱s bl"
define v2 :: "'c :: {ring_1} vec" where "v2 = inc_vec_of 𝒱s bl'"
assume a: "v1 = v2"
then have "dim_vec v1 = dim_vec v2"
by (simp add: inc_vec_dim)
then have "⋀ i. i < dim_vec v1 ⟹ v1 $ i = v2 $ i" using a by simp
then have "⋀ i. i < length 𝒱s ⟹ v1 $ i = v2 $ i" by (simp add: v1_def inc_vec_dim)
then have "⋀ i. i < length 𝒱s ⟹ (𝒱s ! i) ∈ bl ⟷ (𝒱s ! i) ∈ bl'"
using inc_vec_index_one_iff v1_def v2_def by metis
then have "⋀ x. x ∈ 𝒱 ⟹ x ∈ bl ⟷ x ∈ bl'"
using points_list_length valid_points_index_cons by auto
then show "bl = bl'" using wellformed assms
by (meson subset_antisym subset_eq)
qed
text ‹Incidence matrix column properties›
lemma N_col_def: "j < 𝖻 ⟹ i < 𝗏 ⟹ (col N j) $ i = (if (𝒱s ! i ∈ ℬs ! j) then 1 else 0)"
by (metis inc_mat_col_def points_list_length blocks_list_length)
lemma N_col_def_indiv: "j < 𝖻 ⟹ i < 𝗏 ⟹ 𝒱s ! i ∈ ℬs ! j ⟹ (col N j) $ i = 1"
"j < 𝖻 ⟹ i < 𝗏 ⟹ 𝒱s ! i ∉ ℬs ! j ⟹ (col N j) $ i = 0"
by(simp_all add: inc_matrix_point_in_block_one inc_matrix_point_not_in_block_zero points_list_length)
lemma N_col_list_map_elem: "j < 𝖻 ⟹ i < 𝗏 ⟹
col N j $ i = map_vec (λ x . if (x ∈ (ℬs ! j)) then 1 else 0) (vec_of_list 𝒱s) $ i"
by (metis inc_mat_col_list_map_elem points_list_length blocks_list_length)
lemma N_col_list_map: "j < 𝖻 ⟹ col N j = map_vec (λ x . if (x ∈ (ℬs ! j)) then 1 else 0) (vec_of_list 𝒱s)"
by (metis inc_mat_col_list_map blocks_list_length)
lemma N_col_mset_point_set_img: "j < 𝖻 ⟹
vec_mset (col N j) = image_mset (λ x. if (x ∈ (ℬs ! j)) then 1 else 0) (mset_set 𝒱)"
using vec_mset_img_map N_col_list_map points_indexing
by (metis (no_types, lifting) finite_sets permutations_of_multisetD permutations_of_set_altdef)
lemma matrix_col_to_block:
assumes "j < 𝖻"
shows "ℬs ! j = (λ k . 𝒱s ! k) ` {i ∈ {..< 𝗏} . (col N j) $ i = 1}"
proof (intro subset_antisym subsetI)
fix x assume assm1: "x ∈ ℬs ! j"
then have "x ∈ 𝒱" using wellformed assms valid_blocks_index by blast
then obtain i where vs: "𝒱s ! i = x" and "i < 𝗏"
using valid_points_index_cons by auto
then have inset: "i ∈ {..< 𝗏}"
by fastforce
then have "col N j $ i = 1" using assm1 N_col_def assms vs
using ‹i < 𝗏› by presburger
then have "i ∈ {i. i ∈ {..< 𝗏} ∧ col N j $ i = 1}"
using inset by blast
then show "x ∈ (!) 𝒱s ` {i. i ∈ {..<𝗏} ∧ col N j $ i = 1}" using vs by blast
next
fix x assume assm2: "x ∈ ((λ k . 𝒱s ! k) ` {i ∈ {..< 𝗏} . col N j $ i = 1})"
then obtain k where "x = 𝒱s !k" and inner: "k ∈{i ∈ {..< 𝗏} . col N j $ i = 1}"
by blast
then have ilt: "k < 𝗏" by auto
then have "N $$ (k, j) = 1" using inner
by (metis (mono_tags) N_col_def assms matrix_point_in_block_iff matrix_point_not_in_block_zero mem_Collect_eq)
then show "x ∈ ℬs ! j" using ilt
using ‹x = 𝒱s ! k› assms matrix_point_in_block_iff by blast
qed
lemma matrix_col_to_block_v2: "j < 𝖻 ⟹ ℬs ! j = (λ k . 𝒱s ! k) ` map_col_to_block (col N j)"
using matrix_col_to_block map_col_to_block_def by fastforce
lemma matrix_col_in_blocks: "j < 𝖻 ⟹ (!) 𝒱s ` map_col_to_block (col N j) ∈# ℬ"
using matrix_col_to_block_v2 by (metis (no_types, lifting) valid_blocks_index)
lemma inc_matrix_col_block:
assumes "c ∈ set (cols N)"
shows "(λ x. 𝒱s ! x) ` (map_col_to_block c) ∈# ℬ"
proof -
obtain j where "c = col N j" and "j < 𝖻" using assms cols_length cols_nth in_mset_conv_nth
ordered_incidence_system_axioms set_mset_mset by (metis dim_col_is_b)
thus ?thesis
using matrix_col_in_blocks by blast
qed
text ‹ Incidence Matrix Row Definitions ›
lemma N_row_def: "j < 𝖻 ⟹ i < 𝗏 ⟹ (row N i) $ j = (if (𝒱s ! i ∈ ℬs ! j) then 1 else 0)"
by (metis inc_mat_row_def points_list_length blocks_list_length)
lemma N_row_list_map_elem: "j < 𝖻 ⟹ i < 𝗏 ⟹
row N i $ j = map_vec (λ bl . if ((𝒱s ! i) ∈ bl) then 1 else 0) (vec_of_list ℬs) $ j"
by (metis inc_mat_row_list_map_elem points_list_length blocks_list_length)
lemma N_row_list_map: "i < 𝗏 ⟹
row N i = map_vec (λ bl . if ((𝒱s ! i) ∈ bl) then 1 else 0) (vec_of_list ℬs)"
by (simp add: inc_mat_row_list_map points_list_length blocks_list_length)
lemma N_row_mset_blocks_img: "i < 𝗏 ⟹
vec_mset (row N i) = image_mset (λ x . if ((𝒱s ! i) ∈ x) then 1 else 0) ℬ"
using vec_mset_img_map N_row_list_map by metis
text ‹Alternate Block representations ›
lemma block_mat_cond_rep:
assumes "j < length ℬs"
shows "(ℬs ! j) = {𝒱s ! i | i. i < length 𝒱s ∧ N $$ (i, j) = 1}"
proof -
have cond: "⋀ i. i < length 𝒱s ∧ N $$ (i, j) = 1 ⟷i ∈ {..< 𝗏} ∧ (col N j) $ i = 1"
using assms points_list_length by auto
have "(ℬs ! j) = (λ k . 𝒱s ! k) ` {i ∈ {..< 𝗏} . (col N j) $ i = 1}"
using matrix_col_to_block assms by simp
also have "... = {𝒱s ! i | i. i ∈ {..< 𝗏} ∧ (col N j) $ i = 1}" by auto
finally show "(ℬs ! j) = {𝒱s ! i | i. i < length 𝒱s ∧ N $$ (i, j) = 1}"
using Collect_cong cond by auto
qed
lemma block_mat_cond_rep': "j < length ℬs ⟹ (ℬs ! j) = ((!) 𝒱s) ` {i . i < length 𝒱s ∧ N $$ (i, j) = 1}"
by (simp add: block_mat_cond_rep setcompr_eq_image)
lemma block_mat_cond_rev:
assumes "j < length ℬs"
shows "{i . i < length 𝒱s ∧ N $$ (i, j) = 1} = ((List_Index.index) 𝒱s) ` (ℬs ! j)"
proof (intro Set.set_eqI iffI)
fix i assume a1: "i ∈ {i. i < length 𝒱s ∧ N $$ (i, j) = 1}"
then have ilt1: "i < length 𝒱s" and Ni1: "N $$ (i, j) = 1" by auto
then obtain x where "𝒱s ! i = x" and "x ∈ (ℬs ! j)"
using assms inc_matrix_point_in_block by blast
then have "List_Index.index 𝒱s x = i" using distinct index_nth_id ilt1 by auto
then show "i ∈ List_Index.index 𝒱s ` ℬs ! j" by (metis ‹x ∈ ℬs ! j› imageI)
next
fix i assume a2: "i ∈ List_Index.index 𝒱s ` ℬs ! j"
then obtain x where ieq: "i = List_Index.index 𝒱s x" and xin: "x ∈ ℬs !j"
by blast
then have ilt: "i < length 𝒱s"
by (smt (z3) assms index_first index_le_size nat_less_le nth_mem_mset points_list_length
valid_points_index_cons wf_invalid_point)
then have "N $$ (i, j) = 1" using xin inc_matrix_point_in_block_one
by (metis ieq assms index_conv_size_if_notin less_irrefl_nat nth_index)
then show "i ∈ {i. i < length 𝒱s ∧ N $$ (i, j) = 1}" using ilt by simp
qed
text ‹Incidence Matrix incidence system properties ›
lemma incomplete_block_col:
assumes "j < 𝖻"
assumes "incomplete_block (ℬs ! j)"
shows "0 ∈$ (col N j)"
proof -
obtain x where "x ∈ 𝒱" and "x ∉ (ℬs ! j)"
by (metis Diff_iff assms(2) incomplete_block_proper_subset psubset_imp_ex_mem)
then obtain i where "𝒱s ! i = x" and "i< 𝗏"
using valid_points_index_cons by blast
then have "N $$ (i, j) = 0"
using ‹x ∉ ℬs ! j› assms(1) matrix_point_not_in_block_zero by blast
then have "col N j $ i = 0"
using N_col_def ‹𝒱s ! i = x› ‹i < 𝗏› ‹x ∉ ℬs ! j› assms(1) by fastforce
thus ?thesis using vec_setI
by (smt (z3) ‹i < 𝗏› dim_col dim_row_is_v)
qed
lemma mat_rep_num_N_row:
assumes "i < 𝗏"
shows "mat_rep_num N i = ℬ rep (𝒱s ! i)"
proof -
have "count (image_mset (λ x . if ((𝒱s ! i) ∈ x) then 1 else (0 :: int )) ℬ) 1 =
size (filter_mset (λ x . (𝒱s ! i) ∈ x) ℬ)"
using count_mset_split_image_filter[of "ℬ" "1" "λ x . (0 :: int)" "λ x . (𝒱s ! i) ∈ x"] by simp
then have "count (image_mset (λ x . if ((𝒱s ! i) ∈ x) then 1 else (0 :: int )) ℬ) 1
= ℬ rep (𝒱s ! i)" by (simp add: point_rep_number_alt_def)
thus ?thesis using N_row_mset_blocks_img assms
by (simp add: mat_rep_num_def)
qed
lemma point_rep_mat_row_sum: "i < 𝗏 ⟹ sum_vec (row N i) = ℬ rep (𝒱s ! i)"
using count_vec_sum_ones_alt mat_rep_num_N_row mat_row_elems mat_rep_num_def by metis
lemma mat_block_size_N_col:
assumes "j < 𝖻"
shows "mat_block_size N j = card (ℬs ! j)"
proof -
have val_b: "ℬs ! j ∈# ℬ" using assms valid_blocks_index by auto
have "⋀ x. x ∈# mset_set 𝒱 ⟹ (λx . (0 :: int)) x ≠ 1" using zero_neq_one by simp
then have "count (image_mset (λ x. if (x ∈ (ℬs ! j)) then 1 else (0 :: int)) (mset_set 𝒱)) 1 =
size (filter_mset (λ x . x ∈ (ℬs ! j)) (mset_set 𝒱))"
using count_mset_split_image_filter [of "mset_set 𝒱" "1" "(λ x . (0 :: int))" "λ x . x ∈ ℬs ! j"]
by simp
then have "count (image_mset (λ x. if (x ∈ (ℬs ! j)) then 1 else (0 :: int)) (mset_set 𝒱)) 1 = card (ℬs ! j)"
using val_b block_size_alt by (simp add: finite_sets)
thus ?thesis using N_col_mset_point_set_img assms mat_block_size_def by metis
qed
lemma block_size_mat_rep_sum: "j < 𝖻 ⟹ sum_vec (col N j) = mat_block_size N j"
using count_vec_sum_ones_alt mat_block_size_N_col mat_block_size_def by (metis mat_col_elems)
lemma mat_point_index_rep:
assumes "I ⊆ {..<𝗏}"
shows "mat_point_index N I = ℬ index ((λ i. 𝒱s ! i) ` I)"
proof -
have "⋀ i . i ∈ I ⟹ 𝒱s ! i ∈ 𝒱" using assms valid_points_index by auto
then have eqP: "⋀ j. j < dim_col N ⟹ ((λ i. 𝒱s ! i) ` I) ⊆ (ℬs ! j) ⟷ (∀ i ∈ I . N $$ (i, j) = 1)"
proof (intro iffI subsetI, simp_all)
show "⋀j i. j < length ℬs ⟹ (⋀i. i ∈ I ⟹ 𝒱s ! i ∈ 𝒱) ⟹ (!) 𝒱s ` I ⊆ ℬs ! j ⟹
∀i∈I. N $$ (i, j) = 1"
using matrix_subset_implies_one assms by simp
have "⋀x. x∈ (!) 𝒱s ` I ⟹ ∃ i ∈ I. 𝒱s ! i = x"
by auto
then show "⋀j x. j < length ℬs ⟹ ∀i∈I. N $$ (i, j) = 1 ⟹ x ∈ (!) 𝒱s ` I
⟹ (⋀i. i ∈ I ⟹ 𝒱s ! i ∈ 𝒱) ⟹ x ∈ ℬs ! j"
using assms matrix_one_implies_membership by (metis blocks_list_length)
qed
have "card {j . j < dim_col N ∧ (∀ i ∈ I . N $$(i, j) = 1)} =
card {j . j < dim_col N ∧ ((λ i . 𝒱s ! i) ` I) ⊆ ℬs ! j}"
using eqP by (metis (mono_tags, lifting))
also have "... = size {# b ∈# ℬ . ((λ i . 𝒱s ! i) ` I) ⊆ b #}"
using filter_size_blocks_eq_card_indexes by auto
also have "... = points_index ℬ ((λ i . 𝒱s ! i) ` I)"
by (simp add: points_index_def)
finally have "card {j . j < dim_col N ∧ (∀ i ∈ I . N $$(i, j) = 1)} = ℬ