src/HOL/BNF_Wellorder_Embedding.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 60758 d8d85a8172b5 child 61799 4cf66f21b764 permissions -rw-r--r--
prefer symbols;
     1 (*  Title:      HOL/BNF_Wellorder_Embedding.thy

     2     Author:     Andrei Popescu, TU Muenchen

     3     Copyright   2012

     4

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

     6 *)

     7

     8 section \<open>Well-Order Embeddings as Needed by Bounded Natural Functors\<close>

     9

    10 theory BNF_Wellorder_Embedding

    11 imports Hilbert_Choice BNF_Wellorder_Relation

    12 begin

    13

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

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

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

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

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

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

    20 any two types, one is smaller than (i.e., can be injected into) the other.\<close>

    21

    22

    23 subsection \<open>Auxiliaries\<close>

    24

    25 lemma UNION_inj_on_ofilter:

    26 assumes WELL: "Well_order r" and

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

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

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

    30 proof-

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

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

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

    34   with WELL INJ show ?thesis

    35   by (auto simp add: inj_on_UNION_chain)

    36 qed

    37

    38 lemma under_underS_bij_betw:

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

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

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

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

    43 proof-

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

    45   unfolding underS_def by auto

    46   moreover

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

    48    by (auto simp add: order_on_defs)

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

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

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

    52   }

    53   ultimately show ?thesis

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

    55 qed

    56

    57

    58 subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible

    59 functions\<close>

    60

    61 text\<open>Standardly, a function is an embedding of a well-order in another if it injectively and

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

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

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

    65 between the set of strict lower bounds of that element

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

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

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

    69 and an isomorphism (operator @{text "iso"}) is a bijective embedding.\<close>

    70

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

    72 where

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

    74

    75 lemmas embed_defs = embed_def embed_def[abs_def]

    76

    77 text \<open>Strict embeddings:\<close>

    78

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

    80 where

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

    82

    83 lemmas embedS_defs = embedS_def embedS_def[abs_def]

    84

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

    86 where

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

    88

    89 lemmas iso_defs = iso_def iso_def[abs_def]

    90

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

    92 where

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

    94

    95 lemma compat_wf:

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

    97 shows "wf r"

    98 proof-

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

   100   unfolding inv_image_def using CMP

   101   by (auto simp add: compat_def)

   102   with WF show ?thesis

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

   104 qed

   105

   106 lemma id_embed: "embed r r id"

   107 by(auto simp add: id_def embed_def bij_betw_def)

   108

   109 lemma id_iso: "iso r r id"

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

   111

   112 lemma embed_in_Field:

   113 assumes WELL: "Well_order r" and

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

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

   116 proof-

   117   have Well: "wo_rel r"

   118   using WELL by (auto simp add: wo_rel_def)

   119   hence 1: "Refl r"

   120   by (auto simp add: wo_rel.REFL)

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

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

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

   124   thus ?thesis unfolding Field_def

   125   by (auto simp: under_def)

   126 qed

   127

   128 lemma comp_embed:

   129 assumes WELL: "Well_order r" and

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

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

   132 proof(unfold embed_def, auto)

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

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

   135   using embed_def[of r] EMB by auto

   136   moreover

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

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

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

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

   141   }

   142   ultimately

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

   144   by(auto simp add: bij_betw_trans)

   145 qed

   146

   147 lemma comp_iso:

   148 assumes WELL: "Well_order r" and

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

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

   151 using assms unfolding iso_def

   152 by (auto simp add: comp_embed bij_betw_trans)

   153

   154 text\<open>That @{text "embedS"} is also preserved by function composition shall be proved only later.\<close>

   155

   156 lemma embed_Field:

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

   158 by (auto simp add: embed_in_Field)

   159

   160 lemma embed_preserves_ofilter:

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

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

   163 shows "wo_rel.ofilter r' (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)" by (rule subset_inj_on[OF * under_Field])

   309   next

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

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

   312     unfolding under_def using **

   313     by (auto simp add: compat_def)

   314   next

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

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

   317     using 2 by auto

   318     with Field_def[of r] obtain b where

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

   320     have "(b,a): r"

   321     proof-

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

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

   324        by (auto simp add: compat_def)

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

   326        by(auto simp add: under_def antisym_def)

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

   328        by(auto simp add: inj_on_def)

   329       }

   330       moreover

   331       {assume "a = b"

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

   333        by (auto simp add: refl_on_def)

   334       }

   335       ultimately

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

   337     qed

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

   339     unfolding under_def by auto

   340   qed

   341 qed

   342

   343 lemma inv_into_ofilter_embed:

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

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

   346         IMAGE: "f  A = Field r'"

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

   348 proof-

   349   (* Preliminary facts *)

   350   have Well: "wo_rel r"

   351   using WELL wo_rel_def[of r] by simp

   352   have Refl: "Refl r"

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

   354   have Total: "Total r"

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

   356   (* Main proof *)

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

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

   359     fix b1 b2

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

   361            ***: "f b1 = f b2"

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

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

   364     moreover

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

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

   367      unfolding under_def using 11 Refl

   368      by (auto simp add: refl_on_def)

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

   370      by (simp add: bij_betw_def inj_on_def)

   371     }

   372     moreover

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

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

   375      unfolding under_def using 11 Refl

   376      by (auto simp add: refl_on_def)

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

   378      by (simp add: bij_betw_def inj_on_def)

   379     }

   380     ultimately

   381     show "b1 = b2"

   382     using Total by (auto simp add: total_on_def)

   383   qed

   384   (*  *)

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

   386   (*  *)

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

   388   proof(clarify)

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

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

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

   392     moreover

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

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

   395     ultimately

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

   397     using 1 by (auto simp add: bij_betw_inv_into_subset)

   398   qed

   399   (*  *)

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

   401   proof(clarify)

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

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

   404     by (auto simp add: bij_betw_inv_into_right)

   405     moreover

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

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

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

   409     }

   410     ultimately

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

   412     using 2 by auto

   413   qed

   414   (*  *)

   415   thus ?thesis unfolding embed_def .

   416 qed

   417

   418 lemma inv_into_underS_embed:

   419 assumes WELL: "Well_order r" and

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

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

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

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

   424 using assms

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

   426

   427 lemma inv_into_Field_embed:

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

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

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

   431 proof-

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

   433   using EMB by (auto simp add: embed_def)

   434   moreover

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

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

   437   ultimately

   438   show ?thesis using assms

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

   440 qed

   441

   442 lemma inv_into_Field_embed_bij_betw:

   443 assumes WELL: "Well_order r" and

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

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

   446 proof-

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

   448   using BIJ by (auto simp add: bij_betw_def)

   449   thus ?thesis using assms

   450   by(auto simp add: inv_into_Field_embed)

   451 qed

   452

   453

   454 subsection \<open>Given any two well-orders, one can be embedded in the other\<close>

   455

   456 text\<open>Here is an overview of the proof of of this fact, stated in theorem

   457 @{text "wellorders_totally_ordered"}:

   458

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

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

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

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

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

   464    gets exhausted or not.

   465

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

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

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

   469

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

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

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

   473 \<close>

   474

   475 lemma wellorders_totally_ordered_aux:

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

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

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

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

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

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

   482 proof-

   483   (* Preliminary facts *)

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

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

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

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

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

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

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

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

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

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

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

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

   496    using * underS_Field[of r a] by auto

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

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

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

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

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

   502    using t2 by (auto simp add: under_Field)

   503    moreover

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

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

   506    ultimately

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

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

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

   510          f b \<in> Field r'"

   511    using t2 t3 t4 by auto

   512   }

   513   hence bFact:

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

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

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

   517   (*  *)

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

   519   using bFact by blast

   520   (*  *)

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

   522   proof-

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

   524     using UN by auto

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

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

   527     using bFact by auto

   528     finally

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

   530     thus ?thesis

   531     using Well' bFact

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

   533   qed

   534   (*  *)

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

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

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

   538   using subField NOT by blast

   539   (* Main proof *)

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

   541   proof(auto)

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

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

   544     using subField Well' SUC NE *

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

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

   547     unfolding underS_def by simp

   548   qed

   549   (*  *)

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

   551   proof

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

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

   554     unfolding underS_def by simp

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

   556     using Well' SUC NE OF'

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

   558   qed

   559   (*  *)

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

   561   proof-

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

   563     using IH by (auto simp add: bij_betw_def)

   564     moreover

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

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

   567     ultimately show  ?thesis

   568     using WELL bFact UN

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

   570     by auto

   571   qed

   572   (*  *)

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

   574   unfolding bij_betw_def

   575   using INJ INCL1 INCL2 by auto

   576   (*  *)

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

   578   using Well' subField NE SUC

   579   by (auto simp add: wo_rel.suc_inField)

   580   thus ?thesis

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

   582 qed

   583

   584 lemma wellorders_totally_ordered_aux2:

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

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

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

   588 MAIN1:

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

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

   591          \<and>

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

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

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

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

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

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

   598 proof-

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

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

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

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

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

   604   (*  *)

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

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

   607   (*  *)

   608   have 1: "g a = False"

   609   proof-

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

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

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

   613     thus ?thesis by blast

   614   qed

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

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

   617   (*  *)

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

   619   (*  *)

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

   621   proof

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

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

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

   625     by (auto simp add: underS_def)

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

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

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

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

   630     with 32 Antisym show False

   631     by (auto simp add: antisym_def)

   632   qed

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

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

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

   636   (*   *)

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

   638   (*  *)

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

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

   641   (*  *)

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

   643   proof

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

   645     moreover

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

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

   648     ultimately

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

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

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

   652     ultimately

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

   654     using MAIN2 by auto

   655   qed

   656   (*  *)

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

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

   659   thus ?thesis

   660   unfolding embed_def by blast

   661 qed

   662

   663 theorem wellorders_totally_ordered:

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

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

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

   667 proof-

   668   (* Preliminary facts *)

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

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

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

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

   673   (* Main proof *)

   674   obtain H where H_def: "H =

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

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

   677                 else (undefined, False))" by blast

   678   have Adm: "wo_rel.adm_wo r H"

   679   using Well

   680   proof(unfold wo_rel.adm_wo_def, clarify)

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

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

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

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

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

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

   687       by (auto simp add: image_def)

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

   689   qed

   690   (* More constant definitions:  *)

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

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

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

   694   obtain test where test_def:

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

   696   (*  *)

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

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

   699   have Main1:

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

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

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

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

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

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

   706   qed

   707   (*  *)

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

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

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

   711   proof-

   712     fix a show "?phi a"

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

   714           simp only: Well, clarify)

   715       fix a

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

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

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

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

   720       proof(clarify)

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

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

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

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

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

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

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

   728         using IH by auto

   729       qed

   730       (*  *)

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

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

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

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

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

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

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

   738       proof

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

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

   741         with 24 show False using ** by blast

   742       qed

   743       (*  *)

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

   745       using 21 2 Main1 test_def by blast

   746       (*  *)

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

   748       using WELL  WELL' 1 2 3 *

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

   750     qed

   751   qed

   752   (*  *)

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

   754   show ?thesis

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

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

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

   758     using Main2 by blast

   759     thus ?thesis unfolding embed_def by blast

   760   next

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

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

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

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

   765           WELL WELL' Main1 Main2 test_def by fast

   766     thus ?thesis by blast

   767   qed

   768 qed

   769

   770

   771 subsection \<open>Uniqueness of embeddings\<close>

   772

   773 text\<open>Here we show a fact complementary to the one from the previous subsection -- namely,

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

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

   776 embeddings of opposite directions are mutually inverse.\<close>

   777

   778 lemma embed_determined:

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

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

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

   782 proof-

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

   784   using assms by (auto simp add: embed_underS)

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

   786   by (auto simp add: bij_betw_def)

   787   moreover

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

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

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

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

   792   }

   793   ultimately show ?thesis by simp

   794 qed

   795

   796 lemma embed_unique:

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

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

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

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

   801   fix a

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

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

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

   805   unfolding underS_def by (auto simp add: Field_def)

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

   807   thus "f a = g a"

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

   809 qed

   810

   811 lemma embed_bothWays_inverse:

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

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

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

   815 proof-

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

   817   by(auto simp add: comp_embed)

   818   moreover have "embed r r id" using assms

   819   by (auto simp add: id_embed)

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

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

   822   moreover

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

   824    by(auto simp add: comp_embed)

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

   826    by (auto simp add: id_embed)

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

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

   829   }

   830   ultimately show ?thesis by blast

   831 qed

   832

   833 lemma embed_bothWays_bij_betw:

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

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

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

   837 proof-

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

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

   840   using assms by (auto simp add: comp_embed)

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

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

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

   844         id_def by auto

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

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

   847   (*  *)

   848   show ?thesis

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

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

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

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

   853   next

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

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

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

   857   qed

   858 qed

   859

   860 lemma embed_bothWays_iso:

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

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

   863 shows "iso r r' f"

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

   865

   866

   867 subsection \<open>More properties of embeddings, strict embeddings and isomorphisms\<close>

   868

   869 lemma embed_bothWays_Field_bij_betw:

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

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

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

   873 proof-

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

   875   using assms by (auto simp add: embed_bothWays_inverse)

   876   moreover

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

   878   using assms by (auto simp add: embed_Field)

   879   ultimately

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

   881 qed

   882

   883 lemma embedS_comp_embed:

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

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

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

   887 proof-

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

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

   890   using EMB by (auto simp add: embedS_def)

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

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

   893   moreover

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

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

   896    by (auto simp add: inv_into_Field_embed_bij_betw)

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

   898    by (auto simp add: comp_embed)

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

   900    by (auto simp add: embed_bothWays_Field_bij_betw)

   901    with 1 have False by blast

   902   }

   903   ultimately show ?thesis unfolding embedS_def by auto

   904 qed

   905

   906 lemma embed_comp_embedS:

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

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

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

   910 proof-

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

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

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

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

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

   916   moreover

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

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

   919    by (auto simp add: inv_into_Field_embed_bij_betw)

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

   921    by (auto simp add: comp_embed)

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

   923    by (auto simp add: embed_bothWays_Field_bij_betw)

   924    with 1 have False by blast

   925   }

   926   ultimately show ?thesis unfolding embedS_def by auto

   927 qed

   928

   929 lemma embed_comp_iso:

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

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

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

   933 using assms unfolding iso_def

   934 by (auto simp add: comp_embed)

   935

   936 lemma iso_comp_embed:

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

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

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

   940 using assms unfolding iso_def

   941 by (auto simp add: comp_embed)

   942

   943 lemma embedS_comp_iso:

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

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

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

   947 using assms unfolding iso_def

   948 by (auto simp add: embedS_comp_embed)

   949

   950 lemma iso_comp_embedS:

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

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

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

   954 using assms unfolding iso_def  using embed_comp_embedS

   955 by (auto simp add: embed_comp_embedS)

   956

   957 lemma embedS_Field:

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

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

   960 proof-

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

   962   by (auto simp add: embed_Field embedS_def)

   963   moreover

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

   965    by (auto simp add: embedS_def embed_inj_on)

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

   967    by (auto simp add: embedS_def bij_betw_def)

   968   }

   969   ultimately show ?thesis by blast

   970 qed

   971

   972 lemma embedS_iff:

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

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

   975 proof

   976   assume "embedS r r' f"

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

   978   using WELL by (auto simp add: embedS_Field)

   979 next

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

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

   982   unfolding bij_betw_def by blast

   983   thus "embedS r r' f" unfolding embedS_def

   984   using ISO by auto

   985 qed

   986

   987 lemma iso_Field:

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

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

   990

   991 lemma iso_iff:

   992 assumes "Well_order r"

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

   994 proof

   995   assume "iso r r' f"

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

   997   by (auto simp add: iso_Field iso_def)

   998 next

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

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

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

  1002   unfolding bij_betw_def by simp

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

  1004 qed

  1005

  1006 lemma iso_iff2:

  1007 assumes "Well_order r"

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

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

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

  1011 using assms

  1012 proof(auto simp add: iso_def)

  1013   fix a b

  1014   assume "embed r r' f"

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

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

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

  1018 next

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

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

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

  1022   by (auto simp add: inv_into_Field_embed_bij_betw)

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

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

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

  1026   by (auto simp add: bij_betw_inv_into_left)

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

  1028 next

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

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

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

  1032   by (auto simp add: under_Field)

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

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

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

  1036    proof(unfold bij_betw_def, auto)

  1037      show "inj_on f (under r a)" using 1 2 subset_inj_on by blast

  1038    next

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

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

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

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

  1043      unfolding under_def by auto

  1044    next

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

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

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

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

  1049      unfolding bij_betw_def by force

  1050      with 3 ** ***

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

  1052    qed

  1053   }

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

  1055 qed

  1056

  1057 lemma iso_iff3:

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

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

  1060 proof

  1061   assume "iso r r' f"

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

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

  1064 next

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

  1066   by (auto simp add: wo_rel_def)

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

  1068   thus "iso r r' f"

  1069   unfolding "compat_def" using assms

  1070   proof(auto simp add: iso_iff2)

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

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

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

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

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

  1076      hence "f a = f b"

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

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

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

  1080     }

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

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

  1083   qed

  1084 qed

  1085

  1086 end