# Theory Incidence_Matrices

(* Author: Chelsea Edmonds
Theory: Incidence_Matrices.thy
*)

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

lemma inc_vec_dim: "dim_vec (inc_vec_of Vs bl) = length Vs"

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"

lemma in_map_col_valid_index: "i ∈ map_col_to_block c ⟹ i < dim_vec c"

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)"
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
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)"
finally have "card {j . j < dim_col N ∧ (∀ i ∈ I . N (i, j) = 1)} = ℬ `