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 |
(* - all_eqpoll_imp_pair_eqpoll *)
|
|
13 |
(* - Sigma_fun_space_eqpoll *)
|
1123
|
14 |
(* ********************************************************************** *)
|
|
15 |
|
2873
|
16 |
goal ZF.thy "!!A. [| C~:A; B:A |] ==> B~=C";
|
2469
|
17 |
by (Fast_tac 1);
|
1123
|
18 |
val mem_not_eq_not_mem = result();
|
|
19 |
|
|
20 |
goal thy "!!A. [| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
|
2469
|
21 |
by (fast_tac (!claset addSDs [Sigma_empty_iff RS iffD1]
|
1461
|
22 |
addDs [fun_space_emptyD, mem_not_eq_not_mem]
|
|
23 |
addEs [equals0D]
|
|
24 |
addSIs [equals0I,UnionI]) 1);
|
1123
|
25 |
val Sigma_fun_space_not0 = result();
|
|
26 |
|
|
27 |
goal thy "!!A C. (ALL B:A. B eqpoll C) ==> (ALL B1:A. ALL B2:A. B1 eqpoll B2)";
|
1207
|
28 |
by (REPEAT (rtac ballI 1));
|
1123
|
29 |
by (resolve_tac [bspec RS (bspec RSN (2, eqpoll_sym RSN (2, eqpoll_trans)))] 1
|
1461
|
30 |
THEN REPEAT (assume_tac 1));
|
1123
|
31 |
val all_eqpoll_imp_pair_eqpoll = result();
|
|
32 |
|
|
33 |
goal thy "!!A. [| ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)); b:A \
|
1461
|
34 |
\ |] ==> P(b)=R(b)";
|
1207
|
35 |
by (dtac bspec 1 THEN (assume_tac 1));
|
2469
|
36 |
by (Asm_full_simp_tac 1);
|
1123
|
37 |
val if_eqE1 = result();
|
|
38 |
|
|
39 |
goal thy "!!A. ALL a:A. if(a=b, P(a), Q(a)) = if(a=b, R(a), S(a)) \
|
1461
|
40 |
\ ==> ALL a:A. a~=b --> Q(a)=S(a)";
|
1207
|
41 |
by (rtac ballI 1);
|
|
42 |
by (rtac impI 1);
|
|
43 |
by (dtac bspec 1 THEN (assume_tac 1));
|
2469
|
44 |
by (Asm_full_simp_tac 1);
|
1123
|
45 |
val if_eqE2 = result();
|
|
46 |
|
|
47 |
goal thy "!!A. [| (lam x:A. f(x))=(lam x:A. g(x)); a:A |] ==> f(a)=g(a)";
|
2469
|
48 |
by (fast_tac (!claset addDs [subsetD]
|
1461
|
49 |
addSIs [lamI]
|
|
50 |
addEs [equalityE, lamE]) 1);
|
1123
|
51 |
val lam_eqE = result();
|
|
52 |
|
|
53 |
goalw thy [inj_def]
|
1461
|
54 |
"!!A. C:A ==> (lam g:(nat->Union(A))*C. \
|
|
55 |
\ (lam n:nat. if(n=0, snd(g), fst(g)`(n #- 1)))) \
|
|
56 |
\ : inj((nat->Union(A))*C, (nat->Union(A)) ) ";
|
1207
|
57 |
by (rtac CollectI 1);
|
2469
|
58 |
by (fast_tac (!claset addSIs [lam_type,RepFunI,if_type,snd_type,apply_type,
|
1461
|
59 |
fst_type,diff_type,nat_succI,nat_0I]) 1);
|
1123
|
60 |
by (REPEAT (resolve_tac [ballI, impI] 1));
|
2469
|
61 |
by (Asm_full_simp_tac 1);
|
1207
|
62 |
by (REPEAT (etac SigmaE 1));
|
1123
|
63 |
by (REPEAT (hyp_subst_tac 1));
|
2469
|
64 |
by (Asm_full_simp_tac 1);
|
1207
|
65 |
by (rtac conjI 1);
|
1123
|
66 |
by (dresolve_tac [nat_0I RSN (2, lam_eqE)] 2);
|
2469
|
67 |
by (Asm_full_simp_tac 2);
|
1207
|
68 |
by (rtac fun_extension 1 THEN REPEAT (assume_tac 1));
|
1196
|
69 |
by (dresolve_tac [nat_succI RSN (2, lam_eqE)] 1 THEN (assume_tac 1));
|
2469
|
70 |
by (asm_full_simp_tac (!simpset addsimps [succ_not_0 RS if_not_P]) 1);
|
1123
|
71 |
val lemma = result();
|
|
72 |
|
|
73 |
goal thy "!!A. [| C:A; 0~:A |] ==> (nat->Union(A)) * C eqpoll (nat->Union(A))";
|
1207
|
74 |
by (rtac eqpollI 1);
|
2469
|
75 |
by (fast_tac (!claset addSEs [prod_lepoll_self, not_sym RS not_emptyE,
|
1461
|
76 |
subst_elem] addEs [swap]) 2);
|
1207
|
77 |
by (rewtac lepoll_def);
|
2469
|
78 |
by (fast_tac (!claset addSIs [lemma]) 1);
|
1123
|
79 |
val Sigma_fun_space_eqpoll = result();
|
|
80 |
|
|
81 |
|
|
82 |
(* ********************************************************************** *)
|
1461
|
83 |
(* AC6 ==> AC7 *)
|
1123
|
84 |
(* ********************************************************************** *)
|
|
85 |
|
|
86 |
goalw thy AC_defs "!!Z. AC6 ==> AC7";
|
2469
|
87 |
by (Fast_tac 1);
|
1196
|
88 |
qed "AC6_AC7";
|
1123
|
89 |
|
|
90 |
(* ********************************************************************** *)
|
1461
|
91 |
(* AC7 ==> AC6, Rubin & Rubin p. 12, Theorem 2.8 *)
|
|
92 |
(* The case of the empty family of sets added in order to complete *)
|
|
93 |
(* the proof. *)
|
1123
|
94 |
(* ********************************************************************** *)
|
|
95 |
|
|
96 |
goal thy "!!y. y: (PROD B:A. Y*B) ==> (lam B:A. snd(y`B)): (PROD B:A. B)";
|
2469
|
97 |
by (fast_tac (!claset addSIs [lam_type, snd_type, apply_type]) 1);
|
1123
|
98 |
val lemma1_1 = result();
|
|
99 |
|
|
100 |
goal thy "!!A. y: (PROD B:{Y*C. C:A}. B) \
|
1461
|
101 |
\ ==> (lam B:A. y`(Y*B)): (PROD B:A. Y*B)";
|
2469
|
102 |
by (fast_tac (!claset addSIs [lam_type, apply_type]) 1);
|
1123
|
103 |
val lemma1_2 = result();
|
|
104 |
|
|
105 |
goal thy "!!A. (PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0 \
|
1461
|
106 |
\ ==> (PROD B:A. B) ~= 0";
|
2469
|
107 |
by (fast_tac (!claset addSIs [equals0I,lemma1_1, lemma1_2]
|
1461
|
108 |
addSEs [equals0D]) 1);
|
1123
|
109 |
val lemma1 = result();
|
|
110 |
|
|
111 |
goal thy "!!A. 0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
|
2469
|
112 |
by (fast_tac (!claset addEs [RepFunE,
|
1461
|
113 |
Sigma_fun_space_not0 RS not_sym RS notE]) 1);
|
1123
|
114 |
val lemma2 = result();
|
|
115 |
|
|
116 |
goalw thy AC_defs "!!Z. AC7 ==> AC6";
|
1207
|
117 |
by (rtac allI 1);
|
|
118 |
by (rtac impI 1);
|
1123
|
119 |
by (excluded_middle_tac "A=0" 1);
|
2469
|
120 |
by (fast_tac (!claset addSIs [not_emptyI, empty_fun]) 2);
|
1207
|
121 |
by (rtac lemma1 1);
|
|
122 |
by (etac allE 1);
|
|
123 |
by (etac impE 1 THEN (assume_tac 2));
|
2469
|
124 |
by (fast_tac (!claset addSEs [RepFunE]
|
1461
|
125 |
addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
|
|
126 |
Sigma_fun_space_eqpoll]) 1);
|
1196
|
127 |
qed "AC7_AC6";
|
1123
|
128 |
|
|
129 |
|
|
130 |
(* ********************************************************************** *)
|
1461
|
131 |
(* AC1 ==> AC8 *)
|
1123
|
132 |
(* ********************************************************************** *)
|
|
133 |
|
|
134 |
goalw thy [eqpoll_def]
|
1461
|
135 |
"!!A. ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2 \
|
|
136 |
\ ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
|
1207
|
137 |
by (rtac notI 1);
|
|
138 |
by (etac RepFunE 1);
|
|
139 |
by (dtac bspec 1 THEN (assume_tac 1));
|
1123
|
140 |
by (REPEAT (eresolve_tac [exE,conjE] 1));
|
|
141 |
by (hyp_subst_tac 1);
|
2469
|
142 |
by (Asm_full_simp_tac 1);
|
|
143 |
by (fast_tac (!claset addSEs [sym RS equals0D]) 1);
|
1123
|
144 |
val lemma1 = result();
|
|
145 |
|
|
146 |
goal thy "!!A. [| f: (PROD X:RepFun(A,p). X); D:A |] \
|
1461
|
147 |
\ ==> (lam x:A. f`p(x))`D : p(D)";
|
1196
|
148 |
by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
|
2469
|
149 |
by (fast_tac (!claset addSEs [apply_type]) 1);
|
1123
|
150 |
val lemma2 = result();
|
|
151 |
|
|
152 |
goalw thy AC_defs "!!Z. AC1 ==> AC8";
|
1207
|
153 |
by (rtac allI 1);
|
|
154 |
by (etac allE 1);
|
|
155 |
by (rtac impI 1);
|
|
156 |
by (etac impE 1);
|
|
157 |
by (etac lemma1 1);
|
2469
|
158 |
by (fast_tac (!claset addSEs [lemma2]) 1);
|
1196
|
159 |
qed "AC1_AC8";
|
1123
|
160 |
|
|
161 |
|
|
162 |
(* ********************************************************************** *)
|
1461
|
163 |
(* AC8 ==> AC9 *)
|
|
164 |
(* - this proof replaces the following two from Rubin & Rubin: *)
|
|
165 |
(* AC8 ==> AC1 and AC1 ==> AC9 *)
|
1123
|
166 |
(* ********************************************************************** *)
|
|
167 |
|
|
168 |
goal thy "!!A. ALL B1:A. ALL B2:A. B1 eqpoll B2 ==> \
|
1461
|
169 |
\ ALL B:A*A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2";
|
2469
|
170 |
by (Fast_tac 1);
|
1123
|
171 |
val lemma1 = result();
|
|
172 |
|
|
173 |
goal thy "!!f. f:bij(fst(<a,b>),snd(<a,b>)) ==> f:bij(a,b)";
|
2469
|
174 |
by (Asm_full_simp_tac 1);
|
1123
|
175 |
val lemma2 = result();
|
|
176 |
|
|
177 |
goalw thy AC_defs "!!Z. AC8 ==> AC9";
|
1207
|
178 |
by (rtac allI 1);
|
|
179 |
by (rtac impI 1);
|
|
180 |
by (etac allE 1);
|
|
181 |
by (etac impE 1);
|
|
182 |
by (etac lemma1 1);
|
2469
|
183 |
by (fast_tac (!claset addSEs [lemma2]) 1);
|
1196
|
184 |
qed "AC8_AC9";
|
1123
|
185 |
|
|
186 |
|
|
187 |
(* ********************************************************************** *)
|
1461
|
188 |
(* AC9 ==> AC1 *)
|
1123
|
189 |
(* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
|
1461
|
190 |
(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to *)
|
|
191 |
(* (x * y) Un {0} when y is a set of total functions acting from nat to *)
|
|
192 |
(* Union(A) -- therefore we have used the set (y * nat) instead of y. *)
|
1123
|
193 |
(* ********************************************************************** *)
|
|
194 |
|
|
195 |
(* Rules nedded to prove lemma1 *)
|
|
196 |
val snd_lepoll_SigmaI = prod_lepoll_self RS
|
|
197 |
((prod_commute_eqpoll RS eqpoll_imp_lepoll) RSN (2,lepoll_trans));
|
2469
|
198 |
|
1123
|
199 |
|
|
200 |
goal thy "!!A. [| 0~:A; A~=0 |] \
|
1461
|
201 |
\ ==> ALL B1: ({((nat->Union(A))*B)*nat. B:A} \
|
|
202 |
\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
|
|
203 |
\ ALL B2: ({((nat->Union(A))*B)*nat. B:A} \
|
|
204 |
\ Un {cons(0,((nat->Union(A))*B)*nat). B:A}). \
|
|
205 |
\ B1 eqpoll B2";
|
2469
|
206 |
by (fast_tac (!claset addSIs [all_eqpoll_imp_pair_eqpoll, ballI,
|
|
207 |
nat_cons_eqpoll RS eqpoll_trans]
|
|
208 |
addEs [Sigma_fun_space_not0 RS not_emptyE]
|
|
209 |
addIs [snd_lepoll_SigmaI, eqpoll_refl RSN
|
|
210 |
(2, prod_eqpoll_cong), Sigma_fun_space_eqpoll]) 1);
|
1123
|
211 |
val lemma1 = result();
|
|
212 |
|
|
213 |
goal thy "!!A. ALL B1:{(F*B)*N. B:A} Un {cons(0,(F*B)*N). B:A}. \
|
1461
|
214 |
\ ALL B2:{(F*B)*N. B:A} \
|
|
215 |
\ Un {cons(0,(F*B)*N). B:A}. f`<B1,B2> : bij(B1, B2) \
|
|
216 |
\ ==> (lam B:A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) : \
|
|
217 |
\ (PROD X:A. X)";
|
1207
|
218 |
by (rtac lam_type 1);
|
|
219 |
by (rtac snd_type 1);
|
|
220 |
by (rtac fst_type 1);
|
1123
|
221 |
by (resolve_tac [consI1 RSN (2, apply_type)] 1);
|
2469
|
222 |
by (fast_tac (!claset addSIs [fun_weaken_type, bij_is_fun]) 1);
|
1123
|
223 |
val lemma2 = result();
|
|
224 |
|
1196
|
225 |
goalw thy AC_defs "!!Z. AC9 ==> AC1";
|
1207
|
226 |
by (rtac allI 1);
|
|
227 |
by (rtac impI 1);
|
|
228 |
by (etac allE 1);
|
1123
|
229 |
by (excluded_middle_tac "A=0" 1);
|
1207
|
230 |
by (etac impE 1);
|
|
231 |
by (rtac lemma1 1 THEN (REPEAT (assume_tac 1)));
|
2469
|
232 |
by (fast_tac (!claset addSEs [lemma2]) 1);
|
|
233 |
by (fast_tac (!claset addSIs [empty_fun]) 1);
|
1196
|
234 |
qed "AC9_AC1";
|