author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46820  c656222c4dc1 
child 58871  c399ae4b836f 
permissions  rwrr 
1478  1 
(* Title: ZF/Zorn.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

516  3 
Copyright 1994 University of Cambridge 
4 
*) 

5 

13356  6 
header{*Zorn's Lemma*} 
7 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

8 
theory Zorn imports OrderArith AC Inductive_ZF begin 
516  9 

13356  10 
text{*Based upon the unpublished article ``Towards the Mechanization of the 
11 
Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*} 

12 

24893  13 
definition 
14 
Subset_rel :: "i=>i" where 

13558  15 
"Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}" 
13134  16 

24893  17 
definition 
18 
chain :: "i=>i" where 

13558  19 
"chain(A) == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y  Y<=X}" 
516  20 

24893  21 
definition 
22 
super :: "[i,i]=>i" where 

14653  23 
"super(A,c) == {d \<in> chain(A). c<=d & c\<noteq>d}" 
24 

24893  25 
definition 
26 
maxchain :: "i=>i" where 

13558  27 
"maxchain(A) == {c \<in> chain(A). super(A,c)=0}" 
28 

24893  29 
definition 
30 
increasing :: "i=>i" where 

46820  31 
"increasing(A) == {f \<in> Pow(A)>Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}" 
516  32 

13356  33 

13558  34 
text{*Lemma for the inductive definition below*} 
46820  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 sidecondition 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 

46820  48 
domains "TFin(S,next)" \<subseteq> "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 

46820  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 

46820  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: 
46820  66 
"[ c \<in> C; \<forall>x\<in>C. A<=x  x<=B ] ==> A \<subseteq> \<Inter>(C)  \<Inter>(C) \<subseteq> 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 

46820  77 
lemma increasingD2: "[ f \<in> increasing(A); x<=A ] ==> x \<subseteq> f`x" 
13269  78 
by (unfold increasing_def, blast) 
13134  79 

45602  80 
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI] 
13134  81 

45602  82 
lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD] 
13134  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); 

46820  89 
!!Y. [ Y \<subseteq> 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); 
46820  102 
\<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> 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) ] 
46820  114 
==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m  next`n \<subseteq> 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 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

121 
intro: increasing_trans subsetI, blast) 
13558  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) ] 
46820  139 
==> n=m  next`n \<subseteq> m" 
13558  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) ] 
46820  145 
==> n \<subseteq> m  m<=n" 
13558  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: 
46820  156 
"[ n \<in> TFin(S,next); m \<in> TFin(S,next); m = next`m ] ==> n \<subseteq> 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) ] 

46820  165 
==> m = next`m <> m = \<Union>(TFin(S,next))" 
13134  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 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

173 
intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+ 
13134  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 

46820  184 
lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)" 
13134  185 
apply (unfold chain_def) 
186 
apply (rule Collect_subset) 

187 
done 

188 

46820  189 
lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)" 
13134  190 
apply (unfold super_def) 
191 
apply (rule Collect_subset) 

192 
done 

193 

46820  194 
lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)" 
13134  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") 
46820  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]) 

46820  261 
apply (rule_tac x = "\<Union>(TFin (S,next))" in exI) 
13134  262 
apply (rule classical) 
46820  263 
apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))") 
13134  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 

46820  283 
lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z" 
13134  284 
apply (rule Hausdorff [THEN exE]) 
285 
apply (simp add: maxchain_def) 

286 
apply (rename_tac c) 

46820  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 

27704  299 
text {* Alternative version of Zorn's Lemma *} 
300 

301 
theorem Zorn2: 

46820  302 
"\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z" 
27704  303 
apply (cut_tac Hausdorff maxchain_subset_chain) 
304 
apply (erule exE) 

305 
apply (drule subsetD, assumption) 

306 
apply (drule bspec, assumption, erule bexE) 

307 
apply (rule_tac x = y in bexI) 

308 
prefer 2 apply assumption 

309 
apply clarify 

310 
apply rule apply assumption 

311 
apply rule 

312 
apply (rule ccontr) 

313 
apply (frule_tac z=z in chain_extend) 

314 
apply (assumption, blast) 

315 
apply (unfold maxchain_def super_def) 

316 
apply (blast elim!: equalityCE) 

317 
done 

318 

13134  319 

13356  320 
subsection{*Zermelo's Theorem: Every Set can be WellOrdered*} 
13134  321 

13558  322 
text{*Lemma 5*} 
13134  323 
lemma TFin_well_lemma5: 
46820  324 
"[ n \<in> TFin(S,next); Z \<subseteq> TFin(S,next); z:Z; ~ \<Inter>(Z) \<in> Z ] 
325 
==> \<forall>m \<in> Z. n \<subseteq> m" 

13134  326 
apply (erule TFin_induct) 
13558  327 
prefer 2 apply blast txt{*second induction step is easy*} 
13134  328 
apply (rule ballI) 
13558  329 
apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) 
46820  330 
apply (subgoal_tac "m = \<Inter>(Z) ") 
13134  331 
apply blast+ 
332 
done 

333 

13558  334 
text{*Wellordering of @{term "TFin(S,next)"} *} 
46820  335 
lemma well_ord_TFin_lemma: "[ Z \<subseteq> TFin(S,next); z \<in> Z ] ==> \<Inter>(Z) \<in> Z" 
13134  336 
apply (rule classical) 
46820  337 
apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}") 
13134  338 
apply (simp (no_asm_simp) add: Inter_singleton) 
339 
apply (erule equal_singleton) 

340 
apply (rule Union_upper [THEN equalityI]) 

13269  341 
apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+) 
13134  342 
done 
343 

13558  344 
text{*This theorem just packages the previous result*} 
13134  345 
lemma well_ord_TFin: 
13558  346 
"next \<in> increasing(S) 
347 
==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))" 

13134  348 
apply (rule well_ordI) 
349 
apply (unfold Subset_rel_def linear_def) 

13558  350 
txt{*Prove the wellfoundedness goal*} 
13134  351 
apply (rule wf_onI) 
13269  352 
apply (frule well_ord_TFin_lemma, assumption) 
46820  353 
apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption) 
13134  354 
apply blast 
13558  355 
txt{*Now prove the linearity goal*} 
13134  356 
apply (intro ballI) 
357 
apply (case_tac "x=y") 

13269  358 
apply blast 
13558  359 
txt{*The @{term "x\<noteq>y"} case remains*} 
13134  360 
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE], 
13269  361 
assumption+, blast+) 
13134  362 
done 
363 

13558  364 
text{** Defining the "next" operation for Zermelo's Theorem **} 
13134  365 

366 
lemma choice_Diff: 

14171
0cab06e3bbd0
Extended the notion of letter and digit, such that now one may use greek,
skalberg
parents:
13784
diff
changeset

367 
"[ ch \<in> (\<Pi> X \<in> Pow(S)  {0}. X); X \<subseteq> S; X\<noteq>S ] ==> ch ` (SX) \<in> SX" 
13134  368 
apply (erule apply_type) 
369 
apply (blast elim!: equalityE) 

370 
done 

371 

13558  372 
text{*This justifies Definition 6.1*} 
13134  373 
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

374 
"ch \<in> (\<Pi> X \<in> Pow(S){0}. X) ==> 
13558  375 
\<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

376 
next`X = (if X=S then S else cons(ch`(SX), X))" 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset

377 
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(SX), X)" 
81082cfa5618
new definition of "apply" and new simprule "beta_if"
paulson
parents:
13134
diff
changeset

378 
in bexI) 
13558  379 
apply force 
13134  380 
apply (unfold increasing_def) 
381 
apply (rule CollectI) 

382 
apply (rule lam_type) 

13558  383 
txt{*Type checking is surprisingly hard!*} 
13134  384 
apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl) 
385 
apply (blast intro!: choice_Diff [THEN DiffD1]) 

13558  386 
txt{*Verify that it increases*} 
387 
apply (intro allI impI) 

13134  388 
apply (simp add: Pow_iff subset_consI subset_refl) 
389 
done 

390 

391 

13558  392 
text{*The construction of the injection*} 
13134  393 
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

394 
"[ ch \<in> (\<Pi> X \<in> Pow(S){0}. X); 
13558  395 
next \<in> increasing(S); 
396 
\<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(SX), X)) ] 

46820  397 
==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y})) 
13558  398 
\<in> inj(S, TFin(S,next)  {S})" 
13134  399 
apply (rule_tac d = "%y. ch` (Sy) " in lam_injective) 
400 
apply (rule DiffI) 

401 
apply (rule Collect_subset [THEN TFin_UnionI]) 

402 
apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE) 

46820  403 
apply (subgoal_tac "x \<notin> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ") 
13134  404 
prefer 2 apply (blast elim: equalityE) 
46820  405 
apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S") 
13134  406 
prefer 2 apply (blast elim: equalityE) 
46820  407 
txt{*For proving @{text "x \<in> next`\<Union>(...)"}. 
13558  408 
Abrial and Laffitte's justification appears to be faulty.*} 
46820  409 
apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y}) 
410 
\<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ") 

13558  411 
prefer 2 
412 
apply (simp del: Union_iff 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

413 
add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

414 
Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2]) 
46820  415 
apply (subgoal_tac "x \<in> next ` Union({y \<in> TFin (S,next) . x \<notin> y}) ") 
13558  416 
prefer 2 
417 
apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI) 

418 
txt{*End of the lemmas!*} 

13134  419 
apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]) 
420 
done 

421 

13558  422 
text{*The wellordering theorem*} 
423 
theorem AC_well_ord: "\<exists>r. well_ord(S,r)" 

13134  424 
apply (rule AC_Pi_Pow [THEN exE]) 
13269  425 
apply (rule Zermelo_next_exists [THEN bexE], assumption) 
13134  426 
apply (rule exI) 
427 
apply (rule well_ord_rvimage) 

428 
apply (erule_tac [2] well_ord_TFin) 

13269  429 
apply (rule choice_imp_injection [THEN inj_weaken_type], blast+) 
13134  430 
done 
13558  431 

27704  432 

433 
subsection {* Zorn's Lemma for Partial Orders *} 

434 

435 
text {* Reimported from HOL by Clemens Ballarin. *} 

436 

437 

438 
definition Chain :: "i => i" where 

46820  439 
"Chain(r) = {A \<in> Pow(field(r)). \<forall>a\<in>A. \<forall>b\<in>A. <a, b> \<in> r  <b, a> \<in> r}" 
27704  440 

441 
lemma mono_Chain: 

442 
"r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)" 

443 
unfolding Chain_def 

444 
by blast 

445 

446 
theorem Zorn_po: 

447 
assumes po: "Partial_order(r)" 

46820  448 
and u: "\<forall>C\<in>Chain(r). \<exists>u\<in>field(r). \<forall>a\<in>C. <a, u> \<in> r" 
449 
shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m" 

27704  450 
proof  
451 
have "Preorder(r)" using po by (simp add: partial_order_on_def) 

452 
{* Mirror r in the set of subsets below (wrt r) elements of A (?). *} 

46820  453 
let ?B = "\<lambda>x\<in>field(r). r `` {x}" let ?S = "?B `` field(r)" 
454 
have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U" 

27704  455 
proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp) 
456 
fix C 

46820  457 
assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B  B \<subseteq> A" 
458 
let ?A = "{x \<in> field(r). \<exists>M\<in>C. M = ?B`x}" 

27704  459 
have "C = ?B `` ?A" using 1 
460 
apply (auto simp: image_def) 

461 
apply rule 

462 
apply rule 

463 
apply (drule subsetD) apply assumption 

464 
apply (erule CollectE) 

465 
apply rule apply assumption 

466 
apply (erule bexE) 

467 
apply rule prefer 2 apply assumption 

468 
apply rule 

469 
apply (erule lamE) apply simp 

470 
apply assumption 

471 

472 
apply (thin_tac "C \<subseteq> ?X") 

473 
apply (fast elim: lamE) 

474 
done 

46820  475 
have "?A \<in> Chain(r)" 
27704  476 
proof (simp add: Chain_def subsetI, intro conjI ballI impI) 
477 
fix a b 

46820  478 
assume "a \<in> field(r)" "r `` {a} \<in> C" "b \<in> field(r)" "r `` {b} \<in> C" 
27704  479 
hence "r `` {a} \<subseteq> r `` {b}  r `` {b} \<subseteq> r `` {a}" using 2 by auto 
46820  480 
then show "<a, b> \<in> r  <b, a> \<in> r" 
481 
using `Preorder(r)` `a \<in> field(r)` `b \<in> field(r)` 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

482 
by (simp add: subset_vimage1_vimage1_iff) 
27704  483 
qed 
46820  484 
then obtain u where uA: "u \<in> field(r)" "\<forall>a\<in>?A. <a, u> \<in> r" 
27704  485 
using u 
486 
apply auto 

487 
apply (drule bspec) apply assumption 

488 
apply auto 

489 
done 

46820  490 
have "\<forall>A\<in>C. A \<subseteq> r `` {u}" 
27704  491 
proof (auto intro!: vimageI) 
492 
fix a B 

46820  493 
assume aB: "B \<in> C" "a \<in> B" 
494 
with 1 obtain x where "x \<in> field(r)" "B = r `` {x}" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

495 
apply  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

496 
apply (drule subsetD) apply assumption 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

497 
apply (erule imageE) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

498 
apply (erule lamE) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

499 
apply simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

500 
done 
46820  501 
then show "<a, u> \<in> r" using uA aB `Preorder(r)` 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
27704
diff
changeset

502 
by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+ 
27704  503 
qed 
46820  504 
then show "\<exists>U\<in>field(r). \<forall>A\<in>C. A \<subseteq> r `` {U}" 
505 
using `u \<in> field(r)` .. 

27704  506 
qed 
507 
from Zorn2 [OF this] 

46820  508 
obtain m B where "m \<in> field(r)" "B = r `` {m}" 
509 
"\<forall>x\<in>field(r). B \<subseteq> r `` {x} \<longrightarrow> B = r `` {x}" 

27704  510 
by (auto elim!: lamE simp: ball_image_simp) 
46820  511 
then have "\<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m" 
512 
using po `Preorder(r)` `m \<in> field(r)` 

27704  513 
by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff) 
46820  514 
then show ?thesis using `m \<in> field(r)` by blast 
27704  515 
qed 
516 

516  517 
end 