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 ⟹ 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 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 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 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 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 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} ∩ ℱ"
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