Theory Sub_Designs

```(* Title: Sub_Designs.thy
Author: Chelsea Edmonds
*)

section ‹Sub-designs›
text ‹Sub designs are a relationship between two designs using the subset and submultiset relations
This theory defines the concept at the incidence system level, before extending to defining on
well defined designs›

theory Sub_Designs imports Design_Operations
begin

subsection ‹Sub-system and Sub-design Locales›
locale sub_set_system = incidence_system 𝒱 ℬ
for "𝒰" and "𝒜" and "𝒱" and "ℬ" +
assumes points_subset: "𝒰 ⊆ 𝒱"
assumes blocks_subset: "𝒜 ⊆# ℬ"
begin

lemma sub_points: "x ∈ 𝒰 ⟹ x ∈ 𝒱"
using points_subset by auto

lemma sub_blocks: "bl ∈# 𝒜 ⟹ bl ∈# ℬ"
using blocks_subset by auto

lemma sub_blocks_count: "count 𝒜 b ≤ count ℬ b"

end

locale sub_incidence_system = sub_set_system + ins: incidence_system 𝒰 𝒜

locale sub_design = sub_incidence_system + des: design 𝒱 ℬ
begin

lemma sub_non_empty_blocks: "A ∈# 𝒜 ⟹ A ≠ {}"
using des.blocks_nempty sub_blocks by simp

sublocale sub_des: design 𝒰 𝒜
using des.finite_sets finite_subset points_subset sub_non_empty_blocks
by (unfold_locales) (auto)

end

locale proper_sub_set_system = incidence_system 𝒱 ℬ
for "𝒰" and "𝒜" and "𝒱" and "ℬ" +
assumes points_psubset: "𝒰 ⊂ 𝒱"
assumes blocks_subset: "𝒜 ⊆# ℬ"
begin

lemma point_sets_ne: "𝒰 ≠ 𝒱"
using points_psubset by auto

end

sublocale proper_sub_set_system ⊆ sub_set_system
using points_psubset blocks_subset by (unfold_locales) simp_all

context sub_set_system
begin

lemma sub_is_proper: "𝒰 ≠ 𝒱 ⟹ proper_sub_set_system 𝒰 𝒜 𝒱 ℬ"
using blocks_subset incidence_system_axioms
by (simp add: points_subset proper_sub_set_system.intro proper_sub_set_system_axioms_def psubsetI)

end

locale proper_sub_incidence_system = proper_sub_set_system + ins: incidence_system 𝒰 𝒜

sublocale proper_sub_incidence_system ⊆ sub_incidence_system
by (unfold_locales)

context sub_incidence_system
begin
lemma sub_is_proper: "𝒰 ≠ 𝒱 ⟹ proper_sub_incidence_system 𝒰 𝒜 𝒱 ℬ"
by (simp add: ins.incidence_system_axioms proper_sub_incidence_system_def sub_is_proper)

end

locale proper_sub_design = proper_sub_incidence_system + des: design 𝒱 ℬ

sublocale proper_sub_design ⊆ sub_design
by (unfold_locales)

context sub_design
begin
lemma sub_is_proper: "𝒰 ≠ 𝒱 ⟹ proper_sub_design 𝒰 𝒜 𝒱 ℬ"
by (simp add: des.wf_design proper_sub_design.intro sub_is_proper)

end

lemma ss_proper_implies_sub [intro]: "proper_sub_set_system 𝒰 𝒜 𝒱 ℬ ⟹ sub_set_system 𝒰 𝒜 𝒱 ℬ"
using proper_sub_set_system.axioms(1) proper_sub_set_system.blocks_subset psubsetE
by (metis proper_sub_set_system.points_psubset sub_set_system.intro sub_set_system_axioms_def)

lemma sub_ssI [intro!]: "incidence_system 𝒱 ℬ ⟹ 𝒰 ⊆ 𝒱 ⟹ 𝒜 ⊆# ℬ ⟹ sub_set_system 𝒰 𝒜 𝒱 ℬ"
using incidence_system_def subset_iff

lemma sub_ss_equality:
assumes "sub_set_system 𝒰 𝒜 𝒱 ℬ"
and "sub_set_system 𝒱 ℬ 𝒰 𝒜"
shows "𝒰 = 𝒱" and "𝒜 = ℬ"
using assms(1) assms(2) sub_set_system.points_subset apply blast
by (meson assms(1) assms(2) sub_set_system.blocks_subset subset_mset.eq_iff)

subsection ‹Reasoning on Sub-designs›

subsubsection ‹Reasoning on Incidence Sys property relationships›

context sub_incidence_system
begin

lemma sub_sys_block_sizes: "ins.sys_block_sizes ⊆ sys_block_sizes"
by (auto simp add: sys_block_sizes_def ins.sys_block_sizes_def blocks_subset sub_blocks)

lemma sub_point_rep_number_le: "x ∈ 𝒰 ⟹ 𝒜 rep x ≤ ℬ rep x"
by (simp add: point_replication_number_def blocks_subset multiset_filter_mono size_mset_mono)

lemma sub_point_index_le: "ps ⊆ 𝒰 ⟹ 𝒜 index ps ≤ ℬ index ps"
by (simp add: points_index_def blocks_subset multiset_filter_mono size_mset_mono)

lemma sub_sys_intersection_numbers: "ins.intersection_numbers ⊆ intersection_numbers"
apply (auto simp add: intersection_numbers_def ins.intersection_numbers_def)
by (metis blocks_subset insert_DiffM insert_subset_eq_iff)

end

subsubsection ‹Reasoning on Incidence Sys/Design operations›
context incidence_system
begin

lemma sub_set_sysI[intro]: "𝒰 ⊆ 𝒱 ⟹ 𝒜 ⊆# ℬ ⟹ sub_set_system 𝒰 𝒜 𝒱 ℬ"

lemma sub_inc_sysI[intro]: "incidence_system 𝒰 𝒜 ⟹ 𝒰 ⊆ 𝒱 ⟹ 𝒜 ⊆# ℬ ⟹
sub_incidence_system 𝒰 𝒜 𝒱 ℬ"

lemma multiple_orig_sub_system:
assumes "n > 0"
shows "sub_incidence_system 𝒱 ℬ 𝒱 (multiple_blocks n)"
using multiple_block_in_original wellformed multiple_blocks_sub assms
by (unfold_locales) simp_all

by (simp add: sub_ssI subset_insertI incidence_system_axioms sub_incidence_system.intro)

lemma strong_del_point_sub_sys: "sub_incidence_system (del_point p) (str_del_point_blocks p) 𝒱 ℬ "
using strong_del_point_incidence_wf wf_invalid_point del_point_def str_del_point_blocks_def
by (unfold_locales) (auto)

lemma delete_block_sub_sys: "sub_incidence_system 𝒱 (del_block b)  𝒱 ℬ "
using delete_block_wf delete_block_subset incidence_system_def by (unfold_locales, auto)

end

lemma (in two_set_systems) combine_sub_sys: "sub_incidence_system 𝒱 ℬ 𝒱⇧+ ℬ⇧+"
by (unfold_locales) (simp_all)

lemma (in two_set_systems) combine_sub_sys_alt: "sub_incidence_system 𝒱' ℬ' 𝒱⇧+ ℬ⇧+"
by (unfold_locales) (simp_all)

context design
begin

lemma sub_designI [intro]: "design 𝒰 𝒜 ⟹ sub_incidence_system 𝒰 𝒜 𝒱 ℬ ⟹ sub_design 𝒰 𝒜 𝒱 ℬ"

lemma sub_designII [intro]: "design 𝒰 𝒜 ⟹ sub_incidence_system 𝒱 ℬ 𝒰 𝒜 ⟹ sub_design 𝒱 ℬ 𝒰 𝒜"

lemma multiple_orig_sub_des:
assumes "n > 0"
shows "sub_design 𝒱 ℬ 𝒱 (multiple_blocks n)"
using multiple_is_design assms multiple_orig_sub_system by (simp add: sub_design.intro)

lemma strong_del_point_sub_des: "sub_design (del_point p) (str_del_point_blocks p) 𝒱 ℬ "
using strong_del_point_sub_sys sub_design.intro wf_design by blast

lemma add_block_sub_des: "finite b ⟹ b ≠ {} ⟹ sub_design 𝒱 ℬ (𝒱 ∪ b) (add_block b)"