# Theory Design_Theory.Resolvable_Designs

```(* Title: Resolvable_Designs.thy
Author: Chelsea Edmonds
*)

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"

lemma resolution_classD1: "resolution_class S ⟹ partition_on 𝒱 S"

lemma resolution_classD2: "resolution_class S ⟹  bl ∈ S ⟹ bl ∈# ℬ"

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 = 𝒱 "

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"

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 𝒱 ℬ 𝒫"

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
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
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
unique_euclidean_semiring_with_nat_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
(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)))"
also have " ... ⟷ ( ((r - k) * (r * (k - 1) + l )) div l ≥ (k * (r - 1)))"
using div_mult_swap necessary_condition_one intdefs
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)))"
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))"
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))"