src/HOL/Library/Ramsey.thy
 author Andreas Lochbihler Wed Feb 27 10:33:30 2013 +0100 (2013-02-27) changeset 51288 be7e9a675ec9 parent 46575 f1e387195a56 child 53374 a14d2a854c02 permissions -rw-r--r--
add wellorder instance for Numeral_Type (suggested by Jesus Aransay)
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     then have "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     then have "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       then have "card V = card(insert v (?M \<union> ?N))" by metis
66       also have "\<dots> = card ?M + card ?N + 1" using `finite V`
67         by(fastforce intro: card_Un_disjoint)
68       finally have "card V = card ?M + card ?N + 1" .
69       then have "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
70       then have "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           then have "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           then have "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 then show ?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 part :: "nat => nat => 'a set => ('a set => nat) => bool"
160   --{*the function @{term f} partitions the @{term r}-subsets of the typically
161        infinite set @{term Y} into @{term s} distinct categories.*}
162 where
163   "part r s Y f = (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X < s)"
165 text{*For induction, we decrease the value of @{term r} in partitions.*}
166 lemma part_Suc_imp_part:
167      "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
168       ==> part r s (Y - {y}) (%u. f (insert y u))"
169   apply(simp add: part_def, clarify)
170   apply(drule_tac x="insert y X" in spec)
171   apply(force)
172   done
174 lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
175   unfolding part_def by blast
178 subsection {* Ramsey's Theorem: Infinitary Version *}
180 lemma Ramsey_induction:
181   fixes s and r::nat
182   shows
183   "!!(YY::'a set) (f::'a set => nat).
184       [|infinite YY; part r s YY f|]
185       ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
186                   (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
187 proof (induct r)
188   case 0
189   then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
190 next
191   case (Suc r)
192   show ?case
193   proof -
194     from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
195     let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
196     let ?propr = "%(y,Y,t).
197                  y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
198                  & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
199     have infYY': "infinite (YY-{yy})" using Suc.prems by auto
200     have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
201       by (simp add: o_def part_Suc_imp_part yy Suc.prems)
202     have transr: "trans ?ramr" by (force simp add: trans_def)
203     from Suc.hyps [OF infYY' partf']
204     obtain Y0 and t0
205     where "Y0 \<subseteq> YY - {yy}"  "infinite Y0"  "t0 < s"
206           "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
207         by blast
208     with yy have propr0: "?propr(yy,Y0,t0)" by blast
209     have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
210     proof -
211       fix x
212       assume px: "?propr x" then show "?thesis x"
213       proof (cases x)
214         case (fields yx Yx tx)
215         then obtain yx' where yx': "yx' \<in> Yx" using px
216                by (blast dest: infinite_imp_nonempty)
217         have infYx': "infinite (Yx-{yx'})" using fields px by auto
218         with fields px yx' Suc.prems
219         have partfx': "part r s (Yx - {yx'}) (f \<circ> insert yx')"
220           by (simp add: o_def part_Suc_imp_part part_subset [where YY=YY and Y=Yx])
221         from Suc.hyps [OF infYx' partfx']
222         obtain Y' and t'
223         where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
224                "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
225             by blast
226         show ?thesis
227         proof
228           show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
229             using fields Y' yx' px by blast
230         qed
231       qed
232     qed
233     from dependent_choice [OF transr propr0 proprstep]
234     obtain g where pg: "!!n::nat.  ?propr (g n)"
235       and rg: "!!n m. n<m ==> (g n, g m) \<in> ?ramr" by blast
236     let ?gy = "fst o g"
237     let ?gt = "snd o snd o g"
238     have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}"
239     proof (intro exI subsetI)
240       fix x
241       assume "x \<in> range ?gt"
242       then obtain n where "x = ?gt n" ..
243       with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto
244     qed
245     have "finite (range ?gt)"
246       by (simp add: finite_nat_iff_bounded rangeg)
247     then obtain s' and n'
248       where s': "s' = ?gt n'"
249         and infeqs': "infinite {n. ?gt n = s'}"
250       by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: nat_infinite)
251     with pg [of n'] have less': "s'<s" by (cases "g n'") auto
252     have inj_gy: "inj ?gy"
253     proof (rule linorder_injI)
254       fix m m' :: nat assume less: "m < m'" show "?gy m \<noteq> ?gy m'"
255         using rg [OF less] pg [of m] by (cases "g m", cases "g m'") auto
256     qed
257     show ?thesis
258     proof (intro exI conjI)
259       show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
260         by (auto simp add: Let_def split_beta)
261       show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
262         by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
263       show "s' < s" by (rule less')
264       show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
265           --> f X = s'"
266       proof -
267         {fix X
268          assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
269             and cardX: "finite X" "card X = Suc r"
270          then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
271              by (auto simp add: subset_image_iff)
272          with cardX have "AA\<noteq>{}" by auto
273          then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
274          have "f X = s'"
275          proof (cases "g (LEAST x. x \<in> AA)")
276            case (fields ya Ya ta)
277            with AAleast Xeq
278            have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
279            then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
280            also have "... = ta"
281            proof -
282              have "X - {ya} \<subseteq> Ya"
283              proof
284                fix x assume x: "x \<in> X - {ya}"
285                then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
286                  by (auto simp add: Xeq)
287                then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
288                then have lessa': "(LEAST x. x \<in> AA) < a'"
289                  using Least_le [of "%x. x \<in> AA", OF a'] by arith
290                show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
291              qed
292              moreover
293              have "card (X - {ya}) = r"
294                by (simp add: cardX ya)
295              ultimately show ?thesis
296                using pg [of "LEAST x. x \<in> AA"] fields cardX
297                by (clarsimp simp del:insert_Diff_single)
298            qed
299            also have "... = s'" using AA AAleast fields by auto
300            finally show ?thesis .
301          qed}
302         then show ?thesis by blast
303       qed
304     qed
305   qed
306 qed
309 theorem Ramsey:
310   fixes s r :: nat and Z::"'a set" and f::"'a set => nat"
311   shows
312    "[|infinite Z;
313       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
314   ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
315             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
316 by (blast intro: Ramsey_induction [unfolded part_def])
319 corollary Ramsey2:
320   fixes s::nat and Z::"'a set" and f::"'a set => nat"
321   assumes infZ: "infinite Z"
322       and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x\<noteq>y --> f{x,y} < s"
323   shows
324    "\<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)"
325 proof -
326   have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
327     using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
328   obtain Y t
329     where "Y \<subseteq> Z" "infinite Y" "t < s"
330           "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
331     by (insert Ramsey [OF infZ part2]) auto
332   moreover from this have  "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
333   ultimately show ?thesis by iprover
334 qed
337 subsection {* Disjunctive Well-Foundedness *}
339 text {*
340   An application of Ramsey's theorem to program termination. See
341   \cite{Podelski-Rybalchenko}.
342 *}
344 definition disj_wf :: "('a * 'a)set => bool"
345   where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
347 definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
348   where
349     "transition_idx s T A =
350       (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
353 lemma transition_idx_less:
354     "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
355 apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
356 apply (simp add: transition_idx_def, blast intro: Least_le)
357 done
359 lemma transition_idx_in:
360     "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
361 apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
362             cong: conj_cong)
363 apply (erule LeastI)
364 done
366 text{*To be equal to the union of some well-founded relations is equivalent
367 to being the subset of such a union.*}
368 lemma disj_wf:
369      "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
370 apply (auto simp add: disj_wf_def)
371 apply (rule_tac x="%i. T i Int r" in exI)
372 apply (rule_tac x=n in exI)
373 apply (force simp add: wf_Int1)
374 done
376 theorem trans_disj_wf_implies_wf:
377   assumes transr: "trans r"
378       and dwf:    "disj_wf(r)"
379   shows "wf r"
380 proof (simp only: wf_iff_no_infinite_down_chain, rule notI)
381   assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r"
382   then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" ..
383   have s: "!!i j. i < j ==> (s j, s i) \<in> r"
384   proof -
385     fix i and j::nat
386     assume less: "i<j"
387     then show "(s j, s i) \<in> r"
388     proof (rule less_Suc_induct)
389       show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
390       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"
391         using transr by (unfold trans_def, blast)
392     qed
393   qed
394   from dwf
395   obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
396     by (auto simp add: disj_wf_def)
397   have s_in_T: "\<And>i j. i<j ==> \<exists>k. (s j, s i) \<in> T k & k<n"
398   proof -
399     fix i and j::nat
400     assume less: "i<j"
401     then have "(s j, s i) \<in> r" by (rule s [of i j])
402     then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
403   qed
404   have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
405     apply (auto simp add: linorder_neq_iff)
406     apply (blast dest: s_in_T transition_idx_less)
407     apply (subst insert_commute)
408     apply (blast dest: s_in_T transition_idx_less)
409     done
410   have
411    "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
412           (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
413     by (rule Ramsey2) (auto intro: trless nat_infinite)
414   then obtain K and k
415     where infK: "infinite K" and less: "k < n" and
416           allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
417     by auto
418   have "\<forall>m. (s (enumerate K (Suc m)), s(enumerate K m)) \<in> T k"
419   proof
420     fix m::nat
421     let ?j = "enumerate K (Suc m)"
422     let ?i = "enumerate K m"
423     have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
424     have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
425     have ij: "?i < ?j" by (simp add: enumerate_step infK)
426     have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
427       by (simp add: allk)
428     obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
429       using s_in_T [OF ij] by blast
430     then show "(s ?j, s ?i) \<in> T k"
431       by (simp add: ijk [symmetric] transition_idx_in ij)
432   qed
433   then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
434   then show False using wfT less by blast
435 qed
437 end