Theory Design_Theory.Group_Divisible_Designs

(* Title: Group_Divisible_Designs.thy
   Author: Chelsea Edmonds
*)

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