src/HOL/Order_Relation.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (23 months ago) changeset 66831 29ea2b900a05 parent 63952 354808e9f44b child 68484 59793df7f853 permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     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 Wellfounded}:
```
```   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
```