(* author: R. Thiemann *) section ‹Sunflowers› text ‹Sunflowers are sets of sets, such that whenever an element is contained in at least two of the sets, then it is contained in all of the sets.› theory Sunflower imports Main "HOL-Library.FuncSet" begin definition sunflower :: "'a set set ⇒ bool" where "sunflower S = (∀ x. (∃ A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧ x ∈ A ∧ x ∈ B) ⟶ (∀ A. A ∈ S ⟶ x ∈ A))" lemma sunflower_subset: "F ⊆ G ⟹ sunflower G ⟹ sunflower F" unfolding sunflower_def by blast lemma pairwise_disjnt_imp_sunflower: "pairwise disjnt F ⟹ sunflower F" unfolding sunflower_def by (metis disjnt_insert1 mk_disjoint_insert pairwiseD) lemma card2_sunflower: assumes "finite S" and "card S ≤ 2" shows "sunflower S" proof - from assms have "card S = 0 ∨ card S = Suc 0 ∨ card S = 2" by linarith with ‹finite S› obtain A B where "S = {} ∨ S = {A} ∨ S = {A,B}" using card_2_iff[of S] card_1_singleton_iff[of S] by auto thus ?thesis unfolding sunflower_def by auto qed lemma empty_sunflower: "sunflower {}" by (rule card2_sunflower, auto) lemma singleton_sunflower: "sunflower {A}" by (rule card2_sunflower, auto) lemma doubleton_sunflower: "sunflower {A,B}" by (rule card2_sunflower, auto, cases "A = B", auto) lemma sunflower_imp_union_intersect_unique: assumes "sunflower S" and "x ∈ (⋃ S) - (⋂ S)" shows "∃! A. A ∈ S ∧ x ∈ A" proof - from assms obtain A where A: "A ∈ S" "x ∈ A" by auto show ?thesis proof show "A ∈ S ∧ x ∈ A" using A by auto fix B assume B: "B ∈ S ∧ x ∈ B" show "B = A" proof (rule ccontr) assume "B ≠ A" with A B have "∃A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧ x ∈ A ∧ x ∈ B" by auto from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this] have "x ∈ ⋂ S" by auto with assms show False by auto qed qed qed lemma union_intersect_unique_imp_sunflower: assumes "⋀ x. x ∈ (⋃ S) - (⋂ S) ⟹ ∃⇩_{≤}⇩_{1}A. A ∈ S ∧ x ∈ A" shows "sunflower S" unfolding sunflower_def proof (intro allI impI, elim exE conjE, goal_cases) case (1 x C A B) hence x: "x ∈ ⋃ S" by auto show ?case proof (cases "x ∈ ⋂ S") case False with assms[of x] x have "∃⇩_{≤}⇩_{1}A. A ∈ S ∧ x ∈ A" by blast with 1 have False unfolding Uniq_def by blast thus ?thesis .. next case True with 1 show ?thesis by blast qed qed lemma sunflower_iff_union_intersect_unique: "sunflower S ⟷ (∀ x ∈ ⋃ S - ⋂ S. ∃! A. A ∈ S ∧ x ∈ A)" (is "?l = ?r") proof assume ?l from sunflower_imp_union_intersect_unique[OF this] show ?r by auto next assume ?r hence *: "∀x∈⋃ S - ⋂ S. ∃⇩_{≤}⇩_{1}A. A ∈ S ∧ x ∈ A" unfolding ex1_iff_ex_Uniq by auto show ?l by (rule union_intersect_unique_imp_sunflower, insert *, auto) qed lemma sunflower_iff_intersect_Uniq: "sunflower S ⟷ (∀ x. x ∈ ⋂ S ∨ (∃⇩_{≤}⇩_{1}A. A ∈ S ∧ x ∈ A))" (is "?l = ?r") proof assume ?l from sunflower_imp_union_intersect_unique[OF this] show ?r unfolding ex1_iff_ex_Uniq by (metis (no_types, lifting) DiffI UnionI Uniq_I) next assume ?r show ?l by (rule union_intersect_unique_imp_sunflower, insert ‹?r›, auto) qed text ‹If there exists sunflowers whenever all elements are sets of the same cardinality @{term r}, then there also exists sunflowers whenever all elements are sets with cardinality at most @{term r}.› lemma sunflower_card_subset_lift: fixes F :: "'a set set" assumes sunflower: "⋀ G :: ('a + nat) set set. (∀ A ∈ G. finite A ∧ card A = k) ⟹ card G > c ⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r" and kF: "∀ A ∈ F. finite A ∧ card A ≤ k" and cardF: "card F > c" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r" proof - let ?n = "Suc c" from cardF have "card F ≥ ?n" by auto then obtain FF where sub: "FF ⊆ F" and cardF: "card FF = ?n" by (rule obtain_subset_with_card_n) let ?N = "{0 ..< ?n}" from cardF have "finite FF" by (simp add: card_ge_0_finite) from ex_bij_betw_nat_finite[OF this, unfolded cardF] obtain f where f: "bij_betw f ?N FF" by auto hence injf: "inj_on f ?N" by (rule bij_betw_imp_inj_on) have Ff: "FF = f ` ?N" by (metis bij_betw_imp_surj_on f) define g where "g = (λ i. (Inl ` f i) ∪ (Inr ` {0 ..< (k - card (f i))}))" have injg: "inj_on g ?N" unfolding g_def using f proof (intro inj_onI, goal_cases) case (1 x y) hence "f x = f y" by auto with injf 1 show "x = y" by (meson inj_onD) qed hence cardgN: "card (g ` ?N) > c" by (simp add: card_image) { fix i assume "i ∈ ?N" hence "f i ∈ FF" unfolding Ff by auto with sub have "f i ∈ F" by auto hence "card (f i) ≤ k" "finite (f i)" using kF by auto hence "card (g i) = k ∧ finite (g i)" unfolding g_def by (subst card_Un_disjoint, auto, subst (1 2) card_image, auto intro: inj_onI) } hence "∀ A ∈ g ` ?N. finite A ∧ card A = k" by auto from sunflower[OF this cardgN] obtain S where SgN: "S ⊆ g ` ?N" and sf: "sunflower S" and card: "card S = r" by auto from SgN obtain N where NN: "N ⊆ ?N" and SgN: "S = g ` N" by (meson subset_image_iff) from injg NN have inj_g: "inj_on g N" by (rule inj_on_subset) from injf NN have inj_f: "inj_on f N" by (rule inj_on_subset) from card_image[OF inj_g] SgN card have cardN: "card N = r" by auto let ?S = "f ` N" show ?thesis proof (intro exI[of _ ?S] conjI) from NN show "?S ⊆ F" using Ff sub by auto from card_image[OF inj_f] cardN show "card ?S = r" by auto show "sunflower ?S" unfolding sunflower_def proof (intro allI impI, elim exE conjE, goal_cases) case (1 x C A B) from ‹A ∈ f ` N› obtain i where i: "i ∈ N" and A: "A = f i" by auto from ‹B ∈ f ` N› obtain j where j: "j ∈ N" and B: "B = f j" by auto from ‹C ∈ f ` N› obtain k where k: "k ∈ N" and C: "C = f k" by auto hence gk: "g k ∈ g ` N" by auto from ‹A ≠ B› A B have ij: "i ≠ j" by auto from inj_g ij i j have gij: "g i ≠ g j" by (metis inj_on_contraD) from ‹x ∈ A› have memi: "Inl x ∈ g i" unfolding A g_def by auto from ‹x ∈ B› have memj: "Inl x ∈ g j" unfolding B g_def by auto have "∃A B. A ∈ g ` N ∧ B ∈ g ` N ∧ A ≠ B ∧ Inl x ∈ A ∧ Inl x ∈ B" using memi memj gij i j by auto from sf[unfolded sunflower_def SgN, rule_format, OF this gk] have "Inl x ∈ g k" . thus "x ∈ C" unfolding C g_def by auto qed qed qed text ‹We provide another sunflower lifting lemma that ensures non-empty cores. Here, all elements must be taken from a finite set, and the bound is multiplied the cardinality.› lemma sunflower_card_core_lift: assumes finE: "finite (E :: 'a set)" and sunflower: "⋀ G :: 'a set set. (∀ A ∈ G. finite A ∧ card A ≤ k) ⟹ card G > c ⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r" and F: "∀ A ∈ F. A ⊆ E ∧ s ≤ card A ∧ card A ≤ k" and cardF: "card F > (card E choose s) * c" and s: "s ≠ 0" and r: "r ≠ 0" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ card (⋂ S) ≥ s" proof - let ?g = "λ (A :: 'a set) x. card x = s ∧ x ⊆ A" let ?E = "{X. X ⊆ E ∧ card X = s}" from cardF have finF: "finite F" by (metis card.infinite le_0_eq less_le) from cardF have FnE: "F ≠ {}" by force { from FnE obtain B where B: "B ∈ F" by auto with F[rule_format, OF B] obtain A where "A ⊆ E" "card A = s" by (meson obtain_subset_with_card_n order_trans) hence "?E ≠ {}" using B by auto } note EnE = this define f where "f = (λ A. SOME x. ?g A x)" from finE have finiteE: "finite ?E" by simp have "f ∈ F → ?E" proof fix B assume B: "B ∈ F" with F[rule_format, OF B] have "∃ x. ?g B x" by (meson obtain_subset_with_card_n) from someI_ex[OF this] B F show "f B ∈ ?E" unfolding f_def by auto qed from pigeonhole_card[OF this finF finiteE EnE] obtain a where a: "a ∈ ?E" and le: "card F ≤ card (f -` {a} ∩ F) * card ?E" by auto have precond: "∀A∈f -` {a} ∩ F. finite A ∧ card A ≤ k" using F finite_subset[OF _ finE] by auto have "c * (card E choose s) = (card E choose s) * c" by simp also have "… < card F" by fact also have "… ≤ (card (f -` {a} ∩ F)) * card ?E" by fact also have "card ?E = card E choose s" by (rule n_subsets[OF finE]) finally have "c < card (f -` {a} ∩ F)" by auto from sunflower[OF precond this] obtain S where *: "S ⊆ f -` {a} ∩ F" "sunflower S" "card S = r" by auto from finite_subset[OF _ finF, of S] have finS: "finite S" using * by auto from * r have SnE: "S ≠ {}" by auto have finIS: "finite (⋂ S)" proof (rule finite_Inter) from SnE obtain A where A: "A ∈ S" by auto with F s have "finite A" using * precond by blast thus "∃A∈S. finite A" using A by auto qed show ?thesis proof (intro exI[of _ S] conjI *) show "S ⊆ F" using * by auto { fix A assume "A ∈ S" with *(1) have "A ∈ f -` {a}" and A: "A ∈ F" using * by auto from this have **: "f A = a" "A ∈ F" by auto from F[rule_format, OF A] have "∃x. card x = s ∧ x ⊆ A" by (meson obtain_subset_with_card_n order_trans) from someI_ex[of "?g A", OF this] ** have "a ⊆ A" unfolding f_def by auto } hence "a ⊆ ⋂ S" by auto from card_mono[OF finIS this] have "card a ≤ card (⋂ S)" . with a show "s ≤ card (⋂ S)" by auto qed qed lemma sunflower_nonempty_core_lift: assumes finE: "finite (E :: 'a set)" and sunflower: "⋀ G :: 'a set set. (∀ A ∈ G. finite A ∧ card A ≤ k) ⟹ card G > c ⟹ ∃ S. S ⊆ G ∧ sunflower S ∧ card S = r" and F: "∀ A ∈ F. A ⊆ E ∧ card A ≤ k" and empty: "{} ∉ F" and cardF: "card F > card E * c" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ (⋂ S) ≠ {}" proof (cases "r = 0") case False from F empty have F': "∀A∈F. A ⊆ E ∧ 1 ≤ card A ∧ card A ≤ k " using finE by (metis One_nat_def Suc_leI card_gt_0_iff finite_subset) from cardF have cardF': "(card E choose 1) * c < card F" by auto from sunflower_card_core_lift[OF finE sunflower, of k c F 1, OF _ _ F' cardF' _ False] obtain S where "S ⊆ F" and main: "sunflower S" "card S = r" "1 ≤ card (⋂ S)" by auto thus ?thesis by (intro exI[of _ S], auto) next case True thus ?thesis by (intro exI[of _ "{}"], auto simp: empty_sunflower) qed end