author | wenzelm |
Mon, 17 Sep 2007 16:36:41 +0200 | |
changeset 24612 | d1b315bdb8d7 |
parent 21404 | eb85850d3eb7 |
child 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/ramsey.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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. |
|
12867 | 12 |
(CUP, 1991), pages 89-119 |
0 | 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 |
|
12867 | 19 |
|
20 |
This function compute Ramsey numbers according to the proof given below |
|
21 |
(which, does not constrain the base case values at all. |
|
22 |
||
23 |
fun ram 0 j = 1 |
|
24 |
| ram i 0 = 1 |
|
25 |
| ram i j = ram (i-1) j + ram i (j-1) |
|
26 |
||
0 | 27 |
*) |
28 |
||
16417 | 29 |
theory Ramsey imports Main begin |
21233 | 30 |
|
31 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
32 |
Symmetric :: "i=>o" where |
12867 | 33 |
"Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)" |
34 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
35 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
36 |
Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality" |
12867 | 37 |
"Atleast(n,S) == (\<exists>f. f \<in> inj(n,S))" |
38 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
39 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
40 |
Clique :: "[i,i,i]=>o" where |
12867 | 41 |
"Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y --> <x,y> \<in> E)" |
42 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
43 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
44 |
Indept :: "[i,i,i]=>o" where |
12867 | 45 |
"Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y --> <x,y> \<notin> E)" |
46 |
||
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
47 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21233
diff
changeset
|
48 |
Ramsey :: "[i,i,i]=>o" where |
12867 | 49 |
"Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) --> |
50 |
(\<exists>C. Clique(C,V,E) & Atleast(i,C)) | |
|
51 |
(\<exists>I. Indept(I,V,E) & Atleast(j,I))" |
|
52 |
||
53 |
(*** Cliques and Independent sets ***) |
|
54 |
||
55 |
lemma Clique0 [intro]: "Clique(0,V,E)" |
|
56 |
by (unfold Clique_def, blast) |
|
57 |
||
58 |
lemma Clique_superset: "[| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)" |
|
59 |
by (unfold Clique_def, blast) |
|
60 |
||
61 |
lemma Indept0 [intro]: "Indept(0,V,E)" |
|
62 |
by (unfold Indept_def, blast) |
|
0 | 63 |
|
12867 | 64 |
lemma Indept_superset: "[| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)" |
65 |
by (unfold Indept_def, blast) |
|
66 |
||
67 |
(*** Atleast ***) |
|
68 |
||
69 |
lemma Atleast0 [intro]: "Atleast(0,A)" |
|
70 |
by (unfold Atleast_def inj_def Pi_def function_def, blast) |
|
71 |
||
72 |
lemma Atleast_succD: |
|
73 |
"Atleast(succ(m),A) ==> \<exists>x \<in> A. Atleast(m, A-{x})" |
|
74 |
apply (unfold Atleast_def) |
|
75 |
apply (blast dest: inj_is_fun [THEN apply_type] inj_succ_restrict) |
|
76 |
done |
|
0 | 77 |
|
12867 | 78 |
lemma Atleast_superset: |
79 |
"[| Atleast(n,A); A \<subseteq> B |] ==> Atleast(n,B)" |
|
80 |
by (unfold Atleast_def, blast intro: inj_weaken_type) |
|
81 |
||
82 |
lemma Atleast_succI: |
|
83 |
"[| Atleast(m,B); b\<notin> B |] ==> Atleast(succ(m), cons(b,B))" |
|
84 |
apply (unfold Atleast_def succ_def) |
|
85 |
apply (blast intro: inj_extend elim: mem_irrefl) |
|
86 |
done |
|
87 |
||
88 |
lemma Atleast_Diff_succI: |
|
89 |
"[| Atleast(m, B-{x}); x \<in> B |] ==> Atleast(succ(m), B)" |
|
90 |
by (blast intro: Atleast_succI [THEN Atleast_superset]) |
|
91 |
||
92 |
(*** Main Cardinality Lemma ***) |
|
0 | 93 |
|
12867 | 94 |
(*The #-succ(0) strengthens the original theorem statement, but precisely |
95 |
the same proof could be used!!*) |
|
96 |
lemma pigeon2 [rule_format]: |
|
97 |
"m \<in> nat ==> |
|
98 |
\<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A Un B) --> |
|
99 |
Atleast(m,A) | Atleast(n,B)" |
|
100 |
apply (induct_tac "m") |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
101 |
apply (blast intro!: Atleast0, simp) |
12867 | 102 |
apply (rule ballI) |
103 |
apply (rename_tac m' n) (*simplifier does NOT preserve bound names!*) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
104 |
apply (induct_tac "n", auto) |
12867 | 105 |
apply (erule Atleast_succD [THEN bexE]) |
106 |
apply (rename_tac n' A B z) |
|
107 |
apply (erule UnE) |
|
108 |
(**case z \<in> B. Instantiate the '\<forall>A B' induction hypothesis. **) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
109 |
apply (drule_tac [2] x1 = A and x = "B-{z}" in spec [THEN spec]) |
12867 | 110 |
apply (erule_tac [2] mp [THEN disjE]) |
111 |
(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) |
|
112 |
apply (erule_tac [3] asm_rl notE Atleast_Diff_succI)+ |
|
113 |
(*proving the condition*) |
|
114 |
prefer 2 apply (blast intro: Atleast_superset) |
|
115 |
(**case z \<in> A. Instantiate the '\<forall>n \<in> nat. \<forall>A B' induction hypothesis. **) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
116 |
apply (drule_tac x2="succ(n')" and x1="A-{z}" and x=B |
12867 | 117 |
in bspec [THEN spec, THEN spec]) |
118 |
apply (erule nat_succI) |
|
119 |
apply (erule mp [THEN disjE]) |
|
120 |
(*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
121 |
apply (erule_tac [2] asm_rl Atleast_Diff_succI notE)+ |
12867 | 122 |
(*proving the condition*) |
123 |
apply simp |
|
124 |
apply (blast intro: Atleast_superset) |
|
125 |
done |
|
0 | 126 |
|
12867 | 127 |
|
128 |
(**** Ramsey's Theorem ****) |
|
129 |
||
130 |
(** Base cases of induction; they now admit ANY Ramsey number **) |
|
131 |
||
132 |
lemma Ramsey0j: "Ramsey(n,0,j)" |
|
133 |
by (unfold Ramsey_def, blast) |
|
134 |
||
135 |
lemma Ramseyi0: "Ramsey(n,i,0)" |
|
136 |
by (unfold Ramsey_def, blast) |
|
137 |
||
138 |
(** Lemmas for induction step **) |
|
0 | 139 |
|
12867 | 140 |
(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of |
141 |
Ramsey_step_lemma.*) |
|
142 |
lemma Atleast_partition: "[| Atleast(m #+ n, A); m \<in> nat; n \<in> nat |] |
|
143 |
==> Atleast(succ(m), {x \<in> A. ~P(x)}) | Atleast(n, {x \<in> A. P(x)})" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
144 |
apply (rule nat_succI [THEN pigeon2], assumption+) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
145 |
apply (rule Atleast_superset, auto) |
12867 | 146 |
done |
147 |
||
148 |
(*For the Atleast part, proves ~(a \<in> I) from the second premise!*) |
|
149 |
lemma Indept_succ: |
|
150 |
"[| Indept(I, {z \<in> V-{a}. <a,z> \<notin> E}, E); Symmetric(E); a \<in> V; |
|
151 |
Atleast(j,I) |] ==> |
|
152 |
Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))" |
|
153 |
apply (unfold Symmetric_def Indept_def) |
|
154 |
apply (blast intro!: Atleast_succI) |
|
155 |
done |
|
156 |
||
157 |
||
158 |
lemma Clique_succ: |
|
159 |
"[| Clique(C, {z \<in> V-{a}. <a,z>:E}, E); Symmetric(E); a \<in> V; |
|
160 |
Atleast(j,C) |] ==> |
|
161 |
Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))" |
|
162 |
apply (unfold Symmetric_def Clique_def) |
|
163 |
apply (blast intro!: Atleast_succI) |
|
164 |
done |
|
165 |
||
166 |
(** Induction step **) |
|
0 | 167 |
|
12867 | 168 |
(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*) |
169 |
lemma Ramsey_step_lemma: |
|
170 |
"[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); |
|
171 |
m \<in> nat; n \<in> nat |] ==> Ramsey(succ(m#+n), succ(i), succ(j))" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
172 |
apply (unfold Ramsey_def, clarify) |
12867 | 173 |
apply (erule Atleast_succD [THEN bexE]) |
174 |
apply (erule_tac P1 = "%z.<x,z>:E" in Atleast_partition [THEN disjE], |
|
175 |
assumption+) |
|
176 |
(*case m*) |
|
177 |
apply (fast dest!: Indept_succ elim: Clique_superset) |
|
178 |
(*case n*) |
|
179 |
apply (fast dest!: Clique_succ elim: Indept_superset) |
|
180 |
done |
|
181 |
||
182 |
||
183 |
(** The actual proof **) |
|
184 |
||
185 |
(*Again, the induction requires Ramsey numbers to be positive.*) |
|
186 |
lemma ramsey_lemma: "i \<in> nat ==> \<forall>j \<in> nat. \<exists>n \<in> nat. Ramsey(succ(n), i, j)" |
|
187 |
apply (induct_tac "i") |
|
188 |
apply (blast intro!: Ramsey0j) |
|
189 |
apply (rule ballI) |
|
190 |
apply (induct_tac "j") |
|
191 |
apply (blast intro!: Ramseyi0) |
|
192 |
apply (blast intro!: add_type Ramsey_step_lemma) |
|
193 |
done |
|
194 |
||
195 |
(*Final statement in a tidy form, without succ(...) *) |
|
196 |
lemma ramsey: "[| i \<in> nat; j \<in> nat |] ==> \<exists>n \<in> nat. Ramsey(n,i,j)" |
|
197 |
by (blast dest: ramsey_lemma) |
|
0 | 198 |
|
199 |
end |