1.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1146 +0,0 @@
1.4 -(* Title: HOL/Cardinals/Wellorder_Embedding_Base.thy
1.5 - Author: Andrei Popescu, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -Well-order embeddings (base).
1.9 -*)
1.10 -
1.11 -header {* Well-Order Embeddings (Base) *}
1.12 -
1.13 -theory Wellorder_Embedding_Base
1.14 -imports "~~/src/HOL/Library/Zorn" Fun_More_Base Wellorder_Relation_Base
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 (rel.underS r a) (rel.underS r' (f a))"
1.47 -shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
1.48 -proof-
1.49 - have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
1.50 - unfolding rel.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 "rel.under r a = rel.underS r a \<union> {a} \<and>
1.55 - rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
1.56 - using IN IN' by(auto simp add: rel.Refl_under_underS)
1.57 - }
1.58 - ultimately show ?thesis
1.59 - using BIJ notIn_Un_bij_betw[of a "rel.underS r a" f "rel.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 (rel.under r a) (rel.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> rel.under r a" using IN rel.Refl_under_in by fastforce
1.140 - hence "f a \<in> rel.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: rel.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 (rel.under r a) (rel.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' (rel.under r' (f a)) (rel.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) (rel.under r a) (rel.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> rel.under r' (f a)"
1.197 - hence "a \<in> Field r" using 0 by auto
1.198 - hence "bij_betw f (rel.under r a) (rel.under r' (f a))"
1.199 - using * EMB by (auto simp add: embed_def)
1.200 - hence "f`(rel.under r a) = rel.under r' (f a)"
1.201 - by (simp add: bij_betw_def)
1.202 - with ** image_def[of f "rel.under r a"] obtain b where
1.203 - 1: "b \<in> rel.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> rel.under r b"
1.231 - using * rel.under_def[of r] by simp
1.232 - hence "f a \<in> rel.under r' (f b)"
1.233 - using EMB embed_def[of r r' f]
1.234 - bij_betw_def[of f "rel.under r b" "rel.under r' (f b)"]
1.235 - image_def[of f "rel.under r b"] 1 by auto
1.236 - thus "(f a, f b) \<in> r'"
1.237 - by (auto simp add: rel.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> rel.under r b \<and> b \<in> rel.under r b"
1.259 - using Refl by(auto simp add: rel.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> rel.under r a \<and> b \<in> rel.under r a"
1.267 - using Refl by(auto simp add: rel.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 (rel.underS r a) (rel.underS r' (f a))"
1.282 -proof-
1.283 - have "bij_betw f (rel.under r a) (rel.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 "rel.under r a = rel.underS r a \<union> {a} \<and>
1.288 - rel.under r' (f a) = rel.underS r' (f a) \<union> {f a}"
1.289 - using assms by (auto simp add: order_on_defs rel.Refl_under_underS)
1.290 - }
1.291 - moreover
1.292 - {have "a \<notin> rel.underS r a \<and> f a \<notin> rel.underS r' (f a)"
1.293 - unfolding rel.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: "rel.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 (rel.under r a) (rel.under r' (f a))"
1.335 - proof(unfold bij_betw_def, auto)
1.336 - show "inj_on f (rel.under r a)"
1.337 - using *
1.338 - by (auto simp add: rel.under_Field subset_inj_on)
1.339 - next
1.340 - fix b assume "b \<in> rel.under r a"
1.341 - thus "f b \<in> rel.under r' (f a)"
1.342 - unfolding rel.under_def using **
1.343 - by (auto simp add: compat_def)
1.344 - next
1.345 - fix b' assume *****: "b' \<in> rel.under r' (f a)"
1.346 - hence "b' \<in> f`(Field r)"
1.347 - using 2 by auto
1.348 - with Field_def[of r] obtain b where
1.349 - 3: "b \<in> Field r" and 4: "b' = f b" by auto
1.350 - have "(b,a): r"
1.351 - proof-
1.352 - {assume "(a,b) \<in> r"
1.353 - with ** 4 have "(f a, b'): r'"
1.354 - by (auto simp add: compat_def)
1.355 - with ***** Antisym' have "f a = b'"
1.356 - by(auto simp add: rel.under_def antisym_def)
1.357 - with 3 **** 4 * have "a = b"
1.358 - by(auto simp add: inj_on_def)
1.359 - }
1.360 - moreover
1.361 - {assume "a = b"
1.362 - hence "(b,a) \<in> r" using Refl **** 3
1.363 - by (auto simp add: refl_on_def)
1.364 - }
1.365 - ultimately
1.366 - show ?thesis using Total **** 3 by (fastforce simp add: total_on_def)
1.367 - qed
1.368 - with 4 show "b' \<in> f`(rel.under r a)"
1.369 - unfolding rel.under_def by auto
1.370 - qed
1.371 -qed
1.372 -
1.373 -
1.374 -lemma inv_into_ofilter_embed:
1.375 -assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
1.376 - BIJ: "\<forall>b \<in> A. bij_betw f (rel.under r b) (rel.under r' (f b))" and
1.377 - IMAGE: "f ` A = Field r'"
1.378 -shows "embed r' r (inv_into A f)"
1.379 -proof-
1.380 - (* Preliminary facts *)
1.381 - have Well: "wo_rel r"
1.382 - using WELL wo_rel_def[of r] by simp
1.383 - have Refl: "Refl r"
1.384 - using Well wo_rel.REFL[of r] by simp
1.385 - have Total: "Total r"
1.386 - using Well wo_rel.TOTAL[of r] by simp
1.387 - (* Main proof *)
1.388 - have 1: "bij_betw f A (Field r')"
1.389 - proof(unfold bij_betw_def inj_on_def, auto simp add: IMAGE)
1.390 - fix b1 b2
1.391 - assume *: "b1 \<in> A" and **: "b2 \<in> A" and
1.392 - ***: "f b1 = f b2"
1.393 - have 11: "b1 \<in> Field r \<and> b2 \<in> Field r"
1.394 - using * ** Well OF by (auto simp add: wo_rel.ofilter_def)
1.395 - moreover
1.396 - {assume "(b1,b2) \<in> r"
1.397 - hence "b1 \<in> rel.under r b2 \<and> b2 \<in> rel.under r b2"
1.398 - unfolding rel.under_def using 11 Refl
1.399 - by (auto simp add: refl_on_def)
1.400 - hence "b1 = b2" using BIJ * ** ***
1.401 - by (auto simp add: bij_betw_def inj_on_def)
1.402 - }
1.403 - moreover
1.404 - {assume "(b2,b1) \<in> r"
1.405 - hence "b1 \<in> rel.under r b1 \<and> b2 \<in> rel.under r b1"
1.406 - unfolding rel.under_def using 11 Refl
1.407 - by (auto simp add: refl_on_def)
1.408 - hence "b1 = b2" using BIJ * ** ***
1.409 - by (auto simp add: bij_betw_def inj_on_def)
1.410 - }
1.411 - ultimately
1.412 - show "b1 = b2"
1.413 - using Total by (auto simp add: total_on_def)
1.414 - qed
1.415 - (* *)
1.416 - let ?f' = "(inv_into A f)"
1.417 - (* *)
1.418 - have 2: "\<forall>b \<in> A. bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
1.419 - proof(clarify)
1.420 - fix b assume *: "b \<in> A"
1.421 - hence "rel.under r b \<le> A"
1.422 - using Well OF by(auto simp add: wo_rel.ofilter_def)
1.423 - moreover
1.424 - have "f ` (rel.under r b) = rel.under r' (f b)"
1.425 - using * BIJ by (auto simp add: bij_betw_def)
1.426 - ultimately
1.427 - show "bij_betw ?f' (rel.under r' (f b)) (rel.under r b)"
1.428 - using 1 by (auto simp add: bij_betw_inv_into_subset)
1.429 - qed
1.430 - (* *)
1.431 - have 3: "\<forall>b' \<in> Field r'. bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
1.432 - proof(clarify)
1.433 - fix b' assume *: "b' \<in> Field r'"
1.434 - have "b' = f (?f' b')" using * 1
1.435 - by (auto simp add: bij_betw_inv_into_right)
1.436 - moreover
1.437 - {obtain b where 31: "b \<in> A" and "f b = b'" using IMAGE * by force
1.438 - hence "?f' b' = b" using 1 by (auto simp add: bij_betw_inv_into_left)
1.439 - with 31 have "?f' b' \<in> A" by auto
1.440 - }
1.441 - ultimately
1.442 - show "bij_betw ?f' (rel.under r' b') (rel.under r (?f' b'))"
1.443 - using 2 by auto
1.444 - qed
1.445 - (* *)
1.446 - thus ?thesis unfolding embed_def .
1.447 -qed
1.448 -
1.449 -
1.450 -lemma inv_into_underS_embed:
1.451 -assumes WELL: "Well_order r" and
1.452 - BIJ: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
1.453 - IN: "a \<in> Field r" and
1.454 - IMAGE: "f ` (rel.underS r a) = Field r'"
1.455 -shows "embed r' r (inv_into (rel.underS r a) f)"
1.456 -using assms
1.457 -by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
1.458 -
1.459 -
1.460 -lemma inv_into_Field_embed:
1.461 -assumes WELL: "Well_order r" and EMB: "embed r r' f" and
1.462 - IMAGE: "Field r' \<le> f ` (Field r)"
1.463 -shows "embed r' r (inv_into (Field r) f)"
1.464 -proof-
1.465 - have "(\<forall>b \<in> Field r. bij_betw f (rel.under r b) (rel.under r' (f b)))"
1.466 - using EMB by (auto simp add: embed_def)
1.467 - moreover
1.468 - have "f ` (Field r) \<le> Field r'"
1.469 - using EMB WELL by (auto simp add: embed_Field)
1.470 - ultimately
1.471 - show ?thesis using assms
1.472 - by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
1.473 -qed
1.474 -
1.475 -
1.476 -lemma inv_into_Field_embed_bij_betw:
1.477 -assumes WELL: "Well_order r" and
1.478 - EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
1.479 -shows "embed r' r (inv_into (Field r) f)"
1.480 -proof-
1.481 - have "Field r' \<le> f ` (Field r)"
1.482 - using BIJ by (auto simp add: bij_betw_def)
1.483 - thus ?thesis using assms
1.484 - by(auto simp add: inv_into_Field_embed)
1.485 -qed
1.486 -
1.487 -
1.488 -
1.489 -
1.490 -
1.491 -subsection {* Given any two well-orders, one can be embedded in the other *}
1.492 -
1.493 -
1.494 -text{* Here is an overview of the proof of of this fact, stated in theorem
1.495 -@{text "wellorders_totally_ordered"}:
1.496 -
1.497 - Fix the well-orders @{text "r::'a rel"} and @{text "r'::'a' rel"}.
1.498 - Attempt to define an embedding @{text "f::'a \<Rightarrow> 'a'"} from @{text "r"} to @{text "r'"} in the
1.499 - natural way by well-order recursion ("hoping" that @{text "Field r"} turns out to be smaller
1.500 - than @{text "Field r'"}), but also record, at the recursive step, in a function
1.501 - @{text "g::'a \<Rightarrow> bool"}, the extra information of whether @{text "Field r'"}
1.502 - gets exhausted or not.
1.503 -
1.504 - If @{text "Field r'"} does not get exhausted, then @{text "Field r"} is indeed smaller
1.505 - and @{text "f"} is the desired embedding from @{text "r"} to @{text "r'"}
1.506 - (lemma @{text "wellorders_totally_ordered_aux"}).
1.507 -
1.508 - Otherwise, it means that @{text "Field r'"} is the smaller one, and the inverse of
1.509 - (the "good" segment of) @{text "f"} is the desired embedding from @{text "r'"} to @{text "r"}
1.510 - (lemma @{text "wellorders_totally_ordered_aux2"}).
1.511 -*}
1.512 -
1.513 -
1.514 -lemma wellorders_totally_ordered_aux:
1.515 -fixes r ::"'a rel" and r'::"'a' rel" and
1.516 - f :: "'a \<Rightarrow> 'a'" and a::'a
1.517 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and IN: "a \<in> Field r" and
1.518 - IH: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))" and
1.519 - NOT: "f ` (rel.underS r a) \<noteq> Field r'" and SUC: "f a = wo_rel.suc r' (f`(rel.underS r a))"
1.520 -shows "bij_betw f (rel.under r a) (rel.under r' (f a))"
1.521 -proof-
1.522 - (* Preliminary facts *)
1.523 - have Well: "wo_rel r" using WELL unfolding wo_rel_def .
1.524 - hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
1.525 - have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
1.526 - have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
1.527 - have OF: "wo_rel.ofilter r (rel.underS r a)"
1.528 - by (auto simp add: Well wo_rel.underS_ofilter)
1.529 - hence UN: "rel.underS r a = (\<Union> b \<in> rel.underS r a. rel.under r b)"
1.530 - using Well wo_rel.ofilter_under_UNION[of r "rel.underS r a"] by blast
1.531 - (* Gather facts about elements of rel.underS r a *)
1.532 - {fix b assume *: "b \<in> rel.underS r a"
1.533 - hence t0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
1.534 - have t1: "b \<in> Field r"
1.535 - using * rel.underS_Field[of r a] by auto
1.536 - have t2: "f`(rel.under r b) = rel.under r' (f b)"
1.537 - using IH * by (auto simp add: bij_betw_def)
1.538 - hence t3: "wo_rel.ofilter r' (f`(rel.under r b))"
1.539 - using Well' by (auto simp add: wo_rel.under_ofilter)
1.540 - have "f`(rel.under r b) \<le> Field r'"
1.541 - using t2 by (auto simp add: rel.under_Field)
1.542 - moreover
1.543 - have "b \<in> rel.under r b"
1.544 - using t1 by(auto simp add: Refl rel.Refl_under_in)
1.545 - ultimately
1.546 - have t4: "f b \<in> Field r'" by auto
1.547 - have "f`(rel.under r b) = rel.under r' (f b) \<and>
1.548 - wo_rel.ofilter r' (f`(rel.under r b)) \<and>
1.549 - f b \<in> Field r'"
1.550 - using t2 t3 t4 by auto
1.551 - }
1.552 - hence bFact:
1.553 - "\<forall>b \<in> rel.underS r a. f`(rel.under r b) = rel.under r' (f b) \<and>
1.554 - wo_rel.ofilter r' (f`(rel.under r b)) \<and>
1.555 - f b \<in> Field r'" by blast
1.556 - (* *)
1.557 - have subField: "f`(rel.underS r a) \<le> Field r'"
1.558 - using bFact by blast
1.559 - (* *)
1.560 - have OF': "wo_rel.ofilter r' (f`(rel.underS r a))"
1.561 - proof-
1.562 - have "f`(rel.underS r a) = f`(\<Union> b \<in> rel.underS r a. rel.under r b)"
1.563 - using UN by auto
1.564 - also have "\<dots> = (\<Union> b \<in> rel.underS r a. f`(rel.under r b))" by blast
1.565 - also have "\<dots> = (\<Union> b \<in> rel.underS r a. (rel.under r' (f b)))"
1.566 - using bFact by auto
1.567 - finally
1.568 - have "f`(rel.underS r a) = (\<Union> b \<in> rel.underS r a. (rel.under r' (f b)))" .
1.569 - thus ?thesis
1.570 - using Well' bFact
1.571 - wo_rel.ofilter_UNION[of r' "rel.underS r a" "\<lambda> b. rel.under r' (f b)"] by fastforce
1.572 - qed
1.573 - (* *)
1.574 - have "f`(rel.underS r a) \<union> rel.AboveS r' (f`(rel.underS r a)) = Field r'"
1.575 - using Well' OF' by (auto simp add: wo_rel.ofilter_AboveS_Field)
1.576 - hence NE: "rel.AboveS r' (f`(rel.underS r a)) \<noteq> {}"
1.577 - using subField NOT by blast
1.578 - (* Main proof *)
1.579 - have INCL1: "f`(rel.underS r a) \<le> rel.underS r' (f a) "
1.580 - proof(auto)
1.581 - fix b assume *: "b \<in> rel.underS r a"
1.582 - have "f b \<noteq> f a \<and> (f b, f a) \<in> r'"
1.583 - using subField Well' SUC NE *
1.584 - wo_rel.suc_greater[of r' "f`(rel.underS r a)" "f b"] by auto
1.585 - thus "f b \<in> rel.underS r' (f a)"
1.586 - unfolding rel.underS_def by simp
1.587 - qed
1.588 - (* *)
1.589 - have INCL2: "rel.underS r' (f a) \<le> f`(rel.underS r a)"
1.590 - proof
1.591 - fix b' assume "b' \<in> rel.underS r' (f a)"
1.592 - hence "b' \<noteq> f a \<and> (b', f a) \<in> r'"
1.593 - unfolding rel.underS_def by simp
1.594 - thus "b' \<in> f`(rel.underS r a)"
1.595 - using Well' SUC NE OF'
1.596 - wo_rel.suc_ofilter_in[of r' "f ` rel.underS r a" b'] by auto
1.597 - qed
1.598 - (* *)
1.599 - have INJ: "inj_on f (rel.underS r a)"
1.600 - proof-
1.601 - have "\<forall>b \<in> rel.underS r a. inj_on f (rel.under r b)"
1.602 - using IH by (auto simp add: bij_betw_def)
1.603 - moreover
1.604 - have "\<forall>b. wo_rel.ofilter r (rel.under r b)"
1.605 - using Well by (auto simp add: wo_rel.under_ofilter)
1.606 - ultimately show ?thesis
1.607 - using WELL bFact UN
1.608 - UNION_inj_on_ofilter[of r "rel.underS r a" "\<lambda>b. rel.under r b" f]
1.609 - by auto
1.610 - qed
1.611 - (* *)
1.612 - have BIJ: "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
1.613 - unfolding bij_betw_def
1.614 - using INJ INCL1 INCL2 by auto
1.615 - (* *)
1.616 - have "f a \<in> Field r'"
1.617 - using Well' subField NE SUC
1.618 - by (auto simp add: wo_rel.suc_inField)
1.619 - thus ?thesis
1.620 - using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
1.621 -qed
1.622 -
1.623 -
1.624 -lemma wellorders_totally_ordered_aux2:
1.625 -fixes r ::"'a rel" and r'::"'a' rel" and
1.626 - f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool" and a::'a
1.627 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.628 -MAIN1:
1.629 - "\<And> a. (False \<notin> g`(rel.underS r a) \<and> f`(rel.underS r a) \<noteq> Field r'
1.630 - \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True)
1.631 - \<and>
1.632 - (\<not>(False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')
1.633 - \<longrightarrow> g a = False)" and
1.634 -MAIN2: "\<And> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
1.635 - bij_betw f (rel.under r a) (rel.under r' (f a))" and
1.636 -Case: "a \<in> Field r \<and> False \<in> g`(rel.under r a)"
1.637 -shows "\<exists>f'. embed r' r f'"
1.638 -proof-
1.639 - have Well: "wo_rel r" using WELL unfolding wo_rel_def .
1.640 - hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
1.641 - have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
1.642 - have Antisym: "antisym r" using Well wo_rel.ANTISYM[of r] by auto
1.643 - have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
1.644 - (* *)
1.645 - have 0: "rel.under r a = rel.underS r a \<union> {a}"
1.646 - using Refl Case by(auto simp add: rel.Refl_under_underS)
1.647 - (* *)
1.648 - have 1: "g a = False"
1.649 - proof-
1.650 - {assume "g a \<noteq> False"
1.651 - with 0 Case have "False \<in> g`(rel.underS r a)" by blast
1.652 - with MAIN1 have "g a = False" by blast}
1.653 - thus ?thesis by blast
1.654 - qed
1.655 - let ?A = "{a \<in> Field r. g a = False}"
1.656 - let ?a = "(wo_rel.minim r ?A)"
1.657 - (* *)
1.658 - have 2: "?A \<noteq> {} \<and> ?A \<le> Field r" using Case 1 by blast
1.659 - (* *)
1.660 - have 3: "False \<notin> g`(rel.underS r ?a)"
1.661 - proof
1.662 - assume "False \<in> g`(rel.underS r ?a)"
1.663 - then obtain b where "b \<in> rel.underS r ?a" and 31: "g b = False" by auto
1.664 - hence 32: "(b,?a) \<in> r \<and> b \<noteq> ?a"
1.665 - by (auto simp add: rel.underS_def)
1.666 - hence "b \<in> Field r" unfolding Field_def by auto
1.667 - with 31 have "b \<in> ?A" by auto
1.668 - hence "(?a,b) \<in> r" using wo_rel.minim_least 2 Well by fastforce
1.669 - (* again: why worked without type annotations? *)
1.670 - with 32 Antisym show False
1.671 - by (auto simp add: antisym_def)
1.672 - qed
1.673 - have temp: "?a \<in> ?A"
1.674 - using Well 2 wo_rel.minim_in[of r ?A] by auto
1.675 - hence 4: "?a \<in> Field r" by auto
1.676 - (* *)
1.677 - have 5: "g ?a = False" using temp by blast
1.678 - (* *)
1.679 - have 6: "f`(rel.underS r ?a) = Field r'"
1.680 - using MAIN1[of ?a] 3 5 by blast
1.681 - (* *)
1.682 - have 7: "\<forall>b \<in> rel.underS r ?a. bij_betw f (rel.under r b) (rel.under r' (f b))"
1.683 - proof
1.684 - fix b assume as: "b \<in> rel.underS r ?a"
1.685 - moreover
1.686 - have "wo_rel.ofilter r (rel.underS r ?a)"
1.687 - using Well by (auto simp add: wo_rel.underS_ofilter)
1.688 - ultimately
1.689 - have "False \<notin> g`(rel.under r b)" using 3 Well by (subst (asm) wo_rel.ofilter_def) fast+
1.690 - moreover have "b \<in> Field r"
1.691 - unfolding Field_def using as by (auto simp add: rel.underS_def)
1.692 - ultimately
1.693 - show "bij_betw f (rel.under r b) (rel.under r' (f b))"
1.694 - using MAIN2 by auto
1.695 - qed
1.696 - (* *)
1.697 - have "embed r' r (inv_into (rel.underS r ?a) f)"
1.698 - using WELL WELL' 7 4 6 inv_into_underS_embed[of r ?a f r'] by auto
1.699 - thus ?thesis
1.700 - unfolding embed_def by blast
1.701 -qed
1.702 -
1.703 -
1.704 -theorem wellorders_totally_ordered:
1.705 -fixes r ::"'a rel" and r'::"'a' rel"
1.706 -assumes WELL: "Well_order r" and WELL': "Well_order r'"
1.707 -shows "(\<exists>f. embed r r' f) \<or> (\<exists>f'. embed r' r f')"
1.708 -proof-
1.709 - (* Preliminary facts *)
1.710 - have Well: "wo_rel r" using WELL unfolding wo_rel_def .
1.711 - hence Refl: "Refl r" using wo_rel.REFL[of r] by auto
1.712 - have Trans: "trans r" using Well wo_rel.TRANS[of r] by auto
1.713 - have Well': "wo_rel r'" using WELL' unfolding wo_rel_def .
1.714 - (* Main proof *)
1.715 - obtain H where H_def: "H =
1.716 - (\<lambda>h a. if False \<notin> (snd o h)`(rel.underS r a) \<and> (fst o h)`(rel.underS r a) \<noteq> Field r'
1.717 - then (wo_rel.suc r' ((fst o h)`(rel.underS r a)), True)
1.718 - else (undefined, False))" by blast
1.719 - have Adm: "wo_rel.adm_wo r H"
1.720 - using Well
1.721 - proof(unfold wo_rel.adm_wo_def, clarify)
1.722 - fix h1::"'a \<Rightarrow> 'a' * bool" and h2::"'a \<Rightarrow> 'a' * bool" and x
1.723 - assume "\<forall>y\<in>rel.underS r x. h1 y = h2 y"
1.724 - hence "\<forall>y\<in>rel.underS r x. (fst o h1) y = (fst o h2) y \<and>
1.725 - (snd o h1) y = (snd o h2) y" by auto
1.726 - hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
1.727 - (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
1.728 - by (auto simp add: image_def)
1.729 - thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
1.730 - qed
1.731 - (* More constant definitions: *)
1.732 - obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"
1.733 - where h_def: "h = wo_rel.worec r H" and
1.734 - f_def: "f = fst o h" and g_def: "g = snd o h" by blast
1.735 - obtain test where test_def:
1.736 - "test = (\<lambda> a. False \<notin> (g`(rel.underS r a)) \<and> f`(rel.underS r a) \<noteq> Field r')" by blast
1.737 - (* *)
1.738 - have *: "\<And> a. h a = H h a"
1.739 - using Adm Well wo_rel.worec_fixpoint[of r H] by (simp add: h_def)
1.740 - have Main1:
1.741 - "\<And> a. (test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
1.742 - (\<not>(test a) \<longrightarrow> g a = False)"
1.743 - proof- (* How can I prove this withou fixing a? *)
1.744 - fix a show "(test a \<longrightarrow> f a = wo_rel.suc r' (f`(rel.underS r a)) \<and> g a = True) \<and>
1.745 - (\<not>(test a) \<longrightarrow> g a = False)"
1.746 - using *[of a] test_def f_def g_def H_def by auto
1.747 - qed
1.748 - (* *)
1.749 - let ?phi = "\<lambda> a. a \<in> Field r \<and> False \<notin> g`(rel.under r a) \<longrightarrow>
1.750 - bij_betw f (rel.under r a) (rel.under r' (f a))"
1.751 - have Main2: "\<And> a. ?phi a"
1.752 - proof-
1.753 - fix a show "?phi a"
1.754 - proof(rule wo_rel.well_order_induct[of r ?phi],
1.755 - simp only: Well, clarify)
1.756 - fix a
1.757 - assume IH: "\<forall>b. b \<noteq> a \<and> (b,a) \<in> r \<longrightarrow> ?phi b" and
1.758 - *: "a \<in> Field r" and
1.759 - **: "False \<notin> g`(rel.under r a)"
1.760 - have 1: "\<forall>b \<in> rel.underS r a. bij_betw f (rel.under r b) (rel.under r' (f b))"
1.761 - proof(clarify)
1.762 - fix b assume ***: "b \<in> rel.underS r a"
1.763 - hence 0: "(b,a) \<in> r \<and> b \<noteq> a" unfolding rel.underS_def by auto
1.764 - moreover have "b \<in> Field r"
1.765 - using *** rel.underS_Field[of r a] by auto
1.766 - moreover have "False \<notin> g`(rel.under r b)"
1.767 - using 0 ** Trans rel.under_incr[of r b a] by auto
1.768 - ultimately show "bij_betw f (rel.under r b) (rel.under r' (f b))"
1.769 - using IH by auto
1.770 - qed
1.771 - (* *)
1.772 - have 21: "False \<notin> g`(rel.underS r a)"
1.773 - using ** rel.underS_subset_under[of r a] by auto
1.774 - have 22: "g`(rel.under r a) \<le> {True}" using ** by auto
1.775 - moreover have 23: "a \<in> rel.under r a"
1.776 - using Refl * by (auto simp add: rel.Refl_under_in)
1.777 - ultimately have 24: "g a = True" by blast
1.778 - have 2: "f`(rel.underS r a) \<noteq> Field r'"
1.779 - proof
1.780 - assume "f`(rel.underS r a) = Field r'"
1.781 - hence "g a = False" using Main1 test_def by blast
1.782 - with 24 show False using ** by blast
1.783 - qed
1.784 - (* *)
1.785 - have 3: "f a = wo_rel.suc r' (f`(rel.underS r a))"
1.786 - using 21 2 Main1 test_def by blast
1.787 - (* *)
1.788 - show "bij_betw f (rel.under r a) (rel.under r' (f a))"
1.789 - using WELL WELL' 1 2 3 *
1.790 - wellorders_totally_ordered_aux[of r r' a f] by auto
1.791 - qed
1.792 - qed
1.793 - (* *)
1.794 - let ?chi = "(\<lambda> a. a \<in> Field r \<and> False \<in> g`(rel.under r a))"
1.795 - show ?thesis
1.796 - proof(cases "\<exists>a. ?chi a")
1.797 - assume "\<not> (\<exists>a. ?chi a)"
1.798 - hence "\<forall>a \<in> Field r. bij_betw f (rel.under r a) (rel.under r' (f a))"
1.799 - using Main2 by blast
1.800 - thus ?thesis unfolding embed_def by blast
1.801 - next
1.802 - assume "\<exists>a. ?chi a"
1.803 - then obtain a where "?chi a" by blast
1.804 - hence "\<exists>f'. embed r' r f'"
1.805 - using wellorders_totally_ordered_aux2[of r r' g f a]
1.806 - WELL WELL' Main1 Main2 test_def by blast
1.807 - thus ?thesis by blast
1.808 - qed
1.809 -qed
1.810 -
1.811 -
1.812 -subsection {* Uniqueness of embeddings *}
1.813 -
1.814 -
1.815 -text{* Here we show a fact complementary to the one from the previous subsection -- namely,
1.816 -that between any two well-orders there is {\em at most} one embedding, and is the one
1.817 -definable by the expected well-order recursive equation. As a consequence, any two
1.818 -embeddings of opposite directions are mutually inverse. *}
1.819 -
1.820 -
1.821 -lemma embed_determined:
1.822 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.823 - EMB: "embed r r' f" and IN: "a \<in> Field r"
1.824 -shows "f a = wo_rel.suc r' (f`(rel.underS r a))"
1.825 -proof-
1.826 - have "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
1.827 - using assms by (auto simp add: embed_underS)
1.828 - hence "f`(rel.underS r a) = rel.underS r' (f a)"
1.829 - by (auto simp add: bij_betw_def)
1.830 - moreover
1.831 - {have "f a \<in> Field r'" using IN
1.832 - using EMB WELL embed_Field[of r r' f] by auto
1.833 - hence "f a = wo_rel.suc r' (rel.underS r' (f a))"
1.834 - using WELL' by (auto simp add: wo_rel_def wo_rel.suc_underS)
1.835 - }
1.836 - ultimately show ?thesis by simp
1.837 -qed
1.838 -
1.839 -
1.840 -lemma embed_unique:
1.841 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.842 - EMBf: "embed r r' f" and EMBg: "embed r r' g"
1.843 -shows "a \<in> Field r \<longrightarrow> f a = g a"
1.844 -proof(rule wo_rel.well_order_induct[of r], auto simp add: WELL wo_rel_def)
1.845 - fix a
1.846 - assume IH: "\<forall>b. b \<noteq> a \<and> (b,a): r \<longrightarrow> b \<in> Field r \<longrightarrow> f b = g b" and
1.847 - *: "a \<in> Field r"
1.848 - hence "\<forall>b \<in> rel.underS r a. f b = g b"
1.849 - unfolding rel.underS_def by (auto simp add: Field_def)
1.850 - hence "f`(rel.underS r a) = g`(rel.underS r a)" by force
1.851 - thus "f a = g a"
1.852 - using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
1.853 -qed
1.854 -
1.855 -
1.856 -lemma embed_bothWays_inverse:
1.857 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.858 - EMB: "embed r r' f" and EMB': "embed r' r f'"
1.859 -shows "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
1.860 -proof-
1.861 - have "embed r r (f' o f)" using assms
1.862 - by(auto simp add: comp_embed)
1.863 - moreover have "embed r r id" using assms
1.864 - by (auto simp add: id_embed)
1.865 - ultimately have "\<forall>a \<in> Field r. f'(f a) = a"
1.866 - using assms embed_unique[of r r "f' o f" id] id_def by auto
1.867 - moreover
1.868 - {have "embed r' r' (f o f')" using assms
1.869 - by(auto simp add: comp_embed)
1.870 - moreover have "embed r' r' id" using assms
1.871 - by (auto simp add: id_embed)
1.872 - ultimately have "\<forall>a' \<in> Field r'. f(f' a') = a'"
1.873 - using assms embed_unique[of r' r' "f o f'" id] id_def by auto
1.874 - }
1.875 - ultimately show ?thesis by blast
1.876 -qed
1.877 -
1.878 -
1.879 -lemma embed_bothWays_bij_betw:
1.880 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.881 - EMB: "embed r r' f" and EMB': "embed r' r g"
1.882 -shows "bij_betw f (Field r) (Field r')"
1.883 -proof-
1.884 - let ?A = "Field r" let ?A' = "Field r'"
1.885 - have "embed r r (g o f) \<and> embed r' r' (f o g)"
1.886 - using assms by (auto simp add: comp_embed)
1.887 - hence 1: "(\<forall>a \<in> ?A. g(f a) = a) \<and> (\<forall>a' \<in> ?A'. f(g a') = a')"
1.888 - using WELL id_embed[of r] embed_unique[of r r "g o f" id]
1.889 - WELL' id_embed[of r'] embed_unique[of r' r' "f o g" id]
1.890 - id_def by auto
1.891 - have 2: "(\<forall>a \<in> ?A. f a \<in> ?A') \<and> (\<forall>a' \<in> ?A'. g a' \<in> ?A)"
1.892 - using assms embed_Field[of r r' f] embed_Field[of r' r g] by blast
1.893 - (* *)
1.894 - show ?thesis
1.895 - proof(unfold bij_betw_def inj_on_def, auto simp add: 2)
1.896 - fix a b assume *: "a \<in> ?A" "b \<in> ?A" and **: "f a = f b"
1.897 - have "a = g(f a) \<and> b = g(f b)" using * 1 by auto
1.898 - with ** show "a = b" by auto
1.899 - next
1.900 - fix a' assume *: "a' \<in> ?A'"
1.901 - hence "g a' \<in> ?A \<and> f(g a') = a'" using 1 2 by auto
1.902 - thus "a' \<in> f ` ?A" by force
1.903 - qed
1.904 -qed
1.905 -
1.906 -
1.907 -lemma embed_bothWays_iso:
1.908 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.909 - EMB: "embed r r' f" and EMB': "embed r' r g"
1.910 -shows "iso r r' f"
1.911 -unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
1.912 -
1.913 -
1.914 -subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
1.915 -
1.916 -
1.917 -lemma embed_bothWays_Field_bij_betw:
1.918 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.919 - EMB: "embed r r' f" and EMB': "embed r' r f'"
1.920 -shows "bij_betw f (Field r) (Field r')"
1.921 -proof-
1.922 - have "(\<forall>a \<in> Field r. f'(f a) = a) \<and> (\<forall>a' \<in> Field r'. f(f' a') = a')"
1.923 - using assms by (auto simp add: embed_bothWays_inverse)
1.924 - moreover
1.925 - have "f`(Field r) \<le> Field r' \<and> f' ` (Field r') \<le> Field r"
1.926 - using assms by (auto simp add: embed_Field)
1.927 - ultimately
1.928 - show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
1.929 -qed
1.930 -
1.931 -
1.932 -lemma embedS_comp_embed:
1.933 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.934 - and EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
1.935 -shows "embedS r r'' (f' o f)"
1.936 -proof-
1.937 - let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g"
1.938 - have 1: "embed r r' f \<and> \<not> (bij_betw f (Field r) (Field r'))"
1.939 - using EMB by (auto simp add: embedS_def)
1.940 - hence 2: "embed r r'' ?g"
1.941 - using WELL EMB' comp_embed[of r r' f r'' f'] by auto
1.942 - moreover
1.943 - {assume "bij_betw ?g (Field r) (Field r'')"
1.944 - hence "embed r'' r ?h" using 2 WELL
1.945 - by (auto simp add: inv_into_Field_embed_bij_betw)
1.946 - hence "embed r' r (?h o f')" using WELL' EMB'
1.947 - by (auto simp add: comp_embed)
1.948 - hence "bij_betw f (Field r) (Field r')" using WELL WELL' 1
1.949 - by (auto simp add: embed_bothWays_Field_bij_betw)
1.950 - with 1 have False by blast
1.951 - }
1.952 - ultimately show ?thesis unfolding embedS_def by auto
1.953 -qed
1.954 -
1.955 -
1.956 -lemma embed_comp_embedS:
1.957 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.958 - and EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
1.959 -shows "embedS r r'' (f' o f)"
1.960 -proof-
1.961 - let ?g = "(f' o f)" let ?h = "inv_into (Field r) ?g"
1.962 - have 1: "embed r' r'' f' \<and> \<not> (bij_betw f' (Field r') (Field r''))"
1.963 - using EMB' by (auto simp add: embedS_def)
1.964 - hence 2: "embed r r'' ?g"
1.965 - using WELL EMB comp_embed[of r r' f r'' f'] by auto
1.966 - moreover
1.967 - {assume "bij_betw ?g (Field r) (Field r'')"
1.968 - hence "embed r'' r ?h" using 2 WELL
1.969 - by (auto simp add: inv_into_Field_embed_bij_betw)
1.970 - hence "embed r'' r' (f o ?h)" using WELL'' EMB
1.971 - by (auto simp add: comp_embed)
1.972 - hence "bij_betw f' (Field r') (Field r'')" using WELL' WELL'' 1
1.973 - by (auto simp add: embed_bothWays_Field_bij_betw)
1.974 - with 1 have False by blast
1.975 - }
1.976 - ultimately show ?thesis unfolding embedS_def by auto
1.977 -qed
1.978 -
1.979 -
1.980 -lemma embed_comp_iso:
1.981 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.982 - and EMB: "embed r r' f" and EMB': "iso r' r'' f'"
1.983 -shows "embed r r'' (f' o f)"
1.984 -using assms unfolding iso_def
1.985 -by (auto simp add: comp_embed)
1.986 -
1.987 -
1.988 -lemma iso_comp_embed:
1.989 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.990 - and EMB: "iso r r' f" and EMB': "embed r' r'' f'"
1.991 -shows "embed r r'' (f' o f)"
1.992 -using assms unfolding iso_def
1.993 -by (auto simp add: comp_embed)
1.994 -
1.995 -
1.996 -lemma embedS_comp_iso:
1.997 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.998 - and EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
1.999 -shows "embedS r r'' (f' o f)"
1.1000 -using assms unfolding iso_def
1.1001 -by (auto simp add: embedS_comp_embed)
1.1002 -
1.1003 -
1.1004 -lemma iso_comp_embedS:
1.1005 -assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
1.1006 - and EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
1.1007 -shows "embedS r r'' (f' o f)"
1.1008 -using assms unfolding iso_def using embed_comp_embedS
1.1009 -by (auto simp add: embed_comp_embedS)
1.1010 -
1.1011 -
1.1012 -lemma embedS_Field:
1.1013 -assumes WELL: "Well_order r" and EMB: "embedS r r' f"
1.1014 -shows "f ` (Field r) < Field r'"
1.1015 -proof-
1.1016 - have "f`(Field r) \<le> Field r'" using assms
1.1017 - by (auto simp add: embed_Field embedS_def)
1.1018 - moreover
1.1019 - {have "inj_on f (Field r)" using assms
1.1020 - by (auto simp add: embedS_def embed_inj_on)
1.1021 - hence "f`(Field r) \<noteq> Field r'" using EMB
1.1022 - by (auto simp add: embedS_def bij_betw_def)
1.1023 - }
1.1024 - ultimately show ?thesis by blast
1.1025 -qed
1.1026 -
1.1027 -
1.1028 -lemma embedS_iff:
1.1029 -assumes WELL: "Well_order r" and ISO: "embed r r' f"
1.1030 -shows "embedS r r' f = (f ` (Field r) < Field r')"
1.1031 -proof
1.1032 - assume "embedS r r' f"
1.1033 - thus "f ` Field r \<subset> Field r'"
1.1034 - using WELL by (auto simp add: embedS_Field)
1.1035 -next
1.1036 - assume "f ` Field r \<subset> Field r'"
1.1037 - hence "\<not> bij_betw f (Field r) (Field r')"
1.1038 - unfolding bij_betw_def by blast
1.1039 - thus "embedS r r' f" unfolding embedS_def
1.1040 - using ISO by auto
1.1041 -qed
1.1042 -
1.1043 -
1.1044 -lemma iso_Field:
1.1045 -"iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
1.1046 -using assms by (auto simp add: iso_def bij_betw_def)
1.1047 -
1.1048 -
1.1049 -lemma iso_iff:
1.1050 -assumes "Well_order r"
1.1051 -shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
1.1052 -proof
1.1053 - assume "iso r r' f"
1.1054 - thus "embed r r' f \<and> f ` (Field r) = Field r'"
1.1055 - by (auto simp add: iso_Field iso_def)
1.1056 -next
1.1057 - assume *: "embed r r' f \<and> f ` Field r = Field r'"
1.1058 - hence "inj_on f (Field r)" using assms by (auto simp add: embed_inj_on)
1.1059 - with * have "bij_betw f (Field r) (Field r')"
1.1060 - unfolding bij_betw_def by simp
1.1061 - with * show "iso r r' f" unfolding iso_def by auto
1.1062 -qed
1.1063 -
1.1064 -
1.1065 -lemma iso_iff2:
1.1066 -assumes "Well_order r"
1.1067 -shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
1.1068 - (\<forall>a \<in> Field r. \<forall>b \<in> Field r.
1.1069 - (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"
1.1070 -using assms
1.1071 -proof(auto simp add: iso_def)
1.1072 - fix a b
1.1073 - assume "embed r r' f"
1.1074 - hence "compat r r' f" using embed_compat[of r] by auto
1.1075 - moreover assume "(a,b) \<in> r"
1.1076 - ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto
1.1077 -next
1.1078 - let ?f' = "inv_into (Field r) f"
1.1079 - assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"
1.1080 - hence "embed r' r ?f'" using assms
1.1081 - by (auto simp add: inv_into_Field_embed_bij_betw)
1.1082 - hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto
1.1083 - fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"
1.1084 - hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1
1.1085 - by (auto simp add: bij_betw_inv_into_left)
1.1086 - thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce
1.1087 -next
1.1088 - assume *: "bij_betw f (Field r) (Field r')" and
1.1089 - **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
1.1090 - have 1: "\<And> a. rel.under r a \<le> Field r \<and> rel.under r' (f a) \<le> Field r'"
1.1091 - by (auto simp add: rel.under_Field)
1.1092 - have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
1.1093 - {fix a assume ***: "a \<in> Field r"
1.1094 - have "bij_betw f (rel.under r a) (rel.under r' (f a))"
1.1095 - proof(unfold bij_betw_def, auto)
1.1096 - show "inj_on f (rel.under r a)"
1.1097 - using 1 2 by (auto simp add: subset_inj_on)
1.1098 - next
1.1099 - fix b assume "b \<in> rel.under r a"
1.1100 - hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
1.1101 - unfolding rel.under_def by (auto simp add: Field_def Range_def Domain_def)
1.1102 - with 1 ** show "f b \<in> rel.under r' (f a)"
1.1103 - unfolding rel.under_def by auto
1.1104 - next
1.1105 - fix b' assume "b' \<in> rel.under r' (f a)"
1.1106 - hence 3: "(b',f a) \<in> r'" unfolding rel.under_def by simp
1.1107 - hence "b' \<in> Field r'" unfolding Field_def by auto
1.1108 - with * obtain b where "b \<in> Field r \<and> f b = b'"
1.1109 - unfolding bij_betw_def by force
1.1110 - with 3 ** ***
1.1111 - show "b' \<in> f ` (rel.under r a)" unfolding rel.under_def by blast
1.1112 - qed
1.1113 - }
1.1114 - thus "embed r r' f" unfolding embed_def using * by auto
1.1115 -qed
1.1116 -
1.1117 -
1.1118 -lemma iso_iff3:
1.1119 -assumes WELL: "Well_order r" and WELL': "Well_order r'"
1.1120 -shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
1.1121 -proof
1.1122 - assume "iso r r' f"
1.1123 - thus "bij_betw f (Field r) (Field r') \<and> compat r r' f"
1.1124 - unfolding compat_def using WELL by (auto simp add: iso_iff2 Field_def)
1.1125 -next
1.1126 - have Well: "wo_rel r \<and> wo_rel r'" using WELL WELL'
1.1127 - by (auto simp add: wo_rel_def)
1.1128 - assume *: "bij_betw f (Field r) (Field r') \<and> compat r r' f"
1.1129 - thus "iso r r' f"
1.1130 - unfolding "compat_def" using assms
1.1131 - proof(auto simp add: iso_iff2)
1.1132 - fix a b assume **: "a \<in> Field r" "b \<in> Field r" and
1.1133 - ***: "(f a, f b) \<in> r'"
1.1134 - {assume "(b,a) \<in> r \<or> b = a"
1.1135 - hence "(b,a): r"using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
1.1136 - hence "(f b, f a) \<in> r'" using * unfolding compat_def by auto
1.1137 - hence "f a = f b"
1.1138 - using Well *** wo_rel.ANTISYM[of r'] antisym_def[of r'] by blast
1.1139 - hence "a = b" using * ** unfolding bij_betw_def inj_on_def by auto
1.1140 - hence "(a,b) \<in> r" using Well ** wo_rel.REFL[of r] refl_on_def[of _ r] by blast
1.1141 - }
1.1142 - thus "(a,b) \<in> r"
1.1143 - using Well ** wo_rel.TOTAL[of r] total_on_def[of _ r] by blast
1.1144 - qed
1.1145 -qed
1.1146 -
1.1147 -
1.1148 -
1.1149 -end