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