--- a/src/ZF/AC/AC18_AC19.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC18_AC19.ML Mon May 21 14:45:52 2001 +0200
@@ -9,17 +9,17 @@
(* AC1 ==> AC18 *)
(* ********************************************************************** *)
-Goal "[| 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))";
+Goal "[| f \\<in> (\\<Pi>b \\<in> {P(a). a \\<in> A}. b); \\<forall>a \\<in> A. P(a)<=Q(a) |] \
+\ ==> (\\<lambda>a \\<in> A. f`P(a)) \\<in> (\\<Pi>a \\<in> A. Q(a))";
by (rtac lam_type 1);
by (dtac apply_type 1);
by Auto_tac;
qed "PROD_subsets";
-Goal "[| 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))";
+Goal "[| \\<forall>A. 0 \\<notin> A --> (\\<exists>f. f \\<in> (\\<Pi>X \\<in> A. X)); A \\<noteq> 0 |] ==> \
+\ (\\<Inter>a \\<in> A. \\<Union>b \\<in> B(a). X(a, b)) \\<subseteq> (\\<Union>f \\<in> \\<Pi>a \\<in> A. B(a). \\<Inter>a \\<in> A. X(a, f`a))";
by (rtac subsetI 1);
-by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
+by (eres_inst_tac [("x","{{b \\<in> B(a). x \\<in> X(a,b)}. a \\<in> A}")] allE 1);
by (etac impE 1);
by (Fast_tac 1);
by (etac exE 1);
@@ -51,13 +51,13 @@
(* ********************************************************************** *)
Goalw [u_def]
- "[| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}";
+ "[| A \\<noteq> 0; 0 \\<notin> A |] ==> {u_(a). a \\<in> A} \\<noteq> 0 & 0 \\<notin> {u_(a). a \\<in> A}";
by (fast_tac (claset() addSIs [not_emptyI]
addSEs [not_emptyE]
addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1);
qed "RepRep_conj";
-Goal "[|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a";
+Goal "[|c \\<in> a; x = c Un {0}; x \\<notin> a |] ==> x - {0} \\<in> a";
by (hyp_subst_tac 1);
by (rtac subst_elem 1 THEN (assume_tac 1));
by (rtac equalityI 1);
@@ -69,15 +69,15 @@
val lemma1_1 = result();
Goalw [u_def]
- "[| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \
-\ ==> f`(u_(a))-{0} : a";
+ "[| f`(u_(a)) \\<notin> a; f \\<in> (\\<Pi>B \\<in> {u_(a). a \\<in> A}. B); a \\<in> A |] \
+\ ==> f`(u_(a))-{0} \\<in> a";
by (fast_tac (claset() addSEs [lemma1_1] addSDs [apply_type]) 1);
val lemma1_2 = result();
-Goal "EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)";
+Goal "\\<exists>f. f \\<in> (\\<Pi>B \\<in> {u_(a). a \\<in> A}. B) ==> \\<exists>f. f \\<in> (\\<Pi>B \\<in> A. B)";
by (etac exE 1);
by (res_inst_tac
- [("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1);
+ [("x","\\<lambda>a \\<in> A. if(f`(u_(a)) \\<in> a, f`(u_(a)), f`(u_(a))-{0})")] exI 1);
by (rtac lam_type 1);
by (split_tac [split_if] 1);
by (rtac conjI 1);
@@ -85,17 +85,17 @@
by (fast_tac (claset() addSEs [lemma1_2]) 1);
val lemma1 = result();
-Goalw [u_def] "a~=0 ==> 0: (UN b:u_(a). b)";
+Goalw [u_def] "a\\<noteq>0 ==> 0 \\<in> (\\<Union>b \\<in> u_(a). b)";
by (fast_tac (claset() addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1);
val lemma2_1 = result();
-Goal "[| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0";
+Goal "[| A\\<noteq>0; 0\\<notin>A |] ==> (\\<Inter>x \\<in> {u_(a). a \\<in> A}. \\<Union>b \\<in> x. b) \\<noteq> 0";
by (etac not_emptyE 1);
by (res_inst_tac [("a","0")] not_emptyI 1);
by (fast_tac (claset() addSIs [lemma2_1]) 1);
val lemma2 = result();
-Goal "(UN f:F. P(f)) ~= 0 ==> F ~= 0";
+Goal "(\\<Union>f \\<in> F. P(f)) \\<noteq> 0 ==> F \\<noteq> 0";
by (fast_tac (claset() addSEs [not_emptyE]) 1);
val lemma3 = result();
@@ -103,12 +103,12 @@
by (Clarify_tac 1);
by (case_tac "A=0" 1);
by (Force_tac 1);
-by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1);
+by (eres_inst_tac [("x","{u_(a). a \\<in> A}")] allE 1);
by (etac impE 1);
by (etac RepRep_conj 1 THEN (assume_tac 1));
by (rtac lemma1 1);
by (dtac lemma2 1 THEN (assume_tac 1));
-by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1));
+by (dres_inst_tac [("P","%x. x\\<noteq>0")] subst 1 THEN (assume_tac 1));
by (fast_tac (claset() addSEs [lemma3 RS not_emptyE]) 1);
qed "AC19_AC1";