|
0
|
1 |
(* Title: ZF/ex/ramsey.thy
|
|
|
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 |
Ramsey = Arith +
|
|
|
22 |
consts
|
|
|
23 |
Symmetric :: "i=>o"
|
|
|
24 |
Atleast :: "[i,i]=>o"
|
|
|
25 |
Clique,Indept,Ramsey :: "[i,i,i]=>o"
|
|
|
26 |
|
|
|
27 |
rules
|
|
|
28 |
|
|
|
29 |
Symmetric_def
|
|
|
30 |
"Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
|
|
|
31 |
|
|
|
32 |
Clique_def
|
|
38
|
33 |
"Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. x~=y --> <x,y> : E)"
|
|
0
|
34 |
|
|
|
35 |
Indept_def
|
|
38
|
36 |
"Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. x~=y --> <x,y> ~: E)"
|
|
0
|
37 |
|
|
|
38 |
Atleast_def
|
|
|
39 |
"Atleast(n,S) == (EX f. f: inj(n,S))"
|
|
|
40 |
|
|
|
41 |
Ramsey_def
|
|
|
42 |
"Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) --> \
|
|
|
43 |
\ (EX C. Clique(C,V,E) & Atleast(i,C)) | \
|
|
|
44 |
\ (EX I. Indept(I,V,E) & Atleast(j,I))"
|
|
|
45 |
|
|
|
46 |
end
|