# HG changeset patch
# User paulson
# Date 860662537 -7200
# Node ID 4eefc6c22d414a9804991e2fc8de6a9796ac8d1a
# Parent  c0e3f1ceabf25e368e2ce0805e101b57403e93b1
Changed some fast_tac to blast_tac

diff -r c0e3f1ceabf2 -r 4eefc6c22d41 src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Thu Apr 10 09:08:05 1997 +0200
+++ b/src/ZF/EquivClass.ML	Thu Apr 10 10:55:37 1997 +0200
@@ -16,17 +16,17 @@
 
 goalw EquivClass.thy [trans_def,sym_def]
     "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
-by (fast_tac (!claset) 1);
+by (Blast_tac 1);
 qed "sym_trans_comp_subset";
 
 goalw EquivClass.thy [refl_def]
     "!!A r. [| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
-by (fast_tac (!claset) 1);
+by (Blast_tac 1);
 qed "refl_comp_subset";
 
 goalw EquivClass.thy [equiv_def]
     "!!A r. equiv(A,r) ==> converse(r) O r = r";
-by (fast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
+by (blast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
 qed "equiv_comp_eq";
 
 (*second half*)
@@ -34,7 +34,7 @@
     "!!A r. [| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
-by (ALLGOALS (fast_tac (!claset)));
+by (ALLGOALS Fast_tac);
 qed "comp_equivI";
 
 (** Equivalence classes **)
@@ -42,25 +42,25 @@
 (*Lemma for the next result*)
 goalw EquivClass.thy [trans_def,sym_def]
     "!!A r. [| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_subset";
 
 goalw EquivClass.thy [equiv_def]
     "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
 by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
 by (rewtac sym_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_eq";
 
 goalw EquivClass.thy [equiv_def,refl_def]
     "!!A r. [| equiv(A,r);  a: A |] ==> a: r``{a}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_self";
 
 (*Lemma for the next result*)
 goalw EquivClass.thy [equiv_def,refl_def]
     "!!A r. [| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_equiv_class";
 
 val prems = goal EquivClass.thy
@@ -71,7 +71,7 @@
 (*thus r``{a} = r``{b} as well*)
 goalw EquivClass.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_nondisjoint";
 
 goalw EquivClass.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A";
@@ -80,13 +80,13 @@
 
 goal EquivClass.thy
     "!!A r. equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
-by (fast_tac (!claset addIs [eq_equiv_class, equiv_class_eq]
+by (blast_tac (!claset addIs [eq_equiv_class, equiv_class_eq]
                       addDs [equiv_type]) 1);
 qed "equiv_class_eq_iff";
 
 goal EquivClass.thy
     "!!A r. [| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
-by (fast_tac (!claset addIs [eq_equiv_class, equiv_class_eq]
+by (blast_tac (!claset addIs [eq_equiv_class, equiv_class_eq]
                       addDs [equiv_type]) 1);
 qed "eq_equiv_class_iff";
 
@@ -109,7 +109,7 @@
 
 goalw EquivClass.thy [equiv_def,refl_def,quotient_def]
     "!!A r. equiv(A,r) ==> Union(A/r) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Union_quotient";
 
 goalw EquivClass.thy [quotient_def]
@@ -117,7 +117,7 @@
 by (safe_tac (!claset addSIs [equiv_class_eq]));
 by (assume_tac 1);
 by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "quotient_disj";
 
 (**** Defining unary operations upon equivalence classes ****)
@@ -134,7 +134,7 @@
 by (etac equiv_class_self 2);
 by (assume_tac 2);
 by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_equiv_class";
 
 (*type checking of  UN x:r``{a}. b(x) *)
@@ -169,7 +169,7 @@
 
 goalw EquivClass.thy [congruent_def,congruent2_def,equiv_def,refl_def]
     "!!A r. [| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "congruent2_implies_congruent";
 
 val equivA::prems = goalw EquivClass.thy [congruent_def]
@@ -182,7 +182,7 @@
 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
                                      congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "congruent2_implies_congruent_UN";
 
 val prems as equivA::_ = goal EquivClass.thy
diff -r c0e3f1ceabf2 -r 4eefc6c22d41 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Thu Apr 10 09:08:05 1997 +0200
+++ b/src/ZF/Nat.ML	Thu Apr 10 10:55:37 1997 +0200
@@ -104,7 +104,7 @@
 by (rtac subset_imp_le 1);
 by (rtac subsetI 1);
 by (etac nat_induct 1);
-by (fast_tac (!claset addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
+by (blast_tac (!claset addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
 by (REPEAT (ares_tac [Limit_has_0 RS ltD,
                       Ord_nat, Limit_is_Ord] 1));
 qed "nat_le_Limit";
@@ -186,11 +186,11 @@
 (** nat_case **)
 
 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a";
-by (fast_tac (!claset addIs [the_equality]) 1);
+by (blast_tac (!claset addIs [the_equality]) 1);
 qed "nat_case_0";
 
 goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)";
-by (fast_tac (!claset addIs [the_equality]) 1);
+by (blast_tac (!claset addIs [the_equality]) 1);
 qed "nat_case_succ";
 
 Addsimps [nat_case_0, nat_case_succ];
diff -r c0e3f1ceabf2 -r 4eefc6c22d41 src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Thu Apr 10 09:08:05 1997 +0200
+++ b/src/ZF/Trancl.ML	Thu Apr 10 10:55:37 1997 +0200
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-For trancl.thy.  Transitive closure of a relation
+Transitive closure of a relation
 *)
 
 open Trancl;
@@ -11,7 +11,7 @@
 goal Trancl.thy "bnd_mono(field(r)*field(r), %s. id(field(r)) Un (r O s))";
 by (rtac bnd_monoI 1);
 by (REPEAT (ares_tac [subset_refl, Un_mono, comp_mono] 2));
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "rtrancl_bnd_mono";
 
 val [prem] = goalw Trancl.thy [rtrancl_def] "r<=s ==> r^* <= s^*";
@@ -51,11 +51,11 @@
 (*The premise ensures that r consists entirely of pairs*)
 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^*";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
+by (blast_tac (!claset addIs [r_into_rtrancl]) 1);
 qed "r_subset_rtrancl";
 
 goal Trancl.thy "field(r^*) = field(r)";
-by (fast_tac (!claset addIs [r_into_rtrancl] 
+by (blast_tac (!claset addIs [r_into_rtrancl] 
                     addSDs [rtrancl_type RS subsetD]) 1);
 qed "rtrancl_field";
 
@@ -131,7 +131,7 @@
 (*The premise ensures that r consists entirely of pairs*)
 val prems = goal Trancl.thy "r <= Sigma(A,B) ==> r <= r^+";
 by (cut_facts_tac prems 1);
-by (fast_tac (!claset addIs [r_into_trancl]) 1);
+by (blast_tac (!claset addIs [r_into_trancl]) 1);
 qed "r_subset_trancl";
 
 (*intro rule by definition: from r^* and r  *)
@@ -159,7 +159,7 @@
 (*by induction on this formula*)
 by (subgoal_tac "ALL z. <y,z> : r --> P(z)" 1);
 (*now solve first subgoal: this formula is sufficient*)
-by (Fast_tac 1);
+by (Blast_tac 1);
 by (etac rtrancl_induct 1);
 by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
 qed "trancl_induct";
@@ -174,11 +174,11 @@
 by (fast_tac (!claset addIs prems) 1);
 by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
 by (etac rtranclE 1);
-by (ALLGOALS (fast_tac (!claset addIs [rtrancl_into_trancl1])));
+by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_trancl1])));
 qed "tranclE";
 
 goalw Trancl.thy [trancl_def] "r^+ <= field(r)*field(r)";
-by (fast_tac (!claset addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
+by (blast_tac (!claset addEs [rtrancl_type RS subsetD RS SigmaE2]) 1);
 qed "trancl_type";
 
 val [prem] = goalw Trancl.thy [trancl_def] "r<=s ==> r^+ <= s^+";
diff -r c0e3f1ceabf2 -r 4eefc6c22d41 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Apr 10 09:08:05 1997 +0200
+++ b/src/ZF/Zorn.ML	Thu Apr 10 10:55:37 1997 +0200
@@ -74,7 +74,7 @@
 by (cut_facts_tac prems 1);
 by (rtac (major RS TFin_induct) 1);
 by (etac Union_lemma0 2);               (*or just Blast_tac*)
-by (fast_tac (subset_cs addIs [increasing_trans]) 1);
+by (blast_tac (subset_cs addIs [increasing_trans]) 1);
 qed "TFin_linear_lemma1";
 
 (*Lemma 2 of section 3.2.  Interesting in its own right!
@@ -88,7 +88,7 @@
 by (res_inst_tac [("n1","n"), ("m1","x")] 
     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
 by (dres_inst_tac [("x","n")] bspec 1 THEN assume_tac 1);
-by (fast_tac (subset_cs addIs [increasing_trans]) 1);
+by (blast_tac (subset_cs addIs [increasing_trans]) 1);
 by (REPEAT (ares_tac [disjI1,equalityI] 1));
 (*second induction step*)
 by (rtac (impI RS ballI) 1);
@@ -100,7 +100,7 @@
 by (set_mp_tac 1);
 by (res_inst_tac [("n1","n"), ("m1","x")] 
     (TFin_linear_lemma1 RS disjE) 1  THEN  REPEAT (assume_tac 1));
-by (fast_tac subset_cs 1);
+by (blast_tac subset_cs 1);
 by (rtac (ninc RS increasingD2 RS subset_trans RS disjI1) 1);
 by (REPEAT (ares_tac [TFin_is_subset] 1));
 qed "TFin_linear_lemma2";
@@ -119,7 +119,7 @@
 \           |] ==> n<=m | m<=n";
 by (rtac (TFin_linear_lemma2 RSN (3,TFin_linear_lemma1) RS disjE) 1);
 by (REPEAT (assume_tac 1) THEN etac disjI2 1);
-by (fast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
+by (blast_tac (subset_cs addIs [increasingD2 RS subset_trans, 
                                TFin_is_subset]) 1);
 qed "TFin_subset_linear";
 
@@ -132,7 +132,7 @@
 by (dtac TFin_subsetD 1);
 by (REPEAT (assume_tac 1));
 by (fast_tac (!claset addEs [ssubst]) 1);
-by (fast_tac (subset_cs addIs [TFin_is_subset]) 1);
+by (blast_tac (subset_cs addIs [TFin_is_subset]) 1);
 qed "equal_next_upper";
 
 (*Property 3.3 of section 3.3*)
@@ -146,7 +146,7 @@
 by (etac ssubst 1);
 by (rtac (increasingD2 RS equalityI) 1 THEN assume_tac 1);
 by (ALLGOALS
-    (fast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
+    (blast_tac (subset_cs addIs [TFin_UnionI, TFin_nextI, TFin_is_subset])));
 qed "equal_next_Union";
 
 
@@ -201,8 +201,8 @@
 by (rtac lam_type 1);
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (fast_tac (!claset addSIs [super_subset_chain RS subsetD,
-                            chain_subset_Pow RS subsetD,
-                            choice_super]) 1);
+			      chain_subset_Pow RS subsetD,
+			      choice_super]) 1);
 (*Now, verify that it increases*)
 by (asm_simp_tac (!simpset addsimps [Pow_iff, subset_refl]
                         setloop split_tac [expand_if]) 1);
@@ -340,7 +340,7 @@
     "!!S. [| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S        \
 \         |] ==> ch ` (S-X) : S-X";
 by (etac apply_type 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "choice_Diff";
 
 (*This justifies Definition 6.1*)
@@ -363,7 +363,7 @@
 (*Type checking is surprisingly hard!*)
 by (asm_simp_tac (!simpset addsimps [Pow_iff, cons_subset_iff, subset_refl]
                         setloop split_tac [expand_if]) 1);
-by (fast_tac (!claset addSIs [choice_Diff RS DiffD1]) 1);
+by (blast_tac (!claset addSIs [choice_Diff RS DiffD1]) 1);
 qed "Zermelo_next_exists";
 
 
@@ -377,12 +377,12 @@
 by (res_inst_tac [("d", "%y. ch`(S-y)")] lam_injective 1);
 by (rtac DiffI 1);
 by (resolve_tac [Collect_subset RS TFin_UnionI] 1);
-by (fast_tac (!claset addSIs [Collect_subset RS TFin_UnionI]
+by (blast_tac (!claset addSIs [Collect_subset RS TFin_UnionI]
                       addEs [equalityE]) 1);
 by (subgoal_tac "x ~: Union({y: TFin(S,next). x~: y})" 1);
-by (fast_tac (!claset addEs [equalityE]) 2);
+by (blast_tac (!claset addEs [equalityE]) 2);
 by (subgoal_tac "Union({y: TFin(S,next). x~: y}) ~= S" 1);
-by (fast_tac (!claset addEs [equalityE]) 2);
+by (blast_tac (!claset addEs [equalityE]) 2);
 (*For proving x : next`Union(...);
   Abrial & Laffitte's justification appears to be faulty.*)
 by (subgoal_tac "~ next ` Union({y: TFin(S,next). x~: y}) <= \
@@ -394,7 +394,7 @@
                      choice_Diff RS DiffD2]
            setloop split_tac [expand_if]) 2);
 by (subgoal_tac "x : next ` Union({y: TFin(S,next). x~: y})" 1);
-by (fast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
+by (blast_tac (subset_cs addSIs [Collect_subset RS TFin_UnionI, TFin_nextI]) 2);
 (*End of the lemmas!*)
 by (asm_full_simp_tac 
     (!simpset addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,