src/HOL/Order_Relation.thy
author blanchet
Sun May 04 18:14:58 2014 +0200 (2014-05-04)
changeset 56846 9df717fef2bb
parent 55173 5556470a02b7
child 58184 db1381d811ab
permissions -rw-r--r--
renamed 'xxx_size' to 'size_xxx' for old datatype package
     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 {* Well-founded recursion via genuine fixpoints *}
   323 
   324 lemma wfrec_fixpoint:
   325 fixes r :: "('a * 'a) set" and
   326       H :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   327 assumes WF: "wf r" and ADM: "adm_wf r H"
   328 shows "wfrec r H = H (wfrec r H)"
   329 proof(rule ext)
   330   fix x
   331   have "wfrec r H x = H (cut (wfrec r H) r x) x"
   332   using wfrec[of r H] WF by simp
   333   also
   334   {have "\<And> y. (y,x) : r \<Longrightarrow> (cut (wfrec r H) r x) y = (wfrec r H) y"
   335    by (auto simp add: cut_apply)
   336    hence "H (cut (wfrec r H) r x) x = H (wfrec r H) x"
   337    using ADM adm_wf_def[of r H] by auto
   338   }
   339   finally show "wfrec r H x = H (wfrec r H) x" .
   340 qed
   341 
   342 
   343 subsubsection {* Characterizations of well-foundedness *}
   344 
   345 text {* A transitive relation is well-founded iff it is ``locally'' well-founded,
   346 i.e., iff its restriction to the lower bounds of of any element is well-founded.  *}
   347 
   348 lemma trans_wf_iff:
   349 assumes "trans r"
   350 shows "wf r = (\<forall>a. wf(r Int (r^-1``{a} \<times> r^-1``{a})))"
   351 proof-
   352   obtain R where R_def: "R = (\<lambda> a. r Int (r^-1``{a} \<times> r^-1``{a}))" by blast
   353   {assume *: "wf r"
   354    {fix a
   355     have "wf(R a)"
   356     using * R_def wf_subset[of r "R a"] by auto
   357    }
   358   }
   359   (*  *)
   360   moreover
   361   {assume *: "\<forall>a. wf(R a)"
   362    have "wf r"
   363    proof(unfold wf_def, clarify)
   364      fix phi a
   365      assume **: "\<forall>a. (\<forall>b. (b,a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
   366      obtain chi where chi_def: "chi = (\<lambda>b. (b,a) \<in> r \<longrightarrow> phi b)" by blast
   367      with * have "wf (R a)" by auto
   368      hence "(\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
   369      unfolding wf_def by blast
   370      moreover
   371      have "\<forall>b. (\<forall>c. (c,b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
   372      proof(auto simp add: chi_def R_def)
   373        fix b
   374        assume 1: "(b,a) \<in> r" and 2: "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
   375        hence "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
   376        using assms trans_def[of r] by blast
   377        thus "phi b" using ** by blast
   378      qed
   379      ultimately have  "\<forall>b. chi b" by (rule mp)
   380      with ** chi_def show "phi a" by blast
   381    qed
   382   }
   383   ultimately show ?thesis using R_def by blast
   384 qed
   385 
   386 text {* The next lemma is a variation of @{text "wf_eq_minimal"} from Wellfounded,
   387 allowing one to assume the set included in the field.  *}
   388 
   389 lemma wf_eq_minimal2:
   390 "wf r = (\<forall>A. A <= Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r))"
   391 proof-
   392   let ?phi = "\<lambda> A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. \<not> (a',a) \<in> r)"
   393   have "wf r = (\<forall>A. ?phi A)"
   394   by (auto simp: ex_in_conv [THEN sym], erule wfE_min, assumption, blast)
   395      (rule wfI_min, fast)
   396   (*  *)
   397   also have "(\<forall>A. ?phi A) = (\<forall>B \<le> Field r. ?phi B)"
   398   proof
   399     assume "\<forall>A. ?phi A"
   400     thus "\<forall>B \<le> Field r. ?phi B" by simp
   401   next
   402     assume *: "\<forall>B \<le> Field r. ?phi B"
   403     show "\<forall>A. ?phi A"
   404     proof(clarify)
   405       fix A::"'a set" assume **: "A \<noteq> {}"
   406       obtain B where B_def: "B = A Int (Field r)" by blast
   407       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r"
   408       proof(cases "B = {}")
   409         assume Case1: "B = {}"
   410         obtain a where 1: "a \<in> A \<and> a \<notin> Field r"
   411         using ** Case1 unfolding B_def by blast
   412         hence "\<forall>a' \<in> A. (a',a) \<notin> r" using 1 unfolding Field_def by blast
   413         thus ?thesis using 1 by blast
   414       next
   415         assume Case2: "B \<noteq> {}" have 1: "B \<le> Field r" unfolding B_def by blast
   416         obtain a where 2: "a \<in> B \<and> (\<forall>a' \<in> B. (a',a) \<notin> r)"
   417         using Case2 1 * by blast
   418         have "\<forall>a' \<in> A. (a',a) \<notin> r"
   419         proof(clarify)
   420           fix a' assume "a' \<in> A" and **: "(a',a) \<in> r"
   421           hence "a' \<in> B" unfolding B_def Field_def by blast
   422           thus False using 2 ** by blast
   423         qed
   424         thus ?thesis using 2 unfolding B_def by blast
   425       qed
   426     qed
   427   qed
   428   finally show ?thesis by blast
   429 qed
   430 
   431 
   432 subsubsection {* Characterizations of well-foundedness *}
   433 
   434 text {* The next lemma and its corollary enable one to prove that
   435 a linear order is a well-order in a way which is more standard than
   436 via well-foundedness of the strict version of the relation.  *}
   437 
   438 lemma Linear_order_wf_diff_Id:
   439 assumes LI: "Linear_order r"
   440 shows "wf(r - Id) = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   441 proof(cases "r \<le> Id")
   442   assume Case1: "r \<le> Id"
   443   hence temp: "r - Id = {}" by blast
   444   hence "wf(r - Id)" by (simp add: temp)
   445   moreover
   446   {fix A assume *: "A \<le> Field r" and **: "A \<noteq> {}"
   447    obtain a where 1: "r = {} \<or> r = {(a,a)}" using LI
   448    unfolding order_on_defs using Case1 Total_subset_Id by auto
   449    hence "A = {a} \<and> r = {(a,a)}" using * ** unfolding Field_def by blast
   450    hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" using 1 by blast
   451   }
   452   ultimately show ?thesis by blast
   453 next
   454   assume Case2: "\<not> r \<le> Id"
   455   hence 1: "Field r = Field(r - Id)" using Total_Id_Field LI
   456   unfolding order_on_defs by blast
   457   show ?thesis
   458   proof
   459     assume *: "wf(r - Id)"
   460     show "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   461     proof(clarify)
   462       fix A assume **: "A \<le> Field r" and ***: "A \<noteq> {}"
   463       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   464       using 1 * unfolding wf_eq_minimal2 by simp
   465       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   466       using Linear_order_in_diff_Id[of r] ** LI by blast
   467       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r" by blast
   468     qed
   469   next
   470     assume *: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)"
   471     show "wf(r - Id)"
   472     proof(unfold wf_eq_minimal2, clarify)
   473       fix A assume **: "A \<le> Field(r - Id)" and ***: "A \<noteq> {}"
   474       hence "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   475       using 1 * by simp
   476       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. ((a,a') \<in> r) = ((a',a) \<notin> r - Id)"
   477       using Linear_order_in_diff_Id[of r] ** LI mono_Field[of "r - Id" r] by blast
   478       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id" by blast
   479     qed
   480   qed
   481 qed
   482 
   483 corollary Linear_order_Well_order_iff:
   484 assumes "Linear_order r"
   485 shows "Well_order r = (\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r))"
   486 using assms unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   487 
   488 end