# HG changeset patch # User paulson # Date 990449152 -7200 # Node ID 7f9e4c3893181a89213d73d2ff73369c27344322 # Parent b4e71bd751e4ddd90d0ccc02daa9f7f4a4ecdd7e X-symbols for set theory diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC0_AC1.ML --- 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\\A ==> A \\ 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:(\\X \\ A. X); D \\ A |] ==> \\g. g:(\\X \\ D. X)"; by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1); val lemma1 = result(); diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC10_AC15.ML --- 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\\0 ==> B lepoll A*B"; by (etac not_emptyE 1); -by (res_inst_tac [("x","lam z:B. ")] exI 1); +by (res_inst_tac [("x","\\z \\ B. ")] 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\\A ==> \\B \\ {cons(0,x*nat). x \\ 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 \\ A |] ==> \\B \\ C. a \\ B & B \\ 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 \\ A; C \\ A; a \\ B; a \\ 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) & \ + "\\B \\ {cons(0, x*nat). x \\ A}. pairwise_disjoint(f`B) & \ \ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ -\ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ -\ 0:u & 2 lepoll u & u lepoll n"; +\ ==> \\B \\ A. \\! u. u \\ f`cons(0, B*nat) & u \\ cons(0, B*nat) & \ +\ 0 \\ 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 \\ 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", "\\x \\ RepFun(A, P). LEAST j. \\a \\ 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 \\ nat; B \\ A; u(B) \\ cons(0, B*nat); 0 \\ u(B); 2 lepoll u(B); \ \ u(B) lepoll succ(n) |] \ -\ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \ -\ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \ -\ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n"; +\ ==> (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ 0 & \ +\ (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ B & \ +\ (\\x \\ A. {fst(x). x \\ 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 "[| \\f. \\B \\ {cons(0, x*nat). x \\ A}. \ \ pairwise_disjoint(f`B) & \ \ sets_of_size_between(f`B, 2, succ(n)) & \ -\ Union(f`B)=B; n:nat |] \ -\ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n"; +\ Union(f`B)=B; n \\ nat |] \ +\ ==> \\f. \\B \\ A. f`B \\ 0 & f`B \\ 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 \\ 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 \\ *) (* 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 \\ 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","\\x \\ 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 \\ 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 \\ n *) (* ********************************************************************** *) -Goalw AC_defs "[| n:nat; 1 le n; AC13(n) |] ==> AC14"; +Goalw AC_defs "[| n \\ 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\\0; A lepoll 1 |] ==> \\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 "\\B \\ A. f(B)\\0 & f(B)<=B & f(B) lepoll 1 \ +\ ==> (\\x \\ A. THE y. f(x)={y}) \\ (\\X \\ A. X)"; by (rtac lam_type 1); by (dtac bspec 1 THEN (assume_tac 1)); by (REPEAT (etac conjE 1)); diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC15_WO6.ML --- 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 (\\aa \\ 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 ix \\ Pow(A)-{0}. f`x\\0 & f`x \\ x & f`x lepoll m ==> \ +\ (\\i \ -\ ALL xx \\ Pow(A)-{0}. f`x\\0 & f`x \\ x & f`x lepoll m ==> \ +\ \\xj \\ (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); diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC16_WO4.ML --- 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 \ -\ EX a f. Ord(a) & domain(f) = a & \ -\ (UN b nat |] ==> \ +\ \\a f. Ord(a) & domain(f) = a & \ +\ (\\bbi \\ 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 \\ 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 "\\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); 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 \\ s(u) such that k lepoll x Int y (in our case succ(k)) *) +(* The idea of the proof is the following \\ *) (* 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 \\ 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} *) (* 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 \\ s(u). a \\ v} is less than or equipollent *) +(* to {v \\ 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 "[| ~(\\x \\ A. f`x=y); f \\ inj(A, B); y \\ B |] \ +\ ==> (\\a \\ succ(A). if(a=A, y, f`a)) \\ 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 \\ nat; nat lepoll X |] ==> \\Y. Y \\ 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 \\ 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 \\ y; b \\ y-a; u \\ x |] ==> cons(b, cons(u, a)) \\ 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 \\ y; b \\ y-a; u \\ 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 \\ A; a \\ A-B; k \\ 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\\ 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 \\ nat; m \\ nat |] ==> \ +\ \\A B. A eqpoll k #+ m & k lepoll B & B \\ 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 \\ A; succ(k) lepoll B; k \\ nat; m \\ 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 \\ nat; m \\ nat |] ==> \ +\ \\A B. A eqpoll k #+ m & k eqpoll B & B \\ 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 \\ A; succ(k) eqpoll B; k \\ nat; m \\ 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 \\ 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 \\ nat ==> {z \\ Pow(y). z lepoll succ(n)} = \ +\ {z \\ Pow(y). z lepoll n} Un {z \\ 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 \\ nat ==> {z \\ Pow(y). z lepoll n} Int {z \\ 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 \\ 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 \\ s(u). a \\ 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 \\ 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) \\ 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 \\ t_n; cons(b,cons(u,a)) \\ w; a \\ y; b \\ y-a; l eqpoll a \ +\ |] ==> w \\ 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 \\ s(u) ==> u \\ 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 \\ y; b \\ y - a; u \\ x |] \ +\ ==> \\! c. c \\ s(u) & a \\ c & b \\ 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 "[| \\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) \ \ 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 "[| \\v \\ s(u). succ(l) eqpoll v Int y; \ +\ l eqpoll a; a \\ y; u \\ x |] \ +\ ==> y lepoll {v \\ s(u). a \\ 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", "\\b \\ y-a. THE c. c \\ s(u) & a \\ c & b \\ 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 \\ 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 \\ {v \\ s(u). a \\ v}; \ +\ l eqpoll a; u \\ x; \ +\ \\v \\ 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 \\ s(u). a \\ v} is less than or equipollent *) +(* to {v \\ Pow(x). v eqpoll n-k} *) (* ********************************************************************** *) -Goal "x eqpoll m ==> x ~= 0"; +Goal "x eqpoll m ==> x \\ 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 \\ xa Int (x - {u}); l eqpoll a; a \\ y; u \\ x |] \ +\ ==> \\! w. w \\ t_n & cons(z, cons(u, a)) \\ 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 "[| \\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","\\w \\ {v \\ s(u). a \\ 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 \\ nat ==> \\S. well_ord({z \\ 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 \\ nat ==> \\R. well_ord({z \\ 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 \\ {z \\ 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 "\\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 \\ LL ==> \\! w. w \\ MM & v \\ 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 \\ MM ==> w Int y \\ LL"; by (Fast_tac 1); qed "Int_in_LL"; Goalw [LL_def] - "v : LL ==> v = (THE x. x : MM & v <= x) Int y"; + "v \\ LL ==> v = (THE x. x \\ MM & v \\ 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 \\ LL ==> (THE x. x \\ MM & v \\ x) \\ 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 \\ LL ==> GG ` v \\ 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 \\ nat ==> \\z. z \\ 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 \\ x ==> \\v \\ 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 "\\v \\ 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 \\ x ==> \\w \\ MM. u \\ 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 \\ x ==> \\w \\ LL. u \\ 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 bb w eqpoll succ(k #+ m)"; +Goalw [MM_def] "w \\ 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 \\ 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 bba f. Ord(a) & domain(f) = a & \ +\ (\\bbb \\ 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 \\ nat; m \\ nat |] ==> WO4(m)"; by (rtac allI 1); by (case_tac "Finite(A)" 1); by (rtac lemma1 1 THEN REPEAT (assume_tac 1)); diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC16_WO4.thy --- 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 "\\z \\ {z \\ Pow(x Un y) . z eqpoll succ(k)}. + \\! w. w \\ t_n & z \\ w " disjoint "x Int y = 0" - includes "t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}" + includes "t_n \\ {v \\ Pow(x Un y). v eqpoll succ(k #+ m)}" WO_R "well_ord(y,R)" - lnat "l:nat" - mnat "m:nat" + lnat "l \\ nat" + mnat "m \\ nat" mpos "0 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 \\ t_n. succ(k) lepoll v Int y}" + LL_def "LL == {v Int y. v \\ MM}" + GG_def "GG == \\v \\ LL. (THE w. w \\ MM & v \\ w) - v" + s_def "s(u) == {v \\ t_n. u \\ v & k lepoll v Int y}" end diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC16_lemmas.ML --- 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\\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 <-> (\\x. x \\ 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","\\a \\ 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 <-> (\\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\\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 \\ Pow(X). Y eqpoll 1} = {{x}. x \\ 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 \\ X}"; +by (res_inst_tac [("x","\\x \\ 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 \\ 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 \\ Pow(x); y eqpoll succ(z) |] \ +\ ==> (LEAST i. i \\ y) \\ 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))}. \ -\ ")] exI 1); +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","\\y \\ {y \\ Pow(x). y eqpoll succ(succ(n))}. \ +\ y, y-{LEAST i. i \\ 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 \\ z ==> Ord(y)) ==> z \\ 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","\\y \\ z. y \\ 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 \\ i ==> i \\ 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 \\ z ==> Ord(y)) ==> succ(Union(z)) \\ 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 \\ 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 \\ nat ==> \ +\ \\z. (\\y \\ z. Ord(y)) & z eqpoll n & z\\0 --> Union(z) \\ 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 "[| \\x \\ z. Ord(x); z eqpoll n; z\\0; n \\ nat |] \ +\ ==> Union(z) \\ 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 \\ Pow(x); z eqpoll n; n \\ nat |] \ +\ ==> succ(Union(z)) \\ 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 \\ nat |] ==> \ +\ {y \\ Pow(x). y eqpoll succ(n)} lepoll \ +\ {y \\ Pow(x). y eqpoll succ(succ(n))}"; +by (res_inst_tac [("x","\\z \\ {y \\ 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 \\ nat |] \ +\ ==> {Y \\ 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 \\ surj(A,B); y \\ 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 \\ inj(A,B); y \\ 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 \\ Pow(A). Y eqpoll n} eqpoll {Y \\ 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","\\X \\ {Y \\ Pow(A). \\f. f \\ 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 ==> \\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 \\ nat; ~Finite(X) |] \ +\ ==> {Y \\ 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) ==> \\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 \\ nat; ~Finite(X) |] \ +\ ==> {Y \\ 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)); diff -r b4e71bd751e4 -r 7f9e4c389318 src/ZF/AC/AC17_AC1.ML --- 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 - (\\j \\ LEAST i. HH(\\X \\ Pow(x)-{0}. {f`X}, x, i) = {x}. \ +\ HH(\\X \\ Pow(x)-{0}. {f`X}, x, j)) = 0; \ +\ f \\ Pow(x)-{0} -> x |] \ +\ ==> \\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"; +\ \\A. \\f \\ Pow(A)-{0} -> A. \\u \\ Pow(A)-{0}. f`u \\ 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 "[| \\f \\ Pow(x) - {0} -> x. \\u \\ Pow(x) - {0}. f`u\\u; \ +\ \\f \\ Pow(x)-{0}->x. \ +\ x - (\\a \\ (LEAST i. HH(\\X \\ Pow(x)-{0}. {f`X},x,i)={x}). \ +\ HH(\\X \\