# HG changeset patch # User lcp # Date 800790683 -7200 # Node ID 5dfdc1464966e59611b3370893fc0233531d70be # Parent 20b708827030581f502bb495762dee0a1db714fb Krzysztof Grabczewski's (nearly) complete AC proofs diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC0_AC1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC0_AC1.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,23 @@ +(* Title: ZF/AC/AC0_AC1.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +AC0 is equivalent to AC1 +AC0 comes from Suppes, AC1 from Rubin & Rubin +*) + +goal thy "!!A. 0~:A ==> A <= Pow(Union(A))-{0}"; +by (fast_tac AC_cs 1); +val subset_Pow_Union = result(); + +goal thy "!!f. [| f:(PROD X:A. X); D<=A |] ==> EX g. g:(PROD X:D. X)"; +by (fast_tac (AC_cs addSIs [restrict_type, apply_type]) 1); +val lemma1 = result(); + +val prems = goalw thy AC_defs "!!Z. AC0 ==> AC1"; +by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); +result(); + +val prems = goalw thy AC_defs "!!Z. AC1 ==> AC0"; +by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); +result(); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC10_AC15.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC10_AC15.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,275 @@ +(* Title: ZF/AC/AC10_AC15.ML + ID: $Id$ + Author: Krzysztof Grabczewski + +The proofs needed to state that AC10, ..., AC15 are equivalent to the rest. +We need the following: + +WO1 ==> AC10(n) ==> AC11 ==> AC12 ==> AC15 ==> WO6 + +In order to add the formulations AC13 and AC14 we need: + +AC10(succ(n)) ==> AC13(n) ==> AC14 ==> AC15 + +or + +AC1 ==> AC13(1); AC13(m) ==> AC13(n); AC13(n) ==> AC14 ==> AC15 + +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 +Rubin & Rubin do. +*) + +(* ********************************************************************** *) +(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) +(* or AC15 *) +(* - cons_times_nat_not_Finite *) +(* - 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); +by (fast_tac (AC_cs addSIs [snd_conv, lam_injective]) 1); +val lepoll_Sigma = result(); + +goal thy "!!A. 0~:A ==> ALL B:{cons(0,x*nat). x:A}. ~Finite(B)"; +by (resolve_tac [ballI] 1); +by (eresolve_tac [RepFunE] 1); +by (hyp_subst_tac 1); +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)); +by (fast_tac AC_cs 1); +val cons_times_nat_not_Finite = result(); + +goal thy "!!A. [| Union(C)=A; a:A |] ==> EX B:C. a:B & B <= A"; +by (fast_tac ZF_cs 1); +val lemma1 = result(); + +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 (dres_inst_tac [("A","B Int C")] not_emptyI 1); +by (fast_tac ZF_cs 1); +val lemma2 = result(); + +goalw thy [sets_of_size_between_def] + "!!A. ALL B:{cons(0, x*nat). x:A}. pairwise_disjoint(f`B) & \ +\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ +\ ==> ALL B:A. EX! u. u:f`cons(0, B*nat) & u <= cons(0, B*nat) & \ +\ 0:u & 2 lepoll u & u lepoll n"; +by (resolve_tac [ballI] 1); +by (eresolve_tac [ballE] 1); +by (fast_tac ZF_cs 2); +by (REPEAT (eresolve_tac [conjE] 1)); +by (dresolve_tac [consI1 RSN (2, lemma1)] 1); +by (eresolve_tac [bexE] 1); +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))); +val lemma3 = result(); + +goalw thy [lepoll_def] "!!A. [| A lepoll i; Ord(i) |] ==> {P(a). a:A} lepoll i"; +by (eresolve_tac [exE] 1); +by (res_inst_tac + [("x", "lam x:RepFun(A, P). LEAST j. EX a:A. x=P(a) & f`a=j")] exI 1); +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 (fast_tac (AC_cs addIs [LeastI2] + addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); +by (eresolve_tac [RepFunE] 1); +by (resolve_tac [LeastI2] 1); +by (fast_tac AC_cs 1); +by (fast_tac (AC_cs addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); +by (fast_tac (AC_cs addEs [sym, left_inverse RS ssubst]) 1); +val lemma4 = result(); + +goal thy "!!A. [| n:nat; B:A; u(B) <= cons(0, B*nat); 0:u(B); 2 lepoll u(B); \ +\ u(B) lepoll succ(n) |] \ +\ ==> (lam x:A. {fst(x). x:u(x)-{0}})`B ~= 0 & \ +\ (lam x:A. {fst(x). x:u(x)-{0}})`B <= B & \ +\ (lam x:A. {fst(x). x:u(x)-{0}})`B lepoll n"; +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] + addEs [lepoll_trans RS succ_lepoll_natE, ssubst] + addSIs [notI, lepoll_refl, nat_0I]) 1); +by (resolve_tac [conjI] 1); +by (fast_tac (ZF_cs addSIs [fst_type] addSEs [consE]) 1); +by (fast_tac (ZF_cs addSEs [equalityE, + Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); +val lemma5 = result(); + +goal thy "!!A. [| EX f. ALL B:{cons(0, x*nat). x:A}. \ +\ pairwise_disjoint(f`B) & \ +\ sets_of_size_between(f`B, 2, succ(n)) & \ +\ Union(f`B)=B; n:nat |] \ +\ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n"; +by (etac exE 1); +by (dtac lemma3 1); +by (fast_tac (empty_cs addSDs [bspec, theI] + addSEs [conjE] + addSIs [exI, ballI, lemma5]) 1); +val ex_fun_AC13_AC15 = result(); + +(* ********************************************************************** *) +(* The target proofs *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC10(n) ==> AC11 *) +(* ********************************************************************** *) + +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(); + +(* ********************************************************************** *) +(* AC11 ==> AC12 *) +(* ********************************************************************** *) + +goalw thy AC_defs "!! Z. AC11 ==> AC12"; +by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1); +result(); + +(* ********************************************************************** *) +(* AC12 ==> AC15 *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!Z. AC12 ==> AC15"; +by (safe_tac ZF_cs); +by (eresolve_tac [allE] 1); +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(); + +(* ********************************************************************** *) +(* AC15 ==> WO6 *) +(* ********************************************************************** *) + +(* in a separate file *) + +(* ********************************************************************** *) +(* The proof needed in the first case, not in the second *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC10(n) ==> AC13(n-1) if 2 le n *) +(* *) +(* Because of the change to the formal definition of AC10(n) we prove *) +(* the following obviously equivalent theorem : *) +(* AC10(n) implies AC13(n) for (1 le n) *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC10(n) |] ==> AC13(n)"; +by (safe_tac ZF_cs); +by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), + ex_fun_AC13_AC15]) 1); +val AC10_imp_AC13 = result(); + +(* ********************************************************************** *) +(* The proofs needed in the second case, not in the first *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC1 ==> AC13(1) *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!Z. AC1 ==> AC13(1)"; +by (resolve_tac [allI] 1); +by (eresolve_tac [allE] 1); +by (resolve_tac [impI] 1); +by (mp_tac 1); +by (eresolve_tac [exE] 1); +by (res_inst_tac [("x","lam x:A. {f`x}")] exI 1); +by (asm_full_simp_tac (AC_ss addsimps + [singleton_eqpoll_1 RS eqpoll_imp_lepoll, + singletonI RS not_emptyI]) 1); +by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1); +result(); + +(* ********************************************************************** *) +(* 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 (fast_tac (ZF_cs addSEs [lepoll_trans]) 1); +result(); + +(* ********************************************************************** *) +(* The proofs necessary for both cases *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC13(n) ==> AC14 if 1 <= n *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!n. [| n:nat; 1 le n; AC13(n) |] ==> AC14"; +by (fast_tac (FOL_cs addIs [bexI]) 1); +result(); + +(* ********************************************************************** *) +(* AC14 ==> AC15 *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!Z. AC14 ==> AC15"; +by (fast_tac ZF_cs 1); +result(); + +(* ********************************************************************** *) +(* The redundant proofs; however cited by Rubin & Rubin *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC13(1) ==> AC1 *) +(* ********************************************************************** *) + +goal thy "!!A. [| A~=0; A lepoll 1 |] ==> EX a. A={a}"; +by (fast_tac (AC_cs addSEs [not_emptyE, lepoll_1_is_sing]) 1); +val lemma_aux = result(); + +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 (REPEAT (eresolve_tac [conjE] 1)); +by (eresolve_tac [lemma_aux RS exE] 1 THEN (atac 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(); + +(* ********************************************************************** *) +(* AC11 ==> AC14 *) +(* ********************************************************************** *) + +goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14"; +by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1); +result(); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC15_WO6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC15_WO6.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,46 @@ +(* Title: ZF/AC/AC15_WO6.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of AC1 ==> WO2 +*) + +open AC15_WO6; + +goal thy "!!x. Ord(x) ==> (UN a \ +\ (UN i \ +\ ALL x WO6"; +by (resolve_tac [allI] 1); +by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac ZF_cs 1); +by (REPEAT (eresolve_tac [bexE,conjE,exE] 1)); +by (resolve_tac [bexI] 1 THEN (assume_tac 2)); +by (resolve_tac [conjI] 1 THEN (assume_tac 1)); +by (res_inst_tac [("x","LEAST i. HH(f,A,i)={A}")] exI 1); +by (res_inst_tac [("x","lam j: (LEAST i. HH(f,A,i)={A}). HH(f,A,j)")] exI 1); +by (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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC15_WO6.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC15_WO6.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +AC15_WO6 = HH \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC17_AC1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC17_AC1.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,95 @@ +(* Title: ZF/AC/AC17_AC1.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of AC1 ==> AC17 +*) + +open AC17_AC1; + +(* *********************************************************************** *) +(* more properties of HH *) +(* *********************************************************************** *) + +goal thy "!!f. [| x - (UN j:LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x}. \ +\ HH(lam X:Pow(x)-{0}. {f`X}, x, j)) = 0; \ +\ f : Pow(x)-{0} -> x |] \ +\ ==> EX r. well_ord(x,r)"; +by (resolve_tac [exI] 1); +by (eresolve_tac [[bij_Least_HH_x RS bij_converse_bij RS bij_is_inj, + Ord_Least RS well_ord_Memrel] MRS well_ord_rvimage] 1); +by (assume_tac 1); +val UN_eq_imp_well_ord = result(); + +(* *********************************************************************** *) +(* theorems closer to the proof *) +(* *********************************************************************** *) + +goalw thy AC_defs "!!Z. ~AC1 ==> \ +\ EX A. ALL f:Pow(A)-{0} -> A. EX u:Pow(A)-{0}. f`u ~: u"; +by (eresolve_tac [swap] 1); +by (resolve_tac [allI] 1); +by (eresolve_tac [swap] 1); +by (res_inst_tac [("x","Union(A)")] exI 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [swap] 1); +by (resolve_tac [impI] 1); +by (fast_tac (AC_cs addSIs [restrict_type]) 1); +val not_AC1_imp_ex = result(); + +goal thy "!!x. [| ALL f:Pow(x) - {0} -> x. EX u: Pow(x) - {0}. f`u~:u; \ +\ EX f: Pow(x)-{0}->x. \ +\ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ +\ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0 |] \ +\ ==> P"; +by (eresolve_tac [bexE] 1); +by (eresolve_tac [UN_eq_imp_well_ord RS exE] 1 THEN (assume_tac 1)); +by (eresolve_tac [ex_choice_fun_Pow RS exE] 1); +by (eresolve_tac [ballE] 1); +by (fast_tac (FOL_cs addEs [bexE, notE, apply_type]) 1); +by (eresolve_tac [notE] 1); +by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); +by (resolve_tac [apply_type RSN (2, subsetD)] 1 THEN TRYALL assume_tac); +by (fast_tac AC_cs 1); +val lemma1 = result(); + +goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0) \ +\ ==> (lam f: Pow(x)-{0}->x. x - F(f)) \ +\ : (Pow(x) -{0} -> x) -> Pow(x) - {0}"; +by (fast_tac (AC_cs addSIs [lam_type] addIs [equalityI] + addSDs [Diff_eq_0_iff RS iffD1]) 1); +val lemma2 = result(); + +goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==> \ +\ (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}"; +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSDs [equals0D]) 1); +val lemma3 = result(); + +goal thy "!!z. EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f \ +\ ==> EX f:F. f`Q(f) : Q(f)"; +by (asm_full_simp_tac AC_ss 1); +val lemma4 = result(); + +goalw thy [AC17_def] "!!Z. [| AC17; ~ AC1 |] ==> False"; +by (eresolve_tac [not_AC1_imp_ex RS exE] 1); +by (excluded_middle_tac + "EX f: Pow(x)-{0}->x. \ +\ x - (UN a:(LEAST i. HH(lam X:Pow(x)-{0}. {f`X},x,i)={x}). \ +\ HH(lam X:Pow(x)-{0}. {f`X},x,a)) = 0" 1); +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 [lemma4] 1); +by (eresolve_tac [bexE] 1); +by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (dresolve_tac [beta RS sym RSN (2, subst_elem)] 1); +by (assume_tac 1); +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(); + + + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC17_AC1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC17_AC1.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +AC17_AC1 = HH \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC18_AC19.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC18_AC19.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,121 @@ +(* Title: ZF/AC/AC18_AC19.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of AC1 ==> AC18 ==> AC19 ==> AC1 +*) + +open AC18_AC19; + +(* ********************************************************************** *) +(* AC1 ==> AC18 *) +(* ********************************************************************** *) + +goal thy "!!f. [| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \ +\ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))"; +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)); +val PROD_subsets = result(); + +goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \ +\ (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))"; +by (resolve_tac [subsetI] 1); +by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac (AC_cs addSEs [RepFunE] addSDs [INT_E] + addEs [UN_E, sym RS equals0D]) 1); +by (eresolve_tac [exE] 1); +by (resolve_tac [UN_I] 1); +by (fast_tac (AC_cs addSEs [PROD_subsets]) 1); +by (simp_tac AC_ss 1); +by (fast_tac (FOL_cs addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)] + addEs [CollectD2] addSIs [INT_I]) 1); +val lemma_AC18 = result(); + +val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18"; +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(); + +(* ********************************************************************** *) +(* AC18 ==> AC19 *) +(* ********************************************************************** *) + +val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19"; +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(); + +(* ********************************************************************** *) +(* AC19 ==> AC1 *) +(* ********************************************************************** *) + +goalw thy [u_def] + "!!A. [| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}"; +by (fast_tac (AC_cs addSIs [not_emptyI, RepFunI] + addSEs [not_emptyE, RepFunE] + addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1); +val RepRep_conj = result(); + +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 [equalityI] 1); +by (fast_tac AC_cs 1); +by (resolve_tac [subsetI] 1); +by (excluded_middle_tac "x=0" 1); +by (fast_tac AC_cs 1); +by (fast_tac (AC_cs addEs [notE, subst_elem] addSIs [equalityI]) 1); +val lemma1_1 = result(); + +goalw thy [u_def] + "!!a. [| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \ +\ ==> f`(u_(a))-{0} : a"; +by (fast_tac (AC_cs addSEs [RepFunI, RepFunE, lemma1_1] + addSDs [apply_type]) 1); +val lemma1_2 = result(); + +goal thy "!!A. EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)"; +by (eresolve_tac [exE] 1); +by (res_inst_tac + [("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1); +by (resolve_tac [lam_type] 1); +by (split_tac [expand_if] 1); +by (resolve_tac [conjI] 1); +by (fast_tac AC_cs 1); +by (fast_tac (AC_cs addSEs [lemma1_2]) 1); +val lemma1 = result(); + +goalw thy [u_def] "!!a. a~=0 ==> 0: (UN b:u_(a). b)"; +by (fast_tac (AC_cs addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1); +val lemma2_1 = result(); + +goal thy "!!A C. [| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0"; +by (eresolve_tac [not_emptyE] 1); +by (res_inst_tac [("a","0")] not_emptyI 1); +by (fast_tac (AC_cs addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1); +val lemma2 = result(); + +goal thy "!!F. (UN f:F. P(f)) ~= 0 ==> F ~= 0"; +by (fast_tac (AC_cs addSEs [not_emptyE]) 1); +val lemma3 = result(); + +goalw thy AC_defs "!!Z. AC19 ==> AC1"; +by (REPEAT (resolve_tac [allI,impI] 1)); +by (excluded_middle_tac "A=0" 1); +by (fast_tac (AC_cs addSIs [empty_fun]) 2); +by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1); +by (eresolve_tac [impE] 1); +by (eresolve_tac [RepRep_conj] 1 THEN (assume_tac 1)); +by (resolve_tac [lemma1] 1); +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(); + + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC18_AC19.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC18_AC19.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,18 @@ +(* Title: ZF/AC/AC18_AC19.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Additional definition used in the proof AC19 ==> AC1 which is a part +of the chain AC1 ==> AC18 ==> AC19 ==> AC1 +*) + +AC18_AC19 = AC_Equiv + + +consts + u_ :: "i => i" + +defs + + u_def "u_(a) == {c Un {0}. c:a}" + +end \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC1_AC17.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC1_AC17.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,25 @@ +(* Title: ZF/AC/AC1_AC17.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of AC1 ==> AC17 +*) + +goal thy "!!f. f : (PROD X:Pow(A) - {0}. X) ==> f : (Pow(A) - {0} -> A)"; +by (resolve_tac [Pi_type] 1 THEN (assume_tac 1)); +by (dresolve_tac [apply_type] 1 THEN (assume_tac 1)); +by (fast_tac AC_cs 1); +val lemma1 = result(); + +goalw thy AC_defs "!!Z. AC1 ==> AC17"; +by (resolve_tac [allI] 1); +by (resolve_tac [ballI] 1); +by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac AC_cs 1); +by (eresolve_tac [exE] 1); +by (resolve_tac [bexI] 1); +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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC1_WO2.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC1_WO2.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,23 @@ +(* Title: ZF/AC/AC1_WO2.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of AC1 ==> WO2 +*) + +open AC1_WO2; + +val [prem] = goal thy "f : (PROD X:Pow(x) - {0}. X) ==> \ +\ ?g(f) : bij(x, LEAST i. HH(lam X:Pow(x)-{0}. {f`X}, x, i) = {x})"; +by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1); +by (resolve_tac [f_subsets_imp_UN_HH_eq_x] 1); +by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2)); +by (fast_tac (AC_cs addSDs [equals0D, prem RS apply_type]) 1); +by (fast_tac (AC_cs addSIs [prem RS Pi_weaken_type]) 1); +val lemma1 = uresult(); + +goalw thy [AC1_def, WO2_def, eqpoll_def] "!!Z. AC1 ==> WO2"; +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(); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC1_WO2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC1_WO2.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +AC1_WO2 = HH \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC2_AC6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC2_AC6.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,201 @@ +(* Title: ZF/AC/AC2_AC6.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proofs needed to state that each of AC2, AC3, ..., AC6 is equivallent +to AC0 and AC1. Namely: +AC1 ==> AC2 ==> AC1 +AC1 ==> AC4 ==> AC3 ==> AC1 +AC4 ==> AC5 ==> AC4 +AC1 <-> AC6 +*) + +(* ********************************************************************** *) +(* AC1 ==> AC2 *) +(* ********************************************************************** *) + +goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |] \ +\ ==> {f`B} <= B Int {f`C. C:A}"; +by (fast_tac (AC_cs addSEs [singletonE, apply_type, RepFunI]) 1); +val lemma1 = result(); + +goalw thy [pairwise_disjoint_def] + "!!A. [| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C"; +by (fast_tac (ZF_cs addSEs [equals0D]) 1); +val lemma2 = result(); + +goalw thy AC_defs "!!Z. AC1 ==> AC2"; +by (resolve_tac [allI] 1); +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 (fast_tac (AC_cs addSEs [RepFunE, lemma2] addEs [apply_type]) 1); +result(); + + +(* ********************************************************************** *) +(* AC2 ==> AC1 *) +(* ********************************************************************** *) + +goal thy "!!A. 0~:A ==> 0 ~: {B*{B}. B:A}"; +by (fast_tac (AC_cs addSDs [sym RS (Sigma_empty_iff RS iffD1)] + addSEs [RepFunE, equals0D]) 1); +val lemma1 = result(); + +goal thy "!!A. [| X*{X} Int C = {y}; X:A |] \ +\ ==> (THE y. X*{X} Int C = {y}): X*A"; +by (resolve_tac [subst_elem] 1); +by (fast_tac (ZF_cs addSIs [the_equality] + addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); +by (fast_tac (AC_cs addSEs [equalityE, make_elim singleton_subsetD]) 1); +val lemma2 = result(); + +goal thy "!!A. ALL D:{E*{E}. E:A}. EX y. D Int C = {y} \ +\ ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) : \ +\ (PROD X:A. X) "; +by (fast_tac (FOL_cs addSEs [lemma2] + addSIs [lam_type, RepFunI, fst_type] + addSDs [bspec]) 1); +val lemma3 = result(); + +goalw thy (AC_defs@AC_aux_defs) "!!Z. AC2 ==> AC1"; +by (REPEAT (resolve_tac [allI, impI] 1)); +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(); + + +(* ********************************************************************** *) +(* AC1 ==> AC4 *) +(* ********************************************************************** *) + +goal thy "!!R. 0 ~: {R``{x}. x:domain(R)}"; +by (fast_tac (AC_cs addSEs [RepFunE, domainE, sym RS equals0D]) 1); +val lemma = result(); + +goalw thy AC_defs "!!Z. AC1 ==> AC4"; +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(); + + +(* ********************************************************************** *) +(* AC4 ==> AC3 *) +(* ********************************************************************** *) + +goal thy "!!f. f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)"; +by (fast_tac (ZF_cs addSDs [apply_type] addSEs [UN_E, singletonE]) 1); +val lemma1 = result(); + +goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}"; +by (fast_tac (ZF_cs addIs [equalityI] + addSEs [not_emptyE] + addSIs [singletonI, not_emptyI] + addDs [range_type]) 1); +val lemma2 = result(); + +goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)"; +by (fast_tac (ZF_cs addIs [equalityI] addSIs [singletonI, UN_I] addSEs [singletonE, UN_E]) 1); +val lemma3 = result(); + +goalw thy AC_defs "!!Z. AC4 ==> AC3"; +by (REPEAT (resolve_tac [allI,ballI] 1)); +by (REPEAT (eresolve_tac [allE,impE] 1)); +by (eresolve_tac [lemma1] 1); +by (asm_full_simp_tac (AC_ss addsimps [lemma2, lemma3] + addcongs [Pi_cong]) 1); +result(); + +(* ********************************************************************** *) +(* AC3 ==> AC1 *) +(* ********************************************************************** *) + +goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)"; +by (asm_full_simp_tac (AC_ss addsimps [id_def] addcongs [Pi_cong]) 1); +by (res_inst_tac [("b","A")] subst_context 1); +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val lemma = result(); + +goalw thy AC_defs "!!Z. AC3 ==> AC1"; +by (REPEAT (resolve_tac [allI, impI] 1)); +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(); + +(* ********************************************************************** *) +(* AC4 ==> AC5 *) +(* ********************************************************************** *) + +goalw thy (range_def::AC_defs) "!!Z. AC4 ==> AC5"; +by (REPEAT (resolve_tac [allI,ballI] 1)); +by (REPEAT (eresolve_tac [allE,impE] 1)); +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 (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 (eresolve_tac [domainE] 1); +by (forward_tac [range_type] 1 THEN (atac 1)); +by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1); +result(); + + +(* ********************************************************************** *) +(* AC5 ==> AC4, Rubin & Rubin, p. 11 *) +(* ********************************************************************** *) + +goal thy "!!A. R <= A*B ==> (lam x:R. fst(x)) : R -> A"; +by (fast_tac (ZF_cs addSIs [lam_type, fst_type]) 1); +val lemma1 = result(); + +goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)"; +by (resolve_tac [equalityI] 1); +by (fast_tac (AC_cs addSEs [lamE, Pair_inject] + addEs [subst_elem] + addSDs [converseD, Pair_fst_snd_eq]) 1); +by (resolve_tac [subsetI] 1); +by (eresolve_tac [domainE] 1); +by (resolve_tac [domainI] 1); +by (fast_tac (AC_cs addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1); +val lemma2 = result(); + +goal thy "!!A. [| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)"; +by (eresolve_tac [bexE] 1); +by (forward_tac [domain_of_fun] 1); +by (fast_tac ZF_cs 1); +val lemma3 = result(); + +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 (resolve_tac [imageI] 1); +by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1 + THEN (REPEAT (atac 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 (fast_tac (AC_cs addSEs [lemma4]) 1); +result(); + + +(* ********************************************************************** *) +(* AC1 <-> AC6 *) +(* ********************************************************************** *) + +goalw thy AC_defs "AC1 <-> AC6"; +by (fast_tac (ZF_cs addDs [equals0D] addSEs [not_emptyE]) 1); +result(); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC7_AC9.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC7_AC9.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,237 @@ +(* Title: ZF/AC/AC7-AC9.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous +instances of AC. +*) + +(* ********************************************************************** *) +(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *) +(* - Sigma_fun_space_not0 *) +(* - all_eqpoll_imp_pair_eqpoll *) +(* - Sigma_fun_space_eqpoll *) +(* ********************************************************************** *) + +goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C"; +by (fast_tac ZF_cs 1); +val mem_not_eq_not_mem = result(); + +goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0"; +by (fast_tac (ZF_cs addSDs [Sigma_empty_iff RS iffD1] + addDs [fun_space_emptyD, mem_not_eq_not_mem] + addEs [equals0D] + addSIs [equals0I,UnionI]) 1); +val Sigma_fun_space_not0 = result(); + +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)); +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 (asm_full_simp_tac ZF_ss 1); +val if_eqE1 = result(); + +goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \ +\ ==> 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 (asm_full_simp_tac ZF_ss 1); +val if_eqE2 = result(); + +goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)"; +by (fast_tac (ZF_cs addDs [subsetD] + addSIs [lamI] + addEs [equalityE, lamE]) 1); +val lam_eqE = result(); + +goalw thy [inj_def] + "!!A. C:A ==> (lam g:(nat->Union(A))*C. \ +\ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \ +\ : inj((nat->Union(A))*C, (nat->Union(A)) ) "; +by (resolve_tac [CollectI] 1); +by (fast_tac (ZF_cs addSIs [lam_type,RepFunI,if_type,snd_type,apply_type, + fst_type,diff_type,nat_succI,nat_0I]) 1); +by (REPEAT (resolve_tac [ballI, impI] 1)); +by (asm_full_simp_tac ZF_ss 1); +by (REPEAT (eresolve_tac [SigmaE] 1)); +by (REPEAT (hyp_subst_tac 1)); +by (asm_full_simp_tac ZF_ss 1); +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 (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); +val lemma = result(); + +goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))"; +by (resolve_tac [eqpollI] 1); +by (fast_tac (ZF_cs addSEs [prod_lepoll_self, not_sym RS not_emptyE, + subst_elem] addEs [swap]) 2); +by (rewrite_goals_tac [lepoll_def]); +by (fast_tac (ZF_cs addSIs [lemma]) 1); +val Sigma_fun_space_eqpoll = result(); + + +(* ********************************************************************** *) +(* AC6 ==> AC7 *) +(* ********************************************************************** *) + +goalw thy AC_defs "!!Z. AC6 ==> AC7"; +by (fast_tac ZF_cs 1); +result(); + +(* ********************************************************************** *) +(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) +(* The case of the empty family of sets added in order to complete *) +(* the proof. *) +(* ********************************************************************** *) + +goal thy "!!y. y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)"; +by (fast_tac (ZF_cs addSIs [lam_type, snd_type, apply_type]) 1); +val lemma1_1 = result(); + +goal thy "!!A. y: (PROD B:{Y*C. C:A}. B) \ +\ ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)"; +by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1); +val lemma1_2 = result(); + +goal thy "!!A. (PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 \ +\ ==> (PROD B:A. B) ~= 0"; +by (fast_tac (ZF_cs addSIs [equals0I,lemma1_1, lemma1_2] + addSEs [equals0D]) 1); +val lemma1 = result(); + +goal thy "!!A. 0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}"; +by (fast_tac (ZF_cs addEs [RepFunE, + Sigma_fun_space_not0 RS not_sym RS notE]) 1); +val lemma2 = result(); + +goalw thy AC_defs "!!Z. AC7 ==> AC6"; +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (excluded_middle_tac "A=0" 1); +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 (fast_tac (AC_cs addSEs [RepFunE] + addSIs [lemma2, all_eqpoll_imp_pair_eqpoll, + Sigma_fun_space_eqpoll]) 1); +result(); + + +(* ********************************************************************** *) +(* AC1 ==> AC8 *) +(* ********************************************************************** *) + +goalw thy [eqpoll_def] + "!!A. ALL B:A. EX B1 B2. B= & B1 eqpoll B2 \ +\ ==> 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 (REPEAT (eresolve_tac [exE,conjE] 1)); +by (hyp_subst_tac 1); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSEs [sym RS equals0D]) 1); +val lemma1 = result(); + +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 (fast_tac (AC_cs addSEs [apply_type]) 1); +val lemma2 = result(); + +goalw thy AC_defs "!!Z. AC1 ==> AC8"; +by (resolve_tac [allI] 1); +by (eresolve_tac [allE] 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [impE] 1); +by (eresolve_tac [lemma1] 1); +by (fast_tac (AC_cs addSEs [lemma2]) 1); +result(); + + +(* ********************************************************************** *) +(* AC8 ==> AC9 *) +(* - this proof replaces the following two from Rubin & Rubin: *) +(* AC8 ==> AC1 and AC1 ==> AC9 *) +(* ********************************************************************** *) + +goal thy "!!A. ALL B1:A. ALL B2:A. B1 eqpoll B2 ==> \ +\ ALL B:A*A. EX B1 B2. B= & B1 eqpoll B2"; +by (fast_tac ZF_cs 1); +val lemma1 = result(); + +goal thy "!!f. f:bij(fst(),snd()) ==> f:bij(a,b)"; +by (asm_full_simp_tac AC_ss 1); +val lemma2 = result(); + +goalw thy AC_defs "!!Z. AC8 ==> AC9"; +by (resolve_tac [allI] 1); +by (resolve_tac [impI] 1); +by (eresolve_tac [allE] 1); +by (eresolve_tac [impE] 1); +by (eresolve_tac [lemma1] 1); +by (fast_tac (AC_cs addSEs [lemma2]) 1); +result(); + + +(* ********************************************************************** *) +(* AC9 ==> AC1 *) +(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) +(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *) +(* (x * y) Un {0} when y is a set of total functions acting from nat to *) +(* Union(A) -- therefore we have used the set (y * nat) instead of y. *) +(* ********************************************************************** *) + +(* Rules nedded to prove lemma1 *) +val snd_lepoll_SigmaI = prod_lepoll_self RS + ((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans)); +val lemma1_cs = FOL_cs addSEs [UnE, RepFunE] + addSIs [all_eqpoll_imp_pair_eqpoll, ballI, + nat_cons_eqpoll RS eqpoll_trans] + addEs [Sigma_fun_space_not0 RS not_emptyE] + addIs [snd_lepoll_SigmaI, eqpoll_refl RSN + (2, prod_eqpoll_cong), Sigma_fun_space_eqpoll]; + +goal thy "!!A. [| 0~:A; A~=0 |] \ +\ ==> ALL B1: ({((nat->Union(A))*B)*nat. B:A} \ +\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \ +\ ALL B2: ({((nat->Union(A))*B)*nat. B:A} \ +\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \ +\ B1 eqpoll B2"; +by (fast_tac lemma1_cs 1); +val lemma1 = result(); + +goal thy "!!A. ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}. \ +\ ALL B2:{(F*B)*N. B:A} \ +\ Un {cons(0,(F*B)*N). B:A}. f` : bij(B1, B2) \ +\ ==> (lam B:A. snd(fst((f`)`0))) : \ +\ (PROD X:A. X)"; +by (resolve_tac [lam_type] 1); +by (resolve_tac [snd_type] 1); +by (resolve_tac [fst_type] 1); +by (resolve_tac [consI1 RSN (2, apply_type)] 1); +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"; +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 (fast_tac (AC_cs addSEs [lemma2]) 1); +result(); \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Mon May 15 09:35:07 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Thu May 18 11:51:23 1995 +0200 @@ -15,7 +15,10 @@ AC17_def, AC18_def, AC19_def]; val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; - + +val AC_cs = OrdQuant_cs; +val AC_ss = OrdQuant_ss; + (* ******************************************** *) (* Theorems analogous to ones presented in "ZF/Ordinal.ML" *) @@ -47,15 +50,13 @@ by (asm_simp_tac (ZF_ss addsimps prems) 1); val def_imp_iff = result(); -val prems = goal ZF.thy "(A == B) ==> P(A) <-> P(B)"; -by (asm_simp_tac (ZF_ss addsimps prems) 1); -val def_imp_iff_P = result(); +val prems = goal ZF.thy "(A == B) ==> A = B"; +by (simp_tac (ZF_ss addsimps prems) 1); +val def_imp_eq = result(); -(* used only in lemmas4-7.ML *) -(*Note modified statement and proof*) -goal ZF.thy "!!X. X~=0 ==> (A->X)~=0"; -by (fast_tac (ZF_cs addSIs [equals0I,lam_type] addSEs [equals0D]) 1); -val fun_space_not0I = result(); +goal thy "!!X. (A->X)=0 ==> X=0"; +by (fast_tac (ZF_cs addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1); +val fun_space_emptyD = result(); (* used only in WO1_DC.ML *) (*Note simpler proof*) @@ -109,3 +110,31 @@ "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); val Inf_Card_is_InfCard = result(); + +goal thy "(THE z. {x}={z}) = x"; +by (fast_tac (AC_cs addSIs [the_equality] + addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); +val the_element = result(); + +goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})"; +by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); +by (TRYALL (eresolve_tac [RepFunI, RepFunE])); +by (REPEAT (asm_full_simp_tac (AC_ss addsimps [the_element]) 1)); +val lam_sing_bij = result(); + +val [major,minor] = goal thy + "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; +by (fast_tac (AC_cs addSIs [major RS Pi_type, minor RS subsetD, + major RS apply_type]) 1); +val Pi_weaken_type = result(); + +val [major, minor] = goalw thy [inj_def] + "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; +by (fast_tac (AC_cs addSEs [minor] + addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); +val inj_strengthen_type = result(); + +goal thy "A*B=0 <-> A=0 | B=0"; +by (fast_tac (ZF_cs addSIs [equals0I] addEs [equals0D]) 1); +val Sigma_empty_iff = result(); + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Mon May 15 09:35:07 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.thy Thu May 18 11:51:23 1995 +0200 @@ -8,11 +8,11 @@ Axiom AC0 comes from "Axiomatic Set Theory" by P. Suppes, 1972. Some Isabelle proofs of equivalences of these axioms are formalizations of -proofs presented by Rubin. The others are based on Rubin's proofs, but -slightly changed. +proofs presented by the Rubins. The others are based on the Rubins' proofs, +but slightly changed. *) -AC_Equiv = CardinalArith + Univ + Transrec2 + +AC_Equiv = CardinalArith + Univ + OrdQuant + consts @@ -26,19 +26,11 @@ AC10, AC13 :: "i => o" AC16 :: "[i, i] => o" AC18 :: "prop" ("AC18") - -(* Auxiliary definitions used in theorems *) - first :: "[i, i, i] => o" - exists_first :: "[i, i] => o" + +(* Auxiliary definitions used in definitions *) pairwise_disjoint :: "i => o" sets_of_size_between :: "[i, i, i] => o" - GG :: "[i, i, i] => i" - GG2 :: "[i, i, i] => i" - HH :: "[i, i, i] => i" - - recfunAC16 :: "[i, i, i, i] => i" - defs (* Well Ordering Theorems *) @@ -60,7 +52,7 @@ WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) --> \ \ well_ord(A,converse(R)))" - WO8_def "WO8 == ALL A. (0~:A --> (EX f. f : (PROD X:A. X))) --> \ + WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) --> \ \ (EX R. well_ord(A,R))" (* Axioms of Choice *) @@ -120,15 +112,9 @@ \ (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))" AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \ -\ (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))" - -(* Auxiliary definitions used in theorems *) +\ (UN f:(PROD B:A. B). INT a:A. f`a))" - 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)" +(* Auxiliary definitions used in the above definitions *) pairwise_disjoint_def "pairwise_disjoint(A) \ \ == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2" @@ -136,22 +122,4 @@ sets_of_size_between_def "sets_of_size_between(A,m,n) \ \ == ALL B:A. m lepoll B & B lepoll n" -(* Auxiliary definitions used in proofs *) - - GG_def "GG(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ -\ if(z=0, x, f`z))`(x - {r`c. c:b}))" - - GG2_def "GG2(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ -\ if(z=0, {x}, f`z))`(x - Union({r`c. c:b})))" - - HH_def "HH(f,x,a) == transrec(a, %b r. (lam z:Pow(x). \ -\ if(z=0|f`z~:z, x, f`z))`(x - {r`c. c:b}))" - - 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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/HH.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/HH.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,230 @@ +(* Title: ZF/AC/HH.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Some properties of the recursive definition of HH used in the proofs of + AC17 ==> AC1 + AC1 ==> WO2 + AC15 ==> WO6 +*) + +open HH; + +(* ********************************************************************** *) +(* Lemmas useful in each of the three proofs *) +(* ********************************************************************** *) + +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)))"; +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 (split_tac [expand_if] 1); +by (fast_tac ZF_cs 1); +val HH_values = result(); + +goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))"; +by (fast_tac (AC_cs addSIs [equalityI]) 1); +val subset_imp_Diff_eq = result(); + +goal thy "!!c. [| c:a-b; b c=b | b P(y) = {x}) ==> x - (UN y:A. P(y)) = x"; +by (asm_full_simp_tac (AC_ss addsimps prems) 1); +by (fast_tac (AC_cs addSIs [equalityI] addSDs [prem] + addSEs [RepFunE, mem_irrefl]) 1); +val Diff_UN_eq_self = result(); + +goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \ +\ ==> HH(f,x,a) = HH(f,x,a1)"; +by (resolve_tac [HH_def_satisfies_eq RS + (HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1); +by (eresolve_tac [subst_context] 1); +val HH_eq = result(); + +goal thy "!!a. [| HH(f,x,b)={x}; b HH(f,x,a)={x}"; +by (res_inst_tac [("P","b HH(f,x,b) : Pow(x)-{0}"; +by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); +by (dresolve_tac [HH_is_x_gt_too] 1 THEN (assume_tac 1)); +by (dresolve_tac [subst] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); +val HH_subset_x_lt_too = result(); + +goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \ +\ ==> 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 (dresolve_tac [expand_if RS iffD1] 1); +by (split_tac [expand_if] 1); +by (fast_tac (AC_cs addSEs [mem_irrefl]) 1); +val HH_subset_x_imp_subset_Diff_UN = result(); + +goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; +by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); +by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); +by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSIs [singleton_iff RS iffD2, equals0I]) 1); +val HH_eq_arg_lt = result(); + +goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \ +\ Ord(v); Ord(w) |] ==> v=w"; +by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); +by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2 + THEN REPEAT (assume_tac 2)); +by (dresolve_tac [subst_elem] 1 THEN (assume_tac 1)); +by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1); +val HH_eq_imp_arg_eq = result(); + +goalw thy [lepoll_def, inj_def] + "!!i. [| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"; +by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1); +by (asm_simp_tac AC_ss 1); +by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too] + addSIs [lam_type, ballI, ltI] addIs [bexI]) 1); +val HH_subset_x_imp_lepoll = result(); + +goal thy "HH(f, x, Hartog(Pow(x)-{0})) = {x}"; +by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 2)); +by (fast_tac (FOL_cs addSDs [HH_subset_x_imp_lepoll] + addSIs [Ord_Hartog] addSEs [HartogE]) 1); +val HH_Hartog_is_x = result(); + +goal thy "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}"; +by (fast_tac (AC_cs addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1); +val HH_Least_eq_x = result(); + +goal thy "!!a. a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}"; +by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); +by (resolve_tac [less_LeastE] 1); +by (eresolve_tac [Ord_Least RSN (2, ltI)] 2); +by (assume_tac 1); +val less_Least_subset_x = result(); + +(* ********************************************************************** *) +(* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *) +(* ********************************************************************** *) + +goalw thy [inj_def] + "(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \ +\ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"; +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSIs [lam_type] addDs [less_Least_subset_x] + addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1); +val lam_Least_HH_inj_Pow = result(); + +goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \ +\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ +\ : inj(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; +by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1); +by (asm_full_simp_tac AC_ss 1); +by (fast_tac (AC_cs addSEs [RepFun_eqI]) 1); +val lam_Least_HH_inj = result(); + +goal thy "!!A. [| A={a}; b:A |] ==> b=a"; +by (fast_tac AC_cs 1); +val elem_of_sing_eq = result(); + +goalw thy [surj_def] + "!!x. [| x - (UN a:A. F(a)) = 0; \ +\ ALL a:A. EX z:x. F(a) = {z} |] \ +\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; +by (asm_full_simp_tac (AC_ss addsimps [Diff_eq_0_iff]) 1); +by (resolve_tac [conjI] 1); +by (fast_tac (AC_cs addSIs [lam_type] addSEs [RepFun_eqI]) 1); +by (resolve_tac [ballI] 1); +by (eresolve_tac [RepFunE] 1); +by (dresolve_tac [subsetD] 1 THEN (assume_tac 1)); +by (eresolve_tac [UN_E] 1); +by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); +by (eresolve_tac [bexE] 1); +by (resolve_tac [bexI] 1 THEN (assume_tac 2)); +by (forward_tac [elem_of_sing_eq] 1 THEN (assume_tac 1)); +by (fast_tac AC_cs 1); +val lam_surj_sing = result(); + +goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0"; +by (fast_tac (AC_cs addSIs [equals0I, singletonI RS subst_elem] + addSDs [equals0D]) 1); +val not_emptyI2 = result(); + +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, + not_emptyI2 RS if_P]) 1); +by (fast_tac AC_cs 1); +val f_subset_imp_HH_subset = result(); + +val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \ +\ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"; +by (excluded_middle_tac "?P : {0}" 1); +by (fast_tac AC_cs 2); +by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS + f_subset_imp_HH_subset] 1); +by (fast_tac (AC_cs addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)] + addSEs [mem_irrefl]) 1); +val f_subsets_imp_UN_HH_eq_x = result(); + +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 (split_tac [expand_if] 1); +by (fast_tac ZF_cs 1); +val HH_values2 = result(); + +goal thy "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; +by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); +by (fast_tac (AC_cs addSEs [equalityE, mem_irrefl] + addSDs [singleton_subsetD]) 1); +val HH_subset_imp_eq = result(); + +goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x}); \ +\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; +by (dresolve_tac [less_Least_subset_x] 1); +by (forward_tac [HH_subset_imp_eq] 1); +by (dresolve_tac [apply_type] 1); +by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); +by (fast_tac (AC_cs addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); +by (fast_tac (AC_cs addSEs [RepFunE] addEs [ssubst]) 1); +val f_sing_imp_HH_sing = result(); + +goalw thy [bij_def] + "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ +\ f : (PROD X:Pow(x)-{0}. {{z}. z:x}) |] \ +\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ +\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; +by (fast_tac (AC_cs addSIs [lam_Least_HH_inj, lam_surj_sing, + f_sing_imp_HH_sing]) 1); +val f_sing_lam_bij = result(); + +goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \ +\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})"; +by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2] + addDs [apply_type]) 1); +val lam_singI = result(); + +val bij_Least_HH_x = standard (lam_singI RSN (2, + [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] MRS comp_bij)); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/HH.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/HH.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,23 @@ +(* Title: ZF/AC/HH.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The theory file for the proofs of + AC17 ==> AC1 + AC1 ==> WO2 + AC15 ==> WO6 +*) + +HH = AC_Equiv + Hartog + WO_AC + + +consts + + HH :: "[i, i, i] => i" + +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)))" + +end + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/Hartog.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/Hartog.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,84 @@ +(* Title: ZF/AC/Hartog.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + + Some proofs on the Hartogs function. +*) + +open Hartog; + +goal thy "!!X. ALL a. Ord(a) --> a:X ==> P"; +by (res_inst_tac [("X1","{y:X. Ord(y)}")] (ON_class RS revcut_rl) 1); +by (fast_tac AC_cs 1); +val Ords_in_set = result(); + +goalw thy [lepoll_def] "!!X. [| Ord(a); a lepoll X |] ==> \ +\ EX Y. Y<=X & (EX R. well_ord(Y,R) & ordertype(Y,R)=a)"; +by (eresolve_tac [exE] 1); +by (REPEAT (resolve_tac [exI, conjI] 1)); +by (eresolve_tac [inj_is_fun RS fun_is_rel RS image_subset] 1); +by (resolve_tac [exI] 1); +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)); +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))); +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 (step_tac AC_cs 1); +by (REPEAT (ares_tac [exI, conjI] 1)); +by (eresolve_tac [ordertype_Int] 2); +by (fast_tac AC_cs 1); +val Ord_lepoll_imp_eq_ordertype = result(); + +goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> \ +\ ALL a. Ord(a) --> \ +\ 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 (fast_tac (AC_cs addSIs [ReplaceI] addEs [sym]) 1); +val Ords_lepoll_set_lemma = result(); + +goal thy "!!X. ALL a. Ord(a) --> a lepoll X ==> P"; +by (eresolve_tac [Ords_lepoll_set_lemma RS Ords_in_set] 1); +val Ords_lepoll_set = result(); + +goal thy "EX a. Ord(a) & ~a lepoll X"; +by (resolve_tac [swap] 1); +by (fast_tac AC_cs 1); +by (resolve_tac [Ords_lepoll_set] 1); +by (fast_tac AC_cs 1); +val ex_Ord_not_lepoll = result(); + +goalw thy [Hartog_def] "~ Hartog(A) lepoll A"; +by (resolve_tac [ex_Ord_not_lepoll RS exE] 1); +by (resolve_tac [LeastI] 1); +by (REPEAT (fast_tac AC_cs 1)); +val HartogI = result(); + +val HartogE = HartogI RS notE; + +goalw thy [Hartog_def] "Ord(Hartog(A))"; +by (resolve_tac [Ord_Least] 1); +val Ord_Hartog = result(); + +goalw thy [Hartog_def] "!!i. [| i < Hartog(A); ~ i lepoll A |] ==> P"; +by (fast_tac (AC_cs addEs [less_LeastE]) 1); +val less_HartogE1 = result(); + +goal thy "!!i. [| i < Hartog(A); i eqpoll Hartog(A) |] ==> P"; +by (fast_tac (AC_cs addEs [less_HartogE1, eqpoll_sym RS eqpoll_imp_lepoll + RS lepoll_trans RS HartogE]) 1); +val less_HartogE = result(); + +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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/Hartog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/Hartog.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,18 @@ +(* Title: ZF/AC/Hartog.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Hartog's function. +*) + +Hartog = Cardinal + + +consts + + Hartog :: "i => i" + +defs + + Hartog_def "Hartog(X) == LEAST i. ~i lepoll X" + +end \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/ROOT.ML --- a/src/ZF/AC/ROOT.ML Mon May 15 09:35:07 1995 +0200 +++ b/src/ZF/AC/ROOT.ML Thu May 18 11:51:23 1995 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge -Executes the proofs of the AC-equivalences, by Krzysztof Gr`abczewski +Executes the proofs of the AC-equivalences, due to Krzysztof Gr`abczewski *) ZF_build_completed; (*Make examples fail if ZF did*) @@ -13,21 +13,28 @@ loadpath := [".", "AC"]; -time_use_thy "WO6_WO1"; +time_use_thy "AC/AC_Equiv"; + +time_use "AC/WO1_WO6.ML"; +time_use_thy "AC/WO6_WO1"; +time_use "AC/WO1_WO7.ML"; +time_use "AC/WO1_WO8.ML"; + +time_use "AC/AC0_AC1.ML"; +time_use "AC/AC2_AC6.ML"; +time_use "AC/AC7_AC9.ML"; -(*New ones pending on ~kg10006/isabelle -time_use "AC10_AC11.ML"; -time_use "AC11_AC12.ML"; -time_use "AC1_AC13.ML"; -time_use "AC13_AC1.ML"; -time_use "AC13_AC13.ML"; -time_use "AC13_AC14.ML"; -time_use "AC14_AC15.ML"; -time_use_thy "lemmas_AC13_AC15"; -time_use_thy "AC10_AC13"; -time_use_thy "AC11_AC14"; -time_use_thy "AC12_AC15"; -time_use "AC14_AC15.ML"; -*) +time_use_thy "AC/WO1_AC1"; +time_use_thy "AC/AC1_WO2"; + +time_use "AC/AC10_AC15.ML"; +time_use_thy "AC/AC15_WO6"; + +(* AC16 to add *) + +time_use "AC/AC1_AC17.ML"; +time_use_thy "AC/AC17_AC1"; + +time_use_thy "AC/AC18_AC19"; writeln"END: Root file for ZF/AC"; diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO1_AC1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_AC1.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,12 @@ +(* 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 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO1_AC1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_AC1.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +WO1_AC1 = AC_Equiv + WO_AC \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO1_WO6.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_WO6.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,79 @@ +(* Title: ZF/AC/WO1-WO6.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + + Proofs needed to state that formulations WO1,...,WO6 are all equivalent. + All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML) + + Every proofs (exept one) presented in this file are referred as clear + by Rubin & Rubin (page 2). + They refer reader to a book by G"odel to see the proof WO1 ==> WO2. + Fortunately order types made this proof also very easy. +*) + +(* ********************************************************************** *) + +goalw thy WO_defs "!!Z. WO2 ==> WO3"; +by (fast_tac ZF_cs 1); +result(); + +(* ********************************************************************** *) + +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(); + +(* ********************************************************************** *) + +goalw thy (eqpoll_def::WO_defs) "!!Z. WO1 ==> WO2"; +by (fast_tac (ZF_cs addSIs [Ord_ordertype, ordermap_bij]) 1); +result(); + +(* ********************************************************************** *) + +goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}"; +by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1); +val lam_sets = result(); + +goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B"; +by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1); +val surj_imp_eq_ = result(); + +goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a WO4(1)"; +by (resolve_tac [allI] 1); +by (eres_inst_tac [("x","A")] allE 1); +by (eresolve_tac [exE] 1); +by (REPEAT (resolve_tac [exI, conjI] 1)); +by (eresolve_tac [Ord_ordertype] 1); +by (resolve_tac [conjI] 1); +by (eresolve_tac [ordermap_bij RS bij_converse_bij RS bij_is_fun RS + lam_sets RS domain_of_fun] 1); +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(); + +(* ********************************************************************** *) + +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(); + +(* ********************************************************************** *) + +val prems = goalw thy WO_defs "!!Z. [| m:nat; 1 le m; WO4(m) |] ==> WO5"; +by (fast_tac ZF_cs 1); +result(); + +(* ********************************************************************** *) + +val prems = goalw thy WO_defs "!!Z. WO5 ==> WO6"; +by (fast_tac ZF_cs 1); +result(); + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO1_WO7.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_WO7.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,90 @@ +(* Title: ZF/AC/WO1_WO7.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5) +LEMMA is the sentence denoted by (**) +*) + +(* ********************************************************************** *) +(* It is easy to see, that WO7 is equivallent to (**) *) +(* ********************************************************************** *) + +goalw thy [WO7_def] "WO7 <-> (ALL X. ~Finite(X) --> \ +\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))))"; +by (fast_tac (ZF_cs addSEs [Finite_well_ord_converse]) 1); +val WO7_iff_LEMMA = result(); + +(* ********************************************************************** *) +(* It is also easy to show that LEMMA implies WO1. *) +(* ********************************************************************** *) + +goalw thy [WO1_def] "!!Z. ALL X. ~Finite(X) --> \ +\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R))) ==> WO1"; +by (resolve_tac [allI] 1); +by (eresolve_tac [allE] 1); +by (excluded_middle_tac "Finite(A)" 1); +by (fast_tac AC_cs 1); +by (rewrite_goals_tac [Finite_def, eqpoll_def]); +by (fast_tac (AC_cs addSIs [nat_into_Ord RS well_ord_Memrel RSN (2, + bij_is_inj RS well_ord_rvimage)]) 1); +val LEMMA_imp_WO1 = result(); + +(* ********************************************************************** *) +(* The Rubins' proof of the other implication is contained within the *) +(* following sentence : *) +(* "... each infinite ordinal is well ordered by < but not by >." *) +(* This statement can be proved by the following two theorems. *) +(* But moreover we need to show similar property for any well ordered *) +(* infinite set. It is not very difficult thanks to Isabelle order types *) +(* We show that if a set is well ordered by some relation and by it's *) +(* converse, then apropriate order type is well ordered by the converse *) +(* of it's membership relation, which in connection with the previous *) +(* gives the conclusion. *) +(* ********************************************************************** *) + +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)); +by (resolve_tac [notI] 1); +by (eres_inst_tac [("x","nat")] allE 1); +by (eresolve_tac [disjE] 1); +by (fast_tac (ZF_cs addSDs [nat_0I RSN (2,equals0D)]) 1); +by (eresolve_tac [bexE] 1); +by (eres_inst_tac [("x","succ(x)")] allE 1); +by (fast_tac (ZF_cs addSIs [nat_succI, converseI, MemrelI, + nat_succI RSN (2, subsetD)]) 1); +val converse_Memrel_not_wf_on = result(); + +goalw thy [well_ord_def] + "!!a. [| Ord(a); ~Finite(a) |] ==> ~well_ord(a,converse(Memrel(a)))"; +by (fast_tac (ZF_cs addSDs [converse_Memrel_not_wf_on]) 1); +val converse_Memrel_not_well_ord = result(); + +goal thy "!!A. [| well_ord(A,r); well_ord(A,converse(r)) |] \ +\ ==> well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))"; +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)); +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)); +val well_ord_converse_Memrel = result(); + +goalw thy [WO1_def] "!!Z. WO1 ==> ALL X. ~Finite(X) --> \ +\ (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"; +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 [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 + bij_is_inj RS (exI RS (lepoll_def RS def_imp_iff RS iffD2)) + RS lepoll_Finite] + addSIs [notI] addEs [notE]) 1); +val WO1_imp_LEMMA = result(); + diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO1_WO8.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO1_WO8.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,30 @@ +(* Title: ZF/AC/WO1_WO8.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) +*) + +(* ********************************************************************** *) +(* Trivial implication "WO1 ==> WO8" *) +(* ********************************************************************** *) + +goalw thy WO_defs "!!Z. WO1 ==> WO8"; +by (fast_tac ZF_cs 1); +result(); + +(* ********************************************************************** *) +(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) +(* ********************************************************************** *) + +goalw thy WO_defs "!!Z. WO8 ==> WO1"; +by (resolve_tac [allI] 1); +by (eres_inst_tac [("x","{{x}. x:A}")] allE 1); +by (eresolve_tac [impE] 1); +by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS + well_ord_rvimage]) 2); +by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1); +by (fast_tac (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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO_AC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO_AC.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,22 @@ +(* Title: ZF/AC/WO_AC.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Lemmas used in the proofs like WO? ==> AC? +*) + +open WO_AC; + +goal thy "!!A. [| well_ord(Union(A),r); 0~:A; B:A |] \ +\ ==> (THE b. first(b,B,r)) : B"; +by (fast_tac (AC_cs addSEs [well_ord_imp_ex1_first RS theI RS + (first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1); +val first_in_B = result(); + +goal thy "!!A. [| well_ord(Union(A), R); 0~:A |] ==> EX f. f:(PROD X:A. X)"; +by (fast_tac (AC_cs addSEs [first_in_B] addSIs [lam_type]) 1); +val ex_choice_fun = result(); + +goal thy "!!A. well_ord(A, R) ==> 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 diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/WO_AC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/WO_AC.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,3 @@ +(*Dummy theory to document dependencies *) + +WO_AC = Order + first \ No newline at end of file diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/first.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/first.ML Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,41 @@ +(* Title: ZF/AC/first.ML + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Lemmas involving the first element of a well ordered set +*) + +open first; + +goalw thy [first_def] "!!b. first(b,B,r) ==> b:B"; +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)); +by (contr_tac 1); +by (eresolve_tac [bexE] 1); +by (res_inst_tac [("a","x")] ex1I 1); +by (fast_tac ZF_cs 2); +by (rewrite_goals_tac [tot_ord_def, linear_def]); +by (fast_tac ZF_cs 1); +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 (resolve_tac [first_is_elem] 1); +by (eresolve_tac [theI] 1); +val the_first_in = result(); diff -r 20b708827030 -r 5dfdc1464966 src/ZF/AC/first.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/first.thy Thu May 18 11:51:23 1995 +0200 @@ -0,0 +1,23 @@ +(* Title: ZF/AC/first.thy + ID: $Id$ + Author: Krzysztof Gr`abczewski + +Theory helpful in proofs using first element of a well ordered set +*) + +first = Order + + +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)" + +end \ No newline at end of file