diff --git a/thys/Design_Theory/BIBD.thy b/thys/Design_Theory/BIBD.thy --- a/thys/Design_Theory/BIBD.thy +++ b/thys/Design_Theory/BIBD.thy @@ -1,943 +1,977 @@ (* Title: BIBD Author: Chelsea Edmonds *) theory BIBD imports Block_Designs begin section \BIBD's\ text \BIBD's are perhaps the most commonly studied type of design in combinatorial design theory, and usually the first type of design explored in a design theory course. These designs are a type of t-design, where $t = 2$\ subsection \BIBD Basics\ locale bibd = t_design \ \ \ 2 \ for point_set ("\") and block_collection ("\") and u_block_size ("\") and index ("\") begin lemma min_block_size_2: "\ \ 2" using block_size_t by simp lemma points_index_pair: "y \ \ \ x \ \ \ x \ y \ size ({# bl \# \ . {x, y} \ bl#}) = \" - using balanced card_2_iff empty_subsetI insert_subset points_index_def - by (metis of_nat_numeral) + using balanced card_2_iff empty_subsetI insert_subset points_index_def by metis lemma index_one_empty_rm_blv [simp]: assumes "\ = 1" and " blv \# \" and "p \ blv" and "card p = 2" shows "{#bl \# remove1_mset blv \ . p \ bl#} = {#}" proof - have blv_in: "blv \# filter_mset ((\) p) \" using assms by simp have "p \ \" using assms wellformed by auto then have "size (filter_mset ((\) p) \) = 1" using balanced assms by (simp add: points_index_def) then show ?thesis using blv_in filter_diff_mset filter_single_mset by (metis (no_types, lifting) add_mset_eq_single assms(3) insert_DiffM size_1_singleton_mset) qed lemma index_one_alt_bl_not_exist: assumes "\ = 1" and " blv \# \" and "p \ blv" and "card p = 2" shows" \ bl. bl \# remove1_mset blv \ \ \ (p \ bl) " using index_one_empty_rm_blv by (metis assms(1) assms(2) assms(3) assms(4) filter_mset_empty_conv) subsection \Necessary Conditions for Existence\ text \The necessary conditions on the existence of a $(v, k, \lambda)$-bibd are one of the fundamental first theorems on designs. Proofs based off MATH3301 lecture notes \cite{HerkeLectureNotes2016} and Stinson \cite{stinsonCombinatorialDesignsConstructions2004}\ lemma necess_cond_1_rhs: assumes "x \ \" shows "size ({# p \# (mset_set (\ - {x}) \# {# bl \# \ . x \ bl #}). fst p \ snd p#}) = \ * (\- 1)" proof - let ?M = "mset_set (\ - {x})" let ?B = "{# bl \# \ . x \ bl #}" have m_distinct: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp have y_point: "\ y . y \# ?M \ y \ \" using assms by (simp add: finite_sets) have b_contents: "\ bl. bl \# ?B \ x \ bl" using assms by auto have "\ y. y \# ?M \ y \ x" using assms by (simp add: finite_sets) - then have "\ y .y \# ?M \ size ({# bl \# ?B . {x, y} \ bl#}) = nat \" - using points_index_pair filter_filter_mset_ss_member y_point assms finite_sets index_ge_zero - by (metis nat_0_le nat_int_comparison(1)) - then have "\ y .y \# ?M \ size ({# bl \# ?B . x \ bl \ y \ bl#}) = nat \" + then have "\ y .y \# ?M \ size ({# bl \# ?B . {x, y} \ bl#}) = \" + using points_index_pair filter_filter_mset_ss_member y_point assms finite_sets + by metis + then have "\ y .y \# ?M \ size ({# bl \# ?B . x \ bl \ y \ bl#}) = \" by auto - then have bl_set_size: "\ y . y \# ?M \ size ({# bl \# ?B . y \ bl#}) = nat \" + then have bl_set_size: "\ y . y \# ?M \ size ({# bl \# ?B . y \ bl#}) = \" using b_contents by (metis (no_types, lifting) filter_mset_cong) - then have final_size: "size (\p\#?M . ({#p#} \# {#bl \# ?B. p \ bl#})) = size (?M) * (nat \)" - using m_distinct size_Union_distinct_cart_prod_filter bl_set_size index_ge_zero by blast + then have final_size: "size (\p\#?M . ({#p#} \# {#bl \# ?B. p \ bl#})) = size (?M) * \" + using m_distinct size_Union_distinct_cart_prod_filter bl_set_size by blast have "size ?M = \ - 1" using v_non_zero by (simp add: assms(1) finite_sets) thus ?thesis using final_size - by (simp add: set_break_down_left index_ge_zero) + by (simp add: set_break_down_left) qed lemma necess_cond_1_lhs: assumes "x \ \" shows "size ({# p \# (mset_set (\ - {x}) \# {# bl \# \ . x \ bl #}). fst p \ snd p#}) = (\ rep x) * (\ - 1)" (is "size ({# p \# (?M \# ?B). fst p \ snd p#}) = (\ rep x) * (\ - 1) ") proof - have "\ y. y \# ?M \ y \ x" using assms by (simp add: finite_sets) have distinct_m: "distinct_mset ?M" using assms mset_points_distinct_diff_one by simp have finite_M: "finite (\ - {x})" using finite_sets by auto have block_choices: "size ?B = \ rep x" by (simp add: assms(1) point_replication_number_def) have bl_size: "\ bl \# ?B. card {p \ \ . p \ bl } = \ " using uniform_unfold_point_set by simp have x_in_set: "\ bl \# ?B . {x} \ {p \ \. p \ bl}" using assms by auto then have "\ bl \# ?B. card {p \ (\ - {x}) . p \ bl } = card ({p \ \ . p \ bl } - {x})" by (simp add: set_filter_diff_card) then have "\ bl \# ?B. card {p \ (\ - {x}) . p \ bl } = \ - 1" using bl_size x_in_set card_Diff_subset finite_sets k_non_zero by auto - then have "\ bl . bl \# ?B \ size {#p \# ?M . p \ bl#} = nat (\ - 1)" + then have "\ bl . bl \# ?B \ size {#p \# ?M . p \ bl#} = \ - 1" using assms finite_M card_size_filter_eq by auto - then have "size (\bl\#?B. ( {# p \# ?M . p \ bl #} \# {#bl#})) = size (?B) * nat (\ - 1)" + then have "size (\bl\#?B. ( {# p \# ?M . p \ bl #} \# {#bl#})) = size (?B) * (\ - 1)" using distinct_m size_Union_distinct_cart_prod_filter2 by blast thus ?thesis using block_choices k_non_zero by (simp add: set_break_down_right) qed lemma r_constant: "x \ \ \ (\ rep x) * (\ -1) = \ * (\ - 1)" using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty by force lemma replication_number_value: assumes "x \ \" shows "(\ rep x) = \ * (\ - 1) div (\ - 1)" - using min_block_size_2 r_constant assms diff_gt_0_iff_gt diff_self zle_diff1_eq numeral_le_one_iff - by (metis less_int_code(1) linorder_neqE_linordered_idom nonzero_mult_div_cancel_right semiring_norm(69)) + using min_block_size_2 r_constant assms + by (metis diff_is_0_eq diffs0_imp_equal div_by_1 k_non_zero nonzero_mult_div_cancel_right + one_div_two_eq_zero one_le_numeral zero_neq_one) lemma r_constant_alt: "\ x \ \. \ rep x = \ * (\ - 1) div (\ - 1)" using r_constant replication_number_value by blast end text \Using the first necessary condition, it is possible to show that a bibd has a constant replication number\ sublocale bibd \ constant_rep_design \ \ "(\ * (\ - 1) div (\ - 1))" using r_constant_alt by (unfold_locales) simp_all lemma (in t_design) bibdI [intro]: "\ = 2 \ bibd \ \ \ \\<^sub>t" using t_lt_order block_size_t by (unfold_locales) (simp_all) context bibd begin abbreviation "\ \ (\ * (\ - 1) div (\ - 1))" lemma necessary_condition_one: shows "\ * (\ - 1) = \ * (\ - 1)" using necess_cond_1_rhs necess_cond_1_lhs design_points_nempty rep_number by auto lemma bibd_point_occ_rep: assumes "x \ bl" assumes "bl \# \" shows "(\ - {#bl#}) rep x = \ - 1" proof - have xin: "x \ \" using assms wf_invalid_point by blast then have rep: "size {# blk \# \. x \ blk #} = \" using rep_number_unfold_set by simp have "(\ - {#bl#}) rep x = size {# blk \# (\ - {#bl#}). x \ blk #}" by (simp add: point_replication_number_def) then have "(\ - {#bl#}) rep x = size {# blk \# \. x \ blk #} - 1" by (simp add: assms size_Diff_singleton) then show ?thesis using assms rep r_gzero by simp qed lemma necess_cond_2_lhs: "size {# x \# (mset_set \ \# \) . (fst x) \ (snd x) #} = \ * \" proof - let ?M = "mset_set \" - have "\ p . p \# ?M \ size ({# bl \# \ . p \ bl #}) = nat (\)" + have "\ p . p \# ?M \ size ({# bl \# \ . p \ bl #}) = \" using finite_sets rep_number_unfold_set r_gzero nat_eq_iff2 by auto - then have "size (\p\#?M. ({#p#} \# {#bl \# \. p \ bl#})) = size ?M * nat (\)" + then have "size (\p\#?M. ({#p#} \# {#bl \# \. p \ bl#})) = size ?M * (\)" using mset_points_distinct size_Union_distinct_cart_prod_filter by blast thus ?thesis using r_gzero by (simp add: set_break_down_left) qed lemma necess_cond_2_rhs: "size {# x \# (mset_set \ \# \) . (fst x) \ (snd x) #} = \*\" (is "size {# x \# (?M \# ?B). (fst x) \ (snd x) #} = \*\") proof - - have "\ bl . bl \# ?B \ size ({# p \# ?M . p \ bl #}) = nat \" + have "\ bl . bl \# ?B \ size ({# p \# ?M . p \ bl #}) = \" using uniform k_non_zero uniform_unfold_point_set_mset by fastforce - then have "size (\bl\#?B. ( {# p \# ?M . p \ bl #} \# {#bl#})) = size (?B) * (nat \)" + then have "size (\bl\#?B. ( {# p \# ?M . p \ bl #} \# {#bl#})) = size (?B) * \" using mset_points_distinct size_Union_distinct_cart_prod_filter2 by blast thus ?thesis using k_non_zero by (simp add: set_break_down_right) qed lemma necessary_condition_two: shows "\ * \ = \ * \" using necess_cond_2_lhs necess_cond_2_rhs by simp theorem admissability_conditions: "\ * (\ - 1) = \ * (\ - 1)" "\ * \ = \ * \" using necessary_condition_one necessary_condition_two by auto subsubsection \BIBD Param Relationships\ lemma bibd_block_number: "\ = \ * \ * (\ - 1) div (\ * (\-1))" proof - have "\ * \ = (\ * \)" using necessary_condition_two by simp then have k_dvd: "\ dvd (\ * \)" by (metis dvd_triv_right) then have "\ = (\ * \) div \" using necessary_condition_two min_block_size_2 by auto then have "\ = (\ * ((\ * (\ - 1) div (\ - 1)))) div \" by simp then have "\ = (\ * \ * (\ - 1)) div ((\ - 1)* \)" using necessary_condition_one - necessary_condition_two dvd_div_div_eq_mult dvd_div_eq_0_iff - by (smt (z3) dvd_triv_right mult.assoc mult.commute mult.left_commute mult_eq_0_iff ) + necessary_condition_two dvd_div_div_eq_mult dvd_div_eq_0_iff dvd_triv_right mult.assoc + mult.commute mult.left_commute mult_eq_0_iff + by (smt (z3) b_non_zero) then show ?thesis by (simp add: mult.commute) qed lemma symmetric_condition_1: "\ * (\ - 1) = \ * (\ - 1) \ \ = \ \ \ = \" using b_non_zero bibd_block_number mult_eq_0_iff necessary_condition_two necessary_condition_one by auto lemma index_lt_replication: "\ < \" proof - have 1: "\ * (\ - 1) = \ * (\ - 1)" using admissability_conditions by simp have lhsnot0: "\ * (\ - 1) \ 0" - using no_zero_divisors rep_not_zero zdiv_eq_0_iff by blast - then have rhsnot0: "\ * (\ - 1) \ 0" using 1 by simp + using no_zero_divisors rep_not_zero by (metis div_by_0) + then have rhsnot0: "\ * (\ - 1) \ 0" using 1 by presburger have "\ - 1 < \ - 1" using incomplete b_non_zero bibd_block_number not_less_eq by fastforce - thus ?thesis using 1 lhsnot0 rhsnot0 - by (smt (verit, best) k_non_zero mult_le_less_imp_less r_gzero) + thus ?thesis using 1 lhsnot0 rhsnot0 k_non_zero mult_le_less_imp_less r_gzero + by (metis div_greater_zero_iff less_or_eq_imp_le nat_less_le nat_neq_iff) qed lemma index_not_zero: "\ \ 1" - using index_ge_zero index_lt_replication int_one_le_iff_zero_less by fastforce + by (metis div_0 leI less_one mult_not_zero rep_not_zero) lemma r_ge_two: "\ \ 2" using index_lt_replication index_not_zero by linarith lemma block_num_gt_rep: "\ > \" proof - have fact: "\ * \ = \ * \" using admissability_conditions by auto have lhsnot0: "\ * \ \ 0" using k_non_zero b_non_zero by auto then have rhsnot0: "\ * \ \ 0" using fact by simp then show ?thesis using incomplete lhsnot0 using complement_rep_number constant_rep_design.r_gzero incomplete_imp_incomp_block by fastforce qed lemma bibd_subset_occ: assumes "x \ bl" and "bl \# \" and "card x = 2" shows "size {# blk \# (\ - {#bl#}). x \ blk #} = \ - 1" proof - have index: "size {# blk \# \. x \ blk #} = \" using points_index_def balanced assms - by (metis (full_types) of_nat_numeral subset_eq wf_invalid_point) + by (metis (full_types) subset_eq wf_invalid_point) then have "size {# blk \# (\ - {#bl#}). x \ blk #} = size {# blk \# \. x \ blk #} - 1" by (simp add: assms size_Diff_singleton) then show ?thesis using assms index_not_zero index by simp qed lemma necess_cond_one_param_balance: "\ > \ \ \ > \" - using necessary_condition_two - by (smt mult_nonneg_nonneg nonzero_mult_div_cancel_right of_nat_0_le_iff r_gzero zdiv_mono2) + using necessary_condition_two b_positive + by (metis div_le_mono2 div_mult_self1_is_m div_mult_self_is_m nat_less_le r_gzero v_non_zero) subsection \Constructing New bibd's\ text \There are many constructions on bibd's to establish new bibds (or other types of designs). This section demonstrates this using both existing constructions, and by defining new constructions.\ subsubsection \BIBD Complement, Multiple, Combine\ lemma comp_params_index_pair: assumes "{x, y} \ \" assumes "x \ y" shows "\\<^sup>C index {x, y} = \ + \ - 2*\" proof - have xin: "x \ \" and yin: "y \ \" using assms by auto have ge: "2*\ \ \" using index_lt_replication using r_gzero by linarith - have "size {# b \# \ . x \ b \ y \ b#} = \" using points_index_pair assms by simp - then have lambda: "size {# b \# \ . x \ b \ y \ b#} = nat \" - using index_ge_zero by auto - have "\\<^sup>C index {x, y} = size {# b \# \ . x \ b \ y \ b #}" + have lambda: "size {# b \# \ . x \ b \ y \ b#} = \" using points_index_pair assms by simp + have s1: "\\<^sup>C index {x, y} = size {# b \# \ . x \ b \ y \ b #}" using complement_index_2 assms by simp - also have "\ = size \ - (size {# b \# \ . \ (x \ b \ y \ b) #})" + also have s2: "... = size \ - (size {# b \# \ . \ (x \ b \ y \ b) #})" using size_filter_neg by blast also have "... = size \ - (size {# b \# \ . x \ b \ y \ b#})" by auto also have "... = \ - (size {# b \# \ . x \ b \ y \ b#})" by (simp add: of_nat_diff) - also have "... = \ - (size {# b \# \ . x \ b#} + + finally have "\\<^sup>C index {x, y} = \ - (size {# b \# \ . x \ b#} + size {# b \# \ . y \ b#} - size {# b \# \ . x \ b \ y \ b#})" - by (simp add: mset_size_partition_dep) - also have "... = \ - (nat \ + nat \ - nat (\))" using rep_number_unfold_set lambda xin yin - by (metis (no_types, lifting) nat_int) - finally have "\\<^sup>C index {x, y} = \ - (2*\ - \)" - using index_ge_zero index_lt_replication by linarith + by (simp add: mset_size_partition_dep s2 s1) + then have "\\<^sup>C index {x, y} = \ - (\ + \ - \)" using rep_number_unfold_set lambda xin yin + by presburger + then have "\\<^sup>C index {x, y} = \ - (2*\ - \)" + using index_lt_replication by (metis mult_2) thus ?thesis using ge diff_diff_right by simp qed lemma complement_bibd_index: assumes "ps \ \" assumes "card ps = 2" shows "\\<^sup>C index ps = \ + \ - 2*\" proof - obtain x y where set: "ps = {x, y}" using b_non_zero bibd_block_number diff_is_0_eq incomplete mult_0_right nat_less_le design_points_nempty assms by (metis card_2_iff) then have "x \ y" using assms by auto thus ?thesis using comp_params_index_pair assms by (simp add: set) qed lemma complement_bibd: assumes "\ \ \ - 2" shows "bibd \ \\<^sup>C (\ - \) (\ + \ - 2*\)" proof - interpret des: incomplete_design \ "\\<^sup>C" "(\ - \)" using assms complement_incomplete by blast show ?thesis proof (unfold_locales, simp_all) show "2 \ des.\" using assms block_size_t by linarith show "\ps. ps \ \ \ card ps = 2 \ - \\<^sup>C index ps = \ + \ - 2 * (\ * (des.\ - 1) div (\ - 1))" + \\<^sup>C index ps = \ + \ - 2 * (\ * (des.\ - Suc 0) div (\ - Suc 0))" using complement_bibd_index by simp show "2 \ des.\ - \" using assms block_size_t by linarith qed qed lemma multiple_bibd: "n > 0 \ bibd \ (multiple_blocks n) \ (\ * n)" using multiple_t_design by (simp add: bibd_def) end locale two_bibd_eq_points = two_t_designs_eq_points \ \ \ \' 2 \ \' + des1: bibd \ \ \ \ + des2: bibd \ \' \ \' for \ \ \ \' \ \' begin lemma combine_is_bibd: "bibd \\<^sup>+ \\<^sup>+ \ (\ + \')" by (unfold_locales) sublocale combine_bibd: bibd "\\<^sup>+" "\\<^sup>+" "\" "(\ + \')" by (unfold_locales) end subsubsection \Derived Designs\ text \A derived bibd takes a block from a valid bibd as the new point sets, and the intersection of that block with other blocks as it's block set\ locale bibd_block_transformations = bibd + fixes block :: "'a set" ("bl") assumes valid_block: "bl \# \" begin definition derived_blocks :: "'a set multiset" ("(\\<^sup>D)") where "\\<^sup>D \ {# bl \ b . b \# (\ - {#bl#}) #}" lemma derive_define_flip: "{# b \ bl . b \# (\ - {#bl#}) #} = \\<^sup>D" by (simp add: derived_blocks_def inf_sup_aci(1)) lemma derived_points_order: "card bl = \" using uniform valid_block by simp lemma derived_block_num: "bl \# \ \ size \\<^sup>D = \ - 1" - apply (simp add: derived_blocks_def size_remove1_mset_If valid_block) - using valid_block int_ops(6) by fastforce + by (simp add: derived_blocks_def size_remove1_mset_If valid_block) lemma derived_is_wellformed: "b \# \\<^sup>D \ b \ bl" by (simp add: derived_blocks_def valid_block) (auto) lemma derived_point_subset_orig: "ps \ bl \ ps \ \" by (simp add: valid_block incomplete_imp_proper_subset subset_psubset_trans) lemma derived_obtain_orig_block: assumes "b \# \\<^sup>D" obtains b2 where "b = b2 \ bl" and "b2 \# remove1_mset bl \" using assms derived_blocks_def by auto sublocale derived_incidence_sys: incidence_system "bl" "\\<^sup>D" using derived_is_wellformed valid_block by (unfold_locales) (auto) sublocale derived_fin_incidence_system: finite_incidence_system "bl" "\\<^sup>D" using valid_block finite_blocks by (unfold_locales) simp_all lemma derived_blocks_nempty: assumes "\ b .b \# remove1_mset bl \ \ bl |\| b > 0" assumes "bld \# \\<^sup>D" shows "bld \ {}" proof - obtain bl2 where inter: "bld = bl2 \ bl" and member: "bl2 \# remove1_mset bl \" using assms derived_obtain_orig_block by blast then have "bl |\| bl2 > 0" using assms(1) by blast thus ?thesis using intersection_number_empty_iff finite_blocks valid_block by (metis Int_commute dual_order.irrefl inter) qed lemma derived_is_design: assumes "\ b. b \# remove1_mset bl \ \ bl |\| b > 0" shows "design bl \\<^sup>D" proof - interpret fin: finite_incidence_system "bl" "\\<^sup>D" by (unfold_locales) show ?thesis using assms derived_blocks_nempty by (unfold_locales) simp qed lemma derived_is_proper: assumes "\ b. b \# remove1_mset bl \ \ bl |\| b > 0" shows "proper_design bl \\<^sup>D" proof - interpret des: design "bl" "\\<^sup>D" using derived_is_design assms by fastforce have "\ - 1 > 1" using block_num_gt_rep r_ge_two by linarith then show ?thesis by (unfold_locales) (simp add: derived_block_num valid_block) qed subsubsection \Residual Designs\ text \Similar to derived designs, a residual design takes the complement of a block bl as it's new point set, and the complement of all other blocks with respect to bl.\ definition residual_blocks :: "'a set multiset" ("(\\<^sup>R)") where "\\<^sup>R \ {# b - bl . b \# (\ - {#bl#}) #}" lemma residual_order: "card (bl\<^sup>c) = \ - \" - apply (simp add: valid_block wellformed block_complement_size) - using block_size_lt_v derived_points_order by auto + by (simp add: valid_block wellformed block_complement_size) lemma residual_block_num: "size (\\<^sup>R) = \ - 1" using b_positive by (simp add: residual_blocks_def size_remove1_mset_If valid_block int_ops(6)) lemma residual_obtain_orig_block: assumes "b \# \\<^sup>R" obtains bl2 where "b = bl2 - bl" and "bl2 \# remove1_mset bl \" using assms residual_blocks_def by auto lemma residual_blocks_ss: assumes "b \# \\<^sup>R" shows "b \ \" proof - have "b \ (bl\<^sup>c)" using residual_obtain_orig_block by (metis Diff_mono assms block_complement_def in_diffD order_refl wellformed) thus ?thesis using block_complement_subset_points by auto qed lemma residual_blocks_exclude: "b \# \\<^sup>R \ x \ b \ x \ bl" using residual_obtain_orig_block by auto lemma residual_is_wellformed: "b \# \\<^sup>R \ b \ (bl\<^sup>c)" apply (auto simp add: residual_blocks_def) by (metis DiffI block_complement_def in_diffD wf_invalid_point) sublocale residual_incidence_sys: incidence_system "bl\<^sup>c" "\\<^sup>R" using residual_is_wellformed by (unfold_locales) lemma residual_is_finite: "finite (bl\<^sup>c)" by (simp add: block_complement_def finite_sets) sublocale residual_fin_incidence_sys: finite_incidence_system "bl\<^sup>c" "\\<^sup>R" using residual_is_finite by (unfold_locales) lemma residual_blocks_nempty: assumes "bld \# \\<^sup>R" assumes "multiplicity bl = 1" shows "bld \ {}" proof - obtain bl2 where inter: "bld = bl2 - bl" and member: "bl2 \# remove1_mset bl \" using assms residual_blocks_def by auto then have ne: "bl2 \ bl" using assms by (metis count_eq_zero_iff in_diff_count less_one union_single_eq_member) have "card bl2 = card bl" using uniform valid_block member - by (metis in_diffD of_nat_eq_iff) + using in_diffD by fastforce then have "card (bl2 - bl) > 0" using finite_blocks member uniform set_card_diff_ge_zero valid_block by (metis in_diffD ne) thus ?thesis using inter by fastforce qed lemma residual_is_design: "multiplicity bl = 1 \ design (bl\<^sup>c) \\<^sup>R" using residual_blocks_nempty by (unfold_locales) lemma residual_is_proper: assumes "multiplicity bl = 1" shows "proper_design (bl\<^sup>c) \\<^sup>R" proof - interpret des: design "bl\<^sup>c" "\\<^sup>R" using residual_is_design assms by blast have "\ - 1 > 1" using r_ge_two block_num_gt_rep by linarith then show ?thesis using residual_block_num by (unfold_locales) auto qed end subsection \Symmetric BIBD's\ text \Symmetric bibd's are those where the order of the design equals the number of blocks\ locale symmetric_bibd = bibd + assumes symmetric: "\ = \" begin lemma rep_value_sym: "\ = \" using b_non_zero local.symmetric necessary_condition_two by auto lemma symmetric_condition_2: "\ * (\ - 1) = \ * (\ - 1)" using necessary_condition_one rep_value_sym by auto lemma sym_design_vk_gt_kl: assumes "\ \ \ + 2" shows "\ - \ > \ - \" proof (rule ccontr) + define k l v where kdef: "k \ int \" and ldef: "l \ int \" and vdef: "v \ int \" assume "\ (\ - \ > \ - \)" - then have "\ \ 2 * \ - \" - by linarith - then have "\ - 1 \ 2 * \ - \ - 1" by linarith - then have "\* (\ - 1) \ \*( 2 * \ - \ - 1)" - using index_ge_zero mult_le_cancel_left by fastforce - then have "\ * (\ - 1) \ \*( 2 * \ - \ - 1)" - by (simp add: symmetric_condition_2) - then have "\ * (\ - 1) - \*( 2 * \ - \ - 1) \ 0" by linarith - then have "(\ - \)*(\ - \ - 1) \ 0" - by (simp add: mult.commute right_diff_distrib') - then have "\ = \ \ \ = \ + 1" + then have a: "\ (v - k > k - l)" using kdef ldef vdef + by (metis block_size_lt_v index_lt_replication less_imp_le_nat of_nat_diff of_nat_less_imp_less + rep_value_sym) + have lge: "l \ 0" using ldef by simp + have sym: "l * (v- 1) = k * (k - 1)" + using symmetric_condition_2 ldef vdef kdef + by (metis (mono_tags, lifting) block_size_lt_v int_ops(2) k_non_zero le_trans of_nat_diff of_nat_mult) + then have "v \ 2 * k - l" using a by linarith + then have "v - 1 \ 2 * k - l - 1" by linarith + then have "l* (v - 1) \ l*( 2 * k - l - 1)" + using lge mult_le_cancel_left by fastforce + then have "k * (k - 1) \ l*( 2 * k - l - 1)" + by (simp add: sym) + then have "k * (k - 1) - l*( 2 * k - l - 1) \ 0" by linarith + then have "k^2 - k - l* 2 * k + l^2 + l \ 0" using mult.commute right_diff_distrib' + by (smt (z3) mult_cancel_left1 power2_diff ring_class.ring_distribs(2)) + then have "(k - l)*(k - l - 1) \ 0" using mult.commute right_diff_distrib' + by (smt (z3) \k * (k - 1) \ l * (2 * k - l - 1)\ combine_common_factor) + then have "k = l \ k = l + 1" using mult_le_0_iff by force - thus False using assms - by simp + thus False using assms kdef ldef by auto qed end context bibd begin lemma symmetric_bibdI: "\ = \ \ symmetric_bibd \ \ \ \" by unfold_locales simp lemma symmetric_bibdII: "\ * (\ - 1) = \ * (\ - 1) \ symmetric_bibd \ \ \ \" using symmetric_condition_1 by unfold_locales blast lemma symmetric_not_admissable: "\ * (\ - 1) \ \ * (\ - 1) \ \ symmetric_bibd \ \ \ \" using symmetric_bibd.symmetric_condition_2 by blast end context symmetric_bibd begin subsubsection \Intersection Property on Symmetric BIBDs\ text \Below is a proof of an important property on symmetric BIBD's regarding the equivalence of intersection numbers and the design index. This is an intuitive counting proof, and involved significantly more work in a formal environment. Based of Lecture Note \cite{HerkeLectureNotes2016}\ lemma intersect_mult_set_eq_block: assumes "blv \# \" shows "p \# \\<^sub>#{# mset_set (bl \ blv) .bl \# (\ - {#blv#})#} \ p \ blv" proof (auto, simp add: assms finite_blocks) assume assm: "p \ blv" then have "(\ - {#blv#}) rep p > 0" using bibd_point_occ_rep r_ge_two assms by auto then obtain bl where "bl \# (\ - {#blv#}) \ p \ bl" using assms rep_number_g0_exists by metis then show "\x\#remove1_mset blv \. p \# mset_set (x \ blv)" using assms assm finite_blocks by auto qed lemma intersect_mult_set_block_subset_iff: assumes "blv \# \" assumes "p \# \\<^sub>#{# mset_set {y .y \ blv \ b2 \ card y = 2} .b2 \# (\ - {#blv#})#}" shows "p \ blv" proof (rule subsetI) fix x assume asm: "x \ p" obtain b2 where "p \# mset_set {y . y \ blv \ b2 \ card y = 2} \ b2 \#(\ - {#blv#})" using assms by blast then have "p \ blv \ b2" by (metis (no_types, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq) thus "x \ blv" using asm by auto qed lemma intersect_mult_set_block_subset_card: assumes "blv \# \" assumes "p \# \\<^sub>#{# mset_set {y .y \ blv \ b2 \ card y = 2} .b2 \# (\ - {#blv#})#}" shows "card p = 2" proof - obtain b2 where "p \# mset_set {y . y \ blv \ b2 \ card y = 2} \ b2 \#(\ - {#blv#})" using assms by blast thus ?thesis by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set mem_Collect_eq) qed lemma intersect_mult_set_block_with_point_exists: assumes "blv \# \" and "p \ blv" and "\ \ 2" and "card p = 2" shows "\x\#remove1_mset blv \. p \# mset_set {y. y \ blv \ y \ x \ card y = 2}" proof - have "size {#b \# \ . p \ b#} = \" using points_index_def assms - by (metis balanced_alt_def_all dual_order.trans of_nat_numeral wellformed) + by (metis balanced_alt_def_all dual_order.trans wellformed) then have "size {#bl \# (\ - {#blv#}) . p \ bl#} \ 1" using assms by (simp add: size_Diff_singleton) then obtain bl where "bl \# (\ - {#blv#}) \ p \ bl" using assms filter_mset_empty_conv by (metis diff_diff_cancel diff_is_0_eq' le_numeral_extra(4) size_empty zero_neq_one) thus ?thesis using assms finite_blocks by auto qed lemma intersect_mult_set_block_subset_iff_2: assumes "blv \# \" and "p \ blv" and "\ \ 2" and "card p = 2" shows "p \# \\<^sub>#{# mset_set {y .y \ blv \ b2 \ card y = 2} .b2 \# (\ - {#blv#})#}" by (auto simp add: intersect_mult_set_block_with_point_exists assms) lemma sym_sum_mset_inter_sets_count: assumes "blv \# \" assumes "p \ blv" shows "count (\\<^sub>#{# mset_set (bl \ blv) .bl \# (\ - {#blv#})#}) p = \ - 1" (is "count (\\<^sub>#?M) p = \ - 1") proof - have size_inter: "size {# mset_set (bl \ blv) | bl \# (\ - {#blv#}) . p \ bl#} = \ - 1" using bibd_point_occ_rep point_replication_number_def by (metis assms(1) assms(2) size_image_mset) have inter_finite: "\ bl \# (\ - {#blv#}) . finite (bl \ blv)" by (simp add: assms(1) finite_blocks) have "\ bl . bl \# (\ - {#blv#}) \ p \ bl \ count (mset_set (bl \ blv)) p = 1" using assms count_mset_set(1) inter_finite by simp then have "\ bl . bl \# {#b1 \#(\ - {#blv#}) . p \ b1#} \ count (mset_set (bl \ blv)) p = 1" by (metis (full_types) count_eq_zero_iff count_filter_mset) then have pin: "\ P. P \# {# mset_set (bl \ blv) | bl \# (\ - {#blv#}) . p \ bl#} \ count P p = 1" by blast have "?M = {# mset_set (bl \ blv) | bl \# (\ - {#blv#}) . p \ bl#} + {# mset_set (bl \ blv) | bl \# (\ - {#blv#}) . p \ bl#}" by (metis image_mset_union multiset_partition) then have "count (\\<^sub>#?M) p = size {# mset_set (bl \ blv) | bl \# (\ - {#blv#}) . p \ bl#} " using pin by (auto simp add: count_sum_mset) then show ?thesis using size_inter by linarith qed lemma sym_sum_mset_inter_sets_size: assumes "blv \# \" shows "size (\\<^sub>#{# mset_set (bl \ blv) .bl \# (\ - {#blv#})#}) = \ * (\ - 1)" (is "size (\\<^sub>#?M) = \* (\ - 1)") proof - have eq: "set_mset (\\<^sub>#{# mset_set (bl \ blv) .bl \# (\ - {#blv#})#}) = blv" using intersect_mult_set_eq_block assms by auto then have k: "card (set_mset (\\<^sub>#?M)) = \" by (simp add: assms) have "\ p. p \# (\\<^sub>#?M) \ count (\\<^sub>#?M) p = \ - 1" using sym_sum_mset_inter_sets_count assms eq by blast - thus ?thesis using k size_multiset_int_count by metis + thus ?thesis using k size_multiset_set_mset_const_count by metis qed lemma sym_sum_inter_num: assumes "b1 \# \" shows "(\b2 \#(\ - {#b1#}). b1 |\| b2) = \* (\ - 1)" proof - have "(\b2 \#(\ - {#b1#}). b1 |\| b2) = (\b2 \#(\ - {#b1#}). size (mset_set (b1 \ b2)))" by (simp add: intersection_number_def) also have "... = size (\\<^sub>#{#mset_set (b1 \ bl). bl \# (\ - {#b1#})#})" by (auto simp add: size_big_union_sum) also have "... = size (\\<^sub>#{#mset_set (bl \ b1). bl \# (\ - {#b1#})#})" by (metis Int_commute) finally have "(\b2 \#(\ - {#b1#}). b1 |\| b2) = \ * (\ - 1)" using sym_sum_mset_inter_sets_size assms by auto then show ?thesis by simp qed -lemma choose_two_int: - assumes " x \ 0" - shows "nat (x :: int) choose 2 = ((x ::int) * ( x - 1)) div 2 " - using choose_two assms dvd_div_mult_self even_numeral int_nat_eq mult_cancel_right2 mult_eq_0_iff - mult_nonneg_nonneg nat_diff_distrib' nat_mult_distrib nat_one_as_int - numeral_Bit0_div_2 numerals(1) of_nat_numeral zdiv_int by (smt (verit)) (* Slow *) - lemma sym_sum_mset_inter2_sets_count: assumes "blv \# \" assumes "p \ blv" assumes "card p = 2" shows "count (\\<^sub>#{#mset_set {y .y \ blv \ b2 \ card y = 2}. b2 \# (\ - {#blv#})#}) p = \ - 1" (is "count (\\<^sub>#?M) p = \ - 1") proof - have size_inter: "size {# mset_set {y .y \ blv \ b2 \ card y = 2} | b2 \# (\ - {#blv#}) . p \ b2#} = \ - 1" using bibd_subset_occ assms by simp have "\ b2 \# (\ - {#blv#}) . p \ b2 \ count (mset_set{y .y \ blv \ b2 \ card y = 2}) p = 1" using assms(2) count_mset_set(1) assms(3) by (auto simp add: assms(1) finite_blocks) then have "\ bl \# {#b1 \#(\ - {#blv#}) . p \ b1#}. count (mset_set {y .y \ blv \ bl \ card y = 2}) p = 1" using count_eq_zero_iff count_filter_mset by (metis (no_types, lifting)) then have pin: "\ P \# {# mset_set {y .y \ blv \ b2 \ card y = 2} | b2 \# (\ - {#blv#}) . p \ b2#}. count P p = 1" using count_eq_zero_iff count_filter_mset by blast have "?M = {# mset_set {y .y \ blv \ b2 \ card y = 2} | b2 \# (\ - {#blv#}) . p \ b2#} + {# mset_set {y .y \ blv \ b2 \ card y = 2} | b2 \# (\ - {#blv#}) . \ (p \ b2)#}" by (metis image_mset_union multiset_partition) then have "count (\\<^sub>#?M) p = size {# mset_set {y .y \ blv \ b2 \ card y = 2} | b2 \# (\ - {#blv#}) . p \ b2#}" using pin by (auto simp add: count_sum_mset) then show ?thesis using size_inter by linarith qed lemma sym_sum_mset_inter2_sets_size: assumes "blv \# \" shows "size (\\<^sub>#{#mset_set {y .y \ blv \ b2 \ card y = 2}. b2 \# (\ - {#blv#})#}) = - ((nat \) choose 2) * (\ -1)" - (is "size (\\<^sub>#?M) = ((nat \) choose 2) * (\ -1)") + ( \ choose 2) * (\ -1)" + (is "size (\\<^sub>#?M) = (\ choose 2) * (\ -1)") proof (cases "\ = 1") case True have empty: "\ b2 . b2 \# remove1_mset blv \ \ {y .y \ blv \ y \ b2 \ card y = 2} = {}" using index_one_alt_bl_not_exist assms True by blast then show ?thesis using sum_mset.neutral True by (simp add: empty) next case False then have index_min: "\ \ 2" using index_not_zero by linarith have subset_card: "\ x . x \# (\\<^sub>#?M) \ card x = 2" proof - fix x assume a: "x \# (\\<^sub>#?M)" then obtain b2 where "x \# mset_set {y . y \ blv \ b2 \ card y = 2} \ b2 \#(\ - {#blv#})" by blast thus "card x = 2" using mem_Collect_eq by (metis (mono_tags, lifting) elem_mset_set equals0D infinite_set_mset_mset_set) qed have eq: "set_mset (\\<^sub>#?M) = {bl . bl \ blv \ card bl = 2}" proof show "set_mset (\\<^sub>#?M) \ {bl . bl \ blv \ card bl = 2}" using subset_card intersect_mult_set_block_subset_iff assms by blast show "{bl . bl \ blv \ card bl = 2} \ set_mset (\\<^sub>#?M)" using intersect_mult_set_block_subset_iff_2 assms index_min by blast qed - have "card blv = (nat \)" using uniform assms by (metis nat_int) - then have k: "card (set_mset (\\<^sub>#?M)) = ((nat \) choose 2)" using eq n_subsets + have "card blv = \" using uniform assms by simp + then have k: "card (set_mset (\\<^sub>#?M)) = (\ choose 2)" using eq n_subsets by (simp add: n_subsets assms finite_blocks) - thus ?thesis using k size_multiset_int_count sym_sum_mset_inter2_sets_count assms eq subset_card - by (metis (no_types, lifting) intersect_mult_set_block_subset_iff) + thus ?thesis using k size_multiset_set_mset_const_count sym_sum_mset_inter2_sets_count assms eq + by (metis (no_types, lifting) intersect_mult_set_block_subset_iff subset_card) qed lemma sum_choose_two_inter_num: assumes "b1 \# \" - shows "(\b2 \# (\ - {#b1#}). (nat (b1 |\| b2) choose 2)) = ((\ * (\ - 1) div 2)) * (\ -1)" + shows "(\b2 \# (\ - {#b1#}). ((b1 |\| b2) choose 2)) = ((\ * (\ - 1) div 2)) * (\ -1)" proof - - have div_fact: "2 dvd (\ * (\ - 1))"by simp - have div_fact_2: "2 dvd (\ * (\ - 1))" using symmetric_condition_2 by simp - have "(\b2 \# (\ - {#b1#}). (nat (b1 |\| b2) choose 2)) = (\b2 \# (\ - {#b1#}). nat (b1 |\|\<^sub>2 b2 ))" + have div_fact: "2 dvd (\ * (\ - 1))" + by fastforce + have div_fact_2: "2 dvd (\ * (\ - 1))" using symmetric_condition_2 by fastforce + have "(\b2 \# (\ - {#b1#}). ((b1 |\| b2) choose 2)) = (\b2 \# (\ - {#b1#}). (b1 |\|\<^sub>2 b2 ))" using n_inter_num_choose_design_inter assms by (simp add: in_diffD) - then have sum_fact: "(\b2 \# (\ - {#b1#}).(nat (b1 |\| b2) choose 2)) - = ((nat \) choose 2) * (\ -1)" + then have sum_fact: "(\b2 \# (\ - {#b1#}).((b1 |\| b2) choose 2)) + = (\ choose 2) * (\ -1)" using assms sym_sum_mset_inter2_sets_size by (auto simp add: size_big_union_sum n_intersect_num_subset_def) - have "((nat \) choose 2) * (\ -1) = ((\ * (\ - 1) div 2)) * (\ -1)" - using choose_two_int symmetric_condition_2 k_non_zero by auto - then have "((nat \) choose 2) * (\ -1) = ((\ * (\ - 1) div 2)) * (\ -1)" + have "(\ choose 2) * (\ -1) = ((\ * (\ - 1) div 2)) * (\ -1)" + using choose_two symmetric_condition_2 k_non_zero by auto + then have "(\ choose 2) * (\ -1) = ((\ * (\ - 1) div 2)) * (\ -1)" using div_fact div_fact_2 by (smt div_mult_swap mult.assoc mult.commute) then show ?thesis using sum_fact by simp qed lemma sym_sum_inter_num_sq: assumes "b1 \# \" shows "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = \^2 * ( \ - 1)" proof - - have dvd: "2 dvd (( \ - 1) * (\ * (\ - 1)))" by simp - have a: "(\b2 \#(\ - {#b1#}). int (nat (b1 |\| b2) choose 2)) = + have dvd: "2 dvd (( \ - 1) * (\ * (\ - 1)))" by fastforce + have inner_dvd: "\ bl \# (remove1_mset b1 \). 2 dvd ((b1 |\| bl) * ((b1 |\| bl) - 1))" + by force + have diff_le: "\ bl . bl \# (remove1_mset b1 \) \ (b1 |\| bl) \ (b1 |\| bl)^2" + by (simp add: power2_nat_le_imp_le) + have a: "(\b2 \#(\ - {#b1#}). ((b1 |\| b2) choose 2)) = (\bl \# (remove1_mset b1 \). ((b1 |\| bl) * ((b1 |\| bl) - 1)) div 2)" - using choose_two_int by (simp add: intersection_num_non_neg) - have b: "(\b2 \#(\ - {#b1#}). int (nat (b1 |\| b2) choose 2)) = - (\b2 \#(\ - {#b1#}). (nat (b1 |\| b2) choose 2))" by simp - have "(\b2 \#(\ - {#b1#}). (nat (b1 |\| b2) choose 2)) = ((\ * (\ - 1)) div 2) * ( \ - 1)" + using choose_two by (simp add: intersection_num_non_neg) + have b: "(\b2 \#(\ - {#b1#}). ((b1 |\| b2) choose 2)) = + (\b2 \#(\ - {#b1#}). ((b1 |\| b2) choose 2))" by simp + have gtsq: "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) \ (\bl \# (remove1_mset b1 \). (b1 |\| bl))" + by (simp add: diff_le sum_mset_mono) + have "(\b2 \#(\ - {#b1#}). ((b1 |\| b2) choose 2)) = ((\ * (\ - 1)) div 2) * ( \ - 1)" using sum_choose_two_inter_num assms by blast then have start: "(\bl \# (remove1_mset b1 \). ((b1 |\| bl) * ((b1 |\| bl) - 1)) div 2) = ((\ * (\ - 1)) div 2) * (\ - 1)" using a b by linarith have sum_dvd: "2 dvd (\bl \# (remove1_mset b1 \). (b1 |\| bl) * ((b1 |\| bl) - 1))" - by (simp add: sum_mset_dvd) + using sum_mset_dvd + by (metis (no_types, lifting) dvd_mult dvd_mult2 dvd_refl odd_two_times_div_two_nat) then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl) * ((b1 |\| bl) - 1)) div 2 - = (\ - 1) * ((\ * (\ - 1)) div 2)" - using start by (simp add: sum_mset_distrib_div_if_dvd) + = ((\ * (\ - 1)) div 2) * (\ - 1)" + using start sum_mset_distrib_div_if_dvd inner_dvd + by (metis (mono_tags, lifting) image_mset_cong2) + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl) * ((b1 |\| bl) - 1)) div 2 + = (\ - 1) * ((\ * (\ - 1)) div 2)" + by simp + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl) * ((b1 |\| bl) - 1)) + = (\ - 1) * (\ * (\ - 1))" + by (metis (no_types, lifting) div_mult_swap dvdI dvd_div_eq_iff dvd_mult dvd_mult2 odd_two_times_div_two_nat sum_dvd) + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2 - (b1 |\| bl)) + = (\ - 1) * (\ * (\ - 1))" + using diff_mult_distrib2 + by (metis (no_types, lifting) multiset.map_cong0 nat_mult_1_right power2_eq_square) then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) - - (\bl \# (remove1_mset b1 \). (b1 |\| bl)) = ((\ - 1) * (\ * (\ - 1)))" - using sum_dvd dvd - by (simp add: dvd_div_eq_iff div_mult_swap int_distrib(4) power2_eq_square sum_mset_add_diff) - then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) - (\ * (\ - 1)) = ((\ - 1) * (\ * (\ - 1)))" + - (\bl \# (remove1_mset b1 \). (b1 |\| bl)) = (\ - 1) * (\ * (\ - 1))" + using sum_mset_add_diff_nat[of "(remove1_mset b1 \)" "\ bl . (b1 |\| bl)" "\ bl . (b1 |\| bl)^2"] + diff_le by presburger + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) + = (\bl \# (remove1_mset b1 \). (b1 |\| bl)) + (\ - 1) * (\ * (\ - 1))" using gtsq + by (metis le_add_diff_inverse) + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = (\ * (\ - 1)) + ((\ - 1) * (\ * (\ - 1)))" using sym_sum_inter_num assms rep_value_sym symmetric_condition_2 by auto - then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = (\ * (\ - 1)) * (\ - 1) + (\ * (\ - 1))" - using diff_eq_eq by fastforce - then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = (\ * (\ - 1)) * (\ - 1 + 1)" - using int_distrib(2) by (metis mult_numeral_1_right numeral_One) + then have prev: "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = (\ * (\ - 1)) * (\ - 1) + (\ * (\ - 1))" + by fastforce + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = (\ * (\ - 1)) * (\)" + by (metis Nat.le_imp_diff_is_add add_mult_distrib2 index_not_zero nat_mult_1_right) + then have "(\bl \# (remove1_mset b1 \). (b1 |\| bl)^2) = \ * \ * (\ - 1)" + using mult.commute by simp thus ?thesis by (simp add: power2_eq_square) qed lemma sym_sum_inter_num_to_zero: assumes "b1 \# \" - shows "(\bl \# (remove1_mset b1 \). ((b1 |\| bl) - \)^2) = 0" + shows "(\bl \# (remove1_mset b1 \). (int (b1 |\| bl) - (int \))^2) = 0" proof - have rm1_size: "size (remove1_mset b1 \) = \ - 1" using assms b_non_zero int_ops(6) by (auto simp add: symmetric size_remove1_mset_If) - have "\ bl . bl \# (remove1_mset b1 \) \ ((b1 |\| bl) - \)^2 = - (((b1 |\| bl)^2) - (2 * \ * (b1 |\| bl)) + (\^2))" + have "(\bl \# (remove1_mset b1 \). ((int (b1 |\| bl))^2)) = + (\bl \# (remove1_mset b1 \). (((b1 |\| bl))^2))" by simp + then have ssi: "(\bl \# (remove1_mset b1 \). ((int (b1 |\| bl))^2)) = \^2 * (\ - 1)" + using sym_sum_inter_num_sq assms by simp + have "\ bl . bl \# (remove1_mset b1 \) \ (int (b1 |\| bl) - (int \))^2 = + (((int (b1 |\| bl))^2) - (2 * (int \) * (int (b1 |\| bl))) + ((int \)^2))" by (simp add: power2_diff) - then have "(\bl \# (remove1_mset b1 \). ((b1 |\| bl) - \)^2) = - (\bl \# (remove1_mset b1 \). (((b1 |\| bl)^2) - (2 * \ * (b1 |\| bl)) + (\^2)))" + then have "(\bl \# (remove1_mset b1 \). (int (b1 |\| bl) - (int \))^2) = + (\bl \# (remove1_mset b1 \). (((int (b1 |\| bl))^2) - (2 * (int \) * (int (b1 |\| bl))) + ((int \)^2)))" using sum_over_fun_eq by auto - also have "... = \^2 * (\ - 1) - 2 * \ * (\bl \# (remove1_mset b1 \). ((b1 |\| bl))) - + (\ - 1) * (\^2)" - using sym_sum_inter_num_sq rm1_size - by (simp add: assms sum_mset.distrib sum_mset_add_diff sum_mset_distrib_left) - finally have "(\bl \# (remove1_mset b1 \). ((b1 |\| bl) - \)^2) = 0" - using rep_value_sym symmetric_condition_2 sym_sum_inter_num assms + also have "... = (\bl \# (remove1_mset b1 \). (((int (b1 |\| bl))^2) + - (2 * (int \) * (int (b1 |\| bl))))) + (\ bl \# (remove1_mset b1 \) . ((int \)^2))" + by (simp add: sum_mset.distrib) + also have "... = (\bl \# (remove1_mset b1 \). ((int (b1 |\| bl))^2)) + - (\bl \# (remove1_mset b1 \). (2 * (int \) * (int (b1 |\| bl)))) + (\ bl \# (remove1_mset b1 \) . ((int \)^2))" + using sum_mset_add_diff_int[of "(\ bl . ((int (b1 |\| bl))^2))" "(\ bl . (2 * (int \) * (int (b1 |\| bl))))" "(remove1_mset b1 \)"] + by simp + also have "... = \^2 * (\ - 1) - 2 * (int \) *(\bl \# (remove1_mset b1 \). ((b1 |\| bl))) + + (\ - 1) * ((int \)^2)" using ssi rm1_size assms by (simp add: sum_mset_distrib_left) + also have "... = 2 * \^2 * (\ - 1) - 2 * (int \) *(\* (\ - 1))" + using sym_sum_inter_num assms by simp + also have "... = 2 * \^2 * (\ - 1) - 2 * (int \) * (\ * (\ - 1))" + using rep_value_sym symmetric_condition_2 by simp + finally have "(\bl \# (remove1_mset b1 \). (int (b1 |\| bl) - int \)^2) = 0" by (auto simp add: power2_eq_square) thus ?thesis by simp qed theorem sym_block_intersections_index [simp]: assumes "b1 \# \" assumes "b2 \# (\ - {#b1#})" shows "b1 |\| b2 = \" proof - - have pos: "\ bl . ((b1 |\| bl) - \)^2 \ 0" by simp - have "(\bl \# (remove1_mset b1 \). ((b1 |\| bl) - \)^2) = 0" - using sym_sum_inter_num_to_zero assms by simp - then have "\ bl. bl \ set_mset (remove1_mset b1 \) \ ((b1 |\| bl) - \)^2 = 0" + define l where l_def: "l = int \" + then have pos: "\ bl . (int (b1 |\| bl) - l)^2 \ 0" by simp + have "(\bl \# (remove1_mset b1 \). (int (b1 |\| bl) - l)^2) = 0" + using sym_sum_inter_num_to_zero assms l_def by simp + then have "\ bl. bl \ set_mset (remove1_mset b1 \) \ (int (b1 |\| bl) - l)^2 = 0" using sum_mset_0_iff_ge_0 pos by (metis (no_types, lifting)) - thus ?thesis - using assms(2) by auto + then have "\ bl. bl \ set_mset (remove1_mset b1 \) \ int (b1 |\| bl) = l" + by auto + thus ?thesis using assms(2) l_def of_nat_eq_iff by blast qed subsubsection \Symmetric BIBD is Simple\ lemma sym_block_mult_one [simp]: assumes "bl \# \" shows "multiplicity bl = 1" proof (rule ccontr) assume "\ (multiplicity bl = 1)" then have not: "multiplicity bl \ 1" by simp have "multiplicity bl \ 0" using assms by simp then have m: "multiplicity bl \ 2" using not by linarith then have blleft: "bl \# (\ - {#bl#})" using in_diff_count by fastforce have "bl |\| bl = \" using k_non_zero assms by (simp add: intersection_number_def) then have keql: "\ = \" using sym_block_intersections_index blleft assms by simp then have "\ = \" using keql index_lt_replication rep_value_sym block_size_lt_v diffs0_imp_equal k_non_zero zero_diff by linarith then show False using incomplete by simp qed end sublocale symmetric_bibd \ simple_design by unfold_locales simp subsubsection \Residual/Derived Sym BIBD Constructions\ text \Using the intersect result, we can reason further on residual and derived designs. Proofs based off lecture notes \cite{HerkeLectureNotes2016}\ locale symmetric_bibd_block_transformations = symmetric_bibd + bibd_block_transformations begin lemma derived_block_size [simp]: assumes "b \# \\<^sup>D" shows "card b = \" proof - obtain bl2 where set: "bl2 \# remove1_mset bl \" and inter: "b = bl2 \ bl" using derived_blocks_def assms by (meson derived_obtain_orig_block) then have "card b = bl2 |\| bl" by (simp add: intersection_number_def) thus ?thesis using sym_block_intersections_index using set intersect_num_commute valid_block by fastforce qed lemma derived_points_index [simp]: assumes "ps \ bl" assumes "card ps = 2" shows "\\<^sup>D index ps = \ - 1" proof - have b_in: "\ b . b \# (remove1_mset bl \) \ ps \ b \ ps \ b \ bl" using assms by blast then have orig: "ps \ \" using valid_block assms wellformed by blast then have lam: "size {# b \# \ . ps \ b #} = \" using balanced by (simp add: assms(2) points_index_def) then have "size {# b \# remove1_mset bl \ . ps \ b #} = size {# b \# \ . ps \ b #} - 1" using assms valid_block by (simp add: size_Diff_submset) then have "size {# b \# remove1_mset bl \ . ps \ b #} = \ - 1" using lam index_not_zero by linarith then have "size {# bl \ b | b \# (remove1_mset bl \) . ps \ bl \ b #} = \ - 1" using b_in by (metis (no_types, lifting) Int_subset_iff filter_mset_cong size_image_mset) then have "size {# x \# {# bl \ b . b \# (remove1_mset bl \) #} . ps \ x #} = \ - 1" by (metis image_mset_filter_swap) then have "size {# x \# \\<^sup>D . ps \ x #} = \ - 1" by (simp add: derived_blocks_def) thus ?thesis by (simp add: points_index_def) qed lemma sym_derive_design_bibd: assumes "\ > 1" shows "bibd bl \\<^sup>D \ (\ - 1)" proof - interpret des: proper_design bl "\\<^sup>D" using derived_is_proper assms valid_block by auto have "\ < \" using index_lt_replication rep_value_sym by linarith then show ?thesis using derived_block_size assms derived_points_index derived_points_order by (unfold_locales) (simp_all) qed lemma residual_block_size [simp]: assumes "b \# \\<^sup>R" shows "card b = \ - \" proof - obtain bl2 where sub: "b = bl2 - bl" and mem: "bl2 \# remove1_mset bl \" using assms residual_blocks_def by auto then have "card b = card bl2 - card (bl2 \ bl)" using card_Diff_subset_Int valid_block finite_blocks by (simp add: card_Diff_subset_Int) then have "card b = card bl2 - bl2 |\| bl" - using intersection_number_def finite_blocks card_inter_lt_single - by (metis assms derived_fin_incidence_system.finite_sets finite_Diff2 of_nat_diff - residual_fin_incidence_sys.finite_blocks sub) + using finite_blocks card_inter_lt_single by (simp add: intersection_number_def) thus ?thesis using sym_block_intersections_index uniform by (metis valid_block in_diffD intersect_num_commute mem) qed lemma residual_index [simp]: assumes "ps \ bl\<^sup>c" assumes "card ps = 2" shows "(\\<^sup>R) index ps = \" proof - have a: "\ b . (b \# remove1_mset bl \ \ ps \ b \ ps \ (b - bl))" using assms by (smt DiffI block_comp_elem_alt_left in_diffD subset_eq wellformed) have b: "\ b . (b \# remove1_mset bl \ \ ps \ (b - bl) \ ps \ b)" by auto have not_ss: "\ (ps \ bl)" using set_diff_non_empty_not_subset blocks_nempty t_non_zero assms block_complement_def by fastforce have "\\<^sup>R index ps = size {# x \# {# b - bl . b \# (remove1_mset bl \) #} . ps \ x #}" using assms valid_block by (simp add: points_index_def residual_blocks_def) also have "... = size {# b - bl | b \# (remove1_mset bl \) . ps \ b - bl #} " by (metis image_mset_filter_swap) finally have "\\<^sup>R index ps = size {# b \# (remove1_mset bl \) . ps \ b #} " using a b by (metis (no_types, lifting) filter_mset_cong size_image_mset) thus ?thesis using balanced not_ss assms points_index_alt_def block_complement_subset_points by auto qed lemma sym_residual_design_bibd: assumes "\ \ \ + 2" shows "bibd (bl\<^sup>c) \\<^sup>R (\ - \) \" proof - interpret des: proper_design "bl\<^sup>c" "\\<^sup>R" using residual_is_proper assms(1) valid_block sym_block_mult_one by fastforce show ?thesis using residual_block_size assms sym_design_vk_gt_kl residual_order residual_index by(unfold_locales) simp_all qed end subsection \BIBD's and Other Block Designs\ text \BIBD's are closely related to other block designs by indirect inheritance\ sublocale bibd \ k_\_PBD \ \ \ \ using block_size_gt_t by (unfold_locales) simp_all lemma incomplete_PBD_is_bibd: assumes "k < card V" and "k_\_PBD V B \ k" shows "bibd V B k \" proof - interpret inc: incomplete_design V B k using assms by (auto simp add: block_design.incomplete_designI k_\_PBD.axioms(2)) interpret pairwise_balance: pairwise_balance V B \ using assms by (auto simp add: k_\_PBD.axioms(1)) show ?thesis using assms k_\_PBD.block_size_t by (unfold_locales) (simp_all) qed lemma (in bibd) bibd_to_pbdI[intro]: assumes "\ = 1" shows "k_PBD \ \ \" proof - interpret pbd: k_\_PBD \ \ \ \ by (simp add: k_\_PBD_axioms) show ?thesis using assms by (unfold_locales) (simp_all add: t_lt_order min_block_size_2) qed locale incomplete_PBD = incomplete_design + k_\_PBD sublocale incomplete_PBD \ bibd using block_size_t by (unfold_locales) simp end \ No newline at end of file diff --git a/thys/Design_Theory/Block_Designs.thy b/thys/Design_Theory/Block_Designs.thy --- a/thys/Design_Theory/Block_Designs.thy +++ b/thys/Design_Theory/Block_Designs.thy @@ -1,558 +1,551 @@ (* Title: Block_Designs.thy Author: Chelsea Edmonds *) section \Block and Balanced Designs\ text \We define a selection of the many different types of block and balanced designs, building up to properties required for defining a BIBD, in addition to several base generalisations\ theory Block_Designs imports Design_Operations begin subsection \Block Designs\ text \A block design is a design where all blocks have the same size.\ subsubsection \K Block Designs\ text \An important generalisation of a typical block design is the $\mathcal{K}$ block design, where all blocks must have a size $x$ where $x \in \mathcal{K}$\ locale K_block_design = proper_design + - fixes sizes :: "int set" ("\") - assumes block_sizes: "bl \# \ \ (int (card bl)) \ \" + fixes sizes :: "nat set" ("\") + assumes block_sizes: "bl \# \ \ card bl \ \" assumes positive_ints: "x \ \ \ x > 0" begin lemma sys_block_size_subset: "sys_block_sizes \ \" using block_sizes sys_block_sizes_obtain_bl by blast end subsubsection\Uniform Block Design\ text \The typical uniform block design is defined below\ locale block_design = proper_design + - fixes u_block_size :: int ("\") + fixes u_block_size :: nat ("\") assumes uniform [simp]: "bl \# \ \ card bl = \" begin lemma k_non_zero: "\ \ 1" proof - obtain bl where bl_in: "bl \# \" using design_blocks_nempty by auto - then have "int (card bl) \ 1" using block_size_gt_0 - by (metis less_not_refl less_one not_le_imp_less of_nat_1 of_nat_less_iff) + then have "card bl \ 1" using block_size_gt_0 + by (metis less_not_refl less_one not_le_imp_less) thus ?thesis by (simp add: bl_in) qed lemma uniform_alt_def_all: "\ bl \# \ .card bl = \" using uniform by auto lemma uniform_unfold_point_set: "bl \# \ \ card {p \ \. p \ bl} = \" using uniform wellformed by (simp add: Collect_conj_eq inf.absorb_iff2) lemma uniform_unfold_point_set_mset: "bl \# \ \ size {#p \# mset_set \. p \ bl #} = \" using uniform_unfold_point_set by (simp add: finite_sets) lemma sys_block_sizes_uniform [simp]: "sys_block_sizes = {\}" proof - have "sys_block_sizes = {bs . \ bl . bs = card bl \ bl\# \}" by (simp add: sys_block_sizes_def) then have "sys_block_sizes = {bs . bs = \}" using uniform uniform_unfold_point_set b_positive block_set_nempty_imp_block_ex by (smt (verit, best) Collect_cong design_blocks_nempty) thus ?thesis by auto qed lemma sys_block_sizes_uniform_single: "is_singleton (sys_block_sizes)" by simp lemma uniform_size_incomp: "\ \ \ - 1 \ bl \# \ \ incomplete_block bl" - using uniform k_non_zero of_nat_less_iff zle_diff1_eq by metis + using uniform k_non_zero + by (metis block_size_lt_v diff_diff_cancel diff_is_0_eq' less_numeral_extra(1) nat_less_le) lemma uniform_complement_block_size: assumes "bl \# \\<^sup>C" shows "card bl = \ - \" proof - obtain bl' where bl_assm: "bl = bl'\<^sup>c \ bl' \# \" using wellformed assms by (auto simp add: complement_blocks_def) then have "int (card bl') = \" by simp thus ?thesis using bl_assm block_complement_size wellformed by (simp add: block_size_lt_order of_nat_diff) qed lemma uniform_complement[intro]: assumes "\ \ \ - 1" shows "block_design \ \\<^sup>C (\ - \)" proof - interpret des: proper_design \ "\\<^sup>C" using uniform_size_incomp assms complement_proper_design by auto show ?thesis using assms uniform_complement_block_size by (unfold_locales) (simp) qed lemma block_size_lt_v: "\ \ \" using v_non_zero block_size_lt_v design_blocks_nempty uniform by auto end lemma (in proper_design) block_designI[intro]: "(\ bl . bl \# \ \ card bl = k) \ block_design \ \ k" by (unfold_locales) (auto) context block_design begin lemma block_design_multiple: "n > 0 \ block_design \ (multiple_blocks n) \" using elem_in_repeat_in_original multiple_proper_design proper_design.block_designI - by (metis block_set_nempty_imp_block_ex design_blocks_nempty int_int_eq uniform_alt_def_all) + by (metis uniform_alt_def_all) end text \A uniform block design is clearly a type of $K$\_block\_design with a singleton $K$ set\ sublocale block_design \ K_block_design \ \ "{\}" using k_non_zero uniform by unfold_locales simp_all subsubsection \Incomplete Designs\ text \An incomplete design is a design where $k < v$, i.e. no block is equal to the point set\ locale incomplete_design = block_design + assumes incomplete: "\ < \" begin lemma incomplete_imp_incomp_block: "bl \# \ \ incomplete_block bl" using incomplete uniform uniform_size_incomp by fastforce lemma incomplete_imp_proper_subset: "bl \# \ \ bl \ \" - by (simp add: incomplete_block_proper_subset incomplete_imp_incomp_block wellformed) + using incomplete_block_proper_subset incomplete_imp_incomp_block by auto end lemma (in block_design) incomplete_designI[intro]: "\ < \ \ incomplete_design \ \ \" by unfold_locales auto context incomplete_design begin lemma multiple_incomplete: "n > 0 \ incomplete_design \ (multiple_blocks n) \" using block_design_multiple incomplete by (simp add: block_design.incomplete_designI) lemma complement_incomplete: "incomplete_design \ (\\<^sup>C) (\ - \)" proof - have "\ - \ < \" using v_non_zero k_non_zero by linarith thus ?thesis using uniform_complement incomplete incomplete_designI by (simp add: block_design.incomplete_designI) qed end subsection \Balanced Designs\ text \t-wise balance is a design with the property that all point subsets of size $t$ occur in $\lambda_t$ blocks\ locale t_wise_balance = proper_design + - fixes grouping :: int ("\") and index :: int ("\\<^sub>t") + fixes grouping :: nat ("\") and index :: nat ("\\<^sub>t") assumes t_non_zero: "\ \ 1" assumes t_lt_order: "\ \ \" assumes balanced [simp]: "ps \ \ \ card ps = \ \ \ index ps = \\<^sub>t" begin +lemma t_non_zero_suc: "\ \ Suc 0" + using t_non_zero by auto + lemma balanced_alt_def_all: "\ ps \ \ . card ps = \ \ \ index ps = \\<^sub>t" using balanced by auto end lemma (in proper_design) t_wise_balanceI[intro]: "\ \ \ \ \ \ 1 \ (\ ps . ps \ \ \ card ps = \ \ \ index ps = \\<^sub>t) \ t_wise_balance \ \ \ \\<^sub>t" by (unfold_locales) auto context t_wise_balance begin lemma obtain_t_subset_points: obtains T where "T \ \" "card T = \" "finite T" - using obtain_subset_with_card_int_n design_points_nempty t_lt_order t_non_zero finite_sets - by (metis int_one_le_iff_zero_less less_eq_int_code(1) linorder_not_le verit_la_generic) + using obtain_subset_with_card_n design_points_nempty t_lt_order t_non_zero finite_sets by auto lemma multiple_t_wise_balance_index [simp]: assumes "ps \ \" assumes "card ps = \" shows "(multiple_blocks n) index ps = \\<^sub>t * n" using multiple_point_index balanced assms by fastforce lemma multiple_t_wise_balance: assumes "n > 0" shows "t_wise_balance \ (multiple_blocks n) \ (\\<^sub>t * n)" proof - interpret des: proper_design \ "(multiple_blocks n)" by (simp add: assms multiple_proper_design) show ?thesis using t_non_zero t_lt_order multiple_t_wise_balance_index by (unfold_locales) (simp_all) qed lemma twise_set_pair_index: "ps \ \ \ ps2 \ \ \ ps \ ps2 \ card ps = \ \ card ps2 = \ \ \ index ps = \ index ps2" - using balanced by (metis of_nat_eq_iff) + using balanced by simp lemma t_wise_balance_alt: "ps \ \ \ card ps = \ \ \ index ps = l2 \ (\ ps . ps \ \ \ card ps = \ \ \ index ps = l2)" using twise_set_pair_index by blast -lemma index_ge_zero: "\\<^sub>t \ 0" -proof - - obtain ps where "ps \ \ \ card ps = \" using t_non_zero t_lt_order obtain_subset_with_card_n - by (metis dual_order.trans of_nat_le_iff zero_le_imp_eq_int zero_le_one) - thus ?thesis - using balanced_alt_def_all of_nat_0_le_iff by blast -qed - lemma index_1_imp_mult_1 [simp]: assumes "\\<^sub>t = 1" assumes "bl \# \" assumes "card bl \ \" shows "multiplicity bl = 1" proof (rule ccontr) assume "\ (multiplicity bl = 1)" then have not: "multiplicity bl \ 1" by simp have "multiplicity bl \ 0" using assms by simp then have m: "multiplicity bl \ 2" using not by linarith obtain ps where ps: "ps \ bl \ card ps = \" using assms obtain_t_subset_points - by (metis obtain_subset_with_card_int_n of_nat_0_le_iff) + by (metis obtain_subset_with_card_n) then have "\ index ps \ 2" using m points_index_count_min ps by blast then show False using balanced ps antisym_conv2 not_numeral_less_zero numeral_le_one_iff points_index_ps_nin semiring_norm(69) zero_neq_numeral - by (metis assms(1) int_int_eq int_ops(2)) + by (metis assms(1)) qed end subsubsection \Sub-types of t-wise balance\ text \Pairwise balance is when $t = 2$. These are commonly of interest\ locale pairwise_balance = t_wise_balance \ \ 2 \ for point_set ("\") and block_collection ("\") and index ("\") text \We can combine the balance properties with $K$\_block design to define tBD's (t-wise balanced designs), and PBD's (pairwise balanced designs)\ locale tBD = t_wise_balance + K_block_design + assumes block_size_gt_t: "k \ \ \ k \ \" locale \_PBD = pairwise_balance + K_block_design + assumes block_size_gt_t: "k \ \ \ k \ 2" sublocale \_PBD \ tBD \ \ 2 \ \ using t_lt_order block_size_gt_t by (unfold_locales) (simp_all) locale PBD = \_PBD \ \ 1 \ for point_set ("\") and block_collection ("\") and sizes ("\") begin lemma multiplicity_is_1: assumes "bl \# \" shows "multiplicity bl = 1" using block_size_gt_t index_1_imp_mult_1 by (simp add: assms block_sizes) end sublocale PBD \ simple_design using multiplicity_is_1 by (unfold_locales) text \PBD's are often only used in the case where $k$ is uniform, defined here.\ locale k_\_PBD = pairwise_balance + block_design + assumes block_size_t: "2 \ \" sublocale k_\_PBD \ \_PBD \ \ \ "{\}" using k_non_zero uniform block_size_t by(unfold_locales) (simp_all) locale k_PBD = k_\_PBD \ \ 1 \ for point_set ("\") and block_collection ("\") and u_block_size ("\") sublocale k_PBD \ PBD \ \ "{\}" using block_size_t by (unfold_locales, simp_all) subsubsection \Covering and Packing Designs\ text \Covering and packing designs involve a looser balance restriction. Upper/lower bounds are placed on the points index, instead of a strict equality\ text \A t-covering design is a relaxed version of a tBD, where, for all point subsets of size t, a lower bound is put on the points index\ locale t_covering_design = block_design + - fixes grouping :: int ("\") - fixes min_index :: int ("\\<^sub>t") + fixes grouping :: nat ("\") + fixes min_index :: nat ("\\<^sub>t") assumes covering: "ps \ \ \ card ps = \ \ \ index ps \ \\<^sub>t" assumes block_size_t: "\ \ \" assumes t_non_zero: "\ \ 1" begin lemma covering_alt_def_all: "\ ps \ \ . card ps = \ \ \ index ps \ \\<^sub>t" using covering by auto end lemma (in block_design) t_covering_designI [intro]: "t \ \ \ t \ 1 \ (\ ps. ps \ \ \ card ps = t \ \ index ps \ \\<^sub>t) \ t_covering_design \ \ \ t \\<^sub>t" by (unfold_locales) simp_all text \A t-packing design is a relaxed version of a tBD, where, for all point subsets of size t, an upper bound is put on the points index\ locale t_packing_design = block_design + - fixes grouping :: int ("\") - fixes min_index :: int ("\\<^sub>t") + fixes grouping :: nat ("\") + fixes min_index :: nat ("\\<^sub>t") assumes packing: "ps \ \ \ card ps = \ \ \ index ps \ \\<^sub>t" assumes block_size_t: "\ \ \" assumes t_non_zero: "\ \ 1" begin lemma packing_alt_def_all: "\ ps \ \ . card ps = \ \ \ index ps \ \\<^sub>t" using packing by auto end lemma (in block_design) t_packing_designI [intro]: "t \ \ \ t \ 1 \ (\ ps . ps \ \ \ card ps = t \ \ index ps \ \\<^sub>t) \ t_packing_design \ \ \ t \\<^sub>t" by (unfold_locales) simp_all lemma packing_covering_imp_balance: assumes "t_packing_design V B k t \\<^sub>t" assumes "t_covering_design V B k t \\<^sub>t" shows "t_wise_balance V B t \\<^sub>t" proof - from assms interpret des: proper_design V B using block_design.axioms(1) t_covering_design.axioms(1) by blast show ?thesis proof (unfold_locales) - show "1 \ t" using assms by (simp add: t_packing_design.t_non_zero) + show "1 \ t" using assms t_packing_design.t_non_zero by auto show "t \ des.\" using block_design.block_size_lt_v t_packing_design.axioms(1) by (metis assms(1) dual_order.trans t_packing_design.block_size_t) show "\ps. ps \ V \ card ps = t \ B index ps = \\<^sub>t" using t_packing_design.packing t_covering_design.covering by (metis assms dual_order.antisym) qed qed subsection \Constant Replication Design\ text \When the replication number for all points in a design is constant, it is the design replication number.\ locale constant_rep_design = proper_design + - fixes design_rep_number :: int ("\") + fixes design_rep_number :: nat ("\") assumes rep_number [simp]: "x \ \ \ \ rep x = \" begin lemma rep_number_alt_def_all: "\ x \ \. \ rep x = \" by (simp) lemma rep_number_unfold_set: "x \ \ \ size {#bl \# \ . x \ bl#} = \" using rep_number by (simp add: point_replication_number_def) lemma rep_numbers_constant [simp]: "replication_numbers = {\}" unfolding replication_numbers_def using rep_number design_points_nempty Collect_cong finite.cases finite_sets insertCI singleton_conv by (smt (verit, ccfv_threshold) fst_conv snd_conv) lemma replication_number_single: "is_singleton (replication_numbers)" using is_singleton_the_elem by simp lemma constant_rep_point_pair: "x1 \ \ \ x2 \ \ \ x1 \ x2 \ \ rep x1 = \ rep x2" using rep_number by auto lemma constant_rep_alt: "x1 \ \ \ \ rep x1 = r2 \ (\ x . x \ \ \ \ rep x = r2)" by (simp) lemma constant_rep_point_not_0: assumes "x \ \" shows "\ rep x \ 0" proof (rule ccontr) assume "\ \ rep x \ 0" then have "\ x . x \ \ \ \ rep x = 0" using rep_number assms by auto then have "\ x . x \ \ \ size {#bl \# \ . x \ bl#} = 0" by (simp add: point_replication_number_def) then show False using design_blocks_nempty wf_design wf_design_iff wf_invalid_point by (metis ex_in_conv filter_mset_empty_conv multiset_nonemptyE size_eq_0_iff_empty) qed lemma rep_not_zero: "\ \ 0" using rep_number constant_rep_point_not_0 design_points_nempty by auto lemma r_gzero: "\ > 0" - using point_replication_number_def rep_number constant_rep_design.rep_not_zero - by (metis constant_rep_design.intro constant_rep_design_axioms.intro leI of_nat_less_0_iff - proper_design_axioms verit_la_disequality) + using rep_not_zero by auto lemma r_lt_eq_b: "\ \ \" using rep_number max_point_rep by (metis all_not_in_conv design_points_nempty) lemma complement_rep_number: assumes "\ bl . bl \# \ \ incomplete_block bl" shows "constant_rep_design \ \\<^sup>C (\ - \)" proof - interpret d: proper_design \ "(\\<^sup>C)" using complement_proper_design by (simp add: assms) show ?thesis using complement_rep_number rep_number by (unfold_locales) simp qed lemma multiple_rep_number: assumes "n > 0" shows "constant_rep_design \ (multiple_blocks n) (\ * n)" proof - interpret d: proper_design \ "(multiple_blocks n)" using multiple_proper_design by (simp add: assms) show ?thesis using multiple_point_rep_num by (unfold_locales) (simp_all) qed end lemma (in proper_design) constant_rep_designI [intro]: "(\ x . x \ \ \ \ rep x = \) \ constant_rep_design \ \ \" by unfold_locales auto subsection \T-designs\ text \All the before mentioned designs build up to the concept of a t-design, which has uniform block size and is t-wise balanced. We limit $t$ to be less than $k$, so the balance condition has relevance\ locale t_design = incomplete_design + t_wise_balance + assumes block_size_t: "\ \ \" begin lemma point_indices_balanced: "point_indices \ = {\\<^sub>t}" proof - - have "point_indices \ = {i . \ ps . i = \ index ps \ int (card ps) = \ \ ps \ \}" + have "point_indices \ = {i . \ ps . i = \ index ps \ card ps = \ \ ps \ \}" by (simp add: point_indices_def) then have "point_indices \ = {i . i = \\<^sub>t}" using balanced Collect_cong obtain_t_subset_points - by smt + by (smt (verit, best)) thus ?thesis by auto qed lemma point_indices_singleton: "is_singleton (point_indices \)" using point_indices_balanced is_singleton_the_elem by simp end lemma t_designI [intro]: assumes "incomplete_design V B k" assumes "t_wise_balance V B t \\<^sub>t" assumes "t \ k" shows "t_design V B k t \\<^sub>t" by (simp add: assms(1) assms(2) assms(3) t_design.intro t_design_axioms.intro) sublocale t_design \ t_covering_design \ \ \ \ \\<^sub>t using t_non_zero by (unfold_locales) (auto simp add: block_size_t) sublocale t_design \ t_packing_design \ \ \ \ \\<^sub>t using t_non_zero by (unfold_locales) (auto simp add: block_size_t) lemma t_design_pack_cov [intro]: assumes "k < card V" assumes "t_covering_design V B k t \\<^sub>t" assumes "t_packing_design V B k t \\<^sub>t" shows "t_design V B k t \\<^sub>t" proof - from assms interpret id: incomplete_design V B k using block_design.incomplete_designI t_packing_design.axioms(1) - by (metis of_nat_less_iff) + by blast from assms interpret balance: t_wise_balance V B t \\<^sub>t using packing_covering_imp_balance by blast show ?thesis using assms(3) by (unfold_locales) (simp_all add: t_packing_design.block_size_t) qed sublocale t_design \ tBD \ \ \ \\<^sub>t "{\}" using uniform k_non_zero block_size_t by (unfold_locales) simp_all context t_design begin lemma multiple_t_design: "n > 0 \ t_design \ (multiple_blocks n) \ \ (\\<^sub>t * n)" using multiple_t_wise_balance multiple_incomplete block_size_t by (simp add: t_designI) lemma t_design_min_v: "\ > 1" using k_non_zero incomplete by simp end subsection \Steiner Systems\ text \Steiner systems are a special type of t-design where $\Lambda_t = 1$\ locale steiner_system = t_design \ \ \ \ 1 for point_set ("\") and block_collection ("\") and u_block_size ("\") and grouping ("\") begin lemma block_multiplicity [simp]: assumes "bl \# \" shows "multiplicity bl = 1" by (simp add: assms block_size_t) end sublocale steiner_system \ simple_design by unfold_locales (simp) lemma (in t_design) steiner_systemI[intro]: "\\<^sub>t = 1 \ steiner_system \ \ \ \" using t_non_zero t_lt_order block_size_t by unfold_locales auto subsection \Combining block designs\ text \We define some closure properties for various block designs under the combine operator. This is done using locales to reason on multiple instances of the same type of design, building on what was presented in the design operations theory\ locale two_t_wise_eq_points = two_designs_proper \ \ \ \' + des1: t_wise_balance \ \ \ \\<^sub>t + des2: t_wise_balance \ \' \ \\<^sub>t' for \ \ \ \\<^sub>t \' \\<^sub>t' begin lemma combine_t_wise_balance_index: "ps \ \ \ card ps = \ \ \\<^sup>+ index ps = (\\<^sub>t + \\<^sub>t')" using des1.balanced des2.balanced by (simp add: combine_points_index) lemma combine_t_wise_balance: "t_wise_balance \\<^sup>+ \\<^sup>+ \ (\\<^sub>t + \\<^sub>t')" -proof (unfold_locales, simp add: des1.t_non_zero) +proof (unfold_locales, simp add: des1.t_non_zero_suc) have "card \\<^sup>+ \ card \" by simp then show "\ \ card (\\<^sup>+)" using des1.t_lt_order by linarith show "\ps. ps \ \\<^sup>+ \ card ps = \ \ (\\<^sup>+ index ps) = \\<^sub>t + \\<^sub>t'" using combine_t_wise_balance_index by blast qed sublocale combine_t_wise_des: t_wise_balance "\\<^sup>+" "\\<^sup>+" "\" "(\\<^sub>t + \\<^sub>t')" using combine_t_wise_balance by auto end locale two_k_block_designs = two_designs_proper \ \ \' \' + des1: block_design \ \ \ + des2: block_design \' \' \ for \ \ \ \' \' begin lemma block_design_combine: "block_design \\<^sup>+ \\<^sup>+ \" using des1.uniform des2.uniform by (unfold_locales) (auto) sublocale combine_block_des: block_design "\\<^sup>+" "\\<^sup>+" "\" using block_design_combine by simp end locale two_rep_designs_eq_points = two_designs_proper \ \ \ \' + des1: constant_rep_design \ \ \ + des2: constant_rep_design \ \' \' for \ \ \ \' \' begin lemma combine_rep_number: "constant_rep_design \\<^sup>+ \\<^sup>+ (\ + \')" using combine_rep_number des1.rep_number des2.rep_number by (unfold_locales) (simp) sublocale combine_const_rep: constant_rep_design "\\<^sup>+" "\\<^sup>+" "(\ + \')" using combine_rep_number by simp end locale two_incomplete_designs = two_k_block_designs \ \ \ \' \' + des1: incomplete_design \ \ \ + des2: incomplete_design \' \' \ for \ \ \ \' \' begin lemma combine_is_incomplete: "incomplete_design \\<^sup>+ \\<^sup>+ \" using combine_order des1.incomplete des2.incomplete by (unfold_locales) (simp) sublocale combine_incomplete: incomplete_design "\\<^sup>+" "\\<^sup>+" "\" using combine_is_incomplete by simp end locale two_t_designs_eq_points = two_incomplete_designs \ \ \ \ \' + two_t_wise_eq_points \ \ \ \\<^sub>t \' \\<^sub>t' + des1: t_design \ \ \ \ \\<^sub>t + des2: t_design \ \' \ \ \\<^sub>t' for \ \ \ \' \ \\<^sub>t \\<^sub>t' begin lemma combine_is_t_des: "t_design \\<^sup>+ \\<^sup>+ \ \ (\\<^sub>t + \\<^sub>t')" using des1.block_size_t des2.block_size_t by (unfold_locales) sublocale combine_t_des: t_design "\\<^sup>+" "\\<^sup>+" "\" "\" "(\\<^sub>t + \\<^sub>t')" using combine_is_t_des by blast end end \ No newline at end of file diff --git a/thys/Design_Theory/Design_Basics.thy b/thys/Design_Theory/Design_Basics.thy --- a/thys/Design_Theory/Design_Basics.thy +++ b/thys/Design_Theory/Design_Basics.thy @@ -1,824 +1,824 @@ theory Design_Basics imports Main Multisets_Extras "HOL-Library.Disjoint_Sets" begin section \Design Theory Basics\ text \All definitions in this section reference the handbook of combinatorial designs \cite{colbournHandbookCombinatorialDesigns2007}\ subsection \Initial setup\ text \Enable coercion of nats to ints to aid with reasoning on design properties\ declare [[coercion_enabled]] declare [[coercion "of_nat :: nat \ int"]] subsection \Incidence System\ text \An incidence system is defined to be a wellformed set system. i.e. each block is a subset of the base point set. Alternatively, an incidence system can be looked at as the point set and an incidence relation which indicates if they are in the same block\ locale incidence_system = fixes point_set :: "'a set" ("\") fixes block_collection :: "'a set multiset" ("\") assumes wellformed: "b \# \ \ b \ \" begin definition "\ \ { (x, b) . b \# \ \ x \ b}" (* incidence relation *) definition incident :: "'a \ 'a set \ bool" where "incident p b \ (p, b) \ \" text \Defines common notation used to indicate number of points ($v$) and number of blocks ($b$)\ -abbreviation "\ \ int (card \)" +abbreviation "\ \ card \" -abbreviation "\ \ int (size \)" +abbreviation "\ \ size \" text \Basic incidence lemmas\ lemma incidence_alt_def: assumes "p \ \" assumes "b \# \" shows "incident p b \ p \ b" by (auto simp add: incident_def \_def assms) lemma wf_invalid_point: "x \ \ \ b \# \ \ x \ b" using wellformed by auto lemma block_set_nempty_imp_block_ex: "\ \ {#} \ \ bl . bl \# \" by auto text \Abbreviations for all incidence systems\ abbreviation multiplicity :: "'a set \ nat" where "multiplicity b \ count \ b" abbreviation incomplete_block :: "'a set \ bool" where "incomplete_block bl \ card bl < card \ \ bl \# \" lemma incomplete_alt_size: "incomplete_block bl \ card bl < \" by simp lemma incomplete_alt_in: "incomplete_block bl \ bl \# \" by simp lemma incomplete_alt_imp[intro]: "card bl < \ \ bl \# \ \ incomplete_block bl" by simp definition design_support :: "'a set set" where "design_support \ set_mset \" end subsection \Finite Incidence Systems\ text \These simply require the point set to be finite. As multisets are only defined to be finite, it is implied that the block set must be finite already\ locale finite_incidence_system = incidence_system + assumes finite_sets: "finite \" begin lemma finite_blocks: "b \# \ \ finite b" using wellformed finite_sets finite_subset by blast lemma mset_points_distinct: "distinct_mset (mset_set \)" using finite_sets by (simp add: distinct_mset_def) lemma mset_points_distinct_diff_one: "distinct_mset (mset_set (\ - {x}))" by (meson count_mset_set_le_one distinct_mset_count_less_1) lemma finite_design_support: "finite (design_support)" using design_support_def by auto lemma block_size_lt_order: "bl \# \ \ card bl \ card \" using wellformed by (simp add: card_mono finite_sets) end subsection \Designs\ text \There are many varied definitions of a design in literature. However, the most commonly accepted definition is a finite point set, $V$ and collection of blocks $B$, where no block in $B$ can be empty\ locale design = finite_incidence_system + assumes blocks_nempty: "bl \# \ \ bl \ {}" begin lemma wf_design: "design \ \" by intro_locales lemma wf_design_iff: "bl \# \ \ design \ \ \ (bl \ \ \ finite \ \ bl \ {})" using blocks_nempty wellformed finite_sets by (simp add: wf_design) text \Reasoning on non empty properties and non zero parameters\ lemma blocks_nempty_alt: "\ bl \# \. bl \ {}" using blocks_nempty by auto lemma block_set_nempty_imp_points: "\ \ {#} \ \ \ {}" using wf_design wf_design_iff by auto lemma b_non_zero_imp_v_non_zero: "\ > 0 \ \ > 0" using block_set_nempty_imp_points finite_sets by fastforce lemma v_eq0_imp_b_eq_0: "\ = 0 \ \ = 0" using b_non_zero_imp_v_non_zero by auto text \Size lemmas\ lemma block_size_lt_v: "bl \# \ \ card bl \ \" by (simp add: card_mono finite_sets wellformed) lemma block_size_gt_0: "bl \# \ \ card bl > 0" using finite_sets blocks_nempty finite_blocks by fastforce lemma design_cart_product_size: "size ((mset_set \) \# \) = \ * \" by (simp add: size_cartesian_product) end text \Intro rules for design locale\ lemma wf_design_implies: assumes "(\ b . b \# \ \ b \ V)" assumes "\ b . b \# \ \ b \ {}" assumes "finite V" assumes "\ \ {#}" assumes "V \ {}" shows "design V \" using assms by (unfold_locales) simp_all lemma (in incidence_system) finite_sysI[intro]: "finite \ \ finite_incidence_system \ \" by (unfold_locales) simp_all lemma (in finite_incidence_system) designI[intro]: "(\ b. b \# \ \ b \ {}) \ \ \ {#} \ \ \ {} \ design \ \" by (unfold_locales) simp_all subsection \Core Property Definitions\ subsubsection \Replication Number\ text \The replication number for a point is the number of blocks that point is incident with\ -definition point_replication_number :: "'a set multiset \ 'a \ int" (infix "rep" 75) where +definition point_replication_number :: "'a set multiset \ 'a \ nat" (infix "rep" 75) where "B rep x \ size {#b \# B . x \ b#}" lemma max_point_rep: "B rep x \ size B" using size_filter_mset_lesseq by (simp add: point_replication_number_def) lemma rep_number_g0_exists: assumes "B rep x > 0" obtains b where "b \# B" and "x \ b" proof - have "size {#b \# B . x \ b#} > 0" using assms point_replication_number_def - by (metis of_nat_0_less_iff) + by metis thus ?thesis by (metis filter_mset_empty_conv nonempty_has_size that) qed lemma rep_number_on_set_def: "finite B \ (mset_set B) rep x = card {b \ B . x \ b}" by (simp add: point_replication_number_def) lemma point_rep_number_split[simp]: "(A + B) rep x = A rep x + B rep x" by (simp add: point_replication_number_def) lemma point_rep_singleton_val [simp]: "x \ b \ {#b#} rep x = 1" by (simp add: point_replication_number_def) lemma point_rep_singleton_inval [simp]: "x \ b \ {#b#} rep x = 0" by (simp add: point_replication_number_def) context incidence_system begin lemma point_rep_number_alt_def: "\ rep x = size {# b \# \ . x \ b#}" by (simp add: point_replication_number_def) lemma rep_number_non_zero_system_point: " \ rep x > 0 \ x \ \" using rep_number_g0_exists wellformed by (metis wf_invalid_point) lemma point_rep_non_existance [simp]: "x \ \ \ \ rep x = 0" using wf_invalid_point by (simp add: point_replication_number_def filter_mset_empty_conv) lemma point_rep_number_inv: "size {# b \# \ . x \ b #} = \ - (\ rep x)" proof - have "\ = size {# b \# \ . x \ b #} + size {# b \# \ . x \ b #}" using multiset_partition by (metis add.commute size_union) thus ?thesis by (simp add: point_replication_number_def) qed lemma point_rep_num_inv_non_empty: "(\ rep x) < \ \ \ \ {#} \ {# b \# \ . x \ b #} \ {#}" by (metis diff_zero point_replication_number_def size_empty size_filter_neg verit_comp_simplify1(1)) end subsubsection \Point Index\ text \The point index of a subset of points in a design, is the number of times those points occur together in a block of the design\ definition points_index :: "'a set multiset \ 'a set \ nat" (infix "index" 75) where "B index ps \ size {#b \# B . ps \ b#}" lemma points_index_empty [simp]: "{#} index ps = 0" by (simp add: points_index_def) lemma point_index_distrib: "(B1 + B2) index ps = B1 index ps + B2 index ps" by (simp add: points_index_def) lemma point_index_diff: "B1 index ps = (B1 + B2) index ps - B2 index ps" by (simp add: points_index_def) lemma points_index_singleton: "{#b#} index ps = 1 \ ps \ b" by (simp add: points_index_def) lemma points_index_singleton_zero: "\ (ps \ b) \ {#b#} index ps = 0" by (simp add: points_index_def) lemma points_index_sum: "(\\<^sub># B ) index ps = (\b \# B . (b index ps))" using points_index_empty by (induction B) (auto simp add: point_index_distrib) lemma points_index_block_image_add_eq: assumes "x \ ps" assumes "B index ps = l" shows "{# insert x b . b \# B#} index ps = l" using points_index_def by (metis (no_types, lifting) assms filter_mset_cong image_mset_filter_swap2 points_index_def size_image_mset subset_insert) lemma points_index_on_set_def [simp]: assumes "finite B" shows "(mset_set B) index ps = card {b \ B. ps \ b}" by (simp add: points_index_def assms) lemma points_index_single_rep_num: "B index {x} = B rep x" by (simp add: points_index_def point_replication_number_def) lemma points_index_pair_rep_num: assumes "\ b. b \# B \ x \ b" shows "B index {x, y} = B rep y" using point_replication_number_def points_index_def by (metis assms empty_subsetI filter_mset_cong insert_subset) lemma points_index_0_left_imp: assumes "B index ps = 0" assumes "b \# B" shows "\ (ps \ b)" proof (rule ccontr) assume "\ \ ps \ b" then have a: "ps \ b" by auto then have "b \# {#bl \# B . ps \ bl#}" by (simp add: assms(2)) thus False by (metis assms(1) count_greater_eq_Suc_zero_iff count_size_set_repr not_less_eq_eq points_index_def size_filter_mset_lesseq) qed lemma points_index_0_right_imp: assumes "\ b . b \# B \ (\ ps \ b)" shows "B index ps = 0" using assms by (simp add: filter_mset_empty_conv points_index_def) lemma points_index_0_iff: "B index ps = 0 \ (\ b. b \# B \ (\ ps \ b))" using points_index_0_left_imp points_index_0_right_imp by metis lemma points_index_gt0_impl_existance: assumes "B index ps > 0" shows "(\ bl . (bl \# B \ ps \ bl))" proof - have "size {#bl \# B . ps \ bl#} > 0" by (metis assms points_index_def) then obtain bl where "bl \# B" and "ps \ bl" by (metis filter_mset_empty_conv nonempty_has_size) thus ?thesis by auto qed lemma points_index_one_unique: assumes "B index ps = 1" assumes "bl \# B" and "ps \ bl" and "bl' \# B" and "ps \ bl'" shows "bl = bl'" proof (rule ccontr) assume assm: "bl \ bl'" then have bl1: "bl \# {#bl \# B . ps \ bl#}" using assms by simp then have bl2: "bl'\# {#bl \# B . ps \ bl#}" using assms by simp then have "{#bl, bl'#} \# {#bl \# B . ps \ bl#}" using assms by (metis bl1 bl2 points_index_def add_mset_subseteq_single_iff assm mset_subset_eq_single size_single subseteq_mset_size_eql) then have "size {#bl \# B . ps \ bl#} \ 2" using size_mset_mono by fastforce thus False using assms by (metis numeral_le_one_iff points_index_def semiring_norm(69)) qed lemma points_index_one_unique_block: assumes "B index ps = 1" shows "\! bl . (bl \# B \ ps \ bl)" using assms points_index_gt0_impl_existance points_index_one_unique by (metis zero_less_one) lemma points_index_one_not_unique_block: assumes "B index ps = 1" assumes "ps \ bl" assumes "bl \# B" assumes "bl' \# B - {#bl#}" shows "\ ps \ bl'" proof - have "B = (B - {#bl#}) + {#bl#}" by (simp add: assms(3)) then have "(B - {#bl#}) index ps = B index ps - {#bl#} index ps" by (metis point_index_diff) then have "(B - {#bl#}) index ps = 0" using assms points_index_singleton by (metis diff_self_eq_0) thus ?thesis using assms(4) points_index_0_left_imp by auto qed lemma (in incidence_system) points_index_alt_def: "\ index ps = size {#b \# \ . ps \ b#}" by (simp add: points_index_def) lemma (in incidence_system) points_index_ps_nin: "\ (ps \ \) \ \ index ps = 0" using points_index_alt_def filter_mset_empty_conv in_mono size_empty subsetI wf_invalid_point by metis lemma (in incidence_system) points_index_count_bl: "multiplicity bl \ n \ ps \ bl \ count {#bl \# \ . ps \ bl#} bl \ n" by simp lemma (in finite_incidence_system) points_index_zero: assumes "card ps > card \" shows "\ index ps = 0" proof - have "\ b. b \# \ \ card ps > card b" using block_size_lt_order card_subset_not_gt_card finite_sets assms by fastforce then have "{#b \# \ . ps \ b#} = {#}" by (simp add: card_subset_not_gt_card filter_mset_empty_conv finite_blocks) thus ?thesis using points_index_alt_def by simp qed lemma (in design) points_index_subset: "x \# {#bl \# \ . ps \ bl#} \ ps \ \ \ (\ index ps) \ (size x)" by (simp add: points_index_def size_mset_mono) lemma (in design) points_index_count_min: "multiplicity bl \ n \ ps \ bl \ \ index ps \ n" using points_index_alt_def set_count_size_min by (metis filter_mset.rep_eq) subsubsection \Intersection Number\ text \The intersection number of two blocks is the size of the intersection of those blocks. i.e. the number of points which occur in both blocks\ -definition intersection_number :: "'a set \ 'a set \ int" (infix "|\|" 70) where +definition intersection_number :: "'a set \ 'a set \ nat" (infix "|\|" 70) where "b1 |\| b2 \ card (b1 \ b2)" lemma intersection_num_non_neg: "b1 |\| b2 \ 0" by (simp add: intersection_number_def) lemma intersection_number_empty_iff: assumes "finite b1" shows "b1 \ b2 = {} \ b1 |\| b2 = 0" by (simp add: intersection_number_def assms) lemma intersect_num_commute: "b1 |\| b2 = b2 |\| b1" by (simp add: inf_commute intersection_number_def) -definition n_intersect_number :: "'a set \ nat\ 'a set \ int" where +definition n_intersect_number :: "'a set \ nat\ 'a set \ nat" where "n_intersect_number b1 n b2 \ card { x \ Pow (b1 \ b2) . card x = n}" notation n_intersect_number ("(_ |\|\<^sub>_ _)" [52, 51, 52] 50) lemma n_intersect_num_subset_def: "b1 |\|\<^sub>n b2 = card {x . x \ b1 \ b2 \ card x = n}" using n_intersect_number_def by auto lemma n_inter_num_one: "finite b1 \ finite b2 \ b1 |\|\<^sub>1 b2 = b1 |\| b2" using n_intersect_number_def intersection_number_def card_Pow_filter_one by (metis (full_types) finite_Int) lemma n_inter_num_choose: "finite b1 \ finite b2 \ b1 |\|\<^sub>n b2 = (card (b1 \ b2) choose n)" using n_subsets n_intersect_num_subset_def by (metis (full_types) finite_Int) lemma set_filter_single: "x \ A \ {a \ A . a = x} = {x}" by auto lemma (in design) n_inter_num_zero: assumes "b1 \# \" and "b2 \# \" shows "b1 |\|\<^sub>0 b2 = 1" proof - have empty: "\x . finite x \ card x = 0 \ x = {}" by simp have empt_in: "{} \ Pow (b1 \ b2)" by simp have "finite (b1 \ b2)" using finite_blocks assms by simp then have "\ x . x \ Pow (b1 \ b2) \ finite x" by (meson PowD finite_subset) then have "{x \ Pow (b1 \ b2) . card x = 0} = {x \ Pow (b1 \ b2) . x = {}}" using empty by (metis card.empty) then have "{x \ Pow (b1 \ b2) . card x = 0} = {{}}" by (simp add: empt_in set_filter_single Collect_conv_if) thus ?thesis by (simp add: n_intersect_number_def) qed lemma (in design) n_inter_num_choose_design: "b1 \# \ \ b2 \# \ \ b1 |\|\<^sub>n b2 = (card (b1 \ b2) choose n) " using finite_blocks by (simp add: n_inter_num_choose) lemma (in design) n_inter_num_choose_design_inter: "b1 \# \ \ b2 \# \ \ b1 |\|\<^sub>n b2 = (nat (b1 |\| b2) choose n) " using finite_blocks by (simp add: n_inter_num_choose intersection_number_def) subsection \Incidence System Set Property Definitions\ context incidence_system begin text \The set of replication numbers for all points of design\ -definition replication_numbers :: "int set" where +definition replication_numbers :: "nat set" where "replication_numbers \ {\ rep x | x . x \ \}" lemma replication_numbers_non_empty: assumes "\ \ {}" shows "replication_numbers \ {}" by (simp add: assms replication_numbers_def) lemma obtain_point_with_rep: "r \ replication_numbers \ \ x. x \ \ \ \ rep x = r" using replication_numbers_def by auto lemma point_rep_number_in_set: "x \ \ \ (\ rep x) \ replication_numbers" by (auto simp add: replication_numbers_def) lemma (in finite_incidence_system) replication_numbers_finite: "finite replication_numbers" using finite_sets by (simp add: replication_numbers_def) text \The set of all block sizes in a system\ -definition sys_block_sizes :: "int set" where -"sys_block_sizes \ { (int (card bl)) | bl. bl \# \}" +definition sys_block_sizes :: "nat set" where +"sys_block_sizes \ { card bl | bl. bl \# \}" lemma block_sizes_non_empty_set: assumes "\ \ {#}" shows "sys_block_sizes \ {}" by (simp add: sys_block_sizes_def assms) lemma finite_block_sizes: "finite (sys_block_sizes)" by (simp add: sys_block_sizes_def) lemma block_sizes_non_empty: assumes "\ \ {#}" shows "card (sys_block_sizes) > 0" using finite_block_sizes block_sizes_non_empty_set by (simp add: assms card_gt_0_iff) lemma sys_block_sizes_in: "bl \# \ \ card bl \ sys_block_sizes" unfolding sys_block_sizes_def by auto -lemma sys_block_sizes_obtain_bl: "x \ sys_block_sizes \ (\ bl \# \. int (card bl) = x)" +lemma sys_block_sizes_obtain_bl: "x \ sys_block_sizes \ (\ bl \# \. card bl = x)" by (auto simp add: sys_block_sizes_def) text \The set of all possible intersection numbers in a system.\ -definition intersection_numbers :: "int set" where +definition intersection_numbers :: "nat set" where "intersection_numbers \ { b1 |\| b2 | b1 b2 . b1 \# \ \ b2 \# (\ - {#b1#})}" lemma obtain_blocks_intersect_num: "n \ intersection_numbers \ \ b1 b2. b1 \# \ \ b2 \# (\ - {#b1#}) \ b1 |\| b2 = n" by (auto simp add: intersection_numbers_def) lemma intersect_num_in_set: "b1 \# \ \ b2 \# (\ - {#b1#}) \ b1 |\| b2 \ intersection_numbers" by (auto simp add: intersection_numbers_def) text \The set of all possible point indices\ -definition point_indices :: "int \ int set" where -"point_indices t \ {\ index ps | ps. int (card ps) = t \ ps \ \}" +definition point_indices :: "nat \ nat set" where +"point_indices t \ {\ index ps | ps. card ps = t \ ps \ \}" lemma point_indices_elem_in: "ps \ \ \ card ps = t \ \ index ps \ point_indices t" by (auto simp add: point_indices_def) -lemma point_indices_alt_def: "point_indices t = { \ index ps | ps. int (card ps) = t \ ps \ \}" +lemma point_indices_alt_def: "point_indices t = { \ index ps | ps. card ps = t \ ps \ \}" by (simp add: point_indices_def) end subsection \Basic Constructions on designs\ text \This section defines some of the most common universal constructions found in design theory involving only a single design\ subsubsection \Design Complements\ context incidence_system begin text \The complement of a block are all the points in the design not in that block. The complement of a design is therefore the original point sets, and set of all block complements\ definition block_complement:: "'a set \ 'a set" ("_\<^sup>c" [56] 55) where "block_complement b \ \ - b" definition complement_blocks :: "'a set multiset" ("(\\<^sup>C)")where "complement_blocks \ {# bl\<^sup>c . bl \# \ #}" lemma block_complement_elem_iff: assumes "ps \ \" shows "ps \ bl\<^sup>c \ (\ x \ ps. x \ bl)" using assms block_complement_def by (auto) lemma block_complement_inter_empty: "bl1\<^sup>c = bl2 \ bl1 \ bl2 = {}" using block_complement_def by auto lemma block_complement_inv: assumes "bl \# \" assumes "bl\<^sup>c = bl2" shows "bl2\<^sup>c = bl" by (metis Diff_Diff_Int assms(1) assms(2) block_complement_def inf.absorb_iff2 wellformed) lemma block_complement_subset_points: "ps \ (bl\<^sup>c) \ ps \ \" using block_complement_def by blast lemma obtain_comp_block_orig: assumes "bl1 \# \\<^sup>C" obtains bl2 where "bl2 \# \" and "bl1 = bl2\<^sup>c" using wellformed assms by (auto simp add: complement_blocks_def) lemma complement_same_b [simp]: "size \\<^sup>C = size \" by (simp add: complement_blocks_def) lemma block_comp_elem_alt_left: "x \ bl \ ps \ bl\<^sup>c \ x \ ps" by (auto simp add: block_complement_def block_complement_elem_iff) lemma block_comp_elem_alt_right: "ps \ \ \ (\ x . x \ ps \ x \ bl) \ ps \ bl\<^sup>c" by (auto simp add: block_complement_elem_iff) lemma complement_index: assumes "ps \ \" shows "\\<^sup>C index ps = size {# b \# \ . (\ x \ ps . x \ b) #}" proof - have "\\<^sup>C index ps = size {# b \# {# bl\<^sup>c . bl \# \#}. ps \ b #}" by (simp add: complement_blocks_def points_index_def) then have "\\<^sup>C index ps = size {# bl\<^sup>c | bl \# \ . ps \ bl\<^sup>c #}" by (metis image_mset_filter_swap) thus ?thesis using assms by (simp add: block_complement_elem_iff) qed lemma complement_index_2: assumes "{x, y} \ \" shows "\\<^sup>C index {x, y} = size {# b \# \ . x \ b \ y \ b #}" proof - have a: "\ b. b \# \ \ \ x' \ {x, y} . x' \ b \ x \ b \ y \ b" by simp have "\ b. b \# \ \ x \ b \ y \ b \ \ x' \ {x, y} . x' \ b " by simp thus ?thesis using assms a complement_index by (smt (verit) filter_mset_cong) qed lemma complement_rep_number: assumes "x \ \" and "\ rep x = r" shows "\\<^sup>C rep x = \ - r" proof - have r: "size {#b \# \ . x \ b#} = r" using assms by (simp add: point_replication_number_def) then have a: "\ b . b \# \ \ x \ b \ x \ b\<^sup>c" by (simp add: block_complement_def) have "\ b . b \# \ \ x \ b \ x \ b\<^sup>c" by (simp add: assms(1) block_complement_def) then have alt: "(image_mset block_complement \) rep x = size {#b \# \ . x \ b#}" using a filter_mset_cong image_mset_filter_swap2 point_replication_number_def by (smt (verit, ccfv_SIG) size_image_mset) have "\ = size {#b \# \ . x \ b#} + size {#b \# \ . x \ b#}" by (metis multiset_partition size_union) thus ?thesis using alt by (simp add: r complement_blocks_def) qed lemma complement_blocks_wf: "bl \# \\<^sup>C \ bl \ \" by (auto simp add: complement_blocks_def block_complement_def) lemma complement_wf [intro]: "incidence_system \ \\<^sup>C" using complement_blocks_wf by (unfold_locales) interpretation sys_complement: incidence_system "\" "\\<^sup>C" using complement_wf by simp end context finite_incidence_system begin lemma block_complement_size: "b \ \ \ card (b\<^sup>c) = card \ - card b" by (simp add: block_complement_def card_Diff_subset finite_subset card_mono of_nat_diff finite_sets) lemma block_comp_incomplete: "incomplete_block bl \ card (bl\<^sup>c) > 0" using block_complement_size by (simp add: wellformed) lemma block_comp_incomplete_nempty: "incomplete_block bl \ bl\<^sup>c \ {}" using wellformed block_complement_def finite_blocks by (auto simp add: block_complement_size block_comp_incomplete card_subset_not_gt_card) lemma incomplete_block_proper_subset: "incomplete_block bl \ bl \ \" using wellformed by fastforce lemma complement_finite: "finite_incidence_system \ \\<^sup>C" using complement_wf finite_sets by (simp add: incidence_system.finite_sysI) interpretation comp_fin: finite_incidence_system \ "\\<^sup>C" using complement_finite by simp end context design begin lemma (in design) complement_design: assumes "\ bl . bl \# \ \ incomplete_block bl" shows "design \ (\\<^sup>C)" proof - interpret fin: finite_incidence_system \ "\\<^sup>C" using complement_finite by simp show ?thesis using assms block_comp_incomplete_nempty wellformed by (unfold_locales) (auto simp add: complement_blocks_def) qed end subsubsection \Multiples\ text \An easy way to construct new set systems is to simply multiply the block collection by some constant\ context incidence_system begin abbreviation multiple_blocks :: "nat \ 'a set multiset" where "multiple_blocks n \ repeat_mset n \" lemma multiple_block_in_original: "b \# multiple_blocks n \ b \# \" by (simp add: elem_in_repeat_in_original) lemma multiple_block_in: "n > 0 \ b \# \ \ b \# multiple_blocks n" by (simp add: elem_in_original_in_repeat) lemma multiple_blocks_gt: "n > 0 \ size (multiple_blocks n) \ size \" by (simp) lemma block_original_count_le: "n > 0 \ count \ b \ count (multiple_blocks n) b" using count_repeat_mset by simp lemma multiple_blocks_sub: "n > 0 \ \ \# (multiple_blocks n)" by (simp add: mset_subset_eqI block_original_count_le) lemma multiple_1_same: "multiple_blocks 1 = \" by simp lemma multiple_unfold_1: "multiple_blocks (Suc n) = (multiple_blocks n) + \" by simp lemma multiple_point_rep_num: "(multiple_blocks n) rep x = (\ rep x) * n" proof (induction n) case 0 then show ?case by (simp add: point_replication_number_def) next case (Suc n) then have "multiple_blocks (Suc n) rep x = \ rep x * n + (\ rep x)" using Suc.IH Suc.prems by (simp add: union_commute point_replication_number_def) then show ?case - by (simp add: int_distrib(2)) + by (simp) qed lemma multiple_point_index: "(multiple_blocks n) index ps = (\ index ps) * n" by (induction n) (auto simp add: points_index_def) lemma repeat_mset_block_point_rel: "\b x. b \# multiple_blocks n \ x \ b \ x \ \" by (induction n) (auto, meson subset_iff wellformed) lemma multiple_is_wellformed: "incidence_system \ (multiple_blocks n)" using repeat_mset_subset_in wellformed repeat_mset_block_point_rel by (unfold_locales) (auto) lemma multiple_blocks_num [simp]: "size (multiple_blocks n) = n*\" by simp interpretation mult_sys: incidence_system \ "(multiple_blocks n)" by (simp add: multiple_is_wellformed) lemma multiple_block_multiplicity [simp]: "mult_sys.multiplicity n bl = (multiplicity bl) * n" by (simp) lemma multiple_block_sizes_same: assumes "n > 0" shows "sys_block_sizes = mult_sys.sys_block_sizes n" proof - have def: "mult_sys.sys_block_sizes n = {card bl | bl. bl \# (multiple_blocks n)}" by (simp add: mult_sys.sys_block_sizes_def) then have eq: "\ bl. bl \# (multiple_blocks n) \ bl \# \" using assms multiple_block_in multiple_block_in_original by blast thus ?thesis using def by (simp add: sys_block_sizes_def eq) qed end context finite_incidence_system begin lemma multiple_is_finite: "finite_incidence_system \ (multiple_blocks n)" using multiple_is_wellformed finite_sets by (unfold_locales) (auto simp add: incidence_system_def) end context design begin lemma multiple_is_design: "design \ (multiple_blocks n)" proof - interpret fis: finite_incidence_system \ "multiple_blocks n" using multiple_is_finite by simp show ?thesis using blocks_nempty by (unfold_locales) (auto simp add: elem_in_repeat_in_original repeat_mset_not_empty) qed end subsection \Simple Designs\ text \Simple designs are those in which the multiplicity of each block is at most one. In other words, the block collection is a set. This can significantly ease reasoning.\ locale simple_incidence_system = incidence_system + assumes simple [simp]: "bl \# \ \ multiplicity bl = 1" begin lemma simple_alt_def_all: "\ bl \# \ . multiplicity bl = 1" using simple by auto lemma simple_blocks_eq_sup: "mset_set (design_support) = \" using distinct_mset_def simple design_support_def by (metis distinct_mset_set_mset_ident) lemma simple_block_size_eq_card: "\ = card (design_support)" by (metis simple_blocks_eq_sup size_mset_set) lemma points_index_simple_def: "\ index ps = card {b \ design_support . ps \ b}" using design_support_def points_index_def card_size_filter_eq simple_blocks_eq_sup by (metis finite_set_mset) lemma replication_num_simple_def: "\ rep x = card {b \ design_support . x \ b}" using design_support_def point_replication_number_def card_size_filter_eq simple_blocks_eq_sup by (metis finite_set_mset) end locale simple_design = design + simple_incidence_system text \Additional reasoning about when something is not simple\ context incidence_system begin lemma simple_not_multiplicity: "b \# \ \ multiplicity b > 1 \ \ simple_incidence_system \ \" using simple_incidence_system_def simple_incidence_system_axioms_def by (metis nat_neq_iff) lemma multiple_not_simple: assumes "n > 1" assumes "\ \ {#}" shows "\ simple_incidence_system \ (multiple_blocks n)" proof (rule ccontr, simp) assume "simple_incidence_system \ (multiple_blocks n)" then have "\ bl. bl \# \ \ count (multiple_blocks n) bl = 1" using assms(1) elem_in_original_in_repeat by (metis not_gr_zero not_less_zero simple_incidence_system.simple) thus False using assms by auto qed end subsection \Proper Designs\ text \Many types of designs rely on parameter conditions that only make sense for non-empty designs. i.e. designs with at least one block, and therefore given well-formed condition, at least one point. To this end we define the notion of a "proper" design\ locale proper_design = design + assumes b_non_zero: "\ \ 0" begin lemma is_proper: "proper_design \ \" by intro_locales lemma v_non_zero: "\ > 0" using b_non_zero v_eq0_imp_b_eq_0 by auto lemma b_positive: "\ > 0" using b_non_zero by (simp add: nonempty_has_size) lemma design_points_nempty: "\ \ {}" using v_non_zero by auto lemma design_blocks_nempty: "\ \ {#}" using b_non_zero by auto end text \Intro rules for a proper design\ lemma (in design) proper_designI[intro]: "\ \ 0 \ proper_design \ \" by (unfold_locales) simp lemma proper_designII[intro]: assumes "design V B" and "B \ {#}" shows "proper_design V B" proof - interpret des: design V B using assms by simp show ?thesis using assms by unfold_locales simp qed text \Reasoning on construction closure for proper designs\ context proper_design begin lemma multiple_proper_design: assumes "n > 0" shows "proper_design \ (multiple_blocks n)" using multiple_is_design assms design_blocks_nempty multiple_block_in by (metis block_set_nempty_imp_block_ex empty_iff proper_designII set_mset_empty) lemma complement_proper_design: assumes "\ bl . bl \# \ \ incomplete_block bl" shows "proper_design \ \\<^sup>C" proof - interpret des: design \ "\\<^sup>C" by (simp add: assms complement_design) show ?thesis using b_non_zero by (unfold_locales) auto qed end end \ No newline at end of file diff --git a/thys/Design_Theory/Design_Operations.thy b/thys/Design_Theory/Design_Operations.thy --- a/thys/Design_Theory/Design_Operations.thy +++ b/thys/Design_Theory/Design_Operations.thy @@ -1,528 +1,528 @@ theory Design_Operations imports Design_Basics begin section \Design Operations\ text \Incidence systems have a number of very typical computational operations which can be used for constructions in design theory. Definitions in this section are based off the handbook of combinatorial designs, hypergraph theory \cite{bergeHypergraphsCombinatoricsFinite1989}, and the GAP design theory library \cite{soicherDesignsGroupsComputing2013}\ subsection \Incidence system definitions\ context incidence_system begin text \The basic add point operation only affects the point set of a design\ definition add_point :: "'a \ 'a set" where "add_point p \ insert p \" lemma add_existing_point [simp]: "p \ \ \ add_point p = \" using add_point_def by fastforce lemma add_point_wf: "incidence_system (add_point p) \" using wf_invalid_point add_point_def by (unfold_locales) (auto) text \An extension of the basic add point operation also adds the point to a given set of blocks\ definition add_point_to_blocks :: "'a \ 'a set set \ 'a set multiset" where "add_point_to_blocks p bs \ {# (insert p b) | b \# \ . b \ bs#} + {# b \# \ . b \ bs#}" lemma add_point_blocks_blocks_alt: "add_point_to_blocks p bs = image_mset (insert p) (filter_mset (\ b . b \ bs) \) + (filter_mset (\ b . b \ bs) \)" using add_point_to_blocks_def by simp lemma add_point_existing_blocks: assumes "(\ bl . bl \ bs \ p \ bl)" shows "add_point_to_blocks p bs = \" proof (simp add: add_point_to_blocks_def) have "image_mset (insert p) {#b \# \. b \ bs#} = {#b \# \. b \ bs#}" using assms by (simp add: image_filter_cong insert_absorb) thus "image_mset (insert p) {#b \# \. b \ bs#} + {#b \# \. b \ bs#} = \" using multiset_partition by simp qed lemma add_new_point_rep_number: assumes "p \ \" shows "(add_point_to_blocks p bs) rep p = size {#b \# \ . b \ bs#}" proof - have "\ b. b \# \ \ b \ bs \ p \ b" by (simp add: assms wf_invalid_point) then have zero: "{# b \# \ . b \ bs#} rep p = 0" by (simp add: filter_mset_empty_conv point_replication_number_def) have "(add_point_to_blocks p bs) rep p = {# (insert p b) | b \# \ . b \ bs#} rep p + {# b \# \ . b \ bs#} rep p" by (simp add: add_point_to_blocks_def) then have eq: "(add_point_to_blocks p bs) rep p = {# (insert p b) | b \# \ . b \ bs#} rep p" using zero by simp have "\ bl . bl \# {# (insert p b) | b \# \ . b \ bs#} \ p \ bl" by auto then have "{# (insert p b) | b \# \ . b \ bs#} rep p = size {# (insert p b) | b \# \ . b \ bs#}" using point_replication_number_def by (metis filter_mset_True filter_mset_cong) thus ?thesis by (simp add: eq) qed lemma add_point_blocks_wf: "incidence_system (add_point p) (add_point_to_blocks p bs)" by (unfold_locales) (auto simp add: add_point_def wf_invalid_point add_point_to_blocks_def) text \Basic (weak) delete point operation removes a point from both the point set and from any blocks that contain it to maintain wellformed property\ definition del_point :: "'a \ 'a set" where "del_point p \ \ - {p}" definition del_point_blocks:: "'a \ 'a set multiset" where "del_point_blocks p \ {# (bl - {p}) . bl \# \ #}" lemma del_point_block_count: "size (del_point_blocks p) = size \" by (simp add: del_point_blocks_def) lemma remove_invalid_point_block: "p \ \ \ bl \# \ \ bl - {p} = bl" using wf_invalid_point by blast lemma del_invalid_point: "p \ \ \ (del_point p) = \" by (simp add: del_point_def) lemma del_invalid_point_blocks: "p \ \ \ (del_point_blocks p) = \" using del_invalid_point by (auto simp add: remove_invalid_point_block del_point_blocks_def) lemma delete_point_p_not_in_bl_blocks: "(\ bl. bl \# \ \ p \ bl) \ (del_point_blocks p) = \" by (simp add: del_point_blocks_def) lemma delete_point_blocks_wf: "b \# (del_point_blocks p) \ b \ \ - {p}" unfolding del_point_blocks_def using wellformed by auto lemma delete_point_blocks_sub: assumes "b \# (del_point_blocks p)" obtains bl where "bl \# \ \ b \ bl" using assms by (auto simp add: del_point_blocks_def) lemma delete_point_split_blocks: "del_point_blocks p = {# bl \#\ . p \ bl#} + {# bl - {p} | bl \# \ . p \ bl#}" proof - have sm: "\ bl . p \ bl \ bl - {p} = bl" by simp have "del_point_blocks p = {# (bl - {p}) . bl \# \ #}" by (simp add: del_point_blocks_def) also have "... = {# (bl - {p}) | bl \# \ . p \ bl #} + {# (bl - {p}) | bl \# \ . p \ bl #}" using multiset_partition by (metis image_mset_union union_commute) finally have "del_point_blocks p = {#bl | bl \# \ . p \ bl#} + {# (bl - {p}) | bl \# \ . p \ bl #}" using sm mem_Collect_eq by (metis (mono_tags, lifting) Multiset.set_mset_filter multiset.map_cong) thus ?thesis by simp qed lemma delete_point_index_eq: assumes "ps \ (del_point p)" shows "(del_point_blocks p) index ps = \ index ps" proof - have eq: "filter_mset ((\) ps) {#bl - {p}. bl \# \#} = image_mset (\ b . b - {p}) (filter_mset (\ b. ps \ b - {p}) \)" using filter_mset_image_mset by blast have "p \ ps" using assms del_point_def by blast then have "\ bl . ps \ bl \ ps \ bl - {p}" by blast then have "((filter_mset (\ b. ps \ b - {p}) \)) = (filter_mset (\ b . ps \ b) \)" by auto then have "size (image_mset (\ b . b - {p}) (filter_mset (\ b. ps \ b - {p}) \)) = \ index ps" by (simp add: points_index_def) thus ?thesis using eq by (simp add: del_point_blocks_def points_index_def) qed lemma delete_point_wf: "incidence_system (del_point p) (del_point_blocks p)" using delete_point_blocks_wf del_point_def by (unfold_locales) auto text \The concept of a strong delete point comes from hypergraph theory. When a point is deleted, any blocks containing it are also deleted\ definition str_del_point_blocks :: "'a \ 'a set multiset" where "str_del_point_blocks p \ {# bl \# \ . p \ bl#}" lemma str_del_point_blocks_alt: "str_del_point_blocks p = \ - {# bl \# \ . p \ bl#}" using add_diff_cancel_left' multiset_partition by (metis str_del_point_blocks_def) lemma delete_point_strong_block_in: "p \ bl \ bl \# \ \ bl \# str_del_point_blocks p" by (simp add: str_del_point_blocks_def) lemma delete_point_strong_block_not_in: "p \ bl \ bl \# (str_del_point_blocks) p" by (simp add: str_del_point_blocks_def) lemma delete_point_strong_block_in_iff: "bl \# \ \ bl \# str_del_point_blocks p \ p \ bl" using delete_point_strong_block_in delete_point_strong_block_not_in by (simp add: str_del_point_blocks_def) lemma delete_point_strong_block_subset: "str_del_point_blocks p \# \" by (simp add: str_del_point_blocks_def) lemma delete_point_strong_block_in_orig: "bl \# str_del_point_blocks p \ bl \# \" using delete_point_strong_block_subset by (metis mset_subset_eqD) lemma delete_invalid_pt_strong_eq: "p \ \ \ \ = str_del_point_blocks p" unfolding str_del_point_blocks_def using wf_invalid_point empty_iff by (metis Multiset.diff_cancel filter_mset_eq_conv set_mset_empty subset_mset.order_refl) lemma strong_del_point_index_alt: assumes "ps \ (del_point p)" shows "(str_del_point_blocks p) index ps = \ index ps - {# bl \# \ . p \ bl#} index ps" using str_del_point_blocks_alt points_index_def by (metis filter_diff_mset multiset_filter_mono multiset_filter_subset size_Diff_submset) lemma strong_del_point_incidence_wf: "incidence_system (del_point p) (str_del_point_blocks p)" using wellformed str_del_point_blocks_def del_point_def by (unfold_locales) auto text \Add block operation\ definition add_block :: "'a set \ 'a set multiset" where "add_block b \ \ + {#b#}" lemma add_block_alt: "add_block b = add_mset b \" by (simp add: add_block_def) lemma add_block_rep_number_in: assumes "x \ b" shows "(add_block b) rep x = \ rep x + 1" proof - have "(add_block b) = {#b#} + \" by (simp add: add_block_def) then have split: "(add_block b) rep x = {#b#} rep x + \ rep x" by (metis point_rep_number_split) have "{#b#} rep x = 1" using assms by simp thus ?thesis using split by auto qed lemma add_block_rep_number_not_in: "x \ b \ (add_block b) rep x = \ rep x" using point_rep_number_split add_block_alt point_rep_singleton_inval by (metis add.right_neutral union_mset_add_mset_right) lemma add_block_index_in: assumes "ps \ b" shows "(add_block b) index ps = \ index ps + 1" proof - have "(add_block b) = {#b#} + \" by (simp add: add_block_def) then have split: "(add_block b) index ps = {#b#} index ps + \ index ps" by (metis point_index_distrib) have "{#b#} index ps = 1" using assms points_index_singleton by auto thus ?thesis using split by simp qed lemma add_block_index_not_in: "\ (ps \ b) \ (add_block b) index ps = \ index ps" using point_index_distrib points_index_singleton_zero by (metis add.right_neutral add_block_def) text \Note the add block incidence system is defined slightly differently then textbook definitions due to the modification to the point set. This ensures the operation is closed, where otherwise a condition that $b \subseteq \mathcal{V}$ would be required.\ lemma add_block_wf: "incidence_system (\ \ b) (add_block b)" using wellformed add_block_def by (unfold_locales) auto lemma add_block_wf_cond: "b \ \ \ incidence_system \ (add_block b)" using add_block_wf by (metis sup.order_iff) text \Delete block removes a block from the block set. The point set is unchanged\ definition del_block :: "'a set \ 'a set multiset" where "del_block b \ \ - {#b#}" lemma delete_block_subset: "(del_block b) \# \" by (simp add: del_block_def) lemma delete_invalid_block_eq: "b \# \ \ del_block b = \" by (simp add: del_block_def) lemma delete_block_wf: "incidence_system \ (del_block b)" by (unfold_locales) (simp add: del_block_def in_diffD wellformed) text \The strong delete block operation effectively deletes the block, as well as all points in that block\ definition str_del_block :: "'a set \ 'a set multiset" where "str_del_block b \ {# bl - b | bl \# \ . bl \ b #}" lemma strong_del_block_alt_def: "str_del_block b = {# bl - b . bl \# removeAll_mset b \ #}" by (simp add: filter_mset_neq str_del_block_def) lemma strong_del_block_wf: "incidence_system (\ - b) (str_del_block b)" using wf_invalid_point str_del_block_def by (unfold_locales) auto lemma str_del_block_del_point: assumes "{x} \# \" shows "str_del_block {x} = (del_point_blocks x)" proof - have neqx: "\ bl. bl \# \ \ bl \ {x}" using assms by auto have "str_del_block {x} = {# bl - {x} | bl \# \ . bl \ {x} #}" by (simp add: str_del_block_def) then have "str_del_block {x} = {# bl - {x} . bl \# \ #}" using assms neqx by (simp add: filter_mset_cong) thus ?thesis by (simp add: del_point_blocks_def) qed subsection \Incidence System Interpretations\ text \It is easy to interpret all operations as incidence systems in there own right. These can then be used to prove local properties on the new constructions, as well as reason on interactions between different operation sequences\ interpretation add_point_sys: incidence_system "add_point p" "\" using add_point_wf by simp lemma add_point_sys_rep_numbers: "add_point_sys.replication_numbers p = replication_numbers \ {\ rep p}" using add_point_sys.replication_numbers_def replication_numbers_def add_point_def by auto interpretation del_point_sys: incidence_system "del_point p" "del_point_blocks p" using delete_point_wf by auto interpretation add_block_sys: incidence_system "\ \ bl" "add_block bl" using add_block_wf by simp interpretation del_block_sys: incidence_system "\" "del_block bl" using delete_block_wf by simp lemma add_del_block_inv: assumes "bl \ \" shows "add_block_sys.del_block bl bl = \" using add_block_sys.del_block_def add_block_def by simp lemma del_add_block_inv: "bl \# \ \ del_block_sys.add_block bl bl = \" using del_block_sys.add_block_def del_block_def wellformed by fastforce lemma del_invalid_add_block_eq: "bl \# \ \ del_block_sys.add_block bl bl = add_block bl" using del_block_sys.add_block_def by (simp add: delete_invalid_block_eq) lemma add_delete_point_inv: assumes "p \ \" shows "add_point_sys.del_point p p = \" proof - have "(add_point_sys.del_point p p) = (insert p \) - {p}" using add_point_sys.del_point_def del_block_sys.add_point_def by auto thus ?thesis by (simp add: assms) qed end subsection \Operation Closure for Designs\ context finite_incidence_system begin lemma add_point_finite: "finite_incidence_system (add_point p) \" using add_point_wf finite_sets add_point_def by (unfold_locales) (simp_all add: incidence_system_def) lemma add_point_to_blocks_finite: "finite_incidence_system (add_point p) (add_point_to_blocks p bs)" using add_point_blocks_wf add_point_finite finite_incidence_system.finite_sets incidence_system.finite_sysI by blast lemma delete_point_finite: "finite_incidence_system (del_point p) (del_point_blocks p)" using finite_sets delete_point_wf by (unfold_locales) (simp_all add: incidence_system_def del_point_def) lemma del_point_order: assumes "p \ \" shows "card (del_point p) = \ - 1" proof - have vg0: "card \ > 0" using assms finite_sets card_gt_0_iff by auto then have "card (del_point p) = card \ - 1" using assms del_point_def - by (metis card_Diff_singleton finite_sets) + by (metis card_Diff_singleton) thus ?thesis using vg0 by linarith qed lemma strong_del_point_finite:"finite_incidence_system (del_point p) (str_del_point_blocks p)" using strong_del_point_incidence_wf del_point_def by (intro_locales) (simp_all add: finite_incidence_system_axioms_def finite_sets) lemma add_block_fin: "finite b \ finite_incidence_system (\ \ b) (add_block b)" using wf_invalid_point finite_sets add_block_def by (unfold_locales) auto lemma add_block_fin_cond: "b \ \ \ finite_incidence_system \ (add_block b)" using add_block_wf_cond finite_incidence_system_axioms.intro finite_sets by (intro_locales) (simp_all) lemma delete_block_fin_incidence_sys: "finite_incidence_system \ (del_block b)" using delete_block_wf finite_sets by (unfold_locales) (simp_all add: incidence_system_def) lemma strong_del_block_fin: "finite_incidence_system (\ - b) (str_del_block b)" using strong_del_block_wf finite_sets finite_incidence_system_axioms_def by (intro_locales) auto end context design begin lemma add_point_design: "design (add_point p) \" using add_point_wf finite_sets blocks_nempty add_point_def by (unfold_locales) (auto simp add: incidence_system_def) lemma delete_point_design: assumes "(\ bl . bl \# \ \ p \ bl \ card bl \ 2)" shows "design (del_point p) (del_point_blocks p)" proof (cases "p \ \") case True interpret fis: finite_incidence_system "(del_point p)" "(del_point_blocks p)" using delete_point_finite by simp show ?thesis proof (unfold_locales) show "\bl. bl \# (del_point_blocks p) \ bl \ {}" using assms del_point_def proof - fix bl assume "bl \#(del_point_blocks p)" then obtain bl' where block: "bl' \# \" and rem: "bl = bl' - {p}" by (auto simp add: del_point_blocks_def) then have eq: "p \ bl' \ bl \ {}" using block blocks_nempty by (simp add: rem) have "p \ bl' \ card bl \ 1" using rem finite_blocks block assms block by fastforce then show "bl \ {}" using eq assms by fastforce qed qed next case False then show ?thesis using del_invalid_point del_invalid_point_blocks by (simp add: wf_design) qed lemma strong_del_point_design: "design (del_point p) (str_del_point_blocks p)" proof - interpret fin: finite_incidence_system "(del_point p)" "(str_del_point_blocks p)" using strong_del_point_finite by simp show ?thesis using wf_design wf_design_iff del_point_def str_del_point_blocks_def by (unfold_locales) (auto) qed lemma add_block_design: assumes "finite bl" assumes "bl \ {}" shows "design (\ \ bl) (add_block bl)" proof - interpret fin: finite_incidence_system "(\ \ bl)" "(add_block bl)" using add_block_fin assms by simp show ?thesis using blocks_nempty assms add_block_def by (unfold_locales) auto qed lemma add_block_design_cond: assumes "bl \ \" and "bl \ {}" shows "design \ (add_block bl)" proof - interpret fin: finite_incidence_system "\" "(add_block bl)" using add_block_fin_cond assms by simp show ?thesis using blocks_nempty assms add_block_def by (unfold_locales) auto qed lemma delete_block_design: "design \ (del_block bl)" proof - interpret fin: finite_incidence_system \ "(del_block bl)" using delete_block_fin_incidence_sys by simp have "\ b . b \# (del_block bl) \ b \ {}" using blocks_nempty delete_block_subset by blast then show ?thesis by (unfold_locales) (simp_all) qed lemma strong_del_block_des: assumes "\ bl . bl \# \ \ \ (bl \ b)" shows "design (\ - b) (str_del_block b)" proof - interpret fin: finite_incidence_system "\ - b" "(str_del_block b)" using strong_del_block_fin by simp show ?thesis using assms str_del_block_def by (unfold_locales) auto qed end context proper_design begin lemma delete_point_proper: assumes "\bl. bl \# \ \ p \ bl \ 2 \ card bl" shows "proper_design (del_point p) (del_point_blocks p)" proof - interpret des: design "del_point p" "del_point_blocks p" using delete_point_design assms by blast show ?thesis using design_blocks_nempty del_point_def del_point_blocks_def by (unfold_locales) simp qed lemma strong_delete_point_proper: assumes "\bl. bl \# \ \ p \ bl \ 2 \ card bl" assumes "\ rep p < \" shows "proper_design (del_point p) (str_del_point_blocks p)" proof - interpret des: design "del_point p" "str_del_point_blocks p" using strong_del_point_design assms by blast show ?thesis using assms design_blocks_nempty point_rep_num_inv_non_empty str_del_point_blocks_def del_point_def by (unfold_locales) simp qed end subsection \Combining Set Systems\ text \Similar to multiple, another way to construct a new set system is to combine two existing ones. We introduce a new locale enabling us to reason on two different incidence systems\ locale two_set_systems = sys1: incidence_system \ \ + sys2: incidence_system \' \' for \ :: "('a set)" and \ and \' :: "('a set)" and \' begin abbreviation "combine_points \ \ \ \'" notation combine_points ("\\<^sup>+") abbreviation "combine_blocks \ \ + \'" notation combine_blocks ("\\<^sup>+") sublocale combine_sys: incidence_system "\\<^sup>+" "\\<^sup>+" using sys1.wellformed sys2.wellformed by (unfold_locales) auto lemma combine_points_index: "\\<^sup>+ index ps = \ index ps + \' index ps" by (simp add: point_index_distrib) lemma combine_rep_number: "\\<^sup>+ rep x = \ rep x + \' rep x" by (simp add: point_replication_number_def) lemma combine_multiple1: "\ = \' \ \ = \' \ \\<^sup>+ = sys1.multiple_blocks 2" by auto lemma combine_multiple2: "\ = \' \ \ = \' \ \\<^sup>+ = sys2.multiple_blocks 2" by auto lemma combine_multiplicity: "combine_sys.multiplicity b = sys1.multiplicity b + sys2.multiplicity b" by simp lemma combine_block_sizes: "combine_sys.sys_block_sizes = sys1.sys_block_sizes \ sys2.sys_block_sizes" using sys1.sys_block_sizes_def sys2.sys_block_sizes_def combine_sys.sys_block_sizes_def by (auto) end locale two_fin_set_systems = two_set_systems \ \ \' \' + sys1: finite_incidence_system \ \ + sys2: finite_incidence_system \' \' for \ \ \' \' begin sublocale combine_fin_sys: finite_incidence_system "\\<^sup>+" "\\<^sup>+" using sys1.finite_sets sys2.finite_sets by (unfold_locales) (simp) lemma combine_order: "card (\\<^sup>+) \ card \" by (meson Un_upper1 card_mono combine_fin_sys.finite_sets) lemma combine_order_2: "card (\\<^sup>+) \ card \'" by (meson Un_upper2 card_mono combine_fin_sys.finite_sets) end locale two_designs = two_fin_set_systems \ \ \' \' + des1: design \ \ + des2: design \' \' for \ \ \' \' begin sublocale combine_des: design "\\<^sup>+" "\\<^sup>+" apply (unfold_locales) using des1.blocks_nempty_alt des2.blocks_nempty_alt by fastforce end locale two_designs_proper = two_designs + assumes blocks_nempty: "\ \ {#} \ \' \ {#}" begin lemma des1_is_proper: "\ \ {#} \ proper_design \ \" by (unfold_locales) (simp) lemma des2_is_proper: "\' \ {#} \ proper_design \' \'" by (unfold_locales) (simp) lemma min_one_proper_design: "proper_design \ \ \ proper_design \' \'" using blocks_nempty des1_is_proper des2_is_proper by (unfold_locales, blast) sublocale combine_proper_des: proper_design "\\<^sup>+" "\\<^sup>+" apply (unfold_locales) - by (metis blocks_nempty of_nat_0_eq_iff size_eq_0_iff_empty subset_mset.zero_eq_add_iff_both_eq_0) + by (metis blocks_nempty size_eq_0_iff_empty subset_mset.zero_eq_add_iff_both_eq_0) end end \ No newline at end of file diff --git a/thys/Design_Theory/Designs_And_Graphs.thy b/thys/Design_Theory/Designs_And_Graphs.thy --- a/thys/Design_Theory/Designs_And_Graphs.thy +++ b/thys/Design_Theory/Designs_And_Graphs.thy @@ -1,336 +1,336 @@ (* Title: Designs_And_Graphs.thy Author: Chelsea Edmonds *) section \Graphs and Designs\ text \There are many links between graphs and design - most fundamentally that graphs are designs\ theory Designs_And_Graphs imports Block_Designs Graph_Theory.Digraph Graph_Theory.Digraph_Component begin subsection \Non-empty digraphs\ text \First, we define the concept of a non-empty digraph. This mirrors the idea of a "proper design" in the design theory library\ locale non_empty_digraph = wf_digraph + assumes arcs_not_empty: "arcs G \ {}" begin lemma verts_not_empty: "verts G \ {}" using wf arcs_not_empty head_in_verts by fastforce end subsection \Arcs to Blocks\ text \A digraph uses a pair of points to define an ordered edge. In the case of simple graphs, both possible orderings will be in the arcs set. Blocks are inherently unordered, and as such a method is required to convert between the two representations\ context graph begin definition arc_to_block :: "'b \ 'a set" where "arc_to_block e \ {tail G e, head G e}" lemma arc_to_block_to_ends: "{fst (arc_to_ends G e), snd (arc_to_ends G e)} = arc_to_block e" by (simp add: arc_to_ends_def arc_to_block_def) lemma arc_to_block_to_ends_swap: "{snd (arc_to_ends G e), fst (arc_to_ends G e)} = arc_to_block e" using arc_to_block_to_ends by (simp add: arc_to_block_to_ends insert_commute) lemma arc_to_ends_to_block: "arc_to_block e = {x, y} \ arc_to_ends G e = (x, y) \ arc_to_ends G e = (y, x)" by (metis arc_to_block_def arc_to_ends_def doubleton_eq_iff) lemma arc_to_block_sym: "arc_to_ends G e1 = (u, v) \ arc_to_ends G e2 = (v, u) \ arc_to_block e1 = arc_to_block e2" by (simp add: arc_to_block_def arc_to_ends_def insert_commute) definition arcs_blocks :: "'a set multiset" where "arcs_blocks \ mset_set (arc_to_block ` (arcs G))" lemma arcs_blocks_ends: "(x, y) \ arcs_ends G \ {x, y} \# arcs_blocks" proof (auto simp add: arcs_ends_def arcs_blocks_def ) fix xa assume assm1: "(x, y) = arc_to_ends G xa" and assm2: "xa \ arcs G" obtain z where zin: "z \ (arc_to_block ` (arcs G))" and "z = arc_to_block xa" using assm2 by blast thus "{x, y} \ arc_to_block ` (arcs G)" using assm1 arc_to_block_to_ends by (metis fst_conv snd_conv) qed lemma arc_ends_blocks_subset: "E \ arcs G \ (x, y) \ ((arc_to_ends G) ` E) \ {x, y} \ (arc_to_block ` E)" by (auto simp add: arc_to_ends_def arc_to_block_def ) lemma arc_blocks_end_subset: assumes "E \ arcs G" and "{x, y} \ (arc_to_block ` E)" shows "(x, y) \ ((arc_to_ends G) ` E) \ (y, x) \ ((arc_to_ends G) ` E)" proof - obtain e where "e \ E" and "arc_to_block e = {x,y}" using assms by fastforce then have "arc_to_ends G e = (x, y) \ arc_to_ends G e = (y, x)" using arc_to_ends_to_block by simp thus ?thesis by (metis \e \ E\ image_iff) qed lemma arcs_ends_blocks: "{x, y} \# arcs_blocks \ (x, y) \ arcs_ends G \ (y, x) \ arcs_ends G" proof (auto simp add: arcs_ends_def arcs_blocks_def ) fix xa assume assm1: "{x, y} = arc_to_block xa" and assm2: "xa \ (arcs G)" obtain z where zin: "z \ (arc_to_ends G ` (arcs G))" and "z = arc_to_ends G xa" using assm2 by blast then have "z = (x, y) \ z = (y, x)" using arc_to_block_to_ends assm1 by (metis arc_to_ends_def doubleton_eq_iff fst_conv snd_conv) (* Slow *) thus "(x, y) \ arc_to_ends G ` (arcs G)" using assm2 by (metis arcs_ends_def arcs_ends_symmetric sym_arcs zin) next fix xa assume assm1: "{x, y} = arc_to_block xa" and assm2: "xa \ (arcs G)" thus "(y, x) \ arc_to_ends G ` arcs G" using arcs_ends_def by (metis dual_order.refl graph.arc_blocks_end_subset graph_axioms graph_symmetric imageI) qed lemma arcs_blocks_iff: "{x, y} \# arcs_blocks \ (x, y) \ arcs_ends G \ (y, x) \ arcs_ends G" using arcs_ends_blocks arcs_blocks_ends by blast lemma arcs_ends_wf: "(x, y) \ arcs_ends G \ x \ verts G \ y \ verts G" by auto lemma arcs_blocks_elem: "bl \# arcs_blocks \ \ x y . bl = {x, y}" apply (auto simp add: arcs_blocks_def) by (meson arc_to_block_def) lemma arcs_ends_blocks_wf: assumes "bl \# arcs_blocks" shows "bl \ verts G" proof - obtain x y where blpair: "bl = {x, y}" using arcs_blocks_elem assms by fastforce then have "(x, y) \ arcs_ends G" using arcs_ends_blocks assms by simp thus ?thesis using arcs_ends_wf blpair by auto qed lemma arcs_blocks_simple: "bl \# arcs_blocks \ count (arcs_blocks) bl = 1" by (simp add: arcs_blocks_def) lemma arcs_blocks_ne: "arcs G \ {} \ arcs_blocks \ {#}" by (simp add: arcs_blocks_iff arcs_blocks_def mset_set_empty_iff) end subsection \Graphs are designs\ text \Prove that a graph is a number of different types of designs\ sublocale graph \ design "verts G" "arcs_blocks" using arcs_ends_blocks_wf arcs_blocks_elem by (unfold_locales) (auto) sublocale graph \ simple_design "verts G" "arcs_blocks" using arcs_ends_blocks_wf arcs_blocks_elem arcs_blocks_simple by (unfold_locales) (auto) locale non_empty_graph = graph + non_empty_digraph sublocale non_empty_graph \ proper_design "verts G" "arcs_blocks" using arcs_blocks_ne arcs_not_empty by (unfold_locales) simp lemma (in graph) graph_block_size: assumes "bl \# arcs_blocks" shows "card bl = 2" proof - obtain x y where blrep: "bl = {x, y}" using assms arcs_blocks_elem by fastforce then have "(x, y) \ arcs_ends G" using arcs_ends_blocks assms by simp then have "x \ y" using no_loops using adj_not_same by blast thus ?thesis using blrep by simp qed sublocale non_empty_graph \ block_design "verts G" "arcs_blocks" 2 using arcs_not_empty graph_block_size arcs_blocks_ne by (unfold_locales) simp_all subsection \R-regular graphs\ text \To reason on r-regular graphs and their link to designs, we require a number of extensions to lemmas reasoning around the degrees of vertices\ context sym_digraph begin lemma in_out_arcs_reflexive: "v \ verts G \ (e \ (in_arcs G v) \ \ e' . (e' \ (out_arcs G v) \ head G e' = tail G e))" using symmetric_conv sym_arcs by fastforce lemma out_in_arcs_reflexive: "v \ verts G \ (e \ (out_arcs G v) \ \ e' . (e' \ (in_arcs G v) \ tail G e' = head G e))" using symmetric_conv sym_arcs by fastforce end context nomulti_digraph begin lemma in_arcs_single_per_vert: assumes "v \ verts G" and "u \ verts G" assumes "e1 \ in_arcs G v" and " e2 \ in_arcs G v" assumes "tail G e1 = u" and "tail G e2 = u" shows "e1 = e2" proof - have in_arcs1: "e1 \ arcs G" and in_arcs2: "e2 \ arcs G" using assms by auto have "arc_to_ends G e1 = arc_to_ends G e2" using assms arc_to_ends_def by (metis in_in_arcs_conv) thus ?thesis using in_arcs1 in_arcs2 no_multi_arcs by simp qed lemma out_arcs_single_per_vert: assumes "v \ verts G" and "u \ verts G" assumes "e1 \ out_arcs G v" and " e2 \ out_arcs G v" assumes "head G e1 = u" and "head G e2 = u" shows "e1 = e2" proof - have in_arcs1: "e1 \ arcs G" and in_arcs2: "e2 \ arcs G" using assms by auto have "arc_to_ends G e1 = arc_to_ends G e2" using assms arc_to_ends_def by (metis in_out_arcs_conv) thus ?thesis using in_arcs1 in_arcs2 no_multi_arcs by simp qed end text \Some helpers on the transformation arc definition\ context graph begin lemma arc_to_block_is_inj_in_arcs: "inj_on arc_to_block (in_arcs G v)" apply (auto simp add: arc_to_block_def inj_on_def) by (metis arc_to_ends_def doubleton_eq_iff no_multi_arcs) lemma arc_to_block_is_inj_out_arcs: "inj_on arc_to_block (out_arcs G v)" apply (auto simp add: arc_to_block_def inj_on_def) by (metis arc_to_ends_def doubleton_eq_iff no_multi_arcs) lemma in_out_arcs_reflexive_uniq: "v \ verts G \ (e \ (in_arcs G v) \ \! e' . (e' \ (out_arcs G v) \ head G e' = tail G e))" apply auto using symmetric_conv apply fastforce using out_arcs_single_per_vert by (metis head_in_verts in_out_arcs_conv) lemma out_in_arcs_reflexive_uniq: "v \ verts G \ e \ (out_arcs G v) \ \! e' . (e' \ (in_arcs G v) \ tail G e' = head G e)" apply auto using symmetric_conv apply fastforce using in_arcs_single_per_vert by (metis tail_in_verts in_in_arcs_conv) lemma in_eq_out_arc_ends: "(u, v) \ ((arc_to_ends G) ` (in_arcs G v)) \ (v, u) \ ((arc_to_ends G) ` (out_arcs G v))" using arc_to_ends_def in_in_arcs_conv in_out_arcs_conv by (smt (z3) Pair_inject adj_in_verts(1) dominatesI image_iff out_in_arcs_reflexive_uniq) lemma in_degree_eq_card_arc_ends: "in_degree G v = card ((arc_to_ends G) ` (in_arcs G v))" apply (simp add: in_degree_def) using no_multi_arcs by (metis card_image in_arcs_in_arcs inj_onI) lemma in_degree_eq_card_arc_blocks: "in_degree G v = card (arc_to_block ` (in_arcs G v))" apply (simp add: in_degree_def) using no_multi_arcs arc_to_block_is_inj_in_arcs by (simp add: card_image) lemma out_degree_eq_card_arc_blocks: "out_degree G v = card (arc_to_block ` (out_arcs G v))" apply (simp add: out_degree_def) using no_multi_arcs arc_to_block_is_inj_out_arcs by (simp add: card_image) lemma out_degree_eq_card_arc_ends: "out_degree G v = card ((arc_to_ends G) ` (out_arcs G v))" apply (simp add: out_degree_def) using no_multi_arcs by (metis card_image out_arcs_in_arcs inj_onI) lemma bij_betw_in_out_arcs: "bij_betw (\ (u, v) . (v, u)) ((arc_to_ends G) ` (in_arcs G v)) ((arc_to_ends G) ` (out_arcs G v))" apply (auto simp add: bij_betw_def) apply (simp add: swap_inj_on) apply (metis Pair_inject arc_to_ends_def image_eqI in_eq_out_arc_ends in_in_arcs_conv) by (metis arc_to_ends_def imageI in_eq_out_arc_ends in_out_arcs_conv pair_imageI) lemma in_eq_out_degree: "in_degree G v = out_degree G v" using bij_betw_in_out_arcs bij_betw_same_card in_degree_eq_card_arc_ends out_degree_eq_card_arc_ends by auto lemma in_out_arcs_blocks: "arc_to_block ` (in_arcs G v) = arc_to_block ` (out_arcs G v)" proof (auto) fix xa assume a1: "xa \ arcs G" and a2: "v = head G xa" then have "xa \ in_arcs G v" by simp then obtain e where out: "e \ out_arcs G v" and "head G e = tail G xa" using out_in_arcs_reflexive_uniq by force then have "arc_to_ends G e = (v, tail G xa)" by (simp add: arc_to_ends_def) then have "arc_to_block xa = arc_to_block e" using arc_to_block_sym by (metis a2 arc_to_ends_def) then show "arc_to_block xa \ arc_to_block ` out_arcs G (head G xa)" using out a2 by blast next fix xa assume a1: "xa \ arcs G" and a2: "v = tail G xa" then have "xa \ out_arcs G v" by simp then obtain e where ina: "e \ in_arcs G v" and "tail G e = head G xa" using out_in_arcs_reflexive_uniq by force then have "arc_to_ends G e = (head G xa, v)" by (simp add: arc_to_ends_def) then have "arc_to_block xa = arc_to_block e" using arc_to_block_sym by (metis a2 arc_to_ends_def) then show "arc_to_block xa \ arc_to_block ` in_arcs G (tail G xa)" using ina a2 by blast qed end text \A regular digraph is defined as one where the in degree equals the out degree which in turn equals some fixed integer $\mathrm{r}$\ locale regular_digraph = wf_digraph + - fixes \ :: int + fixes \ :: nat assumes in_deg_r: "v \ verts G \ in_degree G v = \" assumes out_deg_r: "v \ verts G \ out_degree G v = \" locale regular_graph = graph + regular_digraph begin lemma rep_vertices_in_blocks [simp]: assumes "x \ verts G" shows "size {# e \# arcs_blocks . x \ e #} = \" proof - have "\ e . e \ (arc_to_block ` (arcs G)) \ x \ e \ e \ (arc_to_block ` in_arcs G x)" using arc_to_block_def in_in_arcs_conv insert_commute insert_iff singleton_iff sym_arcs symmetric_conv by fastforce then have "{ e \ (arc_to_block ` (arcs G)) . x \ e} = (arc_to_block ` (in_arcs G x))" using arc_to_block_def by auto then have "card { e \ (arc_to_block ` (arcs G)) . x \ e} = \" using in_deg_r in_degree_eq_card_arc_blocks assms by auto thus ?thesis using arcs_blocks_def finite_arcs by force qed end text \Intro rules for regular graphs\ lemma graph_in_degree_r_imp_reg[intro]: assumes "graph G" assumes "(\ v . v \ (verts G) \ in_degree G v = \)" shows "regular_graph G \" proof - interpret g: graph G using assms by simp interpret wf: wf_digraph G by (simp add: g.wf_digraph_axioms) show ?thesis using assms(2) g.in_eq_out_degree by (unfold_locales) simp_all qed lemma graph_out_degree_r_imp_reg[intro]: assumes "graph G" assumes "(\ v . v \ (verts G) \ out_degree G v = \)" shows "regular_graph G \" proof - interpret g: graph G using assms by simp interpret wf: wf_digraph G by (simp add: g.wf_digraph_axioms) show ?thesis using assms(2) g.in_eq_out_degree by (unfold_locales) simp_all qed text \Regular graphs (non-empty) can be shown to be a constant rep design\ locale non_empty_regular_graph = regular_graph + non_empty_digraph sublocale non_empty_regular_graph \ non_empty_graph by unfold_locales sublocale non_empty_regular_graph \ constant_rep_design "verts G" "arcs_blocks" \ using arcs_blocks_ne arcs_not_empty by (unfold_locales)(simp_all add: point_replication_number_def) end \ No newline at end of file diff --git a/thys/Design_Theory/Group_Divisible_Designs.thy b/thys/Design_Theory/Group_Divisible_Designs.thy --- a/thys/Design_Theory/Group_Divisible_Designs.thy +++ b/thys/Design_Theory/Group_Divisible_Designs.thy @@ -1,1091 +1,1092 @@ (* 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 ::int) \ 2" by simp + show "(1 ::nat) \ 2" by simp show "2 \ inc.\" by (simp add: gdd_min_v) - then show "\ps. ps \ \ \ int (card ps) = 2 \ int ((\ + mset_set \) index ps) = 1" + 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 b_positive + 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 \ int (card (insert x \))" by auto + 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 \ {int (card g + 1) |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 \ {int (card g + 1) |g. g \ \}" + 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 \ \} \ - int (card bl) \ \ \ {int (card g + 1) |g. g \ \}" - using UnI1 UnI2 block_sizes union_iff by (smt (z3) mem_Collect_eq) - show "\x. x \ \ \ {int (card g + 1) |g. g \ \} \ 0 < x" + (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 \ \ \ {int (card g + 1) |g. g \ \} \ 2 \ k" + 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 "(\\<^sub># (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 "(\\<^sub># (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 "(\\<^sub># (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 "(\\<^sub># (image_mset f \)) index {(x, ix), (y, iy)} = (\B \# \. (f B) index {(x, ix), (y, iy)} )" by (simp add: points_index_sum) then have "(\\<^sub># (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 \ (\\<^sub># (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 \ ((\\<^sub># (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 \ int (card (\ - {x}))" + 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 int_ops(3) less_nat_zero_code nat_le_linear verit_comp_simplify1(3) zle_int) + 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 "({\} \ {(card g) + 1 | g . g \ \}) = {\}" - using assms(2) by fastforce + 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 assms sys_block_sizes_obtain_bl add_point_def - by (smt (verit, best) Collect_cong sys_block_sizes_uniform uniform_alt_def_all) + 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 (metis int_eq_iff_numeral of_nat_1_eq_iff) + 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 nat_leq_as_int of_nat_numeral setcompr_eq_image) + 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 pbd_points_index1) + 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 \ No newline at end of file diff --git a/thys/Design_Theory/Multisets_Extras.thy b/thys/Design_Theory/Multisets_Extras.thy --- a/thys/Design_Theory/Multisets_Extras.thy +++ b/thys/Design_Theory/Multisets_Extras.thy @@ -1,796 +1,817 @@ (* Title: Multisets_Extras Author: Chelsea Edmonds *) section \Micellanious Helper Functions on Sets and Multisets\ theory Multisets_Extras imports "HOL-Library.Multiset" Card_Partitions.Set_Partition Nested_Multisets_Ordinals.Multiset_More Nested_Multisets_Ordinals.Duplicate_Free_Multiset "HOL-Library.Disjoint_Sets" begin subsection \Set Theory Extras\ text \A number of extra helper lemmas for reasoning on sets (finite) required for Design Theory proofs\ lemma card_Pow_filter_one: assumes "finite A" shows "card {x \ Pow A . card x = 1} = card (A)" using assms proof (induct rule: finite_induct) case empty then show ?case by auto next case (insert x F) have "Pow (insert x F) = Pow F \ insert x ` Pow F" by (simp add: Pow_insert) then have split: "{y \ Pow (insert x F) . card y = 1} = {y \ (Pow F) . card y = 1} \ {y \ (insert x ` Pow F) . card y = 1}" by blast have "\ y . y \ (insert x ` Pow F) \ finite y" using finite_subset insert.hyps(1) by fastforce then have single: "\ y . y \ (insert x ` Pow F) \ card y = 1 \ y = {x}" by (metis card_1_singletonE empty_iff image_iff insertCI insertE) then have "card {y \ (insert x ` Pow F) . card y = 1} = 1" using empty_iff imageI is_singletonI is_singletonI' is_singleton_altdef (* LONG *) by (metis (full_types, lifting) Collect_empty_eq_bot Pow_bottom bot_empty_eq mem_Collect_eq) then have " {y \ (insert x ` Pow F) . card y = 1} = {{x}}" using single card_1_singletonE card_eq_0_iff by (smt empty_Collect_eq mem_Collect_eq singletonD zero_neq_one) then have split2:"{y \ Pow (insert x F) . card y = 1} = {y \ (Pow F) . card y = 1} \ {{x}}" using split by simp then show ?case proof (cases "x \ F") case True then show ?thesis using insert.hyps(2) by auto next case False then have "{y \ (Pow F) . card y = 1} \ {{x}} = {}" by blast then have fact:"card {y \ Pow (insert x F) . card y = 1} = card {y \ (Pow F) . card y = 1} + card {{x}}" using split2 card_Un_disjoint insert.hyps(1) by auto have "card (insert x F) = card F + 1" using False card_insert_disjoint by (metis Suc_eq_plus1 insert.hyps(1)) then show ?thesis using fact insert.hyps(3) by auto qed qed lemma elem_exists_non_empty_set: assumes "card A > 0" obtains x where "x \ A" using assms card_gt_0_iff by fastforce lemma set_self_img_compr: "{a | a . a \ A} = A" by blast lemma card_subset_not_gt_card: "finite A \ card ps > card A \ \ (ps \ A)" using card_mono leD by auto lemma card_inter_lt_single: "finite A \ finite B \ card (A \ B) \ card A" by (simp add: card_mono) lemma set_diff_non_empty_not_subset: assumes "A \ (B - C)" assumes "C \ {}" assumes "A \ {}" assumes "B \ {}" shows " \ (A \ C)" proof (rule ccontr) assume " \ \ (A \ C)" then have a: "\ x . x \ A \ x \ C" by blast thus False using a assms by blast qed lemma set_card_diff_ge_zero: "finite A \ finite B \ A \ B \ card A = card B \ card (A - B) > 0" by (meson Diff_eq_empty_iff card_0_eq card_subset_eq finite_Diff neq0_conv) lemma set_filter_diff: "{a \ A . P a } - {x} = {a \ (A - {x}) . (P a )}" by (auto) lemma set_filter_diff_card: "card ({a \ A . P a } - {x}) = card {a \ (A - {x}) . (P a )}" by (simp add: set_filter_diff) lemma obtain_subset_with_card_int_n: assumes "(n ::int) \ of_nat (card S)" assumes "(n ::int) \ 0" obtains T where "T \ S" "of_nat (card T) = (n ::int)" "finite T" using obtain_subset_with_card_n assms by (metis nonneg_int_cases of_nat_le_iff) lemma transform_filter_img_empty_rm: assumes "\ g . g \ G \ g \ {}" shows "{g - {x} | g. g \ G \ g \ {x}} = {g - {x} | g. g \ G } - {{}}" proof - let ?f = "\ g . g - {x}" have "\ g . g \ G \ g \ {x} \ ?f g \ {}" using assms by (metis Diff_cancel Diff_empty Diff_insert0 insert_Diff) thus ?thesis by auto qed lemma bij_betw_inter_subsets: "bij_betw f A B \ a1 \ A \ a2 \ A \ f ` (a1 \ a2) = (f ` a1) \ (f ` a2)" by (meson bij_betw_imp_inj_on inj_on_image_Int) text\Partition related set theory lemmas\ lemma partition_on_remove_pt: assumes "partition_on A G" shows "partition_on (A - {x}) {g - {x} | g. g \ G \ g \ {x}}" proof (intro partition_onI) show "\p. p \ {g - {x} |g. g \ G \ g \ {x}} \ p \ {}" using assms partition_onD3 subset_singletonD by force let ?f = "(\ g . g - {x})" have un_img: "\({?f g | g. g \ G }) = ?f (\ G)" by blast have empty: "\ {g - {x} |g. g \ G \ g \ {x}} = \({g - {x} | g. g \ G } - {{}})" by blast then have "\({g - {x} | g. g \ G } - {{}}) = \({g - {x} | g. g \ G })" by blast then show " \ {g - {x} |g. g \ G \ g \ {x}} = A - {x}" using partition_onD1 assms un_img by (metis empty) then show "\p p'. p \ {g - {x} |g. g \ G \ g \ {x}} \ p' \ {g - {x} |g. g \ G \ g \ {x}} \ p \ p' \ p \ p' = {}" proof - fix p1 p2 assume p1: "p1 \ {g - {x} |g. g \ G \ g \ {x}}" and p2: "p2 \ {g - {x} |g. g \ G \ g \ {x}}" and ne: "p1 \ p2" obtain p1' p2' where orig1: "p1 = p1' - {x}" and orig2: "p2 = p2' - {x}" and origne: "p1' \ p2'" and ne1: "p1' \ {x}" and ne2:"p2' \ {x}" and ing1: "p1' \ G" and ing2: "p2' \ G" using p1 p2 using mem_Collect_eq ne by blast then have "p1' \ p2' = {}" using assms partition_onD2 ing1 ing2 origne disjointD by blast thus "p1 \ p2 = {}" using orig1 orig2 by blast qed qed lemma partition_on_cart_prod: assumes "card I > 0" assumes "A \ {}" assumes "G \ {}" assumes "partition_on A G" shows "partition_on (A \ I) {g \ I |g. g \ G}" proof (intro partition_onI) show "\p. p \ {g \ I |g. g \ G} \ p \ {}" using assms(1) assms(4) partition_onD3 by fastforce show "\ {g \ I |g. g \ G} = A \ I" by (metis Setcompr_eq_image Sigma_Union assms(4) partition_onD1) show "\p p'. p \ {g \ I |g. g \ G} \ p' \ {g \ I |g. g \ G} \ p \ p' \ p \ p' = {}" by (smt (verit, best) Sigma_Int_distrib1 Sigma_empty1 assms(4) mem_Collect_eq partition_onE) qed subsection \Multiset Helpers\ text \Generic Size, count and card helpers\ lemma count_size_set_repr: "size {# x \# A . x = g#} = count A g" by (simp add: filter_eq_replicate_mset) lemma mset_nempty_set_nempty: "A \ {#} \ (set_mset A) \ {}" by simp lemma mset_size_ne0_set_card: "size A > 0 \ card (set_mset A) > 0" using mset_nempty_set_nempty by fastforce lemma set_count_size_min: "count A a \ n \ size A \ n" by (metis (full_types) count_le_replicate_mset_subset_eq size_mset_mono size_replicate_mset) lemma card_size_filter_eq: "finite A \ card {a \ A . P a} = size {#a \# mset_set A . P a#}" by simp +lemma size_multiset_set_mset_const_count: + assumes "card (set_mset A) = ca" + assumes "\p. p \# A \ count A p = ca2" + shows "size A = (ca * ca2)" +proof - + have "size A = (\ p \ (set_mset A) . count A p)" using size_multiset_overloaded_eq by auto + then have "size A = (\ p \ (set_mset A) . ca2)" using assms by simp + thus ?thesis using assms(1) by auto +qed + lemma size_multiset_int_count: assumes "of_nat (card (set_mset A)) = (ca :: int)" assumes "\p. p \# A \ of_nat (count A p) = (ca2 :: int)" shows "of_nat (size A) = ((ca :: int) * ca2)" proof - have "size A = (\ p \ (set_mset A) . count A p)" using size_multiset_overloaded_eq by auto then have "of_nat (size A) = (\ p \ (set_mset A) . ca2)" using assms by simp thus ?thesis using assms(1) by auto qed lemma mset_union_size: "size (A \# B) = size (A) + size (B - A)" by (simp add: union_mset_def) lemma mset_union_size_inter: "size (A \# B) = size (A) + size B - size (A \# B)" by (metis diff_add_inverse2 size_Un_Int) text \Lemmas for repeat\_mset\ lemma repeat_mset_size [simp]: "size (repeat_mset n A) = n * size A" by (induction n) auto lemma repeat_mset_subset_in: assumes "\ a . a \# A \ a \ B" assumes "X \# repeat_mset n A" assumes "x \ X" shows " x \ B" using assms by (induction n) auto lemma repeat_mset_not_empty: "n > 0 \ A \ {#} \ repeat_mset n A \ {#}" by (induction n) auto lemma elem_in_repeat_in_original: "a \# repeat_mset n A \ a \# A" by (metis count_inI count_repeat_mset in_countE mult.commute mult_zero_left nat.distinct(1)) lemma elem_in_original_in_repeat: "n > 0 \ a \# A \ a \# repeat_mset n A" by (metis count_greater_zero_iff count_repeat_mset nat_0_less_mult_iff) text \Lemmas on image and filter for multisets\ lemma multiset_add_filter_size: "size {# a \# (A1 + A2) . P a #} = size {# a \# A1 . P a #} + size {# a \# A2 . P a #}" by simp lemma size_filter_neg: "size {#a \# A . P a #} = size A - size {# a \# A . \ P a #}" using size_filter_mset_lesseq size_union union_filter_mset_complement by (metis ordered_cancel_comm_monoid_diff_class.le_imp_diff_is_add) lemma filter_filter_mset_cond_simp: assumes "\ a . P a \ Q a" shows "filter_mset P A = filter_mset P (filter_mset Q A)" proof - have "filter_mset P (filter_mset Q A) = filter_mset (\ a. Q a \ P a) A" by (simp add: filter_filter_mset) thus ?thesis using assms by (metis (mono_tags, lifting) filter_mset_cong) qed lemma filter_filter_mset_ss_member: "filter_mset (\ a . {x, y} \ a) A = filter_mset (\ a . {x, y} \ a) (filter_mset (\ a . x \ a) A)" proof - have filter: "filter_mset (\ a . {x, y} \ a) (filter_mset (\ a . x \ a) A) = filter_mset (\ a . x \ a \ {x, y} \ a) A" by (simp add: filter_filter_mset) have "\ a. {x, y} \ a \ x \ a" by simp thus ?thesis using filter by auto qed lemma multiset_image_do_nothing: "(\ x .x \# A \ f x = x) \ image_mset f A = A" by (induct A) auto lemma set_mset_filter: "set_mset {# f a . a \# A #} = {f a | a. a \# A}" by (simp add: Setcompr_eq_image) lemma mset_exists_imply: "x \# {# f a . a \# A #} \ \ y \# A . x = f y" by auto lemma filter_mset_image_mset: "filter_mset P (image_mset f A) = image_mset f (filter_mset (\x. P (f x)) A)" by (induction A) auto lemma mset_bunion_filter: "{# a \# A . P a \ Q a #} = {# a \# A . P a #} \# {# a \# A . Q a #}" by (rule multiset_eqI) simp lemma mset_inter_filter: "{# a \# A . P a \ Q a #} = {# a \# A . P a #} \# {# a \# A . Q a #}" by (rule multiset_eqI) simp lemma image_image_mset: "image_mset (\ x . f x) (image_mset (\ y . g y) A) = image_mset (\ x. f (g x)) A" by simp text \Big Union over multiset helpers\ lemma mset_big_union_obtain: assumes "x \# \\<^sub># A" obtains a where "a \# A" and "x \# a" using assms by blast lemma size_big_union_sum: "size (\\<^sub># (M :: 'a multiset multiset)) = (\x \#M . size x)" by (induct M) auto text \Cartesian Product on Multisets\ lemma size_cartesian_product_singleton [simp]: "size ({#a#} \# B) = size B" by (simp add: Times_mset_single_left) lemma size_cartesian_product_singleton_right [simp]: "size (A \# {#b#}) = size A" by (simp add: Times_mset_single_right) lemma size_cartesian_product_empty [simp]: "size (A \# {#}) = 0" by simp lemma size_add_elem_step_eq: assumes "size (A \# B) = size A * size B" shows "size (add_mset x A \# B) = size (add_mset x A) * size B" proof - have "(add_mset x A \# B) = A \# B + {#x#} \# B" by (metis Sigma_mset_plus_distrib1 add_mset_add_single) then have "size (add_mset x A \# B) = size (A \# B) + size B" by auto also have "... = size A * size B + size B" by (simp add: assms) finally have "size (add_mset x A \# B) = (size A + 1) * size B" by auto thus ?thesis by simp qed lemma size_cartesian_product: "size (A \# B) = size A * size B" by (induct A) (simp_all add: size_add_elem_step_eq) lemma cart_prod_distinct_mset: assumes assm1: "distinct_mset A" assumes assm2: "distinct_mset B" shows "distinct_mset (A \# B)" unfolding distinct_mset_count_less_1 proof (rule allI) fix x have count_mult: "count (A \# B) x = count A (fst x) * count B (snd x)" using count_Sigma_mset by (metis prod.exhaust_sel) then have "count A (fst x) * count B (snd x) \ 1" using assm1 assm2 unfolding distinct_mset_count_less_1 using mult_le_one by blast thus "count (A \# B) x \ 1" using count_mult by simp qed lemma cart_product_single_intersect: "x1 \ x2 \ ({#x1#} \# A) \# ({#x2#} \# B) = {#}" using multiset_inter_single by fastforce lemma size_union_distinct_cart_prod: "x1 \ x2 \ size (({#x1#} \# A) \# ({#x2#} \# B)) = size ({#x1#} \# A) + size ({#x2#} \# B)" by (simp add: cart_product_single_intersect size_Un_disjoint) lemma size_Union_distinct_cart_prod: "distinct_mset M \ size (\p\#M. ({#p#} \# B)) = size (M) * size (B)" by (induction M) auto lemma size_Union_distinct_cart_prod_filter: "distinct_mset M \ (\ p . p \# M \ size ({# b \# B . P p b #}) = c) \ size (\p\#M. ({#p#} \# {# b \# B . P p b #})) = size (M) * c" by (induction M) auto lemma size_Union_distinct_cart_prod_filter2: "distinct_mset V \ (\ b . b \# B \ size ({# v \# V . P v b #}) = c) \ size (\b\#B. ( {# v \# V . P v b #} \# {#b#})) = size (B) * c" by (induction B) auto lemma cart_product_add_1: "(add_mset a A) \# B = ({#a#} \# B) + (A \# B)" by (metis Sigma_mset_plus_distrib1 add_mset_add_single union_commute) lemma cart_product_add_1_filter: "{#m \# ((add_mset a M) \# N) . P m #} = {#m \# (M \# N) . P m #} + {#m \# ({#a#} \# N) . P m #}" unfolding add_mset_add_single [of a M] Sigma_mset_plus_distrib1 by (simp add: Times_mset_single_left) lemma cart_product_add_1_filter2: "{#m \# (M \# (add_mset b N)) . P m #} = {#m \# (M \# N) . P m #} + {#m \# (M \# {#b#}) . P m #}" unfolding add_mset_add_single [of b N] Sigma_mset_plus_distrib1 by (metis Times_insert_left Times_mset_single_right add_mset_add_single filter_union_mset) lemma cart_prod_singleton_right_gen: assumes "\ x . x \# (A \# {#b#}) \ P x \ Q (fst x)" shows "{#x \# (A \# {#b#}). P x#} = {# a \# A . Q a#} \# {#b#}" using assms proof (induction A) case empty then show ?case by simp next case (add x A) have "add_mset x A \# {#b#} = add_mset (x, b) (A \# {#b#})" by (simp add: Times_mset_single_right) then have lhs: "filter_mset P (add_mset x A \# {#b#}) = filter_mset P (A \# {#b#}) + filter_mset P {#(x, b)#}" by simp have rhs: "filter_mset Q (add_mset x A) \# {#b#} = filter_mset Q A \# {#b#} + filter_mset Q {#x#} \# {#b#}" by (metis Sigma_mset_plus_distrib1 add_mset_add_single filter_union_mset) have "filter_mset P {#(x, b)#} = filter_mset Q {#x#} \# {#b#}" using add.prems by fastforce then show ?case using lhs rhs add.IH add.prems by force qed lemma cart_prod_singleton_left_gen: assumes "\ x . x \# ({#a#} \# B) \ P x \ Q (snd x)" shows "{#x \# ({#a#} \# B). P x#} = {#a#} \# {#b \# B . Q b#}" using assms proof (induction B) case empty then show ?case by simp next case (add x B) have lhs: "filter_mset P ({#a#} \# add_mset x B) = filter_mset P ({#a#} \# B) + filter_mset P {#(a, x)#}" by (simp add: cart_product_add_1_filter2) have rhs: "{#a#} \# filter_mset Q (add_mset x B) = {#a#} \# filter_mset Q B + {#a#} \# filter_mset Q {#x#}" using add_mset_add_single filter_union_mset by (metis Times_mset_single_left image_mset_union) have "filter_mset P {#(a, x)#} = {#a#} \# filter_mset Q {#x#}" using add.prems by fastforce then show ?case using lhs rhs add.IH add.prems by force qed lemma cart_product_singleton_left: "{#m \# ({#a#} \# N) . fst m \ snd m #} = ({#a#} \# {# n \# N . a \ n #})" (is "?A = ?B") proof - have stmt: "\m. m \# ({#a#} \# N) \ fst m \ snd m \ a \ snd m" by (simp add: mem_Times_mset_iff) thus ?thesis by (metis (no_types, lifting) Sigma_mset_cong stmt cart_prod_singleton_left_gen) qed lemma cart_product_singleton_right: "{#m \# (N \# {#b#}) . fst m \ snd m #} = ({# n \# N . n \ b #} \# {# b #})" (is "?A = ?B") proof - have stmt: "\m. m \# (N \# {#b#}) \ fst m \ snd m \ fst m \b" by (simp add: mem_Times_mset_iff) thus ?thesis by (metis (no_types, lifting) Sigma_mset_cong stmt cart_prod_singleton_right_gen) qed lemma cart_product_add_1_filter_eq: "{#m \# ((add_mset a M) \# N) . (fst m \ snd m) #} = {#m \# (M \# N) . (fst m \ snd m) #} + ({#a#} \# {# n \# N . a \ n #})" unfolding add_mset_add_single [of a M] Sigma_mset_plus_distrib1 using cart_product_singleton_left cart_product_add_1_filter by fastforce lemma cart_product_add_1_filter_eq_mirror: "{#m \# M \# (add_mset b N) . (fst m \ snd m) #} = {#m \# (M \# N) . (fst m \ snd m) #} + ({# n \# M . n \ b #} \# {#b#})" unfolding add_mset_add_single [of b N] Sigma_mset_plus_distrib1 (* longish *) by (metis (no_types) add_mset_add_single cart_product_add_1_filter2 cart_product_singleton_right) lemma set_break_down_left: shows "{# m \# (M \# N) . (fst m) \ (snd m) #} = (\m\#M. ({#m#} \# {#n \# N. m \ n#}))" by (induction M) (auto simp add: cart_product_add_1_filter_eq) lemma set_break_down_right: shows "{# x \# M \# N . (fst x) \ (snd x) #} = (\n\#N. ({#m \# M. m \ n#} \# {#n#}))" by (induction N) (auto simp add: cart_product_add_1_filter_eq_mirror) text \Reasoning on sums of elements over multisets\ lemma sum_over_fun_eq: assumes "\ x . x \# A \ f x = g x" shows "(\x \# A . f(x)) = (\ x \# A . g (x))" using assms by auto +lemma sum_mset_add_diff_nat: + fixes x:: 'a and f g :: "'a \ nat" + assumes "\x . x \# A \ f x \ g x" + shows "(\ x \# A. f x - g x) = (\ x \# A . f x) - (\ x \# A . g x)" + using assms by (induction A) (simp_all add: sum_mset_mono) + +lemma sum_mset_add_diff_int: + fixes x:: 'a and f g :: "'a \ int" + shows "(\ x \# A. f x - g x) = (\ x \# A . f x) - (\ x \# A . g x)" + by (induction A) (simp_all add: sum_mset_mono) + context ring_1 begin lemma sum_mset_add_diff: "(\ x \# A. f x - g x) = (\ x \# A . f x) - (\ x \# A . g x)" by (induction A) (auto simp add: algebra_simps) end -context ordered_ring +context ordered_semiring begin lemma sum_mset_ge0:"(\ x . f x \ 0) \ (\ x \# A. f x ) \ 0" proof (induction A) case empty then show ?case by simp next case (add x A) then have hyp2: "0 \ sum_mset (image_mset f A)" by blast then have " sum_mset (image_mset f (add_mset x A)) = sum_mset (image_mset f A) + f x" by (simp add: add_commute) then show ?case by (simp add: add.IH add.prems) qed lemma sum_order_add_mset: "(\ x . f x \ 0) \ (\ x \# A. f x ) \ (\ x \# add_mset a A. f x )" - by simp + by (simp add: local.add_increasing) lemma sum_mset_0_left: "(\ x . f x \ 0) \ (\ x \# A. f x ) = 0 \ (\ x \# A .f x = 0)" apply (induction A) apply auto using local.add_nonneg_eq_0_iff sum_mset_ge0 apply blast using local.add_nonneg_eq_0_iff sum_mset_ge0 by blast lemma sum_mset_0_iff_ge_0: assumes "(\ x . f x \ 0)" shows "(\ x \# A. f x ) = 0 \ (\ x \ set_mset A .f x = 0)" using sum_mset_0_left assms by auto end lemma mset_set_size_card_count: "(\x \# A. x) = (\x \ set_mset A . x * (count A x))" proof (induction A) case empty then show ?case by simp next case (add y A) have lhs: "(\x\#add_mset y A. x) = (\x\# A. x) + y" by simp have rhs: "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = (\x\(insert y (set_mset A)) . x * count (add_mset y A) x)" by simp then show ?case proof (cases "y \# A") case True have x_val: "\ x . x \ (insert y (set_mset A)) \ x \ y \ x* count (add_mset y A) x = x * (count A x)" by auto have y_count: "count (add_mset y A) y = 1 + count A y" using True count_inI by fastforce then have "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = (y * (count (add_mset y A) y)) + (\x\(set_mset A) - {y}. x * count A x)" using x_val finite_set_mset sum.cong sum.insert rhs by (smt DiffD1 Diff_insert_absorb insert_absorb mk_disjoint_insert sum.insert_remove) then have s1: "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = y + y * (count A y) + (\x\(set_mset A) - {y}. x * count A x)" using y_count by simp then have "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = y + (\x\insert y ((set_mset A) - {y} ) . x * count A x)" by (simp add: sum.insert_remove) then have "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = y + (\x\(set_mset A) . x * count A x)" by (simp add: True insert_absorb) then show ?thesis using lhs add.IH by linarith next case False have x_val: "\ x . x \ set_mset A \ x* count (add_mset y A) x = x * (count A x)" using False by auto have y_count: "count (add_mset y A) y = 1" using False count_inI by fastforce have lhs: "(\x\#add_mset y A. x) = (\x\# A. x) + y" by simp have "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = (y * count (add_mset y A) y) + (\x\set_mset A. x * count A x)" using x_val rhs by (metis (no_types, lifting) False finite_set_mset sum.cong sum.insert) then have "(\x\set_mset (add_mset y A). x * count (add_mset y A) x) = y + (\x\set_mset A. x * count A x)" using y_count by simp then show ?thesis using lhs add.IH by linarith qed qed subsection \Partitions on Multisets\ text \A partition on a multiset A is a multiset of multisets, where the sum over P equals A and the empty multiset is not in the partition. Based off set partition definition. We note that unlike set partitions, there is no requirement for elements in the multisets to be distinct due to the definition of union on multisets \cite{benderPartitionsMultisets1974}\ lemma mset_size_partition_dep: "size {# a \# A . P a \ Q a #} = size {# a \# A . P a #} + size {# a \# A . Q a #} - size {# a \# A . P a \ Q a #}" by (simp add: mset_bunion_filter mset_inter_filter mset_union_size_inter) definition partition_on_mset :: "'a multiset \ 'a multiset multiset \ bool" where "partition_on_mset A P \ \\<^sub>#P = A \ {#} \# P" lemma partition_on_msetI [intro]: "\\<^sub>#P = A \ {#} \# P \ partition_on_mset A P" by (simp add: partition_on_mset_def) lemma partition_on_msetD1: "partition_on_mset A P \ \\<^sub>#P = A" by (simp add: partition_on_mset_def) lemma partition_on_msetD2: "partition_on_mset A P \ {#} \# P" by (simp add: partition_on_mset_def) lemma partition_on_mset_empty: "partition_on_mset {#} P \ P = {#}" unfolding partition_on_mset_def using multiset_nonemptyE by fastforce lemma partition_on_mset_all: "A \ {#} \ partition_on_mset A {#A #}" by (simp add: partition_on_mset_def) lemma partition_on_mset_singletons: "partition_on_mset A (image_mset (\ x . {#x#}) A)" by (auto simp: partition_on_mset_def) lemma partition_on_mset_not_empty: "A \ {#} \ partition_on_mset A P \ P \ {#}" by (auto simp: partition_on_mset_def) lemma partition_on_msetI2: "\\<^sub>#P = A \ (\ p . p \# P \ p \ {#}) \ partition_on_mset A P" by (auto simp: partition_on_mset_def) lemma partition_on_mset_elems: "partition_on_mset A P \ p1 \# P \ x \# p1 \ x \# A" by (auto simp: partition_on_mset_def) lemma partition_on_mset_sum_size_eq: "partition_on_mset A P \ (\x \# P. size x) = size A" by (metis partition_on_msetD1 size_big_union_sum) lemma partition_on_mset_card: assumes "partition_on_mset A P" shows " size P \ size A" proof (rule ccontr) assume "\ size P \ size A" then have a: "size P > size A" by simp have "\ x . x \# P \ size x > 0" using partition_on_msetD2 using assms nonempty_has_size by auto then have " (\x \# P. size x) \ size P" by (metis leI less_one not_less_zero size_eq_sum_mset sum_mset_mono) thus False using a partition_on_mset_sum_size_eq using assms by fastforce qed lemma partition_on_mset_count_eq: "partition_on_mset A P \ a \# A \ (\x \# P. count x a) = count A a" by (metis count_sum_mset partition_on_msetD1) lemma partition_on_mset_subsets: "partition_on_mset A P \ x \# P \ x \# A" by (auto simp add: partition_on_mset_def) lemma partition_on_mset_distinct: assumes "partition_on_mset A P" assumes "distinct_mset A" shows "distinct_mset P" proof (rule ccontr) assume "\ distinct_mset P" then obtain p1 where count: "count P p1 \ 2" by (metis Suc_1 distinct_mset_count_less_1 less_Suc_eq_le not_less_eq) then have cge: "\ x . x \# p1 \ (\p \# P. count p x ) \ 2" by (smt count_greater_eq_one_iff count_sum_mset_if_1_0 dual_order.trans sum_mset_mono zero_le) have elem_in: "\ x . x \# p1 \ x \# A" using partition_on_mset_elems by (metis count assms(1) count_eq_zero_iff not_numeral_le_zero) have "\ x . x \# A \ count A x = 1" using assms by (simp add: distinct_mset_def) thus False using assms partition_on_mset_count_eq cge elem_in count_inI local.count multiset_nonemptyE by (metis (mono_tags) not_numeral_le_zero numeral_One numeral_le_iff partition_on_mset_def semiring_norm(69)) qed lemma partition_on_mset_distinct_disjoint: assumes "partition_on_mset A P" assumes "distinct_mset A" assumes "p1 \# P" assumes "p2 \# P - {#p1#}" shows "p1 \# p2 = {#}" using Diff_eq_empty_iff_mset assms diff_add_zero distinct_mset_add multiset_inter_assoc sum_mset.remove by (smt partition_on_msetD1 subset_mset.inf.absorb_iff2 subset_mset.le_add_same_cancel1 subset_mset.le_iff_inf) lemma partition_on_mset_diff: assumes "partition_on_mset A P" assumes "Q \#P" shows "partition_on_mset (A - \\<^sub>#Q) (P - Q)" using assms partition_on_mset_def by (smt diff_union_cancelL subset_mset.add_diff_inverse sum_mset.union union_iff) lemma sigma_over_set_partition_count: assumes "finite A" assumes "partition_on A P" assumes "x \# \\<^sub># (mset_set (mset_set ` P))" shows "count (\\<^sub># (mset_set (mset_set ` P))) x = 1" proof - have disj: "disjoint P" using assms partition_onD2 by auto then obtain p where pin: "p \# mset_set (mset_set ` P)" and xin: "x \# p" using assms by blast then have "count (mset_set (mset_set ` P)) p = 1" by (meson count_eq_zero_iff count_mset_set') then have filter: "\ p' . p' \# ((mset_set (mset_set` P)) - {#p#}) \ p \ p'" using count_eq_zero_iff count_single by fastforce have zero: "\ p'. p' \# mset_set (mset_set ` P) \ p' \ p \ count p' x = 0" proof (rule ccontr) fix p' assume assm: "p' \# mset_set (mset_set ` P)" and ne: "p' \ p" and n0: "count p' x \ 0" then have xin2: "x \# p'" by auto obtain p1 p2 where p1in: "p1 \ P" and p2in: "p2 \ P" and p1eq: "mset_set p1 = p" and p2eq: "mset_set p2 = p'" using assm assms(1) assms(2) pin by (metis (no_types, lifting) elem_mset_set finite_elements finite_imageI image_iff) have origne: "p1 \ p2" using ne p1eq p2eq by auto have "p1 = p2" using partition_onD4 xin xin2 by (metis assms(2) count_eq_zero_iff count_mset_set' p1eq p1in p2eq p2in) then show False using origne by simp qed have one: "count p x = 1" using pin xin assms count_eq_zero_iff count_greater_eq_one_iff by (metis count_mset_set(3) count_mset_set_le_one image_iff le_antisym) then have "count (\\<^sub># (mset_set (mset_set ` P))) x = (\p' \# (mset_set (mset_set ` P)) . count p' x)" using count_sum_mset by auto also have "... = (count p x) + (\p' \# ((mset_set (mset_set ` P)) - {#p#}) . count p' x)" by (metis (mono_tags, lifting) insert_DiffM pin sum_mset.insert) also have "... = 1 + (\p' \# ((mset_set (mset_set ` P)) - {#p#}) . count p' x)" using one by presburger finally have "count (\\<^sub># (mset_set (mset_set ` P))) x = 1 + (\p' \# ((mset_set (mset_set ` P)) - {#p#}) . 0)" using zero filter by (metis (mono_tags, lifting) in_diffD sum_over_fun_eq) then show "count (\\<^sub># (mset_set (mset_set ` P))) x = 1" by simp qed lemma partition_on_mset_set: assumes "finite A" assumes "partition_on A P" shows "partition_on_mset (mset_set A) (mset_set (image (\ x. mset_set x) P))" proof (intro partition_on_msetI) have partd1: "\P = A" using assms partition_onD1 by auto have imp: "\x. x \# \\<^sub># (mset_set (mset_set ` P)) \ x \# mset_set A" proof - fix x assume "x \# \\<^sub># (mset_set (mset_set ` P))" then obtain p where "p \ (mset_set ` P)" and xin: "x \# p" by (metis elem_mset_set equals0D infinite_set_mset_mset_set mset_big_union_obtain) then have "set_mset p \ P" by (metis empty_iff finite_set_mset_mset_set image_iff infinite_set_mset_mset_set) then show "x \# mset_set A" using partd1 xin assms(1) by auto qed have imp2: "\x . x \# mset_set A \ x \# \\<^sub># (mset_set (mset_set ` P))" proof - fix x assume "x \# mset_set A" then have "x \ A" by (simp add: assms(1)) then obtain p where "p \ P" and "x \ p" using assms(2) using partd1 by blast then obtain p' where "p' \ (mset_set ` P)" and "p' = mset_set p" by blast thus "x \# \\<^sub># (mset_set (mset_set ` P))" using assms \p \ P\ \x \ p\ finite_elements partd1 by (metis Sup_upper finite_imageI finite_set_mset_mset_set in_Union_mset_iff rev_finite_subset) qed have a1: "\ x . x \# mset_set A \ count (mset_set A) x = 1" using assms(1) by fastforce then show "\\<^sub># (mset_set (mset_set ` P)) = mset_set A" using imp imp2 a1 by (metis assms(1) assms(2) count_eq_zero_iff multiset_eqI sigma_over_set_partition_count) have "\ p. p \ P \ p \ {} " using assms partition_onD3 by auto then have "\ p. p \ P \ mset_set p \ {#}" using mset_set_empty_iff by (metis Union_upper assms(1) partd1 rev_finite_subset) then show "{#} \# mset_set (mset_set ` P)" by (metis elem_mset_set equals0D image_iff infinite_set_mset_mset_set) qed lemma partition_on_mset_distinct_inter: assumes "partition_on_mset A P" assumes "distinct_mset A" assumes "p1 \# P" and "p2 \# P" and "p1 \ p2" shows "p1 \# p2 = {#}" by (metis assms in_remove1_mset_neq partition_on_mset_distinct_disjoint) lemma partition_on_set_mset_distinct: assumes "partition_on_mset A P" assumes "distinct_mset A" assumes "p \# image_mset set_mset P" assumes "p' \# image_mset set_mset P" assumes "p \ p'" shows "p \ p' = {}" proof - obtain p1 where p1in: "p1 \# P" and p1eq: "set_mset p1 = p" using assms(3) by blast obtain p2 where p2in: "p2 \# P" and p2eq: "set_mset p2 = p'" using assms(4) by blast have "distinct_mset P" using assms partition_on_mset_distinct by blast then have "p1 \ p2" using assms using p1eq p2eq by fastforce then have "p1 \# p2 = {#}" using partition_on_mset_distinct_inter using assms(1) assms(2) p1in p2in by auto thus ?thesis using p1eq p2eq by (metis set_mset_empty set_mset_inter) qed lemma partition_on_set_mset: assumes "partition_on_mset A P" assumes "distinct_mset A" shows "partition_on (set_mset A) (set_mset (image_mset set_mset P))" proof (intro partition_onI) show "\p. p \# image_mset set_mset P \ p \ {}" using assms(1) partition_on_msetD2 by fastforce next have "\ x . x \ set_mset A \ x \ \ (set_mset (image_mset set_mset P))" by (metis Union_iff assms(1) image_eqI mset_big_union_obtain partition_on_msetD1 set_image_mset) then show "\ (set_mset (image_mset set_mset P)) = set_mset A" using set_eqI' partition_on_mset_elems assms by auto show "\p p'. p \# image_mset set_mset P \ p' \# image_mset set_mset P \ p \ p' \ p \ p' = {}" using partition_on_set_mset_distinct assms by blast qed lemma partition_on_mset_eq_imp_eq_carrier: assumes "partition_on_mset A P" assumes "partition_on_mset B P" shows "A = B" using assms partition_on_msetD1 by auto lemma partition_on_mset_add_single: assumes "partition_on_mset A P" shows "partition_on_mset (add_mset a A) (add_mset {#a#} P)" using assms by (auto simp: partition_on_mset_def) lemma partition_on_mset_add_part: assumes "partition_on_mset A P" assumes "X \ {#}" assumes "A + X = A'" shows "partition_on_mset A' (add_mset X P)" using assms by (auto simp: partition_on_mset_def) lemma partition_on_mset_add: assumes "partition_on_mset A P" assumes "X \# P" assumes "add_mset a X = X'" shows "partition_on_mset (add_mset a A) (add_mset X' (P - {#X#}))" using add_mset_add_single assms empty_not_add_mset mset_subset_eq_single partition_on_mset_all by (smt partition_on_mset_def subset_mset.add_diff_inverse sum_mset.add_mset sum_mset.remove union_iff union_mset_add_mset_left) lemma partition_on_mset_elem_exists_part: assumes "partition_on_mset A P" assumes "x \# A" obtains p where "p \# P" and "x \# p" using assms in_Union_mset_iff partition_on_msetD2 partition_on_msetI by (metis partition_on_mset_eq_imp_eq_carrier) lemma partition_on_mset_combine: assumes "partition_on_mset A P" assumes "partition_on_mset B Q" shows "partition_on_mset (A + B) (P + Q)" unfolding partition_on_mset_def using assms partition_on_msetD1 partition_on_msetD2 by auto lemma partition_on_mset_split: assumes "partition_on_mset A (P + Q)" shows "partition_on_mset (\\<^sub>#P) P" using partition_on_mset_def partition_on_msetD2 assms by fastforce end \ No newline at end of file diff --git a/thys/Design_Theory/Resolvable_Designs.thy b/thys/Design_Theory/Resolvable_Designs.thy --- a/thys/Design_Theory/Resolvable_Designs.thy +++ b/thys/Design_Theory/Resolvable_Designs.thy @@ -1,204 +1,220 @@ (* Title: Resolvable_Designs.thy Author: Chelsea Edmonds *) section \Resolvable Designs\ text \Resolvable designs have further structure, and can be "resolved" into a set of resolution classes. A resolution class is a subset of blocks which exactly partitions the point set. Definitions based off the handbook \cite{colbournHandbookCombinatorialDesigns2007} and Stinson \cite{stinsonCombinatorialDesignsConstructions2004}. This theory includes a proof of an alternate statement of Bose's theorem\ theory Resolvable_Designs imports BIBD begin subsection \Resolutions and Resolution Classes\ text \A resolution class is a partition of the point set using a set of blocks from the design A resolution is a group of resolution classes partitioning the block collection\ context incidence_system begin definition resolution_class :: "'a set set \ bool" where "resolution_class S \ partition_on \ S \ (\ bl \ S . bl \# \)" lemma resolution_classI [intro]: "partition_on \ S \ (\ bl . bl \ S \ bl \# \) \ resolution_class S" by (simp add: resolution_class_def) lemma resolution_classD1: "resolution_class S \ partition_on \ S" by (simp add: resolution_class_def) lemma resolution_classD2: "resolution_class S \ bl \ S \ bl \# \" by (simp add: resolution_class_def) lemma resolution_class_empty_iff: "resolution_class {} \ \ = {}" by (auto simp add: resolution_class_def partition_on_def) lemma resolution_class_complete: "\ \ {} \ \ \# \ \ resolution_class {\}" by (auto simp add: resolution_class_def partition_on_space) lemma resolution_class_union: "resolution_class S \ \S = \ " by (simp add: resolution_class_def partition_on_def) lemma (in finite_incidence_system) resolution_class_finite: "resolution_class S \ finite S" using finite_elements finite_sets by (auto simp add: resolution_class_def) lemma (in design) resolution_class_sum_card: "resolution_class S \ (\bl \ S . card bl) = \" using resolution_class_union finite_blocks by (auto simp add: resolution_class_def partition_on_def card_Union_disjoint) definition resolution:: "'a set multiset multiset \ bool" where "resolution P \ partition_on_mset \ P \ (\ S \# P . distinct_mset S \ resolution_class (set_mset S))" lemma resolutionI : "partition_on_mset \ P \ (\ S . S \#P \ distinct_mset S) \ (\ S . S\# P \ resolution_class (set_mset S)) \ resolution P" by (simp add: resolution_def) lemma (in proper_design) resolution_blocks: "distinct_mset \ \ disjoint (set_mset \) \ \(set_mset \) = \ \ resolution {#\#}" unfolding resolution_def resolution_class_def partition_on_mset_def partition_on_def using design_blocks_nempty blocks_nempty by auto end subsection \Resolvable Design Locale\ text \A resolvable design is one with a resolution P\ locale resolvable_design = design + fixes partition :: "'a set multiset multiset" ("\

") assumes resolvable: "resolution \

" begin lemma resolutionD1: "partition_on_mset \ \

" using resolvable by (simp add: resolution_def) lemma resolutionD2: "S \#\

\ distinct_mset S" using resolvable by (simp add: resolution_def) lemma resolutionD3: " S\# \

\ resolution_class (set_mset S)" using resolvable by (simp add: resolution_def) lemma resolution_class_blocks_disjoint: "S \# \

\ disjoint (set_mset S)" using resolutionD3 by (simp add: partition_on_def resolution_class_def) lemma resolution_not_empty: "\ \ {#} \ \

\ {#}" using partition_on_mset_not_empty resolutionD1 by auto lemma resolution_blocks_subset: "S \# \

\ S \# \" using partition_on_mset_subsets resolutionD1 by auto end lemma (in incidence_system) resolvable_designI [intro]: "resolution \

\ design \ \ \ resolvable_design \ \ \

" by (simp add: resolvable_design.intro resolvable_design_axioms.intro) subsection \Resolvable Block Designs\ text \An RBIBD is a resolvable BIBD - a common subclass of interest for block designs\ locale r_block_design = resolvable_design + block_design begin lemma resolution_class_blocks_constant_size: "S \# \

\ bl \# S \ card bl = \" by (metis resolutionD3 resolution_classD2 uniform_alt_def_all) lemma resolution_class_size1: assumes "S \# \

" shows "\ = \ * size S" proof - have "(\bl \# S . card bl) = (\bl \ (set_mset S) . card bl)" using resolutionD2 assms by (simp add: sum_unfold_sum_mset) then have eqv: "(\bl \# S . card bl) = \" using resolutionD3 assms resolution_class_sum_card by presburger have "(\bl \# S . card bl) = (\bl \# S . \)" using resolution_class_blocks_constant_size assms by auto - thus ?thesis using eqv by (metis mult.commute sum_mset_constant) + thus ?thesis using eqv by auto qed lemma resolution_class_size2: assumes "S \# \

" shows "size S = \ div \" using resolution_class_size1 assms by (metis nonzero_mult_div_cancel_left not_one_le_zero k_non_zero) lemma resolvable_necessary_cond_v: "\ dvd \" proof - obtain S where s_in: "S \#\

" using resolution_not_empty design_blocks_nempty by blast then have "\ * size S = \" using resolution_class_size1 by simp thus ?thesis by (metis dvd_triv_left) qed end locale rbibd = r_block_design + bibd begin lemma resolvable_design_num_res_classes: "size \

= \" proof - have k_ne0: "\ \ 0" using k_non_zero by auto have f1: "\ = (\S \# \

. size S)" by (metis partition_on_msetD1 resolutionD1 size_big_union_sum) then have "\ = (\S \# \

. \ div \)" using resolution_class_size2 f1 by auto then have f2: "\ = (size \

) * (\ div \)" by simp then have "size \

= \ div (\ div \)" using b_non_zero by auto then have "size \

= (\ * \) div \" using f2 resolvable_necessary_cond_v by (metis div_div_div_same div_dvd_div dvd_triv_right k_ne0 nonzero_mult_div_cancel_right) thus ?thesis using necessary_condition_two by (metis nonzero_mult_div_cancel_left not_one_less_zero t_design_min_v) qed lemma resolvable_necessary_cond_b: "\ dvd \" proof - have f1: "\ = (\S \# \

. size S)" by (metis partition_on_msetD1 resolutionD1 size_big_union_sum) then have "\ = (\S \# \

. \ div \)" using resolution_class_size2 f1 by auto thus ?thesis using resolvable_design_num_res_classes by simp qed subsubsection \Bose's Inequality\ text \Boses inequality is an important theorem on RBIBD's. This is a proof of an alternate statement of the thm, which does not require a linear algebraic approach, taken directly from Stinson \cite{stinsonCombinatorialDesignsConstructions2004}\ theorem bose_inequality_alternate: "\ \ \ + \ - 1 \ \ \ \ + \" proof - - have kdvd: "\ dvd (\ * (\ - \))" - using necessary_condition_two by (simp add: right_diff_distrib') - have v_eq: "\ = (\ * (\ - 1) + \ ) div \" - using necessary_condition_one index_not_zero by auto - have ldvd: " \ x. \ dvd (x * (\ * (\ - 1) + \))" - using necessary_condition_one by auto - have "(\ \ \ + \ - 1) \ ((\ * \) div \ \ \ + \ - 1)" - using necessary_condition_two k_non_zero by auto - also have "... \ (((\ * \) - (\ * \)) div \ \ \ - 1)" - using k_non_zero div_mult_self3 k_non_zero necessary_condition_two by auto - also have f2: " ... \ ((\ * ( \ - \)) \ \ * ( \ - 1))" - using k_non_zero kdvd by (auto simp add: int_distrib(3) mult_of_nat_commute) - also have "... \ ((((\ * (\ - 1) + \ ) div \) * (\ - \)) \ \ * (\ - 1))" + define k b v l r where intdefs: "k \ (int \)" "b \ int \" "v = int \" "l \ int \" "r \ int \" + have kdvd: "k dvd (v * (r - k))" + using intdefs + by (simp add: resolvable_necessary_cond_v) + have necess1_alt: "l * v - l = r * (k - 1)" using necessary_condition_one intdefs + by (smt (verit) diff_diff_cancel int_ops(2) int_ops(6) k_non_zero nat_mult_1_right of_nat_0_less_iff + of_nat_mult right_diff_distrib' v_non_zero) + then have v_eq: "v = (r * (k - 1) + l) div l" + using necessary_condition_one index_not_zero intdefs + by (metis diff_add_cancel nonzero_mult_div_cancel_left not_one_le_zero of_nat_mult + unique_euclidean_semiring_with_nat_class.of_nat_div) + have ldvd: " \ x. l dvd (x * (r * (k - 1) + l))" + by (metis necess1_alt diff_add_cancel dvd_mult dvd_triv_left) + have "(b \ v + r - 1) \ ((\ * r) div k \ v + r - 1)" + using necessary_condition_two k_non_zero intdefs + by (metis (no_types, lifting) nonzero_mult_div_cancel_right not_one_le_zero of_nat_eq_0_iff of_nat_mult) + also have "... \ (((v * r) - (v * k)) div k \ r - 1)" + using k_non_zero div_mult_self3 k_non_zero necessary_condition_two intdefs + by (smt (verit, ccfv_SIG) Euclidean_Division.div_eq_0_iff b_non_zero bibd_block_number mult_is_0 of_nat_eq_0_iff) + also have f2: " ... \ ((v * ( r - k)) div k \ ( r - 1))" + using int_distrib(3) by (simp add: mult.commute) + also have f2: " ... \ ((v * ( r - k)) \ k * ( r - 1))" + using k_non_zero kdvd intdefs by auto + also have "... \ ((((r * (k - 1) + l ) div l) * (r - k)) \ k * (r - 1))" using v_eq by presburger - also have "... \ ( (\ - \) * ((\ * (\ - 1) + \ ) div \) \ (\ * (\ - 1)))" + also have "... \ ( (r - k) * ((r * (k - 1) + l ) div l) \ (k * (r - 1)))" by (simp add: mult.commute) - also have " ... \ ( ((\ - \) * (\ * (\ - 1) + \ )) div \ \ (\ * (\ - 1)))" - by (metis div_mult_swap dvd_add_triv_right_iff dvd_triv_left necessary_condition_one) - also have " ... \ (((\ - \) * (\ * (\ - 1) + \ )) \ \ * (\ * (\ - 1)))" - using ldvd by (smt dvd_mult_div_cancel index_not_zero mult_strict_left_mono) - also have "... \ (((\ - \) * (\ * (\ - 1))) + ((\ - \) * \ ) \ \ * (\ * (\ - 1)))" + also have " ... \ ( ((r - k) * (r * (k - 1) + l )) div l \ (k * (r - 1)))" + using div_mult_swap necessary_condition_one intdefs + by (metis diff_add_cancel dvd_triv_left necess1_alt) + also have " ... \ (((r - k) * (r * (k - 1) + l )) \ l * (k * (r - 1)))" + using ldvd[of "(r - k)"] dvd_mult_div_cancel index_not_zero mult_strict_left_mono intdefs + by (smt (verit) b_non_zero bibd_block_number bot_nat_0.extremum_strict div_0 less_eq_nat.simps(1) +mult_eq_0_iff mult_left_le_imp_le mult_left_mono of_nat_0 of_nat_le_0_iff of_nat_le_iff of_nat_less_iff) + also have 1: "... \ (((r - k) * (r * (k - 1))) + ((r - k) * l ) \ l * (k * (r - 1)))" by (simp add: distrib_left) - also have "... \ (((\ - \) * \ * (\ - 1)) \ \ * \ * (\ - 1) - ((\ - \) * \ ))" + also have "... \ (((r - k) * r * (k - 1)) \ l * k * (r - 1) - ((r - k) * l ))" using mult.assoc by linarith - also have "... \ (((\ - \) * \ * (\ - 1)) \ (\ * \ * \) - (\ * \) - ((\ * \) -(\ * \ )))" + also have "... \ (((r - k) * r * (k - 1)) \ (l * k * r) - (l * k) - ((r * l) -(k * l )))" using distrib_right by (simp add: distrib_left right_diff_distrib' left_diff_distrib') - also have "... \ (((\ - \) * \ * (\ - 1)) \ (\ * \ * \) - ( \ * \))" + also have "... \ (((r - k) * r * (k - 1)) \ (l * k * r) - ( l * r))" by (simp add: mult.commute) - also have "... \ (((\ - \) * \ * (\ - 1)) \ (\ * (\ * \)) - ( \ * \))" + also have "... \ (((r - k) * r * (k - 1)) \ (l * (k * r)) - ( l * r))" by linarith - also have "... \ (((\ - \) * \ * (\ - 1)) \ (\ * (\ * \)) - ( \ * \))" + also have "... \ (((r - k) * r * (k - 1)) \ (l * (r * k)) - ( l * r))" by (simp add: mult.commute) - also have "... \ (((\ - \) * \ * (\ - 1)) \ \ * \ * ( \ - 1))" + also have "... \ (((r - k) * r * (k - 1)) \ l * r * (k - 1))" by (simp add: mult.assoc int_distrib(4)) - finally have "(\ \ \ + \ - 1) \ (\ \ \ + \)" - using index_lt_replication mult_right_le_imp_le r_gzero - by (smt mult_cancel_right k_non_zero) + finally have "(b \ v + r - 1) \ (r \ k + l)" + using index_lt_replication mult_right_le_imp_le r_gzero mult_cancel_right k_non_zero intdefs + by (smt (z3) of_nat_0_less_iff of_nat_1 of_nat_le_iff of_nat_less_iff) + then have "\ \ \ + \ - 1 \ \ \ \ + \" + using k_non_zero le_add_diff_inverse of_nat_1 of_nat_le_iff intdefs by linarith thus ?thesis by simp qed end end \ No newline at end of file