|
1 (* Title: HOL/BNF/Basic_BNFs.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012 |
|
6 |
|
7 Registration of basic types as bounded natural functors. |
|
8 *) |
|
9 |
|
10 header {* Registration of Basic Types as Bounded Natural Functors *} |
|
11 |
|
12 theory Basic_BNFs |
|
13 imports BNF_Def |
|
14 begin |
|
15 |
|
16 lemma wpull_id: "wpull UNIV B1 B2 id id id id" |
|
17 unfolding wpull_def by simp |
|
18 |
|
19 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq] |
|
20 |
|
21 lemma ctwo_card_order: "card_order ctwo" |
|
22 using Card_order_ctwo by (unfold ctwo_def Field_card_of) |
|
23 |
|
24 lemma natLeq_cinfinite: "cinfinite natLeq" |
|
25 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
|
26 |
|
27 bnf_def ID: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
|
28 "\<lambda>x :: 'a \<Rightarrow> 'b \<Rightarrow> bool. x" |
|
29 apply auto |
|
30 apply (rule natLeq_card_order) |
|
31 apply (rule natLeq_cinfinite) |
|
32 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
|
33 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3] |
|
34 apply (rule ordLeq_transitive) |
|
35 apply (rule ordLeq_cexp1[of natLeq]) |
|
36 apply (rule Cinfinite_Cnotzero) |
|
37 apply (rule conjI) |
|
38 apply (rule natLeq_cinfinite) |
|
39 apply (rule natLeq_Card_order) |
|
40 apply (rule card_of_Card_order) |
|
41 apply (rule cexp_mono1) |
|
42 apply (rule ordLeq_csum1) |
|
43 apply (rule card_of_Card_order) |
|
44 apply (rule disjI2) |
|
45 apply (rule cone_ordLeq_cexp) |
|
46 apply (rule ordLeq_transitive) |
|
47 apply (rule cone_ordLeq_ctwo) |
|
48 apply (rule ordLeq_csum2) |
|
49 apply (rule Card_order_ctwo) |
|
50 apply (rule natLeq_Card_order) |
|
51 apply (auto simp: Gr_def fun_eq_iff) |
|
52 done |
|
53 |
|
54 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
|
55 "op =::'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
56 apply (auto simp add: wpull_id) |
|
57 apply (rule card_order_csum) |
|
58 apply (rule natLeq_card_order) |
|
59 apply (rule card_of_card_order_on) |
|
60 apply (rule cinfinite_csum) |
|
61 apply (rule disjI1) |
|
62 apply (rule natLeq_cinfinite) |
|
63 apply (rule ordLess_imp_ordLeq) |
|
64 apply (rule ordLess_ordLeq_trans) |
|
65 apply (rule ordLess_ctwo_cexp) |
|
66 apply (rule card_of_Card_order) |
|
67 apply (rule cexp_mono2'') |
|
68 apply (rule ordLeq_csum2) |
|
69 apply (rule card_of_Card_order) |
|
70 apply (rule ctwo_Cnotzero) |
|
71 apply (rule card_of_Card_order) |
|
72 apply (auto simp: Id_def Gr_def fun_eq_iff) |
|
73 done |
|
74 |
|
75 definition setl :: "'a + 'b \<Rightarrow> 'a set" where |
|
76 "setl x = (case x of Inl z => {z} | _ => {})" |
|
77 |
|
78 definition setr :: "'a + 'b \<Rightarrow> 'b set" where |
|
79 "setr x = (case x of Inr z => {z} | _ => {})" |
|
80 |
|
81 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def] |
|
82 |
|
83 definition sum_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool" where |
|
84 "sum_rel \<phi> \<psi> x y = |
|
85 (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False) |
|
86 | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))" |
|
87 |
|
88 bnf_def sum_map [setl, setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] sum_rel |
|
89 proof - |
|
90 show "sum_map id id = id" by (rule sum_map.id) |
|
91 next |
|
92 fix f1 f2 g1 g2 |
|
93 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
|
94 by (rule sum_map.comp[symmetric]) |
|
95 next |
|
96 fix x f1 f2 g1 g2 |
|
97 assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and |
|
98 a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z" |
|
99 thus "sum_map f1 f2 x = sum_map g1 g2 x" |
|
100 proof (cases x) |
|
101 case Inl thus ?thesis using a1 by (clarsimp simp: setl_def) |
|
102 next |
|
103 case Inr thus ?thesis using a2 by (clarsimp simp: setr_def) |
|
104 qed |
|
105 next |
|
106 fix f1 f2 |
|
107 show "setl o sum_map f1 f2 = image f1 o setl" |
|
108 by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split) |
|
109 next |
|
110 fix f1 f2 |
|
111 show "setr o sum_map f1 f2 = image f2 o setr" |
|
112 by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split) |
|
113 next |
|
114 show "card_order natLeq" by (rule natLeq_card_order) |
|
115 next |
|
116 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
117 next |
|
118 fix x |
|
119 show "|setl x| \<le>o natLeq" |
|
120 apply (rule ordLess_imp_ordLeq) |
|
121 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
|
122 by (simp add: setl_def split: sum.split) |
|
123 next |
|
124 fix x |
|
125 show "|setr x| \<le>o natLeq" |
|
126 apply (rule ordLess_imp_ordLeq) |
|
127 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
|
128 by (simp add: setr_def split: sum.split) |
|
129 next |
|
130 fix A1 :: "'a set" and A2 :: "'b set" |
|
131 have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and> |
|
132 (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R") |
|
133 proof safe |
|
134 fix x :: "'a + 'b" |
|
135 assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2" |
|
136 hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+ |
|
137 thus "x \<in> A1 <+> A2" by blast |
|
138 qed (auto split: sum.split) |
|
139 show "|{x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}| \<le>o |
|
140 (( |A1| +c |A2| ) +c ctwo) ^c natLeq" |
|
141 apply (rule ordIso_ordLeq_trans) |
|
142 apply (rule card_of_ordIso_subst) |
|
143 apply (unfold sum_set_defs) |
|
144 apply (rule in_alt) |
|
145 apply (rule ordIso_ordLeq_trans) |
|
146 apply (rule Plus_csum) |
|
147 apply (rule ordLeq_transitive) |
|
148 apply (rule ordLeq_csum1) |
|
149 apply (rule Card_order_csum) |
|
150 apply (rule ordLeq_cexp1) |
|
151 apply (rule conjI) |
|
152 using Field_natLeq UNIV_not_empty czeroE apply fast |
|
153 apply (rule natLeq_Card_order) |
|
154 by (rule Card_order_csum) |
|
155 next |
|
156 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
|
157 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
|
158 hence |
|
159 pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2" |
|
160 and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2" |
|
161 unfolding wpull_def by blast+ |
|
162 show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2} |
|
163 {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22} |
|
164 (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)" |
|
165 (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2") |
|
166 proof (unfold wpull_def) |
|
167 { fix B1 B2 |
|
168 assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2" |
|
169 have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2" |
|
170 proof (cases B1) |
|
171 case (Inl b1) |
|
172 { fix b2 assume "B2 = Inr b2" |
|
173 with Inl *(3) have False by simp |
|
174 } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast) |
|
175 with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2" |
|
176 by (simp add: setl_def)+ |
|
177 with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+ |
|
178 with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2" |
|
179 by (simp add: sum_set_defs)+ |
|
180 thus ?thesis by blast |
|
181 next |
|
182 case (Inr b1) |
|
183 { fix b2 assume "B2 = Inl b2" |
|
184 with Inr *(3) have False by simp |
|
185 } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast) |
|
186 with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2" |
|
187 by (simp add: sum_set_defs)+ |
|
188 with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+ |
|
189 with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2" |
|
190 by (simp add: sum_set_defs)+ |
|
191 thus ?thesis by blast |
|
192 qed |
|
193 } |
|
194 thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow> |
|
195 (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce |
|
196 qed |
|
197 next |
|
198 fix R S |
|
199 show "{p. sum_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} = |
|
200 (Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map fst fst))\<inverse> O |
|
201 Gr {x. setl x \<subseteq> R \<and> setr x \<subseteq> S} (sum_map snd snd)" |
|
202 unfolding setl_def setr_def sum_rel_def Gr_def relcomp_unfold converse_unfold |
|
203 by (fastforce split: sum.splits) |
|
204 qed (auto simp: sum_set_defs) |
|
205 |
|
206 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq" |
|
207 apply (rule ordLeq_transitive) |
|
208 apply (rule ordLeq_cprod2) |
|
209 apply (rule ctwo_Cnotzero) |
|
210 apply (auto simp: Field_card_of intro: card_of_card_order_on) |
|
211 apply (rule cprod_mono2) |
|
212 apply (rule ordLess_imp_ordLeq) |
|
213 apply (unfold finite_iff_ordLess_natLeq[symmetric]) |
|
214 by simp |
|
215 |
|
216 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where |
|
217 "fsts x = {fst x}" |
|
218 |
|
219 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
|
220 "snds x = {snd x}" |
|
221 |
|
222 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
|
223 |
|
224 definition prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" where |
|
225 "prod_rel \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> \<phi> a1 a2 \<and> \<psi> b1 b2)" |
|
226 |
|
227 bnf_def map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] prod_rel |
|
228 proof (unfold prod_set_defs) |
|
229 show "map_pair id id = id" by (rule map_pair.id) |
|
230 next |
|
231 fix f1 f2 g1 g2 |
|
232 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
|
233 by (rule map_pair.comp[symmetric]) |
|
234 next |
|
235 fix x f1 f2 g1 g2 |
|
236 assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z" |
|
237 thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp |
|
238 next |
|
239 fix f1 f2 |
|
240 show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})" |
|
241 by (rule ext, unfold o_apply) simp |
|
242 next |
|
243 fix f1 f2 |
|
244 show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})" |
|
245 by (rule ext, unfold o_apply) simp |
|
246 next |
|
247 show "card_order (ctwo *c natLeq)" |
|
248 apply (rule card_order_cprod) |
|
249 apply (rule ctwo_card_order) |
|
250 by (rule natLeq_card_order) |
|
251 next |
|
252 show "cinfinite (ctwo *c natLeq)" |
|
253 apply (rule cinfinite_cprod2) |
|
254 apply (rule ctwo_Cnotzero) |
|
255 apply (rule conjI[OF _ natLeq_Card_order]) |
|
256 by (rule natLeq_cinfinite) |
|
257 next |
|
258 fix x |
|
259 show "|{fst x}| \<le>o ctwo *c natLeq" |
|
260 by (rule singleton_ordLeq_ctwo_natLeq) |
|
261 next |
|
262 fix x |
|
263 show "|{snd x}| \<le>o ctwo *c natLeq" |
|
264 by (rule singleton_ordLeq_ctwo_natLeq) |
|
265 next |
|
266 fix A1 :: "'a set" and A2 :: "'b set" |
|
267 have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto |
|
268 show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o |
|
269 ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)" |
|
270 apply (rule ordIso_ordLeq_trans) |
|
271 apply (rule card_of_ordIso_subst) |
|
272 apply (rule in_alt) |
|
273 apply (rule ordIso_ordLeq_trans) |
|
274 apply (rule Times_cprod) |
|
275 apply (rule ordLeq_transitive) |
|
276 apply (rule cprod_csum_cexp) |
|
277 apply (rule cexp_mono) |
|
278 apply (rule ordLeq_csum1) |
|
279 apply (rule Card_order_csum) |
|
280 apply (rule ordLeq_cprod1) |
|
281 apply (rule Card_order_ctwo) |
|
282 apply (rule Cinfinite_Cnotzero) |
|
283 apply (rule conjI[OF _ natLeq_Card_order]) |
|
284 apply (rule natLeq_cinfinite) |
|
285 apply (rule disjI2) |
|
286 apply (rule cone_ordLeq_cexp) |
|
287 apply (rule ordLeq_transitive) |
|
288 apply (rule cone_ordLeq_ctwo) |
|
289 apply (rule ordLeq_csum2) |
|
290 apply (rule Card_order_ctwo) |
|
291 apply (rule notE) |
|
292 apply (rule ctwo_not_czero) |
|
293 apply assumption |
|
294 by (rule Card_order_ctwo) |
|
295 next |
|
296 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
|
297 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
|
298 thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} |
|
299 {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22} |
|
300 (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" |
|
301 unfolding wpull_def by simp fast |
|
302 next |
|
303 fix R S |
|
304 show "{p. prod_rel (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) (fst p) (snd p)} = |
|
305 (Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair fst fst))\<inverse> O |
|
306 Gr {x. {fst x} \<subseteq> R \<and> {snd x} \<subseteq> S} (map_pair snd snd)" |
|
307 unfolding prod_set_defs prod_rel_def Gr_def relcomp_unfold converse_unfold |
|
308 by auto |
|
309 qed simp+ |
|
310 |
|
311 (* Categorical version of pullback: *) |
|
312 lemma wpull_cat: |
|
313 assumes p: "wpull A B1 B2 f1 f2 p1 p2" |
|
314 and c: "f1 o q1 = f2 o q2" |
|
315 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2" |
|
316 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h" |
|
317 proof- |
|
318 have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d" |
|
319 proof safe |
|
320 fix d |
|
321 have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong) |
|
322 moreover |
|
323 have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto |
|
324 ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d" |
|
325 using p unfolding wpull_def by auto |
|
326 qed |
|
327 then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis |
|
328 thus ?thesis using that by fastforce |
|
329 qed |
|
330 |
|
331 lemma card_of_bounded_range: |
|
332 "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|") |
|
333 proof - |
|
334 let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None" |
|
335 have "inj_on ?f ?LHS" unfolding inj_on_def |
|
336 proof (unfold fun_eq_iff, safe) |
|
337 fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x |
|
338 assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x" |
|
339 hence "f x \<in> B" "g x \<in> B" by auto |
|
340 with eq have "Some (f x) = Some (g x)" by metis |
|
341 thus "f x = g x" by simp |
|
342 qed |
|
343 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
|
344 ultimately show ?thesis using card_of_ordLeq by fast |
|
345 qed |
|
346 |
|
347 definition fun_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b) \<Rightarrow> bool" where |
|
348 "fun_rel \<phi> f g = (\<forall>x. \<phi> (f x) (g x))" |
|
349 |
|
350 bnf_def "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" ["%c x::'b::type. c::'a::type"] |
|
351 fun_rel |
|
352 proof |
|
353 fix f show "id \<circ> f = id f" by simp |
|
354 next |
|
355 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
|
356 unfolding comp_def[abs_def] .. |
|
357 next |
|
358 fix x f g |
|
359 assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z" |
|
360 thus "f \<circ> x = g \<circ> x" by auto |
|
361 next |
|
362 fix f show "range \<circ> op \<circ> f = op ` f \<circ> range" |
|
363 unfolding image_def comp_def[abs_def] by auto |
|
364 next |
|
365 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") |
|
366 apply (rule card_order_csum) |
|
367 apply (rule natLeq_card_order) |
|
368 by (rule card_of_card_order_on) |
|
369 (* *) |
|
370 show "cinfinite (natLeq +c ?U)" |
|
371 apply (rule cinfinite_csum) |
|
372 apply (rule disjI1) |
|
373 by (rule natLeq_cinfinite) |
|
374 next |
|
375 fix f :: "'d => 'a" |
|
376 have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image) |
|
377 also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) |
|
378 finally show "|range f| \<le>o natLeq +c ?U" . |
|
379 next |
|
380 fix B :: "'a set" |
|
381 have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range) |
|
382 also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|" |
|
383 unfolding cexp_def Field_card_of by (rule card_of_refl) |
|
384 also have "|B| ^c |UNIV :: 'd set| \<le>o |
|
385 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" |
|
386 apply (rule cexp_mono) |
|
387 apply (rule ordLeq_csum1) apply (rule card_of_Card_order) |
|
388 apply (rule ordLeq_csum2) apply (rule card_of_Card_order) |
|
389 apply (rule disjI2) apply (rule cone_ordLeq_cexp) |
|
390 apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2) |
|
391 apply (rule Card_order_ctwo) |
|
392 apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast |
|
393 apply (rule card_of_Card_order) |
|
394 done |
|
395 finally |
|
396 show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |
|
397 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" . |
|
398 next |
|
399 fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2" |
|
400 show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2} |
|
401 (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)" |
|
402 unfolding wpull_def |
|
403 proof safe |
|
404 fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2" |
|
405 and c: "f1 \<circ> g1 = f2 \<circ> g2" |
|
406 show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2" |
|
407 using wpull_cat[OF p c r] by simp metis |
|
408 qed |
|
409 next |
|
410 fix R |
|
411 show "{p. fun_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} = |
|
412 (Gr {x. range x \<subseteq> R} (op \<circ> fst))\<inverse> O Gr {x. range x \<subseteq> R} (op \<circ> snd)" |
|
413 unfolding fun_rel_def Gr_def relcomp_unfold converse_unfold |
|
414 by (auto intro!: exI dest!: in_mono) |
|
415 qed auto |
|
416 |
|
417 end |