Theory Design_Theory.Block_Designs

(* Title: Block_Designs.thy
   Author: Chelsea Edmonds
*)

section ‹Block and Balanced Designs›
text ‹We define a selection of the many different types of block and balanced designs, building up 
to properties required for defining a BIBD, in addition to several base generalisations› 

theory Block_Designs imports Design_Operations
begin

subsection ‹Block Designs›
text ‹A block design is a design where all blocks have the same size.›

subsubsection ‹K Block Designs› 
text ‹An important generalisation of a typical block design is the $\mathcal{K}$ block design, 
where all blocks must have a size $x$ where $x \in \mathcal{K}$›
locale K_block_design = proper_design +
  fixes sizes :: "nat set" ("𝒦")
  assumes block_sizes: "bl ∈#   card bl  𝒦"
  assumes positive_ints: "x  𝒦  x > 0"
begin

lemma sys_block_size_subset: "sys_block_sizes  𝒦"
  using block_sizes sys_block_sizes_obtain_bl by blast

end

subsubsection‹Uniform Block Design›
text ‹The typical uniform block design is defined below›
locale block_design = proper_design + 
  fixes u_block_size :: nat ("𝗄")
  assumes uniform [simp]: "bl ∈#   card bl = 𝗄"
begin

lemma k_non_zero: "𝗄  1"
proof -
  obtain bl where bl_in: "bl ∈# "
    using design_blocks_nempty by auto 
  then have "card bl  1" using block_size_gt_0
    by (metis less_not_refl less_one not_le_imp_less) 
  thus ?thesis by (simp add: bl_in)
qed

lemma uniform_alt_def_all: " bl ∈#  .card bl = 𝗄"
  using uniform by auto 

lemma uniform_unfold_point_set: "bl ∈#   card {p  𝒱. p  bl} = 𝗄"
  using uniform wellformed by (simp add: Collect_conj_eq inf.absorb_iff2) 

lemma uniform_unfold_point_set_mset: "bl ∈#   size {#p ∈# mset_set 𝒱. p  bl #} = 𝗄"
  using uniform_unfold_point_set by (simp add: finite_sets) 

lemma sys_block_sizes_uniform [simp]:  "sys_block_sizes  = {𝗄}"
proof -
  have "sys_block_sizes = {bs .  bl . bs = card bl  bl∈# }" by (simp add: sys_block_sizes_def)
  then have "sys_block_sizes  = {bs . bs = 𝗄}" using uniform uniform_unfold_point_set 
      b_positive block_set_nempty_imp_block_ex
    by (smt (verit, best) Collect_cong design_blocks_nempty)
  thus ?thesis by auto
qed

lemma sys_block_sizes_uniform_single: "is_singleton (sys_block_sizes)"
  by simp

lemma uniform_size_incomp: "𝗄  𝗏 - 1  bl ∈#   incomplete_block bl"
  using uniform k_non_zero 
  by (metis block_size_lt_v diff_diff_cancel diff_is_0_eq' less_numeral_extra(1) nat_less_le)

lemma uniform_complement_block_size:
  assumes "bl ∈# C"
  shows "card bl = 𝗏 - 𝗄"
proof -
  obtain bl' where bl_assm: "bl = bl'c  bl' ∈# " 
    using wellformed assms by (auto simp add: complement_blocks_def)
  then have "int (card bl') = 𝗄" by simp
  thus ?thesis using bl_assm block_complement_size wellformed
    by (simp add: block_size_lt_order of_nat_diff) 
qed

lemma uniform_complement[intro]: 
  assumes "𝗄  𝗏 - 1"
  shows "block_design 𝒱 C (𝗏 - 𝗄)"
proof - 
  interpret des: proper_design 𝒱 "C" 
    using  uniform_size_incomp assms complement_proper_design by auto 
  show ?thesis using assms uniform_complement_block_size by (unfold_locales) (simp)
qed

lemma block_size_lt_v: "𝗄  𝗏"
  using v_non_zero block_size_lt_v design_blocks_nempty uniform by auto 

end

lemma (in proper_design) block_designI[intro]: "( bl . bl ∈#   card bl = k) 
   block_design 𝒱  k"
  by (unfold_locales) (auto)

context block_design 
begin

lemma block_design_multiple: "n > 0  block_design 𝒱 (multiple_blocks n) 𝗄"
  using elem_in_repeat_in_original multiple_proper_design proper_design.block_designI 
  by (metis uniform_alt_def_all)

end
text ‹A uniform block design is clearly a type of $K$\_block\_design with a singleton $K$ set›
sublocale block_design  K_block_design 𝒱  "{𝗄}"
  using k_non_zero uniform by unfold_locales simp_all

subsubsection ‹Incomplete Designs›
text ‹An incomplete design is a design where $k < v$, i.e. no block is equal to the point set›
locale incomplete_design = block_design + 
  assumes incomplete: "𝗄 < 𝗏"

begin

lemma incomplete_imp_incomp_block: "bl ∈#   incomplete_block bl"
  using incomplete uniform uniform_size_incomp by fastforce  

lemma incomplete_imp_proper_subset: "bl ∈#   bl  𝒱"
  using incomplete_block_proper_subset incomplete_imp_incomp_block by auto
end

lemma (in block_design) incomplete_designI[intro]: "𝗄 < 𝗏  incomplete_design 𝒱  𝗄"
  by unfold_locales auto

context incomplete_design
begin

lemma multiple_incomplete: "n > 0  incomplete_design 𝒱 (multiple_blocks n) 𝗄"
  using block_design_multiple incomplete by (simp add: block_design.incomplete_designI) 

lemma complement_incomplete: "incomplete_design 𝒱 (C) (𝗏 - 𝗄)"
proof -
  have "𝗏 - 𝗄 < 𝗏" using v_non_zero k_non_zero by linarith
  thus ?thesis using uniform_complement incomplete incomplete_designI
    by (simp add: block_design.incomplete_designI) 
qed

end

subsection ‹Balanced Designs›
text ‹t-wise balance is a design with the property that all point subsets of size $t$ occur in 
$\lambda_t$ blocks›

locale t_wise_balance = proper_design + 
  fixes grouping :: nat ("𝗍") and index :: nat ("Λt")
  assumes t_non_zero: "𝗍  1"
  assumes t_lt_order: "𝗍  𝗏"
  assumes balanced [simp]: "ps  𝒱  card ps = 𝗍   index ps = Λt"
begin

lemma t_non_zero_suc: "𝗍  Suc 0"
  using t_non_zero by auto

lemma balanced_alt_def_all: " ps  𝒱 . card ps = 𝗍   index ps = Λt"
  using balanced by auto

end

lemma (in proper_design) t_wise_balanceI[intro]: "𝗍  𝗏  𝗍  1  
  ( ps . ps  𝒱  card ps = 𝗍    index ps = Λt)  t_wise_balance 𝒱  𝗍 Λt"
  by (unfold_locales) auto

context t_wise_balance
begin

lemma obtain_t_subset_points:
  obtains T where "T  𝒱" "card T = 𝗍" "finite T"
  using obtain_subset_with_card_n design_points_nempty t_lt_order t_non_zero finite_sets by auto

lemma multiple_t_wise_balance_index [simp]:
  assumes "ps  𝒱"
  assumes "card ps = 𝗍"
  shows "(multiple_blocks n) index ps = Λt * n"
  using multiple_point_index balanced assms by fastforce 

lemma multiple_t_wise_balance: 
  assumes "n > 0" 
  shows "t_wise_balance 𝒱 (multiple_blocks n) 𝗍 (Λt * n)"
proof - 
  interpret des: proper_design 𝒱 "(multiple_blocks n)" by (simp add: assms multiple_proper_design)  
  show ?thesis using t_non_zero t_lt_order multiple_t_wise_balance_index 
    by (unfold_locales) (simp_all)
qed

lemma twise_set_pair_index: "ps  𝒱  ps2  𝒱  ps  ps2  card ps = 𝗍  card ps2 = 𝗍 
    index ps =  index ps2"
  using balanced by simp 

lemma t_wise_balance_alt: "ps  𝒱  card ps = 𝗍   index ps = l2 
   ( ps . ps  𝒱  card ps = 𝗍   index ps = l2)"
  using twise_set_pair_index by blast

lemma index_1_imp_mult_1 [simp]: 
  assumes "Λt = 1"
  assumes "bl ∈# "
  assumes "card 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
  obtain ps where ps: "ps  bl  card ps = 𝗍"
    using assms obtain_t_subset_points
    by (metis obtain_subset_with_card_n) 
  then have " index ps  2"
    using m points_index_count_min ps by blast
  then show False using balanced ps antisym_conv2 not_numeral_less_zero numeral_le_one_iff 
      points_index_ps_nin semiring_norm(69) zero_neq_numeral
    by (metis assms(1))
qed

end

subsubsection ‹Sub-types of t-wise balance›

text ‹Pairwise balance is when $t = 2$. These are commonly of interest›
locale pairwise_balance = t_wise_balance 𝒱  2 Λ 
  for point_set ("𝒱") and block_collection ("") and index ("Λ")

text ‹We can combine the balance properties with $K$\_block design to define tBD's 
(t-wise balanced designs), and PBD's (pairwise balanced designs)›

locale tBD = t_wise_balance + K_block_design +
  assumes block_size_gt_t: "k  𝒦  k  𝗍"

locale Λ_PBD = pairwise_balance + K_block_design + 
  assumes block_size_gt_t: "k  𝒦  k  2"

sublocale Λ_PBD  tBD 𝒱  2 Λ 𝒦
  using t_lt_order block_size_gt_t by (unfold_locales) (simp_all)

locale PBD = Λ_PBD 𝒱  1 𝒦 for point_set ("𝒱") and block_collection ("") and sizes ("𝒦")
begin
lemma multiplicity_is_1:
  assumes "bl ∈# "
  shows "multiplicity bl = 1"
  using block_size_gt_t index_1_imp_mult_1 by (simp add: assms block_sizes) 

end

sublocale PBD  simple_design
  using multiplicity_is_1 by (unfold_locales)

text ‹PBD's are often only used in the case where $k$ is uniform, defined here.›
locale k_Λ_PBD = pairwise_balance + block_design + 
  assumes block_size_t: "2  𝗄"

sublocale k_Λ_PBD  Λ_PBD 𝒱  Λ "{𝗄}"
  using k_non_zero uniform block_size_t by(unfold_locales) (simp_all)

locale k_PBD = k_Λ_PBD 𝒱  1 𝗄 for point_set ("𝒱") and block_collection ("") and u_block_size ("𝗄")

sublocale k_PBD  PBD 𝒱  "{𝗄}"
  using  block_size_t by (unfold_locales, simp_all)

subsubsection ‹Covering and Packing Designs›
text ‹Covering and packing designs involve a looser balance restriction. Upper/lower bounds
are placed on the points index, instead of a strict equality›

text ‹A t-covering design is a relaxed version of a tBD, where, for all point subsets of size t, 
a lower bound is put on the points index›
locale t_covering_design = block_design +
  fixes grouping :: nat ("𝗍")
  fixes min_index :: nat ("Λt")
  assumes covering: "ps  𝒱  card ps = 𝗍   index ps  Λt" 
  assumes block_size_t: "𝗍  𝗄"
  assumes t_non_zero: "𝗍  1"
begin

lemma covering_alt_def_all: " ps  𝒱 . card ps = 𝗍   index ps  Λt"
  using covering by auto

end

lemma (in block_design) t_covering_designI [intro]: "t  𝗄  t  1  
  ( ps. ps  𝒱  card ps = t   index ps  Λt)  t_covering_design 𝒱  𝗄 t Λt"
  by (unfold_locales) simp_all

text ‹A t-packing design is a relaxed version of a tBD, where, for all point subsets of size t, 
an upper bound is put on the points index›
locale t_packing_design = block_design + 
  fixes grouping :: nat ("𝗍")
  fixes min_index :: nat ("Λt")
  assumes packing: "ps  𝒱  card ps = 𝗍   index ps  Λt"
  assumes block_size_t: "𝗍  𝗄"
  assumes t_non_zero: "𝗍  1"
begin

lemma packing_alt_def_all: " ps  𝒱 . card ps = 𝗍   index ps  Λt"
  using packing by auto

end

lemma (in block_design) t_packing_designI [intro]: "t  𝗄  t  1  
  ( ps . ps  𝒱  card ps = t   index ps  Λt)  t_packing_design 𝒱  𝗄 t Λt"
  by (unfold_locales) simp_all

lemma packing_covering_imp_balance: 
  assumes "t_packing_design V B k t Λt" 
  assumes "t_covering_design V B k t Λt" 
  shows "t_wise_balance V B t Λt"
proof -
  from assms interpret des: proper_design V B 
    using block_design.axioms(1) t_covering_design.axioms(1) by blast
  show ?thesis 
  proof (unfold_locales)
    show "1  t" using assms t_packing_design.t_non_zero by auto
    show "t  des.𝗏" using block_design.block_size_lt_v t_packing_design.axioms(1) 
      by (metis assms(1) dual_order.trans t_packing_design.block_size_t)
    show "ps. ps  V  card ps = t  B index ps = Λt" 
      using t_packing_design.packing t_covering_design.covering by (metis assms dual_order.antisym) 
  qed
qed

subsection ‹Constant Replication Design›
text ‹When the replication number for all points in a design is constant, it is the 
design replication number.›
locale constant_rep_design = proper_design +
  fixes design_rep_number :: nat ("𝗋")
  assumes rep_number [simp]: "x  𝒱    rep x = 𝗋" 

begin

lemma rep_number_alt_def_all: " x  𝒱.  rep x = 𝗋"
  by (simp)

lemma rep_number_unfold_set: "x  𝒱  size {#bl ∈#  . x  bl#} = 𝗋"
  using rep_number by (simp add: point_replication_number_def)

lemma rep_numbers_constant [simp]: "replication_numbers  = {𝗋}"
  unfolding replication_numbers_def using rep_number design_points_nempty Collect_cong finite.cases 
    finite_sets insertCI singleton_conv
  by (smt (verit, ccfv_threshold) fst_conv snd_conv) 

lemma replication_number_single: "is_singleton (replication_numbers)"
  using is_singleton_the_elem by simp

lemma constant_rep_point_pair: "x1  𝒱  x2  𝒱  x1  x2   rep x1 =  rep x2"
  using rep_number by auto

lemma constant_rep_alt: "x1  𝒱   rep x1 = r2  ( x . x  𝒱   rep x = r2)"
  by (simp)

lemma constant_rep_point_not_0:
  assumes "x  𝒱" 
  shows " rep x  0"
proof (rule ccontr)
  assume "¬  rep x  0"
  then have " x . x  𝒱   rep x = 0" using rep_number assms by auto
  then have " x . x  𝒱   size {#bl ∈#  . x  bl#} = 0" 
    by (simp add: point_replication_number_def)
  then show False using design_blocks_nempty wf_design wf_design_iff wf_invalid_point
    by (metis ex_in_conv filter_mset_empty_conv multiset_nonemptyE size_eq_0_iff_empty)
qed

lemma rep_not_zero: "𝗋  0"
  using rep_number constant_rep_point_not_0 design_points_nempty by auto 

lemma r_gzero: "𝗋 > 0"
  using rep_not_zero by auto 

lemma r_lt_eq_b: "𝗋  𝖻"
  using rep_number max_point_rep
  by (metis all_not_in_conv design_points_nempty) 

lemma complement_rep_number: 
  assumes " bl . bl ∈#   incomplete_block bl"
  shows "constant_rep_design 𝒱 C (𝖻 - 𝗋)"
proof - 
  interpret d: proper_design 𝒱 "(C)" using complement_proper_design
    by (simp add: assms) 
  show ?thesis using complement_rep_number rep_number by (unfold_locales) simp
qed

lemma multiple_rep_number: 
  assumes "n > 0"
  shows "constant_rep_design 𝒱 (multiple_blocks n) (𝗋 * n)"
proof - 
  interpret d: proper_design 𝒱 "(multiple_blocks n)" using multiple_proper_design
    by (simp add: assms) 
  show ?thesis using multiple_point_rep_num by (unfold_locales) (simp_all)
qed
end

lemma (in proper_design) constant_rep_designI [intro]: "( x . x  𝒱   rep x = 𝗋) 
     constant_rep_design 𝒱  𝗋"
  by unfold_locales auto

subsection ‹T-designs›
text ‹All the before mentioned designs build up to the concept of a t-design, which has uniform 
block size and is t-wise balanced. We limit $t$ to be less than $k$, so the balance condition has 
relevance›
locale t_design = incomplete_design + t_wise_balance + 
  assumes block_size_t: "𝗍  𝗄"
begin

lemma point_indices_balanced: "point_indices 𝗍 = {Λt}" 
proof -
  have "point_indices 𝗍 = {i .  ps . i =  index ps  card ps = 𝗍  ps  𝒱}"
    by (simp add: point_indices_def) 
  then have "point_indices  𝗍 = {i . i = Λt}" using balanced Collect_cong obtain_t_subset_points 
     by (smt (verit, best)) 
  thus ?thesis by auto
qed

lemma point_indices_singleton: "is_singleton (point_indices 𝗍)"
  using point_indices_balanced is_singleton_the_elem by simp

end

lemma t_designI [intro]: 
  assumes "incomplete_design V B k"
  assumes "t_wise_balance V B t Λt"
  assumes "t  k"
  shows "t_design V B k t Λt"
  by (simp add: assms(1) assms(2) assms(3) t_design.intro t_design_axioms.intro)

sublocale t_design  t_covering_design 𝒱  𝗄 𝗍 Λt
  using t_non_zero by (unfold_locales) (auto simp add: block_size_t)

sublocale t_design  t_packing_design 𝒱  𝗄 𝗍 Λt
  using t_non_zero by (unfold_locales) (auto simp add: block_size_t)

lemma t_design_pack_cov [intro]: 
  assumes "k < card V"
  assumes "t_covering_design V B k t Λt"
  assumes "t_packing_design V B k t Λt"
  shows "t_design V B k t Λt"
proof -
  from assms interpret id: incomplete_design V B k
    using block_design.incomplete_designI t_packing_design.axioms(1)
    by blast 
  from assms interpret balance: t_wise_balance V B t Λt 
    using packing_covering_imp_balance by blast 
  show ?thesis using assms(3) 
    by (unfold_locales) (simp_all add: t_packing_design.block_size_t)
qed

sublocale t_design  tBD 𝒱  𝗍 Λt "{𝗄}"
  using uniform k_non_zero block_size_t by (unfold_locales) simp_all

context t_design 
begin

lemma multiple_t_design: "n > 0  t_design 𝒱 (multiple_blocks n) 𝗄 𝗍 (Λt * n)"
  using multiple_t_wise_balance multiple_incomplete block_size_t by (simp add: t_designI)

lemma t_design_min_v: "𝗏 > 1"
  using k_non_zero incomplete by simp

end

subsection ‹Steiner Systems›

text ‹Steiner systems are a special type of t-design where $\Lambda_t = 1$›
locale steiner_system = t_design 𝒱  𝗄 𝗍 1 
  for point_set ("𝒱") and block_collection ("") and u_block_size ("𝗄") and grouping ("𝗍")

begin

lemma block_multiplicity [simp]: 
  assumes "bl ∈# "
  shows "multiplicity bl = 1"
  by (simp add: assms block_size_t)

end

sublocale steiner_system  simple_design
  by unfold_locales (simp)

lemma (in t_design) steiner_systemI[intro]: "Λt = 1  steiner_system 𝒱  𝗄 𝗍"
  using t_non_zero t_lt_order block_size_t
  by unfold_locales auto

subsection ‹Combining block designs›
text ‹We define some closure properties for various block designs under the combine operator.
This is done using locales to reason on multiple instances of the same type of design, building 
on what was presented in the design operations theory›

locale two_t_wise_eq_points = two_designs_proper 𝒱  𝒱 ℬ' + des1: t_wise_balance 𝒱  𝗍 Λt + 
  des2: t_wise_balance 𝒱 ℬ' 𝗍 Λt' for 𝒱  𝗍 Λt ℬ' Λt'
begin

lemma combine_t_wise_balance_index: "ps  𝒱  card ps = 𝗍  + index ps = (Λt + Λt')"
  using des1.balanced des2.balanced by (simp add: combine_points_index)

lemma combine_t_wise_balance: "t_wise_balance 𝒱+ + 𝗍 (Λt + Λt')"
proof (unfold_locales, simp add: des1.t_non_zero_suc)
  have "card 𝒱+   card 𝒱" by simp 
  then show "𝗍  card (𝒱+)" using des1.t_lt_order by linarith 
  show "ps. ps  𝒱+  card ps = 𝗍  (+ index ps) = Λt + Λt'" 
    using combine_t_wise_balance_index by blast 
qed

sublocale combine_t_wise_des: t_wise_balance "𝒱+" "+" "𝗍" "(Λt + Λt')"
  using combine_t_wise_balance by auto

end

locale two_k_block_designs = two_designs_proper 𝒱  𝒱' ℬ' + des1: block_design 𝒱  𝗄 + 
  des2: block_design 𝒱' ℬ' 𝗄 for 𝒱  𝗄 𝒱' ℬ'
begin

lemma block_design_combine: "block_design 𝒱+ + 𝗄"
  using des1.uniform des2.uniform by (unfold_locales) (auto)

sublocale combine_block_des: block_design "𝒱+" "+" "𝗄"
  using block_design_combine by simp

end

locale two_rep_designs_eq_points = two_designs_proper 𝒱  𝒱 ℬ' + des1: constant_rep_design 𝒱  𝗋 + 
  des2: constant_rep_design 𝒱 ℬ' 𝗋' for 𝒱  𝗋 ℬ' 𝗋' 
begin

lemma combine_rep_number: "constant_rep_design 𝒱+ + (𝗋 + 𝗋')"
  using combine_rep_number des1.rep_number des2.rep_number by (unfold_locales) (simp)

sublocale combine_const_rep: constant_rep_design "𝒱+" "+" "(𝗋 + 𝗋')"
  using combine_rep_number by simp

end

locale two_incomplete_designs = two_k_block_designs 𝒱  𝗄 𝒱' ℬ' + des1: incomplete_design 𝒱  𝗄 + 
  des2: incomplete_design 𝒱' ℬ' 𝗄 for 𝒱  𝗄 𝒱' ℬ'
begin

lemma combine_is_incomplete: "incomplete_design 𝒱+ + 𝗄"
  using combine_order des1.incomplete des2.incomplete by (unfold_locales) (simp)

sublocale combine_incomplete: incomplete_design "𝒱+" "+" "𝗄"
  using combine_is_incomplete by simp
end

locale two_t_designs_eq_points = two_incomplete_designs 𝒱  𝗄 𝒱 ℬ' 
  + two_t_wise_eq_points 𝒱  𝗍 Λt ℬ' Λt' + des1: t_design 𝒱  𝗄 𝗍 Λt + 
  des2: t_design 𝒱 ℬ' 𝗄 𝗍 Λt' for 𝒱  𝗄 ℬ' 𝗍 Λt Λt'
begin

lemma combine_is_t_des: "t_design 𝒱+ + 𝗄 𝗍 (Λt + Λt')"
  using des1.block_size_t des2.block_size_t by (unfold_locales)

sublocale combine_t_des: t_design "𝒱+" "+" "𝗄" "𝗍" "(Λt + Λt')"
  using combine_is_t_des by blast

end
end