--- a/src/ZF/AC/AC_Equiv.ML Tue Apr 25 11:01:57 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Tue Apr 25 11:06:52 1995 +0200
@@ -7,6 +7,13 @@
open AC_Equiv;
+val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def];
+
+val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def,
+ AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def,
+ AC12_def, AC13_def, AC14_def, AC15_def, AC16_def,
+ AC17_def, AC18_def, AC19_def];
+
val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def];
(* ******************************************** *)
--- a/src/ZF/AC/AC_Equiv.thy Tue Apr 25 11:01:57 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Tue Apr 25 11:06:52 1995 +0200
@@ -22,9 +22,10 @@
(* Axioms of Choice *)
AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
- AC11, AC12, AC14, AC15, AC17, AC18, AC19 :: "o"
+ AC11, AC12, AC14, AC15, AC17, AC19 :: "o"
AC10, AC13 :: "i => o"
AC16 :: "[i, i] => o"
+ AC18 :: "prop" ("AC18")
(* Auxiliary definitions used in theorems *)
first :: "[i, i, i] => o"
@@ -114,12 +115,9 @@
AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}. \
\ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
-(***problems! X is free, and is higher-order!
- AC18_def "AC18 == ALL A. A~=0 --> (ALL F. (domain(F) = A & \
-\ (ALL a:A. F`a ~= 0)) --> \
-\ ((INT a:A. UN b:F`a. X(a,b)) = \
-\ (UN f: PROD a:A. F`a. INT a:A. X(a, f`a))))"
-***)
+ AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(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))))"
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))"
--- a/src/ZF/AC/ROOT.ML Tue Apr 25 11:01:57 1995 +0200
+++ b/src/ZF/AC/ROOT.ML Tue Apr 25 11:06:52 1995 +0200
@@ -15,4 +15,19 @@
time_use_thy "WO6_WO1";
+(*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";
+*)
+
writeln"END: Root file for ZF/AC";
--- a/src/ZF/AC/WO6_WO1.ML Tue Apr 25 11:01:57 1995 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Tue Apr 25 11:06:52 1995 +0200
@@ -159,12 +159,12 @@
(* Case 2 : vv2_subset *)
(* ********************************************************************** *)
-goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
-\ y*y <= y; (UN b<a. f`b)=y \
+goalw thy [uu_def] "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
+\ y*y <= y; (UN b<a. f`b)=y \
\ |] ==> EX d<a. uu(f,b,g,d) ~= 0";
by (fast_tac (AC_cs addSIs [not_emptyI]
- addSDs [SigmaI RSN (2, subsetD)]
- addSEs [not_emptyE]) 1);
+ addSDs [SigmaI RSN (2, subsetD)]
+ addSEs [not_emptyE]) 1);
val ex_d_uu_not_empty = result();
goal thy "!!f. [| b<a; g<a; f`b~=0; f`g~=0; \
@@ -208,24 +208,20 @@
val supset_lepoll_imp_eq = result();
goal thy
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
-\ domain(uu(f, b, g, d)) eqpoll succ(m); \
-\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
-\ (UN b<a. f`b)=y; b<a; g<a; d<a; f`b~=0; f`g~=0; m:nat; s:f`b |] \
-\ ==> uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
-by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2));
-by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1);
-by (eresolve_tac [impE] 1);
-by (eresolve_tac [uu_not_empty RS (uu_subset1 RS not_empty_rel_imp_domain)] 1
- THEN REPEAT (assume_tac 1));
-by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2
- THEN (TRYALL assume_tac));
+ "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+\ domain(uu(f, b, g, d)) eqpoll succ(m); \
+\ ALL b<a. f`b lepoll succ(m); y*y <= y; \
+\ (UN b<a. f`b)=y; b<a; g<a; d<a; \
+\ f`b~=0; f`g~=0; m:nat; s:f`b \
+\ |] ==> uu(f, b, g, LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g";
+by (dres_inst_tac [("x2","g")] (ospec RS ospec RS mp) 1);
+by (rtac ([uu_subset1, uu_not_empty] MRS not_empty_rel_imp_domain) 3);
+by (rtac Least_uu_not_empty_lt_a 2 THEN TRYALL assume_tac);
by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
(Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2,
uu_subset1 RSN (4, rel_is_fun)))] 1
- THEN (TRYALL assume_tac));
-by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2,
- supset_lepoll_imp_eq)] 1);
+ THEN TRYALL assume_tac);
+by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1);
by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1));
val uu_Least_is_fun = result();
@@ -382,8 +378,7 @@
(* ********************************************************************** *)
goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
-by (eresolve_tac [allE] 1);
-by (fast_tac (ZF_cs addSIs [not_emptyI]) 1);
+by (fast_tac (ZF_cs addEs [equals0D]) 1);
val WO6_imp_NN_not_empty = result();
(* ********************************************************************** *)