--- a/src/ZF/AC/AC16_WO4.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/AC16_WO4.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proof of AC16(n, k) ==> WO4(n-k)
*)
@@ -14,9 +14,9 @@
goalw thy [Finite_def] "!!A. [| Finite(A); 0<m; m:nat |] ==> \
\ EX a f. Ord(a) & domain(f) = a & \
\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)";
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (res_inst_tac [("x","n")] exI 1);
by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1);
by (asm_full_simp_tac AC_ss 1);
@@ -104,10 +104,10 @@
\ ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
by (resolve_tac [prem RS FalseE] 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [CollectE] 1);
-by (eresolve_tac [conjE] 1);
-by (eresolve_tac [swap] 1);
+by (rtac ballI 1);
+by (etac CollectE 1);
+by (etac conjE 1);
+by (etac swap 1);
by (fast_tac (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1);
val suppose_not = result();
@@ -127,7 +127,7 @@
goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat \
\ |] ==> EX z. z<=y & n eqpoll z";
-by (eresolve_tac [nat_lepoll_imp_ex_eqpoll_n] 1);
+by (etac nat_lepoll_imp_ex_eqpoll_n 1);
by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
RSN (2, lepoll_trans)] 1 THEN (assume_tac 2));
by (fast_tac (AC_cs addSIs [nat_le_infinite_Ord RS le_imp_lepoll]
@@ -185,18 +185,18 @@
\ EX! w. w:t_n & z <= w; \
\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \
\ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c";
-by (eresolve_tac [ballE] 1);
+by (etac ballE 1);
by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset,
eqpoll_sym RS cons_cons_eqpoll]) 2);
-by (eresolve_tac [ex1E] 1);
+by (etac ex1E 1);
by (res_inst_tac [("a","w")] ex1I 1);
-by (resolve_tac [conjI] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac conjI 1);
+by (rtac CollectI 1);
by (fast_tac (FOL_cs addSEs [s_uI]) 1);
by (fast_tac AC_cs 1);
by (fast_tac AC_cs 1);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
+by (etac allE 1);
+by (etac impE 1);
by (assume_tac 2);
by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
val ex1_superset_a = result();
@@ -204,14 +204,14 @@
goal thy
"!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \
\ |] ==> A = cons(a, B)";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
by (fast_tac AC_cs 2);
by (resolve_tac [Diff_eq_0_iff RS iffD1] 1);
-by (resolve_tac [equals0I] 1);
+by (rtac equals0I 1);
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1);
by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1);
by (fast_tac AC_cs 1);
-by (dresolve_tac [cons_eqpoll_succ] 1);
+by (dtac cons_eqpoll_succ 1);
by (fast_tac AC_cs 1);
by (fast_tac (AC_cs addSIs [nat_succI]
addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS
@@ -226,7 +226,7 @@
\ |] ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c) \
\ Int y = cons(b, a)";
by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [set_eq_cons] 1);
+by (rtac set_eq_cons 1);
by (REPEAT (fast_tac AC_cs 1));
val the_eq_cons = result();
@@ -261,16 +261,16 @@
\ THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1
THEN REPEAT (assume_tac 1));
-by (resolve_tac [ballI] 1);
-by (resolve_tac [ballI] 1);
+by (rtac ballI 1);
+by (rtac ballI 1);
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
-by (resolve_tac [impI] 1);
-by (resolve_tac [cons_eqE] 1);
+by (rtac impI 1);
+by (rtac cons_eqE 1);
by (fast_tac AC_cs 2);
by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1);
by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1
@@ -293,7 +293,7 @@
by (fast_tac AC_cs 1);
by (eres_inst_tac [("x","A - {xa}")] allE 1);
by (eres_inst_tac [("x","B - {xa}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (asm_full_simp_tac (AC_ss addsimps [add_succ]) 1);
by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
@@ -324,7 +324,7 @@
by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1);
by (eres_inst_tac [("x","A - {xa}")] allE 1);
by (eres_inst_tac [("x","B - {xa}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll,
eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym]
addss (AC_ss addsimps [add_succ])) 1);
@@ -355,7 +355,7 @@
\ m:nat; l:nat; x Int y = 0; u : x; \
\ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y \
\ |] ==> w Int (x - {u}) eqpoll m";
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSDs [s_u_subset RS subsetD]) 1);
by (fast_tac (AC_cs addEs [equals0D] addSDs [bspec]
@@ -393,24 +393,24 @@
\ w Int (x - {u})")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (rtac CollectI 1);
by (fast_tac AC_cs 1);
-by (resolve_tac [w_Int_eqpoll_m] 1 THEN REPEAT (assume_tac 1));
+by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
by (simp_tac AC_ss 1);
by (REPEAT (resolve_tac [ballI, impI] 1));
by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1
THEN REPEAT (assume_tac 1));
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [ex1_two_eq] 1);
+by (etac ex1_two_eq 1);
by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
val subset_s_u_lepoll_w = result();
goal thy "!!k. [| 0<k; k:nat |] ==> EX l:nat. k = succ(l)";
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1);
by (fast_tac (empty_cs addSIs [refl, bexI]) 1);
val ex_eq_succ = result();
@@ -422,12 +422,12 @@
\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \
\ |] ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
-by (resolve_tac [suppose_not] 1);
+by (rtac suppose_not 1);
by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1));
by (hyp_subst_tac 1);
by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1
THEN REPEAT (assume_tac 1));
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1
THEN REPEAT (assume_tac 1));
by (contr_tac 1);
@@ -489,14 +489,14 @@
goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \
\ EX R. well_ord({z:Pow(y). z lepoll n}, R)";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
by (fast_tac (ZF_cs addSIs [well_ord_unit]
addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1
THEN REPEAT (assume_tac 1));
by (asm_simp_tac (ZF_ss addsimps [subsets_lepoll_succ]) 1);
-by (dresolve_tac [well_ord_radd] 1 THEN (assume_tac 1));
+by (dtac well_ord_radd 1 THEN (assume_tac 1));
by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS
(eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1);
by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1);
@@ -533,7 +533,7 @@
by (fast_tac (AC_cs addSEs [eqpoll_sym]) 2);
by (res_inst_tac [("a","v")] ex1I 1);
by (fast_tac AC_cs 1);
-by (eresolve_tac [ex1E] 1);
+by (etac ex1E 1);
by (res_inst_tac [("x","v")] allE 1 THEN (assume_tac 1));
by (eres_inst_tac [("x","xb")] allE 1);
by (fast_tac AC_cs 1);
@@ -576,10 +576,10 @@
\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0<k; 0<m; k:nat; m:nat \
\ |] ==> EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w";
by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (res_inst_tac [("x","w Int y")] bexI 1);
-by (eresolve_tac [Int_in_LL] 2);
-by (rewrite_goals_tac [GG_def]);
+by (etac Int_in_LL 2);
+by (rewtac GG_def);
by (asm_full_simp_tac (AC_ss addsimps [Int_in_LL]) 1);
by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
THEN (assume_tac 1));
@@ -611,10 +611,10 @@
\ ==> GG(t_n, k, y) ` v <= x";
by (asm_full_simp_tac AC_ss 1);
by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1));
-by (dresolve_tac [in_LL_eq_Int] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [DiffE] 1);
-by (eresolve_tac [swap] 1);
+by (dtac in_LL_eq_Int 1 THEN REPEAT (assume_tac 1));
+by (rtac subsetI 1);
+by (etac DiffE 1);
+by (etac swap 1);
by (fast_tac (AC_cs addEs [ssubst]) 1);
val GG_subset = result();
@@ -627,16 +627,16 @@
\ |] ==> (UN b<ordertype(LL(t_n, succ(k), y), S). \
\ (GG(t_n, succ(k), y)) ` \
\ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b)) = x";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
+by (rtac equalityI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
by (eresolve_tac [GG_subset RS subsetD] 1 THEN TRYALL assume_tac);
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS
bij_is_fun RS apply_type] 1);
-by (eresolve_tac [ltD] 1);
-by (resolve_tac [subsetI] 1);
+by (etac ltD 1);
+by (rtac subsetI 1);
by (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [OUN_I] 1);
+by (rtac OUN_I 1);
by (resolve_tac [Ord_ordertype RSN (2, ltI)] 1 THEN (assume_tac 2));
by (eresolve_tac [ordermap_type RS apply_type] 1);
by (eresolve_tac [ordermap_bij RS bij_is_inj RS left_inverse RS ssubst] 1
@@ -666,10 +666,10 @@
\ ==> ALL b<ordertype(LL(t_n, succ(k), y), S). \
\ (GG(t_n, succ(k), y)) ` \
\ (converse(ordermap(LL(t_n, succ(k), y), S)) ` b) lepoll m";
-by (resolve_tac [oallI] 1);
+by (rtac oallI 1);
by (asm_full_simp_tac (AC_ss addsimps [ltD,
ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1);
-by (resolve_tac [eqpoll_sum_imp_Diff_lepoll] 1);
+by (rtac eqpoll_sum_imp_Diff_lepoll 1);
by (REPEAT (fast_tac (FOL_cs addSDs [ltD]
addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n]
addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n,
@@ -683,9 +683,9 @@
goalw thy [AC16_def,WO4_def]
"!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
by (excluded_middle_tac "Finite(A)" 1);
-by (resolve_tac [lemma1] 2 THEN REPEAT (assume_tac 2));
+by (rtac lemma1 2 THEN REPEAT (assume_tac 2));
by (resolve_tac [lemma2 RS revcut_rl] 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (eres_inst_tac [("x","A Un y")] allE 1);
--- a/src/ZF/AC/Hartog.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/Hartog.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/Hartog.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Some proofs on the Hartogs function.
*)
@@ -14,11 +14,11 @@
goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==> \
\ EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (REPEAT (resolve_tac [exI, conjI] 1));
by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1);
-by (resolve_tac [exI] 1);
-by (resolve_tac [conjI] 1);
+by (rtac exI 1);
+by (rtac conjI 1);
by (eresolve_tac [well_ord_Memrel RSN (2, subset_refl RSN (2,
restrict_bij RS bij_converse_bij) RS bij_is_inj RS well_ord_rvimage)] 1
THEN (assume_tac 1));
@@ -30,10 +30,10 @@
goal thy "!!X. [| Ord(a); a lepoll X |] ==> \
\ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
-by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1));
+by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1));
by (step_tac ZF_cs 1);
by (REPEAT (ares_tac [exI, conjI] 1));
-by (eresolve_tac [ordertype_Int] 2);
+by (etac ordertype_Int 2);
by (fast_tac ZF_cs 1);
val Ord_lepoll_imp_eq_ordertype = result();
@@ -43,7 +43,7 @@
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE, impE] 1));
by (assume_tac 1);
-by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1));
+by (dtac Ord_lepoll_imp_eq_ordertype 1 THEN (assume_tac 1));
by (fast_tac (ZF_cs addSIs [ReplaceI] addEs [sym]) 1);
val Ords_lepoll_set_lemma = result();
@@ -52,22 +52,22 @@
val Ords_lepoll_set = result();
goal thy "EX a. Ord(a) & ~a lepoll X";
-by (resolve_tac [swap] 1);
+by (rtac swap 1);
by (fast_tac ZF_cs 1);
-by (resolve_tac [Ords_lepoll_set] 1);
+by (rtac Ords_lepoll_set 1);
by (fast_tac ZF_cs 1);
val ex_Ord_not_lepoll = result();
goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
-by (resolve_tac [LeastI] 1);
+by (rtac LeastI 1);
by (REPEAT (fast_tac ZF_cs 1));
val HartogI = result();
val HartogE = HartogI RS notE;
goalw thy [Hartog_def] "Ord(Hartog(A))";
-by (resolve_tac [Ord_Least] 1);
+by (rtac Ord_Least 1);
val Ord_Hartog = result();
goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
--- a/src/ZF/AC/OrdQuant.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/OrdQuant.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/OrdQuant.thy
ID: $Id$
- Authors: Krzysztof Gr`abczewski and L C Paulson
+ Authors: Krzysztof Grabczewski and L C Paulson
Quantifiers and union operator for ordinals.
*)
--- a/src/ZF/AC/ROOT.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/ROOT.ML Fri Jul 28 17:21:44 1995 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
-Executes the proofs of the AC-equivalences, due to Krzysztof Gr`abczewski
+Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski
*)
ZF_build_completed; (*Make examples fail if ZF did*)
--- a/src/ZF/AC/Transrec2.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/Transrec2.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/Transrec2.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Transfinite recursion introduced to handle definitions based on the three
cases of ordinals.
@@ -8,9 +8,6 @@
open Transrec2;
-val AC_cs = OrdQuant_cs;
-val AC_ss = OrdQuant_ss;
-
goal thy "transrec2(0,a,b) = a";
by (rtac (transrec2_def RS def_transrec RS trans) 1);
by (simp_tac ZF_ss 1);
--- a/src/ZF/AC/WO1_AC.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_AC.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO1_AC.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1
@@ -42,10 +42,10 @@
goalw thy [WO1_def] "!!A. [| WO1; ALL B:A. EX C:D(B). P(C,B) |] \
\ ==> EX f. ALL B:A. P(f`B,B)";
by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1);
-by (eresolve_tac [exE] 1);
-by (dresolve_tac [ex_choice_fun] 1);
+by (etac exE 1);
+by (dtac ex_choice_fun 1);
by (fast_tac (AC_cs addEs [RepFunE, sym RS equals0D]) 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1);
by (asm_full_simp_tac AC_ss 1);
by (fast_tac (AC_cs addSDs [RepFunI RSN (2, apply_type)]
@@ -53,16 +53,16 @@
val lemma1 = result();
goalw thy [WO1_def] "!!A. [| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B";
-by (resolve_tac [eqpoll_trans] 1);
+by (rtac eqpoll_trans 1);
by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 2);
by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1);
by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1);
by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1);
by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS
InfCard_cdouble_eq RS ssubst] 1);
-by (resolve_tac [eqpoll_refl] 2);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [notE] 1);
+by (rtac eqpoll_refl 2);
+by (rtac notI 1);
+by (etac notE 1);
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite] 1
THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1);
@@ -74,7 +74,7 @@
val lemma2_2 = result();
goal thy "!!f. [| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b";
-by (resolve_tac [inj_equality] 1);
+by (rtac inj_equality 1);
by (TRYALL (fast_tac (AC_cs addSEs [inj_is_fun RS apply_Pair] addEs [subst])));
val lemma = result();
@@ -91,7 +91,7 @@
val [major, minor] = goalw thy AC_aux_defs
"[| f : bij(D+D, B); 1 le n |] ==> \
\ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))";
-by (rewrite_goals_tac [succ_def]);
+by (rewtac succ_def);
by (fast_tac (AC_cs addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI]
addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
le_imp_subset RS subset_imp_lepoll]
--- a/src/ZF/AC/WO1_WO6.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO6.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO1-WO6.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML)
@@ -46,12 +46,12 @@
val surj_imp_eq = result();
goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
by (eres_inst_tac [("x","A")] allE 1);
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (REPEAT (resolve_tac [exI, conjI] 1));
-by (eresolve_tac [Ord_ordertype] 1);
-by (resolve_tac [conjI] 1);
+by (etac Ord_ordertype 1);
+by (rtac conjI 1);
by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS
lam_sets RS domain_of_fun] 1);
by (asm_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
--- a/src/ZF/AC/WO1_WO7.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO1_WO7.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
LEMMA is the sentence denoted by (**)
@@ -21,8 +21,8 @@
goalw thy [WO1_def] "!!Z. ALL X. ~Finite(X) --> \
\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))) ==> WO1";
-by (resolve_tac [allI] 1);
-by (eresolve_tac [allE] 1);
+by (rtac allI 1);
+by (etac allE 1);
by (excluded_middle_tac "Finite(A)" 1);
by (fast_tac AC_cs 1);
by (rewrite_goals_tac [Finite_def, eqpoll_def]);
@@ -47,11 +47,11 @@
"!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))";
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1
THEN (assume_tac 1));
-by (resolve_tac [notI] 1);
+by (rtac notI 1);
by (eres_inst_tac [("x","nat")] allE 1);
-by (eresolve_tac [disjE] 1);
+by (etac disjE 1);
by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (eres_inst_tac [("x","succ(x)")] allE 1);
by (fast_tac (ZF_cs addSIs [nat_succI, converseI, MemrelI,
nat_succI RSN (2, subsetD)]) 1);
--- a/src/ZF/AC/WO1_WO8.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO1_WO8.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO1_WO8.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
*)
@@ -18,9 +18,9 @@
(* ********************************************************************** *)
goalw thy WO_defs "!!Z. WO8 ==> WO1";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
well_ord_rvimage]) 2);
by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
--- a/src/ZF/AC/WO2_AC16.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO2_AC16.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proof of WO2 ==> AC16(k #+ m, k)
@@ -24,11 +24,11 @@
\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \
\ ==> V = W";
by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1));
-by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
-by (REPEAT (dresolve_tac [ospec] 1 THEN (assume_tac 1)));
+by (dtac subsetD 1 THEN (assume_tac 1));
+by (REPEAT (dtac ospec 1 THEN (assume_tac 1)));
by (eresolve_tac [disjI2 RSN (2, impE)] 1);
by (fast_tac (FOL_cs addSIs [bexI]) 1);
-by (eresolve_tac [ex1_two_eq] 1 THEN (REPEAT (ares_tac [conjI] 1)));
+by (etac ex1_two_eq 1 THEN (REPEAT (ares_tac [conjI] 1)));
val lemma3_1 = result();
goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \
@@ -39,7 +39,7 @@
by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1
THEN (REPEAT (assume_tac 1)));
by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1)));
-by (eresolve_tac [lemma3_1] 1 THEN (REPEAT (assume_tac 1)));
+by (etac lemma3_1 1 THEN (REPEAT (assume_tac 1)));
val lemma3 = result();
goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \
@@ -60,32 +60,32 @@
\ ==> (UN x<x. F(x)) <= X & \
\ (ALL xa<a. xa < x | (EX x:UN x<x. F(x). fa(xa) <= x) \
\ --> (EX! Y. Y : (UN x<x. F(x)) & fa(xa) <= Y))";
-by (resolve_tac [conjI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
+by (rtac conjI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1));
by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac AC_cs 1);
-by (dresolve_tac [lemma4] 1 THEN (assume_tac 1));
-by (resolve_tac [oallI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
+by (dtac lemma4 1 THEN (assume_tac 1));
+by (rtac oallI 1);
+by (rtac impI 1);
+by (etac disjE 1);
by (forward_tac [Limit_has_succ RSN (2, ospec)] 1 THEN (REPEAT (assume_tac 1)));
by (dres_inst_tac [("A","a"),("x","xa")] ospec 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RS le_refl RSN (2, disjI1 RSN (2, impE))] 1
THEN (assume_tac 1));
by (REPEAT (eresolve_tac [ex1E, conjE] 1));
-by (resolve_tac [ex1I] 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 2));
+by (rtac ex1I 1);
+by (rtac conjI 1 THEN (assume_tac 2));
by (eresolve_tac [Limit_has_succ RS OUN_I] 1 THEN (TRYALL assume_tac));
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
-by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
-by (eresolve_tac [Limit_has_succ] 1 THEN (assume_tac 1));
-by (eresolve_tac [bexE] 1);
-by (resolve_tac [ex1I] 1);
-by (eresolve_tac [conjI] 1 THEN (assume_tac 1));
+by (etac lemma3 1 THEN (TRYALL assume_tac));
+by (etac Limit_has_succ 1 THEN (assume_tac 1));
+by (etac bexE 1);
+by (rtac ex1I 1);
+by (etac conjI 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
-by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
+by (etac lemma3 1 THEN (TRYALL assume_tac));
val lemma5 = result();
(* ********************************************************************** *)
@@ -105,8 +105,8 @@
goal thy "!!A. [| A eqpoll a; Card(a); ~Finite(a); B lesspoll a; \
\ C lesspoll a |] ==> A - B - C eqpoll a";
-by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Diff_lesspoll_eqpoll_Card 1 THEN (REPEAT (assume_tac 1)));
val dbl_Diff_eqpoll_Card = result();
(* ********************************************************************** *)
@@ -115,12 +115,12 @@
goalw thy [lesspoll_def]
"!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1
THEN (assume_tac 1));
-by (rewrite_goals_tac [Finite_def]);
+by (rewtac Finite_def);
by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2);
-by (resolve_tac [lepoll_trans] 1 THEN (assume_tac 2));
+by (rtac lepoll_trans 1 THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS
subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
val Finite_lesspoll_infinite_Ord = result();
@@ -132,21 +132,21 @@
goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \
\ --> Finite(Union(X))";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]
addSIs [nat_0I RS nat_into_Finite] addIs [Union_0 RS ssubst]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1));
by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1
THEN (assume_tac 1));
-by (resolve_tac [Finite_Un] 1);
+by (rtac Finite_Un 1);
by (fast_tac AC_cs 2);
by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]) 1);
val Finite_Union_lemma = result();
goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))";
by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1);
-by (dresolve_tac [Finite_Union_lemma] 1);
+by (dtac Finite_Union_lemma 1);
by (fast_tac AC_cs 1);
val Finite_Union = result();
@@ -173,10 +173,10 @@
by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1);
by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1));
by (hyp_subst_tac 1);
-by (resolve_tac [lepoll_lesspoll_lesspoll] 1);
+by (rtac lepoll_lesspoll_lesspoll 1);
by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
THEN REPEAT (assume_tac 1));
-by (resolve_tac [UN_lepoll] 1
+by (rtac UN_lepoll 1
THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord]))));
val Union_lesspoll = result();
@@ -204,7 +204,7 @@
goal thy "!!x. Ord(x) ==> \
\ recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
-by (eresolve_tac [Ord_cases] 1);
+by (etac Ord_cases 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0,
empty_subsetI RS subset_imp_lepoll]) 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit,
@@ -225,12 +225,12 @@
goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i)); \
\ w:(UN i<a. F(i)); z:(UN i<a. F(i)) |] \
\ ==> EX b<a. w:(F(b) - (UN c<b. F(c))) & z:(F(b) - (UN c<b. F(c)))";
-by (REPEAT (eresolve_tac [OUN_E] 1));
+by (REPEAT (etac OUN_E 1));
by (dresolve_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
by (forward_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
-by (resolve_tac [oexI] 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 2));
-by (eresolve_tac [subst] 1 THEN (assume_tac 1));
+by (rtac oexI 1);
+by (rtac conjI 1 THEN (assume_tac 2));
+by (etac subst 1 THEN (assume_tac 1));
by (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
THEN (REPEAT (assume_tac 1)));
val Least_eq_imp_ex = result();
@@ -243,24 +243,24 @@
\ ==> (UN x<a. F(x)) lepoll a";
by (resolve_tac [lepoll_def RS (def_imp_iff RS iffD2)] 1);
by (res_inst_tac [("x","lam z: (UN x<a. F(x)). LEAST i. z:F(i)")] exI 1);
-by (rewrite_goals_tac [inj_def]);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [lam_type] 1);
-by (eresolve_tac [OUN_E] 1);
-by (eresolve_tac [Least_in_Ord] 1);
-by (eresolve_tac [ltD] 1);
-by (eresolve_tac [lt_Ord2] 1);
-by (resolve_tac [ballI] 1);
-by (resolve_tac [ballI] 1);
+by (rewtac inj_def);
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (etac OUN_E 1);
+by (etac Least_in_Ord 1);
+by (etac ltD 1);
+by (etac lt_Ord2 1);
+by (rtac ballI 1);
+by (rtac ballI 1);
by (asm_simp_tac AC_ss 1);
-by (resolve_tac [impI] 1);
-by (dresolve_tac [Least_eq_imp_ex] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac impI 1);
+by (dtac Least_eq_imp_ex 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (AC_cs addSEs [two_in_lepoll_1]) 1);
val UN_lepoll_index = result();
goal thy "!!y. Ord(y) ==> recfunAC16(f, fa, y, a) lepoll y";
-by (eresolve_tac [trans_induct] 1);
-by (eresolve_tac [Ord_cases] 1);
+by (etac trans_induct 1);
+by (etac Ord_cases 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, lepoll_refl]) 1);
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
by (fast_tac (AC_cs addIs [conjI RS (expand_if RS iffD2)]
@@ -276,7 +276,7 @@
\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \
\ ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
-by (resolve_tac [Union_lesspoll] 1 THEN (TRYALL assume_tac));
+by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac));
by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3);
by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS
well_ord_rvimage] 2 THEN (assume_tac 2));
@@ -289,8 +289,8 @@
\ k : nat; m : nat; y<a; \
\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |] \
\ ==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
-by (resolve_tac [dbl_Diff_eqpoll_Card] 1 THEN (TRYALL assume_tac));
-by (resolve_tac [Union_recfunAC16_lesspoll] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
+by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1));
by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS
iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1
@@ -309,10 +309,10 @@
goal thy "!!x. [| x : Pow(A - B - fa`i); x eqpoll m; \
\ fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |] \
\ ==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}";
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
by (fast_tac (AC_cs addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))]
addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
-by (resolve_tac [disj_Un_eqpoll_nat_sum] 1
+by (rtac disj_Un_eqpoll_nat_sum 1
THEN (TRYALL assume_tac));
by (fast_tac (AC_cs addSIs [equals0I]) 1);
by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1
@@ -327,7 +327,7 @@
\ --> Q(x,y)); succ(j)<a |] \
\ ==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
by (dresolve_tac [succI1 RSN (2, bspec)] 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl) RS lt_trans] 1
THEN (REPEAT (assume_tac 1)));
val lemma6 = result();
@@ -371,20 +371,20 @@
val Diffs_eq_imp_eq = result();
goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
-by (REPEAT (eresolve_tac [conjE] 1));
+by (REPEAT (etac conjE 1));
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
THEN (assume_tac 1));
by (forward_tac [subsetD RS Diff_sing_lepoll] 1
THEN REPEAT (assume_tac 1));
by (forward_tac [lepoll_Diff_sing] 1);
by (REPEAT (eresolve_tac [allE, impE] 1));
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac AC_cs 2);
by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1);
-by (eresolve_tac [Diffs_eq_imp_eq] 1
+by (etac Diffs_eq_imp_eq 1
THEN REPEAT (assume_tac 1));
val subset_imp_eq_lemma = result();
@@ -394,8 +394,8 @@
goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a; \
\ y<a |] ==> b=y";
-by (dresolve_tac [subset_imp_eq] 1);
-by (eresolve_tac [nat_succI] 3);
+by (dtac subset_imp_eq 1);
+by (etac nat_succI 3);
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1);
by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS
@@ -415,22 +415,22 @@
\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1
THEN REPEAT (assume_tac 1));
-by (eresolve_tac [Card_is_Ord] 1);
+by (etac Card_is_Ord 1);
by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2));
-by (eresolve_tac [CollectE] 4);
-by (resolve_tac [bexI] 4);
-by (resolve_tac [CollectI] 5);
+by (etac CollectE 4);
+by (rtac bexI 4);
+by (rtac CollectI 5);
by (assume_tac 5);
by (eresolve_tac [add_succ RS subst] 5);
by (assume_tac 1);
-by (eresolve_tac [nat_succI] 1);
+by (etac nat_succI 1);
by (assume_tac 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac AC_cs 1);
by (REPEAT (resolve_tac [ballI, impI, oallI, notI] 1));
by (dresolve_tac [Int_empty RSN (2, subset_Un_disjoint)] 1
THEN REPEAT (assume_tac 1));
-by (dresolve_tac [bij_imp_arg_eq] 1 THEN REPEAT (assume_tac 1));
+by (dtac bij_imp_arg_eq 1 THEN REPEAT (assume_tac 1));
by (hyp_subst_tac 1);
by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac);
val ex_next_set = result();
@@ -450,8 +450,8 @@
\ ==> EX c<a. fa`y <= f`c & \
\ (ALL b<a. fa`b <= f`c --> \
\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
-by (dresolve_tac [ex_next_set] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (dtac ex_next_set 1 THEN REPEAT (assume_tac 1));
+by (etac bexE 1);
by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN
(2, oexI)] 1);
by (resolve_tac [right_inverse_bij RS ssubst] 1
@@ -472,20 +472,20 @@
\ ==> F(j) Un {L} <= X & \
\ (ALL x<a. x le j | (EX xa:F(j) Un {L}. P(x, xa)) --> \
\ (EX! Y. Y:F(j) Un {L} & P(x, Y)))";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs addSIs [singleton_subsetI]) 1);
-by (resolve_tac [oallI] 1);
-by (eresolve_tac [oallE] 1 THEN (contr_tac 2));
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
-by (eresolve_tac [leE] 1);
+by (rtac oallI 1);
+by (etac oallE 1 THEN (contr_tac 2));
+by (rtac impI 1);
+by (etac disjE 1);
+by (etac leE 1);
by (eresolve_tac [disjI1 RSN (2, impE)] 1 THEN (assume_tac 1));
-by (resolve_tac [ex1E] 1 THEN (assume_tac 1));
-by (eresolve_tac [ex1_in_Un_sing] 1);
+by (rtac ex1E 1 THEN (assume_tac 1));
+by (etac ex1_in_Un_sing 1);
by (fast_tac AC_cs 1);
by (fast_tac AC_cs 1);
-by (eresolve_tac [bexE] 1);
-by (eresolve_tac [UnE] 1);
+by (etac bexE 1);
+by (etac UnE 1);
by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1);
by (fast_tac AC_cs 1);
val lemma8 = result();
@@ -502,27 +502,27 @@
\ ==> recfunAC16(f, fa, b, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)} & \
\ (ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) --> \
\ (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))";
-by (resolve_tac [impE] 1 THEN (REPEAT (assume_tac 2)));
+by (rtac impE 1 THEN (REPEAT (assume_tac 2)));
by (eresolve_tac [lt_Ord RS trans_induct] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [Ord_cases] 1);
+by (rtac impI 1);
+by (etac Ord_cases 1);
(* case 0 *)
by (asm_simp_tac (AC_ss addsimps [recfunAC16_0]) 1);
by (fast_tac (AC_cs addSEs [ltE]) 1);
(* case Limit *)
by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 2);
-by (eresolve_tac [lemma5] 2 THEN (REPEAT (assume_tac 2)));
+by (etac lemma5 2 THEN (REPEAT (assume_tac 2)));
by (fast_tac (FOL_cs addSEs [recfunAC16_mono]) 2);
(* case succ *)
by (hyp_subst_tac 1);
by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1));
by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
-by (eresolve_tac [lemma7] 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [impI] 1);
+by (etac lemma7 1 THEN (REPEAT (assume_tac 1)));
+by (rtac impI 1);
by (resolve_tac [ex_next_Ord RS oexE] 1
THEN REPEAT (ares_tac [le_refl RS lt_trans] 1));
-by (eresolve_tac [lemma8] 1 THEN (assume_tac 1));
+by (etac lemma8 1 THEN (assume_tac 1));
by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1));
by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1
THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1));
@@ -540,23 +540,23 @@
\ f:a->f``(a); Limit(a); (!!i j. i le j ==> F(i) <= F(j)) |] \
\ ==> (UN j<a. F(j)) <= S & \
\ (ALL x:f``a. EX! Y. Y : (UN j<a. F(j)) & x <= Y)";
-by (resolve_tac [conjI] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [OUN_E] 1);
-by (dresolve_tac [prem1] 1);
+by (rtac conjI 1);
+by (rtac subsetI 1);
+by (etac OUN_E 1);
+by (dtac prem1 1);
by (fast_tac AC_cs 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [imageE] 1);
+by (rtac ballI 1);
+by (etac imageE 1);
by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
(prem3 RS Limit_has_succ)] 1);
by (forward_tac [prem1] 1);
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (fast_tac (AC_cs addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1);
by (dresolve_tac [prem2 RSN (2, apply_equality)] 1);
by (REPEAT (eresolve_tac [conjE, ex1E] 1));
-by (resolve_tac [ex1I] 1);
+by (rtac ex1I 1);
by (fast_tac (AC_cs addSIs [OUN_I]) 1);
by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1));
@@ -565,10 +565,10 @@
by (forward_tac [prem1] 1);
by (forward_tac [succ_leE] 1);
by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1));
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac));
by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1));
-by (eresolve_tac [ex1_two_eq] 1);
+by (etac ex1_two_eq 1);
by (REPEAT (fast_tac FOL_cs 1));
val lemma_simp_induct = result();
@@ -578,8 +578,8 @@
goalw thy [AC16_def]
"!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (rtac impI 1);
by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1)));
by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
THEN (REPEAT (ares_tac [add_type] 1)));
@@ -589,17 +589,17 @@
def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
-by (REPEAT (eresolve_tac [exE] 1));
+by (REPEAT (etac exE 1));
by (res_inst_tac [("x","UN j<a. recfunAC16(fa,f,j,a)")] exI 1);
by (res_inst_tac [("P","%z. ?Y & (ALL x:z. ?Z(x))")]
(bij_is_surj RS surj_image_eq RS subst) 1
THEN (assume_tac 1));
-by (resolve_tac [lemma_simp_induct] 1);
+by (rtac lemma_simp_induct 1);
by (eresolve_tac [bij_is_fun RS surj_image RS surj_is_fun] 2);
by (eresolve_tac [eqpoll_imp_lepoll RS lepoll_infinite RS
infinite_Card_is_InfCard RS InfCard_is_Limit] 2
THEN REPEAT (assume_tac 2));
-by (eresolve_tac [recfunAC16_mono] 2);
-by (resolve_tac [main_induct] 1
+by (etac recfunAC16_mono 2);
+by (rtac main_induct 1
THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1));
qed "WO2_AC16";
--- a/src/ZF/AC/WO6_WO1.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO6_WO1.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proof of "WO6 ==> WO1". Simplified by L C Paulson.
@@ -111,7 +111,7 @@
goal thy "!!a b. [| P(a, b); Ord(a); Ord(b); \
\ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \
\ ==> P(Least_a, LEAST b. P(Least_a, b))";
-by (eresolve_tac [ssubst] 1);
+by (etac ssubst 1);
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
by (REPEAT (fast_tac (ZF_cs addSEs [LeastI]) 1));
val nested_LeastI = result();
@@ -141,7 +141,7 @@
by (asm_simp_tac (ZF_ss addsimps [ww1_def]) 1);
by (excluded_middle_tac "f`(b--a) = 0" 1);
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
-by (resolve_tac [Diff_lepoll] 1);
+by (rtac Diff_lepoll 1);
by (fast_tac AC_cs 1);
by (rtac vv1_subset 1);
by (dtac (ospec RS mp) 1);
@@ -170,7 +170,7 @@
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
\ y*y<=y; (UN b<a. f`b)=y |] \
\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
-by (dresolve_tac [ex_d_uu_not_empty] 1 THEN REPEAT (assume_tac 1));
+by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
by (fast_tac (AC_cs addSEs [LeastI, lt_Ord]) 1);
val uu_not_empty = result();
@@ -194,12 +194,12 @@
(*Could this be proved more directly?*)
goal thy "!!A B. [| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
by (hyp_subst_tac 1);
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
by (assume_tac 2);
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
by (excluded_middle_tac "?P" 1 THEN (assume_tac 2));
by (eresolve_tac [subset_Diff_sing RS subset_imp_lepoll RSN (2,
Diff_sing_lepoll RSN (3, lepoll_trans RS lepoll_trans)) RS
@@ -246,7 +246,7 @@
\ ALL b<a. f`b lepoll succ(m); y*y<=y; \
\ (UN b<a.f`b)=y; Ord(a); m:nat; s:f`b; b<a \
\ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
-bd sym 1;
+by (dtac sym 1);
by (asm_simp_tac
(OrdQuant_ss addsimps [UN_oadd, lt_oadd1,
oadd_le_self RS le_imp_not_lt, lt_Ord,
@@ -278,8 +278,8 @@
\ |] ==> ww2(f,b,g,d) lepoll m";
by (excluded_middle_tac "f`g = 0" 1);
by (asm_simp_tac (OrdQuant_ss addsimps [empty_lepollI]) 2);
-by (dresolve_tac [ospec] 1 THEN (assume_tac 1));
-by (resolve_tac [Diff_lepoll] 1
+by (dtac ospec 1 THEN (assume_tac 1));
+by (rtac Diff_lepoll 1
THEN (TRYALL assume_tac));
by (asm_simp_tac (OrdQuant_ss addsimps [vv2_def, expand_if, not_emptyI]) 1);
val ww2_lepoll = result();
@@ -312,8 +312,8 @@
(* case 2 *)
by (REPEAT (eresolve_tac [oexE, conjE] 1));
by (res_inst_tac [("A","f`?B")] not_emptyE 1 THEN (assume_tac 1));
-by (resolve_tac [CollectI] 1);
-by (eresolve_tac [succ_natD] 1);
+by (rtac CollectI 1);
+by (etac succ_natD 1);
by (res_inst_tac [("x","a++a")] exI 1);
by (res_inst_tac [("x","gg2(f,a,b,x)")] exI 1);
(*Calling fast_tac might get rid of the res_inst_tac calls, but it
@@ -392,25 +392,25 @@
goal thy "!!f. [| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
\ ==> f` (LEAST i. f`i = {x}) = {x}";
-by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
by (fast_tac (AC_cs addSEs [lt_Ord] addIs [LeastI]) 1);
val lemma2 = result();
goalw thy [NN_def] "!!y. 1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (res_inst_tac [("x","a")] exI 1);
by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
-by (resolve_tac [conjI] 1 THEN (assume_tac 1));
+by (rtac conjI 1 THEN (assume_tac 1));
by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
-by (dresolve_tac [lemma1] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
by (fast_tac (AC_cs addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
by (fast_tac (ZF_cs addSIs [the_equality]) 1);
val NN_imp_ex_inj = result();
goal thy "!!y. [| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
-by (dresolve_tac [NN_imp_ex_inj] 1);
+by (dtac NN_imp_ex_inj 1);
by (fast_tac (ZF_cs addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
val y_well_ord = result();
@@ -422,7 +422,7 @@
"[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
\ ==> n~=0 --> P(n) --> P(1)";
by (res_inst_tac [("n","n")] nat_induct 1);
-by (resolve_tac [prem1] 1);
+by (rtac prem1 1);
by (fast_tac ZF_cs 1);
by (excluded_middle_tac "x=0" 1);
by (fast_tac ZF_cs 2);
@@ -434,7 +434,7 @@
\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
\ ==> P(1)";
by (resolve_tac [rev_induct_lemma RS impE] 1);
-by (eresolve_tac [impE] 4 THEN (assume_tac 5));
+by (etac impE 4 THEN (assume_tac 5));
by (REPEAT (ares_tac prems 1));
val rev_induct = result();
@@ -443,8 +443,8 @@
val NN_into_nat = result();
goal thy "!!n. [| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
-by (resolve_tac [rev_induct] 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
-by (resolve_tac [lemma_ii] 1 THEN REPEAT (assume_tac 1));
+by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
+by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1));
val lemma3 = result();
(* ********************************************************************** *)
@@ -458,12 +458,12 @@
val NN_y_0 = result();
goalw thy [WO1_def] "!!Z. WO6 ==> WO1";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
by (excluded_middle_tac "A=0" 1);
by (fast_tac (ZF_cs addSIs [well_ord_Memrel, nat_0I RS nat_into_Ord]) 2);
by (res_inst_tac [("x1","A")] (lemma_iv RS revcut_rl) 1);
-by (eresolve_tac [exE] 1);
-by (dresolve_tac [WO6_imp_NN_not_empty] 1);
+by (etac exE 1);
+by (dtac WO6_imp_NN_not_empty 1);
by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1);
by (eres_inst_tac [("A","NN(y)")] not_emptyE 1);
by (forward_tac [y_well_ord] 1);
--- a/src/ZF/AC/WO_AC.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/WO_AC.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/WO_AC.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Lemmas used in the proofs like WO? ==> AC?
*)
--- a/src/ZF/AC/first.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/first.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/first.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Lemmas involving the first element of a well ordered set
*)
@@ -15,7 +15,7 @@
"!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
by (contr_tac 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (res_inst_tac [("a","x")] ex1I 1);
by (fast_tac ZF_cs 2);
by (rewrite_goals_tac [tot_ord_def, linear_def]);
@@ -23,7 +23,7 @@
val well_ord_imp_ex1_first = result();
goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
-by (dresolve_tac [well_ord_imp_ex1_first] 1 THEN REPEAT (assume_tac 1));
-by (resolve_tac [first_is_elem] 1);
-by (eresolve_tac [theI] 1);
+by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1));
+by (rtac first_is_elem 1);
+by (etac theI 1);
val the_first_in = result();
--- a/src/ZF/AC/recfunAC16.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/recfunAC16.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/recfunAC16.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Properties of the recursive definition used in the proof of WO2 ==> AC16
*)
@@ -12,7 +12,7 @@
(* ********************************************************************** *)
goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0";
-by (resolve_tac [transrec2_0] 1);
+by (rtac transrec2_0 1);
val recfunAC16_0 = result();
goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \
@@ -20,12 +20,12 @@
\ recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j & \
\ (ALL b<a. (fa`b <= f`j \
\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
-by (resolve_tac [transrec2_succ] 1);
+by (rtac transrec2_succ 1);
val recfunAC16_succ = result();
goalw thy [recfunAC16_def] "!!i. Limit(i) \
\ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))";
-by (eresolve_tac [transrec2_Limit] 1);
+by (etac transrec2_Limit 1);
val recfunAC16_Limit = result();
(* ********************************************************************** *)
@@ -36,7 +36,7 @@
"[| !!g r. r <= B(g,r); Ord(i) |] \
\ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)";
by (resolve_tac [prem2 RS trans_induct] 1);
-by (resolve_tac [Ord_cases] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac lt_cs 1);
by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1);
by (fast_tac (FOL_cs addSIs [succI1, prem1]
@@ -59,7 +59,7 @@
goalw thy [recfunAC16_def]
"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
-by (resolve_tac [transrec2_mono] 1);
+by (rtac transrec2_mono 1);
by (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1));
val recfunAC16_mono = result();
--- a/src/ZF/AC/rel_is_fun.ML Fri Jul 28 12:01:12 1995 +0200
+++ b/src/ZF/AC/rel_is_fun.ML Fri Jul 28 17:21:44 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/rel_is_fun.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Lemmas needed to state when a finite relation is a function.
@@ -11,23 +11,23 @@
(*Using AC we could trivially prove, for all u, domain(u) lepoll u*)
goalw Cardinal.thy [lepoll_def]
"!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (res_inst_tac [("x",
"lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1);
by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1);
by (fast_tac (ZF_cs addIs [LeastI2, nat_into_Ord RS Ord_in_Ord,
inj_is_fun RS apply_type]) 1);
-by (eresolve_tac [domainE] 1);
+by (etac domainE 1);
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
-by (resolve_tac [LeastI2] 1);
+by (rtac LeastI2 1);
by (REPEAT (fast_tac (ZF_cs addIs [fst_conv, left_inverse RS ssubst]
addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
val lepoll_m_imp_domain_lepoll_m = result();
goal ZF.thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
by (fast_tac (ZF_cs addSIs [domain_mono]) 1);
-by (resolve_tac [subsetI] 1);
+by (rtac subsetI 1);
by (excluded_middle_tac "x = a" 1);
by (REPEAT (fast_tac (ZF_cs addSIs [domainI] addSEs [domainE]) 1));
val domain_Diff_eq_domain = result();