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