src/HOL/Library/Zorn.thy
changeset 26272 d63776c3be97
parent 26191 ae537f315b34
child 26295 afc43168ed85
     1.1 --- a/src/HOL/Library/Zorn.thy	Fri Mar 14 19:57:12 2008 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Fri Mar 14 19:57:32 2008 +0100
     1.3 @@ -8,9 +8,13 @@
     1.4  header {* Zorn's Lemma *}
     1.5  
     1.6  theory Zorn
     1.7 -imports ATP_Linkup Hilbert_Choice
     1.8 +imports Order_Relation
     1.9  begin
    1.10  
    1.11 +(* Define globally? In Set.thy? *)
    1.12 +definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") where
    1.13 +"chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
    1.14 +
    1.15  text{*
    1.16    The lemma and section numbers refer to an unpublished article
    1.17    \cite{Abrial-Laffitte}.
    1.18 @@ -18,7 +22,7 @@
    1.19  
    1.20  definition
    1.21    chain     ::  "'a set set => 'a set set set" where
    1.22 -  "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    1.23 +  "chain S  = {F. F \<subseteq> S & chain\<^bsub>\<subseteq>\<^esub> F}"
    1.24  
    1.25  definition
    1.26    super     ::  "['a set set,'a set set] => 'a set set set" where
    1.27 @@ -145,7 +149,7 @@
    1.28   the subset relation!*}
    1.29  
    1.30  lemma empty_set_mem_chain: "({} :: 'a set set) \<in> chain S"
    1.31 -  by (unfold chain_def) auto
    1.32 +by (unfold chain_def chain_subset_def) auto
    1.33  
    1.34  lemma super_subset_chain: "super S c \<subseteq> chain S"
    1.35    by (unfold super_def) blast
    1.36 @@ -181,7 +185,7 @@
    1.37  lemma TFin_chain_lemma4: "c \<in> TFin S ==> (c :: 'a set set): chain S"
    1.38    apply (erule TFin_induct)
    1.39     apply (simp add: succ_def select_super [THEN super_subset_chain[THEN subsetD]])
    1.40 -  apply (unfold chain_def)
    1.41 +  apply (unfold chain_def chain_subset_def)
    1.42    apply (rule CollectI, safe)
    1.43     apply (drule bspec, assumption)
    1.44     apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
    1.45 @@ -203,106 +207,64 @@
    1.46                                 There Is  a Maximal Element*}
    1.47  
    1.48  lemma chain_extend:
    1.49 -    "[| c \<in> chain S; z \<in> S;
    1.50 -        \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
    1.51 -  by (unfold chain_def) blast
    1.52 +  "[| c \<in> chain S; z \<in> S; \<forall>x \<in> c. x \<subseteq> (z:: 'a set) |] ==> {z} Un c \<in> chain S"
    1.53 +by (unfold chain_def chain_subset_def) blast
    1.54  
    1.55  lemma chain_Union_upper: "[| c \<in> chain S; x \<in> c |] ==> x \<subseteq> Union(c)"
    1.56 -  by (unfold chain_def) auto
    1.57 +by auto
    1.58  
    1.59  lemma chain_ball_Union_upper: "c \<in> chain S ==> \<forall>x \<in> c. x \<subseteq> Union(c)"
    1.60 -  by (unfold chain_def) auto
    1.61 +by auto
    1.62  
    1.63  lemma maxchain_Zorn:
    1.64 -     "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
    1.65 -  apply (rule ccontr)
    1.66 -  apply (simp add: maxchain_def)
    1.67 -  apply (erule conjE)
    1.68 -  apply (subgoal_tac "({u} Un c) \<in> super S c")
    1.69 -   apply simp
    1.70 -  apply (unfold super_def psubset_def)
    1.71 -  apply (blast intro: chain_extend dest: chain_Union_upper)
    1.72 -  done
    1.73 +  "[| c \<in> maxchain S; u \<in> S; Union(c) \<subseteq> u |] ==> Union(c) = u"
    1.74 +apply (rule ccontr)
    1.75 +apply (simp add: maxchain_def)
    1.76 +apply (erule conjE)
    1.77 +apply (subgoal_tac "({u} Un c) \<in> super S c")
    1.78 + apply simp
    1.79 +apply (unfold super_def psubset_def)
    1.80 +apply (blast intro: chain_extend dest: chain_Union_upper)
    1.81 +done
    1.82  
    1.83  theorem Zorn_Lemma:
    1.84 -    "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
    1.85 -  apply (cut_tac Hausdorff maxchain_subset_chain)
    1.86 -  apply (erule exE)
    1.87 -  apply (drule subsetD, assumption)
    1.88 -  apply (drule bspec, assumption)
    1.89 -  apply (rule_tac x = "Union(c)" in bexI)
    1.90 -   apply (rule ballI, rule impI)
    1.91 -   apply (blast dest!: maxchain_Zorn, assumption)
    1.92 -  done
    1.93 +  "\<forall>c \<in> chain S. Union(c): S ==> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z --> y = z"
    1.94 +apply (cut_tac Hausdorff maxchain_subset_chain)
    1.95 +apply (erule exE)
    1.96 +apply (drule subsetD, assumption)
    1.97 +apply (drule bspec, assumption)
    1.98 +apply (rule_tac x = "Union(c)" in bexI)
    1.99 + apply (rule ballI, rule impI)
   1.100 + apply (blast dest!: maxchain_Zorn, assumption)
   1.101 +done
   1.102  
   1.103  subsection{*Alternative version of Zorn's Lemma*}
   1.104  
   1.105  lemma Zorn_Lemma2:
   1.106    "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>x \<in> c. x \<subseteq> y
   1.107      ==> \<exists>y \<in> S. \<forall>x \<in> S. (y :: 'a set) \<subseteq> x --> y = x"
   1.108 -  apply (cut_tac Hausdorff maxchain_subset_chain)
   1.109 -  apply (erule exE)
   1.110 -  apply (drule subsetD, assumption)
   1.111 -  apply (drule bspec, assumption, erule bexE)
   1.112 -  apply (rule_tac x = y in bexI)
   1.113 -   prefer 2 apply assumption
   1.114 -  apply clarify
   1.115 -  apply (rule ccontr)
   1.116 -  apply (frule_tac z = x in chain_extend)
   1.117 -    apply (assumption, blast)
   1.118 -  apply (unfold maxchain_def super_def psubset_def)
   1.119 -  apply (blast elim!: equalityCE)
   1.120 -  done
   1.121 +apply (cut_tac Hausdorff maxchain_subset_chain)
   1.122 +apply (erule exE)
   1.123 +apply (drule subsetD, assumption)
   1.124 +apply (drule bspec, assumption, erule bexE)
   1.125 +apply (rule_tac x = y in bexI)
   1.126 + prefer 2 apply assumption
   1.127 +apply clarify
   1.128 +apply (rule ccontr)
   1.129 +apply (frule_tac z = x in chain_extend)
   1.130 +  apply (assumption, blast)
   1.131 +apply (unfold maxchain_def super_def psubset_def)
   1.132 +apply (blast elim!: equalityCE)
   1.133 +done
   1.134  
   1.135  text{*Various other lemmas*}
   1.136  
   1.137  lemma chainD: "[| c \<in> chain S; x \<in> c; y \<in> c |] ==> x \<subseteq> y | y \<subseteq> x"
   1.138 -  by (unfold chain_def) blast
   1.139 +by (unfold chain_def chain_subset_def) blast
   1.140  
   1.141  lemma chainD2: "!!(c :: 'a set set). c \<in> chain S ==> c \<subseteq> S"
   1.142 -  by (unfold chain_def) blast
   1.143 -
   1.144 -
   1.145 -(* FIXME into Relation.thy *)
   1.146 -
   1.147 -lemma mono_Field: "r \<subseteq> s \<Longrightarrow> Field r \<subseteq> Field s"
   1.148 -by(auto simp:Field_def Domain_def Range_def)
   1.149 -
   1.150 -lemma Field_empty[simp]: "Field {} = {}"
   1.151 -by(auto simp:Field_def)
   1.152 -
   1.153 -lemma Field_insert[simp]: "Field (insert (a,b) r) = {a,b} \<union> Field r"
   1.154 -by(auto simp:Field_def)
   1.155 -
   1.156 -lemma Field_Un[simp]: "Field (r \<union> s) = Field r \<union> Field s"
   1.157 -by(auto simp:Field_def)
   1.158 -
   1.159 -lemma Field_Union[simp]: "Field (\<Union>R) = \<Union>(Field ` R)"
   1.160 -by(auto simp:Field_def)
   1.161 +by (unfold chain_def) blast
   1.162  
   1.163 -lemma Domain_converse[simp]: "Domain(r^-1) = Range r"
   1.164 -by blast
   1.165 -
   1.166 -lemma Range_converse[simp]: "Range(r^-1) = Domain r"
   1.167 -by blast
   1.168 -
   1.169 -lemma Field_converse[simp]: "Field(r^-1) = Field r"
   1.170 -by(auto simp:Field_def)
   1.171 -
   1.172 -lemma reflexive_reflcl[simp]: "reflexive(r^=)"
   1.173 -by(simp add:refl_def)
   1.174 -
   1.175 -lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
   1.176 -by(simp add:antisym_def)
   1.177 -
   1.178 -lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"
   1.179 -unfolding trans_def by blast
   1.180 -
   1.181 -(*********************************************************)
   1.182 -
   1.183 -(* Define globally? In Set.thy?
   1.184 -   Use in def of chain at the beginning *)
   1.185 -definition "subset_chain C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
   1.186  
   1.187  (* Define globally? In Relation.thy? *)
   1.188  definition Chain :: "('a*'a)set \<Rightarrow> 'a set set" where
   1.189 @@ -311,83 +273,6 @@
   1.190  lemma mono_Chain: "r \<subseteq> s \<Longrightarrow> Chain r \<subseteq> Chain s"
   1.191  unfolding Chain_def by blast
   1.192  
   1.193 -(* Are the following definitions the "right" ones?
   1.194 -
   1.195 -Key point: should the set appear as an explicit argument,
   1.196 -(as currently in "refl A r") or should it remain implicitly the Field
   1.197 -(as in Refl below)? I use refl/Refl merely to illusrate the point.
   1.198 -
   1.199 -The notation "refl A r" is closer to the usual (A,<=) in the literature
   1.200 -whereas "Refl r" is shorter and avoids naming the set.
   1.201 -Note that "refl A r \<Longrightarrow> A = Field r & Refl r" and "Refl r \<Longrightarrow> refl (Field r) r"
   1.202 -This makes the A look redundant.
   1.203 -
   1.204 -A slight advantage of having the A around is that one can write "a:A"
   1.205 -rather than "a:Field r". A disavantage is the multiple occurrences of
   1.206 -"refl (Field r) r" (etc) in the proof of the well-ordering thm.
   1.207 -
   1.208 -I propose to move the definitions into Main, either as they are or
   1.209 -with an additional A argument.
   1.210 -
   1.211 -Naming: The capital letters were chosen to distinguish them from
   1.212 -versions on the whole type we have (eg reflexive) or may want to have
   1.213 -(eg preorder). In case of an additional A argument one could append
   1.214 -"_on" to distinguish the relativized versions.
   1.215 -*)
   1.216 -
   1.217 -definition "Refl r \<equiv> \<forall>x \<in> Field r. (x,x) \<in> r"
   1.218 -definition "Preorder r \<equiv> Refl r \<and> trans r"
   1.219 -definition "Partial_order r \<equiv> Preorder r \<and> antisym r"
   1.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"
   1.221 -definition "Linear_order r \<equiv> Partial_order r \<and> Total r"
   1.222 -definition "Well_order r \<equiv> Linear_order r \<and> wf(r - Id)"
   1.223 -
   1.224 -lemmas Order_defs =
   1.225 -  Preorder_def Partial_order_def Linear_order_def Well_order_def
   1.226 -
   1.227 -lemma Refl_empty[simp]: "Refl {}"
   1.228 -by(simp add:Refl_def)
   1.229 -lemma Preorder_empty[simp]: "Preorder {}"
   1.230 -by(simp add:Preorder_def trans_def)
   1.231 -lemma Partial_order_empty[simp]: "Partial_order {}"
   1.232 -by(simp add:Partial_order_def)
   1.233 -lemma Total_empty[simp]: "Total {}"
   1.234 -by(simp add:Total_def)
   1.235 -lemma Linear_order_empty[simp]: "Linear_order {}"
   1.236 -by(simp add:Linear_order_def)
   1.237 -lemma Well_order_empty[simp]: "Well_order {}"
   1.238 -by(simp add:Well_order_def)
   1.239 -
   1.240 -lemma Refl_converse[simp]: "Refl(r^-1) = Refl r"
   1.241 -by(simp add:Refl_def)
   1.242 -
   1.243 -lemma Preorder_converse[simp]: "Preorder (r^-1) = Preorder r"
   1.244 -by (simp add:Preorder_def)
   1.245 -
   1.246 -lemma Partial_order_converse[simp]:
   1.247 -  "Partial_order (r^-1) = Partial_order r"
   1.248 -by (simp add: Partial_order_def)
   1.249 -
   1.250 -lemma subset_Image_Image_iff:
   1.251 -  "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
   1.252 -   r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
   1.253 -apply(auto simp add:subset_def Preorder_def Refl_def Image_def)
   1.254 -apply metis
   1.255 -by(metis trans_def)
   1.256 -
   1.257 -lemma subset_Image1_Image1_iff:
   1.258 -  "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
   1.259 -by(simp add:subset_Image_Image_iff)
   1.260 -
   1.261 -lemma Refl_antisym_eq_Image1_Image1_iff:
   1.262 -  "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   1.263 -by(simp add:Preorder_def expand_set_eq Partial_order_def antisym_def Refl_def)
   1.264 -  metis
   1.265 -
   1.266 -lemma Partial_order_eq_Image1_Image1_iff:
   1.267 -  "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
   1.268 -by(auto simp:Preorder_def Partial_order_def Refl_antisym_eq_Image1_Image1_iff)
   1.269 -
   1.270  text{* Zorn's lemma for partial orders: *}
   1.271  
   1.272  lemma Zorns_po_lemma:
   1.273 @@ -398,7 +283,7 @@
   1.274  --{* Mirror r in the set of subsets below (wrt r) elements of A*}
   1.275    let ?B = "%x. r^-1 `` {x}" let ?S = "?B ` Field r"
   1.276    have "\<forall>C \<in> chain ?S. EX U:?S. ALL A:C. A\<subseteq>U"
   1.277 -  proof (auto simp:chain_def)
   1.278 +  proof (auto simp:chain_def chain_subset_def)
   1.279      fix C assume 1: "C \<subseteq> ?S" and 2: "\<forall>A\<in>C.\<forall>B\<in>C. A\<subseteq>B | B\<subseteq>A"
   1.280      let ?A = "{x\<in>Field r. \<exists>M\<in>C. M = ?B x}"
   1.281      have "C = ?B ` ?A" using 1 by(auto simp: image_def)
   1.282 @@ -457,26 +342,26 @@
   1.283    "R \<in> Chain init_seg_of \<Longrightarrow> r\<in>R \<Longrightarrow> r initial_segment_of \<Union>R"
   1.284  by(auto simp add:init_seg_of_def Chain_def Ball_def) blast
   1.285  
   1.286 -lemma subset_chain_trans_Union:
   1.287 -  "subset_chain R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
   1.288 -apply(auto simp add:subset_chain_def)
   1.289 +lemma chain_subset_trans_Union:
   1.290 +  "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. trans r \<Longrightarrow> trans(\<Union>R)"
   1.291 +apply(auto simp add:chain_subset_def)
   1.292  apply(simp (no_asm_use) add:trans_def)
   1.293  apply (metis subsetD)
   1.294  done
   1.295  
   1.296 -lemma subset_chain_antisym_Union:
   1.297 -  "subset_chain R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
   1.298 -apply(auto simp add:subset_chain_def antisym_def)
   1.299 +lemma chain_subset_antisym_Union:
   1.300 +  "chain\<^bsub>\<subseteq>\<^esub> R \<Longrightarrow> \<forall>r\<in>R. antisym r \<Longrightarrow> antisym(\<Union>R)"
   1.301 +apply(auto simp add:chain_subset_def antisym_def)
   1.302  apply (metis subsetD)
   1.303  done
   1.304  
   1.305 -lemma subset_chain_Total_Union:
   1.306 -assumes "subset_chain R" "\<forall>r\<in>R. Total r"
   1.307 +lemma chain_subset_Total_Union:
   1.308 +assumes "chain\<^bsub>\<subseteq>\<^esub> R" "\<forall>r\<in>R. Total r"
   1.309  shows "Total (\<Union>R)"
   1.310  proof (simp add: Total_def Ball_def, auto del:disjCI)
   1.311    fix r s a b assume A: "r:R" "s:R" "a:Field r" "b:Field s" "a\<noteq>b"
   1.312 -  from `subset_chain R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
   1.313 -    by(simp add:subset_chain_def)
   1.314 +  from `chain\<^bsub>\<subseteq>\<^esub> R` `r:R` `s:R` have "r\<subseteq>s \<or> s\<subseteq>r"
   1.315 +    by(simp add:chain_subset_def)
   1.316    thus "(\<exists>r\<in>R. (a,b) \<in> r) \<or> (\<exists>r\<in>R. (b,a) \<in> r)"
   1.317    proof
   1.318      assume "r\<subseteq>s" hence "(a,b):s \<or> (b,a):s" using assms(2) A
   1.319 @@ -517,14 +402,14 @@
   1.320  apply (metis subsetD)
   1.321  done
   1.322  
   1.323 -theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r"
   1.324 +theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = UNIV"
   1.325  proof-
   1.326  -- {*The initial segment relation on well-orders: *}
   1.327    let ?WO = "{r::('a*'a)set. Well_order r}"
   1.328    def I \<equiv> "init_seg_of \<inter> ?WO \<times> ?WO"
   1.329    have I_init: "I \<subseteq> init_seg_of" by(auto simp:I_def)
   1.330 -  hence subch: "!!R. R : Chain I \<Longrightarrow> subset_chain R"
   1.331 -    by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   1.332 +  hence subch: "!!R. R : Chain I \<Longrightarrow> chain\<^bsub>\<subseteq>\<^esub> R"
   1.333 +    by(auto simp:init_seg_of_def chain_subset_def Chain_def)
   1.334    have Chain_wo: "!!R r. R \<in> Chain I \<Longrightarrow> r \<in> R \<Longrightarrow> Well_order r"
   1.335      by(simp add:Chain_def I_def) blast
   1.336    have FI: "Field I = ?WO" by(auto simp add:I_def init_seg_of_def Field_def)
   1.337 @@ -533,18 +418,18 @@
   1.338  -- {*I-chains have upper bounds in ?WO wrt I: their Union*}
   1.339    { fix R assume "R \<in> Chain I"
   1.340      hence Ris: "R \<in> Chain init_seg_of" using mono_Chain[OF I_init] by blast
   1.341 -    have subch: "subset_chain R" using `R : Chain I` I_init
   1.342 -      by(auto simp:init_seg_of_def subset_chain_def Chain_def)
   1.343 +    have subch: "chain\<^bsub>\<subseteq>\<^esub> R" using `R : Chain I` I_init
   1.344 +      by(auto simp:init_seg_of_def chain_subset_def Chain_def)
   1.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"
   1.346           "\<forall>r\<in>R. wf(r-Id)"
   1.347        using Chain_wo[OF `R \<in> Chain I`] by(simp_all add:Order_defs)
   1.348      have "Refl (\<Union>R)" using `\<forall>r\<in>R. Refl r` by(auto simp:Refl_def)
   1.349      moreover have "trans (\<Union>R)"
   1.350 -      by(rule subset_chain_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   1.351 +      by(rule chain_subset_trans_Union[OF subch `\<forall>r\<in>R. trans r`])
   1.352      moreover have "antisym(\<Union>R)"
   1.353 -      by(rule subset_chain_antisym_Union[OF subch `\<forall>r\<in>R. antisym r`])
   1.354 +      by(rule chain_subset_antisym_Union[OF subch `\<forall>r\<in>R. antisym r`])
   1.355      moreover have "Total (\<Union>R)"
   1.356 -      by(rule subset_chain_Total_Union[OF subch `\<forall>r\<in>R. Total r`])
   1.357 +      by(rule chain_subset_Total_Union[OF subch `\<forall>r\<in>R. Total r`])
   1.358      moreover have "wf((\<Union>R)-Id)"
   1.359      proof-
   1.360        have "(\<Union>R)-Id = \<Union>{r-Id|r. r \<in> R}" by blast
   1.361 @@ -607,8 +492,28 @@
   1.362      have False using max `x \<notin> Field m` unfolding Field_def by blast
   1.363    }
   1.364    hence "Field m = UNIV" by auto
   1.365 -  with `Well_order m` have "Well_order m" by simp
   1.366 -  thus ?thesis ..
   1.367 +  moreover with `Well_order m` have "Well_order m" by simp
   1.368 +  ultimately show ?thesis by blast
   1.369 +qed
   1.370 +
   1.371 +corollary well_ordering_set: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = A"
   1.372 +proof -
   1.373 +  obtain r::"('a*'a)set" where wo: "Well_order r" and univ: "Field r = UNIV"
   1.374 +    using well_ordering[where 'a = "'a"] by blast
   1.375 +  let ?r = "{(x,y). x:A & y:A & (x,y):r}"
   1.376 +  have 1: "Field ?r = A" using wo univ
   1.377 +    by(fastsimp simp: Field_def Domain_def Range_def Order_defs Refl_def)
   1.378 +  have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
   1.379 +    using `Well_order r` by(simp_all add:Order_defs)
   1.380 +  have "Refl ?r" using `Refl r` by(auto simp:Refl_def 1 univ)
   1.381 +  moreover have "trans ?r" using `trans r`
   1.382 +    unfolding trans_def by blast
   1.383 +  moreover have "antisym ?r" using `antisym r`
   1.384 +    unfolding antisym_def by blast
   1.385 +  moreover have "Total ?r" using `Total r` by(simp add:Total_def 1 univ)
   1.386 +  moreover have "wf(?r - Id)" by(rule wf_subset[OF `wf(r-Id)`]) blast
   1.387 +  ultimately have "Well_order ?r" by(simp add:Order_defs)
   1.388 +  with 1 show ?thesis by blast
   1.389  qed
   1.390  
   1.391  end