src/ZF/AC/AC7_AC9.ML

--- 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";