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