author | wenzelm |
Tue, 18 Feb 2014 18:29:02 +0100 | |
changeset 55553 | 99409ccbe04a |
parent 55018 | 2a526bd279ed |
child 55811 | aa1acc25126b |
permissions | -rw-r--r-- |
55018
2a526bd279ed
moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents:
54552
diff
changeset
|
1 |
(* Title: HOL/Zorn.thy |
52181 | 2 |
Author: Jacques D. Fleuriot |
3 |
Author: Tobias Nipkow, TUM |
|
4 |
Author: Christian Sternagel, JAIST |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30663
diff
changeset
|
5 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30663
diff
changeset
|
6 |
Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF). |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30663
diff
changeset
|
7 |
The well-ordering theorem. |
14706 | 8 |
*) |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
9 |
|
14706 | 10 |
header {* Zorn's Lemma *} |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
11 |
|
15131 | 12 |
theory Zorn |
55018
2a526bd279ed
moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents:
54552
diff
changeset
|
13 |
imports Order_Relation Hilbert_Choice |
15131 | 14 |
begin |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
15 |
|
52181 | 16 |
subsection {* Zorn's Lemma for the Subset Relation *} |
17 |
||
18 |
subsubsection {* Results that do not require an order *} |
|
19 |
||
20 |
text {*Let @{text P} be a binary predicate on the set @{text A}.*} |
|
21 |
locale pred_on = |
|
22 |
fixes A :: "'a set" |
|
23 |
and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) |
|
24 |
begin |
|
25 |
||
26 |
abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) where |
|
27 |
"x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y" |
|
28 |
||
29 |
text {*A chain is a totally ordered subset of @{term A}.*} |
|
30 |
definition chain :: "'a set \<Rightarrow> bool" where |
|
31 |
"chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)" |
|
32 |
||
33 |
text {*We call a chain that is a proper superset of some set @{term X}, |
|
34 |
but not necessarily a chain itself, a superchain of @{term X}.*} |
|
35 |
abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50) where |
|
36 |
"X <c C \<equiv> chain C \<and> X \<subset> C" |
|
37 |
||
38 |
text {*A maximal chain is a chain that does not have a superchain.*} |
|
39 |
definition maxchain :: "'a set \<Rightarrow> bool" where |
|
40 |
"maxchain C \<longleftrightarrow> chain C \<and> \<not> (\<exists>S. C <c S)" |
|
41 |
||
42 |
text {*We define the successor of a set to be an arbitrary |
|
43 |
superchain, if such exists, or the set itself, otherwise.*} |
|
44 |
definition suc :: "'a set \<Rightarrow> 'a set" where |
|
45 |
"suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))" |
|
46 |
||
47 |
lemma chainI [Pure.intro?]: |
|
48 |
"\<lbrakk>C \<subseteq> A; \<And>x y. \<lbrakk>x \<in> C; y \<in> C\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> chain C" |
|
49 |
unfolding chain_def by blast |
|
50 |
||
51 |
lemma chain_total: |
|
52 |
"chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
53 |
by (simp add: chain_def) |
|
54 |
||
55 |
lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X" |
|
56 |
by (simp add: suc_def) |
|
57 |
||
58 |
lemma maxchain_suc [simp]: "maxchain X \<Longrightarrow> suc X = X" |
|
59 |
by (simp add: suc_def) |
|
60 |
||
61 |
lemma suc_subset: "X \<subseteq> suc X" |
|
62 |
by (auto simp: suc_def maxchain_def intro: someI2) |
|
63 |
||
64 |
lemma chain_empty [simp]: "chain {}" |
|
65 |
by (auto simp: chain_def) |
|
66 |
||
67 |
lemma not_maxchain_Some: |
|
68 |
"chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)" |
|
69 |
by (rule someI_ex) (auto simp: maxchain_def) |
|
70 |
||
71 |
lemma suc_not_equals: |
|
72 |
"chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C" |
|
54482 | 73 |
by (auto simp: suc_def) (metis (no_types) less_irrefl not_maxchain_Some) |
52181 | 74 |
|
75 |
lemma subset_suc: |
|
76 |
assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y" |
|
77 |
using assms by (rule subset_trans) (rule suc_subset) |
|
78 |
||
79 |
text {*We build a set @{term \<C>} that is closed under applications |
|
80 |
of @{term suc} and contains the union of all its subsets.*} |
|
81 |
inductive_set suc_Union_closed ("\<C>") where |
|
82 |
suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>" | |
|
83 |
Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>" |
|
84 |
||
85 |
text {*Since the empty set as well as the set itself is a subset of |
|
86 |
every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and |
|
87 |
@{term "\<Union>\<C> \<in> \<C>"}.*} |
|
88 |
lemma |
|
89 |
suc_Union_closed_empty: "{} \<in> \<C>" and |
|
90 |
suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>" |
|
91 |
using Union [of "{}"] and Union [of "\<C>"] by simp+ |
|
92 |
text {*Thus closure under @{term suc} will hit a maximal chain |
|
93 |
eventually, as is shown below.*} |
|
94 |
||
95 |
lemma suc_Union_closed_induct [consumes 1, case_names suc Union, |
|
96 |
induct pred: suc_Union_closed]: |
|
97 |
assumes "X \<in> \<C>" |
|
98 |
and "\<And>X. \<lbrakk>X \<in> \<C>; Q X\<rbrakk> \<Longrightarrow> Q (suc X)" |
|
99 |
and "\<And>X. \<lbrakk>X \<subseteq> \<C>; \<forall>x\<in>X. Q x\<rbrakk> \<Longrightarrow> Q (\<Union>X)" |
|
100 |
shows "Q X" |
|
101 |
using assms by (induct) blast+ |
|
26272 | 102 |
|
52181 | 103 |
lemma suc_Union_closed_cases [consumes 1, case_names suc Union, |
104 |
cases pred: suc_Union_closed]: |
|
105 |
assumes "X \<in> \<C>" |
|
106 |
and "\<And>Y. \<lbrakk>X = suc Y; Y \<in> \<C>\<rbrakk> \<Longrightarrow> Q" |
|
107 |
and "\<And>Y. \<lbrakk>X = \<Union>Y; Y \<subseteq> \<C>\<rbrakk> \<Longrightarrow> Q" |
|
108 |
shows "Q" |
|
109 |
using assms by (cases) simp+ |
|
110 |
||
111 |
text {*On chains, @{term suc} yields a chain.*} |
|
112 |
lemma chain_suc: |
|
113 |
assumes "chain X" shows "chain (suc X)" |
|
114 |
using assms |
|
115 |
by (cases "\<not> chain X \<or> maxchain X") |
|
116 |
(force simp: suc_def dest: not_maxchain_Some)+ |
|
117 |
||
118 |
lemma chain_sucD: |
|
119 |
assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)" |
|
120 |
proof - |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
121 |
from `chain X` have *: "chain (suc X)" by (rule chain_suc) |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
122 |
then have "suc X \<subseteq> A" unfolding chain_def by blast |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
123 |
with * show ?thesis by blast |
52181 | 124 |
qed |
125 |
||
126 |
lemma suc_Union_closed_total': |
|
127 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" |
|
128 |
and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y" |
|
129 |
shows "X \<subseteq> Y \<or> suc Y \<subseteq> X" |
|
130 |
using `X \<in> \<C>` |
|
131 |
proof (induct) |
|
132 |
case (suc X) |
|
133 |
with * show ?case by (blast del: subsetI intro: subset_suc) |
|
134 |
qed blast |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
135 |
|
52181 | 136 |
lemma suc_Union_closed_subsetD: |
137 |
assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>" |
|
138 |
shows "X = Y \<or> suc Y \<subseteq> X" |
|
139 |
using assms(2-, 1) |
|
140 |
proof (induct arbitrary: Y) |
|
141 |
case (suc X) |
|
142 |
note * = `\<And>Y. \<lbrakk>Y \<in> \<C>; Y \<subseteq> X\<rbrakk> \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X` |
|
143 |
with suc_Union_closed_total' [OF `Y \<in> \<C>` `X \<in> \<C>`] |
|
144 |
have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast |
|
145 |
then show ?case |
|
146 |
proof |
|
147 |
assume "Y \<subseteq> X" |
|
148 |
with * and `Y \<in> \<C>` have "X = Y \<or> suc Y \<subseteq> X" by blast |
|
149 |
then show ?thesis |
|
150 |
proof |
|
151 |
assume "X = Y" then show ?thesis by simp |
|
152 |
next |
|
153 |
assume "suc Y \<subseteq> X" |
|
154 |
then have "suc Y \<subseteq> suc X" by (rule subset_suc) |
|
155 |
then show ?thesis by simp |
|
156 |
qed |
|
157 |
next |
|
158 |
assume "suc X \<subseteq> Y" |
|
159 |
with `Y \<subseteq> suc X` show ?thesis by blast |
|
160 |
qed |
|
161 |
next |
|
162 |
case (Union X) |
|
163 |
show ?case |
|
164 |
proof (rule ccontr) |
|
165 |
assume "\<not> ?thesis" |
|
166 |
with `Y \<subseteq> \<Union>X` obtain x y z |
|
167 |
where "\<not> suc Y \<subseteq> \<Union>X" |
|
168 |
and "x \<in> X" and "y \<in> x" and "y \<notin> Y" |
|
169 |
and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast |
|
170 |
with `X \<subseteq> \<C>` have "x \<in> \<C>" by blast |
|
171 |
from Union and `x \<in> X` |
|
172 |
have *: "\<And>y. \<lbrakk>y \<in> \<C>; y \<subseteq> x\<rbrakk> \<Longrightarrow> x = y \<or> suc y \<subseteq> x" by blast |
|
173 |
with suc_Union_closed_total' [OF `Y \<in> \<C>` `x \<in> \<C>`] |
|
174 |
have "Y \<subseteq> x \<or> suc x \<subseteq> Y" by blast |
|
175 |
then show False |
|
176 |
proof |
|
177 |
assume "Y \<subseteq> x" |
|
178 |
with * [OF `Y \<in> \<C>`] have "x = Y \<or> suc Y \<subseteq> x" by blast |
|
179 |
then show False |
|
180 |
proof |
|
181 |
assume "x = Y" with `y \<in> x` and `y \<notin> Y` show False by blast |
|
182 |
next |
|
183 |
assume "suc Y \<subseteq> x" |
|
184 |
with `x \<in> X` have "suc Y \<subseteq> \<Union>X" by blast |
|
185 |
with `\<not> suc Y \<subseteq> \<Union>X` show False by contradiction |
|
186 |
qed |
|
187 |
next |
|
188 |
assume "suc x \<subseteq> Y" |
|
189 |
moreover from suc_subset and `y \<in> x` have "y \<in> suc x" by blast |
|
190 |
ultimately show False using `y \<notin> Y` by blast |
|
191 |
qed |
|
192 |
qed |
|
193 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
194 |
|
52181 | 195 |
text {*The elements of @{term \<C>} are totally ordered by the subset relation.*} |
196 |
lemma suc_Union_closed_total: |
|
197 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" |
|
198 |
shows "X \<subseteq> Y \<or> Y \<subseteq> X" |
|
199 |
proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y") |
|
200 |
case True |
|
201 |
with suc_Union_closed_total' [OF assms] |
|
202 |
have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast |
|
203 |
then show ?thesis using suc_subset [of Y] by blast |
|
204 |
next |
|
205 |
case False |
|
206 |
then obtain Z |
|
207 |
where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y" by blast |
|
208 |
with suc_Union_closed_subsetD and `Y \<in> \<C>` show ?thesis by blast |
|
209 |
qed |
|
210 |
||
211 |
text {*Once we hit a fixed point w.r.t. @{term suc}, all other elements |
|
212 |
of @{term \<C>} are subsets of this fixed point.*} |
|
213 |
lemma suc_Union_closed_suc: |
|
214 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y" |
|
215 |
shows "X \<subseteq> Y" |
|
216 |
using `X \<in> \<C>` |
|
217 |
proof (induct) |
|
218 |
case (suc X) |
|
219 |
with `Y \<in> \<C>` and suc_Union_closed_subsetD |
|
220 |
have "X = Y \<or> suc X \<subseteq> Y" by blast |
|
221 |
then show ?case by (auto simp: `suc Y = Y`) |
|
222 |
qed blast |
|
223 |
||
224 |
lemma eq_suc_Union: |
|
225 |
assumes "X \<in> \<C>" |
|
226 |
shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>" |
|
227 |
proof |
|
228 |
assume "suc X = X" |
|
229 |
with suc_Union_closed_suc [OF suc_Union_closed_Union `X \<in> \<C>`] |
|
230 |
have "\<Union>\<C> \<subseteq> X" . |
|
231 |
with `X \<in> \<C>` show "X = \<Union>\<C>" by blast |
|
232 |
next |
|
233 |
from `X \<in> \<C>` have "suc X \<in> \<C>" by (rule suc) |
|
234 |
then have "suc X \<subseteq> \<Union>\<C>" by blast |
|
235 |
moreover assume "X = \<Union>\<C>" |
|
236 |
ultimately have "suc X \<subseteq> X" by simp |
|
237 |
moreover have "X \<subseteq> suc X" by (rule suc_subset) |
|
238 |
ultimately show "suc X = X" .. |
|
239 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
240 |
|
52181 | 241 |
lemma suc_in_carrier: |
242 |
assumes "X \<subseteq> A" |
|
243 |
shows "suc X \<subseteq> A" |
|
244 |
using assms |
|
245 |
by (cases "\<not> chain X \<or> maxchain X") |
|
246 |
(auto dest: chain_sucD) |
|
247 |
||
248 |
lemma suc_Union_closed_in_carrier: |
|
249 |
assumes "X \<in> \<C>" |
|
250 |
shows "X \<subseteq> A" |
|
251 |
using assms |
|
252 |
by (induct) (auto dest: suc_in_carrier) |
|
253 |
||
254 |
text {*All elements of @{term \<C>} are chains.*} |
|
255 |
lemma suc_Union_closed_chain: |
|
256 |
assumes "X \<in> \<C>" |
|
257 |
shows "chain X" |
|
258 |
using assms |
|
259 |
proof (induct) |
|
54482 | 260 |
case (suc X) then show ?case by (simp add: suc_def) (metis (no_types) not_maxchain_Some) |
52181 | 261 |
next |
262 |
case (Union X) |
|
263 |
then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier) |
|
264 |
moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
265 |
proof (intro ballI) |
|
266 |
fix x y |
|
267 |
assume "x \<in> \<Union>X" and "y \<in> \<Union>X" |
|
268 |
then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X" by blast |
|
269 |
with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v" by blast+ |
|
270 |
with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u" by blast |
|
271 |
then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
272 |
proof |
|
273 |
assume "u \<subseteq> v" |
|
274 |
from `chain v` show ?thesis |
|
275 |
proof (rule chain_total) |
|
276 |
show "y \<in> v" by fact |
|
277 |
show "x \<in> v" using `u \<subseteq> v` and `x \<in> u` by blast |
|
278 |
qed |
|
279 |
next |
|
280 |
assume "v \<subseteq> u" |
|
281 |
from `chain u` show ?thesis |
|
282 |
proof (rule chain_total) |
|
283 |
show "x \<in> u" by fact |
|
284 |
show "y \<in> u" using `v \<subseteq> u` and `y \<in> v` by blast |
|
285 |
qed |
|
286 |
qed |
|
287 |
qed |
|
288 |
ultimately show ?case unfolding chain_def .. |
|
289 |
qed |
|
290 |
||
291 |
subsubsection {* Hausdorff's Maximum Principle *} |
|
292 |
||
293 |
text {*There exists a maximal totally ordered subset of @{term A}. (Note that we do not |
|
294 |
require @{term A} to be partially ordered.)*} |
|
46980 | 295 |
|
52181 | 296 |
theorem Hausdorff: "\<exists>C. maxchain C" |
297 |
proof - |
|
298 |
let ?M = "\<Union>\<C>" |
|
299 |
have "maxchain ?M" |
|
300 |
proof (rule ccontr) |
|
301 |
assume "\<not> maxchain ?M" |
|
302 |
then have "suc ?M \<noteq> ?M" |
|
303 |
using suc_not_equals and |
|
304 |
suc_Union_closed_chain [OF suc_Union_closed_Union] by simp |
|
305 |
moreover have "suc ?M = ?M" |
|
306 |
using eq_suc_Union [OF suc_Union_closed_Union] by simp |
|
307 |
ultimately show False by contradiction |
|
308 |
qed |
|
309 |
then show ?thesis by blast |
|
310 |
qed |
|
311 |
||
312 |
text {*Make notation @{term \<C>} available again.*} |
|
313 |
no_notation suc_Union_closed ("\<C>") |
|
314 |
||
315 |
lemma chain_extend: |
|
316 |
"chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)" |
|
317 |
unfolding chain_def by blast |
|
318 |
||
319 |
lemma maxchain_imp_chain: |
|
320 |
"maxchain C \<Longrightarrow> chain C" |
|
321 |
by (simp add: maxchain_def) |
|
322 |
||
323 |
end |
|
324 |
||
325 |
text {*Hide constant @{const pred_on.suc_Union_closed}, which was just needed |
|
326 |
for the proof of Hausforff's maximum principle.*} |
|
327 |
hide_const pred_on.suc_Union_closed |
|
328 |
||
329 |
lemma chain_mono: |
|
330 |
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y" |
|
331 |
and "pred_on.chain A P C" |
|
332 |
shows "pred_on.chain A Q C" |
|
333 |
using assms unfolding pred_on.chain_def by blast |
|
334 |
||
335 |
subsubsection {* Results for the proper subset relation *} |
|
336 |
||
337 |
interpretation subset: pred_on "A" "op \<subset>" for A . |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
338 |
|
52181 | 339 |
lemma subset_maxchain_max: |
340 |
assumes "subset.maxchain A C" and "X \<in> A" and "\<Union>C \<subseteq> X" |
|
341 |
shows "\<Union>C = X" |
|
342 |
proof (rule ccontr) |
|
343 |
let ?C = "{X} \<union> C" |
|
344 |
from `subset.maxchain A C` have "subset.chain A C" |
|
345 |
and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S" |
|
346 |
by (auto simp: subset.maxchain_def) |
|
347 |
moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto |
|
348 |
ultimately have "subset.chain A ?C" |
|
349 |
using subset.chain_extend [of A C X] and `X \<in> A` by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
350 |
moreover assume **: "\<Union>C \<noteq> X" |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
351 |
moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto |
52181 | 352 |
ultimately show False using * by blast |
353 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
354 |
|
52181 | 355 |
subsubsection {* Zorn's lemma *} |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
356 |
|
52181 | 357 |
text {*If every chain has an upper bound, then there is a maximal set.*} |
358 |
lemma subset_Zorn: |
|
359 |
assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U" |
|
360 |
shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
361 |
proof - |
|
362 |
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. |
|
363 |
then have "subset.chain A M" by (rule subset.maxchain_imp_chain) |
|
364 |
with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y" by blast |
|
365 |
moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X" |
|
366 |
proof (intro ballI impI) |
|
367 |
fix X |
|
368 |
assume "X \<in> A" and "Y \<subseteq> X" |
|
369 |
show "Y = X" |
|
370 |
proof (rule ccontr) |
|
371 |
assume "Y \<noteq> X" |
|
372 |
with `Y \<subseteq> X` have "\<not> X \<subseteq> Y" by blast |
|
373 |
from subset.chain_extend [OF `subset.chain A M` `X \<in> A`] and `\<forall>X\<in>M. X \<subseteq> Y` |
|
374 |
have "subset.chain A ({X} \<union> M)" using `Y \<subseteq> X` by auto |
|
375 |
moreover have "M \<subset> {X} \<union> M" using `\<forall>X\<in>M. X \<subseteq> Y` and `\<not> X \<subseteq> Y` by auto |
|
376 |
ultimately show False |
|
377 |
using `subset.maxchain A M` by (auto simp: subset.maxchain_def) |
|
378 |
qed |
|
379 |
qed |
|
54482 | 380 |
ultimately show ?thesis by metis |
52181 | 381 |
qed |
382 |
||
383 |
text{*Alternative version of Zorn's lemma for the subset relation.*} |
|
384 |
lemma subset_Zorn': |
|
385 |
assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A" |
|
386 |
shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
387 |
proof - |
|
388 |
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. |
|
389 |
then have "subset.chain A M" by (rule subset.maxchain_imp_chain) |
|
390 |
with assms have "\<Union>M \<in> A" . |
|
391 |
moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z" |
|
392 |
proof (intro ballI impI) |
|
393 |
fix Z |
|
394 |
assume "Z \<in> A" and "\<Union>M \<subseteq> Z" |
|
395 |
with subset_maxchain_max [OF `subset.maxchain A M`] |
|
396 |
show "\<Union>M = Z" . |
|
397 |
qed |
|
398 |
ultimately show ?thesis by blast |
|
399 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
400 |
|
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
401 |
|
52181 | 402 |
subsection {* Zorn's Lemma for Partial Orders *} |
403 |
||
404 |
text {*Relate old to new definitions.*} |
|
17200 | 405 |
|
52181 | 406 |
(* Define globally? In Set.thy? *) |
407 |
definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") where |
|
408 |
"chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)" |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
409 |
|
52181 | 410 |
definition chains :: "'a set set \<Rightarrow> 'a set set set" where |
411 |
"chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}" |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
412 |
|
52181 | 413 |
(* Define globally? In Relation.thy? *) |
414 |
definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where |
|
415 |
"Chains r = {C. \<forall>a\<in>C. \<forall>b\<in>C. (a, b) \<in> r \<or> (b, a) \<in> r}" |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
416 |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
417 |
lemma chains_extend: |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
418 |
"[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S" |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
419 |
by (unfold chains_def chain_subset_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
420 |
|
52181 | 421 |
lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s" |
422 |
unfolding Chains_def by blast |
|
423 |
||
424 |
lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C" |
|
54482 | 425 |
unfolding chain_subset_def subset.chain_def by fast |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
426 |
|
52181 | 427 |
lemma chains_alt_def: "chains A = {C. subset.chain A C}" |
428 |
by (simp add: chains_def chain_subset_alt_def subset.chain_def) |
|
429 |
||
430 |
lemma Chains_subset: |
|
431 |
"Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
432 |
by (force simp add: Chains_def pred_on.chain_def) |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
433 |
|
52181 | 434 |
lemma Chains_subset': |
435 |
assumes "refl r" |
|
436 |
shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r" |
|
437 |
using assms |
|
438 |
by (auto simp add: Chains_def pred_on.chain_def refl_on_def) |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
439 |
|
52181 | 440 |
lemma Chains_alt_def: |
441 |
assumes "refl r" |
|
442 |
shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
443 |
using assms |
|
444 |
by (metis Chains_subset Chains_subset' subset_antisym) |
|
445 |
||
446 |
lemma Zorn_Lemma: |
|
447 |
"\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
448 |
using subset_Zorn' [of A] by (force simp: chains_alt_def) |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
449 |
|
52181 | 450 |
lemma Zorn_Lemma2: |
451 |
"\<forall>C\<in>chains A. \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
452 |
using subset_Zorn [of A] by (auto simp: chains_alt_def) |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
453 |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
454 |
text{*Various other lemmas*} |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
455 |
|
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
456 |
lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x" |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
457 |
by (unfold chains_def chain_subset_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
458 |
|
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
459 |
lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S" |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
460 |
by (unfold chains_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
461 |
|
52181 | 462 |
lemma Zorns_po_lemma: |
463 |
assumes po: "Partial_order r" |
|
464 |
and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r" |
|
465 |
shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
466 |
proof - |
|
467 |
have "Preorder r" using po by (simp add: partial_order_on_def) |
|
468 |
--{* Mirror r in the set of subsets below (wrt r) elements of A*} |
|
469 |
let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r" |
|
470 |
{ |
|
471 |
fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" |
|
472 |
let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}" |
|
473 |
have "C = ?B ` ?A" using 1 by (auto simp: image_def) |
|
474 |
have "?A \<in> Chains r" |
|
475 |
proof (simp add: Chains_def, intro allI impI, elim conjE) |
|
476 |
fix a b |
|
477 |
assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C" |
|
478 |
hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto |
|
479 |
thus "(a, b) \<in> r \<or> (b, a) \<in> r" |
|
480 |
using `Preorder r` and `a \<in> Field r` and `b \<in> Field r` |
|
481 |
by (simp add:subset_Image1_Image1_iff) |
|
482 |
qed |
|
483 |
then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto |
|
484 |
have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u") |
|
485 |
proof auto |
|
486 |
fix a B assume aB: "B \<in> C" "a \<in> B" |
|
487 |
with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto |
|
488 |
thus "(a, u) \<in> r" using uA and aB and `Preorder r` |
|
54482 | 489 |
unfolding preorder_on_def refl_on_def by simp (fast dest: transD) |
52181 | 490 |
qed |
491 |
then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast |
|
492 |
} |
|
493 |
then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U" |
|
494 |
by (auto simp: chains_def chain_subset_def) |
|
495 |
from Zorn_Lemma2 [OF this] |
|
496 |
obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}" |
|
497 |
and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B" |
|
498 |
by auto |
|
499 |
hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
500 |
using po and `Preorder r` and `m \<in> Field r` |
|
501 |
by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) |
|
502 |
thus ?thesis using `m \<in> Field r` by blast |
|
503 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
504 |
|
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
505 |
|
52181 | 506 |
subsection {* The Well Ordering Theorem *} |
26191 | 507 |
|
508 |
(* The initial segment of a relation appears generally useful. |
|
509 |
Move to Relation.thy? |
|
510 |
Definition correct/most general? |
|
511 |
Naming? |
|
512 |
*) |
|
52181 | 513 |
definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where |
514 |
"init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}" |
|
26191 | 515 |
|
52181 | 516 |
abbreviation |
517 |
initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55) |
|
518 |
where |
|
519 |
"r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of" |
|
26191 | 520 |
|
52181 | 521 |
lemma refl_on_init_seg_of [simp]: "r initial_segment_of r" |
522 |
by (simp add: init_seg_of_def) |
|
26191 | 523 |
|
524 |
lemma trans_init_seg_of: |
|
525 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t" |
|
54482 | 526 |
by (simp (no_asm_use) add: init_seg_of_def) blast |
26191 | 527 |
|
528 |
lemma antisym_init_seg_of: |
|
52181 | 529 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s" |
530 |
unfolding init_seg_of_def by safe |
|
26191 | 531 |
|
52181 | 532 |
lemma Chains_init_seg_of_Union: |
533 |
"R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R" |
|
534 |
by (auto simp: init_seg_of_def Ball_def Chains_def) blast |
|
26191 | 535 |
|
26272 | 536 |
lemma chain_subset_trans_Union: |
52181 | 537 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)" |
538 |
apply (auto simp add: chain_subset_def) |
|
539 |
apply (simp (no_asm_use) add: trans_def) |
|
54482 | 540 |
by (metis subsetD) |
26191 | 541 |
|
26272 | 542 |
lemma chain_subset_antisym_Union: |
52181 | 543 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)" |
54482 | 544 |
unfolding chain_subset_def antisym_def |
545 |
apply simp |
|
546 |
by (metis (no_types) subsetD) |
|
26191 | 547 |
|
26272 | 548 |
lemma chain_subset_Total_Union: |
52181 | 549 |
assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r" |
550 |
shows "Total (\<Union>R)" |
|
551 |
proof (simp add: total_on_def Ball_def, auto del: disjCI) |
|
552 |
fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b" |
|
553 |
from `chain\<^sub>\<subseteq> R` and `r \<in> R` and `s \<in> R` have "r \<subseteq> s \<or> s \<subseteq> r" |
|
554 |
by (auto simp add: chain_subset_def) |
|
555 |
thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)" |
|
26191 | 556 |
proof |
52181 | 557 |
assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A |
54482 | 558 |
by (simp add: total_on_def) (metis (no_types) mono_Field subsetD) |
52181 | 559 |
thus ?thesis using `s \<in> R` by blast |
26191 | 560 |
next |
52181 | 561 |
assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A |
54482 | 562 |
by (simp add: total_on_def) (metis (no_types) mono_Field subsetD) |
52181 | 563 |
thus ?thesis using `r \<in> R` by blast |
26191 | 564 |
qed |
565 |
qed |
|
566 |
||
567 |
lemma wf_Union_wf_init_segs: |
|
52181 | 568 |
assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r" |
569 |
shows "wf (\<Union>R)" |
|
570 |
proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) |
|
571 |
fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r" |
|
572 |
then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto |
|
573 |
{ fix i have "(f (Suc i), f i) \<in> r" |
|
574 |
proof (induct i) |
|
26191 | 575 |
case 0 show ?case by fact |
576 |
next |
|
577 |
case (Suc i) |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
578 |
then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30663
diff
changeset
|
579 |
using 1 by auto |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
580 |
then have "s initial_segment_of r \<or> r initial_segment_of s" |
52181 | 581 |
using assms(1) `r \<in> R` by (simp add: Chains_def) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
582 |
with Suc s show ?case by (simp add: init_seg_of_def) blast |
26191 | 583 |
qed |
584 |
} |
|
52181 | 585 |
thus False using assms(2) and `r \<in> R` |
586 |
by (simp add: wf_iff_no_infinite_down_chain) blast |
|
26191 | 587 |
qed |
588 |
||
27476 | 589 |
lemma initial_segment_of_Diff: |
590 |
"p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s" |
|
52181 | 591 |
unfolding init_seg_of_def by blast |
27476 | 592 |
|
52181 | 593 |
lemma Chains_inits_DiffI: |
594 |
"R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of" |
|
595 |
unfolding Chains_def by (blast intro: initial_segment_of_Diff) |
|
26191 | 596 |
|
52181 | 597 |
theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV" |
598 |
proof - |
|
26191 | 599 |
-- {*The initial segment relation on well-orders: *} |
52181 | 600 |
let ?WO = "{r::'a rel. Well_order r}" |
26191 | 601 |
def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO" |
52181 | 602 |
have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def) |
603 |
hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R" |
|
54482 | 604 |
unfolding init_seg_of_def chain_subset_def Chains_def by blast |
52181 | 605 |
have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r" |
606 |
by (simp add: Chains_def I_def) blast |
|
607 |
have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def) |
|
26191 | 608 |
hence 0: "Partial_order I" |
52181 | 609 |
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def |
610 |
trans_def I_def elim!: trans_init_seg_of) |
|
26191 | 611 |
-- {*I-chains have upper bounds in ?WO wrt I: their Union*} |
52181 | 612 |
{ fix R assume "R \<in> Chains I" |
613 |
hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast |
|
614 |
have subch: "chain\<^sub>\<subseteq> R" using `R : Chains I` I_init |
|
615 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
616 |
have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" |
|
617 |
and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" |
|
618 |
using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs) |
|
54482 | 619 |
have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` unfolding refl_on_def by fastforce |
26191 | 620 |
moreover have "trans (\<Union>R)" |
52181 | 621 |
by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`]) |
622 |
moreover have "antisym (\<Union>R)" |
|
623 |
by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`]) |
|
26191 | 624 |
moreover have "Total (\<Union>R)" |
52181 | 625 |
by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`]) |
626 |
moreover have "wf ((\<Union>R) - Id)" |
|
627 |
proof - |
|
628 |
have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast |
|
629 |
with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] |
|
54482 | 630 |
show ?thesis by fastforce |
26191 | 631 |
qed |
26295 | 632 |
ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs) |
26191 | 633 |
moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris |
52181 | 634 |
by(simp add: Chains_init_seg_of_Union) |
635 |
ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)" |
|
636 |
using mono_Chains [OF I_init] and `R \<in> Chains I` |
|
637 |
by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
|
26191 | 638 |
} |
52181 | 639 |
hence 1: "\<forall>R \<in> Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast |
26191 | 640 |
--{*Zorn's Lemma yields a maximal well-order m:*} |
52181 | 641 |
then obtain m::"'a rel" where "Well_order m" and |
642 |
max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m" |
|
54482 | 643 |
using Zorns_po_lemma[OF 0 1] unfolding FI by fastforce |
26191 | 644 |
--{*Now show by contradiction that m covers the whole type:*} |
645 |
{ fix x::'a assume "x \<notin> Field m" |
|
646 |
--{*We assume that x is not covered and extend m at the top with x*} |
|
647 |
have "m \<noteq> {}" |
|
648 |
proof |
|
52181 | 649 |
assume "m = {}" |
650 |
moreover have "Well_order {(x, x)}" |
|
651 |
by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def) |
|
26191 | 652 |
ultimately show False using max |
52181 | 653 |
by (auto simp: I_def init_seg_of_def simp del: Field_insert) |
26191 | 654 |
qed |
655 |
hence "Field m \<noteq> {}" by(auto simp:Field_def) |
|
52181 | 656 |
moreover have "wf (m - Id)" using `Well_order m` |
657 |
by (simp add: well_order_on_def) |
|
26191 | 658 |
--{*The extension of m by x:*} |
52181 | 659 |
let ?s = "{(a, x) | a. a \<in> Field m}" |
660 |
let ?m = "insert (x, x) m \<union> ?s" |
|
26191 | 661 |
have Fm: "Field ?m = insert x (Field m)" |
52181 | 662 |
by (auto simp: Field_def) |
663 |
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" |
|
664 |
using `Well_order m` by (simp_all add: order_on_defs) |
|
26191 | 665 |
--{*We show that the extension is a well-order*} |
54482 | 666 |
have "Refl ?m" using `Refl m` Fm unfolding refl_on_def by blast |
52181 | 667 |
moreover have "trans ?m" using `trans m` and `x \<notin> Field m` |
668 |
unfolding trans_def Field_def by blast |
|
669 |
moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m` |
|
670 |
unfolding antisym_def Field_def by blast |
|
671 |
moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def) |
|
672 |
moreover have "wf (?m - Id)" |
|
673 |
proof - |
|
26191 | 674 |
have "wf ?s" using `x \<notin> Field m` |
52181 | 675 |
by (auto simp add: wf_eq_minimal Field_def) metis |
676 |
thus ?thesis using `wf (m - Id)` and `x \<notin> Field m` |
|
677 |
wf_subset [OF `wf ?s` Diff_subset] |
|
54482 | 678 |
unfolding Un_Diff Field_def by (auto intro: wf_Un) |
26191 | 679 |
qed |
52181 | 680 |
ultimately have "Well_order ?m" by (simp add: order_on_defs) |
26191 | 681 |
--{*We show that the extension is above m*} |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
682 |
moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m` |
52181 | 683 |
by (fastforce simp: I_def init_seg_of_def Field_def) |
26191 | 684 |
ultimately |
685 |
--{*This contradicts maximality of m:*} |
|
52181 | 686 |
have False using max and `x \<notin> Field m` unfolding Field_def by blast |
26191 | 687 |
} |
688 |
hence "Field m = UNIV" by auto |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52821
diff
changeset
|
689 |
with `Well_order m` show ?thesis by blast |
26272 | 690 |
qed |
691 |
||
52181 | 692 |
corollary well_order_on: "\<exists>r::'a rel. well_order_on A r" |
26272 | 693 |
proof - |
52181 | 694 |
obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" |
695 |
using well_ordering [where 'a = "'a"] by blast |
|
696 |
let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" |
|
26272 | 697 |
have 1: "Field ?r = A" using wo univ |
52181 | 698 |
by (fastforce simp: Field_def order_on_defs refl_on_def) |
699 |
have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)" |
|
700 |
using `Well_order r` by (simp_all add: order_on_defs) |
|
701 |
have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ) |
|
26272 | 702 |
moreover have "trans ?r" using `trans r` |
703 |
unfolding trans_def by blast |
|
704 |
moreover have "antisym ?r" using `antisym r` |
|
705 |
unfolding antisym_def by blast |
|
52181 | 706 |
moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ) |
707 |
moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast |
|
708 |
ultimately have "Well_order ?r" by (simp add: order_on_defs) |
|
54482 | 709 |
with 1 show ?thesis by auto |
26191 | 710 |
qed |
711 |
||
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
712 |
end |