--- a/src/ZF/AC.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/AC.ML Wed Apr 23 10:54:22 1997 +0200
@@ -12,9 +12,9 @@
val [nonempty] = goal AC.thy
"[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)";
by (excluded_middle_tac "A=0" 1);
-by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Fast_tac 2);
+by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Blast_tac 2);
(*The non-trivial case*)
-by (fast_tac (!claset addIs [AC, nonempty]) 1);
+by (blast_tac (!claset addIs [AC, nonempty]) 1);
qed "AC_Pi";
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
@@ -27,7 +27,7 @@
goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
by (etac exI 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "AC_Pi_Pow";
val [nonempty] = goal AC.thy
@@ -35,12 +35,12 @@
\ |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
by (etac nonempty 1);
-by (fast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
+by (blast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
qed "AC_func";
goal ZF.thy "!!x A. [| 0 ~: A; x: A |] ==> EX y. y:x";
by (subgoal_tac "x ~= 0" 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
qed "non_empty_family";
goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
@@ -53,7 +53,7 @@
by (rtac bexI 2);
by (assume_tac 2);
by (etac fun_weaken_type 2);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
qed "AC_func_Pow";
goal AC.thy "!!A. 0 ~: A ==> EX f. f: (PROD x:A. x)";
--- a/src/ZF/Arith.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Arith.ML Wed Apr 23 10:54:22 1997 +0200
@@ -51,7 +51,7 @@
by (etac rev_mp 1);
by (etac nat_induct 1);
by (Simp_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
val lemma = result();
(* [| 0 < k; k: nat; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
@@ -428,7 +428,7 @@
by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);
by (dtac ltD 1);
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "mod2_cases";
goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
@@ -483,7 +483,7 @@
\ i le j; j:k \
\ |] ==> f(i) le f(j)";
by (cut_facts_tac prems 1);
-by (fast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
+by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
qed "Ord_lt_mono_imp_le_mono";
(*le monotonicity, 1st argument*)
@@ -586,7 +586,7 @@
goal Arith.thy (* add_le_elim1 *)
"!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
by (etac rev_mp 1);
-by (eres_inst_tac[("n","n")]nat_induct 1);
+by (eres_inst_tac [("n","n")] nat_induct 1);
by (Asm_simp_tac 1);
by (Step_tac 1);
by (asm_full_simp_tac (!simpset addsimps [not_le_iff_lt,nat_into_Ord]) 1);
@@ -594,6 +594,6 @@
by (assume_tac 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (!simpset addsimps [le_iff, nat_into_Ord]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "add_le_elim1";
--- a/src/ZF/Cardinal.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Cardinal.ML Wed Apr 23 10:54:22 1997 +0200
@@ -159,8 +159,8 @@
by (safe_tac (claset_of"ZF"));
by (swap_res_tac [exI] 1);
by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1);
-by (fast_tac (!claset addSIs [if_type RS lam_type]
- addEs [apply_funtype RS succE]) 1);
+by (best_tac (!claset addSIs [if_type RS lam_type]
+ addEs [apply_funtype RS succE]) 1);
(*Proving it's injective*)
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (blast_tac (!claset delrules [equalityI]) 1);
@@ -170,17 +170,17 @@
goalw Cardinal.thy [lesspoll_def]
"!!X. [| X lesspoll Y; Y lesspoll Z |] ==> X lesspoll Z";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
qed "lesspoll_trans";
goalw Cardinal.thy [lesspoll_def]
"!!X. [| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
qed "lesspoll_lepoll_lesspoll";
goalw Cardinal.thy [lesspoll_def]
"!!X. [| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y";
-by (fast_tac (!claset addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1);
+by (blast_tac (!claset addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
qed "lepoll_lesspoll_lesspoll";
@@ -213,7 +213,7 @@
by (rtac classical 1);
by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
by (etac le_refl 2);
-by (fast_tac (!claset addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
+by (blast_tac (!claset addEs [ltE] addIs [leI, ltI, lt_trans1]) 1);
qed "Least_le";
(*LEAST really is the smallest*)
@@ -259,7 +259,7 @@
Converse also requires AC, but see well_ord_cardinal_eqE*)
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> |X| = |Y|";
by (rtac Least_cong 1);
-by (blast_tac (!claset addIs [comp_bij,bij_converse_bij]) 1);
+by (blast_tac (!claset addIs [comp_bij, bij_converse_bij]) 1);
qed "cardinal_cong";
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
@@ -700,10 +700,10 @@
goalw Cardinal.thy [Finite_def]
"!!X. [| Y lepoll X; Finite(X) |] ==> Finite(Y)";
-by (fast_tac (!claset addSEs [eqpollE]
- addEs [lepoll_trans RS
- rewrite_rule [Finite_def]
- lepoll_nat_imp_Finite]) 1);
+by (blast_tac
+ (!claset addSEs [eqpollE]
+ addIs [lepoll_trans RS
+ rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1);
qed "lepoll_Finite";
bind_thm ("subset_Finite", subset_imp_lepoll RS lepoll_Finite);
@@ -734,7 +734,7 @@
goalw Cardinal.thy [Finite_def, eqpoll_def]
"!!A. Finite(A) ==> EX r. well_ord(A,r)";
by (blast_tac (!claset addIs [well_ord_rvimage, bij_is_inj, well_ord_Memrel,
- nat_into_Ord]) 1);
+ nat_into_Ord]) 1);
qed "Finite_imp_well_ord";
@@ -756,7 +756,8 @@
goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))";
by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1);
by (rewtac well_ord_def);
-by (blast_tac (!claset addSIs [tot_ord_converse, nat_wf_on_converse_Memrel]) 1);
+by (blast_tac (!claset addSIs [tot_ord_converse,
+ nat_wf_on_converse_Memrel]) 1);
qed "nat_well_ord_converse_Memrel";
goal Cardinal.thy
@@ -784,5 +785,5 @@
"!!A. [| Finite(A); well_ord(A,r) |] ==> well_ord(A,converse(r))";
by (rtac well_ord_converse 1 THEN assume_tac 1);
by (blast_tac (!claset addDs [ordertype_eq_n]
- addSIs [nat_well_ord_converse_Memrel]) 1);
+ addSIs [nat_well_ord_converse_Memrel]) 1);
qed "Finite_well_ord_converse";
--- a/src/ZF/CardinalArith.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/CardinalArith.ML Wed Apr 23 10:54:22 1997 +0200
@@ -362,7 +362,7 @@
by (rewtac Card_def);
by (dtac trans 1);
by (etac (le_imp_subset RS nat_succ_eqpoll RS cardinal_cong) 1);
-by (etac (Ord_succD RS Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1);
+by (etac (Ord_cardinal_le RS lt_trans2 RS lt_irrefl) 1);
by (REPEAT (ares_tac [le_eqI, Ord_cardinal] 1));
qed "InfCard_is_Limit";
--- a/src/ZF/Cardinal_AC.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Cardinal_AC.ML Wed Apr 23 10:54:22 1997 +0200
@@ -27,7 +27,7 @@
qed "cardinal_eqE";
goal Cardinal_AC.thy "|X| = |Y| <-> X eqpoll Y";
-by (fast_tac (!claset addSEs [cardinal_cong, cardinal_eqE]) 1);
+by (blast_tac (!claset addIs [cardinal_cong, cardinal_eqE]) 1);
qed "cardinal_eqpoll_iff";
goal Cardinal_AC.thy
@@ -93,11 +93,8 @@
by (etac CollectE 1);
by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
by (fast_tac (!claset addSEs [apply_Pair]) 1);
-by (rtac exI 1);
-by (rtac f_imp_injective 1);
-by (rtac Pi_type 1 THEN assume_tac 1);
-by (fast_tac (!claset addDs [apply_type] addDs [Pi_memberD]) 1);
-by (fast_tac (!claset addDs [apply_type] addEs [apply_equality]) 1);
+by (blast_tac (!claset addDs [apply_type, Pi_memberD]
+ addIs [apply_equality, Pi_type, f_imp_injective]) 1);
qed "surj_implies_inj";
(*Kunen's Lemma 10.20*)
@@ -123,14 +120,14 @@
by (subgoal_tac
"ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
by (fast_tac (!claset addSIs [Least_le RS lt_trans1 RS ltD, ltI]
- addSEs [LeastI, Ord_in_Ord]) 2);
+ addSEs [LeastI, Ord_in_Ord]) 2);
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
("d", "%<i,j>. converse(f`i) ` j")]
lam_injective 1);
(*Instantiate the lemma proved above*)
by (ALLGOALS ball_tac);
-by (fast_tac (!claset addEs [inj_is_fun RS apply_type]
- addDs [apply_type]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type]
+ addDs [apply_type]) 1);
by (dtac apply_type 1);
by (etac conjunct2 1);
by (asm_simp_tac (!simpset addsimps [left_inverse]) 1);
@@ -152,8 +149,8 @@
\ (UN i:K. j(i)) < csucc(K)";
by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
by (assume_tac 1);
-by (fast_tac (!claset addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
-by (fast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 1);
+by (blast_tac (!claset addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
+by (blast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 1);
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
qed "cardinal_UN_Ord_lt_csucc";
@@ -194,7 +191,7 @@
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc]
MRS lt_subset_trans] 1);
by (REPEAT (assume_tac 1));
-by (fast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 2);
+by (blast_tac (!claset addSIs [Ord_UN] addEs [ltE]) 2);
by (asm_simp_tac (!simpset addsimps [inj_converse_fun RS apply_type]
setloop split_tac [expand_if]) 1);
qed "le_UN_Ord_lt_csucc";
--- a/src/ZF/Epsilon.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Epsilon.ML Wed Apr 23 10:54:22 1997 +0200
@@ -66,7 +66,7 @@
by (etac nat_induct 1);
by (asm_simp_tac (!simpset addsimps [nat_rec_0]) 1);
by (asm_simp_tac (!simpset addsimps [nat_rec_succ]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "eclose_least_lemma";
goalw Epsilon.thy [eclose_def]
@@ -86,7 +86,7 @@
by (etac (arg_subset_eclose RS subsetD) 2);
by (etac base 2);
by (rewtac Transset_def);
-by (fast_tac (!claset addEs [step,ecloseD]) 1);
+by (blast_tac (!claset addIs [step,ecloseD]) 1);
qed "eclose_induct_down";
goal Epsilon.thy "!!X. Transset(X) ==> eclose(X) = X";
@@ -112,7 +112,7 @@
goalw Epsilon.thy [Transset_def]
"!!i j. [| Transset(i); j:i |] ==> Memrel(i)-``{j} = j";
-by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (blast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
qed "under_Memrel";
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
@@ -228,14 +228,14 @@
goal Epsilon.thy "rank(0) = 0";
by (rtac (rank RS trans) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "rank_0";
goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
by (rtac (rank RS trans) 1);
by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
by (etac succE 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
qed "rank_succ";
@@ -307,22 +307,21 @@
qed "transrec2_0";
goal thy "(THE j. i=j) = i";
-by (fast_tac (!claset addSIs [the_equality]) 1);
+by (blast_tac (!claset addSIs [the_equality]) 1);
qed "THE_eq";
goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
by (simp_tac (!simpset addsimps [succ_not_0, THE_eq, if_P]
- setSolver K Fast_tac) 1);
+ setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
qed "transrec2_succ";
goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (resolve_tac [if_not_P RS trans] 1 THEN
- fast_tac (!claset addSDs [Limit_has_0] addSEs [ltE]) 1);
-by (resolve_tac [if_not_P RS trans] 1 THEN
- fast_tac (!claset addSEs [succ_LimitE]) 1);
-by (Simp_tac 1);
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (blast_tac (!claset addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
qed "transrec2_Limit";
Addsimps [transrec2_0, transrec2_succ];
+
--- a/src/ZF/Fixedpt.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Fixedpt.ML Wed Apr 23 10:54:22 1997 +0200
@@ -56,13 +56,13 @@
(*lfp is contained in each pre-fixedpoint*)
goalw Fixedpt.thy [lfp_def]
"!!A. [| h(A) <= A; A<=D |] ==> lfp(D,h) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
(*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *)
qed "lfp_lowerbound";
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*)
goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "lfp_subset";
(*Used in datatype package*)
@@ -190,7 +190,7 @@
qed "gfp_upperbound";
goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "gfp_subset";
(*Used in datatype package*)
--- a/src/ZF/List.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/List.ML Wed Apr 23 10:54:22 1997 +0200
@@ -28,7 +28,7 @@
goal List.thy "list(A) = {0} + (A * list(A))";
let open list; val rew = rewrite_rule con_defs in
-by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
+by (blast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
end;
qed "list_unfold";
@@ -44,7 +44,7 @@
goalw List.thy (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
-by (fast_tac (!claset addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
+by (blast_tac (!claset addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
Pair_in_univ]) 1);
qed "list_univ";
@@ -233,7 +233,7 @@
goalw List.thy [set_of_list_def]
"!!l. l: list(A) ==> set_of_list(l) : Pow(A)";
by (etac list_rec_type 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS (Blast_tac));
qed "set_of_list_type";
goal List.thy
@@ -267,19 +267,19 @@
val prems = goal List.thy
"l: list(A) ==> map(%u.u, l) = l";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "map_ident";
val prems = goal List.thy
"l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "map_compose";
val prems = goal List.thy
"xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "map_app_distrib";
val prems = goal List.thy
@@ -293,7 +293,7 @@
\ list_rec(map(h,l), c, d) = \
\ list_rec(l, c, %x xs r. d(h(x), map(h,xs), r))";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "list_rec_map";
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
@@ -304,7 +304,7 @@
val prems = goal List.thy
"l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (list_ind_tac "l" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "map_list_Collect";
(*** theorems about length ***)
@@ -312,13 +312,13 @@
val prems = goal List.thy
"xs: list(A) ==> length(map(h,xs)) = length(xs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "length_map";
val prems = goal List.thy
"xs: list(A) ==> length(xs@ys) = length(xs) #+ length(ys)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "length_app";
(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
@@ -345,7 +345,7 @@
\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "drop_length_Cons_lemma";
bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
@@ -359,12 +359,8 @@
by (rtac natE 1);
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (Fast_tac 1);
-by (Asm_simp_tac 1);
-by (dtac bspec 1);
-by (Fast_tac 2);
-by (fast_tac (!claset addEs [succ_in_naturalD,length_type]) 1);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addIs [succ_in_naturalD, length_type])));
qed "drop_length_lemma";
bind_thm ("drop_length", (drop_length_lemma RS bspec));
@@ -373,12 +369,12 @@
val [major] = goal List.thy "xs: list(A) ==> xs@Nil=xs";
by (rtac (major RS list.induct) 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "app_right_Nil";
val prems = goal List.thy "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (list_ind_tac "xs" prems 1);
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "app_assoc";
val prems = goal List.thy
--- a/src/ZF/OrderArith.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/OrderArith.ML Wed Apr 23 10:54:22 1997 +0200
@@ -82,16 +82,12 @@
by (thin_tac "y : A + B" 2);
by (rtac ballI 2);
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
-by (etac (bspec RS mp) 2);
-by (Blast_tac 2);
-by (best_tac (!claset addSEs [raddE]) 2);
+by (best_tac (!claset addSEs [raddE, bspec RS mp]) 2);
(*Returning to main part of proof*)
by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
-by (Best_tac 1);
+by (Blast_tac 1);
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
-by (etac (bspec RS mp) 1);
-by (Blast_tac 1);
-by (best_tac (!claset addSEs [raddE]) 1);
+by (best_tac (!claset addSEs [raddE, bspec RS mp]) 1);
qed "wf_on_radd";
goal OrderArith.thy
@@ -225,9 +221,7 @@
by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
by (rtac ballI 1);
by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
-by (etac (bspec RS mp) 1);
-by (Blast_tac 1);
-by (best_tac (!claset addSEs [rmultE]) 1);
+by (best_tac (!claset addSEs [rmultE, bspec RS mp]) 1);
qed "wf_on_rmult";
@@ -267,7 +261,7 @@
by (ALLGOALS
(asm_full_simp_tac (!simpset addsimps [bij_is_fun RS apply_type])));
by (Blast_tac 1);
-by (fast_tac (!claset addSEs [bij_is_inj RS inj_apply_equality]) 1);
+by (blast_tac (!claset addIs [bij_is_inj RS inj_apply_equality]) 1);
qed "prod_ord_iso_cong";
goal OrderArith.thy "(lam z:A. <x,z>) : bij(A, {x}*A)";
@@ -313,8 +307,8 @@
(!simpset addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
by (Asm_simp_tac 1);
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE]));
-by (ALLGOALS (Asm_simp_tac));
-by (ALLGOALS (fast_tac (!claset addEs [well_ord_is_wf RS wf_on_asym])));
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS (blast_tac (!claset addEs [well_ord_is_wf RS wf_on_asym])));
qed "prod_sum_singleton_ord_iso";
(** Distributive law **)
@@ -334,7 +328,7 @@
\ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE]));
-by (ALLGOALS (Asm_simp_tac));
+by (ALLGOALS Asm_simp_tac);
qed "sum_prod_distrib_ord_iso";
(** Associativity **)
@@ -442,5 +436,5 @@
goalw OrderArith.thy [ord_iso_def, rvimage_def]
"!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "ord_iso_rvimage_eq";
--- a/src/ZF/OrderType.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/OrderType.ML Wed Apr 23 10:54:22 1997 +0200
@@ -155,9 +155,9 @@
goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
"!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
by (fast_tac (!claset addSIs [ordermap_type, ordermap_surj]
- addEs [linearE]
- addDs [ordermap_mono]
- addss (!simpset addsimps [mem_not_refl])) 1);
+ addEs [linearE]
+ addDs [ordermap_mono]
+ addss (!simpset addsimps [mem_not_refl])) 1);
qed "ordermap_bij";
(*** Isomorphisms involving ordertype ***)
@@ -455,12 +455,12 @@
by (rtac Ord_linear_lt 1);
by (REPEAT_SOME assume_tac);
by (ALLGOALS
- (fast_tac (!claset addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
+ (blast_tac (!claset addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
qed "oadd_lt_cancel2";
goal OrderType.thy
"!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> i++j < i++k <-> j<k";
-by (fast_tac (!claset addSIs [oadd_lt_mono2] addSEs [oadd_lt_cancel2]) 1);
+by (blast_tac (!claset addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
qed "oadd_lt_iff2";
goal OrderType.thy
@@ -469,7 +469,7 @@
by (REPEAT_SOME assume_tac);
by (ALLGOALS
(fast_tac (!claset addDs [oadd_lt_mono2]
- addss (!simpset addsimps [lt_not_refl]))));
+ addss (!simpset addsimps [lt_not_refl]))));
qed "oadd_inject";
goalw OrderType.thy [oadd_def]
@@ -508,7 +508,7 @@
by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
by (REPEAT (ares_tac [Ord_oadd] 1));
by (fast_tac (!claset addIs [lt_oadd1, oadd_lt_mono2]
- addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
+ addss (!simpset addsimps [Ord_mem_iff_lt, Ord_oadd])) 3);
by (Blast_tac 2);
by (blast_tac (!claset addSEs [ltE]) 1);
qed "oadd_unfold";
@@ -667,7 +667,7 @@
(*** A useful unfolding law ***)
goalw OrderType.thy [pred_def]
- "!!A B. [| a:A; b:B |] ==> \
+ "!!A B. [| a:A; b:B |] ==> \
\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \
\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
by (rtac equalityI 1);
@@ -677,9 +677,9 @@
qed "pred_Pair_eq";
goal OrderType.thy
- "!!A B. [| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
+ "!!A B. [| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
\ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
-\ ordertype(pred(A,a,r)*B + pred(B,b,s), \
+\ ordertype(pred(A,a,r)*B + pred(B,b,s), \
\ radd(A*B, rmult(A,r,B,s), B, s))";
by (asm_simp_tac (!simpset addsimps [pred_Pair_eq]) 1);
by (resolve_tac [ordertype_eq RS sym] 1);
@@ -689,12 +689,12 @@
qed "ordertype_pred_Pair_eq";
goalw OrderType.thy [oadd_def, omult_def]
- "!!i j. [| i'<i; j'<j |] ==> \
+ "!!i j. [| i'<i; j'<j |] ==> \
\ ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
-\ rmult(i,Memrel(i),j,Memrel(j))) = \
+\ rmult(i,Memrel(i),j,Memrel(j))) = \
\ j**i' ++ j'";
by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel,
- ltD, lt_Ord2, well_ord_Memrel]) 1);
+ ltD, lt_Ord2, well_ord_Memrel]) 1);
by (rtac trans 1);
by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
by (rtac ord_iso_refl 3);
@@ -702,10 +702,9 @@
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
Ord_ordertype]));
-by (ALLGOALS
- (asm_simp_tac (!simpset addsimps [rmult_iff, id_conv, Memrel_iff])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Memrel_iff])));
by (safe_tac (!claset));
-by (ALLGOALS (fast_tac (!claset addEs [Ord_trans])));
+by (ALLGOALS (blast_tac (!claset addIs [Ord_trans])));
qed "ordertype_pred_Pair_lemma";
goalw OrderType.thy [omult_def]
--- a/src/ZF/Ordinal.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Ordinal.ML Wed Apr 23 10:54:22 1997 +0200
@@ -110,6 +110,8 @@
(* Ord(succ(j)) ==> Ord(j) *)
val Ord_succD = succI1 RSN (2, Ord_in_Ord);
+AddSDs [Ord_succD];
+
goal Ordinal.thy "!!i j. [| Ord(i); Transset(j); j<=i |] ==> Ord(j)";
by (REPEAT (ares_tac [OrdI] 1
ORELSE eresolve_tac [Ord_contains_Transset, subsetD] 1));
@@ -480,8 +482,8 @@
qed "le_imp_subset";
goal Ordinal.thy "j le i <-> j<=i & Ord(i) & Ord(j)";
-by (fast_tac (!claset addSEs [subset_imp_le, le_imp_subset]
- addEs [ltE, make_elim Ord_succD]) 1);
+by (blast_tac (!claset addDs [Ord_succD, subset_imp_le, le_imp_subset]
+ addEs [ltE]) 1);
qed "le_subset_iff";
goal Ordinal.thy "i le succ(j) <-> i le j | i=succ(j) & Ord(i)";
@@ -513,7 +515,7 @@
goal Ordinal.thy "!!i j. i<j ==> succ(i) le j";
by (rtac (not_lt_iff_le RS iffD1) 1);
by (blast_tac le_cs 3);
-by (ALLGOALS (blast_tac (!claset addEs [ltE] addIs [Ord_succ])));
+by (ALLGOALS (blast_tac (!claset addEs [ltE])));
qed "succ_leI";
(*Identical to succ(i) < succ(j) ==> i<j *)
@@ -627,12 +629,12 @@
qed "le_implies_UN_le_UN";
goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (best_tac (!claset addEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
qed "Ord_equality";
(*Holds for all transitive sets, not just ordinals*)
goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
-by (fast_tac (!claset addSEs [Ord_trans]) 1);
+by (blast_tac (!claset addIs [Ord_trans]) 1);
qed "Ord_Union_subset";
--- a/src/ZF/Perm.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Perm.ML Wed Apr 23 10:54:22 1997 +0200
@@ -18,8 +18,7 @@
qed "surj_is_fun";
goalw Perm.thy [surj_def] "!!f A B. f : Pi(A,B) ==> f: surj(A,range(f))";
-by (fast_tac (!claset addIs [apply_equality]
- addEs [range_of_fun,domain_type]) 1);
+by (blast_tac (!claset addIs [apply_equality, range_of_fun, domain_type]) 1);
qed "fun_is_surj";
goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B";
@@ -31,7 +30,7 @@
val prems = goalw Perm.thy [surj_def]
"[| f: A->B; !!y. y:B ==> d(y): A; !!y. y:B ==> f`d(y) = y \
\ |] ==> f: surj(A,B)";
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "f_imp_surjective";
val prems = goal Perm.thy
@@ -61,11 +60,11 @@
goalw Perm.thy [inj_def]
"!!f A B. [| <a,b>:f; <c,b>:f; f: inj(A,B) |] ==> a=c";
by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "inj_equality";
goalw thy [inj_def] "!!A B f. [| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b";
-by (Fast_tac 1);
+by (Blast_tac 1);
val inj_apply_equality = result();
(** A function with a left inverse is an injection **)
@@ -143,15 +142,16 @@
val id_inj = subset_refl RS id_subset_inj;
goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
-by (fast_tac (!claset addIs [lam_type,beta]) 1);
+by (blast_tac (!claset addIs [lam_type, beta]) 1);
qed "id_surj";
goalw Perm.thy [bij_def] "id(A): bij(A,A)";
-by (fast_tac (!claset addIs [id_inj,id_surj]) 1);
+by (blast_tac (!claset addIs [id_inj, id_surj]) 1);
qed "id_bij";
goalw Perm.thy [id_def] "A <= B <-> id(A) : A->B";
-by (fast_tac (!claset addSIs [lam_type] addDs [apply_type] addss (!simpset)) 1);
+by (fast_tac (!claset addSIs [lam_type] addDs [apply_type]
+ addss (!simpset)) 1);
qed "subset_iff_id";
@@ -161,20 +161,21 @@
by (asm_simp_tac (!simpset addsimps [Pi_iff, function_def]) 1);
by (etac CollectE 1);
by (asm_simp_tac (!simpset addsimps [apply_iff]) 1);
-by (fast_tac (!claset addDs [fun_is_rel]) 1);
+by (blast_tac (!claset addDs [fun_is_rel]) 1);
qed "inj_converse_fun";
(** Equations for converse(f) **)
(*The premises are equivalent to saying that f is injective...*)
-val prems = goal Perm.thy
- "[| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a";
-by (fast_tac (!claset addIs (prems@[apply_Pair,apply_equality,converseI])) 1);
+goal Perm.thy
+ "!!f. [| f: A->B; converse(f): C->A; a: A |] ==> converse(f)`(f`a) = a";
+by (blast_tac (!claset addIs [apply_Pair, apply_equality, converseI]) 1);
qed "left_inverse_lemma";
goal Perm.thy
"!!f. [| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
-by (fast_tac (!claset addIs [left_inverse_lemma,inj_converse_fun,inj_is_fun]) 1);
+by (blast_tac (!claset addIs [left_inverse_lemma, inj_converse_fun,
+ inj_is_fun]) 1);
qed "left_inverse";
val left_inverse_bij = bij_is_inj RS left_inverse;
@@ -210,14 +211,13 @@
qed "inj_converse_inj";
goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
-by (ITER_DEEPEN (has_fewer_prems 1)
- (ares_tac [f_imp_surjective, inj_converse_fun, left_inverse,
- inj_is_fun, range_of_fun RS apply_type]));
+by (blast_tac (!claset addIs [f_imp_surjective, inj_converse_fun, left_inverse,
+ inj_is_fun, range_of_fun RS apply_type]) 1);
qed "inj_converse_surj";
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
by (fast_tac (!claset addEs [surj_range RS subst, inj_converse_inj,
- inj_converse_surj]) 1);
+ inj_converse_surj]) 1);
qed "bij_converse_bij";
(*Adding this as an SI seems to cause looping*)
@@ -227,7 +227,7 @@
(*The inductive definition package could derive these theorems for (r O s)*)
goalw Perm.thy [comp_def] "!!r s. [| <a,b>:s; <b,c>:r |] ==> <a,c> : r O s";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "compI";
val prems = goalw Perm.thy [comp_def]
@@ -251,56 +251,56 @@
(*Boyer et al., Set Theory in First-Order Logic, JAR 2 (1986), 287-327*)
goal Perm.thy "range(r O s) <= range(r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "range_comp";
goal Perm.thy "!!r s. domain(r) <= range(s) ==> range(r O s) = range(r)";
by (rtac (range_comp RS equalityI) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "range_comp_eq";
goal Perm.thy "domain(r O s) <= domain(s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "domain_comp";
goal Perm.thy "!!r s. range(s) <= domain(r) ==> domain(r O s) = domain(s)";
by (rtac (domain_comp RS equalityI) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "domain_comp_eq";
goal Perm.thy "(r O s)``A = r``(s``A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "image_comp";
(** Other results **)
goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_mono";
(*composition preserves relations*)
goal Perm.thy "!!r s. [| s<=A*B; r<=B*C |] ==> (r O s) <= A*C";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_rel";
(*associative law for composition*)
goal Perm.thy "(r O s) O t = r O (s O t)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_assoc";
(*left identity of composition; provable inclusions are
id(A) O r <= r
and [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "left_comp_id";
(*right identity of composition; provable inclusions are
r O id(A) <= r
and [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "right_comp_id";
@@ -308,7 +308,7 @@
goalw Perm.thy [function_def]
"!!f g. [| function(g); function(f) |] ==> function(f O g)";
-by (fast_tac (!claset addIs [compI] addSEs [compE, Pair_inject]) 1);
+by (Blast_tac 1);
qed "comp_function";
goal Perm.thy "!!f g. [| g: A->B; f: B->C |] ==> (f O g) : A->C";
@@ -316,7 +316,7 @@
(!simpset addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
setloop etac conjE) 1);
by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "comp_fun";
goal Perm.thy "!!f g. [| g: A->B; f: B->C; a:A |] ==> (f O g)`a = f`(g`a)";
@@ -348,12 +348,12 @@
goalw Perm.thy [surj_def]
"!!f g. [| g: surj(A,B); f: surj(B,C) |] ==> (f O g) : surj(A,C)";
-by (best_tac (!claset addSIs [comp_fun,comp_fun_apply]) 1);
+by (blast_tac (!claset addSIs [comp_fun,comp_fun_apply]) 1);
qed "comp_surj";
goalw Perm.thy [bij_def]
"!!f g. [| g: bij(A,B); f: bij(B,C) |] ==> (f O g) : bij(A,C)";
-by (fast_tac (!claset addIs [comp_inj,comp_surj]) 1);
+by (blast_tac (!claset addIs [comp_inj,comp_surj]) 1);
qed "comp_bij";
@@ -382,7 +382,7 @@
goalw Perm.thy [surj_def]
"!!f g. [| (f O g): surj(A,C); g: A->B; f: B->C |] ==> f: surj(B,C)";
-by (best_tac (!claset addSIs [comp_fun_apply RS sym, apply_type]) 1);
+by (blast_tac (!claset addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
qed "comp_mem_surjD1";
goal Perm.thy
@@ -395,7 +395,7 @@
by (safe_tac (!claset));
by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
-by (best_tac (!claset addSIs [apply_type]) 1);
+by (blast_tac (!claset addSIs [apply_funtype]) 1);
qed "comp_mem_surjD2";
@@ -418,7 +418,7 @@
by (cut_facts_tac [prem] 1);
by (rtac equalityI 1);
by (best_tac (!claset addEs [domain_type, range_type, make_elim appfD]) 1);
-by (best_tac (!claset addIs [apply_Pair]) 1);
+by (blast_tac (!claset addIs [apply_Pair]) 1);
qed "right_comp_inverse";
(** Proving that a function is a bijection **)
@@ -462,16 +462,14 @@
by (ALLGOALS
(asm_simp_tac (!simpset addsimps [inj_is_fun RS apply_type, left_inverse]
setloop (split_tac [expand_if] ORELSE' etac UnE))));
-by (fast_tac (!claset addSEs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
+by (blast_tac (!claset addIs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
qed "inj_disjoint_Un";
goalw Perm.thy [surj_def]
"!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \
\ (f Un g) : surj(A Un C, B Un D)";
-by (DEPTH_SOLVE_1 (eresolve_tac [fun_disjoint_apply1, fun_disjoint_apply2] 1
- ORELSE ball_tac 1
- ORELSE (rtac trans 1 THEN atac 2)
- ORELSE step_tac (!claset addIs [fun_disjoint_Un]) 1));
+by (blast_tac (!claset addIs [fun_disjoint_apply1, fun_disjoint_apply2,
+ fun_disjoint_Un, trans]) 1);
qed "surj_disjoint_Un";
(*A simple, high-level proof; the version for injections follows from it,
@@ -517,23 +515,21 @@
goalw Perm.thy [inj_def,bij_def]
"!!f. [| f: inj(A,B); C<=A |] ==> restrict(f,C): bij(C, f``C)";
-by (safe_tac (!claset));
-by (REPEAT (eresolve_tac [bspec RS bspec RS mp, subsetD,
- box_equals, restrict] 1
- ORELSE ares_tac [surj_is_fun,restrict_surj] 1));
+by (blast_tac (!claset addSIs [restrict, restrict_surj]
+ addIs [box_equals, surj_is_fun]) 1);
qed "restrict_bij";
(*** Lemmas for Ramsey's Theorem ***)
goalw Perm.thy [inj_def] "!!f. [| f: inj(A,B); B<=D |] ==> f: inj(A,D)";
-by (fast_tac (!claset addSEs [fun_weaken_type]) 1);
+by (blast_tac (!claset addIs [fun_weaken_type]) 1);
qed "inj_weaken_type";
val [major] = goal Perm.thy
"[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})";
by (rtac (major RS restrict_bij RS bij_is_inj RS inj_weaken_type) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
by (cut_facts_tac [major] 1);
by (rewtac inj_def);
by (fast_tac (!claset addEs [range_type, mem_irrefl]
@@ -543,8 +539,8 @@
goalw Perm.thy [inj_def]
"!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
-by (fast_tac (!claset addIs [apply_type]
- unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
- fun_extend_apply1]) ) 1);
+by (fast_tac (!claset addIs [apply_type]
+ unsafe_addss (!simpset addsimps [fun_extend, fun_extend_apply2,
+ fun_extend_apply1])) 1);
qed "inj_extend";
--- a/src/ZF/QPair.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/QPair.ML Wed Apr 23 10:54:22 1997 +0200
@@ -51,7 +51,7 @@
qed_goalw "QSigmaI" thy [QSigma_def]
"!!A B. [| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)"
- (fn _ => [ Fast_tac 1 ]);
+ (fn _ => [ Blast_tac 1 ]);
AddSIs [QSigmaI];
@@ -88,10 +88,10 @@
(fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
Addsimps [QSigma_empty1, QSigma_empty2];
@@ -100,11 +100,11 @@
qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
(fn _=>
- [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+ [ (blast_tac (!claset addIs [the_equality]) 1) ]);
qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
(fn _=>
- [ (fast_tac (!claset addIs [the_equality]) 1) ]);
+ [ (blast_tac (!claset addIs [the_equality]) 1) ]);
Addsimps [qfst_conv, qsnd_conv];
@@ -171,11 +171,11 @@
qed_goalw "qconverseI" thy [qconverse_def]
"!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goalw "qconverseD" thy [qconverse_def]
"!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goalw "qconverseE" thy [qconverse_def]
"[| yx : qconverse(r); \
@@ -192,17 +192,17 @@
qed_goal "qconverse_qconverse" thy
"!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "qconverse_type" thy
"!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
qed_goal "qconverse_empty" thy "qconverse(0) = 0"
- (fn _ => [ (Fast_tac 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
(**** The Quine-inspired notion of disjoint sum ****)
@@ -212,11 +212,11 @@
(** Introduction rules for the injections **)
goalw thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "QInlI";
goalw thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "QInrI";
(** Elimination rules **)
@@ -267,27 +267,27 @@
Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
goal thy "!!A B. QInl(a): A<+>B ==> a: A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "QInlD";
goal thy "!!A B. QInr(b): A<+>B ==> b: B";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "QInrD";
(** <+> is itself injective... who cares?? **)
goal thy
"u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "qsum_iff";
goal thy "A <+> B <= C <+> D <-> A<=C & B<=D";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "qsum_subset_iff";
goal thy "A <+> B = C <+> D <-> A=C & B=D";
by (simp_tac (!simpset addsimps [extension,qsum_subset_iff]) 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "qsum_equal_iff";
(*** Eliminator -- qcase ***)
@@ -315,17 +315,17 @@
(** Rules for the Part primitive **)
goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_QInl";
goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_QInr";
goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_QInr2";
goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Part_qsum_equality";
--- a/src/ZF/QUniv.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/QUniv.ML Wed Apr 23 10:54:22 1997 +0200
@@ -20,7 +20,7 @@
val [prem] = goalw QUniv.thy [sum_def]
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
by (stac Int_Un_distrib 1);
-by (fast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
+by (blast_tac (!claset addSDs [prem RS Transset_Pair_D]) 1);
qed "Transset_sum_Int_subset";
(** Introduction and elimination rules avoid tiresome folding/unfolding **)
@@ -187,13 +187,13 @@
goalw Univ.thy [Pair_def]
"!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \
\ a: Vfrom(X,i) & b: Vfrom(X,i)";
-by (fast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
+by (blast_tac (!claset addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1);
qed "Pair_in_Vfrom_D";
goal Univ.thy
"!!X. Transset(X) ==> \
\ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))";
-by (fast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
+by (blast_tac (!claset addSDs [Pair_in_Vfrom_D]) 1);
qed "product_Int_Vfrom_subset";
(*** Intersecting <a;b> with Vfrom... ***)
--- a/src/ZF/Rel.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Rel.ML Wed Apr 23 10:54:22 1997 +0200
@@ -30,7 +30,7 @@
qed "symI";
goalw Rel.thy [sym_def] "!!r. [| sym(r); <x,y>: r |] ==> <y,x>: r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "symE";
(* antisymmetry *)
@@ -43,18 +43,18 @@
val prems = goalw Rel.thy [antisym_def]
"!!r. [| antisym(r); <x,y>: r; <y,x>: r |] ==> x=y";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "antisymE";
(* transitivity *)
goalw Rel.thy [trans_def]
"!!r. [| trans(r); <a,b>:r; <b,c>:r |] ==> <a,c>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "transD";
goalw Rel.thy [trans_on_def]
"!!r. [| trans[A](r); <a,b>:r; <b,c>:r; a:A; b:A; c:A |] ==> <a,c>:r";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "trans_onD";
--- a/src/ZF/Trancl.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Trancl.ML Wed Apr 23 10:54:22 1997 +0200
@@ -68,7 +68,7 @@
\ !!x y z.[| P(<x,y>); <x,y>: r^*; <y,z>: r |] ==> P(<x,z>) |] \
\ ==> P(<a,b>)";
by (rtac ([rtrancl_def, rtrancl_bnd_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
qed "rtrancl_full_induct";
(*nice induction rule.
@@ -85,7 +85,7 @@
by (EVERY1 [etac (spec RS mp), rtac refl]);
(*now do the induction*)
by (resolve_tac [major RS rtrancl_full_induct] 1);
-by (ALLGOALS (fast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
qed "rtrancl_induct";
(*transitivity of transitive closure!! -- by induction.*)
@@ -111,33 +111,30 @@
(*Transitivity of r^+ is proved by transitivity of r^* *)
goalw Trancl.thy [trans_def,trancl_def] "trans(r^+)";
-by (safe_tac (!claset));
-by (rtac (rtrancl_into_rtrancl RS (trans_rtrancl RS transD RS compI)) 1);
-by (REPEAT (assume_tac 1));
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl RS
+ (trans_rtrancl RS transD RS compI)]) 1);
qed "trans_trancl";
(** Conversions between trancl and rtrancl **)
-val [major] = goalw Trancl.thy [trancl_def] "<a,b> : r^+ ==> <a,b> : r^*";
-by (resolve_tac [major RS compEpair] 1);
-by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
+goalw Trancl.thy [trancl_def] "!!r. <a,b> : r^+ ==> <a,b> : r^*";
+by (blast_tac (!claset addIs [rtrancl_into_rtrancl]) 1);
qed "trancl_into_rtrancl";
(*r^+ contains all pairs in r *)
-val [prem] = goalw Trancl.thy [trancl_def] "<a,b> : r ==> <a,b> : r^+";
-by (REPEAT (ares_tac [prem,compI,rtrancl_refl,fieldI1] 1));
+goalw Trancl.thy [trancl_def] "!!r. <a,b> : r ==> <a,b> : r^+";
+by (blast_tac (!claset addSIs [rtrancl_refl]) 1);
qed "r_into_trancl";
(*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);
+goal Trancl.thy "!!r. r <= Sigma(A,B) ==> r <= r^+";
by (blast_tac (!claset addIs [r_into_trancl]) 1);
qed "r_subset_trancl";
(*intro rule by definition: from r^* and r *)
-val prems = goalw Trancl.thy [trancl_def]
- "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
-by (REPEAT (resolve_tac ([compI]@prems) 1));
+goalw Trancl.thy [trancl_def]
+ "!!r. [| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^+";
+by (Blast_tac 1);
qed "rtrancl_into_trancl1";
(*intro rule from r and r^* *)
--- a/src/ZF/Univ.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/Univ.ML Wed Apr 23 10:54:22 1997 +0200
@@ -618,9 +618,7 @@
by (safe_tac (!claset));
by (etac Limit_VfromE 1);
by (assume_tac 1);
-by (res_inst_tac [("x", "xa Un j")] exI 1);
-by (best_tac (!claset addIs [subset_refl RS Vfrom_mono RS subsetD,
- Un_least_lt]) 1);
+by (blast_tac (!claset addSIs [Un_least_lt] addIs [Vfrom_UnI1, Vfrom_UnI2]) 1);
val Fin_Vfrom_lemma = result();
goal Univ.thy "!!i. Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)";
--- a/src/ZF/WF.ML Wed Apr 23 10:52:49 1997 +0200
+++ b/src/ZF/WF.ML Wed Apr 23 10:54:22 1997 +0200
@@ -25,7 +25,7 @@
(** Equivalences between wf and wf_on **)
goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_imp_wf_on";
goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)";
@@ -33,7 +33,7 @@
qed "wf_on_field_imp_wf";
goal WF.thy "wf(r) <-> wf[field(r)](r)";
-by (fast_tac (!claset addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
+by (blast_tac (!claset addIs [wf_imp_wf_on, wf_on_field_imp_wf]) 1);
qed "wf_iff_wf_on_field";
goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r); B<=A |] ==> wf[B](r)";
@@ -52,7 +52,7 @@
\ ==> wf[A](r)";
by (rtac (equals0I RS disjCI RS allI) 1);
by (res_inst_tac [ ("Z", "Z") ] prem 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Blast_tac);
qed "wf_onI";
(*If r allows well-founded induction over A then wf[A](r)
@@ -65,7 +65,7 @@
by (rtac wf_onI 1);
by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1);
by (contr_tac 3);
-by (Fast_tac 2);
+by (Blast_tac 2);
by (Fast_tac 1);
qed "wf_onI2";
@@ -79,9 +79,9 @@
\ |] ==> P(a)";
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1);
by (etac disjE 1);
-by (fast_tac (!claset addEs [equalityE]) 1);
+by (blast_tac (!claset addEs [equalityE]) 1);
by (asm_full_simp_tac (!simpset addsimps [domainI]) 1);
-by (fast_tac (!claset addSDs [minor]) 1);
+by (blast_tac (!claset addSDs [minor]) 1);
qed "wf_induct";
(*Perform induction on i, then prove the wf(r) subgoal using prems. *)
@@ -99,11 +99,11 @@
by (wf_ind_tac "a" [wfr] 1);
by (rtac impI 1);
by (eresolve_tac prems 1);
-by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
+by (blast_tac (!claset addIs (prems RL [subsetD])) 1);
qed "wf_induct2";
goal domrange.thy "!!r A. field(r Int A*A) <= A";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "field_Int_square";
val wfr::amem::prems = goalw WF.thy [wf_on_def]
@@ -112,7 +112,7 @@
\ |] ==> P(a)";
by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1);
by (REPEAT (ares_tac prems 1));
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_on_induct";
fun wf_on_ind_tac a prems i =
@@ -135,26 +135,26 @@
goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
by (wf_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_not_refl";
goal WF.thy "!!r. [| wf(r); <a,x>:r; <x,a>:r |] ==> P";
by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
by (wf_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
qed "wf_asym";
goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r";
by (wf_on_ind_tac "a" [] 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_on_not_refl";
goal WF.thy "!!r. [| wf[A](r); <a,b>:r; <b,a>:r; a:A; b:A |] ==> P";
by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
qed "wf_on_asym";
(*Needed to prove well_ordI. Could also reason that wf[A](r) means
@@ -164,8 +164,8 @@
by (subgoal_tac
"ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1);
by (wf_on_ind_tac "a" [] 2);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 2);
+by (Blast_tac 1);
qed "wf_on_chain3";
@@ -178,20 +178,15 @@
by (rtac wf_onI2 1);
by (bchain_tac 1);
by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1);
-by (rtac (impI RS ballI) 1);
-by (etac tranclE 1);
-by (etac (bspec RS mp) 1 THEN assume_tac 1);
-by (Fast_tac 1);
by (cut_facts_tac [subs] 1);
-(*astar_tac is slightly faster*)
-by (Best_tac 1);
+by (blast_tac (!claset addEs [tranclE]) 1);
qed "wf_on_trancl";
goal WF.thy "!!r. wf(r) ==> wf(r^+)";
by (asm_full_simp_tac (!simpset addsimps [wf_iff_wf_on_field]) 1);
by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1);
by (etac wf_on_trancl 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "wf_trancl";