1(* Title: HOL/Order_Relation.thy 2 Author: Tobias Nipkow 3 Author: Andrei Popescu, TU Muenchen 4*) 5 6section \<open>Orders as Relations\<close> 7 8theory Order_Relation 9imports Wfrec 10begin 11 12subsection \<open>Orders on a set\<close> 13 14definition "preorder_on A r \<equiv> refl_on A r \<and> trans r" 15 16definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r" 17 18definition "linear_order_on A r \<equiv> partial_order_on A r \<and> total_on A r" 19 20definition "strict_linear_order_on A r \<equiv> trans r \<and> irrefl r \<and> total_on A r" 21 22definition "well_order_on A r \<equiv> linear_order_on A r \<and> wf(r - Id)" 23 24lemmas 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 29lemma preorder_on_empty[simp]: "preorder_on {} {}" 30 by (simp add: preorder_on_def trans_def) 31 32lemma partial_order_on_empty[simp]: "partial_order_on {} {}" 33 by (simp add: partial_order_on_def) 34 35lemma lnear_order_on_empty[simp]: "linear_order_on {} {}" 36 by (simp add: linear_order_on_def) 37 38lemma well_order_on_empty[simp]: "well_order_on {} {}" 39 by (simp add: well_order_on_def) 40 41 42lemma preorder_on_converse[simp]: "preorder_on A (r\<inverse>) = preorder_on A r" 43 by (simp add: preorder_on_def) 44 45lemma 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 48lemma 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 52lemma 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 55lemma linear_order_on_singleton [simp]: "linear_order_on {x} {(x, x)}" 56 by (simp add: order_on_defs) 57 58lemma 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 64lemma 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 71subsection \<open>Orders on the field\<close> 72 73abbreviation "Refl r \<equiv> refl_on (Field r) r" 74 75abbreviation "Preorder r \<equiv> preorder_on (Field r) r" 76 77abbreviation "Partial_order r \<equiv> partial_order_on (Field r) r" 78 79abbreviation "Total r \<equiv> total_on (Field r) r" 80 81abbreviation "Linear_order r \<equiv> linear_order_on (Field r) r" 82 83abbreviation "Well_order r \<equiv> well_order_on (Field r) r" 84 85 86lemma 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 94lemma 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 98lemma 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") 104proof 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 112next 113 assume ?rhs 114 then show ?lhs by fast 115qed 116 117lemma 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 121lemma 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] 126proof 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 134qed 135 136 137subsection \<open>Orders on a type\<close> 138 139abbreviation "strict_linear_order \<equiv> strict_linear_order_on UNIV" 140 141abbreviation "linear_order \<equiv> linear_order_on UNIV" 142 143abbreviation "well_order \<equiv> well_order_on UNIV" 144 145 146subsection \<open>Order-like relations\<close> 147 148text \<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 155subsubsection \<open>Auxiliaries\<close> 156 157lemma 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 160corollary 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 163lemma 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 166lemma 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 169lemma Total_subset_Id: 170 assumes "Total r" 171 and "r \<subseteq> Id" 172 shows "r = {} \<or> (\<exists>a. r = {(a, a)})" 173proof - 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 191qed 192 193lemma 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 201subsubsection \<open>The upper and lower bounds operators\<close> 202 203text \<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 212definition under :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 213 where "under r a \<equiv> {b. (b, a) \<in> r}" 214 215definition underS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 216 where "underS r a \<equiv> {b. b \<noteq> a \<and> (b, a) \<in> r}" 217 218definition 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 221definition 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 224definition above :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 225 where "above r a \<equiv> {b. (a, b) \<in> r}" 226 227definition aboveS :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a set" 228 where "aboveS r a \<equiv> {b. b \<noteq> a \<and> (a, b) \<in> r}" 229 230definition 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 233definition 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 236definition 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 239text \<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 245lemma underS_subset_under: "underS r a \<subseteq> under r a" 246 by (auto simp add: underS_def under_def) 247 248lemma underS_notIn: "a \<notin> underS r a" 249 by (simp add: underS_def) 250 251lemma 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 254lemma AboveS_disjoint: "A \<inter> (AboveS r A) = {}" 255 by (auto simp add: AboveS_def) 256 257lemma 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 260lemma 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 264lemma underS_empty: "a \<notin> Field r \<Longrightarrow> underS r a = {}" 265 by (auto simp: Field_def underS_def) 266 267lemma under_Field: "under r a \<subseteq> Field r" 268 by (auto simp: under_def Field_def) 269 270lemma underS_Field: "underS r a \<subseteq> Field r" 271 by (auto simp: underS_def Field_def) 272 273lemma underS_Field2: "a \<in> Field r \<Longrightarrow> underS r a \<subset> Field r" 274 using underS_notIn underS_Field by fast 275 276lemma 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 279lemma AboveS_Field: "AboveS r A \<subseteq> Field r" 280 by (auto simp: AboveS_def Field_def) 281 282lemma 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 287proof auto 288 fix x assume "(x, a) \<in> r" 289 with assms trans_def[of r] show "(x, b) \<in> r" by blast 290qed 291 292lemma 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 298proof 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 302next 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 306qed 307 308lemma 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") 314proof 315 assume ?rhs 316 with \<open>Linear_order r\<close> show ?lhs 317 by (simp add: order_on_defs underS_incr) 318next 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 330qed 331 332lemma 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) 339proof (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 344next 345 case prems: (2 x) 346 show ?case 347 by (rule step) (use prems in \<open>auto simp: aboveS_def intro: FieldI2\<close>) 348qed 349 350 351subsection \<open>Variations on Well-Founded Relations\<close> 352 353text \<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 361subsubsection \<open>Characterizations of well-foundedness\<close> 362 363text \<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 369lemma trans_wf_iff: 370 assumes "trans r" 371 shows "wf r \<longleftrightarrow> (\<forall>a. wf (r \<inter> (r\<inverse>``{a} \<times> r\<inverse>``{a})))" 372proof - 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 398qed 399 400text\<open>A transitive relation is well-founded if all initial segments are finite.\<close> 401corollary wf_finite_segments: 402 assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}" 403 shows "wf (r)" 404proof (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 410qed 411 412text \<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 415lemma 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))" 416proof- 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 461qed 462 463 464subsubsection \<open>Characterizations of well-foundedness\<close> 465 466text \<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 472lemma 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))" 475proof (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 490next 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 522qed 523 524corollary 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 529end 530