--- a/src/ZF/ex/Ramsey.ML Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/ex/Ramsey.ML Fri Jan 03 15:01:55 1997 +0100
@@ -23,42 +23,41 @@
(*** Cliques and Independent sets ***)
goalw Ramsey.thy [Clique_def] "Clique(0,V,E)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Clique0";
goalw Ramsey.thy [Clique_def]
"!!C V E. [| Clique(C,V',E); V'<=V |] ==> Clique(C,V,E)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Clique_superset";
goalw Ramsey.thy [Indept_def] "Indept(0,V,E)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Indept0";
val prems = goalw Ramsey.thy [Indept_def]
"!!I V E. [| Indept(I,V',E); V'<=V |] ==> Indept(I,V,E)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Indept_superset";
(*** Atleast ***)
goalw Ramsey.thy [Atleast_def, inj_def, Pi_def, function_def] "Atleast(0,A)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Atleast0";
goalw Ramsey.thy [Atleast_def]
"!!m A. Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})";
-by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
+by (fast_tac (!claset addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
qed "Atleast_succD";
goalw Ramsey.thy [Atleast_def]
"!!n A. [| Atleast(n,A); A<=B |] ==> Atleast(n,B)";
-by (fast_tac (ZF_cs addEs [inj_weaken_type]) 1);
+by (fast_tac (!claset addEs [inj_weaken_type]) 1);
qed "Atleast_superset";
-val prems = goalw Ramsey.thy [Atleast_def,succ_def]
- "[| Atleast(m,B); b~: B |] ==> Atleast(succ(m), cons(b,B))";
-by (cut_facts_tac prems 1);
+goalw Ramsey.thy [Atleast_def,succ_def]
+ "!!m. [| Atleast(m,B); b~: B |] ==> Atleast(succ(m), cons(b,B))";
by (etac exE 1);
by (rtac exI 1);
by (etac inj_extend 1);
@@ -66,12 +65,11 @@
by (assume_tac 1);
qed "Atleast_succI";
-val prems = goal Ramsey.thy
- "[| Atleast(m, B-{x}); x: B |] ==> Atleast(succ(m), B)";
-by (cut_facts_tac prems 1);
+goal Ramsey.thy
+ "!!m. [| Atleast(m, B-{x}); x: B |] ==> Atleast(succ(m), B)";
by (etac (Atleast_succI RS Atleast_superset) 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
qed "Atleast_Diff_succI";
(*** Main Cardinality Lemma ***)
@@ -83,14 +81,14 @@
\ ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) --> \
\ Atleast(m,A) | Atleast(n,B)";
by (nat_ind_tac "m" prems 1);
-by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (asm_simp_tac arith_ss 1);
+by (fast_tac (!claset addSIs [Atleast0]) 1);
+by (Asm_simp_tac 1);
by (rtac ballI 1);
by (rename_tac "n" 1); (*simplifier does NOT preserve bound names!*)
by (nat_ind_tac "n" [] 1);
-by (fast_tac (ZF_cs addSIs [Atleast0]) 1);
-by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
-by (safe_tac ZF_cs);
+by (fast_tac (!claset addSIs [Atleast0]) 1);
+by (asm_simp_tac (!simpset addsimps [add_succ_right]) 1);
+by (safe_tac (!claset));
by (etac (Atleast_succD RS bexE) 1);
by (etac UnE 1);
(**case x:B. Instantiate the 'ALL A B' induction hypothesis. **)
@@ -99,7 +97,7 @@
(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
(*proving the condition*)
-by (etac Atleast_superset 2 THEN fast_tac ZF_cs 2);
+by (etac Atleast_superset 2 THEN Fast_tac 2);
(**case x:A. Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
by (dres_inst_tac [("x2","succ(n1)"), ("x1","A-{x}"), ("x","B")]
(bspec RS spec RS spec) 1);
@@ -108,8 +106,8 @@
(*cases Atleast(succ(m1),A) and Atleast(succ(n1),B)*)
by (REPEAT (eresolve_tac [asm_rl, Atleast_Diff_succI, notE] 2));
(*proving the condition*)
-by (asm_simp_tac (arith_ss addsimps [add_succ_right]) 1);
-by (etac Atleast_superset 1 THEN fast_tac ZF_cs 1);
+by (asm_simp_tac (!simpset addsimps [add_succ_right]) 1);
+by (etac Atleast_superset 1 THEN Fast_tac 1);
qed "pigeon2_lemma";
(* [| m:nat; n:nat; Atleast(m #+ n #- succ(0), A Un B) |] ==>
@@ -122,11 +120,11 @@
(** Base cases of induction; they now admit ANY Ramsey number **)
goalw Ramsey.thy [Ramsey_def] "Ramsey(n,0,j)";
-by (fast_tac (ZF_cs addIs [Clique0,Atleast0]) 1);
+by (fast_tac (!claset addIs [Clique0,Atleast0]) 1);
qed "Ramsey0j";
goalw Ramsey.thy [Ramsey_def] "Ramsey(n,i,0)";
-by (fast_tac (ZF_cs addIs [Indept0,Atleast0]) 1);
+by (fast_tac (!claset addIs [Indept0,Atleast0]) 1);
qed "Ramseyi0";
(** Lemmas for induction step **)
@@ -137,10 +135,10 @@
"[| Atleast(m #+ n, A); m: nat; n: nat |] ==> \
\ Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
by (rtac (nat_succI RS pigeon2) 1);
-by (simp_tac (arith_ss addsimps prems) 3);
+by (simp_tac (!simpset addsimps prems) 3);
by (rtac Atleast_superset 3);
by (REPEAT (resolve_tac prems 1));
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "Atleast_partition";
(*For the Atleast part, proves ~(a:I) from the second premise!*)
@@ -149,7 +147,7 @@
\ Atleast(j,I) |] ==> \
\ Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
by (cut_facts_tac prems 1);
-by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*34 secs*)
+by (fast_tac (!claset addSEs [Atleast_succI]) 1); (*34 secs*)
qed "Indept_succ";
val prems = goalw Ramsey.thy [Symmetric_def,Clique_def]
@@ -157,7 +155,7 @@
\ Atleast(j,C) |] ==> \
\ Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
by (cut_facts_tac prems 1);
-by (fast_tac (ZF_cs addSEs [Atleast_succI]) 1); (*41 secs*)
+by (fast_tac (!claset addSEs [Atleast_succI]) 1); (*41 secs*)
qed "Clique_succ";
(** Induction step **)
@@ -167,24 +165,24 @@
"[| Ramsey(succ(m), succ(i), j); Ramsey(n, i, succ(j)); \
\ m: nat; n: nat |] ==> \
\ Ramsey(succ(m#+n), succ(i), succ(j))";
-by (safe_tac ZF_cs);
+by (safe_tac (!claset));
by (etac (Atleast_succD RS bexE) 1);
by (eres_inst_tac [("P1","%z.<x,z>:E")] (Atleast_partition RS disjE) 1);
by (REPEAT (resolve_tac prems 1));
(*case m*)
by (rtac (ram1 RS spec RS spec RS mp RS disjE) 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac (ZF_cs addEs [Clique_superset]) 1); (*easy -- given a Clique*)
-by (safe_tac ZF_cs);
+by (Fast_tac 1);
+by (fast_tac (!claset addEs [Clique_superset]) 1); (*easy -- given a Clique*)
+by (safe_tac (!claset));
by (eresolve_tac (swapify [exI]) 1); (*ignore main EX quantifier*)
by (REPEAT (ares_tac [Indept_succ] 1)); (*make a bigger Indept*)
(*case n*)
by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
-by (fast_tac ZF_cs 1);
-by (safe_tac ZF_cs);
+by (Fast_tac 1);
+by (safe_tac (!claset));
by (rtac exI 1);
by (REPEAT (ares_tac [Clique_succ] 1)); (*make a bigger Clique*)
-by (fast_tac (ZF_cs addEs [Indept_superset]) 1); (*easy -- given an Indept*)
+by (fast_tac (!claset addEs [Indept_superset]) 1); (*easy -- given an Indept*)
qed "Ramsey_step_lemma";
@@ -194,16 +192,17 @@
val prems = goal Ramsey.thy
"i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
by (nat_ind_tac "i" prems 1);
-by (fast_tac (ZF_cs addSIs [nat_0I,Ramsey0j]) 1);
+by (fast_tac (!claset addSIs [Ramsey0j]) 1);
by (rtac ballI 1);
by (nat_ind_tac "j" [] 1);
-by (fast_tac (ZF_cs addSIs [nat_0I,Ramseyi0]) 1);
-by (fast_tac (ZF_cs addSIs [nat_succI,add_type,Ramsey_step_lemma]) 1);
+by (fast_tac (!claset addSIs [Ramseyi0]) 1);
+by (fast_tac (!claset addSDs [bspec]
+ addSIs [nat_succI,add_type,Ramsey_step_lemma]) 1);
qed "ramsey_lemma";
(*Final statement in a tidy form, without succ(...) *)
goal Ramsey.thy "!!i j. [| i: nat; j: nat |] ==> EX n:nat. Ramsey(n,i,j)";
-by (best_tac (ZF_cs addDs [ramsey_lemma] addSIs [nat_succI]) 1);
+by (best_tac (!claset addDs [ramsey_lemma] addSIs [nat_succI]) 1);
qed "ramsey";
(*Compute Ramsey numbers according to proof above -- which, actually,