author | popescua |
Fri, 24 May 2013 17:37:06 +0200 | |
changeset 52181 | 59e5dd7b8f9a |
parent 51500 | 01fe31f05aa8 |
child 52183 | 667961fa6a60 |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30663
diff
changeset
|
1 |
(* Title: HOL/Library/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 |
48750 | 13 |
imports Order_Relation |
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" |
|
73 |
by (auto simp: suc_def) (metis less_irrefl not_maxchain_Some) |
|
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 - |
|
121 |
from `chain X` have "chain (suc X)" by (rule chain_suc) |
|
122 |
moreover then have "suc X \<subseteq> A" unfolding chain_def by blast |
|
123 |
ultimately show ?thesis by blast |
|
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) |
|
260 |
case (suc X) then show ?case by (simp add: suc_def) (metis not_maxchain_Some) |
|
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 |
|
350 |
moreover assume "\<Union>C \<noteq> X" |
|
351 |
moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto |
|
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 |
|
380 |
ultimately show ?thesis by blast |
|
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 |
|
52181 | 417 |
lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s" |
418 |
unfolding Chains_def by blast |
|
419 |
||
420 |
lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C" |
|
421 |
by (auto simp add: chain_subset_def subset.chain_def) |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
422 |
|
52181 | 423 |
lemma chains_alt_def: "chains A = {C. subset.chain A C}" |
424 |
by (simp add: chains_def chain_subset_alt_def subset.chain_def) |
|
425 |
||
426 |
lemma Chains_subset: |
|
427 |
"Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
428 |
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
|
429 |
|
52181 | 430 |
lemma Chains_subset': |
431 |
assumes "refl r" |
|
432 |
shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r" |
|
433 |
using assms |
|
434 |
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
|
435 |
|
52181 | 436 |
lemma Chains_alt_def: |
437 |
assumes "refl r" |
|
438 |
shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
439 |
using assms |
|
440 |
by (metis Chains_subset Chains_subset' subset_antisym) |
|
441 |
||
442 |
lemma Zorn_Lemma: |
|
443 |
"\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
444 |
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
|
445 |
|
52181 | 446 |
lemma Zorn_Lemma2: |
447 |
"\<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" |
|
448 |
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
|
449 |
|
52181 | 450 |
lemma Zorns_po_lemma: |
451 |
assumes po: "Partial_order r" |
|
452 |
and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r" |
|
453 |
shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
454 |
proof - |
|
455 |
have "Preorder r" using po by (simp add: partial_order_on_def) |
|
456 |
--{* Mirror r in the set of subsets below (wrt r) elements of A*} |
|
457 |
let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r" |
|
458 |
{ |
|
459 |
fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" |
|
460 |
let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}" |
|
461 |
have "C = ?B ` ?A" using 1 by (auto simp: image_def) |
|
462 |
have "?A \<in> Chains r" |
|
463 |
proof (simp add: Chains_def, intro allI impI, elim conjE) |
|
464 |
fix a b |
|
465 |
assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C" |
|
466 |
hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto |
|
467 |
thus "(a, b) \<in> r \<or> (b, a) \<in> r" |
|
468 |
using `Preorder r` and `a \<in> Field r` and `b \<in> Field r` |
|
469 |
by (simp add:subset_Image1_Image1_iff) |
|
470 |
qed |
|
471 |
then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto |
|
472 |
have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u") |
|
473 |
proof auto |
|
474 |
fix a B assume aB: "B \<in> C" "a \<in> B" |
|
475 |
with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto |
|
476 |
thus "(a, u) \<in> r" using uA and aB and `Preorder r` |
|
477 |
by (auto simp add: preorder_on_def refl_on_def) (metis transD) |
|
478 |
qed |
|
479 |
then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast |
|
480 |
} |
|
481 |
then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U" |
|
482 |
by (auto simp: chains_def chain_subset_def) |
|
483 |
from Zorn_Lemma2 [OF this] |
|
484 |
obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}" |
|
485 |
and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B" |
|
486 |
by auto |
|
487 |
hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
488 |
using po and `Preorder r` and `m \<in> Field r` |
|
489 |
by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) |
|
490 |
thus ?thesis using `m \<in> Field r` by blast |
|
491 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
492 |
|
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
493 |
|
52181 | 494 |
subsection {* The Well Ordering Theorem *} |
26191 | 495 |
|
496 |
(* The initial segment of a relation appears generally useful. |
|
497 |
Move to Relation.thy? |
|
498 |
Definition correct/most general? |
|
499 |
Naming? |
|
500 |
*) |
|
52181 | 501 |
definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where |
502 |
"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 | 503 |
|
52181 | 504 |
abbreviation |
505 |
initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55) |
|
506 |
where |
|
507 |
"r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of" |
|
26191 | 508 |
|
52181 | 509 |
lemma refl_on_init_seg_of [simp]: "r initial_segment_of r" |
510 |
by (simp add: init_seg_of_def) |
|
26191 | 511 |
|
512 |
lemma trans_init_seg_of: |
|
513 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t" |
|
52181 | 514 |
by (simp (no_asm_use) add: init_seg_of_def) |
515 |
(metis UnCI Un_absorb2 subset_trans) |
|
26191 | 516 |
|
517 |
lemma antisym_init_seg_of: |
|
52181 | 518 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s" |
519 |
unfolding init_seg_of_def by safe |
|
26191 | 520 |
|
52181 | 521 |
lemma Chains_init_seg_of_Union: |
522 |
"R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R" |
|
523 |
by (auto simp: init_seg_of_def Ball_def Chains_def) blast |
|
26191 | 524 |
|
26272 | 525 |
lemma chain_subset_trans_Union: |
52181 | 526 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)" |
527 |
apply (auto simp add: chain_subset_def) |
|
528 |
apply (simp (no_asm_use) add: trans_def) |
|
529 |
apply (metis subsetD) |
|
530 |
done |
|
26191 | 531 |
|
26272 | 532 |
lemma chain_subset_antisym_Union: |
52181 | 533 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)" |
534 |
apply (auto simp add: chain_subset_def antisym_def) |
|
535 |
apply (metis subsetD) |
|
536 |
done |
|
26191 | 537 |
|
26272 | 538 |
lemma chain_subset_Total_Union: |
52181 | 539 |
assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r" |
540 |
shows "Total (\<Union>R)" |
|
541 |
proof (simp add: total_on_def Ball_def, auto del: disjCI) |
|
542 |
fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b" |
|
543 |
from `chain\<^sub>\<subseteq> R` and `r \<in> R` and `s \<in> R` have "r \<subseteq> s \<or> s \<subseteq> r" |
|
544 |
by (auto simp add: chain_subset_def) |
|
545 |
thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)" |
|
26191 | 546 |
proof |
52181 | 547 |
assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A |
548 |
by (simp add: total_on_def) (metis mono_Field subsetD) |
|
549 |
thus ?thesis using `s \<in> R` by blast |
|
26191 | 550 |
next |
52181 | 551 |
assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A |
552 |
by (simp add: total_on_def) (metis mono_Field subsetD) |
|
553 |
thus ?thesis using `r \<in> R` by blast |
|
26191 | 554 |
qed |
555 |
qed |
|
556 |
||
557 |
lemma wf_Union_wf_init_segs: |
|
52181 | 558 |
assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r" |
559 |
shows "wf (\<Union>R)" |
|
560 |
proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) |
|
561 |
fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r" |
|
562 |
then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto |
|
563 |
{ fix i have "(f (Suc i), f i) \<in> r" |
|
564 |
proof (induct i) |
|
26191 | 565 |
case 0 show ?case by fact |
566 |
next |
|
567 |
case (Suc i) |
|
52181 | 568 |
moreover obtain s where "s \<in> R" and "(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
|
569 |
using 1 by auto |
26191 | 570 |
moreover hence "s initial_segment_of r \<or> r initial_segment_of s" |
52181 | 571 |
using assms(1) `r \<in> R` by (simp add: Chains_def) |
572 |
ultimately show ?case by (simp add: init_seg_of_def) blast |
|
26191 | 573 |
qed |
574 |
} |
|
52181 | 575 |
thus False using assms(2) and `r \<in> R` |
576 |
by (simp add: wf_iff_no_infinite_down_chain) blast |
|
26191 | 577 |
qed |
578 |
||
27476 | 579 |
lemma initial_segment_of_Diff: |
580 |
"p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s" |
|
52181 | 581 |
unfolding init_seg_of_def by blast |
27476 | 582 |
|
52181 | 583 |
lemma Chains_inits_DiffI: |
584 |
"R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of" |
|
585 |
unfolding Chains_def by (blast intro: initial_segment_of_Diff) |
|
26191 | 586 |
|
52181 | 587 |
theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV" |
588 |
proof - |
|
26191 | 589 |
-- {*The initial segment relation on well-orders: *} |
52181 | 590 |
let ?WO = "{r::'a rel. Well_order r}" |
26191 | 591 |
def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO" |
52181 | 592 |
have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def) |
593 |
hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R" |
|
594 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
595 |
have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r" |
|
596 |
by (simp add: Chains_def I_def) blast |
|
597 |
have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def) |
|
26191 | 598 |
hence 0: "Partial_order I" |
52181 | 599 |
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def |
600 |
trans_def I_def elim!: trans_init_seg_of) |
|
26191 | 601 |
-- {*I-chains have upper bounds in ?WO wrt I: their Union*} |
52181 | 602 |
{ fix R assume "R \<in> Chains I" |
603 |
hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast |
|
604 |
have subch: "chain\<^sub>\<subseteq> R" using `R : Chains I` I_init |
|
605 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
606 |
have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" |
|
607 |
and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" |
|
608 |
using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs) |
|
609 |
have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def) |
|
26191 | 610 |
moreover have "trans (\<Union>R)" |
52181 | 611 |
by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`]) |
612 |
moreover have "antisym (\<Union>R)" |
|
613 |
by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`]) |
|
26191 | 614 |
moreover have "Total (\<Union>R)" |
52181 | 615 |
by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`]) |
616 |
moreover have "wf ((\<Union>R) - Id)" |
|
617 |
proof - |
|
618 |
have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast |
|
619 |
with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] |
|
26191 | 620 |
show ?thesis by (simp (no_asm_simp)) blast |
621 |
qed |
|
26295 | 622 |
ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs) |
26191 | 623 |
moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris |
52181 | 624 |
by(simp add: Chains_init_seg_of_Union) |
625 |
ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)" |
|
626 |
using mono_Chains [OF I_init] and `R \<in> Chains I` |
|
627 |
by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
|
26191 | 628 |
} |
52181 | 629 |
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 | 630 |
--{*Zorn's Lemma yields a maximal well-order m:*} |
52181 | 631 |
then obtain m::"'a rel" where "Well_order m" and |
632 |
max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m" |
|
26191 | 633 |
using Zorns_po_lemma[OF 0 1] by (auto simp:FI) |
634 |
--{*Now show by contradiction that m covers the whole type:*} |
|
635 |
{ fix x::'a assume "x \<notin> Field m" |
|
636 |
--{*We assume that x is not covered and extend m at the top with x*} |
|
637 |
have "m \<noteq> {}" |
|
638 |
proof |
|
52181 | 639 |
assume "m = {}" |
640 |
moreover have "Well_order {(x, x)}" |
|
641 |
by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def) |
|
26191 | 642 |
ultimately show False using max |
52181 | 643 |
by (auto simp: I_def init_seg_of_def simp del: Field_insert) |
26191 | 644 |
qed |
645 |
hence "Field m \<noteq> {}" by(auto simp:Field_def) |
|
52181 | 646 |
moreover have "wf (m - Id)" using `Well_order m` |
647 |
by (simp add: well_order_on_def) |
|
26191 | 648 |
--{*The extension of m by x:*} |
52181 | 649 |
let ?s = "{(a, x) | a. a \<in> Field m}" |
650 |
let ?m = "insert (x, x) m \<union> ?s" |
|
26191 | 651 |
have Fm: "Field ?m = insert x (Field m)" |
52181 | 652 |
by (auto simp: Field_def) |
653 |
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" |
|
654 |
using `Well_order m` by (simp_all add: order_on_defs) |
|
26191 | 655 |
--{*We show that the extension is a well-order*} |
52181 | 656 |
have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) |
657 |
moreover have "trans ?m" using `trans m` and `x \<notin> Field m` |
|
658 |
unfolding trans_def Field_def by blast |
|
659 |
moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m` |
|
660 |
unfolding antisym_def Field_def by blast |
|
661 |
moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def) |
|
662 |
moreover have "wf (?m - Id)" |
|
663 |
proof - |
|
26191 | 664 |
have "wf ?s" using `x \<notin> Field m` |
52181 | 665 |
by (auto simp add: wf_eq_minimal Field_def) metis |
666 |
thus ?thesis using `wf (m - Id)` and `x \<notin> Field m` |
|
667 |
wf_subset [OF `wf ?s` Diff_subset] |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
35175
diff
changeset
|
668 |
by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
26191 | 669 |
qed |
52181 | 670 |
ultimately have "Well_order ?m" by (simp add: order_on_defs) |
26191 | 671 |
--{*We show that the extension is above m*} |
52181 | 672 |
moreover hence "(m, ?m) \<in> I" using `Well_order m` and `x \<notin> Field m` |
673 |
by (fastforce simp: I_def init_seg_of_def Field_def) |
|
26191 | 674 |
ultimately |
675 |
--{*This contradicts maximality of m:*} |
|
52181 | 676 |
have False using max and `x \<notin> Field m` unfolding Field_def by blast |
26191 | 677 |
} |
678 |
hence "Field m = UNIV" by auto |
|
26272 | 679 |
moreover with `Well_order m` have "Well_order m" by simp |
680 |
ultimately show ?thesis by blast |
|
681 |
qed |
|
682 |
||
52181 | 683 |
corollary well_order_on: "\<exists>r::'a rel. well_order_on A r" |
26272 | 684 |
proof - |
52181 | 685 |
obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" |
686 |
using well_ordering [where 'a = "'a"] by blast |
|
687 |
let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" |
|
26272 | 688 |
have 1: "Field ?r = A" using wo univ |
52181 | 689 |
by (fastforce simp: Field_def order_on_defs refl_on_def) |
690 |
have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)" |
|
691 |
using `Well_order r` by (simp_all add: order_on_defs) |
|
692 |
have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ) |
|
26272 | 693 |
moreover have "trans ?r" using `trans r` |
694 |
unfolding trans_def by blast |
|
695 |
moreover have "antisym ?r" using `antisym r` |
|
696 |
unfolding antisym_def by blast |
|
52181 | 697 |
moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ) |
698 |
moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast |
|
699 |
ultimately have "Well_order ?r" by (simp add: order_on_defs) |
|
26295 | 700 |
with 1 show ?thesis by metis |
26191 | 701 |
qed |
702 |
||
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
703 |
end |
52181 | 704 |