src/HOL/Cardinals/Wellorder_Embedding.thy
 author wenzelm Fri Oct 27 13:50:08 2017 +0200 (23 months ago) changeset 66924 b4d4027f743b parent 66453 cc19f7ca2ed6 child 68652 1e37b45ce3fb permissions -rw-r--r--
more permissive;
```     1 (*  Title:      HOL/Cardinals/Wellorder_Embedding.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Well-order embeddings.
```
```     6 *)
```
```     7
```
```     8 section \<open>Well-Order Embeddings\<close>
```
```     9
```
```    10 theory Wellorder_Embedding
```
```    11 imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation
```
```    12 begin
```
```    13
```
```    14 subsection \<open>Auxiliaries\<close>
```
```    15
```
```    16 lemma UNION_bij_betw_ofilter:
```
```    17 assumes WELL: "Well_order r" and
```
```    18         OF: "\<And> i. i \<in> I \<Longrightarrow> ofilter r (A i)" and
```
```    19        BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
```
```    20 shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
```
```    21 proof-
```
```    22   have "wo_rel r" using WELL by (simp add: wo_rel_def)
```
```    23   hence "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i"
```
```    24   using wo_rel.ofilter_linord[of r] OF by blast
```
```    25   with WELL BIJ show ?thesis
```
```    26   by (auto simp add: bij_betw_UNION_chain)
```
```    27 qed
```
```    28
```
```    29
```
```    30 subsection \<open>(Well-order) embeddings, strict embeddings, isomorphisms and order-compatible
```
```    31 functions\<close>
```
```    32
```
```    33 lemma embed_halfcong:
```
```    34 assumes EQ: "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a" and
```
```    35         EMB: "embed r r' f"
```
```    36 shows "embed r r' g"
```
```    37 proof(unfold embed_def, auto)
```
```    38   fix a assume *: "a \<in> Field r"
```
```    39   hence "bij_betw f (under r a) (under r' (f a))"
```
```    40   using EMB unfolding embed_def by simp
```
```    41   moreover
```
```    42   {have "under r a \<le> Field r"
```
```    43    by (auto simp add: under_Field)
```
```    44    hence "\<And> b. b \<in> under r a \<Longrightarrow> f b = g b"
```
```    45    using EQ by blast
```
```    46   }
```
```    47   moreover have "f a = g a" using * EQ by auto
```
```    48   ultimately show "bij_betw g (under r a) (under r' (g a))"
```
```    49   using bij_betw_cong[of "under r a" f g "under r' (f a)"] by auto
```
```    50 qed
```
```    51
```
```    52 lemma embed_cong[fundef_cong]:
```
```    53 assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
```
```    54 shows "embed r r' f = embed r r' g"
```
```    55 using assms embed_halfcong[of r f g r']
```
```    56             embed_halfcong[of r g f r'] by auto
```
```    57
```
```    58 lemma embedS_cong[fundef_cong]:
```
```    59 assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
```
```    60 shows "embedS r r' f = embedS r r' g"
```
```    61 unfolding embedS_def using assms
```
```    62 embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
```
```    63
```
```    64 lemma iso_cong[fundef_cong]:
```
```    65 assumes "\<And> a. a \<in> Field r \<Longrightarrow> f a = g a"
```
```    66 shows "iso r r' f = iso r r' g"
```
```    67 unfolding iso_def using assms
```
```    68 embed_cong[of r f g r'] bij_betw_cong[of "Field r" f g "Field r'"] by blast
```
```    69
```
```    70 lemma id_compat: "compat r r id"
```
```    71 by(auto simp add: id_def compat_def)
```
```    72
```
```    73 lemma comp_compat:
```
```    74 "\<lbrakk>compat r r' f; compat r' r'' f'\<rbrakk> \<Longrightarrow> compat r r'' (f' o f)"
```
```    75 by(auto simp add: comp_def compat_def)
```
```    76
```
```    77 corollary one_set_greater:
```
```    78 "(\<exists>f::'a \<Rightarrow> 'a'. f ` A \<le> A' \<and> inj_on f A) \<or> (\<exists>g::'a' \<Rightarrow> 'a. g ` A' \<le> A \<and> inj_on g A')"
```
```    79 proof-
```
```    80   obtain r where "well_order_on A r" by (fastforce simp add: well_order_on)
```
```    81   hence 1: "A = Field r \<and> Well_order r"
```
```    82   using well_order_on_Well_order by auto
```
```    83   obtain r' where 2: "well_order_on A' r'" by (fastforce simp add: well_order_on)
```
```    84   hence 2: "A' = Field r' \<and> Well_order r'"
```
```    85   using well_order_on_Well_order by auto
```
```    86   hence "(\<exists>f. embed r r' f) \<or> (\<exists>g. embed r' r g)"
```
```    87   using 1 2 by (auto simp add: wellorders_totally_ordered)
```
```    88   moreover
```
```    89   {fix f assume "embed r r' f"
```
```    90    hence "f`A \<le> A' \<and> inj_on f A"
```
```    91    using 1 2 by (auto simp add: embed_Field embed_inj_on)
```
```    92   }
```
```    93   moreover
```
```    94   {fix g assume "embed r' r g"
```
```    95    hence "g`A' \<le> A \<and> inj_on g A'"
```
```    96    using 1 2 by (auto simp add: embed_Field embed_inj_on)
```
```    97   }
```
```    98   ultimately show ?thesis by blast
```
```    99 qed
```
```   100
```
```   101 corollary one_type_greater:
```
```   102 "(\<exists>f::'a \<Rightarrow> 'a'. inj f) \<or> (\<exists>g::'a' \<Rightarrow> 'a. inj g)"
```
```   103 using one_set_greater[of UNIV UNIV] by auto
```
```   104
```
```   105
```
```   106 subsection \<open>Uniqueness of embeddings\<close>
```
```   107
```
```   108 lemma comp_embedS:
```
```   109 assumes WELL: "Well_order r" and WELL': "Well_order r'" and WELL'': "Well_order r''"
```
```   110         and  EMB: "embedS r r' f" and EMB': "embedS r' r'' f'"
```
```   111 shows "embedS r r'' (f' o f)"
```
```   112 proof-
```
```   113   have "embed r' r'' f'" using EMB' unfolding embedS_def by simp
```
```   114   thus ?thesis using assms by (auto simp add: embedS_comp_embed)
```
```   115 qed
```
```   116
```
```   117 lemma iso_iff4:
```
```   118 assumes WELL: "Well_order r"  and WELL': "Well_order r'"
```
```   119 shows "iso r r' f = (embed r r' f \<and> embed r' r (inv_into (Field r) f))"
```
```   120 using assms embed_bothWays_iso
```
```   121 by(unfold iso_def, auto simp add: inv_into_Field_embed_bij_betw)
```
```   122
```
```   123 lemma embed_embedS_iso:
```
```   124 "embed r r' f = (embedS r r' f \<or> iso r r' f)"
```
```   125 unfolding embedS_def iso_def by blast
```
```   126
```
```   127 lemma not_embedS_iso:
```
```   128 "\<not> (embedS r r' f \<and> iso r r' f)"
```
```   129 unfolding embedS_def iso_def by blast
```
```   130
```
```   131 lemma embed_embedS_iff_not_iso:
```
```   132 assumes "embed r r' f"
```
```   133 shows "embedS r r' f = (\<not> iso r r' f)"
```
```   134 using assms unfolding embedS_def iso_def by blast
```
```   135
```
```   136 lemma iso_inv_into:
```
```   137 assumes WELL: "Well_order r" and ISO: "iso r r' f"
```
```   138 shows "iso r' r (inv_into (Field r) f)"
```
```   139 using assms unfolding iso_def
```
```   140 using bij_betw_inv_into inv_into_Field_embed_bij_betw by blast
```
```   141
```
```   142 lemma embedS_or_iso:
```
```   143 assumes WELL: "Well_order r" and WELL': "Well_order r'"
```
```   144 shows "(\<exists>g. embedS r r' g) \<or> (\<exists>h. embedS r' r h) \<or> (\<exists>f. iso r r' f)"
```
```   145 proof-
```
```   146   {fix f assume *: "embed r r' f"
```
```   147    {assume "bij_betw f (Field r) (Field r')"
```
```   148     hence ?thesis using * by (auto simp add: iso_def)
```
```   149    }
```
```   150    moreover
```
```   151    {assume "\<not> bij_betw f (Field r) (Field r')"
```
```   152     hence ?thesis using * by (auto simp add: embedS_def)
```
```   153    }
```
```   154    ultimately have ?thesis by auto
```
```   155   }
```
```   156   moreover
```
```   157   {fix f assume *: "embed r' r f"
```
```   158    {assume "bij_betw f (Field r') (Field r)"
```
```   159     hence "iso r' r f" using * by (auto simp add: iso_def)
```
```   160     hence "iso r r' (inv_into (Field r') f)"
```
```   161     using WELL' by (auto simp add: iso_inv_into)
```
```   162     hence ?thesis by blast
```
```   163    }
```
```   164    moreover
```
```   165    {assume "\<not> bij_betw f (Field r') (Field r)"
```
```   166     hence ?thesis using * by (auto simp add: embedS_def)
```
```   167    }
```
```   168    ultimately have ?thesis by auto
```
```   169   }
```
```   170   ultimately show ?thesis using WELL WELL'
```
```   171   wellorders_totally_ordered[of r r'] by blast
```
```   172 qed
```
```   173
```
```   174 end
```