diff --git a/thys/Nash_Williams/Nash_Williams.thy b/thys/Nash_Williams/Nash_Williams.thy --- a/thys/Nash_Williams/Nash_Williams.thy +++ b/thys/Nash_Williams/Nash_Williams.thy @@ -1,806 +1,775 @@ section \The Nash-Williams Theorem\ text \Following S. Todorčević, \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_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 (auto simp: less_sets_def intro!: Inf_nat_def1) + 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) - assume "S = T" - then show "init_segment S T" - using init_segment_refl by blast - next 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 + 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" + shows "init_segment (insert n S) T \ init_segment S T \ n \ T" (is "?lhs=?rhs") proof - assume "init_segment (insert n S) T" - then have "init_segment ({n} \ S) T" - by auto - then show "init_segment S T \ n \ T" - by (metis Sn Un_iff init_segment_def init_segment_trans insertI1 sup_commute) + assume ?lhs then show ?rhs + by (metis Sn Un_commute init_segment_Un init_segment_subset init_segment_trans insertI1 insert_is_Un subsetD) next - assume rhs: "init_segment S T \ n \ T" + assume rhs: ?rhs then obtain R where R: "T = S \ R" "S \ R" by (auto simp: init_segment_def less_sets_def) then have "S\R = insert n (S \ (R-{n})) \ insert n S \ R-{n}" unfolding less_sets_def using rhs TS nat_less_le by auto - then show "init_segment (insert n S) T" + then show ?lhs using R init_segment_Un by force qed lemma init_segment_insert: assumes "init_segment S T" and T: "T \ {n}" shows "init_segment S (insert n T)" proof (cases "T={}") case False obtain S' where S': "T = S \ S'" "S \ S'" by (meson assms init_segment_def) then have "insert n T = S \ (insert n S')" "S \ (insert n S')" using T False by (auto simp: less_sets_def) then show ?thesis using init_segment_Un by presburger qed (use assms in auto) subsection \Definitions and basic properties\ definition Ramsey :: "[nat set set, nat] \ bool" where "Ramsey \ r \ \f \ \ \ {..M. infinite M \ (\N i. N \ M \ infinite N \ i (\ji \ f - {j} \ \ \ Pow N = {}))" text \Alternative definition suggested by a referee. Despite its simplicity, it doesn't simplify proofs.\ lemma Ramsey_eq: "Ramsey \ r \ (\f \ \ \ {..M. infinite M \ (\N i. N \ M \ infinite N \ i \ \ 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" unfolding decides_def using rejects_subset strongly_accepts_subset by blast 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 0 - with \infinite M\ show ?case - by (auto simp: F_def M0) - next - case (Suc n) - then show ?case + case (Suc n) then show ?case by (metis P_Suc \_def ex_infinite_decides_1 someI_ex subset_trans) - qed + 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 M" by (metis "*" INF_lower2 Pow_iff f imageE order_refl) next have eq: "(\n\m. F n) = F m" for m by (induction m) (use telescope in \auto simp: atMost_Suc\) then show "infinite ?N" by (metis "*" Suc_le_D Suc_le_eq finite_subset le_INF_iff lessThan_Suc_atMost lessThan_iff) next fix T assume "T \ S" then obtain m where "f m = T" "m < card (Pow S)" using f by (blast elim: equalityE) then show "decides \ T ?N" by (metis "*" INT_lower decides_subset lessThan_iff) qed qed lemma sorted_wrt_subset: "\X \ list.set l; sorted_wrt (\) l\ \ hd l \ X" by (induction l) auto text \Todorčević'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 \_def decides_all_def by (metis List.finite_set ex_infinite_decides_finite \infinite (hd NL)\) then have "Inf (N \ {Inf (hd NL)<..}) > Inf (hd NL)" by (metis Inf_nat_def1 Int_iff finite.emptyI finite_nat_Int_greaterThan_iff greaterThan_iff) then show ?thesis unfolding \_def by (meson Int_lower1 N decides_all_def decides_subset finite_nat_Int_greaterThan_iff 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) then have "inj mmap" by (simp add: strict_mono_imp_inj_on) 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 \finite K\ hd_in_set imageI map_Inf_subset not_less_eq_eq set_map subsetD) + 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_in_hd: "Inf (hd (F n)) \ hd (F n)" for n + 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 leD mmap_def not_less_eq_eq subsetD that hd_Suc_eq_Eps) + 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 \inj mmap\ range_inj_infinite 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 "\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 \ 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 with T \x < Inf T\ have "k < j" by (metis F Inf_hd_in_Eps \x \ T\ hd_Suc_eq_Eps mmap_def not_less_eq sorted_wrt_subset subsetD) then have "Eps (\ (F k)) \ list.set (F j)" by (metis Suc_leI hd_Suc_eq_Eps hd_F_in_F) then show "x \ Inf  list.set (F j)" by (auto simp: k image_iff mmap_def) qed then obtain m where "m List.set (map Inf (F m))" using \n \ 0\ by (metis \T \ list.set (F n)\ lessI less_Suc_eq_0_disj) then show False using minS by blast 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 - have "rejects \ S (range mmap)" - proof (clarsimp simp: rejects_def disjoint_iff) - fix X - assume "X \ comparables S (range mmap)" and "X \ \" - moreover have "\x X. \X \ \; init_segment S X; x \ X; x \ S; x \ range mmap\ - \ x \ Eps (\ (F n))" - using less_S Inf_hd_F mmap_def by blast - ultimately have "X \ comparables S (Eps (\ (F n)))" - by (auto simp: comparables_def disjoint_iff subset_iff) - with 1 \X \ \\ show False by (auto simp: rejects_def) - qed + 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" using in_mono that(1) by fastforce then have "infinite (mmap  {n..} \ N)" by (metis finite_Int finite_Un finite_imageI finite_lessThan that(3)) 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 have "strongly_accepts \ S (range mmap)" - by (auto simp: strongly_accepts_def) - then show ?thesis - by (auto simp: decides_def) + with 2 show ?thesis + by (auto simp: decides_def strongly_accepts_def) qed qed qed qed qed text \Todorčević'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 \ M. rejects \ (insert n S) M}" - by simp - then have "infinite N" + 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" + 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 obtain TS: "?n \ T-S" "finite (T-S)" + using T unfolding comparables_iff + by (meson Diff_eq_empty_iff Min_in finite_Diff init_segment_subset subset_antisym) then have "?n \ N" - by (metis Diff_partition Diff_subset_conv Min_in T(1) TSN comparables_iff finite_Diff init_segment_subset subsetD sup_bot.right_neutral) + by (meson Diff_subset_conv TSN in_mono) 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 \Min (T - S) \ N\ \finite S\ - unfolding rejects_def comparables_iff disjoint_iff - by auto - then have "T \ insert ?n S" - proof (elim conjE impCE) - assume "\ init_segment T (insert ?n S)" "\ init_segment (insert ?n S) T" - moreover have "S \ {Min (T - S)}" - using Sup_nat_less_sets_singleton N \Min (T - S) \ N\ \finite S\ by blast - moreover have "finite (T - S)" - using T comparables_iff by blast - ultimately show ?thesis - using \init_segment S T\ Min_in init_segment_insert_iff by auto - qed auto - then show False - using "2" "\
" init_segment_iff by auto + 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 TS Min_in init_segment_insert_iff by fastforce 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 "finite (P S)" unfolding P_def proof (rule strongly_accepts_1_19) show "decides_subsets \ ?M" using NL(2) decides_subsets_subset dsM by blast show "finite S" using finite_surj that(1) by blast qed (use that NL assms in auto) 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) have "Inf (hd NL) \ m" by (simp add: m_def) then show "Inf (hd NL) < Inf (hd NL \ {m<..})" by (metis Inf_nat_def1 Int_iff finite.emptyI finite_nat_Int_greaterThan_iff greaterThan_iff le_less_trans that(1)) show "infinite (hd NL \ {m<..})" by (simp add: finite_nat_Int_greaterThan_iff that(1)) 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 have 1: "Ball (list.set (F n)) ((\) (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) have 2: "infinite (Eps (\ (F n)))" by (metis Ball_Collect Pow_iff Suc.IH Un_subset_iff \_Eps \_def hd_in_set subset_iff) have 3: "Eps (\ (F n)) \ M" by (meson Pow_iff Suc.IH 1 hd_in_set subset_iff) have "Inf (Eps (\ (F n))) \ M" by (metis 2 3 Inf_nat_def1 finite.simps in_mono) with 1 2 3 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 subset_code(1)) 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 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 \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 \ 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. S \ mmap  {..S \ range mmap\ \finite S\ finite_nat_iff_bounded finite_subset_image image_mono) then have S: "S \ mmap  {..m. m \ S \ 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  {.. 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  {..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\ text\Weirdly, the assumption @{term "f  \ \ {..<2}"} is not used here; it's unnecessary due to the particular way that @{term Ramsey} is defined. It's only needed for @{term "r > 2"}\ theorem Nash_Williams_2: assumes "thin_set \" shows "Ramsey \ 2" unfolding Ramsey_def proof clarify fix f :: "nat set \ nat" and M :: "nat set" assume "infinite M" let ?\ = "\i. f - {i} \ \" have fin\: "\X. X \ \ \ finite X" using assms thin_set_def by auto have thin: "thin_set (?\ i)" for i using assms thin_set_def by auto obtain N where "N \ M" "infinite N" and N: "decides_subsets (?\ 0) N" using \infinite M\ ex_infinite_decides_subsets thin 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 \ (\j<2. j \ i \ f -` {j} \ \ \ Pow N = {})" proof cases case 1 then have "?\ 0 \ Pow N = {}" unfolding rejects_def disjoint_iff by (metis IntD2 PowD comparables_iff fin\ init_segment_empty sup_bot.left_neutral) then show ?thesis using \N \ M\ \infinite N\ less_2_cases_iff by auto 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 "?\ 1 \ Pow P = {}" proof (clarsimp simp: disjoint_iff) fix T assume T: "f T = Suc 0" "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 "card (S - {Sup S}) = n" using Suc card_Diff_singleton by fastforce then have sacc: "strongly_accepts (?\ 0) (S - {Sup S}) P" using Suc by blast 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 False using T assms thin_set_def comparables_def by force qed then show ?thesis by (metis One_nat_def \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 then show ?thesis by (metis Nash_Williams_2 One_nat_def Ramsey_def assms(1) less_2_cases less_one numeral_2_eq_2 order_refl) next case False with Suc.IH have Ram: "Ramsey \ r" by auto have "r \ 2" by (simp add: False leI) show ?thesis unfolding Ramsey_def proof clarify fix f and M :: "nat set" assume fim: "f \ \ \ {.. \x. if f x = r then r-1 else f x" have gim: "g \ \ \ {.. M" "infinite N" "ij. \jj\ \ ?avoids g j N" using Ram \infinite M\ by (metis Ramsey_def) show "\N i. N \ M \ infinite N \ i < Suc r \ (\j i \ ?avoids f j N)" proof (cases "i j" for j using \N \ M\ \infinite N\ \i i that apply (clarsimp simp add: disjoint_iff g_def less_Suc_eq) by (metis True diff_less less_nat_zero_code nat_neq_iff zero_less_one) then show ?thesis by (metis \N \ M\ \infinite N\ less_Suc_eq) next case False then have "i = r-1" using \i by linarith then have null: "?avoids f j N" if "ji < r\ by (auto simp: g_def disjoint_iff split: if_split_asm) define h where "h \ \x. if f x = r then 0 else f x" have him: "h \ \ \ {..i by (force simp: h_def) then obtain P j where "P \ N" "infinite P" "jkk \ ?avoids h k P" by (metis Ramsey_def Ram \infinite N\) have "\i. \j i \ ?avoids f j P" proof (cases "j=0") case True then show ?thesis apply (rule_tac x=r in exI) using null [of 0] \r \ 2\ \P \ N\ j by (force simp: h_def disjoint_iff less_Suc_eq) next case False then show ?thesis apply (rule_tac x=j in exI) using j \j < r\ by (auto simp: h_def less_Suc_eq disjoint_iff intro: less_trans) qed then show ?thesis by (metis Suc.prems \N \ M\ \P \ N\ \infinite P\ subset_trans) qed qed qed qed auto end