# Theory 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"

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"

lemma intersect_num_same_eq_size[simp]: "bl |∩| bl = card bl"

lemma index_lt_rep_general: "x ∈ ps ⟹ B index ps ≤ B rep x"
(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 ℬ"

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

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
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#}))"
also have "... = (∑ x ∈# (mset_set 𝒱). size ({#b ∈# ℬ. x ∈ b#}))"
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
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

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
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 = 𝒱#} > Λ"
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 < Λ"
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)
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#}"
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
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#}"
then have "{#b ∈# ℬ . b = bl#} ⊆# {#bl ∈# ℬ. card bl = 𝗆#}" using True
then have "size {#b ∈# ℬ . b = bl#} ≤ size {#bl ∈# ℬ. card bl = 𝗆#}"
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
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```