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