Quelle  Sunflower.thy

(* 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) ==> ∃_\<le>₁ 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 "∃_\<le>₁ 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. ∃_\<le>₁ 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 ∨ (∃_\<le>₁ 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