--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC0_AC1.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/AC0_AC1.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+AC0 is equivalent to AC1
+AC0 comes from Suppes, AC1 from Rubin & Rubin
+*)
+
+goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}";
+by (fast_tac AC_cs 1);
+val subset_Pow_Union = result();
+
+goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
+by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1);
+val lemma1 = result();
+
+val prems = goalw thy AC_defs "!!Z. AC0 ==> AC1";
+by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1);
+result();
+
+val prems = goalw thy AC_defs "!!Z. AC1 ==> AC0";
+by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC10_AC15.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,275 @@
+(* Title: ZF/AC/AC10_AC15.ML
+ ID: $Id$
+ Author: Krzysztof Grabczewski
+
+The proofs needed to state that AC10, ..., AC15 are equivalent to the rest.
+We need the following:
+
+WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6
+
+In order to add the formulations AC13 and AC14 we need:
+
+AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15
+
+or
+
+AC1 ==> AC13(1); AC13(m) ==> AC13(n); AC13(n) ==> AC14 ==> AC15
+
+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
+Rubin & Rubin do.
+*)
+
+(* ********************************************************************** *)
+(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *)
+(* or AC15 *)
+(* - cons_times_nat_not_Finite *)
+(* - 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);
+by (fast_tac (AC_cs addSIs [snd_conv, lam_injective]) 1);
+val lepoll_Sigma = result();
+
+goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)";
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [RepFunE] 1);
+by (hyp_subst_tac 1);
+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));
+by (fast_tac AC_cs 1);
+val cons_times_nat_not_Finite = result();
+
+goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A";
+by (fast_tac ZF_cs 1);
+val lemma1 = result();
+
+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 (dres_inst_tac [("A","B Int C")] not_emptyI 1);
+by (fast_tac ZF_cs 1);
+val lemma2 = result();
+
+goalw thy [sets_of_size_between_def]
+ "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \
+\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \
+\ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \
+\ 0:u & 2 lepoll u & u lepoll n";
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [ballE] 1);
+by (fast_tac ZF_cs 2);
+by (REPEAT (eresolve_tac [conjE] 1));
+by (dresolve_tac [consI1 RSN (2, lemma1)] 1);
+by (eresolve_tac [bexE] 1);
+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)));
+val lemma3 = result();
+
+goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i";
+by (eresolve_tac [exE] 1);
+by (res_inst_tac
+ [("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 (fast_tac (AC_cs addIs [LeastI2]
+ addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
+by (eresolve_tac [RepFunE] 1);
+by (resolve_tac [LeastI2] 1);
+by (fast_tac AC_cs 1);
+by (fast_tac (AC_cs addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
+by (fast_tac (AC_cs addEs [sym, left_inverse RS ssubst]) 1);
+val lemma4 = result();
+
+goal thy "!!A. [| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \
+\ u(B) lepoll succ(n) |] \
+\ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \
+\ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \
+\ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n";
+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]
+ addEs [lepoll_trans RS succ_lepoll_natE, ssubst]
+ addSIs [notI, lepoll_refl, nat_0I]) 1);
+by (resolve_tac [conjI] 1);
+by (fast_tac (ZF_cs addSIs [fst_type] addSEs [consE]) 1);
+by (fast_tac (ZF_cs addSEs [equalityE,
+ Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1);
+val lemma5 = result();
+
+goal thy "!!A. [| EX f. ALL B:{cons(0, x*nat). x:A}. \
+\ pairwise_disjoint(f`B) & \
+\ 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]
+ addSIs [exI, ballI, lemma5]) 1);
+val ex_fun_AC13_AC15 = result();
+
+(* ********************************************************************** *)
+(* The target proofs *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC10(n) ==> AC11 *)
+(* ********************************************************************** *)
+
+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();
+
+(* ********************************************************************** *)
+(* AC11 ==> AC12 *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!! Z. AC11 ==> AC12";
+by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1);
+result();
+
+(* ********************************************************************** *)
+(* AC12 ==> AC15 *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!Z. AC12 ==> AC15";
+by (safe_tac ZF_cs);
+by (eresolve_tac [allE] 1);
+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();
+
+(* ********************************************************************** *)
+(* AC15 ==> WO6 *)
+(* ********************************************************************** *)
+
+(* in a separate file *)
+
+(* ********************************************************************** *)
+(* The proof needed in the first case, not in the second *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC10(n) ==> AC13(n-1) if 2 le n *)
+(* *)
+(* Because of the change to the formal definition of AC10(n) we prove *)
+(* the following obviously equivalent theorem : *)
+(* AC10(n) implies AC13(n) for (1 le n) *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)";
+by (safe_tac ZF_cs);
+by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
+ ex_fun_AC13_AC15]) 1);
+val AC10_imp_AC13 = result();
+
+(* ********************************************************************** *)
+(* The proofs needed in the second case, not in the first *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC1 ==> AC13(1) *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!Z. AC1 ==> AC13(1)";
+by (resolve_tac [allI] 1);
+by (eresolve_tac [allE] 1);
+by (resolve_tac [impI] 1);
+by (mp_tac 1);
+by (eresolve_tac [exE] 1);
+by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1);
+by (asm_full_simp_tac (AC_ss addsimps
+ [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
+ singletonI RS not_emptyI]) 1);
+by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1);
+result();
+
+(* ********************************************************************** *)
+(* 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 (fast_tac (ZF_cs addSEs [lepoll_trans]) 1);
+result();
+
+(* ********************************************************************** *)
+(* The proofs necessary for both cases *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC13(n) ==> AC14 if 1 <= n *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC13(n) |] ==> AC14";
+by (fast_tac (FOL_cs addIs [bexI]) 1);
+result();
+
+(* ********************************************************************** *)
+(* AC14 ==> AC15 *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!Z. AC14 ==> AC15";
+by (fast_tac ZF_cs 1);
+result();
+
+(* ********************************************************************** *)
+(* The redundant proofs; however cited by Rubin & Rubin *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC13(1) ==> AC1 *)
+(* ********************************************************************** *)
+
+goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}";
+by (fast_tac (AC_cs addSEs [not_emptyE, lepoll_1_is_sing]) 1);
+val lemma_aux = result();
+
+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 (REPEAT (eresolve_tac [conjE] 1));
+by (eresolve_tac [lemma_aux RS exE] 1 THEN (atac 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();
+
+(* ********************************************************************** *)
+(* AC11 ==> AC14 *)
+(* ********************************************************************** *)
+
+goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14";
+by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC15_WO6.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,46 @@
+(* Title: ZF/AC/AC15_WO6.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of AC1 ==> WO2
+*)
+
+open AC15_WO6;
+
+goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
+by (fast_tac (AC_cs addSIs [equalityI, ltI] addSDs [ltD]) 1);
+val OUN_eq_UN = result();
+
+val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \
+\ (UN i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A";
+by (simp_tac (AC_ss addsimps [Ord_Least RS OUN_eq_UN]) 1);
+by (resolve_tac [equalityI] 1);
+by (fast_tac (AC_cs addSDs [less_Least_subset_x]) 1);
+by (fast_tac (AC_cs addSDs [prem RS bspec]
+ addSIs [f_subsets_imp_UN_HH_eq_x RS (Diff_eq_0_iff RS iffD1)]) 1);
+val lemma1 = result();
+
+val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==> \
+\ ALL x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
+by (resolve_tac [oallI] 1);
+by (dresolve_tac [ltD RS less_Least_subset_x] 1);
+by (forward_tac [HH_subset_imp_eq] 1);
+by (eresolve_tac [ssubst] 1);
+by (fast_tac (AC_cs addIs [prem RS ballE]
+ addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
+val lemma2 = result();
+
+goalw thy [AC15_def, WO6_def] "!!Z. AC15 ==> WO6";
+by (resolve_tac [allI] 1);
+by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (fast_tac ZF_cs 1);
+by (REPEAT (eresolve_tac [bexE,conjE,exE] 1));
+by (resolve_tac [bexI] 1 THEN (assume_tac 2));
+by (resolve_tac [conjI] 1 THEN (assume_tac 1));
+by (res_inst_tac [("x","LEAST i. HH(f,A,i)={A}")] exI 1);
+by (res_inst_tac [("x","lam j: (LEAST i. HH(f,A,i)={A}). HH(f,A,j)")] exI 1);
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC15_WO6.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+AC15_WO6 = HH
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC17_AC1.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,95 @@
+(* Title: ZF/AC/AC17_AC1.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of AC1 ==> AC17
+*)
+
+open AC17_AC1;
+
+(* *********************************************************************** *)
+(* more properties of HH *)
+(* *********************************************************************** *)
+
+goal thy "!!f. [| x - (UN j:LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x}. \
+\ HH(lam X:Pow(x)-{0}. {f`X}, x, j)) = 0; \
+\ f : Pow(x)-{0} -> x |] \
+\ ==> EX r. well_ord(x,r)";
+by (resolve_tac [exI] 1);
+by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj,
+ Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1);
+by (assume_tac 1);
+val UN_eq_imp_well_ord = result();
+
+(* *********************************************************************** *)
+(* theorems closer to the proof *)
+(* *********************************************************************** *)
+
+goalw thy AC_defs "!!Z. ~AC1 ==> \
+\ EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u";
+by (eresolve_tac [swap] 1);
+by (resolve_tac [allI] 1);
+by (eresolve_tac [swap] 1);
+by (res_inst_tac [("x","Union(A)")] exI 1);
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [swap] 1);
+by (resolve_tac [impI] 1);
+by (fast_tac (AC_cs addSIs [restrict_type]) 1);
+val not_AC1_imp_ex = result();
+
+goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u; \
+\ EX f: Pow(x)-{0}->x. \
+\ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \
+\ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \
+\ ==> P";
+by (eresolve_tac [bexE] 1);
+by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1));
+by (eresolve_tac [ex_choice_fun_Pow RS exE] 1);
+by (eresolve_tac [ballE] 1);
+by (fast_tac (FOL_cs addEs [bexE, notE, apply_type]) 1);
+by (eresolve_tac [notE] 1);
+by (resolve_tac [Pi_type] 1 THEN (assume_tac 1));
+by (resolve_tac [apply_type RSN (2, subsetD)] 1 THEN TRYALL assume_tac);
+by (fast_tac AC_cs 1);
+val lemma1 = result();
+
+goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0) \
+\ ==> (lam f: Pow(x)-{0}->x. x - F(f)) \
+\ : (Pow(x) -{0} -> x) -> Pow(x) - {0}";
+by (fast_tac (AC_cs addSIs [lam_type] addIs [equalityI]
+ addSDs [Diff_eq_0_iff RS iffD1]) 1);
+val lemma2 = result();
+
+goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \
+\ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}";
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSDs [equals0D]) 1);
+val lemma3 = result();
+
+goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \
+\ ==> EX f:F. f`Q(f) : Q(f)";
+by (asm_full_simp_tac AC_ss 1);
+val lemma4 = result();
+
+goalw thy [AC17_def] "!!Z. [| AC17; ~ AC1 |] ==> False";
+by (eresolve_tac [not_AC1_imp_ex RS exE] 1);
+by (excluded_middle_tac
+ "EX f: Pow(x)-{0}->x. \
+\ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \
+\ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0" 1);
+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 [lemma4] 1);
+by (eresolve_tac [bexE] 1);
+by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1);
+by (assume_tac 1);
+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();
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC17_AC1.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+AC17_AC1 = HH
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC18_AC19.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,121 @@
+(* Title: ZF/AC/AC18_AC19.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of AC1 ==> AC18 ==> AC19 ==> AC1
+*)
+
+open AC18_AC19;
+
+(* ********************************************************************** *)
+(* AC1 ==> AC18 *)
+(* ********************************************************************** *)
+
+goal thy "!!f. [| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \
+\ ==> (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));
+val PROD_subsets = result();
+
+goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \
+\ (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))";
+by (resolve_tac [subsetI] 1);
+by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (fast_tac (AC_cs addSEs [RepFunE] addSDs [INT_E]
+ addEs [UN_E, sym RS equals0D]) 1);
+by (eresolve_tac [exE] 1);
+by (resolve_tac [UN_I] 1);
+by (fast_tac (AC_cs addSEs [PROD_subsets]) 1);
+by (simp_tac AC_ss 1);
+by (fast_tac (FOL_cs addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
+ addEs [CollectD2] addSIs [INT_I]) 1);
+val lemma_AC18 = result();
+
+val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
+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();
+
+(* ********************************************************************** *)
+(* AC18 ==> AC19 *)
+(* ********************************************************************** *)
+
+val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19";
+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();
+
+(* ********************************************************************** *)
+(* AC19 ==> AC1 *)
+(* ********************************************************************** *)
+
+goalw thy [u_def]
+ "!!A. [| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}";
+by (fast_tac (AC_cs addSIs [not_emptyI, RepFunI]
+ addSEs [not_emptyE, RepFunE]
+ addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1);
+val RepRep_conj = result();
+
+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 [equalityI] 1);
+by (fast_tac AC_cs 1);
+by (resolve_tac [subsetI] 1);
+by (excluded_middle_tac "x=0" 1);
+by (fast_tac AC_cs 1);
+by (fast_tac (AC_cs addEs [notE, subst_elem] addSIs [equalityI]) 1);
+val lemma1_1 = result();
+
+goalw thy [u_def]
+ "!!a. [| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \
+\ ==> f`(u_(a))-{0} : a";
+by (fast_tac (AC_cs addSEs [RepFunI, RepFunE, lemma1_1]
+ addSDs [apply_type]) 1);
+val lemma1_2 = result();
+
+goal thy "!!A. EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)";
+by (eresolve_tac [exE] 1);
+by (res_inst_tac
+ [("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1);
+by (resolve_tac [lam_type] 1);
+by (split_tac [expand_if] 1);
+by (resolve_tac [conjI] 1);
+by (fast_tac AC_cs 1);
+by (fast_tac (AC_cs addSEs [lemma1_2]) 1);
+val lemma1 = result();
+
+goalw thy [u_def] "!!a. a~=0 ==> 0: (UN b:u_(a). b)";
+by (fast_tac (AC_cs addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1);
+val lemma2_1 = result();
+
+goal thy "!!A C. [| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0";
+by (eresolve_tac [not_emptyE] 1);
+by (res_inst_tac [("a","0")] not_emptyI 1);
+by (fast_tac (AC_cs addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1);
+val lemma2 = result();
+
+goal thy "!!F. (UN f:F. P(f)) ~= 0 ==> F ~= 0";
+by (fast_tac (AC_cs addSEs [not_emptyE]) 1);
+val lemma3 = result();
+
+goalw thy AC_defs "!!Z. AC19 ==> AC1";
+by (REPEAT (resolve_tac [allI,impI] 1));
+by (excluded_middle_tac "A=0" 1);
+by (fast_tac (AC_cs addSIs [empty_fun]) 2);
+by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (eresolve_tac [RepRep_conj] 1 THEN (assume_tac 1));
+by (resolve_tac [lemma1] 1);
+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();
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC18_AC19.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,18 @@
+(* Title: ZF/AC/AC18_AC19.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Additional definition used in the proof AC19 ==> AC1 which is a part
+of the chain AC1 ==> AC18 ==> AC19 ==> AC1
+*)
+
+AC18_AC19 = AC_Equiv +
+
+consts
+ u_ :: "i => i"
+
+defs
+
+ u_def "u_(a) == {c Un {0}. c:a}"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC1_AC17.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,25 @@
+(* Title: ZF/AC/AC1_AC17.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of AC1 ==> AC17
+*)
+
+goal thy "!!f. f : (PROD X:Pow(A) - {0}. X) ==> f : (Pow(A) - {0} -> A)";
+by (resolve_tac [Pi_type] 1 THEN (assume_tac 1));
+by (dresolve_tac [apply_type] 1 THEN (assume_tac 1));
+by (fast_tac AC_cs 1);
+val lemma1 = result();
+
+goalw thy AC_defs "!!Z. AC1 ==> AC17";
+by (resolve_tac [allI] 1);
+by (resolve_tac [ballI] 1);
+by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (fast_tac AC_cs 1);
+by (eresolve_tac [exE] 1);
+by (resolve_tac [bexI] 1);
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC1_WO2.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/AC1_WO2.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of AC1 ==> WO2
+*)
+
+open AC1_WO2;
+
+val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \
+\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})";
+by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
+by (resolve_tac [f_subsets_imp_UN_HH_eq_x] 1);
+by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
+by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1);
+by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1);
+val lemma1 = uresult();
+
+goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2";
+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();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC1_WO2.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+AC1_WO2 = HH
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC2_AC6.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,201 @@
+(* Title: ZF/AC/AC2_AC6.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proofs needed to state that each of AC2, AC3, ..., AC6 is equivallent
+to AC0 and AC1. Namely:
+AC1 ==> AC2 ==> AC1
+AC1 ==> AC4 ==> AC3 ==> AC1
+AC4 ==> AC5 ==> AC4
+AC1 <-> AC6
+*)
+
+(* ********************************************************************** *)
+(* AC1 ==> AC2 *)
+(* ********************************************************************** *)
+
+goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |] \
+\ ==> {f`B} <= B Int {f`C. C:A}";
+by (fast_tac (AC_cs addSEs [singletonE, apply_type, RepFunI]) 1);
+val lemma1 = result();
+
+goalw thy [pairwise_disjoint_def]
+ "!!A. [| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C";
+by (fast_tac (ZF_cs addSEs [equals0D]) 1);
+val lemma2 = result();
+
+goalw thy AC_defs "!!Z. AC1 ==> AC2";
+by (resolve_tac [allI] 1);
+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 (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC2 ==> AC1 *)
+(* ********************************************************************** *)
+
+goal thy "!!A. 0~:A ==> 0 ~: {B*{B}. B:A}";
+by (fast_tac (AC_cs addSDs [sym RS (Sigma_empty_iff RS iffD1)]
+ addSEs [RepFunE, equals0D]) 1);
+val lemma1 = result();
+
+goal thy "!!A. [| X*{X} Int C = {y}; X:A |] \
+\ ==> (THE y. X*{X} Int C = {y}): X*A";
+by (resolve_tac [subst_elem] 1);
+by (fast_tac (ZF_cs addSIs [the_equality]
+ addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
+by (fast_tac (AC_cs addSEs [equalityE, make_elim singleton_subsetD]) 1);
+val lemma2 = result();
+
+goal thy "!!A. ALL D:{E*{E}. E:A}. EX y. D Int C = {y} \
+\ ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) : \
+\ (PROD X:A. X) ";
+by (fast_tac (FOL_cs addSEs [lemma2]
+ addSIs [lam_type, RepFunI, fst_type]
+ addSDs [bspec]) 1);
+val lemma3 = result();
+
+goalw thy (AC_defs@AC_aux_defs) "!!Z. AC2 ==> AC1";
+by (REPEAT (resolve_tac [allI, impI] 1));
+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();
+
+
+(* ********************************************************************** *)
+(* AC1 ==> AC4 *)
+(* ********************************************************************** *)
+
+goal thy "!!R. 0 ~: {R``{x}. x:domain(R)}";
+by (fast_tac (AC_cs addSEs [RepFunE, domainE, sym RS equals0D]) 1);
+val lemma = result();
+
+goalw thy AC_defs "!!Z. AC1 ==> AC4";
+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();
+
+
+(* ********************************************************************** *)
+(* AC4 ==> AC3 *)
+(* ********************************************************************** *)
+
+goal thy "!!f. f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)";
+by (fast_tac (ZF_cs addSDs [apply_type] addSEs [UN_E, singletonE]) 1);
+val lemma1 = result();
+
+goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
+by (fast_tac (ZF_cs addIs [equalityI]
+ addSEs [not_emptyE]
+ addSIs [singletonI, not_emptyI]
+ addDs [range_type]) 1);
+val lemma2 = result();
+
+goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
+by (fast_tac (ZF_cs addIs [equalityI] addSIs [singletonI, UN_I] addSEs [singletonE, UN_E]) 1);
+val lemma3 = result();
+
+goalw thy AC_defs "!!Z. AC4 ==> AC3";
+by (REPEAT (resolve_tac [allI,ballI] 1));
+by (REPEAT (eresolve_tac [allE,impE] 1));
+by (eresolve_tac [lemma1] 1);
+by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3]
+ addcongs [Pi_cong]) 1);
+result();
+
+(* ********************************************************************** *)
+(* AC3 ==> AC1 *)
+(* ********************************************************************** *)
+
+goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
+by (asm_full_simp_tac (AC_ss addsimps [id_def] addcongs [Pi_cong]) 1);
+by (res_inst_tac [("b","A")] subst_context 1);
+by (fast_tac (AC_cs addSIs [equalityI]) 1);
+val lemma = result();
+
+goalw thy AC_defs "!!Z. AC3 ==> AC1";
+by (REPEAT (resolve_tac [allI, impI] 1));
+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();
+
+(* ********************************************************************** *)
+(* AC4 ==> AC5 *)
+(* ********************************************************************** *)
+
+goalw thy (range_def::AC_defs) "!!Z. AC4 ==> AC5";
+by (REPEAT (resolve_tac [allI,ballI] 1));
+by (REPEAT (eresolve_tac [allE,impE] 1));
+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 (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 (eresolve_tac [domainE] 1);
+by (forward_tac [range_type] 1 THEN (atac 1));
+by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
+(* ********************************************************************** *)
+
+goal thy "!!A. R <= A*B ==> (lam x:R. fst(x)) : R -> A";
+by (fast_tac (ZF_cs addSIs [lam_type, fst_type]) 1);
+val lemma1 = result();
+
+goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
+by (resolve_tac [equalityI] 1);
+by (fast_tac (AC_cs addSEs [lamE, Pair_inject]
+ addEs [subst_elem]
+ addSDs [converseD, Pair_fst_snd_eq]) 1);
+by (resolve_tac [subsetI] 1);
+by (eresolve_tac [domainE] 1);
+by (resolve_tac [domainI] 1);
+by (fast_tac (AC_cs addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1);
+val lemma2 = result();
+
+goal thy "!!A. [| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)";
+by (eresolve_tac [bexE] 1);
+by (forward_tac [domain_of_fun] 1);
+by (fast_tac ZF_cs 1);
+val lemma3 = result();
+
+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 (resolve_tac [imageI] 1);
+by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
+ THEN (REPEAT (atac 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 (fast_tac (AC_cs addSEs [lemma4]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC1 <-> AC6 *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "AC1 <-> AC6";
+by (fast_tac (ZF_cs addDs [equals0D] addSEs [not_emptyE]) 1);
+result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/AC7_AC9.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,237 @@
+(* Title: ZF/AC/AC7-AC9.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
+instances of AC.
+*)
+
+(* ********************************************************************** *)
+(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *)
+(* - Sigma_fun_space_not0 *)
+(* - all_eqpoll_imp_pair_eqpoll *)
+(* - Sigma_fun_space_eqpoll *)
+(* ********************************************************************** *)
+
+goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
+by (fast_tac ZF_cs 1);
+val mem_not_eq_not_mem = result();
+
+goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
+by (fast_tac (ZF_cs addSDs [Sigma_empty_iff RS iffD1]
+ addDs [fun_space_emptyD, mem_not_eq_not_mem]
+ addEs [equals0D]
+ addSIs [equals0I,UnionI]) 1);
+val Sigma_fun_space_not0 = result();
+
+goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
+by (REPEAT (resolve_tac [ballI] 1));
+by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
+ THEN REPEAT (atac 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 (asm_full_simp_tac ZF_ss 1);
+val if_eqE1 = result();
+
+goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
+\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
+by (resolve_tac [ballI] 1);
+by (resolve_tac [impI] 1);
+by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (asm_full_simp_tac ZF_ss 1);
+val if_eqE2 = result();
+
+goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
+by (fast_tac (ZF_cs addDs [subsetD]
+ addSIs [lamI]
+ addEs [equalityE, lamE]) 1);
+val lam_eqE = result();
+
+goalw thy [inj_def]
+ "!!A. C:A ==> (lam g:(nat->Union(A))*C. \
+\ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \
+\ : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
+by (resolve_tac [CollectI] 1);
+by (fast_tac (ZF_cs addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
+ fst_type,diff_type,nat_succI,nat_0I]) 1);
+by (REPEAT (resolve_tac [ballI, impI] 1));
+by (asm_full_simp_tac ZF_ss 1);
+by (REPEAT (eresolve_tac [SigmaE] 1));
+by (REPEAT (hyp_subst_tac 1));
+by (asm_full_simp_tac ZF_ss 1);
+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 (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);
+val lemma = result();
+
+goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
+by (resolve_tac [eqpollI] 1);
+by (fast_tac (ZF_cs addSEs [prod_lepoll_self, not_sym RS not_emptyE,
+ subst_elem] addEs [swap]) 2);
+by (rewrite_goals_tac [lepoll_def]);
+by (fast_tac (ZF_cs addSIs [lemma]) 1);
+val Sigma_fun_space_eqpoll = result();
+
+
+(* ********************************************************************** *)
+(* AC6 ==> AC7 *)
+(* ********************************************************************** *)
+
+goalw thy AC_defs "!!Z. AC6 ==> AC7";
+by (fast_tac ZF_cs 1);
+result();
+
+(* ********************************************************************** *)
+(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *)
+(* The case of the empty family of sets added in order to complete *)
+(* the proof. *)
+(* ********************************************************************** *)
+
+goal thy "!!y. y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)";
+by (fast_tac (ZF_cs addSIs [lam_type, snd_type, apply_type]) 1);
+val lemma1_1 = result();
+
+goal thy "!!A. y: (PROD B:{Y*C. C:A}. B) \
+\ ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
+by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1);
+val lemma1_2 = result();
+
+goal thy "!!A. (PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 \
+\ ==> (PROD B:A. B) ~= 0";
+by (fast_tac (ZF_cs addSIs [equals0I,lemma1_1, lemma1_2]
+ addSEs [equals0D]) 1);
+val lemma1 = result();
+
+goal thy "!!A. 0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
+by (fast_tac (ZF_cs addEs [RepFunE,
+ Sigma_fun_space_not0 RS not_sym RS notE]) 1);
+val lemma2 = result();
+
+goalw thy AC_defs "!!Z. AC7 ==> AC6";
+by (resolve_tac [allI] 1);
+by (resolve_tac [impI] 1);
+by (excluded_middle_tac "A=0" 1);
+by (fast_tac (ZF_cs addSIs [not_emptyI, empty_fun]) 2);
+by (resolve_tac [lemma1] 1);
+by (eresolve_tac [allE] 1);
+by (eresolve_tac [impE] 1 THEN (atac 2));
+by (fast_tac (AC_cs addSEs [RepFunE]
+ addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
+ Sigma_fun_space_eqpoll]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC1 ==> AC8 *)
+(* ********************************************************************** *)
+
+goalw thy [eqpoll_def]
+ "!!A. ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \
+\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
+by (resolve_tac [notI] 1);
+by (eresolve_tac [RepFunE] 1);
+by (dresolve_tac [bspec] 1 THEN (atac 1));
+by (REPEAT (eresolve_tac [exE,conjE] 1));
+by (hyp_subst_tac 1);
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSEs [sym RS equals0D]) 1);
+val lemma1 = result();
+
+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 (fast_tac (AC_cs addSEs [apply_type]) 1);
+val lemma2 = result();
+
+goalw thy AC_defs "!!Z. AC1 ==> AC8";
+by (resolve_tac [allI] 1);
+by (eresolve_tac [allE] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [impE] 1);
+by (eresolve_tac [lemma1] 1);
+by (fast_tac (AC_cs addSEs [lemma2]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC8 ==> AC9 *)
+(* - this proof replaces the following two from Rubin & Rubin: *)
+(* AC8 ==> AC1 and AC1 ==> AC9 *)
+(* ********************************************************************** *)
+
+goal thy "!!A. ALL B1:A. ALL B2:A. B1 eqpoll B2 ==> \
+\ ALL B:A*A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2";
+by (fast_tac ZF_cs 1);
+val lemma1 = result();
+
+goal thy "!!f. f:bij(fst(<a,b>),snd(<a,b>)) ==> f:bij(a,b)";
+by (asm_full_simp_tac AC_ss 1);
+val lemma2 = result();
+
+goalw thy AC_defs "!!Z. AC8 ==> AC9";
+by (resolve_tac [allI] 1);
+by (resolve_tac [impI] 1);
+by (eresolve_tac [allE] 1);
+by (eresolve_tac [impE] 1);
+by (eresolve_tac [lemma1] 1);
+by (fast_tac (AC_cs addSEs [lemma2]) 1);
+result();
+
+
+(* ********************************************************************** *)
+(* AC9 ==> AC1 *)
+(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
+(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *)
+(* (x * y) Un {0} when y is a set of total functions acting from nat to *)
+(* Union(A) -- therefore we have used the set (y * nat) instead of y. *)
+(* ********************************************************************** *)
+
+(* Rules nedded to prove lemma1 *)
+val snd_lepoll_SigmaI = prod_lepoll_self RS
+ ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
+val lemma1_cs = FOL_cs addSEs [UnE, RepFunE]
+ addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
+ nat_cons_eqpoll RS eqpoll_trans]
+ addEs [Sigma_fun_space_not0 RS not_emptyE]
+ addIs [snd_lepoll_SigmaI, eqpoll_refl RSN
+ (2, prod_eqpoll_cong), Sigma_fun_space_eqpoll];
+
+goal thy "!!A. [| 0~:A; A~=0 |] \
+\ ==> ALL B1: ({((nat->Union(A))*B)*nat. B:A} \
+\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
+\ ALL B2: ({((nat->Union(A))*B)*nat. B:A} \
+\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
+\ B1 eqpoll B2";
+by (fast_tac lemma1_cs 1);
+val lemma1 = result();
+
+goal thy "!!A. ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}. \
+\ ALL B2:{(F*B)*N. B:A} \
+\ Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2) \
+\ ==> (lam B:A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) : \
+\ (PROD X:A. X)";
+by (resolve_tac [lam_type] 1);
+by (resolve_tac [snd_type] 1);
+by (resolve_tac [fst_type] 1);
+by (resolve_tac [consI1 RSN (2, apply_type)] 1);
+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";
+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 (fast_tac (AC_cs addSEs [lemma2]) 1);
+result();
\ No newline at end of file
--- a/src/ZF/AC/AC_Equiv.ML Mon May 15 09:35:07 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Thu May 18 11:51:23 1995 +0200
@@ -15,7 +15,10 @@
AC17_def, AC18_def, AC19_def];
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
-
+
+val AC_cs = OrdQuant_cs;
+val AC_ss = OrdQuant_ss;
+
(* ******************************************** *)
(* Theorems analogous to ones presented in "ZF/Ordinal.ML" *)
@@ -47,15 +50,13 @@
by (asm_simp_tac (ZF_ss addsimps prems) 1);
val def_imp_iff = result();
-val prems = goal ZF.thy "(A == B) ==> P(A) <-> P(B)";
-by (asm_simp_tac (ZF_ss addsimps prems) 1);
-val def_imp_iff_P = result();
+val prems = goal ZF.thy "(A == B) ==> A = B";
+by (simp_tac (ZF_ss addsimps prems) 1);
+val def_imp_eq = result();
-(* used only in lemmas4-7.ML *)
-(*Note modified statement and proof*)
-goal ZF.thy "!!X. X~=0 ==> (A->X)~=0";
-by (fast_tac (ZF_cs addSIs [equals0I,lam_type] addSEs [equals0D]) 1);
-val fun_space_not0I = result();
+goal thy "!!X. (A->X)=0 ==> X=0";
+by (fast_tac (ZF_cs addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1);
+val fun_space_emptyD = result();
(* used only in WO1_DC.ML *)
(*Note simpler proof*)
@@ -109,3 +110,31 @@
"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
val Inf_Card_is_InfCard = result();
+
+goal thy "(THE z. {x}={z}) = x";
+by (fast_tac (AC_cs addSIs [the_equality]
+ addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
+val the_element = result();
+
+goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})";
+by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1);
+by (TRYALL (eresolve_tac [RepFunI, RepFunE]));
+by (REPEAT (asm_full_simp_tac (AC_ss addsimps [the_element]) 1));
+val lam_sing_bij = result();
+
+val [major,minor] = goal thy
+ "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)";
+by (fast_tac (AC_cs addSIs [major RS Pi_type, minor RS subsetD,
+ major RS apply_type]) 1);
+val Pi_weaken_type = result();
+
+val [major, minor] = goalw thy [inj_def]
+ "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)";
+by (fast_tac (AC_cs addSEs [minor]
+ addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
+val inj_strengthen_type = result();
+
+goal thy "A*B=0 <-> A=0 | B=0";
+by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1);
+val Sigma_empty_iff = result();
+
--- a/src/ZF/AC/AC_Equiv.thy Mon May 15 09:35:07 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Thu May 18 11:51:23 1995 +0200
@@ -8,11 +8,11 @@
Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972.
Some Isabelle proofs of equivalences of these axioms are formalizations of
-proofs presented by Rubin. The others are based on Rubin's proofs, but
-slightly changed.
+proofs presented by the Rubins. The others are based on the Rubins' proofs,
+but slightly changed.
*)
-AC_Equiv = CardinalArith + Univ + Transrec2 +
+AC_Equiv = CardinalArith + Univ + OrdQuant +
consts
@@ -26,19 +26,11 @@
AC10, AC13 :: "i => o"
AC16 :: "[i, i] => o"
AC18 :: "prop" ("AC18")
-
-(* Auxiliary definitions used in theorems *)
- first :: "[i, i, i] => o"
- exists_first :: "[i, i] => o"
+
+(* Auxiliary definitions used in definitions *)
pairwise_disjoint :: "i => o"
sets_of_size_between :: "[i, i, i] => o"
- GG :: "[i, i, i] => i"
- GG2 :: "[i, i, i] => i"
- HH :: "[i, i, i] => i"
-
- recfunAC16 :: "[i, i, i, i] => i"
-
defs
(* Well Ordering Theorems *)
@@ -60,7 +52,7 @@
WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) --> \
\ well_ord(A,converse(R)))"
- WO8_def "WO8 == ALL A. (0~:A --> (EX f. f : (PROD X:A. X))) --> \
+ WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) --> \
\ (EX R. well_ord(A,R))"
(* Axioms of Choice *)
@@ -120,15 +112,9 @@
\ (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \
-\ (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))"
-
-(* Auxiliary definitions used in theorems *)
+\ (UN f:(PROD B:A. B). INT a:A. f`a))"
- 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)"
+(* Auxiliary definitions used in the above definitions *)
pairwise_disjoint_def "pairwise_disjoint(A) \
\ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
@@ -136,22 +122,4 @@
sets_of_size_between_def "sets_of_size_between(A,m,n) \
\ == ALL B:A. m lepoll B & B lepoll n"
-(* Auxiliary definitions used in proofs *)
-
- GG_def "GG(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
-\ if(z=0, x, f`z))`(x - {r`c. c:b}))"
-
- GG2_def "GG2(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
-\ if(z=0, {x}, f`z))`(x - Union({r`c. c:b})))"
-
- HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \
-\ if(z=0|f`z~:z, x, f`z))`(x - {r`c. c:b}))"
-
- 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/HH.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,230 @@
+(* Title: ZF/AC/HH.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Some properties of the recursive definition of HH used in the proofs of
+ AC17 ==> AC1
+ AC1 ==> WO2
+ AC15 ==> WO6
+*)
+
+open HH;
+
+(* ********************************************************************** *)
+(* Lemmas useful in each of the three proofs *)
+(* ********************************************************************** *)
+
+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)))";
+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 (split_tac [expand_if] 1);
+by (fast_tac ZF_cs 1);
+val HH_values = result();
+
+goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
+by (fast_tac (AC_cs addSIs [equalityI]) 1);
+val subset_imp_Diff_eq = result();
+
+goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
+by (eresolve_tac [ltE] 1);
+by (dres_inst_tac [("x","c")] Ord_linear 1);
+by (fast_tac (AC_cs addEs [Ord_in_Ord]) 1);
+by (fast_tac (AC_cs addSIs [ltI] addIs [Ord_in_Ord]) 1);
+val Ord_DiffE = result();
+
+val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
+by (asm_full_simp_tac (AC_ss addsimps prems) 1);
+by (fast_tac (AC_cs addSIs [equalityI] addSDs [prem]
+ addSEs [RepFunE, mem_irrefl]) 1);
+val Diff_UN_eq_self = result();
+
+goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \
+\ ==> HH(f,x,a) = HH(f,x,a1)";
+by (resolve_tac [HH_def_satisfies_eq RS
+ (HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1);
+by (eresolve_tac [subst_context] 1);
+val HH_eq = result();
+
+goal thy "!!a. [| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}";
+by (res_inst_tac [("P","b<a")] impE 1 THEN REPEAT (assume_tac 2));
+by (eresolve_tac [lt_Ord2 RS trans_induct] 1);
+by (resolve_tac [impI] 1);
+by (resolve_tac [HH_eq RS trans] 1 THEN (assume_tac 2));
+by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1
+ THEN (assume_tac 1));
+by (res_inst_tac [("t","%z. z-?X")] subst_context 1);
+by (resolve_tac [Diff_UN_eq_self] 1);
+by (dresolve_tac [Ord_DiffE] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addEs [ltE]) 1);
+val HH_is_x_gt_too = result();
+
+goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}";
+by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
+by (dresolve_tac [HH_is_x_gt_too] 1 THEN (assume_tac 1));
+by (dresolve_tac [subst] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
+val HH_subset_x_lt_too = result();
+
+goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \
+\ ==> 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 (dresolve_tac [expand_if RS iffD1] 1);
+by (split_tac [expand_if] 1);
+by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
+val HH_subset_x_imp_subset_Diff_UN = result();
+
+goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P";
+by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1));
+by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1);
+by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addSIs [singleton_iff RS iffD2, equals0I]) 1);
+val HH_eq_arg_lt = result();
+
+goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \
+\ Ord(v); Ord(w) |] ==> v=w";
+by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac);
+by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2
+ THEN REPEAT (assume_tac 2));
+by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1));
+by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1);
+val HH_eq_imp_arg_eq = result();
+
+goalw thy [lepoll_def, inj_def]
+ "!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}";
+by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1);
+by (asm_simp_tac AC_ss 1);
+by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too]
+ addSIs [lam_type, ballI, ltI] addIs [bexI]) 1);
+val HH_subset_x_imp_lepoll = result();
+
+goal thy "HH(f, x, Hartog(Pow(x)-{0})) = {x}";
+by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 2));
+by (fast_tac (FOL_cs addSDs [HH_subset_x_imp_lepoll]
+ addSIs [Ord_Hartog] addSEs [HartogE]) 1);
+val HH_Hartog_is_x = result();
+
+goal thy "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}";
+by (fast_tac (AC_cs addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1);
+val HH_Least_eq_x = result();
+
+goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}";
+by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
+by (resolve_tac [less_LeastE] 1);
+by (eresolve_tac [Ord_Least RSN (2, ltI)] 2);
+by (assume_tac 1);
+val less_Least_subset_x = result();
+
+(* ********************************************************************** *)
+(* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *)
+(* ********************************************************************** *)
+
+goalw thy [inj_def]
+ "(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \
+\ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})";
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSIs [lam_type] addDs [less_Least_subset_x]
+ addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1);
+val lam_Least_HH_inj_Pow = result();
+
+goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \
+\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
+\ : inj(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
+by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1);
+by (asm_full_simp_tac AC_ss 1);
+by (fast_tac (AC_cs addSEs [RepFun_eqI]) 1);
+val lam_Least_HH_inj = result();
+
+goal thy "!!A. [| A={a}; b:A |] ==> b=a";
+by (fast_tac AC_cs 1);
+val elem_of_sing_eq = result();
+
+goalw thy [surj_def]
+ "!!x. [| x - (UN a:A. F(a)) = 0; \
+\ ALL a:A. EX z:x. F(a) = {z} |] \
+\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})";
+by (asm_full_simp_tac (AC_ss addsimps [Diff_eq_0_iff]) 1);
+by (resolve_tac [conjI] 1);
+by (fast_tac (AC_cs addSIs [lam_type] addSEs [RepFun_eqI]) 1);
+by (resolve_tac [ballI] 1);
+by (eresolve_tac [RepFunE] 1);
+by (dresolve_tac [subsetD] 1 THEN (assume_tac 1));
+by (eresolve_tac [UN_E] 1);
+by (dresolve_tac [bspec] 1 THEN (assume_tac 1));
+by (eresolve_tac [bexE] 1);
+by (resolve_tac [bexI] 1 THEN (assume_tac 2));
+by (forward_tac [elem_of_sing_eq] 1 THEN (assume_tac 1));
+by (fast_tac AC_cs 1);
+val lam_surj_sing = result();
+
+goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0";
+by (fast_tac (AC_cs addSIs [equals0I, singletonI RS subst_elem]
+ addSDs [equals0D]) 1);
+val not_emptyI2 = result();
+
+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,
+ not_emptyI2 RS if_P]) 1);
+by (fast_tac AC_cs 1);
+val f_subset_imp_HH_subset = result();
+
+val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \
+\ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0";
+by (excluded_middle_tac "?P : {0}" 1);
+by (fast_tac AC_cs 2);
+by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS
+ f_subset_imp_HH_subset] 1);
+by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)]
+ addSEs [mem_irrefl]) 1);
+val f_subsets_imp_UN_HH_eq_x = result();
+
+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 (split_tac [expand_if] 1);
+by (fast_tac ZF_cs 1);
+val HH_values2 = result();
+
+goal thy "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
+by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1));
+by (fast_tac (AC_cs addSEs [equalityE, mem_irrefl]
+ addSDs [singleton_subsetD]) 1);
+val HH_subset_imp_eq = result();
+
+goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \
+\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
+by (dresolve_tac [less_Least_subset_x] 1);
+by (forward_tac [HH_subset_imp_eq] 1);
+by (dresolve_tac [apply_type] 1);
+by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
+by (fast_tac (AC_cs addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
+by (fast_tac (AC_cs addSEs [RepFunE] addEs [ssubst]) 1);
+val f_sing_imp_HH_sing = result();
+
+goalw thy [bij_def]
+ "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
+\ f : (PROD X:Pow(x)-{0}. {{z}. z:x}) |] \
+\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
+\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
+by (fast_tac (AC_cs addSIs [lam_Least_HH_inj, lam_surj_sing,
+ f_sing_imp_HH_sing]) 1);
+val f_sing_lam_bij = result();
+
+goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \
+\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
+by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
+ addDs [apply_type]) 1);
+val lam_singI = result();
+
+val bij_Least_HH_x = standard (lam_singI RSN (2,
+ [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] MRS comp_bij));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/HH.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/HH.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The theory file for the proofs of
+ AC17 ==> AC1
+ AC1 ==> WO2
+ AC15 ==> WO6
+*)
+
+HH = AC_Equiv + Hartog + WO_AC +
+
+consts
+
+ HH :: "[i, i, i] => i"
+
+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)))"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Hartog.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,84 @@
+(* Title: ZF/AC/Hartog.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+ Some proofs on the Hartogs function.
+*)
+
+open Hartog;
+
+goal thy "!!X. ALL a. Ord(a) --> a:X ==> P";
+by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1);
+by (fast_tac AC_cs 1);
+val Ords_in_set = result();
+
+goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==> \
+\ EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
+by (eresolve_tac [exE] 1);
+by (REPEAT (resolve_tac [exI, conjI] 1));
+by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1);
+by (resolve_tac [exI] 1);
+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));
+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)));
+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 (step_tac AC_cs 1);
+by (REPEAT (ares_tac [exI, conjI] 1));
+by (eresolve_tac [ordertype_Int] 2);
+by (fast_tac AC_cs 1);
+val Ord_lepoll_imp_eq_ordertype = result();
+
+goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \
+\ ALL a. Ord(a) --> \
+\ 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 (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1);
+val Ords_lepoll_set_lemma = result();
+
+goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P";
+by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1);
+val Ords_lepoll_set = result();
+
+goal thy "EX a. Ord(a) & ~a lepoll X";
+by (resolve_tac [swap] 1);
+by (fast_tac AC_cs 1);
+by (resolve_tac [Ords_lepoll_set] 1);
+by (fast_tac AC_cs 1);
+val ex_Ord_not_lepoll = result();
+
+goalw thy [Hartog_def] "~ Hartog(A) lepoll A";
+by (resolve_tac [ex_Ord_not_lepoll RS exE] 1);
+by (resolve_tac [LeastI] 1);
+by (REPEAT (fast_tac AC_cs 1));
+val HartogI = result();
+
+val HartogE = HartogI RS notE;
+
+goalw thy [Hartog_def] "Ord(Hartog(A))";
+by (resolve_tac [Ord_Least] 1);
+val Ord_Hartog = result();
+
+goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P";
+by (fast_tac (AC_cs addEs [less_LeastE]) 1);
+val less_HartogE1 = result();
+
+goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P";
+by (fast_tac (AC_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll
+ RS lepoll_trans RS HartogE]) 1);
+val less_HartogE = result();
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Hartog.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,18 @@
+(* Title: ZF/AC/Hartog.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Hartog's function.
+*)
+
+Hartog = Cardinal +
+
+consts
+
+ Hartog :: "i => i"
+
+defs
+
+ Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"
+
+end
\ No newline at end of file
--- a/src/ZF/AC/ROOT.ML Mon May 15 09:35:07 1995 +0200
+++ b/src/ZF/AC/ROOT.ML Thu May 18 11:51:23 1995 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
-Executes the proofs of the AC-equivalences, by Krzysztof Gr`abczewski
+Executes the proofs of the AC-equivalences, due to Krzysztof Gr`abczewski
*)
ZF_build_completed; (*Make examples fail if ZF did*)
@@ -13,21 +13,28 @@
loadpath := [".", "AC"];
-time_use_thy "WO6_WO1";
+time_use_thy "AC/AC_Equiv";
+
+time_use "AC/WO1_WO6.ML";
+time_use_thy "AC/WO6_WO1";
+time_use "AC/WO1_WO7.ML";
+time_use "AC/WO1_WO8.ML";
+
+time_use "AC/AC0_AC1.ML";
+time_use "AC/AC2_AC6.ML";
+time_use "AC/AC7_AC9.ML";
-(*New ones pending on ~kg10006/isabelle
-time_use "AC10_AC11.ML";
-time_use "AC11_AC12.ML";
-time_use "AC1_AC13.ML";
-time_use "AC13_AC1.ML";
-time_use "AC13_AC13.ML";
-time_use "AC13_AC14.ML";
-time_use "AC14_AC15.ML";
-time_use_thy "lemmas_AC13_AC15";
-time_use_thy "AC10_AC13";
-time_use_thy "AC11_AC14";
-time_use_thy "AC12_AC15";
-time_use "AC14_AC15.ML";
-*)
+time_use_thy "AC/WO1_AC1";
+time_use_thy "AC/AC1_WO2";
+
+time_use "AC/AC10_AC15.ML";
+time_use_thy "AC/AC15_WO6";
+
+(* AC16 to add *)
+
+time_use "AC/AC1_AC17.ML";
+time_use_thy "AC/AC17_AC1";
+
+time_use_thy "AC/AC18_AC19";
writeln"END: Root file for ZF/AC";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_AC1.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,12 @@
+(* 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_AC1.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+WO1_AC1 = AC_Equiv + WO_AC
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_WO6.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,79 @@
+(* Title: ZF/AC/WO1-WO6.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+ Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
+ All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML)
+
+ Every proofs (exept one) presented in this file are referred as clear
+ by Rubin & Rubin (page 2).
+ They refer reader to a book by G"odel to see the proof WO1 ==> WO2.
+ Fortunately order types made this proof also very easy.
+*)
+
+(* ********************************************************************** *)
+
+goalw thy WO_defs "!!Z. WO2 ==> WO3";
+by (fast_tac ZF_cs 1);
+result();
+
+(* ********************************************************************** *)
+
+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();
+
+(* ********************************************************************** *)
+
+goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2";
+by (fast_tac (ZF_cs addSIs [Ord_ordertype, ordermap_bij]) 1);
+result();
+
+(* ********************************************************************** *)
+
+goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
+by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1);
+val lam_sets = result();
+
+goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
+by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1);
+val surj_imp_eq_ = result();
+
+goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
+by (fast_tac (AC_cs addSDs [surj_imp_eq_]
+ addSIs [equalityI, ltI] addSEs [ltE]) 1);
+val surj_imp_eq = result();
+
+goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
+by (resolve_tac [allI] 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (eresolve_tac [exE] 1);
+by (REPEAT (resolve_tac [exI, conjI] 1));
+by (eresolve_tac [Ord_ordertype] 1);
+by (resolve_tac [conjI] 1);
+by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS
+ lam_sets RS domain_of_fun] 1);
+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();
+
+(* ********************************************************************** *)
+
+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();
+
+(* ********************************************************************** *)
+
+val prems = goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5";
+by (fast_tac ZF_cs 1);
+result();
+
+(* ********************************************************************** *)
+
+val prems = goalw thy WO_defs "!!Z. WO5 ==> WO6";
+by (fast_tac ZF_cs 1);
+result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_WO7.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,90 @@
+(* Title: ZF/AC/WO1_WO7.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
+LEMMA is the sentence denoted by (**)
+*)
+
+(* ********************************************************************** *)
+(* It is easy to see, that WO7 is equivallent to (**) *)
+(* ********************************************************************** *)
+
+goalw thy [WO7_def] "WO7 <-> (ALL X. ~Finite(X) --> \
+\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))))";
+by (fast_tac (ZF_cs addSEs [Finite_well_ord_converse]) 1);
+val WO7_iff_LEMMA = result();
+
+(* ********************************************************************** *)
+(* It is also easy to show that LEMMA implies WO1. *)
+(* ********************************************************************** *)
+
+goalw thy [WO1_def] "!!Z. ALL X. ~Finite(X) --> \
+\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))) ==> WO1";
+by (resolve_tac [allI] 1);
+by (eresolve_tac [allE] 1);
+by (excluded_middle_tac "Finite(A)" 1);
+by (fast_tac AC_cs 1);
+by (rewrite_goals_tac [Finite_def, eqpoll_def]);
+by (fast_tac (AC_cs addSIs [nat_into_Ord RS well_ord_Memrel RSN (2,
+ bij_is_inj RS well_ord_rvimage)]) 1);
+val LEMMA_imp_WO1 = result();
+
+(* ********************************************************************** *)
+(* The Rubins' proof of the other implication is contained within the *)
+(* following sentence : *)
+(* "... each infinite ordinal is well ordered by < but not by >." *)
+(* This statement can be proved by the following two theorems. *)
+(* But moreover we need to show similar property for any well ordered *)
+(* infinite set. It is not very difficult thanks to Isabelle order types *)
+(* We show that if a set is well ordered by some relation and by it's *)
+(* converse, then apropriate order type is well ordered by the converse *)
+(* of it's membership relation, which in connection with the previous *)
+(* gives the conclusion. *)
+(* ********************************************************************** *)
+
+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));
+by (resolve_tac [notI] 1);
+by (eres_inst_tac [("x","nat")] allE 1);
+by (eresolve_tac [disjE] 1);
+by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1);
+by (eresolve_tac [bexE] 1);
+by (eres_inst_tac [("x","succ(x)")] allE 1);
+by (fast_tac (ZF_cs addSIs [nat_succI, converseI, MemrelI,
+ nat_succI RSN (2, subsetD)]) 1);
+val converse_Memrel_not_wf_on = result();
+
+goalw thy [well_ord_def]
+ "!!a. [| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))";
+by (fast_tac (ZF_cs addSDs [converse_Memrel_not_wf_on]) 1);
+val converse_Memrel_not_well_ord = result();
+
+goal thy "!!A. [| well_ord(A,r); well_ord(A,converse(r)) |] \
+\ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))";
+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));
+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));
+val well_ord_converse_Memrel = result();
+
+goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \
+\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))";
+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 [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
+ bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2))
+ RS lepoll_Finite]
+ addSIs [notI] addEs [notE]) 1);
+val WO1_imp_LEMMA = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_WO8.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,30 @@
+(* Title: ZF/AC/WO1_WO8.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
+*)
+
+(* ********************************************************************** *)
+(* Trivial implication "WO1 ==> WO8" *)
+(* ********************************************************************** *)
+
+goalw thy WO_defs "!!Z. WO1 ==> WO8";
+by (fast_tac ZF_cs 1);
+result();
+
+(* ********************************************************************** *)
+(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
+(* ********************************************************************** *)
+
+goalw thy WO_defs "!!Z. WO8 ==> WO1";
+by (resolve_tac [allI] 1);
+by (eres_inst_tac [("x","{{x}. x:A}")] allE 1);
+by (eresolve_tac [impE] 1);
+by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
+ well_ord_rvimage]) 2);
+by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO_AC.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,22 @@
+(* Title: ZF/AC/WO_AC.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Lemmas used in the proofs like WO? ==> AC?
+*)
+
+open WO_AC;
+
+goal thy "!!A. [| well_ord(Union(A),r); 0~:A; B:A |] \
+\ ==> (THE b. first(b,B,r)) : B";
+by (fast_tac (AC_cs addSEs [well_ord_imp_ex1_first RS theI RS
+ (first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
+val first_in_B = result();
+
+goal thy "!!A. [| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)";
+by (fast_tac (AC_cs addSEs [first_in_B] addSIs [lam_type]) 1);
+val ex_choice_fun = result();
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO_AC.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,3 @@
+(*Dummy theory to document dependencies *)
+
+WO_AC = Order + first
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/first.ML Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,41 @@
+(* Title: ZF/AC/first.ML
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Lemmas involving the first element of a well ordered set
+*)
+
+open first;
+
+goalw thy [first_def] "!!b. first(b,B,r) ==> b:B";
+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));
+by (contr_tac 1);
+by (eresolve_tac [bexE] 1);
+by (res_inst_tac [("a","x")] ex1I 1);
+by (fast_tac ZF_cs 2);
+by (rewrite_goals_tac [tot_ord_def, linear_def]);
+by (fast_tac ZF_cs 1);
+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 (resolve_tac [first_is_elem] 1);
+by (eresolve_tac [theI] 1);
+val the_first_in = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/first.thy Thu May 18 11:51:23 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/first.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Theory helpful in proofs using first element of a well ordered set
+*)
+
+first = Order +
+
+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)"
+
+end
\ No newline at end of file