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