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