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