src/ZF/Zorn.thy
 author wenzelm Sun Nov 09 17:04:14 2014 +0100 (2014-11-09) changeset 58957 c9e744ea8a38 parent 58871 c399ae4b836f child 59788 6f7b6adac439 permissions -rw-r--r--
proper context for match_tac etc.;
1 (*  Title:      ZF/Zorn.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1994  University of Cambridge
4 *)
6 section{*Zorn's Lemma*}
8 theory Zorn imports OrderArith AC Inductive_ZF begin
10 text{*Based upon the unpublished article ``Towards the Mechanization of the
11 Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.*}
13 definition
14   Subset_rel :: "i=>i"  where
15    "Subset_rel(A) == {z \<in> A*A . \<exists>x y. z=<x,y> & x<=y & x\<noteq>y}"
17 definition
18   chain      :: "i=>i"  where
19    "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
21 definition
22   super      :: "[i,i]=>i"  where
23    "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
25 definition
26   maxchain   :: "i=>i"  where
27    "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
29 definition
30   increasing :: "i=>i"  where
31     "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
34 text{*Lemma for the inductive definition below*}
35 lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> \<Union>(Y) \<in> Pow(A)"
36 by blast
39 text{*We could make the inductive definition conditional on
40     @{term "next \<in> increasing(S)"}
41     but instead we make this a side-condition of an introduction rule.  Thus
42     the induction rule lets us assume that condition!  Many inductive proofs
43     are therefore unconditional.*}
44 consts
45   "TFin" :: "[i,i]=>i"
47 inductive
48   domains       "TFin(S,next)" \<subseteq> "Pow(S)"
49   intros
50     nextI:       "[| x \<in> TFin(S,next);  next \<in> increasing(S) |]
51                   ==> next`x \<in> TFin(S,next)"
53     Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> \<Union>(Y) \<in> TFin(S,next)"
55   monos         Pow_mono
56   con_defs      increasing_def
57   type_intros   CollectD1 [THEN apply_funtype] Union_in_Pow
60 subsection{*Mathematical Preamble *}
62 lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)"
63 by blast
65 lemma Inter_lemma0:
66      "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B"
67 by blast
70 subsection{*The Transfinite Construction *}
72 lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
73 apply (unfold increasing_def)
74 apply (erule CollectD1)
75 done
77 lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x"
78 by (unfold increasing_def, blast)
80 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
82 lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]
85 text{*Structural induction on @{term "TFin(S,next)"} *}
86 lemma TFin_induct:
87   "[| n \<in> TFin(S,next);
88       !!x. [| x \<in> TFin(S,next);  P(x);  next \<in> increasing(S) |] ==> P(next`x);
89       !!Y. [| Y \<subseteq> TFin(S,next);  \<forall>y\<in>Y. P(y) |] ==> P(\<Union>(Y))
90    |] ==> P(n)"
91 by (erule TFin.induct, blast+)
94 subsection{*Some Properties of the Transfinite Construction *}
96 lemmas increasing_trans = subset_trans [OF _ increasingD2,
97                                         OF _ _ TFin_is_subset]
99 text{*Lemma 1 of section 3.1*}
100 lemma TFin_linear_lemma1:
101      "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);
102          \<forall>x \<in> TFin(S,next) . x<=m \<longrightarrow> x=m | next`x<=m |]
103       ==> n<=m | next`m<=n"
104 apply (erule TFin_induct)
105 apply (erule_tac  Union_lemma0) (*or just Blast_tac*)
106 (*downgrade subsetI from intro! to intro*)
107 apply (blast dest: increasing_trans)
108 done
110 text{*Lemma 2 of section 3.2.  Interesting in its own right!
111   Requires @{term "next \<in> increasing(S)"} in the second induction step.*}
112 lemma TFin_linear_lemma2:
113     "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
114      ==> \<forall>n \<in> TFin(S,next). n<=m \<longrightarrow> n=m | next`n \<subseteq> m"
115 apply (erule TFin_induct)
116 apply (rule impI [THEN ballI])
117 txt{*case split using @{text TFin_linear_lemma1}*}
118 apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
119        assumption+)
120 apply (blast del: subsetI
121              intro: increasing_trans subsetI, blast)
122 txt{*second induction step*}
123 apply (rule impI [THEN ballI])
124 apply (rule Union_lemma0 [THEN disjE])
125 apply (erule_tac  disjI2)
126 prefer 2 apply blast
127 apply (rule ballI)
128 apply (drule bspec, assumption)
129 apply (drule subsetD, assumption)
130 apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
131        assumption+, blast)
132 apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
133 apply (blast dest: TFin_is_subset)+
134 done
136 text{*a more convenient form for Lemma 2*}
137 lemma TFin_subsetD:
138      "[| n<=m;  m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
139       ==> n=m | next`n \<subseteq> m"
140 by (blast dest: TFin_linear_lemma2 [rule_format])
142 text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
143 lemma TFin_subset_linear:
144      "[| m \<in> TFin(S,next);  n \<in> TFin(S,next);  next \<in> increasing(S) |]
145       ==> n \<subseteq> m | m<=n"
146 apply (rule disjE)
147 apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
148 apply (assumption+, erule disjI2)
149 apply (blast del: subsetI
150              intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset)
151 done
154 text{*Lemma 3 of section 3.3*}
155 lemma equal_next_upper:
156      "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n \<subseteq> m"
157 apply (erule TFin_induct)
158 apply (drule TFin_subsetD)
159 apply (assumption+, force, blast)
160 done
162 text{*Property 3.3 of section 3.3*}
163 lemma equal_next_Union:
164      "[| m \<in> TFin(S,next);  next \<in> increasing(S) |]
165       ==> m = next`m <-> m = \<Union>(TFin(S,next))"
166 apply (rule iffI)
167 apply (rule Union_upper [THEN equalityI])
168 apply (rule_tac  equal_next_upper [THEN Union_least])
169 apply (assumption+)
170 apply (erule ssubst)
171 apply (rule increasingD2 [THEN equalityI], assumption)
172 apply (blast del: subsetI
173              intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
174 done
177 subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain*}
179 text{*NOTE: We assume the partial ordering is @{text "\<subseteq>"}, the subset
180 relation!*}
182 text{** Defining the "next" operation for Hausdorff's Theorem **}
184 lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
185 apply (unfold chain_def)
186 apply (rule Collect_subset)
187 done
189 lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
190 apply (unfold super_def)
191 apply (rule Collect_subset)
192 done
194 lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
195 apply (unfold maxchain_def)
196 apply (rule Collect_subset)
197 done
199 lemma choice_super:
200      "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
201       ==> ch ` super(S,X) \<in> super(S,X)"
202 apply (erule apply_type)
203 apply (unfold super_def maxchain_def, blast)
204 done
206 lemma choice_not_equals:
207      "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
208       ==> ch ` super(S,X) \<noteq> X"
209 apply (rule notI)
210 apply (drule choice_super, assumption, assumption)
211 apply (simp add: super_def)
212 done
214 text{*This justifies Definition 4.4*}
215 lemma Hausdorff_next_exists:
216      "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
217       \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
218                    next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
219 apply (rule_tac x="\<lambda>X\<in>Pow(S).
220                    if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
221        in bexI)
222 apply force
223 apply (unfold increasing_def)
224 apply (rule CollectI)
225 apply (rule lam_type)
226 apply (simp (no_asm_simp))
227 apply (blast dest: super_subset_chain [THEN subsetD]
228                    chain_subset_Pow [THEN subsetD] choice_super)
229 txt{*Now, verify that it increases*}
230 apply (simp (no_asm_simp) add: Pow_iff subset_refl)
231 apply safe
232 apply (drule choice_super)
233 apply (assumption+)
234 apply (simp add: super_def, blast)
235 done
237 text{*Lemma 4*}
238 lemma TFin_chain_lemma4:
239      "[| c \<in> TFin(S,next);
240          ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
241          next \<in> increasing(S);
242          \<forall>X \<in> Pow(S). next`X =
243                           if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
244      ==> c \<in> chain(S)"
245 apply (erule TFin_induct)
246 apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
247             choice_super [THEN super_subset_chain [THEN subsetD]])
248 apply (unfold chain_def)
249 apply (rule CollectI, blast, safe)
250 apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+)
251       txt{*@{text "Blast_tac's"} slow*}
252 done
254 theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)"
255 apply (rule AC_Pi_Pow [THEN exE])
256 apply (rule Hausdorff_next_exists [THEN bexE], assumption)
257 apply (rename_tac ch "next")
258 apply (subgoal_tac "\<Union>(TFin (S,next)) \<in> chain (S) ")
259 prefer 2
260  apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI])
261 apply (rule_tac x = "\<Union>(TFin (S,next))" in exI)
262 apply (rule classical)
263 apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))")
264 apply (rule_tac  equal_next_Union [THEN iffD2, symmetric])
265 apply (rule_tac  subset_refl [THEN TFin_UnionI])
266 prefer 2 apply assumption
267 apply (rule_tac  refl)
268 apply (simp add: subset_refl [THEN TFin_UnionI,
269                               THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
270 apply (erule choice_not_equals [THEN notE])
271 apply (assumption+)
272 done
275 subsection{*Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
276        then S contains a Maximal Element*}
278 text{*Used in the proof of Zorn's Lemma*}
279 lemma chain_extend:
280     "[| c \<in> chain(A);  z \<in> A;  \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)"
281 by (unfold chain_def, blast)
283 lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
284 apply (rule Hausdorff [THEN exE])
285 apply (simp add: maxchain_def)
286 apply (rename_tac c)
287 apply (rule_tac x = "\<Union>(c)" in bexI)
288 prefer 2 apply blast
289 apply safe
290 apply (rename_tac z)
291 apply (rule classical)
292 apply (subgoal_tac "cons (z,c) \<in> super (S,c) ")
293 apply (blast elim: equalityE)
294 apply (unfold super_def, safe)
295 apply (fast elim: chain_extend)
296 apply (fast elim: equalityE)
297 done
299 text {* Alternative version of Zorn's Lemma *}
301 theorem Zorn2:
302   "\<forall>c \<in> chain(S). \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z"
303 apply (cut_tac Hausdorff maxchain_subset_chain)
304 apply (erule exE)
305 apply (drule subsetD, assumption)
306 apply (drule bspec, assumption, erule bexE)
307 apply (rule_tac x = y in bexI)
308   prefer 2 apply assumption
309 apply clarify
310 apply rule apply assumption
311 apply rule
312 apply (rule ccontr)
313 apply (frule_tac z=z in chain_extend)
314   apply (assumption, blast)
315 apply (unfold maxchain_def super_def)
316 apply (blast elim!: equalityCE)
317 done
320 subsection{*Zermelo's Theorem: Every Set can be Well-Ordered*}
322 text{*Lemma 5*}
323 lemma TFin_well_lemma5:
324      "[| n \<in> TFin(S,next);  Z \<subseteq> TFin(S,next);  z:Z;  ~ \<Inter>(Z) \<in> Z |]
325       ==> \<forall>m \<in> Z. n \<subseteq> m"
326 apply (erule TFin_induct)
327 prefer 2 apply blast txt{*second induction step is easy*}
328 apply (rule ballI)
329 apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
330 apply (subgoal_tac "m = \<Inter>(Z) ")
331 apply blast+
332 done
334 text{*Well-ordering of @{term "TFin(S,next)"} *}
335 lemma well_ord_TFin_lemma: "[| Z \<subseteq> TFin(S,next);  z \<in> Z |] ==> \<Inter>(Z) \<in> Z"
336 apply (rule classical)
337 apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}")
338 apply (simp (no_asm_simp) add: Inter_singleton)
339 apply (erule equal_singleton)
340 apply (rule Union_upper [THEN equalityI])
341 apply (rule_tac  subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
342 done
344 text{*This theorem just packages the previous result*}
345 lemma well_ord_TFin:
346      "next \<in> increasing(S)
347       ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))"
348 apply (rule well_ordI)
349 apply (unfold Subset_rel_def linear_def)
350 txt{*Prove the well-foundedness goal*}
351 apply (rule wf_onI)
352 apply (frule well_ord_TFin_lemma, assumption)
353 apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption)
354 apply blast
355 txt{*Now prove the linearity goal*}
356 apply (intro ballI)
357 apply (case_tac "x=y")
358  apply blast
359 txt{*The @{term "x\<noteq>y"} case remains*}
360 apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
361        assumption+, blast+)
362 done
364 text{** Defining the "next" operation for Zermelo's Theorem **}
366 lemma choice_Diff:
367      "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
368 apply (erule apply_type)
369 apply (blast elim!: equalityE)
370 done
372 text{*This justifies Definition 6.1*}
373 lemma Zermelo_next_exists:
374      "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
375            \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
376                       next`X = (if X=S then S else cons(ch`(S-X), X))"
377 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
378        in bexI)
379 apply force
380 apply (unfold increasing_def)
381 apply (rule CollectI)
382 apply (rule lam_type)
383 txt{*Type checking is surprisingly hard!*}
384 apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
385 apply (blast intro!: choice_Diff [THEN DiffD1])
386 txt{*Verify that it increases*}
387 apply (intro allI impI)
388 apply (simp add: Pow_iff subset_consI subset_refl)
389 done
392 text{*The construction of the injection*}
393 lemma choice_imp_injection:
394      "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
395          next \<in> increasing(S);
396          \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
397       ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
398                \<in> inj(S, TFin(S,next) - {S})"
399 apply (rule_tac d = "%y. ch` (S-y) " in lam_injective)
400 apply (rule DiffI)
401 apply (rule Collect_subset [THEN TFin_UnionI])
402 apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE)
403 apply (subgoal_tac "x \<notin> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
404 prefer 2 apply (blast elim: equalityE)
405 apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S")
406 prefer 2 apply (blast elim: equalityE)
407 txt{*For proving @{text "x \<in> next`\<Union>(...)"}.
408   Abrial and Laffitte's justification appears to be faulty.*}
409 apply (subgoal_tac "~ next ` Union({y \<in> TFin (S,next) . x \<notin> y})
410                     \<subseteq> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ")
411  prefer 2
412  apply (simp del: Union_iff
413              add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]
414              Pow_iff cons_subset_iff subset_refl choice_Diff [THEN DiffD2])
415 apply (subgoal_tac "x \<in> next ` Union({y \<in> TFin (S,next) . x \<notin> y}) ")
416  prefer 2
417  apply (blast intro!: Collect_subset [THEN TFin_UnionI] TFin.nextI)
418 txt{*End of the lemmas!*}
419 apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
420 done
422 text{*The wellordering theorem*}
423 theorem AC_well_ord: "\<exists>r. well_ord(S,r)"
424 apply (rule AC_Pi_Pow [THEN exE])
425 apply (rule Zermelo_next_exists [THEN bexE], assumption)
426 apply (rule exI)
427 apply (rule well_ord_rvimage)
428 apply (erule_tac  well_ord_TFin)
429 apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
430 done
433 subsection {* Zorn's Lemma for Partial Orders *}
435 text {* Reimported from HOL by Clemens Ballarin. *}
438 definition Chain :: "i => i" where
439   "Chain(r) = {A \<in> Pow(field(r)). \<forall>a\<in>A. \<forall>b\<in>A. <a, b> \<in> r | <b, a> \<in> r}"
441 lemma mono_Chain:
442   "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
443   unfolding Chain_def
444   by blast
446 theorem Zorn_po:
447   assumes po: "Partial_order(r)"
448     and u: "\<forall>C\<in>Chain(r). \<exists>u\<in>field(r). \<forall>a\<in>C. <a, u> \<in> r"
449   shows "\<exists>m\<in>field(r). \<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
450 proof -
451   have "Preorder(r)" using po by (simp add: partial_order_on_def)
452   --{* Mirror r in the set of subsets below (wrt r) elements of A (?). *}
453   let ?B = "\<lambda>x\<in>field(r). r -`` {x}" let ?S = "?B `` field(r)"
454   have "\<forall>C\<in>chain(?S). \<exists>U\<in>?S. \<forall>A\<in>C. A \<subseteq> U"
455   proof (clarsimp simp: chain_def Subset_rel_def bex_image_simp)
456     fix C
457     assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B | B \<subseteq> A"
458     let ?A = "{x \<in> field(r). \<exists>M\<in>C. M = ?B`x}"
459     have "C = ?B `` ?A" using 1
460       apply (auto simp: image_def)
461       apply rule
462       apply rule
463       apply (drule subsetD) apply assumption
464       apply (erule CollectE)
465       apply rule apply assumption
466       apply (erule bexE)
467       apply rule prefer 2 apply assumption
468       apply rule
469       apply (erule lamE) apply simp
470       apply assumption
472       apply (thin_tac "C \<subseteq> ?X")
473       apply (fast elim: lamE)
474       done
475     have "?A \<in> Chain(r)"
476     proof (simp add: Chain_def subsetI, intro conjI ballI impI)
477       fix a b
478       assume "a \<in> field(r)" "r -`` {a} \<in> C" "b \<in> field(r)" "r -`` {b} \<in> C"
479       hence "r -`` {a} \<subseteq> r -`` {b} | r -`` {b} \<subseteq> r -`` {a}" using 2 by auto
480       then show "<a, b> \<in> r | <b, a> \<in> r"
481         using `Preorder(r)` `a \<in> field(r)` `b \<in> field(r)`
482         by (simp add: subset_vimage1_vimage1_iff)
483     qed
484     then obtain u where uA: "u \<in> field(r)" "\<forall>a\<in>?A. <a, u> \<in> r"
485       using u
486       apply auto
487       apply (drule bspec) apply assumption
488       apply auto
489       done
490     have "\<forall>A\<in>C. A \<subseteq> r -`` {u}"
491     proof (auto intro!: vimageI)
492       fix a B
493       assume aB: "B \<in> C" "a \<in> B"
494       with 1 obtain x where "x \<in> field(r)" "B = r -`` {x}"
495         apply -
496         apply (drule subsetD) apply assumption
497         apply (erule imageE)
498         apply (erule lamE)
499         apply simp
500         done
501       then show "<a, u> \<in> r" using uA aB `Preorder(r)`
502         by (auto simp: preorder_on_def refl_def) (blast dest: trans_onD)+
503     qed
504     then show "\<exists>U\<in>field(r). \<forall>A\<in>C. A \<subseteq> r -`` {U}"
505       using `u \<in> field(r)` ..
506   qed
507   from Zorn2 [OF this]
508   obtain m B where "m \<in> field(r)" "B = r -`` {m}"
509     "\<forall>x\<in>field(r). B \<subseteq> r -`` {x} \<longrightarrow> B = r -`` {x}"
510     by (auto elim!: lamE simp: ball_image_simp)
511   then have "\<forall>a\<in>field(r). <m, a> \<in> r \<longrightarrow> a = m"
512     using po `Preorder(r)` `m \<in> field(r)`
513     by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff)
514   then show ?thesis using `m \<in> field(r)` by blast
515 qed
517 end