# Theory Design_Basics

```theory Design_Basics imports Main Multisets_Extras "HOL-Library.Disjoint_Sets"
begin

section ‹Design Theory Basics›
text ‹All definitions in this section reference the handbook of combinatorial designs
\<^cite>‹"colbournHandbookCombinatorialDesigns2007"››

subsection ‹Initial setup›

text ‹Enable coercion of nats to ints to aid with reasoning on design properties›
declare [[coercion_enabled]]
declare [[coercion "of_nat :: nat ⇒ int"]]

subsection ‹Incidence System›

text ‹An incidence system is defined to be a wellformed set system. i.e. each block is a subset
of the base point set. Alternatively, an incidence system can be looked at as the point set
and an incidence relation which indicates if they are in the same block›

locale incidence_system =
fixes point_set :: "'a set" ("𝒱")
fixes block_collection :: "'a set multiset" ("ℬ")
assumes wellformed: "b ∈# ℬ ⟹ b ⊆ 𝒱"
begin

definition "ℐ ≡ { (x, b) . b ∈# ℬ ∧ x ∈ b}" (* incidence relation *)

definition incident :: "'a ⇒ 'a set ⇒ bool" where
"incident p b ≡ (p, b) ∈ ℐ"

text ‹Defines common notation used to indicate number of points (\$v\$) and number of blocks (\$b\$)›
abbreviation "𝗏 ≡ card 𝒱"

abbreviation "𝖻 ≡ size ℬ"

text ‹Basic incidence lemmas›

lemma incidence_alt_def:
assumes "p ∈ 𝒱"
assumes "b ∈# ℬ"
shows "incident p b ⟷ p ∈ b"
by (auto simp add: incident_def ℐ_def assms)

lemma wf_invalid_point: "x ∉ 𝒱 ⟹ b ∈# ℬ ⟹ x ∉ b"
using wellformed by auto

lemma block_set_nempty_imp_block_ex: "ℬ ≠ {#} ⟹ ∃ bl . bl ∈# ℬ"
by auto

text ‹Abbreviations for all incidence systems›
abbreviation multiplicity :: "'a set ⇒ nat" where
"multiplicity b ≡ count ℬ b"

abbreviation incomplete_block :: "'a set ⇒ bool" where
"incomplete_block bl ≡ card bl < card 𝒱 ∧ bl ∈# ℬ"

lemma incomplete_alt_size: "incomplete_block bl ⟹ card bl < 𝗏"
by simp

lemma incomplete_alt_in: "incomplete_block bl ⟹ bl ∈# ℬ"
by simp

lemma incomplete_alt_imp[intro]: "card bl < 𝗏 ⟹ bl ∈# ℬ ⟹ incomplete_block bl"
by simp

definition design_support :: "'a set set" where
"design_support ≡ set_mset ℬ"

end

subsection ‹Finite Incidence Systems›

text ‹These simply require the point set to be finite.
As multisets are only defined to be finite, it is implied that the block set must be finite already›

locale finite_incidence_system = incidence_system +
assumes finite_sets: "finite 𝒱"
begin

lemma finite_blocks: "b ∈# ℬ ⟹ finite b"
using wellformed finite_sets finite_subset by blast

lemma mset_points_distinct: "distinct_mset (mset_set 𝒱)"
using finite_sets by (simp add: distinct_mset_def)

lemma mset_points_distinct_diff_one: "distinct_mset (mset_set (𝒱 - {x}))"
by (meson count_mset_set_le_one distinct_mset_count_less_1)

lemma finite_design_support: "finite (design_support)"
using design_support_def by auto

lemma block_size_lt_order: "bl ∈# ℬ ⟹ card bl ≤ card 𝒱"
using wellformed by (simp add: card_mono finite_sets)

end

subsection ‹Designs›

text ‹There are many varied definitions of a design in literature. However, the most
commonly accepted definition is a finite point set, \$V\$ and collection of blocks \$B\$, where
no block in \$B\$ can be empty›
locale design = finite_incidence_system +
assumes blocks_nempty: "bl ∈# ℬ ⟹ bl ≠ {}"
begin

lemma wf_design: "design 𝒱 ℬ"  by intro_locales

lemma wf_design_iff: "bl ∈# ℬ ⟹ design 𝒱 ℬ ⟷ (bl ⊆ 𝒱 ∧ finite 𝒱 ∧ bl ≠ {})"
using blocks_nempty wellformed finite_sets

text ‹Reasoning on non empty properties and non zero parameters›
lemma blocks_nempty_alt: "∀ bl ∈# ℬ. bl ≠ {}"
using blocks_nempty by auto

lemma block_set_nempty_imp_points: "ℬ ≠ {#} ⟹ 𝒱 ≠ {}"
using wf_design wf_design_iff by auto

lemma b_non_zero_imp_v_non_zero: "𝖻 > 0 ⟹ 𝗏 > 0"
using block_set_nempty_imp_points finite_sets by fastforce

lemma v_eq0_imp_b_eq_0: "𝗏 = 0 ⟹ 𝖻 = 0"
using b_non_zero_imp_v_non_zero by auto

text ‹Size lemmas›
lemma block_size_lt_v: "bl ∈# ℬ ⟹ card bl ≤ 𝗏"
by (simp add: card_mono finite_sets wellformed)

lemma block_size_gt_0: "bl ∈# ℬ ⟹ card bl > 0"
using finite_sets blocks_nempty finite_blocks by fastforce

lemma design_cart_product_size: "size ((mset_set 𝒱) ×# ℬ) = 𝗏 * 𝖻"

end

text ‹Intro rules for design locale›

lemma wf_design_implies:
assumes "(⋀ b . b ∈# ℬ ⟹ b ⊆ V)"
assumes "⋀ b . b ∈# ℬ ⟹ b ≠ {}"
assumes "finite V"
assumes "ℬ ≠ {#}"
assumes "V ≠ {}"
shows "design V ℬ"
using assms by (unfold_locales) simp_all

lemma (in incidence_system) finite_sysI[intro]: "finite 𝒱 ⟹ finite_incidence_system 𝒱 ℬ"
by (unfold_locales) simp_all

lemma (in finite_incidence_system) designI[intro]: "(⋀ b. b ∈# ℬ ⟹ b ≠ {}) ⟹ ℬ ≠ {#}
⟹ 𝒱 ≠ {} ⟹ design 𝒱 ℬ"
by (unfold_locales) simp_all

subsection ‹Core Property Definitions›

subsubsection ‹Replication Number›

text ‹The replication number for a point is the number of blocks that point is incident with›

definition point_replication_number :: "'a set multiset ⇒ 'a ⇒ nat" (infix "rep" 75) where
"B rep x ≡ size {#b ∈# B . x ∈ b#}"

lemma max_point_rep: "B rep x ≤ size B"
using size_filter_mset_lesseq by (simp add: point_replication_number_def)

lemma rep_number_g0_exists:
assumes "B rep x > 0"
obtains b where "b ∈# B" and "x ∈ b"
proof -
have "size {#b ∈# B . x ∈ b#} > 0" using assms point_replication_number_def
by metis
thus ?thesis
by (metis filter_mset_empty_conv nonempty_has_size that)
qed

lemma rep_number_on_set_def: "finite B ⟹ (mset_set B) rep x = card {b ∈ B . x ∈ b}"

lemma point_rep_number_split[simp]: "(A + B) rep x = A rep x + B rep x"

lemma point_rep_singleton_val [simp]: "x ∈ b ⟹ {#b#} rep x = 1"

lemma point_rep_singleton_inval [simp]: "x ∉ b ⟹ {#b#} rep x = 0"

context incidence_system
begin

lemma point_rep_number_alt_def: "ℬ rep x = size {# b ∈# ℬ . x ∈ b#}"

lemma rep_number_non_zero_system_point: " ℬ rep x > 0 ⟹ x ∈ 𝒱"
using rep_number_g0_exists wellformed
by (metis wf_invalid_point)

lemma point_rep_non_existance [simp]: "x ∉ 𝒱 ⟹ ℬ rep x = 0"
using wf_invalid_point by (simp add:  point_replication_number_def filter_mset_empty_conv)

lemma point_rep_number_inv: "size {# b ∈# ℬ . x ∉ b #} = 𝖻 - (ℬ rep x)"
proof -
have "𝖻 = size {# b ∈# ℬ . x ∉ b #} + size {# b ∈# ℬ . x ∈ b #}"
using multiset_partition by (metis add.commute size_union)
thus ?thesis by (simp add: point_replication_number_def)
qed

lemma point_rep_num_inv_non_empty: "(ℬ rep x) < 𝖻 ⟹ ℬ ≠ {#} ⟹ {# b ∈# ℬ . x ∉ b #} ≠ {#}"
by (metis diff_zero point_replication_number_def size_empty size_filter_neg verit_comp_simplify1(1))

end

subsubsection ‹Point Index›

text ‹The point index of a subset of points in a design, is the number of times those points
occur together in a block of the design›
definition points_index :: "'a set multiset ⇒ 'a set ⇒ nat" (infix "index" 75) where
"B index ps ≡ size {#b ∈# B . ps ⊆ b#}"

lemma points_index_empty [simp]: "{#} index ps = 0"

lemma point_index_distrib: "(B1 + B2) index ps =  B1 index ps + B2 index ps"

lemma point_index_diff: "B1 index ps = (B1 + B2) index ps - B2 index ps"

lemma points_index_singleton: "{#b#} index ps = 1 ⟷ ps ⊆ b"

lemma points_index_singleton_zero: "¬ (ps ⊆ b) ⟹ {#b#} index ps = 0"

lemma points_index_sum: "(∑⇩# B ) index ps = (∑b ∈# B . (b index ps))"
using points_index_empty by (induction B) (auto simp add: point_index_distrib)

assumes "x ∉ ps"
assumes "B index ps = l"
shows "{# insert x b . b ∈# B#} index ps = l"
using points_index_def by (metis (no_types, lifting) assms filter_mset_cong
image_mset_filter_swap2 points_index_def size_image_mset subset_insert)

lemma points_index_on_set_def [simp]:
assumes "finite B"
shows "(mset_set B) index ps = card {b ∈ B. ps ⊆ b}"

lemma points_index_single_rep_num: "B index {x} = B rep x"

lemma points_index_pair_rep_num:
assumes "⋀ b. b ∈# B ⟹ x ∈ b"
shows "B index {x, y} = B rep y"
using point_replication_number_def points_index_def
by (metis assms empty_subsetI filter_mset_cong insert_subset)

lemma points_index_0_left_imp:
assumes "B index ps = 0"
assumes "b ∈# B"
shows "¬ (ps ⊆ b)"
proof (rule ccontr)
assume "¬ ¬ ps ⊆ b"
then have a: "ps ⊆ b" by auto
then have "b ∈# {#bl ∈# B . ps ⊆ bl#}" by (simp add: assms(2))
thus False by (metis assms(1) count_greater_eq_Suc_zero_iff count_size_set_repr not_less_eq_eq
points_index_def size_filter_mset_lesseq)
qed

lemma points_index_0_right_imp:
assumes "⋀ b . b ∈# B ⟹ (¬ ps ⊆ b)"
shows "B index ps = 0"
using assms by (simp add: filter_mset_empty_conv points_index_def)

lemma points_index_0_iff: "B index ps = 0 ⟷ (∀ b. b ∈# B ⟶ (¬ ps ⊆ b))"
using points_index_0_left_imp points_index_0_right_imp by metis

lemma points_index_gt0_impl_existance:
assumes "B index ps > 0"
shows "(∃ bl . (bl ∈# B ∧ ps ⊆ bl))"
proof -
have "size {#bl ∈# B . ps ⊆ bl#} > 0"
by (metis assms points_index_def)
then obtain bl where "bl ∈# B" and "ps ⊆ bl"
by (metis filter_mset_empty_conv nonempty_has_size)
thus ?thesis by auto
qed

lemma points_index_one_unique:
assumes "B index ps = 1"
assumes "bl ∈# B" and "ps ⊆ bl" and "bl' ∈# B" and "ps ⊆ bl'"
shows "bl = bl'"
proof (rule ccontr)
assume assm: "bl ≠ bl'"
then have bl1: "bl ∈# {#bl ∈# B . ps ⊆ bl#}" using assms by simp
then have bl2: "bl'∈# {#bl ∈# B . ps ⊆ bl#}" using assms by simp
then have "{#bl, bl'#} ⊆# {#bl ∈# B . ps ⊆ bl#}" using assms by (metis bl1 bl2 points_index_def
then have "size {#bl ∈# B . ps ⊆ bl#} ≥ 2" using size_mset_mono by fastforce
thus False using assms by (metis numeral_le_one_iff points_index_def semiring_norm(69))
qed

lemma points_index_one_unique_block:
assumes "B index ps = 1"
shows "∃! bl . (bl ∈# B ∧ ps ⊆ bl)"
using assms points_index_gt0_impl_existance points_index_one_unique
by (metis zero_less_one)

lemma points_index_one_not_unique_block:
assumes "B index ps = 1"
assumes "ps ⊆ bl"
assumes "bl ∈# B"
assumes "bl' ∈# B - {#bl#}"
shows "¬ ps ⊆ bl'"
proof -
have "B = (B - {#bl#}) + {#bl#}" by (simp add: assms(3))
then have "(B - {#bl#}) index ps = B index ps - {#bl#} index ps"
by (metis point_index_diff)
then have "(B - {#bl#}) index ps = 0" using assms points_index_singleton
by (metis diff_self_eq_0)
thus ?thesis using assms(4) points_index_0_left_imp by auto
qed

lemma (in incidence_system) points_index_alt_def: "ℬ index ps = size {#b ∈# ℬ . ps ⊆ b#}"

lemma (in incidence_system) points_index_ps_nin: "¬ (ps ⊆ 𝒱) ⟹ ℬ index ps = 0"
using points_index_alt_def filter_mset_empty_conv in_mono size_empty subsetI wf_invalid_point
by metis

lemma (in incidence_system) points_index_count_bl:
"multiplicity bl ≥ n ⟹ ps ⊆ bl ⟹ count {#bl ∈# ℬ . ps ⊆ bl#} bl ≥ n"
by simp

lemma (in finite_incidence_system) points_index_zero:
assumes "card ps > card 𝒱"
shows "ℬ index ps = 0"
proof -
have "⋀ b. b ∈# ℬ ⟹ card ps > card b"
using block_size_lt_order card_subset_not_gt_card finite_sets assms by fastforce
then have "{#b ∈# ℬ . ps ⊆ b#} = {#}"
by (simp add: card_subset_not_gt_card filter_mset_empty_conv finite_blocks)
thus ?thesis using points_index_alt_def by simp
qed

lemma (in design) points_index_subset:
"x ⊆# {#bl ∈# ℬ . ps ⊆ bl#} ⟹ ps ⊆ 𝒱 ⟹ (ℬ index ps) ≥ (size x)"

lemma (in design) points_index_count_min: "multiplicity bl ≥ n ⟹ ps ⊆ bl ⟹ ℬ index ps ≥ n"
using points_index_alt_def set_count_size_min by (metis filter_mset.rep_eq)

subsubsection ‹Intersection Number›

text ‹The intersection number of two blocks is the size of the intersection of those blocks. i.e.
the number of points which occur in both blocks›
definition intersection_number :: "'a set ⇒ 'a set ⇒ nat" (infix "|∩|" 70) where
"b1 |∩| b2 ≡ card (b1 ∩ b2)"

lemma intersection_num_non_neg: "b1 |∩| b2 ≥ 0"

lemma intersection_number_empty_iff:
assumes "finite b1"
shows "b1 ∩ b2 = {} ⟷ b1 |∩| b2 = 0"

lemma intersect_num_commute: "b1 |∩| b2 = b2 |∩| b1"

definition n_intersect_number :: "'a set ⇒ nat⇒ 'a set ⇒ nat" where
"n_intersect_number b1 n b2 ≡ card { x ∈ Pow (b1 ∩ b2) . card x = n}"

notation n_intersect_number ("(_ |∩|⇩_ _)" [52, 51, 52] 50)

lemma n_intersect_num_subset_def: "b1 |∩|⇩n b2 = card {x . x ⊆ b1 ∩ b2 ∧ card x = n}"
using n_intersect_number_def by auto

lemma n_inter_num_one: "finite b1 ⟹ finite b2 ⟹ b1 |∩|⇩1 b2 = b1 |∩| b2"
using n_intersect_number_def intersection_number_def card_Pow_filter_one
by (metis (full_types) finite_Int)

lemma n_inter_num_choose: "finite b1 ⟹ finite b2 ⟹ b1 |∩|⇩n b2 = (card (b1 ∩ b2) choose n)"
using n_subsets n_intersect_num_subset_def
by (metis (full_types) finite_Int)

lemma set_filter_single: "x ∈ A ⟹ {a ∈ A . a = x} = {x}"
by auto

lemma (in design) n_inter_num_zero:
assumes "b1 ∈# ℬ" and "b2 ∈# ℬ"
shows "b1 |∩|⇩0 b2 = 1"
proof -
have empty: "⋀x . finite x ⟹ card x = 0 ⟹ x = {}"
by simp
have empt_in: "{} ∈ Pow (b1 ∩ b2)" by simp
have "finite (b1 ∩ b2)" using finite_blocks assms by simp
then have "⋀ x . x ∈ Pow (b1 ∩ b2) ⟹ finite x" by (meson PowD finite_subset)
then have "{x ∈ Pow (b1 ∩ b2) . card x = 0} = {x ∈ Pow (b1 ∩ b2) . x = {}}"
using empty by (metis card.empty)
then have "{x ∈ Pow (b1 ∩ b2) . card x = 0} = {{}}"
by (simp add: empt_in set_filter_single Collect_conv_if)
thus ?thesis by (simp add: n_intersect_number_def)
qed

lemma (in design) n_inter_num_choose_design: "b1 ∈# ℬ ⟹ b2 ∈# ℬ
⟹ b1 |∩|⇩n b2 = (card (b1 ∩ b2) choose n) "
using finite_blocks by (simp add: n_inter_num_choose)

lemma (in design) n_inter_num_choose_design_inter: "b1 ∈# ℬ ⟹ b2 ∈# ℬ
⟹ b1 |∩|⇩n b2 = (nat (b1 |∩| b2) choose n) "
using finite_blocks by (simp add: n_inter_num_choose intersection_number_def)

subsection ‹Incidence System Set Property Definitions›
context incidence_system
begin

text ‹The set of replication numbers for all points of design›
definition replication_numbers :: "nat set" where
"replication_numbers ≡ {ℬ rep x | x . x ∈ 𝒱}"

lemma replication_numbers_non_empty:
assumes "𝒱 ≠ {}"
shows "replication_numbers ≠ {}"

lemma obtain_point_with_rep: "r ∈ replication_numbers ⟹ ∃ x. x ∈ 𝒱 ∧ ℬ rep x = r"
using replication_numbers_def by auto

lemma point_rep_number_in_set: "x ∈ 𝒱 ⟹ (ℬ rep x) ∈ replication_numbers"

lemma (in finite_incidence_system) replication_numbers_finite: "finite replication_numbers"
using finite_sets by (simp add: replication_numbers_def)

text ‹The set of all block sizes in a system›

definition sys_block_sizes :: "nat set" where
"sys_block_sizes ≡ { card bl | bl. bl ∈# ℬ}"

lemma block_sizes_non_empty_set:
assumes "ℬ ≠ {#}"
shows "sys_block_sizes ≠ {}"

lemma finite_block_sizes: "finite (sys_block_sizes)"

lemma block_sizes_non_empty:
assumes "ℬ ≠ {#}"
shows "card (sys_block_sizes) > 0"
using finite_block_sizes block_sizes_non_empty_set

lemma sys_block_sizes_in: "bl ∈# ℬ ⟹ card bl ∈ sys_block_sizes"
unfolding sys_block_sizes_def by auto

lemma sys_block_sizes_obtain_bl: "x ∈ sys_block_sizes  ⟹ (∃ bl ∈# ℬ. card bl = x)"

text ‹The set of all possible intersection numbers in a system.›

definition intersection_numbers :: "nat set" where
"intersection_numbers ≡ { b1 |∩| b2 | b1 b2 . b1 ∈# ℬ ∧ b2 ∈# (ℬ - {#b1#})}"

lemma obtain_blocks_intersect_num: "n ∈ intersection_numbers ⟹
∃ b1 b2. b1 ∈# ℬ ∧ b2 ∈# (ℬ - {#b1#}) ∧  b1 |∩| b2 = n"

lemma intersect_num_in_set: "b1 ∈# ℬ ⟹ b2 ∈# (ℬ - {#b1#}) ⟹ b1 |∩| b2 ∈ intersection_numbers"

text ‹The set of all possible point indices›
definition point_indices :: "nat ⇒ nat set" where
"point_indices t ≡ {ℬ index ps | ps. card ps = t ∧ ps ⊆ 𝒱}"

lemma point_indices_elem_in: "ps ⊆ 𝒱 ⟹ card ps = t ⟹ ℬ index ps ∈ point_indices t"

lemma point_indices_alt_def: "point_indices t = { ℬ index ps | ps. card ps = t ∧ ps ⊆ 𝒱}"

end

subsection ‹Basic Constructions on designs›

text ‹This section defines some of the most common universal constructions found in design theory
involving only a single design›

subsubsection ‹Design Complements›

context incidence_system
begin

text ‹The complement of a block are all the points in the design not in that block.
The complement of a design is therefore the original point sets, and set of all block complements›
definition block_complement:: "'a set ⇒ 'a set" ("_⇧c" [56] 55) where
"block_complement b ≡ 𝒱 - b"

definition complement_blocks :: "'a set multiset" ("(ℬ⇧C)")where
"complement_blocks ≡ {# bl⇧c . bl ∈# ℬ #}"

lemma block_complement_elem_iff:
assumes "ps ⊆ 𝒱"
shows "ps ⊆ bl⇧c ⟷ (∀ x ∈ ps. x ∉ bl)"
using assms block_complement_def by (auto)

lemma block_complement_inter_empty: "bl1⇧c = bl2 ⟹ bl1 ∩ bl2 = {}"
using block_complement_def by auto

lemma block_complement_inv:
assumes "bl ∈# ℬ"
assumes "bl⇧c = bl2"
shows "bl2⇧c = bl"
by (metis Diff_Diff_Int assms(1) assms(2) block_complement_def inf.absorb_iff2 wellformed)

lemma block_complement_subset_points: "ps ⊆ (bl⇧c) ⟹ ps ⊆ 𝒱"
using block_complement_def by blast

lemma obtain_comp_block_orig:
assumes "bl1 ∈# ℬ⇧C"
obtains bl2 where "bl2 ∈# ℬ" and "bl1 = bl2⇧c"
using wellformed assms by (auto simp add: complement_blocks_def)

lemma complement_same_b [simp]: "size ℬ⇧C = size ℬ"

lemma block_comp_elem_alt_left: "x ∈ bl ⟹ ps ⊆ bl⇧c ⟹ x ∉ ps"
by (auto simp add: block_complement_def block_complement_elem_iff)

lemma block_comp_elem_alt_right: "ps ⊆ 𝒱 ⟹ (⋀ x . x ∈ ps ⟹ x ∉ bl) ⟹ ps ⊆ bl⇧c"

lemma complement_index:
assumes "ps ⊆ 𝒱"
shows "ℬ⇧C index ps = size {# b ∈# ℬ . (∀ x ∈ ps . x ∉ b) #}"
proof -
have "ℬ⇧C index ps =  size {# b ∈# {# bl⇧c . bl ∈# ℬ#}. ps ⊆ b #}"
then have "ℬ⇧C index ps = size {# bl⇧c | bl ∈# ℬ . ps ⊆ bl⇧c #}"
by (metis image_mset_filter_swap)
thus ?thesis using assms by (simp add: block_complement_elem_iff)
qed

lemma complement_index_2:
assumes "{x, y} ⊆ 𝒱"
shows "ℬ⇧C index {x, y} = size {# b ∈# ℬ . x ∉ b ∧ y ∉ b #}"
proof -
have a: "⋀ b. b ∈# ℬ ⟹ ∀ x' ∈ {x, y} . x' ∉ b ⟹ x ∉ b ∧ y ∉ b"
by simp
have "⋀ b. b ∈# ℬ ⟹ x ∉ b ∧ y ∉ b ⟹ ∀ x' ∈ {x, y} . x' ∉ b "
by simp
thus ?thesis using assms a complement_index
by (smt (verit) filter_mset_cong)
qed

lemma complement_rep_number:
assumes "x ∈ 𝒱" and "ℬ rep x = r"
shows  "ℬ⇧C rep x = 𝖻 - r"
proof -
have r: "size {#b ∈# ℬ . x ∈ b#} = r" using assms by (simp add: point_replication_number_def)
then have a: "⋀ b . b ∈# ℬ ⟹ x ∈ b ⟹ x ∉ b⇧c"
have "⋀ b . b ∈# ℬ ⟹ x ∉ b ⟹ x ∈ b⇧c"
then have alt: "(image_mset block_complement ℬ) rep x = size {#b ∈# ℬ . x ∉ b#}"
using a filter_mset_cong image_mset_filter_swap2 point_replication_number_def
by (smt (verit, ccfv_SIG) size_image_mset)
have "𝖻 = size {#b ∈# ℬ . x ∈ b#} + size {#b ∈# ℬ . x ∉ b#}"
by (metis multiset_partition size_union)
thus ?thesis using alt
qed

lemma complement_blocks_wf: "bl ∈# ℬ⇧C ⟹ bl ⊆ 𝒱"
by (auto simp add: complement_blocks_def block_complement_def)

lemma complement_wf [intro]: "incidence_system 𝒱 ℬ⇧C"
using complement_blocks_wf by (unfold_locales)

interpretation sys_complement: incidence_system "𝒱" "ℬ⇧C"
using complement_wf by simp
end

context finite_incidence_system
begin
lemma block_complement_size: "b ⊆ 𝒱 ⟹ card (b⇧c) = card 𝒱 - card b"
by (simp add: block_complement_def card_Diff_subset finite_subset card_mono of_nat_diff finite_sets)

lemma block_comp_incomplete: "incomplete_block bl ⟹ card (bl⇧c) > 0"
using block_complement_size by (simp add: wellformed)

lemma  block_comp_incomplete_nempty: "incomplete_block bl ⟹ bl⇧c ≠ {}"
using wellformed block_complement_def finite_blocks
by (auto simp add: block_complement_size block_comp_incomplete card_subset_not_gt_card)

lemma incomplete_block_proper_subset: "incomplete_block bl ⟹ bl ⊂ 𝒱"
using wellformed by fastforce

lemma complement_finite: "finite_incidence_system 𝒱 ℬ⇧C"
using complement_wf finite_sets by (simp add: incidence_system.finite_sysI)

interpretation comp_fin: finite_incidence_system 𝒱 "ℬ⇧C"
using complement_finite by simp

end

context design
begin
lemma (in design) complement_design:
assumes "⋀ bl . bl ∈# ℬ ⟹ incomplete_block bl"
shows "design 𝒱 (ℬ⇧C)"
proof -
interpret fin: finite_incidence_system 𝒱 "ℬ⇧C" using complement_finite by simp
show ?thesis using assms block_comp_incomplete_nempty wellformed
by (unfold_locales) (auto simp add: complement_blocks_def)
qed

end
subsubsection ‹Multiples›
text ‹An easy way to construct new set systems is to simply multiply the block collection by some
constant›

context incidence_system
begin

abbreviation multiple_blocks :: "nat ⇒ 'a set multiset" where
"multiple_blocks n ≡ repeat_mset n ℬ"

lemma multiple_block_in_original: "b ∈# multiple_blocks n ⟹ b ∈# ℬ"

lemma multiple_block_in: "n > 0 ⟹ b ∈# ℬ ⟹  b ∈# multiple_blocks n"

lemma multiple_blocks_gt: "n > 0 ⟹ size (multiple_blocks n) ≥ size ℬ"
by (simp)

lemma block_original_count_le: "n > 0 ⟹ count ℬ b ≤ count (multiple_blocks n) b"
using count_repeat_mset by simp

lemma multiple_blocks_sub: "n > 0 ⟹ ℬ ⊆# (multiple_blocks n)"

lemma multiple_1_same: "multiple_blocks 1 = ℬ"
by simp

lemma multiple_unfold_1: "multiple_blocks (Suc n) = (multiple_blocks n) + ℬ"
by simp

lemma multiple_point_rep_num: "(multiple_blocks n) rep x = (ℬ rep x) * n"
proof (induction n)
case 0
then show ?case by (simp add: point_replication_number_def)
next
case (Suc n)
then have "multiple_blocks (Suc n) rep x = ℬ rep x * n + (ℬ rep x)"
using Suc.IH Suc.prems by (simp add: union_commute point_replication_number_def)
then show ?case
by (simp)
qed

lemma multiple_point_index: "(multiple_blocks n) index ps = (ℬ index ps) * n"
by (induction n) (auto simp add: points_index_def)

lemma repeat_mset_block_point_rel: "⋀b x. b ∈# multiple_blocks  n ⟹ x ∈ b ⟹ x ∈ 𝒱"
by (induction n) (auto, meson subset_iff wellformed)

lemma multiple_is_wellformed: "incidence_system 𝒱 (multiple_blocks n)"
using repeat_mset_subset_in wellformed repeat_mset_block_point_rel by (unfold_locales) (auto)

lemma  multiple_blocks_num [simp]: "size (multiple_blocks n) = n*𝖻"
by simp

interpretation mult_sys: incidence_system 𝒱 "(multiple_blocks n)"

lemma multiple_block_multiplicity [simp]: "mult_sys.multiplicity n bl = (multiplicity bl) * n"
by (simp)

lemma multiple_block_sizes_same:
assumes "n > 0"
shows "sys_block_sizes = mult_sys.sys_block_sizes n"
proof -
have def: "mult_sys.sys_block_sizes n = {card bl | bl. bl ∈# (multiple_blocks n)}"
then have eq: "⋀ bl. bl ∈# (multiple_blocks n) ⟷ bl ∈# ℬ"
using assms multiple_block_in multiple_block_in_original by blast
thus ?thesis using def by (simp add: sys_block_sizes_def eq)
qed

end

context finite_incidence_system
begin

lemma multiple_is_finite: "finite_incidence_system 𝒱 (multiple_blocks n)"
using multiple_is_wellformed finite_sets by (unfold_locales) (auto simp add: incidence_system_def)

end

context design
begin

lemma multiple_is_design: "design 𝒱 (multiple_blocks n)"
proof -
interpret fis: finite_incidence_system 𝒱 "multiple_blocks n" using multiple_is_finite by simp
show ?thesis using blocks_nempty
by (unfold_locales) (auto simp add: elem_in_repeat_in_original repeat_mset_not_empty)
qed

end

subsection ‹Simple Designs›

text ‹Simple designs are those in which the multiplicity of each block is at most one.
In other words, the block collection is a set. This can significantly ease reasoning.›

locale simple_incidence_system = incidence_system +
assumes simple [simp]: "bl ∈# ℬ ⟹ multiplicity bl = 1"

begin

lemma simple_alt_def_all: "∀ bl ∈# ℬ . multiplicity bl = 1"
using simple by auto

lemma simple_blocks_eq_sup: "mset_set (design_support) = ℬ"
using distinct_mset_def simple design_support_def by (metis distinct_mset_set_mset_ident)

lemma simple_block_size_eq_card: "𝖻 = card (design_support)"
by (metis simple_blocks_eq_sup size_mset_set)

lemma points_index_simple_def: "ℬ index ps = card {b ∈ design_support . ps ⊆ b}"
using design_support_def points_index_def card_size_filter_eq simple_blocks_eq_sup
by (metis finite_set_mset)

lemma replication_num_simple_def: "ℬ rep x = card {b ∈ design_support . x ∈ b}"
using design_support_def point_replication_number_def card_size_filter_eq simple_blocks_eq_sup
by (metis finite_set_mset)

end

locale simple_design = design + simple_incidence_system

context incidence_system
begin
lemma simple_not_multiplicity: "b ∈# ℬ ⟹ multiplicity  b > 1 ⟹ ¬ simple_incidence_system 𝒱 ℬ"
using simple_incidence_system_def simple_incidence_system_axioms_def by (metis nat_neq_iff)

lemma multiple_not_simple:
assumes "n > 1"
assumes "ℬ ≠ {#}"
shows "¬ simple_incidence_system 𝒱 (multiple_blocks n)"
proof (rule ccontr, simp)
assume "simple_incidence_system 𝒱 (multiple_blocks n)"
then have "⋀ bl. bl ∈# ℬ ⟹ count (multiple_blocks n) bl = 1"
using assms(1) elem_in_original_in_repeat
by (metis not_gr_zero not_less_zero simple_incidence_system.simple)
thus False using assms by auto
qed

end

subsection ‹Proper Designs›
text ‹Many types of designs rely on parameter conditions that only make sense for non-empty designs.
i.e. designs with at least one block, and therefore given well-formed condition, at least one point.
To this end we define the notion of a "proper" design›

locale proper_design = design +
assumes b_non_zero: "𝖻 ≠ 0"
begin

lemma is_proper: "proper_design 𝒱 ℬ" by intro_locales

lemma v_non_zero: "𝗏 > 0"
using b_non_zero v_eq0_imp_b_eq_0 by auto

lemma b_positive: "𝖻 > 0" using b_non_zero

lemma design_points_nempty: "𝒱 ≠ {}"
using v_non_zero by auto

lemma design_blocks_nempty: "ℬ ≠ {#}"
using b_non_zero by auto

end

text ‹Intro rules for a proper design›
lemma (in design) proper_designI[intro]: "𝖻 ≠ 0 ⟹ proper_design 𝒱 ℬ"
by (unfold_locales) simp

lemma proper_designII[intro]:
assumes "design V B" and "B ≠ {#}"
shows "proper_design V B"
proof -
interpret des: design V B using assms by simp
show ?thesis using assms by unfold_locales simp
qed

text ‹Reasoning on construction closure for proper designs›
context proper_design
begin

lemma multiple_proper_design:
assumes "n > 0"
shows "proper_design 𝒱 (multiple_blocks n)"
using multiple_is_design assms design_blocks_nempty multiple_block_in
by (metis block_set_nempty_imp_block_ex empty_iff proper_designII set_mset_empty)

lemma complement_proper_design:
assumes "⋀ bl . bl ∈# ℬ ⟹ incomplete_block bl"
shows "proper_design 𝒱 ℬ⇧C"
proof -
interpret des: design 𝒱 "ℬ⇧C"