src/HOL/BNF_Wellorder_Embedding.thy
changeset 55056 b5c94200d081
parent 55054 e1f3714bc508
child 55059 ef2e0fb783c6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Mon Jan 20 18:24:55 2014 +0100
     1.3 @@ -0,0 +1,1145 @@
     1.4 +(*  Title:      HOL/BNF_Wellorder_Embedding.thy
     1.5 +    Author:     Andrei Popescu, TU Muenchen
     1.6 +    Copyright   2012
     1.7 +
     1.8 +Well-order embeddings (BNF).
     1.9 +*)
    1.10 +
    1.11 +header {* Well-Order Embeddings (BNF) *}
    1.12 +
    1.13 +theory BNF_Wellorder_Embedding
    1.14 +imports Zorn BNF_Wellorder_Relation
    1.15 +begin
    1.16 +
    1.17 +
    1.18 +text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
    1.19 +prove their basic properties.  The notion of embedding is considered from the point
    1.20 +of view of the theory of ordinals, and therefore requires the source to be injected
    1.21 +as an {\em initial segment} (i.e., {\em order filter}) of the target.  A main result
    1.22 +of this section is the existence of embeddings (in one direction or another) between
    1.23 +any two well-orders, having as a consequence the fact that, given any two sets on
    1.24 +any two types, one is smaller than (i.e., can be injected into) the other. *}
    1.25 +
    1.26 +
    1.27 +subsection {* Auxiliaries *}
    1.28 +
    1.29 +lemma UNION_inj_on_ofilter:
    1.30 +assumes WELL: "Well_order r" and
    1.31 +        OF: "\<And> i. i \<in> I \<Longrightarrow> wo_rel.ofilter r (A i)" and
    1.32 +       INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.33 +shows "inj_on f (\<Union> i \<in> I. A i)"
    1.34 +proof-
    1.35 +  have "wo_rel r" using WELL by (simp add: wo_rel_def)
    1.36 +  hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i <= A j \<or> A j <= A i"
    1.37 +  using wo_rel.ofilter_linord[of r] OF by blast
    1.38 +  with WELL INJ show ?thesis
    1.39 +  by (auto simp add: inj_on_UNION_chain)
    1.40 +qed
    1.41 +
    1.42 +
    1.43 +lemma under_underS_bij_betw:
    1.44 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
    1.45 +        IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
    1.46 +        BIJ: "bij_betw f (underS r a) (underS r' (f a))"
    1.47 +shows "bij_betw f (under r a) (under r' (f a))"
    1.48 +proof-
    1.49 +  have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
    1.50 +  unfolding underS_def by auto
    1.51 +  moreover
    1.52 +  {have "Refl r \<and> Refl r'" using WELL WELL'
    1.53 +   by (auto simp add: order_on_defs)
    1.54 +   hence "under r a = underS r a \<union> {a} \<and>
    1.55 +          under r' (f a) = underS r' (f a) \<union> {f a}"
    1.56 +   using IN IN' by(auto simp add: Refl_under_underS)
    1.57 +  }
    1.58 +  ultimately show ?thesis
    1.59 +  using BIJ notIn_Un_bij_betw[of a "underS r a" f "underS r' (f a)"] by auto
    1.60 +qed
    1.61 +
    1.62 +
    1.63 +
    1.64 +subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
    1.65 +functions  *}
    1.66 +
    1.67 +
    1.68 +text{* Standardly, a function is an embedding of a well-order in another if it injectively and
    1.69 +order-compatibly maps the former into an order filter of the latter.
    1.70 +Here we opt for a more succinct definition (operator @{text "embed"}),
    1.71 +asking that, for any element in the source, the function should be a bijection
    1.72 +between the set of strict lower bounds of that element
    1.73 +and the set of strict lower bounds of its image.  (Later we prove equivalence with
    1.74 +the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
    1.75 +A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding
    1.76 +and an isomorphism (operator @{text "iso"}) is a bijective embedding.   *}
    1.77 +
    1.78 +
    1.79 +definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.80 +where
    1.81 +"embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
    1.82 +
    1.83 +
    1.84 +lemmas embed_defs = embed_def embed_def[abs_def]
    1.85 +
    1.86 +
    1.87 +text {* Strict embeddings: *}
    1.88 +
    1.89 +definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.90 +where
    1.91 +"embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
    1.92 +
    1.93 +
    1.94 +lemmas embedS_defs = embedS_def embedS_def[abs_def]
    1.95 +
    1.96 +
    1.97 +definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.98 +where
    1.99 +"iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
   1.100 +
   1.101 +
   1.102 +lemmas iso_defs = iso_def iso_def[abs_def]
   1.103 +
   1.104 +
   1.105 +definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
   1.106 +where
   1.107 +"compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
   1.108 +
   1.109 +
   1.110 +lemma compat_wf:
   1.111 +assumes CMP: "compat r r' f" and WF: "wf r'"
   1.112 +shows "wf r"
   1.113 +proof-
   1.114 +  have "r \<le> inv_image r' f"
   1.115 +  unfolding inv_image_def using CMP
   1.116 +  by (auto simp add: compat_def)
   1.117 +  with WF show ?thesis
   1.118 +  using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
   1.119 +qed
   1.120 +
   1.121 +
   1.122 +lemma id_embed: "embed r r id"
   1.123 +by(auto simp add: id_def embed_def bij_betw_def)
   1.124 +
   1.125 +
   1.126 +lemma id_iso: "iso r r id"
   1.127 +by(auto simp add: id_def embed_def iso_def bij_betw_def)
   1.128 +
   1.129 +
   1.130 +lemma embed_in_Field:
   1.131 +assumes WELL: "Well_order r" and
   1.132 +        EMB: "embed r r' f" and IN: "a \<in> Field r"
   1.133 +shows "f a \<in> Field r'"
   1.134 +proof-
   1.135 +  have Well: "wo_rel r"
   1.136 +  using WELL by (auto simp add: wo_rel_def)
   1.137 +  hence 1: "Refl r"
   1.138 +  by (auto simp add: wo_rel.REFL)
   1.139 +  hence "a \<in> under r a" using IN Refl_under_in by fastforce
   1.140 +  hence "f a \<in> under r' (f a)"
   1.141 +  using EMB IN by (auto simp add: embed_def bij_betw_def)
   1.142 +  thus ?thesis unfolding Field_def
   1.143 +  by (auto simp: under_def)
   1.144 +qed
   1.145 +
   1.146 +
   1.147 +lemma comp_embed:
   1.148 +assumes WELL: "Well_order r" and
   1.149 +        EMB: "embed r r' f" and EMB': "embed r' r'' f'"
   1.150 +shows "embed r r'' (f' o f)"
   1.151 +proof(unfold embed_def, auto)
   1.152 +  fix a assume *: "a \<in> Field r"
   1.153 +  hence "bij_betw f (under r a) (under r' (f a))"
   1.154 +  using embed_def[of r] EMB by auto
   1.155 +  moreover
   1.156 +  {have "f a \<in> Field r'"
   1.157 +   using EMB WELL * by (auto simp add: embed_in_Field)
   1.158 +   hence "bij_betw f' (under r' (f a)) (under r'' (f' (f a)))"
   1.159 +   using embed_def[of r'] EMB' by auto
   1.160 +  }
   1.161 +  ultimately
   1.162 +  show "bij_betw (f' \<circ> f) (under r a) (under r'' (f'(f a)))"
   1.163 +  by(auto simp add: bij_betw_trans)
   1.164 +qed
   1.165 +
   1.166 +
   1.167 +lemma comp_iso:
   1.168 +assumes WELL: "Well_order r" and
   1.169 +        EMB: "iso r r' f" and EMB': "iso r' r'' f'"
   1.170 +shows "iso r r'' (f' o f)"
   1.171 +using assms unfolding iso_def
   1.172 +by (auto simp add: comp_embed bij_betw_trans)
   1.173 +
   1.174 +
   1.175 +text{* That @{text "embedS"} is also preserved by function composition shall be proved only later.  *}
   1.176 +
   1.177 +
   1.178 +lemma embed_Field:
   1.179 +"\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'"
   1.180 +by (auto simp add: embed_in_Field)
   1.181 +
   1.182 +
   1.183 +lemma embed_preserves_ofilter:
   1.184 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.185 +        EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
   1.186 +shows "wo_rel.ofilter r' (f`A)"
   1.187 +proof-
   1.188 +  (* Preliminary facts *)
   1.189 +  from WELL have Well: "wo_rel r" unfolding wo_rel_def .
   1.190 +  from WELL' have Well': "wo_rel r'" unfolding wo_rel_def .
   1.191 +  from OF have 0: "A \<le> Field r" by(auto simp add: Well wo_rel.ofilter_def)
   1.192 +  (* Main proof *)
   1.193 +  show ?thesis  using Well' WELL EMB 0 embed_Field[of r r' f]
   1.194 +  proof(unfold wo_rel.ofilter_def, auto simp add: image_def)
   1.195 +    fix a b'
   1.196 +    assume *: "a \<in> A" and **: "b' \<in> under r' (f a)"
   1.197 +    hence "a \<in> Field r" using 0 by auto
   1.198 +    hence "bij_betw f (under r a) (under r' (f a))"
   1.199 +    using * EMB by (auto simp add: embed_def)
   1.200 +    hence "f`(under r a) = under r' (f a)"
   1.201 +    by (simp add: bij_betw_def)
   1.202 +    with ** image_def[of f "under r a"] obtain b where
   1.203 +    1: "b \<in> under r a \<and> b' = f b" by blast
   1.204 +    hence "b \<in> A" using Well * OF
   1.205 +    by (auto simp add: wo_rel.ofilter_def)
   1.206 +    with 1 show "\<exists>b \<in> A. b' = f b" by blast
   1.207 +  qed
   1.208 +qed
   1.209 +
   1.210 +
   1.211 +lemma embed_Field_ofilter:
   1.212 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.213 +        EMB: "embed r r' f"
   1.214 +shows "wo_rel.ofilter r' (f`(Field r))"
   1.215 +proof-
   1.216 +  have "wo_rel.ofilter r (Field r)"
   1.217 +  using WELL by (auto simp add: wo_rel_def wo_rel.Field_ofilter)
   1.218 +  with WELL WELL' EMB
   1.219 +  show ?thesis by (auto simp add: embed_preserves_ofilter)
   1.220 +qed
   1.221 +
   1.222 +
   1.223 +lemma embed_compat:
   1.224 +assumes EMB: "embed r r' f"
   1.225 +shows "compat r r' f"
   1.226 +proof(unfold compat_def, clarify)
   1.227 +  fix a b
   1.228 +  assume *: "(a,b) \<in> r"
   1.229 +  hence 1: "b \<in> Field r" using Field_def[of r] by blast
   1.230 +  have "a \<in> under r b"
   1.231 +  using * under_def[of r] by simp
   1.232 +  hence "f a \<in> under r' (f b)"
   1.233 +  using EMB embed_def[of r r' f]
   1.234 +        bij_betw_def[of f "under r b" "under r' (f b)"]
   1.235 +        image_def[of f "under r b"] 1 by auto
   1.236 +  thus "(f a, f b) \<in> r'"
   1.237 +  by (auto simp add: under_def)
   1.238 +qed
   1.239 +
   1.240 +
   1.241 +lemma embed_inj_on:
   1.242 +assumes WELL: "Well_order r" and EMB: "embed r r' f"
   1.243 +shows "inj_on f (Field r)"
   1.244 +proof(unfold inj_on_def, clarify)
   1.245 +  (* Preliminary facts *)
   1.246 +  from WELL have Well: "wo_rel r" unfolding wo_rel_def .
   1.247 +  with wo_rel.TOTAL[of r]
   1.248 +  have Total: "Total r" by simp
   1.249 +  from Well wo_rel.REFL[of r]
   1.250 +  have Refl: "Refl r" by simp
   1.251 +  (* Main proof *)
   1.252 +  fix a b
   1.253 +  assume *: "a \<in> Field r" and **: "b \<in> Field r" and
   1.254 +         ***: "f a = f b"
   1.255 +  hence 1: "a \<in> Field r \<and> b \<in> Field r"
   1.256 +  unfolding Field_def by auto
   1.257 +  {assume "(a,b) \<in> r"
   1.258 +   hence "a \<in> under r b \<and> b \<in> under r b"
   1.259 +   using Refl by(auto simp add: under_def refl_on_def)
   1.260 +   hence "a = b"
   1.261 +   using EMB 1 ***
   1.262 +   by (auto simp add: embed_def bij_betw_def inj_on_def)
   1.263 +  }
   1.264 +  moreover
   1.265 +  {assume "(b,a) \<in> r"
   1.266 +   hence "a \<in> under r a \<and> b \<in> under r a"
   1.267 +   using Refl by(auto simp add: under_def refl_on_def)
   1.268 +   hence "a = b"
   1.269 +   using EMB 1 ***
   1.270 +   by (auto simp add: embed_def bij_betw_def inj_on_def)
   1.271 +  }
   1.272 +  ultimately
   1.273 +  show "a = b" using Total 1
   1.274 +  by (auto simp add: total_on_def)
   1.275 +qed
   1.276 +
   1.277 +
   1.278 +lemma embed_underS:
   1.279 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.280 +        EMB: "embed r r' f" and IN: "a \<in> Field r"
   1.281 +shows "bij_betw f (underS r a) (underS r' (f a))"
   1.282 +proof-
   1.283 +  have "bij_betw f (under r a) (under r' (f a))"
   1.284 +  using assms by (auto simp add: embed_def)
   1.285 +  moreover
   1.286 +  {have "f a \<in> Field r'" using assms  embed_Field[of r r' f] by auto
   1.287 +   hence "under r a = underS r a \<union> {a} \<and>
   1.288 +          under r' (f a) = underS r' (f a) \<union> {f a}"
   1.289 +   using assms by (auto simp add: order_on_defs Refl_under_underS)
   1.290 +  }
   1.291 +  moreover
   1.292 +  {have "a \<notin> underS r a \<and> f a \<notin> underS r' (f a)"
   1.293 +   unfolding underS_def by blast
   1.294 +  }
   1.295 +  ultimately show ?thesis
   1.296 +  by (auto simp add: notIn_Un_bij_betw3)
   1.297 +qed
   1.298 +
   1.299 +
   1.300 +lemma embed_iff_compat_inj_on_ofilter:
   1.301 +assumes WELL: "Well_order r" and WELL': "Well_order r'"
   1.302 +shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))"
   1.303 +using assms
   1.304 +proof(auto simp add: embed_compat embed_inj_on embed_Field_ofilter,
   1.305 +      unfold embed_def, auto) (* get rid of one implication *)
   1.306 +  fix a
   1.307 +  assume *: "inj_on f (Field r)" and
   1.308 +         **: "compat r r' f" and
   1.309 +         ***: "wo_rel.ofilter r' (f`(Field r))" and
   1.310 +         ****: "a \<in> Field r"
   1.311 +  (* Preliminary facts *)
   1.312 +  have Well: "wo_rel r"
   1.313 +  using WELL wo_rel_def[of r] by simp
   1.314 +  hence Refl: "Refl r"
   1.315 +  using wo_rel.REFL[of r] by simp
   1.316 +  have Total: "Total r"
   1.317 +  using Well wo_rel.TOTAL[of r] by simp
   1.318 +  have Well': "wo_rel r'"
   1.319 +  using WELL' wo_rel_def[of r'] by simp
   1.320 +  hence Antisym': "antisym r'"
   1.321 +  using wo_rel.ANTISYM[of r'] by simp
   1.322 +  have "(a,a) \<in> r"
   1.323 +  using **** Well wo_rel.REFL[of r]
   1.324 +        refl_on_def[of _ r] by auto
   1.325 +  hence "(f a, f a) \<in> r'"
   1.326 +  using ** by(auto simp add: compat_def)
   1.327 +  hence 0: "f a \<in> Field r'"
   1.328 +  unfolding Field_def by auto
   1.329 +  have "f a \<in> f`(Field r)"
   1.330 +  using **** by auto
   1.331 +  hence 2: "under r' (f a) \<le> f`(Field r)"
   1.332 +  using Well' *** wo_rel.ofilter_def[of r' "f`(Field r)"] by fastforce
   1.333 +  (* Main proof *)
   1.334 +  show "bij_betw f (under r a) (under r' (f a))"
   1.335 +  proof(unfold bij_betw_def, auto)
   1.336 +    show  "inj_on f (under r a)"
   1.337 +    using * by (metis (no_types) under_Field subset_inj_on)
   1.338 +  next
   1.339 +    fix b assume "b \<in> under r a"
   1.340 +    thus "f b \<in> under r' (f a)"
   1.341 +    unfolding under_def using **
   1.342 +    by (auto simp add: compat_def)
   1.343 +  next
   1.344 +    fix b' assume *****: "b' \<in> under r' (f a)"
   1.345 +    hence "b' \<in> f`(Field r)"
   1.346 +    using 2 by auto
   1.347 +    with Field_def[of r] obtain b where
   1.348 +    3: "b \<in> Field r" and 4: "b' = f b" by auto
   1.349 +    have "(b,a): r"
   1.350 +    proof-
   1.351 +      {assume "(a,b) \<in> r"
   1.352 +       with ** 4 have "(f a, b'): r'"
   1.353 +       by (auto simp add: compat_def)
   1.354 +       with ***** Antisym' have "f a = b'"
   1.355 +       by(auto simp add: under_def antisym_def)
   1.356 +       with 3 **** 4 * have "a = b"
   1.357 +       by(auto simp add: inj_on_def)
   1.358 +      }
   1.359 +      moreover
   1.360 +      {assume "a = b"
   1.361 +       hence "(b,a) \<in> r" using Refl **** 3
   1.362 +       by (auto simp add: refl_on_def)
   1.363 +      }
   1.364 +      ultimately
   1.365 +      show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
   1.366 +    qed
   1.367 +    with 4 show  "b' \<in> f`(under r a)"
   1.368 +    unfolding under_def by auto
   1.369 +  qed
   1.370 +qed
   1.371 +
   1.372 +
   1.373 +lemma inv_into_ofilter_embed:
   1.374 +assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
   1.375 +        BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
   1.376 +        IMAGE: "f ` A = Field r'"
   1.377 +shows "embed r' r (inv_into A f)"
   1.378 +proof-
   1.379 +  (* Preliminary facts *)
   1.380 +  have Well: "wo_rel r"
   1.381 +  using WELL wo_rel_def[of r] by simp
   1.382 +  have Refl: "Refl r"
   1.383 +  using Well wo_rel.REFL[of r] by simp
   1.384 +  have Total: "Total r"
   1.385 +  using Well wo_rel.TOTAL[of r] by simp
   1.386 +  (* Main proof *)
   1.387 +  have 1: "bij_betw f A (Field r')"
   1.388 +  proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
   1.389 +    fix b1 b2
   1.390 +    assume *: "b1 \<in> A" and **: "b2 \<in> A" and
   1.391 +           ***: "f b1 = f b2"
   1.392 +    have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"
   1.393 +    using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
   1.394 +    moreover
   1.395 +    {assume "(b1,b2) \<in> r"
   1.396 +     hence "b1 \<in> under r b2 \<and> b2 \<in> under r b2"
   1.397 +     unfolding under_def using 11 Refl
   1.398 +     by (auto simp add: refl_on_def)
   1.399 +     hence "b1 = b2" using BIJ * ** ***
   1.400 +     by (simp add: bij_betw_def inj_on_def)
   1.401 +    }
   1.402 +    moreover
   1.403 +     {assume "(b2,b1) \<in> r"
   1.404 +     hence "b1 \<in> under r b1 \<and> b2 \<in> under r b1"
   1.405 +     unfolding under_def using 11 Refl
   1.406 +     by (auto simp add: refl_on_def)
   1.407 +     hence "b1 = b2" using BIJ * ** ***
   1.408 +     by (simp add: bij_betw_def inj_on_def)
   1.409 +    }
   1.410 +    ultimately
   1.411 +    show "b1 = b2"
   1.412 +    using Total by (auto simp add: total_on_def)
   1.413 +  qed
   1.414 +  (*  *)
   1.415 +  let ?f' = "(inv_into A f)"
   1.416 +  (*  *)
   1.417 +  have 2: "\<forall>b \<in> A. bij_betw ?f' (under r' (f b)) (under r b)"
   1.418 +  proof(clarify)
   1.419 +    fix b assume *: "b \<in> A"
   1.420 +    hence "under r b \<le> A"
   1.421 +    using Well OF by(auto simp add: wo_rel.ofilter_def)
   1.422 +    moreover
   1.423 +    have "f ` (under r b) = under r' (f b)"
   1.424 +    using * BIJ by (auto simp add: bij_betw_def)
   1.425 +    ultimately
   1.426 +    show "bij_betw ?f' (under r' (f b)) (under r b)"
   1.427 +    using 1 by (auto simp add: bij_betw_inv_into_subset)
   1.428 +  qed
   1.429 +  (*  *)
   1.430 +  have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (under r' b') (under r (?f' b'))"
   1.431 +  proof(clarify)
   1.432 +    fix b' assume *: "b' \<in> Field r'"
   1.433 +    have "b' = f (?f' b')" using * 1
   1.434 +    by (auto simp add: bij_betw_inv_into_right)
   1.435 +    moreover
   1.436 +    {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force
   1.437 +     hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
   1.438 +     with 31 have "?f' b' \<in> A" by auto
   1.439 +    }
   1.440 +    ultimately
   1.441 +    show  "bij_betw ?f' (under r' b') (under r (?f' b'))"
   1.442 +    using 2 by auto
   1.443 +  qed
   1.444 +  (*  *)
   1.445 +  thus ?thesis unfolding embed_def .
   1.446 +qed
   1.447 +
   1.448 +
   1.449 +lemma inv_into_underS_embed:
   1.450 +assumes WELL: "Well_order r" and
   1.451 +        BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
   1.452 +        IN: "a \<in> Field r" and
   1.453 +        IMAGE: "f ` (underS r a) = Field r'"
   1.454 +shows "embed r' r (inv_into (underS r a) f)"
   1.455 +using assms
   1.456 +by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
   1.457 +
   1.458 +
   1.459 +lemma inv_into_Field_embed:
   1.460 +assumes WELL: "Well_order r" and EMB: "embed r r' f" and
   1.461 +        IMAGE: "Field r' \<le> f ` (Field r)"
   1.462 +shows "embed r' r (inv_into (Field r) f)"
   1.463 +proof-
   1.464 +  have "(\<forall>b \<in> Field r. bij_betw f (under r b) (under r' (f b)))"
   1.465 +  using EMB by (auto simp add: embed_def)
   1.466 +  moreover
   1.467 +  have "f ` (Field r) \<le> Field r'"
   1.468 +  using EMB WELL by (auto simp add: embed_Field)
   1.469 +  ultimately
   1.470 +  show ?thesis using assms
   1.471 +  by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
   1.472 +qed
   1.473 +
   1.474 +
   1.475 +lemma inv_into_Field_embed_bij_betw:
   1.476 +assumes WELL: "Well_order r" and
   1.477 +        EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
   1.478 +shows "embed r' r (inv_into (Field r) f)"
   1.479 +proof-
   1.480 +  have "Field r' \<le> f ` (Field r)"
   1.481 +  using BIJ by (auto simp add: bij_betw_def)
   1.482 +  thus ?thesis using assms
   1.483 +  by(auto simp add: inv_into_Field_embed)
   1.484 +qed
   1.485 +
   1.486 +
   1.487 +
   1.488 +
   1.489 +
   1.490 +subsection {* Given any two well-orders, one can be embedded in the other *}
   1.491 +
   1.492 +
   1.493 +text{* Here is an overview of the proof of of this fact, stated in theorem
   1.494 +@{text "wellorders_totally_ordered"}:
   1.495 +
   1.496 +   Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}.
   1.497 +   Attempt to define an embedding @{text "f::'a \<Rightarrow> 'a'"} from @{text "r"} to @{text "r'"} in the
   1.498 +   natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller
   1.499 +   than @{text "Field r'"}), but also record, at the recursive step, in a function
   1.500 +   @{text "g::'a \<Rightarrow> bool"}, the extra information of whether @{text "Field r'"}
   1.501 +   gets exhausted or not.
   1.502 +
   1.503 +   If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller
   1.504 +   and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"}
   1.505 +   (lemma @{text "wellorders_totally_ordered_aux"}).
   1.506 +
   1.507 +   Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of
   1.508 +   (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"}
   1.509 +   (lemma @{text "wellorders_totally_ordered_aux2"}).
   1.510 +*}
   1.511 +
   1.512 +
   1.513 +lemma wellorders_totally_ordered_aux:
   1.514 +fixes r ::"'a rel"  and r'::"'a' rel" and
   1.515 +      f :: "'a \<Rightarrow> 'a'" and a::'a
   1.516 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
   1.517 +        IH: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
   1.518 +        NOT: "f ` (underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(underS r a))"
   1.519 +shows "bij_betw f (under r a) (under r' (f a))"
   1.520 +proof-
   1.521 +  (* Preliminary facts *)
   1.522 +  have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   1.523 +  hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   1.524 +  have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   1.525 +  have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   1.526 +  have OF: "wo_rel.ofilter r (underS r a)"
   1.527 +  by (auto simp add: Well wo_rel.underS_ofilter)
   1.528 +  hence UN: "underS r a = (\<Union>  b \<in> underS r a. under r b)"
   1.529 +  using Well wo_rel.ofilter_under_UNION[of r "underS r a"] by blast
   1.530 +  (* Gather facts about elements of underS r a *)
   1.531 +  {fix b assume *: "b \<in> underS r a"
   1.532 +   hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
   1.533 +   have t1: "b \<in> Field r"
   1.534 +   using * underS_Field[of r a] by auto
   1.535 +   have t2: "f`(under r b) = under r' (f b)"
   1.536 +   using IH * by (auto simp add: bij_betw_def)
   1.537 +   hence t3: "wo_rel.ofilter r' (f`(under r b))"
   1.538 +   using Well' by (auto simp add: wo_rel.under_ofilter)
   1.539 +   have "f`(under r b) \<le> Field r'"
   1.540 +   using t2 by (auto simp add: under_Field)
   1.541 +   moreover
   1.542 +   have "b \<in> under r b"
   1.543 +   using t1 by(auto simp add: Refl Refl_under_in)
   1.544 +   ultimately
   1.545 +   have t4:  "f b \<in> Field r'" by auto
   1.546 +   have "f`(under r b) = under r' (f b) \<and>
   1.547 +         wo_rel.ofilter r' (f`(under r b)) \<and>
   1.548 +         f b \<in> Field r'"
   1.549 +   using t2 t3 t4 by auto
   1.550 +  }
   1.551 +  hence bFact:
   1.552 +  "\<forall>b \<in> underS r a. f`(under r b) = under r' (f b) \<and>
   1.553 +                       wo_rel.ofilter r' (f`(under r b)) \<and>
   1.554 +                       f b \<in> Field r'" by blast
   1.555 +  (*  *)
   1.556 +  have subField: "f`(underS r a) \<le> Field r'"
   1.557 +  using bFact by blast
   1.558 +  (*  *)
   1.559 +  have OF': "wo_rel.ofilter r' (f`(underS r a))"
   1.560 +  proof-
   1.561 +    have "f`(underS r a) = f`(\<Union>  b \<in> underS r a. under r b)"
   1.562 +    using UN by auto
   1.563 +    also have "\<dots> = (\<Union>  b \<in> underS r a. f`(under r b))" by blast
   1.564 +    also have "\<dots> = (\<Union>  b \<in> underS r a. (under r' (f b)))"
   1.565 +    using bFact by auto
   1.566 +    finally
   1.567 +    have "f`(underS r a) = (\<Union>  b \<in> underS r a. (under r' (f b)))" .
   1.568 +    thus ?thesis
   1.569 +    using Well' bFact
   1.570 +          wo_rel.ofilter_UNION[of r' "underS r a" "\<lambda> b. under r' (f b)"] by fastforce
   1.571 +  qed
   1.572 +  (*  *)
   1.573 +  have "f`(underS r a) \<union> AboveS r' (f`(underS r a)) = Field r'"
   1.574 +  using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
   1.575 +  hence NE: "AboveS r' (f`(underS r a)) \<noteq> {}"
   1.576 +  using subField NOT by blast
   1.577 +  (* Main proof *)
   1.578 +  have INCL1: "f`(underS r a) \<le> underS r' (f a) "
   1.579 +  proof(auto)
   1.580 +    fix b assume *: "b \<in> underS r a"
   1.581 +    have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
   1.582 +    using subField Well' SUC NE *
   1.583 +          wo_rel.suc_greater[of r' "f`(underS r a)" "f b"] by force
   1.584 +    thus "f b \<in> underS r' (f a)"
   1.585 +    unfolding underS_def by simp
   1.586 +  qed
   1.587 +  (*  *)
   1.588 +  have INCL2: "underS r' (f a) \<le> f`(underS r a)"
   1.589 +  proof
   1.590 +    fix b' assume "b' \<in> underS r' (f a)"
   1.591 +    hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
   1.592 +    unfolding underS_def by simp
   1.593 +    thus "b' \<in> f`(underS r a)"
   1.594 +    using Well' SUC NE OF'
   1.595 +          wo_rel.suc_ofilter_in[of r' "f ` underS r a" b'] by auto
   1.596 +  qed
   1.597 +  (*  *)
   1.598 +  have INJ: "inj_on f (underS r a)"
   1.599 +  proof-
   1.600 +    have "\<forall>b \<in> underS r a. inj_on f (under r b)"
   1.601 +    using IH by (auto simp add: bij_betw_def)
   1.602 +    moreover
   1.603 +    have "\<forall>b. wo_rel.ofilter r (under r b)"
   1.604 +    using Well by (auto simp add: wo_rel.under_ofilter)
   1.605 +    ultimately show  ?thesis
   1.606 +    using WELL bFact UN
   1.607 +          UNION_inj_on_ofilter[of r "underS r a" "\<lambda>b. under r b" f]
   1.608 +    by auto
   1.609 +  qed
   1.610 +  (*  *)
   1.611 +  have BIJ: "bij_betw f (underS r a) (underS r' (f a))"
   1.612 +  unfolding bij_betw_def
   1.613 +  using INJ INCL1 INCL2 by auto
   1.614 +  (*  *)
   1.615 +  have "f a \<in> Field r'"
   1.616 +  using Well' subField NE SUC
   1.617 +  by (auto simp add: wo_rel.suc_inField)
   1.618 +  thus ?thesis
   1.619 +  using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
   1.620 +qed
   1.621 +
   1.622 +
   1.623 +lemma wellorders_totally_ordered_aux2:
   1.624 +fixes r ::"'a rel"  and r'::"'a' rel" and
   1.625 +      f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
   1.626 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.627 +MAIN1:
   1.628 +  "\<And> a. (False \<notin> g`(underS r a) \<and> f`(underS r a) \<noteq> Field r'
   1.629 +          \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True)
   1.630 +         \<and>
   1.631 +         (\<not>(False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')
   1.632 +          \<longrightarrow> g a = False)" and
   1.633 +MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
   1.634 +              bij_betw f (under r a) (under r' (f a))" and
   1.635 +Case: "a \<in> Field r \<and> False \<in> g`(under r a)"
   1.636 +shows "\<exists>f'. embed r' r f'"
   1.637 +proof-
   1.638 +  have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   1.639 +  hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   1.640 +  have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   1.641 +  have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
   1.642 +  have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   1.643 +  (*  *)
   1.644 +  have 0: "under r a = underS r a \<union> {a}"
   1.645 +  using Refl Case by(auto simp add: Refl_under_underS)
   1.646 +  (*  *)
   1.647 +  have 1: "g a = False"
   1.648 +  proof-
   1.649 +    {assume "g a \<noteq> False"
   1.650 +     with 0 Case have "False \<in> g`(underS r a)" by blast
   1.651 +     with MAIN1 have "g a = False" by blast}
   1.652 +    thus ?thesis by blast
   1.653 +  qed
   1.654 +  let ?A = "{a \<in> Field r. g a = False}"
   1.655 +  let ?a = "(wo_rel.minim r ?A)"
   1.656 +  (*  *)
   1.657 +  have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
   1.658 +  (*  *)
   1.659 +  have 3: "False \<notin> g`(underS r ?a)"
   1.660 +  proof
   1.661 +    assume "False \<in> g`(underS r ?a)"
   1.662 +    then obtain b where "b \<in> underS r ?a" and 31: "g b = False" by auto
   1.663 +    hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
   1.664 +    by (auto simp add: underS_def)
   1.665 +    hence "b \<in> Field r" unfolding Field_def by auto
   1.666 +    with 31 have "b \<in> ?A" by auto
   1.667 +    hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
   1.668 +    (* again: why worked without type annotations? *)
   1.669 +    with 32 Antisym show False
   1.670 +    by (auto simp add: antisym_def)
   1.671 +  qed
   1.672 +  have temp: "?a \<in> ?A"
   1.673 +  using Well 2 wo_rel.minim_in[of r ?A] by auto
   1.674 +  hence 4: "?a \<in> Field r" by auto
   1.675 +  (*   *)
   1.676 +  have 5: "g ?a = False" using temp by blast
   1.677 +  (*  *)
   1.678 +  have 6: "f`(underS r ?a) = Field r'"
   1.679 +  using MAIN1[of ?a] 3 5 by blast
   1.680 +  (*  *)
   1.681 +  have 7: "\<forall>b \<in> underS r ?a. bij_betw f (under r b) (under r' (f b))"
   1.682 +  proof
   1.683 +    fix b assume as: "b \<in> underS r ?a"
   1.684 +    moreover
   1.685 +    have "wo_rel.ofilter r (underS r ?a)"
   1.686 +    using Well by (auto simp add: wo_rel.underS_ofilter)
   1.687 +    ultimately
   1.688 +    have "False \<notin> g`(under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
   1.689 +    moreover have "b \<in> Field r"
   1.690 +    unfolding Field_def using as by (auto simp add: underS_def)
   1.691 +    ultimately
   1.692 +    show "bij_betw f (under r b) (under r' (f b))"
   1.693 +    using MAIN2 by auto
   1.694 +  qed
   1.695 +  (*  *)
   1.696 +  have "embed r' r (inv_into (underS r ?a) f)"
   1.697 +  using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
   1.698 +  thus ?thesis
   1.699 +  unfolding embed_def by blast
   1.700 +qed
   1.701 +
   1.702 +
   1.703 +theorem wellorders_totally_ordered:
   1.704 +fixes r ::"'a rel"  and r'::"'a' rel"
   1.705 +assumes WELL: "Well_order r" and WELL': "Well_order r'"
   1.706 +shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
   1.707 +proof-
   1.708 +  (* Preliminary facts *)
   1.709 +  have Well: "wo_rel r" using WELL unfolding wo_rel_def .
   1.710 +  hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
   1.711 +  have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
   1.712 +  have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
   1.713 +  (* Main proof *)
   1.714 +  obtain H where H_def: "H =
   1.715 +  (\<lambda>h a. if False \<notin> (snd o h)`(underS r a) \<and> (fst o h)`(underS r a) \<noteq> Field r'
   1.716 +                then (wo_rel.suc r' ((fst o h)`(underS r a)), True)
   1.717 +                else (undefined, False))" by blast
   1.718 +  have Adm: "wo_rel.adm_wo r H"
   1.719 +  using Well
   1.720 +  proof(unfold wo_rel.adm_wo_def, clarify)
   1.721 +    fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
   1.722 +    assume "\<forall>y\<in>underS r x. h1 y = h2 y"
   1.723 +    hence "\<forall>y\<in>underS r x. (fst o h1) y = (fst o h2) y \<and>
   1.724 +                          (snd o h1) y = (snd o h2) y" by auto
   1.725 +    hence "(fst o h1)`(underS r x) = (fst o h2)`(underS r x) \<and>
   1.726 +           (snd o h1)`(underS r x) = (snd o h2)`(underS r x)"
   1.727 +      by (auto simp add: image_def)
   1.728 +    thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
   1.729 +  qed
   1.730 +  (* More constant definitions:  *)
   1.731 +  obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
   1.732 +  where h_def: "h = wo_rel.worec r H" and
   1.733 +        f_def: "f = fst o h" and g_def: "g = snd o h" by blast
   1.734 +  obtain test where test_def:
   1.735 +  "test = (\<lambda> a. False \<notin> (g`(underS r a)) \<and> f`(underS r a) \<noteq> Field r')" by blast
   1.736 +  (*  *)
   1.737 +  have *: "\<And> a. h a  = H h a"
   1.738 +  using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
   1.739 +  have Main1:
   1.740 +  "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
   1.741 +         (\<not>(test a) \<longrightarrow> g a = False)"
   1.742 +  proof-  (* How can I prove this withou fixing a? *)
   1.743 +    fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(underS r a)) \<and> g a = True) \<and>
   1.744 +                (\<not>(test a) \<longrightarrow> g a = False)"
   1.745 +    using *[of a] test_def f_def g_def H_def by auto
   1.746 +  qed
   1.747 +  (*  *)
   1.748 +  let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(under r a) \<longrightarrow>
   1.749 +                   bij_betw f (under r a) (under r' (f a))"
   1.750 +  have Main2: "\<And> a. ?phi a"
   1.751 +  proof-
   1.752 +    fix a show "?phi a"
   1.753 +    proof(rule wo_rel.well_order_induct[of r ?phi],
   1.754 +          simp only: Well, clarify)
   1.755 +      fix a
   1.756 +      assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
   1.757 +             *: "a \<in> Field r" and
   1.758 +             **: "False \<notin> g`(under r a)"
   1.759 +      have 1: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))"
   1.760 +      proof(clarify)
   1.761 +        fix b assume ***: "b \<in> underS r a"
   1.762 +        hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding underS_def by auto
   1.763 +        moreover have "b \<in> Field r"
   1.764 +        using *** underS_Field[of r a] by auto
   1.765 +        moreover have "False \<notin> g`(under r b)"
   1.766 +        using 0 ** Trans under_incr[of r b a] by auto
   1.767 +        ultimately show "bij_betw f (under r b) (under r' (f b))"
   1.768 +        using IH by auto
   1.769 +      qed
   1.770 +      (*  *)
   1.771 +      have 21: "False \<notin> g`(underS r a)"
   1.772 +      using ** underS_subset_under[of r a] by auto
   1.773 +      have 22: "g`(under r a) \<le> {True}" using ** by auto
   1.774 +      moreover have 23: "a \<in> under r a"
   1.775 +      using Refl * by (auto simp add: Refl_under_in)
   1.776 +      ultimately have 24: "g a = True" by blast
   1.777 +      have 2: "f`(underS r a) \<noteq> Field r'"
   1.778 +      proof
   1.779 +        assume "f`(underS r a) = Field r'"
   1.780 +        hence "g a = False" using Main1 test_def by blast
   1.781 +        with 24 show False using ** by blast
   1.782 +      qed
   1.783 +      (*  *)
   1.784 +      have 3: "f a = wo_rel.suc r' (f`(underS r a))"
   1.785 +      using 21 2 Main1 test_def by blast
   1.786 +      (*  *)
   1.787 +      show "bij_betw f (under r a) (under r' (f a))"
   1.788 +      using WELL  WELL' 1 2 3 *
   1.789 +            wellorders_totally_ordered_aux[of r r' a f] by auto
   1.790 +    qed
   1.791 +  qed
   1.792 +  (*  *)
   1.793 +  let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(under r a))"
   1.794 +  show ?thesis
   1.795 +  proof(cases "\<exists>a. ?chi a")
   1.796 +    assume "\<not> (\<exists>a. ?chi a)"
   1.797 +    hence "\<forall>a \<in> Field r.  bij_betw f (under r a) (under r' (f a))"
   1.798 +    using Main2 by blast
   1.799 +    thus ?thesis unfolding embed_def by blast
   1.800 +  next
   1.801 +    assume "\<exists>a. ?chi a"
   1.802 +    then obtain a where "?chi a" by blast
   1.803 +    hence "\<exists>f'. embed r' r f'"
   1.804 +    using wellorders_totally_ordered_aux2[of r r' g f a]
   1.805 +          WELL WELL' Main1 Main2 test_def by fast
   1.806 +    thus ?thesis by blast
   1.807 +  qed
   1.808 +qed
   1.809 +
   1.810 +
   1.811 +subsection {* Uniqueness of embeddings  *}
   1.812 +
   1.813 +
   1.814 +text{* Here we show a fact complementary to the one from the previous subsection -- namely,
   1.815 +that between any two well-orders there is {\em at most} one embedding, and is the one
   1.816 +definable by the expected well-order recursive equation.  As a consequence, any two
   1.817 +embeddings of opposite directions are mutually inverse. *}
   1.818 +
   1.819 +
   1.820 +lemma embed_determined:
   1.821 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.822 +        EMB: "embed r r' f" and IN: "a \<in> Field r"
   1.823 +shows "f a = wo_rel.suc r' (f`(underS r a))"
   1.824 +proof-
   1.825 +  have "bij_betw f (underS r a) (underS r' (f a))"
   1.826 +  using assms by (auto simp add: embed_underS)
   1.827 +  hence "f`(underS r a) = underS r' (f a)"
   1.828 +  by (auto simp add: bij_betw_def)
   1.829 +  moreover
   1.830 +  {have "f a \<in> Field r'" using IN
   1.831 +   using EMB WELL embed_Field[of r r' f] by auto
   1.832 +   hence "f a = wo_rel.suc r' (underS r' (f a))"
   1.833 +   using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
   1.834 +  }
   1.835 +  ultimately show ?thesis by simp
   1.836 +qed
   1.837 +
   1.838 +
   1.839 +lemma embed_unique:
   1.840 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.841 +        EMBf: "embed r r' f" and EMBg: "embed r r' g"
   1.842 +shows "a \<in> Field r \<longrightarrow> f a = g a"
   1.843 +proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)
   1.844 +  fix a
   1.845 +  assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
   1.846 +         *: "a \<in> Field r"
   1.847 +  hence "\<forall>b \<in> underS r a. f b = g b"
   1.848 +  unfolding underS_def by (auto simp add: Field_def)
   1.849 +  hence "f`(underS r a) = g`(underS r a)" by force
   1.850 +  thus "f a = g a"
   1.851 +  using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
   1.852 +qed
   1.853 +
   1.854 +
   1.855 +lemma embed_bothWays_inverse:
   1.856 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.857 +        EMB: "embed r r' f" and EMB': "embed r' r f'"
   1.858 +shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
   1.859 +proof-
   1.860 +  have "embed r r (f' o f)" using assms
   1.861 +  by(auto simp add: comp_embed)
   1.862 +  moreover have "embed r r id" using assms
   1.863 +  by (auto simp add: id_embed)
   1.864 +  ultimately have "\<forall>a \<in> Field r. f'(f a) = a"
   1.865 +  using assms embed_unique[of r r "f' o f" id] id_def by auto
   1.866 +  moreover
   1.867 +  {have "embed r' r' (f o f')" using assms
   1.868 +   by(auto simp add: comp_embed)
   1.869 +   moreover have "embed r' r' id" using assms
   1.870 +   by (auto simp add: id_embed)
   1.871 +   ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
   1.872 +   using assms embed_unique[of r' r' "f o f'" id] id_def by auto
   1.873 +  }
   1.874 +  ultimately show ?thesis by blast
   1.875 +qed
   1.876 +
   1.877 +
   1.878 +lemma embed_bothWays_bij_betw:
   1.879 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.880 +        EMB: "embed r r' f" and EMB': "embed r' r g"
   1.881 +shows "bij_betw f (Field r) (Field r')"
   1.882 +proof-
   1.883 +  let ?A = "Field r"  let ?A' = "Field r'"
   1.884 +  have "embed r r (g o f) \<and> embed r' r' (f o g)"
   1.885 +  using assms by (auto simp add: comp_embed)
   1.886 +  hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"
   1.887 +  using WELL id_embed[of r] embed_unique[of r r "g o f" id]
   1.888 +        WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id]
   1.889 +        id_def by auto
   1.890 +  have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"
   1.891 +  using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
   1.892 +  (*  *)
   1.893 +  show ?thesis
   1.894 +  proof(unfold bij_betw_def inj_on_def, auto simp add: 2)
   1.895 +    fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"
   1.896 +    have "a = g(f a) \<and> b = g(f b)" using * 1 by auto
   1.897 +    with ** show "a = b" by auto
   1.898 +  next
   1.899 +    fix a' assume *: "a' \<in> ?A'"
   1.900 +    hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto
   1.901 +    thus "a' \<in> f ` ?A" by force
   1.902 +  qed
   1.903 +qed
   1.904 +
   1.905 +
   1.906 +lemma embed_bothWays_iso:
   1.907 +assumes WELL: "Well_order r"  and WELL': "Well_order r'" and
   1.908 +        EMB: "embed r r' f" and EMB': "embed r' r g"
   1.909 +shows "iso r r' f"
   1.910 +unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
   1.911 +
   1.912 +
   1.913 +subsection {* More properties of embeddings, strict embeddings and isomorphisms  *}
   1.914 +
   1.915 +
   1.916 +lemma embed_bothWays_Field_bij_betw:
   1.917 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.918 +        EMB: "embed r r' f" and EMB': "embed r' r f'"
   1.919 +shows "bij_betw f (Field r) (Field r')"
   1.920 +proof-
   1.921 +  have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
   1.922 +  using assms by (auto simp add: embed_bothWays_inverse)
   1.923 +  moreover
   1.924 +  have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r"
   1.925 +  using assms by (auto simp add: embed_Field)
   1.926 +  ultimately
   1.927 +  show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
   1.928 +qed
   1.929 +
   1.930 +
   1.931 +lemma embedS_comp_embed:
   1.932 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.933 +        and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
   1.934 +shows "embedS r r'' (f' o f)"
   1.935 +proof-
   1.936 +  let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"
   1.937 +  have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))"
   1.938 +  using EMB by (auto simp add: embedS_def)
   1.939 +  hence 2: "embed r r'' ?g"
   1.940 +  using WELL EMB' comp_embed[of r r' f r'' f'] by auto
   1.941 +  moreover
   1.942 +  {assume "bij_betw ?g (Field r) (Field r'')"
   1.943 +   hence "embed r'' r ?h" using 2 WELL
   1.944 +   by (auto simp add: inv_into_Field_embed_bij_betw)
   1.945 +   hence "embed r' r (?h o f')" using WELL' EMB'
   1.946 +   by (auto simp add: comp_embed)
   1.947 +   hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1
   1.948 +   by (auto simp add: embed_bothWays_Field_bij_betw)
   1.949 +   with 1 have False by blast
   1.950 +  }
   1.951 +  ultimately show ?thesis unfolding embedS_def by auto
   1.952 +qed
   1.953 +
   1.954 +
   1.955 +lemma embed_comp_embedS:
   1.956 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.957 +        and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
   1.958 +shows "embedS r r'' (f' o f)"
   1.959 +proof-
   1.960 +  let ?g = "(f' o f)"  let ?h = "inv_into (Field r) ?g"
   1.961 +  have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))"
   1.962 +  using EMB' by (auto simp add: embedS_def)
   1.963 +  hence 2: "embed r r'' ?g"
   1.964 +  using WELL EMB comp_embed[of r r' f r'' f'] by auto
   1.965 +  moreover
   1.966 +  {assume "bij_betw ?g (Field r) (Field r'')"
   1.967 +   hence "embed r'' r ?h" using 2 WELL
   1.968 +   by (auto simp add: inv_into_Field_embed_bij_betw)
   1.969 +   hence "embed r'' r' (f o ?h)" using WELL'' EMB
   1.970 +   by (auto simp add: comp_embed)
   1.971 +   hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1
   1.972 +   by (auto simp add: embed_bothWays_Field_bij_betw)
   1.973 +   with 1 have False by blast
   1.974 +  }
   1.975 +  ultimately show ?thesis unfolding embedS_def by auto
   1.976 +qed
   1.977 +
   1.978 +
   1.979 +lemma embed_comp_iso:
   1.980 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.981 +        and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"
   1.982 +shows "embed r r'' (f' o f)"
   1.983 +using assms unfolding iso_def
   1.984 +by (auto simp add: comp_embed)
   1.985 +
   1.986 +
   1.987 +lemma iso_comp_embed:
   1.988 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.989 +        and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"
   1.990 +shows "embed r r'' (f' o f)"
   1.991 +using assms unfolding iso_def
   1.992 +by (auto simp add: comp_embed)
   1.993 +
   1.994 +
   1.995 +lemma embedS_comp_iso:
   1.996 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.997 +        and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
   1.998 +shows "embedS r r'' (f' o f)"
   1.999 +using assms unfolding iso_def
  1.1000 +by (auto simp add: embedS_comp_embed)
  1.1001 +
  1.1002 +
  1.1003 +lemma iso_comp_embedS:
  1.1004 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
  1.1005 +        and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
  1.1006 +shows "embedS r r'' (f' o f)"
  1.1007 +using assms unfolding iso_def  using embed_comp_embedS
  1.1008 +by (auto simp add: embed_comp_embedS)
  1.1009 +
  1.1010 +
  1.1011 +lemma embedS_Field:
  1.1012 +assumes WELL: "Well_order r" and EMB: "embedS r r' f"
  1.1013 +shows "f ` (Field r) < Field r'"
  1.1014 +proof-
  1.1015 +  have "f`(Field r) \<le> Field r'" using assms
  1.1016 +  by (auto simp add: embed_Field embedS_def)
  1.1017 +  moreover
  1.1018 +  {have "inj_on f (Field r)" using assms
  1.1019 +   by (auto simp add: embedS_def embed_inj_on)
  1.1020 +   hence "f`(Field r) \<noteq> Field r'" using EMB
  1.1021 +   by (auto simp add: embedS_def bij_betw_def)
  1.1022 +  }
  1.1023 +  ultimately show ?thesis by blast
  1.1024 +qed
  1.1025 +
  1.1026 +
  1.1027 +lemma embedS_iff:
  1.1028 +assumes WELL: "Well_order r" and ISO: "embed r r' f"
  1.1029 +shows "embedS r r' f = (f ` (Field r) < Field r')"
  1.1030 +proof
  1.1031 +  assume "embedS r r' f"
  1.1032 +  thus "f ` Field r \<subset> Field r'"
  1.1033 +  using WELL by (auto simp add: embedS_Field)
  1.1034 +next
  1.1035 +  assume "f ` Field r \<subset> Field r'"
  1.1036 +  hence "\<not> bij_betw f (Field r) (Field r')"
  1.1037 +  unfolding bij_betw_def by blast
  1.1038 +  thus "embedS r r' f" unfolding embedS_def
  1.1039 +  using ISO by auto
  1.1040 +qed
  1.1041 +
  1.1042 +
  1.1043 +lemma iso_Field:
  1.1044 +"iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
  1.1045 +using assms by (auto simp add: iso_def bij_betw_def)
  1.1046 +
  1.1047 +
  1.1048 +lemma iso_iff:
  1.1049 +assumes "Well_order r"
  1.1050 +shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
  1.1051 +proof
  1.1052 +  assume "iso r r' f"
  1.1053 +  thus "embed r r' f \<and> f ` (Field r) = Field r'"
  1.1054 +  by (auto simp add: iso_Field iso_def)
  1.1055 +next
  1.1056 +  assume *: "embed r r' f \<and> f ` Field r = Field r'"
  1.1057 +  hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)
  1.1058 +  with * have "bij_betw f (Field r) (Field r')"
  1.1059 +  unfolding bij_betw_def by simp
  1.1060 +  with * show "iso r r' f" unfolding iso_def by auto
  1.1061 +qed
  1.1062 +
  1.1063 +
  1.1064 +lemma iso_iff2:
  1.1065 +assumes "Well_order r"
  1.1066 +shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
  1.1067 +                     (\<forall>a \<in> Field r. \<forall>b \<in> Field r.
  1.1068 +                         (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"
  1.1069 +using assms
  1.1070 +proof(auto simp add: iso_def)
  1.1071 +  fix a b
  1.1072 +  assume "embed r r' f"
  1.1073 +  hence "compat r r' f" using embed_compat[of r] by auto
  1.1074 +  moreover assume "(a,b) \<in> r"
  1.1075 +  ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto
  1.1076 +next
  1.1077 +  let ?f' = "inv_into (Field r) f"
  1.1078 +  assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"
  1.1079 +  hence "embed r' r ?f'" using assms
  1.1080 +  by (auto simp add: inv_into_Field_embed_bij_betw)
  1.1081 +  hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto
  1.1082 +  fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"
  1.1083 +  hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1
  1.1084 +  by (auto simp add: bij_betw_inv_into_left)
  1.1085 +  thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce
  1.1086 +next
  1.1087 +  assume *: "bij_betw f (Field r) (Field r')" and
  1.1088 +         **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
  1.1089 +  have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
  1.1090 +  by (auto simp add: under_Field)
  1.1091 +  have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
  1.1092 +  {fix a assume ***: "a \<in> Field r"
  1.1093 +   have "bij_betw f (under r a) (under r' (f a))"
  1.1094 +   proof(unfold bij_betw_def, auto)
  1.1095 +     show "inj_on f (under r a)"
  1.1096 +     using 1 2 by (metis subset_inj_on)
  1.1097 +   next
  1.1098 +     fix b assume "b \<in> under r a"
  1.1099 +     hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
  1.1100 +     unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
  1.1101 +     with 1 ** show "f b \<in> under r' (f a)"
  1.1102 +     unfolding under_def by auto
  1.1103 +   next
  1.1104 +     fix b' assume "b' \<in> under r' (f a)"
  1.1105 +     hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
  1.1106 +     hence "b' \<in> Field r'" unfolding Field_def by auto
  1.1107 +     with * obtain b where "b \<in> Field r \<and> f b = b'"
  1.1108 +     unfolding bij_betw_def by force
  1.1109 +     with 3 ** ***
  1.1110 +     show "b' \<in> f ` (under r a)" unfolding under_def by blast
  1.1111 +   qed
  1.1112 +  }
  1.1113 +  thus "embed r r' f" unfolding embed_def using * by auto
  1.1114 +qed
  1.1115 +
  1.1116 +
  1.1117 +lemma iso_iff3:
  1.1118 +assumes WELL: "Well_order r" and WELL': "Well_order r'"
  1.1119 +shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
  1.1120 +proof
  1.1121 +  assume "iso r r' f"
  1.1122 +  thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"
  1.1123 +  unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
  1.1124 +next
  1.1125 +  have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'
  1.1126 +  by (auto simp add: wo_rel_def)
  1.1127 +  assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"
  1.1128 +  thus "iso r r' f"
  1.1129 +  unfolding "compat_def" using assms
  1.1130 +  proof(auto simp add: iso_iff2)
  1.1131 +    fix a b assume **: "a \<in> Field r" "b \<in> Field r" and
  1.1132 +                  ***: "(f a, f b) \<in> r'"
  1.1133 +    {assume "(b,a) \<in> r \<or> b = a"
  1.1134 +     hence "(b,a): r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
  1.1135 +     hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
  1.1136 +     hence "f a = f b"
  1.1137 +     using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
  1.1138 +     hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
  1.1139 +     hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
  1.1140 +    }
  1.1141 +    thus "(a,b) \<in> r"
  1.1142 +    using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
  1.1143 +  qed
  1.1144 +qed
  1.1145 +
  1.1146 +
  1.1147 +
  1.1148 +end