(* Title: BIBD Author: Chelsea Edmonds *) theory BIBD imports Block_Designs begin section ‹BIBD's› text ‹BIBD's are perhaps the most commonly studied type of design in combinatorial design theory, and usually the first type of design explored in a design theory course. These designs are a type of t-design, where $t = 2$› subsection ‹BIBD Basics› locale bibd = t_design 𝒱 ℬ 𝗄 2 Λ for point_set ("𝒱") and block_collection ("ℬ") and u_block_size ("𝗄") and index ("Λ") begin lemma min_block_size_2: "𝗄 ≥ 2" using block_size_t by simp lemma points_index_pair: "y ∈ 𝒱 ⟹ x ∈ 𝒱 ⟹ x ≠ y ⟹ size ({# bl ∈# ℬ . {x, y} ⊆ bl#}) = Λ" using balanced card_2_iff empty_subsetI insert_subset points_index_def by metis lemma index_one_empty_rm_blv [simp]: assumes "Λ = 1" and " blv ∈# ℬ" and "p ⊆ blv" and "card p = 2" shows "{#bl ∈# remove1_mset blv ℬ . p ⊆ bl#} = {#}" proof - have blv_in: "blv ∈# filter_mset ((⊆) p) ℬ" using assms by simp have "p ⊆ 𝒱" using assms wellformed by auto then have "size (filter_mset ((⊆) p) ℬ) = 1" using balanced assms by (simp add: points_index_def) then show ?thesis using blv_in filter_diff_mset filter_single_mset by (metis (no_types, lifting) add_mset_eq_single assms(3) insert_DiffM size_1_singleton_mset) qed lemma index_one_alt_bl_not_exist: assumes "Λ = 1" and " blv ∈# ℬ" and "p ⊆ blv" and "card p = 2" shows" ⋀ bl. bl ∈# remove1_mset blv ℬ ⟹ ¬ (p ⊆ bl) " using index_one_empty_rm_blv by (metis assms(1) assms(2) assms(3) assms(4) filter_mset_empty_conv) subsection ‹Necessary Conditions for Existence› text ‹The necessary conditions on the existence of a $(v, k, \lambda)$-bibd are one of the fundamental first theorems on designs. Proofs based off MATH3301 lecture notes \<^cite>‹"HerkeLectureNotes2016"› and Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"›› lemma necess_cond_1_rhs: assumes "x ∈ 𝒱" shows "size ({# p ∈# (mset_set (𝒱 - {x}) ×# {# bl ∈# ℬ . x ∈ bl #}). fst p ∈ snd p#}) = Λ * (𝗏- 1)" proof - let ?M = "mset_set (𝒱 - {x})" let ?B = "{# bl ∈# ℬ . x ∈ bl #}" have m_distinct: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp have y_point: "⋀ y . y ∈# ?M ⟹ y ∈ 𝒱" using assms by (simp add: finite_sets) have b_contents: "⋀ bl. bl ∈# ?B ⟹ x ∈ bl" using assms by auto have "⋀ y. y ∈# ?M ⟹ y ≠ x" using assms by (simp add: finite_sets) then have "⋀ y .y ∈# ?M ⟹ size ({# bl ∈# ?B . {x, y} ⊆ bl#}) = Λ" using points_index_pair filter_filter_mset_ss_member y_point assms finite_sets by metis then have "⋀ y .y ∈# ?M ⟹ size ({# bl ∈# ?B . x ∈ bl ∧ y ∈ bl#}) = Λ" by auto then have bl_set_size: "⋀ y . y ∈# ?M ⟹ size ({# bl ∈# ?B . y ∈ bl#}) = Λ" using b_contents by (metis (no_types, lifting) filter_mset_cong) then have final_size: "size (∑p∈#?M . ({#p#} ×# {#bl ∈# ?B. p ∈ bl#})) = size (?M) * Λ" using m_distinct size_Union_distinct_cart_prod_filter bl_set_size by blast have "size ?M = 𝗏 - 1" using v_non_zero by (simp add: assms(1) finite_sets) thus ?thesis using final_size by (simp add: set_break_down_left) qed lemma necess_cond_1_lhs: assumes "x ∈ 𝒱" shows "size ({# p ∈# (mset_set (𝒱 - {x}) ×# {# bl ∈# ℬ . x ∈ bl #}). fst p ∈ snd p#}) = (ℬ rep x) * (𝗄 - 1)" (is "size ({# p ∈# (?M ×# ?B). fst p ∈ snd p#}) = (ℬ rep x) * (𝗄 - 1) ") proof - have "⋀ y. y ∈# ?M ⟹ y ≠ x" using assms by (simp add: finite_sets) have distinct_m: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp have finite_M: "finite (𝒱 - {x})" using finite_sets by auto have block_choices: "size ?B = ℬ rep x" by (simp add: assms(1) point_replication_number_def) have bl_size: "∀ bl ∈# ?B. card {p ∈ 𝒱 . p ∈ bl } = 𝗄 " using uniform_unfold_point_set by simp have x_in_set: "∀ bl ∈# ?B . {x} ⊆ {p ∈ 𝒱. p ∈ bl}" using assms by auto then have "∀ bl ∈# ?B. card {p ∈ (𝒱 - {x}) . p ∈ bl } = card ({p ∈ 𝒱 . p ∈ bl } - {x})" by (simp add: set_filter_diff_card) then have "∀ bl ∈# ?B. card {p ∈ (𝒱 - {x}) . p ∈ bl } = 𝗄 - 1" using bl_size x_in_set card_Diff_subset finite_sets k_non_zero by auto then have "⋀ bl . bl ∈# ?B ⟹ size {#p ∈# ?M . p ∈ bl#} = 𝗄 - 1" using assms finite_M card_size_filter_eq by auto then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * (𝗄 - 1)" using distinct_m size_Union_distinct_cart_prod_filter2 by blast thus ?thesis using block_choices k_non_zero by (simp add: set_break_down_right) qed lemma r_constant: "x ∈ 𝒱 ⟹ (ℬ rep x) * (𝗄 -1) = Λ * (𝗏 - 1)" using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty by force lemma replication_number_value: assumes "x ∈ 𝒱" shows "(ℬ rep x) = Λ * (𝗏 - 1) div (𝗄 - 1)" using min_block_size_2 r_constant assms by (metis diff_is_0_eq diffs0_imp_equal div_by_1 k_non_zero nonzero_mult_div_cancel_right one_div_two_eq_zero one_le_numeral zero_neq_one) lemma r_constant_alt: "∀ x ∈ 𝒱. ℬ rep x = Λ * (𝗏 - 1) div (𝗄 - 1)" using r_constant replication_number_value by blast end text ‹Using the first necessary condition, it is possible to show that a bibd has a constant replication number› sublocale bibd ⊆ constant_rep_design 𝒱 ℬ "(Λ * (𝗏 - 1) div (𝗄 - 1))" using r_constant_alt by (unfold_locales) simp_all lemma (in t_design) bibdI [intro]: "𝗍 = 2 ⟹ bibd 𝒱 ℬ 𝗄 Λ⇩_{t}" using t_lt_order block_size_t by (unfold_locales) (simp_all) context bibd begin abbreviation "𝗋 ≡ (Λ * (𝗏 - 1) div (𝗄 - 1))" lemma necessary_condition_one: shows "𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)" using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty rep_number by auto lemma bibd_point_occ_rep: assumes "x ∈ bl" assumes "bl ∈# ℬ" shows "(ℬ - {#bl#}) rep x = 𝗋 - 1" proof - have xin: "x ∈ 𝒱" using assms wf_invalid_point by blast then have rep: "size {# blk ∈# ℬ. x ∈ blk #} = 𝗋" using rep_number_unfold_set by simp have "(ℬ - {#bl#}) rep x = size {# blk ∈# (ℬ - {#bl#}). x ∈ blk #}" by (simp add: point_replication_number_def) then have "(ℬ - {#bl#}) rep x = size {# blk ∈# ℬ. x ∈ blk #} - 1" by (simp add: assms size_Diff_singleton) then show ?thesis using assms rep r_gzero by simp qed lemma necess_cond_2_lhs: "size {# x ∈# (mset_set 𝒱 ×# ℬ) . (fst x) ∈ (snd x) #} = 𝗏 * 𝗋" proof - let ?M = "mset_set 𝒱" have "⋀ p . p ∈# ?M ⟹ size ({# bl ∈# ℬ . p ∈ bl #}) = 𝗋" using finite_sets rep_number_unfold_set r_gzero nat_eq_iff2 by auto then have "size (∑p∈#?M. ({#p#} ×# {#bl ∈# ℬ. p ∈ bl#})) = size ?M * (𝗋)" using mset_points_distinct size_Union_distinct_cart_prod_filter by blast thus ?thesis using r_gzero by (simp add: set_break_down_left) qed lemma necess_cond_2_rhs: "size {# x ∈# (mset_set 𝒱 ×# ℬ) . (fst x) ∈ (snd x) #} = 𝖻*𝗄" (is "size {# x ∈# (?M ×# ?B). (fst x) ∈ (snd x) #} = 𝖻*𝗄") proof - have "⋀ bl . bl ∈# ?B ⟹ size ({# p ∈# ?M . p ∈ bl #}) = 𝗄" using uniform k_non_zero uniform_unfold_point_set_mset by fastforce then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * 𝗄" using mset_points_distinct size_Union_distinct_cart_prod_filter2 by blast thus ?thesis using k_non_zero by (simp add: set_break_down_right) qed lemma necessary_condition_two: shows "𝗏 * 𝗋 = 𝖻 * 𝗄" using necess_cond_2_lhs necess_cond_2_rhs by simp theorem admissability_conditions: "𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)" "𝗏 * 𝗋 = 𝖻 * 𝗄" using necessary_condition_one necessary_condition_two by auto subsubsection ‹BIBD Param Relationships› lemma bibd_block_number: "𝖻 = Λ * 𝗏 * (𝗏 - 1) div (𝗄 * (𝗄-1))" proof - have "𝖻 * 𝗄 = (𝗏 * 𝗋)" using necessary_condition_two by simp then have k_dvd: "𝗄 dvd (𝗏 * 𝗋)" by (metis dvd_triv_right) then have "𝖻 = (𝗏 * 𝗋) div 𝗄" using necessary_condition_two min_block_size_2 by auto then have "𝖻 = (𝗏 * ((Λ * (𝗏 - 1) div (𝗄 - 1)))) div 𝗄" by simp then have "𝖻 = (𝗏 * Λ * (𝗏 - 1)) div ((𝗄 - 1)* 𝗄)" using necessary_condition_one necessary_condition_two dvd_div_div_eq_mult dvd_div_eq_0_iff dvd_triv_right mult.assoc mult.commute mult.left_commute mult_eq_0_iff by (smt (z3) b_non_zero) then show ?thesis by (simp add: mult.commute) qed lemma symmetric_condition_1: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1) ⟹ 𝖻 = 𝗏 ∧ 𝗋 = 𝗄" using b_non_zero bibd_block_number mult_eq_0_iff necessary_condition_two necessary_condition_one by auto lemma index_lt_replication: "Λ < 𝗋" proof - have 1: "𝗋 * (𝗄 - 1) = Λ * (𝗏 - 1)" using admissability_conditions by simp have lhsnot0: "𝗋 * (𝗄 - 1) ≠ 0" using no_zero_divisors rep_not_zero by (metis div_by_0) then have rhsnot0: "Λ * (𝗏 - 1) ≠ 0" using 1 by presburger have "𝗄 - 1 < 𝗏 - 1" using incomplete b_non_zero bibd_block_number not_less_eq by fastforce thus ?thesis using 1 lhsnot0 rhsnot0 k_non_zero mult_le_less_imp_less r_gzero by (metis div_greater_zero_iff less_or_eq_imp_le nat_less_le nat_neq_iff) qed lemma index_not_zero: "Λ ≥ 1" by (metis div_0 leI less_one mult_not_zero rep_not_zero) lemma r_ge_two: "𝗋 ≥ 2" using index_lt_replication index_not_zero by linarith lemma block_num_gt_rep: "𝖻 > 𝗋" proof - have fact: "𝖻 * 𝗄 = 𝗏 * 𝗋" using admissability_conditions by auto have lhsnot0: "𝖻 * 𝗄 ≠ 0" using k_non_zero b_non_zero by auto then have rhsnot0: "𝗏 * 𝗋 ≠ 0" using fact by simp then show ?thesis using incomplete lhsnot0 using complement_rep_number constant_rep_design.r_gzero incomplete_imp_incomp_block by fastforce qed lemma bibd_subset_occ: assumes "x ⊆ bl" and "bl ∈# ℬ" and "card x = 2" shows "size {# blk ∈# (ℬ - {#bl#}). x ⊆ blk #} = Λ - 1" proof - have index: "size {# blk ∈# ℬ. x ⊆ blk #} = Λ" using points_index_def balanced assms by (metis (full_types) subset_eq wf_invalid_point) then have "size {# blk ∈# (ℬ - {#bl#}). x ⊆ blk #} = size {# blk ∈# ℬ. x ⊆ blk #} - 1" by (simp add: assms size_Diff_singleton) then show ?thesis using assms index_not_zero index by simp qed lemma necess_cond_one_param_balance: "𝖻 > 𝗏 ⟹ 𝗋 > 𝗄" using necessary_condition_two b_positive by (metis div_le_mono2 div_mult_self1_is_m div_mult_self_is_m nat_less_le r_gzero v_non_zero) subsection ‹Constructing New bibd's› text ‹There are many constructions on bibd's to establish new bibds (or other types of designs). This section demonstrates this using both existing constructions, and by defining new constructions.› subsubsection ‹BIBD Complement, Multiple, Combine› lemma comp_params_index_pair: assumes "{x, y} ⊆ 𝒱" assumes "x ≠ y" shows "ℬ⇧^{C}index {x, y} = 𝖻 + Λ - 2*𝗋" proof - have xin: "x ∈ 𝒱" and yin: "y ∈ 𝒱" using assms by auto have ge: "2*𝗋 ≥ Λ" using index_lt_replication using r_gzero by linarith have lambda: "size {# b ∈# ℬ . x ∈ b ∧ y ∈ b#} = Λ" using points_index_pair assms by simp have s1: "ℬ⇧^{C}index {x, y} = size {# b ∈# ℬ . x ∉ b ∧ y ∉ b #}" using complement_index_2 assms by simp also have s2: "... = size ℬ - (size {# b ∈# ℬ . ¬ (x ∉ b ∧ y ∉ b) #})" using size_filter_neg by blast also have "... = size ℬ - (size {# b ∈# ℬ . x ∈ b ∨ y ∈ b#})" by auto also have "... = 𝖻 - (size {# b ∈# ℬ . x ∈ b ∨ y ∈ b#})" by (simp add: of_nat_diff) finally have "ℬ⇧^{C}index {x, y} = 𝖻 - (size {# b ∈# ℬ . x ∈ b#} + size {# b ∈# ℬ . y ∈ b#} - size {# b ∈# ℬ . x ∈ b ∧ y ∈ b#})" by (simp add: mset_size_partition_dep s2 s1) then have "ℬ⇧^{C}index {x, y} = 𝖻 - (𝗋 + 𝗋 - Λ)" using rep_number_unfold_set lambda xin yin by presburger then have "ℬ⇧^{C}index {x, y} = 𝖻 - (2*𝗋 - Λ)" using index_lt_replication by (metis mult_2) thus ?thesis using ge diff_diff_right by simp qed lemma complement_bibd_index: assumes "ps ⊆ 𝒱" assumes "card ps = 2" shows "ℬ⇧^{C}index ps = 𝖻 + Λ - 2*𝗋" proof - obtain x y where set: "ps = {x, y}" using b_non_zero bibd_block_number diff_is_0_eq incomplete mult_0_right nat_less_le design_points_nempty assms by (metis card_2_iff) then have "x ≠ y" using assms by auto thus ?thesis using comp_params_index_pair assms by (simp add: set) qed lemma complement_bibd: assumes "𝗄 ≤ 𝗏 - 2" shows "bibd 𝒱 ℬ⇧^{C}(𝗏 - 𝗄) (𝖻 + Λ - 2*𝗋)" proof - interpret des: incomplete_design 𝒱 "ℬ⇧^{C}" "(𝗏 - 𝗄)" using assms complement_incomplete by blast show ?thesis proof (unfold_locales, simp_all) show "2 ≤ des.𝗏" using assms block_size_t by linarith show "⋀ps. ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ⇧^{C}index ps = 𝖻 + Λ - 2 * (Λ * (des.𝗏 - Suc 0) div (𝗄 - Suc 0))" using complement_bibd_index by simp show "2 ≤ des.𝗏 - 𝗄" using assms block_size_t by linarith qed qed lemma multiple_bibd: "n > 0 ⟹ bibd 𝒱 (multiple_blocks n) 𝗄 (Λ * n)" using multiple_t_design by (simp add: bibd_def) end locale two_bibd_eq_points = two_t_designs_eq_points 𝒱 ℬ 𝗄 ℬ' 2 Λ Λ' + des1: bibd 𝒱 ℬ 𝗄 Λ + des2: bibd 𝒱 ℬ' 𝗄 Λ' for 𝒱 ℬ 𝗄 ℬ' Λ Λ' begin lemma combine_is_bibd: "bibd 𝒱⇧^{+}ℬ⇧^{+}𝗄 (Λ + Λ')" by (unfold_locales) sublocale combine_bibd: bibd "𝒱⇧^{+}" "ℬ⇧^{+}" "𝗄" "(Λ + Λ')" by (unfold_locales) end subsubsection ‹Derived Designs› text ‹A derived bibd takes a block from a valid bibd as the new point sets, and the intersection of that block with other blocks as it's block set› locale bibd_block_transformations = bibd + fixes block :: "'a set" ("bl") assumes valid_block: "bl ∈# ℬ" begin definition derived_blocks :: "'a set multiset" ("(ℬ⇧^{D})") where "ℬ⇧^{D}≡ {# bl ∩ b . b ∈# (ℬ - {#bl#}) #}" lemma derive_define_flip: "{# b ∩ bl . b ∈# (ℬ - {#bl#}) #} = ℬ⇧^{D}" by (simp add: derived_blocks_def inf_sup_aci(1)) lemma derived_points_order: "card bl = 𝗄" using uniform valid_block by simp lemma derived_block_num: "bl ∈# ℬ ⟹ size ℬ⇧^{D}= 𝖻 - 1" by (simp add: derived_blocks_def size_remove1_mset_If valid_block) lemma derived_is_wellformed: "b ∈# ℬ⇧^{D}⟹ b ⊆ bl" by (simp add: derived_blocks_def valid_block) (auto) lemma derived_point_subset_orig: "ps ⊆ bl ⟹ ps ⊂ 𝒱" by (simp add: valid_block incomplete_imp_proper_subset subset_psubset_trans) lemma derived_obtain_orig_block: assumes "b ∈# ℬ⇧^{D}" obtains b2 where "b = b2 ∩ bl" and "b2 ∈# remove1_mset bl ℬ" using assms derived_blocks_def by auto sublocale derived_incidence_sys: incidence_system "bl" "ℬ⇧^{D}" using derived_is_wellformed valid_block by (unfold_locales) (auto) sublocale derived_fin_incidence_system: finite_incidence_system "bl" "ℬ⇧^{D}" using valid_block finite_blocks by (unfold_locales) simp_all lemma derived_blocks_nempty: assumes "⋀ b .b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0" assumes "bld ∈# ℬ⇧^{D}" shows "bld ≠ {}" proof - obtain bl2 where inter: "bld = bl2 ∩ bl" and member: "bl2 ∈# remove1_mset bl ℬ" using assms derived_obtain_orig_block by blast then have "bl |∩| bl2 > 0" using assms(1) by blast thus ?thesis using intersection_number_empty_iff finite_blocks valid_block by (metis Int_commute dual_order.irrefl inter) qed lemma derived_is_design: assumes "⋀ b. b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0" shows "design bl ℬ⇧^{D}" proof - interpret fin: finite_incidence_system "bl" "ℬ⇧^{D}" by (unfold_locales) show ?thesis using assms derived_blocks_nempty by (unfold_locales) simp qed lemma derived_is_proper: assumes "⋀ b. b ∈# remove1_mset bl ℬ ⟹ bl |∩| b > 0" shows "proper_design bl ℬ⇧^{D}" proof - interpret des: design "bl" "ℬ⇧^{D}" using derived_is_design assms by fastforce have "𝖻 - 1 > 1" using block_num_gt_rep r_ge_two by linarith then show ?thesis by (unfold_locales) (simp add: derived_block_num valid_block) qed subsubsection ‹Residual Designs› text ‹Similar to derived designs, a residual design takes the complement of a block bl as it's new point set, and the complement of all other blocks with respect to bl.› definition residual_blocks :: "'a set multiset" ("(ℬ⇧^{R})") where "ℬ⇧^{R}≡ {# b - bl . b ∈# (ℬ - {#bl#}) #}" lemma residual_order: "card (bl⇧^{c}) = 𝗏 - 𝗄" by (simp add: valid_block wellformed block_complement_size) lemma residual_block_num: "size (ℬ⇧^{R}) = 𝖻 - 1" using b_positive by (simp add: residual_blocks_def size_remove1_mset_If valid_block int_ops(6)) lemma residual_obtain_orig_block: assumes "b ∈# ℬ⇧^{R}" obtains bl2 where "b = bl2 - bl" and "bl2 ∈# remove1_mset bl ℬ" using assms residual_blocks_def by auto lemma residual_blocks_ss: assumes "b ∈# ℬ⇧^{R}" shows "b ⊆ 𝒱" proof - have "b ⊆ (bl⇧^{c})" using residual_obtain_orig_block by (metis Diff_mono assms block_complement_def in_diffD order_refl wellformed) thus ?thesis using block_complement_subset_points by auto qed lemma residual_blocks_exclude: "b ∈# ℬ⇧^{R}⟹ x ∈ b ⟹ x ∉ bl" using residual_obtain_orig_block by auto lemma residual_is_wellformed: "b ∈# ℬ⇧^{R}⟹ b ⊆ (bl⇧^{c})" apply (auto simp add: residual_blocks_def) by (metis DiffI block_complement_def in_diffD wf_invalid_point) sublocale residual_incidence_sys: incidence_system "bl⇧^{c}" "ℬ⇧^{R}" using residual_is_wellformed by (unfold_locales) lemma residual_is_finite: "finite (bl⇧^{c})" by (simp add: block_complement_def finite_sets) sublocale residual_fin_incidence_sys: finite_incidence_system "bl⇧^{c}" "ℬ⇧^{R}" using residual_is_finite by (unfold_locales) lemma residual_blocks_nempty: assumes "bld ∈# ℬ⇧^{R}" assumes "multiplicity bl = 1" shows "bld ≠ {}" proof - obtain bl2 where inter: "bld = bl2 - bl" and member: "bl2 ∈# remove1_mset bl ℬ" using assms residual_blocks_def by auto then have ne: "bl2 ≠ bl" using assms by (metis count_eq_zero_iff in_diff_count less_one union_single_eq_member) have "card bl2 = card bl" using uniform valid_block member using in_diffD by fastforce then have "card (bl2 - bl) > 0" using finite_blocks member uniform set_card_diff_ge_zero valid_block by (metis in_diffD ne) thus ?thesis using inter by fastforce qed lemma residual_is_design: "multiplicity bl = 1 ⟹ design (bl⇧^{c}) ℬ⇧^{R}" using residual_blocks_nempty by (unfold_locales) lemma residual_is_proper: assumes "multiplicity bl = 1" shows "proper_design (bl⇧^{c}) ℬ⇧^{R}" proof - interpret des: design "bl⇧^{c}" "ℬ⇧^{R}" using residual_is_design assms by blast have "𝖻 - 1 > 1" using r_ge_two block_num_gt_rep by linarith then show ?thesis using residual_block_num by (unfold_locales) auto qed end subsection ‹Symmetric BIBD's› text ‹Symmetric bibd's are those where the order of the design equals the number of blocks› locale symmetric_bibd = bibd + assumes symmetric: "𝖻 = 𝗏" begin lemma rep_value_sym: "𝗋 = 𝗄" using b_non_zero local.symmetric necessary_condition_two by auto lemma symmetric_condition_2: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1)" using necessary_condition_one rep_value_sym by auto lemma sym_design_vk_gt_kl: assumes "𝗄 ≥ Λ + 2" shows "𝗏 - 𝗄 > 𝗄 - Λ" proof (rule ccontr) define k l v where kdef: "k ≡ int 𝗄" and ldef: "l ≡ int Λ" and vdef: "v ≡ int 𝗏" assume "¬ (𝗏 - 𝗄 > 𝗄 - Λ)" then have a: "¬ (v - k > k - l)" using kdef ldef vdef by (metis block_size_lt_v index_lt_replication less_imp_le_nat of_nat_diff of_nat_less_imp_less rep_value_sym) have lge: "l ≥ 0" using ldef by simp have sym: "l * (v- 1) = k * (k - 1)" using symmetric_condition_2 ldef vdef kdef by (metis (mono_tags, lifting) block_size_lt_v int_ops(2) k_non_zero le_trans of_nat_diff of_nat_mult) then have "v ≤ 2 * k - l" using a by linarith then have "v - 1 ≤ 2 * k - l - 1" by linarith then have "l* (v - 1) ≤ l*( 2 * k - l - 1)" using lge mult_le_cancel_left by fastforce then have "k * (k - 1) ≤ l*( 2 * k - l - 1)" by (simp add: sym) then have "k * (k - 1) - l*( 2 * k - l - 1) ≤ 0" by linarith then have "k^2 - k - l* 2 * k + l^2 + l ≤ 0" using mult.commute right_diff_distrib' by (smt (z3) mult_cancel_left1 power2_diff ring_class.ring_distribs(2)) then have "(k - l)*(k - l - 1) ≤ 0" using mult.commute right_diff_distrib' by (smt (z3) ‹k * (k - 1) ≤ l * (2 * k - l - 1)› combine_common_factor) then have "k = l ∨ k = l + 1" using mult_le_0_iff by force thus False using assms kdef ldef by auto qed end context bibd begin lemma symmetric_bibdI: "𝖻 = 𝗏 ⟹ symmetric_bibd 𝒱 ℬ 𝗄 Λ" by unfold_locales simp lemma symmetric_bibdII: "Λ * (𝗏 - 1) = 𝗄 * (𝗄 - 1) ⟹ symmetric_bibd 𝒱 ℬ 𝗄 Λ" using symmetric_condition_1 by unfold_locales blast lemma symmetric_not_admissable: "Λ * (𝗏 - 1) ≠ 𝗄 * (𝗄 - 1) ⟹ ¬ symmetric_bibd 𝒱 ℬ 𝗄 Λ" using symmetric_bibd.symmetric_condition_2 by blast end context symmetric_bibd begin subsubsection ‹Intersection Property on Symmetric BIBDs› text ‹Below is a proof of an important property on symmetric BIBD's regarding the equivalence of intersection numbers and the design index. This is an intuitive counting proof, and involved significantly more work in a formal environment. Based of Lecture Note \<^cite>‹"HerkeLectureNotes2016"›› lemma intersect_mult_set_eq_block: assumes "blv ∈# ℬ" shows "p ∈# ∑⇩_{#}{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#} ⟷ p ∈ blv" proof (auto, simp add: assms finite_blocks) assume assm: "p ∈ blv" then have "(ℬ - {#blv#}) rep p > 0" using bibd_point_occ_rep r_ge_two assms by auto then obtain bl where "bl ∈# (ℬ - {#blv#}) ∧ p ∈ bl" using assms rep_number_g0_exists by metis then show "∃x∈#remove1_mset blv ℬ. p ∈# mset_set (x ∩ blv)" using assms assm finite_blocks by auto qed lemma intersect_mult_set_block_subset_iff: assumes "blv ∈# ℬ" assumes "p ∈# ∑⇩_{#}{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}" shows "p ⊆ blv" proof (rule subsetI) fix x assume asm: "x ∈ p" obtain b2 where "p ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})" using assms by blast then have "p ⊆ blv ∩ b2" by (metis (no_types, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq) thus "x ∈ blv" using asm by auto qed lemma intersect_mult_set_block_subset_card: assumes "blv ∈# ℬ" assumes "p ∈# ∑⇩_{#}{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}" shows "card p = 2" proof - obtain b2 where "p ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})" using assms by blast thus ?thesis by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq) qed lemma intersect_mult_set_block_with_point_exists: assumes "blv ∈# ℬ" and "p ⊆ blv" and "Λ ≥ 2" and "card p = 2" shows "∃x∈#remove1_mset blv ℬ. p ∈# mset_set {y. y ⊆ blv ∧ y ⊆ x ∧ card y = 2}" proof - have "size {#b ∈# ℬ . p ⊆ b#} = Λ" using points_index_def assms by (metis balanced_alt_def_all dual_order.trans wellformed) then have "size {#bl ∈# (ℬ - {#blv#}) . p ⊆ bl#} ≥ 1" using assms by (simp add: size_Diff_singleton) then obtain bl where "bl ∈# (ℬ - {#blv#}) ∧ p ⊆ bl" using assms filter_mset_empty_conv by (metis diff_diff_cancel diff_is_0_eq' le_numeral_extra(4) size_empty zero_neq_one) thus ?thesis using assms finite_blocks by auto qed lemma intersect_mult_set_block_subset_iff_2: assumes "blv ∈# ℬ" and "p ⊆ blv" and "Λ ≥ 2" and "card p = 2" shows "p ∈# ∑⇩_{#}{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (ℬ - {#blv#})#}" by (auto simp add: intersect_mult_set_block_with_point_exists assms) lemma sym_sum_mset_inter_sets_count: assumes "blv ∈# ℬ" assumes "p ∈ blv" shows "count (∑⇩_{#}{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) p = 𝗋 - 1" (is "count (∑⇩_{#}?M) p = 𝗋 - 1") proof - have size_inter: "size {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} = 𝗋 - 1" using bibd_point_occ_rep point_replication_number_def by (metis assms(1) assms(2) size_image_mset) have inter_finite: "∀ bl ∈# (ℬ - {#blv#}) . finite (bl ∩ blv)" by (simp add: assms(1) finite_blocks) have "⋀ bl . bl ∈# (ℬ - {#blv#}) ⟹ p ∈ bl ⟶ count (mset_set (bl ∩ blv)) p = 1" using assms count_mset_set(1) inter_finite by simp then have "⋀ bl . bl ∈# {#b1 ∈#(ℬ - {#blv#}) . p ∈ b1#} ⟹ count (mset_set (bl ∩ blv)) p = 1" by (metis (full_types) count_eq_zero_iff count_filter_mset) then have pin: "⋀ P. P ∈# {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} ⟹ count P p = 1" by blast have "?M = {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} + {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∉ bl#}" by (metis image_mset_union multiset_partition) then have "count (∑⇩_{#}?M) p = size {# mset_set (bl ∩ blv) | bl ∈# (ℬ - {#blv#}) . p ∈ bl#} " using pin by (auto simp add: count_sum_mset) then show ?thesis using size_inter by linarith qed lemma sym_sum_mset_inter_sets_size: assumes "blv ∈# ℬ" shows "size (∑⇩_{#}{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) = 𝗄 * (𝗋 - 1)" (is "size (∑⇩_{#}?M) = 𝗄* (𝗋 - 1)") proof - have eq: "set_mset (∑⇩_{#}{# mset_set (bl ∩ blv) .bl ∈# (ℬ - {#blv#})#}) = blv" using intersect_mult_set_eq_block assms by auto then have k: "card (set_mset (∑⇩_{#}?M)) = 𝗄" by (simp add: assms) have "⋀ p. p ∈# (∑⇩_{#}?M) ⟹ count (∑⇩_{#}?M) p = 𝗋 - 1" using sym_sum_mset_inter_sets_count assms eq by blast thus ?thesis using k size_multiset_set_mset_const_count by metis qed lemma sym_sum_inter_num: assumes "b1 ∈# ℬ" shows "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = 𝗄* (𝗋 - 1)" proof - have "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = (∑b2 ∈#(ℬ - {#b1#}). size (mset_set (b1 ∩ b2)))" by (simp add: intersection_number_def) also have "... = size (∑⇩_{#}{#mset_set (b1 ∩ bl). bl ∈# (ℬ - {#b1#})#})" by (auto simp add: size_big_union_sum) also have "... = size (∑⇩_{#}{#mset_set (bl ∩ b1). bl ∈# (ℬ - {#b1#})#})" by (metis Int_commute) finally have "(∑b2 ∈#(ℬ - {#b1#}). b1 |∩| b2) = 𝗄 * (𝗋 - 1)" using sym_sum_mset_inter_sets_size assms by auto then show ?thesis by simp qed lemma sym_sum_mset_inter2_sets_count: assumes "blv ∈# ℬ" assumes "p ⊆ blv" assumes "card p = 2" shows "count (∑⇩_{#}{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (ℬ - {#blv#})#}) p = Λ - 1" (is "count (∑⇩_{#}?M) p = Λ - 1") proof - have size_inter: "size {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#} = Λ - 1" using bibd_subset_occ assms by simp have "∀ b2 ∈# (ℬ - {#blv#}) . p ⊆ b2 ⟶ count (mset_set{y .y ⊆ blv ∩ b2 ∧ card y = 2}) p = 1" using assms(2) count_mset_set(1) assms(3) by (auto simp add: assms(1) finite_blocks) then have "∀ bl ∈# {#b1 ∈#(ℬ - {#blv#}) . p ⊆ b1#}. count (mset_set {y .y ⊆ blv ∩ bl ∧ card y = 2}) p = 1" using count_eq_zero_iff count_filter_mset by (metis (no_types, lifting)) then have pin: "∀ P ∈# {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#}. count P p = 1" using count_eq_zero_iff count_filter_mset by blast have "?M = {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#} + {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . ¬ (p ⊆ b2)#}" by (metis image_mset_union multiset_partition) then have "count (∑⇩_{#}?M) p = size {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (ℬ - {#blv#}) . p ⊆ b2#}" using pin by (auto simp add: count_sum_mset) then show ?thesis using size_inter by linarith qed lemma sym_sum_mset_inter2_sets_size: assumes "blv ∈# ℬ" shows "size (∑⇩_{#}{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (ℬ - {#blv#})#}) = ( 𝗄 choose 2) * (Λ -1)" (is "size (∑⇩_{#}?M) = (𝗄 choose 2) * (Λ -1)") proof (cases "Λ = 1") case True have empty: "⋀ b2 . b2 ∈# remove1_mset blv ℬ ⟹ {y .y ⊆ blv ∧ y ⊆ b2 ∧ card y = 2} = {}" using index_one_alt_bl_not_exist assms True by blast then show ?thesis using sum_mset.neutral True by (simp add: empty) next case False then have index_min: "Λ ≥ 2" using index_not_zero by linarith have subset_card: "⋀ x . x ∈# (∑⇩_{#}?M) ⟹ card x = 2" proof - fix x assume a: "x ∈# (∑⇩_{#}?M)" then obtain b2 where "x ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(ℬ - {#blv#})" by blast thus "card x = 2" using mem_Collect_eq by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set) qed have eq: "set_mset (∑⇩_{#}?M) = {bl . bl ⊆ blv ∧ card bl = 2}" proof show "set_mset (∑⇩_{#}?M) ⊆ {bl . bl ⊆ blv ∧ card bl = 2}" using subset_card intersect_mult_set_block_subset_iff assms by blast show "{bl . bl ⊆ blv ∧ card bl = 2} ⊆ set_mset (∑⇩_{#}?M)" using intersect_mult_set_block_subset_iff_2 assms index_min by blast qed have "card blv = 𝗄" using uniform assms by simp then have k: "card (set_mset (∑⇩_{#}?M)) = (𝗄 choose 2)" using eq n_subsets by (simp add: n_subsets assms finite_blocks) thus ?thesis using k size_multiset_set_mset_const_count sym_sum_mset_inter2_sets_count assms eq by (metis (no_types, lifting) intersect_mult_set_block_subset_iff subset_card) qed lemma sum_choose_two_inter_num: assumes "b1 ∈# ℬ" shows "(∑b2 ∈# (ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1) div 2)) * (𝗏 -1)" proof - have div_fact: "2 dvd (Λ * (Λ - 1))" by fastforce have div_fact_2: "2 dvd (Λ * (𝗏 - 1))" using symmetric_condition_2 by fastforce have "(∑b2 ∈# (ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = (∑b2 ∈# (ℬ - {#b1#}). (b1 |∩|⇩2 b2 ))" using n_inter_num_choose_design_inter assms by (simp add: in_diffD) then have sum_fact: "(∑b2 ∈# (ℬ - {#b1#}).((b1 |∩| b2) choose 2)) = (𝗄 choose 2) * (Λ -1)" using assms sym_sum_mset_inter2_sets_size by (auto simp add: size_big_union_sum n_intersect_num_subset_def) have "(𝗄 choose 2) * (Λ -1) = ((Λ * (𝗏 - 1) div 2)) * (Λ -1)" using choose_two symmetric_condition_2 k_non_zero by auto then have "(𝗄 choose 2) * (Λ -1) = ((Λ * (Λ - 1) div 2)) * (𝗏 -1)" using div_fact div_fact_2 by (smt div_mult_swap mult.assoc mult.commute) then show ?thesis using sum_fact by simp qed lemma sym_sum_inter_num_sq: assumes "b1 ∈# ℬ" shows "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = Λ^2 * ( 𝗏 - 1)" proof - have dvd: "2 dvd (( 𝗏 - 1) * (Λ * (Λ - 1)))" by fastforce have inner_dvd: "∀ bl ∈# (remove1_mset b1 ℬ). 2 dvd ((b1 |∩| bl) * ((b1 |∩| bl) - 1))" by force have diff_le: "⋀ bl . bl ∈# (remove1_mset b1 ℬ) ⟹ (b1 |∩| bl) ≤ (b1 |∩| bl)^2" by (simp add: power2_nat_le_imp_le) have a: "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = (∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2)" using choose_two by (simp add: intersection_num_non_neg) have b: "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = (∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2))" by simp have gtsq: "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) ≥ (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl))" by (simp add: diff_le sum_mset_mono) have "(∑b2 ∈#(ℬ - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1)) div 2) * ( 𝗏 - 1)" using sum_choose_two_inter_num assms by blast then have start: "(∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2) = ((Λ * (Λ - 1)) div 2) * (𝗏 - 1)" using a b by linarith have sum_dvd: "2 dvd (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1))" using sum_mset_dvd by (metis (no_types, lifting) dvd_mult dvd_mult2 dvd_refl odd_two_times_div_two_nat) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2 = ((Λ * (Λ - 1)) div 2) * (𝗏 - 1)" using start sum_mset_distrib_div_if_dvd inner_dvd by (metis (mono_tags, lifting) image_mset_cong2) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2 = (𝗏 - 1) * ((Λ * (Λ - 1)) div 2)" by simp then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) = (𝗏 - 1) * (Λ * (Λ - 1))" by (metis (no_types, lifting) div_mult_swap dvdI dvd_div_eq_iff dvd_mult dvd_mult2 odd_two_times_div_two_nat sum_dvd) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2 - (b1 |∩| bl)) = (𝗏 - 1) * (Λ * (Λ - 1))" using diff_mult_distrib2 by (metis (no_types, lifting) multiset.map_cong0 nat_mult_1_right power2_eq_square) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) - (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)) = (𝗏 - 1) * (Λ * (Λ - 1))" using sum_mset_add_diff_nat[of "(remove1_mset b1 ℬ)" "λ bl . (b1 |∩| bl)" "λ bl . (b1 |∩| bl)^2"] diff_le by presburger then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)) + (𝗏 - 1) * (Λ * (Λ - 1))" using gtsq by (metis le_add_diff_inverse) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) + ((𝗏 - 1) * (Λ * (Λ - 1)))" using sym_sum_inter_num assms rep_value_sym symmetric_condition_2 by auto then have prev: "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) * (Λ - 1) + (Λ * (𝗏 - 1))" by fastforce then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = (Λ * (𝗏 - 1)) * (Λ)" by (metis Nat.le_imp_diff_is_add add_mult_distrib2 index_not_zero nat_mult_1_right) then have "(∑bl ∈# (remove1_mset b1 ℬ). (b1 |∩| bl)^2) = Λ * Λ * (𝗏 - 1)" using mult.commute by simp thus ?thesis by (simp add: power2_eq_square) qed lemma sym_sum_inter_num_to_zero: assumes "b1 ∈# ℬ" shows "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - (int Λ))^2) = 0" proof - have rm1_size: "size (remove1_mset b1 ℬ) = 𝗏 - 1" using assms b_non_zero int_ops(6) by (auto simp add: symmetric size_remove1_mset_If) have "(∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2)) = (∑bl ∈# (remove1_mset b1 ℬ). (((b1 |∩| bl))^2))" by simp then have ssi: "(∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2)) = Λ^2 * (𝗏 - 1)" using sym_sum_inter_num_sq assms by simp have "⋀ bl . bl ∈# (remove1_mset b1 ℬ) ⟹ (int (b1 |∩| bl) - (int Λ))^2 = (((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))) + ((int Λ)^2))" by (simp add: power2_diff) then have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - (int Λ))^2) = (∑bl ∈# (remove1_mset b1 ℬ). (((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))) + ((int Λ)^2)))" using sum_over_fun_eq by auto also have "... = (∑bl ∈# (remove1_mset b1 ℬ). (((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))))) + (∑ bl ∈# (remove1_mset b1 ℬ) . ((int Λ)^2))" by (simp add: sum_mset.distrib) also have "... = (∑bl ∈# (remove1_mset b1 ℬ). ((int (b1 |∩| bl))^2)) - (∑bl ∈# (remove1_mset b1 ℬ). (2 * (int Λ) * (int (b1 |∩| bl)))) + (∑ bl ∈# (remove1_mset b1 ℬ) . ((int Λ)^2))" using sum_mset_add_diff_int[of "(λ bl . ((int (b1 |∩| bl))^2))" "(λ bl . (2 * (int Λ) * (int (b1 |∩| bl))))" "(remove1_mset b1 ℬ)"] by simp also have "... = Λ^2 * (𝗏 - 1) - 2 * (int Λ) *(∑bl ∈# (remove1_mset b1 ℬ). ((b1 |∩| bl))) + (𝗏 - 1) * ((int Λ)^2)" using ssi rm1_size assms by (simp add: sum_mset_distrib_left) also have "... = 2 * Λ^2 * (𝗏 - 1) - 2 * (int Λ) *(𝗄* (𝗋 - 1))" using sym_sum_inter_num assms by simp also have "... = 2 * Λ^2 * (𝗏 - 1) - 2 * (int Λ) * (Λ * (𝗏 - 1))" using rep_value_sym symmetric_condition_2 by simp finally have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - int Λ)^2) = 0" by (auto simp add: power2_eq_square) thus ?thesis by simp qed theorem sym_block_intersections_index [simp]: assumes "b1 ∈# ℬ" assumes "b2 ∈# (ℬ - {#b1#})" shows "b1 |∩| b2 = Λ" proof - define l where l_def: "l = int Λ" then have pos: "⋀ bl . (int (b1 |∩| bl) - l)^2 ≥ 0" by simp have "(∑bl ∈# (remove1_mset b1 ℬ). (int (b1 |∩| bl) - l)^2) = 0" using sym_sum_inter_num_to_zero assms l_def by simp then have "⋀ bl. bl ∈ set_mset (remove1_mset b1 ℬ) ⟹ (int (b1 |∩| bl) - l)^2 = 0" using sum_mset_0_iff_ge_0 pos by (metis (no_types, lifting)) then have "⋀ bl. bl ∈ set_mset (remove1_mset b1 ℬ) ⟹ int (b1 |∩| bl) = l" by auto thus ?thesis using assms(2) l_def of_nat_eq_iff by blast qed subsubsection ‹Symmetric BIBD is Simple› lemma sym_block_mult_one [simp]: assumes "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 then have blleft: "bl ∈# (ℬ - {#bl#})" using in_diff_count by fastforce have "bl |∩| bl = 𝗄" using k_non_zero assms by (simp add: intersection_number_def) then have keql: "𝗄 = Λ" using sym_block_intersections_index blleft assms by simp then have "𝗏 = 𝗄" using keql index_lt_replication rep_value_sym block_size_lt_v diffs0_imp_equal k_non_zero zero_diff by linarith then show False using incomplete by simp qed end sublocale symmetric_bibd ⊆ simple_design by unfold_locales simp subsubsection ‹Residual/Derived Sym BIBD Constructions› text ‹Using the intersect result, we can reason further on residual and derived designs. Proofs based off lecture notes \<^cite>‹"HerkeLectureNotes2016"›› locale symmetric_bibd_block_transformations = symmetric_bibd + bibd_block_transformations begin lemma derived_block_size [simp]: assumes "b ∈# ℬ⇧^{D}" shows "card b = Λ" proof - obtain bl2 where set: "bl2 ∈# remove1_mset bl ℬ" and inter: "b = bl2 ∩ bl" using derived_blocks_def assms by (meson derived_obtain_orig_block) then have "card b = bl2 |∩| bl" by (simp add: intersection_number_def) thus ?thesis using sym_block_intersections_index using set intersect_num_commute valid_block by fastforce qed lemma derived_points_index [simp]: assumes "ps ⊆ bl" assumes "card ps = 2" shows "ℬ⇧^{D}index ps = Λ - 1" proof - have b_in: "⋀ b . b ∈# (remove1_mset bl ℬ) ⟹ ps ⊆ b ⟹ ps ⊆ b ∩ bl" using assms by blast then have orig: "ps ⊆ 𝒱" using valid_block assms wellformed by blast then have lam: "size {# b ∈# ℬ . ps ⊆ b #} = Λ" using balanced by (simp add: assms(2) points_index_def) then have "size {# b ∈# remove1_mset bl ℬ . ps ⊆ b #} = size {# b ∈# ℬ . ps ⊆ b #} - 1" using assms valid_block by (simp add: size_Diff_submset) then have "size {# b ∈# remove1_mset bl ℬ . ps ⊆ b #} = Λ - 1" using lam index_not_zero by linarith then have "size {# bl ∩ b | b ∈# (remove1_mset bl ℬ) . ps ⊆ bl ∩ b #} = Λ - 1" using b_in by (metis (no_types, lifting) Int_subset_iff filter_mset_cong size_image_mset) then have "size {# x ∈# {# bl ∩ b . b ∈# (remove1_mset bl ℬ) #} . ps ⊆ x #} = Λ - 1" by (metis image_mset_filter_swap) then have "size {# x ∈# ℬ⇧^{D}. ps ⊆ x #} = Λ - 1" by (simp add: derived_blocks_def) thus ?thesis by (simp add: points_index_def) qed lemma sym_derive_design_bibd: assumes "Λ > 1" shows "bibd bl ℬ⇧^{D}Λ (Λ - 1)" proof - interpret des: proper_design bl "ℬ⇧^{D}" using derived_is_proper assms valid_block by auto have "Λ < 𝗄" using index_lt_replication rep_value_sym by linarith then show ?thesis using derived_block_size assms derived_points_index derived_points_order by (unfold_locales) (simp_all) qed lemma residual_block_size [simp]: assumes "b ∈# ℬ⇧^{R}" shows "card b = 𝗄 - Λ" proof - obtain bl2 where sub: "b = bl2 - bl" and mem: "bl2 ∈# remove1_mset bl ℬ" using assms residual_blocks_def by auto then have "card b = card bl2 - card (bl2 ∩ bl)" using card_Diff_subset_Int valid_block finite_blocks by (simp add: card_Diff_subset_Int) then have "card b = card bl2 - bl2 |∩| bl" using finite_blocks card_inter_lt_single by (simp add: intersection_number_def) thus ?thesis using sym_block_intersections_index uniform by (metis valid_block in_diffD intersect_num_commute mem) qed lemma residual_index [simp]: assumes "ps ⊆ bl⇧^{c}" assumes "card ps = 2" shows "(ℬ⇧^{R}) index ps = Λ" proof - have a: "⋀ b . (b ∈# remove1_mset bl ℬ ⟹ ps ⊆ b ⟹ ps ⊆ (b - bl))" using assms by (smt DiffI block_comp_elem_alt_left in_diffD subset_eq wellformed) have b: "⋀ b . (b ∈# remove1_mset bl ℬ ⟹ ps ⊆ (b - bl) ⟹ ps ⊆ b)" by auto have not_ss: "¬ (ps ⊆ bl)" using set_diff_non_empty_not_subset blocks_nempty t_non_zero assms block_complement_def by fastforce have "ℬ⇧^{R}index ps = size {# x ∈# {# b - bl . b ∈# (remove1_mset bl ℬ) #} . ps ⊆ x #}" using assms valid_block by (simp add: points_index_def residual_blocks_def) also have "... = size {# b - bl | b ∈# (remove1_mset bl ℬ) . ps ⊆ b - bl #} " by (metis image_mset_filter_swap) finally have "ℬ⇧^{R}index ps = size {# b ∈# (remove1_mset bl ℬ) . ps ⊆ b #} " using a b by (metis (no_types, lifting) filter_mset_cong size_image_mset) thus ?thesis using balanced not_ss assms points_index_alt_def block_complement_subset_points by auto qed lemma sym_residual_design_bibd: assumes "𝗄 ≥ Λ + 2" shows "bibd (bl⇧^{c}) ℬ⇧^{R}(𝗄 - Λ) Λ" proof - interpret des: proper_design "bl⇧^{c}" "ℬ⇧^{R}" using residual_is_proper assms(1) valid_block sym_block_mult_one by fastforce show ?thesis using residual_block_size assms sym_design_vk_gt_kl residual_order residual_index by(unfold_locales) simp_all qed end subsection ‹BIBD's and Other Block Designs› text ‹BIBD's are closely related to other block designs by indirect inheritance› sublocale bibd ⊆ k_Λ_PBD 𝒱 ℬ Λ 𝗄 using block_size_gt_t by (unfold_locales) simp_all lemma incomplete_PBD_is_bibd: assumes "k < card V" and "k_Λ_PBD V B Λ k" shows "bibd V B k Λ" proof - interpret inc: incomplete_design V B k using assms by (auto simp add: block_design.incomplete_designI k_Λ_PBD.axioms(2)) interpret pairwise_balance: pairwise_balance V B Λ using assms by (auto simp add: k_Λ_PBD.axioms(1)) show ?thesis using assms k_Λ_PBD.block_size_t by (unfold_locales) (simp_all) qed lemma (in bibd) bibd_to_pbdI[intro]: assumes "Λ = 1" shows "k_PBD 𝒱 ℬ 𝗄" proof - interpret pbd: k_Λ_PBD 𝒱 ℬ Λ 𝗄 by (simp add: k_Λ_PBD_axioms) show ?thesis using assms by (unfold_locales) (simp_all add: t_lt_order min_block_size_2) qed locale incomplete_PBD = incomplete_design + k_Λ_PBD sublocale incomplete_PBD ⊆ bibd using block_size_t by (unfold_locales) simp end