Theory Erdos_Rado_Sunflower

(* author: R. Thiemann *)

section ‹The Sunflower Lemma›

text ‹We formalize the proof of the sunflower lemma of Erd\H{o}s and Rado~cite"erdos_rado", 
as it is presented in the textbook~cite‹Chapter~6› in "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\H{o}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"
      using card_Union_le_sum_card by blast 
    also have "  of_nat (card G) * Suc k"
      by (metis GF Suc.prems(1) le_Suc_eq subsetD sum_bounded_above) 
    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\H{o}s and Rado in this theory.›

text ‹We further provide the Erd\H{o}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