Theory Resolvable_Designs
section ‹Resolvable Designs›
text ‹Resolvable designs have further structure, and can be "resolved" into a set of resolution
classes. A resolution class is a subset of blocks which exactly partitions the point set.
Definitions based off the handbook \<^cite>‹"colbournHandbookCombinatorialDesigns2007"›
and Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"›.
This theory includes a proof of an alternate statement of Bose's theorem›
theory Resolvable_Designs imports BIBD
begin
subsection ‹Resolutions and Resolution Classes›
text ‹A resolution class is a partition of the point set using a set of blocks from the design
A resolution is a group of resolution classes partitioning the block collection›
context incidence_system
begin
definition resolution_class :: "'a set set ⇒ bool" where
"resolution_class S ⟷ partition_on 𝒱 S ∧ (∀ bl ∈ S . bl ∈# ℬ)"
lemma resolution_classI [intro]: "partition_on 𝒱 S ⟹ (⋀ bl . bl ∈ S ⟹ bl ∈# ℬ)
⟹ resolution_class S"
by (simp add: resolution_class_def)
lemma resolution_classD1: "resolution_class S ⟹ partition_on 𝒱 S"
by (simp add: resolution_class_def)
lemma resolution_classD2: "resolution_class S ⟹ bl ∈ S ⟹ bl ∈# ℬ"
by (simp add: resolution_class_def)
lemma resolution_class_empty_iff: "resolution_class {} ⟷ 𝒱 = {}"
by (auto simp add: resolution_class_def partition_on_def)
lemma resolution_class_complete: "𝒱 ≠ {} ⟹ 𝒱 ∈# ℬ ⟹ resolution_class {𝒱}"
by (auto simp add: resolution_class_def partition_on_space)
lemma resolution_class_union: "resolution_class S ⟹ ⋃S = 𝒱 "
by (simp add: resolution_class_def partition_on_def)
lemma (in finite_incidence_system) resolution_class_finite: "resolution_class S ⟹ finite S"
using finite_elements finite_sets by (auto simp add: resolution_class_def)
lemma (in design) resolution_class_sum_card: "resolution_class S ⟹ (∑bl ∈ S . card bl) = 𝗏"
using resolution_class_union finite_blocks
by (auto simp add: resolution_class_def partition_on_def card_Union_disjoint)
definition resolution:: "'a set multiset multiset ⇒ bool" where
"resolution P ⟷ partition_on_mset ℬ P ∧ (∀ S ∈# P . distinct_mset S ∧ resolution_class (set_mset S))"
lemma resolutionI : "partition_on_mset ℬ P ⟹ (⋀ S . S ∈#P ⟹ distinct_mset S) ⟹
(⋀ S . S∈# P ⟹ resolution_class (set_mset S)) ⟹ resolution P"
by (simp add: resolution_def)
lemma (in proper_design) resolution_blocks: "distinct_mset ℬ ⟹ disjoint (set_mset ℬ) ⟹
⋃(set_mset ℬ) = 𝒱 ⟹ resolution {#ℬ#}"
unfolding resolution_def resolution_class_def partition_on_mset_def partition_on_def
using design_blocks_nempty blocks_nempty by auto
end
subsection ‹Resolvable Design Locale›
text ‹A resolvable design is one with a resolution P›
locale resolvable_design = design +
fixes partition :: "'a set multiset multiset" ("𝒫")
assumes resolvable: "resolution 𝒫"
begin
lemma resolutionD1: "partition_on_mset ℬ 𝒫"
using resolvable by (simp add: resolution_def)
lemma resolutionD2: "S ∈#𝒫 ⟹ distinct_mset S"
using resolvable by (simp add: resolution_def)
lemma resolutionD3: " S∈# 𝒫 ⟹ resolution_class (set_mset S)"
using resolvable by (simp add: resolution_def)
lemma resolution_class_blocks_disjoint: "S ∈# 𝒫 ⟹ disjoint (set_mset S)"
using resolutionD3 by (simp add: partition_on_def resolution_class_def)
lemma resolution_not_empty: "ℬ ≠ {#} ⟹ 𝒫 ≠ {#}"
using partition_on_mset_not_empty resolutionD1 by auto
lemma resolution_blocks_subset: "S ∈# 𝒫 ⟹ S ⊆# ℬ"
using partition_on_mset_subsets resolutionD1 by auto
end
lemma (in incidence_system) resolvable_designI [intro]: "resolution 𝒫 ⟹ design 𝒱 ℬ ⟹
resolvable_design 𝒱 ℬ 𝒫"
by (simp add: resolvable_design.intro resolvable_design_axioms.intro)
subsection ‹Resolvable Block Designs›
text ‹An RBIBD is a resolvable BIBD - a common subclass of interest for block designs›
locale r_block_design = resolvable_design + block_design
begin
lemma resolution_class_blocks_constant_size: "S ∈# 𝒫 ⟹ bl ∈# S ⟹ card bl = 𝗄"
by (metis resolutionD3 resolution_classD2 uniform_alt_def_all)
lemma resolution_class_size1:
assumes "S ∈# 𝒫"
shows "𝗏 = 𝗄 * size S"
proof -
have "(∑bl ∈# S . card bl) = (∑bl ∈ (set_mset S) . card bl)" using resolutionD2 assms
by (simp add: sum_unfold_sum_mset)
then have eqv: "(∑bl ∈# S . card bl) = 𝗏" using resolutionD3 assms resolution_class_sum_card
by presburger
have "(∑bl ∈# S . card bl) = (∑bl ∈# S . 𝗄)" using resolution_class_blocks_constant_size assms
by auto
thus ?thesis using eqv by auto
qed
lemma resolution_class_size2:
assumes "S ∈# 𝒫"
shows "size S = 𝗏 div 𝗄"
using resolution_class_size1 assms
by (metis nonzero_mult_div_cancel_left not_one_le_zero k_non_zero)
lemma resolvable_necessary_cond_v: "𝗄 dvd 𝗏"
proof -
obtain S where s_in: "S ∈#𝒫" using resolution_not_empty design_blocks_nempty by blast
then have "𝗄 * size S = 𝗏" using resolution_class_size1 by simp
thus ?thesis by (metis dvd_triv_left)
qed
end
locale rbibd = r_block_design + bibd
begin
lemma resolvable_design_num_res_classes: "size 𝒫 = 𝗋"
proof -
have k_ne0: "𝗄 ≠ 0" using k_non_zero by auto
have f1: "𝖻 = (∑S ∈# 𝒫 . size S)"
by (metis partition_on_msetD1 resolutionD1 size_big_union_sum)
then have "𝖻 = (∑S ∈# 𝒫 . 𝗏 div 𝗄)" using resolution_class_size2 f1 by auto
then have f2: "𝖻 = (size 𝒫) * (𝗏 div 𝗄)" by simp
then have "size 𝒫 = 𝖻 div (𝗏 div 𝗄)"
using b_non_zero by auto
then have "size 𝒫 = (𝖻 * 𝗄) div 𝗏" using f2 resolvable_necessary_cond_v
by (metis div_div_div_same div_dvd_div dvd_triv_right k_ne0 nonzero_mult_div_cancel_right)
thus ?thesis using necessary_condition_two
by (metis nonzero_mult_div_cancel_left not_one_less_zero t_design_min_v)
qed
lemma resolvable_necessary_cond_b: "𝗋 dvd 𝖻"
proof -
have f1: "𝖻 = (∑S ∈# 𝒫 . size S)"
by (metis partition_on_msetD1 resolutionD1 size_big_union_sum)
then have "𝖻 = (∑S ∈# 𝒫 . 𝗏 div 𝗄)" using resolution_class_size2 f1 by auto
thus ?thesis using resolvable_design_num_res_classes by simp
qed
subsubsection ‹Bose's Inequality›
text ‹Boses inequality is an important theorem on RBIBD's. This is a proof
of an alternate statement of the thm, which does not require a linear algebraic approach,
taken directly from Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››
theorem bose_inequality_alternate: "𝖻 ≥ 𝗏 + 𝗋 - 1 ⟷ 𝗋 ≥ 𝗄 + Λ"
proof -
from necessary_condition_two v_non_zero have r: ‹𝗋 = 𝖻 * 𝗄 div 𝗏›
by (metis div_mult_self1_is_m)
define k b v l r where intdefs: "k ≡ (int 𝗄)" "b ≡ int 𝖻" "v = int 𝗏" "l ≡ int Λ" "r ≡ int 𝗋"
have kdvd: "k dvd (v * (r - k))"
using intdefs
by (simp add: resolvable_necessary_cond_v)
have necess1_alt: "l * v - l = r * (k - 1)" using necessary_condition_one intdefs
by (smt (verit) diff_diff_cancel int_ops(2) int_ops(6) k_non_zero nat_mult_1_right of_nat_0_less_iff
of_nat_mult right_diff_distrib' v_non_zero)
then have v_eq: "v = (r * (k - 1) + l) div l"
using necessary_condition_one index_not_zero intdefs
by (metis diff_add_cancel nonzero_mult_div_cancel_left not_one_le_zero of_nat_mult
linordered_euclidean_semiring_class.of_nat_div)
have ldvd: " ⋀ x. l dvd (x * (r * (k - 1) + l))"
by (metis necess1_alt diff_add_cancel dvd_mult dvd_triv_left)
have "(b ≥ v + r - 1) ⟷ ((𝗏 * r) div k ≥ v + r - 1)"
using necessary_condition_two k_non_zero intdefs
by (metis (no_types, lifting) nonzero_mult_div_cancel_right not_one_le_zero of_nat_eq_0_iff of_nat_mult)
also have "... ⟷ (((v * r) - (v * k)) div k ≥ r - 1)"
using k_non_zero k_non_zero r intdefs
by (simp add: of_nat_div algebra_simps)
(smt (verit, ccfv_threshold) One_nat_def div_mult_self4 of_nat_1 of_nat_mono)
also have f2: " ... ⟷ ((v * ( r - k)) div k ≥ ( r - 1))"
using int_distrib(3) by (simp add: mult.commute)
also have f2: " ... ⟷ ((v * ( r - k)) ≥ k * ( r - 1))"
using k_non_zero kdvd intdefs by auto
also have "... ⟷ ((((r * (k - 1) + l ) div l) * (r - k)) ≥ k * (r - 1))"
using v_eq by presburger
also have "... ⟷ ( (r - k) * ((r * (k - 1) + l ) div l) ≥ (k * (r - 1)))"
by (simp add: mult.commute)
also have " ... ⟷ ( ((r - k) * (r * (k - 1) + l )) div l ≥ (k * (r - 1)))"
using div_mult_swap necessary_condition_one intdefs
by (metis diff_add_cancel dvd_triv_left necess1_alt)
also have " ... ⟷ (((r - k) * (r * (k - 1) + l )) ≥ l * (k * (r - 1)))"
using ldvd[of "(r - k)"] dvd_mult_div_cancel index_not_zero mult_strict_left_mono intdefs
by (smt (verit) b_non_zero bibd_block_number bot_nat_0.extremum_strict div_0 less_eq_nat.simps(1)
mult_eq_0_iff mult_left_le_imp_le mult_left_mono of_nat_0 of_nat_le_0_iff of_nat_le_iff of_nat_less_iff)
also have 1: "... ⟷ (((r - k) * (r * (k - 1))) + ((r - k) * l ) ≥ l * (k * (r - 1)))"
by (simp add: distrib_left)
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ l * k * (r - 1) - ((r - k) * l ))"
using mult.assoc by linarith
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ (l * k * r) - (l * k) - ((r * l) -(k * l )))"
using distrib_right by (simp add: distrib_left right_diff_distrib' left_diff_distrib')
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ (l * k * r) - ( l * r))"
by (simp add: mult.commute)
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ (l * (k * r)) - ( l * r))"
by linarith
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ (l * (r * k)) - ( l * r))"
by (simp add: mult.commute)
also have "... ⟷ (((r - k) * r * (k - 1)) ≥ l * r * (k - 1))"
by (simp add: mult.assoc int_distrib(4))
finally have "(b ≥ v + r - 1) ⟷ (r ≥ k + l)"
using index_lt_replication mult_right_le_imp_le r_gzero mult_cancel_right k_non_zero intdefs
by (smt (z3) of_nat_0_less_iff of_nat_1 of_nat_le_iff of_nat_less_iff)
then have "𝖻 ≥ 𝗏 + 𝗋 - 1 ⟷ 𝗋 ≥ 𝗄 + Λ"
using k_non_zero le_add_diff_inverse of_nat_1 of_nat_le_iff intdefs by linarith
thus ?thesis by simp
qed
end
end