--- a/src/ZF/Cardinal_AC.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/Cardinal_AC.ML Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/Cardinal_AC.ML
+(* Title: ZF/Cardinal_AC.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
Cardinal arithmetic WITH the Axiom of Choice
@@ -14,7 +14,7 @@
goal Cardinal_AC.thy "|A| eqpoll A";
by (resolve_tac [AC_well_ord RS exE] 1);
-by (eresolve_tac [well_ord_cardinal_eqpoll] 1);
+by (etac well_ord_cardinal_eqpoll 1);
qed "cardinal_eqpoll";
val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
@@ -22,13 +22,13 @@
goal Cardinal_AC.thy "!!X Y. |X| = |Y| ==> X eqpoll Y";
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [well_ord_cardinal_eqE] 1);
+by (rtac well_ord_cardinal_eqE 1);
by (REPEAT_SOME assume_tac);
qed "cardinal_eqE";
goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
by (resolve_tac [AC_well_ord RS exE] 1);
-by (eresolve_tac [well_ord_lepoll_imp_Card_le] 1);
+by (etac well_ord_lepoll_imp_Card_le 1);
by (assume_tac 1);
qed "lepoll_imp_Card_le";
@@ -36,7 +36,7 @@
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [well_ord_cadd_assoc] 1);
+by (rtac well_ord_cadd_assoc 1);
by (REPEAT_SOME assume_tac);
qed "cadd_assoc";
@@ -44,7 +44,7 @@
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [well_ord_cmult_assoc] 1);
+by (rtac well_ord_cmult_assoc 1);
by (REPEAT_SOME assume_tac);
qed "cmult_assoc";
@@ -52,13 +52,13 @@
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
by (resolve_tac [AC_well_ord RS exE] 1);
-by (resolve_tac [well_ord_cadd_cmult_distrib] 1);
+by (rtac well_ord_cadd_cmult_distrib 1);
by (REPEAT_SOME assume_tac);
qed "cadd_cmult_distrib";
goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
by (resolve_tac [AC_well_ord RS exE] 1);
-by (eresolve_tac [well_ord_InfCard_square_eq] 1);
+by (etac well_ord_InfCard_square_eq 1);
by (assume_tac 1);
qed "InfCard_square_eq";
@@ -67,7 +67,7 @@
goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B";
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS
- lepoll_trans] 1);
+ lepoll_trans] 1);
by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1);
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
qed "Card_le_imp_lepoll";
@@ -82,46 +82,46 @@
by (etac CollectE 1);
by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);
-by (resolve_tac [exI] 1);
+by (rtac exI 1);
by (rtac f_imp_injective 1);
-by (resolve_tac [Pi_type] 1 THEN assume_tac 1);
+by (rtac Pi_type 1 THEN assume_tac 1);
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1);
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
qed "surj_implies_inj";
(*Kunen's Lemma 10.20*)
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|";
-by (resolve_tac [lepoll_imp_Card_le] 1);
+by (rtac lepoll_imp_Card_le 1);
by (eresolve_tac [surj_implies_inj RS exE] 1);
by (rewtac lepoll_def);
-by (eresolve_tac [exI] 1);
+by (etac exI 1);
qed "surj_implies_cardinal_le";
(*Kunen's Lemma 10.21*)
goal Cardinal_AC.thy
"!!K. [| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K";
by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1);
-by (resolve_tac [lepoll_trans] 1);
+by (rtac lepoll_trans 1);
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);
-by (rewrite_goals_tac [lepoll_def]);
+by (rewtac lepoll_def);
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
by (etac (AC_ball_Pi RS exE) 1);
-by (resolve_tac [exI] 1);
+by (rtac exI 1);
(*Lemma needed in both subgoals, for a fixed z*)
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 (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI]
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);
+ ("d", "%<i,j>. converse(f`i) ` j")]
+ lam_injective 1);
(*Instantiate the lemma proved above*)
by (ALLGOALS ball_tac);
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]
addDs [apply_type]) 1);
-by (dresolve_tac [apply_type] 1);
-by (eresolve_tac [conjunct2] 1);
+by (dtac apply_type 1);
+by (etac conjunct2 1);
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
qed "cardinal_UN_le";
@@ -131,7 +131,7 @@
\ |UN i:K. X(i)| < csucc(K)";
by (asm_full_simp_tac
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le,
- InfCard_is_Card, Card_cardinal]) 1);
+ InfCard_is_Card, Card_cardinal]) 1);
qed "cardinal_UN_lt_csucc";
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i),
@@ -159,9 +159,9 @@
(*Work backwards along the injection from W into K, given that W~=0.*)
goal Perm.thy
- "!!A. [| f: inj(A,B); a:A |] ==> \
+ "!!A. [| f: inj(A,B); a:A |] ==> \
\ (UN x:A. C(x)) <= (UN y:B. C(if(y: range(f), converse(f)`y, a)))";
-by (resolve_tac [UN_least] 1);
+by (rtac UN_least 1);
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
by (asm_simp_tac
@@ -174,17 +174,17 @@
"!!K. [| InfCard(K); |W| le K; ALL w:W. j(w) < csucc(K) |] ==> \
\ (UN w:W. j(w)) < csucc(K)";
by (excluded_middle_tac "W=0" 1);
-by (asm_simp_tac (*solve the easy 0 case*)
+by (asm_simp_tac (*solve the easy 0 case*)
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc,
- Card_is_Ord, Ord_0_lt_csucc]) 2);
+ Card_is_Ord, Ord_0_lt_csucc]) 2);
by (asm_full_simp_tac
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
by (safe_tac eq_cs);
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc]
- MRS lt_subset_trans] 1);
+ MRS lt_subset_trans] 1);
by (REPEAT (assume_tac 1));
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2);
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type]
- setloop split_tac [expand_if]) 1);
+ setloop split_tac [expand_if]) 1);
qed "le_UN_Ord_lt_csucc";