456 done |
456 done |
457 thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}" |
457 thus "finite {xs. lower_map\<cdot>d\<cdot>xs = xs}" |
458 by (rule finite_range_imp_finite_fixes) |
458 by (rule finite_range_imp_finite_fixes) |
459 qed |
459 qed |
460 |
460 |
461 subsection {* Lower powerdomain is a domain *} |
461 subsection {* Lower powerdomain is bifinite *} |
462 |
462 |
463 lemma approx_chain_lower_map: |
463 lemma approx_chain_lower_map: |
464 assumes "approx_chain a" |
464 assumes "approx_chain a" |
465 shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))" |
465 shows "approx_chain (\<lambda>i. lower_map\<cdot>(a i))" |
466 using assms unfolding approx_chain_def |
466 using assms unfolding approx_chain_def |
471 show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a" |
471 show "\<exists>(a::nat \<Rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd). approx_chain a" |
472 using bifinite [where 'a='a] |
472 using bifinite [where 'a='a] |
473 by (fast intro!: approx_chain_lower_map) |
473 by (fast intro!: approx_chain_lower_map) |
474 qed |
474 qed |
475 |
475 |
476 definition |
|
477 lower_approx :: "nat \<Rightarrow> udom lower_pd \<rightarrow> udom lower_pd" |
|
478 where |
|
479 "lower_approx = (\<lambda>i. lower_map\<cdot>(udom_approx i))" |
|
480 |
|
481 lemma lower_approx: "approx_chain lower_approx" |
|
482 using lower_map_ID finite_deflation_lower_map |
|
483 unfolding lower_approx_def by (rule approx_chain_lemma1) |
|
484 |
|
485 definition lower_defl :: "udom defl \<rightarrow> udom defl" |
|
486 where "lower_defl = defl_fun1 lower_approx lower_map" |
|
487 |
|
488 lemma cast_lower_defl: |
|
489 "cast\<cdot>(lower_defl\<cdot>A) = |
|
490 udom_emb lower_approx oo lower_map\<cdot>(cast\<cdot>A) oo udom_prj lower_approx" |
|
491 using lower_approx finite_deflation_lower_map |
|
492 unfolding lower_defl_def by (rule cast_defl_fun1) |
|
493 |
|
494 instantiation lower_pd :: ("domain") liftdomain |
|
495 begin |
|
496 |
|
497 definition |
|
498 "emb = udom_emb lower_approx oo lower_map\<cdot>emb" |
|
499 |
|
500 definition |
|
501 "prj = lower_map\<cdot>prj oo udom_prj lower_approx" |
|
502 |
|
503 definition |
|
504 "defl (t::'a lower_pd itself) = lower_defl\<cdot>DEFL('a)" |
|
505 |
|
506 definition |
|
507 "(liftemb :: 'a lower_pd u \<rightarrow> udom) = udom_emb u_approx oo u_map\<cdot>emb" |
|
508 |
|
509 definition |
|
510 "(liftprj :: udom \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj oo udom_prj u_approx" |
|
511 |
|
512 definition |
|
513 "liftdefl (t::'a lower_pd itself) = u_defl\<cdot>DEFL('a lower_pd)" |
|
514 |
|
515 instance |
|
516 using liftemb_lower_pd_def liftprj_lower_pd_def liftdefl_lower_pd_def |
|
517 proof (rule liftdomain_class_intro) |
|
518 show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)" |
|
519 unfolding emb_lower_pd_def prj_lower_pd_def |
|
520 using ep_pair_udom [OF lower_approx] |
|
521 by (intro ep_pair_comp ep_pair_lower_map ep_pair_emb_prj) |
|
522 next |
|
523 show "cast\<cdot>DEFL('a lower_pd) = emb oo (prj :: udom \<rightarrow> 'a lower_pd)" |
|
524 unfolding emb_lower_pd_def prj_lower_pd_def defl_lower_pd_def cast_lower_defl |
|
525 by (simp add: cast_DEFL oo_def cfun_eq_iff lower_map_map) |
|
526 qed |
|
527 |
|
528 end |
|
529 |
|
530 lemma DEFL_lower: "DEFL('a::domain lower_pd) = lower_defl\<cdot>DEFL('a)" |
|
531 by (rule defl_lower_pd_def) |
|
532 |
|
533 |
|
534 subsection {* Join *} |
476 subsection {* Join *} |
535 |
477 |
536 definition |
478 definition |
537 lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where |
479 lower_join :: "'a lower_pd lower_pd \<rightarrow> 'a lower_pd" where |
538 "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" |
480 "lower_join = (\<Lambda> xss. lower_bind\<cdot>xss\<cdot>(\<Lambda> xs. xs))" |