Added Order_Relation
authornipkow
Fri Mar 14 19:57:32 2008 +0100 (2008-03-14)
changeset 26272d63776c3be97
parent 26271 e324f8918c98
child 26273 6c4d534af98d
Added Order_Relation
src/HOL/Library/Library.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Library.thy	Fri Mar 14 19:57:12 2008 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Fri Mar 14 19:57:32 2008 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4    Numeral_Type
     1.5    OptionalSugar
     1.6    Option_ord
     1.7 +  Order_Relation
     1.8    Parity
     1.9    Permutation
    1.10    Primes
     2.1 --- a/src/HOL/Library/Zorn.thy	Fri Mar 14 19:57:12 2008 +0100
     2.2 +++ b/src/HOL/Library/Zorn.thy	Fri Mar 14 19:57:32 2008 +0100
     2.3 @@ -8,9 +8,13 @@
     2.4  header {* Zorn's Lemma *}
     2.5  
     2.6  theory Zorn
     2.7 -imports ATP_Linkup Hilbert_Choice
     2.8 +imports Order_Relation
     2.9  begin
    2.10  
    2.11 +(* Define globally? In Set.thy? *)
    2.12 +definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") where
    2.13 +"chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
    2.14 +
    2.15  text{*
    2.16    The lemma and section numbers refer to an unpublished article
    2.17    \cite{Abrial-Laffitte}.
    2.18 @@ -18,7 +22,7 @@
    2.19  
    2.20  definition
    2.21    chain     ::  "'a set set => 'a set set set" where
    2.22 -  "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    2.23 +  "chain S  = {F. F \<subseteq> S & chain\<^bsub>\<subseteq>\<^esub> F}"
    2.24  
    2.25  definition
    2.26    super     ::  "['a set set,'a set set] => 'a set set set" where
    2.27 @@ -145,7 +149,7 @@
    2.28   the subset relation!*}
    2.29  
    2.30  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
    2.31 -  by (unfold chain_def) auto
    2.32 +by (unfold chain_def chain_subset_def) auto
    2.33  
    2.34  lemma super_subset_chain: "super S c \<subseteq> chain S"
    2.35    by (unfold super_def) blast
    2.36 @@ -181,7 +185,7 @@
    2.37  lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
    2.38    apply (erule TFin_induct)
    2.39     apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
    2.40 -  apply (unfold chain_def)
    2.41 +  apply (unfold chain_def chain_subset_def)
    2.42    apply (rule CollectI, safe)
    2.43     apply (drule bspec, assumption)
    2.44     apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
    2.45 @@ -203,106 +207,64 @@
    2.46                                 There Is  a Maximal Element*}
    2.47  
    2.48  lemma chain_extend:
    2.49 -    "[| c \<in> chain S; z \<in> S;
    2.50 -        \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
    2.51 -  by (unfold chain_def) blast
    2.52 +  "[| c \<in> chain S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
    2.53 +by (unfold chain_def chain_subset_def) blast
    2.54  
    2.55  lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
    2.56 -  by (unfold chain_def) auto
    2.57 +by auto
    2.58  
    2.59  lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
    2.60 -  by (unfold chain_def) auto
    2.61 +by auto
    2.62  
    2.63  lemma maxchain_Zorn:
    2.64 -     "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
    2.65 -  apply (rule ccontr)
    2.66 -  apply (simp add: maxchain_def)
    2.67 -  apply (erule conjE)
    2.68 -  apply (subgoal_tac "({u} Un c) \<in> super S c")
    2.69 -   apply simp
    2.70 -  apply (unfold super_def psubset_def)
    2.71 -  apply (blast intro: chain_extend dest: chain_Union_upper)
    2.72 -  done
    2.73 +  "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
    2.74 +apply (rule ccontr)
    2.75 +apply (simp add: maxchain_def)
    2.76 +apply (erule conjE)
    2.77 +apply (subgoal_tac "({u} Un c) \<in> super S c")
    2.78 + apply simp
    2.79 +apply (unfold super_def psubset_def)
    2.80 +apply (blast intro: chain_extend dest: chain_Union_upper)
    2.81 +done
    2.82  
    2.83  theorem Zorn_Lemma:
    2.84 -    "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
    2.85 -  apply (cut_tac Hausdorff maxchain_subset_chain)
    2.86 -  apply (erule exE)
    2.87 -  apply (drule subsetD, assumption)
    2.88 -  apply (drule bspec, assumption)
    2.89 -  apply (rule_tac x = "Union(c)" in bexI)
    2.90 -   apply (rule ballI, rule impI)
    2.91 -   apply (blast dest!: maxchain_Zorn, assumption)
    2.92 -  done
    2.93 +  "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
    2.94 +apply (cut_tac Hausdorff maxchain_subset_chain)
    2.95 +apply (erule exE)
    2.96 +apply (drule subsetD, assumption)
    2.97 +apply (drule bspec, assumption)
    2.98 +apply (rule_tac x = "Union(c)" in bexI)
    2.99 + apply (rule ballI, rule impI)
   2.100 + apply (blast dest!: maxchain_Zorn, assumption)
   2.101 +done
   2.102  
   2.103  subsection{*Alternative version of Zorn's Lemma*}
   2.104  
   2.105  lemma Zorn_Lemma2:
   2.106    "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   2.107      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   2.108 -  apply (cut_tac Hausdorff maxchain_subset_chain)
   2.109 -  apply (erule exE)
   2.110 -  apply (drule subsetD, assumption)
   2.111 -  apply (drule bspec, assumption, erule bexE)
   2.112 -  apply (rule_tac x = y in bexI)
   2.113 -   prefer 2 apply assumption
   2.114 -  apply clarify
   2.115 -  apply (rule ccontr)
   2.116 -  apply (frule_tac z = x in chain_extend)
   2.117 -    apply (assumption, blast)
   2.118 -  apply (unfold maxchain_def super_def psubset_def)
   2.119 -  apply (blast elim!: equalityCE)
   2.120 -  done
   2.121 +apply (cut_tac Hausdorff maxchain_subset_chain)
   2.122 +apply (erule exE)
   2.123 +apply (drule subsetD, assumption)
   2.124 +apply (drule bspec, assumption, erule bexE)
   2.125 +apply (rule_tac x = y in bexI)
   2.126 + prefer 2 apply assumption
   2.127 +apply clarify
   2.128 +apply (rule ccontr)
   2.129 +apply (frule_tac z = x in chain_extend)
   2.130 +  apply (assumption, blast)
   2.131 +apply (unfold maxchain_def super_def psubset_def)
   2.132 +apply (blast elim!: equalityCE)
   2.133 +done
   2.134  
   2.135  text{*Various other lemmas*}
   2.136  
   2.137  lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   2.138 -  by (unfold chain_def) blast
   2.139 +by (unfold chain_def chain_subset_def) blast
   2.140  
   2.141  lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   2.142 -  by (unfold chain_def) blast
   2.143 -
   2.144 -
   2.145 -(* FIXME into Relation.thy *)
   2.146 -
   2.147 -lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   2.148 -by(auto simp:Field_def Domain_def Range_def)
   2.149 -
   2.150 -lemma Field_empty[simp]: "Field {} = {}"
   2.151 -by(auto simp:Field_def)
   2.152 -
   2.153 -lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r"
   2.154 -by(auto simp:Field_def)
   2.155 -
   2.156 -lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s"
   2.157 -by(auto simp:Field_def)
   2.158 -
   2.159 -lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
   2.160 -by(auto simp:Field_def)
   2.161 +by (unfold chain_def) blast
   2.162  
   2.163 -lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   2.164 -by blast
   2.165 -
   2.166 -lemma Range_converse[simp]: "Range(r^-1) = Domain r"
   2.167 -by blast
   2.168 -
   2.169 -lemma Field_converse[simp]: "Field(r^-1) = Field r"
   2.170 -by(auto simp:Field_def)
   2.171 -
   2.172 -lemma reflexive_reflcl[simp]: "reflexive(r^=)"
   2.173 -by(simp add:refl_def)
   2.174 -
   2.175 -lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
   2.176 -by(simp add:antisym_def)
   2.177 -
   2.178 -lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
   2.179 -unfolding trans_def by blast
   2.180 -
   2.181 -(*********************************************************)
   2.182 -
   2.183 -(* Define globally? In Set.thy?
   2.184 -   Use in def of chain at the beginning *)
   2.185 -definition "subset_chain C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
   2.186  
   2.187  (* Define globally? In Relation.thy? *)
   2.188  definition Chain :: "('a*'a)set \<Rightarrow> 'a set set" where
   2.189 @@ -311,83 +273,6 @@
   2.190  lemma mono_Chain: "r \<subseteq> s \<Longrightarrow> Chain r \<subseteq> Chain s"
   2.191  unfolding Chain_def by blast
   2.192  
   2.193 -(* Are the following definitions the "right" ones?
   2.194 -
   2.195 -Key point: should the set appear as an explicit argument,
   2.196 -(as currently in "refl A r") or should it remain implicitly the Field
   2.197 -(as in Refl below)? I use refl/Refl merely to illusrate the point.
   2.198 -
   2.199 -The notation "refl A r" is closer to the usual (A,<=) in the literature
   2.200 -whereas "Refl r" is shorter and avoids naming the set.
   2.201 -Note that "refl A r \<Longrightarrow> A = Field r & Refl r" and "Refl r \<Longrightarrow> refl (Field r) r"
   2.202 -This makes the A look redundant.
   2.203 -
   2.204 -A slight advantage of having the A around is that one can write "a:A"
   2.205 -rather than "a:Field r". A disavantage is the multiple occurrences of
   2.206 -"refl (Field r) r" (etc) in the proof of the well-ordering thm.
   2.207 -
   2.208 -I propose to move the definitions into Main, either as they are or
   2.209 -with an additional A argument.
   2.210 -
   2.211 -Naming: The capital letters were chosen to distinguish them from
   2.212 -versions on the whole type we have (eg reflexive) or may want to have
   2.213 -(eg preorder). In case of an additional A argument one could append
   2.214 -"_on" to distinguish the relativized versions.
   2.215 -*)
   2.216 -
   2.217 -definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
   2.218 -definition "Preorder r \<equiv> Refl r \<and> trans r"
   2.219 -definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
   2.220 -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"
   2.221 -definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
   2.222 -definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
   2.223 -
   2.224 -lemmas Order_defs =
   2.225 -  Preorder_def Partial_order_def Linear_order_def Well_order_def
   2.226 -
   2.227 -lemma Refl_empty[simp]: "Refl {}"
   2.228 -by(simp add:Refl_def)
   2.229 -lemma Preorder_empty[simp]: "Preorder {}"
   2.230 -by(simp add:Preorder_def trans_def)
   2.231 -lemma Partial_order_empty[simp]: "Partial_order {}"
   2.232 -by(simp add:Partial_order_def)
   2.233 -lemma Total_empty[simp]: "Total {}"
   2.234 -by(simp add:Total_def)
   2.235 -lemma Linear_order_empty[simp]: "Linear_order {}"
   2.236 -by(simp add:Linear_order_def)
   2.237 -lemma Well_order_empty[simp]: "Well_order {}"
   2.238 -by(simp add:Well_order_def)
   2.239 -
   2.240 -lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
   2.241 -by(simp add:Refl_def)
   2.242 -
   2.243 -lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
   2.244 -by (simp add:Preorder_def)
   2.245 -
   2.246 -lemma Partial_order_converse[simp]:
   2.247 -  "Partial_order (r^-1) = Partial_order r"
   2.248 -by (simp add: Partial_order_def)
   2.249 -
   2.250 -lemma subset_Image_Image_iff:
   2.251 -  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
   2.252 -   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
   2.253 -apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
   2.254 -apply metis
   2.255 -by(metis trans_def)
   2.256 -
   2.257 -lemma subset_Image1_Image1_iff:
   2.258 -  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
   2.259 -by(simp add:subset_Image_Image_iff)
   2.260 -
   2.261 -lemma Refl_antisym_eq_Image1_Image1_iff:
   2.262 -  "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   2.263 -by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
   2.264 -  metis
   2.265 -
   2.266 -lemma Partial_order_eq_Image1_Image1_iff:
   2.267 -  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   2.268 -by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)
   2.269 -
   2.270  text{* Zorn's lemma for partial orders: *}
   2.271  
   2.272  lemma Zorns_po_lemma:
   2.273 @@ -398,7 +283,7 @@
   2.274  --{* Mirror r in the set of subsets below (wrt r) elements of A*}
   2.275    let ?B = "%x. r^-1 `` {x}" let ?S = "?B ` Field r"
   2.276    have "\<forall>C \<in> chain ?S. EX U:?S. ALL A:C. A\<subseteq>U"
   2.277 -  proof (auto simp:chain_def)
   2.278 +  proof (auto simp:chain_def chain_subset_def)
   2.279      fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C.\<forall>B\<in>C. A\<subseteq>B | B\<subseteq>A"
   2.280      let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
   2.281      have "C = ?B ` ?A" using 1 by(auto simp: image_def)
   2.282 @@ -457,26 +342,26 @@
   2.283    "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   2.284  by(auto simp add:init_seg_of_def Chain_def Ball_def) blast
   2.285  
   2.286 -lemma subset_chain_trans_Union:
   2.287 -  "subset_chain R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
   2.288 -apply(auto simp add:subset_chain_def)
   2.289 +lemma chain_subset_trans_Union:
   2.290 +  "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
   2.291 +apply(auto simp add:chain_subset_def)
   2.292  apply(simp (no_asm_use) add:trans_def)
   2.293  apply (metis subsetD)
   2.294  done
   2.295  
   2.296 -lemma subset_chain_antisym_Union:
   2.297 -  "subset_chain R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
   2.298 -apply(auto simp add:subset_chain_def antisym_def)
   2.299 +lemma chain_subset_antisym_Union:
   2.300 +  "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
   2.301 +apply(auto simp add:chain_subset_def antisym_def)
   2.302  apply (metis subsetD)
   2.303  done
   2.304  
   2.305 -lemma subset_chain_Total_Union:
   2.306 -assumes "subset_chain R" "\<forall>r\<in>R. Total r"
   2.307 +lemma chain_subset_Total_Union:
   2.308 +assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r"
   2.309  shows "Total (\<Union>R)"
   2.310  proof (simp add: Total_def Ball_def, auto del:disjCI)
   2.311    fix r s a b assume A: "r:R" "s:R" "a:Field r" "b:Field s" "a\<noteq>b"
   2.312 -  from `subset_chain R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
   2.313 -    by(simp add:subset_chain_def)
   2.314 +  from `chain\<^bsub>\<subseteq>\<^esub> R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
   2.315 +    by(simp add:chain_subset_def)
   2.316    thus "(\<exists>r\<in>R. (a,b) \<in> r) \<or> (\<exists>r\<in>R. (b,a) \<in> r)"
   2.317    proof
   2.318      assume "r\<subseteq>s" hence "(a,b):s \<or> (b,a):s" using assms(2) A
   2.319 @@ -517,14 +402,14 @@
   2.320  apply (metis subsetD)
   2.321  done
   2.322  
   2.323 -theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r"
   2.324 +theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = UNIV"
   2.325  proof-
   2.326  -- {*The initial segment relation on well-orders: *}
   2.327    let ?WO = "{r::('a*'a)set. Well_order r}"
   2.328    def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
   2.329    have I_init: "I \<subseteq> init_seg_of" by(auto simp:I_def)
   2.330 -  hence subch: "!!R. R : Chain I \<Longrightarrow> subset_chain R"
   2.331 -    by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   2.332 +  hence subch: "!!R. R : Chain I \<Longrightarrow> chain\<^bsub>\<subseteq>\<^esub> R"
   2.333 +    by(auto simp:init_seg_of_def chain_subset_def Chain_def)
   2.334    have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
   2.335      by(simp add:Chain_def I_def) blast
   2.336    have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   2.337 @@ -533,18 +418,18 @@
   2.338  -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   2.339    { fix R assume "R \<in> Chain I"
   2.340      hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
   2.341 -    have subch: "subset_chain R" using `R : Chain I` I_init
   2.342 -      by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   2.343 +    have subch: "chain\<^bsub>\<subseteq>\<^esub> R" using `R : Chain I` I_init
   2.344 +      by(auto simp:init_seg_of_def chain_subset_def Chain_def)
   2.345      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"
   2.346           "\<forall>r\<in>R. wf(r-Id)"
   2.347        using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:Order_defs)
   2.348      have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:Refl_def)
   2.349      moreover have "trans (\<Union>R)"
   2.350 -      by(rule subset_chain_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   2.351 +      by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   2.352      moreover have "antisym(\<Union>R)"
   2.353 -      by(rule subset_chain_antisym_Union[OF subch `\<forall>r\<in>R. antisym r`])
   2.354 +      by(rule chain_subset_antisym_Union[OF subch `\<forall>r\<in>R. antisym r`])
   2.355      moreover have "Total (\<Union>R)"
   2.356 -      by(rule subset_chain_Total_Union[OF subch `\<forall>r\<in>R. Total r`])
   2.357 +      by(rule chain_subset_Total_Union[OF subch `\<forall>r\<in>R. Total r`])
   2.358      moreover have "wf((\<Union>R)-Id)"
   2.359      proof-
   2.360        have "(\<Union>R)-Id = \<Union>{r-Id|r. r \<in> R}" by blast
   2.361 @@ -607,8 +492,28 @@
   2.362      have False using max `x \<notin> Field m` unfolding Field_def by blast
   2.363    }
   2.364    hence "Field m = UNIV" by auto
   2.365 -  with `Well_order m` have "Well_order m" by simp
   2.366 -  thus ?thesis ..
   2.367 +  moreover with `Well_order m` have "Well_order m" by simp
   2.368 +  ultimately show ?thesis by blast
   2.369 +qed
   2.370 +
   2.371 +corollary well_ordering_set: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = A"
   2.372 +proof -
   2.373 +  obtain r::"('a*'a)set" where wo: "Well_order r" and univ: "Field r = UNIV"
   2.374 +    using well_ordering[where 'a = "'a"] by blast
   2.375 +  let ?r = "{(x,y). x:A & y:A & (x,y):r}"
   2.376 +  have 1: "Field ?r = A" using wo univ
   2.377 +    by(fastsimp simp: Field_def Domain_def Range_def Order_defs Refl_def)
   2.378 +  have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
   2.379 +    using `Well_order r` by(simp_all add:Order_defs)
   2.380 +  have "Refl ?r" using `Refl r` by(auto simp:Refl_def 1 univ)
   2.381 +  moreover have "trans ?r" using `trans r`
   2.382 +    unfolding trans_def by blast
   2.383 +  moreover have "antisym ?r" using `antisym r`
   2.384 +    unfolding antisym_def by blast
   2.385 +  moreover have "Total ?r" using `Total r` by(simp add:Total_def 1 univ)
   2.386 +  moreover have "wf(?r - Id)" by(rule wf_subset[OF `wf(r-Id)`]) blast
   2.387 +  ultimately have "Well_order ?r" by(simp add:Order_defs)
   2.388 +  with 1 show ?thesis by blast
   2.389  qed
   2.390  
   2.391  end