src/ZF/ex/Ramsey.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 438 52e8393ccd77
child 694 c7d592f6312a
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     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 (*** Cliques and Independent sets ***)
    24 
    25 goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
    26 by (fast_tac ZF_cs 1);
    27 val Clique0 = result();
    28 
    29 goalw Ramsey.thy [Clique_def]
    30     "!!C V E. [| Clique(C,V',E);  V'<=V |] ==> Clique(C,V,E)";
    31 by (fast_tac ZF_cs 1);
    32 val Clique_superset = result();
    33 
    34 goalw Ramsey.thy [Indept_def] "Indept(0,V,E)";
    35 by (fast_tac ZF_cs 1);
    36 val Indept0 = result();
    37 
    38 val prems = goalw Ramsey.thy [Indept_def]
    39     "!!I V E. [| Indept(I,V',E);  V'<=V |] ==> Indept(I,V,E)";
    40 by (fast_tac ZF_cs 1);
    41 val Indept_superset = result();
    42 
    43 (*** Atleast ***)
    44 
    45 goalw Ramsey.thy [Atleast_def,inj_def] "Atleast(0,A)";
    46 by (fast_tac (ZF_cs addIs [PiI]) 1);
    47 val Atleast0 = result();
    48 
    49 val [major] = goalw Ramsey.thy [Atleast_def]
    50     "Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})";
    51 by (rtac (major RS exE) 1);
    52 by (rtac bexI 1);
    53 by (etac (inj_is_fun RS apply_type) 2);
    54 by (rtac succI1 2);
    55 by (rtac exI 1);
    56 by (etac inj_succ_restrict 1);
    57 val Atleast_succD = result();
    58 
    59 val major::prems = goalw Ramsey.thy [Atleast_def]
    60     "[| Atleast(n,A);  A<=B |] ==> Atleast(n,B)";
    61 by (rtac (major RS exE) 1);
    62 by (rtac exI 1);
    63 by (etac inj_weaken_type 1);
    64 by (resolve_tac prems 1);
    65 val Atleast_superset = result();
    66 
    67 val prems = goalw Ramsey.thy [Atleast_def,succ_def]
    68     "[| Atleast(m,B);  b~: B |] ==> Atleast(succ(m), cons(b,B))";
    69 by (cut_facts_tac prems 1);
    70 by (etac exE 1);
    71 by (rtac exI 1);
    72 by (etac inj_extend 1);
    73 by (rtac mem_not_refl 1);
    74 by (assume_tac 1);
    75 val Atleast_succI = result();
    76 
    77 val prems = goal Ramsey.thy
    78     "[| Atleast(m, B-{x});  x: B |] ==> Atleast(succ(m), B)";
    79 by (cut_facts_tac prems 1);
    80 by (etac (Atleast_succI RS Atleast_superset) 1);
    81 by (fast_tac ZF_cs 1);
    82 by (fast_tac ZF_cs 1);
    83 val Atleast_Diff_succI = result();
    84 
    85 (*** Main Cardinality Lemma ***)
    86 
    87 (*The #-succ(0) strengthens the original theorem statement, but precisely
    88   the same proof could be used!!*)
    89 val prems = goal Ramsey.thy
    90     "m: nat ==> \
    91 \    ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
    92 \                         Atleast(m,A) | Atleast(n,B)";
    93 by (nat_ind_tac "m" prems 1);
    94 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
    95 by (asm_simp_tac arith_ss 1);
    96 by (rtac ballI 1);
    97 by (rename_tac "n" 1);		(*simplifier does NOT preserve bound names!*)
    98 by (nat_ind_tac "n" [] 1);
    99 by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
   100 by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
   101 by (safe_tac ZF_cs);
   102 by (etac (Atleast_succD RS bexE) 1);
   103 by (etac UnE 1);
   104 (**case x:B.  Instantiate the 'ALL A B' induction hypothesis. **)
   105 by (dres_inst_tac [("x1","A"), ("x","B-{x}")] (spec RS spec) 2);
   106 by (etac (mp RS disjE) 2);
   107 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
   108 by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
   109 (*proving the condition*)
   110 by (etac Atleast_superset 2 THEN fast_tac ZF_cs 2);
   111 (**case x:A.  Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
   112 by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")] 
   113     (bspec RS spec RS spec) 1);
   114 by (etac nat_succI 1);
   115 by (etac (mp RS disjE) 1);
   116 (*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
   117 by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
   118 (*proving the condition*)
   119 by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
   120 by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
   121 val pigeon2_lemma = result();
   122 
   123 (* [| m:nat;  n:nat;  Atleast(m #+ n #- succ(0), A Un B) |] ==> 
   124    Atleast(m,A) | Atleast(n,B) *)
   125 val pigeon2 = standard (pigeon2_lemma RS bspec RS spec RS spec RS mp);
   126 
   127 
   128 (**** Ramsey's Theorem ****)
   129 
   130 (** Base cases of induction; they now admit ANY Ramsey number **)
   131 
   132 goalw Ramsey.thy [Ramsey_def] "Ramsey(n,0,j)";
   133 by (fast_tac (ZF_cs addIs [Clique0,Atleast0]) 1);
   134 val Ramsey0j = result();
   135 
   136 goalw Ramsey.thy [Ramsey_def] "Ramsey(n,i,0)";
   137 by (fast_tac (ZF_cs addIs [Indept0,Atleast0]) 1);
   138 val Ramseyi0 = result();
   139 
   140 (** Lemmas for induction step **)
   141 
   142 (*The use of succ(m) here, rather than #-succ(0), simplifies the proof of 
   143   Ramsey_step_lemma.*)
   144 val prems = goal Ramsey.thy
   145     "[| Atleast(m #+ n, A);  m: nat;  n: nat |] ==> \
   146 \    Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
   147 by (rtac (nat_succI RS pigeon2) 1);
   148 by (simp_tac (arith_ss addsimps prems) 3);
   149 by (rtac Atleast_superset 3);
   150 by (REPEAT (resolve_tac prems 1));
   151 by (fast_tac ZF_cs 1);
   152 val Atleast_partition = result();
   153 
   154 (*For the Atleast part, proves ~(a:I) from the second premise!*)
   155 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
   156     "[| Symmetric(E);  Indept(I, {z: V-{a}. <a,z> ~: E}, E);  a: V;  \
   157 \       Atleast(j,I) |] ==>   \
   158 \    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
   159 by (cut_facts_tac prems 1);
   160 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1);	 (*34 secs*)
   161 val Indept_succ = result();
   162 
   163 val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
   164     "[| Symmetric(E);  Clique(C, {z: V-{a}. <a,z>:E}, E);  a: V;  \
   165 \       Atleast(j,C) |] ==>   \
   166 \    Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
   167 by (cut_facts_tac prems 1);
   168 by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1);  (*41 secs*)
   169 val Clique_succ = result();
   170 
   171 (** Induction step **)
   172 
   173 (*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
   174 val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def] 
   175    "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));  \
   176 \      m: nat;  n: nat |] ==> \
   177 \   Ramsey(succ(m#+n), succ(i), succ(j))";
   178 by (safe_tac ZF_cs);
   179 by (etac (Atleast_succD RS bexE) 1);
   180 by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
   181 by (REPEAT (resolve_tac prems 1));
   182 (*case m*)
   183 by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
   184 by (fast_tac ZF_cs 1);
   185 by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*)
   186 by (safe_tac ZF_cs);
   187 by (eresolve_tac (swapify [exI]) 1);		 (*ignore main EX quantifier*)
   188 by (REPEAT (ares_tac [Indept_succ] 1));  	 (*make a bigger Indept*)
   189 (*case n*)
   190 by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
   191 by (fast_tac ZF_cs 1);
   192 by (safe_tac ZF_cs);
   193 by (rtac exI 1);
   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*)
   196 val Ramsey_step_lemma = result();
   197 
   198 
   199 (** The actual proof **)
   200 
   201 (*Again, the induction requires Ramsey numbers to be positive.*)
   202 val prems = goal Ramsey.thy
   203     "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
   204 by (nat_ind_tac "i" prems 1);
   205 by (fast_tac (ZF_cs addSIs [nat_0I,Ramsey0j]) 1);
   206 by (rtac ballI 1);
   207 by (nat_ind_tac "j" [] 1);
   208 by (fast_tac (ZF_cs addSIs [nat_0I,Ramseyi0]) 1);
   209 by (dres_inst_tac [("x","succ(j1)")] bspec 1);
   210 by (REPEAT (eresolve_tac [nat_succI,bexE] 1));
   211 by (rtac bexI 1);
   212 by (rtac Ramsey_step_lemma 1);
   213 by (REPEAT (ares_tac [nat_succI,add_type] 1));
   214 val ramsey_lemma = result();
   215 
   216 (*Final statement in a tidy form, without succ(...) *)
   217 val prems = goal Ramsey.thy
   218     "[| i: nat;  j: nat |] ==> EX n:nat. Ramsey(n,i,j)";
   219 by (rtac (ramsey_lemma RS bspec RS bexE) 1);
   220 by (etac bexI 3);
   221 by (REPEAT (ares_tac (prems@[nat_succI]) 1));
   222 val ramsey = result();
   223 
   224 (*Compute Ramsey numbers according to proof above -- which, actually,
   225   does not constrain the base case values at all!*)
   226 fun ram 0 j = 1
   227   | ram i 0 = 1
   228   | ram i j = ram (i-1) j + ram i (j-1);
   229 
   230 (*Previous proof gave the following Ramsey numbers, which are smaller than
   231   those above by one!*)
   232 fun ram' 0 j = 0
   233   | ram' i 0 = 0
   234   | ram' i j = ram' (i-1) j + ram' i (j-1) + 1;