(* Title: HOL/Library/Ramsey.thy Author: Tom Ridge. Full finite version by L C Paulson. *) section ‹Ramsey's Theorem› theory Ramsey imports Infinite_Set FuncSet begin subsection ‹Preliminary definitions› abbreviation strict_sorted :: "'a::linorder list ⇒ bool" where "strict_sorted ≡ sorted_wrt (<)" subsubsection ‹The $n$-element subsets of a set $A$› definition nsets :: "['a set, nat] ⇒ 'a set set" ("([_]⇗_⇖)" [0,999] 999) where "nsets A n ≡ {N. N ⊆ A ∧ finite N ∧ card N = n}" lemma nsets_mono: "A ⊆ B ⟹ nsets A n ⊆ nsets B n" by (auto simp: nsets_def) lemma nsets_Pi_contra: "A' ⊆ A ⟹ Pi ([A]⇗n⇖) B ⊆ Pi ([A']⇗n⇖) B" by (auto simp: nsets_def) lemma nsets_2_eq: "nsets A 2 = (⋃x∈A. ⋃y∈A - {x}. {{x, y}})" by (auto simp: nsets_def card_2_iff) lemma nsets_doubleton_2_eq [simp]: "[{x, y}]⇗2⇖ = (if x=y then {} else {{x, y}})" by (auto simp: nsets_2_eq) lemma doubleton_in_nsets_2 [simp]: "{x,y} ∈ [A]⇗2⇖ ⟷ x ∈ A ∧ y ∈ A ∧ x ≠ y" by (auto simp: nsets_2_eq Set.doubleton_eq_iff) lemma nsets_3_eq: "nsets A 3 = (⋃x∈A. ⋃y∈A - {x}. ⋃z∈A - {x,y}. {{x,y,z}})" by (simp add: eval_nat_numeral nsets_def card_Suc_eq) blast lemma nsets_4_eq: "[A]⇗4⇖ = (⋃u∈A. ⋃x∈A - {u}. ⋃y∈A - {u,x}. ⋃z∈A - {u,x,y}. {{u,x,y,z}})" (is "_ = ?rhs") proof show "[A]⇗4⇖ ⊆ ?rhs" by (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) blast show "?rhs ⊆ [A]⇗4⇖" apply (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) by (metis insert_iff singletonD) qed lemma nsets_disjoint_2: "X ∩ Y = {} ⟹ [X ∪ Y]⇗2⇖ = [X]⇗2⇖ ∪ [Y]⇗2⇖ ∪ (⋃x∈X. ⋃y∈Y. {{x,y}})" by (fastforce simp: nsets_2_eq Set.doubleton_eq_iff) lemma ordered_nsets_2_eq: fixes A :: "'a::linorder set" shows "nsets A 2 = {{x,y} | x y. x ∈ A ∧ y ∈ A ∧ x<y}" (is "_ = ?rhs") proof show "nsets A 2 ⊆ ?rhs" unfolding numeral_nat apply (clarsimp simp add: nsets_def card_Suc_eq Set.doubleton_eq_iff not_less) by (metis antisym) show "?rhs ⊆ nsets A 2" unfolding numeral_nat by (auto simp: nsets_def card_Suc_eq) qed lemma ordered_nsets_3_eq: fixes A :: "'a::linorder set" shows "nsets A 3 = {{x,y,z} | x y z. x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ x<y ∧ y<z}" (is "_ = ?rhs") proof show "nsets A 3 ⊆ ?rhs" apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral) by (metis insert_commute linorder_cases) show "?rhs ⊆ nsets A 3" apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral) by (metis empty_iff insert_iff not_less_iff_gr_or_eq) qed lemma ordered_nsets_4_eq: fixes A :: "'a::linorder set" shows "[A]⇗4⇖ = {U. ∃u x y z. U = {u,x,y,z} ∧ u ∈ A ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ u < x ∧ x < y ∧ y < z}" (is "_ = Collect ?RHS") proof - { fix U assume "U ∈ [A]⇗4⇖" then obtain l where "strict_sorted l" "List.set l = U" "length l = 4" "U ⊆ A" by (simp add: nsets_def) (metis finite_set_strict_sorted) then have "?RHS U" unfolding numeral_nat length_Suc_conv by auto blast } moreover have "Collect ?RHS ⊆ [A]⇗4⇖" apply (clarsimp simp add: nsets_def eval_nat_numeral) apply (subst card_insert_disjoint, auto)+ done ultimately show ?thesis by auto qed lemma ordered_nsets_5_eq: fixes A :: "'a::linorder set" shows "[A]⇗5⇖ = {U. ∃u v x y z. U = {u,v,x,y,z} ∧ u ∈ A ∧ v ∈ A ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ u < v ∧ v < x ∧ x < y ∧ y < z}" (is "_ = Collect ?RHS") proof - { fix U assume "U ∈ [A]⇗5⇖" then obtain l where "strict_sorted l" "List.set l = U" "length l = 5" "U ⊆ A" apply (simp add: nsets_def) by (metis finite_set_strict_sorted) then have "?RHS U" unfolding numeral_nat length_Suc_conv by auto blast } moreover have "Collect ?RHS ⊆ [A]⇗5⇖" apply (clarsimp simp add: nsets_def eval_nat_numeral) apply (subst card_insert_disjoint, auto)+ done ultimately show ?thesis by auto qed lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" apply (simp add: binomial_def nsets_def) by (meson subset_eq_atLeast0_lessThan_finite) lemma nsets_eq_empty_iff: "nsets A r = {} ⟷ finite A ∧ card A < r" unfolding nsets_def proof (intro iffI conjI) assume that: "{N. N ⊆ A ∧ finite N ∧ card N = r} = {}" show "finite A" using infinite_arbitrarily_large that by auto then have "¬ r ≤ card A" using that by (simp add: set_eq_iff) (metis obtain_subset_with_card_n) then show "card A < r" using not_less by blast next show "{N. N ⊆ A ∧ finite N ∧ card N = r} = {}" if "finite A ∧ card A < r" using that card_mono leD by auto qed lemma nsets_eq_empty: "⟦finite A; card A < r⟧ ⟹ nsets A r = {}" by (simp add: nsets_eq_empty_iff) lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})" by (auto simp: nsets_def) lemma nsets_singleton_iff: "nsets {a} r = (if r=0 then {{}} else if r=1 then {{a}} else {})" by (auto simp: nsets_def card_gt_0_iff subset_singleton_iff) lemma nsets_self [simp]: "nsets {..<m} m = {{..<m}}" unfolding nsets_def apply auto by (metis add.left_neutral lessThan_atLeast0 lessThan_iff subset_card_intvl_is_intvl) lemma nsets_zero [simp]: "nsets A 0 = {{}}" by (auto simp: nsets_def) lemma nsets_one: "nsets A (Suc 0) = (λx. {x}) ` A" using card_eq_SucD by (force simp: nsets_def) lemma inj_on_nsets: assumes "inj_on f A" shows "inj_on (λX. f ` X) ([A]⇗n⇖)" using assms unfolding nsets_def by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq) lemma bij_betw_nsets: assumes "bij_betw f A B" shows "bij_betw (λX. f ` X) ([A]⇗n⇖) ([B]⇗n⇖)" proof - have "(`) f ` [A]⇗n⇖ = [f ` A]⇗n⇖" using assms apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset) by (metis card_image inj_on_finite order_refl subset_image_inj) with assms show ?thesis by (auto simp: bij_betw_def inj_on_nsets) qed lemma nset_image_obtains: assumes "X ∈ [f`A]⇗k⇖" "inj_on f A" obtains Y where "Y ∈ [A]⇗k⇖" "X = f ` Y" using assms apply (clarsimp simp add: nsets_def subset_image_iff) by (metis card_image finite_imageD inj_on_subset) lemma nsets_image_funcset: assumes "g ∈ S → T" and "inj_on g S" shows "(λX. g ` X) ∈ [S]⇗k⇖ → [T]⇗k⇖" using assms by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset) lemma nsets_compose_image_funcset: assumes f: "f ∈ [T]⇗k⇖ → D" and "g ∈ S → T" and "inj_on g S" shows "f ∘ (λX. g ` X) ∈ [S]⇗k⇖ → D" proof - have "(λX. g ` X) ∈ [S]⇗k⇖ → [T]⇗k⇖" using assms by (simp add: nsets_image_funcset) then show ?thesis using f by fastforce qed subsubsection ‹Partition predicates› definition partn :: "'a set ⇒ nat ⇒ nat ⇒ 'b set ⇒ bool" where "partn β α γ δ ≡ ∀f ∈ nsets β γ → δ. ∃H ∈ nsets β α. ∃ξ∈δ. f ` (nsets H γ) ⊆ {ξ}" definition partn_lst :: "'a set ⇒ nat list ⇒ nat ⇒ bool" where "partn_lst β α γ ≡ ∀f ∈ nsets β γ → {..<length α}. ∃i < length α. ∃H ∈ nsets β (α!i). f ` (nsets H γ) ⊆ {i}" lemma partn_lst_greater_resource: fixes M::nat assumes M: "partn_lst {..<M} α γ" and "M ≤ N" shows "partn_lst {..<N} α γ" proof (clarsimp simp: partn_lst_def) fix f assume "f ∈ nsets {..<N} γ → {..<length α}" then have "f ∈ nsets {..<M} γ → {..<length α}" by (meson Pi_anti_mono ‹M ≤ N› lessThan_subset_iff nsets_mono subsetD) then obtain i H where i: "i < length α" and H: "H ∈ nsets {..<M} (α ! i)" and subi: "f ` nsets H γ ⊆ {i}" using M partn_lst_def by blast have "H ∈ nsets {..<N} (α ! i)" using ‹M ≤ N› H by (auto simp: nsets_def subset_iff) then show "∃i<length α. ∃H∈nsets {..<N} (α ! i). f ` nsets H γ ⊆ {i}" using i subi by blast qed lemma partn_lst_fewer_colours: assumes major: "partn_lst β (n#α) γ" and "n ≥ γ" shows "partn_lst β α γ" proof (clarsimp simp: partn_lst_def) fix f :: "'a set ⇒ nat" assume f: "f ∈ [β]⇗γ⇖ → {..<length α}" then obtain i H where i: "i < Suc (length α)" and H: "H ∈ [β]⇗((n # α) ! i)⇖" and hom: "∀x∈[H]⇗γ⇖. Suc (f x) = i" using ‹n ≥ γ› major [unfolded partn_lst_def, rule_format, of "Suc o f"] by (fastforce simp: image_subset_iff nsets_eq_empty_iff) show "∃i<length α. ∃H∈nsets β (α ! i). f ` [H]⇗γ⇖ ⊆ {i}" proof (cases i) case 0 then have "[H]⇗γ⇖ = {}" using hom by blast then show ?thesis using 0 H ‹n ≥ γ› by (simp add: nsets_eq_empty_iff) (simp add: nsets_def) next case (Suc i') then show ?thesis using i H hom by auto qed qed lemma partn_lst_eq_partn: "partn_lst {..<n} [m,m] 2 = partn {..<n} m 2 {..<2::nat}" apply (simp add: partn_lst_def partn_def numeral_2_eq_2) by (metis less_2_cases numeral_2_eq_2 lessThan_iff nth_Cons_0 nth_Cons_Suc) subsection ‹Finite versions of Ramsey's theorem› text ‹ To distinguish the finite and infinite ones, lower and upper case names are used. › subsubsection ‹Trivial cases› text ‹Vacuous, since we are dealing with 0-sets!› lemma ramsey0: "∃N::nat. partn_lst {..<N} [q1,q2] 0" by (force simp: partn_lst_def ex_in_conv less_Suc_eq nsets_eq_empty_iff) text ‹Just the pigeon hole principle, since we are dealing with 1-sets› lemma ramsey1: "∃N::nat. partn_lst {..<N} [q0,q1] 1" proof - have "∃i<Suc (Suc 0). ∃H∈nsets {..<Suc (q0 + q1)} ([q0, q1] ! i). f ` nsets H (Suc 0) ⊆ {i}" if "f ∈ nsets {..<Suc (q0 + q1)} (Suc 0) → {..<Suc (Suc 0)}" for f proof - define A where "A ≡ λi. {q. q ≤ q0+q1 ∧ f {q} = i}" have "A 0 ∪ A 1 = {..q0 + q1}" using that by (auto simp: A_def PiE_iff nsets_one lessThan_Suc_atMost le_Suc_eq) moreover have "A 0 ∩ A 1 = {}" by (auto simp: A_def) ultimately have "q0 + q1 ≤ card (A 0) + card (A 1)" by (metis card_Un_le card_atMost eq_imp_le le_SucI le_trans) then consider "card (A 0) ≥ q0" | "card (A 1) ≥ q1" by linarith then obtain i where "i < Suc (Suc 0)" "card (A i) ≥ [q0, q1] ! i" by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc) then obtain B where "B ⊆ A i" "card B = [q0, q1] ! i" "finite B" by (meson obtain_subset_with_card_n) then have "B ∈ nsets {..<Suc (q0 + q1)} ([q0, q1] ! i) ∧ f ` nsets B (Suc 0) ⊆ {i}" by (auto simp: A_def nsets_def card_1_singleton_iff) then show ?thesis using ‹i < Suc (Suc 0)› by auto qed then show ?thesis by (clarsimp simp: partn_lst_def) blast qed subsubsection ‹Ramsey's theorem with two colours and arbitrary exponents (hypergraph version)› proposition ramsey2_full: "∃N::nat. partn_lst {..<N} [q1,q2] r" proof (induction r arbitrary: q1 q2) case 0 then show ?case by (simp add: ramsey0) next case (Suc r) note outer = this show ?case proof (cases "r = 0") case True then show ?thesis using ramsey1 by auto next case False then have "r > 0" by simp show ?thesis using Suc.prems proof (induct k ≡ "q1 + q2" arbitrary: q1 q2) case 0 show ?case proof show "partn_lst {..<1::nat} [q1, q2] (Suc r)" using nsets_empty_iff subset_insert 0 by (fastforce simp: partn_lst_def funcset_to_empty_iff nsets_eq_empty image_subset_iff) qed next case (Suc k) consider "q1 = 0 ∨ q2 = 0" | "q1 ≠ 0" "q2 ≠ 0" by auto then show ?case proof cases case 1 then have "partn_lst {..< Suc 0} [q1, q2] (Suc r)" unfolding partn_lst_def using ‹r > 0› by (fastforce simp add: nsets_empty_iff nsets_singleton_iff lessThan_Suc) then show ?thesis by blast next case 2 with Suc have "k = (q1 - 1) + q2" "k = q1 + (q2 - 1)" by auto then obtain p1 p2::nat where p1: "partn_lst {..<p1} [q1-1,q2] (Suc r)" and p2: "partn_lst {..<p2} [q1,q2-1] (Suc r)" using Suc.hyps by blast then obtain p::nat where p: "partn_lst {..<p} [p1,p2] r" using outer Suc.prems by auto show ?thesis proof (intro exI conjI) have "∃i<Suc (Suc 0). ∃H∈nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) ⊆ {i}" if f: "f ∈ nsets {..p} (Suc r) → {..<Suc (Suc 0)}" for f proof - define g where "g ≡ λR. f (insert p R)" have "f (insert p i) ∈ {..<Suc (Suc 0)}" if "i ∈ nsets {..<p} r" for i using that card_insert_if by (fastforce simp: nsets_def intro!: Pi_mem [OF f]) then have g: "g ∈ nsets {..<p} r → {..<Suc (Suc 0)}" by (force simp: g_def PiE_iff) then obtain i U where i: "i < Suc (Suc 0)" and gi: "g ` nsets U r ⊆ {i}" and U: "U ∈ nsets {..<p} ([p1, p2] ! i)" using p by (auto simp: partn_lst_def) then have Usub: "U ⊆ {..<p}" by (auto simp: nsets_def) consider (izero) "i = 0" | (ione) "i = Suc 0" using i by linarith then show ?thesis proof cases case izero then have "U ∈ nsets {..<p} p1" using U by simp then obtain u where u: "bij_betw u {..<p1} U" using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) have u_nsets: "u ` X ∈ nsets {..p} n" if "X ∈ nsets {..<p1} n" for X n proof - have "inj_on u X" using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def) then show ?thesis using Usub u that bij_betwE by (fastforce simp add: nsets_def card_image) qed define h where "h ≡ λR. f (u ` R)" have "h ∈ nsets {..<p1} (Suc r) → {..<Suc (Suc 0)}" unfolding h_def using f u_nsets by auto then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) ⊆ {j}" and V: "V ∈ nsets {..<p1} ([q1 - Suc 0, q2] ! j)" using p1 by (auto simp: partn_lst_def) then have Vsub: "V ⊆ {..<p1}" by (auto simp: nsets_def) have invinv_eq: "u ` inv_into {..<p1} u ` X = X" if "X ⊆ u ` {..<p1}" for X by (simp add: image_inv_into_cancel that) let ?W = "insert p (u ` V)" consider (jzero) "j = 0" | (jone) "j = Suc 0" using j by linarith then show ?thesis proof cases case jzero then have "V ∈ nsets {..<p1} (q1 - Suc 0)" using V by simp then have "u ` V ∈ nsets {..<p} (q1 - Suc 0)" using u_nsets [of _ "q1 - Suc 0"] nsets_mono [OF Vsub] Usub u unfolding bij_betw_def nsets_def by (fastforce elim!: subsetD) then have inq1: "?W ∈ nsets {..p} q1" unfolding nsets_def using ‹q1 ≠ 0› card_insert_if by fastforce have invu_nsets: "inv_into {..<p1} u ` X ∈ nsets V r" if "X ∈ nsets (u ` V) r" for X r proof - have "X ⊆ u ` V ∧ finite X ∧ card X = r" using nsets_def that by auto then have [simp]: "card (inv_into {..<p1} u ` X) = card X" by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u) show ?thesis using that u Vsub by (fastforce simp: nsets_def bij_betw_def) qed have "f X = i" if X: "X ∈ nsets ?W (Suc r)" for X proof (cases "p ∈ X") case True then have Xp: "X - {p} ∈ nsets (u ` V) r" using X by (auto simp: nsets_def) moreover have "u ` V ⊆ U" using Vsub bij_betwE u by blast ultimately have "X - {p} ∈ nsets U r" by (meson in_mono nsets_mono) then have "g (X - {p}) = i" using gi by blast have "f X = i" using gi True ‹X - {p} ∈ nsets U r› insert_Diff by (fastforce simp add: g_def image_subset_iff) then show ?thesis by (simp add: ‹f X = i› ‹g (X - {p}) = i›) next case False then have Xim: "X ∈ nsets (u ` V) (Suc r)" using X by (auto simp: nsets_def subset_insert) then have "u ` inv_into {..<p1} u ` X = X" using Vsub bij_betw_imp_inj_on u by (fastforce simp: nsets_def image_mono invinv_eq subset_trans) then show ?thesis using izero jzero hj Xim invu_nsets unfolding h_def by (fastforce simp add: image_subset_iff) qed moreover have "insert p (u ` V) ∈ nsets {..p} q1" by (simp add: izero inq1) ultimately show ?thesis by (metis izero image_subsetI insertI1 nth_Cons_0 zero_less_Suc) next case jone then have "u ` V ∈ nsets {..p} q2" using V u_nsets by auto moreover have "f ` nsets (u ` V) (Suc r) ⊆ {j}" using hj by (force simp add: h_def image_subset_iff nsets_def subset_image_inj card_image dest: finite_imageD) ultimately show ?thesis using jone not_less_eq by fastforce qed next case ione then have "U ∈ nsets {..<p} p2" using U by simp then obtain u where u: "bij_betw u {..<p2} U" using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) have u_nsets: "u ` X ∈ nsets {..p} n" if "X ∈ nsets {..<p2} n" for X n proof - have "inj_on u X" using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def) then show ?thesis using Usub u that bij_betwE by (fastforce simp add: nsets_def card_image) qed define h where "h ≡ λR. f (u ` R)" have "h ∈ nsets {..<p2} (Suc r) → {..<Suc (Suc 0)}" unfolding h_def using f u_nsets by auto then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) ⊆ {j}" and V: "V ∈ nsets {..<p2} ([q1, q2 - Suc 0] ! j)" using p2 by (auto simp: partn_lst_def) then have Vsub: "V ⊆ {..<p2}" by (auto simp: nsets_def) have invinv_eq: "u ` inv_into {..<p2} u ` X = X" if "X ⊆ u ` {..<p2}" for X by (simp add: image_inv_into_cancel that) let ?W = "insert p (u ` V)" consider (jzero) "j = 0" | (jone) "j = Suc 0" using j by linarith then show ?thesis proof cases case jone then have "V ∈ nsets {..<p2} (q2 - Suc 0)" using V by simp then have "u ` V ∈ nsets {..<p} (q2 - Suc 0)" using u_nsets [of _ "q2 - Suc 0"] nsets_mono [OF Vsub] Usub u unfolding bij_betw_def nsets_def by (fastforce elim!: subsetD) then have inq1: "?W ∈ nsets {..p} q2" unfolding nsets_def using ‹q2 ≠ 0› card_insert_if by fastforce have invu_nsets: "inv_into {..<p2} u ` X ∈ nsets V r" if "X ∈ nsets (u ` V) r" for X r proof - have "X ⊆ u ` V ∧ finite X ∧ card X = r" using nsets_def that by auto then have [simp]: "card (inv_into {..<p2} u ` X) = card X" by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u) show ?thesis using that u Vsub by (fastforce simp: nsets_def bij_betw_def) qed have "f X = i" if X: "X ∈ nsets ?W (Suc r)" for X proof (cases "p ∈ X") case True then have Xp: "X - {p} ∈ nsets (u ` V) r" using X by (auto simp: nsets_def) moreover have "u ` V ⊆ U" using Vsub bij_betwE u by blast ultimately have "X - {p} ∈ nsets U r" by (meson in_mono nsets_mono) then have "g (X - {p}) = i" using gi by blast have "f X = i" using gi True ‹X - {p} ∈ nsets U r› insert_Diff by (fastforce simp add: g_def image_subset_iff) then show ?thesis by (simp add: ‹f X = i› ‹g (X - {p}) = i›) next case False then have Xim: "X ∈ nsets (u ` V) (Suc r)" using X by (auto simp: nsets_def subset_insert) then have "u ` inv_into {..<p2} u ` X = X" using Vsub bij_betw_imp_inj_on u by (fastforce simp: nsets_def image_mono invinv_eq subset_trans) then show ?thesis using ione jone hj Xim invu_nsets unfolding h_def by (fastforce simp add: image_subset_iff) qed moreover have "insert p (u ` V) ∈ nsets {..p} q2" by (simp add: ione inq1) ultimately show ?thesis by (metis ione image_subsetI insertI1 lessI nth_Cons_0 nth_Cons_Suc) next case jzero then have "u ` V ∈ nsets {..p} q1" using V u_nsets by auto moreover have "f ` nsets (u ` V) (Suc r) ⊆ {j}" using hj apply (clarsimp simp add: h_def image_subset_iff nsets_def) by (metis Zero_not_Suc card_eq_0_iff card_image subset_image_inj) ultimately show ?thesis using jzero not_less_eq by fastforce qed qed qed then show "partn_lst {..<Suc p} [q1,q2] (Suc r)" using lessThan_Suc lessThan_Suc_atMost by (auto simp: partn_lst_def insert_commute) qed qed qed qed qed subsubsection ‹Full Ramsey's theorem with multiple colours and arbitrary exponents› theorem ramsey_full: "∃N::nat. partn_lst {..<N} qs r" proof (induction k ≡ "length qs" arbitrary: qs) case 0 then show ?case by (rule_tac x=" r" in exI) (simp add: partn_lst_def) next case (Suc k) note IH = this show ?case proof (cases k) case 0 with Suc obtain q where "qs = [q]" by (metis length_0_conv length_Suc_conv) then show ?thesis by (rule_tac x=q in exI) (auto simp: partn_lst_def funcset_to_empty_iff) next case (Suc k') then obtain q1 q2 l where qs: "qs = q1#q2#l" by (metis Suc.hyps(2) length_Suc_conv) then obtain q::nat where q: "partn_lst {..<q} [q1,q2] r" using ramsey2_full by blast then obtain p::nat where p: "partn_lst {..<p} (q#l) r" using IH ‹qs = q1 # q2 # l› by fastforce have keq: "Suc (length l) = k" using IH qs by auto show ?thesis proof (intro exI conjI) show "partn_lst {..<p} qs r" proof (auto simp: partn_lst_def) fix f assume f: "f ∈ nsets {..<p} r → {..<length qs}" define g where "g ≡ λX. if f X < Suc (Suc 0) then 0 else f X - Suc 0" have "g ∈ nsets {..<p} r → {..<k}" unfolding g_def using f Suc IH by (auto simp: Pi_def not_less) then obtain i U where i: "i < k" and gi: "g ` nsets U r ⊆ {i}" and U: "U ∈ nsets {..<p} ((q#l) ! i)" using p keq by (auto simp: partn_lst_def) show "∃i<length qs. ∃H∈nsets {..<p} (qs ! i). f ` nsets H r ⊆ {i}" proof (cases "i = 0") case True then have "U ∈ nsets {..<p} q" and f01: "f ` nsets U r ⊆ {0, Suc 0}" using U gi unfolding g_def by (auto simp: image_subset_iff) then obtain u where u: "bij_betw u {..<q} U" using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) then have Usub: "U ⊆ {..<p}" by (smt (verit) U mem_Collect_eq nsets_def) have u_nsets: "u ` X ∈ nsets {..<p} n" if "X ∈ nsets {..<q} n" for X n proof - have "inj_on u X" using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def) then show ?thesis using Usub u that bij_betwE by (fastforce simp add: nsets_def card_image) qed define h where "h ≡ λX. f (u ` X)" have "f (u ` X) < Suc (Suc 0)" if "X ∈ nsets {..<q} r" for X proof - have "u ` X ∈ nsets U r" using u u_nsets that by (auto simp: nsets_def bij_betwE subset_eq) then show ?thesis using f01 by auto qed then have "h ∈ nsets {..<q} r → {..<Suc (Suc 0)}" unfolding h_def by blast then obtain j V where j: "j < Suc (Suc 0)" and hj: "h ` nsets V r ⊆ {j}" and V: "V ∈ nsets {..<q} ([q1,q2] ! j)" using q by (auto simp: partn_lst_def) show ?thesis proof (intro exI conjI bexI) show "j < length qs" using Suc Suc.hyps(2) j by linarith have "nsets (u ` V) r ⊆ (λx. (u ` x)) ` nsets V r" apply (clarsimp simp add: nsets_def image_iff) by (metis card_eq_0_iff card_image image_is_empty subset_image_inj) then have "f ` nsets (u ` V) r ⊆ h ` nsets V r" by (auto simp: h_def) then show "f ` nsets (u ` V) r ⊆ {j}" using hj by auto show "(u ` V) ∈ nsets {..<p} (qs ! j)" using V j less_2_cases numeral_2_eq_2 qs u_nsets by fastforce qed next case False show ?thesis proof (intro exI conjI bexI) show "Suc i < length qs" using Suc.hyps(2) i by auto show "f ` nsets U r ⊆ {Suc i}" using i gi False apply (auto simp: g_def image_subset_iff) by (metis Suc_lessD Suc_pred g_def gi image_subset_iff not_less_eq singleton_iff) show "U ∈ nsets {..<p} (qs ! (Suc i))" using False U qs by auto qed qed qed qed qed qed subsubsection ‹Simple graph version› text ‹This is the most basic version in terms of cliques and independent sets, i.e. the version for graphs and 2 colours. › definition "clique V E ⟷ (∀v∈V. ∀w∈V. v ≠ w ⟶ {v, w} ∈ E)" definition "indep V E ⟷ (∀v∈V. ∀w∈V. v ≠ w ⟶ {v, w} ∉ E)" lemma ramsey2: "∃r≥1. ∀(V::'a set) (E::'a set set). finite V ∧ card V ≥ r ⟶ (∃R ⊆ V. card R = m ∧ clique R E ∨ card R = n ∧ indep R E)" proof - obtain N where "N ≥ Suc 0" and N: "partn_lst {..<N} [m,n] 2" using ramsey2_full nat_le_linear partn_lst_greater_resource by blast have "∃R⊆V. card R = m ∧ clique R E ∨ card R = n ∧ indep R E" if "finite V" "N ≤ card V" for V :: "'a set" and E :: "'a set set" proof - from that obtain v where u: "inj_on v {..<N}" "v ` {..<N} ⊆ V" by (metis card_le_inj card_lessThan finite_lessThan) define f where "f ≡ λe. if v ` e ∈ E then 0 else Suc 0" have f: "f ∈ nsets {..<N} 2 → {..<Suc (Suc 0)}" by (simp add: f_def) then obtain i U where i: "i < 2" and gi: "f ` nsets U 2 ⊆ {i}" and U: "U ∈ nsets {..<N} ([m,n] ! i)" using N numeral_2_eq_2 by (auto simp: partn_lst_def) show ?thesis proof (intro exI conjI) show "v ` U ⊆ V" using U u by (auto simp: image_subset_iff nsets_def) show "card (v ` U) = m ∧ clique (v ` U) E ∨ card (v ` U) = n ∧ indep (v ` U) E" using i unfolding numeral_2_eq_2 using gi U u apply (simp add: image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq) apply (auto simp: f_def nsets_def card_image inj_on_subset split: if_split_asm) done qed qed then show ?thesis using ‹Suc 0 ≤ N› by auto qed subsection ‹Preliminaries› subsubsection ‹``Axiom'' of Dependent Choice› primrec choice :: "('a ⇒ bool) ⇒ ('a × 'a) set ⇒ nat ⇒ 'a" where ― ‹An integer-indexed chain of choices› choice_0: "choice P r 0 = (SOME x. P x)" | choice_Suc: "choice P r (Suc n) = (SOME y. P y ∧ (choice P r n, y) ∈ r)" lemma choice_n: assumes P0: "P x0" and Pstep: "⋀x. P x ⟹ ∃y. P y ∧ (x, y) ∈ r" shows "P (choice P r n)" proof (induct n) case 0 show ?case by (force intro: someI P0) next case Suc then show ?case by (auto intro: someI2_ex [OF Pstep]) qed lemma dependent_choice: assumes trans: "trans r" and P0: "P x0" and Pstep: "⋀x. P x ⟹ ∃y. P y ∧ (x, y) ∈ r" obtains f :: "nat ⇒ 'a" where "⋀n. P (f n)" and "⋀n m. n < m ⟹ (f n, f m) ∈ r" proof fix n show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep]) next fix n m :: nat assume "n < m" from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) ∈ r" for k by (auto intro: someI2_ex) then show "(choice P r n, choice P r m) ∈ r" by (auto intro: less_Suc_induct [OF ‹n < m›] transD [OF trans]) qed subsubsection ‹Partition functions› definition part_fn :: "nat ⇒ nat ⇒ 'a set ⇒ ('a set ⇒ nat) ⇒ bool" ― ‹the function \<^term>‹f› partitions the \<^term>‹r›-subsets of the typically infinite set \<^term>‹Y› into \<^term>‹s› distinct categories.› where "part_fn r s Y f ⟷ (f ∈ nsets Y r → {..<s})" text ‹For induction, we decrease the value of \<^term>‹r› in partitions.› lemma part_fn_Suc_imp_part_fn: "⟦infinite Y; part_fn (Suc r) s Y f; y ∈ Y⟧ ⟹ part_fn r s (Y - {y}) (λu. f (insert y u))" by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert) lemma part_fn_subset: "part_fn r s YY f ⟹ Y ⊆ YY ⟹ part_fn r s Y f" unfolding part_fn_def nsets_def by blast subsection ‹Ramsey's Theorem: Infinitary Version› lemma Ramsey_induction: fixes s r :: nat and YY :: "'a set" and f :: "'a set ⇒ nat" assumes "infinite YY" "part_fn r s YY f" shows "∃Y' t'. Y' ⊆ YY ∧ infinite Y' ∧ t' < s ∧ (∀X. X ⊆ Y' ∧ finite X ∧ card X = r ⟶ f X = t')" using assms proof (induct r arbitrary: YY f) case 0 then show ?case by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong) next case (Suc r) show ?case proof - from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy ∈ YY" by blast let ?ramr = "{((y, Y, t), (y', Y', t')). y' ∈ Y ∧ Y' ⊆ Y}" let ?propr = "λ(y, Y, t). y ∈ YY ∧ y ∉ Y ∧ Y ⊆ YY ∧ infinite Y ∧ t < s ∧ (∀X. X⊆Y ∧ finite X ∧ card X = r ⟶ (f ∘ insert y) X = t)" from Suc.prems have infYY': "infinite (YY - {yy})" by auto from Suc.prems have partf': "part_fn r s (YY - {yy}) (f ∘ insert yy)" by (simp add: o_def part_fn_Suc_imp_part_fn yy) have transr: "trans ?ramr" by (force simp add: trans_def) from Suc.hyps [OF infYY' partf'] obtain Y0 and t0 where "Y0 ⊆ YY - {yy}" "infinite Y0" "t0 < s" "X ⊆ Y0 ∧ finite X ∧ card X = r ⟶ (f ∘ insert yy) X = t0" for X by blast with yy have propr0: "?propr(yy, Y0, t0)" by blast have proprstep: "∃y. ?propr y ∧ (x, y) ∈ ?ramr" if x: "?propr x" for x proof (cases x) case (fields yx Yx tx) with x obtain yx' where yx': "yx' ∈ Yx" by (blast dest: infinite_imp_nonempty) from fields x have infYx': "infinite (Yx - {yx'})" by auto with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f ∘ insert yx')" by (simp add: o_def part_fn_Suc_imp_part_fn part_fn_subset [where YY=YY and Y=Yx]) from Suc.hyps [OF infYx' partfx'] obtain Y' and t' where Y': "Y' ⊆ Yx - {yx'}" "infinite Y'" "t' < s" "X ⊆ Y' ∧ finite X ∧ card X = r ⟶ (f ∘ insert yx') X = t'" for X by blast from fields x Y' yx' have "?propr (yx', Y', t') ∧ (x, (yx', Y', t')) ∈ ?ramr" by blast then show ?thesis .. qed from dependent_choice [OF transr propr0 proprstep] obtain g where pg: "?propr (g n)" and rg: "n < m ⟹ (g n, g m) ∈ ?ramr" for n m :: nat by blast let ?gy = "fst ∘ g" let ?gt = "snd ∘ snd ∘ g" have rangeg: "∃k. range ?gt ⊆ {..<k}" proof (intro exI subsetI) fix x assume "x ∈ range ?gt" then obtain n where "x = ?gt n" .. with pg [of n] show "x ∈ {..<s}" by (cases "g n") auto qed from rangeg have "finite (range ?gt)" by (simp add: finite_nat_iff_bounded) then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}" by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat) with pg [of n'] have less': "s'<s" by (cases "g n'") auto have inj_gy: "inj ?gy" proof (rule linorder_injI) fix m m' :: nat assume "m < m'" from rg [OF this] pg [of m] show "?gy m ≠ ?gy m'" by (cases "g m", cases "g m'") auto qed show ?thesis proof (intro exI conjI) from pg show "?gy ` {n. ?gt n = s'} ⊆ YY" by (auto simp add: Let_def split_beta) from infeqs' show "infinite (?gy ` {n. ?gt n = s'})" by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) show "s' < s" by (rule less') show "∀X. X ⊆ ?gy ` {n. ?gt n = s'} ∧ finite X ∧ card X = Suc r ⟶ f X = s'" proof - have "f X = s'" if X: "X ⊆ ?gy ` {n. ?gt n = s'}" and cardX: "finite X" "card X = Suc r" for X proof - from X obtain AA where AA: "AA ⊆ {n. ?gt n = s'}" and Xeq: "X = ?gy`AA" by (auto simp add: subset_image_iff) with cardX have "AA ≠ {}" by auto then have AAleast: "(LEAST x. x ∈ AA) ∈ AA" by (auto intro: LeastI_ex) show ?thesis proof (cases "g (LEAST x. x ∈ AA)") case (fields ya Ya ta) with AAleast Xeq have ya: "ya ∈ X" by (force intro!: rev_image_eqI) then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb) also have "… = ta" proof - have *: "X - {ya} ⊆ Ya" proof fix x assume x: "x ∈ X - {ya}" then obtain a' where xeq: "x = ?gy a'" and a': "a' ∈ AA" by (auto simp add: Xeq) with fields x have "a' ≠ (LEAST x. x ∈ AA)" by auto with Least_le [of "λx. x ∈ AA", OF a'] have "(LEAST x. x ∈ AA) < a'" by arith from xeq fields rg [OF this] show "x ∈ Ya" by auto qed have "card (X - {ya}) = r" by (simp add: cardX ya) with pg [of "LEAST x. x ∈ AA"] fields cardX * show ?thesis by (auto simp del: insert_Diff_single) qed also from AA AAleast fields have "… = s'" by auto finally show ?thesis . qed qed then show ?thesis by blast qed qed qed qed theorem Ramsey: fixes s r :: nat and Z :: "'a set" and f :: "'a set ⇒ nat" shows "⟦infinite Z; ∀X. X ⊆ Z ∧ finite X ∧ card X = r ⟶ f X < s⟧ ⟹ ∃Y t. Y ⊆ Z ∧ infinite Y ∧ t < s ∧ (∀X. X ⊆ Y ∧ finite X ∧ card X = r ⟶ f X = t)" by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def]) corollary Ramsey2: fixes s :: nat and Z :: "'a set" and f :: "'a set ⇒ nat" assumes infZ: "infinite Z" and part: "∀x∈Z. ∀y∈Z. x ≠ y ⟶ f {x, y} < s" shows "∃Y t. Y ⊆ Z ∧ infinite Y ∧ t < s ∧ (∀x∈Y. ∀y∈Y. x≠y ⟶ f {x, y} = t)" proof - from part have part2: "∀X. X ⊆ Z ∧ finite X ∧ card X = 2 ⟶ f X < s" by (fastforce simp add: eval_nat_numeral card_Suc_eq) obtain Y t where *: "Y ⊆ Z" "infinite Y" "t < s" "(∀X. X ⊆ Y ∧ finite X ∧ card X = 2 ⟶ f X = t)" by (insert Ramsey [OF infZ part2]) auto then have "∀x∈Y. ∀y∈Y. x ≠ y ⟶ f {x, y} = t" by auto with * show ?thesis by iprover qed corollary Ramsey_nsets: fixes f :: "'a set ⇒ nat" assumes "infinite Z" "f ` nsets Z r ⊆ {..<s}" obtains Y t where "Y ⊆ Z" "infinite Y" "t < s" "f ` nsets Y r ⊆ {t}" using Ramsey [of Z r f s] assms by (auto simp: nsets_def image_subset_iff) subsection ‹Disjunctive Well-Foundedness› text ‹ An application of Ramsey's theorem to program termination. See \<^cite>‹"Podelski-Rybalchenko"›. › definition disj_wf :: "('a × 'a) set ⇒ bool" where "disj_wf r ⟷ (∃T. ∃n::nat. (∀i<n. wf (T i)) ∧ r = (⋃i<n. T i))" definition transition_idx :: "(nat ⇒ 'a) ⇒ (nat ⇒ ('a × 'a) set) ⇒ nat set ⇒ nat" where "transition_idx s T A = (LEAST k. ∃i j. A = {i, j} ∧ i < j ∧ (s j, s i) ∈ T k)" lemma transition_idx_less: assumes "i < j" "(s j, s i) ∈ T k" "k < n" shows "transition_idx s T {i, j} < n" proof - from assms(1,2) have "transition_idx s T {i, j} ≤ k" by (simp add: transition_idx_def, blast intro: Least_le) with assms(3) show ?thesis by simp qed lemma transition_idx_in: assumes "i < j" "(s j, s i) ∈ T k" shows "(s j, s i) ∈ T (transition_idx s T {i, j})" using assms by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI) text ‹To be equal to the union of some well-founded relations is equivalent to being the subset of such a union.› lemma disj_wf: "disj_wf r ⟷ (∃T. ∃n::nat. (∀i<n. wf(T i)) ∧ r ⊆ (⋃i<n. T i))" proof - have *: "⋀T n. ⟦∀i<n. wf (T i); r ⊆ ⋃ (T ` {..<n})⟧ ⟹ (∀i<n. wf (T i ∩ r)) ∧ r = (⋃i<n. T i ∩ r)" by (force simp add: wf_Int1) show ?thesis unfolding disj_wf_def by auto (metis "*") qed theorem trans_disj_wf_implies_wf: assumes "trans r" and "disj_wf r" shows "wf r" proof (simp only: wf_iff_no_infinite_down_chain, rule notI) assume "∃s. ∀i. (s (Suc i), s i) ∈ r" then obtain s where sSuc: "∀i. (s (Suc i), s i) ∈ r" .. from ‹disj_wf r› obtain T and n :: nat where wfT: "∀k<n. wf(T k)" and r: "r = (⋃k<n. T k)" by (auto simp add: disj_wf_def) have s_in_T: "∃k. (s j, s i) ∈ T k ∧ k<n" if "i < j" for i j proof - from ‹i < j› have "(s j, s i) ∈ r" proof (induct rule: less_Suc_induct) case 1 then show ?case by (simp add: sSuc) next case 2 with ‹trans r› show ?case unfolding trans_def by blast qed then show ?thesis by (auto simp add: r) qed have "i < j ⟹ transition_idx s T {i, j} < n" for i j using s_in_T transition_idx_less by blast then have trless: "i ≠ j ⟹ transition_idx s T {i, j} < n" for i j by (metis doubleton_eq_iff less_linear) have "∃K k. K ⊆ UNIV ∧ infinite K ∧ k < n ∧ (∀i∈K. ∀j∈K. i ≠ j ⟶ transition_idx s T {i, j} = k)" by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat) then obtain K and k where infK: "infinite K" and "k < n" and allk: "∀i∈K. ∀j∈K. i ≠ j ⟶ transition_idx s T {i, j} = k" by auto have "(s (enumerate K (Suc m)), s (enumerate K m)) ∈ T k" for m :: nat proof - let ?j = "enumerate K (Suc m)" let ?i = "enumerate K m" have ij: "?i < ?j" by (simp add: enumerate_step infK) have "?j ∈ K" "?i ∈ K" by (simp_all add: enumerate_in_set infK) with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk) from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) ∈ T k'" "k'<n" by blast then show "(s ?j, s ?i) ∈ T k" by (simp add: k transition_idx_in ij) qed then have "¬ wf (T k)" unfolding wf_iff_no_infinite_down_chain by iprover with wfT ‹k < n› show False by blast qed end