Theory Design_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}"
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
by (simp add: wf_design)
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 𝒱) ×# ℬ) = 𝗏 * 𝖻"
by (simp add: size_cartesian_product)
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}"
by (simp add: point_replication_number_def)
lemma point_rep_number_split[simp]: "(A + B) rep x = A rep x + B rep x"
by (simp add: point_replication_number_def)
lemma point_rep_singleton_val [simp]: "x ∈ b ⟹ {#b#} rep x = 1"
by (simp add: point_replication_number_def)
lemma point_rep_singleton_inval [simp]: "x ∉ b ⟹ {#b#} rep x = 0"
by (simp add: point_replication_number_def)
context incidence_system
begin
lemma point_rep_number_alt_def: "ℬ rep x = size {# b ∈# ℬ . x ∈ b#}"
by (simp add: point_replication_number_def)
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"
by (simp add: points_index_def)
lemma point_index_distrib: "(B1 + B2) index ps = B1 index ps + B2 index ps"
by (simp add: points_index_def)
lemma point_index_diff: "B1 index ps = (B1 + B2) index ps - B2 index ps"
by (simp add: points_index_def)
lemma points_index_singleton: "{#b#} index ps = 1 ⟷ ps ⊆ b"
by (simp add: points_index_def)
lemma points_index_singleton_zero: "¬ (ps ⊆ b) ⟹ {#b#} index ps = 0"
by (simp add: points_index_def)
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)
lemma points_index_block_image_add_eq:
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}"
by (simp add: points_index_def assms)
lemma points_index_single_rep_num: "B index {x} = B rep x"
by (simp add: points_index_def point_replication_number_def)
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
add_mset_subseteq_single_iff assm mset_subset_eq_single size_single subseteq_mset_size_eql)
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#}"
by (simp add: points_index_def)
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)"
by (simp add: points_index_def size_mset_mono)
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"
by (simp add: intersection_number_def)
lemma intersection_number_empty_iff:
assumes "finite b1"
shows "b1 ∩ b2 = {} ⟷ b1 |∩| b2 = 0"
by (simp add: intersection_number_def assms)
lemma intersect_num_commute: "b1 |∩| b2 = b2 |∩| b1"
by (simp add: inf_commute intersection_number_def)
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 ≠ {}"
by (simp add: assms replication_numbers_def)
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"
by (auto simp add: replication_numbers_def)
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 ≠ {}"
by (simp add: sys_block_sizes_def assms)
lemma finite_block_sizes: "finite (sys_block_sizes)"
by (simp add: sys_block_sizes_def)
lemma block_sizes_non_empty:
assumes "ℬ ≠ {#}"
shows "card (sys_block_sizes) > 0"
using finite_block_sizes block_sizes_non_empty_set
by (simp add: assms card_gt_0_iff)
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)"
by (auto simp add: sys_block_sizes_def)
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"
by (auto simp add: intersection_numbers_def)
lemma intersect_num_in_set: "b1 ∈# ℬ ⟹ b2 ∈# (ℬ - {#b1#}) ⟹ b1 |∩| b2 ∈ intersection_numbers"
by (auto simp add: intersection_numbers_def)
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"
by (auto simp add: point_indices_def)
lemma point_indices_alt_def: "point_indices t = { ℬ index ps | ps. card ps = t ∧ ps ⊆ 𝒱}"
by (simp add: point_indices_def)
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 ℬ"
by (simp add: complement_blocks_def)
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"
by (auto simp add: block_complement_elem_iff)
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 #}"
by (simp add: complement_blocks_def points_index_def)
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"
by (simp add: block_complement_def)
have "⋀ b . b ∈# ℬ ⟹ x ∉ b ⟹ x ∈ b⇧c"
by (simp add: assms(1) block_complement_def)
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
by (simp add: r complement_blocks_def)
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 ∈# ℬ"
by (simp add: elem_in_repeat_in_original)
lemma multiple_block_in: "n > 0 ⟹ b ∈# ℬ ⟹ b ∈# multiple_blocks n"
by (simp add: elem_in_original_in_repeat)
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)"
by (simp add: mset_subset_eqI block_original_count_le)
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)"
by (simp add: multiple_is_wellformed)
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)}"
by (simp add: mult_sys.sys_block_sizes_def)
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
text ‹Additional reasoning about when something is not simple›
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
by (simp add: nonempty_has_size)
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"
by (simp add: assms complement_design)
show ?thesis using b_non_zero by (unfold_locales) auto
qed
end
end