Theory Design_Theory.Design_Basics

theory Design_Basics imports Main Multisets_Extras "HOL-Library.Disjoint_Sets"
begin

section ‹Design Theory Basics›
text ‹All definitions in this section reference the handbook of combinatorial designs
 cite"colbournHandbookCombinatorialDesigns2007"

subsection ‹Initial setup›

text ‹Enable coercion of nats to ints to aid with reasoning on design properties›
declare [[coercion_enabled]]
declare [[coercion "of_nat :: nat  int"]]

subsection ‹Incidence System›

text ‹An incidence system is defined to be a wellformed set system. i.e. each block is a subset
of the base point set. Alternatively, an incidence system can be looked at as the point set
and an incidence relation which indicates if they are in the same block›

locale incidence_system = 
  fixes point_set :: "'a set" ("𝒱")
  fixes block_collection :: "'a set multiset" ("")
  assumes wellformed: "b ∈#   b  𝒱"
begin

definition "  { (x, b) . b ∈#   x  b}" (* incidence relation *)

definition incident :: "'a  'a set  bool" where
"incident p b  (p, b)  "

text ‹Defines common notation used to indicate number of points ($v$) and number of blocks ($b$)›
abbreviation "𝗏  card 𝒱"

abbreviation "𝖻  size "

text ‹Basic incidence lemmas›

lemma incidence_alt_def: 
  assumes "p  𝒱"
  assumes "b ∈# "
  shows "incident p b  p  b"
  by (auto simp add: incident_def ℐ_def assms)

lemma wf_invalid_point: "x  𝒱  b ∈#   x  b"
  using wellformed by auto

lemma block_set_nempty_imp_block_ex: "  {#}   bl . bl ∈# "
  by auto

text ‹Abbreviations for all incidence systems›
abbreviation multiplicity :: "'a set  nat" where
"multiplicity b  count  b"

abbreviation incomplete_block :: "'a set  bool" where
"incomplete_block bl  card bl < card 𝒱  bl ∈# "

lemma incomplete_alt_size: "incomplete_block bl  card bl < 𝗏" 
  by simp

lemma incomplete_alt_in: "incomplete_block bl  bl ∈# "
  by simp

lemma incomplete_alt_imp[intro]: "card bl < 𝗏  bl ∈#   incomplete_block bl"
  by simp

definition design_support :: "'a set set" where
"design_support  set_mset "

end

subsection ‹Finite Incidence Systems›

text ‹These simply require the point set to be finite.
As multisets are only defined to be finite, it is implied that the block set must be finite already›

locale finite_incidence_system = incidence_system + 
  assumes finite_sets: "finite 𝒱"
begin

lemma finite_blocks: "b ∈#   finite b"
  using wellformed finite_sets finite_subset by blast 

lemma mset_points_distinct: "distinct_mset (mset_set 𝒱)"
  using finite_sets by (simp add: distinct_mset_def)

lemma mset_points_distinct_diff_one: "distinct_mset (mset_set (𝒱 - {x}))"
  by (meson count_mset_set_le_one distinct_mset_count_less_1)

lemma finite_design_support: "finite (design_support)"
  using design_support_def by auto 

lemma block_size_lt_order: "bl ∈#   card bl  card 𝒱"
  using wellformed by (simp add: card_mono finite_sets)  

end

subsection ‹Designs›

text ‹There are many varied definitions of a design in literature. However, the most
commonly accepted definition is a finite point set, $V$ and collection of blocks $B$, where
no block in $B$ can be empty›
locale design = finite_incidence_system +
  assumes blocks_nempty: "bl ∈#   bl  {}"
begin

lemma wf_design: "design 𝒱 "  by intro_locales

lemma wf_design_iff: "bl ∈#   design 𝒱   (bl  𝒱  finite 𝒱  bl  {})"
  using blocks_nempty wellformed finite_sets
  by (simp add: wf_design) 

text ‹Reasoning on non empty properties and non zero parameters›
lemma blocks_nempty_alt: " bl ∈# . bl  {}"
  using blocks_nempty by auto

lemma block_set_nempty_imp_points: "  {#}  𝒱  {}"
  using wf_design wf_design_iff by auto

lemma b_non_zero_imp_v_non_zero: "𝖻 > 0  𝗏 > 0"
  using block_set_nempty_imp_points finite_sets by fastforce

lemma v_eq0_imp_b_eq_0: "𝗏 = 0  𝖻 = 0"
  using b_non_zero_imp_v_non_zero by auto

text ‹Size lemmas›
lemma block_size_lt_v: "bl ∈#   card bl  𝗏"
  by (simp add: card_mono finite_sets wellformed)

lemma block_size_gt_0: "bl ∈#   card bl > 0"
  using finite_sets blocks_nempty finite_blocks by fastforce

lemma design_cart_product_size: "size ((mset_set 𝒱) ×# ) = 𝗏 * 𝖻"
  by (simp add: size_cartesian_product) 

end

text ‹Intro rules for design locale›

lemma wf_design_implies: 
  assumes "( b . b ∈#   b  V)"
  assumes " b . b ∈#   b  {}"
  assumes "finite V"
  assumes "  {#}"
  assumes "V  {}"
  shows "design V "
  using assms by (unfold_locales) simp_all

lemma (in incidence_system) finite_sysI[intro]: "finite 𝒱  finite_incidence_system 𝒱 "
  by (unfold_locales) simp_all

lemma (in finite_incidence_system) designI[intro]: "( b. b ∈#   b  {})    {#}
      𝒱  {}  design 𝒱 "
  by (unfold_locales) simp_all

subsection ‹Core Property Definitions›

subsubsection ‹Replication Number›

text ‹The replication number for a point is the number of blocks that point is incident with›

definition point_replication_number :: "'a set multiset  'a  nat" (infix "rep" 75) where
"B rep x  size {#b ∈# B . x  b#}"

lemma max_point_rep: "B rep x  size B"
  using size_filter_mset_lesseq by (simp add: point_replication_number_def)

lemma rep_number_g0_exists: 
  assumes "B rep x > 0" 
  obtains b where "b ∈# B" and "x  b"
proof -
  have "size {#b ∈# B . x  b#} > 0" using assms point_replication_number_def
    by metis
  thus ?thesis
    by (metis filter_mset_empty_conv nonempty_has_size that) 
qed

lemma rep_number_on_set_def: "finite B  (mset_set B) rep x = card {b  B . x  b}"
  by (simp add: point_replication_number_def)

lemma point_rep_number_split[simp]: "(A + B) rep x = A rep x + B rep x"
  by (simp add: point_replication_number_def)

lemma point_rep_singleton_val [simp]: "x  b  {#b#} rep x = 1"
  by (simp add: point_replication_number_def)

lemma point_rep_singleton_inval [simp]: "x  b  {#b#} rep x = 0"
  by (simp add: point_replication_number_def)

context incidence_system
begin

lemma point_rep_number_alt_def: " rep x = size {# b ∈#  . x  b#}"
  by (simp add: point_replication_number_def)

lemma rep_number_non_zero_system_point: "  rep x > 0  x  𝒱"
  using rep_number_g0_exists wellformed
  by (metis wf_invalid_point) 

lemma point_rep_non_existance [simp]: "x  𝒱   rep x = 0"
  using wf_invalid_point by (simp add:  point_replication_number_def filter_mset_empty_conv) 

lemma point_rep_number_inv: "size {# b ∈#  . x  b #} = 𝖻 - ( rep x)"
proof -
  have "𝖻 = size {# b ∈#  . x  b #} + size {# b ∈#  . x  b #}"
    using multiset_partition by (metis add.commute size_union)  
  thus ?thesis by (simp add: point_replication_number_def) 
qed

lemma point_rep_num_inv_non_empty: "( rep x) < 𝖻    {#}  {# b ∈#  . x  b #}  {#}"
  by (metis diff_zero point_replication_number_def size_empty size_filter_neg verit_comp_simplify1(1))

end

subsubsection ‹Point Index›

text ‹The point index of a subset of points in a design, is the number of times those points 
occur together in a block of the design›
definition points_index :: "'a set multiset  'a set  nat" (infix "index" 75) where
"B index ps  size {#b ∈# B . ps  b#}"

lemma points_index_empty [simp]: "{#} index ps = 0"
  by (simp add: points_index_def)

lemma point_index_distrib: "(B1 + B2) index ps =  B1 index ps + B2 index ps"
  by (simp add: points_index_def)

lemma point_index_diff: "B1 index ps = (B1 + B2) index ps - B2 index ps"
  by (simp add: points_index_def)

lemma points_index_singleton: "{#b#} index ps = 1  ps  b"
  by (simp add: points_index_def)

lemma points_index_singleton_zero: "¬ (ps  b)  {#b#} index ps = 0"
  by (simp add: points_index_def)

lemma points_index_sum: "(# B ) index ps = (b ∈# B . (b index ps))"
  using points_index_empty by (induction B) (auto simp add: point_index_distrib)

lemma points_index_block_image_add_eq: 
  assumes "x  ps"
  assumes "B index ps = l"
  shows "{# insert x b . b ∈# B#} index ps = l"
  using points_index_def by (metis (no_types, lifting) assms filter_mset_cong 
      image_mset_filter_swap2 points_index_def size_image_mset subset_insert)

lemma points_index_on_set_def [simp]: 
  assumes "finite B"
  shows "(mset_set B) index ps = card {b  B. ps  b}"
  by (simp add: points_index_def assms)

lemma points_index_single_rep_num: "B index {x} = B rep x"
  by (simp add: points_index_def point_replication_number_def)

lemma points_index_pair_rep_num: 
  assumes " b. b ∈# B  x  b"
  shows "B index {x, y} = B rep y"
  using point_replication_number_def points_index_def
  by (metis assms empty_subsetI filter_mset_cong insert_subset)

lemma points_index_0_left_imp: 
  assumes "B index ps = 0"
  assumes "b ∈# B"
  shows "¬ (ps  b)"
proof (rule ccontr)
  assume "¬ ¬ ps  b"
  then have a: "ps  b" by auto
  then have "b ∈# {#bl ∈# B . ps  bl#}" by (simp add: assms(2)) 
  thus False by (metis assms(1) count_greater_eq_Suc_zero_iff count_size_set_repr not_less_eq_eq 
        points_index_def size_filter_mset_lesseq) 
qed

lemma points_index_0_right_imp: 
  assumes " b . b ∈# B  (¬ ps  b)"
  shows "B index ps = 0"
  using assms by (simp add: filter_mset_empty_conv points_index_def)

lemma points_index_0_iff: "B index ps = 0  ( b. b ∈# B  (¬ ps  b))"
  using points_index_0_left_imp points_index_0_right_imp by metis

lemma points_index_gt0_impl_existance: 
  assumes "B index ps > 0"
  shows "( bl . (bl ∈# B  ps  bl))"
proof -
  have "size {#bl ∈# B . ps  bl#} > 0"
    by (metis assms points_index_def)
  then obtain bl where "bl ∈# B" and "ps  bl"
    by (metis filter_mset_empty_conv nonempty_has_size) 
  thus ?thesis by auto
qed

lemma points_index_one_unique: 
  assumes "B index ps = 1"
  assumes "bl ∈# B" and "ps  bl" and "bl' ∈# B" and "ps  bl'"
  shows "bl = bl'"
proof (rule ccontr)
  assume assm: "bl  bl'"
  then have bl1: "bl ∈# {#bl ∈# B . ps  bl#}" using assms by simp
  then have bl2: "bl'∈# {#bl ∈# B . ps  bl#}" using assms by simp
  then have "{#bl, bl'#} ⊆# {#bl ∈# B . ps  bl#}" using assms by (metis bl1 bl2 points_index_def
        add_mset_subseteq_single_iff assm mset_subset_eq_single size_single subseteq_mset_size_eql) 
  then have "size {#bl ∈# B . ps  bl#}  2" using size_mset_mono by fastforce 
  thus False using assms by (metis numeral_le_one_iff points_index_def semiring_norm(69))
qed

lemma points_index_one_unique_block: 
  assumes "B index ps = 1"
  shows "∃! bl . (bl ∈# B  ps  bl)"
  using assms points_index_gt0_impl_existance points_index_one_unique
  by (metis zero_less_one) 

lemma points_index_one_not_unique_block: 
  assumes "B index ps = 1"
  assumes "ps  bl"
  assumes "bl ∈# B"
  assumes "bl' ∈# B - {#bl#}"
  shows "¬ ps  bl'"
proof - 
  have "B = (B - {#bl#}) + {#bl#}" by (simp add: assms(3)) 
  then have "(B - {#bl#}) index ps = B index ps - {#bl#} index ps"
    by (metis point_index_diff) 
  then have "(B - {#bl#}) index ps = 0" using assms points_index_singleton
    by (metis diff_self_eq_0) 
  thus ?thesis using assms(4) points_index_0_left_imp by auto
qed

lemma (in incidence_system) points_index_alt_def: " index ps = size {#b ∈#  . ps  b#}"
  by (simp add: points_index_def)

lemma (in incidence_system) points_index_ps_nin: "¬ (ps  𝒱)   index ps = 0"
  using points_index_alt_def filter_mset_empty_conv in_mono size_empty subsetI wf_invalid_point
  by metis 

lemma (in incidence_system) points_index_count_bl: 
    "multiplicity bl  n  ps  bl  count {#bl ∈#  . ps  bl#} bl  n"
  by simp

lemma (in finite_incidence_system) points_index_zero: 
  assumes "card ps > card 𝒱" 
  shows " index ps = 0"
proof -
  have " b. b ∈#   card ps > card b" 
    using block_size_lt_order card_subset_not_gt_card finite_sets assms by fastforce 
  then have "{#b ∈#  . ps  b#} = {#}"
    by (simp add: card_subset_not_gt_card filter_mset_empty_conv finite_blocks)
  thus ?thesis using points_index_alt_def by simp
qed

lemma (in design) points_index_subset: 
    "x ⊆# {#bl ∈#  . ps  bl#}  ps  𝒱  ( index ps)  (size x)"
  by (simp add: points_index_def size_mset_mono)

lemma (in design) points_index_count_min: "multiplicity bl  n  ps  bl   index ps  n"
  using points_index_alt_def set_count_size_min by (metis filter_mset.rep_eq) 

subsubsection ‹Intersection Number›

text ‹The intersection number of two blocks is the size of the intersection of those blocks. i.e. 
the number of points which occur in both blocks›
definition intersection_number :: "'a set  'a set  nat" (infix "|∩|" 70) where
"b1 |∩| b2  card (b1  b2)"

lemma intersection_num_non_neg: "b1 |∩| b2  0"
  by (simp add: intersection_number_def)

lemma intersection_number_empty_iff: 
  assumes "finite b1"
  shows "b1  b2 = {}  b1 |∩| b2 = 0"
  by (simp add: intersection_number_def assms)

lemma intersect_num_commute: "b1 |∩| b2 = b2 |∩| b1"
  by (simp add: inf_commute intersection_number_def) 

definition n_intersect_number :: "'a set  nat 'a set  nat" where
"n_intersect_number b1 n b2  card { x  Pow (b1  b2) . card x = n}"

notation n_intersect_number ("(_ |∩|⇩_ _)" [52, 51, 52] 50)

lemma n_intersect_num_subset_def: "b1 |∩|⇩n b2 = card {x . x  b1  b2  card x = n}"
  using n_intersect_number_def by auto

lemma n_inter_num_one: "finite b1  finite b2  b1 |∩|⇩1 b2 = b1 |∩| b2"
  using n_intersect_number_def intersection_number_def card_Pow_filter_one
  by (metis (full_types) finite_Int) 

lemma n_inter_num_choose: "finite b1  finite b2  b1 |∩|⇩n b2 = (card (b1  b2) choose n)" 
  using n_subsets n_intersect_num_subset_def
  by (metis (full_types) finite_Int) 

lemma set_filter_single: "x  A  {a  A . a = x} = {x}"
  by auto 

lemma (in design) n_inter_num_zero: 
  assumes "b1 ∈# " and "b2 ∈# "
  shows "b1 |∩|⇩0 b2 = 1"
proof -
  have empty: "x . finite x  card x = 0  x = {}"
    by simp
  have empt_in: "{}  Pow (b1  b2)" by simp
  have "finite (b1  b2)" using finite_blocks assms by simp
  then have " x . x  Pow (b1  b2)  finite x" by (meson PowD finite_subset) 
  then have "{x  Pow (b1  b2) . card x = 0} = {x  Pow (b1  b2) . x = {}}" 
    using empty by (metis card.empty)
  then have "{x  Pow (b1  b2) . card x = 0} = {{}}" 
    by (simp add: empt_in set_filter_single Collect_conv_if)
  thus ?thesis by (simp add: n_intersect_number_def)
qed

lemma (in design) n_inter_num_choose_design: "b1 ∈#   b2 ∈#  
     b1 |∩|⇩n b2 = (card (b1  b2) choose n) "
  using finite_blocks by (simp add: n_inter_num_choose)

lemma (in design) n_inter_num_choose_design_inter: "b1 ∈#   b2 ∈#  
     b1 |∩|⇩n b2 = (nat (b1 |∩| b2) choose n) "
  using finite_blocks by (simp add: n_inter_num_choose intersection_number_def)

subsection ‹Incidence System Set Property Definitions›
context incidence_system
begin

text ‹The set of replication numbers for all points of design›
definition replication_numbers :: "nat set" where
"replication_numbers  { rep x | x . x  𝒱}"

lemma replication_numbers_non_empty: 
  assumes "𝒱  {}"
  shows "replication_numbers  {}"
  by (simp add: assms replication_numbers_def) 

lemma obtain_point_with_rep: "r  replication_numbers   x. x  𝒱   rep x = r"
  using replication_numbers_def by auto

lemma point_rep_number_in_set: "x  𝒱  ( rep x)  replication_numbers"
  by (auto simp add: replication_numbers_def)

lemma (in finite_incidence_system) replication_numbers_finite: "finite replication_numbers"
  using finite_sets by (simp add: replication_numbers_def)

text ‹The set of all block sizes in a system›

definition sys_block_sizes :: "nat set" where
"sys_block_sizes  { card bl | bl. bl ∈# }"

lemma block_sizes_non_empty_set: 
  assumes "  {#}"
  shows "sys_block_sizes  {}"
by (simp add: sys_block_sizes_def assms)

lemma finite_block_sizes: "finite (sys_block_sizes)"
  by (simp add: sys_block_sizes_def)

lemma block_sizes_non_empty: 
  assumes "  {#}"
  shows "card (sys_block_sizes) > 0"
  using finite_block_sizes block_sizes_non_empty_set
  by (simp add: assms card_gt_0_iff) 

lemma sys_block_sizes_in: "bl ∈#   card bl  sys_block_sizes"
  unfolding sys_block_sizes_def by auto 

lemma sys_block_sizes_obtain_bl: "x  sys_block_sizes   ( bl ∈# . card bl = x)"
  by (auto simp add: sys_block_sizes_def)

text ‹The set of all possible intersection numbers in a system.›

definition intersection_numbers :: "nat set" where
"intersection_numbers  { b1 |∩| b2 | b1 b2 . b1 ∈#   b2 ∈# ( - {#b1#})}"

lemma obtain_blocks_intersect_num: "n  intersection_numbers  
   b1 b2. b1 ∈#   b2 ∈# ( - {#b1#})   b1 |∩| b2 = n"
  by (auto simp add: intersection_numbers_def)

lemma intersect_num_in_set: "b1 ∈#   b2 ∈# ( - {#b1#})  b1 |∩| b2  intersection_numbers"
  by (auto simp add: intersection_numbers_def)

text ‹The set of all possible point indices›
definition point_indices :: "nat  nat set" where
"point_indices t  { index ps | ps. card ps = t  ps  𝒱}"

lemma point_indices_elem_in: "ps  𝒱  card ps = t   index ps  point_indices t"
  by (auto simp add: point_indices_def)

lemma point_indices_alt_def: "point_indices t = {  index ps | ps. card ps = t  ps  𝒱}"
  by (simp add: point_indices_def)

end

subsection ‹Basic Constructions on designs›

text ‹This section defines some of the most common universal constructions found in design theory
involving only a single design›

subsubsection ‹Design Complements›

context incidence_system
begin

text ‹The complement of a block are all the points in the design not in that block. 
The complement of a design is therefore the original point sets, and set of all block complements›
definition block_complement:: "'a set  'a set" ("_c" [56] 55) where
"block_complement b  𝒱 - b"

definition complement_blocks :: "'a set multiset" ("(C)")where
"complement_blocks  {# blc . bl ∈#  #}" 

lemma block_complement_elem_iff: 
  assumes "ps  𝒱"
  shows "ps  blc  ( x  ps. x  bl)"
  using assms block_complement_def by (auto)

lemma block_complement_inter_empty: "bl1c = bl2  bl1  bl2 = {}"
  using block_complement_def by auto

lemma block_complement_inv: 
  assumes "bl ∈# "
  assumes "blc = bl2"
  shows "bl2c = bl"
  by (metis Diff_Diff_Int assms(1) assms(2) block_complement_def inf.absorb_iff2 wellformed)

lemma block_complement_subset_points: "ps  (blc)  ps  𝒱"
  using block_complement_def by blast

lemma obtain_comp_block_orig: 
  assumes "bl1 ∈# C"
  obtains bl2 where "bl2 ∈# " and "bl1 = bl2c"
  using wellformed assms by (auto simp add: complement_blocks_def)

lemma complement_same_b [simp]: "size C = size "
  by (simp add: complement_blocks_def)

lemma block_comp_elem_alt_left: "x  bl  ps  blc  x  ps"
  by (auto simp add: block_complement_def block_complement_elem_iff)

lemma block_comp_elem_alt_right: "ps  𝒱  ( x . x  ps  x  bl)  ps  blc"
  by (auto simp add: block_complement_elem_iff)

lemma complement_index:
  assumes "ps  𝒱"
  shows "C index ps = size {# b ∈#  . ( x  ps . x  b) #}"
proof -
  have "C index ps =  size {# b ∈# {# blc . bl ∈# #}. ps  b #}"
    by (simp add: complement_blocks_def points_index_def) 
  then have "C index ps = size {# blc | bl ∈#  . ps  blc #}"
    by (metis image_mset_filter_swap)
  thus ?thesis using assms by (simp add: block_complement_elem_iff)
qed

lemma complement_index_2:
  assumes "{x, y}  𝒱"
  shows "C index {x, y} = size {# b ∈#  . x  b  y  b #}"
proof -
  have a: " b. b ∈#    x'  {x, y} . x'  b  x  b  y  b"
    by simp 
  have " b. b ∈#   x  b  y  b   x'  {x, y} . x'  b "
    by simp 
  thus ?thesis using assms a complement_index
    by (smt (verit) filter_mset_cong) 
qed

lemma complement_rep_number: 
  assumes "x  𝒱" and " rep x = r" 
  shows  "C rep x = 𝖻 - r"
proof - 
  have r: "size {#b ∈#  . x  b#} = r" using assms by (simp add: point_replication_number_def)
  then have a: " b . b ∈#   x  b  x  bc"
    by (simp add: block_complement_def)
  have " b . b ∈#   x  b  x  bc"
    by (simp add: assms(1) block_complement_def) 
  then have alt: "(image_mset block_complement ) rep x = size {#b ∈#  . x  b#}" 
    using a filter_mset_cong image_mset_filter_swap2 point_replication_number_def
    by (smt (verit, ccfv_SIG) size_image_mset) 
  have "𝖻 = size {#b ∈#  . x  b#} + size {#b ∈#  . x  b#}"
    by (metis multiset_partition size_union) 
  thus ?thesis using alt
    by (simp add: r complement_blocks_def)
qed

lemma complement_blocks_wf: "bl ∈# C  bl  𝒱"
  by (auto simp add: complement_blocks_def block_complement_def)

lemma complement_wf [intro]: "incidence_system 𝒱 C"
  using complement_blocks_wf by (unfold_locales)

interpretation sys_complement: incidence_system "𝒱" "C"
  using complement_wf by simp 
end

context finite_incidence_system
begin
lemma block_complement_size: "b  𝒱  card (bc) = card 𝒱 - card b"
  by (simp add: block_complement_def card_Diff_subset finite_subset card_mono of_nat_diff finite_sets)  

lemma block_comp_incomplete: "incomplete_block bl  card (blc) > 0"
  using block_complement_size by (simp add: wellformed) 

lemma  block_comp_incomplete_nempty: "incomplete_block bl  blc  {}"
  using wellformed block_complement_def finite_blocks
  by (auto simp add: block_complement_size block_comp_incomplete card_subset_not_gt_card)

lemma incomplete_block_proper_subset: "incomplete_block bl  bl  𝒱"
  using wellformed by fastforce

lemma complement_finite: "finite_incidence_system 𝒱 C"
  using complement_wf finite_sets by (simp add: incidence_system.finite_sysI) 

interpretation comp_fin: finite_incidence_system 𝒱 "C"
  using complement_finite by simp 

end

context design
begin
lemma (in design) complement_design: 
  assumes " bl . bl ∈#   incomplete_block bl" 
  shows "design 𝒱 (C)"
proof -
  interpret fin: finite_incidence_system 𝒱 "C" using complement_finite by simp
  show ?thesis using assms block_comp_incomplete_nempty wellformed 
    by (unfold_locales) (auto simp add: complement_blocks_def)
qed

end
subsubsection ‹Multiples›
text ‹An easy way to construct new set systems is to simply multiply the block collection by some 
constant›

context incidence_system 
begin

abbreviation multiple_blocks :: "nat  'a set multiset" where
"multiple_blocks n  repeat_mset n "

lemma multiple_block_in_original: "b ∈# multiple_blocks n  b ∈# "
  by (simp add: elem_in_repeat_in_original) 

lemma multiple_block_in: "n > 0  b ∈#    b ∈# multiple_blocks n"
  by (simp add: elem_in_original_in_repeat)

lemma multiple_blocks_gt: "n > 0  size (multiple_blocks n)  size " 
  by (simp)

lemma block_original_count_le: "n > 0  count  b  count (multiple_blocks n) b"
  using count_repeat_mset by simp 

lemma multiple_blocks_sub: "n > 0   ⊆# (multiple_blocks n)"
  by (simp add: mset_subset_eqI block_original_count_le) 

lemma multiple_1_same: "multiple_blocks 1 = "
  by simp

lemma multiple_unfold_1: "multiple_blocks (Suc n) = (multiple_blocks n) + "
  by simp

lemma multiple_point_rep_num: "(multiple_blocks n) rep x = ( rep x) * n"
proof (induction n)
  case 0
  then show ?case by (simp add: point_replication_number_def)
next
  case (Suc n)
  then have "multiple_blocks (Suc n) rep x =  rep x * n + ( rep x)"
    using Suc.IH Suc.prems by (simp add: union_commute point_replication_number_def)
  then show ?case
    by (simp)
qed

lemma multiple_point_index: "(multiple_blocks n) index ps = ( index ps) * n"
  by (induction n) (auto simp add: points_index_def)

lemma repeat_mset_block_point_rel: "b x. b ∈# multiple_blocks  n  x  b  x  𝒱"
  by (induction n) (auto, meson subset_iff wellformed)

lemma multiple_is_wellformed: "incidence_system 𝒱 (multiple_blocks n)"
  using repeat_mset_subset_in wellformed repeat_mset_block_point_rel by (unfold_locales) (auto)

lemma  multiple_blocks_num [simp]: "size (multiple_blocks n) = n*𝖻"
  by simp

interpretation mult_sys: incidence_system 𝒱 "(multiple_blocks n)"
  by (simp add: multiple_is_wellformed)

lemma multiple_block_multiplicity [simp]: "mult_sys.multiplicity n bl = (multiplicity bl) * n"
  by (simp)

lemma multiple_block_sizes_same: 
  assumes "n > 0" 
  shows "sys_block_sizes = mult_sys.sys_block_sizes n"
proof -
  have def: "mult_sys.sys_block_sizes n = {card bl | bl. bl ∈# (multiple_blocks n)}"
    by (simp add: mult_sys.sys_block_sizes_def) 
  then have eq: " bl. bl ∈# (multiple_blocks n)  bl ∈# "
    using assms multiple_block_in multiple_block_in_original by blast 
  thus ?thesis using def by (simp add: sys_block_sizes_def eq)
qed 

end

context finite_incidence_system
begin

lemma multiple_is_finite: "finite_incidence_system 𝒱 (multiple_blocks n)"
  using multiple_is_wellformed finite_sets by (unfold_locales) (auto simp add: incidence_system_def)

end

context design
begin

lemma multiple_is_design: "design 𝒱 (multiple_blocks n)"
proof -
  interpret fis: finite_incidence_system 𝒱 "multiple_blocks n" using multiple_is_finite by simp
  show ?thesis using blocks_nempty
    by (unfold_locales) (auto simp add: elem_in_repeat_in_original repeat_mset_not_empty)
qed

end

subsection ‹Simple Designs›

text ‹Simple designs are those in which the multiplicity of each block is at most one. 
In other words, the block collection is a set. This can significantly ease reasoning.›

locale simple_incidence_system = incidence_system + 
  assumes simple [simp]: "bl ∈#   multiplicity bl = 1"

begin 

lemma simple_alt_def_all: " bl ∈#  . multiplicity bl = 1"
  using simple by auto
  
lemma simple_blocks_eq_sup: "mset_set (design_support) = "
  using distinct_mset_def simple design_support_def by (metis distinct_mset_set_mset_ident) 

lemma simple_block_size_eq_card: "𝖻 = card (design_support)"
  by (metis simple_blocks_eq_sup size_mset_set)

lemma points_index_simple_def: " index ps = card {b  design_support . ps  b}"
  using design_support_def points_index_def card_size_filter_eq simple_blocks_eq_sup
  by (metis finite_set_mset) 

lemma replication_num_simple_def: " rep x = card {b  design_support . x  b}"
  using design_support_def point_replication_number_def card_size_filter_eq simple_blocks_eq_sup
  by (metis finite_set_mset) 

end

locale simple_design = design + simple_incidence_system

text ‹Additional reasoning about when something is not simple›
context incidence_system
begin
lemma simple_not_multiplicity: "b ∈#   multiplicity  b > 1  ¬ simple_incidence_system 𝒱 "
  using simple_incidence_system_def simple_incidence_system_axioms_def by (metis nat_neq_iff) 

lemma multiple_not_simple: 
  assumes "n > 1"
  assumes "  {#}"
  shows "¬ simple_incidence_system 𝒱 (multiple_blocks n)"
proof (rule ccontr, simp)
  assume "simple_incidence_system 𝒱 (multiple_blocks n)"
  then have " bl. bl ∈#   count (multiple_blocks n) bl = 1"
    using assms(1) elem_in_original_in_repeat
    by (metis not_gr_zero not_less_zero simple_incidence_system.simple)
  thus False using assms by auto 
qed

end

subsection ‹Proper Designs›
text ‹Many types of designs rely on parameter conditions that only make sense for non-empty designs. 
i.e. designs with at least one block, and therefore given well-formed condition, at least one point. 
To this end we define the notion of a "proper" design›

locale proper_design = design + 
  assumes b_non_zero: "𝖻  0"
begin

lemma is_proper: "proper_design 𝒱 " by intro_locales

lemma v_non_zero: "𝗏 > 0"
  using b_non_zero v_eq0_imp_b_eq_0 by auto

lemma b_positive: "𝖻 > 0" using b_non_zero
  by (simp add: nonempty_has_size)

lemma design_points_nempty: "𝒱  {}"
  using v_non_zero by auto 

lemma design_blocks_nempty: "  {#}"
  using b_non_zero by auto

end

text ‹Intro rules for a proper design›
lemma (in design) proper_designI[intro]: "𝖻  0  proper_design 𝒱 "
  by (unfold_locales) simp

lemma proper_designII[intro]: 
  assumes "design V B" and "B  {#}" 
  shows "proper_design V B"
proof -
  interpret des: design V B using assms by simp
  show ?thesis using assms by unfold_locales simp
qed

text ‹Reasoning on construction closure for proper designs›
context proper_design
begin

lemma multiple_proper_design: 
  assumes "n > 0"
  shows "proper_design 𝒱 (multiple_blocks n)"
  using multiple_is_design assms design_blocks_nempty multiple_block_in
  by (metis block_set_nempty_imp_block_ex empty_iff proper_designII set_mset_empty) 

lemma complement_proper_design: 
  assumes " bl . bl ∈#   incomplete_block bl"
  shows "proper_design 𝒱 C"
proof -
  interpret des: design 𝒱 "C"
    by (simp add: assms complement_design)  
  show ?thesis using b_non_zero by (unfold_locales) auto
qed

end
end