src/HOL/Library/Ramsey.thy
 author hoelzl Tue Jul 19 14:37:49 2011 +0200 (2011-07-19) changeset 43922 c6f35921056e parent 40695 1b2573c3b222 child 44890 22f665a2e91c permissions -rw-r--r--
add nat => enat coercion
1 (*  Title:      HOL/Library/Ramsey.thy
2     Author:     Tom Ridge.  Converted to structured Isar by L C Paulson
3 *)
5 header "Ramsey's Theorem"
7 theory Ramsey
8 imports Main Infinite_Set
9 begin
11 subsection{* Finite Ramsey theorem(s) *}
13 text{* To distinguish the finite and infinite ones, lower and upper case
14 names are used.
16 This is the most basic version in terms of cliques and independent
17 sets, i.e. the version for graphs and 2 colours. *}
19 definition "clique V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> {v,w} : E)"
20 definition "indep V E = (\<forall>v\<in>V. \<forall>w\<in>V. v\<noteq>w \<longrightarrow> \<not> {v,w} : E)"
22 lemma ramsey2:
23   "\<exists>r\<ge>1. \<forall> (V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow>
24   (\<exists> R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)"
25   (is "\<exists>r\<ge>1. ?R m n r")
26 proof(induct k == "m+n" arbitrary: m n)
27   case 0
28   show ?case (is "EX r. ?R r")
29   proof
30     show "?R 1" using 0
31       by (clarsimp simp: indep_def)(metis card.empty emptyE empty_subsetI)
32   qed
33 next
34   case (Suc k)
35   { assume "m=0"
36     have ?case (is "EX r. ?R r")
37     proof
38       show "?R 1" using `m=0`
39         by (simp add:clique_def)(metis card.empty emptyE empty_subsetI)
40     qed
41   } moreover
42   { assume "n=0"
43     have ?case (is "EX r. ?R r")
44     proof
45       show "?R 1" using `n=0`
46         by (simp add:indep_def)(metis card.empty emptyE empty_subsetI)
47     qed
48   } moreover
49   { assume "m\<noteq>0" "n\<noteq>0"
50     hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
51     from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
52     obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
53       by auto
54     hence "r1+r2 \<ge> 1" by arith
55     moreover
56     have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
57     proof clarify
58       fix V :: "'a set" and E :: "'a set set"
59       assume "finite V" "r1+r2 \<le> card V"
60       with `r1\<ge>1` have "V \<noteq> {}" by auto
61       then obtain v where "v : V" by blast
62       let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
63       let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
64       have "V = insert v (?M \<union> ?N)" using `v : V` by auto
65       hence "card V = card(insert v (?M \<union> ?N))" by metis
66       also have "\<dots> = card ?M + card ?N + 1" using `finite V`
67         by(fastsimp intro: card_Un_disjoint)
68       finally have "card V = card ?M + card ?N + 1" .
69       hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
70       hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
71       moreover
72       { assume "r1 \<le> card ?M"
73         moreover have "finite ?M" using `finite V` by auto
74         ultimately have "?EX ?M E (m - 1) n" using `?R (m - 1) n r1` by blast
75         then obtain R where "R \<subseteq> ?M" "v ~: R" and
76           CI: "card R = m - 1 \<and> clique R E \<or>
77                card R = n \<and> indep R E" (is "?C \<or> ?I")
78           by blast
79         have "R <= V" using `R <= ?M` by auto
80         have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
81         { assume "?I"
82           with `R <= V` have "?EX V E m n" by blast
83         } moreover
84         { assume "?C"
85           hence "clique (insert v R) E" using `R <= ?M`
86            by(auto simp:clique_def insert_commute)
87           moreover have "card(insert v R) = m"
88             using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
89           ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
90         } ultimately have "?EX V E m n" using CI by blast
91       } moreover
92       { assume "r2 \<le> card ?N"
93         moreover have "finite ?N" using `finite V` by auto
94         ultimately have "?EX ?N E m (n - 1)" using `?R m (n - 1) r2` by blast
95         then obtain R where "R \<subseteq> ?N" "v ~: R" and
96           CI: "card R = m \<and> clique R E \<or>
97                card R = n - 1 \<and> indep R E" (is "?C \<or> ?I")
98           by blast
99         have "R <= V" using `R <= ?N` by auto
100         have "finite R" using `finite V` `R \<subseteq> V` by (metis finite_subset)
101         { assume "?C"
102           with `R <= V` have "?EX V E m n" by blast
103         } moreover
104         { assume "?I"
105           hence "indep (insert v R) E" using `R <= ?N`
106             by(auto simp:indep_def insert_commute)
107           moreover have "card(insert v R) = n"
108             using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
109           ultimately have "?EX V E m n" using `R <= V` `v : V` by blast
110         } ultimately have "?EX V E m n" using CI by blast
111       } ultimately show "?EX V E m n" by blast
112     qed
113     ultimately have ?case by blast
114   } ultimately show ?case by blast
115 qed
118 subsection {* Preliminaries *}
120 subsubsection {* ``Axiom'' of Dependent Choice *}
122 primrec choice :: "('a => bool) => ('a * 'a) set => nat => 'a" where
123   --{*An integer-indexed chain of choices*}
124     choice_0:   "choice P r 0 = (SOME x. P x)"
125   | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
127 lemma choice_n:
128   assumes P0: "P x0"
129       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
130   shows "P (choice P r n)"
131 proof (induct n)
132   case 0 show ?case by (force intro: someI P0)
133 next
134   case Suc thus ?case by (auto intro: someI2_ex [OF Pstep])
135 qed
137 lemma dependent_choice:
138   assumes trans: "trans r"
139       and P0: "P x0"
140       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
141   obtains f :: "nat => 'a" where
142     "!!n. P (f n)" and "!!n m. n < m ==> (f n, f m) \<in> r"
143 proof
144   fix n
145   show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
146 next
147   have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
148     using Pstep [OF choice_n [OF P0 Pstep]]
149     by (auto intro: someI2_ex)
150   fix n m :: nat
151   assume less: "n < m"
152   show "(choice P r n, choice P r m) \<in> r" using PSuc
153     by (auto intro: less_Suc_induct [OF less] transD [OF trans])
154 qed
157 subsubsection {* Partitions of a Set *}
159 definition
160   part :: "nat => nat => 'a set => ('a set => nat) => bool"
161   --{*the function @{term f} partitions the @{term r}-subsets of the typically
162        infinite set @{term Y} into @{term s} distinct categories.*}
163 where
164   "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
166 text{*For induction, we decrease the value of @{term r} in partitions.*}
167 lemma part_Suc_imp_part:
168      "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
169       ==> part r s (Y - {y}) (%u. f (insert y u))"
170   apply(simp add: part_def, clarify)
171   apply(drule_tac x="insert y X" in spec)
172   apply(force)
173   done
175 lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
176   unfolding part_def by blast
179 subsection {* Ramsey's Theorem: Infinitary Version *}
181 lemma Ramsey_induction:
182   fixes s and r::nat
183   shows
184   "!!(YY::'a set) (f::'a set => nat).
185       [|infinite YY; part r s YY f|]
186       ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
187                   (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
188 proof (induct r)
189   case 0
190   thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
191 next
192   case (Suc r)
193   show ?case
194   proof -
195     from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
196     let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
197     let ?propr = "%(y,Y,t).
198                  y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
199                  & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
200     have infYY': "infinite (YY-{yy})" using Suc.prems by auto
201     have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
202       by (simp add: o_def part_Suc_imp_part yy Suc.prems)
203     have transr: "trans ?ramr" by (force simp add: trans_def)
204     from Suc.hyps [OF infYY' partf']
205     obtain Y0 and t0
206     where "Y0 \<subseteq> YY - {yy}"  "infinite Y0"  "t0 < s"
207           "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
208         by blast
209     with yy have propr0: "?propr(yy,Y0,t0)" by blast
210     have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
211     proof -
212       fix x
213       assume px: "?propr x" thus "?thesis x"
214       proof (cases x)
215         case (fields yx Yx tx)
216         then obtain yx' where yx': "yx' \<in> Yx" using px
217                by (blast dest: infinite_imp_nonempty)
218         have infYx': "infinite (Yx-{yx'})" using fields px by auto
219         with fields px yx' Suc.prems
220         have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
221           by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
222         from Suc.hyps [OF infYx' partfx']
223         obtain Y' and t'
224         where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
225                "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
226             by blast
227         show ?thesis
228         proof
229           show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
230             using fields Y' yx' px by blast
231         qed
232       qed
233     qed
234     from dependent_choice [OF transr propr0 proprstep]
235     obtain g where pg: "!!n::nat.  ?propr (g n)"
236       and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
237     let ?gy = "fst o g"
238     let ?gt = "snd o snd o g"
239     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
240     proof (intro exI subsetI)
241       fix x
242       assume "x \<in> range ?gt"
243       then obtain n where "x = ?gt n" ..
244       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
245     qed
246     have "finite (range ?gt)"
247       by (simp add: finite_nat_iff_bounded rangeg)
248     then obtain s' and n'
249       where s': "s' = ?gt n'"
250         and infeqs': "infinite {n. ?gt n = s'}"
251       by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
252     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
253     have inj_gy: "inj ?gy"
254     proof (rule linorder_injI)
255       fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
256         using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
257     qed
258     show ?thesis
259     proof (intro exI conjI)
260       show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
261         by (auto simp add: Let_def split_beta)
262       show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
263         by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
264       show "s' < s" by (rule less')
265       show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
266           --> f X = s'"
267       proof -
268         {fix X
269          assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
270             and cardX: "finite X" "card X = Suc r"
271          then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
272              by (auto simp add: subset_image_iff)
273          with cardX have "AA\<noteq>{}" by auto
274          hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
275          have "f X = s'"
276          proof (cases "g (LEAST x. x \<in> AA)")
277            case (fields ya Ya ta)
278            with AAleast Xeq
279            have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
280            hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
281            also have "... = ta"
282            proof -
283              have "X - {ya} \<subseteq> Ya"
284              proof
285                fix x assume x: "x \<in> X - {ya}"
286                then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
287                  by (auto simp add: Xeq)
288                hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
289                hence lessa': "(LEAST x. x \<in> AA) < a'"
290                  using Least_le [of "%x. x \<in> AA", OF a'] by arith
291                show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
292              qed
293              moreover
294              have "card (X - {ya}) = r"
295                by (simp add: cardX ya)
296              ultimately show ?thesis
297                using pg [of "LEAST x. x \<in> AA"] fields cardX
298                by (clarsimp simp del:insert_Diff_single)
299            qed
300            also have "... = s'" using AA AAleast fields by auto
301            finally show ?thesis .
302          qed}
303         thus ?thesis by blast
304       qed
305     qed
306   qed
307 qed
310 theorem Ramsey:
311   fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
312   shows
313    "[|infinite Z;
314       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
315   ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
316             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
317 by (blast intro: Ramsey_induction [unfolded part_def])
320 corollary Ramsey2:
321   fixes s::nat and Z::"'a set" and f::"'a set => nat"
322   assumes infZ: "infinite Z"
323       and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x\<noteq>y --> f{x,y} < s"
324   shows
325    "\<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)"
326 proof -
327   have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
328     using part by (fastsimp simp add: eval_nat_numeral card_Suc_eq)
329   obtain Y t
330     where "Y \<subseteq> Z" "infinite Y" "t < s"
331           "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
332     by (insert Ramsey [OF infZ part2]) auto
333   moreover from this have  "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
334   ultimately show ?thesis by iprover
335 qed
338 subsection {* Disjunctive Well-Foundedness *}
340 text {*
341   An application of Ramsey's theorem to program termination. See
342   \cite{Podelski-Rybalchenko}.
343 *}
345 definition
346   disj_wf         :: "('a * 'a)set => bool"
347 where
348   "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
350 definition
351   transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
352 where
353   "transition_idx s T A =
354     (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
357 lemma transition_idx_less:
358     "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
359 apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
360 apply (simp add: transition_idx_def, blast intro: Least_le)
361 done
363 lemma transition_idx_in:
364     "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
365 apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
366             cong: conj_cong)
367 apply (erule LeastI)
368 done
370 text{*To be equal to the union of some well-founded relations is equivalent
371 to being the subset of such a union.*}
372 lemma disj_wf:
373      "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
374 apply (auto simp add: disj_wf_def)
375 apply (rule_tac x="%i. T i Int r" in exI)
376 apply (rule_tac x=n in exI)
377 apply (force simp add: wf_Int1)
378 done
380 theorem trans_disj_wf_implies_wf:
381   assumes transr: "trans r"
382       and dwf:    "disj_wf(r)"
383   shows "wf r"
384 proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
385   assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
386   then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
387   have s: "!!i j. i < j ==> (s j, s i) \<in> r"
388   proof -
389     fix i and j::nat
390     assume less: "i<j"
391     thus "(s j, s i) \<in> r"
392     proof (rule less_Suc_induct)
393       show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
394       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"
395         using transr by (unfold trans_def, blast)
396     qed
397   qed
398   from dwf
399   obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
400     by (auto simp add: disj_wf_def)
401   have s_in_T: "\<And>i j. i<j ==> \<exists>k. (s j, s i) \<in> T k & k<n"
402   proof -
403     fix i and j::nat
404     assume less: "i<j"
405     hence "(s j, s i) \<in> r" by (rule s [of i j])
406     thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
407   qed
408   have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
409     apply (auto simp add: linorder_neq_iff)
410     apply (blast dest: s_in_T transition_idx_less)
411     apply (subst insert_commute)
412     apply (blast dest: s_in_T transition_idx_less)
413     done
414   have
415    "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
416           (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
417     by (rule Ramsey2) (auto intro: trless nat_infinite)
418   then obtain K and k
419     where infK: "infinite K" and less: "k < n" and
420           allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
421     by auto
422   have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"
423   proof
424     fix m::nat
425     let ?j = "enumerate K (Suc m)"
426     let ?i = "enumerate K m"
427     have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
428     have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
429     have ij: "?i < ?j" by (simp add: enumerate_step infK)
430     have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
431       by (simp add: allk)
432     obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
433       using s_in_T [OF ij] by blast
434     thus "(s ?j, s ?i) \<in> T k"
435       by (simp add: ijk [symmetric] transition_idx_in ij)
436   qed
437   hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
438   thus False using wfT less by blast
439 qed
441 end