9 begin |
9 begin |
10 |
10 |
11 subsection {* Class of bifinite domains *} |
11 subsection {* Class of bifinite domains *} |
12 |
12 |
13 text {* |
13 text {* |
14 We define a bifinite domain as a pcpo that is isomorphic to some |
14 We define a ``domain'' as a pcpo that is isomorphic to some |
15 algebraic deflation over the universal domain. |
15 algebraic deflation over the universal domain; this is equivalent |
16 |
16 to being omega-bifinite. |
17 A predomain is a cpo that, when lifted, becomes bifinite. |
17 |
|
18 A predomain is a cpo that, when lifted, becomes a domain. |
18 *} |
19 *} |
19 |
20 |
20 class predomain = cpo + |
21 class predomain = cpo + |
21 fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl" |
22 fixes liftdefl :: "('a::cpo) itself \<Rightarrow> defl" |
22 fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom" |
23 fixes liftemb :: "'a\<^sub>\<bottom> \<rightarrow> udom" |
25 assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj" |
26 assumes cast_liftdefl: "cast\<cdot>(liftdefl TYPE('a::cpo)) = liftemb oo liftprj" |
26 |
27 |
27 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))") |
28 syntax "_LIFTDEFL" :: "type \<Rightarrow> logic" ("(1LIFTDEFL/(1'(_')))") |
28 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)" |
29 translations "LIFTDEFL('t)" \<rightleftharpoons> "CONST liftdefl TYPE('t)" |
29 |
30 |
30 class bifinite = predomain + pcpo + |
31 class "domain" = predomain + pcpo + |
31 fixes emb :: "'a::cpo \<rightarrow> udom" |
32 fixes emb :: "'a::cpo \<rightarrow> udom" |
32 fixes prj :: "udom \<rightarrow> 'a::cpo" |
33 fixes prj :: "udom \<rightarrow> 'a::cpo" |
33 fixes defl :: "'a itself \<Rightarrow> defl" |
34 fixes defl :: "'a itself \<Rightarrow> defl" |
34 assumes ep_pair_emb_prj: "ep_pair emb prj" |
35 assumes ep_pair_emb_prj: "ep_pair emb prj" |
35 assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" |
36 assumes cast_DEFL: "cast\<cdot>(defl TYPE('a)) = emb oo prj" |
36 |
37 |
37 syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))") |
38 syntax "_DEFL" :: "type \<Rightarrow> defl" ("(1DEFL/(1'(_')))") |
38 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" |
39 translations "DEFL('t)" \<rightleftharpoons> "CONST defl TYPE('t)" |
39 |
40 |
40 interpretation bifinite: pcpo_ep_pair emb prj |
41 interpretation "domain": pcpo_ep_pair emb prj |
41 unfolding pcpo_ep_pair_def |
42 unfolding pcpo_ep_pair_def |
42 by (rule ep_pair_emb_prj) |
43 by (rule ep_pair_emb_prj) |
43 |
44 |
44 lemmas emb_inverse = bifinite.e_inverse |
45 lemmas emb_inverse = domain.e_inverse |
45 lemmas emb_prj_below = bifinite.e_p_below |
46 lemmas emb_prj_below = domain.e_p_below |
46 lemmas emb_eq_iff = bifinite.e_eq_iff |
47 lemmas emb_eq_iff = domain.e_eq_iff |
47 lemmas emb_strict = bifinite.e_strict |
48 lemmas emb_strict = domain.e_strict |
48 lemmas prj_strict = bifinite.p_strict |
49 lemmas prj_strict = domain.p_strict |
49 |
50 |
50 subsection {* Bifinite domains have a countable compact basis *} |
51 subsection {* Domains have a countable compact basis *} |
51 |
52 |
52 text {* |
53 text {* |
53 Eventually it should be possible to generalize this to an unpointed |
54 Eventually it should be possible to generalize this to an unpointed |
54 variant of the bifinite class. |
55 variant of the domain class. |
55 *} |
56 *} |
56 |
57 |
57 interpretation compact_basis: |
58 interpretation compact_basis: |
58 ideal_completion below Rep_compact_basis "approximants::'a::bifinite \<Rightarrow> _" |
59 ideal_completion below Rep_compact_basis "approximants::'a::domain \<Rightarrow> _" |
59 proof - |
60 proof - |
60 obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
61 obtain Y where Y: "\<forall>i. Y i \<sqsubseteq> Y (Suc i)" |
61 and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))" |
62 and DEFL: "DEFL('a) = (\<Squnion>i. defl_principal (Y i))" |
62 by (rule defl.obtain_principal_chain) |
63 by (rule defl.obtain_principal_chain) |
63 def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a" |
64 def approx \<equiv> "\<lambda>i. (prj oo cast\<cdot>(defl_principal (Y i)) oo emb) :: 'a \<rightarrow> 'a" |
68 show "(\<Squnion>i. approx i) = ID" |
69 show "(\<Squnion>i. approx i) = ID" |
69 unfolding approx_def |
70 unfolding approx_def |
70 by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff) |
71 by (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL cfun_eq_iff) |
71 show "\<And>i. finite_deflation (approx i)" |
72 show "\<And>i. finite_deflation (approx i)" |
72 unfolding approx_def |
73 unfolding approx_def |
73 apply (rule bifinite.finite_deflation_p_d_e) |
74 apply (rule domain.finite_deflation_p_d_e) |
74 apply (rule finite_deflation_cast) |
75 apply (rule finite_deflation_cast) |
75 apply (rule defl.compact_principal) |
76 apply (rule defl.compact_principal) |
76 apply (rule below_trans [OF monofun_cfun_fun]) |
77 apply (rule below_trans [OF monofun_cfun_fun]) |
77 apply (rule is_ub_thelub, simp add: Y) |
78 apply (rule is_ub_thelub, simp add: Y) |
78 apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL) |
79 apply (simp add: lub_distribs Y DEFL [symmetric] cast_DEFL) |
252 "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = |
253 "cast\<cdot>(ssum_defl\<cdot>A\<cdot>B) = |
253 udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx" |
254 udom_emb ssum_approx oo ssum_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj ssum_approx" |
254 using ssum_approx finite_deflation_ssum_map |
255 using ssum_approx finite_deflation_ssum_map |
255 unfolding ssum_defl_def by (rule cast_defl_fun2) |
256 unfolding ssum_defl_def by (rule cast_defl_fun2) |
256 |
257 |
257 subsection {* Lemma for proving bifinite instances *} |
258 subsection {* Lemma for proving domain instances *} |
258 |
259 |
259 text {* |
260 text {* |
260 A class of bifinite domains where @{const liftemb}, @{const liftprj}, |
261 A class of domains where @{const liftemb}, @{const liftprj}, |
261 and @{const liftdefl} are all defined in the standard way. |
262 and @{const liftdefl} are all defined in the standard way. |
262 *} |
263 *} |
263 |
264 |
264 class liftdomain = bifinite + |
265 class liftdomain = "domain" + |
265 assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\<cdot>emb" |
266 assumes liftemb_eq: "liftemb = udom_emb u_approx oo u_map\<cdot>emb" |
266 assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx" |
267 assumes liftprj_eq: "liftprj = u_map\<cdot>prj oo udom_prj u_approx" |
267 assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)" |
268 assumes liftdefl_eq: "liftdefl TYPE('a::cpo) = u_defl\<cdot>DEFL('a)" |
268 |
269 |
269 text {* Temporarily relax type constraints. *} |
270 text {* Temporarily relax type constraints. *} |
297 |
298 |
298 text {* Restore original type constraints. *} |
299 text {* Restore original type constraints. *} |
299 |
300 |
300 setup {* |
301 setup {* |
301 fold Sign.add_const_constraint |
302 fold Sign.add_const_constraint |
302 [ (@{const_name defl}, SOME @{typ "'a::bifinite itself \<Rightarrow> defl"}) |
303 [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> defl"}) |
303 , (@{const_name emb}, SOME @{typ "'a::bifinite \<rightarrow> udom"}) |
304 , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}) |
304 , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::bifinite"}) |
305 , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"}) |
305 , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"}) |
306 , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> defl"}) |
306 , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"}) |
307 , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom"}) |
307 , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ] |
308 , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ] |
308 *} |
309 *} |
309 |
310 |
310 subsection {* The universal domain is bifinite *} |
311 subsection {* The universal domain is a domain *} |
311 |
312 |
312 instantiation udom :: liftdomain |
313 instantiation udom :: liftdomain |
313 begin |
314 begin |
314 |
315 |
315 definition [simp]: |
316 definition [simp]: |
508 qed |
511 qed |
509 |
512 |
510 end |
513 end |
511 |
514 |
512 lemma DEFL_prod: |
515 lemma DEFL_prod: |
513 "DEFL('a::bifinite \<times> 'b::bifinite) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
516 "DEFL('a::domain \<times> 'b::domain) = prod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)" |
514 by (rule defl_prod_def) |
517 by (rule defl_prod_def) |
515 |
518 |
516 lemma LIFTDEFL_prod: |
519 lemma LIFTDEFL_prod: |
517 "LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)" |
520 "LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)" |
518 by (rule liftdefl_prod_def) |
521 by (rule liftdefl_prod_def) |
519 |
522 |
520 subsection {* Strict product is a bifinite domain *} |
523 subsection {* Strict product is a domain *} |
521 |
524 |
522 instantiation sprod :: (bifinite, bifinite) liftdomain |
525 instantiation sprod :: ("domain", "domain") liftdomain |
523 begin |
526 begin |
524 |
527 |
525 definition |
528 definition |
526 "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb" |
529 "emb = udom_emb sprod_approx oo sprod_map\<cdot>emb\<cdot>emb" |
527 |
530 |