--- a/src/ZF/AC/AC7_AC9.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/AC7-AC9.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
instances of AC.
@@ -25,22 +25,22 @@
val Sigma_fun_space_not0 = result();
goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
-by (REPEAT (resolve_tac [ballI] 1));
+by (REPEAT (rtac ballI 1));
by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
THEN REPEAT (assume_tac 1));
val all_eqpoll_imp_pair_eqpoll = result();
goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \
\ |] ==> P(b)=R(b)";
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (dtac bspec 1 THEN (assume_tac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE1 = result();
goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
-by (resolve_tac [ballI] 1);
-by (resolve_tac [impI] 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (rtac ballI 1);
+by (rtac impI 1);
+by (dtac bspec 1 THEN (assume_tac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE2 = result();
@@ -54,18 +54,18 @@
"!!A. C:A ==> (lam g:(nat->Union(A))*C. \
\ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \
\ : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
-by (resolve_tac [CollectI] 1);
+by (rtac CollectI 1);
by (fast_tac (ZF_cs addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
fst_type,diff_type,nat_succI,nat_0I]) 1);
by (REPEAT (resolve_tac [ballI, impI] 1));
by (asm_full_simp_tac ZF_ss 1);
-by (REPEAT (eresolve_tac [SigmaE] 1));
+by (REPEAT (etac SigmaE 1));
by (REPEAT (hyp_subst_tac 1));
by (asm_full_simp_tac ZF_ss 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2);
by (asm_full_simp_tac AC_ss 2);
-by (resolve_tac [fun_extension] 1 THEN REPEAT (assume_tac 1));
+by (rtac fun_extension 1 THEN REPEAT (assume_tac 1));
by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1));
by (asm_full_simp_tac (AC_ss addsimps [succ_not_0 RS if_not_P]) 1);
by (fast_tac (AC_cs addSEs [diff_succ_succ RS (diff_0 RSN (2, trans)) RS subst]
@@ -73,10 +73,10 @@
val lemma = result();
goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
-by (resolve_tac [eqpollI] 1);
+by (rtac eqpollI 1);
by (fast_tac (ZF_cs addSEs [prod_lepoll_self, not_sym RS not_emptyE,
subst_elem] addEs [swap]) 2);
-by (rewrite_goals_tac [lepoll_def]);
+by (rewtac lepoll_def);
by (fast_tac (ZF_cs addSIs [lemma]) 1);
val Sigma_fun_space_eqpoll = result();
@@ -116,13 +116,13 @@
val lemma2 = result();
goalw thy AC_defs "!!Z. AC7 ==> AC6";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (rtac impI 1);
by (excluded_middle_tac "A=0" 1);
by (fast_tac (ZF_cs addSIs [not_emptyI, empty_fun]) 2);
-by (resolve_tac [lemma1] 1);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1 THEN (assume_tac 2));
+by (rtac lemma1 1);
+by (etac allE 1);
+by (etac impE 1 THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [RepFunE]
addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
Sigma_fun_space_eqpoll]) 1);
@@ -136,9 +136,9 @@
goalw thy [eqpoll_def]
"!!A. ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \
\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
-by (resolve_tac [notI] 1);
-by (eresolve_tac [RepFunE] 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (rtac notI 1);
+by (etac RepFunE 1);
+by (dtac bspec 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [exE,conjE] 1));
by (hyp_subst_tac 1);
by (asm_full_simp_tac AC_ss 1);
@@ -152,11 +152,11 @@
val lemma2 = result();
goalw thy AC_defs "!!Z. AC1 ==> AC8";
-by (resolve_tac [allI] 1);
-by (eresolve_tac [allE] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [impE] 1);
-by (eresolve_tac [lemma1] 1);
+by (rtac allI 1);
+by (etac allE 1);
+by (rtac impI 1);
+by (etac impE 1);
+by (etac lemma1 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
qed "AC1_AC8";
@@ -177,11 +177,11 @@
val lemma2 = result();
goalw thy AC_defs "!!Z. AC8 ==> AC9";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
-by (eresolve_tac [lemma1] 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac allE 1);
+by (etac impE 1);
+by (etac lemma1 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
qed "AC8_AC9";
@@ -218,20 +218,20 @@
\ Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2) \
\ ==> (lam B:A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) : \
\ (PROD X:A. X)";
-by (resolve_tac [lam_type] 1);
-by (resolve_tac [snd_type] 1);
-by (resolve_tac [fst_type] 1);
+by (rtac lam_type 1);
+by (rtac snd_type 1);
+by (rtac fst_type 1);
by (resolve_tac [consI1 RSN (2, apply_type)] 1);
by (fast_tac (ZF_cs addSIs [fun_weaken_type, bij_is_fun]) 1);
val lemma2 = result();
goalw thy AC_defs "!!Z. AC9 ==> AC1";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [allE] 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac allE 1);
by (excluded_middle_tac "A=0" 1);
by (fast_tac (FOL_cs addSIs [empty_fun]) 2);
-by (eresolve_tac [impE] 1);
-by (resolve_tac [lemma1] 1 THEN (REPEAT (assume_tac 1)));
+by (etac impE 1);
+by (rtac lemma1 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (AC_cs addSEs [lemma2]) 1);
qed "AC9_AC1";
--- a/src/ZF/AC/AC_Equiv.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/AC_Equiv.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
*)
@@ -71,7 +71,7 @@
(*I don't know where to put this one.*)
goal Cardinal.thy
"!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
-by (resolve_tac [not_emptyE] 1 THEN (assume_tac 1));
+by (rtac not_emptyE 1 THEN (assume_tac 1));
by (forward_tac [singleton_subsetI] 1);
by (forward_tac [subsetD] 1 THEN (assume_tac 1));
by (res_inst_tac [("A2","A")]
@@ -90,7 +90,7 @@
(* lemma for ordertype_Int *)
goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
by (step_tac ZF_cs 1);
by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1
THEN (assume_tac 1));
@@ -156,7 +156,7 @@
(* ********************************************************************** *)
goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y";
-by (eresolve_tac [ex1E] 1);
+by (etac ex1E 1);
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1);
by (fast_tac AC_cs 1);
by (fast_tac AC_cs 1);
@@ -167,7 +167,7 @@
(* ********************************************************************** *)
goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B";
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [RepFunE, apply_type]
addSIs [RepFunI] addIs [equalityI]) 1);
--- a/src/ZF/AC/Cardinal_aux.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/Cardinal_aux.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Auxiliary lemmas concerning cardinalities
*)
@@ -15,8 +15,8 @@
val nat_0_in_2 = Ord_0 RS le_refl RS leI RS ltD;
goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)";
-by (resolve_tac [conjI] 1);
-by (resolve_tac [Card_cardinal] 1);
+by (rtac conjI 1);
+by (rtac Card_cardinal 1);
by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1);
by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll
RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1
@@ -49,7 +49,7 @@
goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \
\ ==> A Un B eqpoll i";
-by (resolve_tac [eqpollI] 1);
+by (rtac eqpollI 1);
by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll
RS lepoll_trans)] 2);
by (fast_tac AC_cs 2);
@@ -70,26 +70,26 @@
goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] \
\ ==> A Un C lepoll B Un D";
-by (REPEAT (eresolve_tac [exE] 1));
+by (REPEAT (etac exE 1));
by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1);
by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")]
lam_injective 1);
by (split_tac [expand_if] 1);
-by (eresolve_tac [UnE] 1);
+by (etac UnE 1);
by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1);
by (REPEAT (split_tac [expand_if] 1));
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type]
addEs [swap]) 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [UnE] 1);
+by (rtac impI 1);
+by (etac UnE 1);
by (contr_tac 1);
-by (resolve_tac [conjI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [equals0D] 1);
+by (rtac conjI 1);
+by (rtac impI 1);
+by (etac equals0D 1);
by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
by (fast_tac (AC_cs addSEs [left_inverse]) 1);
val Un_lepoll_Un = result();
@@ -123,7 +123,7 @@
goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \
\ ==> A Un B lepoll i";
by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1);
-by (eresolve_tac [conjE] 1);
+by (etac conjE 1);
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1);
by (assume_tac 1);
by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1)));
@@ -134,10 +134,10 @@
goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j";
by (eresolve_tac [Least_le RS leE] 1);
-by (eresolve_tac [Ord_in_Ord] 1 THEN (assume_tac 1));
-by (eresolve_tac [ltE] 1);
+by (etac Ord_in_Ord 1 THEN (assume_tac 1));
+by (etac ltE 1);
by (fast_tac (AC_cs addDs [OrdmemD]) 1);
-by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (etac subst_elem 1 THEN (assume_tac 1));
val Least_in_Ord = result();
goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \
@@ -145,7 +145,7 @@
by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1);
by (fast_tac (AC_cs addSIs [Diff_sing_lepoll, the_first_in]) 1);
by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1);
-by (resolve_tac [empty_lepollI] 2);
+by (rtac empty_lepollI 2);
by (fast_tac (AC_cs addSIs [equalityI]) 1);
val Diff_first_lepoll = result();
@@ -162,24 +162,24 @@
goal thy "!!a T. [| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \
\ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a";
-by (eresolve_tac [nat_induct] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (etac nat_induct 1);
+by (rtac allI 1);
+by (rtac impI 1);
by (res_inst_tac [("b","UN b:a. f`b")] subst 1);
-by (resolve_tac [empty_lepollI] 2);
+by (rtac empty_lepollI 2);
by (resolve_tac [equals0I RS sym] 1);
by (REPEAT (eresolve_tac [UN_E, allE] 1));
by (fast_tac (AC_cs addDs [lepoll_0_is_0 RS subst]) 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
+by (rtac allI 1);
+by (rtac impI 1);
by (eres_inst_tac [("x","lam x:a. f`x - {THE b. first(b,f`x,R)}")] allE 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (asm_full_simp_tac AC_ss 1);
by (fast_tac (AC_cs addSIs [Diff_first_lepoll]) 1);
by (asm_full_simp_tac AC_ss 1);
by (resolve_tac [UN_subset_split RS subset_imp_lepoll RS lepoll_trans] 1);
-by (resolve_tac [Un_lepoll_Inf_Ord] 1 THEN (REPEAT_FIRST assume_tac));
-by (eresolve_tac [UN_sing_lepoll] 1);
+by (rtac Un_lepoll_Inf_Ord 1 THEN (REPEAT_FIRST assume_tac));
+by (etac UN_sing_lepoll 1);
val UN_fun_lepoll_lemma = result();
goal thy "!!a f. [| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \
@@ -190,7 +190,7 @@
goal thy "!!a f. [| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \
\ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a";
-by (resolve_tac [impE] 1 THEN (assume_tac 3));
+by (rtac impE 1 THEN (assume_tac 3));
by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2
THEN (TRYALL assume_tac));
by (simp_tac AC_ss 2);
@@ -198,16 +198,16 @@
val UN_lepoll = result();
goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))";
-by (resolve_tac [equalityI] 1);
+by (rtac equalityI 1);
by (fast_tac AC_cs 2);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [UN_E] 1);
-by (resolve_tac [UN_I] 1);
+by (rtac subsetI 1);
+by (etac UN_E 1);
+by (rtac UN_I 1);
by (res_inst_tac [("P","%z. x:F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [DiffI] 1);
+by (rtac DiffI 1);
by (resolve_tac [Ord_in_Ord RSN (2, LeastI)] 1 THEN (REPEAT (assume_tac 1)));
-by (resolve_tac [notI] 1);
-by (eresolve_tac [UN_E] 1);
+by (rtac notI 1);
+by (etac UN_E 1);
by (eres_inst_tac [("P","%z. x:F(z)"),("i","c")] less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 1);
val UN_eq_UN_Diffs = result();
@@ -216,7 +216,7 @@
by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
by (res_inst_tac [("d","%z. case(%x.x, %x.x, z)")] lam_bijective 1);
by (fast_tac (AC_cs addSIs [if_type, InlI, InrI]) 1);
-by (TRYALL (eresolve_tac [sumE]));
+by (TRYALL (etac sumE ));
by (TRYALL (split_tac [expand_if]));
by (TRYALL (asm_simp_tac sum_ss));
by (fast_tac (AC_cs addDs [equals0D]) 1);
@@ -224,7 +224,7 @@
goalw thy [lepoll_def, eqpoll_def]
"!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
-by (eresolve_tac [exE] 1);
+by (etac exE 1);
by (forward_tac [subset_refl RSN (2, restrict_bij)] 1);
by (res_inst_tac [("x","f``a")] exI 1);
by (fast_tac (AC_cs addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1);
@@ -235,7 +235,7 @@
(* ********************************************************************** *)
goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
-by (resolve_tac [eqpoll_trans] 1);
+by (rtac eqpoll_trans 1);
by (eresolve_tac [nat_implies_well_ord RS (
nat_implies_well_ord RSN (2,
well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1
@@ -253,17 +253,17 @@
by (forw_inst_tac [("A2","b")]
([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1
THEN REPEAT (assume_tac 1));
-by (eresolve_tac [disjE] 1);
-by (eresolve_tac [ltI] 1);
-by (eresolve_tac [Ord_ordertype] 1);
-by (eresolve_tac [disjE] 1);
+by (etac disjE 1);
+by (etac ltI 1);
+by (etac Ord_ordertype 1);
+by (etac disjE 1);
by (REPEAT (eresolve_tac [conjE,notE] 1));
by (resolve_tac [exI RS (eqpoll_def RS (def_imp_iff RS iffD2))] 1);
by (eresolve_tac [ordermap_bij RS comp_bij] 1);
-by (eresolve_tac [ssubst] 1);
+by (etac ssubst 1);
by (eresolve_tac [ordermap_bij RS bij_converse_bij] 1);
by (REPEAT (eresolve_tac [conjE,notE] 1));
-by (eresolve_tac [eqpollI] 1);
+by (etac eqpollI 1);
by (resolve_tac [Ord_ordertype RSN (2, OrdmemD RS subset_imp_lepoll) RSN (2,
eqpoll_ordertype RS eqpoll_imp_lepoll RS (
eqpoll_ordertype RS eqpoll_sym RS eqpoll_imp_lepoll RSN (3,
@@ -306,9 +306,9 @@
val le_in_nat = result();
goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)";
-by (REPEAT (eresolve_tac [bexE] 1));
-by (REPEAT (dresolve_tac [eqpoll_imp_lepoll] 1));
-by (dresolve_tac [sum_lepoll_mono] 1 THEN (assume_tac 1));
+by (REPEAT (etac bexE 1));
+by (REPEAT (dtac eqpoll_imp_lepoll 1));
+by (dtac sum_lepoll_mono 1 THEN (assume_tac 1));
by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2,
Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1
THEN (REPEAT (assume_tac 1)));
@@ -339,7 +339,7 @@
THEN (assume_tac 1));
by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1
THEN (assume_tac 1));
-by (dresolve_tac [Un_least_lt] 1 THEN (assume_tac 1));
+by (dtac Un_least_lt 1 THEN (assume_tac 1));
by (dresolve_tac [le_imp_lepoll RSN
(2, eqpoll_imp_lepoll RS lepoll_trans)] 1
THEN (assume_tac 1));
@@ -363,8 +363,8 @@
goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \
\ ==> A - B eqpoll a";
-by (resolve_tac [swap] 1 THEN (fast_tac AC_cs 1));
-by (resolve_tac [Diff_lesspoll_eqpoll_Card_lemma] 1 THEN (REPEAT (assume_tac 1)));
+by (rtac swap 1 THEN (fast_tac AC_cs 1));
+by (rtac Diff_lesspoll_eqpoll_Card_lemma 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (AC_cs addSIs [lesspoll_def RS def_imp_iff RS iffD2,
subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
val Diff_lesspoll_eqpoll_Card = result();
--- a/src/ZF/AC/DC.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/DC.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/DC.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
The proofs concerning the Axiom of Dependent Choice
*)
@@ -43,13 +43,13 @@
\ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \
\ domain(snd(z))=succ(domain(fst(z))) \
\ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0";
-by (eresolve_tac [ballE] 1);
+by (etac ballE 1);
by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2);
by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [SigmaI] 1);
+by (rtac CollectI 1);
+by (rtac SigmaI 1);
by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1);
by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type]
addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing,
@@ -67,25 +67,25 @@
\ (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}). \
\ domain(snd(z))=succ(domain(fst(z))) \
\ & restrict(snd(z), domain(fst(z))) = fst(z)})";
-by (resolve_tac [range_subset_domain] 1);
-by (resolve_tac [subsetI] 2);
-by (eresolve_tac [CollectD1] 2);
-by (eresolve_tac [UN_E] 1);
-by (eresolve_tac [CollectE] 1);
+by (rtac range_subset_domain 1);
+by (rtac subsetI 2);
+by (etac CollectD1 2);
+by (etac UN_E 1);
+by (etac CollectE 1);
by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1
THEN (assume_tac 1));
by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)]
MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1
THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1);
-by (resolve_tac [CollectI] 1);
-by (resolve_tac [SigmaI] 1);
+by (rtac CollectI 1);
+by (rtac SigmaI 1);
by (fast_tac AC_cs 1);
-by (resolve_tac [UN_I] 1);
-by (eresolve_tac [nat_succI] 1);
-by (resolve_tac [CollectI] 1);
-by (eresolve_tac [cons_fun_type2] 1 THEN (assume_tac 1));
+by (rtac UN_I 1);
+by (etac nat_succI 1);
+by (rtac CollectI 1);
+by (etac cons_fun_type2 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [succE] addss (AC_ss
addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1);
by (asm_full_simp_tac (AC_ss
@@ -104,14 +104,14 @@
\ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \
\ XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); f:k->X \
\ |] ==> g:succ(k)->X";
-by (eresolve_tac [CollectE] 1);
-by (dresolve_tac [SigmaD2] 1);
+by (etac CollectE 1);
+by (dtac SigmaD2 1);
by (hyp_subst_tac 1);
-by (eresolve_tac [UN_E] 1);
-by (eresolve_tac [CollectE] 1);
+by (etac UN_E 1);
+by (etac CollectE 1);
by (asm_full_simp_tac AC_ss 1);
-by (dresolve_tac [domain_of_fun] 1);
-by (eresolve_tac [conjE] 1);
+by (dtac domain_of_fun 1);
+by (etac conjE 1);
by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1));
by (fast_tac AC_cs 1);
val lemma2_1 = result();
@@ -123,24 +123,24 @@
\ f: nat -> XX; n:nat \
\ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \
\ & <f`succ(n)``n, f`succ(n)`n> : R";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
by (asm_full_simp_tac AC_ss 1);
-by (eresolve_tac [UN_E] 1);
-by (eresolve_tac [CollectE] 1);
-by (resolve_tac [bexI] 1 THEN (assume_tac 2));
+by (etac UN_E 1);
+by (etac CollectE 1);
+by (rtac bexI 1 THEN (assume_tac 2));
by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)]
addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
-by (eresolve_tac [conjE] 1);
-by (dresolve_tac [lemma2_1] 1 THEN REPEAT (assume_tac 1));
+by (etac conjE 1);
+by (dtac lemma2_1 1 THEN REPEAT (assume_tac 1));
by (hyp_subst_tac 1);
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1
THEN (assume_tac 1));
-by (eresolve_tac [UN_E] 1);
-by (eresolve_tac [CollectE] 1);
+by (etac UN_E 1);
+by (etac CollectE 1);
by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1
THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ]
@@ -153,21 +153,21 @@
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \
\ f: nat -> XX; n:nat \
\ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x";
-by (eresolve_tac [nat_induct] 1);
+by (etac nat_induct 1);
by (fast_tac AC_cs 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [succE] 1);
-by (resolve_tac [restrict_eq_imp_val_eq] 1);
+by (rtac ballI 1);
+by (etac succE 1);
+by (rtac restrict_eq_imp_val_eq 1);
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
by (asm_full_simp_tac AC_ss 1);
-by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma2 1 THEN REPEAT (assume_tac 1));
by (fast_tac (AC_cs addSDs [domain_of_fun]) 1);
by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1));
by (eresolve_tac [sym RS trans RS sym] 1);
by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1);
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
by (asm_full_simp_tac AC_ss 1);
-by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1));
+by (dtac lemma2 1 THEN REPEAT (assume_tac 1));
by (fast_tac (FOL_cs addSDs [domain_of_fun]
addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1);
val lemma3_1 = result();
@@ -183,7 +183,7 @@
\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \
\ f: nat -> XX; n:nat \
\ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n";
-by (eresolve_tac [natE] 1);
+by (etac natE 1);
by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1);
by (resolve_tac [image_lam RS ssubst] 1);
by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1);
@@ -197,7 +197,7 @@
val lemma3 = result();
goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C";
-by (resolve_tac [Pi_type] 1 THEN (assume_tac 1));
+by (rtac Pi_type 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [apply_type]) 1);
val fun_type_gen = result();
@@ -206,11 +206,11 @@
by (REPEAT (eresolve_tac [conjE, allE] 1));
by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1
THEN (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1);
by (fast_tac (AC_cs addSIs [lam_type] addSDs [refl RS lemma2]
addSEs [fun_type_gen, apply_type]) 2);
-by (resolve_tac [oallI] 1);
+by (rtac oallI 1);
by (forward_tac [ltD RSN (3, refl RS lemma2)] 1
THEN assume_tac 2);
by (fast_tac (AC_cs addSEs [fun_type_gen]) 1);
@@ -257,29 +257,29 @@
val lesspoll_nat_is_Finite = result();
goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
-by (eresolve_tac [nat_induct] 1);
-by (resolve_tac [allI] 1);
+by (etac nat_induct 1);
+by (rtac allI 1);
by (fast_tac (AC_cs addSIs [Fin.emptyI]
addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [conjE] 1);
+by (rtac allI 1);
+by (rtac impI 1);
+by (etac conjE 1);
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1
THEN (assume_tac 1));
by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1));
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
+by (etac allE 1);
+by (etac impE 1);
by (fast_tac AC_cs 1);
-by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
+by (dtac subsetD 1 THEN (assume_tac 1));
by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1));
by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1);
val Finite_Fin_lemma = result();
goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)";
-by (eresolve_tac [bexE] 1);
-by (dresolve_tac [Finite_Fin_lemma] 1);
-by (eresolve_tac [allE] 1);
-by (eresolve_tac [impE] 1);
+by (etac bexE 1);
+by (dtac Finite_Fin_lemma 1);
+by (etac allE 1);
+by (etac impE 1);
by (assume_tac 2);
by (fast_tac AC_cs 1);
val Finite_Fin = result();
@@ -301,11 +301,11 @@
\ range(R) <= domain(R); x:domain(R) \
\ |] ==> RR <= Pow(XX)*XX & \
\ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE]
addSIs [subsetI, SigmaI]) 1);
-by (resolve_tac [ballI] 1);
-by (resolve_tac [impI] 1);
+by (rtac ballI 1);
+by (rtac impI 1);
by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
THEN (assume_tac 1));
by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \
@@ -343,7 +343,7 @@
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
\ u=k; n:nat \
\ |] ==> f`n : succ(k) -> domain(R)";
-by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (dtac apply_type 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1);
val f_n_type = result();
@@ -351,11 +351,11 @@
\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
\ domain(f`n) = succ(k); n:nat \
\ |] ==> ALL i:k. <f`n`i, f`n`succ(i)> : R";
-by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
-by (eresolve_tac [UN_E] 1);
-by (eresolve_tac [CollectE] 1);
+by (dtac apply_type 1 THEN (assume_tac 1));
+by (etac UN_E 1);
+by (etac CollectE 1);
by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1));
-by (dresolve_tac [succ_eqD] 1);
+by (dtac succ_eqD 1);
by (asm_full_simp_tac AC_ss 1);
val f_n_pairs_in_R = result();
@@ -363,7 +363,7 @@
"!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \
\ |] ==> restrict(cons(<n, y>, f), domain(x)) = x";
by (eresolve_tac [sym RS trans RS sym] 1);
-by (resolve_tac [fun_extension] 1);
+by (rtac fun_extension 1);
by (fast_tac (AC_cs addSIs [lam_type]) 1);
by (fast_tac (AC_cs addSIs [lam_type]) 1);
by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1);
@@ -375,12 +375,12 @@
\ n:nat; domain(f`n) = succ(n); \
\ (UN x:f``n. domain(x)) <= n |] \
\ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x))=x";
-by (resolve_tac [ballI] 1);
+by (rtac ballI 1);
by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1);
-by (dresolve_tac [f_n_type] 1 THEN REPEAT (ares_tac [refl] 1));
-by (eresolve_tac [consE] 1);
+by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1));
+by (etac consE 1);
by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (dtac bspec 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1);
val all_in_image_restrict_eq = result();
@@ -396,9 +396,9 @@
\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \
\ & (UN f:fst(z). domain(f)) = b \
\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}";
-by (resolve_tac [oallI] 1);
-by (dresolve_tac [ltD] 1);
-by (eresolve_tac [nat_induct] 1);
+by (rtac oallI 1);
+by (dtac ltD 1);
+by (etac nat_induct 1);
by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1);
by (fast_tac (FOL_cs addss
(ZF_ss addsimps [image_0, singleton_fun RS domain_of_fun,
@@ -408,29 +408,29 @@
by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1));
by (fast_tac (FOL_cs addSEs [trans, subst_context]
addSIs [UN_image_succ_eq_succ] addss AC_ss) 1);
-by (eresolve_tac [conjE] 1);
-by (eresolve_tac [notE] 1);
+by (etac conjE 1);
+by (etac notE 1);
by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1);
-by (eresolve_tac [conjE] 1);
-by (dresolve_tac [apply_UN_type] 1 THEN REPEAT (assume_tac 1));
-by (eresolve_tac [domainE] 1);
-by (eresolve_tac [domainE] 1);
+by (etac conjE 1);
+by (dtac apply_UN_type 1 THEN REPEAT (assume_tac 1));
+by (etac domainE 1);
+by (etac domainE 1);
by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1));
by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1);
by (fast_tac (FOL_cs
addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ,
subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1);
-by (resolve_tac [UN_I] 1);
-by (eresolve_tac [nat_succI] 1);
-by (resolve_tac [CollectI] 1);
+by (rtac UN_I 1);
+by (etac nat_succI 1);
+by (rtac CollectI 1);
by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 1
THEN REPEAT (assume_tac 1));
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [succE] 1);
+by (rtac ballI 1);
+by (etac succE 1);
by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1);
by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1
THEN REPEAT (assume_tac 1));
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (dtac bspec 1 THEN (assume_tac 1));
by (asm_full_simp_tac (AC_ss
addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1);
val simplify_recursion = result();
@@ -444,11 +444,11 @@
\ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \
\ |] ==> f`n : succ(n) -> domain(R) \
\ & (ALL i:n. <f`n`i, f`n`succ(i)>:R)";
-by (dresolve_tac [ospec] 1);
+by (dtac ospec 1);
by (eresolve_tac [Ord_nat RSN (2, ltI)] 1);
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
by (asm_full_simp_tac AC_ss 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs
addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1);
by (fast_tac (FOL_cs
@@ -468,8 +468,8 @@
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
THEN (assume_tac 1));
by (asm_full_simp_tac AC_ss 1);
-by (REPEAT (eresolve_tac [conjE] 1));
-by (eresolve_tac [ballE] 1);
+by (REPEAT (etac conjE 1));
+by (etac ballE 1);
by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1);
by (fast_tac (AC_cs addSEs [ssubst]) 1);
by (asm_full_simp_tac (AC_ss
@@ -481,14 +481,14 @@
by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1));
by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1
THEN REPEAT (assume_tac 1));
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (dresolve_tac [refl RSN (2, simplify_recursion)] 1
THEN REPEAT (assume_tac 1));
by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1);
-by (resolve_tac [lam_type] 2);
+by (rtac lam_type 2);
by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2
THEN REPEAT (assume_tac 2));
-by (resolve_tac [ballI] 1);
+by (rtac ballI 1);
by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1
THEN REPEAT (assume_tac 1));
by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1));
@@ -522,19 +522,19 @@
goalw thy [DC_def, WO3_def]
"!!Z. ALL K. Card(K) --> DC(K) ==> WO3";
-by (resolve_tac [allI] 1);
+by (rtac allI 1);
by (excluded_middle_tac "A lesspoll Hartog(A)" 1);
by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll]
addSIs [Ord_Hartog, leI RS le_imp_subset]) 2);
by (REPEAT (eresolve_tac [allE, impE] 1));
-by (resolve_tac [Card_Hartog] 1);
+by (rtac Card_Hartog 1);
by (eres_inst_tac [("x","A")] allE 1);
by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \
\ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1);
by (asm_full_simp_tac AC_ss 1);
-by (eresolve_tac [impE] 1);
+by (etac impE 1);
by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1);
-by (eresolve_tac [bexE] 1);
+by (etac bexE 1);
by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2))
RS (HartogI RS notE)] 1);
by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1));
@@ -551,10 +551,10 @@
goal thy
"!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
-by (resolve_tac [images_eq] 1);
+by (rtac images_eq 1);
by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD]
addSIs [lam_type]) 2));
-by (resolve_tac [ballI] 1);
+by (rtac ballI 1);
by (dresolve_tac [OrdmemD RS subsetD] 1
THEN REPEAT (assume_tac 1));
by (asm_full_simp_tac AC_ss 1);
@@ -582,13 +582,13 @@
by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac);
by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1
THEN REPEAT (assume_tac 1));
-by (resolve_tac [impI] 1);
+by (rtac impI 1);
by (resolve_tac [ff_def RS def_transrec RS ssubst] 1);
-by (eresolve_tac [the_first_in] 1);
+by (etac the_first_in 1);
by (fast_tac AC_cs 1);
by (asm_full_simp_tac (AC_ss
addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1);
-by (eresolve_tac [lemma_] 1 THEN (assume_tac 1));
+by (etac lemma_ 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [RepFunE, impE, notE]
addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1);
by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll]
@@ -600,7 +600,7 @@
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1);
-by (resolve_tac [lam_type] 2);
+by (rtac lam_type 2);
by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2));
by (asm_full_simp_tac (AC_ss
addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1);
--- a/src/ZF/AC/DC_lemmas.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/DC_lemmas.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/DC_lemmas.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
More general lemmas used in the proofs concerning DC
@@ -15,11 +15,11 @@
val RepFun_lepoll = result();
goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat";
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1);
-by (resolve_tac [notI] 1);
-by (eresolve_tac [eqpollE] 1);
-by (resolve_tac [succ_lepoll_natE] 1 THEN (assume_tac 2));
+by (rtac notI 1);
+by (etac eqpollE 1);
+by (rtac succ_lepoll_natE 1 THEN (assume_tac 2));
by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS
subset_imp_lepoll) RS lepoll_trans] 1
THEN (assume_tac 1));
@@ -44,8 +44,8 @@
val [major, minor] = goal thy
"[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \
\ |] ==> range(R) <= domain(R)";
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [rangeE] 1);
+by (rtac subsetI 1);
+by (etac rangeE 1);
by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1);
by (fast_tac AC_cs 1);
val range_subset_domain = result();
@@ -64,11 +64,11 @@
goal thy "!!g. g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)";
by (resolve_tac [Pi_iff_old RS iffD2] 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs addSIs [cons_subset, succI1]
addEs [fun_is_rel RS subset_trans RS subsetD, succI2]) 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [succE] 1);
+by (rtac ballI 1);
+by (etac succE 1);
by (fast_tac (AC_cs addDs [domain_of_fun, domainI] addSEs [mem_irrefl]) 1);
by (fast_tac (AC_cs addDs [fun_unique_Pair] addSEs [mem_irrefl]) 1);
val cons_fun_type = result();
@@ -103,10 +103,10 @@
val domain_cons_eq_succ = result();
goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(<n,x>, g), n)=g";
-by (resolve_tac [fun_extension] 1);
-by (resolve_tac [lam_type] 1);
+by (rtac fun_extension 1);
+by (rtac lam_type 1);
by (eresolve_tac [cons_fun_type RS apply_type] 1);
-by (eresolve_tac [succI2] 1);
+by (etac succI2 1);
by (assume_tac 1);
by (asm_full_simp_tac (AC_ss addsimps [cons_val_k]) 1);
val restrict_cons_eq = result();
@@ -120,13 +120,13 @@
goalw thy [restrict_def]
"!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
-by (eresolve_tac [subst] 1);
+by (etac subst 1);
by (asm_full_simp_tac AC_ss 1);
val restrict_eq_imp_val_eq = result();
goal thy "!!a. succ(a) = succ(b) ==> a = b";
-by (eresolve_tac [equalityE] 1);
-by (resolve_tac [equalityI] 1);
+by (etac equalityE 1);
+by (rtac equalityI 1);
by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1);
by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1);
val succ_eqD = result();
--- a/src/ZF/AC/HH.ML Fri Jul 28 11:48:55 1995 +0200
+++ b/src/ZF/AC/HH.ML Fri Jul 28 12:01:12 1995 +0200
@@ -1,6 +1,6 @@
(* Title: ZF/AC/HH.ML
ID: $Id$
- Author: Krzysztof Gr`abczewski
+ Author: Krzysztof Grabczewski
Some properties of the recursive definition of HH used in the proofs of
AC17 ==> AC1
@@ -33,7 +33,7 @@
val subset_imp_Diff_eq = result();
goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
-by (eresolve_tac [ltE] 1);
+by (etac ltE 1);
by (dres_inst_tac [("x","c")] Ord_linear 1);
by (fast_tac (AC_cs addEs [Ord_in_Ord]) 1);
by (fast_tac (AC_cs addSIs [ltI] addIs [Ord_in_Ord]) 1);
@@ -49,26 +49,26 @@
\ ==> HH(f,x,a) = HH(f,x,a1)";
by (resolve_tac [HH_def_satisfies_eq RS
(HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1);
-by (eresolve_tac [subst_context] 1);
+by (etac subst_context 1);
val HH_eq = result();
goal thy "!!a. [| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}";
by (res_inst_tac [("P","b<a")] impE 1 THEN REPEAT (assume_tac 2));
by (eresolve_tac [lt_Ord2 RS trans_induct] 1);
-by (resolve_tac [impI] 1);
+by (rtac impI 1);
by (resolve_tac [HH_eq RS trans] 1 THEN (assume_tac 2));
by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1
THEN (assume_tac 1));
by (res_inst_tac [("t","%z. z-?X")] subst_context 1);
-by (resolve_tac [Diff_UN_eq_self] 1);
-by (dresolve_tac [Ord_DiffE] 1 THEN (assume_tac 1));
+by (rtac Diff_UN_eq_self 1);
+by (dtac Ord_DiffE 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addEs [ltE]) 1);
val HH_is_x_gt_too = result();
goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
-by (dresolve_tac [HH_is_x_gt_too] 1 THEN (assume_tac 1));
-by (dresolve_tac [subst] 1 THEN (assume_tac 1));
+by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1));
+by (dtac subst 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
val HH_subset_x_lt_too = result();
@@ -85,7 +85,7 @@
goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P";
by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1));
by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1);
-by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (dtac subst_elem 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSIs [singleton_iff RS iffD2, equals0I]) 1);
val HH_eq_arg_lt = result();
@@ -94,7 +94,7 @@
by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac);
by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2
THEN REPEAT (assume_tac 2));
-by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (dtac subst_elem 1 THEN (assume_tac 1));
by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1);
val HH_eq_imp_arg_eq = result();
@@ -118,7 +118,7 @@
goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
-by (resolve_tac [less_LeastE] 1);
+by (rtac less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 2);
by (assume_tac 1);
val less_Least_subset_x = result();
@@ -152,15 +152,15 @@
\ ALL a:A. EX z:x. F(a) = {z} |] \
\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})";
by (asm_full_simp_tac (AC_ss addsimps [Diff_eq_0_iff]) 1);
-by (resolve_tac [conjI] 1);
+by (rtac conjI 1);
by (fast_tac (AC_cs addSIs [lam_type] addSEs [RepFun_eqI]) 1);
-by (resolve_tac [ballI] 1);
-by (eresolve_tac [RepFunE] 1);
-by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
-by (eresolve_tac [UN_E] 1);
-by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
-by (eresolve_tac [bexE] 1);
-by (resolve_tac [bexI] 1 THEN (assume_tac 2));
+by (rtac ballI 1);
+by (etac RepFunE 1);
+by (dtac subsetD 1 THEN (assume_tac 1));
+by (etac UN_E 1);
+by (dtac bspec 1 THEN (assume_tac 1));
+by (etac bexE 1);
+by (rtac bexI 1 THEN (assume_tac 2));
by (forward_tac [elem_of_sing_eq] 1 THEN (assume_tac 1));
by (fast_tac AC_cs 1);
val lam_surj_sing = result();
@@ -203,9 +203,9 @@
goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \
\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
-by (dresolve_tac [less_Least_subset_x] 1);
+by (dtac less_Least_subset_x 1);
by (forward_tac [HH_subset_imp_eq] 1);
-by (dresolve_tac [apply_type] 1);
+by (dtac apply_type 1);
by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
by (fast_tac (AC_cs addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
by (fast_tac (AC_cs addSEs [RepFunE] addEs [ssubst]) 1);