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