(* Title: HOL/Library/Ramsey.thy

Author: Tom Ridge. Converted to structured Isar by L C Paulson

*)

header "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 blast

} 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 blast

} 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 o 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 o 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 o 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 o 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: "!!n::nat. ?propr (g n)"

and rg: "!!n m. n<m ==> (g n, g m) ∈ ?ramr" 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: nat_infinite)

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 = (\<Union>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 ⊆ (\<Union>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 = (\<Union>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 nat_infinite)

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