src/ZF/ex/ramsey.ML
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/ramsey.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,236 @@
     1.4 +(*  Title: 	ZF/ex/ramsey.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Ramsey's Theorem (finite exponent 2 version)
    1.10 +
    1.11 +Based upon the article
    1.12 +    D Basin and M Kaufmann,
    1.13 +    The Boyer-Moore Prover and Nuprl: An Experimental Comparison.
    1.14 +    In G Huet and G Plotkin, editors, Logical Frameworks.
    1.15 +    (CUP, 1991), pages 89--119
    1.16 +
    1.17 +See also
    1.18 +    M Kaufmann,
    1.19 +    An example in NQTHM: Ramsey's Theorem
    1.20 +    Internal Note, Computational Logic, Inc., Austin, Texas 78703
    1.21 +    Available from the author: kaufmann@cli.com
    1.22 +*)
    1.23 +
    1.24 +open Ramsey;
    1.25 +
    1.26 +val ramsey_congs = mk_congs Ramsey.thy ["Atleast"];
    1.27 +val ramsey_ss = arith_ss addcongs ramsey_congs;
    1.28 +
    1.29 +(*** Cliques and Independent sets ***)
    1.30 +
    1.31 +goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
    1.32 +by (fast_tac ZF_cs 1);
    1.33 +val Clique0 = result();
    1.34 +
    1.35 +goalw Ramsey.thy [Clique_def]
    1.36 +    "!!C V E. [| Clique(C,V',E);  V'<=V |] ==> Clique(C,V,E)";
    1.37 +by (fast_tac ZF_cs 1);
    1.38 +val Clique_superset = result();
    1.39 +
    1.40 +goalw Ramsey.thy [Indept_def] "Indept(0,V,E)";
    1.41 +by (fast_tac ZF_cs 1);
    1.42 +val Indept0 = result();
    1.43 +
    1.44 +val prems = goalw Ramsey.thy [Indept_def]
    1.45 +    "!!I V E. [| Indept(I,V',E);  V'<=V |] ==> Indept(I,V,E)";
    1.46 +by (fast_tac ZF_cs 1);
    1.47 +val Indept_superset = result();
    1.48 +
    1.49 +(*** Atleast ***)
    1.50 +
    1.51 +goalw Ramsey.thy [Atleast_def,inj_def] "Atleast(0,A)";
    1.52 +by (fast_tac (ZF_cs addIs [PiI]) 1);
    1.53 +val Atleast0 = result();
    1.54 +
    1.55 +val [major] = goalw Ramsey.thy [Atleast_def]
    1.56 +    "Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})";
    1.57 +by (rtac (major RS exE) 1);
    1.58 +by (rtac bexI 1);
    1.59 +by (etac (inj_is_fun RS apply_type) 2);
    1.60 +by (rtac succI1 2);
    1.61 +by (rtac exI 1);
    1.62 +by (etac inj_succ_restrict 1);
    1.63 +val Atleast_succD = result();
    1.64 +
    1.65 +val major::prems = goalw Ramsey.thy [Atleast_def]
    1.66 +    "[| Atleast(n,A);  A<=B |] ==> Atleast(n,B)";
    1.67 +by (rtac (major RS exE) 1);
    1.68 +by (rtac exI 1);
    1.69 +by (etac inj_weaken_type 1);
    1.70 +by (resolve_tac prems 1);
    1.71 +val Atleast_superset = result();
    1.72 +
    1.73 +val prems = goalw Ramsey.thy [Atleast_def,succ_def]
    1.74 +    "[| Atleast(m,B);  ~ b: B |] ==> Atleast(succ(m), cons(b,B))";
    1.75 +by (cut_facts_tac prems 1);
    1.76 +by (etac exE 1);
    1.77 +by (rtac exI 1);
    1.78 +by (etac inj_extend 1);
    1.79 +by (rtac mem_not_refl 1);
    1.80 +by (assume_tac 1);
    1.81 +val Atleast_succI = result();
    1.82 +
    1.83 +val prems = goal Ramsey.thy
    1.84 +    "[| Atleast(m, B-{x});  x: B |] ==> Atleast(succ(m), B)";
    1.85 +by (cut_facts_tac prems 1);
    1.86 +by (etac (Atleast_succI RS Atleast_superset) 1);
    1.87 +by (fast_tac ZF_cs 1);
    1.88 +by (fast_tac ZF_cs 1);
    1.89 +val Atleast_Diff_succI = result();
    1.90 +
    1.91 +(*** Main Cardinality Lemma ***)
    1.92 +
    1.93 +(*The #-succ(0) strengthens the original theorem statement, but precisely
    1.94 +  the same proof could be used!!*)
    1.95 +val prems = goal Ramsey.thy
    1.96 +    "m: nat ==> \
    1.97 +\    ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
    1.98 +\                         Atleast(m,A) | Atleast(n,B)";
    1.99 +by (nat_ind_tac "m" prems 1);
   1.100 +by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
   1.101 +by (ASM_SIMP_TAC ramsey_ss 1);
   1.102 +by (rtac ballI 1);
   1.103 +by (nat_ind_tac "n" [] 1);
   1.104 +by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
   1.105 +by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
   1.106 +by (safe_tac ZF_cs);
   1.107 +by (etac (Atleast_succD RS bexE) 1);
   1.108 +by (etac UnE 1);
   1.109 +(**case x:B.  Instantiate the 'ALL A B' induction hypothesis. **)
   1.110 +by (dres_inst_tac [("x1","A"), ("x","B-{x}")] (spec RS spec) 2);
   1.111 +by (etac (mp RS disjE) 2);
   1.112 +(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
   1.113 +by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
   1.114 +(*proving the condition*)
   1.115 +by (etac Atleast_superset 2 THEN fast_tac ZF_cs 2);
   1.116 +(**case x:A.  Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
   1.117 +by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")] 
   1.118 +    (bspec RS spec RS spec) 1);
   1.119 +by (etac nat_succI 1);
   1.120 +by (etac (mp RS disjE) 1);
   1.121 +(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
   1.122 +by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
   1.123 +(*proving the condition*)
   1.124 +by (ASM_SIMP_TAC (ramsey_ss addrews [add_succ_right]) 1);
   1.125 +by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
   1.126 +val pigeon2_lemma = result();
   1.127 +
   1.128 +(* [| m:nat;  n:nat;  Atleast(m #+ n #- succ(0), A Un B) |] ==> 
   1.129 +   Atleast(m,A) | Atleast(n,B) *)
   1.130 +val pigeon2 = standard (pigeon2_lemma RS bspec RS spec RS spec RS mp);
   1.131 +
   1.132 +
   1.133 +(**** Ramsey's Theorem ****)
   1.134 +
   1.135 +(** Base cases of induction; they now admit ANY Ramsey number **)
   1.136 +
   1.137 +goalw Ramsey.thy [Ramsey_def] "Ramsey(n,0,j)";
   1.138 +by (fast_tac (ZF_cs addIs [Clique0,Atleast0]) 1);
   1.139 +val Ramsey0j = result();
   1.140 +
   1.141 +goalw Ramsey.thy [Ramsey_def] "Ramsey(n,i,0)";
   1.142 +by (fast_tac (ZF_cs addIs [Indept0,Atleast0]) 1);
   1.143 +val Ramseyi0 = result();
   1.144 +
   1.145 +(** Lemmas for induction step **)
   1.146 +
   1.147 +(*The use of succ(m) here, rather than #-succ(0), simplifies the proof of 
   1.148 +  Ramsey_step_lemma.*)
   1.149 +val prems = goal Ramsey.thy
   1.150 +    "[| Atleast(m #+ n, A);  m: nat;  n: nat |] ==> \
   1.151 +\    Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
   1.152 +by (rtac (nat_succI RS pigeon2) 1);
   1.153 +by (SIMP_TAC (ramsey_ss addrews prems) 3);
   1.154 +by (rtac Atleast_superset 3);
   1.155 +by (REPEAT (resolve_tac prems 1));
   1.156 +by (fast_tac ZF_cs 1);
   1.157 +val Atleast_partition = result();
   1.158 +
   1.159 +(*For the Atleast part, proves ~(a:I) from the second premise!*)
   1.160 +val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
   1.161 +    "[| Symmetric(E);  Indept(I, {z: V-{a}. ~ <a,z>:E}, E);  a: V;  \
   1.162 +\       Atleast(j,I) |] ==>   \
   1.163 +\    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
   1.164 +by (cut_facts_tac prems 1);
   1.165 +by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1);	 (*34 secs*)
   1.166 +val Indept_succ = result();
   1.167 +
   1.168 +val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
   1.169 +    "[| Symmetric(E);  Clique(C, {z: V-{a}. <a,z>:E}, E);  a: V;  \
   1.170 +\       Atleast(j,C) |] ==>   \
   1.171 +\    Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
   1.172 +by (cut_facts_tac prems 1);
   1.173 +by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1);  (*41 secs*)
   1.174 +val Clique_succ = result();
   1.175 +
   1.176 +(** Induction step **)
   1.177 +
   1.178 +(*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
   1.179 +val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def] 
   1.180 +   "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));  \
   1.181 +\      m: nat;  n: nat |] ==> \
   1.182 +\   Ramsey(succ(m#+n), succ(i), succ(j))";
   1.183 +by (safe_tac ZF_cs);
   1.184 +by (etac (Atleast_succD RS bexE) 1);
   1.185 +by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
   1.186 +by (REPEAT (resolve_tac prems 1));
   1.187 +(*case m*)
   1.188 +by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
   1.189 +by (fast_tac ZF_cs 1);
   1.190 +by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*)
   1.191 +by (safe_tac ZF_cs);
   1.192 +by (eresolve_tac (swapify [exI]) 1);		 (*ignore main EX quantifier*)
   1.193 +by (REPEAT (ares_tac [Indept_succ] 1));  	 (*make a bigger Indept*)
   1.194 +(*case n*)
   1.195 +by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
   1.196 +by (fast_tac ZF_cs 1);
   1.197 +by (safe_tac ZF_cs);
   1.198 +by (rtac exI 1);
   1.199 +by (REPEAT (ares_tac [Clique_succ] 1));  	 (*make a bigger Clique*)
   1.200 +by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*)
   1.201 +val Ramsey_step_lemma = result();
   1.202 +
   1.203 +
   1.204 +(** The actual proof **)
   1.205 +
   1.206 +(*Again, the induction requires Ramsey numbers to be positive.*)
   1.207 +val prems = goal Ramsey.thy
   1.208 +    "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
   1.209 +by (nat_ind_tac "i" prems 1);
   1.210 +by (fast_tac (ZF_cs addSIs [nat_0I,Ramsey0j]) 1);
   1.211 +by (rtac ballI 1);
   1.212 +by (nat_ind_tac "j" [] 1);
   1.213 +by (fast_tac (ZF_cs addSIs [nat_0I,Ramseyi0]) 1);
   1.214 +by (dres_inst_tac [("x","succ(j1)")] bspec 1);
   1.215 +by (REPEAT (eresolve_tac [nat_succI,bexE] 1));
   1.216 +by (rtac bexI 1);
   1.217 +by (rtac Ramsey_step_lemma 1);
   1.218 +by (REPEAT (ares_tac [nat_succI,add_type] 1));
   1.219 +val ramsey_lemma = result();
   1.220 +
   1.221 +(*Final statement in a tidy form, without succ(...) *)
   1.222 +val prems = goal Ramsey.thy
   1.223 +    "[| i: nat;  j: nat |] ==> EX n:nat. Ramsey(n,i,j)";
   1.224 +by (rtac (ramsey_lemma RS bspec RS bexE) 1);
   1.225 +by (etac bexI 3);
   1.226 +by (REPEAT (ares_tac (prems@[nat_succI]) 1));
   1.227 +val ramsey = result();
   1.228 +
   1.229 +(*Computer Ramsey numbers according to proof above -- which, actually,
   1.230 +  does not constrain the base case values at all!*)
   1.231 +fun ram 0 j = 1
   1.232 +  | ram i 0 = 1
   1.233 +  | ram i j = ram (i-1) j + ram i (j-1);
   1.234 +
   1.235 +(*Previous proof gave the following Ramsey numbers, which are smaller than
   1.236 +  those above by one!*)
   1.237 +fun ram' 0 j = 0
   1.238 +  | ram' i 0 = 0
   1.239 +  | ram' i j = ram' (i-1) j + ram' i (j-1) + 1;