src/HOL/Order_Relation.thy
author wenzelm
Fri Jun 22 20:31:49 2018 +0200 (13 months ago)
changeset 68484 59793df7f853
parent 63952 354808e9f44b
child 68745 345ce5f262ea
permissions -rw-r--r--
clarified document antiquotation @{theory};
     1 (*  Title:      HOL/Order_Relation.thy
     2     Author:     Tobias Nipkow
     3     Author:     Andrei Popescu, TU Muenchen
     4 *)
     5 
     6 section \<open>Orders as Relations\<close>
     7 
     8 theory Order_Relation
     9 imports Wfrec
    10 begin
    11 
    12 subsection \<open>Orders on a set\<close>
    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\<inverse>) = preorder_on A r"
    43   by (simp add: preorder_on_def)
    44 
    45 lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
    46   by (simp add: partial_order_on_def)
    47 
    48 lemma linear_order_on_converse[simp]: "linear_order_on A (r\<inverse>) = linear_order_on A r"
    49   by (simp add: linear_order_on_def)
    50 
    51 
    52 lemma strict_linear_order_on_diff_Id: "linear_order_on A r \<Longrightarrow> strict_linear_order_on A (r - Id)"
    53   by (simp add: order_on_defs trans_diff_Id)
    54 
    55 lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}"
    56   by (simp add: order_on_defs)
    57 
    58 lemma linear_order_on_acyclic:
    59   assumes "linear_order_on A r"
    60   shows "acyclic (r - Id)"
    61   using strict_linear_order_on_diff_Id[OF assms]
    62   by (auto simp add: acyclic_irrefl strict_linear_order_on_def)
    63 
    64 lemma linear_order_on_well_order_on:
    65   assumes "finite r"
    66   shows "linear_order_on A r \<longleftrightarrow> well_order_on A r"
    67   unfolding well_order_on_def
    68   using assms finite_acyclic_wf[OF _ linear_order_on_acyclic, of r] by blast
    69 
    70 
    71 subsection \<open>Orders on the field\<close>
    72 
    73 abbreviation "Refl r \<equiv> refl_on (Field r) r"
    74 
    75 abbreviation "Preorder r \<equiv> preorder_on (Field r) r"
    76 
    77 abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r"
    78 
    79 abbreviation "Total r \<equiv> total_on (Field r) r"
    80 
    81 abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r"
    82 
    83 abbreviation "Well_order r \<equiv> well_order_on (Field r) r"
    84 
    85 
    86 lemma subset_Image_Image_iff:
    87   "Preorder r \<Longrightarrow> A \<subseteq> Field r \<Longrightarrow> B \<subseteq> Field r \<Longrightarrow>
    88     r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b, a) \<in> r)"
    89   apply (simp add: preorder_on_def refl_on_def Image_def subset_eq)
    90   apply (simp only: trans_def)
    91   apply fast
    92   done
    93 
    94 lemma subset_Image1_Image1_iff:
    95   "Preorder r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} \<subseteq> r `` {b} \<longleftrightarrow> (b, a) \<in> r"
    96   by (simp add: subset_Image_Image_iff)
    97 
    98 lemma Refl_antisym_eq_Image1_Image1_iff:
    99   assumes "Refl r"
   100     and as: "antisym r"
   101     and abf: "a \<in> Field r" "b \<in> Field r"
   102   shows "r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   103     (is "?lhs \<longleftrightarrow> ?rhs")
   104 proof
   105   assume ?lhs
   106   then have *: "\<And>x. (a, x) \<in> r \<longleftrightarrow> (b, x) \<in> r"
   107     by (simp add: set_eq_iff)
   108   have "(a, a) \<in> r" "(b, b) \<in> r" using \<open>Refl r\<close> abf by (simp_all add: refl_on_def)
   109   then have "(a, b) \<in> r" "(b, a) \<in> r" using *[of a] *[of b] by simp_all
   110   then show ?rhs
   111     using \<open>antisym r\<close>[unfolded antisym_def] by blast
   112 next
   113   assume ?rhs
   114   then show ?lhs by fast
   115 qed
   116 
   117 lemma Partial_order_eq_Image1_Image1_iff:
   118   "Partial_order r \<Longrightarrow> a \<in> Field r \<Longrightarrow> b \<in> Field r \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a = b"
   119   by (auto simp: order_on_defs Refl_antisym_eq_Image1_Image1_iff)
   120 
   121 lemma Total_Id_Field:
   122   assumes "Total r"
   123     and not_Id: "\<not> r \<subseteq> Id"
   124   shows "Field r = Field (r - Id)"
   125   using mono_Field[of "r - Id" r] Diff_subset[of r Id]
   126 proof auto
   127   fix a assume *: "a \<in> Field r"
   128   from not_Id have "r \<noteq> {}" by fast
   129   with not_Id obtain b and c where "b \<noteq> c \<and> (b,c) \<in> r" by auto
   130   then have "b \<noteq> c \<and> {b, c} \<subseteq> Field r" by (auto simp: Field_def)
   131   with * obtain d where "d \<in> Field r" "d \<noteq> a" by auto
   132   with * \<open>Total r\<close> have "(a, d) \<in> r \<or> (d, a) \<in> r" by (simp add: total_on_def)
   133   with \<open>d \<noteq> a\<close> show "a \<in> Field (r - Id)" unfolding Field_def by blast
   134 qed
   135 
   136 
   137 subsection \<open>Orders on a type\<close>
   138 
   139 abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV"
   140 
   141 abbreviation "linear_order \<equiv> linear_order_on UNIV"
   142 
   143 abbreviation "well_order \<equiv> well_order_on UNIV"
   144 
   145 
   146 subsection \<open>Order-like relations\<close>
   147 
   148 text \<open>
   149   In this subsection, we develop basic concepts and results pertaining
   150   to order-like relations, i.e., to reflexive and/or transitive and/or symmetric and/or
   151   total relations. We also further define upper and lower bounds operators.
   152 \<close>
   153 
   154 
   155 subsubsection \<open>Auxiliaries\<close>
   156 
   157 lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
   158   by (auto simp add: refl_on_def)
   159 
   160 corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
   161   by (auto simp add: refl_on_domain order_on_defs)
   162 
   163 lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> A = Field r"
   164   by (auto simp add: refl_on_def Field_def order_on_defs)
   165 
   166 lemma well_order_on_Well_order: "well_order_on A r \<Longrightarrow> A = Field r \<and> Well_order r"
   167   using well_order_on_Field [of A] by auto
   168 
   169 lemma Total_subset_Id:
   170   assumes "Total r"
   171     and "r \<subseteq> Id"
   172   shows "r = {} \<or> (\<exists>a. r = {(a, a)})"
   173 proof -
   174   have "\<exists>a. r = {(a, a)}" if "r \<noteq> {}"
   175   proof -
   176     from that obtain a b where ab: "(a, b) \<in> r" by fast
   177     with \<open>r \<subseteq> Id\<close> have "a = b" by blast
   178     with ab have aa: "(a, a) \<in> r" by simp
   179     have "a = c \<and> a = d" if "(c, d) \<in> r" for c d
   180     proof -
   181       from that have "{a, c, d} \<subseteq> Field r"
   182         using ab unfolding Field_def by blast
   183       then have "((a, c) \<in> r \<or> (c, a) \<in> r \<or> a = c) \<and> ((a, d) \<in> r \<or> (d, a) \<in> r \<or> a = d)"
   184         using \<open>Total r\<close> unfolding total_on_def by blast
   185       with \<open>r \<subseteq> Id\<close> show ?thesis by blast
   186     qed
   187     then have "r \<subseteq> {(a, a)}" by auto
   188     with aa show ?thesis by blast
   189   qed
   190   then show ?thesis by blast
   191 qed
   192 
   193 lemma Linear_order_in_diff_Id:
   194   assumes "Linear_order r"
   195     and "a \<in> Field r"
   196     and "b \<in> Field r"
   197   shows "(a, b) \<in> r \<longleftrightarrow> (b, a) \<notin> r - Id"
   198   using assms unfolding order_on_defs total_on_def antisym_def Id_def refl_on_def by force
   199 
   200 
   201 subsubsection \<open>The upper and lower bounds operators\<close>
   202 
   203 text \<open>
   204   Here we define upper (``above") and lower (``below") bounds operators. We
   205   think of \<open>r\<close> as a \<^emph>\<open>non-strict\<close> relation. The suffix \<open>S\<close> at the names of
   206   some operators indicates that the bounds are strict -- e.g., \<open>underS a\<close> is
   207   the set of all strict lower bounds of \<open>a\<close> (w.r.t. \<open>r\<close>). Capitalization of
   208   the first letter in the name reminds that the operator acts on sets, rather
   209   than on individual elements.
   210 \<close>
   211 
   212 definition under :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   213   where "under r a \<equiv> {b. (b, a) \<in> r}"
   214 
   215 definition underS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   216   where "underS r a \<equiv> {b. b \<noteq> a \<and> (b, a) \<in> r}"
   217 
   218 definition Under :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   219   where "Under r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (b, a) \<in> r}"
   220 
   221 definition UnderS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   222   where "UnderS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (b, a) \<in> r}"
   223 
   224 definition above :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   225   where "above r a \<equiv> {b. (a, b) \<in> r}"
   226 
   227 definition aboveS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set"
   228   where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a, b) \<in> r}"
   229 
   230 definition Above :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   231   where "Above r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. (a, b) \<in> r}"
   232 
   233 definition AboveS :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
   234   where "AboveS r A \<equiv> {b \<in> Field r. \<forall>a \<in> A. b \<noteq> a \<and> (a, b) \<in> r}"
   235 
   236 definition ofilter :: "'a rel \<Rightarrow> 'a set \<Rightarrow> bool"
   237   where "ofilter r A \<equiv> A \<subseteq> Field r \<and> (\<forall>a \<in> A. under r a \<subseteq> A)"
   238 
   239 text \<open>
   240   Note: In the definitions of \<open>Above[S]\<close> and \<open>Under[S]\<close>, we bounded
   241   comprehension by \<open>Field r\<close> in order to properly cover the case of \<open>A\<close> being
   242   empty.
   243 \<close>
   244 
   245 lemma underS_subset_under: "underS r a \<subseteq> under r a"
   246   by (auto simp add: underS_def under_def)
   247 
   248 lemma underS_notIn: "a \<notin> underS r a"
   249   by (simp add: underS_def)
   250 
   251 lemma Refl_under_in: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> a \<in> under r a"
   252   by (simp add: refl_on_def under_def)
   253 
   254 lemma AboveS_disjoint: "A \<inter> (AboveS r A) = {}"
   255   by (auto simp add: AboveS_def)
   256 
   257 lemma in_AboveS_underS: "a \<in> Field r \<Longrightarrow> a \<in> AboveS r (underS r a)"
   258   by (auto simp add: AboveS_def underS_def)
   259 
   260 lemma Refl_under_underS: "Refl r \<Longrightarrow> a \<in> Field r \<Longrightarrow> under r a = underS r a \<union> {a}"
   261   unfolding under_def underS_def
   262   using refl_on_def[of _ r] by fastforce
   263 
   264 lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}"
   265   by (auto simp: Field_def underS_def)
   266 
   267 lemma under_Field: "under r a \<subseteq> Field r"
   268   by (auto simp: under_def Field_def)
   269 
   270 lemma underS_Field: "underS r a \<subseteq> Field r"
   271   by (auto simp: underS_def Field_def)
   272 
   273 lemma underS_Field2: "a \<in> Field r \<Longrightarrow> underS r a \<subset> Field r"
   274   using underS_notIn underS_Field by fast
   275 
   276 lemma underS_Field3: "Field r \<noteq> {} \<Longrightarrow> underS r a \<subset> Field r"
   277   by (cases "a \<in> Field r") (auto simp: underS_Field2 underS_empty)
   278 
   279 lemma AboveS_Field: "AboveS r A \<subseteq> Field r"
   280   by (auto simp: AboveS_def Field_def)
   281 
   282 lemma under_incr:
   283   assumes "trans r"
   284     and "(a, b) \<in> r"
   285   shows "under r a \<subseteq> under r b"
   286   unfolding under_def
   287 proof auto
   288   fix x assume "(x, a) \<in> r"
   289   with assms trans_def[of r] show "(x, b) \<in> r" by blast
   290 qed
   291 
   292 lemma underS_incr:
   293   assumes "trans r"
   294     and "antisym r"
   295     and ab: "(a, b) \<in> r"
   296   shows "underS r a \<subseteq> underS r b"
   297   unfolding underS_def
   298 proof auto
   299   assume *: "b \<noteq> a" and **: "(b, a) \<in> r"
   300   with \<open>antisym r\<close> antisym_def[of r] ab show False
   301     by blast
   302 next
   303   fix x assume "x \<noteq> a" "(x, a) \<in> r"
   304   with ab \<open>trans r\<close> trans_def[of r] show "(x, b) \<in> r"
   305     by blast
   306 qed
   307 
   308 lemma underS_incl_iff:
   309   assumes LO: "Linear_order r"
   310     and INa: "a \<in> Field r"
   311     and INb: "b \<in> Field r"
   312   shows "underS r a \<subseteq> underS r b \<longleftrightarrow> (a, b) \<in> r"
   313     (is "?lhs \<longleftrightarrow> ?rhs")
   314 proof
   315   assume ?rhs
   316   with \<open>Linear_order r\<close> show ?lhs
   317     by (simp add: order_on_defs underS_incr)
   318 next
   319   assume *: ?lhs
   320   have "(a, b) \<in> r" if "a = b"
   321     using assms that by (simp add: order_on_defs refl_on_def)
   322   moreover have False if "a \<noteq> b" "(b, a) \<in> r"
   323   proof -
   324     from that have "b \<in> underS r a" unfolding underS_def by blast
   325     with * have "b \<in> underS r b" by blast
   326     then show ?thesis by (simp add: underS_notIn)
   327   qed
   328   ultimately show "(a,b) \<in> r"
   329     using assms order_on_defs[of "Field r" r] total_on_def[of "Field r" r] by blast
   330 qed
   331 
   332 lemma finite_Linear_order_induct[consumes 3, case_names step]:
   333   assumes "Linear_order r"
   334     and "x \<in> Field r"
   335     and "finite r"
   336     and step: "\<And>x. x \<in> Field r \<Longrightarrow> (\<And>y. y \<in> aboveS r x \<Longrightarrow> P y) \<Longrightarrow> P x"
   337   shows "P x"
   338   using assms(2)
   339 proof (induct rule: wf_induct[of "r\<inverse> - Id"])
   340   case 1
   341   from assms(1,3) show "wf (r\<inverse> - Id)"
   342     using linear_order_on_well_order_on linear_order_on_converse
   343     unfolding well_order_on_def by blast
   344 next
   345   case prems: (2 x)
   346   show ?case
   347     by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>)
   348 qed
   349 
   350 
   351 subsection \<open>Variations on Well-Founded Relations\<close>
   352 
   353 text \<open>
   354   This subsection contains some variations of the results from \<^theory>\<open>HOL.Wellfounded\<close>:
   355     \<^item> means for slightly more direct definitions by well-founded recursion;
   356     \<^item> variations of well-founded induction;
   357     \<^item> means for proving a linear order to be a well-order.
   358 \<close>
   359 
   360 
   361 subsubsection \<open>Characterizations of well-foundedness\<close>
   362 
   363 text \<open>
   364   A transitive relation is well-founded iff it is ``locally'' well-founded,
   365   i.e., iff its restriction to the lower bounds of of any element is
   366   well-founded.
   367 \<close>
   368 
   369 lemma trans_wf_iff:
   370   assumes "trans r"
   371   shows "wf r \<longleftrightarrow> (\<forall>a. wf (r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})))"
   372 proof -
   373   define R where "R a = r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})" for a
   374   have "wf (R a)" if "wf r" for a
   375     using that R_def wf_subset[of r "R a"] by auto
   376   moreover
   377   have "wf r" if *: "\<forall>a. wf(R a)"
   378     unfolding wf_def
   379   proof clarify
   380     fix phi a
   381     assume **: "\<forall>a. (\<forall>b. (b, a) \<in> r \<longrightarrow> phi b) \<longrightarrow> phi a"
   382     define chi where "chi b \<longleftrightarrow> (b, a) \<in> r \<longrightarrow> phi b" for b
   383     with * have "wf (R a)" by auto
   384     then have "(\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b) \<longrightarrow> (\<forall>b. chi b)"
   385       unfolding wf_def by blast
   386     also have "\<forall>b. (\<forall>c. (c, b) \<in> R a \<longrightarrow> chi c) \<longrightarrow> chi b"
   387     proof (auto simp add: chi_def R_def)
   388       fix b
   389       assume "(b, a) \<in> r" and "\<forall>c. (c, b) \<in> r \<and> (c, a) \<in> r \<longrightarrow> phi c"
   390       then have "\<forall>c. (c, b) \<in> r \<longrightarrow> phi c"
   391         using assms trans_def[of r] by blast
   392       with ** show "phi b" by blast
   393     qed
   394     finally have  "\<forall>b. chi b" .
   395     with ** chi_def show "phi a" by blast
   396   qed
   397   ultimately show ?thesis unfolding R_def by blast
   398 qed
   399 
   400 text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
   401 corollary wf_finite_segments:
   402   assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
   403   shows "wf (r)"
   404 proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
   405   fix a
   406   have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
   407     using assms unfolding trans_def Field_def by blast
   408   then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
   409     using assms acyclic_def assms irrefl_def by fastforce
   410 qed
   411 
   412 text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
   413   allowing one to assume the set included in the field.\<close>
   414 
   415 lemma wf_eq_minimal2: "wf r \<longleftrightarrow> (\<forall>A. A \<subseteq> Field r \<and> A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r))"
   416 proof-
   417   let ?phi = "\<lambda>A. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r)"
   418   have "wf r \<longleftrightarrow> (\<forall>A. ?phi A)"
   419     apply (auto simp: ex_in_conv [THEN sym])
   420      apply (erule wfE_min)
   421       apply assumption
   422      apply blast
   423     apply (rule wfI_min)
   424     apply fast
   425     done
   426   also have "(\<forall>A. ?phi A) \<longleftrightarrow> (\<forall>B \<subseteq> Field r. ?phi B)"
   427   proof
   428     assume "\<forall>A. ?phi A"
   429     then show "\<forall>B \<subseteq> Field r. ?phi B" by simp
   430   next
   431     assume *: "\<forall>B \<subseteq> Field r. ?phi B"
   432     show "\<forall>A. ?phi A"
   433     proof clarify
   434       fix A :: "'a set"
   435       assume **: "A \<noteq> {}"
   436       define B where "B = A \<inter> Field r"
   437       show "\<exists>a \<in> A. \<forall>a' \<in> A. (a', a) \<notin> r"
   438       proof (cases "B = {}")
   439         case True
   440         with ** obtain a where a: "a \<in> A" "a \<notin> Field r"
   441           unfolding B_def by blast
   442         with a have "\<forall>a' \<in> A. (a',a) \<notin> r"
   443           unfolding Field_def by blast
   444         with a show ?thesis by blast
   445       next
   446         case False
   447         have "B \<subseteq> Field r" unfolding B_def by blast
   448         with False * obtain a where a: "a \<in> B" "\<forall>a' \<in> B. (a', a) \<notin> r"
   449           by blast
   450         have "(a', a) \<notin> r" if "a' \<in> A" for a'
   451         proof
   452           assume a'a: "(a', a) \<in> r"
   453           with that have "a' \<in> B" unfolding B_def Field_def by blast
   454           with a a'a show False by blast
   455         qed
   456         with a show ?thesis unfolding B_def by blast
   457       qed
   458     qed
   459   qed
   460   finally show ?thesis by blast
   461 qed
   462 
   463 
   464 subsubsection \<open>Characterizations of well-foundedness\<close>
   465 
   466 text \<open>
   467   The next lemma and its corollary enable one to prove that a linear order is
   468   a well-order in a way which is more standard than via well-foundedness of
   469   the strict version of the relation.
   470 \<close>
   471 
   472 lemma Linear_order_wf_diff_Id:
   473   assumes "Linear_order r"
   474   shows "wf (r - Id) \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
   475 proof (cases "r \<subseteq> Id")
   476   case True
   477   then have *: "r - Id = {}" by blast
   478   have "wf (r - Id)" by (simp add: *)
   479   moreover have "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r"
   480     if *: "A \<subseteq> Field r" and **: "A \<noteq> {}" for A
   481   proof -
   482     from \<open>Linear_order r\<close> True
   483     obtain a where a: "r = {} \<or> r = {(a, a)}"
   484       unfolding order_on_defs using Total_subset_Id [of r] by blast
   485     with * ** have "A = {a} \<and> r = {(a, a)}"
   486       unfolding Field_def by blast
   487     with a show ?thesis by blast
   488   qed
   489   ultimately show ?thesis by blast
   490 next
   491   case False
   492   with \<open>Linear_order r\<close> have Field: "Field r = Field (r - Id)"
   493     unfolding order_on_defs using Total_Id_Field [of r] by blast
   494   show ?thesis
   495   proof
   496     assume *: "wf (r - Id)"
   497     show "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
   498     proof clarify
   499       fix A
   500       assume **: "A \<subseteq> Field r" and ***: "A \<noteq> {}"
   501       then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   502         using Field * unfolding wf_eq_minimal2 by simp
   503       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
   504         using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** by blast
   505       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r" by blast
   506     qed
   507   next
   508     assume *: "\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r)"
   509     show "wf (r - Id)"
   510       unfolding wf_eq_minimal2
   511     proof clarify
   512       fix A
   513       assume **: "A \<subseteq> Field(r - Id)" and ***: "A \<noteq> {}"
   514       then have "\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r"
   515         using Field * by simp
   516       moreover have "\<forall>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r \<longleftrightarrow> (a', a) \<notin> r - Id"
   517         using Linear_order_in_diff_Id [OF \<open>Linear_order r\<close>] ** mono_Field[of "r - Id" r] by blast
   518       ultimately show "\<exists>a \<in> A. \<forall>a' \<in> A. (a',a) \<notin> r - Id"
   519         by blast
   520     qed
   521   qed
   522 qed
   523 
   524 corollary Linear_order_Well_order_iff:
   525   "Linear_order r \<Longrightarrow>
   526     Well_order r \<longleftrightarrow> (\<forall>A \<subseteq> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a, a') \<in> r))"
   527   unfolding well_order_on_def using Linear_order_wf_diff_Id[of r] by blast
   528 
   529 end