author | popescua |
Tue, 28 May 2013 13:19:51 +0200 | |
changeset 52199 | d25fc4c0ff62 |
parent 52183 | 667961fa6a60 |
child 52821 | 05eb2d77b195 |
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. |
52199 | 8 |
The extension of any well-founded relation to a well-order. |
14706 | 9 |
*) |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
10 |
|
14706 | 11 |
header {* Zorn's Lemma *} |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
12 |
|
15131 | 13 |
theory Zorn |
52199 | 14 |
imports Order_Union |
15131 | 15 |
begin |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
16 |
|
52181 | 17 |
subsection {* Zorn's Lemma for the Subset Relation *} |
18 |
||
19 |
subsubsection {* Results that do not require an order *} |
|
20 |
||
21 |
text {*Let @{text P} be a binary predicate on the set @{text A}.*} |
|
22 |
locale pred_on = |
|
23 |
fixes A :: "'a set" |
|
24 |
and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50) |
|
25 |
begin |
|
26 |
||
27 |
abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) where |
|
28 |
"x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y" |
|
29 |
||
30 |
text {*A chain is a totally ordered subset of @{term A}.*} |
|
31 |
definition chain :: "'a set \<Rightarrow> bool" where |
|
32 |
"chain C \<longleftrightarrow> C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)" |
|
33 |
||
34 |
text {*We call a chain that is a proper superset of some set @{term X}, |
|
35 |
but not necessarily a chain itself, a superchain of @{term X}.*} |
|
36 |
abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50) where |
|
37 |
"X <c C \<equiv> chain C \<and> X \<subset> C" |
|
38 |
||
39 |
text {*A maximal chain is a chain that does not have a superchain.*} |
|
40 |
definition maxchain :: "'a set \<Rightarrow> bool" where |
|
41 |
"maxchain C \<longleftrightarrow> chain C \<and> \<not> (\<exists>S. C <c S)" |
|
42 |
||
43 |
text {*We define the successor of a set to be an arbitrary |
|
44 |
superchain, if such exists, or the set itself, otherwise.*} |
|
45 |
definition suc :: "'a set \<Rightarrow> 'a set" where |
|
46 |
"suc C = (if \<not> chain C \<or> maxchain C then C else (SOME D. C <c D))" |
|
47 |
||
48 |
lemma chainI [Pure.intro?]: |
|
49 |
"\<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" |
|
50 |
unfolding chain_def by blast |
|
51 |
||
52 |
lemma chain_total: |
|
53 |
"chain C \<Longrightarrow> x \<in> C \<Longrightarrow> y \<in> C \<Longrightarrow> x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
54 |
by (simp add: chain_def) |
|
55 |
||
56 |
lemma not_chain_suc [simp]: "\<not> chain X \<Longrightarrow> suc X = X" |
|
57 |
by (simp add: suc_def) |
|
58 |
||
59 |
lemma maxchain_suc [simp]: "maxchain X \<Longrightarrow> suc X = X" |
|
60 |
by (simp add: suc_def) |
|
61 |
||
62 |
lemma suc_subset: "X \<subseteq> suc X" |
|
63 |
by (auto simp: suc_def maxchain_def intro: someI2) |
|
64 |
||
65 |
lemma chain_empty [simp]: "chain {}" |
|
66 |
by (auto simp: chain_def) |
|
67 |
||
68 |
lemma not_maxchain_Some: |
|
69 |
"chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> C <c (SOME D. C <c D)" |
|
70 |
by (rule someI_ex) (auto simp: maxchain_def) |
|
71 |
||
72 |
lemma suc_not_equals: |
|
73 |
"chain C \<Longrightarrow> \<not> maxchain C \<Longrightarrow> suc C \<noteq> C" |
|
74 |
by (auto simp: suc_def) (metis less_irrefl not_maxchain_Some) |
|
75 |
||
76 |
lemma subset_suc: |
|
77 |
assumes "X \<subseteq> Y" shows "X \<subseteq> suc Y" |
|
78 |
using assms by (rule subset_trans) (rule suc_subset) |
|
79 |
||
80 |
text {*We build a set @{term \<C>} that is closed under applications |
|
81 |
of @{term suc} and contains the union of all its subsets.*} |
|
82 |
inductive_set suc_Union_closed ("\<C>") where |
|
83 |
suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>" | |
|
84 |
Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>" |
|
85 |
||
86 |
text {*Since the empty set as well as the set itself is a subset of |
|
87 |
every set, @{term \<C>} contains at least @{term "{} \<in> \<C>"} and |
|
88 |
@{term "\<Union>\<C> \<in> \<C>"}.*} |
|
89 |
lemma |
|
90 |
suc_Union_closed_empty: "{} \<in> \<C>" and |
|
91 |
suc_Union_closed_Union: "\<Union>\<C> \<in> \<C>" |
|
92 |
using Union [of "{}"] and Union [of "\<C>"] by simp+ |
|
93 |
text {*Thus closure under @{term suc} will hit a maximal chain |
|
94 |
eventually, as is shown below.*} |
|
95 |
||
96 |
lemma suc_Union_closed_induct [consumes 1, case_names suc Union, |
|
97 |
induct pred: suc_Union_closed]: |
|
98 |
assumes "X \<in> \<C>" |
|
99 |
and "\<And>X. \<lbrakk>X \<in> \<C>; Q X\<rbrakk> \<Longrightarrow> Q (suc X)" |
|
100 |
and "\<And>X. \<lbrakk>X \<subseteq> \<C>; \<forall>x\<in>X. Q x\<rbrakk> \<Longrightarrow> Q (\<Union>X)" |
|
101 |
shows "Q X" |
|
102 |
using assms by (induct) blast+ |
|
26272 | 103 |
|
52181 | 104 |
lemma suc_Union_closed_cases [consumes 1, case_names suc Union, |
105 |
cases pred: suc_Union_closed]: |
|
106 |
assumes "X \<in> \<C>" |
|
107 |
and "\<And>Y. \<lbrakk>X = suc Y; Y \<in> \<C>\<rbrakk> \<Longrightarrow> Q" |
|
108 |
and "\<And>Y. \<lbrakk>X = \<Union>Y; Y \<subseteq> \<C>\<rbrakk> \<Longrightarrow> Q" |
|
109 |
shows "Q" |
|
110 |
using assms by (cases) simp+ |
|
111 |
||
112 |
text {*On chains, @{term suc} yields a chain.*} |
|
113 |
lemma chain_suc: |
|
114 |
assumes "chain X" shows "chain (suc X)" |
|
115 |
using assms |
|
116 |
by (cases "\<not> chain X \<or> maxchain X") |
|
117 |
(force simp: suc_def dest: not_maxchain_Some)+ |
|
118 |
||
119 |
lemma chain_sucD: |
|
120 |
assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)" |
|
121 |
proof - |
|
122 |
from `chain X` have "chain (suc X)" by (rule chain_suc) |
|
123 |
moreover then have "suc X \<subseteq> A" unfolding chain_def by blast |
|
124 |
ultimately show ?thesis by blast |
|
125 |
qed |
|
126 |
||
127 |
lemma suc_Union_closed_total': |
|
128 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" |
|
129 |
and *: "\<And>Z. Z \<in> \<C> \<Longrightarrow> Z \<subseteq> Y \<Longrightarrow> Z = Y \<or> suc Z \<subseteq> Y" |
|
130 |
shows "X \<subseteq> Y \<or> suc Y \<subseteq> X" |
|
131 |
using `X \<in> \<C>` |
|
132 |
proof (induct) |
|
133 |
case (suc X) |
|
134 |
with * show ?case by (blast del: subsetI intro: subset_suc) |
|
135 |
qed blast |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
136 |
|
52181 | 137 |
lemma suc_Union_closed_subsetD: |
138 |
assumes "Y \<subseteq> X" and "X \<in> \<C>" and "Y \<in> \<C>" |
|
139 |
shows "X = Y \<or> suc Y \<subseteq> X" |
|
140 |
using assms(2-, 1) |
|
141 |
proof (induct arbitrary: Y) |
|
142 |
case (suc X) |
|
143 |
note * = `\<And>Y. \<lbrakk>Y \<in> \<C>; Y \<subseteq> X\<rbrakk> \<Longrightarrow> X = Y \<or> suc Y \<subseteq> X` |
|
144 |
with suc_Union_closed_total' [OF `Y \<in> \<C>` `X \<in> \<C>`] |
|
145 |
have "Y \<subseteq> X \<or> suc X \<subseteq> Y" by blast |
|
146 |
then show ?case |
|
147 |
proof |
|
148 |
assume "Y \<subseteq> X" |
|
149 |
with * and `Y \<in> \<C>` have "X = Y \<or> suc Y \<subseteq> X" by blast |
|
150 |
then show ?thesis |
|
151 |
proof |
|
152 |
assume "X = Y" then show ?thesis by simp |
|
153 |
next |
|
154 |
assume "suc Y \<subseteq> X" |
|
155 |
then have "suc Y \<subseteq> suc X" by (rule subset_suc) |
|
156 |
then show ?thesis by simp |
|
157 |
qed |
|
158 |
next |
|
159 |
assume "suc X \<subseteq> Y" |
|
160 |
with `Y \<subseteq> suc X` show ?thesis by blast |
|
161 |
qed |
|
162 |
next |
|
163 |
case (Union X) |
|
164 |
show ?case |
|
165 |
proof (rule ccontr) |
|
166 |
assume "\<not> ?thesis" |
|
167 |
with `Y \<subseteq> \<Union>X` obtain x y z |
|
168 |
where "\<not> suc Y \<subseteq> \<Union>X" |
|
169 |
and "x \<in> X" and "y \<in> x" and "y \<notin> Y" |
|
170 |
and "z \<in> suc Y" and "\<forall>x\<in>X. z \<notin> x" by blast |
|
171 |
with `X \<subseteq> \<C>` have "x \<in> \<C>" by blast |
|
172 |
from Union and `x \<in> X` |
|
173 |
have *: "\<And>y. \<lbrakk>y \<in> \<C>; y \<subseteq> x\<rbrakk> \<Longrightarrow> x = y \<or> suc y \<subseteq> x" by blast |
|
174 |
with suc_Union_closed_total' [OF `Y \<in> \<C>` `x \<in> \<C>`] |
|
175 |
have "Y \<subseteq> x \<or> suc x \<subseteq> Y" by blast |
|
176 |
then show False |
|
177 |
proof |
|
178 |
assume "Y \<subseteq> x" |
|
179 |
with * [OF `Y \<in> \<C>`] have "x = Y \<or> suc Y \<subseteq> x" by blast |
|
180 |
then show False |
|
181 |
proof |
|
182 |
assume "x = Y" with `y \<in> x` and `y \<notin> Y` show False by blast |
|
183 |
next |
|
184 |
assume "suc Y \<subseteq> x" |
|
185 |
with `x \<in> X` have "suc Y \<subseteq> \<Union>X" by blast |
|
186 |
with `\<not> suc Y \<subseteq> \<Union>X` show False by contradiction |
|
187 |
qed |
|
188 |
next |
|
189 |
assume "suc x \<subseteq> Y" |
|
190 |
moreover from suc_subset and `y \<in> x` have "y \<in> suc x" by blast |
|
191 |
ultimately show False using `y \<notin> Y` by blast |
|
192 |
qed |
|
193 |
qed |
|
194 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
195 |
|
52181 | 196 |
text {*The elements of @{term \<C>} are totally ordered by the subset relation.*} |
197 |
lemma suc_Union_closed_total: |
|
198 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" |
|
199 |
shows "X \<subseteq> Y \<or> Y \<subseteq> X" |
|
200 |
proof (cases "\<forall>Z\<in>\<C>. Z \<subseteq> Y \<longrightarrow> Z = Y \<or> suc Z \<subseteq> Y") |
|
201 |
case True |
|
202 |
with suc_Union_closed_total' [OF assms] |
|
203 |
have "X \<subseteq> Y \<or> suc Y \<subseteq> X" by blast |
|
204 |
then show ?thesis using suc_subset [of Y] by blast |
|
205 |
next |
|
206 |
case False |
|
207 |
then obtain Z |
|
208 |
where "Z \<in> \<C>" and "Z \<subseteq> Y" and "Z \<noteq> Y" and "\<not> suc Z \<subseteq> Y" by blast |
|
209 |
with suc_Union_closed_subsetD and `Y \<in> \<C>` show ?thesis by blast |
|
210 |
qed |
|
211 |
||
212 |
text {*Once we hit a fixed point w.r.t. @{term suc}, all other elements |
|
213 |
of @{term \<C>} are subsets of this fixed point.*} |
|
214 |
lemma suc_Union_closed_suc: |
|
215 |
assumes "X \<in> \<C>" and "Y \<in> \<C>" and "suc Y = Y" |
|
216 |
shows "X \<subseteq> Y" |
|
217 |
using `X \<in> \<C>` |
|
218 |
proof (induct) |
|
219 |
case (suc X) |
|
220 |
with `Y \<in> \<C>` and suc_Union_closed_subsetD |
|
221 |
have "X = Y \<or> suc X \<subseteq> Y" by blast |
|
222 |
then show ?case by (auto simp: `suc Y = Y`) |
|
223 |
qed blast |
|
224 |
||
225 |
lemma eq_suc_Union: |
|
226 |
assumes "X \<in> \<C>" |
|
227 |
shows "suc X = X \<longleftrightarrow> X = \<Union>\<C>" |
|
228 |
proof |
|
229 |
assume "suc X = X" |
|
230 |
with suc_Union_closed_suc [OF suc_Union_closed_Union `X \<in> \<C>`] |
|
231 |
have "\<Union>\<C> \<subseteq> X" . |
|
232 |
with `X \<in> \<C>` show "X = \<Union>\<C>" by blast |
|
233 |
next |
|
234 |
from `X \<in> \<C>` have "suc X \<in> \<C>" by (rule suc) |
|
235 |
then have "suc X \<subseteq> \<Union>\<C>" by blast |
|
236 |
moreover assume "X = \<Union>\<C>" |
|
237 |
ultimately have "suc X \<subseteq> X" by simp |
|
238 |
moreover have "X \<subseteq> suc X" by (rule suc_subset) |
|
239 |
ultimately show "suc X = X" .. |
|
240 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
241 |
|
52181 | 242 |
lemma suc_in_carrier: |
243 |
assumes "X \<subseteq> A" |
|
244 |
shows "suc X \<subseteq> A" |
|
245 |
using assms |
|
246 |
by (cases "\<not> chain X \<or> maxchain X") |
|
247 |
(auto dest: chain_sucD) |
|
248 |
||
249 |
lemma suc_Union_closed_in_carrier: |
|
250 |
assumes "X \<in> \<C>" |
|
251 |
shows "X \<subseteq> A" |
|
252 |
using assms |
|
253 |
by (induct) (auto dest: suc_in_carrier) |
|
254 |
||
255 |
text {*All elements of @{term \<C>} are chains.*} |
|
256 |
lemma suc_Union_closed_chain: |
|
257 |
assumes "X \<in> \<C>" |
|
258 |
shows "chain X" |
|
259 |
using assms |
|
260 |
proof (induct) |
|
261 |
case (suc X) then show ?case by (simp add: suc_def) (metis not_maxchain_Some) |
|
262 |
next |
|
263 |
case (Union X) |
|
264 |
then have "\<Union>X \<subseteq> A" by (auto dest: suc_Union_closed_in_carrier) |
|
265 |
moreover have "\<forall>x\<in>\<Union>X. \<forall>y\<in>\<Union>X. x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
266 |
proof (intro ballI) |
|
267 |
fix x y |
|
268 |
assume "x \<in> \<Union>X" and "y \<in> \<Union>X" |
|
269 |
then obtain u v where "x \<in> u" and "u \<in> X" and "y \<in> v" and "v \<in> X" by blast |
|
270 |
with Union have "u \<in> \<C>" and "v \<in> \<C>" and "chain u" and "chain v" by blast+ |
|
271 |
with suc_Union_closed_total have "u \<subseteq> v \<or> v \<subseteq> u" by blast |
|
272 |
then show "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" |
|
273 |
proof |
|
274 |
assume "u \<subseteq> v" |
|
275 |
from `chain v` show ?thesis |
|
276 |
proof (rule chain_total) |
|
277 |
show "y \<in> v" by fact |
|
278 |
show "x \<in> v" using `u \<subseteq> v` and `x \<in> u` by blast |
|
279 |
qed |
|
280 |
next |
|
281 |
assume "v \<subseteq> u" |
|
282 |
from `chain u` show ?thesis |
|
283 |
proof (rule chain_total) |
|
284 |
show "x \<in> u" by fact |
|
285 |
show "y \<in> u" using `v \<subseteq> u` and `y \<in> v` by blast |
|
286 |
qed |
|
287 |
qed |
|
288 |
qed |
|
289 |
ultimately show ?case unfolding chain_def .. |
|
290 |
qed |
|
291 |
||
292 |
subsubsection {* Hausdorff's Maximum Principle *} |
|
293 |
||
294 |
text {*There exists a maximal totally ordered subset of @{term A}. (Note that we do not |
|
295 |
require @{term A} to be partially ordered.)*} |
|
46980 | 296 |
|
52181 | 297 |
theorem Hausdorff: "\<exists>C. maxchain C" |
298 |
proof - |
|
299 |
let ?M = "\<Union>\<C>" |
|
300 |
have "maxchain ?M" |
|
301 |
proof (rule ccontr) |
|
302 |
assume "\<not> maxchain ?M" |
|
303 |
then have "suc ?M \<noteq> ?M" |
|
304 |
using suc_not_equals and |
|
305 |
suc_Union_closed_chain [OF suc_Union_closed_Union] by simp |
|
306 |
moreover have "suc ?M = ?M" |
|
307 |
using eq_suc_Union [OF suc_Union_closed_Union] by simp |
|
308 |
ultimately show False by contradiction |
|
309 |
qed |
|
310 |
then show ?thesis by blast |
|
311 |
qed |
|
312 |
||
313 |
text {*Make notation @{term \<C>} available again.*} |
|
314 |
no_notation suc_Union_closed ("\<C>") |
|
315 |
||
316 |
lemma chain_extend: |
|
317 |
"chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)" |
|
318 |
unfolding chain_def by blast |
|
319 |
||
320 |
lemma maxchain_imp_chain: |
|
321 |
"maxchain C \<Longrightarrow> chain C" |
|
322 |
by (simp add: maxchain_def) |
|
323 |
||
324 |
end |
|
325 |
||
326 |
text {*Hide constant @{const pred_on.suc_Union_closed}, which was just needed |
|
327 |
for the proof of Hausforff's maximum principle.*} |
|
328 |
hide_const pred_on.suc_Union_closed |
|
329 |
||
330 |
lemma chain_mono: |
|
331 |
assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A; P x y\<rbrakk> \<Longrightarrow> Q x y" |
|
332 |
and "pred_on.chain A P C" |
|
333 |
shows "pred_on.chain A Q C" |
|
334 |
using assms unfolding pred_on.chain_def by blast |
|
335 |
||
336 |
subsubsection {* Results for the proper subset relation *} |
|
337 |
||
338 |
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
|
339 |
|
52181 | 340 |
lemma subset_maxchain_max: |
341 |
assumes "subset.maxchain A C" and "X \<in> A" and "\<Union>C \<subseteq> X" |
|
342 |
shows "\<Union>C = X" |
|
343 |
proof (rule ccontr) |
|
344 |
let ?C = "{X} \<union> C" |
|
345 |
from `subset.maxchain A C` have "subset.chain A C" |
|
346 |
and *: "\<And>S. subset.chain A S \<Longrightarrow> \<not> C \<subset> S" |
|
347 |
by (auto simp: subset.maxchain_def) |
|
348 |
moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto |
|
349 |
ultimately have "subset.chain A ?C" |
|
350 |
using subset.chain_extend [of A C X] and `X \<in> A` by auto |
|
351 |
moreover assume "\<Union>C \<noteq> X" |
|
352 |
moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto |
|
353 |
ultimately show False using * by blast |
|
354 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
355 |
|
52181 | 356 |
subsubsection {* Zorn's lemma *} |
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
357 |
|
52181 | 358 |
text {*If every chain has an upper bound, then there is a maximal set.*} |
359 |
lemma subset_Zorn: |
|
360 |
assumes "\<And>C. subset.chain A C \<Longrightarrow> \<exists>U\<in>A. \<forall>X\<in>C. X \<subseteq> U" |
|
361 |
shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
362 |
proof - |
|
363 |
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. |
|
364 |
then have "subset.chain A M" by (rule subset.maxchain_imp_chain) |
|
365 |
with assms obtain Y where "Y \<in> A" and "\<forall>X\<in>M. X \<subseteq> Y" by blast |
|
366 |
moreover have "\<forall>X\<in>A. Y \<subseteq> X \<longrightarrow> Y = X" |
|
367 |
proof (intro ballI impI) |
|
368 |
fix X |
|
369 |
assume "X \<in> A" and "Y \<subseteq> X" |
|
370 |
show "Y = X" |
|
371 |
proof (rule ccontr) |
|
372 |
assume "Y \<noteq> X" |
|
373 |
with `Y \<subseteq> X` have "\<not> X \<subseteq> Y" by blast |
|
374 |
from subset.chain_extend [OF `subset.chain A M` `X \<in> A`] and `\<forall>X\<in>M. X \<subseteq> Y` |
|
375 |
have "subset.chain A ({X} \<union> M)" using `Y \<subseteq> X` by auto |
|
376 |
moreover have "M \<subset> {X} \<union> M" using `\<forall>X\<in>M. X \<subseteq> Y` and `\<not> X \<subseteq> Y` by auto |
|
377 |
ultimately show False |
|
378 |
using `subset.maxchain A M` by (auto simp: subset.maxchain_def) |
|
379 |
qed |
|
380 |
qed |
|
381 |
ultimately show ?thesis by blast |
|
382 |
qed |
|
383 |
||
384 |
text{*Alternative version of Zorn's lemma for the subset relation.*} |
|
385 |
lemma subset_Zorn': |
|
386 |
assumes "\<And>C. subset.chain A C \<Longrightarrow> \<Union>C \<in> A" |
|
387 |
shows "\<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M" |
|
388 |
proof - |
|
389 |
from subset.Hausdorff [of A] obtain M where "subset.maxchain A M" .. |
|
390 |
then have "subset.chain A M" by (rule subset.maxchain_imp_chain) |
|
391 |
with assms have "\<Union>M \<in> A" . |
|
392 |
moreover have "\<forall>Z\<in>A. \<Union>M \<subseteq> Z \<longrightarrow> \<Union>M = Z" |
|
393 |
proof (intro ballI impI) |
|
394 |
fix Z |
|
395 |
assume "Z \<in> A" and "\<Union>M \<subseteq> Z" |
|
396 |
with subset_maxchain_max [OF `subset.maxchain A M`] |
|
397 |
show "\<Union>M = Z" . |
|
398 |
qed |
|
399 |
ultimately show ?thesis by blast |
|
400 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
401 |
|
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
402 |
|
52181 | 403 |
subsection {* Zorn's Lemma for Partial Orders *} |
404 |
||
405 |
text {*Relate old to new definitions.*} |
|
17200 | 406 |
|
52181 | 407 |
(* Define globally? In Set.thy? *) |
408 |
definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") where |
|
409 |
"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
|
410 |
|
52181 | 411 |
definition chains :: "'a set set \<Rightarrow> 'a set set set" where |
412 |
"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
|
413 |
|
52181 | 414 |
(* Define globally? In Relation.thy? *) |
415 |
definition Chains :: "('a \<times> 'a) set \<Rightarrow> 'a set set" where |
|
416 |
"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
|
417 |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
418 |
lemma chains_extend: |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
419 |
"[| 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
|
420 |
by (unfold chains_def chain_subset_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
421 |
|
52181 | 422 |
lemma mono_Chains: "r \<subseteq> s \<Longrightarrow> Chains r \<subseteq> Chains s" |
423 |
unfolding Chains_def by blast |
|
424 |
||
425 |
lemma chain_subset_alt_def: "chain\<^sub>\<subseteq> C = subset.chain UNIV C" |
|
426 |
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
|
427 |
|
52181 | 428 |
lemma chains_alt_def: "chains A = {C. subset.chain A C}" |
429 |
by (simp add: chains_def chain_subset_alt_def subset.chain_def) |
|
430 |
||
431 |
lemma Chains_subset: |
|
432 |
"Chains r \<subseteq> {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
433 |
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
|
434 |
|
52181 | 435 |
lemma Chains_subset': |
436 |
assumes "refl r" |
|
437 |
shows "{C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C} \<subseteq> Chains r" |
|
438 |
using assms |
|
439 |
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
|
440 |
|
52181 | 441 |
lemma Chains_alt_def: |
442 |
assumes "refl r" |
|
443 |
shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}" |
|
444 |
using assms |
|
445 |
by (metis Chains_subset Chains_subset' subset_antisym) |
|
446 |
||
447 |
lemma Zorn_Lemma: |
|
448 |
"\<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
|
449 |
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
|
450 |
|
52181 | 451 |
lemma Zorn_Lemma2: |
452 |
"\<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" |
|
453 |
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
|
454 |
|
52183
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
455 |
text{*Various other lemmas*} |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
456 |
|
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
457 |
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
|
458 |
by (unfold chains_def chain_subset_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
459 |
|
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
460 |
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
|
461 |
by (unfold chains_def) blast |
667961fa6a60
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua
parents:
52181
diff
changeset
|
462 |
|
52181 | 463 |
lemma Zorns_po_lemma: |
464 |
assumes po: "Partial_order r" |
|
465 |
and u: "\<forall>C\<in>Chains r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a, u) \<in> r" |
|
466 |
shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
467 |
proof - |
|
468 |
have "Preorder r" using po by (simp add: partial_order_on_def) |
|
469 |
--{* Mirror r in the set of subsets below (wrt r) elements of A*} |
|
470 |
let ?B = "%x. r\<inverse> `` {x}" let ?S = "?B ` Field r" |
|
471 |
{ |
|
472 |
fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" |
|
473 |
let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}" |
|
474 |
have "C = ?B ` ?A" using 1 by (auto simp: image_def) |
|
475 |
have "?A \<in> Chains r" |
|
476 |
proof (simp add: Chains_def, intro allI impI, elim conjE) |
|
477 |
fix a b |
|
478 |
assume "a \<in> Field r" and "?B a \<in> C" and "b \<in> Field r" and "?B b \<in> C" |
|
479 |
hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto |
|
480 |
thus "(a, b) \<in> r \<or> (b, a) \<in> r" |
|
481 |
using `Preorder r` and `a \<in> Field r` and `b \<in> Field r` |
|
482 |
by (simp add:subset_Image1_Image1_iff) |
|
483 |
qed |
|
484 |
then obtain u where uA: "u \<in> Field r" "\<forall>a\<in>?A. (a, u) \<in> r" using u by auto |
|
485 |
have "\<forall>A\<in>C. A \<subseteq> r\<inverse> `` {u}" (is "?P u") |
|
486 |
proof auto |
|
487 |
fix a B assume aB: "B \<in> C" "a \<in> B" |
|
488 |
with 1 obtain x where "x \<in> Field r" and "B = r\<inverse> `` {x}" by auto |
|
489 |
thus "(a, u) \<in> r" using uA and aB and `Preorder r` |
|
490 |
by (auto simp add: preorder_on_def refl_on_def) (metis transD) |
|
491 |
qed |
|
492 |
then have "\<exists>u\<in>Field r. ?P u" using `u \<in> Field r` by blast |
|
493 |
} |
|
494 |
then have "\<forall>C\<in>chains ?S. \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U" |
|
495 |
by (auto simp: chains_def chain_subset_def) |
|
496 |
from Zorn_Lemma2 [OF this] |
|
497 |
obtain m B where "m \<in> Field r" and "B = r\<inverse> `` {m}" |
|
498 |
and "\<forall>x\<in>Field r. B \<subseteq> r\<inverse> `` {x} \<longrightarrow> r\<inverse> `` {x} = B" |
|
499 |
by auto |
|
500 |
hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" |
|
501 |
using po and `Preorder r` and `m \<in> Field r` |
|
502 |
by (auto simp: subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff) |
|
503 |
thus ?thesis using `m \<in> Field r` by blast |
|
504 |
qed |
|
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
505 |
|
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
506 |
|
52181 | 507 |
subsection {* The Well Ordering Theorem *} |
26191 | 508 |
|
509 |
(* The initial segment of a relation appears generally useful. |
|
510 |
Move to Relation.thy? |
|
511 |
Definition correct/most general? |
|
512 |
Naming? |
|
513 |
*) |
|
52181 | 514 |
definition init_seg_of :: "(('a \<times> 'a) set \<times> ('a \<times> 'a) set) set" where |
515 |
"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 | 516 |
|
52181 | 517 |
abbreviation |
518 |
initialSegmentOf :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infix "initial'_segment'_of" 55) |
|
519 |
where |
|
520 |
"r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of" |
|
26191 | 521 |
|
52181 | 522 |
lemma refl_on_init_seg_of [simp]: "r initial_segment_of r" |
523 |
by (simp add: init_seg_of_def) |
|
26191 | 524 |
|
525 |
lemma trans_init_seg_of: |
|
526 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t" |
|
52181 | 527 |
by (simp (no_asm_use) add: init_seg_of_def) |
528 |
(metis UnCI Un_absorb2 subset_trans) |
|
26191 | 529 |
|
530 |
lemma antisym_init_seg_of: |
|
52181 | 531 |
"r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s" |
532 |
unfolding init_seg_of_def by safe |
|
26191 | 533 |
|
52181 | 534 |
lemma Chains_init_seg_of_Union: |
535 |
"R \<in> Chains init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R" |
|
536 |
by (auto simp: init_seg_of_def Ball_def Chains_def) blast |
|
26191 | 537 |
|
26272 | 538 |
lemma chain_subset_trans_Union: |
52181 | 539 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans (\<Union>R)" |
540 |
apply (auto simp add: chain_subset_def) |
|
541 |
apply (simp (no_asm_use) add: trans_def) |
|
542 |
apply (metis subsetD) |
|
543 |
done |
|
26191 | 544 |
|
26272 | 545 |
lemma chain_subset_antisym_Union: |
52181 | 546 |
"chain\<^sub>\<subseteq> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym (\<Union>R)" |
547 |
apply (auto simp add: chain_subset_def antisym_def) |
|
548 |
apply (metis subsetD) |
|
549 |
done |
|
26191 | 550 |
|
26272 | 551 |
lemma chain_subset_Total_Union: |
52181 | 552 |
assumes "chain\<^sub>\<subseteq> R" and "\<forall>r\<in>R. Total r" |
553 |
shows "Total (\<Union>R)" |
|
554 |
proof (simp add: total_on_def Ball_def, auto del: disjCI) |
|
555 |
fix r s a b assume A: "r \<in> R" "s \<in> R" "a \<in> Field r" "b \<in> Field s" "a \<noteq> b" |
|
556 |
from `chain\<^sub>\<subseteq> R` and `r \<in> R` and `s \<in> R` have "r \<subseteq> s \<or> s \<subseteq> r" |
|
557 |
by (auto simp add: chain_subset_def) |
|
558 |
thus "(\<exists>r\<in>R. (a, b) \<in> r) \<or> (\<exists>r\<in>R. (b, a) \<in> r)" |
|
26191 | 559 |
proof |
52181 | 560 |
assume "r \<subseteq> s" hence "(a, b) \<in> s \<or> (b, a) \<in> s" using assms(2) A |
561 |
by (simp add: total_on_def) (metis mono_Field subsetD) |
|
562 |
thus ?thesis using `s \<in> R` by blast |
|
26191 | 563 |
next |
52181 | 564 |
assume "s \<subseteq> r" hence "(a, b) \<in> r \<or> (b, a) \<in> r" using assms(2) A |
565 |
by (simp add: total_on_def) (metis mono_Field subsetD) |
|
566 |
thus ?thesis using `r \<in> R` by blast |
|
26191 | 567 |
qed |
568 |
qed |
|
569 |
||
570 |
lemma wf_Union_wf_init_segs: |
|
52181 | 571 |
assumes "R \<in> Chains init_seg_of" and "\<forall>r\<in>R. wf r" |
572 |
shows "wf (\<Union>R)" |
|
573 |
proof(simp add: wf_iff_no_infinite_down_chain, rule ccontr, auto) |
|
574 |
fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f (Suc i), f i) \<in> r" |
|
575 |
then obtain r where "r \<in> R" and "(f (Suc 0), f 0) \<in> r" by auto |
|
576 |
{ fix i have "(f (Suc i), f i) \<in> r" |
|
577 |
proof (induct i) |
|
26191 | 578 |
case 0 show ?case by fact |
579 |
next |
|
580 |
case (Suc i) |
|
52181 | 581 |
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
|
582 |
using 1 by auto |
26191 | 583 |
moreover hence "s initial_segment_of r \<or> r initial_segment_of s" |
52181 | 584 |
using assms(1) `r \<in> R` by (simp add: Chains_def) |
585 |
ultimately show ?case by (simp add: init_seg_of_def) blast |
|
26191 | 586 |
qed |
587 |
} |
|
52181 | 588 |
thus False using assms(2) and `r \<in> R` |
589 |
by (simp add: wf_iff_no_infinite_down_chain) blast |
|
26191 | 590 |
qed |
591 |
||
27476 | 592 |
lemma initial_segment_of_Diff: |
593 |
"p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s" |
|
52181 | 594 |
unfolding init_seg_of_def by blast |
27476 | 595 |
|
52181 | 596 |
lemma Chains_inits_DiffI: |
597 |
"R \<in> Chains init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chains init_seg_of" |
|
598 |
unfolding Chains_def by (blast intro: initial_segment_of_Diff) |
|
26191 | 599 |
|
52181 | 600 |
theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV" |
601 |
proof - |
|
26191 | 602 |
-- {*The initial segment relation on well-orders: *} |
52181 | 603 |
let ?WO = "{r::'a rel. Well_order r}" |
26191 | 604 |
def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO" |
52181 | 605 |
have I_init: "I \<subseteq> init_seg_of" by (auto simp: I_def) |
606 |
hence subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R" |
|
607 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
608 |
have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r" |
|
609 |
by (simp add: Chains_def I_def) blast |
|
610 |
have FI: "Field I = ?WO" by (auto simp add: I_def init_seg_of_def Field_def) |
|
26191 | 611 |
hence 0: "Partial_order I" |
52181 | 612 |
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def |
613 |
trans_def I_def elim!: trans_init_seg_of) |
|
26191 | 614 |
-- {*I-chains have upper bounds in ?WO wrt I: their Union*} |
52181 | 615 |
{ fix R assume "R \<in> Chains I" |
616 |
hence Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast |
|
617 |
have subch: "chain\<^sub>\<subseteq> R" using `R : Chains I` I_init |
|
618 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
619 |
have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" |
|
620 |
and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" |
|
621 |
using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs) |
|
622 |
have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def) |
|
26191 | 623 |
moreover have "trans (\<Union>R)" |
52181 | 624 |
by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`]) |
625 |
moreover have "antisym (\<Union>R)" |
|
626 |
by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`]) |
|
26191 | 627 |
moreover have "Total (\<Union>R)" |
52181 | 628 |
by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`]) |
629 |
moreover have "wf ((\<Union>R) - Id)" |
|
630 |
proof - |
|
631 |
have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast |
|
632 |
with `\<forall>r\<in>R. wf (r - Id)` and wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] |
|
26191 | 633 |
show ?thesis by (simp (no_asm_simp)) blast |
634 |
qed |
|
26295 | 635 |
ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs) |
26191 | 636 |
moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris |
52181 | 637 |
by(simp add: Chains_init_seg_of_Union) |
638 |
ultimately have "\<Union>R \<in> ?WO \<and> (\<forall>r\<in>R. (r, \<Union>R) \<in> I)" |
|
639 |
using mono_Chains [OF I_init] and `R \<in> Chains I` |
|
640 |
by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
|
26191 | 641 |
} |
52181 | 642 |
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 | 643 |
--{*Zorn's Lemma yields a maximal well-order m:*} |
52181 | 644 |
then obtain m::"'a rel" where "Well_order m" and |
645 |
max: "\<forall>r. Well_order r \<and> (m, r) \<in> I \<longrightarrow> r = m" |
|
26191 | 646 |
using Zorns_po_lemma[OF 0 1] by (auto simp:FI) |
647 |
--{*Now show by contradiction that m covers the whole type:*} |
|
648 |
{ fix x::'a assume "x \<notin> Field m" |
|
649 |
--{*We assume that x is not covered and extend m at the top with x*} |
|
650 |
have "m \<noteq> {}" |
|
651 |
proof |
|
52181 | 652 |
assume "m = {}" |
653 |
moreover have "Well_order {(x, x)}" |
|
654 |
by (simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def) |
|
26191 | 655 |
ultimately show False using max |
52181 | 656 |
by (auto simp: I_def init_seg_of_def simp del: Field_insert) |
26191 | 657 |
qed |
658 |
hence "Field m \<noteq> {}" by(auto simp:Field_def) |
|
52181 | 659 |
moreover have "wf (m - Id)" using `Well_order m` |
660 |
by (simp add: well_order_on_def) |
|
26191 | 661 |
--{*The extension of m by x:*} |
52181 | 662 |
let ?s = "{(a, x) | a. a \<in> Field m}" |
663 |
let ?m = "insert (x, x) m \<union> ?s" |
|
26191 | 664 |
have Fm: "Field ?m = insert x (Field m)" |
52181 | 665 |
by (auto simp: Field_def) |
666 |
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" |
|
667 |
using `Well_order m` by (simp_all add: order_on_defs) |
|
26191 | 668 |
--{*We show that the extension is a well-order*} |
52181 | 669 |
have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) |
670 |
moreover have "trans ?m" using `trans m` and `x \<notin> Field m` |
|
671 |
unfolding trans_def Field_def by blast |
|
672 |
moreover have "antisym ?m" using `antisym m` and `x \<notin> Field m` |
|
673 |
unfolding antisym_def Field_def by blast |
|
674 |
moreover have "Total ?m" using `Total m` and Fm by (auto simp: total_on_def) |
|
675 |
moreover have "wf (?m - Id)" |
|
676 |
proof - |
|
26191 | 677 |
have "wf ?s" using `x \<notin> Field m` |
52181 | 678 |
by (auto simp add: wf_eq_minimal Field_def) metis |
679 |
thus ?thesis using `wf (m - Id)` and `x \<notin> Field m` |
|
680 |
wf_subset [OF `wf ?s` Diff_subset] |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
35175
diff
changeset
|
681 |
by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
26191 | 682 |
qed |
52181 | 683 |
ultimately have "Well_order ?m" by (simp add: order_on_defs) |
26191 | 684 |
--{*We show that the extension is above m*} |
52181 | 685 |
moreover hence "(m, ?m) \<in> I" using `Well_order m` and `x \<notin> Field m` |
686 |
by (fastforce simp: I_def init_seg_of_def Field_def) |
|
26191 | 687 |
ultimately |
688 |
--{*This contradicts maximality of m:*} |
|
52181 | 689 |
have False using max and `x \<notin> Field m` unfolding Field_def by blast |
26191 | 690 |
} |
691 |
hence "Field m = UNIV" by auto |
|
26272 | 692 |
moreover with `Well_order m` have "Well_order m" by simp |
693 |
ultimately show ?thesis by blast |
|
694 |
qed |
|
695 |
||
52181 | 696 |
corollary well_order_on: "\<exists>r::'a rel. well_order_on A r" |
26272 | 697 |
proof - |
52181 | 698 |
obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV" |
699 |
using well_ordering [where 'a = "'a"] by blast |
|
700 |
let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" |
|
26272 | 701 |
have 1: "Field ?r = A" using wo univ |
52181 | 702 |
by (fastforce simp: Field_def order_on_defs refl_on_def) |
703 |
have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)" |
|
704 |
using `Well_order r` by (simp_all add: order_on_defs) |
|
705 |
have "Refl ?r" using `Refl r` by (auto simp: refl_on_def 1 univ) |
|
26272 | 706 |
moreover have "trans ?r" using `trans r` |
707 |
unfolding trans_def by blast |
|
708 |
moreover have "antisym ?r" using `antisym r` |
|
709 |
unfolding antisym_def by blast |
|
52181 | 710 |
moreover have "Total ?r" using `Total r` by (simp add:total_on_def 1 univ) |
711 |
moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf (r - Id)`]) blast |
|
712 |
ultimately have "Well_order ?r" by (simp add: order_on_defs) |
|
26295 | 713 |
with 1 show ?thesis by metis |
26191 | 714 |
qed |
715 |
||
52199 | 716 |
subsection {* Extending Well-founded Relations to Well-Orders *} |
717 |
||
718 |
text {*A \emph{downset} (also lower set, decreasing set, initial segment, or |
|
719 |
downward closed set) is closed w.r.t.\ smaller elements.*} |
|
720 |
definition downset_on where |
|
721 |
"downset_on A r = (\<forall>x y. (x, y) \<in> r \<and> y \<in> A \<longrightarrow> x \<in> A)" |
|
722 |
||
723 |
(* |
|
724 |
text {*Connection to order filters of the @{theory Cardinals} theory.*} |
|
725 |
lemma (in wo_rel) ofilter_downset_on_conv: |
|
726 |
"ofilter A \<longleftrightarrow> downset_on A r \<and> A \<subseteq> Field r" |
|
727 |
by (auto simp: downset_on_def ofilter_def under_def) |
|
728 |
*) |
|
729 |
||
730 |
lemma downset_onI: |
|
731 |
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> downset_on A r" |
|
732 |
by (auto simp: downset_on_def) |
|
733 |
||
734 |
lemma downset_onD: |
|
735 |
"downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A" |
|
736 |
by (auto simp: downset_on_def) |
|
737 |
||
738 |
text {*Extensions of relations w.r.t.\ a given set.*} |
|
739 |
definition extension_on where |
|
740 |
"extension_on A r s = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> s \<longrightarrow> (x, y) \<in> r)" |
|
741 |
||
742 |
lemma extension_onI: |
|
743 |
"(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; (x, y) \<in> s\<rbrakk> \<Longrightarrow> (x, y) \<in> r) \<Longrightarrow> extension_on A r s" |
|
744 |
by (auto simp: extension_on_def) |
|
745 |
||
746 |
lemma extension_onD: |
|
747 |
"extension_on A r s \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> s \<Longrightarrow> (x, y) \<in> r" |
|
748 |
by (auto simp: extension_on_def) |
|
749 |
||
750 |
lemma downset_on_Union: |
|
751 |
assumes "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" |
|
752 |
shows "downset_on (Field (\<Union>R)) p" |
|
753 |
using assms by (auto intro: downset_onI dest: downset_onD) |
|
754 |
||
755 |
lemma chain_subset_extension_on_Union: |
|
756 |
assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
|
757 |
shows "extension_on (Field (\<Union>R)) (\<Union>R) p" |
|
758 |
using assms |
|
759 |
by (simp add: chain_subset_def extension_on_def) |
|
760 |
(metis Field_def mono_Field set_mp) |
|
761 |
||
762 |
lemma downset_on_empty [simp]: "downset_on {} p" |
|
763 |
by (auto simp: downset_on_def) |
|
764 |
||
765 |
lemma extension_on_empty [simp]: "extension_on {} p q" |
|
766 |
by (auto simp: extension_on_def) |
|
767 |
||
768 |
text {*Every well-founded relation can be extended to a well-order.*} |
|
769 |
theorem well_order_extension: |
|
770 |
assumes "wf p" |
|
771 |
shows "\<exists>w. p \<subseteq> w \<and> Well_order w" |
|
772 |
proof - |
|
773 |
let ?K = "{r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p}" |
|
774 |
def I \<equiv> "init_seg_of \<inter> ?K \<times> ?K" |
|
775 |
have I_init: "I \<subseteq> init_seg_of" by (simp add: I_def) |
|
776 |
then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R" |
|
777 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
778 |
have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow> |
|
779 |
Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p" |
|
780 |
by (simp add: Chains_def I_def) blast |
|
781 |
have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def) |
|
782 |
then have 0: "Partial_order I" |
|
783 |
by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def |
|
784 |
trans_def I_def elim: trans_init_seg_of) |
|
785 |
{ fix R assume "R \<in> Chains I" |
|
786 |
then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast |
|
787 |
have subch: "chain\<^sub>\<subseteq> R" using `R \<in> Chains I` I_init |
|
788 |
by (auto simp: init_seg_of_def chain_subset_def Chains_def) |
|
789 |
have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and |
|
790 |
"\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" and |
|
791 |
"\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and |
|
792 |
"\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p" |
|
793 |
using Chains_wo [OF `R \<in> Chains I`] by (simp_all add: order_on_defs) |
|
794 |
have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by (auto simp: refl_on_def) |
|
795 |
moreover have "trans (\<Union>R)" |
|
796 |
by (rule chain_subset_trans_Union [OF subch `\<forall>r\<in>R. trans r`]) |
|
797 |
moreover have "antisym (\<Union>R)" |
|
798 |
by (rule chain_subset_antisym_Union [OF subch `\<forall>r\<in>R. antisym r`]) |
|
799 |
moreover have "Total (\<Union>R)" |
|
800 |
by (rule chain_subset_Total_Union [OF subch `\<forall>r\<in>R. Total r`]) |
|
801 |
moreover have "wf ((\<Union>R) - Id)" |
|
802 |
proof - |
|
803 |
have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast |
|
804 |
with `\<forall>r\<in>R. wf (r - Id)` wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]] |
|
805 |
show ?thesis by (simp (no_asm_simp)) blast |
|
806 |
qed |
|
807 |
ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs) |
|
808 |
moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris |
|
809 |
by (simp add: Chains_init_seg_of_Union) |
|
810 |
moreover have "downset_on (Field (\<Union>R)) p" |
|
811 |
by (rule downset_on_Union [OF `\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p`]) |
|
812 |
moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p" |
|
813 |
by (rule chain_subset_extension_on_Union [OF subch `\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p`]) |
|
814 |
ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)" |
|
815 |
using mono_Chains [OF I_init] and `R \<in> Chains I` |
|
816 |
by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo) |
|
817 |
} |
|
818 |
then have 1: "\<forall>R\<in>Chains I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r, u) \<in> I" by (subst FI) blast |
|
819 |
txt {*Zorn's Lemma yields a maximal well-order m.*} |
|
820 |
from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set" |
|
821 |
where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and |
|
822 |
max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and> |
|
823 |
(m, r) \<in> I \<longrightarrow> r = m" |
|
824 |
by (auto simp: FI) |
|
825 |
have "Field p \<subseteq> Field m" |
|
826 |
proof (rule ccontr) |
|
827 |
let ?Q = "Field p - Field m" |
|
828 |
assume "\<not> (Field p \<subseteq> Field m)" |
|
829 |
with assms [unfolded wf_eq_minimal, THEN spec, of ?Q] |
|
830 |
obtain x where "x \<in> Field p" and "x \<notin> Field m" and |
|
831 |
min: "\<forall>y. (y, x) \<in> p \<longrightarrow> y \<notin> ?Q" by blast |
|
832 |
txt {*Add @{term x} as topmost element to @{term m}.*} |
|
833 |
let ?s = "{(y, x) | y. y \<in> Field m}" |
|
834 |
let ?m = "insert (x, x) m \<union> ?s" |
|
835 |
have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def) |
|
836 |
have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" |
|
837 |
using `Well_order m` by (simp_all add: order_on_defs) |
|
838 |
txt {*We show that the extension is a well-order.*} |
|
839 |
have "Refl ?m" using `Refl m` Fm by (auto simp: refl_on_def) |
|
840 |
moreover have "trans ?m" using `trans m` `x \<notin> Field m` |
|
841 |
unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
|
842 |
moreover have "antisym ?m" using `antisym m` `x \<notin> Field m` |
|
843 |
unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast |
|
844 |
moreover have "Total ?m" using `Total m` Fm by (auto simp: Relation.total_on_def) |
|
845 |
moreover have "wf (?m - Id)" |
|
846 |
proof - |
|
847 |
have "wf ?s" using `x \<notin> Field m` |
|
848 |
by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis |
|
849 |
thus ?thesis using `wf (m - Id)` `x \<notin> Field m` |
|
850 |
wf_subset [OF `wf ?s` Diff_subset] |
|
851 |
by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) |
|
852 |
qed |
|
853 |
ultimately have "Well_order ?m" by (simp add: order_on_defs) |
|
854 |
moreover have "extension_on (Field ?m) ?m p" |
|
855 |
using `extension_on (Field m) m p` `downset_on (Field m) p` |
|
856 |
by (subst Fm) (auto simp: extension_on_def dest: downset_onD) |
|
857 |
moreover have "downset_on (Field ?m) p" |
|
858 |
using `downset_on (Field m) p` and min |
|
859 |
by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff) |
|
860 |
moreover have "(m, ?m) \<in> I" |
|
861 |
using `Well_order m` and `Well_order ?m` and |
|
862 |
`downset_on (Field m) p` and `downset_on (Field ?m) p` and |
|
863 |
`extension_on (Field m) m p` and `extension_on (Field ?m) ?m p` and |
|
864 |
`Refl m` and `x \<notin> Field m` |
|
865 |
by (auto simp: I_def init_seg_of_def refl_on_def) |
|
866 |
ultimately |
|
867 |
--{*This contradicts maximality of m:*} |
|
868 |
show False using max and `x \<notin> Field m` unfolding Field_def by blast |
|
869 |
qed |
|
870 |
have "p \<subseteq> m" |
|
871 |
using `Field p \<subseteq> Field m` and `extension_on (Field m) m p` |
|
872 |
by (force simp: Field_def extension_on_def) |
|
873 |
with `Well_order m` show ?thesis by blast |
|
874 |
qed |
|
875 |
||
876 |
text {*Every well-founded relation can be extended to a total well-order.*} |
|
877 |
corollary total_well_order_extension: |
|
878 |
assumes "wf p" |
|
879 |
shows "\<exists>w. p \<subseteq> w \<and> Well_order w \<and> Field w = UNIV" |
|
880 |
proof - |
|
881 |
from well_order_extension [OF assms] obtain w |
|
882 |
where "p \<subseteq> w" and wo: "Well_order w" by blast |
|
883 |
let ?A = "UNIV - Field w" |
|
884 |
from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" .. |
|
885 |
have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp |
|
886 |
have *: "Field w \<inter> Field w' = {}" by simp |
|
887 |
let ?w = "w \<union>o w'" |
|
888 |
have "p \<subseteq> ?w" using `p \<subseteq> w` by (auto simp: Osum_def) |
|
889 |
moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp |
|
890 |
moreover have "Field ?w = UNIV" by (simp add: Field_Osum) |
|
891 |
ultimately show ?thesis by blast |
|
892 |
qed |
|
893 |
||
894 |
corollary well_order_on_extension: |
|
895 |
assumes "wf p" and "Field p \<subseteq> A" |
|
896 |
shows "\<exists>w. p \<subseteq> w \<and> well_order_on A w" |
|
897 |
proof - |
|
898 |
from total_well_order_extension [OF `wf p`] obtain r |
|
899 |
where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast |
|
900 |
let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}" |
|
901 |
from `p \<subseteq> r` have "p \<subseteq> ?r" using `Field p \<subseteq> A` by (auto simp: Field_def) |
|
902 |
have 1: "Field ?r = A" using wo univ |
|
903 |
by (fastforce simp: Field_def order_on_defs refl_on_def) |
|
904 |
have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" |
|
905 |
using `Well_order r` by (simp_all add: order_on_defs) |
|
906 |
have "refl_on A ?r" using `Refl r` by (auto simp: refl_on_def univ) |
|
907 |
moreover have "trans ?r" using `trans r` |
|
908 |
unfolding trans_def by blast |
|
909 |
moreover have "antisym ?r" using `antisym r` |
|
910 |
unfolding antisym_def by blast |
|
911 |
moreover have "total_on A ?r" using `Total r` by (simp add: total_on_def univ) |
|
912 |
moreover have "wf (?r - Id)" by (rule wf_subset [OF `wf(r - Id)`]) blast |
|
913 |
ultimately have "well_order_on A ?r" by (simp add: order_on_defs) |
|
914 |
with `p \<subseteq> ?r` show ?thesis by blast |
|
915 |
qed |
|
916 |
||
13551
b7f64ee8da84
converted Hyperreal/Zorn to Isar format and moved to Library
paulson
parents:
diff
changeset
|
917 |
end |
52181 | 918 |