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
     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;