208 apply (induct y, simp) |
209 apply (induct y, simp) |
209 apply (simp add: spair_below_iff flat_below_iff) |
210 apply (simp add: spair_below_iff flat_below_iff) |
210 done |
211 done |
211 qed |
212 qed |
212 |
213 |
213 subsection {* Map function for strict products *} |
|
214 |
|
215 definition |
|
216 sprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<otimes> 'c \<rightarrow> 'b \<otimes> 'd" |
|
217 where |
|
218 "sprod_map = (\<Lambda> f g. ssplit\<cdot>(\<Lambda> x y. (:f\<cdot>x, g\<cdot>y:)))" |
|
219 |
|
220 lemma sprod_map_strict [simp]: "sprod_map\<cdot>a\<cdot>b\<cdot>\<bottom> = \<bottom>" |
|
221 unfolding sprod_map_def by simp |
|
222 |
|
223 lemma sprod_map_spair [simp]: |
|
224 "x \<noteq> \<bottom> \<Longrightarrow> y \<noteq> \<bottom> \<Longrightarrow> sprod_map\<cdot>f\<cdot>g\<cdot>(:x, y:) = (:f\<cdot>x, g\<cdot>y:)" |
|
225 by (simp add: sprod_map_def) |
|
226 |
|
227 lemma sprod_map_spair': |
|
228 "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:)" |
|
229 by (cases "x = \<bottom> \<or> y = \<bottom>") auto |
|
230 |
|
231 lemma sprod_map_ID: "sprod_map\<cdot>ID\<cdot>ID = ID" |
|
232 unfolding sprod_map_def by (simp add: cfun_eq_iff eta_cfun) |
|
233 |
|
234 lemma sprod_map_map: |
|
235 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
|
236 sprod_map\<cdot>f1\<cdot>g1\<cdot>(sprod_map\<cdot>f2\<cdot>g2\<cdot>p) = |
|
237 sprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
|
238 apply (induct p, simp) |
|
239 apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
|
240 apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
|
241 apply simp |
|
242 done |
|
243 |
|
244 lemma ep_pair_sprod_map: |
|
245 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
|
246 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
|
247 proof |
|
248 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
|
249 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
|
250 fix x show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" |
|
251 by (induct x) simp_all |
|
252 fix y show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" |
|
253 apply (induct y, simp) |
|
254 apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
|
255 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
|
256 done |
|
257 qed |
|
258 |
|
259 lemma deflation_sprod_map: |
|
260 assumes "deflation d1" and "deflation d2" |
|
261 shows "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
|
262 proof |
|
263 interpret d1: deflation d1 by fact |
|
264 interpret d2: deflation d2 by fact |
|
265 fix x |
|
266 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
|
267 apply (induct x, simp) |
|
268 apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp) |
|
269 apply (simp add: d1.idem d2.idem) |
|
270 done |
|
271 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
|
272 apply (induct x, simp) |
|
273 apply (simp add: monofun_cfun d1.below d2.below) |
|
274 done |
|
275 qed |
|
276 |
|
277 lemma finite_deflation_sprod_map: |
|
278 assumes "finite_deflation d1" and "finite_deflation d2" |
|
279 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
|
280 proof (rule finite_deflation_intro) |
|
281 interpret d1: finite_deflation d1 by fact |
|
282 interpret d2: finite_deflation d2 by fact |
|
283 have "deflation d1" and "deflation d2" by fact+ |
|
284 thus "deflation (sprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_sprod_map) |
|
285 have "{x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x} \<subseteq> insert \<bottom> |
|
286 ((\<lambda>(x, y). (:x, y:)) ` ({x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}))" |
|
287 by (rule subsetI, case_tac x, auto simp add: spair_eq_iff) |
|
288 thus "finite {x. sprod_map\<cdot>d1\<cdot>d2\<cdot>x = x}" |
|
289 by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes) |
|
290 qed |
|
291 |
|
292 end |
214 end |