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