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