src/HOL/BNF_Wellorder_Embedding.thy
changeset 55101 57c875e488bd
parent 55059 ef2e0fb783c6
child 55811 aa1acc25126b
     1.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Tue Jan 21 16:56:34 2014 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Wed Jan 22 09:45:30 2014 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4  imports Zorn BNF_Wellorder_Relation
     1.5  begin
     1.6  
     1.7 -
     1.8  text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and
     1.9  prove their basic properties.  The notion of embedding is considered from the point
    1.10  of view of the theory of ordinals, and therefore requires the source to be injected
    1.11 @@ -36,7 +35,6 @@
    1.12    by (auto simp add: inj_on_UNION_chain)
    1.13  qed
    1.14  
    1.15 -
    1.16  lemma under_underS_bij_betw:
    1.17  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
    1.18          IN: "a \<in> Field r" and IN': "f a \<in> Field r'" and
    1.19 @@ -57,10 +55,8 @@
    1.20  qed
    1.21  
    1.22  
    1.23 -
    1.24  subsection {* (Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
    1.25 -functions  *}
    1.26 -
    1.27 +functions *}
    1.28  
    1.29  text{* Standardly, a function is an embedding of a well-order in another if it injectively and
    1.30  order-compatibly maps the former into an order filter of the latter.
    1.31 @@ -70,40 +66,32 @@
    1.32  and the set of strict lower bounds of its image.  (Later we prove equivalence with
    1.33  the standard definition -- lemma @{text "embed_iff_compat_inj_on_ofilter"}.)
    1.34  A {\em strict embedding} (operator @{text "embedS"})  is a non-bijective embedding
    1.35 -and an isomorphism (operator @{text "iso"}) is a bijective embedding.   *}
    1.36 -
    1.37 +and an isomorphism (operator @{text "iso"}) is a bijective embedding. *}
    1.38  
    1.39  definition embed :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.40  where
    1.41  "embed r r' f \<equiv> \<forall>a \<in> Field r. bij_betw f (under r a) (under r' (f a))"
    1.42  
    1.43 -
    1.44  lemmas embed_defs = embed_def embed_def[abs_def]
    1.45  
    1.46 -
    1.47  text {* Strict embeddings: *}
    1.48  
    1.49  definition embedS :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.50  where
    1.51  "embedS r r' f \<equiv> embed r r' f \<and> \<not> bij_betw f (Field r) (Field r')"
    1.52  
    1.53 -
    1.54  lemmas embedS_defs = embedS_def embedS_def[abs_def]
    1.55  
    1.56 -
    1.57  definition iso :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.58  where
    1.59  "iso r r' f \<equiv> embed r r' f \<and> bij_betw f (Field r) (Field r')"
    1.60  
    1.61 -
    1.62  lemmas iso_defs = iso_def iso_def[abs_def]
    1.63  
    1.64 -
    1.65  definition compat :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> bool"
    1.66  where
    1.67  "compat r r' f \<equiv> \<forall>a b. (a,b) \<in> r \<longrightarrow> (f a, f b) \<in> r'"
    1.68  
    1.69 -
    1.70  lemma compat_wf:
    1.71  assumes CMP: "compat r r' f" and WF: "wf r'"
    1.72  shows "wf r"
    1.73 @@ -115,15 +103,12 @@
    1.74    using wf_inv_image[of r' f] wf_subset[of "inv_image r' f"] by auto
    1.75  qed
    1.76  
    1.77 -
    1.78  lemma id_embed: "embed r r id"
    1.79  by(auto simp add: id_def embed_def bij_betw_def)
    1.80  
    1.81 -
    1.82  lemma id_iso: "iso r r id"
    1.83  by(auto simp add: id_def embed_def iso_def bij_betw_def)
    1.84  
    1.85 -
    1.86  lemma embed_in_Field:
    1.87  assumes WELL: "Well_order r" and
    1.88          EMB: "embed r r' f" and IN: "a \<in> Field r"
    1.89 @@ -140,7 +125,6 @@
    1.90    by (auto simp: under_def)
    1.91  qed
    1.92  
    1.93 -
    1.94  lemma comp_embed:
    1.95  assumes WELL: "Well_order r" and
    1.96          EMB: "embed r r' f" and EMB': "embed r' r'' f'"
    1.97 @@ -160,7 +144,6 @@
    1.98    by(auto simp add: bij_betw_trans)
    1.99  qed
   1.100  
   1.101 -
   1.102  lemma comp_iso:
   1.103  assumes WELL: "Well_order r" and
   1.104          EMB: "iso r r' f" and EMB': "iso r' r'' f'"
   1.105 @@ -168,15 +151,12 @@
   1.106  using assms unfolding iso_def
   1.107  by (auto simp add: comp_embed bij_betw_trans)
   1.108  
   1.109 -
   1.110 -text{* That @{text "embedS"} is also preserved by function composition shall be proved only later.  *}
   1.111 -
   1.112 +text{* That @{text "embedS"} is also preserved by function composition shall be proved only later. *}
   1.113  
   1.114  lemma embed_Field:
   1.115  "\<lbrakk>Well_order r; embed r r' f\<rbrakk> \<Longrightarrow> f`(Field r) \<le> Field r'"
   1.116  by (auto simp add: embed_in_Field)
   1.117  
   1.118 -
   1.119  lemma embed_preserves_ofilter:
   1.120  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.121          EMB: "embed r r' f" and OF: "wo_rel.ofilter r A"
   1.122 @@ -204,7 +184,6 @@
   1.123    qed
   1.124  qed
   1.125  
   1.126 -
   1.127  lemma embed_Field_ofilter:
   1.128  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.129          EMB: "embed r r' f"
   1.130 @@ -216,7 +195,6 @@
   1.131    show ?thesis by (auto simp add: embed_preserves_ofilter)
   1.132  qed
   1.133  
   1.134 -
   1.135  lemma embed_compat:
   1.136  assumes EMB: "embed r r' f"
   1.137  shows "compat r r' f"
   1.138 @@ -234,7 +212,6 @@
   1.139    by (auto simp add: under_def)
   1.140  qed
   1.141  
   1.142 -
   1.143  lemma embed_inj_on:
   1.144  assumes WELL: "Well_order r" and EMB: "embed r r' f"
   1.145  shows "inj_on f (Field r)"
   1.146 @@ -271,7 +248,6 @@
   1.147    by (auto simp add: total_on_def)
   1.148  qed
   1.149  
   1.150 -
   1.151  lemma embed_underS:
   1.152  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.153          EMB: "embed r r' f" and IN: "a \<in> Field r"
   1.154 @@ -293,7 +269,6 @@
   1.155    by (auto simp add: notIn_Un_bij_betw3)
   1.156  qed
   1.157  
   1.158 -
   1.159  lemma embed_iff_compat_inj_on_ofilter:
   1.160  assumes WELL: "Well_order r" and WELL': "Well_order r'"
   1.161  shows "embed r r' f = (compat r r' f \<and> inj_on f (Field r) \<and> wo_rel.ofilter r' (f`(Field r)))"
   1.162 @@ -366,7 +341,6 @@
   1.163    qed
   1.164  qed
   1.165  
   1.166 -
   1.167  lemma inv_into_ofilter_embed:
   1.168  assumes WELL: "Well_order r" and OF: "wo_rel.ofilter r A" and
   1.169          BIJ: "\<forall>b \<in> A. bij_betw f (under r b) (under r' (f b))" and
   1.170 @@ -442,7 +416,6 @@
   1.171    thus ?thesis unfolding embed_def .
   1.172  qed
   1.173  
   1.174 -
   1.175  lemma inv_into_underS_embed:
   1.176  assumes WELL: "Well_order r" and
   1.177          BIJ: "\<forall>b \<in> underS r a. bij_betw f (under r b) (under r' (f b))" and
   1.178 @@ -452,7 +425,6 @@
   1.179  using assms
   1.180  by(auto simp add: wo_rel_def wo_rel.underS_ofilter inv_into_ofilter_embed)
   1.181  
   1.182 -
   1.183  lemma inv_into_Field_embed:
   1.184  assumes WELL: "Well_order r" and EMB: "embed r r' f" and
   1.185          IMAGE: "Field r' \<le> f ` (Field r)"
   1.186 @@ -468,7 +440,6 @@
   1.187    by(auto simp add: wo_rel_def wo_rel.Field_ofilter inv_into_ofilter_embed)
   1.188  qed
   1.189  
   1.190 -
   1.191  lemma inv_into_Field_embed_bij_betw:
   1.192  assumes WELL: "Well_order r" and
   1.193          EMB: "embed r r' f" and BIJ: "bij_betw f (Field r) (Field r')"
   1.194 @@ -481,12 +452,8 @@
   1.195  qed
   1.196  
   1.197  
   1.198 -
   1.199 -
   1.200 -
   1.201  subsection {* Given any two well-orders, one can be embedded in the other *}
   1.202  
   1.203 -
   1.204  text{* Here is an overview of the proof of of this fact, stated in theorem
   1.205  @{text "wellorders_totally_ordered"}:
   1.206  
   1.207 @@ -506,7 +473,6 @@
   1.208     (lemma @{text "wellorders_totally_ordered_aux2"}).
   1.209  *}
   1.210  
   1.211 -
   1.212  lemma wellorders_totally_ordered_aux:
   1.213  fixes r ::"'a rel"  and r'::"'a' rel" and
   1.214        f :: "'a \<Rightarrow> 'a'" and a::'a
   1.215 @@ -616,7 +582,6 @@
   1.216    using WELL WELL' IN BIJ under_underS_bij_betw[of r r' a f] by auto
   1.217  qed
   1.218  
   1.219 -
   1.220  lemma wellorders_totally_ordered_aux2:
   1.221  fixes r ::"'a rel"  and r'::"'a' rel" and
   1.222        f :: "'a \<Rightarrow> 'a'" and g :: "'a \<Rightarrow> bool"  and a::'a
   1.223 @@ -696,7 +661,6 @@
   1.224    unfolding embed_def by blast
   1.225  qed
   1.226  
   1.227 -
   1.228  theorem wellorders_totally_ordered:
   1.229  fixes r ::"'a rel"  and r'::"'a' rel"
   1.230  assumes WELL: "Well_order r" and WELL': "Well_order r'"
   1.231 @@ -805,15 +769,13 @@
   1.232  qed
   1.233  
   1.234  
   1.235 -subsection {* Uniqueness of embeddings  *}
   1.236 -
   1.237 +subsection {* Uniqueness of embeddings *}
   1.238  
   1.239  text{* Here we show a fact complementary to the one from the previous subsection -- namely,
   1.240  that between any two well-orders there is {\em at most} one embedding, and is the one
   1.241  definable by the expected well-order recursive equation.  As a consequence, any two
   1.242  embeddings of opposite directions are mutually inverse. *}
   1.243  
   1.244 -
   1.245  lemma embed_determined:
   1.246  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.247          EMB: "embed r r' f" and IN: "a \<in> Field r"
   1.248 @@ -832,7 +794,6 @@
   1.249    ultimately show ?thesis by simp
   1.250  qed
   1.251  
   1.252 -
   1.253  lemma embed_unique:
   1.254  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.255          EMBf: "embed r r' f" and EMBg: "embed r r' g"
   1.256 @@ -848,7 +809,6 @@
   1.257    using assms * embed_determined[of r r' f a] embed_determined[of r r' g a] by auto
   1.258  qed
   1.259  
   1.260 -
   1.261  lemma embed_bothWays_inverse:
   1.262  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.263          EMB: "embed r r' f" and EMB': "embed r' r f'"
   1.264 @@ -871,7 +831,6 @@
   1.265    ultimately show ?thesis by blast
   1.266  qed
   1.267  
   1.268 -
   1.269  lemma embed_bothWays_bij_betw:
   1.270  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.271          EMB: "embed r r' f" and EMB': "embed r' r g"
   1.272 @@ -899,7 +858,6 @@
   1.273    qed
   1.274  qed
   1.275  
   1.276 -
   1.277  lemma embed_bothWays_iso:
   1.278  assumes WELL: "Well_order r"  and WELL': "Well_order r'" and
   1.279          EMB: "embed r r' f" and EMB': "embed r' r g"
   1.280 @@ -907,8 +865,7 @@
   1.281  unfolding iso_def using assms by (auto simp add: embed_bothWays_bij_betw)
   1.282  
   1.283  
   1.284 -subsection {* More properties of embeddings, strict embeddings and isomorphisms  *}
   1.285 -
   1.286 +subsection {* More properties of embeddings, strict embeddings and isomorphisms *}
   1.287  
   1.288  lemma embed_bothWays_Field_bij_betw:
   1.289  assumes WELL: "Well_order r" and WELL': "Well_order r'" and
   1.290 @@ -924,7 +881,6 @@
   1.291    show ?thesis using bij_betw_byWitness[of "Field r" f' f "Field r'"] by auto
   1.292  qed
   1.293  
   1.294 -
   1.295  lemma embedS_comp_embed:
   1.296  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.297          and  EMB: "embedS r r' f" and EMB': "embed r' r'' f'"
   1.298 @@ -948,7 +904,6 @@
   1.299    ultimately show ?thesis unfolding embedS_def by auto
   1.300  qed
   1.301  
   1.302 -
   1.303  lemma embed_comp_embedS:
   1.304  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.305          and  EMB: "embed r r' f" and EMB': "embedS r' r'' f'"
   1.306 @@ -972,7 +927,6 @@
   1.307    ultimately show ?thesis unfolding embedS_def by auto
   1.308  qed
   1.309  
   1.310 -
   1.311  lemma embed_comp_iso:
   1.312  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.313          and  EMB: "embed r r' f" and EMB': "iso r' r'' f'"
   1.314 @@ -980,7 +934,6 @@
   1.315  using assms unfolding iso_def
   1.316  by (auto simp add: comp_embed)
   1.317  
   1.318 -
   1.319  lemma iso_comp_embed:
   1.320  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.321          and  EMB: "iso r r' f" and EMB': "embed r' r'' f'"
   1.322 @@ -988,7 +941,6 @@
   1.323  using assms unfolding iso_def
   1.324  by (auto simp add: comp_embed)
   1.325  
   1.326 -
   1.327  lemma embedS_comp_iso:
   1.328  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.329          and  EMB: "embedS r r' f" and EMB': "iso r' r'' f'"
   1.330 @@ -996,7 +948,6 @@
   1.331  using assms unfolding iso_def
   1.332  by (auto simp add: embedS_comp_embed)
   1.333  
   1.334 -
   1.335  lemma iso_comp_embedS:
   1.336  assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
   1.337          and  EMB: "iso r r' f" and EMB': "embedS r' r'' f'"
   1.338 @@ -1004,7 +955,6 @@
   1.339  using assms unfolding iso_def  using embed_comp_embedS
   1.340  by (auto simp add: embed_comp_embedS)
   1.341  
   1.342 -
   1.343  lemma embedS_Field:
   1.344  assumes WELL: "Well_order r" and EMB: "embedS r r' f"
   1.345  shows "f ` (Field r) < Field r'"
   1.346 @@ -1020,7 +970,6 @@
   1.347    ultimately show ?thesis by blast
   1.348  qed
   1.349  
   1.350 -
   1.351  lemma embedS_iff:
   1.352  assumes WELL: "Well_order r" and ISO: "embed r r' f"
   1.353  shows "embedS r r' f = (f ` (Field r) < Field r')"
   1.354 @@ -1036,12 +985,10 @@
   1.355    using ISO by auto
   1.356  qed
   1.357  
   1.358 -
   1.359  lemma iso_Field:
   1.360  "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
   1.361  using assms by (auto simp add: iso_def bij_betw_def)
   1.362  
   1.363 -
   1.364  lemma iso_iff:
   1.365  assumes "Well_order r"
   1.366  shows "iso r r' f = (embed r r' f \<and> f ` (Field r) = Field r')"
   1.367 @@ -1057,7 +1004,6 @@
   1.368    with * show "iso r r' f" unfolding iso_def by auto
   1.369  qed
   1.370  
   1.371 -
   1.372  lemma iso_iff2:
   1.373  assumes "Well_order r"
   1.374  shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
   1.375 @@ -1110,7 +1056,6 @@
   1.376    thus "embed r r' f" unfolding embed_def using * by auto
   1.377  qed
   1.378  
   1.379 -
   1.380  lemma iso_iff3:
   1.381  assumes WELL: "Well_order r" and WELL': "Well_order r'"
   1.382  shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and> compat r r' f)"
   1.383 @@ -1140,6 +1085,4 @@
   1.384    qed
   1.385  qed
   1.386  
   1.387 -
   1.388 -
   1.389  end