1478
|
1 |
(* Title: ZF/AC/DC.thy
|
1196
|
2 |
ID: $Id$
|
1478
|
3 |
Author: Krzysztof Grabczewski
|
1196
|
4 |
|
12776
|
5 |
The proofs concerning the Axiom of Dependent Choice
|
1196
|
6 |
*)
|
|
7 |
|
12776
|
8 |
theory DC = AC_Equiv + Hartog + Cardinal_aux:
|
|
9 |
|
|
10 |
lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
|
|
11 |
apply (unfold lepoll_def)
|
|
12 |
apply (rule_tac x = "\<lambda>z \<in> RepFun (a,P) . LEAST i. z=P (i) " in exI)
|
|
13 |
apply (rule_tac d="%z. P (z)" in lam_injective)
|
|
14 |
apply (fast intro!: Least_in_Ord)
|
|
15 |
apply (rule sym)
|
|
16 |
apply (fast intro: LeastI Ord_in_Ord)
|
|
17 |
done
|
1196
|
18 |
|
12776
|
19 |
text{*Trivial in the presence of AC, but here we need a wellordering of X*}
|
|
20 |
lemma image_Ord_lepoll: "[| f \<in> X->Y; Ord(X) |] ==> f``X \<lesssim> X"
|
|
21 |
apply (unfold lepoll_def)
|
|
22 |
apply (rule_tac x = "\<lambda>x \<in> f``X. LEAST y. f`y = x" in exI)
|
|
23 |
apply (rule_tac d = "%z. f`z" in lam_injective)
|
|
24 |
apply (fast intro!: Least_in_Ord apply_equality, clarify)
|
|
25 |
apply (rule LeastI)
|
|
26 |
apply (erule apply_equality, assumption+)
|
|
27 |
apply (blast intro: Ord_in_Ord)
|
|
28 |
done
|
1196
|
29 |
|
12776
|
30 |
lemma range_subset_domain:
|
|
31 |
"[| R \<subseteq> X*X; !!g. g \<in> X ==> \<exists>u. <g,u> \<in> R |]
|
|
32 |
==> range(R) \<subseteq> domain(R)"
|
|
33 |
by (blast );
|
|
34 |
|
|
35 |
lemma cons_fun_type: "g \<in> n->X ==> cons(<n,x>, g) \<in> succ(n) -> cons(x, X)"
|
|
36 |
apply (unfold succ_def)
|
|
37 |
apply (fast intro!: fun_extend elim!: mem_irrefl)
|
|
38 |
done
|
1196
|
39 |
|
12776
|
40 |
lemma cons_fun_type2:
|
|
41 |
"[| g \<in> n->X; x \<in> X |] ==> cons(<n,x>, g) \<in> succ(n) -> X"
|
|
42 |
by (erule cons_absorb [THEN subst], erule cons_fun_type)
|
|
43 |
|
|
44 |
lemma cons_image_n: "n \<in> nat ==> cons(<n,x>, g)``n = g``n"
|
|
45 |
by (fast elim!: mem_irrefl)
|
|
46 |
|
|
47 |
lemma cons_val_n: "g \<in> n->X ==> cons(<n,x>, g)`n = x"
|
|
48 |
by (fast intro!: apply_equality elim!: cons_fun_type)
|
|
49 |
|
|
50 |
lemma cons_image_k: "k \<in> n ==> cons(<n,x>, g)``k = g``k"
|
|
51 |
by (fast elim: mem_asym)
|
1196
|
52 |
|
12776
|
53 |
lemma cons_val_k: "[| k \<in> n; g \<in> n->X |] ==> cons(<n,x>, g)`k = g`k"
|
|
54 |
by (fast intro!: apply_equality consI2 elim!: cons_fun_type apply_Pair)
|
|
55 |
|
|
56 |
lemma domain_cons_eq_succ: "domain(f)=x ==> domain(cons(<x,y>, f)) = succ(x)"
|
|
57 |
by (simp add: domain_cons succ_def)
|
|
58 |
|
|
59 |
lemma restrict_cons_eq: "g \<in> n->X ==> restrict(cons(<n,x>, g), n) = g"
|
12891
|
60 |
apply (simp add: restrict_def Pi_iff)
|
|
61 |
apply (blast intro: elim: mem_irrefl)
|
12776
|
62 |
done
|
|
63 |
|
|
64 |
lemma succ_in_succ: "[| Ord(k); i \<in> k |] ==> succ(i) \<in> succ(k)"
|
|
65 |
apply (rule Ord_linear [of "succ(i)" "succ(k)", THEN disjE])
|
|
66 |
apply (fast elim: Ord_in_Ord mem_irrefl mem_asym)+
|
|
67 |
done
|
1196
|
68 |
|
12776
|
69 |
lemma restrict_eq_imp_val_eq:
|
12891
|
70 |
"[|restrict(f, domain(g)) = g; x \<in> domain(g)|]
|
|
71 |
==> f`x = g`x"
|
|
72 |
by (erule subst, simp add: restrict)
|
12776
|
73 |
|
|
74 |
lemma domain_eq_imp_fun_type: "[| domain(f)=A; f \<in> B->C |] ==> f \<in> A->C"
|
|
75 |
by (frule domain_of_fun, fast)
|
|
76 |
|
|
77 |
lemma ex_in_domain: "[| R \<subseteq> A * B; R \<noteq> 0 |] ==> \<exists>x. x \<in> domain(R)"
|
|
78 |
by (fast elim!: not_emptyE)
|
|
79 |
|
5482
|
80 |
|
12776
|
81 |
constdefs
|
|
82 |
|
|
83 |
DC :: "i => o"
|
|
84 |
"DC(a) == \<forall>X R. R \<subseteq> Pow(X)*X &
|
|
85 |
(\<forall>Y \<in> Pow(X). Y \<prec> a --> (\<exists>x \<in> X. <Y,x> \<in> R))
|
|
86 |
--> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
|
|
87 |
|
|
88 |
DC0 :: o
|
|
89 |
"DC0 == \<forall>A B R. R \<subseteq> A*B & R\<noteq>0 & range(R) \<subseteq> domain(R)
|
|
90 |
--> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
|
|
91 |
|
|
92 |
ff :: "[i, i, i, i] => i"
|
|
93 |
"ff(b, X, Q, R) ==
|
|
94 |
transrec(b, %c r. THE x. first(x, {x \<in> X. <r``c, x> \<in> R}, Q))"
|
|
95 |
|
5482
|
96 |
|
|
97 |
locale DC0_imp =
|
12776
|
98 |
fixes XX and RR and X and R
|
|
99 |
|
|
100 |
assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
|
|
101 |
|
|
102 |
defines XX_def: "XX == (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})"
|
|
103 |
and RR_def: "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))
|
|
104 |
& restrict(z2, domain(z1)) = z1}"
|
|
105 |
|
|
106 |
|
|
107 |
(* ********************************************************************** *)
|
|
108 |
(* DC ==> DC(omega) *)
|
|
109 |
(* *)
|
|
110 |
(* The scheme of the proof: *)
|
|
111 |
(* *)
|
|
112 |
(* Assume DC. Let R and X satisfy the premise of DC(omega). *)
|
|
113 |
(* *)
|
|
114 |
(* Define XX and RR as follows: *)
|
|
115 |
(* *)
|
|
116 |
(* XX = (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R}) *)
|
|
117 |
(* f RR g iff domain(g)=succ(domain(f)) & *)
|
|
118 |
(* restrict(g, domain(f)) = f *)
|
|
119 |
(* *)
|
|
120 |
(* Then RR satisfies the hypotheses of DC. *)
|
|
121 |
(* So applying DC: *)
|
|
122 |
(* *)
|
|
123 |
(* \<exists>f \<in> nat->XX. \<forall>n \<in> nat. f`n RR f`succ(n) *)
|
|
124 |
(* *)
|
|
125 |
(* Thence *)
|
|
126 |
(* *)
|
|
127 |
(* ff = {<n, f`succ(n)`n>. n \<in> nat} *)
|
|
128 |
(* *)
|
|
129 |
(* is the desired function. *)
|
|
130 |
(* *)
|
|
131 |
(* ********************************************************************** *)
|
|
132 |
|
|
133 |
lemma (in DC0_imp) lemma1_1: "RR \<subseteq> XX*XX"
|
|
134 |
by (unfold RR_def, fast)
|
|
135 |
|
|
136 |
lemma (in DC0_imp) lemma1_2: "RR \<noteq> 0"
|
|
137 |
apply (unfold RR_def XX_def)
|
|
138 |
apply (rule all_ex [THEN ballE])
|
|
139 |
apply (erule_tac [2] notE [OF _ empty_subsetI [THEN PowI]])
|
|
140 |
apply (erule_tac impE [OF _ nat_0I [THEN n_lesspoll_nat]])
|
|
141 |
apply (erule bexE)
|
|
142 |
apply (rule_tac a = "<0, {<0, x>}>" in not_emptyI)
|
|
143 |
apply (rule CollectI)
|
|
144 |
apply (rule SigmaI)
|
|
145 |
apply (rule nat_0I [THEN UN_I])
|
|
146 |
apply (simp (no_asm_simp) add: nat_0I [THEN UN_I])
|
|
147 |
apply (rule nat_1I [THEN UN_I])
|
|
148 |
apply (force intro!: singleton_fun [THEN Pi_type]
|
|
149 |
simp add: singleton_0 [symmetric])
|
|
150 |
apply (simp add: singleton_0)
|
|
151 |
done
|
|
152 |
|
|
153 |
lemma (in DC0_imp) lemma1_3: "range(RR) \<subseteq> domain(RR)"
|
|
154 |
apply (unfold RR_def XX_def)
|
|
155 |
apply (rule range_subset_domain, blast, clarify)
|
|
156 |
apply (frule fun_is_rel [THEN image_subset, THEN PowI,
|
|
157 |
THEN all_ex [THEN bspec]])
|
|
158 |
apply (erule impE[OF _ lesspoll_trans1[OF image_Ord_lepoll
|
|
159 |
[OF _ nat_into_Ord] n_lesspoll_nat]],
|
|
160 |
assumption+)
|
|
161 |
apply (erule bexE)
|
|
162 |
apply (rule_tac x = "cons (<n,x>, g) " in exI)
|
|
163 |
apply (rule CollectI)
|
|
164 |
apply (force elim!: cons_fun_type2
|
|
165 |
simp add: cons_image_n cons_val_n cons_image_k cons_val_k)
|
|
166 |
apply (simp add: domain_of_fun succ_def restrict_cons_eq)
|
|
167 |
done
|
5482
|
168 |
|
12776
|
169 |
lemma (in DC0_imp) lemma2:
|
|
170 |
"[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; n \<in> nat |]
|
|
171 |
==> \<exists>k \<in> nat. f`succ(n) \<in> k -> X & n \<in> k
|
|
172 |
& <f`succ(n)``n, f`succ(n)`n> \<in> R"
|
|
173 |
apply (induct_tac "n")
|
|
174 |
apply (drule apply_type [OF _ nat_1I])
|
|
175 |
apply (drule bspec [OF _ nat_0I])
|
|
176 |
apply (simp add: XX_def, safe)
|
|
177 |
apply (rule rev_bexI, assumption)
|
|
178 |
apply (subgoal_tac "0 \<in> x", force)
|
|
179 |
apply (force simp add: RR_def
|
|
180 |
intro: ltD elim!: nat_0_le [THEN leE])
|
|
181 |
(** LEVEL 7, other subgoal **)
|
|
182 |
apply (drule bspec [OF _ nat_succI], assumption)
|
|
183 |
apply (subgoal_tac "f ` succ (succ (x)) \<in> succ (k) ->X")
|
|
184 |
apply (drule apply_type [OF _ nat_succI [THEN nat_succI]], assumption)
|
|
185 |
apply (simp (no_asm_use) add: XX_def RR_def)
|
|
186 |
apply safe
|
|
187 |
apply (frule_tac a="succ(k)" in domain_of_fun [symmetric, THEN trans],
|
|
188 |
assumption)
|
|
189 |
apply (frule_tac a="xa" in domain_of_fun [symmetric, THEN trans],
|
|
190 |
assumption)
|
|
191 |
apply (fast elim!: nat_into_Ord [THEN succ_in_succ]
|
|
192 |
dest!: bspec [OF _ nat_into_Ord [THEN succ_in_succ]])
|
|
193 |
apply (drule domain_of_fun)
|
|
194 |
apply (simp add: XX_def RR_def, clarify)
|
|
195 |
apply (blast dest: domain_of_fun [symmetric, THEN trans] )
|
|
196 |
done
|
|
197 |
|
|
198 |
lemma (in DC0_imp) lemma3_1:
|
|
199 |
"[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; m \<in> nat |]
|
|
200 |
==> {f`succ(x)`x. x \<in> m} = {f`succ(m)`x. x \<in> m}"
|
|
201 |
apply (subgoal_tac "\<forall>x \<in> m. f`succ (m) `x = f`succ (x) `x")
|
|
202 |
apply simp
|
|
203 |
apply (induct_tac "m", blast)
|
|
204 |
apply (rule ballI)
|
|
205 |
apply (erule succE)
|
|
206 |
apply (rule restrict_eq_imp_val_eq)
|
|
207 |
apply (drule bspec [OF _ nat_succI], assumption)
|
|
208 |
apply (simp add: RR_def)
|
|
209 |
apply (drule lemma2, assumption+)
|
|
210 |
apply (fast dest!: domain_of_fun)
|
|
211 |
apply (drule_tac x = "xa" in bspec, assumption)
|
|
212 |
apply (erule sym [THEN trans, symmetric])
|
|
213 |
apply (rule restrict_eq_imp_val_eq [symmetric])
|
|
214 |
apply (drule bspec [OF _ nat_succI], assumption)
|
|
215 |
apply (simp add: RR_def)
|
|
216 |
apply (drule lemma2, assumption+)
|
|
217 |
apply (blast dest!: domain_of_fun
|
12891
|
218 |
intro: nat_into_Ord OrdmemD [THEN subsetD])
|
12776
|
219 |
done
|
5482
|
220 |
|
12776
|
221 |
lemma (in DC0_imp) lemma3:
|
|
222 |
"[| \<forall>n \<in> nat. <f`n, f`succ(n)> \<in> RR; f \<in> nat -> XX; m \<in> nat |]
|
|
223 |
==> (\<lambda>x \<in> nat. f`succ(x)`x) `` m = f`succ(m)``m"
|
|
224 |
apply (erule natE, simp)
|
|
225 |
apply (subst image_lam)
|
|
226 |
apply (fast elim!: OrdmemD [OF nat_succI Ord_nat])
|
|
227 |
apply (subst lemma3_1, assumption+)
|
|
228 |
apply fast
|
|
229 |
apply (fast dest!: lemma2
|
|
230 |
elim!: image_fun [symmetric, OF _ OrdmemD [OF _ nat_into_Ord]])
|
|
231 |
done
|
|
232 |
|
|
233 |
|
|
234 |
theorem DC0_imp_DC_nat: "DC0 ==> DC(nat)"
|
|
235 |
apply (unfold DC_def DC0_def, clarify)
|
|
236 |
apply (elim allE)
|
|
237 |
apply (erule impE)
|
|
238 |
(*these three results comprise Lemma 1*)
|
|
239 |
apply (blast intro!: DC0_imp.lemma1_1 DC0_imp.lemma1_2 DC0_imp.lemma1_3)
|
|
240 |
apply (erule bexE)
|
|
241 |
apply (rule_tac x = "\<lambda>n \<in> nat. f`succ (n) `n" in rev_bexI)
|
|
242 |
apply (rule lam_type, blast dest!: DC0_imp.lemma2 intro: fun_weaken_type)
|
|
243 |
apply (rule oallI)
|
|
244 |
apply (frule DC0_imp.lemma2, assumption)
|
|
245 |
apply (blast intro: fun_weaken_type)
|
|
246 |
apply (erule ltD)
|
|
247 |
(** LEVEL 11: last subgoal **)
|
|
248 |
apply (subst DC0_imp.lemma3, assumption+)
|
|
249 |
apply (fast elim!: fun_weaken_type)
|
|
250 |
apply (erule ltD, force)
|
|
251 |
done
|
|
252 |
|
|
253 |
|
|
254 |
(* ************************************************************************
|
|
255 |
DC(omega) ==> DC
|
|
256 |
|
|
257 |
The scheme of the proof:
|
|
258 |
|
|
259 |
Assume DC(omega). Let R and x satisfy the premise of DC.
|
|
260 |
|
|
261 |
Define XX and RR as follows:
|
|
262 |
|
|
263 |
XX = (\<Union>n \<in> nat. {f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})
|
|
264 |
|
|
265 |
RR = {<z1,z2>:Fin(XX)*XX.
|
|
266 |
(domain(z2)=succ(\<Union>f \<in> z1. domain(f)) &
|
|
267 |
(\<forall>f \<in> z1. restrict(z2, domain(f)) = f)) |
|
|
268 |
(~ (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f)) &
|
|
269 |
(\<forall>f \<in> z1. restrict(g, domain(f)) = f)) &
|
|
270 |
z2={<0,x>})}
|
|
271 |
|
|
272 |
Then XX and RR satisfy the hypotheses of DC(omega).
|
|
273 |
So applying DC:
|
|
274 |
|
|
275 |
\<exists>f \<in> nat->XX. \<forall>n \<in> nat. f``n RR f`n
|
|
276 |
|
|
277 |
Thence
|
|
278 |
|
|
279 |
ff = {<n, f`n`n>. n \<in> nat}
|
|
280 |
|
|
281 |
is the desired function.
|
|
282 |
|
|
283 |
************************************************************************* *)
|
|
284 |
|
|
285 |
lemma singleton_in_funs:
|
|
286 |
"x \<in> X ==> {<0,x>} \<in>
|
|
287 |
(\<Union>n \<in> nat. {f \<in> succ(n)->X. \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
|
|
288 |
apply (rule nat_0I [THEN UN_I])
|
|
289 |
apply (force simp add: singleton_0 [symmetric]
|
|
290 |
intro!: singleton_fun [THEN Pi_type])
|
|
291 |
done
|
5482
|
292 |
|
1196
|
293 |
|
5482
|
294 |
locale imp_DC0 =
|
12776
|
295 |
fixes XX and RR and x and R and f and allRR
|
|
296 |
defines XX_def: "XX == (\<Union>n \<in> nat.
|
|
297 |
{f \<in> succ(n)->domain(R). \<forall>k \<in> n. <f`k, f`succ(k)> \<in> R})"
|
|
298 |
and RR_def:
|
|
299 |
"RR == {<z1,z2>:Fin(XX)*XX.
|
|
300 |
(domain(z2)=succ(\<Union>f \<in> z1. domain(f))
|
|
301 |
& (\<forall>f \<in> z1. restrict(z2, domain(f)) = f))
|
|
302 |
| (~ (\<exists>g \<in> XX. domain(g)=succ(\<Union>f \<in> z1. domain(f))
|
|
303 |
& (\<forall>f \<in> z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
|
|
304 |
and allRR_def:
|
|
305 |
"allRR == \<forall>b<nat.
|
|
306 |
<f``b, f`b> \<in>
|
|
307 |
{<z1,z2>\<in>Fin(XX)*XX. (domain(z2)=succ(\<Union>f \<in> z1. domain(f))
|
|
308 |
& (\<Union>f \<in> z1. domain(f)) = b
|
|
309 |
& (\<forall>f \<in> z1. restrict(z2,domain(f)) = f))}"
|
|
310 |
|
|
311 |
lemma (in imp_DC0) lemma4:
|
|
312 |
"[| range(R) \<subseteq> domain(R); x \<in> domain(R) |]
|
|
313 |
==> RR \<subseteq> Pow(XX)*XX &
|
|
314 |
(\<forall>Y \<in> Pow(XX). Y \<prec> nat --> (\<exists>x \<in> XX. <Y,x>:RR))"
|
|
315 |
apply (rule conjI)
|
|
316 |
apply (force dest!: FinD [THEN PowI] simp add: RR_def)
|
|
317 |
apply (rule impI [THEN ballI])
|
|
318 |
apply (drule Finite_Fin [OF lesspoll_nat_is_Finite PowD], assumption)
|
|
319 |
apply (case_tac
|
|
320 |
"\<exists>g \<in> XX. domain (g) =
|
|
321 |
succ(\<Union>f \<in> Y. domain(f)) & (\<forall>f\<in>Y. restrict(g, domain(f)) = f)")
|
|
322 |
apply (simp add: RR_def, blast)
|
|
323 |
apply (safe del: domainE)
|
|
324 |
apply (unfold XX_def RR_def)
|
|
325 |
apply (rule rev_bexI, erule singleton_in_funs)
|
|
326 |
apply (simp add: nat_0I [THEN rev_bexI] cons_fun_type2)
|
|
327 |
done
|
|
328 |
|
|
329 |
lemma (in imp_DC0) UN_image_succ_eq:
|
|
330 |
"[| f \<in> nat->X; n \<in> nat |]
|
|
331 |
==> (\<Union>x \<in> f``succ(n). P(x)) = P(f`n) Un (\<Union>x \<in> f``n. P(x))"
|
|
332 |
by (simp add: image_fun OrdmemD)
|
|
333 |
|
|
334 |
lemma (in imp_DC0) UN_image_succ_eq_succ:
|
|
335 |
"[| (\<Union>x \<in> f``n. P(x)) = y; P(f`n) = succ(y);
|
|
336 |
f \<in> nat -> X; n \<in> nat |] ==> (\<Union>x \<in> f``succ(n). P(x)) = succ(y)"
|
|
337 |
by (simp add: UN_image_succ_eq, blast)
|
|
338 |
|
|
339 |
lemma (in imp_DC0) apply_domain_type:
|
|
340 |
"[| h \<in> succ(n) -> D; n \<in> nat; domain(h)=succ(y) |] ==> h`y \<in> D"
|
|
341 |
by (fast elim: apply_type dest!: trans [OF sym domain_of_fun])
|
|
342 |
|
|
343 |
lemma (in imp_DC0) image_fun_succ:
|
|
344 |
"[| h \<in> nat -> X; n \<in> nat |] ==> h``succ(n) = cons(h`n, h``n)"
|
|
345 |
by (simp add: image_fun OrdmemD)
|
|
346 |
|
|
347 |
lemma (in imp_DC0) f_n_type:
|
|
348 |
"[| domain(f`n) = succ(k); f \<in> nat -> XX; n \<in> nat |]
|
|
349 |
==> f`n \<in> succ(k) -> domain(R)"
|
|
350 |
apply (unfold XX_def)
|
|
351 |
apply (drule apply_type, assumption)
|
|
352 |
apply (fast elim: domain_eq_imp_fun_type)
|
|
353 |
done
|
|
354 |
|
|
355 |
lemma (in imp_DC0) f_n_pairs_in_R [rule_format]:
|
|
356 |
"[| h \<in> nat -> XX; domain(h`n) = succ(k); n \<in> nat |]
|
|
357 |
==> \<forall>i \<in> k. <h`n`i, h`n`succ(i)> \<in> R"
|
|
358 |
apply (unfold XX_def)
|
|
359 |
apply (drule apply_type, assumption)
|
|
360 |
apply (elim UN_E CollectE)
|
12820
|
361 |
apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
|
12776
|
362 |
done
|
|
363 |
|
|
364 |
lemma (in imp_DC0) restrict_cons_eq_restrict:
|
|
365 |
"[| restrict(h, domain(u))=u; h \<in> n->X; domain(u) \<subseteq> n |]
|
|
366 |
==> restrict(cons(<n, y>, h), domain(u)) = u"
|
|
367 |
apply (unfold restrict_def)
|
12891
|
368 |
apply (simp add: restrict_def Pi_iff)
|
12776
|
369 |
apply (erule sym [THEN trans, symmetric])
|
12891
|
370 |
apply (blast elim: mem_irrefl)
|
12776
|
371 |
done
|
|
372 |
|
|
373 |
lemma (in imp_DC0) all_in_image_restrict_eq:
|
|
374 |
"[| \<forall>x \<in> f``n. restrict(f`n, domain(x))=x;
|
|
375 |
f \<in> nat -> XX;
|
|
376 |
n \<in> nat; domain(f`n) = succ(n);
|
|
377 |
(\<Union>x \<in> f``n. domain(x)) \<subseteq> n |]
|
|
378 |
==> \<forall>x \<in> f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x"
|
|
379 |
apply (rule ballI)
|
|
380 |
apply (simp add: image_fun_succ)
|
|
381 |
apply (drule f_n_type, assumption+)
|
|
382 |
apply (erule disjE)
|
|
383 |
apply (simp add: domain_of_fun restrict_cons_eq)
|
|
384 |
apply (blast intro!: restrict_cons_eq_restrict)
|
|
385 |
done
|
|
386 |
|
|
387 |
lemma (in imp_DC0) simplify_recursion:
|
|
388 |
"[| \<forall>b<nat. <f``b, f`b> \<in> RR;
|
|
389 |
f \<in> nat -> XX; range(R) \<subseteq> domain(R); x \<in> domain(R)|]
|
|
390 |
==> allRR"
|
|
391 |
apply (unfold RR_def allRR_def)
|
|
392 |
apply (rule oallI, drule ltD)
|
|
393 |
apply (erule nat_induct)
|
|
394 |
apply (drule_tac x="0" in ospec, blast intro: Limit_has_0)
|
|
395 |
apply (force simp add: singleton_fun [THEN domain_of_fun] singleton_in_funs)
|
|
396 |
(*induction step*) (** LEVEL 5 **)
|
|
397 |
(*prevent simplification of ~\<exists> to \<forall>~ *)
|
|
398 |
apply (simp only: separation split)
|
12820
|
399 |
apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI)
|
12776
|
400 |
apply (elim conjE disjE)
|
|
401 |
apply (force elim!: trans subst_context
|
|
402 |
intro!: UN_image_succ_eq_succ)
|
|
403 |
apply (erule notE)
|
|
404 |
apply (simp add: XX_def UN_image_succ_eq_succ)
|
|
405 |
apply (elim conjE bexE)
|
|
406 |
apply (drule apply_domain_type, assumption+)
|
|
407 |
apply (erule domainE)+
|
|
408 |
apply (frule f_n_type)
|
|
409 |
apply (simp add: XX_def, assumption+)
|
|
410 |
apply (rule rev_bexI, erule nat_succI)
|
|
411 |
apply (rule_tac x = "cons (<succ (xa), ya>, f`xa) " in bexI)
|
|
412 |
prefer 2 apply (blast intro: cons_fun_type2)
|
|
413 |
apply (rule conjI)
|
|
414 |
prefer 2 apply (fast del: ballI subsetI
|
|
415 |
elim: trans [OF _ subst_context, THEN domain_cons_eq_succ]
|
|
416 |
subst_context
|
|
417 |
all_in_image_restrict_eq [simplified XX_def]
|
|
418 |
trans equalityD1)
|
|
419 |
(*one remaining subgoal*)
|
|
420 |
apply (rule ballI)
|
|
421 |
apply (erule succE)
|
|
422 |
(** LEVEL 25 **)
|
|
423 |
apply (simp add: cons_val_n cons_val_k)
|
|
424 |
(*assumption+ will not perform the required backtracking!*)
|
|
425 |
apply (drule f_n_pairs_in_R [simplified XX_def, OF _ domain_of_fun],
|
|
426 |
assumption, assumption, assumption)
|
|
427 |
apply (simp add: nat_into_Ord [THEN succ_in_succ] succI2 cons_val_k)
|
|
428 |
done
|
|
429 |
|
5482
|
430 |
|
12776
|
431 |
lemma (in imp_DC0) lemma2:
|
|
432 |
"[| allRR; f \<in> nat->XX; range(R) \<subseteq> domain(R); x \<in> domain(R); n \<in> nat |]
|
|
433 |
==> f`n \<in> succ(n) -> domain(R) & (\<forall>i \<in> n. <f`n`i, f`n`succ(i)>:R)"
|
|
434 |
apply (unfold allRR_def)
|
|
435 |
apply (drule ospec)
|
|
436 |
apply (erule ltI [OF _ Ord_nat])
|
|
437 |
apply (erule CollectE, simp)
|
|
438 |
apply (rule conjI)
|
|
439 |
prefer 2 apply (fast elim!: f_n_pairs_in_R trans subst_context)
|
|
440 |
apply (unfold XX_def)
|
|
441 |
apply (fast elim!: trans [THEN domain_eq_imp_fun_type] subst_context)
|
|
442 |
done
|
|
443 |
|
|
444 |
lemma (in imp_DC0) lemma3:
|
|
445 |
"[| allRR; f \<in> nat->XX; n\<in>nat; range(R) \<subseteq> domain(R); x \<in> domain(R) |]
|
|
446 |
==> f`n`n = f`succ(n)`n"
|
|
447 |
apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
|
|
448 |
apply (unfold allRR_def)
|
|
449 |
apply (drule ospec)
|
12820
|
450 |
apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
|
12776
|
451 |
apply (elim conjE ballE)
|
|
452 |
apply (erule restrict_eq_imp_val_eq [symmetric], force)
|
|
453 |
apply (simp add: image_fun OrdmemD)
|
|
454 |
done
|
|
455 |
|
|
456 |
|
|
457 |
theorem DC_nat_imp_DC0: "DC(nat) ==> DC0"
|
|
458 |
apply (unfold DC_def DC0_def)
|
|
459 |
apply (intro allI impI)
|
|
460 |
apply (erule asm_rl conjE ex_in_domain [THEN exE] allE)+
|
|
461 |
apply (erule impE [OF _ imp_DC0.lemma4], assumption+)
|
|
462 |
apply (erule bexE)
|
|
463 |
apply (drule imp_DC0.simplify_recursion, assumption+)
|
|
464 |
apply (rule_tac x = "\<lambda>n \<in> nat. f`n`n" in bexI)
|
|
465 |
apply (rule_tac [2] lam_type)
|
|
466 |
apply (erule_tac [2] apply_type [OF imp_DC0.lemma2 [THEN conjunct1] succI1])
|
|
467 |
apply (rule ballI)
|
|
468 |
apply (frule_tac n="succ(n)" in imp_DC0.lemma2,
|
|
469 |
(assumption|erule nat_succI)+)
|
|
470 |
apply (drule imp_DC0.lemma3, auto)
|
|
471 |
done
|
|
472 |
|
|
473 |
(* ********************************************************************** *)
|
|
474 |
(* \<forall>K. Card(K) --> DC(K) ==> WO3 *)
|
|
475 |
(* ********************************************************************** *)
|
|
476 |
|
|
477 |
lemma fun_Ord_inj:
|
|
478 |
"[| f \<in> a->X; Ord(a);
|
|
479 |
!!b c. [| b<c; c \<in> a |] ==> f`b\<noteq>f`c |]
|
|
480 |
==> f \<in> inj(a, X)"
|
|
481 |
apply (unfold inj_def, simp)
|
|
482 |
apply (intro ballI impI)
|
|
483 |
apply (rule_tac j=x in Ord_in_Ord [THEN Ord_linear_lt], assumption+)
|
|
484 |
apply (blast intro: Ord_in_Ord, auto)
|
|
485 |
apply (atomize, blast dest: not_sym)
|
|
486 |
done
|
|
487 |
|
|
488 |
lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
|
|
489 |
by (fast elim!: image_fun [THEN ssubst]);
|
|
490 |
|
|
491 |
theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
|
|
492 |
apply (unfold DC_def WO3_def)
|
|
493 |
apply (rule allI)
|
12820
|
494 |
apply (case_tac "A \<prec> Hartog (A)")
|
12776
|
495 |
apply (fast dest!: lesspoll_imp_ex_lt_eqpoll
|
|
496 |
intro!: Ord_Hartog leI [THEN le_imp_subset])
|
|
497 |
apply (erule allE impE)+
|
|
498 |
apply (rule Card_Hartog)
|
|
499 |
apply (erule_tac x = "A" in allE)
|
|
500 |
apply (erule_tac x = "{<z1,z2> \<in> Pow (A) *A . z1 \<prec> Hartog (A) & z2 \<notin> z1}"
|
|
501 |
in allE)
|
|
502 |
apply simp
|
|
503 |
apply (erule impE, fast elim: lesspoll_lemma [THEN not_emptyE])
|
|
504 |
apply (erule bexE)
|
|
505 |
apply (rule Hartog_lepoll_selfE)
|
|
506 |
apply (rule lepoll_def [THEN def_imp_iff, THEN iffD2])
|
|
507 |
apply (rule exI, rule fun_Ord_inj, assumption, rule Ord_Hartog)
|
|
508 |
apply (drule value_in_image)
|
|
509 |
apply (drule OrdmemD, rule Ord_Hartog, assumption+, erule ltD)
|
|
510 |
apply (drule ospec)
|
|
511 |
apply (blast intro: ltI Ord_Hartog, force)
|
|
512 |
done
|
|
513 |
|
|
514 |
(* ********************************************************************** *)
|
|
515 |
(* WO1 ==> \<forall>K. Card(K) --> DC(K) *)
|
|
516 |
(* ********************************************************************** *)
|
|
517 |
|
|
518 |
lemma images_eq:
|
|
519 |
"[| \<forall>x \<in> A. f`x=g`x; f \<in> Df->Cf; g \<in> Dg->Cg; A \<subseteq> Df; A \<subseteq> Dg |]
|
|
520 |
==> f``A = g``A"
|
|
521 |
apply (simp (no_asm_simp) add: image_fun)
|
|
522 |
done
|
|
523 |
|
|
524 |
lemma lam_images_eq:
|
|
525 |
"[| Ord(a); b \<in> a |] ==> (\<lambda>x \<in> a. h(x))``b = (\<lambda>x \<in> b. h(x))``b"
|
|
526 |
apply (rule images_eq)
|
|
527 |
apply (rule ballI)
|
|
528 |
apply (drule OrdmemD [THEN subsetD], assumption+)
|
|
529 |
apply simp
|
|
530 |
apply (fast elim!: RepFunI OrdmemD intro!: lam_type)+
|
|
531 |
done
|
|
532 |
|
|
533 |
lemma lam_type_RepFun: "(\<lambda>b \<in> a. h(b)) \<in> a -> {h(b). b \<in> a}"
|
|
534 |
by (fast intro!: lam_type RepFunI)
|
|
535 |
|
|
536 |
lemma lemmaX:
|
|
537 |
"[| \<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R);
|
|
538 |
b \<in> K; Z \<in> Pow(X); Z \<prec> K |]
|
|
539 |
==> {x \<in> X. <Z,x> \<in> R} \<noteq> 0"
|
|
540 |
by blast
|
|
541 |
|
|
542 |
|
|
543 |
lemma WO1_DC_lemma:
|
|
544 |
"[| Card(K); well_ord(X,Q);
|
|
545 |
\<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |]
|
|
546 |
==> ff(b, X, Q, R) \<in> {x \<in> X. <(\<lambda>c \<in> b. ff(c, X, Q, R))``b, x> \<in> R}"
|
|
547 |
apply (rule_tac P = "b \<in> K" in impE, (erule_tac [2] asm_rl)+)
|
|
548 |
apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct],
|
|
549 |
assumption+)
|
|
550 |
apply (rule impI)
|
|
551 |
apply (rule ff_def [THEN def_transrec, THEN ssubst])
|
|
552 |
apply (erule the_first_in, fast)
|
|
553 |
apply (simp add: image_fun [OF lam_type_RepFun subset_refl])
|
|
554 |
apply (erule lemmaX, assumption)
|
|
555 |
apply (blast intro: Card_is_Ord OrdmemD [THEN subsetD])
|
|
556 |
apply (blast intro: lesspoll_trans1 in_Card_imp_lesspoll RepFun_lepoll)
|
|
557 |
done
|
|
558 |
|
|
559 |
theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) --> DC(K)"
|
|
560 |
apply (unfold DC_def WO1_def)
|
|
561 |
apply (rule allI impI)+
|
|
562 |
apply (erule allE exE conjE)+
|
|
563 |
apply (rule_tac x = "\<lambda>b \<in> K. ff (b, X, Ra, R) " in bexI)
|
|
564 |
apply (simp add: lam_images_eq [OF Card_is_Ord ltD])
|
|
565 |
apply (fast elim!: ltE WO1_DC_lemma [THEN CollectD2])
|
|
566 |
apply (rule_tac lam_type)
|
|
567 |
apply (rule WO1_DC_lemma [THEN CollectD1], assumption+)
|
|
568 |
done
|
|
569 |
|
1196
|
570 |
end
|