(* 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