src/HOL/Library/Zorn.thy
author nipkow
Sun Mar 02 15:02:06 2008 +0100 (2008-03-02)
changeset 26191 ae537f315b34
parent 25691 8f8d83af100a
child 26272 d63776c3be97
permissions -rw-r--r--
Generalized Zorn and added well-ordering theorem
     1 (*  Title       : HOL/Library/Zorn.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot, Tobias Nipkow
     4     Description : Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF)
     5                   The well-ordering theorem
     6 *)
     7 
     8 header {* Zorn's Lemma *}
     9 
    10 theory Zorn
    11 imports ATP_Linkup Hilbert_Choice
    12 begin
    13 
    14 text{*
    15   The lemma and section numbers refer to an unpublished article
    16   \cite{Abrial-Laffitte}.
    17 *}
    18 
    19 definition
    20   chain     ::  "'a set set => 'a set set set" where
    21   "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    22 
    23 definition
    24   super     ::  "['a set set,'a set set] => 'a set set set" where
    25   "super S c = {d. d \<in> chain S & c \<subset> d}"
    26 
    27 definition
    28   maxchain  ::  "'a set set => 'a set set set" where
    29   "maxchain S = {c. c \<in> chain S & super S c = {}}"
    30 
    31 definition
    32   succ      ::  "['a set set,'a set set] => 'a set set" where
    33   "succ S c =
    34     (if c \<notin> chain S | c \<in> maxchain S
    35     then c else SOME c'. c' \<in> super S c)"
    36 
    37 inductive_set
    38   TFin :: "'a set set => 'a set set set"
    39   for S :: "'a set set"
    40   where
    41     succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    42   | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    43   monos          Pow_mono
    44 
    45 
    46 subsection{*Mathematical Preamble*}
    47 
    48 lemma Union_lemma0:
    49     "(\<forall>x \<in> C. x \<subseteq> A | B \<subseteq> x) ==> Union(C) \<subseteq> A | B \<subseteq> Union(C)"
    50   by blast
    51 
    52 
    53 text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
    54 
    55 lemma Abrial_axiom1: "x \<subseteq> succ S x"
    56   apply (unfold succ_def)
    57   apply (rule split_if [THEN iffD2])
    58   apply (auto simp add: super_def maxchain_def psubset_def)
    59   apply (rule contrapos_np, assumption)
    60   apply (rule someI2, blast+)
    61   done
    62 
    63 lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
    64 
    65 lemma TFin_induct:
    66           "[| n \<in> TFin S;
    67              !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
    68              !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
    69           ==> P(n)"
    70   apply (induct set: TFin)
    71    apply blast+
    72   done
    73 
    74 lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
    75   apply (erule subset_trans)
    76   apply (rule Abrial_axiom1)
    77   done
    78 
    79 text{*Lemma 1 of section 3.1*}
    80 lemma TFin_linear_lemma1:
    81      "[| n \<in> TFin S;  m \<in> TFin S;
    82          \<forall>x \<in> TFin S. x \<subseteq> m --> x = m | succ S x \<subseteq> m
    83       |] ==> n \<subseteq> m | succ S m \<subseteq> n"
    84   apply (erule TFin_induct)
    85    apply (erule_tac [2] Union_lemma0)
    86   apply (blast del: subsetI intro: succ_trans)
    87   done
    88 
    89 text{* Lemma 2 of section 3.2 *}
    90 lemma TFin_linear_lemma2:
    91      "m \<in> TFin S ==> \<forall>n \<in> TFin S. n \<subseteq> m --> n=m | succ S n \<subseteq> m"
    92   apply (erule TFin_induct)
    93    apply (rule impI [THEN ballI])
    94    txt{*case split using @{text TFin_linear_lemma1}*}
    95    apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    96      assumption+)
    97     apply (drule_tac x = n in bspec, assumption)
    98     apply (blast del: subsetI intro: succ_trans, blast)
    99   txt{*second induction step*}
   100   apply (rule impI [THEN ballI])
   101   apply (rule Union_lemma0 [THEN disjE])
   102     apply (rule_tac [3] disjI2)
   103     prefer 2 apply blast
   104    apply (rule ballI)
   105    apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
   106      assumption+, auto)
   107   apply (blast intro!: Abrial_axiom1 [THEN subsetD])
   108   done
   109 
   110 text{*Re-ordering the premises of Lemma 2*}
   111 lemma TFin_subsetD:
   112      "[| n \<subseteq> m;  m \<in> TFin S;  n \<in> TFin S |] ==> n=m | succ S n \<subseteq> m"
   113   by (rule TFin_linear_lemma2 [rule_format])
   114 
   115 text{*Consequences from section 3.3 -- Property 3.2, the ordering is total*}
   116 lemma TFin_subset_linear: "[| m \<in> TFin S;  n \<in> TFin S|] ==> n \<subseteq> m | m \<subseteq> n"
   117   apply (rule disjE)
   118     apply (rule TFin_linear_lemma1 [OF _ _TFin_linear_lemma2])
   119       apply (assumption+, erule disjI2)
   120   apply (blast del: subsetI
   121     intro: subsetI Abrial_axiom1 [THEN subset_trans])
   122   done
   123 
   124 text{*Lemma 3 of section 3.3*}
   125 lemma eq_succ_upper: "[| n \<in> TFin S;  m \<in> TFin S;  m = succ S m |] ==> n \<subseteq> m"
   126   apply (erule TFin_induct)
   127    apply (drule TFin_subsetD)
   128      apply (assumption+, force, blast)
   129   done
   130 
   131 text{*Property 3.3 of section 3.3*}
   132 lemma equal_succ_Union: "m \<in> TFin S ==> (m = succ S m) = (m = Union(TFin S))"
   133   apply (rule iffI)
   134    apply (rule Union_upper [THEN equalityI])
   135     apply assumption
   136    apply (rule eq_succ_upper [THEN Union_least], assumption+)
   137   apply (erule ssubst)
   138   apply (rule Abrial_axiom1 [THEN equalityI])
   139   apply (blast del: subsetI intro: subsetI TFin_UnionI TFin.succI)
   140   done
   141 
   142 subsection{*Hausdorff's Theorem: Every Set Contains a Maximal Chain.*}
   143 
   144 text{*NB: We assume the partial ordering is @{text "\<subseteq>"},
   145  the subset relation!*}
   146 
   147 lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
   148   by (unfold chain_def) auto
   149 
   150 lemma super_subset_chain: "super S c \<subseteq> chain S"
   151   by (unfold super_def) blast
   152 
   153 lemma maxchain_subset_chain: "maxchain S \<subseteq> chain S"
   154   by (unfold maxchain_def) blast
   155 
   156 lemma mem_super_Ex: "c \<in> chain S - maxchain S ==> EX d. d \<in> super S c"
   157   by (unfold super_def maxchain_def) auto
   158 
   159 lemma select_super:
   160      "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
   161   apply (erule mem_super_Ex [THEN exE])
   162   apply (rule someI2, auto)
   163   done
   164 
   165 lemma select_not_equals:
   166      "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
   167   apply (rule notI)
   168   apply (drule select_super)
   169   apply (simp add: super_def psubset_def)
   170   done
   171 
   172 lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
   173   by (unfold succ_def) (blast intro!: if_not_P)
   174 
   175 lemma succ_not_equals: "c \<in> chain S - maxchain S ==> succ S c \<noteq> c"
   176   apply (frule succI3)
   177   apply (simp (no_asm_simp))
   178   apply (rule select_not_equals, assumption)
   179   done
   180 
   181 lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
   182   apply (erule TFin_induct)
   183    apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
   184   apply (unfold chain_def)
   185   apply (rule CollectI, safe)
   186    apply (drule bspec, assumption)
   187    apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
   188      blast+)
   189   done
   190 
   191 theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   192   apply (rule_tac x = "Union (TFin S)" in exI)
   193   apply (rule classical)
   194   apply (subgoal_tac "succ S (Union (TFin S)) = Union (TFin S) ")
   195    prefer 2
   196    apply (blast intro!: TFin_UnionI equal_succ_Union [THEN iffD2, symmetric])
   197   apply (cut_tac subset_refl [THEN TFin_UnionI, THEN TFin_chain_lemma4])
   198   apply (drule DiffI [THEN succ_not_equals], blast+)
   199   done
   200 
   201 
   202 subsection{*Zorn's Lemma: If All Chains Have Upper Bounds Then
   203                                There Is  a Maximal Element*}
   204 
   205 lemma chain_extend:
   206     "[| c \<in> chain S; z \<in> S;
   207         \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
   208   by (unfold chain_def) blast
   209 
   210 lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
   211   by (unfold chain_def) auto
   212 
   213 lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
   214   by (unfold chain_def) auto
   215 
   216 lemma maxchain_Zorn:
   217      "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
   218   apply (rule ccontr)
   219   apply (simp add: maxchain_def)
   220   apply (erule conjE)
   221   apply (subgoal_tac "({u} Un c) \<in> super S c")
   222    apply simp
   223   apply (unfold super_def psubset_def)
   224   apply (blast intro: chain_extend dest: chain_Union_upper)
   225   done
   226 
   227 theorem Zorn_Lemma:
   228     "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
   229   apply (cut_tac Hausdorff maxchain_subset_chain)
   230   apply (erule exE)
   231   apply (drule subsetD, assumption)
   232   apply (drule bspec, assumption)
   233   apply (rule_tac x = "Union(c)" in bexI)
   234    apply (rule ballI, rule impI)
   235    apply (blast dest!: maxchain_Zorn, assumption)
   236   done
   237 
   238 subsection{*Alternative version of Zorn's Lemma*}
   239 
   240 lemma Zorn_Lemma2:
   241   "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   242     ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   243   apply (cut_tac Hausdorff maxchain_subset_chain)
   244   apply (erule exE)
   245   apply (drule subsetD, assumption)
   246   apply (drule bspec, assumption, erule bexE)
   247   apply (rule_tac x = y in bexI)
   248    prefer 2 apply assumption
   249   apply clarify
   250   apply (rule ccontr)
   251   apply (frule_tac z = x in chain_extend)
   252     apply (assumption, blast)
   253   apply (unfold maxchain_def super_def psubset_def)
   254   apply (blast elim!: equalityCE)
   255   done
   256 
   257 text{*Various other lemmas*}
   258 
   259 lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   260   by (unfold chain_def) blast
   261 
   262 lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   263   by (unfold chain_def) blast
   264 
   265 
   266 (* FIXME into Relation.thy *)
   267 
   268 lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   269 by(auto simp:Field_def Domain_def Range_def)
   270 
   271 lemma Field_empty[simp]: "Field {} = {}"
   272 by(auto simp:Field_def)
   273 
   274 lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r"
   275 by(auto simp:Field_def)
   276 
   277 lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s"
   278 by(auto simp:Field_def)
   279 
   280 lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
   281 by(auto simp:Field_def)
   282 
   283 lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   284 by blast
   285 
   286 lemma Range_converse[simp]: "Range(r^-1) = Domain r"
   287 by blast
   288 
   289 lemma Field_converse[simp]: "Field(r^-1) = Field r"
   290 by(auto simp:Field_def)
   291 
   292 lemma reflexive_reflcl[simp]: "reflexive(r^=)"
   293 by(simp add:refl_def)
   294 
   295 lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
   296 by(simp add:antisym_def)
   297 
   298 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
   299 unfolding trans_def by blast
   300 
   301 (*********************************************************)
   302 
   303 (* Define globally? In Set.thy?
   304    Use in def of chain at the beginning *)
   305 definition "subset_chain C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
   306 
   307 (* Define globally? In Relation.thy? *)
   308 definition Chain :: "('a*'a)set \<Rightarrow> 'a set set" where
   309 "Chain r \<equiv> {A. \<forall>a\<in>A.\<forall>b\<in>A. (a,b) : r \<or> (b,a) \<in> r}"
   310 
   311 lemma mono_Chain: "r \<subseteq> s \<Longrightarrow> Chain r \<subseteq> Chain s"
   312 unfolding Chain_def by blast
   313 
   314 (* Are the following definitions the "right" ones?
   315 
   316 Key point: should the set appear as an explicit argument,
   317 (as currently in "refl A r") or should it remain implicitly the Field
   318 (as in Refl below)? I use refl/Refl merely to illusrate the point.
   319 
   320 The notation "refl A r" is closer to the usual (A,<=) in the literature
   321 whereas "Refl r" is shorter and avoids naming the set.
   322 Note that "refl A r \<Longrightarrow> A = Field r & Refl r" and "Refl r \<Longrightarrow> refl (Field r) r"
   323 This makes the A look redundant.
   324 
   325 A slight advantage of having the A around is that one can write "a:A"
   326 rather than "a:Field r". A disavantage is the multiple occurrences of
   327 "refl (Field r) r" (etc) in the proof of the well-ordering thm.
   328 
   329 I propose to move the definitions into Main, either as they are or
   330 with an additional A argument.
   331 
   332 Naming: The capital letters were chosen to distinguish them from
   333 versions on the whole type we have (eg reflexive) or may want to have
   334 (eg preorder). In case of an additional A argument one could append
   335 "_on" to distinguish the relativized versions.
   336 *)
   337 
   338 definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
   339 definition "Preorder r \<equiv> Refl r \<and> trans r"
   340 definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
   341 definition "Total r \<equiv> \<forall>x\<in>Field r.\<forall>y\<in>Field r. x\<noteq>y \<longrightarrow> (x,y)\<in>r \<or> (y,x)\<in>r"
   342 definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
   343 definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
   344 
   345 lemmas Order_defs =
   346   Preorder_def Partial_order_def Linear_order_def Well_order_def
   347 
   348 lemma Refl_empty[simp]: "Refl {}"
   349 by(simp add:Refl_def)
   350 lemma Preorder_empty[simp]: "Preorder {}"
   351 by(simp add:Preorder_def trans_def)
   352 lemma Partial_order_empty[simp]: "Partial_order {}"
   353 by(simp add:Partial_order_def)
   354 lemma Total_empty[simp]: "Total {}"
   355 by(simp add:Total_def)
   356 lemma Linear_order_empty[simp]: "Linear_order {}"
   357 by(simp add:Linear_order_def)
   358 lemma Well_order_empty[simp]: "Well_order {}"
   359 by(simp add:Well_order_def)
   360 
   361 lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
   362 by(simp add:Refl_def)
   363 
   364 lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
   365 by (simp add:Preorder_def)
   366 
   367 lemma Partial_order_converse[simp]:
   368   "Partial_order (r^-1) = Partial_order r"
   369 by (simp add: Partial_order_def)
   370 
   371 lemma subset_Image_Image_iff:
   372   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
   373    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
   374 apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
   375 apply metis
   376 by(metis trans_def)
   377 
   378 lemma subset_Image1_Image1_iff:
   379   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
   380 by(simp add:subset_Image_Image_iff)
   381 
   382 lemma Refl_antisym_eq_Image1_Image1_iff:
   383   "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   384 by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
   385   metis
   386 
   387 lemma Partial_order_eq_Image1_Image1_iff:
   388   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   389 by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)
   390 
   391 text{* Zorn's lemma for partial orders: *}
   392 
   393 lemma Zorns_po_lemma:
   394 assumes po: "Partial_order r" and u: "\<forall>C\<in>Chain r. \<exists>u\<in>Field r. \<forall>a\<in>C. (a,u):r"
   395 shows "\<exists>m\<in>Field r. \<forall>a\<in>Field r. (m,a):r \<longrightarrow> a=m"
   396 proof-
   397   have "Preorder r" using po by(simp add:Partial_order_def)
   398 --{* Mirror r in the set of subsets below (wrt r) elements of A*}
   399   let ?B = "%x. r^-1 `` {x}" let ?S = "?B ` Field r"
   400   have "\<forall>C \<in> chain ?S. EX U:?S. ALL A:C. A\<subseteq>U"
   401   proof (auto simp:chain_def)
   402     fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C.\<forall>B\<in>C. A\<subseteq>B | B\<subseteq>A"
   403     let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
   404     have "C = ?B ` ?A" using 1 by(auto simp: image_def)
   405     have "?A\<in>Chain r"
   406     proof (simp add:Chain_def, intro allI impI, elim conjE)
   407       fix a b
   408       assume "a \<in> Field r" "?B a \<in> C" "b \<in> Field r" "?B b \<in> C"
   409       hence "?B a \<subseteq> ?B b \<or> ?B b \<subseteq> ?B a" using 2 by auto
   410       thus "(a, b) \<in> r \<or> (b, a) \<in> r" using `Preorder r` `a:Field r` `b:Field r`
   411 	by(simp add:subset_Image1_Image1_iff)
   412     qed
   413     then obtain u where uA: "u:Field r" "\<forall>a\<in>?A. (a,u) : r" using u by auto
   414     have "\<forall>A\<in>C. A \<subseteq> r^-1 `` {u}" (is "?P u")
   415     proof auto
   416       fix a B assume aB: "B:C" "a:B"
   417       with 1 obtain x where "x:Field r" "B = r^-1 `` {x}" by auto
   418       thus "(a,u) : r" using uA aB `Preorder r`
   419 	by (auto simp add: Preorder_def Refl_def) (metis transD)
   420     qed
   421     thus "EX u:Field r. ?P u" using `u:Field r` by blast
   422   qed
   423   from Zorn_Lemma2[OF this]
   424   obtain m B where "m:Field r" "B = r^-1 `` {m}"
   425     "\<forall>x\<in>Field r. B \<subseteq> r^-1 `` {x} \<longrightarrow> B = r^-1 `` {x}"
   426     by(auto simp:image_def) blast
   427   hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" using po `Preorder r` `m:Field r`
   428     by(auto simp:subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
   429   thus ?thesis using `m:Field r` by blast
   430 qed
   431 
   432 (* The initial segment of a relation appears generally useful.
   433    Move to Relation.thy?
   434    Definition correct/most general?
   435    Naming?
   436 *)
   437 definition init_seg_of :: "(('a*'a)set * ('a*'a)set)set" where
   438 "init_seg_of == {(r,s). r \<subseteq> s \<and> (\<forall>a b c. (a,b):s \<and> (b,c):r \<longrightarrow> (a,b):r)}"
   439 
   440 abbreviation initialSegmentOf :: "('a*'a)set \<Rightarrow> ('a*'a)set \<Rightarrow> bool"
   441              (infix "initial'_segment'_of" 55) where
   442 "r initial_segment_of s == (r,s):init_seg_of"
   443 
   444 lemma refl_init_seg_of[simp]: "r initial_segment_of r"
   445 by(simp add:init_seg_of_def)
   446 
   447 lemma trans_init_seg_of:
   448   "r initial_segment_of s \<Longrightarrow> s initial_segment_of t \<Longrightarrow> r initial_segment_of t"
   449 by(simp (no_asm_use) add: init_seg_of_def)
   450   (metis Domain_iff UnCI Un_absorb2 subset_trans)
   451 
   452 lemma antisym_init_seg_of:
   453   "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r=s"
   454 by(auto simp:init_seg_of_def)
   455 
   456 lemma Chain_init_seg_of_Union:
   457   "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   458 by(auto simp add:init_seg_of_def Chain_def Ball_def) blast
   459 
   460 lemma subset_chain_trans_Union:
   461   "subset_chain R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
   462 apply(auto simp add:subset_chain_def)
   463 apply(simp (no_asm_use) add:trans_def)
   464 apply (metis subsetD)
   465 done
   466 
   467 lemma subset_chain_antisym_Union:
   468   "subset_chain R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
   469 apply(auto simp add:subset_chain_def antisym_def)
   470 apply (metis subsetD)
   471 done
   472 
   473 lemma subset_chain_Total_Union:
   474 assumes "subset_chain R" "\<forall>r\<in>R. Total r"
   475 shows "Total (\<Union>R)"
   476 proof (simp add: Total_def Ball_def, auto del:disjCI)
   477   fix r s a b assume A: "r:R" "s:R" "a:Field r" "b:Field s" "a\<noteq>b"
   478   from `subset_chain R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
   479     by(simp add:subset_chain_def)
   480   thus "(\<exists>r\<in>R. (a,b) \<in> r) \<or> (\<exists>r\<in>R. (b,a) \<in> r)"
   481   proof
   482     assume "r\<subseteq>s" hence "(a,b):s \<or> (b,a):s" using assms(2) A
   483       by(simp add:Total_def)(metis mono_Field subsetD)
   484     thus ?thesis using `s:R` by blast
   485   next
   486     assume "s\<subseteq>r" hence "(a,b):r \<or> (b,a):r" using assms(2) A
   487       by(simp add:Total_def)(metis mono_Field subsetD)
   488     thus ?thesis using `r:R` by blast
   489   qed
   490 qed
   491 
   492 lemma wf_Union_wf_init_segs:
   493 assumes "R \<in> Chain init_seg_of" and "\<forall>r\<in>R. wf r" shows "wf(\<Union>R)"
   494 proof(simp add:wf_iff_no_infinite_down_chain, rule ccontr, auto)
   495   fix f assume 1: "\<forall>i. \<exists>r\<in>R. (f(Suc i), f i) \<in> r"
   496   then obtain r where "r:R" and "(f(Suc 0), f 0) : r" by auto
   497   { fix i have "(f(Suc i), f i) \<in> r"
   498     proof(induct i)
   499       case 0 show ?case by fact
   500     next
   501       case (Suc i)
   502       moreover obtain s where "s\<in>R" and "(f(Suc(Suc i)), f(Suc i)) \<in> s"
   503 	using 1 by auto
   504       moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
   505 	using assms(1) `r:R` by(simp add: Chain_def)
   506       ultimately show ?case by(simp add:init_seg_of_def) blast
   507     qed
   508   }
   509   thus False using assms(2) `r:R`
   510     by(simp add:wf_iff_no_infinite_down_chain) blast
   511 qed
   512 
   513 lemma Chain_inits_DiffI:
   514   "R \<in> Chain init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chain init_seg_of"
   515 apply(auto simp:Chain_def init_seg_of_def)
   516 apply (metis subsetD)
   517 apply (metis subsetD)
   518 done
   519 
   520 theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r"
   521 proof-
   522 -- {*The initial segment relation on well-orders: *}
   523   let ?WO = "{r::('a*'a)set. Well_order r}"
   524   def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
   525   have I_init: "I \<subseteq> init_seg_of" by(auto simp:I_def)
   526   hence subch: "!!R. R : Chain I \<Longrightarrow> subset_chain R"
   527     by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   528   have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
   529     by(simp add:Chain_def I_def) blast
   530   have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   531   hence 0: "Partial_order I"
   532     by(auto simp add: Partial_order_def Preorder_def antisym_def antisym_init_seg_of Refl_def trans_def I_def)(metis trans_init_seg_of)
   533 -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   534   { fix R assume "R \<in> Chain I"
   535     hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
   536     have subch: "subset_chain R" using `R : Chain I` I_init
   537       by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   538     have "\<forall>r\<in>R. Refl r" "\<forall>r\<in>R. trans r" "\<forall>r\<in>R. antisym r" "\<forall>r\<in>R. Total r"
   539          "\<forall>r\<in>R. wf(r-Id)"
   540       using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:Order_defs)
   541     have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:Refl_def)
   542     moreover have "trans (\<Union>R)"
   543       by(rule subset_chain_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   544     moreover have "antisym(\<Union>R)"
   545       by(rule subset_chain_antisym_Union[OF subch `\<forall>r\<in>R. antisym r`])
   546     moreover have "Total (\<Union>R)"
   547       by(rule subset_chain_Total_Union[OF subch `\<forall>r\<in>R. Total r`])
   548     moreover have "wf((\<Union>R)-Id)"
   549     proof-
   550       have "(\<Union>R)-Id = \<Union>{r-Id|r. r \<in> R}" by blast
   551       with `\<forall>r\<in>R. wf(r-Id)` wf_Union_wf_init_segs[OF Chain_inits_DiffI[OF Ris]]
   552       show ?thesis by (simp (no_asm_simp)) blast
   553     qed
   554     ultimately have "Well_order (\<Union>R)" by(simp add:Order_defs)
   555     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris
   556       by(simp add: Chain_init_seg_of_Union)
   557     ultimately have "\<Union>R : ?WO \<and> (\<forall>r\<in>R. (r,\<Union>R) : I)"
   558       using mono_Chain[OF I_init] `R \<in> Chain I`
   559       by(simp (no_asm) add:I_def del:Field_Union)(metis Chain_wo subsetD)
   560   }
   561   hence 1: "\<forall>R \<in> Chain I. \<exists>u\<in>Field I. \<forall>r\<in>R. (r,u) : I" by (subst FI) blast
   562 --{*Zorn's Lemma yields a maximal well-order m:*}
   563   then obtain m::"('a*'a)set" where "Well_order m" and
   564     max: "\<forall>r. Well_order r \<and> (m,r):I \<longrightarrow> r=m"
   565     using Zorns_po_lemma[OF 0 1] by (auto simp:FI)
   566 --{*Now show by contradiction that m covers the whole type:*}
   567   { fix x::'a assume "x \<notin> Field m"
   568 --{*We assume that x is not covered and extend m at the top with x*}
   569     have "m \<noteq> {}"
   570     proof
   571       assume "m={}"
   572       moreover have "Well_order {(x,x)}"
   573 	by(simp add:Order_defs Refl_def trans_def antisym_def Total_def Field_def Domain_def Range_def)
   574       ultimately show False using max
   575 	by (auto simp:I_def init_seg_of_def simp del:Field_insert)
   576     qed
   577     hence "Field m \<noteq> {}" by(auto simp:Field_def)
   578     moreover have "wf(m-Id)" using `Well_order m` by(simp add:Well_order_def)
   579 --{*The extension of m by x:*}
   580     let ?s = "{(a,x)|a. a : Field m}" let ?m = "insert (x,x) m Un ?s"
   581     have Fm: "Field ?m = insert x (Field m)"
   582       apply(simp add:Field_insert Field_Un)
   583       unfolding Field_def by auto
   584     have "Refl m" "trans m" "antisym m" "Total m" "wf(m-Id)"
   585       using `Well_order m` by(simp_all add:Order_defs)
   586 --{*We show that the extension is a well-order*}
   587     have "Refl ?m" using `Refl m` Fm by(auto simp:Refl_def)
   588     moreover have "trans ?m" using `trans m` `x \<notin> Field m`
   589       unfolding trans_def Field_def Domain_def Range_def by blast
   590     moreover have "antisym ?m" using `antisym m` `x \<notin> Field m`
   591       unfolding antisym_def Field_def Domain_def Range_def by blast
   592     moreover have "Total ?m" using `Total m` Fm by(auto simp: Total_def)
   593     moreover have "wf(?m-Id)"
   594     proof-
   595       have "wf ?s" using `x \<notin> Field m`
   596 	by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
   597       thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
   598 	wf_subset[OF `wf ?s` Diff_subset]
   599 	by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
   600     qed
   601     ultimately have "Well_order ?m" by(simp add:Order_defs)
   602 --{*We show that the extension is above m*}
   603     moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
   604       by(fastsimp simp:I_def init_seg_of_def Field_def Domain_def Range_def)
   605     ultimately
   606 --{*This contradicts maximality of m:*}
   607     have False using max `x \<notin> Field m` unfolding Field_def by blast
   608   }
   609   hence "Field m = UNIV" by auto
   610   with `Well_order m` have "Well_order m" by simp
   611   thus ?thesis ..
   612 qed
   613 
   614 end