--- 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
--- 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];
--- 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^+";
--- 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,