author | obua |
Thu, 16 Feb 2006 04:17:19 +0100 | |
changeset 19067 | c0321d7d6b3d |
parent 16417 | 9bc16273c2d4 |
child 24893 | b8ef7afe3a6b |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Zorn.thy |
516 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
516 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
*) |
|
7 |
||
13356 | 8 |
header{*Zorn's Lemma*} |
9 |
||
16417 | 10 |
theory Zorn imports OrderArith AC Inductive begin |
516 | 11 |
|
13356 | 12 |
text{*Based upon the unpublished article ``Towards the Mechanization of the |
13 |
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*} |
|
14 |
||
13134 | 15 |
constdefs |
16 |
Subset_rel :: "i=>i" |
|
13558 | 17 |
"Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}" |
13134 | 18 |
|
19 |
chain :: "i=>i" |
|
13558 | 20 |
"chain(A) == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}" |
516 | 21 |
|
14653 | 22 |
super :: "[i,i]=>i" |
23 |
"super(A,c) == {d \<in> chain(A). c<=d & c\<noteq>d}" |
|
24 |
||
13134 | 25 |
maxchain :: "i=>i" |
13558 | 26 |
"maxchain(A) == {c \<in> chain(A). super(A,c)=0}" |
27 |
||
516 | 28 |
|
13134 | 29 |
constdefs |
30 |
increasing :: "i=>i" |
|
13558 | 31 |
"increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A --> x<=f`x}" |
516 | 32 |
|
13356 | 33 |
|
13558 | 34 |
text{*Lemma for the inductive definition below*} |
35 |
lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> Union(Y) \<in> Pow(A)" |
|
13356 | 36 |
by blast |
37 |
||
38 |
||
13558 | 39 |
text{*We could make the inductive definition conditional on |
13356 | 40 |
@{term "next \<in> increasing(S)"} |
516 | 41 |
but instead we make this a side-condition of an introduction rule. Thus |
42 |
the induction rule lets us assume that condition! Many inductive proofs |
|
13356 | 43 |
are therefore unconditional.*} |
516 | 44 |
consts |
13134 | 45 |
"TFin" :: "[i,i]=>i" |
516 | 46 |
|
47 |
inductive |
|
48 |
domains "TFin(S,next)" <= "Pow(S)" |
|
13134 | 49 |
intros |
13558 | 50 |
nextI: "[| x \<in> TFin(S,next); next \<in> increasing(S) |] |
51 |
==> next`x \<in> TFin(S,next)" |
|
516 | 52 |
|
13558 | 53 |
Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> Union(Y) \<in> TFin(S,next)" |
516 | 54 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1478
diff
changeset
|
55 |
monos Pow_mono |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
1478
diff
changeset
|
56 |
con_defs increasing_def |
13134 | 57 |
type_intros CollectD1 [THEN apply_funtype] Union_in_Pow |
58 |
||
59 |
||
13356 | 60 |
subsection{*Mathematical Preamble *} |
13134 | 61 |
|
13558 | 62 |
lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)" |
13269 | 63 |
by blast |
13134 | 64 |
|
13356 | 65 |
lemma Inter_lemma0: |
13558 | 66 |
"[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A <= Inter(C) | Inter(C) <= B" |
13269 | 67 |
by blast |
13134 | 68 |
|
69 |
||
13356 | 70 |
subsection{*The Transfinite Construction *} |
13134 | 71 |
|
13558 | 72 |
lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)" |
13134 | 73 |
apply (unfold increasing_def) |
74 |
apply (erule CollectD1) |
|
75 |
done |
|
76 |
||
13558 | 77 |
lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x" |
13269 | 78 |
by (unfold increasing_def, blast) |
13134 | 79 |
|
80 |
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard] |
|
81 |
||
82 |
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard] |
|
83 |
||
84 |
||
13558 | 85 |
text{*Structural induction on @{term "TFin(S,next)"} *} |
13134 | 86 |
lemma TFin_induct: |
13558 | 87 |
"[| n \<in> TFin(S,next); |
88 |
!!x. [| x \<in> TFin(S,next); P(x); next \<in> increasing(S) |] ==> P(next`x); |
|
89 |
!!Y. [| Y <= TFin(S,next); \<forall>y\<in>Y. P(y) |] ==> P(Union(Y)) |
|
13134 | 90 |
|] ==> P(n)" |
13356 | 91 |
by (erule TFin.induct, blast+) |
13134 | 92 |
|
93 |
||
13356 | 94 |
subsection{*Some Properties of the Transfinite Construction *} |
13134 | 95 |
|
13558 | 96 |
lemmas increasing_trans = subset_trans [OF _ increasingD2, |
13134 | 97 |
OF _ _ TFin_is_subset] |
98 |
||
13558 | 99 |
text{*Lemma 1 of section 3.1*} |
13134 | 100 |
lemma TFin_linear_lemma1: |
13558 | 101 |
"[| n \<in> TFin(S,next); m \<in> TFin(S,next); |
102 |
\<forall>x \<in> TFin(S,next) . x<=m --> x=m | next`x<=m |] |
|
13134 | 103 |
==> n<=m | next`m<=n" |
104 |
apply (erule TFin_induct) |
|
105 |
apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*) |
|
106 |
(*downgrade subsetI from intro! to intro*) |
|
107 |
apply (blast dest: increasing_trans) |
|
108 |
done |
|
109 |
||
13558 | 110 |
text{*Lemma 2 of section 3.2. Interesting in its own right! |
111 |
Requires @{term "next \<in> increasing(S)"} in the second induction step.*} |
|
13134 | 112 |
lemma TFin_linear_lemma2: |
13558 | 113 |
"[| m \<in> TFin(S,next); next \<in> increasing(S) |] |
114 |
==> \<forall>n \<in> TFin(S,next). n<=m --> n=m | next`n <= m" |
|
13134 | 115 |
apply (erule TFin_induct) |
116 |
apply (rule impI [THEN ballI]) |
|
13558 | 117 |
txt{*case split using @{text TFin_linear_lemma1}*} |
13784 | 118 |
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], |
13134 | 119 |
assumption+) |
120 |
apply (blast del: subsetI |
|
13558 | 121 |
intro: increasing_trans subsetI, blast) |
122 |
txt{*second induction step*} |
|
13134 | 123 |
apply (rule impI [THEN ballI]) |
124 |
apply (rule Union_lemma0 [THEN disjE]) |
|
125 |
apply (erule_tac [3] disjI2) |
|
13558 | 126 |
prefer 2 apply blast |
13134 | 127 |
apply (rule ballI) |
13558 | 128 |
apply (drule bspec, assumption) |
129 |
apply (drule subsetD, assumption) |
|
13784 | 130 |
apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], |
13558 | 131 |
assumption+, blast) |
13134 | 132 |
apply (erule increasingD2 [THEN subset_trans, THEN disjI1]) |
133 |
apply (blast dest: TFin_is_subset)+ |
|
134 |
done |
|
135 |
||
13558 | 136 |
text{*a more convenient form for Lemma 2*} |
13134 | 137 |
lemma TFin_subsetD: |
13558 | 138 |
"[| n<=m; m \<in> TFin(S,next); n \<in> TFin(S,next); next \<in> increasing(S) |] |
139 |
==> n=m | next`n <= m" |
|
140 |
by (blast dest: TFin_linear_lemma2 [rule_format]) |
|
13134 | 141 |
|
13558 | 142 |
text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*} |
13134 | 143 |
lemma TFin_subset_linear: |
13558 | 144 |
"[| m \<in> TFin(S,next); n \<in> TFin(S,next); next \<in> increasing(S) |] |
145 |
==> n <= m | m<=n" |
|
146 |
apply (rule disjE) |
|
13134 | 147 |
apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2]) |
148 |
apply (assumption+, erule disjI2) |
|
13558 | 149 |
apply (blast del: subsetI |
13134 | 150 |
intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset) |
151 |
done |
|
152 |
||
153 |
||
13558 | 154 |
text{*Lemma 3 of section 3.3*} |
13134 | 155 |
lemma equal_next_upper: |
13558 | 156 |
"[| n \<in> TFin(S,next); m \<in> TFin(S,next); m = next`m |] ==> n <= m" |
13134 | 157 |
apply (erule TFin_induct) |
158 |
apply (drule TFin_subsetD) |
|
13784 | 159 |
apply (assumption+, force, blast) |
13134 | 160 |
done |
161 |
||
13558 | 162 |
text{*Property 3.3 of section 3.3*} |
163 |
lemma equal_next_Union: |
|
164 |
"[| m \<in> TFin(S,next); next \<in> increasing(S) |] |
|
13134 | 165 |
==> m = next`m <-> m = Union(TFin(S,next))" |
166 |
apply (rule iffI) |
|
167 |
apply (rule Union_upper [THEN equalityI]) |
|
168 |
apply (rule_tac [2] equal_next_upper [THEN Union_least]) |
|
169 |
apply (assumption+) |
|
170 |
apply (erule ssubst) |
|
13269 | 171 |
apply (rule increasingD2 [THEN equalityI], assumption) |
13134 | 172 |
apply (blast del: subsetI |
173 |
intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+ |
|
174 |
done |
|
175 |
||
176 |
||
13356 | 177 |
subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*} |
178 |
||
179 |
text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset |
|
180 |
relation!*} |
|
13134 | 181 |
|
13558 | 182 |
text{** Defining the "next" operation for Hausdorff's Theorem **} |
13134 | 183 |
|
184 |
lemma chain_subset_Pow: "chain(A) <= Pow(A)" |
|
185 |
apply (unfold chain_def) |
|
186 |
apply (rule Collect_subset) |
|
187 |
done |
|
188 |
||
189 |
lemma super_subset_chain: "super(A,c) <= chain(A)" |
|
190 |
apply (unfold super_def) |
|
191 |
apply (rule Collect_subset) |
|
192 |
done |
|
193 |
||
194 |
lemma maxchain_subset_chain: "maxchain(A) <= chain(A)" |
|
195 |
apply (unfold maxchain_def) |
|
196 |
apply (rule Collect_subset) |
|
197 |
done |
|
198 |
||
13558 | 199 |
lemma choice_super: |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
200 |
"[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |] |
13558 | 201 |
==> ch ` super(S,X) \<in> super(S,X)" |
13134 | 202 |
apply (erule apply_type) |
13269 | 203 |
apply (unfold super_def maxchain_def, blast) |
13134 | 204 |
done |
205 |
||
206 |
lemma choice_not_equals: |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
207 |
"[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |] |
13558 | 208 |
==> ch ` super(S,X) \<noteq> X" |
13134 | 209 |
apply (rule notI) |
13784 | 210 |
apply (drule choice_super, assumption, assumption) |
13134 | 211 |
apply (simp add: super_def) |
212 |
done |
|
213 |
||
13558 | 214 |
text{*This justifies Definition 4.4*} |
13134 | 215 |
lemma Hausdorff_next_exists: |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
216 |
"ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==> |
13558 | 217 |
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S). |
218 |
next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)" |
|
219 |
apply (rule_tac x="\<lambda>X\<in>Pow(S). |
|
220 |
if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X" |
|
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset
|
221 |
in bexI) |
13558 | 222 |
apply force |
13134 | 223 |
apply (unfold increasing_def) |
224 |
apply (rule CollectI) |
|
225 |
apply (rule lam_type) |
|
226 |
apply (simp (no_asm_simp)) |
|
13558 | 227 |
apply (blast dest: super_subset_chain [THEN subsetD] |
228 |
chain_subset_Pow [THEN subsetD] choice_super) |
|
229 |
txt{*Now, verify that it increases*} |
|
13134 | 230 |
apply (simp (no_asm_simp) add: Pow_iff subset_refl) |
231 |
apply safe |
|
232 |
apply (drule choice_super) |
|
233 |
apply (assumption+) |
|
13269 | 234 |
apply (simp add: super_def, blast) |
13134 | 235 |
done |
236 |
||
13558 | 237 |
text{*Lemma 4*} |
13134 | 238 |
lemma TFin_chain_lemma4: |
13558 | 239 |
"[| c \<in> TFin(S,next); |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
240 |
ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X); |
13558 | 241 |
next \<in> increasing(S); |
242 |
\<forall>X \<in> Pow(S). next`X = |
|
243 |
if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |] |
|
244 |
==> c \<in> chain(S)" |
|
13134 | 245 |
apply (erule TFin_induct) |
13558 | 246 |
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] |
13134 | 247 |
choice_super [THEN super_subset_chain [THEN subsetD]]) |
248 |
apply (unfold chain_def) |
|
13269 | 249 |
apply (rule CollectI, blast, safe) |
13558 | 250 |
apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) |
251 |
txt{*@{text "Blast_tac's"} slow*} |
|
13134 | 252 |
done |
253 |
||
13558 | 254 |
theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)" |
13134 | 255 |
apply (rule AC_Pi_Pow [THEN exE]) |
13269 | 256 |
apply (rule Hausdorff_next_exists [THEN bexE], assumption) |
13134 | 257 |
apply (rename_tac ch "next") |
13558 | 258 |
apply (subgoal_tac "Union (TFin (S,next)) \<in> chain (S) ") |
13134 | 259 |
prefer 2 |
260 |
apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI]) |
|
261 |
apply (rule_tac x = "Union (TFin (S,next))" in exI) |
|
262 |
apply (rule classical) |
|
263 |
apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))") |
|
264 |
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric]) |
|
265 |
apply (rule_tac [2] subset_refl [THEN TFin_UnionI]) |
|
13269 | 266 |
prefer 2 apply assumption |
13134 | 267 |
apply (rule_tac [2] refl) |
13558 | 268 |
apply (simp add: subset_refl [THEN TFin_UnionI, |
13134 | 269 |
THEN TFin.dom_subset [THEN subsetD, THEN PowD]]) |
270 |
apply (erule choice_not_equals [THEN notE]) |
|
271 |
apply (assumption+) |
|
272 |
done |
|
273 |
||
274 |
||
13558 | 275 |
subsection{*Zorn's Lemma: If All Chains in S Have Upper Bounds In S, |
276 |
then S contains a Maximal Element*} |
|
13356 | 277 |
|
13558 | 278 |
text{*Used in the proof of Zorn's Lemma*} |
279 |
lemma chain_extend: |
|
280 |
"[| c \<in> chain(A); z \<in> A; \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)" |
|
13356 | 281 |
by (unfold chain_def, blast) |
13134 | 282 |
|
13558 | 283 |
lemma Zorn: "\<forall>c \<in> chain(S). Union(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z --> y=z" |
13134 | 284 |
apply (rule Hausdorff [THEN exE]) |
285 |
apply (simp add: maxchain_def) |
|
286 |
apply (rename_tac c) |
|
287 |
apply (rule_tac x = "Union (c)" in bexI) |
|
13269 | 288 |
prefer 2 apply blast |
13134 | 289 |
apply safe |
290 |
apply (rename_tac z) |
|
291 |
apply (rule classical) |
|
13558 | 292 |
apply (subgoal_tac "cons (z,c) \<in> super (S,c) ") |
13134 | 293 |
apply (blast elim: equalityE) |
13269 | 294 |
apply (unfold super_def, safe) |
13134 | 295 |
apply (fast elim: chain_extend) |
296 |
apply (fast elim: equalityE) |
|
297 |
done |
|
298 |
||
299 |
||
13356 | 300 |
subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*} |
13134 | 301 |
|
13558 | 302 |
text{*Lemma 5*} |
13134 | 303 |
lemma TFin_well_lemma5: |
13558 | 304 |
"[| n \<in> TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) \<in> Z |] |
305 |
==> \<forall>m \<in> Z. n <= m" |
|
13134 | 306 |
apply (erule TFin_induct) |
13558 | 307 |
prefer 2 apply blast txt{*second induction step is easy*} |
13134 | 308 |
apply (rule ballI) |
13558 | 309 |
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) |
13134 | 310 |
apply (subgoal_tac "m = Inter (Z) ") |
311 |
apply blast+ |
|
312 |
done |
|
313 |
||
13558 | 314 |
text{*Well-ordering of @{term "TFin(S,next)"} *} |
315 |
lemma well_ord_TFin_lemma: "[| Z <= TFin(S,next); z \<in> Z |] ==> Inter(Z) \<in> Z" |
|
13134 | 316 |
apply (rule classical) |
317 |
apply (subgoal_tac "Z = {Union (TFin (S,next))}") |
|
318 |
apply (simp (no_asm_simp) add: Inter_singleton) |
|
319 |
apply (erule equal_singleton) |
|
320 |
apply (rule Union_upper [THEN equalityI]) |
|
13269 | 321 |
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+) |
13134 | 322 |
done |
323 |
||
13558 | 324 |
text{*This theorem just packages the previous result*} |
13134 | 325 |
lemma well_ord_TFin: |
13558 | 326 |
"next \<in> increasing(S) |
327 |
==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))" |
|
13134 | 328 |
apply (rule well_ordI) |
329 |
apply (unfold Subset_rel_def linear_def) |
|
13558 | 330 |
txt{*Prove the well-foundedness goal*} |
13134 | 331 |
apply (rule wf_onI) |
13269 | 332 |
apply (frule well_ord_TFin_lemma, assumption) |
333 |
apply (drule_tac x = "Inter (Z) " in bspec, assumption) |
|
13134 | 334 |
apply blast |
13558 | 335 |
txt{*Now prove the linearity goal*} |
13134 | 336 |
apply (intro ballI) |
337 |
apply (case_tac "x=y") |
|
13269 | 338 |
apply blast |
13558 | 339 |
txt{*The @{term "x\<noteq>y"} case remains*} |
13134 | 340 |
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE], |
13269 | 341 |
assumption+, blast+) |
13134 | 342 |
done |
343 |
||
13558 | 344 |
text{** Defining the "next" operation for Zermelo's Theorem **} |
13134 | 345 |
|
346 |
lemma choice_Diff: |
|
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
347 |
"[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X" |
13134 | 348 |
apply (erule apply_type) |
349 |
apply (blast elim!: equalityE) |
|
350 |
done |
|
351 |
||
13558 | 352 |
text{*This justifies Definition 6.1*} |
13134 | 353 |
lemma Zermelo_next_exists: |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
354 |
"ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==> |
13558 | 355 |
\<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S). |
13175
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset
|
356 |
next`X = (if X=S then S else cons(ch`(S-X), X))" |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset
|
357 |
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)" |
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset
|
358 |
in bexI) |
13558 | 359 |
apply force |
13134 | 360 |
apply (unfold increasing_def) |
361 |
apply (rule CollectI) |
|
362 |
apply (rule lam_type) |
|
13558 | 363 |
txt{*Type checking is surprisingly hard!*} |
13134 | 364 |
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl) |
365 |
apply (blast intro!: choice_Diff [THEN DiffD1]) |
|
13558 | 366 |
txt{*Verify that it increases*} |
367 |
apply (intro allI impI) |
|
13134 | 368 |
apply (simp add: Pow_iff subset_consI subset_refl) |
369 |
done |
|
370 |
||
371 |
||
13558 | 372 |
text{*The construction of the injection*} |
13134 | 373 |
lemma choice_imp_injection: |
14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset
|
374 |
"[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X); |
13558 | 375 |
next \<in> increasing(S); |
376 |
\<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |] |
|
377 |
==> (\<lambda> x \<in> S. Union({y \<in> TFin(S,next). x \<notin> y})) |
|
378 |
\<in> inj(S, TFin(S,next) - {S})" |
|
13134 | 379 |
apply (rule_tac d = "%y. ch` (S-y) " in lam_injective) |
380 |
apply (rule DiffI) |
|
381 |
apply (rule Collect_subset [THEN TFin_UnionI]) |
|
382 |
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE) |
|
13558 | 383 |
apply (subgoal_tac "x \<notin> Union ({y \<in> TFin (S,next) . x \<notin> y}) ") |
13134 | 384 |
prefer 2 apply (blast elim: equalityE) |
13558 | 385 |
apply (subgoal_tac "Union ({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S") |
13134 | 386 |
prefer 2 apply (blast elim: equalityE) |
13558 | 387 |
txt{*For proving @{text "x \<in> next`Union(...)"}. |
388 |
Abrial and Laffitte's justification appears to be faulty.*} |
|
389 |
apply (subgoal_tac "~ next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) |
|
390 |
<= Union ({y \<in> TFin (S,next) . x \<notin> y}) ") |
|
391 |
prefer 2 |
|
392 |
apply (simp del: Union_iff |
|
393 |
add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] |
|
394 |
Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2]) |
|
395 |
apply (subgoal_tac "x \<in> next ` Union ({y \<in> TFin (S,next) . x \<notin> y}) ") |
|
396 |
prefer 2 |
|
397 |
apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI) |
|
398 |
txt{*End of the lemmas!*} |
|
13134 | 399 |
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]) |
400 |
done |
|
401 |
||
13558 | 402 |
text{*The wellordering theorem*} |
403 |
theorem AC_well_ord: "\<exists>r. well_ord(S,r)" |
|
13134 | 404 |
apply (rule AC_Pi_Pow [THEN exE]) |
13269 | 405 |
apply (rule Zermelo_next_exists [THEN bexE], assumption) |
13134 | 406 |
apply (rule exI) |
407 |
apply (rule well_ord_rvimage) |
|
408 |
apply (erule_tac [2] well_ord_TFin) |
|
13269 | 409 |
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+) |
13134 | 410 |
done |
13558 | 411 |
|
516 | 412 |
end |