src/ZF/AC/AC16_WO4.ML

 (*  Title: 	ZF/AC/AC16_WO4.ML
     ID:         $Id$
-    Author: 	Krzysztof Gr`abczewski
+    Author: 	Krzysztof Grabczewski
 
   The proof of AC16(n, k) ==> WO4(n-k)
 *)
 
 open AC16_WO4;

 (* ********************************************************************** *)
 
 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);
 by (rewrite_goals_tac [bij_def, surj_def]);
 by (fast_tac (AC_cs addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun,

 val [prem] = goalw thy [s_u_def]
 	"(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False)  \
 \	==> 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();
 
 (* ********************************************************************** *)
 (* There is a k-2 element subset of y					  *)

 val ordertype_eqpoll =
 	ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2));
 
 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]
 		addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll
 			RS lepoll_infinite]) 1);

 goal thy
 	"!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}.  \
 \	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();
 
 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
 	(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1);
 val set_eq_cons = result();

 \	ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y;  \
 \	k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat   \
 \	|] ==> (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();
 
 goal thy "!!a. [| cons(x,a) = cons(y,a); x~: a |] ==> x = y ";
 by (fast_tac (AC_cs addSEs [equalityE]) 1);

 	THEN REPEAT (assume_tac 1));
 by (res_inst_tac [("f3","lam b:y-a.  \
 \	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
 	THEN REPEAT (assume_tac 1));
 val y_lepoll_subset_s_u = result();

 by (REPEAT (resolve_tac [allI,impI] 1));
 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1);
 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));
 by (fast_tac (AC_cs addSIs [equalityI]) 1);
 val eqpoll_sum_imp_Diff_lepoll_lemma = result();

 by (REPEAT (resolve_tac [allI,impI] 1));
 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1);
 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);
 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2));
 by (fast_tac (AC_cs addSIs [equalityI]) 1);

 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v};  \
 \	l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)};  \
 \	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]
 	addDs [s_u_subset RS subsetD]
 	addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in]

 \		lepoll {v:Pow(x). v eqpoll m}";
 by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}.  \
 \	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 (fast_tac AC_cs 1);
-by (resolve_tac [w_Int_eqpoll_m] 1 THEN REPEAT (assume_tac 1));
+by (rtac CollectI 1);
+by (rtac lam_type 1);
+by (rtac CollectI 1);
+by (fast_tac AC_cs 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();
 
 goal thy

 \	EX! w. w:t_n & z <= w; \
 \	well_ord(y,R); ~Finite(y); u:x; x Int y = 0;  \
 \	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);
 val exists_proper_in_s_u = result();
 

 (* well_ord_subsets_lepoll_n						  *)
 (* ********************************************************************** *)
 
 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);
 val well_ord_subsets_lepoll_n = result();
 

 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1));
 by (eres_inst_tac [("x","xa")] ballE 1);
 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);
 val unique_superset_in_MM = result();
 

 \	well_ord(y,R); ~Finite(y); u:x; x Int y = 0;  \
 \	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 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));
 by (REPEAT (fast_tac (AC_cs addEs [equals0D] addSEs [Int_in_LL]) 1));
 val exists_in_LL = result();

 \	t_n <= {v:Pow(x Un y). v eqpoll n};  \
 \	v : LL(t_n, k, y) |]  \
 \	==> 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();
 
 goal thy  
 	"!!x. [| well_ord(LL(t_n, succ(k), y), S);  \

 \	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  \
 \	|] ==> (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
 	THEN REPEAT (assume_tac 1));
 val OUN_eq_x = result();

 \	t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)};  \
 \	well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |]  \
 \	==> 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,
 	in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)),
 	ordermap_bij RS bij_converse_bij RS bij_is_fun RS apply_type]) 1));

 (* The main theorem AC16(n, k) ==> WO4(n-k)				  *)
 (* ********************************************************************** *)
 
 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);
 by (forward_tac [infinite_Un] 1 THEN (mp_tac 1));
 by (REPEAT (eresolve_tac [exE, conjE] 1));