Theory Design_Theory.Sub_Designs
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"
by (simp add: mset_subset_eq_count blocks_subset)
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
by (unfold_locales) (simp_all add: incidence_system.wellformed)
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 𝒰 𝒜 𝒱 ℬ"
by (simp add: sub_ssI incidence_system_axioms)
lemma sub_inc_sysI[intro]: "incidence_system 𝒰 𝒜 ⟹ 𝒰 ⊆ 𝒱 ⟹ 𝒜 ⊆# ℬ ⟹
sub_incidence_system 𝒰 𝒜 𝒱 ℬ"
by (simp add: sub_incidence_system.intro sub_set_sysI)
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
lemma add_point_sub_sys: "sub_incidence_system 𝒱 ℬ (add_point p) ℬ"
using add_point_wf add_point_def
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 add_block_sub_sys: "sub_incidence_system 𝒱 ℬ (𝒱 ∪ b) (add_block b)"
using add_block_wf wf_invalid_point add_block_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 𝒰 𝒜 𝒱 ℬ"
by (simp add: sub_design.intro wf_design)
lemma sub_designII [intro]: "design 𝒰 𝒜 ⟹ sub_incidence_system 𝒱 ℬ 𝒰 𝒜 ⟹ sub_design 𝒱 ℬ 𝒰 𝒜"
by (simp add: sub_design_def)
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 add_point_sub_des: "sub_design 𝒱 ℬ (add_point p) ℬ"
using add_point_design add_point_sub_sys sub_design.intro by fastforce
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)"
using add_block_sub_sys add_block_design sub_designII by fastforce
lemma delete_block_sub_des: "sub_design 𝒱 (del_block b) 𝒱 ℬ "
using delete_block_design delete_block_sub_sys sub_designI by auto
end
lemma (in two_designs) combine_sub_des: "sub_design 𝒱 ℬ 𝒱⇧+ ℬ⇧+"
by (unfold_locales) (simp_all)
lemma (in two_designs) combine_sub_des_alt: "sub_design 𝒱' ℬ' 𝒱⇧+ ℬ⇧+"
by (unfold_locales) (simp_all)
end