19944

1 
(* Title: HOL/Library/Ramsey.thy


2 
ID: $Id$


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


4 
*)


5 


6 
header "Ramsey's Theorem"


7 

20810

8 
theory Ramsey imports Main Infinite_Set begin

19944

9 


10 

19954

11 
subsection{*Preliminaries*}


12 


13 
subsubsection{*``Axiom'' of Dependent Choice*}

19944

14 

19948

15 
consts choice :: "('a => bool) => ('a * 'a) set => nat => 'a"

19944

16 
{*An integerindexed chain of choices*}


17 
primrec


18 
choice_0: "choice P r 0 = (SOME x. P x)"


19 


20 
choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"


21 


22 


23 
lemma choice_n:


24 
assumes P0: "P x0"


25 
and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"


26 
shows "P (choice P r n)"

19948

27 
proof (induct n)


28 
case 0 show ?case by (force intro: someI P0)


29 
next


30 
case Suc thus ?case by (auto intro: someI2_ex [OF Pstep])


31 
qed

19944

32 


33 
lemma dependent_choice:


34 
assumes trans: "trans r"


35 
and P0: "P x0"


36 
and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"

19954

37 
obtains f :: "nat => 'a" where


38 
"!!n. P (f n)" and "!!n m. n < m ==> (f n, f m) \<in> r"


39 
proof


40 
fix n


41 
show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])

19944

42 
next


43 
have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"


44 
using Pstep [OF choice_n [OF P0 Pstep]]


45 
by (auto intro: someI2_ex)

19954

46 
fix n m :: nat


47 
assume less: "n < m"


48 
show "(choice P r n, choice P r m) \<in> r" using PSuc


49 
by (auto intro: less_Suc_induct [OF less] transD [OF trans])


50 
qed

19944

51 


52 

19954

53 
subsubsection {*Partitions of a Set*}

19944

54 

19948

55 
definition


56 
part :: "nat => nat => 'a set => ('a set => nat) => bool"

19944

57 
{*the function @{term f} partitions the @{term r}subsets of the typically


58 
infinite set @{term Y} into @{term s} distinct categories.*}

21634

59 
where

19948

60 
"part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r > f X < s)"

19944

61 


62 
text{*For induction, we decrease the value of @{term r} in partitions.*}


63 
lemma part_Suc_imp_part:


64 
"[ infinite Y; part (Suc r) s Y f; y \<in> Y ]


65 
==> part r s (Y  {y}) (%u. f (insert y u))"


66 
apply(simp add: part_def, clarify)


67 
apply(drule_tac x="insert y X" in spec)


68 
apply(force simp:card_Diff_singleton_if)


69 
done


70 


71 
lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"

19948

72 
unfolding part_def by blast

19944

73 


74 


75 
subsection {*Ramsey's Theorem: Infinitary Version*}


76 

19954

77 
lemma Ramsey_induction:


78 
fixes s and r::nat

19944

79 
shows


80 
"!!(YY::'a set) (f::'a set => nat).


81 
[infinite YY; part r s YY f]


82 
==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &


83 
(\<forall>X. X \<subseteq> Y' & finite X & card X = r > f X = t')"


84 
proof (induct r)


85 
case 0


86 
thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)


87 
next


88 
case (Suc r)


89 
show ?case


90 
proof 


91 
from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast


92 
let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"


93 
let ?propr = "%(y,Y,t).


94 
y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s


95 
& (\<forall>X. X\<subseteq>Y & finite X & card X = r > (f o insert y) X = t)"


96 
have infYY': "infinite (YY{yy})" using Suc.prems by auto


97 
have partf': "part r s (YY  {yy}) (f \<circ> insert yy)"


98 
by (simp add: o_def part_Suc_imp_part yy Suc.prems)


99 
have transr: "trans ?ramr" by (force simp add: trans_def)


100 
from Suc.hyps [OF infYY' partf']


101 
obtain Y0 and t0


102 
where "Y0 \<subseteq> YY  {yy}" "infinite Y0" "t0 < s"


103 
"\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"


104 
by blast


105 
with yy have propr0: "?propr(yy,Y0,t0)" by blast


106 
have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"


107 
proof 


108 
fix x


109 
assume px: "?propr x" thus "?thesis x"


110 
proof (cases x)


111 
case (fields yx Yx tx)


112 
then obtain yx' where yx': "yx' \<in> Yx" using px


113 
by (blast dest: infinite_imp_nonempty)


114 
have infYx': "infinite (Yx{yx'})" using fields px by auto


115 
with fields px yx' Suc.prems


116 
have partfx': "part r s (Yx  {yx'}) (f \<circ> insert yx')"


117 
by (simp add: o_def part_Suc_imp_part part_subset [where ?YY=YY])


118 
from Suc.hyps [OF infYx' partfx']


119 
obtain Y' and t'


120 
where Y': "Y' \<subseteq> Yx  {yx'}" "infinite Y'" "t' < s"


121 
"\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"


122 
by blast


123 
show ?thesis


124 
proof


125 
show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"


126 
using fields Y' yx' px by blast


127 
qed


128 
qed


129 
qed


130 
from dependent_choice [OF transr propr0 proprstep]

19946

131 
obtain g where pg: "!!n::nat. ?propr (g n)"

19954

132 
and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast

19944

133 
let ?gy = "(\<lambda>n. let (y,Y,t) = g n in y)"


134 
let ?gt = "(\<lambda>n. let (y,Y,t) = g n in t)"


135 
have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"


136 
proof (intro exI subsetI)


137 
fix x


138 
assume "x \<in> range ?gt"


139 
then obtain n where "x = ?gt n" ..


140 
with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto


141 
qed

20810

142 
have "finite (range ?gt)"


143 
by (simp add: finite_nat_iff_bounded rangeg)

19944

144 
then obtain s' and n'

20810

145 
where s': "s' = ?gt n'"


146 
and infeqs': "infinite {n. ?gt n = s'}"


147 
by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)

19944

148 
with pg [of n'] have less': "s'<s" by (cases "g n'") auto


149 
have inj_gy: "inj ?gy"


150 
proof (rule linorder_injI)

19949

151 
fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"

19948

152 
using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto

19944

153 
qed


154 
show ?thesis


155 
proof (intro exI conjI)


156 
show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg


157 
by (auto simp add: Let_def split_beta)


158 
show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'


159 
by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)


160 
show "s' < s" by (rule less')


161 
show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r


162 
> f X = s'"


163 
proof 


164 
{fix X


165 
assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"


166 
and cardX: "finite X" "card X = Suc r"


167 
then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"


168 
by (auto simp add: subset_image_iff)


169 
with cardX have "AA\<noteq>{}" by auto


170 
hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)


171 
have "f X = s'"


172 
proof (cases "g (LEAST x. x \<in> AA)")


173 
case (fields ya Ya ta)


174 
with AAleast Xeq


175 
have ya: "ya \<in> X" by (force intro!: rev_image_eqI)


176 
hence "f X = f (insert ya (X  {ya}))" by (simp add: insert_absorb)


177 
also have "... = ta"


178 
proof 


179 
have "X  {ya} \<subseteq> Ya"


180 
proof

19954

181 
fix x assume x: "x \<in> X  {ya}"

19944

182 
then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"


183 
by (auto simp add: Xeq)


184 
hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto


185 
hence lessa': "(LEAST x. x \<in> AA) < a'"


186 
using Least_le [of "%x. x \<in> AA", OF a'] by arith


187 
show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto


188 
qed


189 
moreover


190 
have "card (X  {ya}) = r"


191 
by (simp add: card_Diff_singleton_if cardX ya)


192 
ultimately show ?thesis


193 
using pg [of "LEAST x. x \<in> AA"] fields cardX

19946

194 
by (clarsimp simp del:insert_Diff_single)

19944

195 
qed


196 
also have "... = s'" using AA AAleast fields by auto


197 
finally show ?thesis .


198 
qed}


199 
thus ?thesis by blast


200 
qed


201 
qed


202 
qed


203 
qed


204 


205 


206 
theorem Ramsey:

19949

207 
fixes s r :: nat and Z::"'a set" and f::"'a set => nat"

19944

208 
shows


209 
"[infinite Z;


210 
\<forall>X. X \<subseteq> Z & finite X & card X = r > f X < s]


211 
==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s


212 
& (\<forall>X. X \<subseteq> Y & finite X & card X = r > f X = t)"

19954

213 
by (blast intro: Ramsey_induction [unfolded part_def])


214 


215 


216 
corollary Ramsey2:


217 
fixes s::nat and Z::"'a set" and f::"'a set => nat"


218 
assumes infZ: "infinite Z"


219 
and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x\<noteq>y > f{x,y} < s"


220 
shows


221 
"\<exists>Y t. Y \<subseteq> Z & infinite Y & t < s & (\<forall>x\<in>Y. \<forall>y\<in>Y. x\<noteq>y > f{x,y} = t)"


222 
proof 


223 
have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 > f X < s"


224 
by (auto simp add: numeral_2_eq_2 card_2_eq part)


225 
obtain Y t


226 
where "Y \<subseteq> Z" "infinite Y" "t < s"


227 
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 > f X = t)"


228 
by (insert Ramsey [OF infZ part2]) auto


229 
moreover from this have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto


230 
ultimately show ?thesis by iprover


231 
qed


232 


233 


234 


235 


236 
subsection {*Disjunctive WellFoundedness*}


237 


238 
text{*An application of Ramsey's theorem to program termination. See


239 


240 
Andreas Podelski and Andrey Rybalchenko, Transition Invariants, 19th Annual


241 
IEEE Symposium on Logic in Computer Science (LICS'04), pages 3241 (2004).


242 
*}


243 

20810

244 
definition

19954

245 
disj_wf :: "('a * 'a)set => bool"

21634

246 
where

20810

247 
"disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"

19954

248 

21634

249 
definition

19954

250 
transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"

21634

251 
where

20810

252 
"transition_idx s T A =


253 
(LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"

19954

254 


255 


256 
lemma transition_idx_less:


257 
"[i<j; (s j, s i) \<in> T k; k<n] ==> transition_idx s T {i,j} < n"


258 
apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)


259 
apply (simp add: transition_idx_def, blast intro: Least_le)


260 
done


261 


262 
lemma transition_idx_in:


263 
"[i<j; (s j, s i) \<in> T k] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"


264 
apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR


265 
cong: conj_cong)


266 
apply (erule LeastI)


267 
done


268 


269 
text{*To be equal to the union of some wellfounded relations is equivalent


270 
to being the subset of such a union.*}


271 
lemma disj_wf:


272 
"disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"


273 
apply (auto simp add: disj_wf_def)


274 
apply (rule_tac x="%i. T i Int r" in exI)


275 
apply (rule_tac x=n in exI)


276 
apply (force simp add: wf_Int1)


277 
done


278 


279 
theorem trans_disj_wf_implies_wf:


280 
assumes transr: "trans r"


281 
and dwf: "disj_wf(r)"


282 
shows "wf r"


283 
proof (simp only: wf_iff_no_infinite_down_chain, rule notI)


284 
assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"


285 
then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..


286 
have s: "!!i j. i < j ==> (s j, s i) \<in> r"


287 
proof 


288 
fix i and j::nat


289 
assume less: "i<j"


290 
thus "(s j, s i) \<in> r"


291 
proof (rule less_Suc_induct)


292 
show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)


293 
show "\<And>i j k. \<lbrakk>(s j, s i) \<in> r; (s k, s j) \<in> r\<rbrakk> \<Longrightarrow> (s k, s i) \<in> r"


294 
using transr by (unfold trans_def, blast)


295 
qed


296 
qed


297 
from dwf


298 
obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"


299 
by (auto simp add: disj_wf_def)


300 
have s_in_T: "\<And>i j. i<j ==> \<exists>k. (s j, s i) \<in> T k & k<n"


301 
proof 


302 
fix i and j::nat


303 
assume less: "i<j"


304 
hence "(s j, s i) \<in> r" by (rule s [of i j])


305 
thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)


306 
qed


307 
have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"


308 
apply (auto simp add: linorder_neq_iff)


309 
apply (blast dest: s_in_T transition_idx_less)


310 
apply (subst insert_commute)


311 
apply (blast dest: s_in_T transition_idx_less)


312 
done


313 
have


314 
"\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &


315 
(\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j > transition_idx s T {i,j} = k)"


316 
by (rule Ramsey2) (auto intro: trless nat_infinite)


317 
then obtain K and k


318 
where infK: "infinite K" and less: "k < n" and


319 
allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j > transition_idx s T {i,j} = k"


320 
by auto


321 
have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"


322 
proof


323 
fix m::nat


324 
let ?j = "enumerate K (Suc m)"


325 
let ?i = "enumerate K m"


326 
have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)


327 
have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)


328 
have ij: "?i < ?j" by (simp add: enumerate_step infK)


329 
have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij


330 
by (simp add: allk)


331 
obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"


332 
using s_in_T [OF ij] by blast


333 
thus "(s ?j, s ?i) \<in> T k"


334 
by (simp add: ijk [symmetric] transition_idx_in ij)


335 
qed


336 
hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)


337 
thus False using wfT less by blast


338 
qed


339 

19944

340 


341 
end
