src/HOL/Library/Zorn.thy
 author Andreas Lochbihler Fri Sep 20 10:09:16 2013 +0200 (2013-09-20) changeset 53745 788730ab7da4 parent 53374 a14d2a854c02 child 54482 a2874c8b3558 permissions -rw-r--r--
prefer Code.abort over code_abort
     1 (*  Title:      HOL/Library/Zorn.thy

     2     Author:     Jacques D. Fleuriot

     3     Author:     Tobias Nipkow, TUM

     4     Author:     Christian Sternagel, JAIST

     5

     6 Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).

     7 The well-ordering theorem.

     8 The extension of any well-founded relation to a well-order.

     9 *)

    10

    11 header {* Zorn's Lemma *}

    12

    13 theory Zorn

    14 imports Order_Union

    15 begin

    16

    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+

   103

   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   then have "suc X \<subseteq> A" unfolding chain_def by blast

   124   with * 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

   136

   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

   195

   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

   241

   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.)*}

   296

   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 .

   339

   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 from ** have "C \<subset> ?C" using \<Union>C \<subseteq> X by auto

   353   ultimately show False using * by blast

   354 qed

   355

   356 subsubsection {* Zorn's lemma *}

   357

   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

   401

   402

   403 subsection {* Zorn's Lemma for Partial Orders *}

   404

   405 text {*Relate old to new definitions.*}

   406

   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)"

   410

   411 definition chains :: "'a set set \<Rightarrow> 'a set set set" where

   412   "chains A = {C. C \<subseteq> A \<and> chain\<^sub>\<subseteq> C}"

   413

   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}"

   417

   418 lemma chains_extend:

   419   "[| c \<in> chains S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chains S"

   420   by (unfold chains_def chain_subset_def) blast

   421

   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)

   427

   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)

   434

   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)

   440

   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"

   449   using subset_Zorn' [of A] by (force simp: chains_alt_def)

   450

   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)

   454

   455 text{*Various other lemmas*}

   456

   457 lemma chainsD: "[| c \<in> chains S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"

   458 by (unfold chains_def chain_subset_def) blast

   459

   460 lemma chainsD2: "!!(c :: 'a set set). c \<in> chains S ==> c \<subseteq> S"

   461 by (unfold chains_def) blast

   462

   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

   505

   506

   507 subsection {* The Well Ordering Theorem *}

   508

   509 (* The initial segment of a relation appears generally useful.

   510    Move to Relation.thy?

   511    Definition correct/most general?

   512    Naming?

   513 *)

   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)}"

   516

   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"

   521

   522 lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"

   523   by (simp add: init_seg_of_def)

   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"

   527   by (simp (no_asm_use) add: init_seg_of_def)

   528      (metis UnCI Un_absorb2 subset_trans)

   529

   530 lemma antisym_init_seg_of:

   531   "r initial_segment_of s \<Longrightarrow> s initial_segment_of r \<Longrightarrow> r = s"

   532   unfolding init_seg_of_def by safe

   533

   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

   537

   538 lemma chain_subset_trans_Union:

   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

   544

   545 lemma chain_subset_antisym_Union:

   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

   550

   551 lemma chain_subset_Total_Union:

   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)"

   559   proof

   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

   563   next

   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

   567   qed

   568 qed

   569

   570 lemma wf_Union_wf_init_segs:

   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)

   578       case 0 show ?case by fact

   579     next

   580       case (Suc i)

   581       then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"

   582         using 1 by auto

   583       then have "s initial_segment_of r \<or> r initial_segment_of s"

   584         using assms(1) r \<in> R by (simp add: Chains_def)

   585       with Suc s show ?case by (simp add: init_seg_of_def) blast

   586     qed

   587   }

   588   thus False using assms(2) and r \<in> R

   589     by (simp add: wf_iff_no_infinite_down_chain) blast

   590 qed

   591

   592 lemma initial_segment_of_Diff:

   593   "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"

   594   unfolding init_seg_of_def by blast

   595

   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)

   599

   600 theorem well_ordering: "\<exists>r::'a rel. Well_order r \<and> Field r = UNIV"

   601 proof -

   602 -- {*The initial segment relation on well-orders: *}

   603   let ?WO = "{r::'a rel. Well_order r}"

   604   def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"

   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)

   611   hence 0: "Partial_order I"

   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)

   614 -- {*I-chains have upper bounds in ?WO wrt I: their Union*}

   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)

   623     moreover have "trans (\<Union>R)"

   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])

   627     moreover have "Total (\<Union>R)"

   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]]

   633       show ?thesis by (simp (no_asm_simp)) blast

   634     qed

   635     ultimately have "Well_order (\<Union>R)" by(simp add:order_on_defs)

   636     moreover have "\<forall>r \<in> R. r initial_segment_of \<Union>R" using Ris

   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)

   641   }

   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

   643 --{*Zorn's Lemma yields a maximal well-order m:*}

   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"

   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

   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)

   655       ultimately show False using max

   656         by (auto simp: I_def init_seg_of_def simp del: Field_insert)

   657     qed

   658     hence "Field m \<noteq> {}" by(auto simp:Field_def)

   659     moreover have "wf (m - Id)" using Well_order m

   660       by (simp add: well_order_on_def)

   661 --{*The extension of m by x:*}

   662     let ?s = "{(a, x) | a. a \<in> Field m}"

   663     let ?m = "insert (x, x) m \<union> ?s"

   664     have Fm: "Field ?m = insert x (Field m)"

   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)

   668 --{*We show that the extension is a well-order*}

   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 -

   677       have "wf ?s" using x \<notin> Field m

   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]

   681         by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)

   682     qed

   683     ultimately have "Well_order ?m" by (simp add: order_on_defs)

   684 --{*We show that the extension is above m*}

   685     moreover have "(m, ?m) \<in> I" using Well_order ?m and Well_order m and x \<notin> Field m

   686       by (fastforce simp: I_def init_seg_of_def Field_def)

   687     ultimately

   688 --{*This contradicts maximality of m:*}

   689     have False using max and x \<notin> Field m unfolding Field_def by blast

   690   }

   691   hence "Field m = UNIV" by auto

   692   with Well_order m show ?thesis by blast

   693 qed

   694

   695 corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"

   696 proof -

   697   obtain r::"'a rel" where wo: "Well_order r" and univ: "Field r = UNIV"

   698     using well_ordering [where 'a = "'a"] by blast

   699   let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"

   700   have 1: "Field ?r = A" using wo univ

   701     by (fastforce simp: Field_def order_on_defs refl_on_def)

   702   have "Refl r" and "trans r" and "antisym r" and "Total r" and "wf (r - Id)"

   703     using Well_order r by (simp_all add: order_on_defs)

   704   have "Refl ?r" using Refl r by (auto simp: refl_on_def 1 univ)

   705   moreover have "trans ?r" using trans r

   706     unfolding trans_def by blast

   707   moreover have "antisym ?r" using antisym r

   708     unfolding antisym_def by blast

   709   moreover have "Total ?r" using Total r by (simp add:total_on_def 1 univ)

   710   moreover have "wf (?r - Id)" by (rule wf_subset [OF wf (r - Id)]) blast

   711   ultimately have "Well_order ?r" by (simp add: order_on_defs)

   712   with 1 show ?thesis by metis

   713 qed

   714

   715 subsection {* Extending Well-founded Relations to Well-Orders *}

   716

   717 text {*A \emph{downset} (also lower set, decreasing set, initial segment, or

   718 downward closed set) is closed w.r.t.\ smaller elements.*}

   719 definition downset_on where

   720   "downset_on A r = (\<forall>x y. (x, y) \<in> r \<and> y \<in> A \<longrightarrow> x \<in> A)"

   721

   722 (*

   723 text {*Connection to order filters of the @{theory Cardinals} theory.*}

   724 lemma (in wo_rel) ofilter_downset_on_conv:

   725   "ofilter A \<longleftrightarrow> downset_on A r \<and> A \<subseteq> Field r"

   726   by (auto simp: downset_on_def ofilter_def under_def)

   727 *)

   728

   729 lemma downset_onI:

   730   "(\<And>x y. (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A) \<Longrightarrow> downset_on A r"

   731   by (auto simp: downset_on_def)

   732

   733 lemma downset_onD:

   734   "downset_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A \<Longrightarrow> x \<in> A"

   735   by (auto simp: downset_on_def)

   736

   737 text {*Extensions of relations w.r.t.\ a given set.*}

   738 definition extension_on where

   739   "extension_on A r s = (\<forall>x\<in>A. \<forall>y\<in>A. (x, y) \<in> s \<longrightarrow> (x, y) \<in> r)"

   740

   741 lemma extension_onI:

   742   "(\<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"

   743   by (auto simp: extension_on_def)

   744

   745 lemma extension_onD:

   746   "extension_on A r s \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> s \<Longrightarrow> (x, y) \<in> r"

   747   by (auto simp: extension_on_def)

   748

   749 lemma downset_on_Union:

   750   assumes "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p"

   751   shows "downset_on (Field (\<Union>R)) p"

   752   using assms by (auto intro: downset_onI dest: downset_onD)

   753

   754 lemma chain_subset_extension_on_Union:

   755   assumes "chain\<^sub>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"

   756   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"

   757   using assms

   758   by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp)

   759

   760 lemma downset_on_empty [simp]: "downset_on {} p"

   761   by (auto simp: downset_on_def)

   762

   763 lemma extension_on_empty [simp]: "extension_on {} p q"

   764   by (auto simp: extension_on_def)

   765

   766 text {*Every well-founded relation can be extended to a well-order.*}

   767 theorem well_order_extension:

   768   assumes "wf p"

   769   shows "\<exists>w. p \<subseteq> w \<and> Well_order w"

   770 proof -

   771   let ?K = "{r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p}"

   772   def I \<equiv> "init_seg_of \<inter> ?K \<times> ?K"

   773   have I_init: "I \<subseteq> init_seg_of" by (simp add: I_def)

   774   then have subch: "\<And>R. R \<in> Chains I \<Longrightarrow> chain\<^sub>\<subseteq> R"

   775     by (auto simp: init_seg_of_def chain_subset_def Chains_def)

   776   have Chains_wo: "\<And>R r. R \<in> Chains I \<Longrightarrow> r \<in> R \<Longrightarrow>

   777       Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p"

   778     by (simp add: Chains_def I_def) blast

   779   have FI: "Field I = ?K" by (auto simp: I_def init_seg_of_def Field_def)

   780   then have 0: "Partial_order I"

   781     by (auto simp: partial_order_on_def preorder_on_def antisym_def antisym_init_seg_of refl_on_def

   782       trans_def I_def elim: trans_init_seg_of)

   783   { fix R assume "R \<in> Chains I"

   784     then have Ris: "R \<in> Chains init_seg_of" using mono_Chains [OF I_init] by blast

   785     have subch: "chain\<^sub>\<subseteq> R" using R \<in> Chains I I_init

   786       by (auto simp: init_seg_of_def chain_subset_def Chains_def)

   787     have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r" and

   788       "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)" and

   789       "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and

   790       "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"

   791       using Chains_wo [OF R \<in> Chains I] by (simp_all add: order_on_defs)

   792     have "Refl (\<Union>R)" using \<forall>r\<in>R. Refl r by (auto simp: refl_on_def)

   793     moreover have "trans (\<Union>R)"

   794       by (rule chain_subset_trans_Union [OF subch \<forall>r\<in>R. trans r])

   795     moreover have "antisym (\<Union>R)"

   796       by (rule chain_subset_antisym_Union [OF subch \<forall>r\<in>R. antisym r])

   797     moreover have "Total (\<Union>R)"

   798       by (rule chain_subset_Total_Union [OF subch \<forall>r\<in>R. Total r])

   799     moreover have "wf ((\<Union>R) - Id)"

   800     proof -

   801       have "(\<Union>R) - Id = \<Union>{r - Id | r. r \<in> R}" by blast

   802       with \<forall>r\<in>R. wf (r - Id) wf_Union_wf_init_segs [OF Chains_inits_DiffI [OF Ris]]

   803       show ?thesis by (simp (no_asm_simp)) blast

   804     qed

   805     ultimately have "Well_order (\<Union>R)" by (simp add: order_on_defs)

   806     moreover have "\<forall>r\<in>R. r initial_segment_of \<Union>R" using Ris

   807       by (simp add: Chains_init_seg_of_Union)

   808     moreover have "downset_on (Field (\<Union>R)) p"

   809       by (rule downset_on_Union [OF \<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p])

   810     moreover have "extension_on (Field (\<Union>R)) (\<Union>R) p"

   811       by (rule chain_subset_extension_on_Union [OF subch \<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p])

   812     ultimately have "\<Union>R \<in> ?K \<and> (\<forall>r\<in>R. (r,\<Union>R) \<in> I)"

   813       using mono_Chains [OF I_init] and R \<in> Chains I

   814       by (simp (no_asm) add: I_def del: Field_Union) (metis Chains_wo)

   815   }

   816   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

   817   txt {*Zorn's Lemma yields a maximal well-order m.*}

   818   from Zorns_po_lemma [OF 0 1] obtain m :: "('a \<times> 'a) set"

   819     where "Well_order m" and "downset_on (Field m) p" and "extension_on (Field m) m p" and

   820     max: "\<forall>r. Well_order r \<and> downset_on (Field r) p \<and> extension_on (Field r) r p \<and>

   821       (m, r) \<in> I \<longrightarrow> r = m"

   822     by (auto simp: FI)

   823   have "Field p \<subseteq> Field m"

   824   proof (rule ccontr)

   825     let ?Q = "Field p - Field m"

   826     assume "\<not> (Field p \<subseteq> Field m)"

   827     with assms [unfolded wf_eq_minimal, THEN spec, of ?Q]

   828       obtain x where "x \<in> Field p" and "x \<notin> Field m" and

   829       min: "\<forall>y. (y, x) \<in> p \<longrightarrow> y \<notin> ?Q" by blast

   830     txt {*Add @{term x} as topmost element to @{term m}.*}

   831     let ?s = "{(y, x) | y. y \<in> Field m}"

   832     let ?m = "insert (x, x) m \<union> ?s"

   833     have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def)

   834     have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"

   835       using Well_order m by (simp_all add: order_on_defs)

   836     txt {*We show that the extension is a well-order.*}

   837     have "Refl ?m" using Refl m Fm by (auto simp: refl_on_def)

   838     moreover have "trans ?m" using trans m x \<notin> Field m

   839       unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast

   840     moreover have "antisym ?m" using antisym m x \<notin> Field m

   841       unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast

   842     moreover have "Total ?m" using Total m Fm by (auto simp: Relation.total_on_def)

   843     moreover have "wf (?m - Id)"

   844     proof -

   845       have "wf ?s" using x \<notin> Field m

   846         by (simp add: wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis

   847       thus ?thesis using wf (m - Id) x \<notin> Field m

   848         wf_subset [OF wf ?s Diff_subset]

   849         by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)

   850     qed

   851     ultimately have "Well_order ?m" by (simp add: order_on_defs)

   852     moreover have "extension_on (Field ?m) ?m p"

   853       using extension_on (Field m) m p downset_on (Field m) p

   854       by (subst Fm) (auto simp: extension_on_def dest: downset_onD)

   855     moreover have "downset_on (Field ?m) p"

   856       using downset_on (Field m) p and min

   857       by (subst Fm, simp add: downset_on_def Field_def) (metis Domain_iff)

   858     moreover have "(m, ?m) \<in> I"

   859       using Well_order m and Well_order ?m and

   860       downset_on (Field m) p and downset_on (Field ?m) p and

   861       extension_on (Field m) m p and extension_on (Field ?m) ?m p and

   862       Refl m and x \<notin> Field m

   863       by (auto simp: I_def init_seg_of_def refl_on_def)

   864     ultimately

   865     --{*This contradicts maximality of m:*}

   866     show False using max and x \<notin> Field m unfolding Field_def by blast

   867   qed

   868   have "p \<subseteq> m"

   869     using Field p \<subseteq> Field m and extension_on (Field m) m p

   870     by (force simp: Field_def extension_on_def)

   871   with Well_order m show ?thesis by blast

   872 qed

   873

   874 text {*Every well-founded relation can be extended to a total well-order.*}

   875 corollary total_well_order_extension:

   876   assumes "wf p"

   877   shows "\<exists>w. p \<subseteq> w \<and> Well_order w \<and> Field w = UNIV"

   878 proof -

   879   from well_order_extension [OF assms] obtain w

   880     where "p \<subseteq> w" and wo: "Well_order w" by blast

   881   let ?A = "UNIV - Field w"

   882   from well_order_on [of ?A] obtain w' where wo': "well_order_on ?A w'" ..

   883   have [simp]: "Field w' = ?A" using rel.well_order_on_Well_order [OF wo'] by simp

   884   have *: "Field w \<inter> Field w' = {}" by simp

   885   let ?w = "w \<union>o w'"

   886   have "p \<subseteq> ?w" using p \<subseteq> w by (auto simp: Osum_def)

   887   moreover have "Well_order ?w" using Osum_Well_order [OF * wo] and wo' by simp

   888   moreover have "Field ?w = UNIV" by (simp add: Field_Osum)

   889   ultimately show ?thesis by blast

   890 qed

   891

   892 corollary well_order_on_extension:

   893   assumes "wf p" and "Field p \<subseteq> A"

   894   shows "\<exists>w. p \<subseteq> w \<and> well_order_on A w"

   895 proof -

   896   from total_well_order_extension [OF wf p] obtain r

   897     where "p \<subseteq> r" and wo: "Well_order r" and univ: "Field r = UNIV" by blast

   898   let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"

   899   from p \<subseteq> r have "p \<subseteq> ?r" using Field p \<subseteq> A by (auto simp: Field_def)

   900   have 1: "Field ?r = A" using wo univ

   901     by (fastforce simp: Field_def order_on_defs refl_on_def)

   902   have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"

   903     using Well_order r by (simp_all add: order_on_defs)

   904   have "refl_on A ?r" using Refl r by (auto simp: refl_on_def univ)

   905   moreover have "trans ?r" using trans r

   906     unfolding trans_def by blast

   907   moreover have "antisym ?r" using antisym r

   908     unfolding antisym_def by blast

   909   moreover have "total_on A ?r" using Total r by (simp add: total_on_def univ)

   910   moreover have "wf (?r - Id)" by (rule wf_subset [OF wf(r - Id)]) blast

   911   ultimately have "well_order_on A ?r" by (simp add: order_on_defs)

   912   with p \<subseteq> ?r show ?thesis by blast

   913 qed

   914

   915 end

   916