Theory Group_Divisible_Designs
section ‹Group Divisible Designs›
text ‹Definitions in this section taken from the handbook \<^cite>‹"colbournHandbookCombinatorialDesigns2007"›
and Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››
theory Group_Divisible_Designs imports Resolvable_Designs
begin
subsection ‹Group design›
text ‹We define a group design to have an additional paramater $G$ which is a partition on the point
set $V$. This is not defined in the handbook, but is a precursor to GDD's without index constraints›
locale group_design = proper_design +
fixes groups :: "'a set set" ("𝒢")
assumes group_partitions: "partition_on 𝒱 𝒢"
assumes groups_size: "card 𝒢 > 1"
begin
lemma groups_not_empty: "𝒢 ≠ {}"
using groups_size by auto
lemma num_groups_lt_points: "card 𝒢 ≤ 𝗏"
by (simp add: partition_on_le_set_elements finite_sets group_partitions)
lemma groups_disjoint: "disjoint 𝒢"
using group_partitions partition_onD2 by auto
lemma groups_disjoint_pairwise: "G1 ∈ 𝒢 ⟹ G2 ∈ 𝒢 ⟹ G1 ≠ G2 ⟹ disjnt G1 G2"
using group_partitions partition_onD2 pairwiseD by fastforce
lemma point_in_one_group: "x ∈ G1 ⟹ G1 ∈ 𝒢 ⟹ G2 ∈ 𝒢 ⟹ G1 ≠ G2 ⟹ x ∉ G2"
using groups_disjoint_pairwise by (simp add: disjnt_iff)
lemma point_has_unique_group: "x ∈ 𝒱 ⟹ ∃!G. x ∈ G ∧ G ∈ 𝒢"
using partition_on_partition_on_unique group_partitions
by fastforce
lemma rep_number_point_group_one:
assumes "x ∈ 𝒱"
shows "card {g ∈ 𝒢 . x ∈ g} = 1"
proof -
obtain g' where "g' ∈ 𝒢" and "x ∈ g'"
using assms point_has_unique_group by blast
then have "{g ∈ 𝒢 . x ∈ g} = {g'}"
using group_partitions partition_onD4 by force
thus ?thesis
by simp
qed
lemma point_in_group: "G ∈ 𝒢 ⟹ x ∈ G ⟹ x ∈ 𝒱"
using group_partitions partition_onD1 by auto
lemma point_subset_in_group: "G ∈ 𝒢 ⟹ ps ⊆ G ⟹ ps ⊆ 𝒱"
using point_in_group by auto
lemma group_subset_point_subset: "G ∈ 𝒢 ⟹ G' ⊆ G ⟹ ps ⊆ G' ⟹ ps ⊆ 𝒱"
using point_subset_in_group by auto
lemma groups_finite: "finite 𝒢"
using finite_elements finite_sets group_partitions by auto
lemma group_elements_finite: "G ∈ 𝒢 ⟹ finite G"
using groups_finite finite_sets group_partitions
by (meson finite_subset point_in_group subset_iff)
lemma v_equals_sum_group_sizes: "𝗏 = (∑G ∈ 𝒢. card G)"
using group_partitions groups_disjoint partition_onD1 card_Union_disjoint group_elements_finite
by fastforce
lemma gdd_min_v: "𝗏 ≥ 2"
proof -
have assm: "card 𝒢 ≥ 2" using groups_size by simp
then have "⋀ G . G ∈ 𝒢 ⟹ G ≠ {}" using partition_onD3 group_partitions by auto
then have "⋀ G . G ∈ 𝒢 ⟹ card G ≥ 1"
using group_elements_finite card_0_eq by fastforce
then have " (∑G ∈ 𝒢. card G) ≥ 2" using assm
using sum_mono by force
thus ?thesis using v_equals_sum_group_sizes
by linarith
qed
lemma min_group_size: "G ∈ 𝒢 ⟹ card G ≥ 1"
using partition_onD3 group_partitions
using group_elements_finite not_le_imp_less by fastforce
lemma group_size_lt_v:
assumes "G ∈ 𝒢"
shows "card G < 𝗏"
proof -
have "(∑G' ∈ 𝒢. card G') = 𝗏" using gdd_min_v v_equals_sum_group_sizes
by linarith
then have split_sum: "card G + (∑G' ∈ (𝒢 - {G}). card G') = 𝗏" using assms sum.remove
by (metis groups_finite v_equals_sum_group_sizes)
have "card (𝒢 - {G}) ≥ 1" using groups_size
by (simp add: assms groups_finite)
then obtain G' where gin: "G' ∈ (𝒢 - {G})"
by (meson elem_exists_non_empty_set less_le_trans less_numeral_extra(1))
then have "card G' ≥ 1" using min_group_size by auto
then have "(∑G' ∈ (𝒢 - {G}). card G') ≥ 1"
by (metis gin finite_Diff groups_finite leI less_one sum_eq_0_iff)
thus ?thesis using split_sum
by linarith
qed
subsubsection ‹Group Type›
text ‹GDD's have a "type", which is defined by a sequence of group sizes $g_i$, and the number
of groups of that size $a_i$: $g_1^{a_1}g2^{a_2}...g_n^{a_n}$›
definition group_sizes :: "nat set" where
"group_sizes ≡ {card G | G . G ∈ 𝒢}"
definition groups_of_size :: "nat ⇒ nat" where
"groups_of_size g ≡ card { G ∈ 𝒢 . card G = g }"
definition group_type :: "(nat × nat) set" where
"group_type ≡ {(g, groups_of_size g) | g . g ∈ group_sizes }"
lemma group_sizes_min: "x ∈ group_sizes ⟹ x ≥ 1 "
unfolding group_sizes_def using min_group_size group_size_lt_v by auto
lemma group_sizes_max: "x ∈ group_sizes ⟹ x < 𝗏 "
unfolding group_sizes_def using min_group_size group_size_lt_v by auto
lemma group_size_implies_group_existance: "x ∈ group_sizes ⟹ ∃G. G ∈ 𝒢 ∧ card G = x"
unfolding group_sizes_def by auto
lemma groups_of_size_zero: "groups_of_size 0 = 0"
proof -
have empty: "{G ∈ 𝒢 . card G = 0} = {}" using min_group_size
by fastforce
thus ?thesis unfolding groups_of_size_def
by (simp add: empty)
qed
lemma groups_of_size_max:
assumes "g ≥ 𝗏"
shows "groups_of_size g = 0"
proof -
have "{G ∈ 𝒢 . card G = g} = {}" using group_size_lt_v assms by fastforce
thus ?thesis unfolding groups_of_size_def
by (simp add: ‹{G ∈ 𝒢. card G = g} = {}›)
qed
lemma group_type_contained_sizes: "(g, a) ∈ group_type ⟹ g ∈ group_sizes"
unfolding group_type_def by simp
lemma group_type_contained_count: "(g, a) ∈ group_type ⟹ card {G ∈ 𝒢 . card G = g} = a"
unfolding group_type_def groups_of_size_def by simp
lemma group_card_in_sizes: "g ∈ 𝒢 ⟹ card g ∈ group_sizes"
unfolding group_sizes_def by auto
lemma group_card_non_zero_groups_of_size_min:
assumes "g ∈ 𝒢"
assumes "card g = a"
shows "groups_of_size a ≥ 1"
proof -
have "g ∈ {G ∈ 𝒢 . card G = a}" using assms by simp
then have "{G ∈ 𝒢 . card G = a} ≠ {}" by auto
then have "card {G ∈ 𝒢 . card G = a} ≠ 0"
by (simp add: groups_finite)
thus ?thesis unfolding groups_of_size_def by simp
qed
lemma elem_in_group_sizes_min_of_size:
assumes "a ∈ group_sizes"
shows "groups_of_size a ≥ 1"
using assms group_card_non_zero_groups_of_size_min group_size_implies_group_existance by blast
lemma group_card_non_zero_groups_of_size_max:
shows "groups_of_size a ≤ 𝗏"
proof -
have "{G ∈ 𝒢 . card G = a} ⊆ 𝒢" by simp
then have "card {G ∈ 𝒢 . card G = a} ≤ card 𝒢"
by (simp add: card_mono groups_finite)
thus ?thesis
using groups_of_size_def num_groups_lt_points by auto
qed
lemma group_card_in_type: "g ∈ 𝒢 ⟹ ∃ x . (card g, x) ∈ group_type ∧ x ≥ 1"
unfolding group_type_def using group_card_non_zero_groups_of_size_min
by (simp add: group_card_in_sizes)
lemma partition_groups_on_size: "partition_on 𝒢 {{ G ∈ 𝒢 . card G = g } | g . g ∈ group_sizes}"
proof (intro partition_onI, auto)
fix g
assume a1: "g ∈ group_sizes"
assume " ∀x. x ∈ 𝒢 ⟶ card x ≠ g"
then show False using a1 group_size_implies_group_existance by auto
next
fix x
assume "x ∈ 𝒢"
then show "∃xa. (∃g. xa = {G ∈ 𝒢. card G = g} ∧ g ∈ group_sizes) ∧ x ∈ xa"
using group_card_in_sizes by auto
qed
lemma group_size_partition_covers_points: "⋃(⋃{{ G ∈ 𝒢 . card G = g } | g . g ∈ group_sizes}) = 𝒱"
by (metis (no_types, lifting) group_partitions partition_groups_on_size partition_onD1)
lemma groups_of_size_alt_def_count: "groups_of_size g = count {# card G . G ∈# mset_set 𝒢 #} g"
proof -
have a: "groups_of_size g = card { G ∈ 𝒢 . card G = g }" unfolding groups_of_size_def by simp
then have "groups_of_size g = size {# G ∈# (mset_set 𝒢) . card G = g #}"
using groups_finite by auto
then have size_repr: "groups_of_size g = size {# x ∈# {# card G . G ∈# mset_set 𝒢 #} . x = g #}"
using groups_finite by (simp add: filter_mset_image_mset)
have "group_sizes = set_mset ({# card G . G ∈# mset_set 𝒢 #})"
using group_sizes_def groups_finite by auto
thus ?thesis using size_repr by (simp add: count_size_set_repr)
qed
lemma v_sum_type_rep: "𝗏 = (∑ g ∈ group_sizes . g * (groups_of_size g))"
proof -
have gs: "set_mset {# card G . G ∈# mset_set 𝒢 #} = group_sizes"
unfolding group_sizes_def using groups_finite by auto
have "𝗏 = card (⋃(⋃{{ G ∈ 𝒢 . card G = g } | g . g ∈ group_sizes}))"
using group_size_partition_covers_points by simp
have v1: "𝗏 = (∑x ∈# {# card G . G ∈# mset_set 𝒢 #}. x)"
by (simp add: sum_unfold_sum_mset v_equals_sum_group_sizes)
then have "𝗏 = (∑x ∈ set_mset {# card G . G ∈# mset_set 𝒢 #} . x * (count {# card G . G ∈# mset_set 𝒢 #} x))"
using mset_set_size_card_count by (simp add: v1)
thus ?thesis using gs groups_of_size_alt_def_count by auto
qed
end
subsubsection ‹Uniform Group designs›
text ‹A group design requiring all groups are the same size›
locale uniform_group_design = group_design +
fixes u_group_size :: nat ("𝗆")
assumes uniform_groups: "G ∈ 𝒢 ⟹ card G = 𝗆"
begin
lemma m_positive: "𝗆 ≥ 1"
proof -
obtain G where "G ∈ 𝒢" using groups_size elem_exists_non_empty_set gr_implies_not_zero by blast
thus ?thesis using uniform_groups min_group_size by fastforce
qed
lemma uniform_groups_alt: " ∀ G ∈ 𝒢 . card G = 𝗆"
using uniform_groups by blast
lemma uniform_groups_group_sizes: "group_sizes = {𝗆}"
using design_points_nempty group_card_in_sizes group_size_implies_group_existance
point_has_unique_group uniform_groups_alt by force
lemma uniform_groups_group_size_singleton: "is_singleton (group_sizes)"
using uniform_groups_group_sizes by auto
lemma set_filter_eq_P_forall:"∀ x ∈ X . P x ⟹ Set.filter P X = X"
by (simp add: Collect_conj_eq Int_absorb2 Set.filter_def subsetI)
lemma uniform_groups_groups_of_size_m: "groups_of_size 𝗆 = card 𝒢"
proof(simp add: groups_of_size_def)
have "{G ∈ 𝒢. card G = 𝗆} = 𝒢" using uniform_groups_alt set_filter_eq_P_forall by auto
thus "card {G ∈ 𝒢. card G = 𝗆} = card 𝒢" by simp
qed
lemma uniform_groups_of_size_not_m: "x ≠ 𝗆 ⟹ groups_of_size x = 0"
by (simp add: groups_of_size_def card_eq_0_iff uniform_groups)
end
subsection ‹GDD›
text ‹A GDD extends a group design with an additional index parameter.
Each pair of elements must occur either \Lambda times if in diff groups, or 0 times if in the same
group›
locale GDD = group_design +
fixes index :: int ("Λ")
assumes index_ge_1: "Λ ≥ 1"
assumes index_together: "G ∈ 𝒢 ⟹ x ∈ G ⟹ y ∈ G ⟹ x ≠ y ⟹ ℬ index {x, y} = 0"
assumes index_distinct: "G1 ∈ 𝒢 ⟹ G2 ∈ 𝒢 ⟹ G1 ≠ G2 ⟹ x ∈ G1 ⟹ y ∈ G2 ⟹
ℬ index {x, y} = Λ"
begin
lemma points_sep_groups_ne: "G1 ∈ 𝒢 ⟹ G2 ∈ 𝒢 ⟹ G1 ≠ G2 ⟹ x ∈ G1 ⟹ y ∈ G2 ⟹ x ≠ y"
by (meson point_in_one_group)
lemma index_together_alt_ss: "ps ⊆ G ⟹ G ∈ 𝒢 ⟹ card ps = 2 ⟹ ℬ index ps = 0"
using index_together by (metis card_2_iff insert_subset)
lemma index_distinct_alt_ss: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ (⋀ G . G ∈ 𝒢 ⟹ ¬ ps ⊆ G) ⟹
ℬ index ps = Λ"
using index_distinct by (metis card_2_iff empty_subsetI insert_subset point_has_unique_group)
lemma gdd_index_options: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps = 0 ∨ ℬ index ps = Λ"
using index_distinct_alt_ss index_together_alt_ss by blast
lemma index_zero_implies_same_group: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps = 0 ⟹
∃ G ∈ 𝒢 . ps ⊆ G" using index_distinct_alt_ss gr_implies_not_zero
by (metis index_ge_1 less_one of_nat_0 of_nat_1 of_nat_le_0_iff)
lemma index_zero_implies_same_group_unique: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps = 0 ⟹
∃! G ∈ 𝒢 . ps ⊆ G"
by (meson GDD.index_zero_implies_same_group GDD_axioms card_2_iff' group_design.point_in_one_group
group_design_axioms in_mono)
lemma index_not_zero_impl_diff_group: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps = Λ ⟹
(⋀ G . G ∈ 𝒢 ⟹ ¬ ps ⊆ G)"
using index_ge_1 index_together_alt_ss by auto
lemma index_zero_implies_one_group:
assumes "ps ⊆ 𝒱"
and "card ps = 2"
and "ℬ index ps = 0"
shows "size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 1"
proof -
obtain G where ging: "G ∈ 𝒢" and psin: "ps ⊆ G"
using index_zero_implies_same_group groups_size assms by blast
then have unique: "⋀ G2 . G2 ∈ 𝒢 ⟹ G ≠ G2 ⟹ ¬ ps ⊆ G2"
using index_zero_implies_same_group_unique by (metis assms)
have "⋀ G'. G' ∈ 𝒢 ⟷ G' ∈# mset_set 𝒢"
by (simp add: groups_finite)
then have eq_mset: "{#b ∈# mset_set 𝒢 . ps ⊆ b#} = mset_set {b ∈ 𝒢 . ps ⊆ b}"
using filter_mset_mset_set groups_finite by blast
then have "{b ∈ 𝒢 . ps ⊆ b} = {G}" using unique psin
by (smt Collect_cong ging singleton_conv)
thus ?thesis by (simp add: eq_mset)
qed
lemma index_distinct_group_num_alt_def: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹
size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 0 ⟹ ℬ index ps = Λ"
by (metis gdd_index_options index_zero_implies_one_group numeral_One zero_neq_numeral)
lemma index_non_zero_implies_no_group:
assumes "ps ⊆ 𝒱"
and "card ps = 2"
and "ℬ index ps = Λ"
shows "size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 0"
proof -
have "⋀ G . G ∈ 𝒢 ⟹ ¬ ps ⊆ G" using index_not_zero_impl_diff_group assms by simp
then have "{#b ∈# mset_set 𝒢 . ps ⊆ b#} = {#}"
using filter_mset_empty_if_finite_and_filter_set_empty by force
thus ?thesis by simp
qed
lemma gdd_index_non_zero_iff: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹
ℬ index ps = Λ ⟷ size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 0"
using index_non_zero_implies_no_group index_distinct_group_num_alt_def by auto
lemma gdd_index_zero_iff: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹
ℬ index ps = 0 ⟷ size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 1"
apply (auto simp add: index_zero_implies_one_group)
by (metis GDD.gdd_index_options GDD_axioms index_non_zero_implies_no_group old.nat.distinct(2))
lemma points_index_upper_bound: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps ≤ Λ"
using gdd_index_options index_ge_1
by (metis int_one_le_iff_zero_less le_refl of_nat_0 of_nat_0_le_iff of_nat_le_iff zero_less_imp_eq_int)
lemma index_1_imp_mult_1:
assumes "Λ = 1"
assumes "bl ∈# ℬ"
assumes "card bl ≥ 2"
shows "multiplicity bl = 1"
proof (rule ccontr)
assume "¬ (multiplicity bl = 1)"
then have "multiplicity bl ≠ 1" and "multiplicity bl ≠ 0" using assms by simp_all
then have m: "multiplicity bl ≥ 2" by linarith
obtain ps where ps: "ps ⊆ bl ∧ card ps = 2"
using nat_int_comparison(3) obtain_subset_with_card_n by (metis assms(3))
then have "ℬ index ps ≥ 2"
using m points_index_count_min ps by blast
then show False using assms index_distinct ps antisym_conv2 not_numeral_less_zero
numeral_le_one_iff points_index_ps_nin semiring_norm(69) zero_neq_numeral
by (metis gdd_index_options int_int_eq int_ops(2))
qed
lemma simple_if_block_size_gt_2:
assumes "⋀ bl . card bl ≥ 2"
assumes "Λ = 1"
shows "simple_design 𝒱 ℬ"
using index_1_imp_mult_1 assms apply (unfold_locales)
by (metis card.empty not_numeral_le_zero)
end
subsubsection ‹Sub types of GDD's›
text ‹In literature, a GDD is usually defined in a number of different ways,
including factors such as block size limitations›
locale K_Λ_GDD = K_block_design + GDD
locale k_Λ_GDD = block_design + GDD
sublocale k_Λ_GDD ⊆ K_Λ_GDD 𝒱 ℬ "{𝗄}" 𝒢 Λ
by (unfold_locales)
locale K_GDD = K_Λ_GDD 𝒱 ℬ 𝒦 𝒢 1
for point_set ("𝒱") and block_collection ("ℬ") and sizes ("𝒦") and groups ("𝒢")
locale k_GDD = k_Λ_GDD 𝒱 ℬ 𝗄 𝒢 1
for point_set ("𝒱") and block_collection ("ℬ") and u_block_size ("𝗄") and groups ("𝒢")
sublocale k_GDD ⊆ K_GDD 𝒱 ℬ "{𝗄}" 𝒢
by (unfold_locales)
lemma (in K_GDD) multiplicity_1: "bl ∈# ℬ ⟹ card bl ≥ 2 ⟹ multiplicity bl = 1"
using index_1_imp_mult_1 by simp
locale RGDD = GDD + resolvable_design
subsection ‹GDD and PBD Constructions›
text ‹GDD's are commonly studied alongside PBD's (pairwise balanced designs). Many constructions
have been developed for designs to create a GDD from a PBD and vice versa. In particular,
Wilsons Construction is a well known construction, which is formalised in this section. It
should be noted that many of the more basic constructions in this section are often stated without
proof/all the necessary assumptions in textbooks/course notes.›
context GDD
begin
subsubsection ‹GDD Delete Point construction›
lemma delete_point_index_zero:
assumes "G ∈ {g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}}"
and "y ∈ G" and "z ∈ G" and "z≠ y"
shows "(del_point_blocks x) index {y, z} = 0"
proof -
have "y ≠ x" using assms(1) assms(2) by blast
have "z ≠ x" using assms(1) assms(3) by blast
obtain G' where ing: "G' ∈ 𝒢" and ss: "G ⊆ G'"
using assms(1) by auto
have "{y, z} ⊆ G" by (simp add: assms(2) assms(3))
then have "{y, z} ⊆ 𝒱"
by (meson ss ing group_subset_point_subset)
then have "{y, z} ⊆ (del_point x)"
using ‹y ≠ x› ‹z ≠ x› del_point_def by fastforce
thus ?thesis using delete_point_index_eq index_together
by (metis assms(2) assms(3) assms(4) in_mono ing ss)
qed
lemma delete_point_index:
assumes "G1 ∈ {g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}}"
assumes "G2 ∈ {g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}}"
assumes "G1 ≠ G2" and "y ∈ G1" and "z ∈ G2"
shows "del_point_blocks x index {y, z} = Λ"
proof -
have "y ≠ x" using assms by blast
have "z ≠ x" using assms by blast
obtain G1' where ing1: "G1' ∈ 𝒢" and t1: "G1 = G1' - {x}"
using assms(1) by auto
obtain G2' where ing2: "G2' ∈ 𝒢" and t2: "G2 = G2' - {x}"
using assms(2) by auto
then have ss1: "G1 ⊆ G1'" and ss2: "G2 ⊆ G2'" using t1 by auto
then have "{y, z} ⊆ 𝒱" using ing1 ing2 ss1 ss2 assms(4) assms(5)
by (metis empty_subsetI insert_absorb insert_subset point_in_group)
then have "{y, z} ⊆ del_point x"
using ‹y ≠ x› ‹z ≠ x› del_point_def by auto
then have indx: "del_point_blocks x index {y, z} = ℬ index {y, z}"
using delete_point_index_eq by auto
have "G1' ≠ G2'" using assms t1 t2 by fastforce
thus ?thesis using index_distinct
using indx assms(4) assms(5) ing1 ing2 t1 t2 by auto
qed
lemma delete_point_group_size:
assumes "{x} ∈ 𝒢 ⟹ card 𝒢 > 2"
shows "1 < card {g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}}"
proof (cases "{x} ∈ 𝒢")
case True
then have "⋀ g . g ∈ (𝒢 - {{x}}) ⟹ x ∉ g"
by (meson disjnt_insert1 groups_disjoint pairwise_alt)
then have simpg: "⋀ g . g ∈ (𝒢 - {{x}}) ⟹ g - {x} = g"
by simp
have "{g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}} = {g - {x} |g. (g ∈ 𝒢 - {{x}})}" using True
by force
then have "{g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}} = {g |g. (g ∈ 𝒢 - {{x}})}" using simpg
by (smt (verit) Collect_cong)
then have eq: "{g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}} = 𝒢 - {{x}}" using set_self_img_compr by blast
have "card (𝒢 - {{x}}) = card 𝒢 - 1" using True
by (simp add: groups_finite)
then show ?thesis using True assms eq diff_is_0_eq' by force
next
case False
then have "⋀g' y. {x} ∉ 𝒢 ⟹ g' ∈ 𝒢 ⟹ y ∈ 𝒢 ⟹ g' - {x} = y - {x} ⟹ g' = y"
by (metis all_not_in_conv insert_Diff_single insert_absorb insert_iff points_sep_groups_ne)
then have inj: "inj_on (λ g . g - {x}) 𝒢" by (simp add: inj_onI False)
have "{g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}} = {g - {x} |g. g ∈ 𝒢}" using False by auto
then have "card {g - {x} |g. g ∈ 𝒢 ∧ g ≠ {x}} = card 𝒢" using inj groups_finite card_image
by (auto simp add: card_image setcompr_eq_image)
then show ?thesis using groups_size by presburger
qed
lemma GDD_by_deleting_point:
assumes "⋀bl. bl ∈# ℬ ⟹ x ∈ bl ⟹ 2 ≤ card bl"
assumes "{x} ∈ 𝒢 ⟹ card 𝒢 > 2"
shows "GDD (del_point x) (del_point_blocks x) {g - {x} | g . g ∈ 𝒢 ∧ g ≠ {x}} Λ"
proof -
interpret pd: proper_design "del_point x" "del_point_blocks x"
using delete_point_proper assms by blast
show ?thesis using delete_point_index_zero delete_point_index assms delete_point_group_size
by(unfold_locales) (simp_all add: partition_on_remove_pt group_partitions index_ge_1 del_point_def)
qed
end
context K_GDD begin
subsubsection ‹PBD construction from GDD›
text ‹Two well known PBD constructions involve taking a GDD and either combining the groups and
blocks to form a new block collection, or by adjoining a point›
text ‹First prove that combining the groups and block set results in a constant index›
lemma kgdd1_points_index_group_block:
assumes "ps ⊆ 𝒱"
and "card ps = 2"
shows "(ℬ + mset_set 𝒢) index ps = 1"
proof -
have index1: "(⋀ G . G ∈ 𝒢 ⟹ ¬ ps ⊆ G) ⟹ ℬ index ps = 1"
using index_distinct_alt_ss assms by fastforce
have groups1: "ℬ index ps = 0 ⟹ size {#b ∈# mset_set 𝒢 . ps ⊆ b#} = 1"
using index_zero_implies_one_group assms by simp
then have "(ℬ + mset_set 𝒢) index ps = size (filter_mset ((⊆) ps) (ℬ + mset_set 𝒢))"
by (simp add: points_index_def)
thus ?thesis using index1 groups1 gdd_index_non_zero_iff gdd_index_zero_iff assms
gdd_index_options points_index_def filter_union_mset union_commute
by (smt (z3) empty_neutral(1) less_irrefl_nat nonempty_has_size of_nat_1_eq_iff)
qed
text ‹Combining blocks and the group set forms a PBD›
lemma combine_block_groups_pairwise: "pairwise_balance 𝒱 (ℬ + mset_set 𝒢) 1"
proof -
let ?B = "ℬ + mset_set 𝒢"
have ss: "⋀ G. G ∈ 𝒢 ⟹ G ⊆ 𝒱"
by (simp add: point_in_group subsetI)
have "⋀ G. G ∈ 𝒢 ⟹ G ≠ {}" using group_partitions
using partition_onD3 by auto
then interpret inc: design 𝒱 ?B
proof (unfold_locales)
show "⋀b. (⋀G. G ∈ 𝒢 ⟹ G ≠ {}) ⟹ b ∈# ℬ + mset_set 𝒢 ⟹ b ⊆ 𝒱"
by (metis finite_set_mset_mset_set groups_finite ss union_iff wellformed)
show "(⋀G. G ∈ 𝒢 ⟹ G ≠ {}) ⟹ finite 𝒱" by (simp add: finite_sets)
show "⋀bl. (⋀G. G ∈ 𝒢 ⟹ G ≠ {}) ⟹ bl ∈# ℬ + mset_set 𝒢 ⟹ bl ≠ {}"
using blocks_nempty groups_finite by auto
qed
show ?thesis proof (unfold_locales)
show "inc.𝖻 ≠ 0" using b_positive by auto
show "(1 ::nat) ≤ 2" by simp
show "2 ≤ inc.𝗏" by (simp add: gdd_min_v)
then show "⋀ps. ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ (ℬ + mset_set 𝒢) index ps = 1"
using kgdd1_points_index_group_block by simp
qed
qed
lemma combine_block_groups_PBD:
assumes "⋀ G. G ∈ 𝒢 ⟹ card G ∈ 𝒦"
assumes "⋀ k . k ∈ 𝒦 ⟹ k ≥ 2"
shows "PBD 𝒱 (ℬ + mset_set 𝒢) 𝒦"
proof -
let ?B = "ℬ + mset_set 𝒢"
interpret inc: pairwise_balance 𝒱 ?B 1 using combine_block_groups_pairwise by simp
show ?thesis using assms block_sizes groups_finite positive_ints
by (unfold_locales) auto
qed
text ‹Prove adjoining a point to each group set results in a constant points index›
lemma kgdd1_index_adjoin_group_block:
assumes "x ∉ 𝒱"
assumes "ps ⊆ insert x 𝒱"
assumes "card ps = 2"
shows "(ℬ + mset_set {insert x g |g. g ∈ 𝒢}) index ps = 1"
proof -
have "inj_on ((insert) x) 𝒢"
by (meson assms(1) inj_onI insert_ident point_in_group)
then have eq: "mset_set {insert x g |g. g ∈ 𝒢} = {# insert x g . g ∈# mset_set 𝒢#}"
by (simp add: image_mset_mset_set setcompr_eq_image)
thus ?thesis
proof (cases "x ∈ ps")
case True
then obtain y where y_ps: "ps = {x, y}" using assms(3)
by (metis card_2_iff doubleton_eq_iff insertE singletonD)
then have ynex: "y ≠ x" using assms by fastforce
have yinv: "y ∈ 𝒱"
using assms(2) y_ps ynex by auto
have all_g: "⋀ g. g ∈# (mset_set {insert x g |g. g ∈ 𝒢}) ⟹ x ∈ g"
using eq by force
have iff: "⋀ g . g ∈ 𝒢 ⟹ y ∈ (insert x g) ⟷ y ∈ g" using ynex by simp
have b: "ℬ index ps = 0"
using True assms(1) points_index_ps_nin by fastforce
then have "(ℬ + mset_set {insert x g |g. g ∈ 𝒢}) index ps =
(mset_set {insert x g |g. g ∈ 𝒢}) index ps"
using eq by (simp add: point_index_distrib)
also have "... = (mset_set {insert x g |g. g ∈ 𝒢}) rep y" using points_index_pair_rep_num
by (metis (no_types, lifting) all_g y_ps)
also have 0: "... = card {b ∈ {insert x g |g. g ∈ 𝒢} . y ∈ b}"
by (simp add: groups_finite rep_number_on_set_def)
also have 1: "... = card {insert x g |g. g ∈ 𝒢 ∧ y ∈ insert x g}"
by (smt (verit) Collect_cong mem_Collect_eq)
also have 2: " ... = card {insert x g |g. g ∈ 𝒢 ∧ y ∈ g}"
using iff by metis
also have "... = card {g ∈ 𝒢 . y ∈ g}" using 1 2 0 empty_iff eq groups_finite ynex insert_iff
by (metis points_index_block_image_add_eq points_index_single_rep_num rep_number_on_set_def)
finally have "(ℬ + mset_set {insert x g |g. g ∈ 𝒢}) index ps = 1"
using rep_number_point_group_one yinv by simp
then show ?thesis
by simp
next
case False
then have v: "ps ⊆ 𝒱" using assms(2) by auto
then have "(ℬ + mset_set {insert x g |g. g ∈ 𝒢}) index ps = (ℬ + mset_set 𝒢) index ps"
using eq by (simp add: points_index_block_image_add_eq False point_index_distrib)
then show ?thesis using v assms kgdd1_points_index_group_block by simp
qed
qed
lemma pairwise_by_adjoining_point:
assumes "x ∉ 𝒱"
shows "pairwise_balance (add_point x) (ℬ + mset_set { insert x g | g. g ∈ 𝒢}) 1"
proof -
let ?B = "ℬ + mset_set { insert x g | g. g ∈ 𝒢}"
let ?V = "add_point x"
have vdef: "?V = 𝒱 ∪ {x}" using add_point_def by simp
show ?thesis unfolding add_point_def using finite_sets design_blocks_nempty
proof (unfold_locales, simp_all)
have "⋀ G. G ∈ 𝒢 ⟹ insert x G ⊆ ?V"
by (simp add: point_in_group subsetI vdef)
then have "⋀ G. G ∈# (mset_set { insert x g | g. g ∈ 𝒢}) ⟹ G ⊆ ?V"
by (smt (verit, del_insts) elem_mset_set empty_iff infinite_set_mset_mset_set mem_Collect_eq)
then show "⋀b. b ∈# ℬ ∨ b ∈# mset_set {insert x g |g. g ∈ 𝒢} ⟹ b ⊆ insert x 𝒱"
using wellformed add_point_def by fastforce
next
have "⋀ G. G ∈ 𝒢 ⟹ insert x G ≠ {}" using group_partitions
using partition_onD3 by auto
then have gnempty: "⋀ G. G ∈# (mset_set { insert x g | g. g ∈ 𝒢}) ⟹ G ≠ {}"
by (smt (verit, del_insts) elem_mset_set empty_iff infinite_set_mset_mset_set mem_Collect_eq)
then show "⋀bl. bl ∈# ℬ ∨ bl ∈# mset_set {insert x g |g. g ∈ 𝒢} ⟹ bl ≠ {}"
using blocks_nempty by auto
next
have "card 𝒱 ≥ 2" using gdd_min_v by simp
then have "card (insert x 𝒱) ≥ 2"
by (meson card_insert_le dual_order.trans finite_sets)
then show "2 ≤ card (insert x 𝒱)" by auto
next
show "⋀ps. ps ⊆ insert x 𝒱 ⟹
card ps = 2 ⟹ (ℬ + mset_set {insert x g |g. g ∈ 𝒢}) index ps = Suc 0"
using kgdd1_index_adjoin_group_block by (simp add: assms)
qed
qed
lemma PBD_by_adjoining_point:
assumes "x ∉ 𝒱"
assumes "⋀ k . k ∈ 𝒦 ⟹ k ≥ 2"
shows "PBD (add_point x) (ℬ + mset_set { insert x g | g. g ∈ 𝒢}) (𝒦 ∪ {(card g) + 1 | g . g ∈ 𝒢})"
proof -
let ?B = "ℬ + mset_set { insert x g | g. g ∈ 𝒢}"
let ?V = "(add_point x)"
interpret inc: pairwise_balance ?V ?B 1 using pairwise_by_adjoining_point assms by auto
show ?thesis using block_sizes positive_ints proof (unfold_locales)
have xg: "⋀ g. g ∈ 𝒢 ⟹ x ∉ g"
using assms point_in_group by auto
have "⋀ bl . bl ∈# ℬ ⟹ card bl ∈ 𝒦" by (simp add: block_sizes)
have "⋀ bl . bl ∈# mset_set {insert x g |g. g ∈ 𝒢} ⟹ bl ∈ {insert x g | g . g ∈ 𝒢}"
by (simp add: groups_finite)
then have "⋀ bl . bl ∈# mset_set {insert x g |g. g ∈ 𝒢} ⟹
card bl ∈ {card g + 1 |g. g ∈ 𝒢}"
proof -
fix bl
assume "bl ∈# mset_set {insert x g |g. g ∈ 𝒢}"
then have "bl ∈ {insert x g | g . g ∈ 𝒢}" by (simp add: groups_finite)
then obtain g where gin: "g ∈ 𝒢" and i: "bl = insert x g" by auto
thus "card bl ∈ {(card g + 1) |g. g ∈ 𝒢}"
using gin group_elements_finite i xg by auto
qed
then show "⋀bl. bl ∈# ℬ + mset_set {insert x g |g. g ∈ 𝒢} ⟹
(card bl) ∈ 𝒦 ∪ {(card g + 1) |g. g ∈ 𝒢}"
using UnI1 UnI2 block_sizes union_iff by (smt (z3) mem_Collect_eq)
show "⋀x. x ∈ 𝒦 ∪ {card g + 1 |g. g ∈ 𝒢} ⟹ 0 < x"
using min_group_size positive_ints by auto
show "⋀k. k ∈ 𝒦 ∪ {card g + 1 |g. g ∈ 𝒢} ⟹ 2 ≤ k"
using min_group_size positive_ints assms by fastforce
qed
qed
subsubsection ‹Wilson's Construction›
text ‹Wilson's construction involves the combination of multiple k-GDD's. This proof was
based of Stinson \<^cite>‹"stinsonCombinatorialDesignsConstructions2004"››
lemma wilsons_construction_proper:
assumes "card I = w"
assumes "w > 0"
assumes "⋀ n. n ∈ 𝒦' ⟹ n ≥ 2"
assumes "⋀ B . B ∈# ℬ ⟹ K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
shows "proper_design (𝒱 × I) (∑B ∈# ℬ. (f B))" (is "proper_design ?Y ?B")
proof (unfold_locales, simp_all)
show "⋀b. ∃x∈#ℬ. b ∈# f x ⟹ b ⊆ 𝒱 × I"
proof -
fix b
assume "∃x∈#ℬ. b ∈# f x"
then obtain B where "B ∈# ℬ" and "b ∈# (f B)" by auto
then interpret kgdd: K_GDD "(B × I)" "(f B)" 𝒦' "{{x} × I |x . x ∈ B }" using assms by auto
show "b ⊆ 𝒱 × I" using kgdd.wellformed
using ‹B ∈# ℬ› ‹b ∈# f B› wellformed by fastforce
qed
show "finite (𝒱 × I)" using finite_sets assms bot_nat_0.not_eq_extremum card.infinite by blast
show "⋀bl. ∃x∈#ℬ. bl ∈# f x ⟹ bl ≠ {}"
proof -
fix bl
assume "∃x∈#ℬ. bl ∈# f x"
then obtain B where "B ∈# ℬ" and "bl ∈# (f B)" by auto
then interpret kgdd: K_GDD "(B × I)" "(f B)" 𝒦' "{{x} × I |x . x ∈ B }" using assms by auto
show "bl ≠ {}" using kgdd.blocks_nempty by (simp add: ‹bl ∈# f B›)
qed
show "∃i∈#ℬ. f i ≠ {#}"
proof -
obtain B where "B ∈# ℬ"
using design_blocks_nempty by auto
then interpret kgdd: K_GDD "(B × I)" "(f B)" 𝒦' "{{x} × I |x . x ∈ B }" using assms by auto
have "f B ≠ {#}" using kgdd.design_blocks_nempty by simp
then show "∃i∈#ℬ. f i ≠ {#}" using ‹B ∈# ℬ› by auto
qed
qed
lemma pair_construction_block_sizes:
assumes "K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
assumes "B ∈# ℬ"
assumes "b ∈# (f B)"
shows "card b ∈ 𝒦'"
proof -
interpret bkgdd: K_GDD "(B × I)" "(f B)" 𝒦' "{{x} × I |x . x ∈ B }"
using assms by simp
show "card b ∈ 𝒦'" using bkgdd.block_sizes by (simp add:assms)
qed
lemma wilsons_construction_index_0:
assumes "⋀ B . B ∈# ℬ ⟹ K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
assumes "G ∈ {GG × I |GG. GG ∈ 𝒢}"
assumes "X ∈ G"
assumes "Y ∈ G"
assumes "X ≠ Y"
shows "(∑⇩# (image_mset f ℬ)) index {X, Y} = 0"
proof -
obtain G' where gi: "G = G' × I" and ging: "G' ∈ 𝒢" using assms by auto
obtain x y ix iy where xpair: "X = (x, ix)" and ypair: "Y = (y, iy)" using assms by auto
then have ixin: "ix ∈ I" and xing: "x ∈ G'" using assms gi by auto
have iyin: "iy ∈ I" and ying: "y ∈ G'" using assms ypair gi by auto
have ne_index_0: "x ≠ y ⟹ ℬ index {x, y} = 0"
using ying xing index_together ging by simp
have "⋀ B. B ∈# ℬ ⟹ (f B) index {(x, ix), (y, iy)} = 0"
proof -
fix B
assume assm: "B ∈# ℬ"
then interpret kgdd: K_GDD "(B × I)" "(f B)" 𝒦' "{{x} × I |x . x ∈ B }" using assms by simp
have not_ss_0: "¬ ({(x, ix), (y, iy)} ⊆ (B × I)) ⟹ (f B) index {(x, ix), (y, iy)} = 0"
by (metis kgdd.points_index_ps_nin)
have "x ≠ y ⟹ ¬ {x, y} ⊆ B" using ne_index_0 assm points_index_0_left_imp by auto
then have "x ≠ y ⟹ ¬ ({(x, ix), (y, iy)} ⊆ (B × I))" using assms
by (meson empty_subsetI insert_subset mem_Sigma_iff)
then have nexy: "x ≠ y ⟹ (f B) index {(x, ix), (y, iy)} = 0" using not_ss_0 by simp
have "x = y ⟹ ({(x, ix), (y, iy)} ⊆ (B × I)) ⟹ (f B) index {(x, ix), (y, iy)} = 0"
proof -
assume eq: "x = y"
assume "({(x, ix), (y, iy)} ⊆ (B × I))"
then obtain g where "g ∈ {{x} × I |x . x ∈ B }" and "(x, ix) ∈ g" and "(y, ix) ∈ g"
using eq by auto
then show ?thesis using kgdd.index_together
by (smt (verit, best) SigmaD1 SigmaD2 SigmaI assms(4) assms(5) gi mem_Collect_eq xpair ypair)
qed
then show "(f B) index {(x, ix), (y, iy)} = 0" using not_ss_0 nexy by auto
qed
then have "⋀ B. B ∈# (image_mset f ℬ) ⟹ B index {(x, ix), (y, iy)} = 0" by auto
then show "(∑⇩# (image_mset f ℬ)) index {X, Y} = 0"
by (simp add: points_index_sum xpair ypair)
qed
lemma wilsons_construction_index_1:
assumes "⋀ B . B ∈# ℬ ⟹ K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
assumes "G1 ∈ {G × I |G. G ∈ 𝒢}"
assumes "G2 ∈ {G × I |G. G ∈ 𝒢}"
assumes "G1 ≠ G2"
and "(x, ix) ∈ G1" and "(y, iy) ∈ G2"
shows "(∑⇩# (image_mset f ℬ)) index {(x, ix), (y, iy)} = (1 ::int)"
proof -
obtain G1' where gi1: "G1 = G1' × I" and ging1: "G1' ∈ 𝒢" using assms by auto
obtain G2' where gi2: "G2 = G2' × I" and ging2: "G2' ∈ 𝒢" using assms by auto
have xing: "x ∈ G1'" using assms gi1 by simp
have ying: "y ∈ G2'" using assms gi2 by simp
have gne: "G1' ≠ G2'" using assms gi1 gi2 by auto
then have xyne: "x ≠ y" using xing ying ging1 ging2 point_in_one_group by blast
have "∃! bl . bl ∈# ℬ ∧ {x, y} ⊆ bl" using index_distinct points_index_one_unique_block
by (metis ging1 ging2 gne of_nat_1_eq_iff xing ying)
then obtain bl where blinb:"bl ∈# ℬ" and xyblss: "{x, y} ⊆ bl" by auto
then have "⋀ b . b ∈# ℬ - {#bl#} ⟹ ¬ {x, y} ⊆ b" using points_index_one_not_unique_block
by (metis ging1 ging2 gne index_distinct int_ops(2) nat_int_comparison(1) xing ying)
then have not_ss: "⋀ b . b ∈# ℬ - {#bl#} ⟹ ¬ ({(x, ix), (y, iy)} ⊆ (b × I))" using assms
by (meson SigmaD1 empty_subsetI insert_subset)
then have pi0: "⋀ b . b ∈# ℬ - {#bl#} ⟹ (f b) index {(x, ix), (y, iy)} = 0"
proof -
fix b
assume assm: "b ∈# ℬ - {#bl#}"
then have "b ∈# ℬ" by (meson in_diffD)
then interpret kgdd: K_GDD "(b × I)" "(f b)" 𝒦' "{{x} × I |x . x ∈ b }" using assms by simp
show "(f b) index {(x, ix), (y, iy)} = 0"
using assm not_ss by (metis kgdd.points_index_ps_nin)
qed
let ?G = "{{x} × I |x . x ∈ bl }"
interpret bkgdd: K_GDD "(bl × I)" "(f bl)" 𝒦' ?G using assms blinb by simp
obtain g1 g2 where xing1: "(x, ix) ∈ g1" and ying2: "(y, iy) ∈ g2" and g1g: "g1 ∈ ?G"
and g2g: "g2 ∈ ?G" using assms(5) assms(6) gi1 gi2
by (metis (no_types, lifting) bkgdd.point_has_unique_group insert_subset mem_Sigma_iff xyblss)
then have "g1 ≠ g2" using xyne by blast
then have pi1: "(f bl) index {(x, ix), (y, iy)} = 1"
using bkgdd.index_distinct xing1 ying2 g1g g2g by simp
have "(∑⇩# (image_mset f ℬ)) index {(x, ix), (y, iy)} =
(∑B ∈# ℬ. (f B) index {(x, ix), (y, iy)} )"
by (simp add: points_index_sum)
then have "(∑⇩# (image_mset f ℬ)) index {(x, ix), (y, iy)} =
(∑B ∈# (ℬ - {#bl#}). (f B) index {(x, ix), (y, iy)}) + (f bl) index {(x, ix), (y, iy)}"
by (metis (no_types, lifting) add.commute blinb insert_DiffM sum_mset.insert)
thus ?thesis using pi0 pi1 by simp
qed
theorem Wilsons_Construction:
assumes "card I = w"
assumes "w > 0"
assumes "⋀ n. n ∈ 𝒦' ⟹ n ≥ 2"
assumes "⋀ B . B ∈# ℬ ⟹ K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
shows "K_GDD (𝒱 × I) (∑B ∈# ℬ. (f B)) 𝒦' {G × I | G . G ∈ 𝒢}"
proof -
let ?Y = "𝒱 × I" and ?H = "{G × I | G . G ∈ 𝒢}" and ?B = "∑B ∈# ℬ. (f B)"
interpret pd: proper_design ?Y ?B using wilsons_construction_proper assms by auto
have "⋀ bl . bl ∈# (∑B ∈# ℬ. (f B)) ⟹ card bl ∈ 𝒦'"
using assms pair_construction_block_sizes by blast
then interpret kdes: K_block_design ?Y ?B 𝒦'
using assms(3) by (unfold_locales) (simp_all,fastforce)
interpret gdd: GDD ?Y ?B ?H "1:: int"
proof (unfold_locales)
show "partition_on (𝒱 × I) {G × I |G. G ∈ 𝒢}"
using assms groups_not_empty design_points_nempty group_partitions
by (simp add: partition_on_cart_prod)
have "inj_on (λ G. G × I) 𝒢"
using inj_on_def pd.design_points_nempty by auto
then have "card {G × I |G. G ∈ 𝒢} = card 𝒢" using card_image by (simp add: Setcompr_eq_image)
then show "1 < card {G × I |G. G ∈ 𝒢}" using groups_size by linarith
show "(1::int) ≤ 1" by simp
have gdd_fact: "⋀ B . B ∈# ℬ ⟹ K_GDD (B × I) (f B) 𝒦' {{x} × I |x . x ∈ B }"
using assms by simp
show "⋀G X Y. G ∈ {GG × I |GG. GG ∈ 𝒢} ⟹ X ∈ G ⟹ Y ∈ G ⟹ X ≠ Y
⟹ (∑⇩# (image_mset f ℬ)) index {X, Y} = 0"
using wilsons_construction_index_0[OF assms(4)] by auto
show "⋀G1 G2 X Y. G1 ∈ {G × I |G. G ∈ 𝒢} ⟹ G2 ∈ {G × I |G. G ∈ 𝒢}
⟹ G1 ≠ G2 ⟹ X ∈ G1 ⟹ Y ∈ G2 ⟹ ((∑⇩# (image_mset f ℬ)) index {X, Y}) = (1 ::int)"
using wilsons_construction_index_1[OF assms(4)] by blast
qed
show ?thesis by (unfold_locales)
qed
end
context pairwise_balance
begin
lemma PBD_by_deleting_point:
assumes "𝗏 > 2"
assumes "⋀ bl . bl ∈# ℬ ⟹ card bl ≥ 2"
shows "pairwise_balance (del_point x) (del_point_blocks x) Λ"
proof (cases "x ∈ 𝒱")
case True
interpret des: design "del_point x" "del_point_blocks x"
using delete_point_design assms by blast
show ?thesis using assms design_blocks_nempty del_point_def del_point_blocks_def
proof (unfold_locales, simp_all)
show "2 < 𝗏 ⟹ (⋀bl. bl ∈# ℬ ⟹ 2 ≤ card bl) ⟹ 2 ≤ (card (𝒱 - {x}))"
using card_Diff_singleton_if diff_diff_cancel diff_le_mono2 finite_sets less_one
by (metis diff_is_0_eq neq0_conv t_lt_order zero_less_diff)
have "⋀ ps . ps ⊆ 𝒱 - {x} ⟹ ps ⊆ 𝒱" by auto
then show "⋀ps. ps ⊆ 𝒱 - {x} ⟹ card ps = 2 ⟹ {#bl - {x}. bl ∈# ℬ#} index ps = Λ"
using delete_point_index_eq del_point_def del_point_blocks_def by simp
qed
next
case False
then show ?thesis
by (simp add: del_invalid_point del_invalid_point_blocks pairwise_balance_axioms)
qed
end
context k_GDD
begin
lemma bibd_from_kGDD:
assumes "𝗄 > 1"
assumes "⋀ g. g ∈ 𝒢 ⟹ card g = 𝗄 - 1"
assumes " x ∉ 𝒱"
shows "bibd (add_point x) (ℬ + mset_set { insert x g | g. g ∈ 𝒢}) (𝗄) 1"
proof -
have "⋀ k . k∈ {𝗄} ⟹ k = 𝗄" by blast
then have kge: "⋀ k . k∈ {𝗄} ⟹ k ≥ 2" using assms(1) by simp
have "⋀ g . g ∈ 𝒢 ⟹ card g + 1 = 𝗄" using assms k_non_zero by auto
then have s: "({𝗄} ∪ {(card g) + 1 | g . g ∈ 𝒢}) = {𝗄}" by auto
then interpret pbd: PBD "(add_point x)" "ℬ + mset_set { insert x g | g. g ∈ 𝒢}" "{𝗄}"
using PBD_by_adjoining_point[of "x"] kge assms by (smt (z3) Collect_cong)
show ?thesis using assms pbd.block_sizes block_size_lt_v finite_sets add_point_def
by (unfold_locales) (simp_all)
qed
end
context PBD
begin
lemma pbd_points_index1: "ps ⊆ 𝒱 ⟹ card ps = 2 ⟹ ℬ index ps = 1"
using balanced by simp
lemma pbd_index1_points_imply_unique_block:
assumes "b1 ∈# ℬ" and "b2 ∈# ℬ" and "b1 ≠ b2"
assumes "x ≠ y" and "{x, y} ⊆ b1" and "x ∈ b2"
shows "y ∉ b2"
proof (rule ccontr)
let ?ps = "{# b ∈# ℬ . {x, y} ⊆ b#}"
assume "¬ y ∉ b2"
then have a: "y ∈ b2" by linarith
then have "{x, y} ⊆ b2"
by (simp add: assms(6))
then have "b1 ∈# ?ps" and "b2 ∈# ?ps" using assms by auto
then have ss: "{#b1, b2#} ⊆# ?ps" using assms
by (metis insert_noteq_member mset_add mset_subset_eq_add_mset_cancel single_subset_iff)
have "size {#b1, b2#} = 2" using assms by auto
then have ge2: "size ?ps ≥ 2" using assms ss by (metis size_mset_mono)
have pair: "card {x, y} = 2" using assms by auto
have "{x, y} ⊆ 𝒱" using assms wellformed by auto
then have "ℬ index {x, y} = 1" using pbd_points_index1 pair by simp
then show False using points_index_def ge2
by (metis numeral_le_one_iff semiring_norm(69))
qed
lemma strong_delete_point_groups_index_zero:
assumes "G ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
assumes "xa ∈ G" and "y ∈ G" and "xa ≠ y"
shows "(str_del_point_blocks x) index {xa, y} = 0"
proof (auto simp add: points_index_0_iff str_del_point_blocks_def)
fix b
assume a1: "b ∈# ℬ" and a2: "x ∉ b" and a3: "xa ∈ b" and a4: "y ∈ b"
obtain b' where "G = b' - {x}" and "b' ∈# ℬ" and "x ∈ b'" using assms by blast
then show False using a1 a2 a3 a4 assms pbd_index1_points_imply_unique_block
by fastforce
qed
lemma strong_delete_point_groups_index_one:
assumes "G1 ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
assumes "G2 ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
assumes "G1 ≠ G2" and "xa ∈ G1" and "y ∈ G2"
shows "(str_del_point_blocks x) index {xa, y} = 1"
proof -
obtain b1 where gb1: "G1 = b1 - {x}" and b1in: "b1 ∈# ℬ" and xin1: "x ∈ b1" using assms by blast
obtain b2 where gb2: "G2 = b2 - {x}" and b2in: "b2 ∈# ℬ" and xin2:"x ∈ b2" using assms by blast
have bneq: "b1 ≠ b2 " using assms(3) gb1 gb2 by auto
have "xa ≠ y" using gb1 b1in xin1 gb2 b2in xin2 assms(3) assms(4) assms(5) insert_subset
by (smt (verit, best) Diff_eq_empty_iff Diff_iff empty_Diff insertCI pbd_index1_points_imply_unique_block)
then have pair: "card {xa, y} = 2" by simp
have inv: "{xa, y} ⊆ 𝒱" using gb1 b1in gb2 b2in assms(4) assms(5)
by (metis Diff_cancel Diff_subset insert_Diff insert_subset wellformed)
have "{# bl ∈# ℬ . x ∈ bl#} index {xa, y} = 0"
proof (auto simp add: points_index_0_iff)
fix b assume a1: "b ∈# ℬ" and a2: "x ∈ b" and a3: "xa ∈ b" and a4: "y ∈ b"
then have yxss: "{y, x} ⊆ b2"
using assms(5) gb2 xin2 by blast
have "{xa, x} ⊆ b1"
using assms(4) gb1 xin1 by auto
then have "xa ∉ b2" using pbd_index1_points_imply_unique_block
by (metis DiffE assms(4) b1in b2in bneq gb1 singletonI xin2)
then have "b2 ≠ b" using a3 by auto
then show False using pbd_index1_points_imply_unique_block
by (metis DiffD2 yxss a1 a2 a4 assms(5) b2in gb2 insertI1)
qed
then have "(str_del_point_blocks x) index {xa, y} = ℬ index {xa, y}"
by (metis multiset_partition plus_nat.add_0 point_index_distrib str_del_point_blocks_def)
thus ?thesis using pbd_points_index1 pair inv by fastforce
qed
lemma blocks_with_x_partition:
assumes "x ∈ 𝒱"
shows "partition_on (𝒱 - {x}) {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
proof (intro partition_onI )
have gtt: "⋀ bl. bl ∈# ℬ ⟹ card bl ≥ 2" using block_size_gt_t
by (simp add: block_sizes nat_int_comparison(3))
show "⋀p. p ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b} ⟹ p ≠ {}"
proof -
fix p assume "p ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
then obtain b where ptx: "p = b - {x}" and "b ∈# ℬ" and xinb: "x ∈ b" by blast
then have ge2: "card b ≥ 2" using gtt by (simp add: nat_int_comparison(3))
then have "finite b" by (metis card.infinite not_numeral_le_zero)
then have "card p = card b - 1" using xinb ptx by simp
then have "card p ≥ 1" using ge2 by linarith
thus "p ≠ {}" by auto
qed
show "⋃ {b - {x} |b. b ∈# ℬ ∧ x ∈ b} = 𝒱 - {x}"
proof (intro subset_antisym subsetI)
fix xa
assume "xa ∈ ⋃ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
then obtain b where "xa ∈ b" and "b ∈# ℬ" and "x ∈ b" and "xa ≠ x" by auto
then show "xa ∈ 𝒱 - {x}" using wf_invalid_point by blast
next
fix xa
assume a: "xa ∈ 𝒱 - {x}"
then have nex: "xa ≠ x" by simp
then have pair: "card {xa, x} = 2" by simp
have "{xa, x} ⊆ 𝒱" using a assms by auto
then have "card {b ∈ design_support . {xa, x} ⊆ b} = 1"
using balanced points_index_simple_def pbd_points_index1 assms by (metis pair)
then obtain b where des: "b ∈ design_support" and ss: "{xa, x} ⊆ b"
by (metis (no_types, lifting) card_1_singletonE mem_Collect_eq singletonI)
then show "xa ∈ ⋃ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
using des ss nex design_support_def by auto
qed
show "⋀p p'. p ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b} ⟹ p' ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b} ⟹
p ≠ p' ⟹ p ∩ p' = {}"
proof -
fix p p'
assume p1: "p ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}" and p2: "p' ∈ {b - {x} |b. b ∈# ℬ ∧ x ∈ b}"
and pne: "p ≠ p'"
then obtain b where b1: "p = b - {x}" and b1in:"b ∈# ℬ" and xinb1:"x ∈ b" by blast
then obtain b' where b2: "p' = b' - {x}" and b2in: "b' ∈# ℬ" and xinb2: "x ∈ b'"
using p2 by blast
then have "b ≠ b'" using pne b1 by auto
then have "⋀ y. y ∈ b ⟹ y ≠ x ⟹ y ∉ b'"
using b1in b2in xinb1 xinb2 pbd_index1_points_imply_unique_block
by (meson empty_subsetI insert_subset)
then have "⋀ y. y ∈ p ⟹ y ∉ p'"
by (metis Diff_iff b1 b2 insertI1)
then show "p ∩ p' = {}" using disjoint_iff by auto
qed
qed
lemma KGDD_by_deleting_point:
assumes "x ∈ 𝒱"
assumes "ℬ rep x < 𝖻"
assumes "ℬ rep x > 1"
shows "K_GDD (del_point x) (str_del_point_blocks x) 𝒦 { b - {x} | b . b ∈# ℬ ∧ x ∈ b}"
proof -
have "⋀ bl. bl ∈# ℬ ⟹ card bl ≥ 2" using block_size_gt_t
by (simp add: block_sizes nat_int_comparison(3))
then interpret des: proper_design "(del_point x)" "(str_del_point_blocks x)"
using strong_delete_point_proper assms by blast
show ?thesis using blocks_with_x_partition strong_delete_point_groups_index_zero
strong_delete_point_groups_index_one str_del_point_blocks_def del_point_def
proof (unfold_locales, simp_all add: block_sizes positive_ints assms)
have ge1: "card {b . b ∈# ℬ ∧ x ∈ b} > 1"
using assms(3) replication_num_simple_def design_support_def by auto
have fin: "finite {b . b ∈# ℬ ∧ x ∈ b}" by simp
have inj: "inj_on (λ b . b - {x}) {b . b ∈# ℬ ∧ x ∈ b}"
using assms(2) inj_on_def mem_Collect_eq by auto
then have "card {b - {x} |b. b ∈# ℬ ∧ x ∈ b} = card {b . b ∈# ℬ ∧ x ∈ b}"
using card_image fin by (simp add: inj card_image setcompr_eq_image)
then show "Suc 0 < card {b - {x} |b. b ∈# ℬ ∧ x ∈ b}" using ge1
by presburger
qed
qed
lemma card_singletons_eq: "card {{a} | a . a ∈ A} = card A"
by (simp add: card_image Setcompr_eq_image)
lemma KGDD_from_PBD: "K_GDD 𝒱 ℬ 𝒦 {{x} | x . x ∈ 𝒱}"
proof (unfold_locales,auto simp add: Setcompr_eq_image partition_on_singletons)
have "card ((λx. {x}) ` 𝒱) ≥ 2" using t_lt_order card_singletons_eq
by (metis Collect_mem_eq setcompr_eq_image)
then show "Suc 0 < card ((λx. {x}) ` 𝒱)" by linarith
show "⋀xa xb. xa ∈ 𝒱 ⟹ xb ∈ 𝒱 ⟹ ℬ index {xa, xb} ≠ Suc 0 ⟹ xa = xb"
proof (rule ccontr)
fix xa xb
assume ain: "xa ∈ 𝒱" and bin: "xb ∈ 𝒱" and ne1: "ℬ index {xa, xb} ≠ Suc 0"
assume "xa ≠ xb"
then have "card {xa, xb} = 2" by auto
then have "ℬ index {xa, xb} = 1"
by (simp add: ain bin)
thus False using ne1 by linarith
qed
qed
end
context bibd
begin
lemma kGDD_from_bibd:
assumes "Λ = 1"
assumes "x ∈ 𝒱"
shows "k_GDD (del_point x) (str_del_point_blocks x) 𝗄 { b - {x} | b . b ∈# ℬ ∧ x ∈ b}"
proof -
interpret pbd: PBD 𝒱 ℬ "{𝗄}" using assms
using PBD.intro Λ_PBD_axioms by auto
have lt: "ℬ rep x < 𝖻" using block_num_gt_rep
by (simp add: assms(2))
have "ℬ rep x > 1" using r_ge_two assms by simp
then interpret kgdd: K_GDD "(del_point x)" "str_del_point_blocks x"
"{𝗄}" "{ b - {x} | b . b ∈# ℬ ∧ x ∈ b}"
using pbd.KGDD_by_deleting_point lt assms by blast
show ?thesis using del_point_def str_del_point_blocks_def by (unfold_locales) (simp_all)
qed
end
end