--- a/src/ZF/AC/AC0_AC1.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC0_AC1.ML Mon May 21 14:45:52 2001 +0200
@@ -6,11 +6,11 @@
AC0 comes from Suppes, AC1 from Rubin & Rubin
*)
-Goal "0~:A ==> A <= Pow(Union(A))-{0}";
+Goal "0\\<notin>A ==> A \\<subseteq> Pow(Union(A))-{0}";
by (Fast_tac 1);
qed "subset_Pow_Union";
-Goal "[| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)";
+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();
--- a/src/ZF/AC/AC10_AC15.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC10_AC15.ML Mon May 21 14:45:52 2001 +0200
@@ -27,13 +27,13 @@
(* - ex_fun_AC13_AC15 *)
(* ********************************************************************** *)
-Goalw [lepoll_def] "A~=0 ==> B lepoll A*B";
+Goalw [lepoll_def] "A\\<noteq>0 ==> B lepoll A*B";
by (etac not_emptyE 1);
-by (res_inst_tac [("x","lam z:B. <x,z>")] exI 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~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)";
+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);
@@ -44,22 +44,22 @@
by (Fast_tac 1);
qed "cons_times_nat_not_Finite";
-Goal "[| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A";
+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:A; C:A; a:B; a:C |] ==> B=C";
+ "[| 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]
- "ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \
+ "\\<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 \
-\ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \
-\ 0:u & 2 lepoll u & u lepoll n";
+\ ==> \\<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);
@@ -72,10 +72,10 @@
by (rtac lemma2 1 THEN (REPEAT (assume_tac 1)));
val lemma3 = result();
-Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i";
+Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a \\<in> A} lepoll i";
by (etac 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);
+ [("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));
@@ -88,11 +88,11 @@
by (fast_tac (claset() addEs [sym, left_inverse RS ssubst]) 1);
val lemma4 = result();
-Goal "[| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \
+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) |] \
-\ ==> (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";
+\ ==> (\\<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]
@@ -105,11 +105,11 @@
Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1);
val lemma5 = result();
-Goal "[| EX f. ALL B:{cons(0, x*nat). x:A}. \
+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:nat |] \
-\ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll 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);
@@ -123,7 +123,7 @@
(* AC10(n) ==> AC11 *)
(* ********************************************************************** *)
-Goalw AC_defs "[| n:nat; 1 le n; 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";
@@ -162,11 +162,11 @@
(* 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 : *)
+(* the following obviously equivalent theorem \\<in> *)
(* AC10(n) implies AC13(n) for (1 le n) *)
(* ********************************************************************** *)
-Goalw AC_defs "[| n:nat; 1 le n; AC10(n) |] ==> AC13(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);
@@ -186,14 +186,14 @@
by (rtac impI 1);
by (mp_tac 1);
by (etac exE 1);
-by (res_inst_tac [("x","lam x:A. {f`x}")] exI 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 <= n *)
+(* AC13(m) ==> AC13(n) for m \\<subseteq> n *)
(* ********************************************************************** *)
Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)";
@@ -206,10 +206,10 @@
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* AC13(n) ==> AC14 if 1 <= n *)
+(* AC13(n) ==> AC14 if 1 \\<subseteq> n *)
(* ********************************************************************** *)
-Goalw AC_defs "[| n:nat; 1 le n; AC13(n) |] ==> AC14";
+Goalw AC_defs "[| n \\<in> nat; 1 le n; AC13(n) |] ==> AC14";
by (fast_tac (FOL_cs addIs [bexI]) 1);
qed "AC13_AC14";
@@ -229,12 +229,12 @@
(* AC13(1) ==> AC1 *)
(* ********************************************************************** *)
-Goal "[| A~=0; A lepoll 1 |] ==> EX a. A={a}";
+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 "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)";
+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));
--- a/src/ZF/AC/AC15_WO6.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC15_WO6.ML Mon May 21 14:45:52 2001 +0200
@@ -5,14 +5,12 @@
The proof of AC1 ==> WO2
*)
-open AC15_WO6;
-
-Goal "Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
+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";
-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";
+val [prem] = goal thy "\\<forall>x \\<in> Pow(A)-{0}. f`x\\<noteq>0 & f`x \\<subseteq> x & f`x lepoll m ==> \
+\ (\\<Union>i<LEAST x. HH(f,A,x)={A}. HH(f,A,i)) = A";
by (simp_tac (simpset() addsimps [Ord_Least RS OUN_eq_UN]) 1);
by (rtac equalityI 1);
by (fast_tac (claset() addSDs [less_Least_subset_x]) 1);
@@ -20,8 +18,8 @@
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";
+val [prem] = goal thy "\\<forall>x \\<in> Pow(A)-{0}. f`x\\<noteq>0 & f`x \\<subseteq> x & f`x lepoll m ==> \
+\ \\<forall>x<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
by (rtac oallI 1);
by (dresolve_tac [ltD RS less_Least_subset_x] 1);
by (ftac HH_subset_imp_eq 1);
@@ -39,7 +37,7 @@
by (rtac bexI 1 THEN (assume_tac 2));
by (rtac 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 (res_inst_tac [("x","\\<lambda>j \\<in> (LEAST i. HH(f,A,i)={A}). HH(f,A,j)")] exI 1);
by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSIs [Ord_Least, lam_type RS domain_of_fun]
addSEs [less_Least_subset_x, lemma1, lemma2]) 1);
--- a/src/ZF/AC/AC16_WO4.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Mon May 21 14:45:52 2001 +0200
@@ -9,14 +9,14 @@
(* The case of finite set *)
(* ********************************************************************** *)
-Goalw [Finite_def] "[| Finite(A); 0<m; m:nat |] ==> \
-\ EX a f. Ord(a) & domain(f) = a & \
-\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)";
+Goalw [Finite_def] "[| Finite(A); 0<m; m \\<in> nat |] ==> \
+\ \\<exists>a f. Ord(a) & domain(f) = a & \
+\ (\\<Union>b<a. f`b) = A & (\\<forall>b<a. f`b lepoll m)";
by (etac bexE 1);
by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1);
by (etac exE 1);
by (res_inst_tac [("x","n")] exI 1);
-by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1);
+by (res_inst_tac [("x","\\<lambda>i \\<in> n. {f`i}")] exI 1);
by (Asm_full_simp_tac 1);
by (rewrite_goals_tac [bij_def, surj_def]);
by (fast_tac (claset() addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun,
@@ -29,7 +29,7 @@
(* The case of infinite set *)
(* ********************************************************************** *)
-(* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **)
+(* well_ord(x,r) ==> well_ord({{y,z}. y \\<in> x}, Something(x,z)) **)
bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage));
Goal "[| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C";
@@ -42,8 +42,8 @@
val lepoll_paired = paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll;
-Goal "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)";
-by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1);
+Goal "\\<exists>y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)";
+by (res_inst_tac [("x","{{a,x}. a \\<in> nat Un Hartog(z)}")] exI 1);
by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS
(Ord_Hartog RS
well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1);
@@ -61,20 +61,20 @@
qed "infinite_Un";
(* ********************************************************************** *)
-(* There is a v : s(u) such that k lepoll x Int y (in our case succ(k)) *)
-(* The idea of the proof is the following : *)
+(* There is a v \\<in> s(u) such that k lepoll x Int y (in our case succ(k)) *)
+(* The idea of the proof is the following \\<in> *)
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y *)
-(* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *)
-(* We have obtained this result in two steps : *)
-(* 1. y is less than or equipollent to {v:s(u). a <= v} *)
+(* Thence y is less than or equipollent to {v \\<in> Pow(x). v eqpoll n#-k} *)
+(* We have obtained this result in two steps \\<in> *)
+(* 1. y is less than or equipollent to {v \\<in> s(u). a \\<subseteq> v} *)
(* where a is certain k-2 element subset of y *)
-(* 2. {v:s(u). a <= v} is less than or equipollent *)
-(* to {v:Pow(x). v eqpoll n-k} *)
+(* 2. {v \\<in> s(u). a \\<subseteq> v} is less than or equipollent *)
+(* to {v \\<in> Pow(x). v eqpoll n-k} *)
(* ********************************************************************** *)
(*Proof simplified by LCP*)
-Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \
-\ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
+Goal "[| ~(\\<exists>x \\<in> A. f`x=y); f \\<in> inj(A, B); y \\<in> B |] \
+\ ==> (\\<lambda>a \\<in> succ(A). if(a=A, y, f`a)) \\<in> inj(succ(A), B)";
by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
by (auto_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]));
qed "succ_not_lepoll_lemma";
@@ -90,7 +90,7 @@
(* ********************************************************************** *)
Goalw [lepoll_def, eqpoll_def]
- "[| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y";
+ "[| 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";
@@ -98,23 +98,23 @@
val ordertype_eqpoll =
ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2));
-Goalw [lesspoll_def] "n: nat ==> n lesspoll nat";
+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<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)";
+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<=y; b:y-a; u:x; x Int y = 0 \
+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 <= A; a : A-B; k:nat \
+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);
@@ -131,7 +131,7 @@
(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1);
qed "set_eq_cons";
-Goal "[| cons(x,a) = cons(y,a); x~: a |] ==> x = y ";
+Goal "[| cons(x,a) = cons(y,a); x\\<notin> a |] ==> x = y ";
by (fast_tac (claset() addSEs [equalityE]) 1);
qed "cons_eqE";
@@ -143,8 +143,8 @@
(* some arithmetic *)
(* ********************************************************************** *)
-Goal "[| k:nat; m:nat |] ==> \
-\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m";
+Goal "[| k \\<in> nat; m \\<in> nat |] ==> \
+\ \\<forall>A B. A eqpoll k #+ m & k lepoll B & B \\<subseteq> A --> A-B lepoll m";
by (induct_tac "k" 1);
by (asm_simp_tac (simpset() addsimps [add_0]) 1);
by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS
@@ -161,7 +161,7 @@
by (Fast_tac 1);
qed "eqpoll_sum_imp_Diff_lepoll_lemma";
-Goal "[| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; k:nat; m:nat |] \
+Goal "[| A eqpoll succ(k #+ m); B \\<subseteq> A; succ(k) lepoll B; k \\<in> nat; m \\<in> nat |] \
\ ==> A-B lepoll m";
by (dresolve_tac [add_succ RS ssubst] 1);
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1
@@ -173,8 +173,8 @@
(* similar properties for eqpoll *)
(* ********************************************************************** *)
-Goal "[| k:nat; m:nat |] ==> \
-\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m";
+Goal "[| k \\<in> nat; m \\<in> nat |] ==> \
+\ \\<forall>A B. A eqpoll k #+ m & k eqpoll B & B \\<subseteq> A --> A-B eqpoll m";
by (induct_tac "k" 1);
by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0]
addss (simpset() addsimps [add_0])) 1);
@@ -191,7 +191,7 @@
by (Fast_tac 1);
qed "eqpoll_sum_imp_Diff_eqpoll_lemma";
-Goal "[| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; k:nat; m:nat |] \
+Goal "[| A eqpoll succ(k #+ m); B \\<subseteq> A; succ(k) eqpoll B; k \\<in> nat; m \\<in> nat |] \
\ ==> A-B eqpoll m";
by (dresolve_tac [add_succ RS ssubst] 1);
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1
@@ -204,18 +204,18 @@
(* LL can be well ordered *)
(* ********************************************************************** *)
-Goal "{x:Pow(X). x lepoll 0} = {0}";
+Goal "{x \\<in> Pow(X). x lepoll 0} = {0}";
by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [lepoll_refl]) 1);
qed "subsets_lepoll_0_eq_unit";
-Goal "n:nat ==> {z:Pow(y). z lepoll succ(n)} = \
-\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
+Goal "n \\<in> nat ==> {z \\<in> Pow(y). z lepoll succ(n)} = \
+\ {z \\<in> Pow(y). z lepoll n} Un {z \\<in> Pow(y). z eqpoll succ(n)}";
by (fast_tac (claset() addIs [le_refl, leI, le_imp_lepoll]
addSDs [lepoll_succ_disj]
addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
qed "subsets_lepoll_succ";
-Goal "n:nat ==> {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0";
+Goal "n \\<in> nat ==> {z \\<in> Pow(y). z lepoll n} Int {z \\<in> Pow(y). z eqpoll succ(n)} = 0";
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_imp_lepoll
RS lepoll_trans RS succ_lepoll_natE]
addSIs [equals0I]) 1);
@@ -243,7 +243,7 @@
Addsimps [disjoint, WO_R, lnat, mnat, mpos, Infinite];
AddSIs [disjoint, WO_R, lnat, mnat, mpos];
-Goalw [k_def] "k: nat";
+Goalw [k_def] "k \\<in> nat";
by Auto_tac;
qed "knat";
Addsimps [knat]; AddSIs [knat];
@@ -258,11 +258,11 @@
val all_ex_l = simplify (FOL_ss addsimps [k_def]) all_ex;
(* ********************************************************************** *)
-(* 1. y is less than or equipollent to {v:s(u). a <= v} *)
+(* 1. y is less than or equipollent to {v \\<in> s(u). a \\<subseteq> v} *)
(* where a is certain k-2 element subset of y *)
(* ********************************************************************** *)
-Goal "[| l eqpoll a; a <= y |] ==> y - a eqpoll y";
+Goal "[| l eqpoll a; a \\<subseteq> y |] ==> y - a eqpoll y";
by (cut_facts_tac [WO_R, Infinite, lnat] 1);
by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll]
addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans,
@@ -276,24 +276,24 @@
RS lepoll_infinite]) 1);
qed "Diff_Finite_eqpoll";
-Goalw [s_def] "s(u) <= t_n";
+Goalw [s_def] "s(u) \\<subseteq> t_n";
by (Fast_tac 1);
qed "s_subset";
Goalw [s_def, succ_def, k_def]
- "[| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; l eqpoll a \
-\ |] ==> w: s(u)";
+ "[| w \\<in> t_n; cons(b,cons(u,a)) \\<subseteq> w; a \\<subseteq> y; b \\<in> y-a; l eqpoll a \
+\ |] ==> w \\<in> s(u)";
by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong]
addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
qed "sI";
-Goalw [s_def] "v : s(u) ==> u : v";
+Goalw [s_def] "v \\<in> s(u) ==> u \\<in> v";
by (Fast_tac 1);
qed "in_s_imp_u_in";
-Goal "[| l eqpoll a; a <= y; b : y - a; u : x |] \
-\ ==> EX! c. c: s(u) & a <= c & b:c";
+Goal "[| l eqpoll a; a \\<subseteq> y; b \\<in> y - a; u \\<in> x |] \
+\ ==> \\<exists>! c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c";
by (rtac (all_ex_l RS ballE) 1);
by (blast_tac (claset() delrules [PowI]
addSIs [cons_cons_subset,
@@ -307,23 +307,23 @@
by (fast_tac (claset() addSEs [s_subset RS subsetD, in_s_imp_u_in]) 1);
qed "ex1_superset_a";
-Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \
-\ l eqpoll a; a <= y; b : y - a; u : x |] \
-\ ==> (THE c. c: s(u) & a <= c & b:c) \
+Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \
+\ l eqpoll a; a \\<subseteq> y; b \\<in> y - a; u \\<in> x |] \
+\ ==> (THE c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c) \
\ Int y = cons(b, a)";
by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
by (rtac set_eq_cons 1);
by (REPEAT (Fast_tac 1));
qed "the_eq_cons";
-Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \
-\ l eqpoll a; a <= y; u:x |] \
-\ ==> y lepoll {v:s(u). a <= v}";
+Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \
+\ l eqpoll a; a \\<subseteq> y; u \\<in> x |] \
+\ ==> y lepoll {v \\<in> s(u). a \\<subseteq> v}";
by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS
eqpoll_imp_lepoll RS lepoll_trans] 1
THEN REPEAT (Fast_tac 1));
by (res_inst_tac
- [("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
+ [("f3", "\\<lambda>b \\<in> y-a. THE c. c \\<in> s(u) & a \\<subseteq> c & b \\<in> c")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
by (simp_tac (simpset() addsimps [inj_def]) 1);
by (rtac conjI 1);
@@ -342,13 +342,13 @@
(* back to the second part *)
(* ********************************************************************** *)
-Goal "w <= x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)";
+Goal "w \\<subseteq> x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)";
by (Fast_tac 1);
qed "w_Int_eq_w_Diff";
-Goal "[| w:{v:s(u). a <= v}; \
-\ l eqpoll a; u : x; \
-\ ALL v:s(u). succ(l) eqpoll v Int y \
+Goal "[| w \\<in> {v \\<in> s(u). a \\<subseteq> v}; \
+\ l eqpoll a; u \\<in> x; \
+\ \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y \
\ |] ==> w Int (x - {u}) eqpoll m";
by (etac CollectE 1);
by (stac w_Int_eq_w_Diff 1);
@@ -361,27 +361,27 @@
qed "w_Int_eqpoll_m";
(* ********************************************************************** *)
-(* 2. {v:s(u). a <= v} is less than or equipollent *)
-(* to {v:Pow(x). v eqpoll n-k} *)
+(* 2. {v \\<in> s(u). a \\<subseteq> v} is less than or equipollent *)
+(* to {v \\<in> Pow(x). v eqpoll n-k} *)
(* ********************************************************************** *)
-Goal "x eqpoll m ==> x ~= 0";
+Goal "x eqpoll m ==> x \\<noteq> 0";
by (cut_facts_tac [mpos] 1);
by (fast_tac (claset() addSEs [zero_lt_natE]
addSDs [eqpoll_succ_imp_not_empty]) 1);
qed "eqpoll_m_not_empty";
-Goal "[| z : xa Int (x - {u}); l eqpoll a; a <= y; u:x |] \
-\ ==> EX! w. w : t_n & cons(z, cons(u, a)) <= w";
+Goal "[| z \\<in> xa Int (x - {u}); l eqpoll a; a \\<subseteq> y; u \\<in> x |] \
+\ ==> \\<exists>! w. w \\<in> t_n & cons(z, cons(u, a)) \\<subseteq> w";
by (rtac (all_ex RS bspec) 1);
by (rewtac k_def);
by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [eqpoll_sym]) 1);
qed "cons_cons_in";
-Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \
-\ a <= y; l eqpoll a; u : x |] \
-\ ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
-by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")]
+Goal "[| \\<forall>v \\<in> s(u). succ(l) eqpoll v Int y; \
+\ a \\<subseteq> y; l eqpoll a; u \\<in> x |] \
+\ ==> {v \\<in> s(u). a \\<subseteq> v} lepoll {v \\<in> Pow(x). v eqpoll m}";
+by (res_inst_tac [("f3","\\<lambda>w \\<in> {v \\<in> s(u). a \\<subseteq> v}. w Int (x - {u})")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
by (simp_tac (simpset() addsimps [inj_def]) 1);
by (rtac conjI 1);
@@ -405,13 +405,13 @@
(* well_ord_subsets_lepoll_n *)
(* ********************************************************************** *)
-Goal "n:nat ==> EX S. well_ord({z: Pow(y) . z eqpoll succ(n)}, S)";
+Goal "n \\<in> nat ==> \\<exists>S. well_ord({z \\<in> Pow(y) . z eqpoll succ(n)}, S)";
by (resolve_tac [WO_R RS well_ord_infinite_subsets_eqpoll_X
RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1);
by (REPEAT (fast_tac (claset() addIs [bij_is_inj RS well_ord_rvimage]) 1));
qed "well_ord_subsets_eqpoll_n";
-Goal "n:nat ==> EX R. well_ord({z:Pow(y). z lepoll n}, R)";
+Goal "n \\<in> nat ==> \\<exists>R. well_ord({z \\<in> Pow(y). z lepoll n}, R)";
by (induct_tac "n" 1);
by (force_tac (claset() addSIs [well_ord_unit],
simpset() addsimps [subsets_lepoll_0_eq_unit]) 1);
@@ -425,14 +425,14 @@
qed "well_ord_subsets_lepoll_n";
-Goalw [LL_def, MM_def] "LL <= {z:Pow(y). z lepoll succ(k #+ m)}";
+Goalw [LL_def, MM_def] "LL \\<subseteq> {z \\<in> Pow(y). z lepoll succ(k #+ m)}";
by (cut_facts_tac [includes] 1);
by (fast_tac (claset() addIs [subset_imp_lepoll
RS (eqpoll_imp_lepoll
RSN (2, lepoll_trans))]) 1);
qed "LL_subset";
-Goal "EX S. well_ord(LL,S)";
+Goal "\\<exists>S. well_ord(LL,S)";
by (rtac (well_ord_subsets_lepoll_n RS exE) 1);
by (blast_tac (claset() addIs [LL_subset RSN (2, well_ord_subset)]) 2);
by Auto_tac;
@@ -442,7 +442,7 @@
(* every element of LL is a contained in exactly one element of MM *)
(* ********************************************************************** *)
-Goalw [MM_def, LL_def] "v:LL ==> EX! w. w:MM & v<=w";
+Goalw [MM_def, LL_def] "v \\<in> LL ==> \\<exists>! w. w \\<in> MM & v \\<subseteq> w";
by Safe_tac;
by (Fast_tac 1);
by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1));
@@ -463,31 +463,31 @@
(* The union of appropriate values is the whole x *)
(* ********************************************************************** *)
-Goalw [LL_def] "w : MM ==> w Int y : LL";
+Goalw [LL_def] "w \\<in> MM ==> w Int y \\<in> LL";
by (Fast_tac 1);
qed "Int_in_LL";
Goalw [LL_def]
- "v : LL ==> v = (THE x. x : MM & v <= x) Int y";
+ "v \\<in> LL ==> v = (THE x. x \\<in> MM & v \\<subseteq> x) Int y";
by (Clarify_tac 1);
by (stac unique_superset2 1);
by (auto_tac (claset(), simpset() addsimps [Int_in_LL]));
qed "in_LL_eq_Int";
-Goal "v : LL ==> (THE x. x : MM & v <= x) <= x Un y";
+Goal "v \\<in> LL ==> (THE x. x \\<in> MM & v \\<subseteq> x) \\<subseteq> x Un y";
by (dtac unique_superset1 1);
by (rewtac MM_def);
by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1);
qed "the_in_MM_subset";
-Goalw [GG_def] "v : LL ==> GG ` v <= x";
+Goalw [GG_def] "v \\<in> LL ==> GG ` v \\<subseteq> x";
by (ftac the_in_MM_subset 1);
by (ftac in_LL_eq_Int 1);
by (force_tac (claset() addEs [equalityE], simpset()) 1);
qed "GG_subset";
-Goal "n:nat ==> EX z. z<=y & n eqpoll z";
+Goal "n \\<in> nat ==> \\<exists>z. z \\<subseteq> y & n eqpoll z";
by (etac nat_lepoll_imp_ex_eqpoll_n 1);
by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
RSN (2, lepoll_trans)] 1);
@@ -501,9 +501,9 @@
qed "ex_subset_eqpoll_n";
-Goal "u:x ==> EX v : s(u). succ(k) lepoll v Int y";
+Goal "u \\<in> x ==> \\<exists>v \\<in> s(u). succ(k) lepoll v Int y";
by (rtac ccontr 1);
-by (subgoal_tac "ALL v:s(u). k eqpoll v Int y" 1);
+by (subgoal_tac "\\<forall>v \\<in> s(u). k eqpoll v Int y" 1);
by (full_simp_tac (simpset() addsimps [s_def]) 2);
by (blast_tac (claset() addIs [succ_not_lepoll_imp_eqpoll]) 2);
by (rewtac k_def);
@@ -514,13 +514,13 @@
[[y_lepoll_subset_s, subset_s_lepoll_w] MRS lepoll_trans]) 1);
qed "exists_proper_in_s";
-Goal "u:x ==> EX w:MM. u:w";
+Goal "u \\<in> x ==> \\<exists>w \\<in> MM. u \\<in> w";
by (eresolve_tac [exists_proper_in_s RS bexE] 1);
by (rewrite_goals_tac [MM_def, s_def]);
by (Fast_tac 1);
qed "exists_in_MM";
-Goal "u:x ==> EX w:LL. u:GG`w";
+Goal "u \\<in> x ==> \\<exists>w \\<in> LL. u \\<in> GG`w";
by (rtac (exists_in_MM RS bexE) 1);
by (assume_tac 1);
by (rtac bexI 1);
@@ -533,7 +533,7 @@
Goal "well_ord(LL,S) ==> \
-\ (UN b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x";
+\ (\\<Union>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x";
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
@@ -552,11 +552,11 @@
(* Every element of the family is less than or equipollent to n-k (m) *)
(* ********************************************************************** *)
-Goalw [MM_def] "w : MM ==> w eqpoll succ(k #+ m)";
+Goalw [MM_def] "w \\<in> MM ==> w eqpoll succ(k #+ m)";
by (fast_tac (claset() addDs [includes RS subsetD]) 1);
qed "in_MM_eqpoll_n";
-Goalw [LL_def, MM_def] "w : LL ==> succ(k) lepoll w";
+Goalw [LL_def, MM_def] "w \\<in> LL ==> succ(k) lepoll w";
by (Fast_tac 1);
qed "in_LL_eqpoll_n";
@@ -564,7 +564,7 @@
Goalw [GG_def]
"well_ord(LL,S) ==> \
-\ ALL b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) lepoll m";
+\ \\<forall>b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) lepoll m";
by (rtac oallI 1);
by (asm_simp_tac
(simpset() addsimps [ltD,
@@ -582,13 +582,13 @@
qed "all_in_lepoll_m";
-Goal "EX a f. Ord(a) & domain(f) = a & \
-\ (UN b<a. f ` b) = x & (ALL b<a. f ` b lepoll m)";
+Goal "\\<exists>a f. Ord(a) & domain(f) = a & \
+\ (\\<Union>b<a. f ` b) = x & (\\<forall>b<a. f ` b lepoll m)";
by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1));
by (rename_tac "S" 1);
by (res_inst_tac [("x","ordertype(LL,S)")] exI 1);
by (res_inst_tac [("x",
- "lam b:ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)")]
+ "\\<lambda>b \\<in> ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)")]
exI 1);
by (Simp_tac 1);
by (REPEAT (ares_tac [conjI, lam_funtype RS domain_of_fun,
@@ -605,7 +605,7 @@
(* ********************************************************************** *)
Goalw [AC16_def,WO4_def]
- "[| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)";
+ "[| AC16(k #+ m, k); 0 < k; 0 < m; k \\<in> nat; m \\<in> nat |] ==> WO4(m)";
by (rtac allI 1);
by (case_tac "Finite(A)" 1);
by (rtac lemma1 1 THEN REPEAT (assume_tac 1));
--- a/src/ZF/AC/AC16_WO4.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC16_WO4.thy Mon May 21 14:45:52 2001 +0200
@@ -21,21 +21,21 @@
GG :: i
s :: i=>i
assumes
- all_ex "ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}.
- EX! w. w:t_n & z <= w "
+ all_ex "\\<forall>z \\<in> {z \\<in> Pow(x Un y) . z eqpoll succ(k)}.
+ \\<exists>! w. w \\<in> t_n & z \\<subseteq> w "
disjoint "x Int y = 0"
- includes "t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}"
+ includes "t_n \\<subseteq> {v \\<in> Pow(x Un y). v eqpoll succ(k #+ m)}"
WO_R "well_ord(y,R)"
- lnat "l:nat"
- mnat "m:nat"
+ lnat "l \\<in> nat"
+ mnat "m \\<in> nat"
mpos "0<m"
Infinite "~ Finite(y)"
- noLepoll "~ y lepoll {v:Pow(x). v eqpoll m}"
+ noLepoll "~ y lepoll {v \\<in> Pow(x). v eqpoll m}"
defines
k_def "k == succ(l)"
- MM_def "MM == {v:t_n. succ(k) lepoll v Int y}"
- LL_def "LL == {v Int y. v:MM}"
- GG_def "GG == lam v:LL. (THE w. w:MM & v <= w) - v"
- s_def "s(u) == {v:t_n. u:v & k lepoll v Int y}"
+ MM_def "MM == {v \\<in> t_n. succ(k) lepoll v Int y}"
+ LL_def "LL == {v Int y. v \\<in> MM}"
+ GG_def "GG == \\<lambda>v \\<in> LL. (THE w. w \\<in> MM & v \\<subseteq> w) - v"
+ s_def "s(u) == {v \\<in> t_n. u \\<in> v & k lepoll v Int y}"
end
--- a/src/ZF/AC/AC16_lemmas.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC16_lemmas.ML Mon May 21 14:45:52 2001 +0200
@@ -5,19 +5,19 @@
Lemmas used in the proofs concerning AC16
*)
-Goal "a~:A ==> cons(a,A)-{a}=A";
+Goal "a\\<notin>A ==> cons(a,A)-{a}=A";
by (Fast_tac 1);
qed "cons_Diff_eq";
-Goalw [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
+Goalw [lepoll_def] "1 lepoll X <-> (\\<exists>x. x \\<in> X)";
by (rtac iffI 1);
by (fast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
by (etac exE 1);
-by (res_inst_tac [("x","lam a:1. x")] exI 1);
+by (res_inst_tac [("x","\\<lambda>a \\<in> 1. x")] exI 1);
by (fast_tac (claset() addSIs [lam_injective]) 1);
qed "nat_1_lepoll_iff";
-Goal "X eqpoll 1 <-> (EX x. X={x})";
+Goal "X eqpoll 1 <-> (\\<exists>x. X={x})";
by (rtac iffI 1);
by (etac eqpollE 1);
by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1);
@@ -25,11 +25,11 @@
by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1);
qed "eqpoll_1_iff_singleton";
-Goalw [succ_def] "[| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)";
+Goalw [succ_def] "[| x eqpoll n; y\\<notin>x |] ==> cons(y,x) eqpoll succ(n)";
by (fast_tac (claset() addSEs [cons_eqpoll_cong, mem_irrefl]) 1);
qed "cons_eqpoll_succ";
-Goal "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}";
+Goal "{Y \\<in> Pow(X). Y eqpoll 1} = {{x}. x \\<in> X}";
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac CollectE 1);
@@ -42,8 +42,8 @@
by (fast_tac (claset() addSIs [singleton_eqpoll_1]) 1);
qed "subsets_eqpoll_1_eq";
-Goalw [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}";
-by (res_inst_tac [("x","lam x:X. {x}")] exI 1);
+Goalw [eqpoll_def, bij_def] "X eqpoll {{x}. x \\<in> X}";
+by (res_inst_tac [("x","\\<lambda>x \\<in> X. {x}")] exI 1);
by (rtac IntI 1);
by (rewrite_goals_tac [inj_def, surj_def]);
by (Asm_full_simp_tac 1);
@@ -53,13 +53,13 @@
by (fast_tac (claset() addSIs [lam_type]) 1);
qed "eqpoll_RepFun_sing";
-Goal "{Y:Pow(X). Y eqpoll 1} eqpoll X";
+Goal "{Y \\<in> Pow(X). Y eqpoll 1} eqpoll X";
by (resolve_tac [subsets_eqpoll_1_eq RS ssubst] 1);
by (resolve_tac [eqpoll_RepFun_sing RS eqpoll_sym] 1);
qed "subsets_eqpoll_1_eqpoll";
-Goal "[| InfCard(x); y:Pow(x); y eqpoll succ(z) |] \
-\ ==> (LEAST i. i:y) : y";
+Goal "[| InfCard(x); y \\<in> Pow(x); y eqpoll succ(z) |] \
+\ ==> (LEAST i. i \\<in> y) \\<in> y";
by (eresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS
succ_lepoll_imp_not_empty RS not_emptyE] 1);
by (fast_tac (claset() addIs [LeastI]
@@ -67,11 +67,11 @@
addEs [Ord_in_Ord]) 1);
qed "InfCard_Least_in";
-Goalw [lepoll_def] "[| InfCard(x); n:nat |] ==> \
-\ {y:Pow(x). y eqpoll succ(succ(n))} lepoll \
-\ x*{y:Pow(x). y eqpoll succ(n)}";
-by (res_inst_tac [("x","lam y:{y:Pow(x). y eqpoll succ(succ(n))}. \
-\ <LEAST i. i:y, y-{LEAST i. i:y}>")] exI 1);
+Goalw [lepoll_def] "[| InfCard(x); n \\<in> nat |] ==> \
+\ {y \\<in> Pow(x). y eqpoll succ(succ(n))} lepoll \
+\ x*{y \\<in> Pow(x). y eqpoll succ(n)}";
+by (res_inst_tac [("x","\\<lambda>y \\<in> {y \\<in> Pow(x). y eqpoll succ(succ(n))}. \
+\ <LEAST i. i \\<in> y, y-{LEAST i. i \\<in> y}>")] exI 1);
by (res_inst_tac [("d","%z. cons(fst(z),snd(z))")] lam_injective 1);
by (rtac SigmaI 1);
by (etac CollectE 1);
@@ -88,9 +88,9 @@
addIs [InfCard_Least_in]) 1));
qed "subsets_lepoll_lemma1";
-val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
+val prems = goal thy "(!!y. y \\<in> z ==> Ord(y)) ==> z \\<subseteq> succ(Union(z))";
by (rtac subsetI 1);
-by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
+by (res_inst_tac [("Q","\\<forall>y \\<in> z. y \\<subseteq> x")] (excluded_middle RS disjE) 1);
by (Fast_tac 2);
by (etac swap 1);
by (rtac ballI 1);
@@ -101,11 +101,11 @@
by (fast_tac (claset() addSEs [leE,ltE]) 1);
qed "set_of_Ord_succ_Union";
-Goal "j<=i ==> i ~: j";
+Goal "j \\<subseteq> i ==> i \\<notin> j";
by (fast_tac (claset() addSEs [mem_irrefl]) 1);
qed "subset_not_mem";
-val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> succ(Union(z)) ~: z";
+val prems = goal thy "(!!y. y \\<in> z ==> Ord(y)) ==> succ(Union(z)) \\<notin> z";
by (resolve_tac [set_of_Ord_succ_Union RS subset_not_mem] 1);
by (eresolve_tac prems 1);
qed "succ_Union_not_mem";
@@ -118,12 +118,12 @@
by (fast_tac (claset() addSDs [le_imp_subset] addEs [Ord_linear_le]) 1);
qed "Un_Ord_disj";
-Goal "x:X ==> Union(X) = x Un Union(X-{x})";
+Goal "x \\<in> X ==> Union(X) = x Un Union(X-{x})";
by (Fast_tac 1);
qed "Union_eq_Un";
-Goal "n:nat ==> \
-\ ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z";
+Goal "n \\<in> nat ==> \
+\ \\<forall>z. (\\<forall>y \\<in> z. Ord(y)) & z eqpoll n & z\\<noteq>0 --> Union(z) \\<in> z";
by (induct_tac "n" 1);
by (fast_tac (claset() addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
@@ -146,14 +146,14 @@
by (rtac subst_elem 1 THEN (TRYALL assume_tac));
qed "Union_in_lemma";
-Goal "[| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |] \
-\ ==> Union(z) : z";
+Goal "[| \\<forall>x \\<in> z. Ord(x); z eqpoll n; z\\<noteq>0; n \\<in> nat |] \
+\ ==> Union(z) \\<in> z";
by (dtac Union_in_lemma 1);
by (fast_tac FOL_cs 1);
qed "Union_in";
-Goal "[| InfCard(x); z:Pow(x); z eqpoll n; n:nat |] \
-\ ==> succ(Union(z)) : x";
+Goal "[| InfCard(x); z \\<in> Pow(x); z eqpoll n; n \\<in> nat |] \
+\ ==> succ(Union(z)) \\<in> x";
by (resolve_tac [Limit_has_succ RS ltE] 1 THEN (assume_tac 3));
by (etac InfCard_is_Limit 1);
by (excluded_middle_tac "z=0" 1);
@@ -167,10 +167,10 @@
(2, InfCard_is_Card RS Card_is_Ord RS Ord_in_Ord)]) 1);
qed "succ_Union_in_x";
-Goalw [lepoll_def] "[| InfCard(x); n:nat |] ==> \
-\ {y:Pow(x). y eqpoll succ(n)} lepoll \
-\ {y:Pow(x). y eqpoll succ(succ(n))}";
-by (res_inst_tac [("x","lam z:{y:Pow(x). y eqpoll succ(n)}. \
+Goalw [lepoll_def] "[| InfCard(x); n \\<in> nat |] ==> \
+\ {y \\<in> Pow(x). y eqpoll succ(n)} lepoll \
+\ {y \\<in> Pow(x). y eqpoll succ(succ(n))}";
+by (res_inst_tac [("x","\\<lambda>z \\<in> {y \\<in> Pow(x). y eqpoll succ(n)}. \
\ cons(succ(Union(z)), z)")] exI 1);
by (res_inst_tac [("d","%z. z-{Union(z)}")] lam_injective 1);
by (resolve_tac [Union_cons_eq_succ_Union RS ssubst] 2);
@@ -185,8 +185,8 @@
by (fast_tac (claset() addSIs [succ_Union_in_x]) 1);
qed "succ_lepoll_succ_succ";
-Goal "[| InfCard(X); n:nat |] \
-\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+Goal "[| InfCard(X); n \\<in> nat |] \
+\ ==> {Y \\<in> Pow(X). Y eqpoll succ(n)} eqpoll X";
by (induct_tac "n" 1);
by (rtac subsets_eqpoll_1_eqpoll 1);
by (rtac eqpollI 1);
@@ -202,21 +202,21 @@
addSIs [succ_lepoll_succ_succ]) 1);
qed "subsets_eqpoll_X";
-Goalw [surj_def] "[| f:surj(A,B); y<=B |] \
+Goalw [surj_def] "[| f \\<in> surj(A,B); y \\<subseteq> B |] \
\ ==> f``(converse(f)``y) = y";
by (fast_tac (claset() addDs [apply_equality2]
addEs [apply_iff RS iffD2]) 1);
qed "image_vimage_eq";
-Goal "[| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
+Goal "[| f \\<in> inj(A,B); y \\<subseteq> A |] ==> converse(f)``(f``y) = y";
by (fast_tac (claset() addSEs [inj_is_fun RS apply_Pair]
addDs [inj_equality]) 1);
qed "vimage_image_eq";
Goalw [eqpoll_def] "A eqpoll B \
-\ ==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}";
+\ ==> {Y \\<in> Pow(A). Y eqpoll n} eqpoll {Y \\<in> Pow(B). Y eqpoll n}";
by (etac exE 1);
-by (res_inst_tac [("x","lam X:{Y:Pow(A). EX f. f : bij(Y, n)}. f``X")] exI 1);
+by (res_inst_tac [("x","\\<lambda>X \\<in> {Y \\<in> Pow(A). \\<exists>f. f \\<in> bij(Y, n)}. f``X")] exI 1);
by (res_inst_tac [("d","%Z. converse(f)``Z")] lam_bijective 1);
by (fast_tac (claset()
addSIs [bij_is_inj RS restrict_bij RS bij_converse_bij RS comp_bij]
@@ -229,7 +229,7 @@
by (fast_tac (claset() addSEs [bij_is_surj RS image_vimage_eq]) 1);
qed "subsets_eqpoll";
-Goalw [WO2_def] "WO2 ==> EX a. Card(a) & X eqpoll a";
+Goalw [WO2_def] "WO2 ==> \\<exists>a. Card(a) & X eqpoll a";
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
by (fast_tac (claset() addSEs [well_ord_Memrel RS well_ord_cardinal_eqpoll RS
(eqpoll_sym RSN (2, eqpoll_trans)) RS eqpoll_sym]
@@ -244,8 +244,8 @@
by (fast_tac (claset() addSEs [Card_is_Ord RS nat_le_infinite_Ord]) 1);
qed "infinite_Card_is_InfCard";
-Goal "[| WO2; n:nat; ~Finite(X) |] \
-\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+Goal "[| WO2; n \\<in> nat; ~Finite(X) |] \
+\ ==> {Y \\<in> Pow(X). Y eqpoll succ(n)} eqpoll X";
by (dtac WO2_imp_ex_Card 1);
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
@@ -256,13 +256,13 @@
by (etac eqpoll_sym 1);
qed "WO2_infinite_subsets_eqpoll_X";
-Goal "well_ord(X,R) ==> EX a. Card(a) & X eqpoll a";
+Goal "well_ord(X,R) ==> \\<exists>a. Card(a) & X eqpoll a";
by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll RS eqpoll_sym]
addSIs [Card_cardinal]) 1);
qed "well_ord_imp_ex_Card";
-Goal "[| well_ord(X,R); n:nat; ~Finite(X) |] \
-\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X";
+Goal "[| well_ord(X,R); n \\<in> nat; ~Finite(X) |] \
+\ ==> {Y \\<in> Pow(X). Y eqpoll succ(n)} eqpoll X";
by (dtac well_ord_imp_ex_Card 1);
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1));
--- a/src/ZF/AC/AC17_AC1.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC17_AC1.ML Mon May 21 14:45:52 2001 +0200
@@ -5,16 +5,14 @@
The proof of AC1 ==> AC17
*)
-open AC17_AC1;
-
(* *********************************************************************** *)
(* more properties of HH *)
(* *********************************************************************** *)
-Goal "[| 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)";
+Goal "[| x - (\\<Union>j \\<in> LEAST i. HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X}, x, i) = {x}. \
+\ HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X}, x, j)) = 0; \
+\ f \\<in> Pow(x)-{0} -> x |] \
+\ ==> \\<exists>r. well_ord(x,r)";
by (rtac 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);
@@ -26,7 +24,7 @@
(* *********************************************************************** *)
Goalw AC_defs "~AC1 ==> \
-\ EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u";
+\ \\<exists>A. \\<forall>f \\<in> Pow(A)-{0} -> A. \\<exists>u \\<in> Pow(A)-{0}. f`u \\<notin> u";
by (etac swap 1);
by (rtac allI 1);
by (etac swap 1);
@@ -37,10 +35,10 @@
by (fast_tac (claset() addSIs [restrict_type]) 1);
qed "not_AC1_imp_ex";
-Goal "[| 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 |] \
+Goal "[| \\<forall>f \\<in> Pow(x) - {0} -> x. \\<exists>u \\<in> Pow(x) - {0}. f`u\\<notin>u; \
+\ \\<exists>f \\<in> Pow(x)-{0}->x. \
+\ x - (\\<Union>a \\<in> (LEAST i. HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X},x,i)={x}). \
+\ HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X},x,a)) = 0 |] \
\ ==> P";
by (etac bexE 1);
by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1));
@@ -53,19 +51,19 @@
by (Fast_tac 1);
val lemma1 = result();
-Goal "~ (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}";
+Goal "~ (\\<exists>f \\<in> Pow(x)-{0}->x. x - F(f) = 0) \
+\ ==> (\\<lambda>f \\<in> Pow(x)-{0}->x. x - F(f)) \
+\ \\<in> (Pow(x) -{0} -> x) -> Pow(x) - {0}";
by (fast_tac (claset() addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1);
val lemma2 = result();
-Goal "[| f`Z : Z; Z:Pow(x)-{0} |] ==> \
-\ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}";
+Goal "[| f`Z \\<in> Z; Z \\<in> Pow(x)-{0} |] ==> \
+\ (\\<lambda>X \\<in> Pow(x)-{0}. {f`X})`Z \\<in> Pow(Z)-{0}";
by Auto_tac;
val lemma3 = result();
-Goal "EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \
-\ ==> EX f:F. f`Q(f) : Q(f)";
+Goal "\\<exists>f \\<in> F. f`((\\<lambda>f \\<in> F. Q(f))`f) \\<in> (\\<lambda>f \\<in> F. Q(f))`f \
+\ ==> \\<exists>f \\<in> F. f`Q(f) \\<in> Q(f)";
by (Asm_full_simp_tac 1);
val lemma4 = result();
@@ -73,9 +71,9 @@
by (rtac classical 1);
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);
+ "\\<exists>f \\<in> Pow(x)-{0}->x. \
+\ x - (\\<Union>a \\<in> (LEAST i. HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X},x,i)={x}). \
+\ HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X},x,a)) = 0" 1);
by (etac lemma1 2 THEN (assume_tac 2));
by (dtac lemma2 1);
by (etac allE 1);
--- 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";
--- a/src/ZF/AC/AC18_AC19.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC18_AC19.thy Mon May 21 14:45:52 2001 +0200
@@ -13,6 +13,6 @@
defs
- u_def "u_(a) == {c Un {0}. c:a}"
+ u_def "u_(a) == {c Un {0}. c \\<in> a}"
end
--- a/src/ZF/AC/AC1_AC17.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC1_AC17.ML Mon May 21 14:45:52 2001 +0200
@@ -5,7 +5,7 @@
The proof of AC1 ==> AC17
*)
-Goal "f : (PROD X:Pow(A) - {0}. X) ==> f : (Pow(A) - {0} -> A)";
+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);
--- a/src/ZF/AC/AC1_WO2.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC1_WO2.ML Mon May 21 14:45:52 2001 +0200
@@ -6,8 +6,8 @@
*)
(*Establishing the existence of a bijection -- hence the need for uresult*)
-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})";
+val [prem] = goal thy "f \\<in> (\\<Pi>X \\<in> Pow(x) - {0}. X) ==> \
+\ ?g(f) \\<in> bij(x, LEAST i. HH(\\<lambda>X \\<in> Pow(x)-{0}. {f`X}, x, i) = {x})";
by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
by (rtac f_subsets_imp_UN_HH_eq_x 1);
by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
--- a/src/ZF/AC/AC2_AC6.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC2_AC6.ML Mon May 21 14:45:52 2001 +0200
@@ -14,12 +14,12 @@
(* AC1 ==> AC2 *)
(* ********************************************************************** *)
-Goal "[| f:(PROD X:A. X); B:A; 0~:A |] ==> {f`B} <= B Int {f`C. C:A}";
+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:A; C:A; D:B; D:C |] ==> f`B = f`C";
+ "[| 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();
@@ -37,11 +37,11 @@
(* AC2 ==> AC1 *)
(* ********************************************************************** *)
-Goal "0~:A ==> 0 ~: {B*{B}. B:A}";
+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:A |] \
+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]
@@ -49,9 +49,8 @@
by (blast_tac (claset() addSEs [equalityE]) 1);
val lemma2 = result();
-Goal "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) ";
+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();
@@ -68,7 +67,7 @@
(* AC1 ==> AC4 *)
(* ********************************************************************** *)
-Goal "0 ~: {R``{x}. x:domain(R)}";
+Goal "0 \\<notin> {R``{x}. x \\<in> domain(R)}";
by (Blast_tac 1);
val lemma = result();
@@ -83,15 +82,15 @@
(* AC4 ==> AC3 *)
(* ********************************************************************** *)
-Goal "f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)";
+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(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
+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:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
+Goal "x \\<in> A ==> (\\<Union>z \\<in> A. {z}*f(z))``{x} = f(x)";
by (Fast_tac 1);
val lemma3 = result();
@@ -107,7 +106,7 @@
(* AC3 ==> AC1 *)
(* ********************************************************************** *)
-Goal "b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
+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);
@@ -142,23 +141,23 @@
(* AC5 ==> AC4, Rubin & Rubin, p. 11 *)
(* ********************************************************************** *)
-Goal "R <= A*B ==> (lam x:R. fst(x)) : R -> A";
+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 <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
+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 "[| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)";
+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 <= 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})";
+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();
--- a/src/ZF/AC/AC7_AC9.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC7_AC9.ML Mon May 21 14:45:52 2001 +0200
@@ -12,15 +12,15 @@
(* - Sigma_fun_space_eqpoll *)
(* ********************************************************************** *)
-Goal "[| 0~:A; B:A |] ==> (nat->Union(A)) * B ~= 0";
+Goal "[| 0\\<notin>A; B \\<in> A |] ==> (nat->Union(A)) * B \\<noteq> 0";
by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1,
Union_empty_iff RS iffD1]) 1);
qed "Sigma_fun_space_not0";
Goalw [inj_def]
- "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)) ) ";
+ "C \\<in> A ==> (\\<lambda>g \\<in> (nat->Union(A))*C. \
+\ (\\<lambda>n \\<in> nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \
+\ \\<in> inj((nat->Union(A))*C, (nat->Union(A)) ) ";
by (rtac CollectI 1);
by (fast_tac (claset() addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
fst_type,diff_type,nat_succI,nat_0I]) 1);
@@ -37,7 +37,7 @@
by (asm_full_simp_tac (simpset() addsimps [succ_not_0 RS if_not_P]) 1);
val lemma = result();
-Goal "[| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
+Goal "[| C \\<in> A; 0\\<notin>A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
by (rtac eqpollI 1);
by (fast_tac (claset() addSEs [prod_lepoll_self, not_sym RS not_emptyE,
subst_elem] addEs [swap]) 2);
@@ -60,19 +60,19 @@
(* the proof. *)
(* ********************************************************************** *)
-Goal "y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)";
+Goal "y \\<in> (\\<Pi>B \\<in> A. Y*B) ==> (\\<lambda>B \\<in> A. snd(y`B)): (\\<Pi>B \\<in> A. B)";
by (fast_tac (claset() addSIs [lam_type, snd_type, apply_type]) 1);
val lemma1_1 = result();
-Goal "y: (PROD B:{Y*C. C:A}. B) ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
+Goal "y \\<in> (\\<Pi>B \\<in> {Y*C. C \\<in> A}. B) ==> (\\<lambda>B \\<in> A. y`(Y*B)): (\\<Pi>B \\<in> A. Y*B)";
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1);
val lemma1_2 = result();
-Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 ==> (PROD B:A. B) ~= 0";
+Goal "(\\<Pi>B \\<in> {(nat->Union(A))*C. C \\<in> A}. B) \\<noteq> 0 ==> (\\<Pi>B \\<in> A. B) \\<noteq> 0";
by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1);
val lemma1 = result();
-Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
+Goal "0 \\<notin> A ==> 0 \\<notin> {(nat -> Union(A)) * C. C \\<in> A}";
by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1);
val lemma2 = result();
@@ -94,12 +94,12 @@
(* ********************************************************************** *)
Goalw [eqpoll_def]
- "ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \
-\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
+ "\\<forall>B \\<in> A. \\<exists>B1 B2. B=<B1,B2> & B1 eqpoll B2 \
+\ ==> 0 \\<notin> { bij(fst(B),snd(B)). B \\<in> A }";
by Auto_tac;
val lemma1 = result();
-Goal "[| f: (PROD X:RepFun(A,p). X); D:A |] ==> (lam x:A. f`p(x))`D : p(D)";
+Goal "[| f \\<in> (\\<Pi>X \\<in> RepFun(A,p). X); D \\<in> A |] ==> (\\<lambda>x \\<in> A. f`p(x))`D \\<in> p(D)";
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
by (fast_tac (claset() addSEs [apply_type]) 1);
val lemma2 = result();
@@ -117,12 +117,12 @@
(* AC8 ==> AC1 and AC1 ==> AC9 *)
(* ********************************************************************** *)
-Goal "ALL B1:A. ALL B2:A. B1 eqpoll B2 ==> \
-\ ALL B:A*A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2";
+Goal "\\<forall>B1 \\<in> A. \\<forall>B2 \\<in> A. B1 eqpoll B2 \
+\ ==> \\<forall>B \\<in> A*A. \\<exists>B1 B2. B=<B1,B2> & B1 eqpoll B2";
by (Fast_tac 1);
val lemma1 = result();
-Goal "f:bij(fst(<a,b>),snd(<a,b>)) ==> f:bij(a,b)";
+Goal "f \\<in> bij(fst(<a,b>),snd(<a,b>)) ==> f \\<in> bij(a,b)";
by (Asm_full_simp_tac 1);
val lemma2 = result();
@@ -155,9 +155,9 @@
qed "nat_lepoll_lemma";
-Goal "[| 0~:A; A~=0; \
-\ C = {((nat->Union(A))*B)*nat. B:A} Un \
-\ {cons(0,((nat->Union(A))*B)*nat). B:A}; \
+Goal "[| 0\\<notin>A; A\\<noteq>0; \
+\ C = {((nat->Union(A))*B)*nat. B \\<in> A} Un \
+\ {cons(0,((nat->Union(A))*B)*nat). B \\<in> A}; \
\ B1: C; B2: C |] \
\ ==> B1 eqpoll B2";
by (blast_tac
@@ -166,11 +166,10 @@
addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1);
val lemma1 = result();
-Goal "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)";
+Goal "\\<forall>B1 \\<in> {(F*B)*N. B \\<in> A} Un {cons(0,(F*B)*N). B \\<in> A}. \
+\ \\<forall>B2 \\<in> {(F*B)*N. B \\<in> A} Un {cons(0,(F*B)*N). B \\<in> A}. \
+\ f`<B1,B2> \\<in> bij(B1, B2) \
+\ ==> (\\<lambda>B \\<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \\<in> (\\<Pi>X \\<in> A. X)";
by (rtac lam_type 1);
by (rtac snd_type 1);
by (rtac fst_type 1);
--- a/src/ZF/AC/AC_Equiv.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC_Equiv.ML Mon May 21 14:45:52 2001 +0200
@@ -20,14 +20,14 @@
(* used only in WO1_DC.ML *)
(*Note simpler proof*)
-Goal "[| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; A<=Df; A<=Dg |] ==> f``A=g``A";
+Goal "[| \\<forall>x \\<in> A. f`x=g`x; f \\<in> Df->Cf; g \\<in> Dg->Cg; A \\<subseteq> Df; A \\<subseteq> Dg |] ==> f``A=g``A";
by (asm_simp_tac (simpset() addsimps [image_fun]) 1);
qed "images_eq";
-(* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
+(* used in \\<in> AC10-AC15.ML AC16WO4.ML WO6WO1.ML *)
(*I don't know where to put this one.*)
goal Cardinal.thy
- "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m";
+ "!!m A B. [| A lepoll succ(m); B \\<subseteq> A; B\\<noteq>0 |] ==> A-B lepoll m";
by (rtac not_emptyE 1 THEN (assume_tac 1));
by (ftac singleton_subsetI 1);
by (ftac subsetD 1 THEN (assume_tac 1));
@@ -74,14 +74,14 @@
by (fast_tac (claset() addSEs [singleton_eq_iff RS iffD1 RS sym]) 1);
qed "the_element";
-Goal "(lam x:A. {x}) : bij(A, {{x}. x:A})";
+Goal "(\\<lambda>x \\<in> A. {x}) \\<in> bij(A, {{x}. x \\<in> 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 (simpset() addsimps [the_element]) 1));
qed "lam_sing_bij";
val [major, minor] = Goalw [inj_def]
- "[| f:inj(A, B); !!a. a:A ==> f`a : C |] ==> f:inj(A,C)";
+ "[| f \\<in> inj(A, B); !!a. a \\<in> A ==> f`a \\<in> C |] ==> f \\<in> inj(A,C)";
by (fast_tac (claset() addSEs [minor]
addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1);
qed "inj_strengthen_type";
@@ -94,10 +94,10 @@
val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll;
(* ********************************************************************** *)
-(* Another elimination rule for EX! *)
+(* Another elimination rule for \\<exists>! *)
(* ********************************************************************** *)
-Goal "[| EX! x. P(x); P(x); P(y) |] ==> x=y";
+Goal "[| \\<exists>! x. P(x); P(x); P(y) |] ==> x=y";
by (etac ex1E 1);
by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1);
by (Fast_tac 1);
@@ -108,7 +108,7 @@
(* image of a surjection *)
(* ********************************************************************** *)
-Goalw [surj_def] "f : surj(A, B) ==> f``A = B";
+Goalw [surj_def] "f \\<in> surj(A, B) ==> f``A = B";
by (etac CollectE 1);
by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1
THEN (assume_tac 1));
@@ -116,11 +116,11 @@
qed "surj_image_eq";
-Goal "succ(x) lepoll y ==> y ~= 0";
+Goal "succ(x) lepoll y ==> y \\<noteq> 0";
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
qed "succ_lepoll_imp_not_empty";
-Goal "x eqpoll succ(n) ==> x ~= 0";
+Goal "x eqpoll succ(n) ==> x \\<noteq> 0";
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1);
qed "eqpoll_succ_imp_not_empty";
--- a/src/ZF/AC/AC_Equiv.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Mon May 21 14:45:52 2001 +0200
@@ -38,91 +38,90 @@
(* Well Ordering Theorems *)
- WO1_def "WO1 == ALL A. EX R. well_ord(A,R)"
+ WO1_def "WO1 == \\<forall>A. \\<exists>R. well_ord(A,R)"
- WO2_def "WO2 == ALL A. EX a. Ord(a) & A eqpoll a"
+ WO2_def "WO2 == \\<forall>A. \\<exists>a. Ord(a) & A eqpoll a"
- WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
+ WO3_def "WO3 == \\<forall>A. \\<exists>a. Ord(a) & (\\<exists>b. b \\<subseteq> a & A eqpoll b)"
- WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &
- (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+ WO4_def "WO4(m) == \\<forall>A. \\<exists>a f. Ord(a) & domain(f)=a &
+ (\\<Union>b<a. f`b) = A & (\\<forall>b<a. f`b lepoll m)"
- WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
+ WO5_def "WO5 == \\<exists>m \\<in> nat. 1 le m & WO4(m)"
- WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a
- & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+ WO6_def "WO6 == \\<forall>A. \\<exists>m \\<in> nat. 1 le m & (\\<exists>a f. Ord(a) & domain(f)=a
+ & (\\<Union>b<a. f`b) = A & (\\<forall>b<a. f`b lepoll m))"
- WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->
+ WO7_def "WO7 == \\<forall>A. Finite(A) <-> (\\<forall>R. well_ord(A,R) -->
well_ord(A,converse(R)))"
- WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->
- (EX R. well_ord(A,R))"
+ WO8_def "WO8 == \\<forall>A. (\\<exists>f. f \\<in> (\\<Pi>X \\<in> A. X)) --> (\\<exists>R. well_ord(A,R))"
(* Axioms of Choice *)
- AC0_def "AC0 == ALL A. EX f. f:(PROD X:Pow(A)-{0}. X)"
+ AC0_def "AC0 == \\<forall>A. \\<exists>f. f \\<in> (\\<Pi>X \\<in> Pow(A)-{0}. X)"
- AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
+ AC1_def "AC1 == \\<forall>A. 0\\<notin>A --> (\\<exists>f. f \\<in> (\\<Pi>X \\<in> A. X))"
- AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)
- --> (EX C. ALL B:A. EX y. B Int C = {y})"
+ AC2_def "AC2 == \\<forall>A. 0\\<notin>A & pairwise_disjoint(A)
+ --> (\\<exists>C. \\<forall>B \\<in> A. \\<exists>y. B Int C = {y})"
- AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
+ AC3_def "AC3 == \\<forall>A B. \\<forall>f \\<in> A->B. \\<exists>g. g \\<in> (\\<Pi>x \\<in> {a \\<in> A. f`a\\<noteq>0}. f`x)"
- AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
+ AC4_def "AC4 == \\<forall>R A B. (R \\<subseteq> A*B --> (\\<exists>f. f \\<in> (\\<Pi>x \\<in> domain(R). R``{x})))"
- AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.
- ALL x:domain(g). f`(g`x) = x"
+ AC5_def "AC5 == \\<forall>A B. \\<forall>f \\<in> A->B. \\<exists>g \\<in> range(f)->A.
+ \\<forall>x \\<in> domain(g). f`(g`x) = x"
- AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
+ AC6_def "AC6 == \\<forall>A. 0\\<notin>A --> (\\<Pi>B \\<in> A. B)\\<noteq>0"
- AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)
- --> (PROD B:A. B)~=0"
+ AC7_def "AC7 == \\<forall>A. 0\\<notin>A & (\\<forall>B1 \\<in> A. \\<forall>B2 \\<in> A. B1 eqpoll B2)
+ --> (\\<Pi>B \\<in> A. B)\\<noteq>0"
- AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)
- --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+ AC8_def "AC8 == \\<forall>A. (\\<forall>B \\<in> A. \\<exists>B1 B2. B=<B1,B2> & B1 eqpoll B2)
+ --> (\\<exists>f. \\<forall>B \\<in> A. f`B \\<in> bij(fst(B),snd(B)))"
- AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->
- (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+ AC9_def "AC9 == \\<forall>A. (\\<forall>B1 \\<in> A. \\<forall>B2 \\<in> A. B1 eqpoll B2) -->
+ (\\<exists>f. \\<forall>B1 \\<in> A. \\<forall>B2 \\<in> A. f`<B1,B2> \\<in> bij(B1,B2))"
- AC10_def "AC10(n) == ALL A. (ALL B:A. ~Finite(B)) -->
- (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ AC10_def "AC10(n) == \\<forall>A. (\\<forall>B \\<in> A. ~Finite(B)) -->
+ (\\<exists>f. \\<forall>B \\<in> A. (pairwise_disjoint(f`B) &
sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
- AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
+ AC11_def "AC11 == \\<exists>n \\<in> nat. 1 le n & AC10(n)"
- AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->
- (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &
+ AC12_def "AC12 == \\<forall>A. (\\<forall>B \\<in> A. ~Finite(B)) -->
+ (\\<exists>n \\<in> nat. 1 le n & (\\<exists>f. \\<forall>B \\<in> A. (pairwise_disjoint(f`B) &
sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
- AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &
- f`B <= B & f`B lepoll m)"
+ AC13_def "AC13(m) == \\<forall>A. 0\\<notin>A --> (\\<exists>f. \\<forall>B \\<in> A. f`B\\<noteq>0 &
+ f`B \\<subseteq> B & f`B lepoll m)"
- AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
+ AC14_def "AC14 == \\<exists>m \\<in> nat. 1 le m & AC13(m)"
- AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.
- f`B~=0 & f`B <= B & f`B lepoll m))"
+ AC15_def "AC15 == \\<forall>A. 0\\<notin>A --> (\\<exists>m \\<in> nat. 1 le m & (\\<exists>f. \\<forall>B \\<in> A.
+ f`B\\<noteq>0 & f`B \\<subseteq> B & f`B lepoll m))"
- AC16_def "AC16(n, k) == ALL A. ~Finite(A) -->
- (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &
- (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+ AC16_def "AC16(n, k) == \\<forall>A. ~Finite(A) -->
+ (\\<exists>T. T \\<subseteq> {X \\<in> Pow(A). X eqpoll succ(n)} &
+ (\\<forall>X \\<in> {X \\<in> Pow(A). X eqpoll succ(k)}. \\<exists>! Y. Y \\<in> T & X \\<subseteq> Y))"
- 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"
+ AC17_def "AC17 == \\<forall>A. \\<forall>g \\<in> (Pow(A)-{0} -> A) -> Pow(A)-{0}.
+ \\<exists>f \\<in> Pow(A)-{0} -> A. f`(g`f) \\<in> g`f"
- 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))))"
+ AC18_def "AC18 == (!!X A B. A\\<noteq>0 & (\\<forall>a \\<in> A. B(a) \\<noteq> 0) -->
+ ((\\<Inter>a \\<in> A. \\<Union>b \\<in> B(a). X(a,b)) =
+ (\\<Union>f \\<in> \\<Pi>a \\<in> A. B(a). \\<Inter>a \\<in> A. X(a, f`a))))"
- AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =
- (UN f:(PROD B:A. B). INT a:A. f`a))"
+ AC19_def "AC19 == \\<forall>A. A\\<noteq>0 & 0\\<notin>A --> ((\\<Inter>a \\<in> A. \\<Union>b \\<in> a. b) =
+ (\\<Union>f \\<in> (\\<Pi>B \\<in> A. B). \\<Inter>a \\<in> A. f`a))"
(* 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"
+ == \\<forall>A1 \\<in> A. \\<forall>A2 \\<in> A. A1 Int A2 \\<noteq> 0 --> A1=A2"
sets_of_size_between_def "sets_of_size_between(A,m,n)
- == ALL B:A. m lepoll B & B lepoll n"
+ == \\<forall>B \\<in> A. m lepoll B & B lepoll n"
end
--- a/src/ZF/AC/Cardinal_aux.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML Mon May 21 14:45:52 2001 +0200
@@ -11,7 +11,7 @@
(* ********************************************************************** *)
(* j=|A| *)
-Goal "[| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j";
+Goal "[| A lepoll i; Ord(i) |] ==> \\<exists>j. j le i & A eqpoll j";
by (blast_tac (claset() addSIs [lepoll_cardinal_le, well_ord_Memrel,
well_ord_cardinal_eqpoll RS eqpoll_sym]
addDs [lepoll_well_ord]) 1);
@@ -19,7 +19,7 @@
(* j=|A| *)
Goalw [lesspoll_def]
- "[| A lesspoll i; Ord(i) |] ==> EX j. j<i & A eqpoll j";
+ "[| A lesspoll i; Ord(i) |] ==> \\<exists>j. j<i & A eqpoll j";
by (blast_tac (claset() addSDs [lepoll_imp_ex_le_eqpoll] addSEs [leE]) 1);
qed "lesspoll_imp_ex_lt_eqpoll";
@@ -54,17 +54,17 @@
qed "Un_eqpoll_Inf_Ord";
-Goal "?f : bij({{y,z}. y:x}, x)";
+Goal "?f \\<in> bij({{y,z}. y \\<in> x}, x)";
by (rtac RepFun_bijective 1);
by (simp_tac (simpset() addsimps [doubleton_eq_iff]) 1);
by (Blast_tac 1);
qed "paired_bij";
-Goalw [eqpoll_def] "{{y,z}. y:x} eqpoll x";
+Goalw [eqpoll_def] "{{y,z}. y \\<in> x} eqpoll x";
by (fast_tac (claset() addSIs [paired_bij]) 1);
qed "paired_eqpoll";
-Goal "EX B. B eqpoll A & B Int C = 0";
+Goal "\\<exists>B. B eqpoll A & B Int C = 0";
by (fast_tac (claset() addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1);
qed "ex_eqpoll_disjoint";
@@ -80,7 +80,7 @@
THEN (REPEAT (assume_tac 1)));
qed "Un_lepoll_Inf_Ord";
-Goal "[| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j";
+Goal "[| P(i); i \\<in> j; Ord(j) |] ==> (LEAST i. P(i)) \\<in> j";
by (eresolve_tac [Least_le RS leE] 1);
by (etac Ord_in_Ord 1 THEN (assume_tac 1));
by (etac ltE 1);
@@ -88,7 +88,7 @@
by (etac subst_elem 1 THEN (assume_tac 1));
qed "Least_in_Ord";
-Goal "[| well_ord(x,r); y<=x; y lepoll succ(n); n:nat |] \
+Goal "[| well_ord(x,r); y \\<subseteq> x; y lepoll succ(n); n \\<in> nat |] \
\ ==> y-{THE b. first(b,y,r)} lepoll n";
by (res_inst_tac [("Q","y=0")] (excluded_middle RS disjE) 1);
by (fast_tac (claset() addSIs [Diff_sing_lepoll, the_first_in]) 1);
@@ -97,30 +97,30 @@
by (Fast_tac 1);
qed "Diff_first_lepoll";
-Goal "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
+Goal "(\\<Union>x \\<in> X. P(x)) \\<subseteq> (\\<Union>x \\<in> X. P(x)-Q(x)) Un (\\<Union>x \\<in> X. Q(x))";
by (Fast_tac 1);
qed "UN_subset_split";
-Goalw [lepoll_def] "Ord(a) ==> (UN x:a. {P(x)}) lepoll a";
-by (res_inst_tac [("x","lam z:(UN x:a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
+Goalw [lepoll_def] "Ord(a) ==> (\\<Union>x \\<in> a. {P(x)}) lepoll a";
+by (res_inst_tac [("x","\\<lambda>z \\<in> (\\<Union>x \\<in> a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
by (res_inst_tac [("d","%z. P(z)")] lam_injective 1);
by (fast_tac (claset() addSIs [Least_in_Ord]) 1);
by (fast_tac (claset() addIs [LeastI] addSEs [Ord_in_Ord]) 1);
qed "UN_sing_lepoll";
-Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==> \
-\ ALL f. (ALL b:a. f`b lepoll n & f`b <= T) --> (UN b:a. f`b) lepoll a";
+Goal "[| well_ord(T, R); ~Finite(a); Ord(a); n \\<in> nat |] ==> \
+\ \\<forall>f. (\\<forall>b \\<in> a. f`b lepoll n & f`b \\<subseteq> T) --> (\\<Union>b \\<in> a. f`b) lepoll a";
by (induct_tac "n" 1);
by (rtac allI 1);
by (rtac impI 1);
-by (res_inst_tac [("b","UN b:a. f`b")] subst 1);
+by (res_inst_tac [("b","\\<Union>b \\<in> a. f`b")] subst 1);
by (rtac empty_lepollI 2);
by (resolve_tac [equals0I RS sym] 1);
by (REPEAT (eresolve_tac [UN_E, allE] 1));
by (fast_tac (claset() addDs [lepoll_0_is_0 RS subst]) 1);
by (rtac allI 1);
by (rtac impI 1);
-by (eres_inst_tac [("x","lam x:a. f`x - {THE b. first(b,f`x,R)}")] allE 1);
+by (eres_inst_tac [("x","\\<lambda>x \\<in> a. f`x - {THE b. first(b,f`x,R)}")] allE 1);
by (etac impE 1);
by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSIs [Diff_first_lepoll]) 1);
@@ -130,37 +130,37 @@
by (etac UN_sing_lepoll 1);
qed "UN_fun_lepoll_lemma";
-Goal "[| ALL b:a. f`b lepoll n & f`b <= T; well_ord(T, R); \
-\ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. f`b) lepoll a";
+Goal "[| \\<forall>b \\<in> a. f`b lepoll n & f`b \\<subseteq> T; well_ord(T, R); \
+\ ~Finite(a); Ord(a); n \\<in> nat |] ==> (\\<Union>b \\<in> a. f`b) lepoll a";
by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1)));
by (Fast_tac 1);
qed "UN_fun_lepoll";
-Goal "[| ALL b:a. F(b) lepoll n & F(b) <= T; well_ord(T, R); \
-\ ~Finite(a); Ord(a); n:nat |] ==> (UN b:a. F(b)) lepoll a";
+Goal "[| \\<forall>b \\<in> a. F(b) lepoll n & F(b) \\<subseteq> T; well_ord(T, R); \
+\ ~Finite(a); Ord(a); n \\<in> nat |] ==> (\\<Union>b \\<in> a. F(b)) lepoll a";
by (rtac impE 1 THEN (assume_tac 3));
-by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2
+by (res_inst_tac [("f","\\<lambda>b \\<in> a. F(b)")] (UN_fun_lepoll) 2
THEN (TRYALL assume_tac));
by Auto_tac;
qed "UN_lepoll";
-Goal "Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))";
+Goal "Ord(a) ==> (\\<Union>b \\<in> a. F(b)) = (\\<Union>b \\<in> a. F(b) - (\\<Union>c \\<in> b. F(c)))";
by (rtac equalityI 1);
by (Fast_tac 2);
by (rtac subsetI 1);
by (etac UN_E 1);
by (rtac UN_I 1);
-by (res_inst_tac [("P","%z. x:F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1)));
+by (res_inst_tac [("P","%z. x \\<in> F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1)));
by (rtac DiffI 1);
by (resolve_tac [Ord_in_Ord RSN (2, LeastI)] 1 THEN (REPEAT (assume_tac 1)));
by (rtac notI 1);
by (etac UN_E 1);
-by (eres_inst_tac [("P","%z. x:F(z)"),("i","c")] less_LeastE 1);
+by (eres_inst_tac [("P","%z. x \\<in> F(z)"),("i","c")] less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 1);
qed "UN_eq_UN_Diffs";
Goalw [lepoll_def, eqpoll_def]
- "a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
+ "a lepoll X ==> \\<exists>Y. Y \\<subseteq> X & a eqpoll Y";
by (etac exE 1);
by (forward_tac [subset_refl RSN (2, restrict_bij)] 1);
by (res_inst_tac [("x","f``a")] exI 1);
--- a/src/ZF/AC/DC.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/DC.ML Mon May 21 14:45:52 2001 +0200
@@ -14,18 +14,18 @@
(* *)
(* Define XX and RR as follows: *)
(* *)
-(* XX = (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R}) *)
+(* XX = (\\<Union>n \\<in> nat. {f \\<in> n->X. \\<forall>k \\<in> n. <f``k, f`k> \\<in> R}) *)
(* f RR g iff domain(g)=succ(domain(f)) & *)
(* restrict(g, domain(f)) = f *)
(* *)
(* Then RR satisfies the hypotheses of DC. *)
(* So applying DC: *)
(* *)
-(* EX f:nat->XX. ALL n:nat. f`n RR f`succ(n) *)
+(* \\<exists>f \\<in> nat->XX. \\<forall>n \\<in> nat. f`n RR f`succ(n) *)
(* *)
(* Thence *)
(* *)
-(* ff = {<n, f`succ(n)`n>. n:nat} *)
+(* ff = {<n, f`succ(n)`n>. n \\<in> nat} *)
(* *)
(* is the desired function. *)
(* *)
@@ -37,11 +37,11 @@
val XX_def = thm "XX_def";
val RR_def = thm "RR_def";
-Goalw [RR_def] "RR <= XX*XX";
+Goalw [RR_def] "RR \\<subseteq> XX*XX";
by (Fast_tac 1);
qed "lemma1_1";
-Goalw [RR_def, XX_def] "RR ~= 0";
+Goalw [RR_def, XX_def] "RR \\<noteq> 0";
by (rtac (all_ex RS ballE) 1);
by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2);
by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1);
@@ -57,7 +57,7 @@
simpset() addsimps [singleton_0 RS sym]) 1);
qed "lemma1_2";
-Goalw [RR_def, XX_def] "range(RR) <= domain(RR)";
+Goalw [RR_def, XX_def] "range(RR) \\<subseteq> domain(RR)";
by (rtac range_subset_domain 1);
by (Blast_tac 2);
by (Clarify_tac 1);
@@ -76,9 +76,9 @@
qed "lemma1_3";
-Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR; f: nat -> XX; n:nat |] \
-\ ==> EX k:nat. f`succ(n) : k -> X & n:k \
-\ & <f`succ(n)``n, f`succ(n)`n> : R";
+Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; n \\<in> nat |] \
+\ ==> \\<exists>k \\<in> nat. f`succ(n) \\<in> k -> X & n \\<in> k \
+\ & <f`succ(n)``n, f`succ(n)`n> \\<in> R";
by (induct_tac "n" 1);
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1);
by (dresolve_tac [nat_0I RSN (2, bspec)] 1);
@@ -91,7 +91,7 @@
addss (simpset() addsimps [RR_def])) 1);
(** LEVEL 7, other subgoal **)
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
-by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1);
+by (subgoal_tac "f ` succ(succ(x)) \\<in> succ(k)->X" 1);
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1
THEN (assume_tac 1));
by (full_simp_tac (simpset() addsimps [XX_def,RR_def]) 1);
@@ -107,9 +107,9 @@
by (deepen_tac (claset() addDs [domain_of_fun RS sym RS trans]) 0 1);
qed "lemma2";
-Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR; f: nat -> XX; m:nat |] \
-\ ==> {f`succ(x)`x. x:m} = {f`succ(m)`x. x:m}";
-by (subgoal_tac "ALL x:m. f`succ(m)`x = f`succ(x)`x" 1);
+Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; m \\<in> nat |] \
+\ ==> {f`succ(x)`x. x \\<in> m} = {f`succ(m)`x. x \\<in> m}";
+by (subgoal_tac "\\<forall>x \\<in> m. f`succ(m)`x = f`succ(x)`x" 1);
by (Asm_full_simp_tac 1);
by (induct_tac "m" 1);
by (Fast_tac 1);
@@ -130,8 +130,8 @@
addIs [nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1);
qed "lemma3_1";
-Goal "[| ALL n:nat. <f`n, f`succ(n)> : RR; f: nat -> XX; m:nat |] \
-\ ==> (lam x:nat. f`succ(x)`x) `` m = f`succ(m)``m";
+Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; m \\<in> nat |] \
+\ ==> (\\<lambda>x \\<in> nat. f`succ(x)`x) `` m = f`succ(m)``m";
by (etac natE 1);
by (Asm_simp_tac 1);
by (stac image_lam 1);
@@ -152,7 +152,7 @@
(*these three results comprise Lemma 1*)
by (blast_tac (claset() addSIs (map export [lemma1_1, lemma1_2, lemma1_3])) 1);
by (etac bexE 1);
-by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1);
+by (res_inst_tac [("x","\\<lambda>n \\<in> nat. f`succ(n)`n")] bexI 1);
by (fast_tac (claset() addSIs [lam_type] addSDs [export lemma2]
addSEs [fun_weaken_type, apply_type]) 2);
by (rtac oallI 1);
@@ -177,23 +177,23 @@
Define XX and RR as follows:
- XX = (UN n:nat. {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})
+ XX = (\\<Union>n \\<in> nat. {f \\<in> succ(n)->domain(R). \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R})
RR = {<z1,z2>:Fin(XX)*XX.
- (domain(z2)=succ(UN f:z1. domain(f)) &
- (ALL f:z1. restrict(z2, domain(f)) = f)) |
- (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f)) &
- (ALL f:z1. restrict(g, domain(f)) = f)) &
+ (domain(z2)=succ(\\<Union>f \\<in> z1. domain(f)) &
+ (\\<forall>f \\<in> z1. restrict(z2, domain(f)) = f)) |
+ (~ (\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> z1. domain(f)) &
+ (\\<forall>f \\<in> z1. restrict(g, domain(f)) = f)) &
z2={<0,x>})}
Then XX and RR satisfy the hypotheses of DC(omega).
So applying DC:
- EX f:nat->XX. ALL n:nat. f``n RR f`n
+ \\<exists>f \\<in> nat->XX. \\<forall>n \\<in> nat. f``n RR f`n
Thence
- ff = {<n, f`n`n>. n:nat}
+ ff = {<n, f`n`n>. n \\<in> nat}
is the desired function.
@@ -204,7 +204,7 @@
by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1);
qed "lesspoll_nat_is_Finite";
-Goal "n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)";
+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);
by (fast_tac (claset() addSIs [Fin.emptyI]
@@ -223,7 +223,7 @@
by (asm_full_simp_tac (simpset() addsimps [cons_Diff]) 1);
qed "Finite_Fin_lemma";
-Goalw [Finite_def] "[| Finite(A); A <= X |] ==> A : Fin(X)";
+Goalw [Finite_def] "[| Finite(A); A \\<subseteq> X |] ==> A \\<in> Fin(X)";
by (etac bexE 1);
by (dtac Finite_Fin_lemma 1);
by (etac allE 1);
@@ -233,7 +233,7 @@
qed "Finite_Fin";
Goal
- "x:X ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
+ "x \\<in> X ==> {<0,x>}: (\\<Union>n \\<in> nat. {f \\<in> succ(n)->X. \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R})";
by (rtac (nat_0I RS UN_I) 1);
by (fast_tac (claset() addSIs [singleton_fun RS Pi_type]
addss (simpset() addsimps [singleton_0 RS sym])) 1);
@@ -246,17 +246,17 @@
val RR_def = thm "RR_def";
val allRR_def = thm "allRR_def";
-Goal "[| range(R) <= domain(R); x:domain(R) |] \
-\ ==> RR <= Pow(XX)*XX & \
-\ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
+Goal "[| range(R) \\<subseteq> domain(R); x \\<in> domain(R) |] \
+\ ==> RR \\<subseteq> Pow(XX)*XX & \
+\ (\\<forall>Y \\<in> Pow(XX). Y lesspoll nat --> (\\<exists>x \\<in> XX. <Y,x>:RR))";
by (rtac conjI 1);
by (force_tac (claset() addSDs [FinD RS PowI],
simpset() addsimps [RR_def]) 1);
by (rtac (impI RS ballI) 1);
by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
THEN (assume_tac 1));
-by (excluded_middle_tac "EX g:XX. domain(g)=succ(UN f:Y. domain(f)) \
-\ & (ALL f:Y. restrict(g, domain(f)) = f)" 1);
+by (excluded_middle_tac "\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> Y. domain(f)) \
+\ & (\\<forall>f \\<in> Y. restrict(g, domain(f)) = f)" 1);
by (fast_tac (claset() addss (simpset() addsimps [RR_def])) 2);
by (safe_tac (claset() delrules [domainE]));
by (rewrite_goals_tac [XX_def,RR_def]);
@@ -265,39 +265,39 @@
cons_fun_type2]) 1);
qed "lemma4";
-Goal "[| f:nat->X; n:nat |] ==> \
-\ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))";
+Goal "[| f \\<in> nat->X; n \\<in> nat |] ==> \
+\ (\\<Union>x \\<in> f``succ(n). P(x)) = P(f`n) Un (\\<Union>x \\<in> f``n. P(x))";
by (asm_full_simp_tac (simpset()
addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun),
[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1);
qed "UN_image_succ_eq";
-Goal "[| (UN x:f``n. P(x)) = y; P(f`n) = succ(y); \
-\ f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
+Goal "[| (\\<Union>x \\<in> f``n. P(x)) = y; P(f`n) = succ(y); \
+\ f \\<in> nat -> X; n \\<in> nat |] ==> (\\<Union>x \\<in> f``succ(n). P(x)) = succ(y)";
by (asm_full_simp_tac (simpset() addsimps [UN_image_succ_eq]) 1);
by (Fast_tac 1);
qed "UN_image_succ_eq_succ";
-Goal "[| f:succ(n) -> D; n:nat; \
-\ domain(f)=succ(x); x=y |] ==> f`y : D";
+Goal "[| f \\<in> succ(n) -> D; n \\<in> nat; \
+\ domain(f)=succ(x); x=y |] ==> f`y \\<in> D";
by (fast_tac (claset() addEs [apply_type]
addSDs [[sym, domain_of_fun] MRS trans]) 1);
qed "apply_domain_type";
-Goal "[| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)";
+Goal "[| f \\<in> nat -> X; n \\<in> nat |] ==> f``succ(n) = cons(f`n, f``n)";
by (asm_full_simp_tac (simpset()
addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1);
qed "image_fun_succ";
-Goalw [XX_def] "[| domain(f`n) = succ(u); f : nat -> XX; u=k; n:nat |] \
-\ ==> f`n : succ(k) -> domain(R)";
+Goalw [XX_def] "[| domain(f`n) = succ(u); f \\<in> nat -> XX; u=k; n \\<in> nat |] \
+\ ==> f`n \\<in> succ(k) -> domain(R)";
by (dtac apply_type 1 THEN (assume_tac 1));
by (fast_tac (claset() addEs [domain_eq_imp_fun_type]) 1);
qed "f_n_type";
Goalw [XX_def]
- "[| f : nat -> XX; domain(f`n) = succ(k); n:nat |] \
-\ ==> ALL i:k. <f`n`i, f`n`succ(i)> : R";
+ "[| f \\<in> nat -> XX; domain(f`n) = succ(k); n \\<in> nat |] \
+\ ==> \\<forall>i \\<in> k. <f`n`i, f`n`succ(i)> \\<in> R";
by (dtac apply_type 1 THEN (assume_tac 1));
by (etac UN_E 1);
by (etac CollectE 1);
@@ -306,7 +306,7 @@
qed "f_n_pairs_in_R";
Goalw [restrict_def]
- "[| restrict(f, domain(x))=x; f:n->X; domain(x) <= n |] \
+ "[| restrict(f, domain(x))=x; f \\<in> n->X; domain(x) \\<subseteq> n |] \
\ ==> restrict(cons(<n, y>, f), domain(x)) = x";
by (eresolve_tac [sym RS trans RS sym] 1);
by (rtac fun_extension 1);
@@ -315,11 +315,11 @@
by (asm_full_simp_tac (simpset() addsimps [subsetD RS cons_val_k]) 1);
qed "restrict_cons_eq_restrict";
-Goal "[| ALL x:f``n. restrict(f`n, domain(x))=x; \
-\ f : nat -> XX; \
-\ n:nat; domain(f`n) = succ(n); \
-\ (UN x:f``n. domain(x)) <= n |] \
-\ ==> ALL x:f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x";
+Goal "[| \\<forall>x \\<in> f``n. restrict(f`n, domain(x))=x; \
+\ f \\<in> nat -> XX; \
+\ n \\<in> nat; domain(f`n) = succ(n); \
+\ (\\<Union>x \\<in> f``n. domain(x)) \\<subseteq> n |] \
+\ ==> \\<forall>x \\<in> f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x";
by (rtac ballI 1);
by (asm_full_simp_tac (simpset() addsimps [image_fun_succ]) 1);
by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1));
@@ -330,8 +330,8 @@
qed "all_in_image_restrict_eq";
Goalw [RR_def, allRR_def]
- "[| ALL b<nat. <f``b, f`b> : RR; \
-\ f: nat -> XX; range(R) <= domain(R); x:domain(R)|] \
+ "[| \\<forall>b<nat. <f``b, f`b> \\<in> RR; \
+\ f \\<in> nat -> XX; range(R) \\<subseteq> domain(R); x \\<in> domain(R)|] \
\ ==> allRR";
by (rtac oallI 1);
by (dtac ltD 1);
@@ -341,7 +341,7 @@
(simpset() addsimps [singleton_fun RS domain_of_fun,
singleton_0, singleton_in_funs])) 1);
(*induction step*) (** LEVEL 5 **)
-by (full_simp_tac (*prevent simplification of ~EX to ALL~*)
+by (full_simp_tac (*prevent simplification of ~\\<exists>to \\<forall>~*)
(FOL_ss addsimps [separation, split]) 1);
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
THEN (assume_tac 1));
@@ -380,8 +380,8 @@
Goalw [allRR_def]
- "[| allRR; f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat |] \
-\ ==> f`n : succ(n) -> domain(R) & (ALL i:n. <f`n`i, f`n`succ(i)>:R)";
+ "[| allRR; f \\<in> nat -> XX; range(R) \\<subseteq> domain(R); x \\<in> domain(R); n \\<in> nat |] \
+\ ==> f`n \\<in> succ(n) -> domain(R) & (\\<forall>i \\<in> n. <f`n`i, f`n`succ(i)>:R)";
by (dtac ospec 1);
by (eresolve_tac [Ord_nat RSN (2, ltI)] 1);
by (etac CollectE 1);
@@ -393,7 +393,7 @@
addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1);
qed "lemma2";
-Goal "[| allRR; f : nat -> XX; n:nat; range(R) <= domain(R); x:domain(R) \
+Goal "[| allRR; f \\<in> nat -> XX; n \\<in> nat; range(R) \\<subseteq> domain(R); x \\<in> domain(R) \
\ |] ==> f`n`n = f`succ(n)`n";
by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1
THEN REPEAT (assume_tac 1));
@@ -420,7 +420,7 @@
by (etac bexE 1);
by (dresolve_tac [export simplify_recursion] 1
THEN REPEAT (assume_tac 1));
-by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1);
+by (res_inst_tac [("x","\\<lambda>n \\<in> nat. f`n`n")] bexI 1);
by (rtac lam_type 2);
by (eresolve_tac [[export lemma2 RS conjunct1, succI1] MRS apply_type] 2
THEN REPEAT (assume_tac 2));
@@ -432,18 +432,18 @@
qed "DC_nat_imp_DC0";
(* ********************************************************************** *)
-(* ALL K. Card(K) --> DC(K) ==> WO3 *)
+(* \\<forall>K. Card(K) --> DC(K) ==> WO3 *)
(* ********************************************************************** *)
Goalw [lesspoll_def]
- "[| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0";
+ "[| ~ A lesspoll B; C lesspoll B |] ==> A - C \\<noteq> 0";
by (fast_tac (claset() addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll]
addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1);
qed "lesspoll_lemma";
val [f_type, Ord_a, not_eq] = goalw thy [inj_def]
- "[| f:a->X; Ord(a); (!!b c. [| b<c; c:a |] ==> f`b~=f`c) |] \
-\ ==> f:inj(a, X)";
+ "[| f \\<in> a->X; Ord(a); (!!b c. [| b<c; c \\<in> a |] ==> f`b\\<noteq>f`c) |] \
+\ ==> f \\<in> inj(a, X)";
by (resolve_tac [f_type RS CollectI] 1);
by (REPEAT (resolve_tac [ballI,impI] 1));
by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1
@@ -452,11 +452,11 @@
by (REPEAT (fast_tac (claset() addDs [not_eq, not_eq RS not_sym]) 1));
qed "fun_Ord_inj";
-Goal "[| f:X->Y; A<=X; a:A |] ==> f`a : f``A";
+Goal "[| f \\<in> X->Y; A \\<subseteq> X; a \\<in> A |] ==> f`a \\<in> f``A";
by (fast_tac (claset() addSEs [image_fun RS ssubst]) 1);
qed "value_in_image";
-Goalw [DC_def, WO3_def] "ALL K. Card(K) --> DC(K) ==> WO3";
+Goalw [DC_def, WO3_def] "\\<forall>K. Card(K) --> DC(K) ==> WO3";
by (rtac allI 1);
by (excluded_middle_tac "A lesspoll Hartog(A)" 1);
by (fast_tac (claset() addSDs [lesspoll_imp_ex_lt_eqpoll]
@@ -465,7 +465,7 @@
by (rtac Card_Hartog 1);
by (eres_inst_tac [("x","A")] allE 1);
by (eres_inst_tac [("x","{<z1,z2>:Pow(A)*A . z1 \
-\ lesspoll Hartog(A) & z2 ~: z1}")] allE 1);
+\ lesspoll Hartog(A) & z2 \\<notin> z1}")] allE 1);
by (Asm_full_simp_tac 1);
by (etac impE 1);
by (fast_tac (claset() addEs [lesspoll_lemma RS not_emptyE]) 1);
@@ -481,10 +481,10 @@
qed "DC_WO3";
(* ********************************************************************** *)
-(* WO1 ==> ALL K. Card(K) --> DC(K) *)
+(* WO1 ==> \\<forall>K. Card(K) --> DC(K) *)
(* ********************************************************************** *)
-Goal "[| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b";
+Goal "[| Ord(a); b \\<in> a |] ==> (\\<lambda>x \\<in> a. P(x))``b = (\\<lambda>x \\<in> b. P(x))``b";
by (rtac images_eq 1);
by (REPEAT (fast_tac (claset() addSEs [RepFunI, OrdmemD]
addSIs [lam_type]) 2));
@@ -494,25 +494,25 @@
by (Asm_full_simp_tac 1);
qed "lam_images_eq";
-Goalw [lesspoll_def] "[| Card(K); b:K |] ==> b lesspoll K";
+Goalw [lesspoll_def] "[| Card(K); b \\<in> K |] ==> b lesspoll K";
by (asm_full_simp_tac (simpset() addsimps [Card_iff_initial]) 1);
by (fast_tac (claset() addSIs [le_imp_lepoll, ltI, leI]) 1);
qed "in_Card_imp_lesspoll";
-Goal "(lam b:a. P(b)) : a -> {P(b). b:a}";
+Goal "(\\<lambda>b \\<in> a. P(b)) \\<in> a -> {P(b). b \\<in> a}";
by (fast_tac (claset() addSIs [lam_type, RepFunI]) 1);
qed "lam_type_RepFun";
-Goal "[| ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); \
-\ b:K; Z:Pow(X); Z lesspoll K |] \
-\ ==> {x:X. <Z,x> : R} ~= 0";
+Goal "[| \\<forall>Y \\<in> Pow(X). Y lesspoll K --> (\\<exists>x \\<in> X. <Y, x> \\<in> R); \
+\ b \\<in> K; Z \\<in> Pow(X); Z lesspoll K |] \
+\ ==> {x \\<in> X. <Z,x> \\<in> R} \\<noteq> 0";
by (Blast_tac 1);
qed "lemmaX";
Goal "[| Card(K); well_ord(X,Q); \
-\ ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |] \
-\ ==> ff(b, X, Q, R) : {x:X. <(lam c:b. ff(c, X, Q, R))``b, x> : R}";
-by (res_inst_tac [("P","b:K")] impE 1 THEN TRYALL assume_tac);
+\ \\<forall>Y \\<in> Pow(X). Y lesspoll K --> (\\<exists>x \\<in> X. <Y, x> \\<in> R); b \\<in> K |] \
+\ ==> ff(b, X, Q, R) \\<in> {x \\<in> X. <(\\<lambda>c \\<in> b. ff(c, X, Q, R))``b, x> \\<in> R}";
+by (res_inst_tac [("P","b \\<in> K")] impE 1 THEN TRYALL assume_tac);
by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1
THEN REPEAT (assume_tac 1));
by (rtac impI 1);
@@ -527,10 +527,10 @@
MRS lepoll_lesspoll_lesspoll]) 1);
qed "lemma";
-Goalw [DC_def, WO1_def] "WO1 ==> ALL K. Card(K) --> DC(K)";
+Goalw [DC_def, WO1_def] "WO1 ==> \\<forall>K. Card(K) --> DC(K)";
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE,exE,conjE] 1));
-by (res_inst_tac [("x","lam b:K. ff(b, X, Ra, R)")] bexI 1);
+by (res_inst_tac [("x","\\<lambda>b \\<in> K. ff(b, X, Ra, R)")] bexI 1);
by (rtac lam_type 2);
by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2));
by (asm_full_simp_tac (simpset()
--- a/src/ZF/AC/DC.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/DC.thy Mon May 21 14:45:52 2001 +0200
@@ -16,15 +16,15 @@
rules
DC_def "DC(a) ==
- ALL X R. R<=Pow(X)*X &
- (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R))
- --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
+ \\<forall>X R. R \\<subseteq> Pow(X)*X &
+ (\\<forall>Y \\<in> Pow(X). Y lesspoll a --> (\\<exists>x \\<in> X. <Y,x> \\<in> R))
+ --> (\\<exists>f \\<in> a->X. \\<forall>b<a. <f``b,f`b> \\<in> R)"
- DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R)
- --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
+ DC0_def "DC0 == \\<forall>A B R. R \\<subseteq> A*B & R\\<noteq>0 & range(R) \\<subseteq> domain(R)
+ --> (\\<exists>f \\<in> nat->domain(R). \\<forall>n \\<in> nat. <f`n,f`succ(n)>:R)"
ff_def "ff(b, X, Q, R) ==
- transrec(b, %c r. THE x. first(x, {x:X. <r``c, x> : R}, Q))"
+ transrec(b, %c r. THE x. first(x, {x \\<in> X. <r``c, x> \\<in> R}, Q))"
locale DC0_imp =
@@ -35,10 +35,10 @@
R :: i
assumes
- all_ex "ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R)"
+ all_ex "\\<forall>Y \\<in> Pow(X). Y lesspoll nat --> (\\<exists>x \\<in> X. <Y, x> \\<in> R)"
defines
- XX_def "XX == (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R})"
+ XX_def "XX == (\\<Union>n \\<in> nat. {f \\<in> n->X. \\<forall>k \\<in> n. <f``k, f`k> \\<in> R})"
RR_def "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))
& restrict(z2, domain(z1)) = z1}"
@@ -53,18 +53,18 @@
allRR :: o
defines
- XX_def "XX == (UN n:nat.
- {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})"
+ XX_def "XX == (\\<Union>n \\<in> nat.
+ {f \\<in> succ(n)->domain(R). \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R})"
RR_def
"RR == {<z1,z2>:Fin(XX)*XX.
- (domain(z2)=succ(UN f:z1. domain(f))
- & (ALL f:z1. restrict(z2, domain(f)) = f))
- | (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f))
- & (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
+ (domain(z2)=succ(\\<Union>f \\<in> z1. domain(f))
+ & (\\<forall>f \\<in> z1. restrict(z2, domain(f)) = f))
+ | (~ (\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> z1. domain(f))
+ & (\\<forall>f \\<in> z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
allRR_def
- "allRR == ALL b<nat.
- <f``b, f`b> :
- {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))
- & (UN f:z1. domain(f)) = b
- & (ALL f:z1. restrict(z2,domain(f)) = f))}"
+ "allRR == \\<forall>b<nat.
+ <f``b, f`b> \\<in>
+ {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(\\<Union>f \\<in> z1. domain(f))
+ & (\\<Union>f \\<in> z1. domain(f)) = b
+ & (\\<forall>f \\<in> z1. restrict(z2,domain(f)) = f))}"
end
--- a/src/ZF/AC/DC_lemmas.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/DC_lemmas.ML Mon May 21 14:45:52 2001 +0200
@@ -7,14 +7,14 @@
*)
val [prem] = goalw thy [lepoll_def]
- "Ord(a) ==> {P(b). b:a} lepoll a";
-by (res_inst_tac [("x","lam z:RepFun(a,P). LEAST i. z=P(i)")] exI 1);
+ "Ord(a) ==> {P(b). b \\<in> a} lepoll a";
+by (res_inst_tac [("x","\\<lambda>z \\<in> RepFun(a,P). LEAST i. z=P(i)")] exI 1);
by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1);
by (fast_tac (claset() addSIs [Least_in_Ord, prem]) 1);
by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1));
qed "RepFun_lepoll";
-Goalw [lesspoll_def] "n:nat ==> n lesspoll nat";
+Goalw [lesspoll_def] "n \\<in> nat ==> n lesspoll nat";
by (rtac conjI 1);
by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1);
by (rtac notI 1);
@@ -26,47 +26,47 @@
qed "n_lesspoll_nat";
Goalw [lepoll_def]
- "[| f:X->Y; Ord(X) |] ==> f``X lepoll X";
-by (res_inst_tac [("x","lam x:f``X. LEAST y. f`y = x")] exI 1);
+ "[| f \\<in> X->Y; Ord(X) |] ==> f``X lepoll X";
+by (res_inst_tac [("x","\\<lambda>x \\<in> f``X. LEAST y. f`y = x")] exI 1);
by (res_inst_tac [("d","%z. f`z")] lam_injective 1);
by (fast_tac (claset() addSIs [Least_in_Ord, apply_equality]) 1);
by (fast_tac (claset() addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1);
qed "image_Ord_lepoll";
val [major, minor] = goal thy
- "[| (!!g. g:X ==> EX u. <g,u>:R); R<=X*X \
-\ |] ==> range(R) <= domain(R)";
+ "[| (!!g. g \\<in> X ==> \\<exists>u. <g,u>:R); R \\<subseteq> X*X \
+\ |] ==> range(R) \\<subseteq> domain(R)";
by (rtac subsetI 1);
by (etac rangeE 1);
by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1);
by (Fast_tac 1);
qed "range_subset_domain";
-val prems = goal thy "!!k. k:n ==> k~=n";
+val prems = goal thy "!!k. k \\<in> n ==> k\\<noteq>n";
by (fast_tac (claset() addSEs [mem_irrefl]) 1);
qed "mem_not_eq";
-Goalw [succ_def] "g:n->X ==> cons(<n,x>, g) : succ(n) -> cons(x, X)";
+Goalw [succ_def] "g \\<in> n->X ==> cons(<n,x>, g) \\<in> succ(n) -> cons(x, X)";
by (fast_tac (claset() addSIs [fun_extend] addSEs [mem_irrefl]) 1);
qed "cons_fun_type";
-Goal "[| g:n->X; x:X |] ==> cons(<n,x>, g) : succ(n) -> X";
+Goal "[| g \\<in> n->X; x \\<in> X |] ==> cons(<n,x>, g) \\<in> succ(n) -> X";
by (etac (cons_absorb RS subst) 1 THEN etac cons_fun_type 1);
qed "cons_fun_type2";
-Goal "n: nat ==> cons(<n,x>, g)``n = g``n";
+Goal "n \\<in> nat ==> cons(<n,x>, g)``n = g``n";
by (fast_tac (claset() addSEs [mem_irrefl]) 1);
qed "cons_image_n";
-Goal "g:n->X ==> cons(<n,x>, g)`n = x";
+Goal "g \\<in> n->X ==> cons(<n,x>, g)`n = x";
by (fast_tac (claset() addSIs [apply_equality] addSEs [cons_fun_type]) 1);
qed "cons_val_n";
-Goal "k : n ==> cons(<n,x>, g)``k = g``k";
+Goal "k \\<in> n ==> cons(<n,x>, g)``k = g``k";
by (fast_tac (claset() addEs [mem_asym]) 1);
qed "cons_image_k";
-Goal "[| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
+Goal "[| k \\<in> n; g \\<in> n->X |] ==> cons(<n,x>, g)`k = g`k";
by (fast_tac (claset() addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1);
qed "cons_val_k";
@@ -74,7 +74,7 @@
by (asm_full_simp_tac (simpset() addsimps [domain_cons, succ_def]) 1);
qed "domain_cons_eq_succ";
-Goalw [restrict_def] "g:n->X ==> restrict(cons(<n,x>, g), n)=g";
+Goalw [restrict_def] "g \\<in> n->X ==> restrict(cons(<n,x>, g), n)=g";
by (rtac fun_extension 1);
by (rtac lam_type 1);
by (eresolve_tac [cons_fun_type RS apply_type] 1);
@@ -83,23 +83,23 @@
by (asm_full_simp_tac (simpset() addsimps [cons_val_k]) 1);
qed "restrict_cons_eq";
-Goal "[| Ord(k); i:k |] ==> succ(i) : succ(k)";
+Goal "[| Ord(k); i \\<in> k |] ==> succ(i) \\<in> succ(k)";
by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3));
by (REPEAT (fast_tac (claset() addEs [Ord_in_Ord, mem_irrefl, mem_asym]) 1));
qed "succ_in_succ";
Goalw [restrict_def]
- "[| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x";
+ "[| restrict(f, domain(g)) = g; x \\<in> domain(g) |] ==> f`x = g`x";
by (etac subst 1);
by (Asm_full_simp_tac 1);
qed "restrict_eq_imp_val_eq";
-Goal "[| domain(f)=A; f:B->C |] ==> f:A->C";
+Goal "[| domain(f)=A; f \\<in> B->C |] ==> f \\<in> A->C";
by (ftac domain_of_fun 1);
by (Fast_tac 1);
qed "domain_eq_imp_fun_type";
-Goal "[| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)";
+Goal "[| R \\<subseteq> A * B; R \\<noteq> 0 |] ==> \\<exists>x. x \\<in> domain(R)";
by (fast_tac (claset() addSEs [not_emptyE]) 1);
qed "ex_in_domain";
--- a/src/ZF/AC/HH.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/HH.ML Mon May 21 14:45:52 2001 +0200
@@ -8,42 +8,40 @@
AC15 ==> WO6
*)
-open HH;
-
(* ********************************************************************** *)
(* Lemmas useful in each of the three proofs *)
(* ********************************************************************** *)
Goal "HH(f,x,a) = \
-\ (let z = x - (UN b:a. HH(f,x,b)) \
-\ in if(f`z:Pow(z)-{0}, f`z, {x}))";
+\ (let z = x - (\\<Union>b \\<in> a. HH(f,x,b)) \
+\ in if(f`z \\<in> Pow(z)-{0}, f`z, {x}))";
by (resolve_tac [HH_def RS def_transrec RS trans] 1);
by (Simp_tac 1);
qed "HH_def_satisfies_eq";
-Goal "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}";
+Goal "HH(f,x,a) \\<in> Pow(x)-{0} | HH(f,x,a)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
by (Fast_tac 1);
qed "HH_values";
-Goal "B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
+Goal "B \\<subseteq> A ==> X-(\\<Union>a \\<in> A. P(a)) = X-(\\<Union>a \\<in> A-B. P(a))-(\\<Union>b \\<in> B. P(b))";
by (Fast_tac 1);
qed "subset_imp_Diff_eq";
-Goal "[| c:a-b; b<a |] ==> c=b | b<c & c<a";
+Goal "[| c \\<in> a-b; b<a |] ==> c=b | b<c & c<a";
by (etac ltE 1);
by (dtac Ord_linear 1);
by (fast_tac (claset() addSIs [ltI] addIs [Ord_in_Ord]) 2);
by (fast_tac (claset() addEs [Ord_in_Ord]) 1);
qed "Ord_DiffE";
-val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
+val prems = goal thy "(!!y. y \\<in> A ==> P(y) = {x}) ==> x - (\\<Union>y \\<in> A. P(y)) = x";
by (asm_full_simp_tac (simpset() addsimps prems) 1);
by (fast_tac (claset() addSDs [prem] addSEs [mem_irrefl]) 1);
qed "Diff_UN_eq_self";
-Goal "x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \
+Goal "x - (\\<Union>b \\<in> a. HH(f,x,b)) = x - (\\<Union>b \\<in> 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);
@@ -63,15 +61,15 @@
by (fast_tac (claset() addEs [ltE]) 1);
qed "HH_is_x_gt_too";
-Goal "[| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}";
+Goal "[| HH(f,x,a) \\<in> Pow(x)-{0}; b<a |] ==> HH(f,x,b) \\<in> Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1));
by (dtac subst 1 THEN (assume_tac 1));
by (fast_tac (claset() addSEs [mem_irrefl]) 1);
qed "HH_subset_x_lt_too";
-Goal "HH(f,x,a) : Pow(x)-{0} \
-\ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}";
+Goal "HH(f,x,a) \\<in> Pow(x)-{0} \
+\ ==> HH(f,x,a) \\<in> Pow(x - (\\<Union>b \\<in> 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 (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
@@ -80,8 +78,8 @@
by (fast_tac (subset_cs addSEs [mem_irrefl]) 1);
qed "HH_subset_x_imp_subset_Diff_UN";
-Goal "[| 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));
+Goal "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v \\<in> w |] ==> P";
+by (forw_inst_tac [("P","%y. y \\<in> Pow(x)-{0}")] subst 1 THEN (assume_tac 1));
by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1);
by (dtac subst_elem 1 THEN (assume_tac 1));
by (fast_tac (claset() addSIs [singleton_iff RS iffD2, equals0I]) 1);
@@ -97,8 +95,8 @@
qed "HH_eq_imp_arg_eq";
Goalw [lepoll_def, inj_def]
- "[| 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);
+ "[| HH(f, x, i) \\<in> Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}";
+by (res_inst_tac [("x","\\<lambda>j \\<in> i. HH(f, x, j)")] exI 1);
by (Asm_simp_tac 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);
@@ -114,7 +112,7 @@
by (fast_tac (claset() addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1);
qed "HH_Least_eq_x";
-Goal "a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}";
+Goal "a \\<in> (LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) \\<in> Pow(x)-{0}";
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1));
by (rtac less_LeastE 1);
by (eresolve_tac [Ord_Least RSN (2, ltI)] 2);
@@ -126,45 +124,45 @@
(* ********************************************************************** *)
Goalw [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})";
+ "(\\<lambda>a \\<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
+\ \\<in> inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})";
by (Asm_full_simp_tac 1);
by (fast_tac (claset() addSIs [lam_type] addDs [less_Least_subset_x]
addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1);
qed "lam_Least_HH_inj_Pow";
-Goal "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})";
+Goal "\\<forall>a \\<in> (LEAST i. HH(f,x,i)={x}). \\<exists>z \\<in> x. HH(f,x,a) = {z} \
+\ ==> (\\<lambda>a \\<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
+\ \\<in> inj(LEAST i. HH(f,x,i)={x}, {{y}. y \\<in> x})";
by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1);
by (Asm_full_simp_tac 1);
qed "lam_Least_HH_inj";
Goalw [surj_def]
- "[| 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})";
+ "[| x - (\\<Union>a \\<in> A. F(a)) = 0; \
+\ \\<forall>a \\<in> A. \\<exists>z \\<in> x. F(a) = {z} |] \
+\ ==> (\\<lambda>a \\<in> A. F(a)) \\<in> surj(A, {{y}. y \\<in> x})";
by (asm_full_simp_tac (simpset() addsimps [lam_type, Diff_eq_0_iff]) 1);
by Safe_tac;
by (set_mp_tac 1);
by (deepen_tac (claset() addSIs [bexI] addSEs [equalityE]) 4 1);
qed "lam_surj_sing";
-Goal "y:Pow(x)-{0} ==> x ~= 0";
+Goal "y \\<in> Pow(x)-{0} ==> x \\<noteq> 0";
by Auto_tac;
qed "not_emptyI2";
-Goal "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}";
+Goal "f`(x - (\\<Union>j \\<in> i. HH(f,x,j))): Pow(x - (\\<Union>j \\<in> i. HH(f,x,j)))-{0} \
+\ ==> HH(f, x, i) \\<in> Pow(x) - {0}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI,
not_emptyI2 RS if_P]) 1);
by (Fast_tac 1);
qed "f_subset_imp_HH_subset";
-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);
+val [prem] = goal thy "(!!z. z \\<in> Pow(x)-{0} ==> f`z \\<in> Pow(z)-{0}) ==> \
+\ x - (\\<Union>j \\<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0";
+by (excluded_middle_tac "?P \\<in> {0}" 1);
by (Fast_tac 2);
by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS
f_subset_imp_HH_subset] 1);
@@ -172,19 +170,19 @@
addSEs [mem_irrefl]) 1);
qed "f_subsets_imp_UN_HH_eq_x";
-Goal "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}";
+Goal "HH(f,x,i)=f`(x - (\\<Union>j \\<in> i. HH(f,x,j))) | HH(f,x,i)={x}";
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1);
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1);
qed "HH_values2";
-Goal "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))";
+Goal "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (\\<Union>j \\<in> i. HH(f,x,j)))";
by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1));
by (fast_tac (claset() addSEs [equalityE, mem_irrefl]
addSDs [singleton_subsetD]) 1);
qed "HH_subset_imp_eq";
-Goal "[| f : (Pow(x)-{0}) -> {{z}. z:x}; \
-\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
+Goal "[| f \\<in> (Pow(x)-{0}) -> {{z}. z \\<in> x}; \
+\ a \\<in> (LEAST i. HH(f,x,i)={x}) |] ==> \\<exists>z \\<in> x. HH(f,x,a) = {z}";
by (dtac less_Least_subset_x 1);
by (ftac HH_subset_imp_eq 1);
by (dtac apply_type 1);
@@ -195,16 +193,16 @@
qed "f_sing_imp_HH_sing";
Goalw [bij_def]
- "[| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
-\ f : (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})";
+ "[| x - (\\<Union>j \\<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \
+\ f \\<in> (Pow(x)-{0}) -> {{z}. z \\<in> x} |] \
+\ ==> (\\<lambda>a \\<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \
+\ \\<in> bij(LEAST i. HH(f,x,i)={x}, {{y}. y \\<in> x})";
by (fast_tac (claset() addSIs [lam_Least_HH_inj, lam_surj_sing,
f_sing_imp_HH_sing]) 1);
qed "f_sing_lam_bij";
-Goal "f: (PROD X: Pow(x)-{0}. F(X)) \
-\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
+Goal "f \\<in> (\\<Pi>X \\<in> Pow(x)-{0}. F(X)) \
+\ ==> (\\<lambda>X \\<in> Pow(x)-{0}. {f`X}) \\<in> (\\<Pi>X \\<in> Pow(x)-{0}. {{z}. z \\<in> F(X)})";
by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
addDs [apply_type]) 1);
qed "lam_singI";
--- a/src/ZF/AC/HH.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/HH.thy Mon May 21 14:45:52 2001 +0200
@@ -16,8 +16,8 @@
defs
- HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (UN c:b. r`c)
- in if(f`z:Pow(z)-{0}, f`z, {x}))"
+ HH_def "HH(f,x,a) == transrec(a, %b r. let z = x - (\\<Union>c \\<in> b. r`c)
+ in if(f`z \\<in> Pow(z)-{0}, f`z, {x}))"
end
--- a/src/ZF/AC/Hartog.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/Hartog.ML Mon May 21 14:45:52 2001 +0200
@@ -5,15 +5,13 @@
Some proofs on the Hartogs function.
*)
-open Hartog;
-
-Goal "ALL a. Ord(a) --> a:X ==> P";
-by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1);
+Goal "\\<forall>a. Ord(a) --> a \\<in> X ==> P";
+by (res_inst_tac [("X1","{y \\<in> X. Ord(y)}")] (ON_class RS revcut_rl) 1);
by (Fast_tac 1);
qed "Ords_in_set";
Goalw [lepoll_def] "[| Ord(a); a lepoll X |] ==> \
-\ EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)";
+\ \\<exists>Y. Y \\<subseteq> X & (\\<exists>R. well_ord(Y,R) & ordertype(Y,R)=a)";
by (etac exE 1);
by (REPEAT (resolve_tac [exI, conjI] 1));
by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1);
@@ -29,7 +27,7 @@
qed "Ord_lepoll_imp_ex_well_ord";
Goal "[| Ord(a); a lepoll X |] ==> \
-\ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)";
+\ \\<exists>Y. Y \\<subseteq> X & (\\<exists>R. R \\<subseteq> X*X & ordertype(Y,R)=a)";
by (dtac Ord_lepoll_imp_ex_well_ord 1 THEN (assume_tac 1));
by Safe_tac;
by (REPEAT (ares_tac [exI, conjI] 1));
@@ -37,9 +35,9 @@
by (Fast_tac 1);
qed "Ord_lepoll_imp_eq_ordertype";
-Goal "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}";
+Goal "\\<forall>a. Ord(a) --> a lepoll X ==> \
+\ \\<forall>a. Ord(a) --> \
+\ a:{a. Z \\<in> Pow(X)*Pow(X*X), \\<exists>Y R. Z=<Y,R> & ordertype(Y,R)=a}";
by (REPEAT (resolve_tac [allI,impI] 1));
by (REPEAT (eresolve_tac [allE, impE] 1));
by (assume_tac 1);
@@ -47,11 +45,11 @@
by (fast_tac (claset() addSIs [ReplaceI] addEs [sym]) 1);
qed "Ords_lepoll_set_lemma";
-Goal "ALL a. Ord(a) --> a lepoll X ==> P";
+Goal "\\<forall>a. Ord(a) --> a lepoll X ==> P";
by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1);
qed "Ords_lepoll_set";
-Goal "EX a. Ord(a) & ~a lepoll X";
+Goal "\\<exists>a. Ord(a) & ~a lepoll X";
by (rtac swap 1);
by (Fast_tac 1);
by (rtac Ords_lepoll_set 1);
--- a/src/ZF/AC/WO1_AC.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_AC.ML Mon May 21 14:45:52 2001 +0200
@@ -11,22 +11,20 @@
Assume WO1. Let s be a set of infinite sets.
-Suppose x:s. Then x is equipollent to |x| (by WO1), an infinite cardinal;
+Suppose x \\<in> s. Then x is equipollent to |x| (by WO1), an infinite cardinal;
call it K. Since K = K |+| K = |K+K| (by InfCard_cdouble_eq) there is an
-isomorphism h: bij(K+K, x). (Here + means disjoint sum.)
+isomorphism h \\<in> bij(K+K, x). (Here + means disjoint sum.)
So there is a partition of x into 2-element sets, namely
- {{h(Inl(i)), h(Inr(i))} . i:K}
+ {{h(Inl(i)), h(Inr(i))} . i \\<in> K}
-So for all x:s the desired partition exists. By AC1 (which follows from WO1)
-there exists a function f that chooses a partition for each x:s. Therefore we
+So for all x \\<in> s the desired partition exists. By AC1 (which follows from WO1)
+there exists a function f that chooses a partition for each x \\<in> s. Therefore we
have AC10(2).
*)
-open WO1_AC;
-
(* ********************************************************************** *)
(* WO1 ==> AC1 *)
(* ********************************************************************** *)
@@ -39,14 +37,14 @@
(* WO1 ==> AC10(n) (n >= 1) *)
(* ********************************************************************** *)
-Goalw [WO1_def] "[| WO1; ALL B:A. EX C:D(B). P(C,B) |] \
-\ ==> EX f. ALL B:A. P(f`B,B)";
-by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1);
+Goalw [WO1_def] "[| WO1; \\<forall>B \\<in> A. \\<exists>C \\<in> D(B). P(C,B) |] \
+\ ==> \\<exists>f. \\<forall>B \\<in> A. P(f`B,B)";
+by (eres_inst_tac [("x","Union({{C \\<in> D(B). P(C,B)}. B \\<in> A})")] allE 1);
by (etac exE 1);
by (dtac ex_choice_fun 1);
by (Fast_tac 1);
by (etac exE 1);
-by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1);
+by (res_inst_tac [("x","\\<lambda>x \\<in> A. f`{C \\<in> D(x). P(C,x)}")] exI 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addSDs [RepFunI RSN (2, apply_type)]) 1);
val lemma1 = result();
@@ -67,23 +65,23 @@
by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1);
val lemma2_1 = result();
-Goal "f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))";
+Goal "f \\<in> bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i \\<in> D} \\<in> Pow(Pow(B))";
by (fast_tac (claset() addSEs [bij_is_fun RS apply_type]) 1);
val lemma2_2 = result();
-Goal "[| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b";
+Goal "[| f \\<in> inj(A,B); f`a = f`b; a \\<in> A; b \\<in> A |] ==> a=b";
by (rtac inj_equality 1);
by (TRYALL (fast_tac (claset() addSEs [inj_is_fun RS apply_Pair] addEs [subst])));
val lemma = result();
Goalw AC_aux_defs
- "f : bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})";
+ "f \\<in> bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i \\<in> D})";
by (blast_tac (claset() addDs [bij_is_inj RS lemma]) 1);
val lemma2_3 = result();
val [major, minor] = goalw thy AC_aux_defs
- "[| f : bij(D+D, B); 1 le n |] ==> \
-\ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))";
+ "[| f \\<in> bij(D+D, B); 1 le n |] ==> \
+\ sets_of_size_between({{f`Inl(i), f`Inr(i)}. i \\<in> D}, 2, succ(n))";
by (rewtac succ_def);
by (fast_tac (claset()
addSIs [cons_lepoll_cong, minor, lepoll_refl]
@@ -94,12 +92,12 @@
val lemma2_4 = result();
Goalw [bij_def, surj_def]
- "f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B";
+ "f \\<in> bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i \\<in> D})=B";
by (fast_tac (claset() addSEs [inj_is_fun RS apply_type]) 1);
val lemma2_5 = result();
Goal "[| WO1; ~Finite(B); 1 le n |] \
-\ ==> EX C:Pow(Pow(B)). pairwise_disjoint(C) & \
+\ ==> \\<exists>C \\<in> Pow(Pow(B)). pairwise_disjoint(C) & \
\ sets_of_size_between(C, 2, succ(n)) & \
\ Union(C)=B";
by (eresolve_tac [lemma2_1 RS (eqpoll_def RS def_imp_iff RS iffD1 RS exE)] 1
--- a/src/ZF/AC/WO1_WO6.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_WO6.ML Mon May 21 14:45:52 2001 +0200
@@ -32,15 +32,15 @@
(* ********************************************************************** *)
-Goal "f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
+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:surj(A,B) ==> (UN a:A. {f`a}) = B";
+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:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
+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";
@@ -68,7 +68,7 @@
(* ********************************************************************** *)
-Goalw WO_defs "[| m:nat; 1 le m; WO4(m) |] ==> WO5";
+Goalw WO_defs "[| m \\<in> nat; 1 le m; WO4(m) |] ==> WO5";
by (Blast_tac 1);
qed "WO4_WO5";
--- a/src/ZF/AC/WO1_WO7.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_WO7.ML Mon May 21 14:45:52 2001 +0200
@@ -31,7 +31,7 @@
(* ********************************************************************** *)
(* The Rubins' proof of the other implication is contained within the *)
-(* following sentence : *)
+(* following sentence \\<in> *)
(* "... 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 *)
--- a/src/ZF/AC/WO1_WO7.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_WO7.thy Mon May 21 14:45:52 2001 +0200
@@ -12,6 +12,6 @@
constdefs
LEMMA :: o
"LEMMA ==
- ALL X. ~Finite(X) --> (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"
+ \\<forall>X. ~Finite(X) --> (\\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
end
--- a/src/ZF/AC/WO1_WO8.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO1_WO8.ML Mon May 21 14:45:52 2001 +0200
@@ -19,11 +19,11 @@
Goalw WO_defs "WO8 ==> WO1";
by (rtac allI 1);
-by (eres_inst_tac [("x","{{x}. x:A}")] allE 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","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
-by (fast_tac (claset() addSIs [lam_type]
- addss (simpset() addsimps [singleton_eq_iff, the_equality])) 1);
+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/WO2_AC16.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO2_AC16.ML Mon May 21 14:45:52 2001 +0200
@@ -19,10 +19,10 @@
(* ********************************************************************** *)
-Goal "[| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \
-\ --> (EX! Y. Y:F(y) & f(z)<=Y); \
-\ ALL i j. i le j --> F(i) <= F(j); j le i; i<x; z<a; \
-\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \
+Goal "[| \\<forall>y<x. \\<forall>z<a. z<y | (\\<exists>Y \\<in> F(y). f(z)<=Y) \
+\ --> (\\<exists>! Y. Y \\<in> F(y) & f(z)<=Y); \
+\ \\<forall>i j. i le j --> F(i) \\<subseteq> F(j); j le i; i<x; z<a; \
+\ V \\<in> F(i); f(z)<=V; W \\<in> F(j); f(z)<=W |] \
\ ==> V = W";
by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1));
by (dtac subsetD 1 THEN (assume_tac 1));
@@ -33,10 +33,10 @@
val lemma3_1 = result();
-Goal "[| ALL y<x. ALL z<a. z<y | (EX Y: F(y). f(z)<=Y) \
-\ --> (EX! Y. Y:F(y) & f(z)<=Y); \
-\ ALL i j. i le j --> F(i) <= F(j); i<x; j<x; z<a; \
-\ V: F(i); f(z)<=V; W:F(j); f(z)<=W |] \
+Goal "[| \\<forall>y<x. \\<forall>z<a. z<y | (\\<exists>Y \\<in> F(y). f(z)<=Y) \
+\ --> (\\<exists>! Y. Y \\<in> F(y) & f(z)<=Y); \
+\ \\<forall>i j. i le j --> F(i) \\<subseteq> F(j); i<x; j<x; z<a; \
+\ V \\<in> F(i); f(z)<=V; W \\<in> F(j); f(z)<=W |] \
\ ==> V = W";
by (res_inst_tac [("j","j")] ([lt_Ord, lt_Ord] MRS Ord_linear_le) 1
THEN (REPEAT (assume_tac 1)));
@@ -45,24 +45,24 @@
val lemma3 = result();
-Goal "[| ALL y<x. F(y) <= X & \
-\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \
-\ (EX! Y. Y : F(y) & fa(x) <= Y)); x < a |] \
-\ ==> ALL y<x. ALL z<a. z < y | (EX Y:F(y). fa(z) <= Y) --> \
-\ (EX! Y. Y : F(y) & fa(z) <= Y)";
+Goal "[| \\<forall>y<x. F(y) \\<subseteq> X & \
+\ (\\<forall>x<a. x < y | (\\<exists>Y \\<in> F(y). fa(x) \\<subseteq> Y) --> \
+\ (\\<exists>! Y. Y \\<in> F(y) & fa(x) \\<subseteq> Y)); x < a |] \
+\ ==> \\<forall>y<x. \\<forall>z<a. z < y | (\\<exists>Y \\<in> F(y). fa(z) \\<subseteq> Y) --> \
+\ (\\<exists>! Y. Y \\<in> F(y) & fa(z) \\<subseteq> Y)";
by (REPEAT (resolve_tac [oallI, impI] 1));
by (dtac ospec 1 THEN (assume_tac 1));
by (fast_tac (FOL_cs addSEs [oallE]) 1);
val lemma4 = result();
-Goal "[| ALL y<x. F(y) <= X & \
-\ (ALL x<a. x < y | (EX Y:F(y). fa(x) <= Y) --> \
-\ (EX! Y. Y : F(y) & fa(x) <= Y)); \
-\ x < a; Limit(x); ALL i j. i le j --> F(i) <= F(j) |] \
-\ ==> (UN x<x. F(x)) <= X & \
-\ (ALL xa<a. xa < x | (EX x:UN x<x. F(x). fa(xa) <= x) \
-\ --> (EX! Y. Y : (UN x<x. F(x)) & fa(xa) <= Y))";
+Goal "[| \\<forall>y<x. F(y) \\<subseteq> X & \
+\ (\\<forall>x<a. x < y | (\\<exists>Y \\<in> F(y). fa(x) \\<subseteq> Y) --> \
+\ (\\<exists>! Y. Y \\<in> F(y) & fa(x) \\<subseteq> Y)); \
+\ x < a; Limit(x); \\<forall>i j. i le j --> F(i) \\<subseteq> F(j) |] \
+\ ==> (\\<Union>x<x. F(x)) \\<subseteq> X & \
+\ (\\<forall>xa<a. xa < x | (\\<exists>x \\<in> \\<Union>x<x. F(x). fa(xa) \\<subseteq> x) \
+\ --> (\\<exists>! Y. Y \\<in> (\\<Union>x<x. F(x)) & fa(xa) \\<subseteq> Y))";
by (rtac conjI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
@@ -129,8 +129,8 @@
subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1);
qed "Finite_lesspoll_infinite_Ord";
-Goal "[| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \
-\ b<a; ~Finite(a); Card(a); n:nat |] \
+Goal "[| \\<forall>x \\<in> X. x lepoll n & x \\<subseteq> T; well_ord(T, R); X lepoll b; \
+\ b<a; ~Finite(a); Card(a); n \\<in> nat |] \
\ ==> Union(X) lesspoll a";
by (excluded_middle_tac "Finite(X)" 1);
by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2
@@ -169,18 +169,18 @@
qed "Un_lepoll_succ";
-Goal "Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
+Goal "Ord(a) ==> F(a) - (\\<Union>b<succ(a). F(b)) = 0";
by (fast_tac (claset() addSIs [OUN_I, le_refl]) 1);
qed "Diff_UN_succ_empty";
-Goal "Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
+Goal "Ord(a) ==> F(a) Un X - (\\<Union>b<succ(a). F(b)) \\<subseteq> X";
by (fast_tac (claset() addSIs [OUN_I, le_refl]) 1);
qed "Diff_UN_succ_subset";
Goal "Ord(x) ==> \
-\ recfunAC16(f, g, x, a) - (UN i<x. recfunAC16(f, g, i, a)) lepoll 1";
+\ recfunAC16(f, g, x, a) - (\\<Union>i<x. recfunAC16(f, g, i, a)) lepoll 1";
by (etac Ord_cases 1);
by (asm_simp_tac (simpset() addsimps [recfunAC16_0,
empty_subsetI RS subset_imp_lepoll]) 1);
@@ -195,15 +195,15 @@
qed "recfunAC16_Diff_lepoll_1";
-Goal "[| z : F(x); Ord(x) |] \
-\ ==> z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))";
+Goal "[| z \\<in> F(x); Ord(x) |] \
+\ ==> z \\<in> F(LEAST i. z \\<in> F(i)) - (\\<Union>j<(LEAST i. z \\<in> F(i)). F(j))";
by (fast_tac (claset() addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1);
qed "in_Least_Diff";
-Goal "[| (LEAST i. w:F(i)) = (LEAST i. z:F(i)); \
-\ w:(UN i<a. F(i)); z:(UN i<a. F(i)) |] \
-\ ==> EX b<a. w:(F(b) - (UN c<b. F(c))) & z:(F(b) - (UN c<b. F(c)))";
+Goal "[| (LEAST i. w \\<in> F(i)) = (LEAST i. z \\<in> F(i)); \
+\ w \\<in> (\\<Union>i<a. F(i)); z \\<in> (\\<Union>i<a. F(i)) |] \
+\ ==> \\<exists>b<a. w \\<in> (F(b) - (\\<Union>c<b. F(c))) & z \\<in> (F(b) - (\\<Union>c<b. F(c)))";
by (REPEAT (etac OUN_E 1));
by (dresolve_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
by (forward_tac [lt_Ord RSN (2, in_Least_Diff)] 1 THEN (assume_tac 1));
@@ -215,15 +215,15 @@
qed "Least_eq_imp_ex";
-Goal "[| A lepoll 1; a:A; b:A |] ==> a=b";
+Goal "[| A lepoll 1; a \\<in> A; b \\<in> A |] ==> a=b";
by (fast_tac (claset() addSDs [lepoll_1_is_sing]) 1);
qed "two_in_lepoll_1";
-Goal "[| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |] \
-\ ==> (UN x<a. F(x)) lepoll a";
+Goal "[| \\<forall>i<a. F(i)-(\\<Union>j<i. F(j)) lepoll 1; Limit(a) |] \
+\ ==> (\\<Union>x<a. F(x)) lepoll a";
by (resolve_tac [lepoll_def RS (def_imp_iff RS iffD2)] 1);
-by (res_inst_tac [("x","lam z: (UN x<a. F(x)). LEAST i. z:F(i)")] exI 1);
+by (res_inst_tac [("x","\\<lambda>z \\<in> (\\<Union>x<a. F(x)). LEAST i. z \\<in> F(i)")] exI 1);
by (rewtac inj_def);
by (rtac CollectI 1);
by (rtac lam_type 1);
@@ -255,8 +255,8 @@
qed "recfunAC16_lepoll_index";
-Goal "[| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \
-\ A eqpoll a; y<a; ~Finite(a); Card(a); n:nat |] \
+Goal "[| recfunAC16(f,g,y,a) \\<subseteq> {X \\<in> Pow(A). X eqpoll n}; \
+\ A eqpoll a; y<a; ~Finite(a); Card(a); n \\<in> nat |] \
\ ==> Union(recfunAC16(f,g,y,a)) lesspoll a";
by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1);
by (rtac Union_lesspoll 1 THEN (TRYALL assume_tac));
@@ -268,10 +268,10 @@
qed "Union_recfunAC16_lesspoll";
-Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) \\<subseteq> {X \\<in> Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
-\ k: nat; y<a; \
-\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}) |] \
+\ k \\<in> nat; y<a; \
+\ fa \\<in> bij(a, {Y \\<in> Pow(A). Y eqpoll succ(k)}) |] \
\ ==> A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a";
by (rtac dbl_Diff_eqpoll_Card 1 THEN (TRYALL assume_tac));
by (rtac Union_recfunAC16_lesspoll 1 THEN (REPEAT (assume_tac 1)));
@@ -291,9 +291,9 @@
(eqpoll_trans RS eqpoll_trans) |> standard;
-Goal "[| x : Pow(A - B - fa`i); x eqpoll m; \
-\ fa : bij(a, {x: Pow(A) . x eqpoll k}); i<a; k:nat; m:nat |] \
-\ ==> fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}";
+Goal "[| x \\<in> Pow(A - B - fa`i); x eqpoll m; \
+\ fa \\<in> bij(a, {x \\<in> Pow(A) . x eqpoll k}); i<a; k \\<in> nat; m \\<in> nat |] \
+\ ==> fa ` i Un x \\<in> {x \\<in> Pow(A) . x eqpoll k #+ m}";
by (rtac CollectI 1);
by (fast_tac (claset()
addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1);
@@ -309,17 +309,17 @@
(* ********************************************************************** *)
-Goal "[| ALL y<succ(j). F(y)<=X & (ALL x<a. x<y | P(x,y) \
+Goal "[| \\<forall>y<succ(j). F(y)<=X & (\\<forall>x<a. x<y | P(x,y) \
\ --> Q(x,y)); succ(j)<a |] \
-\ ==> F(j)<=X & (ALL x<a. x<j | P(x,j) --> Q(x,j))";
+\ ==> F(j)<=X & (\\<forall>x<a. x<j | P(x,j) --> Q(x,j))";
by (dtac ospec 1);
by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl)] 1
THEN (REPEAT (assume_tac 1)));
val lemma6 = result();
-Goal "[| ALL x<a. x<j | P(x,j) --> Q(x,j); succ(j)<a |] \
-\ ==> P(j,j) --> (ALL x<a. x le j | P(x,j) --> Q(x,j))";
+Goal "[| \\<forall>x<a. x<j | P(x,j) --> Q(x,j); succ(j)<a |] \
+\ ==> P(j,j) --> (\\<forall>x<a. x le j | P(x,j) --> Q(x,j))";
by (fast_tac (claset() addSEs [leE]) 1);
val lemma7 = result();
@@ -329,8 +329,8 @@
(* ********************************************************************** *)
-Goal "[| A eqpoll a; ~ Finite(a); Ord(a); m:nat |] \
-\ ==> EX X:Pow(A). X eqpoll m";
+Goal "[| A eqpoll a; ~ Finite(a); Ord(a); m \\<in> nat |] \
+\ ==> \\<exists>X \\<in> Pow(A). X eqpoll m";
by (eresolve_tac [Ord_nat RSN (2, ltI) RS
(nat_le_infinite_Ord RSN (2, lt_trans2)) RS
leI RS le_imp_lepoll RS
@@ -341,12 +341,12 @@
qed "ex_subset_eqpoll";
-Goal "[| A <= B Un C; A Int C = 0 |] ==> A <= B";
+Goal "[| A \\<subseteq> B Un C; A Int C = 0 |] ==> A \\<subseteq> B";
by (Blast_tac 1);
qed "subset_Un_disjoint";
-Goal "[| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0";
+Goal "[| X \\<in> Pow(A - Union(B) -C); T \\<in> B; F \\<subseteq> T |] ==> F Int X = 0";
by (Blast_tac 1);
qed "Int_empty";
@@ -355,12 +355,12 @@
(* ********************************************************************** *)
-Goal "[| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
+Goal "[| A \\<subseteq> B; a \\<in> A; A - {a} = B - {a} |] ==> A = B";
by (fast_tac (claset() addSEs [equalityE]) 1);
qed "Diffs_eq_imp_eq";
-Goal "m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
+Goal "m \\<in> nat ==> \\<forall>A B. A \\<subseteq> B & m lepoll A & B lepoll m --> A=B";
by (induct_tac "m" 1);
by (fast_tac (claset() addSDs [lepoll_0_is_0]) 1);
by (REPEAT (resolve_tac [allI, impI] 1));
@@ -379,12 +379,12 @@
qed "subset_imp_eq_lemma";
-Goal "[| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B";
+Goal "[| A \\<subseteq> B; m lepoll A; B lepoll m; m \\<in> nat |] ==> A=B";
by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1);
qed "subset_imp_eq";
-Goal "[| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b<a; \
+Goal "[| f \\<in> bij(a, {Y \\<in> X. Y eqpoll succ(k)}); k \\<in> nat; f`b \\<subseteq> f`y; b<a; \
\ y<a |] ==> b=y";
by (dtac subset_imp_eq 1);
by (etac nat_succI 3);
@@ -397,14 +397,14 @@
qed "bij_imp_arg_eq";
-Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) \\<subseteq> {X \\<in> Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
-\ k : nat; m : nat; y<a; \
-\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
-\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \
-\ ==> EX X:{Y: Pow(A). Y eqpoll succ(k #+ m)}. fa`y <= X & \
-\ (ALL b<a. fa`b <= X --> \
-\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
+\ k \\<in> nat; m \\<in> nat; y<a; \
+\ fa \\<in> bij(a, {Y \\<in> Pow(A). Y eqpoll succ(k)}); \
+\ ~ (\\<exists>Y \\<in> recfunAC16(f, fa, y, a). fa`y \\<subseteq> Y) |] \
+\ ==> \\<exists>X \\<in> {Y \\<in> Pow(A). Y eqpoll succ(k #+ m)}. fa`y \\<subseteq> X & \
+\ (\\<forall>b<a. fa`b \\<subseteq> X --> \
+\ (\\<forall>T \\<in> recfunAC16(f, fa, y, a). ~ fa`b \\<subseteq> T))";
by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1
THEN REPEAT (assume_tac 1));
by (etac Card_is_Ord 1);
@@ -433,15 +433,15 @@
(* ********************************************************************** *)
-Goal "[| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \
+Goal "[| recfunAC16(f, fa, y, a) \\<subseteq> {X \\<in> Pow(A) . X eqpoll succ(k #+ m)}; \
\ Card(a); ~ Finite(a); A eqpoll a; \
-\ k : nat; m : nat; y<a; \
-\ fa : bij(a, {Y: Pow(A). Y eqpoll succ(k)}); \
-\ f : bij(a, {Y: Pow(A). Y eqpoll succ(k #+ m)}); \
-\ ~ (EX Y:recfunAC16(f, fa, y, a). fa`y <= Y) |] \
-\ ==> EX c<a. fa`y <= f`c & \
-\ (ALL b<a. fa`b <= f`c --> \
-\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))";
+\ k \\<in> nat; m \\<in> nat; y<a; \
+\ fa \\<in> bij(a, {Y \\<in> Pow(A). Y eqpoll succ(k)}); \
+\ f \\<in> bij(a, {Y \\<in> Pow(A). Y eqpoll succ(k #+ m)}); \
+\ ~ (\\<exists>Y \\<in> recfunAC16(f, fa, y, a). fa`y \\<subseteq> Y) |] \
+\ ==> \\<exists>c<a. fa`y \\<subseteq> f`c & \
+\ (\\<forall>b<a. fa`b \\<subseteq> f`c --> \
+\ (\\<forall>T \\<in> recfunAC16(f, fa, y, a). ~ fa`b \\<subseteq> T))";
by (dtac ex_next_set 1 THEN REPEAT (assume_tac 1));
by (etac bexE 1);
by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN
@@ -451,7 +451,7 @@
qed "ex_next_Ord";
-Goal "[| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y: (Z Un {W}) & P(Y)";
+Goal "[| \\<exists>! Y. Y \\<in> Z & P(Y); ~P(W) |] ==> \\<exists>! Y. Y \\<in> (Z Un {W}) & P(Y)";
by (Fast_tac 1);
qed "ex1_in_Un_sing";
@@ -460,12 +460,12 @@
(* ********************************************************************** *)
-Goal "[| ALL x<a. x<j | (EX xa:F(j). P(x, xa)) \
-\ --> (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X; \
-\ L : X; P(j, L) & (ALL x<a. P(x, L) --> (ALL xa:F(j). ~P(x, xa))) |] \
-\ ==> F(j) Un {L} <= X & \
-\ (ALL x<a. x le j | (EX xa: (F(j) Un {L}). P(x, xa)) --> \
-\ (EX! Y. Y: (F(j) Un {L}) & P(x, Y)))";
+Goal "[| \\<forall>x<a. x<j | (\\<exists>xa \\<in> F(j). P(x, xa)) \
+\ --> (\\<exists>! Y. Y \\<in> F(j) & P(x, Y)); F(j) \\<subseteq> X; \
+\ L \\<in> X; P(j, L) & (\\<forall>x<a. P(x, L) --> (\\<forall>xa \\<in> F(j). ~P(x, xa))) |] \
+\ ==> F(j) Un {L} \\<subseteq> X & \
+\ (\\<forall>x<a. x le j | (\\<exists>xa \\<in> (F(j) Un {L}). P(x, xa)) --> \
+\ (\\<exists>! Y. Y \\<in> (F(j) Un {L}) & P(x, Y)))";
by (rtac conjI 1);
by (fast_tac (claset() addSIs [singleton_subsetI]) 1);
by (rtac oallI 1);
@@ -479,12 +479,12 @@
(* ********************************************************************** *)
-Goal "[| b < a; f : bij(a, {Y: Pow(A) . Y eqpoll succ(k #+ m)}); \
-\ fa : bij(a, {Y: Pow(A) . Y eqpoll succ(k)}); \
-\ ~Finite(a); Card(a); A eqpoll a; k : nat; m : nat |] \
-\ ==> recfunAC16(f, fa, b, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)} & \
-\ (ALL x<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) --> \
-\ (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))";
+Goal "[| b < a; f \\<in> bij(a, {Y \\<in> Pow(A) . Y eqpoll succ(k #+ m)}); \
+\ fa \\<in> bij(a, {Y \\<in> Pow(A) . Y eqpoll succ(k)}); \
+\ ~Finite(a); Card(a); A eqpoll a; k \\<in> nat; m \\<in> nat |] \
+\ ==> recfunAC16(f, fa, b, a) \\<subseteq> {X \\<in> Pow(A) . X eqpoll succ(k #+ m)} & \
+\ (\\<forall>x<a. x < b | (\\<exists>Y \\<in> recfunAC16(f, fa, b, a). fa ` x \\<subseteq> Y) --> \
+\ (\\<exists>! Y. Y \\<in> recfunAC16(f, fa, b, a) & fa ` x \\<subseteq> Y))";
by (etac lt_induct 1);
by (ftac lt_Ord 1);
by (etac Ord_cases 1);
@@ -518,11 +518,11 @@
(* ********************************************************************** *)
val [prem1, prem2, prem3, prem4] = goal thy
- "[| (!!b. b<a ==> F(b) <= S & (ALL x<a. (x<b | (EX Y:F(b). f`x <= Y)) \
-\ --> (EX! Y. Y : F(b) & f`x <= Y))); \
-\ f:a->f``(a); Limit(a); (!!i j. i le j ==> F(i) <= F(j)) |] \
-\ ==> (UN j<a. F(j)) <= S & \
-\ (ALL x:f``a. EX! Y. Y : (UN j<a. F(j)) & x <= Y)";
+ "[| (!!b. b<a ==> F(b) \\<subseteq> S & (\\<forall>x<a. (x<b | (\\<exists>Y \\<in> F(b). f`x \\<subseteq> Y)) \
+\ --> (\\<exists>! Y. Y \\<in> F(b) & f`x \\<subseteq> Y))); \
+\ f \\<in> a->f``(a); Limit(a); (!!i j. i le j ==> F(i) \\<subseteq> F(j)) |] \
+\ ==> (\\<Union>j<a. F(j)) \\<subseteq> S & \
+\ (\\<forall>x \\<in> f``a. \\<exists>! Y. Y \\<in> (\\<Union>j<a. F(j)) & x \\<subseteq> Y)";
by (rtac conjI 1);
by (rtac subsetI 1);
by (etac OUN_E 1);
@@ -566,7 +566,7 @@
(* ********************************************************************** *)
-Goalw [AC16_def] "[| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
+Goalw [AC16_def] "[| WO2; 0<m; k \\<in> nat; m \\<in> nat |] ==> AC16(k #+ m,k)";
by (rtac allI 1);
by (rtac impI 1);
by (ftac WO2_infinite_subsets_eqpoll_X 1
@@ -580,8 +580,8 @@
by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS
def_imp_iff RS iffD1)] 1 THEN (assume_tac 1));
by (REPEAT (etac exE 1));
-by (res_inst_tac [("x","UN j<a. recfunAC16(fa,f,j,a)")] exI 1);
-by (res_inst_tac [("P","%z. ?Y & (ALL x:z. ?Z(x))")]
+by (res_inst_tac [("x","\\<Union>j<a. recfunAC16(fa,f,j,a)")] exI 1);
+by (res_inst_tac [("P","%z. ?Y & (\\<forall>x \\<in> z. ?Z(x))")]
(bij_is_surj RS surj_image_eq RS subst) 1
THEN (assume_tac 1));
by (rtac lemma_simp_induct 1);
--- a/src/ZF/AC/WO6_WO1.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO6_WO1.ML Mon May 21 14:45:52 2001 +0200
@@ -30,25 +30,25 @@
(* some properties of relation uu(beta, gamma, delta) - p. 2 *)
(* ********************************************************************** *)
-Goalw [uu_def] "domain(uu(f,b,g,d)) <= f`b";
+Goalw [uu_def] "domain(uu(f,b,g,d)) \\<subseteq> f`b";
by (Blast_tac 1);
qed "domain_uu_subset";
-Goal "ALL b<a. f`b lepoll m ==> \
-\ ALL b<a. ALL g<a. ALL d<a. domain(uu(f,b,g,d)) lepoll m";
+Goal "\\<forall>b<a. f`b lepoll m ==> \
+\ \\<forall>b<a. \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) lepoll m";
by (fast_tac (claset() addSEs
[domain_uu_subset RS subset_imp_lepoll RS lepoll_trans]) 1);
qed "quant_domain_uu_lepoll_m";
-Goalw [uu_def] "uu(f,b,g,d) <= f`b * f`g";
+Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`b * f`g";
by (Blast_tac 1);
qed "uu_subset1";
-Goalw [uu_def] "uu(f,b,g,d) <= f`d";
+Goalw [uu_def] "uu(f,b,g,d) \\<subseteq> f`d";
by (Blast_tac 1);
qed "uu_subset2";
-Goal "[| ALL b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
+Goal "[| \\<forall>b<a. f`b lepoll m; d<a |] ==> uu(f,b,g,d) lepoll m";
by (fast_tac (claset()
addSEs [uu_subset2 RS subset_imp_lepoll RS lepoll_trans]) 1);
qed "uu_lepoll_m";
@@ -57,10 +57,10 @@
(* Two cases for lemma ii *)
(* ********************************************************************** *)
Goalw [lesspoll_def]
- "ALL b<a. ALL g<a. ALL d<a. u(f,b,g,d) lepoll m \
-\ ==> (ALL b<a. f`b ~= 0 --> \
-\ (EX g<a. EX d<a. u(f,b,g,d) ~= 0 & u(f,b,g,d) lesspoll m)) \
-\ | (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 --> \
+ "\\<forall>b<a. \\<forall>g<a. \\<forall>d<a. u(f,b,g,d) lepoll m \
+\ ==> (\\<forall>b<a. f`b \\<noteq> 0 --> \
+\ (\\<exists>g<a. \\<exists>d<a. u(f,b,g,d) \\<noteq> 0 & u(f,b,g,d) lesspoll m)) \
+\ | (\\<exists>b<a. f`b \\<noteq> 0 & (\\<forall>g<a. \\<forall>d<a. u(f,b,g,d) \\<noteq> 0 --> \
\ u(f,b,g,d) eqpoll m))";
by (Asm_simp_tac 1);
by (blast_tac (claset() delrules [equalityI]) 1);
@@ -69,7 +69,7 @@
(* ********************************************************************** *)
(* Lemmas used in both cases *)
(* ********************************************************************** *)
-Goal "Ord(a) ==> (UN b<a++a. C(b)) = (UN b<a. C(b) Un C(a++b))";
+Goal "Ord(a) ==> (\\<Union>b<a++a. C(b)) = (\\<Union>b<a. C(b) Un C(a++b))";
by (fast_tac (claset() addSIs [equalityI] addIs [ltI]
addSDs [lt_oadd_disj]
addSEs [lt_oadd1, oadd_lt_mono2]) 1);
@@ -77,20 +77,20 @@
(* ********************************************************************** *)
-(* Case 1 : lemmas *)
+(* Case 1 \\<in> lemmas *)
(* ********************************************************************** *)
-Goalw [vv1_def] "vv1(f,m,b) <= f`b";
+Goalw [vv1_def] "vv1(f,m,b) \\<subseteq> f`b";
by (rtac (LetI RS LetI) 1);
by (simp_tac (simpset() addsimps [domain_uu_subset]) 1);
qed "vv1_subset";
(* ********************************************************************** *)
-(* Case 1 : Union of images is the whole "y" *)
+(* Case 1 \\<in> Union of images is the whole "y" *)
(* ********************************************************************** *)
Goalw [gg1_def]
- "!! a f y. [| Ord(a); m:nat |] ==> \
-\ (UN b<a++a. gg1(f,a,m)`b) = (UN b<a. f`b)";
+ "!! a f y. [| Ord(a); m \\<in> nat |] ==> \
+\ (\\<Union>b<a++a. gg1(f,a,m)`b) = (\\<Union>b<a. f`b)";
by (asm_simp_tac
(simpset() addsimps [UN_oadd, lt_oadd1,
oadd_le_self RS le_imp_not_lt, lt_Ord,
@@ -106,7 +106,7 @@
(* every value of defined function is less than or equipollent to m *)
(* ********************************************************************** *)
Goal "[| P(a, b); Ord(a); Ord(b); \
-\ Least_a = (LEAST a. EX x. Ord(x) & P(a, x)) |] \
+\ Least_a = (LEAST a. \\<exists>x. Ord(x) & P(a, x)) |] \
\ ==> P(Least_a, LEAST b. P(Least_a, b))";
by (etac ssubst 1);
by (res_inst_tac [("Q","%z. P(z, LEAST b. P(z, b))")] LeastI2 1);
@@ -115,24 +115,24 @@
bind_thm ("nested_Least_instance",
inst "P"
- "%g d. domain(uu(f,b,g,d)) ~= 0 & domain(uu(f,b,g,d)) lepoll m"
+ "%g d. domain(uu(f,b,g,d)) \\<noteq> 0 & domain(uu(f,b,g,d)) lepoll m"
nested_LeastI);
Goalw [gg1_def]
- "!!a. [| Ord(a); m:nat; \
-\ ALL b<a. f`b ~=0 --> \
-\ (EX g<a. EX d<a. domain(uu(f,b,g,d)) ~= 0 & \
+ "!!a. [| Ord(a); m \\<in> nat; \
+\ \\<forall>b<a. f`b \\<noteq>0 --> \
+\ (\\<exists>g<a. \\<exists>d<a. domain(uu(f,b,g,d)) \\<noteq> 0 & \
\ domain(uu(f,b,g,d)) lepoll m); \
-\ ALL b<a. f`b lepoll succ(m); b<a++a \
+\ \\<forall>b<a. f`b lepoll succ(m); b<a++a \
\ |] ==> gg1(f,a,m)`b lepoll m";
by (Asm_simp_tac 1);
by (safe_tac (claset() addSEs [lt_oadd_odiff_cases]));
-(*Case b<a : show vv1(f,m,b) lepoll m *)
+(*Case b<a \\<in> show vv1(f,m,b) lepoll m *)
by (asm_simp_tac (simpset() addsimps [vv1_def, Let_def]) 1);
by (fast_tac (claset() addIs [nested_Least_instance RS conjunct2]
addSEs [lt_Ord]
addSIs [empty_lepollI]) 1);
-(*Case a le b: show ww1(f,m,b--a) lepoll m *)
+(*Case a le b \\<in> show ww1(f,m,b--a) lepoll m *)
by (asm_simp_tac (simpset() addsimps [ww1_def]) 1);
by (excluded_middle_tac "f`(b--a) = 0" 1);
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
@@ -147,47 +147,47 @@
qed "gg1_lepoll_m";
(* ********************************************************************** *)
-(* Case 2 : lemmas *)
+(* Case 2 \\<in> lemmas *)
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* Case 2 : vv2_subset *)
+(* Case 2 \\<in> vv2_subset *)
(* ********************************************************************** *)
-Goalw [uu_def] "[| 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";
+Goalw [uu_def] "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
+\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y \
+\ |] ==> \\<exists>d<a. uu(f,b,g,d) \\<noteq> 0";
by (fast_tac (claset() addSIs [not_emptyI]
addSDs [SigmaI RSN (2, subsetD)]
addSEs [not_emptyE]) 1);
qed "ex_d_uu_not_empty";
-Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
-\ y*y<=y; (UN b<a. f`b)=y |] \
-\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) ~= 0)) ~= 0";
+Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
+\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \
+\ ==> uu(f,b,g,LEAST d. (uu(f,b,g,d) \\<noteq> 0)) \\<noteq> 0";
by (dtac ex_d_uu_not_empty 1 THEN REPEAT (assume_tac 1));
by (fast_tac (claset() addSEs [LeastI, lt_Ord]) 1);
qed "uu_not_empty";
-Goal "[| r<=A*B; r~=0 |] ==> domain(r)~=0";
+Goal "[| r \\<subseteq> A*B; r\\<noteq>0 |] ==> domain(r)\\<noteq>0";
by (Blast_tac 1);
qed "not_empty_rel_imp_domain";
-Goal "[| b<a; g<a; f`b~=0; f`g~=0; \
-\ y*y <= y; (UN b<a. f`b)=y |] \
-\ ==> (LEAST d. uu(f,b,g,d) ~= 0) < a";
+Goal "[| b<a; g<a; f`b\\<noteq>0; f`g\\<noteq>0; \
+\ y*y \\<subseteq> y; (\\<Union>b<a. f`b)=y |] \
+\ ==> (LEAST d. uu(f,b,g,d) \\<noteq> 0) < a";
by (eresolve_tac [ex_d_uu_not_empty RS oexE] 1
THEN REPEAT (assume_tac 1));
by (resolve_tac [Least_le RS lt_trans1] 1
THEN (REPEAT (ares_tac [lt_Ord] 1)));
qed "Least_uu_not_empty_lt_a";
-Goal "[| B<=A; a~:B |] ==> B <= A-{a}";
+Goal "[| B \\<subseteq> A; a\\<notin>B |] ==> B \\<subseteq> A-{a}";
by (Blast_tac 1);
qed "subset_Diff_sing";
(*Could this be proved more directly?*)
-Goal "[| A lepoll m; m lepoll B; B <= A; m:nat |] ==> A=B";
+Goal "[| A lepoll m; m lepoll B; B \\<subseteq> A; m \\<in> nat |] ==> A=B";
by (etac natE 1);
by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
by (safe_tac (claset() addSIs [equalityI]));
@@ -198,12 +198,12 @@
THEN REPEAT (assume_tac 1));
qed "supset_lepoll_imp_eq";
-Goal "[| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+Goal "[| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>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";
+\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
+\ (\\<Union>b<a. f`b)=y; b<a; g<a; d<a; \
+\ f`b\\<noteq>0; f`g\\<noteq>0; m \\<in> nat; s \\<in> f`b \
+\ |] ==> uu(f, b, g, LEAST d. uu(f,b,g,d)\\<noteq>0) \\<in> 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);
@@ -216,11 +216,11 @@
qed "uu_Least_is_fun";
Goalw [vv2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f, b, g, d))~=0 --> \
+ "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f, b, g, d))\\<noteq>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; m:nat; s:f`b \
-\ |] ==> vv2(f,b,g,s) <= f`g";
+\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
+\ (\\<Union>b<a. f`b)=y; b<a; g<a; m \\<in> nat; s \\<in> f`b \
+\ |] ==> vv2(f,b,g,s) \\<subseteq> f`g";
by (split_tac [split_if] 1);
by Safe_tac;
by (etac (uu_Least_is_fun RS apply_type) 1);
@@ -228,14 +228,14 @@
qed "vv2_subset";
(* ********************************************************************** *)
-(* Case 2 : Union of images is the whole "y" *)
+(* Case 2 \\<in> Union of images is the whole "y" *)
(* ********************************************************************** *)
Goalw [gg2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
+ "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 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; Ord(a); m:nat; s:f`b; b<a \
-\ |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
+\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
+\ (\\<Union>b<a. f`b)=y; Ord(a); m \\<in> nat; s \\<in> f`b; b<a \
+\ |] ==> (\\<Union>g<a++a. gg2(f,a,b,s) ` g) = y";
by (dtac sym 1);
by (asm_simp_tac
(simpset() addsimps [UN_oadd, lt_oadd1,
@@ -252,7 +252,7 @@
(* every value of defined function is less than or equipollent to m *)
(* ********************************************************************** *)
-Goalw [vv2_def] "[| m:nat; m~=0 |] ==> vv2(f,b,g,s) lepoll m";
+Goalw [vv2_def] "[| m \\<in> nat; m\\<noteq>0 |] ==> vv2(f,b,g,s) lepoll m";
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 1);
by (fast_tac (claset()
addSDs [le_imp_subset RS subset_imp_lepoll RS lepoll_0_is_0]
@@ -262,7 +262,7 @@
qed "vv2_lepoll";
Goalw [ww2_def]
- "[| ALL b<a. f`b lepoll succ(m); g<a; m:nat; vv2(f,b,g,d) <= f`g |] \
+ "[| \\<forall>b<a. f`b lepoll succ(m); g<a; m \\<in> nat; vv2(f,b,g,d) \\<subseteq> f`g |] \
\ ==> ww2(f,b,g,d) lepoll m";
by (excluded_middle_tac "f`g = 0" 1);
by (asm_simp_tac (simpset() addsimps [empty_lepollI]) 2);
@@ -272,10 +272,10 @@
qed "ww2_lepoll";
Goalw [gg2_def]
- "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 --> \
+ "!!a. [| \\<forall>g<a. \\<forall>d<a. domain(uu(f,b,g,d)) \\<noteq> 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; s:f`b; m:nat; m~= 0; g<a++a \
+\ \\<forall>b<a. f`b lepoll succ(m); y*y \\<subseteq> y; \
+\ (\\<Union>b<a. f`b)=y; b<a; s \\<in> f`b; m \\<in> nat; m\\<noteq> 0; g<a++a \
\ |] ==> gg2(f,a,b,s) ` g lepoll m";
by (Asm_simp_tac 1);
by (safe_tac (claset() addSEs [lt_oadd_odiff_cases, lt_Ord2]));
@@ -286,7 +286,7 @@
(* ********************************************************************** *)
(* lemma ii *)
(* ********************************************************************** *)
-Goalw [NN_def] "[| succ(m) : NN(y); y*y <= y; m:nat; m~=0 |] ==> m : NN(y)";
+Goalw [NN_def] "[| succ(m) \\<in> NN(y); y*y \\<subseteq> y; m \\<in> nat; m\\<noteq>0 |] ==> m \\<in> NN(y)";
by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1));
by (resolve_tac [quant_domain_uu_lepoll_m RS cases RS disjE] 1
THEN (assume_tac 1));
@@ -310,35 +310,35 @@
(* ********************************************************************** *)
-(* lemma iv - p. 4 : *)
-(* For every set x there is a set y such that x Un (y * y) <= y *)
+(* lemma iv - p. 4 \\<in> *)
+(* For every set x there is a set y such that x Un (y * y) \\<subseteq> y *)
(* ********************************************************************** *)
-(* the quantifier ALL looks inelegant but makes the proofs shorter *)
+(* the quantifier \\<forall>looks inelegant but makes the proofs shorter *)
(* (used only in the following two lemmas) *)
-Goal "ALL n:nat. rec(n, x, %k r. r Un r*r) <= \
+Goal "\\<forall>n \\<in> nat. rec(n, x, %k r. r Un r*r) \\<subseteq> \
\ rec(succ(n), x, %k r. r Un r*r)";
by (fast_tac (claset() addIs [rec_succ RS ssubst]) 1);
qed "z_n_subset_z_succ_n";
-Goal "[| ALL n:nat. f(n)<=f(succ(n)); n le m; n : nat; m: nat |] \
+Goal "[| \\<forall>n \\<in> nat. f(n)<=f(succ(n)); n le m; n \\<in> nat; m \\<in> nat |] \
\ ==> f(n)<=f(m)";
by (eres_inst_tac [("P","n le m")] rev_mp 1);
-by (res_inst_tac [("P","%z. n le z --> f(n) <= f(z)")] nat_induct 1);
+by (res_inst_tac [("P","%z. n le z --> f(n) \\<subseteq> f(z)")] nat_induct 1);
by (REPEAT (fast_tac le_cs 1));
qed "le_subsets";
-Goal "[| n le m; m:nat |] ==> \
-\ rec(n, x, %k r. r Un r*r) <= rec(m, x, %k r. r Un r*r)";
+Goal "[| n le m; m \\<in> nat |] ==> \
+\ rec(n, x, %k r. r Un r*r) \\<subseteq> rec(m, x, %k r. r Un r*r)";
by (resolve_tac [z_n_subset_z_succ_n RS le_subsets] 1
THEN (TRYALL assume_tac));
by (eresolve_tac [Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD] 1
THEN (assume_tac 1));
qed "le_imp_rec_subset";
-Goal "EX y. x Un y*y <= y";
-by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
+Goal "\\<exists>y. x Un y*y \\<subseteq> y";
+by (res_inst_tac [("x","\\<Union>n \\<in> nat. rec(n, x, %k r. r Un r*r)")] exI 1);
by Safe_tac;
by (rtac (nat_0I RS UN_I) 1);
by (Asm_simp_tac 1);
@@ -350,64 +350,64 @@
qed "lemma_iv";
(* ********************************************************************** *)
-(* Rubin & Rubin wrote : *)
-(* "It follows from (ii) and mathematical induction that if y*y <= y then *)
+(* Rubin & Rubin wrote \\<in> *)
+(* "It follows from (ii) and mathematical induction that if y*y \\<subseteq> y then *)
(* y can be well-ordered" *)
-(* In fact we have to prove : *)
-(* * WO6 ==> NN(y) ~= 0 *)
-(* * reverse induction which lets us infer that 1 : NN(y) *)
-(* * 1 : NN(y) ==> y can be well-ordered *)
+(* In fact we have to prove \\<in> *)
+(* * WO6 ==> NN(y) \\<noteq> 0 *)
+(* * reverse induction which lets us infer that 1 \\<in> NN(y) *)
+(* * 1 \\<in> NN(y) ==> y can be well-ordered *)
(* ********************************************************************** *)
(* ********************************************************************** *)
-(* WO6 ==> NN(y) ~= 0 *)
+(* WO6 ==> NN(y) \\<noteq> 0 *)
(* ********************************************************************** *)
-Goalw [WO6_def, NN_def] "WO6 ==> NN(y) ~= 0";
+Goalw [WO6_def, NN_def] "WO6 ==> NN(y) \\<noteq> 0";
by (fast_tac ZF_cs 1); (*SLOW if current claset is used*)
qed "WO6_imp_NN_not_empty";
(* ********************************************************************** *)
-(* 1 : NN(y) ==> y can be well-ordered *)
+(* 1 \\<in> NN(y) ==> y can be well-ordered *)
(* ********************************************************************** *)
-Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
-\ ==> EX c<a. f`c = {x}";
+Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \
+\ ==> \\<exists>c<a. f`c = {x}";
by (fast_tac (claset() addSEs [lepoll_1_is_sing]) 1);
val lemma1 = result();
-Goal "[| (UN b<a. f`b)=y; x:y; ALL b<a. f`b lepoll 1; Ord(a) |] \
+Goal "[| (\\<Union>b<a. f`b)=y; x \\<in> y; \\<forall>b<a. f`b lepoll 1; Ord(a) |] \
\ ==> f` (LEAST i. f`i = {x}) = {x}";
by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
by (fast_tac (claset() addSEs [lt_Ord] addIs [LeastI]) 1);
val lemma2 = result();
-Goalw [NN_def] "1 : NN(y) ==> EX a f. Ord(a) & f:inj(y, a)";
+Goalw [NN_def] "1 \\<in> NN(y) ==> \\<exists>a f. Ord(a) & f \\<in> inj(y, a)";
by (etac CollectE 1);
by (REPEAT (eresolve_tac [exE, conjE] 1));
by (res_inst_tac [("x","a")] exI 1);
-by (res_inst_tac [("x","lam x:y. LEAST i. f`i = {x}")] exI 1);
+by (res_inst_tac [("x","\\<lambda>x \\<in> y. LEAST i. f`i = {x}")] exI 1);
by (rtac conjI 1 THEN (assume_tac 1));
-by (res_inst_tac [("d","%i. THE x. x:f`i")] lam_injective 1);
+by (res_inst_tac [("d","%i. THE x. x \\<in> f`i")] lam_injective 1);
by (dtac lemma1 1 THEN REPEAT (assume_tac 1));
by (fast_tac (claset() addSEs [Least_le RS lt_trans1 RS ltD, lt_Ord]) 1);
by (resolve_tac [lemma2 RS ssubst] 1 THEN REPEAT (assume_tac 1));
by (Blast_tac 1);
qed "NN_imp_ex_inj";
-Goal "[| y*y <= y; 1 : NN(y) |] ==> EX r. well_ord(y, r)";
+Goal "[| y*y \\<subseteq> y; 1 \\<in> NN(y) |] ==> \\<exists>r. well_ord(y, r)";
by (dtac NN_imp_ex_inj 1);
by (fast_tac (claset() addSEs [well_ord_Memrel RSN (2, well_ord_rvimage)]) 1);
qed "y_well_ord";
(* ********************************************************************** *)
-(* reverse induction which lets us infer that 1 : NN(y) *)
+(* reverse induction which lets us infer that 1 \\<in> NN(y) *)
(* ********************************************************************** *)
val [prem1, prem2] = goal thy
- "[| n:nat; !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
-\ ==> n~=0 --> P(n) --> P(1)";
+ "[| n \\<in> nat; !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \
+\ ==> n\\<noteq>0 --> P(n) --> P(1)";
by (rtac (prem1 RS nat_induct) 1);
by (Blast_tac 1);
by (excluded_middle_tac "x=0" 1);
@@ -416,19 +416,19 @@
qed "rev_induct_lemma";
val prems =
-Goal "[| P(n); n:nat; n~=0; \
-\ !!m. [| m:nat; m~=0; P(succ(m)) |] ==> P(m) |] \
+Goal "[| P(n); n \\<in> nat; n\\<noteq>0; \
+\ !!m. [| m \\<in> nat; m\\<noteq>0; P(succ(m)) |] ==> P(m) |] \
\ ==> P(1)";
by (resolve_tac [rev_induct_lemma RS impE] 1);
by (etac impE 4 THEN (assume_tac 5));
by (REPEAT (ares_tac prems 1));
qed "rev_induct";
-Goalw [NN_def] "n:NN(y) ==> n:nat";
+Goalw [NN_def] "n \\<in> NN(y) ==> n \\<in> nat";
by (etac CollectD1 1);
qed "NN_into_nat";
-Goal "[| n:NN(y); y*y <= y; n~=0 |] ==> 1:NN(y)";
+Goal "[| n \\<in> NN(y); y*y \\<subseteq> y; n\\<noteq>0 |] ==> 1 \\<in> NN(y)";
by (rtac rev_induct 1 THEN REPEAT (ares_tac [NN_into_nat] 1));
by (rtac lemma_ii 1 THEN REPEAT (assume_tac 1));
val lemma3 = result();
@@ -438,7 +438,7 @@
(* ********************************************************************** *)
(* another helpful lemma *)
-Goalw [NN_def] "0:NN(y) ==> y=0";
+Goalw [NN_def] "0 \\<in> NN(y) ==> y=0";
by (fast_tac (claset() addSIs [equalityI]
addSDs [lepoll_0_is_0] addEs [subst]) 1);
qed "NN_y_0";
--- a/src/ZF/AC/WO6_WO1.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Mon May 21 14:45:52 2001 +0200
@@ -19,32 +19,32 @@
defs
- NN_def "NN(y) == {m:nat. EX a. EX f. Ord(a) & domain(f)=a &
- (UN b<a. f`b) = y & (ALL b<a. f`b lepoll m)}"
+ NN_def "NN(y) == {m \\<in> nat. \\<exists>a. \\<exists>f. Ord(a) & domain(f)=a &
+ (\\<Union>b<a. f`b) = y & (\\<forall>b<a. f`b lepoll m)}"
uu_def "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
(*Definitions for case 1*)
vv1_def "vv1(f,m,b) ==
- let g = LEAST g. (EX d. Ord(d) & (domain(uu(f,b,g,d)) ~= 0 &
+ let g = LEAST g. (\\<exists>d. Ord(d) & (domain(uu(f,b,g,d)) \\<noteq> 0 &
domain(uu(f,b,g,d)) lepoll m));
- d = LEAST d. domain(uu(f,b,g,d)) ~= 0 &
+ d = LEAST d. domain(uu(f,b,g,d)) \\<noteq> 0 &
domain(uu(f,b,g,d)) lepoll m
- in if f`b ~= 0 then domain(uu(f,b,g,d)) else 0"
+ in if f`b \\<noteq> 0 then domain(uu(f,b,g,d)) else 0"
ww1_def "ww1(f,m,b) == f`b - vv1(f,m,b)"
- gg1_def "gg1(f,a,m) == lam b:a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
+ gg1_def "gg1(f,a,m) == \\<lambda>b \\<in> a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
(*Definitions for case 2*)
vv2_def "vv2(f,b,g,s) ==
- if f`g ~= 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) ~= 0)`s} else 0"
+ if f`g \\<noteq> 0 then {uu(f, b, g, LEAST d. uu(f,b,g,d) \\<noteq> 0)`s} else 0"
ww2_def "ww2(f,b,g,s) == f`g - vv2(f,b,g,s)"
gg2_def "gg2(f,a,b,s) ==
- lam g:a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
+ \\<lambda>g \\<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
end
--- a/src/ZF/AC/WO_AC.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/WO_AC.ML Mon May 21 14:45:52 2001 +0200
@@ -5,18 +5,16 @@
Lemmas used in the proofs like WO? ==> AC?
*)
-open WO_AC;
-
-Goal "[| well_ord(Union(A),r); 0~:A; B:A |] \
-\ ==> (THE b. first(b,B,r)) : B";
+Goal "[| well_ord(Union(A),r); 0\\<notin>A; B \\<in> A |] \
+\ ==> (THE b. first(b,B,r)) \\<in> B";
by (fast_tac (claset() addSEs [well_ord_imp_ex1_first RS theI RS
(first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
qed "first_in_B";
-Goal "[| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)";
+Goal "[| well_ord(Union(A), R); 0\\<notin>A |] ==> \\<exists>f. f:(\\<Pi>X \\<in> A. X)";
by (fast_tac (claset() addSEs [first_in_B] addSIs [lam_type]) 1);
qed "ex_choice_fun";
-Goal "well_ord(A, R) ==> EX f. f:(PROD X: Pow(A)-{0}. X)";
+Goal "well_ord(A, R) ==> \\<exists>f. f:(\\<Pi>X \\<in> Pow(A)-{0}. X)";
by (fast_tac (claset() addSEs [well_ord_subset RS ex_choice_fun]) 1);
qed "ex_choice_fun_Pow";
--- a/src/ZF/AC/recfunAC16.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/recfunAC16.ML Mon May 21 14:45:52 2001 +0200
@@ -15,16 +15,16 @@
Goalw [recfunAC16_def]
"recfunAC16(f,fa,succ(i),a) = \
-\ (if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y) then recfunAC16(f,fa,i,a) \
+\ (if (\\<exists>y \\<in> recfunAC16(f,fa,i,a). fa ` i \\<subseteq> y) then recfunAC16(f,fa,i,a) \
\ else recfunAC16(f,fa,i,a) Un \
-\ {f ` (LEAST j. fa ` i <= f ` j & \
-\ (ALL b<a. (fa`b <= f`j \
-\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})";
+\ {f ` (LEAST j. fa ` i \\<subseteq> f ` j & \
+\ (\\<forall>b<a. (fa`b \\<subseteq> f`j \
+\ --> (\\<forall>t \\<in> recfunAC16(f,fa,i,a). ~ fa`b \\<subseteq> t))))})";
by (rtac transrec2_succ 1);
qed "recfunAC16_succ";
Goalw [recfunAC16_def] "Limit(i) \
-\ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))";
+\ ==> recfunAC16(f,fa,i,a) = (\\<Union>j<i. recfunAC16(f,fa,j,a))";
by (etac transrec2_Limit 1);
qed "recfunAC16_Limit";
@@ -33,8 +33,8 @@
(* ********************************************************************** *)
val [prem1, prem2] = goal thy
- "[| !!g r. r <= B(g,r); Ord(i) |] \
-\ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)";
+ "[| !!g r. r \\<subseteq> B(g,r); Ord(i) |] \
+\ ==> j<i --> transrec2(j, 0, B) \\<subseteq> transrec2(i, 0, B)";
by (resolve_tac [prem2 RS trans_induct] 1);
by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1)));
by (Fast_tac 1);
@@ -46,8 +46,8 @@
transrec2_Limit RS ssubst]) 1);
qed "transrec2_mono_lemma";
-val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \
-\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)";
+val [prem1, prem2] = goal thy "[| !!g r. r \\<subseteq> B(g,r); j le i |] \
+\ ==> transrec2(j, 0, B) \\<subseteq> transrec2(i, 0, B)";
by (resolve_tac [prem2 RS leE] 1);
by (resolve_tac [transrec2_mono_lemma RS impE] 1);
by (TRYALL (fast_tac (claset() addSIs [prem1, prem2, lt_Ord2])));
@@ -58,7 +58,7 @@
(* ********************************************************************** *)
Goalw [recfunAC16_def]
- "!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)";
+ "!!i. i le j ==> recfunAC16(f, g, i, a) \\<subseteq> recfunAC16(f, g, j, a)";
by (rtac transrec2_mono 1);
by (REPEAT (fast_tac (claset() addIs [split_if RS iffD2]) 1));
qed "recfunAC16_mono";
--- a/src/ZF/AC/recfunAC16.thy Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/recfunAC16.thy Mon May 21 14:45:52 2001 +0200
@@ -12,8 +12,8 @@
"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))))}))"
+ %g r. if(\\<exists>y \\<in> r. fa`g \\<subseteq> y, r,
+ r Un {f`(LEAST i. fa`g \\<subseteq> f`i &
+ (\\<forall>b<a. (fa`b \\<subseteq> f`i --> (\\<forall>t \\<in> r. ~ fa`b \\<subseteq> t))))}))"
end
--- a/src/ZF/AC/rel_is_fun.ML Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/rel_is_fun.ML Mon May 21 14:45:52 2001 +0200
@@ -10,10 +10,10 @@
(*Using AC we could trivially prove, for all u, domain(u) lepoll u*)
goalw Cardinal.thy [lepoll_def]
- "!!m. [| m:nat; u lepoll m |] ==> domain(u) lepoll m";
+ "!!m. [| m \\<in> nat; u lepoll m |] ==> domain(u) lepoll m";
by (etac exE 1);
by (res_inst_tac [("x",
- "lam x:domain(u). LEAST i. EX y. <x,y> : u & f`<x,y> = i")] exI 1);
+ "\\<lambda>x \\<in> domain(u). LEAST i. \\<exists>y. <x,y> \\<in> u & f`<x,y> = i")] exI 1);
by (res_inst_tac [("d","%y. fst(converse(f)`y)")] lam_injective 1);
by (fast_tac (claset() addIs [LeastI2, nat_into_Ord RS Ord_in_Ord,
inj_is_fun RS apply_type]) 1);
@@ -25,7 +25,7 @@
qed "lepoll_m_imp_domain_lepoll_m";
goalw Cardinal.thy [function_def]
- "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat |] ==> \
+ "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m \\<in> nat |] ==> \
\ function(r)";
by Safe_tac;
by (resolve_tac [excluded_middle RS disjE] 1 THEN (atac 2));
@@ -35,8 +35,8 @@
qed "rel_domain_ex1";
goal Cardinal.thy
- "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m:nat; \
-\ r<=A*B; A=domain(r) |] ==> r: A->B";
+ "!!r. [| succ(m) lepoll domain(r); r lepoll succ(m); m \\<in> nat; \
+\ r \\<subseteq> A*B; A=domain(r) |] ==> r \\<in> A->B";
by (hyp_subst_tac 1);
by (asm_simp_tac (simpset() addsimps [Pi_iff, rel_domain_ex1]) 1);
qed "rel_is_fun";