Theory Nash_Williams

section ‹The Nash-Williams Theorem›

text ‹Following S. Todor\v{c}evi{\'c}, \emph{Introduction to Ramsey Spaces},
Princeton University Press (2010), 11--12.›

theory Nash_Williams
  imports Nash_Extras
begin

lemma finite_nat_Int_greaterThan_iff:
  fixes N :: "nat set"
  shows "finite (N  {n<..})  finite N"
  apply (simp add: finite_nat_iff_bounded subset_iff)
  by (metis dual_order.strict_trans2 nat_less_le not_less_eq)

subsection ‹Initial segments›

definition init_segment :: "nat set  nat set  bool"
  where "init_segment S T  S'. T = S  S'  S  S'"

lemma init_segment_subset: "init_segment S T  S  T"
  by (auto simp: init_segment_def)

lemma init_segment_refl: "init_segment S S"
  by (metis empty_iff init_segment_def less_sets_def sup_bot.right_neutral)

lemma init_segment_antisym: "init_segment S T; init_segment T S  S=T"
  by (auto simp: init_segment_def)

lemma init_segment_trans: "init_segment S T; init_segment T U  init_segment S U"
  unfolding init_segment_def
  by (meson UnE Un_assoc Un_upper1 less_sets_def less_sets_weaken1)

lemma init_segment_empty2 [iff]: "init_segment S {}  S={}"
  by (auto simp: init_segment_def less_sets_def)

lemma init_segment_Un: "S  S'  init_segment S (S  S')"
  by (auto simp: init_segment_def less_sets_def)

lemma init_segment_iff0:
  shows "init_segment S T  S  T  S  (T-S)" 
  by (smt (verit) DiffD1 DiffD2 Diff_partition UnE init_segment_def init_segment_subset less_sets_def)

lemma init_segment_iff:
  shows "init_segment S T  S=T  (m  T. S = {n  T. n < m})" (is "?lhs=?rhs")
proof
  assume ?lhs
  then obtain S' where S': "T = S  S'" "S  S'"
    by (meson init_segment_def)
  then have "S  T"
    by auto
  then have eq: "S' = T-S"
    using S' by (auto simp: less_sets_def)
  show ?rhs
  proof (cases "T  S")
    case True
    with S  T show ?rhs by blast
  next
    case False
    then have "Inf S'  T"
      by (metis Diff_eq_empty_iff Diff_iff Inf_nat_def1 eq)
    moreover have "x. x  S  x < Inf S'"
      using S' False by (metis Diff_eq_empty_iff Inf_nat_def1 eq less_sets_def)
    moreover have "{n  T. n < Inf S'}  S"
      using Inf_nat_def eq not_less_Least by fastforce
    ultimately show ?rhs
      using S  T by blast
  qed
next
  assume ?rhs
  then show ?lhs
  proof (elim disjE bexE)
    fix m
    assume m: "m  T" "S = {n  T. n < m}"
    then have "T = S  {n  T. m  n}"
      by auto
    moreover have "S  {n  T. m  n}"
      using m by (auto simp: less_sets_def)
    ultimately show "init_segment S T"
      using init_segment_Un by force
  qed (use init_segment_refl in blast)
qed

lemma init_segment_empty [iff]: "init_segment {} S"
  by (auto simp: init_segment_def less_sets_def)

lemma init_segment_insert_iff:
  assumes Sn: "S  {n}" and TS: "x. x  T-S  nx"
  shows "init_segment (insert n S) T  init_segment S T  n  T"
  using DiffD1 Sn TS init_segment_iff0 less_sets_def order_less_le by fastforce

lemma init_segment_insert:
  assumes "init_segment S T" and T: "T  {n}"
  shows "init_segment S (insert n T)"
  by (metis assms init_segment_Un init_segment_trans insert_is_Un sup_commute)



subsection ‹Definitions and basic properties›

definition Ramsey :: "[nat set set, nat]  bool"
  where "Ramsey  r  f    {..<r}.
                       M. infinite M 
                           (N i. N  M  infinite N  i<r 
                                  (j<r. ji  f -` {j}    Pow N = {}))"

text ‹Alternative, simpler definition suggested by a referee.›
lemma Ramsey_eq: 
  "Ramsey  r  (f    {..<r}.
                       M. infinite M 
                           (N i. N  M  infinite N  i<r    Pow N  f -` {i}))"
  unfolding Ramsey_def 
  by (intro ball_cong all_cong ex_cong1 conj_cong refl) blast


definition thin_set :: "nat set set  bool"
  where "thin_set     Collect finite  (S. T. init_segment S T  S=T)"

definition comparables :: "nat set  nat set  nat set set"
  where "comparables S M  {T. finite T  (init_segment T S  init_segment S T  T-S  M)}"

lemma comparables_iff: "T  comparables S M  finite T  (init_segment T S  init_segment S T  T  S  M)"
  by (auto simp: comparables_def init_segment_def)

lemma comparables_subset: "(comparables S M)  S  M"
  by (auto simp: comparables_def init_segment_def)

lemma comparables_empty [simp]: "comparables {} M = Fpow M"
  by (auto simp: comparables_def Fpow_def)

lemma comparables_mono: "N  M  comparables S N  comparables S M"
  by (auto simp: comparables_def)

definition "rejects  S M  comparables S M   = {}"

abbreviation accepts
  where "accepts  S M  ¬ rejects  S M"

definition strongly_accepts
  where "strongly_accepts  S M  (NM. rejects  S N  finite N)"

definition decides
  where "decides  S M  rejects  S M  strongly_accepts  S M"

definition decides_subsets
  where "decides_subsets  M  T. T  M  finite T  decides  T M"

lemma strongly_accepts_imp_accepts:
  "strongly_accepts  S M; infinite M  accepts  S M"
  unfolding strongly_accepts_def by blast

lemma rejects_trivial: "rejects  S M; thin_set ; init_segment F S; F    False"
  unfolding rejects_def thin_set_def
  using comparables_iff by blast

lemma rejects_subset: "rejects  S M; N  M  rejects  S N"
  by (fastforce simp add: rejects_def comparables_def)

lemma strongly_accepts_subset: "strongly_accepts  S M; N  M  strongly_accepts  S N"
  by (auto simp: strongly_accepts_def)

lemma decides_subset: "decides  S M; N  M  decides  S N"
  by (meson decides_def rejects_subset strongly_accepts_subset)

lemma decides_subsets_subset: "decides_subsets  M; N  M  decides_subsets  N"
  by (meson decides_subset decides_subsets_def subset_trans)

lemma rejects_empty [simp]: "rejects  {} M  Fpow M   = {}"
  by (auto simp: rejects_def comparables_def Fpow_def)

lemma strongly_accepts_empty [simp]: "strongly_accepts  {} M  (NM. Fpow N   = {}  finite N)"
  by (simp add: strongly_accepts_def Fpow_def disjoint_iff)

lemma ex_infinite_decides_1:
  assumes "infinite M"
  obtains N where "N  M" "infinite N" "decides  S N"
  by (meson assms decides_def order_refl strongly_accepts_def)

proposition ex_infinite_decides_finite:
  assumes "infinite M" "finite S"
  obtains N where "N  M" "infinite N" "T. T  S  decides  T N"
proof -
  have "finite (Pow S)"
    by (simp add: finite S)
  then obtain f :: "nat  nat set" where f: "f ` {..< card (Pow S)} = Pow S"
    by (metis bij_betw_imp_surj_on [OF bij_betw_from_nat_into_finite])
  obtain M0 where M0: "infinite M0" "M0  M" "decides  (f 0) M0"
    by (meson infinite M ex_infinite_decides_1)
  define F where "F  rec_nat M0 (λn N. @N'. N'  N  infinite N'  decides  (f (Suc n)) N')"
  define Φ where "Φ  λn N'. N'  F n  infinite N'  decides  (f (Suc n)) N'"
  have P_Suc: "F (Suc n) = (@N'. Φ n N')" for n
    by (auto simp: F_def Φ_def)
  have *: "infinite (F n)  decides  (f n) (F n)  F n  M" for n
  proof (induction n)
    case (Suc n) then show ?case
      by (metis P_Suc Φ_def ex_infinite_decides_1 someI_ex subset_trans)
  qed (auto simp: F_def M0)
  then have telescope: "F (Suc n)  F n" for n
    by (metis P_Suc Φ_def ex_infinite_decides_1 someI_ex)
  let ?N = "n<card (Pow S). F n"
  show thesis
  proof
    show "?N  M"
      by (metis "*" INF_lower2 Pow_iff f imageE order_refl)
  next
    have eq: "(n < Suc m. F n) = F m" for m
      by (induction m) (use telescope in auto simp: lessThan_Suc)
    then show "infinite ?N"
      by (metis (full_types) "*" Pow_top Suc_le_D Suc_le_eq f imageE lessThan_iff)
  next
    fix T
    assume "T  S" then show "decides  T ?N"
      by (metis (no_types) "*" INT_lower Pow_iff decides_subset f imageE)
  qed
qed


lemma sorted_wrt_subset: "X  list.set l; sorted_wrt (≤) l  hd l  X"
  by (induction l) auto

text ‹Todor\v{c}evi{\'c}'s Lemma 1.18›
proposition ex_infinite_decides_subsets:
  assumes "thin_set " "infinite M"
  obtains N where "N  M" "infinite N" "decides_subsets  N"
proof -
  obtain M0 where M0: "infinite M0" "M0  M" "decides  {} M0"
    by (meson infinite M ex_infinite_decides_1)
  define decides_all where "decides_all  λS N. T  S. decides  T N"
  define Φ where "Φ  λNL N. N  hd NL  Inf N > Inf (hd NL)  infinite N  decides_all (List.set (map Inf NL)) N"
  have "N. Φ NL N" if "infinite (hd NL)" for NL
  proof -
    obtain N where N: "N  hd NL" "infinite N" "decides_all (List.set (map Inf NL)) N"
      unfolding decides_all_def
      by (metis List.finite_set ex_infinite_decides_finite infinite (hd NL))
    then have inf: "infinite (N  {Inf (hd NL)<..})" 
      by (metis finite_nat_Int_greaterThan_iff)
    then have "Inf (N  {Inf (hd NL)<..}) > Inf (hd NL)"
      by (metis finite.emptyI Inf_nat_def1 Int_iff greaterThan_iff)
    with N show ?thesis
      unfolding Φ_def 
      by (meson Int_lower1 decides_all_def decides_subset inf subset_trans)
  qed
  then have Φ_Eps: "Φ NL (Eps (Φ NL))" if "infinite (hd NL)" for NL
    by (simp add: someI_ex that)
  define F where "F  rec_nat [M0] (λn NL. (Eps (Φ NL)) # NL)"
  have F_simps [simp]: "F 0 = [M0]" "F (Suc n) = Eps (Φ (F n)) # F n" for n
    by (auto simp: F_def)
  have F: "F n  []  sorted_wrt (≤) (F n)  list.set (F n)  Collect infinite  list.set (F n)  Pow M" for n
  proof (induction n)
    case 0
    then show ?case
      by (simp add: M0)
  next
    case (Suc n)
    then have *: "Φ (F n) (Eps (Φ (F n)))"
      using Φ_Eps hd_in_set by blast
    show ?case
    proof (intro conjI)
      show "sorted_wrt (⊆) (F (Suc n))"
        using subset_trans [OF _ sorted_wrt_subset] Suc.IH Φ_def "*" by auto
      show "list.set (F (Suc n))  {S. infinite S}"
        using "*" Φ_def Suc.IH by force
      show "list.set (F (Suc n))  Pow M"
        using "*" Suc.IH Φ_def hd_in_set by force
    qed auto
  qed
  have ΦF: "Φ (F n) (Eps (Φ (F n)))" for n
    using F Φ_Eps hd_in_set by blast
  then have decides: "decides_all (List.set (map Inf (F n))) (Eps (Φ (F n)))" for n
    using Φ_def by blast
  have Eps_subset_hd: "Eps (Φ (F n))  hd (F n) " for n
    using ΦF Φ_def by blast
  have "List.set (map Inf (F n))  List.set (map Inf (F (Suc n)))" for n
    by auto
  then have map_Inf_subset: "m  n  List.set (map Inf (F m))  List.set (map Inf (F n))" for m n
    by (rule order_class.lift_Suc_mono_le) auto
  define mmap where "mmap  λn. Inf (hd (F (Suc n)))"
  have "mmap n < mmap (Suc n)" for n
    by (metis F_simps(2) ΦF Φ_def list.sel(1) mmap_def)
  then have "strict_mono mmap"
    by (simp add: lift_Suc_mono_less strict_mono_def)
  have finite_F_bound: "n. S  List.set (map Inf (F n))"
    if S: "S  range mmap" "finite S" for S
  proof -
    obtain K where "finite K" "S  mmap ` K"
      by (metis S finite_subset_image order_refl)
    show ?thesis
    proof
      have "mmap ` K  list.set (map Inf (F (Suc (Max K))))"
        unfolding mmap_def image_subset_iff
        by (metis F Max_ge Suc_le_mono finite K hd_in_set imageI map_Inf_subset set_map subsetD)
      with S show "S  list.set (map Inf (F (Suc (Max K))))"
        using S  mmap ` K by auto
    qed
  qed
  have "Eps (Φ (F (Suc n)))  Eps (Φ (F n))" for n
    by (metis F_simps(2) ΦF Φ_def list.sel(1))
  then have Eps_Φ_decreasing: "m  n  Eps (Φ (F n))  Eps (Φ (F m))" for m n
    by (rule order_class.lift_Suc_antimono_le)
  have hd_Suc_eq_Eps: "hd (F (Suc n)) = Eps (Φ (F n))" for n
    by simp
  have "Inf (hd (F n))  hd (F n)" for n
    by (metis Inf_nat_def1 ΦF Φ_def finite.emptyI rev_finite_subset)
  then have Inf_hd_in_Eps: "Inf (hd (F m))  Eps (Φ (F n))" if "m>n" for m n
    by (metis Eps_Φ_decreasing Nat.lessE hd_Suc_eq_Eps less_imp_le_nat subsetD that)
  then have image_mmap_subset_hd_F: "mmap ` {n..}  hd (F (Suc n))" for n
    by (metis hd_Suc_eq_Eps atLeast_iff image_subsetI le_imp_less_Suc mmap_def)
  have "list.set (F k)  list.set (F n)" if "k  n" for k n
    by (rule order_class.lift_Suc_mono_le) (use that in auto)
  then have hd_F_in_F: "hd (F k)  list.set (F n)" if "k  n" for k n
    by (meson F hd_in_set subsetD that)
  show thesis
  proof
    show infinite_mm: "infinite (range mmap)"
      using strict_mono mmap finite_imageD strict_mono_on_imp_inj_on by blast
    show "range mmap  M"
      using Eps_subset_hd M0  M image_mmap_subset_hd_F by fastforce
    show "decides_subsets  (range mmap)"
      unfolding decides_subsets_def
    proof (intro strip)
      fix S
      assume "S  range mmap" "finite S"
      define n where "n  LEAST n. S  List.set (map Inf (F n))"
      have "m. S  List.set (map Inf (F m))"
        using S  range mmap finite S finite_F_bound by blast
      then have S: "S  List.set (map Inf (F n))" and minS: "m. m<n  ¬ S  List.set (map Inf (F m))"
        unfolding n_def by (meson LeastI_ex not_less_Least)+
      have decides_Fn: "decides  S (Eps (Φ (F n)))"
        using S decides decides_all_def by blast
      show "decides  S (range mmap)"
      proof (cases "n=0")
        case True
        then show ?thesis
          by (metis image_mmap_subset_hd_F decides_Fn decides_subset hd_Suc_eq_Eps atLeast_0)
      next
        case False
        have notin_map_Inf: "x  List.set (map Inf (F n))" if "S  {x}" for x
        proof clarsimp
          fix T
          assume "x = Inf T" and "T  list.set (F n)"
          with that have ls: "S  {Inf T}"
            by auto
          have "S  List.set (map Inf (F j))" if T: "T  list.set (F (Suc j))" for j
          proof clarsimp
            fix x
            assume "x  S"
            then have "x < Inf T"
              using less_setsD ls by blast
            then have "x  T"
              using Inf_nat_def not_less_Least by auto
            obtain k where k: "x = mmap k"
              using S  range mmap x  S by blast
            moreover have "Eps (Φ (F j))  T"
              by (metis F hd_Suc_eq_Eps sorted_wrt_subset that)
            ultimately have "k < j"
              unfolding mmap_def by (metis Inf_hd_in_Eps x  T in_mono not_less_eq)
            then show "x  Inf ` list.set (F j)"
              using Suc_leI hd_F_in_F k mmap_def by blast
          qed
          then show False
            by (metis False T  set (F n) lessI minS not0_implies_Suc)
        qed
        have Inf_hd_F: "Inf (hd (F m))  Eps (Φ (F n))" if "S  {Inf (hd (F m))}" for m
          by (metis Inf_hd_in_Eps hd_F_in_F notin_map_Inf imageI leI set_map that)
        have less_S: "S  {Inf (hd (F m))}"
          if "init_segment S T" "Inf (hd (F m))  T" "Inf (hd (F m))  S" for T m
          using finite S that by (auto simp: init_segment_iff less_sets_def)
        consider "rejects  S (Eps (Φ (F n)))" | "strongly_accepts  S (Eps (Φ (F n)))"
          using decides_Fn by (auto simp: decides_def)
        then show ?thesis
        proof cases
          case 1
          then have "rejects  S (range mmap)"
            apply (simp add: rejects_def disjoint_iff mmap_def comparables_def image_iff subset_iff)
            by (metis less_S Inf_hd_F hd_Suc_eq_Eps)
          then show ?thesis
            by (auto simp: decides_def)
        next
          case 2
          have False
            if "N  range mmap" and "rejects  S N" and "infinite N" for N
          proof -
            have "N = mmap ` {n..}  N  mmap ` {..<n}  N"
              using in_mono that(1) by fastforce
            then have "infinite (mmap ` {n..}  N)"
              by (metis finite_Int finite_Un finite_imageI finite_lessThan infinite N)
            moreover have "rejects  S (mmap ` {n..}  N)"
              using rejects_subset rejects  S N by fastforce
            moreover have "mmap ` {n..}  N  Eps (Φ (F n))"
              using image_mmap_subset_hd_F by fastforce
            ultimately show ?thesis
              using 2 by (auto simp: strongly_accepts_def)
          qed
          with 2 show ?thesis
            by (auto simp: decides_def strongly_accepts_def)
        qed
      qed
    qed
  qed
qed


text ‹Todor\v{c}evi{\'c}'s Lemma 1.19›
proposition strongly_accepts_1_19:
  assumes acc: "strongly_accepts  S M"
    and "thin_set " "infinite M" "S  M" "finite S"
    and dsM: "decides_subsets  M"
  shows "finite {n  M. ¬ strongly_accepts  (insert n S) M}"
proof (rule ccontr)
  define N where "N  {n  M. rejects  (insert n S) M}  {Sup S<..}"
  have "N  M" and N: "n. n  N  n  M  rejects  (insert n S) M  n > Sup S"
    by (auto simp: N_def)
  assume "¬ ?thesis"
  moreover have "{n  M. ¬ strongly_accepts  (insert n S) M} = {n  M. rejects  (insert n S) M}"
    using dsM finite S infinite M S  M unfolding decides_subsets_def
    by (meson decides_def finite.insertI insert_subset strongly_accepts_imp_accepts)
  ultimately have "infinite N"
    by (simp add: N_def finite_nat_Int_greaterThan_iff)
  then have "accepts  S N"
    using acc strongly_accepts_def N  M by blast
  then obtain T where T: "T  comparables S N" "T  " and TSN: "T  S  N"
    unfolding rejects_def using comparables_iff init_segment_subset by fastforce
  then consider "init_segment T S" | "init_segment S T" "ST" "¬ init_segment T S"
    by (auto simp: comparables_def)
  then show False
  proof cases
    case 1
    then have "init_segment T (insert n S)" if "n  N" for n
      by (meson Sup_nat_less_sets_singleton N finite S init_segment_insert that)
    with infinite N thin_set  T   show False
      by (meson N infinite_nat_iff_unbounded rejects_trivial)
  next
    let ?n = "Min (T-S)"
    case 2
    then have TS: "finite (T-S)" "T - S  {}"
      using T(1) init_segment_subset by (force simp: comparables_iff)+
    then have "?n  N"
      by (meson Diff_subset_conv Min_in TSN subsetD)
    then have "rejects  (insert ?n S) N"
      using rejects_subset N  M by (auto simp: N_def)
    then have "¬ init_segment T (insert ?n S)" "(init_segment (insert ?n S) T  insert ?n S = T)"
      using T Diff_partition TSN ?n  N finite S
      by (auto simp: rejects_def comparables_iff disjoint_iff)
    moreover have "S  {?n}"
      using Sup_nat_less_sets_singleton N ?n  N finite S by blast
    ultimately show ?thesis
      using 2 by (metis DiffD1 eq_Min_iff TS init_segment_insert_iff)
  qed
qed

text ‹Much work is needed for this slight strengthening of the previous result!›
proposition strongly_accepts_1_19_plus:
  assumes "thin_set " "infinite M"
    and dsM: "decides_subsets  M"
  obtains N where "N  M" "infinite N"
       "S n. S  N; finite S; strongly_accepts  S N; n  N; S  {n}
               strongly_accepts  (insert n S) N"
proof -
  define insert_closed where
    "insert_closed  λNL N. T  Inf ` set NL. n  N.
                      strongly_accepts  T ((Inf ` set NL)  hd NL) 
                      T  {n}  strongly_accepts  (insert n T) ((Inf ` set NL)  hd NL)"
  define Φ where "Φ  λNL N. N  hd NL  Inf N > Inf (hd NL)  infinite N  insert_closed NL N"
  have "N. Φ NL N" if NL: "infinite (hd NL)" "Inf ` set NL  hd NL  M" for NL
  proof -
    let ?m = "Inf ` set NL"
    let ?M = "?m  hd NL"
    define P where "P  λS. {n  ?M. ¬ strongly_accepts  (insert n S) ?M}"
    have "k. P S  {..k}"
      if "S  Inf ` set NL" "strongly_accepts  S ?M" for S
    proof -
      have "decides_subsets  ?M"
        using NL(2) decides_subsets_subset dsM by blast
      with that NL assms finite_surj have "finite (P S)"
        unfolding P_def by (blast intro!: strongly_accepts_1_19)
      then show ?thesis
        by (simp add: finite_nat_iff_bounded_le)
    qed
    then obtain f where f: "S. S  Inf ` set NL; strongly_accepts  S ?M  P S  {..f S}"
      by metis
    define m where "m  Max (insert (Inf (hd NL)) (f ` Pow (Inf ` set NL)))"
    have §: "strongly_accepts  (insert n S) ?M"
      if S: "S  Inf ` set NL" "strongly_accepts  S ?M" and n: "n  hd NL  {m<..}" for S n
    proof -
      have "f S  m"
        unfolding m_def using that(1) by auto
      then show ?thesis
        using f [OF S] n unfolding P_def by auto
    qed
    have "Φ NL (hd NL  {m<..})"
      unfolding Φ_def
    proof (intro conjI)
      show "infinite (hd NL  {m<..})"
        by (simp add: finite_nat_Int_greaterThan_iff that(1))
      moreover have "Inf (hd NL)  m"
        by (simp add: m_def)
      ultimately show "Inf (hd NL) < Inf (hd NL  {m<..})"
        using Inf_nat_def1 [of "(hd NL  {m<..})"] by force
      show "insert_closed NL (hd NL  {m<..})"
        by (auto intro: § simp: insert_closed_def)
    qed auto
    then show ?thesis ..
  qed
  then have Φ_Eps: "Φ NL (Eps (Φ NL))" if "infinite (hd NL)" "(Inf ` set NL)  hd NL  M" for NL
    by (meson someI_ex that)
  define F where "F  rec_nat [M] (λn NL. (Eps (Φ NL)) # NL)"
  have F_simps [simp]: "F 0 = [M]" "F (Suc n) = Eps (Φ (F n)) # F n" for n
    by (auto simp: F_def)
  have InfM: "Inf M  M"
    by (metis Inf_nat_def1 assms(2) finite.emptyI)
  have F: "F n  []  sorted_wrt (≤) (F n)  list.set (F n)  Collect infinite  set (F n)  Pow M  Inf ` set (F n)  M" for n
  proof (induction n)
    case (Suc n)
    have "hd (F n)  M"
      by (meson Pow_iff Suc.IH hd_in_set subsetD)
    then obtain Φ: "Ball (list.set (F n)) ((⊆) (Eps (Φ (F n))))" "infinite (Eps (Φ (F n)))" 
      using order_trans [OF _ sorted_wrt_subset] 
      by (metis Suc.IH Un_subset_iff Φ_Eps Φ_def hd_in_set mem_Collect_eq subsetD)
    then have M: "Eps (Φ (F n))  M"
      by (meson Pow_iff Suc.IH hd_in_set subset_iff)
    with Φ have "Inf (Eps (Φ (F n)))  M"
      by (metis Inf_nat_def1 finite.simps in_mono)
    with Φ M show ?case
      using Suc by simp
  qed (auto simp: InfM infinite M)
  have ΦF: "Φ (F n) (Eps (Φ (F n)))" for n
    by (metis Ball_Collect F Pow_iff Un_subset_iff Φ_Eps hd_in_set subsetD)
  then have insert_closed: "insert_closed (F n) (Eps (Φ (F n)))" for n
    using Φ_def by blast
  have Eps_subset_hd: "Eps (Φ (F n))  hd (F n)" for n
    using ΦF Φ_def by blast
  define mmap where "mmap  λn. Inf (hd (F (Suc n)))"
  have "mmap n < mmap (Suc n)" for n
    by (metis F_simps(2) ΦF Φ_def list.sel(1) mmap_def)
  then have "strict_mono mmap"
    by (simp add: lift_Suc_mono_less strict_mono_def)
  then have "inj mmap"
    by (simp add: strict_mono_imp_inj_on)
  have "Eps (Φ (F (Suc n)))  Eps (Φ (F n))" for n
    by (metis F_simps(2) ΦF Φ_def list.sel(1))
  then have Eps_Φ_decreasing: "m  n  Eps (Φ (F n))  Eps (Φ (F m))" for m n
    by (rule order_class.lift_Suc_antimono_le)
  have hd_Suc_eq_Eps: "hd (F (Suc n)) = Eps (Φ (F n))" for n
    by simp
  have "Inf (hd (F n))  hd (F n)" for n
    by (metis Inf_nat_def1 ΦF Φ_def finite.emptyI finite_subset)
  then have Inf_hd_in_Eps: "Inf (hd (F m))  Eps (Φ (F n))" if "m>n" for m n
    by (metis Eps_Φ_decreasing Nat.lessE hd_Suc_eq_Eps nat_less_le subsetD that)
  then have image_mmap_subset_hd_F: "mmap ` {n..}  hd (F (Suc n))" for n
    by (metis hd_Suc_eq_Eps atLeast_iff image_subsetI le_imp_less_Suc mmap_def)
  have "list.set (F k)  list.set (F n)" if "k  n" for k n
    by (rule order_class.lift_Suc_mono_le) (use that in auto)
  then have hd_F_in_F: "hd (F k)  list.set (F n)" if "k  n" for k n
    by (meson F hd_in_set subsetD that)
  show ?thesis
  proof
    show infinite_mm: "infinite (range mmap)"
      using inj mmap range_inj_infinite by blast
    show "range mmap  M"
      using Eps_subset_hd image_mmap_subset_hd_F by fastforce
  next
    fix S a
    assume S: "S  range mmap" "finite S" and acc: "strongly_accepts  S (range mmap)"
       and a: "a  range mmap" and Sn: "S  {a}"
    then obtain n where n: "a = mmap n"
      by auto
    define N where "N  LEAST n. S  mmap ` {..<n}"
    have "n. S  mmap ` {..<n}"
      by (metis S finite_nat_iff_bounded finite_subset_image image_mono)
    then have S: "S  mmap ` {..<N}" and minS: "m. m<N  ¬ S  mmap ` {..<m}"
      unfolding N_def by (meson LeastI_ex not_less_Least)+
    have range_mmap_subset: "range mmap  Inf ` list.set (F n)  hd (F n)" for n
    proof (induction n)
      case 0
      then show ?case
        using Eps_subset_hd image_mmap_subset_hd_F by fastforce
    next
      case (Suc n)
      then show ?case
        by clarsimp (metis Inf_hd_in_Eps hd_F_in_F image_iff leI mmap_def)
    qed
    have subM: "(Inf ` list.set (F N)  hd (F N))  M"
      by (meson F PowD hd_in_set subsetD sup.boundedI)
    have "strongly_accepts  (insert a S) (Inf ` list.set (F N)  hd (F N))"
    proof (rule insert_closed [unfolded insert_closed_def, rule_format])
      have "mmap ` {..<N}  Inf ` list.set (F N)"
        using Suc_leI hd_F_in_F by (fastforce simp: mmap_def le_eq_less_or_eq)
      with S show Ssub: "S  Inf ` list.set (F N)"
        by auto
      have "S  mmap ` {..<n}"
        using Sn S strict_mono mmap strict_mono_less
        by (fastforce simp: less_sets_def n image_iff subset_iff Bex_def)
      with leI minS have "nN" by blast
      then show "a  Eps (Φ (F N))"
        using image_mmap_subset_hd_F n by fastforce
      show "strongly_accepts  S (Inf ` list.set (F N)  hd (F N))"
      proof (rule ccontr)
        assume "¬ strongly_accepts  S (Inf ` list.set (F N)  hd (F N))"
        then have "rejects  S (Inf ` list.set (F N)  hd (F N))"
          using dsM subM unfolding decides_subsets_def
          by (meson F Ssub finite S decides_def decides_subset subset_trans)
        moreover have "accepts  S (range mmap)"
          using inj mmap acc range_inj_infinite strongly_accepts_imp_accepts by blast
        ultimately show False
          by (meson range_mmap_subset rejects_subset)
      qed
    qed (auto simp: Sn)
    then show "strongly_accepts  (insert a S) (range mmap)"
      using range_mmap_subset strongly_accepts_subset by auto
  qed
qed


subsection ‹Main Theorem›

lemma Nash_Williams_1: "Ramsey  1"
  by (auto simp: Ramsey_eq)

theorem Nash_Williams_2:
  assumes "thin_set " shows "Ramsey  2"
  unfolding Ramsey_eq
proof clarify
  fix f :: "nat set  nat" and M :: "nat set"
  assume "infinite M" and f2: "f    {..<2}"
  let ?ℱ = "λi. f -` {i}  "  ―‹needed with @{thm[source] Ramsey_eq}, not with  @{thm[source] Ramsey_def}
  have : "?ℱ 0  ?ℱ 1 = "
    using f2 less_2_cases by (auto simp: PiE)
  have finℱ: "X. X    finite X" and thin: "i. thin_set (?ℱ i)" 
    using assms thin_set_def by auto
  then obtain N where "N  M" "infinite N" and N: "decides_subsets (?ℱ 0) N"
    using infinite M ex_infinite_decides_subsets by blast
  then consider "rejects (?ℱ 0) {} N" | "strongly_accepts (?ℱ 0) {} N"
    unfolding decides_def decides_subsets_def by blast
  then show "N i. N  M  infinite N  i<2    Pow N  f -` {i}"
  proof cases
    case 1
    then have "(?ℱ 0  ?ℱ 1)  Pow N  f -` {1}"
      using f2 finℱ by (auto simp: Fpow_Pow_finite)
    then show ?thesis
      by (metis  Suc_1 N  M infinite N lessI)
  next
    case 2
    then have §: "P. PN; S. S  P; finite S  S  ?ℱ 0  finite P"
      by (auto simp: Fpow_def disjoint_iff)
    obtain P where "P  N" "infinite P" and P:
      "S n. S  P; finite S; strongly_accepts (?ℱ 0) S P; n  P; S  {n}
               strongly_accepts (?ℱ 0) (insert n S) P"
      using strongly_accepts_1_19_plus [OF thin infinite N N] by blast
    have "  Pow P  f -` {0}"
    proof (clarsimp simp: subset_vimage_iff)
      fix T
      assume T: "T  " and "T  P"
      then have "finite T"
        using finℱ by blast
      moreover have "strongly_accepts (?ℱ 0) S P" if "finite S" "S  P" for S
        using that
      proof (induction "card S" arbitrary: S)
        case (Suc n)
        then have Seq: "S = insert (Sup S) (S - {Sup S})"
          using Sup_nat_def Max_eq_iff by fastforce
        then have sacc: "strongly_accepts (?ℱ 0) (S - {Sup S}) P"
          by (metis Suc card_Diff_singleton diff_Suc_1 finite_Diff insertCI insert_subset) 
        have "S - {Sup S}  {Sup S}"
          using Suc by (simp add: Sup_nat_def dual_order.strict_iff_order less_sets_def)
        then have "strongly_accepts (?ℱ 0) (insert (Sup S) (S - {Sup S})) P"
          by (metis P Seq Suc.prems finite_Diff insert_subset sacc)
        then show ?case
          using Seq by auto
      qed (use 2 P  N in auto)
      ultimately have "xcomparables T P. f x = 0  x  "
        using T  P infinite P rejects_def strongly_accepts_def by fastforce
      then show "f T = 0"
        using T assms thin_set_def comparables_def by force
    qed
    then show ?thesis
      by (meson N  M P  N infinite P less_2_cases_iff subset_trans)
  qed
qed 
  

theorem Nash_Williams:
  assumes : "thin_set " "r > 0" shows "Ramsey  r"
  using r > 0
proof (induction r)
  case (Suc r)
  show ?case
  proof (cases "r<2")
    case True
    with less_2_cases Nash_Williams_1 Nash_Williams_2 assms show ?thesis
      by (auto simp: numeral_2_eq_2)
  next
    case False
    with Suc.IH have Ram: "Ramsey  r" "r  2"
      by auto
    show ?thesis
      unfolding Ramsey_eq
    proof clarify
      fix f and M :: "nat set"
      assume fim: "f    {..<Suc r}"
        and "infinite M"
      let ?within = "λg i N.   Pow N  g -` {i}"
      define g where "g  λx. if f x = r then r-1 else f x"
      have gim: "g    {..<r}"
        using fim False by (force simp: g_def)
      then obtain N i where "N  M" "infinite N" "i<r" and i: "?within g i N"
        using Ram infinite M by (metis Ramsey_eq)
      show "N j. N  M  infinite N  j < Suc r  ?within f j N"
      proof (cases "i<r-1")
        case True
        then have "?within f i N"
          using N  M infinite N i<r i by (fastforce simp add: g_def)
        then show ?thesis
          by (meson N  M i < r infinite N less_Suc_eq)
      next
        case False
        then have "i = r-1"
          using i<r by linarith
        then have null: "  Pow N  f -` {i,r}" 
          using i i < r 
          by (auto simp: g_def split: if_split_asm)
        define h where "h  λx. if f x = r then 0 else f x"
        have him: "h    {..<r}"
          using fim i False i<r by (force simp: h_def)
        then obtain P j where "P  N" "infinite P" "j<r" and j: "?within h j P"
          using Ram i < r infinite N unfolding Ramsey_eq by metis
        have "i < Suc r. ?within f i P"
        proof (cases "j=0")
          case True
          then have "  Pow P  f -` {r}"
            using Ram(2) P  N i = r - 1  i j  
            unfolding subset_vimage_iff g_def h_def
            by (metis Int_iff Pow_iff Suc_1 diff_is_0_eq insert_iff not_less_eq_eq subset_trans)
          then show ?thesis
            by blast
        next
          case False
          then show ?thesis
            using j j < r by (fastforce simp add: h_def less_Suc_eq)
        qed
        then show ?thesis
          by (meson N  M P  N infinite P subset_trans)
      qed
    qed
  qed
qed auto

end