--- a/src/ZF/AC/AC0_AC1.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: ZF/AC/AC0_AC1.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
-AC0 is equivalent to AC1
-AC0 comes from Suppes, AC1 from Rubin & Rubin
-*)
-
-Goal "0\\<notin>A ==> A \\<subseteq> Pow(Union(A))-{0}";
-by (Fast_tac 1);
-qed "subset_Pow_Union";
-
-Goal "[| f:(\\<Pi>X \\<in> A. X); D \\<subseteq> A |] ==> \\<exists>g. g:(\\<Pi>X \\<in> D. X)";
-by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1);
-val lemma1 = result();
-
-Goalw AC_defs "AC0 ==> AC1";
-by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1);
-qed "AC0_AC1";
-
-Goalw AC_defs "AC1 ==> AC0";
-by (Deepen_tac 0 1);
-(*Large search space. Faster proof by
- by (fast_tac (claset() addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
-*)
-qed "AC1_AC0";
--- a/src/ZF/AC/AC10_AC15.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-(* 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) ==> AC14 ==> AC15 (m le n)
-
-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.
-*)
-
-(* ********************************************************************** *)
-(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *)
-(* or AC15 *)
-(* - cons_times_nat_not_Finite *)
-(* - ex_fun_AC13_AC15 *)
-(* ********************************************************************** *)
-
-Goalw [lepoll_def] "A\\<noteq>0 ==> B lepoll A*B";
-by (etac not_emptyE 1);
-by (res_inst_tac [("x","\\<lambda>z \\<in> B. <x,z>")] exI 1);
-by (fast_tac (claset() addSIs [snd_conv, lam_injective]) 1);
-qed "lepoll_Sigma";
-
-Goal "0\\<notin>A ==> \\<forall>B \\<in> {cons(0,x*nat). x \\<in> A}. ~Finite(B)";
-by (rtac ballI 1);
-by (etac RepFunE 1);
-by (hyp_subst_tac 1);
-by (rtac 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 (assume_tac 2));
-by (Fast_tac 1);
-qed "cons_times_nat_not_Finite";
-
-Goal "[| Union(C)=A; a \\<in> A |] ==> \\<exists>B \\<in> C. a \\<in> B & B \\<subseteq> A";
-by (Fast_tac 1);
-val lemma1 = result();
-
-Goalw [pairwise_disjoint_def]
- "[| pairwise_disjoint(A); B \\<in> A; C \\<in> A; a \\<in> B; a \\<in> C |] ==> B=C";
-by (dtac IntI 1 THEN (assume_tac 1));
-by (dres_inst_tac [("A","B Int C")] not_emptyI 1);
-by (Fast_tac 1);
-val lemma2 = result();
-
-Goalw [sets_of_size_between_def]
- "\\<forall>B \\<in> {cons(0, x*nat). x \\<in> A}. pairwise_disjoint(f`B) & \
-\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \
-\ ==> \\<forall>B \\<in> A. \\<exists>! u. u \\<in> f`cons(0, B*nat) & u \\<subseteq> cons(0, B*nat) & \
-\ 0 \\<in> u & 2 lepoll u & u lepoll n";
-by (rtac ballI 1);
-by (etac ballE 1);
-by (Fast_tac 2);
-by (REPEAT (etac conjE 1));
-by (dresolve_tac [consI1 RSN (2, lemma1)] 1);
-by (etac bexE 1);
-by (rtac ex1I 1);
-by (Fast_tac 1);
-by (REPEAT (etac conjE 1));
-by (rtac lemma2 1 THEN (REPEAT (assume_tac 1)));
-val lemma3 = result();
-
-Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a \\<in> A} lepoll i";
-by (etac exE 1);
-by (res_inst_tac
- [("x", "\\<lambda>x \\<in> RepFun(A, P). LEAST j. \\<exists>a \\<in> A. x=P(a) & f`a=j")] exI 1);
-by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1);
-by (etac RepFunE 1);
-by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1));
-by (fast_tac (claset() addIs [LeastI2]
- addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
-by (etac RepFunE 1);
-by (rtac LeastI2 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
-by (fast_tac (claset() addEs [sym, left_inverse RS ssubst]) 1);
-val lemma4 = result();
-
-Goal "[| n \\<in> nat; B \\<in> A; u(B) \\<subseteq> cons(0, B*nat); 0 \\<in> u(B); 2 lepoll u(B); \
-\ u(B) lepoll succ(n) |] \
-\ ==> (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B \\<noteq> 0 & \
-\ (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B \\<subseteq> B & \
-\ (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B lepoll n";
-by (Asm_simp_tac 1);
-by (rtac 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 (rtac conjI 1);
-by (fast_tac (claset() addSIs [fst_type] addSEs [consE]) 1);
-by (fast_tac (claset() addSEs [equalityE,
- Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1);
-val lemma5 = result();
-
-Goal "[| \\<exists>f. \\<forall>B \\<in> {cons(0, x*nat). x \\<in> A}. \
-\ pairwise_disjoint(f`B) & \
-\ sets_of_size_between(f`B, 2, succ(n)) & \
-\ Union(f`B)=B; n \\<in> nat |] \
-\ ==> \\<exists>f. \\<forall>B \\<in> A. f`B \\<noteq> 0 & f`B \\<subseteq> B & f`B lepoll n";
-by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec]
- addSEs [exE, conjE]
- addIs [exI, ballI, lemma5]) 1);
-qed "ex_fun_AC13_AC15";
-
-(* ********************************************************************** *)
-(* The target proofs *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* AC10(n) ==> AC11 *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "[| n \\<in> nat; 1 le n; AC10(n) |] ==> AC11";
-by (rtac bexI 1 THEN (assume_tac 2));
-by (Fast_tac 1);
-qed "AC10_AC11";
-
-(* ********************************************************************** *)
-(* AC11 ==> AC12 *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "AC11 ==> AC12";
-by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1);
-qed "AC11_AC12";
-
-(* ********************************************************************** *)
-(* AC12 ==> AC15 *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "AC12 ==> AC15";
-by Safe_tac;
-by (etac allE 1);
-by (etac impE 1);
-by (etac cons_times_nat_not_Finite 1);
-by (fast_tac (claset() addSIs [ex_fun_AC13_AC15]) 1);
-qed "AC12_AC15";
-
-(* ********************************************************************** *)
-(* 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 \\<in> *)
-(* AC10(n) implies AC13(n) for (1 le n) *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "[| n \\<in> nat; 1 le n; AC10(n) |] ==> AC13(n)";
-by Safe_tac;
-by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
- ex_fun_AC13_AC15]) 1);
-qed "AC10_AC13";
-
-(* ********************************************************************** *)
-(* The proofs needed in the second case, not in the first *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* AC1 ==> AC13(1) *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "AC1 ==> AC13(1)";
-by (rtac allI 1);
-by (etac allE 1);
-by (rtac impI 1);
-by (mp_tac 1);
-by (etac exE 1);
-by (res_inst_tac [("x","\\<lambda>x \\<in> A. {f`x}")] exI 1);
-by (asm_simp_tac (simpset() addsimps
- [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
- singletonI RS not_emptyI]) 1);
-qed "AC1_AC13";
-
-(* ********************************************************************** *)
-(* AC13(m) ==> AC13(n) for m \\<subseteq> n *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)";
-by (dtac le_imp_lepoll 1);
-by (fast_tac (claset() addSEs [lepoll_trans]) 1);
-qed "AC13_mono";
-
-(* ********************************************************************** *)
-(* The proofs necessary for both cases *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* AC13(n) ==> AC14 if 1 \\<subseteq> n *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "[| n \\<in> nat; 1 le n; AC13(n) |] ==> AC14";
-by (fast_tac (FOL_cs addIs [bexI]) 1);
-qed "AC13_AC14";
-
-(* ********************************************************************** *)
-(* AC14 ==> AC15 *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "AC14 ==> AC15";
-by (Fast_tac 1);
-qed "AC14_AC15";
-
-(* ********************************************************************** *)
-(* The redundant proofs; however cited by Rubin & Rubin *)
-(* ********************************************************************** *)
-
-(* ********************************************************************** *)
-(* AC13(1) ==> AC1 *)
-(* ********************************************************************** *)
-
-Goal "[| A\\<noteq>0; A lepoll 1 |] ==> \\<exists>a. A={a}";
-by (fast_tac (claset() addSEs [not_emptyE, lepoll_1_is_sing]) 1);
-qed "lemma_aux";
-
-Goal "\\<forall>B \\<in> A. f(B)\\<noteq>0 & f(B)<=B & f(B) lepoll 1 \
-\ ==> (\\<lambda>x \\<in> A. THE y. f(x)={y}) \\<in> (\\<Pi>X \\<in> A. X)";
-by (rtac lam_type 1);
-by (dtac bspec 1 THEN (assume_tac 1));
-by (REPEAT (etac conjE 1));
-by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1));
-by (asm_full_simp_tac (simpset() addsimps [the_element]) 1);
-val lemma = result();
-
-Goalw AC_defs "AC13(1) ==> AC1";
-by (fast_tac (claset() addSEs [lemma]) 1);
-qed "AC13_AC1";
-
-(* ********************************************************************** *)
-(* AC11 ==> AC14 *)
-(* ********************************************************************** *)
-
-Goalw [AC11_def, AC14_def] "AC11 ==> AC14";
-by (fast_tac (claset() addSIs [AC10_AC13]) 1);
-qed "AC11_AC14";
--- a/src/ZF/AC/AC15_WO6.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/AC15_WO6.ML Tue Jun 26 16:54:39 2001 +0200
@@ -2,9 +2,156 @@
ID: $Id$
Author: Krzysztof Grabczewski
-The proof of AC1 ==> WO2
+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) ==> AC14 ==> AC15 (m le n)
+
+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.
*)
+(* ********************************************************************** *)
+(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *)
+(* or AC15 *)
+(* - cons_times_nat_not_Finite *)
+(* - ex_fun_AC13_AC15 *)
+(* ********************************************************************** *)
+
+Goalw [lepoll_def] "A\\<noteq>0 ==> B lepoll A*B";
+by (etac not_emptyE 1);
+by (res_inst_tac [("x","\\<lambda>z \\<in> B. <x,z>")] exI 1);
+by (fast_tac (claset() addSIs [snd_conv, lam_injective]) 1);
+qed "lepoll_Sigma";
+
+Goal "0\\<notin>A ==> \\<forall>B \\<in> {cons(0,x*nat). x \\<in> A}. ~Finite(B)";
+by (rtac ballI 1);
+by (etac RepFunE 1);
+by (hyp_subst_tac 1);
+by (rtac 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 (assume_tac 2));
+by (Fast_tac 1);
+qed "cons_times_nat_not_Finite";
+
+Goal "[| Union(C)=A; a \\<in> A |] ==> \\<exists>B \\<in> C. a \\<in> B & B \\<subseteq> A";
+by (Fast_tac 1);
+val lemma1 = result();
+
+Goalw [pairwise_disjoint_def]
+ "[| pairwise_disjoint(A); B \\<in> A; C \\<in> A; a \\<in> B; a \\<in> C |] ==> B=C";
+by (dtac IntI 1 THEN (assume_tac 1));
+by (dres_inst_tac [("A","B Int C")] not_emptyI 1);
+by (Fast_tac 1);
+val lemma2 = result();
+
+Goalw [sets_of_size_between_def]
+ "\\<forall>B \\<in> {cons(0, x*nat). x \\<in> A}. pairwise_disjoint(f`B) & \
+\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \
+\ ==> \\<forall>B \\<in> A. \\<exists>! u. u \\<in> f`cons(0, B*nat) & u \\<subseteq> cons(0, B*nat) & \
+\ 0 \\<in> u & 2 lepoll u & u lepoll n";
+by (rtac ballI 1);
+by (etac ballE 1);
+by (Fast_tac 2);
+by (REPEAT (etac conjE 1));
+by (dresolve_tac [consI1 RSN (2, lemma1)] 1);
+by (etac bexE 1);
+by (rtac ex1I 1);
+by (Fast_tac 1);
+by (REPEAT (etac conjE 1));
+by (rtac lemma2 1 THEN (REPEAT (assume_tac 1)));
+val lemma3 = result();
+
+Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a \\<in> A} lepoll i";
+by (etac exE 1);
+by (res_inst_tac
+ [("x", "\\<lambda>x \\<in> RepFun(A, P). LEAST j. \\<exists>a \\<in> A. x=P(a) & f`a=j")] exI 1);
+by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1);
+by (etac RepFunE 1);
+by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1));
+by (fast_tac (claset() addIs [LeastI2]
+ addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
+by (etac RepFunE 1);
+by (rtac LeastI2 1);
+by (Fast_tac 1);
+by (fast_tac (claset() addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1);
+by (fast_tac (claset() addEs [sym, left_inverse RS ssubst]) 1);
+val lemma4 = result();
+
+Goal "[| n \\<in> nat; B \\<in> A; u(B) \\<subseteq> cons(0, B*nat); 0 \\<in> u(B); 2 lepoll u(B); \
+\ u(B) lepoll succ(n) |] \
+\ ==> (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B \\<noteq> 0 & \
+\ (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B \\<subseteq> B & \
+\ (\\<lambda>x \\<in> A. {fst(x). x \\<in> u(x)-{0}})`B lepoll n";
+by (Asm_simp_tac 1);
+by (rtac 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 (rtac conjI 1);
+by (fast_tac (claset() addSIs [fst_type] addSEs [consE]) 1);
+by (fast_tac (claset() addSEs [equalityE,
+ Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1);
+val lemma5 = result();
+
+Goal "[| \\<exists>f. \\<forall>B \\<in> {cons(0, x*nat). x \\<in> A}. \
+\ pairwise_disjoint(f`B) & \
+\ sets_of_size_between(f`B, 2, succ(n)) & \
+\ Union(f`B)=B; n \\<in> nat |] \
+\ ==> \\<exists>f. \\<forall>B \\<in> A. f`B \\<noteq> 0 & f`B \\<subseteq> B & f`B lepoll n";
+by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec]
+ addSEs [exE, conjE]
+ addIs [exI, ballI, lemma5]) 1);
+qed "ex_fun_AC13_AC15";
+
+(* ********************************************************************** *)
+(* The target proofs *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC10(n) ==> AC11 *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "[| n \\<in> nat; 1 le n; AC10(n) |] ==> AC11";
+by (rtac bexI 1 THEN (assume_tac 2));
+by (Fast_tac 1);
+qed "AC10_AC11";
+
+(* ********************************************************************** *)
+(* AC11 ==> AC12 *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "AC11 ==> AC12";
+by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1);
+qed "AC11_AC12";
+
+(* ********************************************************************** *)
+(* AC12 ==> AC15 *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "AC12 ==> AC15";
+by Safe_tac;
+by (etac allE 1);
+by (etac impE 1);
+by (etac cons_times_nat_not_Finite 1);
+by (fast_tac (claset() addSIs [ex_fun_AC13_AC15]) 1);
+qed "AC12_AC15";
+
+(* ********************************************************************** *)
+(* AC15 ==> WO6 *)
+(* ********************************************************************** *)
+
Goal "Ord(x) ==> (\\<Union>a<x. F(a)) = (\\<Union>a \\<in> x. F(a))";
by (fast_tac (claset() addSIs [ltI] addSDs [ltD]) 1);
qed "OUN_eq_UN";
@@ -42,3 +189,104 @@
by (fast_tac (claset() addSIs [Ord_Least, lam_type RS domain_of_fun]
addSEs [less_Least_subset_x, lemma1, lemma2]) 1);
qed "AC15_WO6";
+
+
+(* ********************************************************************** *)
+(* 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 \\<in> *)
+(* AC10(n) implies AC13(n) for (1 le n) *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "[| n \\<in> nat; 1 le n; AC10(n) |] ==> AC13(n)";
+by Safe_tac;
+by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
+ ex_fun_AC13_AC15]) 1);
+qed "AC10_AC13";
+
+(* ********************************************************************** *)
+(* The proofs needed in the second case, not in the first *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC1 ==> AC13(1) *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "AC1 ==> AC13(1)";
+by (rtac allI 1);
+by (etac allE 1);
+by (rtac impI 1);
+by (mp_tac 1);
+by (etac exE 1);
+by (res_inst_tac [("x","\\<lambda>x \\<in> A. {f`x}")] exI 1);
+by (asm_simp_tac (simpset() addsimps
+ [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
+ singletonI RS not_emptyI]) 1);
+qed "AC1_AC13";
+
+(* ********************************************************************** *)
+(* AC13(m) ==> AC13(n) for m \\<subseteq> n *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)";
+by (dtac le_imp_lepoll 1);
+by (fast_tac (claset() addSEs [lepoll_trans]) 1);
+qed "AC13_mono";
+
+(* ********************************************************************** *)
+(* The proofs necessary for both cases *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC13(n) ==> AC14 if 1 \\<subseteq> n *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "[| n \\<in> nat; 1 le n; AC13(n) |] ==> AC14";
+by (fast_tac (FOL_cs addIs [bexI]) 1);
+qed "AC13_AC14";
+
+(* ********************************************************************** *)
+(* AC14 ==> AC15 *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "AC14 ==> AC15";
+by (Fast_tac 1);
+qed "AC14_AC15";
+
+(* ********************************************************************** *)
+(* The redundant proofs; however cited by Rubin & Rubin *)
+(* ********************************************************************** *)
+
+(* ********************************************************************** *)
+(* AC13(1) ==> AC1 *)
+(* ********************************************************************** *)
+
+Goal "[| A\\<noteq>0; A lepoll 1 |] ==> \\<exists>a. A={a}";
+by (fast_tac (claset() addSEs [not_emptyE, lepoll_1_is_sing]) 1);
+qed "lemma_aux";
+
+Goal "\\<forall>B \\<in> A. f(B)\\<noteq>0 & f(B)<=B & f(B) lepoll 1 \
+\ ==> (\\<lambda>x \\<in> A. THE y. f(x)={y}) \\<in> (\\<Pi>X \\<in> A. X)";
+by (rtac lam_type 1);
+by (dtac bspec 1 THEN (assume_tac 1));
+by (REPEAT (etac conjE 1));
+by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps [the_element]) 1);
+val lemma = result();
+
+Goalw AC_defs "AC13(1) ==> AC1";
+by (fast_tac (claset() addSEs [lemma]) 1);
+qed "AC13_AC1";
+
+(* ********************************************************************** *)
+(* AC11 ==> AC14 *)
+(* ********************************************************************** *)
+
+Goalw [AC11_def, AC14_def] "AC11 ==> AC14";
+by (fast_tac (claset() addSIs [AC10_AC13]) 1);
+qed "AC11_AC14";
--- a/src/ZF/AC/AC16_WO4.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Tue Jun 26 16:54:39 2001 +0200
@@ -89,33 +89,20 @@
(* There is a k-2 element subset of y *)
(* ********************************************************************** *)
-Goalw [lepoll_def, eqpoll_def]
- "[| n \\<in> nat; nat lepoll X |] ==> \\<exists>Y. Y \\<subseteq> X & n eqpoll Y";
-by (fast_tac (subset_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)]
- addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1);
-qed "nat_lepoll_imp_ex_eqpoll_n";
-
val ordertype_eqpoll =
ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2));
-Goalw [lesspoll_def] "n \\<in> nat ==> n lesspoll nat";
-by (fast_tac (claset() 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);
-qed "n_lesspoll_nat";
-
Goal "[| a \\<subseteq> y; b \\<in> y-a; u \\<in> x |] ==> cons(b, cons(u, a)) \\<in> Pow(x Un y)";
by (Fast_tac 1);
qed "cons_cons_subset";
-Goal "[| a eqpoll k; a \\<subseteq> y; b \\<in> y-a; u \\<in> x; x Int y = 0 \
-\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
+Goal "[| a eqpoll k; a \\<subseteq> y; b \\<in> y-a; u \\<in> x; x Int y = 0 |] \
+\ ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1);
qed "cons_cons_eqpoll";
-Goal "[| succ(k) eqpoll A; k eqpoll B; B \\<subseteq> A; a \\<in> A-B; k \\<in> nat \
-\ |] ==> A = cons(a, B)";
+Goal "[| succ(k) eqpoll A; k eqpoll B; B \\<subseteq> A; a \\<in> A-B; k \\<in> nat |] \
+\ ==> A = cons(a, B)";
by (rtac equalityI 1);
by (Fast_tac 2);
by (resolve_tac [Diff_eq_0_iff RS iffD1] 1);
--- a/src/ZF/AC/AC17_AC1.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/AC17_AC1.ML Tue Jun 26 16:54:39 2001 +0200
@@ -1,10 +1,54 @@
-(* Title: ZF/AC/AC17_AC1.ML
+(* Title: ZF/AC/AC1_AC17.ML
ID: $Id$
Author: Krzysztof Grabczewski
-The proof of AC1 ==> AC17
+The equivalence of AC0, AC1 and AC17
+
+Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
+to AC0 and AC1.
*)
+
+(** AC0 is equivalent to AC1.
+ AC0 comes from Suppes, AC1 from Rubin & Rubin **)
+
+Goal "[| f:(\\<Pi>X \\<in> A. X); D \\<subseteq> A |] ==> \\<exists>g. g:(\\<Pi>X \\<in> D. X)";
+by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1);
+val lemma1 = result();
+
+Goalw AC_defs "AC0 ==> AC1";
+by (blast_tac (claset() addIs [lemma1]) 1);
+qed "AC0_AC1";
+
+Goalw AC_defs "AC1 ==> AC0";
+by (Blast_tac 1);
+qed "AC1_AC0";
+
+
+(**** The proof of AC1 ==> AC17 ****)
+
+Goal "f \\<in> (\\<Pi>X \\<in> Pow(A) - {0}. X) ==> f \\<in> (Pow(A) - {0} -> A)";
+by (rtac Pi_type 1 THEN (assume_tac 1));
+by (dtac apply_type 1 THEN (assume_tac 1));
+by (Fast_tac 1);
+val lemma1 = result();
+
+Goalw AC_defs "AC1 ==> AC17";
+by (rtac allI 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
+by (etac impE 1);
+by (Fast_tac 1);
+by (etac exE 1);
+by (rtac bexI 1);
+by (etac lemma1 2);
+by (rtac apply_type 1 THEN (assume_tac 1));
+by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1);
+qed "AC1_AC17";
+
+
+(**** The proof of AC17 ==> AC1 ****)
+
(* *********************************************************************** *)
(* more properties of HH *)
(* *********************************************************************** *)
@@ -87,3 +131,180 @@
by (fast_tac (claset() addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem),
f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1);
qed "AC17_AC1";
+
+
+(* **********************************************************************
+ AC1 ==> AC2 ==> AC1
+ AC1 ==> AC4 ==> AC3 ==> AC1
+ AC4 ==> AC5 ==> AC4
+ AC1 <-> AC6
+************************************************************************* *)
+
+(* ********************************************************************** *)
+(* AC1 ==> AC2 *)
+(* ********************************************************************** *)
+
+Goal "[| f:(\\<Pi>X \\<in> A. X); B \\<in> A; 0\\<notin>A |] ==> {f`B} \\<subseteq> B Int {f`C. C \\<in> A}";
+by (fast_tac (claset() addSEs [apply_type]) 1);
+val lemma1 = result();
+
+Goalw [pairwise_disjoint_def]
+ "[| pairwise_disjoint(A); B \\<in> A; C \\<in> A; D \\<in> B; D \\<in> C |] ==> f`B = f`C";
+by (Fast_tac 1);
+val lemma2 = result();
+
+Goalw AC_defs "AC1 ==> AC2";
+by (rtac allI 1);
+by (rtac impI 1);
+by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
+by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
+by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
+by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1);
+qed "AC1_AC2";
+
+
+(* ********************************************************************** *)
+(* AC2 ==> AC1 *)
+(* ********************************************************************** *)
+
+Goal "0\\<notin>A ==> 0 \\<notin> {B*{B}. B \\<in> A}";
+by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1);
+val lemma1 = result();
+
+Goal "[| X*{X} Int C = {y}; X \\<in> A |] \
+\ ==> (THE y. X*{X} Int C = {y}): X*A";
+by (rtac subst_elem 1);
+by (fast_tac (claset() addSIs [the_equality]
+ addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+val lemma2 = result();
+
+Goal "\\<forall>D \\<in> {E*{E}. E \\<in> A}. \\<exists>y. D Int C = {y} \
+\ ==> (\\<lambda>x \\<in> A. fst(THE z. (x*{x} Int C = {z}))) \\<in> (\\<Pi>X \\<in> A. X)";
+by (fast_tac (claset() addSEs [lemma2]
+ addSIs [lam_type, RepFunI, fst_type]) 1);
+val lemma3 = result();
+
+Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1";
+by (REPEAT (resolve_tac [allI, impI] 1));
+by (REPEAT (eresolve_tac [allE, impE] 1));
+by (fast_tac (claset() addSEs [lemma3]) 2);
+by (fast_tac (claset() addSIs [lemma1, equals0I]) 1);
+qed "AC2_AC1";
+
+
+(* ********************************************************************** *)
+(* AC1 ==> AC4 *)
+(* ********************************************************************** *)
+
+Goal "0 \\<notin> {R``{x}. x \\<in> domain(R)}";
+by (Blast_tac 1);
+val lemma = result();
+
+Goalw AC_defs "AC1 ==> AC4";
+by (REPEAT (resolve_tac [allI, impI] 1));
+by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
+by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1);
+qed "AC1_AC4";
+
+
+(* ********************************************************************** *)
+(* AC4 ==> AC3 *)
+(* ********************************************************************** *)
+
+Goal "f \\<in> A->B ==> (\\<Union>z \\<in> A. {z}*f`z) \\<subseteq> A*Union(B)";
+by (fast_tac (claset() addSDs [apply_type]) 1);
+val lemma1 = result();
+
+Goal "domain(\\<Union>z \\<in> A. {z}*f(z)) = {a \\<in> A. f(a)\\<noteq>0}";
+by (Blast_tac 1);
+val lemma2 = result();
+
+Goal "x \\<in> A ==> (\\<Union>z \\<in> A. {z}*f(z))``{x} = f(x)";
+by (Fast_tac 1);
+val lemma3 = result();
+
+Goalw AC_defs "AC4 ==> AC3";
+by (REPEAT (resolve_tac [allI,ballI] 1));
+by (REPEAT (eresolve_tac [allE,impE] 1));
+by (etac lemma1 1);
+by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3]
+ addcongs [Pi_cong]) 1);
+qed "AC4_AC3";
+
+(* ********************************************************************** *)
+(* AC3 ==> AC1 *)
+(* ********************************************************************** *)
+
+Goal "b\\<notin>A ==> (\\<Pi>x \\<in> {a \\<in> A. id(A)`a\\<noteq>b}. id(A)`x) = (\\<Pi>x \\<in> A. x)";
+by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1);
+by (res_inst_tac [("b","A")] subst_context 1);
+by (Fast_tac 1);
+val lemma = result();
+
+Goalw AC_defs "AC3 ==> AC1";
+by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1);
+qed "AC3_AC1";
+
+(* ********************************************************************** *)
+(* AC4 ==> AC5 *)
+(* ********************************************************************** *)
+
+Goalw (range_def::AC_defs) "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 (etac exE 1);
+by (rtac bexI 1);
+by (rtac Pi_type 2 THEN (assume_tac 2));
+by (fast_tac (claset() addSDs [apply_type]
+ addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
+by (rtac ballI 1);
+by (rtac apply_equality 1 THEN (assume_tac 2));
+by (etac domainE 1);
+by (ftac range_type 1 THEN (assume_tac 1));
+by (fast_tac (claset() addDs [apply_equality]) 1);
+qed "AC4_AC5";
+
+
+(* ********************************************************************** *)
+(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
+(* ********************************************************************** *)
+
+Goal "R \\<subseteq> A*B ==> (\\<lambda>x \\<in> R. fst(x)) \\<in> R -> A";
+by (fast_tac (claset() addSIs [lam_type, fst_type]) 1);
+val lemma1 = result();
+
+Goalw [range_def] "R \\<subseteq> A*B ==> range(\\<lambda>x \\<in> R. fst(x)) = domain(R)";
+by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE],
+ simpset()) 1);
+val lemma2 = result();
+
+Goal "[| \\<exists>f \\<in> A->C. P(f,domain(f)); A=B |] ==> \\<exists>f \\<in> B->C. P(f,B)";
+by (etac bexE 1);
+by (ftac domain_of_fun 1);
+by (Fast_tac 1);
+val lemma3 = result();
+
+Goal "[| R \\<subseteq> A*B; g \\<in> C->R; \\<forall>x \\<in> C. (\\<lambda>z \\<in> R. fst(z))` (g`x) = x |] \
+\ ==> (\\<lambda>x \\<in> C. snd(g`x)): (\\<Pi>x \\<in> C. R``{x})";
+by (rtac lam_type 1);
+by (force_tac (claset() addDs [apply_type], simpset()) 1);
+val lemma4 = result();
+
+Goalw AC_defs "AC5 ==> AC4";
+by (Clarify_tac 1);
+by (REPEAT (eresolve_tac [allE,ballE] 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 (claset() addSEs [lemma4]) 1);
+qed "AC5_AC4";
+
+
+(* ********************************************************************** *)
+(* AC1 <-> AC6 *)
+(* ********************************************************************** *)
+
+Goalw AC_defs "AC1 <-> AC6";
+by (Blast_tac 1);
+qed "AC1_iff_AC6";
--- a/src/ZF/AC/AC1_AC17.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: ZF/AC/AC1_AC17.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
-The proof of AC1 ==> AC17
-*)
-
-Goal "f \\<in> (\\<Pi>X \\<in> Pow(A) - {0}. X) ==> f \\<in> (Pow(A) - {0} -> A)";
-by (rtac Pi_type 1 THEN (assume_tac 1));
-by (dtac apply_type 1 THEN (assume_tac 1));
-by (Fast_tac 1);
-val lemma1 = result();
-
-Goalw AC_defs "AC1 ==> AC17";
-by (rtac allI 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
-by (etac impE 1);
-by (Fast_tac 1);
-by (etac exE 1);
-by (rtac bexI 1);
-by (etac lemma1 2);
-by (rtac apply_type 1 THEN (assume_tac 1));
-by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1);
-qed "AC1_AC17";
--- a/src/ZF/AC/AC2_AC6.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,180 +0,0 @@
-(* Title: ZF/AC/AC2_AC6.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
-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
-AC1 <-> AC6
-*)
-
-(* ********************************************************************** *)
-(* AC1 ==> AC2 *)
-(* ********************************************************************** *)
-
-Goal "[| f:(\\<Pi>X \\<in> A. X); B \\<in> A; 0\\<notin>A |] ==> {f`B} \\<subseteq> B Int {f`C. C \\<in> A}";
-by (fast_tac (claset() addSEs [apply_type]) 1);
-val lemma1 = result();
-
-Goalw [pairwise_disjoint_def]
- "[| pairwise_disjoint(A); B \\<in> A; C \\<in> A; D \\<in> B; D \\<in> C |] ==> f`B = f`C";
-by (Fast_tac 1);
-val lemma2 = result();
-
-Goalw AC_defs "AC1 ==> AC2";
-by (rtac allI 1);
-by (rtac impI 1);
-by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
-by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
-by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
-by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1);
-qed "AC1_AC2";
-
-
-(* ********************************************************************** *)
-(* AC2 ==> AC1 *)
-(* ********************************************************************** *)
-
-Goal "0\\<notin>A ==> 0 \\<notin> {B*{B}. B \\<in> A}";
-by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1);
-val lemma1 = result();
-
-Goal "[| X*{X} Int C = {y}; X \\<in> A |] \
-\ ==> (THE y. X*{X} Int C = {y}): X*A";
-by (rtac subst_elem 1);
-by (fast_tac (claset() addSIs [the_equality]
- addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-val lemma2 = result();
-
-Goal "\\<forall>D \\<in> {E*{E}. E \\<in> A}. \\<exists>y. D Int C = {y} \
-\ ==> (\\<lambda>x \\<in> A. fst(THE z. (x*{x} Int C = {z}))) \\<in> (\\<Pi>X \\<in> A. X)";
-by (fast_tac (claset() addSEs [lemma2]
- addSIs [lam_type, RepFunI, fst_type]) 1);
-val lemma3 = result();
-
-Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1";
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (REPEAT (eresolve_tac [allE, impE] 1));
-by (fast_tac (claset() addSEs [lemma3]) 2);
-by (fast_tac (claset() addSIs [lemma1, equals0I]) 1);
-qed "AC2_AC1";
-
-
-(* ********************************************************************** *)
-(* AC1 ==> AC4 *)
-(* ********************************************************************** *)
-
-Goal "0 \\<notin> {R``{x}. x \\<in> domain(R)}";
-by (Blast_tac 1);
-val lemma = result();
-
-Goalw AC_defs "AC1 ==> AC4";
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
-by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1);
-qed "AC1_AC4";
-
-
-(* ********************************************************************** *)
-(* AC4 ==> AC3 *)
-(* ********************************************************************** *)
-
-Goal "f \\<in> A->B ==> (\\<Union>z \\<in> A. {z}*f`z) \\<subseteq> A*Union(B)";
-by (fast_tac (claset() addSDs [apply_type]) 1);
-val lemma1 = result();
-
-Goal "domain(\\<Union>z \\<in> A. {z}*f(z)) = {a \\<in> A. f(a)\\<noteq>0}";
-by (Blast_tac 1);
-val lemma2 = result();
-
-Goal "x \\<in> A ==> (\\<Union>z \\<in> A. {z}*f(z))``{x} = f(x)";
-by (Fast_tac 1);
-val lemma3 = result();
-
-Goalw AC_defs "AC4 ==> AC3";
-by (REPEAT (resolve_tac [allI,ballI] 1));
-by (REPEAT (eresolve_tac [allE,impE] 1));
-by (etac lemma1 1);
-by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3]
- addcongs [Pi_cong]) 1);
-qed "AC4_AC3";
-
-(* ********************************************************************** *)
-(* AC3 ==> AC1 *)
-(* ********************************************************************** *)
-
-Goal "b\\<notin>A ==> (\\<Pi>x \\<in> {a \\<in> A. id(A)`a\\<noteq>b}. id(A)`x) = (\\<Pi>x \\<in> A. x)";
-by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1);
-by (res_inst_tac [("b","A")] subst_context 1);
-by (Fast_tac 1);
-val lemma = result();
-
-Goalw AC_defs "AC3 ==> AC1";
-by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1);
-qed "AC3_AC1";
-
-(* ********************************************************************** *)
-(* AC4 ==> AC5 *)
-(* ********************************************************************** *)
-
-Goalw (range_def::AC_defs) "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 (etac exE 1);
-by (rtac bexI 1);
-by (rtac Pi_type 2 THEN (assume_tac 2));
-by (fast_tac (claset() addSDs [apply_type]
- addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2);
-by (rtac ballI 1);
-by (rtac apply_equality 1 THEN (assume_tac 2));
-by (etac domainE 1);
-by (ftac range_type 1 THEN (assume_tac 1));
-by (fast_tac (claset() addDs [apply_equality]) 1);
-qed "AC4_AC5";
-
-
-(* ********************************************************************** *)
-(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
-(* ********************************************************************** *)
-
-Goal "R \\<subseteq> A*B ==> (\\<lambda>x \\<in> R. fst(x)) \\<in> R -> A";
-by (fast_tac (claset() addSIs [lam_type, fst_type]) 1);
-val lemma1 = result();
-
-Goalw [range_def] "R \\<subseteq> A*B ==> range(\\<lambda>x \\<in> R. fst(x)) = domain(R)";
-by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE],
- simpset()) 1);
-val lemma2 = result();
-
-Goal "[| \\<exists>f \\<in> A->C. P(f,domain(f)); A=B |] ==> \\<exists>f \\<in> B->C. P(f,B)";
-by (etac bexE 1);
-by (ftac domain_of_fun 1);
-by (Fast_tac 1);
-val lemma3 = result();
-
-Goal "[| R \\<subseteq> A*B; g \\<in> C->R; \\<forall>x \\<in> C. (\\<lambda>z \\<in> R. fst(z))` (g`x) = x |] \
-\ ==> (\\<lambda>x \\<in> C. snd(g`x)): (\\<Pi>x \\<in> C. R``{x})";
-by (rtac lam_type 1);
-by (force_tac (claset() addDs [apply_type], simpset()) 1);
-val lemma4 = result();
-
-Goalw AC_defs "AC5 ==> AC4";
-by (Clarify_tac 1);
-by (REPEAT (eresolve_tac [allE,ballE] 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 (claset() addSEs [lemma4]) 1);
-qed "AC5_AC4";
-
-
-(* ********************************************************************** *)
-(* AC1 <-> AC6 *)
-(* ********************************************************************** *)
-
-Goalw AC_defs "AC1 <-> AC6";
-by (Blast_tac 1);
-qed "AC1_iff_AC6";
--- a/src/ZF/AC/DC.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/DC.ML Tue Jun 26 16:54:39 2001 +0200
@@ -199,11 +199,6 @@
************************************************************************* *)
-Goalw [lesspoll_def, Finite_def]
- "A lesspoll nat ==> Finite(A)";
-by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1);
-qed "lesspoll_nat_is_Finite";
-
Goal "n \\<in> nat ==> \\<forall>A. (A eqpoll n & A \\<subseteq> X) --> A \\<in> Fin(X)";
by (induct_tac "n" 1);
by (rtac allI 1);
--- a/src/ZF/AC/ROOT.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/ROOT.ML Tue Jun 26 16:54:39 2001 +0200
@@ -8,25 +8,19 @@
time_use_thy "AC_Equiv";
-time_use "WO1_WO6.ML";
time_use_thy "WO6_WO1";
time_use_thy "WO1_WO7";
-time_use "WO1_WO8.ML";
-time_use "AC0_AC1.ML";
-time_use "AC2_AC6.ML";
time_use "AC7_AC9.ML";
time_use_thy "WO1_AC";
time_use_thy "AC1_WO2";
-time_use "AC10_AC15.ML";
time_use_thy "AC15_WO6";
time_use_thy "WO2_AC16";
time_use_thy "AC16_WO4";
-time_use "AC1_AC17.ML";
time_use_thy "AC17_AC1";
time_use_thy "AC18_AC19";
--- a/src/ZF/AC/WO1_WO6.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: ZF/AC/WO1_WO6.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
- Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
- All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML)
-
- Every proof (exept one) presented in this file are referred as "clear"
- by Rubin & Rubin (page 2).
- They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
- Fortunately order types made this proof also very easy.
-*)
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO2 ==> WO3";
-by (Fast_tac 1);
-qed "WO2_WO3";
-
-(* ********************************************************************** *)
-
-Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1";
-by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage,
- well_ord_Memrel RS well_ord_subset]) 1);
-qed "WO3_WO1";
-
-(* ********************************************************************** *)
-
-Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2";
-by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1);
-qed "WO1_WO2";
-
-(* ********************************************************************** *)
-
-Goal "f \\<in> A->B ==> (\\<lambda>x \\<in> A. {f`x}): A -> {{b}. b \\<in> B}";
-by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
-qed "lam_sets";
-
-Goalw [surj_def] "f \\<in> surj(A,B) ==> (\\<Union>a \\<in> A. {f`a}) = B";
-by (fast_tac (claset() addSEs [apply_type]) 1);
-qed "surj_imp_eq_";
-
-Goal "[| f \\<in> surj(A,B); Ord(A) |] ==> (\\<Union>a<A. {f`a}) = B";
-by (fast_tac (claset() addSDs [surj_imp_eq_]
- addSIs [ltI] addSEs [ltE]) 1);
-qed "surj_imp_eq";
-
-Goalw WO_defs "WO1 ==> WO4(1)";
-by (rtac allI 1);
-by (eres_inst_tac [("x","A")] allE 1);
-by (etac exE 1);
-by (REPEAT (resolve_tac [exI, conjI] 1));
-by (etac Ord_ordertype 1);
-by (rtac 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 (simpset() 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);
-qed "WO1_WO4";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)";
-by (blast_tac (claset() addSDs [spec]
- addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1);
-qed "WO4_mono";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "[| m \\<in> nat; 1 le m; WO4(m) |] ==> WO5";
-by (Blast_tac 1);
-qed "WO4_WO5";
-
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO5 ==> WO6";
-by (Blast_tac 1);
-qed "WO5_WO6";
-
--- a/src/ZF/AC/WO1_WO7.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Tue Jun 26 16:54:39 2001 +0200
@@ -4,6 +4,8 @@
WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
LEMMA is the sentence denoted by (**)
+
+Also, WO1 <-> WO8
*)
(* ********************************************************************** *)
@@ -86,3 +88,28 @@
by (simp_tac (simpset() addsimps [WO7_iff_LEMMA]) 1);
by (blast_tac (claset() addIs [LEMMA_imp_WO1, WO1_imp_LEMMA]) 1);
qed "WO1_iff_WO7";
+
+
+
+(* ********************************************************************** *)
+
+(* The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) *)
+
+(* ********************************************************************** *)
+
+Goalw WO_defs "WO1 ==> WO8";
+by (Fast_tac 1);
+qed "WO1_WO8";
+
+
+(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
+Goalw WO_defs "WO8 ==> WO1";
+by (rtac allI 1);
+by (eres_inst_tac [("x","{{x}. x \\<in> A}")] allE 1);
+by (etac impE 1);
+by (fast_tac (claset() addSEs [lam_sing_bij RS bij_is_inj RS
+ well_ord_rvimage]) 2);
+by (res_inst_tac [("x","\\<lambda>a \\<in> {{x}. x \\<in> A}. THE x. a={x}")] exI 1);
+by (force_tac (claset() addSIs [lam_type],
+ simpset() addsimps [singleton_eq_iff, the_equality]) 1);
+qed "WO8_WO1";
--- a/src/ZF/AC/WO1_WO8.ML Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: ZF/AC/WO1_WO8.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
-The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)
-*)
-
-(* ********************************************************************** *)
-(* Trivial implication "WO1 ==> WO8" *)
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO1 ==> WO8";
-by (Fast_tac 1);
-qed "WO1_WO8";
-
-(* ********************************************************************** *)
-(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *)
-(* ********************************************************************** *)
-
-Goalw WO_defs "WO8 ==> WO1";
-by (rtac allI 1);
-by (eres_inst_tac [("x","{{x}. x \\<in> A}")] allE 1);
-by (etac impE 1);
-by (fast_tac (claset() addSEs [lam_sing_bij RS bij_is_inj RS
- well_ord_rvimage]) 2);
-by (res_inst_tac [("x","\\<lambda>a \\<in> {{x}. x \\<in> A}. THE x. a={x}")] exI 1);
-by (force_tac (claset() addSIs [lam_type],
- simpset() addsimps [singleton_eq_iff, the_equality]) 1);
-qed "WO8_WO1";
--- a/src/ZF/AC/WO6_WO1.ML Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Tue Jun 26 16:54:39 2001 +0200
@@ -2,11 +2,89 @@
ID: $Id$
Author: Krzysztof Grabczewski
-The proof of "WO6 ==> WO1". Simplified by L C Paulson.
+ Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
+ The only hard one is WO6 ==> WO1.
+
+ Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear"
+ by Rubin & Rubin (page 2).
+ They refer reader to a book by Gödel to see the proof WO1 ==> WO2.
+ Fortunately order types made this proof also very easy.
+*)
+
+(* ********************************************************************** *)
+
+Goalw WO_defs "WO2 ==> WO3";
+by (Fast_tac 1);
+qed "WO2_WO3";
+
+(* ********************************************************************** *)
+
+Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1";
+by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage,
+ well_ord_Memrel RS well_ord_subset]) 1);
+qed "WO3_WO1";
+
+(* ********************************************************************** *)
+
+Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2";
+by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1);
+qed "WO1_WO2";
+
+(* ********************************************************************** *)
+
+Goal "f \\<in> A->B ==> (\\<lambda>x \\<in> A. {f`x}): A -> {{b}. b \\<in> B}";
+by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
+qed "lam_sets";
+
+Goalw [surj_def] "f \\<in> surj(A,B) ==> (\\<Union>a \\<in> A. {f`a}) = B";
+by (fast_tac (claset() addSEs [apply_type]) 1);
+qed "surj_imp_eq_";
-From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
-pages 2-5
-*)
+Goal "[| f \\<in> surj(A,B); Ord(A) |] ==> (\\<Union>a<A. {f`a}) = B";
+by (fast_tac (claset() addSDs [surj_imp_eq_]
+ addSIs [ltI] addSEs [ltE]) 1);
+qed "surj_imp_eq";
+
+Goalw WO_defs "WO1 ==> WO4(1)";
+by (rtac allI 1);
+by (eres_inst_tac [("x","A")] allE 1);
+by (etac exE 1);
+by (REPEAT (resolve_tac [exI, conjI] 1));
+by (etac Ord_ordertype 1);
+by (rtac 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 (simpset() 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);
+qed "WO1_WO4";
+
+(* ********************************************************************** *)
+
+Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)";
+by (blast_tac (claset() addSDs [spec]
+ addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1);
+qed "WO4_mono";
+
+(* ********************************************************************** *)
+
+Goalw WO_defs "[| m \\<in> nat; 1 le m; WO4(m) |] ==> WO5";
+by (Blast_tac 1);
+qed "WO4_WO5";
+
+(* ********************************************************************** *)
+
+Goalw WO_defs "WO5 ==> WO6";
+by (Blast_tac 1);
+qed "WO5_WO6";
+
+
+(* **********************************************************************
+ The proof of "WO6 ==> WO1". Simplified by L C Paulson.
+
+ From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
+ pages 2-5
+************************************************************************* *)
goal OrderType.thy
"!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> \
--- a/src/ZF/IsaMakefile Tue Jun 26 15:28:49 2001 +0200
+++ b/src/ZF/IsaMakefile Tue Jun 26 16:54:39 2001 +0200
@@ -77,15 +77,15 @@
ZF-AC: ZF $(LOG)/ZF-AC.gz
-$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \
+$(LOG)/ZF-AC.gz: $(OUT)/ZF \
AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \
AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \
- AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \
- AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \
+ AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_WO2.ML \
+ AC/AC1_WO2.thy AC/AC7_AC9.ML AC/AC_Equiv.ML \
AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \
AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \
AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \
- AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO1_WO8.ML AC/WO2_AC16.ML \
+ AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO2_AC16.ML \
AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \
AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy
@$(ISATOOL) usedir $(OUT)/ZF AC