186 lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g" |
186 lemma u_map_oo: "u_map\<cdot>(f oo g) = u_map\<cdot>f oo u_map\<cdot>g" |
187 by (simp add: cfcomp1 u_map_map eta_cfun) |
187 by (simp add: cfcomp1 u_map_map eta_cfun) |
188 |
188 |
189 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
189 lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)" |
190 apply standard |
190 apply standard |
191 subgoal for x by (cases x, simp, simp add: ep_pair.e_inverse) |
191 subgoal for x by (cases x) (simp_all add: ep_pair.e_inverse) |
192 subgoal for y by (cases y, simp, simp add: ep_pair.e_p_below) |
192 subgoal for y by (cases y) (simp_all add: ep_pair.e_p_below) |
193 done |
193 done |
194 |
194 |
195 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
195 lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)" |
196 apply standard |
196 apply standard |
197 subgoal for x by (cases x, simp, simp add: deflation.idem) |
197 subgoal for x by (cases x) (simp_all add: deflation.idem) |
198 subgoal for x by (cases x, simp, simp add: deflation.below) |
198 subgoal for x by (cases x) (simp_all add: deflation.below) |
199 done |
199 done |
200 |
200 |
201 lemma finite_deflation_u_map: |
201 lemma finite_deflation_u_map: |
202 assumes "finite_deflation d" |
202 assumes "finite_deflation d" |
203 shows "finite_deflation (u_map\<cdot>d)" |
203 shows "finite_deflation (u_map\<cdot>d)" |
233 |
233 |
234 lemma sprod_map_map: |
234 lemma sprod_map_map: |
235 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
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) = |
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" |
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) |
238 proof (induct p) |
239 apply simp |
239 case bottom |
240 apply (case_tac "f2\<cdot>x = \<bottom>", simp) |
240 then show ?case by simp |
241 apply (case_tac "g2\<cdot>y = \<bottom>", simp) |
241 next |
242 apply simp |
242 case (spair x y) |
243 done |
243 then show ?case |
|
244 apply (cases "f2\<cdot>x = \<bottom>", simp) |
|
245 apply (cases "g2\<cdot>y = \<bottom>", simp) |
|
246 apply simp |
|
247 done |
|
248 qed |
244 |
249 |
245 lemma ep_pair_sprod_map: |
250 lemma ep_pair_sprod_map: |
246 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
251 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
247 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
252 shows "ep_pair (sprod_map\<cdot>e1\<cdot>e2) (sprod_map\<cdot>p1\<cdot>p2)" |
248 proof |
253 proof |
249 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
254 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
250 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
255 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
251 show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
256 show "sprod_map\<cdot>p1\<cdot>p2\<cdot>(sprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
252 by (induct x) simp_all |
257 by (induct x) simp_all |
253 show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
258 show "sprod_map\<cdot>e1\<cdot>e2\<cdot>(sprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
254 apply (induct y) |
259 proof (induct y) |
255 apply simp |
260 case bottom |
256 apply (case_tac "p1\<cdot>x = \<bottom>", simp, case_tac "p2\<cdot>y = \<bottom>", simp) |
261 then show ?case by simp |
257 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
262 next |
258 done |
263 case (spair x y) |
|
264 then show ?case |
|
265 apply simp |
|
266 apply (cases "p1\<cdot>x = \<bottom>", simp, cases "p2\<cdot>y = \<bottom>", simp) |
|
267 apply (simp add: monofun_cfun e1p1.e_p_below e2p2.e_p_below) |
|
268 done |
|
269 qed |
259 qed |
270 qed |
260 |
271 |
261 lemma deflation_sprod_map: |
272 lemma deflation_sprod_map: |
262 assumes "deflation d1" and "deflation d2" |
273 assumes "deflation d1" and "deflation d2" |
263 shows "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
274 shows "deflation (sprod_map\<cdot>d1\<cdot>d2)" |
264 proof |
275 proof |
265 interpret d1: deflation d1 by fact |
276 interpret d1: deflation d1 by fact |
266 interpret d2: deflation d2 by fact |
277 interpret d2: deflation d2 by fact |
267 fix x |
278 fix x |
268 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
279 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>(sprod_map\<cdot>d1\<cdot>d2\<cdot>x) = sprod_map\<cdot>d1\<cdot>d2\<cdot>x" |
269 apply (induct x, simp) |
280 proof (induct x) |
270 apply (case_tac "d1\<cdot>x = \<bottom>", simp, case_tac "d2\<cdot>y = \<bottom>", simp) |
281 case bottom |
271 apply (simp add: d1.idem d2.idem) |
282 then show ?case by simp |
272 done |
283 next |
|
284 case (spair x y) |
|
285 then show ?case |
|
286 apply (cases "d1\<cdot>x = \<bottom>", simp, cases "d2\<cdot>y = \<bottom>", simp) |
|
287 apply (simp add: d1.idem d2.idem) |
|
288 done |
|
289 qed |
273 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
290 show "sprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
274 apply (induct x, simp) |
291 proof (induct x) |
275 apply (simp add: monofun_cfun d1.below d2.below) |
292 case bottom |
276 done |
293 then show ?case by simp |
|
294 next |
|
295 case spair |
|
296 then show ?case by (simp add: monofun_cfun d1.below d2.below) |
|
297 qed |
277 qed |
298 qed |
278 |
299 |
279 lemma finite_deflation_sprod_map: |
300 lemma finite_deflation_sprod_map: |
280 assumes "finite_deflation d1" and "finite_deflation d2" |
301 assumes "finite_deflation d1" and "finite_deflation d2" |
281 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
302 shows "finite_deflation (sprod_map\<cdot>d1\<cdot>d2)" |
317 |
338 |
318 lemma ssum_map_map: |
339 lemma ssum_map_map: |
319 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
340 "\<lbrakk>f1\<cdot>\<bottom> = \<bottom>; g1\<cdot>\<bottom> = \<bottom>\<rbrakk> \<Longrightarrow> |
320 ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
341 ssum_map\<cdot>f1\<cdot>g1\<cdot>(ssum_map\<cdot>f2\<cdot>g2\<cdot>p) = |
321 ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
342 ssum_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p" |
322 apply (induct p) |
343 proof (induct p) |
323 apply simp |
344 case bottom |
324 apply (case_tac "f2\<cdot>x = \<bottom>", simp, simp) |
345 then show ?case by simp |
325 apply (case_tac "g2\<cdot>y = \<bottom>", simp, simp) |
346 next |
326 done |
347 case (sinl x) |
|
348 then show ?case by (cases "f2\<cdot>x = \<bottom>") simp_all |
|
349 next |
|
350 case (sinr y) |
|
351 then show ?case by (cases "g2\<cdot>y = \<bottom>") simp_all |
|
352 qed |
327 |
353 |
328 lemma ep_pair_ssum_map: |
354 lemma ep_pair_ssum_map: |
329 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
355 assumes "ep_pair e1 p1" and "ep_pair e2 p2" |
330 shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
356 shows "ep_pair (ssum_map\<cdot>e1\<cdot>e2) (ssum_map\<cdot>p1\<cdot>p2)" |
331 proof |
357 proof |
332 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
358 interpret e1p1: pcpo_ep_pair e1 p1 unfolding pcpo_ep_pair_def by fact |
333 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
359 interpret e2p2: pcpo_ep_pair e2 p2 unfolding pcpo_ep_pair_def by fact |
334 show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
360 show "ssum_map\<cdot>p1\<cdot>p2\<cdot>(ssum_map\<cdot>e1\<cdot>e2\<cdot>x) = x" for x |
335 by (induct x) simp_all |
361 by (induct x) simp_all |
336 show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
362 show "ssum_map\<cdot>e1\<cdot>e2\<cdot>(ssum_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y" for y |
337 apply (induct y) |
363 proof (induct y) |
338 apply simp |
364 case bottom |
339 apply (case_tac "p1\<cdot>x = \<bottom>", simp, simp add: e1p1.e_p_below) |
365 then show ?case by simp |
340 apply (case_tac "p2\<cdot>y = \<bottom>", simp, simp add: e2p2.e_p_below) |
366 next |
341 done |
367 case (sinl x) |
|
368 then show ?case by (cases "p1\<cdot>x = \<bottom>") (simp_all add: e1p1.e_p_below) |
|
369 next |
|
370 case (sinr y) |
|
371 then show ?case by (cases "p2\<cdot>y = \<bottom>") (simp_all add: e2p2.e_p_below) |
|
372 qed |
342 qed |
373 qed |
343 |
374 |
344 lemma deflation_ssum_map: |
375 lemma deflation_ssum_map: |
345 assumes "deflation d1" and "deflation d2" |
376 assumes "deflation d1" and "deflation d2" |
346 shows "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
377 shows "deflation (ssum_map\<cdot>d1\<cdot>d2)" |
347 proof |
378 proof |
348 interpret d1: deflation d1 by fact |
379 interpret d1: deflation d1 by fact |
349 interpret d2: deflation d2 by fact |
380 interpret d2: deflation d2 by fact |
350 fix x |
381 fix x |
351 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x" |
382 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>(ssum_map\<cdot>d1\<cdot>d2\<cdot>x) = ssum_map\<cdot>d1\<cdot>d2\<cdot>x" |
352 apply (induct x, simp) |
383 proof (induct x) |
353 apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.idem) |
384 case bottom |
354 apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.idem) |
385 then show ?case by simp |
355 done |
386 next |
|
387 case (sinl x) |
|
388 then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.idem) |
|
389 next |
|
390 case (sinr y) |
|
391 then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.idem) |
|
392 qed |
356 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
393 show "ssum_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x" |
357 apply (induct x, simp) |
394 proof (induct x) |
358 apply (case_tac "d1\<cdot>x = \<bottom>", simp, simp add: d1.below) |
395 case bottom |
359 apply (case_tac "d2\<cdot>y = \<bottom>", simp, simp add: d2.below) |
396 then show ?case by simp |
360 done |
397 next |
|
398 case (sinl x) |
|
399 then show ?case by (cases "d1\<cdot>x = \<bottom>") (simp_all add: d1.below) |
|
400 next |
|
401 case (sinr y) |
|
402 then show ?case by (cases "d2\<cdot>y = \<bottom>") (simp_all add: d2.below) |
|
403 qed |
361 qed |
404 qed |
362 |
405 |
363 lemma finite_deflation_ssum_map: |
406 lemma finite_deflation_ssum_map: |
364 assumes "finite_deflation d1" and "finite_deflation d2" |
407 assumes "finite_deflation d1" and "finite_deflation d2" |
365 shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |
408 shows "finite_deflation (ssum_map\<cdot>d1\<cdot>d2)" |