Quelle  BIBD.thy

(* 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,
  usually the first type of design explored in a design theory course.
  designs are a type of t-design, where $t = 2$›

subsection ‹BIBD Basics›
locale bibd = t_design V B k 2 Λ 
  for point_set (‹V›) and block_collection (‹B›) 
    and u_block_size (‹k›) and index (‹Λ›)

begin

lemma min_block_size_2: "k ≥ 2" 
  using block_size_t by simp

lemma points_index_pair: "y ∈ V ==> x ∈ V ==> x ≠ y ==> size ({# bl ∈# B . {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 ∈# B" and "p ⊆ blv" and "card p = 2" 
  shows "{#bl ∈# remove1_mset blv B . p ⊆ bl#} = {#}"
proof -
  have blv_in: "blv ∈# filter_mset ((⊆) p) B"
    using assms by simp
  have "p ⊆ V" using assms wellformed by auto
  then have "size (filter_mset ((⊆) p) B) = 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 ∈# B" and "p ⊆ blv" and "card p = 2" 
  shows" ∧ bl. bl ∈# remove1_mset blv B ==> ¬ (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
  first theorems on designs. Proofs based off MATH3301 lecture notes cite‹"HerkeLectureNotes2016"›
 and Stinson cite‹"stinsonCombinatorialDesignsConstructions2004"››

lemma necess_cond_1_rhs: 
  assumes "x ∈ V"
  shows "size ({# p ∈# (mset_set (V - {x}) ×# {# bl ∈# B . x ∈ bl #}). fst p ∈ snd p#}) = Λ * (v- 1)"
proof -
  let ?M = "mset_set (V - {x})"
  let ?B = "{# bl ∈# B . x ∈ bl #}"
  have m_distinct: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp
  have y_point: "∧ y . y ∈# ?M ==> y ∈ V" 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 = v - 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 ∈ V"
  shows "size ({# p ∈# (mset_set (V - {x}) ×# {# bl ∈# B . x ∈ bl #}). fst p ∈ snd p#})
      = (B rep x) * (k - 1)" 
    (is "size ({# p ∈# (?M ×# ?B). fst p ∈ snd p#}) = (B rep x) * (k - 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 (V - {x})" using finite_sets by auto
  have block_choices: "size ?B = B rep x"
    by (simp add: assms(1) point_replication_number_def)
  have bl_size: "∀ bl ∈# ?B. card {p ∈ V . p ∈ bl } = k " using uniform_unfold_point_set by simp
  have x_in_set: "∀ bl ∈# ?B . {x} ⊆ {p ∈ V. p ∈ bl}" using assms by auto
  then have "∀ bl ∈# ?B. card {p ∈ (V - {x}) . p ∈ bl } = card ({p ∈ V . p ∈ bl } - {x})" 
    by (simp add: set_filter_diff_card)
  then have "∀ bl ∈# ?B. card {p ∈ (V - {x}) . p ∈ bl } = k - 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#} = k - 1" 
    using assms finite_M card_size_filter_eq by auto
  then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * (k - 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 ∈ V ==> (B rep x) * (k -1) = Λ * (v - 1)"
  using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty by force

lemma replication_number_value:
  assumes "x ∈ V"
  shows "(B rep x) = Λ * (v - 1) div (k - 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 ∈ V. B rep x = Λ * (v - 1) div (k - 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
  constant replication number›

sublocale bibd ⊆ constant_rep_design V B  "(Λ * (v - 1) div (k - 1))"
  using r_constant_alt by (unfold_locales) simp_all

lemma (in t_design) bibdI [intro]: "t = 2 ==> bibd V B k Λ_t"
  using t_lt_order block_size_t by (unfold_locales) (simp_all)

context bibd
begin

abbreviation "r ≡ (Λ * (v - 1) div (k - 1))"

lemma necessary_condition_one: 
  shows "r * (k - 1) = Λ * (v - 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 ∈# B"
  shows  "(B - {#bl#}) rep x = r - 1"
proof -
  have xin: "x ∈ V" using assms wf_invalid_point by blast
  then have rep: "size {# blk ∈# B. x ∈ blk #} = r" using rep_number_unfold_set by simp
  have "(B - {#bl#}) rep x = size {# blk ∈# (B - {#bl#}). x ∈ blk #}" 
    by (simp add: point_replication_number_def)
  then have "(B - {#bl#}) rep x = size {# blk ∈# B. 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 V ×# B) . (fst x) ∈ (snd x) #} = v * r" 
proof -
  let ?M = "mset_set V"
  have "∧ p . p ∈# ?M ==> size ({# bl ∈# B . p ∈ bl #}) = r"
    using finite_sets rep_number_unfold_set r_gzero nat_eq_iff2 by auto 
  then have "size (∑p∈#?M. ({#p#} ×# {#bl ∈# B. p ∈ bl#})) = size ?M * (r)" 
    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 V ×# B) . (fst x) ∈ (snd x) #} = b*k" 
  (is "size {# x ∈# (?M ×# ?B). (fst x) ∈ (snd x) #} = b*k")
proof -
  have "∧ bl . bl ∈# ?B ==> size ({# p ∈# ?M . p ∈ bl #}) = k" 
    using uniform k_non_zero uniform_unfold_point_set_mset by fastforce
  then have "size (∑bl∈#?B. ( {# p ∈# ?M . p ∈ bl #} ×# {#bl#})) = size (?B) * k" 
    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 "v * r = b * k"
  using necess_cond_2_lhs necess_cond_2_rhs by simp

theorem admissability_conditions:
"r * (k - 1) = Λ * (v - 1)"
"v * r = b * k"
  using necessary_condition_one necessary_condition_two by auto

subsubsection ‹BIBD Param Relationships›

lemma bibd_block_number: "b = Λ * v * (v - 1) div (k * (k-1))"
proof -
  have "b * k = (v * r)" using necessary_condition_two by simp
  then have k_dvd: "k dvd (v * r)" by (metis dvd_triv_right) 
  then have "b = (v * r) div k" using necessary_condition_two min_block_size_2 by auto
  then have "b = (v * ((Λ * (v - 1) div (k - 1)))) div k" by simp
  then have "b = (v * Λ * (v - 1)) div ((k - 1)* k)" 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 (verit) b_non_zero) 
  then show ?thesis by (simp add: mult.commute) 
qed

lemma symmetric_condition_1: "Λ * (v - 1) = k * (k - 1) ==> b = v ∧ r = k"
  using b_non_zero bibd_block_number mult_eq_0_iff necessary_condition_two necessary_condition_one 
  by auto

lemma index_lt_replication: "Λ < r"
proof -
  have 1: "r * (k - 1) = Λ * (v - 1)" using admissability_conditions by simp
  have lhsnot0: "r * (k - 1) ≠ 0"
    using no_zero_divisors rep_not_zero by (metis div_by_0) 
  then have rhsnot0: "Λ * (v - 1) ≠ 0" using 1 by presburger 
  have "k - 1 < v - 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: "r ≥ 2"
  using index_lt_replication index_not_zero by linarith

lemma block_num_gt_rep: "b > r"
proof -
  have fact: "b * k = v * r" using admissability_conditions by auto
  have lhsnot0: "b * k ≠ 0" using k_non_zero b_non_zero by auto 
  then have rhsnot0: "v * r ≠ 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 ∈# B" and "card x = 2"
  shows "size {# blk ∈# (B - {#bl#}). x ⊆ blk #} = Λ - 1"
proof - 
  have index: "size {# blk ∈# B. x ⊆ blk #} = Λ" using points_index_def balanced assms
    by (metis (full_types) subset_eq wf_invalid_point) 
  then have "size {# blk ∈# (B - {#bl#}). x ⊆ blk #} = size {# blk ∈# B. 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: "b > v ==> r > k"
  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).
  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} ⊆ V"
  assumes "x ≠ y"
  shows "B^C index {x, y} = b + Λ - 2*r"
proof -
  have xin: "x ∈ V" and yin: "y ∈ V" using assms by auto
  have ge: "2*r ≥ Λ" using index_lt_replication
    using r_gzero by linarith 
  have lambda: "size {# b ∈# B . x ∈ b ∧ y ∈ b#} = Λ" using points_index_pair assms by simp
  have s1: "B^C index {x, y} = size {# b ∈# B . x ∉ b ∧ y ∉ b #}" 
    using complement_index_2 assms by simp
  also have s2: "... = size B - (size {# b ∈# B . ¬ (x ∉ b ∧ y ∉ b) #})" 
    using size_filter_neg by blast
  also have "... = size B - (size {# b ∈# B . x ∈ b ∨ y ∈ b#})" by auto
  also have "... = b - (size {# b ∈# B . x ∈ b ∨ y ∈ b#})" by (simp add: of_nat_diff)
  finally have "B^C index {x, y} = b - (size {# b ∈# B . x ∈ b#} +
    size {# b ∈# B . y ∈ b#} - size {# b ∈# B . x ∈ b ∧ y ∈ b#})" 
    by (simp add: mset_size_partition_dep s2 s1) 
  then have "B^C index {x, y} = b - (r + r - Λ)" using rep_number_unfold_set lambda xin yin
    by presburger
  then have "B^C index {x, y} = b - (2*r - Λ)"
    using index_lt_replication by (metis mult_2) 
  thus ?thesis using ge diff_diff_right by simp  
qed

lemma complement_bibd_index: 
  assumes "ps ⊆ V"
  assumes "card ps = 2"
  shows "B^C index ps = b + Λ - 2*r"
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 "k ≤ v - 2" 
  shows "bibd V B^C (v - k) (b + Λ - 2*r)"
proof -
  interpret des: incomplete_design V "B^C" "(v - k)" 
    using assms complement_incomplete by blast
  show ?thesis proof (unfold_locales, simp_all)
    show "2 ≤ des.v" using assms block_size_t by linarith 
    show "∧ps. ps ⊆ V ==> card ps = 2 ==>
      B^C index ps = b + Λ - 2 * (Λ * (des.v - Suc 0) div (k - Suc 0))" 
      using complement_bibd_index by simp
    show "2 ≤ des.v - k" using assms block_size_t by linarith 
  qed
qed

lemma multiple_bibd: "n > 0 ==> bibd V (multiple_blocks n) k (Λ * n)"
  using multiple_t_design by (simp add: bibd_def)  

end 

locale two_bibd_eq_points = two_t_designs_eq_points V B k B' 2 Λ Λ'
  + des1: bibd V B k Λ + des2: bibd V B' k Λ' for V B k B' Λ Λ'
begin

lemma combine_is_bibd: "bibd V⁺ B⁺ k (Λ + Λ')"
  by (unfold_locales)

sublocale combine_bibd: bibd "V⁺" "B⁺" "k" "(Λ + Λ')"
  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
  that block with other blocks as it's block set›

locale bibd_block_transformations = bibd + 
  fixes block :: "'a set" (‹bl›)
  assumes valid_block: "bl ∈# B"
begin

definition derived_blocks :: "'a set multiset" (‹(B^D)›) where 
"B^D ≡ {# bl ∩ b . b ∈# (B - {#bl#}) #}"

lemma derive_define_flip: "{# b ∩ bl . b ∈# (B - {#bl#}) #} = B^D"
  by (simp add: derived_blocks_def inf_sup_aci(1))

lemma derived_points_order: "card bl = k"
  using uniform valid_block by simp

lemma derived_block_num: "bl ∈# B ==> size B^D = b - 1"
  by (simp add: derived_blocks_def size_remove1_mset_If valid_block)

lemma derived_is_wellformed:  "b ∈# B^D ==> b ⊆ bl"
  by (simp add: derived_blocks_def valid_block) (auto)

lemma derived_point_subset_orig: "ps ⊆ bl ==> ps ⊂ V"
  by (simp add: valid_block incomplete_imp_proper_subset subset_psubset_trans) 

lemma derived_obtain_orig_block: 
  assumes "b ∈# B^D"
  obtains b2 where "b = b2 ∩ bl" and "b2 ∈# remove1_mset bl B"
  using assms derived_blocks_def by auto

sublocale derived_incidence_sys: incidence_system "bl" "B^D"
  using derived_is_wellformed valid_block by (unfold_locales) (auto)

sublocale derived_fin_incidence_system: finite_incidence_system "bl" "B^D"
  using valid_block finite_blocks by (unfold_locales) simp_all

lemma derived_blocks_nempty:
  assumes "∧ b .b ∈# remove1_mset bl B ==> bl |∩| b > 0"
  assumes "bld ∈# B^D"
  shows "bld ≠ {}"
proof -
  obtain bl2 where inter: "bld = bl2 ∩ bl" and member: "bl2 ∈# remove1_mset bl B" 
    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 B ==> bl |∩| b > 0"
  shows "design bl B^D"
proof -
  interpret fin: finite_incidence_system "bl" "B^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 B ==> bl |∩| b > 0"
  shows "proper_design bl B^D"
proof -
  interpret des: design "bl" "B^D" 
    using derived_is_design assms by fastforce 
  have "b - 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
  set, and the complement of all other blocks with respect to bl.›

definition residual_blocks :: "'a set multiset" (‹(B^R)›) where
"B^R ≡ {# b - bl . b ∈# (B - {#bl#}) #}" 

lemma residual_order: "card (bl^c) = v - k" 
  by (simp add: valid_block wellformed block_complement_size)

lemma residual_block_num: "size (B^R) = b - 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 ∈# B^R"
  obtains bl2 where "b = bl2 - bl" and "bl2 ∈# remove1_mset bl B"
  using assms residual_blocks_def by auto

lemma residual_blocks_ss: assumes "b ∈# B^R" shows "b ⊆ V"
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 ∈# B^R ==> x ∈ b ==> x ∉ bl"
  using residual_obtain_orig_block by auto

lemma residual_is_wellformed:  "b ∈# 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" "B^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" "B^R"
  using residual_is_finite by (unfold_locales) 

lemma residual_blocks_nempty:
  assumes "bld ∈# B^R"
  assumes "multiplicity bl = 1" 
  shows "bld ≠ {}"
proof -
  obtain bl2 where inter: "bld = bl2 - bl" and member: "bl2 ∈# remove1_mset bl B" 
    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) B^R"
  using residual_blocks_nempty by (unfold_locales)

lemma residual_is_proper: 
  assumes "multiplicity bl = 1" 
  shows "proper_design (bl^c) B^R"
proof -
  interpret des: design "bl^c" "B^R" using residual_is_design assms by blast 
  have "b - 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: "b = v"
begin

lemma rep_value_sym: "r = k"
  using b_non_zero local.symmetric necessary_condition_two by auto

lemma symmetric_condition_2: "Λ * (v - 1) = k * (k - 1)"
  using necessary_condition_one rep_value_sym by auto

lemma sym_design_vk_gt_kl: 
  assumes "k ≥ Λ + 2"
  shows "v - k > k - Λ"
proof (rule ccontr)
  define k l v where kdef: "k ≡ int k" and ldef: "l ≡ int Λ" and vdef: "v ≡ int v"
  assume "¬ (v - k > k - Λ)"
  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"
    by (simp add: mult_ac right_diff_distrib' power2_eq_square)
  then have "(k - l)*(k - l - 1) ≤ 0"
    by (simp add: mult_ac right_diff_distrib' power2_eq_square)
  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: "b = v ==> symmetric_bibd V B k Λ"
  by unfold_locales simp

lemma symmetric_bibdII: "Λ * (v - 1) = k * (k - 1) ==> symmetric_bibd V B k Λ"
  using symmetric_condition_1 by unfold_locales blast 

lemma symmetric_not_admissable: "Λ * (v - 1) ≠ k * (k - 1) ==> ¬ symmetric_bibd V B k Λ"
  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
  intersection numbers and the design index. This is an intuitive counting proof, and involved
  more work in a formal environment. Based of Lecture Note cite‹"HerkeLectureNotes2016"››

lemma intersect_mult_set_eq_block:
  assumes "blv ∈# B"
  shows "p ∈# ∑_#{# mset_set (bl ∩ blv) .bl ∈# (B - {#blv#})#} ⟷ p ∈ blv"
proof (auto, simp add: assms finite_blocks)
  assume assm: "p ∈ blv"
  then have "(B - {#blv#}) rep p > 0" using bibd_point_occ_rep r_ge_two assms by auto 
  then obtain bl where "bl ∈# (B - {#blv#}) ∧ p ∈ bl" using assms rep_number_g0_exists by metis
  then show "∃x∈#remove1_mset blv B. p ∈# mset_set (x ∩ blv)" 
    using assms assm finite_blocks by auto 
qed

lemma intersect_mult_set_block_subset_iff:
  assumes "blv ∈# B"
  assumes "p ∈# ∑_#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (B - {#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 ∈#(B - {#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 ∈# B"
  assumes "p ∈# ∑_#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (B - {#blv#})#}"
  shows "card p = 2"
proof -
  obtain b2 where "p ∈# mset_set {y . y ⊆ blv ∩ b2 ∧ card y = 2} ∧ b2 ∈#(B - {#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 ∈# B" and  "p ⊆ blv" and "Λ ≥ 2" and "card p = 2"
  shows "∃x∈#remove1_mset blv B. p ∈# mset_set {y. y ⊆ blv ∧ y ⊆ x ∧ card y = 2}"
proof -
  have "size {#b ∈# B . p ⊆ b#} = Λ" using points_index_def assms 
    by (metis balanced_alt_def_all dual_order.trans wellformed) 
  then have "size {#bl ∈# (B - {#blv#}) . p ⊆ bl#} ≥ 1"  
    using assms by (simp add: size_Diff_singleton)
  then obtain bl where "bl ∈# (B - {#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 ∈# B" and  "p ⊆ blv" and "Λ ≥ 2" and "card p = 2"
  shows "p ∈# ∑_#{# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} .b2 ∈# (B - {#blv#})#}"
  by (auto simp add: intersect_mult_set_block_with_point_exists assms)

lemma sym_sum_mset_inter_sets_count: 
  assumes "blv ∈# B"
  assumes "p ∈ blv"
  shows "count (∑_#{# mset_set (bl ∩ blv) .bl ∈# (B - {#blv#})#}) p = r - 1" 
    (is "count (∑_#?M) p = r - 1")
proof -
  have size_inter: "size {# mset_set (bl ∩ blv) | bl ∈# (B - {#blv#}) . p ∈ bl#} = r - 1"
    using bibd_point_occ_rep point_replication_number_def
    by (metis assms(1) assms(2) size_image_mset)  
  have inter_finite: "∀ bl ∈# (B - {#blv#}) . finite (bl ∩ blv)"
    by (simp add: assms(1) finite_blocks)
  have "∧ bl . bl ∈# (B - {#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 ∈#(B - {#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 ∈# (B - {#blv#}) . p ∈ bl#}
      ==> count P p = 1" by blast
  have "?M = {# mset_set (bl ∩ blv) | bl ∈# (B - {#blv#}) . p ∈ bl#}
      + {# mset_set (bl ∩ blv) | bl ∈# (B - {#blv#}) . p ∉ bl#}"
    by (metis image_mset_union multiset_partition) 
  then have "count (∑_#?M) p = size {# mset_set (bl ∩ blv) | bl ∈# (B - {#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 ∈# B"
  shows "size (∑_#{# mset_set (bl ∩ blv) .bl ∈# (B - {#blv#})#}) = k * (r - 1)" 
    (is "size (∑_#?M) = k* (r - 1)")
proof - 
  have eq: "set_mset (∑_#{# mset_set (bl ∩ blv) .bl ∈# (B - {#blv#})#}) = blv" 
    using intersect_mult_set_eq_block assms by auto
  then have k: "card (set_mset (∑_#?M)) = k"
    by (simp add: assms)
  have "∧ p. p ∈# (∑_#?M) ==> count (∑_#?M) p = r - 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 ∈# B" 
  shows "(∑b2 ∈#(B - {#b1#}). b1 |∩| b2) = k* (r - 1)"
proof -
  have "(∑b2 ∈#(B - {#b1#}). b1 |∩| b2) = (∑b2 ∈#(B - {#b1#}). size (mset_set (b1 ∩ b2)))" 
    by (simp add: intersection_number_def)
  also have "... = size (∑_#{#mset_set (b1 ∩ bl). bl ∈# (B - {#b1#})#})"
    by (auto simp add: size_big_union_sum) 
  also have "... = size (∑_#{#mset_set (bl ∩ b1). bl ∈# (B - {#b1#})#})"
    by (metis Int_commute) 
  finally have "(∑b2 ∈#(B - {#b1#}). b1 |∩| b2) = k * (r - 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 ∈# B"
  assumes "p ⊆ blv"
  assumes "card p = 2"
  shows "count (∑_#{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (B - {#blv#})#}) p = Λ - 1" 
    (is "count (∑_#?M) p = Λ - 1")
proof -
  have size_inter: "size {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (B - {#blv#}) . p ⊆ b2#}
      = Λ - 1"
    using bibd_subset_occ assms by simp
  have "∀ b2 ∈# (B - {#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 ∈#(B - {#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 ∈# (B - {#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 ∈# (B - {#blv#}) . p ⊆ b2#} +
              {# mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2} | b2 ∈# (B - {#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 ∈# (B - {#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 ∈# B"
  shows "size (∑_#{#mset_set {y .y ⊆ blv ∩ b2 ∧ card y = 2}. b2 ∈# (B - {#blv#})#}) =
    ( k choose 2) * (Λ -1)" 
    (is "size (∑_#?M) = (k choose 2) * (Λ -1)")
proof (cases "Λ = 1")
  case True
  have empty: "∧ b2 . b2 ∈# remove1_mset blv B ==> {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 ∈#(B - {#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 = k" using uniform assms by simp
  then have k: "card (set_mset (∑_#?M)) = (k 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 ∈# B" 
  shows "(∑b2 ∈# (B - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1) div 2)) * (v -1)"
proof - 
  have div_fact: "2 dvd (Λ * (Λ - 1))"
    by fastforce 
  have div_fact_2: "2 dvd (Λ * (v - 1))" using symmetric_condition_2 by fastforce
  have "(∑b2 ∈# (B - {#b1#}). ((b1 |∩| b2) choose 2)) = (∑b2 ∈# (B - {#b1#}). (b1 |∩|₂ b2 ))" 
    using n_inter_num_choose_design_inter assms by (simp add: in_diffD)
  then have sum_fact: "(∑b2 ∈# (B - {#b1#}).((b1 |∩| b2) choose 2))
      = (k 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 "(k choose 2) * (Λ -1) = ((Λ * (v - 1) div 2)) * (Λ -1)" 
    using choose_two symmetric_condition_2 k_non_zero by auto
  also have "… = ((Λ * (Λ - 1) div 2)) * (v - 1)"
    using div_fact div_fact_2
    by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) dvd_div_mult mult.commute)
  finally have "(k choose 2) * (Λ -1) = ((Λ * (Λ - 1) div 2)) * (v -1)" .
  then show ?thesis using sum_fact by simp
qed

lemma sym_sum_inter_num_sq: 
  assumes "b1 ∈# B" 
  shows "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2) = Λ^2 * ( v - 1)"
proof - 
  have dvd: "2 dvd (( v - 1) * (Λ * (Λ - 1)))" by fastforce
  have inner_dvd: "∀ bl ∈# (remove1_mset b1 B). 2 dvd ((b1 |∩| bl) * ((b1 |∩| bl) - 1))"
    by force
  have diff_le: "∧ bl . bl ∈# (remove1_mset b1 B) ==> (b1 |∩| bl) ≤ (b1 |∩| bl)^2"
    by (simp add: power2_nat_le_imp_le)
  have a: "(∑b2 ∈#(B - {#b1#}). ((b1 |∩| b2) choose 2)) =
            (∑bl ∈# (remove1_mset b1 B). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2)" 
    using choose_two by (simp add: intersection_num_non_neg)
  have b: "(∑b2 ∈#(B - {#b1#}). ((b1 |∩| b2) choose 2)) =
              (∑b2 ∈#(B - {#b1#}). ((b1 |∩| b2) choose 2))" by simp
  have gtsq: "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2) ≥ (∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl))"
    by (simp add: diff_le sum_mset_mono) 
  have "(∑b2 ∈#(B - {#b1#}). ((b1 |∩| b2) choose 2)) = ((Λ * (Λ - 1)) div 2) * ( v - 1)" 
    using sum_choose_two_inter_num assms by blast 
  then have start: "(∑bl ∈# (remove1_mset b1 B). ((b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2)
                        = ((Λ * (Λ - 1)) div 2) * (v - 1)"
    using a b by linarith
  have sum_dvd: "2 dvd (∑bl ∈# (remove1_mset b1 B). (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 B). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2
      = ((Λ * (Λ - 1)) div 2) * (v - 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 B). (b1 |∩| bl) * ((b1 |∩| bl) - 1)) div 2
      = (v - 1) * ((Λ * (Λ - 1)) div 2)"
    by simp 
  then have "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl) * ((b1 |∩| bl) - 1))
      = (v - 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 B). (b1 |∩| bl)^2 - (b1 |∩| bl))
      = (v - 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 B). (b1 |∩| bl)^2)
      - (∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)) = (v - 1) * (Λ * (Λ - 1))"
    using sum_mset_add_diff_nat[of "(remove1_mset b1 B)" "λ bl . (b1 |∩| bl)" "λ bl . (b1 |∩| bl)^2"]  
      diff_le by presburger  
  then have "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2)
      = (∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)) + (v - 1) * (Λ * (Λ - 1))" using gtsq
    by (metis le_add_diff_inverse) 
  then have "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2) = (Λ * (v - 1)) + ((v - 1) * (Λ * (Λ - 1)))" 
    using sym_sum_inter_num assms rep_value_sym symmetric_condition_2 by auto 
  then have prev: "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2) = (Λ * (v - 1)) * (Λ - 1) + (Λ * (v - 1))"
    by fastforce 
  then have "(∑bl ∈# (remove1_mset b1 B). (b1 |∩| bl)^2) = (Λ * (v - 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 B). (b1 |∩| bl)^2) = Λ * Λ * (v - 1)"
    using mult.commute by simp 
  thus ?thesis by (simp add: power2_eq_square)
qed

lemma sym_sum_inter_num_to_zero: 
  assumes "b1 ∈# B" 
  shows "(∑bl ∈# (remove1_mset b1 B). (int (b1 |∩| bl) - (int Λ))^2) = 0"
proof -
  have rm1_size: "size (remove1_mset b1 B) = v - 1" using assms b_non_zero int_ops(6) 
    by (auto simp add: symmetric size_remove1_mset_If)
  have  "(∑bl ∈# (remove1_mset b1 B). ((int (b1 |∩| bl))^2)) =
    (∑bl ∈# (remove1_mset b1 B). (((b1 |∩| bl))^2))" by simp
  then have ssi: "(∑bl ∈# (remove1_mset b1 B). ((int (b1 |∩| bl))^2)) = Λ^2 * (v - 1)" 
    using sym_sum_inter_num_sq assms by simp 
  have "∧ bl . bl ∈# (remove1_mset b1 B) ==> (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 B). (int (b1 |∩| bl) - (int Λ))^2) =
              (∑bl ∈# (remove1_mset b1 B). (((int (b1 |∩| bl))^2) - (2 * (int Λ) * (int (b1 |∩| bl))) + ((int Λ)^2)))"
    using sum_over_fun_eq by auto
  also have "... = (∑bl ∈# (remove1_mset b1 B). (((int (b1 |∩| bl))^2)
      - (2 * (int Λ) * (int (b1 |∩| bl))))) + (∑ bl ∈# (remove1_mset b1 B) . ((int Λ)^2))" 
    by (simp add: sum_mset.distrib) 
  also have "... = (∑bl ∈# (remove1_mset b1 B). ((int (b1 |∩| bl))^2))
      - (∑bl ∈# (remove1_mset b1 B). (2 * (int Λ) * (int (b1 |∩| bl)))) + (∑ bl ∈# (remove1_mset b1 B) . ((int Λ)^2))" 
    using sum_mset_add_diff_int[of "(λ bl . ((int (b1 |∩| bl))^2))" "(λ bl . (2 * (int Λ) * (int (b1 |∩| bl))))" "(remove1_mset b1 B)"] 
    by simp
  also have "... = Λ^2 * (v - 1) - 2 * (int Λ) *(∑bl ∈# (remove1_mset b1 B). ((b1 |∩| bl)))
      + (v - 1) * ((int Λ)^2)" using ssi rm1_size assms by (simp add: sum_mset_distrib_left)
  also have "... = 2 * Λ^2 * (v - 1) - 2 * (int Λ) *(k* (r - 1))" 
    using  sym_sum_inter_num assms by simp
  also have "... = 2 * Λ^2 * (v - 1) - 2 * (int Λ) * (Λ * (v - 1))" 
    using rep_value_sym symmetric_condition_2 by simp
  finally have "(∑bl ∈# (remove1_mset b1 B). (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 ∈# B"
  assumes "b2 ∈# (B - {#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 B). (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 B) ==> (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 B) ==> 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 ∈# B"
  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 ∈# (B - {#bl#})"
    using in_diff_count by fastforce
  have "bl |∩| bl = k" using k_non_zero assms
    by (simp add: intersection_number_def) 
  then have keql: "k = Λ" using sym_block_intersections_index blleft assms by simp
  then have "v = k"
    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.
  based off lecture notes cite‹"HerkeLectureNotes2016"››

locale symmetric_bibd_block_transformations = symmetric_bibd + bibd_block_transformations
begin 

lemma derived_block_size [simp]: 
  assumes "b ∈# B^D"
  shows "card b = Λ"
proof -
  obtain bl2 where set: "bl2 ∈# remove1_mset bl B" 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 "B^D index ps = Λ - 1"
proof -
  have b_in: "∧ b . b ∈# (remove1_mset bl B) ==> ps ⊆ b ==> ps ⊆ b ∩ bl"
    using assms by blast 
  then have orig: "ps ⊆ V"
    using valid_block assms wellformed by blast
  then have lam: "size {# b ∈# B . ps ⊆ b #} = Λ" using balanced
    by (simp add: assms(2)  points_index_def) 
  then have "size {# b ∈# remove1_mset bl B . ps ⊆ b #} = size {# b ∈# B . ps ⊆ b #} - 1"
    using assms valid_block by (simp add: size_Diff_submset)
  then have "size {# b ∈# remove1_mset bl B . ps ⊆ b #} = Λ - 1" 
    using lam index_not_zero by linarith 
  then have "size {# bl ∩ b | b ∈# (remove1_mset bl B) . 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 B) #} . ps ⊆ x #} = Λ - 1"
    by (metis image_mset_filter_swap) 
  then have "size {# x ∈# B^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 B^D Λ (Λ - 1)"
proof -
  interpret des: proper_design bl "B^D" using derived_is_proper assms valid_block by auto 
  have "Λ < k" 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 ∈# B^R"
  shows "card b = k - Λ"
proof -
  obtain bl2 where sub: "b = bl2 - bl" and mem: "bl2 ∈# remove1_mset bl B" 
    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  "(B^R) index ps = Λ"
proof - 
  have a: "∧ b . (b ∈# remove1_mset bl B ==> ps ⊆ b ==> ps ⊆ (b - bl))" using assms
    by (meson DiffI block_complement_elem_iff block_complement_subset_points subsetD subsetI)
  have b: "∧ b . (b ∈# remove1_mset bl B ==> 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 "B^R index ps = size {# x ∈# {# b - bl . b ∈# (remove1_mset bl B) #} . ps ⊆ x #}" 
    using assms valid_block by (simp add: points_index_def residual_blocks_def)
  also have "... = size {# b - bl | b ∈# (remove1_mset bl B) . ps ⊆ b - bl #} "
    by (metis image_mset_filter_swap)
  finally have "B^R index ps = size {# b ∈# (remove1_mset bl B) . 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 "k ≥ Λ + 2"
  shows "bibd (bl^c) B^R (k - Λ) Λ"
proof -
  interpret des: proper_design "bl^c" "B^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 V B Λ k
  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 V B k"
proof -
  interpret pbd: k_Λ_PBD V B Λ k
    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