# 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 𝒱"

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#}"

image_mset (insert p) (filter_mset (λ b . b ∈ bs) ℬ) + (filter_mset (λ b . b ∉ bs) ℬ)"

assumes "(⋀ bl . bl ∈ bs ⟹ p ∈ bl)"
shows "add_point_to_blocks p bs = ℬ"
have "image_mset (insert p) {#b ∈# ℬ. b ∈ bs#} = {#b ∈# ℬ. b ∈ bs#}" using assms
thus "image_mset (insert p) {#b ∈# ℬ. b ∈ bs#} + {#b ∈# ℬ. b ∉ bs#} = ℬ"
using multiset_partition by simp
qed

assumes "p ∉ 𝒱"
shows "(add_point_to_blocks p bs) rep p = size {#b ∈# ℬ . b ∈ bs#}"
proof -
have "⋀ b. b ∈# ℬ ⟹ b ∉ bs ⟹ p ∉ b"
then have zero: "{# b ∈# ℬ . b ∉ bs#} rep p = 0"
have "(add_point_to_blocks p bs) rep p = {# (insert p b) | b ∈# ℬ . b ∈ bs#} rep p + {# b ∈# ℬ . b ∉ bs#} rep p"
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

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 ℬ"

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

lemma del_invalid_point: "p ∉ 𝒱 ⟹ (del_point p) = 𝒱"

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) = ℬ"

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"
thus ?thesis using eq
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"

lemma delete_point_strong_block_not_in: "p ∈ bl ⟹ bl ∉# (str_del_point_blocks) p"

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

lemma delete_point_strong_block_subset: "str_del_point_blocks p ⊆# ℬ"

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

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

assumes "x ∈ b"
shows "(add_block b) rep x = ℬ rep x + 1"
proof -
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"

assumes "ps ⊆ b"
shows "(add_block b) index ps = ℬ index ps + 1"
proof -
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

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.›
using wellformed add_block_def by (unfold_locales) auto

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) ⊆# ℬ"

lemma delete_invalid_block_eq: "b ∉# ℬ ⟹ del_block b = ℬ"

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 ℬ #}"

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
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›

replication_numbers ∪ {ℬ rep p}"

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

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

assumes "bl ⊆ 𝒱"
shows "add_block_sys.del_block bl bl = ℬ"

using del_block_sys.add_block_def del_block_def wellformed by fastforce

assumes "p ∉ 𝒱"
shows "add_point_sys.del_point p p = 𝒱"
proof -
have "(add_point_sys.del_point p p) = (insert p 𝒱) - {p}"
thus ?thesis
qed
end

subsection ‹Operation Closure for Designs›

context finite_incidence_system
begin

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)

using wf_invalid_point finite_sets add_block_def by (unfold_locales) auto

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
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}"
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
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

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

assumes "bl ⊆ 𝒱" and "bl ≠ {}"
proof -
interpret fin: finite_incidence_system "𝒱" "(add_block bl)"
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"

lemma combine_rep_number: "ℬ⇧+ rep x = ℬ rep x + ℬ' rep x"

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)
end