Theory Design_Theory.Design_Operations

theory Design_Operations imports Design_Basics
begin

section ‹Design Operations›
text ‹Incidence systems have a number of very typical computational operations
which can be used for constructions in design theory. Definitions in this section are based off
the handbook of combinatorial designs, hypergraph theory \<^cite>‹"bergeHypergraphsCombinatoricsFinite1989"›, 
and the GAP design theory library \<^cite>‹"soicherDesignsGroupsComputing2013"››

subsection ‹Incidence system definitions›

context incidence_system
begin

text ‹The basic add point operation only affects the point set of a design›
definition add_point :: "'a ⇒ 'a set" where
"add_point p ≡ insert p 𝒱"

lemma add_existing_point [simp]: "p ∈ 𝒱 ⟹ add_point p = 𝒱"
  using add_point_def by fastforce

lemma add_point_wf: "incidence_system (add_point p) ℬ"
  using wf_invalid_point add_point_def by (unfold_locales) (auto)

text ‹An extension of the basic add point operation also adds the point to a given set of blocks›
definition add_point_to_blocks :: "'a ⇒ 'a set set ⇒ 'a set multiset" where
"add_point_to_blocks p bs ≡ {# (insert p b) | b ∈# ℬ . b ∈ bs#} + {# b ∈# ℬ . b ∉ bs#}"

lemma add_point_blocks_blocks_alt: "add_point_to_blocks p bs = 
    image_mset (insert p) (filter_mset (λ b . b ∈ bs) ℬ) + (filter_mset (λ b . b ∉ bs) ℬ)"
  using add_point_to_blocks_def by simp

lemma add_point_existing_blocks: 
  assumes "(⋀ bl . bl ∈ bs ⟹ p ∈ bl)" 
  shows "add_point_to_blocks p bs = ℬ"
proof (simp add: add_point_to_blocks_def)
  have "image_mset (insert p) {#b ∈# ℬ. b ∈ bs#} = {#b ∈# ℬ. b ∈ bs#}" using assms
    by (simp add: image_filter_cong insert_absorb) 
  thus "image_mset (insert p) {#b ∈# ℬ. b ∈ bs#} + {#b ∈# ℬ. b ∉ bs#} = ℬ" 
    using multiset_partition by simp 
qed

lemma add_new_point_rep_number: 
  assumes "p ∉ 𝒱"
  shows "(add_point_to_blocks p bs) rep p = size {#b ∈# ℬ . b ∈ bs#}"
proof -
  have "⋀ b. b ∈# ℬ ⟹ b ∉ bs ⟹ p ∉ b"
    by (simp add: assms wf_invalid_point) 
  then have zero: "{# b ∈# ℬ . b ∉ bs#} rep p = 0"
    by (simp add: filter_mset_empty_conv point_replication_number_def)
  have "(add_point_to_blocks p bs) rep p = {# (insert p b) | b ∈# ℬ . b ∈ bs#} rep p + {# b ∈# ℬ . b ∉ bs#} rep p"
    by (simp add: add_point_to_blocks_def)
  then have eq: "(add_point_to_blocks p bs) rep p = {# (insert p b) | b ∈# ℬ . b ∈ bs#} rep p"
    using zero by simp
  have "⋀ bl . bl ∈# {# (insert p b) | b ∈# ℬ . b ∈ bs#} ⟹ p ∈ bl" by auto
  then have "{# (insert p b) | b ∈# ℬ . b ∈ bs#} rep p = size {# (insert p b) | b ∈# ℬ . b ∈ bs#}"
    using point_replication_number_def by (metis filter_mset_True filter_mset_cong) 
  thus ?thesis by (simp add: eq) 
qed

lemma add_point_blocks_wf: "incidence_system (add_point p) (add_point_to_blocks p bs)"
  by (unfold_locales) (auto simp add: add_point_def wf_invalid_point add_point_to_blocks_def)

text ‹Basic (weak) delete point operation removes a point from both the point set and from any 
blocks that contain it to maintain wellformed property›
definition del_point :: "'a ⇒ 'a set" where
"del_point p ≡ 𝒱 - {p}" 

definition del_point_blocks:: "'a ⇒ 'a set multiset" where
"del_point_blocks p ≡ {# (bl - {p}) . bl ∈# ℬ #}"

lemma del_point_block_count: "size (del_point_blocks p) = size ℬ"
  by (simp add: del_point_blocks_def)

lemma remove_invalid_point_block: "p ∉ 𝒱 ⟹ bl ∈# ℬ ⟹ bl - {p} = bl"
  using wf_invalid_point by blast

lemma del_invalid_point: "p ∉ 𝒱 ⟹ (del_point p) = 𝒱"
  by (simp add: del_point_def)

lemma del_invalid_point_blocks: "p ∉ 𝒱 ⟹ (del_point_blocks p) = ℬ"
  using del_invalid_point
  by (auto simp add: remove_invalid_point_block del_point_blocks_def) 

lemma delete_point_p_not_in_bl_blocks: "(⋀ bl. bl ∈# ℬ ⟹ p ∉ bl) ⟹ (del_point_blocks p) = ℬ"
  by (simp add: del_point_blocks_def)

lemma delete_point_blocks_wf: "b ∈# (del_point_blocks p) ⟹ b ⊆ 𝒱 - {p}"
  unfolding del_point_blocks_def using wellformed by auto

lemma delete_point_blocks_sub: 
  assumes "b ∈# (del_point_blocks p)" 
  obtains bl where "bl ∈# ℬ ∧ b ⊆ bl"
  using assms by (auto simp add: del_point_blocks_def)

lemma delete_point_split_blocks: "del_point_blocks p = 
  {# bl ∈#ℬ . p ∉ bl#} + {# bl - {p} | bl ∈# ℬ . p ∈ bl#}"
proof -
  have sm: "⋀ bl . p ∉ bl ⟹ bl - {p} = bl" by simp 
  have "del_point_blocks p = {# (bl - {p}) . bl ∈# ℬ #}" by (simp add: del_point_blocks_def)
  also have "... = {# (bl - {p}) | bl ∈# ℬ . p ∉ bl #} + {# (bl - {p}) | bl ∈# ℬ . p ∈ bl #}"
    using multiset_partition by (metis image_mset_union union_commute) 
  finally have "del_point_blocks p = {#bl | bl ∈# ℬ . p ∉ bl#} + 
      {# (bl - {p}) | bl ∈# ℬ . p ∈ bl #}"
    using sm mem_Collect_eq
    by (metis (mono_tags, lifting) Multiset.set_mset_filter  multiset.map_cong) 
  thus ?thesis by simp
qed

lemma delete_point_index_eq: 
  assumes "ps ⊆ (del_point p)"
  shows "(del_point_blocks p) index ps = ℬ index ps"
proof -
  have eq: "filter_mset ((⊆) ps) {#bl - {p}. bl ∈# ℬ#} = 
      image_mset (λ b . b - {p}) (filter_mset (λ b. ps ⊆ b - {p}) ℬ)"
    using filter_mset_image_mset by blast
  have "p ∉ ps" using assms del_point_def by blast 
  then have "⋀ bl . ps ⊆ bl ⟷ ps ⊆ bl - {p}" by blast
  then have "((filter_mset (λ b. ps ⊆ b - {p}) ℬ)) = (filter_mset (λ b . ps ⊆ b) ℬ)" by auto 
  then have "size (image_mset (λ b . b - {p}) (filter_mset (λ b. ps ⊆ b - {p}) ℬ)) 
      = ℬ index ps" 
    by (simp add: points_index_def) 
  thus ?thesis using eq
    by (simp add: del_point_blocks_def points_index_def) 
qed

lemma delete_point_wf: "incidence_system (del_point p) (del_point_blocks p)"
  using delete_point_blocks_wf del_point_def by (unfold_locales) auto

text ‹The concept of a strong delete point comes from hypergraph theory. When a point is deleted, 
any blocks containing it are also deleted›
definition str_del_point_blocks :: "'a ⇒ 'a set multiset" where
"str_del_point_blocks p ≡ {# bl ∈# ℬ . p ∉ bl#}"

lemma str_del_point_blocks_alt: "str_del_point_blocks p = ℬ - {# bl ∈# ℬ . p ∈ bl#}"  
  using add_diff_cancel_left' multiset_partition by (metis str_del_point_blocks_def) 

lemma delete_point_strong_block_in:  "p ∉ bl ⟹ bl ∈# ℬ  ⟹ bl ∈# str_del_point_blocks p"
  by (simp add: str_del_point_blocks_def)

lemma delete_point_strong_block_not_in: "p ∈ bl ⟹ bl ∉# (str_del_point_blocks) p"
  by (simp add: str_del_point_blocks_def)

lemma delete_point_strong_block_in_iff: "bl ∈# ℬ ⟹ bl ∈# str_del_point_blocks p ⟷ p ∉ bl"
  using delete_point_strong_block_in delete_point_strong_block_not_in
  by (simp add: str_del_point_blocks_def)

lemma delete_point_strong_block_subset: "str_del_point_blocks p ⊆# ℬ"
  by (simp add: str_del_point_blocks_def)

lemma delete_point_strong_block_in_orig: "bl ∈# str_del_point_blocks p ⟹ bl ∈# ℬ"
  using delete_point_strong_block_subset by (metis mset_subset_eqD) 

lemma delete_invalid_pt_strong_eq: "p ∉ 𝒱 ⟹ ℬ = str_del_point_blocks p"
  unfolding str_del_point_blocks_def using wf_invalid_point empty_iff
  by (metis Multiset.diff_cancel filter_mset_eq_conv set_mset_empty subset_mset.order_refl)

lemma strong_del_point_index_alt: 
  assumes "ps ⊆ (del_point p)"
  shows "(str_del_point_blocks p) index ps = 
    ℬ index ps - {# bl ∈# ℬ . p ∈ bl#} index ps"
  using str_del_point_blocks_alt points_index_def
  by (metis filter_diff_mset multiset_filter_mono multiset_filter_subset  size_Diff_submset)

lemma strong_del_point_incidence_wf: "incidence_system (del_point p) (str_del_point_blocks p)"
  using wellformed str_del_point_blocks_def del_point_def by (unfold_locales) auto

text ‹Add block operation›

definition add_block :: "'a set ⇒ 'a set multiset" where 
"add_block b ≡ ℬ + {#b#}"

lemma add_block_alt: "add_block b = add_mset b ℬ"
  by (simp add: add_block_def)

lemma add_block_rep_number_in: 
  assumes "x ∈ b"
  shows "(add_block b) rep x = ℬ rep x + 1"
proof -
  have "(add_block b) = {#b#} + ℬ" by (simp add: add_block_def) 
  then have split: "(add_block b) rep x = {#b#} rep x + ℬ rep x"
    by (metis point_rep_number_split)
  have "{#b#} rep x = 1" using assms by simp
  thus ?thesis using split by auto
qed

lemma add_block_rep_number_not_in: "x ∉ b ⟹ (add_block b) rep x = ℬ rep x"
  using point_rep_number_split add_block_alt point_rep_singleton_inval
  by (metis add.right_neutral union_mset_add_mset_right)

lemma add_block_index_in: 
  assumes "ps ⊆ b"
  shows "(add_block b) index ps = ℬ index ps + 1"
proof -
  have "(add_block b) = {#b#} + ℬ" by (simp add: add_block_def) 
  then have split: "(add_block b) index ps = {#b#} index ps + ℬ index ps"
    by (metis point_index_distrib)
  have "{#b#} index ps = 1" using assms points_index_singleton by auto
  thus ?thesis using split by simp
qed

lemma add_block_index_not_in: "¬ (ps ⊆ b) ⟹ (add_block b) index ps = ℬ index ps"
  using point_index_distrib points_index_singleton_zero
  by (metis add.right_neutral add_block_def)

text ‹Note the add block incidence system is defined slightly differently then textbook 
definitions due to the modification to the point set. This ensures the operation is closed, 
where otherwise a condition that $b \subseteq \mathcal{V}$ would be required.›
lemma add_block_wf: "incidence_system (𝒱 ∪ b) (add_block b)"
  using wellformed add_block_def by (unfold_locales) auto

lemma add_block_wf_cond: "b ⊆ 𝒱 ⟹ incidence_system 𝒱 (add_block b)"
  using add_block_wf by (metis sup.order_iff) 

text ‹Delete block removes a block from the block set. The point set is unchanged›
definition del_block :: "'a set ⇒ 'a set multiset" where
"del_block b ≡ ℬ - {#b#}"

lemma delete_block_subset: "(del_block b) ⊆# ℬ"
  by (simp add: del_block_def)

lemma delete_invalid_block_eq: "b ∉# ℬ ⟹ del_block b = ℬ"
  by (simp add: del_block_def)

lemma delete_block_wf: "incidence_system 𝒱 (del_block b)"
  by (unfold_locales) (simp add: del_block_def in_diffD wellformed) 

text ‹The strong delete block operation effectively deletes the block, as well as 
all points in that block›
definition str_del_block :: "'a set ⇒ 'a set multiset" where
"str_del_block b ≡ {# bl - b | bl ∈# ℬ . bl ≠ b #}"

lemma strong_del_block_alt_def: "str_del_block b = {# bl - b . bl ∈# removeAll_mset b ℬ #}"
  by (simp add: filter_mset_neq str_del_block_def)

lemma strong_del_block_wf: "incidence_system (𝒱 - b) (str_del_block b)"
  using wf_invalid_point str_del_block_def by (unfold_locales) auto

lemma str_del_block_del_point: 
  assumes "{x} ∉# ℬ"
  shows "str_del_block {x} = (del_point_blocks x)"
proof -
  have neqx: "⋀ bl. bl ∈# ℬ ⟹ bl ≠ {x}" using assms by auto
  have "str_del_block {x} = {# bl - {x} | bl ∈# ℬ . bl ≠ {x} #}" by (simp add: str_del_block_def)
  then have "str_del_block {x} = {# bl - {x} . bl ∈# ℬ #}" using assms neqx
    by (simp add: filter_mset_cong) 
  thus ?thesis by (simp add: del_point_blocks_def)
qed

subsection ‹Incidence System Interpretations›
text ‹It is easy to interpret all operations as incidence systems in there own right. 
These can then be used to prove local properties on the new constructions, as well 
as reason on interactions between different operation sequences›

interpretation add_point_sys: incidence_system "add_point p" "ℬ"
  using add_point_wf by simp

lemma add_point_sys_rep_numbers: "add_point_sys.replication_numbers p = 
    replication_numbers ∪ {ℬ rep p}"
  using add_point_sys.replication_numbers_def replication_numbers_def add_point_def by auto

interpretation del_point_sys: incidence_system "del_point p" "del_point_blocks p"
  using delete_point_wf by auto

interpretation add_block_sys: incidence_system "𝒱 ∪ bl" "add_block bl"
  using add_block_wf by simp

interpretation del_block_sys: incidence_system "𝒱" "del_block bl"
  using delete_block_wf by simp 

lemma add_del_block_inv: 
  assumes "bl ⊆ 𝒱"
  shows "add_block_sys.del_block bl bl = ℬ"
  using add_block_sys.del_block_def add_block_def by simp

lemma del_add_block_inv: "bl ∈# ℬ ⟹ del_block_sys.add_block bl bl = ℬ"
  using del_block_sys.add_block_def del_block_def wellformed by fastforce

lemma del_invalid_add_block_eq: "bl ∉# ℬ ⟹ del_block_sys.add_block bl bl = add_block bl"
  using del_block_sys.add_block_def by (simp add: delete_invalid_block_eq) 

lemma add_delete_point_inv: 
  assumes "p ∉ 𝒱"
  shows "add_point_sys.del_point p p = 𝒱"
proof -
  have "(add_point_sys.del_point p p) = (insert p 𝒱) - {p}"
    using add_point_sys.del_point_def del_block_sys.add_point_def by auto 
  thus ?thesis 
    by (simp add: assms) 
qed
end

subsection ‹Operation Closure for Designs›

context finite_incidence_system 
begin

lemma add_point_finite: "finite_incidence_system (add_point p) ℬ"
  using add_point_wf finite_sets add_point_def 
  by (unfold_locales) (simp_all add: incidence_system_def)

lemma add_point_to_blocks_finite: "finite_incidence_system (add_point p) (add_point_to_blocks p bs)"
  using add_point_blocks_wf add_point_finite finite_incidence_system.finite_sets 
    incidence_system.finite_sysI by blast

lemma delete_point_finite: 
    "finite_incidence_system (del_point p) (del_point_blocks p)"
  using finite_sets delete_point_wf 
  by (unfold_locales) (simp_all add: incidence_system_def del_point_def)

lemma del_point_order: 
  assumes "p ∈ 𝒱"
  shows "card (del_point p) = 𝗏 - 1"
proof -
  have vg0: "card 𝒱 > 0" using assms finite_sets card_gt_0_iff by auto 
  then have "card (del_point p) = card 𝒱 - 1" using assms del_point_def
    by (metis card_Diff_singleton)
  thus ?thesis
    using vg0 by linarith 
qed

lemma strong_del_point_finite:"finite_incidence_system (del_point p) (str_del_point_blocks p)"
  using strong_del_point_incidence_wf del_point_def
  by (intro_locales) (simp_all add: finite_incidence_system_axioms_def finite_sets)

lemma add_block_fin: "finite b ⟹ finite_incidence_system (𝒱 ∪ b) (add_block b)"
  using wf_invalid_point finite_sets add_block_def by (unfold_locales) auto

lemma add_block_fin_cond: "b ⊆ 𝒱 ⟹ finite_incidence_system 𝒱 (add_block b)"
  using add_block_wf_cond finite_incidence_system_axioms.intro finite_sets
  by (intro_locales) (simp_all)

lemma delete_block_fin_incidence_sys: "finite_incidence_system 𝒱 (del_block b)"
  using delete_block_wf finite_sets by (unfold_locales) (simp_all add: incidence_system_def)

lemma strong_del_block_fin: "finite_incidence_system (𝒱 - b) (str_del_block b)"
  using strong_del_block_wf finite_sets finite_incidence_system_axioms_def by (intro_locales) auto

end

context design
begin
lemma add_point_design: "design (add_point p) ℬ"
  using add_point_wf finite_sets blocks_nempty add_point_def
  by (unfold_locales) (auto simp add: incidence_system_def)

lemma delete_point_design: 
  assumes "(⋀ bl . bl ∈# ℬ ⟹ p ∈ bl ⟹ card bl ≥ 2)"
  shows "design (del_point p) (del_point_blocks p)"
proof (cases "p ∈ 𝒱")
  case True
  interpret fis: finite_incidence_system "(del_point p)" "(del_point_blocks p)" 
    using delete_point_finite by simp
  show ?thesis 
  proof (unfold_locales)
    show "⋀bl. bl ∈# (del_point_blocks p) ⟹ bl ≠ {}" using assms del_point_def 
    proof -
      fix bl 
      assume "bl ∈#(del_point_blocks p)"
      then obtain bl' where block: "bl' ∈# ℬ" and rem: "bl = bl' - {p}" 
        by (auto simp add: del_point_blocks_def)
      then have eq: "p ∉ bl' ⟹ bl ≠ {}" using block blocks_nempty by (simp add: rem) 
      have "p ∈ bl' ⟹ card bl ≥ 1" using rem finite_blocks block assms block by fastforce  
      then show "bl ≠ {}" using  eq assms by fastforce 
    qed 
  qed
next
  case False
  then show ?thesis using del_invalid_point del_invalid_point_blocks
    by (simp add: wf_design) 
qed

lemma strong_del_point_design: "design (del_point p) (str_del_point_blocks p)"
proof -
  interpret fin: finite_incidence_system "(del_point p)" "(str_del_point_blocks p)"
    using strong_del_point_finite by simp
  show ?thesis using wf_design wf_design_iff del_point_def str_del_point_blocks_def 
    by (unfold_locales) (auto)
qed

lemma add_block_design: 
  assumes "finite bl" 
  assumes "bl ≠ {}" 
  shows "design (𝒱 ∪ bl) (add_block bl)"
proof - 
  interpret fin: finite_incidence_system "(𝒱 ∪ bl)" "(add_block bl)" 
    using add_block_fin assms by simp
  show ?thesis using blocks_nempty assms add_block_def by (unfold_locales) auto
qed

lemma add_block_design_cond: 
  assumes "bl ⊆ 𝒱" and "bl ≠ {}"
  shows "design 𝒱 (add_block bl)"
proof -
  interpret fin: finite_incidence_system "𝒱" "(add_block bl)" 
    using add_block_fin_cond assms by simp
  show ?thesis using blocks_nempty assms add_block_def by (unfold_locales) auto
qed

lemma delete_block_design: "design 𝒱 (del_block bl)"
proof -
  interpret fin: finite_incidence_system 𝒱 "(del_block bl)" 
    using delete_block_fin_incidence_sys by simp
  have "⋀ b . b ∈# (del_block bl) ⟹ b ≠ {}"
    using blocks_nempty delete_block_subset by blast  
  then show ?thesis by (unfold_locales) (simp_all)
qed

lemma strong_del_block_des: 
  assumes "⋀ bl . bl ∈# ℬ ⟹ ¬ (bl ⊂ b)"
  shows "design (𝒱 - b) (str_del_block b)"
proof -
  interpret fin: finite_incidence_system "𝒱 - b" "(str_del_block b)"
    using strong_del_block_fin by simp
  show ?thesis using assms str_del_block_def by (unfold_locales) auto
qed

end

context proper_design
begin
lemma delete_point_proper: 
  assumes "⋀bl. bl ∈# ℬ ⟹ p ∈ bl ⟹ 2 ≤ card bl"
  shows "proper_design (del_point p) (del_point_blocks p)"
proof -
  interpret des: design "del_point p" "del_point_blocks p"
    using delete_point_design assms by blast 
  show ?thesis using design_blocks_nempty del_point_def del_point_blocks_def 
    by (unfold_locales) simp
qed

lemma strong_delete_point_proper: 
  assumes "⋀bl. bl ∈# ℬ ⟹ p ∈ bl ⟹ 2 ≤ card bl"
  assumes "ℬ rep p < 𝖻"
  shows "proper_design (del_point p) (str_del_point_blocks p)"
proof -
  interpret des: design "del_point p" "str_del_point_blocks p"
    using strong_del_point_design assms by blast 
  show ?thesis using assms design_blocks_nempty point_rep_num_inv_non_empty 
    str_del_point_blocks_def del_point_def by (unfold_locales) simp
qed

end

subsection ‹Combining Set Systems›
text ‹Similar to multiple, another way to construct a new set system is to combine two existing ones.
We introduce a new locale enabling us to reason on two different incidence systems›
locale two_set_systems = sys1: incidence_system 𝒱 ℬ + sys2: incidence_system 𝒱' ℬ'
  for 𝒱 :: "('a set)" and ℬ and 𝒱' :: "('a set)" and ℬ'
begin 

abbreviation "combine_points ≡ 𝒱 ∪ 𝒱'" 

notation combine_points (‹𝒱⇧+›)

abbreviation "combine_blocks ≡ ℬ + ℬ'"

notation combine_blocks (‹ℬ⇧+›)

sublocale combine_sys: incidence_system "𝒱⇧+" "ℬ⇧+"
  using sys1.wellformed sys2.wellformed by (unfold_locales) auto

lemma combine_points_index: "ℬ⇧+ index ps = ℬ index ps  + ℬ' index ps"
  by (simp add: point_index_distrib)

lemma combine_rep_number: "ℬ⇧+ rep x = ℬ rep x + ℬ' rep x"
  by (simp add: point_replication_number_def)

lemma combine_multiple1: "𝒱 = 𝒱' ⟹ ℬ = ℬ' ⟹ ℬ⇧+ = sys1.multiple_blocks 2"
  by auto

lemma combine_multiple2: "𝒱 = 𝒱' ⟹ ℬ = ℬ' ⟹ ℬ⇧+ = sys2.multiple_blocks 2"
  by auto

lemma combine_multiplicity: "combine_sys.multiplicity b = sys1.multiplicity b + sys2.multiplicity b"
  by simp

lemma combine_block_sizes: "combine_sys.sys_block_sizes = 
    sys1.sys_block_sizes ∪ sys2.sys_block_sizes"
  using sys1.sys_block_sizes_def sys2.sys_block_sizes_def combine_sys.sys_block_sizes_def by (auto)

end

locale two_fin_set_systems = two_set_systems 𝒱 ℬ 𝒱' ℬ' + sys1: finite_incidence_system 𝒱 ℬ + 
  sys2: finite_incidence_system 𝒱' ℬ' for 𝒱 ℬ 𝒱' ℬ'
begin
  

sublocale combine_fin_sys: finite_incidence_system "𝒱⇧+" "ℬ⇧+"
  using sys1.finite_sets sys2.finite_sets by (unfold_locales) (simp)

lemma combine_order: "card (𝒱⇧+) ≥ card 𝒱"
  by (meson Un_upper1 card_mono combine_fin_sys.finite_sets)

lemma  combine_order_2: "card (𝒱⇧+) ≥ card 𝒱'"
  by (meson Un_upper2 card_mono combine_fin_sys.finite_sets) 

end

locale two_designs = two_fin_set_systems 𝒱 ℬ 𝒱' ℬ' + des1: design 𝒱 ℬ + 
  des2: design 𝒱' ℬ' for 𝒱 ℬ 𝒱' ℬ'
begin

sublocale combine_des: design "𝒱⇧+" "ℬ⇧+"
  apply (unfold_locales)
  using des1.blocks_nempty_alt des2.blocks_nempty_alt by fastforce

end

locale two_designs_proper = two_designs + 
  assumes blocks_nempty: "ℬ ≠ {#} ∨ ℬ' ≠ {#}"
begin

lemma des1_is_proper: "ℬ ≠ {#} ⟹ proper_design 𝒱 ℬ"
  by (unfold_locales) (simp)

lemma des2_is_proper: "ℬ' ≠ {#} ⟹ proper_design 𝒱' ℬ'"
  by (unfold_locales) (simp)

lemma min_one_proper_design: "proper_design 𝒱 ℬ ∨ proper_design 𝒱' ℬ'"
  using blocks_nempty des1_is_proper des2_is_proper by (unfold_locales, blast)

sublocale combine_proper_des: proper_design "𝒱⇧+" "ℬ⇧+"
  apply (unfold_locales)
  by (metis blocks_nempty size_eq_0_iff_empty subset_mset.zero_eq_add_iff_both_eq_0)
end

end