# HG changeset patch # User lcp # Date 806686313 -7200 # Node ID d43c1f7a53febca20f47c73ec740e4613ef762b4 # Parent 686e3eb613b9ad677c6ad1709ad3b41c075ff0b4 Numerous small improvements by KG and LCP diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC0_AC1.ML --- a/src/ZF/AC/AC0_AC1.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC0_AC1.ML Tue Jul 25 17:31:53 1995 +0200 @@ -14,10 +14,10 @@ by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1); val lemma1 = result(); -val prems = goalw thy AC_defs "!!Z. AC0 ==> AC1"; +goalw thy AC_defs "!!Z. AC0 ==> AC1"; by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); -result(); +qed "AC0_AC1"; -val prems = goalw thy AC_defs "!!Z. AC1 ==> AC0"; +goalw thy AC_defs "!!Z. AC1 ==> AC0"; by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); -result(); +qed "AC1_AC0"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC10_AC15.ML --- a/src/ZF/AC/AC10_AC15.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC10_AC15.ML Tue Jul 25 17:31:53 1995 +0200 @@ -13,10 +13,10 @@ or -AC1 ==> AC13(1); AC13(m) ==> AC13(n); AC13(n) ==> AC14 ==> AC15 +AC1 ==> AC13(1); AC13(m) ==> AC13(n) ==> AC14 ==> AC15 (m le n) -So we don't have to prove all impllications of both cases. -Moreover we don't need to prove that AC13(1) ==> AC1, AC11 ==> AC14 as +So we don't have to prove all implications of both cases. +Moreover we don't need to prove AC13(1) ==> AC1 and AC11 ==> AC14 as Rubin & Rubin do. *) @@ -27,22 +27,6 @@ (* - ex_fun_AC13_AC15 *) (* ********************************************************************** *) -(* Change to ZF/Cardinal.ML *) - -goalw Cardinal.thy [succ_def] - "!!A. succ(n) lepoll A ==> n lepoll A - {a}"; -by (rtac cons_lepoll_consD 1); -by (rtac mem_not_refl 2); -by (fast_tac AC_cs 2); -by (fast_tac (AC_cs addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); -val lepoll_diff_sing = result(); -(* qed "lepoll_diff_sing"; *) - -goalw thy [Finite_def] "~Finite(nat)"; -by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll] - addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); -val nat_not_Finite = result(); - goalw thy [lepoll_def] "!!A. A~=0 ==> B lepoll A*B"; by (eresolve_tac [not_emptyE] 1); by (res_inst_tac [("x","lam z:B. ")] exI 1); @@ -56,7 +40,7 @@ by (resolve_tac [notI] 1); by (dresolve_tac [subset_consI RS subset_imp_lepoll RS lepoll_Finite] 1); by (resolve_tac [lepoll_Sigma RS lepoll_Finite RS (nat_not_Finite RS notE)] 1 - THEN (atac 2)); + THEN (assume_tac 2)); by (fast_tac AC_cs 1); val cons_times_nat_not_Finite = result(); @@ -66,7 +50,7 @@ goalw thy [pairwise_disjoint_def] "!!A. [| pairwise_disjoint(A); B:A; C:A; a:B; a:C |] ==> B=C"; -by (dresolve_tac [IntI] 1 THEN (atac 1)); +by (dresolve_tac [IntI] 1 THEN (assume_tac 1)); by (dres_inst_tac [("A","B Int C")] not_emptyI 1); by (fast_tac ZF_cs 1); val lemma2 = result(); @@ -85,7 +69,7 @@ by (resolve_tac [ex1I] 1); by (fast_tac ZF_cs 1); by (REPEAT (eresolve_tac [conjE] 1)); -by (resolve_tac [lemma2] 1 THEN (REPEAT (atac 1))); +by (resolve_tac [lemma2] 1 THEN (REPEAT (assume_tac 1))); val lemma3 = result(); goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i"; @@ -94,7 +78,7 @@ [("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1); by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); by (eresolve_tac [RepFunE] 1); -by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1)); +by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addIs [LeastI2] addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); by (eresolve_tac [RepFunE] 1); @@ -112,7 +96,7 @@ by (asm_simp_tac AC_ss 1); by (resolve_tac [conjI] 1); by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] - addDs [lepoll_diff_sing] + addDs [lepoll_Diff_sing] addEs [lepoll_trans RS succ_lepoll_natE, ssubst] addSIs [notI, lepoll_refl, nat_0I]) 1); by (resolve_tac [conjI] 1); @@ -126,10 +110,8 @@ \ 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"; -by (etac exE 1); -by (dtac lemma3 1); -by (fast_tac (empty_cs addSDs [bspec, theI] - addSEs [conjE] +by (fast_tac (empty_cs addSDs [lemma3, bspec, theI] + addSEs [exE, conjE] addSIs [exI, ballI, lemma5]) 1); val ex_fun_AC13_AC15 = result(); @@ -144,7 +126,7 @@ goalw thy AC_defs "!!Z. [| n:nat; 1 le n; AC10(n) |] ==> AC11"; by (resolve_tac [bexI] 1 THEN (assume_tac 2)); by (fast_tac ZF_cs 1); -result(); +qed "AC10_AC11"; (* ********************************************************************** *) (* AC11 ==> AC12 *) @@ -152,7 +134,7 @@ goalw thy AC_defs "!! Z. AC11 ==> AC12"; by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1); -result(); +qed "AC11_AC12"; (* ********************************************************************** *) (* AC12 ==> AC15 *) @@ -164,7 +146,7 @@ by (eresolve_tac [impE] 1); by (eresolve_tac [cons_times_nat_not_Finite] 1); by (fast_tac (ZF_cs addSIs [ex_fun_AC13_AC15]) 1); -result(); +qed "AC12_AC15"; (* ********************************************************************** *) (* AC15 ==> WO6 *) @@ -209,16 +191,16 @@ [singleton_eqpoll_1 RS eqpoll_imp_lepoll, singletonI RS not_emptyI]) 1); by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1); -result(); +qed "AC1_AC13"; (* ********************************************************************** *) (* AC13(m) ==> AC13(n) for m <= n *) (* ********************************************************************** *) goalw thy AC_defs "!!m n. [| m:nat; n:nat; m le n; AC13(m) |] ==> AC13(n)"; -by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (atac 1)); +by (dresolve_tac [nat_le_imp_lepoll] 1 THEN REPEAT (assume_tac 1)); by (fast_tac (ZF_cs addSEs [lepoll_trans]) 1); -result(); +qed "AC13_mono"; (* ********************************************************************** *) (* The proofs necessary for both cases *) @@ -230,7 +212,7 @@ goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC13(n) |] ==> AC14"; by (fast_tac (FOL_cs addIs [bexI]) 1); -result(); +qed "AC13_AC14"; (* ********************************************************************** *) (* AC14 ==> AC15 *) @@ -238,7 +220,7 @@ goalw thy AC_defs "!!Z. AC14 ==> AC15"; by (fast_tac ZF_cs 1); -result(); +qed "AC14_AC15"; (* ********************************************************************** *) (* The redundant proofs; however cited by Rubin & Rubin *) @@ -255,16 +237,16 @@ goal thy "!!f. 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)"; by (resolve_tac [lam_type] 1); -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [conjE] 1)); -by (eresolve_tac [lemma_aux RS exE] 1 THEN (atac 1)); +by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1)); by (asm_full_simp_tac (AC_ss addsimps [the_element]) 1); by (fast_tac (AC_cs addEs [ssubst]) 1); val lemma = result(); goalw thy AC_defs "!!Z. AC13(1) ==> AC1"; by (fast_tac (AC_cs addSEs [lemma]) 1); -result(); +qed "AC13(1)_AC1"; (* ********************************************************************** *) (* AC11 ==> AC14 *) @@ -272,4 +254,4 @@ goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1); -result(); +qed "AC11_AC14"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC15_WO6.ML --- a/src/ZF/AC/AC15_WO6.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC15_WO6.ML Tue Jul 25 17:31:53 1995 +0200 @@ -43,4 +43,4 @@ by (asm_full_simp_tac AC_ss 1); by (fast_tac (AC_cs addSIs [Ord_Least, lam_type RS domain_of_fun] addSEs [less_Least_subset_x, lemma1, lemma2]) 1); -result(); \ No newline at end of file +qed "AC15_WO6"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC16_WO4.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC16_WO4.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,697 @@ + +open AC16_WO4; + +(* ********************************************************************** *) +(* The case of finite set *) +(* ********************************************************************** *) + +goalw thy [Finite_def] "!!A. [| Finite(A); 0 \ +\ EX a f. Ord(a) & domain(f) = a & \ +\ (UN b well_ord({{y,z}. y:x},?s(x,z))"; +by (eresolve_tac [paired_bij RS bij_is_inj RS well_ord_rvimage] 1); +val well_ord_paired = uresult(); + +goal thy "!!A. [| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; +by (fast_tac (FOL_cs addEs [notE, lepoll_trans]) 1); +val lepoll_trans1 = result(); + +goalw thy [lepoll_def] + "!!X.[| Y lepoll X; well_ord(X, R) |] ==> EX S. well_ord(Y, S)"; +by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); +val well_ord_lepoll = result(); + +goal thy "!!X. [| well_ord(X,R); well_ord(Y,S) \ +\ |] ==> EX T. well_ord(X Un Y, T)"; +by (eresolve_tac [well_ord_radd RS (Un_lepoll_sum RS well_ord_lepoll)] 1); +by (assume_tac 1); +val well_ord_Un = result(); + +(* ********************************************************************** *) +(* There exists a well ordered set y such that ... *) +(* ********************************************************************** *) + +goal thy "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); +by (resolve_tac [Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS + well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); +by (fast_tac (AC_cs addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, + equals0I, HartogI RSN (2, lepoll_trans1), + subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS + eqpoll_imp_lepoll RSN (2, lepoll_trans))] + addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym] + addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, + paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll + RS lepoll_Finite]) 1); +val lemma2 = result(); + +val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; +by (fast_tac (AC_cs + addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); +val infinite_Un = result(); + +(* ********************************************************************** *) +(* 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} *) +(* 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} *) +(* ********************************************************************** *) + +goal thy "!!A. [| ~(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)"; +by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] + addIs [expand_if RS iffD2]) 1); +by (REPEAT (split_tac [expand_if] 1)); +by (fast_tac (AC_cs addSEs [left_inverse]) 1); +val succ_not_lepoll_lemma = result(); + +goalw thy [lepoll_def, eqpoll_def, bij_def, surj_def] + "!!A. [| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; +by (fast_tac (AC_cs addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); +val succ_not_lepoll_imp_eqpoll = result(); + +val [prem] = goalw thy [s_u_def] + "(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False) \ +\ ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; +by (excluded_middle_tac "?P" 1 THEN (assume_tac 2)); +by (resolve_tac [prem RS FalseE] 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [CollectE] 1); +by (eresolve_tac [conjE] 1); +by (eresolve_tac [swap] 1); +by (fast_tac (AC_cs addSEs [succ_not_lepoll_imp_eqpoll]) 1); +val suppose_not = result(); + +(* ********************************************************************** *) +(* There is a k-2 element subset of y *) +(* ********************************************************************** *) + +goalw thy [lepoll_def, eqpoll_def] + "!!X. [| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; +by (fast_tac (FOL_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] + addSIs [subset_refl] + addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); +val nat_lepoll_imp_ex_eqpoll_n = result(); + +val ordertype_eqpoll = + ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); + +goal thy "!!y. [| well_ord(y,R); ~Finite(y); n:nat \ +\ |] ==> EX z. z<=y & n eqpoll z"; +by (eresolve_tac [nat_lepoll_imp_ex_eqpoll_n] 1); +by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll + RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSIs [nat_le_infinite_Ord RS le_imp_lepoll] + addSEs [Ord_ordertype, ordertype_eqpoll RS eqpoll_imp_lepoll + RS lepoll_infinite]) 1); +val ex_subset_eqpoll_n = result(); + +goalw thy [lesspoll_def] "!!n. n: nat ==> n lesspoll nat"; +by (fast_tac (AC_cs 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); +val n_lesspoll_nat = result(); + +goal thy "!!y. [| well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; k: nat |] \ +\ ==> y - a eqpoll y"; +by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] + addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, + Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord + RS le_imp_lepoll] + addSEs [well_ord_cardinal_eqpoll, + well_ord_cardinal_eqpoll RS eqpoll_sym, + eqpoll_sym RS eqpoll_imp_lepoll, + n_lesspoll_nat RS lesspoll_lepoll_lesspoll, + well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll + RS lepoll_infinite]) 1); +val Diff_Finite_eqpoll = result(); + +goal thy "!!x. [| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)"; +by (fast_tac AC_cs 1); +val cons_cons_subset = result(); + +goal thy "!!x. [| 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 (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D]) 1); +val cons_cons_eqpoll = result(); + +goalw thy [s_u_def] "s_u(u, t_n, k, y) <= t_n"; +by (fast_tac AC_cs 1); +val s_u_subset = result(); + +goalw thy [s_u_def, succ_def] + "!!w. [| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a \ +\ |] ==> w: s_u(u, t_n, succ(k), y)"; +by (fast_tac (AC_cs addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] + addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); +val s_uI = result(); + +goalw thy [s_u_def] "!!v. v : s_u(u, t_n, k, y) ==> u : v"; +by (fast_tac AC_cs 1); +val in_s_u_imp_u_in = result(); + +goal thy + "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ +\ EX! w. w:t_n & z <= w; \ +\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0 |] \ +\ ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c"; +by (eresolve_tac [ballE] 1); +by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset, + eqpoll_sym RS cons_cons_eqpoll]) 2); +by (eresolve_tac [ex1E] 1); +by (res_inst_tac [("a","w")] ex1I 1); +by (resolve_tac [conjI] 1); +by (resolve_tac [CollectI] 1); +by (fast_tac (FOL_cs addSEs [s_uI]) 1); +by (fast_tac AC_cs 1); +by (fast_tac AC_cs 1); +by (eresolve_tac [allE] 1); +by (eresolve_tac [impE] 1); +by (assume_tac 2); +by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); +val ex1_superset_a = result(); + +goal thy + "!!A. [| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \ +\ |] ==> A = cons(a, B)"; +by (resolve_tac [equalityI] 1); +by (fast_tac AC_cs 2); +by (resolve_tac [Diff_eq_0_iff RS iffD1] 1); +by (resolve_tac [equals0I] 1); +by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); +by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); +by (fast_tac AC_cs 1); +by (dresolve_tac [cons_eqpoll_succ] 1); +by (fast_tac AC_cs 1); +by (fast_tac (AC_cs addSIs [nat_succI] + addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS + (lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); +val set_eq_cons = result(); + +goal thy + "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ +\ EX! w. w:t_n & z <= w; \ +\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ +\ k eqpoll a; a <= y; b : y - a; u : x; x Int y = 0; k:nat \ +\ |] ==> (THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c) \ +\ Int y = cons(b, a)"; +by (dresolve_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1)); +by (resolve_tac [set_eq_cons] 1); +by (REPEAT (fast_tac AC_cs 1)); +val the_eq_cons = result(); + +goal thy "!!a. [| cons(x,a) = cons(y,a); x~: a |] ==> x = y "; +by (fast_tac (AC_cs addSEs [equalityE]) 1); +val cons_eqE = result(); + +goal thy "!!A. A = B ==> A Int C = B Int C"; +by (asm_simp_tac AC_ss 1); +val eq_imp_Int_eq = result(); + +goal thy "!!a. [| a=b; a=c; b=d |] ==> c=d"; +by (asm_full_simp_tac AC_ss 1); +val msubst = result(); + +(* ********************************************************************** *) +(* 1. y is less than or equipollent to {v:s_u. a <= v} *) +(* where a is certain k-2 element subset of y *) +(* ********************************************************************** *) + +goal thy + "!!y. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(k))}. \ +\ EX! w. w:t_n & z <= w; \ +\ ALL v:s_u(u, t_n, succ(k), y). succ(k) eqpoll v Int y; \ +\ well_ord(y,R); ~Finite(y); k eqpoll a; a <= y; \ +\ k:nat; u:x; x Int y = 0 |] \ +\ ==> y lepoll {v:s_u(u, t_n, succ(k), y). a <= v}"; +by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS + eqpoll_imp_lepoll RS lepoll_trans] 1 + THEN REPEAT (assume_tac 1)); +by (res_inst_tac [("f3","lam b:y-a. \ +\ THE c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c")] + (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); +by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); +by (resolve_tac [CollectI] 1); +by (resolve_tac [lam_type] 1); +by (resolve_tac [ex1_superset_a RS theI RS conjunct1] 1 + THEN REPEAT (assume_tac 1)); +by (resolve_tac [ballI] 1); +by (resolve_tac [ballI] 1); +by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); +by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); +by (resolve_tac [impI] 1); +by (resolve_tac [cons_eqE] 1); +by (fast_tac AC_cs 2); +by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); +by (eresolve_tac [[asm_rl, the_eq_cons, the_eq_cons] MRS msubst] 1 + THEN REPEAT (assume_tac 1)); +val y_lepoll_subset_s_u = result(); + +(* ********************************************************************** *) +(* some arithmetic *) +(* ********************************************************************** *) + +goal thy + "!!k. [| k:nat; m:nat |] ==> \ +\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; +by (eres_inst_tac [("n","k")] nat_induct 1); +by (simp_tac (AC_ss addsimps [add_0]) 1); +by (fast_tac (AC_cs addIs [eqpoll_imp_lepoll RS + (Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); +by (REPEAT (resolve_tac [allI,impI] 1)); +by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); +by (fast_tac AC_cs 1); +by (eres_inst_tac [("x","A - {xa}")] allE 1); +by (eres_inst_tac [("x","B - {xa}")] allE 1); +by (eresolve_tac [impE] 1); +by (asm_full_simp_tac (AC_ss addsimps [add_succ]) 1); +by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); +by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val eqpoll_sum_imp_Diff_lepoll_lemma = result(); + +goal thy "!!k. [| 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 + THEN (REPEAT (assume_tac 1))); +by (fast_tac AC_cs 1); +val eqpoll_sum_imp_Diff_lepoll = result(); + +(* ********************************************************************** *) +(* similar properties for eqpoll *) +(* ********************************************************************** *) + +goal thy + "!!k. [| k:nat; m:nat |] ==> \ +\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; +by (eres_inst_tac [("n","k")] nat_induct 1); +by (fast_tac (AC_cs addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] + addss (AC_ss addsimps [add_0])) 1); +by (REPEAT (resolve_tac [allI,impI] 1)); +by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); +by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1); +by (eres_inst_tac [("x","A - {xa}")] allE 1); +by (eres_inst_tac [("x","B - {xa}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll, + eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] + addss (AC_ss addsimps [add_succ])) 1); +by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val eqpoll_sum_imp_Diff_eqpoll_lemma = result(); + +goal thy "!!k. [| 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 + THEN (REPEAT (assume_tac 1))); +by (fast_tac AC_cs 1); +val eqpoll_sum_imp_Diff_eqpoll = result(); + +(* ********************************************************************** *) +(* back to the second part *) +(* ********************************************************************** *) + +goal thy "!!w. [| x Int y = 0; w <= x Un y |] \ +\ ==> w Int (x - {u}) = w - cons(u, w Int y)"; +by (fast_tac (AC_cs addSIs [equalityI] addEs [equals0D]) 1); +val w_Int_eq_w_Diff = result(); + +goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v}; \ +\ l eqpoll a; t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ +\ m:nat; l:nat; x Int y = 0; u : x; \ +\ ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y \ +\ |] ==> w Int (x - {u}) eqpoll m"; +by (eresolve_tac [CollectE] 1); +by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSDs [s_u_subset RS subsetD]) 1); +by (fast_tac (AC_cs addEs [equals0D] addSDs [bspec] + addDs [s_u_subset RS subsetD] + addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in] + addSIs [nat_succI, eqpoll_sum_imp_Diff_eqpoll]) 1); +val w_Int_eqpoll_m = result(); + +goal thy "!!m. [| 0 x ~= 0"; +by (fast_tac (empty_cs + addSEs [mem_irrefl, ltE, eqpoll_succ_imp_not_empty, natE]) 1); +val eqpoll_m_not_empty = result(); + +goal thy + "!!z. [| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x \ +\ |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}"; +by (fast_tac (AC_cs addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1); +val cons_cons_in = result(); + +(* ********************************************************************** *) +(* 2. {v:s_u. a <= v} is less than or equipollent *) +(* to {v:Pow(x). v eqpoll n-k} *) +(* ********************************************************************** *) + +goal thy + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(succ(l))}. \ +\ EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(succ(l) #+ m)}; \ +\ 0 {v:s_u(u, t_n, succ(l), y). a <= v} \ +\ lepoll {v:Pow(x). v eqpoll m}"; +by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}. \ +\ w Int (x - {u})")] + (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); +by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); +by (resolve_tac [CollectI] 1); +by (resolve_tac [lam_type] 1); +by (resolve_tac [CollectI] 1); +by (fast_tac AC_cs 1); +by (resolve_tac [w_Int_eqpoll_m] 1 THEN REPEAT (assume_tac 1)); +by (simp_tac AC_ss 1); +by (REPEAT (resolve_tac [ballI, impI] 1)); +by (eresolve_tac [w_Int_eqpoll_m RSN (2, eqpoll_m_not_empty) RS not_emptyE] 1 + THEN REPEAT (assume_tac 1)); +by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); +by (dresolve_tac [cons_cons_in RSN (2, bspec)] 1 THEN REPEAT (assume_tac 1)); +by (eresolve_tac [ex1_two_eq] 1); +by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); +by (fast_tac (AC_cs addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1); +val subset_s_u_lepoll_w = result(); + +goal thy "!!k. [| 0 EX l:nat. k = succ(l)"; +by (eresolve_tac [natE] 1); +by (fast_tac (empty_cs addSEs [ltE, mem_irrefl]) 1); +by (fast_tac (empty_cs addSIs [refl, bexI]) 1); +val ex_eq_succ = result(); + +goal thy + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ +\ EX! w. w:t_n & z <= w; \ +\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ +\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0 EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y"; +by (resolve_tac [suppose_not] 1); +by (eresolve_tac [ex_eq_succ RS bexE] 1 THEN (assume_tac 1)); +by (hyp_subst_tac 1); +by (res_inst_tac [("n1","xa")] (ex_subset_eqpoll_n RS exE) 1 + THEN REPEAT (assume_tac 1)); +by (eresolve_tac [conjE] 1); +by (forward_tac [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans] 1 + THEN REPEAT (assume_tac 1)); +by (contr_tac 1); +val exists_proper_in_s_u = result(); + +(* ********************************************************************** *) +(* LL can be well ordered *) +(* ********************************************************************** *) + +goal thy "{x:Pow(X). x lepoll 0} = {0}"; +by (fast_tac (AC_cs addSDs [lepoll_0_is_0] + addSIs [singletonI, lepoll_refl, equalityI] + addSEs [singletonE]) 1); +val subsets_lepoll_0_eq_unit = result(); + +goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |] \ +\ ==> EX S. well_ord({Y: Pow(X) . Y eqpoll succ(n)}, S)"; +by (resolve_tac [well_ord_infinite_subsets_eqpoll_X + RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1 + THEN (REPEAT (assume_tac 1))); +by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); +val well_ord_subsets_eqpoll_n = result(); + +goal thy "!!n. 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 (ZF_cs addSIs [le_refl, leI, + le_imp_lepoll, equalityI] + addSDs [lepoll_succ_disj] + addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); +val subsets_lepoll_succ = result(); + +goal thy "!!n. n:nat ==> \ +\ {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; +by (fast_tac (ZF_cs addSEs [eqpoll_sym RS eqpoll_imp_lepoll + RS lepoll_trans RS succ_lepoll_natE] + addSIs [equals0I]) 1); +val Int_empty = result(); + +(* ********************************************************************** *) +(* unit set is well-ordered by the empty relation *) +(* ********************************************************************** *) + +goalw thy [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def] + "tot_ord({a},0)"; +by (simp_tac ZF_ss 1); +val tot_ord_unit = result(); + +goalw thy [wf_on_def, wf_def] "wf[{a}](0)"; +by (fast_tac (ZF_cs addSIs [equalityI]) 1); +val wf_on_unit = result(); + +goalw thy [well_ord_def] "well_ord({a},0)"; +by (simp_tac (ZF_ss addsimps [tot_ord_unit, wf_on_unit]) 1); +val well_ord_unit = result(); + +(* ********************************************************************** *) +(* well_ord_subsets_lepoll_n *) +(* ********************************************************************** *) + +goal thy "!!y r. [| well_ord(y,r); ~Finite(y); n:nat |] ==> \ +\ EX R. well_ord({z:Pow(y). z lepoll n}, R)"; +by (eresolve_tac [nat_induct] 1); +by (fast_tac (ZF_cs addSIs [well_ord_unit] + addss (ZF_ss addsimps [subsets_lepoll_0_eq_unit])) 1); +by (eresolve_tac [exE] 1); +by (eresolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 + THEN REPEAT (assume_tac 1)); +by (asm_simp_tac (ZF_ss addsimps [subsets_lepoll_succ]) 1); +by (dresolve_tac [well_ord_radd] 1 THEN (assume_tac 1)); +by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS + (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); +by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage]) 1); +val well_ord_subsets_lepoll_n = result(); + +goalw thy [LL_def, MM_def] + "!!x. t_n <= {v:Pow(x Un y). v eqpoll n} \ +\ ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}"; +by (fast_tac (AC_cs addSEs [RepFunE] + addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll + RSN (2, lepoll_trans))]) 1); +val LL_subset = result(); + +goal thy "!!x. [| t_n <= {v:Pow(x Un y). v eqpoll n}; \ +\ well_ord(y, R); ~Finite(y); n:nat \ +\ |] ==> EX S. well_ord(LL(t_n, k, y), S)"; +by (fast_tac (FOL_cs addIs [exI] + addSEs [LL_subset RSN (2, well_ord_subset)] + addEs [well_ord_subsets_lepoll_n RS exE]) 1); +val well_ord_LL = result(); + +(* ********************************************************************** *) +(* every element of LL is a contained in exactly one element of MM *) +(* ********************************************************************** *) + +goalw thy [MM_def, LL_def] + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ +\ v:LL(t_n, k, y) \ +\ |] ==> EX! w. w:MM(t_n, k, y) & v<=w"; +by (step_tac (AC_cs addSEs [RepFunE]) 1); +by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); +by (eres_inst_tac [("x","xa")] ballE 1); +by (fast_tac (AC_cs addSEs [eqpoll_sym]) 2); +by (res_inst_tac [("a","v")] ex1I 1); +by (fast_tac AC_cs 1); +by (eresolve_tac [ex1E] 1); +by (res_inst_tac [("x","v")] allE 1 THEN (assume_tac 1)); +by (eres_inst_tac [("x","xb")] allE 1); +by (fast_tac AC_cs 1); +val unique_superset_in_MM = result(); + +(* ********************************************************************** *) +(* The function GG satisfies the conditions of WO4 *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* The union of appropriate values is the whole x *) +(* ********************************************************************** *) + +goal thy + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ +\ EX! w. w:t_n & z <= w; \ +\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ +\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0 EX w:MM(t_n, succ(k), y). u:w"; +by (eresolve_tac [exists_proper_in_s_u RS bexE] 1 + THEN REPEAT (assume_tac 1)); +by (rewrite_goals_tac [MM_def, s_u_def]); +by (fast_tac AC_cs 1); +val exists_in_MM = result(); + +goalw thy [LL_def] "!!w. w : MM(t_n, k, y) ==> w Int y : LL(t_n, k, y)"; +by (fast_tac AC_cs 1); +val Int_in_LL = result(); + +goalw thy [MM_def] "MM(t_n, k, y) <= t_n"; +by (fast_tac AC_cs 1); +val MM_subset = result(); + +goal thy + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. \ +\ EX! w. w:t_n & z <= w; \ +\ well_ord(y,R); ~Finite(y); u:x; x Int y = 0; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ +\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0 EX w:LL(t_n, succ(k), y). u:GG(t_n, succ(k), y)`w"; +by (forward_tac [exists_in_MM] 1 THEN REPEAT (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (res_inst_tac [("x","w Int y")] bexI 1); +by (eresolve_tac [Int_in_LL] 2); +by (rewrite_goals_tac [GG_def]); +by (asm_full_simp_tac (AC_ss addsimps [Int_in_LL]) 1); +by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1 + THEN (assume_tac 1)); +by (REPEAT (fast_tac (AC_cs addEs [equals0D] addSEs [Int_in_LL]) 1)); +val exists_in_LL = result(); + +goalw thy [LL_def] + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ +\ v : LL(t_n, k, y) |] \ +\ ==> v = (THE x. x : MM(t_n, k, y) & v <= x) Int y"; +by (fast_tac (AC_cs addSEs [Int_in_LL, + unique_superset_in_MM RS the_equality2 RS ssubst]) 1); +val in_LL_eq_Int = result(); + +goal thy + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ +\ v : LL(t_n, k, y) |] \ +\ ==> (THE x. x : MM(t_n, k, y) & v <= x) <= x Un y"; +by (fast_tac (AC_cs addSDs [unique_superset_in_MM RS theI RS conjunct1 RS + (MM_subset RS subsetD)]) 1); +val the_in_MM_subset = result(); + +goalw thy [GG_def] + "!!x. [| ALL z:{z: Pow(x Un y) . z eqpoll k}. EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll n}; \ +\ v : LL(t_n, k, y) |] \ +\ ==> GG(t_n, k, y) ` v <= x"; +by (asm_full_simp_tac AC_ss 1); +by (forward_tac [the_in_MM_subset] 1 THEN REPEAT (assume_tac 1)); +by (dresolve_tac [in_LL_eq_Int] 1 THEN REPEAT (assume_tac 1)); +by (resolve_tac [subsetI] 1); +by (eresolve_tac [DiffE] 1); +by (eresolve_tac [swap] 1); +by (fast_tac (AC_cs addEs [ssubst]) 1); +val GG_subset = result(); + +goal thy + "!!x. [| well_ord(LL(t_n, succ(k), y), S); \ +\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ +\ well_ord(y,R); ~Finite(y); x Int y = 0; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ +\ ~ y lepoll {v:Pow(x). v eqpoll m}; 0 (UN b w eqpoll n"; +by (fast_tac AC_cs 1); +val in_MM_eqpoll_n = result(); + +goalw thy [LL_def, MM_def] + "!!w. w : LL(t_n, k, y) ==> k lepoll w"; +by (fast_tac AC_cs 1); +val in_LL_eqpoll_n = result(); + +goalw thy [GG_def] + "!!x. [| \ +\ ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}. EX! w. w:t_n & z <= w; \ +\ t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}; \ +\ well_ord(LL(t_n, succ(k), y), S); k:nat; m:nat |] \ +\ ==> ALL b WO4(n-k) *) +(* ********************************************************************** *) + +goalw thy [AC16_def,WO4_def] + "!!n k. [| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; +by (resolve_tac [allI] 1); +by (excluded_middle_tac "Finite(A)" 1); +by (resolve_tac [lemma1] 2 THEN REPEAT (assume_tac 2)); +by (resolve_tac [lemma2 RS revcut_rl] 1); +by (REPEAT (eresolve_tac [exE, conjE] 1)); +by (eres_inst_tac [("x","A Un y")] allE 1); +by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); +by (REPEAT (eresolve_tac [exE, conjE] 1)); +by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSIs [nat_succI, add_type]) 1); +by (res_inst_tac [("x","ordertype(LL(T, succ(k), y), x)")] exI 1); +by (res_inst_tac [("x","lam b:ordertype(LL(T, succ(k), y), x). \ +\ (GG(T, succ(k), y)) ` \ +\ (converse(ordermap(LL(T, succ(k), y), x)) ` b)")] exI 1); +by (simp_tac AC_ss 1); +by (fast_tac (empty_cs addSIs [conjI, lam_funtype RS domain_of_fun] + addSEs [Ord_ordertype, all_in_lepoll_m, OUN_eq_x]) 1); +qed "AC16_WO4"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC16_WO4.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC16_WO4.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,29 @@ +(* Title: ZF/AC/AC16_WO4.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski +*) + +AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux + + +consts + + ww :: "[i, i] => i" + s_u :: "[i, i, i, i] => i" + MM :: "[i, i, i] => i" + LL :: "[i, i, i] => i" + GG :: "[i, i, i] => i" + +defs + + ww_def "ww(x, k) == {u:Pow(x). u eqpoll k}" + + s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}" + + MM_def "MM(t_n, k, y) == {v:t_n. k lepoll v Int y}" + + LL_def "LL(t_n, k, y) == {v Int y. v:MM(t_n, k, y)}" + + GG_def "GG(t_n, k, y) == lam v:LL(t_n, k, y). + (THE w. w:MM(t_n, k, y) & v <= w) - v" + +end diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC16_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC16_lemmas.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,279 @@ +(* Title: ZF/AC/AC16_lemmas.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Lemmas used in the proofs concerning AC16 +*) + +open AC16_lemmas; + +goal thy "!!a. a~:A ==> cons(a,A)-{a}=A"; +by (fast_tac (ZF_cs addSIs [equalityI]) 1); +val cons_Diff_eq = result(); + +goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)"; +by (resolve_tac [iffI] 1); +by (fast_tac (ZF_cs addIs [inj_is_fun RS apply_type]) 1); +by (eresolve_tac [exE] 1); +by (res_inst_tac [("x","lam a:1. x")] exI 1); +by (fast_tac (ZF_cs addSIs [lam_injective]) 1); +val nat_1_lepoll_iff = result(); + +goal thy "X eqpoll 1 <-> (EX x. X={x})"; +by (resolve_tac [iffI] 1); +by (eresolve_tac [eqpollE] 1); +by (dresolve_tac [nat_1_lepoll_iff RS iffD1] 1); +by (fast_tac (ZF_cs addSIs [lepoll_1_is_sing]) 1); +by (fast_tac (ZF_cs addSIs [singleton_eqpoll_1]) 1); +val eqpoll_1_iff_singleton = result(); + +goalw thy [succ_def] + "!!x. [| x eqpoll n; y~:x |] ==> cons(y,x) eqpoll succ(n)"; +by (fast_tac (ZF_cs addSEs [cons_eqpoll_cong, mem_irrefl]) 1); +val cons_eqpoll_succ = result(); + +goal thy "{Y:Pow(X). Y eqpoll 1} = {{x}. x:X}"; +by (resolve_tac [equalityI] 1); +by (resolve_tac [subsetI] 1); +by (eresolve_tac [CollectE] 1); +by (dresolve_tac [eqpoll_1_iff_singleton RS iffD1] 1); +by (fast_tac (AC_cs addSIs [RepFunI]) 1); +by (resolve_tac [subsetI] 1); +by (eresolve_tac [RepFunE] 1); +by (resolve_tac [CollectI] 1); +by (fast_tac AC_cs 1); +by (fast_tac (AC_cs addSIs [singleton_eqpoll_1]) 1); +val subsets_eqpoll_1_eq = result(); + +goalw thy [eqpoll_def, bij_def] "X eqpoll {{x}. x:X}"; +by (res_inst_tac [("x","lam x:X. {x}")] exI 1); +by (resolve_tac [IntI] 1); +by (rewrite_goals_tac [inj_def, surj_def]); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSIs [lam_type, RepFunI] + addIs [singleton_eq_iff RS iffD1]) 1); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSIs [lam_type]) 1); +val eqpoll_RepFun_sing = result(); + +goal thy "{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); +val subsets_eqpoll_1_eqpoll = result(); + +goal thy "!!x. [| 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 (AC_cs addIs [LeastI] + addSDs [InfCard_is_Card RS Card_is_Ord, PowD RS subsetD] + addEs [Ord_in_Ord]) 1); +val InfCard_Least_in = result(); + +goalw thy [lepoll_def] "!!i. [| 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); +by (res_inst_tac [("d","%z. cons(fst(z),snd(z))")] lam_injective 1); +by (resolve_tac [SigmaI] 1); +by (eresolve_tac [CollectE] 1); +by (asm_full_simp_tac AC_ss 3); +by (resolve_tac [equalityI] 3); +by (fast_tac AC_cs 4); +by (resolve_tac [subsetI] 3); +by (eresolve_tac [consE] 3); +by (fast_tac AC_cs 4); +by (resolve_tac [CollectI] 2); +by (fast_tac AC_cs 2); +by (resolve_tac [PowD RS subsetD] 1 THEN (assume_tac 1)); +by (REPEAT (fast_tac (AC_cs addSIs [Diff_sing_eqpoll] + addIs [InfCard_Least_in]) 1)); +val subsets_lepoll_lemma1 = result(); + +val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))"; +by (resolve_tac [subsetI] 1); +by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1); +by (fast_tac (AC_cs addSIs [equalityI]) 2); +by (eresolve_tac [swap] 1); +by (resolve_tac [ballI] 1); +by (resolve_tac [Ord_linear_le] 1); +by (dresolve_tac [le_imp_subset] 3 THEN (assume_tac 3)); +by (fast_tac (AC_cs addDs prems) 1); +by (fast_tac (AC_cs addDs prems) 1); +by (fast_tac (AC_cs addSEs [leE,ltE]) 1); +val set_of_Ord_succ_Union = result(); + +goal thy "!!i. j<=i ==> i ~: j"; +by (fast_tac (ZF_cs addSEs [mem_irrefl]) 1); +val subset_not_mem = result(); + +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); +val succ_Union_not_mem = result(); + +goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))"; +by (fast_tac (AC_cs addIs [equalityI]) 1); +val Union_cons_eq_succ_Union = result(); + +goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j"; +by (fast_tac (AC_cs addSDs [le_imp_subset] addIs [equalityI] + addEs [Ord_linear_le]) 1); +val Un_Ord_disj = result(); + +goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})"; +by (fast_tac (AC_cs addIs [equalityI]) 1); +val Union_eq_Un = result(); + +goal thy "!!n. n:nat ==> \ +\ ALL z. (ALL y:z. Ord(y)) & z eqpoll n & z~=0 --> Union(z) : z"; +by (eresolve_tac [nat_induct] 1); +by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); +by (REPEAT (resolve_tac [allI, impI] 1)); +by (eresolve_tac [natE] 1); +by (fast_tac (AC_cs addSDs [eqpoll_1_iff_singleton RS iffD1] + addSIs [Union_singleton]) 1); +by (hyp_subst_tac 1); +by (REPEAT (eresolve_tac [conjE, not_emptyE] 1)); +by (eres_inst_tac [("x","z-{xb}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac (AC_cs addSEs [Diff_sing_eqpoll, + Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1); +by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2)); +by (forward_tac [bspec] 1 THEN (assume_tac 1)); +by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1)); +by (dresolve_tac [Un_Ord_disj] 1 THEN (assume_tac 1)); +by (eresolve_tac [DiffE] 1); +by (eresolve_tac [disjE] 1); +by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (resolve_tac [subst_elem] 1 THEN (TRYALL assume_tac)); +val Union_in_lemma = result(); + +goal thy "!!z. [| ALL x:z. Ord(x); z eqpoll n; z~=0; n:nat |] \ +\ ==> Union(z) : z"; +by (dresolve_tac [Union_in_lemma] 1); +by (fast_tac FOL_cs 1); +val Union_in = result(); + +goal thy "!!x. [| 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 (eresolve_tac [InfCard_is_Limit] 1); +by (excluded_middle_tac "z=0" 1); +by (fast_tac (AC_cs addSIs [InfCard_is_Limit RS Limit_has_0] + addIs [Union_0 RS ssubst]) 2); +by (resolve_tac + [PowD RS subsetD RS (InfCard_is_Card RS Card_is_Ord RSN (2, ltI))] 1 + THEN (TRYALL assume_tac)); +by (fast_tac (AC_cs addSIs [Union_in] + addSEs [PowD RS subsetD RSN (2, + InfCard_is_Card RS Card_is_Ord RS Ord_in_Ord)]) 1); +val succ_Union_in_x = result(); + +goalw thy [lepoll_def] "!!X. [| 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)}. \ +\ 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); +by (resolve_tac [cons_Diff_eq] 2); +by (fast_tac (AC_cs addSDs [InfCard_is_Card RS Card_is_Ord] + addEs [Ord_in_Ord] addSIs [succ_Union_not_mem]) 2); +by (resolve_tac [CollectI] 1); +by (fast_tac (AC_cs addSEs [cons_eqpoll_succ] + addSIs [succ_Union_not_mem] + addSDs [InfCard_is_Card RS Card_is_Ord] + addEs [Ord_in_Ord]) 2); +by (fast_tac (AC_cs addSIs [succ_Union_in_x, nat_succI]) 1); +val succ_lepoll_succ_succ = result(); + +goal thy "!!X. [| InfCard(X); n:nat |] \ +\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; +by (eresolve_tac [nat_induct] 1); +by (resolve_tac [subsets_eqpoll_1_eqpoll] 1); +by (resolve_tac [eqpollI] 1); +by (resolve_tac [subsets_lepoll_lemma1 RS lepoll_trans] 1 + THEN (REPEAT (assume_tac 1))); +by (resolve_tac [InfCard_is_Card RS Card_is_Ord RS well_ord_Memrel RS + well_ord_InfCard_square_eq RS eqpoll_imp_lepoll + RSN (2, lepoll_trans)] 1 THEN (assume_tac 2)); +by (resolve_tac [InfCard_is_Card RS Card_cardinal_eq RS ssubst] 2 + THEN (REPEAT (assume_tac 2))); +by (eresolve_tac [eqpoll_refl RS prod_eqpoll_cong RS eqpoll_imp_lepoll] 1); +by (fast_tac (AC_cs addEs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_trans] + addSIs [succ_lepoll_succ_succ]) 1); +val subsets_eqpoll_X = result(); + +goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |] \ +\ ==> f``(converse(f)``y) = y"; +by (fast_tac (AC_cs addSIs [equalityI] addDs [apply_equality2] + addEs [apply_iff RS iffD2]) 1); +val image_vimage_eq = result(); + +goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y"; +by (fast_tac (AC_cs addSIs [equalityI] addSEs [inj_is_fun RS apply_Pair] + addDs [inj_equality]) 1); +val vimage_image_eq = result(); + +goalw thy [eqpoll_def] "!!A B. A eqpoll B \ +\ ==> {Y:Pow(A). Y eqpoll n} eqpoll {Y:Pow(B). Y eqpoll n}"; +by (eresolve_tac [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 [("d","%Z. converse(f)``Z")] lam_bijective 1); +by (fast_tac (AC_cs + addSIs [bij_is_inj RS restrict_bij RS bij_converse_bij RS comp_bij] + addSEs [bij_is_fun RS fun_is_rel RS image_subset RS PowI]) 1); +by (fast_tac (AC_cs addSIs [bij_converse_bij RS bij_is_inj RS restrict_bij + RS bij_converse_bij RS comp_bij] + addSEs [bij_converse_bij RS bij_is_fun RS fun_is_rel + RS image_subset RS PowI]) 1); +by (fast_tac (AC_cs addSEs [bij_is_inj RS vimage_image_eq]) 1); +by (fast_tac (AC_cs addSEs [bij_is_surj RS image_vimage_eq]) 1); +val subsets_eqpoll = result(); + +goalw thy [WO2_def] "!!X. WO2 ==> EX a. Card(a) & X eqpoll a"; +by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); +by (fast_tac (AC_cs addSEs [well_ord_Memrel RS well_ord_cardinal_eqpoll RS + (eqpoll_sym RSN (2, eqpoll_trans)) RS eqpoll_sym] + addSIs [Card_cardinal]) 1); +val WO2_imp_ex_Card = result(); + +goal thy "!!X. [| X lepoll Y; ~Finite(X) |] ==> ~Finite(Y)"; +by (fast_tac (empty_cs addEs [notE, lepoll_Finite] addSIs [notI]) 1); +val lepoll_infinite = result(); + +goalw thy [InfCard_def] "!!X. [| ~Finite(X); Card(X) |] ==> InfCard(X)"; +by (fast_tac (AC_cs addSEs [Card_is_Ord RS nat_le_infinite_Ord]) 1); +val infinite_Card_is_InfCard = result(); + +goal thy "!!X n. [| WO2; n:nat; ~Finite(X) |] \ +\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; +by (dresolve_tac [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)); +by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1)); +by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1); +by (eresolve_tac [subsets_eqpoll] 1); +by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1)); +by (eresolve_tac [eqpoll_sym] 1); +val WO2_infinite_subsets_eqpoll_X = result(); + +goal thy "!!X. well_ord(X,R) ==> EX a. Card(a) & X eqpoll a"; +by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll RS eqpoll_sym] + addSIs [Card_cardinal]) 1); +val well_ord_imp_ex_Card = result(); + +goal thy "!!X n. [| well_ord(X,R); n:nat; ~Finite(X) |] \ +\ ==> {Y:Pow(X). Y eqpoll succ(n)} eqpoll X"; +by (dresolve_tac [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)); +by (dresolve_tac [infinite_Card_is_InfCard] 1 THEN (assume_tac 1)); +by (resolve_tac [eqpoll_trans RS eqpoll_trans] 1); +by (eresolve_tac [subsets_eqpoll] 1); +by (eresolve_tac [subsets_eqpoll_X] 1 THEN (assume_tac 1)); +by (eresolve_tac [eqpoll_sym] 1); +val well_ord_infinite_subsets_eqpoll_X = result(); + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC16_lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC16_lemmas.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +AC16_lemmas = AC_Equiv + Hartog + first diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC17_AC1.ML --- a/src/ZF/AC/AC17_AC1.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC17_AC1.ML Tue Jul 25 17:31:53 1995 +0200 @@ -71,7 +71,8 @@ by (asm_full_simp_tac AC_ss 1); val lemma4 = result(); -goalw thy [AC17_def] "!!Z. [| AC17; ~ AC1 |] ==> False"; +goalw thy [AC17_def] "!!Z. AC17 ==> AC1"; +by (resolve_tac [classical] 1); by (eresolve_tac [not_AC1_imp_ex RS exE] 1); by (excluded_middle_tac "EX f: Pow(x)-{0}->x. \ @@ -80,7 +81,7 @@ by (eresolve_tac [lemma1] 2 THEN (assume_tac 2)); by (dresolve_tac [lemma2] 1); by (eresolve_tac [allE] 1); -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (dresolve_tac [lemma4] 1); by (eresolve_tac [bexE] 1); by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); @@ -89,7 +90,4 @@ by (dresolve_tac [lemma3] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); -result(); - - - +qed "AC17_AC1"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC18_AC19.ML --- a/src/ZF/AC/AC18_AC19.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC18_AC19.ML Tue Jul 25 17:31:53 1995 +0200 @@ -15,9 +15,9 @@ \ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))"; by (resolve_tac [lam_type] 1); by (dresolve_tac [apply_type] 1); -by (resolve_tac [RepFunI] 1 THEN (atac 1)); -by (dresolve_tac [bspec] 1 THEN (atac 1)); -by (eresolve_tac [subsetD] 1 THEN (atac 1)); +by (resolve_tac [RepFunI] 1 THEN (assume_tac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (eresolve_tac [subsetD] 1 THEN (assume_tac 1)); val PROD_subsets = result(); goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \ @@ -39,7 +39,7 @@ by (resolve_tac [prem RS revcut_rl] 1); by (fast_tac (AC_cs addSEs [lemma_AC18, UN_E, not_emptyE, apply_type] addSIs [equalityI, INT_I, UN_I]) 1); -result(); +qed "AC1_AC18"; (* ********************************************************************** *) (* AC18 ==> AC19 *) @@ -49,7 +49,7 @@ by (resolve_tac [allI] 1); by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1); by (fast_tac AC_cs 1); -result(); +qed "AC18_AC19"; (* ********************************************************************** *) (* AC19 ==> AC1 *) @@ -64,7 +64,7 @@ goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a"; by (hyp_subst_tac 1); -by (resolve_tac [subst_elem] 1 THEN (atac 1)); +by (resolve_tac [subst_elem] 1 THEN (assume_tac 1)); by (resolve_tac [equalityI] 1); by (fast_tac AC_cs 1); by (resolve_tac [subsetI] 1); @@ -116,6 +116,6 @@ by (dresolve_tac [lemma2] 1 THEN (assume_tac 1)); by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [lemma3 RS not_emptyE]) 1); -result(); +qed "AC19_AC1"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC1_AC17.ML --- a/src/ZF/AC/AC1_AC17.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC1_AC17.ML Tue Jul 25 17:31:53 1995 +0200 @@ -22,4 +22,4 @@ by (eresolve_tac [lemma1] 2); by (resolve_tac [apply_type] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSDs [lemma1] addSEs [apply_type]) 1); -result(); \ No newline at end of file +qed "AC1_AC17"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC1_WO2.ML --- a/src/ZF/AC/AC1_WO2.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC1_WO2.ML Tue Jul 25 17:31:53 1995 +0200 @@ -20,4 +20,4 @@ by (resolve_tac [allI] 1); by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); by (fast_tac (AC_cs addSDs [lemma1] addSIs [Ord_Least]) 1); -result(); +qed "AC1_WO2"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC2_AC6.ML --- a/src/ZF/AC/AC2_AC6.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC2_AC6.ML Tue Jul 25 17:31:53 1995 +0200 @@ -2,8 +2,8 @@ ID: $Id$ Author: Krzysztof Gr`abczewski -The proofs needed to state that each of AC2, AC3, ..., AC6 is equivallent -to AC0 and AC1. Namely: +The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent +to AC0 and AC1: AC1 ==> AC2 ==> AC1 AC1 ==> AC4 ==> AC3 ==> AC1 AC4 ==> AC5 ==> AC4 @@ -29,9 +29,9 @@ by (resolve_tac [impI] 1); by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1)); by (REPEAT (resolve_tac [exI,ballI,equalityI] 1)); -by (resolve_tac [lemma1] 2 THEN (REPEAT (atac 2))); +by (resolve_tac [lemma1] 2 THEN (REPEAT (assume_tac 2))); by (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1); -result(); +qed "AC1_AC2"; (* ********************************************************************** *) @@ -64,7 +64,7 @@ by (REPEAT (eresolve_tac [allE, impE] 1)); by (fast_tac (AC_cs addSEs [lemma3]) 2); by (fast_tac (AC_cs addSIs [lemma1, equals0I]) 1); -result(); +qed "AC2_AC1"; (* ********************************************************************** *) @@ -79,7 +79,7 @@ by (REPEAT (resolve_tac [allI, impI] 1)); by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1)); by (fast_tac (AC_cs addSIs [lam_type, RepFunI] addSEs [apply_type]) 1); -result(); +qed "AC1_AC4"; (* ********************************************************************** *) @@ -107,7 +107,7 @@ by (eresolve_tac [lemma1] 1); by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3] addcongs [Pi_cong]) 1); -result(); +qed "AC4_AC3"; (* ********************************************************************** *) (* AC3 ==> AC1 *) @@ -124,7 +124,7 @@ by (REPEAT (eresolve_tac [allE, ballE] 1)); by (fast_tac (AC_cs addSIs [id_type]) 2); by (fast_tac (AC_cs addEs [lemma RS subst]) 1); -result(); +qed "AC3_AC1"; (* ********************************************************************** *) (* AC4 ==> AC5 *) @@ -136,15 +136,15 @@ by (eresolve_tac [fun_is_rel RS converse_type] 1); by (eresolve_tac [exE] 1); by (resolve_tac [bexI] 1); -by (resolve_tac [Pi_type] 2 THEN (atac 2)); +by (resolve_tac [Pi_type] 2 THEN (assume_tac 2)); by (fast_tac (ZF_cs addSDs [apply_type] addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); by (resolve_tac [ballI] 1); -by (resolve_tac [apply_equality] 1 THEN (atac 2)); +by (resolve_tac [apply_equality] 1 THEN (assume_tac 2)); by (eresolve_tac [domainE] 1); -by (forward_tac [range_type] 1 THEN (atac 1)); +by (forward_tac [range_type] 1 THEN (assume_tac 1)); by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1); -result(); +qed "AC4_AC5"; (* ********************************************************************** *) @@ -175,21 +175,21 @@ goal thy "!!g. [| 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})"; by (resolve_tac [lam_type] 1); -by (dresolve_tac [apply_type] 1 THEN (atac 1)); -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (resolve_tac [imageI] 1); by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1 - THEN (REPEAT (atac 1))); + THEN (REPEAT (assume_tac 1))); by (asm_full_simp_tac AC_ss 1); val lemma4 = result(); goalw thy AC_defs "!!Z. AC5 ==> AC4"; by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE,ballE] 1)); -by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (atac 2)); -by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (atac 1)); +by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2)); +by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [lemma4]) 1); -result(); +qed "AC5_AC4"; (* ********************************************************************** *) @@ -198,4 +198,5 @@ goalw thy AC_defs "AC1 <-> AC6"; by (fast_tac (ZF_cs addDs [equals0D] addSEs [not_emptyE]) 1); -result(); +qed "AC1_iff_AC6"; + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC7_AC9.ML --- a/src/ZF/AC/AC7_AC9.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC7_AC9.ML Tue Jul 25 17:31:53 1995 +0200 @@ -27,12 +27,12 @@ goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)"; by (REPEAT (resolve_tac [ballI] 1)); by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1 - THEN REPEAT (atac 1)); + THEN REPEAT (assume_tac 1)); val all_eqpoll_imp_pair_eqpoll = result(); goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \ \ |] ==> P(b)=R(b)"; -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (asm_full_simp_tac ZF_ss 1); val if_eqE1 = result(); @@ -40,7 +40,7 @@ \ ==> ALL a:A. a~=b --> Q(a)=S(a)"; by (resolve_tac [ballI] 1); by (resolve_tac [impI] 1); -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (asm_full_simp_tac ZF_ss 1); val if_eqE2 = result(); @@ -65,8 +65,8 @@ by (resolve_tac [conjI] 1); by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2); by (asm_full_simp_tac AC_ss 2); -by (resolve_tac [fun_extension] 1 THEN REPEAT (atac 1)); -by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (atac 1)); +by (resolve_tac [fun_extension] 1 THEN REPEAT (assume_tac 1)); +by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1)); by (asm_full_simp_tac (AC_ss addsimps [succ_not_0 RS if_not_P]) 1); by (fast_tac (AC_cs addSEs [diff_succ_succ RS (diff_0 RSN (2, trans)) RS subst] addSIs [nat_0I]) 1); @@ -87,7 +87,7 @@ goalw thy AC_defs "!!Z. AC6 ==> AC7"; by (fast_tac ZF_cs 1); -result(); +qed "AC6_AC7"; (* ********************************************************************** *) (* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) @@ -122,11 +122,11 @@ by (fast_tac (ZF_cs addSIs [not_emptyI, empty_fun]) 2); by (resolve_tac [lemma1] 1); by (eresolve_tac [allE] 1); -by (eresolve_tac [impE] 1 THEN (atac 2)); +by (eresolve_tac [impE] 1 THEN (assume_tac 2)); by (fast_tac (AC_cs addSEs [RepFunE] addSIs [lemma2, all_eqpoll_imp_pair_eqpoll, Sigma_fun_space_eqpoll]) 1); -result(); +qed "AC7_AC6"; (* ********************************************************************** *) @@ -138,7 +138,7 @@ \ ==> 0 ~: { bij(fst(B),snd(B)). B:A }"; by (resolve_tac [notI] 1); by (eresolve_tac [RepFunE] 1); -by (dresolve_tac [bspec] 1 THEN (atac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); by (REPEAT (eresolve_tac [exE,conjE] 1)); by (hyp_subst_tac 1); by (asm_full_simp_tac AC_ss 1); @@ -147,7 +147,7 @@ goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |] \ \ ==> (lam x:A. f`p(x))`D : p(D)"; -by (resolve_tac [beta RS ssubst] 1 THEN (atac 1)); +by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSEs [apply_type]) 1); val lemma2 = result(); @@ -158,7 +158,7 @@ by (eresolve_tac [impE] 1); by (eresolve_tac [lemma1] 1); by (fast_tac (AC_cs addSEs [lemma2]) 1); -result(); +qed "AC1_AC8"; (* ********************************************************************** *) @@ -183,7 +183,7 @@ by (eresolve_tac [impE] 1); by (eresolve_tac [lemma1] 1); by (fast_tac (AC_cs addSEs [lemma2]) 1); -result(); +qed "AC8_AC9"; (* ********************************************************************** *) @@ -225,13 +225,13 @@ by (fast_tac (ZF_cs addSIs [fun_weaken_type, bij_is_fun]) 1); val lemma2 = result(); -val prems = goalw thy AC_defs "!!Z. AC9 ==> AC1"; +goalw thy AC_defs "!!Z. AC9 ==> AC1"; by (resolve_tac [allI] 1); by (resolve_tac [impI] 1); by (eresolve_tac [allE] 1); by (excluded_middle_tac "A=0" 1); by (fast_tac (FOL_cs addSIs [empty_fun]) 2); by (eresolve_tac [impE] 1); -by (resolve_tac [lemma1] 1 THEN (REPEAT (atac 1))); +by (resolve_tac [lemma1] 1 THEN (REPEAT (assume_tac 1))); by (fast_tac (AC_cs addSEs [lemma2]) 1); -result(); \ No newline at end of file +qed "AC9_AC1"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Tue Jul 25 17:31:53 1995 +0200 @@ -69,12 +69,12 @@ (*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"; -by (resolve_tac [not_emptyE] 1 THEN (atac 1)); +by (resolve_tac [not_emptyE] 1 THEN (assume_tac 1)); by (forward_tac [singleton_subsetI] 1); -by (forward_tac [subsetD] 1 THEN (atac 1)); +by (forward_tac [subsetD] 1 THEN (assume_tac 1)); by (res_inst_tac [("A2","A")] (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 - THEN (REPEAT (atac 2))); + THEN (REPEAT (assume_tac 2))); by (fast_tac ZF_cs 1); val Diff_lepoll = result(); @@ -91,9 +91,9 @@ by (resolve_tac [equalityI] 1); by (step_tac ZF_cs 1); by (dres_inst_tac [("P","%a. :r")] (id_conv RS subst) 1 - THEN (atac 1)); + THEN (assume_tac 1)); by (dres_inst_tac [("P","%a. :r")] (id_conv RS subst) 1 - THEN (REPEAT (atac 1))); + THEN (REPEAT (assume_tac 1))); by (fast_tac (ZF_cs addIs [id_conv RS ssubst]) 1); val rvimage_id = result(); @@ -138,3 +138,45 @@ by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1); val Sigma_empty_iff = result(); +goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; +by (fast_tac (AC_cs addSIs [eqpoll_refl]) 1); +val nat_into_Finite = result(); + +goalw thy [Finite_def] "~Finite(nat)"; +by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll] + addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); +val nat_not_Finite = result(); + +val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; + +(* ********************************************************************** *) +(* Another elimination rule for EX! *) +(* ********************************************************************** *) + +goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; +by (eresolve_tac [ex1E] 1); +by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); +by (fast_tac AC_cs 1); +by (fast_tac AC_cs 1); +val ex1_two_eq = result(); + +(* ********************************************************************** *) +(* image of a surjection *) +(* ********************************************************************** *) + +goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; +by (eresolve_tac [CollectE] 1); +by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [RepFunE, apply_type] + addSIs [RepFunI] addIs [equalityI]) 1); +val surj_image_eq = result(); + + +goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; +by (fast_tac (ZF_cs addSDs [lepoll_0_is_0]) 1); +val succ_lepoll_imp_not_empty = result(); + +goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; +by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); +val eqpoll_succ_imp_not_empty = result(); + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/Cardinal_aux.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/Cardinal_aux.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,371 @@ +(* Title: ZF/AC/Cardinal_aux.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Auxiliary lemmas concerning cardinalities +*) + +open Cardinal_aux; + +(* ********************************************************************** *) +(* Lemmas involving ordinals and cardinalities used in the proofs *) +(* concerning AC16 and DC *) +(* ********************************************************************** *) + +val nat_0_in_2 = Ord_0 RS le_refl RS leI RS ltD; + +goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)"; +by (resolve_tac [conjI] 1); +by (resolve_tac [Card_cardinal] 1); +by (resolve_tac [Card_nat RS (Card_def RS def_imp_iff RS iffD1 RS ssubst)] 1); +by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll + RSN (2, well_ord_Memrel RS well_ord_lepoll_imp_Card_le)] 1 + THEN REPEAT (assume_tac 1)); +val Inf_Ord_imp_InfCard_cardinal = result(); + +goalw thy [lepoll_def] "A Un B lepoll A+B"; +by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1); +by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1); +by (split_tac [expand_if] 1); +by (fast_tac (AC_cs addSIs [InlI, InrI]) 1); +by (split_tac [expand_if] 1); +by (asm_full_simp_tac (AC_ss addsimps [Inl_def, Inr_def]) 1); +val Un_lepoll_sum = result(); + +goalw thy [sum_def] "A+A = 2*A"; +by (fast_tac (AC_cs addIs [equalityI] + addSIs [singletonI, nat_0_in_2, succI1] + addSEs [succE, singletonE]) 1); +val sum_eq_2_times = result(); + +val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll, + asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans)) + |> standard; + +goal thy "!!A. [| A lepoll B; 2 lepoll A |] ==> A+B lepoll A*B"; +by (REPEAT (ares_tac [[sum_lepoll_mono, sum_lepoll_prod] + MRS lepoll_trans, lepoll_refl] 1)); +val lepoll_imp_sum_lepoll_prod = result(); + +goal thy "!!A. [| A eqpoll i; B eqpoll i; ~Finite(i); Ord(i) |] \ +\ ==> A Un B eqpoll i"; +by (resolve_tac [eqpollI] 1); +by (eresolve_tac [subset_imp_lepoll RSN (2, eqpoll_sym RS eqpoll_imp_lepoll + RS lepoll_trans)] 2); +by (fast_tac AC_cs 2); +by (resolve_tac [Un_lepoll_sum RS lepoll_trans] 1); +by (resolve_tac [lepoll_imp_sum_lepoll_prod RS lepoll_trans] 1); +by (eresolve_tac [eqpoll_sym RSN (2, eqpoll_trans) RS eqpoll_imp_lepoll] 1 + THEN (assume_tac 1)); +by (resolve_tac [nat_le_infinite_Ord RS le_imp_lepoll RS + (Ord_nat RS (nat_2I RS OrdmemD) RS subset_imp_lepoll RS lepoll_trans) + RS (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans))] 1 + THEN (REPEAT (assume_tac 1))); +by (eresolve_tac [prod_eqpoll_cong RS eqpoll_imp_lepoll RS lepoll_trans] 1 + THEN (assume_tac 1)); +by (resolve_tac [Inf_Ord_imp_InfCard_cardinal RSN (2, well_ord_Memrel RS + well_ord_InfCard_square_eq) RS eqpoll_imp_lepoll] 1 + THEN REPEAT (assume_tac 1)); +val Un_eqpoll_Inf_Ord = result(); + +goalw thy [lepoll_def] "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] \ +\ ==> A Un C lepoll B Un D"; +by (REPEAT (eresolve_tac [exE] 1)); +by (res_inst_tac [("x","lam a: A Un C. if(a:A, f`a, fa`a)")] exI 1); +by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(fa)`z)")] + lam_injective 1); +by (split_tac [expand_if] 1); +by (eresolve_tac [UnE] 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type] addSIs [UnI2]) 1); +by (REPEAT (split_tac [expand_if] 1)); +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs addSEs [left_inverse, inj_is_fun RS apply_type] + addEs [swap]) 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [UnE] 1); +by (contr_tac 1); +by (resolve_tac [conjI] 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [equals0D] 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type]) 1); +by (fast_tac (AC_cs addSEs [left_inverse]) 1); +val Un_lepoll_Un = result(); + +goal thy "{x, y} - {y} = {x} - {y}"; +by (fast_tac eq_cs 1); +val double_Diff_sing = result(); + +goal thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y"; +by (split_tac [expand_if] 1); +by (asm_full_simp_tac (AC_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1); +by (fast_tac (AC_cs addSIs [the_equality, equalityI, equals0I] + addEs [equalityE] addSEs [singletonE]) 1); +val paired_bij_lemma = result(); + +goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w})) \ +\ : bij({{y,z}. y:x}, x)"; +by (res_inst_tac [("d","%a. {a,z}")] lam_bijective 1); +by (TRYALL (fast_tac (AC_cs addSEs [RepFunE] addSIs [RepFunI] + addss (AC_ss addsimps [paired_bij_lemma])))); +val paired_bij = result(); + +goalw thy [eqpoll_def] "{{y,z}. y:x} eqpoll x"; +by (fast_tac (AC_cs addSIs [paired_bij]) 1); +val paired_eqpoll = result(); + +goal thy "!!A. EX B. B eqpoll A & B Int C = 0"; +by (fast_tac (AC_cs addSIs [paired_eqpoll, equals0I] addEs [mem_asym]) 1); +val ex_eqpoll_disjoint = result(); + +goal thy "!!A. [| A lepoll i; B lepoll i; ~Finite(i); Ord(i) |] \ +\ ==> A Un B lepoll i"; +by (res_inst_tac [("A1","i"), ("C1","i")] (ex_eqpoll_disjoint RS exE) 1); +by (eresolve_tac [conjE] 1); +by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, lepoll_trans)] 1); +by (assume_tac 1); +by (resolve_tac [Un_lepoll_Un RS lepoll_trans] 1 THEN (REPEAT (assume_tac 1))); +by (eresolve_tac [eqpoll_refl RSN (2, Un_eqpoll_Inf_Ord) RS + eqpoll_imp_lepoll] 1 + THEN (REPEAT (assume_tac 1))); +val Un_lepoll_Inf_Ord = result(); + +goal thy "!!P. [| P(i); i:j; Ord(j) |] ==> (LEAST i. P(i)) : j"; +by (eresolve_tac [Least_le RS leE] 1); +by (eresolve_tac [Ord_in_Ord] 1 THEN (assume_tac 1)); +by (eresolve_tac [ltE] 1); +by (fast_tac (AC_cs addDs [OrdmemD]) 1); +by (eresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +val Least_in_Ord = result(); + +goal thy "!!x. [| well_ord(x,r); y<=x; y lepoll succ(n); n: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 (AC_cs addSIs [Diff_sing_lepoll, the_first_in]) 1); +by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1); +by (resolve_tac [empty_lepollI] 2); +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val Diff_first_lepoll = result(); + +goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))"; +by (fast_tac AC_cs 1); +val UN_subset_split = result(); + +goalw thy [lepoll_def] "!!a. 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); +by (res_inst_tac [("d","%z. P(z)")] lam_injective 1); +by (fast_tac (AC_cs addSIs [Least_in_Ord]) 1); +by (fast_tac (AC_cs addIs [LeastI] addSEs [singletonE, Ord_in_Ord]) 1); +val UN_sing_lepoll = result(); + +goal thy "!!a T. [| 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"; +by (eresolve_tac [nat_induct] 1); +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (res_inst_tac [("b","UN b:a. f`b")] subst 1); +by (resolve_tac [empty_lepollI] 2); +by (resolve_tac [equals0I RS sym] 1); +by (REPEAT (eresolve_tac [UN_E, allE] 1)); +by (fast_tac (AC_cs addDs [lepoll_0_is_0 RS subst]) 1); +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (eres_inst_tac [("x","lam x:a. f`x - {THE b. first(b,f`x,R)}")] allE 1); +by (eresolve_tac [impE] 1); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSIs [Diff_first_lepoll]) 1); +by (asm_full_simp_tac AC_ss 1); +by (resolve_tac [UN_subset_split RS subset_imp_lepoll RS lepoll_trans] 1); +by (resolve_tac [Un_lepoll_Inf_Ord] 1 THEN (REPEAT_FIRST assume_tac)); +by (eresolve_tac [UN_sing_lepoll] 1); +val UN_fun_lepoll_lemma = result(); + +goal thy "!!a f. [| 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"; +by (eresolve_tac [UN_fun_lepoll_lemma RS allE] 1 THEN (REPEAT (assume_tac 1))); +by (fast_tac AC_cs 1); +val UN_fun_lepoll = result(); + +goal thy "!!a f. [| 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"; +by (resolve_tac [impE] 1 THEN (assume_tac 3)); +by (res_inst_tac [("f","lam b:a. F(b)")] (UN_fun_lepoll) 2 + THEN (TRYALL assume_tac)); +by (simp_tac AC_ss 2); +by (asm_full_simp_tac AC_ss 1); +val UN_lepoll = result(); + +goal thy "!!a. Ord(a) ==> (UN b:a. F(b)) = (UN b:a. F(b) - (UN c:b. F(c)))"; +by (resolve_tac [equalityI] 1); +by (fast_tac AC_cs 2); +by (resolve_tac [subsetI] 1); +by (eresolve_tac [UN_E] 1); +by (resolve_tac [UN_I] 1); +by (res_inst_tac [("P","%z. x:F(z)")] Least_in_Ord 1 THEN (REPEAT (assume_tac 1))); +by (resolve_tac [DiffI] 1); +by (resolve_tac [Ord_in_Ord RSN (2, LeastI)] 1 THEN (REPEAT (assume_tac 1))); +by (resolve_tac [notI] 1); +by (eresolve_tac [UN_E] 1); +by (eres_inst_tac [("P","%z. x:F(z)"),("i","c")] less_LeastE 1); +by (eresolve_tac [Ord_Least RSN (2, ltI)] 1); +val UN_eq_UN_Diffs = result(); + +goalw thy [eqpoll_def] "!!A B. A Int B = 0 ==> A Un B eqpoll A + B"; +by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1); +by (res_inst_tac [("d","%z. case(%x.x, %x.x, z)")] lam_bijective 1); +by (fast_tac (AC_cs addSIs [if_type, InlI, InrI]) 1); +by (TRYALL (eresolve_tac [sumE])); +by (TRYALL (split_tac [expand_if])); +by (TRYALL (asm_simp_tac sum_ss)); +by (fast_tac (AC_cs addDs [equals0D]) 1); +val disj_Un_eqpoll_sum = result(); + +goalw thy [lepoll_def, eqpoll_def] + "!!X a. a lepoll X ==> EX Y. Y<=X & a eqpoll Y"; +by (eresolve_tac [exE] 1); +by (forward_tac [subset_refl RSN (2, restrict_bij)] 1); +by (res_inst_tac [("x","f``a")] exI 1); +by (fast_tac (AC_cs addSEs [inj_is_fun RS fun_is_rel RS image_subset]) 1); +val lepoll_imp_eqpoll_subset = result(); + +(* ********************************************************************** *) +(* Some other lemmas *) +(* ********************************************************************** *) + +goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n"; +by (resolve_tac [eqpoll_trans] 1); +by (eresolve_tac [nat_into_Ord RS well_ord_Memrel RS ( + nat_into_Ord RS well_ord_Memrel RSN (2, + well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1 + THEN (assume_tac 1)); +by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac (AC_ss addsimps [cadd_def, eqpoll_refl]) 1); +val nat_sum_eqpoll_sum = result(); + +val eqpoll_ordertype = + ordermap_bij RS (exI RS (eqpoll_def RS (def_imp_iff RS iffD2))); + +goalw thy [lesspoll_def] + "!!a. [| b lesspoll a; well_ord(a,r); well_ord(b,s) |] \ +\ ==> ordertype(b,s) < ordertype(a,r)"; +by (forw_inst_tac [("A2","b")] + ([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1 + THEN REPEAT (assume_tac 1)); +by (eresolve_tac [disjE] 1); +by (eresolve_tac [ltI] 1); +by (eresolve_tac [Ord_ordertype] 1); +by (eresolve_tac [disjE] 1); +by (REPEAT (eresolve_tac [conjE,notE] 1)); +by (resolve_tac [exI RS (eqpoll_def RS (def_imp_iff RS iffD2))] 1); +by (eresolve_tac [ordermap_bij RS comp_bij] 1); +by (eresolve_tac [ssubst] 1); +by (eresolve_tac [ordermap_bij RS bij_converse_bij] 1); +by (REPEAT (eresolve_tac [conjE,notE] 1)); +by (eresolve_tac [eqpollI] 1); +by (resolve_tac [Ord_ordertype RSN (2, OrdmemD RS subset_imp_lepoll) RSN (2, + eqpoll_ordertype RS eqpoll_imp_lepoll RS ( + eqpoll_ordertype RS eqpoll_sym RS eqpoll_imp_lepoll RSN (3, + lepoll_trans RS lepoll_trans)))] 1 + THEN (REPEAT (assume_tac 1))); +val lesspoll_ordertype_lt = result(); + +goalw thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B"; +by (fast_tac AC_cs 1); +val lesspoll_imp_lepoll = result(); + +goalw thy [lepoll_def] + "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)"; +by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1); +val lepoll_well_ord = result(); + +goal thy "!!A a. [| A lesspoll a; Ord(a) |] ==> EX b. b A lesspoll B | A eqpoll B"; +by (fast_tac (AC_cs addSIs [eqpollI] addSEs [eqpollE]) 1); +val lepoll_iff_leqpoll = result(); + +goal thy "!!A. [| A lepoll a; Ord(a) |] ==> EX b. b le a & A eqpoll b"; +by (eresolve_tac [lepoll_iff_leqpoll RS iffD1 RS disjE] 1); +by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] addSIs [leI]) 1); +by (fast_tac (AC_cs addSIs [le_refl]) 1); +val lepoll_imp_ex_le_eqpoll = result(); + +goal thy "!!m. [| m le n; n:nat |] ==> m:nat"; +by (fast_tac (AC_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))] + addSEs [ltE]) 1); +val le_in_nat = result(); + +goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)"; +by (REPEAT (eresolve_tac [bexE] 1)); +by (REPEAT (dresolve_tac [eqpoll_imp_lepoll] 1)); +by (dresolve_tac [sum_lepoll_mono] 1 THEN (assume_tac 1)); +by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2, + Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1 + THEN (REPEAT (assume_tac 1))); +by (forw_inst_tac [("n2","na")] + (add_type RS nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll)) 1 + THEN (REPEAT (assume_tac 1))); +by (fast_tac (AC_cs addSEs [add_type RSN (2, le_in_nat)]) 1); +val Finite_Un = result(); + +goal thy "A <= B Un (A - B)"; +by (fast_tac AC_cs 1); +val subset_Un_Diff = result(); + +goalw thy [lesspoll_def] "!!a. [| Card(a); i i lesspoll a"; +by (dresolve_tac [Card_iff_initial RS iffD1] 1); +by (fast_tac (AC_cs addSEs [leI RS le_imp_lepoll]) 1); +val lt_Card_imp_lesspoll = result(); + +(* ********************************************************************** *) +(* Diff_lesspoll_eqpoll_Card *) +(* ********************************************************************** *) + +goal thy "!!A B. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a; \ +\ A-B lesspoll a |] ==> P"; +by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, + Card_is_Ord, conjE] 1)); +by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper1_le))) 1 + THEN (assume_tac 1)); +by (forw_inst_tac [("j","xa")] (lt_Ord RS (lt_Ord RSN (2, Un_upper2_le))) 1 + THEN (assume_tac 1)); +by (dresolve_tac [Un_least_lt] 1 THEN (assume_tac 1)); +by (dresolve_tac [le_imp_lepoll RSN + (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 + THEN (assume_tac 1)); +by (dresolve_tac [le_imp_lepoll RSN + (2, eqpoll_imp_lepoll RS lepoll_trans)] 1 + THEN (assume_tac 1)); +by (res_inst_tac [("Q","Finite(x Un xa)")] (excluded_middle RS disjE) 1); +by (dresolve_tac [[lepoll_Finite, lepoll_Finite] MRS Finite_Un] 2 + THEN (REPEAT (assume_tac 2))); +by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2); +by (fast_tac (AC_cs + addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2); +by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 + THEN (REPEAT (assume_tac 1))); +by (fast_tac (AC_cs addSEs [ltE, Ord_in_Ord]) 1); +by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN + (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1 + THEN (TRYALL assume_tac)); +by (fast_tac (AC_cs addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1); +val Diff_lesspoll_eqpoll_Card_lemma = result(); + +goal thy "!!A. [| A eqpoll a; ~Finite(a); Card(a); B lesspoll a |] \ +\ ==> A - B eqpoll a"; +by (resolve_tac [swap] 1 THEN (fast_tac AC_cs 1)); +by (resolve_tac [Diff_lesspoll_eqpoll_Card_lemma] 1 THEN (REPEAT (assume_tac 1))); +by (fast_tac (AC_cs addSIs [lesspoll_def RS def_imp_iff RS iffD2, + subset_imp_lepoll RS (eqpoll_imp_lepoll RSN (2, lepoll_trans))]) 1); +val Diff_lesspoll_eqpoll_Card = result(); + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/Cardinal_aux.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/Cardinal_aux.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +Cardinal_aux = Cardinal + OrderType + CardinalArith + first \ No newline at end of file diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/DC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/DC.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,613 @@ +(* Title: ZF/AC/DC.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proofs concerning the Axiom of Dependent Choice +*) + +open DC; + +(* ********************************************************************** *) +(* DC ==> DC(omega) *) +(* *) +(* The scheme of the proof: *) +(* *) +(* Assume DC. Let R and x satisfy the premise of DC(omega). *) +(* *) +(* Define XX and RR as follows: *) +(* *) +(* XX = (UN n:nat. {f:n->X. ALL k:n. : 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) *) +(* *) +(* Thence *) +(* *) +(* ff = {. n:nat} *) +(* *) +(* is the desired function. *) +(* *) +(* ********************************************************************** *) + +goal thy "{z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)} <= XX*XX"; +by (fast_tac AC_cs 1); +val lemma1_1 = result(); + +goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. : R) \ +\ ==> {z: (UN n:nat. {f:n->X. ALL k:n. : R}) * \ +\ (UN n:nat. {f:n->X. ALL k:n. : R}). \ +\ domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)} ~= 0"; +by (eresolve_tac [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); +by (eresolve_tac [bexE] 1); +by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); +by (resolve_tac [CollectI] 1); +by (resolve_tac [SigmaI] 1); +by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, empty_fun]) 1); +by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type] + addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, + apply_singleton_eq, image_0])) 1); +by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing, + [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); +val lemma1_2 = result(); + +goal thy "!!X. ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. : R) \ +\ ==> range({z: (UN n:nat. {f:n->X. ALL k:n. : R}) * \ +\ (UN n:nat. {f:n->X. ALL k:n. : R}). \ +\ domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)}) \ +\ <= domain({z: (UN n:nat. {f:n->X. ALL k:n. : R}) * \ +\ (UN n:nat. {f:n->X. ALL k:n. : R}). \ +\ domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)})"; +by (resolve_tac [range_subset_domain] 1); +by (resolve_tac [subsetI] 2); +by (eresolve_tac [CollectD1] 2); +by (eresolve_tac [UN_E] 1); +by (eresolve_tac [CollectE] 1); +by (dresolve_tac [fun_is_rel RS image_subset RS PowI RSN (2, bspec)] 1 + THEN (assume_tac 1)); +by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] + MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 + THEN REPEAT (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (res_inst_tac [("x","cons(, g)")] exI 1); +by (resolve_tac [CollectI] 1); +by (resolve_tac [SigmaI] 1); +by (fast_tac AC_cs 1); +by (resolve_tac [UN_I] 1); +by (eresolve_tac [nat_succI] 1); +by (resolve_tac [CollectI] 1); +by (eresolve_tac [cons_fun_type2] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [succE] addss (AC_ss + addsimps [cons_image_n, cons_val_n, cons_image_k, cons_val_k])) 1); +by (asm_full_simp_tac (AC_ss + addsimps [domain_cons, domain_of_fun, succ_def, restrict_cons_eq]) 1); +val lemma1_3 = result(); + +goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +\ RR = {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ +\ ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. : R) \ +\ |] ==> RR <= XX*XX & RR ~= 0 & range(RR) <= domain(RR)"; +by (fast_tac (AC_cs addSIs [lemma1_1] addSEs [lemma1_2, lemma1_3]) 1); +val lemma1 = result(); + +goal thy "!!f. [| : {z:XX*XX. \ +\ domain(snd(z))=succ(domain(fst(z))) & Q(z)}; \ +\ XX = (UN n:nat. {f:n->X. ALL k:n. : R}); f:k->X \ +\ |] ==> g:succ(k)->X"; +by (eresolve_tac [CollectE] 1); +by (dresolve_tac [SigmaD2] 1); +by (hyp_subst_tac 1); +by (eresolve_tac [UN_E] 1); +by (eresolve_tac [CollectE] 1); +by (asm_full_simp_tac AC_ss 1); +by (dresolve_tac [domain_of_fun] 1); +by (eresolve_tac [conjE] 1); +by (forward_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); +by (fast_tac AC_cs 1); +val lemma2_1 = result(); + +goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +\ ALL n:nat. : \ +\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ +\ f: nat -> XX; n:nat \ +\ |] ==> EX k:nat. f`succ(n) : k -> X & n:k \ +\ & : R"; +by (eresolve_tac [nat_induct] 1); +by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); +by (dresolve_tac [nat_0I RSN (2, bspec)] 1); +by (asm_full_simp_tac AC_ss 1); +by (eresolve_tac [UN_E] 1); +by (eresolve_tac [CollectE] 1); +by (resolve_tac [bexI] 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSEs [nat_0_le RS leE, ltD, ltD RSN (2, bspec)] + addEs [sym RS trans RS succ_neq_0, domain_of_fun]) 1); +by (eresolve_tac [bexE] 1); +by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); +by (eresolve_tac [conjE] 1); +by (dresolve_tac [lemma2_1] 1 THEN REPEAT (assume_tac 1)); +by (hyp_subst_tac 1); +by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 + THEN (assume_tac 1)); +by (eresolve_tac [UN_E] 1); +by (eresolve_tac [CollectE] 1); +by (dresolve_tac [[domain_of_fun RS sym, domain_of_fun] MRS trans] 1 + THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [nat_succI, nat_into_Ord RS succ_in_succ] + addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); +val lemma2 = result(); + +goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +\ ALL n:nat. : \ +\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ +\ f: nat -> XX; n:nat \ +\ |] ==> ALL x:n. f`succ(n)`x = f`succ(x)`x"; +by (eresolve_tac [nat_induct] 1); +by (fast_tac AC_cs 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [succE] 1); +by (resolve_tac [restrict_eq_imp_val_eq] 1); +by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac AC_ss 1); +by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSDs [domain_of_fun]) 1); +by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); +by (eresolve_tac [sym RS trans RS sym] 1); +by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1); +by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac AC_ss 1); +by (dresolve_tac [lemma2] 1 THEN REPEAT (assume_tac 1)); +by (fast_tac (FOL_cs addSDs [domain_of_fun] + addSEs [bexE, nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); +val lemma3_1 = result(); + +goal thy "!!n. ALL x:n. f`succ(n)`x = f`succ(x)`x \ +\ ==> {f`succ(x)`x. x:n} = {f`succ(n)`x. x:n}"; +by (asm_full_simp_tac AC_ss 1); +val lemma3_2 = result(); + +goal thy "!!X. [| XX = (UN n:nat. {f:n->X. ALL k:n. : R}); \ +\ ALL n:nat. : \ +\ {z:XX*XX. domain(snd(z))=succ(domain(fst(z))) \ +\ & restrict(snd(z), domain(fst(z))) = fst(z)}; \ +\ f: nat -> XX; n:nat \ +\ |] ==> (lam x:nat. f`succ(x)`x) `` n = f`succ(n)``n"; +by (eresolve_tac [natE] 1); +by (asm_full_simp_tac (AC_ss addsimps [image_0]) 1); +by (resolve_tac [image_lam RS ssubst] 1); +by (fast_tac (AC_cs addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); +by (resolve_tac [lemma3_1 RS lemma3_2 RS ssubst] 1 + THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSEs [nat_succI]) 1); +by (dresolve_tac [nat_succI RSN (4, lemma2)] 1 + THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSEs [image_fun RS sym, + nat_into_Ord RSN (2, OrdmemD)]) 1); +val lemma3 = result(); + +goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C"; +by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [apply_type]) 1); +val fun_type_gen = result(); + +goalw thy [DC_def, DC0_def] "!!Z. DC0 ==> DC(nat)"; +by (REPEAT (resolve_tac [allI, impI] 1)); +by (REPEAT (eresolve_tac [conjE, allE] 1)); +by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 + THEN (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (res_inst_tac [("x","lam n:nat. f`succ(n)`n")] bexI 1); +by (fast_tac (AC_cs addSIs [lam_type] addSDs [refl RS lemma2] + addSEs [fun_type_gen, apply_type]) 2); +by (resolve_tac [oallI] 1); +by (forward_tac [ltD RSN (3, refl RS lemma2)] 1 + THEN assume_tac 2); +by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); +by (eresolve_tac [ltD RSN (3, refl RS lemma3) RS ssubst] 1 + THEN assume_tac 2); +by (fast_tac (AC_cs addSEs [fun_type_gen]) 1); +by (fast_tac (AC_cs addss AC_ss) 1); +qed "DC0_DC_nat"; + +(* ********************************************************************** *) +(* DC(omega) ==> DC *) +(* *) +(* The scheme of the proof: *) +(* *) +(* Assume DC(omega). Let R and x satisfy the premise of DC. *) +(* *) +(* Define XX and RR as follows: *) +(* *) +(* XX = (UN n:nat. *) +(* {f:succ(n)->domain(R). ALL k:n. : R}) *) +(* RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) *) +(* & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | *) +(* (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) *) +(* & (ALL f:fst(z). restrict(g, domain(f)) = f)) & *) +(* snd(z)={<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 *) +(* *) +(* Thence *) +(* *) +(* ff = {. n:nat} *) +(* *) +(* is the desired function. *) +(* *) +(* ********************************************************************** *) + +goalw thy [lesspoll_def, Finite_def] + "!!A. A lesspoll nat ==> Finite(A)"; +by (fast_tac (AC_cs addSDs [ltD, lepoll_imp_ex_le_eqpoll] + addSIs [Ord_nat]) 1); +val lesspoll_nat_is_Finite = result(); + +goal thy "!!n. n:nat ==> ALL A. (A eqpoll n & A <= X) --> A : Fin(X)"; +by (eresolve_tac [nat_induct] 1); +by (resolve_tac [allI] 1); +by (fast_tac (AC_cs addSIs [Fin.emptyI] + addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [conjE] 1); +by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 + THEN (assume_tac 1)); +by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); +by (eresolve_tac [allE] 1); +by (eresolve_tac [impE] 1); +by (fast_tac AC_cs 1); +by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); +by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac (AC_ss addsimps [cons_Diff]) 1); +val Finite_Fin_lemma = result(); + +goalw thy [Finite_def] "!!A. [| Finite(A); A <= X |] ==> A : Fin(X)"; +by (eresolve_tac [bexE] 1); +by (dresolve_tac [Finite_Fin_lemma] 1); +by (eresolve_tac [allE] 1); +by (eresolve_tac [impE] 1); +by (assume_tac 2); +by (fast_tac AC_cs 1); +val Finite_Fin = result(); + +goal thy "!!x. x: X ==> {<0,x>}: (UN n:nat. \ +\ {f:succ(n)->X. ALL k:n. : R})"; +by (fast_tac (AC_cs addSIs [nat_0I RS UN_I, singleton_fun RS Pi_type] + addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing, + apply_singleton_eq])) 1); +val singleton_in_funs = result(); + +goal thy + "!!X. [| XX = (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ RR = {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ +\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ +\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ +\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ +\ range(R) <= domain(R); x:domain(R) \ +\ |] ==> RR <= Pow(XX)*XX & \ +\ (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. :RR))"; +by (resolve_tac [conjI] 1); +by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE] + addSIs [subsetI, SigmaI]) 1); +by (resolve_tac [ballI] 1); +by (resolve_tac [impI] 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 (fast_tac (AC_cs addss AC_ss) 2); +by (fast_tac (FOL_cs addSEs [CollectE, singleton_in_funs] + addSIs [SigmaI] addIs [bexI] addss AC_ss) 1); +val lemma1 = result(); + +goal thy "!!f. [| f:nat->X; n:nat |] ==> \ +\ (UN x:f``succ(n). P(x)) = P(f`n) Un (UN x:f``n. P(x))"; +by (asm_full_simp_tac (AC_ss + addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), + [nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); +val UN_image_succ_eq = result(); + +goal thy "!!f. [| (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)"; +by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq]) 1); +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val UN_image_succ_eq_succ = result(); + +goal thy "!!f. [| f: (UN n:nat. {g:succ(n) -> D. P(g, n)}); \ +\ domain(f)=succ(x); x=y |] ==> f`y : D"; +by (fast_tac (AC_cs addEs [apply_type] + addSDs [[sym, domain_of_fun] MRS trans]) 1); +val apply_UN_type = result(); + +goal thy "!!f. [| f : nat -> X; n:nat |] ==> f``succ(n) = cons(f`n, f``n)"; +by (asm_full_simp_tac (AC_ss + addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); +val image_fun_succ = result(); + +goal thy "!!f. [| domain(f`n) = succ(u); f : nat -> (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ u=k; n:nat \ +\ |] ==> f`n : succ(k) -> domain(R)"; +by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addEs [UN_E, domain_eq_imp_fun_type]) 1); +val f_n_type = result(); + +goal thy "!!f. [| f : nat -> (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ domain(f`n) = succ(k); n:nat \ +\ |] ==> ALL i:k. : R"; +by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (eresolve_tac [UN_E] 1); +by (eresolve_tac [CollectE] 1); +by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); +by (dresolve_tac [succ_eqD] 1); +by (asm_full_simp_tac AC_ss 1); +val f_n_pairs_in_R = result(); + +goalw thy [restrict_def] + "!!f. [| restrict(f, domain(x))=x; f:n->X; domain(x) <= n \ +\ |] ==> restrict(cons(, f), domain(x)) = x"; +by (eresolve_tac [sym RS trans RS sym] 1); +by (resolve_tac [fun_extension] 1); +by (fast_tac (AC_cs addSIs [lam_type]) 1); +by (fast_tac (AC_cs addSIs [lam_type]) 1); +by (asm_full_simp_tac (AC_ss addsimps [subsetD RS cons_val_k]) 1); +val restrict_cons_eq_restrict = result(); + +goal thy "!!f. [| ALL x:f``n. restrict(f`n, domain(x))=x; \ +\ f : nat -> (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ n:nat; domain(f`n) = succ(n); \ +\ (UN x:f``n. domain(x)) <= n |] \ +\ ==> ALL x:f``succ(n). restrict(cons(, f`n), domain(x))=x"; +by (resolve_tac [ballI] 1); +by (asm_full_simp_tac (AC_ss addsimps [image_fun_succ]) 1); +by (dresolve_tac [f_n_type] 1 THEN REPEAT (ares_tac [refl] 1)); +by (eresolve_tac [consE] 1); +by (asm_full_simp_tac (AC_ss addsimps [domain_of_fun, restrict_cons_eq]) 1); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [restrict_cons_eq_restrict]) 1); +val all_in_image_restrict_eq = result(); + +goal thy "!!X. [| ALL b : \ +\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ +\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f)) | \ +\ (~ (EX g:XX. domain(g)=succ(UN f:fst(z). domain(f)) \ +\ & (ALL f:fst(z). restrict(g, domain(f)) = f)) & snd(z)={<0,x>})}; \ +\ XX = (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ f: nat -> XX; range(R) <= domain(R); x:domain(R) \ +\ |] ==> ALL b : \ +\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ +\ & (UN f:fst(z). domain(f)) = b \ +\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}"; +by (resolve_tac [oallI] 1); +by (dresolve_tac [ltD] 1); +by (eresolve_tac [nat_induct] 1); +by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); +by (REPEAT (eresolve_tac [CollectE, conjE, disjE] 1)); +by (asm_full_simp_tac (AC_ss + addsimps [image_0, singleton_fun RS domain_of_fun, + [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1); +by (asm_full_simp_tac (AC_ss + addsimps [image_0, singleton_fun RS domain_of_fun, + [lepoll_refl, succI1] MRS lepoll_1_is_sing, singleton_in_funs]) 1); +by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 + THEN (assume_tac 1)); +by (REPEAT (eresolve_tac [conjE, CollectE, disjE] 1)); +by (fast_tac (AC_cs addSEs [trans, subst_context] + addSIs [UN_image_succ_eq_succ] addss AC_ss) 1); +by (eresolve_tac [conjE] 1); +by (eresolve_tac [notE] 1); +by (hyp_subst_tac 1); +by (asm_full_simp_tac (AC_ss addsimps [UN_image_succ_eq_succ]) 1); +by (eresolve_tac [conjE] 1); +by (dresolve_tac [apply_UN_type] 1 THEN REPEAT (assume_tac 1)); +by (eresolve_tac [domainE] 1); +by (eresolve_tac [domainE] 1); +by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1)); +by (res_inst_tac [("x","cons(, f`xa)")] bexI 1); +by (fast_tac (FOL_cs + addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, + subst_context, all_in_image_restrict_eq, trans, equalityD1]) 1); +by (resolve_tac [UN_I] 1); +by (eresolve_tac [nat_succI] 1); +by (resolve_tac [CollectI] 1); +by (fast_tac (AC_cs addSEs [cons_fun_type2]) 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [succE] 1); +by (asm_full_simp_tac (AC_ss addsimps [cons_val_n, cons_val_k]) 1); +by (dresolve_tac [domain_of_fun RSN (2, f_n_pairs_in_R)] 1 + THEN REPEAT (assume_tac 1)); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac (AC_ss + addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 1); +val simplify_recursion = result(); + +goal thy "!!X. [| XX = (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ ALL b : \ +\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ +\ & (UN f:fst(z). domain(f)) = b \ +\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ +\ f: nat -> XX; range(R) <= domain(R); x:domain(R); n:nat \ +\ |] ==> f`n : succ(n) -> domain(R) \ +\ & (ALL i:n. :R)"; +by (dresolve_tac [ospec] 1); +by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); +by (eresolve_tac [CollectE] 1); +by (asm_full_simp_tac AC_ss 1); +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs + addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); +by (fast_tac (AC_cs addSEs [nat_succI, succI2, f_n_pairs_in_R RS bspec, + subst_context, trans]) 1); +val lemma2 = result(); + +goal thy "!!n. [| XX = (UN n:nat. \ +\ {f:succ(n)->domain(R). ALL k:n. : R}); \ +\ ALL b : \ +\ {z:Fin(XX)*XX. (domain(snd(z))=succ(UN f:fst(z). domain(f)) \ +\ & (UN f:fst(z). domain(f)) = b \ +\ & (ALL f:fst(z). restrict(snd(z), domain(f)) = f))}; \ +\ f : nat -> XX; n:nat; range(R) <= domain(R); x: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)); +by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 + THEN (assume_tac 1)); +by (asm_full_simp_tac AC_ss 1); +by (REPEAT (eresolve_tac [conjE] 1)); +by (eresolve_tac [ballE] 1); +by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); +by (fast_tac (AC_cs addSEs [ssubst]) 1); +by (asm_full_simp_tac (AC_ss + addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); +val lemma3 = result(); + +goalw thy [DC_def, DC0_def] "!!Z. DC(nat) ==> DC0"; +by (REPEAT (resolve_tac [allI, impI] 1)); +by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); +by (eresolve_tac [[refl, refl] MRS lemma1 RSN (2, impE)] 1 + THEN REPEAT (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (dresolve_tac [refl RSN (2, simplify_recursion)] 1 + THEN REPEAT (assume_tac 1)); +by (res_inst_tac [("x","lam n:nat. f`n`n")] bexI 1); +by (resolve_tac [lam_type] 2); +by (eresolve_tac [[refl RS lemma2 RS conjunct1, succI1] MRS apply_type] 2 + THEN REPEAT (assume_tac 2)); +by (resolve_tac [ballI] 1); +by (forward_tac [refl RS (nat_succI RSN (6, lemma2)) RS conjunct2] 1 + THEN REPEAT (assume_tac 1)); +by (dresolve_tac [refl RS lemma3] 1 THEN REPEAT (assume_tac 1)); +by (asm_full_simp_tac (AC_ss addsimps [nat_succI]) 1); +qed "DC_nat_DC0"; + +(* ********************************************************************** *) +(* ALL K. Card(K) --> DC(K) ==> WO3 *) +(* ********************************************************************** *) + +goalw thy [lesspoll_def] + "!!A. [| ~ A lesspoll B; C lesspoll B |] ==> A - C ~= 0"; +by (fast_tac (AC_cs addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] + addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); +val lemma1 = result(); + +val [f_type, Ord_a, not_eq] = goalw thy [inj_def] + "[| f:a->X; Ord(a); (!!b c. [| b f`b~=f`c) \ +\ |] ==> f: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 + THEN (assume_tac 1)); +by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); +by (REPEAT (fast_tac (AC_cs addDs [not_eq, not_eq RS not_sym]) 1)); +val fun_Ord_inj = result(); + +goal thy "!!a. [| f:X->Y; A<=X; a:A |] ==> f`a : f``A"; +by (fast_tac (AC_cs addSEs [image_fun RS ssubst]) 1); +val value_in_image = result(); + +goalw thy [DC_def, WO3_def] + "!!Z. ALL K. Card(K) --> DC(K) ==> WO3"; +by (resolve_tac [allI] 1); +by (excluded_middle_tac "A lesspoll Hartog(A)" 1); +by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] + addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); +by (REPEAT (eresolve_tac [allE, impE] 1)); +by (resolve_tac [Card_Hartog] 1); +by (eres_inst_tac [("x","A")] allE 1); +by (eres_inst_tac [("x","{z:Pow(A)*A . fst(z) \ +\ lesspoll Hartog(A) & snd(z) ~: fst(z)}")] allE 1); +by (asm_full_simp_tac AC_ss 1); +by (eresolve_tac [impE] 1); +by (fast_tac (AC_cs addEs [lemma1 RS not_emptyE]) 1); +by (eresolve_tac [bexE] 1); +by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) + RS (HartogI RS notE)] 1); +by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); +by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, + ltD RSN (3, value_in_image))] 1 + THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)] + addEs [subst]) 1); +qed "DC_WO3"; + +(* ********************************************************************** *) +(* WO1 ==> ALL K. Card(K) --> DC(K) *) +(* ********************************************************************** *) + +goal thy + "!!a. [| Ord(a); b:a |] ==> (lam x:a. P(x))``b = (lam x:b. P(x))``b"; +by (resolve_tac [images_eq] 1); +by (REPEAT (fast_tac (AC_cs addSEs [RepFunI, OrdmemD] + addSIs [lam_type]) 2)); +by (resolve_tac [ballI] 1); +by (dresolve_tac [OrdmemD RS subsetD] 1 + THEN REPEAT (assume_tac 1)); +by (asm_full_simp_tac AC_ss 1); +val lam_images_eq = result(); + +goalw thy [lesspoll_def] "!!K. [| Card(K); b:K |] ==> b lesspoll K"; +by (asm_full_simp_tac (AC_ss addsimps [Card_iff_initial]) 1); +by (fast_tac (AC_cs addSIs [le_imp_lepoll, ltI, leI]) 1); +val in_Card_imp_lesspoll = result(); + +goal thy "(lam b:a. P(b)) : a -> {P(b). b:a}"; +by (fast_tac (AC_cs addSIs [lam_type, RepFunI]) 1); +val lam_type_RepFun = result(); + +goal thy "!!Z. [| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. : R); \ +\ b:a; Z:Pow(X); Z lesspoll a |] \ +\ ==> {x:X. : R} ~= 0"; +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSIs [not_emptyI]) 1); +val lemma_ = result(); + +goal thy "!!K. [| Card(K); well_ord(X,Q); \ +\ ALL Y:Pow(X). Y lesspoll K --> (EX x: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); +by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 + THEN REPEAT (assume_tac 1)); +by (resolve_tac [impI] 1); +by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); +by (eresolve_tac [the_first_in] 1); +by (fast_tac AC_cs 1); +by (asm_full_simp_tac (AC_ss + addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); +by (eresolve_tac [lemma_] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [RepFunE, impE, notE] + addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); +by (fast_tac (AC_cs addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] + MRS lepoll_lesspoll_lesspoll]) 1); +val lemma = result(); + +goalw thy [DC_def, WO1_def] + "!!Z. WO1 ==> ALL 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 (resolve_tac [lam_type] 2); +by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); +by (asm_full_simp_tac (AC_ss + addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); +by (fast_tac (AC_cs addSEs [ltE, lemma RS CollectD2]) 1); +qed" WO1_DC_Card"; + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/DC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/DC.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,28 @@ +(* Title: ZF/AC/DC.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Theory file for the proofs concernind the Axiom of Dependent Choice +*) + +DC = AC_Equiv + Hartog + first + Cardinal_aux + "DC_lemmas" + + +consts + + DC :: "i => o" + DC0 :: "o" + ff :: "[i, i, i, i] => i" + +rules + + DC_def "DC(a) == ALL X R. R<=Pow(X)*X & + (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. : R)) + --> (EX f:a->X. ALL b : 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. :R)" + + ff_def "ff(b, X, Q, R) == transrec(b, %c r. + THE x. first(x, {x:X. : R}, Q))" + +end diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/DC_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/DC_lemmas.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,146 @@ +(* Title: ZF/AC/DC_lemmas.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +More general lemmas used in the proofs concerning DC + +*) + +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); +by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1); +by (fast_tac (AC_cs addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1); +by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1)); +val RepFun_lepoll = result(); + +goalw thy [lesspoll_def] "!!n. n:nat ==> n lesspoll nat"; +by (resolve_tac [conjI] 1); +by (eresolve_tac [Ord_nat RSN (2, OrdmemD) RS subset_imp_lepoll] 1); +by (resolve_tac [notI] 1); +by (eresolve_tac [eqpollE] 1); +by (resolve_tac [succ_lepoll_natE] 1 THEN (assume_tac 2)); +by (eresolve_tac [nat_succI RS (Ord_nat RSN (2, OrdmemD) RS + subset_imp_lepoll) RS lepoll_trans] 1 + THEN (assume_tac 1)); +val n_lesspoll_nat = result(); + +goalw thy [lepoll_def] + "!!f. [| 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); +by (res_inst_tac [("d","%z. f`z")] lam_injective 1); +by (fast_tac (AC_cs addSIs [Least_in_Ord, apply_equality]) 1); +by (fast_tac (AC_cs addSEs [Ord_in_Ord] addSIs [LeastI, apply_equality]) 1); +val image_Ord_lepoll = result(); + +val apply_singleton_eq = [singletonI, singleton_fun] MRS apply_equality; + +goal thy "restrict(f, 0) = 0"; +by (resolve_tac [singleton_iff RS iffD1] 1); +by (resolve_tac [Pi_empty1 RS subst] 1); +by (fast_tac (AC_cs addSIs [restrict_type]) 1); +val restrict_0 = result(); + +val [major, minor] = goal thy + "[| (!!g. g:X ==> EX u. :R); R<=X*X \ +\ |] ==> range(R) <= domain(R)"; +by (resolve_tac [subsetI] 1); +by (eresolve_tac [rangeE] 1); +by (dresolve_tac [minor RS subsetD RS SigmaD2 RS major] 1); +by (fast_tac AC_cs 1); +val range_subset_domain = result(); + +goal thy "domain({}) = {x}"; +by (fast_tac (AC_cs addSIs [equalityI, singletonI] addSEs [singletonE]) 1); +val domain_sing = result(); + +val prems = goal thy "!!k. k:n ==> k~=n"; +by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); +val mem_not_eq = result(); + +goal thy "!!a. [| a:B; A<=B |] ==> cons(a, A) <= B"; +by (fast_tac AC_cs 1); +val cons_subset = result(); + +goal thy "!!g. g:n->X ==> cons(, g) : succ(n) -> cons(x, X)"; +by (resolve_tac [Pi_iff_old RS iffD2] 1); +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs addSIs [cons_subset, succI1] + addEs [fun_is_rel RS subset_trans RS subsetD, succI2]) 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [succE] 1); +by (fast_tac (AC_cs addDs [domain_of_fun, domainI] addSEs [mem_irrefl]) 1); +by (fast_tac (AC_cs addDs [fun_unique_Pair] addSEs [mem_irrefl]) 1); +val cons_fun_type = result(); + +goal thy "!!x. x:X ==> cons(x, X) = X"; +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val cons_eq_self = result(); + +val [g_type, x_in] = goal thy "[| g:n->X; x:X |] ==> cons(, g) : succ(n) -> X"; +by (resolve_tac [x_in RS cons_eq_self RS subst] 1); +by (resolve_tac [g_type RS cons_fun_type] 1); +val cons_fun_type2 = result(); + +goal thy "!!n. n: nat ==> cons(, g)``n = g``n"; +by (fast_tac (AC_cs addSIs [equalityI] addSEs [mem_irrefl]) 1); +val cons_image_n = result(); + +goal thy "!!n. g:n->X ==> cons(, g)`n = x"; +by (fast_tac (AC_cs addSIs [apply_equality] addSEs [cons_fun_type]) 1); +val cons_val_n = result(); + +goal thy "!!k. k : n ==> cons(, g)``k = g``k"; +by (fast_tac (AC_cs addSIs [equalityI] addEs [mem_asym]) 1); +val cons_image_k = result(); + +goal thy "!!k. [| k:n; g:n->X |] ==> cons(, g)`k = g`k"; +by (fast_tac (AC_cs addSIs [apply_equality, consI2] addSEs [cons_fun_type, apply_Pair]) 1); +val cons_val_k = result(); + +goal thy "!!f. domain(f)=x ==> domain(cons(, f)) = succ(x)"; +by (asm_full_simp_tac (AC_ss addsimps [domain_cons, succ_def]) 1); +val domain_cons_eq_succ = result(); + +goalw thy [restrict_def] "!!g. g:n->X ==> restrict(cons(, g), n)=g"; +by (resolve_tac [fun_extension] 1); +by (resolve_tac [lam_type] 1); +by (eresolve_tac [cons_fun_type RS apply_type] 1); +by (eresolve_tac [succI2] 1); +by (assume_tac 1); +by (asm_full_simp_tac (AC_ss addsimps [cons_val_k]) 1); +val restrict_cons_eq = result(); + +goal thy "!!k. [| Ord(k); i:k |] ==> succ(i) : succ(k)"; +by (resolve_tac [Ord_linear RS disjE] 1 THEN (assume_tac 3)); +by (REPEAT (fast_tac (AC_cs addSIs [Ord_succ] + addEs [Ord_in_Ord, mem_irrefl, mem_asym] + addSDs [succ_inject]) 1)); +val succ_in_succ = result(); + +goalw thy [restrict_def] + "!!f. [| restrict(f, domain(g)) = g; x: domain(g) |] ==> f`x = g`x"; +by (eresolve_tac [subst] 1); +by (asm_full_simp_tac AC_ss 1); +val restrict_eq_imp_val_eq = result(); + +goal thy "!!a. succ(a) = succ(b) ==> a = b"; +by (eresolve_tac [equalityE] 1); +by (resolve_tac [equalityI] 1); +by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1); +by (fast_tac (AC_cs addSEs [mem_irrefl] addEs [mem_asym]) 1); +val succ_eqD = result(); + +goal thy "!!n. n:nat ==> 0:succ(n)"; +by (fast_tac (AC_cs addSDs [[Ord_0, nat_into_Ord] MRS Ord_linear]) 1); +val nat_0_in_succ = result(); + +goal thy "!!f. [| domain(f)=A; f:B->C |] ==> f:A->C"; +by (forward_tac [domain_of_fun] 1); +by (fast_tac AC_cs 1); +val domain_eq_imp_fun_type = result(); + +goal thy "!!R. [| R <= A * B; R ~= 0 |] ==> EX x. x:domain(R)"; +by (fast_tac (AC_cs addSEs [not_emptyE]) 1); +val ex_in_domain = result(); + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/DC_lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/DC_lemmas.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,4 @@ +(*Dummy theory to document dependencies *) + +DC_lemmas = AC_Equiv + first + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/HH.ML --- a/src/ZF/AC/HH.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/HH.ML Tue Jul 25 17:31:53 1995 +0200 @@ -15,15 +15,15 @@ (* ********************************************************************** *) goal thy "HH(f,x,a) = \ -\ (lam y:Pow(x). if(f`y : Pow(y)-{0},f`y,{x}))` \ -\ (x - (UN b:a. HH(f,x,b)))"; +\ (let z = x - (UN b:a. HH(f,x,b)) \ +\ in if(f`z:Pow(z)-{0}, f`z, {x}))"; by (resolve_tac [HH_def RS def_transrec RS trans] 1); by (asm_full_simp_tac ZF_ss 1); val HH_def_satisfies_eq = result(); goal thy "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}"; by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); -by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1); +by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1); by (split_tac [expand_if] 1); by (fast_tac ZF_cs 1); val HH_values = result(); @@ -76,7 +76,7 @@ \ ==> HH(f,x,a) : Pow(x - (UN b: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 (AC_ss addsimps [Diff_subset RS PowI]) 1); +by (asm_full_simp_tac (AC_ss addsimps [Let_def, Diff_subset RS PowI]) 1); by (dresolve_tac [expand_if RS iffD1] 1); by (split_tac [expand_if] 1); by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); @@ -173,7 +173,7 @@ goal thy "!!f. 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}"; by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); -by (asm_full_simp_tac (AC_ss addsimps [Diff_subset RS PowI, +by (asm_full_simp_tac (AC_ss addsimps [Let_def, Diff_subset RS PowI, not_emptyI2 RS if_P]) 1); by (fast_tac AC_cs 1); val f_subset_imp_HH_subset = result(); @@ -190,7 +190,7 @@ goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); -by (asm_full_simp_tac (ZF_ss addsimps [Diff_subset RS PowI]) 1); +by (asm_full_simp_tac (ZF_ss addsimps [Let_def, Diff_subset RS PowI]) 1); by (split_tac [expand_if] 1); by (fast_tac ZF_cs 1); val HH_values2 = result(); diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/HH.thy --- a/src/ZF/AC/HH.thy Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/HH.thy Tue Jul 25 17:31:53 1995 +0200 @@ -8,7 +8,7 @@ AC15 ==> WO6 *) -HH = AC_Equiv + Hartog + WO_AC + +HH = AC_Equiv + Hartog + WO_AC + Let + consts @@ -16,8 +16,8 @@ defs - HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). - if(f`z:Pow(z)-{0}, f`z, {x}))`(x - (UN c:b. r`c)))" + 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}))" end diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/Hartog.ML --- a/src/ZF/AC/Hartog.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/Hartog.ML Tue Jul 25 17:31:53 1995 +0200 @@ -21,16 +21,16 @@ by (resolve_tac [conjI] 1); by (eresolve_tac [well_ord_Memrel RSN (2, subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS bij_is_inj RS well_ord_rvimage)] 1 - THEN (atac 1)); + THEN (assume_tac 1)); by (resolve_tac [subset_refl RSN (2, restrict_bij RS bij_converse_bij) RS (well_ord_Memrel RSN (2, bij_ordertype_vimage)) RS (ordertype_Memrel RSN (2, trans))] 1 - THEN (REPEAT (atac 1))); + THEN (REPEAT (assume_tac 1))); val Ord_lepoll_imp_ex_well_ord = result(); goal thy "!!X. [| Ord(a); a lepoll X |] ==> \ \ EX Y. Y<=X & (EX R. R<=X*X & ordertype(Y,R)=a)"; -by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (atac 1)); +by (dresolve_tac [Ord_lepoll_imp_ex_well_ord] 1 THEN (assume_tac 1)); by (step_tac AC_cs 1); by (REPEAT (ares_tac [exI, conjI] 1)); by (eresolve_tac [ordertype_Int] 2); @@ -42,8 +42,8 @@ \ a:{a. Z:Pow(X)*Pow(X*X), EX Y R. Z= & ordertype(Y,R)=a}"; by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE, impE] 1)); -by (atac 1); -by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (atac 1)); +by (assume_tac 1); +by (dresolve_tac [Ord_lepoll_imp_eq_ordertype] 1 THEN (assume_tac 1)); by (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1); val Ords_lepoll_set_lemma = result(); @@ -81,4 +81,4 @@ goal thy "Card(Hartog(A))"; by (fast_tac (AC_cs addSIs [CardI, Ord_Hartog] addEs [less_HartogE]) 1); -val Card_Hartog = result(); \ No newline at end of file +val Card_Hartog = result(); diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/ROOT.ML --- a/src/ZF/AC/ROOT.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/ROOT.ML Tue Jul 25 17:31:53 1995 +0200 @@ -24,17 +24,20 @@ time_use "AC/AC2_AC6.ML"; time_use "AC/AC7_AC9.ML"; -time_use_thy "AC/WO1_AC1"; +time_use_thy "AC/WO1_AC"; time_use_thy "AC/AC1_WO2"; time_use "AC/AC10_AC15.ML"; time_use_thy "AC/AC15_WO6"; -(* AC16 to add *) +time_use_thy "AC/WO2_AC16"; +time_use_thy "AC/AC16_WO4"; time_use "AC/AC1_AC17.ML"; time_use_thy "AC/AC17_AC1"; time_use_thy "AC/AC18_AC19"; +time_use_thy "AC/DC"; + writeln"END: Root file for ZF/AC"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_AC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_AC.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,120 @@ +(* Title: ZF/AC/WO1_AC.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proofs of WO1 ==> AC1 and WO1 ==> AC10(n) for n >= 1 + +The latter proof is referred to as clear by the Rubins. +However it seems to be quite complicated. +The formal proof presented below is a mechanisation of the proof +by Lawrence C. Paulson which is the following: + +Assume WO1. Let s be a set of infinite sets. + +Suppose x: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.) + +So there is a partition of x into 2-element sets, namely + + {{h(Inl(i)), h(Inr(i))} . i: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 +have AC10(2). + +*) + +open WO1_AC; + +(* ********************************************************************** *) +(* WO1 ==> AC1 *) +(* ********************************************************************** *) + +goalw thy [AC1_def, WO1_def] "!!Z. WO1 ==> AC1"; +by (fast_tac (AC_cs addSEs [ex_choice_fun]) 1); +qed "WO1_AC1"; + +(* ********************************************************************** *) +(* WO1 ==> AC10(n) (n >= 1) *) +(* ********************************************************************** *) + +goalw thy [WO1_def] "!!A. [| 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); +by (eresolve_tac [exE] 1); +by (dresolve_tac [ex_choice_fun] 1); +by (fast_tac (AC_cs addEs [RepFunE, sym RS equals0D]) 1); +by (eresolve_tac [exE] 1); +by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSDs [RepFunI RSN (2, apply_type)] + addSEs [CollectD2]) 1); +val lemma1 = result(); + +goalw thy [WO1_def] "!!A. [| ~Finite(B); WO1 |] ==> |B| + |B| eqpoll B"; +by (resolve_tac [eqpoll_trans] 1); +by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 2); +by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1); +by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1); +by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1); +by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS + InfCard_cdouble_eq RS ssubst] 1); +by (resolve_tac [eqpoll_refl] 2); +by (resolve_tac [notI] 1); +by (eresolve_tac [notE] 1); +by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite] 1 + THEN (assume_tac 2)); +by (fast_tac (AC_cs addSEs [well_ord_cardinal_eqpoll]) 1); +val lemma2_1 = result(); + +goal thy "!!f. f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))"; +by (fast_tac (AC_cs addSIs [InlI, InrI] + addSEs [RepFunE, bij_is_fun RS apply_type]) 1); +val lemma2_2 = result(); + +goal thy "!!f. [| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b"; +by (resolve_tac [inj_equality] 1); +by (TRYALL (fast_tac (AC_cs addSEs [inj_is_fun RS apply_Pair] addEs [subst]))); +val lemma = result(); + +goalw thy AC_aux_defs + "!!f. f : bij(D+D, B) ==> \ +\ pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})"; +by (fast_tac (AC_cs addSEs [RepFunE, not_emptyE] + addDs [bij_is_inj RS lemma, Inl_iff RS iffD1, + Inr_iff RS iffD1, Inl_Inr_iff RS iffD1 RS FalseE, + Inr_Inl_iff RS iffD1 RS FalseE] + addSIs [InlI, InrI]) 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))"; +by (rewrite_goals_tac [succ_def]); +by (fast_tac (AC_cs addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] + addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, + le_imp_subset RS subset_imp_lepoll] + addDs [major RS bij_is_inj RS lemma, Inl_Inr_iff RS iffD1 RS FalseE] + addSEs [RepFunE, not_emptyE, mem_irrefl]) 1); +val lemma2_4 = result(); + +goalw thy [bij_def, surj_def] + "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B"; +by (fast_tac (AC_cs addSEs [inj_is_fun RS apply_type, CollectE, sumE] + addSIs [InlI, InrI, equalityI]) 1); +val lemma2_5 = result(); + +goal thy "!!A. [| WO1; ~Finite(B); 1 le n |] \ +\ ==> EX C: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 + THEN (assume_tac 1)); +by (fast_tac (FOL_cs addSIs [bexI] + addSEs [lemma2_2, lemma2_3, lemma2_4, lemma2_5]) 1); +val lemma2 = result(); + +goalw thy AC_defs "!!n. [| WO1; 1 le n |] ==> AC10(n)"; +by (fast_tac (AC_cs addSIs [lemma1] addSEs [lemma2]) 1); +qed "WO1_AC10"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_AC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_AC.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +WO1_AC = AC_Equiv + WO_AC diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_AC1.ML --- a/src/ZF/AC/WO1_AC1.ML Tue Jul 25 17:03:59 1995 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: ZF/AC/WO1_AC1.ML - ID: $Id$ - Author: Krzysztof Gr`abczewski - -The proof of WO1 ==> AC1 -*) - -open WO1_AC1; - -goalw thy [AC1_def, WO1_def] "!!Z. WO1 ==> AC1"; -by (fast_tac (AC_cs addSEs [ex_choice_fun]) 1); -result(); \ No newline at end of file diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_AC1.thy --- a/src/ZF/AC/WO1_AC1.thy Tue Jul 25 17:03:59 1995 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,3 +0,0 @@ -(*Dummy theory to document dependencies *) - -WO1_AC1 = AC_Equiv + WO_AC diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_WO6.ML --- a/src/ZF/AC/WO1_WO6.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/WO1_WO6.ML Tue Jul 25 17:31:53 1995 +0200 @@ -15,20 +15,20 @@ goalw thy WO_defs "!!Z. WO2 ==> WO3"; by (fast_tac ZF_cs 1); -result(); +qed "WO2_WO3"; (* ********************************************************************** *) goalw thy (eqpoll_def::WO_defs) "!!Z. WO3 ==> WO1"; by (fast_tac (ZF_cs addSEs [bij_is_inj RS well_ord_rvimage, well_ord_Memrel RS well_ord_subset]) 1); -result(); +qed "WO3_WO1"; (* ********************************************************************** *) goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; by (fast_tac (ZF_cs addSIs [Ord_ordertype, ordermap_bij]) 1); -result(); +qed "WO1_WO2"; (* ********************************************************************** *) @@ -57,23 +57,23 @@ by (asm_simp_tac (AC_ss addsimps [singleton_eqpoll_1 RS eqpoll_imp_lepoll, Ord_ordertype RSN (2, ordermap_bij RS bij_converse_bij RS bij_is_surj RS surj_imp_eq)]) 1); -result(); +qed "WO1_WO4"; (* ********************************************************************** *) goalw thy WO_defs "!!Z. [| m:nat; n:nat; m le n; WO4(m) |] ==> WO4(n)"; by (fast_tac (AC_cs addIs [nat_le_imp_lepoll RSN (2, lepoll_trans)]) 1); -result(); +qed "WO4_mono"; (* ********************************************************************** *) -val prems = goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; +goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; by (fast_tac ZF_cs 1); -result(); +qed "WO4_WO5"; (* ********************************************************************** *) -val prems = goalw thy WO_defs "!!Z. WO5 ==> WO6"; +goalw thy WO_defs "!!Z. WO5 ==> WO6"; by (fast_tac ZF_cs 1); -result(); +qed "WO5_WO6"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_WO7.ML --- a/src/ZF/AC/WO1_WO7.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/WO1_WO7.ML Tue Jul 25 17:31:53 1995 +0200 @@ -46,7 +46,7 @@ goalw thy [wf_on_def, wf_def] "!!a. [| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"; by (dresolve_tac [nat_le_infinite_Ord RS le_imp_subset] 1 - THEN (atac 1)); + THEN (assume_tac 1)); by (resolve_tac [notI] 1); by (eres_inst_tac [("x","nat")] allE 1); by (eresolve_tac [disjE] 1); @@ -67,11 +67,11 @@ by (rtac ([ordertype_ord_iso RS ord_iso_sym RS ord_iso_rvimage_eq, Memrel_type RS (subset_Int_iff RS iffD1)] MRS trans RS subst) 1 - THEN (atac 1)); + THEN (assume_tac 1)); by (rtac (rvimage_converse RS subst) 1); by (etac (ordertype_ord_iso RS ord_iso_sym RS ord_iso_is_bij RS bij_is_inj RS well_ord_rvimage) 1 - THEN (atac 1)); + THEN (assume_tac 1)); val well_ord_converse_Memrel = result(); goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \ @@ -79,7 +79,7 @@ by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE,exE] 1)); by (REPEAT (ares_tac [exI,conjI,notI] 1)); -by (forward_tac [well_ord_converse_Memrel] 1 THEN (atac 1)); +by (forward_tac [well_ord_converse_Memrel] 1 THEN (assume_tac 1)); by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1); by (contr_tac 2); by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO1_WO8.ML --- a/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/WO1_WO8.ML Tue Jul 25 17:31:53 1995 +0200 @@ -11,7 +11,7 @@ goalw thy WO_defs "!!Z. WO1 ==> WO8"; by (fast_tac ZF_cs 1); -result(); +qed "WO1_WO8"; (* ********************************************************************** *) (* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) @@ -27,4 +27,4 @@ by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym] addSIs [lam_type, singletonI] addIs [the_equality RS ssubst]) 1); -result(); \ No newline at end of file +qed "WO8_WO1"; diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO2_AC16.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO2_AC16.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,605 @@ +(* Title: ZF/AC/WO2_AC16.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + + The proof of WO2 ==> AC16(k #+ m, k) + + The main part of the proof is the inductive reasoning concerning + properties of constructed family T_gamma. + The proof deals with three cases for ordinals: 0, succ and limit ordinal. + The first instance is trivial, the third not difficult, but the second + is very complicated requiring many lemmas. + We also need to prove that at any stage gamma the set + (s - Union(...) - k_gamma) (Rubin & Rubin page 15) + contains m distinct elements (in fact is equipollent to s) +*) + +(* ********************************************************************** *) +(* case of limit ordinal *) +(* ********************************************************************** *) + +goal thy "!!Z. [| ALL y (EX! Y. Y:F(y) & f(z)<=Y); \ +\ ALL i j. i le j --> F(i) <= F(j); j le i; i V = W"; +by (REPEAT (eresolve_tac [asm_rl, allE, impE] 1)); +by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); +by (REPEAT (dresolve_tac [ospec] 1 THEN (assume_tac 1))); +by (eresolve_tac [disjI2 RSN (2, impE)] 1); +by (fast_tac (FOL_cs addSIs [bexI]) 1); +by (eresolve_tac [ex1_two_eq] 1 THEN (REPEAT (ares_tac [conjI] 1))); +val lemma3_1 = result(); + +goal thy "!!Z. [| ALL y (EX! Y. Y:F(y) & f(z)<=Y); \ +\ ALL i j. i le j --> F(i) <= F(j); i V = W"; +by (res_inst_tac [("j","j")] (lt_Ord RS (lt_Ord RSN (2, Ord_linear_le))) 1 + THEN (REPEAT (assume_tac 1))); +by (eresolve_tac [lemma3_1 RS sym] 1 THEN (REPEAT (assume_tac 1))); +by (eresolve_tac [lemma3_1] 1 THEN (REPEAT (assume_tac 1))); +val lemma3 = result(); + +goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \ +\ (ALL x \ +\ (EX! Y. Y : F(y) & fa(x) <= Y)); x < a |] \ +\ ==> ALL y \ +\ (EX! Y. Y : F(y) & fa(z) <= Y)"; +by (REPEAT (resolve_tac [oallI, impI] 1)); +by (dresolve_tac [ltD RSN (2, bspec)] 1 THEN (assume_tac 1)); +by (eresolve_tac [lt_trans RSN (2, impE)] 1 THEN (REPEAT (assume_tac 1))); +by (fast_tac (FOL_cs addSEs [oallE]) 1); +val lemma4 = result(); + +goal thy "!!a. [| ALL y:x. y < a --> F(y) <= X & \ +\ (ALL x \ +\ (EX! Y. Y : F(y) & fa(x) <= Y)); \ +\ x < a; Limit(x); ALL i j. i le j --> F(i) <= F(j) |] \ +\ ==> (UN x (EX! Y. Y : (UN x AC16(k #+ m, k)) - the fact that at any stage + gamma the set (s - Union(...) - k_gamma) is equipollent to s + (Rubin & Rubin page 15). +*) + +(* ********************************************************************** *) +(* dbl_Diff_eqpoll_Card *) +(* ********************************************************************** *) + +goal thy "!!A. [| A eqpoll a; Card(a); ~Finite(a); B lesspoll a; \ +\ C lesspoll a |] ==> A - B - C eqpoll a"; +by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1))); +by (resolve_tac [Diff_lesspoll_eqpoll_Card] 1 THEN (REPEAT (assume_tac 1))); +val dbl_Diff_eqpoll_Card = result(); + +(* ********************************************************************** *) +(* Case of finite ordinals *) +(* ********************************************************************** *) + +goalw thy [lesspoll_def] + "!!X. [| Finite(X); ~Finite(a); Ord(a) |] ==> X lesspoll a"; +by (resolve_tac [conjI] 1); +by (dresolve_tac [nat_le_infinite_Ord RS le_imp_lepoll] 1 + THEN (assume_tac 1)); +by (rewrite_goals_tac [Finite_def]); +by (fast_tac (AC_cs addSEs [eqpoll_sym RS eqpoll_trans]) 2); +by (resolve_tac [lepoll_trans] 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_subset RS + subset_imp_lepoll RSN (2, eqpoll_imp_lepoll RS lepoll_trans)]) 1); +val Finite_lesspoll_infinite_Ord = result(); + +goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x"; +by (fast_tac (AC_cs addIs [equalityI] addSIs [singletonI] + addSEs [singletonE]) 1); +val Union_eq_Un_Diff = result(); + +goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x)) \ +\ --> Finite(Union(X))"; +by (eresolve_tac [nat_induct] 1); +by (fast_tac (AC_cs addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0] + addSIs [nat_0I RS nat_into_Finite] addIs [Union_0 RS ssubst]) 1); +by (REPEAT (resolve_tac [allI, impI] 1)); +by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1)); +by (res_inst_tac [("P","%z. Finite(z)")] (Union_eq_Un_Diff RS ssubst) 1 + THEN (assume_tac 1)); +by (resolve_tac [Finite_Un] 1); +by (fast_tac AC_cs 2); +by (fast_tac (AC_cs addSIs [Diff_sing_eqpoll]) 1); +val Finite_Union_lemma = result(); + +goal thy "!!X. [| ALL x:X. Finite(x); Finite(X) |] ==> Finite(Union(X))"; +by (eresolve_tac [Finite_def RS def_imp_iff RS iffD1 RS bexE] 1); +by (dresolve_tac [Finite_Union_lemma] 1); +by (fast_tac AC_cs 1); +val Finite_Union = result(); + +goalw thy [Finite_def] "!!x. [| x lepoll n; n:nat |] ==> Finite(x)"; +by (fast_tac (AC_cs + addEs [nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll) RS exE, + Ord_nat RSN (2, ltI) RSN (2, lt_trans1) RS ltD]) 1); +val lepoll_nat_num_imp_Finite = result(); + +goal thy "!!X. [| ALL x:X. x lepoll n & x <= T; well_ord(T, R); X lepoll b; \ +\ b Union(X) lesspoll a"; +by (excluded_middle_tac "Finite(X)" 1); +by (resolve_tac [Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord)] 2 + THEN (REPEAT (assume_tac 3))); +by (fast_tac (AC_cs addSEs [lepoll_nat_num_imp_Finite] + addSIs [Finite_Union]) 2); +by (dresolve_tac [lt_Ord RSN (2, lepoll_imp_ex_le_eqpoll)] 1 THEN (assume_tac 1)); +by (REPEAT (eresolve_tac [exE, conjE] 1)); +by (forward_tac [eqpoll_imp_lepoll RS lepoll_infinite] 1 THEN (assume_tac 1)); +by (eresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1) RS + exE] 1); +by (forward_tac [bij_is_surj RS surj_image_eq] 1); +by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1); +by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1)); +by (hyp_subst_tac 1); +by (resolve_tac [lepoll_lesspoll_lesspoll] 1); +by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1 + THEN REPEAT (assume_tac 1)); +by (resolve_tac [UN_lepoll] 1 + THEN (TRYALL (fast_tac (AC_cs addSEs [lt_Ord])))); +val Union_lesspoll = result(); + +(* ********************************************************************** *) +(* recfunAC16_lepoll_index *) +(* ********************************************************************** *) + +goal thy "A Un {a} = cons(a, A)"; +by (fast_tac (AC_cs addSIs [singletonI] + addSEs [singletonE] addIs [equalityI]) 1); +val Un_sing_eq_cons = result(); + +goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)"; +by (asm_simp_tac (AC_ss addsimps [Un_sing_eq_cons, succ_def]) 1); +by (eresolve_tac [mem_not_refl RSN (2, cons_lepoll_cong)] 1); +val Un_lepoll_succ = result(); + +goal thy "!!a. Ord(a) ==> F(a) - (UN b F(a) Un X - (UN b \ +\ recfunAC16(f, g, x, a) - (UN i z:F(LEAST i. z:F(i)) - (UN j<(LEAST i. z:F(i)). F(j))"; +by (fast_tac (AC_cs addEs [less_LeastE] addSEs [OUN_E, LeastI]) 1); +val in_Least_Diff = result(); + +goal thy "!!w. [| (LEAST i. w:F(i)) = (LEAST i. z:F(i)); \ +\ w:(UN i EX b a=b"; +by (fast_tac (AC_cs addSDs [lepoll_1_is_sing] addSEs [singletonE]) 1); +val two_in_lepoll_1 = result(); + +goal thy "!!a. [| ALL i (UN x recfunAC16(f, fa, y, a) lepoll y"; +by (eresolve_tac [trans_induct] 1); +by (eresolve_tac [Ord_cases] 1); +by (asm_simp_tac (AC_ss addsimps [recfunAC16_0, lepoll_refl]) 1); +by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1); +by (fast_tac (AC_cs addIs [conjI RS (expand_if RS iffD2)] + addSDs [succI1 RSN (2, bspec)] + addSEs [subset_succI RS subset_imp_lepoll RSN (2, lepoll_trans), + Un_lepoll_succ]) 1); +by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 1); +by (fast_tac (AC_cs addSEs [lt_Ord RS recfunAC16_Diff_lepoll_1] + addSIs [UN_lepoll_index]) 1); +val recfunAC16_lepoll_index = result(); + +goal thy "!!y. [| recfunAC16(f,g,y,a) <= {X: Pow(A). X eqpoll n}; \ +\ A eqpoll a; y Union(recfunAC16(f,g,y,a)) lesspoll a"; +by (eresolve_tac [eqpoll_def RS def_imp_iff RS iffD1 RS exE] 1); +by (resolve_tac [Union_lesspoll] 1 THEN (TRYALL assume_tac)); +by (eresolve_tac [lt_Ord RS recfunAC16_lepoll_index] 3); +by (eresolve_tac [[bij_is_inj, Card_is_Ord RS well_ord_Memrel] MRS + well_ord_rvimage] 2 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSEs [eqpoll_imp_lepoll]) 1); +val Union_recfunAC16_lesspoll = result(); + +goal thy + "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ +\ Card(a); ~ Finite(a); A eqpoll a; \ +\ k : nat; m : nat; y A - Union(recfunAC16(f, fa, y, a)) - fa`y eqpoll a"; +by (resolve_tac [dbl_Diff_eqpoll_Card] 1 THEN (TRYALL assume_tac)); +by (resolve_tac [Union_recfunAC16_lesspoll] 1 THEN (REPEAT (assume_tac 1))); +by (eresolve_tac [add_type RS nat_succI] 1 THEN (assume_tac 1)); +by (resolve_tac [nat_succI RSN (2, bexI RS (Finite_def RS def_imp_iff RS + iffD2)) RS (Card_is_Ord RSN (3, Finite_lesspoll_infinite_Ord))] 1 + THEN (TRYALL assume_tac)); +by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type) RS CollectE] 1 + THEN (TRYALL assume_tac)); +val dbl_Diff_eqpoll = result(); + +(* back to the proof *) + +val disj_Un_eqpoll_nat_sum = disj_Un_eqpoll_sum RS ( + sum_eqpoll_cong RSN (2, + nat_sum_eqpoll_sum RSN (3, + eqpoll_trans RS eqpoll_trans))) |> standard; + +goal thy "!!x. [| x : Pow(A - B - fa`i); x eqpoll m; \ +\ fa : bij(a, {x: Pow(A) . x eqpoll k}); i fa ` i Un x : {x: Pow(A) . x eqpoll k #+ m}"; +by (resolve_tac [CollectI] 1); +by (fast_tac (AC_cs addSIs [PowD RS (PowD RSN (2, Un_least RS PowI))] + addSEs [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)]) 1); +by (resolve_tac [disj_Un_eqpoll_nat_sum] 1 + THEN (TRYALL assume_tac)); +by (fast_tac (AC_cs addSIs [equals0I]) 1); +by (eresolve_tac [ltD RSN (2, bij_is_fun RS apply_type RS CollectE)] 1 + THEN (REPEAT (assume_tac 1))); +val Un_in_Collect = result(); + +(* ********************************************************************** *) +(* Lemmas simplifying assumptions *) +(* ********************************************************************** *) + +goal thy "!!j. [| ALL y:succ(j). y F(y)<=X & (ALL x Q(x,y)); succ(j) F(j)<=X & (ALL x Q(x,j))"; +by (dresolve_tac [succI1 RSN (2, bspec)] 1); +by (eresolve_tac [impE] 1); +by (resolve_tac [lt_Ord RS (succI1 RS ltI RS lt_Ord RS le_refl) RS lt_trans] 1 + THEN (REPEAT (assume_tac 1))); +val lemma6 = result(); + +goal thy "!!j. [| F(j)<=X; (ALL x Q(x,j)); succ(j) P(j,j) --> F(j) <= X & (ALL x Q(x,j))"; +by (fast_tac (AC_cs addSEs [leE]) 1); +val lemma7 = result(); + +(* ********************************************************************** *) +(* Lemmas needded to prove ex_next_set which means that for any successor *) +(* ordinal there is a set satisfying certain properties *) +(* ********************************************************************** *) + +goal thy "!!A. [| A eqpoll a; ~ Finite(a); Ord(a); m:nat |] \ +\ ==> EX X: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 + ((eqpoll_sym RS eqpoll_imp_lepoll) RSN (2, lepoll_trans)) RS + lepoll_imp_eqpoll_subset RS exE] 1 + THEN REPEAT (assume_tac 1)); +by (fast_tac (AC_cs addSEs [eqpoll_sym]) 1); +val ex_subset_eqpoll = result(); + +goal thy "!!A. [| A <= B Un C; A Int C = 0 |] ==> A <= B"; +by (fast_tac (AC_cs addDs [equals0D]) 1); +val subset_Un_disjoint = result(); + +goal thy "!!F. [| X:Pow(A - Union(B) -C); T:B; F<=T |] ==> F Int X = 0"; +by (fast_tac (AC_cs addSIs [equals0I]) 1); +val Int_empty = result(); + +(* ********************************************************************** *) +(* equipollent subset (and finite) is the whole set *) +(* ********************************************************************** *) + +goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B"; +by (fast_tac (AC_cs addSEs [equalityE, singletonE] + addSIs [equalityI, singletonI]) 1); +val Diffs_eq_imp_eq = result(); + +goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B"; +by (eresolve_tac [nat_induct] 1); +by (fast_tac (AC_cs addSDs [lepoll_0_is_0] addSIs [equalityI]) 1); +by (REPEAT (resolve_tac [allI, impI] 1)); +by (REPEAT (eresolve_tac [conjE] 1)); +by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1 + THEN (assume_tac 1)); +by (forward_tac [subsetD RS Diff_sing_lepoll] 1 + THEN REPEAT (assume_tac 1)); +by (forward_tac [lepoll_Diff_sing] 1); +by (REPEAT (eresolve_tac [allE, impE] 1)); +by (resolve_tac [conjI] 1); +by (fast_tac AC_cs 2); +by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1); +by (eresolve_tac [Diffs_eq_imp_eq] 1 + THEN REPEAT (assume_tac 1)); +val subset_imp_eq_lemma = result(); + +goal thy "!!A. [| A <= B; m lepoll A; B lepoll m; m:nat |] ==> A=B"; +by (fast_tac (FOL_cs addSDs [subset_imp_eq_lemma]) 1); +val subset_imp_eq = result(); + +goal thy "!!f. [| f:bij(a, {Y:X. Y eqpoll succ(k)}); k:nat; f`b<=f`y; b b=y"; +by (dresolve_tac [subset_imp_eq] 1); +by (eresolve_tac [nat_succI] 3); +by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS + CollectE, eqpoll_sym RS eqpoll_imp_lepoll]) 1); +by (fast_tac (AC_cs addSEs [bij_is_fun RS (ltD RSN (2, apply_type)) RS + CollectE, eqpoll_imp_lepoll]) 1); +by (rewrite_goals_tac [bij_def, inj_def]); +by (fast_tac (AC_cs addSDs [ltD]) 1); +val bij_imp_arg_eq = result(); + +goal thy + "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ +\ Card(a); ~ Finite(a); A eqpoll a; \ +\ k : nat; m : nat; y EX X:{Y: Pow(A). Y eqpoll succ(k #+ m)}. fa`y <= X & \ +\ (ALL b \ +\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))"; +by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1 + THEN REPEAT (assume_tac 1)); +by (eresolve_tac [Card_is_Ord] 1); +by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2)); +by (eresolve_tac [CollectE] 4); +by (resolve_tac [bexI] 4); +by (resolve_tac [CollectI] 5); +by (assume_tac 5); +by (eresolve_tac [add_succ RS subst] 5); +by (assume_tac 1); +by (eresolve_tac [nat_succI] 1); +by (assume_tac 1); +by (resolve_tac [conjI] 1); +by (fast_tac AC_cs 1); +by (REPEAT (resolve_tac [ballI, impI, oallI, notI] 1)); +by (dresolve_tac [Int_empty RSN (2, subset_Un_disjoint)] 1 + THEN REPEAT (assume_tac 1)); +by (dresolve_tac [bij_imp_arg_eq] 1 THEN REPEAT (assume_tac 1)); +by (hyp_subst_tac 1); +by (eresolve_tac [bexI RSN (2, notE)] 1 THEN TRYALL assume_tac); +val ex_next_set = result(); + +(* ********************************************************************** *) +(* Lemma ex_next_Ord states that for any successor *) +(* ordinal there is a number of the set satisfying certain properties *) +(* ********************************************************************** *) + +goal thy + "!!a. [| recfunAC16(f, fa, y, a) <= {X: Pow(A) . X eqpoll succ(k #+ m)}; \ +\ Card(a); ~ Finite(a); A eqpoll a; \ +\ k : nat; m : nat; y EX c \ +\ (ALL T:recfunAC16(f, fa, y, a). ~ fa`b <= T))"; +by (dresolve_tac [ex_next_set] 1 THEN REPEAT (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (resolve_tac [bij_converse_bij RS bij_is_fun RS apply_type RS ltI RSN + (2, oexI)] 1); +by (resolve_tac [right_inverse_bij RS ssubst] 1 + THEN REPEAT (ares_tac [Card_is_Ord] 1)); +val ex_next_Ord = result(); + +goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)"; +by (fast_tac (AC_cs addSEs [singletonE]) 1); +val ex1_in_Un_sing = result(); + +(* ********************************************************************** *) +(* Lemma simplifying assumptions *) +(* ********************************************************************** *) + +goal thy "!!j. [| ALL x (EX! Y. Y:F(j) & P(x, Y)); F(j) <= X; \ +\ L : X; P(j, L) & (ALL x (ALL xa:F(j). ~P(x, xa))) |] \ +\ ==> F(j) Un {L} <= X & \ +\ (ALL x \ +\ (EX! Y. Y:F(j) Un {L} & P(x, Y)))"; +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs addSIs [singleton_subsetI]) 1); +by (resolve_tac [oallI] 1); +by (eresolve_tac [oallE] 1 THEN (contr_tac 2)); +by (resolve_tac [impI] 1); +by (eresolve_tac [disjE] 1); +by (eresolve_tac [leE] 1); +by (eresolve_tac [disjI1 RSN (2, impE)] 1 THEN (assume_tac 1)); +by (resolve_tac [ex1E] 1 THEN (assume_tac 1)); +by (eresolve_tac [ex1_in_Un_sing] 1); +by (fast_tac AC_cs 1); +by (fast_tac AC_cs 1); +by (eresolve_tac [bexE] 1); +by (eresolve_tac [UnE] 1); +by (fast_tac (AC_cs addSEs [ex1_in_Un_sing]) 1); +by (fast_tac AC_cs 1); +val lemma8 = result(); + +(* ********************************************************************** *) +(* The main part of the proof: inductive proof of the property of T_gamma *) +(* lemma main_induct *) +(* ********************************************************************** *) + +goal thy + "!!a. [| 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 \ +\ (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))"; +by (resolve_tac [impE] 1 THEN (REPEAT (assume_tac 2))); +by (eresolve_tac [lt_Ord RS trans_induct] 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [Ord_cases] 1); +(* case 0 *) +by (asm_simp_tac (AC_ss addsimps [recfunAC16_0]) 1); +by (fast_tac (AC_cs addSEs [ltE]) 1); +(* case Limit *) +by (asm_simp_tac (AC_ss addsimps [recfunAC16_Limit]) 2); +by (eresolve_tac [lemma5] 2 THEN (REPEAT (assume_tac 2))); +by (fast_tac (FOL_cs addSEs [recfunAC16_mono]) 2); +(* case succ *) +by (hyp_subst_tac 1); +by (eresolve_tac [lemma6 RS conjE] 1 THEN (assume_tac 1)); +by (asm_simp_tac (AC_ss addsimps [recfunAC16_succ]) 1); +by (resolve_tac [conjI RS (expand_if RS iffD2)] 1); +by (eresolve_tac [lemma7] 1 THEN (REPEAT (assume_tac 1))); +by (resolve_tac [impI] 1); +by (resolve_tac [ex_next_Ord RS oexE] 1 + THEN REPEAT (ares_tac [le_refl RS lt_trans] 1)); +by (eresolve_tac [lemma8] 1 THEN (assume_tac 1)); +by (resolve_tac [bij_is_fun RS apply_type] 1 THEN (assume_tac 1)); +by (eresolve_tac [Least_le RS lt_trans2 RS ltD] 1 + THEN REPEAT (ares_tac [lt_Ord, succ_leI] 1)); +by (eresolve_tac [lt_Ord RSN (2, LeastI)] 1 THEN (assume_tac 1)); +val main_induct = result(); + +(* ********************************************************************** *) +(* Lemma to simplify the inductive proof *) +(* - the disired property is a consequence of the inductive assumption *) +(* ********************************************************************** *) + +val [prem1, prem2, prem3, prem4] = goal thy + "[| (!!b. b F(b) <= S & (ALL x (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 AC16(k #+ m,k)"; +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1))); +by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1 + THEN (REPEAT (ares_tac [add_type] 1))); +by (forward_tac [WO2_imp_ex_Card] 1); +by (REPEAT (eresolve_tac [exE,conjE] 1)); +by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS + def_imp_iff RS iffD1)] 1 THEN (assume_tac 1)); +by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS + def_imp_iff RS iffD1)] 1 THEN (assume_tac 1)); +by (REPEAT (eresolve_tac [exE] 1)); +by (res_inst_tac [("x","UN j EX f. f:(PROD X: Pow(A)-{0}. X)"; by (fast_tac (AC_cs addSEs [well_ord_subset RS ex_choice_fun]) 1); -val ex_choice_fun_Pow = result(); \ No newline at end of file +val ex_choice_fun_Pow = result(); diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/WO_AC.thy --- a/src/ZF/AC/WO_AC.thy Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/WO_AC.thy Tue Jul 25 17:31:53 1995 +0200 @@ -1,2 +1,3 @@ (*Dummy theory to document dependencies *) + WO_AC = Order + first diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/first.ML --- a/src/ZF/AC/first.ML Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/first.ML Tue Jul 25 17:31:53 1995 +0200 @@ -11,18 +11,6 @@ by (fast_tac AC_cs 1); val first_is_elem = result(); -goalw thy [well_ord_def, wf_on_def, wf_def, exists_first_def, first_def] - "!!r. well_ord(A,r) ==> ALL B. (B<=A & B~=0) --> exists_first(B,r)"; -by (resolve_tac [allI] 1); -by (resolve_tac [impI] 1); -by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); -by (contr_tac 1); -by (eresolve_tac [bexE] 1); -by (resolve_tac [bexI] 1 THEN (atac 2)); -by (rewrite_goals_tac [tot_ord_def, linear_def]); -by (fast_tac ZF_cs 1); -val well_ord_imp_ex_first = result(); - goalw thy [well_ord_def, wf_on_def, wf_def, first_def] "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"; by (REPEAT (eresolve_tac [conjE,allE,disjE] 1)); @@ -35,7 +23,7 @@ val well_ord_imp_ex1_first = result(); goal thy "!!r. [| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"; -by (dresolve_tac [well_ord_imp_ex1_first] 1 THEN REPEAT (atac 1)); +by (dresolve_tac [well_ord_imp_ex1_first] 1 THEN REPEAT (assume_tac 1)); by (resolve_tac [first_is_elem] 1); by (eresolve_tac [theI] 1); val the_first_in = result(); diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/first.thy --- a/src/ZF/AC/first.thy Tue Jul 25 17:03:59 1995 +0200 +++ b/src/ZF/AC/first.thy Tue Jul 25 17:31:53 1995 +0200 @@ -10,14 +10,10 @@ consts first :: "[i, i, i] => o" - exists_first :: "[i, i] => o" defs - first_def "first(u, X, R) - == u:X & (ALL v:X. v~=u --> : R)" - - exists_first_def "exists_first(X,R) - == EX u:X. first(u, X, R)" + first_def "first(u, X, R) + == u:X & (ALL v:X. v~=u --> : R)" end \ No newline at end of file diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/recfunAC16.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/recfunAC16.ML Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,65 @@ +(* Title: ZF/AC/recfunAC16.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Properties of the recursive definition used in the proof of WO2 ==> AC16 +*) + +open recfunAC16; + +(* ********************************************************************** *) +(* Basic properties of recfunAC16 *) +(* ********************************************************************** *) + +goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0"; +by (resolve_tac [transrec2_0] 1); +val recfunAC16_0 = result(); + +goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \ +\ if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y, recfunAC16(f,fa,i,a), \ +\ recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j & \ +\ (ALL b (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})"; +by (resolve_tac [transrec2_succ] 1); +val recfunAC16_succ = result(); + +goalw thy [recfunAC16_def] "!!i. Limit(i) \ +\ ==> recfunAC16(f,fa,i,a) = (UN j j transrec2(j, 0, B) <= transrec2(i, 0, B)"; +by (resolve_tac [prem2 RS trans_induct] 1); +by (resolve_tac [Ord_cases] 1 THEN (REPEAT (assume_tac 1))); +by (fast_tac lt_cs 1); +by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1); +by (fast_tac (FOL_cs addSIs [succI1, prem1] + addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1); +by (fast_tac (AC_cs addIs [OUN_I, ltI] + addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl, + transrec2_Limit RS ssubst]) 1); +val transrec2_mono_lemma = result(); + +val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \ +\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)"; +by (resolve_tac [prem2 RS leE] 1); +by (resolve_tac [transrec2_mono_lemma RS impE] 1); +by (TRYALL (fast_tac (AC_cs addSIs [prem1, prem2, lt_Ord2]))); +val transrec2_mono = result(); + +(* ********************************************************************** *) +(* Monotonicity of recfunAC16 *) +(* ********************************************************************** *) + +goalw thy [recfunAC16_def] + "!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)"; +by (resolve_tac [transrec2_mono] 1); +by (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1)); +val recfunAC16_mono = result(); + diff -r 686e3eb613b9 -r d43c1f7a53fe src/ZF/AC/recfunAC16.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/recfunAC16.thy Tue Jul 25 17:31:53 1995 +0200 @@ -0,0 +1,23 @@ +(* Title: ZF/AC/recfunAC16.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +A recursive definition used in the proof of WO2 ==> AC16 +*) + +recfunAC16 = Transrec2 + Cardinal + + +consts + + recfunAC16 :: "[i, i, i, i] => i" + +defs + + recfunAC16_def + "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 (ALL t:r. ~ fa`b <= t))))}))" + +end