(* 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