1(* Title: HOL/BNF_Wellorder_Embedding.thy 2 Author: Andrei Popescu, TU Muenchen 3 Copyright 2012 4 5Well-order embeddings as needed by bounded natural functors. 6*) 7 8section \<open>Well-Order Embeddings as Needed by Bounded Natural Functors\<close> 9 10theory BNF_Wellorder_Embedding 11imports Hilbert_Choice BNF_Wellorder_Relation 12begin 13 14text\<open>In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and 15prove their basic properties. The notion of embedding is considered from the point 16of view of the theory of ordinals, and therefore requires the source to be injected 17as an {\em initial segment} (i.e., {\em order filter}) of the target. A main result 18of this section is the existence of embeddings (in one direction or another) between 19any two well-orders, having as a consequence the fact that, given any two sets on 20any two types, one is smaller than (i.e., can be injected into) the other.\<close> 21 22 23subsection \<open>Auxiliaries\<close> 24 25lemma UNION_inj_on_ofilter: 26assumes WELL: "Well_order r" and 27 OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and 28 INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)" 29shows "inj_on f (\<Union>i \<in> I. A i)" 30proof- 31 have "wo_rel r" using WELL by (simp add: wo_rel_def) 32 hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i" 33 using wo_rel.ofilter_linord[of r] OF by blast 34 with WELL INJ show ?thesis 35 by (auto simp add: inj_on_UNION_chain) 36qed 37 38lemma under_underS_bij_betw: 39assumes WELL: "Well_order r" and WELL': "Well_order r'" and 40 IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and 41 BIJ: "bij_betw f (underS r a) (underS r' (f a))" 42shows "bij_betw f (under r a) (under r' (f a))" 43proof- 44 have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)" 45 unfolding underS_def by auto 46 moreover 47 {have "Refl r \<and> Refl r'" using WELL WELL' 48 by (auto simp add: order_on_defs) 49 hence "under r a = underS r a \<union> {a} \<and> 50 under r' (f a) = underS r' (f a) \<union> {f a}" 51 using IN IN' by(auto simp add: Refl_under_underS) 52 } 53 ultimately show ?thesis 54 using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto 55qed 56 57 58subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible 59functions\<close> 60 61text\<open>Standardly, a function is an embedding of a well-order in another if it injectively and 62order-compatibly maps the former into an order filter of the latter. 63Here we opt for a more succinct definition (operator \<open>embed\<close>), 64asking that, for any element in the source, the function should be a bijection 65between the set of strict lower bounds of that element 66and the set of strict lower bounds of its image. (Later we prove equivalence with 67the standard definition -- lemma \<open>embed_iff_compat_inj_on_ofilter\<close>.) 68A {\em strict embedding} (operator \<open>embedS\<close>) is a non-bijective embedding 69and an isomorphism (operator \<open>iso\<close>) is a bijective embedding.\<close> 70 71definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" 72where 73"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))" 74 75lemmas embed_defs = embed_def embed_def[abs_def] 76 77text \<open>Strict embeddings:\<close> 78 79definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" 80where 81"embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')" 82 83lemmas embedS_defs = embedS_def embedS_def[abs_def] 84 85definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" 86where 87"iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')" 88 89lemmas iso_defs = iso_def iso_def[abs_def] 90 91definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool" 92where 93"compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'" 94 95lemma compat_wf: 96assumes CMP: "compat r r' f" and WF: "wf r'" 97shows "wf r" 98proof- 99 have "r \<le> inv_image r' f" 100 unfolding inv_image_def using CMP 101 by (auto simp add: compat_def) 102 with WF show ?thesis 103 using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto 104qed 105 106lemma id_embed: "embed r r id" 107by(auto simp add: id_def embed_def bij_betw_def) 108 109lemma id_iso: "iso r r id" 110by(auto simp add: id_def embed_def iso_def bij_betw_def) 111 112lemma embed_in_Field: 113assumes WELL: "Well_order r" and 114 EMB: "embed r r' f" and IN: "a \<in> Field r" 115shows "f a \<in> Field r'" 116proof- 117 have Well: "wo_rel r" 118 using WELL by (auto simp add: wo_rel_def) 119 hence 1: "Refl r" 120 by (auto simp add: wo_rel.REFL) 121 hence "a \<in> under r a" using IN Refl_under_in by fastforce 122 hence "f a \<in> under r' (f a)" 123 using EMB IN by (auto simp add: embed_def bij_betw_def) 124 thus ?thesis unfolding Field_def 125 by (auto simp: under_def) 126qed 127 128lemma comp_embed: 129assumes WELL: "Well_order r" and 130 EMB: "embed r r' f" and EMB': "embed r' r'' f'" 131shows "embed r r'' (f' \<circ> f)" 132proof(unfold embed_def, auto) 133 fix a assume *: "a \<in> Field r" 134 hence "bij_betw f (under r a) (under r' (f a))" 135 using embed_def[of r] EMB by auto 136 moreover 137 {have "f a \<in> Field r'" 138 using EMB WELL * by (auto simp add: embed_in_Field) 139 hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))" 140 using embed_def[of r'] EMB' by auto 141 } 142 ultimately 143 show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))" 144 by(auto simp add: bij_betw_trans) 145qed 146 147lemma comp_iso: 148assumes WELL: "Well_order r" and 149 EMB: "iso r r' f" and EMB': "iso r' r'' f'" 150shows "iso r r'' (f' \<circ> f)" 151using assms unfolding iso_def 152by (auto simp add: comp_embed bij_betw_trans) 153 154text\<open>That \<open>embedS\<close> is also preserved by function composition shall be proved only later.\<close> 155 156lemma embed_Field: 157"\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'" 158by (auto simp add: embed_in_Field) 159 160lemma embed_preserves_ofilter: 161assumes WELL: "Well_order r" and WELL': "Well_order r'" and 162 EMB: "embed r r' f" and OF: "wo_rel.ofilter r A" 163shows "wo_rel.ofilter r' (f`A)" 164proof- 165 (* Preliminary facts *) 166 from WELL have Well: "wo_rel r" unfolding wo_rel_def . 167 from WELL' have Well': "wo_rel r'" unfolding wo_rel_def . 168 from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def) 169 (* Main proof *) 170 show ?thesis using Well' WELL EMB 0 embed_Field[of r r' f] 171 proof(unfold wo_rel.ofilter_def, auto simp add: image_def) 172 fix a b' 173 assume *: "a \<in> A" and **: "b' \<in> under r' (f a)" 174 hence "a \<in> Field r" using 0 by auto 175 hence "bij_betw f (under r a) (under r' (f a))" 176 using * EMB by (auto simp add: embed_def) 177 hence "f`(under r a) = under r' (f a)" 178 by (simp add: bij_betw_def) 179 with ** image_def[of f "under r a"] obtain b where 180 1: "b \<in> under r a \<and> b' = f b" by blast 181 hence "b \<in> A" using Well * OF 182 by (auto simp add: wo_rel.ofilter_def) 183 with 1 show "\<exists>b \<in> A. b' = f b" by blast 184 qed 185qed 186 187lemma embed_Field_ofilter: 188assumes WELL: "Well_order r" and WELL': "Well_order r'" and 189 EMB: "embed r r' f" 190shows "wo_rel.ofilter r' (f`(Field r))" 191proof- 192 have "wo_rel.ofilter r (Field r)" 193 using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter) 194 with WELL WELL' EMB 195 show ?thesis by (auto simp add: embed_preserves_ofilter) 196qed 197 198lemma embed_compat: 199assumes EMB: "embed r r' f" 200shows "compat r r' f" 201proof(unfold compat_def, clarify) 202 fix a b 203 assume *: "(a,b) \<in> r" 204 hence 1: "b \<in> Field r" using Field_def[of r] by blast 205 have "a \<in> under r b" 206 using * under_def[of r] by simp 207 hence "f a \<in> under r' (f b)" 208 using EMB embed_def[of r r' f] 209 bij_betw_def[of f "under r b" "under r' (f b)"] 210 image_def[of f "under r b"] 1 by auto 211 thus "(f a, f b) \<in> r'" 212 by (auto simp add: under_def) 213qed 214 215lemma embed_inj_on: 216assumes WELL: "Well_order r" and EMB: "embed r r' f" 217shows "inj_on f (Field r)" 218proof(unfold inj_on_def, clarify) 219 (* Preliminary facts *) 220 from WELL have Well: "wo_rel r" unfolding wo_rel_def . 221 with wo_rel.TOTAL[of r] 222 have Total: "Total r" by simp 223 from Well wo_rel.REFL[of r] 224 have Refl: "Refl r" by simp 225 (* Main proof *) 226 fix a b 227 assume *: "a \<in> Field r" and **: "b \<in> Field r" and 228 ***: "f a = f b" 229 hence 1: "a \<in> Field r \<and> b \<in> Field r" 230 unfolding Field_def by auto 231 {assume "(a,b) \<in> r" 232 hence "a \<in> under r b \<and> b \<in> under r b" 233 using Refl by(auto simp add: under_def refl_on_def) 234 hence "a = b" 235 using EMB 1 *** 236 by (auto simp add: embed_def bij_betw_def inj_on_def) 237 } 238 moreover 239 {assume "(b,a) \<in> r" 240 hence "a \<in> under r a \<and> b \<in> under r a" 241 using Refl by(auto simp add: under_def refl_on_def) 242 hence "a = b" 243 using EMB 1 *** 244 by (auto simp add: embed_def bij_betw_def inj_on_def) 245 } 246 ultimately 247 show "a = b" using Total 1 248 by (auto simp add: total_on_def) 249qed 250 251lemma embed_underS: 252assumes WELL: "Well_order r" and WELL': "Well_order r'" and 253 EMB: "embed r r' f" and IN: "a \<in> Field r" 254shows "bij_betw f (underS r a) (underS r' (f a))" 255proof- 256 have "bij_betw f (under r a) (under r' (f a))" 257 using assms by (auto simp add: embed_def) 258 moreover 259 {have "f a \<in> Field r'" using assms embed_Field[of r r' f] by auto 260 hence "under r a = underS r a \<union> {a} \<and> 261 under r' (f a) = underS r' (f a) \<union> {f a}" 262 using assms by (auto simp add: order_on_defs Refl_under_underS) 263 } 264 moreover 265 {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)" 266 unfolding underS_def by blast 267 } 268 ultimately show ?thesis 269 by (auto simp add: notIn_Un_bij_betw3) 270qed 271 272lemma embed_iff_compat_inj_on_ofilter: 273assumes WELL: "Well_order r" and WELL': "Well_order r'" 274shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))" 275using assms 276proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter, 277 unfold embed_def, auto) (* get rid of one implication *) 278 fix a 279 assume *: "inj_on f (Field r)" and 280 **: "compat r r' f" and 281 ***: "wo_rel.ofilter r' (f`(Field r))" and 282 ****: "a \<in> Field r" 283 (* Preliminary facts *) 284 have Well: "wo_rel r" 285 using WELL wo_rel_def[of r] by simp 286 hence Refl: "Refl r" 287 using wo_rel.REFL[of r] by simp 288 have Total: "Total r" 289 using Well wo_rel.TOTAL[of r] by simp 290 have Well': "wo_rel r'" 291 using WELL' wo_rel_def[of r'] by simp 292 hence Antisym': "antisym r'" 293 using wo_rel.ANTISYM[of r'] by simp 294 have "(a,a) \<in> r" 295 using **** Well wo_rel.REFL[of r] 296 refl_on_def[of _ r] by auto 297 hence "(f a, f a) \<in> r'" 298 using ** by(auto simp add: compat_def) 299 hence 0: "f a \<in> Field r'" 300 unfolding Field_def by auto 301 have "f a \<in> f`(Field r)" 302 using **** by auto 303 hence 2: "under r' (f a) \<le> f`(Field r)" 304 using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce 305 (* Main proof *) 306 show "bij_betw f (under r a) (under r' (f a))" 307 proof(unfold bij_betw_def, auto) 308 show "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field]) 309 next 310 fix b assume "b \<in> under r a" 311 thus "f b \<in> under r' (f a)" 312 unfolding under_def using ** 313 by (auto simp add: compat_def) 314 next 315 fix b' assume *****: "b' \<in> under r' (f a)" 316 hence "b' \<in> f`(Field r)" 317 using 2 by auto 318 with Field_def[of r] obtain b where 319 3: "b \<in> Field r" and 4: "b' = f b" by auto 320 have "(b,a) \<in> r" 321 proof- 322 {assume "(a,b) \<in> r" 323 with ** 4 have "(f a, b') \<in> r'" 324 by (auto simp add: compat_def) 325 with ***** Antisym' have "f a = b'" 326 by(auto simp add: under_def antisym_def) 327 with 3 **** 4 * have "a = b" 328 by(auto simp add: inj_on_def) 329 } 330 moreover 331 {assume "a = b" 332 hence "(b,a) \<in> r" using Refl **** 3 333 by (auto simp add: refl_on_def) 334 } 335 ultimately 336 show ?thesis using Total **** 3 by (fastforce simp add: total_on_def) 337 qed 338 with 4 show "b' \<in> f`(under r a)" 339 unfolding under_def by auto 340 qed 341qed 342 343lemma inv_into_ofilter_embed: 344assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and 345 BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and 346 IMAGE: "f ` A = Field r'" 347shows "embed r' r (inv_into A f)" 348proof- 349 (* Preliminary facts *) 350 have Well: "wo_rel r" 351 using WELL wo_rel_def[of r] by simp 352 have Refl: "Refl r" 353 using Well wo_rel.REFL[of r] by simp 354 have Total: "Total r" 355 using Well wo_rel.TOTAL[of r] by simp 356 (* Main proof *) 357 have 1: "bij_betw f A (Field r')" 358 proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE) 359 fix b1 b2 360 assume *: "b1 \<in> A" and **: "b2 \<in> A" and 361 ***: "f b1 = f b2" 362 have 11: "b1 \<in> Field r \<and> b2 \<in> Field r" 363 using * ** Well OF by (auto simp add: wo_rel.ofilter_def) 364 moreover 365 {assume "(b1,b2) \<in> r" 366 hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2" 367 unfolding under_def using 11 Refl 368 by (auto simp add: refl_on_def) 369 hence "b1 = b2" using BIJ * ** *** 370 by (simp add: bij_betw_def inj_on_def) 371 } 372 moreover 373 {assume "(b2,b1) \<in> r" 374 hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1" 375 unfolding under_def using 11 Refl 376 by (auto simp add: refl_on_def) 377 hence "b1 = b2" using BIJ * ** *** 378 by (simp add: bij_betw_def inj_on_def) 379 } 380 ultimately 381 show "b1 = b2" 382 using Total by (auto simp add: total_on_def) 383 qed 384 (* *) 385 let ?f' = "(inv_into A f)" 386 (* *) 387 have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)" 388 proof(clarify) 389 fix b assume *: "b \<in> A" 390 hence "under r b \<le> A" 391 using Well OF by(auto simp add: wo_rel.ofilter_def) 392 moreover 393 have "f ` (under r b) = under r' (f b)" 394 using * BIJ by (auto simp add: bij_betw_def) 395 ultimately 396 show "bij_betw ?f' (under r' (f b)) (under r b)" 397 using 1 by (auto simp add: bij_betw_inv_into_subset) 398 qed 399 (* *) 400 have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))" 401 proof(clarify) 402 fix b' assume *: "b' \<in> Field r'" 403 have "b' = f (?f' b')" using * 1 404 by (auto simp add: bij_betw_inv_into_right) 405 moreover 406 {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force 407 hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left) 408 with 31 have "?f' b' \<in> A" by auto 409 } 410 ultimately 411 show "bij_betw ?f' (under r' b') (under r (?f' b'))" 412 using 2 by auto 413 qed 414 (* *) 415 thus ?thesis unfolding embed_def . 416qed 417 418lemma inv_into_underS_embed: 419assumes WELL: "Well_order r" and 420 BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and 421 IN: "a \<in> Field r" and 422 IMAGE: "f ` (underS r a) = Field r'" 423shows "embed r' r (inv_into (underS r a) f)" 424using assms 425by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed) 426 427lemma inv_into_Field_embed: 428assumes WELL: "Well_order r" and EMB: "embed r r' f" and 429 IMAGE: "Field r' \<le> f ` (Field r)" 430shows "embed r' r (inv_into (Field r) f)" 431proof- 432 have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))" 433 using EMB by (auto simp add: embed_def) 434 moreover 435 have "f ` (Field r) \<le> Field r'" 436 using EMB WELL by (auto simp add: embed_Field) 437 ultimately 438 show ?thesis using assms 439 by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed) 440qed 441 442lemma inv_into_Field_embed_bij_betw: 443assumes WELL: "Well_order r" and 444 EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')" 445shows "embed r' r (inv_into (Field r) f)" 446proof- 447 have "Field r' \<le> f ` (Field r)" 448 using BIJ by (auto simp add: bij_betw_def) 449 thus ?thesis using assms 450 by(auto simp add: inv_into_Field_embed) 451qed 452 453 454subsection \<open>Given any two well-orders, one can be embedded in the other\<close> 455 456text\<open>Here is an overview of the proof of of this fact, stated in theorem 457\<open>wellorders_totally_ordered\<close>: 458 459 Fix the well-orders \<open>r::'a rel\<close> and \<open>r'::'a' rel\<close>. 460 Attempt to define an embedding \<open>f::'a \<Rightarrow> 'a'\<close> from \<open>r\<close> to \<open>r'\<close> in the 461 natural way by well-order recursion ("hoping" that \<open>Field r\<close> turns out to be smaller 462 than \<open>Field r'\<close>), but also record, at the recursive step, in a function 463 \<open>g::'a \<Rightarrow> bool\<close>, the extra information of whether \<open>Field r'\<close> 464 gets exhausted or not. 465 466 If \<open>Field r'\<close> does not get exhausted, then \<open>Field r\<close> is indeed smaller 467 and \<open>f\<close> is the desired embedding from \<open>r\<close> to \<open>r'\<close> 468 (lemma \<open>wellorders_totally_ordered_aux\<close>). 469 470 Otherwise, it means that \<open>Field r'\<close> is the smaller one, and the inverse of 471 (the "good" segment of) \<open>f\<close> is the desired embedding from \<open>r'\<close> to \<open>r\<close> 472 (lemma \<open>wellorders_totally_ordered_aux2\<close>). 473\<close> 474 475lemma wellorders_totally_ordered_aux: 476fixes r ::"'a rel" and r'::"'a' rel" and 477 f :: "'a \<Rightarrow> 'a'" and a::'a 478assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and 479 IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and 480 NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))" 481shows "bij_betw f (under r a) (under r' (f a))" 482proof- 483 (* Preliminary facts *) 484 have Well: "wo_rel r" using WELL unfolding wo_rel_def . 485 hence Refl: "Refl r" using wo_rel.REFL[of r] by auto 486 have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto 487 have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . 488 have OF: "wo_rel.ofilter r (underS r a)" 489 by (auto simp add: Well wo_rel.underS_ofilter) 490 hence UN: "underS r a = (\<Union>b \<in> underS r a. under r b)" 491 using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast 492 (* Gather facts about elements of underS r a *) 493 {fix b assume *: "b \<in> underS r a" 494 hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto 495 have t1: "b \<in> Field r" 496 using * underS_Field[of r a] by auto 497 have t2: "f`(under r b) = under r' (f b)" 498 using IH * by (auto simp add: bij_betw_def) 499 hence t3: "wo_rel.ofilter r' (f`(under r b))" 500 using Well' by (auto simp add: wo_rel.under_ofilter) 501 have "f`(under r b) \<le> Field r'" 502 using t2 by (auto simp add: under_Field) 503 moreover 504 have "b \<in> under r b" 505 using t1 by(auto simp add: Refl Refl_under_in) 506 ultimately 507 have t4: "f b \<in> Field r'" by auto 508 have "f`(under r b) = under r' (f b) \<and> 509 wo_rel.ofilter r' (f`(under r b)) \<and> 510 f b \<in> Field r'" 511 using t2 t3 t4 by auto 512 } 513 hence bFact: 514 "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and> 515 wo_rel.ofilter r' (f`(under r b)) \<and> 516 f b \<in> Field r'" by blast 517 (* *) 518 have subField: "f`(underS r a) \<le> Field r'" 519 using bFact by blast 520 (* *) 521 have OF': "wo_rel.ofilter r' (f`(underS r a))" 522 proof- 523 have "f`(underS r a) = f`(\<Union>b \<in> underS r a. under r b)" 524 using UN by auto 525 also have "\<dots> = (\<Union>b \<in> underS r a. f`(under r b))" by blast 526 also have "\<dots> = (\<Union>b \<in> underS r a. (under r' (f b)))" 527 using bFact by auto 528 finally 529 have "f`(underS r a) = (\<Union>b \<in> underS r a. (under r' (f b)))" . 530 thus ?thesis 531 using Well' bFact 532 wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce 533 qed 534 (* *) 535 have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'" 536 using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field) 537 hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}" 538 using subField NOT by blast 539 (* Main proof *) 540 have INCL1: "f`(underS r a) \<le> underS r' (f a) " 541 proof(auto) 542 fix b assume *: "b \<in> underS r a" 543 have "f b \<noteq> f a \<and> (f b, f a) \<in> r'" 544 using subField Well' SUC NE * 545 wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force 546 thus "f b \<in> underS r' (f a)" 547 unfolding underS_def by simp 548 qed 549 (* *) 550 have INCL2: "underS r' (f a) \<le> f`(underS r a)" 551 proof 552 fix b' assume "b' \<in> underS r' (f a)" 553 hence "b' \<noteq> f a \<and> (b', f a) \<in> r'" 554 unfolding underS_def by simp 555 thus "b' \<in> f`(underS r a)" 556 using Well' SUC NE OF' 557 wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto 558 qed 559 (* *) 560 have INJ: "inj_on f (underS r a)" 561 proof- 562 have "\<forall>b \<in> underS r a. inj_on f (under r b)" 563 using IH by (auto simp add: bij_betw_def) 564 moreover 565 have "\<forall>b. wo_rel.ofilter r (under r b)" 566 using Well by (auto simp add: wo_rel.under_ofilter) 567 ultimately show ?thesis 568 using WELL bFact UN 569 UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f] 570 by auto 571 qed 572 (* *) 573 have BIJ: "bij_betw f (underS r a) (underS r' (f a))" 574 unfolding bij_betw_def 575 using INJ INCL1 INCL2 by auto 576 (* *) 577 have "f a \<in> Field r'" 578 using Well' subField NE SUC 579 by (auto simp add: wo_rel.suc_inField) 580 thus ?thesis 581 using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto 582qed 583 584lemma wellorders_totally_ordered_aux2: 585fixes r ::"'a rel" and r'::"'a' rel" and 586 f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a 587assumes WELL: "Well_order r" and WELL': "Well_order r'" and 588MAIN1: 589 "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r' 590 \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) 591 \<and> 592 (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r') 593 \<longrightarrow> g a = False)" and 594MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow> 595 bij_betw f (under r a) (under r' (f a))" and 596Case: "a \<in> Field r \<and> False \<in> g`(under r a)" 597shows "\<exists>f'. embed r' r f'" 598proof- 599 have Well: "wo_rel r" using WELL unfolding wo_rel_def . 600 hence Refl: "Refl r" using wo_rel.REFL[of r] by auto 601 have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto 602 have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto 603 have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . 604 (* *) 605 have 0: "under r a = underS r a \<union> {a}" 606 using Refl Case by(auto simp add: Refl_under_underS) 607 (* *) 608 have 1: "g a = False" 609 proof- 610 {assume "g a \<noteq> False" 611 with 0 Case have "False \<in> g`(underS r a)" by blast 612 with MAIN1 have "g a = False" by blast} 613 thus ?thesis by blast 614 qed 615 let ?A = "{a \<in> Field r. g a = False}" 616 let ?a = "(wo_rel.minim r ?A)" 617 (* *) 618 have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast 619 (* *) 620 have 3: "False \<notin> g`(underS r ?a)" 621 proof 622 assume "False \<in> g`(underS r ?a)" 623 then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto 624 hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a" 625 by (auto simp add: underS_def) 626 hence "b \<in> Field r" unfolding Field_def by auto 627 with 31 have "b \<in> ?A" by auto 628 hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce 629 (* again: why worked without type annotations? *) 630 with 32 Antisym show False 631 by (auto simp add: antisym_def) 632 qed 633 have temp: "?a \<in> ?A" 634 using Well 2 wo_rel.minim_in[of r ?A] by auto 635 hence 4: "?a \<in> Field r" by auto 636 (* *) 637 have 5: "g ?a = False" using temp by blast 638 (* *) 639 have 6: "f`(underS r ?a) = Field r'" 640 using MAIN1[of ?a] 3 5 by blast 641 (* *) 642 have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))" 643 proof 644 fix b assume as: "b \<in> underS r ?a" 645 moreover 646 have "wo_rel.ofilter r (underS r ?a)" 647 using Well by (auto simp add: wo_rel.underS_ofilter) 648 ultimately 649 have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+ 650 moreover have "b \<in> Field r" 651 unfolding Field_def using as by (auto simp add: underS_def) 652 ultimately 653 show "bij_betw f (under r b) (under r' (f b))" 654 using MAIN2 by auto 655 qed 656 (* *) 657 have "embed r' r (inv_into (underS r ?a) f)" 658 using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto 659 thus ?thesis 660 unfolding embed_def by blast 661qed 662 663theorem wellorders_totally_ordered: 664fixes r ::"'a rel" and r'::"'a' rel" 665assumes WELL: "Well_order r" and WELL': "Well_order r'" 666shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')" 667proof- 668 (* Preliminary facts *) 669 have Well: "wo_rel r" using WELL unfolding wo_rel_def . 670 hence Refl: "Refl r" using wo_rel.REFL[of r] by auto 671 have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto 672 have Well': "wo_rel r'" using WELL' unfolding wo_rel_def . 673 (* Main proof *) 674 obtain H where H_def: "H = 675 (\<lambda>h a. if False \<notin> (snd \<circ> h)`(underS r a) \<and> (fst \<circ> h)`(underS r a) \<noteq> Field r' 676 then (wo_rel.suc r' ((fst \<circ> h)`(underS r a)), True) 677 else (undefined, False))" by blast 678 have Adm: "wo_rel.adm_wo r H" 679 using Well 680 proof(unfold wo_rel.adm_wo_def, clarify) 681 fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x 682 assume "\<forall>y\<in>underS r x. h1 y = h2 y" 683 hence "\<forall>y\<in>underS r x. (fst \<circ> h1) y = (fst \<circ> h2) y \<and> 684 (snd \<circ> h1) y = (snd \<circ> h2) y" by auto 685 hence "(fst \<circ> h1)`(underS r x) = (fst \<circ> h2)`(underS r x) \<and> 686 (snd \<circ> h1)`(underS r x) = (snd \<circ> h2)`(underS r x)" 687 by (auto simp add: image_def) 688 thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball) 689 qed 690 (* More constant definitions: *) 691 obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool" 692 where h_def: "h = wo_rel.worec r H" and 693 f_def: "f = fst \<circ> h" and g_def: "g = snd \<circ> h" by blast 694 obtain test where test_def: 695 "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast 696 (* *) 697 have *: "\<And> a. h a = H h a" 698 using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def) 699 have Main1: 700 "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and> 701 (\<not>(test a) \<longrightarrow> g a = False)" 702 proof- (* How can I prove this withou fixing a? *) 703 fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and> 704 (\<not>(test a) \<longrightarrow> g a = False)" 705 using *[of a] test_def f_def g_def H_def by auto 706 qed 707 (* *) 708 let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow> 709 bij_betw f (under r a) (under r' (f a))" 710 have Main2: "\<And> a. ?phi a" 711 proof- 712 fix a show "?phi a" 713 proof(rule wo_rel.well_order_induct[of r ?phi], 714 simp only: Well, clarify) 715 fix a 716 assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and 717 *: "a \<in> Field r" and 718 **: "False \<notin> g`(under r a)" 719 have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" 720 proof(clarify) 721 fix b assume ***: "b \<in> underS r a" 722 hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto 723 moreover have "b \<in> Field r" 724 using *** underS_Field[of r a] by auto 725 moreover have "False \<notin> g`(under r b)" 726 using 0 ** Trans under_incr[of r b a] by auto 727 ultimately show "bij_betw f (under r b) (under r' (f b))" 728 using IH by auto 729 qed 730 (* *) 731 have 21: "False \<notin> g`(underS r a)" 732 using ** underS_subset_under[of r a] by auto 733 have 22: "g`(under r a) \<le> {True}" using ** by auto 734 moreover have 23: "a \<in> under r a" 735 using Refl * by (auto simp add: Refl_under_in) 736 ultimately have 24: "g a = True" by blast 737 have 2: "f`(underS r a) \<noteq> Field r'" 738 proof 739 assume "f`(underS r a) = Field r'" 740 hence "g a = False" using Main1 test_def by blast 741 with 24 show False using ** by blast 742 qed 743 (* *) 744 have 3: "f a = wo_rel.suc r' (f`(underS r a))" 745 using 21 2 Main1 test_def by blast 746 (* *) 747 show "bij_betw f (under r a) (under r' (f a))" 748 using WELL WELL' 1 2 3 * 749 wellorders_totally_ordered_aux[of r r' a f] by auto 750 qed 751 qed 752 (* *) 753 let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))" 754 show ?thesis 755 proof(cases "\<exists>a. ?chi a") 756 assume "\<not> (\<exists>a. ?chi a)" 757 hence "\<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))" 758 using Main2 by blast 759 thus ?thesis unfolding embed_def by blast 760 next 761 assume "\<exists>a. ?chi a" 762 then obtain a where "?chi a" by blast 763 hence "\<exists>f'. embed r' r f'" 764 using wellorders_totally_ordered_aux2[of r r' g f a] 765 WELL WELL' Main1 Main2 test_def by fast 766 thus ?thesis by blast 767 qed 768qed 769 770 771subsection \<open>Uniqueness of embeddings\<close> 772 773text\<open>Here we show a fact complementary to the one from the previous subsection -- namely, 774that between any two well-orders there is {\em at most} one embedding, and is the one 775definable by the expected well-order recursive equation. As a consequence, any two 776embeddings of opposite directions are mutually inverse.\<close> 777 778lemma embed_determined: 779assumes WELL: "Well_order r" and WELL': "Well_order r'" and 780 EMB: "embed r r' f" and IN: "a \<in> Field r" 781shows "f a = wo_rel.suc r' (f`(underS r a))" 782proof- 783 have "bij_betw f (underS r a) (underS r' (f a))" 784 using assms by (auto simp add: embed_underS) 785 hence "f`(underS r a) = underS r' (f a)" 786 by (auto simp add: bij_betw_def) 787 moreover 788 {have "f a \<in> Field r'" using IN 789 using EMB WELL embed_Field[of r r' f] by auto 790 hence "f a = wo_rel.suc r' (underS r' (f a))" 791 using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS) 792 } 793 ultimately show ?thesis by simp 794qed 795 796lemma embed_unique: 797assumes WELL: "Well_order r" and WELL': "Well_order r'" and 798 EMBf: "embed r r' f" and EMBg: "embed r r' g" 799shows "a \<in> Field r \<longrightarrow> f a = g a" 800proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def) 801 fix a 802 assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and 803 *: "a \<in> Field r" 804 hence "\<forall>b \<in> underS r a. f b = g b" 805 unfolding underS_def by (auto simp add: Field_def) 806 hence "f`(underS r a) = g`(underS r a)" by force 807 thus "f a = g a" 808 using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto 809qed 810 811lemma embed_bothWays_inverse: 812assumes WELL: "Well_order r" and WELL': "Well_order r'" and 813 EMB: "embed r r' f" and EMB': "embed r' r f'" 814shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')" 815proof- 816 have "embed r r (f' \<circ> f)" using assms 817 by(auto simp add: comp_embed) 818 moreover have "embed r r id" using assms 819 by (auto simp add: id_embed) 820 ultimately have "\<forall>a \<in> Field r. f'(f a) = a" 821 using assms embed_unique[of r r "f' \<circ> f" id] id_def by auto 822 moreover 823 {have "embed r' r' (f \<circ> f')" using assms 824 by(auto simp add: comp_embed) 825 moreover have "embed r' r' id" using assms 826 by (auto simp add: id_embed) 827 ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'" 828 using assms embed_unique[of r' r' "f \<circ> f'" id] id_def by auto 829 } 830 ultimately show ?thesis by blast 831qed 832 833lemma embed_bothWays_bij_betw: 834assumes WELL: "Well_order r" and WELL': "Well_order r'" and 835 EMB: "embed r r' f" and EMB': "embed r' r g" 836shows "bij_betw f (Field r) (Field r')" 837proof- 838 let ?A = "Field r" let ?A' = "Field r'" 839 have "embed r r (g \<circ> f) \<and> embed r' r' (f \<circ> g)" 840 using assms by (auto simp add: comp_embed) 841 hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')" 842 using WELL id_embed[of r] embed_unique[of r r "g \<circ> f" id] 843 WELL' id_embed[of r'] embed_unique[of r' r' "f \<circ> g" id] 844 id_def by auto 845 have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)" 846 using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast 847 (* *) 848 show ?thesis 849 proof(unfold bij_betw_def inj_on_def, auto simp add: 2) 850 fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b" 851 have "a = g(f a) \<and> b = g(f b)" using * 1 by auto 852 with ** show "a = b" by auto 853 next 854 fix a' assume *: "a' \<in> ?A'" 855 hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto 856 thus "a' \<in> f ` ?A" by force 857 qed 858qed 859 860lemma embed_bothWays_iso: 861assumes WELL: "Well_order r" and WELL': "Well_order r'" and 862 EMB: "embed r r' f" and EMB': "embed r' r g" 863shows "iso r r' f" 864unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw) 865 866 867subsection \<open>More properties of embeddings, strict embeddings and isomorphisms\<close> 868 869lemma embed_bothWays_Field_bij_betw: 870assumes WELL: "Well_order r" and WELL': "Well_order r'" and 871 EMB: "embed r r' f" and EMB': "embed r' r f'" 872shows "bij_betw f (Field r) (Field r')" 873proof- 874 have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')" 875 using assms by (auto simp add: embed_bothWays_inverse) 876 moreover 877 have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r" 878 using assms by (auto simp add: embed_Field) 879 ultimately 880 show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto 881qed 882 883lemma embedS_comp_embed: 884assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 885 and EMB: "embedS r r' f" and EMB': "embed r' r'' f'" 886shows "embedS r r'' (f' \<circ> f)" 887proof- 888 let ?g = "(f' \<circ> f)" let ?h = "inv_into (Field r) ?g" 889 have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))" 890 using EMB by (auto simp add: embedS_def) 891 hence 2: "embed r r'' ?g" 892 using WELL EMB' comp_embed[of r r' f r'' f'] by auto 893 moreover 894 {assume "bij_betw ?g (Field r) (Field r'')" 895 hence "embed r'' r ?h" using 2 WELL 896 by (auto simp add: inv_into_Field_embed_bij_betw) 897 hence "embed r' r (?h \<circ> f')" using WELL' EMB' 898 by (auto simp add: comp_embed) 899 hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1 900 by (auto simp add: embed_bothWays_Field_bij_betw) 901 with 1 have False by blast 902 } 903 ultimately show ?thesis unfolding embedS_def by auto 904qed 905 906lemma embed_comp_embedS: 907assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 908 and EMB: "embed r r' f" and EMB': "embedS r' r'' f'" 909shows "embedS r r'' (f' \<circ> f)" 910proof- 911 let ?g = "(f' \<circ> f)" let ?h = "inv_into (Field r) ?g" 912 have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))" 913 using EMB' by (auto simp add: embedS_def) 914 hence 2: "embed r r'' ?g" 915 using WELL EMB comp_embed[of r r' f r'' f'] by auto 916 moreover 917 {assume "bij_betw ?g (Field r) (Field r'')" 918 hence "embed r'' r ?h" using 2 WELL 919 by (auto simp add: inv_into_Field_embed_bij_betw) 920 hence "embed r'' r' (f \<circ> ?h)" using WELL'' EMB 921 by (auto simp add: comp_embed) 922 hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1 923 by (auto simp add: embed_bothWays_Field_bij_betw) 924 with 1 have False by blast 925 } 926 ultimately show ?thesis unfolding embedS_def by auto 927qed 928 929lemma embed_comp_iso: 930assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 931 and EMB: "embed r r' f" and EMB': "iso r' r'' f'" 932shows "embed r r'' (f' \<circ> f)" 933using assms unfolding iso_def 934by (auto simp add: comp_embed) 935 936lemma iso_comp_embed: 937assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 938 and EMB: "iso r r' f" and EMB': "embed r' r'' f'" 939shows "embed r r'' (f' \<circ> f)" 940using assms unfolding iso_def 941by (auto simp add: comp_embed) 942 943lemma embedS_comp_iso: 944assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 945 and EMB: "embedS r r' f" and EMB': "iso r' r'' f'" 946shows "embedS r r'' (f' \<circ> f)" 947using assms unfolding iso_def 948by (auto simp add: embedS_comp_embed) 949 950lemma iso_comp_embedS: 951assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''" 952 and EMB: "iso r r' f" and EMB': "embedS r' r'' f'" 953shows "embedS r r'' (f' \<circ> f)" 954using assms unfolding iso_def using embed_comp_embedS 955by (auto simp add: embed_comp_embedS) 956 957lemma embedS_Field: 958assumes WELL: "Well_order r" and EMB: "embedS r r' f" 959shows "f ` (Field r) < Field r'" 960proof- 961 have "f`(Field r) \<le> Field r'" using assms 962 by (auto simp add: embed_Field embedS_def) 963 moreover 964 {have "inj_on f (Field r)" using assms 965 by (auto simp add: embedS_def embed_inj_on) 966 hence "f`(Field r) \<noteq> Field r'" using EMB 967 by (auto simp add: embedS_def bij_betw_def) 968 } 969 ultimately show ?thesis by blast 970qed 971 972lemma embedS_iff: 973assumes WELL: "Well_order r" and ISO: "embed r r' f" 974shows "embedS r r' f = (f ` (Field r) < Field r')" 975proof 976 assume "embedS r r' f" 977 thus "f ` Field r \<subset> Field r'" 978 using WELL by (auto simp add: embedS_Field) 979next 980 assume "f ` Field r \<subset> Field r'" 981 hence "\<not> bij_betw f (Field r) (Field r')" 982 unfolding bij_betw_def by blast 983 thus "embedS r r' f" unfolding embedS_def 984 using ISO by auto 985qed 986 987lemma iso_Field: 988"iso r r' f \<Longrightarrow> f ` (Field r) = Field r'" 989by (auto simp add: iso_def bij_betw_def) 990 991lemma iso_iff: 992assumes "Well_order r" 993shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')" 994proof 995 assume "iso r r' f" 996 thus "embed r r' f \<and> f ` (Field r) = Field r'" 997 by (auto simp add: iso_Field iso_def) 998next 999 assume *: "embed r r' f \<and> f ` Field r = Field r'" 1000 hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on) 1001 with * have "bij_betw f (Field r) (Field r')" 1002 unfolding bij_betw_def by simp 1003 with * show "iso r r' f" unfolding iso_def by auto 1004qed 1005 1006lemma iso_iff2: 1007assumes "Well_order r" 1008shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> 1009 (\<forall>a \<in> Field r. \<forall>b \<in> Field r. 1010 (((a,b) \<in> r) = ((f a, f b) \<in> r'))))" 1011using assms 1012proof(auto simp add: iso_def) 1013 fix a b 1014 assume "embed r r' f" 1015 hence "compat r r' f" using embed_compat[of r] by auto 1016 moreover assume "(a,b) \<in> r" 1017 ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto 1018next 1019 let ?f' = "inv_into (Field r) f" 1020 assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')" 1021 hence "embed r' r ?f'" using assms 1022 by (auto simp add: inv_into_Field_embed_bij_betw) 1023 hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto 1024 fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'" 1025 hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1 1026 by (auto simp add: bij_betw_inv_into_left) 1027 thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce 1028next 1029 assume *: "bij_betw f (Field r) (Field r')" and 1030 **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')" 1031 have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'" 1032 by (auto simp add: under_Field) 1033 have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def) 1034 {fix a assume ***: "a \<in> Field r" 1035 have "bij_betw f (under r a) (under r' (f a))" 1036 proof(unfold bij_betw_def, auto) 1037 show "inj_on f (under r a)" using 1 2 subset_inj_on by blast 1038 next 1039 fix b assume "b \<in> under r a" 1040 hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r" 1041 unfolding under_def by (auto simp add: Field_def Range_def Domain_def) 1042 with 1 ** show "f b \<in> under r' (f a)" 1043 unfolding under_def by auto 1044 next 1045 fix b' assume "b' \<in> under r' (f a)" 1046 hence 3: "(b',f a) \<in> r'" unfolding under_def by simp 1047 hence "b' \<in> Field r'" unfolding Field_def by auto 1048 with * obtain b where "b \<in> Field r \<and> f b = b'" 1049 unfolding bij_betw_def by force 1050 with 3 ** *** 1051 show "b' \<in> f ` (under r a)" unfolding under_def by blast 1052 qed 1053 } 1054 thus "embed r r' f" unfolding embed_def using * by auto 1055qed 1056 1057lemma iso_iff3: 1058assumes WELL: "Well_order r" and WELL': "Well_order r'" 1059shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)" 1060proof 1061 assume "iso r r' f" 1062 thus "bij_betw f (Field r) (Field r') \<and> compat r r' f" 1063 unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def) 1064next 1065 have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL' 1066 by (auto simp add: wo_rel_def) 1067 assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f" 1068 thus "iso r r' f" 1069 unfolding "compat_def" using assms 1070 proof(auto simp add: iso_iff2) 1071 fix a b assume **: "a \<in> Field r" "b \<in> Field r" and 1072 ***: "(f a, f b) \<in> r'" 1073 {assume "(b,a) \<in> r \<or> b = a" 1074 hence "(b,a) \<in> r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast 1075 hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto 1076 hence "f a = f b" 1077 using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast 1078 hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto 1079 hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast 1080 } 1081 thus "(a,b) \<in> r" 1082 using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast 1083 qed 1084qed 1085 1086end 1087