|
1 (* Title: HOL/Codatatype/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 various types as bounded natural functors. |
|
8 *) |
|
9 |
|
10 header {* Registration of Various Types as Bounded Natural Functors *} |
|
11 |
|
12 theory Basic_BNFs |
|
13 imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet" |
|
14 "~~/src/HOL/Library/Multiset" Countable_Set |
|
15 begin |
|
16 |
|
17 lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq] |
|
18 |
|
19 lemma ctwo_card_order: "card_order ctwo" |
|
20 using Card_order_ctwo by (unfold ctwo_def Field_card_of) |
|
21 |
|
22 lemma natLeq_cinfinite: "cinfinite natLeq" |
|
23 unfolding cinfinite_def Field_natLeq by (rule nat_infinite) |
|
24 |
|
25 bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"] |
|
26 apply auto |
|
27 apply (rule natLeq_card_order) |
|
28 apply (rule natLeq_cinfinite) |
|
29 apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]]) |
|
30 apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on) |
|
31 apply (rule ordLeq_transitive) |
|
32 apply (rule ordLeq_cexp1[of natLeq]) |
|
33 apply (rule Cinfinite_Cnotzero) |
|
34 apply (rule conjI) |
|
35 apply (rule natLeq_cinfinite) |
|
36 apply (rule natLeq_Card_order) |
|
37 apply (rule card_of_Card_order) |
|
38 apply (rule cexp_mono1) |
|
39 apply (rule ordLeq_csum1) |
|
40 apply (rule card_of_Card_order) |
|
41 apply (rule disjI2) |
|
42 apply (rule cone_ordLeq_cexp) |
|
43 apply (rule ordLeq_transitive) |
|
44 apply (rule cone_ordLeq_ctwo) |
|
45 apply (rule ordLeq_csum2) |
|
46 apply (rule Card_order_ctwo) |
|
47 apply (rule natLeq_Card_order) |
|
48 done |
|
49 |
|
50 lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>" |
|
51 unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto |
|
52 |
|
53 bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
|
54 apply (auto simp add: wpull_id) |
|
55 apply (rule card_order_csum) |
|
56 apply (rule natLeq_card_order) |
|
57 apply (rule card_of_card_order_on) |
|
58 apply (rule cinfinite_csum) |
|
59 apply (rule disjI1) |
|
60 apply (rule natLeq_cinfinite) |
|
61 apply (rule ordLess_imp_ordLeq) |
|
62 apply (rule ordLess_ordLeq_trans) |
|
63 apply (rule ordLess_ctwo_cexp) |
|
64 apply (rule card_of_Card_order) |
|
65 apply (rule cexp_mono2'') |
|
66 apply (rule ordLeq_csum2) |
|
67 apply (rule card_of_Card_order) |
|
68 apply (rule ctwo_Cnotzero) |
|
69 by (rule card_of_Card_order) |
|
70 |
|
71 lemma DEADID_pred[simp]: "DEADID_pred = (op =)" |
|
72 unfolding DEADID_pred_def DEADID.rel_Id by simp |
|
73 |
|
74 ML {* |
|
75 |
|
76 signature BASIC_BNFS = |
|
77 sig |
|
78 val ID_bnf: BNF_Def.BNF |
|
79 val ID_rel_def: thm |
|
80 val ID_pred_def: thm |
|
81 |
|
82 val DEADID_bnf: BNF_Def.BNF |
|
83 end; |
|
84 |
|
85 structure Basic_BNFs : BASIC_BNFS = |
|
86 struct |
|
87 |
|
88 val ID_bnf = the (BNF_Def.bnf_of @{context} "ID"); |
|
89 val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID"); |
|
90 |
|
91 val rel_def = BNF_Def.rel_def_of_bnf ID_bnf; |
|
92 val ID_rel_def = rel_def RS sym; |
|
93 val ID_pred_def = |
|
94 Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym; |
|
95 |
|
96 end; |
|
97 *} |
|
98 |
|
99 definition sum_setl :: "'a + 'b \<Rightarrow> 'a set" where |
|
100 "sum_setl x = (case x of Inl z => {z} | _ => {})" |
|
101 |
|
102 definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where |
|
103 "sum_setr x = (case x of Inr z => {z} | _ => {})" |
|
104 |
|
105 lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def] |
|
106 |
|
107 bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr] |
|
108 proof - |
|
109 show "sum_map id id = id" by (rule sum_map.id) |
|
110 next |
|
111 fix f1 f2 g1 g2 |
|
112 show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" |
|
113 by (rule sum_map.comp[symmetric]) |
|
114 next |
|
115 fix x f1 f2 g1 g2 |
|
116 assume a1: "\<And>z. z \<in> sum_setl x \<Longrightarrow> f1 z = g1 z" and |
|
117 a2: "\<And>z. z \<in> sum_setr x \<Longrightarrow> f2 z = g2 z" |
|
118 thus "sum_map f1 f2 x = sum_map g1 g2 x" |
|
119 proof (cases x) |
|
120 case Inl thus ?thesis using a1 by (clarsimp simp: sum_setl_def) |
|
121 next |
|
122 case Inr thus ?thesis using a2 by (clarsimp simp: sum_setr_def) |
|
123 qed |
|
124 next |
|
125 fix f1 f2 |
|
126 show "sum_setl o sum_map f1 f2 = image f1 o sum_setl" |
|
127 by (rule ext, unfold o_apply) (simp add: sum_setl_def split: sum.split) |
|
128 next |
|
129 fix f1 f2 |
|
130 show "sum_setr o sum_map f1 f2 = image f2 o sum_setr" |
|
131 by (rule ext, unfold o_apply) (simp add: sum_setr_def split: sum.split) |
|
132 next |
|
133 show "card_order natLeq" by (rule natLeq_card_order) |
|
134 next |
|
135 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
136 next |
|
137 fix x |
|
138 show "|sum_setl x| \<le>o natLeq" |
|
139 apply (rule ordLess_imp_ordLeq) |
|
140 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
|
141 by (simp add: sum_setl_def split: sum.split) |
|
142 next |
|
143 fix x |
|
144 show "|sum_setr x| \<le>o natLeq" |
|
145 apply (rule ordLess_imp_ordLeq) |
|
146 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
|
147 by (simp add: sum_setr_def split: sum.split) |
|
148 next |
|
149 fix A1 :: "'a set" and A2 :: "'b set" |
|
150 have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and> |
|
151 (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R") |
|
152 proof safe |
|
153 fix x :: "'a + 'b" |
|
154 assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2" |
|
155 hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+ |
|
156 thus "x \<in> A1 <+> A2" by blast |
|
157 qed (auto split: sum.split) |
|
158 show "|{x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}| \<le>o |
|
159 (( |A1| +c |A2| ) +c ctwo) ^c natLeq" |
|
160 apply (rule ordIso_ordLeq_trans) |
|
161 apply (rule card_of_ordIso_subst) |
|
162 apply (unfold sum_set_defs) |
|
163 apply (rule in_alt) |
|
164 apply (rule ordIso_ordLeq_trans) |
|
165 apply (rule Plus_csum) |
|
166 apply (rule ordLeq_transitive) |
|
167 apply (rule ordLeq_csum1) |
|
168 apply (rule Card_order_csum) |
|
169 apply (rule ordLeq_cexp1) |
|
170 apply (rule conjI) |
|
171 using Field_natLeq UNIV_not_empty czeroE apply fast |
|
172 apply (rule natLeq_Card_order) |
|
173 by (rule Card_order_csum) |
|
174 next |
|
175 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
|
176 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
|
177 hence |
|
178 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" |
|
179 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" |
|
180 unfolding wpull_def by blast+ |
|
181 show "wpull {x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2} |
|
182 {x. sum_setl x \<subseteq> B11 \<and> sum_setr x \<subseteq> B12} {x. sum_setl x \<subseteq> B21 \<and> sum_setr x \<subseteq> B22} |
|
183 (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)" |
|
184 (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2") |
|
185 proof (unfold wpull_def) |
|
186 { fix B1 B2 |
|
187 assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2" |
|
188 have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2" |
|
189 proof (cases B1) |
|
190 case (Inl b1) |
|
191 { fix b2 assume "B2 = Inr b2" |
|
192 with Inl *(3) have False by simp |
|
193 } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast) |
|
194 with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2" |
|
195 by (simp add: sum_setl_def)+ |
|
196 with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+ |
|
197 with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2" |
|
198 by (simp add: sum_set_defs)+ |
|
199 thus ?thesis by blast |
|
200 next |
|
201 case (Inr b1) |
|
202 { fix b2 assume "B2 = Inl b2" |
|
203 with Inr *(3) have False by simp |
|
204 } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast) |
|
205 with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2" |
|
206 by (simp add: sum_set_defs)+ |
|
207 with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+ |
|
208 with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2" |
|
209 by (simp add: sum_set_defs)+ |
|
210 thus ?thesis by blast |
|
211 qed |
|
212 } |
|
213 thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow> |
|
214 (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce |
|
215 qed |
|
216 qed (auto simp: sum_set_defs) |
|
217 |
|
218 lemma sum_pred[simp]: |
|
219 "sum_pred \<phi> \<psi> x y = |
|
220 (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False) |
|
221 | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))" |
|
222 unfolding sum_setl_def sum_setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold |
|
223 by (fastforce split: sum.splits)+ |
|
224 |
|
225 lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq" |
|
226 apply (rule ordLeq_transitive) |
|
227 apply (rule ordLeq_cprod2) |
|
228 apply (rule ctwo_Cnotzero) |
|
229 apply (auto simp: Field_card_of intro: card_of_card_order_on) |
|
230 apply (rule cprod_mono2) |
|
231 apply (rule ordLess_imp_ordLeq) |
|
232 apply (unfold finite_iff_ordLess_natLeq[symmetric]) |
|
233 by simp |
|
234 |
|
235 definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where |
|
236 "fsts x = {fst x}" |
|
237 |
|
238 definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where |
|
239 "snds x = {snd x}" |
|
240 |
|
241 lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def] |
|
242 |
|
243 bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair] |
|
244 proof (unfold prod_set_defs) |
|
245 show "map_pair id id = id" by (rule map_pair.id) |
|
246 next |
|
247 fix f1 f2 g1 g2 |
|
248 show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" |
|
249 by (rule map_pair.comp[symmetric]) |
|
250 next |
|
251 fix x f1 f2 g1 g2 |
|
252 assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z" |
|
253 thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp |
|
254 next |
|
255 fix f1 f2 |
|
256 show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})" |
|
257 by (rule ext, unfold o_apply) simp |
|
258 next |
|
259 fix f1 f2 |
|
260 show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})" |
|
261 by (rule ext, unfold o_apply) simp |
|
262 next |
|
263 show "card_order (ctwo *c natLeq)" |
|
264 apply (rule card_order_cprod) |
|
265 apply (rule ctwo_card_order) |
|
266 by (rule natLeq_card_order) |
|
267 next |
|
268 show "cinfinite (ctwo *c natLeq)" |
|
269 apply (rule cinfinite_cprod2) |
|
270 apply (rule ctwo_Cnotzero) |
|
271 apply (rule conjI[OF _ natLeq_Card_order]) |
|
272 by (rule natLeq_cinfinite) |
|
273 next |
|
274 fix x |
|
275 show "|{fst x}| \<le>o ctwo *c natLeq" |
|
276 by (rule singleton_ordLeq_ctwo_natLeq) |
|
277 next |
|
278 fix x |
|
279 show "|{snd x}| \<le>o ctwo *c natLeq" |
|
280 by (rule singleton_ordLeq_ctwo_natLeq) |
|
281 next |
|
282 fix A1 :: "'a set" and A2 :: "'b set" |
|
283 have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto |
|
284 show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o |
|
285 ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)" |
|
286 apply (rule ordIso_ordLeq_trans) |
|
287 apply (rule card_of_ordIso_subst) |
|
288 apply (rule in_alt) |
|
289 apply (rule ordIso_ordLeq_trans) |
|
290 apply (rule Times_cprod) |
|
291 apply (rule ordLeq_transitive) |
|
292 apply (rule cprod_csum_cexp) |
|
293 apply (rule cexp_mono) |
|
294 apply (rule ordLeq_csum1) |
|
295 apply (rule Card_order_csum) |
|
296 apply (rule ordLeq_cprod1) |
|
297 apply (rule Card_order_ctwo) |
|
298 apply (rule Cinfinite_Cnotzero) |
|
299 apply (rule conjI[OF _ natLeq_Card_order]) |
|
300 apply (rule natLeq_cinfinite) |
|
301 apply (rule disjI2) |
|
302 apply (rule cone_ordLeq_cexp) |
|
303 apply (rule ordLeq_transitive) |
|
304 apply (rule cone_ordLeq_ctwo) |
|
305 apply (rule ordLeq_csum2) |
|
306 apply (rule Card_order_ctwo) |
|
307 apply (rule notE) |
|
308 apply (rule ctwo_not_czero) |
|
309 apply assumption |
|
310 by (rule Card_order_ctwo) |
|
311 next |
|
312 fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22 |
|
313 assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22" |
|
314 thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} |
|
315 {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22} |
|
316 (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)" |
|
317 unfolding wpull_def by simp fast |
|
318 qed simp+ |
|
319 |
|
320 lemma prod_pred[simp]: |
|
321 "prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> (\<phi> a1 a2 \<and> \<psi> b1 b2))" |
|
322 unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto |
|
323 (* TODO: pred characterization for each basic BNF *) |
|
324 |
|
325 (* Categorical version of pullback: *) |
|
326 lemma wpull_cat: |
|
327 assumes p: "wpull A B1 B2 f1 f2 p1 p2" |
|
328 and c: "f1 o q1 = f2 o q2" |
|
329 and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2" |
|
330 obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h" |
|
331 proof- |
|
332 have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d" |
|
333 proof safe |
|
334 fix d |
|
335 have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong) |
|
336 moreover |
|
337 have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto |
|
338 ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d" |
|
339 using p unfolding wpull_def by auto |
|
340 qed |
|
341 then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis |
|
342 thus ?thesis using that by fastforce |
|
343 qed |
|
344 |
|
345 lemma card_of_bounded_range: |
|
346 "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|") |
|
347 proof - |
|
348 let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None" |
|
349 have "inj_on ?f ?LHS" unfolding inj_on_def |
|
350 proof (unfold fun_eq_iff, safe) |
|
351 fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x |
|
352 assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x" |
|
353 hence "f x \<in> B" "g x \<in> B" by auto |
|
354 with eq have "Some (f x) = Some (g x)" by metis |
|
355 thus "f x = g x" by simp |
|
356 qed |
|
357 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce |
|
358 ultimately show ?thesis using card_of_ordLeq by fast |
|
359 qed |
|
360 |
|
361 bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|" |
|
362 ["%c x::'b::type. c::'a::type"] |
|
363 proof |
|
364 fix f show "id \<circ> f = id f" by simp |
|
365 next |
|
366 fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f" |
|
367 unfolding comp_def[abs_def] .. |
|
368 next |
|
369 fix x f g |
|
370 assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z" |
|
371 thus "f \<circ> x = g \<circ> x" by auto |
|
372 next |
|
373 fix f show "range \<circ> op \<circ> f = op ` f \<circ> range" |
|
374 unfolding image_def comp_def[abs_def] by auto |
|
375 next |
|
376 show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)") |
|
377 apply (rule card_order_csum) |
|
378 apply (rule natLeq_card_order) |
|
379 by (rule card_of_card_order_on) |
|
380 (* *) |
|
381 show "cinfinite (natLeq +c ?U)" |
|
382 apply (rule cinfinite_csum) |
|
383 apply (rule disjI1) |
|
384 by (rule natLeq_cinfinite) |
|
385 next |
|
386 fix f :: "'d => 'a" |
|
387 have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image) |
|
388 also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order) |
|
389 finally show "|range f| \<le>o natLeq +c ?U" . |
|
390 next |
|
391 fix B :: "'a set" |
|
392 have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range) |
|
393 also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|" |
|
394 unfolding cexp_def Field_card_of by (rule card_of_refl) |
|
395 also have "|B| ^c |UNIV :: 'd set| \<le>o |
|
396 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" |
|
397 apply (rule cexp_mono) |
|
398 apply (rule ordLeq_csum1) apply (rule card_of_Card_order) |
|
399 apply (rule ordLeq_csum2) apply (rule card_of_Card_order) |
|
400 apply (rule disjI2) apply (rule cone_ordLeq_cexp) |
|
401 apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2) |
|
402 apply (rule Card_order_ctwo) |
|
403 apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast |
|
404 apply (rule card_of_Card_order) |
|
405 done |
|
406 finally |
|
407 show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |
|
408 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" . |
|
409 next |
|
410 fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2" |
|
411 show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2} |
|
412 (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)" |
|
413 unfolding wpull_def |
|
414 proof safe |
|
415 fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2" |
|
416 and c: "f1 \<circ> g1 = f2 \<circ> g2" |
|
417 show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2" |
|
418 using wpull_cat[OF p c r] by simp metis |
|
419 qed |
|
420 qed auto |
|
421 |
|
422 lemma fun_pred[simp]: "fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))" |
|
423 unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold |
|
424 by (auto intro!: exI dest!: in_mono) |
|
425 |
|
426 lemma card_of_list_in: |
|
427 "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|") |
|
428 proof - |
|
429 let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None" |
|
430 have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff |
|
431 proof safe |
|
432 fix xs :: "'a list" and ys :: "'a list" |
|
433 assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i" |
|
434 hence *: "length xs = length ys" |
|
435 by (metis linorder_cases option.simps(2) order_less_irrefl) |
|
436 thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject) |
|
437 qed |
|
438 moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce |
|
439 ultimately show ?thesis using card_of_ordLeq by blast |
|
440 qed |
|
441 |
|
442 lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}" |
|
443 by simp |
|
444 |
|
445 lemma card_of_Func: "|Func A B| =o |B| ^c |A|" |
|
446 unfolding cexp_def Field_card_of by (rule card_of_refl) |
|
447 |
|
448 lemma not_emp_czero_notIn_ordIso_Card_order: |
|
449 "A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|" |
|
450 apply (rule conjI) |
|
451 apply (metis Field_card_of czeroE) |
|
452 by (rule card_of_Card_order) |
|
453 |
|
454 lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" |
|
455 proof - |
|
456 fix A :: "'a set" |
|
457 show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" |
|
458 proof (cases "A = {}") |
|
459 case False thus ?thesis |
|
460 apply - |
|
461 apply (rule ordLeq_transitive) |
|
462 apply (rule card_of_list_in) |
|
463 apply (rule ordLeq_transitive) |
|
464 apply (erule card_of_Pfunc_Pow_Func) |
|
465 apply (rule ordIso_ordLeq_trans) |
|
466 apply (rule Times_cprod) |
|
467 apply (rule cprod_cinfinite_bound) |
|
468 apply (rule ordIso_ordLeq_trans) |
|
469 apply (rule Pow_cexp_ctwo) |
|
470 apply (rule ordIso_ordLeq_trans) |
|
471 apply (rule cexp_cong2) |
|
472 apply (rule card_of_nat) |
|
473 apply (rule Card_order_ctwo) |
|
474 apply (rule card_of_Card_order) |
|
475 apply (rule natLeq_Card_order) |
|
476 apply (rule disjI1) |
|
477 apply (rule ctwo_Cnotzero) |
|
478 apply (rule cexp_mono1) |
|
479 apply (rule ordLeq_csum2) |
|
480 apply (rule Card_order_ctwo) |
|
481 apply (rule disjI1) |
|
482 apply (rule ctwo_Cnotzero) |
|
483 apply (rule natLeq_Card_order) |
|
484 apply (rule ordIso_ordLeq_trans) |
|
485 apply (rule card_of_Func) |
|
486 apply (rule ordIso_ordLeq_trans) |
|
487 apply (rule cexp_cong2) |
|
488 apply (rule card_of_nat) |
|
489 apply (rule card_of_Card_order) |
|
490 apply (rule card_of_Card_order) |
|
491 apply (rule natLeq_Card_order) |
|
492 apply (rule disjI1) |
|
493 apply (erule not_emp_czero_notIn_ordIso_Card_order) |
|
494 apply (rule cexp_mono1) |
|
495 apply (rule ordLeq_csum1) |
|
496 apply (rule card_of_Card_order) |
|
497 apply (rule disjI1) |
|
498 apply (erule not_emp_czero_notIn_ordIso_Card_order) |
|
499 apply (rule natLeq_Card_order) |
|
500 apply (rule card_of_Card_order) |
|
501 apply (rule card_of_Card_order) |
|
502 apply (rule Cinfinite_cexp) |
|
503 apply (rule ordLeq_csum2) |
|
504 apply (rule Card_order_ctwo) |
|
505 apply (rule conjI) |
|
506 apply (rule natLeq_cinfinite) |
|
507 by (rule natLeq_Card_order) |
|
508 next |
|
509 case True thus ?thesis |
|
510 apply - |
|
511 apply (rule ordIso_ordLeq_trans) |
|
512 apply (rule card_of_ordIso_subst) |
|
513 apply (erule list_in_empty) |
|
514 apply (rule ordIso_ordLeq_trans) |
|
515 apply (rule single_cone) |
|
516 apply (rule cone_ordLeq_cexp) |
|
517 apply (rule ordLeq_transitive) |
|
518 apply (rule cone_ordLeq_ctwo) |
|
519 apply (rule ordLeq_csum2) |
|
520 by (rule Card_order_ctwo) |
|
521 qed |
|
522 qed |
|
523 |
|
524 bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"] |
|
525 proof - |
|
526 show "map id = id" by (rule List.map.id) |
|
527 next |
|
528 fix f g |
|
529 show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric]) |
|
530 next |
|
531 fix x f g |
|
532 assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z" |
|
533 thus "map f x = map g x" by simp |
|
534 next |
|
535 fix f |
|
536 show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map) |
|
537 next |
|
538 show "card_order natLeq" by (rule natLeq_card_order) |
|
539 next |
|
540 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
541 next |
|
542 fix x |
|
543 show "|set x| \<le>o natLeq" |
|
544 apply (rule ordLess_imp_ordLeq) |
|
545 apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order]) |
|
546 unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on) |
|
547 next |
|
548 fix A :: "'a set" |
|
549 show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd) |
|
550 next |
|
551 fix A B1 B2 f1 f2 p1 p2 |
|
552 assume "wpull A B1 B2 f1 f2 p1 p2" |
|
553 hence pull: "\<And>b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<Longrightarrow> \<exists>a \<in> A. p1 a = b1 \<and> p2 a = b2" |
|
554 unfolding wpull_def by auto |
|
555 show "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)" |
|
556 (is "wpull ?A ?B1 ?B2 _ _ _ _") |
|
557 proof (unfold wpull_def) |
|
558 { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs" |
|
559 hence "length as = length bs" by (metis length_map) |
|
560 hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using * |
|
561 proof (induct as bs rule: list_induct2) |
|
562 case (Cons a as b bs) |
|
563 hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto |
|
564 with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast |
|
565 moreover |
|
566 from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto |
|
567 ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto |
|
568 thus ?case by (rule_tac x = "z # zs" in bexI) |
|
569 qed simp |
|
570 } |
|
571 thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow> |
|
572 (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast |
|
573 qed |
|
574 qed auto |
|
575 |
|
576 bnf_def deadlist = "map id" [] "\<lambda>_::'a list. |lists (UNIV :: 'a set)|" ["[]"] |
|
577 by (auto simp add: cinfinite_def wpull_def infinite_UNIV_listI map.id |
|
578 ordLeq_transitive ctwo_def card_of_card_order_on Field_card_of card_of_mono1 ordLeq_cexp2) |
|
579 |
|
580 (* Finite sets *) |
|
581 abbreviation afset where "afset \<equiv> abs_fset" |
|
582 abbreviation rfset where "rfset \<equiv> rep_fset" |
|
583 |
|
584 lemma fset_fset_member: |
|
585 "fset A = {a. a |\<in>| A}" |
|
586 unfolding fset_def fset_member_def by auto |
|
587 |
|
588 lemma afset_rfset: |
|
589 "afset (rfset x) = x" |
|
590 by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format]) |
|
591 |
|
592 lemma afset_rfset_id: |
|
593 "afset o rfset = id" |
|
594 unfolding comp_def afset_rfset id_def .. |
|
595 |
|
596 lemma rfset: |
|
597 "rfset A = rfset B \<longleftrightarrow> A = B" |
|
598 by (metis afset_rfset) |
|
599 |
|
600 lemma afset_set: |
|
601 "afset as = afset bs \<longleftrightarrow> set as = set bs" |
|
602 using Quotient_fset unfolding Quotient_def list_eq_def by auto |
|
603 |
|
604 lemma surj_afset: |
|
605 "\<exists> as. A = afset as" |
|
606 by (metis afset_rfset) |
|
607 |
|
608 lemma fset_def2: |
|
609 "fset = set o rfset" |
|
610 unfolding fset_def map_fun_def[abs_def] by simp |
|
611 |
|
612 lemma fset_def2_raw: |
|
613 "fset A = set (rfset A)" |
|
614 unfolding fset_def2 by simp |
|
615 |
|
616 lemma fset_comp_afset: |
|
617 "fset o afset = set" |
|
618 unfolding fset_def2 comp_def apply(rule ext) |
|
619 unfolding afset_set[symmetric] afset_rfset .. |
|
620 |
|
621 lemma fset_afset: |
|
622 "fset (afset as) = set as" |
|
623 unfolding fset_comp_afset[symmetric] by simp |
|
624 |
|
625 lemma set_rfset_afset: |
|
626 "set (rfset (afset as)) = set as" |
|
627 unfolding afset_set[symmetric] afset_rfset .. |
|
628 |
|
629 lemma map_fset_comp_afset: |
|
630 "(map_fset f) o afset = afset o (map f)" |
|
631 unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext) |
|
632 unfolding afset_set set_map set_rfset_afset id_apply .. |
|
633 |
|
634 lemma map_fset_afset: |
|
635 "(map_fset f) (afset as) = afset (map f as)" |
|
636 using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto |
|
637 |
|
638 lemma fset_map_fset: |
|
639 "fset (map_fset f A) = (image f) (fset A)" |
|
640 apply(subst afset_rfset[symmetric, of A]) |
|
641 unfolding map_fset_afset fset_afset set_map |
|
642 unfolding fset_def2_raw .. |
|
643 |
|
644 lemma map_fset_def2: |
|
645 "map_fset f = afset o (map f) o rfset" |
|
646 unfolding map_fset_def map_fun_def[abs_def] by simp |
|
647 |
|
648 lemma map_fset_def2_raw: |
|
649 "map_fset f A = afset (map f (rfset A))" |
|
650 unfolding map_fset_def2 by simp |
|
651 |
|
652 lemma finite_ex_fset: |
|
653 assumes "finite A" |
|
654 shows "\<exists> B. fset B = A" |
|
655 by (metis assms finite_list fset_afset) |
|
656 |
|
657 lemma wpull_image: |
|
658 assumes "wpull A B1 B2 f1 f2 p1 p2" |
|
659 shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)" |
|
660 unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify |
|
661 fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2" |
|
662 def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}" |
|
663 show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2" |
|
664 proof (rule exI[of _ X], intro conjI) |
|
665 show "p1 ` X = Y1" |
|
666 proof |
|
667 show "Y1 \<subseteq> p1 ` X" |
|
668 proof safe |
|
669 fix y1 assume y1: "y1 \<in> Y1" |
|
670 then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto |
|
671 then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2" |
|
672 using assms y1 Y1 Y2 unfolding wpull_def by blast |
|
673 thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto |
|
674 qed |
|
675 qed(unfold X_def, auto) |
|
676 show "p2 ` X = Y2" |
|
677 proof |
|
678 show "Y2 \<subseteq> p2 ` X" |
|
679 proof safe |
|
680 fix y2 assume y2: "y2 \<in> Y2" |
|
681 then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force |
|
682 then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2" |
|
683 using assms y2 Y1 Y2 unfolding wpull_def by blast |
|
684 thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto |
|
685 qed |
|
686 qed(unfold X_def, auto) |
|
687 qed(unfold X_def, auto) |
|
688 qed |
|
689 |
|
690 lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A" |
|
691 by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset) |
|
692 |
|
693 bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] |
|
694 proof - |
|
695 show "map_fset id = id" |
|
696 unfolding map_fset_def2 map_id o_id afset_rfset_id .. |
|
697 next |
|
698 fix f g |
|
699 show "map_fset (g o f) = map_fset g o map_fset f" |
|
700 unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext) |
|
701 unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric] |
|
702 unfolding map_fset_afset[symmetric] map_fset_image afset_rfset |
|
703 by (rule refl) |
|
704 next |
|
705 fix x f g |
|
706 assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z" |
|
707 hence "map f (rfset x) = map g (rfset x)" |
|
708 apply(intro map_cong) unfolding fset_def2_raw by auto |
|
709 thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw |
|
710 by (rule arg_cong) |
|
711 next |
|
712 fix f |
|
713 show "fset o map_fset f = image f o fset" |
|
714 unfolding comp_def fset_map_fset .. |
|
715 next |
|
716 show "card_order natLeq" by (rule natLeq_card_order) |
|
717 next |
|
718 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
719 next |
|
720 fix x |
|
721 show "|fset x| \<le>o natLeq" |
|
722 unfolding fset_def2_raw |
|
723 apply (rule ordLess_imp_ordLeq) |
|
724 apply (rule finite_iff_ordLess_natLeq[THEN iffD1]) |
|
725 by (rule finite_set) |
|
726 next |
|
727 fix A :: "'a set" |
|
728 have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|" |
|
729 apply(rule card_of_mono1) unfolding fset_def2_raw apply auto |
|
730 apply (rule image_eqI) |
|
731 by (auto simp: afset_rfset) |
|
732 also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image . |
|
733 also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd) |
|
734 finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" . |
|
735 next |
|
736 fix A B1 B2 f1 f2 p1 p2 |
|
737 assume wp: "wpull A B1 B2 f1 f2 p1 p2" |
|
738 hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)" |
|
739 by(rule wpull_image) |
|
740 show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2} |
|
741 (map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)" |
|
742 unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify |
|
743 fix y1 y2 |
|
744 assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2" |
|
745 assume "map_fset f1 y1 = map_fset f2 y2" |
|
746 hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw |
|
747 unfolding afset_set set_map fset_def2_raw . |
|
748 with Y1 Y2 obtain X where X: "X \<subseteq> A" |
|
749 and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2" |
|
750 using wpull_image[OF wp] unfolding wpull_def Pow_def |
|
751 unfolding Bex_def mem_Collect_eq apply - |
|
752 apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto |
|
753 have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto |
|
754 then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis |
|
755 have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto |
|
756 then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis |
|
757 def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)" |
|
758 have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2" |
|
759 using X Y1 Y2 q1 q2 unfolding X'_def by auto |
|
760 have fX': "finite X'" unfolding X'_def by simp |
|
761 then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset) |
|
762 show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2" |
|
763 apply(intro exI[of _ "x"]) using X' Y1 Y2 |
|
764 unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric] |
|
765 afset_set[symmetric] afset_rfset by simp |
|
766 qed |
|
767 qed auto |
|
768 |
|
769 lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow> |
|
770 ((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and> |
|
771 (\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R") |
|
772 proof |
|
773 assume ?L thus ?R unfolding fset_rel_def fset_pred_def |
|
774 Gr_def relcomp_unfold converse_unfold |
|
775 apply (simp add: subset_eq Ball_def) |
|
776 apply (rule conjI) |
|
777 apply (clarsimp, metis snd_conv) |
|
778 by (clarsimp, metis fst_conv) |
|
779 next |
|
780 assume ?R |
|
781 def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'") |
|
782 have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto |
|
783 hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset) |
|
784 show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold |
|
785 proof (intro CollectI prod_caseI exI conjI) |
|
786 from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`] |
|
787 by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) |
|
788 from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`] |
|
789 by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits) |
|
790 qed (auto simp add: *) |
|
791 qed |
|
792 |
|
793 (* Countable sets *) |
|
794 |
|
795 lemma card_of_countable_sets_range: |
|
796 fixes A :: "'a set" |
|
797 shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|" |
|
798 apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat |
|
799 unfolding inj_on_def by auto |
|
800 |
|
801 lemma card_of_countable_sets_Func: |
|
802 "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq" |
|
803 using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric] |
|
804 unfolding cexp_def Field_natLeq Field_card_of |
|
805 by(rule ordLeq_ordIso_trans) |
|
806 |
|
807 lemma ordLeq_countable_subsets: |
|
808 "|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|" |
|
809 apply(rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto |
|
810 |
|
811 lemma finite_countable_subset: |
|
812 "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A" |
|
813 apply default |
|
814 apply (erule contrapos_pp) |
|
815 apply (rule card_of_ordLeq_infinite) |
|
816 apply (rule ordLeq_countable_subsets) |
|
817 apply assumption |
|
818 apply (rule finite_Collect_conjI) |
|
819 apply (rule disjI1) |
|
820 by (erule finite_Collect_subsets) |
|
821 |
|
822 lemma card_of_countable_sets: |
|
823 "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq" |
|
824 (is "|?L| \<le>o _") |
|
825 proof(cases "finite A") |
|
826 let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))" |
|
827 case True hence "finite ?L" by simp |
|
828 moreover have "infinite ?R" |
|
829 apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto |
|
830 ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of |
|
831 apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2) |
|
832 next |
|
833 case False |
|
834 hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|" |
|
835 by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric) |
|
836 (unfold finite_countable_subset) |
|
837 also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq" |
|
838 using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto |
|
839 also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq" |
|
840 apply(rule cexp_mono1_cone_ordLeq) |
|
841 apply(rule ordLeq_csum1, rule card_of_Card_order) |
|
842 apply (rule cone_ordLeq_cexp) |
|
843 apply (rule cone_ordLeq_Cnotzero) |
|
844 using csum_Cnotzero2 ctwo_Cnotzero apply blast |
|
845 by (rule natLeq_Card_order) |
|
846 finally show ?thesis . |
|
847 qed |
|
848 |
|
849 bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"] |
|
850 proof - |
|
851 show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto |
|
852 next |
|
853 fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f" |
|
854 unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto |
|
855 next |
|
856 fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a" |
|
857 thus "cIm f C = cIm g C" |
|
858 unfolding cIm_def[abs_def] unfolding image_def by auto |
|
859 next |
|
860 fix f show "rcset \<circ> cIm f = op ` f \<circ> rcset" unfolding cIm_def[abs_def] by auto |
|
861 next |
|
862 show "card_order natLeq" by (rule natLeq_card_order) |
|
863 next |
|
864 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
865 next |
|
866 fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def . |
|
867 next |
|
868 fix A :: "'a set" |
|
869 have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|" |
|
870 apply(rule card_of_mono1) unfolding Pow_def image_def |
|
871 proof (rule Collect_mono, clarsimp) |
|
872 fix x |
|
873 assume "rcset x \<subseteq> A" |
|
874 hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)" |
|
875 using acset_rcset[of x] rcset[of x] by force |
|
876 thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast |
|
877 qed |
|
878 also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|" |
|
879 using card_of_image . |
|
880 also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq" |
|
881 using card_of_countable_sets . |
|
882 finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" . |
|
883 next |
|
884 fix A B1 B2 f1 f2 p1 p2 |
|
885 assume wp: "wpull A B1 B2 f1 f2 p1 p2" |
|
886 show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2} |
|
887 (cIm f1) (cIm f2) (cIm p1) (cIm p2)" |
|
888 unfolding wpull_def proof safe |
|
889 fix y1 y2 |
|
890 assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2" |
|
891 assume "cIm f1 y1 = cIm f2 y2" |
|
892 hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" |
|
893 unfolding cIm_def by auto |
|
894 with Y1 Y2 obtain X where X: "X \<subseteq> A" |
|
895 and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2" |
|
896 using wpull_image[OF wp] unfolding wpull_def Pow_def |
|
897 unfolding Bex_def mem_Collect_eq apply - |
|
898 apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto |
|
899 have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto |
|
900 then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis |
|
901 have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto |
|
902 then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis |
|
903 def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)" |
|
904 have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2" |
|
905 using X Y1 Y2 q1 q2 unfolding X'_def by fast+ |
|
906 have fX': "countable X'" unfolding X'_def by simp |
|
907 then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset) |
|
908 show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cIm p1 x = y1 \<and> cIm p2 x = y2" |
|
909 apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto |
|
910 qed |
|
911 qed (unfold cEmp_def, auto) |
|
912 |
|
913 |
|
914 (* Multisets *) |
|
915 |
|
916 lemma setsum_gt_0_iff: |
|
917 fixes f :: "'a \<Rightarrow> nat" assumes "finite A" |
|
918 shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)" |
|
919 (is "?L \<longleftrightarrow> ?R") |
|
920 proof- |
|
921 have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast |
|
922 also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp |
|
923 also have "... \<longleftrightarrow> ?R" by simp |
|
924 finally show ?thesis . |
|
925 qed |
|
926 |
|
927 (* *) |
|
928 definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> 'b \<Rightarrow> nat" where |
|
929 "mmap h f b = setsum f {a. h a = b \<and> f a > 0}" |
|
930 |
|
931 lemma mmap_id: "mmap id = id" |
|
932 proof (rule ext)+ |
|
933 fix f a show "mmap id f a = id f a" |
|
934 proof(cases "f a = 0") |
|
935 case False |
|
936 hence 1: "{aa. aa = a \<and> 0 < f aa} = {a}" by auto |
|
937 show ?thesis by (simp add: mmap_def id_apply 1) |
|
938 qed(unfold mmap_def, auto) |
|
939 qed |
|
940 |
|
941 lemma inj_on_setsum_inv: |
|
942 assumes f: "f \<in> multiset" |
|
943 and 1: "(0::nat) < setsum f {a. h a = b' \<and> 0 < f a}" (is "0 < setsum f ?A'") |
|
944 and 2: "{a. h a = b \<and> 0 < f a} = {a. h a = b' \<and> 0 < f a}" (is "?A = ?A'") |
|
945 shows "b = b'" |
|
946 proof- |
|
947 have "finite ?A'" using f unfolding multiset_def by auto |
|
948 hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto |
|
949 thus ?thesis using 2 by auto |
|
950 qed |
|
951 |
|
952 lemma mmap_comp: |
|
953 fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c" |
|
954 assumes f: "f \<in> multiset" |
|
955 shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f" |
|
956 unfolding mmap_def[abs_def] comp_def proof(rule ext)+ |
|
957 fix c :: 'c |
|
958 let ?A = "{a. h2 (h1 a) = c \<and> 0 < f a}" |
|
959 let ?As = "\<lambda> b. {a. h1 a = b \<and> 0 < f a}" |
|
960 let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}" |
|
961 have 0: "{?As b | b. b \<in> ?B} = ?As ` ?B" by auto |
|
962 have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp |
|
963 hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto |
|
964 hence A: "?A = \<Union> {?As b | b. b \<in> ?B}" by auto |
|
965 have "setsum f ?A = setsum (setsum f) {?As b | b. b \<in> ?B}" |
|
966 unfolding A apply(rule setsum_Union_disjoint) |
|
967 using f unfolding multiset_def by auto |
|
968 also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 .. |
|
969 also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex) |
|
970 unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast |
|
971 also have "... = setsum (\<lambda> b. setsum f (?As b)) ?B" unfolding comp_def .. |
|
972 finally show "setsum f ?A = setsum (\<lambda> b. setsum f (?As b)) ?B" . |
|
973 qed |
|
974 |
|
975 lemma mmap_comp1: |
|
976 fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c" |
|
977 assumes "f \<in> multiset" |
|
978 shows "mmap (\<lambda> a. h2 (h1 a)) f = mmap h2 (mmap h1 f)" |
|
979 using mmap_comp[OF assms] unfolding comp_def by auto |
|
980 |
|
981 lemma mmap: |
|
982 assumes "f \<in> multiset" |
|
983 shows "mmap h f \<in> multiset" |
|
984 using assms unfolding mmap_def[abs_def] multiset_def proof safe |
|
985 assume fin: "finite {a. 0 < f a}" (is "finite ?A") |
|
986 show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}" |
|
987 (is "finite {b. 0 < setsum f (?As b)}") |
|
988 proof- let ?B = "{b. 0 < setsum f (?As b)}" |
|
989 have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp |
|
990 hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto |
|
991 hence "?B \<subseteq> h ` ?A" by auto |
|
992 thus ?thesis using finite_surj[OF fin] by auto |
|
993 qed |
|
994 qed |
|
995 |
|
996 lemma mmap_cong: |
|
997 assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a" |
|
998 shows "mmap f (count M) = mmap g (count M)" |
|
999 using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto |
|
1000 |
|
1001 abbreviation supp where "supp f \<equiv> {a. f a > 0}" |
|
1002 |
|
1003 lemma mmap_image_comp: |
|
1004 assumes f: "f \<in> multiset" |
|
1005 shows "(supp o mmap h) f = (image h o supp) f" |
|
1006 unfolding mmap_def[abs_def] comp_def proof- |
|
1007 have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)") |
|
1008 using f unfolding multiset_def by auto |
|
1009 thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}" |
|
1010 using setsum_gt_0_iff by auto |
|
1011 qed |
|
1012 |
|
1013 lemma mmap_image: |
|
1014 assumes f: "f \<in> multiset" |
|
1015 shows "supp (mmap h f) = h ` (supp f)" |
|
1016 using mmap_image_comp[OF assms] unfolding comp_def . |
|
1017 |
|
1018 lemma set_of_Abs_multiset: |
|
1019 assumes f: "f \<in> multiset" |
|
1020 shows "set_of (Abs_multiset f) = supp f" |
|
1021 using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse) |
|
1022 |
|
1023 lemma supp_count: |
|
1024 "supp (count M) = set_of M" |
|
1025 using assms unfolding set_of_def by auto |
|
1026 |
|
1027 lemma multiset_of_surj: |
|
1028 "multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}" |
|
1029 proof safe |
|
1030 fix M assume M: "set_of M \<subseteq> A" |
|
1031 obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto |
|
1032 hence "set as \<subseteq> A" using M by auto |
|
1033 thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto |
|
1034 next |
|
1035 show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A" |
|
1036 by (erule set_mp) (unfold set_of_multiset_of) |
|
1037 qed |
|
1038 |
|
1039 lemma card_of_set_of: |
|
1040 "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" |
|
1041 apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto |
|
1042 |
|
1043 lemma nat_sum_induct: |
|
1044 assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2" |
|
1045 shows "phi (n1::nat) (n2::nat)" |
|
1046 proof- |
|
1047 let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)" |
|
1048 have "?chi (n1,n2)" |
|
1049 apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi]) |
|
1050 using assms by (metis fstI sndI) |
|
1051 thus ?thesis by simp |
|
1052 qed |
|
1053 |
|
1054 lemma matrix_count: |
|
1055 fixes ct1 ct2 :: "nat \<Rightarrow> nat" |
|
1056 assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}" |
|
1057 shows |
|
1058 "\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and> |
|
1059 (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)" |
|
1060 (is "?phi ct1 ct2 n1 n2") |
|
1061 proof- |
|
1062 have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat. |
|
1063 setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2" |
|
1064 proof(induct rule: nat_sum_induct[of |
|
1065 "\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat. |
|
1066 setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"], |
|
1067 clarify) |
|
1068 fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat" |
|
1069 assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> |
|
1070 \<forall> dt1 dt2 :: nat \<Rightarrow> nat. |
|
1071 setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2" |
|
1072 and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}" |
|
1073 show "?phi ct1 ct2 n1 n2" |
|
1074 proof(cases n1) |
|
1075 case 0 note n1 = 0 |
|
1076 show ?thesis |
|
1077 proof(cases n2) |
|
1078 case 0 note n2 = 0 |
|
1079 let ?ct = "\<lambda> i1 i2. ct2 0" |
|
1080 show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp |
|
1081 next |
|
1082 case (Suc m2) note n2 = Suc |
|
1083 let ?ct = "\<lambda> i1 i2. ct2 i2" |
|
1084 show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto |
|
1085 qed |
|
1086 next |
|
1087 case (Suc m1) note n1 = Suc |
|
1088 show ?thesis |
|
1089 proof(cases n2) |
|
1090 case 0 note n2 = 0 |
|
1091 let ?ct = "\<lambda> i1 i2. ct1 i1" |
|
1092 show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto |
|
1093 next |
|
1094 case (Suc m2) note n2 = Suc |
|
1095 show ?thesis |
|
1096 proof(cases "ct1 n1 \<le> ct2 n2") |
|
1097 case True |
|
1098 def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2" |
|
1099 have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}" |
|
1100 unfolding dt2_def using ss n1 True by auto |
|
1101 hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp |
|
1102 then obtain dt where |
|
1103 1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and |
|
1104 2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto |
|
1105 let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0) |
|
1106 else dt i1 i2" |
|
1107 show ?thesis apply(rule exI[of _ ?ct]) |
|
1108 using n1 n2 1 2 True unfolding dt2_def by simp |
|
1109 next |
|
1110 case False |
|
1111 hence False: "ct2 n2 < ct1 n1" by simp |
|
1112 def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1" |
|
1113 have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}" |
|
1114 unfolding dt1_def using ss n2 False by auto |
|
1115 hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp |
|
1116 then obtain dt where |
|
1117 1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and |
|
1118 2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force |
|
1119 let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0) |
|
1120 else dt i1 i2" |
|
1121 show ?thesis apply(rule exI[of _ ?ct]) |
|
1122 using n1 n2 1 2 False unfolding dt1_def by simp |
|
1123 qed |
|
1124 qed |
|
1125 qed |
|
1126 qed |
|
1127 thus ?thesis using assms by auto |
|
1128 qed |
|
1129 |
|
1130 definition |
|
1131 "inj2 u B1 B2 \<equiv> |
|
1132 \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2' |
|
1133 \<longrightarrow> b1 = b1' \<and> b2 = b2'" |
|
1134 |
|
1135 lemma matrix_count_finite: |
|
1136 assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2" |
|
1137 and ss: "setsum N1 B1 = setsum N2 B2" |
|
1138 shows "\<exists> M :: 'a \<Rightarrow> nat. |
|
1139 (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and> |
|
1140 (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)" |
|
1141 proof- |
|
1142 obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps) |
|
1143 then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1" |
|
1144 using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into) |
|
1145 hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1" |
|
1146 unfolding bij_betw_def by auto |
|
1147 def f1 \<equiv> "inv_into {..<Suc n1} e1" |
|
1148 have f1: "bij_betw f1 B1 {..<Suc n1}" |
|
1149 and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1" |
|
1150 and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def |
|
1151 apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff) |
|
1152 by (metis e1_surj f_inv_into_f) |
|
1153 (* *) |
|
1154 obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps) |
|
1155 then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2" |
|
1156 using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into) |
|
1157 hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2" |
|
1158 unfolding bij_betw_def by auto |
|
1159 def f2 \<equiv> "inv_into {..<Suc n2} e2" |
|
1160 have f2: "bij_betw f2 B2 {..<Suc n2}" |
|
1161 and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2" |
|
1162 and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def |
|
1163 apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff) |
|
1164 by (metis e2_surj f_inv_into_f) |
|
1165 (* *) |
|
1166 let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2" |
|
1167 have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}" |
|
1168 unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric] |
|
1169 e1_surj e2_surj using ss . |
|
1170 obtain ct where |
|
1171 ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and |
|
1172 ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2" |
|
1173 using matrix_count[OF ss] by blast |
|
1174 (* *) |
|
1175 def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}" |
|
1176 have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a" |
|
1177 unfolding A_def Ball_def mem_Collect_eq by auto |
|
1178 then obtain h1h2 where h12: |
|
1179 "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis |
|
1180 def h1 \<equiv> "fst o h1h2" def h2 \<equiv> "snd o h1h2" |
|
1181 have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a" |
|
1182 "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1" "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2" |
|
1183 using h12 unfolding h1_def h2_def by force+ |
|
1184 {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" |
|
1185 hence inA: "u b1 b2 \<in> A" unfolding A_def by auto |
|
1186 hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto |
|
1187 moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto |
|
1188 ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2" |
|
1189 using u b1 b2 unfolding inj2_def by fastforce |
|
1190 } |
|
1191 hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and |
|
1192 h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto |
|
1193 def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))" |
|
1194 show ?thesis |
|
1195 apply(rule exI[of _ M]) proof safe |
|
1196 fix b1 assume b1: "b1 \<in> B1" |
|
1197 hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def |
|
1198 by (metis bij_betwE f1 lessThan_iff less_Suc_eq_le) |
|
1199 have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))" |
|
1200 unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj] |
|
1201 unfolding M_def comp_def apply(intro setsum_cong) apply force |
|
1202 by (metis e2_surj b1 h1 h2 imageI) |
|
1203 also have "... = N1 b1" using b1 ct1[OF f1b1] by simp |
|
1204 finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" . |
|
1205 next |
|
1206 fix b2 assume b2: "b2 \<in> B2" |
|
1207 hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def |
|
1208 by (metis bij_betwE f2 lessThan_iff less_Suc_eq_le) |
|
1209 have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))" |
|
1210 unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj] |
|
1211 unfolding M_def comp_def apply(intro setsum_cong) apply force |
|
1212 by (metis e1_surj b2 h1 h2 imageI) |
|
1213 also have "... = N2 b2" using b2 ct2[OF f2b2] by simp |
|
1214 finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" . |
|
1215 qed |
|
1216 qed |
|
1217 |
|
1218 lemma supp_vimage_mmap: |
|
1219 assumes "M \<in> multiset" |
|
1220 shows "supp M \<subseteq> f -` (supp (mmap f M))" |
|
1221 using assms by (auto simp: mmap_image) |
|
1222 |
|
1223 lemma mmap_ge_0: |
|
1224 assumes "M \<in> multiset" |
|
1225 shows "0 < mmap f M b \<longleftrightarrow> (\<exists>a. 0 < M a \<and> f a = b)" |
|
1226 proof- |
|
1227 have f: "finite {a. f a = b \<and> 0 < M a}" using assms unfolding multiset_def by auto |
|
1228 show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto |
|
1229 qed |
|
1230 |
|
1231 lemma finite_twosets: |
|
1232 assumes "finite B1" and "finite B2" |
|
1233 shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}" (is "finite ?A") |
|
1234 proof- |
|
1235 have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force |
|
1236 show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto |
|
1237 qed |
|
1238 |
|
1239 lemma wp_mmap: |
|
1240 fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set" |
|
1241 assumes wp: "wpull A B1 B2 f1 f2 p1 p2" |
|
1242 shows |
|
1243 "wpull {M. M \<in> multiset \<and> supp M \<subseteq> A} |
|
1244 {N1. N1 \<in> multiset \<and> supp N1 \<subseteq> B1} {N2. N2 \<in> multiset \<and> supp N2 \<subseteq> B2} |
|
1245 (mmap f1) (mmap f2) (mmap p1) (mmap p2)" |
|
1246 unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq) |
|
1247 fix N1 :: "'b1 \<Rightarrow> nat" and N2 :: "'b2 \<Rightarrow> nat" |
|
1248 assume mmap': "mmap f1 N1 = mmap f2 N2" |
|
1249 and N1[simp]: "N1 \<in> multiset" "supp N1 \<subseteq> B1" |
|
1250 and N2[simp]: "N2 \<in> multiset" "supp N2 \<subseteq> B2" |
|
1251 have mN1[simp]: "mmap f1 N1 \<in> multiset" using N1 by (auto simp: mmap) |
|
1252 have mN2[simp]: "mmap f2 N2 \<in> multiset" using N2 by (auto simp: mmap) |
|
1253 def P \<equiv> "mmap f1 N1" |
|
1254 have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto |
|
1255 note P = P1 P2 |
|
1256 have P_mult[simp]: "P \<in> multiset" unfolding P_def using N1 by auto |
|
1257 have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto |
|
1258 have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto |
|
1259 have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto |
|
1260 (* *) |
|
1261 def set1 \<equiv> "\<lambda> c. {b1 \<in> supp N1. f1 b1 = c}" |
|
1262 have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto |
|
1263 have fin_set1: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set1 c)" |
|
1264 using N1(1) unfolding set1_def multiset_def by auto |
|
1265 have set1_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<noteq> {}" |
|
1266 unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto |
|
1267 have supp_N1_set1: "supp N1 = (\<Union> c \<in> supp P. set1 c)" |
|
1268 using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto |
|
1269 hence set1_inclN1: "\<And>c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> supp N1" by auto |
|
1270 hence set1_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> B1" using N1(2) by blast |
|
1271 have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}" |
|
1272 unfolding set1_def by auto |
|
1273 have setsum_set1: "\<And> c. setsum N1 (set1 c) = P c" |
|
1274 unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto |
|
1275 (* *) |
|
1276 def set2 \<equiv> "\<lambda> c. {b2 \<in> supp N2. f2 b2 = c}" |
|
1277 have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto |
|
1278 have fin_set2: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set2 c)" |
|
1279 using N2(1) unfolding set2_def multiset_def by auto |
|
1280 have set2_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<noteq> {}" |
|
1281 unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto |
|
1282 have supp_N2_set2: "supp N2 = (\<Union> c \<in> supp P. set2 c)" |
|
1283 using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto |
|
1284 hence set2_inclN2: "\<And>c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> supp N2" by auto |
|
1285 hence set2_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> B2" using N2(2) by blast |
|
1286 have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}" |
|
1287 unfolding set2_def by auto |
|
1288 have setsum_set2: "\<And> c. setsum N2 (set2 c) = P c" |
|
1289 unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto |
|
1290 (* *) |
|
1291 have ss: "\<And> c. c \<in> supp P \<Longrightarrow> setsum N1 (set1 c) = setsum N2 (set2 c)" |
|
1292 unfolding setsum_set1 setsum_set2 .. |
|
1293 have "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c). |
|
1294 \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2" |
|
1295 using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq |
|
1296 by simp (metis set1 set2 set_rev_mp) |
|
1297 then obtain uu where uu: |
|
1298 "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c). |
|
1299 uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis |
|
1300 def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)" |
|
1301 have u[simp]: |
|
1302 "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A" |
|
1303 "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1" |
|
1304 "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2" |
|
1305 using uu unfolding u_def by auto |
|
1306 {fix c assume c: "c \<in> supp P" |
|
1307 have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify |
|
1308 fix b1 b1' b2 b2' |
|
1309 assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'" |
|
1310 hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and> |
|
1311 p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'" |
|
1312 using u(2)[OF c] u(3)[OF c] by simp metis |
|
1313 thus "b1 = b1' \<and> b2 = b2'" using 0 by auto |
|
1314 qed |
|
1315 } note inj = this |
|
1316 def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}" |
|
1317 have fin_sset[simp]: "\<And> c. c \<in> supp P \<Longrightarrow> finite (sset c)" unfolding sset_def |
|
1318 using fin_set1 fin_set2 finite_twosets by blast |
|
1319 have sset_A: "\<And> c. c \<in> supp P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto |
|
1320 {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c" |
|
1321 then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c" |
|
1322 and a: "a = u c b1 b2" unfolding sset_def by auto |
|
1323 have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c" |
|
1324 using ac a b1 b2 c u(2) u(3) by simp+ |
|
1325 hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c] |
|
1326 unfolding inj2_def by (metis c u(2) u(3)) |
|
1327 } note u_p12[simp] = this |
|
1328 {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c" |
|
1329 hence "p1 a \<in> set1 c" unfolding sset_def by auto |
|
1330 }note p1[simp] = this |
|
1331 {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c" |
|
1332 hence "p2 a \<in> set2 c" unfolding sset_def by auto |
|
1333 }note p2[simp] = this |
|
1334 (* *) |
|
1335 {fix c assume c: "c \<in> supp P" |
|
1336 hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and> |
|
1337 (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)" |
|
1338 unfolding sset_def |
|
1339 using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c] |
|
1340 set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto |
|
1341 } |
|
1342 then obtain Ms where |
|
1343 ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow> |
|
1344 setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = N1 b1" and |
|
1345 ss2: "\<And> c b2. \<lbrakk>c \<in> supp P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> |
|
1346 setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = N2 b2" |
|
1347 by metis |
|
1348 def SET \<equiv> "\<Union> c \<in> supp P. sset c" |
|
1349 have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto |
|
1350 have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by auto |
|
1351 have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET" |
|
1352 unfolding SET_def sset_def by blast |
|
1353 {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c" |
|
1354 then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'" |
|
1355 unfolding SET_def by auto |
|
1356 hence "p1 a \<in> set1 c'" unfolding sset_def by auto |
|
1357 hence eq: "c = c'" using p1a c c' set1_disj by auto |
|
1358 hence "a \<in> sset c" using ac' by simp |
|
1359 } note p1_rev = this |
|
1360 {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c" |
|
1361 then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'" |
|
1362 unfolding SET_def by auto |
|
1363 hence "p2 a \<in> set2 c'" unfolding sset_def by auto |
|
1364 hence eq: "c = c'" using p2a c c' set2_disj by auto |
|
1365 hence "a \<in> sset c" using ac' by simp |
|
1366 } note p2_rev = this |
|
1367 (* *) |
|
1368 have "\<forall> a \<in> SET. \<exists> c \<in> supp P. a \<in> sset c" unfolding SET_def by auto |
|
1369 then obtain h where h: "\<forall> a \<in> SET. h a \<in> supp P \<and> a \<in> sset (h a)" by metis |
|
1370 have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> |
|
1371 \<Longrightarrow> h (u c b1 b2) = c" |
|
1372 by (metis h p2 set2 u(3) u_SET) |
|
1373 have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> |
|
1374 \<Longrightarrow> h (u c b1 b2) = f1 b1" |
|
1375 using h unfolding sset_def by auto |
|
1376 have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> |
|
1377 \<Longrightarrow> h (u c b1 b2) = f2 b2" |
|
1378 using h unfolding sset_def by auto |
|
1379 def M \<equiv> "\<lambda> a. if a \<in> SET \<and> p1 a \<in> supp N1 \<and> p2 a \<in> supp N2 then Ms (h a) a else 0" |
|
1380 have sM: "supp M \<subseteq> SET" "supp M \<subseteq> p1 -` (supp N1)" "supp M \<subseteq> p2 -` (supp N2)" |
|
1381 unfolding M_def by auto |
|
1382 show "\<exists>M. (M \<in> multiset \<and> supp M \<subseteq> A) \<and> mmap p1 M = N1 \<and> mmap p2 M = N2" |
|
1383 proof(rule exI[of _ M], safe) |
|
1384 show "M \<in> multiset" |
|
1385 unfolding multiset_def using finite_subset[OF sM(1) fin_SET] by simp |
|
1386 next |
|
1387 fix a assume "0 < M a" |
|
1388 thus "a \<in> A" unfolding M_def using SET_A by (cases "a \<in> SET") auto |
|
1389 next |
|
1390 show "mmap p1 M = N1" |
|
1391 unfolding mmap_def[abs_def] proof(rule ext) |
|
1392 fix b1 |
|
1393 let ?K = "{a. p1 a = b1 \<and> 0 < M a}" |
|
1394 show "setsum M ?K = N1 b1" |
|
1395 proof(cases "b1 \<in> supp N1") |
|
1396 case False |
|
1397 hence "?K = {}" using sM(2) by auto |
|
1398 thus ?thesis using False by auto |
|
1399 next |
|
1400 case True |
|
1401 def c \<equiv> "f1 b1" |
|
1402 have c: "c \<in> supp P" and b1: "b1 \<in> set1 c" |
|
1403 unfolding set1_def c_def P1 using True by (auto simp: mmap_image) |
|
1404 have "setsum M ?K = setsum M {a. p1 a = b1 \<and> a \<in> SET}" |
|
1405 apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto |
|
1406 also have "... = setsum M ((\<lambda> b2. u c b1 b2) ` (set2 c))" |
|
1407 apply(rule setsum_cong) using c b1 proof safe |
|
1408 fix a assume p1a: "p1 a \<in> set1 c" and "0 < P c" and "a \<in> SET" |
|
1409 hence ac: "a \<in> sset c" using p1_rev by auto |
|
1410 hence "a = u c (p1 a) (p2 a)" using c by auto |
|
1411 moreover have "p2 a \<in> set2 c" using ac c by auto |
|
1412 ultimately show "a \<in> u c (p1 a) ` set2 c" by auto |
|
1413 next |
|
1414 fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c" |
|
1415 hence "u c b1 b2 \<in> SET" using c by auto |
|
1416 qed auto |
|
1417 also have "... = setsum (\<lambda> b2. M (u c b1 b2)) (set2 c)" |
|
1418 unfolding comp_def[symmetric] apply(rule setsum_reindex) |
|
1419 using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast |
|
1420 also have "... = N1 b1" unfolding ss1[OF c b1, symmetric] |
|
1421 apply(rule setsum_cong[OF refl]) unfolding M_def |
|
1422 using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce |
|
1423 finally show ?thesis . |
|
1424 qed |
|
1425 qed |
|
1426 next |
|
1427 show "mmap p2 M = N2" |
|
1428 unfolding mmap_def[abs_def] proof(rule ext) |
|
1429 fix b2 |
|
1430 let ?K = "{a. p2 a = b2 \<and> 0 < M a}" |
|
1431 show "setsum M ?K = N2 b2" |
|
1432 proof(cases "b2 \<in> supp N2") |
|
1433 case False |
|
1434 hence "?K = {}" using sM(3) by auto |
|
1435 thus ?thesis using False by auto |
|
1436 next |
|
1437 case True |
|
1438 def c \<equiv> "f2 b2" |
|
1439 have c: "c \<in> supp P" and b2: "b2 \<in> set2 c" |
|
1440 unfolding set2_def c_def P2 using True by (auto simp: mmap_image) |
|
1441 have "setsum M ?K = setsum M {a. p2 a = b2 \<and> a \<in> SET}" |
|
1442 apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto |
|
1443 also have "... = setsum M ((\<lambda> b1. u c b1 b2) ` (set1 c))" |
|
1444 apply(rule setsum_cong) using c b2 proof safe |
|
1445 fix a assume p2a: "p2 a \<in> set2 c" and "0 < P c" and "a \<in> SET" |
|
1446 hence ac: "a \<in> sset c" using p2_rev by auto |
|
1447 hence "a = u c (p1 a) (p2 a)" using c by auto |
|
1448 moreover have "p1 a \<in> set1 c" using ac c by auto |
|
1449 ultimately show "a \<in> (\<lambda>b1. u c b1 (p2 a)) ` set1 c" by auto |
|
1450 next |
|
1451 fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c" |
|
1452 hence "u c b1 b2 \<in> SET" using c by auto |
|
1453 qed auto |
|
1454 also have "... = setsum (M o (\<lambda> b1. u c b1 b2)) (set1 c)" |
|
1455 apply(rule setsum_reindex) |
|
1456 using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast |
|
1457 also have "... = setsum (\<lambda> b1. M (u c b1 b2)) (set1 c)" |
|
1458 unfolding comp_def[symmetric] by simp |
|
1459 also have "... = N2 b2" unfolding ss2[OF c b2, symmetric] |
|
1460 apply(rule setsum_cong[OF refl]) unfolding M_def set2_def |
|
1461 using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] |
|
1462 unfolding set1_def by fastforce |
|
1463 finally show ?thesis . |
|
1464 qed |
|
1465 qed |
|
1466 qed |
|
1467 qed |
|
1468 |
|
1469 definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where |
|
1470 "mset_map h = Abs_multiset \<circ> mmap h \<circ> count" |
|
1471 |
|
1472 bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"] |
|
1473 unfolding mset_map_def |
|
1474 proof - |
|
1475 show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse) |
|
1476 next |
|
1477 fix f g |
|
1478 show "Abs_multiset \<circ> mmap (g \<circ> f) \<circ> count = |
|
1479 Abs_multiset \<circ> mmap g \<circ> count \<circ> (Abs_multiset \<circ> mmap f \<circ> count)" |
|
1480 unfolding comp_def apply(rule ext) |
|
1481 by (auto simp: Abs_multiset_inverse count mmap_comp1 mmap) |
|
1482 next |
|
1483 fix M f g assume eq: "\<And>a. a \<in> set_of M \<Longrightarrow> f a = g a" |
|
1484 thus "(Abs_multiset \<circ> mmap f \<circ> count) M = (Abs_multiset \<circ> mmap g \<circ> count) M" apply auto |
|
1485 unfolding cIm_def[abs_def] image_def |
|
1486 by (auto intro!: mmap_cong simp: Abs_multiset_inject count mmap) |
|
1487 next |
|
1488 fix f show "set_of \<circ> (Abs_multiset \<circ> mmap f \<circ> count) = op ` f \<circ> set_of" |
|
1489 by (auto simp: count mmap mmap_image set_of_Abs_multiset supp_count) |
|
1490 next |
|
1491 show "card_order natLeq" by (rule natLeq_card_order) |
|
1492 next |
|
1493 show "cinfinite natLeq" by (rule natLeq_cinfinite) |
|
1494 next |
|
1495 fix M show "|set_of M| \<le>o natLeq" |
|
1496 apply(rule ordLess_imp_ordLeq) |
|
1497 unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of . |
|
1498 next |
|
1499 fix A :: "'a set" |
|
1500 have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of . |
|
1501 also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" |
|
1502 by (rule list_in_bd) |
|
1503 finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" . |
|
1504 next |
|
1505 fix A B1 B2 f1 f2 p1 p2 |
|
1506 let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count" |
|
1507 assume wp: "wpull A B1 B2 f1 f2 p1 p2" |
|
1508 show "wpull {x. set_of x \<subseteq> A} {x. set_of x \<subseteq> B1} {x. set_of x \<subseteq> B2} |
|
1509 (?map f1) (?map f2) (?map p1) (?map p2)" |
|
1510 unfolding wpull_def proof safe |
|
1511 fix y1 y2 |
|
1512 assume y1: "set_of y1 \<subseteq> B1" and y2: "set_of y2 \<subseteq> B2" |
|
1513 and m: "?map f1 y1 = ?map f2 y2" |
|
1514 def N1 \<equiv> "count y1" def N2 \<equiv> "count y2" |
|
1515 have "N1 \<in> multiset \<and> supp N1 \<subseteq> B1" and "N2 \<in> multiset \<and> supp N2 \<subseteq> B2" |
|
1516 and "mmap f1 N1 = mmap f2 N2" |
|
1517 using y1 y2 m unfolding N1_def N2_def |
|
1518 by (auto simp: Abs_multiset_inject count mmap) |
|
1519 then obtain M where M: "M \<in> multiset \<and> supp M \<subseteq> A" |
|
1520 and N1: "mmap p1 M = N1" and N2: "mmap p2 M = N2" |
|
1521 using wp_mmap[OF wp] unfolding wpull_def by auto |
|
1522 def x \<equiv> "Abs_multiset M" |
|
1523 show "\<exists>x\<in>{x. set_of x \<subseteq> A}. ?map p1 x = y1 \<and> ?map p2 x = y2" |
|
1524 apply(intro bexI[of _ x]) using M N1 N2 unfolding N1_def N2_def x_def |
|
1525 by (auto simp: count_inverse Abs_multiset_inverse) |
|
1526 qed |
|
1527 qed (unfold set_of_empty, auto) |
|
1528 |
|
1529 end |