src/HOL/Order_Relation.thy
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 58184 db1381d811ab
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      HOL/Order_Relation.thy
     2     Author:     Tobias Nipkow
     3     Author:     Andrei Popescu, TU Muenchen
     4 *)
     5 
     6 header {* Orders as Relations *}
     7 
     8 theory Order_Relation
     9 imports Wfrec
    10 begin
    11 
    12 subsection{* Orders on a set *}
    13 
    14 definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
    15 
    16 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
    17 
    18 definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r"
    19 
    20 definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r"
    21 
    22 definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)"
    23 
    24 lemmas order_on_defs =
    25   preorder_on_def partial_order_on_def linear_order_on_def
    26   strict_linear_order_on_def well_order_on_def
    27 
    28 
    29 lemma preorder_on_empty[simp]: "preorder_on {} {}"
    30 by(simp add:preorder_on_def trans_def)
    31 
    32 lemma partial_order_on_empty[simp]: "partial_order_on {} {}"
    33 by(simp add:partial_order_on_def)
    34 
    35 lemma lnear_order_on_empty[simp]: "linear_order_on {} {}"
    36 by(simp add:linear_order_on_def)
    37 
    38 lemma well_order_on_empty[simp]: "well_order_on {} {}"
    39 by(simp add:well_order_on_def)
    40 
    41 
    42 lemma preorder_on_converse[simp]: "preorder_on A (r^-1) = preorder_on A r"
    43 by (simp add:preorder_on_def)
    44 
    45 lemma partial_order_on_converse[simp]:
    46   "partial_order_on A (r^-1) = partial_order_on A r"
    47 by (simp add: partial_order_on_def)
    48 
    49 lemma linear_order_on_converse[simp]:
    50   "linear_order_on A (r^-1) = linear_order_on A r"
    51 by (simp add: linear_order_on_def)
    52 
    53 
    54 lemma strict_linear_order_on_diff_Id:
    55   "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r-Id)"
    56 by(simp add: order_on_defs trans_diff_Id)
    57 
    58 
    59 subsection{* Orders on the field *}
    60 
    61 abbreviation "Refl r \<equiv> refl_on (Field r) r"
    62 
    63 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
    64 
    65 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
    66 
    67 abbreviation "Total r \<equiv> total_on (Field r) r"
    68 
    69 abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
    70 
    71 abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
    72 
    73 
    74 lemma subset_Image_Image_iff:
    75   "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
    76    r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
    77 unfolding preorder_on_def refl_on_def Image_def
    78 apply (simp add: subset_eq)
    79 unfolding trans_def by fast
    80 
    81 lemma subset_Image1_Image1_iff:
    82   "\<lbrakk> Preorder r; a : Field r; b : Field r\<rbrakk> \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b,a):r"
    83 by(simp add:subset_Image_Image_iff)
    84 
    85 lemma Refl_antisym_eq_Image1_Image1_iff:
    86   assumes r: "Refl r" and as: "antisym r" and abf: "a \<in> Field r" "b \<in> Field r"
    87   shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
    88 proof
    89   assume "r `` {a} = r `` {b}"
    90   hence e: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r" by (simp add: set_eq_iff)
    91   have "(a, a) \<in> r" "(b, b) \<in> r" using r abf by (simp_all add: refl_on_def)
    92   hence "(a, b) \<in> r" "(b, a) \<in> r" using e[of a] e[of b] by simp_all
    93   thus "a = b" using as[unfolded antisym_def] by blast
    94 qed fast
    95 
    96 lemma Partial_order_eq_Image1_Image1_iff:
    97   "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    98 by(auto simp:order_on_defs Refl_antisym_eq_Image1_Image1_iff)
    99 
   100 lemma Total_Id_Field:
   101 assumes TOT: "Total r" and NID: "\<not> (r <= Id)"
   102 shows "Field r = Field(r - Id)"
   103 using mono_Field[of "r - Id" r] Diff_subset[of r Id]
   104 proof(auto)
   105   have "r \<noteq> {}" using NID by fast
   106   then obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" using NID by auto
   107   hence 1: "b \<noteq> c \<and> {b,c} \<le> Field r" by (auto simp: Field_def)
   108 
   109   fix a assume *: "a \<in> Field r"
   110   obtain d where 2: "d \<in> Field r" and 3: "d \<noteq> a"
   111   using * 1 by auto
   112   hence "(a,d) \<in> r \<or> (d,a) \<in> r" using * TOT
   113   by (simp add: total_on_def)
   114   thus "a \<in> Field(r - Id)" using 3 unfolding Field_def by blast
   115 qed
   116 
   117 
   118 subsection{* Orders on a type *}
   119 
   120 abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
   121 
   122 abbreviation "linear_order \<equiv> linear_order_on UNIV"
   123 
   124 abbreviation "well_order \<equiv> well_order_on UNIV"
   125 
   126 
   127 subsection {* Order-like relations *}
   128 
   129 text{* In this subsection, we develop basic concepts and results pertaining
   130 to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
   131 total relations. We also further define upper and lower bounds operators. *}
   132 
   133 
   134 subsubsection {* Auxiliaries *}
   135 
   136 lemma refl_on_domain:
   137 "\<lbrakk>refl_on A r; (a,b) : r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
   138 by(auto simp add: refl_on_def)
   139 
   140 corollary well_order_on_domain:
   141 "\<lbrakk>well_order_on A r; (a,b) \<in> r\<rbrakk> \<Longrightarrow> a \<in> A \<and> b \<in> A"
   142 by (auto simp add: refl_on_domain order_on_defs)
   143 
   144 lemma well_order_on_Field:
   145 "well_order_on A r \<Longrightarrow> A = Field r"
   146 by(auto simp add: refl_on_def Field_def order_on_defs)
   147 
   148 lemma well_order_on_Well_order:
   149 "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
   150 using well_order_on_Field by auto
   151 
   152 lemma Total_subset_Id:
   153 assumes TOT: "Total r" and SUB: "r \<le> Id"
   154 shows "r = {} \<or> (\<exists>a. r = {(a,a)})"
   155 proof-
   156   {assume "r \<noteq> {}"
   157    then obtain a b where 1: "(a,b) \<in> r" by fast
   158    hence "a = b" using SUB by blast
   159    hence 2: "(a,a) \<in> r" using 1 by simp
   160    {fix c d assume "(c,d) \<in> r"
   161     hence "{a,c,d} \<le> Field r" using 1 unfolding Field_def by blast
   162     hence "((a,c) \<in> r \<or> (c,a) \<in> r \<or> a = c) \<and>
   163            ((a,d) \<in> r \<or> (d,a) \<in> r \<or> a = d)"
   164     using TOT unfolding total_on_def by blast
   165     hence "a = c \<and> a = d" using SUB by blast
   166    }
   167    hence "r \<le> {(a,a)}" by auto
   168    with 2 have "\<exists>a. r = {(a,a)}" by blast
   169   }
   170   thus ?thesis by blast
   171 qed
   172 
   173 lemma Linear_order_in_diff_Id:
   174 assumes LI: "Linear_order r" and
   175         IN1: "a \<in> Field r" and IN2: "b \<in> Field r"
   176 shows "((a,b) \<in> r) = ((b,a) \<notin> r - Id)"
   177 using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
   178 
   179 
   180 subsubsection {* The upper and lower bounds operators  *}
   181 
   182 text{* Here we define upper (``above") and lower (``below") bounds operators.
   183 We think of @{text "r"} as a {\em non-strict} relation.  The suffix ``S"
   184 at the names of some operators indicates that the bounds are strict -- e.g.,
   185 @{text "underS a"} is the set of all strict lower bounds of @{text "a"} (w.r.t. @{text "r"}).
   186 Capitalization of the first letter in the name reminds that the operator acts on sets, rather
   187 than on individual elements. *}
   188 
   189 definition under::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   190 where "under r a \<equiv> {b. (b,a) \<in> r}"
   191 
   192 definition underS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   193 where "underS r a \<equiv> {b. b \<noteq> a \<and> (b,a) \<in> r}"
   194 
   195 definition Under::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   196 where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b,a) \<in> r}"
   197 
   198 definition UnderS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   199 where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b,a) \<in> r}"
   200 
   201 definition above::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   202 where "above r a \<equiv> {b. (a,b) \<in> r}"
   203 
   204 definition aboveS::"'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   205 where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a,b) \<in> r}"
   206 
   207 definition Above::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   208 where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a,b) \<in> r}"
   209 
   210 definition AboveS::"'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   211 where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a,b) \<in> r}"
   212 
   213 definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
   214 where "ofilter r A \<equiv> (A \<le> Field r) \<and> (\<forall>a \<in> A. under r a \<le> A)"
   215 
   216 text{* Note:  In the definitions of @{text "Above[S]"} and @{text "Under[S]"},
   217   we bounded comprehension by @{text "Field r"} in order to properly cover
   218   the case of @{text "A"} being empty. *}
   219 
   220 lemma underS_subset_under: "underS r a \<le> under r a"
   221 by(auto simp add: underS_def under_def)
   222 
   223 lemma underS_notIn: "a \<notin> underS r a"
   224 by(simp add: underS_def)
   225 
   226 lemma Refl_under_in: "\<lbrakk>Refl r; a \<in> Field r\<rbrakk> \<Longrightarrow> a \<in> under r a"
   227 by(simp add: refl_on_def under_def)
   228 
   229 lemma AboveS_disjoint: "A Int (AboveS r A) = {}"
   230 by(auto simp add: AboveS_def)
   231 
   232 lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
   233 by(auto simp add: AboveS_def underS_def)
   234 
   235 lemma Refl_under_underS:
   236   assumes "Refl r" "a \<in> Field r"
   237   shows "under r a = underS r a \<union> {a}"
   238 unfolding under_def underS_def
   239 using assms refl_on_def[of _ r] by fastforce
   240 
   241 lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
   242 by (auto simp: Field_def underS_def)
   243 
   244 lemma under_Field: "under r a \<le> Field r"
   245 by(unfold under_def Field_def, auto)
   246 
   247 lemma underS_Field: "underS r a \<le> Field r"
   248 by(unfold underS_def Field_def, auto)
   249 
   250 lemma underS_Field2:
   251 "a \<in> Field r \<Longrightarrow> underS r a < Field r"
   252 using underS_notIn underS_Field by fast
   253 
   254 lemma underS_Field3:
   255 "Field r \<noteq> {} \<Longrightarrow> underS r a < Field r"
   256 by(cases "a \<in> Field r", simp add: underS_Field2, auto simp add: underS_empty)
   257 
   258 lemma AboveS_Field: "AboveS r A \<le> Field r"
   259 by(unfold AboveS_def Field_def, auto)
   260 
   261 lemma under_incr:
   262   assumes TRANS: "trans r" and REL: "(a,b) \<in> r"
   263   shows "under r a \<le> under r b"
   264 proof(unfold under_def, auto)
   265   fix x assume "(x,a) \<in> r"
   266   with REL TRANS trans_def[of r]
   267   show "(x,b) \<in> r" by blast
   268 qed
   269 
   270 lemma underS_incr:
   271 assumes TRANS: "trans r" and ANTISYM: "antisym r" and
   272         REL: "(a,b) \<in> r"
   273 shows "underS r a \<le> underS r b"
   274 proof(unfold underS_def, auto)
   275   assume *: "b \<noteq> a" and **: "(b,a) \<in> r"
   276   with ANTISYM antisym_def[of r] REL
   277   show False by blast
   278 next
   279   fix x assume "x \<noteq> a" "(x,a) \<in> r"
   280   with REL TRANS trans_def[of r]
   281   show "(x,b) \<in> r" by blast
   282 qed
   283 
   284 lemma underS_incl_iff:
   285 assumes LO: "Linear_order r" and
   286         INa: "a \<in> Field r" and INb: "b \<in> Field r"
   287 shows "(underS r a \<le> underS r b) = ((a,b) \<in> r)"
   288 proof
   289   assume "(a,b) \<in> r"
   290   thus "underS r a \<le> underS r b" using LO
   291   by (simp add: order_on_defs underS_incr)
   292 next
   293   assume *: "underS r a \<le> underS r b"
   294   {assume "a = b"
   295    hence "(a,b) \<in> r" using assms
   296    by (simp add: order_on_defs refl_on_def)
   297   }
   298   moreover
   299   {assume "a \<noteq> b \<and> (b,a) \<in> r"
   300    hence "b \<in> underS r a" unfolding underS_def by blast
   301    hence "b \<in> underS r b" using * by blast
   302    hence False by (simp add: underS_notIn)
   303   }
   304   ultimately
   305   show "(a,b) \<in> r" using assms
   306   order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   307 qed
   308 
   309 
   310 subsection {* Variations on Well-Founded Relations  *}
   311 
   312 text {*
   313 This subsection contains some variations of the results from @{theory Wellfounded}:
   314 \begin{itemize}
   315 \item means for slightly more direct definitions by well-founded recursion;
   316 \item variations of well-founded induction;
   317 \item means for proving a linear order to be a well-order.
   318 \end{itemize}
   319 *}
   320 
   321 
   322 subsubsection {* Characterizations of well-foundedness *}
   323 
   324 text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
   325 i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
   326 
   327 lemma trans_wf_iff:
   328 assumes "trans r"
   329 shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
   330 proof-
   331   obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
   332   {assume *: "wf r"
   333    {fix a
   334     have "wf(R a)"
   335     using * R_def wf_subset[of r "R a"] by auto
   336    }
   337   }
   338   (*  *)
   339   moreover
   340   {assume *: "\<forall>a. wf(R a)"
   341    have "wf r"
   342    proof(unfold wf_def, clarify)
   343      fix phi a
   344      assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
   345      obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
   346      with * have "wf (R a)" by auto
   347      hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
   348      unfolding wf_def by blast
   349      moreover
   350      have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
   351      proof(auto simp add: chi_def R_def)
   352        fix b
   353        assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
   354        hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
   355        using assms trans_def[of r] by blast
   356        thus "phi b" using ** by blast
   357      qed
   358      ultimately have  "\<forall>b. chi b" by (rule mp)
   359      with ** chi_def show "phi a" by blast
   360    qed
   361   }
   362   ultimately show ?thesis using R_def by blast
   363 qed
   364 
   365 text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
   366 allowing one to assume the set included in the field.  *}
   367 
   368 lemma wf_eq_minimal2:
   369 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
   370 proof-
   371   let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
   372   have "wf r = (\<forall>A. ?phi A)"
   373   by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   374      (rule wfI_min, fast)
   375   (*  *)
   376   also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   377   proof
   378     assume "\<forall>A. ?phi A"
   379     thus "\<forall>B \<le> Field r. ?phi B" by simp
   380   next
   381     assume *: "\<forall>B \<le> Field r. ?phi B"
   382     show "\<forall>A. ?phi A"
   383     proof(clarify)
   384       fix A::"'a set" assume **: "A \<noteq> {}"
   385       obtain B where B_def: "B = A Int (Field r)" by blast
   386       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   387       proof(cases "B = {}")
   388         assume Case1: "B = {}"
   389         obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   390         using ** Case1 unfolding B_def by blast
   391         hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   392         thus ?thesis using 1 by blast
   393       next
   394         assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   395         obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   396         using Case2 1 * by blast
   397         have "\<forall>a' \<in> A. (a',a) \<notin> r"
   398         proof(clarify)
   399           fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   400           hence "a' \<in> B" unfolding B_def Field_def by blast
   401           thus False using 2 ** by blast
   402         qed
   403         thus ?thesis using 2 unfolding B_def by blast
   404       qed
   405     qed
   406   qed
   407   finally show ?thesis by blast
   408 qed
   409 
   410 
   411 subsubsection {* Characterizations of well-foundedness *}
   412 
   413 text {* The next lemma and its corollary enable one to prove that
   414 a linear order is a well-order in a way which is more standard than
   415 via well-foundedness of the strict version of the relation.  *}
   416 
   417 lemma Linear_order_wf_diff_Id:
   418 assumes LI: "Linear_order r"
   419 shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   420 proof(cases "r \<le> Id")
   421   assume Case1: "r \<le> Id"
   422   hence temp: "r - Id = {}" by blast
   423   hence "wf(r - Id)" by (simp add: temp)
   424   moreover
   425   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   426    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   427    unfolding order_on_defs using Case1 Total_subset_Id by auto
   428    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   429    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   430   }
   431   ultimately show ?thesis by blast
   432 next
   433   assume Case2: "\<not> r \<le> Id"
   434   hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   435   unfolding order_on_defs by blast
   436   show ?thesis
   437   proof
   438     assume *: "wf(r - Id)"
   439     show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   440     proof(clarify)
   441       fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   442       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   443       using 1 * unfolding wf_eq_minimal2 by simp
   444       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   445       using Linear_order_in_diff_Id[of r] ** LI by blast
   446       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   447     qed
   448   next
   449     assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   450     show "wf(r - Id)"
   451     proof(unfold wf_eq_minimal2, clarify)
   452       fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   453       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   454       using 1 * by simp
   455       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   456       using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   457       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   458     qed
   459   qed
   460 qed
   461 
   462 corollary Linear_order_Well_order_iff:
   463 assumes "Linear_order r"
   464 shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   465 using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   466 
   467 end