# HG changeset patch # User paulson # Date 993567279 -7200 # Node ID e76366922751ffaa6fad8d6b96fb65c9f9d6f189 # Parent 0c90ffd3f3e29c7b9ef1df02ca115c9db7dd4496 tidying and consolidating files diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC0_AC1.ML --- a/src/ZF/AC/AC0_AC1.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* Title: ZF/AC/AC0_AC1.ML - ID: $Id$ - Author: Krzysztof Grabczewski - -AC0 is equivalent to AC1 -AC0 comes from Suppes, AC1 from Rubin & Rubin -*) - -Goal "0\\A ==> A \\ Pow(Union(A))-{0}"; -by (Fast_tac 1); -qed "subset_Pow_Union"; - -Goal "[| f:(\\X \\ A. X); D \\ A |] ==> \\g. g:(\\X \\ D. X)"; -by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1); -val lemma1 = result(); - -Goalw AC_defs "AC0 ==> AC1"; -by (fast_tac (FOL_cs addSEs [lemma1, subset_Pow_Union]) 1); -qed "AC0_AC1"; - -Goalw AC_defs "AC1 ==> AC0"; -by (Deepen_tac 0 1); -(*Large search space. Faster proof by - by (fast_tac (claset() addSIs [notI, singletonI] addSEs [notE, DiffE]) 1); -*) -qed "AC1_AC0"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC10_AC15.ML --- a/src/ZF/AC/AC10_AC15.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,255 +0,0 @@ -(* 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) ==> AC14 ==> AC15 (m le n) - -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. -*) - -(* ********************************************************************** *) -(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) -(* or AC15 *) -(* - cons_times_nat_not_Finite *) -(* - ex_fun_AC13_AC15 *) -(* ********************************************************************** *) - -Goalw [lepoll_def] "A\\0 ==> B lepoll A*B"; -by (etac not_emptyE 1); -by (res_inst_tac [("x","\\z \\ B. ")] exI 1); -by (fast_tac (claset() addSIs [snd_conv, lam_injective]) 1); -qed "lepoll_Sigma"; - -Goal "0\\A ==> \\B \\ {cons(0,x*nat). x \\ A}. ~Finite(B)"; -by (rtac ballI 1); -by (etac RepFunE 1); -by (hyp_subst_tac 1); -by (rtac 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 (assume_tac 2)); -by (Fast_tac 1); -qed "cons_times_nat_not_Finite"; - -Goal "[| Union(C)=A; a \\ A |] ==> \\B \\ C. a \\ B & B \\ A"; -by (Fast_tac 1); -val lemma1 = result(); - -Goalw [pairwise_disjoint_def] - "[| pairwise_disjoint(A); B \\ A; C \\ A; a \\ B; a \\ C |] ==> B=C"; -by (dtac IntI 1 THEN (assume_tac 1)); -by (dres_inst_tac [("A","B Int C")] not_emptyI 1); -by (Fast_tac 1); -val lemma2 = result(); - -Goalw [sets_of_size_between_def] - "\\B \\ {cons(0, x*nat). x \\ A}. pairwise_disjoint(f`B) & \ -\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ -\ ==> \\B \\ A. \\! u. u \\ f`cons(0, B*nat) & u \\ cons(0, B*nat) & \ -\ 0 \\ u & 2 lepoll u & u lepoll n"; -by (rtac ballI 1); -by (etac ballE 1); -by (Fast_tac 2); -by (REPEAT (etac conjE 1)); -by (dresolve_tac [consI1 RSN (2, lemma1)] 1); -by (etac bexE 1); -by (rtac ex1I 1); -by (Fast_tac 1); -by (REPEAT (etac conjE 1)); -by (rtac lemma2 1 THEN (REPEAT (assume_tac 1))); -val lemma3 = result(); - -Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a \\ A} lepoll i"; -by (etac exE 1); -by (res_inst_tac - [("x", "\\x \\ RepFun(A, P). LEAST j. \\a \\ A. x=P(a) & f`a=j")] exI 1); -by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); -by (etac RepFunE 1); -by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1)); -by (fast_tac (claset() addIs [LeastI2] - addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); -by (etac RepFunE 1); -by (rtac LeastI2 1); -by (Fast_tac 1); -by (fast_tac (claset() addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); -by (fast_tac (claset() addEs [sym, left_inverse RS ssubst]) 1); -val lemma4 = result(); - -Goal "[| n \\ nat; B \\ A; u(B) \\ cons(0, B*nat); 0 \\ u(B); 2 lepoll u(B); \ -\ u(B) lepoll succ(n) |] \ -\ ==> (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ 0 & \ -\ (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ B & \ -\ (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B lepoll n"; -by (Asm_simp_tac 1); -by (rtac conjI 1); -by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] - addDs [lepoll_Diff_sing] - addEs [lepoll_trans RS succ_lepoll_natE, ssubst] - addSIs [notI, lepoll_refl, nat_0I]) 1); -by (rtac conjI 1); -by (fast_tac (claset() addSIs [fst_type] addSEs [consE]) 1); -by (fast_tac (claset() addSEs [equalityE, - Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); -val lemma5 = result(); - -Goal "[| \\f. \\B \\ {cons(0, x*nat). x \\ A}. \ -\ pairwise_disjoint(f`B) & \ -\ sets_of_size_between(f`B, 2, succ(n)) & \ -\ Union(f`B)=B; n \\ nat |] \ -\ ==> \\f. \\B \\ A. f`B \\ 0 & f`B \\ B & f`B lepoll n"; -by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec] - addSEs [exE, conjE] - addIs [exI, ballI, lemma5]) 1); -qed "ex_fun_AC13_AC15"; - -(* ********************************************************************** *) -(* The target proofs *) -(* ********************************************************************** *) - -(* ********************************************************************** *) -(* AC10(n) ==> AC11 *) -(* ********************************************************************** *) - -Goalw AC_defs "[| n \\ nat; 1 le n; AC10(n) |] ==> AC11"; -by (rtac bexI 1 THEN (assume_tac 2)); -by (Fast_tac 1); -qed "AC10_AC11"; - -(* ********************************************************************** *) -(* AC11 ==> AC12 *) -(* ********************************************************************** *) - -Goalw AC_defs "AC11 ==> AC12"; -by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1); -qed "AC11_AC12"; - -(* ********************************************************************** *) -(* AC12 ==> AC15 *) -(* ********************************************************************** *) - -Goalw AC_defs "AC12 ==> AC15"; -by Safe_tac; -by (etac allE 1); -by (etac impE 1); -by (etac cons_times_nat_not_Finite 1); -by (fast_tac (claset() addSIs [ex_fun_AC13_AC15]) 1); -qed "AC12_AC15"; - -(* ********************************************************************** *) -(* 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 AC_defs "[| n \\ nat; 1 le n; AC10(n) |] ==> AC13(n)"; -by Safe_tac; -by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), - ex_fun_AC13_AC15]) 1); -qed "AC10_AC13"; - -(* ********************************************************************** *) -(* The proofs needed in the second case, not in the first *) -(* ********************************************************************** *) - -(* ********************************************************************** *) -(* AC1 ==> AC13(1) *) -(* ********************************************************************** *) - -Goalw AC_defs "AC1 ==> AC13(1)"; -by (rtac allI 1); -by (etac allE 1); -by (rtac impI 1); -by (mp_tac 1); -by (etac exE 1); -by (res_inst_tac [("x","\\x \\ A. {f`x}")] exI 1); -by (asm_simp_tac (simpset() addsimps - [singleton_eqpoll_1 RS eqpoll_imp_lepoll, - singletonI RS not_emptyI]) 1); -qed "AC1_AC13"; - -(* ********************************************************************** *) -(* AC13(m) ==> AC13(n) for m \\ n *) -(* ********************************************************************** *) - -Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)"; -by (dtac le_imp_lepoll 1); -by (fast_tac (claset() addSEs [lepoll_trans]) 1); -qed "AC13_mono"; - -(* ********************************************************************** *) -(* The proofs necessary for both cases *) -(* ********************************************************************** *) - -(* ********************************************************************** *) -(* AC13(n) ==> AC14 if 1 \\ n *) -(* ********************************************************************** *) - -Goalw AC_defs "[| n \\ nat; 1 le n; AC13(n) |] ==> AC14"; -by (fast_tac (FOL_cs addIs [bexI]) 1); -qed "AC13_AC14"; - -(* ********************************************************************** *) -(* AC14 ==> AC15 *) -(* ********************************************************************** *) - -Goalw AC_defs "AC14 ==> AC15"; -by (Fast_tac 1); -qed "AC14_AC15"; - -(* ********************************************************************** *) -(* The redundant proofs; however cited by Rubin & Rubin *) -(* ********************************************************************** *) - -(* ********************************************************************** *) -(* AC13(1) ==> AC1 *) -(* ********************************************************************** *) - -Goal "[| A\\0; A lepoll 1 |] ==> \\a. A={a}"; -by (fast_tac (claset() addSEs [not_emptyE, lepoll_1_is_sing]) 1); -qed "lemma_aux"; - -Goal "\\B \\ A. f(B)\\0 & f(B)<=B & f(B) lepoll 1 \ -\ ==> (\\x \\ A. THE y. f(x)={y}) \\ (\\X \\ A. X)"; -by (rtac lam_type 1); -by (dtac bspec 1 THEN (assume_tac 1)); -by (REPEAT (etac conjE 1)); -by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1)); -by (asm_full_simp_tac (simpset() addsimps [the_element]) 1); -val lemma = result(); - -Goalw AC_defs "AC13(1) ==> AC1"; -by (fast_tac (claset() addSEs [lemma]) 1); -qed "AC13_AC1"; - -(* ********************************************************************** *) -(* AC11 ==> AC14 *) -(* ********************************************************************** *) - -Goalw [AC11_def, AC14_def] "AC11 ==> AC14"; -by (fast_tac (claset() addSIs [AC10_AC13]) 1); -qed "AC11_AC14"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC15_WO6.ML --- a/src/ZF/AC/AC15_WO6.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/AC15_WO6.ML Tue Jun 26 16:54:39 2001 +0200 @@ -2,9 +2,156 @@ ID: $Id$ Author: Krzysztof Grabczewski -The proof of AC1 ==> WO2 +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) ==> AC14 ==> AC15 (m le n) + +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. *) +(* ********************************************************************** *) +(* Lemmas used in the proofs in which the conclusion is AC13, AC14 *) +(* or AC15 *) +(* - cons_times_nat_not_Finite *) +(* - ex_fun_AC13_AC15 *) +(* ********************************************************************** *) + +Goalw [lepoll_def] "A\\0 ==> B lepoll A*B"; +by (etac not_emptyE 1); +by (res_inst_tac [("x","\\z \\ B. ")] exI 1); +by (fast_tac (claset() addSIs [snd_conv, lam_injective]) 1); +qed "lepoll_Sigma"; + +Goal "0\\A ==> \\B \\ {cons(0,x*nat). x \\ A}. ~Finite(B)"; +by (rtac ballI 1); +by (etac RepFunE 1); +by (hyp_subst_tac 1); +by (rtac 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 (assume_tac 2)); +by (Fast_tac 1); +qed "cons_times_nat_not_Finite"; + +Goal "[| Union(C)=A; a \\ A |] ==> \\B \\ C. a \\ B & B \\ A"; +by (Fast_tac 1); +val lemma1 = result(); + +Goalw [pairwise_disjoint_def] + "[| pairwise_disjoint(A); B \\ A; C \\ A; a \\ B; a \\ C |] ==> B=C"; +by (dtac IntI 1 THEN (assume_tac 1)); +by (dres_inst_tac [("A","B Int C")] not_emptyI 1); +by (Fast_tac 1); +val lemma2 = result(); + +Goalw [sets_of_size_between_def] + "\\B \\ {cons(0, x*nat). x \\ A}. pairwise_disjoint(f`B) & \ +\ sets_of_size_between(f`B, 2, n) & Union(f`B)=B \ +\ ==> \\B \\ A. \\! u. u \\ f`cons(0, B*nat) & u \\ cons(0, B*nat) & \ +\ 0 \\ u & 2 lepoll u & u lepoll n"; +by (rtac ballI 1); +by (etac ballE 1); +by (Fast_tac 2); +by (REPEAT (etac conjE 1)); +by (dresolve_tac [consI1 RSN (2, lemma1)] 1); +by (etac bexE 1); +by (rtac ex1I 1); +by (Fast_tac 1); +by (REPEAT (etac conjE 1)); +by (rtac lemma2 1 THEN (REPEAT (assume_tac 1))); +val lemma3 = result(); + +Goalw [lepoll_def] "[| A lepoll i; Ord(i) |] ==> {P(a). a \\ A} lepoll i"; +by (etac exE 1); +by (res_inst_tac + [("x", "\\x \\ RepFun(A, P). LEAST j. \\a \\ A. x=P(a) & f`a=j")] exI 1); +by (res_inst_tac [("d", "%y. P(converse(f)`y)")] lam_injective 1); +by (etac RepFunE 1); +by (forward_tac [inj_is_fun RS apply_type] 1 THEN (assume_tac 1)); +by (fast_tac (claset() addIs [LeastI2] + addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); +by (etac RepFunE 1); +by (rtac LeastI2 1); +by (Fast_tac 1); +by (fast_tac (claset() addSEs [Ord_in_Ord, inj_is_fun RS apply_type]) 1); +by (fast_tac (claset() addEs [sym, left_inverse RS ssubst]) 1); +val lemma4 = result(); + +Goal "[| n \\ nat; B \\ A; u(B) \\ cons(0, B*nat); 0 \\ u(B); 2 lepoll u(B); \ +\ u(B) lepoll succ(n) |] \ +\ ==> (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ 0 & \ +\ (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B \\ B & \ +\ (\\x \\ A. {fst(x). x \\ u(x)-{0}})`B lepoll n"; +by (Asm_simp_tac 1); +by (rtac conjI 1); +by (fast_tac (empty_cs addSDs [RepFun_eq_0_iff RS iffD1] + addDs [lepoll_Diff_sing] + addEs [lepoll_trans RS succ_lepoll_natE, ssubst] + addSIs [notI, lepoll_refl, nat_0I]) 1); +by (rtac conjI 1); +by (fast_tac (claset() addSIs [fst_type] addSEs [consE]) 1); +by (fast_tac (claset() addSEs [equalityE, + Diff_lepoll RS (nat_into_Ord RSN (2, lemma4))]) 1); +val lemma5 = result(); + +Goal "[| \\f. \\B \\ {cons(0, x*nat). x \\ A}. \ +\ pairwise_disjoint(f`B) & \ +\ sets_of_size_between(f`B, 2, succ(n)) & \ +\ Union(f`B)=B; n \\ nat |] \ +\ ==> \\f. \\B \\ A. f`B \\ 0 & f`B \\ B & f`B lepoll n"; +by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec] + addSEs [exE, conjE] + addIs [exI, ballI, lemma5]) 1); +qed "ex_fun_AC13_AC15"; + +(* ********************************************************************** *) +(* The target proofs *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC10(n) ==> AC11 *) +(* ********************************************************************** *) + +Goalw AC_defs "[| n \\ nat; 1 le n; AC10(n) |] ==> AC11"; +by (rtac bexI 1 THEN (assume_tac 2)); +by (Fast_tac 1); +qed "AC10_AC11"; + +(* ********************************************************************** *) +(* AC11 ==> AC12 *) +(* ********************************************************************** *) + +Goalw AC_defs "AC11 ==> AC12"; +by (fast_tac (FOL_cs addSEs [bexE] addIs [bexI]) 1); +qed "AC11_AC12"; + +(* ********************************************************************** *) +(* AC12 ==> AC15 *) +(* ********************************************************************** *) + +Goalw AC_defs "AC12 ==> AC15"; +by Safe_tac; +by (etac allE 1); +by (etac impE 1); +by (etac cons_times_nat_not_Finite 1); +by (fast_tac (claset() addSIs [ex_fun_AC13_AC15]) 1); +qed "AC12_AC15"; + +(* ********************************************************************** *) +(* AC15 ==> WO6 *) +(* ********************************************************************** *) + Goal "Ord(x) ==> (\\aa \\ x. F(a))"; by (fast_tac (claset() addSIs [ltI] addSDs [ltD]) 1); qed "OUN_eq_UN"; @@ -42,3 +189,104 @@ by (fast_tac (claset() addSIs [Ord_Least, lam_type RS domain_of_fun] addSEs [less_Least_subset_x, lemma1, lemma2]) 1); qed "AC15_WO6"; + + +(* ********************************************************************** *) +(* 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 AC_defs "[| n \\ nat; 1 le n; AC10(n) |] ==> AC13(n)"; +by Safe_tac; +by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE), + ex_fun_AC13_AC15]) 1); +qed "AC10_AC13"; + +(* ********************************************************************** *) +(* The proofs needed in the second case, not in the first *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC1 ==> AC13(1) *) +(* ********************************************************************** *) + +Goalw AC_defs "AC1 ==> AC13(1)"; +by (rtac allI 1); +by (etac allE 1); +by (rtac impI 1); +by (mp_tac 1); +by (etac exE 1); +by (res_inst_tac [("x","\\x \\ A. {f`x}")] exI 1); +by (asm_simp_tac (simpset() addsimps + [singleton_eqpoll_1 RS eqpoll_imp_lepoll, + singletonI RS not_emptyI]) 1); +qed "AC1_AC13"; + +(* ********************************************************************** *) +(* AC13(m) ==> AC13(n) for m \\ n *) +(* ********************************************************************** *) + +Goalw AC_defs "[| m le n; AC13(m) |] ==> AC13(n)"; +by (dtac le_imp_lepoll 1); +by (fast_tac (claset() addSEs [lepoll_trans]) 1); +qed "AC13_mono"; + +(* ********************************************************************** *) +(* The proofs necessary for both cases *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC13(n) ==> AC14 if 1 \\ n *) +(* ********************************************************************** *) + +Goalw AC_defs "[| n \\ nat; 1 le n; AC13(n) |] ==> AC14"; +by (fast_tac (FOL_cs addIs [bexI]) 1); +qed "AC13_AC14"; + +(* ********************************************************************** *) +(* AC14 ==> AC15 *) +(* ********************************************************************** *) + +Goalw AC_defs "AC14 ==> AC15"; +by (Fast_tac 1); +qed "AC14_AC15"; + +(* ********************************************************************** *) +(* The redundant proofs; however cited by Rubin & Rubin *) +(* ********************************************************************** *) + +(* ********************************************************************** *) +(* AC13(1) ==> AC1 *) +(* ********************************************************************** *) + +Goal "[| A\\0; A lepoll 1 |] ==> \\a. A={a}"; +by (fast_tac (claset() addSEs [not_emptyE, lepoll_1_is_sing]) 1); +qed "lemma_aux"; + +Goal "\\B \\ A. f(B)\\0 & f(B)<=B & f(B) lepoll 1 \ +\ ==> (\\x \\ A. THE y. f(x)={y}) \\ (\\X \\ A. X)"; +by (rtac lam_type 1); +by (dtac bspec 1 THEN (assume_tac 1)); +by (REPEAT (etac conjE 1)); +by (eresolve_tac [lemma_aux RS exE] 1 THEN (assume_tac 1)); +by (asm_full_simp_tac (simpset() addsimps [the_element]) 1); +val lemma = result(); + +Goalw AC_defs "AC13(1) ==> AC1"; +by (fast_tac (claset() addSEs [lemma]) 1); +qed "AC13_AC1"; + +(* ********************************************************************** *) +(* AC11 ==> AC14 *) +(* ********************************************************************** *) + +Goalw [AC11_def, AC14_def] "AC11 ==> AC14"; +by (fast_tac (claset() addSIs [AC10_AC13]) 1); +qed "AC11_AC14"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC16_WO4.ML --- a/src/ZF/AC/AC16_WO4.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/AC16_WO4.ML Tue Jun 26 16:54:39 2001 +0200 @@ -89,33 +89,20 @@ (* There is a k-2 element subset of y *) (* ********************************************************************** *) -Goalw [lepoll_def, eqpoll_def] - "[| n \\ nat; nat lepoll X |] ==> \\Y. Y \\ X & n eqpoll Y"; -by (fast_tac (subset_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] - addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); -qed "nat_lepoll_imp_ex_eqpoll_n"; - val ordertype_eqpoll = ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); -Goalw [lesspoll_def] "n \\ nat ==> n lesspoll nat"; -by (fast_tac (claset() addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, - eqpoll_sym RS eqpoll_imp_lepoll] - addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI - RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1); -qed "n_lesspoll_nat"; - Goal "[| a \\ y; b \\ y-a; u \\ x |] ==> cons(b, cons(u, a)) \\ Pow(x Un y)"; by (Fast_tac 1); qed "cons_cons_subset"; -Goal "[| a eqpoll k; a \\ y; b \\ y-a; u \\ x; x Int y = 0 \ -\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; +Goal "[| a eqpoll k; a \\ y; b \\ y-a; u \\ x; x Int y = 0 |] \ +\ ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1); qed "cons_cons_eqpoll"; -Goal "[| succ(k) eqpoll A; k eqpoll B; B \\ A; a \\ A-B; k \\ nat \ -\ |] ==> A = cons(a, B)"; +Goal "[| succ(k) eqpoll A; k eqpoll B; B \\ A; a \\ A-B; k \\ nat |] \ +\ ==> A = cons(a, B)"; by (rtac equalityI 1); by (Fast_tac 2); by (resolve_tac [Diff_eq_0_iff RS iffD1] 1); diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC17_AC1.ML --- a/src/ZF/AC/AC17_AC1.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/AC17_AC1.ML Tue Jun 26 16:54:39 2001 +0200 @@ -1,10 +1,54 @@ -(* Title: ZF/AC/AC17_AC1.ML +(* Title: ZF/AC/AC1_AC17.ML ID: $Id$ Author: Krzysztof Grabczewski -The proof of AC1 ==> AC17 +The equivalence of AC0, AC1 and AC17 + +Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent +to AC0 and AC1. *) + +(** AC0 is equivalent to AC1. + AC0 comes from Suppes, AC1 from Rubin & Rubin **) + +Goal "[| f:(\\X \\ A. X); D \\ A |] ==> \\g. g:(\\X \\ D. X)"; +by (fast_tac (claset() addSIs [restrict_type, apply_type]) 1); +val lemma1 = result(); + +Goalw AC_defs "AC0 ==> AC1"; +by (blast_tac (claset() addIs [lemma1]) 1); +qed "AC0_AC1"; + +Goalw AC_defs "AC1 ==> AC0"; +by (Blast_tac 1); +qed "AC1_AC0"; + + +(**** The proof of AC1 ==> AC17 ****) + +Goal "f \\ (\\X \\ Pow(A) - {0}. X) ==> f \\ (Pow(A) - {0} -> A)"; +by (rtac Pi_type 1 THEN (assume_tac 1)); +by (dtac apply_type 1 THEN (assume_tac 1)); +by (Fast_tac 1); +val lemma1 = result(); + +Goalw AC_defs "AC1 ==> AC17"; +by (rtac allI 1); +by (rtac ballI 1); +by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); +by (etac impE 1); +by (Fast_tac 1); +by (etac exE 1); +by (rtac bexI 1); +by (etac lemma1 2); +by (rtac apply_type 1 THEN (assume_tac 1)); +by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1); +qed "AC1_AC17"; + + +(**** The proof of AC17 ==> AC1 ****) + (* *********************************************************************** *) (* more properties of HH *) (* *********************************************************************** *) @@ -87,3 +131,180 @@ by (fast_tac (claset() addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem), f_subset_imp_HH_subset] addSEs [mem_irrefl]) 1); qed "AC17_AC1"; + + +(* ********************************************************************** + AC1 ==> AC2 ==> AC1 + AC1 ==> AC4 ==> AC3 ==> AC1 + AC4 ==> AC5 ==> AC4 + AC1 <-> AC6 +************************************************************************* *) + +(* ********************************************************************** *) +(* AC1 ==> AC2 *) +(* ********************************************************************** *) + +Goal "[| f:(\\X \\ A. X); B \\ A; 0\\A |] ==> {f`B} \\ B Int {f`C. C \\ A}"; +by (fast_tac (claset() addSEs [apply_type]) 1); +val lemma1 = result(); + +Goalw [pairwise_disjoint_def] + "[| pairwise_disjoint(A); B \\ A; C \\ A; D \\ B; D \\ C |] ==> f`B = f`C"; +by (Fast_tac 1); +val lemma2 = result(); + +Goalw AC_defs "AC1 ==> AC2"; +by (rtac allI 1); +by (rtac impI 1); +by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1)); +by (REPEAT (resolve_tac [exI,ballI,equalityI] 1)); +by (rtac lemma1 2 THEN (REPEAT (assume_tac 2))); +by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1); +qed "AC1_AC2"; + + +(* ********************************************************************** *) +(* AC2 ==> AC1 *) +(* ********************************************************************** *) + +Goal "0\\A ==> 0 \\ {B*{B}. B \\ A}"; +by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1); +val lemma1 = result(); + +Goal "[| X*{X} Int C = {y}; X \\ A |] \ +\ ==> (THE y. X*{X} Int C = {y}): X*A"; +by (rtac subst_elem 1); +by (fast_tac (claset() addSIs [the_equality] + addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); +by (blast_tac (claset() addSEs [equalityE]) 1); +val lemma2 = result(); + +Goal "\\D \\ {E*{E}. E \\ A}. \\y. D Int C = {y} \ +\ ==> (\\x \\ A. fst(THE z. (x*{x} Int C = {z}))) \\ (\\X \\ A. X)"; +by (fast_tac (claset() addSEs [lemma2] + addSIs [lam_type, RepFunI, fst_type]) 1); +val lemma3 = result(); + +Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1"; +by (REPEAT (resolve_tac [allI, impI] 1)); +by (REPEAT (eresolve_tac [allE, impE] 1)); +by (fast_tac (claset() addSEs [lemma3]) 2); +by (fast_tac (claset() addSIs [lemma1, equals0I]) 1); +qed "AC2_AC1"; + + +(* ********************************************************************** *) +(* AC1 ==> AC4 *) +(* ********************************************************************** *) + +Goal "0 \\ {R``{x}. x \\ domain(R)}"; +by (Blast_tac 1); +val lemma = result(); + +Goalw AC_defs "AC1 ==> AC4"; +by (REPEAT (resolve_tac [allI, impI] 1)); +by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1)); +by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1); +qed "AC1_AC4"; + + +(* ********************************************************************** *) +(* AC4 ==> AC3 *) +(* ********************************************************************** *) + +Goal "f \\ A->B ==> (\\z \\ A. {z}*f`z) \\ A*Union(B)"; +by (fast_tac (claset() addSDs [apply_type]) 1); +val lemma1 = result(); + +Goal "domain(\\z \\ A. {z}*f(z)) = {a \\ A. f(a)\\0}"; +by (Blast_tac 1); +val lemma2 = result(); + +Goal "x \\ A ==> (\\z \\ A. {z}*f(z))``{x} = f(x)"; +by (Fast_tac 1); +val lemma3 = result(); + +Goalw AC_defs "AC4 ==> AC3"; +by (REPEAT (resolve_tac [allI,ballI] 1)); +by (REPEAT (eresolve_tac [allE,impE] 1)); +by (etac lemma1 1); +by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3] + addcongs [Pi_cong]) 1); +qed "AC4_AC3"; + +(* ********************************************************************** *) +(* AC3 ==> AC1 *) +(* ********************************************************************** *) + +Goal "b\\A ==> (\\x \\ {a \\ A. id(A)`a\\b}. id(A)`x) = (\\x \\ A. x)"; +by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1); +by (res_inst_tac [("b","A")] subst_context 1); +by (Fast_tac 1); +val lemma = result(); + +Goalw AC_defs "AC3 ==> AC1"; +by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1); +qed "AC3_AC1"; + +(* ********************************************************************** *) +(* AC4 ==> AC5 *) +(* ********************************************************************** *) + +Goalw (range_def::AC_defs) "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 (etac exE 1); +by (rtac bexI 1); +by (rtac Pi_type 2 THEN (assume_tac 2)); +by (fast_tac (claset() addSDs [apply_type] + addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); +by (rtac ballI 1); +by (rtac apply_equality 1 THEN (assume_tac 2)); +by (etac domainE 1); +by (ftac range_type 1 THEN (assume_tac 1)); +by (fast_tac (claset() addDs [apply_equality]) 1); +qed "AC4_AC5"; + + +(* ********************************************************************** *) +(* AC5 ==> AC4, Rubin & Rubin, p. 11 *) +(* ********************************************************************** *) + +Goal "R \\ A*B ==> (\\x \\ R. fst(x)) \\ R -> A"; +by (fast_tac (claset() addSIs [lam_type, fst_type]) 1); +val lemma1 = result(); + +Goalw [range_def] "R \\ A*B ==> range(\\x \\ R. fst(x)) = domain(R)"; +by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE], + simpset()) 1); +val lemma2 = result(); + +Goal "[| \\f \\ A->C. P(f,domain(f)); A=B |] ==> \\f \\ B->C. P(f,B)"; +by (etac bexE 1); +by (ftac domain_of_fun 1); +by (Fast_tac 1); +val lemma3 = result(); + +Goal "[| R \\ A*B; g \\ C->R; \\x \\ C. (\\z \\ R. fst(z))` (g`x) = x |] \ +\ ==> (\\x \\ C. snd(g`x)): (\\x \\ C. R``{x})"; +by (rtac lam_type 1); +by (force_tac (claset() addDs [apply_type], simpset()) 1); +val lemma4 = result(); + +Goalw AC_defs "AC5 ==> AC4"; +by (Clarify_tac 1); +by (REPEAT (eresolve_tac [allE,ballE] 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 (claset() addSEs [lemma4]) 1); +qed "AC5_AC4"; + + +(* ********************************************************************** *) +(* AC1 <-> AC6 *) +(* ********************************************************************** *) + +Goalw AC_defs "AC1 <-> AC6"; +by (Blast_tac 1); +qed "AC1_iff_AC6"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC1_AC17.ML --- a/src/ZF/AC/AC1_AC17.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: ZF/AC/AC1_AC17.ML - ID: $Id$ - Author: Krzysztof Grabczewski - -The proof of AC1 ==> AC17 -*) - -Goal "f \\ (\\X \\ Pow(A) - {0}. X) ==> f \\ (Pow(A) - {0} -> A)"; -by (rtac Pi_type 1 THEN (assume_tac 1)); -by (dtac apply_type 1 THEN (assume_tac 1)); -by (Fast_tac 1); -val lemma1 = result(); - -Goalw AC_defs "AC1 ==> AC17"; -by (rtac allI 1); -by (rtac ballI 1); -by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1); -by (etac impE 1); -by (Fast_tac 1); -by (etac exE 1); -by (rtac bexI 1); -by (etac lemma1 2); -by (rtac apply_type 1 THEN (assume_tac 1)); -by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1); -qed "AC1_AC17"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/AC2_AC6.ML --- a/src/ZF/AC/AC2_AC6.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,180 +0,0 @@ -(* Title: ZF/AC/AC2_AC6.ML - ID: $Id$ - Author: Krzysztof Grabczewski - -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 -AC1 <-> AC6 -*) - -(* ********************************************************************** *) -(* AC1 ==> AC2 *) -(* ********************************************************************** *) - -Goal "[| f:(\\X \\ A. X); B \\ A; 0\\A |] ==> {f`B} \\ B Int {f`C. C \\ A}"; -by (fast_tac (claset() addSEs [apply_type]) 1); -val lemma1 = result(); - -Goalw [pairwise_disjoint_def] - "[| pairwise_disjoint(A); B \\ A; C \\ A; D \\ B; D \\ C |] ==> f`B = f`C"; -by (Fast_tac 1); -val lemma2 = result(); - -Goalw AC_defs "AC1 ==> AC2"; -by (rtac allI 1); -by (rtac impI 1); -by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1)); -by (REPEAT (resolve_tac [exI,ballI,equalityI] 1)); -by (rtac lemma1 2 THEN (REPEAT (assume_tac 2))); -by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1); -qed "AC1_AC2"; - - -(* ********************************************************************** *) -(* AC2 ==> AC1 *) -(* ********************************************************************** *) - -Goal "0\\A ==> 0 \\ {B*{B}. B \\ A}"; -by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1); -val lemma1 = result(); - -Goal "[| X*{X} Int C = {y}; X \\ A |] \ -\ ==> (THE y. X*{X} Int C = {y}): X*A"; -by (rtac subst_elem 1); -by (fast_tac (claset() addSIs [the_equality] - addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); -by (blast_tac (claset() addSEs [equalityE]) 1); -val lemma2 = result(); - -Goal "\\D \\ {E*{E}. E \\ A}. \\y. D Int C = {y} \ -\ ==> (\\x \\ A. fst(THE z. (x*{x} Int C = {z}))) \\ (\\X \\ A. X)"; -by (fast_tac (claset() addSEs [lemma2] - addSIs [lam_type, RepFunI, fst_type]) 1); -val lemma3 = result(); - -Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1"; -by (REPEAT (resolve_tac [allI, impI] 1)); -by (REPEAT (eresolve_tac [allE, impE] 1)); -by (fast_tac (claset() addSEs [lemma3]) 2); -by (fast_tac (claset() addSIs [lemma1, equals0I]) 1); -qed "AC2_AC1"; - - -(* ********************************************************************** *) -(* AC1 ==> AC4 *) -(* ********************************************************************** *) - -Goal "0 \\ {R``{x}. x \\ domain(R)}"; -by (Blast_tac 1); -val lemma = result(); - -Goalw AC_defs "AC1 ==> AC4"; -by (REPEAT (resolve_tac [allI, impI] 1)); -by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1)); -by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1); -qed "AC1_AC4"; - - -(* ********************************************************************** *) -(* AC4 ==> AC3 *) -(* ********************************************************************** *) - -Goal "f \\ A->B ==> (\\z \\ A. {z}*f`z) \\ A*Union(B)"; -by (fast_tac (claset() addSDs [apply_type]) 1); -val lemma1 = result(); - -Goal "domain(\\z \\ A. {z}*f(z)) = {a \\ A. f(a)\\0}"; -by (Blast_tac 1); -val lemma2 = result(); - -Goal "x \\ A ==> (\\z \\ A. {z}*f(z))``{x} = f(x)"; -by (Fast_tac 1); -val lemma3 = result(); - -Goalw AC_defs "AC4 ==> AC3"; -by (REPEAT (resolve_tac [allI,ballI] 1)); -by (REPEAT (eresolve_tac [allE,impE] 1)); -by (etac lemma1 1); -by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3] - addcongs [Pi_cong]) 1); -qed "AC4_AC3"; - -(* ********************************************************************** *) -(* AC3 ==> AC1 *) -(* ********************************************************************** *) - -Goal "b\\A ==> (\\x \\ {a \\ A. id(A)`a\\b}. id(A)`x) = (\\x \\ A. x)"; -by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1); -by (res_inst_tac [("b","A")] subst_context 1); -by (Fast_tac 1); -val lemma = result(); - -Goalw AC_defs "AC3 ==> AC1"; -by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1); -qed "AC3_AC1"; - -(* ********************************************************************** *) -(* AC4 ==> AC5 *) -(* ********************************************************************** *) - -Goalw (range_def::AC_defs) "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 (etac exE 1); -by (rtac bexI 1); -by (rtac Pi_type 2 THEN (assume_tac 2)); -by (fast_tac (claset() addSDs [apply_type] - addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); -by (rtac ballI 1); -by (rtac apply_equality 1 THEN (assume_tac 2)); -by (etac domainE 1); -by (ftac range_type 1 THEN (assume_tac 1)); -by (fast_tac (claset() addDs [apply_equality]) 1); -qed "AC4_AC5"; - - -(* ********************************************************************** *) -(* AC5 ==> AC4, Rubin & Rubin, p. 11 *) -(* ********************************************************************** *) - -Goal "R \\ A*B ==> (\\x \\ R. fst(x)) \\ R -> A"; -by (fast_tac (claset() addSIs [lam_type, fst_type]) 1); -val lemma1 = result(); - -Goalw [range_def] "R \\ A*B ==> range(\\x \\ R. fst(x)) = domain(R)"; -by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE], - simpset()) 1); -val lemma2 = result(); - -Goal "[| \\f \\ A->C. P(f,domain(f)); A=B |] ==> \\f \\ B->C. P(f,B)"; -by (etac bexE 1); -by (ftac domain_of_fun 1); -by (Fast_tac 1); -val lemma3 = result(); - -Goal "[| R \\ A*B; g \\ C->R; \\x \\ C. (\\z \\ R. fst(z))` (g`x) = x |] \ -\ ==> (\\x \\ C. snd(g`x)): (\\x \\ C. R``{x})"; -by (rtac lam_type 1); -by (force_tac (claset() addDs [apply_type], simpset()) 1); -val lemma4 = result(); - -Goalw AC_defs "AC5 ==> AC4"; -by (Clarify_tac 1); -by (REPEAT (eresolve_tac [allE,ballE] 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 (claset() addSEs [lemma4]) 1); -qed "AC5_AC4"; - - -(* ********************************************************************** *) -(* AC1 <-> AC6 *) -(* ********************************************************************** *) - -Goalw AC_defs "AC1 <-> AC6"; -by (Blast_tac 1); -qed "AC1_iff_AC6"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/DC.ML Tue Jun 26 16:54:39 2001 +0200 @@ -199,11 +199,6 @@ ************************************************************************* *) -Goalw [lesspoll_def, Finite_def] - "A lesspoll nat ==> Finite(A)"; -by (fast_tac (claset() addSDs [ltD, lepoll_imp_ex_le_eqpoll]) 1); -qed "lesspoll_nat_is_Finite"; - Goal "n \\ nat ==> \\A. (A eqpoll n & A \\ X) --> A \\ Fin(X)"; by (induct_tac "n" 1); by (rtac allI 1); diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/ROOT.ML --- a/src/ZF/AC/ROOT.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/ROOT.ML Tue Jun 26 16:54:39 2001 +0200 @@ -8,25 +8,19 @@ time_use_thy "AC_Equiv"; -time_use "WO1_WO6.ML"; time_use_thy "WO6_WO1"; time_use_thy "WO1_WO7"; -time_use "WO1_WO8.ML"; -time_use "AC0_AC1.ML"; -time_use "AC2_AC6.ML"; time_use "AC7_AC9.ML"; time_use_thy "WO1_AC"; time_use_thy "AC1_WO2"; -time_use "AC10_AC15.ML"; time_use_thy "AC15_WO6"; time_use_thy "WO2_AC16"; time_use_thy "AC16_WO4"; -time_use "AC1_AC17.ML"; time_use_thy "AC17_AC1"; time_use_thy "AC18_AC19"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/WO1_WO6.ML --- a/src/ZF/AC/WO1_WO6.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -(* Title: ZF/AC/WO1_WO6.ML - ID: $Id$ - Author: Krzysztof Grabczewski - - Proofs needed to state that formulations WO1,...,WO6 are all equivalent. - All but one WO6 ==> WO1 (placed in separate file WO6_WO1.ML) - - Every proof (exept one) presented in this file are referred as "clear" - by Rubin & Rubin (page 2). - They refer reader to a book by Gödel to see the proof WO1 ==> WO2. - Fortunately order types made this proof also very easy. -*) - -(* ********************************************************************** *) - -Goalw WO_defs "WO2 ==> WO3"; -by (Fast_tac 1); -qed "WO2_WO3"; - -(* ********************************************************************** *) - -Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; -by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, - well_ord_Memrel RS well_ord_subset]) 1); -qed "WO3_WO1"; - -(* ********************************************************************** *) - -Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; -by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); -qed "WO1_WO2"; - -(* ********************************************************************** *) - -Goal "f \\ A->B ==> (\\x \\ A. {f`x}): A -> {{b}. b \\ B}"; -by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); -qed "lam_sets"; - -Goalw [surj_def] "f \\ surj(A,B) ==> (\\a \\ A. {f`a}) = B"; -by (fast_tac (claset() addSEs [apply_type]) 1); -qed "surj_imp_eq_"; - -Goal "[| f \\ surj(A,B); Ord(A) |] ==> (\\a WO4(1)"; -by (rtac allI 1); -by (eres_inst_tac [("x","A")] allE 1); -by (etac exE 1); -by (REPEAT (resolve_tac [exI, conjI] 1)); -by (etac Ord_ordertype 1); -by (rtac 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 (simpset() 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); -qed "WO1_WO4"; - -(* ********************************************************************** *) - -Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)"; -by (blast_tac (claset() addSDs [spec] - addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1); -qed "WO4_mono"; - -(* ********************************************************************** *) - -Goalw WO_defs "[| m \\ nat; 1 le m; WO4(m) |] ==> WO5"; -by (Blast_tac 1); -qed "WO4_WO5"; - -(* ********************************************************************** *) - -Goalw WO_defs "WO5 ==> WO6"; -by (Blast_tac 1); -qed "WO5_WO6"; - diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/WO1_WO7.ML --- a/src/ZF/AC/WO1_WO7.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/WO1_WO7.ML Tue Jun 26 16:54:39 2001 +0200 @@ -4,6 +4,8 @@ WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5) LEMMA is the sentence denoted by (**) + +Also, WO1 <-> WO8 *) (* ********************************************************************** *) @@ -86,3 +88,28 @@ by (simp_tac (simpset() addsimps [WO7_iff_LEMMA]) 1); by (blast_tac (claset() addIs [LEMMA_imp_WO1, WO1_imp_LEMMA]) 1); qed "WO1_iff_WO7"; + + + +(* ********************************************************************** *) + +(* The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) *) + +(* ********************************************************************** *) + +Goalw WO_defs "WO1 ==> WO8"; +by (Fast_tac 1); +qed "WO1_WO8"; + + +(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) +Goalw WO_defs "WO8 ==> WO1"; +by (rtac allI 1); +by (eres_inst_tac [("x","{{x}. x \\ A}")] allE 1); +by (etac impE 1); +by (fast_tac (claset() addSEs [lam_sing_bij RS bij_is_inj RS + well_ord_rvimage]) 2); +by (res_inst_tac [("x","\\a \\ {{x}. x \\ A}. THE x. a={x}")] exI 1); +by (force_tac (claset() addSIs [lam_type], + simpset() addsimps [singleton_eq_iff, the_equality]) 1); +qed "WO8_WO1"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/WO1_WO8.ML --- a/src/ZF/AC/WO1_WO8.ML Tue Jun 26 15:28:49 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ -(* Title: ZF/AC/WO1_WO8.ML - ID: $Id$ - Author: Krzysztof Grabczewski - -The proof of WO8 <-> WO1 (Rubin & Rubin p. 6) -*) - -(* ********************************************************************** *) -(* Trivial implication "WO1 ==> WO8" *) -(* ********************************************************************** *) - -Goalw WO_defs "WO1 ==> WO8"; -by (Fast_tac 1); -qed "WO1_WO8"; - -(* ********************************************************************** *) -(* The proof of "WO8 ==> WO1" - faithful image of Rubin & Rubin's proof *) -(* ********************************************************************** *) - -Goalw WO_defs "WO8 ==> WO1"; -by (rtac allI 1); -by (eres_inst_tac [("x","{{x}. x \\ A}")] allE 1); -by (etac impE 1); -by (fast_tac (claset() addSEs [lam_sing_bij RS bij_is_inj RS - well_ord_rvimage]) 2); -by (res_inst_tac [("x","\\a \\ {{x}. x \\ A}. THE x. a={x}")] exI 1); -by (force_tac (claset() addSIs [lam_type], - simpset() addsimps [singleton_eq_iff, the_equality]) 1); -qed "WO8_WO1"; diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/AC/WO6_WO1.ML --- a/src/ZF/AC/WO6_WO1.ML Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/AC/WO6_WO1.ML Tue Jun 26 16:54:39 2001 +0200 @@ -2,11 +2,89 @@ ID: $Id$ Author: Krzysztof Grabczewski -The proof of "WO6 ==> WO1". Simplified by L C Paulson. + Proofs needed to state that formulations WO1,...,WO6 are all equivalent. + The only hard one is WO6 ==> WO1. + + Every proof (except WO6 ==> WO1 and WO1 ==> WO2) are described as "clear" + by Rubin & Rubin (page 2). + They refer reader to a book by Gödel to see the proof WO1 ==> WO2. + Fortunately order types made this proof also very easy. +*) + +(* ********************************************************************** *) + +Goalw WO_defs "WO2 ==> WO3"; +by (Fast_tac 1); +qed "WO2_WO3"; + +(* ********************************************************************** *) + +Goalw (eqpoll_def::WO_defs) "WO3 ==> WO1"; +by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage, + well_ord_Memrel RS well_ord_subset]) 1); +qed "WO3_WO1"; + +(* ********************************************************************** *) + +Goalw (eqpoll_def::WO_defs) "WO1 ==> WO2"; +by (fast_tac (claset() addSIs [Ord_ordertype, ordermap_bij]) 1); +qed "WO1_WO2"; + +(* ********************************************************************** *) + +Goal "f \\ A->B ==> (\\x \\ A. {f`x}): A -> {{b}. b \\ B}"; +by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); +qed "lam_sets"; + +Goalw [surj_def] "f \\ surj(A,B) ==> (\\a \\ A. {f`a}) = B"; +by (fast_tac (claset() addSEs [apply_type]) 1); +qed "surj_imp_eq_"; -From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, -pages 2-5 -*) +Goal "[| f \\ surj(A,B); Ord(A) |] ==> (\\a WO4(1)"; +by (rtac allI 1); +by (eres_inst_tac [("x","A")] allE 1); +by (etac exE 1); +by (REPEAT (resolve_tac [exI, conjI] 1)); +by (etac Ord_ordertype 1); +by (rtac 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 (simpset() 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); +qed "WO1_WO4"; + +(* ********************************************************************** *) + +Goalw WO_defs "[| m le n; WO4(m) |] ==> WO4(n)"; +by (blast_tac (claset() addSDs [spec] + addIs [le_imp_lepoll RSN (2, lepoll_trans)]) 1); +qed "WO4_mono"; + +(* ********************************************************************** *) + +Goalw WO_defs "[| m \\ nat; 1 le m; WO4(m) |] ==> WO5"; +by (Blast_tac 1); +qed "WO4_WO5"; + +(* ********************************************************************** *) + +Goalw WO_defs "WO5 ==> WO6"; +by (Blast_tac 1); +qed "WO5_WO6"; + + +(* ********************************************************************** + The proof of "WO6 ==> WO1". Simplified by L C Paulson. + + From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin, + pages 2-5 +************************************************************************* *) goal OrderType.thy "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==> \ diff -r 0c90ffd3f3e2 -r e76366922751 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Jun 26 15:28:49 2001 +0200 +++ b/src/ZF/IsaMakefile Tue Jun 26 16:54:39 2001 +0200 @@ -77,15 +77,15 @@ ZF-AC: ZF $(LOG)/ZF-AC.gz -$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/AC0_AC1.ML AC/AC10_AC15.ML \ +$(LOG)/ZF-AC.gz: $(OUT)/ZF \ AC/AC15_WO6.ML AC/AC15_WO6.thy AC/AC16_WO4.ML AC/AC16_WO4.thy \ AC/AC16_lemmas.ML AC/AC16_lemmas.thy AC/AC17_AC1.ML AC/AC17_AC1.thy \ - AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_AC17.ML AC/AC1_WO2.ML \ - AC/AC1_WO2.thy AC/AC2_AC6.ML AC/AC7_AC9.ML AC/AC_Equiv.ML \ + AC/AC18_AC19.ML AC/AC18_AC19.thy AC/AC1_WO2.ML \ + AC/AC1_WO2.thy AC/AC7_AC9.ML AC/AC_Equiv.ML \ AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \ AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \ AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \ - AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO1_WO8.ML AC/WO2_AC16.ML \ + AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO2_AC16.ML \ AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \ AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy @$(ISATOOL) usedir $(OUT)/ZF AC