(* Title: HOL/Library/Ramsey.thy Author: Tom Ridge. Converted to structured Isar by L C Paulson *) section ‹Ramsey's Theorem› theory Ramsey imports Infinite_Set begin subsection ‹Finite Ramsey theorem(s)› text ‹ To distinguish the finite and infinite ones, lower and upper case names are used. 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)" (is "∃r≥1. ?R m n r") proof (induct k ≡ "m + n" arbitrary: m n) case 0 show ?case (is "EX r. ?Q r") proof from 0 show "?Q 1" by (clarsimp simp: indep_def) (metis card.empty emptyE empty_subsetI) qed next case (Suc k) consider "m = 0 ∨ n = 0" | "m ≠ 0" "n ≠ 0" by auto then show ?case (is "EX r. ?Q r") proof cases case 1 then have "?Q 1" by (simp add: clique_def) (meson card_empty empty_iff empty_subsetI indep_def) then show ?thesis .. next case 2 with Suc(2) have "k = (m - 1) + n" "k = m + (n - 1)" by auto from this [THEN Suc(1)] obtain r1 r2 where "r1 ≥ 1" "r2 ≥ 1" "?R (m - 1) n r1" "?R m (n - 1) r2" by auto then have "r1 + r2 ≥ 1" by arith moreover have "?R m n (r1 + r2)" (is "∀V E. _ ⟶ ?EX V E m n") proof clarify fix V :: "'a set" fix E :: "'a set set" assume "finite V" "r1 + r2 ≤ card V" with ‹r1 ≥ 1› have "V ≠ {}" by auto then obtain v where "v ∈ V" by blast let ?M = "{w ∈ V. w ≠ v ∧ {v, w} ∈ E}" let ?N = "{w ∈ V. w ≠ v ∧ {v, w} ∉ E}" from ‹v ∈ V› have "V = insert v (?M ∪ ?N)" by auto then have "card V = card (insert v (?M ∪ ?N))" by metis also from ‹finite V› have "… = card ?M + card ?N + 1" by (fastforce intro: card_Un_disjoint) finally have "card V = card ?M + card ?N + 1" . with ‹r1 + r2 ≤ card V› have "r1 + r2 ≤ card ?M + card ?N + 1" by simp then consider "r1 ≤ card ?M" | "r2 ≤ card ?N" by arith then show "?EX V E m n" proof cases case 1 from ‹finite V› have "finite ?M" by auto with ‹?R (m - 1) n r1› and 1 have "?EX ?M E (m - 1) n" by blast then obtain R where "R ⊆ ?M" "v ∉ R" and CI: "card R = m - 1 ∧ clique R E ∨ card R = n ∧ indep R E" (is "?C ∨ ?I") by blast from ‹R ⊆ ?M› have "R ⊆ V" by auto with ‹finite V› have "finite R" by (metis finite_subset) from CI show ?thesis proof assume "?I" with ‹R ⊆ V› show ?thesis by blast next assume "?C" with ‹R ⊆ ?M› have *: "clique (insert v R) E" by (auto simp: clique_def insert_commute) from ‹?C› ‹finite R› ‹v ∉ R› ‹m ≠ 0› have "card (insert v R) = m" by simp with ‹R ⊆ V› ‹v ∈ V› * show ?thesis by (metis insert_subset) qed next case 2 from ‹finite V› have "finite ?N" by auto with ‹?R m (n - 1) r2› 2 have "?EX ?N E m (n - 1)" by blast then obtain R where "R ⊆ ?N" "v ∉ R" and CI: "card R = m ∧ clique R E ∨ card R = n - 1 ∧ indep R E" (is "?C ∨ ?I") by blast from ‹R ⊆ ?N› have "R ⊆ V" by auto with ‹finite V› have "finite R" by (metis finite_subset) from CI show ?thesis proof assume "?C" with ‹R ⊆ V› show ?thesis by blast next assume "?I" with ‹R ⊆ ?N› have *: "indep (insert v R) E" by (auto simp: indep_def insert_commute) from ‹?I› ‹finite R› ‹v ∉ R› ‹n ≠ 0› have "card (insert v R) = n" by simp with ‹R ⊆ V› ‹v ∈ V› * show ?thesis by (metis insert_subset) qed qed qed ultimately show ?thesis by blast qed 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 ‹Partitions of a Set› definition part :: "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 r s Y f ⟷ (∀X. X ⊆ Y ∧ finite X ∧ card X = r ⟶ f X < s)" text ‹For induction, we decrease the value of @{term r} in partitions.› lemma part_Suc_imp_part: "⟦infinite Y; part (Suc r) s Y f; y ∈ Y⟧ ⟹ part r s (Y - {y}) (λu. f (insert y u))" apply (simp add: part_def) apply clarify apply (drule_tac x="insert y X" in spec) apply force done lemma part_subset: "part r s YY f ⟹ Y ⊆ YY ⟹ part r s Y f" unfolding part_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 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_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 r s (YY - {yy}) (f ∘ insert yy)" by (simp add: o_def part_Suc_imp_part 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 r s (Yx - {yx'}) (f ∘ insert yx')" by (simp add: o_def part_Suc_imp_part part_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 have "finite (range ?gt)" by (simp add: finite_nat_iff_bounded rangeg) 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_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 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))" apply (auto simp add: disj_wf_def) apply (rule_tac x="λi. T i Int r" in exI) apply (rule_tac x=n in exI) apply (force simp add: wf_Int1) done 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 trless: "i ≠ j ⟹ transition_idx s T {i, j} < n" for i j apply (auto simp add: linorder_neq_iff) apply (blast dest: s_in_T transition_idx_less) apply (subst insert_commute) apply (blast dest: s_in_T transition_idx_less) done 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 fast with wfT ‹k < n› show False by blast qed end