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 
      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)} = ℬ index ((λ i . 𝒱s ! i) ` I)"
    by blast
  thus ?thesis unfolding mat_point_index_def by simp
qed

lemma incidence_mat_two_index: "i1 < 𝗏 ⟹ i2 < 𝗏 ⟹ 
    mat_point_index N {i1, i2} = ℬ index {𝒱s ! i1, 𝒱s ! i2}"
  using mat_point_index_two_alt[of  i1 N i2 ] mat_point_index_rep[of "{i1, i2}"] dim_row_is_v
  by (metis (no_types, lifting) empty_subsetI image_empty image_insert insert_subset lessThan_iff) 

lemma ones_incidence_mat_block_size: 
  assumes "j < 𝖻"
  shows "((u⇩v 𝗏) ⇩v* N) $ j = mat_block_size N j"
proof - 
  have "dim_vec ((u⇩v 𝗏) ⇩v* N) = 𝖻" by (simp) 
  then have "((u⇩v 𝗏) ⇩v* N) $ j = (u⇩v 𝗏) ∙ col N j" using assms by simp 
  also have "... = (∑ i ∈ {0 ..< 𝗏}. (u⇩v 𝗏) $ i * (col N j) $ i)" 
    by (simp add: scalar_prod_def)
  also have "... = sum_vec (col N j)" using dim_row_is_v by (simp add: sum_vec_def)
  finally show ?thesis  using block_size_mat_rep_sum assms by simp
qed

lemma mat_block_size_conv:  "j < dim_col N ⟹ card (ℬs ! j) = mat_block_size N j"
  by (simp add: mat_block_size_N_col)

lemma mat_inter_num_conv: 
  assumes "j1 < dim_col N" "j2 < dim_col N"
  shows "(ℬs ! j1) |∩| (ℬs ! j2) = mat_inter_num N j1 j2"
proof -
  have eq_sets: "⋀ P. (λ i . 𝒱s ! i) ` {i ∈ {0..<𝗏}. P (𝒱s ! i)} = {x ∈ 𝒱 . P x}"
    by (metis Compr_image_eq lessThan_atLeast0 points_set_index_img)
  have bin: "ℬs ! j1 ∈# ℬ" "ℬs ! j2 ∈# ℬ" using assms dim_col_is_b by simp_all
  have "(ℬs ! j1) |∩| (ℬs ! j2) = card ((ℬs ! j1) ∩ (ℬs ! j2))" 
    by (simp add: intersection_number_def)
  also have "... = card {x . x ∈ (ℬs ! j1) ∧ x ∈ (ℬs ! j2)}"
    by (simp add: Int_def) 
  also have "... = card {x ∈ 𝒱. x ∈ (ℬs ! j1) ∧ x ∈ (ℬs ! j2)}" using wellformed bin
    by (meson wf_invalid_point) 
  also have "... = card ((λ i . 𝒱s ! i) ` {i ∈ {0..<𝗏}. (𝒱s ! i) ∈ (ℬs ! j1) ∧ (𝒱s ! i) ∈ (ℬs ! j2)})" 
    using eq_sets[of "λ x. x ∈ (ℬs ! j1) ∧ x ∈ (ℬs ! j2)"] by simp
  also have "... = card ({i ∈ {0..<𝗏}. (𝒱s ! i) ∈ (ℬs ! j1) ∧ (𝒱s ! i) ∈ (ℬs ! j2)})"
    using points_indexing_inj card_image
    by (metis (no_types, lifting) lessThan_atLeast0 lessThan_iff mem_Collect_eq points_list_length) 
  also have "... = card ({i . i < 𝗏 ∧ (𝒱s ! i) ∈ (ℬs ! j1) ∧ (𝒱s ! i) ∈ (ℬs ! j2)})" by auto
  also have "... = card ({i . i < 𝗏 ∧ N $$ (i, j1) = 1 ∧ N $$ (i, j2) = 1})" using assms
    by (metis (no_types, opaque_lifting) inc_mat_dim_col inc_matrix_point_in_block_iff points_list_length) 
  finally have "(ℬs ! j1) |∩| (ℬs ! j2) = card {i . i < dim_row N ∧ N $$ (i, j1) = 1 ∧ N $$ (i, j2) = 1}"
    using dim_row_is_v by presburger
  thus ?thesis using assms by (simp add: mat_inter_num_def)
qed

lemma non_empty_col_map_conv: 
  assumes "j < dim_col N"
  shows "non_empty_col N j ⟷ ℬs ! j ≠ {}"
proof (intro iffI)
  assume "non_empty_col N j"
  then obtain i where ilt: "i < dim_row N" and "(col N j) $ i ≠ 0"
    using non_empty_col_obtains assms by blast
  then have "(col N j) $ i = 1"
    using assms
    by (metis N_col_def_indiv(1) N_col_def_indiv(2) dim_col_is_b dim_row_is_v) 
  then have "𝒱s ! i ∈ ℬs ! j"
    by (smt (verit, best) assms ilt inc_mat_col_def dim_col_is_b inc_mat_dim_col inc_mat_dim_row) 
  thus "ℬs ! j ≠ {}" by blast
next
  assume a: "ℬs ! j ≠ {}"
  have "ℬs ! j ∈# ℬ" using assms dim_col_is_b by simp
  then obtain x where "x ∈ ℬs ! j" and "x ∈ 𝒱" using wellformed a by auto
  then obtain i where "𝒱s ! i ∈ ℬs ! j" and "i < dim_row N" using dim_row_is_v
    using valid_points_index_cons by auto 
  then have "N $$ (i, j) = 1"
    using assms by (meson inc_mat_of_index)  
  then show "non_empty_col N j" using non_empty_col_alt_def
    using ‹i < dim_row N› assms by fastforce 
qed

lemma scalar_prod_inc_vec_inter_num: 
  assumes "j1 < 𝖻" "j2 < 𝖻"
  shows "(col N j1) ∙ (col N j2) = (ℬs ! j1) |∩| (ℬs ! j2)"
  using scalar_prod_inc_vec_mat_inter_num assms N_carrier_mat
  by (simp add: mat_inter_num_conv)

lemma scalar_prod_block_size_lift_01: 
  assumes "i < 𝖻"
  shows "((col (lift_01_mat N) i) ∙ (col (lift_01_mat N) i)) = (of_nat (card (ℬs ! i)) :: ('b :: {ring_1}))"
proof -
  interpret z1: zero_one_matrix_ring_1 "(lift_01_mat N)"
    by (intro_locales) (simp add: lift_mat_is_0_1)
  show ?thesis using assms z1.scalar_prod_inc_vec_block_size_mat preserve_mat_block_size 
      mat_block_size_N_col lift_01_mat_def
    by (metis inc_mat_dim_col lift_01_mat_simp(2) of_inj_on_01_hom.inj_on_01_hom_axioms size_mset)
qed

lemma scalar_prod_inter_num_lift_01: 
  assumes "j1 < 𝖻" "j2 < 𝖻"
  shows "((col (lift_01_mat N) j1) ∙ (col (lift_01_mat N) j2)) = (of_nat ((ℬs ! j1) |∩| (ℬs ! j2)) :: ('b :: {ring_1}))"
proof -
  interpret z1: zero_one_matrix_ring_1 "(lift_01_mat N)"
    by (intro_locales) (simp add: lift_mat_is_0_1)
  show ?thesis using assms z1.scalar_prod_inc_vec_mat_inter_num preserve_mat_inter_num 
    mat_inter_num_conv lift_01_mat_def blocks_list_length inc_mat_dim_col
    by (metis  lift_01_mat_simp(2) of_inj_on_01_hom.inj_on_01_hom_axioms)
qed

text ‹ The System complement's incidence matrix flips 0's and 1's ›

lemma map_block_complement_entry: "j < 𝖻 ⟹ (map block_complement ℬs) ! j = block_complement (ℬs ! j)"
  using blocks_list_length by (metis nth_map) 

lemma complement_mat_entries: 
  assumes "i < 𝗏" and "j < 𝖻"
  shows "(𝒱s ! i ∉ ℬs ! j) ⟷ (𝒱s ! i ∈ (map block_complement ℬs) ! j)"
  using assms block_complement_def map_block_complement_entry valid_points_index by simp

lemma length_blocks_complement: "length (map block_complement ℬs) = 𝖻"
  by auto 

lemma ordered_complement: "ordered_incidence_system 𝒱s (map block_complement ℬs)"
proof -
  interpret inc: finite_incidence_system 𝒱 "complement_blocks"
    by (simp add: complement_finite)
  have "map inc.block_complement ℬs ∈ permutations_of_multiset complement_blocks"
    using complement_image by (simp add: permutations_of_multiset_def)
  then show ?thesis using ordered_incidence_sysI[of "𝒱" "complement_blocks" "𝒱s" "(map block_complement ℬs)"]
    by (simp add: inc.finite_incidence_system_axioms points_indexing) 
qed

interpretation ordered_comp: ordered_incidence_system "𝒱s" "(map block_complement ℬs)"
  using ordered_complement by simp

lemma complement_mat_entries_val: 
  assumes "i < 𝗏" and "j < 𝖻"
  shows "ordered_comp.N $$ (i, j) = (if 𝒱s ! i ∈ ℬs ! j then 0 else 1)"
proof -
  have cond: "(𝒱s ! i ∉ ℬs ! j) ⟷ (𝒱s ! i ∈ (map block_complement ℬs) ! j)"
    using complement_mat_entries assms by simp
  then have "ordered_comp.N $$ (i, j) = (if (𝒱s ! i ∈ (map block_complement ℬs) ! j) then 1 else 0)"
    using assms ordered_comp.matrix_point_in_block_one ordered_comp.matrix_point_not_in_block_iff 
    by force 
  then show ?thesis using cond by simp
qed

lemma ordered_complement_mat: "ordered_comp.N = mat 𝗏 𝖻 (λ (i,j) . if (𝒱s ! i) ∈ (ℬs ! j) then 0 else 1)"
  using complement_mat_entries_val by (intro eq_matI, simp_all)

lemma ordered_complement_mat_map: "ordered_comp.N = map_mat (λx. if x = 1 then 0 else 1) N"
  apply (intro eq_matI, simp_all)
  using ordered_incidence_system.matrix_point_in_block_iff ordered_incidence_system_axioms 
    complement_mat_entries_val by (metis blocks_list_length) 


end

text ‹Establishing connection between incidence system and ordered incidence system locale ›

lemma (in incidence_system) alt_ordering_sysI: "Vs ∈ permutations_of_set 𝒱 ⟹ Bs ∈ permutations_of_multiset ℬ ⟹ 
    ordered_incidence_system Vs Bs"
  by (unfold_locales) (simp_all add: permutations_of_multisetD permutations_of_setD wellformed)

lemma (in finite_incidence_system) exists_ordering_sysI: "∃ Vs Bs . Vs ∈ permutations_of_set 𝒱 ∧ 
  Bs ∈ permutations_of_multiset ℬ ∧ ordered_incidence_system Vs Bs"
proof -
  obtain Vs where "Vs ∈ permutations_of_set 𝒱"
    by (meson all_not_in_conv finite_sets permutations_of_set_empty_iff) 
  obtain Bs where "Bs ∈ permutations_of_multiset ℬ"
    by (meson all_not_in_conv permutations_of_multiset_not_empty) 
  then show ?thesis using alt_ordering_sysI ‹Vs ∈ permutations_of_set 𝒱› by blast 
qed

lemma inc_sys_orderedI: 
  assumes "incidence_system V B" and "distinct Vs" and "set Vs = V" and "mset Bs = B" 
  shows "ordered_incidence_system Vs Bs"
proof -
  interpret inc: incidence_system V B using assms by simp
  show ?thesis proof (unfold_locales)
    show "⋀b. b ∈# mset Bs ⟹ b ⊆ set Vs" using inc.wellformed assms by simp
    show "distinct Vs" using assms(2)permutations_of_setD(2) by auto 
  qed
qed

text ‹Generalise the idea of an incidence matrix to an unordered context ›

definition is_incidence_matrix :: "'c :: {ring_1} mat ⇒ 'a set ⇒ 'a set multiset ⇒ bool" where
"is_incidence_matrix N V B ⟷ 
  (∃ Vs Bs . (Vs ∈ permutations_of_set V ∧ Bs ∈ permutations_of_multiset B ∧ N = (inc_mat_of Vs Bs)))"

lemma (in incidence_system) is_incidence_mat_alt: "is_incidence_matrix N 𝒱 ℬ ⟷ 
  (∃ Vs Bs. (set Vs = 𝒱 ∧ mset Bs = ℬ ∧ ordered_incidence_system Vs Bs ∧ N = (inc_mat_of Vs Bs)))"
proof (intro iffI, simp add: is_incidence_matrix_def)
  assume "∃Vs. Vs ∈ permutations_of_set 𝒱 ∧ (∃Bs. Bs ∈ permutations_of_multiset ℬ ∧ N = inc_mat_of Vs Bs)"
  then obtain Vs Bs where "Vs ∈ permutations_of_set 𝒱 ∧ Bs ∈ permutations_of_multiset ℬ ∧ N = inc_mat_of Vs Bs"
    by auto
  then show "∃Vs. set Vs = 𝒱 ∧ (∃Bs. mset Bs = ℬ ∧ ordered_incidence_system Vs Bs ∧ N = inc_mat_of Vs Bs)"
    using incidence_system.alt_ordering_sysI incidence_system_axioms permutations_of_multisetD permutations_of_setD(1) 
    by blast 
next
  assume "∃Vs Bs. set Vs = 𝒱 ∧ mset Bs = ℬ ∧ ordered_incidence_system Vs Bs ∧ N = inc_mat_of Vs Bs"
  then obtain Vs Bs where s: "set Vs = 𝒱" and ms: "mset Bs = ℬ" and "ordered_incidence_system Vs Bs" 
    and n: "N = inc_mat_of Vs Bs" by auto 
  then interpret ois: ordered_incidence_system Vs Bs by simp 
  have vs: "Vs ∈ permutations_of_set 𝒱"
    using ois.points_indexing s by blast 
  have "Bs ∈ permutations_of_multiset ℬ" using ois.blocks_indexing ms by blast
  then show "is_incidence_matrix N 𝒱 ℬ " using n vs
    using is_incidence_matrix_def by blast 
qed

lemma (in ordered_incidence_system) is_incidence_mat_true: "is_incidence_matrix N 𝒱 ℬ = True"
  using blocks_indexing is_incidence_matrix_def points_indexing by blast

subsection‹Incidence Matrices on Design Subtypes ›

locale ordered_design = ordered_incidence_system 𝒱s ℬs + design "set 𝒱s" "mset ℬs" 
  for 𝒱s and ℬs
begin

lemma incidence_mat_non_empty_blocks: 
  assumes "j < 𝖻"
  shows "1 ∈$ (col N j)" 
proof -
  obtain bl where isbl: "ℬs ! j = bl" by simp
  then have "bl ∈# ℬ"
    using assms valid_blocks_index by auto 
  then obtain x where inbl: "x ∈ bl"
    using blocks_nempty by blast
  then obtain i where isx: "𝒱s ! i = x" and vali: "i < 𝗏"
    using ‹bl ∈# ℬ› valid_points_index_cons wf_invalid_point by blast
  then have "N $$ (i, j) = 1"
    using ‹ℬs ! j = bl› ‹x ∈ bl› assms matrix_point_in_block_one by blast
  thus ?thesis using vec_setI
    by (smt (verit, ccfv_SIG) N_col_def isx vali isbl inbl assms dim_vec_col_N of_nat_less_imp_less) 
qed

lemma all_cols_non_empty: "j < dim_col N ⟹ non_empty_col N j"
  using blocks_nempty non_empty_col_map_conv dim_col_is_b by simp 
end

locale ordered_simple_design = ordered_design 𝒱s ℬs + simple_design "(set 𝒱s)" "mset ℬs" for 𝒱s ℬs
begin

lemma block_list_distinct: "distinct ℬs"
  using block_mset_distinct by auto
  
lemma distinct_cols_N: "distinct (cols N)"
proof -
  have "inj_on (λ bl . inc_vec_of 𝒱s bl) (set ℬs)" using inc_vec_eq_iff_blocks 
    by (simp add: inc_vec_eq_iff_blocks inj_on_def) 
  then show ?thesis using distinct_map inc_mat_of_cols_inc_vecs block_list_distinct
    by (simp add: distinct_map inc_mat_of_cols_inc_vecs ) 
qed

lemma simp_blocks_length_card: "length ℬs = card (set ℬs)"
  using design_support_def simple_block_size_eq_card by fastforce

lemma blocks_index_inj_on: "inj_on (λ i . ℬs ! i) {0..<length ℬs}"
  by (auto simp add: inj_on_def) (metis simp_blocks_length_card card_distinct nth_eq_iff_index_eq)

lemma x_in_block_set_img: assumes "x ∈ set ℬs" shows "x ∈ (!) ℬs ` {0..<length ℬs}"
proof -
  obtain i where "ℬs ! i = x" and "i < length ℬs" using assms
    by (meson in_set_conv_nth) 
  thus ?thesis by auto
qed

lemma blocks_index_simp_bij_betw: "bij_betw (λ i . ℬs ! i) {0..<length ℬs} (set ℬs)"
  using blocks_index_inj_on x_in_block_set_img by (auto simp add: bij_betw_def) 

lemma blocks_index_simp_unique:  "i1 < length ℬs ⟹ i2 < length ℬs ⟹ i1 ≠ i2 ⟹ ℬs ! i1 ≠ ℬs ! i2"
  using block_list_distinct nth_eq_iff_index_eq by blast 

lemma lift_01_distinct_cols_N: "distinct (cols (lift_01_mat N))"
  using  lift_01_mat_distinct_cols distinct_cols_N by simp

end

locale ordered_proper_design = ordered_design 𝒱s ℬs + proper_design "set 𝒱s" "mset ℬs" 
  for 𝒱s and ℬs
begin

lemma mat_is_proper: "proper_inc_mat N"
  using design_blocks_nempty v_non_zero 
  by (auto simp add: proper_inc_mat_def)

end

locale ordered_constant_rep = ordered_proper_design 𝒱s ℬs + constant_rep_design "set 𝒱s" "mset ℬs" 𝗋 
  for 𝒱s and ℬs and 𝗋

begin

lemma incidence_mat_rep_num: "i < 𝗏 ⟹ mat_rep_num N i = 𝗋"
  using mat_rep_num_N_row rep_number valid_points_index by simp 

lemma incidence_mat_rep_num_sum: "i < 𝗏 ⟹ sum_vec (row N i) = 𝗋"
  using incidence_mat_rep_num  mat_rep_num_N_row
  by (simp add: point_rep_mat_row_sum)  

lemma transpose_N_mult_diag: 
  assumes "i = j" and "i < 𝗏" and "j < 𝗏" 
  shows "(N * N⇧T) $$ (i, j) = 𝗋"
proof -
  have unsq: "⋀ k . k < 𝖻 ⟹ (N $$ (i, k))^2 = N $$ (i, k)"
    using assms(2) matrix_elems_one_zero by fastforce
  then have "(N * N⇧T) $$ (i, j) = (∑k ∈{0..<𝖻} . N $$ (i, k) * N $$ (j, k))"
    using assms(2) assms(3) transpose_mat_mult_entries[of "i" "N" "j"] by (simp) 
  also have "... = (∑k ∈{0..<𝖻} . (N $$ (i, k))^2)" using assms(1)
    by (simp add: power2_eq_square)
  also have "... = (∑k ∈{0..<𝖻} . N $$ (i, k))"
    by (meson atLeastLessThan_iff sum.cong unsq) 
  also have "... = (∑k ∈{0..<𝖻} . (row N i) $ k)"
    using assms(2) dim_col_is_b dim_row_is_v by auto 
  finally have "(N * N⇧T) $$ (i, j) = sum_vec (row N i)"
    by (simp add: sum_vec_def)
  thus ?thesis using incidence_mat_rep_num_sum
    using assms(2) by presburger 
qed

end

locale ordered_block_design = ordered_proper_design 𝒱s ℬs + block_design "set 𝒱s" "mset ℬs" 𝗄
  for 𝒱s and ℬs and 𝗄

begin 

(* Every col has k ones *)
lemma incidence_mat_block_size: "j < 𝖻 ⟹ mat_block_size N j = 𝗄"
  using mat_block_size_N_col uniform valid_blocks_index by fastforce

lemma incidence_mat_block_size_sum: "j < 𝖻 ⟹ sum_vec (col N j) = 𝗄"
  using incidence_mat_block_size block_size_mat_rep_sum by presburger 

lemma ones_mult_incidence_mat_k_index: "j < 𝖻 ⟹ ((u⇩v 𝗏) ⇩v* N) $ j = 𝗄"
  using ones_incidence_mat_block_size uniform incidence_mat_block_size by blast 

lemma ones_mult_incidence_mat_k: "((u⇩v 𝗏) ⇩v* N) = 𝗄 ⋅⇩v (u⇩v 𝖻)"
  using ones_mult_incidence_mat_k_index dim_col_is_b by (intro eq_vecI) (simp_all)

end

locale ordered_incomplete_design = ordered_block_design 𝒱s ℬs 𝗄 + incomplete_design 𝒱 ℬ 𝗄
  for 𝒱s and ℬs and 𝗄

begin 

lemma incidence_mat_incomplete:  "j < 𝖻 ⟹ 0 ∈$ (col N j)"
  using valid_blocks_index incomplete_block_col incomplete_imp_incomp_block by blast 

end

locale ordered_t_wise_balance = ordered_proper_design 𝒱s ℬs + t_wise_balance "set 𝒱s" "mset ℬs" 𝗍 Λ⇩t
  for 𝒱s and ℬs and 𝗍 and Λ⇩t

begin

lemma incidence_mat_des_index: 
  assumes "I ⊆ {0..<𝗏}"
  assumes "card I = 𝗍"
  shows "mat_point_index N I = Λ⇩t"
proof -
  have card: "card ((!) 𝒱s ` I) = 𝗍" using assms points_indexing_inj
    by (metis (mono_tags, lifting) card_image ex_nat_less_eq not_le points_list_length subset_iff) 
  have "((!) 𝒱s ` I) ⊆ 𝒱" using assms
    by (metis atLeastLessThan_iff image_subset_iff subsetD valid_points_index)
  then have "ℬ index ((!) 𝒱s ` I) = Λ⇩t" using balanced assms(2) card by simp
  thus ?thesis using mat_point_index_rep assms(1) lessThan_atLeast0 by presburger 
qed

end

locale ordered_pairwise_balance = ordered_t_wise_balance 𝒱s ℬs 2 Λ + pairwise_balance "set 𝒱s" "mset ℬs" Λ
  for 𝒱s and ℬs and Λ
begin

lemma incidence_mat_des_two_index: 
  assumes "i1 < 𝗏"
  assumes "i2 < 𝗏"
  assumes "i1 ≠ i2"
  shows "mat_point_index N {i1, i2} = Λ"
  using incidence_mat_des_index incidence_mat_two_index 
proof -
  have "𝒱s ! i1 ≠ 𝒱s ! i2" using assms(3)
    by (simp add: assms(1) assms(2) distinct nth_eq_iff_index_eq points_list_length) 
  then have pair: "card {𝒱s ! i1, 𝒱s ! i2} = 2" using card_2_iff by blast
  have "{𝒱s ! i1, 𝒱s ! i2} ⊆ 𝒱" using assms
    by (simp add: valid_points_index) 
  then have "ℬ index {𝒱s ! i1, 𝒱s ! i2} = Λ" using pair
    using balanced by blast 
  thus ?thesis using incidence_mat_two_index assms by simp
qed

lemma transpose_N_mult_off_diag: 
  assumes "i ≠ j" and "i < 𝗏" and "j < 𝗏"
  shows "(N * N⇧T) $$ (i, j) = Λ"
proof -
  have rev: "⋀ k. k ∈ {0..<𝖻} ⟹ ¬ (N $$ (i, k) = 1 ∧ N $$ (j, k) = 1) ⟷ N $$ (i, k) = 0 ∨ N $$ (j, k) = 0"
    using assms matrix_elems_one_zero by auto
  then have split: "{0..<𝖻} = {k ∈ {0..<𝖻}. N $$ (i, k) = 1 ∧ N $$ (j, k) = 1} ∪ 
      {k ∈ {0..<𝖻}. N $$ (i, k) = 0 ∨ N $$ (j, k) = 0}"
    by blast
  have zero: "⋀ k . k ∈ {0..<𝖻} ⟹ N $$ (i, k) = 0 ∨ N $$ (j, k) = 0 ⟹ N $$ (i, k) * N$$ (j, k) = 0"
    by simp 
  have djnt: "{k ∈ {0..<𝖻}. N $$ (i, k) = 1 ∧ N $$ (j, k) = 1} ∩ 
    {k ∈ {0..<𝖻}. N $$ (i, k) = 0 ∨ N $$ (j, k) = 0} = {}" using rev by auto
  have fin1: "finite {k ∈ {0..<𝖻}. N $$ (i, k) = 1 ∧ N $$ (j, k) = 1}" by simp
  have fin2: "finite {k ∈ {0..<𝖻}. N $$ (i, k) = 0 ∨ N $$ (j, k) = 0}" by simp
  have "(N * N⇧T) $$ (i, j) = (∑k ∈{0..<𝖻} . N $$ (i, k) * N $$ (j, k))"
    using assms(2) assms(3) transpose_mat_mult_entries[of "i" "N" "j"] by (simp)
  also have "... = (∑k ∈({k' ∈ {0..<𝖻}. N $$ (i, k') = 1 ∧ N $$ (j, k') = 1} ∪ 
    {k' ∈ {0..<𝖻}. N $$ (i, k') = 0 ∨ N $$ (j, k') = 0}) . N $$ (i, k) * N $$ (j, k))"
    using split by metis
  also have "... = (∑k ∈{k' ∈ {0..<𝖻}. N $$ (i, k') = 1 ∧ N $$ (j, k') = 1} . N $$ (i, k) * N $$ (j, k)) + 
    (∑k ∈{k' ∈ {0..<𝖻}. N $$ (i, k') = 0 ∨ N $$ (j, k') = 0} . N $$ (i, k) * N $$ (j, k))"
    using fin1 fin2 djnt sum.union_disjoint by blast 
  also have "... = card {k' ∈ {0..<𝖻}. N $$ (i, k') = 1 ∧ N $$ (j, k') = 1}" 
    by (simp add: zero)
  also have "... = mat_point_index N {i, j}" 
    using assms mat_point_index_two_alt[of i N j] by simp
  finally show ?thesis using incidence_mat_des_two_index assms by simp
qed

end

context pairwise_balance
begin

lemma ordered_pbdI: 
  assumes "ℬ = mset ℬs" and "𝒱 = set 𝒱s" and "distinct 𝒱s"
  shows "ordered_pairwise_balance 𝒱s ℬs Λ"
proof -
  interpret ois: ordered_incidence_system 𝒱s ℬs 
    using ordered_incidence_sysII assms finite_incidence_system_axioms by blast 
  show ?thesis using b_non_zero blocks_nempty assms t_lt_order balanced 
    by (unfold_locales)(simp_all)
qed
end

locale ordered_regular_pairwise_balance = ordered_pairwise_balance "𝒱s" "ℬs" Λ + 
  regular_pairwise_balance "set 𝒱s" "mset ℬs" Λ 𝗋 for 𝒱s and ℬs and Λ and 𝗋

sublocale ordered_regular_pairwise_balance ⊆ ordered_constant_rep
  by unfold_locales

context ordered_regular_pairwise_balance
begin

text ‹ Stinson's Theorem 1.15. Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"› 
gives an iff condition for incidence matrices of regular pairwise 
balanced designs. The other direction is proven in the @{term "zero_one_matrix"} context ›
lemma rpbd_incidence_matrix_cond: "N * (N⇧T) = Λ ⋅⇩m (J⇩m 𝗏) + (𝗋 - Λ) ⋅⇩m (1⇩m 𝗏)"
proof (intro eq_matI)
  fix i j
  assume ilt: "i < dim_row (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)" 
    and jlt: "j < dim_col (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
  then have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = 
    (int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) + (int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j)" 
    by simp
  then have split: "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = 
    (int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) + (𝗋 - Λ) * ((1⇩m 𝗏) $$ (i, j))"
    using ilt jlt by simp
  have lhs: "(int Λ ⋅⇩m J⇩m 𝗏) $$(i, j) = Λ" using ilt jlt by simp
  show "(N * N⇧T) $$ (i, j) = (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j)"
  proof (cases "i = j")
    case True
    then have rhs: "(int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = (𝗋 - Λ)" using ilt by fastforce 
    have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = Λ + (𝗋 - Λ)"
      using True jlt by auto
    then have "(int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏) $$ (i, j) = 𝗋" 
      using reg_index_lt_rep by (simp add: nat_diff_split)
    then show ?thesis using lhs split rhs True transpose_N_mult_diag ilt jlt by simp
  next
    case False
    then have "(1⇩m 𝗏) $$ (i, j) = 0" using ilt jlt by simp
    then have "(𝗋 - Λ) * ((1⇩m 𝗏) $$ (i, j)) = 0" using ilt jlt
      by (simp add: ‹1⇩m 𝗏 $$ (i, j) = 0›) 
    then show ?thesis using lhs transpose_N_mult_off_diag ilt jlt False by simp
  qed
next
  show "dim_row (N * N⇧T) = dim_row (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
    using transpose_N_mult_dim(1) by auto
next
  show "dim_col (N * N⇧T) = dim_col (int Λ ⋅⇩m J⇩m 𝗏 + int (𝗋 - Λ) ⋅⇩m 1⇩m 𝗏)"
    using transpose_N_mult_dim(1) by auto
qed
end

locale ordered_bibd = ordered_proper_design 𝒱s ℬs + bibd "set 𝒱s" "mset ℬs" 𝗄 Λ 
  for 𝒱s and ℬs and 𝗄 and Λ

sublocale ordered_bibd ⊆ ordered_incomplete_design
  by unfold_locales

sublocale ordered_bibd ⊆ ordered_constant_rep 𝒱s ℬs 𝗋
  by unfold_locales

sublocale ordered_bibd ⊆ ordered_pairwise_balance
  by unfold_locales

locale ordered_sym_bibd = ordered_bibd 𝒱s ℬs 𝗄 Λ + symmetric_bibd "set 𝒱s" "mset ℬs" 𝗄 Λ 
  for 𝒱s and ℬs and 𝗄 and Λ


sublocale ordered_sym_bibd ⊆ ordered_simple_design
  by (unfold_locales)

locale ordered_const_intersect_design = ordered_proper_design 𝒱s ℬs + const_intersect_design "set 𝒱s" "mset ℬs" 𝗆
  for 𝒱s ℬs 𝗆


locale simp_ordered_const_intersect_design = ordered_const_intersect_design + ordered_simple_design
begin 

lemma max_one_block_size_inter: 
  assumes "𝖻 ≥ 2"
  assumes "bl ∈# ℬ"
  assumes "card bl = 𝗆"
  assumes "bl2 ∈# ℬ - {#bl#}"
  shows "𝗆 < card bl2"
proof -
  have sd: "simple_design 𝒱 ℬ"
    by (simp add: simple_design_axioms) 
  have bl2in: "bl2 ∈# ℬ" using assms(4)
    by (meson in_diffD)
  have blin: "bl ∈# {#b ∈# ℬ . card b = 𝗆#}" using assms(3) assms(2) by simp
  then have slt: "size {#b ∈# ℬ . card b = 𝗆#} = 1" using simple_const_inter_iff sd assms(1)
    by (metis count_empty count_eq_zero_iff less_one nat_less_le size_eq_0_iff_empty) 
  then have "size {#b ∈# (ℬ - {#bl#}) . card b = 𝗆#} = 0" using blin
    by (smt (verit) add_mset_eq_singleton_iff count_eq_zero_iff count_filter_mset 
        filter_mset_add_mset insert_DiffM size_1_singleton_mset size_eq_0_iff_empty) 
  then have ne: "card bl2 ≠ 𝗆" using assms(4)
    by (metis (mono_tags, lifting) filter_mset_empty_conv size_eq_0_iff_empty) 
  thus ?thesis using inter_num_le_block_size assms bl2in nat_less_le by presburger 
qed

lemma block_size_inter_num_cases:
  assumes "bl ∈# ℬ"
  assumes "𝖻 ≥ 2"
  shows "𝗆 < card bl ∨ (card bl = 𝗆 ∧ (∀ bl' ∈# (ℬ - {#bl#}) . 𝗆 < card bl'))"
proof (cases "card bl = 𝗆")
  case True
  have "(⋀ bl'. bl' ∈# (ℬ - {#bl#}) ⟹ 𝗆 < card bl')"
    using max_one_block_size_inter True assms by simp
  then show ?thesis using True by simp
next
  case False
  then have "𝗆 < card bl" using assms inter_num_le_block_size nat_less_le by presburger
  then show ?thesis by simp
qed

lemma indexed_const_intersect: 
  assumes "j1 < 𝖻"
  assumes "j2 < 𝖻"
  assumes "j1 ≠ j2"
  shows "(ℬs ! j1) |∩| (ℬs ! j2) = 𝗆"
proof -
  obtain bl1 bl2 where "bl1 ∈# ℬ" and "ℬs ! j1 = bl1" and "bl2 ∈# ℬ - {#bl1#}" and "ℬs ! j2 = bl2" 
    using obtains_two_diff_block_indexes assms by fastforce 
  thus ?thesis by (simp add: const_intersect)
qed

lemma const_intersect_block_size_diff: 
  assumes "j' < 𝖻" and "j < 𝖻" and "j ≠ j'" and "card (ℬs ! j') = 𝗆" and "𝖻 ≥ 2"
  shows "card (ℬs ! j) - 𝗆 > 0"
proof -
  obtain bl1 bl2 where "bl1 ∈# ℬ" and "ℬs ! j' = bl1" and "bl2 ∈# ℬ - {#bl1#}" and "ℬs ! j = bl2"
    using assms(1) assms(2) assms(3) obtains_two_diff_block_indexes by fastforce 
  then have "𝗆 < card (bl2)" 
    using max_one_block_size_inter assms(4) assms(5) by blast  
  thus ?thesis
    by (simp add: ‹ℬs ! j = bl2›) 
qed

lemma scalar_prod_inc_vec_const_inter: 
  assumes "j1 < 𝖻" "j2 < 𝖻" "j1 ≠ j2"
  shows "(col N j1) ∙ (col N j2) = 𝗆"
  using scalar_prod_inc_vec_inter_num indexed_const_intersect assms by simp

end

subsection ‹ Zero One Matrix Incidence System Existence ›
text ‹We prove 0-1 matrices with certain properties imply the existence of an incidence system
with particular properties. This leads to Stinson's theorem in the other direction \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"› ›

context zero_one_matrix
begin

lemma mat_is_ordered_incidence_sys: "ordered_incidence_system [0..<(dim_row M)] (map (map_col_to_block) (cols M))"
  apply (unfold_locales, simp_all)
  using map_col_to_block_wf atLeastLessThan_upt by blast

interpretation mat_ord_inc_sys: ordered_incidence_system "[0..<(dim_row M)]" "(map (map_col_to_block) (cols M))"
  by (simp add: mat_is_ordered_incidence_sys)

lemma mat_ord_inc_sys_N: "mat_ord_inc_sys.N = lift_01_mat M" 
  by (intro eq_matI, simp_all add: inc_mat_of_def map_col_to_block_elem) 
    (metis lift_01_mat_simp(3) lift_mat_01_index_iff(2) of_zero_neq_one_def)

lemma map_col_to_block_mat_rep_num:
  assumes "x <dim_row M"
  shows "({# map_col_to_block c . c ∈# mset (cols M)#} rep x) = mat_rep_num M x"
proof -
  have "mat_rep_num M x = mat_rep_num (lift_01_mat M) x" 
    using preserve_mat_rep_num mat_ord_inc_sys_N
    by (metis assms lift_01_mat_def of_inj_on_01_hom.inj_on_01_hom_axioms)
  then have "mat_rep_num M x = (mat_rep_num mat_ord_inc_sys.N x)" using mat_ord_inc_sys_N by (simp) 
  then have "mat_rep_num M x = mset (map (map_col_to_block) (cols M)) rep x"
    using assms atLeastLessThan_upt card_atLeastLessThan mat_ord_inc_sys.mat_rep_num_N_row 
      mat_ord_inc_sys_point minus_nat.diff_0 by presburger
  thus ?thesis using ordered_to_mset_col_blocks
    by presburger 
qed

end 

context zero_one_matrix_ring_1
begin

lemma transpose_cond_index_vals: 
  assumes "M * (M⇧T) = Λ ⋅⇩m (J⇩m (dim_row M)) + (r - Λ) ⋅⇩m (1⇩m (dim_row M))"
  assumes "i < dim_row (M * (M⇧T))"
  assumes "j < dim_col (M * (M⇧T))"
  shows "i = j ⟹ (M * (M⇧T)) $$ (i, j) = r" "i ≠ j ⟹ (M * (M⇧T)) $$ (i, j) = Λ"
  using assms by auto

end

locale zero_one_matrix_int = zero_one_matrix_ring_1 M for M :: "int mat"
begin

text ‹Some useful conditions on the transpose product for matrix system properties ›
lemma transpose_cond_diag_r:
  assumes "i < dim_row (M * (M⇧T))"
  assumes "⋀ j. i = j ⟹ (M * (M⇧T)) $$ (i, j) = r"
  shows "mat_rep_num M i = r"
proof -
  have eqr: "(M * M⇧T) $$ (i, i) = r" using assms(2)
    by simp
  have unsq: "⋀ k . k < dim_col M ⟹ (M $$ (i, k))^2 = M $$ (i, k)"
    using assms elems01 by fastforce
  have "sum_vec (row M i) = (∑k ∈{0..<(dim_col M)} . (row M i) $ k)"
    using assms by (simp add: sum_vec_def)
  also have "... = (∑k ∈{0..<(dim_col M)} . M $$ (i, k))"
    using assms by auto
  also have "... = (∑k ∈{0..<(dim_col M)} . M $$ (i, k)^2)"
    using atLeastLessThan_iff sum.cong unsq by simp
  also have "... = (∑k ∈{0..<(dim_col M)} . M $$ (i, k) * M $$ (i, k))"
    using assms by (simp add: power2_eq_square)
  also have "... = (M * M⇧T) $$ (i, i)" 
    using assms transpose_mat_mult_entries[of "i" "M" "i"] by simp
  finally have "sum_vec (row M i) = r" using eqr by simp
  thus ?thesis using mat_rep_num_sum_alt
    by (metis assms(1) elems01 index_mult_mat(2) of_nat_eq_iff) 
qed


lemma transpose_cond_non_diag:
  assumes "i1 < dim_row (M * (M⇧T))"
  assumes "i2 < dim_row (M * (M⇧T))"
  assumes "i1 ≠ i2"
  assumes "⋀ j i. j ≠ i ⟹ i < dim_row (M * (M⇧T)) ⟹ j < dim_row (M * (M⇧T)) ⟹ (M * (M⇧T)) $$ (i, j) = Λ"
  shows "Λ = mat_point_index M {i1, i2}"
proof -
  have ilt: "i1 < dim_row M" "i2 < dim_row M"
    using assms(1) assms (2) by auto
  have rev: "⋀ k. k ∈ {0..<dim_col M} ⟹ 
      ¬ (M $$ (i1, k) = 1 ∧ M $$ (i2, k) = 1) ⟷ M $$ (i1, k) = 0 ∨ M $$ (i2, k) = 0"
    using assms elems01 by fastforce 
  then have split: "{0..<dim_col M} = {k ∈ {0..<dim_col M}. M $$ (i1, k) = 1 ∧ M $$ (i2, k) = 1} ∪ 
      {k ∈ {0..<dim_col M}. M $$ (i1, k) = 0 ∨ M $$ (i2, k) = 0}"
    by blast
  have zero: "⋀ k . k ∈ {0..<dim_col M} ⟹ M $$ (i1, k) = 0 ∨ M $$ (i2, k) = 0 ⟹ M $$ (i1, k) * M$$ (i2, k) = 0"
    by simp 
  have djnt: "{k ∈ {0..<dim_col M}. M $$ (i1, k) = 1 ∧ M $$ (i2, k) = 1} ∩ 
      {k ∈ {0..<dim_col M}. M $$ (i1, k) = 0 ∨ M $$ (i2, k) = 0} = {}" 
    using rev by auto
  have fin1: "finite {k ∈ {0..<dim_col M}. M $$ (i1, k) = 1 ∧ M $$ (i2, k) = 1}" by simp
  have fin2: "finite {k ∈ {0..<dim_col M}. M $$ (i1, k) = 0 ∨ M $$ (i2, k) = 0}" by simp
  have "mat_point_index M {i1, i2} = card {k' ∈ {0..<dim_col M}. M $$ (i1, k') = 1 ∧M $$ (i2, k') = 1}"
    using mat_point_index_two_alt ilt assms(3) by auto
  then have "mat_point_index M {i1, i2} = 
    (∑k ∈{k' ∈ {0..<dim_col M}. M $$ (i1, k') = 1 ∧ M $$ (i2, k') = 1} . M $$ (i1, k) * M $$ (i2, k)) + 
    (∑k ∈{k' ∈ {0..<dim_col M}. M $$ (i1, k') = 0 ∨ M $$ (i2, k') = 0} . M $$ (i1, k) * M $$ (i2, k))"
    by (simp add: zero) (* Odd behaviour if I use also have here *)
  also have "... = (∑k ∈({k' ∈ {0..<dim_col M}. M $$ (i1, k') = 1 ∧ M $$ (i2, k') = 1} ∪ 
    {k' ∈ {0..<dim_col M}. M $$ (i1, k') = 0 ∨ M $$ (i2, k') = 0}) . M $$ (i1, k) * M $$ (i2, k))"
    using fin1 fin2 djnt sum.union_disjoint by (metis (no_types, lifting)) 
  also have "... =  (∑k ∈{0..<dim_col M} . M $$ (i1, k) * M $$ (i2, k))"
    using split by metis
  finally have "mat_point_index M {i1, i2} = (M * (M⇧T)) $$ (i1, i2)"
    using assms(1) assms(2) transpose_mat_mult_entries[of "i1" "M" "i2"] by simp
  thus ?thesis using assms by presburger 
qed

lemma trans_cond_implies_map_rep_num:
  assumes "M * (M⇧T) = Λ ⋅⇩m (J⇩m (dim_row M)) + (r - Λ) ⋅⇩m (1⇩m (dim_row M))"
  assumes "x < dim_row M"
  shows "(image_mset map_col_to_block (mset (cols M))) rep x = r"
proof -
  interpret ois: ordered_incidence_system "[0..<dim_row M]" "map map_col_to_block (cols M)"
    using mat_is_ordered_incidence_sys by simp
  have eq: "ois.ℬ rep x = sum_vec (row M x)" using ois.point_rep_mat_row_sum
    by (simp add: assms(2) inc_mat_of_map_rev) 
  then have "⋀ j. x = j ⟹ (M * (M⇧T)) $$ (x, j) = r" using assms(1) transpose_cond_index_vals
    by (metis assms(2) index_mult_mat(2) index_mult_mat(3) index_transpose_mat(3)) 
  thus ?thesis using eq transpose_cond_diag_r assms(2) index_mult_mat(2)
    by (metis map_col_to_block_mat_rep_num) 
qed

lemma trans_cond_implies_map_index:
  assumes "M * (M⇧T) = Λ ⋅⇩m (J⇩m (dim_row M)) + (r - Λ) ⋅⇩m (1⇩m (dim_row M))"
  assumes "ps ⊆ {0..<dim_row M}"
  assumes "card ps = 2"
  shows "(image_mset map_col_to_block (mset (cols M))) index ps = Λ"
proof - 
  interpret ois: ordered_incidence_system "[0..<dim_row M]" "map map_col_to_block (cols M)"
    using mat_is_ordered_incidence_sys by simp
  obtain i1 i2 where i1in: "i1 <dim_row M" and i2in: "i2 <dim_row M" and psis: "ps = {i1, i2}" and neqi: "i1 ≠ i2"
    using assms(2) assms(3) card_2_iff insert_subset by (metis atLeastLessThan_iff) 
  have cond: "⋀ j i. j ≠ i ⟹ i < dim_row (M * (M⇧T)) ⟹ j < dim_row (M * (M⇧T)) ⟹ (M * (M⇧T)) $$ (i, j) = Λ"
    using assms(1) by simp
  then have "(image_mset map_col_to_block (mset (cols M))) index ps = mat_point_index M ps"
     using ois.incidence_mat_two_index psis i1in i2in by (simp add: neqi inc_mat_of_map_rev)
  thus ?thesis using cond transpose_cond_non_diag[of i1 i2 Λ] i1in i2in index_mult_mat(2)[of "M" "M⇧T"] 
       neqi of_nat_eq_iff psis by simp
qed

text ‹ Stinson Theorem 1.15 existence direction ›
lemma rpbd_exists: 
  assumes "dim_row M ≥ 2" ― ‹Min two points›
  assumes "dim_col M ≥ 1" ― ‹Min one block›
  assumes "⋀ j. j < dim_col M ⟹ 1 ∈$ col M j" ― ‹no empty blocks ›
  assumes "M * (M⇧T) = Λ ⋅⇩m (J⇩m (dim_row M)) + (r - Λ) ⋅⇩m (1⇩m (dim_row M))"
  shows "ordered_regular_pairwise_balance [0..<dim_row M] (map map_col_to_block (cols M)) Λ r"
proof -
  interpret ois: ordered_incidence_system "[0..<dim_row M]" "(map map_col_to_block (cols M))"
    using mat_is_ordered_incidence_sys by simp
  interpret pdes: ordered_design "[0..<dim_row M]" "(map map_col_to_block (cols M))"
    using assms(2) mat_is_design assms(3)
    by (simp add: ordered_design_def ois.ordered_incidence_system_axioms)  
  show ?thesis using assms trans_cond_implies_map_index trans_cond_implies_map_rep_num 
    by (unfold_locales) (simp_all)
qed

lemma vec_k_uniform_mat_block_size: 
  assumes "((u⇩v (dim_row M)) ⇩v* M) = k ⋅⇩v (u⇩v (dim_col M))"
  assumes "j < dim_col M"
  shows "mat_block_size M j = k"
proof -
  have "mat_block_size M j = sum_vec (col M j)" using assms(2)
    by (simp add: elems01 mat_block_size_sum_alt) 
  also have "... = ((u⇩v (dim_row M)) ⇩v* M) $ j" using assms(2) 
    by (simp add: sum_vec_def scalar_prod_def)
  finally show ?thesis using  assms(1) assms(2) by (simp)
qed

lemma vec_k_impl_uniform_block_size: 
  assumes "((u⇩v (dim_row M)) ⇩v* M) = k ⋅⇩v (u⇩v (dim_col M))"
  assumes "bl ∈# (image_mset map_col_to_block (mset (cols M)))"
  shows "card bl = k"
proof -
  obtain j where jlt: "j < dim_col M" and bleq: "bl = map_col_to_block (col M j)"
    using assms(2) obtain_block_index_map_block_set by blast 
  then have "card (map_col_to_block (col M j)) = mat_block_size M j"
    by (simp add: map_col_to_block_size) 
  thus ?thesis using vec_k_uniform_mat_block_size assms(1) bleq jlt by blast 
qed

lemma bibd_exists: 
  assumes "dim_col M ≥ 1" ― ‹Min one block›
  assumes "⋀ j. j < dim_col M ⟹ 1 ∈$ col M j" ― ‹no empty blocks ›
  assumes "M * (M⇧T) = Λ ⋅⇩m (J⇩m (dim_row M)) + (r - Λ) ⋅⇩m (1⇩m (dim_row M))"
  assumes "((u⇩v (dim_row M)) ⇩v* M) = k ⋅⇩v (u⇩v (dim_col M))"
  assumes "(r ::nat) ≥ 0"
  assumes "k ≥ 2" "k < dim_row M"
  shows "ordered_bibd [0..<dim_row M] (map map_col_to_block (cols M)) k Λ"
proof -
  interpret ipbd: ordered_regular_pairwise_balance "[0..<dim_row M]" "(map map_col_to_block (cols M))" Λ r
    using rpbd_exists assms by simp
  show ?thesis using vec_k_impl_uniform_block_size by (unfold_locales, simp_all add: assms)
qed

end

subsection ‹Isomorphisms and Incidence Matrices ›
text ‹If two incidence systems have the same incidence matrix, they are isomorphic. Similarly
if two incidence systems are isomorphic there exists an ordering such that they have the same
incidence matrix ›
locale two_ordered_sys = D1: ordered_incidence_system 𝒱s ℬs + D2: ordered_incidence_system 𝒱s' ℬs'
  for "𝒱s" and "ℬs" and "𝒱s'" and "ℬs'" 

begin

lemma equal_inc_mat_isomorphism: 
  assumes "D1.N = D2.N"
  shows "incidence_system_isomorphism D1.𝒱 D1.ℬ D2.𝒱 D2.ℬ (λ x . 𝒱s' ! (List_Index.index 𝒱s x))"
proof (unfold_locales)
  show "bij_betw (λx. 𝒱s' ! List_Index.index 𝒱s x) D1.𝒱 D2.𝒱" 
  proof -
    have comp: "(λx. 𝒱s' ! List_Index.index 𝒱s x) = (λ i. 𝒱s' ! i) ∘ (λ y . List_Index.index 𝒱s y)"
      by (simp add: comp_def)
    have leq: "length 𝒱s = length 𝒱s'" 
      using assms D1.dim_row_is_v D1.points_list_length D2.dim_row_is_v D2.points_list_length by force 
    have bij1: "bij_betw (λ i. 𝒱s' !i) {..<length 𝒱s} (set 𝒱s') " using leq
      by (simp add: bij_betw_nth D2.distinct) 
    have "bij_betw (List_Index.index 𝒱s) (set 𝒱s) {..<length 𝒱s}" using D1.distinct
      by (simp add: bij_betw_index lessThan_atLeast0) 
    thus ?thesis using bij_betw_trans comp bij1 by simp
  qed
next
  have len:  "length (map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs) = length ℬs'"
    using length_map assms D1.dim_col_is_b by force 
  have mat_eq: "⋀ i j . D1.N $$ (i, j) = D2.N $$ (i, j)" using assms
    by simp 
  have vslen: "length 𝒱s = length 𝒱s'" using assms
      using D1.dim_row_is_v D1.points_list_length D2.dim_row_is_v D2.points_list_length by force 
  have "⋀ j. j < length ℬs' ⟹ (map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs) ! j = ℬs' ! j"
  proof -
    fix j assume a: "j < length ℬs'" 
    then have "(map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs) ! j = (λx. 𝒱s' ! List_Index.index 𝒱s x) ` (ℬs ! j)"
      by (metis D1.blocks_list_length D1.dim_col_is_b D2.blocks_list_length D2.dim_col_is_b assms nth_map) 
    also have "... = (λ i . 𝒱s' ! i) ` ((λ x. List_Index.index 𝒱s x) ` (ℬs ! j))" 
      by blast
    also have "... = ((λ i . 𝒱s' ! i) ` {i . i < length 𝒱s ∧ D1.N $$ (i, j) = 1})" 
      using D1.block_mat_cond_rev a assms
      by (metis (no_types, lifting) D1.blocks_list_length D1.dim_col_is_b D2.blocks_list_length D2.dim_col_is_b) 
    also have "... = ((λ i . 𝒱s' ! i) ` {i . i < length 𝒱s' ∧ D2.N $$ (i, j) = 1})" 
      using vslen mat_eq by simp
    finally have "(map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs) ! j = (ℬs' ! j)" 
      using D2.block_mat_cond_rep' a by presburger
    then show "(map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs) ! j = (ℬs' ! j)" by simp
  qed
  then have "map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs = ℬs'" 
    using len nth_equalityI[of "(map ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) ℬs)" "ℬs'"] by simp
  then show "image_mset ((`) (λx. 𝒱s' ! List_Index.index 𝒱s x)) D1.ℬ = D2.ℬ"
    using mset_map by auto
qed

lemma equal_inc_mat_isomorphism_ex: "D1.N = D2.N ⟹ ∃ π . incidence_system_isomorphism D1.𝒱 D1.ℬ D2.𝒱 D2.ℬ π"
  using equal_inc_mat_isomorphism by auto 

lemma equal_inc_mat_isomorphism_obtain: 
  assumes "D1.N = D2.N"
  obtains π where "incidence_system_isomorphism D1.𝒱 D1.ℬ D2.𝒱 D2.ℬ π"
  using equal_inc_mat_isomorphism assms by auto 

end

context incidence_system_isomorphism
begin

lemma exists_eq_inc_mats:
  assumes "finite 𝒱" "finite 𝒱'"
  obtains N where "is_incidence_matrix N 𝒱 ℬ" and "is_incidence_matrix N 𝒱' ℬ'"
proof -
  obtain Vs where vsis: "Vs ∈ permutations_of_set 𝒱" using assms
    by (meson all_not_in_conv permutations_of_set_empty_iff) 
  obtain Bs where bsis: "Bs ∈ permutations_of_multiset ℬ"
    by (meson all_not_in_conv permutations_of_multiset_not_empty) 
  have inj: "inj_on π 𝒱" using bij
    by (simp add: bij_betw_imp_inj_on) 
  then have mapvs: "map π Vs ∈ permutations_of_set 𝒱'" using permutations_of_set_image_inj
    using ‹Vs ∈ permutations_of_set 𝒱› iso_points_map by blast 
  have "permutations_of_multiset (image_mset ((`)π) ℬ) = map ((`) π) ` permutations_of_multiset ℬ"
    using block_img permutations_of_multiset_image by blast 
  then have mapbs: "map ((`) π) Bs ∈ permutations_of_multiset ℬ'" using bsis block_img by blast 
  define N :: "'c :: {ring_1} mat" where "N ≡ inc_mat_of Vs Bs" 
  have "is_incidence_matrix N 𝒱 ℬ"
    using N_def bsis is_incidence_matrix_def vsis by blast
  have "⋀ bl . bl ∈ (set Bs) ⟹ bl ⊆ (set Vs)"
    by (meson bsis in_multiset_in_set ordered_incidence_system.wf_list source.alt_ordering_sysI vsis) 
  then have "N = inc_mat_of (map π Vs) (map ((`) π) Bs)" 
    using inc_mat_of_bij_betw inj
    by (metis N_def permutations_of_setD(1) vsis) 
  then have "is_incidence_matrix N 𝒱' ℬ'"
    using mapbs mapvs is_incidence_matrix_def by blast 
  thus ?thesis
    using ‹is_incidence_matrix N 𝒱 ℬ› that by auto 
qed

end

end