1(* Title: ZF/Zorn.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1994 University of Cambridge 4*) 5 6section\<open>Zorn's Lemma\<close> 7 8theory Zorn imports OrderArith AC Inductive begin 9 10text\<open>Based upon the unpublished article ``Towards the Mechanization of the 11Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close> 12 13definition 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}" 16 17definition 18 chain :: "i=>i" where 19 "chain(A) == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}" 20 21definition 22 super :: "[i,i]=>i" where 23 "super(A,c) == {d \<in> chain(A). c<=d & c\<noteq>d}" 24 25definition 26 maxchain :: "i=>i" where 27 "maxchain(A) == {c \<in> chain(A). super(A,c)=0}" 28 29definition 30 increasing :: "i=>i" where 31 "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}" 32 33 34text\<open>Lemma for the inductive definition below\<close> 35lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> \<Union>(Y) \<in> Pow(A)" 36by blast 37 38 39text\<open>We could make the inductive definition conditional on 40 \<^term>\<open>next \<in> increasing(S)\<close> 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.\<close> 44consts 45 "TFin" :: "[i,i]=>i" 46 47inductive 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)" 52 53 Pow_UnionI: "Y \<in> Pow(TFin(S,next)) ==> \<Union>(Y) \<in> TFin(S,next)" 54 55 monos Pow_mono 56 con_defs increasing_def 57 type_intros CollectD1 [THEN apply_funtype] Union_in_Pow 58 59 60subsection\<open>Mathematical Preamble\<close> 61 62lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)" 63by blast 64 65lemma Inter_lemma0: 66 "[| c \<in> C; \<forall>x\<in>C. A<=x | x<=B |] ==> A \<subseteq> \<Inter>(C) | \<Inter>(C) \<subseteq> B" 67by blast 68 69 70subsection\<open>The Transfinite Construction\<close> 71 72lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)" 73apply (unfold increasing_def) 74apply (erule CollectD1) 75done 76 77lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x" 78by (unfold increasing_def, blast) 79 80lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI] 81 82lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD] 83 84 85text\<open>Structural induction on \<^term>\<open>TFin(S,next)\<close>\<close> 86lemma 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)" 91by (erule TFin.induct, blast+) 92 93 94subsection\<open>Some Properties of the Transfinite Construction\<close> 95 96lemmas increasing_trans = subset_trans [OF _ increasingD2, 97 OF _ _ TFin_is_subset] 98 99text\<open>Lemma 1 of section 3.1\<close> 100lemma 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" 104apply (erule TFin_induct) 105apply (erule_tac [2] Union_lemma0) (*or just Blast_tac*) 106(*downgrade subsetI from intro! to intro*) 107apply (blast dest: increasing_trans) 108done 109 110text\<open>Lemma 2 of section 3.2. Interesting in its own right! 111 Requires \<^term>\<open>next \<in> increasing(S)\<close> in the second induction step.\<close> 112lemma 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" 115apply (erule TFin_induct) 116apply (rule impI [THEN ballI]) 117txt\<open>case split using \<open>TFin_linear_lemma1\<close>\<close> 118apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 119 assumption+) 120apply (blast del: subsetI 121 intro: increasing_trans subsetI, blast) 122txt\<open>second induction step\<close> 123apply (rule impI [THEN ballI]) 124apply (rule Union_lemma0 [THEN disjE]) 125apply (erule_tac [3] disjI2) 126prefer 2 apply blast 127apply (rule ballI) 128apply (drule bspec, assumption) 129apply (drule subsetD, assumption) 130apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE], 131 assumption+, blast) 132apply (erule increasingD2 [THEN subset_trans, THEN disjI1]) 133apply (blast dest: TFin_is_subset)+ 134done 135 136text\<open>a more convenient form for Lemma 2\<close> 137lemma 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" 140by (blast dest: TFin_linear_lemma2 [rule_format]) 141 142text\<open>Consequences from section 3.3 -- Property 3.2, the ordering is total\<close> 143lemma TFin_subset_linear: 144 "[| m \<in> TFin(S,next); n \<in> TFin(S,next); next \<in> increasing(S) |] 145 ==> n \<subseteq> m | m<=n" 146apply (rule disjE) 147apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2]) 148apply (assumption+, erule disjI2) 149apply (blast del: subsetI 150 intro: subsetI increasingD2 [THEN subset_trans] TFin_is_subset) 151done 152 153 154text\<open>Lemma 3 of section 3.3\<close> 155lemma equal_next_upper: 156 "[| n \<in> TFin(S,next); m \<in> TFin(S,next); m = next`m |] ==> n \<subseteq> m" 157apply (erule TFin_induct) 158apply (drule TFin_subsetD) 159apply (assumption+, force, blast) 160done 161 162text\<open>Property 3.3 of section 3.3\<close> 163lemma equal_next_Union: 164 "[| m \<in> TFin(S,next); next \<in> increasing(S) |] 165 ==> m = next`m <-> m = \<Union>(TFin(S,next))" 166apply (rule iffI) 167apply (rule Union_upper [THEN equalityI]) 168apply (rule_tac [2] equal_next_upper [THEN Union_least]) 169apply (assumption+) 170apply (erule ssubst) 171apply (rule increasingD2 [THEN equalityI], assumption) 172apply (blast del: subsetI 173 intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+ 174done 175 176 177subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close> 178 179text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset 180relation!\<close> 181 182text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close> 183 184lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)" 185apply (unfold chain_def) 186apply (rule Collect_subset) 187done 188 189lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)" 190apply (unfold super_def) 191apply (rule Collect_subset) 192done 193 194lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)" 195apply (unfold maxchain_def) 196apply (rule Collect_subset) 197done 198 199lemma choice_super: 200 "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |] 201 ==> ch ` super(S,X) \<in> super(S,X)" 202apply (erule apply_type) 203apply (unfold super_def maxchain_def, blast) 204done 205 206lemma choice_not_equals: 207 "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S); X \<notin> maxchain(S) |] 208 ==> ch ` super(S,X) \<noteq> X" 209apply (rule notI) 210apply (drule choice_super, assumption, assumption) 211apply (simp add: super_def) 212done 213 214text\<open>This justifies Definition 4.4\<close> 215lemma Hausdorff_next_exists: 216 "ch \<in> (\<Prod>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)" 219apply (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) 222apply force 223apply (unfold increasing_def) 224apply (rule CollectI) 225apply (rule lam_type) 226apply (simp (no_asm_simp)) 227apply (blast dest: super_subset_chain [THEN subsetD] 228 chain_subset_Pow [THEN subsetD] choice_super) 229txt\<open>Now, verify that it increases\<close> 230apply (simp (no_asm_simp) add: Pow_iff subset_refl) 231apply safe 232apply (drule choice_super) 233apply (assumption+) 234apply (simp add: super_def, blast) 235done 236 237text\<open>Lemma 4\<close> 238lemma TFin_chain_lemma4: 239 "[| c \<in> TFin(S,next); 240 ch \<in> (\<Prod>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)" 245apply (erule TFin_induct) 246apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD] 247 choice_super [THEN super_subset_chain [THEN subsetD]]) 248apply (unfold chain_def) 249apply (rule CollectI, blast, safe) 250apply (rule_tac m1=B and n1=Ba in TFin_subset_linear [THEN disjE], fast+) 251 txt\<open>\<open>Blast_tac's\<close> slow\<close> 252done 253 254theorem Hausdorff: "\<exists>c. c \<in> maxchain(S)" 255apply (rule AC_Pi_Pow [THEN exE]) 256apply (rule Hausdorff_next_exists [THEN bexE], assumption) 257apply (rename_tac ch "next") 258apply (subgoal_tac "\<Union>(TFin (S,next)) \<in> chain (S) ") 259prefer 2 260 apply (blast intro!: TFin_chain_lemma4 subset_refl [THEN TFin_UnionI]) 261apply (rule_tac x = "\<Union>(TFin (S,next))" in exI) 262apply (rule classical) 263apply (subgoal_tac "next ` Union(TFin (S,next)) = \<Union>(TFin (S,next))") 264apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric]) 265apply (rule_tac [2] subset_refl [THEN TFin_UnionI]) 266prefer 2 apply assumption 267apply (rule_tac [2] refl) 268apply (simp add: subset_refl [THEN TFin_UnionI, 269 THEN TFin.dom_subset [THEN subsetD, THEN PowD]]) 270apply (erule choice_not_equals [THEN notE]) 271apply (assumption+) 272done 273 274 275subsection\<open>Zorn's Lemma: If All Chains in S Have Upper Bounds In S, 276 then S contains a Maximal Element\<close> 277 278text\<open>Used in the proof of Zorn's Lemma\<close> 279lemma chain_extend: 280 "[| c \<in> chain(A); z \<in> A; \<forall>x \<in> c. x<=z |] ==> cons(z,c) \<in> chain(A)" 281by (unfold chain_def, blast) 282 283lemma Zorn: "\<forall>c \<in> chain(S). \<Union>(c) \<in> S ==> \<exists>y \<in> S. \<forall>z \<in> S. y<=z \<longrightarrow> y=z" 284apply (rule Hausdorff [THEN exE]) 285apply (simp add: maxchain_def) 286apply (rename_tac c) 287apply (rule_tac x = "\<Union>(c)" in bexI) 288prefer 2 apply blast 289apply safe 290apply (rename_tac z) 291apply (rule classical) 292apply (subgoal_tac "cons (z,c) \<in> super (S,c) ") 293apply (blast elim: equalityE) 294apply (unfold super_def, safe) 295apply (fast elim: chain_extend) 296apply (fast elim: equalityE) 297done 298 299text \<open>Alternative version of Zorn's Lemma\<close> 300 301theorem 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" 303apply (cut_tac Hausdorff maxchain_subset_chain) 304apply (erule exE) 305apply (drule subsetD, assumption) 306apply (drule bspec, assumption, erule bexE) 307apply (rule_tac x = y in bexI) 308 prefer 2 apply assumption 309apply clarify 310apply rule apply assumption 311apply rule 312apply (rule ccontr) 313apply (frule_tac z=z in chain_extend) 314 apply (assumption, blast) 315apply (unfold maxchain_def super_def) 316apply (blast elim!: equalityCE) 317done 318 319 320subsection\<open>Zermelo's Theorem: Every Set can be Well-Ordered\<close> 321 322text\<open>Lemma 5\<close> 323lemma 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" 326apply (erule TFin_induct) 327prefer 2 apply blast txt\<open>second induction step is easy\<close> 328apply (rule ballI) 329apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto) 330apply (subgoal_tac "m = \<Inter>(Z) ") 331apply blast+ 332done 333 334text\<open>Well-ordering of \<^term>\<open>TFin(S,next)\<close>\<close> 335lemma well_ord_TFin_lemma: "[| Z \<subseteq> TFin(S,next); z \<in> Z |] ==> \<Inter>(Z) \<in> Z" 336apply (rule classical) 337apply (subgoal_tac "Z = {\<Union>(TFin (S,next))}") 338apply (simp (no_asm_simp) add: Inter_singleton) 339apply (erule equal_singleton) 340apply (rule Union_upper [THEN equalityI]) 341apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+) 342done 343 344text\<open>This theorem just packages the previous result\<close> 345lemma well_ord_TFin: 346 "next \<in> increasing(S) 347 ==> well_ord(TFin(S,next), Subset_rel(TFin(S,next)))" 348apply (rule well_ordI) 349apply (unfold Subset_rel_def linear_def) 350txt\<open>Prove the well-foundedness goal\<close> 351apply (rule wf_onI) 352apply (frule well_ord_TFin_lemma, assumption) 353apply (drule_tac x = "\<Inter>(Z) " in bspec, assumption) 354apply blast 355txt\<open>Now prove the linearity goal\<close> 356apply (intro ballI) 357apply (case_tac "x=y") 358 apply blast 359txt\<open>The \<^term>\<open>x\<noteq>y\<close> case remains\<close> 360apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE], 361 assumption+, blast+) 362done 363 364text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close> 365 366lemma choice_Diff: 367 "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X); X \<subseteq> S; X\<noteq>S |] ==> ch ` (S-X) \<in> S-X" 368apply (erule apply_type) 369apply (blast elim!: equalityE) 370done 371 372text\<open>This justifies Definition 6.1\<close> 373lemma Zermelo_next_exists: 374 "ch \<in> (\<Prod>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))" 377apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)" 378 in bexI) 379apply force 380apply (unfold increasing_def) 381apply (rule CollectI) 382apply (rule lam_type) 383txt\<open>Type checking is surprisingly hard!\<close> 384apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl) 385apply (blast intro!: choice_Diff [THEN DiffD1]) 386txt\<open>Verify that it increases\<close> 387apply (intro allI impI) 388apply (simp add: Pow_iff subset_consI subset_refl) 389done 390 391 392text\<open>The construction of the injection\<close> 393lemma choice_imp_injection: 394 "[| ch \<in> (\<Prod>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})" 399apply (rule_tac d = "%y. ch` (S-y) " in lam_injective) 400apply (rule DiffI) 401apply (rule Collect_subset [THEN TFin_UnionI]) 402apply (blast intro!: Collect_subset [THEN TFin_UnionI] elim: equalityE) 403apply (subgoal_tac "x \<notin> \<Union>({y \<in> TFin (S,next) . x \<notin> y}) ") 404prefer 2 apply (blast elim: equalityE) 405apply (subgoal_tac "\<Union>({y \<in> TFin (S,next) . x \<notin> y}) \<noteq> S") 406prefer 2 apply (blast elim: equalityE) 407txt\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>. 408 Abrial and Laffitte's justification appears to be faulty.\<close> 409apply (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]) 415apply (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) 418txt\<open>End of the lemmas!\<close> 419apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset]) 420done 421 422text\<open>The wellordering theorem\<close> 423theorem AC_well_ord: "\<exists>r. well_ord(S,r)" 424apply (rule AC_Pi_Pow [THEN exE]) 425apply (rule Zermelo_next_exists [THEN bexE], assumption) 426apply (rule exI) 427apply (rule well_ord_rvimage) 428apply (erule_tac [2] well_ord_TFin) 429apply (rule choice_imp_injection [THEN inj_weaken_type], blast+) 430done 431 432 433subsection \<open>Zorn's Lemma for Partial Orders\<close> 434 435text \<open>Reimported from HOL by Clemens Ballarin.\<close> 436 437 438definition 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}" 440 441lemma mono_Chain: 442 "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)" 443 unfolding Chain_def 444 by blast 445 446theorem 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" 450proof - 451 have "Preorder(r)" using po by (simp add: partial_order_on_def) 452 \<comment> \<open>Mirror r in the set of subsets below (wrt r) elements of A (?).\<close> 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 471 472 apply (thin_tac "C \<subseteq> X" for 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 \<open>Preorder(r)\<close> \<open>a \<in> field(r)\<close> \<open>b \<in> field(r)\<close> 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 \<open>Preorder(r)\<close> 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 \<open>u \<in> field(r)\<close> .. 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 \<open>Preorder(r)\<close> \<open>m \<in> field(r)\<close> 513 by (auto simp: subset_vimage1_vimage1_iff Partial_order_eq_vimage1_vimage1_iff) 514 then show ?thesis using \<open>m \<in> field(r)\<close> by blast 515qed 516 517end 518