# 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"
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"
{
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 

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

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.›

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 = {{}}"}.›

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],

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.›

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)

end