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 ⟹ n≤x" 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. j≠i ⟶ 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 ≡ (∀N⊆M. 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 ⟷ (∀N⊆M. 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" "S≠T" "¬ 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 "n≥N" 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. ⟦P⊆N; ⋀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 "∃x∈comparables 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