src/HOL/Cardinals/Wellorder_Embedding_FP.thy
 author blanchet Thu Jan 16 16:33:19 2014 +0100 (2014-01-16) changeset 55018 2a526bd279ed parent 54482 a2874c8b3558 child 55020 96b05fd2aee4 permissions -rw-r--r--
moved 'Zorn' into 'Main', since it's a BNF dependency
     1 (*  Title:      HOL/Cardinals/Wellorder_Embedding_FP.thy

     2     Author:     Andrei Popescu, TU Muenchen

     3     Copyright   2012

     4

     5 Well-order embeddings (FP).

     6 *)

     7

     8 header {* Well-Order Embeddings (FP) *}

     9

    10 theory Wellorder_Embedding_FP

    11 imports Zorn Fun_More_FP Wellorder_Relation_FP

    12 begin

    13

    14

    15 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and

    16 prove their basic properties.  The notion of embedding is considered from the point

    17 of view of the theory of ordinals, and therefore requires the source to be injected

    18 as an {\em initial segment} (i.e., {\em order filter}) of the target.  A main result

    19 of this section is the existence of embeddings (in one direction or another) between

    20 any two well-orders, having as a consequence the fact that, given any two sets on

    21 any two types, one is smaller than (i.e., can be injected into) the other. *}

    22

    23

    24 subsection {* Auxiliaries *}

    25

    26 lemma UNION_inj_on_ofilter:

    27 assumes WELL: "Well_order r" and

    28         OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and

    29        INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"

    30 shows "inj_on f (\<Union> i \<in> I. A i)"

    31 proof-

    32   have "wo_rel r" using WELL by (simp add: wo_rel_def)

    33   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"

    34   using wo_rel.ofilter_linord[of r] OF by blast

    35   with WELL INJ show ?thesis

    36   by (auto simp add: inj_on_UNION_chain)

    37 qed

    38

    39

    40 lemma under_underS_bij_betw:

    41 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

    42         IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and

    43         BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"

    44 shows "bij_betw f (rel.under r a) (rel.under r' (f a))"

    45 proof-

    46   have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"

    47   unfolding rel.underS_def by auto

    48   moreover

    49   {have "Refl r \<and> Refl r'" using WELL WELL'

    50    by (auto simp add: order_on_defs)

    51    hence "rel.under r a = rel.underS r a \<union> {a} \<and>

    52           rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"

    53    using IN IN' by(auto simp add: rel.Refl_under_underS)

    54   }

    55   ultimately show ?thesis

    56   using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.underS r' (f a)"] by auto

    57 qed

    58

    59

    60

    61 subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible

    62 functions  *}

    63

    64

    65 text{* Standardly, a function is an embedding of a well-order in another if it injectively and

    66 order-compatibly maps the former into an order filter of the latter.

    67 Here we opt for a more succinct definition (operator @{text "embed"}),

    68 asking that, for any element in the source, the function should be a bijection

    69 between the set of strict lower bounds of that element

    70 and the set of strict lower bounds of its image.  (Later we prove equivalence with

    71 the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)

    72 A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding

    73 and an isomorphism (operator @{text "iso"}) is a bijective embedding.   *}

    74

    75

    76 definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"

    77 where

    78 "embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"

    79

    80

    81 lemmas embed_defs = embed_def embed_def[abs_def]

    82

    83

    84 text {* Strict embeddings: *}

    85

    86 definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"

    87 where

    88 "embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"

    89

    90

    91 lemmas embedS_defs = embedS_def embedS_def[abs_def]

    92

    93

    94 definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"

    95 where

    96 "iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"

    97

    98

    99 lemmas iso_defs = iso_def iso_def[abs_def]

   100

   101

   102 definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"

   103 where

   104 "compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"

   105

   106

   107 lemma compat_wf:

   108 assumes CMP: "compat r r' f" and WF: "wf r'"

   109 shows "wf r"

   110 proof-

   111   have "r \<le> inv_image r' f"

   112   unfolding inv_image_def using CMP

   113   by (auto simp add: compat_def)

   114   with WF show ?thesis

   115   using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto

   116 qed

   117

   118

   119 lemma id_embed: "embed r r id"

   120 by(auto simp add: id_def embed_def bij_betw_def)

   121

   122

   123 lemma id_iso: "iso r r id"

   124 by(auto simp add: id_def embed_def iso_def bij_betw_def)

   125

   126

   127 lemma embed_in_Field:

   128 assumes WELL: "Well_order r" and

   129         EMB: "embed r r' f" and IN: "a \<in> Field r"

   130 shows "f a \<in> Field r'"

   131 proof-

   132   have Well: "wo_rel r"

   133   using WELL by (auto simp add: wo_rel_def)

   134   hence 1: "Refl r"

   135   by (auto simp add: wo_rel.REFL)

   136   hence "a \<in> rel.under r a" using IN rel.Refl_under_in by fastforce

   137   hence "f a \<in> rel.under r' (f a)"

   138   using EMB IN by (auto simp add: embed_def bij_betw_def)

   139   thus ?thesis unfolding Field_def

   140   by (auto simp: rel.under_def)

   141 qed

   142

   143

   144 lemma comp_embed:

   145 assumes WELL: "Well_order r" and

   146         EMB: "embed r r' f" and EMB': "embed r' r'' f'"

   147 shows "embed r r'' (f' o f)"

   148 proof(unfold embed_def, auto)

   149   fix a assume *: "a \<in> Field r"

   150   hence "bij_betw f (rel.under r a) (rel.under r' (f a))"

   151   using embed_def[of r] EMB by auto

   152   moreover

   153   {have "f a \<in> Field r'"

   154    using EMB WELL * by (auto simp add: embed_in_Field)

   155    hence "bij_betw f' (rel.under r' (f a)) (rel.under r'' (f' (f a)))"

   156    using embed_def[of r'] EMB' by auto

   157   }

   158   ultimately

   159   show "bij_betw (f' \<circ> f) (rel.under r a) (rel.under r'' (f'(f a)))"

   160   by(auto simp add: bij_betw_trans)

   161 qed

   162

   163

   164 lemma comp_iso:

   165 assumes WELL: "Well_order r" and

   166         EMB: "iso r r' f" and EMB': "iso r' r'' f'"

   167 shows "iso r r'' (f' o f)"

   168 using assms unfolding iso_def

   169 by (auto simp add: comp_embed bij_betw_trans)

   170

   171

   172 text{* That @{text "embedS"} is also preserved by function composition shall be proved only later.  *}

   173

   174

   175 lemma embed_Field:

   176 "\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f(Field r) \<le> Field r'"

   177 by (auto simp add: embed_in_Field)

   178

   179

   180 lemma embed_preserves_ofilter:

   181 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   182         EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"

   183 shows "wo_rel.ofilter r' (fA)"

   184 proof-

   185   (* Preliminary facts *)

   186   from WELL have Well: "wo_rel r" unfolding wo_rel_def .

   187   from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .

   188   from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def)

   189   (* Main proof *)

   190   show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]

   191   proof(unfold wo_rel.ofilter_def, auto simp add: image_def)

   192     fix a b'

   193     assume *: "a \<in> A" and **: "b' \<in> rel.under r' (f a)"

   194     hence "a \<in> Field r" using 0 by auto

   195     hence "bij_betw f (rel.under r a) (rel.under r' (f a))"

   196     using * EMB by (auto simp add: embed_def)

   197     hence "f(rel.under r a) = rel.under r' (f a)"

   198     by (simp add: bij_betw_def)

   199     with ** image_def[of f "rel.under r a"] obtain b where

   200     1: "b \<in> rel.under r a \<and> b' = f b" by blast

   201     hence "b \<in> A" using Well * OF

   202     by (auto simp add: wo_rel.ofilter_def)

   203     with 1 show "\<exists>b \<in> A. b' = f b" by blast

   204   qed

   205 qed

   206

   207

   208 lemma embed_Field_ofilter:

   209 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   210         EMB: "embed r r' f"

   211 shows "wo_rel.ofilter r' (f(Field r))"

   212 proof-

   213   have "wo_rel.ofilter r (Field r)"

   214   using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)

   215   with WELL WELL' EMB

   216   show ?thesis by (auto simp add: embed_preserves_ofilter)

   217 qed

   218

   219

   220 lemma embed_compat:

   221 assumes EMB: "embed r r' f"

   222 shows "compat r r' f"

   223 proof(unfold compat_def, clarify)

   224   fix a b

   225   assume *: "(a,b) \<in> r"

   226   hence 1: "b \<in> Field r" using Field_def[of r] by blast

   227   have "a \<in> rel.under r b"

   228   using * rel.under_def[of r] by simp

   229   hence "f a \<in> rel.under r' (f b)"

   230   using EMB embed_def[of r r' f]

   231         bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"]

   232         image_def[of f "rel.under r b"] 1 by auto

   233   thus "(f a, f b) \<in> r'"

   234   by (auto simp add: rel.under_def)

   235 qed

   236

   237

   238 lemma embed_inj_on:

   239 assumes WELL: "Well_order r" and EMB: "embed r r' f"

   240 shows "inj_on f (Field r)"

   241 proof(unfold inj_on_def, clarify)

   242   (* Preliminary facts *)

   243   from WELL have Well: "wo_rel r" unfolding wo_rel_def .

   244   with wo_rel.TOTAL[of r]

   245   have Total: "Total r" by simp

   246   from Well wo_rel.REFL[of r]

   247   have Refl: "Refl r" by simp

   248   (* Main proof *)

   249   fix a b

   250   assume *: "a \<in> Field r" and **: "b \<in> Field r" and

   251          ***: "f a = f b"

   252   hence 1: "a \<in> Field r \<and> b \<in> Field r"

   253   unfolding Field_def by auto

   254   {assume "(a,b) \<in> r"

   255    hence "a \<in> rel.under r b \<and> b \<in> rel.under r b"

   256    using Refl by(auto simp add: rel.under_def refl_on_def)

   257    hence "a = b"

   258    using EMB 1 ***

   259    by (auto simp add: embed_def bij_betw_def inj_on_def)

   260   }

   261   moreover

   262   {assume "(b,a) \<in> r"

   263    hence "a \<in> rel.under r a \<and> b \<in> rel.under r a"

   264    using Refl by(auto simp add: rel.under_def refl_on_def)

   265    hence "a = b"

   266    using EMB 1 ***

   267    by (auto simp add: embed_def bij_betw_def inj_on_def)

   268   }

   269   ultimately

   270   show "a = b" using Total 1

   271   by (auto simp add: total_on_def)

   272 qed

   273

   274

   275 lemma embed_underS:

   276 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   277         EMB: "embed r r' f" and IN: "a \<in> Field r"

   278 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"

   279 proof-

   280   have "bij_betw f (rel.under r a) (rel.under r' (f a))"

   281   using assms by (auto simp add: embed_def)

   282   moreover

   283   {have "f a \<in> Field r'" using assms  embed_Field[of r r' f] by auto

   284    hence "rel.under r a = rel.underS r a \<union> {a} \<and>

   285           rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"

   286    using assms by (auto simp add: order_on_defs rel.Refl_under_underS)

   287   }

   288   moreover

   289   {have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"

   290    unfolding rel.underS_def by blast

   291   }

   292   ultimately show ?thesis

   293   by (auto simp add: notIn_Un_bij_betw3)

   294 qed

   295

   296

   297 lemma embed_iff_compat_inj_on_ofilter:

   298 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   299 shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f(Field r)))"

   300 using assms

   301 proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,

   302       unfold embed_def, auto) (* get rid of one implication *)

   303   fix a

   304   assume *: "inj_on f (Field r)" and

   305          **: "compat r r' f" and

   306          ***: "wo_rel.ofilter r' (f(Field r))" and

   307          ****: "a \<in> Field r"

   308   (* Preliminary facts *)

   309   have Well: "wo_rel r"

   310   using WELL wo_rel_def[of r] by simp

   311   hence Refl: "Refl r"

   312   using wo_rel.REFL[of r] by simp

   313   have Total: "Total r"

   314   using Well wo_rel.TOTAL[of r] by simp

   315   have Well': "wo_rel r'"

   316   using WELL' wo_rel_def[of r'] by simp

   317   hence Antisym': "antisym r'"

   318   using wo_rel.ANTISYM[of r'] by simp

   319   have "(a,a) \<in> r"

   320   using **** Well wo_rel.REFL[of r]

   321         refl_on_def[of _ r] by auto

   322   hence "(f a, f a) \<in> r'"

   323   using ** by(auto simp add: compat_def)

   324   hence 0: "f a \<in> Field r'"

   325   unfolding Field_def by auto

   326   have "f a \<in> f(Field r)"

   327   using **** by auto

   328   hence 2: "rel.under r' (f a) \<le> f(Field r)"

   329   using Well' *** wo_rel.ofilter_def[of r' "f(Field r)"] by fastforce

   330   (* Main proof *)

   331   show "bij_betw f (rel.under r a) (rel.under r' (f a))"

   332   proof(unfold bij_betw_def, auto)

   333     show  "inj_on f (rel.under r a)"

   334     using * by (metis (no_types) rel.under_Field subset_inj_on)

   335   next

   336     fix b assume "b \<in> rel.under r a"

   337     thus "f b \<in> rel.under r' (f a)"

   338     unfolding rel.under_def using **

   339     by (auto simp add: compat_def)

   340   next

   341     fix b' assume *****: "b' \<in> rel.under r' (f a)"

   342     hence "b' \<in> f(Field r)"

   343     using 2 by auto

   344     with Field_def[of r] obtain b where

   345     3: "b \<in> Field r" and 4: "b' = f b" by auto

   346     have "(b,a): r"

   347     proof-

   348       {assume "(a,b) \<in> r"

   349        with ** 4 have "(f a, b'): r'"

   350        by (auto simp add: compat_def)

   351        with ***** Antisym' have "f a = b'"

   352        by(auto simp add: rel.under_def antisym_def)

   353        with 3 **** 4 * have "a = b"

   354        by(auto simp add: inj_on_def)

   355       }

   356       moreover

   357       {assume "a = b"

   358        hence "(b,a) \<in> r" using Refl **** 3

   359        by (auto simp add: refl_on_def)

   360       }

   361       ultimately

   362       show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)

   363     qed

   364     with 4 show  "b' \<in> f(rel.under r a)"

   365     unfolding rel.under_def by auto

   366   qed

   367 qed

   368

   369

   370 lemma inv_into_ofilter_embed:

   371 assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and

   372         BIJ: "\<forall>b \<in> A. bij_betw f (rel.under r b) (rel.under r' (f b))" and

   373         IMAGE: "f  A = Field r'"

   374 shows "embed r' r (inv_into A f)"

   375 proof-

   376   (* Preliminary facts *)

   377   have Well: "wo_rel r"

   378   using WELL wo_rel_def[of r] by simp

   379   have Refl: "Refl r"

   380   using Well wo_rel.REFL[of r] by simp

   381   have Total: "Total r"

   382   using Well wo_rel.TOTAL[of r] by simp

   383   (* Main proof *)

   384   have 1: "bij_betw f A (Field r')"

   385   proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)

   386     fix b1 b2

   387     assume *: "b1 \<in> A" and **: "b2 \<in> A" and

   388            ***: "f b1 = f b2"

   389     have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"

   390     using * ** Well OF by (auto simp add: wo_rel.ofilter_def)

   391     moreover

   392     {assume "(b1,b2) \<in> r"

   393      hence "b1 \<in> rel.under r b2 \<and> b2 \<in> rel.under r b2"

   394      unfolding rel.under_def using 11 Refl

   395      by (auto simp add: refl_on_def)

   396      hence "b1 = b2" using BIJ * ** ***

   397      by (simp add: bij_betw_def inj_on_def)

   398     }

   399     moreover

   400      {assume "(b2,b1) \<in> r"

   401      hence "b1 \<in> rel.under r b1 \<and> b2 \<in> rel.under r b1"

   402      unfolding rel.under_def using 11 Refl

   403      by (auto simp add: refl_on_def)

   404      hence "b1 = b2" using BIJ * ** ***

   405      by (simp add: bij_betw_def inj_on_def)

   406     }

   407     ultimately

   408     show "b1 = b2"

   409     using Total by (auto simp add: total_on_def)

   410   qed

   411   (*  *)

   412   let ?f' = "(inv_into A f)"

   413   (*  *)

   414   have 2: "\<forall>b \<in> A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"

   415   proof(clarify)

   416     fix b assume *: "b \<in> A"

   417     hence "rel.under r b \<le> A"

   418     using Well OF by(auto simp add: wo_rel.ofilter_def)

   419     moreover

   420     have "f  (rel.under r b) = rel.under r' (f b)"

   421     using * BIJ by (auto simp add: bij_betw_def)

   422     ultimately

   423     show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"

   424     using 1 by (auto simp add: bij_betw_inv_into_subset)

   425   qed

   426   (*  *)

   427   have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"

   428   proof(clarify)

   429     fix b' assume *: "b' \<in> Field r'"

   430     have "b' = f (?f' b')" using * 1

   431     by (auto simp add: bij_betw_inv_into_right)

   432     moreover

   433     {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force

   434      hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)

   435      with 31 have "?f' b' \<in> A" by auto

   436     }

   437     ultimately

   438     show  "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"

   439     using 2 by auto

   440   qed

   441   (*  *)

   442   thus ?thesis unfolding embed_def .

   443 qed

   444

   445

   446 lemma inv_into_underS_embed:

   447 assumes WELL: "Well_order r" and

   448         BIJ: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and

   449         IN: "a \<in> Field r" and

   450         IMAGE: "f  (rel.underS r a) = Field r'"

   451 shows "embed r' r (inv_into (rel.underS r a) f)"

   452 using assms

   453 by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)

   454

   455

   456 lemma inv_into_Field_embed:

   457 assumes WELL: "Well_order r" and EMB: "embed r r' f" and

   458         IMAGE: "Field r' \<le> f  (Field r)"

   459 shows "embed r' r (inv_into (Field r) f)"

   460 proof-

   461   have "(\<forall>b \<in> Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))"

   462   using EMB by (auto simp add: embed_def)

   463   moreover

   464   have "f  (Field r) \<le> Field r'"

   465   using EMB WELL by (auto simp add: embed_Field)

   466   ultimately

   467   show ?thesis using assms

   468   by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)

   469 qed

   470

   471

   472 lemma inv_into_Field_embed_bij_betw:

   473 assumes WELL: "Well_order r" and

   474         EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"

   475 shows "embed r' r (inv_into (Field r) f)"

   476 proof-

   477   have "Field r' \<le> f  (Field r)"

   478   using BIJ by (auto simp add: bij_betw_def)

   479   thus ?thesis using assms

   480   by(auto simp add: inv_into_Field_embed)

   481 qed

   482

   483

   484

   485

   486

   487 subsection {* Given any two well-orders, one can be embedded in the other *}

   488

   489

   490 text{* Here is an overview of the proof of of this fact, stated in theorem

   491 @{text "wellorders_totally_ordered"}:

   492

   493    Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}.

   494    Attempt to define an embedding @{text "f::'a \<Rightarrow> 'a'"} from @{text "r"} to @{text "r'"} in the

   495    natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller

   496    than @{text "Field r'"}), but also record, at the recursive step, in a function

   497    @{text "g::'a \<Rightarrow> bool"}, the extra information of whether @{text "Field r'"}

   498    gets exhausted or not.

   499

   500    If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller

   501    and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"}

   502    (lemma @{text "wellorders_totally_ordered_aux"}).

   503

   504    Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of

   505    (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"}

   506    (lemma @{text "wellorders_totally_ordered_aux2"}).

   507 *}

   508

   509

   510 lemma wellorders_totally_ordered_aux:

   511 fixes r ::"'a rel"  and r'::"'a' rel" and

   512       f :: "'a \<Rightarrow> 'a'" and a::'a

   513 assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and

   514         IH: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and

   515         NOT: "f  (rel.underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f(rel.underS r a))"

   516 shows "bij_betw f (rel.under r a) (rel.under r' (f a))"

   517 proof-

   518   (* Preliminary facts *)

   519   have Well: "wo_rel r" using WELL unfolding wo_rel_def .

   520   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto

   521   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto

   522   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .

   523   have OF: "wo_rel.ofilter r (rel.underS r a)"

   524   by (auto simp add: Well wo_rel.underS_ofilter)

   525   hence UN: "rel.underS r a = (\<Union>  b \<in> rel.underS r a. rel.under r b)"

   526   using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast

   527   (* Gather facts about elements of rel.underS r a *)

   528   {fix b assume *: "b \<in> rel.underS r a"

   529    hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto

   530    have t1: "b \<in> Field r"

   531    using * rel.underS_Field[of r a] by auto

   532    have t2: "f(rel.under r b) = rel.under r' (f b)"

   533    using IH * by (auto simp add: bij_betw_def)

   534    hence t3: "wo_rel.ofilter r' (f(rel.under r b))"

   535    using Well' by (auto simp add: wo_rel.under_ofilter)

   536    have "f(rel.under r b) \<le> Field r'"

   537    using t2 by (auto simp add: rel.under_Field)

   538    moreover

   539    have "b \<in> rel.under r b"

   540    using t1 by(auto simp add: Refl rel.Refl_under_in)

   541    ultimately

   542    have t4:  "f b \<in> Field r'" by auto

   543    have "f(rel.under r b) = rel.under r' (f b) \<and>

   544          wo_rel.ofilter r' (f(rel.under r b)) \<and>

   545          f b \<in> Field r'"

   546    using t2 t3 t4 by auto

   547   }

   548   hence bFact:

   549   "\<forall>b \<in> rel.underS r a. f(rel.under r b) = rel.under r' (f b) \<and>

   550                        wo_rel.ofilter r' (f(rel.under r b)) \<and>

   551                        f b \<in> Field r'" by blast

   552   (*  *)

   553   have subField: "f(rel.underS r a) \<le> Field r'"

   554   using bFact by blast

   555   (*  *)

   556   have OF': "wo_rel.ofilter r' (f(rel.underS r a))"

   557   proof-

   558     have "f(rel.underS r a) = f(\<Union>  b \<in> rel.underS r a. rel.under r b)"

   559     using UN by auto

   560     also have "\<dots> = (\<Union>  b \<in> rel.underS r a. f(rel.under r b))" by blast

   561     also have "\<dots> = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))"

   562     using bFact by auto

   563     finally

   564     have "f(rel.underS r a) = (\<Union>  b \<in> rel.underS r a. (rel.under r' (f b)))" .

   565     thus ?thesis

   566     using Well' bFact

   567           wo_rel.ofilter_UNION[of r' "rel.underS r a" "\<lambda> b. rel.under r' (f b)"] by fastforce

   568   qed

   569   (*  *)

   570   have "f(rel.underS r a) \<union> rel.AboveS r' (f(rel.underS r a)) = Field r'"

   571   using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)

   572   hence NE: "rel.AboveS r' (f(rel.underS r a)) \<noteq> {}"

   573   using subField NOT by blast

   574   (* Main proof *)

   575   have INCL1: "f(rel.underS r a) \<le> rel.underS r' (f a) "

   576   proof(auto)

   577     fix b assume *: "b \<in> rel.underS r a"

   578     have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"

   579     using subField Well' SUC NE *

   580           wo_rel.suc_greater[of r' "f(rel.underS r a)" "f b"] by force

   581     thus "f b \<in> rel.underS r' (f a)"

   582     unfolding rel.underS_def by simp

   583   qed

   584   (*  *)

   585   have INCL2: "rel.underS r' (f a) \<le> f(rel.underS r a)"

   586   proof

   587     fix b' assume "b' \<in> rel.underS r' (f a)"

   588     hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"

   589     unfolding rel.underS_def by simp

   590     thus "b' \<in> f(rel.underS r a)"

   591     using Well' SUC NE OF'

   592           wo_rel.suc_ofilter_in[of r' "f  rel.underS r a" b'] by auto

   593   qed

   594   (*  *)

   595   have INJ: "inj_on f (rel.underS r a)"

   596   proof-

   597     have "\<forall>b \<in> rel.underS r a. inj_on f (rel.under r b)"

   598     using IH by (auto simp add: bij_betw_def)

   599     moreover

   600     have "\<forall>b. wo_rel.ofilter r (rel.under r b)"

   601     using Well by (auto simp add: wo_rel.under_ofilter)

   602     ultimately show  ?thesis

   603     using WELL bFact UN

   604           UNION_inj_on_ofilter[of r "rel.underS r a" "\<lambda>b. rel.under r b" f]

   605     by auto

   606   qed

   607   (*  *)

   608   have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"

   609   unfolding bij_betw_def

   610   using INJ INCL1 INCL2 by auto

   611   (*  *)

   612   have "f a \<in> Field r'"

   613   using Well' subField NE SUC

   614   by (auto simp add: wo_rel.suc_inField)

   615   thus ?thesis

   616   using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto

   617 qed

   618

   619

   620 lemma wellorders_totally_ordered_aux2:

   621 fixes r ::"'a rel"  and r'::"'a' rel" and

   622       f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a

   623 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   624 MAIN1:

   625   "\<And> a. (False \<notin> g(rel.underS r a) \<and> f(rel.underS r a) \<noteq> Field r'

   626           \<longrightarrow> f a = wo_rel.suc r' (f(rel.underS r a)) \<and> g a = True)

   627          \<and>

   628          (\<not>(False \<notin> (g(rel.underS r a)) \<and> f(rel.underS r a) \<noteq> Field r')

   629           \<longrightarrow> g a = False)" and

   630 MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g(rel.under r a) \<longrightarrow>

   631               bij_betw f (rel.under r a) (rel.under r' (f a))" and

   632 Case: "a \<in> Field r \<and> False \<in> g(rel.under r a)"

   633 shows "\<exists>f'. embed r' r f'"

   634 proof-

   635   have Well: "wo_rel r" using WELL unfolding wo_rel_def .

   636   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto

   637   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto

   638   have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto

   639   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .

   640   (*  *)

   641   have 0: "rel.under r a = rel.underS r a \<union> {a}"

   642   using Refl Case by(auto simp add: rel.Refl_under_underS)

   643   (*  *)

   644   have 1: "g a = False"

   645   proof-

   646     {assume "g a \<noteq> False"

   647      with 0 Case have "False \<in> g(rel.underS r a)" by blast

   648      with MAIN1 have "g a = False" by blast}

   649     thus ?thesis by blast

   650   qed

   651   let ?A = "{a \<in> Field r. g a = False}"

   652   let ?a = "(wo_rel.minim r ?A)"

   653   (*  *)

   654   have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast

   655   (*  *)

   656   have 3: "False \<notin> g(rel.underS r ?a)"

   657   proof

   658     assume "False \<in> g(rel.underS r ?a)"

   659     then obtain b where "b \<in> rel.underS r ?a" and 31: "g b = False" by auto

   660     hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"

   661     by (auto simp add: rel.underS_def)

   662     hence "b \<in> Field r" unfolding Field_def by auto

   663     with 31 have "b \<in> ?A" by auto

   664     hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce

   665     (* again: why worked without type annotations? *)

   666     with 32 Antisym show False

   667     by (auto simp add: antisym_def)

   668   qed

   669   have temp: "?a \<in> ?A"

   670   using Well 2 wo_rel.minim_in[of r ?A] by auto

   671   hence 4: "?a \<in> Field r" by auto

   672   (*   *)

   673   have 5: "g ?a = False" using temp by blast

   674   (*  *)

   675   have 6: "f(rel.underS r ?a) = Field r'"

   676   using MAIN1[of ?a] 3 5 by blast

   677   (*  *)

   678   have 7: "\<forall>b \<in> rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))"

   679   proof

   680     fix b assume as: "b \<in> rel.underS r ?a"

   681     moreover

   682     have "wo_rel.ofilter r (rel.underS r ?a)"

   683     using Well by (auto simp add: wo_rel.underS_ofilter)

   684     ultimately

   685     have "False \<notin> g(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+

   686     moreover have "b \<in> Field r"

   687     unfolding Field_def using as by (auto simp add: rel.underS_def)

   688     ultimately

   689     show "bij_betw f (rel.under r b) (rel.under r' (f b))"

   690     using MAIN2 by auto

   691   qed

   692   (*  *)

   693   have "embed r' r (inv_into (rel.underS r ?a) f)"

   694   using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto

   695   thus ?thesis

   696   unfolding embed_def by blast

   697 qed

   698

   699

   700 theorem wellorders_totally_ordered:

   701 fixes r ::"'a rel"  and r'::"'a' rel"

   702 assumes WELL: "Well_order r" and WELL': "Well_order r'"

   703 shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"

   704 proof-

   705   (* Preliminary facts *)

   706   have Well: "wo_rel r" using WELL unfolding wo_rel_def .

   707   hence Refl: "Refl r" using wo_rel.REFL[of r] by auto

   708   have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto

   709   have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .

   710   (* Main proof *)

   711   obtain H where H_def: "H =

   712   (\<lambda>h a. if False \<notin> (snd o h)(rel.underS r a) \<and> (fst o h)(rel.underS r a) \<noteq> Field r'

   713                 then (wo_rel.suc r' ((fst o h)(rel.underS r a)), True)

   714                 else (undefined, False))" by blast

   715   have Adm: "wo_rel.adm_wo r H"

   716   using Well

   717   proof(unfold wo_rel.adm_wo_def, clarify)

   718     fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x

   719     assume "\<forall>y\<in>rel.underS r x. h1 y = h2 y"

   720     hence "\<forall>y\<in>rel.underS r x. (fst o h1) y = (fst o h2) y \<and>

   721                           (snd o h1) y = (snd o h2) y" by auto

   722     hence "(fst o h1)(rel.underS r x) = (fst o h2)(rel.underS r x) \<and>

   723            (snd o h1)(rel.underS r x) = (snd o h2)(rel.underS r x)"

   724       by (auto simp add: image_def)

   725     thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)

   726   qed

   727   (* More constant definitions:  *)

   728   obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"

   729   where h_def: "h = wo_rel.worec r H" and

   730         f_def: "f = fst o h" and g_def: "g = snd o h" by blast

   731   obtain test where test_def:

   732   "test = (\<lambda> a. False \<notin> (g(rel.underS r a)) \<and> f(rel.underS r a) \<noteq> Field r')" by blast

   733   (*  *)

   734   have *: "\<And> a. h a  = H h a"

   735   using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)

   736   have Main1:

   737   "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f(rel.underS r a)) \<and> g a = True) \<and>

   738          (\<not>(test a) \<longrightarrow> g a = False)"

   739   proof-  (* How can I prove this withou fixing a? *)

   740     fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f(rel.underS r a)) \<and> g a = True) \<and>

   741                 (\<not>(test a) \<longrightarrow> g a = False)"

   742     using *[of a] test_def f_def g_def H_def by auto

   743   qed

   744   (*  *)

   745   let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g(rel.under r a) \<longrightarrow>

   746                    bij_betw f (rel.under r a) (rel.under r' (f a))"

   747   have Main2: "\<And> a. ?phi a"

   748   proof-

   749     fix a show "?phi a"

   750     proof(rule wo_rel.well_order_induct[of r ?phi],

   751           simp only: Well, clarify)

   752       fix a

   753       assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and

   754              *: "a \<in> Field r" and

   755              **: "False \<notin> g(rel.under r a)"

   756       have 1: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))"

   757       proof(clarify)

   758         fix b assume ***: "b \<in> rel.underS r a"

   759         hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto

   760         moreover have "b \<in> Field r"

   761         using *** rel.underS_Field[of r a] by auto

   762         moreover have "False \<notin> g(rel.under r b)"

   763         using 0 ** Trans rel.under_incr[of r b a] by auto

   764         ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))"

   765         using IH by auto

   766       qed

   767       (*  *)

   768       have 21: "False \<notin> g(rel.underS r a)"

   769       using ** rel.underS_subset_under[of r a] by auto

   770       have 22: "g(rel.under r a) \<le> {True}" using ** by auto

   771       moreover have 23: "a \<in> rel.under r a"

   772       using Refl * by (auto simp add: rel.Refl_under_in)

   773       ultimately have 24: "g a = True" by blast

   774       have 2: "f(rel.underS r a) \<noteq> Field r'"

   775       proof

   776         assume "f(rel.underS r a) = Field r'"

   777         hence "g a = False" using Main1 test_def by blast

   778         with 24 show False using ** by blast

   779       qed

   780       (*  *)

   781       have 3: "f a = wo_rel.suc r' (f(rel.underS r a))"

   782       using 21 2 Main1 test_def by blast

   783       (*  *)

   784       show "bij_betw f (rel.under r a) (rel.under r' (f a))"

   785       using WELL  WELL' 1 2 3 *

   786             wellorders_totally_ordered_aux[of r r' a f] by auto

   787     qed

   788   qed

   789   (*  *)

   790   let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g(rel.under r a))"

   791   show ?thesis

   792   proof(cases "\<exists>a. ?chi a")

   793     assume "\<not> (\<exists>a. ?chi a)"

   794     hence "\<forall>a \<in> Field r.  bij_betw f (rel.under r a) (rel.under r' (f a))"

   795     using Main2 by blast

   796     thus ?thesis unfolding embed_def by blast

   797   next

   798     assume "\<exists>a. ?chi a"

   799     then obtain a where "?chi a" by blast

   800     hence "\<exists>f'. embed r' r f'"

   801     using wellorders_totally_ordered_aux2[of r r' g f a]

   802           WELL WELL' Main1 Main2 test_def by fast

   803     thus ?thesis by blast

   804   qed

   805 qed

   806

   807

   808 subsection {* Uniqueness of embeddings  *}

   809

   810

   811 text{* Here we show a fact complementary to the one from the previous subsection -- namely,

   812 that between any two well-orders there is {\em at most} one embedding, and is the one

   813 definable by the expected well-order recursive equation.  As a consequence, any two

   814 embeddings of opposite directions are mutually inverse. *}

   815

   816

   817 lemma embed_determined:

   818 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   819         EMB: "embed r r' f" and IN: "a \<in> Field r"

   820 shows "f a = wo_rel.suc r' (f(rel.underS r a))"

   821 proof-

   822   have "bij_betw f (rel.underS r a) (rel.underS r' (f a))"

   823   using assms by (auto simp add: embed_underS)

   824   hence "f(rel.underS r a) = rel.underS r' (f a)"

   825   by (auto simp add: bij_betw_def)

   826   moreover

   827   {have "f a \<in> Field r'" using IN

   828    using EMB WELL embed_Field[of r r' f] by auto

   829    hence "f a = wo_rel.suc r' (rel.underS r' (f a))"

   830    using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)

   831   }

   832   ultimately show ?thesis by simp

   833 qed

   834

   835

   836 lemma embed_unique:

   837 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   838         EMBf: "embed r r' f" and EMBg: "embed r r' g"

   839 shows "a \<in> Field r \<longrightarrow> f a = g a"

   840 proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)

   841   fix a

   842   assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and

   843          *: "a \<in> Field r"

   844   hence "\<forall>b \<in> rel.underS r a. f b = g b"

   845   unfolding rel.underS_def by (auto simp add: Field_def)

   846   hence "f(rel.underS r a) = g(rel.underS r a)" by force

   847   thus "f a = g a"

   848   using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto

   849 qed

   850

   851

   852 lemma embed_bothWays_inverse:

   853 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   854         EMB: "embed r r' f" and EMB': "embed r' r f'"

   855 shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"

   856 proof-

   857   have "embed r r (f' o f)" using assms

   858   by(auto simp add: comp_embed)

   859   moreover have "embed r r id" using assms

   860   by (auto simp add: id_embed)

   861   ultimately have "\<forall>a \<in> Field r. f'(f a) = a"

   862   using assms embed_unique[of r r "f' o f" id] id_def by auto

   863   moreover

   864   {have "embed r' r' (f o f')" using assms

   865    by(auto simp add: comp_embed)

   866    moreover have "embed r' r' id" using assms

   867    by (auto simp add: id_embed)

   868    ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"

   869    using assms embed_unique[of r' r' "f o f'" id] id_def by auto

   870   }

   871   ultimately show ?thesis by blast

   872 qed

   873

   874

   875 lemma embed_bothWays_bij_betw:

   876 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   877         EMB: "embed r r' f" and EMB': "embed r' r g"

   878 shows "bij_betw f (Field r) (Field r')"

   879 proof-

   880   let ?A = "Field r"  let ?A' = "Field r'"

   881   have "embed r r (g o f) \<and> embed r' r' (f o g)"

   882   using assms by (auto simp add: comp_embed)

   883   hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"

   884   using WELL id_embed[of r] embed_unique[of r r "g o f" id]

   885         WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id]

   886         id_def by auto

   887   have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"

   888   using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast

   889   (*  *)

   890   show ?thesis

   891   proof(unfold bij_betw_def inj_on_def, auto simp add: 2)

   892     fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"

   893     have "a = g(f a) \<and> b = g(f b)" using * 1 by auto

   894     with ** show "a = b" by auto

   895   next

   896     fix a' assume *: "a' \<in> ?A'"

   897     hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto

   898     thus "a' \<in> f  ?A" by force

   899   qed

   900 qed

   901

   902

   903 lemma embed_bothWays_iso:

   904 assumes WELL: "Well_order r"  and WELL': "Well_order r'" and

   905         EMB: "embed r r' f" and EMB': "embed r' r g"

   906 shows "iso r r' f"

   907 unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)

   908

   909

   910 subsection {* More properties of embeddings, strict embeddings and isomorphisms  *}

   911

   912

   913 lemma embed_bothWays_Field_bij_betw:

   914 assumes WELL: "Well_order r" and WELL': "Well_order r'" and

   915         EMB: "embed r r' f" and EMB': "embed r' r f'"

   916 shows "bij_betw f (Field r) (Field r')"

   917 proof-

   918   have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"

   919   using assms by (auto simp add: embed_bothWays_inverse)

   920   moreover

   921   have "f(Field r) \<le> Field r' \<and> f'  (Field r') \<le> Field r"

   922   using assms by (auto simp add: embed_Field)

   923   ultimately

   924   show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto

   925 qed

   926

   927

   928 lemma embedS_comp_embed:

   929 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

   930         and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"

   931 shows "embedS r r'' (f' o f)"

   932 proof-

   933   let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"

   934   have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))"

   935   using EMB by (auto simp add: embedS_def)

   936   hence 2: "embed r r'' ?g"

   937   using WELL EMB' comp_embed[of r r' f r'' f'] by auto

   938   moreover

   939   {assume "bij_betw ?g (Field r) (Field r'')"

   940    hence "embed r'' r ?h" using 2 WELL

   941    by (auto simp add: inv_into_Field_embed_bij_betw)

   942    hence "embed r' r (?h o f')" using WELL' EMB'

   943    by (auto simp add: comp_embed)

   944    hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1

   945    by (auto simp add: embed_bothWays_Field_bij_betw)

   946    with 1 have False by blast

   947   }

   948   ultimately show ?thesis unfolding embedS_def by auto

   949 qed

   950

   951

   952 lemma embed_comp_embedS:

   953 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

   954         and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"

   955 shows "embedS r r'' (f' o f)"

   956 proof-

   957   let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"

   958   have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))"

   959   using EMB' by (auto simp add: embedS_def)

   960   hence 2: "embed r r'' ?g"

   961   using WELL EMB comp_embed[of r r' f r'' f'] by auto

   962   moreover

   963   {assume "bij_betw ?g (Field r) (Field r'')"

   964    hence "embed r'' r ?h" using 2 WELL

   965    by (auto simp add: inv_into_Field_embed_bij_betw)

   966    hence "embed r'' r' (f o ?h)" using WELL'' EMB

   967    by (auto simp add: comp_embed)

   968    hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1

   969    by (auto simp add: embed_bothWays_Field_bij_betw)

   970    with 1 have False by blast

   971   }

   972   ultimately show ?thesis unfolding embedS_def by auto

   973 qed

   974

   975

   976 lemma embed_comp_iso:

   977 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

   978         and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"

   979 shows "embed r r'' (f' o f)"

   980 using assms unfolding iso_def

   981 by (auto simp add: comp_embed)

   982

   983

   984 lemma iso_comp_embed:

   985 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

   986         and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"

   987 shows "embed r r'' (f' o f)"

   988 using assms unfolding iso_def

   989 by (auto simp add: comp_embed)

   990

   991

   992 lemma embedS_comp_iso:

   993 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

   994         and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"

   995 shows "embedS r r'' (f' o f)"

   996 using assms unfolding iso_def

   997 by (auto simp add: embedS_comp_embed)

   998

   999

  1000 lemma iso_comp_embedS:

  1001 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"

  1002         and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"

  1003 shows "embedS r r'' (f' o f)"

  1004 using assms unfolding iso_def  using embed_comp_embedS

  1005 by (auto simp add: embed_comp_embedS)

  1006

  1007

  1008 lemma embedS_Field:

  1009 assumes WELL: "Well_order r" and EMB: "embedS r r' f"

  1010 shows "f  (Field r) < Field r'"

  1011 proof-

  1012   have "f(Field r) \<le> Field r'" using assms

  1013   by (auto simp add: embed_Field embedS_def)

  1014   moreover

  1015   {have "inj_on f (Field r)" using assms

  1016    by (auto simp add: embedS_def embed_inj_on)

  1017    hence "f(Field r) \<noteq> Field r'" using EMB

  1018    by (auto simp add: embedS_def bij_betw_def)

  1019   }

  1020   ultimately show ?thesis by blast

  1021 qed

  1022

  1023

  1024 lemma embedS_iff:

  1025 assumes WELL: "Well_order r" and ISO: "embed r r' f"

  1026 shows "embedS r r' f = (f  (Field r) < Field r')"

  1027 proof

  1028   assume "embedS r r' f"

  1029   thus "f  Field r \<subset> Field r'"

  1030   using WELL by (auto simp add: embedS_Field)

  1031 next

  1032   assume "f  Field r \<subset> Field r'"

  1033   hence "\<not> bij_betw f (Field r) (Field r')"

  1034   unfolding bij_betw_def by blast

  1035   thus "embedS r r' f" unfolding embedS_def

  1036   using ISO by auto

  1037 qed

  1038

  1039

  1040 lemma iso_Field:

  1041 "iso r r' f \<Longrightarrow> f  (Field r) = Field r'"

  1042 using assms by (auto simp add: iso_def bij_betw_def)

  1043

  1044

  1045 lemma iso_iff:

  1046 assumes "Well_order r"

  1047 shows "iso r r' f = (embed r r' f \<and> f  (Field r) = Field r')"

  1048 proof

  1049   assume "iso r r' f"

  1050   thus "embed r r' f \<and> f  (Field r) = Field r'"

  1051   by (auto simp add: iso_Field iso_def)

  1052 next

  1053   assume *: "embed r r' f \<and> f  Field r = Field r'"

  1054   hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)

  1055   with * have "bij_betw f (Field r) (Field r')"

  1056   unfolding bij_betw_def by simp

  1057   with * show "iso r r' f" unfolding iso_def by auto

  1058 qed

  1059

  1060

  1061 lemma iso_iff2:

  1062 assumes "Well_order r"

  1063 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>

  1064                      (\<forall>a \<in> Field r. \<forall>b \<in> Field r.

  1065                          (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"

  1066 using assms

  1067 proof(auto simp add: iso_def)

  1068   fix a b

  1069   assume "embed r r' f"

  1070   hence "compat r r' f" using embed_compat[of r] by auto

  1071   moreover assume "(a,b) \<in> r"

  1072   ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto

  1073 next

  1074   let ?f' = "inv_into (Field r) f"

  1075   assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"

  1076   hence "embed r' r ?f'" using assms

  1077   by (auto simp add: inv_into_Field_embed_bij_betw)

  1078   hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto

  1079   fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"

  1080   hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1

  1081   by (auto simp add: bij_betw_inv_into_left)

  1082   thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce

  1083 next

  1084   assume *: "bij_betw f (Field r) (Field r')" and

  1085          **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"

  1086   have 1: "\<And> a. rel.under r a \<le> Field r \<and> rel.under r' (f a) \<le> Field r'"

  1087   by (auto simp add: rel.under_Field)

  1088   have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)

  1089   {fix a assume ***: "a \<in> Field r"

  1090    have "bij_betw f (rel.under r a) (rel.under r' (f a))"

  1091    proof(unfold bij_betw_def, auto)

  1092      show "inj_on f (rel.under r a)"

  1093      using 1 2 by (metis subset_inj_on)

  1094    next

  1095      fix b assume "b \<in> rel.under r a"

  1096      hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"

  1097      unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def)

  1098      with 1 ** show "f b \<in> rel.under r' (f a)"

  1099      unfolding rel.under_def by auto

  1100    next

  1101      fix b' assume "b' \<in> rel.under r' (f a)"

  1102      hence 3: "(b',f a) \<in> r'" unfolding rel.under_def by simp

  1103      hence "b' \<in> Field r'" unfolding Field_def by auto

  1104      with * obtain b where "b \<in> Field r \<and> f b = b'"

  1105      unfolding bij_betw_def by force

  1106      with 3 ** ***

  1107      show "b' \<in> f  (rel.under r a)" unfolding rel.under_def by blast

  1108    qed

  1109   }

  1110   thus "embed r r' f" unfolding embed_def using * by auto

  1111 qed

  1112

  1113

  1114 lemma iso_iff3:

  1115 assumes WELL: "Well_order r" and WELL': "Well_order r'"

  1116 shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"

  1117 proof

  1118   assume "iso r r' f"

  1119   thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"

  1120   unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)

  1121 next

  1122   have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'

  1123   by (auto simp add: wo_rel_def)

  1124   assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"

  1125   thus "iso r r' f"

  1126   unfolding "compat_def" using assms

  1127   proof(auto simp add: iso_iff2)

  1128     fix a b assume **: "a \<in> Field r" "b \<in> Field r" and

  1129                   ***: "(f a, f b) \<in> r'"

  1130     {assume "(b,a) \<in> r \<or> b = a"

  1131      hence "(b,a): r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast

  1132      hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto

  1133      hence "f a = f b"

  1134      using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast

  1135      hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto

  1136      hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast

  1137     }

  1138     thus "(a,b) \<in> r"

  1139     using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast

  1140   qed

  1141 qed

  1142

  1143

  1144

  1145 end