1(* Title: HOL/BNF_Wellorder_Relation.thy 2 Author: Andrei Popescu, TU Muenchen 3 Copyright 2012 4 5Well-order relations as needed by bounded natural functors. 6*) 7 8section \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close> 9 10theory BNF_Wellorder_Relation 11imports Order_Relation 12begin 13 14text\<open>In this section, we develop basic concepts and results pertaining 15to well-order relations. Note that we consider well-order relations 16as {\em non-strict relations}, 17i.e., as containing the diagonals of their fields.\<close> 18 19locale wo_rel = 20 fixes r :: "'a rel" 21 assumes WELL: "Well_order r" 22begin 23 24text\<open>The following context encompasses all this section. In other words, 25for the whole section, we consider a fixed well-order relation @{term "r"}.\<close> 26 27(* context wo_rel *) 28 29abbreviation under where "under \<equiv> Order_Relation.under r" 30abbreviation underS where "underS \<equiv> Order_Relation.underS r" 31abbreviation Under where "Under \<equiv> Order_Relation.Under r" 32abbreviation UnderS where "UnderS \<equiv> Order_Relation.UnderS r" 33abbreviation above where "above \<equiv> Order_Relation.above r" 34abbreviation aboveS where "aboveS \<equiv> Order_Relation.aboveS r" 35abbreviation Above where "Above \<equiv> Order_Relation.Above r" 36abbreviation AboveS where "AboveS \<equiv> Order_Relation.AboveS r" 37abbreviation ofilter where "ofilter \<equiv> Order_Relation.ofilter r" 38lemmas ofilter_def = Order_Relation.ofilter_def[of r] 39 40 41subsection \<open>Auxiliaries\<close> 42 43lemma REFL: "Refl r" 44using WELL order_on_defs[of _ r] by auto 45 46lemma TRANS: "trans r" 47using WELL order_on_defs[of _ r] by auto 48 49lemma ANTISYM: "antisym r" 50using WELL order_on_defs[of _ r] by auto 51 52lemma TOTAL: "Total r" 53using WELL order_on_defs[of _ r] by auto 54 55lemma TOTALS: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r" 56using REFL TOTAL refl_on_def[of _ r] total_on_def[of _ r] by force 57 58lemma LIN: "Linear_order r" 59using WELL well_order_on_def[of _ r] by auto 60 61lemma WF: "wf (r - Id)" 62using WELL well_order_on_def[of _ r] by auto 63 64lemma cases_Total: 65"\<And> phi a b. \<lbrakk>{a,b} <= Field r; ((a,b) \<in> r \<Longrightarrow> phi a b); ((b,a) \<in> r \<Longrightarrow> phi a b)\<rbrakk> 66 \<Longrightarrow> phi a b" 67using TOTALS by auto 68 69lemma cases_Total3: 70"\<And> phi a b. \<lbrakk>{a,b} \<le> Field r; ((a,b) \<in> r - Id \<or> (b,a) \<in> r - Id \<Longrightarrow> phi a b); 71 (a = b \<Longrightarrow> phi a b)\<rbrakk> \<Longrightarrow> phi a b" 72using TOTALS by auto 73 74 75subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close> 76 77text\<open>Here we provide induction and recursion principles specific to {\em non-strict} 78well-order relations. 79Although minor variations of those for well-founded relations, they will be useful 80for doing away with the tediousness of 81having to take out the diagonal each time in order to switch to a well-founded relation.\<close> 82 83lemma well_order_induct: 84assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x" 85shows "P a" 86proof- 87 have "\<And>x. \<forall>y. (y, x) \<in> r - Id \<longrightarrow> P y \<Longrightarrow> P x" 88 using IND by blast 89 thus "P a" using WF wf_induct[of "r - Id" P a] by blast 90qed 91 92definition 93worec :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 94where 95"worec F \<equiv> wfrec (r - Id) F" 96 97definition 98adm_wo :: "(('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" 99where 100"adm_wo H \<equiv> \<forall>f g x. (\<forall>y \<in> underS x. f y = g y) \<longrightarrow> H f x = H g x" 101 102lemma worec_fixpoint: 103assumes ADM: "adm_wo H" 104shows "worec H = H (worec H)" 105proof- 106 let ?rS = "r - Id" 107 have "adm_wf (r - Id) H" 108 unfolding adm_wf_def 109 using ADM adm_wo_def[of H] underS_def[of r] by auto 110 hence "wfrec ?rS H = H (wfrec ?rS H)" 111 using WF wfrec_fixpoint[of ?rS H] by simp 112 thus ?thesis unfolding worec_def . 113qed 114 115 116subsection \<open>The notions of maximum, minimum, supremum, successor and order filter\<close> 117 118text\<open> 119We define the successor {\em of a set}, and not of an element (the latter is of course 120a particular case). Also, we define the maximum {\em of two elements}, \<open>max2\<close>, 121and the minimum {\em of a set}, \<open>minim\<close> -- we chose these variants since we 122consider them the most useful for well-orders. The minimum is defined in terms of the 123auxiliary relational operator \<open>isMinim\<close>. Then, supremum and successor are 124defined in terms of minimum as expected. 125The minimum is only meaningful for non-empty sets, and the successor is only 126meaningful for sets for which strict upper bounds exist. 127Order filters for well-orders are also known as ``initial segments".\<close> 128 129definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 130where "max2 a b \<equiv> if (a,b) \<in> r then b else a" 131 132definition isMinim :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" 133where "isMinim A b \<equiv> b \<in> A \<and> (\<forall>a \<in> A. (b,a) \<in> r)" 134 135definition minim :: "'a set \<Rightarrow> 'a" 136where "minim A \<equiv> THE b. isMinim A b" 137 138definition supr :: "'a set \<Rightarrow> 'a" 139where "supr A \<equiv> minim (Above A)" 140 141definition suc :: "'a set \<Rightarrow> 'a" 142where "suc A \<equiv> minim (AboveS A)" 143 144 145subsubsection \<open>Properties of max2\<close> 146 147lemma max2_greater_among: 148assumes "a \<in> Field r" and "b \<in> Field r" 149shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r \<and> max2 a b \<in> {a,b}" 150proof- 151 {assume "(a,b) \<in> r" 152 hence ?thesis using max2_def assms REFL refl_on_def 153 by (auto simp add: refl_on_def) 154 } 155 moreover 156 {assume "a = b" 157 hence "(a,b) \<in> r" using REFL assms 158 by (auto simp add: refl_on_def) 159 } 160 moreover 161 {assume *: "a \<noteq> b \<and> (b,a) \<in> r" 162 hence "(a,b) \<notin> r" using ANTISYM 163 by (auto simp add: antisym_def) 164 hence ?thesis using * max2_def assms REFL refl_on_def 165 by (auto simp add: refl_on_def) 166 } 167 ultimately show ?thesis using assms TOTAL 168 total_on_def[of "Field r" r] by blast 169qed 170 171lemma max2_greater: 172assumes "a \<in> Field r" and "b \<in> Field r" 173shows "(a, max2 a b) \<in> r \<and> (b, max2 a b) \<in> r" 174using assms by (auto simp add: max2_greater_among) 175 176lemma max2_among: 177assumes "a \<in> Field r" and "b \<in> Field r" 178shows "max2 a b \<in> {a, b}" 179using assms max2_greater_among[of a b] by simp 180 181lemma max2_equals1: 182assumes "a \<in> Field r" and "b \<in> Field r" 183shows "(max2 a b = a) = ((b,a) \<in> r)" 184using assms ANTISYM unfolding antisym_def using TOTALS 185by(auto simp add: max2_def max2_among) 186 187lemma max2_equals2: 188assumes "a \<in> Field r" and "b \<in> Field r" 189shows "(max2 a b = b) = ((a,b) \<in> r)" 190using assms ANTISYM unfolding antisym_def using TOTALS 191unfolding max2_def by auto 192 193 194subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close> 195 196lemma isMinim_unique: 197assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'" 198shows "a = a'" 199proof- 200 {have "a \<in> B" 201 using MINIM isMinim_def by simp 202 hence "(a',a) \<in> r" 203 using MINIM' isMinim_def by simp 204 } 205 moreover 206 {have "a' \<in> B" 207 using MINIM' isMinim_def by simp 208 hence "(a,a') \<in> r" 209 using MINIM isMinim_def by simp 210 } 211 ultimately 212 show ?thesis using ANTISYM antisym_def[of r] by blast 213qed 214 215lemma Well_order_isMinim_exists: 216assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}" 217shows "\<exists>b. isMinim B b" 218proof- 219 from spec[OF WF[unfolded wf_eq_minimal[of "r - Id"]], of B] NE obtain b where 220 *: "b \<in> B \<and> (\<forall>b'. b' \<noteq> b \<and> (b',b) \<in> r \<longrightarrow> b' \<notin> B)" by auto 221 show ?thesis 222 proof(simp add: isMinim_def, rule exI[of _ b], auto) 223 show "b \<in> B" using * by simp 224 next 225 fix b' assume As: "b' \<in> B" 226 hence **: "b \<in> Field r \<and> b' \<in> Field r" using As SUB * by auto 227 (* *) 228 from As * have "b' = b \<or> (b',b) \<notin> r" by auto 229 moreover 230 {assume "b' = b" 231 hence "(b,b') \<in> r" 232 using ** REFL by (auto simp add: refl_on_def) 233 } 234 moreover 235 {assume "b' \<noteq> b \<and> (b',b) \<notin> r" 236 hence "(b,b') \<in> r" 237 using ** TOTAL by (auto simp add: total_on_def) 238 } 239 ultimately show "(b,b') \<in> r" by blast 240 qed 241qed 242 243lemma minim_isMinim: 244assumes SUB: "B \<le> Field r" and NE: "B \<noteq> {}" 245shows "isMinim B (minim B)" 246proof- 247 let ?phi = "(\<lambda> b. isMinim B b)" 248 from assms Well_order_isMinim_exists 249 obtain b where *: "?phi b" by blast 250 moreover 251 have "\<And> b'. ?phi b' \<Longrightarrow> b' = b" 252 using isMinim_unique * by auto 253 ultimately show ?thesis 254 unfolding minim_def using theI[of ?phi b] by blast 255qed 256 257subsubsection\<open>Properties of minim\<close> 258 259lemma minim_in: 260assumes "B \<le> Field r" and "B \<noteq> {}" 261shows "minim B \<in> B" 262proof- 263 from minim_isMinim[of B] assms 264 have "isMinim B (minim B)" by simp 265 thus ?thesis by (simp add: isMinim_def) 266qed 267 268lemma minim_inField: 269assumes "B \<le> Field r" and "B \<noteq> {}" 270shows "minim B \<in> Field r" 271proof- 272 have "minim B \<in> B" using assms by (simp add: minim_in) 273 thus ?thesis using assms by blast 274qed 275 276lemma minim_least: 277assumes SUB: "B \<le> Field r" and IN: "b \<in> B" 278shows "(minim B, b) \<in> r" 279proof- 280 from minim_isMinim[of B] assms 281 have "isMinim B (minim B)" by auto 282 thus ?thesis by (auto simp add: isMinim_def IN) 283qed 284 285lemma equals_minim: 286assumes SUB: "B \<le> Field r" and IN: "a \<in> B" and 287 LEAST: "\<And> b. b \<in> B \<Longrightarrow> (a,b) \<in> r" 288shows "a = minim B" 289proof- 290 from minim_isMinim[of B] assms 291 have "isMinim B (minim B)" by auto 292 moreover have "isMinim B a" using IN LEAST isMinim_def by auto 293 ultimately show ?thesis 294 using isMinim_unique by auto 295qed 296 297subsubsection\<open>Properties of successor\<close> 298 299lemma suc_AboveS: 300assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" 301shows "suc B \<in> AboveS B" 302proof(unfold suc_def) 303 have "AboveS B \<le> Field r" 304 using AboveS_Field[of r] by auto 305 thus "minim (AboveS B) \<in> AboveS B" 306 using assms by (simp add: minim_in) 307qed 308 309lemma suc_greater: 310assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}" and 311 IN: "b \<in> B" 312shows "suc B \<noteq> b \<and> (b,suc B) \<in> r" 313proof- 314 from assms suc_AboveS 315 have "suc B \<in> AboveS B" by simp 316 with IN AboveS_def[of r] show ?thesis by simp 317qed 318 319lemma suc_least_AboveS: 320assumes ABOVES: "a \<in> AboveS B" 321shows "(suc B,a) \<in> r" 322proof(unfold suc_def) 323 have "AboveS B \<le> Field r" 324 using AboveS_Field[of r] by auto 325 thus "(minim (AboveS B),a) \<in> r" 326 using assms minim_least by simp 327qed 328 329lemma suc_inField: 330assumes "B \<le> Field r" and "AboveS B \<noteq> {}" 331shows "suc B \<in> Field r" 332proof- 333 have "suc B \<in> AboveS B" using suc_AboveS assms by simp 334 thus ?thesis 335 using assms AboveS_Field[of r] by auto 336qed 337 338lemma equals_suc_AboveS: 339assumes SUB: "B \<le> Field r" and ABV: "a \<in> AboveS B" and 340 MINIM: "\<And> a'. a' \<in> AboveS B \<Longrightarrow> (a,a') \<in> r" 341shows "a = suc B" 342proof(unfold suc_def) 343 have "AboveS B \<le> Field r" 344 using AboveS_Field[of r B] by auto 345 thus "a = minim (AboveS B)" 346 using assms equals_minim 347 by simp 348qed 349 350lemma suc_underS: 351assumes IN: "a \<in> Field r" 352shows "a = suc (underS a)" 353proof- 354 have "underS a \<le> Field r" 355 using underS_Field[of r] by auto 356 moreover 357 have "a \<in> AboveS (underS a)" 358 using in_AboveS_underS IN by fast 359 moreover 360 have "\<forall>a' \<in> AboveS (underS a). (a,a') \<in> r" 361 proof(clarify) 362 fix a' 363 assume *: "a' \<in> AboveS (underS a)" 364 hence **: "a' \<in> Field r" 365 using AboveS_Field by fast 366 {assume "(a,a') \<notin> r" 367 hence "a' = a \<or> (a',a) \<in> r" 368 using TOTAL IN ** by (auto simp add: total_on_def) 369 moreover 370 {assume "a' = a" 371 hence "(a,a') \<in> r" 372 using REFL IN ** by (auto simp add: refl_on_def) 373 } 374 moreover 375 {assume "a' \<noteq> a \<and> (a',a) \<in> r" 376 hence "a' \<in> underS a" 377 unfolding underS_def by simp 378 hence "a' \<notin> AboveS (underS a)" 379 using AboveS_disjoint by fast 380 with * have False by simp 381 } 382 ultimately have "(a,a') \<in> r" by blast 383 } 384 thus "(a, a') \<in> r" by blast 385 qed 386 ultimately show ?thesis 387 using equals_suc_AboveS by auto 388qed 389 390 391subsubsection \<open>Properties of order filters\<close> 392 393lemma under_ofilter: 394"ofilter (under a)" 395proof(unfold ofilter_def under_def, auto simp add: Field_def) 396 fix aa x 397 assume "(aa,a) \<in> r" "(x,aa) \<in> r" 398 thus "(x,a) \<in> r" 399 using TRANS trans_def[of r] by blast 400qed 401 402lemma underS_ofilter: 403"ofilter (underS a)" 404proof(unfold ofilter_def underS_def under_def, auto simp add: Field_def) 405 fix aa assume "(a, aa) \<in> r" "(aa, a) \<in> r" and DIFF: "aa \<noteq> a" 406 thus False 407 using ANTISYM antisym_def[of r] by blast 408next 409 fix aa x 410 assume "(aa,a) \<in> r" "aa \<noteq> a" "(x,aa) \<in> r" 411 thus "(x,a) \<in> r" 412 using TRANS trans_def[of r] by blast 413qed 414 415lemma Field_ofilter: 416"ofilter (Field r)" 417by(unfold ofilter_def under_def, auto simp add: Field_def) 418 419lemma ofilter_underS_Field: 420"ofilter A = ((\<exists>a \<in> Field r. A = underS a) \<or> (A = Field r))" 421proof 422 assume "(\<exists>a\<in>Field r. A = underS a) \<or> A = Field r" 423 thus "ofilter A" 424 by (auto simp: underS_ofilter Field_ofilter) 425next 426 assume *: "ofilter A" 427 let ?One = "(\<exists>a\<in>Field r. A = underS a)" 428 let ?Two = "(A = Field r)" 429 show "?One \<or> ?Two" 430 proof(cases ?Two, simp) 431 let ?B = "(Field r) - A" 432 let ?a = "minim ?B" 433 assume "A \<noteq> Field r" 434 moreover have "A \<le> Field r" using * ofilter_def by simp 435 ultimately have 1: "?B \<noteq> {}" by blast 436 hence 2: "?a \<in> Field r" using minim_inField[of ?B] by blast 437 have 3: "?a \<in> ?B" using minim_in[of ?B] 1 by blast 438 hence 4: "?a \<notin> A" by blast 439 have 5: "A \<le> Field r" using * ofilter_def by auto 440 (* *) 441 moreover 442 have "A = underS ?a" 443 proof 444 show "A \<le> underS ?a" 445 proof(unfold underS_def, auto simp add: 4) 446 fix x assume **: "x \<in> A" 447 hence 11: "x \<in> Field r" using 5 by auto 448 have 12: "x \<noteq> ?a" using 4 ** by auto 449 have 13: "under x \<le> A" using * ofilter_def ** by auto 450 {assume "(x,?a) \<notin> r" 451 hence "(?a,x) \<in> r" 452 using TOTAL total_on_def[of "Field r" r] 453 2 4 11 12 by auto 454 hence "?a \<in> under x" using under_def[of r] by auto 455 hence "?a \<in> A" using ** 13 by blast 456 with 4 have False by simp 457 } 458 thus "(x,?a) \<in> r" by blast 459 qed 460 next 461 show "underS ?a \<le> A" 462 proof(unfold underS_def, auto) 463 fix x 464 assume **: "x \<noteq> ?a" and ***: "(x,?a) \<in> r" 465 hence 11: "x \<in> Field r" using Field_def by fastforce 466 {assume "x \<notin> A" 467 hence "x \<in> ?B" using 11 by auto 468 hence "(?a,x) \<in> r" using 3 minim_least[of ?B x] by blast 469 hence False 470 using ANTISYM antisym_def[of r] ** *** by auto 471 } 472 thus "x \<in> A" by blast 473 qed 474 qed 475 ultimately have ?One using 2 by blast 476 thus ?thesis by simp 477 qed 478qed 479 480lemma ofilter_UNION: 481"(\<And> i. i \<in> I \<Longrightarrow> ofilter(A i)) \<Longrightarrow> ofilter (\<Union>i \<in> I. A i)" 482unfolding ofilter_def by blast 483 484lemma ofilter_under_UNION: 485assumes "ofilter A" 486shows "A = (\<Union>a \<in> A. under a)" 487proof 488 have "\<forall>a \<in> A. under a \<le> A" 489 using assms ofilter_def by auto 490 thus "(\<Union>a \<in> A. under a) \<le> A" by blast 491next 492 have "\<forall>a \<in> A. a \<in> under a" 493 using REFL Refl_under_in[of r] assms ofilter_def[of A] by blast 494 thus "A \<le> (\<Union>a \<in> A. under a)" by blast 495qed 496 497subsubsection\<open>Other properties\<close> 498 499lemma ofilter_linord: 500assumes OF1: "ofilter A" and OF2: "ofilter B" 501shows "A \<le> B \<or> B \<le> A" 502proof(cases "A = Field r") 503 assume Case1: "A = Field r" 504 hence "B \<le> A" using OF2 ofilter_def by auto 505 thus ?thesis by simp 506next 507 assume Case2: "A \<noteq> Field r" 508 with ofilter_underS_Field OF1 obtain a where 509 1: "a \<in> Field r \<and> A = underS a" by auto 510 show ?thesis 511 proof(cases "B = Field r") 512 assume Case21: "B = Field r" 513 hence "A \<le> B" using OF1 ofilter_def by auto 514 thus ?thesis by simp 515 next 516 assume Case22: "B \<noteq> Field r" 517 with ofilter_underS_Field OF2 obtain b where 518 2: "b \<in> Field r \<and> B = underS b" by auto 519 have "a = b \<or> (a,b) \<in> r \<or> (b,a) \<in> r" 520 using 1 2 TOTAL total_on_def[of _ r] by auto 521 moreover 522 {assume "a = b" with 1 2 have ?thesis by auto 523 } 524 moreover 525 {assume "(a,b) \<in> r" 526 with underS_incr[of r] TRANS ANTISYM 1 2 527 have "A \<le> B" by auto 528 hence ?thesis by auto 529 } 530 moreover 531 {assume "(b,a) \<in> r" 532 with underS_incr[of r] TRANS ANTISYM 1 2 533 have "B \<le> A" by auto 534 hence ?thesis by auto 535 } 536 ultimately show ?thesis by blast 537 qed 538qed 539 540lemma ofilter_AboveS_Field: 541assumes "ofilter A" 542shows "A \<union> (AboveS A) = Field r" 543proof 544 show "A \<union> (AboveS A) \<le> Field r" 545 using assms ofilter_def AboveS_Field[of r] by auto 546next 547 {fix x assume *: "x \<in> Field r" and **: "x \<notin> A" 548 {fix y assume ***: "y \<in> A" 549 with ** have 1: "y \<noteq> x" by auto 550 {assume "(y,x) \<notin> r" 551 moreover 552 have "y \<in> Field r" using assms ofilter_def *** by auto 553 ultimately have "(x,y) \<in> r" 554 using 1 * TOTAL total_on_def[of _ r] by auto 555 with *** assms ofilter_def under_def[of r] have "x \<in> A" by auto 556 with ** have False by contradiction 557 } 558 hence "(y,x) \<in> r" by blast 559 with 1 have "y \<noteq> x \<and> (y,x) \<in> r" by auto 560 } 561 with * have "x \<in> AboveS A" unfolding AboveS_def by auto 562 } 563 thus "Field r \<le> A \<union> (AboveS A)" by blast 564qed 565 566lemma suc_ofilter_in: 567assumes OF: "ofilter A" and ABOVE_NE: "AboveS A \<noteq> {}" and 568 REL: "(b,suc A) \<in> r" and DIFF: "b \<noteq> suc A" 569shows "b \<in> A" 570proof- 571 have *: "suc A \<in> Field r \<and> b \<in> Field r" 572 using WELL REL well_order_on_domain[of "Field r"] by auto 573 {assume **: "b \<notin> A" 574 hence "b \<in> AboveS A" 575 using OF * ofilter_AboveS_Field by auto 576 hence "(suc A, b) \<in> r" 577 using suc_least_AboveS by auto 578 hence False using REL DIFF ANTISYM * 579 by (auto simp add: antisym_def) 580 } 581 thus ?thesis by blast 582qed 583 584end (* context wo_rel *) 585 586end 587