Theory Block_Designs
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