--- a/src/ZF/AC/AC0_AC1.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC0_AC1.ML Tue Jul 25 17:31:53 1995 +0200
@@ -14,10 +14,10 @@
by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1);
val lemma1 = result();
-val prems = goalw thy AC_defs "!!Z. AC0 ==> AC1";
+goalw thy AC_defs "!!Z. AC0 ==> AC1";
by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1);
-result();
+qed "AC0_AC1";
-val prems = goalw thy AC_defs "!!Z. AC1 ==> AC0";
+goalw thy AC_defs "!!Z. AC1 ==> AC0";
by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
-result();
+qed "AC1_AC0";
--- a/src/ZF/AC/AC10_AC15.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC10_AC15.ML Tue Jul 25 17:31:53 1995 +0200
@@ -13,10 +13,10 @@
or
-AC1 ==> AC13(1); AC13(m) ==> AC13(n); AC13(n) ==> AC14 ==> AC15
+AC1 ==> AC13(1); AC13(m) ==> AC13(n) ==> AC14 ==> AC15 (m le n)
-So we don't have to prove all impllications of both cases.
-Moreover we don't need to prove that AC13(1) ==> AC1, AC11 ==> AC14 as
+So we don't have to prove all implications of both cases.
+Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as
Rubin & Rubin do.
*)
@@ -27,22 +27,6 @@
(* - ex_fun_AC13_AC15 *)
(* ********************************************************************** *)
-(* Change to ZF/Cardinal.ML *)
-
-goalw Cardinal.thy [succ_def]
- "!!A. succ(n) lepoll A ==> n lepoll A - {a}";
-by (rtac cons_lepoll_consD 1);
-by (rtac mem_not_refl 2);
-by (fast_tac AC_cs 2);
-by (fast_tac (AC_cs addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
-val lepoll_diff_sing = result();
-(* qed "lepoll_diff_sing"; *)
-
-goalw thy [Finite_def] "~Finite(nat)";
-by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll]
- addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
-val nat_not_Finite = result();
-
goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B";
by (eresolve_tac [not_emptyE] 1);
by (res_inst_tac [("x","lam z:B. <x,z>")] exI 1);
@@ -56,7 +40,7 @@
by (resolve_tac [notI] 1);
by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1);
by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1
- THEN (atac 2));
+ THEN (assume_tac 2));
by (fast_tac AC_cs 1);
val cons_times_nat_not_Finite = result();
@@ -66,7 +50,7 @@
goalw thy [pairwise_disjoint_def]
"!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C";
-by (dresolve_tac [IntI] 1 THEN (atac 1));
+by (dresolve_tac [IntI] 1 THEN (assume_tac 1));
by (dres_inst_tac [("A","B Int C")] not_emptyI 1);
by (fast_tac ZF_cs 1);
val lemma2 = result();
@@ -85,7 +69,7 @@
by (resolve_tac [ex1I] 1);
by (fast_tac ZF_cs 1);
by (REPEAT (eresolve_tac [conjE] 1));
-by (resolve_tac [lemma2] 1 THEN (REPEAT (atac 1)));
+by (resolve_tac [lemma2] 1 THEN (REPEAT (assume_tac 1)));
val lemma3 = result();
goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i";
@@ -94,7 +78,7 @@
[("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1);
by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1);
by (eresolve_tac [RepFunE] 1);
-by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
+by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addIs [LeastI2]
addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
by (eresolve_tac [RepFunE] 1);
@@ -112,7 +96,7 @@
by (asm_simp_tac AC_ss 1);
by (resolve_tac [conjI] 1);
by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1]
- addDs [lepoll_diff_sing]
+ addDs [lepoll_Diff_sing]
addEs [lepoll_trans RS succ_lepoll_natE, ssubst]
addSIs [notI, lepoll_refl, nat_0I]) 1);
by (resolve_tac [conjI] 1);
@@ -126,10 +110,8 @@
\ sets_of_size_between(f`B, 2, succ(n)) & \
\ Union(f`B)=B; n:nat |] \
\ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n";
-by (etac exE 1);
-by (dtac lemma3 1);
-by (fast_tac (empty_cs addSDs [bspec, theI]
- addSEs [conjE]
+by (fast_tac (empty_cs addSDs [lemma3, bspec, theI]
+ addSEs [exE, conjE]
addSIs [exI, ballI, lemma5]) 1);
val ex_fun_AC13_AC15 = result();
@@ -144,7 +126,7 @@
goalw thy AC_defs "!!Z. [| n:nat; 1 le n; AC10(n) |] ==> AC11";
by (resolve_tac [bexI] 1 THEN (assume_tac 2));
by (fast_tac ZF_cs 1);
-result();
+qed "AC10_AC11";
(* ********************************************************************** *)
(* AC11 ==> AC12 *)
@@ -152,7 +134,7 @@
goalw thy AC_defs "!! Z. AC11 ==> AC12";
by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1);
-result();
+qed "AC11_AC12";
(* ********************************************************************** *)
(* AC12 ==> AC15 *)
@@ -164,7 +146,7 @@
by (eresolve_tac [impE] 1);
by (eresolve_tac [cons_times_nat_not_Finite] 1);
by (fast_tac (ZF_cs addSIs [ex_fun_AC13_AC15]) 1);
-result();
+qed "AC12_AC15";
(* ********************************************************************** *)
(* AC15 ==> WO6 *)
@@ -209,16 +191,16 @@
[singleton_eqpoll_1 RS eqpoll_imp_lepoll,
singletonI RS not_emptyI]) 1);
by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1);
-result();
+qed "AC1_AC13";
(* ********************************************************************** *)
(* AC13(m) ==> AC13(n) for m <= n *)
(* ********************************************************************** *)
goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)";
-by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (atac 1));
+by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (assume_tac 1));
by (fast_tac (ZF_cs addSEs [lepoll_trans]) 1);
-result();
+qed "AC13_mono";
(* ********************************************************************** *)
(* The proofs necessary for both cases *)
@@ -230,7 +212,7 @@
goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC13(n) |] ==> AC14";
by (fast_tac (FOL_cs addIs [bexI]) 1);
-result();
+qed "AC13_AC14";
(* ********************************************************************** *)
(* AC14 ==> AC15 *)
@@ -238,7 +220,7 @@
goalw thy AC_defs "!!Z. AC14 ==> AC15";
by (fast_tac ZF_cs 1);
-result();
+qed "AC14_AC15";
(* ********************************************************************** *)
(* The redundant proofs; however cited by Rubin & Rubin *)
@@ -255,16 +237,16 @@
goal thy "!!f. ALL B:A. f(B)~=0 & f(B)<=B & f(B) lepoll 1 \
\ ==> (lam x:A. THE y. f(x)={y}) : (PROD X:A. X)";
by (resolve_tac [lam_type] 1);
-by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
by (REPEAT (eresolve_tac [conjE] 1));
-by (eresolve_tac [lemma_aux RS exE] 1 THEN (atac 1));
+by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1));
by (asm_full_simp_tac (AC_ss addsimps [the_element]) 1);
by (fast_tac (AC_cs addEs [ssubst]) 1);
val lemma = result();
goalw thy AC_defs "!!Z. AC13(1) ==> AC1";
by (fast_tac (AC_cs addSEs [lemma]) 1);
-result();
+qed "AC13(1)_AC1";
(* ********************************************************************** *)
(* AC11 ==> AC14 *)
@@ -272,4 +254,4 @@
goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14";
by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1);
-result();
+qed "AC11_AC14";
--- a/src/ZF/AC/AC15_WO6.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC15_WO6.ML Tue Jul 25 17:31:53 1995 +0200
@@ -43,4 +43,4 @@
by (asm_full_simp_tac AC_ss 1);
by (fast_tac (AC_cs addSIs [Ord_Least, lam_type RS domain_of_fun]
addSEs [less_Least_subset_x, lemma1, lemma2]) 1);
-result();
\ No newline at end of file
+qed "AC15_WO6";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC16_WO4.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,697 @@
+
+open AC16_WO4;
+
+(* ********************************************************************** *)
+(* The case of finite set *)
+(* ********************************************************************** *)
+
+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 (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1);
+by (eresolve_tac [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,
+ equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
+ nat_1_lepoll_iff RS iffD2]
+ addSEs [singletonE, apply_type, ltE]) 1);
+val lemma1 = result();
+
+(* ********************************************************************** *)
+(* The case of infinite set *)
+(* ********************************************************************** *)
+
+goal thy "!!x. well_ord(x,r) ==> well_ord({{y,z}. y:x},?s(x,z))";
+by (eresolve_tac [paired_bij RS bij_is_inj RS well_ord_rvimage] 1);
+val well_ord_paired = uresult();
+
+goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C";
+by (fast_tac (FOL_cs addEs [notE, lepoll_trans]) 1);
+val lepoll_trans1 = result();
+
+goalw thy [lepoll_def]
+ "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)";
+by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1);
+val well_ord_lepoll = result();
+
+goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \
+\ |] ==> EX T. well_ord(X Un Y, T)";
+by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1);
+by (assume_tac 1);
+val well_ord_Un = result();
+
+(* ********************************************************************** *)
+(* There exists a well ordered set y such that ... *)
+(* ********************************************************************** *)
+
+goal thy "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)";
+by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1);
+by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS
+ well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1);
+by (fast_tac (AC_cs addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired,
+ equals0I, HartogI RSN (2, lepoll_trans1),
+ subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS
+ eqpoll_imp_lepoll RSN (2, lepoll_trans))]
+ addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym]
+ addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite,
+ paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
+ RS lepoll_Finite]) 1);
+val lemma2 = result();
+
+val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)";
+by (fast_tac (AC_cs
+ addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1);
+val infinite_Un = result();
+
+(* ********************************************************************** *)
+(* There is a v : s_u such that k lepoll x Int y (in our case succ(k)) *)
+(* The idea of the proof is the following : *)
+(* Suppose not, i.e. every element of s_u has exactly k-1 elements of y *)
+(* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *)
+(* We have obtained this result in two steps : *)
+(* 1. y is less than or equipollent to {v:s_u. a <= v} *)
+(* where a is certain k-2 element subset of y *)
+(* 2. {v:s_u. a <= v} is less than or equipollent *)
+(* to {v:Pow(x). v eqpoll n-k} *)
+(* ********************************************************************** *)
+
+goal thy "!!A. [| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \
+\ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
+by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
+by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]
+ addIs [expand_if RS iffD2]) 1);
+by (REPEAT (split_tac [expand_if] 1));
+by (fast_tac (AC_cs addSEs [left_inverse]) 1);
+val succ_not_lepoll_lemma = result();
+
+goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def]
+ "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B";
+by (fast_tac (AC_cs addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1);
+val succ_not_lepoll_imp_eqpoll = result();
+
+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 (fast_tac (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1);
+val suppose_not = result();
+
+(* ********************************************************************** *)
+(* There is a k-2 element subset of y *)
+(* ********************************************************************** *)
+
+goalw thy [lepoll_def, eqpoll_def]
+ "!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y";
+by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
+ addSIs [subset_refl]
+ addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1);
+val nat_lepoll_imp_ex_eqpoll_n = result();
+
+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 (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);
+val ex_subset_eqpoll_n = result();
+
+goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat";
+by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll,
+ eqpoll_sym RS eqpoll_imp_lepoll]
+ addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI
+ RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1);
+val n_lesspoll_nat = result();
+
+goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \
+\ ==> y - a eqpoll y";
+by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll]
+ addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans,
+ Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord
+ RS le_imp_lepoll]
+ addSEs [well_ord_cardinal_eqpoll,
+ well_ord_cardinal_eqpoll RS eqpoll_sym,
+ eqpoll_sym RS eqpoll_imp_lepoll,
+ n_lesspoll_nat RS lesspoll_lepoll_lesspoll,
+ well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
+ RS lepoll_infinite]) 1);
+val Diff_Finite_eqpoll = result();
+
+goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)";
+by (fast_tac AC_cs 1);
+val cons_cons_subset = result();
+
+goal thy "!!x. [| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \
+\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
+by (fast_tac (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D]) 1);
+val cons_cons_eqpoll = result();
+
+goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n";
+by (fast_tac AC_cs 1);
+val s_u_subset = result();
+
+goalw thy [s_u_def, succ_def]
+ "!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \
+\ |] ==> w: s_u(u, t_n, succ(k), y)";
+by (fast_tac (AC_cs addDs [eqpoll_imp_lepoll RS cons_lepoll_cong]
+ addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
+val s_uI = result();
+
+goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v";
+by (fast_tac AC_cs 1);
+val in_s_u_imp_u_in = result();
+
+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 (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset,
+ eqpoll_sym RS cons_cons_eqpoll]) 2);
+by (eresolve_tac [ex1E] 1);
+by (res_inst_tac [("a","w")] ex1I 1);
+by (resolve_tac [conjI] 1);
+by (resolve_tac [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 (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 (fast_tac AC_cs 2);
+by (resolve_tac [Diff_eq_0_iff RS iffD1] 1);
+by (resolve_tac [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 (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();
+
+goal thy
+ "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
+\ EX! w. w:t_n & z <= w; \
+\ 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 (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);
+val cons_eqE = result();
+
+goal thy "!!A. A = B ==> A Int C = B Int C";
+by (asm_simp_tac AC_ss 1);
+val eq_imp_Int_eq = result();
+
+goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d";
+by (asm_full_simp_tac AC_ss 1);
+val msubst = result();
+
+(* ********************************************************************** *)
+(* 1. y is less than or equipollent to {v:s_u. a <= v} *)
+(* where a is certain k-2 element subset of y *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \
+\ EX! w. w:t_n & z <= w; \
+\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \
+\ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \
+\ k:nat; u:x; x Int y = 0 |] \
+\ ==> y lepoll {v:s_u(u, t_n, succ(k), y). a <= v}";
+by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS
+ eqpoll_imp_lepoll RS lepoll_trans] 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 (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 (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 (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();
+
+(* ********************************************************************** *)
+(* some arithmetic *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!k. [| k:nat; m:nat |] ==> \
+\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
+by (eres_inst_tac [("n","k")] nat_induct 1);
+by (simp_tac (AC_ss addsimps [add_0]) 1);
+by (fast_tac (AC_cs addIs [eqpoll_imp_lepoll RS
+ (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1);
+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 (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();
+
+goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; \
+\ k:nat; m:nat |] \
+\ ==> A-B lepoll m";
+by (dresolve_tac [add_succ RS ssubst] 1);
+by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac AC_cs 1);
+val eqpoll_sum_imp_Diff_lepoll = result();
+
+(* ********************************************************************** *)
+(* similar properties for eqpoll *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!k. [| k:nat; m:nat |] ==> \
+\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m";
+by (eres_inst_tac [("n","k")] nat_induct 1);
+by (fast_tac (AC_cs addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0]
+ addss (AC_ss addsimps [add_0])) 1);
+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 (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);
+val eqpoll_sum_imp_Diff_eqpoll_lemma = result();
+
+goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; \
+\ k:nat; m:nat |] \
+\ ==> A-B eqpoll m";
+by (dresolve_tac [add_succ RS ssubst] 1);
+by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac AC_cs 1);
+val eqpoll_sum_imp_Diff_eqpoll = result();
+
+(* ********************************************************************** *)
+(* back to the second part *)
+(* ********************************************************************** *)
+
+goal thy "!!w. [| x Int y = 0; w <= x Un y |] \
+\ ==> w Int (x - {u}) = w - cons(u, w Int y)";
+by (fast_tac (AC_cs addSIs [equalityI] addEs [equals0D]) 1);
+val w_Int_eq_w_Diff = result();
+
+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 (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]
+ addSIs [nat_succI, eqpoll_sum_imp_Diff_eqpoll]) 1);
+val w_Int_eqpoll_m = result();
+
+goal thy "!!m. [| 0<m; x eqpoll m; m:nat |] ==> x ~= 0";
+by (fast_tac (empty_cs
+ addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1);
+val eqpoll_m_not_empty = result();
+
+goal thy
+ "!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \
+\ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}";
+by (fast_tac (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1);
+val cons_cons_in = result();
+
+(* ********************************************************************** *)
+(* 2. {v:s_u. a <= v} is less than or equipollent *)
+(* to {v:Pow(x). v eqpoll n-k} *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \
+\ EX! w. w:t_n & z <= w; \
+\ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \
+\ 0<m; m:nat; l:nat; \
+\ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y; \
+\ a <= y; l eqpoll a; x Int y = 0; u : x \
+\ |] ==> {v:s_u(u, t_n, succ(l), y). a <= v} \
+\ 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 (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 (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 (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
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+\ 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 (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 (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();
+
+(* ********************************************************************** *)
+(* LL can be well ordered *)
+(* ********************************************************************** *)
+
+goal thy "{x:Pow(X). x lepoll 0} = {0}";
+by (fast_tac (AC_cs addSDs [lepoll_0_is_0]
+ addSIs [singletonI, lepoll_refl, equalityI]
+ addSEs [singletonE]) 1);
+val subsets_lepoll_0_eq_unit = result();
+
+goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \
+\ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)";
+by (resolve_tac [well_ord_infinite_subsets_eqpoll_X
+ RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1);
+val well_ord_subsets_eqpoll_n = result();
+
+goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} = \
+\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
+by (fast_tac (ZF_cs addSIs [le_refl, leI,
+ le_imp_lepoll, equalityI]
+ addSDs [lepoll_succ_disj]
+ addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
+val subsets_lepoll_succ = result();
+
+goal thy "!!n. n:nat ==> \
+\ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0";
+by (fast_tac (ZF_cs addSEs [eqpoll_sym RS eqpoll_imp_lepoll
+ RS lepoll_trans RS succ_lepoll_natE]
+ addSIs [equals0I]) 1);
+val Int_empty = result();
+
+(* ********************************************************************** *)
+(* unit set is well-ordered by the empty relation *)
+(* ********************************************************************** *)
+
+goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
+ "tot_ord({a},0)";
+by (simp_tac ZF_ss 1);
+val tot_ord_unit = result();
+
+goalw thy [wf_on_def, wf_def] "wf[{a}](0)";
+by (fast_tac (ZF_cs addSIs [equalityI]) 1);
+val wf_on_unit = result();
+
+goalw thy [well_ord_def] "well_ord({a},0)";
+by (simp_tac (ZF_ss addsimps [tot_ord_unit, wf_on_unit]) 1);
+val well_ord_unit = 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 (fast_tac (ZF_cs addSIs [well_ord_unit]
+ addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1);
+by (eresolve_tac [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 (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();
+
+goalw thy [LL_def, MM_def]
+ "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \
+\ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}";
+by (fast_tac (AC_cs addSEs [RepFunE]
+ addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll
+ RSN (2, lepoll_trans))]) 1);
+val LL_subset = result();
+
+goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \
+\ well_ord(y, R); ~Finite(y); n:nat \
+\ |] ==> EX S. well_ord(LL(t_n, k, y), S)";
+by (fast_tac (FOL_cs addIs [exI]
+ addSEs [LL_subset RSN (2, well_ord_subset)]
+ addEs [well_ord_subsets_lepoll_n RS exE]) 1);
+val well_ord_LL = result();
+
+(* ********************************************************************** *)
+(* every element of LL is a contained in exactly one element of MM *)
+(* ********************************************************************** *)
+
+goalw thy [MM_def, LL_def]
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
+\ t_n <= {v:Pow(x Un y). v eqpoll n}; \
+\ v:LL(t_n, k, y) \
+\ |] ==> EX! w. w:MM(t_n, k, y) & v<=w";
+by (step_tac (AC_cs addSEs [RepFunE]) 1);
+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 (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();
+
+(* ********************************************************************** *)
+(* The function GG satisfies the conditions of WO4 *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* The union of appropriate values is the whole x *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+\ 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 w:MM(t_n, succ(k), y). u:w";
+by (eresolve_tac [exists_proper_in_s_u RS bexE] 1
+ THEN REPEAT (assume_tac 1));
+by (rewrite_goals_tac [MM_def, s_u_def]);
+by (fast_tac AC_cs 1);
+val exists_in_MM = result();
+
+goalw thy [LL_def] "!!w. w : MM(t_n, k, y) ==> w Int y : LL(t_n, k, y)";
+by (fast_tac AC_cs 1);
+val Int_in_LL = result();
+
+goalw thy [MM_def] "MM(t_n, k, y) <= t_n";
+by (fast_tac AC_cs 1);
+val MM_subset = result();
+
+goal thy
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \
+\ 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 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 (res_inst_tac [("x","w Int y")] bexI 1);
+by (eresolve_tac [Int_in_LL] 2);
+by (rewrite_goals_tac [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();
+
+goalw thy [LL_def]
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
+\ t_n <= {v:Pow(x Un y). v eqpoll n}; \
+\ v : LL(t_n, k, y) |] \
+\ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y";
+by (fast_tac (AC_cs addSEs [Int_in_LL,
+ unique_superset_in_MM RS the_equality2 RS ssubst]) 1);
+val in_LL_eq_Int = result();
+
+goal thy
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
+\ t_n <= {v:Pow(x Un y). v eqpoll n}; \
+\ v : LL(t_n, k, y) |] \
+\ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y";
+by (fast_tac (AC_cs addSDs [unique_superset_in_MM RS theI RS conjunct1 RS
+ (MM_subset RS subsetD)]) 1);
+val the_in_MM_subset = result();
+
+goalw thy [GG_def]
+ "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \
+\ 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 (fast_tac (AC_cs addEs [ssubst]) 1);
+val GG_subset = result();
+
+goal thy
+ "!!x. [| well_ord(LL(t_n, succ(k), y), S); \
+\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \
+\ well_ord(y,R); ~Finite(y); 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 \
+\ |] ==> (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 (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 (eresolve_tac [exists_in_LL RS bexE] 1 THEN REPEAT (assume_tac 1));
+by (resolve_tac [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();
+
+(* ********************************************************************** *)
+(* Every element of the family is less than or equipollent to n-k (m) *)
+(* ********************************************************************** *)
+
+goalw thy [MM_def]
+ "!!w. [| w : MM(t_n, k, y); t_n <= {v:Pow(x Un y). v eqpoll n} \
+\ |] ==> w eqpoll n";
+by (fast_tac AC_cs 1);
+val in_MM_eqpoll_n = result();
+
+goalw thy [LL_def, MM_def]
+ "!!w. w : LL(t_n, k, y) ==> k lepoll w";
+by (fast_tac AC_cs 1);
+val in_LL_eqpoll_n = result();
+
+goalw thy [GG_def]
+ "!!x. [| \
+\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \
+\ 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 (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 (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));
+val all_in_lepoll_m = result();
+
+(* ********************************************************************** *)
+(* 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 (excluded_middle_tac "Finite(A)" 1);
+by (resolve_tac [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));
+by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1));
+by (fast_tac (AC_cs addSIs [nat_succI, add_type]) 1);
+by (res_inst_tac [("x","ordertype(LL(T, succ(k), y), x)")] exI 1);
+by (res_inst_tac [("x","lam b:ordertype(LL(T, succ(k), y), x). \
+\ (GG(T, succ(k), y)) ` \
+\ (converse(ordermap(LL(T, succ(k), y), x)) ` b)")] exI 1);
+by (simp_tac AC_ss 1);
+by (fast_tac (empty_cs addSIs [conjI, lam_funtype RS domain_of_fun]
+ addSEs [Ord_ordertype, all_in_lepoll_m, OUN_eq_x]) 1);
+qed "AC16_WO4";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC16_WO4.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,29 @@
+(* Title: ZF/AC/AC16_WO4.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+*)
+
+AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
+
+consts
+
+ ww :: "[i, i] => i"
+ s_u :: "[i, i, i, i] => i"
+ MM :: "[i, i, i] => i"
+ LL :: "[i, i, i] => i"
+ GG :: "[i, i, i] => i"
+
+defs
+
+ ww_def "ww(x, k) == {u:Pow(x). u eqpoll k}"
+
+ s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}"
+
+ MM_def "MM(t_n, k, y) == {v:t_n. k lepoll v Int y}"
+
+ LL_def "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}"
+
+ GG_def "GG(t_n, k, y) == lam v:LL(t_n, k, y).
+ (THE w. w:MM(t_n, k, y) & v <= w) - v"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC16_lemmas.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,279 @@
+(* Title: ZF/AC/AC16_lemmas.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Lemmas used in the proofs concerning AC16
+*)
+
+open AC16_lemmas;
+
+goal thy "!!a. a~:A ==> cons(a,A)-{a}=A";
+by (fast_tac (ZF_cs addSIs [equalityI]) 1);
+val cons_Diff_eq = result();
+
+goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
+by (resolve_tac [iffI] 1);
+by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1);
+by (eresolve_tac [exE] 1);
+by (res_inst_tac [("x","lam a:1. x")] exI 1);
+by (fast_tac (ZF_cs addSIs [lam_injective]) 1);
+val nat_1_lepoll_iff = result();
+
+goal thy "X eqpoll 1 <-> (EX x. X={x})";
+by (resolve_tac [iffI] 1);
+by (eresolve_tac [eqpollE] 1);
+by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1);
+by (fast_tac (ZF_cs addSIs [lepoll_1_is_sing]) 1);
+by (fast_tac (ZF_cs addSIs [singleton_eqpoll_1]) 1);
+val eqpoll_1_iff_singleton = result();
+
+goalw thy [succ_def]
+ "!!x. [| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)";
+by (fast_tac (ZF_cs addSEs [cons_eqpoll_cong, mem_irrefl]) 1);
+val cons_eqpoll_succ = result();
+
+goal thy "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}";
+by (resolve_tac [equalityI] 1);
+by (resolve_tac [subsetI] 1);
+by (eresolve_tac [CollectE] 1);
+by (dresolve_tac [eqpoll_1_iff_singleton RS iffD1] 1);
+by (fast_tac (AC_cs addSIs [RepFunI]) 1);
+by (resolve_tac [subsetI] 1);
+by (eresolve_tac [RepFunE] 1);
+by (resolve_tac [CollectI] 1);
+by (fast_tac AC_cs 1);
+by (fast_tac (AC_cs addSIs [singleton_eqpoll_1]) 1);
+val subsets_eqpoll_1_eq = result();
+
+goalw thy [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}";
+by (res_inst_tac [("x","lam x:X. {x}")] exI 1);
+by (resolve_tac [IntI] 1);
+by (rewrite_goals_tac [inj_def, surj_def]);
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSIs [lam_type, RepFunI]
+ addIs [singleton_eq_iff RS iffD1]) 1);
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSIs [lam_type]) 1);
+val eqpoll_RepFun_sing = result();
+
+goal thy "{Y:Pow(X). Y eqpoll 1} eqpoll X";
+by (resolve_tac [subsets_eqpoll_1_eq RS ssubst] 1);
+by (resolve_tac [eqpoll_RepFun_sing RS eqpoll_sym] 1);
+val subsets_eqpoll_1_eqpoll = result();
+
+goal thy "!!x. [| InfCard(x); y:Pow(x); y eqpoll succ(z) |] \
+\ ==> (LEAST i. i:y) : y";
+by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
+ succ_lepoll_imp_not_empty RS not_emptyE] 1);
+by (fast_tac (AC_cs addIs [LeastI]
+ addSDs [InfCard_is_Card RS Card_is_Ord, PowD RS subsetD]
+ addEs [Ord_in_Ord]) 1);
+val InfCard_Least_in = result();
+
+goalw thy [lepoll_def] "!!i. [| InfCard(x); n:nat |] ==> \
+\ {y:Pow(x). y eqpoll succ(succ(n))} lepoll \
+\ x*{y:Pow(x). y eqpoll succ(n)}";
+by (res_inst_tac [("x","lam y:{y:Pow(x). y eqpoll succ(succ(n))}. \
+\ <LEAST i. i:y, y-{LEAST i. i:y}>")] exI 1);
+by (res_inst_tac [("d","%z. cons(fst(z),snd(z))")] lam_injective 1);
+by (resolve_tac [SigmaI] 1);
+by (eresolve_tac [CollectE] 1);
+by (asm_full_simp_tac AC_ss 3);
+by (resolve_tac [equalityI] 3);
+by (fast_tac AC_cs 4);
+by (resolve_tac [subsetI] 3);
+by (eresolve_tac [consE] 3);
+by (fast_tac AC_cs 4);
+by (resolve_tac [CollectI] 2);
+by (fast_tac AC_cs 2);
+by (resolve_tac [PowD RS subsetD] 1 THEN (assume_tac 1));
+by (REPEAT (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]
+ addIs [InfCard_Least_in]) 1));
+val subsets_lepoll_lemma1 = result();
+
+val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
+by (resolve_tac [subsetI] 1);
+by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
+by (fast_tac (AC_cs addSIs [equalityI]) 2);
+by (eresolve_tac [swap] 1);
+by (resolve_tac [ballI] 1);
+by (resolve_tac [Ord_linear_le] 1);
+by (dresolve_tac [le_imp_subset] 3 THEN (assume_tac 3));
+by (fast_tac (AC_cs addDs prems) 1);
+by (fast_tac (AC_cs addDs prems) 1);
+by (fast_tac (AC_cs addSEs [leE,ltE]) 1);
+val set_of_Ord_succ_Union = result();
+
+goal thy "!!i. j<=i ==> i ~: j";
+by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1);
+val subset_not_mem = result();
+
+val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> succ(Union(z)) ~: z";
+by (resolve_tac [set_of_Ord_succ_Union RS subset_not_mem] 1);
+by (eresolve_tac prems 1);
+val succ_Union_not_mem = result();
+
+goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))";
+by (fast_tac (AC_cs addIs [equalityI]) 1);
+val Union_cons_eq_succ_Union = result();
+
+goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j";
+by (fast_tac (AC_cs addSDs [le_imp_subset] addIs [equalityI]
+ addEs [Ord_linear_le]) 1);
+val Un_Ord_disj = result();
+
+goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})";
+by (fast_tac (AC_cs addIs [equalityI]) 1);
+val Union_eq_Un = result();
+
+goal thy "!!n. n:nat ==> \
+\ ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
+by (eresolve_tac [nat_induct] 1);
+by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
+by (REPEAT (resolve_tac [allI, impI] 1));
+by (eresolve_tac [natE] 1);
+by (fast_tac (AC_cs addSDs [eqpoll_1_iff_singleton RS iffD1]
+ addSIs [Union_singleton]) 1);
+by (hyp_subst_tac 1);
+by (REPEAT (eresolve_tac [conjE, not_emptyE] 1));
+by (eres_inst_tac [("x","z-{xb}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (fast_tac (AC_cs addSEs [Diff_sing_eqpoll,
+ Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1);
+by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2));
+by (forward_tac [bspec] 1 THEN (assume_tac 1));
+by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1));
+by (dresolve_tac [Un_Ord_disj] 1 THEN (assume_tac 1));
+by (eresolve_tac [DiffE] 1);
+by (eresolve_tac [disjE] 1);
+by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (resolve_tac [subst_elem] 1 THEN (TRYALL assume_tac));
+val Union_in_lemma = result();
+
+goal thy "!!z. [| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |] \
+\ ==> Union(z) : z";
+by (dresolve_tac [Union_in_lemma] 1);
+by (fast_tac FOL_cs 1);
+val Union_in = result();
+
+goal thy "!!x. [| InfCard(x); z:Pow(x); z eqpoll n; n:nat |] \
+\ ==> succ(Union(z)) : x";
+by (resolve_tac [Limit_has_succ RS ltE] 1 THEN (assume_tac 3));
+by (eresolve_tac [InfCard_is_Limit] 1);
+by (excluded_middle_tac "z=0" 1);
+by (fast_tac (AC_cs addSIs [InfCard_is_Limit RS Limit_has_0]
+ addIs [Union_0 RS ssubst]) 2);
+by (resolve_tac
+ [PowD RS subsetD RS (InfCard_is_Card RS Card_is_Ord RSN (2, ltI))] 1
+ THEN (TRYALL assume_tac));
+by (fast_tac (AC_cs addSIs [Union_in]
+ addSEs [PowD RS subsetD RSN (2,
+ InfCard_is_Card RS Card_is_Ord RS Ord_in_Ord)]) 1);
+val succ_Union_in_x = result();
+
+goalw thy [lepoll_def] "!!X. [| InfCard(x); n:nat |] ==> \
+\ {y:Pow(x). y eqpoll succ(n)} lepoll \
+\ {y:Pow(x). y eqpoll succ(succ(n))}";
+by (res_inst_tac [("x","lam z:{y:Pow(x). y eqpoll succ(n)}. \
+\ cons(succ(Union(z)), z)")] exI 1);
+by (res_inst_tac [("d","%z. z-{Union(z)}")] lam_injective 1);
+by (resolve_tac [Union_cons_eq_succ_Union RS ssubst] 2);
+by (resolve_tac [cons_Diff_eq] 2);
+by (fast_tac (AC_cs addSDs [InfCard_is_Card RS Card_is_Ord]
+ addEs [Ord_in_Ord] addSIs [succ_Union_not_mem]) 2);
+by (resolve_tac [CollectI] 1);
+by (fast_tac (AC_cs addSEs [cons_eqpoll_succ]
+ addSIs [succ_Union_not_mem]
+ addSDs [InfCard_is_Card RS Card_is_Ord]
+ addEs [Ord_in_Ord]) 2);
+by (fast_tac (AC_cs addSIs [succ_Union_in_x, nat_succI]) 1);
+val succ_lepoll_succ_succ = result();
+
+goal thy "!!X. [| InfCard(X); n:nat |] \
+\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+by (eresolve_tac [nat_induct] 1);
+by (resolve_tac [subsets_eqpoll_1_eqpoll] 1);
+by (resolve_tac [eqpollI] 1);
+by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1
+ THEN (REPEAT (assume_tac 1)));
+by (resolve_tac [InfCard_is_Card RS Card_is_Ord RS well_ord_Memrel RS
+ well_ord_InfCard_square_eq RS eqpoll_imp_lepoll
+ RSN (2, lepoll_trans)] 1 THEN (assume_tac 2));
+by (resolve_tac [InfCard_is_Card RS Card_cardinal_eq RS ssubst] 2
+ THEN (REPEAT (assume_tac 2)));
+by (eresolve_tac [eqpoll_refl RS prod_eqpoll_cong RS eqpoll_imp_lepoll] 1);
+by (fast_tac (AC_cs addEs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans]
+ addSIs [succ_lepoll_succ_succ]) 1);
+val subsets_eqpoll_X = result();
+
+goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |] \
+\ ==> f``(converse(f)``y) = y";
+by (fast_tac (AC_cs addSIs [equalityI] addDs [apply_equality2]
+ addEs [apply_iff RS iffD2]) 1);
+val image_vimage_eq = result();
+
+goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
+by (fast_tac (AC_cs addSIs [equalityI] addSEs [inj_is_fun RS apply_Pair]
+ addDs [inj_equality]) 1);
+val vimage_image_eq = result();
+
+goalw thy [eqpoll_def] "!!A B. A eqpoll B \
+\ ==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}";
+by (eresolve_tac [exE] 1);
+by (res_inst_tac [("x","lam X:{Y:Pow(A). EX f. f : bij(Y, n)}. f``X")] exI 1);
+by (res_inst_tac [("d","%Z. converse(f)``Z")] lam_bijective 1);
+by (fast_tac (AC_cs
+ addSIs [bij_is_inj RS restrict_bij RS bij_converse_bij RS comp_bij]
+ addSEs [bij_is_fun RS fun_is_rel RS image_subset RS PowI]) 1);
+by (fast_tac (AC_cs addSIs [bij_converse_bij RS bij_is_inj RS restrict_bij
+ RS bij_converse_bij RS comp_bij]
+ addSEs [bij_converse_bij RS bij_is_fun RS fun_is_rel
+ RS image_subset RS PowI]) 1);
+by (fast_tac (AC_cs addSEs [bij_is_inj RS vimage_image_eq]) 1);
+by (fast_tac (AC_cs addSEs [bij_is_surj RS image_vimage_eq]) 1);
+val subsets_eqpoll = result();
+
+goalw thy [WO2_def] "!!X. WO2 ==> EX a. Card(a) & X eqpoll a";
+by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
+by (fast_tac (AC_cs addSEs [well_ord_Memrel RS well_ord_cardinal_eqpoll RS
+ (eqpoll_sym RSN (2, eqpoll_trans)) RS eqpoll_sym]
+ addSIs [Card_cardinal]) 1);
+val WO2_imp_ex_Card = result();
+
+goal thy "!!X. [| X lepoll Y; ~Finite(X) |] ==> ~Finite(Y)";
+by (fast_tac (empty_cs addEs [notE, lepoll_Finite] addSIs [notI]) 1);
+val lepoll_infinite = result();
+
+goalw thy [InfCard_def] "!!X. [| ~Finite(X); Card(X) |] ==> InfCard(X)";
+by (fast_tac (AC_cs addSEs [Card_is_Ord RS nat_le_infinite_Ord]) 1);
+val infinite_Card_is_InfCard = result();
+
+goal thy "!!X n. [| WO2; n:nat; ~Finite(X) |] \
+\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+by (dresolve_tac [WO2_imp_ex_Card] 1);
+by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
+by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
+by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1));
+by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1);
+by (eresolve_tac [subsets_eqpoll] 1);
+by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1));
+by (eresolve_tac [eqpoll_sym] 1);
+val WO2_infinite_subsets_eqpoll_X = result();
+
+goal thy "!!X. well_ord(X,R) ==> EX a. Card(a) & X eqpoll a";
+by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll RS eqpoll_sym]
+ addSIs [Card_cardinal]) 1);
+val well_ord_imp_ex_Card = result();
+
+goal thy "!!X n. [| well_ord(X,R); n:nat; ~Finite(X) |] \
+\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+by (dresolve_tac [well_ord_imp_ex_Card] 1);
+by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
+by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
+by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1));
+by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1);
+by (eresolve_tac [subsets_eqpoll] 1);
+by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1));
+by (eresolve_tac [eqpoll_sym] 1);
+val well_ord_infinite_subsets_eqpoll_X = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC16_lemmas.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+AC16_lemmas = AC_Equiv + Hartog + first
--- a/src/ZF/AC/AC17_AC1.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC17_AC1.ML Tue Jul 25 17:31:53 1995 +0200
@@ -71,7 +71,8 @@
by (asm_full_simp_tac AC_ss 1);
val lemma4 = result();
-goalw thy [AC17_def] "!!Z. [| AC17; ~ AC1 |] ==> False";
+goalw thy [AC17_def] "!!Z. AC17 ==> AC1";
+by (resolve_tac [classical] 1);
by (eresolve_tac [not_AC1_imp_ex RS exE] 1);
by (excluded_middle_tac
"EX f: Pow(x)-{0}->x. \
@@ -80,7 +81,7 @@
by (eresolve_tac [lemma1] 2 THEN (assume_tac 2));
by (dresolve_tac [lemma2] 1);
by (eresolve_tac [allE] 1);
-by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
by (dresolve_tac [lemma4] 1);
by (eresolve_tac [bexE] 1);
by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
@@ -89,7 +90,4 @@
by (dresolve_tac [lemma3] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem),
f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1);
-result();
-
-
-
+qed "AC17_AC1";
--- a/src/ZF/AC/AC18_AC19.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Tue Jul 25 17:31:53 1995 +0200
@@ -15,9 +15,9 @@
\ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))";
by (resolve_tac [lam_type] 1);
by (dresolve_tac [apply_type] 1);
-by (resolve_tac [RepFunI] 1 THEN (atac 1));
-by (dresolve_tac [bspec] 1 THEN (atac 1));
-by (eresolve_tac [subsetD] 1 THEN (atac 1));
+by (resolve_tac [RepFunI] 1 THEN (assume_tac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (eresolve_tac [subsetD] 1 THEN (assume_tac 1));
val PROD_subsets = result();
goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \
@@ -39,7 +39,7 @@
by (resolve_tac [prem RS revcut_rl] 1);
by (fast_tac (AC_cs addSEs [lemma_AC18, UN_E, not_emptyE, apply_type]
addSIs [equalityI, INT_I, UN_I]) 1);
-result();
+qed "AC1_AC18";
(* ********************************************************************** *)
(* AC18 ==> AC19 *)
@@ -49,7 +49,7 @@
by (resolve_tac [allI] 1);
by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
by (fast_tac AC_cs 1);
-result();
+qed "AC18_AC19";
(* ********************************************************************** *)
(* AC19 ==> AC1 *)
@@ -64,7 +64,7 @@
goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a";
by (hyp_subst_tac 1);
-by (resolve_tac [subst_elem] 1 THEN (atac 1));
+by (resolve_tac [subst_elem] 1 THEN (assume_tac 1));
by (resolve_tac [equalityI] 1);
by (fast_tac AC_cs 1);
by (resolve_tac [subsetI] 1);
@@ -116,6 +116,6 @@
by (dresolve_tac [lemma2] 1 THEN (assume_tac 1));
by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [lemma3 RS not_emptyE]) 1);
-result();
+qed "AC19_AC1";
--- a/src/ZF/AC/AC1_AC17.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC1_AC17.ML Tue Jul 25 17:31:53 1995 +0200
@@ -22,4 +22,4 @@
by (eresolve_tac [lemma1] 2);
by (resolve_tac [apply_type] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSDs [lemma1] addSEs [apply_type]) 1);
-result();
\ No newline at end of file
+qed "AC1_AC17";
--- a/src/ZF/AC/AC1_WO2.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC1_WO2.ML Tue Jul 25 17:31:53 1995 +0200
@@ -20,4 +20,4 @@
by (resolve_tac [allI] 1);
by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1);
-result();
+qed "AC1_WO2";
--- a/src/ZF/AC/AC2_AC6.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC2_AC6.ML Tue Jul 25 17:31:53 1995 +0200
@@ -2,8 +2,8 @@
ID: $Id$
Author: Krzysztof Gr`abczewski
-The proofs needed to state that each of AC2, AC3, ..., AC6 is equivallent
-to AC0 and AC1. Namely:
+The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
+to AC0 and AC1:
AC1 ==> AC2 ==> AC1
AC1 ==> AC4 ==> AC3 ==> AC1
AC4 ==> AC5 ==> AC4
@@ -29,9 +29,9 @@
by (resolve_tac [impI] 1);
by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
-by (resolve_tac [lemma1] 2 THEN (REPEAT (atac 2)));
+by (resolve_tac [lemma1] 2 THEN (REPEAT (assume_tac 2)));
by (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
-result();
+qed "AC1_AC2";
(* ********************************************************************** *)
@@ -64,7 +64,7 @@
by (REPEAT (eresolve_tac [allE, impE] 1));
by (fast_tac (AC_cs addSEs [lemma3]) 2);
by (fast_tac (AC_cs addSIs [lemma1, equals0I]) 1);
-result();
+qed "AC2_AC1";
(* ********************************************************************** *)
@@ -79,7 +79,7 @@
by (REPEAT (resolve_tac [allI, impI] 1));
by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
by (fast_tac (AC_cs addSIs [lam_type, RepFunI] addSEs [apply_type]) 1);
-result();
+qed "AC1_AC4";
(* ********************************************************************** *)
@@ -107,7 +107,7 @@
by (eresolve_tac [lemma1] 1);
by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3]
addcongs [Pi_cong]) 1);
-result();
+qed "AC4_AC3";
(* ********************************************************************** *)
(* AC3 ==> AC1 *)
@@ -124,7 +124,7 @@
by (REPEAT (eresolve_tac [allE, ballE] 1));
by (fast_tac (AC_cs addSIs [id_type]) 2);
by (fast_tac (AC_cs addEs [lemma RS subst]) 1);
-result();
+qed "AC3_AC1";
(* ********************************************************************** *)
(* AC4 ==> AC5 *)
@@ -136,15 +136,15 @@
by (eresolve_tac [fun_is_rel RS converse_type] 1);
by (eresolve_tac [exE] 1);
by (resolve_tac [bexI] 1);
-by (resolve_tac [Pi_type] 2 THEN (atac 2));
+by (resolve_tac [Pi_type] 2 THEN (assume_tac 2));
by (fast_tac (ZF_cs addSDs [apply_type]
addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
by (resolve_tac [ballI] 1);
-by (resolve_tac [apply_equality] 1 THEN (atac 2));
+by (resolve_tac [apply_equality] 1 THEN (assume_tac 2));
by (eresolve_tac [domainE] 1);
-by (forward_tac [range_type] 1 THEN (atac 1));
+by (forward_tac [range_type] 1 THEN (assume_tac 1));
by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
-result();
+qed "AC4_AC5";
(* ********************************************************************** *)
@@ -175,21 +175,21 @@
goal thy "!!g. [| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \
\ ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})";
by (resolve_tac [lam_type] 1);
-by (dresolve_tac [apply_type] 1 THEN (atac 1));
-by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
by (resolve_tac [imageI] 1);
by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
- THEN (REPEAT (atac 1)));
+ THEN (REPEAT (assume_tac 1)));
by (asm_full_simp_tac AC_ss 1);
val lemma4 = result();
goalw thy AC_defs "!!Z. AC5 ==> AC4";
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE,ballE] 1));
-by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (atac 2));
-by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (atac 1));
+by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2));
+by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [lemma4]) 1);
-result();
+qed "AC5_AC4";
(* ********************************************************************** *)
@@ -198,4 +198,5 @@
goalw thy AC_defs "AC1 <-> AC6";
by (fast_tac (ZF_cs addDs [equals0D] addSEs [not_emptyE]) 1);
-result();
+qed "AC1_iff_AC6";
+
--- a/src/ZF/AC/AC7_AC9.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Tue Jul 25 17:31:53 1995 +0200
@@ -27,12 +27,12 @@
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 (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
- THEN REPEAT (atac 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 (atac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE1 = result();
@@ -40,7 +40,7 @@
\ ==> 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 (atac 1));
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
by (asm_full_simp_tac ZF_ss 1);
val if_eqE2 = result();
@@ -65,8 +65,8 @@
by (resolve_tac [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 (atac 1));
-by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (atac 1));
+by (resolve_tac [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]
addSIs [nat_0I]) 1);
@@ -87,7 +87,7 @@
goalw thy AC_defs "!!Z. AC6 ==> AC7";
by (fast_tac ZF_cs 1);
-result();
+qed "AC6_AC7";
(* ********************************************************************** *)
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *)
@@ -122,11 +122,11 @@
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 (atac 2));
+by (eresolve_tac [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);
-result();
+qed "AC7_AC6";
(* ********************************************************************** *)
@@ -138,7 +138,7 @@
\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
by (resolve_tac [notI] 1);
by (eresolve_tac [RepFunE] 1);
-by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (dresolve_tac [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);
@@ -147,7 +147,7 @@
goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |] \
\ ==> (lam x:A. f`p(x))`D : p(D)";
-by (resolve_tac [beta RS ssubst] 1 THEN (atac 1));
+by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSEs [apply_type]) 1);
val lemma2 = result();
@@ -158,7 +158,7 @@
by (eresolve_tac [impE] 1);
by (eresolve_tac [lemma1] 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
-result();
+qed "AC1_AC8";
(* ********************************************************************** *)
@@ -183,7 +183,7 @@
by (eresolve_tac [impE] 1);
by (eresolve_tac [lemma1] 1);
by (fast_tac (AC_cs addSEs [lemma2]) 1);
-result();
+qed "AC8_AC9";
(* ********************************************************************** *)
@@ -225,13 +225,13 @@
by (fast_tac (ZF_cs addSIs [fun_weaken_type, bij_is_fun]) 1);
val lemma2 = result();
-val prems = goalw thy AC_defs "!!Z. AC9 ==> AC1";
+goalw thy AC_defs "!!Z. AC9 ==> AC1";
by (resolve_tac [allI] 1);
by (resolve_tac [impI] 1);
by (eresolve_tac [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 (atac 1)));
+by (resolve_tac [lemma1] 1 THEN (REPEAT (assume_tac 1)));
by (fast_tac (AC_cs addSEs [lemma2]) 1);
-result();
\ No newline at end of file
+qed "AC9_AC1";
--- a/src/ZF/AC/AC_Equiv.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Tue Jul 25 17:31:53 1995 +0200
@@ -69,12 +69,12 @@
(*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 (atac 1));
+by (resolve_tac [not_emptyE] 1 THEN (assume_tac 1));
by (forward_tac [singleton_subsetI] 1);
-by (forward_tac [subsetD] 1 THEN (atac 1));
+by (forward_tac [subsetD] 1 THEN (assume_tac 1));
by (res_inst_tac [("A2","A")]
(Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1
- THEN (REPEAT (atac 2)));
+ THEN (REPEAT (assume_tac 2)));
by (fast_tac ZF_cs 1);
val Diff_lepoll = result();
@@ -91,9 +91,9 @@
by (resolve_tac [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 (atac 1));
+ THEN (assume_tac 1));
by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1
- THEN (REPEAT (atac 1)));
+ THEN (REPEAT (assume_tac 1)));
by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1);
val rvimage_id = result();
@@ -138,3 +138,45 @@
by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1);
val Sigma_empty_iff = result();
+goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)";
+by (fast_tac (AC_cs addSIs [eqpoll_refl]) 1);
+val nat_into_Finite = result();
+
+goalw thy [Finite_def] "~Finite(nat)";
+by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll]
+ addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1);
+val nat_not_Finite = result();
+
+val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll;
+
+(* ********************************************************************** *)
+(* Another elimination rule for EX! *)
+(* ********************************************************************** *)
+
+goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y";
+by (eresolve_tac [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);
+val ex1_two_eq = result();
+
+(* ********************************************************************** *)
+(* image of a surjection *)
+(* ********************************************************************** *)
+
+goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B";
+by (eresolve_tac [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);
+val surj_image_eq = result();
+
+
+goal thy "!!y. succ(x) lepoll y ==> y ~= 0";
+by (fast_tac (ZF_cs addSDs [lepoll_0_is_0]) 1);
+val succ_lepoll_imp_not_empty = result();
+
+goal thy "!!x. x eqpoll succ(n) ==> x ~= 0";
+by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1);
+val eqpoll_succ_imp_not_empty = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Cardinal_aux.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,371 @@
+(* Title: ZF/AC/Cardinal_aux.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Auxiliary lemmas concerning cardinalities
+*)
+
+open Cardinal_aux;
+
+(* ********************************************************************** *)
+(* Lemmas involving ordinals and cardinalities used in the proofs *)
+(* concerning AC16 and DC *)
+(* ********************************************************************** *)
+
+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 (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
+ THEN REPEAT (assume_tac 1));
+val Inf_Ord_imp_InfCard_cardinal = result();
+
+goalw thy [lepoll_def] "A Un B lepoll A+B";
+by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
+by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
+by (split_tac [expand_if] 1);
+by (fast_tac (AC_cs addSIs [InlI, InrI]) 1);
+by (split_tac [expand_if] 1);
+by (asm_full_simp_tac (AC_ss addsimps [Inl_def, Inr_def]) 1);
+val Un_lepoll_sum = result();
+
+goalw thy [sum_def] "A+A = 2*A";
+by (fast_tac (AC_cs addIs [equalityI]
+ addSIs [singletonI, nat_0_in_2, succI1]
+ addSEs [succE, singletonE]) 1);
+val sum_eq_2_times = result();
+
+val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
+ asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans))
+ |> standard;
+
+goal thy "!!A. [| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B";
+by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod]
+ MRS lepoll_trans, lepoll_refl] 1));
+val lepoll_imp_sum_lepoll_prod = result();
+
+goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \
+\ ==> A Un B eqpoll i";
+by (resolve_tac [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);
+by (resolve_tac [Un_lepoll_sum RS lepoll_trans] 1);
+by (resolve_tac [lepoll_imp_sum_lepoll_prod RS lepoll_trans] 1);
+by (eresolve_tac [eqpoll_sym RSN (2, eqpoll_trans) RS eqpoll_imp_lepoll] 1
+ THEN (assume_tac 1));
+by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RS
+ (Ord_nat RS (nat_2I RS OrdmemD) RS subset_imp_lepoll RS lepoll_trans)
+ RS (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans))] 1
+ THEN (REPEAT (assume_tac 1)));
+by (eresolve_tac [prod_eqpoll_cong RS eqpoll_imp_lepoll RS lepoll_trans] 1
+ THEN (assume_tac 1));
+by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS
+ well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1
+ THEN REPEAT (assume_tac 1));
+val Un_eqpoll_Inf_Ord = result();
+
+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 (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 (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1);
+by (resolve_tac [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 (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 (contr_tac 1);
+by (resolve_tac [conjI] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [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();
+
+goal thy "{x, y} - {y} = {x} - {y}";
+by (fast_tac eq_cs 1);
+val double_Diff_sing = result();
+
+goal thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
+by (split_tac [expand_if] 1);
+by (asm_full_simp_tac (AC_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
+by (fast_tac (AC_cs addSIs [the_equality, equalityI, equals0I]
+ addEs [equalityE] addSEs [singletonE]) 1);
+val paired_bij_lemma = result();
+
+goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \
+\ : bij({{y,z}. y:x}, x)";
+by (res_inst_tac [("d","%a. {a,z}")] lam_bijective 1);
+by (TRYALL (fast_tac (AC_cs addSEs [RepFunE] addSIs [RepFunI]
+ addss (AC_ss addsimps [paired_bij_lemma]))));
+val paired_bij = result();
+
+goalw thy [eqpoll_def] "{{y,z}. y:x} eqpoll x";
+by (fast_tac (AC_cs addSIs [paired_bij]) 1);
+val paired_eqpoll = result();
+
+goal thy "!!A. EX B. B eqpoll A & B Int C = 0";
+by (fast_tac (AC_cs addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1);
+val ex_eqpoll_disjoint = result();
+
+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 (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)));
+by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS
+ eqpoll_imp_lepoll] 1
+ THEN (REPEAT (assume_tac 1)));
+val Un_lepoll_Inf_Ord = result();
+
+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 (fast_tac (AC_cs addDs [OrdmemD]) 1);
+by (eresolve_tac [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 |] \
+\ ==> y-{THE b. first(b,y,r)} lepoll n";
+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 (fast_tac (AC_cs addSIs [equalityI]) 1);
+val Diff_first_lepoll = result();
+
+goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
+by (fast_tac AC_cs 1);
+val UN_subset_split = result();
+
+goalw thy [lepoll_def] "!!a. Ord(a) ==> (UN x:a. {P(x)}) lepoll a";
+by (res_inst_tac [("x","lam z:(UN x:a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
+by (res_inst_tac [("d","%z. P(z)")] lam_injective 1);
+by (fast_tac (AC_cs addSIs [Least_in_Ord]) 1);
+by (fast_tac (AC_cs addIs [LeastI] addSEs [singletonE, Ord_in_Ord]) 1);
+val UN_sing_lepoll = result();
+
+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 (res_inst_tac [("b","UN b:a. f`b")] subst 1);
+by (resolve_tac [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 (eres_inst_tac [("x","lam x:a. f`x - {THE b. first(b,f`x,R)}")] allE 1);
+by (eresolve_tac [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);
+val UN_fun_lepoll_lemma = result();
+
+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 (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1)));
+by (fast_tac AC_cs 1);
+val UN_fun_lepoll = result();
+
+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 (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2
+ THEN (TRYALL assume_tac));
+by (simp_tac AC_ss 2);
+by (asm_full_simp_tac AC_ss 1);
+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 (fast_tac AC_cs 2);
+by (resolve_tac [subsetI] 1);
+by (eresolve_tac [UN_E] 1);
+by (resolve_tac [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 (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 (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();
+
+goalw thy [eqpoll_def] "!!A B. A Int B = 0 ==> A Un B eqpoll A + B";
+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 (split_tac [expand_if]));
+by (TRYALL (asm_simp_tac sum_ss));
+by (fast_tac (AC_cs addDs [equals0D]) 1);
+val disj_Un_eqpoll_sum = result();
+
+goalw thy [lepoll_def, eqpoll_def]
+ "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
+by (eresolve_tac [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);
+val lepoll_imp_eqpoll_subset = result();
+
+(* ********************************************************************** *)
+(* Some other lemmas *)
+(* ********************************************************************** *)
+
+goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
+by (resolve_tac [eqpoll_trans] 1);
+by (eresolve_tac [nat_into_Ord RS well_ord_Memrel RS (
+ nat_into_Ord RS well_ord_Memrel RSN (2,
+ well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1
+ THEN (assume_tac 1));
+by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1));
+by (asm_full_simp_tac (AC_ss addsimps [cadd_def, eqpoll_refl]) 1);
+val nat_sum_eqpoll_sum = result();
+
+val eqpoll_ordertype =
+ ordermap_bij RS (exI RS (eqpoll_def RS (def_imp_iff RS iffD2)));
+
+goalw thy [lesspoll_def]
+ "!!a. [| b lesspoll a; well_ord(a,r); well_ord(b,s) |] \
+\ ==> ordertype(b,s) < ordertype(a,r)";
+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 (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 (eresolve_tac [ordermap_bij RS bij_converse_bij] 1);
+by (REPEAT (eresolve_tac [conjE,notE] 1));
+by (eresolve_tac [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,
+ lepoll_trans RS lepoll_trans)))] 1
+ THEN (REPEAT (assume_tac 1)));
+val lesspoll_ordertype_lt = result();
+
+goalw thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B";
+by (fast_tac AC_cs 1);
+val lesspoll_imp_lepoll = result();
+
+goalw thy [lepoll_def]
+ "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
+by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1);
+val lepoll_well_ord = result();
+
+goal thy "!!A a. [| A lesspoll a; Ord(a) |] ==> EX b. b<a & A eqpoll b";
+by (resolve_tac [well_ord_Memrel RSN (2,
+ lesspoll_imp_lepoll RS lepoll_well_ord) RS exE] 1
+ THEN (REPEAT (assume_tac 1)));
+by (dresolve_tac [well_ord_Memrel RSN (2, lesspoll_ordertype_lt)] 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac (AC_cs addSEs [eqpoll_ordertype]
+ addEs [ordertype_Memrel RS subst]) 1);
+val lesspoll_imp_ex_lt_eqpoll = result();
+
+goalw thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
+by (fast_tac (AC_cs addSIs [eqpollI] addSEs [eqpollE]) 1);
+val lepoll_iff_leqpoll = result();
+
+goal thy "!!A. [| A lepoll a; Ord(a) |] ==> EX b. b le a & A eqpoll b";
+by (eresolve_tac [lepoll_iff_leqpoll RS iffD1 RS disjE] 1);
+by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] addSIs [leI]) 1);
+by (fast_tac (AC_cs addSIs [le_refl]) 1);
+val lepoll_imp_ex_le_eqpoll = result();
+
+goal thy "!!m. [| m le n; n:nat |] ==> m:nat";
+by (fast_tac (AC_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
+ addSEs [ltE]) 1);
+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 (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)));
+by (forw_inst_tac [("n2","na")]
+ (add_type RS nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll)) 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac (AC_cs addSEs [add_type RSN (2, le_in_nat)]) 1);
+val Finite_Un = result();
+
+goal thy "A <= B Un (A - B)";
+by (fast_tac AC_cs 1);
+val subset_Un_Diff = result();
+
+goalw thy [lesspoll_def] "!!a. [| Card(a); i<a |] ==> i lesspoll a";
+by (dresolve_tac [Card_iff_initial RS iffD1] 1);
+by (fast_tac (AC_cs addSEs [leI RS le_imp_lepoll]) 1);
+val lt_Card_imp_lesspoll = result();
+
+(* ********************************************************************** *)
+(* Diff_lesspoll_eqpoll_Card *)
+(* ********************************************************************** *)
+
+goal thy "!!A B. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a; \
+\ A-B lesspoll a |] ==> P";
+by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE,
+ Card_is_Ord, conjE] 1));
+by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1
+ 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 (dresolve_tac [le_imp_lepoll RSN
+ (2, eqpoll_imp_lepoll RS lepoll_trans)] 1
+ THEN (assume_tac 1));
+by (dresolve_tac [le_imp_lepoll RSN
+ (2, eqpoll_imp_lepoll RS lepoll_trans)] 1
+ THEN (assume_tac 1));
+by (res_inst_tac [("Q","Finite(x Un xa)")] (excluded_middle RS disjE) 1);
+by (dresolve_tac [[lepoll_Finite, lepoll_Finite] MRS Finite_Un] 2
+ THEN (REPEAT (assume_tac 2)));
+by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2);
+by (fast_tac (AC_cs
+ addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2);
+by (dresolve_tac [ Un_lepoll_Inf_Ord] 1
+ THEN (REPEAT (assume_tac 1)));
+by (fast_tac (AC_cs addSEs [ltE, Ord_in_Ord]) 1);
+by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN
+ (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1
+ THEN (TRYALL assume_tac));
+by (fast_tac (AC_cs addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1);
+val Diff_lesspoll_eqpoll_Card_lemma = result();
+
+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 (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();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Cardinal_aux.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+Cardinal_aux = Cardinal + OrderType + CardinalArith + first
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/DC.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,613 @@
+(* Title: ZF/AC/DC.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proofs concerning the Axiom of Dependent Choice
+*)
+
+open DC;
+
+(* ********************************************************************** *)
+(* DC ==> DC(omega) *)
+(* *)
+(* The scheme of the proof: *)
+(* *)
+(* Assume DC. Let R and x satisfy the premise of DC(omega). *)
+(* *)
+(* Define XX and RR as follows: *)
+(* *)
+(* XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) *)
+(* f RR g iff domain(g)=succ(domain(f)) & *)
+(* restrict(g, domain(f)) = f *)
+(* *)
+(* Then RR satisfies the hypotheses of DC. *)
+(* So applying DC: *)
+(* *)
+(* EX f:nat->XX. ALL n:nat. f`n RR f`succ(n) *)
+(* *)
+(* Thence *)
+(* *)
+(* ff = {<n, f`succ(n)`n>. n:nat} *)
+(* *)
+(* is the desired function. *)
+(* *)
+(* ********************************************************************** *)
+
+goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \
+\ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX";
+by (fast_tac AC_cs 1);
+val lemma1_1 = result();
+
+goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \
+\ ==> {z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \
+\ (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 (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 (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1);
+by (resolve_tac [CollectI] 1);
+by (resolve_tac [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,
+ apply_singleton_eq, image_0])) 1);
+by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing,
+ [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1);
+val lemma1_2 = result();
+
+goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \
+\ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \
+\ (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)}) \
+\ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) * \
+\ (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 (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 (res_inst_tac [("x","cons(<n,x>, g)")] exI 1);
+by (resolve_tac [CollectI] 1);
+by (resolve_tac [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 (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
+ addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1);
+val lemma1_3 = result();
+
+goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+\ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \
+\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \
+\ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R) \
+\ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)";
+by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1);
+val lemma1 = result();
+
+goal thy "!!f. [| <f,g> : {z:XX*XX. \
+\ 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 (hyp_subst_tac 1);
+by (eresolve_tac [UN_E] 1);
+by (eresolve_tac [CollectE] 1);
+by (asm_full_simp_tac AC_ss 1);
+by (dresolve_tac [domain_of_fun] 1);
+by (eresolve_tac [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();
+
+goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+\ ALL n:nat. <f`n, f`succ(n)> : \
+\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \
+\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \
+\ 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 (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 (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 (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 (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 (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]
+ addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1);
+val lemma2 = result();
+
+goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+\ ALL n:nat. <f`n, f`succ(n)> : \
+\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \
+\ & 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 (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 (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 (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 (fast_tac (FOL_cs addSDs [domain_of_fun]
+ addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1);
+val lemma3_1 = result();
+
+goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \
+\ ==> {f`succ(x)`x. x:n} = {f`succ(n)`x. x:n}";
+by (asm_full_simp_tac AC_ss 1);
+val lemma3_2 = result();
+
+goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}); \
+\ ALL n:nat. <f`n, f`succ(n)> : \
+\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \
+\ & 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 (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);
+by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1
+ THEN REPEAT (assume_tac 1));
+by (fast_tac (AC_cs addSEs [nat_succI]) 1);
+by (dresolve_tac [nat_succI RSN (4, lemma2)] 1
+ THEN REPEAT (assume_tac 1));
+by (fast_tac (AC_cs addSEs [image_fun RS sym,
+ nat_into_Ord RSN (2, OrdmemD)]) 1);
+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 (fast_tac (AC_cs addSEs [apply_type]) 1);
+val fun_type_gen = result();
+
+goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)";
+by (REPEAT (resolve_tac [allI, impI] 1));
+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 (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 (forward_tac [ltD RSN (3, refl RS lemma2)] 1
+ THEN assume_tac 2);
+by (fast_tac (AC_cs addSEs [fun_type_gen]) 1);
+by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1
+ THEN assume_tac 2);
+by (fast_tac (AC_cs addSEs [fun_type_gen]) 1);
+by (fast_tac (AC_cs addss AC_ss) 1);
+qed "DC0_DC_nat";
+
+(* ********************************************************************** *)
+(* DC(omega) ==> DC *)
+(* *)
+(* The scheme of the proof: *)
+(* *)
+(* Assume DC(omega). Let R and x satisfy the premise of DC. *)
+(* *)
+(* Define XX and RR as follows: *)
+(* *)
+(* XX = (UN n:nat. *)
+(* {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}) *)
+(* RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) *)
+(* & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | *)
+(* (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) *)
+(* & (ALL f:fst(z). restrict(g, domain(f)) = f)) & *)
+(* snd(z)={<0,x>})} *)
+(* *)
+(* Then XX and RR satisfy the hypotheses of DC(omega). *)
+(* So applying DC: *)
+(* *)
+(* EX f:nat->XX. ALL n:nat. f``n RR f`n *)
+(* *)
+(* Thence *)
+(* *)
+(* ff = {<n, f`n`n>. n:nat} *)
+(* *)
+(* is the desired function. *)
+(* *)
+(* ********************************************************************** *)
+
+goalw thy [lesspoll_def, Finite_def]
+ "!!A. A lesspoll nat ==> Finite(A)";
+by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll]
+ addSIs [Ord_nat]) 1);
+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 (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 (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 (fast_tac AC_cs 1);
+by (dresolve_tac [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 (assume_tac 2);
+by (fast_tac AC_cs 1);
+val Finite_Fin = result();
+
+goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \
+\ {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
+by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type]
+ addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing,
+ apply_singleton_eq])) 1);
+val singleton_in_funs = result();
+
+goal thy
+ "!!X. [| XX = (UN n:nat. \
+\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
+\ RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \
+\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \
+\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \
+\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \
+\ 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 (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 (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)) \
+\ & (ALL f:Y. restrict(g, domain(f)) = f)" 1);
+by (fast_tac (AC_cs addss AC_ss) 2);
+by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs]
+ addSIs [SigmaI] addIs [bexI] addss AC_ss) 1);
+val lemma1 = result();
+
+goal thy "!!f. [| f:nat->X; n:nat |] ==> \
+\ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))";
+by (asm_full_simp_tac (AC_ss
+ addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun),
+ [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
+val UN_image_succ_eq = result();
+
+goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \
+\ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
+by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1);
+by (fast_tac (AC_cs addSIs [equalityI]) 1);
+val UN_image_succ_eq_succ = result();
+
+goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \
+\ domain(f)=succ(x); x=y |] ==> f`y : D";
+by (fast_tac (AC_cs addEs [apply_type]
+ addSDs [[sym, domain_of_fun] MRS trans]) 1);
+val apply_UN_type = result();
+
+goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)";
+by (asm_full_simp_tac (AC_ss
+ addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1);
+val image_fun_succ = result();
+
+goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \
+\ {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 (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1);
+val f_n_type = result();
+
+goal thy "!!f. [| f : nat -> (UN n:nat. \
+\ {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 (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1));
+by (dresolve_tac [succ_eqD] 1);
+by (asm_full_simp_tac AC_ss 1);
+val f_n_pairs_in_R = result();
+
+goalw thy [restrict_def]
+ "!!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 (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);
+val restrict_cons_eq_restrict = result();
+
+goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \
+\ f : nat -> (UN n:nat. \
+\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
+\ 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 (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 (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1);
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1);
+val all_in_image_restrict_eq = result();
+
+goal thy "!!X. [| ALL b<nat. <f``b, f`b> : \
+\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \
+\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \
+\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \
+\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \
+\ XX = (UN n:nat. \
+\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
+\ f: nat -> XX; range(R) <= domain(R); x:domain(R) \
+\ |] ==> ALL b<nat. <f``b, f`b> : \
+\ {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 (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1);
+by (REPEAT (eresolve_tac [CollectE, conjE, disjE] 1));
+by (asm_full_simp_tac (AC_ss
+ addsimps [image_0, singleton_fun RS domain_of_fun,
+ [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1);
+by (asm_full_simp_tac (AC_ss
+ addsimps [image_0, singleton_fun RS domain_of_fun,
+ [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs]) 1);
+by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
+ THEN (assume_tac 1));
+by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1));
+by (fast_tac (AC_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 (hyp_subst_tac 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 (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 (fast_tac (AC_cs addSEs [cons_fun_type2]) 1);
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [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 (asm_full_simp_tac (AC_ss
+ addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1);
+val simplify_recursion = result();
+
+goal thy "!!X. [| XX = (UN n:nat. \
+\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
+\ ALL b<nat. <f``b, f`b> : \
+\ {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))}; \
+\ 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 (eresolve_tac [Ord_nat RSN (2, ltI)] 1);
+by (eresolve_tac [CollectE] 1);
+by (asm_full_simp_tac AC_ss 1);
+by (resolve_tac [conjI] 1);
+by (fast_tac (AC_cs
+ addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1);
+by (fast_tac (AC_cs addSEs [nat_succI, succI2, f_n_pairs_in_R RS bspec,
+ subst_context, trans]) 1);
+val lemma2 = result();
+
+goal thy "!!n. [| XX = (UN n:nat. \
+\ {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R}); \
+\ ALL b<nat. <f``b, f`b> : \
+\ {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))}; \
+\ f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \
+\ |] ==> f`n`n = f`succ(n)`n";
+by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1
+ THEN REPEAT (assume_tac 1));
+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 (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
+ addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
+val lemma3 = result();
+
+goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0";
+by (REPEAT (resolve_tac [allI, impI] 1));
+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 (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 (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2
+ THEN REPEAT (assume_tac 2));
+by (resolve_tac [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));
+by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1);
+qed "DC_nat_DC0";
+
+(* ********************************************************************** *)
+(* ALL K. Card(K) --> DC(K) ==> WO3 *)
+(* ********************************************************************** *)
+
+goalw thy [lesspoll_def]
+ "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0";
+by (fast_tac (AC_cs addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll]
+ addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1);
+val lemma1 = result();
+
+val [f_type, Ord_a, not_eq] = goalw thy [inj_def]
+ "[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) \
+\ |] ==> f:inj(a, X)";
+by (resolve_tac [f_type RS CollectI] 1);
+by (REPEAT (resolve_tac [ballI,impI] 1));
+by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1
+ THEN (assume_tac 1));
+by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1);
+by (REPEAT (fast_tac (AC_cs addDs [not_eq, not_eq RS not_sym]) 1));
+val fun_Ord_inj = result();
+
+goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A";
+by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1);
+val value_in_image = result();
+
+goalw thy [DC_def, WO3_def]
+ "!!Z. ALL K. Card(K) --> DC(K) ==> WO3";
+by (resolve_tac [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 (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 (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1);
+by (eresolve_tac [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));
+by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2,
+ ltD RSN (3, value_in_image))] 1
+ THEN REPEAT (assume_tac 1));
+by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)]
+ addEs [subst]) 1);
+qed "DC_WO3";
+
+(* ********************************************************************** *)
+(* WO1 ==> ALL K. Card(K) --> DC(K) *)
+(* ********************************************************************** *)
+
+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 (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD]
+ addSIs [lam_type]) 2));
+by (resolve_tac [ballI] 1);
+by (dresolve_tac [OrdmemD RS subsetD] 1
+ THEN REPEAT (assume_tac 1));
+by (asm_full_simp_tac AC_ss 1);
+val lam_images_eq = result();
+
+goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K";
+by (asm_full_simp_tac (AC_ss addsimps [Card_iff_initial]) 1);
+by (fast_tac (AC_cs addSIs [le_imp_lepoll, ltI, leI]) 1);
+val in_Card_imp_lesspoll = result();
+
+goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}";
+by (fast_tac (AC_cs addSIs [lam_type, RepFunI]) 1);
+val lam_type_RepFun = result();
+
+goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R); \
+\ b:a; Z:Pow(X); Z lesspoll a |] \
+\ ==> {x:X. <Z,x> : R} ~= 0";
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addSIs [not_emptyI]) 1);
+val lemma_ = result();
+
+goal thy "!!K. [| Card(K); well_ord(X,Q); \
+\ ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |] \
+\ ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}";
+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 (resolve_tac [ff_def RS def_transrec RS ssubst] 1);
+by (eresolve_tac [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 (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]
+ MRS lepoll_lesspoll_lesspoll]) 1);
+val lemma = result();
+
+goalw thy [DC_def, WO1_def]
+ "!!Z. WO1 ==> ALL K. Card(K) --> DC(K)";
+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 (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);
+by (fast_tac (AC_cs addSEs [ltE, lemma RS CollectD2]) 1);
+qed" WO1_DC_Card";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/DC.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,28 @@
+(* Title: ZF/AC/DC.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Theory file for the proofs concernind the Axiom of Dependent Choice
+*)
+
+DC = AC_Equiv + Hartog + first + Cardinal_aux + "DC_lemmas" +
+
+consts
+
+ DC :: "i => o"
+ DC0 :: "o"
+ ff :: "[i, i, i, i] => i"
+
+rules
+
+ DC_def "DC(a) == ALL X R. R<=Pow(X)*X &
+ (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
+ --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
+
+ DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
+ --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
+
+ ff_def "ff(b, X, Q, R) == transrec(b, %c r.
+ THE x. first(x, {x:X. <r``c, x> : R}, Q))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/DC_lemmas.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,146 @@
+(* Title: ZF/AC/DC_lemmas.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+More general lemmas used in the proofs concerning DC
+
+*)
+
+val [prem] = goalw thy [lepoll_def]
+ "Ord(a) ==> {P(b). b:a} lepoll a";
+by (res_inst_tac [("x","lam z:RepFun(a,P). LEAST i. z=P(i)")] exI 1);
+by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1);
+by (fast_tac (AC_cs addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1);
+by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1));
+val RepFun_lepoll = result();
+
+goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat";
+by (resolve_tac [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 (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS
+ subset_imp_lepoll) RS lepoll_trans] 1
+ THEN (assume_tac 1));
+val n_lesspoll_nat = result();
+
+goalw thy [lepoll_def]
+ "!!f. [| f:X->Y; Ord(X) |] ==> f``X lepoll X";
+by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1);
+by (res_inst_tac [("d","%z. f`z")] lam_injective 1);
+by (fast_tac (AC_cs addSIs [Least_in_Ord, apply_equality]) 1);
+by (fast_tac (AC_cs addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1);
+val image_Ord_lepoll = result();
+
+val apply_singleton_eq = [singletonI, singleton_fun] MRS apply_equality;
+
+goal thy "restrict(f, 0) = 0";
+by (resolve_tac [singleton_iff RS iffD1] 1);
+by (resolve_tac [Pi_empty1 RS subst] 1);
+by (fast_tac (AC_cs addSIs [restrict_type]) 1);
+val restrict_0 = result();
+
+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 (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1);
+by (fast_tac AC_cs 1);
+val range_subset_domain = result();
+
+goal thy "domain({<x,y>}) = {x}";
+by (fast_tac (AC_cs addSIs [equalityI, singletonI] addSEs [singletonE]) 1);
+val domain_sing = result();
+
+val prems = goal thy "!!k. k:n ==> k~=n";
+by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
+val mem_not_eq = result();
+
+goal thy "!!a. [| a:B; A<=B |] ==> cons(a, A) <= B";
+by (fast_tac AC_cs 1);
+val cons_subset = result();
+
+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 (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 (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();
+
+goal thy "!!x. x:X ==> cons(x, X) = X";
+by (fast_tac (AC_cs addSIs [equalityI]) 1);
+val cons_eq_self = result();
+
+val [g_type, x_in] = goal thy "[| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X";
+by (resolve_tac [x_in RS cons_eq_self RS subst] 1);
+by (resolve_tac [g_type RS cons_fun_type] 1);
+val cons_fun_type2 = result();
+
+goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n";
+by (fast_tac (AC_cs addSIs [equalityI] addSEs [mem_irrefl]) 1);
+val cons_image_n = result();
+
+goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x";
+by (fast_tac (AC_cs addSIs [apply_equality] addSEs [cons_fun_type]) 1);
+val cons_val_n = result();
+
+goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k";
+by (fast_tac (AC_cs addSIs [equalityI] addEs [mem_asym]) 1);
+val cons_image_k = result();
+
+goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
+by (fast_tac (AC_cs addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1);
+val cons_val_k = result();
+
+goal thy "!!f. domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)";
+by (asm_full_simp_tac (AC_ss addsimps [domain_cons, succ_def]) 1);
+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 (eresolve_tac [cons_fun_type RS apply_type] 1);
+by (eresolve_tac [succI2] 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (AC_ss addsimps [cons_val_k]) 1);
+val restrict_cons_eq = result();
+
+goal thy "!!k. [| Ord(k); i:k |] ==> succ(i) : succ(k)";
+by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3));
+by (REPEAT (fast_tac (AC_cs addSIs [Ord_succ]
+ addEs [Ord_in_Ord, mem_irrefl, mem_asym]
+ addSDs [succ_inject]) 1));
+val succ_in_succ = result();
+
+goalw thy [restrict_def]
+ "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
+by (eresolve_tac [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 (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();
+
+goal thy "!!n. n:nat ==> 0:succ(n)";
+by (fast_tac (AC_cs addSDs [[Ord_0, nat_into_Ord] MRS Ord_linear]) 1);
+val nat_0_in_succ = result();
+
+goal thy "!!f. [| domain(f)=A; f:B->C |] ==> f:A->C";
+by (forward_tac [domain_of_fun] 1);
+by (fast_tac AC_cs 1);
+val domain_eq_imp_fun_type = result();
+
+goal thy "!!R. [| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)";
+by (fast_tac (AC_cs addSEs [not_emptyE]) 1);
+val ex_in_domain = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/DC_lemmas.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,4 @@
+(*Dummy theory to document dependencies *)
+
+DC_lemmas = AC_Equiv + first
+
--- a/src/ZF/AC/HH.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/HH.ML Tue Jul 25 17:31:53 1995 +0200
@@ -15,15 +15,15 @@
(* ********************************************************************** *)
goal thy "HH(f,x,a) = \
-\ (lam y:Pow(x). if(f`y : Pow(y)-{0},f`y,{x}))` \
-\ (x - (UN b:a. HH(f,x,b)))";
+\ (let z = x - (UN b:a. HH(f,x,b)) \
+\ in if(f`z:Pow(z)-{0}, f`z, {x}))";
by (resolve_tac [HH_def RS def_transrec RS trans] 1);
by (asm_full_simp_tac ZF_ss 1);
val HH_def_satisfies_eq = result();
goal thy "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
-by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1);
by (split_tac [expand_if] 1);
by (fast_tac ZF_cs 1);
val HH_values = result();
@@ -76,7 +76,7 @@
\ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}";
by (dresolve_tac [HH_def_satisfies_eq RS subst] 1);
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
-by (asm_full_simp_tac (AC_ss addsimps [Diff_subset RS PowI]) 1);
+by (asm_full_simp_tac (AC_ss addsimps [Let_def, Diff_subset RS PowI]) 1);
by (dresolve_tac [expand_if RS iffD1] 1);
by (split_tac [expand_if] 1);
by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
@@ -173,7 +173,7 @@
goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \
\ ==> HH(f, x, i) : Pow(x) - {0}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
-by (asm_full_simp_tac (AC_ss addsimps [Diff_subset RS PowI,
+by (asm_full_simp_tac (AC_ss addsimps [Let_def, Diff_subset RS PowI,
not_emptyI2 RS if_P]) 1);
by (fast_tac AC_cs 1);
val f_subset_imp_HH_subset = result();
@@ -190,7 +190,7 @@
goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
-by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1);
by (split_tac [expand_if] 1);
by (fast_tac ZF_cs 1);
val HH_values2 = result();
--- a/src/ZF/AC/HH.thy Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/HH.thy Tue Jul 25 17:31:53 1995 +0200
@@ -8,7 +8,7 @@
AC15 ==> WO6
*)
-HH = AC_Equiv + Hartog + WO_AC +
+HH = AC_Equiv + Hartog + WO_AC + Let +
consts
@@ -16,8 +16,8 @@
defs
- HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x).
- if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))"
+ HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (UN c:b. r`c)
+ in if(f`z:Pow(z)-{0}, f`z, {x}))"
end
--- a/src/ZF/AC/Hartog.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/Hartog.ML Tue Jul 25 17:31:53 1995 +0200
@@ -21,16 +21,16 @@
by (resolve_tac [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 (atac 1));
+ THEN (assume_tac 1));
by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS
(well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS
(ordertype_Memrel RSN (2, trans))] 1
- THEN (REPEAT (atac 1)));
+ THEN (REPEAT (assume_tac 1)));
val Ord_lepoll_imp_ex_well_ord = result();
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 (atac 1));
+by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1));
by (step_tac AC_cs 1);
by (REPEAT (ares_tac [exI, conjI] 1));
by (eresolve_tac [ordertype_Int] 2);
@@ -42,8 +42,8 @@
\ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z=<Y,R> & ordertype(Y,R)=a}";
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE, impE] 1));
-by (atac 1);
-by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (atac 1));
+by (assume_tac 1);
+by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1));
by (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1);
val Ords_lepoll_set_lemma = result();
@@ -81,4 +81,4 @@
goal thy "Card(Hartog(A))";
by (fast_tac (AC_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1);
-val Card_Hartog = result();
\ No newline at end of file
+val Card_Hartog = result();
--- a/src/ZF/AC/ROOT.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/ROOT.ML Tue Jul 25 17:31:53 1995 +0200
@@ -24,17 +24,20 @@
time_use "AC/AC2_AC6.ML";
time_use "AC/AC7_AC9.ML";
-time_use_thy "AC/WO1_AC1";
+time_use_thy "AC/WO1_AC";
time_use_thy "AC/AC1_WO2";
time_use "AC/AC10_AC15.ML";
time_use_thy "AC/AC15_WO6";
-(* AC16 to add *)
+time_use_thy "AC/WO2_AC16";
+time_use_thy "AC/AC16_WO4";
time_use "AC/AC1_AC17.ML";
time_use_thy "AC/AC17_AC1";
time_use_thy "AC/AC18_AC19";
+time_use_thy "AC/DC";
+
writeln"END: Root file for ZF/AC";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_AC.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,120 @@
+(* Title: ZF/AC/WO1_AC.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1
+
+The latter proof is referred to as clear by the Rubins.
+However it seems to be quite complicated.
+The formal proof presented below is a mechanisation of the proof
+by Lawrence C. Paulson which is the following:
+
+Assume WO1. Let s be a set of infinite sets.
+
+Suppose x:s. Then x is equipollent to |x| (by WO1), an infinite cardinal;
+call it K. Since K = K |+| K = |K+K| (by InfCard_cdouble_eq) there is an
+isomorphism h: bij(K+K, x). (Here + means disjoint sum.)
+
+So there is a partition of x into 2-element sets, namely
+
+ {{h(Inl(i)), h(Inr(i))} . i:K}
+
+So for all x:s the desired partition exists. By AC1 (which follows from WO1)
+there exists a function f that chooses a partition for each x:s. Therefore we
+have AC10(2).
+
+*)
+
+open WO1_AC;
+
+(* ********************************************************************** *)
+(* WO1 ==> AC1 *)
+(* ********************************************************************** *)
+
+goalw thy [AC1_def, WO1_def] "!!Z. WO1 ==> AC1";
+by (fast_tac (AC_cs addSEs [ex_choice_fun]) 1);
+qed "WO1_AC1";
+
+(* ********************************************************************** *)
+(* WO1 ==> AC10(n) (n >= 1) *)
+(* ********************************************************************** *)
+
+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 (fast_tac (AC_cs addEs [RepFunE, sym RS equals0D]) 1);
+by (eresolve_tac [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)]
+ addSEs [CollectD2]) 1);
+val lemma1 = result();
+
+goalw thy [WO1_def] "!!A. [| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B";
+by (resolve_tac [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 (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);
+val lemma2_1 = result();
+
+goal thy "!!f. f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))";
+by (fast_tac (AC_cs addSIs [InlI, InrI]
+ addSEs [RepFunE, bij_is_fun RS apply_type]) 1);
+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 (TRYALL (fast_tac (AC_cs addSEs [inj_is_fun RS apply_Pair] addEs [subst])));
+val lemma = result();
+
+goalw thy AC_aux_defs
+ "!!f. f : bij(D+D, B) ==> \
+\ pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})";
+by (fast_tac (AC_cs addSEs [RepFunE, not_emptyE]
+ addDs [bij_is_inj RS lemma, Inl_iff RS iffD1,
+ Inr_iff RS iffD1, Inl_Inr_iff RS iffD1 RS FalseE,
+ Inr_Inl_iff RS iffD1 RS FalseE]
+ addSIs [InlI, InrI]) 1);
+val lemma2_3 = result();
+
+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 (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]
+ addDs [major RS bij_is_inj RS lemma, Inl_Inr_iff RS iffD1 RS FalseE]
+ addSEs [RepFunE, not_emptyE, mem_irrefl]) 1);
+val lemma2_4 = result();
+
+goalw thy [bij_def, surj_def]
+ "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B";
+by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type, CollectE, sumE]
+ addSIs [InlI, InrI, equalityI]) 1);
+val lemma2_5 = result();
+
+goal thy "!!A. [| WO1; ~Finite(B); 1 le n |] \
+\ ==> EX C:Pow(Pow(B)). pairwise_disjoint(C) & \
+\ sets_of_size_between(C, 2, succ(n)) & \
+\ Union(C)=B";
+by (eresolve_tac [lemma2_1 RS (eqpoll_def RS def_imp_iff RS iffD1 RS exE)] 1
+ THEN (assume_tac 1));
+by (fast_tac (FOL_cs addSIs [bexI]
+ addSEs [lemma2_2, lemma2_3, lemma2_4, lemma2_5]) 1);
+val lemma2 = result();
+
+goalw thy AC_defs "!!n. [| WO1; 1 le n |] ==> AC10(n)";
+by (fast_tac (AC_cs addSIs [lemma1] addSEs [lemma2]) 1);
+qed "WO1_AC10";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_AC.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+WO1_AC = AC_Equiv + WO_AC
--- a/src/ZF/AC/WO1_AC1.ML Tue Jul 25 17:03:59 1995 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: ZF/AC/WO1_AC1.ML
- ID: $Id$
- Author: Krzysztof Gr`abczewski
-
-The proof of WO1 ==> AC1
-*)
-
-open WO1_AC1;
-
-goalw thy [AC1_def, WO1_def] "!!Z. WO1 ==> AC1";
-by (fast_tac (AC_cs addSEs [ex_choice_fun]) 1);
-result();
\ No newline at end of file
--- a/src/ZF/AC/WO1_AC1.thy Tue Jul 25 17:03:59 1995 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-(*Dummy theory to document dependencies *)
-
-WO1_AC1 = AC_Equiv + WO_AC
--- a/src/ZF/AC/WO1_WO6.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO1_WO6.ML Tue Jul 25 17:31:53 1995 +0200
@@ -15,20 +15,20 @@
goalw thy WO_defs "!!Z. WO2 ==> WO3";
by (fast_tac ZF_cs 1);
-result();
+qed "WO2_WO3";
(* ********************************************************************** *)
goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1";
by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage,
well_ord_Memrel RS well_ord_subset]) 1);
-result();
+qed "WO3_WO1";
(* ********************************************************************** *)
goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2";
by (fast_tac (ZF_cs addSIs [Ord_ordertype, ordermap_bij]) 1);
-result();
+qed "WO1_WO2";
(* ********************************************************************** *)
@@ -57,23 +57,23 @@
by (asm_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS
bij_is_surj RS surj_imp_eq)]) 1);
-result();
+qed "WO1_WO4";
(* ********************************************************************** *)
goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)";
by (fast_tac (AC_cs addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1);
-result();
+qed "WO4_mono";
(* ********************************************************************** *)
-val prems = goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
+goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
by (fast_tac ZF_cs 1);
-result();
+qed "WO4_WO5";
(* ********************************************************************** *)
-val prems = goalw thy WO_defs "!!Z. WO5 ==> WO6";
+goalw thy WO_defs "!!Z. WO5 ==> WO6";
by (fast_tac ZF_cs 1);
-result();
+qed "WO5_WO6";
--- a/src/ZF/AC/WO1_WO7.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Tue Jul 25 17:31:53 1995 +0200
@@ -46,7 +46,7 @@
goalw thy [wf_on_def, wf_def]
"!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))";
by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1
- THEN (atac 1));
+ THEN (assume_tac 1));
by (resolve_tac [notI] 1);
by (eres_inst_tac [("x","nat")] allE 1);
by (eresolve_tac [disjE] 1);
@@ -67,11 +67,11 @@
by (rtac ([ordertype_ord_iso RS ord_iso_sym RS ord_iso_rvimage_eq,
Memrel_type RS (subset_Int_iff RS iffD1)]
MRS trans RS subst) 1
- THEN (atac 1));
+ THEN (assume_tac 1));
by (rtac (rvimage_converse RS subst) 1);
by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS
bij_is_inj RS well_ord_rvimage) 1
- THEN (atac 1));
+ THEN (assume_tac 1));
val well_ord_converse_Memrel = result();
goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \
@@ -79,7 +79,7 @@
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE,exE] 1));
by (REPEAT (ares_tac [exI,conjI,notI] 1));
-by (forward_tac [well_ord_converse_Memrel] 1 THEN (atac 1));
+by (forward_tac [well_ord_converse_Memrel] 1 THEN (assume_tac 1));
by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1);
by (contr_tac 2);
by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS
--- a/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:31:53 1995 +0200
@@ -11,7 +11,7 @@
goalw thy WO_defs "!!Z. WO1 ==> WO8";
by (fast_tac ZF_cs 1);
-result();
+qed "WO1_WO8";
(* ********************************************************************** *)
(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
@@ -27,4 +27,4 @@
by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
addSIs [lam_type, singletonI]
addIs [the_equality RS ssubst]) 1);
-result();
\ No newline at end of file
+qed "WO8_WO1";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO2_AC16.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,605 @@
+(* Title: ZF/AC/WO2_AC16.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+ The proof of WO2 ==> AC16(k #+ m, k)
+
+ The main part of the proof is the inductive reasoning concerning
+ properties of constructed family T_gamma.
+ The proof deals with three cases for ordinals: 0, succ and limit ordinal.
+ The first instance is trivial, the third not difficult, but the second
+ is very complicated requiring many lemmas.
+ We also need to prove that at any stage gamma the set
+ (s - Union(...) - k_gamma) (Rubin & Rubin page 15)
+ contains m distinct elements (in fact is equipollent to s)
+*)
+
+(* ********************************************************************** *)
+(* case of limit ordinal *)
+(* ********************************************************************** *)
+
+goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \
+\ --> (EX! Y. Y:F(y) & f(z)<=Y); \
+\ ALL i j. i le j --> F(i) <= F(j); j le i; i<x; z<a; \
+\ 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 (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)));
+val lemma3_1 = result();
+
+goal thy "!!Z. [| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \
+\ --> (EX! Y. Y:F(y) & f(z)<=Y); \
+\ ALL i j. i le j --> F(i) <= F(j); i<x; j<x; z<a; \
+\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \
+\ ==> V = W";
+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)));
+val lemma3 = result();
+
+goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \
+\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \
+\ (EX! Y. Y : F(y) & fa(x) <= Y)); x < a |] \
+\ ==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) --> \
+\ (EX! Y. Y : F(y) & fa(z) <= Y)";
+by (REPEAT (resolve_tac [oallI, impI] 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 (FOL_cs addSEs [oallE]) 1);
+val lemma4 = result();
+
+goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \
+\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \
+\ (EX! Y. Y : F(y) & fa(x) <= Y)); \
+\ x < a; Limit(x); ALL i j. i le j --> F(i) <= F(j) |] \
+\ ==> (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 (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 (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 (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 (REPEAT (eresolve_tac [conjE, OUN_E] 1));
+by (eresolve_tac [lemma3] 1 THEN (TRYALL assume_tac));
+val lemma5 = result();
+
+(* ********************************************************************** *)
+(* case of successor ordinal *)
+(* ********************************************************************** *)
+
+(*
+ First quite complicated proof of the fact used in the recursive construction
+ of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage
+ gamma the set (s - Union(...) - k_gamma) is equipollent to s
+ (Rubin & Rubin page 15).
+*)
+
+(* ********************************************************************** *)
+(* dbl_Diff_eqpoll_Card *)
+(* ********************************************************************** *)
+
+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)));
+val dbl_Diff_eqpoll_Card = result();
+
+(* ********************************************************************** *)
+(* Case of finite ordinals *)
+(* ********************************************************************** *)
+
+goalw thy [lesspoll_def]
+ "!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a";
+by (resolve_tac [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 (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2);
+by (resolve_tac [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();
+
+goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
+by (fast_tac (AC_cs addIs [equalityI] addSIs [singletonI]
+ addSEs [singletonE]) 1);
+val Union_eq_Un_Diff = result();
+
+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 (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 (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 (fast_tac AC_cs 1);
+val Finite_Union = result();
+
+goalw thy [Finite_def] "!!x. [| x lepoll n; n:nat |] ==> Finite(x)";
+by (fast_tac (AC_cs
+ addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE,
+ Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1);
+val lepoll_nat_num_imp_Finite = result();
+
+goal thy "!!X. [| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \
+\ b<a; ~Finite(a); Card(a); n:nat |] \
+\ ==> Union(X) lesspoll a";
+by (excluded_middle_tac "Finite(X)" 1);
+by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2
+ THEN (REPEAT (assume_tac 3)));
+by (fast_tac (AC_cs addSEs [lepoll_nat_num_imp_Finite]
+ addSIs [Finite_Union]) 2);
+by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1));
+by (REPEAT (eresolve_tac [exE, conjE] 1));
+by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
+by (eresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1) RS
+ exE] 1);
+by (forward_tac [bij_is_surj RS surj_image_eq] 1);
+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 (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
+ THEN REPEAT (assume_tac 1));
+by (resolve_tac [UN_lepoll] 1
+ THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord]))));
+val Union_lesspoll = result();
+
+(* ********************************************************************** *)
+(* recfunAC16_lepoll_index *)
+(* ********************************************************************** *)
+
+goal thy "A Un {a} = cons(a, A)";
+by (fast_tac (AC_cs addSIs [singletonI]
+ addSEs [singletonE] addIs [equalityI]) 1);
+val Un_sing_eq_cons = result();
+
+goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
+by (asm_simp_tac (AC_ss addsimps [Un_sing_eq_cons, succ_def]) 1);
+by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1);
+val Un_lepoll_succ = result();
+
+goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
+by (fast_tac (AC_cs addSIs [OUN_I, le_refl] addIs [equalityI]) 1);
+val Diff_UN_succ_empty = result();
+
+goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
+by (fast_tac (AC_cs addSIs [OUN_I, le_refl]) 1);
+val Diff_UN_succ_subset = result();
+
+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 (asm_simp_tac (AC_ss addsimps [recfunAC16_0,
+ empty_subsetI RS subset_imp_lepoll]) 1);
+by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit,
+ Diff_cancel, empty_subsetI RS subset_imp_lepoll]) 2);
+by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1);
+by (resolve_tac [conjI RS (expand_if RS iffD2)] 1);
+by (fast_tac (AC_cs addSIs [empty_subsetI RS subset_imp_lepoll]
+ addSEs [Diff_UN_succ_empty RS ssubst]) 1);
+by (fast_tac (AC_cs addSEs [Diff_UN_succ_subset RS subset_imp_lepoll RS
+ (singleton_eqpoll_1 RS eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1);
+val recfunAC16_Diff_lepoll_1 = result();
+
+goal thy "!!z. [| z : F(x); Ord(x) |] \
+\ ==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))";
+by (fast_tac (AC_cs addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1);
+val in_Least_Diff = result();
+
+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 (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 (eresolve_tac [lt_Ord RSN (2, Least_le) RS lt_trans1] 1
+ THEN (REPEAT (assume_tac 1)));
+val Least_eq_imp_ex = result();
+
+goal thy "!!A. [| A lepoll 1; a:A; b:A |] ==> a=b";
+by (fast_tac (AC_cs addSDs [lepoll_1_is_sing] addSEs [singletonE]) 1);
+val two_in_lepoll_1 = result();
+
+goal thy "!!a. [| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |] \
+\ ==> (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 (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 (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 (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)]
+ addSDs [succI1 RSN (2, bspec)]
+ addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans),
+ Un_lepoll_succ]) 1);
+by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 1);
+by (fast_tac (AC_cs addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1]
+ addSIs [UN_lepoll_index]) 1);
+val recfunAC16_lepoll_index = result();
+
+goal thy "!!y. [| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \
+\ 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 (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));
+by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1);
+val Union_recfunAC16_lesspoll = result();
+
+goal thy
+ "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+\ Card(a); ~ Finite(a); A eqpoll a; \
+\ 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 (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
+ THEN (TRYALL assume_tac));
+by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1
+ THEN (TRYALL assume_tac));
+val dbl_Diff_eqpoll = result();
+
+(* back to the proof *)
+
+val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS (
+ sum_eqpoll_cong RSN (2,
+ nat_sum_eqpoll_sum RSN (3,
+ eqpoll_trans RS eqpoll_trans))) |> standard;
+
+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 (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
+ 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
+ THEN (REPEAT (assume_tac 1)));
+val Un_in_Collect = result();
+
+(* ********************************************************************** *)
+(* Lemmas simplifying assumptions *)
+(* ********************************************************************** *)
+
+goal thy "!!j. [| ALL y:succ(j). y<a --> F(y)<=X & (ALL x<a. x<y | P(x,y) \
+\ --> 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 (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();
+
+goal thy "!!j. [| F(j)<=X; (ALL x<a. x<j | P(x,j) --> Q(x,j)); succ(j)<a |] \
+\ ==> P(j,j) --> F(j) <= X & (ALL x<a. x le j | P(x,j) --> Q(x,j))";
+by (fast_tac (AC_cs addSEs [leE]) 1);
+val lemma7 = result();
+
+(* ********************************************************************** *)
+(* Lemmas needded to prove ex_next_set which means that for any successor *)
+(* ordinal there is a set satisfying certain properties *)
+(* ********************************************************************** *)
+
+goal thy "!!A. [| A eqpoll a; ~ Finite(a); Ord(a); m:nat |] \
+\ ==> EX X:Pow(A). X eqpoll m";
+by (eresolve_tac [Ord_nat RSN (2, ltI) RS
+ (nat_le_infinite_Ord RSN (2, lt_trans2)) RS
+ leI RS le_imp_lepoll RS
+ ((eqpoll_sym RS eqpoll_imp_lepoll) RSN (2, lepoll_trans)) RS
+ lepoll_imp_eqpoll_subset RS exE] 1
+ THEN REPEAT (assume_tac 1));
+by (fast_tac (AC_cs addSEs [eqpoll_sym]) 1);
+val ex_subset_eqpoll = result();
+
+goal thy "!!A. [| A <= B Un C; A Int C = 0 |] ==> A <= B";
+by (fast_tac (AC_cs addDs [equals0D]) 1);
+val subset_Un_disjoint = result();
+
+goal thy "!!F. [| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
+by (fast_tac (AC_cs addSIs [equals0I]) 1);
+val Int_empty = result();
+
+(* ********************************************************************** *)
+(* equipollent subset (and finite) is the whole set *)
+(* ********************************************************************** *)
+
+goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
+by (fast_tac (AC_cs addSEs [equalityE, singletonE]
+ addSIs [equalityI, singletonI]) 1);
+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 (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 (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 (fast_tac AC_cs 2);
+by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1);
+by (eresolve_tac [Diffs_eq_imp_eq] 1
+ THEN REPEAT (assume_tac 1));
+val subset_imp_eq_lemma = result();
+
+goal thy "!!A. [| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B";
+by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1);
+val subset_imp_eq = result();
+
+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 (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
+ CollectE, eqpoll_imp_lepoll]) 1);
+by (rewrite_goals_tac [bij_def, inj_def]);
+by (fast_tac (AC_cs addSDs [ltD]) 1);
+val bij_imp_arg_eq = result();
+
+goal thy
+ "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+\ Card(a); ~ Finite(a); A eqpoll a; \
+\ k : nat; m : nat; y<a; \
+\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
+\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \
+\ ==> EX X:{Y: Pow(A). Y eqpoll succ(k #+ m)}. fa`y <= X & \
+\ (ALL b<a. fa`b <= X --> \
+\ (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 (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 (assume_tac 5);
+by (eresolve_tac [add_succ RS subst] 5);
+by (assume_tac 1);
+by (eresolve_tac [nat_succI] 1);
+by (assume_tac 1);
+by (resolve_tac [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 (hyp_subst_tac 1);
+by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac);
+val ex_next_set = result();
+
+(* ********************************************************************** *)
+(* Lemma ex_next_Ord states that for any successor *)
+(* ordinal there is a number of the set satisfying certain properties *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+\ Card(a); ~ Finite(a); A eqpoll a; \
+\ k : nat; m : nat; y<a; \
+\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
+\ f : bij(a, {Y: Pow(A). Y eqpoll succ(k #+ m)}); \
+\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \
+\ ==> 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 (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
+ THEN REPEAT (ares_tac [Card_is_Ord] 1));
+val ex_next_Ord = result();
+
+goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)";
+by (fast_tac (AC_cs addSEs [singletonE]) 1);
+val ex1_in_Un_sing = result();
+
+(* ********************************************************************** *)
+(* Lemma simplifying assumptions *)
+(* ********************************************************************** *)
+
+goal thy "!!j. [| ALL x<a. x<j | (EX xa:F(j). P(x, xa)) \
+\ --> (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X; \
+\ L : X; P(j, L) & (ALL x<a. P(x, L) --> (ALL xa:F(j). ~P(x, xa))) |] \
+\ ==> 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 (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 (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 (fast_tac AC_cs 1);
+by (fast_tac AC_cs 1);
+by (eresolve_tac [bexE] 1);
+by (eresolve_tac [UnE] 1);
+by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1);
+by (fast_tac AC_cs 1);
+val lemma8 = result();
+
+(* ********************************************************************** *)
+(* The main part of the proof: inductive proof of the property of T_gamma *)
+(* lemma main_induct *)
+(* ********************************************************************** *)
+
+goal thy
+ "!!a. [| b < a; f : bij(a, {Y: Pow(A) . Y eqpoll succ(k #+ m)}); \
+\ fa : bij(a, {Y: Pow(A) . Y eqpoll succ(k)}); \
+\ ~Finite(a); Card(a); A eqpoll a; k : nat; m : nat |] \
+\ ==> 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 (eresolve_tac [lt_Ord RS trans_induct] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [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 (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 (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 (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));
+by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1));
+val main_induct = result();
+
+(* ********************************************************************** *)
+(* Lemma to simplify the inductive proof *)
+(* - the disired property is a consequence of the inductive assumption *)
+(* ********************************************************************** *)
+
+val [prem1, prem2, prem3, prem4] = goal thy
+ "[| (!!b. b<a ==> F(b) <= S & (ALL x<a. (x<b | (EX Y:F(b). f`x <= Y)) \
+\ --> (EX! Y. Y : F(b) & f`x <= Y))); \
+\ 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 (fast_tac AC_cs 1);
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [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 (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
+by (eresolve_tac [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 (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));
+by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2));
+by (fast_tac AC_cs 2);
+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 (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 (REPEAT (fast_tac AC_cs 1));
+val lemma_simp_induct = result();
+
+(* ********************************************************************** *)
+(* The target theorem *)
+(* ********************************************************************** *)
+
+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 (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)));
+by (forward_tac [WO2_imp_ex_Card] 1);
+by (REPEAT (eresolve_tac [exE,conjE] 1));
+by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
+ 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 (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 (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
+ THEN REPEAT (ares_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1));
+qed "WO2_AC16";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO2_AC16.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+WO2_AC16 = AC_Equiv + recfunAC16 + AC16_lemmas + Cardinal_aux
--- a/src/ZF/AC/WO_AC.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO_AC.ML Tue Jul 25 17:31:53 1995 +0200
@@ -19,4 +19,4 @@
goal thy "!!A. well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)";
by (fast_tac (AC_cs addSEs [well_ord_subset RS ex_choice_fun]) 1);
-val ex_choice_fun_Pow = result();
\ No newline at end of file
+val ex_choice_fun_Pow = result();
--- a/src/ZF/AC/WO_AC.thy Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/WO_AC.thy Tue Jul 25 17:31:53 1995 +0200
@@ -1,2 +1,3 @@
(*Dummy theory to document dependencies *)
+
WO_AC = Order + first
--- a/src/ZF/AC/first.ML Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/first.ML Tue Jul 25 17:31:53 1995 +0200
@@ -11,18 +11,6 @@
by (fast_tac AC_cs 1);
val first_is_elem = result();
-goalw thy [well_ord_def, wf_on_def, wf_def, exists_first_def, first_def]
- "!!r. well_ord(A,r) ==> ALL B. (B<=A & B~=0) --> exists_first(B,r)";
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
-by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
-by (contr_tac 1);
-by (eresolve_tac [bexE] 1);
-by (resolve_tac [bexI] 1 THEN (atac 2));
-by (rewrite_goals_tac [tot_ord_def, linear_def]);
-by (fast_tac ZF_cs 1);
-val well_ord_imp_ex_first = result();
-
goalw thy [well_ord_def, wf_on_def, wf_def, first_def]
"!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
@@ -35,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 (atac 1));
+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);
val the_first_in = result();
--- a/src/ZF/AC/first.thy Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/first.thy Tue Jul 25 17:31:53 1995 +0200
@@ -10,14 +10,10 @@
consts
first :: "[i, i, i] => o"
- exists_first :: "[i, i] => o"
defs
- first_def "first(u, X, R)
- == u:X & (ALL v:X. v~=u --> <u,v> : R)"
-
- exists_first_def "exists_first(X,R)
- == EX u:X. first(u, X, R)"
+ first_def "first(u, X, R)
+ == u:X & (ALL v:X. v~=u --> <u,v> : R)"
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/recfunAC16.ML Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,65 @@
+(* Title: ZF/AC/recfunAC16.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Properties of the recursive definition used in the proof of WO2 ==> AC16
+*)
+
+open recfunAC16;
+
+(* ********************************************************************** *)
+(* Basic properties of recfunAC16 *)
+(* ********************************************************************** *)
+
+goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0";
+by (resolve_tac [transrec2_0] 1);
+val recfunAC16_0 = result();
+
+goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \
+\ if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y, recfunAC16(f,fa,i,a), \
+\ 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);
+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);
+val recfunAC16_Limit = result();
+
+(* ********************************************************************** *)
+(* Monotonicity of transrec2 *)
+(* ********************************************************************** *)
+
+val [prem1, prem2] = goal thy
+ "[| !!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 (fast_tac lt_cs 1);
+by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1);
+by (fast_tac (FOL_cs addSIs [succI1, prem1]
+ addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1);
+by (fast_tac (AC_cs addIs [OUN_I, ltI]
+ addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl,
+ transrec2_Limit RS ssubst]) 1);
+val transrec2_mono_lemma = result();
+
+val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \
+\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)";
+by (resolve_tac [prem2 RS leE] 1);
+by (resolve_tac [transrec2_mono_lemma RS impE] 1);
+by (TRYALL (fast_tac (AC_cs addSIs [prem1, prem2, lt_Ord2])));
+val transrec2_mono = result();
+
+(* ********************************************************************** *)
+(* Monotonicity of recfunAC16 *)
+(* ********************************************************************** *)
+
+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 (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1));
+val recfunAC16_mono = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/recfunAC16.thy Tue Jul 25 17:31:53 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/recfunAC16.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+A recursive definition used in the proof of WO2 ==> AC16
+*)
+
+recfunAC16 = Transrec2 + Cardinal +
+
+consts
+
+ recfunAC16 :: "[i, i, i, i] => i"
+
+defs
+
+ recfunAC16_def
+ "recfunAC16(f,fa,i,a) ==
+ transrec2(i, 0,
+ %g r. if(EX y:r. fa`g <= y, r,
+ r Un {f`(LEAST i. fa`g <= f`i &
+ (ALL b<a. (fa`b <= f`i --> (ALL t:r. ~ fa`b <= t))))}))"
+
+end