1 (* Title: ZF/ex/ramsey.ML |
1 (* Title: ZF/ex/ramsey.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Ramsey's Theorem (finite exponent 2 version) |
6 Ramsey's Theorem (finite exponent 2 version) |
7 |
7 |
8 Based upon the article |
8 Based upon the article |
92 \ Atleast(m,A) | Atleast(n,B)"; |
92 \ Atleast(m,A) | Atleast(n,B)"; |
93 by (nat_ind_tac "m" prems 1); |
93 by (nat_ind_tac "m" prems 1); |
94 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
94 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
95 by (asm_simp_tac arith_ss 1); |
95 by (asm_simp_tac arith_ss 1); |
96 by (rtac ballI 1); |
96 by (rtac ballI 1); |
97 by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*) |
97 by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*) |
98 by (nat_ind_tac "n" [] 1); |
98 by (nat_ind_tac "n" [] 1); |
99 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
99 by (fast_tac (ZF_cs addSIs [Atleast0]) 1); |
100 by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1); |
100 by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1); |
101 by (safe_tac ZF_cs); |
101 by (safe_tac ZF_cs); |
102 by (etac (Atleast_succD RS bexE) 1); |
102 by (etac (Atleast_succD RS bexE) 1); |
155 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def] |
155 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def] |
156 "[| Symmetric(E); Indept(I, {z: V-{a}. <a,z> ~: E}, E); a: V; \ |
156 "[| Symmetric(E); Indept(I, {z: V-{a}. <a,z> ~: E}, E); a: V; \ |
157 \ Atleast(j,I) |] ==> \ |
157 \ Atleast(j,I) |] ==> \ |
158 \ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))"; |
158 \ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))"; |
159 by (cut_facts_tac prems 1); |
159 by (cut_facts_tac prems 1); |
160 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*34 secs*) |
160 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*34 secs*) |
161 qed "Indept_succ"; |
161 qed "Indept_succ"; |
162 |
162 |
163 val prems = goalw Ramsey.thy [Symmetric_def,Clique_def] |
163 val prems = goalw Ramsey.thy [Symmetric_def,Clique_def] |
164 "[| Symmetric(E); Clique(C, {z: V-{a}. <a,z>:E}, E); a: V; \ |
164 "[| Symmetric(E); Clique(C, {z: V-{a}. <a,z>:E}, E); a: V; \ |
165 \ Atleast(j,C) |] ==> \ |
165 \ Atleast(j,C) |] ==> \ |
182 (*case m*) |
182 (*case m*) |
183 by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1); |
183 by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1); |
184 by (fast_tac ZF_cs 1); |
184 by (fast_tac ZF_cs 1); |
185 by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*) |
185 by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*) |
186 by (safe_tac ZF_cs); |
186 by (safe_tac ZF_cs); |
187 by (eresolve_tac (swapify [exI]) 1); (*ignore main EX quantifier*) |
187 by (eresolve_tac (swapify [exI]) 1); (*ignore main EX quantifier*) |
188 by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*) |
188 by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*) |
189 (*case n*) |
189 (*case n*) |
190 by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1); |
190 by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1); |
191 by (fast_tac ZF_cs 1); |
191 by (fast_tac ZF_cs 1); |
192 by (safe_tac ZF_cs); |
192 by (safe_tac ZF_cs); |
193 by (rtac exI 1); |
193 by (rtac exI 1); |
194 by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*) |
194 by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*) |
195 by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*) |
195 by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*) |
196 qed "Ramsey_step_lemma"; |
196 qed "Ramsey_step_lemma"; |
197 |
197 |
198 |
198 |
199 (** The actual proof **) |
199 (** The actual proof **) |