# Theory Sunflower

(* 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

# Theory Erdos_Rado_Sunflower

(* author: R. Thiemann *) section ‹The Sunflower Lemma› text ‹We formalize the proof of the sunflower lemma of Erdős and Rado~\cite{erdos_rado}, as it is presented in the textbook~\cite[Chapter~6]{book}. We further integrate Exercise 6.2 from the textbook, which provides a lower bound on the existence of sunflowers.› theory Erdos_Rado_Sunflower imports Sunflower begin text ‹When removing an element from all subsets, then one can afterwards add these elements to a sunflower and get a new sunflower.› lemma sunflower_remove_element_lift: assumes S: "S ⊆ { A - {a} | A . A ∈ F ∧ a ∈ A}" and sf: "sunflower S" shows "∃ Sa. sunflower Sa ∧ Sa ⊆ F ∧ card Sa = card S ∧ Sa = insert a ` S" proof (intro exI[of _ "insert a ` S"] conjI refl) let ?Sa = "insert a ` S" { fix B assume "B ∈ ?Sa" then obtain C where C: "C ∈ S" and B: "B = insert a C" by auto from C S obtain T where "T ∈ F" "a ∈ T" "C = T - {a}" by auto with B have "B = T" by auto with ‹T ∈ F› have "B ∈ F" by auto } thus SaF: "?Sa ⊆ F" by auto have inj: "inj_on (insert a) S" using S by (intro inj_on_inverseI[of _ "λ B. B - {a}"], auto) thus "card ?Sa = card S" by (rule card_image) show "sunflower ?Sa" unfolding sunflower_def proof (intro allI, intro impI) fix x assume "∃C D. C ∈ ?Sa ∧ D ∈ ?Sa ∧ C ≠ D ∧ x ∈ C ∧ x ∈ D" then obtain C D where *: "C ∈ ?Sa" "D ∈ ?Sa" "C ≠ D" "x ∈ C" "x ∈ D" by auto from *(1-2) obtain C' D' where **: "C' ∈ S" "D' ∈ S" "C = insert a C'" "D = insert a D'" by auto with ‹C ≠ D› inj have CD': "C' ≠ D'" by auto show "∀E. E ∈ ?Sa ⟶ x ∈ E" proof (cases "x = a") case False with * ** have "x ∈ C'" "x ∈ D'" by auto with ** CD' have "∃C D. C ∈ S ∧ D ∈ S ∧ C ≠ D ∧ x ∈ C ∧ x ∈ D" by auto from sf[unfolded sunflower_def, rule_format, OF this] show ?thesis by auto qed auto qed qed text ‹The sunflower-lemma of Erdős and Rado: if a set has a certain size and all elements have the same cardinality, then a sunflower exists.› lemma Erdos_Rado_sunflower_same_card: assumes "∀ A ∈ F. finite A ∧ card A = k" and "card F > (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ {} ∉ S" using assms proof (induct k arbitrary: F) case 0 hence "F = {{}} ∨ F = {}" "card F ≥ 2" by auto hence False by auto thus ?case by simp next case (Suc k F) define pd_sub :: "'a set set ⇒ nat ⇒ bool" where "pd_sub = (λ G t. G ⊆ F ∧ card G = t ∧ pairwise disjnt G ∧ {} ∉ G)" show ?case proof (cases "∃ t G. pd_sub G t ∧ t ≥ r") case True then obtain t G where pd_sub: "pd_sub G t" and t: "t ≥ r" by auto from pd_sub[unfolded pd_sub_def] pairwise_disjnt_imp_sunflower have *: "G ⊆ F" "card G = t" "sunflower G" "{} ∉ G" by auto from t ‹card G = t› obtain H where "H ⊆ G" "card H = r" by (metis obtain_subset_with_card_n) with sunflower_subset[OF ‹H ⊆ G›] * show ?thesis by blast next case False define P where "P = (λ t. ∃ G. pd_sub G t)" have ex: "∃ t. P t" unfolding P_def by (intro exI[of _ 0] exI[of _ "{}"], auto simp: pd_sub_def) have large': "⋀ t. P t ⟹ t < r" using False unfolding P_def by auto hence large: "⋀ t. P t ⟹ t ≤ r" by fastforce define t where "t = (GREATEST t. P t)" from GreatestI_ex_nat[OF ex large, folded t_def] have Pt: "P t" . from Greatest_le_nat[of P, OF _ large] have greatest: "⋀ s. P s ⟹ s ≤ t" unfolding t_def by auto from large'[OF Pt] have tr: "t ≤ r - 1" by simp from Pt[unfolded P_def pd_sub_def] obtain G where cardG: "card G = t" and disj: "pairwise disjnt G" and GF: "G ⊆ F" by blast define A where "A = (⋃ G)" from Suc(3) have "card F > 0" by simp hence "finite F" by (rule card_ge_0_finite) from GF ‹finite F› have finG: "finite G" by (rule finite_subset) have "card (⋃ G) ≤ sum card G" by (rule card_Union_le_sum_card, insert Suc(2) GF, auto) also have "… ≤ of_nat (card G) * Suc k" by (rule sum_bounded_above, insert GF Suc(2), auto) also have "… ≤ (r - 1) * Suc k" using tr[folded cardG] by (metis id_apply mult_le_mono1 of_nat_eq_id) finally have cardA: "card A ≤ (r - 1) * Suc k" unfolding A_def . { fix B assume *: "B ∈ F" with Suc(2) have nE: "B ≠ {}" by auto from Suc(2) have eF: "{} ∉ F" by auto have "B ∩ A ≠ {}" proof assume dis: "B ∩ A = {}" hence disj: "pairwise disjnt ({B} ∪ G)" using disj unfolding A_def by (smt (verit, ccfv_SIG) Int_commute Un_iff Union_disjoint disjnt_def pairwise_def singleton_iff) from nE dis have "B ∉ G" unfolding A_def by auto with finG have c: "card ({B} ∪ G) = Suc t" by (simp add: cardG) have "P (Suc t)" unfolding P_def pd_sub_def by (intro exI[of _ "{B} ∪ G"], insert eF disj c * GF, auto) with greatest show False by force qed } note overlap = this have "F ≠ {}" using Suc(2-) by auto with overlap have Ane: "A ≠ {}" unfolding A_def by auto have "finite A" unfolding A_def using finG Suc(2-) GF by auto let ?g = "λ B x. x ∈ B ∩ A" define f where "f = (λ B. SOME x. ?g B x)" have "f ∈ F → A" proof fix B assume "B ∈ F" from overlap[OF this] have "∃ x. ?g B x" unfolding A_def by auto from someI_ex[OF this] show "f B ∈ A" unfolding f_def by auto qed from pigeonhole_card[OF this ‹finite F› ‹finite A› Ane] obtain a where a: "a ∈ A" and le: "card F ≤ card (f -` {a} ∩ F) * card A" by auto { fix S assume "S ∈ F" "f S ∈ {a}" with someI_ex[of "?g S"] a overlap[OF this(1)] have "a ∈ S" unfolding f_def by auto } note FaS = this let ?F = "{S - {a} | S . S ∈ F ∧ f S ∈ {a}}" from cardA have "((r - 1) ^ k * fact k) * card A ≤ ((r - 1) ^ k * fact k) * ((r - 1) * Suc k)" by simp also have "… = (r - 1) ^ (Suc k) * fact (Suc k)" by (metis (no_types, lifting) fact_Suc mult.assoc mult.commute of_nat_id power_Suc2) also have "… < card (f -` {a} ∩ F) * card A" using Suc(3) le by auto also have "f -` {a} ∩ F = {S ∈ F. f S ∈ {a}}" by auto also have "card … = card ((λ S. S - {a}) ` {S ∈ F. f S ∈ {a}})" by (subst card_image; intro inj_onI refl, insert FaS) auto also have "(λ S. S - {a}) ` {S ∈ F. f S ∈ {a}} = ?F" by auto finally have lt: "(r - 1) ^ k * fact k < card ?F" by simp have "∀ A ∈ ?F. finite A ∧ card A = k" using Suc(2) FaS by auto from Suc(1)[OF this lt] obtain S where "sunflower S" "card S = r" "S ⊆ ?F" by auto from ‹S ⊆ ?F› FaS have "S ⊆ {A - {a} |A. A ∈ F ∧ a ∈ A}" by auto from sunflower_remove_element_lift[OF this ‹sunflower S›] ‹card S = r› show ?thesis by auto qed qed text ‹Using @{thm [source] sunflower_card_subset_lift} we can easily replace the condition that the cardinality is exactly @{term k} by the requirement that the cardinality is at most @{term k}. However, then @{term "{} ∉ S"} cannot be ensured. Consider @{term "(r :: nat) = 1 ∧ (k :: nat) > 0 ∧ F = {{}}"}.› lemma Erdos_Rado_sunflower: assumes "∀ A ∈ F. finite A ∧ card A ≤ k" and "card F > (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r" by (rule sunflower_card_subset_lift[OF _ assms], metis Erdos_Rado_sunflower_same_card) text ‹We further provide a lower bound on the existence of sunflowers, i.e., Exercise 6.2 of the textbook~\cite{book}. To be more precise, we prove that there is a set of sets of cardinality @{term ‹(r - 1 :: nat)^k›}, where each element is a set of cardinality @{term k}, such that there is no subset which is a sunflower with cardinality of at least @{term r}.› lemma sunflower_lower_bound: assumes inf: "infinite (UNIV :: 'a set)" and r: "r ≠ 0" and rk: "r = 1 ⟹ k ≠ 0" shows "∃ F. card F = (r - 1)^k ∧ finite F ∧ (∀ A ∈ F. finite (A :: 'a set) ∧ card A = k) ∧ (∄ S. S ⊆ F ∧ sunflower S ∧ card S ≥ r)" proof (cases "r = 1") case False with r have r: "r > 1" by auto show ?thesis proof (induct k) case 0 have id: "S ⊆ {{}} ⟷ (S = {} ∨ S = {{}})" for S :: "'a set set" by auto show ?case using r by (intro exI[of _ "{{}}"], auto simp: id) next case (Suc k) then obtain F where cardF: "card F = (r - 1) ^ k" and fin: "finite F" and AF: "⋀ A. (A :: 'a set) ∈ F ⟹ finite A ∧ card A = k" and sf: "¬ (∃S⊆F. sunflower S ∧ r ≤ card S)" by metis text ‹main idea: get @{term "k-1 :: nat"} fresh elements and add one of these to all elements of F› have "finite (⋃ F)" using fin AF by simp hence "infinite (UNIV - ⋃ F)" using inf by simp from infinite_arbitrarily_large[OF this, of "r - 1"] obtain New where New: "finite New" "card New = r - 1" "New ∩ ⋃ F = {}" by auto define G where "G = (λ (A, a). insert a A) ` (F × New)" show ?case proof (intro exI[of _ G] conjI) show "finite G" using New fin unfolding G_def by simp have "card G = card (F × New)" unfolding G_def proof ((subst card_image; (intro refl)?), intro inj_onI, clarsimp, goal_cases) case (1 A a B b) hence ab: "a = b" using New by auto from 1(1) have "insert a A - {a} = insert b B - {a}" by simp also have "insert a A - {a} = A" using New 1 by auto also have "insert b B - {a} = B" using New 1 ab[symmetric] by auto finally show ?case using ab by auto qed also have "… = card F * card New" using New fin by auto finally show "card G = (r - 1) ^ Suc k" unfolding cardF New by simp { fix B assume "B ∈ G" then obtain a A where G: "a ∈ New" "A ∈ F" "B = insert a A" unfolding G_def by auto with AF[of A] New have "finite B" "card B = Suc k" by (auto simp: card_insert_if) } thus "∀A∈G. finite A ∧ card A = Suc k" by auto show "¬ (∃S⊆G. sunflower S ∧ r ≤ card S)" proof (intro notI, elim exE conjE) fix S assume *: "S ⊆ G" "sunflower S" "r ≤ card S" define g where "g B = (SOME a. a ∈ New ∧ a ∈ B)" for B { fix B assume "B ∈ S" with ‹S ⊆ G› have "B ∈ G" by auto hence "∃ a. a ∈ New ∧ a ∈ B" unfolding G_def by auto from someI_ex[OF this, folded g_def] have "g B ∈ New" "g B ∈ B" by auto } note gB = this have "card (g ` S) ≤ card New" by (rule card_mono, insert New gB, auto) also have "… < r" unfolding New using r by simp also have "… ≤ card S" by fact finally have "card (g ` S) < card S" . from pigeonhole[OF this] have "¬ inj_on g S" . then obtain B1 B2 where B12: "B1 ∈ S" "B2 ∈ S" "B1 ≠ B2" "g B1 = g B2" unfolding inj_on_def by auto define a where "a = g B2" from B12 gB[of B1] gB[of B2] have a: "a ∈ New" "a ∈ B1" "a ∈ B2" unfolding a_def by auto with B12 have "∃B1 B2. B1 ∈ S ∧ B2 ∈ S ∧ B1 ≠ B2 ∧ a ∈ B1 ∧ a ∈ B2" unfolding a_def by blast from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this] have aS: "B ∈ S ⟹ a ∈ B" for B by auto define h where "h B = B - {a}" for B define T where "T = h ` S" have "∃S⊆F. sunflower S ∧ r ≤ card S" proof (intro exI[of _ T] conjI) { fix B assume "B ∈ S" have hB: "h B = B - {a}" unfolding h_def T_def by auto from aS ‹B ∈ S› have aB: "a ∈ B" by auto from ‹B ∈ S› ‹S ⊆ G› obtain a' A where AF: "A ∈ F" and B: "B = insert a' A" and a': "a' ∈ New" unfolding G_def by force from aB B a' New AF a(1) hB AF have "insert a (h B) = B" "h B = A" by auto hence "insert a (h B) = B" "h B ∈ F" "insert a (h B) ∈ S" using AF ‹B ∈ S› by auto } note main = this have CTS: "C ∈ T ⟹ insert a C ∈ S" for C using main unfolding T_def by force show "T ⊆ F" unfolding T_def using main by auto have "r ≤ card S" by fact also have "… = card T" unfolding T_def by (subst card_image, intro inj_on_inverseI[of _ "insert a"], insert main, auto) finally show "r ≤ card T" . show "sunflower T" unfolding sunflower_def proof (intro allI impI, elim exE conjE, goal_cases) case (1 x C C1 C2) from CTS[OF ‹C1 ∈ T›] CTS[OF ‹C2 ∈ T›] CTS[OF ‹C ∈ T›] have *: "insert a C1 ∈ S" "insert a C2 ∈ S" "insert a C ∈ S" by auto from 1 have "insert a C1 ≠ insert a C2" using main unfolding T_def by auto hence "∃A B. A ∈ S ∧ B ∈ S ∧ A ≠ B ∧ x ∈ A ∧ x ∈ B" using * 1 by auto from ‹sunflower S›[unfolded sunflower_def, rule_format, OF this *(3)] have "x ∈ insert a C" . with 1 show "x ∈ C" unfolding T_def h_def by auto qed qed with sf show False .. qed qed qed next case r: True with rk have "k ≠ 0" by auto then obtain l where k: "k = Suc l" by (cases k, auto) show ?thesis unfolding r k by (intro exI[of _ "{}"], auto) qed text ‹The difference between the lower and the upper bound on the existence of sunflowers as they have been formalized is @{term ‹fact k›}. There is more recent work with tighter bounds \cite{sunflower_new}, but we only integrate the initial result of Erdős and Rado in this theory.› text ‹We further provide the Erdős Rado lemma lifted to obtain non-empty cores or cores of arbitrary cardinality.› lemma Erdos_Rado_sunflower_card_core: assumes "finite E" and "∀ A ∈ F. A ⊆ E ∧ s ≤ card A ∧ card A ≤ k" and "card F > (card E choose s) * (r - 1)^k * fact k" and "s ≠ 0" and "r ≠ 0" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ card (⋂ S) ≥ s" by (rule sunflower_card_core_lift[OF assms(1) _ assms(2) _ assms(4-5), of "(r - 1)^k * fact k"], rule Erdos_Rado_sunflower, insert assms(3), auto simp: ac_simps) lemma Erdos_Rado_sunflower_nonempty_core: assumes "finite E" and "∀ A ∈ F. A ⊆ E ∧ card A ≤ k" and "{} ∉ F" and "card F > card E * (r - 1)^k * fact k" shows "∃ S. S ⊆ F ∧ sunflower S ∧ card S = r ∧ ⋂ S ≠ {}" by (rule sunflower_nonempty_core_lift[OF assms(1) _ assms(2-3), of "(r - 1)^k * fact k"], rule Erdos_Rado_sunflower, insert assms(4), auto simp: ac_simps) end