author | paulson |
Tue, 26 Jun 2001 16:54:39 +0200 | |
changeset 11380 | e76366922751 |
parent 11317 | 7f9e4c389318 |
child 12153 | dc67fdb03a2a |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/DC.ML |
2 |
ID: $Id$ |
|
3 |
Author: Krzysztof Grabczewski |
|
1196 | 4 |
|
5 |
The proofs concerning the Axiom of Dependent Choice |
|
6 |
*) |
|
7 |
||
8 |
(* ********************************************************************** *) |
|
1461 | 9 |
(* DC ==> DC(omega) *) |
10 |
(* *) |
|
11 |
(* The scheme of the proof: *) |
|
12 |
(* *) |
|
5482 | 13 |
(* Assume DC. Let R and X satisfy the premise of DC(omega). *) |
1461 | 14 |
(* *) |
15 |
(* Define XX and RR as follows: *) |
|
16 |
(* *) |
|
11317 | 17 |
(* XX = (\\<Union>n \\<in> nat. {f \\<in> n->X. \\<forall>k \\<in> n. <f``k, f`k> \\<in> R}) *) |
1461 | 18 |
(* f RR g iff domain(g)=succ(domain(f)) & *) |
19 |
(* restrict(g, domain(f)) = f *) |
|
20 |
(* *) |
|
21 |
(* Then RR satisfies the hypotheses of DC. *) |
|
22 |
(* So applying DC: *) |
|
23 |
(* *) |
|
11317 | 24 |
(* \\<exists>f \\<in> nat->XX. \\<forall>n \\<in> nat. f`n RR f`succ(n) *) |
1461 | 25 |
(* *) |
26 |
(* Thence *) |
|
27 |
(* *) |
|
11317 | 28 |
(* ff = {<n, f`succ(n)`n>. n \\<in> nat} *) |
1461 | 29 |
(* *) |
30 |
(* is the desired function. *) |
|
31 |
(* *) |
|
1196 | 32 |
(* ********************************************************************** *) |
33 |
||
5482 | 34 |
Open_locale "DC0_imp"; |
35 |
||
36 |
val all_ex = thm "all_ex"; |
|
37 |
val XX_def = thm "XX_def"; |
|
38 |
val RR_def = thm "RR_def"; |
|
1196 | 39 |
|
11317 | 40 |
Goalw [RR_def] "RR \\<subseteq> XX*XX"; |
5482 | 41 |
by (Fast_tac 1); |
42 |
qed "lemma1_1"; |
|
43 |
||
11317 | 44 |
Goalw [RR_def, XX_def] "RR \\<noteq> 0"; |
5482 | 45 |
by (rtac (all_ex RS ballE) 1); |
1196 | 46 |
by (eresolve_tac [empty_subsetI RS PowI RSN (2, notE)] 2); |
47 |
by (eresolve_tac [nat_0I RS n_lesspoll_nat RSN (2, impE)] 1); |
|
1207 | 48 |
by (etac bexE 1); |
1196 | 49 |
by (res_inst_tac [("a","<0, {<0, x>}>")] not_emptyI 1); |
1207 | 50 |
by (rtac CollectI 1); |
51 |
by (rtac SigmaI 1); |
|
9683 | 52 |
by (rtac (nat_0I RS UN_I) 1); |
53 |
by (asm_simp_tac (simpset() addsimps [nat_0I RS UN_I]) 1); |
|
2493 | 54 |
by (rtac (nat_1I RS UN_I) 1); |
9683 | 55 |
by (asm_simp_tac (simpset() addsimps [singleton_0]) 2); |
5482 | 56 |
by (force_tac (claset() addSIs [singleton_fun RS Pi_type], |
9683 | 57 |
simpset() addsimps [singleton_0 RS sym]) 1); |
5482 | 58 |
qed "lemma1_2"; |
1196 | 59 |
|
11317 | 60 |
Goalw [RR_def, XX_def] "range(RR) \\<subseteq> domain(RR)"; |
1207 | 61 |
by (rtac range_subset_domain 1); |
5482 | 62 |
by (Blast_tac 2); |
63 |
by (Clarify_tac 1); |
|
64 |
by (forward_tac [fun_is_rel RS image_subset RS PowI RS (all_ex RS bspec)] 1); |
|
1196 | 65 |
by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] |
1461 | 66 |
MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 |
67 |
THEN REPEAT (assume_tac 1)); |
|
1207 | 68 |
by (etac bexE 1); |
1196 | 69 |
by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1); |
1207 | 70 |
by (rtac CollectI 1); |
5482 | 71 |
by (force_tac (claset() addSEs [cons_fun_type2], |
72 |
simpset() addsimps [cons_image_n, cons_val_n, |
|
73 |
cons_image_k, cons_val_k]) 1); |
|
4091 | 74 |
by (asm_full_simp_tac (simpset() |
5482 | 75 |
addsimps [domain_of_fun, succ_def, restrict_cons_eq]) 1); |
76 |
qed "lemma1_3"; |
|
1196 | 77 |
|
78 |
||
11317 | 79 |
Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; n \\<in> nat |] \ |
80 |
\ ==> \\<exists>k \\<in> nat. f`succ(n) \\<in> k -> X & n \\<in> k \ |
|
81 |
\ & <f`succ(n)``n, f`succ(n)`n> \\<in> R"; |
|
6070 | 82 |
by (induct_tac "n" 1); |
1196 | 83 |
by (dresolve_tac [nat_1I RSN (2, apply_type)] 1); |
84 |
by (dresolve_tac [nat_0I RSN (2, bspec)] 1); |
|
5482 | 85 |
by (asm_full_simp_tac (simpset() addsimps [XX_def]) 1); |
3731 | 86 |
by Safe_tac; |
1207 | 87 |
by (rtac bexI 1 THEN (assume_tac 2)); |
9402 | 88 |
by (best_tac (claset() addIs [ltD] |
5482 | 89 |
addSEs [nat_0_le RS leE] |
9402 | 90 |
addEs [sym RS trans RS succ_neq_0, domain_of_fun] |
91 |
addss (simpset() addsimps [RR_def])) 1); |
|
5482 | 92 |
(** LEVEL 7, other subgoal **) |
1196 | 93 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
11317 | 94 |
by (subgoal_tac "f ` succ(succ(x)) \\<in> succ(k)->X" 1); |
1196 | 95 |
by (dresolve_tac [nat_succI RS nat_succI RSN (2, apply_type)] 1 |
1461 | 96 |
THEN (assume_tac 1)); |
5482 | 97 |
by (full_simp_tac (simpset() addsimps [XX_def,RR_def]) 1); |
3731 | 98 |
by Safe_tac; |
2469 | 99 |
by (forw_inst_tac [("a","succ(k)")] (domain_of_fun RS sym RS trans) 1 THEN |
100 |
(assume_tac 1)); |
|
101 |
by (forw_inst_tac [("a","xa")] (domain_of_fun RS sym RS trans) 1 THEN |
|
102 |
(assume_tac 1)); |
|
5482 | 103 |
by (fast_tac (claset() addSEs [nat_into_Ord RS succ_in_succ] |
1461 | 104 |
addSDs [nat_into_Ord RS succ_in_succ RSN (2, bspec)]) 1); |
2469 | 105 |
by (dtac domain_of_fun 1); |
5482 | 106 |
by (full_simp_tac (simpset() addsimps [XX_def,RR_def]) 1); |
4091 | 107 |
by (deepen_tac (claset() addDs [domain_of_fun RS sym RS trans]) 0 1); |
5482 | 108 |
qed "lemma2"; |
1196 | 109 |
|
11317 | 110 |
Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; m \\<in> nat |] \ |
111 |
\ ==> {f`succ(x)`x. x \\<in> m} = {f`succ(m)`x. x \\<in> m}"; |
|
112 |
by (subgoal_tac "\\<forall>x \\<in> m. f`succ(m)`x = f`succ(x)`x" 1); |
|
5482 | 113 |
by (Asm_full_simp_tac 1); |
6070 | 114 |
by (induct_tac "m" 1); |
2469 | 115 |
by (Fast_tac 1); |
1207 | 116 |
by (rtac ballI 1); |
117 |
by (etac succE 1); |
|
118 |
by (rtac restrict_eq_imp_val_eq 1); |
|
1196 | 119 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
5482 | 120 |
by (asm_full_simp_tac (simpset() addsimps [RR_def]) 1); |
1207 | 121 |
by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
4091 | 122 |
by (fast_tac (claset() addSDs [domain_of_fun]) 1); |
1196 | 123 |
by (dres_inst_tac [("x","xa")] bspec 1 THEN (assume_tac 1)); |
124 |
by (eresolve_tac [sym RS trans RS sym] 1); |
|
125 |
by (resolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
|
126 |
by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1)); |
|
5482 | 127 |
by (asm_full_simp_tac (simpset() addsimps [RR_def]) 1); |
1207 | 128 |
by (dtac lemma2 1 THEN REPEAT (assume_tac 1)); |
5482 | 129 |
by (blast_tac (claset() addSDs [domain_of_fun] |
130 |
addIs [nat_into_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
|
131 |
qed "lemma3_1"; |
|
1196 | 132 |
|
11317 | 133 |
Goal "[| \\<forall>n \\<in> nat. <f`n, f`succ(n)> \\<in> RR; f \\<in> nat -> XX; m \\<in> nat |] \ |
134 |
\ ==> (\\<lambda>x \\<in> nat. f`succ(x)`x) `` m = f`succ(m)``m"; |
|
1207 | 135 |
by (etac natE 1); |
5482 | 136 |
by (Asm_simp_tac 1); |
137 |
by (stac image_lam 1); |
|
4091 | 138 |
by (fast_tac (claset() addSEs [[nat_succI, Ord_nat] MRS OrdmemD]) 1); |
5482 | 139 |
by (stac lemma3_1 1 THEN REPEAT (assume_tac 1)); |
140 |
by (Fast_tac 1); |
|
141 |
by (fast_tac (claset() addSDs [lemma2] |
|
142 |
addSEs [nat_into_Ord RSN (2, OrdmemD) RSN |
|
2469 | 143 |
(2, image_fun RS sym)]) 1); |
5482 | 144 |
qed "lemma3"; |
1196 | 145 |
|
6021 | 146 |
Close_locale "DC0_imp"; |
1196 | 147 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
148 |
Goalw [DC_def, DC0_def] "DC0 ==> DC(nat)"; |
5482 | 149 |
by (Clarify_tac 1); |
150 |
by (REPEAT (etac allE 1)); |
|
151 |
by (etac impE 1); |
|
152 |
(*these three results comprise Lemma 1*) |
|
153 |
by (blast_tac (claset() addSIs (map export [lemma1_1, lemma1_2, lemma1_3])) 1); |
|
1207 | 154 |
by (etac bexE 1); |
11317 | 155 |
by (res_inst_tac [("x","\\<lambda>n \\<in> nat. f`succ(n)`n")] bexI 1); |
5482 | 156 |
by (fast_tac (claset() addSIs [lam_type] addSDs [export lemma2] |
157 |
addSEs [fun_weaken_type, apply_type]) 2); |
|
1207 | 158 |
by (rtac oallI 1); |
5482 | 159 |
by (forward_tac [ltD RSN (3, export lemma2)] 1 |
1461 | 160 |
THEN assume_tac 2); |
5482 | 161 |
by (fast_tac (claset() addSEs [fun_weaken_type]) 1); |
162 |
(** LEVEL 10: last subgoal **) |
|
163 |
by (stac (ltD RSN (3, export lemma3)) 1); |
|
164 |
by (Force_tac 4); |
|
165 |
by (assume_tac 3); |
|
166 |
by (assume_tac 1); |
|
167 |
by (fast_tac (claset() addSEs [fun_weaken_type]) 1); |
|
168 |
qed "DC0_imp_DC_nat"; |
|
169 |
||
1196 | 170 |
|
3862 | 171 |
(* ************************************************************************ |
172 |
DC(omega) ==> DC |
|
173 |
||
174 |
The scheme of the proof: |
|
175 |
||
176 |
Assume DC(omega). Let R and x satisfy the premise of DC. |
|
177 |
||
178 |
Define XX and RR as follows: |
|
179 |
||
11317 | 180 |
XX = (\\<Union>n \\<in> nat. {f \\<in> succ(n)->domain(R). \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R}) |
3862 | 181 |
|
182 |
RR = {<z1,z2>:Fin(XX)*XX. |
|
11317 | 183 |
(domain(z2)=succ(\\<Union>f \\<in> z1. domain(f)) & |
184 |
(\\<forall>f \\<in> z1. restrict(z2, domain(f)) = f)) | |
|
185 |
(~ (\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> z1. domain(f)) & |
|
186 |
(\\<forall>f \\<in> z1. restrict(g, domain(f)) = f)) & |
|
3862 | 187 |
z2={<0,x>})} |
188 |
||
189 |
Then XX and RR satisfy the hypotheses of DC(omega). |
|
190 |
So applying DC: |
|
191 |
||
11317 | 192 |
\\<exists>f \\<in> nat->XX. \\<forall>n \\<in> nat. f``n RR f`n |
3862 | 193 |
|
194 |
Thence |
|
195 |
||
11317 | 196 |
ff = {<n, f`n`n>. n \\<in> nat} |
3862 | 197 |
|
198 |
is the desired function. |
|
199 |
||
200 |
************************************************************************* *) |
|
1196 | 201 |
|
11317 | 202 |
Goal "n \\<in> nat ==> \\<forall>A. (A eqpoll n & A \\<subseteq> X) --> A \\<in> Fin(X)"; |
6070 | 203 |
by (induct_tac "n" 1); |
1207 | 204 |
by (rtac allI 1); |
4091 | 205 |
by (fast_tac (claset() addSIs [Fin.emptyI] |
1461 | 206 |
addSDs [eqpoll_imp_lepoll RS lepoll_0_is_0]) 1); |
1207 | 207 |
by (rtac allI 1); |
208 |
by (rtac impI 1); |
|
209 |
by (etac conjE 1); |
|
1196 | 210 |
by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 |
1461 | 211 |
THEN (assume_tac 1)); |
7499 | 212 |
by (ftac Diff_sing_eqpoll 1 THEN (assume_tac 1)); |
1207 | 213 |
by (etac allE 1); |
214 |
by (etac impE 1); |
|
2469 | 215 |
by (Fast_tac 1); |
1207 | 216 |
by (dtac subsetD 1 THEN (assume_tac 1)); |
1196 | 217 |
by (dresolve_tac [Fin.consI] 1 THEN (assume_tac 1)); |
4091 | 218 |
by (asm_full_simp_tac (simpset() addsimps [cons_Diff]) 1); |
3731 | 219 |
qed "Finite_Fin_lemma"; |
1196 | 220 |
|
11317 | 221 |
Goalw [Finite_def] "[| Finite(A); A \\<subseteq> X |] ==> A \\<in> Fin(X)"; |
1207 | 222 |
by (etac bexE 1); |
223 |
by (dtac Finite_Fin_lemma 1); |
|
224 |
by (etac allE 1); |
|
225 |
by (etac impE 1); |
|
1196 | 226 |
by (assume_tac 2); |
2469 | 227 |
by (Fast_tac 1); |
3731 | 228 |
qed "Finite_Fin"; |
1196 | 229 |
|
5482 | 230 |
Goal |
11317 | 231 |
"x \\<in> X ==> {<0,x>}: (\\<Union>n \\<in> nat. {f \\<in> succ(n)->X. \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R})"; |
2493 | 232 |
by (rtac (nat_0I RS UN_I) 1); |
4091 | 233 |
by (fast_tac (claset() addSIs [singleton_fun RS Pi_type] |
234 |
addss (simpset() addsimps [singleton_0 RS sym])) 1); |
|
3731 | 235 |
qed "singleton_in_funs"; |
1196 | 236 |
|
5482 | 237 |
|
238 |
Open_locale "imp_DC0"; |
|
239 |
||
240 |
val XX_def = thm "XX_def"; |
|
241 |
val RR_def = thm "RR_def"; |
|
242 |
val allRR_def = thm "allRR_def"; |
|
243 |
||
11317 | 244 |
Goal "[| range(R) \\<subseteq> domain(R); x \\<in> domain(R) |] \ |
245 |
\ ==> RR \\<subseteq> Pow(XX)*XX & \ |
|
246 |
\ (\\<forall>Y \\<in> Pow(XX). Y lesspoll nat --> (\\<exists>x \\<in> XX. <Y,x>:RR))"; |
|
1207 | 247 |
by (rtac conjI 1); |
5482 | 248 |
by (force_tac (claset() addSDs [FinD RS PowI], |
249 |
simpset() addsimps [RR_def]) 1); |
|
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
250 |
by (rtac (impI RS ballI) 1); |
1196 | 251 |
by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1 |
1461 | 252 |
THEN (assume_tac 1)); |
11317 | 253 |
by (excluded_middle_tac "\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> Y. domain(f)) \ |
254 |
\ & (\\<forall>f \\<in> Y. restrict(g, domain(f)) = f)" 1); |
|
5482 | 255 |
by (fast_tac (claset() addss (simpset() addsimps [RR_def])) 2); |
4091 | 256 |
by (safe_tac (claset() delrules [domainE])); |
5482 | 257 |
by (rewrite_goals_tac [XX_def,RR_def]); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
258 |
by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2); |
4091 | 259 |
by (asm_full_simp_tac (simpset() addsimps [nat_0I RSN (2, bexI), |
5482 | 260 |
cons_fun_type2]) 1); |
261 |
qed "lemma4"; |
|
1196 | 262 |
|
11317 | 263 |
Goal "[| f \\<in> nat->X; n \\<in> nat |] ==> \ |
264 |
\ (\\<Union>x \\<in> f``succ(n). P(x)) = P(f`n) Un (\\<Union>x \\<in> f``n. P(x))"; |
|
4091 | 265 |
by (asm_full_simp_tac (simpset() |
1461 | 266 |
addsimps [Ord_nat RSN (2, OrdmemD) RSN (2, image_fun), |
267 |
[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
|
3731 | 268 |
qed "UN_image_succ_eq"; |
1196 | 269 |
|
11317 | 270 |
Goal "[| (\\<Union>x \\<in> f``n. P(x)) = y; P(f`n) = succ(y); \ |
271 |
\ f \\<in> nat -> X; n \\<in> nat |] ==> (\\<Union>x \\<in> f``succ(n). P(x)) = succ(y)"; |
|
4091 | 272 |
by (asm_full_simp_tac (simpset() addsimps [UN_image_succ_eq]) 1); |
2496 | 273 |
by (Fast_tac 1); |
3731 | 274 |
qed "UN_image_succ_eq_succ"; |
1196 | 275 |
|
11317 | 276 |
Goal "[| f \\<in> succ(n) -> D; n \\<in> nat; \ |
277 |
\ domain(f)=succ(x); x=y |] ==> f`y \\<in> D"; |
|
4091 | 278 |
by (fast_tac (claset() addEs [apply_type] |
5482 | 279 |
addSDs [[sym, domain_of_fun] MRS trans]) 1); |
3731 | 280 |
qed "apply_domain_type"; |
1196 | 281 |
|
11317 | 282 |
Goal "[| f \\<in> nat -> X; n \\<in> nat |] ==> f``succ(n) = cons(f`n, f``n)"; |
4091 | 283 |
by (asm_full_simp_tac (simpset() |
1461 | 284 |
addsimps [nat_succI, Ord_nat RSN (2, OrdmemD), image_fun]) 1); |
3731 | 285 |
qed "image_fun_succ"; |
1196 | 286 |
|
11317 | 287 |
Goalw [XX_def] "[| domain(f`n) = succ(u); f \\<in> nat -> XX; u=k; n \\<in> nat |] \ |
288 |
\ ==> f`n \\<in> succ(k) -> domain(R)"; |
|
1207 | 289 |
by (dtac apply_type 1 THEN (assume_tac 1)); |
5482 | 290 |
by (fast_tac (claset() addEs [domain_eq_imp_fun_type]) 1); |
3731 | 291 |
qed "f_n_type"; |
1196 | 292 |
|
5482 | 293 |
Goalw [XX_def] |
11317 | 294 |
"[| f \\<in> nat -> XX; domain(f`n) = succ(k); n \\<in> nat |] \ |
295 |
\ ==> \\<forall>i \\<in> k. <f`n`i, f`n`succ(i)> \\<in> R"; |
|
1207 | 296 |
by (dtac apply_type 1 THEN (assume_tac 1)); |
297 |
by (etac UN_E 1); |
|
298 |
by (etac CollectE 1); |
|
1196 | 299 |
by (dresolve_tac [domain_of_fun RS sym RS trans] 1 THEN (assume_tac 1)); |
2469 | 300 |
by (Asm_full_simp_tac 1); |
3731 | 301 |
qed "f_n_pairs_in_R"; |
1196 | 302 |
|
5068 | 303 |
Goalw [restrict_def] |
11317 | 304 |
"[| restrict(f, domain(x))=x; f \\<in> n->X; domain(x) \\<subseteq> n |] \ |
5482 | 305 |
\ ==> restrict(cons(<n, y>, f), domain(x)) = x"; |
1196 | 306 |
by (eresolve_tac [sym RS trans RS sym] 1); |
1207 | 307 |
by (rtac fun_extension 1); |
4091 | 308 |
by (fast_tac (claset() addSIs [lam_type]) 1); |
309 |
by (fast_tac (claset() addSIs [lam_type]) 1); |
|
310 |
by (asm_full_simp_tac (simpset() addsimps [subsetD RS cons_val_k]) 1); |
|
3731 | 311 |
qed "restrict_cons_eq_restrict"; |
1196 | 312 |
|
11317 | 313 |
Goal "[| \\<forall>x \\<in> f``n. restrict(f`n, domain(x))=x; \ |
314 |
\ f \\<in> nat -> XX; \ |
|
315 |
\ n \\<in> nat; domain(f`n) = succ(n); \ |
|
316 |
\ (\\<Union>x \\<in> f``n. domain(x)) \\<subseteq> n |] \ |
|
317 |
\ ==> \\<forall>x \\<in> f``succ(n). restrict(cons(<succ(n),y>, f`n), domain(x)) = x"; |
|
1207 | 318 |
by (rtac ballI 1); |
4091 | 319 |
by (asm_full_simp_tac (simpset() addsimps [image_fun_succ]) 1); |
1207 | 320 |
by (dtac f_n_type 1 THEN REPEAT (ares_tac [refl] 1)); |
2469 | 321 |
by (etac disjE 1); |
5482 | 322 |
by (asm_full_simp_tac (simpset() addsimps [domain_of_fun,restrict_cons_eq]) 1); |
1207 | 323 |
by (dtac bspec 1 THEN (assume_tac 1)); |
4091 | 324 |
by (fast_tac (claset() addSEs [restrict_cons_eq_restrict]) 1); |
3731 | 325 |
qed "all_in_image_restrict_eq"; |
1196 | 326 |
|
5482 | 327 |
Goalw [RR_def, allRR_def] |
11317 | 328 |
"[| \\<forall>b<nat. <f``b, f`b> \\<in> RR; \ |
329 |
\ f \\<in> nat -> XX; range(R) \\<subseteq> domain(R); x \\<in> domain(R)|] \ |
|
5482 | 330 |
\ ==> allRR"; |
1207 | 331 |
by (rtac oallI 1); |
332 |
by (dtac ltD 1); |
|
333 |
by (etac nat_induct 1); |
|
1196 | 334 |
by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1); |
1200 | 335 |
by (fast_tac (FOL_cs addss |
4091 | 336 |
(simpset() addsimps [singleton_fun RS domain_of_fun, |
2493 | 337 |
singleton_0, singleton_in_funs])) 1); |
2469 | 338 |
(*induction step*) (** LEVEL 5 **) |
11317 | 339 |
by (full_simp_tac (*prevent simplification of ~\\<exists>to \\<forall>~*) |
3862 | 340 |
(FOL_ss addsimps [separation, split]) 1); |
1196 | 341 |
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
1461 | 342 |
THEN (assume_tac 1)); |
2469 | 343 |
by (REPEAT (eresolve_tac [conjE, disjE] 1)); |
5482 | 344 |
by (force_tac (FOL_cs addSEs [trans, subst_context] |
345 |
addSIs [UN_image_succ_eq_succ], simpset()) 1); |
|
1207 | 346 |
by (etac conjE 1); |
347 |
by (etac notE 1); |
|
5482 | 348 |
by (asm_lr_simp_tac (simpset() addsimps [XX_def, UN_image_succ_eq_succ]) 1); |
2469 | 349 |
(** LEVEL 12 **) |
350 |
by (REPEAT (eresolve_tac [conjE, bexE] 1)); |
|
351 |
by (dtac apply_domain_type 1 THEN REPEAT (assume_tac 1)); |
|
1207 | 352 |
by (etac domainE 1); |
353 |
by (etac domainE 1); |
|
5482 | 354 |
by (forward_tac [export f_n_type] 1 THEN REPEAT (assume_tac 1)); |
2493 | 355 |
by (rtac bexI 1); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
356 |
by (etac nat_succI 2); |
1196 | 357 |
by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1); |
2493 | 358 |
by (rtac conjI 1); |
1196 | 359 |
by (fast_tac (FOL_cs |
1461 | 360 |
addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ, |
5482 | 361 |
subst_context, export all_in_image_restrict_eq, |
362 |
trans, equalityD1]) 2); |
|
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
363 |
by (eresolve_tac [rangeI RSN (2, subsetD) RSN (2, cons_fun_type2)] 2 |
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
364 |
THEN REPEAT (assume_tac 2)); |
1207 | 365 |
by (rtac ballI 1); |
366 |
by (etac succE 1); |
|
2469 | 367 |
(** LEVEL 25 **) |
5482 | 368 |
by (dresolve_tac [domain_of_fun RSN (2, export f_n_pairs_in_R)] 2 |
2469 | 369 |
THEN REPEAT (assume_tac 2)); |
370 |
by (dtac bspec 2 THEN (assume_tac 2)); |
|
4091 | 371 |
by (asm_full_simp_tac (simpset() |
2469 | 372 |
addsimps [nat_into_Ord RS succ_in_succ, succI2, cons_val_k]) 2); |
4091 | 373 |
by (asm_full_simp_tac (simpset() addsimps [cons_val_n, cons_val_k]) 1); |
3731 | 374 |
qed "simplify_recursion"; |
1196 | 375 |
|
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
376 |
|
5482 | 377 |
Goalw [allRR_def] |
11317 | 378 |
"[| allRR; f \\<in> nat -> XX; range(R) \\<subseteq> domain(R); x \\<in> domain(R); n \\<in> nat |] \ |
379 |
\ ==> f`n \\<in> succ(n) -> domain(R) & (\\<forall>i \\<in> n. <f`n`i, f`n`succ(i)>:R)"; |
|
1207 | 380 |
by (dtac ospec 1); |
1196 | 381 |
by (eresolve_tac [Ord_nat RSN (2, ltI)] 1); |
1207 | 382 |
by (etac CollectE 1); |
2469 | 383 |
by (Asm_full_simp_tac 1); |
1207 | 384 |
by (rtac conjI 1); |
5482 | 385 |
by (fast_tac (FOL_cs addSEs [conjE, f_n_pairs_in_R, trans, subst_context]) 2); |
386 |
by (rewtac XX_def); |
|
4091 | 387 |
by (fast_tac (claset() |
1461 | 388 |
addSEs [trans RS domain_eq_imp_fun_type, subst_context]) 1); |
5482 | 389 |
qed "lemma2"; |
1196 | 390 |
|
11317 | 391 |
Goal "[| allRR; f \\<in> nat -> XX; n \\<in> nat; range(R) \\<subseteq> domain(R); x \\<in> domain(R) \ |
1461 | 392 |
\ |] ==> f`n`n = f`succ(n)`n"; |
1196 | 393 |
by (forward_tac [lemma2 RS conjunct1 RS domain_of_fun] 1 |
1461 | 394 |
THEN REPEAT (assume_tac 1)); |
5482 | 395 |
by (rewtac allRR_def); |
1196 | 396 |
by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1 |
1461 | 397 |
THEN (assume_tac 1)); |
2469 | 398 |
by (Asm_full_simp_tac 1); |
1207 | 399 |
by (REPEAT (etac conjE 1)); |
400 |
by (etac ballE 1); |
|
1196 | 401 |
by (eresolve_tac [restrict_eq_imp_val_eq RS sym] 1); |
4091 | 402 |
by (fast_tac (claset() addSEs [ssubst]) 1); |
403 |
by (asm_full_simp_tac (simpset() |
|
1461 | 404 |
addsimps [[nat_succI, Ord_nat] MRS OrdmemD RSN (2, image_fun)]) 1); |
5482 | 405 |
qed "lemma3"; |
406 |
||
6021 | 407 |
Close_locale "imp_DC0"; |
1196 | 408 |
|
3862 | 409 |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
410 |
Goalw [DC_def, DC0_def] "DC(nat) ==> DC0"; |
1196 | 411 |
by (REPEAT (resolve_tac [allI, impI] 1)); |
412 |
by (REPEAT (eresolve_tac [asm_rl, conjE, ex_in_domain RS exE, allE] 1)); |
|
5482 | 413 |
by (eresolve_tac [export lemma4 RSN (2, impE)] 1 |
1461 | 414 |
THEN REPEAT (assume_tac 1)); |
1207 | 415 |
by (etac bexE 1); |
5482 | 416 |
by (dresolve_tac [export simplify_recursion] 1 |
1461 | 417 |
THEN REPEAT (assume_tac 1)); |
11317 | 418 |
by (res_inst_tac [("x","\\<lambda>n \\<in> nat. f`n`n")] bexI 1); |
1207 | 419 |
by (rtac lam_type 2); |
5482 | 420 |
by (eresolve_tac [[export lemma2 RS conjunct1, succI1] MRS apply_type] 2 |
1461 | 421 |
THEN REPEAT (assume_tac 2)); |
1207 | 422 |
by (rtac ballI 1); |
5482 | 423 |
by (forward_tac [export (nat_succI RSN (5,lemma2)) RS conjunct2] 1 |
1461 | 424 |
THEN REPEAT (assume_tac 1)); |
5482 | 425 |
by (dresolve_tac [export lemma3] 1 THEN REPEAT (assume_tac 1)); |
4091 | 426 |
by (asm_full_simp_tac (simpset() addsimps [nat_succI]) 1); |
5482 | 427 |
qed "DC_nat_imp_DC0"; |
1196 | 428 |
|
429 |
(* ********************************************************************** *) |
|
11317 | 430 |
(* \\<forall>K. Card(K) --> DC(K) ==> WO3 *) |
1196 | 431 |
(* ********************************************************************** *) |
432 |
||
5068 | 433 |
Goalw [lesspoll_def] |
11317 | 434 |
"[| ~ A lesspoll B; C lesspoll B |] ==> A - C \\<noteq> 0"; |
4091 | 435 |
by (fast_tac (claset() addSDs [Diff_eq_0_iff RS iffD1 RS subset_imp_lepoll] |
1461 | 436 |
addSIs [eqpollI] addEs [notE] addSEs [eqpollE, lepoll_trans]) 1); |
5482 | 437 |
qed "lesspoll_lemma"; |
1196 | 438 |
|
439 |
val [f_type, Ord_a, not_eq] = goalw thy [inj_def] |
|
11317 | 440 |
"[| f \\<in> a->X; Ord(a); (!!b c. [| b<c; c \\<in> a |] ==> f`b\\<noteq>f`c) |] \ |
441 |
\ ==> f \\<in> inj(a, X)"; |
|
1196 | 442 |
by (resolve_tac [f_type RS CollectI] 1); |
443 |
by (REPEAT (resolve_tac [ballI,impI] 1)); |
|
444 |
by (resolve_tac [Ord_a RS Ord_in_Ord RS Ord_linear_lt] 1 |
|
1461 | 445 |
THEN (assume_tac 1)); |
1196 | 446 |
by (eres_inst_tac [("j","x")] (Ord_a RS Ord_in_Ord) 1); |
4091 | 447 |
by (REPEAT (fast_tac (claset() addDs [not_eq, not_eq RS not_sym]) 1)); |
3731 | 448 |
qed "fun_Ord_inj"; |
1196 | 449 |
|
11317 | 450 |
Goal "[| f \\<in> X->Y; A \\<subseteq> X; a \\<in> A |] ==> f`a \\<in> f``A"; |
4091 | 451 |
by (fast_tac (claset() addSEs [image_fun RS ssubst]) 1); |
3731 | 452 |
qed "value_in_image"; |
1196 | 453 |
|
11317 | 454 |
Goalw [DC_def, WO3_def] "\\<forall>K. Card(K) --> DC(K) ==> WO3"; |
1207 | 455 |
by (rtac allI 1); |
1196 | 456 |
by (excluded_middle_tac "A lesspoll Hartog(A)" 1); |
4091 | 457 |
by (fast_tac (claset() addSDs [lesspoll_imp_ex_lt_eqpoll] |
1461 | 458 |
addSIs [Ord_Hartog, leI RS le_imp_subset]) 2); |
1196 | 459 |
by (REPEAT (eresolve_tac [allE, impE] 1)); |
1207 | 460 |
by (rtac Card_Hartog 1); |
1196 | 461 |
by (eres_inst_tac [("x","A")] allE 1); |
2469 | 462 |
by (eres_inst_tac [("x","{<z1,z2>:Pow(A)*A . z1 \ |
11317 | 463 |
\ lesspoll Hartog(A) & z2 \\<notin> z1}")] allE 1); |
2469 | 464 |
by (Asm_full_simp_tac 1); |
1207 | 465 |
by (etac impE 1); |
4091 | 466 |
by (fast_tac (claset() addEs [lesspoll_lemma RS not_emptyE]) 1); |
1207 | 467 |
by (etac bexE 1); |
1196 | 468 |
by (resolve_tac [exI RS (lepoll_def RS (def_imp_iff RS iffD2)) |
1461 | 469 |
RS (HartogI RS notE)] 1); |
1196 | 470 |
by (resolve_tac [Ord_Hartog RSN (2, fun_Ord_inj)] 1 THEN (assume_tac 1)); |
471 |
by (dresolve_tac [Ord_Hartog RSN (2, OrdmemD) RSN (2, |
|
1461 | 472 |
ltD RSN (3, value_in_image))] 1 |
473 |
THEN REPEAT (assume_tac 1)); |
|
5482 | 474 |
by (force_tac (claset() addSDs [Ord_Hartog RSN (2, ltI) RSN (2, ospec)], |
475 |
simpset()) 1); |
|
1196 | 476 |
qed "DC_WO3"; |
477 |
||
478 |
(* ********************************************************************** *) |
|
11317 | 479 |
(* WO1 ==> \\<forall>K. Card(K) --> DC(K) *) |
1196 | 480 |
(* ********************************************************************** *) |
481 |
||
11317 | 482 |
Goal "[| Ord(a); b \\<in> a |] ==> (\\<lambda>x \\<in> a. P(x))``b = (\\<lambda>x \\<in> b. P(x))``b"; |
1207 | 483 |
by (rtac images_eq 1); |
4091 | 484 |
by (REPEAT (fast_tac (claset() addSEs [RepFunI, OrdmemD] |
1461 | 485 |
addSIs [lam_type]) 2)); |
1207 | 486 |
by (rtac ballI 1); |
1196 | 487 |
by (dresolve_tac [OrdmemD RS subsetD] 1 |
1461 | 488 |
THEN REPEAT (assume_tac 1)); |
2469 | 489 |
by (Asm_full_simp_tac 1); |
3731 | 490 |
qed "lam_images_eq"; |
1196 | 491 |
|
11317 | 492 |
Goalw [lesspoll_def] "[| Card(K); b \\<in> K |] ==> b lesspoll K"; |
4091 | 493 |
by (asm_full_simp_tac (simpset() addsimps [Card_iff_initial]) 1); |
494 |
by (fast_tac (claset() addSIs [le_imp_lepoll, ltI, leI]) 1); |
|
3731 | 495 |
qed "in_Card_imp_lesspoll"; |
1196 | 496 |
|
11317 | 497 |
Goal "(\\<lambda>b \\<in> a. P(b)) \\<in> a -> {P(b). b \\<in> a}"; |
4091 | 498 |
by (fast_tac (claset() addSIs [lam_type, RepFunI]) 1); |
3731 | 499 |
qed "lam_type_RepFun"; |
1196 | 500 |
|
11317 | 501 |
Goal "[| \\<forall>Y \\<in> Pow(X). Y lesspoll K --> (\\<exists>x \\<in> X. <Y, x> \\<in> R); \ |
502 |
\ b \\<in> K; Z \\<in> Pow(X); Z lesspoll K |] \ |
|
503 |
\ ==> {x \\<in> X. <Z,x> \\<in> R} \\<noteq> 0"; |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
504 |
by (Blast_tac 1); |
5482 | 505 |
qed "lemmaX"; |
1196 | 506 |
|
5137 | 507 |
Goal "[| Card(K); well_ord(X,Q); \ |
11317 | 508 |
\ \\<forall>Y \\<in> Pow(X). Y lesspoll K --> (\\<exists>x \\<in> X. <Y, x> \\<in> R); b \\<in> K |] \ |
509 |
\ ==> ff(b, X, Q, R) \\<in> {x \\<in> X. <(\\<lambda>c \\<in> b. ff(c, X, Q, R))``b, x> \\<in> R}"; |
|
510 |
by (res_inst_tac [("P","b \\<in> K")] impE 1 THEN TRYALL assume_tac); |
|
1196 | 511 |
by (res_inst_tac [("i","b")] (Card_is_Ord RS Ord_in_Ord RS trans_induct) 1 |
1461 | 512 |
THEN REPEAT (assume_tac 1)); |
1207 | 513 |
by (rtac impI 1); |
1196 | 514 |
by (resolve_tac [ff_def RS def_transrec RS ssubst] 1); |
1207 | 515 |
by (etac the_first_in 1); |
2469 | 516 |
by (Fast_tac 1); |
4091 | 517 |
by (asm_full_simp_tac (simpset() |
1461 | 518 |
addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); |
5241 | 519 |
by (etac lemmaX 1 THEN assume_tac 1); |
520 |
by (blast_tac (claset() addIs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); |
|
4091 | 521 |
by (fast_tac (claset() addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] |
5241 | 522 |
MRS lepoll_lesspoll_lesspoll]) 1); |
5482 | 523 |
qed "lemma"; |
1196 | 524 |
|
11317 | 525 |
Goalw [DC_def, WO1_def] "WO1 ==> \\<forall>K. Card(K) --> DC(K)"; |
1196 | 526 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
527 |
by (REPEAT (eresolve_tac [allE,exE,conjE] 1)); |
|
11317 | 528 |
by (res_inst_tac [("x","\\<lambda>b \\<in> K. ff(b, X, Ra, R)")] bexI 1); |
1207 | 529 |
by (rtac lam_type 2); |
1196 | 530 |
by (resolve_tac [lemma RS CollectD1] 2 THEN REPEAT (assume_tac 2)); |
4091 | 531 |
by (asm_full_simp_tac (simpset() |
1461 | 532 |
addsimps [[Card_is_Ord, ltD] MRS lam_images_eq]) 1); |
4091 | 533 |
by (fast_tac (claset() addSEs [ltE, lemma RS CollectD2]) 1); |
4723
9e2609b1bfb1
Adapted proofs because of new simplification tactics.
nipkow
parents:
4091
diff
changeset
|
534 |
qed "WO1_DC_Card"; |