1(* Title: HOL/BNF_Wellorder_Constructions.thy 2 Author: Andrei Popescu, TU Muenchen 3 Copyright 2012 4 5Constructions on wellorders as needed by bounded natural functors. 6*) 7 8section \<open>Constructions on Wellorders as Needed by Bounded Natural Functors\<close> 9 10theory BNF_Wellorder_Constructions 11imports BNF_Wellorder_Embedding 12begin 13 14text \<open>In this section, we study basic constructions on well-orders, such as restriction to 15a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders, 16and bounded square. We also define between well-orders 17the relations \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>), 18\<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>), and 19\<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>). We study the 20connections between these relations, order filters, and the aforementioned constructions. 21A main result of this section is that \<open><o\<close> is well-founded.\<close> 22 23 24subsection \<open>Restriction to a set\<close> 25 26abbreviation Restr :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a rel" 27where "Restr r A \<equiv> r Int (A \<times> A)" 28 29lemma Restr_subset: 30"A \<le> B \<Longrightarrow> Restr (Restr r B) A = Restr r A" 31by blast 32 33lemma Restr_Field: "Restr r (Field r) = r" 34unfolding Field_def by auto 35 36lemma Refl_Restr: "Refl r \<Longrightarrow> Refl(Restr r A)" 37unfolding refl_on_def Field_def by auto 38 39lemma linear_order_on_Restr: 40 "linear_order_on A r \<Longrightarrow> linear_order_on (A \<inter> above r x) (Restr r (above r x))" 41by(simp add: order_on_defs refl_on_def trans_def antisym_def total_on_def)(safe; blast) 42 43lemma antisym_Restr: 44"antisym r \<Longrightarrow> antisym(Restr r A)" 45unfolding antisym_def Field_def by auto 46 47lemma Total_Restr: 48"Total r \<Longrightarrow> Total(Restr r A)" 49unfolding total_on_def Field_def by auto 50 51lemma trans_Restr: 52"trans r \<Longrightarrow> trans(Restr r A)" 53unfolding trans_def Field_def by blast 54 55lemma Preorder_Restr: 56"Preorder r \<Longrightarrow> Preorder(Restr r A)" 57unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr) 58 59lemma Partial_order_Restr: 60"Partial_order r \<Longrightarrow> Partial_order(Restr r A)" 61unfolding partial_order_on_def by (simp add: Preorder_Restr antisym_Restr) 62 63lemma Linear_order_Restr: 64"Linear_order r \<Longrightarrow> Linear_order(Restr r A)" 65unfolding linear_order_on_def by (simp add: Partial_order_Restr Total_Restr) 66 67lemma Well_order_Restr: 68assumes "Well_order r" 69shows "Well_order(Restr r A)" 70proof- 71 have "Restr r A - Id \<le> r - Id" using Restr_subset by blast 72 hence "wf(Restr r A - Id)" using assms 73 using well_order_on_def wf_subset by blast 74 thus ?thesis using assms unfolding well_order_on_def 75 by (simp add: Linear_order_Restr) 76qed 77 78lemma Field_Restr_subset: "Field(Restr r A) \<le> A" 79by (auto simp add: Field_def) 80 81lemma Refl_Field_Restr: 82"Refl r \<Longrightarrow> Field(Restr r A) = (Field r) Int A" 83unfolding refl_on_def Field_def by blast 84 85lemma Refl_Field_Restr2: 86"\<lbrakk>Refl r; A \<le> Field r\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" 87by (auto simp add: Refl_Field_Restr) 88 89lemma well_order_on_Restr: 90assumes WELL: "Well_order r" and SUB: "A \<le> Field r" 91shows "well_order_on A (Restr r A)" 92using assms 93using Well_order_Restr[of r A] Refl_Field_Restr2[of r A] 94 order_on_defs[of "Field r" r] by auto 95 96 97subsection \<open>Order filters versus restrictions and embeddings\<close> 98 99lemma Field_Restr_ofilter: 100"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> Field(Restr r A) = A" 101by (auto simp add: wo_rel_def wo_rel.ofilter_def wo_rel.REFL Refl_Field_Restr2) 102 103lemma ofilter_Restr_under: 104assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and IN: "a \<in> A" 105shows "under (Restr r A) a = under r a" 106using assms wo_rel_def 107proof(auto simp add: wo_rel.ofilter_def under_def) 108 fix b assume *: "a \<in> A" and "(b,a) \<in> r" 109 hence "b \<in> under r a \<and> a \<in> Field r" 110 unfolding under_def using Field_def by fastforce 111 thus "b \<in> A" using * assms by (auto simp add: wo_rel_def wo_rel.ofilter_def) 112qed 113 114lemma ofilter_embed: 115assumes "Well_order r" 116shows "wo_rel.ofilter r A = (A \<le> Field r \<and> embed (Restr r A) r id)" 117proof 118 assume *: "wo_rel.ofilter r A" 119 show "A \<le> Field r \<and> embed (Restr r A) r id" 120 proof(unfold embed_def, auto) 121 fix a assume "a \<in> A" thus "a \<in> Field r" using assms * 122 by (auto simp add: wo_rel_def wo_rel.ofilter_def) 123 next 124 fix a assume "a \<in> Field (Restr r A)" 125 thus "bij_betw id (under (Restr r A) a) (under r a)" using assms * 126 by (simp add: ofilter_Restr_under Field_Restr_ofilter) 127 qed 128next 129 assume *: "A \<le> Field r \<and> embed (Restr r A) r id" 130 hence "Field(Restr r A) \<le> Field r" 131 using assms embed_Field[of "Restr r A" r id] id_def 132 Well_order_Restr[of r] by auto 133 {fix a assume "a \<in> A" 134 hence "a \<in> Field(Restr r A)" using * assms 135 by (simp add: order_on_defs Refl_Field_Restr2) 136 hence "bij_betw id (under (Restr r A) a) (under r a)" 137 using * unfolding embed_def by auto 138 hence "under r a \<le> under (Restr r A) a" 139 unfolding bij_betw_def by auto 140 also have "\<dots> \<le> Field(Restr r A)" by (simp add: under_Field) 141 also have "\<dots> \<le> A" by (simp add: Field_Restr_subset) 142 finally have "under r a \<le> A" . 143 } 144 thus "wo_rel.ofilter r A" using assms * by (simp add: wo_rel_def wo_rel.ofilter_def) 145qed 146 147lemma ofilter_Restr_Int: 148assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" 149shows "wo_rel.ofilter (Restr r B) (A Int B)" 150proof- 151 let ?rB = "Restr r B" 152 have Well: "wo_rel r" unfolding wo_rel_def using WELL . 153 hence Refl: "Refl r" by (simp add: wo_rel.REFL) 154 hence Field: "Field ?rB = Field r Int B" 155 using Refl_Field_Restr by blast 156 have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL 157 by (simp add: Well_order_Restr wo_rel_def) 158 (* Main proof *) 159 show ?thesis using WellB assms 160 proof(auto simp add: wo_rel.ofilter_def under_def) 161 fix a assume "a \<in> A" and *: "a \<in> B" 162 hence "a \<in> Field r" using OFA Well by (auto simp add: wo_rel.ofilter_def) 163 with * show "a \<in> Field ?rB" using Field by auto 164 next 165 fix a b assume "a \<in> A" and "(b,a) \<in> r" 166 thus "b \<in> A" using Well OFA by (auto simp add: wo_rel.ofilter_def under_def) 167 qed 168qed 169 170lemma ofilter_Restr_subset: 171assumes WELL: "Well_order r" and OFA: "wo_rel.ofilter r A" and SUB: "A \<le> B" 172shows "wo_rel.ofilter (Restr r B) A" 173proof- 174 have "A Int B = A" using SUB by blast 175 thus ?thesis using assms ofilter_Restr_Int[of r A B] by auto 176qed 177 178lemma ofilter_subset_embed: 179assumes WELL: "Well_order r" and 180 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" 181shows "(A \<le> B) = (embed (Restr r A) (Restr r B) id)" 182proof- 183 let ?rA = "Restr r A" let ?rB = "Restr r B" 184 have Well: "wo_rel r" unfolding wo_rel_def using WELL . 185 hence Refl: "Refl r" by (simp add: wo_rel.REFL) 186 hence FieldA: "Field ?rA = Field r Int A" 187 using Refl_Field_Restr by blast 188 have FieldB: "Field ?rB = Field r Int B" 189 using Refl Refl_Field_Restr by blast 190 have WellA: "wo_rel ?rA \<and> Well_order ?rA" using WELL 191 by (simp add: Well_order_Restr wo_rel_def) 192 have WellB: "wo_rel ?rB \<and> Well_order ?rB" using WELL 193 by (simp add: Well_order_Restr wo_rel_def) 194 (* Main proof *) 195 show ?thesis 196 proof 197 assume *: "A \<le> B" 198 hence "wo_rel.ofilter (Restr r B) A" using assms 199 by (simp add: ofilter_Restr_subset) 200 hence "embed (Restr ?rB A) (Restr r B) id" 201 using WellB ofilter_embed[of "?rB" A] by auto 202 thus "embed (Restr r A) (Restr r B) id" 203 using * by (simp add: Restr_subset) 204 next 205 assume *: "embed (Restr r A) (Restr r B) id" 206 {fix a assume **: "a \<in> A" 207 hence "a \<in> Field r" using Well OFA by (auto simp add: wo_rel.ofilter_def) 208 with ** FieldA have "a \<in> Field ?rA" by auto 209 hence "a \<in> Field ?rB" using * WellA embed_Field[of ?rA ?rB id] by auto 210 hence "a \<in> B" using FieldB by auto 211 } 212 thus "A \<le> B" by blast 213 qed 214qed 215 216lemma ofilter_subset_embedS_iso: 217assumes WELL: "Well_order r" and 218 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" 219shows "((A < B) = (embedS (Restr r A) (Restr r B) id)) \<and> 220 ((A = B) = (iso (Restr r A) (Restr r B) id))" 221proof- 222 let ?rA = "Restr r A" let ?rB = "Restr r B" 223 have Well: "wo_rel r" unfolding wo_rel_def using WELL . 224 hence Refl: "Refl r" by (simp add: wo_rel.REFL) 225 hence "Field ?rA = Field r Int A" 226 using Refl_Field_Restr by blast 227 hence FieldA: "Field ?rA = A" using OFA Well 228 by (auto simp add: wo_rel.ofilter_def) 229 have "Field ?rB = Field r Int B" 230 using Refl Refl_Field_Restr by blast 231 hence FieldB: "Field ?rB = B" using OFB Well 232 by (auto simp add: wo_rel.ofilter_def) 233 (* Main proof *) 234 show ?thesis unfolding embedS_def iso_def 235 using assms ofilter_subset_embed[of r A B] 236 FieldA FieldB bij_betw_id_iff[of A B] by auto 237qed 238 239lemma ofilter_subset_embedS: 240assumes WELL: "Well_order r" and 241 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" 242shows "(A < B) = embedS (Restr r A) (Restr r B) id" 243using assms by (simp add: ofilter_subset_embedS_iso) 244 245lemma embed_implies_iso_Restr: 246assumes WELL: "Well_order r" and WELL': "Well_order r'" and 247 EMB: "embed r' r f" 248shows "iso r' (Restr r (f ` (Field r'))) f" 249proof- 250 let ?A' = "Field r'" 251 let ?r'' = "Restr r (f ` ?A')" 252 have 0: "Well_order ?r''" using WELL Well_order_Restr by blast 253 have 1: "wo_rel.ofilter r (f ` ?A')" using assms embed_Field_ofilter by blast 254 hence "Field ?r'' = f ` (Field r')" using WELL Field_Restr_ofilter by blast 255 hence "bij_betw f ?A' (Field ?r'')" 256 using EMB embed_inj_on WELL' unfolding bij_betw_def by blast 257 moreover 258 {have "\<forall>a b. (a,b) \<in> r' \<longrightarrow> a \<in> Field r' \<and> b \<in> Field r'" 259 unfolding Field_def by auto 260 hence "compat r' ?r'' f" 261 using assms embed_iff_compat_inj_on_ofilter 262 unfolding compat_def by blast 263 } 264 ultimately show ?thesis using WELL' 0 iso_iff3 by blast 265qed 266 267 268subsection \<open>The strict inclusion on proper ofilters is well-founded\<close> 269 270definition ofilterIncl :: "'a rel \<Rightarrow> 'a set rel" 271where 272"ofilterIncl r \<equiv> {(A,B). wo_rel.ofilter r A \<and> A \<noteq> Field r \<and> 273 wo_rel.ofilter r B \<and> B \<noteq> Field r \<and> A < B}" 274 275lemma wf_ofilterIncl: 276assumes WELL: "Well_order r" 277shows "wf(ofilterIncl r)" 278proof- 279 have Well: "wo_rel r" using WELL by (simp add: wo_rel_def) 280 hence Lo: "Linear_order r" by (simp add: wo_rel.LIN) 281 let ?h = "(\<lambda> A. wo_rel.suc r A)" 282 let ?rS = "r - Id" 283 have "wf ?rS" using WELL by (simp add: order_on_defs) 284 moreover 285 have "compat (ofilterIncl r) ?rS ?h" 286 proof(unfold compat_def ofilterIncl_def, 287 intro allI impI, simp, elim conjE) 288 fix A B 289 assume *: "wo_rel.ofilter r A" "A \<noteq> Field r" and 290 **: "wo_rel.ofilter r B" "B \<noteq> Field r" and ***: "A < B" 291 then obtain a and b where 0: "a \<in> Field r \<and> b \<in> Field r" and 292 1: "A = underS r a \<and> B = underS r b" 293 using Well by (auto simp add: wo_rel.ofilter_underS_Field) 294 hence "a \<noteq> b" using *** by auto 295 moreover 296 have "(a,b) \<in> r" using 0 1 Lo *** 297 by (auto simp add: underS_incl_iff) 298 moreover 299 have "a = wo_rel.suc r A \<and> b = wo_rel.suc r B" 300 using Well 0 1 by (simp add: wo_rel.suc_underS) 301 ultimately 302 show "(wo_rel.suc r A, wo_rel.suc r B) \<in> r \<and> wo_rel.suc r A \<noteq> wo_rel.suc r B" 303 by simp 304 qed 305 ultimately show "wf (ofilterIncl r)" by (simp add: compat_wf) 306qed 307 308 309subsection \<open>Ordering the well-orders by existence of embeddings\<close> 310 311text \<open>We define three relations between well-orders: 312\begin{itemize} 313\item \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>); 314\item \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>); 315\item \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>). 316\end{itemize} 317% 318The prefix "ord" and the index "o" in these names stand for "ordinal-like". 319These relations shall be proved to be inter-connected in a similar fashion as the trio 320\<open>\<le>\<close>, \<open><\<close>, \<open>=\<close> associated to a total order on a set. 321\<close> 322 323definition ordLeq :: "('a rel * 'a' rel) set" 324where 325"ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}" 326 327abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50) 328where "r <=o r' \<equiv> (r,r') \<in> ordLeq" 329 330abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50) 331where "r \<le>o r' \<equiv> r <=o r'" 332 333definition ordLess :: "('a rel * 'a' rel) set" 334where 335"ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}" 336 337abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50) 338where "r <o r' \<equiv> (r,r') \<in> ordLess" 339 340definition ordIso :: "('a rel * 'a' rel) set" 341where 342"ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}" 343 344abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50) 345where "r =o r' \<equiv> (r,r') \<in> ordIso" 346 347lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def 348 349lemma ordLeq_Well_order_simp: 350assumes "r \<le>o r'" 351shows "Well_order r \<and> Well_order r'" 352using assms unfolding ordLeq_def by simp 353 354text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders 355on potentially {\em distinct} types. However, some of the lemmas below, including the next one, 356restrict implicitly the type of these relations to \<open>(('a rel) * ('a rel)) set\<close> , i.e., 357to \<open>'a rel rel\<close>.\<close> 358 359lemma ordLeq_reflexive: 360"Well_order r \<Longrightarrow> r \<le>o r" 361unfolding ordLeq_def using id_embed[of r] by blast 362 363lemma ordLeq_transitive[trans]: 364assumes *: "r \<le>o r'" and **: "r' \<le>o r''" 365shows "r \<le>o r''" 366proof- 367 obtain f and f' 368 where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and 369 "embed r r' f" and "embed r' r'' f'" 370 using * ** unfolding ordLeq_def by blast 371 hence "embed r r'' (f' \<circ> f)" 372 using comp_embed[of r r' f r'' f'] by auto 373 thus "r \<le>o r''" unfolding ordLeq_def using 1 by auto 374qed 375 376lemma ordLeq_total: 377"\<lbrakk>Well_order r; Well_order r'\<rbrakk> \<Longrightarrow> r \<le>o r' \<or> r' \<le>o r" 378unfolding ordLeq_def using wellorders_totally_ordered by blast 379 380lemma ordIso_reflexive: 381"Well_order r \<Longrightarrow> r =o r" 382unfolding ordIso_def using id_iso[of r] by blast 383 384lemma ordIso_transitive[trans]: 385assumes *: "r =o r'" and **: "r' =o r''" 386shows "r =o r''" 387proof- 388 obtain f and f' 389 where 1: "Well_order r \<and> Well_order r' \<and> Well_order r''" and 390 "iso r r' f" and 3: "iso r' r'' f'" 391 using * ** unfolding ordIso_def by auto 392 hence "iso r r'' (f' \<circ> f)" 393 using comp_iso[of r r' f r'' f'] by auto 394 thus "r =o r''" unfolding ordIso_def using 1 by auto 395qed 396 397lemma ordIso_symmetric: 398assumes *: "r =o r'" 399shows "r' =o r" 400proof- 401 obtain f where 1: "Well_order r \<and> Well_order r'" and 402 2: "embed r r' f \<and> bij_betw f (Field r) (Field r')" 403 using * by (auto simp add: ordIso_def iso_def) 404 let ?f' = "inv_into (Field r) f" 405 have "embed r' r ?f' \<and> bij_betw ?f' (Field r') (Field r)" 406 using 1 2 by (simp add: bij_betw_inv_into inv_into_Field_embed_bij_betw) 407 thus "r' =o r" unfolding ordIso_def using 1 by (auto simp add: iso_def) 408qed 409 410lemma ordLeq_ordLess_trans[trans]: 411assumes "r \<le>o r'" and " r' <o r''" 412shows "r <o r''" 413proof- 414 have "Well_order r \<and> Well_order r''" 415 using assms unfolding ordLeq_def ordLess_def by auto 416 thus ?thesis using assms unfolding ordLeq_def ordLess_def 417 using embed_comp_embedS by blast 418qed 419 420lemma ordLess_ordLeq_trans[trans]: 421assumes "r <o r'" and " r' \<le>o r''" 422shows "r <o r''" 423proof- 424 have "Well_order r \<and> Well_order r''" 425 using assms unfolding ordLeq_def ordLess_def by auto 426 thus ?thesis using assms unfolding ordLeq_def ordLess_def 427 using embedS_comp_embed by blast 428qed 429 430lemma ordLeq_ordIso_trans[trans]: 431assumes "r \<le>o r'" and " r' =o r''" 432shows "r \<le>o r''" 433proof- 434 have "Well_order r \<and> Well_order r''" 435 using assms unfolding ordLeq_def ordIso_def by auto 436 thus ?thesis using assms unfolding ordLeq_def ordIso_def 437 using embed_comp_iso by blast 438qed 439 440lemma ordIso_ordLeq_trans[trans]: 441assumes "r =o r'" and " r' \<le>o r''" 442shows "r \<le>o r''" 443proof- 444 have "Well_order r \<and> Well_order r''" 445 using assms unfolding ordLeq_def ordIso_def by auto 446 thus ?thesis using assms unfolding ordLeq_def ordIso_def 447 using iso_comp_embed by blast 448qed 449 450lemma ordLess_ordIso_trans[trans]: 451assumes "r <o r'" and " r' =o r''" 452shows "r <o r''" 453proof- 454 have "Well_order r \<and> Well_order r''" 455 using assms unfolding ordLess_def ordIso_def by auto 456 thus ?thesis using assms unfolding ordLess_def ordIso_def 457 using embedS_comp_iso by blast 458qed 459 460lemma ordIso_ordLess_trans[trans]: 461assumes "r =o r'" and " r' <o r''" 462shows "r <o r''" 463proof- 464 have "Well_order r \<and> Well_order r''" 465 using assms unfolding ordLess_def ordIso_def by auto 466 thus ?thesis using assms unfolding ordLess_def ordIso_def 467 using iso_comp_embedS by blast 468qed 469 470lemma ordLess_not_embed: 471assumes "r <o r'" 472shows "\<not>(\<exists>f'. embed r' r f')" 473proof- 474 obtain f where 1: "Well_order r \<and> Well_order r'" and 2: "embed r r' f" and 475 3: " \<not> bij_betw f (Field r) (Field r')" 476 using assms unfolding ordLess_def by (auto simp add: embedS_def) 477 {fix f' assume *: "embed r' r f'" 478 hence "bij_betw f (Field r) (Field r')" using 1 2 479 by (simp add: embed_bothWays_Field_bij_betw) 480 with 3 have False by contradiction 481 } 482 thus ?thesis by blast 483qed 484 485lemma ordLess_Field: 486assumes OL: "r1 <o r2" and EMB: "embed r1 r2 f" 487shows "\<not> (f`(Field r1) = Field r2)" 488proof- 489 let ?A1 = "Field r1" let ?A2 = "Field r2" 490 obtain g where 491 0: "Well_order r1 \<and> Well_order r2" and 492 1: "embed r1 r2 g \<and> \<not>(bij_betw g ?A1 ?A2)" 493 using OL unfolding ordLess_def by (auto simp add: embedS_def) 494 hence "\<forall>a \<in> ?A1. f a = g a" 495 using 0 EMB embed_unique[of r1] by auto 496 hence "\<not>(bij_betw f ?A1 ?A2)" 497 using 1 bij_betw_cong[of ?A1] by blast 498 moreover 499 have "inj_on f ?A1" using EMB 0 by (simp add: embed_inj_on) 500 ultimately show ?thesis by (simp add: bij_betw_def) 501qed 502 503lemma ordLess_iff: 504"r <o r' = (Well_order r \<and> Well_order r' \<and> \<not>(\<exists>f'. embed r' r f'))" 505proof 506 assume *: "r <o r'" 507 hence "\<not>(\<exists>f'. embed r' r f')" using ordLess_not_embed[of r r'] by simp 508 with * show "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')" 509 unfolding ordLess_def by auto 510next 511 assume *: "Well_order r \<and> Well_order r' \<and> \<not> (\<exists>f'. embed r' r f')" 512 then obtain f where 1: "embed r r' f" 513 using wellorders_totally_ordered[of r r'] by blast 514 moreover 515 {assume "bij_betw f (Field r) (Field r')" 516 with * 1 have "embed r' r (inv_into (Field r) f) " 517 using inv_into_Field_embed_bij_betw[of r r' f] by auto 518 with * have False by blast 519 } 520 ultimately show "(r,r') \<in> ordLess" 521 unfolding ordLess_def using * by (fastforce simp add: embedS_def) 522qed 523 524lemma ordLess_irreflexive: "\<not> r <o r" 525proof 526 assume "r <o r" 527 hence "Well_order r \<and> \<not>(\<exists>f. embed r r f)" 528 unfolding ordLess_iff .. 529 moreover have "embed r r id" using id_embed[of r] . 530 ultimately show False by blast 531qed 532 533lemma ordLeq_iff_ordLess_or_ordIso: 534"r \<le>o r' = (r <o r' \<or> r =o r')" 535unfolding ordRels_def embedS_defs iso_defs by blast 536 537lemma ordIso_iff_ordLeq: 538"(r =o r') = (r \<le>o r' \<and> r' \<le>o r)" 539proof 540 assume "r =o r'" 541 then obtain f where 1: "Well_order r \<and> Well_order r' \<and> 542 embed r r' f \<and> bij_betw f (Field r) (Field r')" 543 unfolding ordIso_def iso_defs by auto 544 hence "embed r r' f \<and> embed r' r (inv_into (Field r) f)" 545 by (simp add: inv_into_Field_embed_bij_betw) 546 thus "r \<le>o r' \<and> r' \<le>o r" 547 unfolding ordLeq_def using 1 by auto 548next 549 assume "r \<le>o r' \<and> r' \<le>o r" 550 then obtain f and g where 1: "Well_order r \<and> Well_order r' \<and> 551 embed r r' f \<and> embed r' r g" 552 unfolding ordLeq_def by auto 553 hence "iso r r' f" by (auto simp add: embed_bothWays_iso) 554 thus "r =o r'" unfolding ordIso_def using 1 by auto 555qed 556 557lemma not_ordLess_ordLeq: 558"r <o r' \<Longrightarrow> \<not> r' \<le>o r" 559using ordLess_ordLeq_trans ordLess_irreflexive by blast 560 561lemma ordLess_or_ordLeq: 562assumes WELL: "Well_order r" and WELL': "Well_order r'" 563shows "r <o r' \<or> r' \<le>o r" 564proof- 565 have "r \<le>o r' \<or> r' \<le>o r" 566 using assms by (simp add: ordLeq_total) 567 moreover 568 {assume "\<not> r <o r' \<and> r \<le>o r'" 569 hence "r =o r'" using ordLeq_iff_ordLess_or_ordIso by blast 570 hence "r' \<le>o r" using ordIso_symmetric ordIso_iff_ordLeq by blast 571 } 572 ultimately show ?thesis by blast 573qed 574 575lemma not_ordLess_ordIso: 576"r <o r' \<Longrightarrow> \<not> r =o r'" 577using ordLess_ordIso_trans ordIso_symmetric ordLess_irreflexive by blast 578 579lemma not_ordLeq_iff_ordLess: 580assumes WELL: "Well_order r" and WELL': "Well_order r'" 581shows "(\<not> r' \<le>o r) = (r <o r')" 582using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast 583 584lemma not_ordLess_iff_ordLeq: 585assumes WELL: "Well_order r" and WELL': "Well_order r'" 586shows "(\<not> r' <o r) = (r \<le>o r')" 587using assms not_ordLess_ordLeq ordLess_or_ordLeq by blast 588 589lemma ordLess_transitive[trans]: 590"\<lbrakk>r <o r'; r' <o r''\<rbrakk> \<Longrightarrow> r <o r''" 591using ordLess_ordLeq_trans ordLeq_iff_ordLess_or_ordIso by blast 592 593corollary ordLess_trans: "trans ordLess" 594unfolding trans_def using ordLess_transitive by blast 595 596lemmas ordIso_equivalence = ordIso_transitive ordIso_reflexive ordIso_symmetric 597 598lemma ordIso_imp_ordLeq: 599"r =o r' \<Longrightarrow> r \<le>o r'" 600using ordIso_iff_ordLeq by blast 601 602lemma ordLess_imp_ordLeq: 603"r <o r' \<Longrightarrow> r \<le>o r'" 604using ordLeq_iff_ordLess_or_ordIso by blast 605 606lemma ofilter_subset_ordLeq: 607assumes WELL: "Well_order r" and 608 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" 609shows "(A \<le> B) = (Restr r A \<le>o Restr r B)" 610proof 611 assume "A \<le> B" 612 thus "Restr r A \<le>o Restr r B" 613 unfolding ordLeq_def using assms 614 Well_order_Restr Well_order_Restr ofilter_subset_embed by blast 615next 616 assume *: "Restr r A \<le>o Restr r B" 617 then obtain f where "embed (Restr r A) (Restr r B) f" 618 unfolding ordLeq_def by blast 619 {assume "B < A" 620 hence "Restr r B <o Restr r A" 621 unfolding ordLess_def using assms 622 Well_order_Restr Well_order_Restr ofilter_subset_embedS by blast 623 hence False using * not_ordLess_ordLeq by blast 624 } 625 thus "A \<le> B" using OFA OFB WELL 626 wo_rel_def[of r] wo_rel.ofilter_linord[of r A B] by blast 627qed 628 629lemma ofilter_subset_ordLess: 630assumes WELL: "Well_order r" and 631 OFA: "wo_rel.ofilter r A" and OFB: "wo_rel.ofilter r B" 632shows "(A < B) = (Restr r A <o Restr r B)" 633proof- 634 let ?rA = "Restr r A" let ?rB = "Restr r B" 635 have 1: "Well_order ?rA \<and> Well_order ?rB" 636 using WELL Well_order_Restr by blast 637 have "(A < B) = (\<not> B \<le> A)" using assms 638 wo_rel_def wo_rel.ofilter_linord[of r A B] by blast 639 also have "\<dots> = (\<not> Restr r B \<le>o Restr r A)" 640 using assms ofilter_subset_ordLeq by blast 641 also have "\<dots> = (Restr r A <o Restr r B)" 642 using 1 not_ordLeq_iff_ordLess by blast 643 finally show ?thesis . 644qed 645 646lemma ofilter_ordLess: 647"\<lbrakk>Well_order r; wo_rel.ofilter r A\<rbrakk> \<Longrightarrow> (A < Field r) = (Restr r A <o r)" 648by (simp add: ofilter_subset_ordLess wo_rel.Field_ofilter 649 wo_rel_def Restr_Field) 650 651corollary underS_Restr_ordLess: 652assumes "Well_order r" and "Field r \<noteq> {}" 653shows "Restr r (underS r a) <o r" 654proof- 655 have "underS r a < Field r" using assms 656 by (simp add: underS_Field3) 657 thus ?thesis using assms 658 by (simp add: ofilter_ordLess wo_rel.underS_ofilter wo_rel_def) 659qed 660 661lemma embed_ordLess_ofilterIncl: 662assumes 663 OL12: "r1 <o r2" and OL23: "r2 <o r3" and 664 EMB13: "embed r1 r3 f13" and EMB23: "embed r2 r3 f23" 665shows "(f13`(Field r1), f23`(Field r2)) \<in> (ofilterIncl r3)" 666proof- 667 have OL13: "r1 <o r3" 668 using OL12 OL23 using ordLess_transitive by auto 669 let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A3 ="Field r3" 670 obtain f12 g23 where 671 0: "Well_order r1 \<and> Well_order r2 \<and> Well_order r3" and 672 1: "embed r1 r2 f12 \<and> \<not>(bij_betw f12 ?A1 ?A2)" and 673 2: "embed r2 r3 g23 \<and> \<not>(bij_betw g23 ?A2 ?A3)" 674 using OL12 OL23 by (auto simp add: ordLess_def embedS_def) 675 hence "\<forall>a \<in> ?A2. f23 a = g23 a" 676 using EMB23 embed_unique[of r2 r3] by blast 677 hence 3: "\<not>(bij_betw f23 ?A2 ?A3)" 678 using 2 bij_betw_cong[of ?A2 f23 g23] by blast 679 (* *) 680 have 4: "wo_rel.ofilter r2 (f12 ` ?A1) \<and> f12 ` ?A1 \<noteq> ?A2" 681 using 0 1 OL12 by (simp add: embed_Field_ofilter ordLess_Field) 682 have 5: "wo_rel.ofilter r3 (f23 ` ?A2) \<and> f23 ` ?A2 \<noteq> ?A3" 683 using 0 EMB23 OL23 by (simp add: embed_Field_ofilter ordLess_Field) 684 have 6: "wo_rel.ofilter r3 (f13 ` ?A1) \<and> f13 ` ?A1 \<noteq> ?A3" 685 using 0 EMB13 OL13 by (simp add: embed_Field_ofilter ordLess_Field) 686 (* *) 687 have "f12 ` ?A1 < ?A2" 688 using 0 4 by (auto simp add: wo_rel_def wo_rel.ofilter_def) 689 moreover have "inj_on f23 ?A2" 690 using EMB23 0 by (simp add: wo_rel_def embed_inj_on) 691 ultimately 692 have "f23 ` (f12 ` ?A1) < f23 ` ?A2" by (simp add: inj_on_strict_subset) 693 moreover 694 {have "embed r1 r3 (f23 \<circ> f12)" 695 using 1 EMB23 0 by (auto simp add: comp_embed) 696 hence "\<forall>a \<in> ?A1. f23(f12 a) = f13 a" 697 using EMB13 0 embed_unique[of r1 r3 "f23 \<circ> f12" f13] by auto 698 hence "f23 ` (f12 ` ?A1) = f13 ` ?A1" by force 699 } 700 ultimately 701 have "f13 ` ?A1 < f23 ` ?A2" by simp 702 (* *) 703 with 5 6 show ?thesis 704 unfolding ofilterIncl_def by auto 705qed 706 707lemma ordLess_iff_ordIso_Restr: 708assumes WELL: "Well_order r" and WELL': "Well_order r'" 709shows "(r' <o r) = (\<exists>a \<in> Field r. r' =o Restr r (underS r a))" 710proof(auto) 711 fix a assume *: "a \<in> Field r" and **: "r' =o Restr r (underS r a)" 712 hence "Restr r (underS r a) <o r" using WELL underS_Restr_ordLess[of r] by blast 713 thus "r' <o r" using ** ordIso_ordLess_trans by blast 714next 715 assume "r' <o r" 716 then obtain f where 1: "Well_order r \<and> Well_order r'" and 717 2: "embed r' r f \<and> f ` (Field r') \<noteq> Field r" 718 unfolding ordLess_def embedS_def[abs_def] bij_betw_def using embed_inj_on by blast 719 hence "wo_rel.ofilter r (f ` (Field r'))" using embed_Field_ofilter by blast 720 then obtain a where 3: "a \<in> Field r" and 4: "underS r a = f ` (Field r')" 721 using 1 2 by (auto simp add: wo_rel.ofilter_underS_Field wo_rel_def) 722 have "iso r' (Restr r (f ` (Field r'))) f" 723 using embed_implies_iso_Restr 2 assms by blast 724 moreover have "Well_order (Restr r (f ` (Field r')))" 725 using WELL Well_order_Restr by blast 726 ultimately have "r' =o Restr r (f ` (Field r'))" 727 using WELL' unfolding ordIso_def by auto 728 hence "r' =o Restr r (underS r a)" using 4 by auto 729 thus "\<exists>a \<in> Field r. r' =o Restr r (underS r a)" using 3 by auto 730qed 731 732lemma internalize_ordLess: 733"(r' <o r) = (\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r)" 734proof 735 assume *: "r' <o r" 736 hence 0: "Well_order r \<and> Well_order r'" unfolding ordLess_def by auto 737 with * obtain a where 1: "a \<in> Field r" and 2: "r' =o Restr r (underS r a)" 738 using ordLess_iff_ordIso_Restr by blast 739 let ?p = "Restr r (underS r a)" 740 have "wo_rel.ofilter r (underS r a)" using 0 741 by (simp add: wo_rel_def wo_rel.underS_ofilter) 742 hence "Field ?p = underS r a" using 0 Field_Restr_ofilter by blast 743 hence "Field ?p < Field r" using underS_Field2 1 by fast 744 moreover have "?p <o r" using underS_Restr_ordLess[of r a] 0 1 by blast 745 ultimately 746 show "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" using 2 by blast 747next 748 assume "\<exists>p. Field p < Field r \<and> r' =o p \<and> p <o r" 749 thus "r' <o r" using ordIso_ordLess_trans by blast 750qed 751 752lemma internalize_ordLeq: 753"(r' \<le>o r) = (\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r)" 754proof 755 assume *: "r' \<le>o r" 756 moreover 757 {assume "r' <o r" 758 then obtain p where "Field p < Field r \<and> r' =o p \<and> p <o r" 759 using internalize_ordLess[of r' r] by blast 760 hence "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" 761 using ordLeq_iff_ordLess_or_ordIso by blast 762 } 763 moreover 764 have "r \<le>o r" using * ordLeq_def ordLeq_reflexive by blast 765 ultimately show "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" 766 using ordLeq_iff_ordLess_or_ordIso by blast 767next 768 assume "\<exists>p. Field p \<le> Field r \<and> r' =o p \<and> p \<le>o r" 769 thus "r' \<le>o r" using ordIso_ordLeq_trans by blast 770qed 771 772lemma ordLeq_iff_ordLess_Restr: 773assumes WELL: "Well_order r" and WELL': "Well_order r'" 774shows "(r \<le>o r') = (\<forall>a \<in> Field r. Restr r (underS r a) <o r')" 775proof(auto) 776 assume *: "r \<le>o r'" 777 fix a assume "a \<in> Field r" 778 hence "Restr r (underS r a) <o r" 779 using WELL underS_Restr_ordLess[of r] by blast 780 thus "Restr r (underS r a) <o r'" 781 using * ordLess_ordLeq_trans by blast 782next 783 assume *: "\<forall>a \<in> Field r. Restr r (underS r a) <o r'" 784 {assume "r' <o r" 785 then obtain a where "a \<in> Field r \<and> r' =o Restr r (underS r a)" 786 using assms ordLess_iff_ordIso_Restr by blast 787 hence False using * not_ordLess_ordIso ordIso_symmetric by blast 788 } 789 thus "r \<le>o r'" using ordLess_or_ordLeq assms by blast 790qed 791 792lemma finite_ordLess_infinite: 793assumes WELL: "Well_order r" and WELL': "Well_order r'" and 794 FIN: "finite(Field r)" and INF: "\<not>finite(Field r')" 795shows "r <o r'" 796proof- 797 {assume "r' \<le>o r" 798 then obtain h where "inj_on h (Field r') \<and> h ` (Field r') \<le> Field r" 799 unfolding ordLeq_def using assms embed_inj_on embed_Field by blast 800 hence False using finite_imageD finite_subset FIN INF by blast 801 } 802 thus ?thesis using WELL WELL' ordLess_or_ordLeq by blast 803qed 804 805lemma finite_well_order_on_ordIso: 806assumes FIN: "finite A" and 807 WELL: "well_order_on A r" and WELL': "well_order_on A r'" 808shows "r =o r'" 809proof- 810 have 0: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A" 811 using assms well_order_on_Well_order by blast 812 moreover 813 have "\<forall>r r'. well_order_on A r \<and> well_order_on A r' \<and> r \<le>o r' 814 \<longrightarrow> r =o r'" 815 proof(clarify) 816 fix r r' assume *: "well_order_on A r" and **: "well_order_on A r'" 817 have 2: "Well_order r \<and> Well_order r' \<and> Field r = A \<and> Field r' = A" 818 using * ** well_order_on_Well_order by blast 819 assume "r \<le>o r'" 820 then obtain f where 1: "embed r r' f" and 821 "inj_on f A \<and> f ` A \<le> A" 822 unfolding ordLeq_def using 2 embed_inj_on embed_Field by blast 823 hence "bij_betw f A A" unfolding bij_betw_def using FIN endo_inj_surj by blast 824 thus "r =o r'" unfolding ordIso_def iso_def[abs_def] using 1 2 by auto 825 qed 826 ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast 827qed 828 829subsection\<open>\<open><o\<close> is well-founded\<close> 830 831text \<open>Of course, it only makes sense to state that the \<open><o\<close> is well-founded 832on the restricted type \<open>'a rel rel\<close>. We prove this by first showing that, for any set 833of well-orders all embedded in a fixed well-order, the function mapping each well-order 834in the set to an order filter of the fixed well-order is compatible w.r.t. to \<open><o\<close> versus 835{\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close> 836 837definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set" 838where "ord_to_filter r0 r \<equiv> (SOME f. embed r r0 f) ` (Field r)" 839 840lemma ord_to_filter_compat: 841"compat (ordLess Int (ordLess\<inverse>``{r0} \<times> ordLess\<inverse>``{r0})) 842 (ofilterIncl r0) 843 (ord_to_filter r0)" 844proof(unfold compat_def ord_to_filter_def, clarify) 845 fix r1::"'a rel" and r2::"'a rel" 846 let ?A1 = "Field r1" let ?A2 ="Field r2" let ?A0 ="Field r0" 847 let ?phi10 = "\<lambda> f10. embed r1 r0 f10" let ?f10 = "SOME f. ?phi10 f" 848 let ?phi20 = "\<lambda> f20. embed r2 r0 f20" let ?f20 = "SOME f. ?phi20 f" 849 assume *: "r1 <o r0" "r2 <o r0" and **: "r1 <o r2" 850 hence "(\<exists>f. ?phi10 f) \<and> (\<exists>f. ?phi20 f)" 851 by (auto simp add: ordLess_def embedS_def) 852 hence "?phi10 ?f10 \<and> ?phi20 ?f20" by (auto simp add: someI_ex) 853 thus "(?f10 ` ?A1, ?f20 ` ?A2) \<in> ofilterIncl r0" 854 using * ** by (simp add: embed_ordLess_ofilterIncl) 855qed 856 857theorem wf_ordLess: "wf ordLess" 858proof- 859 {fix r0 :: "('a \<times> 'a) set" 860 (* need to annotate here!*) 861 let ?ordLess = "ordLess::('d rel * 'd rel) set" 862 let ?R = "?ordLess Int (?ordLess\<inverse>``{r0} \<times> ?ordLess\<inverse>``{r0})" 863 {assume Case1: "Well_order r0" 864 hence "wf ?R" 865 using wf_ofilterIncl[of r0] 866 compat_wf[of ?R "ofilterIncl r0" "ord_to_filter r0"] 867 ord_to_filter_compat[of r0] by auto 868 } 869 moreover 870 {assume Case2: "\<not> Well_order r0" 871 hence "?R = {}" unfolding ordLess_def by auto 872 hence "wf ?R" using wf_empty by simp 873 } 874 ultimately have "wf ?R" by blast 875 } 876 thus ?thesis by (simp add: trans_wf_iff ordLess_trans) 877qed 878 879corollary exists_minim_Well_order: 880assumes NE: "R \<noteq> {}" and WELL: "\<forall>r \<in> R. Well_order r" 881shows "\<exists>r \<in> R. \<forall>r' \<in> R. r \<le>o r'" 882proof- 883 obtain r where "r \<in> R \<and> (\<forall>r' \<in> R. \<not> r' <o r)" 884 using NE spec[OF spec[OF subst[OF wf_eq_minimal, of "%x. x", OF wf_ordLess]], of _ R] 885 equals0I[of R] by blast 886 with not_ordLeq_iff_ordLess WELL show ?thesis by blast 887qed 888 889 890subsection \<open>Copy via direct images\<close> 891 892text\<open>The direct image operator is the dual of the inverse image operator \<open>inv_image\<close> 893from \<open>Relation.thy\<close>. It is useful for transporting a well-order between 894different types.\<close> 895 896definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel" 897where 898"dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}" 899 900lemma dir_image_Field: 901"Field(dir_image r f) = f ` (Field r)" 902unfolding dir_image_def Field_def Range_def Domain_def by fast 903 904lemma dir_image_minus_Id: 905"inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f" 906unfolding inj_on_def Field_def dir_image_def by auto 907 908lemma Refl_dir_image: 909assumes "Refl r" 910shows "Refl(dir_image r f)" 911proof- 912 {fix a' b' 913 assume "(a',b') \<in> dir_image r f" 914 then obtain a b where 1: "a' = f a \<and> b' = f b \<and> (a,b) \<in> r" 915 unfolding dir_image_def by blast 916 hence "a \<in> Field r \<and> b \<in> Field r" using Field_def by fastforce 917 hence "(a,a) \<in> r \<and> (b,b) \<in> r" using assms by (simp add: refl_on_def) 918 with 1 have "(a',a') \<in> dir_image r f \<and> (b',b') \<in> dir_image r f" 919 unfolding dir_image_def by auto 920 } 921 thus ?thesis 922 by(unfold refl_on_def Field_def Domain_def Range_def, auto) 923qed 924 925lemma trans_dir_image: 926assumes TRANS: "trans r" and INJ: "inj_on f (Field r)" 927shows "trans(dir_image r f)" 928proof(unfold trans_def, auto) 929 fix a' b' c' 930 assume "(a',b') \<in> dir_image r f" "(b',c') \<in> dir_image r f" 931 then obtain a b1 b2 c where 1: "a' = f a \<and> b' = f b1 \<and> b' = f b2 \<and> c' = f c" and 932 2: "(a,b1) \<in> r \<and> (b2,c) \<in> r" 933 unfolding dir_image_def by blast 934 hence "b1 \<in> Field r \<and> b2 \<in> Field r" 935 unfolding Field_def by auto 936 hence "b1 = b2" using 1 INJ unfolding inj_on_def by auto 937 hence "(a,c) \<in> r" using 2 TRANS unfolding trans_def by blast 938 thus "(a',c') \<in> dir_image r f" 939 unfolding dir_image_def using 1 by auto 940qed 941 942lemma Preorder_dir_image: 943"\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)" 944by (simp add: preorder_on_def Refl_dir_image trans_dir_image) 945 946lemma antisym_dir_image: 947assumes AN: "antisym r" and INJ: "inj_on f (Field r)" 948shows "antisym(dir_image r f)" 949proof(unfold antisym_def, auto) 950 fix a' b' 951 assume "(a',b') \<in> dir_image r f" "(b',a') \<in> dir_image r f" 952 then obtain a1 b1 a2 b2 where 1: "a' = f a1 \<and> a' = f a2 \<and> b' = f b1 \<and> b' = f b2" and 953 2: "(a1,b1) \<in> r \<and> (b2,a2) \<in> r " and 954 3: "{a1,a2,b1,b2} \<le> Field r" 955 unfolding dir_image_def Field_def by blast 956 hence "a1 = a2 \<and> b1 = b2" using INJ unfolding inj_on_def by auto 957 hence "a1 = b2" using 2 AN unfolding antisym_def by auto 958 thus "a' = b'" using 1 by auto 959qed 960 961lemma Partial_order_dir_image: 962"\<lbrakk>Partial_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Partial_order (dir_image r f)" 963by (simp add: partial_order_on_def Preorder_dir_image antisym_dir_image) 964 965lemma Total_dir_image: 966assumes TOT: "Total r" and INJ: "inj_on f (Field r)" 967shows "Total(dir_image r f)" 968proof(unfold total_on_def, intro ballI impI) 969 fix a' b' 970 assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)" 971 then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'" 972 unfolding dir_image_Field[of r f] by blast 973 moreover assume "a' \<noteq> b'" 974 ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto 975 hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto 976 thus "(a',b') \<in> dir_image r f \<or> (b',a') \<in> dir_image r f" 977 using 1 unfolding dir_image_def by auto 978qed 979 980lemma Linear_order_dir_image: 981"\<lbrakk>Linear_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Linear_order (dir_image r f)" 982by (simp add: linear_order_on_def Partial_order_dir_image Total_dir_image) 983 984lemma wf_dir_image: 985assumes WF: "wf r" and INJ: "inj_on f (Field r)" 986shows "wf(dir_image r f)" 987proof(unfold wf_eq_minimal2, intro allI impI, elim conjE) 988 fix A'::"'b set" 989 assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}" 990 obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast 991 have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field) 992 then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)" 993 using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast 994 have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f" 995 proof(clarify) 996 fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f" 997 obtain b1 a1 where 2: "b' = f b1 \<and> f a = f a1" and 998 3: "(b1,a1) \<in> r \<and> {a1,b1} \<le> Field r" 999 using ** unfolding dir_image_def Field_def by blast 1000 hence "a = a1" using 1 A_def INJ unfolding inj_on_def by auto 1001 hence "b1 \<in> A \<and> (b1,a) \<in> r" using 2 3 A_def * by auto 1002 with 1 show False by auto 1003 qed 1004 thus "\<exists>a'\<in>A'. \<forall>b'\<in>A'. (b', a') \<notin> dir_image r f" 1005 using A_def 1 by blast 1006qed 1007 1008lemma Well_order_dir_image: 1009"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Well_order (dir_image r f)" 1010unfolding well_order_on_def 1011using Linear_order_dir_image[of r f] wf_dir_image[of "r - Id" f] 1012 dir_image_minus_Id[of f r] 1013 subset_inj_on[of f "Field r" "Field(r - Id)"] 1014 mono_Field[of "r - Id" r] by auto 1015 1016lemma dir_image_bij_betw: 1017"\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))" 1018unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs) 1019 1020lemma dir_image_compat: 1021"compat r (dir_image r f) f" 1022unfolding compat_def dir_image_def by auto 1023 1024lemma dir_image_iso: 1025"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> iso r (dir_image r f) f" 1026using iso_iff3 dir_image_compat dir_image_bij_betw Well_order_dir_image by blast 1027 1028lemma dir_image_ordIso: 1029"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> r =o dir_image r f" 1030unfolding ordIso_def using dir_image_iso Well_order_dir_image by blast 1031 1032lemma Well_order_iso_copy: 1033assumes WELL: "well_order_on A r" and BIJ: "bij_betw f A A'" 1034shows "\<exists>r'. well_order_on A' r' \<and> r =o r'" 1035proof- 1036 let ?r' = "dir_image r f" 1037 have 1: "A = Field r \<and> Well_order r" 1038 using WELL well_order_on_Well_order by blast 1039 hence 2: "iso r ?r' f" 1040 using dir_image_iso using BIJ unfolding bij_betw_def by auto 1041 hence "f ` (Field r) = Field ?r'" using 1 iso_iff[of r ?r'] by blast 1042 hence "Field ?r' = A'" 1043 using 1 BIJ unfolding bij_betw_def by auto 1044 moreover have "Well_order ?r'" 1045 using 1 Well_order_dir_image BIJ unfolding bij_betw_def by blast 1046 ultimately show ?thesis unfolding ordIso_def using 1 2 by blast 1047qed 1048 1049 1050subsection \<open>Bounded square\<close> 1051 1052text\<open>This construction essentially defines, for an order relation \<open>r\<close>, a lexicographic 1053order \<open>bsqr r\<close> on \<open>(Field r) \<times> (Field r)\<close>, applying the 1054following criteria (in this order): 1055\begin{itemize} 1056\item compare the maximums; 1057\item compare the first components; 1058\item compare the second components. 1059\end{itemize} 1060% 1061The only application of this construction that we are aware of is 1062at proving that the square of an infinite set has the same cardinal 1063as that set. The essential property required there (and which is ensured by this 1064construction) is that any proper order filter of the product order is included in a rectangle, i.e., 1065in a product of proper filters on the original relation (assumed to be a well-order).\<close> 1066 1067definition bsqr :: "'a rel => ('a * 'a)rel" 1068where 1069"bsqr r = {((a1,a2),(b1,b2)). 1070 {a1,a2,b1,b2} \<le> Field r \<and> 1071 (a1 = b1 \<and> a2 = b2 \<or> 1072 (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> 1073 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> 1074 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id 1075 )}" 1076 1077lemma Field_bsqr: 1078"Field (bsqr r) = Field r \<times> Field r" 1079proof 1080 show "Field (bsqr r) \<le> Field r \<times> Field r" 1081 proof- 1082 {fix a1 a2 assume "(a1,a2) \<in> Field (bsqr r)" 1083 moreover 1084 have "\<And> b1 b2. ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r \<Longrightarrow> 1085 a1 \<in> Field r \<and> a2 \<in> Field r" unfolding bsqr_def by auto 1086 ultimately have "a1 \<in> Field r \<and> a2 \<in> Field r" unfolding Field_def by auto 1087 } 1088 thus ?thesis unfolding Field_def by force 1089 qed 1090next 1091 show "Field r \<times> Field r \<le> Field (bsqr r)" 1092 proof(auto) 1093 fix a1 a2 assume "a1 \<in> Field r" and "a2 \<in> Field r" 1094 hence "((a1,a2),(a1,a2)) \<in> bsqr r" unfolding bsqr_def by blast 1095 thus "(a1,a2) \<in> Field (bsqr r)" unfolding Field_def by auto 1096 qed 1097qed 1098 1099lemma bsqr_Refl: "Refl(bsqr r)" 1100by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def) 1101 1102lemma bsqr_Trans: 1103assumes "Well_order r" 1104shows "trans (bsqr r)" 1105proof(unfold trans_def, auto) 1106 (* Preliminary facts *) 1107 have Well: "wo_rel r" using assms wo_rel_def by auto 1108 hence Trans: "trans r" using wo_rel.TRANS by auto 1109 have Anti: "antisym r" using wo_rel.ANTISYM Well by auto 1110 hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) 1111 (* Main proof *) 1112 fix a1 a2 b1 b2 c1 c2 1113 assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(c1,c2)) \<in> bsqr r" 1114 hence 0: "{a1,a2,b1,b2,c1,c2} \<le> Field r" unfolding bsqr_def by auto 1115 have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> 1116 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> 1117 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" 1118 using * unfolding bsqr_def by auto 1119 have 2: "b1 = c1 \<and> b2 = c2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id \<or> 1120 wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id \<or> 1121 wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id" 1122 using ** unfolding bsqr_def by auto 1123 show "((a1,a2),(c1,c2)) \<in> bsqr r" 1124 proof- 1125 {assume Case1: "a1 = b1 \<and> a2 = b2" 1126 hence ?thesis using ** by simp 1127 } 1128 moreover 1129 {assume Case2: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id" 1130 {assume Case21: "b1 = c1 \<and> b2 = c2" 1131 hence ?thesis using * by simp 1132 } 1133 moreover 1134 {assume Case22: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" 1135 hence "(wo_rel.max2 r a1 a2, wo_rel.max2 r c1 c2) \<in> r - Id" 1136 using Case2 TransS trans_def[of "r - Id"] by blast 1137 hence ?thesis using 0 unfolding bsqr_def by auto 1138 } 1139 moreover 1140 {assume Case23_4: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2" 1141 hence ?thesis using Case2 0 unfolding bsqr_def by auto 1142 } 1143 ultimately have ?thesis using 0 2 by auto 1144 } 1145 moreover 1146 {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id" 1147 {assume Case31: "b1 = c1 \<and> b2 = c2" 1148 hence ?thesis using * by simp 1149 } 1150 moreover 1151 {assume Case32: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" 1152 hence ?thesis using Case3 0 unfolding bsqr_def by auto 1153 } 1154 moreover 1155 {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id" 1156 hence "(a1,c1) \<in> r - Id" 1157 using Case3 TransS trans_def[of "r - Id"] by blast 1158 hence ?thesis using Case3 Case33 0 unfolding bsqr_def by auto 1159 } 1160 moreover 1161 {assume Case33: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1" 1162 hence ?thesis using Case3 0 unfolding bsqr_def by auto 1163 } 1164 ultimately have ?thesis using 0 2 by auto 1165 } 1166 moreover 1167 {assume Case4: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" 1168 {assume Case41: "b1 = c1 \<and> b2 = c2" 1169 hence ?thesis using * by simp 1170 } 1171 moreover 1172 {assume Case42: "(wo_rel.max2 r b1 b2, wo_rel.max2 r c1 c2) \<in> r - Id" 1173 hence ?thesis using Case4 0 unfolding bsqr_def by force 1174 } 1175 moreover 1176 {assume Case43: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> (b1,c1) \<in> r - Id" 1177 hence ?thesis using Case4 0 unfolding bsqr_def by auto 1178 } 1179 moreover 1180 {assume Case44: "wo_rel.max2 r b1 b2 = wo_rel.max2 r c1 c2 \<and> b1 = c1 \<and> (b2,c2) \<in> r - Id" 1181 hence "(a2,c2) \<in> r - Id" 1182 using Case4 TransS trans_def[of "r - Id"] by blast 1183 hence ?thesis using Case4 Case44 0 unfolding bsqr_def by auto 1184 } 1185 ultimately have ?thesis using 0 2 by auto 1186 } 1187 ultimately show ?thesis using 0 1 by auto 1188 qed 1189qed 1190 1191lemma bsqr_antisym: 1192assumes "Well_order r" 1193shows "antisym (bsqr r)" 1194proof(unfold antisym_def, clarify) 1195 (* Preliminary facts *) 1196 have Well: "wo_rel r" using assms wo_rel_def by auto 1197 hence Trans: "trans r" using wo_rel.TRANS by auto 1198 have Anti: "antisym r" using wo_rel.ANTISYM Well by auto 1199 hence TransS: "trans(r - Id)" using Trans by (simp add: trans_diff_Id) 1200 hence IrrS: "\<forall>a b. \<not>((a,b) \<in> r - Id \<and> (b,a) \<in> r - Id)" 1201 using Anti trans_def[of "r - Id"] antisym_def[of "r - Id"] by blast 1202 (* Main proof *) 1203 fix a1 a2 b1 b2 1204 assume *: "((a1,a2),(b1,b2)) \<in> bsqr r" and **: "((b1,b2),(a1,a2)) \<in> bsqr r" 1205 hence 0: "{a1,a2,b1,b2} \<le> Field r" unfolding bsqr_def by auto 1206 have 1: "a1 = b1 \<and> a2 = b2 \<or> (wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id \<or> 1207 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id \<or> 1208 wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" 1209 using * unfolding bsqr_def by auto 1210 have 2: "b1 = a1 \<and> b2 = a2 \<or> (wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id \<or> 1211 wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> (b1,a1) \<in> r - Id \<or> 1212 wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2 \<and> b1 = a1 \<and> (b2,a2) \<in> r - Id" 1213 using ** unfolding bsqr_def by auto 1214 show "a1 = b1 \<and> a2 = b2" 1215 proof- 1216 {assume Case1: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r - Id" 1217 {assume Case11: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" 1218 hence False using Case1 IrrS by blast 1219 } 1220 moreover 1221 {assume Case12_3: "wo_rel.max2 r b1 b2 = wo_rel.max2 r a1 a2" 1222 hence False using Case1 by auto 1223 } 1224 ultimately have ?thesis using 0 2 by auto 1225 } 1226 moreover 1227 {assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> (a1,b1) \<in> r - Id" 1228 {assume Case21: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" 1229 hence False using Case2 by auto 1230 } 1231 moreover 1232 {assume Case22: "(b1,a1) \<in> r - Id" 1233 hence False using Case2 IrrS by blast 1234 } 1235 moreover 1236 {assume Case23: "b1 = a1" 1237 hence False using Case2 by auto 1238 } 1239 ultimately have ?thesis using 0 2 by auto 1240 } 1241 moreover 1242 {assume Case3: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2 \<and> a1 = b1 \<and> (a2,b2) \<in> r - Id" 1243 moreover 1244 {assume Case31: "(wo_rel.max2 r b1 b2, wo_rel.max2 r a1 a2) \<in> r - Id" 1245 hence False using Case3 by auto 1246 } 1247 moreover 1248 {assume Case32: "(b1,a1) \<in> r - Id" 1249 hence False using Case3 by auto 1250 } 1251 moreover 1252 {assume Case33: "(b2,a2) \<in> r - Id" 1253 hence False using Case3 IrrS by blast 1254 } 1255 ultimately have ?thesis using 0 2 by auto 1256 } 1257 ultimately show ?thesis using 0 1 by blast 1258 qed 1259qed 1260 1261lemma bsqr_Total: 1262assumes "Well_order r" 1263shows "Total(bsqr r)" 1264proof- 1265 (* Preliminary facts *) 1266 have Well: "wo_rel r" using assms wo_rel_def by auto 1267 hence Total: "\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a,b) \<in> r \<or> (b,a) \<in> r" 1268 using wo_rel.TOTALS by auto 1269 (* Main proof *) 1270 {fix a1 a2 b1 b2 assume "{(a1,a2), (b1,b2)} \<le> Field(bsqr r)" 1271 hence 0: "a1 \<in> Field r \<and> a2 \<in> Field r \<and> b1 \<in> Field r \<and> b2 \<in> Field r" 1272 using Field_bsqr by blast 1273 have "((a1,a2) = (b1,b2) \<or> ((a1,a2),(b1,b2)) \<in> bsqr r \<or> ((b1,b2),(a1,a2)) \<in> bsqr r)" 1274 proof(rule wo_rel.cases_Total[of r a1 a2], clarsimp simp add: Well, simp add: 0) 1275 (* Why didn't clarsimp simp add: Well 0 do the same job? *) 1276 assume Case1: "(a1,a2) \<in> r" 1277 hence 1: "wo_rel.max2 r a1 a2 = a2" 1278 using Well 0 by (simp add: wo_rel.max2_equals2) 1279 show ?thesis 1280 proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) 1281 assume Case11: "(b1,b2) \<in> r" 1282 hence 2: "wo_rel.max2 r b1 b2 = b2" 1283 using Well 0 by (simp add: wo_rel.max2_equals2) 1284 show ?thesis 1285 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) 1286 assume Case111: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" 1287 thus ?thesis using 0 1 2 unfolding bsqr_def by auto 1288 next 1289 assume Case112: "a2 = b2" 1290 show ?thesis 1291 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) 1292 assume Case1121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" 1293 thus ?thesis using 0 1 2 Case112 unfolding bsqr_def by auto 1294 next 1295 assume Case1122: "a1 = b1" 1296 thus ?thesis using Case112 by auto 1297 qed 1298 qed 1299 next 1300 assume Case12: "(b2,b1) \<in> r" 1301 hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) 1302 show ?thesis 1303 proof(rule wo_rel.cases_Total3[of r a2 b1], clarsimp simp add: Well, simp add: 0) 1304 assume Case121: "(a2,b1) \<in> r - Id \<or> (b1,a2) \<in> r - Id" 1305 thus ?thesis using 0 1 3 unfolding bsqr_def by auto 1306 next 1307 assume Case122: "a2 = b1" 1308 show ?thesis 1309 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) 1310 assume Case1221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" 1311 thus ?thesis using 0 1 3 Case122 unfolding bsqr_def by auto 1312 next 1313 assume Case1222: "a1 = b1" 1314 show ?thesis 1315 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) 1316 assume Case12221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" 1317 thus ?thesis using 0 1 3 Case122 Case1222 unfolding bsqr_def by auto 1318 next 1319 assume Case12222: "a2 = b2" 1320 thus ?thesis using Case122 Case1222 by auto 1321 qed 1322 qed 1323 qed 1324 qed 1325 next 1326 assume Case2: "(a2,a1) \<in> r" 1327 hence 1: "wo_rel.max2 r a1 a2 = a1" using Well 0 by (simp add: wo_rel.max2_equals1) 1328 show ?thesis 1329 proof(rule wo_rel.cases_Total[of r b1 b2], clarsimp simp add: Well, simp add: 0) 1330 assume Case21: "(b1,b2) \<in> r" 1331 hence 2: "wo_rel.max2 r b1 b2 = b2" using Well 0 by (simp add: wo_rel.max2_equals2) 1332 show ?thesis 1333 proof(rule wo_rel.cases_Total3[of r a1 b2], clarsimp simp add: Well, simp add: 0) 1334 assume Case211: "(a1,b2) \<in> r - Id \<or> (b2,a1) \<in> r - Id" 1335 thus ?thesis using 0 1 2 unfolding bsqr_def by auto 1336 next 1337 assume Case212: "a1 = b2" 1338 show ?thesis 1339 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) 1340 assume Case2121: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" 1341 thus ?thesis using 0 1 2 Case212 unfolding bsqr_def by auto 1342 next 1343 assume Case2122: "a1 = b1" 1344 show ?thesis 1345 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) 1346 assume Case21221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" 1347 thus ?thesis using 0 1 2 Case212 Case2122 unfolding bsqr_def by auto 1348 next 1349 assume Case21222: "a2 = b2" 1350 thus ?thesis using Case2122 Case212 by auto 1351 qed 1352 qed 1353 qed 1354 next 1355 assume Case22: "(b2,b1) \<in> r" 1356 hence 3: "wo_rel.max2 r b1 b2 = b1" using Well 0 by (simp add: wo_rel.max2_equals1) 1357 show ?thesis 1358 proof(rule wo_rel.cases_Total3[of r a1 b1], clarsimp simp add: Well, simp add: 0) 1359 assume Case221: "(a1,b1) \<in> r - Id \<or> (b1,a1) \<in> r - Id" 1360 thus ?thesis using 0 1 3 unfolding bsqr_def by auto 1361 next 1362 assume Case222: "a1 = b1" 1363 show ?thesis 1364 proof(rule wo_rel.cases_Total3[of r a2 b2], clarsimp simp add: Well, simp add: 0) 1365 assume Case2221: "(a2,b2) \<in> r - Id \<or> (b2,a2) \<in> r - Id" 1366 thus ?thesis using 0 1 3 Case222 unfolding bsqr_def by auto 1367 next 1368 assume Case2222: "a2 = b2" 1369 thus ?thesis using Case222 by auto 1370 qed 1371 qed 1372 qed 1373 qed 1374 } 1375 thus ?thesis unfolding total_on_def by fast 1376qed 1377 1378lemma bsqr_Linear_order: 1379assumes "Well_order r" 1380shows "Linear_order(bsqr r)" 1381unfolding order_on_defs 1382using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast 1383 1384lemma bsqr_Well_order: 1385assumes "Well_order r" 1386shows "Well_order(bsqr r)" 1387using assms 1388proof(simp add: bsqr_Linear_order Linear_order_Well_order_iff, intro allI impI) 1389 have 0: "\<forall>A \<le> Field r. A \<noteq> {} \<longrightarrow> (\<exists>a \<in> A. \<forall>a' \<in> A. (a,a') \<in> r)" 1390 using assms well_order_on_def Linear_order_Well_order_iff by blast 1391 fix D assume *: "D \<le> Field (bsqr r)" and **: "D \<noteq> {}" 1392 hence 1: "D \<le> Field r \<times> Field r" unfolding Field_bsqr by simp 1393 (* *) 1394 obtain M where M_def: "M = {wo_rel.max2 r a1 a2| a1 a2. (a1,a2) \<in> D}" by blast 1395 have "M \<noteq> {}" using 1 M_def ** by auto 1396 moreover 1397 have "M \<le> Field r" unfolding M_def 1398 using 1 assms wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce 1399 ultimately obtain m where m_min: "m \<in> M \<and> (\<forall>a \<in> M. (m,a) \<in> r)" 1400 using 0 by blast 1401 (* *) 1402 obtain A1 where A1_def: "A1 = {a1. \<exists>a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast 1403 have "A1 \<le> Field r" unfolding A1_def using 1 by auto 1404 moreover have "A1 \<noteq> {}" unfolding A1_def using m_min unfolding M_def by blast 1405 ultimately obtain a1 where a1_min: "a1 \<in> A1 \<and> (\<forall>a \<in> A1. (a1,a) \<in> r)" 1406 using 0 by blast 1407 (* *) 1408 obtain A2 where A2_def: "A2 = {a2. (a1,a2) \<in> D \<and> wo_rel.max2 r a1 a2 = m}" by blast 1409 have "A2 \<le> Field r" unfolding A2_def using 1 by auto 1410 moreover have "A2 \<noteq> {}" unfolding A2_def 1411 using m_min a1_min unfolding A1_def M_def by blast 1412 ultimately obtain a2 where a2_min: "a2 \<in> A2 \<and> (\<forall>a \<in> A2. (a2,a) \<in> r)" 1413 using 0 by blast 1414 (* *) 1415 have 2: "wo_rel.max2 r a1 a2 = m" 1416 using a1_min a2_min unfolding A1_def A2_def by auto 1417 have 3: "(a1,a2) \<in> D" using a2_min unfolding A2_def by auto 1418 (* *) 1419 moreover 1420 {fix b1 b2 assume ***: "(b1,b2) \<in> D" 1421 hence 4: "{a1,a2,b1,b2} \<le> Field r" using 1 3 by blast 1422 have 5: "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r" 1423 using *** a1_min a2_min m_min unfolding A1_def A2_def M_def by auto 1424 have "((a1,a2),(b1,b2)) \<in> bsqr r" 1425 proof(cases "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2") 1426 assume Case1: "wo_rel.max2 r a1 a2 \<noteq> wo_rel.max2 r b1 b2" 1427 thus ?thesis unfolding bsqr_def using 4 5 by auto 1428 next 1429 assume Case2: "wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" 1430 hence "b1 \<in> A1" unfolding A1_def using 2 *** by auto 1431 hence 6: "(a1,b1) \<in> r" using a1_min by auto 1432 show ?thesis 1433 proof(cases "a1 = b1") 1434 assume Case21: "a1 \<noteq> b1" 1435 thus ?thesis unfolding bsqr_def using 4 Case2 6 by auto 1436 next 1437 assume Case22: "a1 = b1" 1438 hence "b2 \<in> A2" unfolding A2_def using 2 *** Case2 by auto 1439 hence 7: "(a2,b2) \<in> r" using a2_min by auto 1440 thus ?thesis unfolding bsqr_def using 4 7 Case2 Case22 by auto 1441 qed 1442 qed 1443 } 1444 (* *) 1445 ultimately show "\<exists>d \<in> D. \<forall>d' \<in> D. (d,d') \<in> bsqr r" by fastforce 1446qed 1447 1448lemma bsqr_max2: 1449assumes WELL: "Well_order r" and LEQ: "((a1,a2),(b1,b2)) \<in> bsqr r" 1450shows "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r" 1451proof- 1452 have "{(a1,a2),(b1,b2)} \<le> Field(bsqr r)" 1453 using LEQ unfolding Field_def by auto 1454 hence "{a1,a2,b1,b2} \<le> Field r" unfolding Field_bsqr by auto 1455 hence "{wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2} \<le> Field r" 1456 using WELL wo_rel_def[of r] wo_rel.max2_among[of r] by fastforce 1457 moreover have "(wo_rel.max2 r a1 a2, wo_rel.max2 r b1 b2) \<in> r \<or> wo_rel.max2 r a1 a2 = wo_rel.max2 r b1 b2" 1458 using LEQ unfolding bsqr_def by auto 1459 ultimately show ?thesis using WELL unfolding order_on_defs refl_on_def by auto 1460qed 1461 1462lemma bsqr_ofilter: 1463assumes WELL: "Well_order r" and 1464 OF: "wo_rel.ofilter (bsqr r) D" and SUB: "D < Field r \<times> Field r" and 1465 NE: "\<not> (\<exists>a. Field r = under r a)" 1466shows "\<exists>A. wo_rel.ofilter r A \<and> A < Field r \<and> D \<le> A \<times> A" 1467proof- 1468 let ?r' = "bsqr r" 1469 have Well: "wo_rel r" using WELL wo_rel_def by blast 1470 hence Trans: "trans r" using wo_rel.TRANS by blast 1471 have Well': "Well_order ?r' \<and> wo_rel ?r'" 1472 using WELL bsqr_Well_order wo_rel_def by blast 1473 (* *) 1474 have "D < Field ?r'" unfolding Field_bsqr using SUB . 1475 with OF obtain a1 and a2 where 1476 "(a1,a2) \<in> Field ?r'" and 1: "D = underS ?r' (a1,a2)" 1477 using Well' wo_rel.ofilter_underS_Field[of ?r' D] by auto 1478 hence 2: "{a1,a2} \<le> Field r" unfolding Field_bsqr by auto 1479 let ?m = "wo_rel.max2 r a1 a2" 1480 have "D \<le> (under r ?m) \<times> (under r ?m)" 1481 proof(unfold 1) 1482 {fix b1 b2 1483 let ?n = "wo_rel.max2 r b1 b2" 1484 assume "(b1,b2) \<in> underS ?r' (a1,a2)" 1485 hence 3: "((b1,b2),(a1,a2)) \<in> ?r'" 1486 unfolding underS_def by blast 1487 hence "(?n,?m) \<in> r" using WELL by (simp add: bsqr_max2) 1488 moreover 1489 {have "(b1,b2) \<in> Field ?r'" using 3 unfolding Field_def by auto 1490 hence "{b1,b2} \<le> Field r" unfolding Field_bsqr by auto 1491 hence "(b1,?n) \<in> r \<and> (b2,?n) \<in> r" 1492 using Well by (simp add: wo_rel.max2_greater) 1493 } 1494 ultimately have "(b1,?m) \<in> r \<and> (b2,?m) \<in> r" 1495 using Trans trans_def[of r] by blast 1496 hence "(b1,b2) \<in> (under r ?m) \<times> (under r ?m)" unfolding under_def by simp} 1497 thus "underS ?r' (a1,a2) \<le> (under r ?m) \<times> (under r ?m)" by auto 1498 qed 1499 moreover have "wo_rel.ofilter r (under r ?m)" 1500 using Well by (simp add: wo_rel.under_ofilter) 1501 moreover have "under r ?m < Field r" 1502 using NE under_Field[of r ?m] by blast 1503 ultimately show ?thesis by blast 1504qed 1505 1506definition Func where 1507"Func A B = {f . (\<forall> a \<in> A. f a \<in> B) \<and> (\<forall> a. a \<notin> A \<longrightarrow> f a = undefined)}" 1508 1509lemma Func_empty: 1510"Func {} B = {\<lambda>x. undefined}" 1511unfolding Func_def by auto 1512 1513lemma Func_elim: 1514assumes "g \<in> Func A B" and "a \<in> A" 1515shows "\<exists> b. b \<in> B \<and> g a = b" 1516using assms unfolding Func_def by (cases "g a = undefined") auto 1517 1518definition curr where 1519"curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined" 1520 1521lemma curr_in: 1522assumes f: "f \<in> Func (A \<times> B) C" 1523shows "curr A f \<in> Func A (Func B C)" 1524using assms unfolding curr_def Func_def by auto 1525 1526lemma curr_inj: 1527assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C" 1528shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2" 1529proof safe 1530 assume c: "curr A f1 = curr A f2" 1531 show "f1 = f2" 1532 proof (rule ext, clarify) 1533 fix a b show "f1 (a, b) = f2 (a, b)" 1534 proof (cases "(a,b) \<in> A \<times> B") 1535 case False 1536 thus ?thesis using assms unfolding Func_def by auto 1537 next 1538 case True hence a: "a \<in> A" and b: "b \<in> B" by auto 1539 thus ?thesis 1540 using c unfolding curr_def fun_eq_iff by(elim allE[of _ a]) simp 1541 qed 1542 qed 1543qed 1544 1545lemma curr_surj: 1546assumes "g \<in> Func A (Func B C)" 1547shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g" 1548proof 1549 let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined" 1550 show "curr A ?f = g" 1551 proof (rule ext) 1552 fix a show "curr A ?f a = g a" 1553 proof (cases "a \<in> A") 1554 case False 1555 hence "g a = undefined" using assms unfolding Func_def by auto 1556 thus ?thesis unfolding curr_def using False by simp 1557 next 1558 case True 1559 obtain g1 where "g1 \<in> Func B C" and "g a = g1" 1560 using assms using Func_elim[OF assms True] by blast 1561 thus ?thesis using True unfolding Func_def curr_def by auto 1562 qed 1563 qed 1564 show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto 1565qed 1566 1567lemma bij_betw_curr: 1568"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))" 1569unfolding bij_betw_def inj_on_def image_def 1570apply (intro impI conjI ballI) 1571apply (erule curr_inj[THEN iffD1], assumption+) 1572apply auto 1573apply (erule curr_in) 1574using curr_surj by blast 1575 1576definition Func_map where 1577"Func_map B2 f1 f2 g b2 \<equiv> if b2 \<in> B2 then f1 (g (f2 b2)) else undefined" 1578 1579lemma Func_map: 1580assumes g: "g \<in> Func A2 A1" and f1: "f1 ` A1 \<subseteq> B1" and f2: "f2 ` B2 \<subseteq> A2" 1581shows "Func_map B2 f1 f2 g \<in> Func B2 B1" 1582using assms unfolding Func_def Func_map_def mem_Collect_eq by auto 1583 1584lemma Func_non_emp: 1585assumes "B \<noteq> {}" 1586shows "Func A B \<noteq> {}" 1587proof- 1588 obtain b where b: "b \<in> B" using assms by auto 1589 hence "(\<lambda> a. if a \<in> A then b else undefined) \<in> Func A B" unfolding Func_def by auto 1590 thus ?thesis by blast 1591qed 1592 1593lemma Func_is_emp: 1594"Func A B = {} \<longleftrightarrow> A \<noteq> {} \<and> B = {}" (is "?L \<longleftrightarrow> ?R") 1595proof 1596 assume L: ?L 1597 moreover {assume "A = {}" hence False using L Func_empty by auto} 1598 moreover {assume "B \<noteq> {}" hence False using L Func_non_emp[of B A] by simp } 1599 ultimately show ?R by blast 1600next 1601 assume R: ?R 1602 moreover 1603 {fix f assume "f \<in> Func A B" 1604 moreover obtain a where "a \<in> A" using R by blast 1605 ultimately obtain b where "b \<in> B" unfolding Func_def by blast 1606 with R have False by blast 1607 } 1608 thus ?L by blast 1609qed 1610 1611lemma Func_map_surj: 1612assumes B1: "f1 ` A1 = B1" and A2: "inj_on f2 B2" "f2 ` B2 \<subseteq> A2" 1613and B2A2: "B2 = {} \<Longrightarrow> A2 = {}" 1614shows "Func B2 B1 = Func_map B2 f1 f2 ` Func A2 A1" 1615proof(cases "B2 = {}") 1616 case True 1617 thus ?thesis using B2A2 by (auto simp: Func_empty Func_map_def) 1618next 1619 case False note B2 = False 1620 show ?thesis 1621 proof safe 1622 fix h assume h: "h \<in> Func B2 B1" 1623 define j1 where "j1 = inv_into A1 f1" 1624 have "\<forall> a2 \<in> f2 ` B2. \<exists> b2. b2 \<in> B2 \<and> f2 b2 = a2" by blast 1625 then obtain k where k: "\<forall> a2 \<in> f2 ` B2. k a2 \<in> B2 \<and> f2 (k a2) = a2" 1626 by atomize_elim (rule bchoice) 1627 {fix b2 assume b2: "b2 \<in> B2" 1628 hence "f2 (k (f2 b2)) = f2 b2" using k A2(2) by auto 1629 moreover have "k (f2 b2) \<in> B2" using b2 A2(2) k by auto 1630 ultimately have "k (f2 b2) = b2" using b2 A2(1) unfolding inj_on_def by blast 1631 } note kk = this 1632 obtain b22 where b22: "b22 \<in> B2" using B2 by auto 1633 define j2 where [abs_def]: "j2 a2 = (if a2 \<in> f2 ` B2 then k a2 else b22)" for a2 1634 have j2A2: "j2 ` A2 \<subseteq> B2" unfolding j2_def using k b22 by auto 1635 have j2: "\<And> b2. b2 \<in> B2 \<Longrightarrow> j2 (f2 b2) = b2" 1636 using kk unfolding j2_def by auto 1637 define g where "g = Func_map A2 j1 j2 h" 1638 have "Func_map B2 f1 f2 g = h" 1639 proof (rule ext) 1640 fix b2 show "Func_map B2 f1 f2 g b2 = h b2" 1641 proof(cases "b2 \<in> B2") 1642 case True 1643 show ?thesis 1644 proof (cases "h b2 = undefined") 1645 case True 1646 hence b1: "h b2 \<in> f1 ` A1" using h \<open>b2 \<in> B2\<close> unfolding B1 Func_def by auto 1647 show ?thesis using A2 f_inv_into_f[OF b1] 1648 unfolding True g_def Func_map_def j1_def j2[OF \<open>b2 \<in> B2\<close>] by auto 1649 qed(insert A2 True j2[OF True] h B1, unfold j1_def g_def Func_def Func_map_def, 1650 auto intro: f_inv_into_f) 1651 qed(insert h, unfold Func_def Func_map_def, auto) 1652 qed 1653 moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h]) 1654 using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+ 1655 ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1" 1656 unfolding Func_map_def[abs_def] by auto 1657 qed(insert B1 Func_map[OF _ _ A2(2)], auto) 1658qed 1659 1660end 1661