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