src/ZF/Zorn.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 61980 6b780867d426
child 67443 3abf6a722518
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      ZF/Zorn.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1994  University of Cambridge
     4 *)
     5 
     6 section\<open>Zorn's Lemma\<close>
     7 
     8 theory Zorn imports OrderArith AC Inductive_ZF begin
     9 
    10 text\<open>Based upon the unpublished article ``Towards the Mechanization of the
    11 Proofs of Some Classical Theorems of Set Theory,'' by Abrial and Laffitte.\<close>
    12 
    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}"
    16 
    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}"
    20 
    21 definition
    22   super      :: "[i,i]=>i"  where
    23    "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
    24 
    25 definition
    26   maxchain   :: "i=>i"  where
    27    "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
    28 
    29 definition
    30   increasing :: "i=>i"  where
    31     "increasing(A) == {f \<in> Pow(A)->Pow(A). \<forall>x. x<=A \<longrightarrow> x<=f`x}"
    32 
    33 
    34 text\<open>Lemma for the inductive definition below\<close>
    35 lemma Union_in_Pow: "Y \<in> Pow(Pow(A)) ==> \<Union>(Y) \<in> Pow(A)"
    36 by blast
    37 
    38 
    39 text\<open>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.\<close>
    44 consts
    45   "TFin" :: "[i,i]=>i"
    46 
    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)"
    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 
    60 subsection\<open>Mathematical Preamble\<close>
    61 
    62 lemma Union_lemma0: "(\<forall>x\<in>C. x<=A | B<=x) ==> \<Union>(C)<=A | B<=\<Union>(C)"
    63 by blast
    64 
    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
    68 
    69 
    70 subsection\<open>The Transfinite Construction\<close>
    71 
    72 lemma increasingD1: "f \<in> increasing(A) ==> f \<in> Pow(A)->Pow(A)"
    73 apply (unfold increasing_def)
    74 apply (erule CollectD1)
    75 done
    76 
    77 lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x \<subseteq> f`x"
    78 by (unfold increasing_def, blast)
    79 
    80 lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
    81 
    82 lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]
    83 
    84 
    85 text\<open>Structural induction on @{term "TFin(S,next)"}\<close>
    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+)
    92 
    93 
    94 subsection\<open>Some Properties of the Transfinite Construction\<close>
    95 
    96 lemmas increasing_trans = subset_trans [OF _ increasingD2,
    97                                         OF _ _ TFin_is_subset]
    98 
    99 text\<open>Lemma 1 of section 3.1\<close>
   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 [2] Union_lemma0) (*or just Blast_tac*)
   106 (*downgrade subsetI from intro! to intro*)
   107 apply (blast dest: increasing_trans)
   108 done
   109 
   110 text\<open>Lemma 2 of section 3.2.  Interesting in its own right!
   111   Requires @{term "next \<in> increasing(S)"} in the second induction step.\<close>
   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\<open>case split using \<open>TFin_linear_lemma1\<close>\<close>
   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\<open>second induction step\<close>
   123 apply (rule impI [THEN ballI])
   124 apply (rule Union_lemma0 [THEN disjE])
   125 apply (erule_tac [3] 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
   135 
   136 text\<open>a more convenient form for Lemma 2\<close>
   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])
   141 
   142 text\<open>Consequences from section 3.3 -- Property 3.2, the ordering is total\<close>
   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
   152 
   153 
   154 text\<open>Lemma 3 of section 3.3\<close>
   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
   161 
   162 text\<open>Property 3.3 of section 3.3\<close>
   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 [2] 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
   175 
   176 
   177 subsection\<open>Hausdorff's Theorem: Every Set Contains a Maximal Chain\<close>
   178 
   179 text\<open>NOTE: We assume the partial ordering is \<open>\<subseteq>\<close>, the subset
   180 relation!\<close>
   181 
   182 text\<open>* Defining the "next" operation for Hausdorff's Theorem *\<close>
   183 
   184 lemma chain_subset_Pow: "chain(A) \<subseteq> Pow(A)"
   185 apply (unfold chain_def)
   186 apply (rule Collect_subset)
   187 done
   188 
   189 lemma super_subset_chain: "super(A,c) \<subseteq> chain(A)"
   190 apply (unfold super_def)
   191 apply (rule Collect_subset)
   192 done
   193 
   194 lemma maxchain_subset_chain: "maxchain(A) \<subseteq> chain(A)"
   195 apply (unfold maxchain_def)
   196 apply (rule Collect_subset)
   197 done
   198 
   199 lemma 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)"
   202 apply (erule apply_type)
   203 apply (unfold super_def maxchain_def, blast)
   204 done
   205 
   206 lemma 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"
   209 apply (rule notI)
   210 apply (drule choice_super, assumption, assumption)
   211 apply (simp add: super_def)
   212 done
   213 
   214 text\<open>This justifies Definition 4.4\<close>
   215 lemma 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)"
   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\<open>Now, verify that it increases\<close>
   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
   236 
   237 text\<open>Lemma 4\<close>
   238 lemma 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)"
   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\<open>\<open>Blast_tac's\<close> slow\<close>
   252 done
   253 
   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 [2] equal_next_Union [THEN iffD2, symmetric])
   265 apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
   266 prefer 2 apply assumption
   267 apply (rule_tac [2] 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
   273 
   274 
   275 subsection\<open>Zorn's Lemma: If All Chains in S Have Upper Bounds In S,
   276        then S contains a Maximal Element\<close>
   277 
   278 text\<open>Used in the proof of Zorn's Lemma\<close>
   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)
   282 
   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
   298 
   299 text \<open>Alternative version of Zorn's Lemma\<close>
   300 
   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
   318 
   319 
   320 subsection\<open>Zermelo's Theorem: Every Set can be Well-Ordered\<close>
   321 
   322 text\<open>Lemma 5\<close>
   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\<open>second induction step is easy\<close>
   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
   333 
   334 text\<open>Well-ordering of @{term "TFin(S,next)"}\<close>
   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 [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
   342 done
   343 
   344 text\<open>This theorem just packages the previous result\<close>
   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\<open>Prove the well-foundedness goal\<close>
   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\<open>Now prove the linearity goal\<close>
   356 apply (intro ballI)
   357 apply (case_tac "x=y")
   358  apply blast
   359 txt\<open>The @{term "x\<noteq>y"} case remains\<close>
   360 apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
   361        assumption+, blast+)
   362 done
   363 
   364 text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
   365 
   366 lemma choice_Diff:
   367      "[| ch \<in> (\<Prod>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
   371 
   372 text\<open>This justifies Definition 6.1\<close>
   373 lemma 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))"
   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\<open>Type checking is surprisingly hard!\<close>
   384 apply (simp (no_asm_simp) add: Pow_iff cons_subset_iff subset_refl)
   385 apply (blast intro!: choice_Diff [THEN DiffD1])
   386 txt\<open>Verify that it increases\<close>
   387 apply (intro allI impI)
   388 apply (simp add: Pow_iff subset_consI subset_refl)
   389 done
   390 
   391 
   392 text\<open>The construction of the injection\<close>
   393 lemma 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})"
   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\<open>For proving \<open>x \<in> next`\<Union>(...)\<close>.
   408   Abrial and Laffitte's justification appears to be faulty.\<close>
   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\<open>End of the lemmas!\<close>
   419 apply (simp add: Collect_subset [THEN TFin_UnionI, THEN TFin_is_subset])
   420 done
   421 
   422 text\<open>The wellordering theorem\<close>
   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 [2] well_ord_TFin)
   429 apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
   430 done
   431 
   432 
   433 subsection \<open>Zorn's Lemma for Partial Orders\<close>
   434 
   435 text \<open>Reimported from HOL by Clemens Ballarin.\<close>
   436 
   437 
   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}"
   440 
   441 lemma mono_Chain:
   442   "r \<subseteq> s ==> Chain(r) \<subseteq> Chain(s)"
   443   unfolding Chain_def
   444   by blast
   445 
   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   \<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
   515 qed
   516 
   517 end