# HG changeset patch # User paulson # Date 1011260159 -3600 # Node ID 3ecbc37befab76abe6eb45a629481dbb45d39ae3 # Parent d655138ddadf5a35075ede534792dca3413299ab mistakenly deleted this theory diff -r d655138ddadf -r 3ecbc37befab src/ZF/AC/AC7_AC9.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC/AC7_AC9.thy Thu Jan 17 10:35:59 2002 +0100 @@ -0,0 +1,168 @@ +(* Title: ZF/AC/AC7_AC9.thy + ID: $Id$ + Author: Krzysztof Grabczewski + +The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous +instances of AC. +*) + +theory AC7_AC9 = AC_Equiv: + +(* ********************************************************************** *) +(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *) +(* - Sigma_fun_space_not0 *) +(* - Sigma_fun_space_eqpoll *) +(* ********************************************************************** *) + +lemma Sigma_fun_space_not0: "[| 0\A; B \ A |] ==> (nat->Union(A)) * B \ 0" +by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1]) + +lemma inj_lemma: + "C \ A ==> (\g \ (nat->Union(A))*C. + (\n \ nat. if(n=0, snd(g), fst(g)`(n #- 1)))) + \ inj((nat->Union(A))*C, (nat->Union(A)) ) " +apply (unfold inj_def) +apply (rule CollectI) +apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) +apply (rule fun_extension, assumption+) +apply (drule lam_eqE [OF _ nat_succI], assumption, simp) +apply (drule lam_eqE [OF _ nat_0I], simp) +done + +lemma Sigma_fun_space_eqpoll: + "[| C \ A; 0\A |] ==> (nat->Union(A)) * C \ (nat->Union(A))" +apply (rule eqpollI) +apply (simp add: lepoll_def) +apply (fast intro!: inj_lemma) +apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem + elim: swap) +done + + +(* ********************************************************************** *) +(* AC6 ==> AC7 *) +(* ********************************************************************** *) + +lemma AC6_AC7: "AC6 ==> AC7" +by (unfold AC6_def AC7_def, blast) + +(* ********************************************************************** *) +(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) +(* The case of the empty family of sets added in order to complete *) +(* the proof. *) +(* ********************************************************************** *) + +lemma lemma1_1: "y \ (\B \ A. Y*B) ==> (\B \ A. snd(y`B)) \ (\B \ A. B)" +by (fast intro!: lam_type snd_type apply_type) + +lemma lemma1_2: + "y \ (\B \ {Y*C. C \ A}. B) ==> (\B \ A. y`(Y*B)) \ (\B \ A. Y*B)" +apply (fast intro!: lam_type apply_type) +done + +lemma AC7_AC6_lemma1: + "(\B \ {(nat->Union(A))*C. C \ A}. B) \ 0 ==> (\B \ A. B) \ 0" +by (fast intro!: equals0I lemma1_1 lemma1_2) + +lemma AC7_AC6_lemma2: "0 \ A ==> 0 \ {(nat -> Union(A)) * C. C \ A}" +by (blast dest: Sigma_fun_space_not0) + +lemma AC7_AC6: "AC7 ==> AC6" +apply (unfold AC6_def AC7_def) +apply (rule allI) +apply (rule impI) +apply (case_tac "A=0", simp) +apply (rule AC7_AC6_lemma1) +apply (erule allE) +apply (blast del: notI + intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans + Sigma_fun_space_eqpoll) +done + + +(* ********************************************************************** *) +(* AC1 ==> AC8 *) +(* ********************************************************************** *) + +lemma AC1_AC8_lemma1: + "\B \ A. \B1 B2. B= & B1 \ B2 + ==> 0 \ { bij(fst(B),snd(B)). B \ A }" +apply (unfold eqpoll_def, auto) +done + +lemma AC1_AC8_lemma2: + "[| f \ (\X \ RepFun(A,p). X); D \ A |] ==> (\x \ A. f`p(x))`D \ p(D)" +apply (simp, fast elim!: apply_type) +done + +lemma AC1_AC8: "AC1 ==> AC8" +apply (unfold AC1_def AC8_def) +apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2) +done + + +(* ********************************************************************** *) +(* AC8 ==> AC9 *) +(* - this proof replaces the following two from Rubin & Rubin: *) +(* AC8 ==> AC1 and AC1 ==> AC9 *) +(* ********************************************************************** *) + +lemma AC8_AC9_lemma: + "\B1 \ A. \B2 \ A. B1 \ B2 + ==> \B \ A*A. \B1 B2. B= & B1 \ B2" +by fast + +lemma AC8_AC9: "AC8 ==> AC9" +apply (unfold AC8_def AC9_def) +apply (intro allI impI) +apply (erule allE) +apply (erule impE, erule AC8_AC9_lemma, force) +done + + +(* ********************************************************************** *) +(* 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. *) +(* ********************************************************************** *) + +lemma snd_lepoll_SigmaI: "b \ B \ X \ B \ X" +by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll + prod_commute_eqpoll) + +lemma nat_lepoll_lemma: + "[|0 \ A; B \ A|] ==> nat \ ((nat \ Union(A)) \ B) \ nat" +by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI) + +lemma AC9_AC1_lemma1: + "[| 0\A; A\0; + C = {((nat->Union(A))*B)*nat. B \ A} Un + {cons(0,((nat->Union(A))*B)*nat). B \ A}; + B1 \ C; B2 \ C |] + ==> B1 \ B2" +by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll + nat_cons_eqpoll [THEN eqpoll_trans] + prod_eqpoll_cong [OF _ eqpoll_refl] + intro: eqpoll_trans eqpoll_sym ) + +lemma AC9_AC1_lemma2: + "\B1 \ {(F*B)*N. B \ A} Un {cons(0,(F*B)*N). B \ A}. + \B2 \ {(F*B)*N. B \ A} Un {cons(0,(F*B)*N). B \ A}. + f` \ bij(B1, B2) + ==> (\B \ A. snd(fst((f`)`0))) \ (\X \ A. X)" +apply (intro lam_type snd_type fst_type) +apply (rule apply_type [OF _ consI1]) +apply (fast intro!: fun_weaken_type bij_is_fun) +done + +lemma AC9_AC1: "AC9 ==> AC1" +apply (unfold AC1_def AC9_def) +apply (intro allI impI) +apply (erule allE) +apply (case_tac "A~=0") +apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) +done + +end