Session Sunflowers

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: "Af -` {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 "AS. 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': "AF. 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: "¬ (SF. 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 "AG. finite A  card A = Suc k" by auto
      show "¬ (SG. 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 "SF. 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