src/HOL/BNF_Wellorder_Embedding.thy
 author blanchet Wed Jan 22 09:45:30 2014 +0100 (2014-01-22) changeset 55101 57c875e488bd parent 55059 ef2e0fb783c6 child 55811 aa1acc25126b permissions -rw-r--r--
whitespace tuning
     1 (*  Title:      HOL/BNF_Wellorder_Embedding.thy

     2     Author:     Andrei Popescu, TU Muenchen

     3     Copyright   2012

     4

     5 Well-order embeddings as needed by bounded natural functors.

     6 *)

     7

     8 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *}

     9

    10 theory BNF_Wellorder_Embedding

    11 imports Zorn BNF_Wellorder_Relation

    12 begin

    13

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

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

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

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

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

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

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

    21

    22

    23 subsection {* Auxiliaries *}

    24

    25 lemma UNION_inj_on_ofilter:

    26 assumes WELL: "Well_order r" and

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

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

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

    30 proof-

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

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

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

    34   with WELL INJ show ?thesis

    35   by (auto simp add: inj_on_UNION_chain)

    36 qed

    37

    38 lemma under_underS_bij_betw:

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

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

    41         BIJ: "bij_betw f (underS r a) (underS r' (f a))"

    42 shows "bij_betw f (under r a) (under r' (f a))"

    43 proof-

    44   have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"

    45   unfolding underS_def by auto

    46   moreover

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

    48    by (auto simp add: order_on_defs)

    49    hence "under r a = underS r a \<union> {a} \<and>

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

    51    using IN IN' by(auto simp add: Refl_under_underS)

    52   }

    53   ultimately show ?thesis

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

    55 qed

    56

    57

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

    59 functions *}

    60

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

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

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

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

    65 between the set of strict lower bounds of that element

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

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

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

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

    70

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

    72 where

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

    74

    75 lemmas embed_defs = embed_def embed_def[abs_def]

    76

    77 text {* Strict embeddings: *}

    78

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

    80 where

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

    82

    83 lemmas embedS_defs = embedS_def embedS_def[abs_def]

    84

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

    86 where

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

    88

    89 lemmas iso_defs = iso_def iso_def[abs_def]

    90

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

    92 where

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

    94

    95 lemma compat_wf:

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

    97 shows "wf r"

    98 proof-

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

   100   unfolding inv_image_def using CMP

   101   by (auto simp add: compat_def)

   102   with WF show ?thesis

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

   104 qed

   105

   106 lemma id_embed: "embed r r id"

   107 by(auto simp add: id_def embed_def bij_betw_def)

   108

   109 lemma id_iso: "iso r r id"

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

   111

   112 lemma embed_in_Field:

   113 assumes WELL: "Well_order r" and

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

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

   116 proof-

   117   have Well: "wo_rel r"

   118   using WELL by (auto simp add: wo_rel_def)

   119   hence 1: "Refl r"

   120   by (auto simp add: wo_rel.REFL)

   121   hence "a \<in> under r a" using IN Refl_under_in by fastforce

   122   hence "f a \<in> under r' (f a)"

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

   124   thus ?thesis unfolding Field_def

   125   by (auto simp: under_def)

   126 qed

   127

   128 lemma comp_embed:

   129 assumes WELL: "Well_order r" and

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

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

   132 proof(unfold embed_def, auto)

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

   134   hence "bij_betw f (under r a) (under r' (f a))"

   135   using embed_def[of r] EMB by auto

   136   moreover

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

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

   139    hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"

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

   141   }

   142   ultimately

   143   show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"

   144   by(auto simp add: bij_betw_trans)

   145 qed

   146

   147 lemma comp_iso:

   148 assumes WELL: "Well_order r" and

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

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

   151 using assms unfolding iso_def

   152 by (auto simp add: comp_embed bij_betw_trans)

   153

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

   155

   156 lemma embed_Field:

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

   158 by (auto simp add: embed_in_Field)

   159

   160 lemma embed_preserves_ofilter:

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

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

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

   164 proof-

   165   (* Preliminary facts *)

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

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

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

   169   (* Main proof *)

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

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

   172     fix a b'

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

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

   175     hence "bij_betw f (under r a) (under r' (f a))"

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

   177     hence "f(under r a) = under r' (f a)"

   178     by (simp add: bij_betw_def)

   179     with ** image_def[of f "under r a"] obtain b where

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

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

   182     by (auto simp add: wo_rel.ofilter_def)

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

   184   qed

   185 qed

   186

   187 lemma embed_Field_ofilter:

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

   189         EMB: "embed r r' f"

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

   191 proof-

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

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

   194   with WELL WELL' EMB

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

   196 qed

   197

   198 lemma embed_compat:

   199 assumes EMB: "embed r r' f"

   200 shows "compat r r' f"

   201 proof(unfold compat_def, clarify)

   202   fix a b

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

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

   205   have "a \<in> under r b"

   206   using * under_def[of r] by simp

   207   hence "f a \<in> under r' (f b)"

   208   using EMB embed_def[of r r' f]

   209         bij_betw_def[of f "under r b" "under r' (f b)"]

   210         image_def[of f "under r b"] 1 by auto

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

   212   by (auto simp add: under_def)

   213 qed

   214

   215 lemma embed_inj_on:

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

   217 shows "inj_on f (Field r)"

   218 proof(unfold inj_on_def, clarify)

   219   (* Preliminary facts *)

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

   221   with wo_rel.TOTAL[of r]

   222   have Total: "Total r" by simp

   223   from Well wo_rel.REFL[of r]

   224   have Refl: "Refl r" by simp

   225   (* Main proof *)

   226   fix a b

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

   228          ***: "f a = f b"

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

   230   unfolding Field_def by auto

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

   232    hence "a \<in> under r b \<and> b \<in> under r b"

   233    using Refl by(auto simp add: under_def refl_on_def)

   234    hence "a = b"

   235    using EMB 1 ***

   236    by (auto simp add: embed_def bij_betw_def inj_on_def)

   237   }

   238   moreover

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

   240    hence "a \<in> under r a \<and> b \<in> under r a"

   241    using Refl by(auto simp add: under_def refl_on_def)

   242    hence "a = b"

   243    using EMB 1 ***

   244    by (auto simp add: embed_def bij_betw_def inj_on_def)

   245   }

   246   ultimately

   247   show "a = b" using Total 1

   248   by (auto simp add: total_on_def)

   249 qed

   250

   251 lemma embed_underS:

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

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

   254 shows "bij_betw f (underS r a) (underS r' (f a))"

   255 proof-

   256   have "bij_betw f (under r a) (under r' (f a))"

   257   using assms by (auto simp add: embed_def)

   258   moreover

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

   260    hence "under r a = underS r a \<union> {a} \<and>

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

   262    using assms by (auto simp add: order_on_defs Refl_under_underS)

   263   }

   264   moreover

   265   {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"

   266    unfolding underS_def by blast

   267   }

   268   ultimately show ?thesis

   269   by (auto simp add: notIn_Un_bij_betw3)

   270 qed

   271

   272 lemma embed_iff_compat_inj_on_ofilter:

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

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

   275 using assms

   276 proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,

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

   278   fix a

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

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

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

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

   283   (* Preliminary facts *)

   284   have Well: "wo_rel r"

   285   using WELL wo_rel_def[of r] by simp

   286   hence Refl: "Refl r"

   287   using wo_rel.REFL[of r] by simp

   288   have Total: "Total r"

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

   290   have Well': "wo_rel r'"

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

   292   hence Antisym': "antisym r'"

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

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

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

   296         refl_on_def[of _ r] by auto

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

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

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

   300   unfolding Field_def by auto

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

   302   using **** by auto

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

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

   305   (* Main proof *)

   306   show "bij_betw f (under r a) (under r' (f a))"

   307   proof(unfold bij_betw_def, auto)

   308     show  "inj_on f (under r a)"

   309     using * by (metis (no_types) under_Field subset_inj_on)

   310   next

   311     fix b assume "b \<in> under r a"

   312     thus "f b \<in> under r' (f a)"

   313     unfolding under_def using **

   314     by (auto simp add: compat_def)

   315   next

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

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

   318     using 2 by auto

   319     with Field_def[of r] obtain b where

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

   321     have "(b,a): r"

   322     proof-

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

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

   325        by (auto simp add: compat_def)

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

   327        by(auto simp add: under_def antisym_def)

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

   329        by(auto simp add: inj_on_def)

   330       }

   331       moreover

   332       {assume "a = b"

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

   334        by (auto simp add: refl_on_def)

   335       }

   336       ultimately

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

   338     qed

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

   340     unfolding under_def by auto

   341   qed

   342 qed

   343

   344 lemma inv_into_ofilter_embed:

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

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

   347         IMAGE: "f  A = Field r'"

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

   349 proof-

   350   (* Preliminary facts *)

   351   have Well: "wo_rel r"

   352   using WELL wo_rel_def[of r] by simp

   353   have Refl: "Refl r"

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

   355   have Total: "Total r"

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

   357   (* Main proof *)

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

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

   360     fix b1 b2

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

   362            ***: "f b1 = f b2"

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

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

   365     moreover

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

   367      hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"

   368      unfolding under_def using 11 Refl

   369      by (auto simp add: refl_on_def)

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

   371      by (simp add: bij_betw_def inj_on_def)

   372     }

   373     moreover

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

   375      hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"

   376      unfolding under_def using 11 Refl

   377      by (auto simp add: refl_on_def)

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

   379      by (simp add: bij_betw_def inj_on_def)

   380     }

   381     ultimately

   382     show "b1 = b2"

   383     using Total by (auto simp add: total_on_def)

   384   qed

   385   (*  *)

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

   387   (*  *)

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

   389   proof(clarify)

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

   391     hence "under r b \<le> A"

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

   393     moreover

   394     have "f  (under r b) = under r' (f b)"

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

   396     ultimately

   397     show "bij_betw ?f' (under r' (f b)) (under r b)"

   398     using 1 by (auto simp add: bij_betw_inv_into_subset)

   399   qed

   400   (*  *)

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

   402   proof(clarify)

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

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

   405     by (auto simp add: bij_betw_inv_into_right)

   406     moreover

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

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

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

   410     }

   411     ultimately

   412     show  "bij_betw ?f' (under r' b') (under r (?f' b'))"

   413     using 2 by auto

   414   qed

   415   (*  *)

   416   thus ?thesis unfolding embed_def .

   417 qed

   418

   419 lemma inv_into_underS_embed:

   420 assumes WELL: "Well_order r" and

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

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

   423         IMAGE: "f  (underS r a) = Field r'"

   424 shows "embed r' r (inv_into (underS r a) f)"

   425 using assms

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

   427

   428 lemma inv_into_Field_embed:

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

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

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

   432 proof-

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

   434   using EMB by (auto simp add: embed_def)

   435   moreover

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

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

   438   ultimately

   439   show ?thesis using assms

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

   441 qed

   442

   443 lemma inv_into_Field_embed_bij_betw:

   444 assumes WELL: "Well_order r" and

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

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

   447 proof-

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

   449   using BIJ by (auto simp add: bij_betw_def)

   450   thus ?thesis using assms

   451   by(auto simp add: inv_into_Field_embed)

   452 qed

   453

   454

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

   456

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

   458 @{text "wellorders_totally_ordered"}:

   459

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

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

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

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

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

   465    gets exhausted or not.

   466

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

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

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

   470

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

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

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

   474 *}

   475

   476 lemma wellorders_totally_ordered_aux:

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

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

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

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

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

   482 shows "bij_betw f (under r a) (under r' (f a))"

   483 proof-

   484   (* Preliminary facts *)

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

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

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

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

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

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

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

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

   493   (* Gather facts about elements of underS r a *)

   494   {fix b assume *: "b \<in> underS r a"

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

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

   497    using * underS_Field[of r a] by auto

   498    have t2: "f(under r b) = under r' (f b)"

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

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

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

   502    have "f(under r b) \<le> Field r'"

   503    using t2 by (auto simp add: under_Field)

   504    moreover

   505    have "b \<in> under r b"

   506    using t1 by(auto simp add: Refl Refl_under_in)

   507    ultimately

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

   509    have "f(under r b) = under r' (f b) \<and>

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

   511          f b \<in> Field r'"

   512    using t2 t3 t4 by auto

   513   }

   514   hence bFact:

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

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

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

   518   (*  *)

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

   520   using bFact by blast

   521   (*  *)

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

   523   proof-

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

   525     using UN by auto

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

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

   528     using bFact by auto

   529     finally

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

   531     thus ?thesis

   532     using Well' bFact

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

   534   qed

   535   (*  *)

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

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

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

   539   using subField NOT by blast

   540   (* Main proof *)

   541   have INCL1: "f(underS r a) \<le> underS r' (f a) "

   542   proof(auto)

   543     fix b assume *: "b \<in> underS r a"

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

   545     using subField Well' SUC NE *

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

   547     thus "f b \<in> underS r' (f a)"

   548     unfolding underS_def by simp

   549   qed

   550   (*  *)

   551   have INCL2: "underS r' (f a) \<le> f(underS r a)"

   552   proof

   553     fix b' assume "b' \<in> underS r' (f a)"

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

   555     unfolding underS_def by simp

   556     thus "b' \<in> f(underS r a)"

   557     using Well' SUC NE OF'

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

   559   qed

   560   (*  *)

   561   have INJ: "inj_on f (underS r a)"

   562   proof-

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

   564     using IH by (auto simp add: bij_betw_def)

   565     moreover

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

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

   568     ultimately show  ?thesis

   569     using WELL bFact UN

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

   571     by auto

   572   qed

   573   (*  *)

   574   have BIJ: "bij_betw f (underS r a) (underS r' (f a))"

   575   unfolding bij_betw_def

   576   using INJ INCL1 INCL2 by auto

   577   (*  *)

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

   579   using Well' subField NE SUC

   580   by (auto simp add: wo_rel.suc_inField)

   581   thus ?thesis

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

   583 qed

   584

   585 lemma wellorders_totally_ordered_aux2:

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

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

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

   589 MAIN1:

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

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

   592          \<and>

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

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

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

   596               bij_betw f (under r a) (under r' (f a))" and

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

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

   599 proof-

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

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

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

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

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

   605   (*  *)

   606   have 0: "under r a = underS r a \<union> {a}"

   607   using Refl Case by(auto simp add: Refl_under_underS)

   608   (*  *)

   609   have 1: "g a = False"

   610   proof-

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

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

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

   614     thus ?thesis by blast

   615   qed

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

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

   618   (*  *)

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

   620   (*  *)

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

   622   proof

   623     assume "False \<in> g(underS r ?a)"

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

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

   626     by (auto simp add: underS_def)

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

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

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

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

   631     with 32 Antisym show False

   632     by (auto simp add: antisym_def)

   633   qed

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

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

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

   637   (*   *)

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

   639   (*  *)

   640   have 6: "f(underS r ?a) = Field r'"

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

   642   (*  *)

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

   644   proof

   645     fix b assume as: "b \<in> underS r ?a"

   646     moreover

   647     have "wo_rel.ofilter r (underS r ?a)"

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

   649     ultimately

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

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

   652     unfolding Field_def using as by (auto simp add: underS_def)

   653     ultimately

   654     show "bij_betw f (under r b) (under r' (f b))"

   655     using MAIN2 by auto

   656   qed

   657   (*  *)

   658   have "embed r' r (inv_into (underS r ?a) f)"

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

   660   thus ?thesis

   661   unfolding embed_def by blast

   662 qed

   663

   664 theorem wellorders_totally_ordered:

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

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

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

   668 proof-

   669   (* Preliminary facts *)

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

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

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

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

   674   (* Main proof *)

   675   obtain H where H_def: "H =

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

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

   678                 else (undefined, False))" by blast

   679   have Adm: "wo_rel.adm_wo r H"

   680   using Well

   681   proof(unfold wo_rel.adm_wo_def, clarify)

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

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

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

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

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

   687            (snd o h1)(underS r x) = (snd o h2)(underS r x)"

   688       by (auto simp add: image_def)

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

   690   qed

   691   (* More constant definitions:  *)

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

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

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

   695   obtain test where test_def:

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

   697   (*  *)

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

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

   700   have Main1:

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

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

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

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

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

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

   707   qed

   708   (*  *)

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

   710                    bij_betw f (under r a) (under r' (f a))"

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

   712   proof-

   713     fix a show "?phi a"

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

   715           simp only: Well, clarify)

   716       fix a

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

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

   719              **: "False \<notin> g(under r a)"

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

   721       proof(clarify)

   722         fix b assume ***: "b \<in> underS r a"

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

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

   725         using *** underS_Field[of r a] by auto

   726         moreover have "False \<notin> g(under r b)"

   727         using 0 ** Trans under_incr[of r b a] by auto

   728         ultimately show "bij_betw f (under r b) (under r' (f b))"

   729         using IH by auto

   730       qed

   731       (*  *)

   732       have 21: "False \<notin> g(underS r a)"

   733       using ** underS_subset_under[of r a] by auto

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

   735       moreover have 23: "a \<in> under r a"

   736       using Refl * by (auto simp add: Refl_under_in)

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

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

   739       proof

   740         assume "f(underS r a) = Field r'"

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

   742         with 24 show False using ** by blast

   743       qed

   744       (*  *)

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

   746       using 21 2 Main1 test_def by blast

   747       (*  *)

   748       show "bij_betw f (under r a) (under r' (f a))"

   749       using WELL  WELL' 1 2 3 *

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

   751     qed

   752   qed

   753   (*  *)

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

   755   show ?thesis

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

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

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

   759     using Main2 by blast

   760     thus ?thesis unfolding embed_def by blast

   761   next

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

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

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

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

   766           WELL WELL' Main1 Main2 test_def by fast

   767     thus ?thesis by blast

   768   qed

   769 qed

   770

   771

   772 subsection {* Uniqueness of embeddings *}

   773

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

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

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

   777 embeddings of opposite directions are mutually inverse. *}

   778

   779 lemma embed_determined:

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

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

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

   783 proof-

   784   have "bij_betw f (underS r a) (underS r' (f a))"

   785   using assms by (auto simp add: embed_underS)

   786   hence "f(underS r a) = underS r' (f a)"

   787   by (auto simp add: bij_betw_def)

   788   moreover

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

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

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

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

   793   }

   794   ultimately show ?thesis by simp

   795 qed

   796

   797 lemma embed_unique:

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

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

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

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

   802   fix a

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

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

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

   806   unfolding underS_def by (auto simp add: Field_def)

   807   hence "f(underS r a) = g(underS r a)" by force

   808   thus "f a = g a"

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

   810 qed

   811

   812 lemma embed_bothWays_inverse:

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

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

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

   816 proof-

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

   818   by(auto simp add: comp_embed)

   819   moreover have "embed r r id" using assms

   820   by (auto simp add: id_embed)

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

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

   823   moreover

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

   825    by(auto simp add: comp_embed)

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

   827    by (auto simp add: id_embed)

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

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

   830   }

   831   ultimately show ?thesis by blast

   832 qed

   833

   834 lemma embed_bothWays_bij_betw:

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

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

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

   838 proof-

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

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

   841   using assms by (auto simp add: comp_embed)

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

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

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

   845         id_def by auto

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

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

   848   (*  *)

   849   show ?thesis

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

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

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

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

   854   next

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

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

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

   858   qed

   859 qed

   860

   861 lemma embed_bothWays_iso:

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

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

   864 shows "iso r r' f"

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

   866

   867

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

   869

   870 lemma embed_bothWays_Field_bij_betw:

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

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

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

   874 proof-

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

   876   using assms by (auto simp add: embed_bothWays_inverse)

   877   moreover

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

   879   using assms by (auto simp add: embed_Field)

   880   ultimately

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

   882 qed

   883

   884 lemma embedS_comp_embed:

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

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

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

   888 proof-

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

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

   891   using EMB by (auto simp add: embedS_def)

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

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

   894   moreover

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

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

   897    by (auto simp add: inv_into_Field_embed_bij_betw)

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

   899    by (auto simp add: comp_embed)

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

   901    by (auto simp add: embed_bothWays_Field_bij_betw)

   902    with 1 have False by blast

   903   }

   904   ultimately show ?thesis unfolding embedS_def by auto

   905 qed

   906

   907 lemma embed_comp_embedS:

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

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

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

   911 proof-

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

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

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

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

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

   917   moreover

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

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

   920    by (auto simp add: inv_into_Field_embed_bij_betw)

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

   922    by (auto simp add: comp_embed)

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

   924    by (auto simp add: embed_bothWays_Field_bij_betw)

   925    with 1 have False by blast

   926   }

   927   ultimately show ?thesis unfolding embedS_def by auto

   928 qed

   929

   930 lemma embed_comp_iso:

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

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

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

   934 using assms unfolding iso_def

   935 by (auto simp add: comp_embed)

   936

   937 lemma iso_comp_embed:

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

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

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

   941 using assms unfolding iso_def

   942 by (auto simp add: comp_embed)

   943

   944 lemma embedS_comp_iso:

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

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

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

   948 using assms unfolding iso_def

   949 by (auto simp add: embedS_comp_embed)

   950

   951 lemma iso_comp_embedS:

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

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

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

   955 using assms unfolding iso_def  using embed_comp_embedS

   956 by (auto simp add: embed_comp_embedS)

   957

   958 lemma embedS_Field:

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

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

   961 proof-

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

   963   by (auto simp add: embed_Field embedS_def)

   964   moreover

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

   966    by (auto simp add: embedS_def embed_inj_on)

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

   968    by (auto simp add: embedS_def bij_betw_def)

   969   }

   970   ultimately show ?thesis by blast

   971 qed

   972

   973 lemma embedS_iff:

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

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

   976 proof

   977   assume "embedS r r' f"

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

   979   using WELL by (auto simp add: embedS_Field)

   980 next

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

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

   983   unfolding bij_betw_def by blast

   984   thus "embedS r r' f" unfolding embedS_def

   985   using ISO by auto

   986 qed

   987

   988 lemma iso_Field:

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

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

   991

   992 lemma iso_iff:

   993 assumes "Well_order r"

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

   995 proof

   996   assume "iso r r' f"

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

   998   by (auto simp add: iso_Field iso_def)

   999 next

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

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

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

  1003   unfolding bij_betw_def by simp

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

  1005 qed

  1006

  1007 lemma iso_iff2:

  1008 assumes "Well_order r"

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

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

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

  1012 using assms

  1013 proof(auto simp add: iso_def)

  1014   fix a b

  1015   assume "embed r r' f"

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

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

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

  1019 next

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

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

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

  1023   by (auto simp add: inv_into_Field_embed_bij_betw)

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

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

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

  1027   by (auto simp add: bij_betw_inv_into_left)

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

  1029 next

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

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

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

  1033   by (auto simp add: under_Field)

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

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

  1036    have "bij_betw f (under r a) (under r' (f a))"

  1037    proof(unfold bij_betw_def, auto)

  1038      show "inj_on f (under r a)"

  1039      using 1 2 by (metis subset_inj_on)

  1040    next

  1041      fix b assume "b \<in> under r a"

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

  1043      unfolding under_def by (auto simp add: Field_def Range_def Domain_def)

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

  1045      unfolding under_def by auto

  1046    next

  1047      fix b' assume "b' \<in> under r' (f a)"

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

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

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

  1051      unfolding bij_betw_def by force

  1052      with 3 ** ***

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

  1054    qed

  1055   }

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

  1057 qed

  1058

  1059 lemma iso_iff3:

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

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

  1062 proof

  1063   assume "iso r r' f"

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

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

  1066 next

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

  1068   by (auto simp add: wo_rel_def)

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

  1070   thus "iso r r' f"

  1071   unfolding "compat_def" using assms

  1072   proof(auto simp add: iso_iff2)

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

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

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

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

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

  1078      hence "f a = f b"

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

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

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

  1082     }

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

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

  1085   qed

  1086 qed

  1087

  1088 end