author | paulson |
Mon, 17 Feb 2020 11:07:27 +0000 | |
changeset 71453 | 7b8a6840e85f |
parent 71449 | 3cf130a896a3 |
parent 71452 | 9edb7fb69bc2 |
child 71464 | 4a04b6bd628b |
permissions | -rw-r--r-- |
19944 | 1 |
(* Title: HOL/Library/Ramsey.thy |
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
2 |
Author: Tom Ridge. Full finite version by L C Paulson. |
19944 | 3 |
*) |
4 |
||
65075 | 5 |
section \<open>Ramsey's Theorem\<close> |
19944 | 6 |
|
25594 | 7 |
theory Ramsey |
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
8 |
imports Infinite_Set FuncSet |
25594 | 9 |
begin |
19944 | 10 |
|
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
11 |
subsection \<open>Preliminary definitions\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
12 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
13 |
subsubsection \<open>The $n$-element subsets of a set $A$\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
14 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
15 |
definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
16 |
where "nsets A n \<equiv> {N. N \<subseteq> A \<and> finite N \<and> card N = n}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
17 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
18 |
lemma nsets_mono: "A \<subseteq> B \<Longrightarrow> nsets A n \<subseteq> nsets B n" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
19 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
20 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
21 |
lemma nsets_2_eq: "nsets A 2 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. {{x, y}})" |
71449
3cf130a896a3
lemmas about "card A = 2"; prefer iff to implications
nipkow
parents:
71405
diff
changeset
|
22 |
by (auto simp: nsets_def card_2_iff) |
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
23 |
|
71452 | 24 |
lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})" |
25 |
by (auto simp: nsets_2_eq) |
|
26 |
||
27 |
lemma doubleton_in_nsets_2 [simp]: "{x,y} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y" |
|
28 |
by (auto simp: nsets_2_eq Set.doubleton_eq_iff) |
|
29 |
||
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
30 |
lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
31 |
apply (simp add: binomial_def nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
32 |
by (meson subset_eq_atLeast0_lessThan_finite) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
33 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
34 |
lemma nsets_eq_empty_iff: "nsets A r = {} \<longleftrightarrow> finite A \<and> card A < r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
35 |
unfolding nsets_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
36 |
proof (intro iffI conjI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
37 |
assume that: "{N. N \<subseteq> A \<and> finite N \<and> card N = r} = {}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
38 |
show "finite A" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
39 |
using infinite_arbitrarily_large that by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
40 |
then have "\<not> r \<le> card A" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
41 |
using that by (simp add: set_eq_iff) (metis finite_subset get_smaller_card [of A r]) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
42 |
then show "card A < r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
43 |
using not_less by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
44 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
45 |
show "{N. N \<subseteq> A \<and> finite N \<and> card N = r} = {}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
46 |
if "finite A \<and> card A < r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
47 |
using that card_mono leD by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
48 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
49 |
|
71452 | 50 |
lemma nsets_eq_empty: "\<lbrakk>finite A; card A < r\<rbrakk> \<Longrightarrow> nsets A r = {}" |
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
51 |
by (simp add: nsets_eq_empty_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
52 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
53 |
lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
54 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
55 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
56 |
lemma nsets_singleton_iff: "nsets {a} r = (if r=0 then {{}} else if r=1 then {{a}} else {})" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
57 |
by (auto simp: nsets_def card_gt_0_iff subset_singleton_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
58 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
59 |
lemma nsets_self [simp]: "nsets {..<m} m = {{..<m}}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
60 |
unfolding nsets_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
61 |
apply auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
62 |
by (metis add.left_neutral lessThan_atLeast0 lessThan_iff subset_card_intvl_is_intvl) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
63 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
64 |
lemma nsets_zero [simp]: "nsets A 0 = {{}}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
65 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
66 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
67 |
lemma nsets_one: "nsets A (Suc 0) = (\<lambda>x. {x}) ` A" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
68 |
using card_eq_SucD by (force simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
69 |
|
71405 | 70 |
lemma inj_on_nsets: |
71 |
assumes "inj_on f A" |
|
72 |
shows "inj_on (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>)" |
|
73 |
using assms unfolding nsets_def |
|
74 |
by (metis (no_types, lifting) inj_on_inverseI inv_into_image_cancel mem_Collect_eq) |
|
75 |
||
76 |
lemma bij_betw_nsets: |
|
77 |
assumes "bij_betw f A B" |
|
78 |
shows "bij_betw (\<lambda>X. f ` X) ([A]\<^bsup>n\<^esup>) ([B]\<^bsup>n\<^esup>)" |
|
79 |
proof - |
|
80 |
have "(`) f ` [A]\<^bsup>n\<^esup> = [f ` A]\<^bsup>n\<^esup>" |
|
81 |
using assms |
|
82 |
apply (auto simp: nsets_def bij_betw_def image_iff card_image inj_on_subset) |
|
83 |
by (metis card_image inj_on_finite order_refl subset_image_inj) |
|
84 |
with assms show ?thesis |
|
85 |
by (auto simp: bij_betw_def inj_on_nsets) |
|
86 |
qed |
|
87 |
||
71452 | 88 |
lemma nset_image_obtains: |
89 |
assumes "X \<in> [f`A]\<^bsup>k\<^esup>" "inj_on f A" |
|
90 |
obtains Y where "Y \<in> [A]\<^bsup>k\<^esup>" "X = f ` Y" |
|
91 |
using assms |
|
92 |
apply (clarsimp simp add: nsets_def subset_image_iff) |
|
93 |
by (metis card_image finite_imageD inj_on_subset) |
|
94 |
||
95 |
lemma nsets_image_funcset: |
|
96 |
assumes "g \<in> S \<rightarrow> T" and "inj_on g S" |
|
97 |
shows "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>" |
|
98 |
using assms |
|
99 |
by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset) |
|
100 |
||
101 |
lemma nsets_compose_image_funcset: |
|
102 |
assumes f: "f \<in> [T]\<^bsup>k\<^esup> \<rightarrow> D" and "g \<in> S \<rightarrow> T" and "inj_on g S" |
|
103 |
shows "f \<circ> (\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> D" |
|
104 |
proof - |
|
105 |
have "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>" |
|
106 |
using assms by (simp add: nsets_image_funcset) |
|
107 |
then show ?thesis |
|
108 |
using f by fastforce |
|
109 |
qed |
|
110 |
||
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
111 |
subsubsection \<open>Partition predicates\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
112 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
113 |
definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
114 |
where "partn \<beta> \<alpha> \<gamma> \<delta> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma> \<rightarrow> \<delta>. \<exists>H \<in> nsets \<beta> \<alpha>. \<exists>\<xi>\<in>\<delta>. f ` (nsets H \<gamma>) \<subseteq> {\<xi>}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
115 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
116 |
definition partn_lst :: "'a set \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
117 |
where "partn_lst \<beta> \<alpha> \<gamma> \<equiv> \<forall>f \<in> nsets \<beta> \<gamma> \<rightarrow> {..<length \<alpha>}. |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
118 |
\<exists>i < length \<alpha>. \<exists>H \<in> nsets \<beta> (\<alpha>!i). f ` (nsets H \<gamma>) \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
119 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
120 |
lemma partn_lst_greater_resource: |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
121 |
fixes M::nat |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
122 |
assumes M: "partn_lst {..<M} \<alpha> \<gamma>" and "M \<le> N" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
123 |
shows "partn_lst {..<N} \<alpha> \<gamma>" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
124 |
proof (clarsimp simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
125 |
fix f |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
126 |
assume "f \<in> nsets {..<N} \<gamma> \<rightarrow> {..<length \<alpha>}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
127 |
then have "f \<in> nsets {..<M} \<gamma> \<rightarrow> {..<length \<alpha>}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
128 |
by (meson Pi_anti_mono \<open>M \<le> N\<close> lessThan_subset_iff nsets_mono subsetD) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
129 |
then obtain i H where i: "i < length \<alpha>" and H: "H \<in> nsets {..<M} (\<alpha> ! i)" and subi: "f ` nsets H \<gamma> \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
130 |
using M partn_lst_def by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
131 |
have "H \<in> nsets {..<N} (\<alpha> ! i)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
132 |
using \<open>M \<le> N\<close> H by (auto simp: nsets_def subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
133 |
then show "\<exists>i<length \<alpha>. \<exists>H\<in>nsets {..<N} (\<alpha> ! i). f ` nsets H \<gamma> \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
134 |
using i subi by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
135 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
136 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
137 |
lemma partn_lst_fewer_colours: |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
138 |
assumes major: "partn_lst \<beta> (n#\<alpha>) \<gamma>" and "n \<ge> \<gamma>" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
139 |
shows "partn_lst \<beta> \<alpha> \<gamma>" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
140 |
proof (clarsimp simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
141 |
fix f :: "'a set \<Rightarrow> nat" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
142 |
assume f: "f \<in> [\<beta>]\<^bsup>\<gamma>\<^esup> \<rightarrow> {..<length \<alpha>}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
143 |
then obtain i H where i: "i < Suc (length \<alpha>)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
144 |
and H: "H \<in> [\<beta>]\<^bsup>((n # \<alpha>) ! i)\<^esup>" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
145 |
and hom: "\<forall>x\<in>[H]\<^bsup>\<gamma>\<^esup>. Suc (f x) = i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
146 |
using \<open>n \<ge> \<gamma>\<close> major [unfolded partn_lst_def, rule_format, of "Suc o f"] |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
147 |
by (fastforce simp: image_subset_iff nsets_eq_empty_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
148 |
show "\<exists>i<length \<alpha>. \<exists>H\<in>nsets \<beta> (\<alpha> ! i). f ` [H]\<^bsup>\<gamma>\<^esup> \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
149 |
proof (cases i) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
150 |
case 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
151 |
then have "[H]\<^bsup>\<gamma>\<^esup> = {}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
152 |
using hom by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
153 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
154 |
using 0 H \<open>n \<ge> \<gamma>\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
155 |
by (simp add: nsets_eq_empty_iff) (simp add: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
156 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
157 |
case (Suc i') |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
158 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
159 |
using i H hom by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
160 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
161 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
162 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
163 |
lemma partn_lst_eq_partn: "partn_lst {..<n} [m,m] 2 = partn {..<n} m 2 {..<2::nat}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
164 |
apply (simp add: partn_lst_def partn_def numeral_2_eq_2) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
165 |
by (metis less_2_cases numeral_2_eq_2 lessThan_iff nth_Cons_0 nth_Cons_Suc) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
166 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
167 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
168 |
subsection \<open>Finite versions of Ramsey's theorem\<close> |
40695 | 169 |
|
65075 | 170 |
text \<open> |
171 |
To distinguish the finite and infinite ones, lower and upper case |
|
172 |
names are used. |
|
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
173 |
\<close> |
40695 | 174 |
|
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
175 |
subsubsection \<open>Trivial cases\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
176 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
177 |
text \<open>Vacuous, since we are dealing with 0-sets!\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
178 |
lemma ramsey0: "\<exists>N::nat. partn_lst {..<N} [q1,q2] 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
179 |
by (force simp: partn_lst_def ex_in_conv less_Suc_eq nsets_eq_empty_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
180 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
181 |
text \<open>Just the pigeon hole principle, since we are dealing with 1-sets\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
182 |
lemma ramsey1: "\<exists>N::nat. partn_lst {..<N} [q0,q1] 1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
183 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
184 |
have "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..<Suc (q0 + q1)} ([q0, q1] ! i). f ` nsets H (Suc 0) \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
185 |
if "f \<in> nsets {..<Suc (q0 + q1)} (Suc 0) \<rightarrow> {..<Suc (Suc 0)}" for f |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
186 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
187 |
define A where "A \<equiv> \<lambda>i. {q. q \<le> q0+q1 \<and> f {q} = i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
188 |
have "A 0 \<union> A 1 = {..q0 + q1}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
189 |
using that by (auto simp: A_def PiE_iff nsets_one lessThan_Suc_atMost le_Suc_eq) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
190 |
moreover have "A 0 \<inter> A 1 = {}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
191 |
by (auto simp: A_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
192 |
ultimately have "q0 + q1 \<le> card (A 0) + card (A 1)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
193 |
by (metis card_Un_le card_atMost eq_imp_le le_SucI le_trans) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
194 |
then consider "card (A 0) \<ge> q0" | "card (A 1) \<ge> q1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
195 |
by linarith |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
196 |
then obtain i where "i < Suc (Suc 0)" "card (A i) \<ge> [q0, q1] ! i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
197 |
by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
198 |
then obtain B where "B \<subseteq> A i" "card B = [q0, q1] ! i" "finite B" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
199 |
by (meson finite_subset get_smaller_card infinite_arbitrarily_large) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
200 |
then have "B \<in> nsets {..<Suc (q0 + q1)} ([q0, q1] ! i) \<and> f ` nsets B (Suc 0) \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
201 |
by (auto simp: A_def nsets_def card_1_singleton_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
202 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
203 |
using \<open>i < Suc (Suc 0)\<close> by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
204 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
205 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
206 |
by (clarsimp simp: partn_lst_def) blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
207 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
208 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
209 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
210 |
subsubsection \<open>Ramsey's theorem with two colours and arbitrary exponents (hypergraph version)\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
211 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
212 |
proposition ramsey2_full: "\<exists>N::nat. partn_lst {..<N} [q1,q2] r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
213 |
proof (induction r arbitrary: q1 q2) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
214 |
case 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
215 |
then show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
216 |
by (simp add: ramsey0) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
217 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
218 |
case (Suc r) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
219 |
note outer = this |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
220 |
show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
221 |
proof (cases "r = 0") |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
222 |
case True |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
223 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
224 |
using ramsey1 by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
225 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
226 |
case False |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
227 |
then have "r > 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
228 |
by simp |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
229 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
230 |
using Suc.prems |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
231 |
proof (induct k \<equiv> "q1 + q2" arbitrary: q1 q2) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
232 |
case 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
233 |
show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
234 |
proof |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
235 |
show "partn_lst {..<1::nat} [q1, q2] (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
236 |
using nsets_empty_iff subset_insert 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
237 |
by (fastforce simp: partn_lst_def funcset_to_empty_iff nsets_eq_empty image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
238 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
239 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
240 |
case (Suc k) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
241 |
consider "q1 = 0 \<or> q2 = 0" | "q1 \<noteq> 0" "q2 \<noteq> 0" by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
242 |
then show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
243 |
proof cases |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
244 |
case 1 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
245 |
then have "partn_lst {..< Suc 0} [q1, q2] (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
246 |
unfolding partn_lst_def using \<open>r > 0\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
247 |
by (fastforce simp add: nsets_empty_iff nsets_singleton_iff lessThan_Suc) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
248 |
then show ?thesis by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
249 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
250 |
case 2 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
251 |
with Suc have "k = (q1 - 1) + q2" "k = q1 + (q2 - 1)" by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
252 |
then obtain p1 p2::nat where p1: "partn_lst {..<p1} [q1-1,q2] (Suc r)" and p2: "partn_lst {..<p2} [q1,q2-1] (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
253 |
using Suc.hyps by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
254 |
then obtain p::nat where p: "partn_lst {..<p} [p1,p2] r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
255 |
using outer Suc.prems by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
256 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
257 |
proof (intro exI conjI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
258 |
have "\<exists>i<Suc (Suc 0). \<exists>H\<in>nsets {..p} ([q1,q2] ! i). f ` nsets H (Suc r) \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
259 |
if f: "f \<in> nsets {..p} (Suc r) \<rightarrow> {..<Suc (Suc 0)}" for f |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
260 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
261 |
define g where "g \<equiv> \<lambda>R. f (insert p R)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
262 |
have "f (insert p i) \<in> {..<Suc (Suc 0)}" if "i \<in> nsets {..<p} r" for i |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
263 |
using that card_insert_if by (fastforce simp: nsets_def intro!: Pi_mem [OF f]) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
264 |
then have g: "g \<in> nsets {..<p} r \<rightarrow> {..<Suc (Suc 0)}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
265 |
by (force simp: g_def PiE_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
266 |
then obtain i U where i: "i < Suc (Suc 0)" and gi: "g ` nsets U r \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
267 |
and U: "U \<in> nsets {..<p} ([p1, p2] ! i)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
268 |
using p by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
269 |
then have Usub: "U \<subseteq> {..<p}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
270 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
271 |
consider (izero) "i = 0" | (ione) "i = Suc 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
272 |
using i by linarith |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
273 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
274 |
proof cases |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
275 |
case izero |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
276 |
then have "U \<in> nsets {..<p} p1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
277 |
using U by simp |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
278 |
then obtain u where u: "bij_betw u {..<p1} U" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
279 |
using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
280 |
have u_nsets: "u ` X \<in> nsets {..p} n" if "X \<in> nsets {..<p1} n" for X n |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
281 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
282 |
have "inj_on u X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
283 |
using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
284 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
285 |
using Usub u that bij_betwE |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
286 |
by (fastforce simp add: nsets_def card_image) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
287 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
288 |
define h where "h \<equiv> \<lambda>R. f (u ` R)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
289 |
have "h \<in> nsets {..<p1} (Suc r) \<rightarrow> {..<Suc (Suc 0)}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
290 |
unfolding h_def using f u_nsets by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
291 |
then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
292 |
and V: "V \<in> nsets {..<p1} ([q1 - Suc 0, q2] ! j)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
293 |
using p1 by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
294 |
then have Vsub: "V \<subseteq> {..<p1}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
295 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
296 |
have invinv_eq: "u ` inv_into {..<p1} u ` X = X" if "X \<subseteq> u ` {..<p1}" for X |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
297 |
by (simp add: image_inv_into_cancel that) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
298 |
let ?W = "insert p (u ` V)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
299 |
consider (jzero) "j = 0" | (jone) "j = Suc 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
300 |
using j by linarith |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
301 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
302 |
proof cases |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
303 |
case jzero |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
304 |
then have "V \<in> nsets {..<p1} (q1 - Suc 0)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
305 |
using V by simp |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
306 |
then have "u ` V \<in> nsets {..<p} (q1 - Suc 0)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
307 |
using u_nsets [of _ "q1 - Suc 0"] nsets_mono [OF Vsub] Usub u |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
308 |
unfolding bij_betw_def nsets_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
309 |
by (fastforce elim!: subsetD) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
310 |
then have inq1: "?W \<in> nsets {..p} q1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
311 |
unfolding nsets_def using \<open>q1 \<noteq> 0\<close> card_insert_if by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
312 |
have invu_nsets: "inv_into {..<p1} u ` X \<in> nsets V r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
313 |
if "X \<in> nsets (u ` V) r" for X r |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
314 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
315 |
have "X \<subseteq> u ` V \<and> finite X \<and> card X = r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
316 |
using nsets_def that by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
317 |
then have [simp]: "card (inv_into {..<p1} u ` X) = card X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
318 |
by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
319 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
320 |
using that u Vsub by (fastforce simp: nsets_def bij_betw_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
321 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
322 |
have "f X = i" if X: "X \<in> nsets ?W (Suc r)" for X |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
323 |
proof (cases "p \<in> X") |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
324 |
case True |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
325 |
then have Xp: "X - {p} \<in> nsets (u ` V) r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
326 |
using X by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
327 |
moreover have "u ` V \<subseteq> U" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
328 |
using Vsub bij_betwE u by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
329 |
ultimately have "X - {p} \<in> nsets U r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
330 |
by (meson in_mono nsets_mono) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
331 |
then have "g (X - {p}) = i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
332 |
using gi by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
333 |
have "f X = i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
334 |
using gi True \<open>X - {p} \<in> nsets U r\<close> insert_Diff |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
335 |
by (fastforce simp add: g_def image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
336 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
337 |
by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
338 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
339 |
case False |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
340 |
then have Xim: "X \<in> nsets (u ` V) (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
341 |
using X by (auto simp: nsets_def subset_insert) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
342 |
then have "u ` inv_into {..<p1} u ` X = X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
343 |
using Vsub bij_betw_imp_inj_on u |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
344 |
by (fastforce simp: nsets_def image_mono invinv_eq subset_trans) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
345 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
346 |
using izero jzero hj Xim invu_nsets unfolding h_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
347 |
by (fastforce simp add: image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
348 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
349 |
moreover have "insert p (u ` V) \<in> nsets {..p} q1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
350 |
by (simp add: izero inq1) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
351 |
ultimately show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
352 |
by (metis izero image_subsetI insertI1 nth_Cons_0 zero_less_Suc) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
353 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
354 |
case jone |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
355 |
then have "u ` V \<in> nsets {..p} q2" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
356 |
using V u_nsets by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
357 |
moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
358 |
using hj |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
359 |
by (force simp add: h_def image_subset_iff nsets_def subset_image_inj card_image dest: finite_imageD) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
360 |
ultimately show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
361 |
using jone not_less_eq by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
362 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
363 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
364 |
case ione |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
365 |
then have "U \<in> nsets {..<p} p2" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
366 |
using U by simp |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
367 |
then obtain u where u: "bij_betw u {..<p2} U" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
368 |
using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
369 |
have u_nsets: "u ` X \<in> nsets {..p} n" if "X \<in> nsets {..<p2} n" for X n |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
370 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
371 |
have "inj_on u X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
372 |
using u that bij_betw_imp_inj_on inj_on_subset by (force simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
373 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
374 |
using Usub u that bij_betwE |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
375 |
by (fastforce simp add: nsets_def card_image) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
376 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
377 |
define h where "h \<equiv> \<lambda>R. f (u ` R)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
378 |
have "h \<in> nsets {..<p2} (Suc r) \<rightarrow> {..<Suc (Suc 0)}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
379 |
unfolding h_def using f u_nsets by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
380 |
then obtain j V where j: "j <Suc (Suc 0)" and hj: "h ` nsets V (Suc r) \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
381 |
and V: "V \<in> nsets {..<p2} ([q1, q2 - Suc 0] ! j)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
382 |
using p2 by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
383 |
then have Vsub: "V \<subseteq> {..<p2}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
384 |
by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
385 |
have invinv_eq: "u ` inv_into {..<p2} u ` X = X" if "X \<subseteq> u ` {..<p2}" for X |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
386 |
by (simp add: image_inv_into_cancel that) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
387 |
let ?W = "insert p (u ` V)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
388 |
consider (jzero) "j = 0" | (jone) "j = Suc 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
389 |
using j by linarith |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
390 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
391 |
proof cases |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
392 |
case jone |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
393 |
then have "V \<in> nsets {..<p2} (q2 - Suc 0)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
394 |
using V by simp |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
395 |
then have "u ` V \<in> nsets {..<p} (q2 - Suc 0)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
396 |
using u_nsets [of _ "q2 - Suc 0"] nsets_mono [OF Vsub] Usub u |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
397 |
unfolding bij_betw_def nsets_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
398 |
by (fastforce elim!: subsetD) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
399 |
then have inq1: "?W \<in> nsets {..p} q2" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
400 |
unfolding nsets_def using \<open>q2 \<noteq> 0\<close> card_insert_if by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
401 |
have invu_nsets: "inv_into {..<p2} u ` X \<in> nsets V r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
402 |
if "X \<in> nsets (u ` V) r" for X r |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
403 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
404 |
have "X \<subseteq> u ` V \<and> finite X \<and> card X = r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
405 |
using nsets_def that by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
406 |
then have [simp]: "card (inv_into {..<p2} u ` X) = card X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
407 |
by (meson Vsub bij_betw_def bij_betw_inv_into card_image image_mono inj_on_subset u) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
408 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
409 |
using that u Vsub by (fastforce simp: nsets_def bij_betw_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
410 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
411 |
have "f X = i" if X: "X \<in> nsets ?W (Suc r)" for X |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
412 |
proof (cases "p \<in> X") |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
413 |
case True |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
414 |
then have Xp: "X - {p} \<in> nsets (u ` V) r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
415 |
using X by (auto simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
416 |
moreover have "u ` V \<subseteq> U" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
417 |
using Vsub bij_betwE u by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
418 |
ultimately have "X - {p} \<in> nsets U r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
419 |
by (meson in_mono nsets_mono) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
420 |
then have "g (X - {p}) = i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
421 |
using gi by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
422 |
have "f X = i" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
423 |
using gi True \<open>X - {p} \<in> nsets U r\<close> insert_Diff |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
424 |
by (fastforce simp add: g_def image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
425 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
426 |
by (simp add: \<open>f X = i\<close> \<open>g (X - {p}) = i\<close>) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
427 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
428 |
case False |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
429 |
then have Xim: "X \<in> nsets (u ` V) (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
430 |
using X by (auto simp: nsets_def subset_insert) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
431 |
then have "u ` inv_into {..<p2} u ` X = X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
432 |
using Vsub bij_betw_imp_inj_on u |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
433 |
by (fastforce simp: nsets_def image_mono invinv_eq subset_trans) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
434 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
435 |
using ione jone hj Xim invu_nsets unfolding h_def |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
436 |
by (fastforce simp add: image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
437 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
438 |
moreover have "insert p (u ` V) \<in> nsets {..p} q2" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
439 |
by (simp add: ione inq1) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
440 |
ultimately show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
441 |
by (metis ione image_subsetI insertI1 lessI nth_Cons_0 nth_Cons_Suc) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
442 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
443 |
case jzero |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
444 |
then have "u ` V \<in> nsets {..p} q1" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
445 |
using V u_nsets by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
446 |
moreover have "f ` nsets (u ` V) (Suc r) \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
447 |
using hj |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
448 |
apply (clarsimp simp add: h_def image_subset_iff nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
449 |
by (metis Zero_not_Suc card_eq_0_iff card_image subset_image_inj) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
450 |
ultimately show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
451 |
using jzero not_less_eq by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
452 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
453 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
454 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
455 |
then show "partn_lst {..<Suc p} [q1,q2] (Suc r)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
456 |
using lessThan_Suc lessThan_Suc_atMost by (auto simp: partn_lst_def insert_commute) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
457 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
458 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
459 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
460 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
461 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
462 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
463 |
subsubsection \<open>Full Ramsey's theorem with multiple colours and arbitrary exponents\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
464 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
465 |
theorem ramsey_full: "\<exists>N::nat. partn_lst {..<N} qs r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
466 |
proof (induction k \<equiv> "length qs" arbitrary: qs) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
467 |
case 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
468 |
then show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
469 |
by (rule_tac x=" r" in exI) (simp add: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
470 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
471 |
case (Suc k) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
472 |
note IH = this |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
473 |
show ?case |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
474 |
proof (cases k) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
475 |
case 0 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
476 |
with Suc obtain q where "qs = [q]" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
477 |
by (metis length_0_conv length_Suc_conv) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
478 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
479 |
by (rule_tac x=q in exI) (auto simp: partn_lst_def funcset_to_empty_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
480 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
481 |
case (Suc k') |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
482 |
then obtain q1 q2 l where qs: "qs = q1#q2#l" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
483 |
by (metis Suc.hyps(2) length_Suc_conv) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
484 |
then obtain q::nat where q: "partn_lst {..<q} [q1,q2] r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
485 |
using ramsey2_full by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
486 |
then obtain p::nat where p: "partn_lst {..<p} (q#l) r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
487 |
using IH \<open>qs = q1 # q2 # l\<close> by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
488 |
have keq: "Suc (length l) = k" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
489 |
using IH qs by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
490 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
491 |
proof (intro exI conjI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
492 |
show "partn_lst {..<p} qs r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
493 |
proof (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
494 |
fix f |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
495 |
assume f: "f \<in> nsets {..<p} r \<rightarrow> {..<length qs}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
496 |
define g where "g \<equiv> \<lambda>X. if f X < Suc (Suc 0) then 0 else f X - Suc 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
497 |
have "g \<in> nsets {..<p} r \<rightarrow> {..<k}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
498 |
unfolding g_def using f Suc IH |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
499 |
by (auto simp: Pi_def not_less) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
500 |
then obtain i U where i: "i < k" and gi: "g ` nsets U r \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
501 |
and U: "U \<in> nsets {..<p} ((q#l) ! i)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
502 |
using p keq by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
503 |
show "\<exists>i<length qs. \<exists>H\<in>nsets {..<p} (qs ! i). f ` nsets H r \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
504 |
proof (cases "i = 0") |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
505 |
case True |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
506 |
then have "U \<in> nsets {..<p} q" and f01: "f ` nsets U r \<subseteq> {0, Suc 0}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
507 |
using U gi unfolding g_def by (auto simp: image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
508 |
then obtain u where u: "bij_betw u {..<q} U" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
509 |
using ex_bij_betw_nat_finite lessThan_atLeast0 by (fastforce simp add: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
510 |
then have Usub: "U \<subseteq> {..<p}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
511 |
by (smt \<open>U \<in> nsets {..<p} q\<close> mem_Collect_eq nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
512 |
have u_nsets: "u ` X \<in> nsets {..<p} n" if "X \<in> nsets {..<q} n" for X n |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
513 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
514 |
have "inj_on u X" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
515 |
using u that bij_betw_imp_inj_on inj_on_subset |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
516 |
by (force simp: nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
517 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
518 |
using Usub u that bij_betwE |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
519 |
by (fastforce simp add: nsets_def card_image) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
520 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
521 |
define h where "h \<equiv> \<lambda>X. f (u ` X)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
522 |
have "f (u ` X) < Suc (Suc 0)" if "X \<in> nsets {..<q} r" for X |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
523 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
524 |
have "u ` X \<in> nsets U r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
525 |
using u u_nsets that by (auto simp: nsets_def bij_betwE subset_eq) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
526 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
527 |
using f01 by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
528 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
529 |
then have "h \<in> nsets {..<q} r \<rightarrow> {..<Suc (Suc 0)}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
530 |
unfolding h_def by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
531 |
then obtain j V where j: "j < Suc (Suc 0)" and hj: "h ` nsets V r \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
532 |
and V: "V \<in> nsets {..<q} ([q1,q2] ! j)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
533 |
using q by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
534 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
535 |
proof (intro exI conjI bexI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
536 |
show "j < length qs" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
537 |
using Suc Suc.hyps(2) j by linarith |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
538 |
have "nsets (u ` V) r \<subseteq> (\<lambda>x. (u ` x)) ` nsets V r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
539 |
apply (clarsimp simp add: nsets_def image_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
540 |
by (metis card_eq_0_iff card_image image_is_empty subset_image_inj) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
541 |
then have "f ` nsets (u ` V) r \<subseteq> h ` nsets V r" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
542 |
by (auto simp: h_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
543 |
then show "f ` nsets (u ` V) r \<subseteq> {j}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
544 |
using hj by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
545 |
show "(u ` V) \<in> nsets {..<p} (qs ! j)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
546 |
using V j less_2_cases numeral_2_eq_2 qs u_nsets by fastforce |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
547 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
548 |
next |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
549 |
case False |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
550 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
551 |
proof (intro exI conjI bexI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
552 |
show "Suc i < length qs" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
553 |
using Suc.hyps(2) i by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
554 |
show "f ` nsets U r \<subseteq> {Suc i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
555 |
using i gi False |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
556 |
apply (auto simp: g_def image_subset_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
557 |
by (metis Suc_lessD Suc_pred g_def gi image_subset_iff not_less_eq singleton_iff) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
558 |
show "U \<in> nsets {..<p} (qs ! (Suc i))" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
559 |
using False U qs by auto |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
560 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
561 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
562 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
563 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
564 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
565 |
qed |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
566 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
567 |
subsubsection \<open>Simple graph version\<close> |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
568 |
|
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
569 |
text \<open>This is the most basic version in terms of cliques and independent |
65075 | 570 |
sets, i.e. the version for graphs and 2 colours. |
571 |
\<close> |
|
40695 | 572 |
|
65075 | 573 |
definition "clique V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<in> E)" |
574 |
definition "indep V E \<longleftrightarrow> (\<forall>v\<in>V. \<forall>w\<in>V. v \<noteq> w \<longrightarrow> {v, w} \<notin> E)" |
|
40695 | 575 |
|
576 |
lemma ramsey2: |
|
65075 | 577 |
"\<exists>r\<ge>1. \<forall>(V::'a set) (E::'a set set). finite V \<and> card V \<ge> r \<longrightarrow> |
578 |
(\<exists>R \<subseteq> V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E)" |
|
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
579 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
580 |
obtain N where "N \<ge> Suc 0" and N: "partn_lst {..<N} [m,n] 2" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
581 |
using ramsey2_full nat_le_linear partn_lst_greater_resource by blast |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
582 |
have "\<exists>R\<subseteq>V. card R = m \<and> clique R E \<or> card R = n \<and> indep R E" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
583 |
if "finite V" "N \<le> card V" for V :: "'a set" and E :: "'a set set" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
584 |
proof - |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
585 |
from that |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
586 |
obtain v where u: "inj_on v {..<N}" "v ` {..<N} \<subseteq> V" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
587 |
by (metis card_le_inj card_lessThan finite_lessThan) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
588 |
define f where "f \<equiv> \<lambda>e. if v ` e \<in> E then 0 else Suc 0" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
589 |
have f: "f \<in> nsets {..<N} 2 \<rightarrow> {..<Suc (Suc 0)}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
590 |
by (simp add: f_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
591 |
then obtain i U where i: "i < 2" and gi: "f ` nsets U 2 \<subseteq> {i}" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
592 |
and U: "U \<in> nsets {..<N} ([m,n] ! i)" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
593 |
using N numeral_2_eq_2 by (auto simp: partn_lst_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
594 |
show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
595 |
proof (intro exI conjI) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
596 |
show "v ` U \<subseteq> V" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
597 |
using U u by (auto simp: image_subset_iff nsets_def) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
598 |
show "card (v ` U) = m \<and> clique (v ` U) E \<or> card (v ` U) = n \<and> indep (v ` U) E" |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
599 |
using i unfolding numeral_2_eq_2 |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
600 |
using gi U u |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
601 |
apply (simp add: image_subset_iff nsets_2_eq clique_def indep_def less_Suc_eq) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
602 |
apply (auto simp: f_def nsets_def card_image inj_on_subset split: if_split_asm) |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
603 |
done |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
604 |
qed |
40695 | 605 |
qed |
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
606 |
then show ?thesis |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71083
diff
changeset
|
607 |
using \<open>Suc 0 \<le> N\<close> by auto |
40695 | 608 |
qed |
609 |
||
610 |
||
60500 | 611 |
subsection \<open>Preliminaries\<close> |
19944 | 612 |
|
60500 | 613 |
subsubsection \<open>``Axiom'' of Dependent Choice\<close> |
19944 | 614 |
|
65075 | 615 |
primrec choice :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> 'a" |
616 |
where \<comment> \<open>An integer-indexed chain of choices\<close> |
|
617 |
choice_0: "choice P r 0 = (SOME x. P x)" |
|
618 |
| choice_Suc: "choice P r (Suc n) = (SOME y. P y \<and> (choice P r n, y) \<in> r)" |
|
19944 | 619 |
|
46575 | 620 |
lemma choice_n: |
19944 | 621 |
assumes P0: "P x0" |
65075 | 622 |
and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r" |
19944 | 623 |
shows "P (choice P r n)" |
19948 | 624 |
proof (induct n) |
65075 | 625 |
case 0 |
626 |
show ?case by (force intro: someI P0) |
|
19948 | 627 |
next |
65075 | 628 |
case Suc |
629 |
then show ?case by (auto intro: someI2_ex [OF Pstep]) |
|
19948 | 630 |
qed |
19944 | 631 |
|
46575 | 632 |
lemma dependent_choice: |
19944 | 633 |
assumes trans: "trans r" |
65075 | 634 |
and P0: "P x0" |
635 |
and Pstep: "\<And>x. P x \<Longrightarrow> \<exists>y. P y \<and> (x, y) \<in> r" |
|
636 |
obtains f :: "nat \<Rightarrow> 'a" where "\<And>n. P (f n)" and "\<And>n m. n < m \<Longrightarrow> (f n, f m) \<in> r" |
|
19954 | 637 |
proof |
638 |
fix n |
|
65075 | 639 |
show "P (choice P r n)" |
640 |
by (blast intro: choice_n [OF P0 Pstep]) |
|
19944 | 641 |
next |
65075 | 642 |
fix n m :: nat |
643 |
assume "n < m" |
|
644 |
from Pstep [OF choice_n [OF P0 Pstep]] have "(choice P r k, choice P r (Suc k)) \<in> r" for k |
|
19944 | 645 |
by (auto intro: someI2_ex) |
65075 | 646 |
then show "(choice P r n, choice P r m) \<in> r" |
647 |
by (auto intro: less_Suc_induct [OF \<open>n < m\<close>] transD [OF trans]) |
|
19954 | 648 |
qed |
19944 | 649 |
|
650 |
||
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
651 |
subsubsection \<open>Partition functions\<close> |
19944 | 652 |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
653 |
definition part_fn :: "nat \<Rightarrow> nat \<Rightarrow> 'a set \<Rightarrow> ('a set \<Rightarrow> nat) \<Rightarrow> bool" |
69593 | 654 |
\<comment> \<open>the function \<^term>\<open>f\<close> partitions the \<^term>\<open>r\<close>-subsets of the typically |
655 |
infinite set \<^term>\<open>Y\<close> into \<^term>\<open>s\<close> distinct categories.\<close> |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
656 |
where "part_fn r s Y f \<longleftrightarrow> (f \<in> nsets Y r \<rightarrow> {..<s})" |
19944 | 657 |
|
69593 | 658 |
text \<open>For induction, we decrease the value of \<^term>\<open>r\<close> in partitions.\<close> |
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
659 |
lemma part_fn_Suc_imp_part_fn: |
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
660 |
"\<lbrakk>infinite Y; part_fn (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part_fn r s (Y - {y}) (\<lambda>u. f (insert y u))" |
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
661 |
by (simp add: part_fn_def nsets_def Pi_def subset_Diff_insert) |
19944 | 662 |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
663 |
lemma part_fn_subset: "part_fn r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part_fn r s Y f" |
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
664 |
unfolding part_fn_def nsets_def by blast |
46575 | 665 |
|
19944 | 666 |
|
60500 | 667 |
subsection \<open>Ramsey's Theorem: Infinitary Version\<close> |
19944 | 668 |
|
46575 | 669 |
lemma Ramsey_induction: |
65075 | 670 |
fixes s r :: nat |
671 |
and YY :: "'a set" |
|
672 |
and f :: "'a set \<Rightarrow> nat" |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
673 |
assumes "infinite YY" "part_fn r s YY f" |
65075 | 674 |
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')" |
675 |
using assms |
|
676 |
proof (induct r arbitrary: YY f) |
|
19944 | 677 |
case 0 |
65075 | 678 |
then show ?case |
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
679 |
by (auto simp add: part_fn_def card_eq_0_iff cong: conj_cong) |
19944 | 680 |
next |
46575 | 681 |
case (Suc r) |
19944 | 682 |
show ?case |
683 |
proof - |
|
65075 | 684 |
from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" |
685 |
by blast |
|
686 |
let ?ramr = "{((y, Y, t), (y', Y', t')). y' \<in> Y \<and> Y' \<subseteq> Y}" |
|
687 |
let ?propr = "\<lambda>(y, Y, t). |
|
688 |
y \<in> YY \<and> y \<notin> Y \<and> Y \<subseteq> YY \<and> infinite Y \<and> t < s |
|
689 |
\<and> (\<forall>X. X\<subseteq>Y \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert y) X = t)" |
|
690 |
from Suc.prems have infYY': "infinite (YY - {yy})" by auto |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
691 |
from Suc.prems have partf': "part_fn r s (YY - {yy}) (f \<circ> insert yy)" |
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
692 |
by (simp add: o_def part_fn_Suc_imp_part_fn yy) |
46575 | 693 |
have transr: "trans ?ramr" by (force simp add: trans_def) |
19944 | 694 |
from Suc.hyps [OF infYY' partf'] |
65075 | 695 |
obtain Y0 and t0 where "Y0 \<subseteq> YY - {yy}" "infinite Y0" "t0 < s" |
696 |
"X \<subseteq> Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0" for X |
|
697 |
by blast |
|
698 |
with yy have propr0: "?propr(yy, Y0, t0)" by blast |
|
699 |
have proprstep: "\<exists>y. ?propr y \<and> (x, y) \<in> ?ramr" if x: "?propr x" for x |
|
700 |
proof (cases x) |
|
701 |
case (fields yx Yx tx) |
|
702 |
with x obtain yx' where yx': "yx' \<in> Yx" |
|
703 |
by (blast dest: infinite_imp_nonempty) |
|
704 |
from fields x have infYx': "infinite (Yx - {yx'})" by auto |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
705 |
with fields x yx' Suc.prems have partfx': "part_fn r s (Yx - {yx'}) (f \<circ> insert yx')" |
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
706 |
by (simp add: o_def part_fn_Suc_imp_part_fn part_fn_subset [where YY=YY and Y=Yx]) |
65075 | 707 |
from Suc.hyps [OF infYx' partfx'] obtain Y' and t' |
708 |
where Y': "Y' \<subseteq> Yx - {yx'}" "infinite Y'" "t' < s" |
|
709 |
"X \<subseteq> Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'" for X |
|
46575 | 710 |
by blast |
65075 | 711 |
from fields x Y' yx' have "?propr (yx', Y', t') \<and> (x, (yx', Y', t')) \<in> ?ramr" |
712 |
by blast |
|
713 |
then show ?thesis .. |
|
19944 | 714 |
qed |
715 |
from dependent_choice [OF transr propr0 proprstep] |
|
65075 | 716 |
obtain g where pg: "?propr (g n)" and rg: "n < m \<Longrightarrow> (g n, g m) \<in> ?ramr" for n m :: nat |
63060 | 717 |
by blast |
65075 | 718 |
let ?gy = "fst \<circ> g" |
719 |
let ?gt = "snd \<circ> snd \<circ> g" |
|
19944 | 720 |
have rangeg: "\<exists>k. range ?gt \<subseteq> {..<k}" |
721 |
proof (intro exI subsetI) |
|
722 |
fix x |
|
723 |
assume "x \<in> range ?gt" |
|
724 |
then obtain n where "x = ?gt n" .. |
|
725 |
with pg [of n] show "x \<in> {..<s}" by (cases "g n") auto |
|
726 |
qed |
|
69661 | 727 |
from rangeg have "finite (range ?gt)" |
728 |
by (simp add: finite_nat_iff_bounded) |
|
65075 | 729 |
then obtain s' and n' where s': "s' = ?gt n'" and infeqs': "infinite {n. ?gt n = s'}" |
54580 | 730 |
by (rule inf_img_fin_domE) (auto simp add: vimage_def intro: infinite_UNIV_nat) |
19944 | 731 |
with pg [of n'] have less': "s'<s" by (cases "g n'") auto |
732 |
have inj_gy: "inj ?gy" |
|
733 |
proof (rule linorder_injI) |
|
65075 | 734 |
fix m m' :: nat |
735 |
assume "m < m'" |
|
736 |
from rg [OF this] pg [of m] show "?gy m \<noteq> ?gy m'" |
|
737 |
by (cases "g m", cases "g m'") auto |
|
19944 | 738 |
qed |
739 |
show ?thesis |
|
740 |
proof (intro exI conjI) |
|
65075 | 741 |
from pg show "?gy ` {n. ?gt n = s'} \<subseteq> YY" |
46575 | 742 |
by (auto simp add: Let_def split_beta) |
65075 | 743 |
from infeqs' show "infinite (?gy ` {n. ?gt n = s'})" |
46575 | 744 |
by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) |
19944 | 745 |
show "s' < s" by (rule less') |
65075 | 746 |
show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} \<and> finite X \<and> card X = Suc r \<longrightarrow> f X = s'" |
19944 | 747 |
proof - |
65075 | 748 |
have "f X = s'" |
749 |
if X: "X \<subseteq> ?gy ` {n. ?gt n = s'}" |
|
750 |
and cardX: "finite X" "card X = Suc r" |
|
751 |
for X |
|
752 |
proof - |
|
753 |
from X obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA" |
|
754 |
by (auto simp add: subset_image_iff) |
|
755 |
with cardX have "AA \<noteq> {}" by auto |
|
756 |
then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex) |
|
757 |
show ?thesis |
|
758 |
proof (cases "g (LEAST x. x \<in> AA)") |
|
759 |
case (fields ya Ya ta) |
|
760 |
with AAleast Xeq have ya: "ya \<in> X" by (force intro!: rev_image_eqI) |
|
761 |
then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb) |
|
762 |
also have "\<dots> = ta" |
|
763 |
proof - |
|
764 |
have *: "X - {ya} \<subseteq> Ya" |
|
765 |
proof |
|
766 |
fix x assume x: "x \<in> X - {ya}" |
|
767 |
then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA" |
|
768 |
by (auto simp add: Xeq) |
|
769 |
with fields x have "a' \<noteq> (LEAST x. x \<in> AA)" by auto |
|
770 |
with Least_le [of "\<lambda>x. x \<in> AA", OF a'] have "(LEAST x. x \<in> AA) < a'" |
|
771 |
by arith |
|
772 |
from xeq fields rg [OF this] show "x \<in> Ya" by auto |
|
773 |
qed |
|
774 |
have "card (X - {ya}) = r" |
|
775 |
by (simp add: cardX ya) |
|
776 |
with pg [of "LEAST x. x \<in> AA"] fields cardX * show ?thesis |
|
777 |
by (auto simp del: insert_Diff_single) |
|
778 |
qed |
|
779 |
also from AA AAleast fields have "\<dots> = s'" by auto |
|
780 |
finally show ?thesis . |
|
781 |
qed |
|
782 |
qed |
|
46575 | 783 |
then show ?thesis by blast |
784 |
qed |
|
785 |
qed |
|
19944 | 786 |
qed |
787 |
qed |
|
788 |
||
789 |
||
790 |
theorem Ramsey: |
|
65075 | 791 |
fixes s r :: nat |
792 |
and Z :: "'a set" |
|
793 |
and f :: "'a set \<Rightarrow> nat" |
|
19944 | 794 |
shows |
65075 | 795 |
"\<lbrakk>infinite Z; |
796 |
\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = r \<longrightarrow> f X < s\<rbrakk> |
|
797 |
\<Longrightarrow> \<exists>Y t. Y \<subseteq> Z \<and> infinite Y \<and> t < s |
|
798 |
\<and> (\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = r \<longrightarrow> f X = t)" |
|
71260
308baf6b450a
corrected some confusing terminology / notation
paulson <lp15@cam.ac.uk>
parents:
71259
diff
changeset
|
799 |
by (blast intro: Ramsey_induction [unfolded part_fn_def nsets_def]) |
19954 | 800 |
|
801 |
||
802 |
corollary Ramsey2: |
|
65075 | 803 |
fixes s :: nat |
804 |
and Z :: "'a set" |
|
805 |
and f :: "'a set \<Rightarrow> nat" |
|
19954 | 806 |
assumes infZ: "infinite Z" |
65075 | 807 |
and part: "\<forall>x\<in>Z. \<forall>y\<in>Z. x \<noteq> y \<longrightarrow> f {x, y} < s" |
808 |
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)" |
|
19954 | 809 |
proof - |
65075 | 810 |
from part have part2: "\<forall>X. X \<subseteq> Z \<and> finite X \<and> card X = 2 \<longrightarrow> f X < s" |
811 |
by (fastforce simp add: eval_nat_numeral card_Suc_eq) |
|
812 |
obtain Y t where *: |
|
813 |
"Y \<subseteq> Z" "infinite Y" "t < s" "(\<forall>X. X \<subseteq> Y \<and> finite X \<and> card X = 2 \<longrightarrow> f X = t)" |
|
19954 | 814 |
by (insert Ramsey [OF infZ part2]) auto |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
46575
diff
changeset
|
815 |
then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
46575
diff
changeset
|
816 |
with * show ?thesis by iprover |
19954 | 817 |
qed |
818 |
||
819 |
||
60500 | 820 |
subsection \<open>Disjunctive Well-Foundedness\<close> |
19954 | 821 |
|
60500 | 822 |
text \<open> |
22367 | 823 |
An application of Ramsey's theorem to program termination. See |
58622 | 824 |
@{cite "Podelski-Rybalchenko"}. |
60500 | 825 |
\<close> |
19954 | 826 |
|
65075 | 827 |
definition disj_wf :: "('a \<times> 'a) set \<Rightarrow> bool" |
828 |
where "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf (T i)) \<and> r = (\<Union>i<n. T i))" |
|
19954 | 829 |
|
65075 | 830 |
definition transition_idx :: "(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> ('a \<times> 'a) set) \<Rightarrow> nat set \<Rightarrow> nat" |
831 |
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)" |
|
19954 | 832 |
|
833 |
||
834 |
lemma transition_idx_less: |
|
65075 | 835 |
assumes "i < j" "(s j, s i) \<in> T k" "k < n" |
836 |
shows "transition_idx s T {i, j} < n" |
|
837 |
proof - |
|
838 |
from assms(1,2) have "transition_idx s T {i, j} \<le> k" |
|
839 |
by (simp add: transition_idx_def, blast intro: Least_le) |
|
840 |
with assms(3) show ?thesis by simp |
|
841 |
qed |
|
19954 | 842 |
|
843 |
lemma transition_idx_in: |
|
65075 | 844 |
assumes "i < j" "(s j, s i) \<in> T k" |
845 |
shows "(s j, s i) \<in> T (transition_idx s T {i, j})" |
|
846 |
using assms |
|
847 |
by (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR cong: conj_cong) (erule LeastI) |
|
19954 | 848 |
|
65075 | 849 |
text \<open>To be equal to the union of some well-founded relations is equivalent |
850 |
to being the subset of such a union.\<close> |
|
851 |
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))" |
|
71083
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
852 |
proof - |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
853 |
have *: "\<And>T n. \<lbrakk>\<forall>i<n. wf (T i); r \<subseteq> \<Union> (T ` {..<n})\<rbrakk> |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
854 |
\<Longrightarrow> (\<forall>i<n. wf (T i \<inter> r)) \<and> r = (\<Union>i<n. T i \<inter> r)" |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
855 |
by (force simp add: wf_Int1) |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
856 |
show ?thesis |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
857 |
unfolding disj_wf_def by auto (metis "*") |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
858 |
qed |
19954 | 859 |
|
860 |
theorem trans_disj_wf_implies_wf: |
|
65075 | 861 |
assumes "trans r" |
862 |
and "disj_wf r" |
|
19954 | 863 |
shows "wf r" |
864 |
proof (simp only: wf_iff_no_infinite_down_chain, rule notI) |
|
865 |
assume "\<exists>s. \<forall>i. (s (Suc i), s i) \<in> r" |
|
866 |
then obtain s where sSuc: "\<forall>i. (s (Suc i), s i) \<in> r" .. |
|
65075 | 867 |
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)" |
868 |
by (auto simp add: disj_wf_def) |
|
869 |
have s_in_T: "\<exists>k. (s j, s i) \<in> T k \<and> k<n" if "i < j" for i j |
|
19954 | 870 |
proof - |
65075 | 871 |
from \<open>i < j\<close> have "(s j, s i) \<in> r" |
872 |
proof (induct rule: less_Suc_induct) |
|
873 |
case 1 |
|
874 |
then show ?case by (simp add: sSuc) |
|
875 |
next |
|
876 |
case 2 |
|
877 |
with \<open>trans r\<close> show ?case |
|
878 |
unfolding trans_def by blast |
|
19954 | 879 |
qed |
65075 | 880 |
then show ?thesis by (auto simp add: r) |
46575 | 881 |
qed |
71083
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
882 |
have "i < j \<Longrightarrow> transition_idx s T {i, j} < n" for i j |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
883 |
using s_in_T transition_idx_less by blast |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
884 |
then have trless: "i \<noteq> j \<Longrightarrow> transition_idx s T {i, j} < n" for i j |
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
885 |
by (metis doubleton_eq_iff less_linear) |
65075 | 886 |
have "\<exists>K k. K \<subseteq> UNIV \<and> infinite K \<and> k < n \<and> |
887 |
(\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k)" |
|
54580 | 888 |
by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat) |
65075 | 889 |
then obtain K and k where infK: "infinite K" and "k < n" |
890 |
and allk: "\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k" |
|
19954 | 891 |
by auto |
65075 | 892 |
have "(s (enumerate K (Suc m)), s (enumerate K m)) \<in> T k" for m :: nat |
893 |
proof - |
|
19954 | 894 |
let ?j = "enumerate K (Suc m)" |
895 |
let ?i = "enumerate K m" |
|
46575 | 896 |
have ij: "?i < ?j" by (simp add: enumerate_step infK) |
65075 | 897 |
have "?j \<in> K" "?i \<in> K" by (simp_all add: enumerate_in_set infK) |
898 |
with ij have k: "k = transition_idx s T {?i, ?j}" by (simp add: allk) |
|
899 |
from s_in_T [OF ij] obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" by blast |
|
900 |
then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij) |
|
19954 | 901 |
qed |
65075 | 902 |
then have "\<not> wf (T k)" |
71083
ce92360f0692
A slight tidying up of messy proof steps
paulson <lp15@cam.ac.uk>
parents:
69661
diff
changeset
|
903 |
by (meson wf_iff_no_infinite_down_chain) |
65075 | 904 |
with wfT \<open>k < n\<close> show False by blast |
19954 | 905 |
qed |
906 |
||
19944 | 907 |
end |