Theory Fishers_Inequality.Design_Extras

(* Title: Design Extras.thy
   Author: Chelsea Edmonds
*)

section ‹ Micellaneous Design Extras ›

text ‹Extension's to the author's previous entry on Design Theory ›

theory Design_Extras imports Set_Multiset_Extras Design_Theory.BIBD
begin

subsection ‹Extensions to existing Locales and Properties ›

text ‹Extend lemmas on intersection number›
lemma inter_num_max_bound: 
  assumes "finite b1" "finite b2"
  shows "b1 |∩| b2 ≤ card b1" "b1 |∩| b2 ≤ card b2"
  by(simp_all add: assms intersection_number_def card_mono)

lemma inter_eq_blocks_eq_card: "card b1 = card b2 ⟹ finite b1 ⟹ finite b2 ⟹ b1 |∩| b2 = card b1 
    ⟹ b1 = b2"
  using equal_card_inter_fin_eq_sets intersection_number_def by (metis) 

lemma inter_num_of_eq_blocks: "b1 = b2 ⟹ b1 |∩| b2 = card b1"
  by (simp add: intersection_number_def)

lemma intersect_num_same_eq_size[simp]: "bl |∩| bl = card bl"
  by (simp add: intersection_number_def)

lemma index_lt_rep_general: "x ∈ ps ⟹ B index ps ≤ B rep x"
  by (simp add: points_index_def point_replication_number_def) 
    (metis filter_filter_mset_cond_simp size_filter_mset_lesseq subset_iff)

context incidence_system 
begin

lemma block_size_alt:
  assumes "bl ∈# ℬ"
  shows "card bl = card {x ∈ 𝒱 . x ∈ bl}" 
proof -
  have "⋀ x. x ∈ bl ⟹ x ∈ 𝒱" using wellformed assms by auto
  thus ?thesis
    by (metis (no_types, lifting) Collect_cong Collect_mem_eq) 
qed

lemma complement_image: "ℬ⇧C = image_mset block_complement ℬ"
  by (simp add: complement_blocks_def)

lemma point_in_block_rep_min_iff:
  assumes "x ∈ 𝒱" 
  shows "∃ bl . bl ∈# ℬ ∧ x ∈ bl ⟷ (ℬ rep x > 0)"
  using rep_number_g0_exists
  by (metis block_complement_elem_iff block_complement_inv wellformed)

lemma points_inter_num_rep: 
  assumes "b1 ∈# ℬ" and "b2 ∈# ℬ - {#b1#}"
  shows "card {v ∈ 𝒱 . v ∈ b1 ∧ v ∈ b2} = b1 |∩| b2"
proof -
  have "⋀ x. x ∈ b1 ∩ b2 ⟹ x ∈ 𝒱" using wellformed assms by auto
  then have "{v ∈ 𝒱 . v ∈ (b1 ∩ b2)} = (b1 ∩ b2)"
    by blast 
  then have "card {v ∈ 𝒱 . v ∈ b1 ∧ v ∈ b2} = card (b1 ∩ b2)"
    by simp 
  thus ?thesis using assms intersection_number_def by metis 
qed

text ‹Extensions on design operation lemmas ›
lemma del_block_b: 
  "bl ∈# ℬ ⟹ size (del_block bl) = 𝖻 - 1"
  "bl ∉# ℬ ⟹ size (del_block bl) = 𝖻"
  by (simp_all add: del_block_def size_Diff_singleton)

lemma del_block_points_index: 
  assumes "ps ⊆ 𝒱"
  assumes "card ps = 2"
  assumes "bl ∈# ℬ"
  shows "ps ⊆ bl ⟹ points_index (del_block bl) ps = points_index ℬ ps - 1"
        "¬ (ps ⊆ bl) ⟹ points_index (del_block bl) ps = points_index ℬ ps"
proof -
  assume "ps ⊆ bl"
  then show "points_index (del_block bl) ps = points_index ℬ ps - 1"
    using point_index_diff del_block_def
    by (metis assms(3) insert_DiffM2 points_index_singleton) 
next
  assume "¬ ps ⊆ bl"
  then show "del_block bl index ps = ℬ index ps"
    using point_index_diff del_block_def
    by (metis add_block_def add_block_index_not_in assms(3) insert_DiffM2) 
qed

end

text ‹Extensions to properties of design sub types ›

context finite_incidence_system
begin

lemma complete_block_size_eq_points: "bl ∈# ℬ ⟹ card bl = 𝗏 ⟹ bl = 𝒱"
  using wellformed by (simp add:  card_subset_eq finite_sets) 

lemma complete_block_all_subsets: "bl ∈# ℬ ⟹ card bl = 𝗏 ⟹ ps ⊆ 𝒱 ⟹ ps ⊆ bl"
  using complete_block_size_eq_points by auto

lemma del_block_complete_points_index: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ bl ∈# ℬ ⟹ card bl = 𝗏 ⟹ 
  points_index (del_block bl) ps = points_index ℬ ps - 1"
  using complete_block_size_eq_points del_block_points_index(1) by blast

end

context design
begin

lemma block_num_rep_bound: "𝖻 ≤ (∑ x ∈ 𝒱. ℬ rep x)"
proof -
  have exists: "⋀ bl. bl ∈# ℬ ⟹ (∃ x ∈ 𝒱 . bl ∈# {#b ∈# ℬ. x ∈ b#})" using wellformed
    using blocks_nempty by fastforce 
  then have bss: "ℬ ⊆# ∑⇩# (image_mset (λ v. {#b ∈# ℬ. v ∈ b#}) (mset_set 𝒱))"
  proof (intro  mset_subset_eqI)
    fix bl
    show "count ℬ bl ≤ count (∑v∈#mset_set 𝒱. filter_mset ((∈) v) ℬ) bl"
    proof (cases "bl ∈# ℬ")
      case True
      then obtain x where xin: "x ∈ 𝒱" and blin: "bl ∈# filter_mset ((∈) x) ℬ" using exists by auto
      then have eq: "count ℬ bl = count (filter_mset ((∈) x) ℬ) bl" by simp 
      have "(∑v∈#mset_set 𝒱. filter_mset ((∈) v) ℬ) = (filter_mset ((∈) x) ℬ) + 
        (∑v∈#(mset_set 𝒱) - {#x#}. filter_mset ((∈) v) ℬ)"
        using xin by (simp add: finite_sets mset_set.remove) 
      then have "count (∑v∈#mset_set 𝒱. filter_mset ((∈) v) ℬ) bl = count (filter_mset ((∈) x) ℬ) bl 
        +  count (∑v∈#(mset_set 𝒱) - {#x#}. filter_mset ((∈) v) ℬ) bl"
        by simp
      then show ?thesis using eq by linarith 
    next
      case False
      then show ?thesis by (metis count_eq_zero_iff le0)
    qed
  qed
  have "(∑ x ∈ 𝒱. ℬ rep x) = (∑ x ∈ 𝒱. size ({#b ∈# ℬ. x ∈ b#}))" 
    by (simp add: point_replication_number_def)
  also have "... = (∑ x ∈# (mset_set 𝒱). size ({#b ∈# ℬ. x ∈ b#}))"
    by (simp add: sum_unfold_sum_mset) 
  also have "... = (∑ x ∈# (image_mset (λ v. {#b ∈# ℬ. v ∈ b#}) (mset_set 𝒱)) . size x)"
    by auto  
  finally have "(∑ x ∈ 𝒱. ℬ rep x) = size (∑⇩# (image_mset (λ v. {#b ∈# ℬ. v ∈ b#}) (mset_set 𝒱)))" 
    using size_big_union_sum by metis 
  then show ?thesis using bss
    by (simp add: size_mset_mono)
qed

end

context proper_design
begin

lemma del_block_proper: 
  assumes "𝖻 > 1"
  shows "proper_design 𝒱 (del_block bl)"
proof -
  interpret d: design 𝒱 "(del_block bl)"
    using delete_block_design by simp
  have "d.𝖻 > 0" using del_block_b assms
    by (metis b_positive zero_less_diff) 
  then show ?thesis by(unfold_locales) (auto)
qed

end

context simple_design 
begin

lemma inter_num_lt_block_size_strict: 
  assumes "bl1 ∈# ℬ"
  assumes "bl2 ∈# ℬ"
  assumes "bl1 ≠ bl2"
  assumes "card bl1 = card bl2"
  shows "bl1 |∩| bl2 < card bl1" "bl1 |∩| bl2 < card bl2"
proof -
  have lt: "bl1 |∩| bl2 ≤ card bl1" using finite_blocks
    by (simp add: ‹bl1 ∈# ℬ› ‹bl2 ∈# ℬ› inter_num_max_bound(1)) 
  have ne: "bl1 |∩| bl2 ≠ card bl1" 
  proof (rule ccontr, simp)
    assume "bl1 |∩| bl2 = card bl1"
    then have "bl1 = bl2" using assms(4) inter_eq_blocks_eq_card assms(1) assms(2) finite_blocks 
      by blast 
    then show False using assms(3) by simp
  qed
  then show "bl1 |∩| bl2 < card bl1" using lt by simp
  have "bl1 |∩| bl2 ≠ card bl2" using ne by (simp add: assms(4)) 
  then show "bl1 |∩| bl2 < card bl2" using lt assms(4) by simp
qed

lemma block_mset_distinct: "distinct_mset ℬ" using simple
  by (simp add: distinct_mset_def) 

end

context constant_rep_design 
begin

lemma index_lt_const_rep: 
  assumes "ps ⊆ 𝒱"
  assumes "ps ≠ {}"
  shows "ℬ index ps ≤ 𝗋"
proof -
  obtain x where xin: "x ∈ ps" using assms by auto
  then have "ℬ rep x = 𝗋"
    by (meson assms(1) in_mono rep_number_alt_def_all) 
  thus ?thesis using index_lt_rep_general xin by auto
qed

end

context t_wise_balance
begin

lemma  obtain_t_subset_with_point: 
  assumes "x ∈ 𝒱"
  obtains ps where "ps ⊆ 𝒱" and "card ps = 𝗍" and "x ∈ ps"
proof (cases "𝗍 = 1")
  case True
  have "{x} ⊆ 𝒱" "card {x} = 1" "x ∈ {x}"
    using assms by simp_all
  then show ?thesis
    using True that by blast 
next
  case False
  have "𝗍 - 1 ≤ card (𝒱 - {x})"
    by (simp add: assms diff_le_mono finite_sets t_lt_order) 
  then obtain ps' where psss: "ps' ⊆ (𝒱 - {x})" and psc: "card ps' = 𝗍 - 1" 
    by (meson obtain_subset_with_card_n)
  then have xs: "(insert x ps') ⊆ 𝒱"
    using assms by blast 
  have xnotin: "x ∉ ps'" using psss
    by blast 
  then have "card (insert x ps') = Suc (card ps')"
    by (meson ‹insert x ps' ⊆ 𝒱› finite_insert card_insert_disjoint finite_sets finite_subset) 
  then have "card (insert x ps') = card ps' + 1"
    by presburger 
  then have xc: "card (insert x ps') = 𝗍" using psc
    using add.commute add_diff_inverse t_non_zero by linarith 
  have "x ∈ (insert x ps')" by simp
  then show ?thesis using xs xc that by blast 
qed

lemma const_index_lt_rep: 
  assumes "x ∈ 𝒱"
  shows "Λ⇩t ≤ ℬ rep x"
proof -
  obtain ps where psin: "ps ⊆ 𝒱" and "card ps = 𝗍" and xin: "x ∈ ps" 
    using assms t_lt_order obtain_t_subset_with_point by auto
  then have "ℬ index ps = Λ⇩t " using balanced by simp
  thus ?thesis using index_lt_rep_general xin 
    by (meson) 
qed

end

context pairwise_balance
begin

lemma index_zero_iff: "Λ = 0 ⟷ (∀ bl ∈# ℬ . card bl = 1)"
proof (auto)
  fix bl assume l0: "Λ = 0" assume blin: "bl ∈# ℬ"
  have "card bl = 1"
  proof (rule ccontr)
    assume "card bl ≠ 1"
    then have "card bl ≥ 2" using block_size_gt_0
      by (metis Suc_1 Suc_leI blin less_one nat_neq_iff) 
    then obtain ps where psss: "ps ⊆ bl" and pscard: "card ps = 2"
      by (meson obtain_subset_with_card_n)
    then have psin: "ℬ index ps ≥ 1"
      using blin points_index_count_min by auto
    have "ps ⊆ 𝒱" using wellformed psss blin by auto
    then show False using balanced l0 psin pscard by auto
  qed
  thus "card bl = (Suc 0)" by simp
next
  assume a: "∀bl∈#ℬ. card bl = Suc 0"
  obtain ps where psss: "ps ⊆ 𝒱" and ps2: "card ps = 2"
    by (meson obtain_t_subset_points) 
  then have "⋀ bl. bl ∈# ℬ ⟹ (card ps > card bl)" using a
    by simp 
  then have cond: "⋀ bl. bl ∈# ℬ ⟹ ¬( ps ⊆  bl)"
    by (metis card_mono finite_blocks le_antisym less_imp_le_nat less_not_refl3) 
  have "ℬ index ps = size {# bl ∈# ℬ . ps ⊆ bl #}" by (simp add:points_index_def)
  then have "ℬ index ps = size {#}" using cond
    by (metis points_index_0_iff size_empty) 
  thus "Λ = 0" using psss ps2 balanced by simp
qed

lemma count_complete_lt_balance: "count ℬ 𝒱 ≤ Λ"
proof (rule ccontr)
  assume a: "¬ count ℬ 𝒱 ≤ Λ"
  then have assm: "count ℬ 𝒱 > Λ"
    by simp
  then have gt: "size {# bl ∈# ℬ . bl = 𝒱#} > Λ"
    by (simp add: count_size_set_repr) 
  obtain ps where psss: "ps ⊆ 𝒱" and pscard: "card ps = 2" using t_lt_order
    by (meson obtain_t_subset_points) 
  then have "{# bl ∈# ℬ . bl = 𝒱#} ⊆# {# bl ∈# ℬ . ps ⊆ bl #}"
    by (metis a balanced le_refl points_index_count_min) 
  then have "size {# bl ∈# ℬ . bl = 𝒱#} ≤ ℬ index ps " 
    using points_index_def[of ℬ ps] size_mset_mono by simp
  thus False using pscard psss balanced gt by auto
qed

lemma eq_index_rep_imp_complete: 
  assumes "Λ = ℬ rep x"
  assumes "x ∈ 𝒱"
  assumes "bl ∈# ℬ"
  assumes "x ∈ bl"
  shows "card bl = 𝗏"
proof -
  have "⋀ y. y ∈ 𝒱 ⟹ y ≠ x ⟹ card {x, y} = 2 ∧ {x, y} ⊆ 𝒱" using assms by simp
  then have size_eq: "⋀ y. y ∈ 𝒱 ⟹ y ≠ x ⟹ size {# b ∈# ℬ . {x, y} ⊆ b#} = size {# b ∈# ℬ . x ∈ b#}"
    using point_replication_number_def balanced points_index_def assms by metis 
  have "⋀ y b. y ∈ 𝒱 ⟹ y ≠ x ⟹ b ∈# ℬ ⟹ {x, y} ⊆ b ⟶ x ∈ b" by simp
  then have "⋀ y. y ∈ 𝒱 ⟹ y ≠ x ⟹ {# b ∈# ℬ . {x, y} ⊆ b#} ⊆# {# b ∈# ℬ . x ∈ b#}" 
    using multiset_filter_mono2 assms by auto
  then have eq_sets: "⋀ y. y ∈ 𝒱 ⟹ y ≠ x ⟹ {# b ∈# ℬ . {x, y} ⊆ b#} = {# b ∈# ℬ . x ∈ b#}" 
    using size_eq by (smt (z3) Diff_eq_empty_iff_mset cancel_comm_monoid_add_class.diff_cancel 
        size_Diff_submset size_empty size_eq_0_iff_empty subset_mset.antisym) 
  have "bl ∈# {# b ∈# ℬ . x ∈ b#}" using assms by simp
  then have "⋀ y. y ∈ 𝒱 ⟹ y ≠ x ⟹ {x, y} ⊆ bl" using eq_sets
    by (metis (no_types, lifting) Multiset.set_mset_filter mem_Collect_eq) 
  then have "⋀ y. y ∈ 𝒱 ⟹ y ∈ bl" using assms by blast 
  then have "bl = 𝒱" using wellformed assms(3) by blast 
  thus ?thesis by simp
qed

lemma incomplete_index_strict_lt_rep:
  assumes "⋀ bl. bl ∈# ℬ ⟹ incomplete_block bl" 
  assumes "x ∈ 𝒱"
  assumes "Λ > 0"
  shows "Λ < ℬ rep x"
proof (rule ccontr)
  assume "¬ (Λ < ℬ rep x)"
  then have a: "Λ ≥ ℬ rep x"
    by simp
  then have "Λ = ℬ rep x" using const_index_lt_rep
    using assms(2) le_antisym by blast 
  then obtain bl where xin: "x ∈ bl" and blin: "bl ∈# ℬ"
    by (metis assms(3) rep_number_g0_exists) 
  thus False using assms eq_index_rep_imp_complete incomplete_alt_size
    using ‹Λ = ℬ rep x› nat_less_le by blast  
qed

text ‹Construct new PBD's from existing PBD's ›

lemma remove_complete_block_pbd: 
  assumes "𝖻 ≥ 2"
  assumes "bl ∈# ℬ"
  assumes "card bl = 𝗏"
  shows "pairwise_balance 𝒱 (del_block bl) (Λ - 1)"
proof -
  interpret pd: proper_design 𝒱 "(del_block bl)" using assms(1) del_block_proper by simp
  show ?thesis using t_lt_order assms del_block_complete_points_index 
    by (unfold_locales) (simp_all)
qed

lemma remove_complete_block_pbd_alt: 
  assumes "𝖻 ≥ 2"
  assumes "bl ∈# ℬ"
  assumes "bl = 𝒱"
  shows "pairwise_balance 𝒱 (del_block bl) (Λ - 1)"
  using remove_complete_block_pbd assms by blast 

lemma b_gt_index:"𝖻 ≥ Λ"
proof (rule ccontr)
  assume blt: "¬ 𝖻 ≥ Λ"
  obtain ps where "card ps = 2" and "ps ⊆ 𝒱" using t_lt_order
    by (meson obtain_t_subset_points) 
  then have "size {#bl ∈# ℬ. ps ⊆ bl#} = Λ" using balanced by (simp add: points_index_def)
  thus False using blt by auto 
qed

lemma remove_complete_blocks_set_pbd:
  assumes "x < Λ"
  assumes "size A = x"
  assumes "A ⊂# ℬ"
  assumes "⋀ a. a ∈# A ⟹ a = 𝒱"
  shows "pairwise_balance 𝒱 (ℬ - A) (Λ - x)"
using assms proof (induct "x" arbitrary: A)
  case 0
  then have beq: "ℬ - A = ℬ" by simp
  have "pairwise_balance 𝒱 ℬ Λ" by (unfold_locales)
  then show ?case using beq by simp
next
  case (Suc x)
  then have "size A > 0" by simp
  let ?A' = "A - {#𝒱#}"
  have ss: "?A' ⊂# ℬ"
    using Suc.prems(3) by (metis diff_subset_eq_self subset_mset.le_less_trans)
  have sx: "size ?A' = x"
    by (metis Suc.prems(2) Suc.prems(4) Suc_inject size_Suc_Diff1 size_eq_Suc_imp_elem)
  have xlt: "x < Λ"
    by (simp add: Suc.prems(1) Suc_lessD) 
  have av: "⋀ a. a ∈# ?A' ⟹ a = 𝒱" using Suc.prems(4)
    by (meson in_remove1_mset_neq)
  then interpret pbd: pairwise_balance 𝒱 "(ℬ - ?A')" "(Λ - x)" using Suc.hyps sx ss xlt by simp
  have "Suc x < 𝖻" using Suc.prems(3)
    by (metis Suc.prems(2) mset_subset_size) 
  then have "𝖻 - x ≥ 2"
    by linarith 
  then have bgt: "size (ℬ - ?A') ≥ 2" using ss size_Diff_submset
    by (metis subset_msetE sx)
  have ar: "add_mset 𝒱 (remove1_mset 𝒱 A) = A" using Suc.prems(2) Suc.prems(4)
    by (metis insert_DiffM size_eq_Suc_imp_elem) 
  then have db: "pbd.del_block 𝒱 = ℬ - A" by(simp add: pbd.del_block_def)
  then have "ℬ - ?A' = ℬ - A + {#𝒱#}" using Suc.prems(2) Suc.prems(4)
    by (metis (no_types, lifting) Suc.prems(3) ar add_diff_cancel_left' add_mset_add_single add_right_cancel 
        pbd.del_block_def remove_1_mset_id_iff_notin ss subset_mset.lessE trivial_add_mset_remove_iff) 
  then have "𝒱 ∈# (ℬ - ?A')" by simp 
  then have "pairwise_balance 𝒱 (ℬ - A) (Λ - (Suc x))" using db bgt diff_Suc_eq_diff_pred 
      diff_commute pbd.remove_complete_block_pbd_alt by presburger
  then show ?case by simp
qed

lemma remove_all_complete_blocks_pbd:
  assumes "count ℬ 𝒱 < Λ"
  shows "pairwise_balance 𝒱 (removeAll_mset 𝒱 ℬ) (Λ - (count ℬ 𝒱))" (is "pairwise_balance 𝒱 ?B ?Λ")
proof -
  let ?A = "replicate_mset (count ℬ 𝒱) 𝒱"
  let ?x = "size ?A"
  have blt: "count ℬ 𝒱 ≠ 𝖻" using b_gt_index assms
    by linarith 
  have xeq: "?x = count ℬ 𝒱" by simp
  have av: "⋀ a. a ∈# ?A ⟹ a = 𝒱"
    by (metis in_replicate_mset)
  have "?A ⊆# ℬ"
    by (meson count_le_replicate_mset_subset_eq le_eq_less_or_eq)
  then have "?A ⊂# ℬ" using blt
    by (metis subset_mset.nless_le xeq) 
  thus ?thesis using assms av xeq remove_complete_blocks_set_pbd
    by presburger 
qed

end

context bibd
begin
lemma symmetric_bibdIII: "𝗋 = 𝗄 ⟹ symmetric_bibd 𝒱 ℬ 𝗄 Λ"
  using necessary_condition_one symmetric_condition_1 by (unfold_locales) (simp)
end

subsection ‹ New Design Locales ›
text ‹ We establish a number of new locales and link them to the existing locale hierarchy
in order to reason in contexts requiring specific combinations of contexts ›

text ‹Regular t-wise balance ›
locale regular_t_wise_balance = t_wise_balance + constant_rep_design
begin

lemma reg_index_lt_rep: 
  shows "Λ⇩t ≤ 𝗋"
proof -
  obtain ps where psin: "ps ⊆ 𝒱" and pst: "card ps = 𝗍"
    by (metis obtain_t_subset_points) 
  then have ne: "ps ≠ {}" using t_non_zero by auto
  then have "ℬ index ps = Λ⇩t" using balanced pst psin by simp
  thus ?thesis using index_lt_const_rep
    using ne psin by auto 
qed

end

locale regular_pairwise_balance = regular_t_wise_balance 𝒱 ℬ 2 Λ 𝗋 + pairwise_balance 𝒱 ℬ Λ
  for 𝒱 and ℬ and Λ and 𝗋

text ‹ Const Intersect Design ›
text ‹ This is the dual of a balanced design, and used extensively in the remaining formalisation ›

locale const_intersect_design = proper_design + 
  fixes 𝗆 :: nat
  assumes const_intersect: "b1 ∈# ℬ ⟹ b2 ∈# (ℬ - {#b1#}) ⟹ b1 |∩| b2 = 𝗆"

sublocale symmetric_bibd ⊆ const_intersect_design 𝒱 ℬ Λ
  by (unfold_locales) (simp)

context const_intersect_design
begin

lemma inter_num_le_block_size: 
  assumes "bl ∈# ℬ"
  assumes "𝖻 ≥ 2"
  shows "𝗆 ≤ card bl"
proof (rule ccontr)
  assume a: "¬ (𝗆 ≤ card bl)"
  obtain bl' where blin: "bl' ∈# ℬ - {#bl#}"
    using assms by (metis add_mset_add_single diff_add_inverse2 diff_is_0_eq' multiset_nonemptyE 
        nat_1_add_1 remove1_mset_eqE size_single zero_neq_one)
  then have const: "bl |∩| bl' = 𝗆" using const_intersect assms by auto
  thus False using inter_num_max_bound(1) finite_blocks 
    by (metis a blin assms(1) finite_blocks in_diffD) 
qed

lemma const_inter_multiplicity_one: 
  assumes "bl ∈# ℬ"
  assumes "𝗆 < card bl"
  shows "multiplicity bl = 1"
proof (rule ccontr)
  assume "multiplicity bl ≠ 1"
  then have "multiplicity bl > 1" using assms
    by (simp add: le_neq_implies_less)
  then obtain bl2 where "bl = bl2" and "bl2 ∈# ℬ - {#bl#}"
    by (metis count_single in_diff_count)
  then have "bl |∩| bl2 = card bl"
    using inter_num_of_eq_blocks by blast  
  thus False using assms const_intersect
    by (simp add: ‹bl2 ∈# remove1_mset bl ℬ›) 
qed

lemma mult_blocks_const_inter: 
  assumes "bl ∈# ℬ"
  assumes "multiplicity bl > 1"
  assumes "𝖻 ≥ 2"
  shows "𝗆 = card bl"
proof (rule ccontr)
  assume "𝗆 ≠ card bl"
  then have "𝗆 < card bl" using inter_num_le_block_size assms
    using nat_less_le by blast 
  then have "multiplicity bl = 1" using const_inter_multiplicity_one assms by simp
  thus False using assms(2) by simp
qed

lemma simple_const_inter_block_size: "(⋀ bl. bl ∈# ℬ ⟹ 𝗆 < card bl) ⟹ simple_design 𝒱 ℬ"
  using const_inter_multiplicity_one by (unfold_locales) (simp)

lemma simple_const_inter_iff: 
  assumes "𝖻 ≥ 2"
  shows "size {#bl ∈# ℬ . card bl = 𝗆  #} ≤ 1 ⟷ simple_design 𝒱 ℬ"
proof (intro iffI)
  assume a: "size {#bl ∈# ℬ. card bl = 𝗆#} ≤ 1"
  show "simple_design 𝒱 ℬ" 
  proof (unfold_locales)
    fix bl assume blin: "bl ∈# ℬ"
    show "multiplicity bl = 1"
    proof (cases "card bl = 𝗆")
      case True
      then have m: "multiplicity bl = size {#b ∈# ℬ . b = bl#}"
        by (simp add: count_size_set_repr)
      then have "{#b ∈# ℬ . b = bl#} ⊆# {#bl ∈# ℬ. card bl = 𝗆#}" using True
        by (simp add: mset_subset_eqI)
      then have "size {#b ∈# ℬ . b = bl#} ≤ size {#bl ∈# ℬ. card bl = 𝗆#}"
        by (simp add: size_mset_mono) 
      then show ?thesis using a blin
        by (metis count_eq_zero_iff le_neq_implies_less le_trans less_one m) 
    next
      case False
      then have "𝗆 < card bl" using assms
        by (simp add: blin inter_num_le_block_size le_neq_implies_less) 
      then show ?thesis using const_inter_multiplicity_one
        by (simp add: blin) 
    qed
  qed
next
  assume simp: "simple_design 𝒱 ℬ"
  then have mult: "⋀ bl. bl ∈# ℬ ⟹ multiplicity bl = 1"
    using simple_design.axioms(2) simple_incidence_system.simple_alt_def_all by blast 
  show "size {#bl ∈# ℬ . card bl = 𝗆 #} ≤ 1"
  proof (rule ccontr)
    assume "¬ size {#bl ∈# ℬ. card bl = 𝗆#} ≤ 1"
    then have "size {#bl ∈# ℬ . card bl = 𝗆 #} > 1" by simp
    then obtain bl1 bl2 where blin: "bl1 ∈# ℬ" and bl2in: "bl2 ∈# ℬ - {#bl1#}" and 
        card1: "card bl1 = 𝗆" and card2: "card bl2 = 𝗆"
      using obtain_two_items_mset_filter by blast 
    then have "bl1 |∩| bl2 = 𝗆" using const_intersect by simp
    then have "bl1 = bl2"
      by (metis blin bl2in card1 card2 finite_blocks in_diffD inter_eq_blocks_eq_card)
    then have "multiplicity bl1 > 1"
      using ‹bl2 ∈# remove1_mset bl1 ℬ› count_eq_zero_iff by force 
    thus False using mult blin by simp
  qed
qed

lemma empty_inter_implies_rep_one: 
  assumes "𝗆 = 0"
  assumes "x ∈ 𝒱"
  shows "ℬ rep x ≤ 1"
proof (rule ccontr)
  assume a: "¬ ℬ rep x ≤ 1"
  then have gt1: "ℬ rep x > 1" by simp
  then obtain bl1 where blin1: "bl1 ∈# ℬ" and xin1: "x ∈ bl1"
    by (metis gr_implies_not0 linorder_neqE_nat rep_number_g0_exists) 
  then have "(ℬ - {#bl1#}) rep x > 0" using gt1 point_rep_number_split point_rep_singleton_val
    by (metis a add_0 eq_imp_le neq0_conv remove1_mset_eqE) 
  then obtain bl2 where blin2: "bl2 ∈# (ℬ - {#bl1#})" and xin2: "x ∈ bl2" 
    by (metis rep_number_g0_exists) 
  then have "x ∈ (bl1 ∩ bl2)" using xin1 by simp
  then have "bl1 |∩| bl2 ≠ 0"
    by (metis blin1 empty_iff finite_blocks intersection_number_empty_iff) 
  thus False using const_intersect assms blin1 blin2 by simp
qed

lemma empty_inter_implies_b_lt_v: 
  assumes "𝗆 = 0"
  shows "𝖻 ≤ 𝗏"
proof -
  have le1: "⋀ x. x ∈ 𝒱 ⟹ ℬ rep x ≤ 1" using empty_inter_implies_rep_one assms by simp
  have disj: "{v ∈ 𝒱 . ℬ rep v = 0} ∩ {v ∈ 𝒱 . ¬ (ℬ rep v = 0)} = {}" by auto
  have eqv: "𝒱 = ({v ∈ 𝒱 . ℬ rep v = 0} ∪ {v ∈ 𝒱 . ¬ (ℬ rep v = 0)})" by auto
  have "𝖻 ≤ (∑ x ∈ 𝒱 . ℬ rep x)" using block_num_rep_bound by simp
  also have 1: "... ≤ (∑ x ∈ ({v ∈ 𝒱 . ℬ rep v = 0} ∪ {v ∈ 𝒱 . ¬ (ℬ rep v = 0)}) . ℬ rep x)" 
    using eqv by simp
  also have "... ≤ (∑ x ∈ ({v ∈ 𝒱 . ℬ rep v = 0}) . ℬ rep x) + (∑ x ∈ ({v ∈ 𝒱 . ¬ (ℬ rep v = 0)}) . ℬ rep x)"
    using sum.union_disjoint finite_sets eqv disj
    by (metis (no_types, lifting) 1 finite_Un) 
  also have "... ≤ (∑ x ∈ ({v ∈ 𝒱 . ¬ (ℬ rep v = 0)}) . ℬ rep x)" by simp
  also have "... ≤ (∑ x ∈ ({v ∈ 𝒱 . ¬ (ℬ rep v = 0)}) . 1)" using le1
    by (metis (mono_tags, lifting) mem_Collect_eq sum_mono)
  also have "... ≤ card {v ∈ 𝒱 . ¬ (ℬ rep v = 0)}" by simp
  also have "... ≤ card 𝒱" using finite_sets
    using card_mono eqv by blast 
  finally show ?thesis by simp
qed

end

locale simple_const_intersect_design = const_intersect_design + simple_design

end