Theory Design_Isomorphisms
section ‹Design Isomorphisms›
theory Design_Isomorphisms imports Design_Basics Sub_Designs
begin
subsection ‹Images of Set Systems›
text ‹We loosely define the concept of taking the "image" of a set system, as done in isomorphisms.
Note that this is not based off mathematical theory, but is for ease of notation›
definition blocks_image :: "'a set multiset ⇒ ('a ⇒ 'b) ⇒ 'b set multiset" where
"blocks_image B f ≡ image_mset ((`) f) B"
lemma image_block_set_constant_size: "size (B) = size (blocks_image B f)"
by (simp add: blocks_image_def)
lemma (in incidence_system) image_set_system_wellformed:
"incidence_system (f ` 𝒱) (blocks_image ℬ f)"
by (unfold_locales, auto simp add: blocks_image_def) (meson image_eqI wf_invalid_point)
lemma (in finite_incidence_system) image_set_system_finite:
"finite_incidence_system (f ` 𝒱) (blocks_image ℬ f)"
using image_set_system_wellformed finite_sets
by (intro_locales) (simp_all add: blocks_image_def finite_incidence_system_axioms.intro)
subsection ‹Incidence System Isomorphisms›
text ‹Isomorphism's are defined by the Handbook of Combinatorial Designs
\<^cite>‹"colbournHandbookCombinatorialDesigns2007"››
locale incidence_system_isomorphism = source: incidence_system 𝒱 ℬ + target: incidence_system 𝒱' ℬ'
for "𝒱" and "ℬ" and "𝒱'" and "ℬ'" + fixes bij_map ("π")
assumes bij: "bij_betw π 𝒱 𝒱'"
assumes block_img: "image_mset ((`) π) ℬ = ℬ'"
begin
lemma iso_eq_order: "card 𝒱 = card 𝒱'"
using bij bij_betw_same_card by auto
lemma iso_eq_block_num: "size ℬ = size ℬ'"
using block_img by (metis size_image_mset)
lemma iso_block_img_alt_rep: "{# π ` bl . bl ∈# ℬ#} = ℬ'"
using block_img by simp
lemma inv_iso_block_img: "image_mset ((`) (inv_into 𝒱 π)) ℬ' = ℬ"
proof -
have "⋀ x. x ∈ 𝒱 ⟹ ((inv_into 𝒱 π) ∘ π) x = x"
using bij bij_betw_inv_into_left comp_apply by fastforce
then have "⋀ bl x . bl ∈# ℬ ⟹ x ∈ bl ⟹ ((inv_into 𝒱 π) ∘ π) x = x"
using source.wellformed by blast
then have img: "⋀ bl . bl ∈# ℬ ⟹ image ((inv_into 𝒱 π) ∘ π) bl = bl"
by simp
have "image_mset ((`) (inv_into 𝒱 π)) ℬ' = image_mset ((`) (inv_into 𝒱 π)) (image_mset ((`) π) ℬ)"
using block_img by simp
then have "image_mset ((`) (inv_into 𝒱 π)) ℬ' = image_mset ((`) ((inv_into 𝒱 π) ∘ π)) ℬ"
by (metis (no_types, opaque_lifting) block_img comp_apply image_comp multiset.map_comp multiset.map_cong0)
thus ?thesis using img by simp
qed
lemma inverse_incidence_sys_iso: "incidence_system_isomorphism 𝒱' ℬ' 𝒱 ℬ (inv_into 𝒱 π)"
using bij bij_betw_inv_into inv_iso_block_img by (unfold_locales) simp
lemma iso_points_map: "π ` 𝒱 = 𝒱'"
using bij by (simp add: bij_betw_imp_surj_on)
lemma iso_points_inv_map: "(inv_into 𝒱 π) ` 𝒱' = 𝒱"
using incidence_system_isomorphism.iso_points_map inverse_incidence_sys_iso by blast
lemma iso_points_ss_card:
assumes "ps ⊆ 𝒱"
shows "card ps = card (π ` ps)"
using assms bij bij_betw_same_card bij_betw_subset by blast
lemma iso_block_in: "bl ∈# ℬ ⟹ (π ` bl) ∈# ℬ'"
using iso_block_img_alt_rep
by (metis image_eqI in_image_mset)
lemma iso_inv_block_in: "x ∈# ℬ' ⟹ x ∈ (`) π ` set_mset ℬ"
by (metis block_img in_image_mset)
lemma iso_img_block_orig_exists: "x ∈# ℬ' ⟹ ∃ bl . bl ∈# ℬ ∧ x = π ` bl"
using iso_inv_block_in by blast
lemma iso_blocks_map_inj: "x ∈# ℬ ⟹ y ∈# ℬ ⟹ π ` x = π ` y ⟹ x = y"
using image_inv_into_cancel incidence_system.wellformed iso_points_inv_map iso_points_map
by (metis (no_types, lifting) source.incidence_system_axioms subset_image_iff)
lemma iso_bij_betwn_block_sets: "bij_betw ((`) π) (set_mset ℬ) (set_mset ℬ')"
apply ( simp add: bij_betw_def inj_on_def)
using iso_block_in iso_inv_block_in iso_blocks_map_inj by auto
lemma iso_bij_betwn_block_sets_inv: "bij_betw ((`) (inv_into 𝒱 π)) (set_mset ℬ') (set_mset ℬ)"
using incidence_system_isomorphism.iso_bij_betwn_block_sets inverse_incidence_sys_iso by blast
lemma iso_bij_betw_individual_blocks: "bl ∈# ℬ ⟹ bij_betw π bl (π ` bl)"
using bij bij_betw_subset source.wellformed by blast
lemma iso_bij_betw_individual_blocks_inv: "bl ∈# ℬ ⟹ bij_betw (inv_into 𝒱 π) (π ` bl) bl"
using bij bij_betw_subset source.wellformed bij_betw_inv_into_subset by fastforce
lemma iso_bij_betw_individual_blocks_inv_alt:
"bl ∈# ℬ' ⟹ bij_betw (inv_into 𝒱 π) bl ((inv_into 𝒱 π) ` bl)"
using incidence_system_isomorphism.iso_bij_betw_individual_blocks inverse_incidence_sys_iso
by blast
lemma iso_inv_block_in_alt: "(π ` bl) ∈# ℬ' ⟹ bl ⊆ 𝒱 ⟹ bl ∈# ℬ"
using image_eqI image_inv_into_cancel inv_iso_block_img iso_points_inv_map
by (metis (no_types, lifting) iso_points_map multiset.set_map subset_image_iff)
lemma iso_img_block_not_in:
assumes "x ∉# ℬ"
assumes "x ⊆ 𝒱"
shows "(π ` x) ∉# ℬ'"
proof (rule ccontr)
assume a: "¬ π ` x ∉# ℬ'"
then have a: "π ` x ∈# ℬ'" by simp
then have "⋀ y . y ∈ (π ` x) ⟹ (inv_into 𝒱 π) y ∈ 𝒱"
using target.wf_invalid_point iso_points_inv_map by auto
then have "((`) (inv_into 𝒱 π)) (π ` x) ∈# ℬ"
using iso_bij_betwn_block_sets_inv by (meson a bij_betw_apply)
thus False
using a assms(1) assms(2) iso_inv_block_in_alt by blast
qed
lemma iso_block_multiplicity:
assumes "bl ⊆ 𝒱"
shows "source.multiplicity bl = target.multiplicity (π ` bl)"
proof (cases "bl ∈# ℬ")
case True
have "inj_on ((`) π) (set_mset ℬ)"
using bij_betw_imp_inj_on iso_bij_betwn_block_sets by auto
then have "count ℬ bl = count ℬ' (π ` bl)"
using count_image_mset_le_count_inj_on count_image_mset_ge_count True block_img inv_into_f_f
less_le_not_le order.not_eq_order_implies_strict by metis
thus ?thesis by simp
next
case False
have s_mult: "source.multiplicity bl = 0"
by (simp add: False count_eq_zero_iff)
then have "target.multiplicity (π ` bl) = 0"
using False count_inI iso_inv_block_in_alt
by (metis assms)
thus ?thesis
using s_mult by simp
qed
lemma iso_point_in_block_img_iff: "p ∈ 𝒱 ⟹ bl ∈# ℬ ⟹ p ∈ bl ⟷ (π p) ∈ (π ` bl)"
by (metis bij bij_betw_imp_surj_on iso_bij_betw_individual_blocks_inv bij_betw_inv_into_left imageI)
lemma iso_point_subset_block_iff: "p ⊆ 𝒱 ⟹ bl ∈# ℬ ⟹ p ⊆ bl ⟷ (π ` p) ⊆ (π ` bl)"
apply auto
using image_subset_iff iso_point_in_block_img_iff subset_iff by metis
lemma iso_is_image_block: "ℬ' = blocks_image ℬ π"
unfolding blocks_image_def by (simp add: block_img iso_points_map)
end
subsection ‹Design Isomorphisms›
text ‹Apply the concept of isomorphisms to designs only›
locale design_isomorphism = incidence_system_isomorphism 𝒱 ℬ 𝒱' ℬ' π + source: design 𝒱 ℬ +
target: design 𝒱' ℬ' for 𝒱 and ℬ and 𝒱' and ℬ' and bij_map ("π")
context design_isomorphism
begin
lemma inverse_design_isomorphism: "design_isomorphism 𝒱' ℬ' 𝒱 ℬ (inv_into 𝒱 π)"
using inverse_incidence_sys_iso source.wf_design target.wf_design
by (simp add: design_isomorphism.intro)
end
subsubsection ‹Isomorphism Operation›
text ‹Define the concept of isomorphic designs outside the scope of locale›
definition isomorphic_designs (infixl "≅⇩D" 50) where
"𝒟 ≅⇩D 𝒟' ⟷ (∃ π . design_isomorphism (fst 𝒟) (snd 𝒟) (fst 𝒟') (snd 𝒟') π)"
lemma isomorphic_designs_symmetric: "(𝒱, ℬ) ≅⇩D (𝒱', ℬ') ⟹ (𝒱', ℬ') ≅⇩D (𝒱, ℬ)"
using isomorphic_designs_def design_isomorphism.inverse_design_isomorphism
by metis
lemma isomorphic_designs_implies_bij: "(𝒱, ℬ) ≅⇩D (𝒱', ℬ') ⟹ ∃ π . bij_betw π 𝒱 𝒱'"
using incidence_system_isomorphism.bij isomorphic_designs_def
by (metis design_isomorphism.axioms(1) fst_conv)
lemma isomorphic_designs_implies_block_map: "(𝒱, ℬ) ≅⇩D (𝒱', ℬ') ⟹ ∃ π . image_mset ((`) π) ℬ = ℬ'"
using incidence_system_isomorphism.block_img isomorphic_designs_def
using design_isomorphism.axioms(1) by fastforce
context design
begin
lemma isomorphic_designsI [intro]: "design 𝒱' ℬ' ⟹ bij_betw π 𝒱 𝒱' ⟹ image_mset ((`) π) ℬ = ℬ'
⟹ (𝒱, ℬ) ≅⇩D (𝒱', ℬ')"
using design_isomorphism.intro isomorphic_designs_def wf_design image_set_system_wellformed
by (metis bij_betw_imp_surj_on blocks_image_def fst_conv incidence_system_axioms
incidence_system_isomorphism.intro incidence_system_isomorphism_axioms_def snd_conv)
lemma eq_designs_isomorphic:
assumes "𝒱 = 𝒱'"
assumes "ℬ = ℬ'"
shows "(𝒱, ℬ) ≅⇩D (𝒱', ℬ')"
proof -
interpret d1: design 𝒱 ℬ using assms
using wf_design by auto
interpret d2: design 𝒱' ℬ' using assms
using wf_design by blast
have "design_isomorphism 𝒱 ℬ 𝒱' ℬ' id" using assms by (unfold_locales) simp_all
thus ?thesis unfolding isomorphic_designs_def by auto
qed
end
context design_isomorphism
begin
subsubsection ‹Design Properties/Operations under Isomorphism›
lemma design_iso_point_rep_num_eq:
assumes "p ∈ 𝒱"
shows "ℬ rep p = ℬ' rep (π p)"
proof -
have "{#b ∈# ℬ . p ∈ b#} = {#b ∈# ℬ . π p ∈ π ` b#}"
using assms filter_mset_cong iso_point_in_block_img_iff assms by force
then have "{#b ∈# ℬ' . π p ∈ b#} = image_mset ((`) π) {#b ∈# ℬ . p ∈ b#}"
by (simp add: image_mset_filter_swap block_img)
thus ?thesis
by (simp add: point_replication_number_def)
qed
lemma design_iso_rep_numbers_eq: "source.replication_numbers = target.replication_numbers"
apply (simp add: source.replication_numbers_def target.replication_numbers_def)
using design_iso_point_rep_num_eq design_isomorphism.design_iso_point_rep_num_eq iso_points_map
by (metis (no_types, lifting) inverse_design_isomorphism iso_points_inv_map rev_image_eqI)
lemma design_iso_block_size_eq: "bl ∈# ℬ ⟹ card bl = card (π ` bl)"
using card_image_le finite_subset_image image_inv_into_cancel
by (metis iso_points_inv_map iso_points_map le_antisym source.finite_blocks source.wellformed)
lemma design_iso_block_sizes_eq: "source.sys_block_sizes = target.sys_block_sizes"
apply (simp add: source.sys_block_sizes_def target.sys_block_sizes_def)
by (metis (no_types, lifting) design_iso_block_size_eq iso_block_in iso_img_block_orig_exists)
lemma design_iso_points_index_eq:
assumes "ps ⊆ 𝒱"
shows "ℬ index ps = ℬ' index (π ` ps)"
proof -
have "⋀ b . b ∈# ℬ ⟹ ((ps ⊆ b) = ((π ` ps) ⊆ π ` b))"
using iso_point_subset_block_iff assms by blast
then have "{#b ∈# ℬ . ps ⊆ b#} = {#b ∈# ℬ . (π ` ps) ⊆ (π ` b)#}"
using assms filter_mset_cong by force
then have "{#b ∈# ℬ' . π ` ps ⊆ b#} = image_mset ((`) π) {#b ∈# ℬ . ps ⊆ b#}"
by (simp add: image_mset_filter_swap block_img)
thus ?thesis
by (simp add: points_index_def)
qed
lemma design_iso_points_indices_imp:
assumes "x ∈ source.point_indices t"
shows "x ∈ target.point_indices t"
proof -
obtain ps where t: "card ps = t" and ss: "ps ⊆ 𝒱" and x: "ℬ index ps = x" using assms
by (auto simp add: source.point_indices_def)
then have x_val: "x = ℬ' index (π ` ps)" using design_iso_points_index_eq by auto
have x_img: " (π ` ps) ⊆ 𝒱'"
using ss bij iso_points_map by fastforce
then have "card (π ` ps) = t" using t ss iso_points_ss_card by auto
then show ?thesis using target.point_indices_elem_in x_img x_val by blast
qed
lemma design_iso_points_indices_eq: "source.point_indices t = target.point_indices t"
using inverse_design_isomorphism design_isomorphism.design_iso_points_indices_imp
design_iso_points_indices_imp by blast
lemma design_iso_block_intersect_num_eq:
assumes "b1 ∈# ℬ"
assumes "b2 ∈# ℬ"
shows "b1 |∩| b2 = (π ` b1) |∩| (π ` b2)"
proof -
have split: "π ` (b1 ∩ b2) = (π ` b1) ∩ (π ` b2)" using assms bij bij_betw_inter_subsets
by (metis source.wellformed)
thus ?thesis using source.wellformed
by (simp add: intersection_number_def iso_points_ss_card split assms(2) inf.coboundedI2)
qed
lemma design_iso_inter_numbers_imp:
assumes "x ∈ source.intersection_numbers"
shows "x ∈ target.intersection_numbers"
proof -
obtain b1 b2 where 1: "b1 ∈# ℬ" and 2: "b2 ∈# (remove1_mset b1 ℬ)" and xval: "x = b1 |∩| b2"
using assms by (auto simp add: source.intersection_numbers_def)
then have pi1: "π ` b1 ∈# ℬ'" by (simp add: iso_block_in)
have pi2: "π ` b2 ∈# (remove1_mset (π ` b1) ℬ')" using iso_block_in 2
by (metis (no_types, lifting) "1" block_img image_mset_remove1_mset_if in_remove1_mset_neq
iso_blocks_map_inj more_than_one_mset_mset_diff multiset.set_map)
have "x = (π ` b1) |∩| (π ` b2)" using 1 2 design_iso_block_intersect_num_eq
by (metis in_diffD xval)
then have "x ∈ {b1 |∩| b2 | b1 b2 . b1 ∈# ℬ' ∧ b2 ∈# (ℬ' - {#b1#})}"
using pi1 pi2 by blast
then show ?thesis by (simp add: target.intersection_numbers_def)
qed
lemma design_iso_intersection_numbers: "source.intersection_numbers = target.intersection_numbers"
using inverse_design_isomorphism design_isomorphism.design_iso_inter_numbers_imp
design_iso_inter_numbers_imp by blast
lemma design_iso_n_intersect_num:
assumes "b1 ∈# ℬ"
assumes "b2 ∈# ℬ"
shows "b1 |∩|⇩n b2 = ((π ` b1) |∩|⇩n (π ` b2))"
proof -
let ?A = "{x . x ⊆ b1 ∧ x ⊆ b2 ∧ card x = n}"
let ?B = "{y . y ⊆ (π ` b1) ∧ y ⊆ (π ` b2) ∧ card y = n}"
have b1v: "b1 ⊆ 𝒱" by (simp add: assms(1) source.wellformed)
have b2v: "b2 ⊆ 𝒱" by (simp add: assms(2) source.wellformed)
then have "⋀x y . x ⊆ b1 ⟹ x ⊆ b2 ⟹ y ⊆ b1 ⟹ y ⊆ b2 ⟹ π ` x = π ` y ⟹ x = y"
using b1v bij by (metis bij_betw_imp_surj_on bij_betw_inv_into_subset dual_order.trans)
then have inj: "inj_on ((`) π) ?A" by (simp add: inj_on_def)
have eqcard: "⋀xa. xa ⊆ b1 ⟹ xa ⊆ b2 ⟹ card (π ` xa) = card xa" using b1v b2v bij
using iso_points_ss_card by auto
have surj: "⋀x. x ⊆ π ` b1 ⟹ x ⊆ π ` b2 ⟹
x ∈ {(π ` xa) | xa . xa ⊆ b1 ∧ xa ⊆ b2 ∧ card xa = card x}"
proof -
fix x
assume x1: "x ⊆ π ` b1" and x2: "x ⊆ π ` b2"
then obtain xa where eq_x: "π ` xa = x" and ss: "xa ⊆ 𝒱"
by (metis b1v dual_order.trans subset_imageE)
then have f1: "xa ⊆ b1" by (simp add: x1 assms(1) iso_point_subset_block_iff)
then have f2: "xa ⊆ b2" by (simp add: eq_x ss assms(2) iso_point_subset_block_iff x2)
then have f3: "card xa = card x" using bij by (simp add: eq_x ss iso_points_ss_card)
then show "x ∈ {(π ` xa) | xa . xa ⊆ b1 ∧ xa ⊆ b2 ∧ card xa = card x}"
using f1 f2 f3 ‹π ` xa = x› by auto
qed
have "bij_betw ( (`) π) ?A ?B"
proof (auto simp add: bij_betw_def)
show "inj_on ((`) π) {x. x ⊆ b1 ∧ x ⊆ b2 ∧ card x = n}" using inj by simp
show "⋀xa. xa ⊆ b1 ⟹ xa ⊆ b2 ⟹ n = card xa ⟹ card (π ` xa) = card xa"
using eqcard by simp
show "⋀x. x ⊆ π ` b1 ⟹ x ⊆ π ` b2 ⟹ n = card x ⟹
x ∈ (`) π ` {xa. xa ⊆ b1 ∧ xa ⊆ b2 ∧ card xa = card x}"
using surj by (simp add: setcompr_eq_image)
qed
thus ?thesis
using bij_betw_same_card by (auto simp add: n_intersect_number_def)
qed
lemma subdesign_iso_implies:
assumes "sub_set_system V B 𝒱 ℬ"
shows "sub_set_system (π ` V) (blocks_image B π) 𝒱' ℬ'"
proof (unfold_locales)
show "π ` V ⊆ 𝒱'"
by (metis assms image_mono iso_points_map sub_set_system.points_subset)
show "blocks_image B π ⊆# ℬ'"
by (metis assms block_img blocks_image_def image_mset_subseteq_mono sub_set_system.blocks_subset)
qed
lemma subdesign_image_is_design:
assumes "sub_set_system V B 𝒱 ℬ"
assumes "design V B"
shows "design (π ` V) (blocks_image B π)"
proof -
interpret fin: finite_incidence_system "(π ` V)" "(blocks_image B π)" using assms(2)
by (simp add: design.axioms(1) finite_incidence_system.image_set_system_finite)
interpret des: sub_design V B 𝒱 ℬ using assms design.wf_design_iff
by (unfold_locales, auto simp add: sub_set_system.points_subset sub_set_system.blocks_subset)
have bl_img: "blocks_image B π ⊆# ℬ'"
by (simp add: blocks_image_def des.blocks_subset image_mset_subseteq_mono iso_is_image_block)
then show ?thesis
proof (unfold_locales, auto)
show "{} ∈# blocks_image B π ⟹ False"
using assms subdesign_iso_implies target.blocks_nempty bl_img by auto
qed
qed
lemma sub_design_isomorphism:
assumes "sub_set_system V B 𝒱 ℬ"
assumes "design V B"
shows "design_isomorphism V B (π ` V) (blocks_image B π) π"
proof -
interpret design "(π ` V)" "(blocks_image B π)"
by (simp add: assms(1) assms(2) subdesign_image_is_design)
interpret des: design V B by fact
show ?thesis
proof (unfold_locales)
show "bij_betw π V (π ` V)" using bij
by (metis assms(1) bij_betw_subset sub_set_system.points_subset)
show "image_mset ((`) π) B = blocks_image B π" by (simp add: blocks_image_def)
qed
qed
end
end