Theory Design_Theory.BIBD
theory BIBD imports Block_Designs
begin
section ‹BIBD's›
text ‹BIBD's are perhaps the most commonly studied type of design in combinatorial design theory,
and usually the first type of design explored in a design theory course.
These designs are a type of t-design, where $t = 2$›
subsection ‹BIBD Basics›
locale bibd = t_design 𝒱 ℬ 𝗄 2 Λ
for point_set ("𝒱") and block_collection ("ℬ")
and u_block_size ("𝗄") and index ("Λ")
begin
lemma min_block_size_2: "𝗄 ≥ 2"
using block_size_t by simp
lemma points_index_pair: "y ∈ 𝒱 ⟹ x ∈ 𝒱 ⟹ x ≠ y ⟹ size ({# bl ∈# ℬ . {x, y} ⊆ bl#}) = Λ"
using balanced card_2_iff empty_subsetI insert_subset points_index_def by metis
lemma index_one_empty_rm_blv [simp]:
assumes "Λ = 1" and " blv ∈# ℬ" and "p ⊆ blv" and "card p = 2"
shows "{#bl ∈# remove1_mset blv ℬ . p ⊆ bl#} = {#}"
proof -
have blv_in: "blv ∈# filter_mset ((⊆) p) ℬ"
using assms by simp
have "p ⊆ 𝒱" using assms wellformed by auto
then have "size (filter_mset ((⊆) p) ℬ) = 1"
using balanced assms by (simp add: points_index_def)
then show ?thesis using blv_in filter_diff_mset filter_single_mset
by (metis (no_types, lifting) add_mset_eq_single assms(3) insert_DiffM size_1_singleton_mset)
qed
lemma index_one_alt_bl_not_exist:
assumes "Λ = 1" and " blv ∈# ℬ" and "p ⊆ blv" and "card p = 2"
shows" ⋀ bl. bl ∈# remove1_mset blv ℬ ⟹ ¬ (p ⊆ bl) "
using index_one_empty_rm_blv
by (metis assms(1) assms(2) assms(3) assms(4) filter_mset_empty_conv)
subsection ‹Necessary Conditions for Existence›
text ‹The necessary conditions on the existence of a $(v, k, \lambda)$-bibd are one of the
fundamental first theorems on designs. Proofs based off MATH3301 lecture notes \<^cite>‹"HerkeLectureNotes2016"›
and Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››
lemma necess_cond_1_rhs:
assumes "x ∈ 𝒱"
shows "size ({# p ∈# (mset_set (𝒱 - {x}) ×# {# bl ∈# ℬ . x ∈ bl #}). fst p ∈ snd p#}) = Λ * (𝗏- 1)"
proof -
let ?M = "mset_set (𝒱 - {x})"
let ?B = "{# bl ∈# ℬ . x ∈ bl #}"
have m_distinct: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp
have y_point: "⋀ y . y ∈# ?M ⟹ y ∈ 𝒱" using assms
by (simp add: finite_sets)
have b_contents: "⋀ bl. bl ∈# ?B ⟹ x ∈ bl" using assms by auto
have "⋀ y. y ∈# ?M ⟹ y ≠ x" using assms
by (simp add: finite_sets)
then have "⋀ y .y ∈# ?M ⟹ size ({# bl ∈# ?B . {x, y} ⊆ bl#}) = Λ"
using points_index_pair filter_filter_mset_ss_member y_point assms finite_sets
by metis
then have "⋀ y .y ∈# ?M ⟹ size ({# bl ∈# ?B . x ∈ bl ∧ y ∈ bl#}) = Λ"
by auto
then have bl_set_size: "⋀ y . y ∈# ?M ⟹ size ({# bl ∈# ?B . y ∈ bl#}) = Λ"
using b_contents by (metis (no_types, lifting) filter_mset_cong)
then have final_size: "size (∑p∈#?M . ({#p#} ×# {#bl ∈# ?B. p ∈ bl#})) = size (?M) * Λ"
using m_distinct size_Union_distinct_cart_prod_filter bl_set_size by blast
have "size ?M = 𝗏 - 1" using v_non_zero
by (simp add: assms(1) finite_sets)
thus ?thesis using final_size
by (simp add: set_break_down_left)
qed
lemma necess_cond_1_lhs:
assumes "x ∈ 𝒱"
shows "size ({# p ∈# (mset_set (𝒱 - {x}) ×# {# bl ∈# ℬ . x ∈ bl #}). fst p ∈ snd p#})
= (ℬ rep x) * (𝗄 - 1)"
(is "size ({# p ∈# (?M ×# ?B). fst p ∈ snd p#}) = (ℬ rep x) * (𝗄 - 1) ")
proof -
have "⋀ y. y ∈# ?M ⟹ y ≠ x" using assms
by (simp add: finite_sets)
have distinct_m: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp
have finite_M: "finite (𝒱 - {x})" using finite_sets by auto
have block_choices: "size ?B = ℬ rep x"
by (simp add: assms(1) point_replication_number_def)
have bl_size: "∀ bl ∈# ?B. card {p ∈ 𝒱 . p ∈ bl } = 𝗄 " using uniform_unfold_point_set by simp
have x_in_set: "∀ bl ∈# ?B . {x} ⊆ {p ∈ 𝒱. p ∈ bl}" using assms by auto
then have "∀ bl ∈# ?B. card {p ∈ (𝒱 - {x}) . p ∈ bl } = card ({p ∈ 𝒱 . p ∈ bl } - {x})"
by (simp add: set_filter_diff_card)
then have "∀ bl ∈# ?B. card {p ∈ (𝒱 - {x}) . p ∈ bl } = 𝗄 - 1"
using bl_size x_in_set card_Diff_subset finite_sets k_non_zero by auto
then have "⋀ bl . bl ∈# ?B ⟹ size {#p ∈# ?M . p ∈ bl#} = 𝗄 - 1"
using assms finite_M card_size_filter_eq by auto
then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * (𝗄 - 1)"
using distinct_m size_Union_distinct_cart_prod_filter2 by blast
thus ?thesis using block_choices k_non_zero by (simp add: set_break_down_right)
qed
lemma r_constant: "x ∈ 𝒱 ⟹ (ℬ rep x) * (𝗄 -1) = Λ * (𝗏 - 1)"
using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty by force
lemma replication_number_value:
assumes "x ∈ 𝒱"
shows "(ℬ rep x) = Λ * (𝗏 - 1) div (𝗄 - 1)"
using min_block_size_2 r_constant assms
by (metis diff_is_0_eq diffs0_imp_equal div_by_1 k_non_zero nonzero_mult_div_cancel_right
one_div_two_eq_zero one_le_numeral zero_neq_one)
lemma r_constant_alt: "∀ x ∈ 𝒱. ℬ rep x = Λ * (𝗏 - 1) div (𝗄 - 1)"
using r_constant replication_number_value by blast
end
text ‹Using the first necessary condition, it is possible to show that a bibd has
a constant replication number›
sublocale bibd ⊆ constant_rep_design 𝒱 ℬ "(Λ * (𝗏 - 1) div (𝗄 - 1))"
using r_constant_alt by (unfold_locales) simp_all
lemma (in t_design) bibdI [intro]: "𝗍 = 2 ⟹ bibd 𝒱 ℬ 𝗄 Λ⇩t"
using t_lt_order block_size_t by (unfold_locales) (simp_all)
context bibd
begin
abbreviation "𝗋 ≡ (Λ * (𝗏 - 1) div (𝗄 - 1))"
lemma necessary_condition_one:
shows "𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)"
using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty rep_number by auto
lemma bibd_point_occ_rep:
assumes "x ∈ bl"
assumes "bl ∈# ℬ"
shows "(ℬ - {#bl#}) rep x = 𝗋 - 1"
proof -
have xin: "x ∈ 𝒱" using assms wf_invalid_point by blast
then have rep: "size {# blk ∈# ℬ. x ∈ blk #} = 𝗋" using rep_number_unfold_set by simp
have "(ℬ - {#bl#}) rep x = size {# blk ∈# (ℬ - {#bl#}). x ∈ blk #}"
by (simp add: point_replication_number_def)
then have "(ℬ - {#bl#}) rep x = size {# blk ∈# ℬ. x ∈ blk #} - 1"
by (simp add: assms size_Diff_singleton)
then show ?thesis using assms rep r_gzero by simp
qed
lemma necess_cond_2_lhs: "size {# x ∈# (mset_set 𝒱 ×# ℬ) . (fst x) ∈ (snd x) #} = 𝗏 * 𝗋"
proof -
let ?M = "mset_set 𝒱"
have "⋀ p . p ∈# ?M ⟹ size ({# bl ∈# ℬ . p ∈ bl #}) = 𝗋"
using finite_sets rep_number_unfold_set r_gzero nat_eq_iff2 by auto
then have "size (∑p∈#?M. ({#p#} ×# {#bl ∈# ℬ. p ∈ bl#})) = size ?M * (𝗋)"
using mset_points_distinct size_Union_distinct_cart_prod_filter by blast
thus ?thesis using r_gzero
by (simp add: set_break_down_left)
qed
lemma necess_cond_2_rhs: "size {# x ∈# (mset_set 𝒱 ×# ℬ) . (fst x) ∈ (snd x) #} = 𝖻*𝗄"
(is "size {# x ∈# (?M ×# ?B). (fst x) ∈ (snd x) #} = 𝖻*𝗄")
proof -
have "⋀ bl . bl ∈# ?B ⟹ size ({# p ∈# ?M . p ∈ bl #}) = 𝗄"
using uniform k_non_zero uniform_unfold_point_set_mset by fastforce
then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * 𝗄"
using mset_points_distinct size_Union_distinct_cart_prod_filter2 by blast
thus ?thesis using k_non_zero by (simp add: set_break_down_right)
qed
lemma necessary_condition_two:
shows "𝗏 * 𝗋 = 𝖻 * 𝗄"
using necess_cond_2_lhs necess_cond_2_rhs by simp
theorem admissability_conditions:
"𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)"
"𝗏 * 𝗋 = 𝖻 * 𝗄"
using necessary_condition_one necessary_condition_two by auto
subsubsection ‹BIBD Param Relationships›
lemma bibd_block_number: "𝖻 = Λ * 𝗏 * (𝗏 - 1) div (𝗄 * (𝗄-1))"
proof -
have "𝖻 * 𝗄 = (𝗏 * 𝗋)" using necessary_condition_two by simp
then have k_dvd: "𝗄 dvd (𝗏 * 𝗋)" by (metis dvd_triv_right)
then have "𝖻 = (𝗏 * 𝗋) div 𝗄" using necessary_condition_two min_block_size_2 by auto
then have "𝖻 = (𝗏 * ((Λ * (𝗏 - 1) div (𝗄 - 1)))) div 𝗄" by simp
then have "𝖻 = (𝗏 * Λ * (𝗏 - 1)) div ((𝗄 - 1)* 𝗄)" using necessary_condition_one
necessary_condition_two dvd_div_div_eq_mult dvd_div_eq_0_iff dvd_triv_right mult.assoc
mult.commute mult.left_commute mult_eq_0_iff
by (smt (z3) b_non_zero)
then show ?thesis by (simp add: mult.commute)
qed
lemma symmetric_condition_1: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1) ⟹ 𝖻 = 𝗏 ∧ 𝗋 = 𝗄"
using b_non_zero bibd_block_number mult_eq_0_iff necessary_condition_two necessary_condition_one
by auto
lemma index_lt_replication: "Λ < 𝗋"
proof -
have 1: "𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)" using admissability_conditions by simp
have lhsnot0: "𝗋 * (𝗄 - 1) ≠ 0"
using no_zero_divisors rep_not_zero by (metis div_by_0)
then have rhsnot0: "Λ * (𝗏 - 1) ≠ 0" using 1 by presburger
have "𝗄 - 1 < 𝗏 - 1" using incomplete b_non_zero bibd_block_number not_less_eq by fastforce
thus ?thesis using 1 lhsnot0 rhsnot0 k_non_zero mult_le_less_imp_less r_gzero
by (metis div_greater_zero_iff less_or_eq_imp_le nat_less_le nat_neq_iff)
qed
lemma index_not_zero: "Λ ≥ 1"
by (metis div_0 leI less_one mult_not_zero rep_not_zero)
lemma r_ge_two: "𝗋 ≥ 2"
using index_lt_replication index_not_zero by linarith
lemma block_num_gt_rep: "𝖻 > 𝗋"
proof -
have fact: "𝖻 * 𝗄 = 𝗏 * 𝗋" using admissability_conditions by auto
have lhsnot0: "𝖻 * 𝗄 ≠ 0" using k_non_zero b_non_zero by auto
then have rhsnot0: "𝗏 * 𝗋 ≠ 0" using fact by simp
then show ?thesis using incomplete lhsnot0
using complement_rep_number constant_rep_design.r_gzero incomplete_imp_incomp_block by fastforce
qed
lemma bibd_subset_occ:
assumes "x ⊆ bl" and "bl ∈# ℬ" and "card x = 2"
shows "size {# blk ∈# (ℬ - {#bl#}). x ⊆ blk #} = Λ - 1"
proof -
have index: "size {# blk ∈# ℬ. x ⊆ blk #} = Λ" using points_index_def balanced assms
by (metis (full_types) subset_eq wf_invalid_point)
then have "size {# blk ∈# (ℬ - {#bl#}). x ⊆ blk #} = size {# blk ∈# ℬ. x ⊆ blk #} - 1"
by (simp add: assms size_Diff_singleton)
then show ?thesis using assms index_not_zero index by simp
qed
lemma necess_cond_one_param_balance: "𝖻 > 𝗏 ⟹ 𝗋 > 𝗄"
using necessary_condition_two b_positive
by (metis div_le_mono2 div_mult_self1_is_m div_mult_self_is_m nat_less_le r_gzero v_non_zero)
subsection ‹Constructing New bibd's›
text ‹There are many constructions on bibd's to establish new bibds (or other types of designs).
This section demonstrates this using both existing constructions, and by defining new constructions.›
subsubsection ‹BIBD Complement, Multiple, Combine›
lemma comp_params_index_pair:
assumes "{x, y} ⊆ 𝒱"
assumes "x ≠ y"
shows "ℬ⇧C index {x, y} = 𝖻 + Λ - 2*𝗋"
proof -
have xin: "x ∈ 𝒱" and yin: "y ∈ 𝒱" using assms by auto
have ge: "2*𝗋 ≥ Λ" using index_lt_replication
using r_gzero by linarith
have lambda: "size {# b ∈# ℬ . x ∈ b ∧ y ∈ b#} = Λ" using points_index_pair assms by simp
have s1: "ℬ⇧C index {x, y} = size {# b ∈# ℬ . x ∉ b ∧ y ∉ b #}"
using complement_index_2 assms by simp
also have s2: "... = size ℬ - (size {# b ∈# ℬ . ¬ (x ∉ b ∧ y ∉ b) #})"
using size_filter_neg by blast
also have "... = size ℬ - (size {# b ∈# ℬ . x ∈ b ∨ y ∈ b#})" by auto
also have "... = 𝖻 - (size {# b ∈# ℬ . x ∈ b ∨ y ∈ b#})" by (simp add: of_nat_diff)
finally have "ℬ⇧C index {x, y} = 𝖻 - (size {# b ∈# ℬ . x ∈ b#} +
size {# b ∈# ℬ . y ∈ b#} - size {# b ∈# ℬ . x ∈ b ∧ y ∈ b#})"
by (simp add: mset_size_partition_dep s2 s1)
then have "ℬ⇧C index {x, y} = 𝖻 - (𝗋 + 𝗋 - Λ)" using rep_number_unfold_set lambda xin yin
by presburger
then have "ℬ⇧C index {x, y} = 𝖻 - (2*𝗋 - Λ)"
using index_lt_replication by (metis mult_2)
thus ?thesis using ge diff_diff_right by simp
qed
lemma complement_bibd_index:
assumes "ps ⊆ 𝒱"
assumes "card ps = 2"
shows "ℬ⇧C index ps = 𝖻 + Λ - 2*𝗋"
proof -
obtain x y where set: "ps = {x, y}" using b_non_zero bibd_block_number diff_is_0_eq incomplete
mult_0_right nat_less_le design_points_nempty assms by (metis card_2_iff)
then have "x ≠ y" using assms by auto
thus ?thesis using comp_params_index_pair assms
by (simp add: set)
qed
lemma complement_bibd:
assumes "𝗄 ≤ 𝗏 - 2"
shows "bibd 𝒱 ℬ⇧C (𝗏 - 𝗄) (𝖻 + Λ - 2*𝗋)"
proof -
interpret des: incomplete_design 𝒱 "ℬ⇧C" "(𝗏 - 𝗄)"
using assms complement_incomplete by blast
show ?thesis proof (unfold_locales, simp_all)
show "2 ≤ des.𝗏" using assms block_size_t by linarith
show "⋀ps. ps ⊆ 𝒱 ⟹ card ps = 2 ⟹
ℬ⇧C index ps = 𝖻 + Λ - 2 * (Λ * (des.𝗏 - Suc 0) div (𝗄 - Suc 0))"
using complement_bibd_index by simp
show "2 ≤ des.𝗏 - 𝗄" using assms block_size_t by linarith
qed
qed
lemma multiple_bibd: "n > 0 ⟹ bibd 𝒱 (multiple_blocks n) 𝗄 (Λ * n)"
using multiple_t_design by (simp add: bibd_def)
end
locale two_bibd_eq_points = two_t_designs_eq_points 𝒱 ℬ 𝗄 ℬ' 2 Λ Λ'
+ des1: bibd 𝒱 ℬ 𝗄 Λ + des2: bibd 𝒱 ℬ' 𝗄 Λ' for 𝒱 ℬ 𝗄 ℬ' Λ Λ'
begin
lemma combine_is_bibd: "bibd 𝒱⇧+ ℬ⇧+ 𝗄 (Λ + Λ')"
by (unfold_locales)
sublocale combine_bibd: bibd "𝒱⇧+" "ℬ⇧+" "𝗄" "(Λ + Λ')"
by (unfold_locales)
end
subsubsection ‹Derived Designs›
text ‹A derived bibd takes a block from a valid bibd as the new point sets, and the intersection
of that block with other blocks as it's block set›
locale bibd_block_transformations = bibd +
fixes block :: "'a set" ("bl")
assumes valid_block: "bl ∈# ℬ"
begin
definition derived_blocks :: "'a set multiset" ("(ℬ⇧D)") where
"ℬ⇧D ≡ {# bl ∩ b . b ∈# (ℬ - {#bl#}) #}"
lemma derive_define_flip: "{# b ∩ bl . b ∈# (ℬ - {#bl#}) #} = ℬ⇧D"
by (simp add: derived_blocks_def inf_sup_aci(1))
lemma derived_points_order: "card bl = 𝗄"
using uniform valid_block by simp
lemma derived_block_num: "bl ∈# ℬ ⟹ size ℬ⇧D = 𝖻 - 1"
by (simp add: derived_blocks_def size_remove1_mset_If valid_block)
lemma derived_is_wellformed: "b ∈# ℬ⇧D ⟹ b ⊆ bl"
by (simp add: derived_blocks_def valid_block) (auto)
lemma derived_point_subset_orig: "ps ⊆ bl ⟹ ps ⊂ 𝒱"
by (simp add: valid_block incomplete_imp_proper_subset subset_psubset_trans)
lemma derived_obtain_orig_block:
assumes "b ∈# ℬ⇧D"
obtains b2 where "b = b2 ∩ bl" and "b2 ∈# remove1_mset bl ℬ"
using assms derived_blocks_def by auto
sublocale derived_incidence_sys: incidence_system "bl" "ℬ⇧D"
using derived_is_wellformed valid_block by (unfold_locales) (auto)
sublocale derived_fin_incidence_system: finite_incidence_system "bl" "ℬ⇧D"
using valid_block finite_blocks by (unfold_locales) simp_all
lemma derived_blocks_nempty:
assumes "⋀ b .b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0"
assumes "bld ∈# ℬ⇧D"
shows "bld ≠ {}"
proof -
obtain bl2 where inter: "bld = bl2 ∩ bl" and member: "bl2 ∈# remove1_mset bl ℬ"
using assms derived_obtain_orig_block by blast
then have "bl |∩| bl2 > 0" using assms(1) by blast
thus ?thesis using intersection_number_empty_iff finite_blocks valid_block
by (metis Int_commute dual_order.irrefl inter)
qed
lemma derived_is_design:
assumes "⋀ b. b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0"
shows "design bl ℬ⇧D"
proof -
interpret fin: finite_incidence_system "bl" "ℬ⇧D"
by (unfold_locales)
show ?thesis using assms derived_blocks_nempty by (unfold_locales) simp
qed
lemma derived_is_proper:
assumes "⋀ b. b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0"
shows "proper_design bl ℬ⇧D"
proof -
interpret des: design "bl" "ℬ⇧D"
using derived_is_design assms by fastforce
have "𝖻 - 1 > 1" using block_num_gt_rep r_ge_two by linarith
then show ?thesis by (unfold_locales) (simp add: derived_block_num valid_block)
qed
subsubsection ‹Residual Designs›
text ‹Similar to derived designs, a residual design takes the complement of a block bl as it's new
point set, and the complement of all other blocks with respect to bl.›
definition residual_blocks :: "'a set multiset" ("(ℬ⇧R)") where
"ℬ⇧R ≡ {# b - bl . b ∈# (ℬ - {#bl#}) #}"
lemma residual_order: "card (bl⇧c) = 𝗏 - 𝗄"
by (simp add: valid_block wellformed block_complement_size)
lemma residual_block_num: "size (ℬ⇧R) = 𝖻 - 1"
using b_positive by (simp add: residual_blocks_def size_remove1_mset_If valid_block int_ops(6))
lemma residual_obtain_orig_block:
assumes "b ∈# ℬ⇧R"
obtains bl2 where "b = bl2 - bl" and "bl2 ∈# remove1_mset bl ℬ"
using assms residual_blocks_def by auto
lemma residual_blocks_ss: assumes "b ∈# ℬ⇧R" shows "b ⊆ 𝒱"
proof -
have "b ⊆ (bl⇧c)" using residual_obtain_orig_block
by (metis Diff_mono assms block_complement_def in_diffD order_refl wellformed)
thus ?thesis
using block_complement_subset_points by auto
qed
lemma residual_blocks_exclude: "b ∈# ℬ⇧R ⟹ x ∈ b ⟹ x ∉ bl"
using residual_obtain_orig_block by auto
lemma residual_is_wellformed: "b ∈# ℬ⇧R ⟹ b ⊆ (bl⇧c)"
apply (auto simp add: residual_blocks_def)
by (metis DiffI block_complement_def in_diffD wf_invalid_point)
sublocale residual_incidence_sys: incidence_system "bl⇧c" "ℬ⇧R"
using residual_is_wellformed by (unfold_locales)
lemma residual_is_finite: "finite (bl⇧c)"
by (simp add: block_complement_def finite_sets)
sublocale residual_fin_incidence_sys: finite_incidence_system "bl⇧c" "ℬ⇧R"
using residual_is_finite by (unfold_locales)
lemma residual_blocks_nempty:
assumes "bld ∈# ℬ⇧R"
assumes "multiplicity bl = 1"
shows "bld ≠ {}"
proof -
obtain bl2 where inter: "bld = bl2 - bl" and member: "bl2 ∈# remove1_mset bl ℬ"
using assms residual_blocks_def by auto
then have ne: "bl2 ≠ bl" using assms
by (metis count_eq_zero_iff in_diff_count less_one union_single_eq_member)
have "card bl2 = card bl" using uniform valid_block member
using in_diffD by fastforce
then have "card (bl2 - bl) > 0"
using finite_blocks member uniform set_card_diff_ge_zero valid_block by (metis in_diffD ne)
thus ?thesis using inter by fastforce
qed
lemma residual_is_design: "multiplicity bl = 1 ⟹ design (bl⇧c) ℬ⇧R"
using residual_blocks_nempty by (unfold_locales)
lemma residual_is_proper:
assumes "multiplicity bl = 1"
shows "proper_design (bl⇧c) ℬ⇧R"
proof -
interpret des: design "bl⇧c" "ℬ⇧R" using residual_is_design assms by blast
have "𝖻 - 1 > 1" using r_ge_two block_num_gt_rep by linarith
then show ?thesis using residual_block_num by (unfold_locales) auto
qed
end
subsection ‹Symmetric BIBD's›
text ‹Symmetric bibd's are those where the order of the design equals the number of blocks›
locale symmetric_bibd = bibd +
assumes symmetric: "𝖻 = 𝗏"
begin
lemma rep_value_sym: "𝗋 = 𝗄"
using b_non_zero local.symmetric necessary_condition_two by auto
lemma symmetric_condition_2: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1)"
using necessary_condition_one rep_value_sym by auto
lemma sym_design_vk_gt_kl:
assumes "𝗄 ≥ Λ + 2"
shows "𝗏 - 𝗄 > 𝗄 - Λ"
proof (rule ccontr)
define k l v where kdef: "k ≡ int 𝗄" and ldef: "l ≡ int Λ" and vdef: "v ≡ int 𝗏"
assume "¬ (𝗏 - 𝗄 > 𝗄 - Λ)"
then have a: "¬ (v - k > k - l)" using kdef ldef vdef
by (metis block_size_lt_v index_lt_replication less_imp_le_nat of_nat_diff of_nat_less_imp_less
rep_value_sym)
have lge: "l ≥ 0" using ldef by simp
have sym: "l * (v- 1) = k * (k - 1)"
using symmetric_condition_2 ldef vdef kdef
by (metis (mono_tags, lifting) block_size_lt_v int_ops(2) k_non_zero le_trans of_nat_diff of_nat_mult)
then have "v ≤ 2 * k - l" using a by linarith
then have "v - 1 ≤ 2 * k - l - 1" by linarith
then have "l* (v - 1) ≤ l*( 2 * k - l - 1)"
using lge mult_le_cancel_left by fastforce
then have "k * (k - 1) ≤ l*( 2 * k - l - 1)"
by (simp add: sym)
then have "k * (k - 1) - l*( 2 * k - l - 1) ≤ 0" by linarith
then have "k^2 - k - l* 2 * k + l^2 + l ≤ 0" using mult.commute right_diff_distrib'
by (smt (z3) mult_cancel_left1 power2_diff ring_class.ring_distribs(2))
then have "(k - l)*(k - l - 1) ≤ 0" using mult.commute right_diff_distrib'
by (smt (z3) ‹k * (k - 1) ≤ l * (2 * k - l - 1)› combine_common_factor)
then have "k = l ∨ k = l + 1"
using mult_le_0_iff by force
thus False using assms kdef ldef by auto
qed
end
context bibd
begin
lemma symmetric_bibdI: "𝖻 = 𝗏 ⟹ symmetric_bibd 𝒱 ℬ 𝗄 Λ"
by unfold_locales simp
lemma symmetric_bibdII: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1) ⟹ symmetric_bibd 𝒱 ℬ 𝗄 Λ"
using symmetric_condition_1 by unfold_locales blast
lemma symmetric_not_admissable: "Λ * (𝗏 - 1) ≠ 𝗄 * (𝗄 - 1) ⟹ ¬ symmetric_bibd 𝒱 ℬ 𝗄 Λ"
using symmetric_bibd.symmetric_condition_2 by blast
end
context symmetric_bibd
begin
subsubsection ‹Intersection Property on Symmetric BIBDs›
text ‹Below is a proof of an important property on symmetric BIBD's regarding the equivalence
of intersection numbers and the design index. This is an intuitive counting proof, and involved
significantly more work in a formal environment. Based of Lecture Note \<^cite>‹"HerkeLectureNotes2016"››
lemma intersect_mult_set_eq_block:
assumes "blv ∈# ℬ"
shows "p ∈# ∑⇩#{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#} ⟷ p ∈ blv"
proof (auto, simp add: assms finite_blocks)
assume assm: "p ∈ blv"
then have "(ℬ - {#blv#}) rep p > 0" using bibd_point_occ_rep r_ge_two assms by auto
then obtain bl where "bl ∈# (ℬ - {#blv#}) ∧ p ∈ bl" using assms rep_number_g0_exists by metis
then show "∃x∈#remove1_mset blv ℬ. p ∈# mset_set (x ∩ blv)"
using assms assm finite_blocks by auto
qed
lemma intersect_mult_set_block_subset_iff:
assumes "blv ∈# ℬ"
assumes "p ∈# ∑⇩#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}"
shows "p ⊆ blv"
proof (rule subsetI)
fix x
assume asm: "x ∈ p"
obtain b2 where "p ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})"
using assms by blast
then have "p ⊆ blv ∩ b2"
by (metis (no_types, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq)
thus "x ∈ blv" using asm by auto
qed
lemma intersect_mult_set_block_subset_card:
assumes "blv ∈# ℬ"
assumes "p ∈# ∑⇩#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}"
shows "card p = 2"
proof -
obtain b2 where "p ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})"
using assms by blast
thus ?thesis
by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq)
qed
lemma intersect_mult_set_block_with_point_exists:
assumes "blv ∈# ℬ" and "p ⊆ blv" and "Λ ≥ 2" and "card p = 2"
shows "∃x∈#remove1_mset blv ℬ. p ∈# mset_set {y. y ⊆ blv ∧ y ⊆ x ∧ card y = 2}"
proof -
have "size {#b ∈# ℬ . p ⊆ b#} = Λ" using points_index_def assms
by (metis balanced_alt_def_all dual_order.trans wellformed)
then have "size {#bl ∈# (ℬ - {#blv#}) . p ⊆ bl#} ≥ 1"
using assms by (simp add: size_Diff_singleton)
then obtain bl where "bl ∈# (ℬ - {#blv#}) ∧ p ⊆ bl" using assms filter_mset_empty_conv
by (metis diff_diff_cancel diff_is_0_eq' le_numeral_extra(4) size_empty zero_neq_one)
thus ?thesis
using assms finite_blocks by auto
qed
lemma intersect_mult_set_block_subset_iff_2:
assumes "blv ∈# ℬ" and "p ⊆ blv" and "Λ ≥ 2" and "card p = 2"
shows "p ∈# ∑⇩#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}"
by (auto simp add: intersect_mult_set_block_with_point_exists assms)
lemma sym_sum_mset_inter_sets_count:
assumes "blv ∈# ℬ"
assumes "p ∈ blv"
shows "count (∑⇩#{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) p = 𝗋 - 1"
(is "count (∑⇩#?M) p = 𝗋 - 1")
proof -
have size_inter: "size {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} = 𝗋 - 1"
using bibd_point_occ_rep point_replication_number_def
by (metis assms(1) assms(2) size_image_mset)
have inter_finite: "∀ bl ∈# (ℬ - {#blv#}) . finite (bl ∩ blv)"
by (simp add: assms(1) finite_blocks)
have "⋀ bl . bl ∈# (ℬ - {#blv#}) ⟹ p ∈ bl ⟶ count (mset_set (bl ∩ blv)) p = 1"
using assms count_mset_set(1) inter_finite by simp
then have "⋀ bl . bl ∈# {#b1 ∈#(ℬ - {#blv#}) . p ∈ b1#} ⟹ count (mset_set (bl ∩ blv)) p = 1"
by (metis (full_types) count_eq_zero_iff count_filter_mset)
then have pin: "⋀ P. P ∈# {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#}
⟹ count P p = 1" by blast
have "?M = {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#}
+ {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∉ bl#}"
by (metis image_mset_union multiset_partition)
then have "count (∑⇩#?M) p = size {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} "
using pin by (auto simp add: count_sum_mset)
then show ?thesis using size_inter by linarith
qed
lemma sym_sum_mset_inter_sets_size:
assumes "blv ∈# ℬ"
shows "size (∑⇩#{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) = 𝗄 * (𝗋 - 1)"
(is "size (∑⇩#?M) = 𝗄* (𝗋 - 1)")
proof -
have eq: "set_mset (∑⇩#{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) = blv"
using intersect_mult_set_eq_block assms by auto
then have k: "card (set_mset (∑⇩#?M)) = 𝗄"
by (simp add: assms)
have "⋀ p. p ∈# (∑⇩#?M) ⟹ count (∑⇩#?M) p = 𝗋 - 1"
using sym_sum_mset_inter_sets_count assms eq by blast
thus ?thesis using k size_multiset_set_mset_const_count by metis
qed
lemma sym_sum_inter_num:
assumes "b1 ∈# ℬ"
shows "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = 𝗄* (𝗋 - 1)"
proof -
have "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = (∑b2 ∈#(ℬ - {#b1#}). size (mset_set (b1 ∩ b2)))"
by (simp add: intersection_number_def)
also have "... = size (∑⇩#{#mset_set (b1 ∩ bl). bl ∈# (ℬ - {#b1#})#})"
by (auto simp add: size_big_union_sum)
also have "... = size (∑⇩#{#mset_set (bl ∩ b1). bl ∈# (ℬ - {#b1#})#})"
by (metis Int_commute)
finally have "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = 𝗄 * (𝗋 - 1)"
using sym_sum_mset_inter_sets_size assms by auto
then show ?thesis by simp
qed
lemma sym_sum_mset_inter2_sets_count:
assumes "blv ∈# ℬ"
assumes "p ⊆ blv"
assumes "card p = 2"
shows "count (∑⇩#{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (ℬ - {#blv#})#}) p = Λ - 1"
(is "count (∑⇩#?M) p = Λ - 1")
proof -
have size_inter: "size {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#}
= Λ - 1"
using bibd_subset_occ assms by simp
have "∀ b2 ∈# (ℬ - {#blv#}) . p ⊆ b2 ⟶ count (mset_set{y .y ⊆ blv ∩ b2 ∧ card y = 2}) p = 1"
using assms(2) count_mset_set(1) assms(3) by (auto simp add: assms(1) finite_blocks)
then have "∀ bl ∈# {#b1 ∈#(ℬ - {#blv#}) . p ⊆ b1#}.
count (mset_set {y .y ⊆ blv ∩ bl ∧ card y = 2}) p = 1"
using count_eq_zero_iff count_filter_mset by (metis (no_types, lifting))
then have pin: "∀ P ∈# {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#}.
count P p = 1"
using count_eq_zero_iff count_filter_mset by blast
have "?M = {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#} +
{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . ¬ (p ⊆ b2)#}"
by (metis image_mset_union multiset_partition)
then have "count (∑⇩#?M) p =
size {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#}"
using pin by (auto simp add: count_sum_mset)
then show ?thesis using size_inter by linarith
qed
lemma sym_sum_mset_inter2_sets_size:
assumes "blv ∈# ℬ"
shows "size (∑⇩#{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (ℬ - {#blv#})#}) =
( 𝗄 choose 2) * (Λ -1)"
(is "size (∑⇩#?M) = (𝗄 choose 2) * (Λ -1)")
proof (cases "Λ = 1")
case True
have empty: "⋀ b2 . b2 ∈# remove1_mset blv ℬ ⟹ {y .y ⊆ blv ∧ y ⊆ b2 ∧ card y = 2} = {}"
using index_one_alt_bl_not_exist assms True by blast
then show ?thesis using sum_mset.neutral True by (simp add: empty)
next
case False
then have index_min: "Λ ≥ 2" using index_not_zero by linarith
have subset_card: "⋀ x . x ∈# (∑⇩#?M) ⟹ card x = 2"
proof -
fix x
assume a: "x ∈# (∑⇩#?M)"
then obtain b2 where "x ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})"
by blast
thus "card x = 2" using mem_Collect_eq
by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set)
qed
have eq: "set_mset (∑⇩#?M) = {bl . bl ⊆ blv ∧ card bl = 2}"
proof
show "set_mset (∑⇩#?M) ⊆ {bl . bl ⊆ blv ∧ card bl = 2}"
using subset_card intersect_mult_set_block_subset_iff assms by blast
show "{bl . bl ⊆ blv ∧ card bl = 2} ⊆ set_mset (∑⇩#?M)"
using intersect_mult_set_block_subset_iff_2 assms index_min by blast
qed
have "card blv = 𝗄" using uniform assms by simp
then have k: "card (set_mset (∑⇩#?M)) = (𝗄 choose 2)" using eq n_subsets
by (simp add: n_subsets assms finite_blocks)
thus ?thesis using k size_multiset_set_mset_const_count sym_sum_mset_inter2_sets_count assms eq
by (metis (no_types, lifting) intersect_mult_set_block_subset_iff subset_card)
qed
lemma sum_choose_two_inter_num:
assumes "b1 ∈# ℬ"
shows "(∑b2 ∈# (ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1) div 2)) * (𝗏 -1)"
proof -
have div_fact: "2 dvd (Λ * (Λ - 1))"
by fastforce
have div_fact_2: "2 dvd (Λ * (𝗏 - 1))" using symmetric_condition_2 by fastforce
have "(∑b2 ∈# (ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = (∑b2 ∈# (ℬ - {#b1#}). (b1 |∩|⇩2 b2 ))"
using n_inter_num_choose_design_inter assms by (simp add: in_diffD)
then have sum_fact: "(∑b2 ∈# (ℬ - {#b1#}).((b1 |∩| b2) choose 2))
= (𝗄 choose 2) * (Λ -1)"
using assms sym_sum_mset_inter2_sets_size
by (auto simp add: size_big_union_sum n_intersect_num_subset_def)
have "(𝗄 choose 2) * (Λ -1) = ((Λ * (𝗏 - 1) div 2)) * (Λ -1)"
using choose_two symmetric_condition_2 k_non_zero by auto
then have "(𝗄 choose 2) * (Λ -1) = ((Λ * (Λ - 1) div 2)) * (𝗏 -1)"
using div_fact div_fact_2 by (smt div_mult_swap mult.assoc mult.commute)
then show ?thesis using sum_fact by simp
qed
lemma sym_sum_inter_num_sq:
assumes "b1 ∈# ℬ"
shows "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = Λ^2 * ( 𝗏 - 1)"
proof -
have dvd: "2 dvd (( 𝗏 - 1) * (Λ * (Λ - 1)))" by fastforce
have inner_dvd: "∀ bl ∈# (remove1_mset b1 ℬ). 2 dvd ((b1 |∩| bl) * ((b1 |∩| bl) - 1))"
by force
have diff_le: "⋀ bl . bl ∈# (remove1_mset b1 ℬ) ⟹ (b1 |∩| bl) ≤ (b1 |∩| bl)^2"
by (simp add: power2_nat_le_imp_le)
have a: "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) =
(∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2)"
using choose_two by (simp add: intersection_num_non_neg)
have b: "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) =
(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2))" by simp
have gtsq: "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) ≥ (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl))"
by (simp add: diff_le sum_mset_mono)
have "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1)) div 2) * ( 𝗏 - 1)"
using sum_choose_two_inter_num assms by blast
then have start: "(∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2)
= ((Λ * (Λ - 1)) div 2) * (𝗏 - 1)"
using a b by linarith
have sum_dvd: "2 dvd (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1))"
using sum_mset_dvd
by (metis (no_types, lifting) dvd_mult dvd_mult2 dvd_refl odd_two_times_div_two_nat)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2
= ((Λ * (Λ - 1)) div 2) * (𝗏 - 1)"
using start sum_mset_distrib_div_if_dvd inner_dvd
by (metis (mono_tags, lifting) image_mset_cong2)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2
= (𝗏 - 1) * ((Λ * (Λ - 1)) div 2)"
by simp
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1))
= (𝗏 - 1) * (Λ * (Λ - 1))"
by (metis (no_types, lifting) div_mult_swap dvdI dvd_div_eq_iff dvd_mult dvd_mult2 odd_two_times_div_two_nat sum_dvd)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2 - (b1 |∩| bl))
= (𝗏 - 1) * (Λ * (Λ - 1))"
using diff_mult_distrib2
by (metis (no_types, lifting) multiset.map_cong0 nat_mult_1_right power2_eq_square)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2)
- (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)) = (𝗏 - 1) * (Λ * (Λ - 1))"
using sum_mset_add_diff_nat[of "(remove1_mset b1 ℬ)" "λ bl . (b1 |∩| bl)" "λ bl . (b1 |∩| bl)^2"]
diff_le by presburger
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2)
= (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)) + (𝗏 - 1) * (Λ * (Λ - 1))" using gtsq
by (metis le_add_diff_inverse)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) + ((𝗏 - 1) * (Λ * (Λ - 1)))"
using sym_sum_inter_num assms rep_value_sym symmetric_condition_2 by auto
then have prev: "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) * (Λ - 1) + (Λ * (𝗏 - 1))"
by fastforce
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) * (Λ)"
by (metis Nat.le_imp_diff_is_add add_mult_distrib2 index_not_zero nat_mult_1_right)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = Λ * Λ * (𝗏 - 1)"
using mult.commute by simp
thus ?thesis by (simp add: power2_eq_square)
qed
lemma sym_sum_inter_num_to_zero:
assumes "b1 ∈# ℬ"
shows "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - (int Λ))^2) = 0"
proof -
have rm1_size: "size (remove1_mset b1 ℬ) = 𝗏 - 1" using assms b_non_zero int_ops(6)
by (auto simp add: symmetric size_remove1_mset_If)
have "(∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2)) =
(∑bl ∈# (remove1_mset b1 ℬ). (((b1 |∩| bl))^2))" by simp
then have ssi: "(∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2)) = Λ^2 * (𝗏 - 1)"
using sym_sum_inter_num_sq assms by simp
have "⋀ bl . bl ∈# (remove1_mset b1 ℬ) ⟹ (int (b1 |∩| bl) - (int Λ))^2 =
(((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))) + ((int Λ)^2))"
by (simp add: power2_diff)
then have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - (int Λ))^2) =
(∑bl ∈# (remove1_mset b1 ℬ). (((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))) + ((int Λ)^2)))"
using sum_over_fun_eq by auto
also have "... = (∑bl ∈# (remove1_mset b1 ℬ). (((int (b1 |∩| bl))^2)
- (2 * (int Λ) * (int (b1 |∩| bl))))) + (∑ bl ∈# (remove1_mset b1 ℬ) . ((int Λ)^2))"
by (simp add: sum_mset.distrib)
also have "... = (∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2))
- (∑bl ∈# (remove1_mset b1 ℬ). (2 * (int Λ) * (int (b1 |∩| bl)))) + (∑ bl ∈# (remove1_mset b1 ℬ) . ((int Λ)^2))"
using sum_mset_add_diff_int[of "(λ bl . ((int (b1 |∩| bl))^2))" "(λ bl . (2 * (int Λ) * (int (b1 |∩| bl))))" "(remove1_mset b1 ℬ)"]
by simp
also have "... = Λ^2 * (𝗏 - 1) - 2 * (int Λ) *(∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl)))
+ (𝗏 - 1) * ((int Λ)^2)" using ssi rm1_size assms by (simp add: sum_mset_distrib_left)
also have "... = 2 * Λ^2 * (𝗏 - 1) - 2 * (int Λ) *(𝗄* (𝗋 - 1))"
using sym_sum_inter_num assms by simp
also have "... = 2 * Λ^2 * (𝗏 - 1) - 2 * (int Λ) * (Λ * (𝗏 - 1))"
using rep_value_sym symmetric_condition_2 by simp
finally have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - int Λ)^2) = 0"
by (auto simp add: power2_eq_square)
thus ?thesis by simp
qed
theorem sym_block_intersections_index [simp]:
assumes "b1 ∈# ℬ"
assumes "b2 ∈# (ℬ - {#b1#})"
shows "b1 |∩| b2 = Λ"
proof -
define l where l_def: "l = int Λ"
then have pos: "⋀ bl . (int (b1 |∩| bl) - l)^2 ≥ 0" by simp
have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - l)^2) = 0"
using sym_sum_inter_num_to_zero assms l_def by simp
then have "⋀ bl. bl ∈ set_mset (remove1_mset b1 ℬ) ⟹ (int (b1 |∩| bl) - l)^2 = 0"
using sum_mset_0_iff_ge_0 pos by (metis (no_types, lifting))
then have "⋀ bl. bl ∈ set_mset (remove1_mset b1 ℬ) ⟹ int (b1 |∩| bl) = l"
by auto
thus ?thesis using assms(2) l_def of_nat_eq_iff by blast
qed
subsubsection ‹Symmetric BIBD is Simple›
lemma sym_block_mult_one [simp]:
assumes "bl ∈# ℬ"
shows "multiplicity bl = 1"
proof (rule ccontr)
assume "¬ (multiplicity bl = 1)"
then have not: "multiplicity bl ≠ 1" by simp
have "multiplicity bl ≠ 0" using assms
by simp
then have m: "multiplicity bl ≥ 2" using not by linarith
then have blleft: "bl ∈# (ℬ - {#bl#})"
using in_diff_count by fastforce
have "bl |∩| bl = 𝗄" using k_non_zero assms
by (simp add: intersection_number_def)
then have keql: "𝗄 = Λ" using sym_block_intersections_index blleft assms by simp
then have "𝗏 = 𝗄"
using keql index_lt_replication rep_value_sym block_size_lt_v diffs0_imp_equal k_non_zero zero_diff by linarith
then show False using incomplete
by simp
qed
end
sublocale symmetric_bibd ⊆ simple_design
by unfold_locales simp
subsubsection ‹Residual/Derived Sym BIBD Constructions›
text ‹Using the intersect result, we can reason further on residual and derived designs.
Proofs based off lecture notes \<^cite>‹"HerkeLectureNotes2016"››
locale symmetric_bibd_block_transformations = symmetric_bibd + bibd_block_transformations
begin
lemma derived_block_size [simp]:
assumes "b ∈# ℬ⇧D"
shows "card b = Λ"
proof -
obtain bl2 where set: "bl2 ∈# remove1_mset bl ℬ" and inter: "b = bl2 ∩ bl"
using derived_blocks_def assms by (meson derived_obtain_orig_block)
then have "card b = bl2 |∩| bl"
by (simp add: intersection_number_def)
thus ?thesis using sym_block_intersections_index
using set intersect_num_commute valid_block by fastforce
qed
lemma derived_points_index [simp]:
assumes "ps ⊆ bl"
assumes "card ps = 2"
shows "ℬ⇧D index ps = Λ - 1"
proof -
have b_in: "⋀ b . b ∈# (remove1_mset bl ℬ) ⟹ ps ⊆ b ⟹ ps ⊆ b ∩ bl"
using assms by blast
then have orig: "ps ⊆ 𝒱"
using valid_block assms wellformed by blast
then have lam: "size {# b ∈# ℬ . ps ⊆ b #} = Λ" using balanced
by (simp add: assms(2) points_index_def)
then have "size {# b ∈# remove1_mset bl ℬ . ps ⊆ b #} = size {# b ∈# ℬ . ps ⊆ b #} - 1"
using assms valid_block by (simp add: size_Diff_submset)
then have "size {# b ∈# remove1_mset bl ℬ . ps ⊆ b #} = Λ - 1"
using lam index_not_zero by linarith
then have "size {# bl ∩ b | b ∈# (remove1_mset bl ℬ) . ps ⊆ bl ∩ b #} = Λ - 1"
using b_in by (metis (no_types, lifting) Int_subset_iff filter_mset_cong size_image_mset)
then have "size {# x ∈# {# bl ∩ b . b ∈# (remove1_mset bl ℬ) #} . ps ⊆ x #} = Λ - 1"
by (metis image_mset_filter_swap)
then have "size {# x ∈# ℬ⇧D . ps ⊆ x #} = Λ - 1" by (simp add: derived_blocks_def)
thus ?thesis by (simp add: points_index_def)
qed
lemma sym_derive_design_bibd:
assumes "Λ > 1"
shows "bibd bl ℬ⇧D Λ (Λ - 1)"
proof -
interpret des: proper_design bl "ℬ⇧D" using derived_is_proper assms valid_block by auto
have "Λ < 𝗄" using index_lt_replication rep_value_sym by linarith
then show ?thesis using derived_block_size assms derived_points_index derived_points_order
by (unfold_locales) (simp_all)
qed
lemma residual_block_size [simp]:
assumes "b ∈# ℬ⇧R"
shows "card b = 𝗄 - Λ"
proof -
obtain bl2 where sub: "b = bl2 - bl" and mem: "bl2 ∈# remove1_mset bl ℬ"
using assms residual_blocks_def by auto
then have "card b = card bl2 - card (bl2 ∩ bl)"
using card_Diff_subset_Int valid_block finite_blocks
by (simp add: card_Diff_subset_Int)
then have "card b = card bl2 - bl2 |∩| bl"
using finite_blocks card_inter_lt_single by (simp add: intersection_number_def)
thus ?thesis using sym_block_intersections_index uniform
by (metis valid_block in_diffD intersect_num_commute mem)
qed
lemma residual_index [simp]:
assumes "ps ⊆ bl⇧c"
assumes "card ps = 2"
shows "(ℬ⇧R) index ps = Λ"
proof -
have a: "⋀ b . (b ∈# remove1_mset bl ℬ ⟹ ps ⊆ b ⟹ ps ⊆ (b - bl))" using assms
by (smt DiffI block_comp_elem_alt_left in_diffD subset_eq wellformed)
have b: "⋀ b . (b ∈# remove1_mset bl ℬ ⟹ ps ⊆ (b - bl) ⟹ ps ⊆ b)"
by auto
have not_ss: "¬ (ps ⊆ bl)" using set_diff_non_empty_not_subset blocks_nempty t_non_zero assms
block_complement_def by fastforce
have "ℬ⇧R index ps = size {# x ∈# {# b - bl . b ∈# (remove1_mset bl ℬ) #} . ps ⊆ x #}"
using assms valid_block by (simp add: points_index_def residual_blocks_def)
also have "... = size {# b - bl | b ∈# (remove1_mset bl ℬ) . ps ⊆ b - bl #} "
by (metis image_mset_filter_swap)
finally have "ℬ⇧R index ps = size {# b ∈# (remove1_mset bl ℬ) . ps ⊆ b #} " using a b
by (metis (no_types, lifting) filter_mset_cong size_image_mset)
thus ?thesis
using balanced not_ss assms points_index_alt_def block_complement_subset_points by auto
qed
lemma sym_residual_design_bibd:
assumes "𝗄 ≥ Λ + 2"
shows "bibd (bl⇧c) ℬ⇧R (𝗄 - Λ) Λ"
proof -
interpret des: proper_design "bl⇧c" "ℬ⇧R"
using residual_is_proper assms(1) valid_block sym_block_mult_one by fastforce
show ?thesis using residual_block_size assms sym_design_vk_gt_kl residual_order residual_index
by(unfold_locales) simp_all
qed
end
subsection ‹BIBD's and Other Block Designs›
text ‹BIBD's are closely related to other block designs by indirect inheritance›
sublocale bibd ⊆ k_Λ_PBD 𝒱 ℬ Λ 𝗄
using block_size_gt_t by (unfold_locales) simp_all
lemma incomplete_PBD_is_bibd:
assumes "k < card V" and "k_Λ_PBD V B Λ k"
shows "bibd V B k Λ"
proof -
interpret inc: incomplete_design V B k using assms
by (auto simp add: block_design.incomplete_designI k_Λ_PBD.axioms(2))
interpret pairwise_balance: pairwise_balance V B Λ using assms
by (auto simp add: k_Λ_PBD.axioms(1))
show ?thesis using assms k_Λ_PBD.block_size_t by (unfold_locales) (simp_all)
qed
lemma (in bibd) bibd_to_pbdI[intro]:
assumes "Λ = 1"
shows "k_PBD 𝒱 ℬ 𝗄"
proof -
interpret pbd: k_Λ_PBD 𝒱 ℬ Λ 𝗄
by (simp add: k_Λ_PBD_axioms)
show ?thesis using assms by (unfold_locales) (simp_all add: t_lt_order min_block_size_2)
qed
locale incomplete_PBD = incomplete_design + k_Λ_PBD
sublocale incomplete_PBD ⊆ bibd
using block_size_t by (unfold_locales) simp
end