### merged

 ... ... @@ -208,8 +208,9 @@ proof - 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')" have P_Suc: "F (Suc n) = (@N'. N' \ F n \ infinite N' \ decides \ (f (Suc n)) N')" for n by (auto simp: F_def) 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 ... ... @@ -217,16 +218,11 @@ proof - by (auto simp: F_def M0) next case (Suc n) let ?\ = "\N'. N' \ F n \ infinite N' \ decides \ (f (Suc n)) N'" have "\N'. ?\ N'" by (meson Suc ex_infinite_decides_1 subset_trans) then have "Eps ?\ \ F n \ infinite (Eps ?\) \ decides \ (f (Suc n)) (Eps ?\)" by (rule someI_ex) with Suc.IH show ?case by (auto simp: P_Suc) then show ?case by (metis P_Suc \_def ex_infinite_decides_1 someI_ex subset_trans) qed then have telescope: "F (Suc n) \ F n" for n unfolding P_Suc by (metis (no_types, lifting) ex_infinite_decides_1 someI_ex) by (metis P_Suc \_def ex_infinite_decides_1 someI_ex) let ?N = "\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 decides_all_def 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 ... ... @@ -373,8 +369,7 @@ proof - 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 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" ... ... @@ -385,7 +380,7 @@ proof - 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 Eps_\_decreasing F Inf_hd_in_hd hd_Suc_eq_Eps \x \ T\ mmap_def not_le sorted_wrt_subset subsetD) 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)" ... ... @@ -453,7 +448,7 @@ proposition strongly_accepts_1_19: 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<..}" 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" ... ... @@ -485,39 +480,22 @@ proof (rule ccontr) by (metis Diff_partition Diff_subset_conv Min_in T(1) TSN comparables_iff finite_Diff init_segment_subset subsetD sup_bot.right_neutral) 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)" 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_nS: "T \ insert ?n S" proof (elim conjE disjE) 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\ assms(5) by blast 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 have non_TS: "\ init_segment T S" by (meson Sup_nat_less_sets_singleton N \?n \ N\ \\ init_segment T (insert (?n) S) \ (\ init_segment (insert (?n) S) T \ insert (?n) S = T)\ assms(5) init_segment_insert) consider (ST) "S \ T" | (TS) "T \ S" using 2 init_segment_subset by blast then show False proof cases case ST with \
show ?thesis using 2 T(1) \T \ insert (?n) S\ comparables_iff init_segment_iff by auto next case TS then show ?thesis proof - have "\ init_segment T S" by (meson Sup_nat_less_sets_singleton N \?n \ N\ \
assms(5) init_segment_insert) then show ?thesis using 2 TS init_segment_subset by fastforce qed qed using "2" "\
" init_segment_iff by auto qed qed ... ... @@ -585,7 +563,7 @@ proof - 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 ` list.set (F n) \ M" for n 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" ... ... @@ -692,7 +670,7 @@ qed subsection \Main Theorem\ text\Weirdly, the assumption @{term "f ` \ \ {..<2}"} is not used here; it's perhaps unnecessary due to 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" ... ... @@ -741,18 +719,15 @@ proof clarify using Suc card_Diff_singleton by fastforce then have sacc: "strongly_accepts (?\ 0) (S - {Sup S}) P" using Suc by blast have "S \ {}" using Suc.hyps(2) by auto have "S - {Sup S} \ {Sup S}" by (simp add: Suc.prems(1) Sup_nat_def \S \ {}\ dual_order.strict_iff_order less_sets_def) 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 \ \" unfolding strongly_accepts_def rejects_def disjoint_iff by (metis \T \ P\ \infinite P\ IntE order_refl vimage_singleton_eq) 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 ... ... @@ -783,15 +758,16 @@ proof (induction r) 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\ \ g -` {j} \ \ \ Pow N = {}" then obtain N i where "N \ 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 \ f -` {j} \ \ \ Pow N = {})" show "\N i. N \ M \ infinite N \ i < Suc r \ (\j i \ ?avoids f j N)" proof (cases "i \ \ Pow N = {}" if "j < Suc r" "i \ j" for j have "?avoids f j N" if "j < Suc r" "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) ... ... @@ -801,14 +777,14 @@ proof (induction r) case False then have "i = r-1" using \i by linarith then have null: "f -` {j} \ \ \ Pow 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 \ h -` {k} \ \ \ Pow P = {}" 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 \ f -` {j} \ \ \ Pow P = {}" have "\i. \j i \ ?avoids f j P" proof (cases "j=0") case True then show ?thesis ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!