|
1 (* Title: ZF/ex/ramsey.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Ramsey's Theorem (finite exponent 2 version) |
|
7 |
|
8 Based upon the article |
|
9 D Basin and M Kaufmann, |
|
10 The Boyer-Moore Prover and Nuprl: An Experimental Comparison. |
|
11 In G Huet and G Plotkin, editors, Logical Frameworks. |
|
12 (CUP, 1991), pages 89--119 |
|
13 |
|
14 See also |
|
15 M Kaufmann, |
|
16 An example in NQTHM: Ramsey's Theorem |
|
17 Internal Note, Computational Logic, Inc., Austin, Texas 78703 |
|
18 Available from the author: kaufmann@cli.com |
|
19 *) |
|
20 |
|
21 open Ramsey; |
|
22 |
|
23 val ramsey_congs = mk_congs Ramsey.thy ["Atleast"]; |
|
24 val ramsey_ss = arith_ss addcongs ramsey_congs; |
|
25 |
|
26 (*** Cliques and Independent sets ***) |
|
27 |
|
28 goalw Ramsey.thy [Clique_def] "Clique(0,V,E)"; |
|
29 by (fast_tac ZF_cs 1); |
|
30 val Clique0 = result(); |
|
31 |
|
32 goalw Ramsey.thy [Clique_def] |
|
33 "!!C V E. [| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)"; |
|
34 by (fast_tac ZF_cs 1); |
|
35 val Clique_superset = result(); |
|
36 |
|
37 goalw Ramsey.thy [Indept_def] "Indept(0,V,E)"; |
|
38 by (fast_tac ZF_cs 1); |
|
39 val Indept0 = result(); |
|
40 |
|
41 val prems = goalw Ramsey.thy [Indept_def] |
|
42 "!!I V E. [| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)"; |
|
43 by (fast_tac ZF_cs 1); |
|
44 val Indept_superset = result(); |
|
45 |
|
46 (*** Atleast ***) |
|
47 |
|
48 goalw Ramsey.thy [Atleast_def,inj_def] "Atleast(0,A)"; |
|
49 by (fast_tac (ZF_cs addIs [PiI]) 1); |
|
50 val Atleast0 = result(); |
|
51 |
|
52 val [major] = goalw Ramsey.thy [Atleast_def] |
|
53 "Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})"; |
|
54 by (rtac (major RS exE) 1); |
|
55 by (rtac bexI 1); |
|
56 by (etac (inj_is_fun RS apply_type) 2); |
|
57 by (rtac succI1 2); |
|
58 by (rtac exI 1); |
|
59 by (etac inj_succ_restrict 1); |
|
60 val Atleast_succD = result(); |
|
61 |
|
62 val major::prems = goalw Ramsey.thy [Atleast_def] |
|
63 "[| Atleast(n,A); A<=B |] ==> Atleast(n,B)"; |
|
64 by (rtac (major RS exE) 1); |
|
65 by (rtac exI 1); |
|
66 by (etac inj_weaken_type 1); |
|
67 by (resolve_tac prems 1); |
|
68 val Atleast_superset = result(); |
|
69 |
|
70 val prems = goalw Ramsey.thy [Atleast_def,succ_def] |
|
71 "[| Atleast(m,B); ~ b: B |] ==> Atleast(succ(m), cons(b,B))"; |
|
72 by (cut_facts_tac prems 1); |
|
73 by (etac exE 1); |
|
74 by (rtac exI 1); |
|
75 by (etac inj_extend 1); |
|
76 by (rtac mem_not_refl 1); |
|
77 by (assume_tac 1); |
|
78 val Atleast_succI = result(); |
|
79 |
|
80 val prems = goal Ramsey.thy |
|
81 "[| Atleast(m, B-{x}); x: B |] ==> Atleast(succ(m), B)"; |
|
82 by (cut_facts_tac prems 1); |
|
83 by (etac (Atleast_succI RS Atleast_superset) 1); |
|
84 by (fast_tac ZF_cs 1); |
|
85 by (fast_tac ZF_cs 1); |
|
86 val Atleast_Diff_succI = result(); |
|
87 |
|
88 (*** Main Cardinality Lemma ***) |
|
89 |
|
90 (*The #-succ(0) strengthens the original theorem statement, but precisely |
|
91 the same proof could be used!!*) |
|
92 val prems = goal Ramsey.thy |
|
93 "m: nat ==> \ |
|
94 \ ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) --> \ |
|
95 \ Atleast(m,A) | Atleast(n,B)"; |
|
96 by (nat_ind_tac "m" prems 1); |
|
97 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
|
98 by (ASM_SIMP_TAC ramsey_ss 1); |
|
99 by (rtac ballI 1); |
|
100 by (nat_ind_tac "n" [] 1); |
|
101 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
|
102 by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1); |
|
103 by (safe_tac ZF_cs); |
|
104 by (etac (Atleast_succD RS bexE) 1); |
|
105 by (etac UnE 1); |
|
106 (**case x:B. Instantiate the 'ALL A B' induction hypothesis. **) |
|
107 by (dres_inst_tac [("x1","A"), ("x","B-{x}")] (spec RS spec) 2); |
|
108 by (etac (mp RS disjE) 2); |
|
109 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*) |
|
110 by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3)); |
|
111 (*proving the condition*) |
|
112 by (etac Atleast_superset 2 THEN fast_tac ZF_cs 2); |
|
113 (**case x:A. Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **) |
|
114 by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")] |
|
115 (bspec RS spec RS spec) 1); |
|
116 by (etac nat_succI 1); |
|
117 by (etac (mp RS disjE) 1); |
|
118 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*) |
|
119 by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2)); |
|
120 (*proving the condition*) |
|
121 by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1); |
|
122 by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1); |
|
123 val pigeon2_lemma = result(); |
|
124 |
|
125 (* [| m:nat; n:nat; Atleast(m #+ n #- succ(0), A Un B) |] ==> |
|
126 Atleast(m,A) | Atleast(n,B) *) |
|
127 val pigeon2 = standard (pigeon2_lemma RS bspec RS spec RS spec RS mp); |
|
128 |
|
129 |
|
130 (**** Ramsey's Theorem ****) |
|
131 |
|
132 (** Base cases of induction; they now admit ANY Ramsey number **) |
|
133 |
|
134 goalw Ramsey.thy [Ramsey_def] "Ramsey(n,0,j)"; |
|
135 by (fast_tac (ZF_cs addIs [Clique0,Atleast0]) 1); |
|
136 val Ramsey0j = result(); |
|
137 |
|
138 goalw Ramsey.thy [Ramsey_def] "Ramsey(n,i,0)"; |
|
139 by (fast_tac (ZF_cs addIs [Indept0,Atleast0]) 1); |
|
140 val Ramseyi0 = result(); |
|
141 |
|
142 (** Lemmas for induction step **) |
|
143 |
|
144 (*The use of succ(m) here, rather than #-succ(0), simplifies the proof of |
|
145 Ramsey_step_lemma.*) |
|
146 val prems = goal Ramsey.thy |
|
147 "[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \ |
|
148 \ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})"; |
|
149 by (rtac (nat_succI RS pigeon2) 1); |
|
150 by (SIMP_TAC (ramsey_ss addrews prems) 3); |
|
151 by (rtac Atleast_superset 3); |
|
152 by (REPEAT (resolve_tac prems 1)); |
|
153 by (fast_tac ZF_cs 1); |
|
154 val Atleast_partition = result(); |
|
155 |
|
156 (*For the Atleast part, proves ~(a:I) from the second premise!*) |
|
157 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def] |
|
158 "[| Symmetric(E); Indept(I, {z: V-{a}. ~ <a,z>:E}, E); a: V; \ |
|
159 \ Atleast(j,I) |] ==> \ |
|
160 \ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))"; |
|
161 by (cut_facts_tac prems 1); |
|
162 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*34 secs*) |
|
163 val Indept_succ = result(); |
|
164 |
|
165 val prems = goalw Ramsey.thy [Symmetric_def,Clique_def] |
|
166 "[| Symmetric(E); Clique(C, {z: V-{a}. <a,z>:E}, E); a: V; \ |
|
167 \ Atleast(j,C) |] ==> \ |
|
168 \ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))"; |
|
169 by (cut_facts_tac prems 1); |
|
170 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*41 secs*) |
|
171 val Clique_succ = result(); |
|
172 |
|
173 (** Induction step **) |
|
174 |
|
175 (*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*) |
|
176 val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def] |
|
177 "[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); \ |
|
178 \ m: nat; n: nat |] ==> \ |
|
179 \ Ramsey(succ(m#+n), succ(i), succ(j))"; |
|
180 by (safe_tac ZF_cs); |
|
181 by (etac (Atleast_succD RS bexE) 1); |
|
182 by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1); |
|
183 by (REPEAT (resolve_tac prems 1)); |
|
184 (*case m*) |
|
185 by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1); |
|
186 by (fast_tac ZF_cs 1); |
|
187 by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*) |
|
188 by (safe_tac ZF_cs); |
|
189 by (eresolve_tac (swapify [exI]) 1); (*ignore main EX quantifier*) |
|
190 by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*) |
|
191 (*case n*) |
|
192 by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1); |
|
193 by (fast_tac ZF_cs 1); |
|
194 by (safe_tac ZF_cs); |
|
195 by (rtac exI 1); |
|
196 by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*) |
|
197 by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*) |
|
198 val Ramsey_step_lemma = result(); |
|
199 |
|
200 |
|
201 (** The actual proof **) |
|
202 |
|
203 (*Again, the induction requires Ramsey numbers to be positive.*) |
|
204 val prems = goal Ramsey.thy |
|
205 "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)"; |
|
206 by (nat_ind_tac "i" prems 1); |
|
207 by (fast_tac (ZF_cs addSIs [nat_0I,Ramsey0j]) 1); |
|
208 by (rtac ballI 1); |
|
209 by (nat_ind_tac "j" [] 1); |
|
210 by (fast_tac (ZF_cs addSIs [nat_0I,Ramseyi0]) 1); |
|
211 by (dres_inst_tac [("x","succ(j1)")] bspec 1); |
|
212 by (REPEAT (eresolve_tac [nat_succI,bexE] 1)); |
|
213 by (rtac bexI 1); |
|
214 by (rtac Ramsey_step_lemma 1); |
|
215 by (REPEAT (ares_tac [nat_succI,add_type] 1)); |
|
216 val ramsey_lemma = result(); |
|
217 |
|
218 (*Final statement in a tidy form, without succ(...) *) |
|
219 val prems = goal Ramsey.thy |
|
220 "[| i: nat; j: nat |] ==> EX n:nat. Ramsey(n,i,j)"; |
|
221 by (rtac (ramsey_lemma RS bspec RS bexE) 1); |
|
222 by (etac bexI 3); |
|
223 by (REPEAT (ares_tac (prems@[nat_succI]) 1)); |
|
224 val ramsey = result(); |
|
225 |
|
226 (*Computer Ramsey numbers according to proof above -- which, actually, |
|
227 does not constrain the base case values at all!*) |
|
228 fun ram 0 j = 1 |
|
229 | ram i 0 = 1 |
|
230 | ram i j = ram (i-1) j + ram i (j-1); |
|
231 |
|
232 (*Previous proof gave the following Ramsey numbers, which are smaller than |
|
233 those above by one!*) |
|
234 fun ram' 0 j = 0 |
|
235 | ram' i 0 = 0 |
|
236 | ram' i j = ram' (i-1) j + ram' i (j-1) + 1; |