|
1 (* Title: HOLCF/Map_Functions.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Map functions for various types *} |
|
6 |
|
7 theory Map_Functions |
|
8 imports Deflation |
|
9 begin |
|
10 |
|
11 subsection {* Map operator for continuous function space *} |
|
12 |
|
13 default_sort cpo |
|
14 |
|
15 definition |
|
16 cfun_map :: "('b \<rightarrow> 'a) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'c) \<rightarrow> ('b \<rightarrow> 'd)" |
|
17 where |
|
18 "cfun_map = (\<Lambda> a b f x. b\<cdot>(f\<cdot>(a\<cdot>x)))" |
|
19 |
|
20 lemma cfun_map_beta [simp]: "cfun_map\<cdot>a\<cdot>b\<cdot>f\<cdot>x = b\<cdot>(f\<cdot>(a\<cdot>x))" |
|
21 unfolding cfun_map_def by simp |
|
22 |
|
23 lemma cfun_map_ID: "cfun_map\<cdot>ID\<cdot>ID = ID" |
|
24 unfolding cfun_eq_iff by simp |
|
25 |
|
26 lemma cfun_map_map: |
|
27 "cfun_map\<cdot>f1\<cdot>g1\<cdot>(cfun_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
28 cfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
29 by (rule cfun_eqI) simp |
|
30 |
|
31 lemma ep_pair_cfun_map: |
|
32 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
|
33 shows "ep_pair (cfun_map\<cdot>p1\<cdot>e2) (cfun_map\<cdot>e1\<cdot>p2)" |
|
34 proof |
|
35 interpret e1p1: ep_pair e1 p1 by fact |
|
36 interpret e2p2: ep_pair e2 p2 by fact |
|
37 fix f show "cfun_map\<cdot>e1\<cdot>p2\<cdot>(cfun_map\<cdot>p1\<cdot>e2\<cdot>f) = f" |
|
38 by (simp add: cfun_eq_iff) |
|
39 fix g show "cfun_map\<cdot>p1\<cdot>e2\<cdot>(cfun_map\<cdot>e1\<cdot>p2\<cdot>g) \<sqsubseteq> g" |
|
40 apply (rule cfun_belowI, simp) |
|
41 apply (rule below_trans [OF e2p2.e_p_below]) |
|
42 apply (rule monofun_cfun_arg) |
|
43 apply (rule e1p1.e_p_below) |
|
44 done |
|
45 qed |
|
46 |
|
47 lemma deflation_cfun_map: |
|
48 assumes "deflation d1" and "deflation d2" |
|
49 shows "deflation (cfun_map\<cdot>d1\<cdot>d2)" |
|
50 proof |
|
51 interpret d1: deflation d1 by fact |
|
52 interpret d2: deflation d2 by fact |
|
53 fix f |
|
54 show "cfun_map\<cdot>d1\<cdot>d2\<cdot>(cfun_map\<cdot>d1\<cdot>d2\<cdot>f) = cfun_map\<cdot>d1\<cdot>d2\<cdot>f" |
|
55 by (simp add: cfun_eq_iff d1.idem d2.idem) |
|
56 show "cfun_map\<cdot>d1\<cdot>d2\<cdot>f \<sqsubseteq> f" |
|
57 apply (rule cfun_belowI, simp) |
|
58 apply (rule below_trans [OF d2.below]) |
|
59 apply (rule monofun_cfun_arg) |
|
60 apply (rule d1.below) |
|
61 done |
|
62 qed |
|
63 |
|
64 lemma finite_range_cfun_map: |
|
65 assumes a: "finite (range (\<lambda>x. a\<cdot>x))" |
|
66 assumes b: "finite (range (\<lambda>y. b\<cdot>y))" |
|
67 shows "finite (range (\<lambda>f. cfun_map\<cdot>a\<cdot>b\<cdot>f))" (is "finite (range ?h)") |
|
68 proof (rule finite_imageD) |
|
69 let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))" |
|
70 show "finite (?f ` range ?h)" |
|
71 proof (rule finite_subset) |
|
72 let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))" |
|
73 show "?f ` range ?h \<subseteq> ?B" |
|
74 by clarsimp |
|
75 show "finite ?B" |
|
76 by (simp add: a b) |
|
77 qed |
|
78 show "inj_on ?f (range ?h)" |
|
79 proof (rule inj_onI, rule cfun_eqI, clarsimp) |
|
80 fix x f g |
|
81 assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
|
82 hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
|
83 by (rule equalityD1) |
|
84 hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" |
|
85 by (simp add: subset_eq) |
|
86 then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))" |
|
87 by (rule rangeE) |
|
88 thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))" |
|
89 by clarsimp |
|
90 qed |
|
91 qed |
|
92 |
|
93 lemma finite_deflation_cfun_map: |
|
94 assumes "finite_deflation d1" and "finite_deflation d2" |
|
95 shows "finite_deflation (cfun_map\<cdot>d1\<cdot>d2)" |
|
96 proof (rule finite_deflation_intro) |
|
97 interpret d1: finite_deflation d1 by fact |
|
98 interpret d2: finite_deflation d2 by fact |
|
99 have "deflation d1" and "deflation d2" by fact+ |
|
100 thus "deflation (cfun_map\<cdot>d1\<cdot>d2)" by (rule deflation_cfun_map) |
|
101 have "finite (range (\<lambda>f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f))" |
|
102 using d1.finite_range d2.finite_range |
|
103 by (rule finite_range_cfun_map) |
|
104 thus "finite {f. cfun_map\<cdot>d1\<cdot>d2\<cdot>f = f}" |
|
105 by (rule finite_range_imp_finite_fixes) |
|
106 qed |
|
107 |
|
108 text {* Finite deflations are compact elements of the function space *} |
|
109 |
|
110 lemma finite_deflation_imp_compact: "finite_deflation d \<Longrightarrow> compact d" |
|
111 apply (frule finite_deflation_imp_deflation) |
|
112 apply (subgoal_tac "compact (cfun_map\<cdot>d\<cdot>d\<cdot>d)") |
|
113 apply (simp add: cfun_map_def deflation.idem eta_cfun) |
|
114 apply (rule finite_deflation.compact) |
|
115 apply (simp only: finite_deflation_cfun_map) |
|
116 done |
|
117 |
|
118 subsection {* Map operator for product type *} |
|
119 |
|
120 definition |
|
121 cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd" |
|
122 where |
|
123 "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))" |
|
124 |
|
125 lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)" |
|
126 unfolding cprod_map_def by simp |
|
127 |
|
128 lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID" |
|
129 unfolding cfun_eq_iff by auto |
|
130 |
|
131 lemma cprod_map_map: |
|
132 "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
133 cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
134 by (induct p) simp |
|
135 |
|
136 lemma ep_pair_cprod_map: |
|
137 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
|
138 shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)" |
|
139 proof |
|
140 interpret e1p1: ep_pair e1 p1 by fact |
|
141 interpret e2p2: ep_pair e2 p2 by fact |
|
142 fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
|
143 by (induct x) simp |
|
144 fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
|
145 by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below) |
|
146 qed |
|
147 |
|
148 lemma deflation_cprod_map: |
|
149 assumes "deflation d1" and "deflation d2" |
|
150 shows "deflation (cprod_map\<cdot>d1\<cdot>d2)" |
|
151 proof |
|
152 interpret d1: deflation d1 by fact |
|
153 interpret d2: deflation d2 by fact |
|
154 fix x |
|
155 show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
|
156 by (induct x) (simp add: d1.idem d2.idem) |
|
157 show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
|
158 by (induct x) (simp add: d1.below d2.below) |
|
159 qed |
|
160 |
|
161 lemma finite_deflation_cprod_map: |
|
162 assumes "finite_deflation d1" and "finite_deflation d2" |
|
163 shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)" |
|
164 proof (rule finite_deflation_intro) |
|
165 interpret d1: finite_deflation d1 by fact |
|
166 interpret d2: finite_deflation d2 by fact |
|
167 have "deflation d1" and "deflation d2" by fact+ |
|
168 thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map) |
|
169 have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}" |
|
170 by clarsimp |
|
171 thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}" |
|
172 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
|
173 qed |
|
174 |
|
175 subsection {* Map function for lifted cpo *} |
|
176 |
|
177 definition |
|
178 u_map :: "('a \<rightarrow> 'b) \<rightarrow> 'a u \<rightarrow> 'b u" |
|
179 where |
|
180 "u_map = (\<Lambda> f. fup\<cdot>(up oo f))" |
|
181 |
|
182 lemma u_map_strict [simp]: "u_map\<cdot>f\<cdot>\<bottom> = \<bottom>" |
|
183 unfolding u_map_def by simp |
|
184 |
|
185 lemma u_map_up [simp]: "u_map\<cdot>f\<cdot>(up\<cdot>x) = up\<cdot>(f\<cdot>x)" |
|
186 unfolding u_map_def by simp |
|
187 |
|
188 lemma u_map_ID: "u_map\<cdot>ID = ID" |
|
189 unfolding u_map_def by (simp add: cfun_eq_iff eta_cfun) |
|
190 |
|
191 lemma u_map_map: "u_map\<cdot>f\<cdot>(u_map\<cdot>g\<cdot>p) = u_map\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>p" |
|
192 by (induct p) simp_all |
|
193 |
|
194 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
|
195 apply default |
|
196 apply (case_tac x, simp, simp add: ep_pair.e_inverse) |
|
197 apply (case_tac y, simp, simp add: ep_pair.e_p_below) |
|
198 done |
|
199 |
|
200 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
|
201 apply default |
|
202 apply (case_tac x, simp, simp add: deflation.idem) |
|
203 apply (case_tac x, simp, simp add: deflation.below) |
|
204 done |
|
205 |
|
206 lemma finite_deflation_u_map: |
|
207 assumes "finite_deflation d" shows "finite_deflation (u_map\<cdot>d)" |
|
208 proof (rule finite_deflation_intro) |
|
209 interpret d: finite_deflation d by fact |
|
210 have "deflation d" by fact |
|
211 thus "deflation (u_map\<cdot>d)" by (rule deflation_u_map) |
|
212 have "{x. u_map\<cdot>d\<cdot>x = x} \<subseteq> insert \<bottom> ((\<lambda>x. up\<cdot>x) ` {x. d\<cdot>x = x})" |
|
213 by (rule subsetI, case_tac x, simp_all) |
|
214 thus "finite {x. u_map\<cdot>d\<cdot>x = x}" |
|
215 by (rule finite_subset, simp add: d.finite_fixes) |
|
216 qed |
|
217 |
|
218 subsection {* Map function for strict products *} |
|
219 |
|
220 default_sort pcpo |
|
221 |
|
222 definition |
|
223 sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
|
224 where |
|
225 "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
|
226 |
|
227 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
|
228 unfolding sprod_map_def by simp |
|
229 |
|
230 lemma sprod_map_spair [simp]: |
|
231 "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
|
232 by (simp add: sprod_map_def) |
|
233 |
|
234 lemma sprod_map_spair': |
|
235 "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
|
236 by (cases "x = \<bottom> \<or> y = \<bottom>") auto |
|
237 |
|
238 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID" |
|
239 unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun) |
|
240 |
|
241 lemma sprod_map_map: |
|
242 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
|
243 sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
244 sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
245 apply (induct p, simp) |
|
246 apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
|
247 apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
|
248 apply simp |
|
249 done |
|
250 |
|
251 lemma ep_pair_sprod_map: |
|
252 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
|
253 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
|
254 proof |
|
255 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
|
256 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
|
257 fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
|
258 by (induct x) simp_all |
|
259 fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
|
260 apply (induct y, simp) |
|
261 apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
|
262 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
|
263 done |
|
264 qed |
|
265 |
|
266 lemma deflation_sprod_map: |
|
267 assumes "deflation d1" and "deflation d2" |
|
268 shows "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
|
269 proof |
|
270 interpret d1: deflation d1 by fact |
|
271 interpret d2: deflation d2 by fact |
|
272 fix x |
|
273 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
|
274 apply (induct x, simp) |
|
275 apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp) |
|
276 apply (simp add: d1.idem d2.idem) |
|
277 done |
|
278 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
|
279 apply (induct x, simp) |
|
280 apply (simp add: monofun_cfun d1.below d2.below) |
|
281 done |
|
282 qed |
|
283 |
|
284 lemma finite_deflation_sprod_map: |
|
285 assumes "finite_deflation d1" and "finite_deflation d2" |
|
286 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
|
287 proof (rule finite_deflation_intro) |
|
288 interpret d1: finite_deflation d1 by fact |
|
289 interpret d2: finite_deflation d2 by fact |
|
290 have "deflation d1" and "deflation d2" by fact+ |
|
291 thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map) |
|
292 have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom> |
|
293 ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))" |
|
294 by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) |
|
295 thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
|
296 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
|
297 qed |
|
298 |
|
299 subsection {* Map function for strict sums *} |
|
300 |
|
301 definition |
|
302 ssum_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<oplus> 'c \<rightarrow> 'b \<oplus> 'd" |
|
303 where |
|
304 "ssum_map = (\<Lambda> f g. sscase\<cdot>(sinl oo f)\<cdot>(sinr oo g))" |
|
305 |
|
306 lemma ssum_map_strict [simp]: "ssum_map\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>" |
|
307 unfolding ssum_map_def by simp |
|
308 |
|
309 lemma ssum_map_sinl [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
|
310 unfolding ssum_map_def by simp |
|
311 |
|
312 lemma ssum_map_sinr [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
|
313 unfolding ssum_map_def by simp |
|
314 |
|
315 lemma ssum_map_sinl': "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinl\<cdot>x) = sinl\<cdot>(f\<cdot>x)" |
|
316 by (cases "x = \<bottom>") simp_all |
|
317 |
|
318 lemma ssum_map_sinr': "g\<cdot>\<bottom> = \<bottom> \<Longrightarrow> ssum_map\<cdot>f\<cdot>g\<cdot>(sinr\<cdot>x) = sinr\<cdot>(g\<cdot>x)" |
|
319 by (cases "x = \<bottom>") simp_all |
|
320 |
|
321 lemma ssum_map_ID: "ssum_map\<cdot>ID\<cdot>ID = ID" |
|
322 unfolding ssum_map_def by (simp add: cfun_eq_iff eta_cfun) |
|
323 |
|
324 lemma ssum_map_map: |
|
325 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
|
326 ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
327 ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
328 apply (induct p, simp) |
|
329 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp) |
|
330 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp) |
|
331 done |
|
332 |
|
333 lemma ep_pair_ssum_map: |
|
334 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
|
335 shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
|
336 proof |
|
337 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
|
338 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
|
339 fix x show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
|
340 by (induct x) simp_all |
|
341 fix y show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
|
342 apply (induct y, simp) |
|
343 apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below) |
|
344 apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below) |
|
345 done |
|
346 qed |
|
347 |
|
348 lemma deflation_ssum_map: |
|
349 assumes "deflation d1" and "deflation d2" |
|
350 shows "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
|
351 proof |
|
352 interpret d1: deflation d1 by fact |
|
353 interpret d2: deflation d2 by fact |
|
354 fix x |
|
355 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x" |
|
356 apply (induct x, simp) |
|
357 apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem) |
|
358 apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem) |
|
359 done |
|
360 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
|
361 apply (induct x, simp) |
|
362 apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below) |
|
363 apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below) |
|
364 done |
|
365 qed |
|
366 |
|
367 lemma finite_deflation_ssum_map: |
|
368 assumes "finite_deflation d1" and "finite_deflation d2" |
|
369 shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |
|
370 proof (rule finite_deflation_intro) |
|
371 interpret d1: finite_deflation d1 by fact |
|
372 interpret d2: finite_deflation d2 by fact |
|
373 have "deflation d1" and "deflation d2" by fact+ |
|
374 thus "deflation (ssum_map\<cdot>d1\<cdot>d2)" by (rule deflation_ssum_map) |
|
375 have "{x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> |
|
376 (\<lambda>x. sinl\<cdot>x) ` {x. d1\<cdot>x = x} \<union> |
|
377 (\<lambda>x. sinr\<cdot>x) ` {x. d2\<cdot>x = x} \<union> {\<bottom>}" |
|
378 by (rule subsetI, case_tac x, simp_all) |
|
379 thus "finite {x. ssum_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
|
380 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
|
381 qed |
|
382 |
|
383 end |