(* Title: HOL/Library/Ramsey.thy Author: Tom Ridge. Converted to structured Isar by L C Paulson *) section "Ramsey's Theorem" theory Ramsey imports Main 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. ?R r") proof show "?R 1" using 0 by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI) qed next case (Suc k) { assume "m=0" have ?case (is "EX r. ?R r") proof show "?R 1" using ‹m=0› by (simp add:clique_def)(metis card.empty emptyE empty_subsetI) qed } moreover { assume "n=0" have ?case (is "EX r. ?R r") proof show "?R 1" using ‹n=0› by (simp add:indep_def)(metis card.empty emptyE empty_subsetI) qed } moreover { assume "m≠0" "n≠0" then have "k = (m - 1) + n" "k = m + (n - 1)" using ‹Suc k = m+n› by auto from Suc(1)[OF this(1)] Suc(1)[OF this(2)] 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 "ALL V E. _ ⟶ ?EX V E m n") proof clarify fix V :: "'a set" and 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}" have "V = insert v (?M ∪ ?N)" using ‹v : V› by auto then have "card V = card(insert v (?M ∪ ?N))" by metis also have "… = card ?M + card ?N + 1" using ‹finite V› by(fastforce intro: card_Un_disjoint) finally have "card V = card ?M + card ?N + 1" . then have "r1+r2 ≤ card ?M + card ?N + 1" using ‹r1+r2 ≤ card V› by simp then have "r1 ≤ card ?M ∨ r2 ≤ card ?N" by arith moreover { assume "r1 ≤ card ?M" moreover have "finite ?M" using ‹finite V› by auto ultimately have "?EX ?M E (m - 1) n" using ‹?R (m - 1) n r1› 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 have "R <= V" using ‹R <= ?M› by auto have "finite R" using ‹finite V› ‹R ⊆ V› by (metis finite_subset) { assume "?I" with ‹R <= V› have "?EX V E m n" by blast } moreover { assume "?C" then have "clique (insert v R) E" using ‹R <= ?M› by(auto simp:clique_def insert_commute) moreover have "card(insert v R) = m" using ‹?C› ‹finite R› ‹v ~: R› ‹m≠0› by simp ultimately have "?EX V E m n" using ‹R <= V› ‹v : V› by (metis insert_subset) } ultimately have "?EX V E m n" using CI by blast } moreover { assume "r2 ≤ card ?N" moreover have "finite ?N" using ‹finite V› by auto ultimately have "?EX ?N E m (n - 1)" using ‹?R m (n - 1) r2› 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 have "R <= V" using ‹R <= ?N› by auto have "finite R" using ‹finite V› ‹R ⊆ V› by (metis finite_subset) { assume "?C" with ‹R <= V› have "?EX V E m n" by blast } moreover { assume "?I" then have "indep (insert v R) E" using ‹R <= ?N› by(auto simp:indep_def insert_commute) moreover have "card(insert v R) = n" using ‹?I› ‹finite R› ‹v ~: R› ‹n≠0› by simp ultimately have "?EX V E m n" using ‹R <= V› ‹v : V› by (metis insert_subset) } ultimately have "?EX V E m n" using CI by blast } ultimately show "?EX V E m n" by blast qed ultimately have ?case by blast } ultimately show ?case by blast 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 have PSuc: "∀n. (choice P r n, choice P r (Suc n)) ∈ r" using Pstep [OF choice_n [OF P0 Pstep]] by (auto intro: someI2_ex) fix n m :: nat assume less: "n < m" show "(choice P r n, choice P r m) ∈ r" using PSuc by (auto intro: less_Suc_induct [OF less] 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, 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 and r::nat shows "!!(YY::'a set) (f::'a set => nat). [|infinite YY; part r s YY f|] ==> ∃Y' t'. Y' ⊆ YY & infinite Y' & t' < s & (∀X. X ⊆ Y' & finite X & card X = r --> f X = t')" proof (induct r) 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 o insert y) X = t)" have infYY': "infinite (YY-{yy})" using Suc.prems by auto have partf': "part r s (YY - {yy}) (f ∘ insert yy)" by (simp add: o_def part_Suc_imp_part yy Suc.prems) 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. X⊆Y0 ∧ finite X ∧ card X = r ⟶ (f ∘ insert yy) X = t0" by blast with yy have propr0: "?propr(yy,Y0,t0)" by blast have proprstep: "⋀x. ?propr x ⟹ ∃y. ?propr y ∧ (x, y) ∈ ?ramr" proof - fix x assume px: "?propr x" then show "?thesis x" proof (cases x) case (fields yx Yx tx) then obtain yx' where yx': "yx' ∈ Yx" using px by (blast dest: infinite_imp_nonempty) have infYx': "infinite (Yx-{yx'})" using fields px by auto with fields px 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. X⊆Y' ∧ finite X ∧ card X = r ⟶ (f ∘ insert yx') X = t'" by blast show ?thesis proof show "?propr (yx',Y',t') & (x, (yx',Y',t')) ∈ ?ramr" using fields Y' yx' px by blast qed qed 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 o g" let ?gt = "snd o snd o 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 less: "m < m'" show "?gy m ≠ ?gy m'" using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto qed show ?thesis proof (intro exI conjI) show "?gy ` {n. ?gt n = s'} ⊆ YY" using pg by (auto simp add: Let_def split_beta) show "infinite (?gy ` {n. ?gt n = s'})" using infeqs' 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 - {fix X assume "X ⊆ ?gy ` {n. ?gt n = s'}" and cardX: "finite X" "card X = Suc r" then 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) have "f X = s'" 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) then have "a' ≠ (LEAST x. x ∈ AA)" using x fields by auto then have lessa': "(LEAST x. x ∈ AA) < a'" using Least_le [of "%x. x ∈ AA", OF a'] by arith show "x ∈ Ya" using xeq fields rg [OF lessa'] by auto qed moreover have "card (X - {ya}) = r" by (simp add: cardX ya) ultimately show ?thesis using pg [of "LEAST x. x ∈ AA"] fields cardX by (clarsimp simp del:insert_Diff_single) qed also have "... = s'" using AA AAleast fields by auto finally show ?thesis . 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 - have part2: "∀X. X ⊆ Z & finite X & card X = 2 --> f X < s" using part 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: "[|i<j; (s j, s i) ∈ T k; k<n|] ==> transition_idx s T {i,j} < n" apply (subgoal_tac "transition_idx s T {i, j} ≤ k", simp) apply (simp add: transition_idx_def, blast intro: Least_le) done lemma transition_idx_in: "[|i<j; (s j, s i) ∈ T k|] ==> (s j, s i) ∈ T (transition_idx s T {i,j})" apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) apply (erule LeastI) done 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 transr: "trans r" and dwf: "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" .. have s: "!!i j. i < j ==> (s j, s i) ∈ r" proof - fix i and j::nat assume less: "i<j" then show "(s j, s i) ∈ r" proof (rule less_Suc_induct) show "⋀i. (s (Suc i), s i) ∈ r" by (simp add: sSuc) show "⋀i j k. ⟦(s j, s i) ∈ r; (s k, s j) ∈ r⟧ ⟹ (s k, s i) ∈ r" using transr by (unfold trans_def, blast) qed qed from dwf 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: "⋀i j. i<j ==> ∃k. (s j, s i) ∈ T k & k<n" proof - fix i and j::nat assume less: "i<j" then have "(s j, s i) ∈ r" by (rule s [of i j]) then show "∃k. (s j, s i) ∈ T k & k<n" by (auto simp add: r) qed have trless: "!!i j. i≠j ==> transition_idx s T {i,j} < n" 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 less: "k < n" and allk: "∀i∈K. ∀j∈K. i≠j --> transition_idx s T {i,j} = k" by auto have "∀m. (s (enumerate K (Suc m)), s(enumerate K m)) ∈ T k" proof fix m::nat let ?j = "enumerate K (Suc m)" let ?i = "enumerate K m" have jK: "?j ∈ K" by (simp add: enumerate_in_set infK) have iK: "?i ∈ K" by (simp add: enumerate_in_set infK) have ij: "?i < ?j" by (simp add: enumerate_step infK) have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij by (simp add: allk) obtain k' where "(s ?j, s ?i) ∈ T k'" "k'<n" using s_in_T [OF ij] by blast then show "(s ?j, s ?i) ∈ T k" by (simp add: ijk [symmetric] transition_idx_in ij) qed then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain) then show False using wfT less by blast qed end