author | paulson |
Tue, 08 Jan 2002 16:09:09 +0100 | |
changeset 12667 | 7e6eaaa125f2 |
parent 11317 | 7f9e4c389318 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC7-AC9.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous |
|
6 |
instances of AC. |
|
7 |
*) |
|
8 |
||
9 |
(* ********************************************************************** *) |
|
1461 | 10 |
(* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1 *) |
11 |
(* - Sigma_fun_space_not0 *) |
|
12 |
(* - Sigma_fun_space_eqpoll *) |
|
1123 | 13 |
(* ********************************************************************** *) |
14 |
||
11317 | 15 |
Goal "[| 0\\<notin>A; B \\<in> A |] ==> (nat->Union(A)) * B \\<noteq> 0"; |
5325
f7a5e06adea1
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
paulson
parents:
5265
diff
changeset
|
16 |
by (blast_tac (claset() addSDs [Sigma_empty_iff RS iffD1, |
9683 | 17 |
Union_empty_iff RS iffD1]) 1); |
3731 | 18 |
qed "Sigma_fun_space_not0"; |
1123 | 19 |
|
5068 | 20 |
Goalw [inj_def] |
11317 | 21 |
"C \\<in> A ==> (\\<lambda>g \\<in> (nat->Union(A))*C. \ |
22 |
\ (\\<lambda>n \\<in> nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \ |
|
23 |
\ \\<in> inj((nat->Union(A))*C, (nat->Union(A)) ) "; |
|
1207 | 24 |
by (rtac CollectI 1); |
4091 | 25 |
by (fast_tac (claset() addSIs [lam_type,RepFunI,if_type,snd_type,apply_type, |
1461 | 26 |
fst_type,diff_type,nat_succI,nat_0I]) 1); |
1123 | 27 |
by (REPEAT (resolve_tac [ballI, impI] 1)); |
2469 | 28 |
by (Asm_full_simp_tac 1); |
1207 | 29 |
by (REPEAT (etac SigmaE 1)); |
1123 | 30 |
by (REPEAT (hyp_subst_tac 1)); |
2469 | 31 |
by (Asm_full_simp_tac 1); |
1207 | 32 |
by (rtac conjI 1); |
1123 | 33 |
by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2); |
2469 | 34 |
by (Asm_full_simp_tac 2); |
1207 | 35 |
by (rtac fun_extension 1 THEN REPEAT (assume_tac 1)); |
1196 | 36 |
by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1)); |
4091 | 37 |
by (asm_full_simp_tac (simpset() addsimps [succ_not_0 RS if_not_P]) 1); |
1123 | 38 |
val lemma = result(); |
39 |
||
11317 | 40 |
Goal "[| C \\<in> A; 0\\<notin>A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))"; |
1207 | 41 |
by (rtac eqpollI 1); |
4091 | 42 |
by (fast_tac (claset() addSEs [prod_lepoll_self, not_sym RS not_emptyE, |
1461 | 43 |
subst_elem] addEs [swap]) 2); |
1207 | 44 |
by (rewtac lepoll_def); |
4091 | 45 |
by (fast_tac (claset() addSIs [lemma]) 1); |
3731 | 46 |
qed "Sigma_fun_space_eqpoll"; |
1123 | 47 |
|
48 |
||
49 |
(* ********************************************************************** *) |
|
1461 | 50 |
(* AC6 ==> AC7 *) |
1123 | 51 |
(* ********************************************************************** *) |
52 |
||
5137 | 53 |
Goalw AC_defs "AC6 ==> AC7"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
54 |
by (Blast_tac 1); |
1196 | 55 |
qed "AC6_AC7"; |
1123 | 56 |
|
57 |
(* ********************************************************************** *) |
|
1461 | 58 |
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *) |
59 |
(* The case of the empty family of sets added in order to complete *) |
|
60 |
(* the proof. *) |
|
1123 | 61 |
(* ********************************************************************** *) |
62 |
||
11317 | 63 |
Goal "y \\<in> (\\<Pi>B \\<in> A. Y*B) ==> (\\<lambda>B \\<in> A. snd(y`B)): (\\<Pi>B \\<in> A. B)"; |
4091 | 64 |
by (fast_tac (claset() addSIs [lam_type, snd_type, apply_type]) 1); |
1123 | 65 |
val lemma1_1 = result(); |
66 |
||
11317 | 67 |
Goal "y \\<in> (\\<Pi>B \\<in> {Y*C. C \\<in> A}. B) ==> (\\<lambda>B \\<in> A. y`(Y*B)): (\\<Pi>B \\<in> A. Y*B)"; |
4091 | 68 |
by (fast_tac (claset() addSIs [lam_type, apply_type]) 1); |
1123 | 69 |
val lemma1_2 = result(); |
70 |
||
11317 | 71 |
Goal "(\\<Pi>B \\<in> {(nat->Union(A))*C. C \\<in> A}. B) \\<noteq> 0 ==> (\\<Pi>B \\<in> A. B) \\<noteq> 0"; |
5470 | 72 |
by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1); |
1123 | 73 |
val lemma1 = result(); |
74 |
||
11317 | 75 |
Goal "0 \\<notin> A ==> 0 \\<notin> {(nat -> Union(A)) * C. C \\<in> A}"; |
5241 | 76 |
by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1); |
1123 | 77 |
val lemma2 = result(); |
78 |
||
5137 | 79 |
Goalw AC_defs "AC7 ==> AC6"; |
1207 | 80 |
by (rtac allI 1); |
81 |
by (rtac impI 1); |
|
9683 | 82 |
by (case_tac "A=0" 1); |
83 |
by (Asm_simp_tac 1); |
|
1207 | 84 |
by (rtac lemma1 1); |
85 |
by (etac allE 1); |
|
86 |
by (etac impE 1 THEN (assume_tac 2)); |
|
9683 | 87 |
by (blast_tac (claset() addSIs [lemma2] |
88 |
addIs [eqpoll_sym, eqpoll_trans, Sigma_fun_space_eqpoll]) 1); |
|
1196 | 89 |
qed "AC7_AC6"; |
1123 | 90 |
|
91 |
||
92 |
(* ********************************************************************** *) |
|
1461 | 93 |
(* AC1 ==> AC8 *) |
1123 | 94 |
(* ********************************************************************** *) |
95 |
||
5068 | 96 |
Goalw [eqpoll_def] |
11317 | 97 |
"\\<forall>B \\<in> A. \\<exists>B1 B2. B=<B1,B2> & B1 eqpoll B2 \ |
98 |
\ ==> 0 \\<notin> { bij(fst(B),snd(B)). B \\<in> A }"; |
|
5241 | 99 |
by Auto_tac; |
1123 | 100 |
val lemma1 = result(); |
101 |
||
11317 | 102 |
Goal "[| f \\<in> (\\<Pi>X \\<in> RepFun(A,p). X); D \\<in> A |] ==> (\\<lambda>x \\<in> A. f`p(x))`D \\<in> p(D)"; |
1196 | 103 |
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1)); |
4091 | 104 |
by (fast_tac (claset() addSEs [apply_type]) 1); |
1123 | 105 |
val lemma2 = result(); |
106 |
||
5137 | 107 |
Goalw AC_defs "AC1 ==> AC8"; |
5241 | 108 |
by (Clarify_tac 1); |
109 |
by (dtac lemma1 1); |
|
4091 | 110 |
by (fast_tac (claset() addSEs [lemma2]) 1); |
1196 | 111 |
qed "AC1_AC8"; |
1123 | 112 |
|
113 |
||
114 |
(* ********************************************************************** *) |
|
1461 | 115 |
(* AC8 ==> AC9 *) |
116 |
(* - this proof replaces the following two from Rubin & Rubin: *) |
|
117 |
(* AC8 ==> AC1 and AC1 ==> AC9 *) |
|
1123 | 118 |
(* ********************************************************************** *) |
119 |
||
11317 | 120 |
Goal "\\<forall>B1 \\<in> A. \\<forall>B2 \\<in> A. B1 eqpoll B2 \ |
121 |
\ ==> \\<forall>B \\<in> A*A. \\<exists>B1 B2. B=<B1,B2> & B1 eqpoll B2"; |
|
2469 | 122 |
by (Fast_tac 1); |
1123 | 123 |
val lemma1 = result(); |
124 |
||
11317 | 125 |
Goal "f \\<in> bij(fst(<a,b>),snd(<a,b>)) ==> f \\<in> bij(a,b)"; |
2469 | 126 |
by (Asm_full_simp_tac 1); |
1123 | 127 |
val lemma2 = result(); |
128 |
||
5137 | 129 |
Goalw AC_defs "AC8 ==> AC9"; |
1207 | 130 |
by (rtac allI 1); |
131 |
by (rtac impI 1); |
|
132 |
by (etac allE 1); |
|
133 |
by (etac impE 1); |
|
134 |
by (etac lemma1 1); |
|
4091 | 135 |
by (fast_tac (claset() addSEs [lemma2]) 1); |
1196 | 136 |
qed "AC8_AC9"; |
1123 | 137 |
|
138 |
||
139 |
(* ********************************************************************** *) |
|
1461 | 140 |
(* AC9 ==> AC1 *) |
1123 | 141 |
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *) |
1461 | 142 |
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *) |
143 |
(* (x * y) Un {0} when y is a set of total functions acting from nat to *) |
|
144 |
(* Union(A) -- therefore we have used the set (y * nat) instead of y. *) |
|
1123 | 145 |
(* ********************************************************************** *) |
146 |
||
147 |
(* Rules nedded to prove lemma1 *) |
|
148 |
val snd_lepoll_SigmaI = prod_lepoll_self RS |
|
149 |
((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans)); |
|
2469 | 150 |
|
1123 | 151 |
|
11151 | 152 |
Goal "[|0 \\<notin> A; B \\<in> A|] ==> nat \\<lesssim> ((nat \\<rightarrow> Union(A)) \\<times> B) \\<times> nat"; |
153 |
by (blast_tac (claset() addDs [Sigma_fun_space_not0] |
|
154 |
addIs [snd_lepoll_SigmaI]) 1); |
|
155 |
qed "nat_lepoll_lemma"; |
|
156 |
||
157 |
||
11317 | 158 |
Goal "[| 0\\<notin>A; A\\<noteq>0; \ |
159 |
\ C = {((nat->Union(A))*B)*nat. B \\<in> A} Un \ |
|
160 |
\ {cons(0,((nat->Union(A))*B)*nat). B \\<in> A}; \ |
|
9683 | 161 |
\ B1: C; B2: C |] \ |
162 |
\ ==> B1 eqpoll B2"; |
|
11151 | 163 |
by (blast_tac |
12667 | 164 |
(claset() delrules [eqpoll_refl] |
165 |
addSIs [nat_lepoll_lemma, nat_cons_eqpoll RS eqpoll_trans, |
|
11151 | 166 |
eqpoll_refl RSN (2, prod_eqpoll_cong)] |
167 |
addIs [eqpoll_trans, eqpoll_sym, Sigma_fun_space_eqpoll]) 1); |
|
1123 | 168 |
val lemma1 = result(); |
169 |
||
11317 | 170 |
Goal "\\<forall>B1 \\<in> {(F*B)*N. B \\<in> A} Un {cons(0,(F*B)*N). B \\<in> A}. \ |
171 |
\ \\<forall>B2 \\<in> {(F*B)*N. B \\<in> A} Un {cons(0,(F*B)*N). B \\<in> A}. \ |
|
172 |
\ f`<B1,B2> \\<in> bij(B1, B2) \ |
|
173 |
\ ==> (\\<lambda>B \\<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \\<in> (\\<Pi>X \\<in> A. X)"; |
|
1207 | 174 |
by (rtac lam_type 1); |
175 |
by (rtac snd_type 1); |
|
176 |
by (rtac fst_type 1); |
|
1123 | 177 |
by (resolve_tac [consI1 RSN (2, apply_type)] 1); |
4091 | 178 |
by (fast_tac (claset() addSIs [fun_weaken_type, bij_is_fun]) 1); |
1123 | 179 |
val lemma2 = result(); |
180 |
||
5137 | 181 |
Goalw AC_defs "AC9 ==> AC1"; |
1207 | 182 |
by (rtac allI 1); |
183 |
by (rtac impI 1); |
|
184 |
by (etac allE 1); |
|
9683 | 185 |
by (case_tac "A=0" 1); |
186 |
by (blast_tac (claset() addDs [lemma1,lemma2]) 2); |
|
187 |
by Auto_tac; |
|
1196 | 188 |
qed "AC9_AC1"; |