# Theory BIBD

(* 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
have b_contents: "⋀ bl. bl ∈# ?B ⟹ x ∈ bl" using assms by auto
have "⋀ y. y ∈# ?M ⟹ y ≠ x" using assms
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
thus ?thesis using final_size
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
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"
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})"
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 #}"
then have "(ℬ - {#bl#}) rep x = size {# blk ∈# ℬ. x ∈ blk #} - 1"
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
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

"𝗋 * (𝗄 - 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"
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
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"

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

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)"
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)"
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)) = 𝗄"
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)))"
also have "... = size (∑⇩#{#mset_set (b1 ∩ bl). bl ∈# (ℬ - {#b1#})#})"
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"
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))"
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
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)) * (Λ)"
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))"
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))"
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"
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
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"
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
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
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
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 𝒱 ℬ Λ 𝗄
end